awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_5
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : IsOrderedCancelMonoid M
inst_4 : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : Set.IsPWO.{u_5} (α := M) {x : M | x ∈ P ∧ x ≠ 1}
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
y : M
h : Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} y
hy₁ : y ∈ P
hy₂ : y ≠ 1
ih :
  ∀ z ∈ P,
    z ≠ 1 →
      z ≤ y → ¬y ≤ z → Membership.mem (γ := Submonoid M) (closure {x : M | Minimal (fun (x : M) ↦ x ∈ P ∧ x ≠ 1) x}) z
⊢ Membership.mem (γ := Submonoid M)
    (closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) x}) y
have pos : ∀ (hy₃ : Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) y),
  Membership.mem (γ := Submonoid M)
    (closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) x}) y
Tactic: by_cases hy₃ : Minimal (· ∈ { x | x ∈ P ∧ x ≠ 1 }) y
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_5
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : IsOrderedCancelMonoid M
inst_4 : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : Set.IsPWO.{u_5} (α := M) {x : M | x ∈ P ∧ x ≠ 1}
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
y : M
h : Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} y
hy₁ : y ∈ P
hy₂ : y ≠ 1
ih :
  ∀ z ∈ P,
    z ≠ 1 →
      z ≤ y → ¬y ≤ z → Membership.mem (γ := Submonoid M) (closure {x : M | Minimal (fun (x : M) ↦ x ∈ P ∧ x ≠ 1) x}) z
pos :
  ∀ (hy₃ : Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) y),
    Membership.mem (γ := Submonoid M)
      (closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) x}) y
⊢ Membership.mem (γ := Submonoid M)
    (closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) x}) y
have neg : ∀ (hy₃ : ¬Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) y),
  Membership.mem (γ := Submonoid M)
    (closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) x}) y
Tactic: by_cases hy₃ : Minimal (· ∈ { x | x ∈ P ∧ x ≠ 1 }) y
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_5
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : IsOrderedCancelMonoid M
inst_4 : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : Set.IsPWO.{u_5} (α := M) {x : M | x ∈ P ∧ x ≠ 1}
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
y : M
h : Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} y
hy₁ : y ∈ P
hy₂ : y ≠ 1
ih :
  ∀ z ∈ P,
    z ≠ 1 →
      z ≤ y → ¬y ≤ z → Membership.mem (γ := Submonoid M) (closure {x : M | Minimal (fun (x : M) ↦ x ∈ P ∧ x ≠ 1) x}) z
hy₃ : ¬Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) y
⊢ Membership.mem (γ := Submonoid M)
    (closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) x}) y
have neg : ∀ (z : M) (hz₁ : z < y) (hz₂ : z ∈ P) (hz₃ : z ≠ 1),
  Membership.mem (γ := Submonoid M)
    (closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) x}) y
Tactic: rcases exists_lt_of_not_minimal ⟨hy₁, hy₂⟩ hy₃ with ⟨z, hz₁, hz₂, hz₃⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_5
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : IsOrderedCancelMonoid M
inst_4 : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : Set.IsPWO.{u_5} (α := M) {x : M | x ∈ P ∧ x ≠ 1}
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
y : M
h : Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} y
hy₁ : y ∈ P
hy₂ : y ≠ 1
ih :
  ∀ z ∈ P,
    z ≠ 1 →
      z ≤ y → ¬y ≤ z → Membership.mem (γ := Submonoid M) (closure {x : M | Minimal (fun (x : M) ↦ x ∈ P ∧ x ≠ 1) x}) z
hy₃ : ¬Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) y
z : M
hz₁ : z < y
hz₂ : z ∈ P
hz₃ : z ≠ 1
⊢ Membership.mem (γ := Submonoid M)
    (closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) x}) y
have neg : ∀ (y : M),
  Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} (z * y) →
    ∀ (hy₁ : z * y ∈ P) (hy₂ : z * y ≠ 1)
      (ih :
        ∀ z_1 ∈ P,
          z_1 ≠ 1 →
            z_1 ≤ z * y →
              ¬z * y ≤ z_1 →
                Membership.mem (γ := Submonoid M) (closure {x : M | Minimal (fun (x : M) ↦ x ∈ P ∧ x ≠ 1) x}) z_1)
      (hy₃ : ¬Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) (z * y)) (hz₁ : z < z * y),
      Membership.mem (γ := Submonoid M)
        (closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) x}) (z * y)
Tactic: rcases exists_mul_of_le hz₁.le with ⟨y, rfl⟩
Cleared hypotheses: y, h, hy₁, hy₂, ih, hy₃, hz₁
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_5
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : IsOrderedCancelMonoid M
inst_4 : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : Set.IsPWO.{u_5} (α := M) {x : M | x ∈ P ∧ x ≠ 1}
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
h : Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} (z * y)
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih :
  ∀ z_1 ∈ P,
    z_1 ≠ 1 →
      z_1 ≤ z * y →
        ¬z * y ≤ z_1 → Membership.mem (γ := Submonoid M) (closure {x : M | Minimal (fun (x : M) ↦ x ∈ P ∧ x ≠ 1) x}) z_1
hy₃ : ¬Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) (z * y)
hz₁ : z < z * y
⊢ Membership.mem (γ := Submonoid M)
    (closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) x}) (z * y)
have neg : Membership.mem (γ := Submonoid M)
  (closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) x}) z
Tactic: apply mul_mem
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_5
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : IsOrderedCancelMonoid M
inst_4 : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : Set.IsPWO.{u_5} (α := M) {x : M | x ∈ P ∧ x ≠ 1}
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
h : Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} (z * y)
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih :
  ∀ z_1 ∈ P,
    z_1 ≠ 1 →
      z_1 ≤ z * y →
        ¬z * y ≤ z_1 → Membership.mem (γ := Submonoid M) (closure {x : M | Minimal (fun (x : M) ↦ x ∈ P ∧ x ≠ 1) x}) z_1
hy₃ : ¬Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) (z * y)
hz₁ : z < z * y
neg :
  Membership.mem (γ := Submonoid M)
    (closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) x}) z
⊢ Membership.mem (γ := Submonoid M)
    (closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) x}) (z * y)
have neg₁ : Membership.mem (γ := Submonoid M)
  (closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) x}) y
Tactic: apply mul_mem
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_5
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : IsOrderedCancelMonoid M
inst_4 : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : Set.IsPWO.{u_5} (α := M) {x : M | x ∈ P ∧ x ≠ 1}
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
h : Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} (z * y)
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih :
  ∀ z_1 ∈ P,
    z_1 ≠ 1 →
      z_1 ≤ z * y →
        ¬z * y ≤ z_1 → Membership.mem (γ := Submonoid M) (closure {x : M | Minimal (fun (x : M) ↦ x ∈ P ∧ x ≠ 1) x}) z_1
hy₃ : ¬Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) (z * y)
hz₁ : z < z * y
⊢ Membership.mem (γ := Submonoid M)
    (closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) x}) y
have neg : y ∈ P
Tactic: apply ih
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_5
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : IsOrderedCancelMonoid M
inst_4 : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : Set.IsPWO.{u_5} (α := M) {x : M | x ∈ P ∧ x ≠ 1}
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
h : Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} (z * y)
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih :
  ∀ z_1 ∈ P,
    z_1 ≠ 1 →
      z_1 ≤ z * y →
        ¬z * y ≤ z_1 → Membership.mem (γ := Submonoid M) (closure {x : M | Minimal (fun (x : M) ↦ x ∈ P ∧ x ≠ 1) x}) z_1
hy₃ : ¬Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) (z * y)
hz₁ : z < z * y
neg : y ∈ P
⊢ Membership.mem (γ := Submonoid M)
    (closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) x}) y
have neg₁ : y ≠ 1
Tactic: apply ih
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_5
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : IsOrderedCancelMonoid M
inst_4 : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : Set.IsPWO.{u_5} (α := M) {x : M | x ∈ P ∧ x ≠ 1}
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
h : Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} (z * y)
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih :
  ∀ z_1 ∈ P,
    z_1 ≠ 1 →
      z_1 ≤ z * y →
        ¬z * y ≤ z_1 → Membership.mem (γ := Submonoid M) (closure {x : M | Minimal (fun (x : M) ↦ x ∈ P ∧ x ≠ 1) x}) z_1
hy₃ : ¬Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) (z * y)
hz₁ : z < z * y
neg : y ∈ P
neg₁ : y ≠ 1
⊢ Membership.mem (γ := Submonoid M)
    (closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) x}) y
have neg₂ : y ≤ z * y
Tactic: apply ih
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_5
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : IsOrderedCancelMonoid M
inst_4 : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : Set.IsPWO.{u_5} (α := M) {x : M | x ∈ P ∧ x ≠ 1}
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
h : Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} (z * y)
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih :
  ∀ z_1 ∈ P,
    z_1 ≠ 1 →
      z_1 ≤ z * y →
        ¬z * y ≤ z_1 → Membership.mem (γ := Submonoid M) (closure {x : M | Minimal (fun (x : M) ↦ x ∈ P ∧ x ≠ 1) x}) z_1
hy₃ : ¬Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) (z * y)
hz₁ : z < z * y
neg : y ∈ P
neg₁ : y ≠ 1
neg₂ : y ≤ z * y
⊢ Membership.mem (γ := Submonoid M)
    (closure {x : M | Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) x}) y
have neg₃ : ¬z * y ≤ y
Tactic: apply ih
-- Lean 4 proof step from Mathlib.GroupTheory.Finiteness (goal)
Goal:
M : Type u_5
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : IsOrderedCancelMonoid M
inst_4 : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : Set.IsPWO.{u_5} (α := M) {x : M | x ∈ P ∧ x ≠ 1}
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
h : Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} (z * y)
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih :
  ∀ z_1 ∈ P,
    z_1 ≠ 1 →
      z_1 ≤ z * y →
        ¬z * y ≤ z_1 → Membership.mem (γ := Submonoid M) (closure {x : M | Minimal (fun (x : M) ↦ x ∈ P ∧ x ≠ 1) x}) z_1
