awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.Invertible
Goal:
R : Type u_1
inst : Ring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : ¬IsUnit a
⊢ ¬IsUnit b

Tactic:
have hb := h.not.mp ha
-- Module: Mathlib.Algebra.Ring.Invertible
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⁻¹ʳ

Tactic:
simp [inverse_non_unit, ha, hb]

Premises used: Ring.inverse_non_unit
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
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₂)
sq_add : ∀ {a s : R}, a ≠ 0 → IsSumNonzeroSq s → IsSumNonzeroSq (s + s₂) → IsSumNonzeroSq (a * a + s + s₂)
⊢ IsSumNonzeroSq (s₁ + s₂)

Tactic:
induction h₁
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
Goal:
R : Type u_1
inst : AddMonoid R
inst_1 : Mul R
s₁ s₂ : R
h₂ : IsSumNonzeroSq s₂
a : R
ha : a ≠ 0
⊢ IsSumNonzeroSq (a * a + s₂)

Tactic:
simp_all [sq_add, add_assoc]

Premises used: IsSumNonzeroSq.sq_add, add_assoc
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
Goal:
R : Type u_1
inst : AddMonoid R
inst_1 : Mul R
s₁ s₂ : R
h₂ : IsSumNonzeroSq s₂
a s : R
ha : a ≠ 0
hs : IsSumNonzeroSq s
hs_ih : IsSumNonzeroSq (s + s₂)
⊢ IsSumNonzeroSq (a * a + s + s₂)

Tactic:
simp_all [sq_add, add_assoc]

Premises used: IsSumNonzeroSq.sq_add, add_assoc
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
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)
sq_add : ∀ {a s : R}, a ≠ 0 → IsSumNonzeroSq s → IsSumSq s → IsSumSq (a * a + s)
⊢ IsSumSq s

Tactic:
induction h
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
Goal:
R : Type u_1
inst : AddMonoid R
inst_1 : Mul R
s a : R
ha : a ≠ 0
⊢ IsSumSq (a * a)

Tactic:
aesop
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
Goal:
R : Type u_1
inst : AddMonoid R
inst_1 : Mul R
s a s_1 : R
ha : a ≠ 0
hs : IsSumNonzeroSq s_1
hs_ih : IsSumSq s_1
⊢ IsSumSq (a * a + s_1)

Tactic:
aesop
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
s : R
hs : Ne.{u_1 + 1} (α := R) 0 0
⊢ IsSumNonzeroSq.{u_1} (R := R) 0

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
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)
sq_add₁ : ∀ (ne_a : a ≠ 0), IsSumNonzeroSq (a * a + s)
⊢ IsSumNonzeroSq (a * a + s)

Tactic:
rcases eq_or_ne a 0 with (rfl | ne_a)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
s_1 s : R
hs_1 : IsSumSq s
ih : ∀ (hs : s ≠ 0), IsSumNonzeroSq s
hs : HMul.hMul (α := R) 0 0 + s ≠ 0
⊢ IsSumNonzeroSq (HMul.hMul (α := R) 0 0 + s)

Tactic:
simp_all
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
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)
sq_add₁ : ∀ (ne_s : s ≠ 0), IsSumNonzeroSq (a * a + s)
⊢ IsSumNonzeroSq (a * a + s)

Tactic:
rcases eq_or_ne s 0 with (rfl | ne_s)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
s a : R
ne_a : a ≠ 0
hs_1 : 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:
simpa using IsSumNonzeroSq.sq ne_a

Premises used: IsSumNonzeroSq.sq
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
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
ne_s : s ≠ 0
⊢ IsSumNonzeroSq (a * a + s)

Tactic:
IsSumNonzeroSq.sq_add ne_a (ih ne_s)

Premises used: IsSumNonzeroSq.sq_add
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
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
ne_s : s ≠ 0
⊢ IsSumNonzeroSq (a * a + s)

Tactic:
exact IsSumNonzeroSq.sq_add ne_a (ih ne_s)

Premises used: IsSumNonzeroSq.sq_add
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
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
sq_add :
  ∀ (a : R) {s : R} (hs : IsSumSq s) (ih : ∀ (hs : s ≠ 0), IsSumNonzeroSq s) (hs : a * a + s ≠ 0),
    IsSumNonzeroSq (a * a + s)
