mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.ObjectProperty.Retract

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
⊢ ∀ {X Y : C} (x : Retract X Y), P.retractClosure Y → P.retractClosure X

Tactic:
rintro X Y r₁ ⟨Z, hZ, ⟨r₂⟩⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
X Y : C
r₁ : Retract X Y
Z : C
hZ : P Z
r₂ : Retract Y Z
⊢ P.retractClosure X
Module: Mathlib.CategoryTheory.ObjectProperty.Retract

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v, u} P
inst✝ : LocallySmall.{w, v, u} C
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : P ≤ Q.isoClosure
α : Type (max u v) := (X : Subtype Q) × { p // p ≫ p = p }
g : {X Y : C} → Retract Y X → Q X → α := fun {X Y} h hX ↦ ⟨⟨X, hX⟩, ⟨h.r ≫ h.i, ⋯⟩⟩
R : α → Prop := fun a ↦ ∃ X Y h, ∃ (hX : Q X), g h hX = a
X Y : Subtype R → C
h : (a : Subtype R) → Retract (Y a) (X a)
hX : ∀ (a : Subtype R), ∃ (hX : Q (X a)), g (h a) hX = ↑a
y x : C
hx : Q x
r : Retract y x
⊢ ∃ a, ∃ (h₁ : Q (X a)), g (h a) h₁ = g r hx

Tactic:
obtain ⟨_, hr⟩ := hX ⟨⟨⟨_, hx⟩, r.r ≫ r.i, by simp⟩, ⟨_, _, r, hx, rfl⟩⟩
      exact ⟨_, _, hr⟩

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
inst✝ : HasPushouts C
S T : C
f : T ⟶ X
g : T ⟶ Y
i : S ⟶ T
⊢ IsPushout (pushout.map i i (i ≫ f) (i ≫ g) f g (𝟙 S) ⋯ ⋯) (pushout.codiagonal i)
    (pushout.map (i ≫ f) (i ≫ g) f g (𝟙 X) (𝟙 Y) i ⋯ ⋯) (f ≫ pushout.inl f g)

Tactic:
← IsPullback.op_iff

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
inst✝ : HasPushouts C
S T : C
f : T ⟶ X
g : T ⟶ Y
i : S ⟶ T
⊢ IsPullback (f ≫ pushout.inl f g).op (pushout.map (i ≫ f) (i ≫ g) f g (𝟙 X) (𝟙 Y) i ⋯ ⋯).op (pushout.codiagonal i).op
    (pushout.map i i (i ≫ f) (i ≫ g) f g (𝟙 S) ⋯ ⋯).op
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : MonObj B
f g h : A ⟶ B
⊢ lift (lift f g ≫ μ) h ≫ μ = lift f (lift g h ≫ μ) ≫ μ

Tactic:
have := lift (lift f g) h ≫= mul_assoc B
  rwa [lift_whiskerRight_assoc, lift_lift_associator_hom_assoc, lift_whiskerLeft_assoc] at this

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

Goal state before:
pp: C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
inst✝ : P.IsClosedUnderLimitsOfShape (Discrete WalkingPair)
X Y : C
hX : P X
hY : P Y
⊢ ∀ (j : Discrete WalkingPair), P ((pair X Y).obj j)

Tactic:
by rintro (_ | _) <;> assumption

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.DivisionRing

Goal state before:
pp: K : Type u
V✝ V₁ V₂ V₃ : Type v
ι : Type w
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V✝
inst✝² : Module K V✝
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
V : Type u₀
x✝¹ : AddCommGroup V
x✝ : Module K V
b : Module.Basis (Module.Free.ChooseBasisIndex K V) K V := Module.Free.chooseBasis K V
⊢ ∃ s, #↑s = Module.rank K V ∧ LinearIndepOn K id s

Tactic:
refine ⟨range b, ?_, b.linearIndependent.linearIndepOn_id⟩

Goal state after:
K : Type u
V✝ V₁ V₂ V₃ : Type v
ι : Type w
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V✝
inst✝² : Module K V✝
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
V : Type u₀
x✝¹ : AddCommGroup V
x✝ : Module K V
b : Module.Basis (Module.Free.ChooseBasisIndex K V) K V := Module.Free.chooseBasis K V
⊢ #↑(range ⇑b) = Module.rank K V
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: R : Type u_2
M : Type u
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : HasRankNullity.{u, u_2} R
inst✝⁵ : StrongRankCondition R
inst✝⁴ : Module.Finite R M
S : Type u_1
inst✝³ : Ring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
N : Submodule S M
⊢ finrank R (M ⧸ N) = finrank R M - finrank R ↥N

Tactic:
rw [← (N.restrictScalars R).finrank_quotient_add_finrank]
  exact Nat.eq_sub_of_add_eq rfl

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Semiring R
n m : ℕ
f : Matrix (Fin m) (Fin n) R
g : Matrix (Fin n) (Fin m) R
⊢ (transposeAddEquiv (Fin m) (Fin m) R) (opEquiv.mapMatrix.symm (opEquiv.mapMatrix f * opEquiv.mapMatrix g)) =
    (transposeAddEquiv (Fin n) (Fin m) R).toEquiv g * (transposeAddEquiv (Fin m) (Fin n) R).toEquiv f

Tactic:
ext; simp [map, mul_apply]

Goal state after:
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
f : V →ₗ[K] V₂
⊢ finrank K ↥f.range + finrank K ↥f.ker = finrank K V

Tactic:
← f.quotKerEquivRange.finrank_eq

Goal state after:
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
f : V →ₗ[K] V₂
⊢ finrank K (V ⧸ f.ker) + finrank K ↥f.ker = finrank K V
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: case refine_1
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₂
this : finrank K ↥f.range + finrank K ↥f.ker = finrank K V
h : f.ker = ⊥
⊢ f.range = ⊤

pp: case refine_2
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₂
this : finrank K ↥f.range + finrank K ↥f.ker = finrank K V
h : f.range = ⊤
⊢ f.ker = ⊥

Tactic:
· rw [h, finrank_bot, add_zero, H] at this
    exact eq_top_of_finrank_eq this

Goal state after:
case refine_2
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₂
this : finrank K ↥f.range + finrank K ↥f.ker = finrank K V
h : f.range = ⊤
⊢ f.ker = ⊥
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: case zero
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
h_contra : ∀ x ≤ finrank K V, ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ x.succ)
hn : 0 ≤ (finrank K V).succ
⊢ 0 ≤ finrank K ↥(LinearMap.ker (f ^ 0))

