mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝¹⁵ : CommSemiring R
S : Submonoid R
M₀ : Type u_6
M₀' : Type u_9
inst✝¹⁴ : AddCommMonoid M₀
inst✝¹³ : AddCommMonoid M₀'
inst✝¹² : Module R M₀
inst✝¹¹ : Module R M₀'
f₀ : M₀ →ₗ[R] M₀'
inst✝¹⁰ : IsLocalizedModule S f₀
M₁ : Type u_7
M₁' : Type u_11
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₁'
inst✝⁷ : Module R M₁
inst✝⁶ : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst✝⁵ : IsLocalizedModule S f₁
M₂ : Type u_8
M₂' : Type u_10
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₂'
inst✝² : Module R M₂
inst✝¹ : Module R M₂'
f₂ : M₂ →ₗ[R] M₂'
inst✝ : IsLocalizedModule S f₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
⊢ (map S f₀ f₂) (h ∘ₗ g) = (map S f₁ f₂) h ∘ₗ (map S f₀ f₁) g

Tactic:
by
  ext x
  obtain ⟨⟨x, s⟩, rfl⟩ := IsLocalizedModule.mk'_surjective S f₀ x
  simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case fac_left
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
s : PullbackCone f g
x : ↑s.pt
⊢ (Hom.hom
        (ofHom
            (((Hom.hom s.fst).prod (Hom.hom s.snd)).codRestrict
              (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))) ⋯) ≫
          ofHom
            ((RingHom.fst ↑A ↑B).comp
              (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype)))
      x =
    (Hom.hom s.fst) x

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case fac_right
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
s : PullbackCone f g
x : ↑s.pt
⊢ (Hom.hom
        (ofHom
            (((Hom.hom s.fst).prod (Hom.hom s.snd)).codRestrict
              (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))) ⋯) ≫
          ofHom
            ((RingHom.snd ↑A ↑B).comp
              (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype)))
      x =
    (Hom.hom s.snd) x

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case uniq
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
s : PullbackCone f g
m : s.pt ⟶ of ↥(((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B)))
e₁ :
  m ≫
      ofHom
        ((RingHom.fst ↑A ↑B).comp
          (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype) =
    s.fst
e₂ :
  m ≫
      ofHom
        ((RingHom.snd ↑A ↑B).comp
          (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype) =
    s.snd
x : ↑s.pt
eq1 :
  (Hom.hom
        (m ≫
          ofHom
            ((RingHom.fst ↑A ↑B).comp
              (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype)))
      x =
    (Hom.hom s.fst) x
eq2 :
  (Hom.hom
        (m ≫
          ofHom
            ((RingHom.snd ↑A ↑B).comp
              (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype)))
      x =
    (Hom.hom s.snd) x
⊢ ↑((ConcreteCategory.hom m) x) =
    ((Hom.hom
          (m ≫
            ofHom
              ((RingHom.fst ↑A ↑B).comp
                (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype)))
        x,
      (Hom.hom
          (m ≫
            ofHom
              ((RingHom.snd ↑A ↑B).comp
                (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype)))
        x)

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
inst✝ : IsLocalHom (Hom.hom g)
x : ↑(limit.cone (cospan f g)).pt
hx : IsUnit ((ConcreteCategory.hom ((limit.cone (cospan f g)).π.app left)) x)
⊢ (RingHom.id ↑C) (((Hom.hom f).comp (Hom.hom (pullback.fst f g))) x) =
    (ConcreteCategory.hom f) ((ConcreteCategory.hom (pullback.fst f g)) x)

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Opposite

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
P : ObjectProperty C
⊢ P.op = P.op

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Opposite

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
P : ObjectProperty Cᵒᵖ
⊢ P.unop = P.unop

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : σ → A
p : MvPolynomial σ R
⊢ (eval₂Hom (algebraMap R B) (⇑(algebraMap A B) ∘ x)) p = (eval₂Hom (algebraMap R B) fun i ↦ (algebraMap A B) (x i)) p

Tactic:
Function.comp_def

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : σ → A
p : MvPolynomial σ R
⊢ (eval₂Hom (algebraMap R B) fun x_1 ↦ (algebraMap A B) (x x_1)) p =
    (eval₂Hom (algebraMap R B) fun i ↦ (algebraMap A B) (x i)) p
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: case refl
X : Type u_1
a b : Discrete X
⊢ a.as = a.as

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: case refl
J : Type u₁
inst✝ : Category.{v₁, u₁} J
α : Type u₁
F : J → α
hF : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂
j j' : J
⊢ F j = F j

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Products

Goal state before:
pp: case refine_1.refine_2.h₁
X X✝ Y✝ : Type u
x✝ : X✝ ⟶ Y✝
⊢ (↾fun x ↦ (x.1, (ConcreteCategory.hom x✝) x.2)) ≫ ↾_root_.Prod.fst = ↾_root_.Prod.fst

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Products

Goal state before:
pp: case h₂
X X✝ Y✝ : Type u
x✝ : X✝ ⟶ Y✝
⊢ (↾fun x ↦ (x.1, (ConcreteCategory.hom x✝) x.2)) ≫ ↾_root_.Prod.snd = ↾_root_.Prod.snd ≫ x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Products

Goal state before:
pp: case refine_2.h₁
X✝ Y✝ : Type u
x✝¹ : X✝ ⟶ Y✝
x✝ : Type u
⊢ BinaryFan.IsLimit.lift (binaryProductLimit Y✝ x✝) (↾_root_.Prod.fst ≫ x✝¹) (↾_root_.Prod.snd) ≫ ↾_root_.Prod.fst =
    ↾_root_.Prod.fst ≫ x✝¹

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Products

Goal state before:
pp: case h₂
X✝ Y✝ : Type u
x✝¹ : X✝ ⟶ Y✝
x✝ : Type u
⊢ BinaryFan.IsLimit.lift (binaryProductLimit Y✝ x✝) (↾_root_.Prod.fst ≫ x✝¹) (↾_root_.Prod.snd) ≫ ↾_root_.Prod.snd =
    ↾_root_.Prod.snd

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Products

Goal state before:
pp: J : Type v
F : J → Type (max v u)
j : J
⊢ ((productIso F).hom ≫ ↾fun f ↦ f j) = Pi.π F j

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
P Q : ObjectProperty C
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v, u} P
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} Q
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (P ⊔ Q)

Tactic:
obtain ⟨P', _, hP'⟩ := EssentiallySmall.exists_small_le' P
  obtain ⟨Q', _, hQ'⟩ := EssentiallySmall.exists_small_le' Q
  refine ⟨P' ⊔ Q', inferInstance, ?_⟩
  simp only [sup_le_iff]
  constructor
  · exact hP'.trans (monotone_isoClosure le_sup_left)
  · exact hQ'.trans (monotone_isoClosure le_sup_right)

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
x✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty C
h₁ : ObjectProperty.Small.{w, v, u} Q
left✝ : Q ≤ P
h₂ : P ≤ Q.isoClosure
⊢ P.op ≤ Q.isoClosure.op

Tactic:
op_monotone_iff

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
x✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty C
h₁ : ObjectProperty.Small.{w, v, u} Q
left✝ : Q ≤ P
h₂ : P ≤ Q.isoClosure
⊢ P ≤ Q.isoClosure
Module: Mathlib.CategoryTheory.MorphismProperty.Comma

Goal state before:
pp: A : Type u_1
inst✝⁴ : Category.{v_1, u_1} A
B : Type u_2
inst✝³ : Category.{v_2, u_2} B
T : Type u_3
inst✝² : Category.{v_3, u_3} T
L : A ⥤ T
R : B ⥤ T
P : MorphismProperty T
Q : MorphismProperty A
W : MorphismProperty B
inst✝¹ : Q.IsMultiplicative
inst✝ : W.IsMultiplicative
X : MorphismProperty.Comma L R P Q W
⊢ (eqToHom ⋯).left = eqToHom ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Comma

Goal state before:
pp: A : Type u_1
inst✝⁴ : Category.{v_1, u_1} A
B : Type u_2
inst✝³ : Category.{v_2, u_2} B
T : Type u_3
inst✝² : Category.{v_3, u_3} T
L : A ⥤ T
R : B ⥤ T
P : MorphismProperty T
Q : MorphismProperty A
W : MorphismProperty B
inst✝¹ : Q.IsMultiplicative
inst✝ : W.IsMultiplicative
X : MorphismProperty.Comma L R P Q W
⊢ (eqToHom ⋯).right = eqToHom ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
X✝ Y✝ : StructuredArrow PUnit.{w + 1} F
f : X✝ ⟶ Y✝
⊢ (ConcreteCategory.hom (F.map (StructuredArrow.Hom.right f))) ((ConcreteCategory.hom X✝.hom) PUnit.unit) =
    (ConcreteCategory.hom (X✝.hom ≫ F.map (StructuredArrow.Hom.right f))) PUnit.unit

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
X Y : StructuredArrow PUnit.{w + 1} F
f : X ⟶ Y
⊢ (ConcreteCategory.hom (F.map (StructuredArrow.Hom.right f))) ((ConcreteCategory.hom X.hom) PUnit.unit) =
    (ConcreteCategory.hom (X.hom ≫ F.map (StructuredArrow.Hom.right f))) PUnit.unit

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X : F.Elementsᵒᵖ
⊢ (ConcreteCategory.hom (𝟙 (F.obj (unop X).1))) (unop X).snd = (unop X).snd

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X : CostructuredArrow yoneda F
⊢ yoneda.map (Iso.refl (((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj X).left).hom ≫
      ((𝟭 (CostructuredArrow yoneda F)).obj X).hom =
    (((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj X).hom

Tactic:
by
    dsimp
    simpa only [Functor.map_id, Category.id_comp] using!
      (yonedaEquiv.symm_apply_apply X.hom).symm

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
X : C
d : ↑(F.obj X)
⊢ G.map { base := 𝟙 X, fiber := 𝟙 ((F.map (𝟙 X)).toFunctor.obj d) } ≫
      colimit.ι (Grothendieck.ι F X ⋙ G) ((F.map (𝟙 X)).toFunctor.obj d) =
    G.map { base := eqToHom ⋯, fiber := eqToHom ⋯ } ≫ colimit.ι (Grothendieck.ι F X ⋙ G) ((F.map (𝟙 X)).toFunctor.obj d)

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
f : X ⟶ Y
⊢ (F.map f.base).toFunctor.obj X.fiber = (F.map f.base).toFunctor.obj X.fiber

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X : Grothendieck F
⊢ (eqToHom ⋯).base = eqToHom ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X : Grothendieck F
⊢ (eqToHom ⋯).fiber = eqToHom ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X : Grothendieck F
⊢ X.base = X.base

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X : Grothendieck F
⊢ eqToHom ⋯ = { base := eqToHom ⋯, fiber := eqToHom ⋯ }

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F G : C ⥤ D
η : F ⟶ G
X Y : WithTerminal C
f : X ⟶ Y
x : C
x✝ : of x ⟶ star
⊢ ((map F).map x✝ ≫
      match star with
      | of x => η.app x
      | star => 𝟙 star) =
    (match of x with
      | of x => η.app x
      | star => 𝟙 star) ≫
      (map G).map x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F G : C ⥤ D
η : F ⟶ G
X Y : WithTerminal C
f : X ⟶ Y
x✝ : star ⟶ star
⊢ ((map F).map x✝ ≫
      match star with
      | of x => η.app x
      | star => 𝟙 star) =
    (match star with
      | of x => η.app x
      | star => 𝟙 star) ≫
      (map G).map x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: case of
C : Type u
inst✝ : Category.{v, u} C
a✝¹ b✝ : Cat
f✝ : a✝¹ ⟶ b✝
a✝ : ↑a✝¹
⊢ (NatTrans.toCatHom₂ (map₂ (𝟙 f✝).toNatTrans)).toNatTrans.app (of a✝) =
    (𝟙 (map f✝.toFunctor).toCatHom).toNatTrans.app (of a✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: case star
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : Cat
f✝ : a✝ ⟶ b✝
⊢ (NatTrans.toCatHom₂ (map₂ (𝟙 f✝).toNatTrans)).toNatTrans.app star =
    (𝟙 (map f✝.toFunctor).toCatHom).toNatTrans.app star

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: case h_obj
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X : Grothendieck F
⊢ (map (𝟙 F)).obj X = (𝟭 (Grothendieck F)).obj X

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: case of
C : Type u
inst✝ : Category.{v, u} C
a✝¹ b✝ : Cat
f✝ g✝ h✝ : a✝¹ ⟶ b✝
η✝ : f✝ ⟶ g✝
θ✝ : g✝ ⟶ h✝
a✝ : ↑a✝¹
⊢ (NatTrans.toCatHom₂ (map₂ (η✝ ≫ θ✝).toNatTrans)).toNatTrans.app (of a✝) =
    (NatTrans.toCatHom₂ (map₂ η✝.toNatTrans) ≫ NatTrans.toCatHom₂ (map₂ θ✝.toNatTrans)).toNatTrans.app (of a✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: case star
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : Cat
f✝ g✝ h✝ : a✝ ⟶ b✝
η✝ : f✝ ⟶ g✝
θ✝ : g✝ ⟶ h✝
⊢ (NatTrans.toCatHom₂ (map₂ (η✝ ≫ θ✝).toNatTrans)).toNatTrans.app star =
    (NatTrans.toCatHom₂ (map₂ η✝.toNatTrans) ≫ NatTrans.toCatHom₂ (map₂ θ✝.toNatTrans)).toNatTrans.app star

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: case h_map
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
f : X ⟶ Y
⊢ { base := f.base, fiber := f.fiber } = f

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: case h_obj
C : Type u
inst✝ : Category.{v, u} C
F G H : C ⥤ Cat
α : F ⟶ G
β : G ⟶ H
X : Grothendieck F
⊢ (map (α ≫ β)).obj X = (map α ⋙ map β).obj X

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: case star
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ c✝ : Cat
f✝ : a✝ ⟶ b✝
g✝ h✝ : b✝ ⟶ c✝
η✝ : g✝ ⟶ h✝
⊢ (prelaxfunctor.map₂ (Bicategory.whiskerLeft f✝ η✝)).toNatTrans.app star =
    ((Cat.Hom.isoMk (mapComp f✝.toFunctor g✝.toFunctor)).hom ≫
            Bicategory.whiskerLeft (prelaxfunctor.map f✝) (prelaxfunctor.map₂ η✝) ≫
              (Cat.Hom.isoMk (mapComp f✝.toFunctor h✝.toFunctor)).inv).toNatTrans.app
      star

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: case of
C : Type u
inst✝ : Category.{v, u} C
a✝¹ b✝ c✝ : Cat
f✝ g✝ : a✝¹ ⟶ b✝
η✝ : f✝ ⟶ g✝
h✝ : b✝ ⟶ c✝
a✝ : ↑a✝¹
⊢ h✝.toFunctor.map (η✝.toNatTrans.app a✝) = h✝.toFunctor.map (down (η✝.toNatTrans.app a✝))

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: case star
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ c✝ : Cat
f✝ g✝ : a✝ ⟶ b✝
η✝ : f✝ ⟶ g✝
h✝ : b✝ ⟶ c✝
⊢ (prelaxfunctor.map₂ (Bicategory.whiskerRight η✝ h✝)).toNatTrans.app star =
    ((Cat.Hom.isoMk (mapComp f✝.toFunctor h✝.toFunctor)).hom ≫
            Bicategory.whiskerRight (prelaxfunctor.map₂ η✝) (prelaxfunctor.map h✝) ≫
              (Cat.Hom.isoMk (mapComp g✝.toFunctor h✝.toFunctor)).inv).toNatTrans.app
      star

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
E : Cat
X✝ Y✝ Z✝ : ↑E ⥤ Cat
α : X✝ ⟶ Y✝
β : Y✝ ⟶ Z✝
⊢ Over.homMk (map α ⋙ map β).toCatHom ⋯ = Over.homMk (map α).toCatHom ⋯ ≫ Over.homMk (map β).toCatHom ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Type w
base✝¹ : C
as✝¹ : G.obj base✝¹
base✝ : C
as✝ : G.obj base✝
base : { base := base✝¹, fiber := { as := as✝¹ } }.base ⟶ { base := base✝, fiber := { as := as✝ } }.base
f :
  (((G ⋙ typeToCat).map base).toFunctor.obj { base := base✝¹, fiber := { as := as✝¹ } }.fiber).as =
    { base := base✝, fiber := { as := as✝ } }.fiber.as
⊢ { base := base, fiber := { down := { down := f } } } =
    (grothendieckTypeToCatInverse G).map
      ((grothendieckTypeToCatFunctor G).map { base := base, fiber := { down := { down := f } } })

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: case star
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ c✝ d✝ : Cat
f✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ c✝
h✝ : c✝ ⟶ d✝
⊢ (NatTrans.toCatHom₂ (map₂ (f✝.toFunctor.associator g✝.toFunctor h✝.toFunctor).hom)).toNatTrans.app star =
    (NatTrans.toCatHom₂ (mapComp (f✝.toFunctor ⋙ g✝.toFunctor) h✝.toFunctor).hom ≫
            Bicategory.whiskerRight (NatTrans.toCatHom₂ (mapComp f✝.toFunctor g✝.toFunctor).hom)
                (map h✝.toFunctor).toCatHom ≫
              (Bicategory.associator (map f✝.toFunctor).toCatHom (map g✝.toFunctor).toCatHom
                    (map h✝.toFunctor).toCatHom).hom ≫
                Bicategory.whiskerLeft (map f✝.toFunctor).toCatHom
                    (NatTrans.toCatHom₂ (mapComp g✝.toFunctor h✝.toFunctor).inv) ≫
                  NatTrans.toCatHom₂ (mapComp f✝.toFunctor (g✝.toFunctor ⋙ h✝.toFunctor)).inv).toNatTrans.app
      star

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Type w
fst✝¹ : C
snd✝¹ : G.obj fst✝¹
fst✝ : C
snd✝ : G.obj fst✝
f : ⟨fst✝¹, snd✝¹⟩.fst ⟶ ⟨fst✝, snd✝⟩.fst
e : (ConcreteCategory.hom (G.map f)) ⟨fst✝¹, snd✝¹⟩.snd = ⟨fst✝, snd✝⟩.snd
⊢ (grothendieckTypeToCatFunctor G).map ((grothendieckTypeToCatInverse G).map ⟨f, e⟩) = ⟨f, e⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Type w
base✝ : C
as✝ : G.obj base✝
⊢ (Sigma.rec (motive := fun t ↦
        (grothendieckTypeToCatFunctor G).obj { base := base✝, fiber := { as := as✝ } } = t →
          ((grothendieckTypeToCatFunctor G).obj
              ((grothendieckTypeToCatInverse G).obj
                ((grothendieckTypeToCatFunctor G).obj { base := base✝, fiber := { as := as✝ } })) ≅
            (grothendieckTypeToCatFunctor G).obj { base := base✝, fiber := { as := as✝ } }))
        (fun fst snd h ↦
          ⋯ ▸ Iso.refl ((grothendieckTypeToCatFunctor G).obj ((grothendieckTypeToCatInverse G).obj ⟨fst, snd⟩)))
        ((grothendieckTypeToCatFunctor G).obj { base := base✝, fiber := { as := as✝ } }) ⋯).hom =
    𝟙 ((grothendieckTypeToCatFunctor G).obj { base := base✝, fiber := { as := as✝ } })

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: case star
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : Cat
f✝ : a✝ ⟶ b✝
⊢ (prelaxfunctor.map₂ (Bicategory.leftUnitor f✝).hom).toNatTrans.app star =
    ((Cat.Hom.isoMk (mapComp (𝟙 a✝).toFunctor f✝.toFunctor)).hom ≫
            Bicategory.whiskerRight (Cat.Hom.isoMk (mapId ↑a✝)).hom (prelaxfunctor.map f✝) ≫
              (Bicategory.leftUnitor (prelaxfunctor.map f✝)).hom).toNatTrans.app
      star

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: case star
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : Cat
f✝ : a✝ ⟶ b✝
⊢ (prelaxfunctor.map₂ (Bicategory.rightUnitor f✝).hom).toNatTrans.app star =
    ((Cat.Hom.isoMk (mapComp f✝.toFunctor (𝟙 b✝).toFunctor)).hom ≫
            Bicategory.whiskerLeft (prelaxfunctor.map f✝) (Cat.Hom.isoMk (mapId ↑b✝)).hom ≫
              (Bicategory.rightUnitor (prelaxfunctor.map f✝)).hom).toNatTrans.app
      star

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
x : C
⊢ (match incl.obj x, star, starTerminal.from (incl.obj x) with
    | of a, of a_1, f => F.map (down f)
    | of x, star, x_1 => M x
    | star, star, x => 𝟙 Z) =
    M x

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Type w
E : Type u_1
inst✝ : Category.{v_1, u_1} E
fib : (c : C) → ↑(F.obj c) ⥤ E
hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ (F.map f).toFunctor ⋙ fib c'
c : C
⊢ fib c = (𝟙 (F.obj c)).toFunctor ⋙ fib c

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Type w
E : Type u_1
inst✝ : Category.{v_1, u_1} E
fib : (c : C) → ↑(F.obj c) ⥤ E
hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ (F.map f).toFunctor ⋙ fib c'
hom_id : ∀ (c : C), hom (𝟙 c) = eqToHom ⋯
c₁ c₂ c₃ : C
f : c₁ ⟶ c₂
g : c₂ ⟶ c₃
⊢ (F.map f).toFunctor ⋙ (F.map g).toFunctor ⋙ fib c₃ = (F.map f ≫ F.map g).toFunctor ⋙ fib c₃

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Type w
E : Type u_1
inst✝ : Category.{v_1, u_1} E
fib : (c : C) → ↑(F.obj c) ⥤ E
hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ (F.map f).toFunctor ⋙ fib c'
hom_id : ∀ (c : C), hom (𝟙 c) = eqToHom (@_proof_145 C inst✝² F E inst✝ fib c)
c₁ c₂ c₃ : C
f : c₁ ⟶ c₂
g : c₂ ⟶ c₃
⊢ (F.map f).toFunctor ⋙ (F.map g).toFunctor ⋙ fib c₃ = (F.map f ≫ F.map g).toFunctor ⋙ fib c₃

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : WithTerminal C ⥤ D
x : C
⊢ F.map (starTerminal.from (incl.obj x)) = F.map (starTerminal.from (of x))

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
x : WithTerminal C ⥤ D
x✝ : C
⊢ (mkCommaMorphism
            (NatIso.ofComponents
                (fun X ↦
                  match X with
                  | of x_1 => (Iso.refl (incl ⋙ x)).app x_1
                  | star => Iso.refl (x.obj star))
                ⋯).hom).left.app
      x✝ =
    (𝟙 (mkCommaObject x)).left.app x✝

Tactic:
rfl

Goal state after: