awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Center (goal)
Goal:
M : Type u_1
inst : Mul M
z : M
h : IsMulCentral z
a c : M
rw : a * z * c = a * (c * z)
rw₁ : a * z * c = a * c * z
rw₂ : z * a * c = a * c * z
rw₃ : z * (a * c) = a * c * z
⊢ a * z * c = a * (z * c)
have rw₄ : a * c * z = a * c * z
Tactic: rw [h.comm, ← h.right_assoc, ← h.comm, ← h.left_assoc, h.comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Center (goal)
Goal:
M : Type u_1
inst : Mul M
z₁ z₂ : M
hz₁ : z₁ ∈ center M
hz₂ : z₂ ∈ center M
⊢ z₁ * z₂ ∈ center M
have simp : ∀
  (hz₁ :
    (∀ (a : M), z₁ * a = a * z₁) ∧ (∀ (b c : M), z₁ * (b * c) = z₁ * b * c) ∧ ∀ (a b : M), a * b * z₁ = a * (b * z₁))
  (hz₂ :
    (∀ (a : M), z₂ * a = a * z₂) ∧ (∀ (b c : M), z₂ * (b * c) = z₂ * b * c) ∧ ∀ (a b : M), a * b * z₂ = a * (b * z₂)),
  (∀ (a : M), z₁ * z₂ * a = a * (z₁ * z₂)) ∧
    (∀ (b c : M), z₁ * z₂ * (b * c) = z₁ * z₂ * b * c) ∧ ∀ (a b : M), a * b * (z₁ * z₂) = a * (b * (z₁ * z₂))
Tactic: simp only [commute_iff_eq, mem_center_iff, isMulCentral_iff] at *
Cleared hypotheses: hz₁, hz₂
-- Lean 4 proof step from Mathlib.Algebra.Group.Center (goal)
Goal:
M : Type u_1
inst : Mul M
S : Set M
⊢ S.centralizer.centralizer.centralizer = S.centralizer
have refine : S.centralizer.centralizer.centralizer ⊆ S.centralizer
Tactic: refine Set.Subset.antisymm ?_ Set.subset_centralizer_centralizer
-- Lean 4 proof step from Mathlib.Algebra.Group.Center (goal)
Goal:
M : Type u_1
inst : Mul M
N : Type u_2
inst_1 : Mul N
S : Set M
T : Set N
hS : S.Nonempty
hT : T.Nonempty
⊢ (S ×ˢ T).centralizer = S.centralizer ×ˢ T.centralizer
have h : ∀ (x : M × N), x ∈ (S ×ˢ T).centralizer ↔ x ∈ S.centralizer ×ˢ T.centralizer
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Center (goal)
Goal:
M : Type u_1
inst : Mul M
N : Type u_2
inst_1 : Mul N
S : Set M
T : Set N
hS : S.Nonempty
hT : T.Nonempty
x : M × N
⊢ x ∈ (S ×ˢ T).centralizer ↔ x ∈ S.centralizer ×ˢ T.centralizer
have h : (∀ (a : M) (b : N), a ∈ S ∧ b ∈ T → (a * x.1, b * x.2) = (x.1 * a, x.2 * b)) ↔
  (∀ m ∈ S, m * x.1 = x.1 * m) ∧ ∀ m ∈ T, m * x.2 = x.2 * m
Tactic: simp only [mem_prod, mem_centralizer_iff, Prod.forall, Prod.mul_def]
-- Lean 4 proof step from Mathlib.Algebra.Group.Center (goal)
Goal:
ι : Type u_2
A : ι → Type u_3
inst : (i : ι) → Mul (A i)
⊢ Eq (α := Set ((i : ι) → A i)) (center ((i : ι) → A i)) (pi (α := A) univ fun (i : ι) ↦ center (A i))
have h : ∀ (x : (i : ι) → A i),
  Membership.mem (γ := Set ((i : ι) → A i)) (center ((i : ι) → A i)) x ↔
    Membership.mem (γ := Set ((i : ι) → A i)) (pi (α := A) univ fun (i : ι) ↦ center (A i)) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Group.Center (goal)
Goal:
ι : Type u_2
A : ι → Type u_3
inst : (i : ι) → Mul (A i)
x : (i : ι) → A i
⊢ Membership.mem (γ := Set ((i : ι) → A i)) (center ((i : ι) → A i)) x ↔
    Membership.mem (γ := Set ((i : ι) → A i)) (pi (α := A) univ fun (i : ι) ↦ center (A i)) x
have h : ((∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1) ∧
    (∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1) ∧
      ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)) ↔
  ∀ (i : ι),
    (∀ (a : A i), x i * a = a * x i) ∧
      (∀ (b c : A i), x i * (b * c) = x i * b * c) ∧ ∀ (a b : A i), a * b * x i = a * (b * x i)
