[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
