awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ a + ∑ i ∈ Ico 1 n.succ, a / b ^ i = a / HPow.hPow (β := ℕ) b 0 + ∑ i ∈ Ico 1 n.succ, a / b ^ i
have rw : a + ∑ i ∈ Ico 1 n.succ, a / b ^ i = a / 1 + ∑ i ∈ Ico 1 n.succ, a / b ^ i
Tactic: rw [pow_zero, Nat.div_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
b : ℕ
hb : 2 ≤ b
a n : ℕ
rw : a + ∑ i ∈ Ico 1 n.succ, a / b ^ i = a / 1 + ∑ i ∈ Ico 1 n.succ, a / b ^ i
⊢ a + ∑ i ∈ Ico 1 n.succ, a / b ^ i = a / HPow.hPow (β := ℕ) b 0 + ∑ i ∈ Ico 1 n.succ, a / b ^ i
have rw₁ : a + ∑ i ∈ Ico 1 n.succ, a / b ^ i = a + ∑ i ∈ Ico 1 n.succ, a / b ^ i
Tactic: rw [pow_zero, Nat.div_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ a / HPow.hPow (β := ℕ) b 0 + ∑ i ∈ Ico 1 n.succ, a / b ^ i = ∑ i ∈ range n.succ, a / b ^ i
have rw : a / HPow.hPow (β := ℕ) b 0 + ∑ i ∈ Ico 1 n.succ, a / b ^ i =
  a / HPow.hPow (β := ℕ) b 0 + ∑ x ∈ Ico (HAdd.hAdd (α := ℕ) 0 1) n.succ, a / b ^ x
Tactic: rw [range_eq_Ico, ← Finset.insert_Ico_add_one_left_eq_Ico (Nat.succ_pos _), sum_insert]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
b : ℕ
hb : 2 ≤ b
a n : ℕ
rw :
  a / HPow.hPow (β := ℕ) b 0 + ∑ i ∈ Ico 1 n.succ, a / b ^ i =
    a / HPow.hPow (β := ℕ) b 0 + ∑ x ∈ Ico (HAdd.hAdd (α := ℕ) 0 1) n.succ, a / b ^ x
⊢ a / HPow.hPow (β := ℕ) b 0 + ∑ i ∈ Ico 1 n.succ, a / b ^ i = ∑ i ∈ range n.succ, a / b ^ i
have rw₁ : 0 ∉ Ico (HAdd.hAdd (α := ℕ) 0 1) n.succ
Tactic: rw [range_eq_Ico, ← Finset.insert_Ico_add_one_left_eq_Ico (Nat.succ_pos _), sum_insert]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ a * b / (b - 1) = (a * 1 + a * (b - 1)) / (b - 1)
have rw : a * b / (b - 1) = a * (1 + (b - 1)) / (b - 1)
Tactic: rw [← mul_add, add_tsub_cancel_of_le (by lia)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
b : ℕ
hb : 2 ≤ b
a n : ℕ
rw : a * b / (b - 1) = a * (1 + (b - 1)) / (b - 1)
⊢ a * b / (b - 1) = (a * 1 + a * (b - 1)) / (b - 1)
have rw₁ : a * b / (b - 1) = a * b / (b - 1)
Tactic: rw [← mul_add, add_tsub_cancel_of_le (by lia)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ (a * 1 + a * (b - 1)) / (b - 1) = a + a / (b - 1)
have rw : (a + a * (b - 1)) / (b - 1) = a + a / (b - 1)
Tactic: rw [mul_one, Nat.add_mul_div_right _ _ (tsub_pos_of_lt hb), add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
b : ℕ
hb : 2 ≤ b
a n : ℕ
rw : (a + a * (b - 1)) / (b - 1) = a + a / (b - 1)
⊢ (a * 1 + a * (b - 1)) / (b - 1) = a + a / (b - 1)
have rw₁ : a / (b - 1) + a = a + a / (b - 1)
Tactic: rw [mul_one, Nat.add_mul_div_right _ _ (tsub_pos_of_lt hb), add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
b : ℕ
hb : 2 ≤ b
a n : ℕ
rw : (a + a * (b - 1)) / (b - 1) = a + a / (b - 1)
rw₁ : a / (b - 1) + a = a + a / (b - 1)
⊢ (a * 1 + a * (b - 1)) / (b - 1) = a + a / (b - 1)
have rw₂ : a + a / (b - 1) = a + a / (b - 1)
Tactic: rw [mul_one, Nat.add_mul_div_right _ _ (tsub_pos_of_lt hb), add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ a + ∑ i ∈ Ico 1 (n + 1), a / b ^ i ≤ a + a / (b - 1)
have i : a + ∑ i ∈ Ico 1 n.succ, a / b ^ i = a / HPow.hPow (β := ℕ) b 0 + ∑ i ∈ Ico 1 n.succ, a / b ^ i
Tactic: calc
    (a + ∑ i ∈ Ico 1 n.succ, a / b ^ i) = a / b ^ 0 + ∑ i ∈ Ico 1 n.succ, a / b ^ i := by
      rw [pow_zero, Nat.div_one]
    _ = ∑ i ∈ range n.succ, a / b ^ i := by
      rw [range_eq_Ico, ← Finset.insert_Ico_add_one_left_eq_Ico (Nat.succ_pos _), sum_insert] <;>
        simp
    _ ≤ a * b / (b - 1) := Nat.geom_sum_le hb a _
    _ = (a * 1 + a * (b - 1)) / (b - 1) := by rw [← mul_add, add_tsub_cancel_of_le (by lia)]
    _ = a + a / (b - 1) := by rw [mul_one, Nat.add_mul_div_right _ _ (tsub_pos_of_lt hb), add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
b : ℕ
hb : 2 ≤ b
a n : ℕ
i : a + ∑ i ∈ Ico 1 n.succ, a / b ^ i = a / HPow.hPow (β := ℕ) b 0 + ∑ i ∈ Ico 1 n.succ, a / b ^ i
⊢ a + ∑ i ∈ Ico 1 (n + 1), a / b ^ i ≤ a + a / (b - 1)
have i₁ : a / HPow.hPow (β := ℕ) b 0 + ∑ i ∈ Ico 1 n.succ, a / b ^ i = ∑ i ∈ range n.succ, a / b ^ i
Tactic: calc
    (a + ∑ i ∈ Ico 1 n.succ, a / b ^ i) = a / b ^ 0 + ∑ i ∈ Ico 1 n.succ, a / b ^ i := by
      rw [pow_zero, Nat.div_one]
    _ = ∑ i ∈ range n.succ, a / b ^ i := by
      rw [range_eq_Ico, ← Finset.insert_Ico_add_one_left_eq_Ico (Nat.succ_pos _), sum_insert] <;>
        simp
    _ ≤ a * b / (b - 1) := Nat.geom_sum_le hb a _
    _ = (a * 1 + a * (b - 1)) / (b - 1) := by rw [← mul_add, add_tsub_cancel_of_le (by lia)]
    _ = a + a / (b - 1) := by rw [mul_one, Nat.add_mul_div_right _ _ (tsub_pos_of_lt hb), add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
b : ℕ
hb : 2 ≤ b
a n : ℕ
i : a + ∑ i ∈ Ico 1 n.succ, a / b ^ i = a / HPow.hPow (β := ℕ) b 0 + ∑ i ∈ Ico 1 n.succ, a / b ^ i
i₁ : a / HPow.hPow (β := ℕ) b 0 + ∑ i ∈ Ico 1 n.succ, a / b ^ i = ∑ i ∈ range n.succ, a / b ^ i
⊢ a + ∑ i ∈ Ico 1 (n + 1), a / b ^ i ≤ a + a / (b - 1)
have i₂ : a * b / (b - 1) = (a * 1 + a * (b - 1)) / (b - 1)
Tactic: calc
    (a + ∑ i ∈ Ico 1 n.succ, a / b ^ i) = a / b ^ 0 + ∑ i ∈ Ico 1 n.succ, a / b ^ i := by
      rw [pow_zero, Nat.div_one]
    _ = ∑ i ∈ range n.succ, a / b ^ i := by
      rw [range_eq_Ico, ← Finset.insert_Ico_add_one_left_eq_Ico (Nat.succ_pos _), sum_insert] <;>
        simp
    _ ≤ a * b / (b - 1) := Nat.geom_sum_le hb a _
    _ = (a * 1 + a * (b - 1)) / (b - 1) := by rw [← mul_add, add_tsub_cancel_of_le (by lia)]
    _ = a + a / (b - 1) := by rw [mul_one, Nat.add_mul_div_right _ _ (tsub_pos_of_lt hb), add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
b : ℕ
hb : 2 ≤ b
a n : ℕ
i : a + ∑ i ∈ Ico 1 n.succ, a / b ^ i = a / HPow.hPow (β := ℕ) b 0 + ∑ i ∈ Ico 1 n.succ, a / b ^ i
i₁ : a / HPow.hPow (β := ℕ) b 0 + ∑ i ∈ Ico 1 n.succ, a / b ^ i = ∑ i ∈ range n.succ, a / b ^ i
i₂ : a * b / (b - 1) = (a * 1 + a * (b - 1)) / (b - 1)
⊢ a + ∑ i ∈ Ico 1 (n + 1), a / b ^ i ≤ a + a / (b - 1)
have i₃ : (a * 1 + a * (b - 1)) / (b - 1) = a + a / (b - 1)
Tactic: calc
    (a + ∑ i ∈ Ico 1 n.succ, a / b ^ i) = a / b ^ 0 + ∑ i ∈ Ico 1 n.succ, a / b ^ i := by
      rw [pow_zero, Nat.div_one]
    _ = ∑ i ∈ range n.succ, a / b ^ i := by
      rw [range_eq_Ico, ← Finset.insert_Ico_add_one_left_eq_Ico (Nat.succ_pos _), sum_insert] <;>
        simp
    _ ≤ a * b / (b - 1) := Nat.geom_sum_le hb a _
    _ = (a * 1 + a * (b - 1)) / (b - 1) := by rw [← mul_add, add_tsub_cancel_of_le (by lia)]
    _ = a + a / (b - 1) := by rw [mul_one, Nat.add_mul_div_right _ _ (tsub_pos_of_lt hb), add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
a b c : R
mul : a * b = c * a
add_ab : a + b = 1
add_ac : a + c = 1
⊢ b = (a + c) * b
have rw : b = 1 * b
Tactic: rw [add_ac, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
a b c : R
mul : a * b = c * a
add_ab : a + b = 1
add_ac : a + c = 1
rw : b = 1 * b
⊢ b = (a + c) * b
have rw₁ : b = b
Tactic: rw [add_ac, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
a b c : R
mul : a * b = c * a
add_ab : a + b = 1
add_ac : a + c = 1
⊢ (a + c) * b = c * (a + b)
have rw : a * b + c * b = c * (a + b)
Tactic: rw [add_mul, mul, mul_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
a b c : R
mul : a * b = c * a
add_ab : a + b = 1
add_ac : a + c = 1
rw : a * b + c * b = c * (a + b)
⊢ (a + c) * b = c * (a + b)
have rw₁ : c * a + c * b = c * (a + b)
Tactic: rw [add_mul, mul, mul_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
a b c : R
mul : a * b = c * a
add_ab : a + b = 1
add_ac : a + c = 1
rw : a * b + c * b = c * (a + b)
rw₁ : c * a + c * b = c * (a + b)
⊢ (a + c) * b = c * (a + b)
have rw₂ : c * a + c * b = c * a + c * b
Tactic: rw [add_mul, mul, mul_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
a b c : R
mul : a * b = c * a
add_ab : a + b = 1
add_ac : a + c = 1
⊢ c * (a + b) = c
have rw : c * 1 = c
Tactic: rw [add_ab, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
a b c : R
mul : a * b = c * a
add_ab : a + b = 1
add_ac : a + c = 1
rw : c * 1 = c
⊢ c * (a + b) = c
have rw₁ : c = c
Tactic: rw [add_ab, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a b : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a : R × R).1 = (↑b : R × R).1
⊢ a = b
have refine_1 : (↑a : R × R).1 * (↑a : R × R).2 = (↑b : R × R).2 * (↑a : R × R).1
Tactic: refine Subtype.ext <| Prod.ext_iff.mpr ⟨eq, eq_of_mul_eq_add_eq_one a.1.1 ?_ a.2.2 ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a b : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a : R × R).1 = (↑b : R × R).1
refine_1 : (↑a : R × R).1 * (↑a : R × R).2 = (↑b : R × R).2 * (↑a : R × R).1
⊢ a = b
have refine_2 : (↑a : R × R).1 + (↑b : R × R).2 = 1
Tactic: refine Subtype.ext <| Prod.ext_iff.mpr ⟨eq, eq_of_mul_eq_add_eq_one a.1.1 ?_ a.2.2 ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a b : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a : R × R).1 = (↑b : R × R).1
⊢ (↑a : R × R).1 * (↑a : R × R).2 = (↑b : R × R).2 * (↑a : R × R).1
have refine_1 : 0 = (↑b : R × R).2 * (↑a : R × R).1
Tactic: rw [a.2.1, mul_comm, eq, b.2.1]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a b : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a : R × R).1 = (↑b : R × R).1
refine_1 : 0 = (↑b : R × R).2 * (↑a : R × R).1
⊢ (↑a : R × R).1 * (↑a : R × R).2 = (↑b : R × R).2 * (↑a : R × R).1
have refine_1₁ : 0 = (↑a : R × R).1 * (↑b : R × R).2
Tactic: rw [a.2.1, mul_comm, eq, b.2.1]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a b : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a : R × R).1 = (↑b : R × R).1
refine_1 : 0 = (↑b : R × R).2 * (↑a : R × R).1
refine_1₁ : 0 = (↑a : R × R).1 * (↑b : R × R).2
⊢ (↑a : R × R).1 * (↑a : R × R).2 = (↑b : R × R).2 * (↑a : R × R).1
have refine_1₂ : 0 = (↑b : R × R).1 * (↑b : R × R).2
Tactic: rw [a.2.1, mul_comm, eq, b.2.1]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a b : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a : R × R).1 = (↑b : R × R).1
refine_1 : 0 = (↑b : R × R).2 * (↑a : R × R).1
refine_1₁ : 0 = (↑a : R × R).1 * (↑b : R × R).2
refine_1₂ : 0 = (↑b : R × R).1 * (↑b : R × R).2
⊢ (↑a : R × R).1 * (↑a : R × R).2 = (↑b : R × R).2 * (↑a : R × R).1
have refine_1₃ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [a.2.1, mul_comm, eq, b.2.1]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a b : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a : R × R).1 = (↑b : R × R).1
⊢ (↑a : R × R).1 + (↑b : R × R).2 = 1
have refine_2 : (↑b : R × R).1 + (↑b : R × R).2 = 1
Tactic: rw [eq, b.2.2]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a b : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a : R × R).1 = (↑b : R × R).1
refine_2 : (↑b : R × R).1 + (↑b : R × R).2 = 1
⊢ (↑a : R × R).1 + (↑b : R × R).2 = 1
have refine_2₁ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [eq, b.2.2]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a b : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a : R × R).2 = (↑b : R × R).2
⊢ a = b
have refine_1 : (↑a : R × R).2 * (↑a : R × R).1 = (↑b : R × R).1 * (↑a : R × R).2
Tactic: refine Subtype.ext <| Prod.ext_iff.mpr ⟨eq_of_mul_eq_add_eq_one a.1.2 ?_ ?_ ?_, eq⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a b : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a : R × R).2 = (↑b : R × R).2
refine_1 : (↑a : R × R).2 * (↑a : R × R).1 = (↑b : R × R).1 * (↑a : R × R).2
⊢ a = b
have refine_2 : (↑a : R × R).2 + (↑a : R × R).1 = 1
Tactic: refine Subtype.ext <| Prod.ext_iff.mpr ⟨eq_of_mul_eq_add_eq_one a.1.2 ?_ ?_ ?_, eq⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a b : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a : R × R).2 = (↑b : R × R).2
refine_1 : (↑a : R × R).2 * (↑a : R × R).1 = (↑b : R × R).1 * (↑a : R × R).2
refine_2 : (↑a : R × R).2 + (↑a : R × R).1 = 1
⊢ a = b
have refine_3 : (↑a : R × R).2 + (↑b : R × R).1 = 1
Tactic: refine Subtype.ext <| Prod.ext_iff.mpr ⟨eq_of_mul_eq_add_eq_one a.1.2 ?_ ?_ ?_, eq⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a b : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a : R × R).2 = (↑b : R × R).2
⊢ (↑a : R × R).2 * (↑a : R × R).1 = (↑b : R × R).1 * (↑a : R × R).2
have refine_1 : (↑a : R × R).1 * (↑a : R × R).2 = (↑b : R × R).1 * (↑a : R × R).2
Tactic: rw [mul_comm, a.2.1, eq, b.2.1]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a b : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a : R × R).2 = (↑b : R × R).2
refine_1 : (↑a : R × R).1 * (↑a : R × R).2 = (↑b : R × R).1 * (↑a : R × R).2
⊢ (↑a : R × R).2 * (↑a : R × R).1 = (↑b : R × R).1 * (↑a : R × R).2
have refine_1₁ : 0 = (↑b : R × R).1 * (↑a : R × R).2
Tactic: rw [mul_comm, a.2.1, eq, b.2.1]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a b : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a : R × R).2 = (↑b : R × R).2
refine_1 : (↑a : R × R).1 * (↑a : R × R).2 = (↑b : R × R).1 * (↑a : R × R).2
refine_1₁ : 0 = (↑b : R × R).1 * (↑a : R × R).2
⊢ (↑a : R × R).2 * (↑a : R × R).1 = (↑b : R × R).1 * (↑a : R × R).2
have refine_1₂ : 0 = (↑b : R × R).1 * (↑b : R × R).2
Tactic: rw [mul_comm, a.2.1, eq, b.2.1]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a b : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a : R × R).2 = (↑b : R × R).2
refine_1 : (↑a : R × R).1 * (↑a : R × R).2 = (↑b : R × R).1 * (↑a : R × R).2
refine_1₁ : 0 = (↑b : R × R).1 * (↑a : R × R).2
refine_1₂ : 0 = (↑b : R × R).1 * (↑b : R × R).2
⊢ (↑a : R × R).2 * (↑a : R × R).1 = (↑b : R × R).1 * (↑a : R × R).2
have refine_1₃ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [mul_comm, a.2.1, eq, b.2.1]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a b : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a : R × R).2 = (↑b : R × R).2
⊢ (↑a : R × R).2 + (↑a : R × R).1 = 1
have refine_2 : (↑a : R × R).1 + (↑a : R × R).2 = 1
Tactic: rw [add_comm, a.2.2]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a b : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a : R × R).2 = (↑b : R × R).2
refine_2 : (↑a : R × R).1 + (↑a : R × R).2 = 1
⊢ (↑a : R × R).2 + (↑a : R × R).1 = 1
have refine_2₁ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [add_comm, a.2.2]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a b : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a : R × R).2 = (↑b : R × R).2
⊢ (↑a : R × R).2 + (↑b : R × R).1 = 1
have refine_3 : (↑b : R × R).1 + (↑a : R × R).2 = 1
Tactic: rw [add_comm, eq, b.2.2]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a b : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a : R × R).2 = (↑b : R × R).2
refine_3 : (↑b : R × R).1 + (↑a : R × R).2 = 1
⊢ (↑a : R × R).2 + (↑b : R × R).1 = 1
have refine_3₁ : (↑b : R × R).1 + (↑b : R × R).2 = 1
Tactic: rw [add_comm, eq, b.2.2]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a b : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a : R × R).2 = (↑b : R × R).2
refine_3 : (↑b : R × R).1 + (↑a : R × R).2 = 1
refine_3₁ : (↑b : R × R).1 + (↑b : R × R).2 = 1
⊢ (↑a : R × R).2 + (↑b : R × R).1 = 1
have refine_3₂ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [add_comm, eq, b.2.2]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a_1 b_1 a b c : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
hab : (↑a : R × R).1 * (↑b : R × R).1 = (↑a : R × R).1
hbc : (↑b : R × R).1 * (↑c : R × R).1 = (↑b : R × R).1
⊢ (↑a : R × R).1 * (↑c : R × R).1 = (↑a : R × R).1
have rw : (↑a : R × R).1 * (↑b : R × R).1 * (↑c : R × R).1 = (↑a : R × R).1 * (↑b : R × R).1
Tactic: rw [← hab, mul_assoc, hbc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a_1 b_1 a b c : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
hab : (↑a : R × R).1 * (↑b : R × R).1 = (↑a : R × R).1
hbc : (↑b : R × R).1 * (↑c : R × R).1 = (↑b : R × R).1
rw : (↑a : R × R).1 * (↑b : R × R).1 * (↑c : R × R).1 = (↑a : R × R).1 * (↑b : R × R).1
⊢ (↑a : R × R).1 * (↑c : R × R).1 = (↑a : R × R).1
have rw₁ : (↑a : R × R).1 * ((↑b : R × R).1 * (↑c : R × R).1) = (↑a : R × R).1 * (↑b : R × R).1
Tactic: rw [← hab, mul_assoc, hbc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a_1 b_1 a b c : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
hab : (↑a : R × R).1 * (↑b : R × R).1 = (↑a : R × R).1
hbc : (↑b : R × R).1 * (↑c : R × R).1 = (↑b : R × R).1
rw : (↑a : R × R).1 * (↑b : R × R).1 * (↑c : R × R).1 = (↑a : R × R).1 * (↑b : R × R).1
rw₁ : (↑a : R × R).1 * ((↑b : R × R).1 * (↑c : R × R).1) = (↑a : R × R).1 * (↑b : R × R).1
⊢ (↑a : R × R).1 * (↑c : R × R).1 = (↑a : R × R).1
have rw₂ : (↑a : R × R).1 * (↑b : R × R).1 = (↑a : R × R).1 * (↑b : R × R).1
Tactic: rw [← hab, mul_assoc, hbc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a_1 b_1 a b : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
hab : (↑a : R × R).1 * (↑b : R × R).1 = (↑a : R × R).1
hba : (↑b : R × R).1 * (↑a : R × R).1 = (↑b : R × R).1
⊢ (↑a : R × R).1 = (↑b : R × R).1
have rw : (↑a : R × R).1 * (↑b : R × R).1 = (↑b : R × R).1
Tactic: rw [← hab, mul_comm, hba]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a_1 b_1 a b : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
hab : (↑a : R × R).1 * (↑b : R × R).1 = (↑a : R × R).1
hba : (↑b : R × R).1 * (↑a : R × R).1 = (↑b : R × R).1
rw : (↑a : R × R).1 * (↑b : R × R).1 = (↑b : R × R).1
rw₁ : (↑b : R × R).1 * (↑a : R × R).1 = (↑b : R × R).1
⊢ (↑a : R × R).1 = (↑b : R × R).1
have rw₂ : (↑b : R × R).1 = (↑b : R × R).1
Tactic: rw [← hab, mul_comm, hba]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a_1 b_1 a b : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ ((↑a : R × R).1 + (↑a : R × R).2 * (↑b : R × R).1, (↑a : R × R).2 * (↑b : R × R).2).1 *
      ((↑a : R × R).1 + (↑a : R × R).2 * (↑b : R × R).1, (↑a : R × R).2 * (↑b : R × R).2).2 =
    0
have simp_rw : ((↑a : R × R).1 + (↑a : R × R).2 * (↑b : R × R).1) * ((↑a : R × R).2 * (↑b : R × R).2) = 0
Tactic: simp_rw [add_mul,
      mul_mul_mul_comm _ b.1.1, b.2.1, mul_zero, ← mul_assoc, a.2.1, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a_1 b_1 a b : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
simp_rw simp_rw₁ : ((↑a : R × R).1 + (↑a : R × R).2 * (↑b : R × R).1) * ((↑a : R × R).2 * (↑b : R × R).2) = 0
⊢ ((↑a : R × R).1 + (↑a : R × R).2 * (↑b : R × R).1, (↑a : R × R).2 * (↑b : R × R).2).1 *
      ((↑a : R × R).1 + (↑a : R × R).2 * (↑b : R × R).1, (↑a : R × R).2 * (↑b : R × R).2).2 =
    0
have simp_rw₂ : (↑a : R × R).1 * ((↑a : R × R).2 * (↑b : R × R).2) +
    (↑a : R × R).2 * (↑b : R × R).1 * ((↑a : R × R).2 * (↑b : R × R).2) =
  0
Tactic: simp_rw [add_mul,
      mul_mul_mul_comm _ b.1.1, b.2.1, mul_zero, ← mul_assoc, a.2.1, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a_1 b_1 a b : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
simp_rw simp_rw₁ : ((↑a : R × R).1 + (↑a : R × R).2 * (↑b : R × R).1) * ((↑a : R × R).2 * (↑b : R × R).2) = 0
simp_rw₂ :
  (↑a : R × R).1 * ((↑a : R × R).2 * (↑b : R × R).2) +
      (↑a : R × R).2 * (↑b : R × R).1 * ((↑a : R × R).2 * (↑b : R × R).2) =
    0
⊢ ((↑a : R × R).1 + (↑a : R × R).2 * (↑b : R × R).1, (↑a : R × R).2 * (↑b : R × R).2).1 *
      ((↑a : R × R).1 + (↑a : R × R).2 * (↑b : R × R).1, (↑a : R × R).2 * (↑b : R × R).2).2 =
    0
have simp_rw₃ : (↑a : R × R).1 * ((↑a : R × R).2 * (↑b : R × R).2) +
    (↑a : R × R).2 * (↑a : R × R).2 * ((↑b : R × R).1 * (↑b : R × R).2) =
  0
Tactic: simp_rw [add_mul,
      mul_mul_mul_comm _ b.1.1, b.2.1, mul_zero, ← mul_assoc, a.2.1, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a_1 b_1 a b : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
simp_rw simp_rw₁ : ((↑a : R × R).1 + (↑a : R × R).2 * (↑b : R × R).1) * ((↑a : R × R).2 * (↑b : R × R).2) = 0
simp_rw₂ :
  (↑a : R × R).1 * ((↑a : R × R).2 * (↑b : R × R).2) +
      (↑a : R × R).2 * (↑b : R × R).1 * ((↑a : R × R).2 * (↑b : R × R).2) =
    0
simp_rw₃ :
  (↑a : R × R).1 * ((↑a : R × R).2 * (↑b : R × R).2) +
      (↑a : R × R).2 * (↑a : R × R).2 * ((↑b : R × R).1 * (↑b : R × R).2) =
    0
⊢ ((↑a : R × R).1 + (↑a : R × R).2 * (↑b : R × R).1, (↑a : R × R).2 * (↑b : R × R).2).1 *
      ((↑a : R × R).1 + (↑a : R × R).2 * (↑b : R × R).1, (↑a : R × R).2 * (↑b : R × R).2).2 =
    0
have simp_rw₄ : (↑a : R × R).1 * ((↑a : R × R).2 * (↑b : R × R).2) + (↑a : R × R).2 * (↑a : R × R).2 * 0 = 0
Tactic: simp_rw [add_mul,
      mul_mul_mul_comm _ b.1.1, b.2.1, mul_zero, ← mul_assoc, a.2.1, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
a_1 b_1 a b : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
simp_rw simp_rw₁ : ((↑a : R × R).1 + (↑a : R × R).2 * (↑b : R × R).1) * ((↑a : R × R).2 * (↑b : R × R).2) = 0
simp_rw₂ :
  (↑a : R × R).1 * ((↑a : R × R).2 * (↑b : R × R).2) +
      (↑a : R × R).2 * (↑b : R × R).1 * ((↑a : R × R).2 * (↑b : R × R).2) =
    0
simp_rw₃ :
  (↑a : R × R).1 * ((↑a : R × R).2 * (↑b : R × R).2) +
      (↑a : R × R).2 * (↑a : R × R).2 * ((↑b : R × R).1 * (↑b : R × R).2) =
    0
simp_rw₄ : (↑a : R × R).1 * ((↑a : R × R).2 * (↑b : R × R).2) + (↑a : R × R).2 * (↑a : R × R).2 * 0 = 0
⊢ ((↑a : R × R).1 + (↑a : R × R).2 * (↑b : R × R).1, (↑a : R × R).2 * (↑b : R × R).2).1 *
      ((↑a : R × R).1 + (↑a : R × R).2 * (↑b : R × R).1, (↑a : R × R).2 * (↑b : R × R).2).2 =
    0
have simp_rw₅ : (↑a : R × R).1 * ((↑a : R × R).2 * (↑b : R × R).2) + 0 = 0
Tactic: simp_rw [add_mul,
      mul_mul_mul_comm _ b.1.1, b.2.1, mul_zero, ← mul_assoc, a.2.1, zero_mul, add_zero]