awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.FixedPointFree (goal)
Goal:
F : Type u_1
G : Type u_2
inst : Group G
inst_1 : FunLike F G G
inst_2 : MonoidHomClass F G G
φ : F
inst_3 : Finite G
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
h2 : Eq.{u_2 + 1} (α := G → G) (⇑φ : (a : G) → G)^[2] _root_.id
g : G
key : HMul.hMul (β := G) g ((φ : (a : G) → G) g : G) = 1
h : ∀ (key : g⁻¹ = (φ : (a : G) → G) g), (φ : (a : G) → G) g = g⁻¹
⊢ (φ : (a : G) → G) g = g⁻¹
have h₁ : ∀ (key : (φ : (a : G) → G) g = g⁻¹), (φ : (a : G) → G) g = g⁻¹
Tactic: rwa [← inv_eq_iff_mul_eq_one, eq_comm] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.GroupTheory.FixedPointFree (hypothesis)
Goal:
F : Type u_1
G : Type u_2
inst : Group G
inst_1 : FunLike F G G
inst_2 : MonoidHomClass F G G
φ : F
inst_3 : Finite G
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
h2 : Function.Involutive.{u_2 + 1} (α := G) (⇑φ : (a : G) → G)
g h : G
⊢ Commute g h
have key : (φ : (a : G) → G) (g * h) = HMul.hMul (α := G) (β := G) ((φ : (a : G) → G) g : G) ((φ : (a : G) → G) h : G)
Tactic: have key := map_mul φ g h
-- Lean 4 proof step from Mathlib.GroupTheory.FixedPointFree (goal)
Goal:
F : Type u_1
G : Type u_2
inst : Group G
inst_1 : FunLike F G G
inst_2 : MonoidHomClass F G G
φ : F
inst_3 : Finite G
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
h2 : Function.Involutive.{u_2 + 1} (α := G) (⇑φ : (a : G) → G)
g h : G
key : (φ : (a : G) → G) (g * h) = HMul.hMul (α := G) (β := G) ((φ : (a : G) → G) g : G) ((φ : (a : G) → G) h : G)
⊢ Commute g h
have rwa : ∀ (key : (fun (x : G) ↦ x⁻¹) (g * h) = HMul.hMul (α := G) ((fun (x : G) ↦ x⁻¹) g) ((fun (x : G) ↦ x⁻¹) h)), Commute g h
Tactic: rwa [hφ.coe_eq_inv_of_involutive h2, inv_eq_iff_eq_inv, mul_inv_rev, inv_inv, inv_inv] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.GroupTheory.FixedPointFree (goal)
Goal:
F : Type u_1
G : Type u_2
inst : Group G
inst_1 : FunLike F G G
inst_2 : MonoidHomClass F G G
φ : F
inst_3 : Finite G
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
h2 : Function.Involutive.{u_2 + 1} (α := G) (⇑φ : (a : G) → G)
g h : G
key : (φ : (a : G) → G) (g * h) = HMul.hMul (α := G) (β := G) ((φ : (a : G) → G) g : G) ((φ : (a : G) → G) h : G)
rwa :
  ∀ (key : (fun (x : G) ↦ x⁻¹) (g * h) = HMul.hMul (α := G) ((fun (x : G) ↦ x⁻¹) g) ((fun (x : G) ↦ x⁻¹) h)),
    Commute g h
⊢ Commute g h
have rwa₁ : ∀ (key : g * h = (HMul.hMul (α := G) ((fun (x : G) ↦ x⁻¹) g) ((fun (x : G) ↦ x⁻¹) h))⁻¹), Commute g h
Tactic: rwa [hφ.coe_eq_inv_of_involutive h2, inv_eq_iff_eq_inv, mul_inv_rev, inv_inv, inv_inv] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.GroupTheory.FixedPointFree (goal)
Goal:
F : Type u_1
G : Type u_2
inst : Group G
inst_1 : FunLike F G G
inst_2 : MonoidHomClass F G G
φ : F
inst_3 : Finite G
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
h2 : Function.Involutive.{u_2 + 1} (α := G) (⇑φ : (a : G) → G)
g h : G
key : (φ : (a : G) → G) (g * h) = HMul.hMul (α := G) (β := G) ((φ : (a : G) → G) g : G) ((φ : (a : G) → G) h : G)
rwa :
  ∀ (key : (fun (x : G) ↦ x⁻¹) (g * h) = HMul.hMul (α := G) ((fun (x : G) ↦ x⁻¹) g) ((fun (x : G) ↦ x⁻¹) h)),
    Commute g h
