awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
m : List (Perm α)
hm₁ : m.prod = (g.cycleOf x)⁻¹ * g
hm₂ : ∀ g' ∈ m, g'.IsCycle
hm₃ : List.Pairwise Disjoint m
refine_1 : (g.cycleOf x :: m).prod = g
refine_2 : ∀ (g' : Perm α) (hg' : g' ∈ g.cycleOf x :: m), g'.IsCycle
⊢ (g.cycleOf x :: m).prod = g ∧
    (∀ g' ∈ g.cycleOf x :: m, g'.IsCycle) ∧ (∀ a' ∈ m, (g.cycleOf x).Disjoint a') ∧ List.Pairwise Disjoint m
have refine_3 : ∀ (g' : Perm α) (hg' : g' ∈ m) (y : α), (g.cycleOf x : (a : α) → α) y = y ∨ (g' : (a : α) → α) y = y
Tactic: refine ⟨?_, fun g' hg' ↦ ?_, fun g' hg' y ↦ ?_, hm₃⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
m : List (Perm α)
hm₁ : m.prod = (g.cycleOf x)⁻¹ * g
hm₂ : ∀ g' ∈ m, g'.IsCycle
hm₃ : List.Pairwise Disjoint m
g' : Perm α
hg' : g' ∈ m
y : α
⊢ (g.cycleOf x : (a : α) → α) y = y ∨ (g' : (a : α) → α) y = y
have refine_3 : ∀ (hgy : (g.cycleOf x : (a : α) → α) y ≠ y) (hg'y : (g' : (a : α) → α) y ≠ y), False
Tactic: by_contra! ⟨hgy, hg'y⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
m : List (Perm α)
hm₁ : m.prod = (g.cycleOf x)⁻¹ * g
hm₂ : ∀ g' ∈ m, g'.IsCycle
hm₃ : List.Pairwise Disjoint m
g' : Perm α
hg' : g' ∈ m
y : α
hgy : (g.cycleOf x : (a : α) → α) y ≠ y
hg'y : (g' : (a : α) → α) y ≠ y
⊢ False
have hxy : g.SameCycle x y
Tactic: have hxy : SameCycle g x y := not_imp_comm.1 cycleOf_apply_of_not_sameCycle hgy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
m : List (Perm α)
hm₁ : m.prod = (g.cycleOf x)⁻¹ * g
hm₂ : ∀ g' ∈ m, g'.IsCycle
hm₃ : List.Pairwise Disjoint m
g' : Perm α
hg' : g' ∈ m
y : α
hgy : (g.cycleOf x : (a : α) → α) y ≠ y
hg'y : (g' : (a : α) → α) y ≠ y
hxy : g.SameCycle x y
⊢ False
have hg'm : g' :: m.erase g' ~ m
Tactic: have hg'm : g' :: m.erase g' ~ m := List.cons_perm_iff_perm_erase.2 ⟨hg', .refl _⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
m : List (Perm α)
hm₁ : m.prod = (g.cycleOf x)⁻¹ * g
hm₂ : ∀ g' ∈ m, g'.IsCycle
hm₃ : List.Pairwise Disjoint m
g' : Perm α
hg' : g' ∈ m
y : α
hgy : (g.cycleOf x : (a : α) → α) y ≠ y
hg'y : (g' : (a : α) → α) y ≠ y
hxy : g.SameCycle x y
hg'm : g' :: m.erase g' ~ m
⊢ False
have this : ∀ h ∈ m.erase g', g'.Disjoint h
Tactic: have : ∀ h ∈ m.erase g', Disjoint g' h :=
          (List.pairwise_cons.1 ((hg'm.pairwise_iff Disjoint.symm).2 hm₃)).1
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
m : List (Perm α)
hm₁ : m.prod = (g.cycleOf x)⁻¹ * g
hm₂ : ∀ g' ∈ m, g'.IsCycle
hm₃ : List.Pairwise Disjoint m
g' : Perm α
hg' : g' ∈ m
y : α
hgy : (g.cycleOf x : (a : α) → α) y ≠ y
hg'y : (g' : (a : α) → α) y ≠ y
hxy : g.SameCycle x y
hg'm : g' :: m.erase g' ~ m
this : ∀ h ∈ m.erase g', g'.Disjoint h
⊢ False
have refine_3 : ¬((m.erase g').prod : (a : α) → α) y = y
Tactic: refine hg'y <| (disjoint_prod_right _ this y).resolve_right ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
m : List (Perm α)
hm₁ : m.prod = (g.cycleOf x)⁻¹ * g
hm₂ : ∀ g' ∈ m, g'.IsCycle
hm₃ : List.Pairwise Disjoint m
g' : Perm α
hg' : g' ∈ m
y : α
hgy : (g.cycleOf x : (a : α) → α) y ≠ y
hg'y : (g' : (a : α) → α) y ≠ y
hxy : g.SameCycle x y
hg'm : g' :: m.erase g' ~ m
this : ∀ h ∈ m.erase g', g'.Disjoint h
⊢ g⁻¹.SameCycle x ((g : (a : α) → α) y)
have rwa : g.SameCycle x ((g : (a : α) → α) y)
Tactic: rwa [sameCycle_inv, sameCycle_apply_right]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
m : List (Perm α)
hm₁ : m.prod = (g.cycleOf x)⁻¹ * g
hm₂ : ∀ g' ∈ m, g'.IsCycle
hm₃ : List.Pairwise Disjoint m
g' : Perm α
hg' : g' ∈ m
y : α
hgy : (g.cycleOf x : (a : α) → α) y ≠ y
hg'y : (g' : (a : α) → α) y ≠ y
hxy : g.SameCycle x y
hg'm : g' :: m.erase g' ~ m
this : ∀ h ∈ m.erase g', g'.Disjoint h
⊢ ¬((m.erase g').prod : (a : α) → α) y = y
have hsc : g⁻¹.SameCycle x ((g : (a : α) → α) y)
Tactic: have hsc : SameCycle g⁻¹ x (g y) := by rwa [sameCycle_inv, sameCycle_apply_right]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : Fintype α
l_1 : List α
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l_1
l_2 : List α
g : Perm α
hfg : ∀ {x : α}, (g : (a : α) → α) x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, (g : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬(g : (a : α) → α) x = x
m : List (Perm α)
hm₁ : m.prod = (g.cycleOf x)⁻¹ * g
hm₂ : ∀ g' ∈ m, g'.IsCycle
hm₃ : List.Pairwise Disjoint m
g' : Perm α
hg' : g' ∈ m
y : α
hgy : (g.cycleOf x : (a : α) → α) y ≠ y
hg'y : (g' : (a : α) → α) y ≠ y
hxy : g.SameCycle x y
hg'm : g' :: m.erase g' ~ m
this : ∀ h ∈ m.erase g', g'.Disjoint h
hsc : g⁻¹.SameCycle x ((g : (a : α) → α) y)
⊢ ¬((m.erase g').prod : (a : α) → α) y = y
have refine_3 : ∀ (hm₁ : (m.erase g').prod = g'⁻¹ * ((g.cycleOf x)⁻¹ * g)) (hg' : g' ∈ m) (y : α)
  (hgy : (g.cycleOf x : (a : α) → α) y ≠ y) (hg'y : (g' : (a : α) → α) y ≠ y) (hxy : g.SameCycle x y)
  (hg'm : g' :: m.erase g' ~ m) (this : ∀ h ∈ m.erase g', g'.Disjoint h) (hsc : g⁻¹.SameCycle x ((g : (a : α) → α) y)),
  ¬((m.erase g').prod : (a : α) → α) y = y
Tactic: rw [disjoint_prod_perm hm₃ hg'm.symm, List.prod_cons, ← eq_inv_mul_iff_mul_eq] at hm₁
Cleared hypotheses: hm₁, hg', y, hgy, hg'y, hxy, hg'm, this, hsc
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_4
inst : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
⊢ σ ∈ l ↔
    σ.IsCycle ∧
      ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)
have suffices : σ.IsCycle →
  (σ ∈ l ↔ ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α))
Tactic: suffices σ.IsCycle → (σ ∈ l ↔ ∀ a, σ a ≠ a → σ a = l.prod a) by
    exact ⟨fun hσ => ⟨h1 σ hσ, (this (h1 σ hσ)).mp hσ⟩, fun hσ => (this hσ.1).mpr hσ.2⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_4
inst : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
⊢ σ ∈ l ↔ ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)
have intro : ∀ (val : Fintype α),
  σ ∈ l ↔ ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)
Tactic: cases nonempty_fintype α
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_4
inst : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val : Fintype α
⊢ σ ∈ l ↔ ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)
have intro : σ ∈ l → ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_4
inst : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val : Fintype α
intro :
  σ ∈ l → ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)
⊢ σ ∈ l ↔ ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)
have intro₁ : (∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)) → σ ∈ l
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (hypothesis)
Goal:
α : Type u_4
inst : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val : Fintype α
h : ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)
x : α
hx : x ∈ σ.support
⊢ x ∈ l.prod.support
have hx₁ : (σ : (a : α) → α) x ≠ x
Tactic: rw [mem_support] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_4
inst : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val : Fintype α
h : ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)
x : α
hx : (σ : (a : α) → α) x ≠ x
⊢ x ∈ l.prod.support
have rwa : (l.prod : (a : α) → α) x ≠ x
Tactic: rwa [mem_support, ← h _ hx]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (hypothesis)
Goal:
α : Type u_4
inst : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val : Fintype α
h : ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)
⊢ σ ∈ l
have hσl : σ.support ⊆ l.prod.support
Tactic: have hσl : σ.support ⊆ l.prod.support := by
        intro x hx
        rw [mem_support] at hx
        rwa [mem_support, ← h _ hx]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_4
inst : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val : Fintype α
h : ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)
hσl : σ.support ⊆ l.prod.support
⊢ σ ∈ l
have intro : ∀ (a : α) (ha : (σ : (a : α) → α) a ≠ a), σ ∈ l
Tactic: obtain ⟨a, ha, -⟩ := id h3
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (hypothesis)
Goal:
α : Type u_4
inst : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val : Fintype α
h : ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)
hσl : σ.support ⊆ l.prod.support
a : α
ha : (σ : (a : α) → α) a ≠ a
⊢ σ ∈ l
have ha₁ : a ∈ σ.support
Tactic: rw [← mem_support] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_4
inst : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val : Fintype α
h : ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)
hσl : σ.support ⊆ l.prod.support
a : α
ha : a ∈ σ.support
⊢ σ ∈ l
have intro : ∀ (τ : Perm α) (hτ : τ ∈ l) (hτa : a ∈ τ.support), σ ∈ l
Tactic: obtain ⟨τ, hτ, hτa⟩ := exists_mem_support_of_mem_support_prod (hσl ha)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (hypothesis)
Goal:
α : Type u_4
inst : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val : Fintype α
h : ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)
hσl : σ.support ⊆ l.prod.support
a : α
ha : a ∈ σ.support
τ : Perm α
hτ : τ ∈ l
hτa : a ∈ τ.support
⊢ σ ∈ l
have hτl : ∀ x ∈ τ.support, Eq (α := α) ((τ : (a : α) → α) x : α) ((l.prod : (a : α) → α) x : α)
Tactic: have hτl : ∀ x ∈ τ.support, τ x = l.prod x := eq_on_support_mem_disjoint hτ h2
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_4
inst : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val : Fintype α
h : ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)
hσl : σ.support ⊆ l.prod.support
a : α
ha : a ∈ σ.support
τ : Perm α
hτ : τ ∈ l
hτa : a ∈ τ.support
hτl : ∀ x ∈ τ.support, Eq (α := α) ((τ : (a : α) → α) x : α) ((l.prod : (a : α) → α) x : α)
x : α
hx : x ∈ σ.support ∩ τ.support
⊢ Eq (α := α) ((σ : (a : α) → α) x : α) ((τ : (a : α) → α) x : α)
have rw : Eq (α := α) ((l.prod : (a : α) → α) x : α) ((τ : (a : α) → α) x : α)
Tactic: rw [h x (mem_support.mp (mem_of_mem_inter_left hx)), hτl x (mem_of_mem_inter_right hx)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_4
inst : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val : Fintype α
h : ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)
hσl : σ.support ⊆ l.prod.support
a : α
ha : a ∈ σ.support
τ : Perm α
hτ : τ ∈ l
hτa : a ∈ τ.support
hτl : ∀ x ∈ τ.support, Eq (α := α) ((τ : (a : α) → α) x : α) ((l.prod : (a : α) → α) x : α)
x : α
hx : x ∈ σ.support ∩ τ.support
rw : Eq (α := α) ((l.prod : (a : α) → α) x : α) ((τ : (a : α) → α) x : α)
⊢ Eq (α := α) ((σ : (a : α) → α) x : α) ((τ : (a : α) → α) x : α)
have rw₁ : Eq (α := α) ((l.prod : (a : α) → α) x : α) ((l.prod : (a : α) → α) x : α)
Tactic: rw [h x (mem_support.mp (mem_of_mem_inter_left hx)), hτl x (mem_of_mem_inter_right hx)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (hypothesis)
Goal:
α : Type u_4
inst : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val : Fintype α
h : ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)
hσl : σ.support ⊆ l.prod.support
a : α
ha : a ∈ σ.support
τ : Perm α
hτ : τ ∈ l
hτa : a ∈ τ.support
hτl : ∀ x ∈ τ.support, Eq (α := α) ((τ : (a : α) → α) x : α) ((l.prod : (a : α) → α) x : α)
⊢ σ ∈ l
have key : ∀ x ∈ σ.support ∩ τ.support, Eq (α := α) ((σ : (a : α) → α) x : α) ((τ : (a : α) → α) x : α)
Tactic: have key : ∀ x ∈ σ.support ∩ τ.support, σ x = τ x := by
        intro x hx
        rw [h x (mem_support.mp (mem_of_mem_inter_left hx)), hτl x (mem_of_mem_inter_right hx)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_4
inst : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val : Fintype α
h : ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)
hσl : σ.support ⊆ l.prod.support
a : α
ha : a ∈ σ.support
τ : Perm α
hτ : τ ∈ l
hτa : a ∈ τ.support
hτl : ∀ x ∈ τ.support, Eq (α := α) ((τ : (a : α) → α) x : α) ((l.prod : (a : α) → α) x : α)
key : ∀ x ∈ σ.support ∩ τ.support, Eq (α := α) ((σ : (a : α) → α) x : α) ((τ : (a : α) → α) x : α)
⊢ σ ∈ l
have h₁ : σ = τ
Tactic: convert! hτ
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_4
inst : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val : Fintype α
h : ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)
hσl : σ.support ⊆ l.prod.support
a : α
ha : a ∈ σ.support
τ : Perm α
hτ : τ ∈ l
hτa : a ∈ τ.support
hτl : ∀ x ∈ τ.support, Eq (α := α) ((τ : (a : α) → α) x : α) ((l.prod : (a : α) → α) x : α)
key : ∀ x ∈ σ.support ∩ τ.support, Eq (α := α) ((σ : (a : α) → α) x : α) ((τ : (a : α) → α) x : α)
⊢ σ = τ
have h₁ : Eq (α := α) ((σ : (a : α) → α) a : α) ((τ : (a : α) → α) a : α)
Tactic: refine h3.eq_on_support_inter_nonempty_congr (h1 _ hτ) key ?_ ha
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_4
inst : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
⊢ σ ∈ l ↔ ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)
have intro : ∀ (val : Fintype α),
  σ ∈ l ↔ ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)
