mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝²³ : AddCommMonoid M
inst✝²² : AddCommMonoid N
inst✝²¹ : CommSemiring R
inst✝²⁰ : CommSemiring S
inst✝¹⁹ : Algebra R S
inst✝¹⁸ : Module R M
inst✝¹⁷ : Module R N
inst✝¹⁶ : Module S N
inst✝¹⁵ : IsScalarTower R S N
T : Type u_4
O : Type u_5
inst✝¹⁴ : CommSemiring T
inst✝¹³ : Algebra R T
inst✝¹² : Algebra S T
inst✝¹¹ : IsScalarTower R S T
inst✝¹⁰ : AddCommMonoid O
inst✝⁹ : Module R O
inst✝⁸ : Module S O
inst✝⁷ : Module T O
inst✝⁶ : IsScalarTower S T O
inst✝⁵ : IsScalarTower R S O
inst✝⁴ : IsScalarTower R T O
f : M →ₗ[R] N
hf : IsBaseChange S f
g : N →ₗ[S] O
hg : IsBaseChange T g
Q : Type (max v₁ u_5 u_4)
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Module T Q
inst✝ : IsScalarTower R T Q
i : M →ₗ[R] Q
this✝¹ : Module S Q := Module.compHom Q (algebraMap S T)
this✝ : IsScalarTower S T Q
this : IsScalarTower R S Q
g' : O →ₗ[T] Q
e : ↑R g' ∘ₗ ↑R g ∘ₗ f = i
⊢ ↑R (↑S g' ∘ₗ g) ∘ₗ f = i

Tactic:
← e

Goal state after:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝²³ : AddCommMonoid M
inst✝²² : AddCommMonoid N
inst✝²¹ : CommSemiring R
inst✝²⁰ : CommSemiring S
inst✝¹⁹ : Algebra R S
inst✝¹⁸ : Module R M
inst✝¹⁷ : Module R N
inst✝¹⁶ : Module S N
inst✝¹⁵ : IsScalarTower R S N
T : Type u_4
O : Type u_5
inst✝¹⁴ : CommSemiring T
inst✝¹³ : Algebra R T
inst✝¹² : Algebra S T
inst✝¹¹ : IsScalarTower R S T
inst✝¹⁰ : AddCommMonoid O
inst✝⁹ : Module R O
inst✝⁸ : Module S O
inst✝⁷ : Module T O
inst✝⁶ : IsScalarTower S T O
inst✝⁵ : IsScalarTower R S O
inst✝⁴ : IsScalarTower R T O
f : M →ₗ[R] N
hf : IsBaseChange S f
g : N →ₗ[S] O
hg : IsBaseChange T g
Q : Type (max v₁ u_5 u_4)
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Module T Q
inst✝ : IsScalarTower R T Q
i : M →ₗ[R] Q
this✝¹ : Module S Q := Module.compHom Q (algebraMap S T)
this✝ : IsScalarTower S T Q
this : IsScalarTower R S Q
g' : O →ₗ[T] Q
e : ↑R g' ∘ₗ ↑R g ∘ₗ f = i
⊢ ↑R (↑S g' ∘ₗ g) ∘ₗ f = ↑R g' ∘ₗ ↑R g ∘ₗ f
Module: Mathlib.Combinatorics.Quiver.Push

Goal state before:
pp: case h_map
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
⊢ ∀ (X Y : V) (f : X ⟶ Y), (of σ ⋙q lift σ φ τ h).map f = Eq.recOn ⋯ (Eq.recOn ⋯ (φ.map f))

Tactic:
· rintro X Y f
    simp only [Prefunctor.comp_map]
    apply eq_of_heq
    iterate 2 apply (cast_heq _ _).trans
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Basic

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
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.ReflectsIsomorphisms
inst✝ : G.ReflectsIsomorphisms
A✝ B✝ : C
f : A✝ ⟶ B✝
hf : IsIso (G.map (F.map f))
this : IsIso (F.map f)
⊢ IsIso f

Tactic:
exact isIso_of_reflects_iso f F

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
β : Sort u_1
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
X Y : C
e : X ≅ Y
hX : F.obj X = G.obj X
hY : F.obj Y = G.obj Y
⊢ F.obj X = G.obj X

Tactic:
by rw [hX]

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
β : Sort u_1
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
X Y : C
e : X ≅ Y
hX : F.obj X = G.obj X
hY : F.obj Y = G.obj Y
h₂ : F.map e.hom = eqToHom ⋯ ≫ G.map e.hom ≫ eqToHom ⋯
⊢ G.obj X = F.obj X

Tactic:
by rw [hX]

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
p : X = Y
⊢ F.mapIso (eqToIso p) = eqToIso ⋯

Tactic:
by ext; cases p; simp

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

Goal state before:
pp: α✝ : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
α : Type u₁
β : Type u₂
h : Discrete α ≌ Discrete β
a : α
⊢ (as ∘ h.inverse.obj ∘ mk) ((as ∘ h.functor.obj ∘ mk) a) = a

Tactic:
by simpa using eq_of_hom (h.unitIso.app (Discrete.mk a)).2

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : IsDiscrete C
unop✝¹ unop✝ : C
f : Opposite.unop (Opposite.op unop✝) ⟶ Opposite.unop (Opposite.op unop✝¹)
⊢ Opposite.op unop✝¹ = Opposite.op unop✝

Tactic:
obtain rfl := obj_ext_of_isDiscrete f

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : IsDiscrete C
unop✝ : C
f : Opposite.unop (Opposite.op unop✝) ⟶ Opposite.unop (Opposite.op (Opposite.unop (Opposite.op unop✝)))
⊢ Opposite.op (Opposite.unop (Opposite.op unop✝)) = Opposite.op unop✝
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: case a.a
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 : C ≌ D
f : D ≌ E
X : C
| f.functor.map (e.counitIso.inv.app (f.inverse.obj (f.functor.obj (e.functor.obj X)))) ≫
    f.functor.map (e.counitIso.hom.app (f.inverse.obj (f.functor.obj (e.functor.obj X))))

pp: case a.a
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 : C ≌ D
f : D ≌ E
X : C
| f.counitIso.hom.app (f.functor.obj (e.functor.obj X))

pp: case a
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 : C ≌ D
f : D ≌ E
X : C
| f.functor.map (f.unitIso.hom.app (e.functor.obj X))

Tactic:
rw [← Functor.map_comp, Iso.inv_hom_id_app]

Goal state after:
case a.a
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 : C ≌ D
f : D ≌ E
X : C
| f.functor.map (𝟙 ((𝟭 D).obj (f.inverse.obj (f.functor.obj (e.functor.obj X)))))

case a.a
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 : C ≌ D
f : D ≌ E
X : C
| f.counitIso.hom.app (f.functor.obj (e.functor.obj X))

case a
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 : C ≌ D
f : D ≌ E
X : C
| f.functor.map (f.unitIso.hom.app (e.functor.obj X))
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cone F
ht : ∀ (s : Cone F), ∃! l, ∀ (j : J), l ≫ t.π.app j = s.π.app j
⊢ IsLimit t

Tactic:
by
  choose s hs hs' using ht
  exact ⟨s, hs, hs'⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : F.cocones.CorepresentableBy X
s : Cocone F
⊢ (colimitCocone h).extend (homOfCocone h (coconeOfHom h (homOfCocone h s))) = coconeOfHom h (homOfCocone h s)

Tactic:
conv_lhs => simp only [homOfCocone_coconeOfHom]

Goal state after:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : F.cocones.CorepresentableBy X
s : Cocone F
⊢ (colimitCocone h).extend (homOfCocone h s) = coconeOfHom h (homOfCocone h s)
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Cᵒᵖ
F : Cᵒᵖ ⥤ Type v₁
⊢ ∀ {Y : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)} (f : (X, F) ⟶ Y),
    (yonedaPairing C).map f ≫ (yonedaEquiv.trans Equiv.ulift.symm).toIso.hom =
      (yonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫ (yonedaEvaluation C).map f

Tactic:
(Y, G)

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Cᵒᵖ
F : Cᵒᵖ ⥤ Type v₁
Y : Cᵒᵖ
G : Cᵒᵖ ⥤ Type v₁
⊢ ∀ (f : (X, F) ⟶ (Y, G)),
    (yonedaPairing C).map f ≫ (yonedaEquiv.trans Equiv.ulift.symm).toIso.hom =
      (yonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫ (yonedaEvaluation C).map f
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
F : C ⥤ Type v₁
f : coyoneda.obj (op X) ⟶ F
g : X ⟶ Y
⊢ (ConcreteCategory.hom (F.map g)) (coyonedaEquiv f) = coyonedaEquiv (coyoneda.map g.op ≫ f)

Tactic:
change (f.app X ≫ F.map g) (𝟙 X) = f.app Y (g ≫ 𝟙 Y)
  rw [← f.naturality]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F : C ⥤ Type v₁
⊢ ∀ {Y : C × (C ⥤ Type v₁)} (f : (X, F) ⟶ Y),
    (coyonedaPairing C).map f ≫ (coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom =
      (coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫ (coyonedaEvaluation C).map f

Tactic:
(Y, G)

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F : C ⥤ Type v₁
Y : C
G : C ⥤ Type v₁
⊢ ∀ (f : (X, F) ⟶ (Y, G)),
    (coyonedaPairing C).map f ≫ (coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom =
      (coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫ (coyonedaEvaluation C).map f
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: X✝ Y✝ : Type u
F : typeToCat.obj X✝ ⟶ typeToCat.obj Y✝
⊢ typeToCat.map (↾(Discrete.as ∘ F.toFunctor.obj ∘ Discrete.mk)) = F

Tactic:
by
    ext
    refine Functor.ext (by cat_disch) ?_
    intro x y f
    apply ULift.ext
    cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Functor.EpiMono

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X Y : C
f : X ⟶ Y
hf : Epi f
Z : D
g h : F.obj Y ⟶ Z
H : (adj.homEquiv Y Z) g = (adj.homEquiv Y Z) h
⊢ g = h

Tactic:
Equiv.apply_eq_iff_eq

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X Y : C
f : X ⟶ Y
hf : Epi f
Z : D
g h : F.obj Y ⟶ Z
H : g = h
⊢ g = h
Module: Mathlib.CategoryTheory.PUnit

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Discrete PUnit.{w + 1}
X : C
⊢ F.obj X = G.obj X

Tactic:
simp only [eq_iff_true_of_subsingleton]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty.{1} ⥤ C
Y : C
x : IsLimit { pt := Y, π := { app := fun X ↦ ⋯.elim, naturality := ⋯ } }
⊢ { lift := fun s ↦ default, fac := ⋯, uniq := ⋯ } = x

Tactic:
simp only [eq_iff_true_of_subsingleton]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty.{1} ⥤ C
X : C
x✝ : IsColimit { pt := X, ι := { app := fun X_1 ↦ ⋯.elim, naturality := ⋯ } }
⊢ { desc := fun s ↦ default, fac := ⋯, uniq := ⋯ } = x✝

Tactic:
simp only [eq_iff_true_of_subsingleton]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : Discrete PEmpty.{w' + 1} ⥤ C
c₁ : Cone F₁
c₂ : Cone F₂
h : c₁.pt ≅ c₂.pt
x✝ : IsLimit c₁
⊢ isLimitChangeEmptyCone C (isLimitChangeEmptyCone C x✝ c₂ h) c₁ h.symm = x✝

Tactic:
simp only [eq_iff_true_of_subsingleton]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : Discrete PEmpty.{w' + 1} ⥤ C
c₁ : Cone F₁
c₂ : Cone F₂
h : c₁.pt ≅ c₂.pt
x✝ : IsLimit c₂
⊢ isLimitChangeEmptyCone C (isLimitChangeEmptyCone C x✝ c₁ h.symm) c₂ h = x✝

Tactic:
simp only [eq_iff_true_of_subsingleton]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : Discrete PEmpty.{w' + 1} ⥤ C
c₁ : Cocone F₁
c₂ : Cocone F₂
h : c₁.pt ≅ c₂.pt
x✝ : IsColimit c₁
⊢ isColimitChangeEmptyCocone C (isColimitChangeEmptyCocone C x✝ c₂ h) c₁ h.symm = x✝

Tactic:
simp only [eq_iff_true_of_subsingleton]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : Discrete PEmpty.{w' + 1} ⥤ C
c₁ : Cocone F₁
c₂ : Cocone F₂
h : c₁.pt ≅ c₂.pt
x✝ : IsColimit c₂
⊢ isColimitChangeEmptyCocone C (isColimitChangeEmptyCocone C x✝ c₁ h.symm) c₂ h = x✝

Tactic:
simp only [eq_iff_true_of_subsingleton]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : C
hI : IsInitial I
h : ∀ (X : C), Mono (hI.to X)
I' X : C
hI' : IsInitial I'
⊢ Mono (hI'.to X)

Tactic:
by
    rw [hI'.hom_ext (hI'.to X) ((hI'.uniqueUpToIso hI).hom ≫ hI.to X)]
    apply mono_comp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasColimit F
E : K ⥤ J
inst✝¹ : HasColimit (E ⋙ F)
inst✝ : IsIso (pre F E)
k : K
⊢ ι F (E.obj k) ≫ inv (pre F E) = ι (E ⋙ F) k

Tactic:
by
  simp [IsIso.comp_inv_eq]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasColimit F
E : K ⥤ J
inst✝¹ : HasColimit (E ⋙ F)
L : Type u₃
inst✝ : Category.{v₃, u₃} L
D : L ⥤ K
h : HasColimit (D ⋙ E ⋙ F)
j : L
⊢ ι (D ⋙ E ⋙ F) j ≫ pre (E ⋙ F) D ≫ pre F E = ι (D ⋙ E ⋙ F) j ≫ pre F (D ⋙ E)

Tactic:
rw [← assoc, colimit.ι_pre, colimit.ι_pre]

Goal state after:
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasColimit F
E : K ⥤ J
inst✝¹ : HasColimit (E ⋙ F)
L : Type u₃
inst✝ : Category.{v₃, u₃} L
D : L ⥤ K
h : HasColimit (D ⋙ E ⋙ F)
j : L
⊢ ι F (E.obj (D.obj j)) = ι (D ⋙ E ⋙ F) j ≫ pre F (D ⋙ E)
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
C : Type u
inst✝⁴ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasColimit F
G : C ⥤ D
inst✝¹ : HasColimit (F ⋙ G)
E : Type u''
inst✝ : Category.{v'', u''} E
H : D ⥤ E
h : HasColimit ((F ⋙ G) ⋙ H)
⊢ post (F ⋙ G) H ≫ H.map (post F G) = post F (G ⋙ H)

Tactic:
ext j
  rw [← assoc, colimit.ι_post, ← H.map_comp, colimit.ι_post]
  have : HasColimit (F ⋙ G ⋙ H) := h
  exact (colimit.ι_post F (G ⋙ H) j).symm

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

Goal state before:
pp: J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : C
g1 g2 : X ⟶ widePullback B objs arrows
⊢ (∀ (j : J), g1 ≫ π arrows j = g2 ≫ π arrows j) → g1 ≫ base arrows = g2 ≫ base arrows → g1 = g2

Tactic:
intro h1 h2
  apply limit.hom_ext
  rintro (_ | _)
  · apply h2
  · apply h1

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: X Y : WalkingCospan
⊢ Subsingleton (X ⟶ Y)

Tactic:
constructor; intros; simp [eq_iff_true_of_subsingleton]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
s t : Cocone F
i : s.pt ≅ t.pt
w₁ : s.ι.app WalkingCospan.left ≫ i.hom = t.ι.app WalkingCospan.left
w₂ : s.ι.app WalkingCospan.right ≫ i.hom = t.ι.app WalkingCospan.right
⊢ s ≅ t

Tactic:
by
  apply Cocone.ext i _
  rintro (⟨⟩ | ⟨⟨⟩⟩)
  · have h₁ := s.ι.naturality WalkingSpan.Hom.fst
    dsimp at h₁
    simp only [Category.comp_id] at h₁
    have h₂ := t.ι.naturality WalkingSpan.Hom.fst
    dsimp at h₂
    simp only [Category.comp_id] at h₂
    simp_rw [← h₁, Category.assoc, w₁, h₂]
  · exact w₁
  · exact w₂

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingCospan ⥤ C
z : F.obj WalkingCospan.one ⟶ G.obj WalkingCospan.one
l : F.obj WalkingCospan.left ⟶ G.obj WalkingCospan.left
r : F.obj WalkingCospan.right ⟶ G.obj WalkingCospan.right
hl : F.map inl ≫ z = l ≫ G.map inl
hr : F.map inr ≫ z = r ≫ G.map inr
⊢ ∀ ⦃X Y : WalkingCospan⦄ (f : X ⟶ Y),
    (F.map f ≫ Option.casesOn Y z fun val ↦ WalkingPair.casesOn val l r) =
      (Option.casesOn X z fun val ↦ WalkingPair.casesOn val l r) ≫ G.map f

Tactic:
by rintro (_ | _ | _) (_ | _ | _) (_ | _); all_goals cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingCospan ⥤ C
z : F.obj WalkingCospan.one ≅ G.obj WalkingCospan.one
l : F.obj WalkingCospan.left ≅ G.obj WalkingCospan.left
r : F.obj WalkingCospan.right ≅ G.obj WalkingCospan.right
hl : F.map inl ≫ z.hom = l.hom ≫ G.map inl
hr : F.map inr ≫ z.hom = r.hom ≫ G.map inr
⊢ ∀ {X Y : WalkingCospan} (f : X ⟶ Y),
    F.map f ≫ (Option.casesOn Y z fun val ↦ WalkingPair.casesOn val l r).hom =
      (Option.casesOn X z fun val ↦ WalkingPair.casesOn val l r).hom ≫ G.map f

Tactic:
by rintro (_ | _ | _) (_ | _ | _) (_ | _); all_goals cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingSpan ⥤ C
z : F.obj WalkingSpan.zero ⟶ G.obj WalkingSpan.zero
l : F.obj WalkingSpan.left ⟶ G.obj WalkingSpan.left
r : F.obj WalkingSpan.right ⟶ G.obj WalkingSpan.right
hl : F.map fst ≫ l = z ≫ G.map fst
hr : F.map snd ≫ r = z ≫ G.map snd
⊢ ∀ ⦃X Y : WalkingSpan⦄ (f : X ⟶ Y),
    (F.map f ≫ Option.casesOn Y z fun val ↦ WalkingPair.casesOn val l r) =
      (Option.casesOn X z fun val ↦ WalkingPair.casesOn val l r) ≫ G.map f

Tactic:
by rintro (_ | _ | _) (_ | _ | _) (_ | _); all_goals cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Goal state before:
pp: case none.none.id
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
⊢ (((Functor.const WalkingCospan).obj W).map (WidePullbackShape.Hom.id none) ≫
      Option.casesOn none (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) =
    (Option.casesOn none (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) ≫
      (cospan f g).map (WidePullbackShape.Hom.id none)

Tactic:
simp [eq]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Goal state before:
pp: case some.left.none.term
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
⊢ (((Functor.const WalkingCospan).obj W).map (term WalkingPair.left) ≫
      Option.casesOn none (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) =
    (Option.casesOn (some WalkingPair.left) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) ≫
      (cospan f g).map (term WalkingPair.left)

Tactic:
simp [eq]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Goal state before:
pp: case some.left.some.left.id
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
⊢ (((Functor.const WalkingCospan).obj W).map (WidePullbackShape.Hom.id (some WalkingPair.left)) ≫
      Option.casesOn (some WalkingPair.left) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) =
    (Option.casesOn (some WalkingPair.left) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) ≫
      (cospan f g).map (WidePullbackShape.Hom.id (some WalkingPair.left))

Tactic:
simp [eq]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Goal state before:
pp: case some.right.none.term
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
⊢ (((Functor.const WalkingCospan).obj W).map (term WalkingPair.right) ≫
      Option.casesOn none (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) =
    (Option.casesOn (some WalkingPair.right) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) ≫
      (cospan f g).map (term WalkingPair.right)

Tactic:
simp [eq]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Goal state before:
pp: case some.right.some.right.id
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
⊢ (((Functor.const WalkingCospan).obj W).map (WidePullbackShape.Hom.id (some WalkingPair.right)) ≫
      Option.casesOn (some WalkingPair.right) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) =
    (Option.casesOn (some WalkingPair.right) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) ≫
      (cospan f g).map (WidePullbackShape.Hom.id (some WalkingPair.right))

Tactic:
simp [eq]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingSpan ⥤ C
z : F.obj WalkingSpan.zero ≅ G.obj WalkingSpan.zero
l : F.obj WalkingSpan.left ≅ G.obj WalkingSpan.left
r : F.obj WalkingSpan.right ≅ G.obj WalkingSpan.right
hl : F.map fst ≫ l.hom = z.hom ≫ G.map fst
hr : F.map snd ≫ r.hom = z.hom ≫ G.map snd
⊢ ∀ {X Y : WalkingSpan} (f : X ⟶ Y),
    F.map f ≫ (Option.casesOn Y z fun val ↦ WalkingPair.casesOn val l r).hom =
      (Option.casesOn X z fun val ↦ WalkingPair.casesOn val l r).hom ≫ G.map f

Tactic:
by rintro (_ | _ | _) (_ | _ | _) (_ | _); all_goals cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: case e_right
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
U V : Over X
f g : U ⟶ V
left✝¹ : U.left ⟶ V.left
b : U.right ⟶ V.right
w✝¹ : (𝟭 T).map left✝¹ ≫ V.hom = U.hom ≫ (Functor.fromPUnit X).map b
left✝ : U.left ⟶ V.left
e : U.right ⟶ V.right
w✝ : (𝟭 T).map left✝ ≫ V.hom = U.hom ≫ (Functor.fromPUnit X).map e
h : Hom.left { left := left✝¹, right := b, w := w✝¹ } = Hom.left { left := left✝, right := e, w := w✝ }
⊢ b = e

Tactic:
simp only [eq_iff_true_of_subsingleton]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: case e_left
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
U V : Under X
f g : U ⟶ V
left✝¹ : U.left ⟶ V.left
b : U.right ⟶ V.right
w✝¹ : (Functor.fromPUnit X).map left✝¹ ≫ V.hom = U.hom ≫ (𝟭 T).map b
left✝ : U.left ⟶ V.left
e : U.right ⟶ V.right
w✝ : (Functor.fromPUnit X).map left✝ ≫ V.hom = U.hom ≫ (𝟭 T).map e
h : Hom.right { left := left✝¹, right := b, w := w✝¹ } = Hom.right { left := left✝, right := e, w := w✝ }
⊢ left✝¹ = left✝

Tactic:
simp only [eq_iff_true_of_subsingleton]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Y
g✝ : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst✝ : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
reassoc₁ : h ≫ x ≫ s.inl = f ≫ s.inl
reassoc₂ : h ≫ y ≫ s.inr = g ≫ s.inr
⊢ h ≫ x ≫ s.inl = h ≫ y ≫ s.inr

Tactic:
reassoc₁,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Y
g✝ : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst✝ : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
reassoc₁ : h ≫ x ≫ s.inl = f ≫ s.inl
reassoc₂ : h ≫ y ≫ s.inr = g ≫ s.inr
⊢ f ≫ s.inl = h ≫ y ≫ s.inr
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: case h₀
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Y
g✝ : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst✝ : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
t : PushoutCocone x y
m✝ : (mk s.inl s.inr ⋯).pt ⟶ t.pt
hr : (mk s.inl s.inr ⋯).inl ≫ m✝ = t.inl
hr' : (mk s.inl s.inr ⋯).inr ≫ m✝ = t.inr
⊢ s.inl ≫ m✝ = s.inl ≫ hs.desc (mk t.inl t.inr ⋯)

Tactic:
simp only [PushoutCocone.mk_inl, PushoutCocone.mk_inr] at hr hr' ⊢
          simp only [hr]
          symm
          exact hs.fac _ WalkingSpan.left

Goal state after: