mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.EffectiveEpi.Extensive

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : FinitaryPreExtensive C
α : Type
inst✝ : Finite α
B : C
X : α → C
π : (a : α) → X a ⟶ B
⊢ EffectiveEpi (Sigma.desc π) ↔ EffectiveEpiFamily X π

Tactic:
exact ⟨fun h ↦ ⟨⟨@effectiveEpiFamilyStructOfEffectiveEpiDesc _ _ _ _ X π _ h _ _ (fun g ↦
    (FinitaryPreExtensive.isIso_sigmaDesc_fst (fun a ↦ Sigma.ι X a) g inferInstance).epi_of_iso)⟩⟩,
    fun _ ↦ inferInstance⟩

Goal state after:
Module: Mathlib.CategoryTheory.EffectiveEpi.Coproduct

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝⁴ : HasCoproduct X
inst✝³ : EffectiveEpi (Sigma.desc π)
inst✝² : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)
inst✝¹ : ∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a ↦ pullback g (Sigma.ι X a)
inst✝ : ∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a ↦ pullback.fst g (Sigma.ι X a))
W✝ : C
x✝² : (a : α) → X a ⟶ W✝
x✝¹ : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ x✝² a₁ = g₂ ≫ x✝² a₂
x✝ : B ⟶ W✝
hm : ∀ (a : α), π a ≫ x✝ = x✝² a
⊢ Sigma.desc π ≫ x✝ = Sigma.desc x✝²

Tactic:
ext

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝⁴ : HasCoproduct X
inst✝³ : EffectiveEpi (Sigma.desc π)
inst✝² : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)
inst✝¹ : ∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a ↦ pullback g (Sigma.ι X a)
inst✝ : ∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a ↦ pullback.fst g (Sigma.ι X a))
W✝ : C
x✝² : (a : α) → X a ⟶ W✝
x✝¹ : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ x✝² a₁ = g₂ ≫ x✝² a₂
x✝ : B ⟶ W✝
hm : ∀ (a : α), π a ≫ x✝ = x✝² a
b✝ : α
⊢ Sigma.ι X b✝ ≫ Sigma.desc π ≫ x✝ = Sigma.ι X b✝ ≫ Sigma.desc x✝²
Module: Mathlib.CategoryTheory.Enriched.HomCongr

Goal state before:
pp: V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X₁ Y₁ X₂ Y₂ X₃ Y₃ : C
α₁ : X₁ ≅ X₂
β₁ : Y₁ ≅ Y₂
α₂ : X₂ ≅ X₃
β₂ : Y₂ ≅ Y₃
⊢ eHomCongr V (α₁ ≪≫ α₂) (β₁ ≪≫ β₂) = eHomCongr V α₁ β₁ ≪≫ eHomCongr V α₂ β₂

Tactic:
ext

Goal state after:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X₁ Y₁ X₂ Y₂ X₃ Y₃ : C
α₁ : X₁ ≅ X₂
β₁ : Y₁ ≅ Y₂
α₂ : X₂ ≅ X₃
β₂ : Y₂ ≅ Y₃
⊢ (eHomCongr V (α₁ ≪≫ α₂) (β₁ ≪≫ β₂)).hom = (eHomCongr V α₁ β₁ ≪≫ eHomCongr V α₂ β₂).hom
Module: Mathlib.CategoryTheory.Enriched.HomCongr

Goal state before:
pp: V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Z X₁ Y₁ Z₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
γ : Z ≅ Z₁
f : X ⟶ Y
g : Y ⟶ Z
⊢ (eHomEquiv V) (f ≫ g) ≫ (eHomCongr V α γ).hom =
    (λ_ (𝟙_ V)).inv ≫
      ((eHomEquiv V) f ≫ (eHomCongr V α β).hom) ▷ 𝟙_ V ≫
        (X₁ ⟶[V] Y₁) ◁ ((eHomEquiv V) g ≫ (eHomCongr V β γ).hom) ≫ eComp V X₁ Y₁ Z₁

Tactic:
by
  simp only [eHomCongr, MonoidalCategory.whiskerRight_id, assoc,
    MonoidalCategory.whiskerLeft_comp]
  rw [rightUnitor_inv_naturality_assoc, rightUnitor_inv_naturality_assoc,
    rightUnitor_inv_naturality_assoc, hom_inv_id_assoc, ← whisker_exchange_assoc,
    ← whisker_exchange_assoc, ← eComp_eHomWhiskerLeft, eHom_whisker_cancel_assoc,
    ← eComp_eHomWhiskerRight_assoc, ← tensorHom_def_assoc,
    ← eHomEquiv_comp_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Endofunctor.Algebra

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
A : Algebra F
⊢ (Algebra.toCoalgebraOf adj).map ((AlgCoalgEquiv.unitIso adj).hom.app A) ≫
      (AlgCoalgEquiv.counitIso adj).hom.app ((Algebra.toCoalgebraOf adj).obj A) =
    𝟙 ((Algebra.toCoalgebraOf adj).obj A)

Tactic:
ext

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
A : Algebra F
⊢ autoParam
    (((Algebra.toCoalgebraOf adj).map ((AlgCoalgEquiv.unitIso adj).hom.app A) ≫
          (AlgCoalgEquiv.counitIso adj).hom.app ((Algebra.toCoalgebraOf adj).obj A)).f =
      (𝟙 ((Algebra.toCoalgebraOf adj).obj A)).f)
    Coalgebra.ext._auto_1
Module: Mathlib.CategoryTheory.Equivalence.Symmetry

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
E : Type u_3
inst✝ : Category.{v_3, u_3} E
X✝ Y✝ Z✝ : (C ≌ D)ᵒᵖ
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ mkHom
      ((whiskeringLeft D C E).map
        ((conjugateEquiv (Opposite.unop X✝).toAdjunction (Opposite.unop Z✝).toAdjunction)
          (asNatTrans (x✝¹ ≫ x✝).unop))) =
    mkHom
        ((whiskeringLeft D C E).map
          ((conjugateEquiv (Opposite.unop X✝).toAdjunction (Opposite.unop Y✝).toAdjunction) (asNatTrans x✝¹.unop))) ≫
      mkHom
        ((whiskeringLeft D C E).map
          ((conjugateEquiv (Opposite.unop Y✝).toAdjunction (Opposite.unop Z✝).toAdjunction) (asNatTrans x✝.unop)))

Tactic:
ext

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
E : Type u_3
inst✝ : Category.{v_3, u_3} E
X✝ Y✝ Z✝ : (C ≌ D)ᵒᵖ
x✝³ : X✝ ⟶ Y✝
x✝² : Y✝ ⟶ Z✝
x✝¹ : C ⥤ E
x✝ : D
⊢ ((asNatTrans
              (mkHom
                ((whiskeringLeft D C E).map
                  ((conjugateEquiv (Opposite.unop X✝).toAdjunction (Opposite.unop Z✝).toAdjunction)
                    (asNatTrans (x✝³ ≫ x✝²).unop))))).app
          x✝¹).app
      x✝ =
    ((asNatTrans
              (mkHom
                  ((whiskeringLeft D C E).map
                    ((conjugateEquiv (Opposite.unop X✝).toAdjunction (Opposite.unop Y✝).toAdjunction)
                      (asNatTrans x✝³.unop))) ≫
                mkHom
                  ((whiskeringLeft D C E).map
                    ((conjugateEquiv (Opposite.unop Y✝).toAdjunction (Opposite.unop Z✝).toAdjunction)
                      (asNatTrans x✝².unop))))).app
          x✝¹).app
      x✝
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₂} 𝒳
inst✝¹ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝ : p.IsHomLift f φ
⊢ p.obj a = R

