awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Order (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁_1 b₁_1 : α
a₂_1 b₂_1 : ↥s
a b : Localization s
a₁ b₁ : α
a₂ b₂ : ↥s
c₁ d₁ : α
c₂ d₂ : ↥s
hab : (r s : (a : α × ↥s) → α × ↥s → Prop) (a₁, a₂) (b₁, b₂)
hcd : (r s : (a : α × ↥s) → α × ↥s → Prop) (c₁, c₂) (d₁, d₂)
e f : ↥s
he : (↑b₂ : α) * a₁ = (↑a₂ : α) * b₁
hf : (↑d₂ : α) * c₁ = (↑c₂ : α) * d₁
rw : (↑c₂ : α) * a₁ * d₁ < (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
a₃ : α
rw₁ : (↑c₂ : α) * d₁ * a₁ < (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
c : α
rw₂ : (↑d₂ : α) * c₁ * a₁ < (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
rw₃ : (↑d₂ : α) * a₁ * c₁ < (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
rw₄ : (↑d₂ : α) * a₁ * c₁ < (↑a₂ : α) * d₁ * c₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
rw₅ : (↑d₂ : α) * a₁ < (↑a₂ : α) * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
rw₆ : (↑b₂ : α) * ((↑d₂ : α) * a₁) < (↑b₂ : α) * ((↑a₂ : α) * d₁) ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
a₄ : α
rw₇ : (↑d₂ : α) * ((↑b₂ : α) * a₁) < (↑b₂ : α) * ((↑a₂ : α) * d₁) ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
a₅ : α
rw₈ : (↑d₂ : α) * ((↑a₂ : α) * b₁) < (↑b₂ : α) * ((↑a₂ : α) * d₁) ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
rw₉ : (↑a₂ : α) * ((↑d₂ : α) * b₁) < (↑b₂ : α) * ((↑a₂ : α) * d₁) ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
⊢ (↑c₂ : α) * a₁ < (↑a₂ : α) * c₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
have rw₁₀ : (↑a₂ : α) * ((↑d₂ : α) * b₁) < (↑a₂ : α) * ((↑b₂ : α) * d₁) ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
Tactic: rw [← mul_lt_mul_iff_right, mul_right_comm, ← hf, mul_right_comm, mul_right_comm (a₂ : α),
          mul_lt_mul_iff_right, ← mul_lt_mul_iff_left, mul_left_comm, he, mul_left_comm,
          mul_left_comm (b₂ : α), mul_lt_mul_iff_left]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Order (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁_1 b₁_1 : α
a₂_1 b₂_1 : ↥s
a b : Localization s
a₁ b₁ : α
a₂ b₂ : ↥s
c₁ d₁ : α
c₂ d₂ : ↥s
hab : (r s : (a : α × ↥s) → α × ↥s → Prop) (a₁, a₂) (b₁, b₂)
hcd : (r s : (a : α × ↥s) → α × ↥s → Prop) (c₁, c₂) (d₁, d₂)
e f : ↥s
he : (↑b₂ : α) * a₁ = (↑a₂ : α) * b₁
hf : (↑d₂ : α) * c₁ = (↑c₂ : α) * d₁
rw : (↑c₂ : α) * a₁ * d₁ < (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
a₃ : α
rw₁ : (↑c₂ : α) * d₁ * a₁ < (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
c : α
rw₂ : (↑d₂ : α) * c₁ * a₁ < (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
rw₃ : (↑d₂ : α) * a₁ * c₁ < (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
rw₄ : (↑d₂ : α) * a₁ * c₁ < (↑a₂ : α) * d₁ * c₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
rw₅ : (↑d₂ : α) * a₁ < (↑a₂ : α) * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
rw₆ : (↑b₂ : α) * ((↑d₂ : α) * a₁) < (↑b₂ : α) * ((↑a₂ : α) * d₁) ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
a₄ : α
rw₇ : (↑d₂ : α) * ((↑b₂ : α) * a₁) < (↑b₂ : α) * ((↑a₂ : α) * d₁) ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
a₅ : α
rw₈ : (↑d₂ : α) * ((↑a₂ : α) * b₁) < (↑b₂ : α) * ((↑a₂ : α) * d₁) ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
rw₉ : (↑a₂ : α) * ((↑d₂ : α) * b₁) < (↑b₂ : α) * ((↑a₂ : α) * d₁) ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
rw₁₀ : (↑a₂ : α) * ((↑d₂ : α) * b₁) < (↑a₂ : α) * ((↑b₂ : α) * d₁) ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
⊢ (↑c₂ : α) * a₁ < (↑a₂ : α) * c₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
have rw₁₁ : (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
Tactic: rw [← mul_lt_mul_iff_right, mul_right_comm, ← hf, mul_right_comm, mul_right_comm (a₂ : α),
          mul_lt_mul_iff_right, ← mul_lt_mul_iff_left, mul_left_comm, he, mul_left_comm,
          mul_left_comm (b₂ : α), mul_lt_mul_iff_left]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Order (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a_1 b_1 c_1 : Localization s
a b c : α × ↥s
hab : mk a.1 a.2 ≤ mk b.1 b.2
hbc : mk b.1 b.2 ≤ mk c.1 c.2
⊢ mk a.1 a.2 ≤ mk c.1 c.2
have simp : ∀ (hab : (↑b.2 : α) * a.1 ≤ (↑a.2 : α) * b.1) (hbc : (↑c.2 : α) * b.1 ≤ (↑b.2 : α) * c.1),
  (↑c.2 : α) * a.1 ≤ (↑a.2 : α) * c.1
Tactic: simp only [mk_le_mk] at hab hbc ⊢
Cleared hypotheses: hab, hbc
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Order (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a_1 b_1 c_1 : Localization s
a b c : α × ↥s
hab : (↑b.2 : α) * a.1 ≤ (↑a.2 : α) * b.1
hbc : (↑c.2 : α) * b.1 ≤ (↑b.2 : α) * c.1
apply : α
⊢ (↑c.2 : α) * a.1 ≤ (↑a.2 : α) * c.1
have apply₁ : (↑b.2 : α) * ((↑c.2 : α) * a.1) ≤ (↑b.2 : α) * ((↑a.2 : α) * c.1)
Tactic: apply le_of_mul_le_mul_left' _
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Order (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a_1 b_1 c_1 : Localization s
a b c : α × ↥s
hab : (↑b.2 : α) * a.1 ≤ (↑a.2 : α) * b.1
hbc : (↑c.2 : α) * b.1 ≤ (↑b.2 : α) * c.1
⊢ (↑b.2 : α) * ((↑c.2 : α) * a.1) ≤ (↑b.2 : α) * ((↑a.2 : α) * c.1)
have grw : (↑c.2 : α) * ((↑a.2 : α) * b.1) ≤ (↑b.2 : α) * ((↑a.2 : α) * c.1)
Tactic: grw [mul_left_comm, hab]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Order (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a_1 b_1 c_1 : Localization s
a b c : α × ↥s
hab : (↑b.2 : α) * a.1 ≤ (↑a.2 : α) * b.1
hbc : (↑c.2 : α) * b.1 ≤ (↑b.2 : α) * c.1
⊢ (↑c.2 : α) * ((↑a.2 : α) * b.1) ≤ (↑b.2 : α) * ((↑a.2 : α) * c.1)
have rwa : (↑a.2 : α) * ((↑c.2 : α) * b.1) ≤ (↑b.2 : α) * ((↑a.2 : α) * c.1)
Tactic: rwa [mul_left_comm, mul_left_comm (b.2 : α), mul_le_mul_iff_left]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Order (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a_1 b_1 c_1 : Localization s
a b c : α × ↥s
hab : (↑b.2 : α) * a.1 ≤ (↑a.2 : α) * b.1
hbc : (↑c.2 : α) * b.1 ≤ (↑b.2 : α) * c.1
rwa : (↑a.2 : α) * ((↑c.2 : α) * b.1) ≤ (↑b.2 : α) * ((↑a.2 : α) * c.1)
⊢ (↑c.2 : α) * ((↑a.2 : α) * b.1) ≤ (↑b.2 : α) * ((↑a.2 : α) * c.1)
have rwa₁ : (↑a.2 : α) * ((↑c.2 : α) * b.1) ≤ (↑a.2 : α) * ((↑b.2 : α) * c.1)
Tactic: rwa [mul_left_comm, mul_left_comm (b.2 : α), mul_le_mul_iff_left]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Order (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a b : Localization s
⊢ a ≤ b → b ≤ a → a = b
have f : ∀ (a : α) (b_1 : ↥s), mk a b_1 ≤ b → b ≤ mk a b_1 → mk a b_1 = b
Tactic: induction a using Localization.rec
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Order (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a b : Localization s
f : ∀ (a : α) (b_1 : ↥s), mk a b_1 ≤ b → b ≤ mk a b_1 → mk a b_1 = b
⊢ a ≤ b → b ≤ a → a = b
have H : ∀ {a c : α} {b_1 d : ↥s} (h : (r s : (a : α × ↥s) → α × ↥s → Prop) (a, b_1) (c, d)),
  Eq (α := mk c d ≤ b → b ≤ mk c d → mk c d = b) sorry sorry
Tactic: induction a using Localization.rec
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Order (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
b : Localization s
a : α
b_1 : ↥s
⊢ mk a b_1 ≤ b → b ≤ mk a b_1 → mk a b_1 = b
have f : ∀ (a_1 : α) (b : ↥s), mk a b_1 ≤ mk a_1 b → mk a_1 b ≤ mk a b_1 → mk a b_1 = mk a_1 b
Tactic: induction b using Localization.rec
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Order (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
b : Localization s
a : α
b_1 : ↥s
f : ∀ (a_1 : α) (b : ↥s), mk a b_1 ≤ mk a_1 b → mk a_1 b ≤ mk a b_1 → mk a b_1 = mk a_1 b
⊢ mk a b_1 ≤ b → b ≤ mk a b_1 → mk a b_1 = b
have f₁ : ∀ {a_1 c : α} {b d : ↥s} (h : (r s : (a : α × ↥s) → α × ↥s → Prop) (a_1, b) (c, d)),
  Eq (α := mk a b_1 ≤ mk c d → mk c d ≤ mk a b_1 → mk a b_1 = mk c d) sorry sorry
Tactic: induction b using Localization.rec
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Order (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a : α
b : ↥s
a_1 : α
b_1 : ↥s
⊢ mk a b ≤ mk a_1 b_1 → mk a_1 b_1 ≤ mk a b → mk a b = mk a_1 b_1
have f : (↑b_1 : α) * a ≤ (↑b : α) * a_1 →
  (↑b : α) * a_1 ≤ (↑b_1 : α) * a → ∃ (c : ↥s), (↑c : α) * ((↑b_1 : α) * a) = (↑c : α) * ((↑b : α) * a_1)
Tactic: simp_rw [mk_le_mk, mk_eq_mk_iff, r_iff_exists]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Order (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a : α
b : ↥s
a_1 : α
b_1 : ↥s
hab : (↑b_1 : α) * a ≤ (↑b : α) * a_1
hba : (↑b : α) * a_1 ≤ (↑b_1 : α) * a
⊢ (↑1 : α) * ((↑b_1 : α) * a) = (↑1 : α) * ((↑b : α) * a_1)
have rw : (↑1 : α) * ((↑b : α) * a_1) = (↑1 : α) * ((↑b : α) * a_1)
Tactic: rw [hab.antisymm hba]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Order (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
b : Localization s
a : α
b_1 : ↥s
⊢ mk a b_1 ≤ b → b ≤ mk a b_1 → mk a b_1 = b
have f : ∀ {a_1 c : α} {b d : ↥s} (h : (r s : (a : α × ↥s) → α × ↥s → Prop) (a_1, b) (c, d)),
  Eq (α := mk a b_1 ≤ mk c d → mk c d ≤ mk a b_1 → mk a b_1 = mk c d) sorry sorry
Tactic: on_goal 1 =>
      induction b using Localization.rec
      · simp_rw [mk_le_mk, mk_eq_mk_iff, r_iff_exists]
        exact fun hab hba => ⟨1, by rw [hab.antisymm hba]⟩
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Order (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a_1 b_1 : Localization s
a b : α × ↥s
hab : mk a.1 a.2 ≤ mk b.1 b.2
c_1 : Localization s
c : α × ↥s
⊢ mk a.1 a.2 * mk c.1 c.2 ≤ mk b.1 b.2 * mk c.1 c.2
have simp : ∀ (hab : (↑b.2 : α) * a.1 ≤ (↑a.2 : α) * b.1),
  (↑b.2 : α) * a.1 * ((↑c.2 : α) * c.1) ≤ (↑a.2 : α) * b.1 * ((↑c.2 : α) * c.1)
Tactic: simp only [mk_mul, mk_le_mk, Submonoid.coe_mul, mul_mul_mul_comm _ (c.2 : α)] at hab ⊢
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Order (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a_1 b_1 c_1 : Localization s
a b c : α × ↥s
hab : mk a.1 a.2 * mk b.1 b.2 ≤ mk a.1 a.2 * mk c.1 c.2
⊢ mk b.1 b.2 ≤ mk c.1 c.2
have simp : ∀ (hab : (↑a.2 : α) * a.1 * ((↑c.2 : α) * b.1) ≤ (↑a.2 : α) * a.1 * ((↑b.2 : α) * c.1)),
  (↑c.2 : α) * b.1 ≤ (↑b.2 : α) * c.1
Tactic: simp only [mk_mul, mk_le_mk, Submonoid.coe_mul, mul_mul_mul_comm _ _ a.1] at hab ⊢
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Order (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a b : Localization s
x x_1 : α × ↥s
⊢ mk x.1 x.2 ≤ mk x_1.1 x_1.2 ∨ mk x_1.1 x_1.2 ≤ mk x.1 x.2
have simp_rw : (↑x_1.2 : α) * x.1 ≤ (↑x.2 : α) * x_1.1 ∨ (↑x.2 : α) * x_1.1 ≤ (↑x_1.2 : α) * x.1
Tactic: simp_rw [mk_le_mk]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
a b : G
ha : Membership.mem (γ := Set G) {x : G | ∀ (y : G), ⁅x, y⁆ ∈ H} a
hb : Membership.mem (γ := Set G) {x : G | ∀ (y : G), ⁅x, y⁆ ∈ H} b
y : G
⊢ ⁅a * b, y⁆ ∈ H
have h : ⁅a * b, y⁆ = ⁅a, b * y * b⁻¹⁆ * ⁅b, y⁆
Tactic: convert! Subgroup.mul_mem _ (ha (b * y * b⁻¹)) (hb y) using 1
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (hypothesis)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
x : G
hx : Membership.mem (γ := Set G) {x : G | ∀ (y : G), ⁅x, y⁆ ∈ H} x
y : G
⊢ ⁅x⁻¹, y⁆ ∈ H
have hx₁ : ⁅x, y⁻¹⁆ ∈ H
Tactic: specialize hx y⁻¹
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
x y : G
hx : ⁅x, y⁻¹⁆ ∈ H
⊢ ⁅x⁻¹, y⁆ ∈ H
have rw : ∀ (hx : x * y⁻¹ * (x⁻¹ * y) ∈ H), x⁻¹ * y * (x * y⁻¹) ∈ H
Tactic: rw [commutatorElement_def, mul_assoc, inv_inv] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
⊢ H.upperCentralSeriesStep = comap (mk' H) (center (G ⧸ H))
have h : ∀ (x : G), x ∈ H.upperCentralSeriesStep ↔ x ∈ comap (mk' H) (center (G ⧸ H))
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
x : G
⊢ x ∈ H.upperCentralSeriesStep ↔ x ∈ comap (mk' H) (center (G ⧸ H))
have h : x ∈ H.upperCentralSeriesStep ↔
  ∀ (x_1 : G),
    HMul.hMul (α := G ⧸ H) (β := G ⧸ H) (↑x_1 : G ⧸ H) ((mk' H : (a : G) → G ⧸ H) x : G ⧸ H) =
      HMul.hMul (α := G ⧸ H) (β := G ⧸ H) ((mk' H : (a : G) → G ⧸ H) x : G ⧸ H) (↑x_1 : G ⧸ H)
Tactic: rw [mem_comap, mem_center_iff, forall_mk]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
x : G
⊢ x ∈ H.upperCentralSeriesStep ↔
    ∀ (x_1 : G),
      HMul.hMul (α := G ⧸ H) (β := G ⧸ H) (↑x_1 : G ⧸ H) ((mk' H : (a : G) → G ⧸ H) x : G ⧸ H) =
        HMul.hMul (α := G ⧸ H) (β := G ⧸ H) ((mk' H : (a : G) → G ⧸ H) x : G ⧸ H) (↑x_1 : G ⧸ H)
have h : ∀ (y : G),
  ⁅x, y⁆ ∈ H ↔
    HMul.hMul (α := G ⧸ H) (β := G ⧸ H) (↑y : G ⧸ H) ((mk' H : (a : G) → G ⧸ H) x : G ⧸ H) =
      HMul.hMul (α := G ⧸ H) (β := G ⧸ H) ((mk' H : (a : G) → G ⧸ H) x : G ⧸ H) (↑y : G ⧸ H)
Tactic: refine forall_congr' fun y => ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
x y : G
⊢ ⁅x, y⁆ ∈ H ↔
    HMul.hMul (α := G ⧸ H) (β := G ⧸ H) (↑y : G ⧸ H) ((mk' H : (a : G) → G ⧸ H) x : G ⧸ H) =
      HMul.hMul (α := G ⧸ H) (β := G ⧸ H) ((mk' H : (a : G) → G ⧸ H) x : G ⧸ H) (↑y : G ⧸ H)
have h : x * y * x⁻¹ * y⁻¹ ∈ H ↔ x * y * (x⁻¹ * y⁻¹) ∈ H
Tactic: rw [coe_mk', ← QuotientGroup.mk_mul, ← QuotientGroup.mk_mul, eq_comm, eq_iff_div_mem,
    div_eq_mul_inv, mul_inv_rev, commutatorElement_def]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
⊢ Eq (α := Subgroup G) (upperCentralSeries G 1) (center G)
have h : ∀ (x : G), Membership.mem (γ := Subgroup G) (upperCentralSeries G 1) x ↔ Membership.mem (γ := Subgroup G) (center G) x
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
x : G
⊢ Membership.mem (γ := Subgroup G) (upperCentralSeries G 1) x ↔ Membership.mem (γ := Subgroup G) (center G) x
have h : (∀ (y : G), ⁅x, y⁆ = 1) ↔ ∀ (g : G), g * x = x * g
Tactic: simp only [upperCentralSeries, upperCentralSeriesAux, upperCentralSeriesStep, mem_bot, mem_mk,
    Submonoid.mem_mk, Subsemigroup.mem_mk, Set.mem_setOf_eq, mem_center_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
x y : G
⊢ ⁅x, y⁆ = 1 ↔ y * x = x * y
have rw : x * y * x⁻¹ * y⁻¹ = 1 ↔ y * x = x * y
Tactic: rw [commutatorElement_def, mul_inv_eq_one, mul_inv_eq_iff_eq_mul, eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
x y : G
rw : x * y * x⁻¹ * y⁻¹ = 1 ↔ y * x = x * y
⊢ ⁅x, y⁆ = 1 ↔ y * x = x * y
have rw₁ : x * y * x⁻¹ = y ↔ y * x = x * y
Tactic: rw [commutatorElement_def, mul_inv_eq_one, mul_inv_eq_iff_eq_mul, eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
x y : G
rw : x * y * x⁻¹ * y⁻¹ = 1 ↔ y * x = x * y
rw₁ : x * y * x⁻¹ = y ↔ y * x = x * y
⊢ ⁅x, y⁆ = 1 ↔ y * x = x * y
have rw₂ : x * y = y * x ↔ y * x = x * y
Tactic: rw [commutatorElement_def, mul_inv_eq_one, mul_inv_eq_iff_eq_mul, eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
x y : G
rw : x * y * x⁻¹ * y⁻¹ = 1 ↔ y * x = x * y
rw₁ : x * y * x⁻¹ = y ↔ y * x = x * y
rw₂ : x * y = y * x ↔ y * x = x * y
⊢ ⁅x, y⁆ = 1 ↔ y * x = x * y
have rw₃ : y * x = x * y ↔ y * x = x * y
Tactic: rw [commutatorElement_def, mul_inv_eq_one, mul_inv_eq_iff_eq_mul, eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_2
inst : AddGroup G
⊢ Eq (α := AddSubgroup G) (AddSubgroup.upperCentralSeries G 1) (AddSubgroup.center G)
have h : ∀ (x : G),
  Membership.mem (γ := AddSubgroup G) (AddSubgroup.upperCentralSeries G 1) x ↔
    Membership.mem (γ := AddSubgroup G) (AddSubgroup.center G) x
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_2
inst : AddGroup G
x : G
⊢ Membership.mem (γ := AddSubgroup G) (AddSubgroup.upperCentralSeries G 1) x ↔
    Membership.mem (γ := AddSubgroup G) (AddSubgroup.center G) x
have h : (∀ (y : G), ⁅x, y⁆ = 0) ↔ ∀ (g : G), g + x = x + g
Tactic: simp only [AddSubgroup.upperCentralSeries, AddSubgroup.upperCentralSeriesAux,
    AddSubgroup.upperCentralSeriesStep, AddSubgroup.mem_bot, AddSubgroup.mem_mk,
    AddSubmonoid.mem_mk, AddSubsemigroup.mem_mk, Set.mem_setOf_eq, AddSubgroup.mem_center_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_2
inst : AddGroup G
x y : G
⊢ ⁅x, y⁆ = 0 ↔ y + x = x + y
have rw : x + y + -x + -y = 0 ↔ y + x = x + y
Tactic: rw [addCommutatorElement_def, add_neg_eq_zero, add_neg_eq_iff_eq_add, eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_2
inst : AddGroup G
x y : G
rw : x + y + -x + -y = 0 ↔ y + x = x + y
⊢ ⁅x, y⁆ = 0 ↔ y + x = x + y
have rw₁ : x + y + -x = y ↔ y + x = x + y
Tactic: rw [addCommutatorElement_def, add_neg_eq_zero, add_neg_eq_iff_eq_add, eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_2
inst : AddGroup G
x y : G
rw : x + y + -x + -y = 0 ↔ y + x = x + y
rw₁ : x + y + -x = y ↔ y + x = x + y
⊢ ⁅x, y⁆ = 0 ↔ y + x = x + y
have rw₂ : x + y = y + x ↔ y + x = x + y
Tactic: rw [addCommutatorElement_def, add_neg_eq_zero, add_neg_eq_iff_eq_add, eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_2
inst : AddGroup G
x y : G
rw : x + y + -x + -y = 0 ↔ y + x = x + y
rw₁ : x + y + -x = y ↔ y + x = x + y
rw₂ : x + y = y + x ↔ y + x = x + y
⊢ ⁅x, y⁆ = 0 ↔ y + x = x + y
have rw₃ : y + x = x + y ↔ y + x = x + y
Tactic: rw [addCommutatorElement_def, add_neg_eq_zero, add_neg_eq_iff_eq_add, eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
e : H ≃* G
n : ℕ
⊢ Eq (α := Subgroup H) (comap (↑e : H →* G) (upperCentralSeries G (n + 1))) (upperCentralSeries H (n + 1))
have h : ∀ (x : H),
  Membership.mem (γ := Subgroup H) (comap (↑e : H →* G) (upperCentralSeries G (n + 1))) x ↔
    Membership.mem (γ := Subgroup H) (upperCentralSeries H (n + 1)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
e : G ≃* H
⊢ IsNilpotent G ↔ IsNilpotent H
have simp_rw : (∃ (n : ℕ), Eq (α := Subgroup G) (upperCentralSeries G n) ⊤) ↔
  ∃ (n : ℕ), Eq (α := Subgroup H) (upperCentralSeries H n) ⊤
Tactic: simp_rw [isNilpotent_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
e : G ≃* H
⊢ (∃ (n : ℕ), Eq (α := Subgroup G) (upperCentralSeries G n) ⊤) ↔
    ∃ (n : ℕ), Eq (α := Subgroup H) (upperCentralSeries H n) ⊤
have refine_1 : ∀ (n : ℕ) (h : Eq (α := Subgroup G) (upperCentralSeries G n) ⊤), Eq (α := Subgroup H) (upperCentralSeries H n) ⊤
Tactic: refine exists_congr fun n ↦ ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
e : G ≃* H
refine_1 :
  ∀ (n : ℕ) (h : Eq (α := Subgroup G) (upperCentralSeries G n) ⊤), Eq (α := Subgroup H) (upperCentralSeries H n) ⊤
⊢ (∃ (n : ℕ), Eq (α := Subgroup G) (upperCentralSeries G n) ⊤) ↔
    ∃ (n : ℕ), Eq (α := Subgroup H) (upperCentralSeries H n) ⊤
have refine_2 : ∀ (n : ℕ) (h : Eq (α := Subgroup H) (upperCentralSeries H n) ⊤), Eq (α := Subgroup G) (upperCentralSeries G n) ⊤
Tactic: refine exists_congr fun n ↦ ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
n : ℕ
x : G
hx : x ∈ H (n + 1)
⊢ Membership.mem (γ := Subgroup G) (upperCentralSeries G (n + 1)) x
have rw : ∀ (y : G), Membership.mem (γ := Subgroup G) (upperCentralSeries G n) ⁅x, y⁆
Tactic: rw [mem_upperCentralSeries_succ_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
⊢ Monotone (β := Subgroup G) (upperCentralSeries G)
have refine : ∀ (n : ℕ), LE.le (α := Subgroup G) (upperCentralSeries G n) (upperCentralSeries G (n + 1))
Tactic: refine monotone_nat_of_le_succ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
n : ℕ
x : G
hx : Membership.mem (γ := Subgroup G) (upperCentralSeries G n) x
y : G
⊢ Membership.mem (γ := Subgroup G)
    (PSigma.fst (β := fun (H : Subgroup G) ↦ H.Characteristic) (upperCentralSeriesAux G n)) ⁅x, y⁆
have rw : Membership.mem (γ := Subgroup G) (PSigma.fst (β := fun (H : Subgroup G) ↦ H.Characteristic) (upperCentralSeriesAux G n))
  (x * (y * x⁻¹ * y⁻¹))
Tactic: rw [commutatorElement_def, mul_assoc, mul_assoc, ← mul_assoc y x⁻¹ y⁻¹]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
⊢ Group.IsNilpotent G ↔ ∃ (n : ℕ) (H : ℕ → Subgroup G), IsAscendingCentralSeries H ∧ H n = ⊤
have mp : Group.IsNilpotent G → ∃ (n : ℕ) (H : ℕ → Subgroup G), IsAscendingCentralSeries H ∧ H n = ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
mp : Group.IsNilpotent G → ∃ (n : ℕ) (H : ℕ → Subgroup G), IsAscendingCentralSeries H ∧ H n = ⊤
⊢ Group.IsNilpotent G ↔ ∃ (n : ℕ) (H : ℕ → Subgroup G), IsAscendingCentralSeries H ∧ H n = ⊤
have mpr : (∃ (n : ℕ) (H : ℕ → Subgroup G), IsAscendingCentralSeries H ∧ H n = ⊤) → Group.IsNilpotent G
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ Group.IsNilpotent G
have h : Eq (α := Subgroup G) (upperCentralSeries G n) ⊤
Tactic: use n
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (goal)
Goal:
G : Type u_1
inst : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ Eq (α := Subgroup G) (upperCentralSeries G n) ⊤
have h : H n ≤ upperCentralSeries G n
Tactic: rw [eq_top_iff, ← hn]
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (hypothesis)
Goal:
G : Type u_1
inst : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊤
hasc : IsAscendingCentralSeries H
⊢ IsDescendingCentralSeries.{u_1} (G := G) fun (m : ℕ) ↦ H (n - m)
have h0 : H 0 = ⊥
Tactic: obtain ⟨h0, hH⟩ := hasc
Cleared hypotheses: hasc
-- Lean 4 proof step from Mathlib.GroupTheory.Nilpotent (hypothesis)
Goal:
G : Type u_1
inst : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊤
hasc : IsAscendingCentralSeries H
h0 : H 0 = ⊥
⊢ IsDescendingCentralSeries.{u_1} (G := G) fun (m : ℕ) ↦ H (n - m)
have hH : ∀ (x : G) (n : ℕ), x ∈ H (n + 1) → ∀ (g : G), ⁅x, g⁆ ∈ H n
Tactic: obtain ⟨h0, hH⟩ := hasc
Cleared hypotheses: hasc