awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
a : α
hc :
  Eq (α := AddMonoid.End α) ((R : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
    ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
T : CentroidHom α
hT :
  Eq (α := AddMonoid.End α) ((toEndRingHom α : (a : CentroidHom α) → AddMonoid.End α) T : AddMonoid.End α)
    ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
e1 : ∀ (d : α), (T : (a : α) → α) d = a * d
e2 : ∀ (d : α), (T : (a : α) → α) d = d * a
⊢ ∀ (a_1 b : α), a_1 * b * a = a_1 * (b * a)

Tactic:
simpa [e2] using (map_mul_left T · ·)

Premises used: CentroidHomClass.map_mul_left
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
a : α
hc :
  Eq (α := AddMonoid.End α) ((R : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
    ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
T : CentroidHom α
hT :
  Eq (α := AddMonoid.End α) ((toEndRingHom α : (a : CentroidHom α) → AddMonoid.End α) T : AddMonoid.End α)
    ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
e1 : ∀ (d : α), (T : (a : α) → α) d = a * d
e2 : ∀ (d : α), (T : (a : α) → α) d = d * a
⊢ ∀ (a_1 b : α), a_1 * b * a = a_1 * (b * a)

Tactic:
case right_assoc => simpa [e2] using (map_mul_left T · ·)

Premises used: CentroidHomClass.map_mul_left
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocCommSemiring α
a : α
rw :
  (Eq (α := AddMonoid.End α) ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
        ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α) ∧
      ∀ (g : AddMonoid.End α),
        Membership.mem (γ := Set (AddMonoid.End α)) (Set.range (ι := α) (⇑L : (a : α) → AddMonoid.End α)) g →
          HMul.hMul (β := AddMonoid.End α) g ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α) =
            HMul.hMul (α := AddMonoid.End α) ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α) g) ↔
    ∀ (b : α),
      Commute (S := AddMonoid.End α) ((L : (a : α) → AddMonoid.End α) b : AddMonoid.End α)
        ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
⊢ Membership.mem (γ := NonUnitalSubsemiring α) (NonUnitalSubsemiring.center α) a ↔
    ∀ (b : α),
      Commute (S := AddMonoid.End α) ((L : (a : α) → AddMonoid.End α) b : AddMonoid.End α)
        ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α)

Tactic:
rw [NonUnitalNonAssocSemiring.mem_center_iff, CentroidHom.centroid_eq_centralizer_mulLeftRight,
    Subsemiring.mem_centralizer_iff, AddMonoid.End.mulRight_eq_mulLeft, Set.union_self]

Premises used: AddMonoid.End.mulRight_eq_mulLeft, CentroidHom.centroid_eq_centralizer_mulLeftRight, Subsemiring.mem_centralizer_iff, NonUnitalNonAssocSemiring.mem_center_iff, Set.union_self
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocCommSemiring α
a : α
⊢ (Eq (α := AddMonoid.End α) ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
        ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α) ∧
      ∀ (g : AddMonoid.End α),
        Membership.mem (γ := Set (AddMonoid.End α)) (Set.range (ι := α) (⇑L : (a : α) → AddMonoid.End α)) g →
          HMul.hMul (β := AddMonoid.End α) g ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α) =
            HMul.hMul (α := AddMonoid.End α) ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α) g) ↔
    ∀ (b : α),
      Commute (S := AddMonoid.End α) ((L : (a : α) → AddMonoid.End α) b : AddMonoid.End α)
        ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α)

Tactic:
aesop
-- 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 : NonAssocSemiring α
T : CentroidHom α
comm : ∀ (a : α), Commute ((T : (a : α) → α) 1) a
left_assoc :
  ∀ (b c : α), HMul.hMul (α := α) ((T : (a : α) → α) 1 : α) (b * c) = HMul.hMul (α := α) ((T : (a : α) → α) 1 : α) b * c
right_assoc :
  ∀ (a b : α), HMul.hMul (β := α) (a * b) ((T : (a : α) → α) 1 : α) = a * HMul.hMul (β := α) b ((T : (a : α) → α) 1 : α)
⊢ Membership.mem (α := α) (γ := Subsemiring α) (Subsemiring.center α) ((T : (a : α) → α) 1 : α)

Tactic:
constructor
-- 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 : NonAssocSemiring α
T : CentroidHom α
⊢ ∀ (a : α), Commute ((T : (a : α) → α) 1) a

Tactic:
simp [commute_iff_eq, ← map_mul_left, ← map_mul_right]

Premises used: commute_iff_eq, CentroidHomClass.map_mul_left, CentroidHomClass.map_mul_right
-- 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 : NonAssocSemiring α
T : CentroidHom α
⊢ ∀ (b c : α), HMul.hMul (α := α) ((T : (a : α) → α) 1 : α) (b * c) = HMul.hMul (α := α) ((T : (a : α) → α) 1 : α) b * c

Tactic:
simp [commute_iff_eq, ← map_mul_left, ← map_mul_right]

Premises used: commute_iff_eq, CentroidHomClass.map_mul_left, CentroidHomClass.map_mul_right
-- 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 : NonAssocSemiring α
T : CentroidHom α
⊢ ∀ (a b : α), HMul.hMul (β := α) (a * b) ((T : (a : α) → α) 1 : α) = a * HMul.hMul (β := α) b ((T : (a : α) → α) 1 : α)

Tactic:
simp [commute_iff_eq, ← map_mul_left, ← map_mul_right]

Premises used: commute_iff_eq, CentroidHomClass.map_mul_left, CentroidHomClass.map_mul_right
-- 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 : NonAssocSemiring α
z : ↥(Subsemiring.center α)
⊢ (↑((fun (T : CentroidHom α) ↦
            (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Subsemiring α) (Subsemiring.center α) x)
                ((T : (a : α) → α) 1) ⋯ :
              ↥(Subsemiring.center α)))
          (MulHom.toFun (NonUnitalRingHom.toMulHom centerToCentroid) z)) :
      α) =
    (↑z : α)

Tactic:
simp only [MulHom.toFun_eq_coe,
      NonUnitalRingHom.coe_toMulHom, centerToCentroid_apply, mul_one]

Premises used: MulHom.toFun_eq_coe, CentroidHom.centerToCentroid_apply, mul_one, NonUnitalRingHom.coe_toMulHom
-- 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 : NonAssocSemiring α
T : CentroidHom α
x : α
rw :
  Eq (α := α)
    (((NonUnitalRingHom.toMulHom centerToCentroid : (a : ↥(NonUnitalSubsemiring.center α)) → CentroidHom α)
            ((fun (T : CentroidHom α) ↦
                (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Subsemiring α) (Subsemiring.center α) x)
                    ((T : (a : α) → α) 1) ⋯ :
                  ↥(Subsemiring.center α)))
              T) :
          (a : α) → α)
        x :
      α)
    ((T : (a : α) → α) x : α)
rw₁ :
  Eq (α := α)
    (((centerToCentroid : (a : ↥(NonUnitalSubsemiring.center α)) → CentroidHom α)
            ((fun (T : CentroidHom α) ↦
                (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Subsemiring α) (Subsemiring.center α) x)
                    ((T : (a : α) → α) 1) ⋯ :
                  ↥(Subsemiring.center α)))
              T) :
          (a : α) → α)
        x :
      α)
    ((T : (a : α) → α) x : α)
rw₂ :
  (↑((fun (T : CentroidHom α) ↦
              (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Subsemiring α) (Subsemiring.center α) x)
                  ((T : (a : α) → α) 1) ⋯ :
                ↥(Subsemiring.center α)))
            T) :
        α) *
      x =
    (T : (a : α) → α) x
rw₃ : Eq (α := α) ((T : (a : α) → α) (1 * x) : α) ((T : (a : α) → α) x : α)
rw₄ rw₅ : Eq (α := α) ((T : (a : α) → α) x : α) ((T : (a : α) → α) x : α)
⊢ Eq (α := α)
    ((MulHom.toFun (NonUnitalRingHom.toMulHom centerToCentroid)
            ((fun (T : CentroidHom α) ↦
                (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Subsemiring α) (Subsemiring.center α) x)
                    ((T : (a : α) → α) 1) ⋯ :
                  ↥(Subsemiring.center α)))
              T) :
          (a : α) → α)
        x :
      α)
    ((T : (a : α) → α) x : α)

