awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.ENat.BigOperators
Goal:
α : Type u_1
s : Finset α
f : α → ℕ∞
h : ∀ a ∈ s, f a < ⊤
⊢ LT.lt (α := ℕ∞) (∏ a ∈ s, f a) ⊤

Tactic:
WithTop.prod_lt_top h

Premises used: WithTop.prod_lt_top, ENat
-- Module: Mathlib.Data.ENat.BigOperators
Goal:
α : Type u_1
s : Finset α
f : α → ℕ∞
⊢ Eq (α := ℕ∞) (∑ x ∈ s, f x) ⊤ ↔ ∃ a ∈ s, f a = ⊤

Tactic:
WithTop.sum_eq_top

Premises used: WithTop.sum_eq_top, ENat
-- Module: Mathlib.Data.ENat.BigOperators
Goal:
α : Type u_1
s : Finset α
f : α → ℕ∞
⊢ Ne (α := ℕ∞) (∑ a ∈ s, f a) ⊤ ↔ ∀ a ∈ s, f a ≠ ⊤

Tactic:
WithTop.sum_ne_top

Premises used: ENat, WithTop.sum_ne_top
-- Module: Mathlib.Data.ENat.BigOperators
Goal:
α : Type u_1
s : Finset α
f : α → ℕ∞
⊢ LT.lt (α := ℕ∞) (∑ a ∈ s, f a) ⊤ ↔ ∀ a ∈ s, f a < ⊤

Tactic:
WithTop.sum_lt_top

Premises used: ENat, WithTop.sum_lt_top
-- Module: Mathlib.Data.ENat.BigOperators
Goal:
α : Type u_1
s : Finset α
f : α → ℕ∞
h : Ne (α := ℕ∞) (∑ x ∈ s, f x) ⊤
a : α
ha : a ∈ s
⊢ f a < ⊤

Tactic:
sum_lt_top.1 h.lt_top a ha

Premises used: ENat.sum_lt_top, Ne.lt_top, Iff.mp
-- Module: Mathlib.Data.ENat.BigOperators
Goal:
α : Type u_1
s : Finset α
f : α → ℕ∞
hf : ∀ a ∈ s, f a ≠ ⊤
rw : Eq (α := ℕ∞) (∑ a ∈ s, f a) (∑ x ∈ s, (↑(f x).toNat : ℕ∞))
⊢ toNat (∑ a ∈ s, f a) = ∑ a ∈ s, (f a).toNat

Tactic:
rw [← coe_inj, coe_toNat (sum_ne_top.2 hf), Nat.cast_sum]

Premises used: Iff.mpr, ENat.coe_toNat, ENat.sum_ne_top, ENat.coe_inj, Nat.cast_sum
-- Module: Mathlib.Data.ENat.BigOperators
Goal:
α : Type u_1
s : Finset α
f : α → ℕ∞
hf : ∀ a ∈ s, f a ≠ ⊤
⊢ Eq (α := ℕ∞) (∑ a ∈ s, f a) (∑ x ∈ s, (↑(f x).toNat : ℕ∞))

Tactic:
sum_congr rfl fun x hx => (coe_toNat (hf x hx)).symm

Premises used: ENat.coe_toNat, Eq.symm, Finset.sum_congr, rfl
-- Module: Mathlib.Data.ENat.BigOperators
Goal:
α : Type u_1
s : Finset α
f : α → ℕ∞
hf : ∀ a ∈ s, f a ≠ ⊤
⊢ Eq (α := ℕ∞) (∑ a ∈ s, f a) (∑ x ∈ s, (↑(f x).toNat : ℕ∞))

Tactic:
exact sum_congr rfl fun x hx => (coe_toNat (hf x hx)).symm

Premises used: ENat.coe_toNat, Eq.symm, Finset.sum_congr, rfl
-- Module: Mathlib.Data.ENat.BigOperators
Goal:
α : Type u_1
s : Finset α
f g : α → ℕ∞
a : α
Hlt : ∀ (i : α), Membership.mem (γ := Finset α) {a} i → f i < g i
⊢ LT.lt (α := ℕ∞) (∑ i ∈ {a}, f i) (∑ i ∈ {a}, g i)

Tactic:
simp [Hlt _ (mem_singleton_self _)]

Premises used: Finset.mem_singleton_self
-- Module: Mathlib.Data.ENat.BigOperators
Goal:
α : Type u_1
s : Finset α
f g : α → ℕ∞
a : α
s_1 : Finset α
h : a ∉ s_1
hs : s_1.Nonempty
ih : ∀ (Hlt : ∀ i ∈ s_1, f i < g i), LT.lt (α := ℕ∞) (∑ i ∈ s_1, f i) (∑ i ∈ s_1, g i)
Hlt : ∀ i ∈ Finset.cons a s_1 h, f i < g i
cons : ∀ (Hlt : f a < g a ∧ ∀ x ∈ s_1, f x < g x), f a + ∑ i ∈ s_1, f i < g a + ∑ i ∈ s_1, g i
⊢ LT.lt (α := ℕ∞) (∑ i ∈ Finset.cons a s_1 h, f i) (∑ i ∈ Finset.cons a s_1 h, g i)

