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

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
inst✝ : IsIso g
H : P ((CommRingCat.Hom.hom g).comp (CommRingCat.Hom.hom f))
⊢ P (CommRingCat.Hom.hom f)

Tactic:
convert! hP.1 (f ≫ g).hom (asIso g).symm.commRingCatIsoToRingEquiv H
    simp [← CommRingCat.hom_comp]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝² : Category.{v_1, u_1} J
J' : Type u_2
inst✝¹ : Category.{v_2, u_2} J'
F : J ⥤ J'
inst✝ : F.Final
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X₁ X₂ : J' ⥤ C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J' f
h₁' : IsColimit (Cocone.whisker F c₁)
h₂' : IsColimit (Cocone.whisker F c₂)
j : J
this :
  c₁.ι.app (F.obj j) ≫ h₁'.desc { pt := c₂.pt, ι := F.whiskerLeft f ≫ F.whiskerLeft c₂.ι } =
    f.app (F.obj j) ≫ c₂.ι.app (F.obj j)
⊢ c₁.ι.app (F.obj j) ≫ h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } =
    c₁.ι.app (F.obj j) ≫ h₁'.desc { pt := c₂.pt, ι := F.whiskerLeft f ≫ F.whiskerLeft c₂.ι }

Tactic:
simp [this]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
n : ℕ
K : Discrete (Fin n) ⥤ C
⊢ HasColimit K

Tactic:
let that : K ≅ Discrete.functor fun n => K.obj ⟨n⟩ := Discrete.natIso fun ⟨_⟩ => Iso.refl _

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
n : ℕ
K : Discrete (Fin n) ⥤ C
that : K ≅ Discrete.functor fun n_1 ↦ K.obj { as := n_1 } :=
  Discrete.natIso fun x ↦
    match x with
    | { as := as } => Iso.refl (K.obj { as := as })
⊢ HasColimit K
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
X₁ X₂ : C
f : X₁ ⟶ X₂
hf : W f
h : IsInitial (⊥_ Discrete PUnit.{w + 1})
c₁ : Cocone (Discrete.functor fun x ↦ X₁) := coconeOfDiagramInitial h (Discrete.functor fun x ↦ X₁)
c₂ : Cocone (Discrete.functor fun x ↦ X₂) := coconeOfDiagramInitial h (Discrete.functor fun x ↦ X₂)
hc₁ : IsColimit c₁
⊢ W.colimitsOfShape (Discrete PUnit.{w + 1}) f

Tactic:
have hc₂ : IsColimit c₂ := colimitOfDiagramInitial h _

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
X₁ X₂ : C
f : X₁ ⟶ X₂
hf : W f
h : IsInitial (⊥_ Discrete PUnit.{w + 1})
c₁ : Cocone (Discrete.functor fun x ↦ X₁) := coconeOfDiagramInitial h (Discrete.functor fun x ↦ X₁)
c₂ : Cocone (Discrete.functor fun x ↦ X₂) := coconeOfDiagramInitial h (Discrete.functor fun x ↦ X₂)
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
⊢ W.colimitsOfShape (Discrete PUnit.{w + 1}) f
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : IsStableUnderCoproducts.{w, v, u} Q
h : P ≤ Q
⊢ coproducts.{w, v, u} P ≤ Q

Tactic:
exact le_trans (coproducts_monotone h) Q.coproducts_le

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

Goal state before:
pp: case refine_2.hf
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
P : MorphismProperty C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
Q : MorphismProperty C
inst✝ : Q.IsStableUnderBaseChange
hP : Q ≤ P.diagonal
Y X S : C
g : Y ⟶ X
f : X ⟶ S
hf : Q f
hcomp : P (g ≫ f)
gr : Y ⟶ pullback (g ≫ f) f := ⋯
this : g = gr ≫ pullback.snd (g ≫ f) f
⊢ P gr

Tactic:
exact P.of_isPullback (pullback_lift_diagonal_isPullback g f) (hP _ hf)

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
X Y : C
g : X ⟶ Y
H : ∀ {T : C} (f : T ⟶ Y) [inst : HasPullback f g], P (pullback.fst f g)
X' Y' : C
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
h : IsPullback f' i₁ i₂ g
this : HasPullback i₂ g
⊢ P (pullback.fst i₂ g)

Tactic:
exact H ..

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.IsStableUnderBaseChangeAgainst ⊤
x✝⁷ x✝⁶ x✝⁵ x✝⁴ : C
x✝³ : x✝⁷ ⟶ x✝⁴
x✝² : x✝⁶ ⟶ x✝⁴
x✝¹ : x✝⁵ ⟶ x✝⁶
x✝ : x✝⁵ ⟶ x✝⁷
h' : IsPullback x✝¹ x✝ x✝² x✝³
h'' : P x✝²
⊢ ⊤ x✝³

Tactic:
tauto

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.HasPullbacksAgainst ⊤
X✝ Y✝ S✝ : C
f✝ : X✝ ⟶ S✝
x✝ : Y✝ ⟶ S✝
h' : P f✝
⊢ ⊤ x✝

Tactic:
tauto

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.IsStableUnderCobaseChangeAgainst ⊤
x✝⁷ x✝⁶ x✝⁵ x✝⁴ : C
x✝³ : x✝⁷ ⟶ x✝⁶
x✝² : x✝⁷ ⟶ x✝⁵
x✝¹ : x✝⁵ ⟶ x✝⁴
x✝ : x✝⁶ ⟶ x✝⁴
h' : IsPushout x✝² x✝³ x✝¹ x✝
h'' : P x✝³
⊢ ⊤ x✝²

Tactic:
tauto

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.HasPushoutsAgainst ⊤
X✝ Y✝ S✝ : C
f✝ : S✝ ⟶ X✝
x✝ : S✝ ⟶ Y✝
h' : P f✝
⊢ ⊤ x✝

Tactic:
tauto

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : CartesianMonoidalCategory C
M : C
inst✝¹ : MonObj M
inst✝ : BraidedCategory C
h : ∀ (X : C), IsMulCommutative (X ⟶ M)
⊢ (β_ M M).hom ≫ μ = μ

Tactic:
simp [mul_eq_mul, comp_mul, mul_comm]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
inst✝ : CartesianMonoidalCategory D
F : C ⥤ D
A B B' : C
g : B ⟶ B'
⊢ F.map (A ◁ g) ≫ prodComparison F A B' = prodComparison F A B ≫ F.obj A ◁ F.map g

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

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
inst✝ : CartesianMonoidalCategory D
F : C ⥤ D
A B A' : C
f : A ⟶ A'
⊢ F.map (f ▷ B) ≫ prodComparison F A' B = prodComparison F A B ≫ F.map f ▷ F.obj B

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

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : CartesianMonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : CartesianMonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : CartesianMonoidalCategory E
F✝ : C ⥤ D
G : D ⥤ E
X✝¹ Y Z : C
inst✝¹ : F✝.OplaxMonoidal
inst✝ : PreservesFiniteProducts F✝
F : C ⥤ D
X✝ Y✝ : C
f : X✝ ⟶ Y✝
X : C
⊢ CartesianMonoidalCategory.prodComparison F X✝ X ≫ F.map f ▷ F.obj X =
    F.map (f ▷ X) ≫ CartesianMonoidalCategory.prodComparison F Y✝ X

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

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : CartesianMonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : CartesianMonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : CartesianMonoidalCategory E
F✝ : C ⥤ D
G : D ⥤ E
X✝¹ Y Z : C
inst✝¹ : F✝.OplaxMonoidal
inst✝ : PreservesFiniteProducts F✝
F : C ⥤ D
X✝ Y✝ X : C
g : X✝ ⟶ Y✝
⊢ CartesianMonoidalCategory.prodComparison F X X✝ ≫ F.obj X ◁ F.map g =
    F.map (X ◁ g) ≫ CartesianMonoidalCategory.prodComparison F X Y✝

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

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : CartesianMonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : CartesianMonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : CartesianMonoidalCategory E
F✝ : C ⥤ D
G : D ⥤ E
X Y Z : C
inst✝¹ : F✝.OplaxMonoidal
inst✝ : PreservesFiniteProducts F✝
F : C ⥤ D
x✝² x✝¹ x✝ : C
⊢ CartesianMonoidalCategory.prodComparison F (x✝² ⊗ x✝¹) x✝ ≫
      CartesianMonoidalCategory.prodComparison F x✝² x✝¹ ▷ F.obj x✝ ≫ (α_ (F.obj x✝²) (F.obj x✝¹) (F.obj x✝)).hom =
    F.map (α_ x✝² x✝¹ x✝).hom ≫
      CartesianMonoidalCategory.prodComparison F x✝² (x✝¹ ⊗ x✝) ≫
        F.obj x✝² ◁ CartesianMonoidalCategory.prodComparison F x✝¹ x✝

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

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : CartesianMonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : CartesianMonoidalCategory D
F : C ⥤ D
inst✝¹ : F.Monoidal
inst✝ : PreservesFiniteProducts F
X Y : C
⊢ μ F X Y = (prodComparisonIso F X Y).inv

Tactic:
by
  change (μIso F X Y).symm.inv = _; congr; ext : 1; simpa using δ_of_cartesianMonoidalCategory F X Y

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.Convolution

Goal state before:
pp: R : Type u_1
C : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring C
inst✝ : HopfAlgebra R C
⊢ mul' R (C ⊗[R] C) ∘ₗ (δ ⊗ₘ δ) ∘ₗ (id ⊗ₘ antipode R) ∘ₗ δ = δ ∘ₗ mul' R C ∘ₗ (id ⊗ₘ antipode R) ∘ₗ δ

Tactic:
by
        have : (μ ∘ₗ (δ ⊗ₘ δ) : C ⊗[R] C →ₗ[R] C ⊗[R] C) = δ ∘ₗ μ := by ext; simp
        simp [this, ← comp_assoc]

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
l : ι →₀ R
i : ι
⊢ (ε i) (lc e l) = l i

Tactic:
lc,

Goal state after:
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
l : ι →₀ R
i : ι
⊢ (ε i) (l.sum fun i a ↦ a • e i) = l i
Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
h : ∀ (n m : ℕ) (f : Matrix (Fin n) (Fin m) R) (g : Matrix (Fin m) (Fin n) R), f * g = 1 → g * f = 1 → n = m
n m : ℕ
e : (Fin n → R) ≃ₗ[R] Fin m → R
⊢ toMatrixRight' ↑e * toMatrixRight' ↑e.symm = 1