Tactic:
exact zero_le

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: case left
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
inst✝¹ : Module.Finite R M
inst✝ : Projective R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
g : M →ₗ[R] Fin n → R
eq : f ∘ₗ g = LinearMap.id
⊢ Function.Injective ⇑(lcomp R N f ∘ₗ dualTensorHom R M N)

Tactic:
← dualTensorHom_comp_rTensor_dualMap,

Goal state after:
case left
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
inst✝¹ : Module.Finite R M
inst✝ : Projective R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
g : M →ₗ[R] Fin n → R
eq : f ∘ₗ g = LinearMap.id
⊢ Function.Injective ⇑(dualTensorHom R (Fin n → R) N ∘ₗ rTensor N f.dualMap)
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: R : Type u_2
M : Type u_3
P : Type u_5
Q : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid P
inst✝⁵ : AddCommMonoid Q
inst✝⁴ : Module R M
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : Projective R M
inst✝ : Module.Finite R M
⊢ ↑(lTensorHomEquivHomLTensor R M P Q) = lTensorHomToHomLTensor (RingHom.id R) M P Q

Tactic:
let e := congr (LinearEquiv.refl R P) (dualTensorHomEquiv R M Q)
  have h : Function.Surjective e.toLinearMap := e.surjective
  refine (cancel_right h).1 ?_
  ext f q m
  simp [e, lTensorHomEquivHomLTensor]

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
⊢ B.flip.SeparatingLeft ↔ B.flip.ker = ⊥

Tactic:
separatingLeft_iff_ker_eq_bot

Goal state after:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
⊢ B.flip.ker = ⊥ ↔ B.flip.ker = ⊥
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: R : Type u_7
M : Type u_8
N : Type u_9
ι : Type u_10
κ : Type u_11
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
⊢ dualDistrib R M N ∘ₗ dualDistribInvOfBasis b c = LinearMap.id

