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

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

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

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

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