Theorem: fact1 (MIL/C02_Basics/S03_Using_Theorems_and_Lemmas.lean)

State before:
a b c d e : ℝ
⊢ a * b * 2 ≤ a ^ 2 + b ^ 2
Tactic:
have h : 0 ≤ a ^ 2 - 2 * a * b + b ^ 2
State after:
case h
a b c d e : ℝ
⊢ 0 ≤ a ^ 2 - 2 * a * b + b ^ 2

a b c d e : ℝ
h : 0 ≤ a ^ 2 - 2 * a * b + b ^ 2
⊢ a * b * 2 ≤ a ^ 2 + b ^ 2

State before:
case h
a b c d e : ℝ
⊢ 0 ≤ a ^ 2 - 2 * a * b + b ^ 2

a b c d e : ℝ
h : 0 ≤ a ^ 2 - 2 * a * b + b ^ 2
⊢ a * b * 2 ≤ a ^ 2 + b ^ 2
Tactic:
calc
  a ^ 2 - 2 * a * b + b ^ 2 = (a - b) ^ 2 := by ring
  _ ≥ 0 := by apply pow_two_nonneg
State after:
a b c d e : ℝ
h : 0 ≤ a ^ 2 - 2 * a * b + b ^ 2
⊢ a * b * 2 ≤ a ^ 2 + b ^ 2

State before:
a b c d e : ℝ
h : 0 ≤ a ^ 2 - 2 * a * b + b ^ 2
⊢ a * b * 2 ≤ a ^ 2 + b ^ 2
Tactic:
linarith
State after:
no goals

State before:
a b c d e : ℝ
⊢ a ^ 2 - 2 * a * b + b ^ 2 = (a - b) ^ 2
Tactic:
ring
State after:
no goals

State before:
a b c d e : ℝ
⊢ (a - b) ^ 2 ≥ 0
Tactic:
apply pow_two_nonneg
State after:
no goals