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

Goal state before:
pp: case refine_2
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
h : N →ₗ[S] O
hc : IsBaseChange T (↑R h ∘ₗ f)
Q : Type (max v₂ u_5 u_4)
inst✝³ : AddCommMonoid Q
inst✝² : Module S Q
inst✝¹ : Module T Q
inst✝ : IsScalarTower S T Q
r : N →ₗ[S] Q
this✝¹ : Module R Q := ⋯
this✝ : IsScalarTower R S Q
this : IsScalarTower R T Q
r' : M →ₗ[R] Q := ⋯
q : O →ₗ[T] Q := ⋯
q' : O →ₗ[T] Q
hq' : ↑S q' ∘ₗ h = r
⊢ ↑R q' ∘ₗ ↑R h ∘ₗ f = ↑R q ∘ₗ ↑R h ∘ₗ f

Tactic:
apply_fun LinearMap.restrictScalars R at hq'

Goal state after:
case refine_2
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
h : N →ₗ[S] O
hc : IsBaseChange T (↑R h ∘ₗ f)
Q : Type (max v₂ u_5 u_4)
inst✝³ : AddCommMonoid Q
inst✝² : Module S Q
inst✝¹ : Module T Q
inst✝ : IsScalarTower S T Q
r : N →ₗ[S] Q
this✝¹ : Module R Q := Module.restrictScalars R S Q
this✝ : IsScalarTower R S Q
this : IsScalarTower R T Q
r' : M →ₗ[R] Q := ↑R r ∘ₗ f
q : O →ₗ[T] Q := hc.lift r'
q' : O →ₗ[T] Q
hq' : ↑R (↑S q' ∘ₗ h) = ↑R r
⊢ ↑R q' ∘ₗ ↑R h ∘ₗ f = ↑R q ∘ₗ ↑R h ∘ₗ f
Module: Mathlib.Combinatorics.Quiver.Symmetric

Goal state before:
pp: V : Type u_2
inst✝ : Quiver V
h : HasInvolutiveReverse V
a b : V
p : Path a b
⊢ p.reverse.reverse = p

Tactic:
induction p with

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u₁
inst✝² : Quiver V
W : Type u₂
inst✝¹ : Quiver W
F : V ⥤q W
U : Type u₃
inst✝ : Quiver U
G : W ⥤q U
a b : V
p : Path a b
⊢ (F ⋙q G).mapPath p = G.mapPath (F.mapPath p)

Tactic:
induction p with

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ e.unit.app (e.inverse.obj Y) ≫ e.inverse.map (𝟙 (e.functor.obj (e.inverse.obj Y))) ≫ e.inverse.map (e.counit.app Y) =
    𝟙 (e.inverse.obj Y)

Tactic:
← counitInv_functor_comp,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ e.unit.app (e.inverse.obj Y) ≫
      e.inverse.map
          (e.counitInv.app (e.functor.obj (e.inverse.obj Y)) ≫ e.functor.map (e.unitInv.app (e.inverse.obj Y))) ≫
        e.inverse.map (e.counit.app Y) =
    𝟙 (e.inverse.obj Y)
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Faithful
X✝ Y✝ : Cᵒᵖ
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : F.op.map a₁✝ = F.op.map a₂✝
⊢ a₁✝.unop = a₂✝.unop

Tactic:
by simpa using map_injective F (Quiver.Hom.op_inj h)

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
hf : Arrow.mk f ∈ P.toSet
X' Y' : C
f' : X' ⟶ Y'
hX : X = X'
hY : Y = Y'
h : f' = eqToHom ⋯ ≫ f ≫ eqToHom hY
⊢ Arrow.mk f' ∈ P.toSet

Tactic:
(Arrow.mk_eq_mk_iff f' f).2 ⟨hX.symm, hY.symm, h⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
hf : Arrow.mk f ∈ P.toSet
X' Y' : C
f' : X' ⟶ Y'
hX : X = X'
hY : Y = Y'
h : f' = eqToHom ⋯ ≫ f ≫ eqToHom hY
⊢ Arrow.mk f ∈ P.toSet
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
P : MorphismProperty D
inst✝¹ : P.RespectsIso
F : C ⥤ D
inst✝ : F.IsEquivalence
⊢ P.map (F.asEquivalence.inverse ⋙ F) = P

Tactic:
P.map_eq_of_iso F.asEquivalence.counitIso,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
P : MorphismProperty D
inst✝¹ : P.RespectsIso
F : C ⥤ D
inst✝ : F.IsEquivalence
⊢ P.map (𝟭 D) = P
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
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
g : X ⟶ widePullback B objs arrows
h1 : ∀ (j : J), g ≫ π arrows j = fs j
h2 : g ≫ base arrows = f
⊢ ∀ (j : WidePullbackShape J),
    g ≫ (limit.cone (WidePullbackShape.wideCospan B objs arrows)).π.app j = (WidePullbackShape.mkCone f fs w).π.app j

Tactic:
rintro (_ | _)

Goal state after:
case none
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
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
g : X ⟶ widePullback B objs arrows
h1 : ∀ (j : J), g ≫ π arrows j = fs j
h2 : g ≫ base arrows = f
⊢ g ≫ (limit.cone (WidePullbackShape.wideCospan B objs arrows)).π.app none =
    (WidePullbackShape.mkCone f fs w).π.app none

case some
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
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
g : X ⟶ widePullback B objs arrows
h1 : ∀ (j : J), g ≫ π arrows j = fs j
h2 : g ≫ base arrows = f
val✝ : J
⊢ g ≫ (limit.cone (WidePullbackShape.wideCospan B objs arrows)).π.app (some val✝) =
    (WidePullbackShape.mkCone f fs w).π.app (some val✝)
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
h1 : ∀ (j : J), g1 ≫ π arrows j = g2 ≫ π arrows j
h2 : g1 ≫ base arrows = g2 ≫ base arrows
⊢ ∀ (j : WidePullbackShape J),
    g1 ≫ limit.π (WidePullbackShape.wideCospan B objs arrows) j =
      g2 ≫ limit.π (WidePullbackShape.wideCospan B objs arrows) j

Tactic:
rintro (_ | _)

Goal state after:
case none
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
h1 : ∀ (j : J), g1 ≫ π arrows j = g2 ≫ π arrows j
h2 : g1 ≫ base arrows = g2 ≫ base arrows
⊢ g1 ≫ limit.π (WidePullbackShape.wideCospan B objs arrows) none =
    g2 ≫ limit.π (WidePullbackShape.wideCospan B objs arrows) none

case some
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
h1 : ∀ (j : J), g1 ≫ π arrows j = g2 ≫ π arrows j
h2 : g1 ≫ base arrows = g2 ≫ base arrows
val✝ : J
⊢ g1 ≫ limit.π (WidePullbackShape.wideCospan B objs arrows) (some val✝) =
    g2 ≫ limit.π (WidePullbackShape.wideCospan B objs arrows) (some val✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
ι✝ : Type u_1
X✝ : C
Y✝ : ι✝ → C
f✝ : (i : ι✝) → Y✝ i ⟶ X✝
ι : Type u_2
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s t : WidePullbackCone f
e : s.pt ≅ t.pt
base : e.hom ≫ t.base = s.base
π : ∀ (i : ι), e.hom ≫ t.π i = s.π i
⊢ ∀ (j : WidePullbackShape ι), s.π.app j = e.hom ≫ t.π.app j

Tactic:
rintro (_ | _)

Goal state after:
case none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
ι✝ : Type u_1
X✝ : C
Y✝ : ι✝ → C
f✝ : (i : ι✝) → Y✝ i ⟶ X✝
ι : Type u_2
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s t : WidePullbackCone f
e : s.pt ≅ t.pt
base : e.hom ≫ t.base = s.base
π : ∀ (i : ι), e.hom ≫ t.π i = s.π i
⊢ s.π.app none = e.hom ≫ t.π.app none

case some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
ι✝ : Type u_1
X✝ : C
Y✝ : ι✝ → C
f✝ : (i : ι✝) → Y✝ i ⟶ X✝
ι : Type u_2
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s t : WidePullbackCone f
e : s.pt ≅ t.pt
base : e.hom ≫ t.base = s.base
π : ∀ (i : ι), e.hom ≫ t.π i = s.π i
val✝ : ι
⊢ s.π.app (some val✝) = e.hom ≫ t.π.app (some val✝)
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) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : C
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g : widePushout B objs arrows ⟶ X
h1 : ∀ (j : J), ι arrows j ≫ g = fs j
h2 : head arrows ≫ g = f
⊢ ∀ (j : WidePushoutShape J),
    (colimit.cocone (WidePushoutShape.wideSpan B objs arrows)).ι.app j ≫ g = (WidePushoutShape.mkCocone f fs w).ι.app j

Tactic:
rintro (_ | _)

Goal state after:
case none
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : C
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g : widePushout B objs arrows ⟶ X
h1 : ∀ (j : J), ι arrows j ≫ g = fs j
h2 : head arrows ≫ g = f
⊢ (colimit.cocone (WidePushoutShape.wideSpan B objs arrows)).ι.app none ≫ g =
    (WidePushoutShape.mkCocone f fs w).ι.app none

case some
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : C
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g : widePushout B objs arrows ⟶ X
h1 : ∀ (j : J), ι arrows j ≫ g = fs j
h2 : head arrows ≫ g = f
val✝ : J
⊢ (colimit.cocone (WidePushoutShape.wideSpan B objs arrows)).ι.app (some val✝) ≫ g =
    (WidePushoutShape.mkCocone f fs w).ι.app (some val✝)
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) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : C
g1 g2 : widePushout B objs arrows ⟶ X
h1 : ∀ (j : J), ι arrows j ≫ g1 = ι arrows j ≫ g2
h2 : head arrows ≫ g1 = head arrows ≫ g2
⊢ ∀ (j : WidePushoutShape J),
    colimit.ι (WidePushoutShape.wideSpan B objs arrows) j ≫ g1 =
      colimit.ι (WidePushoutShape.wideSpan B objs arrows) j ≫ g2

Tactic:
rintro (_ | _)

Goal state after:
case none
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : C
g1 g2 : widePushout B objs arrows ⟶ X
h1 : ∀ (j : J), ι arrows j ≫ g1 = ι arrows j ≫ g2
h2 : head arrows ≫ g1 = head arrows ≫ g2
⊢ colimit.ι (WidePushoutShape.wideSpan B objs arrows) none ≫ g1 =
    colimit.ι (WidePushoutShape.wideSpan B objs arrows) none ≫ g2

case some
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : C
g1 g2 : widePushout B objs arrows ⟶ X
h1 : ∀ (j : J), ι arrows j ≫ g1 = ι arrows j ≫ g2
h2 : head arrows ≫ g1 = head arrows ≫ g2
val✝ : J
⊢ colimit.ι (WidePushoutShape.wideSpan B objs arrows) (some val✝) ≫ g1 =
    colimit.ι (WidePushoutShape.wideSpan B objs arrows) (some val✝) ≫ g2
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsTerminal Y
c : BinaryFan X Y
a✝ : IsIso c.fst
⊢ Nonempty (IsLimit c)

Tactic:
exact
      ⟨BinaryFan.IsLimit.mk _ (fun f _ => f ≫ inv c.fst) (fun _ _ => by simp)
          (fun _ _ => h.hom_ext _ _) fun _ _ _ e _ => by simp [← e]⟩

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

Goal state before:
pp: T : Type u₁
inst✝² : Category.{v₁, u₁} T
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X : T
f✝ g✝ : Over X
φ : f✝ ⟶ g✝
f g : Over X
k : f ⟶ g
inst✝ : Mono k
⊢ Mono (Hom.left k)

Tactic:
refine ⟨fun {Y : T} l m a => ?_⟩

Goal state after:
T : Type u₁
inst✝² : Category.{v₁, u₁} T
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X : T
f✝ g✝ : Over X
φ : f✝ ⟶ g✝
f g : Over X
k : f ⟶ g
inst✝ : Mono k
Y : T
l m : Y ⟶ f.left
a : l ≫ Hom.left k = m ≫ Hom.left k
⊢ l = m
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝² : Category.{v₁, u₁} T
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X : T
f✝ g✝ : Over X
φ : f✝ ⟶ g✝
f g : Over X
k : f ⟶ g
inst✝ : Mono k
Y : T
l m : Y ⟶ f.left
a : l ≫ Hom.left k = m ≫ Hom.left k
⊢ l = m

Tactic:
let l' : mk (m ≫ f.hom) ⟶ f := homMk l (by
        dsimp; rw [← Over.w k, ← Category.assoc, congrArg (· ≫ g.hom) a, Category.assoc])

Goal state after:
T : Type u₁
inst✝² : Category.{v₁, u₁} T
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X : T
f✝ g✝ : Over X
φ : f✝ ⟶ g✝
f g : Over X
k : f ⟶ g
inst✝ : Mono k
Y : T
l m : Y ⟶ f.left
a : l ≫ Hom.left k = m ≫ Hom.left k
l' : mk (m ≫ f.hom) ⟶ f := homMk l ⋯
⊢ l = m
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝² : Category.{v₁, u₁} T
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X : T
f✝ g✝ : Under X
φ : f✝ ⟶ g✝
f g : Under X
k : f ⟶ g
inst✝ : Epi k
⊢ Epi (Hom.right k)

Tactic:
refine ⟨fun {Y : T} l m a => ?_⟩

Goal state after:
T : Type u₁
inst✝² : Category.{v₁, u₁} T
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X : T
f✝ g✝ : Under X
φ : f✝ ⟶ g✝
f g : Under X
k : f ⟶ g
inst✝ : Epi k
Y : T
l m : g.right ⟶ Y
a : Hom.right k ≫ l = Hom.right k ≫ m
⊢ l = m
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ⟶ G.obj zero
q : F.obj one ⟶ G.obj one
hl : F.map left ≫ q = p ≫ G.map left
hr : F.map right ≫ q = p ≫ G.map right
⊢ (X : WalkingParallelPair) → F.obj X ⟶ G.obj X

Tactic:
rintro (_ | _)

Goal state after:
case zero
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ⟶ G.obj zero
q : F.obj one ⟶ G.obj one
hl : F.map left ≫ q = p ≫ G.map left
hr : F.map right ≫ q = p ≫ G.map right
⊢ F.obj zero ⟶ G.obj zero

case one
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ⟶ G.obj zero
q : F.obj one ⟶ G.obj one
hl : F.map left ≫ q = p ≫ G.map left
hr : F.map right ≫ q = p ≫ G.map right
⊢ F.obj one ⟶ G.obj one
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ≅ G.obj zero
q : F.obj one ≅ G.obj one
hl : F.map left ≫ q.hom = p.hom ≫ G.map left
hr : F.map right ≫ q.hom = p.hom ≫ G.map right
⊢ (X : WalkingParallelPair) → F.obj X ≅ G.obj X

Tactic:
rintro (_ | _)

Goal state after:
case zero
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ≅ G.obj zero
q : F.obj one ≅ G.obj one
hl : F.map left ≫ q.hom = p.hom ≫ G.map left
hr : F.map right ≫ q.hom = p.hom ≫ G.map right
⊢ F.obj zero ≅ G.obj zero

case one
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ≅ G.obj zero
q : F.obj one ≅ G.obj one
hl : F.map left ≫ q.hom = p.hom ≫ G.map left
hr : F.map right ≫ q.hom = p.hom ≫ G.map right
⊢ F.obj one ≅ G.obj one
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝³ : HasEqualizers C
inst✝² : HasImage g
inst✝¹ : HasImage (f ≫ g)
inst✝ : Epi f
⊢ Epi (f ≫ factorThruImage g)

Tactic:
exact epi_comp _ _

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

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
t : Fork f g
⊢ t.ι ≫ f = t.ι ≫ g

