[GOAL]
X✝ Y✝ : Grpd
x✝ : X✝ ⟶ Y✝
⊢ 𝟙 X✝ ≫ x✝ = x✝
[PROOFSTEP]
rfl
[GOAL]
X✝ Y✝ : Grpd
x✝ : X✝ ⟶ Y✝
⊢ x✝ ≫ 𝟙 Y✝ = x✝
[PROOFSTEP]
rfl
[GOAL]
⊢ ∀ {W X Y Z : Grpd} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
intros
[GOAL]
W✝ X✝ Y✝ Z✝ : Grpd
f✝ : W✝ ⟶ X✝
g✝ : X✝ ⟶ Y✝
h✝ : Y✝ ⟶ Z✝
⊢ (f✝ ≫ g✝) ≫ h✝ = f✝ ≫ g✝ ≫ h✝
[PROOFSTEP]
rfl
[GOAL]
J : Type u
F : J → Grpd
⊢ ∀ (s : Limits.Fan F) (j : J),
    (fun s => Functor.pi' fun j => Limits.Fan.proj s j) s ≫ Limits.Fan.proj (piLimitFan F) j = Limits.Fan.proj s j
[PROOFSTEP]
intros
[GOAL]
J : Type u
F : J → Grpd
s✝ : Limits.Fan F
j✝ : J
⊢ (fun s => Functor.pi' fun j => Limits.Fan.proj s j) s✝ ≫ Limits.Fan.proj (piLimitFan F) j✝ = Limits.Fan.proj s✝ j✝
[PROOFSTEP]
dsimp only [piLimitFan]
[GOAL]
J : Type u
F : J → Grpd
s✝ : Limits.Fan F
j✝ : J
⊢ (Functor.pi' fun j => Limits.Fan.proj s✝ j) ≫
      Limits.Fan.proj (Limits.Fan.mk (of ((j : J) → ↑(F j))) fun j => Pi.eval (fun j => ↑(F j)) j) j✝ =
    Limits.Fan.proj s✝ j✝
[PROOFSTEP]
simp [hom_to_functor]
[GOAL]
J : Type u
F : J → Grpd
⊢ ∀ (s : Limits.Fan F) (m : s.pt ⟶ (piLimitFan F).pt),
    (∀ (j : J), m ≫ Limits.Fan.proj (piLimitFan F) j = Limits.Fan.proj s j) →
      m = (fun s => Functor.pi' fun j => Limits.Fan.proj s j) s
[PROOFSTEP]
intro s m w
[GOAL]
J : Type u
F : J → Grpd
s : Limits.Fan F
m : s.pt ⟶ (piLimitFan F).pt
w : ∀ (j : J), m ≫ Limits.Fan.proj (piLimitFan F) j = Limits.Fan.proj s j
⊢ m = (fun s => Functor.pi' fun j => Limits.Fan.proj s j) s
[PROOFSTEP]
apply Functor.pi_ext
[GOAL]
case h
J : Type u
F : J → Grpd
s : Limits.Fan F
m : s.pt ⟶ (piLimitFan F).pt
w : ∀ (j : J), m ≫ Limits.Fan.proj (piLimitFan F) j = Limits.Fan.proj s j
⊢ ∀ (i : J),
    m ⋙ Pi.eval (fun i => ↑(F i)) i =
      (fun s => Functor.pi' fun j => Limits.Fan.proj s j) s ⋙ Pi.eval (fun i => ↑(F i)) i
[PROOFSTEP]
intro j
[GOAL]
case h
J : Type u
F : J → Grpd
s : Limits.Fan F
m : s.pt ⟶ (piLimitFan F).pt
w : ∀ (j : J), m ≫ Limits.Fan.proj (piLimitFan F) j = Limits.Fan.proj s j
j : J
⊢ m ⋙ Pi.eval (fun i => ↑(F i)) j = (fun s => Functor.pi' fun j => Limits.Fan.proj s j) s ⋙ Pi.eval (fun i => ↑(F i)) j
[PROOFSTEP]
specialize w j
[GOAL]
case h
J : Type u
F : J → Grpd
s : Limits.Fan F
m : s.pt ⟶ (piLimitFan F).pt
j : J
w : m ≫ Limits.Fan.proj (piLimitFan F) j = Limits.Fan.proj s j
⊢ m ⋙ Pi.eval (fun i => ↑(F i)) j = (fun s => Functor.pi' fun j => Limits.Fan.proj s j) s ⋙ Pi.eval (fun i => ↑(F i)) j
[PROOFSTEP]
simpa
[GOAL]
⊢ {J : Type ?u.17117} → (f : J → Grpd) → Limits.Fan f
[PROOFSTEP]
apply piLimitFan
[GOAL]
⊢ {J : Type u} → (f : J → Grpd) → Limits.IsLimit (piLimitFan f)
[PROOFSTEP]
apply piLimitFanIsLimit
[GOAL]
J : Type u
f : J → Grpd
j : J
⊢ (piIsoPi J f).hom ≫ Limits.Pi.π f j = Pi.eval (fun i => ↑(f i)) j
[PROOFSTEP]
simp [piIsoPi]
[GOAL]
J : Type u
f : J → Grpd
j : J
⊢ NatTrans.app (piLimitFan f).π { as := j } = Pi.eval (fun i => ↑(f i)) j
[PROOFSTEP]
rfl
