mathlib-initiative/mathlib-tactics huggingface dataset:
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✝ : HasPullbacks C
A : C
f g h : MonoOver A
k₁ : h ⟶ f
k₂ : h ⟶ g
⊢ Over.Hom.left k₂.hom ≫ ((forget A).obj g).hom = Over.Hom.left k₁.hom ≫ f.arrow

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f✝ : X✝ ⟶ Y
inst✝¹ : HasKernel f✝
inst✝ : HasKernels C
X : C
A B : Cᵒᵖ
f : A ⟶ op X
g : B ⟶ op X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ (kernel.lift g.unop (kernel.ι f.unop) ⋯ ≫ kernel.ι g.unop).op = (kernel.ι f.unop).op

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasImage f
W : C
k : W ⟶ X
⊢ (k ≫ factorThruImage f) ≫ (MonoOver.mk (image.ι f)).arrow = k ≫ f

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y X' : C
h : X' ⟶ X
f : X ⟶ Y
inst✝¹ : HasImage f
inst✝ : HasImage (h ≫ f)
⊢ image.preComp h f ≫ image.ι f = image.ι (h ≫ f)

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
A B : C
⊢ (imageSubobjectIso 0 ≪≫ imageZero ≪≫ botCoeIsoZero.symm).hom ≫ ⊥.arrow = (imageSubobject 0).arrow

Tactic:
by 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
a✝ : IsIso (imageToKernel S.f S.g ⋯)
⊢ (asIso (imageToKernel S.f S.g ⋯)).hom ≫ (kernelSubobject S.g).arrow = (imageSubobject S.f).arrow

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ (imageSubobjectIso f ≪≫ imageMonoIsoSource f ≪≫ (underlyingIso f).symm).hom ≫ (Subobject.mk f).arrow =
    (imageSubobject f).arrow

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y : C
inst✝² : HasEqualizers C
X' : C
h : X' ⟶ X
inst✝¹ : IsIso h
f : X ⟶ Y
inst✝ : HasImage f
⊢ inv (image.preComp h f) ≫ image.ι (h ≫ f) = image.ι f

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : mk f = ⊤
⊢ IsIso f

Tactic:
rw [← ofMkLEMk_comp h.le, Category.comp_id]
    exact (isoOfMkEqMk _ _ h).isIso_hom

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
B : C
⊢ (initialIsInitial.uniqueUpToIso HasZeroObject.zeroIsInitial).hom ≫ 0 = initial.to B

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
A B : C
⊢ 0 ≫ ⊥.arrow = 0

Tactic:
by 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✝ : HasPullbacks C
A : C
f g : Subobject A
⊢ f ⊓ g ≤ f

Tactic:
by 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✝ : HasPullbacks C
A : C
f g : Subobject A
⊢ f ⊓ g ≤ g

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
A : C
f g : Subobject A
⊢ (f ⊓ g).ofLE f ⋯ ≫ f.arrow = (f ⊓ g).ofLE g ⋯ ≫ g.arrow