Tactic:
← t.app_one_eq_ι_comp_left,

Goal state after:
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
t : Fork f g
⊢ t.π.app one = t.ι ≫ g
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : f = 0
⊢ IsZero X

Tactic:
subst h
  apply of_mono_zero X Y

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝ : F.IsEquivalence
h : HasStrongEpiMonoFactorisations C
X Y : D
f : X ⟶ Y
em : StrongEpiMonoFactorisation (F.inv.map f) := ⋯.some
this✝ : Mono (F.map em.m ≫ F.asEquivalence.counitIso.hom.app Y)
this : StrongEpi (F.asEquivalence.counitIso.inv.app X ≫ F.map em.e)
⊢ Nonempty (StrongEpiMonoFactorisation f)

Tactic:
exact
      Nonempty.intro
        { I := F.obj em.I
          e := F.asEquivalence.counitIso.inv.app X ≫ F.map em.e
          m := F.map em.m ≫ F.asEquivalence.counitIso.hom.app Y
          fac := by
            simp only [Category.assoc, ← F.map_comp_assoc,
              MonoFactorisation.fac, fun_inv_map, id_obj, Iso.inv_hom_id_app, Category.comp_id,
              Iso.inv_hom_id_app_assoc] }

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

Goal state before:
pp: C : Type u
X✝ Y✝ : C
inst✝² : Category.{v, u} C
f✝ g : X✝ ⟶ Y✝
inst✝¹ : IsSplitMono f✝
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
s : Fork (𝟙 Y) (retraction f ≫ f)
⊢ (s.ι ≫ retraction f) ≫ f = s.ι

Tactic:
rw [Category.assoc, ← s.condition]

Goal state after:
C : Type u
X✝ Y✝ : C
inst✝² : Category.{v, u} C
f✝ g : X✝ ⟶ Y✝
inst✝¹ : IsSplitMono f✝
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
s : Fork (𝟙 Y) (retraction f ≫ f)
⊢ s.ι ≫ 𝟙 Y = s.ι
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryProduct X Y
⊢ inr X Y ≫ fst = 0

Tactic:
by
  simp [prod.inr]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryProduct X Y
⊢ inr X Y ≫ snd = 𝟙 Y

Tactic:
by
  simp [prod.inr]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
F : J ⥤ C
G : C ⥤ D
inst✝² : G.ReflectsIsomorphisms
inst✝¹ : HasColimit F
inst✝ : PreservesColimit F G
c : Cocone F
t : IsColimit (G.mapCocone c)
⊢ Nonempty (IsColimit c)

