-- Mathlib/Algebra/Order/GroupWithZero/Bounds.lean
/-- A variant of `BddAbove.range_comp` that assumes that `f` is nonnegative and `g` is monotone on
  nonnegative values. -/
lemma BddAbove.range_comp_of_nonneg {α β γ : Type*} [Nonempty α] [Preorder β] [Zero β] [Preorder γ]
    {f : α → β} {g : β → γ} (hf : BddAbove (range f)) (hf0 : 0 ≤ f)
    (hg : MonotoneOn g {x : β | 0 ≤ x}) : BddAbove (range (fun x => g (f x)))

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Nonempty α
inst✝² : Preorder β
inst✝¹ : Zero β
inst✝ : Preorder γ
f : α → β
g : β → γ
hf : BddAbove (range f)
hf0 : 0 ≤ f
hg : MonotoneOn g {x | 0 ≤ x}
⊢ BddAbove (g '' range f)

Tactic:
apply hg.map_bddAbove (by rintro x ⟨a, rfl⟩; exact hf0 a)

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Nonempty α
inst✝² : Preorder β
inst✝¹ : Zero β
inst✝ : Preorder γ
f : α → β
g : β → γ
hf : BddAbove (range f)
hf0 : 0 ≤ f
hg : MonotoneOn g {x | 0 ≤ x}
⊢ (upperBounds (range f) ∩ {x | 0 ≤ x}).Nonempty

Proof state:
case right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Nonempty α
inst✝² : Preorder β
inst✝¹ : Zero β
inst✝ : Preorder γ
f : α → β
g : β → γ
hf0 : 0 ≤ f
hg : MonotoneOn g {x | 0 ≤ x}
b : β
hb : b ∈ upperBounds (range f)
⊢ b ∈ {x | 0 ≤ x}

Tactic:
simp only [mem_upperBounds, mem_range, forall_exists_index, forall_apply_eq_imp_iff] at hb

Result:
case right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Nonempty α
inst✝² : Preorder β
inst✝¹ : Zero β
inst✝ : Preorder γ
f : α → β
g : β → γ
hf0 : 0 ≤ f
hg : MonotoneOn g {x | 0 ≤ x}
b : β
hb : ∀ (a : α), f a ≤ b
⊢ b ∈ {x | 0 ≤ x}

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Nonempty α
inst✝² : Preorder β
inst✝¹ : Zero β
inst✝ : Preorder γ
f : α → β
g : β → γ
hf : BddAbove (range f)
hf0 : 0 ≤ f
hg : MonotoneOn g {x | 0 ≤ x}
⊢ BddAbove (range fun x => g (f x))

Tactic:
suffices hg' : BddAbove (g '' range f) by
  rwa [← Function.comp_def, Set.range_comp]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Nonempty α
inst✝² : Preorder β
inst✝¹ : Zero β
inst✝ : Preorder γ
f : α → β
g : β → γ
hf : BddAbove (range f)
hf0 : 0 ≤ f
hg : MonotoneOn g {x | 0 ≤ x}
⊢ BddAbove (g '' range f)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Nonempty α
inst✝² : Preorder β
inst✝¹ : Zero β
inst✝ : Preorder γ
f : α → β
g : β → γ
hf : BddAbove (range f)
hf0 : 0 ≤ f
hg : MonotoneOn g {x | 0 ≤ x}
hg' : BddAbove (g '' range f)
⊢ BddAbove (range fun x => g (f x))

Tactic:
rwa [← Function.comp_def, Set.range_comp]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Nonempty α
inst✝² : Preorder β
inst✝¹ : Zero β
inst✝ : Preorder γ
f : α → β
g : β → γ
hf : BddAbove (range f)
hf0 : 0 ≤ f
hg : MonotoneOn g {x | 0 ≤ x}
⊢ range f ⊆ {x | 0 ≤ x}

Tactic:
rintro x ⟨a, rfl⟩

Result:
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Nonempty α
inst✝² : Preorder β
inst✝¹ : Zero β
inst✝ : Preorder γ
f : α → β
g : β → γ
hf : BddAbove (range f)
hf0 : 0 ≤ f
hg : MonotoneOn g {x | 0 ≤ x}
a : α
⊢ f a ∈ {x | 0 ≤ x}

Proof state:
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Nonempty α
inst✝² : Preorder β
inst✝¹ : Zero β
inst✝ : Preorder γ
f : α → β
g : β → γ
hf : BddAbove (range f)
hf0 : 0 ≤ f
hg : MonotoneOn g {x | 0 ≤ x}
a : α
⊢ f a ∈ {x | 0 ≤ x}

Tactic:
exact hf0 a

Result:
no goals

Proof state:
case right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Nonempty α
inst✝² : Preorder β
inst✝¹ : Zero β
inst✝ : Preorder γ
f : α → β
g : β → γ
hf0 : 0 ≤ f
hg : MonotoneOn g {x | 0 ≤ x}
b : β
hb : ∀ (a : α), f a ≤ b
⊢ b ∈ {x | 0 ≤ x}

Tactic:
exact le_trans (hf0 Classical.ofNonempty) (hb Classical.ofNonempty)

Result:
no goals

Proof state:
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Nonempty α
inst✝² : Preorder β
inst✝¹ : Zero β
inst✝ : Preorder γ
f : α → β
g : β → γ
hf0 : 0 ≤ f
hg : MonotoneOn g {x | 0 ≤ x}
b : β
hb : b ∈ upperBounds (range f)
⊢ (upperBounds (range f) ∩ {x | 0 ≤ x}).Nonempty

Tactic:
use b, hb

Result:
case right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Nonempty α
inst✝² : Preorder β
inst✝¹ : Zero β
inst✝ : Preorder γ
f : α → β
g : β → γ
hf0 : 0 ≤ f
hg : MonotoneOn g {x | 0 ≤ x}
b : β
hb : b ∈ upperBounds (range f)
⊢ b ∈ {x | 0 ≤ x}

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Nonempty α
inst✝² : Preorder β
inst✝¹ : Zero β
inst✝ : Preorder γ
f : α → β
g : β → γ
hf : BddAbove (range f)
hf0 : 0 ≤ f
hg : MonotoneOn g {x | 0 ≤ x}
⊢ (upperBounds (range f) ∩ {x | 0 ≤ x}).Nonempty

Tactic:
obtain ⟨b, hb⟩ := hf

Result:
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Nonempty α
inst✝² : Preorder β
inst✝¹ : Zero β
inst✝ : Preorder γ
f : α → β
g : β → γ
hf0 : 0 ≤ f
hg : MonotoneOn g {x | 0 ≤ x}
b : β
hb : b ∈ upperBounds (range f)
⊢ (upperBounds (range f) ∩ {x | 0 ≤ x}).Nonempty