awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : DecidableEq ι
f : ι → α
s t st : Finset ι
a : α
h : Membership.mem (γ := Set α) (Set.range fun (x : ι) ↦ ⨆ (_ : x ∈ st), f x) a
i : ι
ha : (fun (x : ι) ↦ (⨆ (_ : x ∈ st), f x : α)) i = a
pos : ∀ (h : i ∈ st), (fun (x : ι) ↦ (⨆ (_ : x ∈ st), f x : α)) i ≤ st.sup f
neg : ∀ (h : i ∉ st), (fun (x : ι) ↦ (⨆ (_ : x ∈ st), f x : α)) i ≤ st.sup f
⊢ (fun (x : ι) ↦ (⨆ (_ : x ∈ st), f x : α)) i ≤ st.sup f

Tactic:
by_cases h : i ∈ st
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : DecidableEq ι
f : ι → α
s t st : Finset ι
a : α
h_1 : Membership.mem (γ := Set α) (Set.range fun (x : ι) ↦ ⨆ (_ : x ∈ st), f x) a
i : ι
ha : (fun (x : ι) ↦ (⨆ (_ : x ∈ st), f x : α)) i = a
h : i ∈ st
⊢ (fun (x : ι) ↦ (⨆ (_ : x ∈ st), f x : α)) i ≤ st.sup f

Tactic:
simp [h, le_sup]

Premises used: Finset.le_sup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : DecidableEq ι
f : ι → α
s t st : Finset ι
a : α
h_1 : Membership.mem (γ := Set α) (Set.range fun (x : ι) ↦ ⨆ (_ : x ∈ st), f x) a
i : ι
ha : (fun (x : ι) ↦ (⨆ (_ : x ∈ st), f x : α)) i = a
h : i ∉ st
⊢ (fun (x : ι) ↦ (⨆ (_ : x ∈ st), f x : α)) i ≤ st.sup f

Tactic:
simp [h, le_sup]

Premises used: Finset.le_sup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
f : ι → α
s : Finset ι
h : s.Nonempty
h' : (image f s).Nonempty
⊢ ∀ a ∈ s, a ∈ s ∧ sSup ∅ ≤ f a

Tactic:
simp
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
f : ι → α
s : Finset ι
h : s.Nonempty
⊢ ∀ a ∈ s, a ∈ s ∧ sSup ∅ ≤ f a

Tactic:
simp
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
f : ι → α
s : Set ι
h : s.Nonempty
hs : s.Finite
⊢ ∀ a ∈ s, a ∈ s ∧ sSup ∅ ≤ f a

Tactic:
simp
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
s : Set ι
a : α
f : ι → α
h : s.Nonempty
hs : s.Finite
⊢ ∀ a ∈ s, a ∈ s ∧ sSup ∅ ≤ f a

Tactic:
simp
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
l : List ι
f : ι → α
h : l ≠ []
⊢ ∃ x ∈ l, sSup ∅ ≤ f x

Tactic:
simpa using exists_mem_of_ne_nil _ h

Premises used: List.exists_mem_of_ne_nil
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
s : Multiset ι
f : ι → α
h : s ≠ 0
⊢ ∃ x ∈ s, sSup ∅ ≤ f x

Tactic:
simpa using exists_mem_of_ne_zero h

Premises used: Multiset.exists_mem_of_ne_zero
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Group
Goal:
α : Type u_1
ι : Sort u_2
inst : Nonempty ι
inst_1 : ConditionallyCompleteLattice α
inst_2 : Mul α
inst_3 : MulLeftMono α
inst_4 : MulRightMono α
f g : ι → α
hf : BddAbove (range f)
hg : BddAbove (range g)
⊢ ⨆ (i : ι), f i * g i ≤ HMul.hMul (α := α) (⨆ (i : ι), f i) (⨆ (i : ι), g i)

Tactic:
ciSup_le fun i ↦ mul_le_mul' (le_ciSup hf i) (le_ciSup hg i)

Premises used: le_ciSup, ciSup_le, mul_le_mul'
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Group
Goal:
α : Type u_1
ι : Sort u_2
inst : Nonempty ι
inst_1 : ConditionallyCompleteLattice α
inst_2 : Mul α
inst_3 : MulLeftMono α
inst_4 : MulRightMono α
f g : ι → α
hf : BddBelow (range f)
hg : BddBelow (range g)
⊢ HMul.hMul (α := α) (⨅ (i : ι), f i) (⨅ (i : ι), g i) ≤ ⨅ (i : ι), f i * g i

Tactic:
le_ciInf fun i ↦ mul_le_mul' (ciInf_le hf i) (ciInf_le hg i)

Premises used: le_ciInf, ciInf_le, mul_le_mul'
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Group
Goal:
α : Type u_1
ι : Sort u_2
inst : Nonempty ι
inst_1 : ConditionallyCompleteLattice α
inst_2 : Group α
inst_3 : MulLeftMono α
a g : α
h : ι → α
H : ∀ (j : ι), a ≤ g * h j
⊢ a ≤ g * iInf h

Tactic:
inv_mul_le_iff_le_mul.mp <| le_ciInf fun _ => inv_mul_le_iff_le_mul.mpr <| H _

Premises used: Iff.mpr, le_ciInf, Iff.mp, inv_mul_le_iff_le_mul
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Group
Goal:
α : Type u_1
ι : Sort u_2
inst : Nonempty ι
inst_1 : ConditionallyCompleteLattice α
inst_2 : Group α
inst_3 : MulLeftMono α
a g : α
h : ι → α
H : ∀ (j : ι), g * h j ≤ a
⊢ g * iSup h ≤ a

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

Premises used: le_mul_ciInf, iSup, OrderDual
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Group
Goal:
α : Type u_1
ι : Sort u_2
inst : Nonempty ι
inst_1 : ConditionallyCompleteLattice α
inst_2 : Group α
inst_3 : MulRightMono α
a : α
g : ι → α
h : α
H : ∀ (i : ι), a ≤ g i * h
⊢ a ≤ iInf g * h

Tactic:
mul_inv_le_iff_le_mul.mp <| le_ciInf fun _ => mul_inv_le_iff_le_mul.mpr <| H _

Premises used: Iff.mpr, mul_inv_le_iff_le_mul, le_ciInf, Iff.mp
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Group
Goal:
α : Type u_1
ι : Sort u_2
inst : Nonempty ι
inst_1 : ConditionallyCompleteLattice α
inst_2 : Group α
inst_3 : MulRightMono α
a : α
g : ι → α
h : α
H : ∀ (i : ι), g i * h ≤ a
⊢ iSup g * h ≤ a

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

Premises used: iSup, le_ciInf_mul, OrderDual
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Group
Goal:
α : Type u_1
ι : Sort u_2
ι' : Sort u_3
inst : Nonempty ι
inst_1 : Nonempty ι'
inst_2 : ConditionallyCompleteLattice α
inst_3 : Group α
inst_4 : MulLeftMono α
inst_5 : MulRightMono α
a : α
g : ι → α
h : ι' → α
H : ∀ (i : ι) (j : ι'), a ≤ g i * h j
⊢ a ≤ iInf g * iInf h

Tactic:
le_ciInf_mul fun _ => le_mul_ciInf <| H _

Premises used: le_mul_ciInf, le_ciInf_mul
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Group
Goal:
α : Type u_1
ι : Sort u_2
ι' : Sort u_3
inst : Nonempty ι
inst_1 : Nonempty ι'
inst_2 : ConditionallyCompleteLattice α
inst_3 : Group α
inst_4 : MulLeftMono α
inst_5 : MulRightMono α
a : α
g : ι → α
h : ι' → α
H : ∀ (i : ι) (j : ι'), g i * h j ≤ a
⊢ iSup g * iSup h ≤ a

Tactic:
ciSup_mul_le fun _ => mul_ciSup_le <| H _

Premises used: ciSup_mul_le, mul_ciSup_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : Preorder α
inst_1 : IsEmpty ι
inst_2 : InfSet α
f : ι → WithTop α
rw : Eq.{u_1 + 1} (α := WithTop α) (sInf (range fun (i : ι) ↦ f i)) ⊤
rw₁ : Eq.{u_1 + 1} (α := WithTop α) (sInf ∅) ⊤
rw₂ rw₃ : Eq.{u_1 + 1} (α := WithTop α) ⊤ ⊤
⊢ Eq.{u_1 + 1} (α := WithTop α) (⨅ (i : ι), f i) ⊤

Tactic:
rw [iInf, range_eq_empty, WithTop.sInf_empty]

Premises used: iInf, WithTop.sInf_empty, Set.range_eq_empty
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
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 α)))
rw₄ rw₅ :
  Eq.{u_1 + 1} (α := WithTop α) (sInf (range fun (x : ι) ↦ (↑(f x) : WithTop α)))
    (sInf (range fun (i : ι) ↦ (↑(f i) : WithTop α)))
⊢ Eq.{u_1 + 1} (α := WithTop α) (↑(⨅ (i : ι), f i) : WithTop α) (⨅ (i : ι), (↑(f i) : WithTop α))

Tactic:
rw [iInf, iInf, WithTop.coe_sInf' (range_nonempty f) hf, ← range_comp, Function.comp_def]

Premises used: Set.range_comp, iInf, WithTop.coe_sInf', Function.comp_def, Set.range_nonempty
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
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 α)))
rw₄ rw₅ :
  Eq.{u_1 + 1} (α := WithTop α) (sSup (range fun (x : ι) ↦ (↑(f x) : WithTop α)))
    (sSup (range fun (i : ι) ↦ (↑(f i) : WithTop α)))
⊢ Eq.{u_1 + 1} (α := WithTop α) (↑(⨆ (i : ι), f i) : WithTop α) (⨆ (i : ι), (↑(f i) : WithTop α))

Tactic:
rw [iSup, iSup, WithTop.coe_sSup' h, ← range_comp, Function.comp_def]

Premises used: Set.range_comp, iSup, WithTop.coe_sSup', Function.comp_def
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : Preorder α
inst_1 : IsEmpty ι
inst_2 : SupSet α
f : ι → WithBot α
⊢ Eq.{u_1 + 1} (α := WithBot α) (⨆ (i : ι), f i) ⊥

Tactic:
WithTop.iInf_empty (α := αᵒᵈ) _

Premises used: WithBot, WithTop.iInf_empty, iSup, OrderDual
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : Preorder α
inst_1 : Nonempty ι
inst_2 : SupSet α
f : ι → α
hf : BddAbove (range f)
⊢ Eq.{u_1 + 1} (α := WithBot α) (↑(⨆ (i : ι), f i) : WithBot α) (⨆ (i : ι), (↑(f i) : WithBot α))

Tactic:
WithTop.coe_iInf (α := αᵒᵈ) hf

Premises used: WithBot.some, WithBot, iSup, WithTop.coe_iInf, OrderDual
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
ι : Type u_5
s : Set ι
hs : s.Nonempty
α : Type u_6
inst : CompleteLattice α
f : ι → α
rcases :
  ∀ (j : ι) (hj : j ∈ s), Eq.{u_6 + 1} (α := WithBot α) (↑(⨆ i ∈ s, f i) : WithBot α) (⨆ i ∈ s, (↑(f i) : WithBot α))
⊢ Eq.{u_6 + 1} (α := WithBot α) (↑(⨆ i ∈ s, f i) : WithBot α) (⨆ i ∈ s, (↑(f i) : WithBot α))

Tactic:
rcases hs with ⟨j, hj⟩
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
ι : Type u_5
s : Set ι
α : Type u_6
inst : CompleteLattice α
f : ι → α
j : ι
hj : j ∈ s
⊢ Nonempty ι

Tactic:
have : Nonempty ι := Nonempty.intro j
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
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 α))

Tactic:
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)

Premises used: Iff.mpr, OrderTop.bddAbove, Eq.trans_le, WithBot.coe_le_coe, le_antisymm, WithBot.coe_iSup, iSup_le_iff, le_biSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
ι : Type u_5
s : Set ι
α : Type u_6
inst : CompleteLattice α
f : ι → α
j : ι
hj : j ∈ s
this : Nonempty ι
refine : ∀ (i : ι), LE.le.{u_6} (α := WithBot α) (↑(⨆ (_ : i ∈ s), f i) : WithBot α) (⨆ i ∈ s, (↑(f i) : WithBot α))
⊢ Eq.{u_6 + 1} (α := 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)

Premises used: Iff.mpr, OrderTop.bddAbove, Eq.trans_le, le_antisymm, WithBot.coe_iSup, iSup_le_iff
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
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 α))
neg : ∀ (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 α))

Tactic:
by_cases h : i ∈ s
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
ι : Type u_5
s : Set ι
α : Type u_6
inst : CompleteLattice α
f : ι → α
j : ι
hj : j ∈ s
this : Nonempty ι
i : ι
h : i ∈ s
⊢ (↑(f i) : WithBot α) ≤ ⨆ i ∈ s, (↑(f i) : WithBot α)

Tactic:
apply le_biSup _ h

Premises used: le_biSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
ι : Type u_5
s : Set ι
α : Type u_6
inst : CompleteLattice α
f : ι → α
j : ι
hj : j ∈ s
this : Nonempty ι
i : ι
h : i ∈ s
simpa : (↑(f i) : WithBot α) ≤ ⨆ i ∈ s, (↑(f i) : WithBot α)
⊢ LE.le.{u_6} (α := WithBot α) (↑(⨆ (_ : i ∈ s), f i) : WithBot α) (⨆ i ∈ s, (↑(f i) : WithBot α))

Tactic:
simpa only [iSup_pos h] using by apply le_biSup _ h

Premises used: iSup_pos
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
ι : Type u_5
s : Set ι
α : Type u_6
inst : CompleteLattice α
f : ι → α
j : ι
hj : j ∈ s
this : Nonempty ι
i : ι
h : i ∉ s
⊢ (↑⊥ : WithBot α) ≤ (↑(f j) : WithBot α)

Tactic:
simp
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
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 α))

Tactic:
simpa only [iSup_neg h] using le_trans (by simp) (le_biSup _ hj)

Premises used: iSup_neg, le_biSup, le_trans
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : Preorder α
inst_1 : InfSet α
f : ι → α
h : BddBelow (range f)
⊢ Eq.{u_1 + 1} (α := WithBot α) (↑(⨅ (i : ι), f i) : WithBot α) (⨅ (i : ι), (↑(f i) : WithBot α))

Tactic:
WithTop.coe_iSup (α := αᵒᵈ) _ h

Premises used: WithBot.some, WithBot, iInf, Set.Mem, OrderDual, WithTop.coe_iSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
ι : Type u_5
s : Set ι
α : Type u_6
inst : CompleteLattice α
f : ι → α
⊢ LE.le.{u_6} (α := WithBot α) (↑(⨅ i ∈ s, f i) : WithBot α) (⨅ i ∈ s, (↑(f i) : WithBot α))

Tactic:
simpa using fun _ ↦ biInf_le _

Premises used: biInf_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
ι : Type u_5
s : Set ι
α : Type u_6
inst : CompleteLattice α
f : ι → α
refine : ∀ (i : ι), LE.le.{u_6} (α := WithBot α) (⨅ i ∈ s, (↑(f i) : WithBot α)) (↑(⨅ (_ : i ∈ s), f i) : WithBot α)
⊢ Eq.{u_6 + 1} (α := 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

Premises used: Iff.mpr, LE.le.trans_eq, le_iInf_iff, le_antisymm
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
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 α)
neg : ∀ (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 α)

Tactic:
by_cases h : i ∈ s
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
ι : Type u_5
s : Set ι
α : Type u_6
inst : CompleteLattice α
f : ι → α
i : ι
h : i ∈ s
⊢ ⨅ i ∈ s, (↑(f i) : WithBot α) ≤ (↑(f i) : WithBot α)

Tactic:
apply biInf_le _ h

Premises used: biInf_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
ι : Type u_5
s : Set ι
α : Type u_6
inst : CompleteLattice α
f : ι → α
i : ι
h : i ∈ s
simpa : ⨅ i ∈ s, (↑(f i) : WithBot α) ≤ (↑(f i) : WithBot α)
⊢ LE.le.{u_6} (α := WithBot α) (⨅ i ∈ s, (↑(f i) : WithBot α)) (↑(⨅ (_ : i ∈ s), f i) : WithBot α)

Tactic:
simpa only [iInf_pos h] using by apply biInf_le _ h

Premises used: iInf_pos
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
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 α)

Tactic:
simp [iInf_neg h]

Premises used: iInf_neg
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
inst_1 : Nonempty ι
f : ι → α
H : BddAbove (range f)
⊢ IsLUB (range f) (⨆ (i : ι), f i)

Tactic:
isLUB_csSup (range_nonempty f) H

Premises used: iSup, Set.range_nonempty, isLUB_csSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
f : β → α
s : Set β
H : BddAbove (f '' s)
Hne : s.Nonempty
rw : IsLUB (f '' s) (sSup (f '' s))
⊢ IsLUB (f '' s) (⨆ (i : (↑s : Type u_2)), f (↑i : β))

Tactic:
rw [← sSup_image']

Premises used: sSup_image'
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
f : β → α
s : Set β
H : BddAbove (f '' s)
Hne : s.Nonempty
⊢ IsLUB (f '' s) (sSup (f '' s))

Tactic:
isLUB_csSup (Hne.image _) H

Premises used: Set.Nonempty.image, isLUB_csSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
f : β → α
s : Set β
H : BddAbove (f '' s)
Hne : s.Nonempty
⊢ IsLUB (f '' s) (sSup (f '' s))

Tactic:
exact isLUB_csSup (Hne.image _) H

Premises used: Set.Nonempty.image, isLUB_csSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
inst_1 : Nonempty ι
f : ι → α
H : BddBelow (range f)
⊢ IsGLB (range f) (⨅ (i : ι), f i)

Tactic:
isGLB_csInf (range_nonempty f) H

Premises used: iInf, isGLB_csInf, Set.range_nonempty
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
f : β → α
s : Set β
H : BddBelow (f '' s)
Hne : s.Nonempty
⊢ IsGLB (f '' s) (⨅ (i : (↑s : Type u_2)), f (↑i : β))

Tactic:
isLUB_ciSup_set (α := αᵒᵈ) H Hne

Premises used: iInf, lowerBounds, Set.Mem, setOf, upperBounds, IsGreatest, isLUB_ciSup_set, IsGLB, OrderDual
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
inst_1 : Nonempty ι
f : ι → α
a : α
hf : BddAbove (range f)
⊢ iSup f ≤ a ↔ ∀ (i : ι), f i ≤ a

Tactic:
(isLUB_le_iff <| isLUB_ciSup hf).trans forall_mem_range

Premises used: Set.forall_mem_range, isLUB_ciSup, isLUB_le_iff, Iff.trans
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
inst_1 : Nonempty ι
f : ι → α
a : α
hf : BddBelow (range f)
⊢ a ≤ iInf f ↔ ∀ (i : ι), a ≤ f i

Tactic:
(le_isGLB_iff <| isGLB_ciInf hf).trans forall_mem_range

Premises used: Set.forall_mem_range, isGLB_ciInf, Iff.trans, le_isGLB_iff
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_5
s : Set ι
f : ι → α
a : α
hs : s.Nonempty
hf : BddAbove (f '' s)
⊢ ⨆ (i : (↑s : Type u_5)), f (↑i : ι) ≤ a ↔ ∀ i ∈ s, f i ≤ a

Tactic:
(isLUB_le_iff <| isLUB_ciSup_set hf hs).trans forall_mem_image

Premises used: isLUB_le_iff, isLUB_ciSup_set, Iff.trans, Set.forall_mem_image
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_5
s : Set ι
f : ι → α
a : α
hs : s.Nonempty
hf : BddBelow (f '' s)
⊢ a ≤ ⨅ (i : (↑s : Type u_5)), f (↑i : ι) ↔ ∀ i ∈ s, a ≤ f i

Tactic:
(le_isGLB_iff <| isGLB_ciInf_set hf hs).trans forall_mem_image

Premises used: isGLB_ciInf_set, Iff.trans, le_isGLB_iff, Set.forall_mem_image
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
a : α
inst_1 : Nonempty ι
f : ι → α
H : IsLUB (range f) a
⊢ ⨆ (i : ι), f i = a

Tactic:
H.csSup_eq (range_nonempty f)

Premises used: iSup, Set.range_nonempty, IsLUB.csSup_eq
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
a : α
s : Set β
f : β → α
H : IsLUB (f '' s) a
Hne : s.Nonempty
⊢ ⨆ (i : (↑s : Type u_2)), f (↑i : β) = a

Tactic:
IsLUB.csSup_eq (image_eq_range f s ▸ H) (image_eq_range f s ▸ Hne.image f)

Premises used: iSup, Eq.rec, Set.image_eq_range, Set.Nonempty.image, IsLUB.csSup_eq
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
a : α
inst_1 : Nonempty ι
f : ι → α
H : IsGLB (range f) a
⊢ ⨅ (i : ι), f i = a

Tactic:
H.csInf_eq (range_nonempty f)

Premises used: iInf, IsGLB.csInf_eq, Set.range_nonempty
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
a : α
s : Set β
f : β → α
H : IsGLB (f '' s) a
Hne : s.Nonempty
⊢ ⨅ (i : (↑s : Type u_2)), f (↑i : β) = a

Tactic:
IsGLB.csInf_eq (image_eq_range f s ▸ H) (image_eq_range f s ▸ Hne.image f)

Premises used: iInf, Eq.rec, Set.image_eq_range, IsGLB.csInf_eq, Set.Nonempty.image
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
inst_1 : Nonempty ι
f : ι → α
c : α
H : ∀ (x : ι), f x ≤ c
rwa rwa₁ rwa₂ rwa₃ : ∀ (i : ι), f i ≤ c
⊢ ∀ b ∈ range f, b ≤ c

Tactic:
rwa [forall_mem_range]

Premises used: Set.forall_mem_range
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
f : ι → α
H : BddAbove (range f)
c : ι
⊢ f c ≤ iSup f

Tactic:
le_csSup H (mem_range_self _)

Premises used: Set.mem_range_self, iSup, le_csSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
a : α
f : ι → α
H : BddAbove (range f)
c : ι
h : a ≤ f c
⊢ a ≤ iSup f

Tactic:
le_trans h (le_ciSup H c)

Premises used: le_ciSup, le_trans
-- 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))
have :
  ∀ (a : α) (h : Membership.mem (γ := Set α) (upperBounds (⋃ (i : ι), range (f i))) a),
    BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ ⨆ (j : κ i), f i j)
⊢ BddAbove.{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 : 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)

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

Premises used: _private.0.BddAbove.range_iSup_of_iUnion_range.match_2, Eq.rec, LE.le, BddAbove, Set.Nonempty, Max.max, Exists.intro, EmptyCollection.emptyCollection, SupSet.sSup
-- 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
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 ∅
⊢ BddAbove.{u_1} (α := α) (range fun (i : ι) ↦ ⨆ (j : κ i), f i j)

Tactic:
refine ⟨a ⊔ (sSup ∅), fun x ⟨i, hx⟩ ↦ hx ▸ ?_⟩