-- 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.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:
norm_cast

Result:
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✝²

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

Tactic:
rw [mul_bot_of_pos a_pos, mul_bot_of_pos b_pos, mul_bot_of_pos (add_pos a_pos b_pos),
  add_bot ⊥]

Result:
no goals

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 < ⊥
⊢ (⊥ + b) * ↑a✝ = ⊥ * ↑a✝ + b * ↑a✝

Tactic:
exfalso

Result:
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

Proof state:
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

Tactic:
induction c

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

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✝

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

Proof state:
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✝

Tactic:
rw [top_add_of_ne_bot (ne_bot_of_gt b_pos), top_mul_of_neg c_neg, bot_add]

Result:
no goals

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

Tactic:
rcases eq_or_lt_of_le ha with (rfl | a_pos)

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

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

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

Tactic:
induction b

Result:
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✝¹

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✝²

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✝¹

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

Tactic:
rw [top_add_of_ne_bot (ne_bot_of_gt b_pos), top_mul_of_pos c_pos,
  top_add_of_ne_bot (ne_bot_of_gt (mul_pos b_pos c_pos))]

Result:
no goals

Proof state:
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✝¹

Tactic:
induction b

Result:
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✝¹

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✝²

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.inl.h_real.h_bot
b : EReal
hb : 0 ≤ b
b_pos : 0 < b
a✝ : ℝ
c_neg : ↑a✝ < 0
ha : 0 ≤ ⊥
a_pos : 0 < ⊥
⊢ False

Tactic:
exact not_lt_bot a_pos

Result:
no goals

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

Tactic:
simp

Result:
no goals

Proof state:
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 * ⊤

Tactic:
rw [mul_top_of_pos a_pos, mul_top_of_pos b_pos, mul_top_of_pos (add_pos a_pos b_pos),
  top_add_top]

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:
norm_cast

Result:
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✝²

Proof state:
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✝

Tactic:
induction a

Result:
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 < ⊥
⊢ (⊥ + b) * ↑a✝ = ⊥ * ↑a✝ + b * ↑a✝

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

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

Proof state:
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

Tactic:
simp

Result:
no goals

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

Tactic:
exfalso

Result:
case inr.inr.inl.h_top
a b : EReal
ha : 0 ≤ a
hb : 0 ≤ b
a_pos : 0 < a
b_pos : 0 < b
c_neg : ⊤ < 0
⊢ False

Proof state:
case inr.inr.inl.h_top
a b : EReal
ha : 0 ≤ a
hb : 0 ≤ b
a_pos : 0 < a
b_pos : 0 < b
c_neg : ⊤ < 0
⊢ False

Tactic:
exact not_top_lt c_neg

Result:
no goals

Proof state:
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✝

Tactic:
exfalso

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 < ⊥
⊢ 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:
norm_cast

Result:
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✝¹

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

Tactic:
rcases eq_or_lt_of_le hb with (rfl | b_pos)

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

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