R : Type u
inst✝ : LinearOrder R
a b : Tropical (WithTop R)
⊢ a = 0 ∧ a ≤ b ∨ b = 0 ∧ b ≤ a ↔ a = 0 ∧ b = 0
R : Type u
inst✝ : LinearOrder R
a b : Tropical (WithTop R)
⊢ a + b = 0 ↔ a = 0 ∧ b = 0
rw [add_eq_iff]
case mp
R : Type u
inst✝ : LinearOrder R
a b : Tropical (WithTop R)
⊢ a = 0 ∧ a ≤ b ∨ b = 0 ∧ b ≤ a → a = 0 ∧ b = 0

case mpr
R : Type u
inst✝ : LinearOrder R
a b : Tropical (WithTop R)
⊢ a = 0 ∧ b = 0 → a = 0 ∧ a ≤ b ∨ b = 0 ∧ b ≤ a
R : Type u
inst✝ : LinearOrder R
a b : Tropical (WithTop R)
⊢ a = 0 ∧ a ≤ b ∨ b = 0 ∧ b ≤ a ↔ a = 0 ∧ b = 0
constructor
case mp.inl.intro
R : Type u
inst✝ : LinearOrder R
b : Tropical (WithTop R)
h : 0 ≤ b
⊢ 0 = 0 ∧ b = 0

case mp.inr.intro
R : Type u
inst✝ : LinearOrder R
a : Tropical (WithTop R)
h : 0 ≤ a
⊢ a = 0 ∧ 0 = 0
case mp
R : Type u
inst✝ : LinearOrder R
a b : Tropical (WithTop R)
⊢ a = 0 ∧ a ≤ b ∨ b = 0 ∧ b ≤ a → a = 0 ∧ b = 0
rintro (⟨rfl, h⟩ | ⟨rfl, h⟩)
no goals
case mp.inl.intro
R : Type u
inst✝ : LinearOrder R
b : Tropical (WithTop R)
h : 0 ≤ b
⊢ 0 = 0 ∧ b = 0
exact ⟨rfl, le_antisymm (le_zero _) h⟩
no goals
case mp.inr.intro
R : Type u
inst✝ : LinearOrder R
a : Tropical (WithTop R)
h : 0 ≤ a
⊢ a = 0 ∧ 0 = 0
exact ⟨le_antisymm (le_zero _) h, rfl⟩
case mpr.intro
R : Type u
inst✝ : LinearOrder R
⊢ 0 = 0 ∧ 0 ≤ 0 ∨ 0 = 0 ∧ 0 ≤ 0
case mpr
R : Type u
inst✝ : LinearOrder R
a b : Tropical (WithTop R)
⊢ a = 0 ∧ b = 0 → a = 0 ∧ a ≤ b ∨ b = 0 ∧ b ≤ a
rintro ⟨rfl, rfl⟩
no goals
case mpr.intro
R : Type u
inst✝ : LinearOrder R
⊢ 0 = 0 ∧ 0 ≤ 0 ∨ 0 = 0 ∧ 0 ≤ 0
simp