awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice α
f : β × γ → α
h : Nonempty β
h_1 : Nonempty γ
h₁ : BddAbove.{u_1} (α := α) (range fun (b : β) ↦ ⨆ (c : γ), f (b, c))
b : β
B : α
hB : ∀ y ∈ range f, y ≤ B
⊢ ∀ (y : α), Membership.mem (γ := Set α) (range fun (c : γ) ↦ f (b, c)) y → y ≤ B

Tactic:
grind
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice α
f : β × γ → α
h : Nonempty β
h_1 : Nonempty γ
h₁ : BddAbove.{u_1} (α := α) (range fun (b : β) ↦ ⨆ (c : γ), f (b, c))
b : β
B : α
hB : ∀ y ∈ range f, y ≤ B
⊢ ∃ (x : α), ∀ (y : α), Membership.mem (γ := Set α) (range fun (c : γ) ↦ f (b, c)) y → y ≤ x

Tactic:
exact ⟨B, by grind⟩
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
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))

Tactic:
have h₂ b : BddAbove (Set.range fun c ↦ f (b, c)) := by
    rw [bddAbove_def] at hf ⊢
    obtain ⟨B, hB⟩ := hf
    exact ⟨B, by grind⟩
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
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))
h₂ : ∀ (b : β), BddAbove.{u_1} (α := α) (range fun (c : γ) ↦ f (b, c))
⊢ Eq.{u_1 + 1} (α := α) (⨆ (p : β × γ), f p) (⨆ (b : β), ⨆ (c : γ), f (b, c))

Tactic:
eq_of_forall_ge_iff fun c ↦ ?_

Premises used: eq_of_forall_ge_iff
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
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))
h₂ : ∀ (b : β), BddAbove.{u_1} (α := α) (range fun (c : γ) ↦ f (b, c))
inr : ∀ (c : α), ⨆ (p : β × γ), f p ≤ c ↔ ⨆ (b : β), ⨆ (c : γ), f (b, c) ≤ c
⊢ Eq.{u_1 + 1} (α := α) (⨆ (p : β × γ), f p) (⨆ (b : β), ⨆ (c : γ), f (b, c))

Tactic:
refine eq_of_forall_ge_iff fun c ↦ ?_

Premises used: eq_of_forall_ge_iff
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
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))
h₂ : ∀ (b : β), BddAbove.{u_1} (α := α) (range fun (c : γ) ↦ f (b, c))
c : α
inr : (∀ (i : β × γ), f i ≤ c) ↔ ∀ (i : β), ⨆ (c : γ), f (i, c) ≤ c
⊢ ⨆ (p : β × γ), f p ≤ c ↔ ⨆ (b : β), ⨆ (c : γ), f (b, c) ≤ c

Tactic:
rw [ciSup_le_iff (bddAbove_iff_subset_Iic.mpr hf), ciSup_le_iff h₁]

Premises used: Iff.mpr, ciSup_le_iff, bddAbove_iff_subset_Iic
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
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))
h₂ : ∀ (b : β), BddAbove.{u_1} (α := α) (range fun (c : γ) ↦ f (b, c))
c : α
enter : ∀ (b : β), ⨆ (c : γ), f (b, c) ≤ c
| ∀ (i : β), ⨆ (c : γ), f (i, c) ≤ c

Tactic:
enter [b]
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
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))
h₂ : ∀ (b : β), BddAbove.{u_1} (α := α) (range fun (c : γ) ↦ f (b, c))
c : α
b : β
rw : ∀ (i : γ), f (b, i) ≤ c
| ⨆ (c : γ), f (b, c) ≤ c

Tactic:
rw [ciSup_le_iff (h₂ b)]

Premises used: ciSup_le_iff
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
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))
h₂ : ∀ (b : β), BddAbove.{u_1} (α := α) (range fun (c : γ) ↦ f (b, c))
c : α
enter : ∀ (b : β) (i : γ), f (b, i) ≤ c
| ∀ (i : β), ⨆ (c : γ), f (i, c) ≤ c

Tactic:
enter [b]; rw [ciSup_le_iff (h₂ b)]
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
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))
h₂ : ∀ (b : β), BddAbove.{u_1} (α := α) (range fun (c : γ) ↦ f (b, c))
c : α
inr : (∀ (i : β × γ), f i ≤ c) ↔ ∀ (b : β) (i : γ), f (b, i) ≤ c
⊢ (∀ (i : β × γ), f i ≤ c) ↔ ∀ (i : β), ⨆ (c : γ), f (i, c) ≤ c

Tactic:
conv_rhs => enter [b]; rw [ciSup_le_iff (h₂ b)]
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
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))
h₂ : ∀ (b : β), BddAbove.{u_1} (α := α) (range fun (c : γ) ↦ f (b, c))
c : α
⊢ (∀ (i : β × γ), f i ≤ c) ↔ ∀ (b : β) (i : γ), f (b, i) ≤ c

Tactic:
simp [Prod.forall]

Premises used: Prod.forall
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddBelow (range f)
⊢ Eq.{u_1 + 1} (α := α) (⨅ (p : β × γ), f p) (⨅ (b : β), ⨅ (c : γ), f (b, c))

Tactic:
ciSup_prod (α := αᵒᵈ) hf

Premises used: iInf, ciSup_prod, OrderDual
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
b : α
inst_1 : Nonempty ι
f : ι → α
h₁ : ∀ (i : ι), f i ≤ b
h₂ : ∀ w < b, ∃ (i : ι), w < f i
⊢ ⨆ (i : ι), f i = b

Tactic:
csSup_eq_of_forall_le_of_forall_lt_exists_gt (range_nonempty f) (forall_mem_range.mpr h₁)
    fun w hw => exists_range_iff.mpr <| h₂ w hw

Premises used: Iff.mpr, Set.forall_mem_range, iSup, Set.range_nonempty, csSup_eq_of_forall_le_of_forall_lt_exists_gt, Set.exists_range_iff
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
b : α
inst_1 : Nonempty ι
f : ι → α
h₁ : ∀ (i : ι), b ≤ f i
h₂ : ∀ (w : α), b < w → ∃ (i : ι), f i < w
⊢ ⨅ (i : ι), f i = b

Tactic:
ciSup_eq_of_forall_le_of_forall_lt_exists_gt (α := αᵒᵈ) h₁ h₂

Premises used: iInf, ciSup_eq_of_forall_le_of_forall_lt_exists_gt, OrderDual
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
inst_1 : Nonempty ι
f : ι → α
hf : BddBelow (range f)
h :
  ∀ (x : α), Membership.mem (γ := Set α) (Iic (⨅ (i : ι), f i)) x ↔ Membership.mem (γ := Set α) (⋂ (i : ι), Iic (f i)) x
⊢ Eq.{u_1 + 1} (α := Set α) (Iic (⨅ (i : ι), f i)) (⋂ (i : ι), Iic (f i))

Tactic:
ext
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
inst_1 : Nonempty ι
f : ι → α
hf : BddBelow (range f)
x : α
⊢ Membership.mem (γ := Set α) (Iic (⨅ (i : ι), f i)) x ↔ Membership.mem (γ := Set α) (⋂ (i : ι), Iic (f i)) x

Tactic:
simpa using le_ciInf_iff hf

Premises used: le_ciInf_iff
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
inst_1 : Nonempty ι
f : ι → α
hf : BddAbove (range f)
⊢ Eq.{u_1 + 1} (α := Set α) (Ici (⨆ (i : ι), f i)) (⋂ (i : ι), Ici (f i))

Tactic:
Iic_ciInf (α := αᵒᵈ) hf

Premises used: Set.Ici, Set.Iic_ciInf, iSup, setOf, OrderDual
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range.{u_1, max 1 u_4} f)
hf' : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
inl : IsEmpty.{max 1 u_4} (Subtype p) → iSup.{u_1, max 1 u_4} f = ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h)
inr : Nonempty.{max 1 u_4} (Subtype p) → iSup.{u_1, max 1 u_4} f = ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h)
⊢ iSup.{u_1, max 1 u_4} f = ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h)