rwa₁ : ∀ (key : g * h = (HMul.hMul (α := G) ((fun (x : G) ↦ x⁻¹) g) ((fun (x : G) ↦ x⁻¹) h))⁻¹), Commute g h
⊢ Commute g h
have rwa₂ : ∀ (key : g * h = HMul.hMul (α := G) ((fun (x : G) ↦ x⁻¹) h)⁻¹ ((fun (x : G) ↦ x⁻¹) g)⁻¹), Commute g h
Tactic: rwa [hφ.coe_eq_inv_of_involutive h2, inv_eq_iff_eq_inv, mul_inv_rev, inv_inv, inv_inv] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.GroupTheory.FixedPointFree (goal)
Goal:
F : Type u_1
G : Type u_2
inst : Group G
inst_1 : FunLike F G G
inst_2 : MonoidHomClass F G G
φ : F
inst_3 : Finite G
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
h2 : Function.Involutive.{u_2 + 1} (α := G) (⇑φ : (a : G) → G)
g h : G
key : (φ : (a : G) → G) (g * h) = HMul.hMul (α := G) (β := G) ((φ : (a : G) → G) g : G) ((φ : (a : G) → G) h : G)
rwa :
  ∀ (key : (fun (x : G) ↦ x⁻¹) (g * h) = HMul.hMul (α := G) ((fun (x : G) ↦ x⁻¹) g) ((fun (x : G) ↦ x⁻¹) h)),
    Commute g h
rwa₁ : ∀ (key : g * h = (HMul.hMul (α := G) ((fun (x : G) ↦ x⁻¹) g) ((fun (x : G) ↦ x⁻¹) h))⁻¹), Commute g h
rwa₂ : ∀ (key : g * h = HMul.hMul (α := G) ((fun (x : G) ↦ x⁻¹) h)⁻¹ ((fun (x : G) ↦ x⁻¹) g)⁻¹), Commute g h
⊢ Commute g h
have rwa₃ : ∀ (key : g * h = h * ((fun (x : G) ↦ x⁻¹) g)⁻¹), Commute g h
Tactic: rwa [hφ.coe_eq_inv_of_involutive h2, inv_eq_iff_eq_inv, mul_inv_rev, inv_inv, inv_inv] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.GroupTheory.FixedPointFree (goal)
Goal:
F : Type u_1
G : Type u_2
inst : Group G
inst_1 : FunLike F G G
inst_2 : MonoidHomClass F G G
φ : F
inst_3 : Finite G
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
h2 : Function.Involutive.{u_2 + 1} (α := G) (⇑φ : (a : G) → G)
g h : G
key : (φ : (a : G) → G) (g * h) = HMul.hMul (α := G) (β := G) ((φ : (a : G) → G) g : G) ((φ : (a : G) → G) h : G)
rwa :
  ∀ (key : (fun (x : G) ↦ x⁻¹) (g * h) = HMul.hMul (α := G) ((fun (x : G) ↦ x⁻¹) g) ((fun (x : G) ↦ x⁻¹) h)),
    Commute g h
rwa₁ : ∀ (key : g * h = (HMul.hMul (α := G) ((fun (x : G) ↦ x⁻¹) g) ((fun (x : G) ↦ x⁻¹) h))⁻¹), Commute g h
rwa₂ : ∀ (key : g * h = HMul.hMul (α := G) ((fun (x : G) ↦ x⁻¹) h)⁻¹ ((fun (x : G) ↦ x⁻¹) g)⁻¹), Commute g h
rwa₃ : ∀ (key : g * h = h * ((fun (x : G) ↦ x⁻¹) g)⁻¹), Commute g h
⊢ Commute g h
have rwa₄ : ∀ (key : g * h = h * g), Commute g h
Tactic: rwa [hφ.coe_eq_inv_of_involutive h2, inv_eq_iff_eq_inv, mul_inv_rev, inv_inv, inv_inv] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.GroupTheory.FixedPointFree (goal)
Goal:
F : Type u_1
G : Type u_2
inst : Group G
inst_1 : FunLike F G G
inst_2 : MonoidHomClass F G G
φ : F
inst_3 : Finite G
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
h2 : Function.Involutive.{u_2 + 1} (α := G) (⇑φ : (a : G) → G)
g : G
hg : orderOf g = 2
⊢ (φ : (a : G) → G) g = g
have rw : (fun (x : G) ↦ x⁻¹) g = g
Tactic: rw [hφ.coe_eq_inv_of_involutive h2, inv_eq_iff_mul_eq_one, ← sq, ← hg, pow_orderOf_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.FixedPointFree (goal)
Goal:
F : Type u_1
G : Type u_2
inst : Group G
inst_1 : FunLike F G G
inst_2 : MonoidHomClass F G G
φ : F
inst_3 : Finite G
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
h2 : Function.Involutive.{u_2 + 1} (α := G) (⇑φ : (a : G) → G)
g : G
hg : orderOf g = 2
rw : (fun (x : G) ↦ x⁻¹) g = g
⊢ (φ : (a : G) → G) g = g
have rw₁ : g * g = 1
Tactic: rw [hφ.coe_eq_inv_of_involutive h2, inv_eq_iff_mul_eq_one, ← sq, ← hg, pow_orderOf_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.FixedPointFree (goal)
Goal:
F : Type u_1
G : Type u_2
inst : Group G
inst_1 : FunLike F G G
inst_2 : MonoidHomClass F G G
φ : F
inst_3 : Finite G
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
h2 : Function.Involutive.{u_2 + 1} (α := G) (⇑φ : (a : G) → G)
g : G
hg : orderOf g = 2
rw : (fun (x : G) ↦ x⁻¹) g = g
rw₁ : g * g = 1
⊢ (φ : (a : G) → G) g = g
have rw₂ : HPow.hPow (β := ℕ) g 2 = 1
Tactic: rw [hφ.coe_eq_inv_of_involutive h2, inv_eq_iff_mul_eq_one, ← sq, ← hg, pow_orderOf_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.FixedPointFree (goal)
Goal:
F : Type u_1
G : Type u_2
inst : Group G
inst_1 : FunLike F G G
inst_2 : MonoidHomClass F G G
φ : F
inst_3 : Finite G
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
h2 : Function.Involutive.{u_2 + 1} (α := G) (⇑φ : (a : G) → G)
g : G
hg : orderOf g = 2
rw : (fun (x : G) ↦ x⁻¹) g = g
rw₁ : g * g = 1
rw₂ : HPow.hPow (β := ℕ) g 2 = 1
⊢ (φ : (a : G) → G) g = g
have rw₃ : g ^ orderOf g = 1
Tactic: rw [hφ.coe_eq_inv_of_involutive h2, inv_eq_iff_mul_eq_one, ← sq, ← hg, pow_orderOf_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.FixedPointFree (goal)
Goal:
F : Type u_1
G : Type u_2
inst : Group G
inst_1 : FunLike F G G
inst_2 : MonoidHomClass F G G
φ : F
inst_3 : Finite G
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
h2 : Function.Involutive.{u_2 + 1} (α := G) (⇑φ : (a : G) → G)
g : G
hg : orderOf g = 2
rw : (fun (x : G) ↦ x⁻¹) g = g
rw₁ : g * g = 1
rw₂ : HPow.hPow (β := ℕ) g 2 = 1
rw₃ : g ^ orderOf g = 1
⊢ (φ : (a : G) → G) g = g
have rw₄ : Eq.{u_2 + 1} (α := G) 1 1
Tactic: rw [hφ.coe_eq_inv_of_involutive h2, inv_eq_iff_mul_eq_one, ← sq, ← hg, pow_orderOf_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.FixedPointFree (hypothesis)
Goal:
F : Type u_1
G : Type u_2
inst : Group G
inst_1 : FunLike F G G
inst_2 : MonoidHomClass F G G
φ : F
inst_3 : Finite G
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
h2 : Function.Involutive.{u_2 + 1} (α := G) (⇑φ : (a : G) → G)
g : G
hg : orderOf g = 2
⊢ False
have key : (φ : (a : G) → G) g = g
Tactic: have key : φ g = g := by
    rw [hφ.coe_eq_inv_of_involutive h2, inv_eq_iff_mul_eq_one, ← sq, ← hg, pow_orderOf_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.FixedPointFree (hypothesis)
Goal:
F : Type u_1
G : Type u_2
inst : Group G
inst_1 : FunLike F G G
inst_2 : MonoidHomClass F G G
φ : F
inst_3 : Finite G
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
h2 : Function.Involutive.{u_2 + 1} (α := G) (⇑φ : (a : G) → G)
g : G
hg : orderOf g = 2
key : (φ : (a : G) → G) g = g
⊢ False
have hg₁ : Eq (α := ℕ) 1 2
Tactic: rw [hφ g key, orderOf_one] at hg
Cleared hypotheses: hg, key
-- Lean 4 proof step from Mathlib.GroupTheory.FixedPointFree (goal)
Goal:
F : Type u_1
G : Type u_2
inst : Group G
inst_1 : FunLike F G G
inst_2 : MonoidHomClass F G G
φ : F
inst_3 : Finite G
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
h2 : Function.Involutive.{u_2 + 1} (α := G) (⇑φ : (a : G) → G)
⊢ Odd (Nat.card G)
have have : ∀ (this : Fintype G), Odd (Nat.card G)
Tactic: have := Fintype.ofFinite G
-- Lean 4 proof step from Mathlib.GroupTheory.FixedPointFree (goal)
Goal:
F : Type u_1
G : Type u_2
inst : Group G
inst_1 : FunLike F G G
inst_2 : MonoidHomClass F G G
φ : F
inst_3 : Finite G
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
h2 : Function.Involutive.{u_2 + 1} (α := G) (⇑φ : (a : G) → G)
this : Fintype G
⊢ Odd (Nat.card G)
have by_contra : ∀ (h : ¬Odd (Nat.card G)), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.GroupTheory.FixedPointFree (hypothesis)
Goal:
F : Type u_1
G : Type u_2
inst : Group G
inst_1 : FunLike F G G
inst_2 : MonoidHomClass F G G
φ : F
inst_3 : Finite G
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
h2 : Function.Involutive.{u_2 + 1} (α := G) (⇑φ : (a : G) → G)
this : Fintype G
h : ¬Odd (Nat.card G)
⊢ False
have h₁ : 2 ∣ Fintype.card G
Tactic: rw [Nat.not_odd_iff_even, even_iff_two_dvd, Nat.card_eq_fintype_card] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.FixedPointFree (goal)
Goal:
F : Type u_1
G : Type u_2
inst : Group G
inst_1 : FunLike F G G
inst_2 : MonoidHomClass F G G
φ : F
inst_3 : Finite G
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
h2 : Function.Involutive.{u_2 + 1} (α := G) (⇑φ : (a : G) → G)
this : Fintype G
h : 2 ∣ Fintype.card G
⊢ False
have obtain : ∀ (g : G) (hg : orderOf g = 2), False
Tactic: obtain ⟨g, hg⟩ := exists_prime_orderOf_dvd_card 2 h
-- Lean 4 proof step from Mathlib.GroupTheory.Focal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H.focalSubgroup ≤ H
have rw : {g : G | g ∈ H ∧ ∃ x ∈ H, ∃ (u : G), g = ⁅x, u⁆} ⊆ (↑H : Set G)
Tactic: rw [focalSubgroup_def, closure_le]
-- Lean 4 proof step from Mathlib.GroupTheory.Focal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H.focalSubgroupOf.Normal
have rw : ∀ (h k : G), h ∈ H.focalSubgroup → k ∈ H → k * h * k⁻¹ ∈ H.focalSubgroup
Tactic: rw [focalSubgroupOf_def, normal_subgroupOf_iff (focalSubgroup_le H)]
-- Lean 4 proof step from Mathlib.GroupTheory.Focal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
n g : G
hg : g ∈ H
z : G
hz : Membership.mem (γ := Set G) {g : G | g ∈ H ∧ ∃ x ∈ H, ∃ (u : G), g = ⁅x, u⁆} z
⊢ g * z * g⁻¹ ∈ H.focalSubgroup
have mem : ∀ (x : G) (hxP : x ∈ H) (u : G) (hzH : ⁅x, u⁆ ∈ H), g * ⁅x, u⁆ * g⁻¹ ∈ H.focalSubgroup
Tactic: obtain ⟨hzH, x, hxP, u, rfl⟩ := hz
Cleared hypotheses: z, hz
-- Lean 4 proof step from Mathlib.GroupTheory.Focal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
n g : G
hn : n ∈ H.focalSubgroup
hg : g ∈ H
⊢ g * n * g⁻¹ ∈ H.focalSubgroup
have mem : ∀ (z : G) (hz : Membership.mem (γ := Set G) {g : G | g ∈ H ∧ ∃ x ∈ H, ∃ (u : G), g = ⁅x, u⁆} z),
  g * z * g⁻¹ ∈ H.focalSubgroup
Tactic: induction hn using closure_induction with
  | mem z hz =>
    obtain ⟨hzH, x, hxP, u, rfl⟩ := hz
    exact subset_closure ⟨by aesop, g * x * g⁻¹, by aesop, g * u * g⁻¹, by group⟩
  | one => simp
  | mul _ _ _ _ IHa IHb => simpa using mul_mem IHa IHb
  | inv _ _ IH => simpa [mul_assoc] using inv_mem IH
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.GroupTheory.Focal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
n g : G
hn : n ∈ H.focalSubgroup
hg : g ∈ H
mem :
  ∀ (z : G) (hz : Membership.mem (γ := Set G) {g : G | g ∈ H ∧ ∃ x ∈ H, ∃ (u : G), g = ⁅x, u⁆} z),
    g * z * g⁻¹ ∈ H.focalSubgroup
⊢ g * n * g⁻¹ ∈ H.focalSubgroup
have one : g * 1 * g⁻¹ ∈ H.focalSubgroup
Tactic: induction hn using closure_induction with
  | mem z hz =>
    obtain ⟨hzH, x, hxP, u, rfl⟩ := hz
    exact subset_closure ⟨by aesop, g * x * g⁻¹, by aesop, g * u * g⁻¹, by group⟩
  | one => simp
  | mul _ _ _ _ IHa IHb => simpa using mul_mem IHa IHb
  | inv _ _ IH => simpa [mul_assoc] using inv_mem IH
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.GroupTheory.Focal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
n g : G
hn : n ∈ H.focalSubgroup
hg : g ∈ H
mem :
  ∀ (z : G) (hz : Membership.mem (γ := Set G) {g : G | g ∈ H ∧ ∃ x ∈ H, ∃ (u : G), g = ⁅x, u⁆} z),
    g * z * g⁻¹ ∈ H.focalSubgroup
one : g * 1 * g⁻¹ ∈ H.focalSubgroup
⊢ g * n * g⁻¹ ∈ H.focalSubgroup
have mul : ∀ (x y : G),
  Membership.mem (γ := Subgroup G) (closure {g : G | g ∈ H ∧ ∃ x ∈ H, ∃ (u : G), g = ⁅x, u⁆}) x →
    Membership.mem (γ := Subgroup G) (closure {g : G | g ∈ H ∧ ∃ x ∈ H, ∃ (u : G), g = ⁅x, u⁆}) y →
      ∀ (IHa : g * x * g⁻¹ ∈ H.focalSubgroup) (IHb : g * y * g⁻¹ ∈ H.focalSubgroup), g * (x * y) * g⁻¹ ∈ H.focalSubgroup
Tactic: induction hn using closure_induction with
  | mem z hz =>
    obtain ⟨hzH, x, hxP, u, rfl⟩ := hz
    exact subset_closure ⟨by aesop, g * x * g⁻¹, by aesop, g * u * g⁻¹, by group⟩
  | one => simp
  | mul _ _ _ _ IHa IHb => simpa using mul_mem IHa IHb
  | inv _ _ IH => simpa [mul_assoc] using inv_mem IH
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.GroupTheory.Focal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
n g : G
hn : n ∈ H.focalSubgroup
hg : g ∈ H
mem :
  ∀ (z : G) (hz : Membership.mem (γ := Set G) {g : G | g ∈ H ∧ ∃ x ∈ H, ∃ (u : G), g = ⁅x, u⁆} z),
    g * z * g⁻¹ ∈ H.focalSubgroup
one : g * 1 * g⁻¹ ∈ H.focalSubgroup
mul :
  ∀ (x y : G),
    Membership.mem (γ := Subgroup G) (closure {g : G | g ∈ H ∧ ∃ x ∈ H, ∃ (u : G), g = ⁅x, u⁆}) x →
      Membership.mem (γ := Subgroup G) (closure {g : G | g ∈ H ∧ ∃ x ∈ H, ∃ (u : G), g = ⁅x, u⁆}) y →
        ∀ (IHa : g * x * g⁻¹ ∈ H.focalSubgroup) (IHb : g * y * g⁻¹ ∈ H.focalSubgroup),
          g * (x * y) * g⁻¹ ∈ H.focalSubgroup
⊢ g * n * g⁻¹ ∈ H.focalSubgroup
have inv : ∀ (x : G),
  Membership.mem (γ := Subgroup G) (closure {g : G | g ∈ H ∧ ∃ x ∈ H, ∃ (u : G), g = ⁅x, u⁆}) x →
    ∀ (IH : g * x * g⁻¹ ∈ H.focalSubgroup), g * x⁻¹ * g⁻¹ ∈ H.focalSubgroup
Tactic: induction hn using closure_induction with
  | mem z hz =>
    obtain ⟨hzH, x, hxP, u, rfl⟩ := hz
    exact subset_closure ⟨by aesop, g * x * g⁻¹, by aesop, g * u * g⁻¹, by group⟩
  | one => simp
  | mul _ _ _ _ IHa IHb => simpa using mul_mem IHa IHb
  | inv _ _ IH => simpa [mul_assoc] using inv_mem IH
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.GroupTheory.Focal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H.focalSubgroup ≤ _root_.commutator G
have rw : {g : G | g ∈ H ∧ ∃ x ∈ H, ∃ (u : G), g = ⁅x, u⁆} ⊆ (↑(_root_.commutator G) : Set G)
Tactic: rw [focalSubgroup_def, closure_le]
-- Lean 4 proof step from Mathlib.GroupTheory.Focal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : G
hh : h ∈ H
g : G
hconj : g⁻¹ * h * g ∈ H
⊢ Eq (α := ↥H ⧸ H.focalSubgroupOf)
    ((QuotientGroup.mk' H.focalSubgroupOf : (a : ↥H) → ↥H ⧸ H.focalSubgroupOf)
        (Subtype.mk (p := fun (x : G) ↦ x ∈ H) (g⁻¹ * h * g) hconj) :
      ↥H ⧸ H.focalSubgroupOf)
    ((QuotientGroup.mk' H.focalSubgroupOf : (a : ↥H) → ↥H ⧸ H.focalSubgroupOf)
        (Subtype.mk (p := fun (x : G) ↦ x ∈ H) h hh) :
      ↥H ⧸ H.focalSubgroupOf)
have apply : (Subtype.mk (p := fun (x : G) ↦ x ∈ H) (g⁻¹ * h * g) hconj)⁻¹ * Subtype.mk (p := fun (x : G) ↦ x ∈ H) h hh ∈
  H.focalSubgroupOf
Tactic: apply QuotientGroup.eq.mpr
-- Lean 4 proof step from Mathlib.GroupTheory.Focal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : G
hh : h ∈ H
g : G
hconj : g⁻¹ * h * g ∈ H
⊢ (Subtype.mk (p := fun (x : G) ↦ x ∈ H) (g⁻¹ * h * g) hconj)⁻¹ * Subtype.mk (p := fun (x : G) ↦ x ∈ H) h hh ∈
    H.focalSubgroupOf
have rw : (↑((Subtype.mk (p := fun (x : G) ↦ x ∈ H) (g⁻¹ * h * g) hconj)⁻¹ * Subtype.mk (p := fun (x : G) ↦ x ∈ H) h hh) : G) ∈
  H.focalSubgroup
Tactic: rw [focalSubgroupOf_def, mem_subgroupOf]
-- Lean 4 proof step from Mathlib.GroupTheory.Focal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : G
hh : h ∈ H
g : G
hconj : g⁻¹ * h * g ∈ H
⊢ (↑((Subtype.mk (p := fun (x : G) ↦ x ∈ H) (g⁻¹ * h * g) hconj)⁻¹ * Subtype.mk (p := fun (x : G) ↦ x ∈ H) h hh) : G) ∈
    H.focalSubgroup
have a : Membership.mem (γ := Set G) {g : G | g ∈ H ∧ ∃ x ∈ H, ∃ (u : G), g = ⁅x, u⁆}
  (↑((Subtype.mk (p := fun (x : G) ↦ x ∈ H) (g⁻¹ * h * g) hconj)⁻¹ * Subtype.mk (p := fun (x : G) ↦ x ∈ H) h hh) : G)
Tactic: apply subset_closure
-- Lean 4 proof step from Mathlib.GroupTheory.Focal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : G
hh : h ∈ H
g : G
hconj : g⁻¹ * h * g ∈ H
⊢ Membership.mem (γ := Set G) {g : G | g ∈ H ∧ ∃ x ∈ H, ∃ (u : G), g = ⁅x, u⁆}
    (↑((Subtype.mk (p := fun (x : G) ↦ x ∈ H) (g⁻¹ * h * g) hconj)⁻¹ * Subtype.mk (p := fun (x : G) ↦ x ∈ H) h hh) : G)
have a : Membership.mem (γ := Set G) {g : G | g ∈ H ∧ ∃ x ∈ H, ∃ (u : G), g = ⁅x, u⁆} ((g⁻¹ * h * g)⁻¹ * h)
Tactic: simp only [coe_mul, coe_inv]
-- Lean 4 proof step from Mathlib.GroupTheory.Focal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H.focalSubgroupOf = closure {g : ↥H | ∃ x ∈ H, ∃ (u : G), (↑g : G) = ⁅x, u⁆}
have rw : Eq (α := Subgroup G) (closure {g : G | g ∈ H ∧ ∃ x ∈ H, ∃ (u : G), g = ⁅x, u⁆})
  (closure (Set.image (α := ↥H) (⇑H.subtype : (a : ↥H) → G) {g : ↥H | ∃ x ∈ H, ∃ (u : G), (↑g : G) = ⁅x, u⁆}))
Tactic: rw [← map_subtype_inj, map_focalSubgroupOf, MonoidHom.map_closure, focalSubgroup_def]
-- Lean 4 proof step from Mathlib.GroupTheory.Focal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ Eq (α := Subgroup G) (closure {g : G | g ∈ H ∧ ∃ x ∈ H, ∃ (u : G), g = ⁅x, u⁆})
    (closure (Set.image (α := ↥H) (⇑H.subtype : (a : ↥H) → G) {g : ↥H | ∃ x ∈ H, ∃ (u : G), (↑g : G) = ⁅x, u⁆}))
have e_k : Eq.{u_1 + 1} (α := G → Prop) (fun (g : G) ↦ g ∈ H ∧ ∃ x ∈ H, ∃ (u : G), g = ⁅x, u⁆) fun (x : G) ↦
  ∃ (a : ↥H),
    Membership.mem (γ := Set ↥H) {g : ↥H | ∃ x ∈ H, ∃ (u : G), (↑g : G) = ⁅x, u⁆} a ∧ (H.subtype : (a : ↥H) → G) a = x
Tactic: congr
-- Lean 4 proof step from Mathlib.GroupTheory.Focal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ Eq.{u_1 + 1} (α := G → Prop) (fun (g : G) ↦ g ∈ H ∧ ∃ x ∈ H, ∃ (u : G), g = ⁅x, u⁆) fun (x : G) ↦
    ∃ (a : ↥H),
      Membership.mem (γ := Set ↥H) {g : ↥H | ∃ x ∈ H, ∃ (u : G), (↑g : G) = ⁅x, u⁆} a ∧ (H.subtype : (a : ↥H) → G) a = x
have e_k : Eq.{u_1 + 1} (α := G → Prop) (fun (g : G) ↦ g ∈ H ∧ ∃ x ∈ H, ∃ (u : G), g = ⁅x, u⁆) fun (x : G) ↦
  (∃ x_1 ∈ H, ∃ (u : G), x = ⁅x_1, u⁆) ∧ x ∈ H
Tactic: simp
-- Lean 4 proof step from Mathlib.GroupTheory.Focal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ _root_.commutator ↥H ≤ H.focalSubgroupOf
have rw : LE.le.{u_1} (α := Subgroup ↥H) (_root_.commutator ↥H) (closure {g : ↥H | ∃ x ∈ H, ∃ (u : G), (↑g : G) = ⁅x, u⁆})
Tactic: rw [focalSubgroupOf_eq_closure]
-- Lean 4 proof step from Mathlib.GroupTheory.Focal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ LE.le.{u_1} (α := Subgroup ↥H) (_root_.commutator ↥H) (closure {g : ↥H | ∃ x ∈ H, ∃ (u : G), (↑g : G) = ⁅x, u⁆})
have h' : Subset.{u_1} (α := Set ↥H)
  {g : ↥H |
    ∃ (g₁ : ↥H),
      Membership.mem (γ := Subgroup ↥H) ⊤ g₁ ∧ ∃ (g₂ : ↥H), Membership.mem (γ := Subgroup ↥H) ⊤ g₂ ∧ ⁅g₁, g₂⁆ = g}
  {g : ↥H | ∃ x ∈ H, ∃ (u : G), (↑g : G) = ⁅x, u⁆}
Tactic: apply closure_mono
-- Lean 4 proof step from Mathlib.GroupTheory.Focal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ ⁅H, H⁆ ≤ H.focalSubgroup
have grw : map H.subtype (_root_.commutator ↥H) ≤ H.focalSubgroup
Tactic: grw [← map_subtype_commutator, H.commutator_le_focalSubgroupOf, map_focalSubgroupOf]
-- Lean 4 proof step from Mathlib.GroupTheory.Focal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
grw : map H.subtype (_root_.commutator ↥H) ≤ H.focalSubgroup
⊢ ⁅H, H⁆ ≤ H.focalSubgroup
have grw₁ : map H.subtype H.focalSubgroupOf ≤ H.focalSubgroup
Tactic: grw [← map_subtype_commutator, H.commutator_le_focalSubgroupOf, map_focalSubgroupOf]
-- Lean 4 proof step from Mathlib.GroupTheory.Focal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
grw : map H.subtype (_root_.commutator ↥H) ≤ H.focalSubgroup
grw₁ : map H.subtype H.focalSubgroupOf ≤ H.focalSubgroup
⊢ ⁅H, H⁆ ≤ H.focalSubgroup
have grw₂ : H.focalSubgroup ≤ H.focalSubgroup
Tactic: grw [← map_subtype_commutator, H.commutator_le_focalSubgroupOf, map_focalSubgroupOf]
-- Lean 4 proof step from Mathlib.GroupTheory.Focal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.FiniteIndex
x : ↥H
⊢ (H.transferFocal : (a : G) → ↥H ⧸ H.focalSubgroupOf) (↑x : G) =
    HPow.hPow (α := ↥H ⧸ H.focalSubgroupOf) (↑x : ↥H ⧸ H.focalSubgroupOf) H.index
have have : ∀ (this : Fintype (Quotient (α := G ⧸ H) (MulAction.orbitRel (↥(zpowers (↑x : G))) (G ⧸ H)))),
  (H.transferFocal : (a : G) → ↥H ⧸ H.focalSubgroupOf) (↑x : G) =
    HPow.hPow (α := ↥H ⧸ H.focalSubgroupOf) (↑x : ↥H ⧸ H.focalSubgroupOf) H.index
Tactic: have : Fintype (Quotient (MulAction.orbitRel (zpowers (x : G)) (G ⧸ H))) :=
    Fintype.ofFinite _
-- Lean 4 proof step from Mathlib.GroupTheory.Focal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.FiniteIndex
x : ↥H
this : Fintype (Quotient (α := G ⧸ H) (MulAction.orbitRel (↥(zpowers (↑x : G))) (G ⧸ H)))
⊢ (H.transferFocal : (a : G) → ↥H ⧸ H.focalSubgroupOf) (↑x : G) =
    HPow.hPow (α := ↥H ⧸ H.focalSubgroupOf) (↑x : ↥H ⧸ H.focalSubgroupOf) H.index
have rw : Eq.{u_1 + 1} (α := ↥H ⧸ H.focalSubgroupOf)
  (∏ q : Quotient (MulAction.orbitRel (↥(zpowers (↑x : G))) (G ⧸ H)),
    (QuotientGroup.mk' H.focalSubgroupOf : (a : ↥H) → ↥H ⧸ H.focalSubgroupOf)
      (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
        ((Quotient.out q.out)⁻¹ * (↑x : G) ^ minimalPeriod (fun (x_1 : G ⧸ H) ↦ (↑x : G) • x_1) q.out *
          Quotient.out q.out)
        sorry))
  (∏ i : Quotient (MulAction.orbitRel (↥(zpowers (↑x : G))) (G ⧸ H)),
    HPow.hPow (α := ↥H ⧸ H.focalSubgroupOf) (↑x : ↥H ⧸ H.focalSubgroupOf)
      (minimalPeriod (fun (x_1 : G ⧸ H) ↦ (↑x : G) • x_1) i.out))
Tactic: rw [transferFocal, index_eq_sum_minimalPeriod H x, ← Finset.prod_pow_eq_pow_sum,
    MonoidHom.transfer_eq_prod_quotient_orbitRel_zpowers_quot]