hy₃ : ¬Minimal (fun (x : M) ↦ Membership.mem (γ := Set M) {x : M | x ∈ P ∧ x ≠ 1} x) (z * y)
hz₁ : z < z * y
⊢ ¬z * y ≤ y
have neg : ¬z ≤ 1
Tactic: rw [mul_le_iff_le_one_left']
-- 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
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
⊢ Function.Injective.{u_2 + 1, u_2 + 1} (α := G) (commutatorMap (⇑φ : (a : G) → G))
have refine : ∀ (x y : G) (h : commutatorMap (⇑φ : (a : G) → G) x = commutatorMap (⇑φ : (a : G) → G) y),
  (φ : (a : G) → G) (x⁻¹ * y) = x⁻¹ * y
Tactic: refine fun x y h ↦ inv_mul_eq_one.mp <| 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
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
x y : G
h : commutatorMap (⇑φ : (a : G) → G) x = commutatorMap (⇑φ : (a : G) → G) y
⊢ (φ : (a : G) → G) (x⁻¹ * y) = x⁻¹ * y
have rwa : HMul.hMul (α := G) (β := G) ((φ : (a : G) → G) x⁻¹ : G) ((φ : (a : G) → G) y : G) = x⁻¹ * y
Tactic: rwa [map_mul, map_inv, eq_inv_mul_iff_mul_eq, ← mul_assoc, ← eq_div_iff_mul_eq', ← division_def]
-- 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
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
x y : G
h : commutatorMap (⇑φ : (a : G) → G) x = commutatorMap (⇑φ : (a : G) → G) y
rwa : HMul.hMul (α := G) (β := G) ((φ : (a : G) → G) x⁻¹ : G) ((φ : (a : G) → G) y : G) = x⁻¹ * y
⊢ (φ : (a : G) → G) (x⁻¹ * y) = x⁻¹ * y
have rwa₁ : HMul.hMul (α := G) (β := G) (((φ : (a : G) → G) x)⁻¹ : G) ((φ : (a : G) → G) y : G) = x⁻¹ * y
Tactic: rwa [map_mul, map_inv, eq_inv_mul_iff_mul_eq, ← mul_assoc, ← eq_div_iff_mul_eq', ← division_def]
-- 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
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
x y : G
h : commutatorMap (⇑φ : (a : G) → G) x = commutatorMap (⇑φ : (a : G) → G) y
rwa : HMul.hMul (α := G) (β := G) ((φ : (a : G) → G) x⁻¹ : G) ((φ : (a : G) → G) y : G) = x⁻¹ * y
rwa₁ : HMul.hMul (α := G) (β := G) (((φ : (a : G) → G) x)⁻¹ : G) ((φ : (a : G) → G) y : G) = x⁻¹ * y
⊢ (φ : (a : G) → G) (x⁻¹ * y) = x⁻¹ * y
have rwa₂ : x * HMul.hMul (α := G) (β := G) (((φ : (a : G) → G) x)⁻¹ : G) ((φ : (a : G) → G) y : G) = y
Tactic: rwa [map_mul, map_inv, eq_inv_mul_iff_mul_eq, ← mul_assoc, ← eq_div_iff_mul_eq', ← division_def]
-- 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
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
x y : G
h : commutatorMap (⇑φ : (a : G) → G) x = commutatorMap (⇑φ : (a : G) → G) y
rwa : HMul.hMul (α := G) (β := G) ((φ : (a : G) → G) x⁻¹ : G) ((φ : (a : G) → G) y : G) = x⁻¹ * y
rwa₁ : HMul.hMul (α := G) (β := G) (((φ : (a : G) → G) x)⁻¹ : G) ((φ : (a : G) → G) y : G) = x⁻¹ * y
rwa₂ : x * HMul.hMul (α := G) (β := G) (((φ : (a : G) → G) x)⁻¹ : G) ((φ : (a : G) → G) y : G) = y
⊢ (φ : (a : G) → G) (x⁻¹ * y) = x⁻¹ * y
have rwa₃ : HMul.hMul (β := G) (HMul.hMul (β := G) x (((φ : (a : G) → G) x)⁻¹ : G)) ((φ : (a : G) → G) y : G) = y
Tactic: rwa [map_mul, map_inv, eq_inv_mul_iff_mul_eq, ← mul_assoc, ← eq_div_iff_mul_eq', ← division_def]
-- 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
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
x y : G
h : commutatorMap (⇑φ : (a : G) → G) x = commutatorMap (⇑φ : (a : G) → G) y
rwa : HMul.hMul (α := G) (β := G) ((φ : (a : G) → G) x⁻¹ : G) ((φ : (a : G) → G) y : G) = x⁻¹ * y
rwa₁ : HMul.hMul (α := G) (β := G) (((φ : (a : G) → G) x)⁻¹ : G) ((φ : (a : G) → G) y : G) = x⁻¹ * y
rwa₂ : x * HMul.hMul (α := G) (β := G) (((φ : (a : G) → G) x)⁻¹ : G) ((φ : (a : G) → G) y : G) = y
rwa₃ : HMul.hMul (β := G) (HMul.hMul (β := G) x (((φ : (a : G) → G) x)⁻¹ : G)) ((φ : (a : G) → G) y : G) = y
⊢ (φ : (a : G) → G) (x⁻¹ * y) = x⁻¹ * y
have rwa₄ : HMul.hMul (β := G) x (((φ : (a : G) → G) x)⁻¹ : G) = HDiv.hDiv (β := G) y ((φ : (a : G) → G) y : G)
Tactic: rwa [map_mul, map_inv, eq_inv_mul_iff_mul_eq, ← mul_assoc, ← eq_div_iff_mul_eq', ← division_def]
-- 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
hφ : FixedPointFree.{u_2} (G := G) (⇑φ : (a : G) → G)
x y : G
h : commutatorMap (⇑φ : (a : G) → G) x = commutatorMap (⇑φ : (a : G) → G) y
rwa : HMul.hMul (α := G) (β := G) ((φ : (a : G) → G) x⁻¹ : G) ((φ : (a : G) → G) y : G) = x⁻¹ * y
rwa₁ : HMul.hMul (α := G) (β := G) (((φ : (a : G) → G) x)⁻¹ : G) ((φ : (a : G) → G) y : G) = x⁻¹ * y
rwa₂ : x * HMul.hMul (α := G) (β := G) (((φ : (a : G) → G) x)⁻¹ : G) ((φ : (a : G) → G) y : G) = y
rwa₃ : HMul.hMul (β := G) (HMul.hMul (β := G) x (((φ : (a : G) → G) x)⁻¹ : G)) ((φ : (a : G) → G) y : G) = y
rwa₄ : HMul.hMul (β := G) x (((φ : (a : G) → G) x)⁻¹ : G) = HDiv.hDiv (β := G) y ((φ : (a : G) → G) y : G)
⊢ (φ : (a : G) → G) (x⁻¹ * y) = x⁻¹ * y
have rwa₅ : HDiv.hDiv (β := G) x ((φ : (a : G) → G) x : G) = HDiv.hDiv (β := G) y ((φ : (a : G) → G) y : G)
Tactic: rwa [map_mul, map_inv, eq_inv_mul_iff_mul_eq, ← mul_assoc, ← eq_div_iff_mul_eq', ← division_def]
-- 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)
n : ℕ
hn : Eq.{u_2 + 1} (α := G → G) (⇑φ : (a : G) → G)^[n] _root_.id
g : G
⊢ Eq.{u_2 + 1} (α := G) (List.prod (List.map (fun (k : ℕ) ↦ (⇑φ : (a : G) → G)^[k] g) (List.range n))) 1
have obtain : ∀ (g : G),
  Eq.{u_2 + 1} (α := G)
    (List.prod (List.map (fun (k : ℕ) ↦ (⇑φ : (a : G) → G)^[k] (commutatorMap (⇑φ : (a : G) → G) g)) (List.range n))) 1
Tactic: obtain ⟨g, rfl⟩ := commutatorMap_surjective hφ g
Cleared hypotheses: 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)
n : ℕ
hn : Eq.{u_2 + 1} (α := G → G) (⇑φ : (a : G) → G)^[n] _root_.id
g : G
⊢ Eq.{u_2 + 1} (α := G)
    (List.prod (List.map (fun (k : ℕ) ↦ (⇑φ : (a : G) → G)^[k] (commutatorMap (⇑φ : (a : G) → G) g)) (List.range n))) 1
have simp : Eq.{u_2 + 1} (α := G)
  (List.prod (List.map (fun (k : ℕ) ↦ (⇑φ : (a : G) → G)^[k] g / (⇑φ : (a : G) → G)^[k.succ] g) (List.range n))) 1
Tactic: simp only [commutatorMap_apply, iterate_map_div, ← Function.iterate_succ_apply]
-- 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)
n : ℕ
hn : Eq.{u_2 + 1} (α := G → G) (⇑φ : (a : G) → G)^[n] _root_.id
g : G
⊢ Eq.{u_2 + 1} (α := G)
    (List.prod (List.map (fun (k : ℕ) ↦ (⇑φ : (a : G) → G)^[k] g / (⇑φ : (a : G) → G)^[k.succ] g) (List.range n))) 1
have rw : (⇑φ : (a : G) → G)^[0] g / (⇑φ : (a : G) → G)^[n] g = 1
Tactic: rw [List.prod_range_div', Function.iterate_zero_apply, hn, Function.id_def, div_self']
-- 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)
n : ℕ
hn : Eq.{u_2 + 1} (α := G → G) (⇑φ : (a : G) → G)^[n] _root_.id
g : G
rw : (⇑φ : (a : G) → G)^[0] g / (⇑φ : (a : G) → G)^[n] g = 1
⊢ Eq.{u_2 + 1} (α := G)
    (List.prod (List.map (fun (k : ℕ) ↦ (⇑φ : (a : G) → G)^[k] g / (⇑φ : (a : G) → G)^[k.succ] g) (List.range n))) 1
have rw₁ : g / (⇑φ : (a : G) → G)^[n] g = 1
Tactic: rw [List.prod_range_div', Function.iterate_zero_apply, hn, Function.id_def, div_self']
-- 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)
n : ℕ
hn : Eq.{u_2 + 1} (α := G → G) (⇑φ : (a : G) → G)^[n] _root_.id
g : G
rw : (⇑φ : (a : G) → G)^[0] g / (⇑φ : (a : G) → G)^[n] g = 1
rw₁ : g / (⇑φ : (a : G) → G)^[n] g = 1
⊢ Eq.{u_2 + 1} (α := G)
    (List.prod (List.map (fun (k : ℕ) ↦ (⇑φ : (a : G) → G)^[k] g / (⇑φ : (a : G) → G)^[k.succ] g) (List.range n))) 1
have rw₂ : g / _root_.id g = 1
Tactic: rw [List.prod_range_div', Function.iterate_zero_apply, hn, Function.id_def, div_self']
-- 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)
n : ℕ
hn : Eq.{u_2 + 1} (α := G → G) (⇑φ : (a : G) → G)^[n] _root_.id
g : G
rw : (⇑φ : (a : G) → G)^[0] g / (⇑φ : (a : G) → G)^[n] g = 1
rw₁ : g / (⇑φ : (a : G) → G)^[n] g = 1
rw₂ : g / _root_.id g = 1
⊢ Eq.{u_2 + 1} (α := G)
    (List.prod (List.map (fun (k : ℕ) ↦ (⇑φ : (a : G) → G)^[k] g / (⇑φ : (a : G) → G)^[k.succ] g) (List.range n))) 1
have rw₃ : g / (fun (x : G) ↦ x) g = 1
Tactic: rw [List.prod_range_div', Function.iterate_zero_apply, hn, Function.id_def, div_self']
-- 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)
n : ℕ
hn : Eq.{u_2 + 1} (α := G → G) (⇑φ : (a : G) → G)^[n] _root_.id
g : G
rw : (⇑φ : (a : G) → G)^[0] g / (⇑φ : (a : G) → G)^[n] g = 1
rw₁ : g / (⇑φ : (a : G) → G)^[n] g = 1
rw₂ : g / _root_.id g = 1
rw₃ : g / (fun (x : G) ↦ x) g = 1
⊢ Eq.{u_2 + 1} (α := G)
    (List.prod (List.map (fun (k : ℕ) ↦ (⇑φ : (a : G) → G)^[k] g / (⇑φ : (a : G) → G)^[k.succ] g) (List.range n))) 1
have rw₄ : Eq.{u_2 + 1} (α := G) 1 1
Tactic: rw [List.prod_range_div', Function.iterate_zero_apply, hn, Function.id_def, div_self']
-- 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
⊢ Eq.{u_2 + 1} (α := (a : G) → G) (⇑φ : (a : G) → G) fun (x : G) ↦ x⁻¹
have h : ∀ (g : G), (φ : (a : G) → G) g = g⁻¹
Tactic: ext g
-- 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 : Eq.{u_2 + 1} (α := G → G) (⇑φ : (a : G) → G)^[2] _root_.id
g : G
⊢ (φ : (a : G) → G) g = g⁻¹
have key : HMul.hMul (β := G) g ((φ : (a : G) → G) g : G) = 1
Tactic: have key : g * φ g = 1 := by simpa [List.range_succ] using hφ.prod_pow_eq_one h2 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 : 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
⊢ (φ : (a : G) → G) g = g⁻¹
have h : ∀ (key : g⁻¹ = (φ : (a : G) → G) g), (φ : (a : G) → G) g = g⁻¹
Tactic: rwa [← inv_eq_iff_mul_eq_one, eq_comm] at key
Cleared hypotheses: key