Tactic: classical
    cases nonempty_fintype α
    constructor
    · intro h a ha
      exact eq_on_support_mem_disjoint h h2 _ (mem_support.mpr ha)
    · intro h
      have hσl : σ.support ⊆ l.prod.support := by
        intro x hx
        rw [mem_support] at hx
        rwa [mem_support, ← h _ hx]
      obtain ⟨a, ha, -⟩ := id h3
      rw [← mem_support] at ha
      obtain ⟨τ, hτ, hτa⟩ := exists_mem_support_of_mem_support_prod (hσl ha)
      have hτl : ∀ x ∈ τ.support, τ x = l.prod x := eq_on_support_mem_disjoint hτ h2
      have key : ∀ x ∈ σ.support ∩ τ.support, σ x = τ x := by
        intro x hx
        rw [h x (mem_support.mp (mem_of_mem_inter_left hx)), hτl x (mem_of_mem_inter_right hx)]
      convert! hτ
      refine h3.eq_on_support_inter_nonempty_congr (h1 _ hτ) key ?_ ha
      exact key a (mem_inter_of_mem ha hτa)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_4
inst : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
intro :
  ∀ (val : Fintype α),
    σ ∈ l ↔ ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)
⊢ σ ∈ l ↔ ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)
have intro₁ : ∀ (val : Fintype α),
  σ ∈ l → ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)
