-- Mathlib/CategoryTheory/Filtered/Final.lean
lemma Monotone.final_functor_iff {J₁ J₂ : Type*} [Preorder J₁] [Preorder J₂]
    [IsDirected J₁ (· ≤ · )] {f : J₁ → J₂} (hf : Monotone f) :
    hf.functor.Final ↔ ∀ (j₂ : J₂), ∃ (j₁ : J₁), j₂ ≤ f j₁

Proof state:
case mpr.left
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsDirected J₁ fun x1 x2 => x1 ≤ x2
f : J₁ → J₂
hf : Monotone f
h : ∀ (j₂ : J₂), ∃ j₁, j₂ ≤ f j₁
j₂ : J₂
⊢ ∃ c, Nonempty (j₂ ⟶ hf.functor.obj c)

Tactic:
obtain ⟨j₁, h₁⟩ := h j₂

Result:
case mpr.left.intro
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsDirected J₁ fun x1 x2 => x1 ≤ x2
f : J₁ → J₂
hf : Monotone f
h : ∀ (j₂ : J₂), ∃ j₁, j₂ ≤ f j₁
j₂ : J₂
j₁ : J₁
h₁ : j₂ ≤ f j₁
⊢ ∃ c, Nonempty (j₂ ⟶ hf.functor.obj c)

Proof state:
case mpr.left.intro
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsDirected J₁ fun x1 x2 => x1 ≤ x2
f : J₁ → J₂
hf : Monotone f
h : ∀ (j₂ : J₂), ∃ j₁, j₂ ≤ f j₁
j₂ : J₂
j₁ : J₁
h₁ : j₂ ≤ f j₁
⊢ ∃ c, Nonempty (j₂ ⟶ hf.functor.obj c)

Tactic:
exact ⟨j₁, ⟨homOfLE h₁⟩⟩

Result:
no goals

Proof state:
case mpr
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsDirected J₁ fun x1 x2 => x1 ≤ x2
f : J₁ → J₂
hf : Monotone f
h : ∀ (j₂ : J₂), ∃ j₁, j₂ ≤ f j₁
⊢ (∀ (d : J₂), ∃ c, Nonempty (d ⟶ hf.functor.obj c)) ∧
    ∀ {d : J₂} {c : J₁} (s s' : d ⟶ hf.functor.obj c), ∃ c' t, s ≫ hf.functor.map t = s' ≫ hf.functor.map t

Tactic:
constructor

Result:
case mpr.left
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsDirected J₁ fun x1 x2 => x1 ≤ x2
f : J₁ → J₂
hf : Monotone f
h : ∀ (j₂ : J₂), ∃ j₁, j₂ ≤ f j₁
⊢ ∀ (d : J₂), ∃ c, Nonempty (d ⟶ hf.functor.obj c)

case mpr.right
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsDirected J₁ fun x1 x2 => x1 ≤ x2
f : J₁ → J₂
hf : Monotone f
h : ∀ (j₂ : J₂), ∃ j₁, j₂ ≤ f j₁
⊢ ∀ {d : J₂} {c : J₁} (s s' : d ⟶ hf.functor.obj c), ∃ c' t, s ≫ hf.functor.map t = s' ≫ hf.functor.map t

Proof state:
case mpr.right
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsDirected J₁ fun x1 x2 => x1 ≤ x2
f : J₁ → J₂
hf : Monotone f
h : ∀ (j₂ : J₂), ∃ j₁, j₂ ≤ f j₁
⊢ ∀ {d : J₂} {c : J₁} (s s' : d ⟶ hf.functor.obj c), ∃ c' t, s ≫ hf.functor.map t = s' ≫ hf.functor.map t

Tactic:
intro _ c _ _

Result:
case mpr.right
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsDirected J₁ fun x1 x2 => x1 ≤ x2
f : J₁ → J₂
hf : Monotone f
h : ∀ (j₂ : J₂), ∃ j₁, j₂ ≤ f j₁
d✝ : J₂
c : J₁
s✝ s'✝ : d✝ ⟶ hf.functor.obj c
⊢ ∃ c' t, s✝ ≫ hf.functor.map t = s'✝ ≫ hf.functor.map t

Proof state:
case mpr.left
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsDirected J₁ fun x1 x2 => x1 ≤ x2
f : J₁ → J₂
hf : Monotone f
h : ∀ (j₂ : J₂), ∃ j₁, j₂ ≤ f j₁
⊢ ∀ (d : J₂), ∃ c, Nonempty (d ⟶ hf.functor.obj c)

Tactic:
intro j₂

Result:
case mpr.left
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsDirected J₁ fun x1 x2 => x1 ≤ x2
f : J₁ → J₂
hf : Monotone f
h : ∀ (j₂ : J₂), ∃ j₁, j₂ ≤ f j₁
j₂ : J₂
⊢ ∃ c, Nonempty (j₂ ⟶ hf.functor.obj c)

Proof state:
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsDirected J₁ fun x1 x2 => x1 ≤ x2
f : J₁ → J₂
hf : Monotone f
⊢ hf.functor.Final ↔ ∀ (j₂ : J₂), ∃ j₁, j₂ ≤ f j₁

Tactic:
rw [Functor.final_iff_of_isFiltered]

Result:
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsDirected J₁ fun x1 x2 => x1 ≤ x2
f : J₁ → J₂
hf : Monotone f
⊢ ((∀ (d : J₂), ∃ c, Nonempty (d ⟶ hf.functor.obj c)) ∧
      ∀ {d : J₂} {c : J₁} (s s' : d ⟶ hf.functor.obj c), ∃ c' t, s ≫ hf.functor.map t = s' ≫ hf.functor.map t) ↔
    ∀ (j₂ : J₂), ∃ j₁, j₂ ≤ f j₁

Proof state:
case mpr.right
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsDirected J₁ fun x1 x2 => x1 ≤ x2
f : J₁ → J₂
hf : Monotone f
h : ∀ (j₂ : J₂), ∃ j₁, j₂ ≤ f j₁
d✝ : J₂
c : J₁
s✝ s'✝ : d✝ ⟶ hf.functor.obj c
⊢ ∃ c' t, s✝ ≫ hf.functor.map t = s'✝ ≫ hf.functor.map t

Tactic:
exact ⟨c, 𝟙 _, rfl⟩

Result:
no goals

Proof state:
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsDirected J₁ fun x1 x2 => x1 ≤ x2
f : J₁ → J₂
hf : Monotone f
⊢ ((∀ (d : J₂), ∃ c, Nonempty (d ⟶ hf.functor.obj c)) ∧
      ∀ {d : J₂} {c : J₁} (s s' : d ⟶ hf.functor.obj c), ∃ c' t, s ≫ hf.functor.map t = s' ≫ hf.functor.map t) ↔
    ∀ (j₂ : J₂), ∃ j₁, j₂ ≤ f j₁

Tactic:
constructor

Result:
case mp
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsDirected J₁ fun x1 x2 => x1 ≤ x2
f : J₁ → J₂
hf : Monotone f
⊢ ((∀ (d : J₂), ∃ c, Nonempty (d ⟶ hf.functor.obj c)) ∧
      ∀ {d : J₂} {c : J₁} (s s' : d ⟶ hf.functor.obj c), ∃ c' t, s ≫ hf.functor.map t = s' ≫ hf.functor.map t) →
    ∀ (j₂ : J₂), ∃ j₁, j₂ ≤ f j₁

case mpr
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsDirected J₁ fun x1 x2 => x1 ≤ x2
f : J₁ → J₂
hf : Monotone f
⊢ (∀ (j₂ : J₂), ∃ j₁, j₂ ≤ f j₁) →
    (∀ (d : J₂), ∃ c, Nonempty (d ⟶ hf.functor.obj c)) ∧
      ∀ {d : J₂} {c : J₁} (s s' : d ⟶ hf.functor.obj c), ∃ c' t, s ≫ hf.functor.map t = s' ≫ hf.functor.map t

Proof state:
case mp
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsDirected J₁ fun x1 x2 => x1 ≤ x2
f : J₁ → J₂
hf : Monotone f
⊢ ((∀ (d : J₂), ∃ c, Nonempty (d ⟶ hf.functor.obj c)) ∧
      ∀ {d : J₂} {c : J₁} (s s' : d ⟶ hf.functor.obj c), ∃ c' t, s ≫ hf.functor.map t = s' ≫ hf.functor.map t) →
    ∀ (j₂ : J₂), ∃ j₁, j₂ ≤ f j₁

Tactic:
rintro ⟨h, _⟩ j₂

Result:
case mp.intro
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsDirected J₁ fun x1 x2 => x1 ≤ x2
f : J₁ → J₂
hf : Monotone f
h : ∀ (d : J₂), ∃ c, Nonempty (d ⟶ hf.functor.obj c)
right✝ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ hf.functor.obj c), ∃ c' t, s ≫ hf.functor.map t = s' ≫ hf.functor.map t
j₂ : J₂
⊢ ∃ j₁, j₂ ≤ f j₁

Proof state:
case mp.intro.intro.intro
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsDirected J₁ fun x1 x2 => x1 ≤ x2
f : J₁ → J₂
hf : Monotone f
h : ∀ (d : J₂), ∃ c, Nonempty (d ⟶ hf.functor.obj c)
right✝ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ hf.functor.obj c), ∃ c' t, s ≫ hf.functor.map t = s' ≫ hf.functor.map t
j₂ : J₂
j₁ : J₁
φ : j₂ ⟶ hf.functor.obj j₁
⊢ ∃ j₁, j₂ ≤ f j₁

Tactic:
exact ⟨j₁, leOfHom φ⟩

Result:
no goals

Proof state:
case mpr
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsDirected J₁ fun x1 x2 => x1 ≤ x2
f : J₁ → J₂
hf : Monotone f
⊢ (∀ (j₂ : J₂), ∃ j₁, j₂ ≤ f j₁) →
    (∀ (d : J₂), ∃ c, Nonempty (d ⟶ hf.functor.obj c)) ∧
      ∀ {d : J₂} {c : J₁} (s s' : d ⟶ hf.functor.obj c), ∃ c' t, s ≫ hf.functor.map t = s' ≫ hf.functor.map t

Tactic:
intro h

Result:
case mpr
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsDirected J₁ fun x1 x2 => x1 ≤ x2
f : J₁ → J₂
hf : Monotone f
h : ∀ (j₂ : J₂), ∃ j₁, j₂ ≤ f j₁
⊢ (∀ (d : J₂), ∃ c, Nonempty (d ⟶ hf.functor.obj c)) ∧
    ∀ {d : J₂} {c : J₁} (s s' : d ⟶ hf.functor.obj c), ∃ c' t, s ≫ hf.functor.map t = s' ≫ hf.functor.map t

Proof state:
case mp.intro
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsDirected J₁ fun x1 x2 => x1 ≤ x2
f : J₁ → J₂
hf : Monotone f
h : ∀ (d : J₂), ∃ c, Nonempty (d ⟶ hf.functor.obj c)
right✝ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ hf.functor.obj c), ∃ c' t, s ≫ hf.functor.map t = s' ≫ hf.functor.map t
j₂ : J₂
⊢ ∃ j₁, j₂ ≤ f j₁

Tactic:
obtain ⟨j₁, ⟨φ⟩⟩ := h j₂

Result:
case mp.intro.intro.intro
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsDirected J₁ fun x1 x2 => x1 ≤ x2
f : J₁ → J₂
hf : Monotone f
h : ∀ (d : J₂), ∃ c, Nonempty (d ⟶ hf.functor.obj c)
right✝ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ hf.functor.obj c), ∃ c' t, s ≫ hf.functor.map t = s' ≫ hf.functor.map t
j₂ : J₂
j₁ : J₁
φ : j₂ ⟶ hf.functor.obj j₁
⊢ ∃ j₁, j₂ ≤ f j₁