mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
h : S.Exact
⊢ (Cofork.π (CokernelCofork.ofπ (Abelian.coimage.π S.g) ⋯) ≫ (Abelian.coimageIsoImage' S.g).hom) ≫ image.ι S.g =
    factorThruImage S.g ≫ image.ι S.g

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
X Y : C
f : X ⟶ Y
⊢ kernel.ι f ≫ f = 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
X Y : C
f : X ⟶ Y
⊢ f ≫ cokernel.π f = 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
B : C
X Y : Subobject B
⊢ (X ⊓ Y).ofLE X ⋯ ≫ (representative.obj X).arrow = (X ⊓ Y).arrow

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : kernel.ι f = 0 → Mono f
tfae_1_to_2 : Mono f → kernel.ι f = 0
⊢ { X₁ := Z, X₂ := X, X₃ := Y, f := 0, g := f, zero := ⋯ }.f = 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
B : C
X Y : Subobject B
⊢ (X ⊓ Y).ofLE Y ⋯ ≫ (representative.obj Y).arrow = (X ⊓ Y).arrow

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : cokernel.π f = 0 → Epi f
tfae_1_to_2 : Epi f → cokernel.π f = 0
⊢ { X₁ := X, X₂ := Y, X₃ := Z, f := f, g := 0, zero := ⋯ }.g = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
tfae_1_to_3 : (∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact) → F.PreservesHomology
hF : ∀ (S : ShortComplex C), S.Exact → (S.map F).Exact
S : ShortComplex C
hS : S.ShortExact
⊢ ({ X₁ := 0, X₂ := S.X₁, X₃ := S.X₂, f := 0, g := S.f, zero := ?m.210 }.map F).f = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
tfae_1_to_3 : (∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact) → F.PreservesHomology
hF : ∀ (S : ShortComplex C), S.Exact → (S.map F).Exact
S : ShortComplex C
hS : S.ShortExact
⊢ 0 ≫ S.f = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
tfae_1_to_3 : (∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact) → F.PreservesHomology
hF : ∀ (S : ShortComplex C), S.Exact → (S.map F).Exact
S : ShortComplex C
hS : S.ShortExact
⊢ { X₁ := 0, X₂ := S.X₁, X₃ := S.X₂, f := 0, g := S.f, zero := ⋯ }.f = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
tfae_1_to_3 : (∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact) → F.PreservesHomology
hF : ∀ (S : ShortComplex C), S.Exact → (S.map F).Exact
S : ShortComplex C
hS : S.ShortExact
this : Mono (S.map F).f
⊢ ({ X₁ := S.X₂, X₂ := S.X₃, X₃ := 0, f := S.g, g := 0, zero := ?m.265 }.map F).g = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
tfae_1_to_3 : (∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact) → F.PreservesHomology
hF : ∀ (S : ShortComplex C), S.Exact → (S.map F).Exact
S : ShortComplex C
hS : S.ShortExact
this : Mono (S.map F).f
⊢ S.g ≫ 0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
tfae_1_to_3 : (∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact) → F.PreservesHomology
hF : ∀ (S : ShortComplex C), S.Exact → (S.map F).Exact
S : ShortComplex C
hS : S.ShortExact
this : Mono (S.map F).f
⊢ { X₁ := S.X₂, X₂ := S.X₃, X₃ := 0, f := S.g, g := 0, zero := ⋯ }.g = 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : LocallySmall.{w, v₁, u₁} C
inst✝ : WellPowered.{w, v₁, u₁} C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, f ≤ g
⊢ ∀ (j : ↑(⇑(equivShrink (Subobject A)) '' s)),
    underlying.map (homOfLE ⋯) ≫ (wideCospan s).map (WidePullbackShape.Hom.term j) = f.arrow

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: case e'_2.e'_7
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : LocallySmall.{w, v₁, u₁} C
inst✝¹ : WellPowered.{w, v₁, u₁} C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
e_1✝ : (widePullback s ⟶ A) = (limit (wideCospan s) ⟶ (wideCospan s).obj none)
e_5✝ : A = (wideCospan s).obj none
⊢ eqToHom ⋯ ≫ f.arrow = (wideCospan s).map (WidePullbackShape.Hom.term ⟨(equivShrink (Subobject A)) f, ⋯⟩)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.FunctorCategory

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ (cokernel.π α).app X ≫ 𝟙 ((cokernel α).obj X) =
    𝟙 (G.obj X) ≫ cokernel.π (α.app X) ≫ (PreservesCokernel.iso ((evaluation C D).obj X) α).inv

Tactic:
simp only [PreservesCokernel.iso_inv, Category.id_comp, Category.comp_id]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ (cokernel.π α).app X = cokernel.π (α.app X) ≫ cokernelComparison α ((evaluation C D).obj X)
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
x : β
h : e.symm x ∈ s
⊢ e (e.symm x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: case f.refine_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, g ≤ f
b✝ : ↑(⇑(equivShrink (Subobject A)) '' s)
⊢ Sigma.ι (fun j ↦ underlying.obj ((equivShrink (Subobject A)).symm ↑j)) b✝ ≫
      (Sigma.desc fun b ↦ underlying.map (homOfLE ⋯)) ≫ f.arrow =
    Sigma.ι (fun j ↦ underlying.obj ((equivShrink (Subobject A)).symm ↑j)) b✝ ≫
      Sigma.desc fun j ↦ ((equivShrink (Subobject A)).symm ↑j).arrow

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
Y : Subobject X
Z : Subobject (underlying.obj Y)
⊢ ((underlyingIso (Z.arrow ≫ Y.arrow)).hom ≫ Z.arrow) ≫ Y.arrow = (mk (Z.arrow ≫ Y.arrow)).arrow

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
Y : Subobject X
W Z : Subobject (underlying.obj Y)
h : W ≤ Z
⊢ ((underlyingIso (W.arrow ≫ Y.arrow)).hom ≫ W.ofLE Z h ≫ (underlyingIso (Z.arrow ≫ Y.arrow)).inv) ≫
      (mk (Z.arrow ≫ Y.arrow)).arrow =
    (mk (W.arrow ≫ Y.arrow)).arrow

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: case h₁
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst✝ : HasBinaryProduct A B
⊢ (((prod.lift coprod.inl.unop coprod.inr.unop).op ≫ coprod.desc prod.fst.op prod.snd.op).unop ≫ prod.fst).op =
    ((𝟙 (op (A ⨯ B))).unop ≫ prod.fst).op

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: case h₂
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst✝ : HasBinaryProduct A B
⊢ (((prod.lift coprod.inl.unop coprod.inr.unop).op ≫ coprod.desc prod.fst.op prod.snd.op).unop ≫ prod.snd).op =
    ((𝟙 (op (A ⨯ B))).unop ≫ prod.snd).op

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: case h₁
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst✝ : HasBinaryProduct A B
⊢ ((BinaryCofan.mk prod.fst.op prod.snd.op).ι.app { as := WalkingPair.left } ≫
        (prod.lift coprod.inl.unop coprod.inr.unop).op).unop =
    (coprod.inl ≫ 𝟙 (op A ⨿ op B)).unop

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: case h₂
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst✝ : HasBinaryProduct A B
⊢ ((BinaryCofan.mk prod.fst.op prod.snd.op).ι.app { as := WalkingPair.right } ≫
        (prod.lift coprod.inl.unop coprod.inr.unop).op).unop =
    (coprod.inr ≫ 𝟙 (op A ⨿ op B)).unop

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
α : Type w
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasColimitsOfShape (Finset (Discrete α)) C
F : Discrete α ⥤ C
j : Discrete α
⊢ j ∈ {j}

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered

Goal state before:
pp: case e'_3
C : Type u
inst✝² : Category.{v, u} C
α : Type w
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasColimitsOfShape (Finset (Discrete α)) C
F : Discrete α ⥤ C
s : Cocone F
m :
  { pt := colimit (liftToFinsetObj F),
        ι := Discrete.natTrans fun j ↦ Sigma.ι (fun x ↦ F.obj ↑x) ⟨j, ⋯⟩ ≫ colimit.ι (liftToFinsetObj F) {j} }.pt ⟶
    s.pt
h :
  ∀ (j : Discrete α),
    { pt := colimit (liftToFinsetObj F),
                ι :=
                  Discrete.natTrans fun j ↦
                    Sigma.ι (fun x ↦ F.obj ↑x) ⟨j, ⋯⟩ ≫ colimit.ι (liftToFinsetObj F) {j} }.ι.app
          j ≫
        m =
      s.ι.app j
t : Finset (Discrete α)
j : Discrete α
hj : j ∈ t
e_1✝ : ((Discrete.functor fun x ↦ F.obj ↑x).obj { as := ⟨j, hj⟩ } ⟶ s.pt) = (F.obj j ⟶ s.pt)
⊢ colimit.ι (Discrete.functor fun x ↦ F.obj ↑x) { as := ⟨j, hj⟩ } ≫
      colimit.ι
          { obj := fun s ↦ ∐ fun x ↦ F.obj ↑x,
            map := fun {x Y} h ↦ Sigma.desc fun y ↦ Sigma.ι (fun x ↦ F.obj ↑x) ⟨↑y, ⋯⟩, map_id := ⋯, map_comp := ⋯ }
          t ≫
        colimit.desc
          { obj := fun s ↦ ∐ fun x ↦ F.obj ↑x,
            map := fun {x Y} h ↦ Sigma.desc fun y ↦ Sigma.ι (fun x ↦ F.obj ↑x) ⟨↑y, ⋯⟩, map_id := ⋯, map_comp := ⋯ }
          { pt := s.pt, ι := { app := fun x ↦ Sigma.desc fun x_1 ↦ s.ι.app ↑x_1, naturality := ⋯ } } =
    s.ι.app j

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
α : Type w
inst✝² : HasFiniteCoproducts C
f : α → C
inst✝¹ : HasColimitsOfShape (Finset (Discrete α)) C
inst✝ : HasCoproduct f
S : Finset (Discrete α)
j : ↥S
e_1✝ : (f (↑j).as ⟶ ∐ f) = ((Discrete.functor f).obj ↑j ⟶ (colimit.cocone (Discrete.functor f)).pt)
e_3✝ : f (↑j).as = (Discrete.functor f).obj ↑j
e_4✝ : colimit (liftToFinsetObj (Discrete.functor f)) = (liftToFinsetColimitCocone (Discrete.functor f)).cocone.pt
⊢ {↑j} ⊆ S

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered

Goal state before:
pp: case e'_3
C : Type u
inst✝³ : Category.{v, u} C
α : Type w
inst✝² : HasFiniteCoproducts C
f : α → C
inst✝¹ : HasColimitsOfShape (Finset (Discrete α)) C
inst✝ : HasCoproduct f
S : Finset (Discrete α)
j : ↥S
e_1✝ : (f (↑j).as ⟶ ∐ f) = ((Discrete.functor f).obj ↑j ⟶ (colimit.cocone (Discrete.functor f)).pt)
⊢ (Sigma.ι (fun x ↦ f (↑x).as) j ≫ Sigma.desc fun s ↦ Sigma.ι f (↑s).as) =
    (colimit.cocone (Discrete.functor f)).ι.app ↑j

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
α : Type w
inst✝ : HasFiniteCoproducts C
I : Finset (Discrete α)
X✝ Y✝ : Discrete α ⥤ C
x✝ : X✝ ⟶ Y✝
b✝ : ↥I
⊢ Sigma.ι (fun x ↦ X✝.obj ↑x) b✝ ≫
      (Sigma.map fun x ↦ x✝.app ↑x) ≫ (HasColimit.isoOfNatIso (Discrete.natIso fun x ↦ Iso.refl (Y✝.obj ↑x.as))).hom =
    Sigma.ι (fun x ↦ X✝.obj ↑x) b✝ ≫
      (HasColimit.isoOfNatIso (Discrete.natIso fun x ↦ Iso.refl (X✝.obj ↑x.as))).hom ≫
        colimMap ((Discrete.functor fun x ↦ ↑x).whiskerLeft x✝)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
α : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : HasLimitsOfShape (Finset (Discrete α))ᵒᵖ C
F : Discrete α ⥤ C
j : Discrete α
⊢ j ∈ {j}

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered

Goal state before:
pp: case e'_3
C : Type u
inst✝² : Category.{v, u} C
α : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : HasLimitsOfShape (Finset (Discrete α))ᵒᵖ C
F : Discrete α ⥤ C
s : Cone F
m :
  s.pt ⟶
    { pt := limit (liftToFinsetObj F),
        π := Discrete.natTrans fun j ↦ limit.π (liftToFinsetObj F) (op {j}) ≫ Pi.π (fun x ↦ F.obj ↑x) ⟨j, ⋯⟩ }.pt
h :
  ∀ (j : Discrete α),
    m ≫
        { pt := limit (liftToFinsetObj F),
                π :=
                  Discrete.natTrans fun j ↦
                    limit.π (liftToFinsetObj F) (op {j}) ≫ Pi.π (fun x ↦ F.obj ↑x) ⟨j, ⋯⟩ }.π.app
          j =
      s.π.app j
t : (Finset (Discrete α))ᵒᵖ
j : Discrete α
hj : j ∈ unop t
e_1✝ : (s.pt ⟶ (Discrete.functor fun x ↦ F.obj ↑x).obj { as := ⟨j, hj⟩ }) = (s.pt ⟶ F.obj j)
⊢ (limit.lift
          { obj := fun s ↦ ∏ᶜ fun x ↦ F.obj ↑x, map := fun {Y x} h ↦ Pi.lift fun y ↦ Pi.π (fun x ↦ F.obj ↑x) ⟨↑y, ⋯⟩,
            map_id := ⋯, map_comp := ⋯ }
          { pt := s.pt, π := { app := fun x ↦ Pi.lift fun x_1 ↦ s.π.app ↑x_1, naturality := ⋯ } } ≫
        limit.π
          { obj := fun s ↦ ∏ᶜ fun x ↦ F.obj ↑x, map := fun {Y x} h ↦ Pi.lift fun y ↦ Pi.π (fun x ↦ F.obj ↑x) ⟨↑y, ⋯⟩,
            map_id := ⋯, map_comp := ⋯ }
          t) ≫
      limit.π (Discrete.functor fun x ↦ F.obj ↑x) { as := ⟨j, hj⟩ } =
    s.π.app j

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
α : Type w
inst✝² : HasFiniteProducts C
f : α → C
inst✝¹ : HasLimitsOfShape (Finset (Discrete α))ᵒᵖ C
inst✝ : HasProduct f
S : (Finset (Discrete α))ᵒᵖ
j : ↥(unop S)
⊢ {↑j} ⊆ unop S

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Functor

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : C ⥤ D
d : Dᵒᵖ
x✝ : ↑(Cat.of (StructuredArrow (Opposite.unop d) T))
left✝ : Discrete PUnit.{1}
right✝ : C
hom✝ : (Functor.fromPUnit (Opposite.unop d)).obj left✝ ⟶ T.obj right✝
⊢ (map (𝟙 d).unop).toCatHom.toFunctor.obj { left := left✝, right := right✝, hom := hom✝ } =
    (𝟙 (Cat.of (StructuredArrow (Opposite.unop d) T))).toFunctor.obj { left := left✝, right := right✝, hom := hom✝ }

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Functor

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : C ⥤ D
X✝ Y✝ Z✝ : Dᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x✝ : ↑(Cat.of (StructuredArrow (Opposite.unop X✝) T))
⊢ (map (f ≫ g).unop).toCatHom.toFunctor.obj x✝ = ((map f.unop).toCatHom ≫ (map g.unop).toCatHom).toFunctor.obj x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_4, u_4} H
F : C ⥤ H
Y : D
L L' : C ⥤ D
e : L ≅ L'
inst✝ : L.HasPointwiseLeftKanExtensionAt F Y
Φ : CostructuredArrow L' Y ≌ CostructuredArrow L Y := Comma.mapLeftIso (fromPUnit Y) e.symm
⊢ L'.HasPointwiseLeftKanExtensionAt F Y

Tactic:
let e' : CostructuredArrow.proj L' Y ⋙ F ≅
    Φ.functor ⋙ CostructuredArrow.proj L Y ⋙ F := Iso.refl _

Goal state after:
C : Type u_1
D : Type u_2
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_4, u_4} H
F : C ⥤ H
Y : D
L L' : C ⥤ D
e : L ≅ L'
inst✝ : L.HasPointwiseLeftKanExtensionAt F Y
Φ : CostructuredArrow L' Y ≌ CostructuredArrow L Y := Comma.mapLeftIso (fromPUnit Y) e.symm
e' : CostructuredArrow.proj L' Y ⋙ F ≅ Φ.functor ⋙ CostructuredArrow.proj L Y ⋙ F :=
  Iso.refl (CostructuredArrow.proj L' Y ⋙ F)
⊢ L'.HasPointwiseLeftKanExtensionAt F Y
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Functor

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
L : C ⥤ D
R : E ⥤ D
X✝ Y✝ : Grothendieck (R ⋙ functor L)
f : X✝ ⟶ Y✝
⊢ L.map f.fiber.left ≫ { left := left Y✝.fiber, right := Y✝.base, hom := hom Y✝.fiber }.hom =
    { left := left X✝.fiber, right := X✝.base, hom := hom X✝.fiber }.hom ≫ R.map f.base

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Functor

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
L : C ⥤ D
R : E ⥤ D
X : E
X✝ Y✝ : ↑((R ⋙ functor L).obj X)
x✝ : X✝ ⟶ Y✝
⊢ (Grothendieck.ι (R ⋙ functor L) X ⋙ grothendieckPrecompFunctorToComma L R ⋙ Comma.fst L R).map x✝ ≫
      (Iso.refl
          ((Grothendieck.ι (R ⋙ functor L) X ⋙ grothendieckPrecompFunctorToComma L R ⋙ Comma.fst L R).obj Y✝)).hom =
    (Iso.refl ((Grothendieck.ι (R ⋙ functor L) X ⋙ grothendieckPrecompFunctorToComma L R ⋙ Comma.fst L R).obj X✝)).hom ≫
      (proj L (R.obj X)).map x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Functor

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
L : C ⥤ D
R : E ⥤ D
X : Comma L R
⊢ eqToHom ⋯ ≫ { base := (𝟙 X).right, fiber := homMk (𝟙 X).left ⋯ }.fiber =
    (𝟙 { base := X.right, fiber := mk X.hom }).fiber

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Functor

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
L : C ⥤ D
R : E ⥤ D
X✝ Y✝ Z✝ : Comma L R
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ eqToHom ⋯ ≫ { base := (f ≫ g).right, fiber := homMk (f ≫ g).left ⋯ }.fiber =
    ({ base := f.right, fiber := homMk f.left ⋯ } ≫ { base := g.right, fiber := homMk g.left ⋯ }).fiber

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
H : Type u_3
inst✝² : Category.{v_3, u_3} H
F : C ⥤ H
inst✝¹ : L.HasPointwiseLeftKanExtension F
inst✝ : L.HasLeftKanExtension F
this : ∀ (X : D), HasColimit (Grothendieck.ι (functor L) X ⋙ grothendieckProj L ⋙ F) :=
  fun X ↦
    hasColimit_of_iso
      (isoWhiskerRight (eqToIso (id (congrArg Cat.Hom.toFunctor ((functor L).map_id X))))
            (Grothendieck.ι (functor L) X ⋙ grothendieckProj L ⋙ F) ≪≫
          (Grothendieck.ι (functor L) X ⋙ grothendieckProj L ⋙ F).leftUnitor).symm
X✝ Y✝ : D
f : X✝ ⟶ Y✝
⊢ ∀ (j : ↑((functor L).obj X✝)),
    colimit.ι (Grothendieck.ι (functor L) X✝ ⋙ grothendieckProj L ⋙ F) j ≫
        (fiberwiseColimit (grothendieckProj L ⋙ F)).map f ≫
          (HasColimit.isoOfNatIso (isoWhiskerRight (ιCompGrothendieckProj L Y✝) F) ≪≫
              (L.leftKanExtensionObjIsoColimit F Y✝).symm).hom =
      colimit.ι (Grothendieck.ι (functor L) X✝ ⋙ grothendieckProj L ⋙ F) j ≫
        (HasColimit.isoOfNatIso (isoWhiskerRight (ιCompGrothendieckProj L X✝) F) ≪≫
              (L.leftKanExtensionObjIsoColimit F X✝).symm).hom ≫
          (L.leftKanExtension F).map f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_4, u_4} H
L L' : C ⥤ D
F F' : C ⥤ H
Y : D
inst✝ : L.HasPointwiseRightKanExtensionAt F Y
e₁ : L ≅ L'
e₂ : F ≅ F'
⊢ L'.HasPointwiseRightKanExtensionAt F' Y

Tactic:
rw [hasPointwiseRightKanExtensionAt_iff_of_natIso_left _ e₁.symm]

Goal state after:
C : Type u_1
D : Type u_2
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_4, u_4} H
L L' : C ⥤ D
F F' : C ⥤ H
Y : D
inst✝ : L.HasPointwiseRightKanExtensionAt F Y
e₁ : L ≅ L'
e₂ : F ≅ F'
⊢ L.HasPointwiseRightKanExtensionAt F' Y
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E✝ : L.LeftExtension F
Y : D
E E' : L.LeftExtension F
φ : E ⟶ E'
G : CostructuredArrow L Y
⊢ ((StructuredArrow.hom E).app G.left ≫ (StructuredArrow.right E).map G.hom) ≫ (StructuredArrow.Hom.right φ).app Y =
    (StructuredArrow.hom E ≫ ((whiskeringLeft C D H).obj L).map (StructuredArrow.Hom.right φ)).app G.left ≫
      (StructuredArrow.right E').map G.hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{v_3, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasLeftKanExtension F
F : C ⥤ H
⊢ L.lanUnit.app F ≫ 𝟙 (L ⋙ L.lan.obj F) = L.lanUnit.app F

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E E' : L.LeftExtension F
e : E ≅ E'
h : E.IsPointwiseLeftKanExtension
⊢ (fun h Y ↦ (isPointwiseLeftKanExtensionAtEquivOfIso e Y).symm (h Y))
      ((fun h Y ↦ (isPointwiseLeftKanExtensionAtEquivOfIso e Y) (h Y)) h) =
    h

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{v_3, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasLeftKanExtension F
G : D ⥤ H
⊢ L.lanUnit.app (L ⋙ G) ≫ L.whiskerLeft ((L.lanAdjunction H).counit.app G) = 𝟙 (L ⋙ G)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E E' : L.LeftExtension F
e : E ≅ E'
h : E'.IsPointwiseLeftKanExtension
⊢ (fun h Y ↦ (isPointwiseLeftKanExtensionAtEquivOfIso e Y) (h Y))
      ((fun h Y ↦ (isPointwiseLeftKanExtensionAtEquivOfIso e Y).symm (h Y)) h) =
    h

Tactic:
simp

Goal state after: