[GOAL]
V : Type v
inst✝⁴ : Category.{w, v} V
inst✝³ : MonoidalCategory V
C : Type u₁
inst✝² : EnrichedCategory V C
W : Type v
inst✝¹ : Category.{w, v} W
inst✝ : MonoidalCategory W
F : LaxMonoidalFunctor V W
X Y : TransportEnrichment F C
⊢ (λ_ ((fun X Y => F.obj (EnrichedCategory.Hom X Y)) X Y)).inv ≫
      ((fun X => F.ε ≫ F.map (eId V X)) X ⊗ 𝟙 ((fun X Y => F.obj (EnrichedCategory.Hom X Y)) X Y)) ≫
        (fun X Y Z =>
            LaxMonoidalFunctor.μ F (EnrichedCategory.Hom X Y) (EnrichedCategory.Hom Y Z) ≫ F.map (eComp V X Y Z))
          X X Y =
    𝟙 ((fun X Y => F.obj (EnrichedCategory.Hom X Y)) X Y)
[PROOFSTEP]
rw [comp_tensor_id, Category.assoc, ← F.toFunctor.map_id, F.μ_natural_assoc, F.toFunctor.map_id,
  F.left_unitality_inv_assoc, ← F.toFunctor.map_comp, ← F.toFunctor.map_comp, e_id_comp, F.toFunctor.map_id]
[GOAL]
V : Type v
inst✝⁴ : Category.{w, v} V
inst✝³ : MonoidalCategory V
C : Type u₁
inst✝² : EnrichedCategory V C
W : Type v
inst✝¹ : Category.{w, v} W
inst✝ : MonoidalCategory W
F : LaxMonoidalFunctor V W
X Y : TransportEnrichment F C
⊢ (ρ_ ((fun X Y => F.obj (EnrichedCategory.Hom X Y)) X Y)).inv ≫
      (𝟙 ((fun X Y => F.obj (EnrichedCategory.Hom X Y)) X Y) ⊗ (fun X => F.ε ≫ F.map (eId V X)) Y) ≫
        (fun X Y Z =>
            LaxMonoidalFunctor.μ F (EnrichedCategory.Hom X Y) (EnrichedCategory.Hom Y Z) ≫ F.map (eComp V X Y Z))
          X Y Y =
    𝟙 ((fun X Y => F.obj (EnrichedCategory.Hom X Y)) X Y)
[PROOFSTEP]
rw [id_tensor_comp, Category.assoc, ← F.toFunctor.map_id, F.μ_natural_assoc, F.toFunctor.map_id,
  F.right_unitality_inv_assoc, ← F.toFunctor.map_comp, ← F.toFunctor.map_comp, e_comp_id, F.toFunctor.map_id]
[GOAL]
V : Type v
inst✝⁴ : Category.{w, v} V
inst✝³ : MonoidalCategory V
C : Type u₁
inst✝² : EnrichedCategory V C
W : Type v
inst✝¹ : Category.{w, v} W
inst✝ : MonoidalCategory W
F : LaxMonoidalFunctor V W
P Q R S : TransportEnrichment F C
⊢ (α_ ((fun X Y => F.obj (EnrichedCategory.Hom X Y)) P Q) ((fun X Y => F.obj (EnrichedCategory.Hom X Y)) Q R)
          ((fun X Y => F.obj (EnrichedCategory.Hom X Y)) R S)).inv ≫
      ((fun X Y Z =>
              LaxMonoidalFunctor.μ F (EnrichedCategory.Hom X Y) (EnrichedCategory.Hom Y Z) ≫ F.map (eComp V X Y Z))
            P Q R ⊗
          𝟙 ((fun X Y => F.obj (EnrichedCategory.Hom X Y)) R S)) ≫
        (fun X Y Z =>
            LaxMonoidalFunctor.μ F (EnrichedCategory.Hom X Y) (EnrichedCategory.Hom Y Z) ≫ F.map (eComp V X Y Z))
          P R S =
    (𝟙 ((fun X Y => F.obj (EnrichedCategory.Hom X Y)) P Q) ⊗
        (fun X Y Z =>
            LaxMonoidalFunctor.μ F (EnrichedCategory.Hom X Y) (EnrichedCategory.Hom Y Z) ≫ F.map (eComp V X Y Z))
          Q R S) ≫
      (fun X Y Z =>
          LaxMonoidalFunctor.μ F (EnrichedCategory.Hom X Y) (EnrichedCategory.Hom Y Z) ≫ F.map (eComp V X Y Z))
        P Q S
[PROOFSTEP]
rw [comp_tensor_id, Category.assoc, ← F.toFunctor.map_id, F.μ_natural_assoc, F.toFunctor.map_id, ←
  F.associativity_inv_assoc, ← F.toFunctor.map_comp, ← F.toFunctor.map_comp, e_assoc, id_tensor_comp, Category.assoc, ←
  F.toFunctor.map_id, F.μ_natural_assoc, F.toFunctor.map_comp]
[GOAL]
V : Type v
inst✝² : Category.{w, v} V
inst✝¹ : MonoidalCategory V
C✝ : Type u₁
inst✝ : EnrichedCategory V C✝
C : Type u₁
𝒞 : Category.{v, u₁} C
X Y : C
⊢ (λ_ (X ⟶ Y)).inv ≫ ((fun X x => 𝟙 X) X ⊗ 𝟙 (X ⟶ Y)) ≫ (fun X Y Z p => p.fst ≫ p.snd) X X Y = 𝟙 (X ⟶ Y)
[PROOFSTEP]
ext
[GOAL]
case h
V : Type v
inst✝² : Category.{w, v} V
inst✝¹ : MonoidalCategory V
C✝ : Type u₁
inst✝ : EnrichedCategory V C✝
C : Type u₁
𝒞 : Category.{v, u₁} C
X Y : C
a✝ : X ⟶ Y
⊢ ((λ_ (X ⟶ Y)).inv ≫ ((fun X x => 𝟙 X) X ⊗ 𝟙 (X ⟶ Y)) ≫ (fun X Y Z p => p.fst ≫ p.snd) X X Y) a✝ = 𝟙 (X ⟶ Y) a✝
[PROOFSTEP]
simp
[GOAL]
V : Type v
inst✝² : Category.{w, v} V
inst✝¹ : MonoidalCategory V
C✝ : Type u₁
inst✝ : EnrichedCategory V C✝
C : Type u₁
𝒞 : Category.{v, u₁} C
X Y : C
⊢ (ρ_ (X ⟶ Y)).inv ≫ (𝟙 (X ⟶ Y) ⊗ (fun X x => 𝟙 X) Y) ≫ (fun X Y Z p => p.fst ≫ p.snd) X Y Y = 𝟙 (X ⟶ Y)
[PROOFSTEP]
ext
[GOAL]
case h
V : Type v
inst✝² : Category.{w, v} V
inst✝¹ : MonoidalCategory V
C✝ : Type u₁
inst✝ : EnrichedCategory V C✝
C : Type u₁
𝒞 : Category.{v, u₁} C
X Y : C
a✝ : X ⟶ Y
⊢ ((ρ_ (X ⟶ Y)).inv ≫ (𝟙 (X ⟶ Y) ⊗ (fun X x => 𝟙 X) Y) ≫ (fun X Y Z p => p.fst ≫ p.snd) X Y Y) a✝ = 𝟙 (X ⟶ Y) a✝
[PROOFSTEP]
simp
[GOAL]
V : Type v
inst✝² : Category.{w, v} V
inst✝¹ : MonoidalCategory V
C✝ : Type u₁
inst✝ : EnrichedCategory V C✝
C : Type u₁
𝒞 : Category.{v, u₁} C
W X Y Z : C
⊢ (α_ (W ⟶ X) (X ⟶ Y) (Y ⟶ Z)).inv ≫
      ((fun X Y Z p => p.fst ≫ p.snd) W X Y ⊗ 𝟙 (Y ⟶ Z)) ≫ (fun X Y Z p => p.fst ≫ p.snd) W Y Z =
    (𝟙 (W ⟶ X) ⊗ (fun X Y Z p => p.fst ≫ p.snd) X Y Z) ≫ (fun X Y Z p => p.fst ≫ p.snd) W X Z
[PROOFSTEP]
ext ⟨f, g, h⟩
[GOAL]
case h.mk.mk
V : Type v
inst✝² : Category.{w, v} V
inst✝¹ : MonoidalCategory V
C✝ : Type u₁
inst✝ : EnrichedCategory V C✝
C : Type u₁
𝒞 : Category.{v, u₁} C
W X Y Z : C
f : W ⟶ X
g : X ⟶ Y
h : Y ⟶ Z
⊢ ((α_ (W ⟶ X) (X ⟶ Y) (Y ⟶ Z)).inv ≫
        ((fun X Y Z p => p.fst ≫ p.snd) W X Y ⊗ 𝟙 (Y ⟶ Z)) ≫ (fun X Y Z p => p.fst ≫ p.snd) W Y Z)
      (f, g, h) =
    ((𝟙 (W ⟶ X) ⊗ (fun X Y Z p => p.fst ≫ p.snd) X Y Z) ≫ (fun X Y Z p => p.fst ≫ p.snd) W X Z) (f, g, h)
[PROOFSTEP]
simp
[GOAL]
V : Type v
inst✝⁵ : Category.{w, v} V
inst✝⁴ : MonoidalCategory V
C : Type u₁
inst✝³ : EnrichedCategory V C
W : Type (v + 1)
inst✝² : Category.{v, v + 1} W
inst✝¹ : MonoidalCategory W
inst✝ : EnrichedCategory W C
⊢ Category.{?u.96214, u₁} (ForgetEnrichment W C)
[PROOFSTEP]
let I : EnrichedCategory (Type v) (TransportEnrichment (coyonedaTensorUnit W) C) := inferInstance
[GOAL]
V : Type v
inst✝⁵ : Category.{w, v} V
inst✝⁴ : MonoidalCategory V
C : Type u₁
inst✝³ : EnrichedCategory V C
W : Type (v + 1)
inst✝² : Category.{v, v + 1} W
inst✝¹ : MonoidalCategory W
inst✝ : EnrichedCategory W C
I : EnrichedCategory (Type v) (TransportEnrichment (coyonedaTensorUnit W) C) := inferInstance
⊢ Category.{?u.96214, u₁} (ForgetEnrichment W C)
[PROOFSTEP]
exact enrichedCategoryTypeEquivCategory C I
[GOAL]
V : Type v
inst✝⁶ : Category.{w, v} V
inst✝⁵ : MonoidalCategory V
C✝ : Type u₁
inst✝⁴ : EnrichedCategory V C✝
W : Type (v + 1)
inst✝³ : Category.{v, v + 1} W
inst✝² : MonoidalCategory W
C : Type u₁
D : Type u₂
inst✝¹ : EnrichedCategory W C
inst✝ : EnrichedCategory W D
F : EnrichedFunctor W C D
X✝ Y✝ Z✝ : ForgetEnrichment W C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { obj := fun X => ForgetEnrichment.of W (obj F (ForgetEnrichment.to W X)),
          map := fun {X Y} f =>
            ForgetEnrichment.homOf W
              (ForgetEnrichment.homTo W f ≫ map F (ForgetEnrichment.to W X) (ForgetEnrichment.to W Y)) }.map
      (f ≫ g) =
    { obj := fun X => ForgetEnrichment.of W (obj F (ForgetEnrichment.to W X)),
            map := fun {X Y} f =>
              ForgetEnrichment.homOf W
                (ForgetEnrichment.homTo W f ≫ map F (ForgetEnrichment.to W X) (ForgetEnrichment.to W Y)) }.map
        f ≫
      { obj := fun X => ForgetEnrichment.of W (obj F (ForgetEnrichment.to W X)),
            map := fun {X Y} f =>
              ForgetEnrichment.homOf W
                (ForgetEnrichment.homTo W f ≫ map F (ForgetEnrichment.to W X) (ForgetEnrichment.to W Y)) }.map
        g
[PROOFSTEP]
dsimp
[GOAL]
V : Type v
inst✝⁶ : Category.{w, v} V
inst✝⁵ : MonoidalCategory V
C✝ : Type u₁
inst✝⁴ : EnrichedCategory V C✝
W : Type (v + 1)
inst✝³ : Category.{v, v + 1} W
inst✝² : MonoidalCategory W
C : Type u₁
D : Type u₂
inst✝¹ : EnrichedCategory W C
inst✝ : EnrichedCategory W D
F : EnrichedFunctor W C D
X✝ Y✝ Z✝ : ForgetEnrichment W C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ForgetEnrichment.homOf W
      ((((λ_ (𝟙_ W)).inv ≫ (ForgetEnrichment.homTo W f ⊗ ForgetEnrichment.homTo W g)) ≫
          eComp W (ForgetEnrichment.to W X✝) (ForgetEnrichment.to W Y✝) (ForgetEnrichment.to W Z✝)) ≫
        map F (ForgetEnrichment.to W X✝) (ForgetEnrichment.to W Z✝)) =
    ForgetEnrichment.homOf W
        (ForgetEnrichment.homTo W f ≫ map F (ForgetEnrichment.to W X✝) (ForgetEnrichment.to W Y✝)) ≫
      ForgetEnrichment.homOf W
        (ForgetEnrichment.homTo W g ≫ map F (ForgetEnrichment.to W Y✝) (ForgetEnrichment.to W Z✝))
[PROOFSTEP]
apply_fun ForgetEnrichment.homTo W
[GOAL]
V : Type v
inst✝⁶ : Category.{w, v} V
inst✝⁵ : MonoidalCategory V
C✝ : Type u₁
inst✝⁴ : EnrichedCategory V C✝
W : Type (v + 1)
inst✝³ : Category.{v, v + 1} W
inst✝² : MonoidalCategory W
C : Type u₁
D : Type u₂
inst✝¹ : EnrichedCategory W C
inst✝ : EnrichedCategory W D
F : EnrichedFunctor W C D
X✝ Y✝ Z✝ : ForgetEnrichment W C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ForgetEnrichment.homTo W
      (ForgetEnrichment.homOf W
        ((((λ_ (𝟙_ W)).inv ≫ (ForgetEnrichment.homTo W f ⊗ ForgetEnrichment.homTo W g)) ≫
            eComp W (ForgetEnrichment.to W X✝) (ForgetEnrichment.to W Y✝) (ForgetEnrichment.to W Z✝)) ≫
          map F (ForgetEnrichment.to W X✝) (ForgetEnrichment.to W Z✝))) =
    ForgetEnrichment.homTo W
      (ForgetEnrichment.homOf W
          (ForgetEnrichment.homTo W f ≫ map F (ForgetEnrichment.to W X✝) (ForgetEnrichment.to W Y✝)) ≫
        ForgetEnrichment.homOf W
          (ForgetEnrichment.homTo W g ≫ map F (ForgetEnrichment.to W Y✝) (ForgetEnrichment.to W Z✝)))
[PROOFSTEP]
simp only [Iso.cancel_iso_inv_left, Category.assoc, tensor_comp, ForgetEnrichment.homTo_homOf, EnrichedFunctor.map_comp,
  forgetEnrichment_comp]
[GOAL]
V : Type v
inst✝⁶ : Category.{w, v} V
inst✝⁵ : MonoidalCategory V
C✝ : Type u₁
inst✝⁴ : EnrichedCategory V C✝
W : Type (v + 1)
inst✝³ : Category.{v, v + 1} W
inst✝² : MonoidalCategory W
C : Type u₁
D : Type u₂
inst✝¹ : EnrichedCategory W C
inst✝ : EnrichedCategory W D
F : EnrichedFunctor W C D
X✝ Y✝ Z✝ : ForgetEnrichment W C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (ForgetEnrichment.homTo W f ⊗ ForgetEnrichment.homTo W g) ≫
      (map F (ForgetEnrichment.to W X✝) (ForgetEnrichment.to W Y✝) ⊗
          map F (ForgetEnrichment.to W Y✝) (ForgetEnrichment.to W Z✝)) ≫
        eComp W (obj F (ForgetEnrichment.to W X✝)) (obj F (ForgetEnrichment.to W Y✝))
          (obj F (ForgetEnrichment.to W Z✝)) =
    (ForgetEnrichment.homTo W f ⊗ ForgetEnrichment.homTo W g) ≫
      (map F (ForgetEnrichment.to W X✝) (ForgetEnrichment.to W Y✝) ⊗
          map F (ForgetEnrichment.to W Y✝) (ForgetEnrichment.to W Z✝)) ≫
        eComp W (ForgetEnrichment.to W (ForgetEnrichment.of W (obj F (ForgetEnrichment.to W X✝))))
          (ForgetEnrichment.to W (ForgetEnrichment.of W (obj F (ForgetEnrichment.to W Y✝))))
          (ForgetEnrichment.to W (ForgetEnrichment.of W (obj F (ForgetEnrichment.to W Z✝))))
[PROOFSTEP]
rfl
[GOAL]
case inj
V : Type v
inst✝⁶ : Category.{w, v} V
inst✝⁵ : MonoidalCategory V
C✝ : Type u₁
inst✝⁴ : EnrichedCategory V C✝
W : Type (v + 1)
inst✝³ : Category.{v, v + 1} W
inst✝² : MonoidalCategory W
C : Type u₁
D : Type u₂
inst✝¹ : EnrichedCategory W C
inst✝ : EnrichedCategory W D
F : EnrichedFunctor W C D
X✝ Y✝ Z✝ : ForgetEnrichment W C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ Function.Injective (ForgetEnrichment.homTo W)
[PROOFSTEP]
intro f g w
[GOAL]
case inj
V : Type v
inst✝⁶ : Category.{w, v} V
inst✝⁵ : MonoidalCategory V
C✝ : Type u₁
inst✝⁴ : EnrichedCategory V C✝
W : Type (v + 1)
inst✝³ : Category.{v, v + 1} W
inst✝² : MonoidalCategory W
C : Type u₁
D : Type u₂
inst✝¹ : EnrichedCategory W C
inst✝ : EnrichedCategory W D
F : EnrichedFunctor W C D
X✝ Y✝ Z✝ : ForgetEnrichment W C
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
f g :
  ForgetEnrichment.of W (obj F (ForgetEnrichment.to W X✝)) ⟶ ForgetEnrichment.of W (obj F (ForgetEnrichment.to W Z✝))
w : ForgetEnrichment.homTo W f = ForgetEnrichment.homTo W g
⊢ f = g
[PROOFSTEP]
apply_fun ForgetEnrichment.homOf W at w
[GOAL]
case inj
V : Type v
inst✝⁶ : Category.{w, v} V
inst✝⁵ : MonoidalCategory V
C✝ : Type u₁
inst✝⁴ : EnrichedCategory V C✝
W : Type (v + 1)
inst✝³ : Category.{v, v + 1} W
inst✝² : MonoidalCategory W
C : Type u₁
D : Type u₂
inst✝¹ : EnrichedCategory W C
inst✝ : EnrichedCategory W D
F : EnrichedFunctor W C D
X✝ Y✝ Z✝ : ForgetEnrichment W C
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
f g :
  ForgetEnrichment.of W (obj F (ForgetEnrichment.to W X✝)) ⟶ ForgetEnrichment.of W (obj F (ForgetEnrichment.to W Z✝))
w : ForgetEnrichment.homOf W (ForgetEnrichment.homTo W f) = ForgetEnrichment.homOf W (ForgetEnrichment.homTo W g)
⊢ f = g
[PROOFSTEP]
simpa using w
[GOAL]
V : Type v
inst✝⁴ : Category.{w, v} V
inst✝³ : MonoidalCategory V
C : Type u₁
inst✝² : EnrichedCategory V C
D : Type u₂
inst✝¹ : EnrichedCategory V D
inst✝ : BraidedCategory V
F G : EnrichedFunctor V C D
X✝ Y✝ : Vᵒᵖ
f : X✝ ⟶ Y✝
σ : (fun A => GradedNatTrans ((Center.ofBraided V).toLaxMonoidalFunctor.toFunctor.obj A.unop) F G) X✝
X Y : C
⊢ (HalfBraiding.β ((Center.ofBraided V).toLaxMonoidalFunctor.toFunctor.obj Y✝.unop).snd
          (EnrichedCategory.Hom X Y)).hom ≫
      (EnrichedFunctor.map F X Y ⊗ (fun X => f.unop ≫ GradedNatTrans.app σ X) Y) ≫
        eComp V (EnrichedFunctor.obj F X) (EnrichedFunctor.obj F Y) (EnrichedFunctor.obj G Y) =
    ((fun X => f.unop ≫ GradedNatTrans.app σ X) X ⊗ EnrichedFunctor.map G X Y) ≫
      eComp V (EnrichedFunctor.obj F X) (EnrichedFunctor.obj G X) (EnrichedFunctor.obj G Y)
[PROOFSTEP]
have p := σ.naturality X Y
[GOAL]
V : Type v
inst✝⁴ : Category.{w, v} V
inst✝³ : MonoidalCategory V
C : Type u₁
inst✝² : EnrichedCategory V C
D : Type u₂
inst✝¹ : EnrichedCategory V D
inst✝ : BraidedCategory V
F G : EnrichedFunctor V C D
X✝ Y✝ : Vᵒᵖ
f : X✝ ⟶ Y✝
σ : (fun A => GradedNatTrans ((Center.ofBraided V).toLaxMonoidalFunctor.toFunctor.obj A.unop) F G) X✝
X Y : C
p :
  (HalfBraiding.β ((Center.ofBraided V).toLaxMonoidalFunctor.toFunctor.obj X✝.unop).snd
          (EnrichedCategory.Hom X Y)).hom ≫
      (EnrichedFunctor.map F X Y ⊗ GradedNatTrans.app σ Y) ≫
        eComp V (EnrichedFunctor.obj F X) (EnrichedFunctor.obj F Y) (EnrichedFunctor.obj G Y) =
    (GradedNatTrans.app σ X ⊗ EnrichedFunctor.map G X Y) ≫
      eComp V (EnrichedFunctor.obj F X) (EnrichedFunctor.obj G X) (EnrichedFunctor.obj G Y)
⊢ (HalfBraiding.β ((Center.ofBraided V).toLaxMonoidalFunctor.toFunctor.obj Y✝.unop).snd
          (EnrichedCategory.Hom X Y)).hom ≫
      (EnrichedFunctor.map F X Y ⊗ (fun X => f.unop ≫ GradedNatTrans.app σ X) Y) ≫
        eComp V (EnrichedFunctor.obj F X) (EnrichedFunctor.obj F Y) (EnrichedFunctor.obj G Y) =
    ((fun X => f.unop ≫ GradedNatTrans.app σ X) X ⊗ EnrichedFunctor.map G X Y) ≫
      eComp V (EnrichedFunctor.obj F X) (EnrichedFunctor.obj G X) (EnrichedFunctor.obj G Y)
[PROOFSTEP]
dsimp at p ⊢
[GOAL]
V : Type v
inst✝⁴ : Category.{w, v} V
inst✝³ : MonoidalCategory V
C : Type u₁
inst✝² : EnrichedCategory V C
D : Type u₂
inst✝¹ : EnrichedCategory V D
inst✝ : BraidedCategory V
F G : EnrichedFunctor V C D
X✝ Y✝ : Vᵒᵖ
f : X✝ ⟶ Y✝
σ : (fun A => GradedNatTrans ((Center.ofBraided V).toLaxMonoidalFunctor.toFunctor.obj A.unop) F G) X✝
X Y : C
p :
  (β_ X✝.unop (EnrichedCategory.Hom X Y)).hom ≫
      (EnrichedFunctor.map F X Y ⊗ GradedNatTrans.app σ Y) ≫
        eComp V (EnrichedFunctor.obj F X) (EnrichedFunctor.obj F Y) (EnrichedFunctor.obj G Y) =
    (GradedNatTrans.app σ X ⊗ EnrichedFunctor.map G X Y) ≫
      eComp V (EnrichedFunctor.obj F X) (EnrichedFunctor.obj G X) (EnrichedFunctor.obj G Y)
⊢ (β_ Y✝.unop (EnrichedCategory.Hom X Y)).hom ≫
      (EnrichedFunctor.map F X Y ⊗ f.unop ≫ GradedNatTrans.app σ Y) ≫
        eComp V (EnrichedFunctor.obj F X) (EnrichedFunctor.obj F Y) (EnrichedFunctor.obj G Y) =
    (f.unop ≫ GradedNatTrans.app σ X ⊗ EnrichedFunctor.map G X Y) ≫
      eComp V (EnrichedFunctor.obj F X) (EnrichedFunctor.obj G X) (EnrichedFunctor.obj G Y)
[PROOFSTEP]
rw [← id_tensor_comp_tensor_id (f.unop ≫ σ.app Y) _, id_tensor_comp, Category.assoc, Category.assoc, ←
  braiding_naturality_assoc, id_tensor_comp_tensor_id_assoc, p, ← tensor_comp_assoc, Category.id_comp]
[GOAL]
V : Type v
inst✝² : Category.{w, v} V
inst✝¹ : MonoidalCategory V
C✝ : Type u₁
inst✝ : EnrichedCategory V C✝
C : Type u₁
𝒞 : EnrichedCategory (Type v) C
D : Type u₂
𝒟 : EnrichedCategory (Type v) D
F : C ⥤ D
X : C
⊢ eId (Type v) X ≫ (fun X Y f => F.map f) X X = eId (Type v) ((fun X => F.obj X) X)
[PROOFSTEP]
ext ⟨⟩
[GOAL]
case h.unit
V : Type v
inst✝² : Category.{w, v} V
inst✝¹ : MonoidalCategory V
C✝ : Type u₁
inst✝ : EnrichedCategory V C✝
C : Type u₁
𝒞 : EnrichedCategory (Type v) C
D : Type u₂
𝒟 : EnrichedCategory (Type v) D
F : C ⥤ D
X : C
⊢ (eId (Type v) X ≫ (fun X Y f => F.map f) X X) PUnit.unit = eId (Type v) ((fun X => F.obj X) X) PUnit.unit
[PROOFSTEP]
exact F.map_id X
[GOAL]
V : Type v
inst✝² : Category.{w, v} V
inst✝¹ : MonoidalCategory V
C✝ : Type u₁
inst✝ : EnrichedCategory V C✝
C : Type u₁
𝒞 : EnrichedCategory (Type v) C
D : Type u₂
𝒟 : EnrichedCategory (Type v) D
F : C ⥤ D
X Y Z : C
⊢ eComp (Type v) X Y Z ≫ (fun X Y f => F.map f) X Z =
    ((fun X Y f => F.map f) X Y ⊗ (fun X Y f => F.map f) Y Z) ≫
      eComp (Type v) ((fun X => F.obj X) X) ((fun X => F.obj X) Y) ((fun X => F.obj X) Z)
[PROOFSTEP]
ext ⟨f, g⟩
[GOAL]
case h.mk
V : Type v
inst✝² : Category.{w, v} V
inst✝¹ : MonoidalCategory V
C✝ : Type u₁
inst✝ : EnrichedCategory V C✝
C : Type u₁
𝒞 : EnrichedCategory (Type v) C
D : Type u₂
𝒟 : EnrichedCategory (Type v) D
F : C ⥤ D
X Y Z : C
f : EnrichedCategory.Hom X Y
g : EnrichedCategory.Hom Y Z
⊢ (eComp (Type v) X Y Z ≫ (fun X Y f => F.map f) X Z) (f, g) =
    (((fun X Y f => F.map f) X Y ⊗ (fun X Y f => F.map f) Y Z) ≫
        eComp (Type v) ((fun X => F.obj X) X) ((fun X => F.obj X) Y) ((fun X => F.obj X) Z))
      (f, g)
[PROOFSTEP]
exact F.map_comp f g
[GOAL]
V : Type v
inst✝⁴ : Category.{w, v} V
inst✝³ : MonoidalCategory V
C✝ : Type u₁
inst✝² : EnrichedCategory V C✝
C : Type v
inst✝¹ : EnrichedCategory (Type v) C
D : Type v
inst✝ : EnrichedCategory (Type v) D
F G : EnrichedFunctor (Type v) C D
α : Type vᵒᵖ
σ : (yoneda.obj (↑enrichedFunctorTypeEquivFunctor F ⟶ ↑enrichedFunctorTypeEquivFunctor G)).obj α
X Y : C
⊢ (HalfBraiding.β ((Center.ofBraided (Type v)).toLaxMonoidalFunctor.toFunctor.obj α.unop).snd
          (EnrichedCategory.Hom X Y)).hom ≫
      (EnrichedFunctor.map F X Y ⊗ (fun X x => NatTrans.app (σ x) X) Y) ≫
        eComp (Type v) (EnrichedFunctor.obj F X) (EnrichedFunctor.obj F Y) (EnrichedFunctor.obj G Y) =
    ((fun X x => NatTrans.app (σ x) X) X ⊗ EnrichedFunctor.map G X Y) ≫
      eComp (Type v) (EnrichedFunctor.obj F X) (EnrichedFunctor.obj G X) (EnrichedFunctor.obj G Y)
[PROOFSTEP]
ext ⟨x, f⟩
[GOAL]
case h.mk
V : Type v
inst✝⁴ : Category.{w, v} V
inst✝³ : MonoidalCategory V
C✝ : Type u₁
inst✝² : EnrichedCategory V C✝
C : Type v
inst✝¹ : EnrichedCategory (Type v) C
D : Type v
inst✝ : EnrichedCategory (Type v) D
F G : EnrichedFunctor (Type v) C D
α : Type vᵒᵖ
σ : (yoneda.obj (↑enrichedFunctorTypeEquivFunctor F ⟶ ↑enrichedFunctorTypeEquivFunctor G)).obj α
X Y : C
x : ((Center.ofBraided (Type v)).toLaxMonoidalFunctor.toFunctor.obj α.unop).fst
f : EnrichedCategory.Hom X Y
⊢ ((HalfBraiding.β ((Center.ofBraided (Type v)).toLaxMonoidalFunctor.toFunctor.obj α.unop).snd
            (EnrichedCategory.Hom X Y)).hom ≫
        (EnrichedFunctor.map F X Y ⊗ (fun X x => NatTrans.app (σ x) X) Y) ≫
          eComp (Type v) (EnrichedFunctor.obj F X) (EnrichedFunctor.obj F Y) (EnrichedFunctor.obj G Y))
      (x, f) =
    (((fun X x => NatTrans.app (σ x) X) X ⊗ EnrichedFunctor.map G X Y) ≫
        eComp (Type v) (EnrichedFunctor.obj F X) (EnrichedFunctor.obj G X) (EnrichedFunctor.obj G Y))
      (x, f)
[PROOFSTEP]
exact (σ x).naturality f
[GOAL]
V : Type v
inst✝⁴ : Category.{w, v} V
inst✝³ : MonoidalCategory V
C✝ : Type u₁
inst✝² : EnrichedCategory V C✝
C : Type v
inst✝¹ : EnrichedCategory (Type v) C
D : Type v
inst✝ : EnrichedCategory (Type v) D
F G : EnrichedFunctor (Type v) C D
⊢ ∀ {X Y : Type vᵒᵖ} (f : X ⟶ Y),
    (enrichedNatTransYoneda F G).map f ≫
        ((fun α =>
              Iso.mk (fun σ x => NatTrans.mk fun X => GradedNatTrans.app σ X x) fun σ =>
                { app := fun X x => NatTrans.app (σ x) X,
                  naturality :=
                    (_ :
                      ∀ (X Y : C),
                        (HalfBraiding.β ((Center.ofBraided (Type v)).toLaxMonoidalFunctor.toFunctor.obj α.unop).snd
                                (EnrichedCategory.Hom X Y)).hom ≫
                            (EnrichedFunctor.map F X Y ⊗ (fun X x => NatTrans.app (σ x) X) Y) ≫
                              eComp (Type v) (EnrichedFunctor.obj F X) (EnrichedFunctor.obj F Y)
                                (EnrichedFunctor.obj G Y) =
                          ((fun X x => NatTrans.app (σ x) X) X ⊗ EnrichedFunctor.map G X Y) ≫
                            eComp (Type v) (EnrichedFunctor.obj F X) (EnrichedFunctor.obj G X)
                              (EnrichedFunctor.obj G Y)) })
            Y).hom =
      ((fun α =>
              Iso.mk (fun σ x => NatTrans.mk fun X => GradedNatTrans.app σ X x) fun σ =>
                { app := fun X x => NatTrans.app (σ x) X,
                  naturality :=
                    (_ :
                      ∀ (X Y : C),
                        (HalfBraiding.β ((Center.ofBraided (Type v)).toLaxMonoidalFunctor.toFunctor.obj α.unop).snd
                                (EnrichedCategory.Hom X Y)).hom ≫
                            (EnrichedFunctor.map F X Y ⊗ (fun X x => NatTrans.app (σ x) X) Y) ≫
                              eComp (Type v) (EnrichedFunctor.obj F X) (EnrichedFunctor.obj F Y)
                                (EnrichedFunctor.obj G Y) =
                          ((fun X x => NatTrans.app (σ x) X) X ⊗ EnrichedFunctor.map G X Y) ≫
                            eComp (Type v) (EnrichedFunctor.obj F X) (EnrichedFunctor.obj G X)
                              (EnrichedFunctor.obj G Y)) })
            X).hom ≫
        (yoneda.obj (↑enrichedFunctorTypeEquivFunctor F ⟶ ↑enrichedFunctorTypeEquivFunctor G)).map f
[PROOFSTEP]
aesop_cat


[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
⊢ ↑(Adjunction.homEquiv adj A X) u ≫ F.map p = i ≫ ↑(Adjunction.homEquiv adj B Y) v
[PROOFSTEP]
simp only [Adjunction.homEquiv_unit, assoc, ← F.map_comp, sq.w]
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
⊢ NatTrans.app adj.unit A ≫ F.map (G.map i ≫ v) = i ≫ NatTrans.app adj.unit B ≫ F.map v
[PROOFSTEP]
rw [F.map_comp, Adjunction.unit_naturality_assoc]
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.1925, u_1} C
inst✝ : Category.{?u.1929, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
l : LiftStruct sq
⊢ i ≫ ↑(Adjunction.homEquiv adj B X) l.l = ↑(Adjunction.homEquiv adj A X) u
[PROOFSTEP]
rw [← adj.homEquiv_naturality_left, l.fac_left]
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.1925, u_1} C
inst✝ : Category.{?u.1929, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
l : LiftStruct sq
⊢ ↑(Adjunction.homEquiv adj B X) l.l ≫ F.map p = ↑(Adjunction.homEquiv adj B Y) v
[PROOFSTEP]
rw [← Adjunction.homEquiv_naturality_right, l.fac_right]
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.1925, u_1} C
inst✝ : Category.{?u.1929, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
l : LiftStruct (_ : CommSq (↑(Adjunction.homEquiv adj A X) u) i (F.map p) (↑(Adjunction.homEquiv adj B Y) v))
⊢ G.map i ≫ ↑(Adjunction.homEquiv adj B X).symm l.l = u
[PROOFSTEP]
rw [← Adjunction.homEquiv_naturality_left_symm, l.fac_left]
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.1925, u_1} C
inst✝ : Category.{?u.1929, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
l : LiftStruct (_ : CommSq (↑(Adjunction.homEquiv adj A X) u) i (F.map p) (↑(Adjunction.homEquiv adj B Y) v))
⊢ ↑(Adjunction.homEquiv adj A X).symm (↑(Adjunction.homEquiv adj A X) u) = u
[PROOFSTEP]
apply (adj.homEquiv _ _).left_inv
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.1925, u_1} C
inst✝ : Category.{?u.1929, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
l : LiftStruct (_ : CommSq (↑(Adjunction.homEquiv adj A X) u) i (F.map p) (↑(Adjunction.homEquiv adj B Y) v))
⊢ ↑(Adjunction.homEquiv adj B X).symm l.l ≫ p = v
[PROOFSTEP]
rw [← Adjunction.homEquiv_naturality_right_symm, l.fac_right]
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.1925, u_1} C
inst✝ : Category.{?u.1929, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
l : LiftStruct (_ : CommSq (↑(Adjunction.homEquiv adj A X) u) i (F.map p) (↑(Adjunction.homEquiv adj B Y) v))
⊢ ↑(Adjunction.homEquiv adj B Y).symm (↑(Adjunction.homEquiv adj B Y) v) = v
[PROOFSTEP]
apply (adj.homEquiv _ _).left_inv
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.1925, u_1} C
inst✝ : Category.{?u.1929, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
⊢ Function.LeftInverse
    (fun l =>
      { l := ↑(Adjunction.homEquiv adj B X).symm l.l,
        fac_left := (_ : G.map i ≫ ↑(Adjunction.homEquiv adj B X).symm l.l = u),
        fac_right := (_ : ↑(Adjunction.homEquiv adj B X).symm l.l ≫ p = v) })
    fun l =>
    { l := ↑(Adjunction.homEquiv adj B X) l.l,
      fac_left := (_ : i ≫ ↑(Adjunction.homEquiv adj B X) l.l = ↑(Adjunction.homEquiv adj A X) u),
      fac_right := (_ : ↑(Adjunction.homEquiv adj B X) l.l ≫ F.map p = ↑(Adjunction.homEquiv adj B Y) v) }
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.1925, u_1} C
inst✝ : Category.{?u.1929, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
⊢ Function.RightInverse
    (fun l =>
      { l := ↑(Adjunction.homEquiv adj B X).symm l.l,
        fac_left := (_ : G.map i ≫ ↑(Adjunction.homEquiv adj B X).symm l.l = u),
        fac_right := (_ : ↑(Adjunction.homEquiv adj B X).symm l.l ≫ p = v) })
    fun l =>
    { l := ↑(Adjunction.homEquiv adj B X) l.l,
      fac_left := (_ : i ≫ ↑(Adjunction.homEquiv adj B X) l.l = ↑(Adjunction.homEquiv adj A X) u),
      fac_right := (_ : ↑(Adjunction.homEquiv adj B X) l.l ≫ F.map p = ↑(Adjunction.homEquiv adj B Y) v) }
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
⊢ HasLift (_ : CommSq (↑(Adjunction.homEquiv adj A X) u) i (F.map p) (↑(Adjunction.homEquiv adj B Y) v)) ↔ HasLift sq
[PROOFSTEP]
simp only [HasLift.iff]
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
⊢ Nonempty (LiftStruct (_ : CommSq (↑(Adjunction.homEquiv adj A X) u) i (F.map p) (↑(Adjunction.homEquiv adj B Y) v))) ↔
    Nonempty (LiftStruct sq)
[PROOFSTEP]
exact Equiv.nonempty_congr (sq.rightAdjointLiftStructEquiv adj).symm
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.8583, u_1} C
inst✝¹ : Category.{?u.8587, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
inst✝ : HasLift sq
⊢ HasLift (_ : CommSq (↑(Adjunction.homEquiv adj A X) u) i (F.map p) (↑(Adjunction.homEquiv adj B Y) v))
[PROOFSTEP]
rw [right_adjoint_hasLift_iff]
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.8583, u_1} C
inst✝¹ : Category.{?u.8587, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
inst✝ : HasLift sq
⊢ HasLift ?sq
case sq
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.8583, u_1} C
inst✝¹ : Category.{?u.8587, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
inst✝ : HasLift sq
⊢ CommSq u (G.map i) p v
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_4, u_1} C
inst✝ : Category.{u_3, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : A ⟶ F.obj X
v : B ⟶ F.obj Y
sq : CommSq u i (F.map p) v
adj : G ⊣ F
⊢ ↑(Adjunction.homEquiv adj A X).symm u ≫ p = G.map i ≫ ↑(Adjunction.homEquiv adj B Y).symm v
[PROOFSTEP]
simp only [Adjunction.homEquiv_counit, assoc, ← G.map_comp_assoc, ← sq.w]
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_4, u_1} C
inst✝ : Category.{u_3, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : A ⟶ F.obj X
v : B ⟶ F.obj Y
sq : CommSq u i (F.map p) v
adj : G ⊣ F
⊢ G.map u ≫ NatTrans.app adj.counit X ≫ p = G.map (u ≫ F.map p) ≫ NatTrans.app adj.counit Y
[PROOFSTEP]
rw [G.map_comp, assoc, Adjunction.counit_naturality]
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.11857, u_1} C
inst✝ : Category.{?u.11861, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : A ⟶ F.obj X
v : B ⟶ F.obj Y
sq : CommSq u i (F.map p) v
adj : G ⊣ F
l : LiftStruct sq
⊢ G.map i ≫ ↑(Adjunction.homEquiv adj B X).symm l.l = ↑(Adjunction.homEquiv adj A X).symm u
[PROOFSTEP]
rw [← adj.homEquiv_naturality_left_symm, l.fac_left]
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.11857, u_1} C
inst✝ : Category.{?u.11861, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : A ⟶ F.obj X
v : B ⟶ F.obj Y
sq : CommSq u i (F.map p) v
adj : G ⊣ F
l : LiftStruct sq
⊢ ↑(Adjunction.homEquiv adj B X).symm l.l ≫ p = ↑(Adjunction.homEquiv adj B Y).symm v
[PROOFSTEP]
rw [← adj.homEquiv_naturality_right_symm, l.fac_right]
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.11857, u_1} C
inst✝ : Category.{?u.11861, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : A ⟶ F.obj X
v : B ⟶ F.obj Y
sq : CommSq u i (F.map p) v
adj : G ⊣ F
l : LiftStruct (_ : CommSq (↑(Adjunction.homEquiv adj A X).symm u) (G.map i) p (↑(Adjunction.homEquiv adj B Y).symm v))
⊢ i ≫ ↑(Adjunction.homEquiv adj B X) l.l = u
[PROOFSTEP]
rw [← adj.homEquiv_naturality_left, l.fac_left]
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.11857, u_1} C
inst✝ : Category.{?u.11861, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : A ⟶ F.obj X
v : B ⟶ F.obj Y
sq : CommSq u i (F.map p) v
adj : G ⊣ F
l : LiftStruct (_ : CommSq (↑(Adjunction.homEquiv adj A X).symm u) (G.map i) p (↑(Adjunction.homEquiv adj B Y).symm v))
⊢ ↑(Adjunction.homEquiv adj A X) (↑(Adjunction.homEquiv adj A X).symm u) = u
[PROOFSTEP]
apply (adj.homEquiv _ _).right_inv
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.11857, u_1} C
inst✝ : Category.{?u.11861, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : A ⟶ F.obj X
v : B ⟶ F.obj Y
sq : CommSq u i (F.map p) v
adj : G ⊣ F
l : LiftStruct (_ : CommSq (↑(Adjunction.homEquiv adj A X).symm u) (G.map i) p (↑(Adjunction.homEquiv adj B Y).symm v))
⊢ ↑(Adjunction.homEquiv adj B X) l.l ≫ F.map p = v
[PROOFSTEP]
rw [← adj.homEquiv_naturality_right, l.fac_right]
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.11857, u_1} C
inst✝ : Category.{?u.11861, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : A ⟶ F.obj X
v : B ⟶ F.obj Y
sq : CommSq u i (F.map p) v
adj : G ⊣ F
l : LiftStruct (_ : CommSq (↑(Adjunction.homEquiv adj A X).symm u) (G.map i) p (↑(Adjunction.homEquiv adj B Y).symm v))
⊢ ↑(Adjunction.homEquiv adj B Y) (↑(Adjunction.homEquiv adj B Y).symm v) = v
[PROOFSTEP]
apply (adj.homEquiv _ _).right_inv
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.11857, u_1} C
inst✝ : Category.{?u.11861, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : A ⟶ F.obj X
v : B ⟶ F.obj Y
sq : CommSq u i (F.map p) v
adj : G ⊣ F
⊢ Function.LeftInverse
    (fun l =>
      { l := ↑(Adjunction.homEquiv adj B X) l.l, fac_left := (_ : i ≫ ↑(Adjunction.homEquiv adj B X) l.l = u),
        fac_right := (_ : ↑(Adjunction.homEquiv adj B X) l.l ≫ F.map p = v) })
    fun l =>
    { l := ↑(Adjunction.homEquiv adj B X).symm l.l,
      fac_left := (_ : G.map i ≫ ↑(Adjunction.homEquiv adj B X).symm l.l = ↑(Adjunction.homEquiv adj A X).symm u),
      fac_right := (_ : ↑(Adjunction.homEquiv adj B X).symm l.l ≫ p = ↑(Adjunction.homEquiv adj B Y).symm v) }
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{?u.11857, u_1} C
inst✝ : Category.{?u.11861, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : A ⟶ F.obj X
v : B ⟶ F.obj Y
sq : CommSq u i (F.map p) v
adj : G ⊣ F
⊢ Function.RightInverse
    (fun l =>
      { l := ↑(Adjunction.homEquiv adj B X) l.l, fac_left := (_ : i ≫ ↑(Adjunction.homEquiv adj B X) l.l = u),
        fac_right := (_ : ↑(Adjunction.homEquiv adj B X) l.l ≫ F.map p = v) })
    fun l =>
    { l := ↑(Adjunction.homEquiv adj B X).symm l.l,
      fac_left := (_ : G.map i ≫ ↑(Adjunction.homEquiv adj B X).symm l.l = ↑(Adjunction.homEquiv adj A X).symm u),
      fac_right := (_ : ↑(Adjunction.homEquiv adj B X).symm l.l ≫ p = ↑(Adjunction.homEquiv adj B Y).symm v) }
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_4, u_1} C
inst✝ : Category.{u_3, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : A ⟶ F.obj X
v : B ⟶ F.obj Y
sq : CommSq u i (F.map p) v
adj : G ⊣ F
⊢ HasLift (_ : CommSq (↑(Adjunction.homEquiv adj A X).symm u) (G.map i) p (↑(Adjunction.homEquiv adj B Y).symm v)) ↔
    HasLift sq
[PROOFSTEP]
simp only [HasLift.iff]
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_4, u_1} C
inst✝ : Category.{u_3, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : A ⟶ F.obj X
v : B ⟶ F.obj Y
sq : CommSq u i (F.map p) v
adj : G ⊣ F
⊢ Nonempty
      (LiftStruct
        (_ : CommSq (↑(Adjunction.homEquiv adj A X).symm u) (G.map i) p (↑(Adjunction.homEquiv adj B Y).symm v))) ↔
    Nonempty (LiftStruct sq)
[PROOFSTEP]
exact Equiv.nonempty_congr (sq.leftAdjointLiftStructEquiv adj).symm
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.18083, u_1} C
inst✝¹ : Category.{?u.18087, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : A ⟶ F.obj X
v : B ⟶ F.obj Y
sq : CommSq u i (F.map p) v
adj : G ⊣ F
inst✝ : HasLift sq
⊢ HasLift (_ : CommSq (↑(Adjunction.homEquiv adj A X).symm u) (G.map i) p (↑(Adjunction.homEquiv adj B Y).symm v))
[PROOFSTEP]
rw [left_adjoint_hasLift_iff]
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.18083, u_1} C
inst✝¹ : Category.{?u.18087, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : A ⟶ F.obj X
v : B ⟶ F.obj Y
sq : CommSq u i (F.map p) v
adj : G ⊣ F
inst✝ : HasLift sq
⊢ HasLift ?sq
case sq
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.18083, u_1} C
inst✝¹ : Category.{?u.18087, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : A ⟶ F.obj X
v : B ⟶ F.obj Y
sq : CommSq u i (F.map p) v
adj : G ⊣ F
inst✝ : HasLift sq
⊢ CommSq u i (F.map p) v
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
⊢ HasLiftingProperty (G.map i) p ↔ HasLiftingProperty i (F.map p)
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
⊢ HasLiftingProperty (G.map i) p → HasLiftingProperty i (F.map p)
[PROOFSTEP]
intro
[GOAL]
case mpr
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
⊢ HasLiftingProperty i (F.map p) → HasLiftingProperty (G.map i) p
[PROOFSTEP]
intro
[GOAL]
case mp
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty (G.map i) p
⊢ HasLiftingProperty i (F.map p)
[PROOFSTEP]
constructor
[GOAL]
case mpr
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty i (F.map p)
⊢ HasLiftingProperty (G.map i) p
[PROOFSTEP]
constructor
[GOAL]
case mp.sq_hasLift
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty (G.map i) p
⊢ ∀ {f : A ⟶ F.obj X} {g : B ⟶ F.obj Y} (sq : CommSq f i (F.map p) g), CommSq.HasLift sq
[PROOFSTEP]
intro f g sq
[GOAL]
case mpr.sq_hasLift
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty i (F.map p)
⊢ ∀ {f : G.obj A ⟶ X} {g : G.obj B ⟶ Y} (sq : CommSq f (G.map i) p g), CommSq.HasLift sq
[PROOFSTEP]
intro f g sq
[GOAL]
case mp.sq_hasLift
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty (G.map i) p
f : A ⟶ F.obj X
g : B ⟶ F.obj Y
sq : CommSq f i (F.map p) g
⊢ CommSq.HasLift sq
[PROOFSTEP]
rw [← sq.left_adjoint_hasLift_iff adj]
[GOAL]
case mp.sq_hasLift
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty (G.map i) p
f : A ⟶ F.obj X
g : B ⟶ F.obj Y
sq : CommSq f i (F.map p) g
⊢ CommSq.HasLift (_ : CommSq (↑(homEquiv adj A X).symm f) (G.map i) p (↑(homEquiv adj B Y).symm g))
[PROOFSTEP]
infer_instance
[GOAL]
case mpr.sq_hasLift
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty i (F.map p)
f : G.obj A ⟶ X
g : G.obj B ⟶ Y
sq : CommSq f (G.map i) p g
⊢ CommSq.HasLift sq
[PROOFSTEP]
rw [← sq.right_adjoint_hasLift_iff adj]
[GOAL]
case mpr.sq_hasLift
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty i (F.map p)
f : G.obj A ⟶ X
g : G.obj B ⟶ Y
sq : CommSq f (G.map i) p g
⊢ CommSq.HasLift (_ : CommSq (↑(homEquiv adj A X) f) i (F.map p) (↑(homEquiv adj B Y) g))
[PROOFSTEP]
infer_instance


[GOAL]
I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
f : J → I
⊢ (j : J) → Category.{?u.5215, u₁} ((C ∘ f) j)
[PROOFSTEP]
dsimp
[GOAL]
I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
f : J → I
⊢ (j : J) → Category.{?u.5215, u₁} (C (f j))
[PROOFSTEP]
infer_instance
[GOAL]
I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
g : J → I
⊢ (j : J) → Category.{?u.19534, u₁} (C (g j))
[PROOFSTEP]
infer_instance
[GOAL]
I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
K : Type w₂
f : K → J
g : J → I
X Y : (i : I) → C i
f' : X ⟶ Y
⊢ (comap C g ⋙ comap (C ∘ g) f).map f' ≫ (fun X b => 𝟙 (X (g (f b)))) Y =
    (fun X b => 𝟙 (X (g (f b)))) X ≫ (comap C (g ∘ f)).map f'
[PROOFSTEP]
simp only [comap, Function.comp]
[GOAL]
I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
K : Type w₂
f : K → J
g : J → I
X Y : (i : I) → C i
f' : X ⟶ Y
⊢ ((Functor.mk { obj := fun f i => f (g i), map := fun {X Y} α i => α (g i) } ⋙
            Functor.mk { obj := fun f_1 i => f_1 (f i), map := fun {X Y} α i => α (f i) }).map
        f' ≫
      fun b => 𝟙 (Y (g (f b)))) =
    (fun b => 𝟙 (X (g (f b)))) ≫ fun i => f' (g (f i))
[PROOFSTEP]
funext
[GOAL]
case h
I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
K : Type w₂
f : K → J
g : J → I
X Y : (i : I) → C i
f' : X ⟶ Y
x✝ : K
⊢ ((Functor.mk { obj := fun f i => f (g i), map := fun {X Y} α i => α (g i) } ⋙
              Functor.mk { obj := fun f_1 i => f_1 (f i), map := fun {X Y} α i => α (f i) }).map
          f' ≫
        fun b => 𝟙 (Y (g (f b))))
      x✝ =
    ((fun b => 𝟙 (X (g (f b)))) ≫ fun i => f' (g (f i))) x✝
[PROOFSTEP]
simp
[GOAL]
I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
K : Type w₂
f : K → J
g : J → I
X Y : (i : I) → C i
f' : X ⟶ Y
⊢ (comap C (g ∘ f)).map f' ≫ (fun X b => 𝟙 (X (g (f b)))) Y =
    (fun X b => 𝟙 (X (g (f b)))) X ≫ (comap C g ⋙ comap (C ∘ g) f).map f'
[PROOFSTEP]
simp only [comap, Function.comp]
[GOAL]
I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
K : Type w₂
f : K → J
g : J → I
X Y : (i : I) → C i
f' : X ⟶ Y
⊢ ((fun i => f' (g (f i))) ≫ fun b => 𝟙 (Y (g (f b)))) =
    (fun b => 𝟙 (X (g (f b)))) ≫
      (Functor.mk { obj := fun f i => f (g i), map := fun {X Y} α i => α (g i) } ⋙
            Functor.mk { obj := fun f_1 i => f_1 (f i), map := fun {X Y} α i => α (f i) }).map
        f'
[PROOFSTEP]
funext
[GOAL]
case h
I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
K : Type w₂
f : K → J
g : J → I
X Y : (i : I) → C i
f' : X ⟶ Y
x✝ : K
⊢ ((fun i => f' (g (f i))) ≫ fun b => 𝟙 (Y (g (f b)))) x✝ =
    ((fun b => 𝟙 (X (g (f b)))) ≫
        (Functor.mk { obj := fun f i => f (g i), map := fun {X Y} α i => α (g i) } ⋙
              Functor.mk { obj := fun f_1 i => f_1 (f i), map := fun {X Y} α i => α (f i) }).map
          f')
      x✝
[PROOFSTEP]
simp
[GOAL]
I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
K : Type w₂
h : J → I
j : J
⊢ ∀ {X Y : (i : I) → C i} (f : X ⟶ Y),
    (comap C h ⋙ eval (C ∘ h) j).map f ≫ ((fun f => Iso.refl ((comap C h ⋙ eval (C ∘ h) j).obj f)) Y).hom =
      ((fun f => Iso.refl ((comap C h ⋙ eval (C ∘ h) j).obj f)) X).hom ≫ (eval C (h j)).map f
[PROOFSTEP]
simp only [Iso.refl]
[GOAL]
I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
K : Type w₂
h : J → I
j : J
⊢ ∀ {X Y : (i : I) → C i} (f : X ⟶ Y),
    (comap C h ⋙ eval (C ∘ h) j).map f ≫ 𝟙 ((comap C h ⋙ eval (C ∘ h) j).obj Y) =
      𝟙 ((comap C h ⋙ eval (C ∘ h) j).obj X) ≫ (eval C (h j)).map f
[PROOFSTEP]
aesop_cat
[GOAL]
I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₀
D : J → Type u₁
inst✝ : (j : J) → Category.{v₁, u₁} (D j)
i : I
⊢ Category.{v₁, u₁} (Sum.elim C D (Sum.inl i))
[PROOFSTEP]
dsimp
[GOAL]
I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₀
D : J → Type u₁
inst✝ : (j : J) → Category.{v₁, u₁} (D j)
i : I
⊢ Category.{v₁, u₁} (C i)
[PROOFSTEP]
infer_instance
[GOAL]
I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₀
D : J → Type u₁
inst✝ : (j : J) → Category.{v₁, u₁} (D j)
j : J
⊢ Category.{v₁, u₁} (Sum.elim C D (Sum.inr j))
[PROOFSTEP]
dsimp
[GOAL]
I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₀
D : J → Type u₁
inst✝ : (j : J) → Category.{v₁, u₁} (D j)
j : J
⊢ Category.{v₁, u₁} (D j)
[PROOFSTEP]
infer_instance
[GOAL]
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ≅ Y
i : I
⊢ f.hom i ≫ f.inv i = 𝟙 (X i)
[PROOFSTEP]
rw [← comp_apply, Iso.hom_inv_id, id_apply]
[GOAL]
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ≅ Y
i : I
⊢ f.inv i ≫ f.hom i = 𝟙 (Y i)
[PROOFSTEP]
rw [← comp_apply, Iso.inv_hom_id, id_apply]
[GOAL]
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (D i)
A : Type u₁
inst✝ : Category.{u₁, u₁} A
x x' : (i : I) → C i
h : x = x'
i : I
⊢ eqToHom h i = eqToHom (_ : x i = x' i)
[PROOFSTEP]
subst h
[GOAL]
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (D i)
A : Type u₁
inst✝ : Category.{u₁, u₁} A
x : (i : I) → C i
i : I
⊢ eqToHom (_ : x = x) i = eqToHom (_ : x i = x i)
[PROOFSTEP]
rfl
[GOAL]
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (D i)
A : Type u₁
inst✝ : Category.{u₁, u₁} A
f : (i : I) → A ⥤ C i
i : I
⊢ pi' f ⋙ Pi.eval C i = f i
[PROOFSTEP]
apply Functor.ext
[GOAL]
case h_map
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (D i)
A : Type u₁
inst✝ : Category.{u₁, u₁} A
f : (i : I) → A ⥤ C i
i : I
⊢ autoParam
    (∀ (X Y : A) (f_1 : X ⟶ Y),
      (pi' f ⋙ Pi.eval C i).map f_1 =
        eqToHom (_ : ?F.obj X = ?G.obj X) ≫ (f i).map f_1 ≫ eqToHom (_ : (f i).obj Y = (pi' f ⋙ Pi.eval C i).obj Y))
    _auto✝
case h_obj
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (D i)
A : Type u₁
inst✝ : Category.{u₁, u₁} A
f : (i : I) → A ⥤ C i
i : I
⊢ ∀ (X : A), (pi' f ⋙ Pi.eval C i).obj X = (f i).obj X
[PROOFSTEP]
intro _ _ _
[GOAL]
case h_map
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (D i)
A : Type u₁
inst✝ : Category.{u₁, u₁} A
f : (i : I) → A ⥤ C i
i : I
X✝ Y✝ : A
f✝ : X✝ ⟶ Y✝
⊢ (pi' f ⋙ Pi.eval C i).map f✝ =
    eqToHom (_ : ?F.obj X✝ = ?G.obj X✝) ≫ (f i).map f✝ ≫ eqToHom (_ : (f i).obj Y✝ = (pi' f ⋙ Pi.eval C i).obj Y✝)
[PROOFSTEP]
simp
[GOAL]
case h_obj
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (D i)
A : Type u₁
inst✝ : Category.{u₁, u₁} A
f : (i : I) → A ⥤ C i
i : I
⊢ ∀ (X : A), (pi' f ⋙ Pi.eval C i).obj X = (f i).obj X
[PROOFSTEP]
intro _
[GOAL]
case h_obj
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (D i)
A : Type u₁
inst✝ : Category.{u₁, u₁} A
f : (i : I) → A ⥤ C i
i : I
X✝ : A
⊢ (pi' f ⋙ Pi.eval C i).obj X✝ = (f i).obj X✝
[PROOFSTEP]
rfl
[GOAL]
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (D i)
A : Type u₁
inst✝ : Category.{u₁, u₁} A
f f' : A ⥤ ((i : I) → C i)
h : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
⊢ f = f'
[PROOFSTEP]
apply Functor.ext
[GOAL]
case h_map
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (D i)
A : Type u₁
inst✝ : Category.{u₁, u₁} A
f f' : A ⥤ ((i : I) → C i)
h : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
⊢ autoParam
    (∀ (X Y : A) (f_1 : X ⟶ Y),
      f.map f_1 = eqToHom (_ : ?F.obj X = ?G.obj X) ≫ f'.map f_1 ≫ eqToHom (_ : f'.obj Y = f.obj Y))
    _auto✝
case h_obj
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (D i)
A : Type u₁
inst✝ : Category.{u₁, u₁} A
f f' : A ⥤ ((i : I) → C i)
h : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
⊢ ∀ (X : A), f.obj X = f'.obj X
[PROOFSTEP]
rotate_left
[GOAL]
case h_obj
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (D i)
A : Type u₁
inst✝ : Category.{u₁, u₁} A
f f' : A ⥤ ((i : I) → C i)
h : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
⊢ ∀ (X : A), f.obj X = f'.obj X
[PROOFSTEP]
intro X
[GOAL]
case h_obj
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (D i)
A : Type u₁
inst✝ : Category.{u₁, u₁} A
f f' : A ⥤ ((i : I) → C i)
h : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
X : A
⊢ f.obj X = f'.obj X
[PROOFSTEP]
ext i
[GOAL]
case h_obj.h
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (D i)
A : Type u₁
inst✝ : Category.{u₁, u₁} A
f f' : A ⥤ ((i : I) → C i)
h : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
X : A
i : I
⊢ f.obj X i = f'.obj X i
[PROOFSTEP]
specialize h i
[GOAL]
case h_obj.h
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (D i)
A : Type u₁
inst✝ : Category.{u₁, u₁} A
f f' : A ⥤ ((i : I) → C i)
X : A
i : I
h : f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
⊢ f.obj X i = f'.obj X i
[PROOFSTEP]
have := congr_obj h X
[GOAL]
case h_obj.h
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (D i)
A : Type u₁
inst✝ : Category.{u₁, u₁} A
f f' : A ⥤ ((i : I) → C i)
X : A
i : I
h : f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
this : (f ⋙ Pi.eval C i).obj X = (f' ⋙ Pi.eval C i).obj X
⊢ f.obj X i = f'.obj X i
[PROOFSTEP]
simpa
[GOAL]
case h_map
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (D i)
A : Type u₁
inst✝ : Category.{u₁, u₁} A
f f' : A ⥤ ((i : I) → C i)
h : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
⊢ autoParam
    (∀ (X Y : A) (f_1 : X ⟶ Y),
      f.map f_1 = eqToHom (_ : f.obj X = f'.obj X) ≫ f'.map f_1 ≫ eqToHom (_ : f'.obj Y = f.obj Y))
    _auto✝
[PROOFSTEP]
intro X Y g
[GOAL]
case h_map
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (D i)
A : Type u₁
inst✝ : Category.{u₁, u₁} A
f f' : A ⥤ ((i : I) → C i)
h : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
X Y : A
g : X ⟶ Y
⊢ f.map g = eqToHom (_ : f.obj X = f'.obj X) ≫ f'.map g ≫ eqToHom (_ : f'.obj Y = f.obj Y)
[PROOFSTEP]
dsimp
[GOAL]
case h_map
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (D i)
A : Type u₁
inst✝ : Category.{u₁, u₁} A
f f' : A ⥤ ((i : I) → C i)
h : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
X Y : A
g : X ⟶ Y
⊢ f.map g = eqToHom (_ : f.obj X = f'.obj X) ≫ f'.map g ≫ eqToHom (_ : f'.obj Y = f.obj Y)
[PROOFSTEP]
funext i
[GOAL]
case h_map.h
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (D i)
A : Type u₁
inst✝ : Category.{u₁, u₁} A
f f' : A ⥤ ((i : I) → C i)
h : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
X Y : A
g : X ⟶ Y
i : I
⊢ f.map g i = (eqToHom (_ : f.obj X = f'.obj X) ≫ f'.map g ≫ eqToHom (_ : f'.obj Y = f.obj Y)) i
[PROOFSTEP]
specialize h i
[GOAL]
case h_map.h
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (D i)
A : Type u₁
inst✝ : Category.{u₁, u₁} A
f f' : A ⥤ ((i : I) → C i)
h✝ : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
X Y : A
g : X ⟶ Y
i : I
h : f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
⊢ f.map g i = (eqToHom (_ : f.obj X = f'.obj X) ≫ f'.map g ≫ eqToHom (_ : f'.obj Y = f.obj Y)) i
[PROOFSTEP]
have := congr_hom h g
[GOAL]
case h_map.h
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (D i)
A : Type u₁
inst✝ : Category.{u₁, u₁} A
f f' : A ⥤ ((i : I) → C i)
h✝ : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
X Y : A
g : X ⟶ Y
i : I
h : f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
this :
  (f ⋙ Pi.eval C i).map g =
    eqToHom (_ : (f ⋙ Pi.eval C i).obj X = (f' ⋙ Pi.eval C i).obj X) ≫
      (f' ⋙ Pi.eval C i).map g ≫ eqToHom (_ : (f' ⋙ Pi.eval C i).obj Y = (f ⋙ Pi.eval C i).obj Y)
⊢ f.map g i = (eqToHom (_ : f.obj X = f'.obj X) ≫ f'.map g ≫ eqToHom (_ : f'.obj Y = f.obj Y)) i
[PROOFSTEP]
simpa


[GOAL]
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X✝ B : C
J : Type w
F : Discrete J ⥤ Over B
c : Cone F
X Y : WidePullbackShape J
f : X ⟶ Y
⊢ ((Functor.const (WidePullbackShape J)).obj c.pt.left).map f ≫
      (fun X => Option.casesOn X c.pt.hom fun j => (NatTrans.app c.π { as := j }).left) Y =
    (fun X => Option.casesOn X c.pt.hom fun j => (NatTrans.app c.π { as := j }).left) X ≫
      (widePullbackDiagramOfDiagramOver B F).map f
[PROOFSTEP]
dsimp
[GOAL]
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X✝ B : C
J : Type w
F : Discrete J ⥤ Over B
c : Cone F
X Y : WidePullbackShape J
f : X ⟶ Y
⊢ 𝟙 c.pt.left ≫ Option.rec c.pt.hom (fun val => (NatTrans.app c.π { as := val }).left) Y =
    Option.rec c.pt.hom (fun val => (NatTrans.app c.π { as := val }).left) X ≫
      WidePullbackShape.Hom.rec (motive := fun a a_1 t =>
        X = a →
          Y = a_1 →
            HEq f t →
              (Option.rec B (fun val => (F.obj { as := val }).left) X ⟶
                Option.rec B (fun val => (F.obj { as := val }).left) Y))
        (fun X_1 h =>
          Eq.rec (motive := fun x x_1 =>
            Y = x →
              HEq f (𝟙 x) →
                (Option.rec B (fun val => (F.obj { as := val }).left) X ⟶
                  Option.rec B (fun val => (F.obj { as := val }).left) Y))
            (fun h =>
              Eq.rec (motive := fun x x_1 =>
                (f : X ⟶ x) →
                  HEq f (𝟙 X) →
                    (Option.rec B (fun val => (F.obj { as := val }).left) X ⟶
                      Option.rec B (fun val => (F.obj { as := val }).left) x))
                (fun f h =>
                  (_ : WidePullbackShape.Hom.id X = f) ▸ 𝟙 (Option.rec B (fun val => (F.obj { as := val }).left) X))
                (_ : X = Y) f)
            h)
        (fun j h =>
          Eq.rec (motive := fun x x_1 =>
            (f : x ⟶ Y) →
              Y = none →
                HEq f (WidePullbackShape.Hom.term j) →
                  (Option.rec B (fun val => (F.obj { as := val }).left) x ⟶
                    Option.rec B (fun val => (F.obj { as := val }).left) Y))
            (fun f h =>
              Eq.rec (motive := fun x x_1 =>
                (f : some j ⟶ x) →
                  HEq f (WidePullbackShape.Hom.term j) →
                    ((F.obj { as := j }).left ⟶ Option.rec B (fun val => (F.obj { as := val }).left) x))
                (fun f h => (_ : WidePullbackShape.Hom.term j = f) ▸ (F.obj { as := j }).hom) (_ : none = Y) f)
            (_ : some j = X) f)
        f (_ : X = X) (_ : Y = Y) (_ : HEq f f)
[PROOFSTEP]
cases X
[GOAL]
case none
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X B : C
J : Type w
F : Discrete J ⥤ Over B
c : Cone F
Y : WidePullbackShape J
f : none ⟶ Y
⊢ 𝟙 c.pt.left ≫ Option.rec c.pt.hom (fun val => (NatTrans.app c.π { as := val }).left) Y =
    Option.rec c.pt.hom (fun val => (NatTrans.app c.π { as := val }).left) none ≫
      WidePullbackShape.Hom.rec (motive := fun a a_1 t =>
        none = a →
          Y = a_1 →
            HEq f t →
              (Option.rec B (fun val => (F.obj { as := val }).left) none ⟶
                Option.rec B (fun val => (F.obj { as := val }).left) Y))
        (fun X h =>
          Eq.rec (motive := fun x x_1 =>
            Y = x →
              HEq f (𝟙 x) →
                (Option.rec B (fun val => (F.obj { as := val }).left) none ⟶
                  Option.rec B (fun val => (F.obj { as := val }).left) Y))
            (fun h =>
              Eq.rec (motive := fun x x_1 =>
                (f : none ⟶ x) →
                  HEq f (𝟙 none) →
                    (Option.rec B (fun val => (F.obj { as := val }).left) none ⟶
                      Option.rec B (fun val => (F.obj { as := val }).left) x))
                (fun f h =>
                  (_ : WidePullbackShape.Hom.id none = f) ▸
                    𝟙 (Option.rec B (fun val => (F.obj { as := val }).left) none))
                (_ : none = Y) f)
            h)
        (fun j h =>
          Eq.rec (motive := fun x x_1 =>
            (f : x ⟶ Y) →
              Y = none →
                HEq f (WidePullbackShape.Hom.term j) →
                  (Option.rec B (fun val => (F.obj { as := val }).left) x ⟶
                    Option.rec B (fun val => (F.obj { as := val }).left) Y))
            (fun f h =>
              Eq.rec (motive := fun x x_1 =>
                (f : some j ⟶ x) →
                  HEq f (WidePullbackShape.Hom.term j) →
                    ((F.obj { as := j }).left ⟶ Option.rec B (fun val => (F.obj { as := val }).left) x))
                (fun f h => (_ : WidePullbackShape.Hom.term j = f) ▸ (F.obj { as := j }).hom) (_ : none = Y) f)
            (_ : some j = none) f)
        f (_ : none = none) (_ : Y = Y) (_ : HEq f f)
[PROOFSTEP]
cases Y
[GOAL]
case some
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X B : C
J : Type w
F : Discrete J ⥤ Over B
c : Cone F
Y : WidePullbackShape J
val✝ : J
f : some val✝ ⟶ Y
⊢ 𝟙 c.pt.left ≫ Option.rec c.pt.hom (fun val => (NatTrans.app c.π { as := val }).left) Y =
    Option.rec c.pt.hom (fun val => (NatTrans.app c.π { as := val }).left) (some val✝) ≫
      WidePullbackShape.Hom.rec (motive := fun a a_1 t =>
        some val✝ = a →
          Y = a_1 →
            HEq f t →
              (Option.rec B (fun val => (F.obj { as := val }).left) (some val✝) ⟶
                Option.rec B (fun val => (F.obj { as := val }).left) Y))
        (fun X h =>
          Eq.rec (motive := fun x x_1 =>
            Y = x →
              HEq f (𝟙 x) →
                (Option.rec B (fun val => (F.obj { as := val }).left) (some val✝) ⟶
                  Option.rec B (fun val => (F.obj { as := val }).left) Y))
            (fun h =>
              Eq.rec (motive := fun x x_1 =>
                (f : some val✝ ⟶ x) →
                  HEq f (𝟙 (some val✝)) →
                    (Option.rec B (fun val => (F.obj { as := val }).left) (some val✝) ⟶
                      Option.rec B (fun val => (F.obj { as := val }).left) x))
                (fun f h =>
                  (_ : WidePullbackShape.Hom.id (some val✝) = f) ▸
                    𝟙 (Option.rec B (fun val => (F.obj { as := val }).left) (some val✝)))
                (_ : some val✝ = Y) f)
            h)
        (fun j h =>
          Eq.rec (motive := fun x x_1 =>
            (f : x ⟶ Y) →
              Y = none →
                HEq f (WidePullbackShape.Hom.term j) →
                  (Option.rec B (fun val => (F.obj { as := val }).left) x ⟶
                    Option.rec B (fun val => (F.obj { as := val }).left) Y))
            (fun f h =>
              Eq.rec (motive := fun x x_1 =>
                (f : some j ⟶ x) →
                  HEq f (WidePullbackShape.Hom.term j) →
                    ((F.obj { as := j }).left ⟶ Option.rec B (fun val => (F.obj { as := val }).left) x))
                (fun f h => (_ : WidePullbackShape.Hom.term j = f) ▸ (F.obj { as := j }).hom) (_ : none = Y) f)
            (_ : some j = some val✝) f)
        f (_ : some val✝ = some val✝) (_ : Y = Y) (_ : HEq f f)
[PROOFSTEP]
cases Y
[GOAL]
case none.none
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X B : C
J : Type w
F : Discrete J ⥤ Over B
c : Cone F
f : none ⟶ none
⊢ 𝟙 c.pt.left ≫ Option.rec c.pt.hom (fun val => (NatTrans.app c.π { as := val }).left) none =
    Option.rec c.pt.hom (fun val => (NatTrans.app c.π { as := val }).left) none ≫
      WidePullbackShape.Hom.rec (motive := fun a a_1 t =>
        none = a →
          none = a_1 →
            HEq f t →
              (Option.rec B (fun val => (F.obj { as := val }).left) none ⟶
                Option.rec B (fun val => (F.obj { as := val }).left) none))
        (fun X h =>
          Eq.rec (motive := fun x x_1 =>
            none = x →
              HEq f (𝟙 x) →
                (Option.rec B (fun val => (F.obj { as := val }).left) none ⟶
                  Option.rec B (fun val => (F.obj { as := val }).left) none))
            (fun h =>
              Eq.rec (motive := fun x x_1 =>
                (f : none ⟶ x) →
                  HEq f (𝟙 none) →
                    (Option.rec B (fun val => (F.obj { as := val }).left) none ⟶
                      Option.rec B (fun val => (F.obj { as := val }).left) x))
                (fun f h =>
                  (_ : WidePullbackShape.Hom.id none = f) ▸
                    𝟙 (Option.rec B (fun val => (F.obj { as := val }).left) none))
                (_ : none = none) f)
            h)
        (fun j h =>
          Eq.rec (motive := fun x x_1 =>
            (f : x ⟶ none) →
              none = none →
                HEq f (WidePullbackShape.Hom.term j) →
                  (Option.rec B (fun val => (F.obj { as := val }).left) x ⟶
                    Option.rec B (fun val => (F.obj { as := val }).left) none))
            (fun f h =>
              Eq.rec (motive := fun x x_1 =>
                (f : some j ⟶ x) →
                  HEq f (WidePullbackShape.Hom.term j) →
                    ((F.obj { as := j }).left ⟶ Option.rec B (fun val => (F.obj { as := val }).left) x))
                (fun f h => (_ : WidePullbackShape.Hom.term j = f) ▸ (F.obj { as := j }).hom) (_ : none = none) f)
            (_ : some j = none) f)
        f (_ : none = none) (_ : none = none) (_ : HEq f f)
[PROOFSTEP]
cases f
[GOAL]
case none.some
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X B : C
J : Type w
F : Discrete J ⥤ Over B
c : Cone F
val✝ : J
f : none ⟶ some val✝
⊢ 𝟙 c.pt.left ≫ Option.rec c.pt.hom (fun val => (NatTrans.app c.π { as := val }).left) (some val✝) =
    Option.rec c.pt.hom (fun val => (NatTrans.app c.π { as := val }).left) none ≫
      WidePullbackShape.Hom.rec (motive := fun a a_1 t =>
        none = a →
          some val✝ = a_1 →
            HEq f t →
              (Option.rec B (fun val => (F.obj { as := val }).left) none ⟶
                Option.rec B (fun val => (F.obj { as := val }).left) (some val✝)))
        (fun X h =>
          Eq.rec (motive := fun x x_1 =>
            some val✝ = x →
              HEq f (𝟙 x) →
                (Option.rec B (fun val => (F.obj { as := val }).left) none ⟶
                  Option.rec B (fun val => (F.obj { as := val }).left) (some val✝)))
            (fun h =>
              Eq.rec (motive := fun x x_1 =>
                (f : none ⟶ x) →
                  HEq f (𝟙 none) →
                    (Option.rec B (fun val => (F.obj { as := val }).left) none ⟶
                      Option.rec B (fun val => (F.obj { as := val }).left) x))
                (fun f h =>
                  (_ : WidePullbackShape.Hom.id none = f) ▸
                    𝟙 (Option.rec B (fun val => (F.obj { as := val }).left) none))
                (_ : none = some val✝) f)
            h)
        (fun j h =>
          Eq.rec (motive := fun x x_1 =>
            (f : x ⟶ some val✝) →
              some val✝ = none →
                HEq f (WidePullbackShape.Hom.term j) →
                  (Option.rec B (fun val => (F.obj { as := val }).left) x ⟶
                    Option.rec B (fun val => (F.obj { as := val }).left) (some val✝)))
            (fun f h =>
              Eq.rec (motive := fun x x_1 =>
                (f : some j ⟶ x) →
                  HEq f (WidePullbackShape.Hom.term j) →
                    ((F.obj { as := j }).left ⟶ Option.rec B (fun val => (F.obj { as := val }).left) x))
                (fun f h => (_ : WidePullbackShape.Hom.term j = f) ▸ (F.obj { as := j }).hom) (_ : none = some val✝) f)
            (_ : some j = none) f)
        f (_ : none = none) (_ : some val✝ = some val✝) (_ : HEq f f)
[PROOFSTEP]
cases f
[GOAL]
case some.none
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X B : C
J : Type w
F : Discrete J ⥤ Over B
c : Cone F
val✝ : J
f : some val✝ ⟶ none
⊢ 𝟙 c.pt.left ≫ Option.rec c.pt.hom (fun val => (NatTrans.app c.π { as := val }).left) none =
    Option.rec c.pt.hom (fun val => (NatTrans.app c.π { as := val }).left) (some val✝) ≫
      WidePullbackShape.Hom.rec (motive := fun a a_1 t =>
        some val✝ = a →
          none = a_1 →
            HEq f t →
              (Option.rec B (fun val => (F.obj { as := val }).left) (some val✝) ⟶
                Option.rec B (fun val => (F.obj { as := val }).left) none))
        (fun X h =>
          Eq.rec (motive := fun x x_1 =>
            none = x →
              HEq f (𝟙 x) →
                (Option.rec B (fun val => (F.obj { as := val }).left) (some val✝) ⟶
                  Option.rec B (fun val => (F.obj { as := val }).left) none))
            (fun h =>
              Eq.rec (motive := fun x x_1 =>
                (f : some val✝ ⟶ x) →
                  HEq f (𝟙 (some val✝)) →
                    (Option.rec B (fun val => (F.obj { as := val }).left) (some val✝) ⟶
                      Option.rec B (fun val => (F.obj { as := val }).left) x))
                (fun f h =>
                  (_ : WidePullbackShape.Hom.id (some val✝) = f) ▸
                    𝟙 (Option.rec B (fun val => (F.obj { as := val }).left) (some val✝)))
                (_ : some val✝ = none) f)
            h)
        (fun j h =>
          Eq.rec (motive := fun x x_1 =>
            (f : x ⟶ none) →
              none = none →
                HEq f (WidePullbackShape.Hom.term j) →
                  (Option.rec B (fun val => (F.obj { as := val }).left) x ⟶
                    Option.rec B (fun val => (F.obj { as := val }).left) none))
            (fun f h =>
              Eq.rec (motive := fun x x_1 =>
                (f : some j ⟶ x) →
                  HEq f (WidePullbackShape.Hom.term j) →
                    ((F.obj { as := j }).left ⟶ Option.rec B (fun val => (F.obj { as := val }).left) x))
                (fun f h => (_ : WidePullbackShape.Hom.term j = f) ▸ (F.obj { as := j }).hom) (_ : none = none) f)
            (_ : some j = some val✝) f)
        f (_ : some val✝ = some val✝) (_ : none = none) (_ : HEq f f)
[PROOFSTEP]
cases f
[GOAL]
case some.some
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X B : C
J : Type w
F : Discrete J ⥤ Over B
c : Cone F
val✝¹ val✝ : J
f : some val✝¹ ⟶ some val✝
⊢ 𝟙 c.pt.left ≫ Option.rec c.pt.hom (fun val => (NatTrans.app c.π { as := val }).left) (some val✝) =
    Option.rec c.pt.hom (fun val => (NatTrans.app c.π { as := val }).left) (some val✝¹) ≫
      WidePullbackShape.Hom.rec (motive := fun a a_1 t =>
        some val✝¹ = a →
          some val✝ = a_1 →
            HEq f t →
              (Option.rec B (fun val => (F.obj { as := val }).left) (some val✝¹) ⟶
                Option.rec B (fun val => (F.obj { as := val }).left) (some val✝)))
        (fun X h =>
          Eq.rec (motive := fun x x_1 =>
            some val✝ = x →
              HEq f (𝟙 x) →
                (Option.rec B (fun val => (F.obj { as := val }).left) (some val✝¹) ⟶
                  Option.rec B (fun val => (F.obj { as := val }).left) (some val✝)))
            (fun h =>
              Eq.rec (motive := fun x x_1 =>
                (f : some val✝¹ ⟶ x) →
                  HEq f (𝟙 (some val✝¹)) →
                    (Option.rec B (fun val => (F.obj { as := val }).left) (some val✝¹) ⟶
                      Option.rec B (fun val => (F.obj { as := val }).left) x))
                (fun f h =>
                  (_ : WidePullbackShape.Hom.id (some val✝¹) = f) ▸
                    𝟙 (Option.rec B (fun val => (F.obj { as := val }).left) (some val✝¹)))
                (_ : some val✝¹ = some val✝) f)
            h)
        (fun j h =>
          Eq.rec (motive := fun x x_1 =>
            (f : x ⟶ some val✝) →
              some val✝ = none →
                HEq f (WidePullbackShape.Hom.term j) →
                  (Option.rec B (fun val => (F.obj { as := val }).left) x ⟶
                    Option.rec B (fun val => (F.obj { as := val }).left) (some val✝)))
            (fun f h =>
              Eq.rec (motive := fun x x_1 =>
                (f : some j ⟶ x) →
                  HEq f (WidePullbackShape.Hom.term j) →
                    ((F.obj { as := j }).left ⟶ Option.rec B (fun val => (F.obj { as := val }).left) x))
                (fun f h => (_ : WidePullbackShape.Hom.term j = f) ▸ (F.obj { as := j }).hom) (_ : none = some val✝) f)
            (_ : some j = some val✝¹) f)
        f (_ : some val✝¹ = some val✝¹) (_ : some val✝ = some val✝) (_ : HEq f f)
[PROOFSTEP]
cases f
[GOAL]
case none.none.id
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X B : C
J : Type w
F : Discrete J ⥤ Over B
c : Cone F
⊢ 𝟙 c.pt.left ≫ Option.rec c.pt.hom (fun val => (NatTrans.app c.π { as := val }).left) none =
    Option.rec c.pt.hom (fun val => (NatTrans.app c.π { as := val }).left) none ≫
      WidePullbackShape.Hom.rec (motive := fun a a_1 t =>
        none = a →
          none = a_1 →
            HEq (WidePullbackShape.Hom.id none) t →
              (Option.rec B (fun val => (F.obj { as := val }).left) none ⟶
                Option.rec B (fun val => (F.obj { as := val }).left) none))
        (fun X h =>
          Eq.rec (motive := fun x x_1 =>
            none = x →
              HEq (WidePullbackShape.Hom.id none) (𝟙 x) →
                (Option.rec B (fun val => (F.obj { as := val }).left) none ⟶
                  Option.rec B (fun val => (F.obj { as := val }).left) none))
            (fun h =>
              Eq.rec (motive := fun x x_1 =>
                (f : none ⟶ x) →
                  HEq f (𝟙 none) →
                    (Option.rec B (fun val => (F.obj { as := val }).left) none ⟶
                      Option.rec B (fun val => (F.obj { as := val }).left) x))
                (fun f h =>
                  (_ : WidePullbackShape.Hom.id none = f) ▸
                    𝟙 (Option.rec B (fun val => (F.obj { as := val }).left) none))
                (_ : none = none) (WidePullbackShape.Hom.id none))
            h)
        (fun j h =>
          Eq.rec (motive := fun x x_1 =>
            (f : x ⟶ none) →
              none = none →
                HEq f (WidePullbackShape.Hom.term j) →
                  (Option.rec B (fun val => (F.obj { as := val }).left) x ⟶
                    Option.rec B (fun val => (F.obj { as := val }).left) none))
            (fun f h =>
              Eq.rec (motive := fun x x_1 =>
                (f : some j ⟶ x) →
                  HEq f (WidePullbackShape.Hom.term j) →
                    ((F.obj { as := j }).left ⟶ Option.rec B (fun val => (F.obj { as := val }).left) x))
                (fun f h => (_ : WidePullbackShape.Hom.term j = f) ▸ (F.obj { as := j }).hom) (_ : none = none) f)
            (_ : some j = none) (WidePullbackShape.Hom.id none))
        (WidePullbackShape.Hom.id none) (_ : none = none) (_ : none = none)
        (_ : HEq (WidePullbackShape.Hom.id none) (WidePullbackShape.Hom.id none))
[PROOFSTEP]
rw [Category.id_comp, Category.comp_id]
[GOAL]
case some.none.term
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X B : C
J : Type w
F : Discrete J ⥤ Over B
c : Cone F
val✝ : J
⊢ 𝟙 c.pt.left ≫ Option.rec c.pt.hom (fun val => (NatTrans.app c.π { as := val }).left) none =
    Option.rec c.pt.hom (fun val => (NatTrans.app c.π { as := val }).left) (some val✝) ≫
      WidePullbackShape.Hom.rec (motive := fun a a_1 t =>
        some val✝ = a →
          none = a_1 →
            HEq (WidePullbackShape.Hom.term val✝) t →
              (Option.rec B (fun val => (F.obj { as := val }).left) (some val✝) ⟶
                Option.rec B (fun val => (F.obj { as := val }).left) none))
        (fun X h =>
          Eq.rec (motive := fun x x_1 =>
            none = x →
              HEq (WidePullbackShape.Hom.term val✝) (𝟙 x) →
                (Option.rec B (fun val => (F.obj { as := val }).left) (some val✝) ⟶
                  Option.rec B (fun val => (F.obj { as := val }).left) none))
            (fun h =>
              Eq.rec (motive := fun x x_1 =>
                (f : some val✝ ⟶ x) →
                  HEq f (𝟙 (some val✝)) →
                    (Option.rec B (fun val => (F.obj { as := val }).left) (some val✝) ⟶
                      Option.rec B (fun val => (F.obj { as := val }).left) x))
                (fun f h =>
                  (_ : WidePullbackShape.Hom.id (some val✝) = f) ▸
                    𝟙 (Option.rec B (fun val => (F.obj { as := val }).left) (some val✝)))
                (_ : some val✝ = none) (WidePullbackShape.Hom.term val✝))
            h)
        (fun j h =>
          Eq.rec (motive := fun x x_1 =>
            (f : x ⟶ none) →
              none = none →
                HEq f (WidePullbackShape.Hom.term j) →
                  (Option.rec B (fun val => (F.obj { as := val }).left) x ⟶
                    Option.rec B (fun val => (F.obj { as := val }).left) none))
            (fun f h =>
              Eq.rec (motive := fun x x_1 =>
                (f : some j ⟶ x) →
                  HEq f (WidePullbackShape.Hom.term j) →
                    ((F.obj { as := j }).left ⟶ Option.rec B (fun val => (F.obj { as := val }).left) x))
                (fun f h => (_ : WidePullbackShape.Hom.term j = f) ▸ (F.obj { as := j }).hom) (_ : none = none) f)
            (_ : some j = some val✝) (WidePullbackShape.Hom.term val✝))
        (WidePullbackShape.Hom.term val✝) (_ : some val✝ = some val✝) (_ : none = none)
        (_ : HEq (WidePullbackShape.Hom.term val✝) (WidePullbackShape.Hom.term val✝))
[PROOFSTEP]
rw [Over.w, Category.id_comp]
[GOAL]
case some.some.id
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X B : C
J : Type w
F : Discrete J ⥤ Over B
c : Cone F
val✝ : J
⊢ 𝟙 c.pt.left ≫ Option.rec c.pt.hom (fun val => (NatTrans.app c.π { as := val }).left) (some val✝) =
    Option.rec c.pt.hom (fun val => (NatTrans.app c.π { as := val }).left) (some val✝) ≫
      WidePullbackShape.Hom.rec (motive := fun a a_1 t =>
        some val✝ = a →
          some val✝ = a_1 →
            HEq (WidePullbackShape.Hom.id (some val✝)) t →
              (Option.rec B (fun val => (F.obj { as := val }).left) (some val✝) ⟶
                Option.rec B (fun val => (F.obj { as := val }).left) (some val✝)))
        (fun X h =>
          Eq.rec (motive := fun x x_1 =>
            some val✝ = x →
              HEq (WidePullbackShape.Hom.id (some val✝)) (𝟙 x) →
                (Option.rec B (fun val => (F.obj { as := val }).left) (some val✝) ⟶
                  Option.rec B (fun val => (F.obj { as := val }).left) (some val✝)))
            (fun h =>
              Eq.rec (motive := fun x x_1 =>
                (f : some val✝ ⟶ x) →
                  HEq f (𝟙 (some val✝)) →
                    (Option.rec B (fun val => (F.obj { as := val }).left) (some val✝) ⟶
                      Option.rec B (fun val => (F.obj { as := val }).left) x))
                (fun f h =>
                  (_ : WidePullbackShape.Hom.id (some val✝) = f) ▸
                    𝟙 (Option.rec B (fun val => (F.obj { as := val }).left) (some val✝)))
                (_ : some val✝ = some val✝) (WidePullbackShape.Hom.id (some val✝)))
            h)
        (fun j h =>
          Eq.rec (motive := fun x x_1 =>
            (f : x ⟶ some val✝) →
              some val✝ = none →
                HEq f (WidePullbackShape.Hom.term j) →
                  (Option.rec B (fun val => (F.obj { as := val }).left) x ⟶
                    Option.rec B (fun val => (F.obj { as := val }).left) (some val✝)))
            (fun f h =>
              Eq.rec (motive := fun x x_1 =>
                (f : some j ⟶ x) →
                  HEq f (WidePullbackShape.Hom.term j) →
                    ((F.obj { as := j }).left ⟶ Option.rec B (fun val => (F.obj { as := val }).left) x))
                (fun f h => (_ : WidePullbackShape.Hom.term j = f) ▸ (F.obj { as := j }).hom) (_ : none = some val✝) f)
            (_ : some j = some val✝) (WidePullbackShape.Hom.id (some val✝)))
        (WidePullbackShape.Hom.id (some val✝)) (_ : some val✝ = some val✝) (_ : some val✝ = some val✝)
        (_ : HEq (WidePullbackShape.Hom.id (some val✝)) (WidePullbackShape.Hom.id (some val✝)))
[PROOFSTEP]
rw [Category.id_comp, Category.comp_id]
[GOAL]
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X B : C
J : Type w
F : Discrete J ⥤ Over B
X✝ Y✝ : Cone F
f : X✝ ⟶ Y✝
j : WidePullbackShape J
⊢ f.Hom.left ≫ NatTrans.app (conesEquivInverseObj B F Y✝).π j = NatTrans.app (conesEquivInverseObj B F X✝).π j
[PROOFSTEP]
cases' j with j
[GOAL]
case none
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X B : C
J : Type w
F : Discrete J ⥤ Over B
X✝ Y✝ : Cone F
f : X✝ ⟶ Y✝
⊢ f.Hom.left ≫ NatTrans.app (conesEquivInverseObj B F Y✝).π none = NatTrans.app (conesEquivInverseObj B F X✝).π none
[PROOFSTEP]
simp
[GOAL]
case some
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X B : C
J : Type w
F : Discrete J ⥤ Over B
X✝ Y✝ : Cone F
f : X✝ ⟶ Y✝
j : J
⊢ f.Hom.left ≫ NatTrans.app (conesEquivInverseObj B F Y✝).π (some j) =
    NatTrans.app (conesEquivInverseObj B F X✝).π (some j)
[PROOFSTEP]
dsimp
[GOAL]
case some
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X B : C
J : Type w
F : Discrete J ⥤ Over B
X✝ Y✝ : Cone F
f : X✝ ⟶ Y✝
j : J
⊢ f.Hom.left ≫ (NatTrans.app Y✝.π { as := j }).left = (NatTrans.app X✝.π { as := j }).left
[PROOFSTEP]
rw [← f.w ⟨j⟩]
[GOAL]
case some
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X B : C
J : Type w
F : Discrete J ⥤ Over B
X✝ Y✝ : Cone F
f : X✝ ⟶ Y✝
j : J
⊢ f.Hom.left ≫ (NatTrans.app Y✝.π { as := j }).left = (f.Hom ≫ NatTrans.app Y✝.π { as := j }).left
[PROOFSTEP]
rfl
[GOAL]
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X✝ B : C
J : Type w
F : Discrete J ⥤ Over B
c : Cone (widePullbackDiagramOfDiagramOver B F)
x✝² x✝¹ : Discrete J
X Y : J
x✝ : { as := X } ⟶ { as := Y }
f : { as := X }.as = { as := Y }.as
⊢ ((Functor.const (Discrete J)).obj (mk (NatTrans.app c.π none))).map { down := { down := f } } ≫
      (fun x =>
          match x with
          | { as := j } => homMk (NatTrans.app c.π (some j)))
        { as := Y } =
    (fun x =>
          match x with
          | { as := j } => homMk (NatTrans.app c.π (some j)))
        { as := X } ≫
      F.map { down := { down := f } }
[PROOFSTEP]
dsimp at f ⊢
[GOAL]
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X✝ B : C
J : Type w
F : Discrete J ⥤ Over B
c : Cone (widePullbackDiagramOfDiagramOver B F)
x✝² x✝¹ : Discrete J
X Y : J
x✝ : { as := X } ⟶ { as := Y }
f : X = Y
⊢ 𝟙 (mk (NatTrans.app c.π none)) ≫ homMk (NatTrans.app c.π (some Y)) =
    homMk (NatTrans.app c.π (some X)) ≫ F.map { down := { down := f } }
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X B : C
F : Discrete J ⥤ Over B
x✝ : Cone (widePullbackDiagramOfDiagramOver B F)
⊢ ∀ (j : WidePullbackShape J),
    NatTrans.app ((𝟭 (Cone (widePullbackDiagramOfDiagramOver B F))).obj x✝).π j =
      (Iso.mk (𝟙 ((𝟭 (Cone (widePullbackDiagramOfDiagramOver B F))).obj x✝).pt)
            (𝟙 ((conesEquivFunctor B F ⋙ conesEquivInverse B F).obj x✝).pt)).hom ≫
        NatTrans.app ((conesEquivFunctor B F ⋙ conesEquivInverse B F).obj x✝).π j
[PROOFSTEP]
rintro (j | j)
[GOAL]
case none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X B : C
F : Discrete J ⥤ Over B
x✝ : Cone (widePullbackDiagramOfDiagramOver B F)
⊢ NatTrans.app ((𝟭 (Cone (widePullbackDiagramOfDiagramOver B F))).obj x✝).π none =
    (Iso.mk (𝟙 ((𝟭 (Cone (widePullbackDiagramOfDiagramOver B F))).obj x✝).pt)
          (𝟙 ((conesEquivFunctor B F ⋙ conesEquivInverse B F).obj x✝).pt)).hom ≫
      NatTrans.app ((conesEquivFunctor B F ⋙ conesEquivInverse B F).obj x✝).π none
[PROOFSTEP]
aesop_cat
[GOAL]
case some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X B : C
F : Discrete J ⥤ Over B
x✝ : Cone (widePullbackDiagramOfDiagramOver B F)
j : J
⊢ NatTrans.app ((𝟭 (Cone (widePullbackDiagramOfDiagramOver B F))).obj x✝).π (some j) =
    (Iso.mk (𝟙 ((𝟭 (Cone (widePullbackDiagramOfDiagramOver B F))).obj x✝).pt)
          (𝟙 ((conesEquivFunctor B F ⋙ conesEquivInverse B F).obj x✝).pt)).hom ≫
      NatTrans.app ((conesEquivFunctor B F ⋙ conesEquivInverse B F).obj x✝).π (some j)
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X B : C
F : Discrete PEmpty ⥤ Over B
s : Cone F
m : s.pt ⟶ { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.pt
x✝ :
  ∀ (j : Discrete PEmpty),
    m ≫ NatTrans.app { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.π j = NatTrans.app s.π j
⊢ m = (fun s => homMk s.pt.hom) s
[PROOFSTEP]
simp only
[GOAL]
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X B : C
F : Discrete PEmpty ⥤ Over B
s : Cone F
m : s.pt ⟶ { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.pt
x✝ :
  ∀ (j : Discrete PEmpty),
    m ≫ NatTrans.app { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.π j = NatTrans.app s.π j
⊢ m = homMk s.pt.hom
[PROOFSTEP]
ext
[GOAL]
case h
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X B : C
F : Discrete PEmpty ⥤ Over B
s : Cone F
m : s.pt ⟶ { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.pt
x✝ :
  ∀ (j : Discrete PEmpty),
    m ≫ NatTrans.app { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.π j = NatTrans.app s.π j
⊢ m.left = (homMk s.pt.hom).left
[PROOFSTEP]
rw [Over.homMk_left _]
[GOAL]
case h
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X B : C
F : Discrete PEmpty ⥤ Over B
s : Cone F
m : s.pt ⟶ { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.pt
x✝ :
  ∀ (j : Discrete PEmpty),
    m ≫ NatTrans.app { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.π j = NatTrans.app s.π j
⊢ m.left = s.pt.hom
[PROOFSTEP]
have := m.w
[GOAL]
case h
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X B : C
F : Discrete PEmpty ⥤ Over B
s : Cone F
m : s.pt ⟶ { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.pt
x✝ :
  ∀ (j : Discrete PEmpty),
    m ≫ NatTrans.app { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.π j = NatTrans.app s.π j
this :
  (𝟭 C).map m.left ≫ { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.pt.hom =
    s.pt.hom ≫ (Functor.fromPUnit B).map m.right
⊢ m.left = s.pt.hom
[PROOFSTEP]
dsimp at this
[GOAL]
case h
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X B : C
F : Discrete PEmpty ⥤ Over B
s : Cone F
m : s.pt ⟶ { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.pt
x✝ :
  ∀ (j : Discrete PEmpty),
    m ≫ NatTrans.app { pt := mk (𝟙 B), π := NatTrans.mk fun p => PEmpty.elim p.as }.π j = NatTrans.app s.π j
this : m.left ≫ 𝟙 B = s.pt.hom ≫ 𝟙 B
⊢ m.left = s.pt.hom
[PROOFSTEP]
rwa [Category.comp_id, Category.comp_id] at this


[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A A₀ A₁ A₂ : Algebra F
f : A₀ ⟶ A₁
g : A₁ ⟶ A₂
h : A₀.a ≅ A₁.a
w : autoParam (F.map h.hom ≫ A₁.str = A₀.str ≫ h.hom) _auto✝
⊢ F.map h.inv ≫ A₀.str = A₁.str ≫ h.inv
[PROOFSTEP]
rw [h.eq_comp_inv, Category.assoc, ← w, ← Functor.map_comp_assoc]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A A₀ A₁ A₂ : Algebra F
f : A₀ ⟶ A₁
g : A₁ ⟶ A₂
h : A₀.a ≅ A₁.a
w : autoParam (F.map h.hom ≫ A₁.str = A₀.str ≫ h.hom) _auto✝
⊢ F.map (h.inv ≫ h.hom) ≫ A₁.str = A₁.str
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ C
A A₀ A₁ A₂ : Algebra F
f✝ : A₀ ⟶ A₁
g : A₁ ⟶ A₂
f : A₀ ⟶ A₁
inst✝ : IsIso f.f
⊢ F.map (inv f.f) ≫ A₀.str = A₁.str ≫ inv f.f
[PROOFSTEP]
rw [IsIso.eq_comp_inv f.1, Category.assoc, ← f.h]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ C
A A₀ A₁ A₂ : Algebra F
f✝ : A₀ ⟶ A₁
g : A₁ ⟶ A₂
f : A₀ ⟶ A₁
inst✝ : IsIso f.f
⊢ F.map (inv f.f) ≫ F.map f.f ≫ A₁.str = A₁.str
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ C
A A₀ A₁ A₂ : Algebra F
f✝ : A₀ ⟶ A₁
g : A₁ ⟶ A₂
f : A₀ ⟶ A₁
inst✝ : IsIso f.f
⊢ f ≫ Hom.mk (inv f.f) = 𝟙 A₀
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ C
A A₀ A₁ A₂ : Algebra F
f✝ : A₀ ⟶ A₁
g : A₁ ⟶ A₂
f : A₀ ⟶ A₁
inst✝ : IsIso f.f
⊢ Hom.mk (inv f.f) ≫ f = 𝟙 A₁
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ C
A A₀ A₁ A₂ : Algebra F✝
f : A₀ ⟶ A₁
g : A₁ ⟶ A₂
F G : C ⥤ C
α : F ≅ G
⊢ 𝟙 F = α.hom ≫ α.inv
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ C
A A₀ A₁ A₂ : Algebra F✝
f : A₀ ⟶ A₁
g : A₁ ⟶ A₂
F G : C ⥤ C
α : F ≅ G
⊢ α.inv ≫ α.hom = 𝟙 G
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A A₀ A₁ A₂ : Algebra F
f : A₀ ⟶ A₁
g : A₁ ⟶ A₂
h : Limits.IsInitial A
⊢ F.map (strInv h ≫ A.str) ≫ A.str = A.str ≫ strInv h ≫ A.str
[PROOFSTEP]
rw [← Category.assoc, F.map_comp, strInv, ← Hom.h]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A A₀ A₁ A₂ : Algebra F
f : A₀ ⟶ A₁
g : A₁ ⟶ A₂
h : Limits.IsInitial A
⊢ A.str ≫ strInv h = 𝟙 (F.obj A.a)
[PROOFSTEP]
rw [strInv, ← (h.to ⟨F.obj A.1, F.map A.str⟩).h, ← F.map_id, ← F.map_comp]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A A₀ A₁ A₂ : Algebra F
f : A₀ ⟶ A₁
g : A₁ ⟶ A₂
h : Limits.IsInitial A
⊢ F.map ((Limits.IsInitial.to h { a := F.obj A.a, str := F.map A.str }).f ≫ A.str) = F.map (𝟙 A.a)
[PROOFSTEP]
congr
[GOAL]
case e_a
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A A₀ A₁ A₂ : Algebra F
f : A₀ ⟶ A₁
g : A₁ ⟶ A₂
h : Limits.IsInitial A
⊢ (Limits.IsInitial.to h { a := F.obj A.a, str := F.map A.str }).f ≫ A.str = 𝟙 A.a
[PROOFSTEP]
exact left_inv h
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
V V₀ V₁ V₂ : Coalgebra F
f : V₀ ⟶ V₁
g : V₁ ⟶ V₂
h : V₀.V ≅ V₁.V
w : autoParam (V₀.str ≫ F.map h.hom = h.hom ≫ V₁.str) _auto✝
⊢ V₁.str ≫ F.map h.inv = h.inv ≫ V₀.str
[PROOFSTEP]
rw [h.eq_inv_comp, ← Category.assoc, ← w, Category.assoc, ← F.map_comp]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
V V₀ V₁ V₂ : Coalgebra F
f : V₀ ⟶ V₁
g : V₁ ⟶ V₂
h : V₀.V ≅ V₁.V
w : autoParam (V₀.str ≫ F.map h.hom = h.hom ≫ V₁.str) _auto✝
⊢ V₀.str ≫ F.map (h.hom ≫ h.inv) = V₀.str
[PROOFSTEP]
simp only [Iso.hom_inv_id, Functor.map_id, Category.comp_id]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ C
V V₀ V₁ V₂ : Coalgebra F
f✝ : V₀ ⟶ V₁
g : V₁ ⟶ V₂
f : V₀ ⟶ V₁
inst✝ : IsIso f.f
⊢ V₁.str ≫ F.map (inv f.f) = inv f.f ≫ V₀.str
[PROOFSTEP]
rw [IsIso.eq_inv_comp f.1, ← Category.assoc, ← f.h, Category.assoc]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ C
V V₀ V₁ V₂ : Coalgebra F
f✝ : V₀ ⟶ V₁
g : V₁ ⟶ V₂
f : V₀ ⟶ V₁
inst✝ : IsIso f.f
⊢ V₀.str ≫ F.map f.f ≫ F.map (inv f.f) = V₀.str
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ C
V V₀ V₁ V₂ : Coalgebra F
f✝ : V₀ ⟶ V₁
g : V₁ ⟶ V₂
f : V₀ ⟶ V₁
inst✝ : IsIso f.f
⊢ f ≫ Hom.mk (inv f.f) = 𝟙 V₀
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ C
V V₀ V₁ V₂ : Coalgebra F
f✝ : V₀ ⟶ V₁
g : V₁ ⟶ V₂
f : V₀ ⟶ V₁
inst✝ : IsIso f.f
⊢ Hom.mk (inv f.f) ≫ f = 𝟙 V₁
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ C
V V₀ V₁ V₂ : Coalgebra F✝
f✝ : V₀ ⟶ V₁
g : V₁ ⟶ V₂
F G : C ⥤ C
α : F ⟶ G
X✝ Y✝ : Coalgebra F
f : X✝ ⟶ Y✝
⊢ ((fun V => { V := V.V, str := V.str ≫ NatTrans.app α V.V }) X✝).str ≫ G.map f.f =
    f.f ≫ ((fun V => { V := V.V, str := V.str ≫ NatTrans.app α V.V }) Y✝).str
[PROOFSTEP]
rw [Category.assoc, ← α.naturality, ← Category.assoc, f.h, Category.assoc]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ C
V V₀ V₁ V₂ : Coalgebra F✝
f : V₀ ⟶ V₁
g : V₁ ⟶ V₂
F G : C ⥤ C
α : F ≅ G
⊢ 𝟙 F = α.hom ≫ α.inv
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ C
V V₀ V₁ V₂ : Coalgebra F✝
f : V₀ ⟶ V₁
g : V₁ ⟶ V₂
F G : C ⥤ C
α : F ≅ G
⊢ α.inv ≫ α.hom = 𝟙 G
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
A₁ A₂ : Algebra F
f : A₁ ⟶ A₂
⊢ ↑(Adjunction.homEquiv adj A₁.a A₁.a) A₁.str ≫ G.map f.f = f.f ≫ ↑(Adjunction.homEquiv adj A₂.a A₂.a) A₂.str
[PROOFSTEP]
rw [← Adjunction.homEquiv_naturality_right, ← Adjunction.homEquiv_naturality_left, f.h]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
V₁ V₂ : Coalgebra G
f : V₁ ⟶ V₂
⊢ F.map f.f ≫ ↑(Adjunction.homEquiv adj V₂.V V₂.V).symm V₂.str = ↑(Adjunction.homEquiv adj V₁.V V₁.V).symm V₁.str ≫ f.f
[PROOFSTEP]
rw [← Adjunction.homEquiv_naturality_left_symm, ← Adjunction.homEquiv_naturality_right_symm, f.h]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
A : Algebra F
⊢ F.map (𝟙 A.a) ≫ ((Algebra.toCoalgebraOf adj ⋙ Coalgebra.toAlgebraOf adj).obj A).str =
    ((𝟭 (Algebra F)).obj A).str ≫ 𝟙 A.a
[PROOFSTEP]
erw [F.map_id, Category.id_comp, Category.comp_id]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
A : Algebra F
⊢ ((Algebra.toCoalgebraOf adj ⋙ Coalgebra.toAlgebraOf adj).obj A).str = ((𝟭 (Algebra F)).obj A).str
[PROOFSTEP]
apply (adj.homEquiv _ _).left_inv A.str
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
A : Algebra F
⊢ F.map (𝟙 A.a) ≫ ((𝟭 (Algebra F)).obj A).str =
    ((Algebra.toCoalgebraOf adj ⋙ Coalgebra.toAlgebraOf adj).obj A).str ≫ 𝟙 A.a
[PROOFSTEP]
erw [F.map_id, Category.id_comp, Category.comp_id]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
A : Algebra F
⊢ ((𝟭 (Algebra F)).obj A).str = ((Algebra.toCoalgebraOf adj ⋙ Coalgebra.toAlgebraOf adj).obj A).str
[PROOFSTEP]
apply ((adj.homEquiv _ _).left_inv A.str).symm
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
A₁ A₂ : Algebra F
f : A₁ ⟶ A₂
⊢ (Algebra.toCoalgebraOf adj ⋙ Coalgebra.toAlgebraOf adj).map f ≫ (fun A => Algebra.Hom.mk (𝟙 A.a)) A₂ =
    (fun A => Algebra.Hom.mk (𝟙 A.a)) A₁ ≫ (𝟭 (Algebra F)).map f
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
A₁ A₂ : Algebra F
f : A₁ ⟶ A₂
⊢ autoParam
    (((Algebra.toCoalgebraOf adj ⋙ Coalgebra.toAlgebraOf adj).map f ≫ (fun A => Algebra.Hom.mk (𝟙 A.a)) A₂).f =
      ((fun A => Algebra.Hom.mk (𝟙 A.a)) A₁ ≫ (𝟭 (Algebra F)).map f).f)
    _auto✝
[PROOFSTEP]
dsimp
[GOAL]
case w
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
A₁ A₂ : Algebra F
f : A₁ ⟶ A₂
⊢ autoParam (((Coalgebra.toAlgebraOf adj).map ((Algebra.toCoalgebraOf adj).map f)).f ≫ 𝟙 A₂.a = 𝟙 A₁.a ≫ f.f) _auto✝
[PROOFSTEP]
erw [Category.comp_id, Category.id_comp]
[GOAL]
case w
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
A₁ A₂ : Algebra F
f : A₁ ⟶ A₂
⊢ autoParam (((Coalgebra.toAlgebraOf adj).map ((Algebra.toCoalgebraOf adj).map f)).f = f.f) _auto✝
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
V : Coalgebra G
⊢ ((Coalgebra.toAlgebraOf adj ⋙ Algebra.toCoalgebraOf adj).obj V).str ≫ G.map (𝟙 V.V) =
    𝟙 V.V ≫ ((𝟭 (Coalgebra G)).obj V).str
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
V : Coalgebra G
⊢ ((Algebra.toCoalgebraOf adj).obj ((Coalgebra.toAlgebraOf adj).obj V)).str ≫ G.map (𝟙 V.V) = 𝟙 V.V ≫ V.str
[PROOFSTEP]
erw [G.map_id, Category.id_comp, Category.comp_id]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
V : Coalgebra G
⊢ ((Algebra.toCoalgebraOf adj).obj ((Coalgebra.toAlgebraOf adj).obj V)).str = V.str
[PROOFSTEP]
apply (adj.homEquiv _ _).right_inv V.str
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
V₁ V₂ : Coalgebra G
f : V₁ ⟶ V₂
⊢ (Coalgebra.toAlgebraOf adj ⋙ Algebra.toCoalgebraOf adj).map f ≫ (fun V => Coalgebra.Hom.mk (𝟙 V.V)) V₂ =
    (fun V => Coalgebra.Hom.mk (𝟙 V.V)) V₁ ≫ (𝟭 (Coalgebra G)).map f
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
V₁ V₂ : Coalgebra G
f : V₁ ⟶ V₂
⊢ autoParam
    (((Coalgebra.toAlgebraOf adj ⋙ Algebra.toCoalgebraOf adj).map f ≫ (fun V => Coalgebra.Hom.mk (𝟙 V.V)) V₂).f =
      ((fun V => Coalgebra.Hom.mk (𝟙 V.V)) V₁ ≫ (𝟭 (Coalgebra G)).map f).f)
    _auto✝
[PROOFSTEP]
dsimp
[GOAL]
case w
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
V₁ V₂ : Coalgebra G
f : V₁ ⟶ V₂
⊢ autoParam (((Algebra.toCoalgebraOf adj).map ((Coalgebra.toAlgebraOf adj).map f)).f ≫ 𝟙 V₂.V = 𝟙 V₁.V ≫ f.f) _auto✝
[PROOFSTEP]
erw [Category.comp_id, Category.id_comp]
[GOAL]
case w
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
V₁ V₂ : Coalgebra G
f : V₁ ⟶ V₂
⊢ autoParam (((Algebra.toCoalgebraOf adj).map ((Coalgebra.toAlgebraOf adj).map f)).f = f.f) _auto✝
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
V : Coalgebra G
⊢ ((𝟭 (Coalgebra G)).obj V).str ≫ G.map (𝟙 V.V) =
    𝟙 V.V ≫ ((Coalgebra.toAlgebraOf adj ⋙ Algebra.toCoalgebraOf adj).obj V).str
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
V : Coalgebra G
⊢ V.str ≫ G.map (𝟙 V.V) = 𝟙 V.V ≫ ((Algebra.toCoalgebraOf adj).obj ((Coalgebra.toAlgebraOf adj).obj V)).str
[PROOFSTEP]
rw [G.map_id, Category.comp_id, Category.id_comp]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
V : Coalgebra G
⊢ V.str = ((Algebra.toCoalgebraOf adj).obj ((Coalgebra.toAlgebraOf adj).obj V)).str
[PROOFSTEP]
apply ((adj.homEquiv _ _).right_inv V.str).symm
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
A : Algebra F
⊢ (Algebra.toCoalgebraOf adj).map (NatTrans.app (AlgCoalgEquiv.unitIso adj).hom A) ≫
      NatTrans.app (AlgCoalgEquiv.counitIso adj).hom ((Algebra.toCoalgebraOf adj).obj A) =
    𝟙 ((Algebra.toCoalgebraOf adj).obj A)
[PROOFSTEP]
ext
  -- Porting note: why doesn't `simp` work here?
[GOAL]
case w
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
A : Algebra F
⊢ autoParam
    (((Algebra.toCoalgebraOf adj).map (NatTrans.app (AlgCoalgEquiv.unitIso adj).hom A) ≫
          NatTrans.app (AlgCoalgEquiv.counitIso adj).hom ((Algebra.toCoalgebraOf adj).obj A)).f =
      (𝟙 ((Algebra.toCoalgebraOf adj).obj A)).f)
    _auto✝
[PROOFSTEP]
exact Category.comp_id _


[GOAL]
C : Type u₁
D : Type u₂
E : Type u₃
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Category.{v₃, u₃} E
F : C × D ⥤ E
W : C
X Y Z : D
f : X ⟶ Y
g : Y ⟶ Z
⊢ F.map (𝟙 W, f ≫ g) = F.map (𝟙 W, f) ≫ F.map (𝟙 W, g)
[PROOFSTEP]
rw [← Functor.map_comp, prod_comp, Category.comp_id]
[GOAL]
C : Type u₁
D : Type u₂
E : Type u₃
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Category.{v₃, u₃} E
F : C × D ⥤ E
X Y Z : C
W : D
f : X ⟶ Y
g : Y ⟶ Z
⊢ F.map (f ≫ g, 𝟙 W) = F.map (f, 𝟙 W) ≫ F.map (g, 𝟙 W)
[PROOFSTEP]
rw [← Functor.map_comp, prod_comp, Category.comp_id]
[GOAL]
C : Type u₁
D : Type u₂
E : Type u₃
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Category.{v₃, u₃} E
F : C × D ⥤ E
X X' : C
f : X ⟶ X'
Y Y' : D
g : Y ⟶ Y'
⊢ F.map (𝟙 X, g) ≫ F.map (f, 𝟙 Y') = F.map (f, g)
[PROOFSTEP]
rw [← Functor.map_comp, prod_comp, Category.id_comp, Category.comp_id]
[GOAL]
C : Type u₁
D : Type u₂
E : Type u₃
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Category.{v₃, u₃} E
F : C × D ⥤ E
X X' : C
f : X ⟶ X'
Y Y' : D
g : Y ⟶ Y'
⊢ F.map (f, 𝟙 Y) ≫ F.map (𝟙 X', g) = F.map (f, g)
[PROOFSTEP]
rw [← Functor.map_comp, prod_comp, Category.id_comp, Category.comp_id]