mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst✝² : ChosenPullbacksAlong g
Y' Z' X' Y'' Z'' X'' : C
f' : Y' ⟶ X'
g' : Z' ⟶ X'
f'' : Y'' ⟶ X''
g'' : Z'' ⟶ X''
inst✝¹ : ChosenPullbacksAlong g'
inst✝ : ChosenPullbacksAlong g''
γ₁ : Y' ⟶ Y
γ₂ : Z' ⟶ Z
γ₃ : X' ⟶ X
δ₁ : Y'' ⟶ Y'
δ₂ : Z'' ⟶ Z'
δ₃ : X'' ⟶ X'
comm₁ : autoParam (f' ≫ γ₃ = γ₁ ≫ f) pullbackMap_comp._auto_1
comm₂ : autoParam (g' ≫ γ₃ = γ₂ ≫ g) pullbackMap_comp._auto_3
comm₁' : autoParam (f'' ≫ δ₃ = δ₁ ≫ f') pullbackMap_comp._auto_5
comm₂' : autoParam (g'' ≫ δ₃ = δ₂ ≫ g') pullbackMap_comp._auto_7
⊢ g'' ≫ δ₃ ≫ γ₃ = (δ₂ ≫ γ₂) ≫ g

Tactic:
reassoc_of% comm₂',

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst✝² : ChosenPullbacksAlong g
Y' Z' X' Y'' Z'' X'' : C
f' : Y' ⟶ X'
g' : Z' ⟶ X'
f'' : Y'' ⟶ X''
g'' : Z'' ⟶ X''
inst✝¹ : ChosenPullbacksAlong g'
inst✝ : ChosenPullbacksAlong g''
γ₁ : Y' ⟶ Y
γ₂ : Z' ⟶ Z
γ₃ : X' ⟶ X
δ₁ : Y'' ⟶ Y'
δ₂ : Z'' ⟶ Z'
δ₃ : X'' ⟶ X'
comm₁ : autoParam (f' ≫ γ₃ = γ₁ ≫ f) pullbackMap_comp._auto_1
comm₂ : autoParam (g' ≫ γ₃ = γ₂ ≫ g) pullbackMap_comp._auto_3
comm₁' : autoParam (f'' ≫ δ₃ = δ₁ ≫ f') pullbackMap_comp._auto_5
comm₂' : autoParam (g'' ≫ δ₃ = δ₂ ≫ g') pullbackMap_comp._auto_7
⊢ δ₂ ≫ g' ≫ γ₃ = (δ₂ ≫ γ₂) ≫ g
Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F G : 𝒳 ⥤ᵇ 𝒴
α β : BasedNatTrans F G
h : α.toNatTrans = β.toNatTrans
⊢ α = β

Tactic:
cases α; subst h; rfl

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

Goal state before:
pp: G : Type u
inst✝ : Group G
⊢ PreservesFiniteLimits (forget (Action FintypeCat G))

Tactic:
change PreservesFiniteLimits (Action.forget FintypeCat _ ⋙ FintypeCat.incl)

Goal state after:
G : Type u
inst✝ : Group G
⊢ PreservesFiniteLimits (Action.forget FintypeCat G ⋙ FintypeCat.incl)
Module: Mathlib.CategoryTheory.Galois.Examples

Goal state before:
pp: G : Type u
inst✝¹ : Group G
X : Action FintypeCat G
inst✝ : IsConnected X
x y : X.V.obj
T : Set X.V.obj := MulAction.orbit G x
this : Fintype ↑T
⊢ ∃ g, g • x = y

Tactic:
let : MulAction G (FintypeCat.of T) := inferInstanceAs <| MulAction G
      ↑(MulAction.orbit G x)

Goal state after:
G : Type u
inst✝¹ : Group G
X : Action FintypeCat G
inst✝ : IsConnected X
x y : X.V.obj
T : Set X.V.obj := MulAction.orbit G x
this✝ : Fintype ↑T
this : MulAction G (FintypeCat.of ↑T).obj :=
  { toSemigroupAction := MulAction.instElemOrbit.toSemigroupAction, one_smul := ⋯ }
