-- Mathlib/Data/Real/EReal.lean
lemma right_distrib_of_nonneg {a b c : EReal} (ha : 0 ≤ a) (hb : 0 ≤ b) :
    (a + b) * c = a * c + b * c

Proof state:
case inr.inr.inr.inr
a b c : EReal
ha : 0 ≤ a
hb : 0 ≤ b
a_pos : 0 < a
b_pos : 0 < b
c_pos : 0 < c
⊢ (a + b) * c = a * c + b * c

Tactic:
induction c

Result:
case inr.inr.inr.inr.h_bot
a b : EReal
ha : 0 ≤ a
hb : 0 ≤ b
a_pos : 0 < a
b_pos : 0 < b
c_pos : 0 < ⊥
⊢ (a + b) * ⊥ = a * ⊥ + b * ⊥

case inr.inr.inr.inr.h_real
a b : EReal
ha : 0 ≤ a
hb : 0 ≤ b
a_pos : 0 < a
b_pos : 0 < b
a✝ : ℝ
c_pos : 0 < ↑a✝
⊢ (a + b) * ↑a✝ = a * ↑a✝ + b * ↑a✝

case inr.inr.inr.inr.h_top
a b : EReal
ha : 0 ≤ a
hb : 0 ≤ b
a_pos : 0 < a
b_pos : 0 < b
c_pos : 0 < ⊤
⊢ (a + b) * ⊤ = a * ⊤ + b * ⊤

Proof state:
case inr.inr.inl.h_real
a b : EReal
ha : 0 ≤ a
hb : 0 ≤ b
a_pos : 0 < a
b_pos : 0 < b
a✝ : ℝ
c_neg : ↑a✝ < 0
⊢ (a + b) * ↑a✝ = a * ↑a✝ + b * ↑a✝

Tactic:
induction a

Result:
case inr.inr.inl.h_real.h_bot
b : EReal
hb : 0 ≤ b
b_pos : 0 < b
a✝ : ℝ
c_neg : ↑a✝ < 0
ha : 0 ≤ ⊥
a_pos : 0 < ⊥
⊢ (⊥ + b) * ↑a✝ = ⊥ * ↑a✝ + b * ↑a✝

case inr.inr.inl.h_real.h_real
b : EReal
hb : 0 ≤ b
b_pos : 0 < b
a✝¹ : ℝ
c_neg : ↑a✝¹ < 0
a✝ : ℝ
ha : 0 ≤ ↑a✝
a_pos : 0 < ↑a✝
⊢ (↑a✝ + b) * ↑a✝¹ = ↑a✝ * ↑a✝¹ + b * ↑a✝¹

case inr.inr.inl.h_real.h_top
b : EReal
hb : 0 ≤ b
b_pos : 0 < b
a✝ : ℝ
c_neg : ↑a✝ < 0
ha : 0 ≤ ⊤
a_pos : 0 < ⊤
⊢ (⊤ + b) * ↑a✝ = ⊤ * ↑a✝ + b * ↑a✝

Proof state:
case inr.inr.inr.inr.h_bot
a b : EReal
ha : 0 ≤ a
hb : 0 ≤ b
a_pos : 0 < a
b_pos : 0 < b
c_pos : 0 < ⊥
⊢ False

Tactic:
exact not_lt_bot c_pos

Result:
no goals

Proof state:
case inr.inr.inl.h_real.h_real.h_top
a✝¹ : ℝ
c_neg : ↑a✝¹ < 0
a✝ : ℝ
ha : 0 ≤ ↑a✝
a_pos : 0 < ↑a✝
hb : 0 ≤ ⊤
b_pos : 0 < ⊤
⊢ (↑a✝ + ⊤) * ↑a✝¹ = ↑(a✝ * a✝¹) + ⊤ * ↑a✝¹

Tactic:
rw [add_top_of_ne_bot (coe_ne_bot _), top_mul_of_neg c_neg, add_bot]

Result:
no goals

Proof state:
case inr.inr.inr.inr.h_real.h_real.h_real
a✝² : ℝ
c_pos : 0 < ↑a✝²
a✝¹ : ℝ
ha : 0 ≤ ↑a✝¹
a_pos : 0 < ↑a✝¹
a✝ : ℝ
hb : 0 ≤ ↑a✝
b_pos : 0 < ↑a✝
⊢ (a✝¹ + a✝) * a✝² = a✝¹ * a✝² + a✝ * a✝²

Tactic:
exact right_distrib _ _ _

Result:
no goals

Proof state:
case inl
b c : EReal
hb : 0 ≤ b
ha : 0 ≤ 0
⊢ (0 + b) * c = 0 * c + b * c

Tactic:
simp

Result:
no goals

Proof state:
case inr.inr.inr.inr.h_bot
a b : EReal
ha : 0 ≤ a
hb : 0 ≤ b
a_pos : 0 < a
b_pos : 0 < b
c_pos : 0 < ⊥
⊢ (a + b) * ⊥ = a * ⊥ + b * ⊥

