awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.Aut
Goal:
R : Type u_1
inst : Mul R
inst_1 : Add R
⊢ Eq (α := R ≃+* R) 1 (RingEquiv.refl R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Aut
Goal:
R : Type u_1
inst : Mul R
inst_1 : Add R
x : R
⊢ (1 : (a : R) → R) x = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Aut
Goal:
R : Type u_1
inst : Mul R
inst_1 : Add R
⊢ Eq.{u_1 + 1} (α := (a : R) → R) (⇑1 : (a : R) → R) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Aut
Goal:
R : Type u_1
inst : Mul R
inst_1 : Add R
f g : R ≃+* R
x : R
⊢ Eq (α := R) ((f * g : (a : R) → R) x : R) ((f : (a : R) → R) ((g : (a : R) → R) x : R) : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Aut
Goal:
R : Type u_1
inst : Mul R
inst_1 : Add R
f : R ≃+* R
x : R
⊢ Eq (α := R) ((f⁻¹ : (a : R) → R) x : R) ((f.symm : (a : R) → R) x : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Aut
Goal:
R : Type u_1
inst : Mul R
inst_1 : Add R
f : R ≃+* R
⊢ Eq (α := (a : R) → R) (⇑(HPow.hPow (β := ℕ) f 0) : (a : R) → R) (⇑f : (a : R) → R)^[0]

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Aut
Goal:
R : Type u_1
inst : Mul R
inst_1 : Add R
f : R ≃+* R
n : ℕ
ih : Eq (α := (a : R) → R) (⇑(f ^ n) : (a : R) → R) (⇑f : (a : R) → R)^[n]
succ : ∀ (x : R), (f ^ (n + 1) : (a : R) → R) x = (⇑f : (a : R) → R)^[n + 1] x
⊢ Eq (α := (a : R) → R) (⇑(f ^ (n + 1)) : (a : R) → R) (⇑f : (a : R) → R)^[n + 1]

Tactic:
ext
-- Module: Mathlib.Algebra.Ring.Aut
Goal:
R : Type u_1
inst : Mul R
inst_1 : Add R
f : R ≃+* R
n : ℕ
ih : Eq (α := (a : R) → R) (⇑(f ^ n) : (a : R) → R) (⇑f : (a : R) → R)^[n]
x : R
⊢ (f ^ (n + 1) : (a : R) → R) x = (⇑f : (a : R) → R)^[n + 1] x

Tactic:
simp [pow_succ, ih]

Premises used: pow_succ
-- Module: Mathlib.Algebra.Ring.Aut
Goal:
R : Type u_1
inst : Mul R
inst_1 : Add R
f : R ≃+* R
n : ℕ
zero : Eq (α := (a : R) → R) (⇑(HPow.hPow (β := ℕ) f 0) : (a : R) → R) (⇑f : (a : R) → R)^[0]
succ :
  ∀ (n : ℕ) (ih : Eq (α := (a : R) → R) (⇑(f ^ n) : (a : R) → R) (⇑f : (a : R) → R)^[n]),
    Eq (α := (a : R) → R) (⇑(f ^ (n + 1)) : (a : R) → R) (⇑f : (a : R) → R)^[n + 1]
⊢ Eq (α := (a : R) → R) (⇑(f ^ n) : (a : R) → R) (⇑f : (a : R) → R)^[n]

Tactic:
induction n with
  | zero =>
    simp
  | succ n ih =>
    ext
    simp [pow_succ, ih]

Premises used: pow_succ
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
r : R
⊢ Eq (α := (a : R) → R) (⇑(mulLeft r) : (a : R) → R) (HMul.hMul r)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
r : R
⊢ Eq (α := (a : R) → R) (⇑(mulRight r) : (a : R) → R) fun (x : R) ↦ x * r

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
a r : R
⊢ (mulRight r : (a : R) → R) a = a * r

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
x y : R
⊢ (((mul : (a : R) → R →+ R) x : R →+ R) : (a : R) → R) y = x * y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
⊢ Eq.{u_1 + 1} (α := (a : R) → R →+ R) (⇑mul : (a : R) → R →+ R) mulLeft

Tactic:
rfl

Premises used: AddMonoidHom.mulLeft, rfl
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
⊢ Eq.{u_1 + 1} (α := (a : R) → R →+ R) (⇑(flip mul) : (a : R) → R →+ R) mulRight

Tactic:
rfl

Premises used: AddMonoidHom.mulRight, rfl
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_1
S : Type u_2
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
f : R →+ S
⊢ (∀ (x y : R),
      (f : (a : R) → S) (x * y) = HMul.hMul (α := S) (β := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) y : S)) ↔
    compr₂ mul f = (comp mul f).compl₂ f

Tactic:
Iff.symm ext_iff₂

Premises used: Iff.symm, AddMonoidHom.ext_iff₂
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
a : R
⊢ Eq (α := R →+ R) (mulLeft a) (mulRight a) ↔ ∀ (b : R), Commute a b

Tactic:
DFunLike.ext_iff

Premises used: SemiconjBy, Commute, DFunLike.ext_iff
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
b : R
⊢ Eq (α := R →+ R) (mulRight b) (mulLeft b) ↔ ∀ (a : R), Commute a b

Tactic:
DFunLike.ext_iff

Premises used: SemiconjBy, Commute, DFunLike.ext_iff
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocCommSemiring R
⊢ Eq.{u_1 + 1} (α := R →+ AddMonoid.End R) mulRight mulLeft

Tactic:
AddMonoidHom.ext fun _ =>
    Eq.symm <| AddMonoidHom.mulLeft_eq_mulRight_iff_forall_commute.2 (.all _)

Premises used: Iff.mpr, AddMonoidHom.ext, Eq.symm, Commute.all, AddMonoidHom.mulLeft_eq_mulRight_iff_forall_commute
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
α : Type u_3
inst : NonUnitalCommRing α
b c x : α
h : x * x - b * x + c = 0
⊢ -(x * x - b * x) = x * (b - x)

Tactic:
simp [mul_sub, mul_comm]

Premises used: mul_sub, mul_comm
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
α : Type u_3
inst : NonUnitalCommRing α
b c x : α
h : x * x - b * x + c = 0
⊢ c = x * (b - x)

Tactic:
have : c = x * (b - x) := (eq_neg_of_add_eq_zero_right h).trans (by simp [mul_sub, mul_comm])
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
α : Type u_3
inst : NonUnitalCommRing α
b c x : α
h : x * x - b * x + c = 0
this : c = x * (b - x)
⊢ x + (b - x) = b

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
α : Type u_3
inst : NonUnitalCommRing α
b c x : α
h : x * x - b * x + c = 0
this : c = x * (b - x)
rw rw₁ : x * (b - x) = x * (b - x)
⊢ x * (b - x) = c

Tactic:
rw [this]
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
α : Type u_3
inst : NonUnitalCommRing α
b c x : α
h : x * x - b * x + c = 0
this : c = x * (b - x)
refine : (b - x) * (b - x) - b * (b - x) + c = 0
⊢ ∃ (y : α), y * y - b * y + c = 0 ∧ x + y = b ∧ x * y = c

Tactic:
refine ⟨b - x, ?_, by simp, by rw [this]⟩
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
α : Type u_3
inst : NonUnitalCommRing α
b c x : α
h : x * x - b * x + c = 0
this : c = x * (b - x)
rw : (b - x) * (b - x) - b * (b - x) + x * (b - x) = 0
rw₁ : (b - x) * (b - x) - (b * (b - x) - x * (b - x)) = 0
rw₂ : (b - x) * (b - x) - (b - x) * (b - x) = 0
rw₃ rw₄ : Eq.{u_3 + 1} (α := α) 0 0
⊢ (b - x) * (b - x) - b * (b - x) + c = 0

Tactic:
rw [this, sub_add, ← sub_mul, sub_self]

Premises used: sub_add, sub_self, sub_mul
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
α : Type u_3
inst : NonAssocRing α
inst_1 : Nontrivial α
a : α
h : a + 1 = a
⊢ a + 1 = a + 0

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
α : Type u_3
inst : NonAssocRing α
inst_1 : Nontrivial α
a : α
h : a - 1 = a
⊢ a + -1 = a + -0

Tactic:
simp [← sub_eq_add_neg, h]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_3
inst : NonUnitalNonAssocRing R
r : R
h : IsLeftRegular r
r' : R
eq : r * r' = 0
simp_rw simp_rw₁ : r * r' = r * 0
simp_rw₂ : 0 = r * 0
⊢ Eq.{u_3 + 1} (α := R) ((fun (x : R) ↦ r * x) r') ((fun (x : R) ↦ r * x) 0)

Tactic:
simp_rw [eq, mul_zero]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_3
inst : NonUnitalNonAssocRing R
r : R
h : ∀ (x : R), r * x = 0 → x = 0
r₁ r₂ : R
eq : Eq.{u_3 + 1} (α := R) ((fun (x : R) ↦ r * x) r₁) ((fun (x : R) ↦ r * x) r₂)
simp_rw : r * r₁ - r * r₂ = 0
simp_rw₁ : r * r₂ - r * r₂ = 0
⊢ r * (r₁ - r₂) = 0

Tactic:
simp_rw [mul_sub, eq, sub_self]

Premises used: mul_sub, sub_self
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_3
inst : NonUnitalNonAssocRing R
r : R
h : IsRightRegular r
r' : R
eq : r' * r = 0
simp_rw simp_rw₁ : r' * r = 0 * r
simp_rw₂ : 0 = 0 * r
⊢ Eq.{u_3 + 1} (α := R) ((fun (x : R) ↦ x * r) r') ((fun (x : R) ↦ x * r) 0)

Tactic:
simp_rw [eq, zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_3
inst : NonUnitalNonAssocRing R
r : R
h : ∀ (x : R), x * r = 0 → x = 0
r₁ r₂ : R
eq : Eq.{u_3 + 1} (α := R) ((fun (x : R) ↦ x * r) r₁) ((fun (x : R) ↦ x * r) r₂)
simp_rw : r₁ * r - r₂ * r = 0
simp_rw₁ : r₂ * r - r₂ * r = 0
⊢ (r₁ - r₂) * r = 0

Tactic:
simp_rw [sub_mul, eq, sub_self]

Premises used: sub_self, sub_mul
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_3
inst : NonUnitalNonAssocRing R
r : R
rw : IsLeftRegular r ∧ IsRightRegular r ↔ (∀ (x : R), r * x = 0 → x = 0) ∧ ∀ (x : R), x * r = 0 → x = 0
rw₁ : (∀ (x : R), r * x = 0 → x = 0) ∧ IsRightRegular r ↔ (∀ (x : R), r * x = 0 → x = 0) ∧ ∀ (x : R), x * r = 0 → x = 0
rw₂ rw₃ :
  ((∀ (x : R), r * x = 0 → x = 0) ∧ ∀ (x : R), x * r = 0 → x = 0) ↔
    (∀ (x : R), r * x = 0 → x = 0) ∧ ∀ (x : R), x * r = 0 → x = 0
⊢ IsRegular r ↔ (∀ (x : R), r * x = 0 → x = 0) ∧ ∀ (x : R), x * r = 0 → x = 0

Tactic:
rw [isRegular_iff, isLeftRegular_iff_right_eq_zero_of_mul, isRightRegular_iff_left_eq_zero_of_mul]

Premises used: isRegular_iff, isLeftRegular_iff_right_eq_zero_of_mul, isRightRegular_iff_left_eq_zero_of_mul
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_3
inst : NonUnitalNonAssocRing R
simp_rw :
  [NoZeroDivisors R, ∀ {a : R}, a ≠ 0 → ∀ (x : R), a * x = 0 → x = 0, ∀ {a : R}, a ≠ 0 → ∀ (x : R), x * a = 0 → x = 0,
      ∀ {a : R}, a ≠ 0 → (∀ (x : R), a * x = 0 → x = 0) ∧ ∀ (x : R), x * a = 0 → x = 0].TFAE
⊢ [NoZeroDivisors R, IsLeftCancelMulZero R, IsRightCancelMulZero R, IsCancelMulZero R].TFAE

Tactic:
simp_rw [isLeftCancelMulZero_iff, isRightCancelMulZero_iff, isCancelMulZero_iff_forall_isRegular,
    isLeftRegular_iff_right_eq_zero_of_mul, isRightRegular_iff_left_eq_zero_of_mul,
    isRegular_iff_eq_zero_of_mul]

Premises used: isRegular_iff_eq_zero_of_mul, isRightCancelMulZero_iff, isLeftRegular_iff_right_eq_zero_of_mul, isRightRegular_iff_left_eq_zero_of_mul, isLeftCancelMulZero_iff, isCancelMulZero_iff_forall_isRegular
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_3
inst : NonUnitalNonAssocRing R
⊢ NoZeroDivisors R

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_3
inst : NonUnitalNonAssocRing R
⊢ ∀ {a : R}, a ≠ 0 → ∀ (x : R), a * x = 0 → x = 0

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_3
inst : NonUnitalNonAssocRing R
⊢ NoZeroDivisors R ↔ ∀ {a : R}, a ≠ 0 → ∀ (x : R), a * x = 0 → x = 0

Tactic:
1 ↔ 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_3
inst : NonUnitalNonAssocRing R
⊢ NoZeroDivisors R ↔ ∀ {a : R}, a ≠ 0 → ∀ (x : R), a * x = 0 → x = 0

Tactic:
tfae_have 1 ↔ 2 := noZeroDivisors_iff_right_eq_zero_of_mul

Premises used: noZeroDivisors_iff_right_eq_zero_of_mul
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_3
inst : NonUnitalNonAssocRing R
tfae_1_iff_2 : NoZeroDivisors R ↔ ∀ {a : R}, a ≠ 0 → ∀ (x : R), a * x = 0 → x = 0
⊢ NoZeroDivisors R

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_3
inst : NonUnitalNonAssocRing R
tfae_1_iff_2 : NoZeroDivisors R ↔ ∀ {a : R}, a ≠ 0 → ∀ (x : R), a * x = 0 → x = 0
⊢ ∀ {a : R}, a ≠ 0 → ∀ (x : R), x * a = 0 → x = 0

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_3
inst : NonUnitalNonAssocRing R
tfae_1_iff_2 : NoZeroDivisors R ↔ ∀ {a : R}, a ≠ 0 → ∀ (x : R), a * x = 0 → x = 0
⊢ NoZeroDivisors R ↔ ∀ {a : R}, a ≠ 0 → ∀ (x : R), x * a = 0 → x = 0

Tactic:
1 ↔ 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_3
inst : NonUnitalNonAssocRing R
tfae_1_iff_2 : NoZeroDivisors R ↔ ∀ {a : R}, a ≠ 0 → ∀ (x : R), a * x = 0 → x = 0
⊢ NoZeroDivisors R ↔ ∀ {a : R}, a ≠ 0 → ∀ (x : R), x * a = 0 → x = 0

Tactic:
tfae_have 1 ↔ 3 := noZeroDivisors_iff_left_eq_zero_of_mul

Premises used: noZeroDivisors_iff_left_eq_zero_of_mul
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_3
inst : NonUnitalNonAssocRing R
tfae_1_iff_2 : NoZeroDivisors R ↔ ∀ {a : R}, a ≠ 0 → ∀ (x : R), a * x = 0 → x = 0
tfae_1_iff_3 : NoZeroDivisors R ↔ ∀ {a : R}, a ≠ 0 → ∀ (x : R), x * a = 0 → x = 0
⊢ NoZeroDivisors R

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_3
inst : NonUnitalNonAssocRing R
tfae_1_iff_2 : NoZeroDivisors R ↔ ∀ {a : R}, a ≠ 0 → ∀ (x : R), a * x = 0 → x = 0
tfae_1_iff_3 : NoZeroDivisors R ↔ ∀ {a : R}, a ≠ 0 → ∀ (x : R), x * a = 0 → x = 0
⊢ ∀ {a : R}, a ≠ 0 → (∀ (x : R), a * x = 0 → x = 0) ∧ ∀ (x : R), x * a = 0 → x = 0

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_3
inst : NonUnitalNonAssocRing R
tfae_1_iff_2 : NoZeroDivisors R ↔ ∀ {a : R}, a ≠ 0 → ∀ (x : R), a * x = 0 → x = 0
tfae_1_iff_3 : NoZeroDivisors R ↔ ∀ {a : R}, a ≠ 0 → ∀ (x : R), x * a = 0 → x = 0
⊢ NoZeroDivisors R ↔ ∀ {a : R}, a ≠ 0 → (∀ (x : R), a * x = 0 → x = 0) ∧ ∀ (x : R), x * a = 0 → x = 0

Tactic:
1 ↔ 4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_3
inst : NonUnitalNonAssocRing R
tfae_1_iff_2 : NoZeroDivisors R ↔ ∀ {a : R}, a ≠ 0 → ∀ (x : R), a * x = 0 → x = 0
tfae_1_iff_3 : NoZeroDivisors R ↔ ∀ {a : R}, a ≠ 0 → ∀ (x : R), x * a = 0 → x = 0
⊢ NoZeroDivisors R ↔ ∀ {a : R}, a ≠ 0 → (∀ (x : R), a * x = 0 → x = 0) ∧ ∀ (x : R), x * a = 0 → x = 0

Tactic:
tfae_have 1 ↔ 4 := noZeroDivisors_iff_eq_zero_of_mul

Premises used: noZeroDivisors_iff_eq_zero_of_mul
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_3
inst : NonUnitalNonAssocRing R
tfae_1_iff_2 : NoZeroDivisors R ↔ ∀ {a : R}, a ≠ 0 → ∀ (x : R), a * x = 0 → x = 0
tfae_1_iff_3 : NoZeroDivisors R ↔ ∀ {a : R}, a ≠ 0 → ∀ (x : R), x * a = 0 → x = 0
tfae_1_iff_4 : NoZeroDivisors R ↔ ∀ {a : R}, a ≠ 0 → (∀ (x : R), a * x = 0 → x = 0) ∧ ∀ (x : R), x * a = 0 → x = 0
⊢ [NoZeroDivisors R, ∀ {a : R}, a ≠ 0 → ∀ (x : R), a * x = 0 → x = 0, ∀ {a : R}, a ≠ 0 → ∀ (x : R), x * a = 0 → x = 0,
      ∀ {a : R}, a ≠ 0 → (∀ (x : R), a * x = 0 → x = 0) ∧ ∀ (x : R), x * a = 0 → x = 0].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_3
inst : NonUnitalNonAssocRing R
⊢ IsCancelMulZero R ↔ NoZeroDivisors R

Tactic:
noZeroDivisors_tfae.out 3 0

Premises used: noZeroDivisors_tfae, List.TFAE.out, OfNat.ofNat
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R_1 : Type u_1
S : Type u_2
α : ?m.1
R : Type u_3
inst : NonUnitalNonAssocRing R
r : R
inst_1 : NoZeroDivisors R
⊢ IsCancelMulZero R

Tactic:
isCancelMulZero_iff_noZeroDivisors.mpr ‹_›

Premises used: Iff.mpr, isCancelMulZero_iff_noZeroDivisors
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
α : Type u_3
inst : Ring α
h : Nontrivial α
inst_1 : NoZeroDivisors α
⊢ IsDomain α

Tactic:
{ NoZeroDivisors.to_isCancelMulZero α, h with .. }

Premises used: IsDomain.mk, NoZeroDivisors.to_isCancelMulZero
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_1
S : Type u_2
α : Type u_3
inst : Semiring α
inst_1 : IsDomain α
⊢ NoZeroDivisors α

Tactic:
IsRightCancelMulZero.to_noZeroDivisors α

Premises used: IsRightCancelMulZero.to_noZeroDivisors
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
α : Type u_3
inst : Semiring α
⊢ IsDomain α ↔ IsCancelMulZero α ∧ Nontrivial α

Tactic:
⟨fun _ ↦ ⟨inferInstance, inferInstance⟩, fun ⟨_, _⟩ ↦ {}⟩

Premises used: IsDomain, _private.0.isDomain_iff_cancelMulZero_and_nontrivial.match_1, inferInstance, IsDomain.mk, And.intro, Iff.intro
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
α : Type u_3
inst : Semiring α
⊢ IsCancelMulZero α ↔ IsDomain α ∨ Subsingleton α

Tactic:
⟨fun t ↦ ?_, fun h ↦ h.elim (fun _ ↦ inferInstance) (fun _ ↦ inferInstance)⟩

Premises used: inferInstance, Iff.intro, Or.elim
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
α : Type u_3
inst : Semiring α
refine : ∀ (t : IsCancelMulZero α), IsDomain α ∨ Subsingleton α
⊢ IsCancelMulZero α ↔ IsDomain α ∨ Subsingleton α

Tactic:
refine ⟨fun t ↦ ?_, fun h ↦ h.elim (fun _ ↦ inferInstance) (fun _ ↦ inferInstance)⟩
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
α : Type u_3
inst : Semiring α
t : IsCancelMulZero α
rw : Nontrivial α → IsDomain α
⊢ IsDomain α ∨ Subsingleton α

Tactic:
rw [or_iff_not_imp_right, not_subsingleton_iff_nontrivial]

Premises used: Classical.or_iff_not_imp_right, not_subsingleton_iff_nontrivial
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
α : Type u_3
inst : Semiring α
t : IsCancelMulZero α
⊢ Nontrivial α → IsDomain α

Tactic:
fun _ ↦ {}

Premises used: IsDomain.mk
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
α : Type u_3
inst : Semiring α
t : IsCancelMulZero α
⊢ Nontrivial α → IsDomain α

Tactic:
exact fun _ ↦ {}
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
α : Type u_3
inst : Ring α
rw : IsDomain α ↔ IsCancelMulZero α ∧ Nontrivial α
rw₁ rw₂ : IsCancelMulZero α ∧ Nontrivial α ↔ IsCancelMulZero α ∧ Nontrivial α
⊢ IsDomain α ↔ NoZeroDivisors α ∧ Nontrivial α

Tactic:
rw [← isCancelMulZero_iff_noZeroDivisors, isDomain_iff_cancelMulZero_and_nontrivial]

Premises used: isDomain_iff_cancelMulZero_and_nontrivial, isCancelMulZero_iff_noZeroDivisors
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
α : Type u_3
inst : Ring α
rw : IsCancelMulZero α ↔ IsDomain α ∨ Subsingleton α
rw₁ rw₂ : IsDomain α ∨ Subsingleton α ↔ IsDomain α ∨ Subsingleton α
⊢ NoZeroDivisors α ↔ IsDomain α ∨ Subsingleton α

Tactic:
rw [← isCancelMulZero_iff_noZeroDivisors, isCancelMulZero_iff_isDomain_or_subsingleton]

Premises used: isCancelMulZero_iff_isDomain_or_subsingleton, isCancelMulZero_iff_noZeroDivisors
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : DivisionMonoid R
inst_1 : HasDistribNeg R
rw : HMul.hMul (α := R) 1 1 = 1
rw₁ rw₂ : Eq.{u_1 + 1} (α := R) 1 1
⊢ HMul.hMul (α := R) (-1) (-1) = 1

Tactic:
rw [neg_mul_neg, one_mul]

Premises used: neg_mul_neg, one_mul
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : DivisionMonoid R
inst_1 : HasDistribNeg R
a : R
rw rw₁ : 1 / (-1 * a) = 1 / (-1 * a)
⊢ 1 / -a = 1 / (-1 * a)

Tactic:
rw [neg_eq_neg_one_mul]

Premises used: neg_eq_neg_one_mul
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : DivisionMonoid R
inst_1 : HasDistribNeg R
a : R
rw rw₁ : 1 / (-1 * a) = 1 / (-1 * a)
⊢ 1 / (-1 * a) = 1 / a * HDiv.hDiv (α := R) 1 (-1)

Tactic:
rw [one_div_mul_one_div_rev]

Premises used: one_div_mul_one_div_rev
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : DivisionMonoid R
inst_1 : HasDistribNeg R
a : R
rw rw₁ : 1 / a * -1 = 1 / a * -1
⊢ 1 / a * HDiv.hDiv (α := R) 1 (-1) = 1 / a * -1

Tactic:
rw [one_div_neg_one_eq_neg_one]

Premises used: one_div_neg_one_eq_neg_one
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : DivisionMonoid R
inst_1 : HasDistribNeg R
a : R
rw : -(1 / a * 1) = -(1 / a)
rw₁ rw₂ : -(1 / a) = -(1 / a)
⊢ 1 / a * -1 = -(1 / a)

Tactic:
rw [mul_neg, mul_one]

Premises used: mul_one, mul_neg
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : DivisionMonoid R
inst_1 : HasDistribNeg R
a b : R
rw : b / -a = b * (-a)⁻¹
rw₁ rw₂ : b * (-a)⁻¹ = b * (-a)⁻¹
⊢ b / -a = b * (1 / -a)

Tactic:
rw [← inv_eq_one_div, division_def]

Premises used: division_def, inv_eq_one_div
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : DivisionMonoid R
inst_1 : HasDistribNeg R
a b : R
rw rw₁ : b * -(1 / a) = b * -(1 / a)
⊢ b * (1 / -a) = b * -(1 / a)

Tactic:
rw [one_div_neg_eq_neg_one_div]

Premises used: one_div_neg_eq_neg_one_div
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : DivisionMonoid R
inst_1 : HasDistribNeg R
a b : R
rw rw₁ : b * -(1 / a) = b * -(1 / a)
⊢ b * -(1 / a) = -(b * (1 / a))

Tactic:
rw [neg_mul_eq_mul_neg]

Premises used: neg_mul_eq_mul_neg
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : DivisionMonoid R
inst_1 : HasDistribNeg R
a b : R
rw rw₁ : -(b / a) = -(b / a)
⊢ -(b * (1 / a)) = -(b / a)

Tactic:
rw [mul_one_div]

Premises used: mul_one_div
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : DivisionMonoid R
inst_1 : HasDistribNeg R
a b : R
rw : -1 * b / a = -(b / a)
rw₁ : -1 * (b / a) = -(b / a)
rw₂ rw₃ : -(b / a) = -(b / a)
⊢ -b / a = -(b / a)

Tactic:
rw [neg_eq_neg_one_mul, mul_div_assoc, ← neg_eq_neg_one_mul]

Premises used: mul_div_assoc, neg_eq_neg_one_mul
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : DivisionMonoid R
inst_1 : HasDistribNeg R
a b : R
rw rw₁ : -(b / a) = -(b / a)
⊢ -(b / a) = -b / a

Tactic:
rw [neg_div]

Premises used: neg_div
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : DivisionMonoid R
inst_1 : HasDistribNeg R
a b : R
rw : -(-a / b) = a / b
rw₁ : - -(a / b) = a / b
rw₂ rw₃ : a / b = a / b
⊢ -a / -b = a / b

Tactic:
rw [div_neg_eq_neg_div, neg_div, neg_neg]

Premises used: neg_div, neg_neg, div_neg_eq_neg_div
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : DivisionMonoid R
inst_1 : HasDistribNeg R
a : R
rw : -(1 / a) = (-a)⁻¹
rw₁ : -(1 / a) = 1 / -a
rw₂ rw₃ : -(1 / a) = -(1 / a)
⊢ -a⁻¹ = (-a)⁻¹

Tactic:
rw [inv_eq_one_div, inv_eq_one_div, div_neg_eq_neg_div]

Premises used: inv_eq_one_div, div_neg_eq_neg_div
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : DivisionMonoid R
inst_1 : HasDistribNeg R
b a : R
rw rw₁ : a / -b = a / -b
⊢ a / -b = -(a / b)

Tactic:
rw [← div_neg_eq_neg_div]

Premises used: div_neg_eq_neg_div
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : DivisionMonoid R
inst_1 : HasDistribNeg R
b a : R
⊢ a / -b = -a / b

Tactic:
neg_div b a ▸ div_neg _

Premises used: neg_div, Eq.rec, div_neg, Eq.symm
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : DivisionMonoid R
inst_1 : HasDistribNeg R
a : R
rw rw₁ : (-a)⁻¹ = (-a)⁻¹
⊢ (-a)⁻¹ = -a⁻¹

Tactic:
rw [neg_inv]

Premises used: neg_inv
-- Module: Mathlib.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : DivisionMonoid R
inst_1 : HasDistribNeg R
rw : Eq.{u_1 + 1} (α := R) (-1⁻¹) (-1)
rw₁ rw₂ : Eq.{u_1 + 1} (α := R) (-1) (-1)
⊢ Eq.{u_1 + 1} (α := R) (-1)⁻¹ (-1)

Tactic:
rw [← neg_inv, inv_one]

Premises used: inv_one, neg_inv
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
a : α
⊢ a * a = a

Tactic:
IsIdempotentElem.eq (isIdempotentElem a)

Premises used: BooleanRing.isIdempotentElem, IsIdempotentElem.eq
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : BooleanRing α
a b : α
⊢ Std.IdempotentOp fun (x1 x2 : α) ↦ x1 * x2

Tactic:
⟨BooleanRing.mul_self⟩

Premises used: BooleanRing.mul_self, Std.IdempotentOp.mk
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
a : α
rw rw₁ : a + a = a + a
⊢ a + a = (a + a) * (a + a)

Tactic:
rw [mul_self]

Premises used: BooleanRing.mul_self
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
a : α
rw : a * (a + a) + a * (a + a) = a * a + a * a + (a * a + a * a)
rw₁ rw₂ : a * a + a * a + (a * a + a * a) = a * a + a * a + (a * a + a * a)
⊢ (a + a) * (a + a) = a * a + a * a + (a * a + a * a)

Tactic:
rw [add_mul, mul_add]

Premises used: add_mul, mul_add
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
a : α
rw rw₁ : a + a + (a + a) = a + a + (a + a)
⊢ a * a + a * a + (a * a + a * a) = a + a + (a + a)

Tactic:
rw [mul_self]

Premises used: BooleanRing.mul_self
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
a : α
⊢ a + a = a + a + (a + a)

Tactic:
have : a + a = a + a + (a + a) :=
    calc
      a + a = (a + a) * (a + a) := by rw [mul_self]
      _ = a * a + a * a + (a * a + a * a) := by rw [add_mul, mul_add]
      _ = a + a + (a + a) := by rw [mul_self]
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
a : α
this : a + a = a + a + (a + a)
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : a + a = 0), a + a = 0
⊢ a + a = 0

Tactic:
rwa [right_eq_add] at this

Premises used: right_eq_add
-- Module: Mathlib.Algebra.Ring.BooleanRing
Goal:
α : Type u_1
inst : BooleanRing α
a : α
rw rw₁ : -a = -a
⊢ -a = -a + 0

Tactic:
rw [add_zero]

Premises used: add_zero