-- Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean
/-- The general adjoint functor theorem says that if `G : D ⥤ C` preserves limits and `D` has them,
if `G` satisfies the solution set condition then `G` is a right adjoint.
-/
lemma isRightAdjoint_of_preservesLimits_of_solutionSetCondition [HasLimits D]
    [PreservesLimits G] (hG : SolutionSetCondition G) : G.IsRightAdjoint

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
A : C
ι : Type v
B : ι → D
f : (i : ι) → A ⟶ G.obj (B i)
g : ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h
B' : ι → StructuredArrow A G := fun i => StructuredArrow.mk (f i)
⊢ ∀ (A' : StructuredArrow A G), ∃ i, Nonempty (B' i ⟶ A')

Tactic:
intro A'

Result:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
A : C
ι : Type v
B : ι → D
f : (i : ι) → A ⟶ G.obj (B i)
g : ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h
B' : ι → StructuredArrow A G := fun i => StructuredArrow.mk (f i)
A' : StructuredArrow A G
⊢ ∃ i, Nonempty (B' i ⟶ A')

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
hG : SolutionSetCondition G
⊢ G.IsRightAdjoint

Tactic:
refine @isRightAdjointOfStructuredArrowInitials _ _ _ _ G ?_

Result:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
hG : SolutionSetCondition G
⊢ ∀ (A : C), HasInitial (StructuredArrow A G)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
A : C
ι : Type v
B : ι → D
f : (i : ι) → A ⟶ G.obj (B i)
g : ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h
⊢ HasInitial (StructuredArrow A G)

Tactic:
let B' : ι → StructuredArrow A G := fun i => StructuredArrow.mk (f i)

Result:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
A : C
ι : Type v
B : ι → D
f : (i : ι) → A ⟶ G.obj (B i)
g : ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h
B' : ι → StructuredArrow A G := fun i => StructuredArrow.mk (f i)
⊢ HasInitial (StructuredArrow A G)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
A : C
ι : Type v
B : ι → D
f : (i : ι) → A ⟶ G.obj (B i)
g : ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h
B' : ι → StructuredArrow A G := fun i => StructuredArrow.mk (f i)
hB' : ∀ (A' : StructuredArrow A G), ∃ i, Nonempty (B' i ⟶ A')
⊢ HasInitial (StructuredArrow A G)

Tactic:
obtain ⟨T, hT⟩ := has_weakly_initial_of_weakly_initial_set_and_hasProducts hB'

Result:
case intro
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
A : C
ι : Type v
B : ι → D
f : (i : ι) → A ⟶ G.obj (B i)
g : ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h
B' : ι → StructuredArrow A G := fun i => StructuredArrow.mk (f i)
hB' : ∀ (A' : StructuredArrow A G), ∃ i, Nonempty (B' i ⟶ A')
T : StructuredArrow A G
hT : ∀ (X : StructuredArrow A G), Nonempty (T ⟶ X)
⊢ HasInitial (StructuredArrow A G)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
hG : SolutionSetCondition G
⊢ ∀ (A : C), HasInitial (StructuredArrow A G)

Tactic:
intro A

Result:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
hG : SolutionSetCondition G
A : C
⊢ HasInitial (StructuredArrow A G)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
hG : SolutionSetCondition G
A : C
⊢ HasInitial (StructuredArrow A G)

Tactic:
specialize hG A

Result:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
A : C
hG : ∃ ι B f, ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h
⊢ HasInitial (StructuredArrow A G)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
A : C
hG : ∃ ι B f, ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h
⊢ HasInitial (StructuredArrow A G)

Tactic:
choose ι B f g using hG

Result:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
A : C
ι : Type v
B : ι → D
f : (i : ι) → A ⟶ G.obj (B i)
g : ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h
⊢ HasInitial (StructuredArrow A G)

Proof state:
case intro.intro
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
A : C
ι : Type v
B : ι → D
f : (i : ι) → A ⟶ G.obj (B i)
g : ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h
B' : ι → StructuredArrow A G := fun i => StructuredArrow.mk (f i)
A' : StructuredArrow A G
i : ι
w✝ : B i ⟶ A'.right
t : f i ≫ G.map w✝ = A'.hom
⊢ ∃ i, Nonempty (B' i ⟶ A')

Tactic:
exact ⟨i, ⟨StructuredArrow.homMk _ t⟩⟩

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
A : C
ι : Type v
B : ι → D
f : (i : ι) → A ⟶ G.obj (B i)
g : ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h
B' : ι → StructuredArrow A G := fun i => StructuredArrow.mk (f i)
A' : StructuredArrow A G
⊢ ∃ i, Nonempty (B' i ⟶ A')

Tactic:
obtain ⟨i, _, t⟩ := g _ A'.hom

Result:
case intro.intro
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
A : C
ι : Type v
B : ι → D
f : (i : ι) → A ⟶ G.obj (B i)
g : ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h
B' : ι → StructuredArrow A G := fun i => StructuredArrow.mk (f i)
A' : StructuredArrow A G
i : ι
w✝ : B i ⟶ A'.right
t : f i ≫ G.map w✝ = A'.hom
⊢ ∃ i, Nonempty (B' i ⟶ A')

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
A : C
ι : Type v
B : ι → D
f : (i : ι) → A ⟶ G.obj (B i)
g : ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h
B' : ι → StructuredArrow A G := fun i => StructuredArrow.mk (f i)
⊢ HasInitial (StructuredArrow A G)

Tactic:
have hB' : ∀ A' : StructuredArrow A G, ∃ i, Nonempty (B' i ⟶ A') := by
  intro A'
  obtain ⟨i, _, t⟩ := g _ A'.hom
  exact ⟨i, ⟨StructuredArrow.homMk _ t⟩⟩

Result:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
A : C
ι : Type v
B : ι → D
f : (i : ι) → A ⟶ G.obj (B i)
g : ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h
B' : ι → StructuredArrow A G := fun i => StructuredArrow.mk (f i)
hB' : ∀ (A' : StructuredArrow A G), ∃ i, Nonempty (B' i ⟶ A')
⊢ HasInitial (StructuredArrow A G)

Proof state:
case intro
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
A : C
ι : Type v
B : ι → D
f : (i : ι) → A ⟶ G.obj (B i)
g : ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h
B' : ι → StructuredArrow A G := fun i => StructuredArrow.mk (f i)
hB' : ∀ (A' : StructuredArrow A G), ∃ i, Nonempty (B' i ⟶ A')
T : StructuredArrow A G
hT : ∀ (X : StructuredArrow A G), Nonempty (T ⟶ X)
⊢ HasInitial (StructuredArrow A G)

Tactic:
apply hasInitial_of_weakly_initial_and_hasWideEqualizers hT

Result:
no goals