-- Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
lemma MonotoneOn.csInf_eq_of_subset_of_forall_exists_le
    [Preorder α] [ConditionallyCompleteLattice β] {f : α → β}
    {s t : Set α} (ht : BddBelow (f '' t)) (hf : MonotoneOn f t)
    (hst : s ⊆ t) (h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y) :
    sInf (f '' s) = sInf (f '' t)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
⊢ sInf (f '' s) ≤ sInf (f '' t)

Tactic:
refine le_csInf ((hs.mono hst).image f) ?_

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
⊢ ∀ b ∈ f '' t, sInf (f '' s) ≤ b

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
⊢ sInf (f '' s) = sInf (f '' t)

Tactic:
obtain rfl | hs := Set.eq_empty_or_nonempty s

Result:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : ∅ ⊆ t
h : ∀ y ∈ t, ∃ x ∈ ∅, x ≤ y
⊢ sInf (f '' ∅) = sInf (f '' t)

case inr
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
⊢ sInf (f '' s) = sInf (f '' t)

Proof state:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
ht : BddBelow (f '' ∅)
hf : MonotoneOn f ∅
hst : ∅ ⊆ ∅
h : ∀ y ∈ ∅, ∃ x ∈ ∅, x ≤ y
⊢ sInf (f '' ∅) = sInf (f '' ∅)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
⊢ ∀ b ∈ f '' t, sInf (f '' s) ≤ b

Tactic:
simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
⊢ ∀ a ∈ t, sInf (f '' s) ≤ f a

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : ∅ ⊆ t
h : ∀ y ∈ t, ∃ x ∈ ∅, x ≤ y
⊢ t = ∅

Tactic:
simpa [Set.eq_empty_iff_forall_not_mem] using h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
⊢ ∀ a ∈ t, sInf (f '' s) ≤ f a

Tactic:
intro a ha

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
a : α
ha : a ∈ t
⊢ sInf (f '' s) ≤ f a

Proof state:
case inr
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
⊢ sInf (f '' s) = sInf (f '' t)

Tactic:
apply le_antisymm _ (csInf_le_csInf ht (hs.image _) (image_subset _ hst))

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
⊢ sInf (f '' s) ≤ sInf (f '' t)

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
a : α
ha : a ∈ t
x : α
hxs : x ∈ s
hxa : x ≤ a
⊢ sInf (f '' s) ≤ f a

Tactic:
exact csInf_le_of_le (ht.mono (image_subset _ hst)) ⟨x, hxs, rfl⟩ (hf (hst hxs) ha hxa)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
a : α
ha : a ∈ t
⊢ sInf (f '' s) ≤ f a

Tactic:
obtain ⟨x, hxs, hxa⟩ := h a ha

Result:
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
a : α
ha : a ∈ t
x : α
hxs : x ∈ s
hxa : x ≤ a
⊢ sInf (f '' s) ≤ f a

Proof state:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : ∅ ⊆ t
h : ∀ y ∈ t, ∃ x ∈ ∅, x ≤ y
⊢ sInf (f '' ∅) = sInf (f '' t)

Tactic:
obtain rfl : t = ∅ := by simpa [Set.eq_empty_iff_forall_not_mem] using h

Result:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
ht : BddBelow (f '' ∅)
hf : MonotoneOn f ∅
hst : ∅ ⊆ ∅
h : ∀ y ∈ ∅, ∃ x ∈ ∅, x ≤ y
⊢ sInf (f '' ∅) = sInf (f '' ∅)