Tactic: classical
    cases nonempty_fintype α
    constructor
    · intro h a ha
      exact eq_on_support_mem_disjoint h h2 _ (mem_support.mpr ha)
    · intro h
      have hσl : σ.support ⊆ l.prod.support := by
        intro x hx
        rw [mem_support] at hx
        rwa [mem_support, ← h _ hx]
      obtain ⟨a, ha, -⟩ := id h3
      rw [← mem_support] at ha
      obtain ⟨τ, hτ, hτa⟩ := exists_mem_support_of_mem_support_prod (hσl ha)
      have hτl : ∀ x ∈ τ.support, τ x = l.prod x := eq_on_support_mem_disjoint hτ h2
      have key : ∀ x ∈ σ.support ∩ τ.support, σ x = τ x := by
        intro x hx
        rw [h x (mem_support.mp (mem_of_mem_inter_left hx)), hτl x (mem_of_mem_inter_right hx)]
      convert! hτ
      refine h3.eq_on_support_inter_nonempty_congr (h1 _ hτ) key ?_ ha
      exact key a (mem_inter_of_mem ha hτa)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_4
inst : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
intro :
  ∀ (val : Fintype α),
    σ ∈ l ↔ ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)
intro₁ :
  ∀ (val : Fintype α),
    σ ∈ l → ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)
