mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.End

Goal state before:
pp: J : Type u
inst✝⁴ : Category.{v, u} J
C : Type u'
inst✝³ : Category.{v', u'} C
F : Jᵒᵖ ⥤ J ⥤ C
inst✝² : HasEnd F
F' : Jᵒᵖ ⥤ J ⥤ C
inst✝¹ : HasEnd F'
f : F ⟶ F'
F'' : Jᵒᵖ ⥤ J ⥤ C
inst✝ : HasEnd F''
g : F' ⟶ F''
⊢ map f ≫ map g = map (f ≫ g)

Tactic:
cat_disch

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

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
C : Type u'
inst✝¹ : Category.{v', u'} C
F : Jᵒᵖ ⥤ J ⥤ C
inst✝ : HasEnd F
⊢ map (𝟙 F) = 𝟙 (end_ F)

Tactic:
cat_disch

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

Goal state before:
pp: J : Type u
inst✝⁴ : Category.{v, u} J
C : Type u'
inst✝³ : Category.{v', u'} C
F : Jᵒᵖ ⥤ J ⥤ C
inst✝² : HasCoend F
F' : Jᵒᵖ ⥤ J ⥤ C
inst✝¹ : HasCoend F'
f : F ⟶ F'
F'' : Jᵒᵖ ⥤ J ⥤ C
inst✝ : HasCoend F''
g : F' ⟶ F''
⊢ map f ≫ map g = map (f ≫ g)

Tactic:
cat_disch

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

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
C : Type u'
inst✝¹ : Category.{v', u'} C
F : Jᵒᵖ ⥤ J ⥤ C
inst✝ : HasCoend F
⊢ map (𝟙 F) = 𝟙 (coend F)

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ C
A₀ A₁ : Algebra F
f : A₀ ⟶ A₁
inst✝ : IsIso f.f
⊢ f ≫ { f := inv f.f, h := ⋯ } = 𝟙 A₀

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ C
A₀ A₁ : Algebra F
f : A₀ ⟶ A₁
inst✝ : IsIso f.f
⊢ { f := inv f.f, h := ⋯ } ≫ f = 𝟙 A₁

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ C
V₀ V₁ : Coalgebra F
f : V₀ ⟶ V₁
inst✝ : IsIso f.f
⊢ f ≫ { f := inv f.f, h := ⋯ } = 𝟙 V₀

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ C
V₀ V₁ : Coalgebra F
f : V₀ ⟶ V₁
inst✝ : IsIso f.f
⊢ { f := inv f.f, h := ⋯ } ≫ f = 𝟙 V₁

Tactic:
cat_disch

Goal state after:
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
X✝ Y✝ Z✝ : C ≌ D
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ (mkHom ((conjugateEquiv Z✝.toAdjunction X✝.toAdjunction) (asNatTrans (x✝¹ ≫ x✝)))).op.unop =
    ((mkHom ((conjugateEquiv Y✝.toAdjunction X✝.toAdjunction) (asNatTrans x✝¹))).op ≫
        (mkHom ((conjugateEquiv Z✝.toAdjunction Y✝.toAdjunction) (asNatTrans x✝))).op).unop

Tactic:
cat_disch

Goal state after:
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
X✝ Y✝ Z✝ : D ≌ C
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ (mkHom ((conjugateEquiv X✝.symm.toAdjunction Z✝.symm.toAdjunction).invFun (asNatTrans (x✝¹ ≫ x✝)))).op.unop =
    ((mkHom ((conjugateEquiv X✝.symm.toAdjunction Y✝.symm.toAdjunction).invFun (asNatTrans x✝¹))).op ≫
        (mkHom ((conjugateEquiv Y✝.symm.toAdjunction Z✝.symm.toAdjunction).invFun (asNatTrans x✝))).op).unop

Tactic:
cat_disch

Goal state after:
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 f : C ≌ D
α : e ≅ f
⊢ ((inverseFunctor C D).mapIso α.symm).unop = ((functorFunctor C D).mapIso α).isoInverseOfIsoFunctor

Tactic:
cat_disch

Goal state after:
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
        simp [← map_comp]

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

Goal state before:
pp: V : Type u₁
inst✝⁵ : Category.{v₁, u₁} V
inst✝⁴ : MonoidalCategory V
inst✝³ : BraidedCategory V
C : Type u
inst✝² : EnrichedCategory V C
D : Type u
inst✝¹ : Category.{v, u} D
inst✝ : EnrichedOrdinaryCategory V D
X✝ Y✝ Z✝ : Dᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (Quiver.Hom.opEquiv.symm.trans homEquiv) (f ≫ g) =
    (λ_ (𝟙_ V)).inv ≫
      ((Quiver.Hom.opEquiv.symm.trans homEquiv) f ⊗ₘ (Quiver.Hom.opEquiv.symm.trans homEquiv) g) ≫ eComp V X✝ Y✝ Z✝

Tactic:
by
    simp only [tensorHom_eComp_op_eq, leftUnitor_inv_braiding_assoc, ← unitors_inv_equal]
    exact homEquiv_comp g.unop f.unop

Goal state after:
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.IsHomLift f φ.hom
a' : 𝒳
g : p.obj a' ⟶ R
τ : a' ⟶ b
hτ : p.IsHomLift (g ≫ f) τ
⊢ ∀ (y : a' ⟶ a), (fun χ ↦ p.IsHomLift g χ ∧ χ ≫ φ.hom = τ) y → y = τ ≫ φ.inv

Tactic:
cat_disch

Goal state after:
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.IsHomLift f φ.hom
b' : 𝒳
g : S ⟶ p.obj b'
τ : a ⟶ b'
hτ : p.IsHomLift (f ≫ g) τ
⊢ ∀ (y : b ⟶ b'), (fun χ ↦ p.IsHomLift g χ ∧ φ.hom ≫ χ = τ) y → y = φ.inv ≫ τ

Tactic:
cat_disch

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

Goal state before:
pp: V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasFunctorEnrichedHom V F₁ F₂
inst✝ : HasFunctorEnrichedHom V F₁ F₁
⊢ (λ_ (functorEnrichedHom V F₁ F₂)).inv ≫
      functorEnrichedId V F₁ ▷ functorEnrichedHom V F₁ F₂ ≫ functorEnrichedComp V F₁ F₁ F₂ =
    𝟙 (functorEnrichedHom V F₁ F₂)

Tactic:
cat_disch

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

Goal state before:
pp: V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasFunctorEnrichedHom V F₁ F₂
inst✝ : HasFunctorEnrichedHom V F₂ F₂
⊢ (ρ_ (functorEnrichedHom V F₁ F₂)).inv ≫
      functorEnrichedHom V F₁ F₂ ◁ functorEnrichedId V F₂ ≫ functorEnrichedComp V F₁ F₂ F₂ =
    𝟙 (functorEnrichedHom V F₁ F₂)

Tactic:
cat_disch

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

Goal state before:
pp: V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ : J ⥤ C
inst✝¹ : HasFunctorEnrichedHom V F₁ F₁
inst✝ : HasEnrichedHom V F₁ F₁
⊢ (functorHomEquiv V) (𝟙 F₁) = functorEnrichedId V F₁

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck

Goal state before:
pp: 𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
a b : ↑(F.obj { as := op S })
⊢ Function.Injective (Fiber.inducedFunctor ⋯).map

Tactic:
by
    intro f g heq
    replace heq := fiberInclusion.congr_map heq
    simpa [cancel_mono, ← Cat.Hom.toNatIso_hom,
      ← Cat.Hom.toNatIso_inv] using ((Hom.ext_iff _ _).mp heq).2

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived

Goal state before:
pp: C : Type u₁
H : Type u₃
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₃, u₃} H
F : C ⥤ H
W : MorphismProperty C
hF : W.IsInvertedBy F
X : C
⊢ W.Q.HasPointwiseRightKanExtensionAt F (W.Q.obj X)

Tactic:
exact (isPointwiseRightKanExtensionOfIsoOfIsLocalization W
    (Localization.fac F hF W.Q).symm).hasPointwiseRightKanExtension _

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X A B : C
f : A ⟶ X
g : B ⟶ X
a : (F.obj A).obj
b : (F.obj B).obj
h : (ConcreteCategory.hom (F.map f)) a = (ConcreteCategory.hom (F.map g)) b
⊢ (ConcreteCategory.hom
        ((Types.pullbackIsoPullback ((cospan f g ⋙ F ⋙ FintypeCat.incl).map WalkingCospan.Hom.inl)
              ((cospan f g ⋙ F ⋙ FintypeCat.incl).map WalkingCospan.Hom.inr)).inv ≫
          ((Cone.postcomposeEquivalence (diagramIsoCospan (cospan f g ⋙ F ⋙ FintypeCat.incl))).symm.inverse.map
                ((isLimitOfPreserves (F ⋙ FintypeCat.incl) (pullbackIsPullback f g)).liftConeMorphism
                  ((Cone.postcomposeEquivalence (diagramIsoCospan (cospan f g ⋙ F ⋙ FintypeCat.incl))).symm.functor.obj
                    (limit.cone (cospan ((F ⋙ FintypeCat.incl).map f) ((F ⋙ FintypeCat.incl).map g)))))).hom ≫
            (F ⋙ FintypeCat.incl).map (pullback.snd f g)))
      ⟨(a, b), h⟩ =
    b

Tactic:
erw [PreservesPullback.iso_inv_snd, Types.pullbackIsoPullback_inv_snd]

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X A B : C
f : A ⟶ X
g : B ⟶ X
a : (F.obj A).obj
b : (F.obj B).obj
h : (ConcreteCategory.hom (F.map f)) a = (ConcreteCategory.hom (F.map g)) b
⊢ (ConcreteCategory.hom (↾fun p ↦ (↑p).2)) ⟨(a, b), h⟩ = b
Module: Mathlib.CategoryTheory.Galois.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : ¬IsIso f
⊢ Nat.card (F.obj X).obj < Nat.card (F.obj Y).obj

Tactic:
by
  by_contra hlt
  apply h
  apply isIso_of_mono_of_eq_card_fiber F f
  simp only [not_lt] at hlt
  exact Nat.le_antisymm
    (Nat.card_le_card_of_injective (F.map f) (injective_of_mono_of_preservesPullback (F.map f))) hlt

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Fan f₁
c₂ : Fan f₂
bc : BinaryFan c₁.pt c₂.pt
h₁ : IsLimit c₁
h₂ : IsLimit c₂
h : IsLimit bc
s : Fan (Sum.elim f₁ f₂)
w : ι₁ ⊕ ι₂
⊢ (IsLimit.lift h fun i ↦
        WalkingPair.casesOn (motive := fun t ↦ i = t → (s.pt ⟶ WalkingPair.casesOn i c₁.pt c₂.pt)) i
          (fun h ↦ ⋯ ▸ IsLimit.lift h₁ fun a ↦ s.proj (Sum.inl a))
          (fun h ↦ ⋯ ▸ IsLimit.lift h₂ fun a ↦ s.proj (Sum.inr a)) ⋯) ≫
      (mk bc.pt (c₁.combPairHoms c₂ bc)).proj w =
    s.proj w

Tactic:
cases w

Goal state after:
case inl
C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Fan f₁
c₂ : Fan f₂
bc : BinaryFan c₁.pt c₂.pt
h₁ : IsLimit c₁
h₂ : IsLimit c₂
h : IsLimit bc
s : Fan (Sum.elim f₁ f₂)
val✝ : ι₁
⊢ (IsLimit.lift h fun i ↦
        WalkingPair.casesOn (motive := fun t ↦ i = t → (s.pt ⟶ WalkingPair.casesOn i c₁.pt c₂.pt)) i
          (fun h ↦ ⋯ ▸ IsLimit.lift h₁ fun a ↦ s.proj (Sum.inl a))
          (fun h ↦ ⋯ ▸ IsLimit.lift h₂ fun a ↦ s.proj (Sum.inr a)) ⋯) ≫
      (mk bc.pt (c₁.combPairHoms c₂ bc)).proj (Sum.inl val✝) =
    s.proj (Sum.inl val✝)

case inr
C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Fan f₁
c₂ : Fan f₂
bc : BinaryFan c₁.pt c₂.pt
h₁ : IsLimit c₁
h₂ : IsLimit c₂
h : IsLimit bc
s : Fan (Sum.elim f₁ f₂)
val✝ : ι₂
⊢ (IsLimit.lift h fun i ↦
        WalkingPair.casesOn (motive := fun t ↦ i = t → (s.pt ⟶ WalkingPair.casesOn i c₁.pt c₂.pt)) i
          (fun h ↦ ⋯ ▸ IsLimit.lift h₁ fun a ↦ s.proj (Sum.inl a))
          (fun h ↦ ⋯ ▸ IsLimit.lift h₂ fun a ↦ s.proj (Sum.inr a)) ⋯) ≫
      (mk bc.pt (c₁.combPairHoms c₂ bc)).proj (Sum.inr val✝) =
    s.proj (Sum.inr val✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Fan f₁
c₂ : Fan f₂
bc : BinaryFan c₁.pt c₂.pt
h₁ : IsLimit c₁
h₂ : IsLimit c₂
h : IsLimit bc
s : Fan (Sum.elim f₁ f₂)
m : s.pt ⟶ (mk bc.pt (c₁.combPairHoms c₂ bc)).pt
hm : ∀ (j : ι₁ ⊕ ι₂), m ≫ (mk bc.pt (c₁.combPairHoms c₂ bc)).proj j = s.proj j
w : WalkingPair
⊢ m ≫ proj bc w =
    (IsLimit.lift h fun i ↦
        WalkingPair.casesOn (motive := fun t ↦ i = t → (s.pt ⟶ WalkingPair.casesOn i c₁.pt c₂.pt)) i
          (fun h ↦ ⋯ ▸ IsLimit.lift h₁ fun a ↦ s.proj (Sum.inl a))
          (fun h ↦ ⋯ ▸ IsLimit.lift h₂ fun a ↦ s.proj (Sum.inr a)) ⋯) ≫
      proj bc w

Tactic:
cases w

Goal state after:
case left
C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Fan f₁
c₂ : Fan f₂
bc : BinaryFan c₁.pt c₂.pt
h₁ : IsLimit c₁
h₂ : IsLimit c₂
h : IsLimit bc
s : Fan (Sum.elim f₁ f₂)
m : s.pt ⟶ (mk bc.pt (c₁.combPairHoms c₂ bc)).pt
hm : ∀ (j : ι₁ ⊕ ι₂), m ≫ (mk bc.pt (c₁.combPairHoms c₂ bc)).proj j = s.proj j
⊢ m ≫ proj bc WalkingPair.left =
    (IsLimit.lift h fun i ↦
        WalkingPair.casesOn (motive := fun t ↦ i = t → (s.pt ⟶ WalkingPair.casesOn i c₁.pt c₂.pt)) i
          (fun h ↦ ⋯ ▸ IsLimit.lift h₁ fun a ↦ s.proj (Sum.inl a))
          (fun h ↦ ⋯ ▸ IsLimit.lift h₂ fun a ↦ s.proj (Sum.inr a)) ⋯) ≫
      proj bc WalkingPair.left

case right
C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Fan f₁
c₂ : Fan f₂
bc : BinaryFan c₁.pt c₂.pt
h₁ : IsLimit c₁
h₂ : IsLimit c₂
h : IsLimit bc
s : Fan (Sum.elim f₁ f₂)
m : s.pt ⟶ (mk bc.pt (c₁.combPairHoms c₂ bc)).pt
hm : ∀ (j : ι₁ ⊕ ι₂), m ≫ (mk bc.pt (c₁.combPairHoms c₂ bc)).proj j = s.proj j
⊢ m ≫ proj bc WalkingPair.right =
    (IsLimit.lift h fun i ↦
        WalkingPair.casesOn (motive := fun t ↦ i = t → (s.pt ⟶ WalkingPair.casesOn i c₁.pt c₂.pt)) i
          (fun h ↦ ⋯ ▸ IsLimit.lift h₁ fun a ↦ s.proj (Sum.inl a))
          (fun h ↦ ⋯ ▸ IsLimit.lift h₂ fun a ↦ s.proj (Sum.inr a)) ⋯) ≫
      proj bc WalkingPair.right
Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Cofan f₁
c₂ : Cofan f₂
bc : BinaryCofan c₁.pt c₂.pt
h₁ : IsColimit c₁
h₂ : IsColimit c₂
h : IsColimit bc
s : Cofan (Sum.elim f₁ f₂)
w : ι₁ ⊕ ι₂
⊢ ((mk bc.pt (c₁.combPairHoms c₂ bc)).inj w ≫
      IsColimit.desc h fun i ↦
        WalkingPair.casesOn (motive := fun t ↦ i = t → (WalkingPair.casesOn i c₁.pt c₂.pt ⟶ s.pt)) i
          (fun h ↦ ⋯ ▸ IsColimit.desc h₁ fun a ↦ s.inj (Sum.inl a))
          (fun h ↦ ⋯ ▸ IsColimit.desc h₂ fun a ↦ s.inj (Sum.inr a)) ⋯) =
    s.inj w

Tactic:
cases w

Goal state after:
case inl
C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Cofan f₁
c₂ : Cofan f₂
bc : BinaryCofan c₁.pt c₂.pt
h₁ : IsColimit c₁
h₂ : IsColimit c₂
h : IsColimit bc
s : Cofan (Sum.elim f₁ f₂)
val✝ : ι₁
⊢ ((mk bc.pt (c₁.combPairHoms c₂ bc)).inj (Sum.inl val✝) ≫
      IsColimit.desc h fun i ↦
        WalkingPair.casesOn (motive := fun t ↦ i = t → (WalkingPair.casesOn i c₁.pt c₂.pt ⟶ s.pt)) i
          (fun h ↦ ⋯ ▸ IsColimit.desc h₁ fun a ↦ s.inj (Sum.inl a))
          (fun h ↦ ⋯ ▸ IsColimit.desc h₂ fun a ↦ s.inj (Sum.inr a)) ⋯) =
    s.inj (Sum.inl val✝)

case inr
C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Cofan f₁
c₂ : Cofan f₂
bc : BinaryCofan c₁.pt c₂.pt
h₁ : IsColimit c₁
h₂ : IsColimit c₂
h : IsColimit bc
s : Cofan (Sum.elim f₁ f₂)
val✝ : ι₂
⊢ ((mk bc.pt (c₁.combPairHoms c₂ bc)).inj (Sum.inr val✝) ≫
      IsColimit.desc h fun i ↦
        WalkingPair.casesOn (motive := fun t ↦ i = t → (WalkingPair.casesOn i c₁.pt c₂.pt ⟶ s.pt)) i
          (fun h ↦ ⋯ ▸ IsColimit.desc h₁ fun a ↦ s.inj (Sum.inl a))
          (fun h ↦ ⋯ ▸ IsColimit.desc h₂ fun a ↦ s.inj (Sum.inr a)) ⋯) =
    s.inj (Sum.inr val✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Cofan f₁
c₂ : Cofan f₂
bc : BinaryCofan c₁.pt c₂.pt
h₁ : IsColimit c₁
h₂ : IsColimit c₂
h : IsColimit bc
s : Cofan (Sum.elim f₁ f₂)
m : (mk bc.pt (c₁.combPairHoms c₂ bc)).pt ⟶ s.pt
hm : ∀ (j : ι₁ ⊕ ι₂), (mk bc.pt (c₁.combPairHoms c₂ bc)).inj j ≫ m = s.inj j
w : WalkingPair
⊢ inj bc w ≫ m =
    inj bc w ≫
      IsColimit.desc h fun i ↦
        WalkingPair.casesOn (motive := fun t ↦ i = t → (WalkingPair.casesOn i c₁.pt c₂.pt ⟶ s.pt)) i
          (fun h ↦ ⋯ ▸ IsColimit.desc h₁ fun a ↦ s.inj (Sum.inl a))
          (fun h ↦ ⋯ ▸ IsColimit.desc h₂ fun a ↦ s.inj (Sum.inr a)) ⋯

Tactic:
cases w

Goal state after:
case left
C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Cofan f₁
c₂ : Cofan f₂
bc : BinaryCofan c₁.pt c₂.pt
h₁ : IsColimit c₁
h₂ : IsColimit c₂
h : IsColimit bc
s : Cofan (Sum.elim f₁ f₂)
m : (mk bc.pt (c₁.combPairHoms c₂ bc)).pt ⟶ s.pt
hm : ∀ (j : ι₁ ⊕ ι₂), (mk bc.pt (c₁.combPairHoms c₂ bc)).inj j ≫ m = s.inj j
⊢ inj bc WalkingPair.left ≫ m =
    inj bc WalkingPair.left ≫
      IsColimit.desc h fun i ↦
        WalkingPair.casesOn (motive := fun t ↦ i = t → (WalkingPair.casesOn i c₁.pt c₂.pt ⟶ s.pt)) i
          (fun h ↦ ⋯ ▸ IsColimit.desc h₁ fun a ↦ s.inj (Sum.inl a))
          (fun h ↦ ⋯ ▸ IsColimit.desc h₂ fun a ↦ s.inj (Sum.inr a)) ⋯

case right
C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Cofan f₁
c₂ : Cofan f₂
bc : BinaryCofan c₁.pt c₂.pt
h₁ : IsColimit c₁
h₂ : IsColimit c₂
h : IsColimit bc
s : Cofan (Sum.elim f₁ f₂)
m : (mk bc.pt (c₁.combPairHoms c₂ bc)).pt ⟶ s.pt
hm : ∀ (j : ι₁ ⊕ ι₂), (mk bc.pt (c₁.combPairHoms c₂ bc)).inj j ≫ m = s.inj j
⊢ inj bc WalkingPair.right ≫ m =
    inj bc WalkingPair.right ≫
      IsColimit.desc h fun i ↦
        WalkingPair.casesOn (motive := fun t ↦ i = t → (WalkingPair.casesOn i c₁.pt c₂.pt ⟶ s.pt)) i
          (fun h ↦ ⋯ ▸ IsColimit.desc h₁ fun a ↦ s.inj (Sum.inl a))
          (fun h ↦ ⋯ ▸ IsColimit.desc h₂ fun a ↦ s.inj (Sum.inr a)) ⋯
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
inst✝⁵ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝⁴ : FiberFunctor F
X A B : C
inst✝³ : IsConnected A
inst✝² : IsConnected B
a : (F.obj A).obj
b : (F.obj B).obj
i : A ⟶ X
j : B ⟶ X
h : (ConcreteCategory.hom (F.map i)) a = (ConcreteCategory.hom (F.map j)) b
inst✝¹ : Mono i
inst✝ : Mono j
Y : C := pullback i j
u : Y ⟶ A := pullback.fst i j
v : Y ⟶ B := pullback.snd i j
G : C ⥤ Type w := F ⋙ FintypeCat.incl
e : (F.obj Y).obj ≃ { p // (ConcreteCategory.hom (F.map i)) p.1 = (ConcreteCategory.hom (F.map j)) p.2 } :=
  fiberPullbackEquiv F i j
y : (F.obj Y).obj := e.symm ⟨(a, b), h⟩
hn : ∀ (a : IsInitial Y), False
this✝ : IsIso u
this : IsIso v
⊢ ∃ f, (ConcreteCategory.hom (F.map f.hom)) a = b

Tactic:
use (asIso u).symm ≪≫ asIso v

Goal state after:
case h
C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
inst✝⁵ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝⁴ : FiberFunctor F
X A B : C
inst✝³ : IsConnected A
inst✝² : IsConnected B
a : (F.obj A).obj
b : (F.obj B).obj
i : A ⟶ X
j : B ⟶ X
h : (ConcreteCategory.hom (F.map i)) a = (ConcreteCategory.hom (F.map j)) b
inst✝¹ : Mono i
inst✝ : Mono j
Y : C := ⋯
u : Y ⟶ A := ⋯
v : Y ⟶ B := ⋯
G : C ⥤ Type w := ⋯
e : (F.obj Y).obj ≃ { p // (ConcreteCategory.hom (F.map i)) p.1 = (ConcreteCategory.hom (F.map j)) p.2 } := ⋯
y : (F.obj Y).obj := ⋯
hn : ∀ (a : IsInitial Y), False
this✝ : IsIso u
this : IsIso v
⊢ (ConcreteCategory.hom (F.map ((asIso u).symm ≪≫ asIso v).hom)) a = b
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: case h
C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
inst✝⁵ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝⁴ : FiberFunctor F
X A B : C
inst✝³ : IsConnected A
inst✝² : IsConnected B
a : (F.obj A).obj
b : (F.obj B).obj
i : A ⟶ X
j : B ⟶ X
h : (ConcreteCategory.hom (F.map i)) a = (ConcreteCategory.hom (F.map j)) b
inst✝¹ : Mono i
inst✝ : Mono j
Y : C := ⋯
u : Y ⟶ A := ⋯
v : Y ⟶ B := ⋯
G : C ⥤ Type w := ⋯
e : (F.obj Y).obj ≃ { p // (ConcreteCategory.hom (F.map i)) p.1 = (ConcreteCategory.hom (F.map j)) p.2 } := ⋯
y : (F.obj Y).obj := ⋯
hn : ∀ (a : IsInitial Y), False
this✝ : IsIso u
this : IsIso v
⊢ (ConcreteCategory.hom (F.map ((asIso u).symm ≪≫ asIso v).hom)) a = b

Tactic:
have hu : G.map u y = a := fiberPullbackEquiv_symm_fst_apply _ _ _ h

Goal state after:
case h
C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
inst✝⁵ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝⁴ : FiberFunctor F
X A B : C
inst✝³ : IsConnected A
inst✝² : IsConnected B
a : (F.obj A).obj
b : (F.obj B).obj
i : A ⟶ X
j : B ⟶ X
h : (ConcreteCategory.hom (F.map i)) a = (ConcreteCategory.hom (F.map j)) b
inst✝¹ : Mono i
inst✝ : Mono j
Y : C := pullback i j
u : Y ⟶ A := pullback.fst i j
v : Y ⟶ B := pullback.snd i j
G : C ⥤ Type w := F ⋙ FintypeCat.incl
e : (F.obj Y).obj ≃ { p // (ConcreteCategory.hom (F.map i)) p.1 = (ConcreteCategory.hom (F.map j)) p.2 } :=
  fiberPullbackEquiv F i j
y : (F.obj Y).obj := e.symm ⟨(a, b), h⟩
hn : ∀ (a : IsInitial Y), False
this✝ : IsIso u
this : IsIso v
hu : (ConcreteCategory.hom (G.map u)) y = a
⊢ (ConcreteCategory.hom (F.map ((asIso u).symm ≪≫ asIso v).hom)) a = b
Module: Mathlib.CategoryTheory.Galois.Prorepresentability

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{u₂, u₁} C
inst✝ : GaloisCategory C
F : C ⥤ FintypeCat
x✝² x✝¹ : (PointedGaloisObject F)ᵒᵖ
A : C
a : (F.obj A).obj
isGalois✝¹ : IsGalois A
B : C
b : (F.obj B).obj
isGalois✝ : IsGalois B
x✝ :
  Opposite.op { obj := A, pt := a, isGalois := isGalois✝¹ } ⟶ Opposite.op { obj := B, pt := b, isGalois := isGalois✝ }
f :
  (Opposite.unop (Opposite.op { obj := B, pt := b, isGalois := isGalois✝ })).obj ⟶
    (Opposite.unop (Opposite.op { obj := A, pt := a, isGalois := isGalois✝¹ })).obj
hf : (ConcreteCategory.hom (F.map f)) b = a
Y : C
g : A ⟶ Y
⊢ (ConcreteCategory.hom (F.map g)) ((ConcreteCategory.hom (F.map f)) b) = (ConcreteCategory.hom (F.map g)) a

Tactic:
rw [hf]

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Topology

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
a : (X : C) → Aut (F.obj X)
x✝ : ∃ y, (autEmbedding F) y = a
i : Arrow C
σ : Aut F
h : (autEmbedding F) σ = a
⊢ F.map i.hom ≫ (a i.right).hom = (a i.left).hom ≫ F.map i.hom

Tactic:
cat_disch

Goal state after: