awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Regular.SMul (goal)
Goal:
R : Type u_1
M : Type u_3
inst : MonoidWithZero R
inst_1 : Zero M
inst_2 : MulActionWithZero R M
⊢ (¬∃ (x : M), ∃ (y : M), x ≠ y) ↔ ∀ (x y : M), x = y
have push : (∀ (x y : M), x = y) ↔ ∀ (x y : M), x = y
Tactic: push Not
-- Lean 4 proof step from Mathlib.Algebra.Regular.SMul (goal)
Goal:
R : Type u_1
M : Type u_3
a b : R
inst : CommSemigroup R
inst_1 : SMul R M
inst_2 : IsScalarTower R R M
⊢ IsSMulRegular M (a * b) ↔ IsSMulRegular M a ∧ IsSMulRegular M b
have rw : IsSMulRegular M (a * b) ↔ IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a)
Tactic: rw [← mul_and_mul_iff]
-- Lean 4 proof step from Mathlib.Algebra.Regular.SMul (goal)
Goal:
R : Type u_1
G : Type u_4
inst : Group G
inst_1 : MulAction G R
g : G
x y : R
h : Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ g • x) x) ((fun (x : R) ↦ g • x) y)
⊢ x = y
have h₁ : x = HSMul.hSMul (β := R) g⁻¹ ((fun (x : R) ↦ g • x) x)
Tactic: convert! congr_arg (g⁻¹ • ·) h using 1
-- Lean 4 proof step from Mathlib.Algebra.Regular.SMul (goal)
Goal:
R : Type u_1
G : Type u_4
inst : Group G
inst_1 : MulAction G R
g : G
x y : R
h : Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ g • x) x) ((fun (x : R) ↦ g • x) y)
h₁ : x = HSMul.hSMul (β := R) g⁻¹ ((fun (x : R) ↦ g • x) x)
⊢ x = y
have h₂ : y = HSMul.hSMul (β := R) g⁻¹ ((fun (x : R) ↦ g • x) y)
Tactic: convert! congr_arg (g⁻¹ • ·) h using 1
-- Lean 4 proof step from Mathlib.Algebra.Regular.SMul (goal)
Goal:
R : Type u_1
M : Type u_3
a : R
inst : Monoid R
inst_1 : MulAction R M
ua : IsUnit a
⊢ IsSMulRegular M a
have rcases : ∀ (a : Rˣ), IsSMulRegular M (↑a : R)
Tactic: rcases ua with ⟨a, rfl⟩
Cleared hypotheses: a, ua
-- Lean 4 proof step from Mathlib.Algebra.Regular.SMul (goal)
Goal:
R : Type u_1
M : Type u_3
inst : AddGroup M
inst_1 : DistribSMul R M
r : R
h : ∀ (m : M), r • m = 0 → m = 0
m₁ m₂ : M
eq : Eq.{u_3 + 1} (α := M) ((fun (x : M) ↦ r • x) m₁) ((fun (x : M) ↦ r • x) m₂)
⊢ r • (m₁ - m₂) = 0
have simp_rw : r • m₁ - r • m₂ = 0
Tactic: simp_rw [smul_sub, eq, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Regular.SMul (goal)
Goal:
R : Type u_1
M : Type u_3
inst : AddGroup M
inst_1 : DistribSMul R M
r : R
h : ∀ (m : M), r • m = 0 → m = 0
m₁ m₂ : M
eq : Eq.{u_3 + 1} (α := M) ((fun (x : M) ↦ r • x) m₁) ((fun (x : M) ↦ r • x) m₂)
simp_rw : r • m₁ - r • m₂ = 0
⊢ r • (m₁ - m₂) = 0
have simp_rw₁ : r • m₂ - r • m₂ = 0
Tactic: simp_rw [smul_sub, eq, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Action.Pointwise.Set (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : AddGroup β
inst_2 : DistribMulAction α β
a : α
t : Set β
⊢ a • -t = -(a • t)
have simp_rw : Eq (α := Set β) ((fun (x : β) ↦ a • x) '' (-t)) (-(fun (x : β) ↦ a • x) '' t)
Tactic: simp_rw [← image_smul, ← image_neg_eq_neg, image_image, smul_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Action.Pointwise.Set (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : AddGroup β
inst_2 : DistribMulAction α β
a : α
t : Set β
simp_rw : Eq (α := Set β) ((fun (x : β) ↦ a • x) '' (-t)) (-(fun (x : β) ↦ a • x) '' t)
⊢ a • -t = -(a • t)
have simp_rw₁ : Eq (α := Set β) ((fun (x : β) ↦ a • x) '' (fun (x : β) ↦ -x) '' t) ((fun (x : β) ↦ -x) '' (fun (x : β) ↦ a • x) '' t)
Tactic: simp_rw [← image_smul, ← image_neg_eq_neg, image_image, smul_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Action.Pointwise.Set (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : AddGroup β
inst_2 : DistribMulAction α β
a : α
t : Set β
simp_rw : Eq (α := Set β) ((fun (x : β) ↦ a • x) '' (-t)) (-(fun (x : β) ↦ a • x) '' t)
simp_rw₁ :
  Eq (α := Set β) ((fun (x : β) ↦ a • x) '' (fun (x : β) ↦ -x) '' t) ((fun (x : β) ↦ -x) '' (fun (x : β) ↦ a • x) '' t)
⊢ a • -t = -(a • t)
have simp_rw₂ : Eq (α := Set β) ((fun (x : β) ↦ a • -x) '' t) ((fun (x : β) ↦ -(a • x)) '' t)
Tactic: simp_rw [← image_smul, ← image_neg_eq_neg, image_image, smul_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Action.Pointwise.Set (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : AddGroup β
inst_2 : DistribMulAction α β
s : Set α
t : Set β
⊢ s • -t = -(s • t)
have simp_rw : HSMul.hSMul (β := Set β) s ((fun (x : β) ↦ -x) '' t) = (fun (x : β) ↦ -x) '' (s • t)
Tactic: simp_rw [← image_neg_eq_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Action.Pointwise.Set (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Semiring α
inst_1 : AddCommMonoid β
inst_2 : Module α β
inst_3 : IsDomain α
inst_4 : Module.IsTorsionFree α β
a : α
t : Set β
ha : a ≠ 0
⊢ 0 ∈ a • t ↔ 0 ∈ t
have refine : 0 ∈ a • t → 0 ∈ t
Tactic: refine ⟨?_, zero_mem_smul_set⟩
-- Lean 4 proof step from Mathlib.Algebra.Ring.Action.Pointwise.Set (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Semiring α
inst_1 : AddCommMonoid β
inst_2 : Module α β
inst_3 : IsDomain α
inst_4 : Module.IsTorsionFree α β
a : α
t : Set β
ha : a ≠ 0
b : β
hb : b ∈ t
h : Eq.{u_2 + 1} (α := β) ((fun (x : β) ↦ a • x) b) 0
⊢ 0 ∈ t
have rwa : ∀ (hb : 0 ∈ t) (h : Eq.{u_2 + 1} (α := β) ((fun (x : β) ↦ a • x) b) 0), 0 ∈ t
Tactic: rwa [(smul_eq_zero.1 h).resolve_left ha] at hb
Cleared hypotheses: hb, h
-- Lean 4 proof step from Mathlib.Algebra.Ring.Action.Pointwise.Set (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Semiring α
inst_1 : AddCommMonoid β
inst_2 : Module α β
inst_3 : IsDomain α
inst_4 : Module.IsTorsionFree α β
s : Set α
t : Set β
a : α
ha : a ∈ s
b : β
hb : b ∈ t
h : Eq.{u_2 + 1} (α := β) ((fun (x1 : α) (x2 : β) ↦ x1 • x2) a b) 0
⊢ 0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty
have inl : ∀ (ha : 0 ∈ s) (h : Eq.{u_2 + 1} (α := β) ((fun (x1 : α) (x2 : β) ↦ x1 • x2) 0 b) 0),
  0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty
Tactic: obtain rfl | rfl := smul_eq_zero.1 h
Cleared hypotheses: a, ha, h
-- Lean 4 proof step from Mathlib.Algebra.Ring.Action.Pointwise.Set (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Semiring α
inst_1 : AddCommMonoid β
inst_2 : Module α β
inst_3 : IsDomain α
inst_4 : Module.IsTorsionFree α β
s : Set α
t : Set β
a : α
ha : a ∈ s
b : β
hb : b ∈ t
h : Eq.{u_2 + 1} (α := β) ((fun (x1 : α) (x2 : β) ↦ x1 • x2) a b) 0
inl :
  ∀ (ha : 0 ∈ s) (h : Eq.{u_2 + 1} (α := β) ((fun (x1 : α) (x2 : β) ↦ x1 • x2) 0 b) 0),
    0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty
⊢ 0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty
have inr : ∀ (hb : 0 ∈ t) (h : Eq.{u_2 + 1} (α := β) ((fun (x1 : α) (x2 : β) ↦ x1 • x2) a 0) 0),
  0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty
Tactic: obtain rfl | rfl := smul_eq_zero.1 h
Cleared hypotheses: b, hb, h
-- Lean 4 proof step from Mathlib.Algebra.Ring.Action.Pointwise.Set (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : AddCommGroup β
inst_2 : Module α β
a : α
t : Set β
⊢ -a • t = -(a • t)
have simp_rw : Eq (α := Set β) ((fun (x : β) ↦ -a • x) '' t) (-(fun (x : β) ↦ a • x) '' t)
Tactic: simp_rw [← image_smul, ← image_neg_eq_neg, image_image, neg_smul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Action.Pointwise.Set (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : AddCommGroup β
inst_2 : Module α β
a : α
t : Set β
simp_rw : Eq (α := Set β) ((fun (x : β) ↦ -a • x) '' t) (-(fun (x : β) ↦ a • x) '' t)
⊢ -a • t = -(a • t)
have simp_rw₁ : Eq (α := Set β) ((fun (x : β) ↦ -a • x) '' t) ((fun (x : β) ↦ -x) '' (fun (x : β) ↦ a • x) '' t)
Tactic: simp_rw [← image_smul, ← image_neg_eq_neg, image_image, neg_smul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Action.Pointwise.Set (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : AddCommGroup β
inst_2 : Module α β
a : α
t : Set β
simp_rw : Eq (α := Set β) ((fun (x : β) ↦ -a • x) '' t) (-(fun (x : β) ↦ a • x) '' t)
simp_rw₁ : Eq (α := Set β) ((fun (x : β) ↦ -a • x) '' t) ((fun (x : β) ↦ -x) '' (fun (x : β) ↦ a • x) '' t)
⊢ -a • t = -(a • t)
have simp_rw₂ : Eq (α := Set β) ((fun (x : β) ↦ -a • x) '' t) ((fun (x : β) ↦ -(a • x)) '' t)
Tactic: simp_rw [← image_smul, ← image_neg_eq_neg, image_image, neg_smul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Action.Pointwise.Set (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : AddCommGroup β
inst_2 : Module α β
s : Set α
t : Set β
⊢ -s • t = -(s • t)
have simp_rw : HSMul.hSMul (α := Set α) ((fun (x : α) ↦ -x) '' s) t = (fun (x : β) ↦ -x) '' (s • t)
Tactic: simp_rw [← image_neg_eq_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Action.Rat (goal)
Goal:
R : Type u_1
inst : DivisionSemiring R
a : ℚ≥0
⊢ HSMul.hSMul (β := R) a 0 = 0
have rw : HMul.hMul (α := R) (↑a : R) 0 = 0
Tactic: rw [smul_def, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Action.Rat (goal)
Goal:
R : Type u_1
inst : DivisionSemiring R
a : ℚ≥0
rw : HMul.hMul (α := R) (↑a : R) 0 = 0
⊢ HSMul.hSMul (β := R) a 0 = 0
have rw₁ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [smul_def, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Action.Rat (goal)
Goal:
R : Type u_1
inst : DivisionSemiring R
a : ℚ≥0
x y : R
⊢ a • (x + y) = a • x + a • y
have rw : (↑a : R) * (x + y) = a • x + a • y
Tactic: rw [smul_def, smul_def, smul_def, mul_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Action.Rat (goal)
Goal:
R : Type u_1
inst : DivisionSemiring R
a : ℚ≥0
x y : R
rw : (↑a : R) * (x + y) = a • x + a • y
⊢ a • (x + y) = a • x + a • y
have rw₁ : (↑a : R) * (x + y) = (↑a : R) * x + a • y
Tactic: rw [smul_def, smul_def, smul_def, mul_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Action.Rat (goal)
Goal:
R : Type u_1
inst : DivisionSemiring R
a : ℚ≥0
x y : R
rw : (↑a : R) * (x + y) = a • x + a • y
rw₁ : (↑a : R) * (x + y) = (↑a : R) * x + a • y
⊢ a • (x + y) = a • x + a • y
have rw₂ : (↑a : R) * (x + y) = (↑a : R) * x + (↑a : R) * y
Tactic: rw [smul_def, smul_def, smul_def, mul_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Action.Rat (goal)
Goal:
R : Type u_1
inst : DivisionSemiring R
a : ℚ≥0
x y : R
rw : (↑a : R) * (x + y) = a • x + a • y
rw₁ : (↑a : R) * (x + y) = (↑a : R) * x + a • y
rw₂ : (↑a : R) * (x + y) = (↑a : R) * x + (↑a : R) * y
⊢ a • (x + y) = a • x + a • y
have rw₃ : (↑a : R) * x + (↑a : R) * y = (↑a : R) * x + (↑a : R) * y
Tactic: rw [smul_def, smul_def, smul_def, mul_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Action.Rat (goal)
Goal:
R : Type u_1
inst : DivisionRing R
a : ℚ
⊢ HSMul.hSMul (β := R) a 0 = 0
have rw : HMul.hMul (α := R) (↑a : R) 0 = 0
Tactic: rw [smul_def, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Action.Rat (goal)
Goal:
R : Type u_1
inst : DivisionRing R
a : ℚ
rw : HMul.hMul (α := R) (↑a : R) 0 = 0
⊢ HSMul.hSMul (β := R) a 0 = 0
have rw₁ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [smul_def, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Action.Rat (goal)
Goal:
R : Type u_1
inst : DivisionRing R
a : ℚ
x y : R
⊢ a • (x + y) = a • x + a • y
have rw : (↑a : R) * (x + y) = a • x + a • y
Tactic: rw [smul_def, smul_def, smul_def, mul_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Action.Rat (goal)
Goal:
R : Type u_1
inst : DivisionRing R
a : ℚ
x y : R
rw : (↑a : R) * (x + y) = a • x + a • y
⊢ a • (x + y) = a • x + a • y
have rw₁ : (↑a : R) * (x + y) = (↑a : R) * x + a • y
Tactic: rw [smul_def, smul_def, smul_def, mul_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Action.Rat (goal)
Goal:
R : Type u_1
inst : DivisionRing R
a : ℚ
x y : R
rw : (↑a : R) * (x + y) = a • x + a • y
rw₁ : (↑a : R) * (x + y) = (↑a : R) * x + a • y
⊢ a • (x + y) = a • x + a • y
have rw₂ : (↑a : R) * (x + y) = (↑a : R) * x + (↑a : R) * y
Tactic: rw [smul_def, smul_def, smul_def, mul_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Action.Rat (goal)
Goal:
R : Type u_1
inst : DivisionRing R
a : ℚ
x y : R
rw : (↑a : R) * (x + y) = a • x + a • y
rw₁ : (↑a : R) * (x + y) = (↑a : R) * x + a • y
rw₂ : (↑a : R) * (x + y) = (↑a : R) * x + (↑a : R) * y
⊢ a • (x + y) = a • x + a • y
have rw₃ : (↑a : R) * x + (↑a : R) * y = (↑a : R) * x + (↑a : R) * y
Tactic: rw [smul_def, smul_def, smul_def, mul_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Action.Submonoid (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Monoid M
inst_1 : AddMonoid α
inst_2 : DistribMulAction M α
a b : α
ha : a ∈ MulAction.fixedPoints M α
hb : b ∈ MulAction.fixedPoints M α
x : M
⊢ x • (a + b) = a + b
have rw : x • a + x • b = a + b
Tactic: rw [smul_add, ha, hb]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Action.Submonoid (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Monoid M
inst_1 : AddMonoid α
inst_2 : DistribMulAction M α
a b : α
ha : a ∈ MulAction.fixedPoints M α
hb : b ∈ MulAction.fixedPoints M α
x : M
rw : x • a + x • b = a + b
⊢ x • (a + b) = a + b
have rw₁ : a + x • b = a + b
Tactic: rw [smul_add, ha, hb]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Action.Submonoid (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Monoid M
inst_1 : AddMonoid α
inst_2 : DistribMulAction M α
a b : α
ha : a ∈ MulAction.fixedPoints M α
hb : b ∈ MulAction.fixedPoints M α
x : M
rw : x • a + x • b = a + b
rw₁ : a + x • b = a + b
⊢ x • (a + b) = a + b
have rw₂ : a + b = a + b
Tactic: rw [smul_add, ha, hb]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Action.Submonoid (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Monoid M
inst_1 : AddGroup α
inst_2 : DistribMulAction M α
x : α
ha : x ∈ AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (addSubmonoid M α))
x_1 : M
⊢ x_1 • -x = -x
have rw : -(x_1 • x) = -x
Tactic: rw [smul_neg, ha]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Action.Submonoid (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Monoid M
inst_1 : AddGroup α
inst_2 : DistribMulAction M α
x : α
ha : x ∈ AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (addSubmonoid M α))
x_1 : M
rw : -(x_1 • x) = -x
⊢ x_1 • -x = -x
have rw₁ : -x = -x
Tactic: rw [smul_neg, ha]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Associator (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
h : Std.Associative fun (x y : R) ↦ x * y
⊢ Eq.{u_1 + 1} (α := (x y z : R) → R) associator 0
have h₁ : ∀ (x y z : R), associator x y z = 0 x y z
Tactic: ext x y z
-- Lean 4 proof step from Mathlib.Algebra.Ring.Associator (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
a b c d : R
⊢ a * associator b c d - associator (a * b) c d + associator a (b * c) d - associator a b (c * d) +
      associator a b c * d =
    0
have simp : a * (b * c * d) - a * (b * (c * d)) - (a * b * c * d - a * b * (c * d)) + (a * (b * c) * d - a * (b * c * d)) -
      (a * b * (c * d) - a * (b * (c * d))) +
    (a * b * c * d - a * (b * c) * d) =
  0
Tactic: simp only [associator, mul_sub, sub_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Associator (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
⊢ Eq.{u_1 + 1} (α := R →+ R →+ R) (comp mul (mulLeft 0)) 0
have h : ∀ (x x_1 : R),
  Eq (α := R) ((((comp mul (mulLeft 0) : (a : R) → R →+ R) x : R →+ R) : (a : R) → R) x_1 : R)
    ((((0 : (a : R) → R →+ R) x : R →+ R) : (a : R) → R) x_1 : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Ring.Associator (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
x y : R
⊢ comp mul (mulLeft (x + y)) = HAdd.hAdd (α := R →+ R →+ R) (comp mul (mulLeft x)) (comp mul (mulLeft y))
have h : ∀ (x_1 x_2 : R),
  Eq (α := R) ((((comp mul (mulLeft (x + y)) : (a : R) → R →+ R) x_1 : R →+ R) : (a : R) → R) x_2 : R)
    ((((HAdd.hAdd (α := R →+ R →+ R) (comp mul (mulLeft x)) (comp mul (mulLeft y)) : (a : R) → R →+ R) x_1 : R →+ R) :
          (a : R) → R)
        x_2 :
      R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Ring.Associator (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
⊢ Eq.{u_1 + 1} (α := R →+ R →+ R) (compr₂ mul (mulLeft 0)) 0
have h : ∀ (x x_1 : R),
  Eq (α := R) ((((compr₂ mul (mulLeft 0) : (a : R) → R →+ R) x : R →+ R) : (a : R) → R) x_1 : R)
    ((((0 : (a : R) → R →+ R) x : R →+ R) : (a : R) → R) x_1 : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Ring.Associator (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
x y : R
⊢ compr₂ mul (mulLeft (x + y)) = HAdd.hAdd (α := R →+ R →+ R) (compr₂ mul (mulLeft x)) (compr₂ mul (mulLeft y))
have h : ∀ (x_1 x_2 : R),
  Eq (α := R) ((((compr₂ mul (mulLeft (x + y)) : (a : R) → R →+ R) x_1 : R →+ R) : (a : R) → R) x_2 : R)
    ((((HAdd.hAdd (α := R →+ R →+ R) (compr₂ mul (mulLeft x)) (compr₂ mul (mulLeft y)) : (a : R) → R →+ R) x_1 :
            R →+ R) :
          (a : R) → R)
        x_2 :
      R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Ring.Associator (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
h : Eq.{u_1 + 1} (α := R →+ R →+ R →+ R) mulLeft₃ mulRight₃
x y z : R
⊢ x * y * z = x * (y * z)
have rw : (((((mulLeft₃ : (a : R) → R →+ R →+ R) x : R →+ R →+ R) : (a : R) → R →+ R) y : R →+ R) : (a : R) → R) z = x * (y * z)
Tactic: rw [← mulLeft₃_apply, ← mulRight₃_apply, h]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Associator (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
h : Eq.{u_1 + 1} (α := R →+ R →+ R →+ R) mulLeft₃ mulRight₃
x y z : R
rw :
  (((((mulLeft₃ : (a : R) → R →+ R →+ R) x : R →+ R →+ R) : (a : R) → R →+ R) y : R →+ R) : (a : R) → R) z = x * (y * z)
⊢ x * y * z = x * (y * z)
have rw₁ : Eq (α := R)
  ((((((mulLeft₃ : (a : R) → R →+ R →+ R) x : R →+ R →+ R) : (a : R) → R →+ R) y : R →+ R) : (a : R) → R) z : R)
  ((((((mulRight₃ : (a : R) → R →+ R →+ R) x : R →+ R →+ R) : (a : R) → R →+ R) y : R →+ R) : (a : R) → R) z : R)
Tactic: rw [← mulLeft₃_apply, ← mulRight₃_apply, h]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Associator (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
h : Eq.{u_1 + 1} (α := R →+ R →+ R →+ R) mulLeft₃ mulRight₃
x y z : R
rw :
  (((((mulLeft₃ : (a : R) → R →+ R →+ R) x : R →+ R →+ R) : (a : R) → R →+ R) y : R →+ R) : (a : R) → R) z = x * (y * z)
rw₁ :
  Eq (α := R)
    ((((((mulLeft₃ : (a : R) → R →+ R →+ R) x : R →+ R →+ R) : (a : R) → R →+ R) y : R →+ R) : (a : R) → R) z : R)
    ((((((mulRight₃ : (a : R) → R →+ R →+ R) x : R →+ R →+ R) : (a : R) → R →+ R) y : R →+ R) : (a : R) → R) z : R)
⊢ x * y * z = x * (y * z)
have rw₂ : Eq (α := R)
  ((((((mulRight₃ : (a : R) → R →+ R →+ R) x : R →+ R →+ R) : (a : R) → R →+ R) y : R →+ R) : (a : R) → R) z : R)
  ((((((mulRight₃ : (a : R) → R →+ R →+ R) x : R →+ R →+ R) : (a : R) → R →+ R) y : R →+ R) : (a : R) → R) z : R)
Tactic: rw [← mulLeft₃_apply, ← mulRight₃_apply, h]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Associator (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
h : Std.Associative fun (x y : R) ↦ x * y
⊢ Eq.{u_1 + 1} (α := R →+ R →+ R →+ R) mulLeft₃ mulRight₃
have h₁ : ∀ (x y z : R),
  Eq (α := R)
    ((((((mulLeft₃ : (a : R) → R →+ R →+ R) x : R →+ R →+ R) : (a : R) → R →+ R) y : R →+ R) : (a : R) → R) z : R)
    ((((((mulRight₃ : (a : R) → R →+ R →+ R) x : R →+ R →+ R) : (a : R) → R →+ R) y : R →+ R) : (a : R) → R) z : R)
Tactic: ext x y z
-- Lean 4 proof step from Mathlib.Algebra.Ring.Aut (goal)
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]
⊢ Eq (α := (a : R) → R) (⇑(f ^ (n + 1)) : (a : R) → R) (⇑f : (a : R) → R)^[n + 1]
have succ : ∀ (x : R), (f ^ (n + 1) : (a : R) → R) x = (⇑f : (a : R) → R)^[n + 1] x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Ring.Aut (goal)
Goal:
R : Type u_1
inst : Mul R
inst_1 : Add R
f : R ≃+* R
n : ℕ
⊢ Eq (α := (a : R) → R) (⇑(f ^ n) : (a : R) → R) (⇑f : (a : R) → R)^[n]
have zero : Eq (α := (a : R) → R) (⇑(HPow.hPow (β := ℕ) f 0) : (a : R) → R) (⇑f : (a : R) → R)^[0]
Tactic: induction n with
  | zero =>
    simp
  | succ n ih =>
    ext
    simp [pow_succ, ih]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Ring.Aut (goal)
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]
⊢ Eq (α := (a : R) → R) (⇑(f ^ n) : (a : R) → R) (⇑f : (a : R) → R)^[n]
have 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]
Tactic: induction n with
  | zero =>
    simp
  | succ n ih =>
    ext
    simp [pow_succ, ih]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (hypothesis)
Goal:
α : Type u_3
inst : NonUnitalCommRing α
b c x : α
h : x * x - b * x + c = 0
⊢ ∃ (y : α), y * y - b * y + c = 0 ∧ x + y = b ∧ x * y = c
have this : 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])
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (goal)
Goal:
α : Type u_3
inst : NonUnitalCommRing α
b c x : α
h : x * x - b * x + c = 0
this : c = x * (b - x)
⊢ x * (b - x) = c
have rw : x * (b - x) = x * (b - x)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (goal)
Goal:
α : Type u_3
inst : NonUnitalCommRing α
b c x : α
h : x * x - b * x + c = 0
this : c = x * (b - x)
⊢ ∃ (y : α), y * y - b * y + c = 0 ∧ x + y = b ∧ x * y = c
have refine : (b - x) * (b - x) - b * (b - x) + c = 0
Tactic: refine ⟨b - x, ?_, by simp, by rw [this]⟩
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (goal)
Goal:
α : Type u_3
inst : NonUnitalCommRing α
b c x : α
h : x * x - b * x + c = 0
this : c = x * (b - x)
⊢ (b - x) * (b - x) - b * (b - x) + c = 0
have rw : (b - x) * (b - x) - b * (b - x) + x * (b - x) = 0
Tactic: rw [this, sub_add, ← sub_mul, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (goal)
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
⊢ (b - x) * (b - x) - b * (b - x) + c = 0
have rw₁ : (b - x) * (b - x) - (b * (b - x) - x * (b - x)) = 0
Tactic: rw [this, sub_add, ← sub_mul, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (goal)
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
⊢ (b - x) * (b - x) - b * (b - x) + c = 0
have rw₂ : (b - x) * (b - x) - (b - x) * (b - x) = 0
Tactic: rw [this, sub_add, ← sub_mul, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (goal)
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
⊢ (b - x) * (b - x) - b * (b - x) + c = 0
have rw₃ : Eq.{u_3 + 1} (α := α) 0 0
Tactic: rw [this, sub_add, ← sub_mul, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (goal)
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
⊢ Eq.{u_3 + 1} (α := R) ((fun (x : R) ↦ r * x) r') ((fun (x : R) ↦ r * x) 0)
have simp_rw₂ : 0 = r * 0
Tactic: simp_rw [eq, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (goal)
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₂)
⊢ r * (r₁ - r₂) = 0
have simp_rw : r * r₁ - r * r₂ = 0
Tactic: simp_rw [mul_sub, eq, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (goal)
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
⊢ r * (r₁ - r₂) = 0
have simp_rw₁ : r * r₂ - r * r₂ = 0
Tactic: simp_rw [mul_sub, eq, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Basic (goal)
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
⊢ Eq.{u_3 + 1} (α := R) ((fun (x : R) ↦ x * r) r') ((fun (x : R) ↦ x * r) 0)
have simp_rw₂ : 0 = 0 * r
Tactic: simp_rw [eq, zero_mul]
-- 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₂)
⊢ (r₁ - r₂) * r = 0
have simp_rw : r₁ * r - r₂ * r = 0
Tactic: simp_rw [sub_mul, eq, sub_self]