Tactic:
simp only [sum_cons, forall_mem_cons] at Hlt ⊢

Premises used: Finset.sum_cons, Finset.forall_mem_cons
-- Module: Mathlib.Data.ENat.BigOperators
Goal:
α : Type u_1
s : Finset α
f g : α → ℕ∞
a : α
s_1 : Finset α
h : a ∉ s_1
hs : s_1.Nonempty
ih : ∀ (Hlt : ∀ i ∈ s_1, f i < g i), LT.lt (α := ℕ∞) (∑ i ∈ s_1, f i) (∑ i ∈ s_1, g i)
Hlt : f a < g a ∧ ∀ x ∈ s_1, f x < g x
⊢ f a + ∑ i ∈ s_1, f i < g a + ∑ i ∈ s_1, g i

Tactic:
ENat.add_lt_add Hlt.1 (ih Hlt.2)

Premises used: ENat.add_lt_add, And.right, And.left
-- Module: Mathlib.Data.ENat.BigOperators
Goal:
α : Type u_1
s : Finset α
f g : α → ℕ∞
a : α
s_1 : Finset α
h : a ∉ s_1
hs : s_1.Nonempty
ih : ∀ (Hlt : ∀ i ∈ s_1, f i < g i), LT.lt (α := ℕ∞) (∑ i ∈ s_1, f i) (∑ i ∈ s_1, g i)
Hlt : f a < g a ∧ ∀ x ∈ s_1, f x < g x
⊢ f a + ∑ i ∈ s_1, f i < g a + ∑ i ∈ s_1, g i

Tactic:
exact ENat.add_lt_add Hlt.1 (ih Hlt.2)

Premises used: ENat.add_lt_add, And.right, And.left
-- Module: Mathlib.Data.ENat.BigOperators
Goal:
α : Type u_1
s : Finset α
hs : s.Nonempty
f g : α → ℕ∞
Hlt : ∀ i ∈ s, f i < g i
singleton :
  ∀ (a : α) (Hlt : ∀ (i : α), Membership.mem (γ := Finset α) {a} i → f i < g i),
    LT.lt (α := ℕ∞) (∑ i ∈ {a}, f i) (∑ i ∈ {a}, g i)
cons :
  ∀ (a : α) (s : Finset α) (h : a ∉ s),
    s.Nonempty →
      ∀ (ih : ∀ (Hlt : ∀ i ∈ s, f i < g i), LT.lt (α := ℕ∞) (∑ i ∈ s, f i) (∑ i ∈ s, g i))
        (Hlt : ∀ i ∈ Finset.cons a s h, f i < g i),
        LT.lt (α := ℕ∞) (∑ i ∈ Finset.cons a s h, f i) (∑ i ∈ Finset.cons a s h, g i)
⊢ LT.lt (α := ℕ∞) (∑ i ∈ s, f i) (∑ i ∈ s, g i)

Tactic:
induction hs using Nonempty.cons_induction with
  | singleton => simp [Hlt _ (mem_singleton_self _)]
  | cons _ _ _ _ ih =>
    simp only [sum_cons, forall_mem_cons] at Hlt ⊢
    exact ENat.add_lt_add Hlt.1 (ih Hlt.2)

Premises used: Finset.sum_cons, Finset.cons, Finset.forall_mem_cons, Singleton.singleton
-- Module: Mathlib.Data.ENat.BigOperators
Goal:
α : Type u_1
s : Finset α
hs : s.Nonempty
f g : α → ℕ∞
Hle : LE.le (α := ℕ∞) (∑ i ∈ s, f i) (∑ i ∈ s, g i)
contrapose! : ∀ (Hle : ∀ (i : α) (_ : i ∈ s), g i < f i), LT.lt (α := ℕ∞) (∑ i ∈ s, g i) (∑ i ∈ s, f i)
⊢ ∃ i ∈ s, f i ≤ g i

Tactic:
contrapose! Hle
-- Module: Mathlib.Data.ENat.BigOperators
Goal:
α : Type u_1
s : Finset α
hs : s.Nonempty
f g : α → ℕ∞
Hle : ∀ (i : α) (_ : i ∈ s), g i < f i
⊢ LT.lt (α := ℕ∞) (∑ i ∈ s, g i) (∑ i ∈ s, f i)

Tactic:
apply sum_lt_sum_of_nonempty hs Hle

Premises used: ENat.sum_lt_sum_of_nonempty
-- Module: Mathlib.Data.ENat.BigOperators
Goal:
α : Type u_1
ι : Type u_2
f : α → ι → ℕ∞
hf : ∀ (i j : ι), ∃ (k : ι), ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
⊢ Eq (α := ℕ∞) (∑ a ∈ ∅, ⨆ (i : ι), f a i) (⨆ (i : ι), ∑ a ∈ ∅, f a i)

Tactic:
simp
-- Module: Mathlib.Data.ENat.BigOperators
Goal:
α : Type u_1
ι : Type u_2
f : α → ι → ℕ∞
hf : ∀ (i j : ι), ∃ (k : ι), ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
a : α
s : Finset α
ha : a ∉ s
ihs : Eq (α := ℕ∞) (∑ a ∈ s, ⨆ (i : ι), f a i) (⨆ (i : ι), ∑ a ∈ s, f a i)
cons : HAdd.hAdd (α := ℕ∞) (⨆ (i : ι), f a i) (⨆ (i : ι), ∑ a ∈ s, f a i) = ⨆ (i : ι), f a i + ∑ a ∈ s, f a i
⊢ Eq (α := ℕ∞) (∑ a ∈ Finset.cons a s ha, ⨆ (i : ι), f a i) (⨆ (i : ι), ∑ a ∈ Finset.cons a s ha, f a i)

Tactic:
simp_rw [Finset.sum_cons, ihs]

Premises used: Finset.sum_cons
-- Module: Mathlib.Data.ENat.BigOperators
Goal:
α : Type u_1
ι : Type u_2
f : α → ι → ℕ∞
hf : ∀ (i j : ι), ∃ (k : ι), ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
a : α
s : Finset α
ha : a ∉ s
ihs : Eq (α := ℕ∞) (∑ a ∈ s, ⨆ (i : ι), f a i) (⨆ (i : ι), ∑ a ∈ s, f a i)
⊢ HAdd.hAdd (α := ℕ∞) (⨆ (i : ι), f a i) (⨆ (i : ι), ∑ a ∈ s, f a i) = ⨆ (i : ι), f a i + ∑ a ∈ s, f a i

Tactic:
iSup_add_iSup fun i j ↦ (hf i j).imp fun k hk ↦ ?_

Premises used: Exists.imp, ENat.iSup_add_iSup
-- Module: Mathlib.Data.ENat.BigOperators
Goal:
α : Type u_1
ι : Type u_2
f : α → ι → ℕ∞
hf : ∀ (i j : ι), ∃ (k : ι), ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
a : α
s : Finset α
ha : a ∉ s
ihs : Eq (α := ℕ∞) (∑ a ∈ s, ⨆ (i : ι), f a i) (⨆ (i : ι), ∑ a ∈ s, f a i)
cons : ∀ (i j k : ι) (hk : ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k), f a i + ∑ a ∈ s, f a j ≤ f a k + ∑ a ∈ s, f a k
⊢ HAdd.hAdd (α := ℕ∞) (⨆ (i : ι), f a i) (⨆ (i : ι), ∑ a ∈ s, f a i) = ⨆ (i : ι), f a i + ∑ a ∈ s, f a i

Tactic:
refine iSup_add_iSup fun i j ↦ (hf i j).imp fun k hk ↦ ?_

Premises used: Exists.imp, ENat.iSup_add_iSup
-- Module: Mathlib.Data.ENat.BigOperators
Goal:
α : Type u_1
ι : Type u_2
f : α → ι → ℕ∞
hf : ∀ (i j : ι), ∃ (k : ι), ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
a : α
s : Finset α
ha : a ∉ s
ihs : Eq (α := ℕ∞) (∑ a ∈ s, ⨆ (i : ι), f a i) (⨆ (i : ι), ∑ a ∈ s, f a i)
i j k : ι
hk : ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
cons : f a i ≤ f a k
cons₁ : ∀ i ∈ s, f i j ≤ f i k
⊢ f a i + ∑ a ∈ s, f a j ≤ f a k + ∑ a ∈ s, f a k

Tactic:
gcongr
-- Module: Mathlib.Data.ENat.BigOperators
Goal:
α : Type u_1
ι : Type u_2
f : α → ι → ℕ∞
hf : ∀ (i j : ι), ∃ (k : ι), ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
a : α
s : Finset α
ha : a ∉ s
ihs : Eq (α := ℕ∞) (∑ a ∈ s, ⨆ (i : ι), f a i) (⨆ (i : ι), ∑ a ∈ s, f a i)
i j k : ι
hk : ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
⊢ f a i ≤ f a k

Tactic:
(hk a).1

Premises used: And.left
-- Module: Mathlib.Data.ENat.BigOperators
Goal:
α : Type u_1
ι : Type u_2
f : α → ι → ℕ∞
hf : ∀ (i j : ι), ∃ (k : ι), ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
a : α
s : Finset α
ha : a ∉ s
ihs : Eq (α := ℕ∞) (∑ a ∈ s, ⨆ (i : ι), f a i) (⨆ (i : ι), ∑ a ∈ s, f a i)
i j k : ι
hk : ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
i_1 : α
h : i_1 ∈ s
⊢ f i_1 j ≤ f i_1 k

Tactic:
(hk _).2

Premises used: And.right
-- Module: Mathlib.Data.ENat.BigOperators
Goal:
α : Type u_1
ι : Type u_2
f : α → ι → ℕ∞
hf : ∀ (i j : ι), ∃ (k : ι), ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
a : α
s : Finset α
ha : a ∉ s
ihs : Eq (α := ℕ∞) (∑ a ∈ s, ⨆ (i : ι), f a i) (⨆ (i : ι), ∑ a ∈ s, f a i)
i j k : ι
hk : ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
⊢ f a i ≤ f a k

Tactic:
exacts [(hk a).1, (hk _).2]

Premises used: And.right, And.left
-- Module: Mathlib.Data.ENat.BigOperators
Goal:
α : Type u_1
ι : Type u_2
s : Finset α
f : α → ι → ℕ∞
hf : ∀ (i j : ι), ∃ (k : ι), ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
empty : Eq (α := ℕ∞) (∑ a ∈ ∅, ⨆ (i : ι), f a i) (⨆ (i : ι), ∑ a ∈ ∅, f a i)
cons :
  ∀ (a : α) (s : Finset α) (ha : a ∉ s) (ihs : Eq (α := ℕ∞) (∑ a ∈ s, ⨆ (i : ι), f a i) (⨆ (i : ι), ∑ a ∈ s, f a i)),
    Eq (α := ℕ∞) (∑ a ∈ Finset.cons a s ha, ⨆ (i : ι), f a i) (⨆ (i : ι), ∑ a ∈ Finset.cons a s ha, f a i)
⊢ Eq (α := ℕ∞) (∑ a ∈ s, ⨆ (i : ι), f a i) (⨆ (i : ι), ∑ a ∈ s, f a i)

Tactic:
induction s using Finset.cons_induction with
  | empty => simp
  | cons a s ha ihs =>
    simp_rw [Finset.sum_cons, ihs]
    refine iSup_add_iSup fun i j ↦ (hf i j).imp fun k hk ↦ ?_
    gcongr
    exacts [(hk a).1, (hk _).2]

Premises used: Finset.sum_cons, Exists.imp, ENat.iSup_add_iSup
-- Module: Mathlib.Data.ENat.BigOperators
Goal:
α : Type u_1
ι : Type u_2
inst : Preorder ι
inst_1 : IsDirectedOrder ι
s : Finset α
f : α → ι → ℕ∞
hf : ∀ (a : α), Monotone (f a)
⊢ Eq (α := ℕ∞) (∑ a ∈ s, iSup (f a)) (⨆ (n : ι), ∑ a ∈ s, f a n)

Tactic:
sum_iSup fun i j ↦ (exists_ge_ge i j).imp fun _k ⟨hi, hj⟩ a ↦ ⟨hf a hi, hf a hj⟩

Premises used: ENat.sum_iSup, Exists.imp, exists_ge_ge
-- Module: Mathlib.Data.ENat.Defs
Goal:
C : ℕ∞ → Sort u_1
d : C ⊤
f : (a : ℕ) → C (↑a : ℕ∞)
⊢ recTopCoe (C := C) d f ⊤ = d

Tactic:
rfl

Premises used: ENat.recTopCoe, rfl
-- Module: Mathlib.Data.ENat.Defs
Goal:
C : ℕ∞ → Sort u_1
d : C ⊤
f : (a : ℕ) → C (↑a : ℕ∞)
x : ℕ
⊢ recTopCoe (C := C) d f (↑x : ℕ∞) = f x

Tactic:
rfl

Premises used: ENat.recTopCoe, rfl
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_1
f : ι → ℕ
⊢ Eq (α := ℕ∞) (⨆ (i : ι), (↑(f i) : ℕ∞)) ⊤ ↔ ¬BddAbove (range f)

Tactic:
WithTop.iSup_coe_eq_top

Premises used: ENat, WithTop.iSup_coe_eq_top
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_1
f : ι → ℕ
⊢ Ne (α := ℕ∞) (⨆ (i : ι), (↑(f i) : ℕ∞)) ⊤ ↔ BddAbove (range f)

Tactic:
iSup_coe_eq_top.not_left

Premises used: Iff.not_left, ENat.iSup_coe_eq_top
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_1
f : ι → ℕ
⊢ LT.lt (α := ℕ∞) (⨆ (i : ι), (↑(f i) : ℕ∞)) ⊤ ↔ BddAbove (range f)

Tactic:
WithTop.iSup_coe_lt_top

Premises used: WithTop.iSup_coe_lt_top, ENat
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_1
f : ι → ℕ
⊢ Eq (α := ℕ∞) (⨅ (i : ι), (↑(f i) : ℕ∞)) ⊤ ↔ IsEmpty ι

Tactic:
WithTop.iInf_coe_eq_top

Premises used: WithTop.iInf_coe_eq_top, ENat
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_1
f : ι → ℕ
rw : ¬Eq (α := ℕ∞) (⨅ (i : ι), (↑(f i) : ℕ∞)) ⊤ ↔ Nonempty ι
rw₁ : ¬IsEmpty ι ↔ Nonempty ι
rw₂ rw₃ : Nonempty ι ↔ Nonempty ι
⊢ Ne (α := ℕ∞) (⨅ (i : ι), (↑(f i) : ℕ∞)) ⊤ ↔ Nonempty ι

Tactic:
rw [Ne, iInf_coe_eq_top, not_isEmpty_iff]

Premises used: Ne, ENat.iInf_coe_eq_top, not_isEmpty_iff
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_1
f : ι → ℕ
⊢ LT.lt (α := ℕ∞) (⨅ (i : ι), (↑(f i) : ℕ∞)) ⊤ ↔ Nonempty ι

Tactic:
WithTop.iInf_coe_lt_top

Premises used: WithTop.iInf_coe_lt_top, ENat
-- Module: Mathlib.Data.ENat.Lattice
Goal:
s : Set ℕ
⊢ BddAbove s → Eq (α := ℕ∞) (↑(sSup s) : ℕ∞) (⨆ a ∈ s, (↑a : ℕ∞))

Tactic:
WithTop.coe_sSup

Premises used: WithTop.coe_sSup, ENat
-- Module: Mathlib.Data.ENat.Lattice
Goal:
s : Set ℕ
hs : s.Nonempty
⊢ Eq (α := ℕ∞) (↑(sInf s) : ℕ∞) (⨅ a ∈ s, (↑a : ℕ∞))

Tactic:
WithTop.coe_sInf hs (OrderBot.bddBelow s)

Premises used: ENat, OrderBot.bddBelow, WithTop.coe_sInf
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_1
f : ι → ℕ
⊢ BddAbove (range f) → Eq (α := ℕ∞) (↑(⨆ (i : ι), f i) : ℕ∞) (⨆ (i : ι), (↑(f i) : ℕ∞))

Tactic:
WithTop.coe_iSup _

Premises used: ENat, WithTop.coe_iSup
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_1
f : ι → ℕ
inst : Nonempty ι
⊢ Eq (α := ℕ∞) (↑(⨅ (i : ι), f i) : ℕ∞) (⨅ (i : ι), (↑(f i) : ℕ∞))

Tactic:
WithTop.coe_iInf (OrderBot.bddBelow _)

Premises used: WithTop.coe_iInf, ENat, OrderBot.bddBelow
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_1
f : ι → ℕ
inst : IsEmpty ι
⊢ Eq (α := ℕ∞) (⨅ (i : ι), (↑(f i) : ℕ∞)) ⊤

Tactic:
iInf_coe_eq_top.mpr ‹_›

Premises used: Iff.mpr, ENat.iInf_coe_eq_top
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_1
f : ι → ℕ∞
n : ℕ
pos :
  ∀ (hι : IsEmpty ι),
    Eq (α := ℕ∞) (⨅ (i : ι), f i) (↑n : ℕ∞) ↔ (∃ (i : ι), f i = (↑n : ℕ∞)) ∧ ∀ (i : ι), (↑n : ℕ∞) ≤ f i
neg :
  ∀ (hι : Nonempty ι),
    Eq (α := ℕ∞) (⨅ (i : ι), f i) (↑n : ℕ∞) ↔ (∃ (i : ι), f i = (↑n : ℕ∞)) ∧ ∀ (i : ι), (↑n : ℕ∞) ≤ f i
⊢ Eq (α := ℕ∞) (⨅ (i : ι), f i) (↑n : ℕ∞) ↔ (∃ (i : ι), f i = (↑n : ℕ∞)) ∧ ∀ (i : ι), (↑n : ℕ∞) ≤ f i

Tactic:
by_cases! hι : IsEmpty ι

Premises used: IsEmpty
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_1
f : ι → ℕ∞
n : ℕ
hι : IsEmpty ι
⊢ Eq (α := ℕ∞) (⨅ (i : ι), f i) (↑n : ℕ∞) ↔ (∃ (i : ι), f i = (↑n : ℕ∞)) ∧ ∀ (i : ι), (↑n : ℕ∞) ≤ f i

Tactic:
simp [iInf_of_isEmpty]

Premises used: iInf_of_isEmpty
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_1
f : ι → ℕ∞
n : ℕ
hι : Nonempty ι
⊢ Eq (α := ℕ∞) (⨅ (i : ι), f i) (↑n : ℕ∞) ↔ (∃ (i : ι), f i = (↑n : ℕ∞)) ∧ ∀ (i : ι), (↑n : ℕ∞) ≤ f i

Tactic:
apply ciInf_eq_iff

Premises used: ciInf_eq_iff
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_1
f : ι → ℕ
inl : IsEmpty ι → toNat (⨅ (i : ι), (↑(f i) : ℕ∞)) = ⨅ (i : ι), f i
inr : Nonempty ι → toNat (⨅ (i : ι), (↑(f i) : ℕ∞)) = ⨅ (i : ι), f i
⊢ toNat (⨅ (i : ι), (↑(f i) : ℕ∞)) = ⨅ (i : ι), f i

Tactic:
cases isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_1
f : ι → ℕ
h : IsEmpty ι
⊢ toNat (⨅ (i : ι), (↑(f i) : ℕ∞)) = ⨅ (i : ι), f i

