mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B C D T✝ : CommAlgCat R
f : A ⟶ T✝
g : B ⟶ T✝
⊢ (A.binaryCofan B).inl ≫ ofHom (Algebra.TensorProduct.lift (Hom.hom f) (Hom.hom g) ⋯) = f

Tactic:
ext1

Goal state after:
R : Type u
inst✝ : CommRing R
A B C D T✝ : CommAlgCat R
f : A ⟶ T✝
g : B ⟶ T✝
⊢ Hom.hom ((A.binaryCofan B).inl ≫ ofHom (Algebra.TensorProduct.lift (Hom.hom f) (Hom.hom g) ⋯)) = Hom.hom f
Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B C D T✝ : CommAlgCat R
f : A ⟶ T✝
g : B ⟶ T✝
⊢ (A.binaryCofan B).inr ≫ ofHom (Algebra.TensorProduct.lift (Hom.hom f) (Hom.hom g) ⋯) = g

Tactic:
ext1

Goal state after:
R : Type u
inst✝ : CommRing R
A B C D T✝ : CommAlgCat R
f : A ⟶ T✝
g : B ⟶ T✝
⊢ Hom.hom ((A.binaryCofan B).inr ≫ ofHom (Algebra.TensorProduct.lift (Hom.hom f) (Hom.hom g) ⋯)) = Hom.hom g
Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B C D T✝ : CommAlgCat R
f : A ⟶ T✝
g : B ⟶ T✝
m : (A.binaryCofan B).pt ⟶ T✝
hm₁ : (A.binaryCofan B).inl ≫ m = f
hm₂ : (A.binaryCofan B).inr ≫ m = g
⊢ m = ofHom (Algebra.TensorProduct.lift (Hom.hom f) (Hom.hom g) ⋯)

Tactic:
ext1

Goal state after:
R : Type u
inst✝ : CommRing R
A B C D T✝ : CommAlgCat R
f : A ⟶ T✝
g : B ⟶ T✝
m : (A.binaryCofan B).pt ⟶ T✝
hm₁ : (A.binaryCofan B).inl ≫ m = f
hm₂ : (A.binaryCofan B).inr ≫ m = g
⊢ Hom.hom m = Hom.hom (ofHom (Algebra.TensorProduct.lift (Hom.hom f) (Hom.hom g) ⋯))
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
a b : F.OplaxMonoidal
⊢ a = b

Tactic:
ext1

Goal state after:
case η
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
a b : F.OplaxMonoidal
⊢ η F = η F

case δ
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
a b : F.OplaxMonoidal
⊢ δ F = δ F
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: case δ
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
a b : F.OplaxMonoidal
⊢ δ F = δ F

Tactic:
ext1

Goal state after:
case δ
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
a b : F.OplaxMonoidal
x✝ : C
⊢ δ F x✝ = δ F x✝
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: case δ
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
a b : F.OplaxMonoidal
x✝ : C
⊢ δ F x✝ = δ F x✝

Tactic:
ext1

Goal state after:
case δ
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
a b : F.OplaxMonoidal
x✝¹ x✝ : C
⊢ δ F x✝¹ x✝ = δ F x✝¹ x✝
Module: Mathlib.RingTheory.HopfAlgebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Bialgebra R A
antipode : A →ₗ[R] A
antipode_convMul_id : toConv antipode * toConv LinearMap.id = 1
id_convMul_antipode : toConv LinearMap.id * toConv antipode = 1
⊢ mul' R A ∘ₗ lTensor A antipode ∘ₗ comul = Algebra.linearMap R A ∘ₗ counit

Tactic:
by simpa using! congr(($id_convMul_antipode).ofConv)

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
A X : C
inst✝ : Closed A
⊢ (ihom.coev A).app ((𝟭 C).obj X) ≫ 𝟙 ((ihom A).obj (A ⊗ (𝟭 C).obj X)) = (ihom.coev A).app X

Tactic:
apply comp_id

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) (l i • e i) = l i

pp: case h₀
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 : ι
⊢ ∀ (b : ι), l b ≠ 0 → b ≠ i → (ε i) (l b • e b) = 0

pp: case h₁
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 : ι
⊢ l i = 0 → (ε i) (0 • e i) = 0

Tactic:
· simp [h.eval_same, smul_eq_mul]

Goal state after:
case h₀
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 : ι
⊢ ∀ (b : ι), l b ≠ 0 → b ≠ i → (ε i) (l b • e b) = 0

case h₁
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 : ι
⊢ l i = 0 → (ε i) (0 • e i) = 0
Module: Mathlib.LinearAlgebra.Dimension.DivisionRing

Goal state before:
pp: case e_a.refine_2
K : Type u
V V₁ V₂ V₃ : Type v
inst✝⁸ : DivisionRing K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module K V₁
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
db : V₂ →ₗ[K] V
eb : V₃ →ₗ[K] V
cd : V₁ →ₗ[K] V₂
ce : V₁ →ₗ[K] V₃
hde : ⊤ ≤ db.range ⊔ eb.range
hgd : cd.ker = ⊥
eq : db ∘ₗ cd = eb ∘ₗ ce
eq₂ : ∀ (d : V₂) (e : V₃), db d = eb e → ∃ c, cd c = d ∧ ce c = e
hf : Surjective ⇑(db.coprod eb)
L : V₁ →ₗ[K] ↥(db.coprod eb).ker := LinearMap.codRestrict (db.coprod eb).ker (cd.prod (-ce)) ⋯
⊢ ⊤ ≤ comap (db.coprod eb).ker.subtype (cd.prod (-ce)).range

Tactic:
← map_le_iff_le_comap,

Goal state after:
case e_a.refine_2
K : Type u
V V₁ V₂ V₃ : Type v
inst✝⁸ : DivisionRing K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module K V₁
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
db : V₂ →ₗ[K] V
eb : V₃ →ₗ[K] V
cd : V₁ →ₗ[K] V₂
ce : V₁ →ₗ[K] V₃
hde : ⊤ ≤ db.range ⊔ eb.range
hgd : cd.ker = ⊥
eq : db ∘ₗ cd = eb ∘ₗ ce
eq₂ : ∀ (d : V₂) (e : V₃), db d = eb e → ∃ c, cd c = d ∧ ce c = e
hf : Surjective ⇑(db.coprod eb)
L : V₁ →ₗ[K] ↥(db.coprod eb).ker := LinearMap.codRestrict (db.coprod eb).ker (cd.prod (-ce)) ⋯
⊢ Submodule.map (db.coprod eb).ker.subtype ⊤ ≤ (cd.prod (-ce)).range
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: K : Type u
V : Type v
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
V₂ : Type v'
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : FiniteDimensional K V
inst✝ : FiniteDimensional K V₂
H : finrank K V = finrank K V₂
f : V →ₗ[K] V₂
⊢ f.ker = ⊥ ↔ f.range = ⊤

Tactic:
rw [range_eq_top, ker_eq_bot, injective_iff_surjective_of_finrank_eq_finrank H]

Goal state after:
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsRefl
p : Submodule R₁ M₁
x✝¹ x✝ : ↥p
⊢ ((B.domRestrict₁₂ p p) x✝¹) x✝ = 0 → ((B.domRestrict₁₂ p p) x✝) x✝¹ = 0

Tactic:
by
  simp_rw [domRestrict₁₂_apply]
  exact H _ _

Goal state after:
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
M : Type u_5
M₁ : Type u_6
M₃ : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
I : R →+* R
B : M →ₗ[R] M →ₛₗ[I] M₃
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃
f : M →ₗ[R] M₁
g : M₁ →ₗ[R] M
⊢ B.IsAdjointPair B' ⇑f ⇑g ↔ B' ∘ₗ f = B.compl₂ g

Tactic:
by
  constructor <;> intro h
  · ext x y
    rw [comp_apply, compl₂_apply]
    exact h x y
  · intro _ _
    rw [← compl₂_apply, ← comp_apply, h]

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: case inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
h : Function.Bijective ⇑(dualTensorHom R M N)
h✝ : Module.Finite R M
⊢ Function.Bijective ⇑(finsuppLinearMap R)

Tactic:
apply finsuppLinearMap_bijective_of_moduleFinite

Goal state after:
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : M →ₗ[R] M →ₗ[R] R
hB : B.IsSymm
W : Submodule R M
hW : IsCompl W B.ker
hB' : (B.domRestrict₁₂ W W).IsRefl
x : M
hx : x ∈ W
hx' : ∀ (y : ↥W), ((B.domRestrict₁₂ W W) ⟨x, hx⟩) y = 0
⊢ ∀ y ∈ W, (B x) y = 0

Tactic:
simpa [Subtype.forall] using! hx'

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