Tactic:
rw [MulHom.toFun_eq_coe,
      NonUnitalRingHom.coe_toMulHom, centerToCentroid_apply, ← map_mul_right, one_mul]

Premises used: MulHom.toFun_eq_coe, CentroidHom.centerToCentroid_apply, CentroidHomClass.map_mul_right, NonUnitalRingHom.coe_toMulHom, one_mul
-- 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 : NonUnitalNonAssocRing α
f : CentroidHom α
a b : α
⊢ ZeroHom.toFun (↑(-(↑f : α →+ α)) : ZeroHom α α) (a * b) = a * ZeroHom.toFun (↑(-(↑f : α →+ α)) : ZeroHom α α) b

Tactic:
simp [map_mul_left]

Premises used: CentroidHomClass.map_mul_left
-- 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 : NonUnitalNonAssocRing α
f : CentroidHom α
a b : α
⊢ ZeroHom.toFun (↑(-(↑f : α →+ α)) : ZeroHom α α) (a * b) = ZeroHom.toFun (↑(-(↑f : α →+ α)) : ZeroHom α α) a * b

Tactic:
simp [map_mul_right]

Premises used: CentroidHomClass.map_mul_right
-- 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 : NonUnitalNonAssocRing α
f g : CentroidHom α
a b : α
⊢ (↑(HSub.hSub (α := α →+ α) (↑f : α →+ α) (↑g : α →+ α)) : ZeroHom α α).toFun (a * b) =
    a * (↑(HSub.hSub (α := α →+ α) (↑f : α →+ α) (↑g : α →+ α)) : ZeroHom α α).toFun b

Tactic:
simp [map_mul_left, mul_sub]

Premises used: mul_sub, CentroidHomClass.map_mul_left
-- 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 : NonUnitalNonAssocRing α
f g : CentroidHom α
a b : α
⊢ (↑(HSub.hSub (α := α →+ α) (↑f : α →+ α) (↑g : α →+ α)) : ZeroHom α α).toFun (a * b) =
    (↑(HSub.hSub (α := α →+ α) (↑f : α →+ α) (↑g : α →+ α)) : ZeroHom α α).toFun a * b

Tactic:
simp [map_mul_right, sub_mul]

Premises used: sub_mul, CentroidHomClass.map_mul_right
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocRing α
z : ℤ
⊢ (⇑(↑z : CentroidHom α) : (a : α) → α) = HSMul.hSMul (β := (a : α) → α) z (⇑(CentroidHom.id α) : (a : α) → α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocRing α
z : ℤ
m : α
⊢ ((↑z : CentroidHom α) : (a : α) → α) m = z • m

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocRing α
x : CentroidHom α
⊢ (-x).toEnd = -x.toEnd

Tactic:
rfl

Premises used: AddMonoidHomClass.toAddMonoidHom, AddMonoidHom.mk', CentroidHom.toEnd, rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocRing α
x y : CentroidHom α
⊢ (x - y).toEnd = x.toEnd - y.toEnd

Tactic:
rfl

Premises used: AddMonoidHomClass.toAddMonoidHom, AddMonoidHom.mk', CentroidHom.toEnd, rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocRing α
f : CentroidHom α
⊢ Eq (α := (a : α) → α) (⇑(-f) : (a : α) → α) (-(⇑f : (a : α) → α))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocRing α
f g : CentroidHom α
⊢ (⇑(f - g) : (a : α) → α) = HSub.hSub (α := (a : α) → α) (⇑f : (a : α) → α) (⇑g : (a : α) → α)

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocRing α
f g : CentroidHom α
a : α
⊢ (f - g : (a : α) → α) a = HSub.hSub (α := α) (β := α) ((f : (a : α) → α) a : α) ((g : (a : α) → α) a : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocRing α
z : ℤ
⊢ Eq.{u_5 + 1} (α := AddMonoid.End α) (toEnd (↑z : CentroidHom α)) (↑z : AddMonoid.End α)

Tactic:
rfl

Premises used: AddMonoidHomClass.toAddMonoidHom, CentroidHom.toEnd, rfl
-- 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 : NonUnitalRing α
h : ∀ (a b : α), (∀ (r : α), a * r * b = 0) → a = 0 ∨ b = 0
f g : CentroidHom α
h₁ : ∀ (a : α), Eq (α := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α)
⊢ f * g = g * f

Tactic:
ext
-- 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 : NonUnitalRing α
h : ∀ (a b : α), (∀ (r : α), a * r * b = 0) → a = 0 ∨ b = 0
f g : CentroidHom α
a : α
⊢ Eq (α := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α)

Tactic:
sub_eq_zero.1 (or_self_iff.1 <| (h _ _) fun r ↦ ?_)

Premises used: sub_eq_zero, or_self_iff, Iff.mp
-- 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 : NonUnitalRing α
h : ∀ (a b : α), (∀ (r : α), a * r * b = 0) → a = 0 ∨ b = 0
f g : CentroidHom α
a : α
h₁ :
  ∀ (r : α),
    HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α) * r *
        HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α) =
      0
⊢ Eq (α := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α)

Tactic:
refine sub_eq_zero.1 (or_self_iff.1 <| (h _ _) fun r ↦ ?_)

Premises used: sub_eq_zero, or_self_iff, Iff.mp
-- Module: Mathlib.Algebra.Ring.CharZero
Goal:
α : Type u_1
R : Type u_2
S : Type u_3
n : ℕ
inst : AddMonoidWithOne R
inst_1 : CharZero R
rw : Ne (α := ℕ) 2 0
⊢ Ne.{u_2 + 1} (α := R) 2 0

Tactic:
rw [← Nat.cast_two, Nat.cast_ne_zero]

Premises used: Nat.cast_two, Nat.cast_ne_zero
-- Module: Mathlib.Algebra.Ring.CharZero
Goal:
α : Type u_1
R : Type u_2
S : Type u_3
n : ℕ
inst : AddMonoidWithOne R
inst_1 : CharZero R
⊢ Ne (α := ℕ) 2 0

Tactic:
decide
-- Module: Mathlib.Algebra.Ring.CharZero
Goal:
α : Type u_1
R : Type u_2
n : ℕ
inst : AddMonoidWithOne R
inst_1 : CharZero R
hn : n ≠ 0
⊢ Eq.{u_1 + 1} (α := Set α) (support.{u_1, u_2} (M := R) (↑n : α → R)) univ

Tactic:
support_const <| Nat.cast_ne_zero.2 hn

Premises used: Iff.mpr, Function.support_const, Nat.cast_ne_zero
-- Module: Mathlib.Algebra.Ring.CharZero
Goal:
α : Type u_1
R : Type u_2
n : ℕ
inst : AddMonoidWithOne R
inst_1 : CharZero R
hn : n ≠ 1
⊢ Eq.{u_1 + 1} (α := Set α) (mulSupport.{u_1, u_2} (M := R) (↑n : α → R)) univ

Tactic:
mulSupport_const <| Nat.cast_ne_one.2 hn

Premises used: Iff.mpr, Nat.cast_ne_one, Function.mulSupport_const
-- Module: Mathlib.Algebra.Ring.CharZero
Goal:
R : Type u_2
S : Type u_3
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
ϕ : R →+* S
inst_2 : CharZero S
a b : ℕ
h : Eq.{u_2 + 1} (α := R) (↑a : R) (↑b : R)
rw : Eq.{u_3 + 1} (α := S) ((ϕ : (a : R) → S) (↑a : R) : S) ((↑b : S) : S)
rw₁ : Eq.{u_3 + 1} (α := S) ((ϕ : (a : R) → S) (↑a : R) : S) ((ϕ : (a : R) → S) (↑b : R) : S)
rw₂ rw₃ : Eq.{u_3 + 1} (α := S) ((ϕ : (a : R) → S) (↑b : R) : S) ((ϕ : (a : R) → S) (↑b : R) : S)
⊢ Eq.{u_3 + 1} (α := S) (↑a : S) (↑b : S)

Tactic:
rw [← map_natCast ϕ, ← map_natCast ϕ, h]

Premises used: map_natCast
-- Module: Mathlib.Algebra.Ring.CharZero
Goal:
R : Type u_2
S : Type u_3
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
ϕ : R →+* S
hϕ : Injective.{u_2 + 1, u_3 + 1} (α := R) (β := S) (⇑ϕ : (a : R) → S)
hR : CharZero R
a b : ℕ
h : Eq.{u_3 + 1} (α := S) (↑a : S) (↑b : S)
rwa : Eq.{u_2 + 1} (α := R) (↑a : R) (↑b : R)
rwa₁ : Eq.{u_3 + 1} (α := S) ((ϕ : (a : R) → S) (↑a : R) : S) ((ϕ : (a : R) → S) (↑b : R) : S)
rwa₂ : Eq.{u_3 + 1} (α := S) ((↑a : S) : S) ((ϕ : (a : R) → S) (↑b : R) : S)
rwa₃ rwa₄ rwa₅ rwa₆ : Eq.{u_3 + 1} (α := S) (↑a : S) (↑b : S)
⊢ a = b

Tactic:
rwa [← @Nat.cast_inj R, ← hϕ.eq_iff, map_natCast ϕ, map_natCast ϕ]

Premises used: Function.Injective.eq_iff, Nat.cast_inj, map_natCast
-- Module: Mathlib.Algebra.Ring.CharZero
Goal:
R : Type u_2
inst : NonAssocSemiring R
f : ℕ →+* R
inst_1 : CharZero R
⊢ Injective (α := ℕ) (β := R) (⇑f : (a : ℕ) → R)

Tactic:
Subsingleton.elim (Nat.castRingHom _) f ▸ Nat.cast_injective

Premises used: Eq.rec, Nat.castRingHom, Subsingleton.elim, Nat.cast_injective
-- Module: Mathlib.Algebra.Ring.CharZero
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
a : R
⊢ a + a = 0 ↔ a = 0

Tactic:
simp only [(two_mul a).symm, mul_eq_zero, two_ne_zero, false_or]

Premises used: two_mul, false_or, mul_eq_zero, two_ne_zero, Eq.symm
-- Module: Mathlib.Algebra.Ring.CharZero
Goal:
R : Type u_2
n : ℕ
inst : Semiring R
inst_1 : CharZero R
a : ℕ
hn : n ≠ 0
⊢ HPow.hPow (α := R) (↑a : R) n = 1 ↔ a = 1

Tactic:
simp [← cast_pow, cast_eq_one, hn]

Premises used: Nat.cast_eq_one, Nat.cast_pow
-- Module: Mathlib.Algebra.Ring.CharZero
Goal:
α : Type u_1
R : Type u_2
S : Type u_3
n_1 : ℕ
inst : Semiring R
inst_1 : CharZero R
inst_2 : IsCancelMulZero R
n : ℕ
hn : n ≠ 0
a b : R
hab : Eq.{u_2 + 1} (α := R) ((fun (a : R) ↦ n • a) a) ((fun (a : R) ↦ n • a) b)
⊢ a = b

Tactic:
simpa [hn] using hab
-- Module: Mathlib.Algebra.Ring.CharZero
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
a : R
⊢ -a = a ↔ a = 0

Tactic:
neg_eq_iff_add_eq_zero.trans add_self_eq_zero

Premises used: neg_eq_iff_add_eq_zero, add_self_eq_zero, Iff.trans
-- Module: Mathlib.Algebra.Ring.CharZero
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
a : R
⊢ a = -a ↔ a = 0

Tactic:
eq_neg_iff_add_eq_zero.trans add_self_eq_zero

Premises used: add_self_eq_zero, Iff.trans, eq_neg_iff_add_eq_zero
-- Module: Mathlib.Algebra.Ring.CharZero
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
n : ℕ
a b : R
h : (↑n : R) * a = (↑n : R) * b
⊢ Eq.{u_2 + 1} (α := R) (↑n : R) 0 ∨ a = b

Tactic:
rw [← sub_eq_zero, ← mul_sub, mul_eq_zero, sub_eq_zero] at h

Premises used: mul_sub, sub_eq_zero, mul_eq_zero
-- Module: Mathlib.Algebra.Ring.CharZero
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
n : ℕ
a b : R
h : Eq.{u_2 + 1} (α := R) (↑n : R) 0 ∨ a = b
⊢ n = 0 ∨ a = b