Tactic:
exfalso

Result:
case inr.inr.inr.inr.h_bot
a b : EReal
ha : 0 ≤ a
hb : 0 ≤ b
a_pos : 0 < a
b_pos : 0 < b
c_pos : 0 < ⊥
⊢ False

Proof state:
case inr.inr.inr.inr.h_real.h_real.h_top
a✝¹ : ℝ
c_pos : 0 < ↑a✝¹
a✝ : ℝ
ha : 0 ≤ ↑a✝
a_pos : 0 < ↑a✝
hb : 0 ≤ ⊤
b_pos : 0 < ⊤
⊢ (↑a✝ + ⊤) * ↑a✝¹ = ↑(a✝ * a✝¹) + ⊤ * ↑a✝¹

Tactic:
rw [add_top_of_ne_bot (coe_ne_bot _), top_mul_of_pos c_pos,
  add_top_of_ne_bot (coe_ne_bot _)]

Result:
no goals

Proof state:
case inr.inr.inl.h_real.h_real.h_real
a✝² : ℝ
c_neg : ↑a✝² < 0
a✝¹ : ℝ
ha : 0 ≤ ↑a✝¹
a_pos : 0 < ↑a✝¹
a✝ : ℝ
hb : 0 ≤ ↑a✝
b_pos : 0 < ↑a✝
⊢ (a✝¹ + a✝) * a✝² = a✝¹ * a✝² + a✝ * a✝²

Tactic:
exact right_distrib _ _ _

Result:
no goals

Proof state:
case inr.inr.inl.h_real.h_real.h_bot
a✝¹ : ℝ
c_neg : ↑a✝¹ < 0
a✝ : ℝ
ha : 0 ≤ ↑a✝
a_pos : 0 < ↑a✝
hb : 0 ≤ ⊥
b_pos : 0 < ⊥
⊢ (↑a✝ + ⊥) * ↑a✝¹ = ↑a✝ * ↑a✝¹ + ⊥ * ↑a✝¹

Tactic:
norm_cast

Result:
no goals

Proof state:
case inr.inr.inr.inr.h_real.h_real.h_bot
a✝¹ : ℝ
c_pos : 0 < ↑a✝¹
a✝ : ℝ
ha : 0 ≤ ↑a✝
a_pos : 0 < ↑a✝
hb : 0 ≤ ⊥
b_pos : 0 < ⊥
⊢ (↑a✝ + ⊥) * ↑a✝¹ = ↑a✝ * ↑a✝¹ + ⊥ * ↑a✝¹

Tactic:
norm_cast

Result:
no goals

Proof state:
case inr.inr.inl.h_real.h_real.h_top
a✝¹ : ℝ
c_neg : ↑a✝¹ < 0
a✝ : ℝ
ha : 0 ≤ ↑a✝
a_pos : 0 < ↑a✝
hb : 0 ≤ ⊤
b_pos : 0 < ⊤
⊢ (↑a✝ + ⊤) * ↑a✝¹ = ↑a✝ * ↑a✝¹ + ⊤ * ↑a✝¹

Tactic:
norm_cast

Result:
case inr.inr.inl.h_real.h_real.h_top
a✝¹ : ℝ
c_neg : ↑a✝¹ < 0
a✝ : ℝ
ha : 0 ≤ ↑a✝
a_pos : 0 < ↑a✝
hb : 0 ≤ ⊤
b_pos : 0 < ⊤
⊢ (↑a✝ + ⊤) * ↑a✝¹ = ↑(a✝ * a✝¹) + ⊤ * ↑a✝¹

Proof state:
case inr.inr
a b c : EReal
ha : 0 ≤ a
hb : 0 ≤ b
a_pos : 0 < a
b_pos : 0 < b
⊢ (a + b) * c = a * c + b * c

Tactic:
rcases lt_trichotomy c 0 with (c_neg | rfl | c_pos)

Result:
case inr.inr.inl
a b c : EReal
ha : 0 ≤ a
hb : 0 ≤ b
a_pos : 0 < a
b_pos : 0 < b
c_neg : c < 0
⊢ (a + b) * c = a * c + b * c

case inr.inr.inr.inl
a b : EReal
ha : 0 ≤ a
hb : 0 ≤ b
a_pos : 0 < a
b_pos : 0 < b
⊢ (a + b) * 0 = a * 0 + b * 0

case inr.inr.inr.inr
a b c : EReal
ha : 0 ≤ a
hb : 0 ≤ b
a_pos : 0 < a
b_pos : 0 < b
c_pos : 0 < c
⊢ (a + b) * c = a * c + b * c

Proof state:
case inr.inr.inr.inr.h_real.h_bot
b : EReal
hb : 0 ≤ b
b_pos : 0 < b
a✝ : ℝ
c_pos : 0 < ↑a✝
ha : 0 ≤ ⊥
a_pos : 0 < ⊥
⊢ False

Tactic:
exact not_lt_bot a_pos

Result:
no goals