case intro.intro
ι : Type ?u.342424
α : Type u_1
β : Type ?u.342430
f g : Perm α
x✝ y x : α
hx : ↑f x ≠ x
h : ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f x y
⊢ IsCycle (g * f * g⁻¹)
ι : Type ?u.342424
α : Type u_1
β : Type ?u.342430
f g : Perm α
x y : α
⊢ IsCycle f → IsCycle (g * f * g⁻¹)
rintro ⟨x, hx, h⟩
case intro.intro
ι : Type ?u.342424
α : Type u_1
β : Type ?u.342430
f g : Perm α
x✝ y✝ x : α
hx : ↑f x ≠ x
h : ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f x y
y : α
hy : ↑(g * f * g⁻¹) y ≠ y
⊢ SameCycle (g * f * g⁻¹) (↑g x) y
case intro.intro
ι : Type ?u.342424
α : Type u_1
β : Type ?u.342430
f g : Perm α
x✝ y x : α
hx : ↑f x ≠ x
h : ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f x y
⊢ IsCycle (g * f * g⁻¹)
refine' ⟨g x, by simp [coe_mul, inv_apply_self, hx], fun y hy => _⟩
case intro.intro
ι : Type ?u.342424
α : Type u_1
β : Type ?u.342430
f g : Perm α
x✝ y✝ x : α
hx : ↑f x ≠ x
h : ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f x y
y : α
hy : ↑(g * f * g⁻¹) y ≠ y
⊢ SameCycle (g * f * g⁻¹) (↑g x) (↑g (↑g⁻¹ y))
case intro.intro
ι : Type ?u.342424
α : Type u_1
β : Type ?u.342430
f g : Perm α
x✝ y✝ x : α
hx : ↑f x ≠ x
h : ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f x y
y : α
hy : ↑(g * f * g⁻¹) y ≠ y
⊢ SameCycle (g * f * g⁻¹) (↑g x) y
rw [← apply_inv_self g y]
no goals
case intro.intro
ι : Type ?u.342424
α : Type u_1
β : Type ?u.342430
f g : Perm α
x✝ y✝ x : α
hx : ↑f x ≠ x
h : ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f x y
y : α
hy : ↑(g * f * g⁻¹) y ≠ y
⊢ SameCycle (g * f * g⁻¹) (↑g x) (↑g (↑g⁻¹ y))
exact (h <| eq_inv_iff_eq.not.2 hy).conj
no goals
ι : Type ?u.342424
α : Type u_1
β : Type ?u.342430
f g : Perm α
x✝ y x : α
hx : ↑f x ≠ x
h : ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f x y
⊢ ↑(g * f * g⁻¹) (↑g x) ≠ ↑g x
simp [coe_mul, inv_apply_self, hx]