awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Ring.Units (goal)
Goal:
α : Type u
inst : CommSemiring α
a b : α
u₁ u₂ : αˣ
rw :
  a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b =
    a * (↑u₂ : α) * (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) * ((↑u₁ : α) * b)
rw₁ :
  a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b =
    a * (↑u₂ : α) * (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) * (↑u₁ : α) * b
rw₂ :
  a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b =
    a * ((↑u₂ : α) * (↑u₂⁻¹ : α)) * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) * (↑u₁ : α) * b
rw₃ :
  a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b =
    a * ((↑u₂ : α) * (↑u₂⁻¹ : α)) * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * ((↑u₁⁻¹ : α) * (↑u₁ : α)) * b
rw₄ : a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b = a * 1 * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * ((↑u₁⁻¹ : α) * (↑u₁ : α)) * b
⊢ a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b =
    a * (↑u₂ : α) * ((↑u₂⁻¹ : α) * (↑u₁⁻¹ : α)) + (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) * ((↑u₁ : α) * b)
have rw₅ : a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b = a * 1 * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * 1 * b
Tactic: rw [← mul_assoc, ← mul_assoc, mul_assoc a, mul_assoc (↑u₂⁻¹ : α), mul_inv, inv_mul, mul_one,
    mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Units (goal)
Goal:
α : Type u
inst : CommSemiring α
a b : α
u₁ u₂ : αˣ
rw :
  a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b =
    a * (↑u₂ : α) * (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) * ((↑u₁ : α) * b)
rw₁ :
  a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b =
    a * (↑u₂ : α) * (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) * (↑u₁ : α) * b
rw₂ :
  a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b =
    a * ((↑u₂ : α) * (↑u₂⁻¹ : α)) * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) * (↑u₁ : α) * b
rw₃ :
  a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b =
    a * ((↑u₂ : α) * (↑u₂⁻¹ : α)) * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * ((↑u₁⁻¹ : α) * (↑u₁ : α)) * b
rw₄ : a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b = a * 1 * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * ((↑u₁⁻¹ : α) * (↑u₁ : α)) * b
rw₅ : a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b = a * 1 * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * 1 * b
⊢ a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b =
    a * (↑u₂ : α) * ((↑u₂⁻¹ : α) * (↑u₁⁻¹ : α)) + (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) * ((↑u₁ : α) * b)
have rw₆ : a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b = a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * 1 * b
Tactic: rw [← mul_assoc, ← mul_assoc, mul_assoc a, mul_assoc (↑u₂⁻¹ : α), mul_inv, inv_mul, mul_one,
    mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Units (goal)
Goal:
α : Type u
inst : CommSemiring α
a b : α
u₁ u₂ : αˣ
rw :
  a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b =
    a * (↑u₂ : α) * (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) * ((↑u₁ : α) * b)
rw₁ :
  a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b =
    a * (↑u₂ : α) * (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) * (↑u₁ : α) * b
rw₂ :
  a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b =
    a * ((↑u₂ : α) * (↑u₂⁻¹ : α)) * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) * (↑u₁ : α) * b
rw₃ :
  a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b =
    a * ((↑u₂ : α) * (↑u₂⁻¹ : α)) * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * ((↑u₁⁻¹ : α) * (↑u₁ : α)) * b
rw₄ : a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b = a * 1 * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * ((↑u₁⁻¹ : α) * (↑u₁ : α)) * b
rw₅ : a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b = a * 1 * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * 1 * b
rw₆ : a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b = a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * 1 * b
⊢ a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b =
    a * (↑u₂ : α) * ((↑u₂⁻¹ : α) * (↑u₁⁻¹ : α)) + (↑u₂⁻¹ : α) * (↑u₁⁻¹ : α) * ((↑u₁ : α) * b)