Tactic:
cases isEmpty_or_nonempty (Subtype p)

Premises used: isEmpty_or_nonempty, Subtype
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range.{u_1, max 1 u_4} f)
hf' : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
h : IsEmpty.{max 1 u_4} (Subtype p)
inl : Eq.{u_1 + 1} (α := α) (sSup ∅) (⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h))
inl₁ inl₂ : Eq.{u_1 + 1} (α := α) (sSup ∅) (sSup ∅)
⊢ iSup.{u_1, max 1 u_4} f = ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h)

Tactic:
rw [iSup_of_empty', cbiSup_eq_of_forall_not fun i h ↦ isEmptyElim (⟨i, h⟩ : Subtype p)]

Premises used: isEmptyElim, Subtype.mk, cbiSup_eq_of_forall_not, iSup_of_empty'
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range.{u_1, max 1 u_4} f)
hf' : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
h : Nonempty.{max 1 u_4} (Subtype p)
⊢ Nonempty ι

Tactic:
have : Nonempty ι := (nonempty_subtype.mp ‹_›).nonempty
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range.{u_1, max 1 u_4} f)
hf' : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
h : Nonempty.{max 1 u_4} (Subtype p)
this : Nonempty ι
⊢ iSup.{u_1, max 1 u_4} f = ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h)

Tactic:
le_antisymm (ciSup_le ?_) ?_

Premises used: le_antisymm, ciSup_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range.{u_1, max 1 u_4} f)
hf' : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
h : Nonempty.{max 1 u_4} (Subtype p)
this : Nonempty ι
inr : ∀ (x : Subtype p), f x ≤ ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h)
inr₁ : ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h) ≤ iSup.{u_1, max 1 u_4} f
⊢ iSup.{u_1, max 1 u_4} f = ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h)

Tactic:
refine le_antisymm (ciSup_le ?_) ?_

Premises used: le_antisymm, ciSup_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range.{u_1, max 1 u_4} f)
hf' : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
h_1 : Nonempty.{max 1 u_4} (Subtype p)
this : Nonempty ι
i : ι
h : p i
⊢ f (Subtype.mk (p := p) i h) = (fun (i : ι) ↦ (⨆ (h : p i), f (Subtype.mk (p := p) i h) : α)) i

Tactic:
simp [h]
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range.{u_1, max 1 u_4} f)
hf' : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
h_1 : Nonempty.{max 1 u_4} (Subtype p)
this : Nonempty ι
i : ι
h : p i
⊢ f (Subtype.mk (p := p) i h) = (fun (i : ι) ↦ (⨆ (h : p i), f (Subtype.mk (p := p) i h) : α)) i

Tactic:
have : f ⟨i, h⟩ = (fun i : ι ↦ ⨆ (h : p i), f ⟨i, h⟩) i := by simp [h]
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range.{u_1, max 1 u_4} f)
hf' : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
h_1 : Nonempty.{max 1 u_4} (Subtype p)
this_1 : Nonempty ι
i : ι
h : p i
this : f (Subtype.mk (p := p) i h) = (fun (i : ι) ↦ (⨆ (h : p i), f (Subtype.mk (p := p) i h) : α)) i
inr :
  LE.le.{u_1} (α := α) ((fun (i : ι) ↦ (⨆ (h : p i), f (Subtype.mk (p := p) i h) : α)) i)
    (⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h))
⊢ f (Subtype.mk (p := p) i h) ≤ ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h)

Tactic:
rw [this]
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range.{u_1, max 1 u_4} f)
hf' : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
h_1 : Nonempty.{max 1 u_4} (Subtype p)
this_1 : Nonempty ι
i : ι
h : p i
this : f (Subtype.mk (p := p) i h) = (fun (i : ι) ↦ (⨆ (h : p i), f (Subtype.mk (p := p) i h) : α)) i
⊢ LE.le.{u_1} (α := α) ((fun (i : ι) ↦ (⨆ (h : p i), f (Subtype.mk (p := p) i h) : α)) i)
    (⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h))

Tactic:
le_ciSup (f := (fun i : ι ↦ ⨆ (h : p i), f ⟨i, h⟩)) ?_ i

Premises used: le_ciSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range.{u_1, max 1 u_4} f)
hf' : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
h_1 : Nonempty.{max 1 u_4} (Subtype p)
this_1 : Nonempty ι
i : ι
h : p i
this : f (Subtype.mk (p := p) i h) = (fun (i : ι) ↦ (⨆ (h : p i), f (Subtype.mk (p := p) i h) : α)) i
inr : BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ ⨆ (h : p i), f (Subtype.mk (p := p) i h))
⊢ LE.le.{u_1} (α := α) ((fun (i : ι) ↦ (⨆ (h : p i), f (Subtype.mk (p := p) i h) : α)) i)
    (⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h))

Tactic:
refine le_ciSup (f := (fun i : ι ↦ ⨆ (h : p i), f ⟨i, h⟩)) ?_ i

Premises used: le_ciSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range.{u_1, max 1 u_4} f)
hf' : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
h_1 : Nonempty.{max 1 u_4} (Subtype p)
this_1 : Nonempty ι
i : ι
h : p i
this : f (Subtype.mk (p := p) i h) = (fun (i : ι) ↦ (⨆ (h : p i), f (Subtype.mk (p := p) i h) : α)) i
inr : BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ if h : p i then f (Subtype.mk (p := p) i h) else sSup ∅)
⊢ BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ ⨆ (h : p i), f (Subtype.mk (p := p) i h))

Tactic:
simp_rw [ciSup_eq_ite]

Premises used: ciSup_eq_ite
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range.{u_1, max 1 u_4} f)
hf' : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
h_1 : Nonempty.{max 1 u_4} (Subtype p)
this_1 : Nonempty ι
i : ι
h : p i
this : f (Subtype.mk (p := p) i h) = (fun (i : ι) ↦ (⨆ (h : p i), f (Subtype.mk (p := p) i h) : α)) i
⊢ BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ if h : p i then f (Subtype.mk (p := p) i h) else sSup ∅)

Tactic:
(hf.union (bddAbove_singleton (a := sSup ∅))).mono ?_

Premises used: bddAbove_singleton, BddAbove.union, BddAbove.mono
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range.{u_1, max 1 u_4} f)
hf' : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
h_1 : Nonempty.{max 1 u_4} (Subtype p)
this_1 : Nonempty ι
i : ι
h : p i
this : f (Subtype.mk (p := p) i h) = (fun (i : ι) ↦ (⨆ (h : p i), f (Subtype.mk (p := p) i h) : α)) i
inr :
  (range fun (i : ι) ↦ if h : p i then f (Subtype.mk (p := p) i h) else sSup ∅) ⊆ range.{u_1, max 1 u_4} f ∪ {sSup ∅}
⊢ BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ if h : p i then f (Subtype.mk (p := p) i h) else sSup ∅)

Tactic:
refine (hf.union (bddAbove_singleton (a := sSup ∅))).mono ?_

Premises used: bddAbove_singleton, BddAbove.union, BddAbove.mono
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range.{u_1, max 1 u_4} f)
hf' : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
h_1 : Nonempty.{max 1 u_4} (Subtype p)
this_1 : Nonempty ι
i : ι
h : p i
this : f (Subtype.mk (p := p) i h) = (fun (i : ι) ↦ (⨆ (h : p i), f (Subtype.mk (p := p) i h) : α)) i
⊢ (range fun (i : ι) ↦ if h : p i then f (Subtype.mk (p := p) i h) else sSup ∅) ⊆ range.{u_1, max 1 u_4} f ∪ {sSup ∅}

Tactic:
grind
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range.{u_1, max 1 u_4} f)
hf' : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
h : Nonempty.{max 1 u_4} (Subtype p)
this : Nonempty ι
⊢ ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h) ≤ iSup.{u_1, max 1 u_4} f

Tactic:
ciSup_le fun i ↦ ?_

Premises used: ciSup_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range.{u_1, max 1 u_4} f)
hf' : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
h : Nonempty.{max 1 u_4} (Subtype p)
this : Nonempty ι
inr : ∀ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h) ≤ iSup.{u_1, max 1 u_4} f
⊢ ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h) ≤ iSup.{u_1, max 1 u_4} f

Tactic:
refine ciSup_le fun i ↦ ?_

Premises used: ciSup_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range.{u_1, max 1 u_4} f)
hf' : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
h : Nonempty.{max 1 u_4} (Subtype p)
this : Nonempty ι
i : ι
inr : (if h : p i then f (Subtype.mk (p := p) i h) else sSup ∅) ≤ iSup.{u_1, max 1 u_4} f
⊢ ⨆ (h : p i), f (Subtype.mk (p := p) i h) ≤ iSup.{u_1, max 1 u_4} f

Tactic:
simp_rw [ciSup_eq_ite]

Premises used: ciSup_eq_ite
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range.{u_1, max 1 u_4} f)
hf' : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
h : Nonempty.{max 1 u_4} (Subtype p)
this : Nonempty ι
i : ι
pos : ∀ (h : p i), f (Subtype.mk (p := p) i h) ≤ iSup.{u_1, max 1 u_4} f
neg : ¬p i → sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
⊢ (if h : p i then f (Subtype.mk (p := p) i h) else sSup ∅) ≤ iSup.{u_1, max 1 u_4} f

Tactic:
split_ifs
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range.{u_1, max 1 u_4} f)
hf' : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
h : Nonempty.{max 1 u_4} (Subtype p)
this : Nonempty ι
i : ι
h_1 : p i
⊢ f (Subtype.mk (p := p) i h_1) ≤ iSup.{u_1, max 1 u_4} f

Tactic:
le_ciSup hf ?_

Premises used: le_ciSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range.{u_1, max 1 u_4} f)
hf' : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
h : Nonempty.{max 1 u_4} (Subtype p)
this : Nonempty ι
i : ι
h_1 : p i
⊢ f (Subtype.mk (p := p) i h_1) ≤ iSup.{u_1, max 1 u_4} f

Tactic:
exact le_ciSup hf ?_

Premises used: le_ciSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range.{u_1, max 1 u_4} f)
hf' : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
h : Nonempty.{max 1 u_4} (Subtype p)
this : Nonempty ι
i : ι
h_1 : ¬p i
⊢ sSup ∅ ≤ iSup.{u_1, max 1 u_4} f

Tactic:
hf'
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range.{u_1, max 1 u_4} f)
hf' : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
h : Nonempty.{max 1 u_4} (Subtype p)
this : Nonempty ι
i : ι
h_1 : ¬p i
⊢ sSup ∅ ≤ iSup.{u_1, max 1 u_4} f

Tactic:
exact hf'
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range.{u_1, max 1 u_4} f)
hf' : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
h : Nonempty.{max 1 u_4} (Subtype p)
this : Nonempty ι
inr : ∀ (x : Subtype p), f x ≤ ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h)
inr₁ inr₂ : ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h) ≤ iSup.{u_1, max 1 u_4} f
⊢ iSup.{u_1, max 1 u_4} f = ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h)

Tactic:
classical
  refine le_antisymm (ciSup_le ?_) ?_
  · intro ⟨i, h⟩
    have : f ⟨i, h⟩ = (fun i : ι ↦ ⨆ (h : p i), f ⟨i, h⟩) i := by simp [h]
    rw [this]
    refine le_ciSup (f := (fun i : ι ↦ ⨆ (h : p i), f ⟨i, h⟩)) ?_ i
    simp_rw [ciSup_eq_ite]
    refine (hf.union (bddAbove_singleton (a := sSup ∅))).mono ?_
    grind
  · refine ciSup_le fun i ↦ ?_
    simp_rw [ciSup_eq_ite]
    split_ifs
    · exact le_ciSup hf ?_
    · exact hf'

Premises used: bddAbove_singleton, le_antisymm, le_ciSup, ciSup_eq_ite, BddAbove.union, ciSup_le, BddAbove.mono
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddBelow (range.{u_1, max 1 u_4} f)
hf' : iInf.{u_1, max 1 u_4} f ≤ sInf ∅
⊢ iInf.{u_1, max 1 u_4} f = ⨅ (i : ι), ⨅ (h : p i), f (Subtype.mk (p := p) i h)

Tactic:
ciSup_subtype (α := αᵒᵈ) hf hf'

Premises used: iInf, ciSup_subtype, OrderDual
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : (i : ι) → p i → α
hf : BddAbove.{u_1} (α := α) (range.{u_1, max 1 u_4} fun (i : Subtype p) ↦ f (↑i : ι) ⋯)
hf' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : Subtype p), f (↑i : ι) ⋯)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), ⨆ (h : p i), f i h) (⨆ (x : Subtype p), f (↑x : ι) ⋯)

Tactic:
(ciSup_subtype (f := fun x => f x.val x.property) hf hf').symm

Premises used: ciSup_subtype, Eq.symm
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : (i : ι) → p i → α
hf : BddBelow.{u_1} (α := α) (range.{u_1, max 1 u_4} fun (i : Subtype p) ↦ f (↑i : ι) ⋯)
hf' : LE.le.{u_1} (α := α) (⨅ (i : Subtype p), f (↑i : ι) ⋯) (sInf ∅)
⊢ Eq.{u_1 + 1} (α := α) (⨅ (i : ι), ⨅ (h : p i), f i h) (⨅ (x : Subtype p), f (↑x : ι) ⋯)

Tactic:
(ciInf_subtype (f := fun x => f x.val x.property) hf hf').symm

Premises used: ciInf_subtype, Eq.symm
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_5
s : Set ι
f : ι → α
hf : BddAbove.{u_1} (α := α) (range fun (i : (↑s : Type u_5)) ↦ f (↑i : ι))
hf' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑s : Type u_5)), f (↑i : ι))
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : (↑s : Type u_5)), f (↑i : ι)) (⨆ t ∈ s, f t)

Tactic:
ciSup_subtype hf hf'

Premises used: ciSup_subtype
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_5
s : Set ι
f : ι → α
hf : BddBelow.{u_1} (α := α) (range fun (i : (↑s : Type u_5)) ↦ f (↑i : ι))
hf' : LE.le.{u_1} (α := α) (⨅ (i : (↑s : Type u_5)), f (↑i : ι)) (sInf ∅)
⊢ Eq.{u_1 + 1} (α := α) (⨅ (i : (↑s : Type u_5)), f (↑i : ι)) (⨅ t ∈ s, f t)

Tactic:
ciInf_subtype hf hf'

Premises used: ciInf_subtype
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
s : Set β
f : β → α
hf : BddAbove.{u_1} (α := α) (range fun (i : (↑s : Type u_2)) ↦ f (↑i : β))
hf' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑s : Type u_2)), f (↑i : β))
rw : sSup (f '' s) = ⨆ (i : (↑s : Type u_2)), f (↑i : β)
rw₁ : sSup (f '' s) = sSup (range fun (i : (↑s : Type u_2)) ↦ f (↑i : β))
rw₂ rw₃ :
  Eq.{u_1 + 1} (α := α) (sSup (range fun (x : (↑s : Type u_2)) ↦ f (↑x : β)))
    (sSup (range fun (i : (↑s : Type u_2)) ↦ f (↑i : β)))
⊢ sSup (f '' s) = ⨆ a ∈ s, f a

Tactic:
rw [← ciSup_subtype_fun hf hf', iSup, Set.image_eq_range]

Premises used: iSup, Set.image_eq_range, ciSup_subtype_fun