mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Goal state before:
pp: V : Type u
inst✝ : Quiver V
X✝² Y✝¹ X✝¹ Y✝ X Y : Paths (Symmetrify V)
X✝ Z✝ : Symmetrify V
f : X✝ ⟶ Z✝
XW : X✝² ⟶ (Paths.of (Symmetrify V)).obj X✝
WY : (Paths.of (Symmetrify V)).obj X✝ ⟶ Y✝¹
this :
  HomRel.CompClosure redStep (Path.reverse WY ≫ 𝟙 ((Paths.of (Symmetrify V)).obj X✝) ≫ Path.reverse XW)
    (Path.reverse WY ≫ (f.toPath ≫ (reverse f).toPath) ≫ Path.reverse XW)
⊢ HomRel.CompClosure redStep (Path.reverse (XW ≫ 𝟙 ((Paths.of (Symmetrify V)).obj X✝) ≫ WY))
    (Path.reverse (XW ≫ (f.toPath ≫ (reverse f).toPath) ≫ WY))

Tactic:
simpa using

Goal state after:
V : Type u
inst✝ : Quiver V
X✝² Y✝¹ X✝¹ Y✝ X Y : Paths (Symmetrify V)
X✝ Z✝ : Symmetrify V
f : X✝ ⟶ Z✝
XW : X✝² ⟶ (Paths.of (Symmetrify V)).obj X✝
WY : (Paths.of (Symmetrify V)).obj X✝ ⟶ Y✝¹
this :
  HomRel.CompClosure redStep (Path.reverse WY ≫ 𝟙 ((Paths.of (Symmetrify V)).obj X✝) ≫ Path.reverse XW)
    (Path.reverse WY ≫ (f.toPath ≫ (reverse f).toPath) ≫ Path.reverse XW)
⊢ HomRel.CompClosure redStep ((Path.reverse WY).comp (Path.reverse XW))
    ((Path.reverse WY).comp (f.toPath.comp ((reverse f).toPath.comp (Path.reverse XW))))
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
E : Type u₂
inst✝ : Groupoid E
φ : C ⥤ E
X Y : C
f : X ⟶ Y
⊢ (lift φ).map (homMk f) = φ.map f

Tactic:
simpa using

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
E : Type u₂
inst✝ : Groupoid E
φ : C ⥤ E
X Y : C
f : X ⟶ Y
⊢ (lift φ).map (homMk f) = φ.map f
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory

Goal state before:
pp: G : Type u₁
inst✝ : Groupoid G
⊢ lift (𝟭 G) ⋙ of G = 𝟭 (FreeGroupoid G)

Tactic:
rw [lift_unique (of G) (lift (𝟭 G) ⋙ of G) (by rw [← Functor.assoc, lift_spec, Functor.id_comp])]
  symm; apply lift_unique
  rw [Functor.comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.GuitartExact.Over

Goal state before:
pp: case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X : C
inst✝¹ : ∀ (Y : C), HasBinaryProduct X Y
inst✝ : ∀ (Y : C), PreservesLimit (pair X Y) F
W : Over (F.obj X)
Z : C
g : (Over.forget (F.obj X)).obj W ⟶ F.obj Z
P : (TwoSquare.overPost F X).StructuredArrowRightwards g := ⋯
this : Nonempty ((TwoSquare.overPost F X).StructuredArrowRightwards g)
Q : (TwoSquare.overPost F X).StructuredArrowRightwards g
⊢ ((Over.Hom.left (StructuredArrow.hom Q).left ≫
          F.map (prod.lift (StructuredArrow.right Q).left.hom (StructuredArrow.right Q).hom)) ≫
        prodComparison F X Z) ≫
      prod.fst =
    (Over.Hom.left (StructuredArrow.hom P).left ≫ prodComparison F X Z) ≫ prod.fst

Tactic:
simpa using

Goal state after:
case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X : C
inst✝¹ : ∀ (Y : C), HasBinaryProduct X Y
inst✝ : ∀ (Y : C), PreservesLimit (pair X Y) F
W : Over (F.obj X)
Z : C
g : (Over.forget (F.obj X)).obj W ⟶ F.obj Z
P : (TwoSquare.overPost F X).StructuredArrowRightwards g :=
  TwoSquare.StructuredArrowRightwards.mk (TwoSquare.overPost F X) g (Over.mk prod.fst)
    (Over.homMk
      (prod.lift
          (have this := W.hom;
          this)
          g ≫
        inv (prodComparison F X Z))
      ⋯)
    prod.snd ⋯
this : Nonempty ((TwoSquare.overPost F X).StructuredArrowRightwards g)
Q : (TwoSquare.overPost F X).StructuredArrowRightwards g
⊢ Over.Hom.left (StructuredArrow.hom Q).left ≫ F.map (StructuredArrow.right Q).left.hom = W.hom
Module: Mathlib.CategoryTheory.GuitartExact.Over

Goal state before:
pp: case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X : C
inst✝¹ : ∀ (Y : C), HasBinaryProduct X Y
inst✝ : ∀ (Y : C), PreservesLimit (pair X Y) F
W : Over (F.obj X)
Z : C
g : (Over.forget (F.obj X)).obj W ⟶ F.obj Z
P : (TwoSquare.overPost F X).StructuredArrowRightwards g := ⋯
this : Nonempty ((TwoSquare.overPost F X).StructuredArrowRightwards g)
Q : (TwoSquare.overPost F X).StructuredArrowRightwards g
⊢ ((Over.Hom.left (StructuredArrow.hom Q).left ≫
          F.map (prod.lift (StructuredArrow.right Q).left.hom (StructuredArrow.right Q).hom)) ≫
        prodComparison F X Z) ≫
      prod.snd =
    (Over.Hom.left (StructuredArrow.hom P).left ≫ prodComparison F X Z) ≫ prod.snd

Tactic:
simpa using

Goal state after:
case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X : C
inst✝¹ : ∀ (Y : C), HasBinaryProduct X Y
inst✝ : ∀ (Y : C), PreservesLimit (pair X Y) F
W : Over (F.obj X)
Z : C
g : (Over.forget (F.obj X)).obj W ⟶ F.obj Z
P : (TwoSquare.overPost F X).StructuredArrowRightwards g :=
  TwoSquare.StructuredArrowRightwards.mk (TwoSquare.overPost F X) g (Over.mk prod.fst)
    (Over.homMk
      (prod.lift
          (have this := W.hom;
          this)
          g ≫
        inv (prodComparison F X Z))
      ⋯)
    prod.snd ⋯
this : Nonempty ((TwoSquare.overPost F X).StructuredArrowRightwards g)
Q : (TwoSquare.overPost F X).StructuredArrowRightwards g
⊢ Over.Hom.left (StructuredArrow.hom Q).left ≫ F.map (StructuredArrow.right Q).hom = g
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d : C
f : c ⟶ d
h : Groupoid.inv f ∈ S.arrows d c
⊢ f ∈ S.arrows c d

Tactic:
simpa using

Goal state after:
case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d : C
f : c ⟶ d
h : Groupoid.inv f ∈ S.arrows d c
⊢ f ∈ S.arrows c d
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hf : f ∈ S.arrows c d
h : f ≫ g ∈ S.arrows c e
this : Groupoid.inv f ≫ f ≫ g ∈ S.arrows d e
⊢ g ∈ S.arrows d e

Tactic:
simpa using

Goal state after:
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hf : f ∈ S.arrows c d
h : f ≫ g ∈ S.arrows c e
this : Groupoid.inv f ≫ f ≫ g ∈ S.arrows d e
⊢ g ∈ S.arrows d e
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hg : g ∈ S.arrows d e
h : f ≫ g ∈ S.arrows c e
this : (f ≫ g) ≫ Groupoid.inv g ∈ S.arrows c d
⊢ f ∈ S.arrows c d

Tactic:
simpa using

Goal state after:
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hg : g ∈ S.arrows d e
h : f ≫ g ∈ S.arrows c e
this : (f ≫ g) ≫ Groupoid.inv g ∈ S.arrows c d
⊢ f ∈ S.arrows c d
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S T : Subgroupoid C
h : S ≤ T
x✝¹ x✝ : ↑S.objs
s : C
hs : s ∈ S.objs
t : C
ht : t ∈ S.objs
⊢ (inclusion h).obj ⟨s, hs⟩ = (inclusion h).obj ⟨t, ht⟩ → ⟨s, hs⟩ = ⟨t, ht⟩

Tactic:
simpa using

Goal state after:
C : Type u
inst✝ : Groupoid C
S T : Subgroupoid C
h : S ≤ T
x✝¹ x✝ : ↑S.objs
s : C
hs : s ∈ S.objs
t : C
ht : t ∈ S.objs
⊢ s = t → s = t
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
Sn : S.IsNormal
c d : C
p : c ⟶ d
γ₁ : c ⟶ c
x✝¹ : γ₁ ∈ S.arrows c c
γ₂ : c ⟶ c
x✝ : γ₂ ∈ S.arrows c c
h : (fun γ ↦ Groupoid.inv p ≫ γ ≫ p) γ₁ = (fun γ ↦ Groupoid.inv p ≫ γ ≫ p) γ₂
⊢ γ₁ = γ₂

Tactic:
simpa using

Goal state after:
case refine_1
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
Sn : S.IsNormal
c d : C
p : c ⟶ d
γ₁ : c ⟶ c
x✝¹ : γ₁ ∈ S.arrows c c
γ₂ : c ⟶ c
x✝ : γ₂ ∈ S.arrows c c
h : (fun γ ↦ Groupoid.inv p ≫ γ ≫ p) γ₁ = (fun γ ↦ Groupoid.inv p ≫ γ ≫ p) γ₂
⊢ γ₁ = γ₂
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
c d : D
f : c ⟶ d
⊢ (∃ a b g, ∃ (ha : φ.obj a = c) (hb : φ.obj b = d) (_ : g ∈ S.arrows a b), f = eqToHom ⋯ ≫ φ.map g ≫ eqToHom hb) →
    Arrows φ hφ S c d f

Tactic:
rintro ⟨a, b, g, rfl, rfl, hg, rfl⟩

Goal state after:
case mpr
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
a b : C
g : a ⟶ b
hg : g ∈ S.arrows a b
⊢ Arrows φ hφ S (φ.obj a) (φ.obj b) (eqToHom ⋯ ≫ φ.map g ≫ eqToHom ⋯)
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case refl.refl.refl
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
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
c' : C
hb : φ.obj c = φ.obj c
hb' : φ.obj c' = φ.obj c'
f : c ⟶ c'
⊢ Map.Arrows φ hφ S (φ.obj c') (φ.obj c')
    (Groupoid.inv (eqToHom ⋯ ≫ φ.map f ≫ eqToHom hb') ≫
      (eqToHom ⋯ ≫ φ.map γ ≫ eqToHom cd') ≫ eqToHom ⋯ ≫ φ.map f ≫ eqToHom hb')

Tactic:
simp only [eqToHom_refl, Category.comp_id, Category.id_comp, inv_eq_inv]

Goal state after:
case refl.refl.refl
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
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
c' : C
hb : φ.obj c = φ.obj c
hb' : φ.obj c' = φ.obj c'
f : c ⟶ c'
⊢ Map.Arrows φ hφ S (φ.obj c') (φ.obj c') (inv (φ.map f) ≫ φ.map γ ≫ φ.map f)
Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
r : R
j : J
x : ToType (F.obj j)
hx : (ModuleCat.Hom.hom (colimit.ι F j)) (r • x) = 0
j' : J
i : j ⟶ j'
h : (ModuleCat.Hom.hom (F.map i)) (r • x) = 0
j'' : J
H : ∀ (j : J) (x : j'' ⟶ j) (c : ↑(F.obj j)), r • c = 0 → c = 0
⊢ (ConcreteCategory.hom (colimit.ι F j)) x = 0

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
r : R
j : J
x : ToType (F.obj j)
hx : (ModuleCat.Hom.hom (colimit.ι F j)) (r • x) = 0
j' : J
i : j ⟶ j'
h : (ModuleCat.Hom.hom (F.map i)) (r • x) = 0
j'' : J
H : ∀ (j : J) (x : j'' ⟶ j) (c : ↑(F.obj j)), r • c = 0 → c = 0
⊢ (ConcreteCategory.hom (colimit.ι F j)) x = 0
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 : α
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

Tactic:
simpa using

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 ≫ Pi.π (U.obj ∘ fun a ↦ (s.proj a).f i) a = (s.proj a).φ i
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F G : C ⋆ D ⥤ E
eₗ : inclLeft C D ⋙ F ≅ inclLeft C D ⋙ G
eᵣ : inclRight C D ⋙ F ≅ inclRight C D ⋙ G
h :
  whiskerRight (edgeTransform C D) F ≫ ((Prod.snd C D).isoWhiskerLeft eᵣ).hom =
    ((Prod.fst C D).isoWhiskerLeft eₗ).hom ≫ whiskerRight (edgeTransform C D) G
⊢ whiskerRight (edgeTransform C D) F ≫ (Prod.snd C D).whiskerLeft eᵣ.hom =
    (Prod.fst C D).whiskerLeft eₗ.hom ≫ whiskerRight (edgeTransform C D) G

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F G : C ⋆ D ⥤ E
eₗ : inclLeft C D ⋙ F ≅ inclLeft C D ⋙ G
eᵣ : inclRight C D ⋙ F ≅ inclRight C D ⋙ G
h :
  whiskerRight (edgeTransform C D) F ≫ ((Prod.snd C D).isoWhiskerLeft eᵣ).hom =
    ((Prod.fst C D).isoWhiskerLeft eₗ).hom ≫ whiskerRight (edgeTransform C D) G
⊢ whiskerRight (edgeTransform C D) F ≫ (Prod.snd C D).whiskerLeft eᵣ.hom =
    (Prod.fst C D).whiskerLeft eₗ.hom ≫ whiskerRight (edgeTransform C D) G
Module: Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C : Type u_3
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} C
inst✝⁸ : HasZeroMorphisms C₁
inst✝⁷ : HasZeroMorphisms C₂
inst✝⁶ : HasZeroMorphisms C
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
F : C₁ ⥤ C₂ ⥤ C
inst✝⁵ : (F.obj c₁.pt).PreservesZeroMorphisms
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : PreservesColimit (parallelPair f₂ 0) (F.obj c₁.pt)
inst✝² : PreservesColimit (parallelPair f₁ 0) (F.flip.obj Y₂)
inst✝¹ : HasBinaryCoproduct ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)
inst✝ : PreservesColimit (parallelPair f₁ 0) (F.flip.obj X₂)
s : Cofork (coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂)) 0
⊢ Cofork.π (c₁.mapBifunctor c₂ F) ≫ ⋯.choose = s.π

Tactic:
simpa using

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C : Type u_3
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} C
inst✝⁸ : HasZeroMorphisms C₁
inst✝⁷ : HasZeroMorphisms C₂
inst✝⁶ : HasZeroMorphisms C
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
F : C₁ ⥤ C₂ ⥤ C
inst✝⁵ : (F.obj c₁.pt).PreservesZeroMorphisms
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : PreservesColimit (parallelPair f₂ 0) (F.obj c₁.pt)
inst✝² : PreservesColimit (parallelPair f₁ 0) (F.flip.obj Y₂)
inst✝¹ : HasBinaryCoproduct ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)
inst✝ : PreservesColimit (parallelPair f₁ 0) (F.flip.obj X₂)
s : Cofork (coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂)) 0
⊢ (F.map (Cofork.π c₁)).app Y₂ ≫ (F.obj c₁.pt).map (Cofork.π c₂) ≫ ⋯.choose = s.π
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : FormalCoproduct C
f : X.I → Y.I
F G : (i : X.I) → X.obj i ⟶ Y.obj (f i)
h₂ : ∀ (i : X.I), { f := f, φ := F }.φ i ≫ eqToHom ⋯ = { f := f, φ := G }.φ i
i : X.I
⊢ F i = G i

Tactic:
simpa using

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : FormalCoproduct C
f : X.I → Y.I
F G : (i : X.I) → X.obj i ⟶ Y.obj (f i)
h₂ : ∀ (i : X.I), { f := f, φ := F }.φ i ≫ eqToHom ⋯ = { f := f, φ := G }.φ i
i : X.I
⊢ F i = G i
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
X Y Z : FormalCoproduct C
f : X ⟶ Z
g : Y ⟶ Z
pb :
  (i : Function.Pullback f.f g.f) → PullbackCone (f.φ (↑i).1 ≫ eqToHom (@_proof_107 C inst✝¹ X Y Z f g i)) (g.φ (↑i).2)