Tactic:
mod_cast h

Premises used: congrArg, cast, Nat.cast, Nat.cast_inj._simp_1, congrFun', Or, Nat.cast_zero, Eq.symm, Eq, Eq.trans
-- Module: Mathlib.Algebra.Ring.CharZero
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
n : ℕ
a b : R
h : Eq.{u_2 + 1} (α := R) (↑n : R) 0 ∨ a = b
⊢ n = 0 ∨ a = b

Tactic:
exact mod_cast h
-- Module: Mathlib.Algebra.Ring.CharZero
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
n : ℕ
a b : R
h : (↑n : R) * a = (↑n : R) * b
w : n ≠ 0
⊢ a = b

Tactic:
simpa [w] using nat_mul_inj h

Premises used: nat_mul_inj
-- Module: Mathlib.Algebra.Ring.CharZero
Goal:
R : Type u_2
inst : Ring R
inst_1 : CharZero R
u : Rˣ
simp_rw : ¬u = -u
simp_rw₁ : ¬(↑u : R) = (↑(-u) : R)
simp_rw₂ : ¬(↑u : R) = -(↑u : R)
simp_rw₃ : ¬(↑u : R) + (↑u : R) = 0
simp_rw₄ : ¬2 * (↑u : R) = 0
simp_rw₅ : ¬Eq.{u_2 + 1} (α := R) 2 0
simp_rw₆ : ¬False
⊢ u ≠ -u

Tactic:
simp_rw [ne_eq, Units.ext_iff, Units.val_neg, eq_neg_iff_add_eq_zero, ← two_mul,
    Units.mul_left_eq_zero, two_ne_zero, not_false_iff]

Premises used: Units.ext_iff, two_mul, ne_eq, Units.val_neg, two_ne_zero, eq_neg_iff_add_eq_zero, not_false_iff, Units.mul_left_eq_zero
-- Module: Mathlib.Algebra.Ring.CharZero
Goal:
R : Type u_2
inst : Ring R
inst_1 : CharZero R
u : Rˣ
⊢ -u ≠ u

Tactic:
(units_ne_neg_self u).symm

Premises used: units_ne_neg_self, Ne.symm
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : Distrib R
a b c : R
⊢ Commute a b → Commute a c → Commute a (b + c)

Tactic:
SemiconjBy.add_right

Premises used: Commute, SemiconjBy.add_right
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : Distrib R
a b c : R
⊢ Commute a c → Commute b c → Commute (a + b) c

Tactic:
SemiconjBy.add_left

Premises used: Commute, SemiconjBy.add_left
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
a b : R
h : Commute a b
rw : a * a - b * b = a * (a - b) + b * (a - b)
rw₁ : a * a - b * b = a * a - a * b + b * (a - b)
rw₂ : a * a - b * b = a * a - a * b + (b * a - b * b)
rw₃ : a * a - b * b = a * a - b * a + (b * a - b * b)
rw₄ rw₅ : a * a - b * b = a * a - b * b
⊢ a * a - b * b = (a + b) * (a - b)

Tactic:
rw [add_mul, mul_sub, mul_sub, h.eq, sub_add_sub_cancel]

Premises used: add_mul, sub_add_sub_cancel, mul_sub, Commute.eq
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
a b : R
h : Commute a b
rw : a * a - b * b = (a - b) * a + (a - b) * b
rw₁ : a * a - b * b = a * a - b * a + (a - b) * b
rw₂ : a * a - b * b = a * a - b * a + (a * b - b * b)
rw₃ : a * a - b * b = a * a - b * a + (b * a - b * b)
rw₄ rw₅ : a * a - b * b = a * a - b * b
⊢ a * a - b * b = (a - b) * (a + b)

Tactic:
rw [mul_add, sub_mul, sub_mul, h.eq, sub_add_sub_cancel]

Premises used: sub_add_sub_cancel, sub_mul, mul_add, Commute.eq
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
inst_1 : NoZeroDivisors R
a b : R
h : Commute a b
rw : a * a - b * b = 0 ↔ a = b ∨ a = -b
rw₁ : (a + b) * (a - b) = 0 ↔ a = b ∨ a = -b
rw₂ : a + b = 0 ∨ a - b = 0 ↔ a = b ∨ a = -b
rw₃ : a - b = 0 ∨ a + b = 0 ↔ a = b ∨ a = -b
rw₄ : a = b ∨ a + b = 0 ↔ a = b ∨ a = -b
rw₅ rw₆ : a = b ∨ a = -b ↔ a = b ∨ a = -b
⊢ a * a = b * b ↔ a = b ∨ a = -b

Tactic:
rw [← sub_eq_zero, h.mul_self_sub_mul_self_eq, mul_eq_zero, or_comm, sub_eq_zero,
    add_eq_zero_iff_eq_neg]

Premises used: sub_eq_zero, add_eq_zero_iff_eq_neg, mul_eq_zero, Commute.mul_self_sub_mul_self_eq, or_comm
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : Mul R
inst_1 : HasDistribNeg R
a b : R
⊢ Commute a b → Commute a (-b)

Tactic:
SemiconjBy.neg_right

Premises used: Commute, SemiconjBy.neg_right
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : Mul R
inst_1 : HasDistribNeg R
a b : R
⊢ Commute a (-b) ↔ Commute a b

Tactic:
SemiconjBy.neg_right_iff

Premises used: Commute, SemiconjBy.neg_right_iff
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : Mul R
inst_1 : HasDistribNeg R
a b : R
⊢ Commute a b → Commute (-a) b

Tactic:
SemiconjBy.neg_left

Premises used: Commute, SemiconjBy.neg_left
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : Mul R
inst_1 : HasDistribNeg R
a b : R
⊢ Commute (-a) b ↔ Commute a b

Tactic:
SemiconjBy.neg_left_iff

Premises used: Commute, SemiconjBy.neg_left_iff
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : MulOneClass R
inst_1 : HasDistribNeg R
a : R
⊢ Commute a (-1)

Tactic:
SemiconjBy.neg_one_right a

Premises used: Commute, SemiconjBy.neg_one_right
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : MulOneClass R
inst_1 : HasDistribNeg R
a : R
⊢ Commute (-1) a

Tactic:
SemiconjBy.neg_one_left a

Premises used: Commute, SemiconjBy.neg_one_left
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
a b c : R
⊢ Commute a b → Commute a c → Commute a (b - c)

Tactic:
SemiconjBy.sub_right

Premises used: Commute, SemiconjBy.sub_right
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : NonUnitalNonAssocRing R
a b c : R
⊢ Commute a c → Commute b c → Commute (a - b) c

Tactic:
SemiconjBy.sub_left

Premises used: Commute, SemiconjBy.sub_left
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : Semiring R
a b : R
h : Commute a b
⊢ HPow.hPow (β := ℕ) (a + b) 2 = HPow.hPow (β := ℕ) a 2 + 2 * a * b + HPow.hPow (β := ℕ) b 2

Tactic:
simp [sq, add_mul, mul_add, two_mul, h.eq, add_assoc]

Premises used: add_mul, add_assoc, two_mul, sq, mul_add, Commute.eq
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : Ring R
a b : R
h : Commute a b
rw : a * a - HPow.hPow (β := ℕ) b 2 = (a + b) * (a - b)
rw₁ : a * a - b * b = (a + b) * (a - b)
rw₂ rw₃ : (a + b) * (a - b) = (a + b) * (a - b)
⊢ HPow.hPow (β := ℕ) a 2 - HPow.hPow (β := ℕ) b 2 = (a + b) * (a - b)

Tactic:
rw [sq, sq, h.mul_self_sub_mul_self_eq]

Premises used: sq, Commute.mul_self_sub_mul_self_eq
-- Module: Mathlib.Algebra.Ring.Commute
Goal:
R : Type u
inst : Ring R
a b : R
h : Commute a b
⊢ HPow.hPow (β := ℕ) (a - b) 2 = HPow.hPow (β := ℕ) a 2 - 2 * a * b + HPow.hPow (β := ℕ) b 2

Tactic:
simp [sq, add_mul, sub_mul, mul_sub, two_mul, h.eq, ← sub_add, ← sub_sub]

Premises used: sub_add, add_mul, mul_sub, two_mul, sq, sub_mul, sub_sub, Commute.eq