awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanAlgebra α
a b : AsBoolRing α
⊢ LE.le (α := α) ((ofBoolRing : (a : AsBoolRing α) → α) a : α) ((ofBoolRing : (a : AsBoolRing α) → α) b : α) ↔ a * b = a

Tactic:
inf_eq_left.symm

Premises used: AsBoolRing, inf_eq_left, Iff.symm
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanAlgebra α
⊢ Eq.{u_1 + 1} (α := AsBoolRing α) ((toBoolRing : (a : α) → AsBoolRing α) ⊥ : AsBoolRing α) (0 : AsBoolRing α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanAlgebra α
⊢ Eq.{u_1 + 1} (α := AsBoolRing α) ((toBoolRing : (a : α) → AsBoolRing α) ⊤ : AsBoolRing α) (1 : AsBoolRing α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanAlgebra α
a b : α
⊢ (toBoolRing : (a : α) → AsBoolRing α) (a ⊓ b) =
    HMul.hMul (α := AsBoolRing α) (β := AsBoolRing α) ((toBoolRing : (a : α) → AsBoolRing α) a : AsBoolRing α)
      ((toBoolRing : (a : α) → AsBoolRing α) b : AsBoolRing α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanAlgebra α
a b : α
⊢ (toBoolRing : (a : α) → AsBoolRing α) (a ∆ b) =
    HAdd.hAdd (α := AsBoolRing α) (β := AsBoolRing α) ((toBoolRing : (a : α) → AsBoolRing α) a : AsBoolRing α)
      ((toBoolRing : (a : α) → AsBoolRing α) b : AsBoolRing α)

Tactic:
rfl

Premises used: symmDiff, rfl
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanAlgebra α
⊢ Eq (α := AsBoolRing α →+* AsBoolRing α) (BoundedLatticeHom.asBoolRing (BoundedLatticeHom.id α))
    (RingHom.id (AsBoolRing α))

Tactic:
rfl

Premises used: BoundedLatticeHom.asBoolRing, rfl
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
inst_2 : BooleanAlgebra γ
g : BoundedLatticeHom β γ
f : BoundedLatticeHom α β
⊢ (g.comp f).asBoolRing = g.asBoolRing.comp f.asBoolRing

Tactic:
rfl

Premises used: BoundedLatticeHom.asBoolRing, rfl
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
a : Bool
false : Bool.false * 0 = 0
true : Bool.true * 0 = 0
⊢ a * 0 = 0

Tactic:
cases a
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ false * 0 = 0

Tactic:
rfl
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ true * 0 = 0

Tactic:
rfl
-- Module: Mathlib.Algebra.Ring.Center
Goal:
M : Type u_1
inst : NonAssocSemiring M
n : ℕ
x : M
rw : (↑n : M) * x = x * (↑n : M)
rw₁ rw₂ : (↑n : M) * x = (↑n : M) * x
⊢ Commute (↑n : M) x

Tactic:
rw [commute_iff_eq, Nat.commute_cast]

Premises used: Nat.commute_cast, commute_iff_eq
-- Module: Mathlib.Algebra.Ring.Center
Goal:
M : Type u_1
inst : NonAssocSemiring M
x x_1 : M
zero : 0 * (x * x_1) = 0 * x * x_1
zero₁ : 0 = 0 * x * x_1
zero₂ : 0 = 0 * x_1
zero₃ zero₄ : Eq.{u_1 + 1} (α := M) 0 0
⊢ (↑0 : M) * (x * x_1) = (↑0 : M) * x * x_1

Tactic:
rw [Nat.cast_zero, zero_mul, zero_mul, zero_mul]

Premises used: MulZeroClass.zero_mul, Nat.cast_zero
-- Module: Mathlib.Algebra.Ring.Center
Goal:
M : Type u_1
inst : NonAssocSemiring M
x x_1 : M
n : ℕ
ihn : (↑n : M) * (x * x_1) = (↑n : M) * x * x_1
succ : HAdd.hAdd (α := M) (↑n : M) 1 * (x * x_1) = HAdd.hAdd (α := M) (↑n : M) 1 * x * x_1
succ₁ : (↑n : M) * (x * x_1) + 1 * (x * x_1) = HAdd.hAdd (α := M) (↑n : M) 1 * x * x_1
succ₂ : (↑n : M) * (x * x_1) + x * x_1 = HAdd.hAdd (α := M) (↑n : M) 1 * x * x_1
succ₃ : (↑n : M) * x * x_1 + x * x_1 = HAdd.hAdd (α := M) (↑n : M) 1 * x * x_1
succ₄ : (↑n : M) * x * x_1 + x * x_1 = ((↑n : M) * x + 1 * x) * x_1
succ₅ : (↑n : M) * x * x_1 + x * x_1 = (↑n : M) * x * x_1 + 1 * x * x_1
succ₆ succ₇ : (↑n : M) * x * x_1 + x * x_1 = (↑n : M) * x * x_1 + x * x_1
⊢ (↑(n + 1) : M) * (x * x_1) = (↑(n + 1) : M) * x * x_1

Tactic:
rw [Nat.cast_succ, add_mul, one_mul, ihn, add_mul, add_mul, one_mul]

Premises used: add_mul, Nat.cast_succ, one_mul
-- Module: Mathlib.Algebra.Ring.Center
Goal:
M : Type u_1
inst : NonAssocSemiring M
n : ℕ
x x_1 : M
zero : (↑0 : M) * (x * x_1) = (↑0 : M) * x * x_1
succ :
  ∀ (n : ℕ) (ihn : (↑n : M) * (x * x_1) = (↑n : M) * x * x_1), (↑(n + 1) : M) * (x * x_1) = (↑(n + 1) : M) * x * x_1
⊢ (↑n : M) * (x * x_1) = (↑n : M) * x * x_1

Tactic:
induction n with
    | zero => rw [Nat.cast_zero, zero_mul, zero_mul, zero_mul]
    | succ n ihn => rw [Nat.cast_succ, add_mul, one_mul, ihn, add_mul, add_mul, one_mul]

Premises used: add_mul, Nat.cast_succ, MulZeroClass.zero_mul, Nat.cast_zero, one_mul
-- Module: Mathlib.Algebra.Ring.Center
Goal:
M : Type u_1
inst : NonAssocSemiring M
x x_1 : M
zero : x * x_1 * 0 = x * (x_1 * 0)
zero₁ : 0 = x * (x_1 * 0)
zero₂ : 0 = x * 0
zero₃ zero₄ : Eq.{u_1 + 1} (α := M) 0 0
⊢ x * x_1 * (↑0 : M) = x * (x_1 * (↑0 : M))

Tactic:
rw [Nat.cast_zero, mul_zero, mul_zero, mul_zero]

Premises used: MulZeroClass.mul_zero, Nat.cast_zero
-- Module: Mathlib.Algebra.Ring.Center
Goal:
M : Type u_1
inst : NonAssocSemiring M
x x_1 : M
n : ℕ
ihn : x * x_1 * (↑n : M) = x * (x_1 * (↑n : M))
succ : x * x_1 * HAdd.hAdd (α := M) (↑n : M) 1 = x * (x_1 * HAdd.hAdd (α := M) (↑n : M) 1)
succ₁ : x * x_1 * (↑n : M) + x * x_1 * 1 = x * (x_1 * HAdd.hAdd (α := M) (↑n : M) 1)
succ₂ : x * (x_1 * (↑n : M)) + x * x_1 * 1 = x * (x_1 * HAdd.hAdd (α := M) (↑n : M) 1)
succ₃ : x * (x_1 * (↑n : M)) + x * x_1 * 1 = x * (x_1 * (↑n : M) + x_1 * 1)
succ₄ : x * (x_1 * (↑n : M)) + x * x_1 * 1 = x * (x_1 * (↑n : M)) + x * (x_1 * 1)
succ₅ : x * (x_1 * (↑n : M)) + x * x_1 = x * (x_1 * (↑n : M)) + x * (x_1 * 1)
succ₆ succ₇ : x * (x_1 * (↑n : M)) + x * x_1 = x * (x_1 * (↑n : M)) + x * x_1
⊢ x * x_1 * (↑(n + 1) : M) = x * (x_1 * (↑(n + 1) : M))

Tactic:
rw [Nat.cast_succ, mul_add, ihn, mul_add, mul_add, mul_one, mul_one]

Premises used: Nat.cast_succ, mul_add, mul_one
-- Module: Mathlib.Algebra.Ring.Center
Goal:
M : Type u_1
inst : NonAssocSemiring M
n : ℕ
x x_1 : M
zero : x * x_1 * (↑0 : M) = x * (x_1 * (↑0 : M))
succ :
  ∀ (n : ℕ) (ihn : x * x_1 * (↑n : M) = x * (x_1 * (↑n : M))), x * x_1 * (↑(n + 1) : M) = x * (x_1 * (↑(n + 1) : M))
⊢ x * x_1 * (↑n : M) = x * (x_1 * (↑n : M))

Tactic:
induction n with
    | zero => rw [Nat.cast_zero, mul_zero, mul_zero, mul_zero]
    | succ n ihn => rw [Nat.cast_succ, mul_add, ihn, mul_add, mul_add, mul_one, mul_one]

Premises used: Nat.cast_succ, MulZeroClass.mul_zero, mul_add, Nat.cast_zero, mul_one
-- Module: Mathlib.Algebra.Ring.Center
Goal:
M : Type u_1
inst : NonAssocSemiring M
n : ℕ
inst_1 : n.AtLeastTwo
⊢ OfNat.ofNat n ∈ center M

Tactic:
natCast_mem_center M n

Premises used: Set.Mem, Set.natCast_mem_center
-- Module: Mathlib.Algebra.Ring.Center
Goal:
M : Type u_1
inst : NonAssocRing M
n : ℤ
x : M
rw : (↑n : M) * x = x * (↑n : M)
rw₁ rw₂ : (↑n : M) * x = (↑n : M) * x
⊢ Commute (↑n : M) x

Tactic:
rw [commute_iff_eq, Int.commute_cast]

Premises used: Int.commute_cast, commute_iff_eq
-- Module: Mathlib.Algebra.Ring.Center
Goal:
M : Type u_1
inst : NonAssocRing M
n_1 : ℤ
x x_1 : M
n : ℕ
rw : (↑n : M) * (x * x_1) = (↑n : M) * x * x_1
rw₁ rw₂ : (↑n : M) * x * x_1 = (↑n : M) * x * x_1
⊢ (↑(↑n : ℤ) : M) * (x * x_1) = (↑(↑n : ℤ) : M) * x * x_1

Tactic:
rw [Int.cast_natCast, (natCast_mem_center _ n).left_assoc _ _]

Premises used: Int.cast_natCast, IsMulCentral.left_assoc, Set.natCast_mem_center
-- Module: Mathlib.Algebra.Ring.Center
Goal:
M : Type u_1
inst : NonAssocRing M
n_1 : ℤ
x x_1 : M
n : ℕ
rw : -(↑(n + 1) : M) * (x * x_1) = -(↑(n + 1) : M) * x * x_1
rw₁ : -HAdd.hAdd (α := M) (↑n : M) (↑1 : M) * (x * x_1) = -HAdd.hAdd (α := M) (↑n : M) (↑1 : M) * x * x_1
rw₂ : -HAdd.hAdd (α := M) (↑n : M) 1 * (x * x_1) = -HAdd.hAdd (α := M) (↑n : M) 1 * x * x_1
rw₃ : HAdd.hAdd (α := M) (-1) (-(↑n : M)) * (x * x_1) = HAdd.hAdd (α := M) (-1) (-(↑n : M)) * x * x_1
rw₄ : -1 * (x * x_1) + -(↑n : M) * (x * x_1) = HAdd.hAdd (α := M) (-1) (-(↑n : M)) * x * x_1
rw₅ : -1 * (x * x_1) + -(↑n : M) * (x * x_1) = (-1 * x + -(↑n : M) * x) * x_1
rw₆ : -1 * (x * x_1) + -(↑n : M) * (x * x_1) = -1 * x * x_1 + -(↑n : M) * x * x_1
rw₇ : -(1 * (x * x_1)) + -(↑n : M) * (x * x_1) = -1 * x * x_1 + -(↑n : M) * x * x_1
rw₈ : -(x * x_1) + -(↑n : M) * (x * x_1) = -1 * x * x_1 + -(↑n : M) * x * x_1
rw₉ : -(x * x_1) + -(↑n : M) * (x * x_1) = -(1 * x) * x_1 + -(↑n : M) * x * x_1
rw₁₀ : -(x * x_1) + -(↑n : M) * (x * x_1) = -x * x_1 + -(↑n : M) * x * x_1
rw₁₁ : -x * x_1 + -(↑n : M) * (x * x_1) = -x * x_1 + -(↑n : M) * x * x_1
rw₁₂ : -(↑n : M) * (x * x_1) = -(↑n : M) * x * x_1
rw₁₃ : -((↑n : M) * (x * x_1)) = -(↑n : M) * x * x_1
rw₁₄ : -((↑n : M) * x * x_1) = -(↑n : M) * x * x_1
rw₁₅ : -((↑n : M) * x * x_1) = -((↑n : M) * x) * x_1
rw₁₆ rw₁₇ : -((↑n : M) * x * x_1) = -((↑n : M) * x * x_1)
⊢ (↑(Int.negSucc n) : M) * (x * x_1) = (↑(Int.negSucc n) : M) * x * x_1

Tactic:
rw [Int.cast_negSucc, Nat.cast_add, Nat.cast_one, neg_add_rev, add_mul, add_mul, add_mul,
        neg_mul, one_mul, neg_mul 1, one_mul, ← neg_mul, add_right_inj, neg_mul,
        (natCast_mem_center _ n).left_assoc _ _, neg_mul, neg_mul]

Premises used: neg_add_rev, add_mul, Int.cast_negSucc, Nat.cast_add, IsMulCentral.left_assoc, neg_mul, OfNat.ofNat, Nat.cast_one, add_right_inj, Set.natCast_mem_center, one_mul
-- Module: Mathlib.Algebra.Ring.Center
Goal:
M : Type u_1
inst : NonAssocRing M
n_1 : ℤ
x x_1 : M
n : ℕ
rw : x * x_1 * (↑n : M) = x * (x_1 * (↑n : M))
rw₁ rw₂ : x * (x_1 * (↑n : M)) = x * (x_1 * (↑n : M))
⊢ x * x_1 * (↑(↑n : ℤ) : M) = x * (x_1 * (↑(↑n : ℤ) : M))

Tactic:
rw [Int.cast_natCast, (natCast_mem_center _ n).right_assoc _ _]

Premises used: Int.cast_natCast, IsMulCentral.right_assoc, Set.natCast_mem_center
-- Module: Mathlib.Algebra.Ring.Center
Goal:
M : Type u_1
inst : NonAssocRing M
n_1 : ℤ
x x_1 : M
n : ℕ
simp : x * x_1 * HAdd.hAdd (α := M) (-1) (-(↑n : M)) = x * (x_1 * HAdd.hAdd (α := M) (-1) (-(↑n : M)))
⊢ x * x_1 * (↑(Int.negSucc n) : M) = x * (x_1 * (↑(Int.negSucc n) : M))

Tactic:
simp only [Int.cast_negSucc, Nat.cast_add, Nat.cast_one, neg_add_rev]

Premises used: neg_add_rev, Int.cast_negSucc, Nat.cast_add, Nat.cast_one
-- Module: Mathlib.Algebra.Ring.Center
Goal:
M : Type u_1
inst : NonAssocRing M
n_1 : ℤ
x x_1 : M
n : ℕ
rw : x * x_1 * -1 + x * x_1 * -(↑n : M) = x * (x_1 * HAdd.hAdd (α := M) (-1) (-(↑n : M)))
rw₁ : x * x_1 * -1 + x * x_1 * -(↑n : M) = x * (x_1 * -1 + x_1 * -(↑n : M))
rw₂ : x * x_1 * -1 + x * x_1 * -(↑n : M) = x * (x_1 * -1) + x * (x_1 * -(↑n : M))
rw₃ : -(x * x_1 * 1) + x * x_1 * -(↑n : M) = x * (x_1 * -1) + x * (x_1 * -(↑n : M))
rw₄ : -(x * x_1) + x * x_1 * -(↑n : M) = x * (x_1 * -1) + x * (x_1 * -(↑n : M))
rw₅ : -(x * x_1) + -(x * x_1 * (↑n : M)) = x * (x_1 * -1) + x * (x_1 * -(↑n : M))
rw₆ : -(x * x_1) + -(x * x_1 * (↑n : M)) = x * -(x_1 * 1) + x * (x_1 * -(↑n : M))
rw₇ : -(x * x_1) + -(x * x_1 * (↑n : M)) = x * -x_1 + x * (x_1 * -(↑n : M))
rw₈ : -(x * x_1) + -(x * x_1 * (↑n : M)) = -(x * x_1) + x * (x_1 * -(↑n : M))
rw₉ : -(x * x_1 * (↑n : M)) = x * (x_1 * -(↑n : M))
rw₁₀ : -(x * (x_1 * (↑n : M))) = x * (x_1 * -(↑n : M))
rw₁₁ : -(x * (x_1 * (↑n : M))) = x * -(x_1 * (↑n : M))
rw₁₂ rw₁₃ : -(x * (x_1 * (↑n : M))) = -(x * (x_1 * (↑n : M)))
⊢ x * x_1 * HAdd.hAdd (α := M) (-1) (-(↑n : M)) = x * (x_1 * HAdd.hAdd (α := M) (-1) (-(↑n : M)))

Tactic:
rw [mul_add, mul_add, mul_add, mul_neg, mul_one, mul_neg, mul_neg, mul_one, mul_neg,
          add_right_inj, (natCast_mem_center _ n).right_assoc _ _, mul_neg, mul_neg]

Premises used: mul_add, IsMulCentral.right_assoc, mul_one, add_right_inj, Set.natCast_mem_center, mul_neg
-- Module: Mathlib.Algebra.Ring.Center
Goal:
M : Type u_1
inst : Distrib M
a b : M
ha : a ∈ center M
hb : b ∈ center M
x : M
rw : (a + b) * x = x * (a + b)
rw₁ : a * x + b * x = x * (a + b)
rw₂ : a * x + b * x = x * a + x * b
rw₃ : x * a + b * x = x * a + x * b
rw₄ rw₅ : x * a + x * b = x * a + x * b
⊢ Commute (a + b) x

Tactic:
rw [commute_iff_eq, add_mul, mul_add, ha.comm, hb.comm]

Premises used: add_mul, commute_iff_eq, IsMulCentral.comm, mul_add
-- Module: Mathlib.Algebra.Ring.Center
Goal:
M : Type u_1
inst : Distrib M
a b : M
ha : a ∈ center M
hb : b ∈ center M
x x_1 : M
rw : a * (x * x_1) + b * (x * x_1) = (a + b) * x * x_1
rw₁ : a * x * x_1 + b * (x * x_1) = (a + b) * x * x_1
rw₂ : a * x * x_1 + b * x * x_1 = (a + b) * x * x_1
rw₃ : (a * x + b * x) * x_1 = (a + b) * x * x_1
rw₄ rw₅ : (a + b) * x * x_1 = (a + b) * x * x_1
⊢ (a + b) * (x * x_1) = (a + b) * x * x_1

Tactic:
rw [add_mul, ha.left_assoc, hb.left_assoc, ← add_mul, ← add_mul]

Premises used: add_mul, IsMulCentral.left_assoc
-- Module: Mathlib.Algebra.Ring.Center
Goal:
M : Type u_1
inst : Distrib M
a b : M
ha : a ∈ center M
hb : b ∈ center M
x x_1 : M
rw : x * x_1 * a + x * x_1 * b = x * (x_1 * (a + b))
rw₁ : x * (x_1 * a) + x * x_1 * b = x * (x_1 * (a + b))
rw₂ : x * (x_1 * a) + x * (x_1 * b) = x * (x_1 * (a + b))
rw₃ : x * (x_1 * a + x_1 * b) = x * (x_1 * (a + b))
rw₄ rw₅ : x * (x_1 * (a + b)) = x * (x_1 * (a + b))
⊢ x * x_1 * (a + b) = x * (x_1 * (a + b))

Tactic:
rw [mul_add, ha.right_assoc, hb.right_assoc, ← mul_add, ← mul_add]

Premises used: mul_add, IsMulCentral.right_assoc
-- Module: Mathlib.Algebra.Ring.Center
Goal:
M : Type u_1
inst : NonUnitalNonAssocRing M
a : M
ha : a ∈ center M
x : M
rw : -a * x = x * -a
rw₁ : -a * x = -x * a
rw₂ : -a * x = a * -x
rw₃ rw₄ : a * -x = a * -x
⊢ Commute (-a) x

Tactic:
rw [commute_iff_eq, ← neg_mul_comm, ← ha.comm, neg_mul_comm]

Premises used: commute_iff_eq, IsMulCentral.comm, neg_mul_comm
-- Module: Mathlib.Algebra.Ring.Center
Goal:
M : Type u_1
inst : NonUnitalNonAssocRing M
a : M
ha : a ∈ center M
x x_1 : M
rw : -(a * (x * x_1)) = -a * x * x_1
rw₁ : -(a * x * x_1) = -a * x * x_1
rw₂ : -(a * x * x_1) = -(a * x) * x_1
rw₃ rw₄ : -(a * x * x_1) = -(a * x * x_1)
⊢ -a * (x * x_1) = -a * x * x_1

Tactic:
rw [neg_mul, ha.left_assoc, neg_mul, neg_mul]

Premises used: IsMulCentral.left_assoc, neg_mul
-- Module: Mathlib.Algebra.Ring.Center
Goal:
M : Type u_1
inst : NonUnitalNonAssocRing M
a : M
ha : a ∈ center M
x x_1 : M
rw : -(x * x_1 * a) = x * (x_1 * -a)
rw₁ : -(x * (x_1 * a)) = x * (x_1 * -a)
rw₂ : -(x * (x_1 * a)) = x * -(x_1 * a)
rw₃ rw₄ : -(x * (x_1 * a)) = -(x * (x_1 * a))
⊢ x * x_1 * -a = x * (x_1 * -a)

Tactic:
rw [mul_neg, ha.right_assoc, mul_neg, mul_neg]

Premises used: IsMulCentral.right_assoc, mul_neg
-- Module: Mathlib.Algebra.Ring.Centralizer
Goal:
M : Type u_1
S : Set M
a b : M
inst : Distrib M
ha : a ∈ S.centralizer
hb : b ∈ S.centralizer
c : M
hc : c ∈ S
rw : c * (a + b) = a * c + b * c
rw₁ : c * a + c * b = a * c + b * c
rw₂ : a * c + c * b = a * c + b * c
rw₃ rw₄ : a * c + b * c = a * c + b * c
⊢ c * (a + b) = (a + b) * c

Tactic:
rw [add_mul, mul_add, ha c hc, hb c hc]

Premises used: add_mul, mul_add
-- Module: Mathlib.Algebra.Ring.Centralizer
Goal:
M : Type u_1
S : Set M
a : M
inst : Mul M
inst_1 : HasDistribNeg M
ha : a ∈ S.centralizer
c : M
hc : c ∈ S
rw : -(c * a) = -a * c
rw₁ : -(a * c) = -a * c
rw₂ rw₃ : -(a * c) = -(a * c)
⊢ c * -a = -a * c

Tactic:
rw [mul_neg, ha c hc, neg_mul]

Premises used: neg_mul, mul_neg
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst : NonUnitalNonAssocSemiring α
f g : CentroidHom α
h :
  Eq.{u_5 + 1} (α := (a : α) → α) ((fun (f : CentroidHom α) ↦ (↑f.toAddMonoidHom : ZeroHom α α).toFun) f)
    ((fun (f : CentroidHom α) ↦ (↑f.toAddMonoidHom : ZeroHom α α).toFun) g)
mk :
  ∀ (toAddMonoidHom : α →+ α)
    (map_mul_left' :
      ∀ (a b : α), (↑toAddMonoidHom : ZeroHom α α).toFun (a * b) = a * (↑toAddMonoidHom : ZeroHom α α).toFun b)
    (map_mul_right' :
      ∀ (a b : α), (↑toAddMonoidHom : ZeroHom α α).toFun (a * b) = (↑toAddMonoidHom : ZeroHom α α).toFun a * b)
    (h :
      Eq.{u_5 + 1} (α := (a : α) → α)
        ((fun (f : CentroidHom α) ↦ (↑f.toAddMonoidHom : ZeroHom α α).toFun)
          { toAddMonoidHom := toAddMonoidHom, map_mul_left' := map_mul_left', map_mul_right' := map_mul_right' })
        ((fun (f : CentroidHom α) ↦ (↑f.toAddMonoidHom : ZeroHom α α).toFun) g)),
    { toAddMonoidHom := toAddMonoidHom, map_mul_left' := map_mul_left', map_mul_right' := map_mul_right' :
        CentroidHom α } =
      g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst : NonUnitalNonAssocSemiring α
g : CentroidHom α
toAddMonoidHom : α →+ α
map_mul_left' : ∀ (a b : α), (↑toAddMonoidHom : ZeroHom α α).toFun (a * b) = a * (↑toAddMonoidHom : ZeroHom α α).toFun b
map_mul_right' :
  ∀ (a b : α), (↑toAddMonoidHom : ZeroHom α α).toFun (a * b) = (↑toAddMonoidHom : ZeroHom α α).toFun a * b
h :
  Eq.{u_5 + 1} (α := (a : α) → α)
    ((fun (f : CentroidHom α) ↦ (↑f.toAddMonoidHom : ZeroHom α α).toFun)
      { toAddMonoidHom := toAddMonoidHom, map_mul_left' := map_mul_left', map_mul_right' := map_mul_right' })
    ((fun (f : CentroidHom α) ↦ (↑f.toAddMonoidHom : ZeroHom α α).toFun) g)
mk :
  ∀ (toAddMonoidHom_1 : α →+ α)
    (map_mul_left'_1 :
      ∀ (a b : α), (↑toAddMonoidHom_1 : ZeroHom α α).toFun (a * b) = a * (↑toAddMonoidHom_1 : ZeroHom α α).toFun b)
    (map_mul_right'_1 :
      ∀ (a b : α), (↑toAddMonoidHom_1 : ZeroHom α α).toFun (a * b) = (↑toAddMonoidHom_1 : ZeroHom α α).toFun a * b)
    (h :
      Eq.{u_5 + 1} (α := (a : α) → α)
        ((fun (f : CentroidHom α) ↦ (↑f.toAddMonoidHom : ZeroHom α α).toFun)
          { toAddMonoidHom := toAddMonoidHom, map_mul_left' := map_mul_left', map_mul_right' := map_mul_right' })
        ((fun (f : CentroidHom α) ↦ (↑f.toAddMonoidHom : ZeroHom α α).toFun)
          { toAddMonoidHom := toAddMonoidHom_1, map_mul_left' := map_mul_left'_1,
            map_mul_right' := map_mul_right'_1 })),
    { toAddMonoidHom := toAddMonoidHom, map_mul_left' := map_mul_left', map_mul_right' := map_mul_right' :
        CentroidHom α } =
      { toAddMonoidHom := toAddMonoidHom_1, map_mul_left' := map_mul_left'_1, map_mul_right' := map_mul_right'_1 }
⊢ { toAddMonoidHom := toAddMonoidHom, map_mul_left' := map_mul_left', map_mul_right' := map_mul_right' :
      CentroidHom α } =
    g

Tactic:
cases g
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst : NonUnitalNonAssocSemiring α
toAddMonoidHom : α →+ α
map_mul_left' : ∀ (a b : α), (↑toAddMonoidHom : ZeroHom α α).toFun (a * b) = a * (↑toAddMonoidHom : ZeroHom α α).toFun b
map_mul_right' :
  ∀ (a b : α), (↑toAddMonoidHom : ZeroHom α α).toFun (a * b) = (↑toAddMonoidHom : ZeroHom α α).toFun a * b
toAddMonoidHom_1 : α →+ α
map_mul_left'_1 :
  ∀ (a b : α), (↑toAddMonoidHom_1 : ZeroHom α α).toFun (a * b) = a * (↑toAddMonoidHom_1 : ZeroHom α α).toFun b
map_mul_right'_1 :
  ∀ (a b : α), (↑toAddMonoidHom_1 : ZeroHom α α).toFun (a * b) = (↑toAddMonoidHom_1 : ZeroHom α α).toFun a * b
h :
  Eq.{u_5 + 1} (α := (a : α) → α)
    ((fun (f : CentroidHom α) ↦ (↑f.toAddMonoidHom : ZeroHom α α).toFun)
      { toAddMonoidHom := toAddMonoidHom, map_mul_left' := map_mul_left', map_mul_right' := map_mul_right' })
    ((fun (f : CentroidHom α) ↦ (↑f.toAddMonoidHom : ZeroHom α α).toFun)
      { toAddMonoidHom := toAddMonoidHom_1, map_mul_left' := map_mul_left'_1, map_mul_right' := map_mul_right'_1 })
mk : ∀ (x : α), Eq (α := α) ((toAddMonoidHom : (a : α) → α) x : α) ((toAddMonoidHom_1 : (a : α) → α) x : α)
⊢ { toAddMonoidHom := toAddMonoidHom, map_mul_left' := map_mul_left', map_mul_right' := map_mul_right' :
      CentroidHom α } =
    { toAddMonoidHom := toAddMonoidHom_1, map_mul_left' := map_mul_left'_1, map_mul_right' := map_mul_right'_1 }

Tactic:
congr with x
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst : NonUnitalNonAssocSemiring α
toAddMonoidHom : α →+ α
map_mul_left' : ∀ (a b : α), (↑toAddMonoidHom : ZeroHom α α).toFun (a * b) = a * (↑toAddMonoidHom : ZeroHom α α).toFun b
map_mul_right' :
  ∀ (a b : α), (↑toAddMonoidHom : ZeroHom α α).toFun (a * b) = (↑toAddMonoidHom : ZeroHom α α).toFun a * b
toAddMonoidHom_1 : α →+ α
map_mul_left'_1 :
  ∀ (a b : α), (↑toAddMonoidHom_1 : ZeroHom α α).toFun (a * b) = a * (↑toAddMonoidHom_1 : ZeroHom α α).toFun b
map_mul_right'_1 :
  ∀ (a b : α), (↑toAddMonoidHom_1 : ZeroHom α α).toFun (a * b) = (↑toAddMonoidHom_1 : ZeroHom α α).toFun a * b
h :
  Eq.{u_5 + 1} (α := (a : α) → α)
    ((fun (f : CentroidHom α) ↦ (↑f.toAddMonoidHom : ZeroHom α α).toFun)
      { toAddMonoidHom := toAddMonoidHom, map_mul_left' := map_mul_left', map_mul_right' := map_mul_right' })
    ((fun (f : CentroidHom α) ↦ (↑f.toAddMonoidHom : ZeroHom α α).toFun)
      { toAddMonoidHom := toAddMonoidHom_1, map_mul_left' := map_mul_left'_1, map_mul_right' := map_mul_right'_1 })
x : α
⊢ Eq (α := α) ((toAddMonoidHom : (a : α) → α) x : α) ((toAddMonoidHom_1 : (a : α) → α) x : α)

Tactic:
congrFun h x

Premises used: congrFun
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst : NonUnitalNonAssocSemiring α
toAddMonoidHom : α →+ α
map_mul_left' : ∀ (a b : α), (↑toAddMonoidHom : ZeroHom α α).toFun (a * b) = a * (↑toAddMonoidHom : ZeroHom α α).toFun b
map_mul_right' :
  ∀ (a b : α), (↑toAddMonoidHom : ZeroHom α α).toFun (a * b) = (↑toAddMonoidHom : ZeroHom α α).toFun a * b
toAddMonoidHom_1 : α →+ α
map_mul_left'_1 :
  ∀ (a b : α), (↑toAddMonoidHom_1 : ZeroHom α α).toFun (a * b) = a * (↑toAddMonoidHom_1 : ZeroHom α α).toFun b
map_mul_right'_1 :
  ∀ (a b : α), (↑toAddMonoidHom_1 : ZeroHom α α).toFun (a * b) = (↑toAddMonoidHom_1 : ZeroHom α α).toFun a * b
h :
  Eq.{u_5 + 1} (α := (a : α) → α)
    ((fun (f : CentroidHom α) ↦ (↑f.toAddMonoidHom : ZeroHom α α).toFun)
      { toAddMonoidHom := toAddMonoidHom, map_mul_left' := map_mul_left', map_mul_right' := map_mul_right' })
    ((fun (f : CentroidHom α) ↦ (↑f.toAddMonoidHom : ZeroHom α α).toFun)
      { toAddMonoidHom := toAddMonoidHom_1, map_mul_left' := map_mul_left'_1, map_mul_right' := map_mul_right'_1 })
x : α
⊢ Eq (α := α) ((toAddMonoidHom : (a : α) → α) x : α) ((toAddMonoidHom_1 : (a : α) → α) x : α)

Tactic:
exact congrFun h x

Premises used: congrFun
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
f : CentroidHom α
⊢ (↑f.toAddMonoidHom : ZeroHom α α).toFun = (⇑f : (a : α) → α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
f g : CentroidHom α
h : ∀ (a : α), Eq (α := α) ((f : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
⊢ f = g

Tactic:
DFunLike.ext f g h

Premises used: DFunLike.ext
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
f : CentroidHom α
⊢ Eq (α := (a : α) → α) (⇑(↑f : α →+ α) : (a : α) → α) (⇑f : (a : α) → α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
f : CentroidHom α
⊢ f.toAddMonoidHom = (↑f : α →+ α)

Tactic:
rfl

Premises used: AddMonoidHomClass.toAddMonoidHom, rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
⊢ Injective (α := CentroidHom α) (β := α →+ α) AddMonoidHomClass.toAddMonoidHom

Tactic:
fun _f _g h => ext fun a ↦
    haveI := DFunLike.congr_fun h a
    this

Premises used: CentroidHom.ext, DFunLike.congr_fun, Function.Injective
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
⊢ Injective.{u_5 + 1, u_5 + 1} (α := CentroidHom α) toEnd

Tactic:
coe_toAddMonoidHom_injective

Premises used: CentroidHom.coe_toAddMonoidHom_injective, AddMonoid.End, CentroidHom.toEnd
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst : NonUnitalNonAssocSemiring α
f : CentroidHom α
f' : α → α
h : f' = (⇑f : (a : α) → α)
a b : α
simp_rw : (f : (a : α) → α) (a * b) = HMul.hMul (β := α) a ((f : (a : α) → α) b : α)
⊢ f' (a * b) = a * f' b

Tactic:
simp_rw [h, map_mul_left]

Premises used: CentroidHomClass.map_mul_left