[GOAL]
R : Type u
inst✝ : LinearOrder R
src✝ : PartialOrder (Tropical R) := instPartialOrderTropical
a b : Tropical R
⊢ untrop (min a b) = untrop (if a ≤ b then a else b)
[PROOFSTEP]
simp [min_def]
[GOAL]
R : Type u
inst✝ : LinearOrder R
src✝ : PartialOrder (Tropical R) := instPartialOrderTropical
a b : Tropical R
⊢ (if a ≤ b then untrop a else untrop b) = untrop (if a ≤ b then a else b)
[PROOFSTEP]
split_ifs
[GOAL]
case pos
R : Type u
inst✝ : LinearOrder R
src✝ : PartialOrder (Tropical R) := instPartialOrderTropical
a b : Tropical R
h✝ : a ≤ b
⊢ untrop a = untrop a
[PROOFSTEP]
simp
[GOAL]
case neg
R : Type u
inst✝ : LinearOrder R
src✝ : PartialOrder (Tropical R) := instPartialOrderTropical
a b : Tropical R
h✝ : ¬a ≤ b
⊢ untrop b = untrop b
[PROOFSTEP]
simp
[GOAL]
R : Type u
inst✝ : LinearOrder R
src✝ : PartialOrder (Tropical R) := instPartialOrderTropical
a b : Tropical R
⊢ untrop (max a b) = untrop (if a ≤ b then b else a)
[PROOFSTEP]
simp [max_def]
[GOAL]
R : Type u
inst✝ : LinearOrder R
src✝ : PartialOrder (Tropical R) := instPartialOrderTropical
a b : Tropical R
⊢ (if a ≤ b then untrop b else untrop a) = untrop (if a ≤ b then b else a)
[PROOFSTEP]
split_ifs
[GOAL]
case pos
R : Type u
inst✝ : LinearOrder R
src✝ : PartialOrder (Tropical R) := instPartialOrderTropical
a b : Tropical R
h✝ : a ≤ b
⊢ untrop b = untrop b
[PROOFSTEP]
simp
[GOAL]
case neg
R : Type u
inst✝ : LinearOrder R
src✝ : PartialOrder (Tropical R) := instPartialOrderTropical
a b : Tropical R
h✝ : ¬a ≤ b
⊢ untrop a = untrop a
[PROOFSTEP]
simp
[GOAL]
R : Type u
inst✝ : LinearOrder R
x y : Tropical R
h : x ≤ y
⊢ untrop (x + y) = untrop x
[PROOFSTEP]
simpa using h
[GOAL]
R : Type u
inst✝ : LinearOrder R
x y : Tropical R
h : y ≤ x
⊢ untrop (x + y) = untrop y
[PROOFSTEP]
simpa using h
[GOAL]
R : Type u
inst✝ : LinearOrder R
x y : Tropical R
⊢ x + y = x ↔ x ≤ y
[PROOFSTEP]
rw [trop_add_def, trop_eq_iff_eq_untrop, ← untrop_le_iff, min_eq_left_iff]
[GOAL]
R : Type u
inst✝ : LinearOrder R
x y : Tropical R
⊢ x + y = y ↔ y ≤ x
[PROOFSTEP]
rw [trop_add_def, trop_eq_iff_eq_untrop, ← untrop_le_iff, min_eq_right_iff]
[GOAL]
R : Type u
inst✝ : LinearOrder R
x y z : Tropical R
⊢ x + y = z ↔ x = z ∧ x ≤ y ∨ y = z ∧ y ≤ x
[PROOFSTEP]
rw [trop_add_def, trop_eq_iff_eq_untrop]
[GOAL]
R : Type u
inst✝ : LinearOrder R
x y z : Tropical R
⊢ min (untrop x) (untrop y) = untrop z ↔ x = z ∧ x ≤ y ∨ y = z ∧ y ≤ x
[PROOFSTEP]
simp [min_eq_iff]
[GOAL]
R : Type u
inst✝ : LinearOrder R
a b : Tropical (WithTop R)
⊢ a + b = 0 ↔ a = 0 ∧ b = 0
[PROOFSTEP]
rw [add_eq_iff]
[GOAL]
R : Type u
inst✝ : LinearOrder R
a b : Tropical (WithTop R)
⊢ a = 0 ∧ a ≤ b ∨ b = 0 ∧ b ≤ a ↔ a = 0 ∧ b = 0
[PROOFSTEP]
constructor
[GOAL]
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
[PROOFSTEP]
rintro (⟨rfl, h⟩ | ⟨rfl, h⟩)
[GOAL]
case mp.inl.intro
R : Type u
inst✝ : LinearOrder R
b : Tropical (WithTop R)
h : 0 ≤ b
⊢ 0 = 0 ∧ b = 0
[PROOFSTEP]
exact ⟨rfl, le_antisymm (le_zero _) h⟩
[GOAL]
case mp.inr.intro
R : Type u
inst✝ : LinearOrder R
a : Tropical (WithTop R)
h : 0 ≤ a
⊢ a = 0 ∧ 0 = 0
[PROOFSTEP]
exact ⟨le_antisymm (le_zero _) h, rfl⟩
[GOAL]
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
[PROOFSTEP]
rintro ⟨rfl, rfl⟩
[GOAL]
case mpr.intro
R : Type u
inst✝ : LinearOrder R
⊢ 0 = 0 ∧ 0 ≤ 0 ∨ 0 = 0 ∧ 0 ≤ 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
inst✝² : LinearOrder R
inst✝¹ : OrderTop R
inst✝ : Zero R
src✝¹ : One (Tropical R) := instOneTropical
src✝ : AddCommMonoid (Tropical R) := instAddCommMonoidTropical
n : ℕ
⊢ untrop (NatCast.natCast (n + 1)) = untrop (NatCast.natCast n + 1)
[PROOFSTEP]
cases n
[GOAL]
case zero
R : Type u
inst✝² : LinearOrder R
inst✝¹ : OrderTop R
inst✝ : Zero R
src✝¹ : One (Tropical R) := instOneTropical
src✝ : AddCommMonoid (Tropical R) := instAddCommMonoidTropical
⊢ untrop (NatCast.natCast (Nat.zero + 1)) = untrop (NatCast.natCast Nat.zero + 1)
[PROOFSTEP]
simp [Nat.cast]
[GOAL]
case succ
R : Type u
inst✝² : LinearOrder R
inst✝¹ : OrderTop R
inst✝ : Zero R
src✝¹ : One (Tropical R) := instOneTropical
src✝ : AddCommMonoid (Tropical R) := instAddCommMonoidTropical
n✝ : ℕ
⊢ untrop (NatCast.natCast (Nat.succ n✝ + 1)) = untrop (NatCast.natCast (Nat.succ n✝) + 1)
[PROOFSTEP]
simp [Nat.cast]
[GOAL]
R : Type u
inst✝ : AddMonoid R
src✝¹ : MulOneClass (Tropical R) := instMulOneClassTropical
src✝ : Semigroup (Tropical R) := instSemigroupTropical
x✝ : Tropical R
⊢ untrop ((fun n x => x ^ n) 0 x✝) = untrop 1
[PROOFSTEP]
simp
[GOAL]
R : Type u
inst✝ : AddGroup R
src✝ : Monoid (Tropical R) := instMonoidTropical
x✝¹ x✝ : Tropical R
⊢ untrop (x✝¹ / x✝) = untrop (x✝¹ * x✝⁻¹)
[PROOFSTEP]
simp [sub_eq_add_neg]
[GOAL]
R : Type u
inst✝ : LinearOrder R
x y z : Tropical R
h : y ≤ z
⊢ x + y ≤ x + z
[PROOFSTEP]
cases' le_total x y with hx hy
[GOAL]
case inl
R : Type u
inst✝ : LinearOrder R
x y z : Tropical R
h : y ≤ z
hx : x ≤ y
⊢ x + y ≤ x + z
[PROOFSTEP]
rw [add_eq_left hx, add_eq_left (hx.trans h)]
[GOAL]
case inr
R : Type u
inst✝ : LinearOrder R
x y z : Tropical R
h : y ≤ z
hy : y ≤ x
⊢ x + y ≤ x + z
[PROOFSTEP]
rw [add_eq_right hy]
[GOAL]
case inr
R : Type u
inst✝ : LinearOrder R
x y z : Tropical R
h : y ≤ z
hy : y ≤ x
⊢ y ≤ x + z
[PROOFSTEP]
cases' le_total x z with hx hx
[GOAL]
case inr.inl
R : Type u
inst✝ : LinearOrder R
x y z : Tropical R
h : y ≤ z
hy : y ≤ x
hx : x ≤ z
⊢ y ≤ x + z
[PROOFSTEP]
rwa [add_eq_left hx]
[GOAL]
case inr.inr
R : Type u
inst✝ : LinearOrder R
x y z : Tropical R
h : y ≤ z
hy : y ≤ x
hx : z ≤ x
⊢ y ≤ x + z
[PROOFSTEP]
rwa [add_eq_right hx]
[GOAL]
R : Type u
inst✝³ : LinearOrder R
inst✝² : AddMonoid R
inst✝¹ : CovariantClass R R (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass R R (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
x y : Tropical R
n : ℕ
⊢ (x + y) ^ n = x ^ n + y ^ n
[PROOFSTEP]
cases' le_total x y with h h
[GOAL]
case inl
R : Type u
inst✝³ : LinearOrder R
inst✝² : AddMonoid R
inst✝¹ : CovariantClass R R (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass R R (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
x y : Tropical R
n : ℕ
h : x ≤ y
⊢ (x + y) ^ n = x ^ n + y ^ n
[PROOFSTEP]
rw [add_eq_left h, add_eq_left (pow_le_pow_of_le_left' h _)]
[GOAL]
case inr
R : Type u
inst✝³ : LinearOrder R
inst✝² : AddMonoid R
inst✝¹ : CovariantClass R R (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass R R (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
x y : Tropical R
n : ℕ
h : y ≤ x
⊢ (x + y) ^ n = x ^ n + y ^ n
[PROOFSTEP]
rw [add_eq_right h, add_eq_right (pow_le_pow_of_le_left' h _)]
[GOAL]
R : Type u
inst✝ : LinearOrderedAddCommMonoidWithTop R
src✝³ : AddMonoidWithOne (Tropical R) := instAddMonoidWithOneTropical
src✝² : Distrib (Tropical R) := instDistribTropical
src✝¹ : AddCommMonoid (Tropical R) := instAddCommMonoidTropical
src✝ : CommMonoid (Tropical R) := instCommMonoidTropical
x✝ : Tropical R
⊢ untrop (0 * x✝) = untrop 0
[PROOFSTEP]
simp [top_add]
[GOAL]
R : Type u
inst✝ : LinearOrderedAddCommMonoidWithTop R
src✝³ : AddMonoidWithOne (Tropical R) := instAddMonoidWithOneTropical
src✝² : Distrib (Tropical R) := instDistribTropical
src✝¹ : AddCommMonoid (Tropical R) := instAddCommMonoidTropical
src✝ : CommMonoid (Tropical R) := instCommMonoidTropical
x✝ : Tropical R
⊢ untrop (x✝ * 0) = untrop 0
[PROOFSTEP]
simp [add_top]
[GOAL]
R✝ : Type u
inst✝² : LinearOrderedAddCommMonoidWithTop R✝
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
x : Tropical R
n : ℕ
⊢ (n + 1) • x = x
[PROOFSTEP]
induction' n with n IH
[GOAL]
case zero
R✝ : Type u
inst✝² : LinearOrderedAddCommMonoidWithTop R✝
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
x : Tropical R
⊢ (Nat.zero + 1) • x = x
[PROOFSTEP]
simp
[GOAL]
case succ
R✝ : Type u
inst✝² : LinearOrderedAddCommMonoidWithTop R✝
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
x : Tropical R
n : ℕ
IH : (n + 1) • x = x
⊢ (Nat.succ n + 1) • x = x
[PROOFSTEP]
rw [add_nsmul, IH, one_nsmul, add_self]
[GOAL]
R✝ : Type u
inst✝¹ : LinearOrderedAddCommMonoidWithTop R✝
R : Type u_1
inst✝ : LinearOrderedAddCommMonoid R
a b : Tropical (WithTop R)
⊢ a * b = 0 ↔ a = 0 ∨ b = 0
[PROOFSTEP]
simp [← untrop_inj_iff, WithTop.add_eq_top]