Tactic:
by 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
h : kernel.ι S.g ≫ cokernel.π S.f = 0
⊢ ∀ {W' : C} (g' : W' ⟶ S.X₂) (eq' : g' ≫ S.g = 0), kernel.lift (cokernel.π S.f) g' ⋯ ≫ Abelian.image.ι S.f = g'

Tactic:
by 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
h : kernel.ι S.g ≫ cokernel.π S.f = 0
⊢ ∀ {Z' : C} (g' : S.X₂ ⟶ Z') (eq' : S.f ≫ g' = 0), Abelian.coimage.π S.g ≫ cokernel.desc (kernel.ι S.g) g' ⋯ = g'

Tactic:
by 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
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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by simp

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

Goal state before:
pp: case insert
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
a✝¹ : I
s✝ : Finset I
a✝ : a✝¹ ∉ s✝
ih : ∀ i ∈ s✝, (P i).Factors (s✝.inf P).arrow
⊢ ∀ i ∈ insert a✝¹ s✝, (P i).Factors ((insert a✝¹ s✝).inf P).arrow

Tactic:
intro _ m
    rw [Finset.inf_insert]
    simp only [Finset.mem_insert] at m
    rcases m with (rfl | m)
    · rw [← factorThru_arrow _ _ (inf_arrow_factors_left _ _)]
      exact factors_comp_arrow _
    · rw [← factorThru_arrow _ _ (inf_arrow_factors_right _ _)]
      apply factors_of_factors_right
      exact ih _ m

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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by simp

Goal state after:
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:
by simp

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

Goal state before:
pp: case f.refine_1
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
⊢ (∐ fun j ↦ underlying.obj ((equivShrink (Subobject A)).symm ↑j)) ⟶ underlying.obj f

Tactic:
refine Sigma.desc ?_
      rintro ⟨g, m⟩
      refine underlying.map (homOfLE (k _ ?_))
      simpa using m

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:
by 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:
by 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:
by 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
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
⊢ m =
    colimit.desc (liftToFinsetObj F)
      { pt := s.pt, ι := { app := fun x ↦ Sigma.desc fun x_1 ↦ s.ι.app ↑x_1, naturality := ⋯ } }

Tactic:
by
        apply colimit.hom_ext
        rintro t
        dsimp [liftToFinsetObj]
        apply colimit.hom_ext
        rintro ⟨⟨j, hj⟩⟩
        convert! h j using 1
        · simp [← colimit.w (liftToFinsetObj F) ⟨⟨Finset.singleton_subset_iff.2 hj⟩⟩]
          rfl
        · 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:
by 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:
by 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:
by 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:
by 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ᵒᵖ
⊢ (map (𝟙 d).unop).toCatHom = 𝟙 (Cat.of (StructuredArrow (Opposite.unop d) T))

Tactic:
by
    ext
    exact Functor.ext (fun ⟨_, _, _⟩ => by 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:
by 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✝ : 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:
by 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:
by 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:
by 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:
by 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:
by 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₁ F₂ : C ⥤ H
G : D ⥤ H
f : F₁ ⟶ F₂
α : F₂ ⟶ ((whiskeringLeft C D H).obj L).obj G
X : C
⊢ (L.lanUnit.app F₁).app X ≫ ((L.lan.obj F₁).descOfIsLeftKanExtension (L.lanUnit.app F₁) G (f ≫ α)).app (L.obj X) =
    (L.lanUnit.app F₁).app X ≫
      (L.lan.map f).app (L.obj X) ≫ ((L.lan.obj F₂).descOfIsLeftKanExtension (L.lanUnit.app F₂) G α).app (L.obj X)

Tactic:
rw [descOfIsLeftKanExtension_fac_app, NatTrans.comp_app, ← assoc]

Goal state after:
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₁ F₂ : C ⥤ H
G : D ⥤ H
f : F₁ ⟶ F₂
α : F₂ ⟶ ((whiskeringLeft C D H).obj L).obj G
X : C
⊢ f.app X ≫ α.app X =
    ((L.lanUnit.app F₁).app X ≫ (L.lan.map f).app (L.obj X)) ≫
      ((L.lan.obj F₂).descOfIsLeftKanExtension (L.lanUnit.app F₂) G α).app (L.obj X)
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:
by 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:
by 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:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
s t : CostructuredArrow yoneda A
p : OverArrows s.hom t.hom
⊢ yoneda.map p.val ≫ s.hom = t.hom

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
inst✝ : F'.IsRightKanExtension α
G : D ⥤ H
β : G ⟶ F'
⊢ L.whiskerLeft ((fun β ↦ F'.liftOfIsRightKanExtension α G β) ((fun β ↦ L.whiskerLeft β ≫ α) β)) ≫ α =
    L.whiskerLeft β ≫ α

Tactic:
by 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.RightExtension F
e : E ≅ E'
h : E.IsPointwiseRightKanExtension
⊢ (fun h Y ↦ (isPointwiseRightKanExtensionAtEquivOfIso e Y).symm (h Y))
      ((fun h Y ↦ (isPointwiseRightKanExtensionAtEquivOfIso e Y) (h Y)) h) =
    h

Tactic:
by simp

Goal state after: