Theorem: Usa2023P2.lemma_3 (Compfiles/Usa2023P2.lean)

State before:
a b c : ℝ+
h : a = b + c
⊢ c < a
Tactic:
rw [h]
State after:
a b c : ℝ+
h : a = b + c
⊢ c < b + c

State before:
a b c : ℝ+
h : a = b + c
⊢ c < b + c
Tactic:
obtain ⟨b, hb⟩ := b
State after:
case mk
a c : ℝ+
b : ℝ
hb : 0 < b
h : a = ⟨b, hb⟩ + c
⊢ c < ⟨b, hb⟩ + c

State before:
case mk
a c : ℝ+
b : ℝ
hb : 0 < b
h : a = ⟨b, hb⟩ + c
⊢ c < ⟨b, hb⟩ + c
Tactic:
obtain ⟨c, hc⟩ := c
State after:
case mk.mk
a : ℝ+
b : ℝ
hb : 0 < b
c : ℝ
hc : 0 < c
h : a = ⟨b, hb⟩ + ⟨c, hc⟩
⊢ ⟨c, hc⟩ < ⟨b, hb⟩ + ⟨c, hc⟩

State before:
case mk.mk
a : ℝ+
b : ℝ
hb : 0 < b
c : ℝ
hc : 0 < c
h : a = ⟨b, hb⟩ + ⟨c, hc⟩
⊢ ⟨c, hc⟩ < ⟨b, hb⟩ + ⟨c, hc⟩
Tactic:
rw [←Subtype.coe_lt_coe, Positive.coe_add]
State after:
case mk.mk
a : ℝ+
b : ℝ
hb : 0 < b
c : ℝ
hc : 0 < c
h : a = ⟨b, hb⟩ + ⟨c, hc⟩
⊢ ↑⟨c, hc⟩ < ↑⟨b, hb⟩ + ↑⟨c, hc⟩

State before:
case mk.mk
a : ℝ+
b : ℝ
hb : 0 < b
c : ℝ
hc : 0 < c
h : a = ⟨b, hb⟩ + ⟨c, hc⟩
⊢ ↑⟨c, hc⟩ < ↑⟨b, hb⟩ + ↑⟨c, hc⟩
Tactic:
exact lt_add_of_pos_left c hb
State after:
no goals