awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : Preorder α
inst_1 : Nonempty ι
inst_2 : InfSet α
f : ι → α
hf : BddBelow (range f)
rw : Eq.{u_1 + 1} (α := WithTop α) (↑(sInf (range fun (i : ι) ↦ f i)) : WithTop α) (⨅ (i : ι), (↑(f i) : WithTop α))
rw₁ :
  Eq.{u_1 + 1} (α := WithTop α) (↑(sInf (range fun (i : ι) ↦ f i)) : WithTop α)
    (sInf (range fun (i : ι) ↦ (↑(f i) : WithTop α)))
rw₂ :
  Eq (α := WithTop α) (sInf ((fun (a : α) ↦ (↑a : WithTop α)) '' range f))
    (sInf (range fun (i : ι) ↦ (↑(f i) : WithTop α)))
⊢ Eq.{u_1 + 1} (α := WithTop α) (↑(⨅ (i : ι), f i) : WithTop α) (⨅ (i : ι), (↑(f i) : WithTop α))
have rw₃ : Eq (α := WithTop α) (sInf (range ((fun (a : α) ↦ (↑a : WithTop α)) ∘ f)))
  (sInf (range fun (i : ι) ↦ (↑(f i) : WithTop α)))
Tactic: rw [iInf, iInf, WithTop.coe_sInf' (range_nonempty f) hf, ← range_comp, Function.comp_def]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : Preorder α
inst_1 : Nonempty ι
inst_2 : InfSet α
f : ι → α
hf : BddBelow (range f)
rw : Eq.{u_1 + 1} (α := WithTop α) (↑(sInf (range fun (i : ι) ↦ f i)) : WithTop α) (⨅ (i : ι), (↑(f i) : WithTop α))
rw₁ :
  Eq.{u_1 + 1} (α := WithTop α) (↑(sInf (range fun (i : ι) ↦ f i)) : WithTop α)
    (sInf (range fun (i : ι) ↦ (↑(f i) : WithTop α)))
rw₂ :
  Eq (α := WithTop α) (sInf ((fun (a : α) ↦ (↑a : WithTop α)) '' range f))
    (sInf (range fun (i : ι) ↦ (↑(f i) : WithTop α)))
rw₃ :
  Eq (α := WithTop α) (sInf (range ((fun (a : α) ↦ (↑a : WithTop α)) ∘ f)))
    (sInf (range fun (i : ι) ↦ (↑(f i) : WithTop α)))
⊢ Eq.{u_1 + 1} (α := WithTop α) (↑(⨅ (i : ι), f i) : WithTop α) (⨅ (i : ι), (↑(f i) : WithTop α))
have rw₄ : Eq.{u_1 + 1} (α := WithTop α) (sInf (range fun (x : ι) ↦ (↑(f x) : WithTop α)))
  (sInf (range fun (i : ι) ↦ (↑(f i) : WithTop α)))
Tactic: rw [iInf, iInf, WithTop.coe_sInf' (range_nonempty f) hf, ← range_comp, Function.comp_def]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : Preorder α
inst_1 : SupSet α
f : ι → α
h : BddAbove (range f)
⊢ Eq.{u_1 + 1} (α := WithTop α) (↑(⨆ (i : ι), f i) : WithTop α) (⨆ (i : ι), (↑(f i) : WithTop α))
have rw : Eq.{u_1 + 1} (α := WithTop α) (↑(sSup (range fun (i : ι) ↦ f i)) : WithTop α) (⨆ (i : ι), (↑(f i) : WithTop α))
Tactic: rw [iSup, iSup, WithTop.coe_sSup' h, ← range_comp, Function.comp_def]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : Preorder α
inst_1 : SupSet α
f : ι → α
h : BddAbove (range f)
rw : Eq.{u_1 + 1} (α := WithTop α) (↑(sSup (range fun (i : ι) ↦ f i)) : WithTop α) (⨆ (i : ι), (↑(f i) : WithTop α))
⊢ Eq.{u_1 + 1} (α := WithTop α) (↑(⨆ (i : ι), f i) : WithTop α) (⨆ (i : ι), (↑(f i) : WithTop α))
have rw₁ : Eq.{u_1 + 1} (α := WithTop α) (↑(sSup (range fun (i : ι) ↦ f i)) : WithTop α)
  (sSup (range fun (i : ι) ↦ (↑(f i) : WithTop α)))
Tactic: rw [iSup, iSup, WithTop.coe_sSup' h, ← range_comp, Function.comp_def]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : Preorder α
inst_1 : SupSet α
f : ι → α
h : BddAbove (range f)
rw : Eq.{u_1 + 1} (α := WithTop α) (↑(sSup (range fun (i : ι) ↦ f i)) : WithTop α) (⨆ (i : ι), (↑(f i) : WithTop α))
rw₁ :
  Eq.{u_1 + 1} (α := WithTop α) (↑(sSup (range fun (i : ι) ↦ f i)) : WithTop α)
    (sSup (range fun (i : ι) ↦ (↑(f i) : WithTop α)))
⊢ Eq.{u_1 + 1} (α := WithTop α) (↑(⨆ (i : ι), f i) : WithTop α) (⨆ (i : ι), (↑(f i) : WithTop α))
have rw₂ : Eq (α := WithTop α) (sSup ((fun (a : α) ↦ (↑a : WithTop α)) '' range f))
  (sSup (range fun (i : ι) ↦ (↑(f i) : WithTop α)))
Tactic: rw [iSup, iSup, WithTop.coe_sSup' h, ← range_comp, Function.comp_def]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : Preorder α
inst_1 : SupSet α
f : ι → α
h : BddAbove (range f)
rw : Eq.{u_1 + 1} (α := WithTop α) (↑(sSup (range fun (i : ι) ↦ f i)) : WithTop α) (⨆ (i : ι), (↑(f i) : WithTop α))
rw₁ :
  Eq.{u_1 + 1} (α := WithTop α) (↑(sSup (range fun (i : ι) ↦ f i)) : WithTop α)
    (sSup (range fun (i : ι) ↦ (↑(f i) : WithTop α)))
rw₂ :
  Eq (α := WithTop α) (sSup ((fun (a : α) ↦ (↑a : WithTop α)) '' range f))
    (sSup (range fun (i : ι) ↦ (↑(f i) : WithTop α)))
⊢ Eq.{u_1 + 1} (α := WithTop α) (↑(⨆ (i : ι), f i) : WithTop α) (⨆ (i : ι), (↑(f i) : WithTop α))
have rw₃ : Eq (α := WithTop α) (sSup (range ((fun (a : α) ↦ (↑a : WithTop α)) ∘ f)))
  (sSup (range fun (i : ι) ↦ (↑(f i) : WithTop α)))
Tactic: rw [iSup, iSup, WithTop.coe_sSup' h, ← range_comp, Function.comp_def]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : Preorder α
inst_1 : SupSet α
f : ι → α
h : BddAbove (range f)
rw : Eq.{u_1 + 1} (α := WithTop α) (↑(sSup (range fun (i : ι) ↦ f i)) : WithTop α) (⨆ (i : ι), (↑(f i) : WithTop α))
rw₁ :
  Eq.{u_1 + 1} (α := WithTop α) (↑(sSup (range fun (i : ι) ↦ f i)) : WithTop α)
    (sSup (range fun (i : ι) ↦ (↑(f i) : WithTop α)))
rw₂ :
  Eq (α := WithTop α) (sSup ((fun (a : α) ↦ (↑a : WithTop α)) '' range f))
    (sSup (range fun (i : ι) ↦ (↑(f i) : WithTop α)))
rw₃ :
  Eq (α := WithTop α) (sSup (range ((fun (a : α) ↦ (↑a : WithTop α)) ∘ f)))
    (sSup (range fun (i : ι) ↦ (↑(f i) : WithTop α)))
⊢ Eq.{u_1 + 1} (α := WithTop α) (↑(⨆ (i : ι), f i) : WithTop α) (⨆ (i : ι), (↑(f i) : WithTop α))
have rw₄ : Eq.{u_1 + 1} (α := WithTop α) (sSup (range fun (x : ι) ↦ (↑(f x) : WithTop α)))
  (sSup (range fun (i : ι) ↦ (↑(f i) : WithTop α)))
Tactic: rw [iSup, iSup, WithTop.coe_sSup' h, ← range_comp, Function.comp_def]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
ι : Type u_5
s : Set ι
hs : s.Nonempty
α : Type u_6
inst : CompleteLattice α
f : ι → α
⊢ Eq.{u_6 + 1} (α := WithBot α) (↑(⨆ i ∈ s, f i) : WithBot α) (⨆ i ∈ s, (↑(f i) : WithBot α))
have rcases : ∀ (j : ι) (hj : j ∈ s), Eq.{u_6 + 1} (α := WithBot α) (↑(⨆ i ∈ s, f i) : WithBot α) (⨆ i ∈ s, (↑(f i) : WithBot α))
Tactic: rcases hs with ⟨j, hj⟩
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (hypothesis)
Goal:
ι : Type u_5
s : Set ι
α : Type u_6
inst : CompleteLattice α
f : ι → α
j : ι
hj : j ∈ s
⊢ Eq.{u_6 + 1} (α := WithBot α) (↑(⨆ i ∈ s, f i) : WithBot α) (⨆ i ∈ s, (↑(f i) : WithBot α))
have this : Nonempty ι
Tactic: have : Nonempty ι := Nonempty.intro j
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
ι : Type u_5
s : Set ι
α : Type u_6
inst : CompleteLattice α
f : ι → α
j : ι
hj : j ∈ s
this : Nonempty ι
⊢ Eq.{u_6 + 1} (α := WithBot α) (↑(⨆ i ∈ s, f i) : WithBot α) (⨆ i ∈ s, (↑(f i) : WithBot α))
have refine : ∀ (i : ι), LE.le.{u_6} (α := WithBot α) (↑(⨆ (_ : i ∈ s), f i) : WithBot α) (⨆ i ∈ s, (↑(f i) : WithBot α))
Tactic: refine le_antisymm ((WithBot.coe_iSup (OrderTop.bddAbove _)).trans_le <|
    iSup_le_iff.mpr fun i ↦ ?_) <| iSup_le_iff.mpr <| fun _ ↦ iSup_le_iff.mpr <|
      fun hi ↦ WithBot.coe_le_coe.mpr (le_biSup _ hi)
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
ι : Type u_5
s : Set ι
α : Type u_6
inst : CompleteLattice α
f : ι → α
j : ι
hj : j ∈ s
this : Nonempty ι
i : ι
⊢ LE.le.{u_6} (α := WithBot α) (↑(⨆ (_ : i ∈ s), f i) : WithBot α) (⨆ i ∈ s, (↑(f i) : WithBot α))
have pos : ∀ (h : i ∈ s), LE.le.{u_6} (α := WithBot α) (↑(⨆ (_ : i ∈ s), f i) : WithBot α) (⨆ i ∈ s, (↑(f i) : WithBot α))
Tactic: by_cases h : i ∈ s
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
ι : Type u_5
s : Set ι
α : Type u_6
inst : CompleteLattice α
f : ι → α
j : ι
hj : j ∈ s
this : Nonempty ι
i : ι
pos : ∀ (h : i ∈ s), LE.le.{u_6} (α := WithBot α) (↑(⨆ (_ : i ∈ s), f i) : WithBot α) (⨆ i ∈ s, (↑(f i) : WithBot α))
⊢ LE.le.{u_6} (α := WithBot α) (↑(⨆ (_ : i ∈ s), f i) : WithBot α) (⨆ i ∈ s, (↑(f i) : WithBot α))
have neg : ∀ (h : i ∉ s), LE.le.{u_6} (α := WithBot α) (↑(⨆ (_ : i ∈ s), f i) : WithBot α) (⨆ i ∈ s, (↑(f i) : WithBot α))
Tactic: by_cases h : i ∈ s
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
ι : Type u_5
s : Set ι
α : Type u_6
inst : CompleteLattice α
f : ι → α
j : ι
hj : j ∈ s
this : Nonempty ι
i : ι
h : i ∈ s
⊢ LE.le.{u_6} (α := WithBot α) (↑(⨆ (_ : i ∈ s), f i) : WithBot α) (⨆ i ∈ s, (↑(f i) : WithBot α))
have simpa : (↑(f i) : WithBot α) ≤ ⨆ i ∈ s, (↑(f i) : WithBot α)
Tactic: simpa only [iSup_pos h] using by apply le_biSup _ h
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
ι : Type u_5
s : Set ι
α : Type u_6
inst : CompleteLattice α
f : ι → α
⊢ Eq.{u_6 + 1} (α := WithBot α) (↑(⨅ i ∈ s, f i) : WithBot α) (⨅ i ∈ s, (↑(f i) : WithBot α))
have refine : ∀ (i : ι), LE.le.{u_6} (α := WithBot α) (⨅ i ∈ s, (↑(f i) : WithBot α)) (↑(⨅ (_ : i ∈ s), f i) : WithBot α)
Tactic: refine le_antisymm (by simpa using fun _ ↦ biInf_le _) <|
    (le_iInf_iff.mpr fun i ↦ ?_).trans_eq (WithBot.coe_iInf _ (OrderBot.bddBelow _)).symm
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
ι : Type u_5
s : Set ι
α : Type u_6
inst : CompleteLattice α
f : ι → α
i : ι
⊢ LE.le.{u_6} (α := WithBot α) (⨅ i ∈ s, (↑(f i) : WithBot α)) (↑(⨅ (_ : i ∈ s), f i) : WithBot α)
have pos : ∀ (h : i ∈ s), LE.le.{u_6} (α := WithBot α) (⨅ i ∈ s, (↑(f i) : WithBot α)) (↑(⨅ (_ : i ∈ s), f i) : WithBot α)
Tactic: by_cases h : i ∈ s
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
ι : Type u_5
s : Set ι
α : Type u_6
inst : CompleteLattice α
f : ι → α
i : ι
pos : ∀ (h : i ∈ s), LE.le.{u_6} (α := WithBot α) (⨅ i ∈ s, (↑(f i) : WithBot α)) (↑(⨅ (_ : i ∈ s), f i) : WithBot α)
⊢ LE.le.{u_6} (α := WithBot α) (⨅ i ∈ s, (↑(f i) : WithBot α)) (↑(⨅ (_ : i ∈ s), f i) : WithBot α)
have neg : ∀ (h : i ∉ s), LE.le.{u_6} (α := WithBot α) (⨅ i ∈ s, (↑(f i) : WithBot α)) (↑(⨅ (_ : i ∈ s), f i) : WithBot α)
Tactic: by_cases h : i ∈ s
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
ι : Type u_5
s : Set ι
α : Type u_6
inst : CompleteLattice α
f : ι → α
i : ι
h : i ∈ s
⊢ LE.le.{u_6} (α := WithBot α) (⨅ i ∈ s, (↑(f i) : WithBot α)) (↑(⨅ (_ : i ∈ s), f i) : WithBot α)
have simpa : ⨅ i ∈ s, (↑(f i) : WithBot α) ≤ (↑(f i) : WithBot α)
Tactic: simpa only [iInf_pos h] using by apply biInf_le _ h
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
f : β → α
s : Set β
H : BddAbove (f '' s)
Hne : s.Nonempty
⊢ IsLUB (f '' s) (⨆ (i : (↑s : Type u_2)), f (↑i : β))
have rw : IsLUB (f '' s) (sSup (f '' s))
Tactic: rw [← sSup_image']
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
κ : ι → Sort u_5
f : (i : ι) → κ i → α
H : BddAbove.{u_1} (α := α) (⋃ (i : ι), range (f i))
⊢ BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ ⨆ (j : κ i), f i j)
have have : ∀ (a : α) (h : Membership.mem (γ := Set α) (upperBounds (⋃ (i : ι), range (f i))) a),
  BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ ⨆ (j : κ i), f i j)
Tactic: have ⟨a, h⟩ := H
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
κ : ι → Sort u_5
f : (i : ι) → κ i → α
H : BddAbove.{u_1} (α := α) (⋃ (i : ι), range (f i))
a : α
h : Membership.mem (γ := Set α) (upperBounds (⋃ (i : ι), range (f i))) a
⊢ BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ ⨆ (j : κ i), f i j)
have refine : ∀ (x : α),
  Membership.mem (γ := Set α) (range fun (i : ι) ↦ ⨆ (j : κ i), f i j) x →
    ∀ (i : ι) (hx : (fun (i : ι) ↦ (⨆ (j : κ i), f i j : α)) i = x),
      (fun (i : ι) ↦ (⨆ (j : κ i), f i j : α)) i ≤ a ⊔ sSup ∅
Tactic: refine ⟨a ⊔ (sSup ∅), fun x ⟨i, hx⟩ ↦ hx ▸ ?_⟩
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
κ : ι → Sort u_5
f : (i : ι) → κ i → α
H : BddAbove.{u_1} (α := α) (⋃ (i : ι), range (f i))
a : α
h : Membership.mem (γ := Set α) (upperBounds (⋃ (i : ι), range (f i))) a
x : α
h_1 : Membership.mem (γ := Set α) (range fun (i : ι) ↦ ⨆ (j : κ i), f i j) x
i : ι
hx : (fun (i : ι) ↦ (⨆ (j : κ i), f i j : α)) i = x
⊢ (fun (i : ι) ↦ (⨆ (j : κ i), f i j : α)) i ≤ a ⊔ sSup ∅
have inl : IsEmpty.{u_5} (κ i) → (fun (i : ι) ↦ (⨆ (j : κ i), f i j : α)) i ≤ a ⊔ sSup ∅
Tactic: cases isEmpty_or_nonempty <| κ i
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
κ : ι → Sort u_5
f : (i : ι) → κ i → α
H : BddAbove.{u_1} (α := α) (⋃ (i : ι), range (f i))
a : α
h : Membership.mem (γ := Set α) (upperBounds (⋃ (i : ι), range (f i))) a
x : α
h_1 : Membership.mem (γ := Set α) (range fun (i : ι) ↦ ⨆ (j : κ i), f i j) x
i : ι
hx : (fun (i : ι) ↦ (⨆ (j : κ i), f i j : α)) i = x
inl : IsEmpty.{u_5} (κ i) → (fun (i : ι) ↦ (⨆ (j : κ i), f i j : α)) i ≤ a ⊔ sSup ∅
⊢ (fun (i : ι) ↦ (⨆ (j : κ i), f i j : α)) i ≤ a ⊔ sSup ∅
have inr : Nonempty.{u_5} (κ i) → (fun (i : ι) ↦ (⨆ (j : κ i), f i j : α)) i ≤ a ⊔ sSup ∅
Tactic: cases isEmpty_or_nonempty <| κ i
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
f g : ι → α
B : BddAbove (range g)
H : ∀ (x : ι), f x ≤ g x
⊢ iSup f ≤ iSup g
have inl : IsEmpty ι → iSup f ≤ iSup g
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
f g : ι → α
B : BddAbove (range g)
H : ∀ (x : ι), f x ≤ g x
inl : IsEmpty ι → iSup f ≤ iSup g
⊢ iSup f ≤ iSup g
have inr : Nonempty ι → iSup f ≤ iSup g
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
f g : ι → α
B : BddAbove (range g)
H : ∀ (x : ι), f x ≤ g x
h : IsEmpty ι
⊢ iSup f ≤ iSup g
have inl : sSup ∅ ≤ iSup g
Tactic: rw [iSup_of_empty', iSup_of_empty']
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
f g : ι → α
B : BddAbove (range g)
H : ∀ (x : ι), f x ≤ g x
h : IsEmpty ι
inl : sSup ∅ ≤ iSup g
⊢ iSup f ≤ iSup g
have inl₁ : LE.le.{u_1} (α := α) (sSup ∅) (sSup ∅)
Tactic: rw [iSup_of_empty', iSup_of_empty']
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
f g : ι → α
Hf : BddAbove (range f)
Hg : BddAbove (range g)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (x : ι), f x ⊔ g x) ((⨆ (x : ι), f x) ⊔ ⨆ (x : ι), g x)
have inl : IsEmpty ι → Eq.{u_1 + 1} (α := α) (⨆ (x : ι), f x ⊔ g x) ((⨆ (x : ι), f x) ⊔ ⨆ (x : ι), g x)
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
f g : ι → α
Hf : BddAbove (range f)
Hg : BddAbove (range g)
inl : IsEmpty ι → Eq.{u_1 + 1} (α := α) (⨆ (x : ι), f x ⊔ g x) ((⨆ (x : ι), f x) ⊔ ⨆ (x : ι), g x)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (x : ι), f x ⊔ g x) ((⨆ (x : ι), f x) ⊔ ⨆ (x : ι), g x)
have inr : Nonempty ι → Eq.{u_1 + 1} (α := α) (⨆ (x : ι), f x ⊔ g x) ((⨆ (x : ι), f x) ⊔ ⨆ (x : ι), g x)
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
f g : ι → α
Hf : BddAbove (range f)
Hg : BddAbove (range g)
h : Nonempty ι
⊢ Eq.{u_1 + 1} (α := α) (⨆ (x : ι), f x ⊔ g x) ((⨆ (x : ι), f x) ⊔ ⨆ (x : ι), g x)
have inr : iSup f ⊔ iSup g ≤ ⨆ (x : ι), f x ⊔ g x
Tactic: apply le_antisymm <| ciSup_le fun x ↦ sup_le_sup (le_ciSup Hf x) (le_ciSup Hg x)
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (hypothesis)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
f g : ι → α
Hf : BddAbove (range f)
Hg : BddAbove (range g)
h : Nonempty ι
⊢ iSup f ⊔ iSup g ≤ ⨆ (x : ι), f x ⊔ g x
have this : BddAbove.{u_1} (α := α) (range fun (x : ι) ↦ f x ⊔ g x)
Tactic: have := bbdAbove_range_sup Hf Hg
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
κ : ι → Sort u_5
f : (i : ι) → κ i → α
H : BddBelow.{u_1} (α := α) (⋃ (i : ι), range (f i))
⊢ BddBelow.{u_1} (α := α) (range fun (i : ι) ↦ ⨅ (j : κ i), f i j)
have have : ∀ (a : α) (h : Membership.mem (γ := Set α) (lowerBounds (⋃ (i : ι), range (f i))) a),
  BddBelow.{u_1} (α := α) (range fun (i : ι) ↦ ⨅ (j : κ i), f i j)
Tactic: have ⟨a, h⟩ := H
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
κ : ι → Sort u_5
f : (i : ι) → κ i → α
H : BddBelow.{u_1} (α := α) (⋃ (i : ι), range (f i))
a : α
h : Membership.mem (γ := Set α) (lowerBounds (⋃ (i : ι), range (f i))) a
⊢ BddBelow.{u_1} (α := α) (range fun (i : ι) ↦ ⨅ (j : κ i), f i j)
have refine : ∀ (x : α),
  Membership.mem (γ := Set α) (range fun (i : ι) ↦ ⨅ (j : κ i), f i j) x →
    ∀ (i : ι) (hx : (fun (i : ι) ↦ (⨅ (j : κ i), f i j : α)) i = x),
      a ⊓ sInf ∅ ≤ (fun (i : ι) ↦ (⨅ (j : κ i), f i j : α)) i
Tactic: refine ⟨a ⊓ (sInf ∅), fun x ⟨i, hx⟩ ↦ hx ▸ ?_⟩
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
κ : ι → Sort u_5
f : (i : ι) → κ i → α
H : BddBelow.{u_1} (α := α) (⋃ (i : ι), range (f i))
a : α
h : Membership.mem (γ := Set α) (lowerBounds (⋃ (i : ι), range (f i))) a
x : α
h_1 : Membership.mem (γ := Set α) (range fun (i : ι) ↦ ⨅ (j : κ i), f i j) x
i : ι
hx : (fun (i : ι) ↦ (⨅ (j : κ i), f i j : α)) i = x
⊢ a ⊓ sInf ∅ ≤ (fun (i : ι) ↦ (⨅ (j : κ i), f i j : α)) i
have inl : IsEmpty.{u_5} (κ i) → a ⊓ sInf ∅ ≤ (fun (i : ι) ↦ (⨅ (j : κ i), f i j : α)) i
Tactic: cases isEmpty_or_nonempty <| κ i
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
κ : ι → Sort u_5
f : (i : ι) → κ i → α
H : BddBelow.{u_1} (α := α) (⋃ (i : ι), range (f i))
a : α
h : Membership.mem (γ := Set α) (lowerBounds (⋃ (i : ι), range (f i))) a
x : α
h_1 : Membership.mem (γ := Set α) (range fun (i : ι) ↦ ⨅ (j : κ i), f i j) x
i : ι
hx : (fun (i : ι) ↦ (⨅ (j : κ i), f i j : α)) i = x
inl : IsEmpty.{u_5} (κ i) → a ⊓ sInf ∅ ≤ (fun (i : ι) ↦ (⨅ (j : κ i), f i j : α)) i
⊢ a ⊓ sInf ∅ ≤ (fun (i : ι) ↦ (⨅ (j : κ i), f i j : α)) i
have inr : Nonempty.{u_5} (κ i) → a ⊓ sInf ∅ ≤ (fun (i : ι) ↦ (⨅ (j : κ i), f i j : α)) i
Tactic: cases isEmpty_or_nonempty <| κ i
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (p : β × γ), f p) (⨆ (b : β), ⨆ (c : γ), f (b, c))
have inl : IsEmpty β → Eq.{u_1 + 1} (α := α) (⨆ (p : β × γ), f p) (⨆ (b : β), ⨆ (c : γ), f (b, c))
Tactic: rcases isEmpty_or_nonempty β
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
inl : IsEmpty β → Eq.{u_1 + 1} (α := α) (⨆ (p : β × γ), f p) (⨆ (b : β), ⨆ (c : γ), f (b, c))
⊢ Eq.{u_1 + 1} (α := α) (⨆ (p : β × γ), f p) (⨆ (b : β), ⨆ (c : γ), f (b, c))
have inr : Nonempty β → Eq.{u_1 + 1} (α := α) (⨆ (p : β × γ), f p) (⨆ (b : β), ⨆ (c : γ), f (b, c))
Tactic: rcases isEmpty_or_nonempty β
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h : Nonempty β
⊢ Eq.{u_1 + 1} (α := α) (⨆ (p : β × γ), f p) (⨆ (b : β), ⨆ (c : γ), f (b, c))
have inr : IsEmpty γ → Eq.{u_1 + 1} (α := α) (⨆ (p : β × γ), f p) (⨆ (b : β), ⨆ (c : γ), f (b, c))
Tactic: rcases isEmpty_or_nonempty γ
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h : Nonempty β
inr : IsEmpty γ → Eq.{u_1 + 1} (α := α) (⨆ (p : β × γ), f p) (⨆ (b : β), ⨆ (c : γ), f (b, c))
⊢ Eq.{u_1 + 1} (α := α) (⨆ (p : β × γ), f p) (⨆ (b : β), ⨆ (c : γ), f (b, c))
have inr₁ : Nonempty γ → Eq.{u_1 + 1} (α := α) (⨆ (p : β × γ), f p) (⨆ (b : β), ⨆ (c : γ), f (b, c))
Tactic: rcases isEmpty_or_nonempty γ
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h : Nonempty β
h_1 : Nonempty γ
⊢ BddAbove.{u_1} (α := α) (range fun (b : β) ↦ ⨆ (c : γ), f (b, c))
have hf₁ : ∃ (x : α), ∀ y ∈ range f, y ≤ x
Tactic: rw [bddAbove_def] at hf ⊢
Cleared hypotheses: hf, h, h_1
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice α
f : β × γ → α
hf : ∃ (x : α), ∀ y ∈ range f, y ≤ x
h : Nonempty β
h_1 : Nonempty γ
⊢ ∃ (x : α), ∀ (y : α), Membership.mem (γ := Set α) (range fun (b : β) ↦ ⨆ (c : γ), f (b, c)) y → y ≤ x
have obtain : ∀ (B : α) (hB : ∀ y ∈ range f, y ≤ B),
  ∃ (x : α), ∀ (y : α), Membership.mem (γ := Set α) (range fun (b : β) ↦ ⨆ (c : γ), f (b, c)) y → y ≤ x
Tactic: obtain ⟨B, hB⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice α
f : β × γ → α
h : Nonempty β
h_1 : Nonempty γ
B : α
hB : ∀ y ∈ range f, y ≤ B
⊢ ∃ (x : α), ∀ (y : α), Membership.mem (γ := Set α) (range fun (b : β) ↦ ⨆ (c : γ), f (b, c)) y → y ≤ x
have refine : ∀ (y : α) (hy : Membership.mem (γ := Set α) (range fun (b : β) ↦ ⨆ (c : γ), f (b, c)) y), y ≤ B
Tactic: refine ⟨B, fun y hy ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice α
f : β × γ → α
h : Nonempty β
h_1 : Nonempty γ
B : α
hB : ∀ y ∈ range f, y ≤ B
y : α
hy : Membership.mem (γ := Set α) (range fun (b : β) ↦ ⨆ (c : γ), f (b, c)) y
⊢ y ≤ B
have obtain : ∀ (z : β) (hy : Membership.mem (γ := Set α) (range fun (b : β) ↦ ⨆ (c : γ), f (b, c)) (⨆ (c : γ), f (z, c))),
  ⨆ (c : γ), f (z, c) ≤ B
Tactic: obtain ⟨z, rfl⟩ := Set.mem_range.mp hy
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h : Nonempty β
h_1 : Nonempty γ
⊢ Eq.{u_1 + 1} (α := α) (⨆ (p : β × γ), f p) (⨆ (b : β), ⨆ (c : γ), f (b, c))
have h₁ : BddAbove.{u_1} (α := α) (range fun (b : β) ↦ ⨆ (c : γ), f (b, c))
Tactic: have h₁ : BddAbove (Set.range fun b ↦ ⨆ c, f (b, c)) := by
    rw [bddAbove_def] at hf ⊢
    obtain ⟨B, hB⟩ := hf
    refine ⟨B, fun y hy ↦ ?_⟩
    obtain ⟨z, rfl⟩ := Set.mem_range.mp hy
    exact ciSup_le fun c ↦ by grind
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h : Nonempty β
h_1 : Nonempty γ
h₁ : BddAbove.{u_1} (α := α) (range fun (b : β) ↦ ⨆ (c : γ), f (b, c))
b : β
⊢ BddAbove.{u_1} (α := α) (range fun (c : γ) ↦ f (b, c))
have rw : ∀ (hf : ∃ (x : α), ∀ y ∈ range f, y ≤ x),
  Nonempty β →
    Nonempty γ →
      ∀ (h₁ : BddAbove.{u_1} (α := α) (range fun (b : β) ↦ ⨆ (c : γ), f (b, c))) (b : β),
        ∃ (x : α), ∀ (y : α), Membership.mem (γ := Set α) (range fun (c : γ) ↦ f (b, c)) y → y ≤ x
Tactic: rw [bddAbove_def] at hf ⊢
Cleared hypotheses: hf, h, h_1, h₁, b