awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g_1 k_1 c_1 g k c : Perm α
hc : ∀ a ∈ c.support, Eq (α := α) ((c : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
a : α
ha : a ∈ (k * c * k⁻¹).support
⊢ Eq (α := α) ((k * c * k⁻¹ : (a : α) → α) a : α) ((k * g * k⁻¹ : (a : α) → α) a : α)
have simp : Eq (α := α) ((c : (a : α) → α) ((k⁻¹ : (a : α) → α) a : α) : α) ((g : (a : α) → α) ((k⁻¹ : (a : α) → α) a : α) : α)
Tactic: simp only [coe_mul, Function.comp_apply, EmbeddingLike.apply_eq_iff_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g_1 k_1 c_1 g k c : Perm α
hc : ∀ a ∈ c.support, Eq (α := α) ((c : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
a : α
ha : a ∈ (k * c * k⁻¹).support
⊢ Eq (α := α) ((c : (a : α) → α) ((k⁻¹ : (a : α) → α) a : α) : α) ((g : (a : α) → α) ((k⁻¹ : (a : α) → α) a : α) : α)
have a₁ : Membership.mem (α := α) c.support ((k⁻¹ : (a : α) → α) a : α)
Tactic: apply hc
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
k g : Perm α
hk : ∀ c ∈ g.cycleFactorsFinset, Commute k c
⊢ Commute k g
have rw : Commute k (g.cycleFactorsFinset.noncommProd id sorry)
Tactic: rw [← cycleFactorsFinset_noncommProd g (cycleFactorsFinset_mem_commute g)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
k g : Perm α
hk : ∀ c ∈ g.cycleFactorsFinset, Commute k c
⊢ Commute k (g.cycleFactorsFinset.noncommProd id ⋯)
have h : ∀ x ∈ g.cycleFactorsFinset, Commute k (id x)
Tactic: apply Finset.noncommProd_commute
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
⊢ Commute c g
have hk : ∀ c_1 ∈ g.cycleFactorsFinset, Commute c c_1
Tactic: apply commute_of_mem_cycleFactorsFinset_commute
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
c' : Perm α
hc' : c' ∈ g.cycleFactorsFinset
⊢ Commute c c'
have pos : ∀ (hcc' : c = c'), Commute c c'
Tactic: by_cases hcc' : c = c'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
c' : Perm α
hc' : c' ∈ g.cycleFactorsFinset
pos : ∀ (hcc' : c = c'), Commute c c'
⊢ Commute c c'
have neg : ∀ (hcc' : ¬c = c'), Commute c c'
Tactic: by_cases hcc' : c = c'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
c' : Perm α
hc' : c' ∈ g.cycleFactorsFinset
hcc' : c = c'
⊢ Commute c c'
have pos : Commute c' c'
Tactic: rw [hcc']
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
c' : Perm α
hc' : c' ∈ g.cycleFactorsFinset
hcc' : ¬c = c'
⊢ Commute c c'
have neg : c ≠ c'
Tactic: apply g.cycleFactorsFinset_mem_commute hc hc'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g d c : Perm α
hc : c ∈ g.cycleFactorsFinset
hd : d ∈ g.cycleFactorsFinset
x : α
⊢ Membership.mem (α := α) c.support ((d : (a : α) → α) x : α) ↔ x ∈ c.support
have simp : Eq (α := α) ((c : (a : α) → α) ((d : (a : α) → α) x : α) : α) ((d : (a : α) → α) x : α) ↔ (c : (a : α) → α) x = x
Tactic: simp only [mem_support, not_iff_not]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g d c : Perm α
hc : c ∈ g.cycleFactorsFinset
hd : d ∈ g.cycleFactorsFinset
x : α
⊢ Eq (α := α) ((c : (a : α) → α) ((d : (a : α) → α) x : α) : α) ((d : (a : α) → α) x : α) ↔ (c : (a : α) → α) x = x
have pos : ∀ (h : c = d),
  Eq (α := α) ((c : (a : α) → α) ((d : (a : α) → α) x : α) : α) ((d : (a : α) → α) x : α) ↔ (c : (a : α) → α) x = x
Tactic: by_cases h : c = d
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g d c : Perm α
hc : c ∈ g.cycleFactorsFinset
hd : d ∈ g.cycleFactorsFinset
x : α
pos :
  ∀ (h : c = d),
    Eq (α := α) ((c : (a : α) → α) ((d : (a : α) → α) x : α) : α) ((d : (a : α) → α) x : α) ↔ (c : (a : α) → α) x = x
⊢ Eq (α := α) ((c : (a : α) → α) ((d : (a : α) → α) x : α) : α) ((d : (a : α) → α) x : α) ↔ (c : (a : α) → α) x = x
have neg : ∀ (h : ¬c = d),
  Eq (α := α) ((c : (a : α) → α) ((d : (a : α) → α) x : α) : α) ((d : (a : α) → α) x : α) ↔ (c : (a : α) → α) x = x
Tactic: by_cases h : c = d
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g d c : Perm α
hc : c ∈ g.cycleFactorsFinset
hd : d ∈ g.cycleFactorsFinset
x : α
h : c = d
⊢ Eq (α := α) ((c : (a : α) → α) ((d : (a : α) → α) x : α) : α) ((d : (a : α) → α) x : α) ↔ (c : (a : α) → α) x = x
have pos : Eq (α := α) ((c : (a : α) → α) ((c : (a : α) → α) x : α) : α) ((c : (a : α) → α) x : α) ↔ (c : (a : α) → α) x = x
Tactic: rw [← h, EmbeddingLike.apply_eq_iff_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g d c : Perm α
hc : c ∈ g.cycleFactorsFinset
hd : d ∈ g.cycleFactorsFinset
x : α
h : c = d
pos : Eq (α := α) ((c : (a : α) → α) ((c : (a : α) → α) x : α) : α) ((c : (a : α) → α) x : α) ↔ (c : (a : α) → α) x = x
⊢ Eq (α := α) ((c : (a : α) → α) ((d : (a : α) → α) x : α) : α) ((d : (a : α) → α) x : α) ↔ (c : (a : α) → α) x = x
have pos₁ : (c : (a : α) → α) x = x ↔ (c : (a : α) → α) x = x
Tactic: rw [← h, EmbeddingLike.apply_eq_iff_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g d c : Perm α
hc : c ∈ g.cycleFactorsFinset
hd : d ∈ g.cycleFactorsFinset
x : α
h : ¬c = d
⊢ Eq (α := α) ((c : (a : α) → α) ((d : (a : α) → α) x : α) : α) ((d : (a : α) → α) x : α) ↔ (c : (a : α) → α) x = x
have neg : Eq (α := α) ((c * d : (a : α) → α) x : α) ((d : (a : α) → α) x : α) ↔ (c : (a : α) → α) x = x
Tactic: rw [← Perm.mul_apply,
      Commute.eq (cycleFactorsFinset_mem_commute g hc hd h),
      mul_apply, EmbeddingLike.apply_eq_iff_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g d c : Perm α
hc : c ∈ g.cycleFactorsFinset
hd : d ∈ g.cycleFactorsFinset
x : α
h : ¬c = d
neg : Eq (α := α) ((c * d : (a : α) → α) x : α) ((d : (a : α) → α) x : α) ↔ (c : (a : α) → α) x = x
⊢ Eq (α := α) ((c : (a : α) → α) ((d : (a : α) → α) x : α) : α) ((d : (a : α) → α) x : α) ↔ (c : (a : α) → α) x = x
have neg₁ : Eq (α := α) ((d * c : (a : α) → α) x : α) ((d : (a : α) → α) x : α) ↔ (c : (a : α) → α) x = x
Tactic: rw [← Perm.mul_apply,
      Commute.eq (cycleFactorsFinset_mem_commute g hc hd h),
      mul_apply, EmbeddingLike.apply_eq_iff_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g d c : Perm α
hc : c ∈ g.cycleFactorsFinset
hd : d ∈ g.cycleFactorsFinset
x : α
h : ¬c = d
neg : Eq (α := α) ((c * d : (a : α) → α) x : α) ((d : (a : α) → α) x : α) ↔ (c : (a : α) → α) x = x
neg₁ : Eq (α := α) ((d * c : (a : α) → α) x : α) ((d : (a : α) → α) x : α) ↔ (c : (a : α) → α) x = x
⊢ Eq (α := α) ((c : (a : α) → α) ((d : (a : α) → α) x : α) : α) ((d : (a : α) → α) x : α) ↔ (c : (a : α) → α) x = x
have neg₂ : Eq (α := α) ((d : (a : α) → α) ((c : (a : α) → α) x : α) : α) ((d : (a : α) → α) x : α) ↔ (c : (a : α) → α) x = x
Tactic: rw [← Perm.mul_apply,
      Commute.eq (cycleFactorsFinset_mem_commute g hc hd h),
      mul_apply, EmbeddingLike.apply_eq_iff_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g d c : Perm α
hc : c ∈ g.cycleFactorsFinset
hd : d ∈ g.cycleFactorsFinset
x : α
h : ¬c = d
neg : Eq (α := α) ((c * d : (a : α) → α) x : α) ((d : (a : α) → α) x : α) ↔ (c : (a : α) → α) x = x
neg₁ : Eq (α := α) ((d * c : (a : α) → α) x : α) ((d : (a : α) → α) x : α) ↔ (c : (a : α) → α) x = x
neg₂ : Eq (α := α) ((d : (a : α) → α) ((c : (a : α) → α) x : α) : α) ((d : (a : α) → α) x : α) ↔ (c : (a : α) → α) x = x
⊢ Eq (α := α) ((c : (a : α) → α) ((d : (a : α) → α) x : α) : α) ((d : (a : α) → α) x : α) ↔ (c : (a : α) → α) x = x
have neg₃ : (c : (a : α) → α) x = x ↔ (c : (a : α) → α) x = x
Tactic: rw [← Perm.mul_apply,
      Commute.eq (cycleFactorsFinset_mem_commute g hc hd h),
      mul_apply, EmbeddingLike.apply_eq_iff_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
β : Type u_3
inst : Finite β
P : Perm β → Prop
σ : Perm β
base_one : P 1
base_cycles : ∀ (σ : Perm β), σ.IsCycle → P σ
induction_disjoint : ∀ (σ τ : Perm β), σ.Disjoint τ → σ.IsCycle → P σ → P τ → P (σ * τ)
⊢ P σ
have intro : ∀ (val : Fintype β), P σ
Tactic: cases nonempty_fintype β
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
β : Type u_3
inst : Finite β
P : Perm β → Prop
σ : Perm β
base_one : P 1
base_cycles : ∀ (σ : Perm β), σ.IsCycle → P σ
induction_disjoint : ∀ (σ τ : Perm β), σ.Disjoint τ → σ.IsCycle → P σ → P τ → P (σ * τ)
val : Fintype β
⊢ P σ
have intro : ∀ (l : List (Perm β)), (∀ τ ∈ l, τ.IsCycle) → List.Pairwise Disjoint l → P l.prod
Tactic: suffices ∀ l : List (Perm β),
      (∀ τ : Perm β, τ ∈ l → τ.IsCycle) → l.Pairwise Disjoint → P l.prod by
    classical
      let x := σ.truncCycleFactors.out
      exact (congr_arg P x.2.1).mp (this x.1 x.2.2.1 x.2.2.2)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
β : Type u_3
inst : Finite β
P : Perm β → Prop
σ_1 : Perm β
base_one : P 1
base_cycles : ∀ (σ : Perm β), σ.IsCycle → P σ
induction_disjoint : ∀ (σ τ : Perm β), σ.Disjoint τ → σ.IsCycle → P σ → P τ → P (σ * τ)
val : Fintype β
σ : Perm β
l : List (Perm β)
ih : (∀ τ ∈ l, τ.IsCycle) → List.Pairwise Disjoint l → P l.prod
h1 : ∀ τ ∈ σ :: l, τ.IsCycle
h2 : List.Pairwise Disjoint (σ :: l)
⊢ P (σ :: l).prod
have intro : P (σ * l.prod)
Tactic: rw [List.prod_cons]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
β : Type u_3
inst : Finite β
P : Perm β → Prop
σ : Perm β
base_one : P 1
base_cycles : ∀ (σ : Perm β), σ.IsCycle → P σ
induction_disjoint : ∀ (σ τ : Perm β), σ.Disjoint τ → σ.IsCycle → P σ → P τ → P (σ * τ)
val : Fintype β
l : List (Perm β)
⊢ (∀ τ ∈ l, τ.IsCycle) → List.Pairwise Disjoint l → P l.prod
have intro : (∀ (τ : Perm β), Membership.mem (γ := List (Perm β)) [] τ → τ.IsCycle) →
  List.Pairwise.{u_3} (α := Perm β) Disjoint [] → P (List.prod [])
Tactic: induction l with
  | nil => exact fun _ _ => base_one
  | cons σ l ih =>
    intro h1 h2
    rw [List.prod_cons]
    exact
      induction_disjoint σ l.prod (disjoint_prod_right _ (List.pairwise_cons.mp h2).1)
        (h1 _ List.mem_cons_self) (base_cycles σ (h1 σ List.mem_cons_self))
        (ih (fun τ hτ => h1 τ (List.mem_cons_of_mem σ hτ)) h2.of_cons)
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
β : Type u_3
inst : Finite β
P : Perm β → Prop
σ : Perm β
base_one : P 1
base_cycles : ∀ (σ : Perm β), σ.IsCycle → P σ
induction_disjoint : ∀ (σ τ : Perm β), σ.Disjoint τ → σ.IsCycle → P σ → P τ → P (σ * τ)
val : Fintype β
l : List (Perm β)
intro :
  (∀ (τ : Perm β), Membership.mem (γ := List (Perm β)) [] τ → τ.IsCycle) →
    List.Pairwise.{u_3} (α := Perm β) Disjoint [] → P (List.prod [])
⊢ (∀ τ ∈ l, τ.IsCycle) → List.Pairwise Disjoint l → P l.prod
have intro₁ : ∀ (σ : Perm β) (l : List (Perm β)) (ih : (∀ τ ∈ l, τ.IsCycle) → List.Pairwise Disjoint l → P l.prod),
  (∀ τ ∈ σ :: l, τ.IsCycle) → List.Pairwise Disjoint (σ :: l) → P (σ :: l).prod
Tactic: induction l with
  | nil => exact fun _ _ => base_one
  | cons σ l ih =>
    intro h1 h2
    rw [List.prod_cons]
    exact
      induction_disjoint σ l.prod (disjoint_prod_right _ (List.pairwise_cons.mp h2).1)
        (h1 _ List.mem_cons_self) (base_cycles σ (h1 σ List.mem_cons_self))
        (ih (fun τ hτ => h1 τ (List.mem_cons_of_mem σ hτ)) h2.of_cons)
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f ∈ g.cycleFactorsFinset
⊢ (g * f⁻¹).cycleFactorsFinset = g.cycleFactorsFinset \ {f}
have revert : ∀ {f : Perm α} (h : f ∈ g.cycleFactorsFinset), (g * f⁻¹).cycleFactorsFinset = g.cycleFactorsFinset \ {f}
Tactic: revert f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
⊢ ∀ {f : Perm α} (h : f ∈ g.cycleFactorsFinset), (g * f⁻¹).cycleFactorsFinset = g.cycleFactorsFinset \ {f}
have refine_1 : ∀ {f : Perm α},
  (fun {g : Perm α} ↦
      ∀ {f : Perm α}, f ∈ g.cycleFactorsFinset → (g * f⁻¹).cycleFactorsFinset = g.cycleFactorsFinset \ {f})
    (g := 1)
Tactic: refine
    cycle_induction_on (P := fun {g : Perm α} ↦
      ∀ {f}, (f ∈ cycleFactorsFinset g)
        → cycleFactorsFinset (g * f⁻¹) = cycleFactorsFinset g \ {f}) _ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
refine_1 :
  ∀ {f : Perm α},
    (fun {g : Perm α} ↦
        ∀ {f : Perm α}, f ∈ g.cycleFactorsFinset → (g * f⁻¹).cycleFactorsFinset = g.cycleFactorsFinset \ {f})
      (g := 1)
⊢ ∀ {f : Perm α} (h : f ∈ g.cycleFactorsFinset), (g * f⁻¹).cycleFactorsFinset = g.cycleFactorsFinset \ {f}
have refine_2 : ∀ {f : Perm α} (σ : Perm α),
  σ.IsCycle →
    (fun {g : Perm α} ↦
        ∀ {f : Perm α}, f ∈ g.cycleFactorsFinset → (g * f⁻¹).cycleFactorsFinset = g.cycleFactorsFinset \ {f})
      (g := σ)
Tactic: refine
    cycle_induction_on (P := fun {g : Perm α} ↦
      ∀ {f}, (f ∈ cycleFactorsFinset g)
        → cycleFactorsFinset (g * f⁻¹) = cycleFactorsFinset g \ {f}) _ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
refine_1 :
  ∀ {f : Perm α},
    (fun {g : Perm α} ↦
        ∀ {f : Perm α}, f ∈ g.cycleFactorsFinset → (g * f⁻¹).cycleFactorsFinset = g.cycleFactorsFinset \ {f})
      (g := 1)
refine_2 :
  ∀ {f : Perm α} (σ : Perm α),
    σ.IsCycle →
      (fun {g : Perm α} ↦
          ∀ {f : Perm α}, f ∈ g.cycleFactorsFinset → (g * f⁻¹).cycleFactorsFinset = g.cycleFactorsFinset \ {f})
        (g := σ)
⊢ ∀ {f : Perm α} (h : f ∈ g.cycleFactorsFinset), (g * f⁻¹).cycleFactorsFinset = g.cycleFactorsFinset \ {f}
have refine_3 : ∀ {f : Perm α} (σ τ : Perm α),
  σ.Disjoint τ →
    σ.IsCycle →
      (fun {g : Perm α} ↦
            ∀ {f : Perm α}, f ∈ g.cycleFactorsFinset → (g * f⁻¹).cycleFactorsFinset = g.cycleFactorsFinset \ {f})
          (g := σ) →
        (fun {g : Perm α} ↦
              ∀ {f : Perm α}, f ∈ g.cycleFactorsFinset → (g * f⁻¹).cycleFactorsFinset = g.cycleFactorsFinset \ {f})
            (g := τ) →
          (fun {g : Perm α} ↦
              ∀ {f : Perm α}, f ∈ g.cycleFactorsFinset → (g * f⁻¹).cycleFactorsFinset = g.cycleFactorsFinset \ {f})
            (g := σ * τ)
Tactic: refine
    cycle_induction_on (P := fun {g : Perm α} ↦
      ∀ {f}, (f ∈ cycleFactorsFinset g)
        → cycleFactorsFinset (g * f⁻¹) = cycleFactorsFinset g \ {f}) _ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ : Perm α
hσ : σ.IsCycle
f : Perm α
hf : f ∈ σ.cycleFactorsFinset
⊢ (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
have refine_2 : ∀ (hf : f = σ), (σ * f⁻¹).cycleFactorsFinset = {σ} \ {f}
Tactic: simp only [cycleFactorsFinset_eq_singleton_self_iff.mpr hσ, mem_singleton] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
⊢ f ∈ (σ * τ).cycleFactorsFinset → (σ * τ * f⁻¹).cycleFactorsFinset = (σ * τ).cycleFactorsFinset \ {f}
have refine_3 : f ∈ σ.cycleFactorsFinset ∨ f ∈ τ.cycleFactorsFinset →
  (σ * τ * f⁻¹).cycleFactorsFinset = (σ.cycleFactorsFinset ∪ τ.cycleFactorsFinset) \ {f}
Tactic: simp_rw [hd.cycleFactorsFinset_mul_eq_union, mem_union]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f ∈ σ.cycleFactorsFinset
⊢ (σ * τ * f⁻¹).cycleFactorsFinset = (σ.cycleFactorsFinset ∪ τ.cycleFactorsFinset) \ {f}
have refine_3 : τ.Disjoint (σ * f⁻¹)
Tactic: rw [hd.commute.eq, union_comm, union_sdiff_distrib, sdiff_singleton_eq_erase,
        erase_eq_of_notMem, mul_assoc, Disjoint.cycleFactorsFinset_mul_eq_union, hσ hf]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f ∈ σ.cycleFactorsFinset
refine_3 : τ.Disjoint (σ * f⁻¹)
⊢ (σ * τ * f⁻¹).cycleFactorsFinset = (σ.cycleFactorsFinset ∪ τ.cycleFactorsFinset) \ {f}
have refine_3₁ : f ∉ τ.cycleFactorsFinset
Tactic: rw [hd.commute.eq, union_comm, union_sdiff_distrib, sdiff_singleton_eq_erase,
        erase_eq_of_notMem, mul_assoc, Disjoint.cycleFactorsFinset_mul_eq_union, hσ hf]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (hypothesis)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f ∈ σ.cycleFactorsFinset
⊢ τ.Disjoint (σ * f⁻¹)
have hf₁ : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((σ : (a : α) → α) a : α)
Tactic: rw [mem_cycleFactorsFinset_iff] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((σ : (a : α) → α) a : α)
x : α
⊢ (τ : (a : α) → α) x = x ∨ (σ * f⁻¹ : (a : α) → α) x = x
have refine_3 : ∀ (hx : (τ : (a : α) → α) x = x), (τ : (a : α) → α) x = x ∨ (σ * f⁻¹ : (a : α) → α) x = x
Tactic: rcases hd.symm x with hx | hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((σ : (a : α) → α) a : α)
x : α
refine_3 : ∀ (hx : (τ : (a : α) → α) x = x), (τ : (a : α) → α) x = x ∨ (σ * f⁻¹ : (a : α) → α) x = x
⊢ (τ : (a : α) → α) x = x ∨ (σ * f⁻¹ : (a : α) → α) x = x
have refine_3₁ : ∀ (hx : (σ : (a : α) → α) x = x), (τ : (a : α) → α) x = x ∨ (σ * f⁻¹ : (a : α) → α) x = x
Tactic: rcases hd.symm x with hx | hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((σ : (a : α) → α) a : α)
x : α
hx : (σ : (a : α) → α) x = x
⊢ (τ : (a : α) → α) x = x ∨ (σ * f⁻¹ : (a : α) → α) x = x
have refine_3 : (σ * f⁻¹ : (a : α) → α) x = x
Tactic: refine Or.inr ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((σ : (a : α) → α) a : α)
x : α
hx : (σ : (a : α) → α) x = x
⊢ (σ * f⁻¹ : (a : α) → α) x = x
have pos : ∀ (hfx : (f : (a : α) → α) x = x), (σ * f⁻¹ : (a : α) → α) x = x
Tactic: by_cases hfx : f x = x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((σ : (a : α) → α) a : α)
x : α
hx : (σ : (a : α) → α) x = x
pos : ∀ (hfx : (f : (a : α) → α) x = x), (σ * f⁻¹ : (a : α) → α) x = x
⊢ (σ * f⁻¹ : (a : α) → α) x = x
have neg : ∀ (hfx : ¬(f : (a : α) → α) x = x), (σ * f⁻¹ : (a : α) → α) x = x
Tactic: by_cases hfx : f x = x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((σ : (a : α) → α) a : α)
x : α
hx : (σ : (a : α) → α) x = x
hfx : (f : (a : α) → α) x = x
⊢ (σ * f⁻¹ : (a : α) → α) x = x
have pos : Eq (α := α) ((σ * f⁻¹ : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α)
Tactic: rw [← hfx]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Factors (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
g f_1 σ τ : Perm α
hd : σ.Disjoint τ
h : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, Eq (α := α) ((f : (a : α) → α) a : α) ((σ : (a : α) → α) a : α)
x : α
hx : (σ : (a : α) → α) x = x
hfx : ¬(f : (a : α) → α) x = x
⊢ (σ * f⁻¹ : (a : α) → α) x = x
have neg : (σ : (a : α) → α) ((f⁻¹ : (a : α) → α) x : α) = x
Tactic: rw [mul_apply]