awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Ring.Invertible (hypothesis)
Goal:
R : Type u_1
inst : Ring R
a b : R
inst_1 : Invertible a
inst_2 : Invertible b
inst_3 : Invertible (a + b)
h :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (a + b) _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
⊢ a * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a =
    b * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b
have h' : -1 =
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b +
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a
Tactic: have h' := neg_one_eq_invOf_mul_add_invOf_mul_iff.mp h
-- Lean 4 proof step from Mathlib.Algebra.Ring.Invertible (hypothesis)
Goal:
R : Type u_1
inst : Ring R
a b : R
inst_1 : Invertible a
inst_2 : Invertible b
inst_3 : Invertible (a + b)
h :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (a + b) _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
h' :
  -1 =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a
⊢ a * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a =
    b * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b
have h_a_binv_a : -(b + a) = a * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a
Tactic: have h_a_binv_a : -(b + a) = a * ⅟b * a := neg_add_eq_mul_invOf_mul_same_iff.mpr h'
-- Lean 4 proof step from Mathlib.Algebra.Ring.Invertible (hypothesis)
Goal:
R : Type u_1
inst : Ring R
a b : R
inst_1 : Invertible a
inst_2 : Invertible b
inst_3 : Invertible (a + b)
h :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (a + b) _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
h' :
  -1 =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a
h_a_binv_a : -(b + a) = a * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a
⊢ -(a + b) = b * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b
have h'₁ : -1 =
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a +
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b
Tactic: rw [add_comm] at h'
Cleared hypotheses: h', h_a_binv_a
-- Lean 4 proof step from Mathlib.Algebra.Ring.Invertible (hypothesis)
Goal:
R : Type u_1
inst : Ring R
a b : R
inst_1 : Invertible a
inst_2 : Invertible b
inst_3 : Invertible (a + b)
h :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (a + b) _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
h' :
  -1 =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a
h_a_binv_a : -(b + a) = a * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a
⊢ a * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a =
    b * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b
have h_b_ainv_b : -(a + b) = b * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b
Tactic: have h_b_ainv_b : -(a + b) = b * ⅟a * b := by
    rw [add_comm] at h'
    exact neg_add_eq_mul_invOf_mul_same_iff.mpr h'
-- Lean 4 proof step from Mathlib.Algebra.Ring.Invertible (goal)
Goal:
R : Type u_1
inst : Ring R
a b : R
inst_1 : Invertible a
inst_2 : Invertible b
inst_3 : Invertible (a + b)
h :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (a + b) _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
h' :
  -1 =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a
h_a_binv_a : -(b + a) = a * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a
h_b_ainv_b : -(a + b) = b * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b
⊢ a * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a =
    b * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b