Goal state before:
pp: K : Type uK
V : Type uV
inst✝³ : CommSemiring K
inst✝² : AddCommMonoid V
inst✝¹ : Module K V
inst✝ : Projective K V
⊢ Nontrivial (Dual K V) ↔ Nontrivial V

Tactic:
by
  contrapose!; exact subsingleton_dual_iff K

Goal state after:
Module: Mathlib.Algebra.Category.FGModuleCat.Colimits

Goal state before:
pp: J✝ : Type
inst✝⁴ : SmallCategory J✝
inst✝³ : FinCategory J✝
k : Type u
inst✝² : Ring k
J : Type
inst✝¹ : Finite J
Z : J → ModuleCat k
inst✝ : ∀ (j : J), Module.Finite k ↑(Z j)
⊢ Module.Finite k ↑(∐ fun j ↦ Z j)

Tactic:
exact (Module.Finite.equiv_iff (ModuleCat.coprodIsoDirectSum Z).toLinearEquiv).mpr inferInstance

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

Goal state before:
pp: case right
K : Type u_1
V₁ : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
⊢ (Submodule.dualPairing W).SeparatingRight

Tactic:
· intro x h
    rw [← forall_dual_apply_eq_zero_iff K x]
    intro φ
    simpa only [Submodule.dualPairing_apply, dualLift_of_subtype] using
      h (Submodule.Quotient.mk (W.dualLift φ))

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
hn : NormalMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
W : C
h' : S ⟶ W
⊢ f ≫ h ≫ h' = g ≫ k ≫ h'

Tactic:
simp only [← Category.assoc, eq_whisker comm]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
P Q : C
f : P ⟶ Q
I : C := Abelian.image f
p : P ⟶ Abelian.image f := Abelian.factorThruImage f
i : kernel (cokernel.π f) ⟶ Q := kernel.ι (cokernel.π f)
R : C
g : I ⟶ R
hpg : p ≫ g = 0
u : kernel g ⟶ Q := kernel.ι g ≫ i
hu : NormalMono u
h : Q ⟶ NormalMono.Z u := NormalMono.g
t : P ⟶ kernel g
ht : t ≫ kernel.ι g = p
fh : f ≫ h = 0
l : cokernel f ⟶ NormalMono.Z u
hl : cokernel.π f ≫ l = h
hih : i ≫ h = 0
s : kernel (cokernel.π f) ⟶ kernel g
hs : s ≫ u = i
⊢ g = 0

Tactic:
have hs' : (s ≫ kernel.ι g) ≫ i = 𝟙 I ≫ i := by rw [Category.assoc, hs, Category.id_comp]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
P Q : C
f : P ⟶ Q
I : C := Abelian.image f
p : P ⟶ Abelian.image f := Abelian.factorThruImage f
i : kernel (cokernel.π f) ⟶ Q := kernel.ι (cokernel.π f)
R : C
g : I ⟶ R
hpg : p ≫ g = 0
u : kernel g ⟶ Q := kernel.ι g ≫ i
hu : NormalMono u
h : Q ⟶ NormalMono.Z u := NormalMono.g
t : P ⟶ kernel g
ht : t ≫ kernel.ι g = p
fh : f ≫ h = 0
l : cokernel f ⟶ NormalMono.Z u
hl : cokernel.π f ≫ l = h
hih : i ≫ h = 0
s : kernel (cokernel.π f) ⟶ kernel g
hs : s ≫ u = i
hs' : (s ≫ kernel.ι g) ≫ i = 𝟙 I ≫ i
⊢ g = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroMorphisms C
inst✝⁴ : HasFiniteCoproducts C
inst✝³ : HasCokernels C
inst✝² : IsNormalEpiCategory C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst✝¹ : Epi a
inst✝ : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
a' : (CokernelCofork.ofπ a hfa).pt ⟶ cokernel (coprod.desc f g)
ha' : Cofork.π (CokernelCofork.ofπ a hfa) ≫ a' = cokernel.π (coprod.desc f g)
b' : (CokernelCofork.ofπ b hgb).pt ⟶ cokernel (coprod.desc f g)
hb' : Cofork.π (CokernelCofork.ofπ b hgb) ≫ b' = cokernel.π (coprod.desc f g)
s : PushoutCocone a b
⊢ f ≫ a ≫ s.inl = 0 ≫ s.inl

Tactic:
rw [← Category.assoc, eq_whisker hfa]

Goal state after:
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
b : ↑B
hb : b ∈ (Hom.hom f).range
⊢ b • ↑(Hom.hom f).range = 1 • ↑(Hom.hom f).range

