awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Basic (goal)
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
⊢ x + y = x ↔ x ≤ y
have rw₂ : min (untrop x) (untrop y) = untrop x ↔ untrop x ≤ untrop y
Tactic: rw [trop_add_def, trop_eq_iff_eq_untrop, ← untrop_le_iff, min_eq_left_iff]
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Basic (goal)
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
⊢ x + y = x ↔ x ≤ y
have rw₃ : untrop x ≤ untrop y ↔ untrop x ≤ untrop y
Tactic: rw [trop_add_def, trop_eq_iff_eq_untrop, ← untrop_le_iff, min_eq_left_iff]
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Basic (goal)
Goal:
R : Type u
inst : LinearOrder R
x y : Tropical R
⊢ x + y = y ↔ y ≤ x
have rw : trop (min (untrop x) (untrop y)) = y ↔ y ≤ x
Tactic: rw [trop_add_def, trop_eq_iff_eq_untrop, ← untrop_le_iff, min_eq_right_iff]
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Basic (goal)
Goal:
R : Type u
inst : LinearOrder R
x y : Tropical R
rw : trop (min (untrop x) (untrop y)) = y ↔ y ≤ x
⊢ x + y = y ↔ y ≤ x
have rw₁ : min (untrop x) (untrop y) = untrop y ↔ y ≤ x
Tactic: rw [trop_add_def, trop_eq_iff_eq_untrop, ← untrop_le_iff, min_eq_right_iff]
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Basic (goal)
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
⊢ x + y = y ↔ y ≤ x
have rw₂ : min (untrop x) (untrop y) = untrop y ↔ untrop y ≤ untrop x
Tactic: rw [trop_add_def, trop_eq_iff_eq_untrop, ← untrop_le_iff, min_eq_right_iff]
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Basic (goal)
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
⊢ x + y = y ↔ y ≤ x
have rw₃ : untrop y ≤ untrop x ↔ untrop y ≤ untrop x
Tactic: rw [trop_add_def, trop_eq_iff_eq_untrop, ← untrop_le_iff, min_eq_right_iff]
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Basic (goal)
Goal:
R : Type u
inst : LinearOrder R
x y z : Tropical R
⊢ x + y = z ↔ x = z ∧ x ≤ y ∨ y = z ∧ y ≤ x
have rw : min (untrop x) (untrop y) = untrop z ↔ x = z ∧ x ≤ y ∨ y = z ∧ y ≤ x
Tactic: rw [trop_add_def, trop_eq_iff_eq_untrop]
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Basic (goal)
Goal:
R : Type u
inst : LinearOrder R
a b : Tropical (WithTop R)
⊢ a + b = 0 ↔ a = 0 ∧ b = 0
have rw : a = 0 ∧ a ≤ b ∨ b = 0 ∧ b ≤ a ↔ a = 0 ∧ b = 0
Tactic: rw [add_eq_iff]
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Basic (goal)
Goal:
R : Type u
inst : LinearOrder R
a b : Tropical (WithTop R)
⊢ a = 0 ∧ a ≤ b ∨ b = 0 ∧ b ≤ a ↔ a = 0 ∧ b = 0
have mp : a = 0 ∧ a ≤ b ∨ b = 0 ∧ b ≤ a → a = 0 ∧ b = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Basic (goal)
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
⊢ a = 0 ∧ a ≤ b ∨ b = 0 ∧ b ≤ a ↔ a = 0 ∧ b = 0
have mpr : a = 0 ∧ b = 0 → a = 0 ∧ a ≤ b ∨ b = 0 ∧ b ≤ a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Basic (goal)
Goal:
R : Type u
inst : LinearOrder R
inst_1 : OrderTop R
inst_2 : Zero R
n : ℕ
⊢ untrop (if n + 1 = 0 then 0 else 1) = untrop (HAdd.hAdd (α := Tropical R) (if n = 0 then 0 else 1) 1)
have 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)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Basic (goal)
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)
⊢ untrop (if n + 1 = 0 then 0 else 1) = untrop (HAdd.hAdd (α := Tropical R) (if n = 0 then 0 else 1) 1)
have 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)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Basic (goal)
Goal:
R : Type u
inst : LinearOrder R
x y z : Tropical R
h : y ≤ z
⊢ x + y ≤ x + z
have inl : ∀ (hx : x ≤ y), x + y ≤ x + z
Tactic: rcases le_total x y with hx | hy
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Basic (goal)
Goal:
R : Type u
inst : LinearOrder R
x y z : Tropical R
h : y ≤ z
inl : ∀ (hx : x ≤ y), x + y ≤ x + z
⊢ x + y ≤ x + z
have inr : ∀ (hy : y ≤ x), x + y ≤ x + z
Tactic: rcases le_total x y with hx | hy
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Basic (goal)
Goal:
R : Type u
inst : LinearOrder R
x y z : Tropical R
h : y ≤ z
hx : x ≤ y
⊢ x + y ≤ x + z
have inl : x ≤ x + z
Tactic: rw [add_eq_left hx, add_eq_left (hx.trans h)]
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Basic (goal)
Goal:
R : Type u
inst : LinearOrder R
x y z : Tropical R
h : y ≤ z
hx : x ≤ y
inl : x ≤ x + z
⊢ x + y ≤ x + z
have inl₁ : x ≤ x
Tactic: rw [add_eq_left hx, add_eq_left (hx.trans h)]
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Basic (goal)
Goal:
R : Type u
inst : LinearOrder R
x y z : Tropical R
h : y ≤ z
hy : y ≤ x
⊢ x + y ≤ x + z
have inr : y ≤ x + z
Tactic: rw [add_eq_right hy]
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Basic (goal)
Goal:
R : Type u
inst : LinearOrder R
x y z : Tropical R
h : y ≤ z
hy : y ≤ x
⊢ y ≤ x + z
have inr : ∀ (hx : x ≤ z), y ≤ x + z
Tactic: rcases le_total x z with hx | hx
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Basic (goal)
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
⊢ y ≤ x + z
have inr₁ : ∀ (hx : z ≤ x), y ≤ x + z
Tactic: rcases le_total x z with hx | hx
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Basic (goal)
Goal:
R : Type u
inst : LinearOrder R
inst_1 : AddMonoid R
inst_2 : AddLeftMono R
inst_3 : AddRightMono R
x y : Tropical R
n : ℕ
⊢ (x + y) ^ n = x ^ n + y ^ n
have inl : ∀ (h : x ≤ y), (x + y) ^ n = x ^ n + y ^ n
Tactic: rcases le_total x y with h | h
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Basic (goal)
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
⊢ (x + y) ^ n = x ^ n + y ^ n
have inr : ∀ (h : y ≤ x), (x + y) ^ n = x ^ n + y ^ n
Tactic: rcases le_total x y with h | h
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Basic (goal)
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
⊢ (x + y) ^ n = x ^ n + y ^ n
have inl : x ^ n = x ^ n + y ^ n
Tactic: rw [add_eq_left h, add_eq_left (pow_le_pow_left' h _)]
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Basic (goal)
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
⊢ (x + y) ^ n = x ^ n + y ^ n
have inl₁ : x ^ n = x ^ n
Tactic: rw [add_eq_left h, add_eq_left (pow_le_pow_left' h _)]
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Basic (goal)
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
⊢ (x + y) ^ n = x ^ n + y ^ n
have inr : y ^ n = x ^ n + y ^ n
Tactic: rw [add_eq_right h, add_eq_right (pow_le_pow_left' h _)]
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Basic (goal)
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
⊢ (x + y) ^ n = x ^ n + y ^ n
have inr₁ : y ^ n = y ^ n
Tactic: rw [add_eq_right h, add_eq_right (pow_le_pow_left' h _)]
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Basic (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : OrderTop R
x : Tropical R
n : ℕ
IH : (n + 1) • x = x
⊢ (n + 1 + 1) • x = x
have succ : (n + 1) • x + HSMul.hSMul (α := ℕ) 1 x = x
Tactic: rw [add_nsmul, IH, one_nsmul, add_self]
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Basic (goal)
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
⊢ (n + 1 + 1) • x = x
have succ₁ : x + HSMul.hSMul (α := ℕ) 1 x = x
Tactic: rw [add_nsmul, IH, one_nsmul, add_self]
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Basic (goal)
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
⊢ (n + 1 + 1) • x = x
have succ₂ : x + x = x
Tactic: rw [add_nsmul, IH, one_nsmul, add_self]
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Basic (goal)
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
⊢ (n + 1 + 1) • x = x
have succ₃ : x = x
Tactic: rw [add_nsmul, IH, one_nsmul, add_self]
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Basic (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : OrderTop R
x : Tropical R
n : ℕ
⊢ (n + 1) • x = x
have zero : HAdd.hAdd (α := ℕ) 0 1 • x = x
Tactic: induction n with
  | zero => simp [one_nsmul]
  | succ n IH => rw [add_nsmul, IH, one_nsmul, add_self]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Basic (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : OrderTop R
x : Tropical R
n : ℕ
zero : HAdd.hAdd (α := ℕ) 0 1 • x = x
⊢ (n + 1) • x = x
have succ : ∀ (n : ℕ) (IH : (n + 1) • x = x), (n + 1 + 1) • x = x
Tactic: induction n with
  | zero => simp [one_nsmul]
  | succ n IH => rw [add_nsmul, IH, one_nsmul, add_self]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Tropical.BigOperators (goal)
Goal:
R : Type u_1
inst : AddMonoid R
l : List R
⊢ trop l.sum = (map trop l).prod
have nil : Eq.{u_1 + 1} (α := Tropical R) (trop (sum [])) (prod (map trop []))
Tactic: induction l with
  | nil => simp
  | cons hd tl IH => simp [← IH]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.Tropical.BigOperators (goal)
Goal:
R : Type u_1
inst : AddMonoid R
l : List R
nil : Eq.{u_1 + 1} (α := Tropical R) (trop (sum [])) (prod (map trop []))
⊢ trop l.sum = (map trop l).prod
have cons : ∀ (hd : R) (tl : List R) (IH : trop tl.sum = (map trop tl).prod), trop (hd :: tl).sum = (map trop (hd :: tl)).prod
Tactic: induction l with
  | nil => simp
  | cons hd tl IH => simp [← IH]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.Tropical.BigOperators (goal)
Goal:
R : Type u_1
S : Type u_2
inst : AddCommMonoid R
s : Finset S
f : S → R
⊢ Eq.{u_1 + 1} (α := Tropical R) (trop (∑ i ∈ s, f i)) (∏ i ∈ s, trop (f i))
have h : ∏ i ∈ s, trop (f i) = (Multiset.map trop (Multiset.map f s.val)).prod
Tactic: convert! Multiset.trop_sum (s.val.map f)
-- Lean 4 proof step from Mathlib.Algebra.Tropical.BigOperators (goal)
Goal:
R : Type u_1
S : Type u_2
inst : AddCommMonoid R
s : Finset S
f : S → R
⊢ ∏ i ∈ s, trop (f i) = (Multiset.map trop (Multiset.map f s.val)).prod
have h : Eq.{u_1 + 1} (α := Tropical R) (∏ i ∈ s, trop (f i)) (Multiset.prod (Multiset.map (fun (i : S) ↦ trop (f i)) s.val))
Tactic: simp only [Multiset.map_map, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Tropical.BigOperators (goal)
Goal:
R : Type u_1
inst : AddMonoid R
l : List (Tropical R)
⊢ untrop l.prod = (map untrop l).sum
have nil : Eq.{u_1 + 1} (α := R) (untrop (prod [])) (sum (map untrop []))
Tactic: induction l with
  | nil => simp
  | cons hd tl IH => simp [← IH]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.Tropical.BigOperators (goal)
Goal:
R : Type u_1
inst : AddMonoid R
l : List (Tropical R)
nil : Eq.{u_1 + 1} (α := R) (untrop (prod [])) (sum (map untrop []))
⊢ untrop l.prod = (map untrop l).sum
have 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
Tactic: induction l with
  | nil => simp
  | cons hd tl IH => simp [← IH]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.Tropical.BigOperators (goal)
Goal:
R : Type u_1
S : Type u_2
inst : AddCommMonoid R
s : Finset S
f : S → Tropical R
⊢ Eq.{u_1 + 1} (α := R) (untrop (∏ i ∈ s, f i)) (∑ i ∈ s, untrop (f i))
have h : ∑ i ∈ s, untrop (f i) = (Multiset.map untrop (Multiset.map f s.val)).sum
Tactic: convert! Multiset.untrop_prod (s.val.map f)
-- Lean 4 proof step from Mathlib.Algebra.Tropical.BigOperators (goal)
Goal:
R : Type u_1
S : Type u_2
inst : AddCommMonoid R
s : Finset S
f : S → Tropical R
⊢ ∑ i ∈ s, untrop (f i) = (Multiset.map untrop (Multiset.map f s.val)).sum
have h : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, untrop (f i)) (Multiset.sum (Multiset.map (fun (i : S) ↦ untrop (f i)) s.val))
Tactic: simp only [Multiset.map_map, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Tropical.BigOperators (goal)
Goal:
R : Type u_1
inst : LinearOrder R
l : List R
⊢ trop l.minimum = (map (trop ∘ WithTop.some) l).sum
have nil : Eq.{u_1 + 1} (α := Tropical (WithTop R)) (trop (minimum [])) (sum (map (trop ∘ WithTop.some) []))
Tactic: induction l with
  | nil => simp
  | cons hd tl IH => simp [List.minimum_cons, ← IH]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.Tropical.BigOperators (goal)
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) []))
⊢ trop l.minimum = (map (trop ∘ WithTop.some) l).sum
have 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
Tactic: induction l with
  | nil => simp
  | cons hd tl IH => simp [List.minimum_cons, ← IH]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.Tropical.BigOperators (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : OrderTop R
s : Multiset R
⊢ trop s.inf = (map trop s).sum
have empty : Eq.{u_1 + 1} (α := Tropical R) (trop (inf 0)) (sum (map trop 0))
Tactic: induction s using Multiset.induction with
  | empty => simp
  | cons s x IH => simp [← IH]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.Tropical.BigOperators (goal)
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))
⊢ trop s.inf = (map trop s).sum
have cons : ∀ (s : R) (x : Multiset R) (IH : trop x.inf = (map trop x).sum), trop (s ::ₘ x).inf = (map trop (s ::ₘ x)).sum
Tactic: induction s using Multiset.induction with
  | empty => simp
  | cons s x IH => simp [← IH]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.Tropical.BigOperators (goal)
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : OrderTop R
s : Finset S
f : S → R
⊢ trop (s.inf f) = ∑ i ∈ s, trop (f i)
have h : ∑ i ∈ s, trop (f i) = (Multiset.map trop (Multiset.map f s.val)).sum
Tactic: convert! Multiset.trop_inf (s.val.map f)
-- Lean 4 proof step from Mathlib.Algebra.Tropical.BigOperators (goal)
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : OrderTop R
s : Finset S
f : S → R
⊢ ∑ i ∈ s, trop (f i) = (Multiset.map trop (Multiset.map f s.val)).sum
have h : Eq.{u_1 + 1} (α := Tropical R) (∑ i ∈ s, trop (f i)) (Multiset.sum (Multiset.map (fun (i : S) ↦ trop (f i)) s.val))
Tactic: simp only [Multiset.map_map, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Tropical.BigOperators (goal)
Goal:
R : Type u_1
S : Type u_2
inst : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → WithTop R
⊢ trop (sInf (f '' (↑s : Set S))) = ∑ i ∈ s, trop (f i)
have inl : trop (sInf (f '' (↑∅ : Set S))) = ∑ i ∈ ∅, trop (f i)
Tactic: rcases s.eq_empty_or_nonempty with (rfl | h)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.Tropical.BigOperators (goal)
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)
⊢ trop (sInf (f '' (↑s : Set S))) = ∑ i ∈ s, trop (f i)
have inr : ∀ (h : s.Nonempty), trop (sInf (f '' (↑s : Set S))) = ∑ i ∈ s, trop (f i)
Tactic: rcases s.eq_empty_or_nonempty with (rfl | h)
-- Lean 4 proof step from Mathlib.Algebra.Tropical.BigOperators (goal)
Goal:
R : Type u_1
S : Type u_2
inst : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → WithTop R
h : s.Nonempty
⊢ trop (sInf (f '' (↑s : Set S))) = ∑ i ∈ s, trop (f i)
have inr : trop (s.inf' h f) = ∑ i ∈ s, trop (f i)
Tactic: rw [← inf'_eq_csInf_image _ h, inf'_eq_inf, s.trop_inf]
-- Lean 4 proof step from Mathlib.Algebra.Tropical.BigOperators (goal)
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)
⊢ trop (sInf (f '' (↑s : Set S))) = ∑ i ∈ s, trop (f i)
have inr₁ : trop (s.inf f) = ∑ i ∈ s, trop (f i)
Tactic: rw [← inf'_eq_csInf_image _ h, inf'_eq_inf, s.trop_inf]
-- Lean 4 proof step from Mathlib.Algebra.Tropical.BigOperators (goal)
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)
⊢ trop (sInf (f '' (↑s : Set S))) = ∑ i ∈ s, trop (f i)
have inr₂ : Eq.{u_1 + 1} (α := Tropical (WithTop R)) (∑ i ∈ s, trop (f i)) (∑ i ∈ s, trop (f i))
Tactic: rw [← inf'_eq_csInf_image _ h, inf'_eq_inf, s.trop_inf]
-- Lean 4 proof step from Mathlib.Algebra.Tropical.BigOperators (goal)
Goal:
R : Type u_1
S : Type u_2
inst : ConditionallyCompleteLinearOrder R
inst_1 : Fintype S
f : S → WithTop R
⊢ Eq.{u_1 + 1} (α := Tropical (WithTop R)) (trop (⨅ (i : S), f i)) (∑ i : S, trop (f i))
have rw : Eq.{u_1 + 1} (α := Tropical (WithTop R)) (trop (sInf (Set.range fun (i : S) ↦ f i))) (∑ i : S, trop (f i))
Tactic: rw [iInf, ← Set.image_univ, ← coe_univ, trop_sInf_image]
-- Lean 4 proof step from Mathlib.Algebra.Tropical.BigOperators (goal)
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))
⊢ Eq.{u_1 + 1} (α := Tropical (WithTop R)) (trop (⨅ (i : S), f i)) (∑ i : S, trop (f i))
have rw₁ : Eq.{u_1 + 1} (α := Tropical (WithTop R)) (trop (sInf ((fun (i : S) ↦ f i) '' Set.univ))) (∑ i : S, trop (f i))
Tactic: rw [iInf, ← Set.image_univ, ← coe_univ, trop_sInf_image]
-- Lean 4 proof step from Mathlib.Algebra.Tropical.BigOperators (goal)
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))
⊢ Eq.{u_1 + 1} (α := Tropical (WithTop R)) (trop (⨅ (i : S), f i)) (∑ i : S, trop (f i))
have rw₂ : Eq.{u_1 + 1} (α := Tropical (WithTop R)) (trop (sInf ((fun (i : S) ↦ f i) '' (↑univ : Set S)))) (∑ i : S, trop (f i))
Tactic: rw [iInf, ← Set.image_univ, ← coe_univ, trop_sInf_image]
-- Lean 4 proof step from Mathlib.Algebra.Tropical.BigOperators (goal)
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))
⊢ Eq.{u_1 + 1} (α := Tropical (WithTop R)) (trop (⨅ (i : S), f i)) (∑ i : S, trop (f i))
have rw₃ : Eq.{u_1 + 1} (α := Tropical (WithTop R)) (∑ i : S, trop (f i)) (∑ i : S, trop (f i))
Tactic: rw [iInf, ← Set.image_univ, ← coe_univ, trop_sInf_image]
-- Lean 4 proof step from Mathlib.Algebra.Tropical.BigOperators (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : OrderTop R
s : Multiset (Tropical R)
⊢ untrop s.sum = (map untrop s).inf
have empty : Eq.{u_1 + 1} (α := R) (untrop (sum 0)) (inf (map untrop 0))
Tactic: induction s using Multiset.induction with
  | empty => simp
  | cons s x IH => simp only [sum_cons, untrop_add, map_cons, inf_cons, ← IH]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.Tropical.BigOperators (goal)
Goal:
R : Type u_1
inst : LinearOrder R
inst_1 : OrderTop R
s : Multiset (Tropical R)
empty : Eq.{u_1 + 1} (α := R) (untrop (sum 0)) (inf (map untrop 0))
⊢ untrop s.sum = (map untrop s).inf
have cons : ∀ (s : Tropical R) (x : Multiset (Tropical R)) (IH : untrop x.sum = (map untrop x).inf),
  untrop (s ::ₘ x).sum = (map untrop (s ::ₘ x)).inf
Tactic: induction s using Multiset.induction with
  | empty => simp
  | cons s x IH => simp only [sum_cons, untrop_add, map_cons, inf_cons, ← IH]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.Tropical.BigOperators (goal)
Goal:
R : Type u_1
S : Type u_2
inst : LinearOrder R
inst_1 : OrderTop R
s : Finset S
f : S → Tropical R
⊢ untrop (∑ i ∈ s, f i) = s.inf (untrop ∘ f)
have h : s.inf (untrop ∘ f) = (Multiset.map untrop (Multiset.map f s.val)).inf
Tactic: convert! Multiset.untrop_sum (s.val.map f)
-- Lean 4 proof step from Mathlib.Algebra.Tropical.BigOperators (goal)
Goal:
R : Type u_1
S : Type u_2
inst : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → Tropical (WithTop R)
⊢ untrop (∑ i ∈ s, f i) = sInf (untrop ∘ f '' (↑s : Set S))
have inl : untrop (∑ i ∈ ∅, f i) = sInf (untrop ∘ f '' (↑∅ : Set S))
Tactic: rcases s.eq_empty_or_nonempty with (rfl | h)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.Tropical.BigOperators (goal)
Goal:
R : Type u_1
S : Type u_2
inst : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → Tropical (WithTop R)
inl : untrop (∑ i ∈ ∅, f i) = sInf (untrop ∘ f '' (↑∅ : Set S))
⊢ untrop (∑ i ∈ s, f i) = sInf (untrop ∘ f '' (↑s : Set S))
have inr : ∀ (h : s.Nonempty), untrop (∑ i ∈ s, f i) = sInf (untrop ∘ f '' (↑s : Set S))
Tactic: rcases s.eq_empty_or_nonempty with (rfl | h)
-- Lean 4 proof step from Mathlib.Algebra.Tropical.BigOperators (goal)
Goal:
R : Type u_1
S : Type u_2
inst : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → Tropical (WithTop R)
h : s.Nonempty
⊢ untrop (∑ i ∈ s, f i) = sInf (untrop ∘ f '' (↑s : Set S))
have inr : untrop (∑ i ∈ s, f i) = s.inf' h (untrop ∘ f)
Tactic: rw [← inf'_eq_csInf_image _ h, inf'_eq_inf, Finset.untrop_sum']
-- Lean 4 proof step from Mathlib.Algebra.Tropical.BigOperators (goal)
Goal:
R : Type u_1
S : Type u_2
inst : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → Tropical (WithTop R)
h : s.Nonempty
inr : untrop (∑ i ∈ s, f i) = s.inf' h (untrop ∘ f)
⊢ untrop (∑ i ∈ s, f i) = sInf (untrop ∘ f '' (↑s : Set S))
have inr₁ : untrop (∑ i ∈ s, f i) = s.inf (untrop ∘ f)
Tactic: rw [← inf'_eq_csInf_image _ h, inf'_eq_inf, Finset.untrop_sum']
-- Lean 4 proof step from Mathlib.Algebra.Tropical.BigOperators (goal)
Goal:
R : Type u_1
S : Type u_2
inst : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → Tropical (WithTop R)
h : s.Nonempty
inr : untrop (∑ i ∈ s, f i) = s.inf' h (untrop ∘ f)
inr₁ : untrop (∑ i ∈ s, f i) = s.inf (untrop ∘ f)
⊢ untrop (∑ i ∈ s, f i) = sInf (untrop ∘ f '' (↑s : Set S))
have inr₂ : s.inf (untrop ∘ f) = s.inf (untrop ∘ f)
Tactic: rw [← inf'_eq_csInf_image _ h, inf'_eq_inf, Finset.untrop_sum']
-- Lean 4 proof step from Mathlib.Algebra.Tropical.BigOperators (goal)
Goal:
R : Type u_1
S : Type u_2
inst : ConditionallyCompleteLinearOrder R
inst_1 : Fintype S
f : S → Tropical (WithTop R)
⊢ Eq.{u_1 + 1} (α := WithTop R) (untrop (∑ i : S, f i)) (⨅ (i : S), untrop (f i))
have rw : Eq.{u_1 + 1} (α := WithTop R) (untrop (∑ i : S, f i)) (sInf (Set.range fun (i : S) ↦ untrop (f i)))
Tactic: rw [iInf, ← Set.image_univ, ← coe_univ, untrop_sum_eq_sInf_image, Function.comp_def]