awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : Ring R
a : R
inst_1 : NoZeroDivisors R
⊢ HPow.hPow (β := ℕ) a 2 = 1 ↔ a = 1 ∨ a = -1
have rw : HPow.hPow (β := ℕ) a 2 = 1 ↔ HPow.hPow (β := ℕ) a 2 = HPow.hPow (α := R) (β := ℕ) 1 2
Tactic: rw [← (Commute.one_right a).sq_eq_sq_iff_eq_or_eq_neg, one_pow]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : Ring R
a : R
inst_1 : NoZeroDivisors R
rw : HPow.hPow (β := ℕ) a 2 = 1 ↔ HPow.hPow (β := ℕ) a 2 = HPow.hPow (α := R) (β := ℕ) 1 2
⊢ HPow.hPow (β := ℕ) a 2 = 1 ↔ a = 1 ∨ a = -1
have rw₁ : HPow.hPow (β := ℕ) a 2 = 1 ↔ HPow.hPow (β := ℕ) a 2 = 1
Tactic: rw [← (Commute.one_right a).sq_eq_sq_iff_eq_or_eq_neg, one_pow]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : NonAssocRing R
a : R
⊢ a * a - 1 = (a + 1) * (a - 1)
have rw : a * a - 1 = a * a - HMul.hMul (α := R) 1 1
Tactic: rw [← (Commute.one_right a).mul_self_sub_mul_self_eq, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : NonAssocRing R
a : R
rw : a * a - 1 = a * a - HMul.hMul (α := R) 1 1
⊢ a * a - 1 = (a + 1) * (a - 1)
have rw₁ : a * a - 1 = a * a - 1
Tactic: rw [← (Commute.one_right a).mul_self_sub_mul_self_eq, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : NonAssocRing R
inst_1 : NoZeroDivisors R
a : R
⊢ a * a = 1 ↔ a = 1 ∨ a = -1
have rw : a * a = 1 ↔ a * a = HMul.hMul (α := R) 1 1
Tactic: rw [← (Commute.one_right a).mul_self_eq_mul_self_iff, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : NonAssocRing R
inst_1 : NoZeroDivisors R
a : R
rw : a * a = 1 ↔ a * a = HMul.hMul (α := R) 1 1
⊢ a * a = 1 ↔ a = 1 ∨ a = -1
have rw₁ : a * a = 1 ↔ a * a = 1
Tactic: rw [← (Commute.one_right a).mul_self_eq_mul_self_iff, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : CommRing R
a b : R
⊢ HPow.hPow (β := ℕ) (a - b) 2 = HPow.hPow (β := ℕ) a 2 - 2 * a * b + HPow.hPow (β := ℕ) b 2
have rw : HPow.hPow (β := ℕ) (a + -b) 2 = HPow.hPow (β := ℕ) a 2 - 2 * a * b + HPow.hPow (β := ℕ) b 2
Tactic: rw [sub_eq_add_neg, add_sq, neg_sq, mul_neg, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : CommRing R
a b : R
rw : HPow.hPow (β := ℕ) (a + -b) 2 = HPow.hPow (β := ℕ) a 2 - 2 * a * b + HPow.hPow (β := ℕ) b 2
⊢ HPow.hPow (β := ℕ) (a - b) 2 = HPow.hPow (β := ℕ) a 2 - 2 * a * b + HPow.hPow (β := ℕ) b 2
have rw₁ : HPow.hPow (β := ℕ) a 2 + 2 * a * -b + HPow.hPow (β := ℕ) (-b) 2 =
  HPow.hPow (β := ℕ) a 2 - 2 * a * b + HPow.hPow (β := ℕ) b 2
Tactic: rw [sub_eq_add_neg, add_sq, neg_sq, mul_neg, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : CommRing R
a b : R
rw : HPow.hPow (β := ℕ) (a + -b) 2 = HPow.hPow (β := ℕ) a 2 - 2 * a * b + HPow.hPow (β := ℕ) b 2
rw₁ :
  HPow.hPow (β := ℕ) a 2 + 2 * a * -b + HPow.hPow (β := ℕ) (-b) 2 =
    HPow.hPow (β := ℕ) a 2 - 2 * a * b + HPow.hPow (β := ℕ) b 2
⊢ HPow.hPow (β := ℕ) (a - b) 2 = HPow.hPow (β := ℕ) a 2 - 2 * a * b + HPow.hPow (β := ℕ) b 2
have rw₂ : HPow.hPow (β := ℕ) a 2 + 2 * a * -b + HPow.hPow (β := ℕ) b 2 =
  HPow.hPow (β := ℕ) a 2 - 2 * a * b + HPow.hPow (β := ℕ) b 2
Tactic: rw [sub_eq_add_neg, add_sq, neg_sq, mul_neg, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : CommRing R
a b : R
rw : HPow.hPow (β := ℕ) (a + -b) 2 = HPow.hPow (β := ℕ) a 2 - 2 * a * b + HPow.hPow (β := ℕ) b 2
rw₁ :
  HPow.hPow (β := ℕ) a 2 + 2 * a * -b + HPow.hPow (β := ℕ) (-b) 2 =
    HPow.hPow (β := ℕ) a 2 - 2 * a * b + HPow.hPow (β := ℕ) b 2
rw₂ :
  HPow.hPow (β := ℕ) a 2 + 2 * a * -b + HPow.hPow (β := ℕ) b 2 =
    HPow.hPow (β := ℕ) a 2 - 2 * a * b + HPow.hPow (β := ℕ) b 2
⊢ HPow.hPow (β := ℕ) (a - b) 2 = HPow.hPow (β := ℕ) a 2 - 2 * a * b + HPow.hPow (β := ℕ) b 2
have rw₃ : HPow.hPow (β := ℕ) a 2 + -(2 * a * b) + HPow.hPow (β := ℕ) b 2 =
  HPow.hPow (β := ℕ) a 2 - 2 * a * b + HPow.hPow (β := ℕ) b 2
Tactic: rw [sub_eq_add_neg, add_sq, neg_sq, mul_neg, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : CommRing R
a b : R
rw : HPow.hPow (β := ℕ) (a + -b) 2 = HPow.hPow (β := ℕ) a 2 - 2 * a * b + HPow.hPow (β := ℕ) b 2
rw₁ :
  HPow.hPow (β := ℕ) a 2 + 2 * a * -b + HPow.hPow (β := ℕ) (-b) 2 =
    HPow.hPow (β := ℕ) a 2 - 2 * a * b + HPow.hPow (β := ℕ) b 2
rw₂ :
  HPow.hPow (β := ℕ) a 2 + 2 * a * -b + HPow.hPow (β := ℕ) b 2 =
    HPow.hPow (β := ℕ) a 2 - 2 * a * b + HPow.hPow (β := ℕ) b 2
rw₃ :
  HPow.hPow (β := ℕ) a 2 + -(2 * a * b) + HPow.hPow (β := ℕ) b 2 =
    HPow.hPow (β := ℕ) a 2 - 2 * a * b + HPow.hPow (β := ℕ) b 2
⊢ HPow.hPow (β := ℕ) (a - b) 2 = HPow.hPow (β := ℕ) a 2 - 2 * a * b + HPow.hPow (β := ℕ) b 2
have rw₄ : HPow.hPow (β := ℕ) a 2 - 2 * a * b + HPow.hPow (β := ℕ) b 2 =
  HPow.hPow (β := ℕ) a 2 - 2 * a * b + HPow.hPow (β := ℕ) b 2
Tactic: rw [sub_eq_add_neg, add_sq, neg_sq, mul_neg, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : CommRing R
a b : R
⊢ HPow.hPow (β := ℕ) (a - b) 2 = HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 - 2 * a * b
have rw : HPow.hPow (β := ℕ) (a + -b) 2 = HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 - 2 * a * b
Tactic: rw [sub_eq_add_neg, add_sq', neg_sq, mul_neg, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : CommRing R
a b : R
rw : HPow.hPow (β := ℕ) (a + -b) 2 = HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 - 2 * a * b
⊢ HPow.hPow (β := ℕ) (a - b) 2 = HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 - 2 * a * b
have rw₁ : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) (-b) 2 + 2 * a * -b =
  HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 - 2 * a * b
Tactic: rw [sub_eq_add_neg, add_sq', neg_sq, mul_neg, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : CommRing R
a b : R
rw : HPow.hPow (β := ℕ) (a + -b) 2 = HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 - 2 * a * b
rw₁ :
  HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) (-b) 2 + 2 * a * -b =
    HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 - 2 * a * b
⊢ HPow.hPow (β := ℕ) (a - b) 2 = HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 - 2 * a * b
have rw₂ : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 2 * a * -b =
  HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 - 2 * a * b
Tactic: rw [sub_eq_add_neg, add_sq', neg_sq, mul_neg, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : CommRing R
a b : R
rw : HPow.hPow (β := ℕ) (a + -b) 2 = HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 - 2 * a * b
rw₁ :
  HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) (-b) 2 + 2 * a * -b =
    HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 - 2 * a * b
rw₂ :
  HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 2 * a * -b =
    HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 - 2 * a * b
⊢ HPow.hPow (β := ℕ) (a - b) 2 = HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 - 2 * a * b
have rw₃ : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + -(2 * a * b) =
  HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 - 2 * a * b
Tactic: rw [sub_eq_add_neg, add_sq', neg_sq, mul_neg, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : CommRing R
a b : R
rw : HPow.hPow (β := ℕ) (a + -b) 2 = HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 - 2 * a * b
rw₁ :
  HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) (-b) 2 + 2 * a * -b =
    HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 - 2 * a * b
rw₂ :
  HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 2 * a * -b =
    HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 - 2 * a * b
rw₃ :
  HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + -(2 * a * b) =
    HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 - 2 * a * b
⊢ HPow.hPow (β := ℕ) (a - b) 2 = HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 - 2 * a * b
have rw₄ : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 - 2 * a * b =
  HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 - 2 * a * b
Tactic: rw [sub_eq_add_neg, add_sq', neg_sq, mul_neg, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : CommRing R
a b : R
⊢ HPow.hPow (β := ℕ) (a - b) 2 = HPow.hPow (β := ℕ) (b - a) 2
have rw : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 - 2 * a * b = HPow.hPow (β := ℕ) (b - a) 2
Tactic: rw [sub_sq', mul_right_comm, add_comm, sub_sq']
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : CommRing R
a b : R
rw : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 - 2 * a * b = HPow.hPow (β := ℕ) (b - a) 2
⊢ HPow.hPow (β := ℕ) (a - b) 2 = HPow.hPow (β := ℕ) (b - a) 2
have rw₁ : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 - 2 * b * a = HPow.hPow (β := ℕ) (b - a) 2
Tactic: rw [sub_sq', mul_right_comm, add_comm, sub_sq']
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : CommRing R
a b : R
rw : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 - 2 * a * b = HPow.hPow (β := ℕ) (b - a) 2
rw₁ : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 - 2 * b * a = HPow.hPow (β := ℕ) (b - a) 2
⊢ HPow.hPow (β := ℕ) (a - b) 2 = HPow.hPow (β := ℕ) (b - a) 2
have rw₂ : HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) a 2 - 2 * b * a = HPow.hPow (β := ℕ) (b - a) 2
Tactic: rw [sub_sq', mul_right_comm, add_comm, sub_sq']
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : CommRing R
a b : R
rw : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 - 2 * a * b = HPow.hPow (β := ℕ) (b - a) 2
rw₁ : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 - 2 * b * a = HPow.hPow (β := ℕ) (b - a) 2
rw₂ : HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) a 2 - 2 * b * a = HPow.hPow (β := ℕ) (b - a) 2
⊢ HPow.hPow (β := ℕ) (a - b) 2 = HPow.hPow (β := ℕ) (b - a) 2
have rw₃ : HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) a 2 - 2 * b * a =
  HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) a 2 - 2 * b * a
Tactic: rw [sub_sq', mul_right_comm, add_comm, sub_sq']
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
a b : Rˣ
⊢ HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) b 2 ↔ a = b ∨ a = -b
have simp_rw : (↑(HPow.hPow (β := ℕ) a 2) : R) = (↑(HPow.hPow (β := ℕ) b 2) : R) ↔ (↑a : R) = (↑b : R) ∨ (↑a : R) = (↑(-b) : R)
Tactic: simp_rw [Units.ext_iff, val_pow_eq_pow_val, sq_eq_sq_iff_eq_or_eq_neg, Units.val_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
a b : Rˣ
simp_rw :
  (↑(HPow.hPow (β := ℕ) a 2) : R) = (↑(HPow.hPow (β := ℕ) b 2) : R) ↔ (↑a : R) = (↑b : R) ∨ (↑a : R) = (↑(-b) : R)
⊢ HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) b 2 ↔ a = b ∨ a = -b
have simp_rw₁ : HPow.hPow (β := ℕ) (↑a : R) 2 = HPow.hPow (β := ℕ) (↑b : R) 2 ↔ (↑a : R) = (↑b : R) ∨ (↑a : R) = (↑(-b) : R)
Tactic: simp_rw [Units.ext_iff, val_pow_eq_pow_val, sq_eq_sq_iff_eq_or_eq_neg, Units.val_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
a b : Rˣ
simp_rw :
  (↑(HPow.hPow (β := ℕ) a 2) : R) = (↑(HPow.hPow (β := ℕ) b 2) : R) ↔ (↑a : R) = (↑b : R) ∨ (↑a : R) = (↑(-b) : R)
simp_rw₁ : HPow.hPow (β := ℕ) (↑a : R) 2 = HPow.hPow (β := ℕ) (↑b : R) 2 ↔ (↑a : R) = (↑b : R) ∨ (↑a : R) = (↑(-b) : R)
⊢ HPow.hPow (β := ℕ) a 2 = HPow.hPow (β := ℕ) b 2 ↔ a = b ∨ a = -b
have simp_rw₂ : (↑a : R) = (↑b : R) ∨ (↑a : R) = -(↑b : R) ↔ (↑a : R) = (↑b : R) ∨ (↑a : R) = (↑(-b) : R)
Tactic: simp_rw [Units.ext_iff, val_pow_eq_pow_val, sq_eq_sq_iff_eq_or_eq_neg, Units.val_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : NoZeroDivisors R
u : Rˣ
⊢ u⁻¹ = u ↔ u = 1 ∨ u = -1
have rw : u * u = 1 ↔ u = 1 ∨ u = -1
Tactic: rw [inv_eq_iff_mul_eq_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : NoZeroDivisors R
u : Rˣ
⊢ u * u = 1 ↔ u = 1 ∨ u = -1
have simp : (↑(u * u) : R) = (↑1 : R) ↔ (↑u : R) = (↑1 : R) ∨ (↑u : R) = (↑(-1) : R)
Tactic: simp only [Units.ext_iff]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Commute (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : NoZeroDivisors R
u : Rˣ
⊢ (↑(u * u) : R) = (↑1 : R) ↔ (↑u : R) = (↑1 : R) ∨ (↑u : R) = (↑(-1) : R)
have push_cast : (↑u : R) * (↑u : R) = 1 ↔ (↑u : R) = 1 ∨ (↑u : R) = -1
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Algebra.Ring.CompTypeclasses (goal)
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
inst_2 : RingHomInvPair σ σ'
x : R₁
⊢ (σ' : (a : R₂) → R₁) ((σ : (a : R₁) → R₂) x : R₂) = x
have rw : (RingHom.id R₁ : (a : R₁) → R₁) x = x
Tactic: rw [← RingHom.comp_apply, comp_eq]
-- Lean 4 proof step from Mathlib.Algebra.Ring.CompTypeclasses (goal)
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
inst_2 : RingHomInvPair σ σ'
x : R₂
⊢ (σ : (a : R₁) → R₂) ((σ' : (a : R₂) → R₁) x : R₁) = x
have rw : (RingHom.id R₂ : (a : R₂) → R₂) x = x
Tactic: rw [← RingHom.comp_apply, comp_eq₂]
-- Lean 4 proof step from Mathlib.Algebra.Ring.CompTypeclasses (hypothesis)
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_3 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_4 : RingHomSurjective σ₁₂
inst_5 : RingHomSurjective σ₂₃
⊢ Function.Surjective.{u_1 + 1, u_3 + 1} (α := R₁) (β := R₃) (⇑σ₁₃ : (a : R₁) → R₃)
have this : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R₁) (β := R₃)
  (Function.comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := R₂) (⇑σ₂₃ : (a : R₂) → R₃) (⇑σ₁₂ : (a : R₁) → R₂))
Tactic: have := σ₂₃.surjective.comp σ₁₂.surjective
-- Lean 4 proof step from Mathlib.Algebra.Ring.CompTypeclasses (goal)
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_3 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_4 : RingHomSurjective σ₁₂
inst_5 : RingHomSurjective σ₂₃
this :
  Function.Surjective.{u_1 + 1, u_3 + 1} (α := R₁) (β := R₃)
    (Function.comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := R₂) (⇑σ₂₃ : (a : R₂) → R₃) (⇑σ₁₂ : (a : R₁) → R₂))
⊢ Function.Surjective.{u_1 + 1, u_3 + 1} (α := R₁) (β := R₃) (⇑σ₁₃ : (a : R₁) → R₃)
have rwa : ∀ (this : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R₁) (β := R₃) (⇑(σ₂₃.comp σ₁₂) : (a : R₁) → R₃)),
  Function.Surjective.{u_1 + 1, u_3 + 1} (α := R₁) (β := R₃) (⇑σ₁₃ : (a : R₁) → R₃)
Tactic: rwa [← RingHom.coe_comp, RingHomCompTriple.comp_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Ring.CompTypeclasses (goal)
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_3 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_4 : RingHomSurjective σ₁₂
inst_5 : RingHomSurjective σ₂₃
this :
  Function.Surjective.{u_1 + 1, u_3 + 1} (α := R₁) (β := R₃)
    (Function.comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := R₂) (⇑σ₂₃ : (a : R₂) → R₃) (⇑σ₁₂ : (a : R₁) → R₂))
rwa :
  ∀ (this : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R₁) (β := R₃) (⇑(σ₂₃.comp σ₁₂) : (a : R₁) → R₃)),
    Function.Surjective.{u_1 + 1, u_3 + 1} (α := R₁) (β := R₃) (⇑σ₁₃ : (a : R₁) → R₃)
⊢ Function.Surjective.{u_1 + 1, u_3 + 1} (α := R₁) (β := R₃) (⇑σ₁₃ : (a : R₁) → R₃)
have rwa₁ : ∀ (this : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R₁) (β := R₃) (⇑σ₁₃ : (a : R₁) → R₃)),
  Function.Surjective.{u_1 + 1, u_3 + 1} (α := R₁) (β := R₃) (⇑σ₁₃ : (a : R₁) → R₃)
Tactic: rwa [← RingHom.coe_comp, RingHomCompTriple.comp_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Ring.Defs (goal)
Goal:
α : Type u
inst : Add α
inst_1 : MulOneClass α
inst_2 : RightDistribClass α
a b : α
⊢ (a + 1) * b = a * b + b
have rw : a * b + 1 * b = a * b + b
Tactic: rw [add_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Defs (goal)
Goal:
α : Type u
inst : Add α
inst_1 : MulOneClass α
inst_2 : RightDistribClass α
a b : α
rw : a * b + 1 * b = a * b + b
⊢ (a + 1) * b = a * b + b
have rw₁ : a * b + b = a * b + b
Tactic: rw [add_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Defs (goal)
Goal:
α : Type u
inst : Add α
inst_1 : MulOneClass α
inst_2 : LeftDistribClass α
a b : α
⊢ a * (b + 1) = a * b + a
have rw : a * b + a * 1 = a * b + a
Tactic: rw [mul_add, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Defs (goal)
Goal:
α : Type u
inst : Add α
inst_1 : MulOneClass α
inst_2 : LeftDistribClass α
a b : α
rw : a * b + a * 1 = a * b + a
⊢ a * (b + 1) = a * b + a
have rw₁ : a * b + a = a * b + a
Tactic: rw [mul_add, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Defs (goal)
Goal:
α : Type u
inst : Add α
inst_1 : MulOneClass α
inst_2 : RightDistribClass α
a b : α
⊢ (1 + a) * b = b + a * b
have rw : 1 * b + a * b = b + a * b
Tactic: rw [add_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Defs (goal)
Goal:
α : Type u
inst : Add α
inst_1 : MulOneClass α
inst_2 : RightDistribClass α
a b : α
rw : 1 * b + a * b = b + a * b
⊢ (1 + a) * b = b + a * b
have rw₁ : b + a * b = b + a * b
Tactic: rw [add_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Defs (goal)
Goal:
α : Type u
inst : Add α
inst_1 : MulOneClass α
inst_2 : LeftDistribClass α
a b : α
⊢ a * (1 + b) = a + a * b
have rw : a * 1 + a * b = a + a * b
Tactic: rw [mul_add, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Defs (goal)
Goal:
α : Type u
inst : Add α
inst_1 : MulOneClass α
inst_2 : LeftDistribClass α
a b : α
rw : a * 1 + a * b = a + a * b
⊢ a * (1 + b) = a + a * b
have rw₁ : a + a * b = a + a * b
Tactic: rw [mul_add, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Defs (goal)
Goal:
α : Type u
inst : NonAssocSemiring α
n : α
⊢ 1 * n + 1 * n = n + n
have rw : n + n = n + n
Tactic: rw [one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Defs (goal)
Goal:
α : Type u
inst : NonAssocSemiring α
n : α
⊢ n * 1 + n * 1 = n + n
have rw : n + n = n + n
Tactic: rw [mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Defs (goal)
Goal:
α : Type u
inst : NonAssocSemiring α
a : α
⊢ HSMul.hSMul (α := ℕ) 0 a = (↑0 : α) * a
have zero : 0 = (↑0 : α) * a
Tactic: rw [zero_nsmul, Nat.cast_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Defs (goal)
Goal:
α : Type u
inst : NonAssocSemiring α
a : α
zero : 0 = (↑0 : α) * a
⊢ HSMul.hSMul (α := ℕ) 0 a = (↑0 : α) * a
have zero₁ : 0 = 0 * a
Tactic: rw [zero_nsmul, Nat.cast_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Defs (goal)
Goal:
α : Type u
inst : NonAssocSemiring α
a : α
zero : 0 = (↑0 : α) * a
zero₁ : 0 = 0 * a
⊢ HSMul.hSMul (α := ℕ) 0 a = (↑0 : α) * a
have zero₂ : Eq.{u + 1} (α := α) 0 0
Tactic: rw [zero_nsmul, Nat.cast_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Defs (goal)
Goal:
α : Type u
inst : NonAssocSemiring α
a : α
n : ℕ
ih : n • a = (↑n : α) * a
⊢ (n + 1) • a = (↑(n + 1) : α) * a
have succ : n • a + a = (↑(n + 1) : α) * a
Tactic: rw [succ_nsmul, ih, Nat.cast_succ, add_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Defs (goal)
Goal:
α : Type u
inst : NonAssocSemiring α
a : α
n : ℕ
ih : n • a = (↑n : α) * a
succ : n • a + a = (↑(n + 1) : α) * a
⊢ (n + 1) • a = (↑(n + 1) : α) * a
have succ₁ : (↑n : α) * a + a = (↑(n + 1) : α) * a
Tactic: rw [succ_nsmul, ih, Nat.cast_succ, add_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Defs (goal)
Goal:
α : Type u
inst : NonAssocSemiring α
a : α
n : ℕ
ih : n • a = (↑n : α) * a
succ : n • a + a = (↑(n + 1) : α) * a
succ₁ : (↑n : α) * a + a = (↑(n + 1) : α) * a
⊢ (n + 1) • a = (↑(n + 1) : α) * a
have succ₂ : (↑n : α) * a + a = HAdd.hAdd (α := α) (↑n : α) 1 * a
Tactic: rw [succ_nsmul, ih, Nat.cast_succ, add_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Defs (goal)
Goal:
α : Type u
inst : NonAssocSemiring α
a : α
n : ℕ
ih : n • a = (↑n : α) * a
succ : n • a + a = (↑(n + 1) : α) * a
succ₁ : (↑n : α) * a + a = (↑(n + 1) : α) * a
succ₂ : (↑n : α) * a + a = HAdd.hAdd (α := α) (↑n : α) 1 * a
⊢ (n + 1) • a = (↑(n + 1) : α) * a
have succ₃ : (↑n : α) * a + a = (↑n : α) * a + 1 * a
Tactic: rw [succ_nsmul, ih, Nat.cast_succ, add_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Defs (goal)
Goal:
α : Type u
inst : NonAssocSemiring α
a : α
n : ℕ
ih : n • a = (↑n : α) * a
succ : n • a + a = (↑(n + 1) : α) * a
succ₁ : (↑n : α) * a + a = (↑(n + 1) : α) * a
succ₂ : (↑n : α) * a + a = HAdd.hAdd (α := α) (↑n : α) 1 * a
succ₃ : (↑n : α) * a + a = (↑n : α) * a + 1 * a
⊢ (n + 1) • a = (↑(n + 1) : α) * a
have succ₄ : (↑n : α) * a + a = (↑n : α) * a + a
Tactic: rw [succ_nsmul, ih, Nat.cast_succ, add_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Defs (goal)
Goal:
α : Type u
inst : NonAssocSemiring α
n : ℕ
a : α
⊢ n • a = (↑n : α) * a
have zero : HSMul.hSMul (α := ℕ) 0 a = (↑0 : α) * a
Tactic: induction n with
  | zero => rw [zero_nsmul, Nat.cast_zero, zero_mul]
  | succ n ih => rw [succ_nsmul, ih, Nat.cast_succ, add_mul, one_mul]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Ring.Defs (goal)
Goal:
α : Type u
inst : NonAssocSemiring α
n : ℕ
a : α
zero : HSMul.hSMul (α := ℕ) 0 a = (↑0 : α) * a
⊢ n • a = (↑n : α) * a
have succ : ∀ (n : ℕ) (ih : n • a = (↑n : α) * a), (n + 1) • a = (↑(n + 1) : α) * a
Tactic: induction n with
  | zero => rw [zero_nsmul, Nat.cast_zero, zero_mul]
  | succ n ih => rw [succ_nsmul, ih, Nat.cast_succ, add_mul, one_mul]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Ring.Defs (goal)
Goal:
α : Type u
inst : CommSemiring α
a b : α
⊢ HPow.hPow (β := ℕ) (a + b) 2 = HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 2 * a * b
have rw : HPow.hPow (β := ℕ) a 2 + 2 * a * b + HPow.hPow (β := ℕ) b 2 =
  HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 2 * a * b
Tactic: rw [add_sq, add_assoc, add_comm _ (b ^ 2), add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Defs (goal)
Goal:
α : Type u
inst : CommSemiring α
a b : α
rw :
  HPow.hPow (β := ℕ) a 2 + 2 * a * b + HPow.hPow (β := ℕ) b 2 =
    HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 2 * a * b
⊢ HPow.hPow (β := ℕ) (a + b) 2 = HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 2 * a * b
have rw₁ : HPow.hPow (β := ℕ) a 2 + (2 * a * b + HPow.hPow (β := ℕ) b 2) =
  HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 2 * a * b
Tactic: rw [add_sq, add_assoc, add_comm _ (b ^ 2), add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Defs (goal)
Goal:
α : Type u
inst : CommSemiring α
a b : α
rw :
  HPow.hPow (β := ℕ) a 2 + 2 * a * b + HPow.hPow (β := ℕ) b 2 =
    HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 2 * a * b
rw₁ :
  HPow.hPow (β := ℕ) a 2 + (2 * a * b + HPow.hPow (β := ℕ) b 2) =
    HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 2 * a * b
⊢ HPow.hPow (β := ℕ) (a + b) 2 = HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 2 * a * b
have rw₂ : HPow.hPow (β := ℕ) a 2 + (HPow.hPow (β := ℕ) b 2 + 2 * a * b) =
  HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 2 * a * b
Tactic: rw [add_sq, add_assoc, add_comm _ (b ^ 2), add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Defs (goal)
Goal:
α : Type u
inst : CommSemiring α
a b : α
rw :
  HPow.hPow (β := ℕ) a 2 + 2 * a * b + HPow.hPow (β := ℕ) b 2 =
    HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 2 * a * b
rw₁ :
  HPow.hPow (β := ℕ) a 2 + (2 * a * b + HPow.hPow (β := ℕ) b 2) =
    HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 2 * a * b
rw₂ :
  HPow.hPow (β := ℕ) a 2 + (HPow.hPow (β := ℕ) b 2 + 2 * a * b) =
    HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 2 * a * b
⊢ HPow.hPow (β := ℕ) (a + b) 2 = HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 2 * a * b
have rw₃ : HPow.hPow (β := ℕ) a 2 + (HPow.hPow (β := ℕ) b 2 + 2 * a * b) =
  HPow.hPow (β := ℕ) a 2 + (HPow.hPow (β := ℕ) b 2 + 2 * a * b)
Tactic: rw [add_sq, add_assoc, add_comm _ (b ^ 2), add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Defs (goal)
Goal:
α : Type u
R : Type v
inst : MulZeroClass α
inst_1 : HasDistribNeg α
⊢ Eq.{u + 1} (α := α) (-0) 0
have rw : -HMul.hMul (α := α) 0 0 = HMul.hMul (α := α) 0 0
Tactic: rw [← zero_mul (0 : α), ← neg_mul, mul_zero, mul_zero]