hpb : (i : Function.Pullback f.f g.f) → IsLimit (pb i)
T : FormalCoproduct C
s : { p // p.1 ≫ f = p.2 ≫ g }
i : T.I
⊢ (↑s).1.φ i ≫
      f.φ (↑⟨((↑s).1.f i, (↑s).2.f i), ⋯⟩).1 ≫ eqToHom (@_proof_107 C inst✝¹ X Y Z f g ⟨((↑s).1.f i, (↑s).2.f i), ⋯⟩) =
    (↑s).2.φ i ≫ g.φ (↑⟨((↑s).1.f i, (↑s).2.f i), ⋯⟩).2

Tactic:
simpa using

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
X Y Z : FormalCoproduct C
f : X ⟶ Z
g : Y ⟶ Z
pb :
  (i : Function.Pullback f.f g.f) → PullbackCone (f.φ (↑i).1 ≫ eqToHom (@_proof_107 C inst✝¹ X Y Z f g i)) (g.φ (↑i).2)
hpb : (i : Function.Pullback f.f g.f) → IsLimit (pb i)
T : FormalCoproduct C
s : { p // p.1 ≫ f = p.2 ≫ g }
i : T.I
⊢ (↑s).1.φ i ≫ f.φ ((↑s).1.f i) ≫ eqToHom (@_proof_107 C inst✝¹ X Y Z f g ⟨((↑s).1.f i, (↑s).2.f i), ⋯⟩) =
    (↑s).2.φ i ≫ g.φ ((↑s).2.f i)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: 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₁₃
⊢ h.p₁ ≫ f₁ = h.p

Tactic:
simpa using

Goal state after:
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₁₃
⊢ h.chosenPullback.p₁ ≫ h₁₂.p₁ ≫ f₁ = h.p
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: 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₁₃
⊢ h.p₃ ≫ f₃ = h.p

Tactic:
simpa using

Goal state after:
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₁₃
⊢ h.chosenPullback.p₂ ≫ h₂₃.p₂ ≫ f₃ = h.p
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: 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₁₃
x✝² : C
x✝¹ x✝ : x✝² ⟶ h.pullback
h₁ : x✝¹ ≫ h.p₁₂ = x✝ ≫ h.p₁₂
h₂ : x✝¹ ≫ h.p₁₃ = x✝ ≫ h.p₁₃
⊢ x✝¹ ≫ h.p₁ = x✝ ≫ h.p₁

Tactic:
simpa using

Goal state after:
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₁₃
x✝² : C
x✝¹ x✝ : x✝² ⟶ h.pullback
h₁ : x✝¹ ≫ h.p₁₂ = x✝ ≫ h.p₁₂
h₂ : x✝¹ ≫ h.p₁₃ = x✝ ≫ h.p₁₃
⊢ x✝¹ ≫ h.p₁ = x✝ ≫ h.p₁
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: 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₁₃
x✝² : C
x✝¹ x✝ : x✝² ⟶ h.pullback
h₁ : x✝¹ ≫ h.p₁₂ = x✝ ≫ h.p₁₂
h₂ : x✝¹ ≫ h.p₁₃ = x✝ ≫ h.p₁₃
⊢ x✝¹ ≫ h.p₂ = x✝ ≫ h.p₂

Tactic:
simpa using

Goal state after:
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₁₃
x✝² : C
x✝¹ x✝ : x✝² ⟶ h.pullback
h₁ : x✝¹ ≫ h.p₁₂ = x✝ ≫ h.p₁₂
h₂ : x✝¹ ≫ h.p₁₃ = x✝ ≫ h.p₁₃
⊢ x✝¹ ≫ h.p₂ = x✝ ≫ h.p₂
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: 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₁₃
x✝² : C
x✝¹ x✝ : x✝² ⟶ h.pullback
h₁ : x✝¹ ≫ h.p₁₂ = x✝ ≫ h.p₁₂
h₂ : x✝¹ ≫ h.p₁₃ = x✝ ≫ h.p₁₃
⊢ x✝¹ ≫ h.p₃ = x✝ ≫ h.p₃

Tactic:
simpa using

Goal state after:
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₁₃
x✝² : C
x✝¹ x✝ : x✝² ⟶ h.pullback
h₁ : x✝¹ ≫ h.p₁₂ = x✝ ≫ h.p₁₂
h₂ : x✝¹ ≫ h.p₁₃ = x✝ ≫ h.p₁₃
⊢ x✝¹ ≫ h.p₃ = x✝ ≫ h.p₃
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: 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₁₃
x✝ : C
a : x✝ ⟶ h₁₂.pullback
b : x✝ ⟶ h₁₃.pullback
w : a ≫ h₁₂.p₁ = b ≫ h₁₃.p₁
⊢ (b ≫ h₁₃.p₂) ≫ f₃ = (a ≫ h₁₂.p₁) ≫ f₁

Tactic:
simpa using

Goal state after:
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₁₃
x✝ : C
a : x✝ ⟶ h₁₂.pullback
b : x✝ ⟶ h₁₃.pullback
w : a ≫ h₁₂.p₁ = b ≫ h₁₃.p₁
⊢ b ≫ h₁₃.p = a ≫ h₁₂.p
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: 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₁₃
x✝² : C
x✝¹ x✝ : x✝² ⟶ h.pullback
h₁ : x✝¹ ≫ h.p₁₃ = x✝ ≫ h.p₁₃
h₂ : x✝¹ ≫ h.p₂₃ = x✝ ≫ h.p₂₃
⊢ x✝¹ ≫ h.p₁ = x✝ ≫ h.p₁

Tactic:
simpa using

Goal state after:
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₁₃
x✝² : C
x✝¹ x✝ : x✝² ⟶ h.pullback
h₁ : x✝¹ ≫ h.p₁₃ = x✝ ≫ h.p₁₃
h₂ : x✝¹ ≫ h.p₂₃ = x✝ ≫ h.p₂₃
⊢ x✝¹ ≫ h.p₁ = x✝ ≫ h.p₁
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: 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₁₃
x✝² : C
x✝¹ x✝ : x✝² ⟶ h.pullback
h₁ : x✝¹ ≫ h.p₁₃ = x✝ ≫ h.p₁₃
h₂ : x✝¹ ≫ h.p₂₃ = x✝ ≫ h.p₂₃
⊢ x✝¹ ≫ h.p₂ = x✝ ≫ h.p₂

Tactic:
simpa using

Goal state after:
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₁₃
x✝² : C
x✝¹ x✝ : x✝² ⟶ h.pullback
h₁ : x✝¹ ≫ h.p₁₃ = x✝ ≫ h.p₁₃
h₂ : x✝¹ ≫ h.p₂₃ = x✝ ≫ h.p₂₃
⊢ x✝¹ ≫ h.p₂ = x✝ ≫ h.p₂
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: 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₁₃
x✝² : C
x✝¹ x✝ : x✝² ⟶ h.pullback
h₁ : x✝¹ ≫ h.p₁₃ = x✝ ≫ h.p₁₃
h₂ : x✝¹ ≫ h.p₂₃ = x✝ ≫ h.p₂₃
⊢ x✝¹ ≫ h.p₃ = x✝ ≫ h.p₃

Tactic:
simpa using

Goal state after:
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₁₃
x✝² : C
x✝¹ x✝ : x✝² ⟶ h.pullback
h₁ : x✝¹ ≫ h.p₁₃ = x✝ ≫ h.p₁₃
h₂ : x✝¹ ≫ h.p₂₃ = x✝ ≫ h.p₂₃
⊢ x✝¹ ≫ h.p₃ = x✝ ≫ h.p₃
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: 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₁₃
x✝ : C
a : x✝ ⟶ h₁₃.pullback
b : x✝ ⟶ h₂₃.pullback
w : a ≫ h₁₃.p₂ = b ≫ h₂₃.p₂
⊢ (b ≫ h₂₃.p₁) ≫ f₂ = (a ≫ h₁₃.p₁) ≫ f₁

Tactic:
simpa using

Goal state after:
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₁₃
x✝ : C
a : x✝ ⟶ h₁₃.pullback
b : x✝ ⟶ h₂₃.pullback
w : a ≫ h₁₃.p₂ = b ≫ h₂₃.p₂
⊢ b ≫ h₂₃.p = a ≫ h₁₃.p
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : Cone (cospan (𝟙 X) 0)
⊢ ∀ (j : WalkingCospan), 0 ≫ (PullbackCone.mk 0 0 ⋯).π.app j = s.π.app j

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : Cone (cospan (𝟙 X) 0)
⊢ ∀ (j : WalkingCospan), 0 = s.π.app j