⊢ ∃ g, g • x = y
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
e : (F.obj (X ⨿ Y)).obj ≃ (F.obj X).obj ⊕ (F.obj Y).obj :=
  ((PreservesColimitPair.iso (F ⋙ FintypeCat.incl) X Y).symm ≪≫
      Types.binaryCoproductIso (FintypeCat.incl.obj (F.obj X)) (FintypeCat.incl.obj (F.obj Y))).toEquiv
⊢ Nat.card (F.obj (X ⨿ Y)).obj = Nat.card (F.obj X).obj + Nat.card (F.obj Y).obj

Tactic:
← Nat.card_sum

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X Y : C
e : (F.obj (X ⨿ Y)).obj ≃ (F.obj X).obj ⊕ (F.obj Y).obj :=
  ((PreservesColimitPair.iso (F ⋙ FintypeCat.incl) X Y).symm ≪≫
      Types.binaryCoproductIso (FintypeCat.incl.obj (F.obj X)) (FintypeCat.incl.obj (F.obj Y))).toEquiv
⊢ Nat.card (F.obj (X ⨿ Y)).obj = Nat.card ((F.obj X).obj ⊕ (F.obj Y).obj)
Module: Mathlib.CategoryTheory.Galois.Equivalence

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
F' : C ⥤ FintypeCat := F ⋙ FintypeCat.uSwitch
this✝ : FiberFunctor F' := FiberFunctor.comp_right FintypeCat.uSwitch
this : (functorToContAction F').EssSurj
f : Aut F ≃ₜ* Aut F' := autEquivAutWhiskerRight F FintypeCat.uSwitchEquivalence.fullyFaithfulFunctor
⊢ (functorToContAction F).EssSurj

Tactic:
let equiv : ContAction FintypeCat.{u₁} (Aut F') ≌ ContAction FintypeCat.{w} (Aut F) :=
    (FintypeCat.uSwitchEquivalence.{u₁, w}.mapContAction (Aut F')
       (fun X ↦ by
          rw [Action.isContinuous_def]
          change Continuous ((fun p ↦ (FintypeCat.uSwitchEquiv X.obj.V).symm p) ∘
              (fun p : Aut F' × _ ↦ (X.obj.ρ p.1).hom p.2) ∘
              (fun p : Aut F' × _ ↦ (p.1, FintypeCat.uSwitchEquiv _ p.2)))
          exact Continuous.comp (by fun_prop) (Continuous.comp X.2.1 (by fun_prop)))
       (fun X ↦ by
          rw [Action.isContinuous_def]
          change Continuous ((fun p ↦ (FintypeCat.uSwitchEquiv X.obj.V).symm p) ∘
              (fun p : Aut F' × _ ↦ (X.obj.ρ p.1).hom p.2) ∘
              (fun p : Aut F' × _ ↦ (p.1, FintypeCat.uSwitchEquiv _ p.2)))
          exact Continuous.comp (by fun_prop) (Continuous.comp X.2.1 (by fun_prop)))).trans <|
      ContAction.resEquiv _ f

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
F' : C ⥤ FintypeCat := F ⋙ FintypeCat.uSwitch
this✝ : FiberFunctor F' := FiberFunctor.comp_right FintypeCat.uSwitch
this : (functorToContAction F').EssSurj
f : Aut F ≃ₜ* Aut F' := autEquivAutWhiskerRight F FintypeCat.uSwitchEquivalence.fullyFaithfulFunctor
equiv : ContAction FintypeCat (Aut F') ≌ ContAction FintypeCat (Aut F) :=
  (Equivalence.mapContAction (Aut F') FintypeCat.uSwitchEquivalence ⋯ ⋯).trans (ContAction.resEquiv FintypeCat f)
⊢ (functorToContAction F).EssSurj
Module: Mathlib.CategoryTheory.Galois.Prorepresentability

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X✝ : C
inst✝ : IsConnected X✝
x y : (F.obj X✝).obj
F' : C ⥤ FintypeCat := F ⋙ FintypeCat.uSwitch
this : FiberFunctor F' := comp_right FintypeCat.uSwitch
e : (Y : C) → (F'.obj Y).obj ≃ (F.obj Y).obj := fun Y ↦ (F.obj Y).uSwitchEquiv
x' : (F'.obj X✝).obj := (e X✝).symm x
hx' : x' = (e X✝).symm x
y' : (F'.obj X✝).obj := (e X✝).symm y
hy' : y' = (e X✝).symm y
g' : Aut F'
hg' : (ConcreteCategory.hom (g'.hom.app X✝)) x' = y'
gapp : (Y : C) → F.obj Y ≅ F.obj Y :=
  fun Y ↦ FintypeCat.equivEquivIso ((e Y).symm.trans ((FintypeCat.equivEquivIso.symm (Iso.app g' Y)).trans (e Y)))
X Y : C
f : X ⟶ Y
⊢ F.map f ≫ (gapp Y).hom = (gapp X).hom ≫ F.map f

Tactic:
ext x
      dsimp [gapp, e]
      erw [FintypeCat.uSwitchEquiv_naturality (F.map f)]
      rw [← Functor.comp_map]
      erw [← NatTrans.naturality_apply, FintypeCat.uSwitchEquiv_symm_naturality (F.map f)]
      rfl

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

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : (X : C) → MulAction G (F.obj X).obj
inst✝⁴ : IsNaturalSMul F G
inst✝³ : GaloisCategory C
inst✝² : FiberFunctor F
t : Aut F
ι : Type u_2
inst✝¹ : Finite ι
X : ι → C
inst✝ : ∀ (i : ι), IsGalois (X i)
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
⊢ ∃ g, ∀ (i : ι) (x : (F.obj (X i)).obj), g • x = (ConcreteCategory.hom (t.hom.app (X i))) x

Tactic:
let x (i : ι) : F.obj (X i) := (nonempty_fiber_of_isConnected F (X i)).some

Goal state after:
C : Type u₁
inst✝⁷ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : (X : C) → MulAction G (F.obj X).obj
inst✝⁴ : IsNaturalSMul F G
inst✝³ : GaloisCategory C
inst✝² : FiberFunctor F
t : Aut F
ι : Type u_2
inst✝¹ : Finite ι
X : ι → C
inst✝ : ∀ (i : ι), IsGalois (X i)
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
x : (i : ι) → (F.obj (X i)).obj := fun i ↦ ⋯.some
⊢ ∃ g, ∀ (i : ι) (x : (F.obj (X i)).obj), g • x = (ConcreteCategory.hom (t.hom.app (X i))) x
Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup

Goal state before:
pp: case hst
C : Type u₁
inst✝⁹ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : (X : C) → MulAction G (F.obj X).obj
inst✝⁶ : IsNaturalSMul F G
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj), gi X • x = (ConcreteCategory.hom (t.hom.app X.obj)) x
cl : PointedGaloisObject F → Set G := fun X ↦ gi X • ↑(MulAction.stabilizer G X.pt)
c : Set G := ⋂ i, cl i
s : Finset (PointedGaloisObject F)
⊢ (⋂ i ∈ s, cl i).Nonempty

Tactic:
obtain ⟨gs, hgs⟩ :=
        toAut_surjective_isGalois_finite_family F G t (fun X : s ↦ X.val.obj) h

Goal state after:
case hst
C : Type u₁
inst✝⁹ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : (X : C) → MulAction G (F.obj X).obj
inst✝⁶ : IsNaturalSMul F G
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj), gi X • x = (ConcreteCategory.hom (t.hom.app X.obj)) x
cl : PointedGaloisObject F → Set G := fun X ↦ gi X • ↑(MulAction.stabilizer G X.pt)
c : Set G := ⋂ i, cl i
s : Finset (PointedGaloisObject F)
gs : G
hgs : ∀ (i : ↥s) (x : (F.obj (↑i).obj).obj), gs • x = (ConcreteCategory.hom (t.hom.app (↑i).obj)) x
⊢ (⋂ i ∈ s, cl i).Nonempty
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
G : Type u₁
inst✝ : Groupoid G
φ : C ⥤ G
Φ : FreeGroupoid C ⥤ G
hΦ : of C ⋙ Φ = φ
⊢ Φ = lift φ

Tactic:
by
  apply Quotient.lift_unique
  apply Quiver.FreeGroupoid.lift_unique
  exact congr_arg Functor.toPrefunctor hΦ

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
d : D
⊢ 𝟙 d ∈ (map φ hφ S).arrows d d

Tactic:
obtain ⟨c, rfl⟩ := obj_surjective_of_im_eq_top φ hφ hφ' d

Goal state after:
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
c : C
⊢ 𝟙 (φ.obj c) ∈ (map φ hφ S).arrows (φ.obj c) (φ.obj c)
Module: Mathlib.CategoryTheory.Limits.Final.ParallelPair

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty (X ⟶ Z)
h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), Zigzag (mk i) (mk j)
Z : C
this : Nonempty (CostructuredArrow (parallelPair f g) Z)
⊢ ∀ (x : CostructuredArrow (parallelPair f g) Z), Zigzag x (mk ⋯.some)

Tactic:
rintro ⟨(_ | _), ⟨⟩, φ⟩

Goal state after:
case zero
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty (X ⟶ Z)
h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), Zigzag (mk i) (mk j)
Z : C
this : Nonempty (CostructuredArrow (parallelPair f g) Z)
as✝ : PUnit.{1}
φ : (parallelPair f g).obj zero ⟶ (Functor.fromPUnit Z).obj { as := as✝ }
⊢ Zigzag { left := zero, right := { as := as✝ }, hom := φ } (mk ⋯.some)

case one
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty (X ⟶ Z)
h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), Zigzag (mk i) (mk j)
Z : C
this : Nonempty (CostructuredArrow (parallelPair f g) Z)
as✝ : PUnit.{1}
φ : (parallelPair f g).obj one ⟶ (Functor.fromPUnit Z).obj { as := as✝ }
⊢ Zigzag { left := one, right := { as := as✝ }, hom := φ } (mk ⋯.some)
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech

Goal state before:
pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
U : FormalCoproduct C
α : Type
inst✝ : HasProductsOfShape α C
s : Fan fun x ↦ U
φ : (i : s.pt.I) → s.pt.obj i ⟶ (U.powerFan α).pt.obj ((fun i a ↦ (s.proj a).f i) i)
i : s.pt.I
a : α
hm :
  ∃ (h₁ : ({ f := fun i a ↦ (s.proj a).f i, φ := φ } ≫ (U.powerFan α).proj a).f = (s.proj a).f),
    ∀ (i : s.pt.I), ({ f := fun i a ↦ (s.proj a).f i, φ := φ } ≫ (U.powerFan α).proj a).φ i ≫ eqToHom ⋯ = (s.proj a).φ i
⊢ (φ i ≫ 𝟙 (∏ᶜ U.obj ∘ fun a ↦ (s.proj a).f i)) ≫ Pi.π (U.obj ∘ fun a ↦ (s.proj a).f i) a =
    (Pi.lift fun a ↦ (s.proj a).φ i) ≫ Pi.π (U.obj ∘ fun a ↦ (s.proj a).f i) a

Tactic:
obtain ⟨_, hm⟩ := hm

Goal state after:
case h₂
C : Type u
inst✝¹ : Category.{v, u} C
U : FormalCoproduct C
α : Type
inst✝ : HasProductsOfShape α C
s : Fan fun x ↦ U
φ : (i : s.pt.I) → s.pt.obj i ⟶ (U.powerFan α).pt.obj ((fun i a ↦ (s.proj a).f i) i)
i : s.pt.I
a : α
w✝ : ({ f := fun i a ↦ (s.proj a).f i, φ := φ } ≫ (U.powerFan α).proj a).f = (s.proj a).f
hm :
  ∀ (i : s.pt.I), ({ f := fun i a ↦ (s.proj a).f i, φ := φ } ≫ (U.powerFan α).proj a).φ i ≫ eqToHom ⋯ = (s.proj a).φ i
⊢ (φ i ≫ 𝟙 (∏ᶜ U.obj ∘ fun a ↦ (s.proj a).f i)) ≫ Pi.π (U.obj ∘ fun a ↦ (s.proj a).f i) a =
    (Pi.lift fun a ↦ (s.proj a).φ i) ≫ Pi.π (U.obj ∘ fun a ↦ (s.proj a).f i) a
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
g₃ : Y ⟶ X₃
b : Y ⟶ S
hg₁ : g₁ ≫ f₁ = b
hg₂ : g₂ ≫ f₂ = b
hg₃ : g₃ ≫ f₃ = b
φ₁₂ : Y ⟶ h₁₂.pullback
w₁ : φ₁₂ ≫ h₁₂.p₁ = g₁
w₂ : φ₁₂ ≫ h₁₂.p₂ = g₂
φ₂₃ : Y ⟶ h₂₃.pullback
w₂' : φ₂₃ ≫ h₂₃.p₁ = g₂
w₃ : φ₂₃ ≫ h₂₃.p₂ = g₃
φ : Y ⟶ h.chosenPullback.pullback
w₁₂ : φ ≫ h.chosenPullback.p₁ = φ₁₂
w₂₃ : φ ≫ h.chosenPullback.p₂ = φ₂₃
⊢ φ ≫ h.p₁ = φ ≫ h.chosenPullback.p₁ ≫ h₁₂.p₁

Tactic:
← p₁₂,

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
g₃ : Y ⟶ X₃
b : Y ⟶ S
hg₁ : g₁ ≫ f₁ = b
hg₂ : g₂ ≫ f₂ = b
hg₃ : g₃ ≫ f₃ = b
φ₁₂ : Y ⟶ h₁₂.pullback
w₁ : φ₁₂ ≫ h₁₂.p₁ = g₁
w₂ : φ₁₂ ≫ h₁₂.p₂ = g₂
φ₂₃ : Y ⟶ h₂₃.pullback
w₂' : φ₂₃ ≫ h₂₃.p₁ = g₂
w₃ : φ₂₃ ≫ h₂₃.p₂ = g₃
φ : Y ⟶ h.chosenPullback.pullback
w₁₂ : φ ≫ h.chosenPullback.p₁ = φ₁₂
w₂₃ : φ ≫ h.chosenPullback.p₂ = φ₂₃
⊢ φ ≫ h.p₁ = φ ≫ h.p₁₂ ≫ h₁₂.p₁
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
g₃ : Y ⟶ X₃
b : Y ⟶ S
hg₁ : g₁ ≫ f₁ = b
hg₂ : g₂ ≫ f₂ = b
hg₃ : g₃ ≫ f₃ = b
φ₁₂ : Y ⟶ h₁₂.pullback
w₁ : φ₁₂ ≫ h₁₂.p₁ = g₁
w₂ : φ₁₂ ≫ h₁₂.p₂ = g₂
φ₂₃ : Y ⟶ h₂₃.pullback
w₂' : φ₂₃ ≫ h₂₃.p₁ = g₂
w₃ : φ₂₃ ≫ h₂₃.p₂ = g₃
φ : Y ⟶ h.chosenPullback.pullback
w₁₂ : φ ≫ h.chosenPullback.p₁ = φ₁₂
w₂₃ : φ ≫ h.chosenPullback.p₂ = φ₂₃
⊢ φ ≫ h.p₂ = φ ≫ h.chosenPullback.p₁ ≫ h₁₂.p₂

Tactic:
← p₁₂,

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
g₃ : Y ⟶ X₃
b : Y ⟶ S
hg₁ : g₁ ≫ f₁ = b
hg₂ : g₂ ≫ f₂ = b
hg₃ : g₃ ≫ f₃ = b
φ₁₂ : Y ⟶ h₁₂.pullback
w₁ : φ₁₂ ≫ h₁₂.p₁ = g₁
w₂ : φ₁₂ ≫ h₁₂.p₂ = g₂
φ₂₃ : Y ⟶ h₂₃.pullback
w₂' : φ₂₃ ≫ h₂₃.p₁ = g₂
w₃ : φ₂₃ ≫ h₂₃.p₂ = g₃
φ : Y ⟶ h.chosenPullback.pullback
w₁₂ : φ ≫ h.chosenPullback.p₁ = φ₁₂
w₂₃ : φ ≫ h.chosenPullback.p₂ = φ₂₃
⊢ φ ≫ h.p₂ = φ ≫ h.p₁₂ ≫ h₁₂.p₂
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n : ℕ
⊢ functorObj M N (n + 1) ⟶ functorObj M N n

Tactic:
refine Limits.Pi.map fun m ↦ if h : m < n then eqToHom ?_ else
    if h' : m < n + 1 then eqToHom ?_ ≫ f m ≫ eqToHom ?_ else eqToHom ?_

Goal state after:
case refine_1
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
h : m < n
⊢ (if x : m < n + 1 then M m else N m) = if x : m < n then M m else N m

case refine_2
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
h : ¬m < n
h' : m < n + 1
⊢ (if x : m < n + 1 then M m else N m) = M m

case refine_3
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
h : ¬m < n
h' : m < n + 1
⊢ N m = if x : m < n then M m else N m

case refine_4
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m : ℕ
h : ¬m < n
h' : ¬m < n + 1
⊢ (if x : m < n + 1 then M m else N m) = if x : m < n then M m else N m
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
s : Cone (Functor.ofOpSequence (functorMap f))
⊢ ∀ (j : ℕᵒᵖ),
    (Pi.lift fun m ↦ s.π.app (Opposite.op (m + 1)) ≫ Pi.π (fun i ↦ if x : i < m + 1 then M i else N i) m ≫ eqToHom ⋯) ≫
        (cone f).π.app j =
      s.π.app j

Tactic:
intro ⟨n⟩

Goal state after:
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
s : Cone (Functor.ofOpSequence (functorMap f))
n : ℕ
⊢ (Pi.lift fun m ↦ s.π.app (Opposite.op (m + 1)) ≫ Pi.π (fun i ↦ if x : i < m + 1 then M i else N i) m ≫ eqToHom ⋯) ≫
      (cone f).π.app (Opposite.op n) =
    s.π.app (Opposite.op n)
Module: Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits

Goal state before:
pp: J : Type u_1
C : Type u_3
K : Type u_5
K' : Type u_6
inst✝³ : Category.{v_1, u_5} K
inst✝² : Category.{v_2, u_6} K'
inst✝¹ : Category.{v_3, u_1} J
inst✝ : Category.{v_5, u_3} C
e : K ≌ K'
⊢ preservesLimitsOfShape K = preservesLimitsOfShape K'

Tactic:
by
  ext G
  simp only [preservesLimitsOfShape_iff]
  exact ⟨fun _ ↦ preservesLimitsOfShape_of_equiv e _,
    fun _ ↦ preservesLimitsOfShape_of_equiv e.symm _⟩

Goal state after:
Module: Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
P : ObjectProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f : X ⟶ Y
x✝ : P.isLocal.transfiniteCompositionsOfShape J f
Z : C
hZ : P Z
hf : P.isLocal.TransfiniteCompositionOfShape J f
g : X ⟶ Z
d : (hf.F.op ⋙ yoneda.obj Z).WellOrderInductionData := Functor.WellOrderInductionData.ofExists ⋯ ⋯
⊢ ∃ a, (fun g ↦ f ≫ g) a = g

Tactic:
let σ := d.sectionsMk (hf.isoBot.hom ≫ g)

Goal state after:
case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
P : ObjectProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f : X ⟶ Y
x✝ : P.isLocal.transfiniteCompositionsOfShape J f
Z : C
hZ : P Z
hf : P.isLocal.TransfiniteCompositionOfShape J f
g : X ⟶ Z
d : (hf.F.op ⋙ yoneda.obj Z).WellOrderInductionData := Functor.WellOrderInductionData.ofExists ⋯ ⋯
σ : ↑(hf.F.op ⋙ yoneda.obj Z).sections := d.sectionsMk (hf.isoBot.hom ≫ g)
⊢ ∃ a, (fun g ↦ f ≫ g) a = g
Module: Mathlib.CategoryTheory.Subterminal

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : C
inst✝¹ : HasBinaryProduct A A
inst✝ : IsIso (diag A)
Z : C
f g : Z ⟶ A
⊢ f = g

Tactic:
have : (Limits.prod.fst : A ⨯ A ⟶ _) = Limits.prod.snd := by simp [← cancel_epi (diag A)]
  rw [← prod.lift_fst f g, this, prod.lift_snd]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
⊢ ((reflectorAdjunction i).homEquiv (A ⊗ B) ((reflector i).obj A ⊗ (reflector i).obj B)).symm
      ((β_ A B).hom ≫
        ((ihom.adjunction B).homEquiv A (i.obj ((reflector i).obj A ⊗ (reflector i).obj B))).symm
          ((reflectorAdjunction i).unit.app A ≫
            ((ihom.adjunction B).homEquiv (i.obj ((reflector i).obj A))
                (i.obj ((reflector i).obj A ⊗ (reflector i).obj B)))
              ((β_ B (i.obj ((reflector i).obj A))).hom ≫
                ((ihom.adjunction (i.obj ((reflector i).obj A))).homEquiv B
                      (i.obj ((reflector i).obj A ⊗ (reflector i).obj B))).symm
                  ((reflectorAdjunction i).unit.app B ≫
                    ((ihom.adjunction (i.obj ((reflector i).obj A))).homEquiv (i.obj ((reflector i).obj B))
                        (i.obj ((reflector i).obj A ⊗ (reflector i).obj B)))
                      (prodComparisonIso i ((reflector i).obj A) ((reflector i).obj B)).inv)))) =
    prodComparison (reflector i) A B

Tactic:
homEquiv_symm_apply_eq,

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
⊢ ((reflectorAdjunction i).homEquiv (A ⊗ B) ((reflector i).obj A ⊗ (reflector i).obj B)).symm
      ((β_ A B).hom ≫
        uncurry
          ((reflectorAdjunction i).unit.app A ≫
            ((ihom.adjunction B).homEquiv (i.obj ((reflector i).obj A))
                (i.obj ((reflector i).obj A ⊗ (reflector i).obj B)))
              ((β_ B (i.obj ((reflector i).obj A))).hom ≫
                ((ihom.adjunction (i.obj ((reflector i).obj A))).homEquiv B
                      (i.obj ((reflector i).obj A ⊗ (reflector i).obj B))).symm
                  ((reflectorAdjunction i).unit.app B ≫
                    ((ihom.adjunction (i.obj ((reflector i).obj A))).homEquiv (i.obj ((reflector i).obj B))
                        (i.obj ((reflector i).obj A ⊗ (reflector i).obj B)))
                      (prodComparisonIso i ((reflector i).obj A) ((reflector i).obj B)).inv)))) =
    prodComparison (reflector i) A B