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

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : CommSemiring R
inst✝¹ : Module R M
inst✝ : Module R N
e : M ≃ₗ[R] N
⊢ IsBaseChange R ↑e

Tactic:
by
  apply IsBaseChange.of_lift_unique
  intro Q I₁ I₂ I₃ I₄ g
  have : I₂ = I₃ := by
    ext r q
    change (by let _ := I₂; exact r • q) = (by let _ := I₃; exact r • q)
    dsimp
    rw [← one_smul R q, smul_smul, ← @smul_assoc _ _ _ (id _) (id _) (id _) I₄, smul_eq_mul]
  cases this
  refine
    ⟨g.comp e.symm.toLinearMap, by
      ext
      simp, ?_⟩
  rintro y (rfl : _ = _)
  ext
  simp

Goal state after:
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 := 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'
⊢ ∀ (y : O →ₗ[T] Q), (fun g' ↦ ↑S g' ∘ₗ h = r) y → y = q

Tactic:
intro q'

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
⊢ (fun g' ↦ ↑S g' ∘ₗ h = r) q' → q' = q
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_3
R : Type u_1
S : Type v₃
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
R' : Type u_6
S' : Type u_7
inst✝⁹ : CommSemiring R'
inst✝⁸ : CommSemiring S'
inst✝⁷ : Algebra R R'
inst✝⁶ : Algebra S S'
inst✝⁵ : Algebra R' S'
inst✝⁴ : Algebra R S'
inst✝³ : IsScalarTower R R' S'
inst✝² : IsScalarTower R S S'
H : IsPushout R S R' S'
A : Type u_8
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : S' →ₐ[R] A
h₁ : f.comp (toAlgHom R R' S') = g.comp (toAlgHom R R' S')
h₂ : f.comp (toAlgHom R S S') = g.comp (toAlgHom R S S')
x : S'
s : S
s' : S'
e : f s' = g s'
⊢ f ((algebraMap S S') s * s') = g ((algebraMap S S') s * s')

Tactic:
map_mul,

Goal state after:
case refine_3
R : Type u_1
S : Type v₃
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
R' : Type u_6
S' : Type u_7
inst✝⁹ : CommSemiring R'
inst✝⁸ : CommSemiring S'
inst✝⁷ : Algebra R R'
inst✝⁶ : Algebra S S'
inst✝⁵ : Algebra R' S'
inst✝⁴ : Algebra R S'
inst✝³ : IsScalarTower R R' S'
inst✝² : IsScalarTower R S S'
H : IsPushout R S R' S'
A : Type u_8
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : S' →ₐ[R] A
h₁ : f.comp (toAlgHom R R' S') = g.comp (toAlgHom R R' S')
h₂ : f.comp (toAlgHom R S S') = g.comp (toAlgHom R S S')
x : S'
s : S
s' : S'
e : f s' = g s'
⊢ f ((algebraMap S S') s) * f s' = g ((algebraMap S S') s * s')
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_3
R : Type u_1
S : Type v₃
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
R' : Type u_6
S' : Type u_7
inst✝⁹ : CommSemiring R'
inst✝⁸ : CommSemiring S'
inst✝⁷ : Algebra R R'
inst✝⁶ : Algebra S S'
inst✝⁵ : Algebra R' S'
inst✝⁴ : Algebra R S'
inst✝³ : IsScalarTower R R' S'
inst✝² : IsScalarTower R S S'
H : IsPushout R S R' S'
A : Type u_8
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : S' →ₐ[R] A
h₁ : f.comp (toAlgHom R R' S') = g.comp (toAlgHom R R' S')
h₂ : f.comp (toAlgHom R S S') = g.comp (toAlgHom R S S')
x : S'
s : S
s' : S'
e : f s' = g s'
⊢ f ((algebraMap S S') s) * f s' = g ((algebraMap S S') s * s')

Tactic:
map_mul,

Goal state after:
case refine_3
R : Type u_1
S : Type v₃
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
R' : Type u_6
S' : Type u_7
inst✝⁹ : CommSemiring R'
inst✝⁸ : CommSemiring S'
inst✝⁷ : Algebra R R'
inst✝⁶ : Algebra S S'
inst✝⁵ : Algebra R' S'
inst✝⁴ : Algebra R S'
inst✝³ : IsScalarTower R R' S'
inst✝² : IsScalarTower R S S'
H : IsPushout R S R' S'
A : Type u_8
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : S' →ₐ[R] A
h₁ : f.comp (toAlgHom R R' S') = g.comp (toAlgHom R R' S')
h₂ : f.comp (toAlgHom R S S') = g.comp (toAlgHom R S S')
x : S'
s : S
s' : S'
e : f s' = g s'
⊢ f ((algebraMap S S') s) * f s' = g ((algebraMap S S') s) * g s'
Module: Mathlib.CategoryTheory.ObjectProperty.Basic

Goal state before:
pp: C : Type u
inst✝¹ : CategoryStruct.{v, u} C
P : ObjectProperty C
X : C
inst✝ : P.Is X
⊢ P X

Tactic:
← P.is_iff

Goal state after:
C : Type u
inst✝¹ : CategoryStruct.{v, u} C
P : ObjectProperty C
X : C
inst✝ : P.Is X
⊢ P.Is X
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
⊢ p.length ≠ 0 ↔ ∃ c e p', p = e.toPath.comp p' ∧ p.length = p'.length + 1

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
  · have h_len : p.length = (p.length - 1) + 1 := by lia
    obtain ⟨c, e, p', hp', rfl⟩ := Path.eq_toPath_comp_of_length_eq_succ p h_len
    exact ⟨c, e, p', rfl, by lia⟩
  · rintro ⟨c, p', e, rfl, h⟩
    simp [h]

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

Goal state before:
pp: I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ≅ Y
i : I
⊢ f.inv i ≫ f.hom i = 𝟙 (Y i)

Tactic:
rw [← comp_apply, Iso.inv_hom_id, id_apply]

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 : Type u_1
inst✝² : Category.{v_1, u_1} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.IsEquivalence
inst✝ : (F ⋙ G).IsEquivalence
⊢ G.IsEquivalence

Tactic:
rw [isEquivalence_iff_of_iso (G.leftUnitor.symm ≪≫
    isoWhiskerRight F.asEquivalence.counitIso.symm G)]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u_1
inst✝² : Category.{v_1, u_1} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.IsEquivalence
inst✝ : (F ⋙ G).IsEquivalence
⊢ ((F.asEquivalence.inverse ⋙ F.asEquivalence.functor) ⋙ G).IsEquivalence
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: case mp
T : Type u
inst✝ : Category.{v, u} T
X Y X' Y' : T
f : X ⟶ Y
f' : X' ⟶ Y'
⊢ mk f = mk f' → ∃ hX hY, f = eqToHom hX ≫ f' ≫ eqToHom ⋯

Tactic:
intro h
    refine ⟨congr_arg Arrow.left h, congr_arg Arrow.right h, ?_⟩
    simpa [eqToHom_left, eqToHom_right] using! iso_w (eqToIso h.symm)

Goal state after:
Module: Mathlib.CategoryTheory.EpiMono

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝¹ : Mono f
inst✝ : IsSplitEpi f
⊢ f ≫ section_ f = 𝟙 X

Tactic:
by simp [← cancel_mono f]

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

Goal state before:
pp: case mpr
X Y : Type u
f : X → Y
⊢ Function.Injective f → Mono (↾f)

Tactic:
· refine fun H => ⟨fun g g' h => ConcreteCategory.hom_ext _ _ fun x ↦
      congrFun (H.comp_left ?_) x⟩
    ext y
    exact ConcreteCategory.congr_hom h y

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

Goal state before:
pp: m : Type u → Type v
inst✝¹ : _root_.Functor m
inst✝ : LawfulFunctor m
α : Type u
⊢ ↾_root_.Functor.map ⇑(Hom.hom (𝟙 α)) = 𝟙 (m α)

Tactic:
by ext X; apply id_map

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type v₁
f g : P ⟶ Q
h : ∀ (X : C) (p : yoneda.obj X ⟶ P), p ≫ f = p ≫ g
⊢ f = g

Tactic:
ext X x
  simpa only [yonedaEquiv_comp, Equiv.apply_symm_apply]
    using! congr_arg (yonedaEquiv) (h _ (yonedaEquiv.symm x))

Goal state after:
Module: Mathlib.CategoryTheory.Retract

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
τ : F ⟶ G
X Y : C
h : Retract X Y
⊢ Arrow.homMk (F.map h.i) (G.map h.i) ⋯ ≫ Arrow.homMk (F.map h.r) (G.map h.r) ⋯ = 𝟙 (Arrow.mk (τ.app X))

Tactic:
by ext <;> simp [← Functor.map_comp]

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

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
F' : D ⥤ C
A B : C
adj : F ⊣ F'
X : C
Y : D
f : F.obj X ⟶ Y
hf : Mono f
inst✝ : F.ReflectsMonomorphisms
⊢ Mono (F.map ((adj.homEquiv X Y) f))

Tactic:
by
    rw [← (homEquiv adj X Y).symm_apply_apply f] at hf
    exact mono_of_mono_fac (adj.homEquiv_counit _ _ _).symm

Goal state after:
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)
j : J
⊢ ι ((F ⋙ G) ⋙ H) j ≫ post (F ⋙ G) H ≫ H.map (post F G) = ι ((F ⋙ G) ⋙ H) j ≫ post F (G ⋙ H)

Tactic:
rw [← assoc, colimit.ι_post, ← H.map_comp, colimit.ι_post]

Goal state after:
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)
j : J
⊢ H.map (G.map (ι F j)) = ι ((F ⋙ G) ⋙ H) j ≫ post F (G ⋙ H)
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 : WidePullbackCone f
ι' : Type u_3
e : ι' ≃ ι
⊢ (Iso.refl
          ((Cone.postcompose (WidePullbackShape.functorExt (Iso.refl X) (fun i ↦ eqToIso ⋯) ⋯).hom).obj
              (Cone.whisker (WidePullbackShape.equivalenceOfEquiv ι' e.symm).functor (s.reindex e))).pt).hom ≫
      s.base =
    base
      ((Cone.postcompose (WidePullbackShape.functorExt (Iso.refl X) (fun i ↦ eqToIso ⋯) ⋯).hom).obj
        (Cone.whisker (WidePullbackShape.equivalenceOfEquiv ι' e.symm).functor (s.reindex e)))

Tactic:
by simp [base, reindex, mk]

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

Goal state before:
pp: case refine_2
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
e : X ≅ Y
J : Type u_1
inst✝ : Unique J
s : Cofan fun x ↦ X
m : (mk Y fun x ↦ e.hom).pt ⟶ s.pt
hm : ∀ (j : J), (mk Y fun x ↦ e.hom).inj j ≫ m = s.inj j
⊢ m = e.inv ≫ s.inj default

Tactic:
· simpa [← cancel_epi e.hom] using hm default

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z P : C
s : BinaryFan X Y
t✝ : BinaryFan Y X
I : IsLimit s
t : Cone (pair Y X)
m : t.pt ⟶ s.swap.pt
w : ∀ (j : Discrete WalkingPair), m ≫ s.swap.π.app j = t.π.app j
⊢ m = I.lift (BinaryFan.swap t)

Tactic:
have h := I.uniq (BinaryFan.swap t) m

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z P : C
s : BinaryFan X Y
t✝ : BinaryFan Y X
I : IsLimit s
t : Cone (pair Y X)
m : t.pt ⟶ s.swap.pt
w : ∀ (j : Discrete WalkingPair), m ≫ s.swap.π.app j = t.π.app j
h : (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.swap t).π.app j) → m = I.lift (BinaryFan.swap t)
⊢ m = I.lift (BinaryFan.swap t)
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S S' S'' : D
T : C ⥤ D
f : S ⟶ S'
f' : S' ⟶ S''
h : StructuredArrow S'' T
⊢ (map (f ≫ f')).obj h = (map f).obj ((map f').obj h)

Tactic:
by
  rw [eq_mk h]
  simp

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
B : Type u₄
inst✝ : Category.{v₄, u₄} B
L : D
R : C ⥤ D
L' : B
R' : A ⥤ B
F : C ⥤ A
G : D ⥤ B
α : L' ⟶ G.obj L
β : R ⋙ G ⟶ F ⋙ R'
F' : C ⥤ A
G' : D ⥤ B
e₁ : F ≅ F'
e₂ : G ≅ G'
α' : L' ⟶ G'.obj L
β' : R ⋙ G' ⟶ F' ⋙ R'
hα : α = α' ≫ e₂.inv.app L
hβ : β ≫ Functor.whiskerRight e₁.hom R' = R.whiskerLeft e₂.hom ≫ β'
X : StructuredArrow L R
⊢ ((map₂ α β).obj X).hom ≫ R'.map (e₁.app X.right).hom = ((map₂ α' β').obj X).hom

pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
B : Type u₄
inst✝ : Category.{v₄, u₄} B
L : D
R : C ⥤ D
L' : B
R' : A ⥤ B
F : C ⥤ A
G : D ⥤ B
α : L' ⟶ G.obj L
β : R ⋙ G ⟶ F ⋙ R'
F' : C ⥤ A
G' : D ⥤ B
e₁ : F ≅ F'
e₂ : G ≅ G'
α' : L' ⟶ G'.obj L
β' : R ⋙ G' ⟶ F' ⋙ R'
hα : α = α' ≫ e₂.inv.app L
hβ : β ≫ Functor.whiskerRight e₁.hom R' = R.whiskerLeft e₂.hom ≫ β'
⊢ ∀ {X Y : StructuredArrow L R} (f : X ⟶ Y),
    (map₂ α β).map f ≫ (isoMk (e₁.app Y.right) ⋯).hom = (isoMk (e₁.app X.right) ⋯).hom ≫ (map₂ α' β').map f

Tactic:
finally
  · subst hα
    simp [dsimp% congr($(hβ).app X.right)]
  · simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
S : C ⥤ D
f : T ⟶ T'
f' : T' ⟶ T''
h : CostructuredArrow S T
⊢ (map (f ≫ f')).obj h = (map f').obj ((map f).obj h)

Tactic:
by
  rw [eq_mk h]
  simp

Goal state after:
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✝
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasBinaryProduct X Y
W : C
i₁ i₂ : W ⟶ pullback f g
h : i₁ ≫ prod.lift (pullback.fst f g) (pullback.snd f g) = i₂ ≫ prod.lift (pullback.fst f g) (pullback.snd f g)
⊢ i₁ ≫ pullback.snd f g = i₂ ≫ pullback.snd f g

Tactic:
simpa using congrArg (fun f => f ≫ prod.snd) h

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

Goal state before:
pp: ⊢ ∀ {X Y : WalkingParallelPair} (f : X ⟶ Y),
    (𝟭 WalkingParallelPair).map f ≫ (eqToIso ⋯).hom =
      (eqToIso ⋯).hom ≫ (walkingParallelPairOp ⋙ walkingParallelPairOp.leftOp).map f

Tactic:
rintro _ _ (_ | _ | _)

Goal state after:
case left
⊢ (𝟭 WalkingParallelPair).map left ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (walkingParallelPairOp ⋙ walkingParallelPairOp.leftOp).map left

case right
⊢ (𝟭 WalkingParallelPair).map right ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (walkingParallelPairOp ⋙ walkingParallelPairOp.leftOp).map right

case id
X✝ : WalkingParallelPair
⊢ (𝟭 WalkingParallelPair).map (WalkingParallelPairHom.id X✝) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (walkingParallelPairOp ⋙ walkingParallelPairOp.leftOp).map (WalkingParallelPairHom.id X✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
F : WalkingParallelPair ⥤ C
⊢ ∀ {X Y : WalkingParallelPair} (f : X ⟶ Y),
    F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (parallelPair (F.map left) (F.map right)).map f

Tactic:
rintro _ _ (_ | _ | _)

Goal state after:
case left
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F : WalkingParallelPair ⥤ C
⊢ F.map left ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (parallelPair (F.map left) (F.map right)).map left

case right
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F : WalkingParallelPair ⥤ C
⊢ F.map right ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (parallelPair (F.map left) (F.map right)).map right

case id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F : WalkingParallelPair ⥤ C
X✝ : WalkingParallelPair
⊢ F.map (WalkingParallelPairHom.id X✝) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (parallelPair (F.map left) (F.map right)).map (WalkingParallelPairHom.id X✝)
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✝¹ : HasImage g
inst✝ : HasImage (f ≫ g)
⊢ Mono (preComp f g)

Tactic:
refine @mono_of_mono _ _ _ _ _ _ (image.ι g) ?_

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝¹ : HasImage g
inst✝ : HasImage (f ≫ g)
⊢ Mono (preComp f g ≫ ι g)
Module: Mathlib.Algebra.Category.ModuleCat.Semi

Goal state before:
pp: R : Type u
inst✝ : Semiring R
X₁ X₂ : Type v
g₁ : AddCommMonoid X₁
g₂ : AddCommMonoid X₂
m₁ : Module R X₁
m₂ : Module R X₂
e : X₁ ≃ₗ[R] X₂
⊢ ↟↑e.symm ≫ ↟↑e = 𝟙 (of R X₂)

Tactic:
by ext; apply e.right_inv

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Semi

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
X₁ X₂ : Type v
S₀ : Type u₀
inst✝² : CommSemiring S₀
S : Type u
inst✝¹ : Semiring S
inst✝ : Algebra S₀ S
M N : SemimoduleCat S
s : S
s₀ : S₀
n : ↑M
⊢ s • (algebraMap S₀ S) s₀ • n = (algebraMap S₀ S) s₀ • s • n

Tactic:
rw [← smul_assoc, smul_eq_mul, ← Algebra.commutes, mul_smul]

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
F : WalkingParallelPair ⥤ C
t : Fork (F.map left) (F.map right)
⊢ ∀ ⦃X Y : WalkingParallelPair⦄ (f : X ⟶ Y),
    ((Functor.const WalkingParallelPair).obj t.pt).map f ≫ t.π.app Y ≫ eqToHom ⋯ = (t.π.app X ≫ eqToHom ⋯) ≫ F.map f

Tactic:
rintro _ _ (_ | _ | _)

Goal state after:
case left
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Fork (F.map left) (F.map right)
⊢ ((Functor.const WalkingParallelPair).obj t.pt).map left ≫ t.π.app one ≫ eqToHom ⋯ =
    (t.π.app zero ≫ eqToHom ⋯) ≫ F.map left

case right
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Fork (F.map left) (F.map right)
⊢ ((Functor.const WalkingParallelPair).obj t.pt).map right ≫ t.π.app one ≫ eqToHom ⋯ =
    (t.π.app zero ≫ eqToHom ⋯) ≫ F.map right

case id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Fork (F.map left) (F.map right)
X✝ : WalkingParallelPair
⊢ ((Functor.const WalkingParallelPair).obj t.pt).map (WalkingParallelPairHom.id X✝) ≫ t.π.app X✝ ≫ eqToHom ⋯ =
    (t.π.app X✝ ≫ eqToHom ⋯) ≫ F.map (WalkingParallelPairHom.id X✝)
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
F : WalkingParallelPair ⥤ C
t : Cofork (F.map left) (F.map right)
⊢ ∀ ⦃X Y : WalkingParallelPair⦄ (f : X ⟶ Y),
    F.map f ≫ eqToHom ⋯ ≫ t.ι.app Y = (eqToHom ⋯ ≫ t.ι.app X) ≫ ((Functor.const WalkingParallelPair).obj t.pt).map f

Tactic:
rintro _ _ (_ | _ | _)

Goal state after:
case left
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Cofork (F.map left) (F.map right)
⊢ F.map left ≫ eqToHom ⋯ ≫ t.ι.app one =
    (eqToHom ⋯ ≫ t.ι.app zero) ≫ ((Functor.const WalkingParallelPair).obj t.pt).map left

case right
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Cofork (F.map left) (F.map right)
⊢ F.map right ≫ eqToHom ⋯ ≫ t.ι.app one =
    (eqToHom ⋯ ≫ t.ι.app zero) ≫ ((Functor.const WalkingParallelPair).obj t.pt).map right

case id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Cofork (F.map left) (F.map right)
X✝ : WalkingParallelPair
⊢ F.map (WalkingParallelPairHom.id X✝) ≫ eqToHom ⋯ ≫ t.ι.app X✝ =
    (eqToHom ⋯ ≫ t.ι.app X✝) ≫ ((Functor.const WalkingParallelPair).obj t.pt).map (WalkingParallelPairHom.id X✝)
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
F : WalkingParallelPair ⥤ C
t : Cone F
⊢ ∀ ⦃X Y : WalkingParallelPair⦄ (f : X ⟶ Y),
    ((Functor.const WalkingParallelPair).obj t.pt).map f ≫ t.π.app Y ≫ eqToHom ⋯ =
      (t.π.app X ≫ eqToHom ⋯) ≫ (parallelPair (F.map left) (F.map right)).map f

Tactic:
rintro _ _ (_ | _ | _)

Goal state after:
case left
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Cone F
⊢ ((Functor.const WalkingParallelPair).obj t.pt).map left ≫ t.π.app one ≫ eqToHom ⋯ =
    (t.π.app zero ≫ eqToHom ⋯) ≫ (parallelPair (F.map left) (F.map right)).map left

case right
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Cone F
⊢ ((Functor.const WalkingParallelPair).obj t.pt).map right ≫ t.π.app one ≫ eqToHom ⋯ =
    (t.π.app zero ≫ eqToHom ⋯) ≫ (parallelPair (F.map left) (F.map right)).map right

case id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Cone F
X✝ : WalkingParallelPair
⊢ ((Functor.const WalkingParallelPair).obj t.pt).map (WalkingParallelPairHom.id X✝) ≫ t.π.app X✝ ≫ eqToHom ⋯ =
    (t.π.app X✝ ≫ eqToHom ⋯) ≫ (parallelPair (F.map left) (F.map right)).map (WalkingParallelPairHom.id X✝)
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
F : WalkingParallelPair ⥤ C
t : Cocone F
⊢ ∀ ⦃X Y : WalkingParallelPair⦄ (f : X ⟶ Y),
    (parallelPair (F.map left) (F.map right)).map f ≫ eqToHom ⋯ ≫ t.ι.app Y =
      (eqToHom ⋯ ≫ t.ι.app X) ≫ ((Functor.const WalkingParallelPair).obj t.pt).map f

Tactic:
rintro _ _ (_ | _ | _)

Goal state after:
case left
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Cocone F
⊢ (parallelPair (F.map left) (F.map right)).map left ≫ eqToHom ⋯ ≫ t.ι.app one =
    (eqToHom ⋯ ≫ t.ι.app zero) ≫ ((Functor.const WalkingParallelPair).obj t.pt).map left

case right
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Cocone F
⊢ (parallelPair (F.map left) (F.map right)).map right ≫ eqToHom ⋯ ≫ t.ι.app one =
    (eqToHom ⋯ ≫ t.ι.app zero) ≫ ((Functor.const WalkingParallelPair).obj t.pt).map right

case id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Cocone F
X✝ : WalkingParallelPair
⊢ (parallelPair (F.map left) (F.map right)).map (WalkingParallelPairHom.id X✝) ≫ eqToHom ⋯ ≫ t.ι.app X✝ =
    (eqToHom ⋯ ≫ t.ι.app X✝) ≫ ((Functor.const WalkingParallelPair).obj t.pt).map (WalkingParallelPairHom.id X✝)
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✝
X Y : C
f g : X ⟶ Y
X' Y' : C
f' g' : X' ⟶ Y'
e₀ : X ≅ X'
e₁ : Y ≅ Y'
comm₁ : e₀.hom ≫ f' = f ≫ e₁.hom
comm₂ : e₀.hom ≫ g' = g ≫ e₁.hom
⊢ (parallelPair f g).map right ≫ e₁.hom = e₀.hom ≫ (parallelPair f' g').map right

Tactic:
simp [comm₂]

Goal state after: