awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
a : ℕ∞
f : ι → ℕ∞
hne : a ≠ 0
hι : Nonempty ι
d : ℕ
h : ∀ (i : ι), a * f i ≤ (↑d : ℕ∞)
htop : Eq (α := ℕ∞) (⨆ (i : ι), f i) ⊤
i : ι
hi : (↑d : ℕ∞) < f i
⊢ False

Tactic:
exact (((h i).trans_lt hi).trans_le (ENat.self_le_mul_left _ hne)).false

Premises used: ENat.self_le_mul_left, LT.lt.trans_le, LT.lt.false, LE.le.trans_lt
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
a : ℕ∞
f : ι → ℕ∞
hne : a ≠ 0
hι : Nonempty ι
d : ℕ
h : ∀ (i : ι), a * f i ≤ (↑d : ℕ∞)
⊢ LT.lt (α := ℕ∞) (⨆ (i : ι), f i) ⊤

Tactic:
have hlt : ⨆ i, f i < ⊤ := by
    rw [lt_top_iff_ne_top]
    intro htop
    obtain ⟨i, hi : d < f i⟩ := (iSup_eq_top ..).1 htop d (by simp)
    exact (((h i).trans_lt hi).trans_le (ENat.self_le_mul_left _ hne)).false
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
a : ℕ∞
f : ι → ℕ∞
hne : a ≠ 0
hι : Nonempty ι
d : ℕ
h : ∀ (i : ι), a * f i ≤ (↑d : ℕ∞)
hlt : LT.lt (α := ℕ∞) (⨆ (i : ι), f i) ⊤
inr : ∀ (j : ι) (hj : f j = ⨆ (i : ι), f i), a * ⨆ (i : ι), f i ≤ (↑d : ℕ∞)
⊢ a * ⨆ (i : ι), f i ≤ (↑d : ℕ∞)

Tactic:
obtain ⟨j, hj⟩ := exists_eq_iSup_of_lt_top hlt

Premises used: ENat.exists_eq_iSup_of_lt_top
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
a : ℕ∞
f : ι → ℕ∞
hne : a ≠ 0
hι : Nonempty ι
d : ℕ
h : ∀ (i : ι), a * f i ≤ (↑d : ℕ∞)
hlt : LT.lt (α := ℕ∞) (⨆ (i : ι), f i) ⊤
j : ι
hj : f j = ⨆ (i : ι), f i
inr : a * f j ≤ (↑d : ℕ∞)
⊢ a * ⨆ (i : ι), f i ≤ (↑d : ℕ∞)

Tactic:
rw [← hj]
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
a : ℕ∞
f : ι → ℕ∞
hne : a ≠ 0
hι : Nonempty ι
d : ℕ
h : ∀ (i : ι), a * f i ≤ (↑d : ℕ∞)
hlt : LT.lt (α := ℕ∞) (⨆ (i : ι), f i) ⊤
j : ι
hj : f j = ⨆ (i : ι), f i
⊢ a * f j ≤ (↑d : ℕ∞)

Tactic:
apply h
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
a : ℕ∞
f : ι → ℕ∞
d : ℕ∞
h : ∀ (i : ι), a * f i ≤ d
hne : a ≠ 0
hι : Nonempty ι
inr : ∀ (h : ∀ (i : ι), a * f i ≤ ⊤), a * ⨆ (i : ι), f i ≤ ⊤
inr₁ : ∀ (d : ℕ) (h : ∀ (i : ι), a * f i ≤ (↑d : ℕ∞)), a * ⨆ (i : ι), f i ≤ (↑d : ℕ∞)
⊢ a * ⨆ (i : ι), f i ≤ d

Tactic:
cases d with
  | top => simp
  | coe d =>
  have hlt : ⨆ i, f i < ⊤ := by
    rw [lt_top_iff_ne_top]
    intro htop
    obtain ⟨i, hi : d < f i⟩ := (iSup_eq_top ..).1 htop d (by simp)
    exact (((h i).trans_lt hi).trans_le (ENat.self_le_mul_left _ hne)).false
  obtain ⟨j, hj⟩ := exists_eq_iSup_of_lt_top hlt
  rw [← hj]
  apply h
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
simp_rw : a * ⨆ (i : ι), f i = ⨆ (i : ι), a * f i
⊢ (⨆ (i : ι), f i) * a = ⨆ (i : ι), f i * a

Tactic:
simp_rw [mul_comm, ENat.mul_iSup]

Premises used: ENat.mul_iSup, mul_comm
-- Module: Mathlib.Data.ENat.Lattice
Goal:
s : Set ℕ∞
a : ℕ∞
simp_rw : a * ⨆ a ∈ s, a = ⨆ b ∈ s, a * b
⊢ a * sSup s = ⨆ b ∈ s, a * b

Tactic:
simp_rw [sSup_eq_iSup, mul_iSup]

Premises used: ENat.mul_iSup, sSup_eq_iSup
-- Module: Mathlib.Data.ENat.Lattice
Goal:
s : Set ℕ∞
a : ℕ∞
simp_rw : a * sSup s = ⨆ b ∈ s, a * b
⊢ sSup s * a = ⨆ b ∈ s, b * a

Tactic:
simp_rw [mul_comm, mul_sSup]

Premises used: ENat.mul_sSup, mul_comm
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst : Nonempty ι
x : ι
grw : a * f x ≤ a * f x
i : ι
grw₁ : a * f x ≤ a * f x
i₁ : ι
⊢ a * ⨅ (i : ι), f i ≤ a * f x

Tactic:
grw [iInf_le]

Premises used: iInf_le
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst : Nonempty ι
refine : ⨅ (i : ι), a * f i ≤ a * ⨅ (i : ι), f i
⊢ a * ⨅ (i : ι), f i = ⨅ (i : ι), a * f i

Tactic:
refine (le_iInf fun x ↦ by grw [iInf_le]).antisymm ?_

Premises used: le_iInf, LE.le.antisymm
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst : Nonempty ι
obtain : ∀ (b : ι) (hb : f b = ⨅ (x : ι), f x), ⨅ (i : ι), a * f i ≤ a * ⨅ (i : ι), f i
⊢ ⨅ (i : ι), a * f i ≤ a * ⨅ (i : ι), f i

Tactic:
obtain ⟨b, hb⟩ := ENat.exists_eq_iInf f

Premises used: ENat.exists_eq_iInf
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst : Nonempty ι
b : ι
hb : f b = ⨅ (x : ι), f x
rw : ∀ (b_1 : ℕ∞), (∀ (i : ι), b_1 ≤ a * f i) → b_1 ≤ a * f b
⊢ ⨅ (i : ι), a * f i ≤ a * ⨅ (i : ι), f i

Tactic:
rw [← hb, iInf_le_iff]

Premises used: iInf_le_iff
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst : Nonempty ι
b : ι
hb : f b = ⨅ (x : ι), f x
⊢ ∀ (b_1 : ℕ∞), (∀ (i : ι), b_1 ≤ a * f i) → b_1 ≤ a * f b

Tactic:
fun x h ↦ h _
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst : Nonempty ι
b : ι
hb : f b = ⨅ (x : ι), f x
⊢ ∀ (b_1 : ℕ∞), (∀ (i : ι), b_1 ≤ a * f i) → b_1 ≤ a * f b

Tactic:
exact fun x h ↦ h _
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst : Nonempty ι
simp_rw : a * ⨅ (i : ι), f i = ⨅ (i : ι), a * f i
⊢ (⨅ (i : ι), f i) * a = ⨅ (i : ι), f i * a

Tactic:
simp_rw [mul_comm, mul_iInf]

Premises used: ENat.mul_iInf, mul_comm
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
h₀ : a = 0 → Nonempty ι
inl : ∀ (hι : IsEmpty ι), a * ⨅ (i : ι), f i = ⨅ (i : ι), a * f i
inr : ∀ (hι : Nonempty ι), a * ⨅ (i : ι), f i = ⨅ (i : ι), a * f i
⊢ a * ⨅ (i : ι), f i = ⨅ (i : ι), a * f i

Tactic:
obtain hι | hι := isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
h₀ : a = 0 → Nonempty ι
hι : IsEmpty ι
this : a ≠ 0
⊢ a * ⨅ (i : ι), f i = ⨅ (i : ι), a * f i

Tactic:
simpa [iInf_of_empty, ite_eq_right_iff, mul_top']

Premises used: iInf_of_empty, ENat.mul_top', ite_eq_right_iff
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
h₀ : a = 0 → Nonempty ι
hι : IsEmpty ι
inl : a ≠ 0
⊢ a * ⨅ (i : ι), f i = ⨅ (i : ι), a * f i

Tactic:
suffices a ≠ 0 by simpa [iInf_of_empty, ite_eq_right_iff, mul_top']
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
h₀ : a = 0 → Nonempty ι
hι : IsEmpty ι
⊢ a ≠ 0

Tactic:
aesop
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
h₀ : a = 0 → Nonempty ι
hι : Nonempty ι
inr inr₁ : Eq (α := ℕ∞) (⨅ (i : ι), a * f i) (⨅ (i : ι), a * f i)
⊢ a * ⨅ (i : ι), f i = ⨅ (i : ι), a * f i

Tactic:
rw [mul_iInf]

Premises used: ENat.mul_iInf
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
h₀ : a = 0 → Nonempty ι
simp_rw : a * ⨅ (i : ι), f i = ⨅ (i : ι), a * f i
⊢ (⨅ (i : ι), f i) * a = ⨅ (i : ι), f i * a

Tactic:
simp_rw [mul_comm, mul_iInf' h₀]

Premises used: mul_comm, ENat.mul_iInf'
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
ha₀ : a ≠ 0
⊢ a = 0 → Nonempty ι

Tactic:
simp [ha₀]
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
a : ℕ∞
inst : Nonempty ι
f : ι → ℕ∞
inl : HAdd.hAdd (α := ℕ∞) ⊤ (⨆ (i : ι), f i) = ⨆ (i : ι), ⊤ + f i
inr : ∀ (ha : a ≠ ⊤), a + ⨆ (i : ι), f i = ⨆ (i : ι), a + f i
⊢ a + ⨆ (i : ι), f i = ⨆ (i : ι), a + f i

Tactic:
obtain rfl | ha := eq_or_ne a ⊤

Premises used: eq_or_ne, Top.top, rfl
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
inst : Nonempty ι
f : ι → ℕ∞
⊢ HAdd.hAdd (α := ℕ∞) ⊤ (⨆ (i : ι), f i) = ⨆ (i : ι), ⊤ + f i

Tactic:
simp
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
a : ℕ∞
inst : Nonempty ι
f : ι → ℕ∞
ha : a ≠ ⊤
i : ι
grw : a + f i ≤ a + f i
i₁ : ι
grw₁ : a + f i ≤ a + f i
i₂ : ι
⊢ a + f i ≤ a + ⨆ (i : ι), f i

Tactic:
grw [← le_iSup]

Premises used: le_iSup
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
a : ℕ∞
inst : Nonempty ι
f : ι → ℕ∞
ha : a ≠ ⊤
inr : a + ⨆ (i : ι), f i ≤ ⨆ (i : ι), a + f i
⊢ a + ⨆ (i : ι), f i = ⨆ (i : ι), a + f i

Tactic:
refine le_antisymm ?_ <| iSup_le fun i ↦ by grw [← le_iSup]

Premises used: le_antisymm, iSup_le
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
a : ℕ∞
inst : Nonempty ι
f : ι → ℕ∞
ha : a ≠ ⊤
⊢ a + ⨆ (i : ι), f i ≤ ⨆ (i : ι), a + f i

Tactic:
add_le_of_le_tsub_left_of_le (le_iSup_of_le (Classical.arbitrary _) le_self_add) ?_

Premises used: le_iSup_of_le, Classical.arbitrary, add_le_of_le_tsub_left_of_le, le_self_add
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
a : ℕ∞
inst : Nonempty ι
f : ι → ℕ∞
ha : a ≠ ⊤
inr : ⨆ (i : ι), f i ≤ (⨆ (i : ι), a + f i) - a
⊢ a + ⨆ (i : ι), f i ≤ ⨆ (i : ι), a + f i

Tactic:
refine add_le_of_le_tsub_left_of_le (le_iSup_of_le (Classical.arbitrary _) le_self_add) ?_

Premises used: le_iSup_of_le, Classical.arbitrary, add_le_of_le_tsub_left_of_le, le_self_add
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
a : ℕ∞
inst : Nonempty ι
f : ι → ℕ∞
ha : a ≠ ⊤
⊢ ⨆ (i : ι), f i ≤ (⨆ (i : ι), a + f i) - a

Tactic:
iSup_le fun i ↦ ENat.le_sub_of_add_le_left ha <| le_iSup (a + f ·) i

Premises used: le_iSup, ENat.le_sub_of_add_le_left, HAdd.hAdd, iSup_le
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
a : ℕ∞
inst : Nonempty ι
f : ι → ℕ∞
ha : a ≠ ⊤
⊢ ⨆ (i : ι), f i ≤ (⨆ (i : ι), a + f i) - a

Tactic:
exact iSup_le fun i ↦ ENat.le_sub_of_add_le_left ha <| le_iSup (a + f ·) i

Premises used: le_iSup, ENat.le_sub_of_add_le_left, HAdd.hAdd, iSup_le
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
a : ℕ∞
inst : Nonempty ι
f : ι → ℕ∞
⊢ (⨆ (i : ι), f i) + a = ⨆ (i : ι), f i + a

Tactic:
simp [add_comm, add_iSup]

Premises used: ENat.add_iSup, add_comm
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
a : ℕ∞
p : ι → Prop
h : ∃ (i : ι), p i
f : ι → ℕ∞
⊢ Nonempty.{max 1 u_2} { i : ι // p i }

Tactic:
haveI : Nonempty {i // p i} := nonempty_subtype.2 h
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
a : ℕ∞
p : ι → Prop
h : ∃ (i : ι), p i
f : ι → ℕ∞
this : Nonempty.{max 1 u_2} { i : ι // p i }
⊢ a + ⨆ (i : ι), ⨆ (_ : p i), f i = ⨆ (i : ι), ⨆ (_ : p i), a + f i

Tactic:
simp only [iSup_subtype', add_iSup]

Premises used: iSup_subtype', ENat.add_iSup
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
a : ℕ∞
p : ι → Prop
h : ∃ (i : ι), p i
f : ι → ℕ∞
⊢ (⨆ (i : ι), ⨆ (_ : p i), f i) + a = ⨆ (i : ι), ⨆ (_ : p i), f i + a

Tactic:
simp only [add_comm, add_biSup' h]

Premises used: add_comm, ENat.add_biSup'
-- Module: Mathlib.Data.ENat.Lattice
Goal:
a : ℕ∞
ι : Type u_4
s : Set ι
hs : s.Nonempty
f : ι → ℕ∞
⊢ a + ⨆ i ∈ s, f i = ⨆ i ∈ s, a + f i

Tactic:
add_biSup' hs _

Premises used: ENat.add_biSup'
-- Module: Mathlib.Data.ENat.Lattice
Goal:
a : ℕ∞
ι : Type u_4
s : Set ι
hs : s.Nonempty
f : ι → ℕ∞
⊢ (⨆ i ∈ s, f i) + a = ⨆ i ∈ s, f i + a

Tactic:
biSup_add' hs _

Premises used: ENat.biSup_add'
-- Module: Mathlib.Data.ENat.Lattice
Goal:
s : Set ℕ∞
a : ℕ∞
hs : s.Nonempty
rw : a + ⨆ a ∈ s, a = ⨆ b ∈ s, a + b
rw₁ rw₂ : Eq (α := ℕ∞) (⨆ i ∈ s, a + i) (⨆ b ∈ s, a + b)
⊢ a + sSup s = ⨆ b ∈ s, a + b

Tactic:
rw [sSup_eq_iSup, add_biSup hs]

Premises used: sSup_eq_iSup, ENat.add_biSup
-- Module: Mathlib.Data.ENat.Lattice
Goal:
s : Set ℕ∞
a : ℕ∞
hs : s.Nonempty
rw : (⨆ a ∈ s, a) + a = ⨆ b ∈ s, b + a
rw₁ rw₂ : Eq (α := ℕ∞) (⨆ i ∈ s, i + a) (⨆ b ∈ s, b + a)
⊢ sSup s + a = ⨆ b ∈ s, b + a

Tactic:
rw [sSup_eq_iSup, biSup_add hs]

Premises used: sSup_eq_iSup, ENat.biSup_add
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
κ : Sort u_3
f : ι → ℕ∞
a : ℕ∞
inst : Nonempty ι
inst_1 : Nonempty κ
g : κ → ℕ∞
h : ∀ (i : ι) (j : κ), f i + g j ≤ a
simp_rw : ⨆ (i : ι), ⨆ (i_1 : κ), f i + g i_1 ≤ a
⊢ iSup f + iSup g ≤ a

Tactic:
simp_rw [iSup_add, add_iSup]

Premises used: ENat.add_iSup, ENat.iSup_add
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
κ : Sort u_3
f : ι → ℕ∞
a : ℕ∞
inst : Nonempty ι
inst_1 : Nonempty κ
g : κ → ℕ∞
h : ∀ (i : ι) (j : κ), f i + g j ≤ a
⊢ ⨆ (i : ι), ⨆ (i_1 : κ), f i + g i_1 ≤ a

Tactic:
iSup₂_le h

Premises used: iSup₂_le
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
κ : Sort u_3
f : ι → ℕ∞
a : ℕ∞
inst : Nonempty ι
inst_1 : Nonempty κ
g : κ → ℕ∞
h : ∀ (i : ι) (j : κ), f i + g j ≤ a
⊢ ⨆ (i : ι), ⨆ (i_1 : κ), f i + g i_1 ≤ a

Tactic:
exact iSup₂_le h

Premises used: iSup₂_le
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
κ : Sort u_3
f : ι → ℕ∞
a : ℕ∞
p : ι → Prop
q : κ → Prop
hp : ∃ (i : ι), p i
hq : ∃ (j : κ), q j
g : κ → ℕ∞
h : ∀ (i : ι), p i → ∀ (j : κ), q j → f i + g j ≤ a
simp_rw : ⨆ (i : ι), ⨆ (_ : p i), ⨆ (i_1 : κ), ⨆ (_ : q i_1), f i + g i_1 ≤ a
⊢ HAdd.hAdd (α := ℕ∞) (⨆ (i : ι), ⨆ (_ : p i), f i) (⨆ (j : κ), ⨆ (_ : q j), g j) ≤ a

Tactic:
simp_rw [biSup_add' hp, add_biSup' hq]

Premises used: ENat.biSup_add', ENat.add_biSup'
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
κ : Sort u_3
f : ι → ℕ∞
a : ℕ∞
p : ι → Prop
q : κ → Prop
hp : ∃ (i : ι), p i
hq : ∃ (j : κ), q j
g : κ → ℕ∞
h : ∀ (i : ι), p i → ∀ (j : κ), q j → f i + g j ≤ a
⊢ ⨆ (i : ι), ⨆ (_ : p i), ⨆ (i_1 : κ), ⨆ (_ : q i_1), f i + g i_1 ≤ a

Tactic:
iSup₂_le fun i hi => iSup₂_le (h i hi)

Premises used: iSup₂_le
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
κ : Sort u_3
f : ι → ℕ∞
a : ℕ∞
p : ι → Prop
q : κ → Prop
hp : ∃ (i : ι), p i
hq : ∃ (j : κ), q j
g : κ → ℕ∞
h : ∀ (i : ι), p i → ∀ (j : κ), q j → f i + g j ≤ a
⊢ ⨆ (i : ι), ⨆ (_ : p i), ⨆ (i_1 : κ), ⨆ (_ : q i_1), f i + g i_1 ≤ a

Tactic:
exact iSup₂_le fun i hi => iSup₂_le (h i hi)

Premises used: iSup₂_le
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Type u_4
κ : Type u_5
s : Set ι
t : Set κ
hs : s.Nonempty
ht : t.Nonempty
f : ι → ℕ∞
g : κ → ℕ∞
a : ℕ∞
h : ∀ i ∈ s, ∀ j ∈ t, f i + g j ≤ a
⊢ HAdd.hAdd (α := ℕ∞) (⨆ i ∈ s, f i) (⨆ j ∈ t, g j) ≤ a

Tactic:
biSup_add_biSup_le' hs ht h

Premises used: ENat.biSup_add_biSup_le'
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
f g : ι → ℕ∞
h : ∀ (i j : ι), ∃ (k : ι), f i + g j ≤ f k + g k
inl : IsEmpty ι → iSup f + iSup g = ⨆ (i : ι), f i + g i
inr : Nonempty ι → iSup f + iSup g = ⨆ (i : ι), f i + g i
⊢ iSup f + iSup g = ⨆ (i : ι), f i + g i

Tactic:
cases isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
f g : ι → ℕ∞
h : ∀ (i j : ι), ∃ (k : ι), f i + g j ≤ f k + g k
h_1 : IsEmpty ι
⊢ iSup f + iSup g = ⨆ (i : ι), f i + g i

Tactic:
simp
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
f g : ι → ℕ∞
h : ∀ (i j : ι), ∃ (k : ι), f i + g j ≤ f k + g k
h_1 : Nonempty ι
⊢ iSup f + iSup g = ⨆ (i : ι), f i + g i

Tactic:
le_antisymm ?_ (iSup_le fun a => add_le_add (le_iSup _ _) (le_iSup _ _))

Premises used: add_le_add, le_iSup, le_antisymm, iSup_le
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
f g : ι → ℕ∞
h : ∀ (i j : ι), ∃ (k : ι), f i + g j ≤ f k + g k
h_1 : Nonempty ι
inr : iSup f + iSup g ≤ ⨆ (i : ι), f i + g i
⊢ iSup f + iSup g = ⨆ (i : ι), f i + g i

Tactic:
refine le_antisymm ?_ (iSup_le fun a => add_le_add (le_iSup _ _) (le_iSup _ _))

Premises used: add_le_add, le_iSup, le_antisymm, iSup_le
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
f g : ι → ℕ∞
h : ∀ (i j : ι), ∃ (k : ι), f i + g j ≤ f k + g k
h_1 : Nonempty ι
⊢ iSup f + iSup g ≤ ⨆ (i : ι), f i + g i

Tactic:
iSup_add_iSup_le fun i j => ?_

Premises used: ENat.iSup_add_iSup_le
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
f g : ι → ℕ∞
h : ∀ (i j : ι), ∃ (k : ι), f i + g j ≤ f k + g k
h_1 : Nonempty ι
inr : ∀ (i j : ι), f i + g j ≤ ⨆ (i : ι), f i + g i
⊢ iSup f + iSup g ≤ ⨆ (i : ι), f i + g i

Tactic:
refine iSup_add_iSup_le fun i j => ?_

Premises used: ENat.iSup_add_iSup_le
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
f g : ι → ℕ∞
h : ∀ (i j : ι), ∃ (k : ι), f i + g j ≤ f k + g k
h_1 : Nonempty ι
i j : ι
inr : ∀ (k : ι) (hk : f i + g j ≤ f k + g k), f i + g j ≤ ⨆ (i : ι), f i + g i
⊢ f i + g j ≤ ⨆ (i : ι), f i + g i

Tactic:
rcases h i j with ⟨k, hk⟩
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
f g : ι → ℕ∞
h : ∀ (i j : ι), ∃ (k : ι), f i + g j ≤ f k + g k
h_1 : Nonempty ι
i j k : ι
hk : f i + g j ≤ f k + g k
⊢ f i + g j ≤ ⨆ (i : ι), f i + g i

Tactic:
le_iSup_of_le k hk

Premises used: le_iSup_of_le
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
f g : ι → ℕ∞
h : ∀ (i j : ι), ∃ (k : ι), f i + g j ≤ f k + g k
h_1 : Nonempty ι
i j k : ι
hk : f i + g j ≤ f k + g k
⊢ f i + g j ≤ ⨆ (i : ι), f i + g i

Tactic:
exact le_iSup_of_le k hk

Premises used: le_iSup_of_le
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Type u_4
inst : Preorder ι
inst_1 : IsDirectedOrder ι
f g : ι → ℕ∞
hf : Monotone f
hg : Monotone g
i j _k : ι
h : i ≤ _k ∧ j ≤ _k
hi : i ≤ _k
hj : j ≤ _k
h₁ : f i ≤ f _k
h₂ : g j ≤ g _k
⊢ f i + g j ≤ f _k + g _k

Tactic:
gcongr
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Type u_4
inst : Preorder ι
inst_1 : IsDirectedOrder ι
f g : ι → ℕ∞
hf : Monotone f
hg : Monotone g
i j _k : ι
h : i ≤ _k ∧ j ≤ _k
hi : i ≤ _k
hj : j ≤ _k
⊢ f i ≤ f _k

Tactic:
apply_rules
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Type u_4
inst : Preorder ι
inst_1 : IsDirectedOrder ι
f g : ι → ℕ∞
hf : Monotone f
hg : Monotone g
i j _k : ι
h : i ≤ _k ∧ j ≤ _k
hi : i ≤ _k
hj : j ≤ _k
⊢ g j ≤ g _k

Tactic:
apply_rules
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
R : Type u_4
inst : SMul R ℕ∞
inst_1 : IsScalarTower R ℕ∞ ℕ∞
f : ι → ℕ∞
c : R
⊢ HSMul.hSMul (β := ℕ∞) c (⨆ (i : ι), f i) = ⨆ (i : ι), c • f i

Tactic:
simpa using mul_iSup (c • 1) f

Premises used: ENat.mul_iSup, HSMul.hSMul, OfNat.ofNat
-- Module: Mathlib.Data.ENat.Lattice
Goal:
R : Type u_4
inst : SMul R ℕ∞
inst_1 : IsScalarTower R ℕ∞ ℕ∞
s : Set ℕ∞
c : R
simp_rw : HSMul.hSMul (β := ℕ∞) c (⨆ a ∈ s, a) = ⨆ a ∈ s, c • a
⊢ c • sSup s = ⨆ a ∈ s, c • a

Tactic:
simp_rw [sSup_eq_iSup, smul_iSup]

Premises used: ENat.smul_iSup, sSup_eq_iSup
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst : Nonempty ι
ha : a ≠ ⊤
inl : ∀ (i : ι) (hi : a < f i), a - ⨆ (i : ι), f i = ⨅ (i : ι), a - f i
inr : ∀ (h : ¬∃ (i : ι), a < f i), a - ⨆ (i : ι), f i = ⨅ (i : ι), a - f i
⊢ a - ⨆ (i : ι), f i = ⨅ (i : ι), a - f i

Tactic:
obtain ⟨i, hi⟩ | h := em (∃ i, a < f i)

Premises used: Exists, em, LT.lt
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst : Nonempty ι
ha : a ≠ ⊤
i : ι
hi : a < f i
inl : ∀ (b : ℕ∞), ⊥ < b → ∃ (i : ι), a - f i < b
⊢ a - ⨆ (i : ι), f i = ⨅ (i : ι), a - f i

Tactic:
rw [tsub_eq_zero_iff_le.2 <| le_iSup_of_le _ hi.le, iInf_eq_bot.2, bot_eq_zero]

Premises used: Iff.mpr, LT.lt.le, tsub_eq_zero_iff_le, le_iSup_of_le, iInf_eq_bot, bot_eq_zero
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst : Nonempty ι
ha : a ≠ ⊤
i : ι
hi : a < f i
x : ℕ∞
hx : ⊥ < x
⊢ a - f i < x

Tactic:
simpa [hi.le, tsub_eq_zero_of_le]

Premises used: tsub_eq_zero_of_le, LT.lt.le
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst : Nonempty ι
ha : a ≠ ⊤
i : ι
hi : a < f i
⊢ ∀ (b : ℕ∞), ⊥ < b → ∃ (i : ι), a - f i < b

Tactic:
exact fun x hx ↦ ⟨i, by simpa [hi.le, tsub_eq_zero_of_le]⟩
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst : Nonempty ι
ha : a ≠ ⊤
h : ¬∃ (i : ι), a < f i
⊢ ∀ (x : ι), f x ≤ a

Tactic:
simp_rw [not_exists, not_lt] at h

Premises used: not_exists, not_lt
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst : Nonempty ι
ha : a ≠ ⊤
h : ∀ (x : ι), f x ≤ a
⊢ a - ⨆ (i : ι), f i = ⨅ (i : ι), a - f i

Tactic:
le_antisymm (le_iInf fun i ↦ tsub_le_tsub_left (le_iSup ..) _) <|
    ENat.le_sub_of_add_le_left (ne_top_of_le_ne_top ha <| iSup_le h) <|
    add_le_of_le_tsub_right_of_le (iInf_le_of_le (Classical.arbitrary _) tsub_le_self) <|
    iSup_le fun i ↦ ?_

Premises used: le_iInf, le_iSup, ENat.le_sub_of_add_le_left, tsub_le_tsub_left, add_le_of_le_tsub_right_of_le, tsub_le_self, le_antisymm, ne_top_of_le_ne_top, Classical.arbitrary, iSup_le, iInf_le_of_le
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst : Nonempty ι
ha : a ≠ ⊤
h : ∀ (x : ι), f x ≤ a
inr : ∀ (i : ι), f i ≤ a - ⨅ (i : ι), a - f i
⊢ a - ⨆ (i : ι), f i = ⨅ (i : ι), a - f i

Tactic:
refine le_antisymm (le_iInf fun i ↦ tsub_le_tsub_left (le_iSup ..) _) <|
    ENat.le_sub_of_add_le_left (ne_top_of_le_ne_top ha <| iSup_le h) <|
    add_le_of_le_tsub_right_of_le (iInf_le_of_le (Classical.arbitrary _) tsub_le_self) <|
    iSup_le fun i ↦ ?_

Premises used: le_iInf, le_iSup, ENat.le_sub_of_add_le_left, tsub_le_tsub_left, add_le_of_le_tsub_right_of_le, tsub_le_self, le_antisymm, ne_top_of_le_ne_top, Classical.arbitrary, iSup_le, iInf_le_of_le
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst : Nonempty ι
ha : a ≠ ⊤
h : ∀ (x : ι), f x ≤ a
i : ι
inr : a - (a - f i) ≤ a - ⨅ (i : ι), a - f i
⊢ f i ≤ a - ⨅ (i : ι), a - f i

Tactic:
rw [← ENat.sub_sub_cancel ha (h _)]

Premises used: ENat.sub_sub_cancel
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst : Nonempty ι
ha : a ≠ ⊤
h : ∀ (x : ι), f x ≤ a
i : ι
⊢ a - (a - f i) ≤ a - ⨅ (i : ι), a - f i

Tactic:
tsub_le_tsub_left (iInf_le (a - f ·) i) _

Premises used: HSub.hSub, tsub_le_tsub_left, iInf_le
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst : Nonempty ι
ha : a ≠ ⊤
h : ∀ (x : ι), f x ≤ a
i : ι
⊢ a - (a - f i) ≤ a - ⨅ (i : ι), a - f i

Tactic:
exact tsub_le_tsub_left (iInf_le (a - f ·) i) _

Premises used: HSub.hSub, tsub_le_tsub_left, iInf_le
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
⊢ iInf f + a = ⨅ (i : ι), f i + a

Tactic:
le_antisymm (le_iInf fun _ ↦ add_le_add (iInf_le _ _) le_rfl) <|
    (tsub_le_iff_right.1 <| le_iInf fun _ ↦ tsub_le_iff_right.2 <| iInf_le _ _)

Premises used: Iff.mpr, le_rfl, add_le_add, le_iInf, tsub_le_iff_right, le_antisymm, HAdd.hAdd, Iff.mp, iInf_le
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
⊢ a - ⨅ (i : ι), f i = ⨆ (i : ι), a - f i

Tactic:
eq_of_forall_ge_iff fun c => ?_

Premises used: eq_of_forall_ge_iff
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
refine : ∀ (c : ℕ∞), a - ⨅ (i : ι), f i ≤ c ↔ ⨆ (i : ι), a - f i ≤ c
⊢ a - ⨅ (i : ι), f i = ⨆ (i : ι), a - f i

Tactic:
refine eq_of_forall_ge_iff fun c => ?_

Premises used: eq_of_forall_ge_iff
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
f : ι → ℕ∞
a c : ℕ∞
rw : a ≤ ⨅ (i : ι), f i + c ↔ ⨆ (i : ι), a - f i ≤ c
⊢ a - ⨅ (i : ι), f i ≤ c ↔ ⨆ (i : ι), a - f i ≤ c

Tactic:
rw [tsub_le_iff_right, add_comm, iInf_add]

Premises used: tsub_le_iff_right, add_comm, ENat.iInf_add
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
f : ι → ℕ∞
a c : ℕ∞
⊢ a ≤ ⨅ (i : ι), f i + c ↔ ⨆ (i : ι), a - f i ≤ c

Tactic:
simp [tsub_le_iff_right, add_comm]

Premises used: tsub_le_iff_right, add_comm
-- Module: Mathlib.Data.ENat.Lattice
Goal:
a : ℕ∞
s : Set ℕ∞
⊢ sInf s + a = ⨅ b ∈ s, b + a

Tactic:
simp [sInf_eq_iInf, iInf_add]

Premises used: sInf_eq_iInf, ENat.iInf_add
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
rw : Eq (α := ℕ∞) (⨅ (i : ι), f i + a) (⨅ (b : ι), a + f b)
⊢ a + iInf f = ⨅ (b : ι), a + f b

Tactic:
rw [add_comm, iInf_add]

Premises used: add_comm, ENat.iInf_add
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
⊢ Eq (α := ℕ∞) (⨅ (i : ι), f i + a) (⨅ (b : ι), a + f b)

Tactic:
simp [add_comm]

Premises used: add_comm
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
f g : ι → ℕ∞
h : ∀ (i j : ι), ∃ (k : ι), f k + g k ≤ f i + g j
simp_rw : Eq (α := ℕ∞) (⨅ (a : ι), ⨅ (a' : ι), f a + g a') (⨅ (i : ι), f i + iInf g)
⊢ ⨅ (a : ι), ⨅ (a' : ι), f a + g a' = iInf f + iInf g

Tactic:
simp_rw [iInf_add, add_iInf]

Premises used: ENat.add_iInf, ENat.iInf_add
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Type u_4
inst : Preorder ι
inst_1 : IsCodirectedOrder ι
f g : ι → ℕ∞
hf : Monotone f
hg : Monotone g
i j _k : ι
h : _k ≤ i ∧ _k ≤ j
hi : _k ≤ i
hj : _k ≤ j
h₁ : f _k ≤ f i
h₂ : g _k ≤ g j
⊢ f _k + g _k ≤ f i + g j

Tactic:
gcongr
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Type u_4
inst : Preorder ι
inst_1 : IsCodirectedOrder ι
f g : ι → ℕ∞
hf : Monotone f
hg : Monotone g
i j _k : ι
h : _k ≤ i ∧ _k ≤ j
hi : _k ≤ i
hj : _k ≤ j
⊢ f _k ≤ f i

Tactic:
apply_rules
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Type u_4
inst : Preorder ι
inst_1 : IsCodirectedOrder ι
f g : ι → ℕ∞
hf : Monotone f
hg : Monotone g
i j _k : ι
h : _k ≤ i ∧ _k ≤ j
hi : _k ≤ i
hj : _k ≤ j
⊢ g _k ≤ g j

Tactic:
apply_rules
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
a : ℕ∞
κ : ι → Sort u_4
f : (i : ι) → κ i → ℕ∞
⊢ a + ⨅ (i : ι), ⨅ (j : κ i), f i j = ⨅ (i : ι), ⨅ (j : κ i), a + f i j

Tactic:
simp [add_iInf]

Premises used: ENat.add_iInf
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
a : ℕ∞
κ : ι → Sort u_4
f : (i : ι) → κ i → ℕ∞
⊢ (⨅ (i : ι), ⨅ (j : κ i), f i j) + a = ⨅ (i : ι), ⨅ (j : κ i), f i j + a

Tactic:
simp only [add_comm, add_iInf₂]

Premises used: add_comm, ENat.add_iInf₂