Tactic:
apply (b.tensorProduct c).dualBasis.ext
  rintro ⟨i, j⟩
  apply (b.tensorProduct c).ext
  rintro ⟨i', j'⟩
  simp only [dualDistrib, Basis.coe_dualBasis, coe_comp, Function.comp_apply,
    dualDistribInvOfBasis_apply, Basis.coord_apply, Basis.tensorProduct_repr_tmul_apply,
    Basis.repr_self, _root_.map_sum, map_smul, homTensorHomMap_apply, compRight_apply,
    Basis.tensorProduct_apply, LinearMap.coe_sum, Finset.sum_apply, smul_apply, LinearEquiv.coe_coe,
    map_tmul, lid_tmul, smul_eq_mul, id_coe, id_eq]
  rw [Finset.sum_eq_single i, Finset.sum_eq_single j]
  · simpa using mul_comm _ _
  all_goals { intros; simp [*] at * }

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
inst✝² : HasEqualizer f g
inst✝¹ : HasEqualizer (G.map f) (G.map g)
inst✝ : PreservesLimit (parallelPair f g) G
⊢ (iso G f g).inv ≫ G.map (equalizer.ι f g) = equalizer.ι (G.map f) (G.map g)

Tactic:
rw [← Iso.cancel_iso_hom_left (PreservesEqualizer.iso G f g), ← Category.assoc, Iso.hom_inv_id]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
inst✝² : HasEqualizer f g
inst✝¹ : HasEqualizer (G.map f) (G.map g)
inst✝ : PreservesLimit (parallelPair f g) G
⊢ 𝟙 (G.obj (equalizer f g)) ≫ G.map (equalizer.ι f g) = (iso G f g).hom ≫ equalizer.ι (G.map f) (G.map g)
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
inst✝¹ : IsReflexive R M
s : Set (M →ₗ[R] R)
inst✝ : Projective R ((M →ₗ[R] R) ⧸ span R s)
h : ∀ (z : M), z ≠ 0 → ∃ f ∈ s, f z ≠ 0
hn : span R s ≠ ⊤
φ : Dual R (M →ₗ[R] R)
φne : φ ≠ 0
hφ : map φ (span R s) = ⊥
φs : M := (evalEquiv R M).symm φ
f : M →ₗ[R] R
hf : f ∈ s
⊢ f φs = 0

Tactic:
rw [← mem_bot R, ← hφ, mem_map]

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsReflexive R M
s : Set (M →ₗ[R] R)
inst✝ : Projective R ((M →ₗ[R] R) ⧸ span R s)
h : ∀ (z : M), z ≠ 0 → ∃ f ∈ s, f z ≠ 0
hn : span R s ≠ ⊤
φ : Dual R (M →ₗ[R] R)
φne : φ ≠ 0
hφ : map φ (span R s) = ⊥
φs : M := (evalEquiv R M).symm φ
f : M →ₗ[R] R
hf : f ∈ s
⊢ ∃ y ∈ span R s, φ y = f φs
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: case neg
R : Type u_1
M : Type u_5
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y : M
he : (B x) y * (B y) x = (B x) x * (B y) y
hz : (B x) y • x - (B x) x • y = 0
hL : LinearIndependent R ![x, y]
hx : ¬x = 0
h : (B x) x • y - (B x) y • x = 0
⊢ False

Tactic:
sub_eq_add_neg,

Goal state after:
case neg
R : Type u_1
M : Type u_5
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y : M
he : (B x) y * (B y) x = (B x) x * (B y) y
hz : (B x) y • x - (B x) x • y = 0
hL : LinearIndependent R ![x, y]
hx : ¬x = 0
h : (B x) x • y + -((B x) y • x) = 0
⊢ False
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : LinearMap.BilinForm R M
inst✝ : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y : M
hle : ∀ (z : M), 0 ≤ (B z) z
r s : R
hl : r • x + s • y = 0
h0 : r = 0 → s ≠ 0
hr : ¬r = 0
hs : ¬s = 0
⊢ s • y = -(r • x)

Tactic:
← add_eq_zero_iff_eq_neg'

Goal state after:
R : Type u_1
M : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : LinearMap.BilinForm R M
inst✝ : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y : M
hle : ∀ (z : M), 0 ≤ (B z) z
r s : R
hl : r • x + s • y = 0
h0 : r = 0 → s ≠ 0
hr : ¬r = 0
hs : ¬s = 0
⊢ r • x + s • y = 0
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
⊢ W.dualAnnihilator = ⊥ ↔ Subsingleton (Dual R (M ⧸ W))

Tactic:
by
  rw [W.dualQuotEquivDualAnnihilator.toEquiv.subsingleton_congr, subsingleton_iff_eq_bot]

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
D : Type u₂
inst✝² : Category.{v₁, u₂} D
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.IsEquivalence
X Y : C
f : X ⟶ Y
hf : NormalEpi (F.map f)
⊢ F.map (F.preimage ((F.objObjPreimageIso (NormalEpi.W (F.map f))).hom ≫ NormalEpi.g) ≫ f) = F.map 0

Tactic:
simp [hf.w]

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

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c d : X ⟶ Y
⊢ (prod.lift (prod.lift a b) (prod.lift c d) ≫ σ) ≫ prod.fst =
    prod.lift (prod.lift a c ≫ σ) (prod.lift b d ≫ σ) ≫ prod.fst