have rw : -(b + a) = b * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b
Tactic: rw [← h_a_binv_a, ← h_b_ainv_b, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Invertible (goal)
Goal:
R : Type u_1
inst : Ring R
a b : R
inst_1 : Invertible a
inst_2 : Invertible b
inst_3 : Invertible (a + b)
h :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (a + b) _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
h' :
  -1 =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a
h_a_binv_a : -(b + a) = a * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a
h_b_ainv_b : -(a + b) = b * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b
rw : -(b + a) = b * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b
⊢ a * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a =
    b * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b
have rw₁ : -(b + a) = -(a + b)
Tactic: rw [← h_a_binv_a, ← h_b_ainv_b, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Invertible (goal)
Goal:
R : Type u_1
inst : Ring R
a b : R
inst_1 : Invertible a
inst_2 : Invertible b
inst_3 : Invertible (a + b)
h :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (a + b) _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
h' :
  -1 =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a
h_a_binv_a : -(b + a) = a * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a
h_b_ainv_b : -(a + b) = b * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b
rw : -(b + a) = b * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b
rw₁ : -(b + a) = -(a + b)
⊢ a * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a =
    b * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b
have rw₂ : -(a + b) = -(a + b)
Tactic: rw [← h_a_binv_a, ← h_b_ainv_b, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Invertible (goal)
Goal:
R : Type u_1
inst : Semiring R
a b : R
h : IsUnit a ↔ IsUnit b
⊢ a⁻¹ʳ + b⁻¹ʳ = a⁻¹ʳ * (a + b) * b⁻¹ʳ
have pos : ∀ (ha : IsUnit a), a⁻¹ʳ + b⁻¹ʳ = a⁻¹ʳ * (a + b) * b⁻¹ʳ
Tactic: by_cases ha : IsUnit a
-- Lean 4 proof step from Mathlib.Algebra.Ring.Invertible (goal)
Goal:
R : Type u_1
inst : Semiring R
a b : R
h : IsUnit a ↔ IsUnit b
pos : ∀ (ha : IsUnit a), a⁻¹ʳ + b⁻¹ʳ = a⁻¹ʳ * (a + b) * b⁻¹ʳ
⊢ a⁻¹ʳ + b⁻¹ʳ = a⁻¹ʳ * (a + b) * b⁻¹ʳ
have neg : ∀ (ha : ¬IsUnit a), a⁻¹ʳ + b⁻¹ʳ = a⁻¹ʳ * (a + b) * b⁻¹ʳ
Tactic: by_cases ha : IsUnit a
-- Lean 4 proof step from Mathlib.Algebra.Ring.Invertible (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
⊢ a⁻¹ʳ + b⁻¹ʳ = a⁻¹ʳ * (a + b) * b⁻¹ʳ
have hb : IsUnit b
Tactic: have hb := h.mp ha
-- Lean 4 proof step from Mathlib.Algebra.Ring.Invertible (goal)
Goal:
R : Type u_1
inst : Semiring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
hb : IsUnit b
⊢ a⁻¹ʳ + b⁻¹ʳ = a⁻¹ʳ * (a + b) * b⁻¹ʳ
have pos : ∀ (ia : Invertible a), a⁻¹ʳ + b⁻¹ʳ = a⁻¹ʳ * (a + b) * b⁻¹ʳ
Tactic: obtain ⟨ia⟩ := ha.nonempty_invertible
-- Lean 4 proof step from Mathlib.Algebra.Ring.Invertible (goal)
Goal:
R : Type u_1
inst : Semiring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
hb : IsUnit b
ia : Invertible a
⊢ a⁻¹ʳ + b⁻¹ʳ = a⁻¹ʳ * (a + b) * b⁻¹ʳ
have pos : ∀ (ib : Invertible b), a⁻¹ʳ + b⁻¹ʳ = a⁻¹ʳ * (a + b) * b⁻¹ʳ
Tactic: obtain ⟨ib⟩ := hb.nonempty_invertible
-- Lean 4 proof step from Mathlib.Algebra.Ring.Invertible (goal)
Goal:
R : Type u_1
inst : Semiring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
hb : IsUnit b
ia : Invertible a
ib : Invertible b
⊢ a⁻¹ʳ + b⁻¹ʳ = a⁻¹ʳ * (a + b) * b⁻¹ʳ
have pos : @Invertible.invOf _ MulZeroClass.toMul MulOne.toOne a _ + @Invertible.invOf _ MulZeroClass.toMul MulOne.toOne b _ =
  @Invertible.invOf _ MulZeroClass.toMul MulOne.toOne a _ * (a + b) *
    @Invertible.invOf _ MulZeroClass.toMul MulOne.toOne b _
Tactic: simp_rw [inverse_invertible, invOf_add_invOf]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Invertible (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : ¬IsUnit a
⊢ a⁻¹ʳ + b⁻¹ʳ = a⁻¹ʳ * (a + b) * b⁻¹ʳ
have hb : ¬IsUnit b
Tactic: have hb := h.not.mp ha
-- Lean 4 proof step from Mathlib.Algebra.Ring.Invertible (goal)
Goal:
R : Type u_1
inst : Ring R
a b : R
h : IsUnit a ↔ IsUnit b
⊢ a⁻¹ʳ - b⁻¹ʳ = a⁻¹ʳ * (b - a) * b⁻¹ʳ
have pos : ∀ (ha : IsUnit a), a⁻¹ʳ - b⁻¹ʳ = a⁻¹ʳ * (b - a) * b⁻¹ʳ
Tactic: by_cases ha : IsUnit a
-- Lean 4 proof step from Mathlib.Algebra.Ring.Invertible (goal)
Goal:
R : Type u_1
inst : Ring R
a b : R
h : IsUnit a ↔ IsUnit b
pos : ∀ (ha : IsUnit a), a⁻¹ʳ - b⁻¹ʳ = a⁻¹ʳ * (b - a) * b⁻¹ʳ
⊢ a⁻¹ʳ - b⁻¹ʳ = a⁻¹ʳ * (b - a) * b⁻¹ʳ
have neg : ∀ (ha : ¬IsUnit a), a⁻¹ʳ - b⁻¹ʳ = a⁻¹ʳ * (b - a) * b⁻¹ʳ
Tactic: by_cases ha : IsUnit a
-- Lean 4 proof step from Mathlib.Algebra.Ring.Invertible (hypothesis)
Goal:
R : Type u_1
inst : Ring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
⊢ a⁻¹ʳ - b⁻¹ʳ = a⁻¹ʳ * (b - a) * b⁻¹ʳ
have hb : IsUnit b
Tactic: have hb := h.mp ha
-- Lean 4 proof step from Mathlib.Algebra.Ring.Invertible (goal)
Goal:
R : Type u_1
inst : Ring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
hb : IsUnit b
⊢ a⁻¹ʳ - b⁻¹ʳ = a⁻¹ʳ * (b - a) * b⁻¹ʳ
have pos : ∀ (ia : Invertible a), a⁻¹ʳ - b⁻¹ʳ = a⁻¹ʳ * (b - a) * b⁻¹ʳ
Tactic: obtain ⟨ia⟩ := ha.nonempty_invertible
-- Lean 4 proof step from Mathlib.Algebra.Ring.Invertible (goal)
Goal:
R : Type u_1
inst : Ring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
hb : IsUnit b
ia : Invertible a
⊢ a⁻¹ʳ - b⁻¹ʳ = a⁻¹ʳ * (b - a) * b⁻¹ʳ
have pos : ∀ (ib : Invertible b), a⁻¹ʳ - b⁻¹ʳ = a⁻¹ʳ * (b - a) * b⁻¹ʳ
Tactic: obtain ⟨ib⟩ := hb.nonempty_invertible
-- Lean 4 proof step from Mathlib.Algebra.Ring.Invertible (goal)
Goal:
R : Type u_1
inst : Ring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
hb : IsUnit b
ia : Invertible a
ib : Invertible b
⊢ a⁻¹ʳ - b⁻¹ʳ = a⁻¹ʳ * (b - a) * b⁻¹ʳ
have pos : @Invertible.invOf _ MulZeroClass.toMul MulOne.toOne a _ - @Invertible.invOf _ MulZeroClass.toMul MulOne.toOne b _ =
  @Invertible.invOf _ MulZeroClass.toMul MulOne.toOne a _ * (b - a) *
    @Invertible.invOf _ MulZeroClass.toMul MulOne.toOne b _
Tactic: simp_rw [inverse_invertible, invOf_sub_invOf]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Invertible (hypothesis)
Goal:
R : Type u_1
inst : Ring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : ¬IsUnit a
⊢ a⁻¹ʳ - b⁻¹ʳ = a⁻¹ʳ * (b - a) * b⁻¹ʳ
have hb : ¬IsUnit b
Tactic: have hb := h.not.mp ha
-- Lean 4 proof step from Mathlib.Algebra.Ring.IsFormallyReal (goal)
Goal:
R : Type u_1
inst : AddMonoid R
inst_1 : Mul R
s₁ s₂ : R
h₁ : IsSumNonzeroSq s₁
h₂ : IsSumNonzeroSq s₂
⊢ IsSumNonzeroSq (s₁ + s₂)
have sq : ∀ {a : R}, a ≠ 0 → IsSumNonzeroSq (a * a + s₂)
Tactic: induction h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Algebra.Ring.IsFormallyReal (goal)
Goal:
R : Type u_1
inst : AddMonoid R
inst_1 : Mul R
s₁ s₂ : R
h₁ : IsSumNonzeroSq s₁
h₂ : IsSumNonzeroSq s₂
sq : ∀ {a : R}, a ≠ 0 → IsSumNonzeroSq (a * a + s₂)
⊢ IsSumNonzeroSq (s₁ + s₂)
have sq_add : ∀ {a s : R}, a ≠ 0 → IsSumNonzeroSq s → IsSumNonzeroSq (s + s₂) → IsSumNonzeroSq (a * a + s + s₂)
Tactic: induction h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Algebra.Ring.IsFormallyReal (goal)
Goal:
R : Type u_1
inst : AddMonoid R
inst_1 : Mul R
s : R
h : IsSumNonzeroSq s
⊢ IsSumSq s
have sq : ∀ {a : R}, a ≠ 0 → IsSumSq (a * a)
Tactic: induction h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Ring.IsFormallyReal (goal)
Goal:
R : Type u_1
inst : AddMonoid R
inst_1 : Mul R
s : R
h : IsSumNonzeroSq s
sq : ∀ {a : R}, a ≠ 0 → IsSumSq (a * a)
⊢ IsSumSq s
have sq_add : ∀ {a s : R}, a ≠ 0 → IsSumNonzeroSq s → IsSumSq s → IsSumSq (a * a + s)
Tactic: induction h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Ring.IsFormallyReal (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
s_1 a s : R
hs_1 : IsSumSq s
ih : ∀ (hs : s ≠ 0), IsSumNonzeroSq s
hs : a * a + s ≠ 0
⊢ IsSumNonzeroSq (a * a + s)
have sq_add : ∀ (hs : HMul.hMul (α := R) 0 0 + s ≠ 0), IsSumNonzeroSq (HMul.hMul (α := R) 0 0 + s)
Tactic: rcases eq_or_ne a 0 with (rfl | ne_a)
Cleared hypotheses: a, hs
-- Lean 4 proof step from Mathlib.Algebra.Ring.IsFormallyReal (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
s_1 a s : R
hs_1 : IsSumSq s
ih : ∀ (hs : s ≠ 0), IsSumNonzeroSq s
hs : a * a + s ≠ 0
sq_add : ∀ (hs : HMul.hMul (α := R) 0 0 + s ≠ 0), IsSumNonzeroSq (HMul.hMul (α := R) 0 0 + s)
⊢ IsSumNonzeroSq (a * a + s)
have sq_add₁ : ∀ (ne_a : a ≠ 0), IsSumNonzeroSq (a * a + s)
Tactic: rcases eq_or_ne a 0 with (rfl | ne_a)
-- Lean 4 proof step from Mathlib.Algebra.Ring.IsFormallyReal (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
s_1 a s : R
hs_1 : IsSumSq s
ih : ∀ (hs : s ≠ 0), IsSumNonzeroSq s
hs : a * a + s ≠ 0
ne_a : a ≠ 0
⊢ IsSumNonzeroSq (a * a + s)
have sq_add : ∀ (hs : IsSumSq.{u_1} (R := R) 0) (ih : ∀ (hs : Ne.{u_1 + 1} (α := R) 0 0), IsSumNonzeroSq.{u_1} (R := R) 0)
  (hs : a * a + 0 ≠ 0), IsSumNonzeroSq (a * a + 0)
Tactic: rcases eq_or_ne s 0 with (rfl | ne_s)
Cleared hypotheses: s, hs_1, ih, hs
-- Lean 4 proof step from Mathlib.Algebra.Ring.IsFormallyReal (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
s_1 a s : R
hs_1 : IsSumSq s
ih : ∀ (hs : s ≠ 0), IsSumNonzeroSq s
hs : a * a + s ≠ 0
ne_a : a ≠ 0
sq_add :
  ∀ (hs : IsSumSq.{u_1} (R := R) 0) (ih : ∀ (hs : Ne.{u_1 + 1} (α := R) 0 0), IsSumNonzeroSq.{u_1} (R := R) 0)
    (hs : a * a + 0 ≠ 0), IsSumNonzeroSq (a * a + 0)
⊢ IsSumNonzeroSq (a * a + s)
have sq_add₁ : ∀ (ne_s : s ≠ 0), IsSumNonzeroSq (a * a + s)
Tactic: rcases eq_or_ne s 0 with (rfl | ne_s)
-- Lean 4 proof step from Mathlib.Algebra.Ring.IsFormallyReal (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
s : R
hs : s ≠ 0
h : IsSumSq s
⊢ IsSumNonzeroSq s
have zero : ∀ (hs : Ne.{u_1 + 1} (α := R) 0 0), IsSumNonzeroSq.{u_1} (R := R) 0
Tactic: induction h with
    | zero => grind
    | @sq_add a s hs ih =>
    rcases eq_or_ne a 0 with (rfl | ne_a)
    · simp_all
    · rcases eq_or_ne s 0 with (rfl | ne_s)
      · simpa using IsSumNonzeroSq.sq ne_a
      · exact IsSumNonzeroSq.sq_add ne_a (ih ne_s)
Cleared hypotheses: hs, h
-- Lean 4 proof step from Mathlib.Algebra.Ring.IsFormallyReal (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
s : R
hs : s ≠ 0
h : IsSumSq s
zero : ∀ (hs : Ne.{u_1 + 1} (α := R) 0 0), IsSumNonzeroSq.{u_1} (R := R) 0
⊢ IsSumNonzeroSq s
have sq_add : ∀ (a : R) {s : R} (hs : IsSumSq s) (ih : ∀ (hs : s ≠ 0), IsSumNonzeroSq s) (hs : a * a + s ≠ 0),
  IsSumNonzeroSq (a * a + s)
Tactic: induction h with
    | zero => grind
    | @sq_add a s hs ih =>
    rcases eq_or_ne a 0 with (rfl | ne_a)
    · simp_all
    · rcases eq_or_ne s 0 with (rfl | ne_s)
      · simpa using IsSumNonzeroSq.sq ne_a
      · exact IsSumNonzeroSq.sq_add ne_a (ih ne_s)
Cleared hypotheses: hs, h
-- Lean 4 proof step from Mathlib.Algebra.Ring.IsFormallyReal (goal)
Goal:
R : Type u_1
inst : AddMonoid R
inst_1 : Mul R
⊢ Eq (α := AddSubsemigroup R) (closure {x : R | ∃ (x_1 : R), x_1 ≠ 0 ∧ x_1 * x_1 = x}) (sumNonzeroSq R)
have refine : ∀ (x : R) (hx : Membership.mem (γ := AddSubsemigroup R) (sumNonzeroSq R) x),
  Membership.mem (γ := AddSubsemigroup R) (closure {x : R | ∃ (x_1 : R), x_1 ≠ 0 ∧ x_1 * x_1 = x}) x
Tactic: refine closure_eq_of_le (fun x hx ↦ by aesop) (fun x hx ↦ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Ring.IsFormallyReal (goal)
Goal:
R : Type u_1
inst : AddMonoid R
inst_1 : Mul R
x a s : R
ha : a ≠ 0
hs : IsSumNonzeroSq s
ih : Membership.mem (γ := AddSubsemigroup R) (closure {x : R | ∃ (x_1 : R), x_1 ≠ 0 ∧ x_1 * x_1 = x}) s
⊢ Membership.mem (γ := AddSubsemigroup R) (closure {x : R | ∃ (x_1 : R), x_1 ≠ 0 ∧ x_1 * x_1 = x}) (a * a + s)
have sq_add : Membership.mem (γ := AddSubsemigroup R) (closure {x : R | ∃ (x_1 : R), x_1 ≠ 0 ∧ x_1 * x_1 = x}) (a * a)
Tactic: apply add_mem
-- Lean 4 proof step from Mathlib.Algebra.Ring.IsFormallyReal (goal)
Goal:
R : Type u_1
inst : AddMonoid R
inst_1 : Mul R
x a s : R
ha : a ≠ 0
hs : IsSumNonzeroSq s
ih : Membership.mem (γ := AddSubsemigroup R) (closure {x : R | ∃ (x_1 : R), x_1 ≠ 0 ∧ x_1 * x_1 = x}) s
⊢ Membership.mem (γ := AddSubsemigroup R) (closure {x : R | ∃ (x_1 : R), x_1 ≠ 0 ∧ x_1 * x_1 = x}) (a * a)
have sq_add : Membership.mem (γ := Set R) {x : R | ∃ (x_1 : R), x_1 ≠ 0 ∧ x_1 * x_1 = x} (a * a)
Tactic: apply AddSubsemigroup.mem_closure_of_mem
-- Lean 4 proof step from Mathlib.Algebra.Ring.IsFormallyReal (goal)
Goal:
R : Type u_1
inst : AddMonoid R
inst_1 : Mul R
x : R
hx : Membership.mem (γ := AddSubsemigroup R) (sumNonzeroSq R) x
⊢ Membership.mem (γ := AddSubsemigroup R) (closure {x : R | ∃ (x_1 : R), x_1 ≠ 0 ∧ x_1 * x_1 = x}) x
have sq : ∀ {a : R} (ha : a ≠ 0),
  Membership.mem (γ := AddSubsemigroup R) (closure {x : R | ∃ (x_1 : R), x_1 ≠ 0 ∧ x_1 * x_1 = x}) (a * a)
Tactic: induction hx with
  | sq ha => aesop
  | sq_add ha hs ih =>
    -- `aesop` times out
    apply add_mem
    · apply AddSubsemigroup.mem_closure_of_mem
      aesop
    aesop
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Ring.IsFormallyReal (goal)
Goal:
R : Type u_1
inst : AddMonoid R
inst_1 : Mul R
x : R
hx : Membership.mem (γ := AddSubsemigroup R) (sumNonzeroSq R) x
sq :
  ∀ {a : R} (ha : a ≠ 0),
    Membership.mem (γ := AddSubsemigroup R) (closure {x : R | ∃ (x_1 : R), x_1 ≠ 0 ∧ x_1 * x_1 = x}) (a * a)
⊢ Membership.mem (γ := AddSubsemigroup R) (closure {x : R | ∃ (x_1 : R), x_1 ≠ 0 ∧ x_1 * x_1 = x}) x
have sq_add : ∀ {a s : R} (ha : a ≠ 0) (hs : IsSumNonzeroSq s)
  (ih : Membership.mem (γ := AddSubsemigroup R) (closure {x : R | ∃ (x_1 : R), x_1 ≠ 0 ∧ x_1 * x_1 = x}) s),
  Membership.mem (γ := AddSubsemigroup R) (closure {x : R | ∃ (x_1 : R), x_1 ≠ 0 ∧ x_1 * x_1 = x}) (a * a + s)
Tactic: induction hx with
  | sq ha => aesop
  | sq_add ha hs ih =>
    -- `aesop` times out
    apply add_mem
    · apply AddSubsemigroup.mem_closure_of_mem
      aesop
    aesop
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Ring.IsFormallyReal (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : Mul R
hz : ∀ {a : R}, a * a = 0 → a = 0
ha : ∀ {s₁ s₂ : R}, IsSumSq s₁ → IsSumSq s₂ → s₁ + s₂ = 0 → s₁ = 0
⊢ ¬IsSumNonzeroSq.{u_1} (R := R) 0
have suffices : ∀ (x : R), IsSumNonzeroSq x → x ≠ 0
Tactic: suffices ∀ (x : R), IsSumNonzeroSq x → x ≠ 0 by grind
-- Lean 4 proof step from Mathlib.Algebra.Ring.IsFormallyReal (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : Mul R
hz : ∀ {a : R}, a * a = 0 → a = 0
ha : ∀ {s₁ s₂ : R}, IsSumSq s₁ → IsSumSq s₂ → s₁ + s₂ = 0 → s₁ = 0
x : R
hx : IsSumNonzeroSq x
⊢ x ≠ 0
have sq : ∀ {a : R} (ha : a ≠ 0), a * a ≠ 0
Tactic: induction hx with
    | sq ha => grind
    | @sq_add b s hb hs ih => grind [ha (IsSumSq.mul_self b) hs.isSumSq]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Ring.IsFormallyReal (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : Mul R
hz : ∀ {a : R}, a * a = 0 → a = 0
ha : ∀ {s₁ s₂ : R}, IsSumSq s₁ → IsSumSq s₂ → s₁ + s₂ = 0 → s₁ = 0
x : R
hx : IsSumNonzeroSq x
sq : ∀ {a : R} (ha : a ≠ 0), a * a ≠ 0
⊢ x ≠ 0
have sq_add : ∀ {b s : R} (hb : b ≠ 0) (hs : IsSumNonzeroSq s) (ih : s ≠ 0), b * b + s ≠ 0
Tactic: induction hx with
    | sq ha => grind
    | @sq_add b s hb hs ih => grind [ha (IsSumSq.mul_self b) hs.isSumSq]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Ring.IsFormallyReal (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
h : ∀ {s a : R}, IsSumSq s → a * a + s = 0 → a = 0
⊢ ¬IsSumNonzeroSq.{u_1} (R := R) 0
have suffices : ∀ (x : R), IsSumNonzeroSq x → x ≠ 0
Tactic: suffices ∀ (x : R), IsSumNonzeroSq x → x ≠ 0 by grind
-- Lean 4 proof step from Mathlib.Algebra.Ring.IsFormallyReal (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
h : ∀ {s a : R}, IsSumSq s → a * a + s = 0 → a = 0
x : R
hx : IsSumNonzeroSq x
⊢ x ≠ 0
have sq : ∀ {a : R} (ha : a ≠ 0), a * a ≠ 0
Tactic: induction hx with
    | sq ha => exact fun hc ↦ ha (h IsSumSq.zero (by simpa using hc))
    | sq_add ha hs ih => grind [hs.isSumSq]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Ring.IsFormallyReal (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
h : ∀ {s a : R}, IsSumSq s → a * a + s = 0 → a = 0
x : R
hx : IsSumNonzeroSq x
sq : ∀ {a : R} (ha : a ≠ 0), a * a ≠ 0
⊢ x ≠ 0
have sq_add : ∀ {a s : R} (ha : a ≠ 0) (hs : IsSumNonzeroSq s) (ih : s ≠ 0), a * a + s ≠ 0
Tactic: induction hx with
    | sq ha => exact fun hc ↦ ha (h IsSumSq.zero (by simpa using hc))
    | sq_add ha hs ih => grind [hs.isSumSq]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Ring.IsFormallyReal (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsFormallyReal R
⊢ IsReduced R
have rw : ∀ (x : R), HPow.hPow (β := ℕ) x 2 = 0 → x = 0
Tactic: rw [isReduced_iff_pow_one_lt 2 (by lia)]
-- Lean 4 proof step from Mathlib.Algebra.Ring.IsFormallyReal (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsFormallyReal R
x : R
hx : HPow.hPow (β := ℕ) x 2 = 0
⊢ x = 0
have by_contra! : ∀ (hc : x ≠ 0), False
Tactic: by_contra! hc
-- Lean 4 proof step from Mathlib.Algebra.Ring.IsFormallyReal (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
inst_1 : IsFormallyReal R
s₁ s₂ : R
hs₁ : IsSumSq s₁
hs₂ : IsSumSq s₂
h : s₁ + s₂ = 0
⊢ s₁ = 0
have by_contra! : ∀ (h₁ : s₁ ≠ 0), False
Tactic: by_contra! h₁
-- Lean 4 proof step from Mathlib.Algebra.Ring.IsFormallyReal (hypothesis)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
inst_1 : IsFormallyReal R
s₁ s₂ : R
hs₁ : IsSumSq s₁
hs₂ : IsSumSq s₂
h : s₁ + s₂ = 0
h₁ : s₁ ≠ 0
⊢ False
have h₂ : s₂ ≠ 0
Tactic: have h₂ : s₂ ≠ 0 := fun hc ↦ by simp_all
-- Lean 4 proof step from Mathlib.Algebra.Ring.IsFormallyReal (hypothesis)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
inst_1 : IsFormallyReal R
s₁ s₂ : R
hs₁ : IsSumSq s₁
hs₂ : IsSumSq s₂
h : s₁ + s₂ = 0
h₁ : s₁ ≠ 0
h₂ : s₂ ≠ 0
⊢ False
have hs₃ : IsSumNonzeroSq s₁
Tactic: rw [← isSumNonzeroSq_iff_isSumSq h₁] at hs₁
Cleared hypotheses: hs₁, hs₂, h, h₁, h₂
-- Lean 4 proof step from Mathlib.Algebra.Ring.IsFormallyReal (hypothesis)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
inst_1 : IsFormallyReal R
s₁ s₂ : R
hs₁ : IsSumNonzeroSq s₁
hs₂ : IsSumSq s₂
h : s₁ + s₂ = 0
h₁ : s₁ ≠ 0
h₂ : s₂ ≠ 0
⊢ False
have hs₃ : IsSumNonzeroSq s₂
Tactic: rw [← isSumNonzeroSq_iff_isSumSq h₂] at hs₂
Cleared hypotheses: hs₂, h, h₁, h₂
-- Lean 4 proof step from Mathlib.Algebra.Ring.MinimalAxioms (goal)
Goal:
R : Type u
inst : Add R
inst_1 : Mul R
inst_2 : Neg R
inst_3 : Zero R
inst_4 : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add neg_add_cancel
a b : R
⊢ HAdd.hAdd (α := R) 1 1 * (a + b) = a + (a + b) + b
have rw : HAdd.hAdd (α := R) 1 1 * a + HAdd.hAdd (α := R) 1 1 * b = a + (a + b) + b
Tactic: rw [left_distrib]