[GOAL]
α✝ : Type u
β : Type v
α : Type u_1
σ : Perm α
m n : ℤ
x : α
⊢ ↑(σ ^ m) (↑(σ ^ n) x) = ↑(σ ^ n) (↑(σ ^ m) x)
[PROOFSTEP]
rw [← Equiv.Perm.mul_apply, ← Equiv.Perm.mul_apply, zpow_mul_comm]
[GOAL]
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
⊢ Function.Injective ↑(sumCongrHom α β)
[PROOFSTEP]
rintro ⟨⟩ ⟨⟩ h
[GOAL]
case mk.mk
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : ↑(sumCongrHom α β) (fst✝¹, snd✝¹) = ↑(sumCongrHom α β) (fst✝, snd✝)
⊢ (fst✝¹, snd✝¹) = (fst✝, snd✝)
[PROOFSTEP]
rw [Prod.mk.inj_iff]
[GOAL]
case mk.mk
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : ↑(sumCongrHom α β) (fst✝¹, snd✝¹) = ↑(sumCongrHom α β) (fst✝, snd✝)
⊢ fst✝¹ = fst✝ ∧ snd✝¹ = snd✝
[PROOFSTEP]
constructor
[GOAL]
case mk.mk.left
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : ↑(sumCongrHom α β) (fst✝¹, snd✝¹) = ↑(sumCongrHom α β) (fst✝, snd✝)
⊢ fst✝¹ = fst✝
[PROOFSTEP]
ext i
[GOAL]
case mk.mk.right
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : ↑(sumCongrHom α β) (fst✝¹, snd✝¹) = ↑(sumCongrHom α β) (fst✝, snd✝)
⊢ snd✝¹ = snd✝
[PROOFSTEP]
ext i
[GOAL]
case mk.mk.left.H
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : ↑(sumCongrHom α β) (fst✝¹, snd✝¹) = ↑(sumCongrHom α β) (fst✝, snd✝)
i : α
⊢ ↑fst✝¹ i = ↑fst✝ i
[PROOFSTEP]
simpa using Equiv.congr_fun h (Sum.inl i)
[GOAL]
case mk.mk.right.H
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : ↑(sumCongrHom α β) (fst✝¹, snd✝¹) = ↑(sumCongrHom α β) (fst✝, snd✝)
i : β
⊢ ↑snd✝¹ i = ↑snd✝ i
[PROOFSTEP]
simpa using Equiv.congr_fun h (Sum.inr i)
[GOAL]
α✝ : Type u
β✝ : Type v
α : Type u_1
β : α → Type u_2
⊢ Function.Injective ↑(sigmaCongrRightHom β)
[PROOFSTEP]
intro x y h
[GOAL]
α✝ : Type u
β✝ : Type v
α : Type u_1
β : α → Type u_2
x y : (a : α) → Perm (β a)
h : ↑(sigmaCongrRightHom β) x = ↑(sigmaCongrRightHom β) y
⊢ x = y
[PROOFSTEP]
ext a b
[GOAL]
case h.H
α✝ : Type u
β✝ : Type v
α : Type u_1
β : α → Type u_2
x y : (a : α) → Perm (β a)
h : ↑(sigmaCongrRightHom β) x = ↑(sigmaCongrRightHom β) y
a : α
b : β a
⊢ ↑(x a) b = ↑(y a) b
[PROOFSTEP]
simpa using Equiv.congr_fun h ⟨a, b⟩
[GOAL]
α : Type u
β : Type v
p : α → Prop
inst✝ : DecidablePred p
⊢ Function.Injective ↑(subtypeCongrHom p)
[PROOFSTEP]
rintro ⟨⟩ ⟨⟩ h
[GOAL]
case mk.mk
α : Type u
β : Type v
p : α → Prop
inst✝ : DecidablePred p
fst✝¹ : Perm { a // p a }
snd✝¹ : Perm { a // ¬p a }
fst✝ : Perm { a // p a }
snd✝ : Perm { a // ¬p a }
h : ↑(subtypeCongrHom p) (fst✝¹, snd✝¹) = ↑(subtypeCongrHom p) (fst✝, snd✝)
⊢ (fst✝¹, snd✝¹) = (fst✝, snd✝)
[PROOFSTEP]
rw [Prod.mk.inj_iff]
[GOAL]
case mk.mk
α : Type u
β : Type v
p : α → Prop
inst✝ : DecidablePred p
fst✝¹ : Perm { a // p a }
snd✝¹ : Perm { a // ¬p a }
fst✝ : Perm { a // p a }
snd✝ : Perm { a // ¬p a }
h : ↑(subtypeCongrHom p) (fst✝¹, snd✝¹) = ↑(subtypeCongrHom p) (fst✝, snd✝)
⊢ fst✝¹ = fst✝ ∧ snd✝¹ = snd✝
[PROOFSTEP]
constructor
[GOAL]
case mk.mk.left
α : Type u
β : Type v
p : α → Prop
inst✝ : DecidablePred p
fst✝¹ : Perm { a // p a }
snd✝¹ : Perm { a // ¬p a }
fst✝ : Perm { a // p a }
snd✝ : Perm { a // ¬p a }
h : ↑(subtypeCongrHom p) (fst✝¹, snd✝¹) = ↑(subtypeCongrHom p) (fst✝, snd✝)
⊢ fst✝¹ = fst✝
[PROOFSTEP]
ext i
[GOAL]
case mk.mk.right
α : Type u
β : Type v
p : α → Prop
inst✝ : DecidablePred p
fst✝¹ : Perm { a // p a }
snd✝¹ : Perm { a // ¬p a }
fst✝ : Perm { a // p a }
snd✝ : Perm { a // ¬p a }
h : ↑(subtypeCongrHom p) (fst✝¹, snd✝¹) = ↑(subtypeCongrHom p) (fst✝, snd✝)
⊢ snd✝¹ = snd✝
[PROOFSTEP]
ext i
[GOAL]
case mk.mk.left.H.a
α : Type u
β : Type v
p : α → Prop
inst✝ : DecidablePred p
fst✝¹ : Perm { a // p a }
snd✝¹ : Perm { a // ¬p a }
fst✝ : Perm { a // p a }
snd✝ : Perm { a // ¬p a }
h : ↑(subtypeCongrHom p) (fst✝¹, snd✝¹) = ↑(subtypeCongrHom p) (fst✝, snd✝)
i : { a // p a }
⊢ ↑(↑fst✝¹ i) = ↑(↑fst✝ i)
[PROOFSTEP]
simpa using Equiv.congr_fun h i
[GOAL]
case mk.mk.right.H.a
α : Type u
β : Type v
p : α → Prop
inst✝ : DecidablePred p
fst✝¹ : Perm { a // p a }
snd✝¹ : Perm { a // ¬p a }
fst✝ : Perm { a // p a }
snd✝ : Perm { a // ¬p a }
h : ↑(subtypeCongrHom p) (fst✝¹, snd✝¹) = ↑(subtypeCongrHom p) (fst✝, snd✝)
i : { a // ¬p a }
⊢ ↑(↑snd✝¹ i) = ↑(↑snd✝ i)
[PROOFSTEP]
simpa using Equiv.congr_fun h i
[GOAL]
α : Type u
β : Type v
p : α → Prop
f✝ f : Perm α
h : ∀ (x : α), p x ↔ p (↑f x)
x : { x // p x }
⊢ p (↑f (↑f⁻¹ ↑x))
[PROOFSTEP]
simpa using x.2
[GOAL]
α : Type u
β : Type v
p : α → Prop
f✝ f : Perm α
h : ∀ (x : α), p x ↔ p (↑f x)
x✝ : { x // p x }
⊢ (fun x => { val := ↑f⁻¹ ↑x, property := (_ : p (↑f⁻¹ ↑x)) })
      ((fun x => { val := ↑f ↑x, property := (_ : p (↑f ↑x)) }) x✝) =
    x✝
[PROOFSTEP]
simp only [Perm.inv_apply_self, Subtype.coe_eta, Subtype.coe_mk]
[GOAL]
α : Type u
β : Type v
p : α → Prop
f✝ f : Perm α
h : ∀ (x : α), p x ↔ p (↑f x)
x✝ : { x // p x }
⊢ (fun x => { val := ↑f ↑x, property := (_ : p (↑f ↑x)) })
      ((fun x => { val := ↑f⁻¹ ↑x, property := (_ : p (↑f⁻¹ ↑x)) }) x✝) =
    x✝
[PROOFSTEP]
simp only [Perm.apply_inv_self, Subtype.coe_eta, Subtype.coe_mk]
[GOAL]
α : Type u
β : Type v
p : α → Prop
f : Perm α
⊢ (∀ (x : α), p (↑f⁻¹ x) ↔ p (↑f (↑f⁻¹ x))) ↔ ∀ (x : α), p x ↔ p (↑f⁻¹ x)
[PROOFSTEP]
simp_rw [f.apply_inv_self, Iff.comm]
[GOAL]
α : Type u
β : Type v
p : α → Prop
f✝ f : Perm α
n : ℕ
hf : ∀ (x : α), p x ↔ p (↑f x)
⊢ subtypePerm f hf ^ n = subtypePerm (f ^ n) (_ : ∀ (x : α), p x ↔ p (↑(f ^ n) x))
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
α : Type u
β : Type v
p : α → Prop
f✝ f : Perm α
hf : ∀ (x : α), p x ↔ p (↑f x)
⊢ subtypePerm f hf ^ Nat.zero = subtypePerm (f ^ Nat.zero) (_ : ∀ (x : α), p x ↔ p (↑(f ^ Nat.zero) x))
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u
β : Type v
p : α → Prop
f✝ f : Perm α
hf : ∀ (x : α), p x ↔ p (↑f x)
n : ℕ
ih : subtypePerm f hf ^ n = subtypePerm (f ^ n) (_ : ∀ (x : α), p x ↔ p (↑(f ^ n) x))
⊢ subtypePerm f hf ^ Nat.succ n = subtypePerm (f ^ Nat.succ n) (_ : ∀ (x : α), p x ↔ p (↑(f ^ Nat.succ n) x))
[PROOFSTEP]
simp_rw [pow_succ', ih, subtypePerm_mul]
[GOAL]
α : Type u
β : Type v
p : α → Prop
f : Perm α
hf : ∀ (x : α), p x ↔ p (↑f x)
n : ℕ
⊢ ∀ (x : α), p x ↔ p (↑(f ^ Int.negSucc n) x)
[PROOFSTEP]
rw [zpow_negSucc]
[GOAL]
α : Type u
β : Type v
p : α → Prop
f : Perm α
hf : ∀ (x : α), p x ↔ p (↑f x)
n : ℕ
⊢ ∀ (x : α), p x ↔ p (↑(f ^ (n + 1))⁻¹ x)
[PROOFSTEP]
exact inv_aux.1 (pow_aux hf)
[GOAL]
α : Type u
β : Type v
p : α → Prop
f✝ f : Perm α
n : ℤ
hf : ∀ (x : α), p x ↔ p (↑f x)
⊢ subtypePerm f hf ^ n = subtypePerm (f ^ n) (_ : ∀ (x : α), p x ↔ p (↑(f ^ n) x))
[PROOFSTEP]
induction' n with n ih
[GOAL]
case ofNat
α : Type u
β : Type v
p : α → Prop
f✝ f : Perm α
hf : ∀ (x : α), p x ↔ p (↑f x)
n : ℕ
⊢ subtypePerm f hf ^ Int.ofNat n = subtypePerm (f ^ Int.ofNat n) (_ : ∀ (x : α), p x ↔ p (↑(f ^ Int.ofNat n) x))
[PROOFSTEP]
exact subtypePerm_pow _ _ _
[GOAL]
case negSucc
α : Type u
β : Type v
p : α → Prop
f✝ f : Perm α
hf : ∀ (x : α), p x ↔ p (↑f x)
ih : ℕ
⊢ subtypePerm f hf ^ Int.negSucc ih =
    subtypePerm (f ^ Int.negSucc ih) (_ : ∀ (x : α), p x ↔ p (↑(f ^ Int.negSucc ih) x))
[PROOFSTEP]
simp only [zpow_negSucc, subtypePerm_pow, subtypePerm_inv]
[GOAL]
α : Type u
β : Type v
p : α → Prop
f✝ : Perm α
inst✝ : DecidablePred p
a : α
f : Perm α
h₁ : ∀ (x : α), p x ↔ p (↑f x)
h₂ : ∀ (x : α), ↑f x ≠ x → p x
x : α
⊢ ↑(↑ofSubtype (subtypePerm f h₁)) x = ↑f x
[PROOFSTEP]
by_cases hx : p x
[GOAL]
case pos
α : Type u
β : Type v
p : α → Prop
f✝ : Perm α
inst✝ : DecidablePred p
a : α
f : Perm α
h₁ : ∀ (x : α), p x ↔ p (↑f x)
h₂ : ∀ (x : α), ↑f x ≠ x → p x
x : α
hx : p x
⊢ ↑(↑ofSubtype (subtypePerm f h₁)) x = ↑f x
[PROOFSTEP]
exact (subtypePerm f h₁).extendDomain_apply_subtype _ hx
[GOAL]
case neg
α : Type u
β : Type v
p : α → Prop
f✝ : Perm α
inst✝ : DecidablePred p
a : α
f : Perm α
h₁ : ∀ (x : α), p x ↔ p (↑f x)
h₂ : ∀ (x : α), ↑f x ≠ x → p x
x : α
hx : ¬p x
⊢ ↑(↑ofSubtype (subtypePerm f h₁)) x = ↑f x
[PROOFSTEP]
rw [ofSubtype, MonoidHom.coe_mk]
  -- Porting note: added `dsimp`
[GOAL]
case neg
α : Type u
β : Type v
p : α → Prop
f✝ : Perm α
inst✝ : DecidablePred p
a : α
f : Perm α
h₁ : ∀ (x : α), p x ↔ p (↑f x)
h₂ : ∀ (x : α), ↑f x ≠ x → p x
x : α
hx : ¬p x
⊢ ↑(↑{ toFun := fun f => extendDomain f (Equiv.refl { x // p x }),
              map_one' := (_ : extendDomain 1 (Equiv.refl { x // p x }) = 1) }
          (subtypePerm f h₁))
      x =
    ↑f x
[PROOFSTEP]
dsimp only [OneHom.coe_mk]
[GOAL]
case neg
α : Type u
β : Type v
p : α → Prop
f✝ : Perm α
inst✝ : DecidablePred p
a : α
f : Perm α
h₁ : ∀ (x : α), p x ↔ p (↑f x)
h₂ : ∀ (x : α), ↑f x ≠ x → p x
x : α
hx : ¬p x
⊢ ↑(extendDomain (subtypePerm f h₁) (Equiv.refl { x // p x })) x = ↑f x
[PROOFSTEP]
rw [Equiv.Perm.extendDomain_apply_not_subtype _ _ hx]
[GOAL]
case neg
α : Type u
β : Type v
p : α → Prop
f✝ : Perm α
inst✝ : DecidablePred p
a : α
f : Perm α
h₁ : ∀ (x : α), p x ↔ p (↑f x)
h₂ : ∀ (x : α), ↑f x ≠ x → p x
x : α
hx : ¬p x
⊢ x = ↑f x
[PROOFSTEP]
exact not_not.mp fun h => hx (h₂ x (Ne.symm h))
[GOAL]
α : Type u
β : Type v
p : α → Prop
f✝ : Perm α
inst✝ : DecidablePred p
a : α
f : Perm (Subtype p)
x : α
h : p x
⊢ p x ↔ p (↑(↑ofSubtype f) x)
[PROOFSTEP]
simpa only [h, true_iff_iff, MonoidHom.coe_mk, ofSubtype_apply_of_mem f h] using (f ⟨x, h⟩).2
[GOAL]
α : Type u
β : Type v
p : α → Prop
f✝ : Perm α
inst✝ : DecidablePred p
a : α
f : Perm (Subtype p)
x : α
h : ¬p x
⊢ p x ↔ p (↑(↑ofSubtype f) x)
[PROOFSTEP]
simp [h, ofSubtype_apply_of_not_mem f h]
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
f : Perm α
x y z : α
⊢ ↑(swap x y * f) z = ↑(f * swap (↑f⁻¹ x) (↑f⁻¹ y)) z
[PROOFSTEP]
simp only [Perm.mul_apply, swap_apply_def]
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
f : Perm α
x y z : α
⊢ (if ↑f z = x then y else if ↑f z = y then x else ↑f z) =
    ↑f (if z = ↑f⁻¹ x then ↑f⁻¹ y else if z = ↑f⁻¹ y then ↑f⁻¹ x else z)
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
f : Perm α
x y z : α
h✝¹ : ↑f z = x
h✝ : z = ↑f⁻¹ x
⊢ y = ↑f (↑f⁻¹ y)
[PROOFSTEP]
simp_all only [Perm.apply_inv_self, Perm.eq_inv_iff_eq, eq_self_iff_true, not_true]
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
f : Perm α
x y z : α
h✝² : ↑f z = x
h✝¹ : ¬z = ↑f⁻¹ x
h✝ : z = ↑f⁻¹ y
⊢ y = ↑f (↑f⁻¹ x)
[PROOFSTEP]
simp_all only [Perm.apply_inv_self, Perm.eq_inv_iff_eq, eq_self_iff_true, not_true]
[GOAL]
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
f : Perm α
x y z : α
h✝² : ↑f z = x
h✝¹ : ¬z = ↑f⁻¹ x
h✝ : ¬z = ↑f⁻¹ y
⊢ y = ↑f z
[PROOFSTEP]
simp_all only [Perm.apply_inv_self, Perm.eq_inv_iff_eq, eq_self_iff_true, not_true]
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
f : Perm α
x y z : α
h✝² : ¬↑f z = x
h✝¹ : ↑f z = y
h✝ : z = ↑f⁻¹ x
⊢ x = ↑f (↑f⁻¹ y)
[PROOFSTEP]
simp_all only [Perm.apply_inv_self, Perm.eq_inv_iff_eq, eq_self_iff_true, not_true]
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
f : Perm α
x y z : α
h✝³ : ¬↑f z = x
h✝² : ↑f z = y
h✝¹ : ¬z = ↑f⁻¹ x
h✝ : z = ↑f⁻¹ y
⊢ x = ↑f (↑f⁻¹ x)
[PROOFSTEP]
simp_all only [Perm.apply_inv_self, Perm.eq_inv_iff_eq, eq_self_iff_true, not_true]
[GOAL]
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
f : Perm α
x y z : α
h✝³ : ¬↑f z = x
h✝² : ↑f z = y
h✝¹ : ¬z = ↑f⁻¹ x
h✝ : ¬z = ↑f⁻¹ y
⊢ x = ↑f z
[PROOFSTEP]
simp_all only [Perm.apply_inv_self, Perm.eq_inv_iff_eq, eq_self_iff_true, not_true]
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
f : Perm α
x y z : α
h✝² : ¬↑f z = x
h✝¹ : ¬↑f z = y
h✝ : z = ↑f⁻¹ x
⊢ ↑f z = ↑f (↑f⁻¹ y)
[PROOFSTEP]
simp_all only [Perm.apply_inv_self, Perm.eq_inv_iff_eq, eq_self_iff_true, not_true]
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
f : Perm α
x y z : α
h✝³ : ¬↑f z = x
h✝² : ¬↑f z = y
h✝¹ : ¬z = ↑f⁻¹ x
h✝ : z = ↑f⁻¹ y
⊢ ↑f z = ↑f (↑f⁻¹ x)
[PROOFSTEP]
simp_all only [Perm.apply_inv_self, Perm.eq_inv_iff_eq, eq_self_iff_true, not_true]
[GOAL]
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
f : Perm α
x y z : α
h✝³ : ¬↑f z = x
h✝² : ¬↑f z = y
h✝¹ : ¬z = ↑f⁻¹ x
h✝ : ¬z = ↑f⁻¹ y
⊢ ↑f z = ↑f z
[PROOFSTEP]
simp_all only [Perm.apply_inv_self, Perm.eq_inv_iff_eq, eq_self_iff_true, not_true]
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
f : Perm α
x y : α
⊢ f * swap x y = swap (↑f x) (↑f y) * f
[PROOFSTEP]
rw [swap_mul_eq_mul_swap, Perm.inv_apply_self, Perm.inv_apply_self]
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
f : Perm α
x y : α
⊢ swap (↑f x) (↑f y) = f * swap x y * f⁻¹
[PROOFSTEP]
rw [mul_swap_eq_swap_mul, mul_inv_cancel_right]
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
i j : α
σ : Perm α
⊢ swap i j * (swap i j * σ) = σ
[PROOFSTEP]
rw [← mul_assoc, swap_mul_self, one_mul]
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
i j : α
σ : Perm α
⊢ σ * swap i j * swap i j = σ
[PROOFSTEP]
rw [mul_assoc, swap_mul_self, mul_one]
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
i j : α
σ : Perm α
h : swap i j * σ = σ
⊢ i = j
[PROOFSTEP]
have swap_id : swap i j = 1 := mul_right_cancel (_root_.trans h (one_mul σ).symm)
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
i j : α
σ : Perm α
h : swap i j * σ = σ
swap_id : swap i j = 1
⊢ i = j
[PROOFSTEP]
rw [← swap_apply_right i j, swap_id]
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
i j : α
σ : Perm α
h : swap i j * σ = σ
swap_id : swap i j = 1
⊢ ↑1 j = j
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
i j : α
σ : Perm α
h : i = j
⊢ swap i j * σ = σ
[PROOFSTEP]
erw [h, swap_self, one_mul]
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
i j : α
σ : Perm α
h : σ * swap i j = σ
⊢ i = j
[PROOFSTEP]
have swap_id : swap i j = 1 := mul_left_cancel (_root_.trans h (one_mul σ).symm)
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
i j : α
σ : Perm α
h : σ * swap i j = σ
swap_id : swap i j = 1
⊢ i = j
[PROOFSTEP]
rw [← swap_apply_right i j, swap_id]
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
i j : α
σ : Perm α
h : σ * swap i j = σ
swap_id : swap i j = 1
⊢ ↑1 j = j
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
i j : α
σ : Perm α
h : i = j
⊢ σ * swap i j = σ
[PROOFSTEP]
erw [h, swap_self, mul_one]
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
x y z : α
hwz : x ≠ y
hxz : x ≠ z
n : α
⊢ ↑(swap y z * swap x y * swap y z) n = ↑(swap z x) n
[PROOFSTEP]
simp only [swap_apply_def, Perm.mul_apply]
  -- Porting note: was `cc`
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
x y z : α
hwz : x ≠ y
hxz : x ≠ z
n : α
⊢ (if
        (if (if n = y then z else if n = z then y else n) = x then y
          else
            if (if n = y then z else if n = z then y else n) = y then x
            else if n = y then z else if n = z then y else n) =
          y then
      z
    else
      if
          (if (if n = y then z else if n = z then y else n) = x then y
            else
              if (if n = y then z else if n = z then y else n) = y then x
              else if n = y then z else if n = z then y else n) =
            z then
        y
      else
        if (if n = y then z else if n = z then y else n) = x then y
        else
          if (if n = y then z else if n = z then y else n) = y then x
          else if n = y then z else if n = z then y else n) =
    if n = z then x else if n = x then z else n
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
x y z : α
hwz : x ≠ y
hxz : x ≠ z
n : α
h✝³ : n = y
h✝² : z = x
h✝¹ : y = y
h✝ : n = z
⊢ z = x
[PROOFSTEP]
aesop
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
x y z : α
hwz : x ≠ y
hxz : x ≠ z
n : α
h✝⁴ : n = y
h✝³ : z = x
h✝² : y = y
h✝¹ : ¬n = z
h✝ : n = x
⊢ z = z
[PROOFSTEP]
aesop
[GOAL]
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
x y z : α
hwz : x ≠ y
hxz : x ≠ z
n : α
h✝⁴ : n = y
h✝³ : z = x
h✝² : y = y
h✝¹ : ¬n = z
h✝ : ¬n = x
⊢ z = n
[PROOFSTEP]
aesop
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
x y z : α
hwz : x ≠ y
hxz : x ≠ z
n : α
h✝⁴ : n = y
h✝³ : z = x
h✝² : ¬y = y
h✝¹ : y = z
h✝ : n = z
⊢ y = x
[PROOFSTEP]
aesop
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
x y z : α
hwz : x ≠ y
hxz : x ≠ z
n : α
h✝⁵ : n = y
h✝⁴ : z = x
h✝³ : ¬y = y
h✝² : y = z
h✝¹ : ¬n = z
h✝ : n = x
⊢ y = z
[PROOFSTEP]
aesop
[GOAL]
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
x y z : α
hwz : x ≠ y
hxz : x ≠ z
n : α
h✝⁵ : n = y
h✝⁴ : z = x
h✝³ : ¬y = y
h✝² : y = z
h✝¹ : ¬n = z
h✝ : ¬n = x
⊢ y = n
[PROOFSTEP]
aesop
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
x y z : α
hwz : x ≠ y
hxz : x ≠ z
n : α
h✝⁴ : n = y
h✝³ : z = x
h✝² : ¬y = y
h✝¹ : ¬y = z
h✝ : n = z
⊢ y = x
[PROOFSTEP]
aesop
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
x y z : α
hwz : x ≠ y
hxz : x ≠ z
n : α
h✝⁵ : n = y
h✝⁴ : z = x
h✝³ : ¬y = y
h✝² : ¬y = z
h✝¹ : ¬n = z
h✝ : n = x
⊢ y = z
[PROOFSTEP]
aesop
[GOAL]
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
x y z : α
hwz : x ≠ y
hxz : x ≠ z
n : α
h✝⁵ : n = y
h✝⁴ : z = x
h✝³ : ¬y = y
h✝² : ¬y = z
h✝¹ : ¬n = z
h✝ : ¬n = x
⊢ y = n
[PROOFSTEP]
aesop
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
x y z : α
hwz : x ≠ y
hxz : x ≠ z
n : α
h✝³ : n = y
h✝² : ¬z = x
h✝¹ : z = y
h✝ : n = z
⊢ x = x
[PROOFSTEP]
aesop
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
x y z : α
hwz : x ≠ y
hxz : x ≠ z
n : α
h✝⁴ : n = y
h✝³ : ¬z = x
h✝² : z = y
h✝¹ : ¬n = z
h✝ : n = x
⊢ x = z
[PROOFSTEP]
aesop
[GOAL]
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
x y z : α
hwz : x ≠ y
hxz : x ≠ z
n : α
h✝⁴ : n = y
h✝³ : ¬z = x
h✝² : z = y
h✝¹ : ¬n = z
h✝ : ¬n = x
⊢ x = n
[PROOFSTEP]
aesop
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
x y z : α
hwz : x ≠ y
hxz : x ≠ z
n : α
h✝⁴ : n = y
h✝³ : ¬z = x
h✝² : ¬z = y
h✝¹ : z = z
h✝ : n = z
⊢ y = x
[PROOFSTEP]
aesop
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
x y z : α
hwz : x ≠ y
hxz : x ≠ z
n : α
h✝⁵ : n = y
h✝⁴ : ¬z = x
h✝³ : ¬z = y
h✝² : z = z
h✝¹ : ¬n = z
h✝ : n = x
⊢ y = z
[PROOFSTEP]
aesop
[GOAL]
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
x y z : α
hwz : x ≠ y
hxz : x ≠ z
n : α
h✝⁵ : n = y
h✝⁴ : ¬z = x
h✝³ : ¬z = y
h✝² : z = z
h✝¹ : ¬n = z
h✝ : ¬n = x
⊢ y = n
[PROOFSTEP]
aesop
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
x y z : α
hwz : x ≠ y
hxz : x ≠ z
n : α
h✝⁴ : n = y
h✝³ : ¬z = x
h✝² : ¬z = y
h✝¹ : ¬z = z
h✝ : n = z
⊢ z = x
[PROOFSTEP]
aesop
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
x y z : α
hwz : x ≠ y
hxz : x ≠ z
n : α
h✝⁵ : n = y
h✝⁴ : ¬z = x
h✝³ : ¬z = y
h✝² : ¬z = z
h✝¹ : ¬n = z
h✝ : n = x
⊢ z = z
[PROOFSTEP]
aesop
[GOAL]
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
x y z : α
hwz : x ≠ y
hxz : x ≠ z
n : α
h✝⁵ : n = y
h✝⁴ : ¬z = x
h✝³ : ¬z = y
h✝² : ¬z = z
h✝¹ : ¬n = z
h✝ : ¬n = x
⊢ z = n
[PROOFSTEP]
aesop
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
x y z : α
hwz : x ≠ y
hxz : x ≠ z
n : α
h✝³ : ¬n = y
h✝² : n = z
h✝¹ : y = x
h✝ : y = y
⊢ z = x
[PROOFSTEP]
aesop
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
x y z : α
hwz : x ≠ y
hxz : x ≠ z
n : α
h✝⁴ : ¬n = y
h✝³ : n = z
h✝² : y = x
h✝¹ : ¬y = y
h✝ : y = z
⊢ y = x
[PROOFSTEP]
aesop
[GOAL]
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
x y z : α
hwz : x ≠ y
hxz : x ≠ z
n : α
h✝⁴ : ¬n = y
h✝³ : n = z
h✝² : y = x
h✝¹ : ¬y = y
h✝ : ¬y = z
⊢ y = x
[PROOFSTEP]
aesop
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
x y z : α
hwz : x ≠ y
hxz : x ≠ z
n : α
h✝³ : ¬n = y
h✝² : n = z
h✝¹ : ¬y = x
h✝ : y = y
⊢ x = x
[PROOFSTEP]
aesop
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
x y z : α
hwz : x ≠ y
hxz : x ≠ z
n : α
h✝⁴ : ¬n = y
h✝³ : n = z
h✝² : ¬y = x
h✝¹ : ¬y = y
h✝ : y = z
⊢ y = x
[PROOFSTEP]
aesop
[GOAL]
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
x y z : α
hwz : x ≠ y
hxz : x ≠ z
n : α
h✝⁴ : ¬n = y
h✝³ : n = z
h✝² : ¬y = x
h✝¹ : ¬y = y
h✝ : ¬y = z
⊢ y = x
[PROOFSTEP]
aesop
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
x y z : α
hwz : x ≠ y
hxz : x ≠ z
n : α
h✝³ : ¬n = y
h✝² : ¬n = z
h✝¹ : n = x
h✝ : y = y
⊢ z = z
[PROOFSTEP]
aesop
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
x y z : α
hwz : x ≠ y
hxz : x ≠ z
n : α
h✝⁴ : ¬n = y
h✝³ : ¬n = z
h✝² : n = x
h✝¹ : ¬y = y
h✝ : y = z
⊢ y = z
[PROOFSTEP]
aesop
[GOAL]
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
x y z : α
hwz : x ≠ y
hxz : x ≠ z
n : α
h✝⁴ : ¬n = y
h✝³ : ¬n = z
h✝² : n = x
h✝¹ : ¬y = y
h✝ : ¬y = z
⊢ y = z
[PROOFSTEP]
aesop
[GOAL]
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
x y z : α
hwz : x ≠ y
hxz : x ≠ z
n : α
h✝² : ¬n = y
h✝¹ : ¬n = z
h✝ : ¬n = x
⊢ n = n
[PROOFSTEP]
aesop
[GOAL]
α : Type u
β : Type v
inst✝ : AddGroup α
a b : α
n : ℕ
⊢ Equiv.addLeft a ^ n = Equiv.addLeft (n • a)
[PROOFSTEP]
ext
[GOAL]
case H
α : Type u
β : Type v
inst✝ : AddGroup α
a b : α
n : ℕ
x✝ : α
⊢ ↑(Equiv.addLeft a ^ n) x✝ = ↑(Equiv.addLeft (n • a)) x✝
[PROOFSTEP]
simp [Perm.coe_pow]
[GOAL]
α : Type u
β : Type v
inst✝ : AddGroup α
a b : α
n : ℕ
⊢ Equiv.addRight a ^ n = Equiv.addRight (n • a)
[PROOFSTEP]
ext
[GOAL]
case H
α : Type u
β : Type v
inst✝ : AddGroup α
a b : α
n : ℕ
x✝ : α
⊢ ↑(Equiv.addRight a ^ n) x✝ = ↑(Equiv.addRight (n • a)) x✝
[PROOFSTEP]
simp [Perm.coe_pow]
[GOAL]
α : Type u
β : Type v
inst✝ : AddGroup α
a b : α
n : ℕ
⊢ Equiv.addRight a ^ Int.ofNat n = Equiv.addRight (Int.ofNat n • a)
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
inst✝ : AddGroup α
a b : α
n : ℕ
⊢ Equiv.addRight a ^ Int.negSucc n = Equiv.addRight (Int.negSucc n • a)
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
inst✝ : Group α
a b : α
n : ℕ
⊢ Equiv.mulLeft a ^ n = Equiv.mulLeft (a ^ n)
[PROOFSTEP]
ext
[GOAL]
case H
α : Type u
β : Type v
inst✝ : Group α
a b : α
n : ℕ
x✝ : α
⊢ ↑(Equiv.mulLeft a ^ n) x✝ = ↑(Equiv.mulLeft (a ^ n)) x✝
[PROOFSTEP]
simp [Perm.coe_pow]
[GOAL]
α : Type u
β : Type v
inst✝ : Group α
a b : α
n : ℕ
⊢ Equiv.mulRight a ^ n = Equiv.mulRight (a ^ n)
[PROOFSTEP]
ext
[GOAL]
case H
α : Type u
β : Type v
inst✝ : Group α
a b : α
n : ℕ
x✝ : α
⊢ ↑(Equiv.mulRight a ^ n) x✝ = ↑(Equiv.mulRight (a ^ n)) x✝
[PROOFSTEP]
simp [Perm.coe_pow]
[GOAL]
α : Type u
β : Type v
inst✝ : Group α
a b : α
n : ℕ
⊢ Equiv.mulRight a ^ Int.ofNat n = Equiv.mulRight (a ^ Int.ofNat n)
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
inst✝ : Group α
a b : α
n : ℕ
⊢ Equiv.mulRight a ^ Int.negSucc n = Equiv.mulRight (a ^ Int.negSucc n)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
f : Perm α
s : Set α
⊢ MapsTo (↑f) s s → ∀ (n : ℕ), MapsTo (↑(f ^ n)) s s
[PROOFSTEP]
simp_rw [Equiv.Perm.coe_pow]
[GOAL]
α : Type u_1
f : Perm α
s : Set α
⊢ MapsTo (↑f) s s → ∀ (n : ℕ), MapsTo (↑f)^[n] s s
[PROOFSTEP]
exact MapsTo.iterate
[GOAL]
α : Type u_1
f : Perm α
s : Set α
⊢ SurjOn (↑f) s s → ∀ (n : ℕ), SurjOn (↑(f ^ n)) s s
[PROOFSTEP]
simp_rw [Equiv.Perm.coe_pow]
[GOAL]
α : Type u_1
f : Perm α
s : Set α
⊢ SurjOn (↑f) s s → ∀ (n : ℕ), SurjOn (↑f)^[n] s s
[PROOFSTEP]
exact SurjOn.iterate
[GOAL]
α : Type u_1
f : Perm α
s : Set α
⊢ BijOn (↑f) s s → ∀ (n : ℕ), BijOn (↑(f ^ n)) s s
[PROOFSTEP]
simp_rw [Equiv.Perm.coe_pow]
[GOAL]
α : Type u_1
f : Perm α
s : Set α
⊢ BijOn (↑f) s s → ∀ (n : ℕ), BijOn (↑f)^[n] s s
[PROOFSTEP]
exact BijOn.iterate


[GOAL]
p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
⊢ Nat.Prime p
[PROOFSTEP]
have h0 : p ≠ 0 := by
  rintro ⟨⟩
  exact hd 2 Nat.prime_two (dvd_zero _) (pow_zero _)
[GOAL]
p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
⊢ p ≠ 0
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case refl
a : ZMod 0
ha : a ^ (0 - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ 0 - 1 → a ^ ((0 - 1) / q) ≠ 1
⊢ False
[PROOFSTEP]
exact hd 2 Nat.prime_two (dvd_zero _) (pow_zero _)
[GOAL]
p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
h0 : p ≠ 0
⊢ Nat.Prime p
[PROOFSTEP]
have h1 : p ≠ 1 := by
  rintro ⟨⟩
  exact hd 2 Nat.prime_two (dvd_zero _) (pow_zero _)
[GOAL]
p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
h0 : p ≠ 0
⊢ p ≠ 1
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case refl
a : ZMod 1
ha : a ^ (1 - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ 1 - 1 → a ^ ((1 - 1) / q) ≠ 1
h0 : 1 ≠ 0
⊢ False
[PROOFSTEP]
exact hd 2 Nat.prime_two (dvd_zero _) (pow_zero _)
[GOAL]
p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
h0 : p ≠ 0
h1 : p ≠ 1
⊢ Nat.Prime p
[PROOFSTEP]
have hp1 : 1 < p := lt_of_le_of_ne h0.bot_lt h1.symm
[GOAL]
p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
h0 : p ≠ 0
h1 : p ≠ 1
hp1 : 1 < p
⊢ Nat.Prime p
[PROOFSTEP]
have order_of_a : orderOf a = p - 1 :=
  by
  apply orderOf_eq_of_pow_and_pow_div_prime _ ha hd
  exact tsub_pos_of_lt hp1
[GOAL]
p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
h0 : p ≠ 0
h1 : p ≠ 1
hp1 : 1 < p
⊢ orderOf a = p - 1
[PROOFSTEP]
apply orderOf_eq_of_pow_and_pow_div_prime _ ha hd
[GOAL]
p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
h0 : p ≠ 0
h1 : p ≠ 1
hp1 : 1 < p
⊢ 0 < p - 1
[PROOFSTEP]
exact tsub_pos_of_lt hp1
[GOAL]
p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
h0 : p ≠ 0
h1 : p ≠ 1
hp1 : 1 < p
order_of_a : orderOf a = p - 1
⊢ Nat.Prime p
[PROOFSTEP]
haveI : NeZero p := ⟨h0⟩
[GOAL]
p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
h0 : p ≠ 0
h1 : p ≠ 1
hp1 : 1 < p
order_of_a : orderOf a = p - 1
this : NeZero p
⊢ Nat.Prime p
[PROOFSTEP]
rw [Nat.prime_iff_card_units]
  -- Prove cardinality of `Units` of `ZMod p` is both `≤ p-1` and `≥ p-1`
[GOAL]
p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
h0 : p ≠ 0
h1 : p ≠ 1
hp1 : 1 < p
order_of_a : orderOf a = p - 1
this : NeZero p
⊢ Fintype.card (ZMod p)ˣ = p - 1
[PROOFSTEP]
refine' le_antisymm (Nat.card_units_zmod_lt_sub_one hp1) _
[GOAL]
p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
h0 : p ≠ 0
h1 : p ≠ 1
hp1 : 1 < p
order_of_a : orderOf a = p - 1
this : NeZero p
⊢ p - 1 ≤ Fintype.card (ZMod p)ˣ
[PROOFSTEP]
have hp' : p - 2 + 1 = p - 1 := tsub_add_eq_add_tsub hp1
[GOAL]
p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
h0 : p ≠ 0
h1 : p ≠ 1
hp1 : 1 < p
order_of_a : orderOf a = p - 1
this : NeZero p
hp' : p - 2 + 1 = p - 1
⊢ p - 1 ≤ Fintype.card (ZMod p)ˣ
[PROOFSTEP]
let a' : (ZMod p)ˣ := Units.mkOfMulEqOne a (a ^ (p - 2)) (by rw [← pow_succ, hp', ha])
[GOAL]
p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
h0 : p ≠ 0
h1 : p ≠ 1
hp1 : 1 < p
order_of_a : orderOf a = p - 1
this : NeZero p
hp' : p - 2 + 1 = p - 1
⊢ a * a ^ (p - 2) = 1
[PROOFSTEP]
rw [← pow_succ, hp', ha]
[GOAL]
p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
h0 : p ≠ 0
h1 : p ≠ 1
hp1 : 1 < p
order_of_a : orderOf a = p - 1
this : NeZero p
hp' : p - 2 + 1 = p - 1
a' : (ZMod p)ˣ := Units.mkOfMulEqOne a (a ^ (p - 2)) (_ : a * a ^ (p - 2) = 1)
⊢ p - 1 ≤ Fintype.card (ZMod p)ˣ
[PROOFSTEP]
calc
  p - 1 = orderOf a := order_of_a.symm
  _ = orderOf a' := (orderOf_injective (Units.coeHom (ZMod p)) Units.ext a')
  _ ≤ Fintype.card (ZMod p)ˣ := orderOf_le_card_univ


[GOAL]
a k : ℕ
h0 : 0 < a
h1 : a < k
n : ℕ
⊢ π' (k + n) ≤ card (filter Prime (range k)) + card (filter Prime (Ico k (k + n)))
[PROOFSTEP]
rw [primeCounting', count_eq_card_filter_range, range_eq_Ico, ← Ico_union_Ico_eq_Ico (zero_le k) le_self_add,
  filter_union]
[GOAL]
a k : ℕ
h0 : 0 < a
h1 : a < k
n : ℕ
⊢ card (filter Prime (Ico 0 k) ∪ filter Prime (Ico k (k + n))) ≤
    card (filter Prime (Ico 0 k)) + card (filter Prime (Ico k (k + n)))
[PROOFSTEP]
apply card_union_le
[GOAL]
a k : ℕ
h0 : 0 < a
h1 : a < k
n : ℕ
⊢ card (filter Prime (range k)) + card (filter Prime (Ico k (k + n))) ≤ π' k + card (filter Prime (Ico k (k + n)))
[PROOFSTEP]
rw [primeCounting', count_eq_card_filter_range]
[GOAL]
a k : ℕ
h0 : 0 < a
h1 : a < k
n : ℕ
⊢ π' k + card (filter Prime (Ico k (k + n))) ≤ π' k + card (filter (coprime a) (Ico k (k + n)))
[PROOFSTEP]
refine' add_le_add_left (card_le_of_subset _) k.primeCounting'
[GOAL]
a k : ℕ
h0 : 0 < a
h1 : a < k
n : ℕ
⊢ filter Prime (Ico k (k + n)) ⊆ filter (coprime a) (Ico k (k + n))
[PROOFSTEP]
simp only [subset_iff, and_imp, mem_filter, mem_Ico]
[GOAL]
a k : ℕ
h0 : 0 < a
h1 : a < k
n : ℕ
⊢ ∀ ⦃x : ℕ⦄, k ≤ x → x < k + n → Prime x → (k ≤ x ∧ x < k + n) ∧ coprime a x
[PROOFSTEP]
intro p succ_k_le_p p_lt_n p_prime
[GOAL]
a k : ℕ
h0 : 0 < a
h1 : a < k
n p : ℕ
succ_k_le_p : k ≤ p
p_lt_n : p < k + n
p_prime : Prime p
⊢ (k ≤ p ∧ p < k + n) ∧ coprime a p
[PROOFSTEP]
constructor
[GOAL]
case left
a k : ℕ
h0 : 0 < a
h1 : a < k
n p : ℕ
succ_k_le_p : k ≤ p
p_lt_n : p < k + n
p_prime : Prime p
⊢ k ≤ p ∧ p < k + n
[PROOFSTEP]
exact ⟨succ_k_le_p, p_lt_n⟩
[GOAL]
case right
a k : ℕ
h0 : 0 < a
h1 : a < k
n p : ℕ
succ_k_le_p : k ≤ p
p_lt_n : p < k + n
p_prime : Prime p
⊢ coprime a p
[PROOFSTEP]
rw [coprime_comm]
[GOAL]
case right
a k : ℕ
h0 : 0 < a
h1 : a < k
n p : ℕ
succ_k_le_p : k ≤ p
p_lt_n : p < k + n
p_prime : Prime p
⊢ coprime p a
[PROOFSTEP]
exact coprime_of_lt_prime h0 (gt_of_ge_of_gt succ_k_le_p h1) p_prime
[GOAL]
a k : ℕ
h0 : 0 < a
h1 : a < k
n : ℕ
⊢ π' k + card (filter (coprime a) (Ico k (k + n))) ≤ π' k + φ a * (n / a + 1)
[PROOFSTEP]
rw [add_le_add_iff_left]
[GOAL]
a k : ℕ
h0 : 0 < a
h1 : a < k
n : ℕ
⊢ card (filter (coprime a) (Ico k (k + n))) ≤ φ a * (n / a + 1)
[PROOFSTEP]
exact Ico_filter_coprime_le k n h0