have rw₇ : a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b = a * (↑u₁⁻¹ : α) + (↑u₂⁻¹ : α) * b
Tactic: rw [← mul_assoc, ← mul_assoc, mul_assoc a, mul_assoc (↑u₂⁻¹ : α), mul_inv, inv_mul, mul_one,
    mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Units (goal)
Goal:
R : Type x
inst : Semiring R
a : Rˣ
b : R
⊢ (↑a : R) + b = (↑a : R) * (1 + (↑a⁻¹ : R) * b)
have rw : (↑a : R) + b = (↑a : R) * 1 + (↑a : R) * ((↑a⁻¹ : R) * b)
Tactic: rw [mul_add, mul_one, ← mul_assoc, Units.mul_inv, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Units (goal)
Goal:
R : Type x
inst : Semiring R
a : Rˣ
b : R
rw : (↑a : R) + b = (↑a : R) * 1 + (↑a : R) * ((↑a⁻¹ : R) * b)
⊢ (↑a : R) + b = (↑a : R) * (1 + (↑a⁻¹ : R) * b)
have rw₁ : (↑a : R) + b = (↑a : R) + (↑a : R) * ((↑a⁻¹ : R) * b)
Tactic: rw [mul_add, mul_one, ← mul_assoc, Units.mul_inv, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Units (goal)
Goal:
R : Type x
inst : Semiring R
a : Rˣ
b : R
rw : (↑a : R) + b = (↑a : R) * 1 + (↑a : R) * ((↑a⁻¹ : R) * b)
rw₁ : (↑a : R) + b = (↑a : R) + (↑a : R) * ((↑a⁻¹ : R) * b)
⊢ (↑a : R) + b = (↑a : R) * (1 + (↑a⁻¹ : R) * b)
have rw₂ : (↑a : R) + b = (↑a : R) + (↑a : R) * (↑a⁻¹ : R) * b
Tactic: rw [mul_add, mul_one, ← mul_assoc, Units.mul_inv, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Units (goal)
Goal:
R : Type x
inst : Semiring R
a : Rˣ
b : R
rw : (↑a : R) + b = (↑a : R) * 1 + (↑a : R) * ((↑a⁻¹ : R) * b)
rw₁ : (↑a : R) + b = (↑a : R) + (↑a : R) * ((↑a⁻¹ : R) * b)
rw₂ : (↑a : R) + b = (↑a : R) + (↑a : R) * (↑a⁻¹ : R) * b
⊢ (↑a : R) + b = (↑a : R) * (1 + (↑a⁻¹ : R) * b)
have rw₃ : (↑a : R) + b = (↑a : R) + 1 * b
Tactic: rw [mul_add, mul_one, ← mul_assoc, Units.mul_inv, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Units (goal)
Goal:
R : Type x
inst : Semiring R
a : Rˣ
b : R
rw : (↑a : R) + b = (↑a : R) * 1 + (↑a : R) * ((↑a⁻¹ : R) * b)
rw₁ : (↑a : R) + b = (↑a : R) + (↑a : R) * ((↑a⁻¹ : R) * b)
rw₂ : (↑a : R) + b = (↑a : R) + (↑a : R) * (↑a⁻¹ : R) * b
rw₃ : (↑a : R) + b = (↑a : R) + 1 * b
⊢ (↑a : R) + b = (↑a : R) * (1 + (↑a⁻¹ : R) * b)
have rw₄ : (↑a : R) + b = (↑a : R) + b
Tactic: rw [mul_add, mul_one, ← mul_assoc, Units.mul_inv, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.WithZero (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : Add α
inst_2 : LeftDistribClass α
a b c : WithZero α
⊢ a * (b + c) = a * b + a * c
have zero : 0 * (b + c) = 0 * b + 0 * c
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Ring.WithZero (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : Add α
inst_2 : LeftDistribClass α
a b c : WithZero α
zero : 0 * (b + c) = 0 * b + 0 * c
⊢ a * (b + c) = a * b + a * c
have coe : ∀ (a : α), (↑a : WithZero α) * (b + c) = (↑a : WithZero α) * b + (↑a : WithZero α) * c
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Ring.WithZero (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : Add α
inst_2 : LeftDistribClass α
b c : WithZero α
a : α
⊢ (↑a : WithZero α) * (b + c) = (↑a : WithZero α) * b + (↑a : WithZero α) * c
have coe : (↑a : WithZero α) * (0 + c) = (↑a : WithZero α) * 0 + (↑a : WithZero α) * c
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Ring.WithZero (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : Add α
inst_2 : LeftDistribClass α
b c : WithZero α
a : α
coe : (↑a : WithZero α) * (0 + c) = (↑a : WithZero α) * 0 + (↑a : WithZero α) * c
⊢ (↑a : WithZero α) * (b + c) = (↑a : WithZero α) * b + (↑a : WithZero α) * c
have coe₁ : ∀ (a_1 : α),
  (↑a : WithZero α) * ((↑a_1 : WithZero α) + c) = (↑a : WithZero α) * (↑a_1 : WithZero α) + (↑a : WithZero α) * c
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Ring.WithZero (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : Add α
inst_2 : LeftDistribClass α
c : WithZero α
a : α
⊢ (↑a : WithZero α) * (0 + c) = (↑a : WithZero α) * 0 + (↑a : WithZero α) * c
have coe : (↑a : WithZero α) * HAdd.hAdd (α := WithZero α) 0 0 = (↑a : WithZero α) * 0 + (↑a : WithZero α) * 0
Tactic: cases c
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Algebra.Ring.WithZero (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : Add α
inst_2 : LeftDistribClass α
c : WithZero α
a : α
coe : (↑a : WithZero α) * HAdd.hAdd (α := WithZero α) 0 0 = (↑a : WithZero α) * 0 + (↑a : WithZero α) * 0
⊢ (↑a : WithZero α) * (0 + c) = (↑a : WithZero α) * 0 + (↑a : WithZero α) * c
have coe₁ : ∀ (a_1 : α),
  (↑a : WithZero α) * (0 + (↑a_1 : WithZero α)) = (↑a : WithZero α) * 0 + (↑a : WithZero α) * (↑a_1 : WithZero α)
Tactic: cases c
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Algebra.Ring.WithZero (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : Add α
inst_2 : LeftDistribClass α
c : WithZero α
a a_1 : α
⊢ (↑a : WithZero α) * ((↑a_1 : WithZero α) + c) = (↑a : WithZero α) * (↑a_1 : WithZero α) + (↑a : WithZero α) * c
have coe : (↑a : WithZero α) * ((↑a_1 : WithZero α) + 0) = (↑a : WithZero α) * (↑a_1 : WithZero α) + (↑a : WithZero α) * 0
Tactic: cases c
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Algebra.Ring.WithZero (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : Add α
inst_2 : LeftDistribClass α
c : WithZero α
a a_1 : α
coe : (↑a : WithZero α) * ((↑a_1 : WithZero α) + 0) = (↑a : WithZero α) * (↑a_1 : WithZero α) + (↑a : WithZero α) * 0
⊢ (↑a : WithZero α) * ((↑a_1 : WithZero α) + c) = (↑a : WithZero α) * (↑a_1 : WithZero α) + (↑a : WithZero α) * c
have coe₁ : ∀ (a_2 : α),
  (↑a : WithZero α) * ((↑a_1 : WithZero α) + (↑a_2 : WithZero α)) =
    (↑a : WithZero α) * (↑a_1 : WithZero α) + (↑a : WithZero α) * (↑a_2 : WithZero α)
Tactic: cases c
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Algebra.Ring.WithZero (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : Add α
inst_2 : RightDistribClass α
a b c : WithZero α
⊢ (a + b) * c = a * c + b * c
have zero : (a + b) * 0 = a * 0 + b * 0
Tactic: cases c
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Algebra.Ring.WithZero (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : Add α
inst_2 : RightDistribClass α
a b c : WithZero α
zero : (a + b) * 0 = a * 0 + b * 0
⊢ (a + b) * c = a * c + b * c
have coe : ∀ (a_1 : α), (a + b) * (↑a_1 : WithZero α) = a * (↑a_1 : WithZero α) + b * (↑a_1 : WithZero α)
Tactic: cases c
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Algebra.Ring.WithZero (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : Add α
inst_2 : RightDistribClass α
a b : WithZero α
a_1 : α
⊢ (a + b) * (↑a_1 : WithZero α) = a * (↑a_1 : WithZero α) + b * (↑a_1 : WithZero α)
have coe : (0 + b) * (↑a_1 : WithZero α) = 0 * (↑a_1 : WithZero α) + b * (↑a_1 : WithZero α)
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Ring.WithZero (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : Add α
inst_2 : RightDistribClass α
a b : WithZero α
a_1 : α
coe : (0 + b) * (↑a_1 : WithZero α) = 0 * (↑a_1 : WithZero α) + b * (↑a_1 : WithZero α)
⊢ (a + b) * (↑a_1 : WithZero α) = a * (↑a_1 : WithZero α) + b * (↑a_1 : WithZero α)
have coe₁ : ∀ (a : α),
  ((↑a : WithZero α) + b) * (↑a_1 : WithZero α) = (↑a : WithZero α) * (↑a_1 : WithZero α) + b * (↑a_1 : WithZero α)
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Ring.WithZero (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : Add α
inst_2 : RightDistribClass α
b : WithZero α
a : α
⊢ (0 + b) * (↑a : WithZero α) = 0 * (↑a : WithZero α) + b * (↑a : WithZero α)
have coe : HAdd.hAdd (α := WithZero α) 0 0 * (↑a : WithZero α) = 0 * (↑a : WithZero α) + 0 * (↑a : WithZero α)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Ring.WithZero (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : Add α
inst_2 : RightDistribClass α
b : WithZero α
a : α
coe : HAdd.hAdd (α := WithZero α) 0 0 * (↑a : WithZero α) = 0 * (↑a : WithZero α) + 0 * (↑a : WithZero α)
⊢ (0 + b) * (↑a : WithZero α) = 0 * (↑a : WithZero α) + b * (↑a : WithZero α)
have coe₁ : ∀ (a_1 : α),
  (0 + (↑a_1 : WithZero α)) * (↑a : WithZero α) = 0 * (↑a : WithZero α) + (↑a_1 : WithZero α) * (↑a : WithZero α)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Ring.WithZero (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : Add α
inst_2 : RightDistribClass α
b : WithZero α
a a_1 : α
⊢ ((↑a_1 : WithZero α) + b) * (↑a : WithZero α) = (↑a_1 : WithZero α) * (↑a : WithZero α) + b * (↑a : WithZero α)
have coe : ((↑a_1 : WithZero α) + 0) * (↑a : WithZero α) = (↑a_1 : WithZero α) * (↑a : WithZero α) + 0 * (↑a : WithZero α)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Ring.WithZero (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : Add α
inst_2 : RightDistribClass α
b : WithZero α
a a_1 : α
coe : ((↑a_1 : WithZero α) + 0) * (↑a : WithZero α) = (↑a_1 : WithZero α) * (↑a : WithZero α) + 0 * (↑a : WithZero α)
⊢ ((↑a_1 : WithZero α) + b) * (↑a : WithZero α) = (↑a_1 : WithZero α) * (↑a : WithZero α) + b * (↑a : WithZero α)
have coe₁ : ∀ (a_2 : α),
  ((↑a_1 : WithZero α) + (↑a_2 : WithZero α)) * (↑a : WithZero α) =
    (↑a_1 : WithZero α) * (↑a : WithZero α) + (↑a_2 : WithZero α) * (↑a : WithZero α)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
Goal:
R : Type uR
inst : Semiring R
r : R → R → Prop
a b c : R
h : Rel r b c
⊢ Rel r (a + b) (a + c)
have rw : Rel r (b + a) (c + a)
Tactic: rw [add_comm a b, add_comm a c]
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
a b x y : R
hab : Rel r x y
c d : R
hcd : Relation.EqvGen (Rel r) c d
⊢ Relation.EqvGen (Rel r) (x * c) (y * d)
have rel : Relation.EqvGen (Rel r) (y * c) (y * d)
Tactic: refine (Relation.EqvGen.rel _ _ hab.mul_left).trans _ _ _ ?_
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
a b x y : R
hab : Rel r x y
c d : R
hcd : Relation.EqvGen (Rel r) c d
⊢ Relation.EqvGen (Rel r) (y * c) (y * d)
have rel : ∀ (x y_1 : R) (hcd : Rel r x y_1), Relation.EqvGen (Rel r) (y * x) (y * y_1)
Tactic: induction hcd with
      | rel _ _ hcd => exact Relation.EqvGen.rel _ _ hcd.mul_right
      | refl => exact Relation.EqvGen.refl _
      | symm _ _ _ h => exact h.symm _ _
      | trans _ _ _ _ _ h h' => exact h.trans _ _ _ h'
Cleared hypotheses: hcd
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
a b x y : R
hab : Rel r x y
c d : R
hcd : Relation.EqvGen (Rel r) c d
rel : ∀ (x y_1 : R) (hcd : Rel r x y_1), Relation.EqvGen (Rel r) (y * x) (y * y_1)
⊢ Relation.EqvGen (Rel r) (y * c) (y * d)
have rel₁ : ∀ (x : R), Relation.EqvGen (Rel r) (y * x) (y * x)
Tactic: induction hcd with
      | rel _ _ hcd => exact Relation.EqvGen.rel _ _ hcd.mul_right
      | refl => exact Relation.EqvGen.refl _
      | symm _ _ _ h => exact h.symm _ _
      | trans _ _ _ _ _ h h' => exact h.trans _ _ _ h'
Cleared hypotheses: hcd
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
a b x y : R
hab : Rel r x y
c d : R
hcd : Relation.EqvGen (Rel r) c d
rel : ∀ (x y_1 : R) (hcd : Rel r x y_1), Relation.EqvGen (Rel r) (y * x) (y * y_1)
rel₁ : ∀ (x : R), Relation.EqvGen (Rel r) (y * x) (y * x)
⊢ Relation.EqvGen (Rel r) (y * c) (y * d)
have rel₂ : ∀ (x y_1 : R),
  Relation.EqvGen (Rel r) x y_1 →
    ∀ (h : Relation.EqvGen (Rel r) (y * x) (y * y_1)), Relation.EqvGen (Rel r) (y * y_1) (y * x)
Tactic: induction hcd with
      | rel _ _ hcd => exact Relation.EqvGen.rel _ _ hcd.mul_right
      | refl => exact Relation.EqvGen.refl _
      | symm _ _ _ h => exact h.symm _ _
      | trans _ _ _ _ _ h h' => exact h.trans _ _ _ h'
Cleared hypotheses: hcd
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
a b x y : R
hab : Rel r x y
c d : R
hcd : Relation.EqvGen (Rel r) c d
rel : ∀ (x y_1 : R) (hcd : Rel r x y_1), Relation.EqvGen (Rel r) (y * x) (y * y_1)
rel₁ : ∀ (x : R), Relation.EqvGen (Rel r) (y * x) (y * x)
rel₂ :
  ∀ (x y_1 : R),
    Relation.EqvGen (Rel r) x y_1 →
      ∀ (h : Relation.EqvGen (Rel r) (y * x) (y * y_1)), Relation.EqvGen (Rel r) (y * y_1) (y * x)
⊢ Relation.EqvGen (Rel r) (y * c) (y * d)
have rel₃ : ∀ (x y_1 z : R),
  Relation.EqvGen (Rel r) x y_1 →
    Relation.EqvGen (Rel r) y_1 z →
      ∀ (h : Relation.EqvGen (Rel r) (y * x) (y * y_1)) (h' : Relation.EqvGen (Rel r) (y * y_1) (y * z)),
        Relation.EqvGen (Rel r) (y * x) (y * z)
Tactic: induction hcd with
      | rel _ _ hcd => exact Relation.EqvGen.rel _ _ hcd.mul_right
      | refl => exact Relation.EqvGen.refl _
      | symm _ _ _ h => exact h.symm _ _
      | trans _ _ _ _ _ h h' => exact h.trans _ _ _ h'
Cleared hypotheses: hcd
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
a b x c d : R
hcd : Relation.EqvGen (Rel r) c d
⊢ Relation.EqvGen (Rel r) (x * c) (x * d)
have refl : ∀ (x_1 y : R) (hcd : Rel r x_1 y), Relation.EqvGen (Rel r) (x * x_1) (x * y)
Tactic: induction hcd with
      | rel _ _ hcd => exact Relation.EqvGen.rel _ _ hcd.mul_right
      | refl => exact Relation.EqvGen.refl _
      | symm _ _ _ h => exact h.symm _ _
      | trans _ _ _ _ _ h h' => exact h.trans _ _ _ h'
Cleared hypotheses: hcd
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
a b x c d : R
hcd : Relation.EqvGen (Rel r) c d
refl : ∀ (x_1 y : R) (hcd : Rel r x_1 y), Relation.EqvGen (Rel r) (x * x_1) (x * y)
⊢ Relation.EqvGen (Rel r) (x * c) (x * d)
have refl₁ : ∀ (x_1 : R), Relation.EqvGen (Rel r) (x * x_1) (x * x_1)
Tactic: induction hcd with
      | rel _ _ hcd => exact Relation.EqvGen.rel _ _ hcd.mul_right
      | refl => exact Relation.EqvGen.refl _
      | symm _ _ _ h => exact h.symm _ _
      | trans _ _ _ _ _ h h' => exact h.trans _ _ _ h'
Cleared hypotheses: hcd
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
a b x c d : R
hcd : Relation.EqvGen (Rel r) c d
refl : ∀ (x_1 y : R) (hcd : Rel r x_1 y), Relation.EqvGen (Rel r) (x * x_1) (x * y)
refl₁ : ∀ (x_1 : R), Relation.EqvGen (Rel r) (x * x_1) (x * x_1)
⊢ Relation.EqvGen (Rel r) (x * c) (x * d)
have refl₂ : ∀ (x_1 y : R),
  Relation.EqvGen (Rel r) x_1 y →
    ∀ (h : Relation.EqvGen (Rel r) (x * x_1) (x * y)), Relation.EqvGen (Rel r) (x * y) (x * x_1)
Tactic: induction hcd with
      | rel _ _ hcd => exact Relation.EqvGen.rel _ _ hcd.mul_right
      | refl => exact Relation.EqvGen.refl _
      | symm _ _ _ h => exact h.symm _ _
      | trans _ _ _ _ _ h h' => exact h.trans _ _ _ h'
Cleared hypotheses: hcd
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
a b x c d : R
hcd : Relation.EqvGen (Rel r) c d
refl : ∀ (x_1 y : R) (hcd : Rel r x_1 y), Relation.EqvGen (Rel r) (x * x_1) (x * y)
refl₁ : ∀ (x_1 : R), Relation.EqvGen (Rel r) (x * x_1) (x * x_1)
refl₂ :
  ∀ (x_1 y : R),
    Relation.EqvGen (Rel r) x_1 y →
      ∀ (h : Relation.EqvGen (Rel r) (x * x_1) (x * y)), Relation.EqvGen (Rel r) (x * y) (x * x_1)
⊢ Relation.EqvGen (Rel r) (x * c) (x * d)
have refl₃ : ∀ (x_1 y z : R),
  Relation.EqvGen (Rel r) x_1 y →
    Relation.EqvGen (Rel r) y z →
      ∀ (h : Relation.EqvGen (Rel r) (x * x_1) (x * y)) (h' : Relation.EqvGen (Rel r) (x * y) (x * z)),
        Relation.EqvGen (Rel r) (x * x_1) (x * z)
Tactic: induction hcd with
      | rel _ _ hcd => exact Relation.EqvGen.rel _ _ hcd.mul_right
      | refl => exact Relation.EqvGen.refl _
      | symm _ _ _ h => exact h.symm _ _
      | trans _ _ _ _ _ h h' => exact h.trans _ _ _ h'
Cleared hypotheses: hcd
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
a b c d : R
hab : Relation.EqvGen (Rel r) a b
hcd : Relation.EqvGen (Rel r) c d
⊢ Relation.EqvGen (Rel r) (a * c) (b * d)
have rel : ∀ (x y : R) (hab : Rel r x y) {c d : R} (hcd : Relation.EqvGen (Rel r) c d), Relation.EqvGen (Rel r) (x * c) (y * d)
Tactic: induction hab generalizing c d with
    | rel _ _ hab =>
      refine (Relation.EqvGen.rel _ _ hab.mul_left).trans _ _ _ ?_
      induction hcd with
      | rel _ _ hcd => exact Relation.EqvGen.rel _ _ hcd.mul_right
      | refl => exact Relation.EqvGen.refl _
      | symm _ _ _ h => exact h.symm _ _
      | trans _ _ _ _ _ h h' => exact h.trans _ _ _ h'
    | refl => induction hcd with
      | rel _ _ hcd => exact Relation.EqvGen.rel _ _ hcd.mul_right
      | refl => exact Relation.EqvGen.refl _
      | symm _ _ _ h => exact h.symm _ _
      | trans _ _ _ _ _ h h' => exact h.trans _ _ _ h'
    | symm x y _ hxy => exact (hxy hcd.symm).symm
    | trans x y z _ _ h h' => exact (h hcd).trans _ _ _ (h' <| Relation.EqvGen.refl _)
Cleared hypotheses: c, d, hab, hcd
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
a b c d : R
hab : Relation.EqvGen (Rel r) a b
hcd : Relation.EqvGen (Rel r) c d
rel :
  ∀ (x y : R) (hab : Rel r x y) {c d : R} (hcd : Relation.EqvGen (Rel r) c d), Relation.EqvGen (Rel r) (x * c) (y * d)
⊢ Relation.EqvGen (Rel r) (a * c) (b * d)
have refl : ∀ (x : R) {c d : R} (hcd : Relation.EqvGen (Rel r) c d), Relation.EqvGen (Rel r) (x * c) (x * d)
Tactic: induction hab generalizing c d with
    | rel _ _ hab =>
      refine (Relation.EqvGen.rel _ _ hab.mul_left).trans _ _ _ ?_
      induction hcd with
      | rel _ _ hcd => exact Relation.EqvGen.rel _ _ hcd.mul_right
      | refl => exact Relation.EqvGen.refl _
      | symm _ _ _ h => exact h.symm _ _
      | trans _ _ _ _ _ h h' => exact h.trans _ _ _ h'
    | refl => induction hcd with
      | rel _ _ hcd => exact Relation.EqvGen.rel _ _ hcd.mul_right
      | refl => exact Relation.EqvGen.refl _
      | symm _ _ _ h => exact h.symm _ _
      | trans _ _ _ _ _ h h' => exact h.trans _ _ _ h'
    | symm x y _ hxy => exact (hxy hcd.symm).symm
    | trans x y z _ _ h h' => exact (h hcd).trans _ _ _ (h' <| Relation.EqvGen.refl _)
Cleared hypotheses: c, d, hab, hcd
-- Lean 4 proof step from Mathlib.Algebra.RingQuot (goal)
Goal:
R : Type uR
inst : Semiring R
S : Type uS
inst_1 : CommSemiring S
T : Type uT
A : Type uA
inst_2 : Semiring A
inst_3 : Algebra S A
r : R → R → Prop
a b c d : R
hab : Relation.EqvGen (Rel r) a b
hcd : Relation.EqvGen (Rel r) c d
rel :
  ∀ (x y : R) (hab : Rel r x y) {c d : R} (hcd : Relation.EqvGen (Rel r) c d), Relation.EqvGen (Rel r) (x * c) (y * d)
refl : ∀ (x : R) {c d : R} (hcd : Relation.EqvGen (Rel r) c d), Relation.EqvGen (Rel r) (x * c) (x * d)
⊢ Relation.EqvGen (Rel r) (a * c) (b * d)
have symm : ∀ (x y : R),
  Relation.EqvGen (Rel r) x y →
    ∀ (hxy : ∀ {c d : R} (hcd : Relation.EqvGen (Rel r) c d), Relation.EqvGen (Rel r) (x * c) (y * d)) {c d : R}
      (hcd : Relation.EqvGen (Rel r) c d), Relation.EqvGen (Rel r) (y * c) (x * d)
Tactic: induction hab generalizing c d with
    | rel _ _ hab =>
      refine (Relation.EqvGen.rel _ _ hab.mul_left).trans _ _ _ ?_
      induction hcd with
      | rel _ _ hcd => exact Relation.EqvGen.rel _ _ hcd.mul_right
      | refl => exact Relation.EqvGen.refl _
      | symm _ _ _ h => exact h.symm _ _
      | trans _ _ _ _ _ h h' => exact h.trans _ _ _ h'
    | refl => induction hcd with
      | rel _ _ hcd => exact Relation.EqvGen.rel _ _ hcd.mul_right
      | refl => exact Relation.EqvGen.refl _
      | symm _ _ _ h => exact h.symm _ _
      | trans _ _ _ _ _ h h' => exact h.trans _ _ _ h'
    | symm x y _ hxy => exact (hxy hcd.symm).symm
    | trans x y z _ _ h h' => exact (h hcd).trans _ _ _ (h' <| Relation.EqvGen.refl _)
Cleared hypotheses: c, d, hab, hcd