-- Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
lemma sq_nonneg [IsRightCancelAdd α]
    [ZeroLEOneClass α] [ExistsAddOfLE α] [PosMulMono α] [AddLeftStrictMono α]
    (a : α) : 0 ≤ a ^ 2

Proof state:
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsRightCancelAdd α
inst✝³ : ZeroLEOneClass α
inst✝² : ExistsAddOfLE α
inst✝¹ : PosMulMono α
inst✝ : AddLeftStrictMono α
a : α
ha : a ≤ 0
b : α
hab : 0 = a + b
⊢ (a + b) * b = a * (a + b)

Tactic:
simp [← hab]

Result:
no goals

Proof state:
case inr.intro
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsRightCancelAdd α
inst✝³ : ZeroLEOneClass α
inst✝² : ExistsAddOfLE α
inst✝¹ : PosMulMono α
inst✝ : AddLeftStrictMono α
a : α
ha : a ≤ 0
b : α
hab : 0 = a + b
⊢ 0 ≤ a ^ 2

Tactic:
calc
  0 ≤ b ^ 2 := pow_nonneg (not_lt.1 fun hb ↦ hab.not_gt <| add_neg_of_nonpos_of_neg ha hb) _
  _ = a ^ 2 := add_left_injective (a * b) ?_

Result:
case inr.intro
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsRightCancelAdd α
inst✝³ : ZeroLEOneClass α
inst✝² : ExistsAddOfLE α
inst✝¹ : PosMulMono α
inst✝ : AddLeftStrictMono α
a : α
ha : a ≤ 0
b : α
hab : 0 = a + b
⊢ (fun x => x + a * b) (b ^ 2) = (fun x => x + a * b) (a ^ 2)

Proof state:
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsRightCancelAdd α
inst✝³ : ZeroLEOneClass α
inst✝² : ExistsAddOfLE α
inst✝¹ : PosMulMono α
inst✝ : AddLeftStrictMono α
a : α
ha : a ≤ 0
b : α
hab : 0 = a + b
⊢ b ^ 2 + a * b = (a + b) * b

Tactic:
rw [add_comm, sq, add_mul]

Result:
no goals

Proof state:
case inl
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsRightCancelAdd α
inst✝³ : ZeroLEOneClass α
inst✝² : ExistsAddOfLE α
inst✝¹ : PosMulMono α
inst✝ : AddLeftStrictMono α
a : α
ha : 0 ≤ a
⊢ 0 ≤ a ^ 2

Tactic:
exact pow_nonneg ha _

Result:
no goals

Proof state:
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsRightCancelAdd α
inst✝³ : ZeroLEOneClass α
inst✝² : ExistsAddOfLE α
inst✝¹ : PosMulMono α
inst✝ : AddLeftStrictMono α
a : α
⊢ 0 ≤ a ^ 2

Tactic:
obtain ha | ha := le_total 0 a

Result:
case inl
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsRightCancelAdd α
inst✝³ : ZeroLEOneClass α
inst✝² : ExistsAddOfLE α
inst✝¹ : PosMulMono α
inst✝ : AddLeftStrictMono α
a : α
ha : 0 ≤ a
⊢ 0 ≤ a ^ 2

case inr
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsRightCancelAdd α
inst✝³ : ZeroLEOneClass α
inst✝² : ExistsAddOfLE α
inst✝¹ : PosMulMono α
inst✝ : AddLeftStrictMono α
a : α
ha : a ≤ 0
⊢ 0 ≤ a ^ 2

Proof state:
case inr
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsRightCancelAdd α
inst✝³ : ZeroLEOneClass α
inst✝² : ExistsAddOfLE α
inst✝¹ : PosMulMono α
inst✝ : AddLeftStrictMono α
a : α
ha : a ≤ 0
⊢ 0 ≤ a ^ 2

Tactic:
obtain ⟨b, hab⟩ := exists_add_of_le ha

Result:
case inr.intro
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsRightCancelAdd α
inst✝³ : ZeroLEOneClass α
inst✝² : ExistsAddOfLE α
inst✝¹ : PosMulMono α
inst✝ : AddLeftStrictMono α
a : α
ha : a ≤ 0
b : α
hab : 0 = a + b
⊢ 0 ≤ a ^ 2

Proof state:
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsRightCancelAdd α
inst✝³ : ZeroLEOneClass α
inst✝² : ExistsAddOfLE α
inst✝¹ : PosMulMono α
inst✝ : AddLeftStrictMono α
a : α
ha : a ≤ 0
b : α
hab : 0 = a + b
⊢ a * (a + b) = a ^ 2 + a * b

Tactic:
rw [sq, mul_add]

Result:
no goals

Proof state:
case inr.intro
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsRightCancelAdd α
inst✝³ : ZeroLEOneClass α
inst✝² : ExistsAddOfLE α
inst✝¹ : PosMulMono α
inst✝ : AddLeftStrictMono α
a : α
ha : a ≤ 0
b : α
hab : 0 = a + b
⊢ (fun x => x + a * b) (b ^ 2) = (fun x => x + a * b) (a ^ 2)

Tactic:
calc
  b ^ 2 + a * b = (a + b) * b := by rw [add_comm, sq, add_mul]
  _ = a * (a + b) := by simp [← hab]
  _ = a ^ 2 + a * b := by rw [sq, mul_add]

Result:
no goals