awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Center
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)
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)
⊢ Eq (α := Set ((i : ι) → A i)) (center ((i : ι) → A i)) (pi (α := A) univ fun (i : ι) ↦ center (A 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⟩

Premises used: forall_true_left, funext_iff, commute_iff_eq, isMulCentral_iff, Set.mem_pi, Set.mem_center_iff, Set.mem_univ, Pi.mul_def
-- Module: Mathlib.Algebra.Group.Center
Goal:
M : Type u_1
inst : Semigroup M
z : M
a : z ∈ center M
g : M
rw rw₁ : g * z = g * z
⊢ g * z = z * g

Tactic:
rw [IsMulCentral.comm a g]

Premises used: IsMulCentral.comm
-- Module: Mathlib.Algebra.Group.Center
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)
rw₄ rw₅ : a * (g * b) = a * (g * b)
⊢ g * (a * b) = a * b * g

Tactic:
rw [mul_assoc, ← hb g hg, ← mul_assoc, ha g hg, mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.Center
Goal:
M : Type u_1
S : Set M
inst : Semigroup M
h : ⊤ ≤ S.centralizer
x : M
hx : x ∈ S
x_1 : M
rw rw₁ : x_1 * x = x_1 * x
⊢ x_1 * x = x * x_1

Tactic:
rw [h trivial _ hx]

Premises used: trivial
-- Module: Mathlib.Algebra.Group.Center
Goal:
M : Type u_1
inst : Semigroup M
⊢ centralizer univ = center M

Tactic:
Subset.antisymm (fun _ ha ↦ Semigroup.mem_center_iff.mpr fun b ↦ ha b (Set.mem_univ b))
  fun _ ha b _ ↦ (ha.comm b).symm

Premises used: Set.Subset.antisymm, Iff.mpr, IsMulCentral.comm, Semigroup.mem_center_iff, Commute.symm, Set.mem_univ
-- Module: Mathlib.Algebra.Group.Center
Goal:
M : Type u_1
inst : CommSemigroup M
⊢ center M = univ

Tactic:
(Subset.antisymm (subset_univ _)) fun _ _ => Semigroup.mem_center_iff.mpr (fun _ => mul_comm _ _)

Premises used: Set.Subset.antisymm, Iff.mpr, Set.subset_univ, Semigroup.mem_center_iff, mul_comm
-- Module: Mathlib.Algebra.Group.Center
Goal:
M : Type u_1
S : Set M
inst : CommSemigroup M
⊢ S.centralizer = univ

Tactic:
eq_univ_of_forall fun _ _ _ ↦ mul_comm _ _

Premises used: Set.eq_univ_of_forall, mul_comm
-- Module: Mathlib.Algebra.Group.Center
Goal:
M : Type u_1
inst : MulOneClass M
x : M
rw : 1 * x = x * 1
rw₁ : x = x * 1
rw₂ rw₃ : x = x
⊢ Commute 1 x

Tactic:
rw [commute_iff_eq, one_mul, mul_one]

Premises used: commute_iff_eq, mul_one, one_mul
-- Module: Mathlib.Algebra.Group.Center
Goal:
M : Type u_1
inst : MulOneClass M
x x_1 : M
rw : x * x_1 = 1 * x * x_1
rw₁ rw₂ : x * x_1 = x * x_1
⊢ 1 * (x * x_1) = 1 * x * x_1

Tactic:
rw [one_mul, one_mul]

Premises used: one_mul
-- Module: Mathlib.Algebra.Group.Center
Goal:
M : Type u_1
inst : MulOneClass M
x x_1 : M
rw : x * x_1 = x * (x_1 * 1)
rw₁ rw₂ : x * x_1 = x * x_1
⊢ x * x_1 * 1 = x * (x_1 * 1)

Tactic:
rw [mul_one, mul_one]

Premises used: mul_one
-- Module: Mathlib.Algebra.Group.Center
Goal:
M : Type u_1
S : Set M
inst : MulOneClass M
⊢ 1 ∈ S.centralizer

Tactic:
simp [mem_centralizer_iff]

Premises used: Set.mem_centralizer_iff
-- Module: Mathlib.Algebra.Group.Center
Goal:
M : Type u_1
inst : Monoid M
x : Mˣ
ha : Membership.mem (γ := Set Mˣ) (Units.val ⁻¹' center M) x
rw : ∀ (g : Mˣ), g * x = x * g
⊢ Membership.mem (γ := Set Mˣ) (center Mˣ) x

Tactic:
rw [_root_.Semigroup.mem_center_iff]

Premises used: Semigroup.mem_center_iff
-- Module: Mathlib.Algebra.Group.Center
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)
rw₃ rw₄ : (↑g : M) * (↑x : M) = (↑g : M) * (↑x : M)
⊢ g * x = x * g

Tactic:
rw [← Units.val_inj, Units.val_mul, Units.val_mul, ha.comm]

Premises used: IsMulCentral.comm, Units.val_inj, Units.val_mul
-- Module: Mathlib.Algebra.Group.Center
Goal:
M : Type u_1
inst : Monoid M
a : Mˣ
ha : (↑a : M) ∈ center M
rw : ∀ (ha : ∀ (g : M), g * (↑a : M) = (↑a : M) * g) (g : M), g * (↑a⁻¹ : M) = (↑a⁻¹ : M) * g
⊢ (↑a⁻¹ : M) ∈ center M

Tactic:
rw [Semigroup.mem_center_iff] at *

Premises used: Semigroup.mem_center_iff
-- Module: Mathlib.Algebra.Group.Center
Goal:
M : Type u_1
inst : Monoid M
a : Mˣ
ha : ∀ (g : M), g * (↑a : M) = (↑a : M) * g
⊢ ∀ (g : M), g * (↑a⁻¹ : M) = (↑a⁻¹ : M) * g

Tactic:
(Commute.units_inv_right <| ha ·)

Premises used: SemiconjBy, Commute, Commute.units_inv_right
-- Module: Mathlib.Algebra.Group.Center
Goal:
M : Type u_1
inst : Monoid M
a : Mˣ
ha : ∀ (g : M), g * (↑a : M) = (↑a : M) * g
⊢ ∀ (g : M), g * (↑a⁻¹ : M) = (↑a⁻¹ : M) * g

Tactic:
exact (Commute.units_inv_right <| ha ·)

Premises used: Commute.units_inv_right
-- Module: Mathlib.Algebra.Group.Center
Goal:
M : Type u_1
inst : Monoid M
a : M
inst_1 : Invertible a
ha : a ∈ center M
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
⊢ @Invertible.invOf _ MulOne.toMul MulOne.toOne a _ ∈ center M

Tactic:
rw [Semigroup.mem_center_iff] at *

Premises used: Semigroup.mem_center_iff
-- Module: Mathlib.Algebra.Group.Center
Goal:
M : Type u_1
inst : Monoid M
a : M
inst_1 : Invertible a
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:
(Commute.invOf_right <| ha ·)

Premises used: Commute.invOf_right, SemiconjBy, Commute
-- Module: Mathlib.Algebra.Group.Center
Goal:
M : Type u_1
inst : Monoid M
a : M
inst_1 : Invertible a
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:
exact (Commute.invOf_right <| ha ·)

Premises used: Commute.invOf_right
-- Module: Mathlib.Algebra.Group.Center
Goal:
M : Type u_1
inst : DivisionMonoid M
a : M
ha : a ∈ center M
rw : ∀ (g : M), g * a⁻¹ = a⁻¹ * g
⊢ a⁻¹ ∈ center M

Tactic:
rw [_root_.Semigroup.mem_center_iff]

Premises used: Semigroup.mem_center_iff
-- Module: Mathlib.Algebra.Group.Center
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⁻¹⁻¹
rw₅ rw₆ : g⁻¹ * a = g⁻¹ * a
⊢ g * a⁻¹ = a⁻¹ * g

Tactic:
rw [← inv_inj, mul_inv_rev, inv_inv, ha.comm, mul_inv_rev, inv_inv]

Premises used: IsMulCentral.comm, inv_inj, inv_inv, mul_inv_rev
-- Module: Mathlib.Algebra.Group.Center
Goal:
M : Type u_1
inst : DivisionMonoid M
a b : M
ha : a ∈ center M
hb : b ∈ center M
rw : a * b⁻¹ ∈ center M
⊢ a / b ∈ center M

Tactic:
rw [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Group.Center
Goal:
M : Type u_1
inst : DivisionMonoid M
a b : M
ha : a ∈ center M
hb : b ∈ center M
⊢ a * b⁻¹ ∈ center M

Tactic:
mul_mem_center ha (inv_mem_center hb)

Premises used: Set.mul_mem_center, Set.inv_mem_center
-- Module: Mathlib.Algebra.Group.Center
Goal:
M : Type u_1
inst : DivisionMonoid M
a b : M
ha : a ∈ center M
hb : b ∈ center M
⊢ a * b⁻¹ ∈ center M

Tactic:
exact mul_mem_center ha (inv_mem_center hb)

Premises used: Set.mul_mem_center, Set.inv_mem_center
-- Module: Mathlib.Algebra.Group.Center
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
rw₃ rw₄ : a * g = a * g
⊢ g * a⁻¹ = a⁻¹ * g

Tactic:
rw [mul_inv_eq_iff_eq_mul, mul_assoc, eq_inv_mul_iff_mul_eq, ha g hg]

Premises used: mul_assoc, eq_inv_mul_iff_mul_eq, mul_inv_eq_iff_eq_mul
-- Module: Mathlib.Algebra.Group.Center
Goal:
M : Type u_1
S : Set M
inst : Group M
a b : M
ha : a ∈ S.centralizer
hb : b ∈ S.centralizer
⊢ a / b ∈ S.centralizer

Tactic:
simpa only [div_eq_mul_inv] using mul_mem_centralizer ha (inv_mem_centralizer hb)

Premises used: div_eq_mul_inv, Set.mul_mem_centralizer, Set.inv_mem_centralizer
-- Module: Mathlib.Algebra.Group.Commutator
Goal:
G : Type u_1
inst : Group G
g₁ g₂ : G
⊢ ⁅g₁, g₂⁆ = g₁ * g₂ * g₁⁻¹ * g₂⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Commute.Basic
Goal:
G : Type u_1
inst : Semigroup G
a b c : G
h : SemiconjBy a b c
j : G
⊢ Eq.{u_1 + 1} (α := G) ((fun (x : G) ↦ a * x) ((fun (x : G) ↦ b * x) j))
    ((fun (x : G) ↦ c * x) ((fun (x : G) ↦ a * x) j))

Tactic:
simp only [← mul_assoc, h.eq]

Premises used: mul_assoc, SemiconjBy.eq
-- Module: Mathlib.Algebra.Group.Commute.Basic
Goal:
G : Type u_1
inst : Semigroup G
a b : G
h : Commute a b
⊢ Function.Commute (fun (x : G) ↦ a * x) fun (x : G) ↦ b * x

Tactic:
SemiconjBy.function_semiconj_mul_left h

Premises used: Function.Commute, SemiconjBy.function_semiconj_mul_left
-- Module: Mathlib.Algebra.Group.Commute.Basic
Goal:
G : Type u_1
inst : Semigroup G
a b c : G
h : SemiconjBy a b c
j : G
⊢ Eq.{u_1 + 1} (α := G) ((fun (x : G) ↦ x * a) ((fun (x : G) ↦ x * c) j))
    ((fun (x : G) ↦ x * b) ((fun (x : G) ↦ x * a) j))

Tactic:
simp only [mul_assoc, ← h.eq]

Premises used: mul_assoc, SemiconjBy.eq
-- Module: Mathlib.Algebra.Group.Commute.Basic
Goal:
G : Type u_1
inst : Semigroup G
a b : G
h : Commute a b
⊢ Function.Commute (fun (x : G) ↦ x * a) fun (x : G) ↦ x * b

Tactic:
SemiconjBy.function_semiconj_mul_right_swap h

Premises used: Function.Commute, SemiconjBy.function_semiconj_mul_right_swap
-- Module: Mathlib.Algebra.Group.Commute.Basic
Goal:
G : Type u_1
inst : DivisionMonoid G
a b : G
⊢ Commute a b → Commute a⁻¹ b⁻¹

Tactic:
SemiconjBy.inv_inv_symm

Premises used: SemiconjBy.inv_inv_symm, Commute
-- Module: Mathlib.Algebra.Group.Commute.Basic
Goal:
G : Type u_1
inst : DivisionMonoid G
a b : G
⊢ Commute a⁻¹ b⁻¹ ↔ Commute a b

Tactic:
SemiconjBy.inv_inv_symm_iff

Premises used: SemiconjBy.inv_inv_symm_iff, Commute
-- Module: Mathlib.Algebra.Group.Commute.Basic
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⁻¹)
simp_rw₂ : a * b⁻¹ * (c * d⁻¹) = a * c * (b⁻¹ * d⁻¹)
⊢ 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]

Premises used: Commute.mul_mul_mul_comm, div_eq_mul_inv, Commute.symm, mul_inv_rev, Commute.inv_inv, Commute.eq
-- Module: Mathlib.Algebra.Group.Commute.Basic
Goal:
G : Type u_1
inst : DivisionMonoid G
a b c d : G
hcd : Commute c d
hbc : Commute b c⁻¹
⊢ a * b / (c * d) = a / c * (b / d)

Tactic:
(hcd.div_mul_div_comm hbc.symm).symm

Premises used: Commute.div_mul_div_comm, Commute.symm, Eq.symm
-- Module: Mathlib.Algebra.Group.Commute.Basic
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)
simp_rw₄ : a * b⁻¹ * (c⁻¹ * d) = a * c⁻¹ * (b⁻¹ * d)
⊢ 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]

Premises used: Commute.mul_mul_mul_comm, div_eq_mul_inv, Commute.symm, inv_inv, mul_inv_rev, Commute.inv_inv, Commute.eq
-- Module: Mathlib.Algebra.Group.Commute.Basic
Goal:
G : Type u_1
inst : Group G
a b : G
⊢ Commute a⁻¹ b ↔ Commute a b

Tactic:
SemiconjBy.inv_symm_left_iff

Premises used: Commute, SemiconjBy.inv_symm_left_iff
-- Module: Mathlib.Algebra.Group.Commute.Basic
Goal:
G : Type u_1
inst : Group G
a b : G
⊢ Commute a b⁻¹ ↔ Commute a b

Tactic:
SemiconjBy.inv_right_iff

Premises used: Commute, SemiconjBy.inv_right_iff
-- Module: Mathlib.Algebra.Group.Commute.Basic
Goal:
G : Type u_1
inst : Group G
a b : G
h : Commute a b
rw : b * a⁻¹ * a = b
rw₁ rw₂ : b = b
⊢ a⁻¹ * b * a = b

Tactic:
rw [h.inv_left.eq, inv_mul_cancel_right]

Premises used: Commute.inv_left, inv_mul_cancel_right, Commute.eq
-- Module: Mathlib.Algebra.Group.Commute.Basic
Goal:
G : Type u_1
inst : Group G
a b : G
h : Commute a b
rw : a⁻¹ * b * a = b
rw₁ rw₂ : b = b
⊢ a⁻¹ * (b * a) = b

Tactic:
rw [← mul_assoc, h.inv_mul_cancel]

Premises used: mul_assoc, Commute.inv_mul_cancel
-- Module: Mathlib.Algebra.Group.Commute.Basic
Goal:
G : Type u_1
inst : Group G
a b h : G
⊢ Commute (h * a * h⁻¹) (h * b * h⁻¹) ↔ Commute a b

Tactic:
SemiconjBy.conj_iff

Premises used: Commute, SemiconjBy.conj_iff
-- Module: Mathlib.Algebra.Group.Commute.Basic
Goal:
G : Type u_1
inst : Group G
a b : G
comm : Commute a b
h : G
⊢ Commute (h * a * h⁻¹) (h * b * h⁻¹)

Tactic:
(Commute.conj_iff h).mpr comm

Premises used: Iff.mpr, Commute.conj_iff
-- Module: Mathlib.Algebra.Group.Commute.Basic
Goal:
G : Type u_1
inst : Group G
a b : G
h : Commute a b
m : ℤ
⊢ Commute a (b ^ m)

Tactic:
SemiconjBy.zpow_right h m

Premises used: Commute, SemiconjBy.zpow_right
-- Module: Mathlib.Algebra.Group.Commute.Basic
Goal:
G : Type u_1
inst : Group G
a b : G
h : Commute a b
m : ℤ
⊢ Commute (a ^ m) b

Tactic:
(h.symm.zpow_right m).symm

Premises used: Commute.zpow_right, Commute.symm
-- Module: Mathlib.Algebra.Group.Commute.Basic
Goal:
G : Type u_1
inst : Group G
a b : G
h : Commute a b
m n : ℤ
⊢ Commute (a ^ m) (b ^ n)

Tactic:
(h.zpow_left m).zpow_right n

Premises used: Commute.zpow_right, Commute.zpow_left
-- Module: Mathlib.Algebra.Group.Commute.Basic
Goal:
G : Type u_1
inst : Group G
a : G
n : ℤ
⊢ Commute a (a ^ n)

Tactic:
(Commute.refl a).zpow_right n

Premises used: Commute.zpow_right, Commute.refl
-- Module: Mathlib.Algebra.Group.Commute.Basic
Goal:
G : Type u_1
inst : Group G
a : G
n : ℤ
⊢ Commute (a ^ n) a

Tactic:
(Commute.refl a).zpow_left n

Premises used: Commute.zpow_left, Commute.refl
-- Module: Mathlib.Algebra.Group.Commute.Basic
Goal:
G : Type u_1
inst : Group G
a : G
m n : ℤ
⊢ Commute (a ^ m) (a ^ n)

Tactic:
(Commute.refl a).zpow_zpow m n

Premises used: Commute.zpow_zpow, Commute.refl
-- Module: Mathlib.Algebra.Group.Commute.Basic
Goal:
G : Type u_1
inst : Group G
a : G
m n : ℕ
⊢ a⁻¹ ^ m * a ^ n = a ^ n * a⁻¹ ^ m

Tactic:
(Commute.refl a).inv_left.pow_pow _ _

Premises used: SemiconjBy, Commute.pow_pow, Commute, Commute.inv_left, Commute.refl
-- Module: Mathlib.Algebra.Group.Commute.Defs
Goal:
S : Type u_3
inst : Mul S
a b : S
⊢ Commute a b ↔ a * b = b * a

Tactic:
Iff.rfl

Premises used: Iff.rfl, SemiconjBy, Commute
-- Module: Mathlib.Algebra.Group.Commute.Defs
Goal:
S : Type u_3
inst : Mul S
a b : S
h : Commute a b
⊢ a * b = b * a

Tactic:
h

Premises used: SemiconjBy, Commute
-- Module: Mathlib.Algebra.Group.Commute.Defs
Goal:
S : Type u_3
inst : Mul S
a : S
⊢ Commute a a

Tactic:
Eq.refl (a * a)

Premises used: HMul.hMul, SemiconjBy, Commute, Eq.refl
-- Module: Mathlib.Algebra.Group.Commute.Defs
Goal:
S : Type u_3
inst : Mul S
a b : S
h : Commute a b
⊢ Commute b a

Tactic:
Eq.symm h

Premises used: SemiconjBy, Commute, Eq.symm
-- Module: Mathlib.Algebra.Group.Commute.Defs
Goal:
S : Type u_3
inst : Mul S
a b : S
h : Commute a b
⊢ SemiconjBy a b b

Tactic:
h

Premises used: Commute
-- Module: Mathlib.Algebra.Group.Commute.Defs
Goal:
S : Type u_3
inst : Mul S
a b : S
⊢ Commute a b ↔ Commute b a

Tactic:
⟨Commute.symm, Commute.symm⟩

Premises used: Commute.symm, Iff.intro
-- Module: Mathlib.Algebra.Group.Commute.Defs
Goal:
G : Type u_1
M : Type u_2
S : Type u_3
inst : Mul S
⊢ Std.Refl.{u_3 + 1} (α := S) Commute

Tactic:
⟨Commute.refl⟩

Premises used: Std.Refl.mk, Commute.refl
-- Module: Mathlib.Algebra.Group.Commute.Defs
Goal:
G : Type u_1
M : Type u_2
S : Type u_3
inst : Mul S
f : G → S
⊢ Std.Refl fun (a b : G) ↦ Commute (f a) (f b)

Tactic:
⟨fun _ => Commute.refl _⟩

Premises used: Std.Refl.mk, Commute.refl
-- Module: Mathlib.Algebra.Group.Commute.Defs
Goal:
S : Type u_3
inst : Semigroup S
a b c : S
hab : Commute a b
hac : Commute a c
⊢ Commute a (b * c)

Tactic:
SemiconjBy.mul_right hab hac

Premises used: Commute, SemiconjBy.mul_right
-- Module: Mathlib.Algebra.Group.Commute.Defs
Goal:
S : Type u_3
inst : Semigroup S
a b c : S
hac : Commute a c
hbc : Commute b c
⊢ Commute (a * b) c

Tactic:
SemiconjBy.mul_left hac hbc

Premises used: Commute, SemiconjBy.mul_left
-- Module: Mathlib.Algebra.Group.Commute.Defs
Goal:
S : Type u_3
inst : Semigroup S
b c : S
h : Commute b c
a : S
⊢ a * b * c = a * c * b

Tactic:
simp only [mul_assoc, h.eq]

Premises used: mul_assoc, Commute.eq
-- Module: Mathlib.Algebra.Group.Commute.Defs
Goal:
S : Type u_3
inst : Semigroup S
a b : S
h : Commute a b
c : S
⊢ a * (b * c) = b * (a * c)

Tactic:
simp only [← mul_assoc, h.eq]

Premises used: mul_assoc, Commute.eq
-- Module: Mathlib.Algebra.Group.Commute.Defs
Goal:
S : Type u_3
inst : Semigroup S
b c : S
hbc : Commute b c
a d : S
⊢ a * b * (c * d) = a * c * (b * d)

Tactic:
simp only [hbc.left_comm, mul_assoc]

Premises used: Commute.left_comm, mul_assoc
-- Module: Mathlib.Algebra.Group.Commute.Defs
Goal:
S : Type u_3
inst : CommMagma S
a b : S
⊢ Commute a b

Tactic:
mul_comm a b

Premises used: SemiconjBy, Commute, mul_comm
-- Module: Mathlib.Algebra.Group.Commute.Defs
Goal:
M : Type u_2
inst : MulOneClass M
a : M
⊢ Commute a 1

Tactic:
SemiconjBy.one_right a

Premises used: Commute, SemiconjBy.one_right
-- Module: Mathlib.Algebra.Group.Commute.Defs
Goal:
M : Type u_2
inst : MulOneClass M
a : M
⊢ Commute 1 a

Tactic:
SemiconjBy.one_left a

Premises used: Commute, SemiconjBy.one_left
-- Module: Mathlib.Algebra.Group.Commute.Defs
Goal:
M : Type u_2
inst : Monoid M
a b : M
h : Commute a b
n : ℕ
⊢ Commute a (b ^ n)

Tactic:
SemiconjBy.pow_right h n

Premises used: Commute, SemiconjBy.pow_right
-- Module: Mathlib.Algebra.Group.Commute.Defs
Goal:
M : Type u_2
inst : Monoid M
a b : M
h : Commute a b
n : ℕ
⊢ Commute (a ^ n) b

Tactic:
(h.symm.pow_right n).symm

Premises used: Commute.pow_right, Commute.symm
-- Module: Mathlib.Algebra.Group.Commute.Defs
Goal:
M : Type u_2
inst : Monoid M
a b : M
h : Commute a b
m n : ℕ
⊢ Commute (a ^ m) (b ^ n)

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Group.Commute.Defs
Goal:
M : Type u_2
inst : Monoid M
a : M
n : ℕ
⊢ Commute a (a ^ n)

Tactic:
(Commute.refl a).pow_right n

Premises used: Commute.pow_right, Commute.refl
-- Module: Mathlib.Algebra.Group.Commute.Defs
Goal:
M : Type u_2
inst : Monoid M
a : M
n : ℕ
⊢ Commute (a ^ n) a

Tactic:
(Commute.refl a).pow_left n

Premises used: Commute.pow_left, Commute.refl
-- Module: Mathlib.Algebra.Group.Commute.Defs
Goal:
M : Type u_2
inst : Monoid M
a : M
m n : ℕ
⊢ Commute (a ^ m) (a ^ n)

Tactic:
(Commute.refl a).pow_pow m n

Premises used: Commute.pow_pow, Commute.refl
-- Module: Mathlib.Algebra.Group.Commute.Defs
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
rw₂ : 1 = HMul.hMul (α := M) 1 1
rw₃ rw₄ : Eq.{u_2 + 1} (α := M) 1 1
⊢ HPow.hPow (β := ℕ) (a * b) 0 = HPow.hPow (β := ℕ) a 0 * HPow.hPow (β := ℕ) b 0

Tactic:
rw [pow_zero, pow_zero, pow_zero, one_mul]

Premises used: pow_zero, one_mul
-- Module: Mathlib.Algebra.Group.Commute.Defs
Goal:
M : Type u_2
inst : Monoid M
a b : M
h : Commute a b
n : ℕ
⊢ (a * b) ^ (n + 1) = a ^ (n + 1) * b ^ (n + 1)