Tactic: simp only [mem_pi, mem_center_iff, isMulCentral_iff, mem_univ, forall_true_left,
    commute_iff_eq, funext_iff, Pi.mul_def]
-- Lean 4 proof step from Mathlib.Algebra.Group.Center (goal)
Goal:
ι : Type u_2
A : ι → Type u_3
inst : (i : ι) → Mul (A i)
x : (i : ι) → A i
⊢ ((∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1) ∧
      (∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1) ∧
        ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)) ↔
    ∀ (i : ι),
      (∀ (a : A i), x i * a = a * x i) ∧
        (∀ (b c : A i), x i * (b * c) = x i * b * c) ∧ ∀ (a b : A i), a * b * x i = a * (b * x i)
have h : ((∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1) ∧
    (∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1) ∧
      ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)) →
  ∀ (i : ι) (h1 : ∀ (a : (i : ι) → A i) (x_2 : ι), x x_2 * a x_2 = a x_2 * x x_2)
    (h2 : ∀ (b c : (i : ι) → A i) (x_2 : ι), x x_2 * (b x_2 * c x_2) = x x_2 * b x_2 * c x_2)
    (h3 : ∀ (a b : (i : ι) → A i) (x_2 : ι), a x_2 * b x_2 * x x_2 = a x_2 * (b x_2 * x x_2)),
    (∀ (a : A i), x i * a = a * x i) ∧
      (∀ (b c : A i), x i * (b * c) = x i * b * c) ∧ ∀ (a b : A i), a * b * x i = a * (b * x i)
Tactic: refine ⟨fun ⟨h1, h2, h3⟩ i ↦ ?_, by grind⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Center (goal)
Goal:
ι : Type u_2
A : ι → Type u_3
inst : (i : ι) → Mul (A i)
⊢ Eq (α := Set ((i : ι) → A i)) (center ((i : ι) → A i)) (pi (α := A) univ fun (i : ι) ↦ center (A i))
have h : ∀ (x : (i : ι) → A i),
  Membership.mem (γ := Set ((i : ι) → A i)) (center ((i : ι) → A i)) x ↔
    Membership.mem (γ := Set ((i : ι) → A i)) (pi (α := A) univ fun (i : ι) ↦ center (A i)) x
Tactic: classical
  ext x
  simp only [mem_pi, mem_center_iff, isMulCentral_iff, mem_univ, forall_true_left,
    commute_iff_eq, funext_iff, Pi.mul_def]
  refine ⟨fun ⟨h1, h2, h3⟩ i ↦ ?_, by grind⟩
  exact ⟨fun a ↦ by simpa using h1 (update x i a) i,
    fun b c ↦ by simpa using h2 (update x i b) (update x i c) i,
    fun a b ↦ by simpa using h3 (update x i a) (update x i b) i⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Center (goal)
Goal:
ι : Type u_2
A : ι → Type u_3
inst : (i : ι) → Mul (A i)
h :
  ∀ (x : (i : ι) → A i),
    Membership.mem (γ := Set ((i : ι) → A i)) (center ((i : ι) → A i)) x ↔
      Membership.mem (γ := Set ((i : ι) → A i)) (pi (α := A) univ fun (i : ι) ↦ center (A i)) x
⊢ Eq (α := Set ((i : ι) → A i)) (center ((i : ι) → A i)) (pi (α := A) univ fun (i : ι) ↦ center (A i))
have h₁ : ∀ (x : (i : ι) → A i),
  ((∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1) ∧
      (∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1) ∧
        ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)) ↔
    ∀ (i : ι),
      (∀ (a : A i), x i * a = a * x i) ∧
        (∀ (b c : A i), x i * (b * c) = x i * b * c) ∧ ∀ (a b : A i), a * b * x i = a * (b * x i)
Tactic: classical
  ext x
  simp only [mem_pi, mem_center_iff, isMulCentral_iff, mem_univ, forall_true_left,
    commute_iff_eq, funext_iff, Pi.mul_def]
  refine ⟨fun ⟨h1, h2, h3⟩ i ↦ ?_, by grind⟩
  exact ⟨fun a ↦ by simpa using h1 (update x i a) i,
    fun b c ↦ by simpa using h2 (update x i b) (update x i c) i,
    fun a b ↦ by simpa using h3 (update x i a) (update x i b) i⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Center (goal)