Tactic:
suffices IsIso (IsColimit.desc (colimit.isColimit F) c) from ⟨by
      apply IsColimit.ofPointIso (colimit.isColimit F)⟩

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
F : J ⥤ C
G : C ⥤ D
inst✝² : G.ReflectsIsomorphisms
inst✝¹ : HasColimit F
inst✝ : PreservesColimit F G
c : Cocone F
t : IsColimit (G.mapCocone c)
⊢ IsIso ((colimit.isColimit F).desc c)
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J✝ : Type w
inst✝² : Category.{w', w} J✝
K✝ : J✝ ⥤ C
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
J : Type w'
𝒥₁ : Category.{w, w'} J
K : J ⥤ C
c : Cone K
t : IsLimit (F.mapCone c)
s : Cone K
m : s ⟶ c
⊢ (Cone.functoriality K F).map m =
    (Cone.functoriality K F).map
      ((Cone.functoriality K F).preimage (t.liftConeMorphism ((Cone.functoriality K F).obj s)))

Tactic:
Functor.map_preimage

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J✝ : Type w
inst✝² : Category.{w', w} J✝
K✝ : J✝ ⥤ C
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
J : Type w'
𝒥₁ : Category.{w, w'} J
K : J ⥤ C
c : Cone K
t : IsLimit (F.mapCone c)
s : Cone K
m : s ⟶ c
⊢ (Cone.functoriality K F).map m = t.liftConeMorphism ((Cone.functoriality K F).obj s)
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J✝ : Type w
inst✝² : Category.{w', w} J✝
K✝ : J✝ ⥤ C
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
J : Type w'
𝒥₁ : Category.{w, w'} J
K : J ⥤ C
c : Cocone K
t : IsColimit (F.mapCocone c)
s : Cocone K
m : c ⟶ s
⊢ (Cocone.functoriality K F).map m =
    (Cocone.functoriality K F).map
      ((Cocone.functoriality K F).preimage (t.descCoconeMorphism ((Cocone.functoriality K F).obj s)))

Tactic:
Functor.map_preimage

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J✝ : Type w
inst✝² : Category.{w', w} J✝
K✝ : J✝ ⥤ C
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
J : Type w'
𝒥₁ : Category.{w, w'} J
K : J ⥤ C
c : Cocone K
t : IsColimit (F.mapCocone c)
s : Cocone K
m : c ⟶ s
⊢ (Cocone.functoriality K F).map m = t.descCoconeMorphism ((Cocone.functoriality K F).obj s)
Module: Mathlib.CategoryTheory.Linear.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type w
inst✝¹ : Semiring R
inst✝ : Linear R C
X Y Z : C
r : Rˣ
f : X ⟶ Y
g : Y ⟶ Z
⊢ (r • f) ≫ g = r • f ≫ g

Tactic:
by
  apply Linear.smul_comp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type v
j j' : WidePullbackShape J
⊢ ∀ (x : j ⟶ j'),
    x ∈
      Option.casesOn j' (Option.casesOn j {Hom.id none} fun j ↦ {Hom.term j}) fun j' ↦
        if h : some j' = j then ⋯.mpr {Hom.id j} else ∅

Tactic:
rintro (_ | _)

Goal state after:
case id
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : WidePullbackShape J
⊢ Hom.id j ∈
    Option.casesOn j (Option.casesOn j {Hom.id none} fun j ↦ {Hom.term j}) fun j' ↦
      if h : some j' = j then ⋯.mpr {Hom.id j} else ∅

case term
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j✝ : J
⊢ Hom.term j✝ ∈
    Option.casesOn none (Option.casesOn (some j✝) {Hom.id none} fun j ↦ {Hom.term j}) fun j' ↦
      if h : some j' = some j✝ then ⋯.mpr {Hom.id (some j✝)} else ∅
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type v
j j' : WidePushoutShape J
⊢ ∀ (x : j ⟶ j'),
    x ∈
      Option.casesOn j (Option.casesOn j' {Hom.id none} fun j' ↦ {Hom.init j'}) fun j ↦
        if h : some j = j' then ⋯.mpr {Hom.id j'} else ∅

Tactic:
rintro (_ | _)

Goal state after:
case id
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : WidePushoutShape J
⊢ Hom.id j ∈
    Option.casesOn j (Option.casesOn j {Hom.id none} fun j' ↦ {Hom.init j'}) fun j_1 ↦
      if h : some j_1 = j then ⋯.mpr {Hom.id j} else ∅

case init
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j✝ : J
⊢ Hom.init j✝ ∈
    Option.casesOn none (Option.casesOn (some j✝) {Hom.id none} fun j' ↦ {Hom.init j'}) fun j ↦
      if h : some j = some j✝ then ⋯.mpr {Hom.id (some j✝)} else ∅
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J✝ : Type v
J : Type
inst✝¹ : Finite J
inst✝ : HasFiniteWidePushouts C
⊢ HasColimitsOfShape (WidePushoutShape J) C

Tactic:
have := @HasFiniteWidePushouts.out C _ _ J

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J✝ : Type v
J : Type
inst✝¹ : Finite J
inst✝ : HasFiniteWidePushouts C
this : ∀ [Finite J], HasColimitsOfShape (WidePushoutShape J) C
⊢ HasColimitsOfShape (WidePushoutShape J) C
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
⊢ ¬¬P = ⊥ ↔ P = ⊥

Tactic:
not_not

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
⊢ P = ⊥ ↔ P = ⊥