Tactic:
rw [Category.assoc, σ_comp, prod.lift_map_assoc, prod.lift_fst, prod.lift_fst, prod.lift_fst]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ coequalizer.π (kernel.ι f) 0 ≫ (coimageIsoImage' f).hom =
    coequalizer.π (kernel.ι f) 0 ≫ cokernel.desc (kernel.ι f) (factorThruImage f) ⋯

Tactic:
simp only [← cancel_mono (Limits.image.ι f), IsImage.isoExt_hom, cokernel.π_desc,
    Category.assoc, IsImage.lift_ι, coimageStrongEpiMonoFactorisation_m,
    Limits.image.fac]

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
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (biprod.desc f (-g)) 0
⊢ s.ι ≫ (biprod.fst ≫ f - biprod.snd ≫ g) = 0

Tactic:
sub_eq_add_neg,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (biprod.desc f (-g)) 0
⊢ s.ι ≫ (biprod.fst ≫ f + -biprod.snd ≫ g) = 0
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
s : Cofork (biprod.lift f (-g)) 0
⊢ (f ≫ biprod.inl - g ≫ biprod.inr) ≫ s.π = 0

Tactic:
sub_eq_add_neg,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
s : Cofork (biprod.lift f (-g)) 0
⊢ (f ≫ biprod.inl + -g ≫ biprod.inr) ≫ s.π = 0
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
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ (h₁.i ≫ φ.τ₂) ≫ S₂.g = 0

Tactic:
by rw [assoc, φ.comm₂₃, h₁.wi_assoc, zero_comp]

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₂
inst✝¹ : S₁.HasRightHomology
inst✝ : S₂.HasRightHomology
⊢ (S₁.pOpcycles ≫ opcyclesMap φ).op = S₂.pOpcycles.op ≫ (opMap φ).τ₂

Tactic:
p_opcyclesMap,

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasRightHomology
inst✝ : S₂.HasRightHomology
⊢ (φ.τ₂ ≫ S₂.pOpcycles).op = S₂.pOpcycles.op ≫ (opMap φ).τ₂
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₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₂✝ : IsIso φ.τ₂
h₃ : Mono φ.τ₃
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ IsIso (cyclesMap' φ h₁ h₂)

Tactic:
refine ⟨h₁.liftK (h₂.i ≫ inv φ.τ₂) ?_, ?_, ?_⟩
  · simp only [assoc, ← cancel_mono φ.τ₃, zero_comp, ← φ.comm₂₃, IsIso.inv_hom_id_assoc, h₂.wi]
  · simp only [← cancel_mono h₁.i, assoc, h₁.liftK_i, cyclesMap'_i_assoc,
      IsIso.hom_inv_id, comp_id, id_comp]
  · simp only [← cancel_mono h₂.i, assoc, cyclesMap'_i, h₁.liftK_i_assoc,
      IsIso.inv_hom_id, comp_id, id_comp]

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
a b : S₁ ⟶ S₂
⊢ a - b = a + -b

Tactic:
by ext <;> apply sub_eq_add_neg

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
S : ShortComplex C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
f' : S.X₁ ⟶ kernel S.g := kernel.lift S.g S.f ⋯
hf' : f' = kernel.lift γ f' ⋯ ≫ kernel.ι γ
wπ : f' ≫ cokernel.π (kernel.ι γ) = 0
e : Abelian.image S.f ≅ kernel γ :=
  S.abelianImageToKernelIsKernel.conePointUniqueUpToIso (limit.isLimit (parallelPair (kernel.ι S.g ≫ cokernel.π S.f) 0))
he : e.hom ≫ kernel.ι γ = S.abelianImageToKernel
⊢ kernel.lift γ f' ⋯ ≫ kernel.ι γ = Abelian.factorThruImage S.f ≫ S.abelianImageToKernel

Tactic:
simp only [γ, f', kernel.lift_ι, abelianImageToKernel, ← cancel_mono (kernel.ι S.g),
      assoc]

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
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hl₁ : S₁.LeftHomologyData
hl₂ : S₂.LeftHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : hl₁.IsPreservedBy F
inst✝ : hl₂.IsPreservedBy F
⊢ F.map (cyclesMap' φ hl₁ hl₂) = cyclesMap' (F.mapShortComplex.map φ) (hl₁.map F) (hl₂.map F)

Tactic:
have γ : ShortComplex.LeftHomologyMapData φ hl₁ hl₂ := default

Goal state after:
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
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hl₁ : S₁.LeftHomologyData
hl₂ : S₂.LeftHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : hl₁.IsPreservedBy F
inst✝ : hl₂.IsPreservedBy F
γ : LeftHomologyMapData φ hl₁ hl₂
⊢ F.map (cyclesMap' φ hl₁ hl₂) = cyclesMap' (F.mapShortComplex.map φ) (hl₁.map F) (hl₂.map F)
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
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hl₁ : S₁.LeftHomologyData
hl₂ : S₂.LeftHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : hl₁.IsPreservedBy F
inst✝ : hl₂.IsPreservedBy F
⊢ F.map (leftHomologyMap' φ hl₁ hl₂) = leftHomologyMap' (F.mapShortComplex.map φ) (hl₁.map F) (hl₂.map F)

Tactic:
have γ : ShortComplex.LeftHomologyMapData φ hl₁ hl₂ := default

Goal state after:
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
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hl₁ : S₁.LeftHomologyData
hl₂ : S₂.LeftHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : hl₁.IsPreservedBy F
inst✝ : hl₂.IsPreservedBy F
γ : LeftHomologyMapData φ hl₁ hl₂
⊢ F.map (leftHomologyMap' φ hl₁ hl₂) = leftHomologyMap' (F.mapShortComplex.map φ) (hl₁.map F) (hl₂.map F)
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
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hr₁ : S₁.RightHomologyData
hr₂ : S₂.RightHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : hr₁.IsPreservedBy F
inst✝ : hr₂.IsPreservedBy F
γ : RightHomologyMapData φ hr₁ hr₂
⊢ F.map γ.φQ = (γ.map F).φQ

Tactic:
ShortComplex.RightHomologyMapData.map_φQ

Goal state after:
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
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hr₁ : S₁.RightHomologyData
hr₂ : S₂.RightHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : hr₁.IsPreservedBy F
inst✝ : hr₂.IsPreservedBy F
γ : RightHomologyMapData φ hr₁ hr₂
⊢ F.map γ.φQ = F.map γ.φQ
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
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hr₁ : S₁.RightHomologyData
hr₂ : S₂.RightHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : hr₁.IsPreservedBy F
inst✝ : hr₂.IsPreservedBy F
γ : RightHomologyMapData φ hr₁ hr₂
⊢ F.map (opcyclesMap' φ hr₁ hr₂) = opcyclesMap' (F.mapShortComplex.map φ) (hr₁.map F) (hr₂.map F)

Tactic:
rw [γ.opcyclesMap'_eq, (γ.map F).opcyclesMap'_eq, ShortComplex.RightHomologyMapData.map_φQ]

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₁.g ≫ (-h.h₂) + (-h.h₁) ≫ S₂.f + (-φ₂).τ₂

Tactic:
rw [neg_τ₂, neg_τ₂, h.comm₂, neg_add_rev, comp_neg, neg_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₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f) = -S₁.g ≫ h.h₂ + -h.h₁ ≫ S₂.f + -φ₂.τ₂