Tactic:
by simp [← toMatrixRight'_comp]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
h : ∀ (n m : ℕ) (f : Matrix (Fin n) (Fin m) R) (g : Matrix (Fin m) (Fin n) R), f * g = 1 → g * f = 1 → n = m
n m : ℕ
e : (Fin n → R) ≃ₗ[R] Fin m → R
⊢ toMatrixRight' ↑e.symm * toMatrixRight' ↑e = 1

Tactic:
by simp [← toMatrixRight'_comp]

Goal state after:
Module: Mathlib.LinearAlgebra.Coevaluation

Goal state before:
pp: K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ ∑ x, ((Basis.ofVectorSpace K V).dualBasis j) ((Basis.ofVectorSpace K V) x) ⊗ₜ[K] (Basis.ofVectorSpace K V).coord x =
    1 ⊗ₜ[K] (Basis.ofVectorSpace K V).dualBasis j

Tactic:
simp only [Basis.coe_dualBasis, Basis.coord_apply, Basis.repr_self_apply, TensorProduct.ite_tmul]

Goal state after:
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (∑ x, if x = j then 1 ⊗ₜ[K] (Basis.ofVectorSpace K V).coord x else 0) = 1 ⊗ₜ[K] (Basis.ofVectorSpace K V).coord j
Module: Mathlib.LinearAlgebra.Coevaluation

Goal state before:
pp: K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (LinearMap.lTensor V (contractLeft K V))
      ((TensorProduct.assoc K V (Dual K V) V)
        ((LinearMap.rTensor V (coevaluation K V)) (1 ⊗ₜ[K] (Basis.ofVectorSpace K V) j))) =
    (TensorProduct.rid K V).symm ((TensorProduct.lid K V) (1 ⊗ₜ[K] (Basis.ofVectorSpace K V) j))

Tactic:
lid_tmul,

Goal state after:
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (LinearMap.lTensor V (contractLeft K V))
      ((TensorProduct.assoc K V (Dual K V) V)
        ((LinearMap.rTensor V (coevaluation K V)) (1 ⊗ₜ[K] (Basis.ofVectorSpace K V) j))) =
    (TensorProduct.rid K V).symm (1 • (Basis.ofVectorSpace K V) j)
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: V : Type uV
inst✝³ : AddCommMonoid V
R : Type u_1
inst✝² : Semiring R
inst✝¹ : Module R V
inst✝ : Projective R V
v : V
⊢ (∀ (φ : Dual R V), φ v = 0) ↔ v = 0

Tactic:
refine ⟨fun h ↦ ?_, fun hv ↦ by simp [hv]⟩
  contrapose! h
  exact Projective.exists_dual_ne_zero R h

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
W : Submodule R M
φ : Dual R M
⊢ φ ∈ W.mkQ.dualMap.range ↔ φ ∈ W.dualAnnihilator

Tactic:
rw [LinearMap.mem_range]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
W : Submodule R M
φ : Dual R M
⊢ (∃ y, W.mkQ.dualMap y = φ) ↔ φ ∈ W.dualAnnihilator
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
W : Submodule R M
φ : Dual R M
⊢ φ ∈ W.dualAnnihilator → ∃ y, W.mkQ.dualMap y = φ

Tactic:
· intro hφ
    exists W.dualCopairing ⟨φ, hφ⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
W : Submodule R (Dual R M)
⊢ W.quotDualCoannihilatorToDual.Nondegenerate

Tactic:
by
  rw [Nondegenerate, separatingLeft_iff_ker_eq_bot, separatingRight_iff_flip_ker_eq_bot]
  simp_rw [ker_eq_bot]
  exact ⟨W.quotDualCoannihilatorToDual_injective, W.flip_quotDualCoannihilatorToDual_injective⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K : Type u_1
V₁ : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')
this : F.ker = W ⊓ W'
φ : Dual K V₁
⊢ φ ∈ F.dualMap.range → φ ∈ dualAnnihilator W ⊔ dualAnnihilator W'

Tactic:
rw [LinearMap.mem_range]

Goal state after:
K : Type u_1
V₁ : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')
this : F.ker = W ⊓ W'
φ : Dual K V₁
⊢ (∃ y, F.dualMap y = φ) → φ ∈ dualAnnihilator W ⊔ dualAnnihilator W'
Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ⋯
Q : C := ⋯
s : Q ⟶ P := ⋯
t : Q ⟶ P := ⋯
I : C := ⋯
i : P ⟶ I := ⋯
⊢ Cofan fun f ↦ (K ⋙ G).obj f.fst.1

Tactic:
refine Cofan.mk (G.obj Q) fun j => G.map ?_

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f ↦ K.obj f.fst.1
s : Q ⟶ P := Sigma.desc fun f ↦ K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f ↦ colimit.ι (Discrete.functor K.obj) { as := f.fst.1 }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
j : (p : J × J) × (p.1 ⟶ p.2)
⊢ K.obj j.fst.1 ⟶ Q
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
hf : NormalMono f
X' Y' : C
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
this : Arrow.Hom.left e.inv ≫ f = f' ≫ Arrow.Hom.right e.inv
⊢ f' ≫ Arrow.Hom.right e.inv ≫ g = 0

Tactic:
rw [← reassoc_of% this, hf.w, comp_zero]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : HasZeroMorphisms C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gn : NormalEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
⊢ IsColimit (CokernelCofork.ofπ h ⋯)

Tactic:
letI hn := regularOfIsPushoutSndOfRegular gn.regularEpi comm t

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : HasZeroMorphisms C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gn : NormalEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
hn : RegularEpi h := regularOfIsPushoutSndOfRegular (NormalEpi.regularEpi g) comm t
⊢ IsColimit (CokernelCofork.ofπ h ⋯)
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
hf : NormalEpi f
X' Y' : C
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
⊢ (g ≫ Arrow.Hom.left e.hom) ≫ f' = 0

Tactic:
have := Arrow.w e.hom

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
hf : NormalEpi f
X' Y' : C
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
this : Arrow.Hom.left e.hom ≫ (Arrow.mk f').hom = (Arrow.mk f).hom ≫ Arrow.Hom.right e.hom
⊢ (g ≫ Arrow.Hom.left e.hom) ≫ f' = 0
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi f
R : C
e : Y ⟶ R
h : pullback.snd f g ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc 0 e
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
⊢ e = 0

Tactic:
have :=
      epiIsCokernelOfKernel _
        (PullbackToBiproductIsKernel.isLimitPullbackToBiproduct f g)

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi f
R : C
e : Y ⟶ R
h : pullback.snd f g ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc 0 e
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this : IsColimit (CokernelCofork.ofπ (biprod.desc f (-g)) ⋯)
⊢ e = 0
Module: Mathlib.Algebra.Homology.ShortComplex.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Category.{v_3, u_3} E
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
inst✝¹ : HasZeroMorphisms E
S S₁ S₂ S₃ : ShortComplex C
F : C ⥤ D
inst✝ : F.PreservesZeroMorphisms
X✝ Y✝ : ShortComplex C
φ : X✝ ⟶ Y✝
⊢ F.map φ.τ₂ ≫ (Y✝.map F).g = (X✝.map F).g ≫ F.map φ.τ₃

Tactic:
by
        dsimp
        simp only [← F.map_comp, φ.comm₂₃]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi g
R : C
e : X ⟶ R
h : pullback.fst f g ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc e 0
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
⊢ e = 0

Tactic:
have :=
      epiIsCokernelOfKernel _
        (PullbackToBiproductIsKernel.isLimitPullbackToBiproduct f g)

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi g
R : C
e : X ⟶ R
h : pullback.fst f g ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc e 0
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this : IsColimit (CokernelCofork.ofπ (biprod.desc f (-g)) ⋯)
⊢ e = 0
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
β : ↑B
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ 1 • x = x

Tactic:
one_smul

Goal state after:
A B : GrpCat
f : A ⟶ B
β : ↑B
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ x = x
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : S.LeftHomologyData
A : C
hf : S.f = 0
c : KernelFork S.g
hc : IsLimit c
⊢ ((hc.ofIsoLimit (Fork.ext (Iso.refl c.pt) ⋯)).lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 c.pt) ≫ Fork.ι c = 0 ≫ Fork.ι c

Tactic:
by
    dsimp
    simp only [comp_id, zero_comp, Fork.IsLimit.lift_ι, Fork.ι_ofι, hf]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : S.LeftHomologyData
A : C
hf : S.f = 0
c : KernelFork S.g
hc : IsLimit c
⊢ (hc.ofIsoLimit (Fork.ext (Iso.refl c.pt) ⋯)).lift (KernelFork.ofι S.f ⋯) ≫ Fork.ι c = 0 ≫ Fork.ι c

Tactic:
by
    dsimp
    simp only [comp_id, zero_comp, Fork.IsLimit.lift_ι, Fork.ι_ofι, hf]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ S₄ : ShortComplex C
φ : S₁ ⟶ S₂
h₁✝ : S₁.HomologyData
h₂✝ : S₂.HomologyData
inst✝ : S.HasHomology
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
⊢ IsIso (leftRightHomologyComparison' h₁ h₂)

Tactic:
by
  rw [leftRightHomologyComparison'_compatibility h₁ S.homologyData.left h₂
    S.homologyData.right]
  infer_instance

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂ := rightHomologyMapData φ h₁ h₂
⊢ (rightHomologyMap' φ h₁ h₂).op = leftHomologyMap' (opMap φ) h₂.op h₁.op

Tactic:
simp only [γ.rightHomologyMap'_eq, γ.op.leftHomologyMap'_eq,
    RightHomologyMapData.op_φH]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
a : S₁ ⟶ S₂
⊢ (a + 0).τ₁ = a.τ₁

Tactic:
apply add_zero

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: case h₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
a : S₁ ⟶ S₂
⊢ (a + 0).τ₂ = a.τ₂

Tactic:
apply add_zero

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: case h₃
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
a : S₁ ⟶ S₂
⊢ (a + 0).τ₃ = a.τ₃

Tactic:
apply add_zero

Goal state after: