awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
s : Set β
f : β → α
hf : BddBelow.{u_1} (α := α) (range fun (i : (↑s : Type u_2)) ↦ f (↑i : β))
hf' : LE.le.{u_1} (α := α) (⨅ (i : (↑s : Type u_2)), f (↑i : β)) (sInf ∅)
⊢ sInf (f '' s) = ⨅ a ∈ s, f a

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

Premises used: iInf, csSup_image, OrderDual
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
s : Set α
hs : BddAbove s
h : sSup ∅ ≤ sSup s
rw : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑s : Type u_1)), (↑i : α))
⊢ ⨆ i ∈ s, i = sSup s

Tactic:
rw [← csSup_image (Subtype.range_coe ▸ hs), Set.image_id']

Premises used: Set.image_id', csSup_image
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
s : Set α
hs : BddAbove s
h : sSup ∅ ≤ sSup s
⊢ sSup ∅ ≤ sSup s

Tactic:
h
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
s : Set α
hs : BddAbove s
h : sSup ∅ ≤ sSup s
h₁ : ⨆ (i : (↑s : Type u_1)), (↑i : α) = sSup s
⊢ LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑s : Type u_1)), (↑i : α))

Tactic:
convert! h
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
s : Set α
hs : BddAbove s
h : sSup ∅ ≤ sSup s
h₁ : sSup (range fun (i : (↑s : Type u_1)) ↦ (↑i : α)) = sSup s
h₂ h₃ : sSup s = sSup s
⊢ ⨆ (i : (↑s : Type u_1)), (↑i : α) = sSup s

Tactic:
rw [← sSup_range, Subtype.range_coe]

Premises used: Subtype.range_coe, sSup_range
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
s : Set α
hs : BddBelow s
h : sInf s ≤ sInf ∅
rw : LE.le.{u_1} (α := α) (⨅ (i : (↑s : Type u_1)), (↑i : α)) (sInf ∅)
⊢ ⨅ i ∈ s, i = sInf s

Tactic:
rw [← csInf_image (Subtype.range_coe ▸ hs), Set.image_id']

Premises used: csInf_image, Set.image_id'
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
s : Set α
hs : BddBelow s
h : sInf s ≤ sInf ∅
⊢ sInf s ≤ sInf ∅

Tactic:
h
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
s : Set α
hs : BddBelow s
h : sInf s ≤ sInf ∅
h₁ : ⨅ (i : (↑s : Type u_1)), (↑i : α) = sInf s
⊢ LE.le.{u_1} (α := α) (⨅ (i : (↑s : Type u_1)), (↑i : α)) (sInf ∅)

Tactic:
convert! h
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
s : Set α
hs : BddBelow s
h : sInf s ≤ sInf ∅
h₁ : sInf (range fun (i : (↑s : Type u_1)) ↦ (↑i : α)) = sInf s
h₂ h₃ : sInf s = sInf s
⊢ ⨅ (i : (↑s : Type u_1)), (↑i : α) = sInf s

Tactic:
rw [← sInf_range, Subtype.range_coe]

Premises used: Subtype.range_coe, sInf_range
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove.{u_1} (α := α) (range fun (i : (↑s : Type u_5)) ↦ g (f (↑i : ι)))
hg' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑s : Type u_5)), g (f (↑i : ι)))
inl :
  ∀ (hf : BddAbove.{u_1} (α := α) (range fun (i : (↑∅ : Type u_5)) ↦ g (f (↑i : ι))))
    (hg' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑∅ : Type u_5)), g (f (↑i : ι)))),
    Eq.{u_1 + 1} (α := α) (⨆ i ∈ f '' ∅, g i) (⨆ (x : ι), ⨆ (_ : Membership.mem (γ := Set ι) ∅ x), g (f x))
inr : ∀ (hs : s.Nonempty), Eq.{u_1 + 1} (α := α) (⨆ i ∈ f '' s, g i) (⨆ x ∈ s, g (f x))
⊢ Eq.{u_1 + 1} (α := α) (⨆ i ∈ f '' s, g i) (⨆ x ∈ s, g (f x))

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | hs)

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
f : ι → ι'
g : ι' → α
hf : BddAbove.{u_1} (α := α) (range fun (i : (↑∅ : Type u_5)) ↦ g (f (↑i : ι)))
hg' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑∅ : Type u_5)), g (f (↑i : ι)))
inl :
  Eq.{u_1 + 1} (α := α) (⨆ (i : ι'), ⨆ (_ : Membership.mem (γ := Set ι') ∅ i), g i)
    (⨆ (x : ι), ⨆ (_ : Membership.mem (γ := Set ι) ∅ x), g (f x))
inl₁ : Eq.{u_1 + 1} (α := α) (sSup ∅) (⨆ (x : ι), ⨆ (_ : Membership.mem (γ := Set ι) ∅ x), g (f x))
inl₂ inl₃ : Eq.{u_1 + 1} (α := α) (sSup ∅) (sSup ∅)
⊢ Eq.{u_1 + 1} (α := α) (⨆ i ∈ f '' ∅, g i) (⨆ (x : ι), ⨆ (_ : Membership.mem (γ := Set ι) ∅ x), g (f x))

Tactic:
rw [Set.image_empty, cbiSup_empty, cbiSup_empty]

Premises used: cbiSup_empty, Set.image_empty
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove.{u_1} (α := α) (range fun (i : (↑s : Type u_5)) ↦ g (f (↑i : ι)))
hg' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑s : Type u_5)), g (f (↑i : ι)))
hs : s.Nonempty
⊢ BddAbove.{u_1} (α := α) (range fun (i : (↑(f '' s) : Type u_6)) ↦ g (↑i : ι'))

Tactic:
simpa [bddAbove_def] using hf

Premises used: bddAbove_def
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove.{u_1} (α := α) (range fun (i : (↑s : Type u_5)) ↦ g (f (↑i : ι)))
hg' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑s : Type u_5)), g (f (↑i : ι)))
hs : s.Nonempty
⊢ BddAbove.{u_1} (α := α) (range fun (i : (↑(f '' s) : Type u_6)) ↦ g (↑i : ι'))

Tactic:
have hg : BddAbove (Set.range fun i : f '' s ↦ g i) := by
    simpa [bddAbove_def] using hf
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove.{u_1} (α := α) (range fun (i : (↑s : Type u_5)) ↦ g (f (↑i : ι)))
hg' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑s : Type u_5)), g (f (↑i : ι)))
hs : s.Nonempty
hg : BddAbove.{u_1} (α := α) (range fun (i : (↑(f '' s) : Type u_6)) ↦ g (↑i : ι'))
⊢ LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑(f '' s) : Type u_6)), g (↑i : ι'))

Tactic:
hg'.trans ?_

Premises used: LE.le.trans
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove.{u_1} (α := α) (range fun (i : (↑s : Type u_5)) ↦ g (f (↑i : ι)))
hg' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑s : Type u_5)), g (f (↑i : ι)))
hs : s.Nonempty
hg : BddAbove.{u_1} (α := α) (range fun (i : (↑(f '' s) : Type u_6)) ↦ g (↑i : ι'))
refine : LE.le.{u_1} (α := α) (⨆ (i : (↑s : Type u_5)), g (f (↑i : ι))) (⨆ (i : (↑(f '' s) : Type u_6)), g (↑i : ι'))
⊢ LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑(f '' s) : Type u_6)), g (↑i : ι'))

Tactic:
refine hg'.trans ?_

Premises used: LE.le.trans
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove.{u_1} (α := α) (range fun (i : (↑s : Type u_5)) ↦ g (f (↑i : ι)))
hg' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑s : Type u_5)), g (f (↑i : ι)))
hs : s.Nonempty
hg : BddAbove.{u_1} (α := α) (range fun (i : (↑(f '' s) : Type u_6)) ↦ g (↑i : ι'))
⊢ Nonempty.{u_5 + 1} (↑s : Type u_5)

Tactic:
have : Nonempty s := Set.Nonempty.to_subtype hs
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove.{u_1} (α := α) (range fun (i : (↑s : Type u_5)) ↦ g (f (↑i : ι)))
hg' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑s : Type u_5)), g (f (↑i : ι)))
hs : s.Nonempty
hg : BddAbove.{u_1} (α := α) (range fun (i : (↑(f '' s) : Type u_6)) ↦ g (↑i : ι'))
this : Nonempty.{u_5 + 1} (↑s : Type u_5)
⊢ LE.le.{u_1} (α := α) (⨆ (i : (↑s : Type u_5)), g (f (↑i : ι))) (⨆ (i : (↑(f '' s) : Type u_6)), g (↑i : ι'))

Tactic:
ciSup_le ?_

Premises used: ciSup_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove.{u_1} (α := α) (range fun (i : (↑s : Type u_5)) ↦ g (f (↑i : ι)))
hg' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑s : Type u_5)), g (f (↑i : ι)))
hs : s.Nonempty
hg : BddAbove.{u_1} (α := α) (range fun (i : (↑(f '' s) : Type u_6)) ↦ g (↑i : ι'))
this : Nonempty.{u_5 + 1} (↑s : Type u_5)
refine : ∀ (x : (↑s : Type u_5)), g (f (↑x : ι)) ≤ ⨆ (i : (↑(f '' s) : Type u_6)), g (↑i : ι')
⊢ LE.le.{u_1} (α := α) (⨆ (i : (↑s : Type u_5)), g (f (↑i : ι))) (⨆ (i : (↑(f '' s) : Type u_6)), g (↑i : ι'))

Tactic:
refine ciSup_le ?_

Premises used: ciSup_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove.{u_1} (α := α) (range fun (i : (↑s : Type u_5)) ↦ g (f (↑i : ι)))
hg' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑s : Type u_5)), g (f (↑i : ι)))
hs : s.Nonempty
hg : BddAbove.{u_1} (α := α) (range fun (i : (↑(f '' s) : Type u_6)) ↦ g (↑i : ι'))
this : Nonempty.{u_5 + 1} (↑s : Type u_5)
i : ι
h : i ∈ s
⊢ f i ∈ f '' s

Tactic:
have : f i ∈ f '' s := Set.mem_image_of_mem _ h
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove.{u_1} (α := α) (range fun (i : (↑s : Type u_5)) ↦ g (f (↑i : ι)))
hg' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑s : Type u_5)), g (f (↑i : ι)))
hs : s.Nonempty
hg : BddAbove.{u_1} (α := α) (range fun (i : (↑(f '' s) : Type u_6)) ↦ g (↑i : ι'))
this_1 : Nonempty.{u_5 + 1} (↑s : Type u_5)
i : ι
h : i ∈ s
this : f i ∈ f '' s
⊢ g (↑(Subtype.mk (p := fun (x : ι') ↦ x ∈ f '' s) (f i) this) : ι') =
    g (f (↑(Subtype.mk (p := Membership.mem s) i h) : ι))

Tactic:
simp
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove.{u_1} (α := α) (range fun (i : (↑s : Type u_5)) ↦ g (f (↑i : ι)))
hg' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑s : Type u_5)), g (f (↑i : ι)))
hs : s.Nonempty
hg : BddAbove.{u_1} (α := α) (range fun (i : (↑(f '' s) : Type u_6)) ↦ g (↑i : ι'))
this_1 : Nonempty.{u_5 + 1} (↑s : Type u_5)
i : ι
h : i ∈ s
this : f i ∈ f '' s
⊢ ∃ (t : (↑(f '' s) : Type u_6)), g (↑t : ι') = g (f (↑(Subtype.mk (p := Membership.mem s) i h) : ι))

Tactic:
exact ⟨⟨f i, this⟩, by simp⟩
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove.{u_1} (α := α) (range fun (i : (↑s : Type u_5)) ↦ g (f (↑i : ι)))
hg' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑s : Type u_5)), g (f (↑i : ι)))
hs : s.Nonempty
hg : BddAbove.{u_1} (α := α) (range fun (i : (↑(f '' s) : Type u_6)) ↦ g (↑i : ι'))
this : Nonempty.{u_5 + 1} (↑s : Type u_5)
i : ι
h : i ∈ s
obtain :
  ∀ (t : (↑(f '' s) : Type u_6)) (ht : g (↑t : ι') = g (f (↑(Subtype.mk (p := Membership.mem s) i h) : ι))),
    g (f (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) : ι)) ≤ ⨆ (i : (↑(f '' s) : Type u_6)), g (↑i : ι')
⊢ g (f (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) : ι)) ≤ ⨆ (i : (↑(f '' s) : Type u_6)), g (↑i : ι')

Tactic:
obtain ⟨t, ht⟩ : ∃ t : f '' s, g t = g (f (Subtype.mk i h)) := by
      have : f i ∈ f '' s := Set.mem_image_of_mem _ h
      exact ⟨⟨f i, this⟩, by simp⟩

Premises used: Subtype.mk, Subtype.val
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove.{u_1} (α := α) (range fun (i : (↑s : Type u_5)) ↦ g (f (↑i : ι)))
hg' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑s : Type u_5)), g (f (↑i : ι)))
hs : s.Nonempty
hg : BddAbove.{u_1} (α := α) (range fun (i : (↑(f '' s) : Type u_6)) ↦ g (↑i : ι'))
this : Nonempty.{u_5 + 1} (↑s : Type u_5)
i : ι
h : i ∈ s
t : (↑(f '' s) : Type u_6)
ht : g (↑t : ι') = g (f (↑(Subtype.mk (p := Membership.mem s) i h) : ι))
rw : g (↑t : ι') ≤ ⨆ (i : (↑(f '' s) : Type u_6)), g (↑i : ι')
⊢ g (f (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) : ι)) ≤ ⨆ (i : (↑(f '' s) : Type u_6)), g (↑i : ι')

Tactic:
rw [← ht]
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove.{u_1} (α := α) (range fun (i : (↑s : Type u_5)) ↦ g (f (↑i : ι)))
hg' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑s : Type u_5)), g (f (↑i : ι)))
hs : s.Nonempty
hg : BddAbove.{u_1} (α := α) (range fun (i : (↑(f '' s) : Type u_6)) ↦ g (↑i : ι'))
this : Nonempty.{u_5 + 1} (↑s : Type u_5)
i : ι
h : i ∈ s
t : (↑(f '' s) : Type u_6)
ht : g (↑t : ι') = g (f (↑(Subtype.mk (p := Membership.mem s) i h) : ι))
⊢ g (↑t : ι') ≤ ⨆ (i : (↑(f '' s) : Type u_6)), g (↑i : ι')

Tactic:
le_ciSup_set ?_ t.prop

Premises used: le_ciSup_set, Subtype.prop
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove.{u_1} (α := α) (range fun (i : (↑s : Type u_5)) ↦ g (f (↑i : ι)))
hg' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑s : Type u_5)), g (f (↑i : ι)))
hs : s.Nonempty
hg : BddAbove.{u_1} (α := α) (range fun (i : (↑(f '' s) : Type u_6)) ↦ g (↑i : ι'))
this : Nonempty.{u_5 + 1} (↑s : Type u_5)
i : ι
h : i ∈ s
t : (↑(f '' s) : Type u_6)
ht : g (↑t : ι') = g (f (↑(Subtype.mk (p := Membership.mem s) i h) : ι))
refine : BddAbove (g '' f '' s)
⊢ g (↑t : ι') ≤ ⨆ (i : (↑(f '' s) : Type u_6)), g (↑i : ι')

Tactic:
refine le_ciSup_set ?_ t.prop

Premises used: le_ciSup_set, Subtype.prop
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove.{u_1} (α := α) (range fun (i : (↑s : Type u_5)) ↦ g (f (↑i : ι)))
hg' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑s : Type u_5)), g (f (↑i : ι)))
hs : s.Nonempty
hg : BddAbove.{u_1} (α := α) (range fun (i : (↑(f '' s) : Type u_6)) ↦ g (↑i : ι'))
this : Nonempty.{u_5 + 1} (↑s : Type u_5)
i : ι
h : i ∈ s
t : (↑(f '' s) : Type u_6)
ht : g (↑t : ι') = g (f (↑(Subtype.mk (p := Membership.mem s) i h) : ι))
⊢ BddAbove (g '' f '' s)

Tactic:
simpa [bddAbove_def] using hf

Premises used: bddAbove_def
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove.{u_1} (α := α) (range fun (i : (↑s : Type u_5)) ↦ g (f (↑i : ι)))
hg' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑s : Type u_5)), g (f (↑i : ι)))
hs : s.Nonempty
hg : BddAbove.{u_1} (α := α) (range fun (i : (↑(f '' s) : Type u_6)) ↦ g (↑i : ι'))
⊢ LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑(f '' s) : Type u_6)), g (↑i : ι'))

Tactic:
have hf' : sSup ∅ ≤ ⨆ i : f '' s, g i := by
    refine hg'.trans ?_
    have : Nonempty s := Set.Nonempty.to_subtype hs
    refine ciSup_le ?_
    intro ⟨i, h⟩
    obtain ⟨t, ht⟩ : ∃ t : f '' s, g t = g (f (Subtype.mk i h)) := by
      have : f i ∈ f '' s := Set.mem_image_of_mem _ h
      exact ⟨⟨f i, this⟩, by simp⟩
    rw [← ht]
    refine le_ciSup_set ?_ t.prop
    simpa [bddAbove_def] using hf
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove.{u_1} (α := α) (range fun (i : (↑s : Type u_5)) ↦ g (f (↑i : ι)))
hg' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑s : Type u_5)), g (f (↑i : ι)))
hs : s.Nonempty
hg : BddAbove.{u_1} (α := α) (range fun (i : (↑(f '' s) : Type u_6)) ↦ g (↑i : ι'))
hf' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑(f '' s) : Type u_6)), g (↑i : ι'))
inr : sSup (g '' f '' s) = ⨆ x ∈ s, g (f x)
inr₁ : sSup (g '' f '' s) = sSup ((fun (x : ι) ↦ g (f x)) '' s)
inr₂ : sSup (g ∘ f '' s) = sSup ((fun (x : ι) ↦ g (f x)) '' s)
inr₃ inr₄ : Eq.{u_1 + 1} (α := α) (sSup ((fun (x : ι) ↦ g (f x)) '' s)) (sSup ((fun (x : ι) ↦ g (f x)) '' s))
⊢ Eq.{u_1 + 1} (α := α) (⨆ i ∈ f '' s, g i) (⨆ x ∈ s, g (f x))

Tactic:
rw [← csSup_image hg hf', ← csSup_image hf hg', ← Set.image_comp, comp_def]

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

Tactic:
ciSup_image (α := αᵒᵈ) hf hg'

Premises used: iInf, ciSup_image, OrderDual
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Exists p → α
pos : ∀ (h : Exists p), LE.le.{u_1} (α := α) (⨆ (ih : Exists p), f ih) (⨆ (i : ι), ⨆ (h : p i), f ⋯)
neg : ∀ (h : ∀ (x : ι), ¬p x), LE.le.{u_1} (α := α) (⨆ (ih : Exists p), f ih) (⨆ (i : ι), ⨆ (h : p i), f ⋯)
⊢ LE.le.{u_1} (α := α) (⨆ (ih : Exists p), f ih) (⨆ (i : ι), ⨆ (h : p i), f ⋯)

Tactic:
by_cases! h : Exists p

Premises used: Exists
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Exists p → α
h : Exists p
⊢ Nonempty (Exists p)

Tactic:
have : Nonempty <| Exists p := ⟨h⟩
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Exists p → α
h : Exists p
this : Nonempty (Exists p)
⊢ LE.le.{u_1} (α := α) (⨆ (ih : Exists p), f ih) (⨆ (i : ι), ⨆ (h : p i), f ⋯)

Tactic:
ciSup_le fun ⟨i, hi⟩ ↦ le_ciSup₂ (f := fun _ _ ↦ _) ⟨f ⟨i, hi⟩, ?_⟩ i hi

Premises used: le_ciSup₂, iSup, LE.le, Exists.intro, _private.0.ciSup_exists_le.match_1, ciSup_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Exists p → α
h : Exists p
this : Nonempty (Exists p)
pos :
  Exists p →
    ∀ (i : ι) (hi : p i),
      Membership.mem (γ := Set α) (upperBounds (⋃ (i_1 : ι), range (ι := p i_1) ((fun (x : ι) (x_1 : p x) ↦ f ⋯) i_1)))
        (f ⋯)
⊢ LE.le.{u_1} (α := α) (⨆ (ih : Exists p), f ih) (⨆ (i : ι), ⨆ (h : p i), f ⋯)

Tactic:
refine ciSup_le fun ⟨i, hi⟩ ↦ le_ciSup₂ (f := fun _ _ ↦ _) ⟨f ⟨i, hi⟩, ?_⟩ i hi

Premises used: ciSup_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Exists p → α
h : Exists p
this : Nonempty (Exists p)
h_1 : Exists p
i : ι
hi : p i
j : ι
hj : p j
⊢ LE.le.{u_1} (α := α) ((fun (x : ι) (x_1 : p x) ↦ f ⋯) j hj) ((fun (x : ι) (x_1 : p x) ↦ f ⋯) j hj)

Tactic:
rfl
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Exists p → α
h : ∀ (x : ι), ¬p x
neg : IsEmpty ι → LE.le.{u_1} (α := α) (⨆ (ih : Exists p), f ih) (⨆ (i : ι), ⨆ (h : p i), f ⋯)
neg₁ : Nonempty ι → LE.le.{u_1} (α := α) (⨆ (ih : Exists p), f ih) (⨆ (i : ι), ⨆ (h : p i), f ⋯)
⊢ LE.le.{u_1} (α := α) (⨆ (ih : Exists p), f ih) (⨆ (i : ι), ⨆ (h : p i), f ⋯)

Tactic:
cases isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Exists p → α
h : ∀ (x : ι), ¬p x
h_1 : IsEmpty ι
⊢ LE.le.{u_1} (α := α) (⨆ (ih : Exists p), f ih) (⨆ (i : ι), ⨆ (h : p i), f ⋯)

Tactic:
simp [h, iSup_of_empty', ciSup_const]

Premises used: ciSup_const, iSup_of_empty'
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Exists p → α
h : ∀ (x : ι), ¬p x
h_1 : Nonempty ι
⊢ LE.le.{u_1} (α := α) (⨆ (ih : Exists p), f ih) (⨆ (i : ι), ⨆ (h : p i), f ⋯)

Tactic:
simp [h, iSup_of_empty', ciSup_const]

Premises used: ciSup_const, iSup_of_empty'
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Exists p → α
⊢ LE.le.{u_1} (α := α) (⨅ (i : ι), ⨅ (h : p i), f ⋯) (⨅ (ih : Exists p), f ih)

Tactic:
ciSup_exists_le (α := αᵒᵈ)

Premises used: iInf, OrderDual, ciSup_exists_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
p q : Prop
f : p ∧ q → α
pos : ∀ (hp : p), Eq.{u_1 + 1} (α := α) (⨆ (ih : p ∧ q), f ih) (⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯)
neg : ∀ (hp : ¬p), Eq.{u_1 + 1} (α := α) (⨆ (ih : p ∧ q), f ih) (⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (ih : p ∧ q), f ih) (⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯)

Tactic:
by_cases hp : p
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
p q : Prop
f : p ∧ q → α
hp : p
pos : ∀ (hq : q), Eq.{u_1 + 1} (α := α) (⨆ (ih : p ∧ q), f ih) (⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯)
neg : ∀ (hq : ¬q), Eq.{u_1 + 1} (α := α) (⨆ (ih : p ∧ q), f ih) (⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (ih : p ∧ q), f ih) (⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯)

Tactic:
by_cases hq : q
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
p q : Prop
f : p ∧ q → α
hp : ¬p
pos : ∀ (hq : q), Eq.{u_1 + 1} (α := α) (⨆ (ih : p ∧ q), f ih) (⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯)
neg : ∀ (hq : ¬q), Eq.{u_1 + 1} (α := α) (⨆ (ih : p ∧ q), f ih) (⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (ih : p ∧ q), f ih) (⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯)

Tactic:
by_cases hq : q
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
p q : Prop
f : p ∧ q → α
hp : p
hq : q
⊢ Eq.{u_1 + 1} (α := α) (⨆ (ih : p ∧ q), f ih) (⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯)

Tactic:
simp [hp, hq, iSup_of_empty']

Premises used: iSup_of_empty'
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
p q : Prop
f : p ∧ q → α
hp : p
hq : ¬q
⊢ Eq.{u_1 + 1} (α := α) (⨆ (ih : p ∧ q), f ih) (⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯)

Tactic:
simp [hp, hq, iSup_of_empty']

Premises used: iSup_of_empty'
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
p q : Prop
f : p ∧ q → α
hp : ¬p
hq : q
⊢ Eq.{u_1 + 1} (α := α) (⨆ (ih : p ∧ q), f ih) (⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯)

Tactic:
simp [hp, hq, iSup_of_empty']

Premises used: iSup_of_empty'
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
p q : Prop
f : p ∧ q → α
hp : ¬p
hq : ¬q
⊢ Eq.{u_1 + 1} (α := α) (⨆ (ih : p ∧ q), f ih) (⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯)

Tactic:
simp [hp, hq, iSup_of_empty']

Premises used: iSup_of_empty'
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
p q : Prop
f : p ∧ q → α
⊢ Eq.{u_1 + 1} (α := α) (⨅ (ih : p ∧ q), f ih) (⨅ (h₁ : p), ⨅ (h₂ : q), f ⋯)

Tactic:
ciSup_and (α := αᵒᵈ)

Premises used: iInf, ciSup_and, OrderDual
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
f g : ι → α
pos :
  ∀ (hf : ¬BddAbove (range f)),
    LE.le.{u_1} (α := α) (⨆ (x : ι), max (f x) (g x)) (max (⨆ (x : ι), f x) (⨆ (x : ι), g x))
neg :
  ∀ (hf : BddAbove (range f)), LE.le.{u_1} (α := α) (⨆ (x : ι), max (f x) (g x)) (max (⨆ (x : ι), f x) (⨆ (x : ι), g x))
⊢ LE.le.{u_1} (α := α) (⨆ (x : ι), max (f x) (g x)) (max (⨆ (x : ι), f x) (⨆ (x : ι), g x))

Tactic:
by_cases! hf : ¬BddAbove (range f)

Premises used: BddAbove, Set.range