Tactic:
rw [leftCoset_eq_iff, mul_one]

Goal state after:
A B : GrpCat
f : A ⟶ B
b : ↑B
hb : b ∈ (Hom.hom f).range
⊢ b⁻¹ ∈ (Hom.hom f).range
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 : ShortComplex C
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
⊢ h.ι ≫ h.descQ k ⋯ = 0

Tactic:
by
  rw [show 0 = h.ι ≫ h.g' ≫ x by simp]
  congr 1
  simp only [← cancel_epi h.p, hx, p_descQ, p_g'_assoc]

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₂
inst✝¹ : S₁.HasRightHomology
inst✝ : S₂.HasRightHomology
⊢ opcyclesMap φ ≫ h₂.opcyclesIso.hom = h₁.opcyclesIso.hom ≫ γ.φQ

Tactic:
simp only [γ.opcyclesMap_eq, assoc, Iso.inv_hom_id, comp_id]

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

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
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
S : ShortComplex C
h : S.LeftHomologyData
inst✝ : h.IsPreservedBy F
h' : S.LeftHomologyData
this : PreservesColimit (parallelPair h.f' 0) F
e : parallelPair h.f' 0 ≅ parallelPair h'.f' 0 :=
  parallelPair.ext (Iso.refl ((parallelPair h.f' 0).obj WalkingParallelPair.zero))
    (ShortComplex.cyclesMapIso' (Iso.refl S) h h') ⋯ ⋯
⊢ PreservesColimit (parallelPair h'.f' 0) F

Tactic:
exact preservesColimit_of_iso_diagram F e

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₃ ⟶ S₁
⊢ (ψ ≫ φ₁).τ₂ = S₃.g ≫ ψ.τ₃ ≫ h.h₂ + (ψ.τ₂ ≫ h.h₁) ≫ S₂.f + (ψ ≫ φ₂).τ₂

Tactic:
comp_τ₂,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₃ ⟶ S₁
⊢ ψ.τ₂ ≫ φ₁.τ₂ = S₃.g ≫ ψ.τ₃ ≫ h.h₂ + (ψ.τ₂ ≫ h.h₁) ≫ S₂.f + (ψ ≫ φ₂).τ₂
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₃ ⟶ S₁
⊢ ψ.τ₂ ≫ φ₁.τ₂ = S₃.g ≫ ψ.τ₃ ≫ h.h₂ + (ψ.τ₂ ≫ h.h₁) ≫ S₂.f + (ψ ≫ φ₂).τ₂

Tactic:
comp_τ₂,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₃ ⟶ S₁
⊢ ψ.τ₂ ≫ φ₁.τ₂ = S₃.g ≫ ψ.τ₃ ≫ h.h₂ + (ψ.τ₂ ≫ h.h₁) ≫ S₂.f + ψ.τ₂ ≫ φ₂.τ₂
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₂ ⟶ S₃
⊢ (φ₁ ≫ ψ).τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + (φ₂ ≫ ψ).τ₂

Tactic:
comp_τ₂,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₂ ⟶ S₃
⊢ φ₁.τ₂ ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + (φ₂ ≫ ψ).τ₂
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₂ ⟶ S₃
⊢ φ₁.τ₂ ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + (φ₂ ≫ ψ).τ₂

Tactic:
comp_τ₂,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₂ ⟶ S₃
⊢ φ₁.τ₂ ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + φ₂.τ₂ ≫ ψ.τ₂
Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact

Goal state before:
pp: case mpr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : S.ShortExact
inst✝ : Balanced C
this✝¹ : HasZeroObject C
this✝ : Mono S.f
this : Epi S.g
hX₁ : IsZero S.X₁
⊢ IsIso S.g

Tactic:
have : Mono S.g := (S.exact_iff_mono (hX₁.eq_of_src _ _)).1 hS.exact

Goal state after:
case mpr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : S.ShortExact
inst✝ : Balanced C
this✝² : HasZeroObject C
this✝¹ : Mono S.f
this✝ : Epi S.g
hX₁ : IsZero S.X₁
this : Mono S.g
⊢ IsIso S.g
Module: Mathlib.CategoryTheory.Adjunction.Reflective

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
j : C ⥤ D
inst✝¹ : Coreflective j
A : D
inst✝ : IsSplitEpi ((coreflectorAdjunction j).counit.app A)
ε : coreflector j ⋙ j ⟶ 𝟭 D := (coreflectorAdjunction j).counit
this✝¹ : IsIso (ε.app (j.obj ((coreflector j).obj A)))
this✝ : Mono (ε.app A)
this : IsIso (ε.app A)
⊢ j.essImage A

Tactic:
exact (coreflectorAdjunction j).mem_essImage_of_counit_isIso A

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.LeftHomologyData
⊢ S.Exact ↔ Epi h.f'

Tactic:
constructor
  · intro hS
    exact hS.epi_f' h
  · intro
    simp only [h.exact_iff, IsZero.iff_id_eq_zero, ← cancel_epi h.π, ← cancel_epi h.f',
      comp_id, h.f'_π, comp_zero]

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

Goal state before:
pp: case refine_1
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f✝ : X✝ ⟶ Y
inst✝¹ : HasKernel f✝
inst✝ : HasCokernels C
X A B : C
f : A ⟶ X
g : B ⟶ X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ f ≫ cokernel.π g = 0

Tactic:
← Subobject.ofMkLEMk_comp h,

Goal state after:
case refine_1
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f✝ : X✝ ⟶ Y
inst✝¹ : HasKernel f✝
inst✝ : HasCokernels C
X A B : C
f : A ⟶ X
g : B ⟶ X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ (ofMkLEMk f g h ≫ g) ≫ cokernel.π g = 0
Module: Mathlib.CategoryTheory.Subobject.Limits

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f : X✝ ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasKernels C
X : C
A B : Cᵒᵖ
g : B ⟶ op X
hg : Mono g
i : A ≅ B
hf : Mono (i.hom ≫ g)
⊢ Subobject.mk (kernel.ι (i.hom ≫ g).unop) = Subobject.mk (kernel.ι g.unop)

Tactic:
refine Subobject.mk_eq_mk_of_comm _ _ ?_ ?_

Goal state after:
case refine_1
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f : X✝ ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasKernels C
X : C
A B : Cᵒᵖ
g : B ⟶ op X
hg : Mono g
i : A ≅ B
hf : Mono (i.hom ≫ g)
⊢ kernel (i.hom ≫ g).unop ≅ kernel g.unop

case refine_2
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f : X✝ ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasKernels C
X : C
A B : Cᵒᵖ
g : B ⟶ op X
hg : Mono g
i : A ≅ B
hf : Mono (i.hom ≫ g)
⊢ Iso.hom ?refine_1 ≫ kernel.ι g.unop = kernel.ι (i.hom ≫ g).unop
Module: Mathlib.CategoryTheory.Subobject.Limits

Goal state before:
pp: case refine_1
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f✝ : X✝ ⟶ Y
inst✝¹ : HasKernel f✝
inst✝ : HasKernels C
X : C
A B : Cᵒᵖ
f : A ⟶ op X
g : B ⟶ op X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ kernel.ι f.unop ≫ g.unop = 0

Tactic:
← Subobject.ofMkLEMk_comp h,

Goal state after:
case refine_1
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f✝ : X✝ ⟶ Y
inst✝¹ : HasKernel f✝
inst✝ : HasKernels C
X : C
A B : Cᵒᵖ
f : A ⟶ op X
g : B ⟶ op X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ kernel.ι f.unop ≫ (ofMkLEMk g f h ≫ f).unop = 0
Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor

Goal state before:
pp: case refine_1
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
x✝ : ∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact
hF : ∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact := x✝
X Y : C
f : X ⟶ Y
⊢ PreservesLimit (parallelPair f 0) F

pp: case refine_2
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
x✝ : ∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact
hF : ∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact := x✝
X Y : C
f : X ⟶ Y
⊢ PreservesColimit (parallelPair f 0) F

Tactic:
· have h := (preservesFiniteLimits_tfae F |>.out 0 2 |>.1 fun S hS ↦
        And.intro (hF S hS).exact (hF S hS).mono_f)
      exact h f

Goal state after:
case refine_2
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
x✝ : ∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact
hF : ∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact := x✝
X Y : C
f : X ⟶ Y
⊢ PreservesColimit (parallelPair f 0) F
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: case e'_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
A : C
f₁ f₂ : Subobject A
⊢ min f₁ = (inf.obj (Quotient.mk'' (representative.obj f₁))).obj

Tactic:
ext1

Goal state after:
case e'_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
A : C
f₁ f₂ x✝ : Subobject A
⊢ f₁ ⊓ x✝ = (inf.obj (Quotient.mk'' (representative.obj f₁))).obj x✝