awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.ENat.BigOperators (goal)
Goal:
ι : Type u_2
α : Type u_3
f : ι → α → ℕ∞
inst : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ (k : ι), ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a
a : α
s : Finset α
ha : a ∉ s
ih : Eq (α := ℕ∞) (⨅ (i : ι), ∑ a ∈ s, f i a) (∑ a ∈ s, ⨅ (i : ι), f i a)
⊢ ⨅ (i : ι), f i a + ∑ a ∈ s, f i a = HAdd.hAdd (α := ℕ∞) (⨅ (i : ι), f i a) (⨅ (i : ι), ∑ a ∈ s, f i a)
have cons : ∀ (i j : ι), ∃ (k : ι), f k a + ∑ a ∈ s, f k a ≤ f i a + ∑ a ∈ s, f j a
Tactic: refine (iInf_add_iInf fun i j => ?_).symm
-- Lean 4 proof step from Mathlib.Data.ENat.BigOperators (goal)
Goal:
ι : Type u_2
α : Type u_3
f : ι → α → ℕ∞
inst : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ (k : ι), ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a
a : α
s : Finset α
ha : a ∉ s
ih : Eq (α := ℕ∞) (⨅ (i : ι), ∑ a ∈ s, f i a) (∑ a ∈ s, ⨅ (i : ι), f i a)
i j : ι
⊢ ∃ (k : ι), f k a + ∑ a ∈ s, f k a ≤ f i a + ∑ a ∈ s, f j a
have cons : ∀ (k : ι) (hk : ∀ a_1 ∈ Finset.cons a s ha, f k a_1 ≤ f i a_1 ∧ f k a_1 ≤ f j a_1),
  f k a + ∑ a ∈ s, f k a ≤ f i a + ∑ a ∈ s, f j a
Tactic: refine (h (Finset.cons a s ha) i j).imp fun k hk => ?_
-- Lean 4 proof step from Mathlib.Data.ENat.BigOperators (hypothesis)
Goal:
ι : Type u_2
α : Type u_3
f : ι → α → ℕ∞
inst : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ (k : ι), ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a
a : α
s : Finset α
ha : a ∉ s
ih : Eq (α := ℕ∞) (⨅ (i : ι), ∑ a ∈ s, f i a) (∑ a ∈ s, ⨅ (i : ι), f i a)
i j k : ι
hk : ∀ a_1 ∈ Finset.cons a s ha, f k a_1 ≤ f i a_1 ∧ f k a_1 ≤ f j a_1
⊢ f k a + ∑ a ∈ s, f k a ≤ f i a + ∑ a ∈ s, f j a
have hk₁ : (f k a ≤ f i a ∧ f k a ≤ f j a) ∧ ∀ x ∈ s, f k x ≤ f i x ∧ f k x ≤ f j x
Tactic: rw [Finset.forall_mem_cons] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Data.ENat.BigOperators (goal)
Goal:
ι : Type u_2
α : Type u_3
f : ι → α → ℕ∞
s : Finset α
inst : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ (k : ι), ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a
⊢ Eq (α := ℕ∞) (⨅ (i : ι), ∑ a ∈ s, f i a) (∑ a ∈ s, ⨅ (i : ι), f i a)
have empty : Eq (α := ℕ∞) (⨅ (i : ι), ∑ a ∈ ∅, f i a) (∑ a ∈ ∅, ⨅ (i : ι), f i a)
Tactic: induction s using Finset.cons_induction_on with
  | empty => simp only [Finset.sum_empty, ciInf_const]
  | cons a s ha ih =>
    simp only [Finset.sum_cons, ← ih]
    refine (iInf_add_iInf fun i j => ?_).symm
    refine (h (Finset.cons a s ha) i j).imp fun k hk => ?_
    rw [Finset.forall_mem_cons] at hk
    exact add_le_add hk.1.1 (Finset.sum_le_sum fun a ha => (hk.2 a ha).2)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.ENat.BigOperators (goal)
Goal:
ι : Type u_2
α : Type u_3
f : ι → α → ℕ∞
s : Finset α
inst : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ (k : ι), ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a
empty : Eq (α := ℕ∞) (⨅ (i : ι), ∑ a ∈ ∅, f i a) (∑ a ∈ ∅, ⨅ (i : ι), f i a)
⊢ Eq (α := ℕ∞) (⨅ (i : ι), ∑ a ∈ s, f i a) (∑ a ∈ s, ⨅ (i : ι), f i a)
have cons : ∀ (a : α) (s : Finset α) (ha : a ∉ s) (ih : Eq (α := ℕ∞) (⨅ (i : ι), ∑ a ∈ s, f i a) (∑ a ∈ s, ⨅ (i : ι), f i a)),
  Eq (α := ℕ∞) (⨅ (i : ι), ∑ a ∈ Finset.cons a s ha, f i a) (∑ a ∈ Finset.cons a s ha, ⨅ (i : ι), f i a)
Tactic: induction s using Finset.cons_induction_on with
  | empty => simp only [Finset.sum_empty, ciInf_const]
  | cons a s ha ih =>
    simp only [Finset.sum_cons, ← ih]
    refine (iInf_add_iInf fun i j => ?_).symm
    refine (h (Finset.cons a s ha) i j).imp fun k hk => ?_
    rw [Finset.forall_mem_cons] at hk
    exact add_le_add hk.1.1 (Finset.sum_le_sum fun a ha => (hk.2 a ha).2)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.ENat.BigOperators (goal)
Goal:
α : Type u_1
s : Finset α
f : α → ℕ∞
hf : ∀ a ∈ s, f a ≠ ⊤
⊢ toNat (∑ a ∈ s, f a) = ∑ a ∈ s, (f a).toNat
have rw : Eq (α := ℕ∞) (∑ a ∈ s, f a) (∑ x ∈ s, (↑(f x).toNat : ℕ∞))
Tactic: rw [← coe_inj, coe_toNat (sum_ne_top.2 hf), Nat.cast_sum]
-- Lean 4 proof step from Mathlib.Data.ENat.BigOperators (goal)
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 ∈ cons a s_1 h, f i < g i
⊢ LT.lt (α := ℕ∞) (∑ i ∈ cons a s_1 h, f i) (∑ i ∈ cons a s_1 h, g i)
have 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
Tactic: simp only [sum_cons, forall_mem_cons] at Hlt ⊢
Cleared hypotheses: Hlt
-- Lean 4 proof step from Mathlib.Data.ENat.BigOperators (goal)
Goal:
α : Type u_1
s : Finset α
hs : s.Nonempty
f g : α → ℕ∞
Hlt : ∀ i ∈ s, f i < g i
⊢ LT.lt (α := ℕ∞) (∑ i ∈ s, f i) (∑ i ∈ s, g i)
have singleton : ∀ (a : α) (Hlt : ∀ (i : α), Membership.mem (γ := Finset α) {a} i → f i < g i),
  LT.lt (α := ℕ∞) (∑ i ∈ {a}, f i) (∑ i ∈ {a}, 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)
Cleared hypotheses: hs, Hlt
-- Lean 4 proof step from Mathlib.Data.ENat.BigOperators (goal)
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)
⊢ LT.lt (α := ℕ∞) (∑ i ∈ s, f i) (∑ i ∈ s, g i)
have 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 ∈ cons a s h, f i < g i), LT.lt (α := ℕ∞) (∑ i ∈ cons a s h, f i) (∑ i ∈ cons a s h, 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)
Cleared hypotheses: hs, Hlt
-- Lean 4 proof step from Mathlib.Data.ENat.BigOperators (goal)
Goal:
α : Type u_1
s : Finset α
hs : s.Nonempty
f g : α → ℕ∞
Hle : LE.le (α := ℕ∞) (∑ i ∈ s, f i) (∑ i ∈ s, g i)
⊢ ∃ i ∈ s, f i ≤ g i
have contrapose! : ∀ (Hle : ∀ (i : α) (_ : i ∈ s), g i < f i), LT.lt (α := ℕ∞) (∑ i ∈ s, g i) (∑ i ∈ s, f i)
Tactic: contrapose! Hle
Cleared hypotheses: Hle
-- Lean 4 proof step from Mathlib.Data.ENat.BigOperators (goal)
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)
⊢ Eq (α := ℕ∞) (∑ a ∈ Finset.cons a s ha, ⨆ (i : ι), f a i) (⨆ (i : ι), ∑ a ∈ Finset.cons a s ha, f a i)
have cons : HAdd.hAdd (α := ℕ∞) (⨆ (i : ι), f a i) (⨆ (i : ι), ∑ a ∈ s, f a i) = ⨆ (i : ι), f a i + ∑ a ∈ s, f a i
Tactic: simp_rw [Finset.sum_cons, ihs]
-- Lean 4 proof step from Mathlib.Data.ENat.BigOperators (goal)
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
have 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
Tactic: refine iSup_add_iSup fun i j ↦ (hf i j).imp fun k hk ↦ ?_
-- Lean 4 proof step from Mathlib.Data.ENat.BigOperators (goal)
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 + ∑ a ∈ s, f a j ≤ f a k + ∑ a ∈ s, f a k
have cons : f a i ≤ f a k
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Data.ENat.BigOperators (goal)
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
⊢ f a i + ∑ a ∈ s, f a j ≤ f a k + ∑ a ∈ s, f a k
have cons₁ : ∀ i ∈ s, f i j ≤ f i k
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Data.ENat.BigOperators (goal)
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
⊢ Eq (α := ℕ∞) (∑ a ∈ s, ⨆ (i : ι), f a i) (⨆ (i : ι), ∑ a ∈ s, f a i)
have empty : Eq (α := ℕ∞) (∑ a ∈ ∅, ⨆ (i : ι), f a i) (⨆ (i : ι), ∑ a ∈ ∅, 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]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.ENat.BigOperators (goal)
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)
⊢ Eq (α := ℕ∞) (∑ a ∈ s, ⨆ (i : ι), f a i) (⨆ (i : ι), ∑ a ∈ s, f a i)
have 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)
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]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_1
f : ι → ℕ
⊢ Ne (α := ℕ∞) (⨅ (i : ι), (↑(f i) : ℕ∞)) ⊤ ↔ Nonempty ι
have rw : ¬Eq (α := ℕ∞) (⨅ (i : ι), (↑(f i) : ℕ∞)) ⊤ ↔ Nonempty ι
Tactic: rw [Ne, iInf_coe_eq_top, not_isEmpty_iff]
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_1
f : ι → ℕ
rw : ¬Eq (α := ℕ∞) (⨅ (i : ι), (↑(f i) : ℕ∞)) ⊤ ↔ Nonempty ι
⊢ Ne (α := ℕ∞) (⨅ (i : ι), (↑(f i) : ℕ∞)) ⊤ ↔ Nonempty ι
have rw₁ : ¬IsEmpty ι ↔ Nonempty ι
Tactic: rw [Ne, iInf_coe_eq_top, not_isEmpty_iff]
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_1
f : ι → ℕ
rw : ¬Eq (α := ℕ∞) (⨅ (i : ι), (↑(f i) : ℕ∞)) ⊤ ↔ Nonempty ι
rw₁ : ¬IsEmpty ι ↔ Nonempty ι
⊢ Ne (α := ℕ∞) (⨅ (i : ι), (↑(f i) : ℕ∞)) ⊤ ↔ Nonempty ι
have rw₂ : Nonempty ι ↔ Nonempty ι
Tactic: rw [Ne, iInf_coe_eq_top, not_isEmpty_iff]
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_1
f : ι → ℕ∞
n : ℕ
⊢ Eq (α := ℕ∞) (⨅ (i : ι), f i) (↑n : ℕ∞) ↔ (∃ (i : ι), f i = (↑n : ℕ∞)) ∧ ∀ (i : ι), (↑n : ℕ∞) ≤ f i
have pos : ∀ (hι : IsEmpty ι), Eq (α := ℕ∞) (⨅ (i : ι), f i) (↑n : ℕ∞) ↔ (∃ (i : ι), f i = (↑n : ℕ∞)) ∧ ∀ (i : ι), (↑n : ℕ∞) ≤ f i
Tactic: by_cases! hι : IsEmpty ι
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_1
f : ι → ℕ∞
n : ℕ
pos :
  ∀ (hι : IsEmpty ι),
    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
have neg : ∀ (hι : Nonempty ι), Eq (α := ℕ∞) (⨅ (i : ι), f i) (↑n : ℕ∞) ↔ (∃ (i : ι), f i = (↑n : ℕ∞)) ∧ ∀ (i : ι), (↑n : ℕ∞) ≤ f i
Tactic: by_cases! hι : IsEmpty ι
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_1
f : ι → ℕ
⊢ toNat (⨅ (i : ι), (↑(f i) : ℕ∞)) = ⨅ (i : ι), f i
have inl : IsEmpty ι → toNat (⨅ (i : ι), (↑(f i) : ℕ∞)) = ⨅ (i : ι), f i
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_1
f : ι → ℕ
inl : IsEmpty ι → toNat (⨅ (i : ι), (↑(f i) : ℕ∞)) = ⨅ (i : ι), f i
⊢ toNat (⨅ (i : ι), (↑(f i) : ℕ∞)) = ⨅ (i : ι), f i
have inr : Nonempty ι → toNat (⨅ (i : ι), (↑(f i) : ℕ∞)) = ⨅ (i : ι), f i
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_1
f : ι → ℕ
h : Nonempty ι
⊢ toNat (⨅ (i : ι), (↑(f i) : ℕ∞)) = ⨅ (i : ι), f i
have inr : toNat (↑(⨅ (i : ι), f i) : ℕ∞) = ⨅ (i : ι), f i
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
s : Set ℕ∞
⊢ sInf s = 0 ↔ 0 ∈ s
have rw : sInf s < 1 ↔ 0 ∈ s
Tactic: rw [← lt_one_iff_eq_zero]
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
s : Set ℕ∞
h : s.Infinite
⊢ sSup s = ⊤
have apply : ∀ b < ⊤, ∃ a ∈ s, b < a
Tactic: apply (sSup_eq_top ..).mpr
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
s : Set ℕ∞
h : s.Infinite
x : ℕ
hx : LT.lt (α := ℕ∞) (↑x : ℕ∞) ⊤
⊢ ∃ a ∈ s, (↑x : ℕ∞) < a
have coe : ∀ (h : ∀ (a : ℕ∞) (_ : a ∈ s), a ≤ (↑x : ℕ∞)), s.Finite
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
s : Set ℕ∞
x : ℕ
hx : LT.lt (α := ℕ∞) (↑x : ℕ∞) ⊤
h : ∀ (a : ℕ∞) (_ : a ∈ s), a ≤ (↑x : ℕ∞)
⊢ s.Finite
have coe : s ⊆ (fun (n : ℕ) ↦ (↑n : ℕ∞)) '' {n : ℕ | n ≤ x}
Tactic: apply Finite.subset <| Finite.Set.finite_image {n : ℕ | n ≤ x} (fun (n : ℕ) => (n : ℕ∞))
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (hypothesis)
Goal:
s : Set ℕ∞
x : ℕ
hx : LT.lt (α := ℕ∞) (↑x : ℕ∞) ⊤
h : ∀ (a : ℕ∞) (_ : a ∈ s), a ≤ (↑x : ℕ∞)
y : ℕ∞
hy : y ∈ s
⊢ Membership.mem (γ := Set ℕ∞) ((fun (n : ℕ) ↦ (↑n : ℕ∞)) '' {n : ℕ | n ≤ x}) y
have h₁ : y ≤ (↑x : ℕ∞)
Tactic: specialize h y hy
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (hypothesis)
Goal:
s : Set ℕ∞
x : ℕ
hx : LT.lt (α := ℕ∞) (↑x : ℕ∞) ⊤
y : ℕ∞
hy : y ∈ s
h : y ≤ (↑x : ℕ∞)
⊢ Membership.mem (γ := Set ℕ∞) ((fun (n : ℕ) ↦ (↑n : ℕ∞)) '' {n : ℕ | n ≤ x}) y
have hxt : y < ⊤
Tactic: have hxt : y < ⊤ := lt_of_le_of_lt h hx
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
s : Set ℕ∞
x : ℕ
hx : LT.lt (α := ℕ∞) (↑x : ℕ∞) ⊤
y : ℕ∞
hy : y ∈ s
h : y ≤ (↑x : ℕ∞)
hxt : y < ⊤
⊢ Membership.mem (γ := Set ℕ∞) ((fun (n : ℕ) ↦ (↑n : ℕ∞)) '' {n : ℕ | n ≤ x}) y
have h₁ : Membership.mem (γ := Set ℕ) {n : ℕ | n ≤ x} y.toNat ∧ (fun (n : ℕ) ↦ ((↑n : ℕ∞) : ℕ∞)) y.toNat = y
Tactic: use y.toNat
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
s : Set ℕ∞
h : s.Infinite
x : ℕ∞
hx : x < ⊤
⊢ ∃ a ∈ s, x < a
have top : ∀ (hx : LT.lt (α := ℕ∞) ⊤ ⊤), ∃ a ∈ s, ⊤ < 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]
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
s : Set ℕ∞
h : s.Infinite
x : ℕ∞
hx : x < ⊤
top : ∀ (hx : LT.lt (α := ℕ∞) ⊤ ⊤), ∃ a ∈ s, ⊤ < a
⊢ ∃ a ∈ s, x < a
have coe : ∀ (x : ℕ) (hx : LT.lt (α := ℕ∞) (↑x : ℕ∞) ⊤), ∃ 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]
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
s : Set ℕ∞
h : sSup s < ⊤
⊢ s.Finite
have contrapose! : ∀ (h : s.Infinite), ⊤ ≤ sSup s
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
s : Set ℕ∞
h : s.Infinite
⊢ ⊤ ≤ sSup s
have simp : sSup s = ⊤
Tactic: simp only [top_le_iff]
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ι₂ → ℕ∞
inst : Nonempty ι₁
inst_1 : Nonempty ι₂
h : LT.lt (α := ℕ∞) (⨆ (i : ι₁), ⨆ (j : ι₂), f i j) ⊤
⊢ ∃ (i : ι₁) (j : ι₂), f i j = ⨆ (i : ι₁), ⨆ (j : ι₂), f i j
have rw : ∀ (h : LT.lt (α := ℕ∞) (⨆ (x : ι₁ × ι₂), f x.1 x.2) ⊤), ∃ (i : ι₁) (j : ι₂), f i j = ⨆ (x : ι₁ × ι₂), f x.1 x.2
Tactic: rw [iSup_prod'] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_2
a : ℕ∞
f : ι → ℕ∞
⊢ a * ⨆ (i : ι), f i = ⨆ (i : ι), a * f i
have refine : ∀ (d : ℕ∞) (h : ∀ (i : ι), a * f i ≤ d), a * ⨆ (i : ι), f i ≤ d
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 ↦ ?_
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_2
a : ℕ∞
f : ι → ℕ∞
d : ℕ∞
h : ∀ (i : ι), a * f i ≤ d
⊢ a * ⨆ (i : ι), f i ≤ d
have inl : ∀ (h : ∀ (i : ι), 0 * f i ≤ d), HMul.hMul (α := ℕ∞) 0 (⨆ (i : ι), f i) ≤ d
Tactic: obtain rfl | hne := eq_or_ne a 0
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
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
⊢ a * ⨆ (i : ι), f i ≤ d
have inr : ∀ (hne : a ≠ 0), a * ⨆ (i : ι), f i ≤ d
Tactic: obtain rfl | hne := eq_or_ne a 0
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_2
a : ℕ∞
f : ι → ℕ∞
d : ℕ∞
h : ∀ (i : ι), a * f i ≤ d
hne : a ≠ 0
⊢ a * ⨆ (i : ι), f i ≤ d
have inr : ∀ (hι : IsEmpty ι), a * ⨆ (i : ι), f i ≤ d
Tactic: obtain hι | hι := isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_2
a : ℕ∞
f : ι → ℕ∞
d : ℕ∞
h : ∀ (i : ι), a * f i ≤ d
hne : a ≠ 0
inr : ∀ (hι : IsEmpty ι), a * ⨆ (i : ι), f i ≤ d
⊢ a * ⨆ (i : ι), f i ≤ d
have inr₁ : ∀ (hι : Nonempty ι), a * ⨆ (i : ι), f i ≤ d
Tactic: obtain hι | hι := isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_2
a : ℕ∞
f : ι → ℕ∞
hne : a ≠ 0
hι : Nonempty ι
d : ℕ
h : ∀ (i : ι), a * f i ≤ (↑d : ℕ∞)
⊢ LT.lt (α := ℕ∞) (⨆ (i : ι), f i) ⊤
have rw : Ne (α := ℕ∞) (⨆ (i : ι), f i) ⊤
Tactic: rw [lt_top_iff_ne_top]
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_2
a : ℕ∞
f : ι → ℕ∞
hne : a ≠ 0
hι : Nonempty ι
d : ℕ
h : ∀ (i : ι), a * f i ≤ (↑d : ℕ∞)
htop : Eq (α := ℕ∞) (⨆ (i : ι), f i) ⊤
⊢ False
have obtain : ∀ (i : ι) (hi : (↑d : ℕ∞) < f i), False
Tactic: obtain ⟨i, hi : d < f i⟩ := (iSup_eq_top ..).1 htop d (by simp)
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (hypothesis)
Goal:
ι : Sort u_2
a : ℕ∞
f : ι → ℕ∞
hne : a ≠ 0
hι : Nonempty ι
d : ℕ
h : ∀ (i : ι), a * f i ≤ (↑d : ℕ∞)
⊢ a * ⨆ (i : ι), f i ≤ (↑d : ℕ∞)
have hlt : 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
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_2
a : ℕ∞
f : ι → ℕ∞
hne : a ≠ 0
hι : Nonempty ι
d : ℕ
h : ∀ (i : ι), a * f i ≤ (↑d : ℕ∞)
hlt : LT.lt (α := ℕ∞) (⨆ (i : ι), f i) ⊤
⊢ a * ⨆ (i : ι), f i ≤ (↑d : ℕ∞)
have inr : ∀ (j : ι) (hj : f j = ⨆ (i : ι), f i), a * ⨆ (i : ι), f i ≤ (↑d : ℕ∞)
Tactic: obtain ⟨j, hj⟩ := exists_eq_iSup_of_lt_top hlt
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
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 * ⨆ (i : ι), f i ≤ (↑d : ℕ∞)
have inr : a * f j ≤ (↑d : ℕ∞)
Tactic: rw [← hj]
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_2
a : ℕ∞
f : ι → ℕ∞
d : ℕ∞
h : ∀ (i : ι), a * f i ≤ d
hne : a ≠ 0
hι : Nonempty ι
⊢ a * ⨆ (i : ι), f i ≤ d
have inr : ∀ (h : ∀ (i : ι), a * f i ≤ ⊤), a * ⨆ (i : ι), f i ≤ ⊤
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
Cleared hypotheses: d, h
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
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 ≤ ⊤
⊢ a * ⨆ (i : ι), f i ≤ d
have inr₁ : ∀ (d : ℕ) (h : ∀ (i : ι), a * 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
Cleared hypotheses: d, h
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
⊢ (⨆ (i : ι), f i) * a = ⨆ (i : ι), f i * a
have simp_rw : a * ⨆ (i : ι), f i = ⨆ (i : ι), a * f i
Tactic: simp_rw [mul_comm, ENat.mul_iSup]
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
s : Set ℕ∞
a : ℕ∞
⊢ a * sSup s = ⨆ b ∈ s, a * b
have simp_rw : a * ⨆ a ∈ s, a = ⨆ b ∈ s, a * b
Tactic: simp_rw [sSup_eq_iSup, mul_iSup]
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
s : Set ℕ∞
a : ℕ∞
⊢ sSup s * a = ⨆ b ∈ s, b * a
have simp_rw : a * sSup s = ⨆ b ∈ s, a * b
Tactic: simp_rw [mul_comm, mul_sSup]
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst : Nonempty ι
x : ι
⊢ a * ⨅ (i : ι), f i ≤ a * f x
have grw : a * f x ≤ a * f x
Tactic: grw [iInf_le]
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst : Nonempty ι
⊢ a * ⨅ (i : ι), f i = ⨅ (i : ι), a * f i
have refine : ⨅ (i : ι), a * f i ≤ a * ⨅ (i : ι), f i
Tactic: refine (le_iInf fun x ↦ by grw [iInf_le]).antisymm ?_
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst : Nonempty ι
⊢ ⨅ (i : ι), a * f i ≤ a * ⨅ (i : ι), f i
have obtain : ∀ (b : ι) (hb : f b = ⨅ (x : ι), f x), ⨅ (i : ι), a * f i ≤ a * ⨅ (i : ι), f i
Tactic: obtain ⟨b, hb⟩ := ENat.exists_eq_iInf f
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst : Nonempty ι
b : ι
hb : f b = ⨅ (x : ι), f x
⊢ ⨅ (i : ι), a * f i ≤ a * ⨅ (i : ι), f i
have rw : ∀ (b_1 : ℕ∞), (∀ (i : ι), b_1 ≤ a * f i) → b_1 ≤ a * f b
Tactic: rw [← hb, iInf_le_iff]
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst : Nonempty ι
⊢ (⨅ (i : ι), f i) * a = ⨅ (i : ι), f i * a
have simp_rw : a * ⨅ (i : ι), f i = ⨅ (i : ι), a * f i
Tactic: simp_rw [mul_comm, mul_iInf]
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
h₀ : a = 0 → Nonempty ι
⊢ a * ⨅ (i : ι), f i = ⨅ (i : ι), a * f i
have inl : ∀ (hι : IsEmpty ι), a * ⨅ (i : ι), f i = ⨅ (i : ι), a * f i
Tactic: obtain hι | hι := isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
h₀ : a = 0 → Nonempty ι
inl : ∀ (hι : IsEmpty ι), a * ⨅ (i : ι), f i = ⨅ (i : ι), a * f i
⊢ a * ⨅ (i : ι), f i = ⨅ (i : ι), a * f i
have inr : ∀ (hι : Nonempty ι), a * ⨅ (i : ι), f i = ⨅ (i : ι), a * f i
Tactic: obtain hι | hι := isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
h₀ : a = 0 → Nonempty ι
hι : IsEmpty ι
⊢ a * ⨅ (i : ι), f i = ⨅ (i : ι), a * f i
have inl : a ≠ 0
Tactic: suffices a ≠ 0 by simpa [iInf_of_empty, ite_eq_right_iff, mul_top']
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
h₀ : a = 0 → Nonempty ι
hι : Nonempty ι
⊢ a * ⨅ (i : ι), f i = ⨅ (i : ι), a * f i
have inr : Eq (α := ℕ∞) (⨅ (i : ι), a * f i) (⨅ (i : ι), a * f i)
Tactic: rw [mul_iInf]
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
h₀ : a = 0 → Nonempty ι
⊢ (⨅ (i : ι), f i) * a = ⨅ (i : ι), f i * a
have simp_rw : a * ⨅ (i : ι), f i = ⨅ (i : ι), a * f i
Tactic: simp_rw [mul_comm, mul_iInf' h₀]
-- Lean 4 proof step from Mathlib.Data.ENat.Lattice (goal)
Goal:
ι : Sort u_2
a : ℕ∞
inst : Nonempty ι
f : ι → ℕ∞
⊢ a + ⨆ (i : ι), f i = ⨆ (i : ι), a + f i
have inl : HAdd.hAdd (α := ℕ∞) ⊤ (⨆ (i : ι), f i) = ⨆ (i : ι), ⊤ + f i
Tactic: obtain rfl | ha := eq_or_ne a ⊤
Cleared hypotheses: a