case h₁
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
F : C ⥤ D
inst✝¹ : Final F
E : Type u₃
inst✝ : Category E
G : D ⥤ E
s : Cocone (F ⋙ G)
j : C
⊢ ∀ (X₁ X₂ : C) (k₁ : F.obj j ⟶ F.obj X₁) (k₂ : F.obj j ⟶ F.obj X₂) (f : X₁ ⟶ X₂),
    k₁ ≫ F.map f = k₂ → G.map k₁ ≫ s.ι.app X₁ = s.ι.app j → G.map k₂ ≫ s.ι.app X₂ = s.ι.app j

case h₂
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
F : C ⥤ D
inst✝¹ : Final F
E : Type u₃
inst✝ : Category E
G : D ⥤ E
s : Cocone (F ⋙ G)
j : C
⊢ ∀ (X₁ X₂ : C) (k₁ : F.obj j ⟶ F.obj X₁) (k₂ : F.obj j ⟶ F.obj X₂) (f : X₁ ⟶ X₂),
    k₁ ≫ F.map f = k₂ → G.map k₂ ≫ s.ι.app X₂ = s.ι.app j → G.map k₁ ≫ s.ι.app X₁ = s.ι.app j

case z
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
F : C ⥤ D
inst✝¹ : Final F
E : Type u₃
inst✝ : Category E
G : D ⥤ E
s : Cocone (F ⋙ G)
j : C
⊢ G.map ?k₀ ≫ s.ι.app ?X₀ = s.ι.app j

case X₀
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
F : C ⥤ D
inst✝¹ : Final F
E : Type u₃
inst✝ : Category E
G : D ⥤ E
s : Cocone (F ⋙ G)
j : C
⊢ C

case k₀
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
F : C ⥤ D
inst✝¹ : Final F
E : Type u₃
inst✝ : Category E
G : D ⥤ E
s : Cocone (F ⋙ G)
j : C
⊢ F.obj j ⟶ F.obj ?X₀
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
F : C ⥤ D
inst✝¹ : Final F
E : Type u₃
inst✝ : Category E
G : D ⥤ E
s : Cocone (F ⋙ G)
j : C
⊢ G.map (homToLift F (F.obj j)) ≫ s.ι.app (lift F (F.obj j)) = s.ι.app j
apply induction F fun X k => G.map k ≫ s.ι.app X = (s.ι.app j : _)
case h₁
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
F : C ⥤ D
inst✝¹ : Final F
E : Type u₃
inst✝ : Category E
G : D ⥤ E
s : Cocone (F ⋙ G)
j j₁ j₂ : C
k₁ : F.obj j ⟶ F.obj j₁
k₂ : F.obj j ⟶ F.obj j₂
f : j₁ ⟶ j₂
w : k₁ ≫ F.map f = k₂
h : G.map k₁ ≫ s.ι.app j₁ = s.ι.app j
⊢ G.map k₂ ≫ s.ι.app j₂ = s.ι.app j
case h₁
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
F : C ⥤ D
inst✝¹ : Final F
E : Type u₃
inst✝ : Category E
G : D ⥤ E
s : Cocone (F ⋙ G)
j : C
⊢ ∀ (X₁ X₂ : C) (k₁ : F.obj j ⟶ F.obj X₁) (k₂ : F.obj j ⟶ F.obj X₂) (f : X₁ ⟶ X₂),
    k₁ ≫ F.map f = k₂ → G.map k₁ ≫ s.ι.app X₁ = s.ι.app j → G.map k₂ ≫ s.ι.app X₂ = s.ι.app j
intro j₁ j₂ k₁ k₂ f w h
case h₁
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
F : C ⥤ D
inst✝¹ : Final F
E : Type u₃
inst✝ : Category E
G : D ⥤ E
s : Cocone (F ⋙ G)
j j₁ j₂ : C
k₁ : F.obj j ⟶ F.obj j₁
k₂ : F.obj j ⟶ F.obj j₂
f : j₁ ⟶ j₂
w : k₁ ≫ F.map f = k₂
h : G.map k₁ ≫ s.ι.app j₁ = s.ι.app j
⊢ G.map (k₁ ≫ F.map f) ≫ s.ι.app j₂ = s.ι.app j
case h₁
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
F : C ⥤ D
inst✝¹ : Final F
E : Type u₃
inst✝ : Category E
G : D ⥤ E
s : Cocone (F ⋙ G)
j j₁ j₂ : C
k₁ : F.obj j ⟶ F.obj j₁
k₂ : F.obj j ⟶ F.obj j₂
f : j₁ ⟶ j₂
w : k₁ ≫ F.map f = k₂
h : G.map k₁ ≫ s.ι.app j₁ = s.ι.app j
⊢ G.map k₂ ≫ s.ι.app j₂ = s.ι.app j
rw [← w]
case h₁
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
F : C ⥤ D
inst✝¹ : Final F
E : Type u₃
inst✝ : Category E
G : D ⥤ E
s : Cocone (F ⋙ G)
j j₁ j₂ : C
k₁ : F.obj j ⟶ F.obj j₁
k₂ : F.obj j ⟶ F.obj j₂
f : j₁ ⟶ j₂
w : k₁ ≫ F.map f = k₂
h : G.map k₁ ≫ (F ⋙ G).map f ≫ s.ι.app j₂ = s.ι.app j
⊢ G.map (k₁ ≫ F.map f) ≫ s.ι.app j₂ = s.ι.app j
case h₁
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
F : C ⥤ D
inst✝¹ : Final F
E : Type u₃
inst✝ : Category E
G : D ⥤ E
s : Cocone (F ⋙ G)
j j₁ j₂ : C
k₁ : F.obj j ⟶ F.obj j₁
k₂ : F.obj j ⟶ F.obj j₂
f : j₁ ⟶ j₂
w : k₁ ≫ F.map f = k₂
h : G.map k₁ ≫ s.ι.app j₁ = s.ι.app j
⊢ G.map (k₁ ≫ F.map f) ≫ s.ι.app j₂ = s.ι.app j
rw [← s.w f] at h
no goals
case h₁
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
F : C ⥤ D
inst✝¹ : Final F
E : Type u₃
inst✝ : Category E
G : D ⥤ E
s : Cocone (F ⋙ G)
j j₁ j₂ : C
k₁ : F.obj j ⟶ F.obj j₁
k₂ : F.obj j ⟶ F.obj j₂
f : j₁ ⟶ j₂
w : k₁ ≫ F.map f = k₂
h : G.map k₁ ≫ (F ⋙ G).map f ≫ s.ι.app j₂ = s.ι.app j
⊢ G.map (k₁ ≫ F.map f) ≫ s.ι.app j₂ = s.ι.app j
simpa using h
case h₂
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
F : C ⥤ D
inst✝¹ : Final F
E : Type u₃
inst✝ : Category E
G : D ⥤ E
s : Cocone (F ⋙ G)
j j₁ j₂ : C
k₁ : F.obj j ⟶ F.obj j₁
k₂ : F.obj j ⟶ F.obj j₂
f : j₁ ⟶ j₂
w : k₁ ≫ F.map f = k₂
h : G.map k₂ ≫ s.ι.app j₂ = s.ι.app j
⊢ G.map k₁ ≫ s.ι.app j₁ = s.ι.app j
case h₂
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
F : C ⥤ D
inst✝¹ : Final F
E : Type u₃
inst✝ : Category E
G : D ⥤ E
s : Cocone (F ⋙ G)
j : C
⊢ ∀ (X₁ X₂ : C) (k₁ : F.obj j ⟶ F.obj X₁) (k₂ : F.obj j ⟶ F.obj X₂) (f : X₁ ⟶ X₂),
    k₁ ≫ F.map f = k₂ → G.map k₂ ≫ s.ι.app X₂ = s.ι.app j → G.map k₁ ≫ s.ι.app X₁ = s.ι.app j
intro j₁ j₂ k₁ k₂ f w h
case h₂
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
F : C ⥤ D
inst✝¹ : Final F
E : Type u₃
inst✝ : Category E
G : D ⥤ E
s : Cocone (F ⋙ G)
j j₁ j₂ : C
k₁ : F.obj j ⟶ F.obj j₁
k₂ : F.obj j ⟶ F.obj j₂
f : j₁ ⟶ j₂
w : k₁ ≫ F.map f = k₂
h : G.map (k₁ ≫ F.map f) ≫ s.ι.app j₂ = s.ι.app j
⊢ G.map k₁ ≫ s.ι.app j₁ = s.ι.app j
case h₂
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
F : C ⥤ D
inst✝¹ : Final F
E : Type u₃
inst✝ : Category E
G : D ⥤ E
s : Cocone (F ⋙ G)
j j₁ j₂ : C
k₁ : F.obj j ⟶ F.obj j₁
k₂ : F.obj j ⟶ F.obj j₂
f : j₁ ⟶ j₂
w : k₁ ≫ F.map f = k₂
h : G.map k₂ ≫ s.ι.app j₂ = s.ι.app j
⊢ G.map k₁ ≫ s.ι.app j₁ = s.ι.app j
rw [← w] at h
case h₂
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
F : C ⥤ D
inst✝¹ : Final F
E : Type u₃
inst✝ : Category E
G : D ⥤ E
s : Cocone (F ⋙ G)
j j₁ j₂ : C
k₁ : F.obj j ⟶ F.obj j₁
k₂ : F.obj j ⟶ F.obj j₂
f : j₁ ⟶ j₂
w : k₁ ≫ F.map f = k₂
h : G.map (k₁ ≫ F.map f) ≫ s.ι.app j₂ = s.ι.app j
⊢ G.map k₁ ≫ (F ⋙ G).map f ≫ s.ι.app j₂ = s.ι.app j
case h₂
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
F : C ⥤ D
inst✝¹ : Final F
E : Type u₃
inst✝ : Category E
G : D ⥤ E
s : Cocone (F ⋙ G)
j j₁ j₂ : C
k₁ : F.obj j ⟶ F.obj j₁
k₂ : F.obj j ⟶ F.obj j₂
f : j₁ ⟶ j₂
w : k₁ ≫ F.map f = k₂
h : G.map (k₁ ≫ F.map f) ≫ s.ι.app j₂ = s.ι.app j
⊢ G.map k₁ ≫ s.ι.app j₁ = s.ι.app j
rw [← s.w f]
no goals
case h₂
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
F : C ⥤ D
inst✝¹ : Final F
E : Type u₃
inst✝ : Category E
G : D ⥤ E
s : Cocone (F ⋙ G)
j j₁ j₂ : C
k₁ : F.obj j ⟶ F.obj j₁
k₂ : F.obj j ⟶ F.obj j₂
f : j₁ ⟶ j₂
w : k₁ ≫ F.map f = k₂
h : G.map (k₁ ≫ F.map f) ≫ s.ι.app j₂ = s.ι.app j
⊢ G.map k₁ ≫ (F ⋙ G).map f ≫ s.ι.app j₂ = s.ι.app j
simpa using h
no goals
case z
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
F : C ⥤ D
inst✝¹ : Final F
E : Type u₃
inst✝ : Category E
G : D ⥤ E
s : Cocone (F ⋙ G)
j : C
⊢ G.map ?k₀ ≫ s.ι.app ?X₀ = s.ι.app j
exact s.w (𝟙 _)