Goal:
ι : Type u_2
A : ι → Type u_3
inst : (i : ι) → Mul (A i)
h :
  ∀ (x : (i : ι) → A i),
    Membership.mem (γ := Set ((i : ι) → A i)) (center ((i : ι) → A i)) x ↔
      Membership.mem (γ := Set ((i : ι) → A i)) (pi (α := A) univ fun (i : ι) ↦ center (A i)) x
h₁ :
  ∀ (x : (i : ι) → A i),
    ((∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1) ∧
        (∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1) ∧
          ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)) ↔
      ∀ (i : ι),
        (∀ (a : A i), x i * a = a * x i) ∧
          (∀ (b c : A i), x i * (b * c) = x i * b * c) ∧ ∀ (a b : A i), a * b * x i = a * (b * x i)
⊢ Eq (α := Set ((i : ι) → A i)) (center ((i : ι) → A i)) (pi (α := A) univ fun (i : ι) ↦ center (A i))
have h₂ : ∀ (x : (i : ι) → A i),
  ((∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1) ∧
      (∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1) ∧
        ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)) →
    ∀ (i : ι) (h1 : ∀ (a : (i : ι) → A i) (x_2 : ι), x x_2 * a x_2 = a x_2 * x x_2)
      (h2 : ∀ (b c : (i : ι) → A i) (x_2 : ι), x x_2 * (b x_2 * c x_2) = x x_2 * b x_2 * c x_2)
      (h3 : ∀ (a b : (i : ι) → A i) (x_2 : ι), a x_2 * b x_2 * x x_2 = a x_2 * (b x_2 * x x_2)),
      (∀ (a : A i), x i * a = a * x i) ∧
        (∀ (b c : A i), x i * (b * c) = x i * b * c) ∧ ∀ (a b : A i), a * b * x i = a * (b * x i)
Tactic: classical
  ext x
  simp only [mem_pi, mem_center_iff, isMulCentral_iff, mem_univ, forall_true_left,
    commute_iff_eq, funext_iff, Pi.mul_def]
  refine ⟨fun ⟨h1, h2, h3⟩ i ↦ ?_, by grind⟩
  exact ⟨fun a ↦ by simpa using h1 (update x i a) i,
    fun b c ↦ by simpa using h2 (update x i b) (update x i c) i,
    fun a b ↦ by simpa using h3 (update x i a) (update x i b) i⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Center (goal)
Goal:
M : Type u_1
inst : Semigroup M
z : M
a : z ∈ center M
g : M
⊢ g * z = z * g
have rw : g * z = g * z
Tactic: rw [IsMulCentral.comm a g]
-- Lean 4 proof step from Mathlib.Algebra.Group.Center (goal)
Goal:
M : Type u_1
S : Set M
inst : Semigroup M
a b : M
ha : a ∈ S.centralizer
hb : b ∈ S.centralizer
g : M
hg : g ∈ S
⊢ g * (a * b) = a * b * g
have rw : g * (a * b) = a * (b * g)
Tactic: rw [mul_assoc, ← hb g hg, ← mul_assoc, ha g hg, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Center (goal)
Goal:
M : Type u_1
S : Set M
inst : Semigroup M
a b : M
ha : a ∈ S.centralizer
hb : b ∈ S.centralizer
g : M
hg : g ∈ S
rw : g * (a * b) = a * (b * g)
⊢ g * (a * b) = a * b * g
have rw₁ : g * (a * b) = a * (g * b)
Tactic: rw [mul_assoc, ← hb g hg, ← mul_assoc, ha g hg, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Center (goal)
Goal:
M : Type u_1
S : Set M
inst : Semigroup M
a b : M
ha : a ∈ S.centralizer
hb : b ∈ S.centralizer
g : M
hg : g ∈ S
rw : g * (a * b) = a * (b * g)
rw₁ : g * (a * b) = a * (g * b)
⊢ g * (a * b) = a * b * g
have rw₂ : g * a * b = a * (g * b)
Tactic: rw [mul_assoc, ← hb g hg, ← mul_assoc, ha g hg, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Center (goal)
Goal:
M : Type u_1
S : Set M
inst : Semigroup M
a b : M
ha : a ∈ S.centralizer
hb : b ∈ S.centralizer
g : M
hg : g ∈ S
rw : g * (a * b) = a * (b * g)
rw₁ : g * (a * b) = a * (g * b)
rw₂ : g * a * b = a * (g * b)
⊢ g * (a * b) = a * b * g
have rw₃ : a * g * b = a * (g * b)
Tactic: rw [mul_assoc, ← hb g hg, ← mul_assoc, ha g hg, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Center (goal)
Goal:
M : Type u_1
S : Set M
inst : Semigroup M
a b : M
ha : a ∈ S.centralizer
hb : b ∈ S.centralizer
g : M
hg : g ∈ S
rw : g * (a * b) = a * (b * g)
rw₁ : g * (a * b) = a * (g * b)
rw₂ : g * a * b = a * (g * b)
rw₃ : a * g * b = a * (g * b)
⊢ g * (a * b) = a * b * g
have rw₄ : a * (g * b) = a * (g * b)
Tactic: rw [mul_assoc, ← hb g hg, ← mul_assoc, ha g hg, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Center (goal)
Goal:
M : Type u_1
S : Set M
inst : Semigroup M
h : ⊤ ≤ S.centralizer
x : M
hx : x ∈ S
x_1 : M
⊢ x_1 * x = x * x_1
have rw : x_1 * x = x_1 * x
Tactic: rw [h trivial _ hx]
-- Lean 4 proof step from Mathlib.Algebra.Group.Center (goal)
Goal:
M : Type u_1
inst : MulOneClass M
x : M
⊢ Commute 1 x
have rw : 1 * x = x * 1
Tactic: rw [commute_iff_eq, one_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Center (goal)
Goal:
M : Type u_1
inst : MulOneClass M
x : M
rw : 1 * x = x * 1
⊢ Commute 1 x
have rw₁ : x = x * 1
Tactic: rw [commute_iff_eq, one_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Center (goal)
Goal:
M : Type u_1
inst : MulOneClass M
x : M
rw : 1 * x = x * 1
rw₁ : x = x * 1
⊢ Commute 1 x
have rw₂ : x = x
Tactic: rw [commute_iff_eq, one_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Center (goal)
Goal:
M : Type u_1
inst : MulOneClass M
x x_1 : M
⊢ 1 * (x * x_1) = 1 * x * x_1
have rw : x * x_1 = 1 * x * x_1
Tactic: rw [one_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Center (goal)
Goal:
M : Type u_1
inst : MulOneClass M
x x_1 : M
rw : x * x_1 = 1 * x * x_1
⊢ 1 * (x * x_1) = 1 * x * x_1
have rw₁ : x * x_1 = x * x_1
Tactic: rw [one_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Center (goal)
Goal:
M : Type u_1
inst : MulOneClass M
x x_1 : M
⊢ x * x_1 * 1 = x * (x_1 * 1)
have rw : x * x_1 = x * (x_1 * 1)
Tactic: rw [mul_one, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Center (goal)
Goal:
M : Type u_1
inst : MulOneClass M
x x_1 : M
rw : x * x_1 = x * (x_1 * 1)
⊢ x * x_1 * 1 = x * (x_1 * 1)
have rw₁ : x * x_1 = x * x_1
Tactic: rw [mul_one, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Center (goal)
Goal:
M : Type u_1
inst : Monoid M
x : Mˣ
ha : Membership.mem (γ := Set Mˣ) (Units.val ⁻¹' center M) x
⊢ Membership.mem (γ := Set Mˣ) (center Mˣ) x
have rw : ∀ (g : Mˣ), g * x = x * g
Tactic: rw [_root_.Semigroup.mem_center_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.Center (goal)
Goal:
M : Type u_1
inst : Monoid M
x : Mˣ
ha : Membership.mem (γ := Set Mˣ) (Units.val ⁻¹' center M) x
g : Mˣ
⊢ g * x = x * g
have rw : (↑(g * x) : M) = (↑(x * g) : M)
Tactic: rw [← Units.val_inj, Units.val_mul, Units.val_mul, ha.comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Center (goal)
Goal:
M : Type u_1
inst : Monoid M
x : Mˣ
ha : Membership.mem (γ := Set Mˣ) (Units.val ⁻¹' center M) x
g : Mˣ
rw : (↑(g * x) : M) = (↑(x * g) : M)
⊢ g * x = x * g
have rw₁ : (↑g : M) * (↑x : M) = (↑(x * g) : M)
Tactic: rw [← Units.val_inj, Units.val_mul, Units.val_mul, ha.comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Center (goal)
Goal:
M : Type u_1
inst : Monoid M
x : Mˣ
ha : Membership.mem (γ := Set Mˣ) (Units.val ⁻¹' center M) x
g : Mˣ
rw : (↑(g * x) : M) = (↑(x * g) : M)
rw₁ : (↑g : M) * (↑x : M) = (↑(x * g) : M)
⊢ g * x = x * g
have rw₂ : (↑g : M) * (↑x : M) = (↑x : M) * (↑g : M)
Tactic: rw [← Units.val_inj, Units.val_mul, Units.val_mul, ha.comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Center (goal)
Goal:
M : Type u_1
inst : Monoid M
x : Mˣ
ha : Membership.mem (γ := Set Mˣ) (Units.val ⁻¹' center M) x
g : Mˣ
rw : (↑(g * x) : M) = (↑(x * g) : M)
rw₁ : (↑g : M) * (↑x : M) = (↑(x * g) : M)
rw₂ : (↑g : M) * (↑x : M) = (↑x : M) * (↑g : M)
⊢ g * x = x * g
have rw₃ : (↑g : M) * (↑x : M) = (↑g : M) * (↑x : M)
Tactic: rw [← Units.val_inj, Units.val_mul, Units.val_mul, ha.comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Center (goal)
Goal:
M : Type u_1
inst : Monoid M
a : Mˣ
ha : (↑a : M) ∈ center M
⊢ (↑a⁻¹ : M) ∈ center M
have rw : ∀ (ha : ∀ (g : M), g * (↑a : M) = (↑a : M) * g) (g : M), g * (↑a⁻¹ : M) = (↑a⁻¹ : M) * g
Tactic: rw [Semigroup.mem_center_iff] at *
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Algebra.Group.Center (goal)
Goal:
M : Type u_1
inst : Monoid M
a : M
inst_1 : Invertible a
ha : a ∈ center M
⊢ @Invertible.invOf _ MulOne.toMul MulOne.toOne a _ ∈ center M
have rw : ∀ (ha : ∀ (g : M), g * a = a * g) (g : M),
  g * @Invertible.invOf _ MulOne.toMul MulOne.toOne a _ = @Invertible.invOf _ MulOne.toMul MulOne.toOne a _ * g
Tactic: rw [Semigroup.mem_center_iff] at *
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Algebra.Group.Center (goal)
Goal:
M : Type u_1
inst : DivisionMonoid M
a : M
ha : a ∈ center M
⊢ a⁻¹ ∈ center M
have rw : ∀ (g : M), g * a⁻¹ = a⁻¹ * g
Tactic: rw [_root_.Semigroup.mem_center_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.Center (goal)
Goal:
M : Type u_1
inst : DivisionMonoid M
a : M
ha : a ∈ center M
g : M
⊢ g * a⁻¹ = a⁻¹ * g
have rw : (g * a⁻¹)⁻¹ = (a⁻¹ * g)⁻¹
Tactic: rw [← inv_inj, mul_inv_rev, inv_inv, ha.comm, mul_inv_rev, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Center (goal)
Goal:
M : Type u_1
inst : DivisionMonoid M
a : M
ha : a ∈ center M
g : M
rw : (g * a⁻¹)⁻¹ = (a⁻¹ * g)⁻¹
⊢ g * a⁻¹ = a⁻¹ * g
have rw₁ : a⁻¹⁻¹ * g⁻¹ = (a⁻¹ * g)⁻¹
Tactic: rw [← inv_inj, mul_inv_rev, inv_inv, ha.comm, mul_inv_rev, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Center (goal)
Goal:
M : Type u_1
inst : DivisionMonoid M
a : M
ha : a ∈ center M
g : M
rw : (g * a⁻¹)⁻¹ = (a⁻¹ * g)⁻¹
rw₁ : a⁻¹⁻¹ * g⁻¹ = (a⁻¹ * g)⁻¹
⊢ g * a⁻¹ = a⁻¹ * g
have rw₂ : a * g⁻¹ = (a⁻¹ * g)⁻¹
Tactic: rw [← inv_inj, mul_inv_rev, inv_inv, ha.comm, mul_inv_rev, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Center (goal)
Goal:
M : Type u_1
inst : DivisionMonoid M
a : M
ha : a ∈ center M
g : M
rw : (g * a⁻¹)⁻¹ = (a⁻¹ * g)⁻¹
rw₁ : a⁻¹⁻¹ * g⁻¹ = (a⁻¹ * g)⁻¹
rw₂ : a * g⁻¹ = (a⁻¹ * g)⁻¹
⊢ g * a⁻¹ = a⁻¹ * g
have rw₃ : g⁻¹ * a = (a⁻¹ * g)⁻¹
Tactic: rw [← inv_inj, mul_inv_rev, inv_inv, ha.comm, mul_inv_rev, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Center (goal)
Goal:
M : Type u_1
inst : DivisionMonoid M
a : M
ha : a ∈ center M
g : M
rw : (g * a⁻¹)⁻¹ = (a⁻¹ * g)⁻¹
rw₁ : a⁻¹⁻¹ * g⁻¹ = (a⁻¹ * g)⁻¹
rw₂ : a * g⁻¹ = (a⁻¹ * g)⁻¹
rw₃ : g⁻¹ * a = (a⁻¹ * g)⁻¹
⊢ g * a⁻¹ = a⁻¹ * g
have rw₄ : g⁻¹ * a = g⁻¹ * a⁻¹⁻¹
Tactic: rw [← inv_inj, mul_inv_rev, inv_inv, ha.comm, mul_inv_rev, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Center (goal)
Goal:
M : Type u_1
inst : DivisionMonoid M
a : M
ha : a ∈ center M
g : M
rw : (g * a⁻¹)⁻¹ = (a⁻¹ * g)⁻¹
rw₁ : a⁻¹⁻¹ * g⁻¹ = (a⁻¹ * g)⁻¹
rw₂ : a * g⁻¹ = (a⁻¹ * g)⁻¹
rw₃ : g⁻¹ * a = (a⁻¹ * g)⁻¹
rw₄ : g⁻¹ * a = g⁻¹ * a⁻¹⁻¹
⊢ g * a⁻¹ = a⁻¹ * g
have rw₅ : g⁻¹ * a = g⁻¹ * a
Tactic: rw [← inv_inj, mul_inv_rev, inv_inv, ha.comm, mul_inv_rev, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Center (goal)
Goal:
M : Type u_1
inst : DivisionMonoid M
a b : M
ha : a ∈ center M
hb : b ∈ center M
⊢ a / b ∈ center M
have rw : a * b⁻¹ ∈ center M
Tactic: rw [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Center (goal)
Goal:
M : Type u_1
S : Set M
inst : Group M
a : M
ha : a ∈ S.centralizer
g : M
hg : g ∈ S
⊢ g * a⁻¹ = a⁻¹ * g
have rw : g = a⁻¹ * g * a
Tactic: rw [mul_inv_eq_iff_eq_mul, mul_assoc, eq_inv_mul_iff_mul_eq, ha g hg]
-- Lean 4 proof step from Mathlib.Algebra.Group.Center (goal)
Goal:
M : Type u_1
S : Set M
inst : Group M
a : M
ha : a ∈ S.centralizer
g : M
hg : g ∈ S
rw : g = a⁻¹ * g * a
⊢ g * a⁻¹ = a⁻¹ * g
have rw₁ : g = a⁻¹ * (g * a)
Tactic: rw [mul_inv_eq_iff_eq_mul, mul_assoc, eq_inv_mul_iff_mul_eq, ha g hg]
-- Lean 4 proof step from Mathlib.Algebra.Group.Center (goal)
Goal:
M : Type u_1
S : Set M
inst : Group M
a : M
ha : a ∈ S.centralizer
g : M
hg : g ∈ S
rw : g = a⁻¹ * g * a
rw₁ : g = a⁻¹ * (g * a)
⊢ g * a⁻¹ = a⁻¹ * g
have rw₂ : a * g = g * a
Tactic: rw [mul_inv_eq_iff_eq_mul, mul_assoc, eq_inv_mul_iff_mul_eq, ha g hg]
-- Lean 4 proof step from Mathlib.Algebra.Group.Center (goal)
Goal:
M : Type u_1
S : Set M
inst : Group M
a : M
ha : a ∈ S.centralizer
g : M
hg : g ∈ S
rw : g = a⁻¹ * g * a
rw₁ : g = a⁻¹ * (g * a)
rw₂ : a * g = g * a
⊢ g * a⁻¹ = a⁻¹ * g
have rw₃ : a * g = a * g
Tactic: rw [mul_inv_eq_iff_eq_mul, mul_assoc, eq_inv_mul_iff_mul_eq, ha g hg]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Basic (goal)
Goal:
G : Type u_1
inst : DivisionMonoid G
a b c d : G
hbd : Commute b d
hbc : Commute b⁻¹ c
⊢ a / b * (c / d) = a * c / (b * d)
have simp_rw : a * b⁻¹ * (c * d⁻¹) = a * c * (b * d)⁻¹
Tactic: simp_rw [div_eq_mul_inv, mul_inv_rev, hbd.inv_inv.symm.eq, hbc.mul_mul_mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Basic (goal)
Goal:
G : Type u_1
inst : DivisionMonoid G
a b c d : G
hbd : Commute b d
hbc : Commute b⁻¹ c
simp_rw : a * b⁻¹ * (c * d⁻¹) = a * c * (b * d)⁻¹
⊢ a / b * (c / d) = a * c / (b * d)
have simp_rw₁ : a * b⁻¹ * (c * d⁻¹) = a * c * (d⁻¹ * b⁻¹)
Tactic: simp_rw [div_eq_mul_inv, mul_inv_rev, hbd.inv_inv.symm.eq, hbc.mul_mul_mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Basic (goal)
Goal:
G : Type u_1
inst : DivisionMonoid G
a b c d : G
hbd : Commute b d
hbc : Commute b⁻¹ c
simp_rw : a * b⁻¹ * (c * d⁻¹) = a * c * (b * d)⁻¹
simp_rw₁ : a * b⁻¹ * (c * d⁻¹) = a * c * (d⁻¹ * b⁻¹)
⊢ a / b * (c / d) = a * c / (b * d)
have simp_rw₂ : a * b⁻¹ * (c * d⁻¹) = a * c * (b⁻¹ * d⁻¹)
Tactic: simp_rw [div_eq_mul_inv, mul_inv_rev, hbd.inv_inv.symm.eq, hbc.mul_mul_mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Basic (goal)
Goal:
G : Type u_1
inst : DivisionMonoid G
a b c d : G
hbc : Commute b c
hbd : Commute b⁻¹ d
hcd : Commute c⁻¹ d
⊢ a / b / (c / d) = a / c / (b / d)
have simp_rw : a * b⁻¹ * (c * d⁻¹)⁻¹ = a * c⁻¹ * (b * d⁻¹)⁻¹
Tactic: simp_rw [div_eq_mul_inv, mul_inv_rev, inv_inv, hbd.symm.eq, hcd.symm.eq,
    hbc.inv_inv.mul_mul_mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Basic (goal)
Goal:
G : Type u_1
inst : DivisionMonoid G
a b c d : G
hbc : Commute b c
hbd : Commute b⁻¹ d
hcd : Commute c⁻¹ d
simp_rw : a * b⁻¹ * (c * d⁻¹)⁻¹ = a * c⁻¹ * (b * d⁻¹)⁻¹
⊢ a / b / (c / d) = a / c / (b / d)
have simp_rw₁ : a * b⁻¹ * (d⁻¹⁻¹ * c⁻¹) = a * c⁻¹ * (d⁻¹⁻¹ * b⁻¹)
Tactic: simp_rw [div_eq_mul_inv, mul_inv_rev, inv_inv, hbd.symm.eq, hcd.symm.eq,
    hbc.inv_inv.mul_mul_mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Basic (goal)
Goal:
G : Type u_1
inst : DivisionMonoid G
a b c d : G
hbc : Commute b c
hbd : Commute b⁻¹ d
hcd : Commute c⁻¹ d
simp_rw : a * b⁻¹ * (c * d⁻¹)⁻¹ = a * c⁻¹ * (b * d⁻¹)⁻¹
simp_rw₁ : a * b⁻¹ * (d⁻¹⁻¹ * c⁻¹) = a * c⁻¹ * (d⁻¹⁻¹ * b⁻¹)
⊢ a / b / (c / d) = a / c / (b / d)
have simp_rw₂ : a * b⁻¹ * (d * c⁻¹) = a * c⁻¹ * (d * b⁻¹)
Tactic: simp_rw [div_eq_mul_inv, mul_inv_rev, inv_inv, hbd.symm.eq, hcd.symm.eq,
    hbc.inv_inv.mul_mul_mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Basic (goal)
Goal:
G : Type u_1
inst : DivisionMonoid G
a b c d : G
hbc : Commute b c
hbd : Commute b⁻¹ d
hcd : Commute c⁻¹ d
simp_rw : a * b⁻¹ * (c * d⁻¹)⁻¹ = a * c⁻¹ * (b * d⁻¹)⁻¹
simp_rw₁ : a * b⁻¹ * (d⁻¹⁻¹ * c⁻¹) = a * c⁻¹ * (d⁻¹⁻¹ * b⁻¹)
simp_rw₂ : a * b⁻¹ * (d * c⁻¹) = a * c⁻¹ * (d * b⁻¹)
⊢ a / b / (c / d) = a / c / (b / d)
have simp_rw₃ : a * b⁻¹ * (d * c⁻¹) = a * c⁻¹ * (b⁻¹ * d)
Tactic: simp_rw [div_eq_mul_inv, mul_inv_rev, inv_inv, hbd.symm.eq, hcd.symm.eq,
    hbc.inv_inv.mul_mul_mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Basic (goal)
Goal:
G : Type u_1
inst : DivisionMonoid G
a b c d : G
hbc : Commute b c
hbd : Commute b⁻¹ d
hcd : Commute c⁻¹ d
simp_rw : a * b⁻¹ * (c * d⁻¹)⁻¹ = a * c⁻¹ * (b * d⁻¹)⁻¹
simp_rw₁ : a * b⁻¹ * (d⁻¹⁻¹ * c⁻¹) = a * c⁻¹ * (d⁻¹⁻¹ * b⁻¹)
simp_rw₂ : a * b⁻¹ * (d * c⁻¹) = a * c⁻¹ * (d * b⁻¹)
simp_rw₃ : a * b⁻¹ * (d * c⁻¹) = a * c⁻¹ * (b⁻¹ * d)
⊢ a / b / (c / d) = a / c / (b / d)
have simp_rw₄ : a * b⁻¹ * (c⁻¹ * d) = a * c⁻¹ * (b⁻¹ * d)
Tactic: simp_rw [div_eq_mul_inv, mul_inv_rev, inv_inv, hbd.symm.eq, hcd.symm.eq,
    hbc.inv_inv.mul_mul_mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Basic (goal)
Goal:
G : Type u_1
inst : Group G
a b : G
h : Commute a b
⊢ a⁻¹ * b * a = b
have rw : b * a⁻¹ * a = b
Tactic: rw [h.inv_left.eq, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Basic (goal)
Goal:
G : Type u_1
inst : Group G
a b : G
h : Commute a b
rw : b * a⁻¹ * a = b
⊢ a⁻¹ * b * a = b
have rw₁ : b = b
Tactic: rw [h.inv_left.eq, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Basic (goal)
Goal:
G : Type u_1
inst : Group G
a b : G
h : Commute a b
⊢ a⁻¹ * (b * a) = b
have rw : a⁻¹ * b * a = b
Tactic: rw [← mul_assoc, h.inv_mul_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Basic (goal)
Goal:
G : Type u_1
inst : Group G
a b : G
h : Commute a b
rw : a⁻¹ * b * a = b
⊢ a⁻¹ * (b * a) = b
have rw₁ : b = b
Tactic: rw [← mul_assoc, h.inv_mul_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a b : M
h : Commute a b
⊢ HPow.hPow (β := ℕ) (a * b) 0 = HPow.hPow (β := ℕ) a 0 * HPow.hPow (β := ℕ) b 0
have rw : 1 = HPow.hPow (β := ℕ) a 0 * HPow.hPow (β := ℕ) b 0
Tactic: rw [pow_zero, pow_zero, pow_zero, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a b : M
h : Commute a b
rw : 1 = HPow.hPow (β := ℕ) a 0 * HPow.hPow (β := ℕ) b 0
⊢ HPow.hPow (β := ℕ) (a * b) 0 = HPow.hPow (β := ℕ) a 0 * HPow.hPow (β := ℕ) b 0
have rw₁ : 1 = 1 * HPow.hPow (β := ℕ) b 0
Tactic: rw [pow_zero, pow_zero, pow_zero, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Commute.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a b : M
h : Commute a b
rw : 1 = HPow.hPow (β := ℕ) a 0 * HPow.hPow (β := ℕ) b 0
rw₁ : 1 = 1 * HPow.hPow (β := ℕ) b 0
⊢ HPow.hPow (β := ℕ) (a * b) 0 = HPow.hPow (β := ℕ) a 0 * HPow.hPow (β := ℕ) b 0
have rw₂ : 1 = HMul.hMul (α := M) 1 1
Tactic: rw [pow_zero, pow_zero, pow_zero, one_mul]