Tactic:
simp only [pow_succ', h.mul_pow n, ← mul_assoc, (h.pow_left n).right_comm]

Premises used: mul_assoc, Commute.pow_left, Commute.right_comm, pow_succ'
-- Module: Mathlib.Algebra.Group.Commute.Defs
Goal:
G : Type u_1
inst : DivisionMonoid G
a b : G
hab : Commute a b
rw : (b * a)⁻¹ = a⁻¹ * b⁻¹
rw₁ rw₂ : a⁻¹ * b⁻¹ = a⁻¹ * b⁻¹
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹

Tactic:
rw [hab.eq, mul_inv_rev]

Premises used: mul_inv_rev, Commute.eq
-- Module: Mathlib.Algebra.Group.Commute.Defs
Goal:
G : Type u_1
inst : DivisionMonoid G
a b : G
h : Commute a b
n : ℕ
⊢ HPow.hPow (β := ℤ) (a * b) (↑n : ℤ) = HPow.hPow (β := ℤ) a (↑n : ℤ) * HPow.hPow (β := ℤ) b (↑n : ℤ)

Tactic:
simp [zpow_natCast, h.mul_pow n]

Premises used: zpow_natCast, Commute.mul_pow
-- Module: Mathlib.Algebra.Group.Commute.Defs
Goal:
G : Type u_1
inst : DivisionMonoid G
a b : G
h : Commute a b
n : ℕ
⊢ (a * b) ^ Int.negSucc n = a ^ Int.negSucc n * b ^ Int.negSucc n

Tactic:
simp [h.mul_pow, (h.pow_pow _ _).eq, mul_inv_rev]

Premises used: Commute.pow_pow, Commute.mul_pow, mul_inv_rev, Commute.eq
-- Module: Mathlib.Algebra.Group.Commute.Defs
Goal:
G : Type u_1
inst : Group G
a b : G
h : Commute a b
rw : b * a * a⁻¹ = b
rw₁ rw₂ : b = b
⊢ a * b * a⁻¹ = b

Tactic:
rw [h.eq, mul_inv_cancel_right]

Premises used: mul_inv_cancel_right, Commute.eq
-- Module: Mathlib.Algebra.Group.Commute.Defs
Goal:
G : Type u_1
inst : Group G
a b : G
h : Commute a b
rw : a * b * a⁻¹ = b
rw₁ rw₂ : b = b
⊢ a * (b * a⁻¹) = b

Tactic:
rw [← mul_assoc, h.mul_inv_cancel]

Premises used: mul_assoc, Commute.mul_inv_cancel
-- Module: Mathlib.Algebra.Group.Commute.Hom
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
inst : Mul M
inst_1 : Mul N
a x y : M
inst_2 : FunLike F M N
inst_3 : MulHomClass F M N
h : SemiconjBy a x y
f : F
⊢ SemiconjBy.{u_3} (M := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)

Tactic:
simpa only [SemiconjBy, map_mul] using congr_arg f h

Premises used: SemiconjBy, congr_arg, map_mul, DFunLike.coe
-- Module: Mathlib.Algebra.Group.Commute.Hom
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
inst : Mul M
inst_1 : Mul N
x y : M
inst_2 : FunLike F M N
inst_3 : MulHomClass F M N
h : Commute x y
f : F
⊢ Commute.{u_3} (S := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)

Tactic:
SemiconjBy.map h f

Premises used: Commute, SemiconjBy.map
-- Module: Mathlib.Algebra.Group.Commute.Hom
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
inst : Mul M
inst_1 : Mul N
a x y : M
inst_2 : FunLike F M N
inst_3 : MulHomClass F M N
f : F
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
h : SemiconjBy.{u_3} (M := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)
⊢ Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) (a * x) : N) ((f : (a : M) → N) (y * a) : N)

Tactic:
simpa only [SemiconjBy, map_mul] using h

Premises used: SemiconjBy, map_mul
-- Module: Mathlib.Algebra.Group.Commute.Hom
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
inst : Mul M
inst_1 : Mul N
x y : M
inst_2 : FunLike F M N
inst_3 : MulHomClass F M N
f : F
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
h : Commute.{u_3} (S := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)
⊢ Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) (x * y) : N) ((f : (a : M) → N) (y * x) : N)

Tactic:
simpa only [map_mul] using h.eq

Premises used: map_mul, Commute.eq