⊢ IsSumNonzeroSq 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)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
Goal:
R : Type u_1
inst : AddMonoid R
inst_1 : Mul R
s : R
⊢ Membership.mem (γ := AddSubsemigroup R) (sumNonzeroSq R) s ↔ IsSumNonzeroSq s

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
Goal:
R : Type u_1
inst : AddMonoid R
inst_1 : Mul R
x : R
hx : Membership.mem (γ := Set R) {x : R | ∃ (x_1 : R), x_1 ≠ 0 ∧ x_1 * x_1 = x} x
⊢ x ∈ (↑(sumNonzeroSq R) : Set R)

Tactic:
aesop
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
Goal:
R : Type u_1
inst : AddMonoid R
inst_1 : Mul R
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
⊢ Eq (α := AddSubsemigroup R) (closure {x : R | ∃ (x_1 : R), x_1 ≠ 0 ∧ x_1 * x_1 = x}) (sumNonzeroSq R)

Tactic:
refine closure_eq_of_le (fun x hx ↦ by aesop) (fun x hx ↦ ?_)

Premises used: AddSubsemigroup.closure_eq_of_le
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
Goal:
R : Type u_1
inst : AddMonoid R
inst_1 : Mul R
x 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:
aesop
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
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
sq_add : Membership.mem (γ := AddSubsemigroup R) (closure {x : R | ∃ (x_1 : R), x_1 ≠ 0 ∧ x_1 * x_1 = x}) (a * a)
sq_add₁ : 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:
apply add_mem

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
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
sq_add : Membership.mem (γ := Set R) {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}) (a * a)

Tactic:
apply AddSubsemigroup.mem_closure_of_mem

Premises used: AddSubsemigroup.mem_closure_of_mem
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
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 (γ := Set R) {x : R | ∃ (x_1 : R), x_1 ≠ 0 ∧ x_1 * x_1 = x} (a * a)

Tactic:
aesop
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
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}) s

Tactic:
aesop
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
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)
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)
⊢ Membership.mem (γ := AddSubsemigroup R) (closure {x : R | ∃ (x_1 : R), x_1 ≠ 0 ∧ x_1 * x_1 = x}) x

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

Premises used: AddSubsemigroup.mem_closure_of_mem, sq, AddMemClass.add_mem
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
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
this : ∀ (x : R), IsSumNonzeroSq x → x ≠ 0
⊢ ¬IsSumNonzeroSq.{u_1} (R := R) 0

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
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
suffices : ∀ (x : R), IsSumNonzeroSq x → x ≠ 0
⊢ ¬IsSumNonzeroSq.{u_1} (R := R) 0

Tactic:
suffices ∀ (x : R), IsSumNonzeroSq x → x ≠ 0 by grind
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : Mul R
hz : ∀ {a : R}, a * a = 0 → a = 0
ha_1 : ∀ {s₁ s₂ : R}, IsSumSq s₁ → IsSumSq s₂ → s₁ + s₂ = 0 → s₁ = 0
x a : R
ha : a ≠ 0
⊢ a * a ≠ 0

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
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 b s : R
hb : b ≠ 0
hs : IsSumNonzeroSq s
ih : s ≠ 0
⊢ b * b + s ≠ 0

Tactic:
grind [ha (IsSumSq.mul_self b) hs.isSumSq]

Premises used: IsSumNonzeroSq.isSumSq, IsSumSq.mul_self
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
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
sq_add : ∀ {b s : R} (hb : b ≠ 0) (hs : IsSumNonzeroSq s) (ih : s ≠ 0), b * b + s ≠ 0
⊢ x ≠ 0

Tactic:
induction hx with
    | sq ha => grind
    | @sq_add b s hb hs ih => grind [ha (IsSumSq.mul_self b) hs.isSumSq]

Premises used: sq
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
h : ∀ {s a : R}, IsSumSq s → a * a + s = 0 → a = 0
this : ∀ (x : R), IsSumNonzeroSq x → x ≠ 0
⊢ ¬IsSumNonzeroSq.{u_1} (R := R) 0

Tactic:
grind
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
h : ∀ {s a : R}, IsSumSq s → a * a + s = 0 → a = 0
suffices : ∀ (x : R), IsSumNonzeroSq x → x ≠ 0
⊢ ¬IsSumNonzeroSq.{u_1} (R := R) 0

Tactic:
suffices ∀ (x : R), IsSumNonzeroSq x → x ≠ 0 by grind
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
h : ∀ {s a : R}, IsSumSq s → a * a + s = 0 → a = 0
x a : R
ha : a ≠ 0
hc : a * a = 0
⊢ a * a + 0 = 0

Tactic:
simpa using hc
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
h : ∀ {s a : R}, IsSumSq s → a * a + s = 0 → a = 0
x a : R
ha : a ≠ 0
⊢ a * a ≠ 0

Tactic:
exact fun hc ↦ ha (h IsSumSq.zero (by simpa using hc))

Premises used: IsSumSq.zero
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
h : ∀ {s a : R}, IsSumSq s → a * a + s = 0 → a = 0
x a s : R
ha : a ≠ 0
hs : IsSumNonzeroSq s
ih : s ≠ 0
⊢ a * a + s ≠ 0

Tactic:
grind [hs.isSumSq]

Premises used: IsSumNonzeroSq.isSumSq
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
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
sq_add : ∀ {a s : R} (ha : a ≠ 0) (hs : IsSumNonzeroSq s) (ih : s ≠ 0), a * a + s ≠ 0
⊢ x ≠ 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]

Premises used: sq
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
⊢ IsFormallyReal R

Tactic:
of_eq_zero_of_mul_self_of_eq_zero_of_add mul_self_eq_zero.mp <|
    fun hs₁ hs₂ h ↦ ((add_eq_zero_iff_of_nonneg (IsSumSq.nonneg hs₁) (IsSumSq.nonneg hs₂)).mp h).1

Premises used: mul_self_eq_zero, add_eq_zero_iff_of_nonneg, IsFormallyReal.of_eq_zero_of_mul_self_of_eq_zero_of_add, And.left, Iff.mp, IsSumSq.nonneg
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsFormallyReal R
⊢ LT.lt (α := ℕ) 1 2

Tactic:
lia
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsFormallyReal R
rw : ∀ (x : R), HPow.hPow (β := ℕ) x 2 = 0 → x = 0
⊢ IsReduced R

Tactic:
rw [isReduced_iff_pow_one_lt 2 (by lia)]

Premises used: isReduced_iff_pow_one_lt, OfNat.ofNat
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsFormallyReal R
x : R
hx : HPow.hPow (β := ℕ) x 2 = 0
by_contra! : ∀ (hc : x ≠ 0), False
⊢ x = 0

Tactic:
by_contra! hc
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsFormallyReal R
x : R
hx : HPow.hPow (β := ℕ) x 2 = 0
hc : x ≠ 0
⊢ IsSumNonzeroSq.{u_1} (R := R) 0

Tactic:
simpa [← pow_two, hx] using IsSumNonzeroSq.sq hc

Premises used: pow_two, IsSumNonzeroSq.sq
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsFormallyReal R
x : R
hx : HPow.hPow (β := ℕ) x 2 = 0
hc : x ≠ 0
⊢ False

Tactic:
exact not_isSumNonzeroSq_zero <| by simpa [← pow_two, hx] using IsSumNonzeroSq.sq hc

Premises used: IsFormallyReal.not_isSumNonzeroSq_zero
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
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
by_contra! : ∀ (h₁ : s₁ ≠ 0), False
⊢ s₁ = 0

Tactic:
by_contra! h₁
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
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
hc : s₂ = 0
⊢ False

Tactic:
simp_all
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
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
⊢ s₂ ≠ 0

Tactic:
have h₂ : s₂ ≠ 0 := fun hc ↦ by simp_all
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
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
⊢ IsSumNonzeroSq s₁

Tactic:
rw [← isSumNonzeroSq_iff_isSumSq h₁] at hs₁

Premises used: isSumNonzeroSq_iff_isSumSq
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
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
hs₃ : IsSumNonzeroSq s₁
⊢ IsSumSq s₂

Tactic:
rw [← isSumNonzeroSq_iff_isSumSq h₁] at hs₁

Premises used: isSumNonzeroSq_iff_isSumSq
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
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
hs₃ : IsSumNonzeroSq s₁
hs₄ : IsSumSq s₂
⊢ s₁ + s₂ = 0

Tactic:
rw [← isSumNonzeroSq_iff_isSumSq h₁] at hs₁

Premises used: isSumNonzeroSq_iff_isSumSq
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
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
hs₃ : IsSumNonzeroSq s₁
hs₄ : IsSumSq s₂
h₃ : s₁ + s₂ = 0
⊢ s₁ ≠ 0

Tactic:
rw [← isSumNonzeroSq_iff_isSumSq h₁] at hs₁

Premises used: isSumNonzeroSq_iff_isSumSq
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
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
hs₃ : IsSumNonzeroSq s₁
hs₄ : IsSumSq s₂
h₃ : s₁ + s₂ = 0
h₄ : s₁ ≠ 0
⊢ s₂ ≠ 0

Tactic:
rw [← isSumNonzeroSq_iff_isSumSq h₁] at hs₁

Premises used: isSumNonzeroSq_iff_isSumSq
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
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
⊢ IsSumNonzeroSq s₂

Tactic:
rw [← isSumNonzeroSq_iff_isSumSq h₂] at hs₂

Premises used: isSumNonzeroSq_iff_isSumSq
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
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
hs₃ : IsSumNonzeroSq s₂
⊢ s₁ + s₂ = 0

Tactic:
rw [← isSumNonzeroSq_iff_isSumSq h₂] at hs₂

Premises used: isSumNonzeroSq_iff_isSumSq
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
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
hs₃ : IsSumNonzeroSq s₂
h₃ : s₁ + s₂ = 0
⊢ s₁ ≠ 0

Tactic:
rw [← isSumNonzeroSq_iff_isSumSq h₂] at hs₂

Premises used: isSumNonzeroSq_iff_isSumSq
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
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
hs₃ : IsSumNonzeroSq s₂
h₃ : s₁ + s₂ = 0
h₄ : s₁ ≠ 0
⊢ s₂ ≠ 0

Tactic:
rw [← isSumNonzeroSq_iff_isSumSq h₂] at hs₂

Premises used: isSumNonzeroSq_iff_isSumSq
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
inst_1 : IsFormallyReal R
s₁ s₂ : R
hs₁ : IsSumNonzeroSq s₁
hs₂ : IsSumNonzeroSq s₂
h : s₁ + s₂ = 0
h₁ : s₁ ≠ 0
h₂ : s₂ ≠ 0
⊢ False

Tactic:
not_isSumNonzeroSq_zero (h ▸ IsSumNonzeroSq.add hs₁ hs₂)

Premises used: IsFormallyReal.not_isSumNonzeroSq_zero
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
inst_1 : IsFormallyReal R
s₁ s₂ : R
hs₁ : IsSumNonzeroSq s₁
hs₂ : IsSumNonzeroSq s₂
h : s₁ + s₂ = 0
h₁ : s₁ ≠ 0
h₂ : s₂ ≠ 0
⊢ False

Tactic:
exact not_isSumNonzeroSq_zero (h ▸ IsSumNonzeroSq.add hs₁ hs₂)

Premises used: IsFormallyReal.not_isSumNonzeroSq_zero
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
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

Tactic:
simp_all [eq_zero_of_add_right hs₁ hs₂ h]

Premises used: IsFormallyReal.eq_zero_of_add_right
-- Module: Mathlib.Algebra.Ring.IsFormallyReal
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
inst_1 : IsFormallyReal R
s : R
h₁ : IsSumSq s
h₂ : IsSumSq (-s)
⊢ s + -s = 0

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.MinimalAxioms
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
rw : HAdd.hAdd (α := R) 1 1 * a + HAdd.hAdd (α := R) 1 1 * b = a + (a + b) + b
⊢ HAdd.hAdd (α := R) 1 1 * (a + b) = a + (a + b) + b

Tactic:
rw [left_distrib]
-- Module: Mathlib.Algebra.Ring.MinimalAxioms
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 + HAdd.hAdd (α := R) 1 1 * b = a + (a + b) + b

Tactic:
simp only [right_distrib, one_mul, add_assoc]
-- Module: Mathlib.Algebra.Ring.MinimalAxioms
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

Tactic:
have h₁ : (1 + 1 : R) * (a + b) = a + (a + b) + b := by
      rw [left_distrib]
      simp only [right_distrib, one_mul, add_assoc]
-- Module: Mathlib.Algebra.Ring.MinimalAxioms
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
h₁ : HAdd.hAdd (α := R) 1 1 * (a + b) = a + (a + b) + b
rw : 1 * (a + b) + 1 * (a + b) = a + (b + a) + b
⊢ HAdd.hAdd (α := R) 1 1 * (a + b) = a + (b + a) + b

Tactic:
rw [right_distrib]
-- Module: Mathlib.Algebra.Ring.MinimalAxioms
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
h₁ : HAdd.hAdd (α := R) 1 1 * (a + b) = a + (a + b) + b
⊢ 1 * (a + b) + 1 * (a + b) = a + (b + a) + b

Tactic:
simp only [left_distrib, one_mul, add_assoc]
-- Module: Mathlib.Algebra.Ring.MinimalAxioms
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
h₁ : HAdd.hAdd (α := R) 1 1 * (a + b) = a + (a + b) + b
⊢ HAdd.hAdd (α := R) 1 1 * (a + b) = a + (b + a) + b

Tactic:
have h₂ : (1 + 1 : R) * (a + b) = a + (b + a) + b := by
      rw [right_distrib]
      simp only [left_distrib, one_mul, add_assoc]