⊢ σ ∈ l ↔ ∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)
have intro₂ : ∀ (val : Fintype α),
  (∀ (a : α), (σ : (a : α) → α) a ≠ a → Eq (α := α) ((σ : (a : α) → α) a : α) ((l.prod : (a : α) → α) a : α)) → σ ∈ l
Tactic: classical
    cases nonempty_fintype α
    constructor
    · intro h a ha
      exact eq_on_support_mem_disjoint h h2 _ (mem_support.mpr ha)
    · intro h
      have hσl : σ.support ⊆ l.prod.support := by
        intro x hx
        rw [mem_support] at hx
        rwa [mem_support, ← h _ hx]
      obtain ⟨a, ha, -⟩ := id h3
      rw [← mem_support] at ha
      obtain ⟨τ, hτ, hτa⟩ := exists_mem_support_of_mem_support_prod (hσl ha)
      have hτl : ∀ x ∈ τ.support, τ x = l.prod x := eq_on_support_mem_disjoint hτ h2
      have key : ∀ x ∈ σ.support ∩ τ.support, σ x = τ x := by
        intro x hx
        rw [h x (mem_support.mp (mem_of_mem_inter_left hx)), hτl x (mem_of_mem_inter_right hx)]
      convert! hτ
      refine h3.eq_on_support_inter_nonempty_congr (h1 _ hτ) key ?_ ha
      exact key a (mem_inter_of_mem ha hτa)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_4
inst : Finite α
l₁ l₂ : List (Perm α)
h₀ : l₁.prod = l₂.prod
h₁l₁ : ∀ σ ∈ l₁, σ.IsCycle
h₁l₂ : ∀ σ ∈ l₂, σ.IsCycle
h₂l₁ : List.Pairwise Disjoint l₁
h₂l₂ : List.Pairwise Disjoint l₂
⊢ l₁ ~ l₂
have h₁l₃ : ∀ (σ : Perm α), σ ∈ l₁ ↔ σ ∈ l₂
Tactic: refine
      (List.perm_ext_iff_of_nodup (nodup_of_pairwise_disjoint_cycles h₁l₁ h₂l₁)
            (nodup_of_pairwise_disjoint_cycles h₁l₂ h₂l₂)).mpr
        fun σ => ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_4
inst : Finite α
l₁ l₂ : List (Perm α)
h₀ : l₁.prod = l₂.prod
h₁l₁ : ∀ σ ∈ l₁, σ.IsCycle
h₁l₂ : ∀ σ ∈ l₂, σ.IsCycle
h₂l₁ : List.Pairwise Disjoint l₁
h₂l₂ : List.Pairwise Disjoint l₂
σ : Perm α
⊢ σ ∈ l₁ ↔ σ ∈ l₂
have pos : ∀ (hσ : σ.IsCycle), σ ∈ l₁ ↔ σ ∈ l₂
Tactic: by_cases hσ : σ.IsCycle
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_4
inst : Finite α
l₁ l₂ : List (Perm α)
h₀ : l₁.prod = l₂.prod
h₁l₁ : ∀ σ ∈ l₁, σ.IsCycle
h₁l₂ : ∀ σ ∈ l₂, σ.IsCycle
h₂l₁ : List.Pairwise Disjoint l₁
h₂l₂ : List.Pairwise Disjoint l₂
σ : Perm α
pos : ∀ (hσ : σ.IsCycle), σ ∈ l₁ ↔ σ ∈ l₂
⊢ σ ∈ l₁ ↔ σ ∈ l₂
have neg : ∀ (hσ : ¬σ.IsCycle), σ ∈ l₁ ↔ σ ∈ l₂
Tactic: by_cases hσ : σ.IsCycle
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (hypothesis)
Goal:
α : Type u_4
inst : Finite α
l₁ l₂ : List (Perm α)
h₀ : l₁.prod = l₂.prod
h₁l₁ : ∀ σ ∈ l₁, σ.IsCycle
h₁l₂ : ∀ σ ∈ l₂, σ.IsCycle
h₂l₁ : List.Pairwise Disjoint l₁
h₂l₂ : List.Pairwise Disjoint l₂
σ : Perm α
hσ : σ.IsCycle
⊢ σ ∈ l₁ ↔ σ ∈ l₂
have x : ∃ (x : α), ¬Eq (α := α) ((σ : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)
Tactic: obtain _ := not_forall.mp (mt ext hσ.ne_one)