awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
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 ∅
inr : Nonempty.{u_5} (κ i) → (fun (i : ι) ↦ (⨆ (j : κ i), f i j : α)) i ≤ a ⊔ sSup ∅
⊢ (fun (i : ι) ↦ (⨆ (j : κ i), f i j : α)) i ≤ a ⊔ sSup ∅

Tactic:
cases isEmpty_or_nonempty <| κ i

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
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
h_2 : IsEmpty.{u_5} (κ i)
⊢ (fun (i : ι) ↦ (⨆ (j : κ i), f i j : α)) i ≤ a ⊔ sSup ∅

Tactic:
iSup_of_empty' (f i) ▸ le_sup_right

Premises used: Eq.rec, le_sup_right, iSup_of_empty'
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
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
h_2 : IsEmpty.{u_5} (κ i)
⊢ (fun (i : ι) ↦ (⨆ (j : κ i), f i j : α)) i ≤ a ⊔ sSup ∅

Tactic:
exact iSup_of_empty' (f i) ▸ le_sup_right
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
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
h_2 : Nonempty.{u_5} (κ i)
⊢ (fun (i : ι) ↦ (⨆ (j : κ i), f i j : α)) i ≤ a ⊔ sSup ∅

Tactic:
ciSup_le fun j ↦ le_sup_of_le_left <| h ⟨_, ⟨i, rfl⟩, ⟨j, rfl⟩⟩

Premises used: le_sup_of_le_left, And.intro, Exists.intro, Set.range, ciSup_le, rfl
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
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
h_2 : Nonempty.{u_5} (κ i)
⊢ (fun (i : ι) ↦ (⨆ (j : κ i), f i j : α)) i ≤ a ⊔ sSup ∅

Tactic:
exact ciSup_le fun j ↦ le_sup_of_le_left <| h ⟨_, ⟨i, rfl⟩, ⟨j, rfl⟩⟩

Premises used: le_sup_of_le_left, And.intro, Exists.intro, Set.range, ciSup_le, rfl
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
κ : ι → Sort u_5
f : (i : ι) → κ i → α
H : BddAbove.{u_1} (α := α) (⋃ (i : ι), range (f i))
i : ι
j : κ i
⊢ f i j ≤ ⨆ (i : ι), ⨆ (j : κ i), f i j

Tactic:
le_ciSup_of_le H.range_iSup_of_iUnion_range i <|
    le_ciSup (H.mono <| subset_iUnion (range <| f ·) i) j

Premises used: le_ciSup_of_le, Set.subset_iUnion, le_ciSup, BddAbove.range_iSup_of_iUnion_range, Set.range, BddAbove.mono
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
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
inr : Nonempty ι → iSup f ≤ iSup g
⊢ iSup f ≤ iSup g

Tactic:
cases isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
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
inl₁ inl₂ : LE.le.{u_1} (α := α) (sSup ∅) (sSup ∅)
⊢ iSup f ≤ iSup g

Tactic:
rw [iSup_of_empty', iSup_of_empty']

Premises used: iSup_of_empty'
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
f g : ι → α
B : BddAbove (range g)
H : ∀ (x : ι), f x ≤ g x
h : Nonempty ι
⊢ iSup f ≤ iSup g

Tactic:
ciSup_le fun x => le_ciSup_of_le B x (H x)

Premises used: le_ciSup_of_le, ciSup_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
f g : ι → α
B : BddAbove (range g)
H : ∀ (x : ι), f x ≤ g x
h : Nonempty ι
⊢ iSup f ≤ iSup g

Tactic:
exact ciSup_le fun x => le_ciSup_of_le B x (H x)

Premises used: le_ciSup_of_le, ciSup_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
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)
inr : Nonempty ι → 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)

Tactic:
cases isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
f g : ι → α
Hf : BddAbove (range f)
Hg : BddAbove (range g)
h : IsEmpty ι
⊢ Eq.{u_1 + 1} (α := α) (⨆ (x : ι), f x ⊔ g x) ((⨆ (x : ι), f x) ⊔ ⨆ (x : ι), g x)