Tactic:
subst_hom_lift p f φ

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₂} 𝒳
inst✝¹ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝ : p.IsHomLift (p.map φ) φ
⊢ p.obj a✝ = p.obj a✝
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₂} 𝒳
inst✝¹ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝ : p.IsHomLift f φ
⊢ p.obj b = S

Tactic:
subst_hom_lift p f φ

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₂} 𝒳
inst✝¹ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝ : p.IsHomLift (p.map φ) φ
⊢ p.obj b✝ = p.obj b✝
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₂} 𝒳
inst✝¹ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝ : p.IsHomLift f φ
⊢ f = eqToHom ⋯ ≫ p.map φ ≫ eqToHom ⋯

Tactic:
subst_hom_lift p f φ

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₂} 𝒳
inst✝¹ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝ : p.IsHomLift (p.map φ) φ
⊢ p.map φ = eqToHom ⋯ ≫ p.map φ ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₂} 𝒳
inst✝¹ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝ : p.IsHomLift f φ
⊢ p.map φ = eqToHom ⋯ ≫ f ≫ eqToHom ⋯

Tactic:
subst_hom_lift p f φ

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₂} 𝒳
inst✝¹ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝ : p.IsHomLift (p.map φ) φ
⊢ p.map φ = eqToHom ⋯ ≫ p.map φ ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝ : p.IsCartesian f φ
⊢ IsCartesian.map p f φ φ = 𝟙 a

Tactic:
subst_hom_lift p f φ

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝ : p.IsCartesian (p.map φ) φ
⊢ IsCartesian.map p (p.map φ) φ φ = 𝟙 a✝
Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝¹ : p.IsCartesian f φ
a' : 𝒳
φ' : a' ⟶ b
inst✝ : p.IsCartesian f φ'
⊢ IsCartesian.map p f φ' φ ≫ IsCartesian.map p f φ φ' = 𝟙 a

Tactic:
subst_hom_lift p f φ

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
a' : 𝒳
φ' : a' ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝¹ : p.IsCartesian (p.map φ) φ
inst✝ : p.IsCartesian (p.map φ) φ'
⊢ IsCartesian.map p (p.map φ) φ' φ ≫ IsCartesian.map p (p.map φ) φ φ' = 𝟙 a✝
Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝ : p.IsStronglyCartesian f φ
⊢ map p f φ ⋯ φ = 𝟙 a

Tactic:
subst_hom_lift p f φ

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝ : p.IsStronglyCartesian (p.map φ) φ
⊢ map p (p.map φ) φ ⋯ φ = 𝟙 a✝
Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F G : 𝒳 ⥤ᵇ 𝒴
α : F ⟶ G
x✝ : IsIso ((forgetful 𝒳 𝒴).map α)
⊢ IsIso α

Tactic:
constructor

Goal state after:
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F G : 𝒳 ⥤ᵇ 𝒴
α : F ⟶ G
x✝ : IsIso ((forgetful 𝒳 𝒴).map α)
⊢ ∃ inv, α ≫ inv = 𝟙 F ∧ inv ≫ α = 𝟙 G
Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝¹ : p.IsStronglyCartesian f φ
inst✝ : IsIso f
⊢ IsIso φ

Tactic:
subst_hom_lift p f φ

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝¹ : p.IsStronglyCartesian (p.map φ) φ
inst✝ : IsIso (p.map φ)
⊢ IsIso φ
Module: Mathlib.CategoryTheory.FiberedCategory.Fibered

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ b φ, p.IsStronglyCartesian f φ
R S : 𝒮
f : R ⟶ S
a b : 𝒳
φ : a ⟶ b
inst✝ : p.IsCartesian f φ
⊢ p.IsStronglyCartesian f φ

Tactic:
constructor

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ b φ, p.IsStronglyCartesian f φ
R S : 𝒮
f : R ⟶ S
a b : 𝒳
φ : a ⟶ b
inst✝ : p.IsCartesian f φ
⊢ ∀ {a' : 𝒳} (g : p.obj a' ⟶ R) (φ' : a' ⟶ b) [p.IsHomLift (g ≫ f) φ'], ∃! χ, p.IsHomLift g χ ∧ χ ≫ φ = φ'
Module: Mathlib.CategoryTheory.FiberedCategory.Fibered

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ b φ, p.IsStronglyCartesian f φ
R S : 𝒮
f : R ⟶ S
a b : 𝒳
φ : a ⟶ b
inst✝ : p.IsCartesian f φ
c : 𝒳
g : p.obj c ⟶ R
φ' : c ⟶ b
hφ' : p.IsHomLift (g ≫ f) φ'
⊢ ∃! χ, p.IsHomLift g χ ∧ χ ≫ φ = φ'

Tactic:
subst_hom_lift p f φ

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ b φ, p.IsStronglyCartesian f φ
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
c : 𝒳
φ' : c ⟶ b✝
R S : 𝒮
a b : 𝒳
g : p.obj c ⟶ p.obj a✝
inst✝ : p.IsCartesian (p.map φ) φ
hφ' : p.IsHomLift (g ≫ p.map φ) φ'
⊢ ∃! χ, p.IsHomLift g χ ∧ χ ≫ φ = φ'
Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝ : p.IsCocartesian f φ
⊢ IsCocartesian.map p f φ φ = 𝟙 b

Tactic:
subst_hom_lift p f φ

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝ : p.IsCocartesian (p.map φ) φ
⊢ IsCocartesian.map p (p.map φ) φ φ = 𝟙 b✝
Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝¹ : p.IsCocartesian f φ
b' : 𝒳
φ' : a ⟶ b'
inst✝ : p.IsCocartesian f φ'
⊢ IsCocartesian.map p f φ φ' ≫ IsCocartesian.map p f φ' φ = 𝟙 b

Tactic:
subst_hom_lift p f φ

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
b' : 𝒳
φ' : a✝ ⟶ b'
R S : 𝒮
a b : 𝒳
inst✝¹ : p.IsCocartesian (p.map φ) φ
inst✝ : p.IsCocartesian (p.map φ) φ'
⊢ IsCocartesian.map p (p.map φ) φ φ' ≫ IsCocartesian.map p (p.map φ) φ' φ = 𝟙 b✝
Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝ : p.IsStronglyCocartesian f φ
⊢ map p f φ ⋯ φ = 𝟙 b

Tactic:
subst_hom_lift p f φ

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝ : p.IsStronglyCocartesian (p.map φ) φ
⊢ map p (p.map φ) φ ⋯ φ = 𝟙 b✝
Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝¹ : p.IsStronglyCocartesian f φ
inst✝ : IsIso f
⊢ IsIso φ

Tactic:
subst_hom_lift p f φ

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝¹ : p.IsStronglyCocartesian (p.map φ) φ
inst✝ : IsIso (p.map φ)
⊢ IsIso φ
Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck

Goal state before:
pp: case refine_2
𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
R S : 𝒮
a : ↑(F.obj { as := op S })
f : R ⟶ S
a' : ∫ᶜ F
χ' : a' ⟶ domainCartesianLift a f
hχ'.symm : (forget F).IsHomLift χ'.base χ'
hφ' : (forget F).IsHomLift (χ'.base ≫ f) (χ' ≫ cartesianLift a f)
⊢ χ' = homCartesianLift f χ'.base (χ' ≫ cartesianLift a f)

Tactic:
ext

Goal state after:
case refine_2.hfg₁
𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
R S : 𝒮
a : ↑(F.obj { as := op S })
f : R ⟶ S
a' : ∫ᶜ F
χ' : a' ⟶ domainCartesianLift a f
hχ'.symm : (forget F).IsHomLift χ'.base χ'
hφ' : (forget F).IsHomLift (χ'.base ≫ f) (χ' ≫ cartesianLift a f)
⊢ χ'.base = (homCartesianLift f χ'.base (χ' ≫ cartesianLift a f)).base

case hfg₂
𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
R S : 𝒮
a : ↑(F.obj { as := op S })
f : R ⟶ S
a' : ∫ᶜ F
χ' : a' ⟶ domainCartesianLift a f
hχ'.symm : (forget F).IsHomLift χ'.base χ'
hφ' : (forget F).IsHomLift (χ'.base ≫ f) (χ' ≫ cartesianLift a f)
⊢ χ'.fiber = (homCartesianLift f χ'.base (χ' ≫ cartesianLift a f)).fiber ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck

Goal state before:
pp: 𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
a b c : ↑(F.obj { as := op S })
φ : a ⟶ b
ψ : b ⟶ c
⊢ { base := 𝟙 S, fiber := (φ ≫ ψ) ≫ (F.mapId { as := op S }).inv.toNatTrans.app c } =
    { base := 𝟙 S, fiber := φ ≫ (F.mapId { as := op S }).inv.toNatTrans.app b } ≫
      { base := 𝟙 S, fiber := ψ ≫ (F.mapId { as := op S }).inv.toNatTrans.app c }

Tactic:
ext

Goal state after:
case hfg₁
𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
a b c : ↑(F.obj { as := op S })
φ : a ⟶ b
ψ : b ⟶ c
⊢ { base := 𝟙 S, fiber := (φ ≫ ψ) ≫ (F.mapId { as := op S }).inv.toNatTrans.app c }.base =
    ({ base := 𝟙 S, fiber := φ ≫ (F.mapId { as := op S }).inv.toNatTrans.app b } ≫
        { base := 𝟙 S, fiber := ψ ≫ (F.mapId { as := op S }).inv.toNatTrans.app c }).base

case hfg₂
𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
a b c : ↑(F.obj { as := op S })
φ : a ⟶ b
ψ : b ⟶ c
⊢ { base := 𝟙 S, fiber := (φ ≫ ψ) ≫ (F.mapId { as := op S }).inv.toNatTrans.app c }.fiber =
    ({ base := 𝟙 S, fiber := φ ≫ (F.mapId { as := op S }).inv.toNatTrans.app b } ≫
          { base := 𝟙 S, fiber := ψ ≫ (F.mapId { as := op S }).inv.toNatTrans.app c }).fiber ≫
      eqToHom ⋯
Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck

Goal state before:
pp: case h
𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
X Y : ↑(F.obj { as := op S })
f : (Fiber.inducedFunctor ⋯).obj X ⟶ (Fiber.inducedFunctor ⋯).obj Y
hf : (fiberInclusion.map f).base = 𝟙 S
⊢ (Fiber.inducedFunctor ⋯).map
      ((fiberInclusion.map f).fiber ≫ eqToHom ⋯ ≫ (F.mapId { as := op S }).hom.toNatTrans.app Y) =
    f

Tactic:
ext

Goal state after:
case h.hfg₁
𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
X Y : ↑(F.obj { as := op S })
f : (Fiber.inducedFunctor ⋯).obj X ⟶ (Fiber.inducedFunctor ⋯).obj Y
hf : (fiberInclusion.map f).base = 𝟙 S
⊢ (fiberInclusion.map
        ((Fiber.inducedFunctor ⋯).map
          ((fiberInclusion.map f).fiber ≫ eqToHom ⋯ ≫ (F.mapId { as := op S }).hom.toNatTrans.app Y))).base =
    (fiberInclusion.map f).base

case hfg₂
𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
X Y : ↑(F.obj { as := op S })
f : (Fiber.inducedFunctor ⋯).obj X ⟶ (Fiber.inducedFunctor ⋯).obj Y
hf : (fiberInclusion.map f).base = 𝟙 S
⊢ (fiberInclusion.map
        ((Fiber.inducedFunctor ⋯).map
          ((fiberInclusion.map f).fiber ≫ eqToHom ⋯ ≫ (F.mapId { as := op S }).hom.toNatTrans.app Y))).fiber =
    (fiberInclusion.map f).fiber ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Limits.Preserves.Grothendieck

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
H : Type u₂
inst✝⁶ : Category.{v₂, u₂} H
J : Type u₃
inst✝⁵ : Category.{v₃, u₃} J
F : C ⥤ Cat
inst✝⁴ : HasColimitsOfShape C H
inst✝³ : HasLimitsOfShape J H
inst✝² : ∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H
inst✝¹ : PreservesLimitsOfShape J colim
inst✝ : ∀ (c : C), PreservesLimitsOfShape J colim
⊢ PreservesLimitsOfShape J colim

Tactic:
constructor

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
H : Type u₂
inst✝⁶ : Category.{v₂, u₂} H
J : Type u₃
inst✝⁵ : Category.{v₃, u₃} J
F : C ⥤ Cat
inst✝⁴ : HasColimitsOfShape C H
inst✝³ : HasLimitsOfShape J H
inst✝² : ∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H
inst✝¹ : PreservesLimitsOfShape J colim
inst✝ : ∀ (c : C), PreservesLimitsOfShape J colim
⊢ autoParam (∀ {K : J ⥤ Grothendieck F ⥤ H}, PreservesLimit K colim) PreservesLimitsOfShape.preservesLimit._autoParam
Module: Mathlib.CategoryTheory.Limits.Preserves.Grothendieck

Goal state before:
pp: case e'_5
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
H : Type u₂
inst✝⁶ : Category.{v₂, u₂} H
J : Type u₃
inst✝⁵ : Category.{v₃, u₃} J
F : C ⥤ Cat
inst✝⁴ : HasColimitsOfShape C H
inst✝³ : HasLimitsOfShape J H
inst✝² : ∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H
inst✝¹ : PreservesLimitsOfShape J colim
inst✝ : ∀ (c : C), PreservesLimitsOfShape J colim
K : J ⥤ Grothendieck F ⥤ H
i₂ : colimit (limit K) ≅ limit (K ⋙ colim) := ⋯
e_3✝ : colim.obj (limit K) = colimit (limit K)
⊢ limit.post K colim = i₂.hom

Tactic:
ext

Goal state after:
case e'_5
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
H : Type u₂
inst✝⁶ : Category.{v₂, u₂} H
J : Type u₃
inst✝⁵ : Category.{v₃, u₃} J
F : C ⥤ Cat
inst✝⁴ : HasColimitsOfShape C H
inst✝³ : HasLimitsOfShape J H
inst✝² : ∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H
inst✝¹ : PreservesLimitsOfShape J colim
inst✝ : ∀ (c : C), PreservesLimitsOfShape J colim
K : J ⥤ Grothendieck F ⥤ H
i₂ : colimit (limit K) ≅ limit (K ⋙ colim) :=
  Trans.trans
    (Trans.trans
      (Trans.trans (Trans.trans ⋯ (colimitFiberwiseColimitIso (limit K)).symm)
        (HasColimit.isoOfNatIso (fiberwiseColimitLimitIso K)))
      (preservesLimitIso colim (K ⋙ fiberwiseColim F H)))
    (HasLimit.isoOfNatIso (K.associator (fiberwiseColim F H) colim ≪≫ K.isoWhiskerLeft fiberwiseColimCompColimIso))
e_3✝ : colim.obj (limit K) = colimit (limit K)
j✝ : J
⊢ limit.post K colim ≫ limit.π (K ⋙ colim) j✝ = i₂.hom ≫ limit.π (K ⋙ colim) j✝
Module: Mathlib.CategoryTheory.Limits.Preserves.Grothendieck

Goal state before:
pp: case e'_5
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
H : Type u₂
inst✝⁶ : Category.{v₂, u₂} H
J : Type u₃
inst✝⁵ : Category.{v₃, u₃} J
F : C ⥤ Cat
inst✝⁴ : HasColimitsOfShape C H
inst✝³ : HasLimitsOfShape J H
inst✝² : ∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H
inst✝¹ : PreservesLimitsOfShape J colim
inst✝ : ∀ (c : C), PreservesLimitsOfShape J colim
K : J ⥤ Grothendieck F ⥤ H
i₂ : colimit (limit K) ≅ limit (K ⋙ colim) :=
  Trans.trans
    (Trans.trans
      (Trans.trans (Trans.trans ⋯ (colimitFiberwiseColimitIso (limit K)).symm)
        (HasColimit.isoOfNatIso (fiberwiseColimitLimitIso K)))
      (preservesLimitIso colim (K ⋙ fiberwiseColim F H)))
    (HasLimit.isoOfNatIso (K.associator (fiberwiseColim F H) colim ≪≫ K.isoWhiskerLeft fiberwiseColimCompColimIso))
e_3✝ : colim.obj (limit K) = colimit (limit K)
j✝ : J
⊢ colimMap (limit.π K j✝) =
    (Trans.trans ⋯ (colimitFiberwiseColimitIso (limit K)).symm).hom ≫
      (HasColimit.isoOfNatIso (fiberwiseColimitLimitIso K)).hom ≫
        colimMap (limit.π (K ⋙ fiberwiseColim F H) j✝) ≫ (colimitFiberwiseColimitIso (K.obj j✝)).hom

Tactic:
ext

Goal state after:
case e'_5
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
H : Type u₂
inst✝⁶ : Category.{v₂, u₂} H
J : Type u₃
inst✝⁵ : Category.{v₃, u₃} J
F : C ⥤ Cat
inst✝⁴ : HasColimitsOfShape C H
inst✝³ : HasLimitsOfShape J H
inst✝² : ∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H
inst✝¹ : PreservesLimitsOfShape J colim
inst✝ : ∀ (c : C), PreservesLimitsOfShape J colim
K : J ⥤ Grothendieck F ⥤ H
i₂ : colimit (limit K) ≅ limit (K ⋙ colim) :=
  Trans.trans
    (Trans.trans
      (Trans.trans (Trans.trans ⋯ (colimitFiberwiseColimitIso (limit K)).symm)
        (HasColimit.isoOfNatIso (fiberwiseColimitLimitIso K)))
      (preservesLimitIso colim (K ⋙ fiberwiseColim F H)))
    (HasLimit.isoOfNatIso (K.associator (fiberwiseColim F H) colim ≪≫ K.isoWhiskerLeft fiberwiseColimCompColimIso))
e_3✝ : colim.obj (limit K) = colimit (limit K)
j✝¹ : J
j✝ : Grothendieck F
⊢ colimit.ι (limit K) j✝ ≫ colimMap (limit.π K j✝¹) =
    colimit.ι (limit K) j✝ ≫
      (Trans.trans ⋯ (colimitFiberwiseColimitIso (limit K)).symm).hom ≫
        (HasColimit.isoOfNatIso (fiberwiseColimitLimitIso K)).hom ≫
          colimMap (limit.π (K ⋙ fiberwiseColim F H) j✝¹) ≫ (colimitFiberwiseColimitIso (K.obj j✝¹)).hom
Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck

Goal state before:
pp: case h
𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
Y : (forget F).Fiber S
hYS : (fiberInclusion.obj Y).base = S
⊢ fiberInclusion.obj ((Fiber.inducedFunctor ⋯).obj (hYS ▸ (fiberInclusion.obj Y).fiber)) = fiberInclusion.obj Y

Tactic:
ext

Goal state after:
case h.base
𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
Y : (forget F).Fiber S
hYS : (fiberInclusion.obj Y).base = S
⊢ (fiberInclusion.obj ((Fiber.inducedFunctor ⋯).obj (hYS ▸ (fiberInclusion.obj Y).fiber))).base =
    (fiberInclusion.obj Y).base

case h.fiber
𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
Y : (forget F).Fiber S
hYS : (fiberInclusion.obj Y).base = S
⊢ (fiberInclusion.obj ((Fiber.inducedFunctor ⋯).obj (hYS ▸ (fiberInclusion.obj Y).fiber))).fiber ≍
    (fiberInclusion.obj Y).fiber