awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LinearOrder R
x y : Tropical R
rw : trop (min (untrop x) (untrop y)) = x ↔ x ≤ y
rw₁ : min (untrop x) (untrop y) = untrop x ↔ x ≤ y
rw₂ : min (untrop x) (untrop y) = untrop x ↔ untrop x ≤ untrop y
rw₃ rw₄ : untrop x ≤ untrop y ↔ untrop x ≤ untrop y
⊢ x + y = x ↔ x ≤ y

Tactic:
rw [trop_add_def, trop_eq_iff_eq_untrop, ← untrop_le_iff, min_eq_left_iff]

Premises used: Tropical.trop_add_def, Tropical.trop_eq_iff_eq_untrop, Tropical.untrop_le_iff, min_eq_left_iff
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LinearOrder R
x y : Tropical R
rw : trop (min (untrop x) (untrop y)) = y ↔ y ≤ x
rw₁ : min (untrop x) (untrop y) = untrop y ↔ y ≤ x
rw₂ : min (untrop x) (untrop y) = untrop y ↔ untrop y ≤ untrop x
rw₃ rw₄ : untrop y ≤ untrop x ↔ untrop y ≤ untrop x
⊢ x + y = y ↔ y ≤ x

Tactic:
rw [trop_add_def, trop_eq_iff_eq_untrop, ← untrop_le_iff, min_eq_right_iff]

Premises used: min_eq_right_iff, Tropical.trop_add_def, Tropical.trop_eq_iff_eq_untrop, Tropical.untrop_le_iff
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LinearOrder R
x : Tropical R
⊢ x + x = x

Tactic:
untrop_injective (min_eq_right le_rfl)

Premises used: le_rfl, min_eq_right, Tropical.untrop_injective
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LinearOrder R
x y z : Tropical R
rw : min (untrop x) (untrop y) = untrop z ↔ x = z ∧ x ≤ y ∨ y = z ∧ y ≤ x
⊢ x + y = z ↔ x = z ∧ x ≤ y ∨ y = z ∧ y ≤ x

Tactic:
rw [trop_add_def, trop_eq_iff_eq_untrop]

Premises used: Tropical.trop_add_def, Tropical.trop_eq_iff_eq_untrop
-- Module: Mathlib.Algebra.Tropical.Basic
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

Tactic:
simp [min_eq_iff]

Premises used: min_eq_iff
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LinearOrder R
a b : Tropical (WithTop R)
rw : a = 0 ∧ a ≤ b ∨ b = 0 ∧ b ≤ a ↔ a = 0 ∧ b = 0
⊢ a + b = 0 ↔ a = 0 ∧ b = 0

Tactic:
rw [add_eq_iff]

Premises used: Tropical.add_eq_iff
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LinearOrder R
a b : Tropical (WithTop R)
mp : a = 0 ∧ a ≤ b ∨ b = 0 ∧ b ≤ a → a = 0 ∧ b = 0
mpr : a = 0 ∧ b = 0 → a = 0 ∧ a ≤ b ∨ b = 0 ∧ b ≤ a
⊢ a = 0 ∧ a ≤ b ∨ b = 0 ∧ b ≤ a ↔ a = 0 ∧ b = 0

Tactic:
constructor
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LinearOrder R
b : Tropical (WithTop R)
h : 0 ≤ b
⊢ Eq.{u + 1} (α := Tropical (WithTop R)) 0 0 ∧ b = 0

Tactic:
⟨rfl, le_antisymm (le_zero _) h⟩

Premises used: Tropical.le_zero, le_antisymm, And.intro, rfl
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LinearOrder R
b : Tropical (WithTop R)
h : 0 ≤ b
⊢ Eq.{u + 1} (α := Tropical (WithTop R)) 0 0 ∧ b = 0

Tactic:
exact ⟨rfl, le_antisymm (le_zero _) h⟩
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LinearOrder R
a : Tropical (WithTop R)
h : 0 ≤ a
⊢ a = 0 ∧ Eq.{u + 1} (α := Tropical (WithTop R)) 0 0

Tactic:
⟨le_antisymm (le_zero _) h, rfl⟩

Premises used: Tropical.le_zero, le_antisymm, And.intro, rfl
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LinearOrder R
a : Tropical (WithTop R)
h : 0 ≤ a
⊢ a = 0 ∧ Eq.{u + 1} (α := Tropical (WithTop R)) 0 0

Tactic:
exact ⟨le_antisymm (le_zero _) h, rfl⟩
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LinearOrder R
⊢ Eq.{u + 1} (α := Tropical (WithTop R)) 0 0 ∧ LE.le.{u} (α := Tropical (WithTop R)) 0 0 ∨
    Eq.{u + 1} (α := Tropical (WithTop R)) 0 0 ∧ LE.le.{u} (α := Tropical (WithTop R)) 0 0

Tactic:
simp
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : Add R
x y : R
⊢ trop (x + y) = trop x * trop y

Tactic:
rfl

Premises used: Tropical.trop, rfl, Tropical.untrop
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : Add R
x y : Tropical R
⊢ untrop (x * y) = untrop x + untrop y

Tactic:
rfl

Premises used: Tropical.trop, rfl, Tropical.untrop
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : Add R
x y : Tropical R
⊢ x * y = trop (untrop x + untrop y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : Zero R
⊢ Eq.{u + 1} (α := Tropical R) (trop 0) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : Zero R
⊢ Eq.{u + 1} (α := R) (untrop 1) 0

Tactic:
rfl

Premises used: Tropical.trop, rfl, Tropical.untrop
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LinearOrder R
inst_1 : OrderTop R
inst_2 : Zero R
n : ℕ
zero :
  untrop (if HAdd.hAdd (α := ℕ) 0 1 = 0 then 0 else 1) =
    untrop (HAdd.hAdd (α := Tropical R) (if Eq (α := ℕ) 0 0 then 0 else 1) 1)
succ :
  ∀ (n : ℕ),
    untrop (if n + 1 + 1 = 0 then 0 else 1) = untrop (HAdd.hAdd (α := Tropical R) (if n + 1 = 0 then 0 else 1) 1)
⊢ untrop (if n + 1 = 0 then 0 else 1) = untrop (HAdd.hAdd (α := Tropical R) (if n = 0 then 0 else 1) 1)

Tactic:
cases n
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LinearOrder R
inst_1 : OrderTop R
inst_2 : Zero R
⊢ untrop (if HAdd.hAdd (α := ℕ) 0 1 = 0 then 0 else 1) =
    untrop (HAdd.hAdd (α := Tropical R) (if Eq (α := ℕ) 0 0 then 0 else 1) 1)

Tactic:
simp
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LinearOrder R
inst_1 : OrderTop R
inst_2 : Zero R
n : ℕ
⊢ untrop (if n + 1 + 1 = 0 then 0 else 1) = untrop (HAdd.hAdd (α := Tropical R) (if n + 1 = 0 then 0 else 1) 1)

Tactic:
simp
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : Zero R
⊢ Nontrivial.{u} (Tropical (WithTop R))

Tactic:
⟨⟨0, 1, trop_injective.ne WithTop.top_ne_coe⟩⟩

Premises used: WithTop.top_ne_coe, Function.Injective.ne, Nontrivial.mk, Exists.intro, OfNat.ofNat, Tropical.trop_injective
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : Neg R
x : Tropical R
⊢ untrop x⁻¹ = -untrop x

Tactic:
rfl

Premises used: Tropical.trop, rfl, Tropical.untrop
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : Sub R
x y : Tropical R
⊢ untrop (x / y) = untrop x - untrop y

Tactic:
rfl

Premises used: Tropical.trop, rfl, Tropical.untrop
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
α : Type u_1
inst : SMul α R
x : Tropical R
n : α
⊢ untrop (x ^ n) = n • untrop x

Tactic:
rfl

Premises used: Tropical.trop, rfl, Tropical.untrop
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
α : Type u_1
inst : SMul α R
x : R
n : α
⊢ trop (n • x) = trop x ^ n

Tactic:
rfl

Premises used: Tropical.trop, rfl, Tropical.untrop
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : AddMonoid R
x : Tropical R
⊢ untrop (HPow.hPow (β := ℕ) x 0) = untrop 1

Tactic:
simp
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : AddMonoid R
x : R
n : ℕ
⊢ trop (n • x) = trop x ^ n

Tactic:
rfl

Premises used: Tropical.trop, rfl, Tropical.untrop
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : AddGroup R
x x_1 : Tropical R
⊢ untrop (x / x_1) = untrop (x * x_1⁻¹)

Tactic:
simp [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : AddGroup R
x : Tropical R
n : ℤ
⊢ untrop (x ^ n) = n • untrop x

Tactic:
rfl

Premises used: Tropical.trop, rfl, Tropical.untrop
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : AddGroup R
x : R
n : ℤ
⊢ trop (n • x) = trop x ^ n

Tactic:
rfl

Premises used: Tropical.trop, rfl, Tropical.untrop
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LE R
inst_1 : Add R
inst_2 : AddLeftMono R
⊢ MulLeftMono.{u} (Tropical R)

Tactic:
⟨fun _ y z h => add_le_add_right (show untrop y ≤ untrop z from h) _⟩

Premises used: CovariantClass.mk, add_le_add_right, Tropical.untrop
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LE R
inst_1 : Add R
inst_2 : AddRightMono R
⊢ MulRightMono.{u} (Tropical R)

Tactic:
⟨fun _ y z h => add_le_add_left (show untrop y ≤ untrop z from h) _⟩

Premises used: CovariantClass.mk, add_le_add_left, Tropical.untrop
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LinearOrder R
x y z : Tropical R
h : y ≤ z
inl : ∀ (hx : x ≤ y), x + y ≤ x + z
inr : ∀ (hy : y ≤ x), x + y ≤ x + z
⊢ x + y ≤ x + z

Tactic:
rcases le_total x y with hx | hy

Premises used: le_total
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LinearOrder R
x y z : Tropical R
h : y ≤ z
hx : x ≤ y
inl : x ≤ x + z
inl₁ inl₂ : x ≤ x
⊢ x + y ≤ x + z

Tactic:
rw [add_eq_left hx, add_eq_left (hx.trans h)]

Premises used: LE.le.trans, Tropical.add_eq_left
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LinearOrder R
x y z : Tropical R
h : y ≤ z
hy : y ≤ x
inr : y ≤ x + z
⊢ x + y ≤ x + z

Tactic:
rw [add_eq_right hy]

Premises used: Tropical.add_eq_right
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LinearOrder R
x y z : Tropical R
h : y ≤ z
hy : y ≤ x
inr : ∀ (hx : x ≤ z), y ≤ x + z
inr₁ : ∀ (hx : z ≤ x), y ≤ x + z
⊢ y ≤ x + z

Tactic:
rcases le_total x z with hx | hx

Premises used: le_total
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LinearOrder R
x y z : Tropical R
h : y ≤ z
hy : y ≤ x
hx : x ≤ z
inr inr₁ inr₂ inr₃ : y ≤ x
⊢ y ≤ x + z

Tactic:
rwa [add_eq_left hx]

Premises used: Tropical.add_eq_left
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LinearOrder R
x y z : Tropical R
h : y ≤ z
hy : y ≤ x
hx : z ≤ x
inr inr₁ inr₂ inr₃ : y ≤ z
⊢ y ≤ x + z

Tactic:
rwa [add_eq_right hx]

Premises used: Tropical.add_eq_right
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LT R
inst_1 : Add R
inst_2 : AddLeftStrictMono R
⊢ MulLeftStrictMono.{u} (Tropical R)

Tactic:
⟨fun _ _ _ h => add_lt_add_right (untrop_lt_iff.2 h) _⟩

Premises used: CovariantClass.mk, Iff.mpr, add_lt_add_right, Tropical.untrop_lt_iff, Tropical.untrop
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : Preorder R
inst_1 : Add R
inst_2 : AddRightStrictMono R
⊢ MulRightStrictMono.{u} (Tropical R)

Tactic:
⟨fun _ y z h => add_lt_add_left (show untrop y < untrop z from h) _⟩

Premises used: CovariantClass.mk, add_lt_add_left, Tropical.untrop
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LinearOrder R
inst_1 : AddMonoid R
inst_2 : AddLeftMono R
inst_3 : AddRightMono R
x y : Tropical R
n : ℕ
inl : ∀ (h : x ≤ y), (x + y) ^ n = x ^ n + y ^ n
inr : ∀ (h : y ≤ x), (x + y) ^ n = x ^ n + y ^ n
⊢ (x + y) ^ n = x ^ n + y ^ n

Tactic:
rcases le_total x y with h | h

Premises used: le_total
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LinearOrder R
inst_1 : AddMonoid R
inst_2 : AddLeftMono R
inst_3 : AddRightMono R
x y : Tropical R
n : ℕ
h : x ≤ y
inl : x ^ n = x ^ n + y ^ n
inl₁ inl₂ : x ^ n = x ^ n
⊢ (x + y) ^ n = x ^ n + y ^ n

Tactic:
rw [add_eq_left h, add_eq_left (pow_le_pow_left' h _)]

Premises used: pow_le_pow_left', Tropical.add_eq_left
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LinearOrder R
inst_1 : AddMonoid R
inst_2 : AddLeftMono R
inst_3 : AddRightMono R
x y : Tropical R
n : ℕ
h : y ≤ x
inr : y ^ n = x ^ n + y ^ n
inr₁ inr₂ : y ^ n = y ^ n
⊢ (x + y) ^ n = x ^ n + y ^ n

Tactic:
rw [add_eq_right h, add_eq_right (pow_le_pow_left' h _)]

Premises used: pow_le_pow_left', Tropical.add_eq_right
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LinearOrderedAddCommMonoidWithTop R
x : Tropical R
⊢ untrop (0 * x) = untrop 0

Tactic:
simp [top_add]

Premises used: top_add
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LinearOrderedAddCommMonoidWithTop R
x : Tropical R
⊢ untrop (x * 0) = untrop 0

Tactic:
simp [add_top]

Premises used: add_top
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : OrderTop R
x : Tropical R
⊢ HAdd.hAdd (α := ℕ) 0 1 • x = x

Tactic:
simp [one_nsmul]

Premises used: one_nsmul
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : OrderTop R
x : Tropical R
n : ℕ
IH : (n + 1) • x = x
succ : (n + 1) • x + HSMul.hSMul (α := ℕ) 1 x = x
succ₁ : x + HSMul.hSMul (α := ℕ) 1 x = x
succ₂ : x + x = x
succ₃ succ₄ : x = x
⊢ (n + 1 + 1) • x = x

Tactic:
rw [add_nsmul, IH, one_nsmul, add_self]

Premises used: Tropical.add_self, one_nsmul, add_nsmul
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : OrderTop R
x : Tropical R
n : ℕ
zero : HAdd.hAdd (α := ℕ) 0 1 • x = x
succ : ∀ (n : ℕ) (IH : (n + 1) • x = x), (n + 1 + 1) • x = x
⊢ (n + 1) • x = x

Tactic:
induction n with
  | zero => simp [one_nsmul]
  | succ n IH => rw [add_nsmul, IH, one_nsmul, add_self]

Premises used: Tropical.add_self, one_nsmul, add_nsmul
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u_1
inst : AddCommMonoid R
a b : Tropical (WithTop R)
⊢ a * b = 0 ↔ a = 0 ∨ b = 0

Tactic:
simp [← untrop_inj_iff, WithTop.add_eq_top]

Premises used: Tropical.untrop_inj_iff, WithTop.add_eq_top
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R_1 : Type u
inst : LinearOrderedAddCommMonoidWithTop R_1
R : Type u_1
inst_1 : AddCommMonoid R
⊢ NoZeroDivisors.{u_1} (Tropical (WithTop R))

Tactic:
⟨mul_eq_zero_iff.mp⟩

Premises used: Tropical.mul_eq_zero_iff, Iff.mp, NoZeroDivisors.mk
-- Module: Mathlib.Algebra.Tropical.BigOperators
Goal:
R : Type u_1
inst : AddMonoid R
⊢ Eq.{u_1 + 1} (α := Tropical R) (trop (sum [])) (prod (map trop []))

Tactic:
simp
-- Module: Mathlib.Algebra.Tropical.BigOperators
Goal:
R : Type u_1
inst : AddMonoid R
hd : R
tl : List R
IH : trop tl.sum = (map trop tl).prod
⊢ trop (hd :: tl).sum = (map trop (hd :: tl)).prod

Tactic:
simp [← IH]
-- Module: Mathlib.Algebra.Tropical.BigOperators
Goal:
R : Type u_1
inst : AddMonoid R
l : List R
nil : Eq.{u_1 + 1} (α := Tropical R) (trop (sum [])) (prod (map trop []))
cons :
  ∀ (hd : R) (tl : List R) (IH : trop tl.sum = (map trop tl).prod), trop (hd :: tl).sum = (map trop (hd :: tl)).prod
⊢ trop l.sum = (map trop l).prod

Tactic:
induction l with
  | nil => simp
  | cons hd tl IH => simp [← IH]

Premises used: List.cons, List.nil
-- Module: Mathlib.Algebra.Tropical.BigOperators
Goal:
R : Type u_1
inst : AddCommMonoid R
s : Multiset R
⊢ ∀ (a : List R), trop (sum ⟦a⟧) = (map trop ⟦a⟧).prod

Tactic:
simpa using List.trop_sum

Premises used: List.trop_sum
-- Module: Mathlib.Algebra.Tropical.BigOperators
Goal:
R : Type u_1
S : Type u_2
inst : AddCommMonoid R
s : Finset S
f : S → R
⊢ trop (Multiset.map f s.val).sum = (Multiset.map trop (Multiset.map f s.val)).prod

Tactic:
Multiset.trop_sum (s.val.map f)

Premises used: Multiset.map, Multiset.trop_sum, Finset.val
-- Module: Mathlib.Algebra.Tropical.BigOperators
Goal:
R : Type u_1
S : Type u_2
inst : AddCommMonoid R
s : Finset S
f : S → R
h : ∏ i ∈ s, trop (f i) = (Multiset.map trop (Multiset.map f s.val)).prod
⊢ Eq.{u_1 + 1} (α := Tropical R) (trop (∑ i ∈ s, f i)) (∏ i ∈ s, trop (f i))

Tactic:
convert! Multiset.trop_sum (s.val.map f)

Premises used: Multiset.map, Multiset.trop_sum, Finset.val
-- Module: Mathlib.Algebra.Tropical.BigOperators
Goal:
R : Type u_1
S : Type u_2
inst : AddCommMonoid R
s : Finset S
f : S → R
h : Eq.{u_1 + 1} (α := Tropical R) (∏ i ∈ s, trop (f i)) (Multiset.prod (Multiset.map (fun (i : S) ↦ trop (f i)) s.val))
⊢ ∏ i ∈ s, trop (f i) = (Multiset.map trop (Multiset.map f s.val)).prod

Tactic:
simp only [Multiset.map_map, Function.comp_apply]

Premises used: Multiset.map_map, Function.comp_apply
-- Module: Mathlib.Algebra.Tropical.BigOperators
Goal:
R : Type u_1
S : Type u_2
inst : AddCommMonoid R
s : Finset S
f : S → R
⊢ Eq.{u_1 + 1} (α := Tropical R) (∏ i ∈ s, trop (f i)) (Multiset.prod (Multiset.map (fun (i : S) ↦ trop (f i)) s.val))

Tactic:
rfl
-- Module: Mathlib.Algebra.Tropical.BigOperators
Goal:
R : Type u_1
inst : AddMonoid R
⊢ Eq.{u_1 + 1} (α := R) (untrop (prod [])) (sum (map untrop []))

Tactic:
simp
-- Module: Mathlib.Algebra.Tropical.BigOperators
Goal:
R : Type u_1
inst : AddMonoid R
hd : Tropical R
tl : List (Tropical R)
IH : untrop tl.prod = (map untrop tl).sum
⊢ untrop (hd :: tl).prod = (map untrop (hd :: tl)).sum

Tactic:
simp [← IH]
-- Module: Mathlib.Algebra.Tropical.BigOperators
Goal:
R : Type u_1
inst : AddMonoid R
l : List (Tropical R)
nil : Eq.{u_1 + 1} (α := R) (untrop (prod [])) (sum (map untrop []))
cons :
  ∀ (hd : Tropical R) (tl : List (Tropical R)) (IH : untrop tl.prod = (map untrop tl).sum),
    untrop (hd :: tl).prod = (map untrop (hd :: tl)).sum
⊢ untrop l.prod = (map untrop l).sum

Tactic:
induction l with
  | nil => simp
  | cons hd tl IH => simp [← IH]

Premises used: List.cons, List.nil
-- Module: Mathlib.Algebra.Tropical.BigOperators
Goal:
R : Type u_1
inst : AddCommMonoid R
s : Multiset (Tropical R)
⊢ ∀ (a : List (Tropical R)), untrop (prod ⟦a⟧) = (map untrop ⟦a⟧).sum

Tactic:
simpa using List.untrop_prod

Premises used: List.untrop_prod
-- Module: Mathlib.Algebra.Tropical.BigOperators
Goal:
R : Type u_1
S : Type u_2
inst : AddCommMonoid R
s : Finset S
f : S → Tropical R
⊢ untrop (Multiset.map f s.val).prod = (Multiset.map untrop (Multiset.map f s.val)).sum

Tactic:
Multiset.untrop_prod (s.val.map f)

Premises used: Multiset.map, Multiset.untrop_prod, Finset.val
-- Module: Mathlib.Algebra.Tropical.BigOperators
Goal:
R : Type u_1
S : Type u_2
inst : AddCommMonoid R
s : Finset S
f : S → Tropical R
h : ∑ i ∈ s, untrop (f i) = (Multiset.map untrop (Multiset.map f s.val)).sum
⊢ Eq.{u_1 + 1} (α := R) (untrop (∏ i ∈ s, f i)) (∑ i ∈ s, untrop (f i))

Tactic:
convert! Multiset.untrop_prod (s.val.map f)

Premises used: Multiset.map, Multiset.untrop_prod, Finset.val
-- Module: Mathlib.Algebra.Tropical.BigOperators
Goal:
R : Type u_1
S : Type u_2
inst : AddCommMonoid R
s : Finset S
f : S → Tropical R
h : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, untrop (f i)) (Multiset.sum (Multiset.map (fun (i : S) ↦ untrop (f i)) s.val))
⊢ ∑ i ∈ s, untrop (f i) = (Multiset.map untrop (Multiset.map f s.val)).sum

Tactic:
simp only [Multiset.map_map, Function.comp_apply]

Premises used: Multiset.map_map, Function.comp_apply
-- Module: Mathlib.Algebra.Tropical.BigOperators
Goal:
R : Type u_1
S : Type u_2
inst : AddCommMonoid R
s : Finset S
f : S → Tropical R
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ s, untrop (f i)) (Multiset.sum (Multiset.map (fun (i : S) ↦ untrop (f i)) s.val))

Tactic:
rfl
-- Module: Mathlib.Algebra.Tropical.BigOperators
Goal:
R : Type u_1
inst : LinearOrder R
⊢ Eq.{u_1 + 1} (α := Tropical (WithTop R)) (trop (minimum [])) (sum (map (trop ∘ WithTop.some) []))

Tactic:
simp
-- Module: Mathlib.Algebra.Tropical.BigOperators
Goal:
R : Type u_1
inst : LinearOrder R
hd : R
tl : List R
IH : trop tl.minimum = (map (trop ∘ WithTop.some) tl).sum
⊢ trop (hd :: tl).minimum = (map (trop ∘ WithTop.some) (hd :: tl)).sum

Tactic:
simp [List.minimum_cons, ← IH]

Premises used: List.minimum_cons
-- Module: Mathlib.Algebra.Tropical.BigOperators
Goal:
R : Type u_1
inst : LinearOrder R
l : List R
nil : Eq.{u_1 + 1} (α := Tropical (WithTop R)) (trop (minimum [])) (sum (map (trop ∘ WithTop.some) []))
cons :
  ∀ (hd : R) (tl : List R) (IH : trop tl.minimum = (map (trop ∘ WithTop.some) tl).sum),
    trop (hd :: tl).minimum = (map (trop ∘ WithTop.some) (hd :: tl)).sum
⊢ trop l.minimum = (map (trop ∘ WithTop.some) l).sum

Tactic:
induction l with
  | nil => simp
  | cons hd tl IH => simp [List.minimum_cons, ← IH]

Premises used: List.minimum_cons, List.cons, List.nil
-- Module: Mathlib.Algebra.Tropical.BigOperators
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : OrderTop R
⊢ Eq.{u_1 + 1} (α := Tropical R) (trop (inf 0)) (sum (map trop 0))

Tactic:
simp
-- Module: Mathlib.Algebra.Tropical.BigOperators
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : OrderTop R
s : R
x : Multiset R
IH : trop x.inf = (map trop x).sum
⊢ trop (s ::ₘ x).inf = (map trop (s ::ₘ x)).sum

Tactic:
simp [← IH]
-- Module: Mathlib.Algebra.Tropical.BigOperators
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : OrderTop R
s : Multiset R
empty : Eq.{u_1 + 1} (α := Tropical R) (trop (inf 0)) (sum (map trop 0))
cons : ∀ (s : R) (x : Multiset R) (IH : trop x.inf = (map trop x).sum), trop (s ::ₘ x).inf = (map trop (s ::ₘ x)).sum
⊢ trop s.inf = (map trop s).sum

Tactic:
induction s using Multiset.induction with
  | empty => simp
  | cons s x IH => simp [← IH]

Premises used: Multiset.cons
-- Module: Mathlib.Algebra.Tropical.BigOperators
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : OrderTop R
s : Finset S
f : S → R
⊢ trop (Multiset.map f s.val).inf = (Multiset.map trop (Multiset.map f s.val)).sum

Tactic:
Multiset.trop_inf (s.val.map f)

Premises used: Multiset.map, Multiset.trop_inf, Finset.val
-- Module: Mathlib.Algebra.Tropical.BigOperators
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : OrderTop R
s : Finset S
f : S → R
h : ∑ i ∈ s, trop (f i) = (Multiset.map trop (Multiset.map f s.val)).sum
⊢ trop (s.inf f) = ∑ i ∈ s, trop (f i)

Tactic:
convert! Multiset.trop_inf (s.val.map f)

Premises used: Multiset.map, Multiset.trop_inf, Finset.val
-- Module: Mathlib.Algebra.Tropical.BigOperators
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : OrderTop R
s : Finset S
f : S → R
h : Eq.{u_1 + 1} (α := Tropical R) (∑ i ∈ s, trop (f i)) (Multiset.sum (Multiset.map (fun (i : S) ↦ trop (f i)) s.val))
⊢ ∑ i ∈ s, trop (f i) = (Multiset.map trop (Multiset.map f s.val)).sum

Tactic:
simp only [Multiset.map_map, Function.comp_apply]

Premises used: Multiset.map_map, Function.comp_apply
-- Module: Mathlib.Algebra.Tropical.BigOperators
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : OrderTop R
s : Finset S
f : S → R
⊢ Eq.{u_1 + 1} (α := Tropical R) (∑ i ∈ s, trop (f i)) (Multiset.sum (Multiset.map (fun (i : S) ↦ trop (f i)) s.val))

Tactic:
rfl
-- Module: Mathlib.Algebra.Tropical.BigOperators
Goal:
R : Type u_1
S : Type u_2
inst : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → WithTop R
inl : trop (sInf (f '' (↑∅ : Set S))) = ∑ i ∈ ∅, trop (f i)
inr : ∀ (h : s.Nonempty), trop (sInf (f '' (↑s : Set S))) = ∑ i ∈ s, trop (f i)
⊢ trop (sInf (f '' (↑s : Set S))) = ∑ i ∈ s, trop (f i)

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | h)

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Algebra.Tropical.BigOperators
Goal:
R : Type u_1
S : Type u_2
inst : ConditionallyCompleteLinearOrder R
f : S → WithTop R
⊢ trop (sInf (f '' (↑∅ : Set S))) = ∑ i ∈ ∅, trop (f i)

Tactic:
simp only [Set.image_empty, coe_empty, sum_empty, WithTop.sInf_empty, trop_top]

Premises used: Finset.coe_empty, WithTop.sInf_empty, Tropical.trop_top, Finset.sum_empty, Set.image_empty
-- Module: Mathlib.Algebra.Tropical.BigOperators
Goal:
R : Type u_1
S : Type u_2
inst : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → WithTop R
h : s.Nonempty
inr : trop (s.inf' h f) = ∑ i ∈ s, trop (f i)
inr₁ : trop (s.inf f) = ∑ i ∈ s, trop (f i)
inr₂ inr₃ : Eq.{u_1 + 1} (α := Tropical (WithTop R)) (∑ i ∈ s, trop (f i)) (∑ i ∈ s, trop (f i))
⊢ trop (sInf (f '' (↑s : Set S))) = ∑ i ∈ s, trop (f i)

Tactic:
rw [← inf'_eq_csInf_image _ h, inf'_eq_inf, s.trop_inf]

Premises used: Finset.trop_inf, Finset.inf'_eq_csInf_image, Finset.inf'_eq_inf
-- Module: Mathlib.Algebra.Tropical.BigOperators
Goal:
R : Type u_1
S : Type u_2
inst : ConditionallyCompleteLinearOrder R
inst_1 : Fintype S
f : S → WithTop R
rw : Eq.{u_1 + 1} (α := Tropical (WithTop R)) (trop (sInf (Set.range fun (i : S) ↦ f i))) (∑ i : S, trop (f i))
rw₁ : Eq.{u_1 + 1} (α := Tropical (WithTop R)) (trop (sInf ((fun (i : S) ↦ f i) '' Set.univ))) (∑ i : S, trop (f i))
rw₂ :
  Eq.{u_1 + 1} (α := Tropical (WithTop R)) (trop (sInf ((fun (i : S) ↦ f i) '' (↑univ : Set S)))) (∑ i : S, trop (f i))
rw₃ rw₄ : Eq.{u_1 + 1} (α := Tropical (WithTop R)) (∑ i : S, trop (f i)) (∑ i : S, trop (f i))
⊢ Eq.{u_1 + 1} (α := Tropical (WithTop R)) (trop (⨅ (i : S), f i)) (∑ i : S, trop (f i))

Tactic:
rw [iInf, ← Set.image_univ, ← coe_univ, trop_sInf_image]

Premises used: Set.image_univ, iInf, Finset.coe_univ, trop_sInf_image
-- Module: Mathlib.Algebra.Tropical.BigOperators
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : OrderTop R
⊢ Eq.{u_1 + 1} (α := R) (untrop (sum 0)) (inf (map untrop 0))

Tactic:
simp