Tactic:
simp [iSup_of_empty']

Premises used: iSup_of_empty'
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
f g : ι → α
Hf : BddAbove (range f)
Hg : BddAbove (range g)
h : Nonempty ι
inr : iSup f ⊔ iSup g ≤ ⨆ (x : ι), f x ⊔ g x
⊢ Eq.{u_1 + 1} (α := α) (⨆ (x : ι), f x ⊔ g x) ((⨆ (x : ι), f x) ⊔ ⨆ (x : ι), g x)

Tactic:
apply le_antisymm <| ciSup_le fun x ↦ sup_le_sup (le_ciSup Hf x) (le_ciSup Hg x)

Premises used: sup_le_sup, le_antisymm, le_ciSup, ciSup_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
f g : ι → α
Hf : BddAbove (range f)
Hg : BddAbove (range g)
h : Nonempty ι
⊢ BddAbove.{u_1} (α := α) (range fun (x : ι) ↦ f x ⊔ g x)

Tactic:
have := bbdAbove_range_sup Hf Hg
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
f g : ι → α
Hf : BddAbove (range f)
Hg : BddAbove (range g)
h : Nonempty ι
this : BddAbove.{u_1} (α := α) (range fun (x : ι) ↦ f x ⊔ g x)
⊢ iSup f ⊔ iSup g ≤ ⨆ (x : ι), f x ⊔ g x

Tactic:
sup_le (ciSup_mono this fun _ ↦ le_sup_left) (ciSup_mono this fun _ ↦ le_sup_right)

Premises used: le_sup_left, le_sup_right, sup_le, ciSup_mono
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
f g : ι → α
Hf : BddAbove (range f)
Hg : BddAbove (range g)
h : Nonempty ι
this : BddAbove.{u_1} (α := α) (range fun (x : ι) ↦ f x ⊔ g x)
⊢ iSup f ⊔ iSup g ≤ ⨆ (x : ι), f x ⊔ g x

Tactic:
exact sup_le (ciSup_mono this fun _ ↦ le_sup_left) (ciSup_mono this fun _ ↦ le_sup_right)

Premises used: le_sup_left, le_sup_right, sup_le, ciSup_mono
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
f : β → α
s : Set β
H : BddAbove (f '' s)
c : β
hc : c ∈ s
⊢ f c ≤ ⨆ (i : (↑s : Type u_2)), f (↑i : β)

Tactic:
(le_csSup H <| mem_image_of_mem f hc).trans_eq sSup_image'

Premises used: LE.le.trans_eq, Set.mem_image_of_mem, le_csSup, sSup_image'
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
f g : ι → α
B : BddBelow (range f)
H : ∀ (x : ι), f x ≤ g x
⊢ iInf f ≤ iInf g

Tactic:
ciSup_mono (α := αᵒᵈ) B H

Premises used: iInf, OrderDual, ciSup_mono
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
f g : ι → α
Hf : BddBelow (range f)
Hg : BddBelow (range g)
⊢ Eq.{u_1 + 1} (α := α) (⨅ (x : ι), f x ⊓ g x) ((⨅ (x : ι), f x) ⊓ ⨅ (x : ι), g x)

Tactic:
ciSup_sup_eq (α := αᵒᵈ) Hf Hg

Premises used: iInf, OrderDual, ciSup_sup_eq
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
inst_1 : Nonempty ι
f : ι → α
c : α
H : ∀ (x : ι), c ≤ f x
⊢ c ≤ iInf f

Tactic:
ciSup_le (α := αᵒᵈ) H

Premises used: iInf, OrderDual, ciSup_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
f : ι → α
H : BddBelow (range f)
c : ι
⊢ iInf f ≤ f c

Tactic:
le_ciSup (α := αᵒᵈ) H c

Premises used: iInf, le_ciSup, OrderDual
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
a : α
f : ι → α
H : BddBelow (range f)
c : ι
h : f c ≤ a
⊢ iInf f ≤ a

Tactic:
le_ciSup_of_le (α := αᵒᵈ) H c h

Premises used: iInf, le_ciSup_of_le, OrderDual
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
ι' : Sort u_5
inst_1 : Nonempty ι
f : ι → α
g : ι' → α
hg : BddAbove (range g)
h : ∀ (i : ι), ∃ (i' : ι'), f i ≤ g i'
⊢ LE.le.{u_1} (α := α) (⨆ (i : ι), f i) (⨆ (i' : ι'), g i')

Tactic:
ciSup_le fun i ↦ h i |>.elim <| le_ciSup_of_le hg

Premises used: le_ciSup_of_le, ciSup_le, Exists.elim
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
ι' : Sort u_5
inst_1 : Nonempty ι'
f : ι → α
g : ι' → α
hf : BddBelow (range f)
h : ∀ (i' : ι'), ∃ (i : ι), f i ≤ g i'
⊢ LE.le.{u_1} (α := α) (⨅ (i : ι), f i) (⨅ (i' : ι'), g i')

Tactic:
ciSup_mono_of_forall_exists (α := αᵒᵈ) hf h

Premises used: iInf, OrderDual, ciSup_mono_of_forall_exists
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
κ : ι → Sort u_5
f : (i : ι) → κ i → α
H : BddBelow.{u_1} (α := α) (⋃ (i : ι), range (f i))
have :
  ∀ (a : α) (h : Membership.mem (γ := Set α) (lowerBounds (⋃ (i : ι), range (f i))) a),
    BddBelow.{u_1} (α := α) (range fun (i : ι) ↦ ⨅ (j : κ i), f i j)
⊢ BddBelow.{u_1} (α := α) (range fun (i : ι) ↦ ⨅ (j : κ i), f i j)

Tactic:
have ⟨a, h⟩ := H
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
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)

Tactic:
⟨a ⊓ (sInf ∅), fun x ⟨i, hx⟩ ↦ hx ▸ ?_⟩

Premises used: Eq.rec, LE.le, Set.Nonempty, BddBelow, Exists.intro, _private.0.BddBelow.range_iInf_of_iUnion_range.match_2, EmptyCollection.emptyCollection, InfSet.sInf, Min.min
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
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
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
⊢ BddBelow.{u_1} (α := α) (range fun (i : ι) ↦ ⨅ (j : κ i), f i j)

Tactic:
refine ⟨a ⊓ (sInf ∅), fun x ⟨i, hx⟩ ↦ hx ▸ ?_⟩
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
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
inr : Nonempty.{u_5} (κ i) → a ⊓ sInf ∅ ≤ (fun (i : ι) ↦ (⨅ (j : κ i), f i j : α)) i
⊢ a ⊓ sInf ∅ ≤ (fun (i : ι) ↦ (⨅ (j : κ i), f i j : α)) i

Tactic:
cases isEmpty_or_nonempty <| κ i

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
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
h_2 : IsEmpty.{u_5} (κ i)
⊢ a ⊓ sInf ∅ ≤ (fun (i : ι) ↦ (⨅ (j : κ i), f i j : α)) i

Tactic:
iInf_of_isEmpty (f i) ▸ inf_le_right

Premises used: inf_le_right, Eq.rec, iInf_of_isEmpty
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
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
h_2 : IsEmpty.{u_5} (κ i)
⊢ a ⊓ sInf ∅ ≤ (fun (i : ι) ↦ (⨅ (j : κ i), f i j : α)) i

Tactic:
exact iInf_of_isEmpty (f i) ▸ inf_le_right
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
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
h_2 : Nonempty.{u_5} (κ i)
⊢ a ⊓ sInf ∅ ≤ (fun (i : ι) ↦ (⨅ (j : κ i), f i j : α)) i

Tactic:
le_ciInf fun j ↦ inf_le_of_left_le <| h ⟨_, ⟨i, rfl⟩, ⟨j, rfl⟩⟩

Premises used: inf_le_of_left_le, le_ciInf, And.intro, Exists.intro, Set.range, rfl
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
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
h_2 : Nonempty.{u_5} (κ i)
⊢ a ⊓ sInf ∅ ≤ (fun (i : ι) ↦ (⨅ (j : κ i), f i j : α)) i

Tactic:
exact le_ciInf fun j ↦ inf_le_of_left_le <| h ⟨_, ⟨i, rfl⟩, ⟨j, rfl⟩⟩

Premises used: inf_le_of_left_le, le_ciInf, And.intro, Exists.intro, Set.range, rfl
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
κ : ι → Sort u_5
f : (i : ι) → κ i → α
H : BddBelow.{u_1} (α := α) (⋃ (i : ι), range (f i))
i : ι
j : κ i
⊢ ⨅ (i : ι), ⨅ (j : κ i), f i j ≤ f i j

Tactic:
ciInf_le_of_le H.range_iInf_of_iUnion_range i <|
    ciInf_le (H.mono <| subset_iUnion (range <| f ·) i) j

Premises used: ciInf_le_of_le, Set.subset_iUnion, BddBelow.mono, BddBelow.range_iInf_of_iUnion_range, ciInf_le, Set.range
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
f : β → α
s : Set β
H : BddBelow (f '' s)
c : β
hc : c ∈ s
⊢ ⨅ (i : (↑s : Type u_2)), f (↑i : β) ≤ f c

Tactic:
le_ciSup_set (α := αᵒᵈ) H hc

Premises used: iInf, le_ciSup_set, OrderDual
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
inst_1 : Nonempty ι
f : ι → α
hf : BddBelow (range f)
hf' : BddAbove (range f)
⊢ LE.le.{u_1} (α := α) (⨅ (i : ι), f i) (⨆ (i : ι), f i)

Tactic:
(ciInf_le hf (Classical.arbitrary _)).trans <| le_ciSup hf' (Classical.arbitrary _)

Premises used: le_ciSup, ciInf_le, Classical.arbitrary, LE.le.trans
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
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))
inr : Nonempty β → Eq.{u_1 + 1} (α := α) (⨆ (p : β × γ), f p) (⨆ (b : β), ⨆ (c : γ), f (b, c))
⊢ Eq.{u_1 + 1} (α := α) (⨆ (p : β × γ), f p) (⨆ (b : β), ⨆ (c : γ), f (b, c))

Tactic:
rcases isEmpty_or_nonempty β

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

Tactic:
simp [iSup_of_empty']

Premises used: iSup_of_empty'
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
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))
inr₁ : Nonempty γ → Eq.{u_1 + 1} (α := α) (⨆ (p : β × γ), f p) (⨆ (b : β), ⨆ (c : γ), f (b, c))
⊢ Eq.{u_1 + 1} (α := α) (⨆ (p : β × γ), f p) (⨆ (b : β), ⨆ (c : γ), f (b, c))

Tactic:
rcases isEmpty_or_nonempty γ

Premises used: isEmpty_or_nonempty
-- 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 : IsEmpty γ
⊢ Eq.{u_1 + 1} (α := α) (⨆ (p : β × γ), f p) (⨆ (b : β), ⨆ (c : γ), f (b, c))

Tactic:
simp [iSup_of_empty']

Premises used: iSup_of_empty'
-- 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 γ
⊢ ∃ (x : α), ∀ y ∈ range f, y ≤ x

Tactic:
rw [bddAbove_def] at hf ⊢

Premises used: bddAbove_def
-- 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 γ
hf₁ : ∃ (x : α), ∀ y ∈ range f, y ≤ x
⊢ Nonempty β

Tactic:
rw [bddAbove_def] at hf ⊢

Premises used: bddAbove_def
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h_1 : Nonempty β
h_2 : Nonempty γ
hf₁ : ∃ (x : α), ∀ y ∈ range f, y ≤ x
h : Nonempty β
⊢ Nonempty γ

Tactic:
rw [bddAbove_def] at hf ⊢

Premises used: bddAbove_def
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
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 γ
obtain :
  ∀ (B : α) (hB : ∀ y ∈ range f, y ≤ B),
    ∃ (x : α), ∀ (y : α), Membership.mem (γ := Set α) (range fun (b : β) ↦ ⨆ (c : γ), f (b, c)) y → y ≤ x
⊢ ∃ (x : α), ∀ (y : α), Membership.mem (γ := Set α) (range fun (b : β) ↦ ⨆ (c : γ), f (b, c)) y → y ≤ x

Tactic:
obtain ⟨B, hB⟩ := hf
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
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

Tactic:
⟨B, fun y hy ↦ ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
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
refine : ∀ (y : α) (hy : Membership.mem (γ := Set α) (range fun (b : β) ↦ ⨆ (c : γ), f (b, c)) y), y ≤ B
⊢ ∃ (x : α), ∀ (y : α), Membership.mem (γ := Set α) (range fun (b : β) ↦ ⨆ (c : γ), f (b, c)) y → y ≤ x

Tactic:
refine ⟨B, fun y hy ↦ ?_⟩
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
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
obtain :
  ∀ (z : β) (hy : Membership.mem (γ := Set α) (range fun (b : β) ↦ ⨆ (c : γ), f (b, c)) (⨆ (c : γ), f (z, c))),
    ⨆ (c : γ), f (z, c) ≤ B
⊢ y ≤ B

Tactic:
obtain ⟨z, rfl⟩ := Set.mem_range.mp hy

Premises used: Set.mem_range, Iff.mp, rfl
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
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
z : β
hy : Membership.mem (γ := Set α) (range fun (b : β) ↦ ⨆ (c : γ), f (b, c)) (⨆ (c : γ), f (z, c))
c : γ
⊢ f (z, c) ≤ 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 γ
B : α
hB : ∀ y ∈ range f, y ≤ B
z : β
hy : Membership.mem (γ := Set α) (range fun (b : β) ↦ ⨆ (c : γ), f (b, c)) (⨆ (c : γ), f (z, c))
⊢ ⨆ (c : γ), f (z, c) ≤ B

Tactic:
exact ciSup_le fun c ↦ by grind

Premises used: ciSup_le
-- 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 γ
⊢ 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
-- 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 : β
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
⊢ BddAbove.{u_1} (α := α) (range fun (c : γ) ↦ f (b, c))

Tactic:
rw [bddAbove_def] at hf ⊢

Premises used: bddAbove_def
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
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 γ
h₁ : BddAbove.{u_1} (α := α) (range fun (b : β) ↦ ⨆ (c : γ), f (b, c))
b : β
obtain :
  ∀ (B : α) (hB : ∀ y ∈ range f, y ≤ B),
    ∃ (x : α), ∀ (y : α), Membership.mem (γ := Set α) (range fun (c : γ) ↦ f (b, c)) y → y ≤ x
⊢ ∃ (x : α), ∀ (y : α), Membership.mem (γ := Set α) (range fun (c : γ) ↦ f (b, c)) y → y ≤ x

Tactic:
obtain ⟨B, hB⟩ := hf