Tactic:
simp
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_1
f : ι → ℕ
h : Nonempty ι
inr inr₁ inr₂ inr₃ : toNat (↑(⨅ (i : ι), f i) : ℕ∞) = ⨅ (i : ι), f i
⊢ toNat (⨅ (i : ι), (↑(f i) : ℕ∞)) = ⨅ (i : ι), f i

Tactic:
norm_cast
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_1
f : ι → ℕ∞
⊢ Eq (α := ℕ∞) (⨅ (i : ι), f i) 0 ↔ ∃ (i : ι), f i = 0

Tactic:
simpa [lt_one_iff_eq_zero] using iInf_lt_iff (α := ℕ∞) (a := 1)

Premises used: iInf_lt_iff, ENat.lt_one_iff_eq_zero
-- Module: Mathlib.Data.ENat.Lattice
Goal:
s : Set ℕ∞
⊢ sSup s = 0 ↔ ∀ a ∈ s, a = 0

Tactic:
sSup_eq_bot

Premises used: sSup_eq_bot, WithTop.some
-- Module: Mathlib.Data.ENat.Lattice
Goal:
s : Set ℕ∞
rw : sInf s < 1 ↔ 0 ∈ s
⊢ sInf s = 0 ↔ 0 ∈ s

Tactic:
rw [← lt_one_iff_eq_zero]

Premises used: ENat.lt_one_iff_eq_zero
-- Module: Mathlib.Data.ENat.Lattice
Goal:
s : Set ℕ∞
⊢ sInf s < 1 ↔ 0 ∈ s

Tactic:
simp only [sInf_lt_iff, lt_one_iff_eq_zero, exists_eq_right]

Premises used: sInf_lt_iff, exists_eq_right, ENat.lt_one_iff_eq_zero
-- Module: Mathlib.Data.ENat.Lattice
Goal:
s : Set ℕ∞
⊢ sSup s = 0 ↔ s = ∅ ∨ s = {0}

Tactic:
sSup_eq_bot'

Premises used: sSup_eq_bot', WithTop.some
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_1
f : ι → ℕ∞
⊢ iSup f = 0 ↔ ∀ (i : ι), f i = 0

Tactic:
iSup_eq_bot

Premises used: WithTop.some, iSup_eq_bot
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_1
⊢ Eq (α := ℕ∞) (⨆ (x : ι), 0) 0

Tactic:
simp
-- Module: Mathlib.Data.ENat.Lattice
Goal:
s : Set ℕ∞
h : s.Infinite
apply : ∀ b < ⊤, ∃ a ∈ s, b < a
⊢ sSup s = ⊤

Tactic:
apply (sSup_eq_top ..).mpr

Premises used: Iff.mpr, sSup_eq_top
-- Module: Mathlib.Data.ENat.Lattice
Goal:
s : Set ℕ∞
h : s.Infinite
hx : LT.lt (α := ℕ∞) ⊤ ⊤
⊢ ∃ a ∈ s, ⊤ < a

Tactic:
simp at hx
-- Module: Mathlib.Data.ENat.Lattice
Goal:
s : Set ℕ∞
h : s.Infinite
x : ℕ
hx : LT.lt (α := ℕ∞) (↑x : ℕ∞) ⊤
coe : ∀ (h : ∀ (a : ℕ∞) (_ : a ∈ s), a ≤ (↑x : ℕ∞)), s.Finite
⊢ ∃ a ∈ s, (↑x : ℕ∞) < a

Tactic:
contrapose! h
-- Module: Mathlib.Data.ENat.Lattice
Goal:
s : Set ℕ∞
x : ℕ
hx : LT.lt (α := ℕ∞) (↑x : ℕ∞) ⊤
h : ∀ (a : ℕ∞) (_ : a ∈ s), a ≤ (↑x : ℕ∞)
coe : s ⊆ (fun (n : ℕ) ↦ (↑n : ℕ∞)) '' {n : ℕ | n ≤ x}
⊢ s.Finite

Tactic:
apply Finite.subset <| Finite.Set.finite_image {n : ℕ | n ≤ x} (fun (n : ℕ) => (n : ℕ∞))

Premises used: Finite.Set.finite_image, setOf, Set.Finite.subset, LE.le, Nat.cast
-- Module: Mathlib.Data.ENat.Lattice
Goal:
s : Set ℕ∞
x : ℕ
hx : LT.lt (α := ℕ∞) (↑x : ℕ∞) ⊤
h : ∀ (a : ℕ∞) (_ : a ∈ s), a ≤ (↑x : ℕ∞)
y : ℕ∞
hy : y ∈ s
⊢ y ≤ (↑x : ℕ∞)

Tactic:
specialize h y hy
-- Module: Mathlib.Data.ENat.Lattice
Goal:
s : Set ℕ∞
x : ℕ
hx : LT.lt (α := ℕ∞) (↑x : ℕ∞) ⊤
y : ℕ∞
hy : y ∈ s
h : y ≤ (↑x : ℕ∞)
⊢ y < ⊤

Tactic:
have hxt : y < ⊤ := lt_of_le_of_lt h hx
-- Module: Mathlib.Data.ENat.Lattice
Goal:
s : Set ℕ∞
x : ℕ
hx : LT.lt (α := ℕ∞) (↑x : ℕ∞) ⊤
y : ℕ∞
hy : y ∈ s
h : y ≤ (↑x : ℕ∞)
hxt : y < ⊤
h₁ : Membership.mem (γ := Set ℕ) {n : ℕ | n ≤ x} y.toNat ∧ (fun (n : ℕ) ↦ ((↑n : ℕ∞) : ℕ∞)) y.toNat = y
⊢ Membership.mem (γ := Set ℕ∞) ((fun (n : ℕ) ↦ (↑n : ℕ∞)) '' {n : ℕ | n ≤ x}) y

Tactic:
use y.toNat

Premises used: ENat.toNat
-- Module: Mathlib.Data.ENat.Lattice
Goal:
s : Set ℕ∞
x : ℕ
hx : LT.lt (α := ℕ∞) (↑x : ℕ∞) ⊤
y : ℕ∞
hy : y ∈ s
h : y ≤ (↑x : ℕ∞)
hxt : y < ⊤
⊢ Membership.mem (γ := Set ℕ) {n : ℕ | n ≤ x} y.toNat ∧ (fun (n : ℕ) ↦ ((↑n : ℕ∞) : ℕ∞)) y.toNat = y

Tactic:
simp [toNat_le_of_le_coe h, LT.lt.ne_top hxt]

Premises used: LT.lt.ne_top, ENat.toNat_le_of_le_coe
-- Module: Mathlib.Data.ENat.Lattice
Goal:
s : Set ℕ∞
h : s.Infinite
x : ℕ∞
hx : x < ⊤
top : ∀ (hx : LT.lt (α := ℕ∞) ⊤ ⊤), ∃ a ∈ s, ⊤ < a
coe : ∀ (x : ℕ) (hx : LT.lt (α := ℕ∞) (↑x : ℕ∞) ⊤), ∃ a ∈ s, (↑x : ℕ∞) < a
⊢ ∃ a ∈ s, x < a

Tactic:
cases x with
  | top => simp at hx
  | coe x =>
    contrapose! h
    apply Finite.subset <| Finite.Set.finite_image {n : ℕ | n ≤ x} (fun (n : ℕ) => (n : ℕ∞))
    intro y hy
    specialize h y hy
    have hxt : y < ⊤ := lt_of_le_of_lt h hx
    use y.toNat
    simp [toNat_le_of_le_coe h, LT.lt.ne_top hxt]

Premises used: Set.Finite.subset, ENat.toNat_le_of_le_coe
-- Module: Mathlib.Data.ENat.Lattice
Goal:
s : Set ℕ∞
h : sSup s < ⊤
contrapose! : ∀ (h : s.Infinite), ⊤ ≤ sSup s
⊢ s.Finite

Tactic:
contrapose! h
-- Module: Mathlib.Data.ENat.Lattice
Goal:
s : Set ℕ∞
h : s.Infinite
simp : sSup s = ⊤
⊢ ⊤ ≤ sSup s

Tactic:
simp only [top_le_iff]

Premises used: top_le_iff
-- Module: Mathlib.Data.ENat.Lattice
Goal:
s : Set ℕ∞
h : s.Infinite
⊢ sSup s = ⊤

Tactic:
sSup_eq_top_of_infinite h

Premises used: ENat.sSup_eq_top_of_infinite
-- Module: Mathlib.Data.ENat.Lattice
Goal:
s : Set ℕ∞
h : s.Infinite
⊢ sSup s = ⊤

Tactic:
exact sSup_eq_top_of_infinite h

Premises used: ENat.sSup_eq_top_of_infinite
-- Module: Mathlib.Data.ENat.Lattice
Goal:
s : Set ℕ∞
inst : Nonempty (↑s : Type)
hs' : sSup s < ⊤
⊢ sSup s ∈ s

Tactic:
Nonempty.csSup_mem .of_subtype (finite_of_sSup_lt_top hs')

Premises used: Set.Nonempty.of_subtype, ENat.finite_of_sSup_lt_top, Set.Nonempty.csSup_mem
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_1
f : ι → ℕ∞
inst : Nonempty ι
h : LT.lt (α := ℕ∞) (⨆ (i : ι), f i) ⊤
⊢ ∃ (i : ι), f i = ⨆ (i : ι), f i

Tactic:
sSup_mem_of_nonempty_of_lt_top h

Premises used: Set.Mem, iSup, setOf, Set.range, ENat.sSup_mem_of_nonempty_of_lt_top
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_1
inst : Nonempty ι
f : ι → ℕ∞
⊢ ∃ (a : ι), f a = ⨅ (x : ι), f x

Tactic:
csInf_mem (range_nonempty fun i ↦ f i)

Premises used: csInf_mem, iInf, Set.Mem, setOf, Set.range_nonempty, Set.range
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ι₂ → ℕ∞
inst : Nonempty ι₁
inst_1 : Nonempty ι₂
h : LT.lt (α := ℕ∞) (⨆ (i : ι₁), ⨆ (j : ι₂), f i j) ⊤
rw : ∀ (h : LT.lt (α := ℕ∞) (⨆ (x : ι₁ × ι₂), f x.1 x.2) ⊤), ∃ (i : ι₁) (j : ι₂), f i j = ⨆ (x : ι₁ × ι₂), f x.1 x.2
⊢ ∃ (i : ι₁) (j : ι₂), f i j = ⨆ (i : ι₁), ⨆ (j : ι₂), f i j

Tactic:
rw [iSup_prod'] at h ⊢

Premises used: iSup_prod'
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ι₂ → ℕ∞
inst : Nonempty ι₁
inst_1 : Nonempty ι₂
h : LT.lt (α := ℕ∞) (⨆ (x : ι₁ × ι₂), f x.1 x.2) ⊤
⊢ ∃ (i : ι₁) (j : ι₂), f i j = ⨆ (x : ι₁ × ι₂), f x.1 x.2

Tactic:
Prod.exists'.mp (exists_eq_iSup_of_lt_top h)

Premises used: ENat.exists_eq_iSup_of_lt_top, Prod.exists', Iff.mp
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ι₂ → ℕ∞
inst : Nonempty ι₁
inst_1 : Nonempty ι₂
h : LT.lt (α := ℕ∞) (⨆ (x : ι₁ × ι₂), f x.1 x.2) ⊤
⊢ ∃ (i : ι₁) (j : ι₂), f i j = ⨆ (x : ι₁ × ι₂), f x.1 x.2

Tactic:
exact Prod.exists'.mp (exists_eq_iSup_of_lt_top h)

Premises used: Prod.exists', Iff.mp
-- Module: Mathlib.Data.ENat.Lattice
Goal:
⊢ Eq (α := ℕ∞) (⨆ (n : ℕ), (↑n : ℕ∞)) ⊤

Tactic:
iSup_eq_top.2 fun _b hb ↦ ENat.exists_nat_gt (lt_top_iff_ne_top.1 hb)

Premises used: Iff.mpr, iSup_eq_top, lt_top_iff_ne_top, Iff.mp, ENat.exists_nat_gt
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
a : ℕ∞
f : ι → ℕ∞
⊢ a * ⨆ (i : ι), f i = ⨆ (i : ι), a * f i

Tactic:
(iSup_le fun i ↦ mul_le_mul' rfl.le <| le_iSup_iff.2 fun _ a ↦ a i).antisymm' <|
    le_iSup_iff.2 fun d h ↦ ?_

Premises used: Iff.mpr, LE.le.antisymm', Eq.le, iSup_le, le_iSup_iff, mul_le_mul', rfl
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
a : ℕ∞
f : ι → ℕ∞
refine : ∀ (d : ℕ∞) (h : ∀ (i : ι), a * f i ≤ d), a * ⨆ (i : ι), f i ≤ d
⊢ a * ⨆ (i : ι), f i = ⨆ (i : ι), a * f i

Tactic:
refine (iSup_le fun i ↦ mul_le_mul' rfl.le <| le_iSup_iff.2 fun _ a ↦ a i).antisymm' <|
    le_iSup_iff.2 fun d h ↦ ?_

Premises used: Iff.mpr, LE.le.antisymm', Eq.le, iSup_le, le_iSup_iff, mul_le_mul', rfl
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
a : ℕ∞
f : ι → ℕ∞
d : ℕ∞
h : ∀ (i : ι), a * f i ≤ d
inl : ∀ (h : ∀ (i : ι), 0 * f i ≤ d), HMul.hMul (α := ℕ∞) 0 (⨆ (i : ι), f i) ≤ d
inr : ∀ (hne : a ≠ 0), a * ⨆ (i : ι), f i ≤ d
⊢ a * ⨆ (i : ι), f i ≤ d

Tactic:
obtain rfl | hne := eq_or_ne a 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
f : ι → ℕ∞
d : ℕ∞
h : ∀ (i : ι), 0 * f i ≤ d
⊢ HMul.hMul (α := ℕ∞) 0 (⨆ (i : ι), f i) ≤ d

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

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

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Data.ENat.Lattice
Goal:
ι : Sort u_2
a : ℕ∞
f : ι → ℕ∞
d : ℕ∞
h : ∀ (i : ι), a * f i ≤ d
hne : a ≠ 0
hι : IsEmpty ι
⊢ a * ⨆ (i : ι), f i ≤ d

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

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

Tactic:
rw [lt_top_iff_ne_top]

Premises used: lt_top_iff_ne_top
-- 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) ⊤
⊢ LT.lt (α := ℕ∞) (↑d : ℕ∞) ⊤

Tactic:
simp
-- 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) ⊤
obtain : ∀ (i : ι) (hi : (↑d : ℕ∞) < f i), False
⊢ False

Tactic:
obtain ⟨i, hi : d < f i⟩ := (iSup_eq_top ..).1 htop d (by simp)

Premises used: iSup_eq_top, Nat.cast, Iff.mp
-- 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:
(((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