awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (goal)
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
⊢ (r₁ - r₂) * r = 0
have simp_rw₁ : r₂ * r - r₂ * r = 0
Tactic: simp_rw [sub_mul, eq, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (goal)
Goal:
R : Type u_3
inst : NonUnitalNonAssocRing R
r : R
⊢ IsRegular r ↔ (∀ (x : R), r * x = 0 → x = 0) ∧ ∀ (x : R), x * r = 0 → x = 0
have rw : IsLeftRegular r ∧ IsRightRegular 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]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (goal)
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
⊢ IsRegular r ↔ (∀ (x : R), r * x = 0 → x = 0) ∧ ∀ (x : R), x * r = 0 → x = 0
have rw₁ : (∀ (x : R), r * x = 0 → x = 0) ∧ IsRightRegular 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]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (goal)
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
⊢ IsRegular r ↔ (∀ (x : R), r * x = 0 → x = 0) ∧ ∀ (x : R), x * r = 0 → x = 0
have 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
Tactic: rw [isRegular_iff, isLeftRegular_iff_right_eq_zero_of_mul, isRightRegular_iff_left_eq_zero_of_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (goal)
Goal:
R : Type u_3
inst : NonUnitalNonAssocRing R
⊢ [NoZeroDivisors R, IsLeftCancelMulZero R, IsRightCancelMulZero R, IsCancelMulZero R].TFAE
have 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
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]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (hypothesis)
Goal:
R : Type u_3
inst : NonUnitalNonAssocRing R
⊢ [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
have tfae_1_iff_2 : 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
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (hypothesis)
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), 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
have tfae_1_iff_3 : 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
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (hypothesis)
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, ∀ {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
have tfae_1_iff_4 : 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
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (goal)
Goal:
α : Type u_3
inst : Semiring α
⊢ IsCancelMulZero α ↔ IsDomain α ∨ Subsingleton α
have refine : ∀ (t : IsCancelMulZero α), IsDomain α ∨ Subsingleton α
Tactic: refine ⟨fun t ↦ ?_, fun h ↦ h.elim (fun _ ↦ inferInstance) (fun _ ↦ inferInstance)⟩
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (goal)
Goal:
α : Type u_3
inst : Semiring α
t : IsCancelMulZero α
⊢ IsDomain α ∨ Subsingleton α
have rw : Nontrivial α → IsDomain α
Tactic: rw [or_iff_not_imp_right, not_subsingleton_iff_nontrivial]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (goal)
Goal:
α : Type u_3
inst : Ring α
⊢ IsDomain α ↔ NoZeroDivisors α ∧ Nontrivial α
have rw : IsDomain α ↔ IsCancelMulZero α ∧ Nontrivial α
Tactic: rw [← isCancelMulZero_iff_noZeroDivisors, isDomain_iff_cancelMulZero_and_nontrivial]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (goal)
Goal:
α : Type u_3
inst : Ring α
rw : IsDomain α ↔ IsCancelMulZero α ∧ Nontrivial α
⊢ IsDomain α ↔ NoZeroDivisors α ∧ Nontrivial α
have rw₁ : IsCancelMulZero α ∧ Nontrivial α ↔ IsCancelMulZero α ∧ Nontrivial α
Tactic: rw [← isCancelMulZero_iff_noZeroDivisors, isDomain_iff_cancelMulZero_and_nontrivial]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (goal)
Goal:
α : Type u_3
inst : Ring α
⊢ NoZeroDivisors α ↔ IsDomain α ∨ Subsingleton α
have rw : IsCancelMulZero α ↔ IsDomain α ∨ Subsingleton α
Tactic: rw [← isCancelMulZero_iff_noZeroDivisors, isCancelMulZero_iff_isDomain_or_subsingleton]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (goal)
Goal:
α : Type u_3
inst : Ring α
rw : IsCancelMulZero α ↔ IsDomain α ∨ Subsingleton α
⊢ NoZeroDivisors α ↔ IsDomain α ∨ Subsingleton α
have rw₁ : IsDomain α ∨ Subsingleton α ↔ IsDomain α ∨ Subsingleton α
Tactic: rw [← isCancelMulZero_iff_noZeroDivisors, isCancelMulZero_iff_isDomain_or_subsingleton]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (goal)
Goal:
R : Type u_1
inst : DivisionMonoid R
inst_1 : HasDistribNeg R
⊢ HMul.hMul (α := R) (-1) (-1) = 1
have rw : HMul.hMul (α := R) 1 1 = 1
Tactic: rw [neg_mul_neg, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (goal)
Goal:
R : Type u_1
inst : DivisionMonoid R
inst_1 : HasDistribNeg R
rw : HMul.hMul (α := R) 1 1 = 1
⊢ HMul.hMul (α := R) (-1) (-1) = 1
have rw₁ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [neg_mul_neg, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (goal)
Goal:
R : Type u_1
inst : DivisionMonoid R
inst_1 : HasDistribNeg R
a : R
⊢ 1 / -a = 1 / (-1 * a)
have rw : 1 / (-1 * a) = 1 / (-1 * a)
Tactic: rw [neg_eq_neg_one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (goal)
Goal:
R : Type u_1
inst : DivisionMonoid R
inst_1 : HasDistribNeg R
a : R
⊢ 1 / (-1 * a) = 1 / a * HDiv.hDiv (α := R) 1 (-1)
have rw : 1 / (-1 * a) = 1 / (-1 * a)
Tactic: rw [one_div_mul_one_div_rev]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (goal)
Goal:
R : Type u_1
inst : DivisionMonoid R
inst_1 : HasDistribNeg R
a : R
⊢ 1 / a * HDiv.hDiv (α := R) 1 (-1) = 1 / a * -1
have rw : 1 / a * -1 = 1 / a * -1
Tactic: rw [one_div_neg_one_eq_neg_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (goal)
Goal:
R : Type u_1
inst : DivisionMonoid R
inst_1 : HasDistribNeg R
a : R
⊢ 1 / a * -1 = -(1 / a)
have rw : -(1 / a * 1) = -(1 / a)
Tactic: rw [mul_neg, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (goal)
Goal:
R : Type u_1
inst : DivisionMonoid R
inst_1 : HasDistribNeg R
a : R
rw : -(1 / a * 1) = -(1 / a)
⊢ 1 / a * -1 = -(1 / a)
have rw₁ : -(1 / a) = -(1 / a)
Tactic: rw [mul_neg, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (goal)
Goal:
R : Type u_1
inst : DivisionMonoid R
inst_1 : HasDistribNeg R
a b : R
⊢ b / -a = b * (1 / -a)
have rw : b / -a = b * (-a)⁻¹
Tactic: rw [← inv_eq_one_div, division_def]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (goal)
Goal:
R : Type u_1
inst : DivisionMonoid R
inst_1 : HasDistribNeg R
a b : R
rw : b / -a = b * (-a)⁻¹
⊢ b / -a = b * (1 / -a)
have rw₁ : b * (-a)⁻¹ = b * (-a)⁻¹
Tactic: rw [← inv_eq_one_div, division_def]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (goal)
Goal:
R : Type u_1
inst : DivisionMonoid R
inst_1 : HasDistribNeg R
a b : R
⊢ b * (1 / -a) = b * -(1 / a)
have rw : b * -(1 / a) = b * -(1 / a)
Tactic: rw [one_div_neg_eq_neg_one_div]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (goal)
Goal:
R : Type u_1
inst : DivisionMonoid R
inst_1 : HasDistribNeg R
a b : R
⊢ b * -(1 / a) = -(b * (1 / a))
have rw : b * -(1 / a) = b * -(1 / a)
Tactic: rw [neg_mul_eq_mul_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (goal)
Goal:
R : Type u_1
inst : DivisionMonoid R
inst_1 : HasDistribNeg R
a b : R
⊢ -(b * (1 / a)) = -(b / a)
have rw : -(b / a) = -(b / a)
Tactic: rw [mul_one_div]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (goal)
Goal:
R : Type u_1
inst : DivisionMonoid R
inst_1 : HasDistribNeg R
a b : R
⊢ -b / a = -(b / a)
have rw : -1 * b / a = -(b / a)
Tactic: rw [neg_eq_neg_one_mul, mul_div_assoc, ← neg_eq_neg_one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (goal)
Goal:
R : Type u_1
inst : DivisionMonoid R
inst_1 : HasDistribNeg R
a b : R
rw : -1 * b / a = -(b / a)
⊢ -b / a = -(b / a)
have rw₁ : -1 * (b / a) = -(b / a)
Tactic: rw [neg_eq_neg_one_mul, mul_div_assoc, ← neg_eq_neg_one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (goal)
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)
⊢ -b / a = -(b / a)
have rw₂ : -(b / a) = -(b / a)
Tactic: rw [neg_eq_neg_one_mul, mul_div_assoc, ← neg_eq_neg_one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (goal)
Goal:
R : Type u_1
inst : DivisionMonoid R
inst_1 : HasDistribNeg R
a b : R
⊢ -(b / a) = -b / a
have rw : -(b / a) = -(b / a)
Tactic: rw [neg_div]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (goal)
Goal:
R : Type u_1
inst : DivisionMonoid R
inst_1 : HasDistribNeg R
a b : R
⊢ -a / -b = a / b
have rw : -(-a / b) = a / b
Tactic: rw [div_neg_eq_neg_div, neg_div, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (goal)
Goal:
R : Type u_1
inst : DivisionMonoid R
inst_1 : HasDistribNeg R
a b : R
rw : -(-a / b) = a / b
⊢ -a / -b = a / b
have rw₁ : - -(a / b) = a / b
Tactic: rw [div_neg_eq_neg_div, neg_div, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (goal)
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
⊢ -a / -b = a / b
have rw₂ : a / b = a / b
Tactic: rw [div_neg_eq_neg_div, neg_div, neg_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (goal)
Goal:
R : Type u_1
inst : DivisionMonoid R
inst_1 : HasDistribNeg R
a : R
⊢ -a⁻¹ = (-a)⁻¹
have rw : -(1 / a) = (-a)⁻¹
Tactic: rw [inv_eq_one_div, inv_eq_one_div, div_neg_eq_neg_div]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (goal)
Goal:
R : Type u_1
inst : DivisionMonoid R
inst_1 : HasDistribNeg R
a : R
rw : -(1 / a) = (-a)⁻¹
⊢ -a⁻¹ = (-a)⁻¹
have rw₁ : -(1 / a) = 1 / -a
Tactic: rw [inv_eq_one_div, inv_eq_one_div, div_neg_eq_neg_div]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (goal)
Goal:
R : Type u_1
inst : DivisionMonoid R
inst_1 : HasDistribNeg R
a : R
rw : -(1 / a) = (-a)⁻¹
rw₁ : -(1 / a) = 1 / -a
⊢ -a⁻¹ = (-a)⁻¹
have rw₂ : -(1 / a) = -(1 / a)
Tactic: rw [inv_eq_one_div, inv_eq_one_div, div_neg_eq_neg_div]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (goal)
Goal:
R : Type u_1
inst : DivisionMonoid R
inst_1 : HasDistribNeg R
b a : R
⊢ a / -b = -(a / b)
have rw : a / -b = a / -b
Tactic: rw [← div_neg_eq_neg_div]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (goal)
Goal:
R : Type u_1
inst : DivisionMonoid R
inst_1 : HasDistribNeg R
a : R
⊢ (-a)⁻¹ = -a⁻¹
have rw : (-a)⁻¹ = (-a)⁻¹
Tactic: rw [neg_inv]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (goal)
Goal:
R : Type u_1
inst : DivisionMonoid R
inst_1 : HasDistribNeg R
⊢ Eq.{u_1 + 1} (α := R) (-1)⁻¹ (-1)
have rw : Eq.{u_1 + 1} (α := R) (-1⁻¹) (-1)
Tactic: rw [← neg_inv, inv_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (goal)
Goal:
R : Type u_1
inst : DivisionMonoid R
inst_1 : HasDistribNeg R
rw : Eq.{u_1 + 1} (α := R) (-1⁻¹) (-1)
⊢ Eq.{u_1 + 1} (α := R) (-1)⁻¹ (-1)
have rw₁ : Eq.{u_1 + 1} (α := R) (-1) (-1)
Tactic: rw [← neg_inv, inv_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a : α
⊢ a + a = (a + a) * (a + a)
have rw : a + a = a + a
Tactic: rw [mul_self]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a : α
⊢ (a + a) * (a + a) = a * a + a * a + (a * a + a * a)
have rw : a * (a + a) + a * (a + a) = a * a + a * a + (a * a + a * a)
Tactic: rw [add_mul, mul_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a : α
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)
have rw₁ : a * a + a * a + (a * a + a * a) = a * a + a * a + (a * a + a * a)
Tactic: rw [add_mul, mul_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a : α
⊢ a * a + a * a + (a * a + a * a) = a + a + (a + a)
have rw : a + a + (a + a) = a + a + (a + a)
Tactic: rw [mul_self]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (hypothesis)
Goal:
α : Type u_1
inst : BooleanRing α
a : α
⊢ a + a = 0
have this : 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]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a : α
this : a + a = a + a + (a + a)
⊢ a + a = 0
have rwa : ∀ (this : a + a = 0), a + a = 0
Tactic: rwa [right_eq_add] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a : α
⊢ -a = -a + 0
have rw : -a = -a
Tactic: rw [add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a : α
⊢ -a + 0 = -a + -a + a
have rw : -a + (-a + a) = -a + -a + a
Tactic: rw [← neg_add_cancel, add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a : α
rw : -a + (-a + a) = -a + -a + a
rw₁ : α
⊢ -a + 0 = -a + -a + a
have rw₂ : -a + (-a + a) = -a + (-a + a)
Tactic: rw [← neg_add_cancel, add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a : α
⊢ -a + -a + a = a
have rw : 0 + a = a
Tactic: rw [add_self, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a : α
rw : 0 + a = a
⊢ -a + -a + a = a
have rw₁ : a = a
Tactic: rw [add_self, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
⊢ a = -b ↔ a = b
have rw : a = b ↔ a = b
Tactic: rw [neg_eq]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
⊢ a + b = (a + b) * (a + b)
have rw : a + b = a + b
Tactic: rw [mul_self]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
⊢ (a + b) * (a + b) = a * a + a * b + (b * a + b * b)
have rw : a * (a + b) + b * (a + b) = a * a + a * b + (b * a + b * b)
Tactic: rw [add_mul, mul_add, mul_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
rw : a * (a + b) + b * (a + b) = a * a + a * b + (b * a + b * b)
⊢ (a + b) * (a + b) = a * a + a * b + (b * a + b * b)
have rw₁ : a * a + a * b + b * (a + b) = a * a + a * b + (b * a + b * b)
Tactic: rw [add_mul, mul_add, mul_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
rw : a * (a + b) + b * (a + b) = a * a + a * b + (b * a + b * b)
rw₁ : a * a + a * b + b * (a + b) = a * a + a * b + (b * a + b * b)
⊢ (a + b) * (a + b) = a * a + a * b + (b * a + b * b)
have rw₂ : a * a + a * b + (b * a + b * b) = a * a + a * b + (b * a + b * b)
Tactic: rw [add_mul, mul_add, mul_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (hypothesis)
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
⊢ a * b + b * a = 0
have this : a + b = a + b + (a * b + b * a)
Tactic: have : a + b = a + b + (a * b + b * a) :=
    calc
      a + b = (a + b) * (a + b) := by rw [mul_self]
      _ = a * a + a * b + (b * a + b * b) := by rw [add_mul, mul_add, mul_add]
      _ = a + a * b + (b * a + b) := by simp only [mul_self]
      _ = a + b + (a * b + b * a) := by abel
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
this : a + b = a + b + (a * b + b * a)
⊢ a * b + b * a = 0
have rwa : ∀ (this : a * b + b * a = 0), a * b + b * a = 0
Tactic: rwa [left_eq_add] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
⊢ a - b = a + b
have rw : a + -b = a + b
Tactic: rw [sub_eq_add_neg, add_right_inj, neg_eq]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
rw : a + -b = a + b
⊢ a - b = a + b
have rw₁ : -b = b
Tactic: rw [sub_eq_add_neg, add_right_inj, neg_eq]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
rw : a + -b = a + b
rw₁ : -b = b
⊢ a - b = a + b
have rw₂ : b = b
Tactic: rw [sub_eq_add_neg, add_right_inj, neg_eq]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a : α
⊢ a * (1 + a) = 0
have rw : a * 1 + a * a = 0
Tactic: rw [mul_add, mul_one, mul_self, add_self]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a : α
rw : a * 1 + a * a = 0
⊢ a * (1 + a) = 0
have rw₁ : a + a * a = 0
Tactic: rw [mul_add, mul_one, mul_self, add_self]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a : α
rw : a * 1 + a * a = 0
rw₁ : a + a * a = 0
⊢ a * (1 + a) = 0
have rw₂ : a + a = 0
Tactic: rw [mul_add, mul_one, mul_self, add_self]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a : α
rw : a * 1 + a * a = 0
rw₁ : a + a * a = 0
rw₂ : a + a = 0
⊢ a * (1 + a) = 0
have rw₃ : Eq.{u_1 + 1} (α := α) 0 0
Tactic: rw [mul_add, mul_one, mul_self, add_self]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : BooleanRing α
a_1 b_1 a b : α
⊢ a * b = b * a
have rw : a * b + b * a = 0
Tactic: rw [← add_eq_zero', mul_add_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : BooleanRing α
a_1 b_1 a b : α
rw : a * b + b * a = 0
⊢ a * b = b * a
have rw₁ : Eq.{u_1 + 1} (α := α) 0 0
Tactic: rw [← add_eq_zero', mul_add_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
⊢ a ⊔ b = b ⊔ a
have dsimp : a + b + a * b = b + a + b * a
Tactic: dsimp only [(· ⊔ ·)]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
⊢ a ⊓ b = b ⊓ a
have dsimp : a * b = b * a
Tactic: dsimp only [(· ⊓ ·)]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a b c : α
⊢ a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
have dsimp : a + b + a * b + c + (a + b + a * b) * c = a + (b + c + b * c) + a * (b + c + b * c)
Tactic: dsimp only [(· ⊔ ·)]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a b c : α
⊢ a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
have dsimp : a * b * c = a * (b * c)
Tactic: dsimp only [(· ⊓ ·)]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
⊢ a ⊔ a ⊓ b = a
have dsimp : a + a * b + a * (a * b) = a
Tactic: dsimp only [(· ⊔ ·), (· ⊓ ·)]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
⊢ a + a * b + a * (a * b) = a
have rw : a + a * b + a * a * b = a
Tactic: rw [← mul_assoc, mul_self, add_assoc, add_self, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
rw : a + a * b + a * a * b = a
⊢ a + a * b + a * (a * b) = a
have rw₁ : a + a * b + a * b = a
Tactic: rw [← mul_assoc, mul_self, add_assoc, add_self, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
rw : a + a * b + a * a * b = a
rw₁ : a + a * b + a * b = a
⊢ a + a * b + a * (a * b) = a
have rw₂ : a + (a * b + a * b) = a
Tactic: rw [← mul_assoc, mul_self, add_assoc, add_self, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
rw : a + a * b + a * a * b = a
rw₁ : a + a * b + a * b = a
rw₂ : a + (a * b + a * b) = a
⊢ a + a * b + a * (a * b) = a
have rw₃ : a + 0 = a
Tactic: rw [← mul_assoc, mul_self, add_assoc, add_self, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
rw : a + a * b + a * a * b = a
rw₁ : a + a * b + a * b = a
rw₂ : a + (a * b + a * b) = a
rw₃ : a + 0 = a
⊢ a + a * b + a * (a * b) = a
have rw₄ : a = a
Tactic: rw [← mul_assoc, mul_self, add_assoc, add_self, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
⊢ a ⊓ (a ⊔ b) = a
have dsimp : a * (a + b + a * b) = a
Tactic: dsimp only [(· ⊔ ·), (· ⊓ ·)]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
⊢ a * (a + b + a * b) = a
have rw : a * (a + b) + a * (a * b) = a
Tactic: rw [mul_add, mul_add, mul_self, ← mul_assoc, mul_self, add_assoc, add_self, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
rw : a * (a + b) + a * (a * b) = a
⊢ a * (a + b + a * b) = a
have rw₁ : a * a + a * b + a * (a * b) = a
Tactic: rw [mul_add, mul_add, mul_self, ← mul_assoc, mul_self, add_assoc, add_self, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
rw : a * (a + b) + a * (a * b) = a
rw₁ : a * a + a * b + a * (a * b) = a
⊢ a * (a + b + a * b) = a
have rw₂ : a + a * b + a * (a * b) = a
Tactic: rw [mul_add, mul_add, mul_self, ← mul_assoc, mul_self, add_assoc, add_self, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
rw : a * (a + b) + a * (a * b) = a
rw₁ : a * a + a * b + a * (a * b) = a
rw₂ : a + a * b + a * (a * b) = a
⊢ a * (a + b + a * b) = a
have rw₃ : a + a * b + a * a * b = a
Tactic: rw [mul_add, mul_add, mul_self, ← mul_assoc, mul_self, add_assoc, add_self, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.BooleanRing (goal)
Goal:
α : Type u_1
inst : BooleanRing α
a b : α
rw : a * (a + b) + a * (a * b) = a
rw₁ : a * a + a * b + a * (a * b) = a
rw₂ : a + a * b + a * (a * b) = a
rw₃ : a + a * b + a * a * b = a
⊢ a * (a + b + a * b) = a
have rw₄ : a + a * b + a * b = a
Tactic: rw [mul_add, mul_add, mul_self, ← mul_assoc, mul_self, add_assoc, add_self, add_zero]