case refine'_1
ι : Type ?u.1652168
α : Type u_1
β : Type ?u.1652174
f g : Perm α
s t : Set α
a b x y : α
hf : IsCycle f
⊢ Set.Nontrivial {x | ↑f x ≠ x}

case refine'_2
ι : Type ?u.1652168
α : Type u_1
β : Type ?u.1652174
f g : Perm α
s t : Set α
a b x y : α
⊢ (∃ s, Set.Nontrivial s ∧ IsCycleOn f s ∧ ∀ ⦃x : α⦄, ¬IsFixedPt (↑f) x → x ∈ s) → IsCycle f
ι : Type ?u.1652168
α : Type u_1
β : Type ?u.1652174
f g : Perm α
s t : Set α
a b x y : α
⊢ IsCycle f ↔ ∃ s, Set.Nontrivial s ∧ IsCycleOn f s ∧ ∀ ⦃x : α⦄, ¬IsFixedPt (↑f) x → x ∈ s
refine' ⟨fun hf => ⟨{ x | f x ≠ x }, _, hf.isCycleOn, fun _ => id⟩, _⟩
case refine'_1.intro
ι : Type ?u.1652168
α : Type u_1
β : Type ?u.1652174
f g : Perm α
s t : Set α
a✝ b x y a : α
ha : ↑f a ≠ a ∧ ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f a y
⊢ Set.Nontrivial {x | ↑f x ≠ x}
case refine'_1
ι : Type ?u.1652168
α : Type u_1
β : Type ?u.1652174
f g : Perm α
s t : Set α
a b x y : α
hf : IsCycle f
⊢ Set.Nontrivial {x | ↑f x ≠ x}
obtain ⟨a, ha⟩ := hf
no goals
case refine'_1.intro
ι : Type ?u.1652168
α : Type u_1
β : Type ?u.1652174
f g : Perm α
s t : Set α
a✝ b x y a : α
ha : ↑f a ≠ a ∧ ∀ ⦃y : α⦄, ↑f y ≠ y → SameCycle f a y
⊢ Set.Nontrivial {x | ↑f x ≠ x}
exact ⟨f a, f.injective.ne ha.1, a, ha.1, ha.1⟩
case refine'_2.intro.intro.intro
ι : Type ?u.1652168
α : Type u_1
β : Type ?u.1652174
f g : Perm α
s✝ t : Set α
a b x y : α
s : Set α
hs : Set.Nontrivial s
hf : IsCycleOn f s
hsf : ∀ ⦃x : α⦄, ¬IsFixedPt (↑f) x → x ∈ s
⊢ IsCycle f
case refine'_2
ι : Type ?u.1652168
α : Type u_1
β : Type ?u.1652174
f g : Perm α
s t : Set α
a b x y : α
⊢ (∃ s, Set.Nontrivial s ∧ IsCycleOn f s ∧ ∀ ⦃x : α⦄, ¬IsFixedPt (↑f) x → x ∈ s) → IsCycle f
rintro ⟨s, hs, hf, hsf⟩
case refine'_2.intro.intro.intro.intro
ι : Type ?u.1652168
α : Type u_1
β : Type ?u.1652174
f g : Perm α
s✝ t : Set α
a✝ b x y : α
s : Set α
hs : Set.Nontrivial s
hf : IsCycleOn f s
hsf : ∀ ⦃x : α⦄, ¬IsFixedPt (↑f) x → x ∈ s
a : α
ha : a ∈ s
⊢ IsCycle f
case refine'_2.intro.intro.intro
ι : Type ?u.1652168
α : Type u_1
β : Type ?u.1652174
f g : Perm α
s✝ t : Set α
a b x y : α
s : Set α
hs : Set.Nontrivial s
hf : IsCycleOn f s
hsf : ∀ ⦃x : α⦄, ¬IsFixedPt (↑f) x → x ∈ s
⊢ IsCycle f
obtain ⟨a, ha⟩ := hs.nonempty
no goals
case refine'_2.intro.intro.intro.intro
ι : Type ?u.1652168
α : Type u_1
β : Type ?u.1652174
f g : Perm α
s✝ t : Set α
a✝ b x y : α
s : Set α
hs : Set.Nontrivial s
hf : IsCycleOn f s
hsf : ∀ ⦃x : α⦄, ¬IsFixedPt (↑f) x → x ∈ s
a : α
ha : a ∈ s
⊢ IsCycle f
exact ⟨a, hf.apply_ne hs ha, fun b hb => hf.2 ha <| hsf hb⟩