mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝ : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : W ⊔ K ∙ v = ⊤
this : W ⊓ K ∙ v = ⊥
⊢ finrank K (V ⧸ W) = 1

Tactic:
by
      have hv₀ : v ≠ 0 := by aesop
      have aux := finrank_sup_add_finrank_inf_eq W (span K {v})
      rw [hW, finrank_span_singleton hv₀, this, finrank_bot, finrank_top,
        ← finrank_quotient_add_finrank W] at aux
      lia

Goal state after:
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
inst✝ : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : W ⊔ K ∙ v = ⊤
⊢ finrank K (V ⧸ W) = 1

Tactic:
suffices W ⊓ span K {v} = ⊥ by
      have hv₀ : v ≠ 0 := by aesop
      have aux := finrank_sup_add_finrank_inf_eq W (span K {v})
      rw [hW, finrank_span_singleton hv₀, this, finrank_bot, finrank_top,
        ← finrank_quotient_add_finrank W] at aux
      lia

Goal state after:
case refine_1
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : W ⊔ K ∙ v = ⊤
⊢ W ⊓ K ∙ v = ⊥
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: K : Type u
V : Type v
W : Type v'
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Module K W
f : V →ₗ[K] W
p : Submodule K W
inst✝¹ : FiniteDimensional K ↥p
inst✝ : FiniteDimensional K ↥f.ker
⊢ lift.{v, v'} (Module.rank K ↥p) + lift.{v', v} (Module.rank K ↥f.ker) < ℵ₀

Tactic:
apply add_lt_aleph0 <;> rwa [lift_lt_aleph0, rank_lt_aleph0_iff]

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

Goal state before:
pp: K : Type u
V : Type v
W : Type v'
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Module K W
f : V →ₗ[K] W
p : Submodule K V
inst✝¹ : FiniteDimensional K (V ⧸ p)
inst✝ : FiniteDimensional K (W ⧸ f.range)
⊢ lift.{v, v'} (Module.rank K (W ⧸ f.range)) + lift.{v', v} (Module.rank K (V ⧸ p)) < ℵ₀

Tactic:
apply add_lt_aleph0 <;> rwa [lift_lt_aleph0, rank_lt_aleph0_iff]

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
⊢ (coevaluation K V) 1 =
    let bV := Basis.ofVectorSpace K V;
    ∑ i, bV i ⊗ₜ[K] bV.coord i

Tactic:
by
  simp only [coevaluation]
  rw [(Basis.singleton Unit K).constr_apply_fintype K]
  simp only [Fintype.univ_punit, Finset.sum_const, one_smul, Basis.singleton_repr,
    Basis.equivFun_apply, Basis.coe_ofVectorSpace, Finset.card_singleton]

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)
⊢ (LinearMap.lTensor V (contractLeft K V))
      (∑ x,
        (TensorProduct.assoc K V (Dual K V) V)
          ((Basis.ofVectorSpace K V) x ⊗ₜ[K] (Basis.ofVectorSpace K V).coord x ⊗ₜ[K] (Basis.ofVectorSpace K V) j)) =
    (Basis.ofVectorSpace K V) j ⊗ₜ[K] 1

Tactic:
simp only [assoc_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))
      (∑ x, (Basis.ofVectorSpace K V) x ⊗ₜ[K] ((Basis.ofVectorSpace K V).coord x ⊗ₜ[K] (Basis.ofVectorSpace K V) j)) =
    (Basis.ofVectorSpace K V) j ⊗ₜ[K] 1
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: case neg.inl
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
m : Type u_7
n : Type u_8
inst✝³ : Fintype m
inst✝² : Finite n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
bM : Basis m R M
bN : Basis n R N
j : m
i i' : n
j' : m
hij : ¬i = i'
⊢ (toMatrix bM bN) ((dualTensorHom R M N) (bM.coord j ⊗ₜ[R] bN i)) i' j' = Matrix.single i j 1 i' j'

Tactic:
simp [LinearMap.toMatrix_apply, Finsupp.single_eq_pi_single, hij]

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: case neg.inr
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
m : Type u_7
n : Type u_8
inst✝³ : Fintype m
inst✝² : Finite n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
bM : Basis m R M
bN : Basis n R N
j : m
i i' : n
j' : m
hij : ¬j = j'
⊢ (toMatrix bM bN) ((dualTensorHom R M N) (bM.coord j ⊗ₜ[R] bN i)) i' j' = Matrix.single i j 1 i' j'

Tactic:
simp [LinearMap.toMatrix_apply, Finsupp.single_eq_pi_single, hij]

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

Goal state before:
pp: R : Type u_1
M : Type u_5
Mₗ₁ : Type u_9
Mₗ₁' : Type u_10
Mₗ₂ : Type u_11
Mₗ₂' : Type u_12
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid Mₗ₁
inst✝⁶ : AddCommMonoid Mₗ₂
inst✝⁵ : AddCommMonoid Mₗ₁'
inst✝⁴ : AddCommMonoid Mₗ₂'
inst✝³ : Module R Mₗ₁
inst✝² : Module R Mₗ₂
inst✝¹ : Module R Mₗ₁'
inst✝ : Module R Mₗ₂'
B : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M
e₁ : Mₗ₁ ≃ₗ[R] Mₗ₁'
e₂ : Mₗ₂ ≃ₗ[R] Mₗ₂'
h : B.SeparatingLeft
x : Mₗ₁'
hx : ∀ (y : Mₗ₂'), (((e₁.arrowCongr (e₂.arrowCongr (LinearEquiv.refl R M))) B) x) y = 0
y : Mₗ₂
⊢ (B (e₁.symm x)) y = 0

Tactic:
specialize hx (e₂ y)

Goal state after:
R : Type u_1
M : Type u_5
Mₗ₁ : Type u_9
Mₗ₁' : Type u_10
Mₗ₂ : Type u_11
Mₗ₂' : Type u_12
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid Mₗ₁
inst✝⁶ : AddCommMonoid Mₗ₂
inst✝⁵ : AddCommMonoid Mₗ₁'
inst✝⁴ : AddCommMonoid Mₗ₂'
inst✝³ : Module R Mₗ₁
inst✝² : Module R Mₗ₂
inst✝¹ : Module R Mₗ₁'
inst✝ : Module R Mₗ₂'
B : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M
e₁ : Mₗ₁ ≃ₗ[R] Mₗ₁'
e₂ : Mₗ₂ ≃ₗ[R] Mₗ₂'
h : B.SeparatingLeft
x : Mₗ₁'
y : Mₗ₂
hx : (((e₁.arrowCongr (e₂.arrowCongr (LinearEquiv.refl R M))) B) x) (e₂ y) = 0
⊢ (B (e₁.symm x)) y = 0
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : B.IsOrthoᵢ ⇑v
h : ∀ (i : n), (B (v i)) (v i) ≠ 0
⊢ B.SeparatingLeft

Tactic:
by
  intro m hB
  obtain ⟨vi, rfl⟩ := v.repr.symm.surjective m
  rw [LinearEquiv.map_eq_zero_iff]
  ext i
  rw [Finsupp.zero_apply]
  specialize hB (v i)
  simp_rw [Basis.repr_symm_apply, Finsupp.linearCombination_apply, Finsupp.sum, map_sum₂,
           map_smulₛₗ₂] at hB
  rw [Finset.sum_eq_single i] at hB
  · cases smul_eq_zero.mp hB
    · assumption
    · specialize h i
      contradiction
  · intro j _hj hij
    replace hij : B (v j) (v i) = 0 := hO hij
    rw [hij, RingHom.id_apply, smul_zero]
  · intro hi
    replace hi : vi i = 0 := Finsupp.notMem_support_iff.mp hi
    rw [hi, RingHom.id_apply, zero_smul]

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
inst✝ : Projective R M
⊢ ⊤.dualCoannihilator = ⊥

Tactic:
by
  rw [dualCoannihilator, dualAnnihilator_top, comap_bot, Module.eval_ker]

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 : Subspace K V
φ : Dual K V
⊢ W.quotAnnihilatorEquiv (Submodule.Quotient.mk φ) = (dualRestrict W) φ

Tactic:
by
  ext
  rfl

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

Goal state before:
pp: K : Type u_1
V₁ : Type u_2
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
f : Dual K V₁
hf : f ≠ 0
inst✝ : FiniteDimensional K V₁
p : Submodule K V₁
hpf : Disjoint (LinearMap.ker f) p
hp : p ≠ ⊥
⊢ IsCompl (LinearMap.ker f) p

Tactic:
by
  refine ⟨hpf, codisjoint_iff.mpr <| eq_of_le_of_finrank_le le_top ?_⟩
  have : finrank K ↑(LinearMap.ker f ⊔ p) = finrank K (LinearMap.ker f) + finrank K p := by
    simp [← Submodule.finrank_sup_add_finrank_inf_eq (LinearMap.ker f) p, hpf.eq_bot]
  rwa [finrank_top, this, ← finrank_ker_add_one_of_ne_zero hf, add_le_add_iff_left,
    Submodule.one_le_finrank_iff]

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 : Subspace K V₁
⊢ Submodule.dualPairing W = ↑W.quotAnnihilatorEquiv

Tactic:
by
  ext
  rfl

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

Goal state before:
pp: C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁶ : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝⁵ : HasCokernel f
inst✝⁴ : HasCokernel (G.map f)
inst✝³ : PreservesColimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst✝² : HasCokernel g
inst✝¹ : HasCokernel (G.map g)
inst✝ : PreservesColimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ (PreservesCokernel.iso G f).hom ≫
      cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯ ≫ (PreservesCokernel.iso G g).inv =
    G.map (cokernel.map f g p q hpq)

Tactic:
← Iso.eq_inv_comp,

Goal state after:
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁶ : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝⁵ : HasCokernel f
inst✝⁴ : HasCokernel (G.map f)
inst✝³ : PreservesColimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst✝² : HasCokernel g
inst✝¹ : HasCokernel (G.map g)
inst✝ : PreservesColimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯ ≫ (PreservesCokernel.iso G g).inv =
    (PreservesCokernel.iso G f).inv ≫ G.map (cokernel.map f g p q hpq)
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)
⊢ (NormalEpi.g ≫ f) ≫ h = 0

Tactic:
by
    have reassoc' {W : C} (h' : R ⟶ W) : gn.g ≫ g ≫ h' = 0 ≫ h' := by
      rw [← Category.assoc, eq_whisker gn.w]
    rw [Category.assoc, comm, reassoc', zero_comp]

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

Goal state before:
pp: J : Type w
f : J → AddCommGrpCat
s : Cone (Discrete.functor f)
m :
  s.pt ⟶
    { pt := of ((j : J) → ↑(f j)), π := Discrete.natTrans fun j ↦ ofHom (Pi.evalAddMonoidHom (fun j ↦ ↑(f j)) j.as) }.pt
w :
  ∀ (j : Discrete J),
    m ≫
        { pt := of ((j : J) → ↑(f j)),
                π := Discrete.natTrans fun j ↦ ofHom (Pi.evalAddMonoidHom (fun j ↦ ↑(f j)) j.as) }.π.app
          j =
      s.π.app j
⊢ m = lift f s

Tactic:
ext x j
        exact CategoryTheory.congr_fun (w ⟨j⟩) x

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

Goal state before:
pp: case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Epi f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
aux :
  ∀ (s : CokernelCofork (kernel.ι f)),
    Cofork.π (CokernelCofork.ofπ f ⋯) ≫
        inv (imageMonoFactorisation f).m ≫
          inv (coimageImageComparison f) ≫ colimit.desc (parallelPair (kernel.ι f) 0) s =
      Cofork.π s
⊢ IsColimit (CokernelCofork.ofπ f ⋯)

Tactic:
refine isColimitAux _ (fun A => inv (imageMonoFactorisation f).m ≫
                  inv (Abelian.coimageImageComparison f) ≫ colimit.desc _ _) aux ?_

Goal state after:
case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Epi f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
aux :
  ∀ (s : CokernelCofork (kernel.ι f)),
    Cofork.π (CokernelCofork.ofπ f ⋯) ≫
        inv (imageMonoFactorisation f).m ≫
          inv (coimageImageComparison f) ≫ colimit.desc (parallelPair (kernel.ι f) 0) s =
      Cofork.π s
⊢ ∀ (s : CokernelCofork (kernel.ι f)) (m_1 : (CokernelCofork.ofπ f ⋯).pt ⟶ s.pt),
    Cofork.π (CokernelCofork.ofπ f ⋯) ≫ m_1 = Cofork.π s →
      m_1 =
        inv (imageMonoFactorisation f).m ≫ inv (coimageImageComparison f) ≫ colimit.desc (parallelPair (kernel.ι f) 0) s
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
⊢ (imageStrongEpiMonoFactorisation f).e ≫ equalizer.ι (cokernel.π f) 0 =
    (factorThruImage f ≫ kernel.lift (cokernel.π f) (Limits.image.ι f) ⋯) ≫ equalizer.ι (cokernel.π f) 0

Tactic:
imageStrongEpiMonoFactorisation_e,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ Abelian.factorThruImage f ≫ equalizer.ι (cokernel.π f) 0 =
    (factorThruImage f ≫ kernel.lift (cokernel.π f) (Limits.image.ι f) ⋯) ≫ equalizer.ι (cokernel.π 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
this✝¹ : IsColimit (CokernelCofork.ofπ (biprod.desc f (-g)) ⋯)
d : Z ⟶ R
hd : biprod.desc f (-g) ≫ d = biprod.desc 0 e
this✝ : f ≫ d = 0
this : d = 0
⊢ biprod.inr ≫ biprod.desc 0 e = biprod.inr ≫ biprod.desc f (-g) ≫ d

Tactic:
← hd

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)) ⋯)
d : Z ⟶ R
hd : biprod.desc f (-g) ≫ d = biprod.desc 0 e
this✝ : f ≫ d = 0
this : d = 0
⊢ biprod.inr ≫ biprod.desc f (-g) ≫ d = biprod.inr ≫ biprod.desc f (-g) ≫ d
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
this✝¹ : IsColimit (CokernelCofork.ofπ (biprod.desc f (-g)) ⋯)
d : Z ⟶ R
hd : biprod.desc f (-g) ≫ d = biprod.desc e 0
this✝ : (-g) ≫ d = 0
this : d = 0
⊢ biprod.inl ≫ biprod.desc e 0 = biprod.inl ≫ biprod.desc f (-g) ≫ d

Tactic:
← hd

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)) ⋯)
d : Z ⟶ R
hd : biprod.desc f (-g) ≫ d = biprod.desc e 0
this✝ : (-g) ≫ d = 0
this : d = 0
⊢ biprod.inl ≫ biprod.desc f (-g) ≫ d = biprod.inl ≫ biprod.desc f (-g) ≫ d
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
inst✝ : Mono f
R : C
e : R ⟶ Z
h : e ≫ pushout.inr f g = 0
u : R ⟶ Y ⊞ Z := biprod.lift 0 e
hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0
this✝¹ : IsLimit (KernelFork.ofι (biprod.lift f (-g)) ⋯)
d : R ⟶ X
hd : d ≫ biprod.lift f (-g) = biprod.lift 0 e
this✝ : d ≫ f = 0
this : d = 0
⊢ biprod.lift 0 e ≫ biprod.snd = (d ≫ biprod.lift f (-g)) ≫ biprod.snd

Tactic:
← hd

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
inst✝ : Mono f
R : C
e : R ⟶ Z
h : e ≫ pushout.inr f g = 0
u : R ⟶ Y ⊞ Z := biprod.lift 0 e
hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0
this✝¹ : IsLimit (KernelFork.ofι (biprod.lift f (-g)) ⋯)
d : R ⟶ X
hd : d ≫ biprod.lift f (-g) = biprod.lift 0 e
this✝ : d ≫ f = 0
this : d = 0
⊢ (d ≫ biprod.lift f (-g)) ≫ biprod.snd = (d ≫ biprod.lift f (-g)) ≫ biprod.snd
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
inst✝ : Mono g
R : C
e : R ⟶ Y
h : e ≫ pushout.inl f g = 0
u : R ⟶ Y ⊞ Z := biprod.lift e 0
hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0
this✝¹ : IsLimit (KernelFork.ofι (biprod.lift f (-g)) ⋯)
d : R ⟶ X
hd : d ≫ biprod.lift f (-g) = biprod.lift e 0
this✝ : d ≫ (-g) = 0
this : d = 0
⊢ biprod.lift e 0 ≫ biprod.fst = (d ≫ biprod.lift f (-g)) ≫ biprod.fst

Tactic:
← hd

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
inst✝ : Mono g
R : C
e : R ⟶ Y
h : e ≫ pushout.inl f g = 0
u : R ⟶ Y ⊞ Z := biprod.lift e 0
hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0
this✝¹ : IsLimit (KernelFork.ofι (biprod.lift f (-g)) ⋯)
d : R ⟶ X
hd : d ≫ biprod.lift f (-g) = biprod.lift e 0
this✝ : d ≫ (-g) = 0
this : d = 0
⊢ (d ≫ biprod.lift f (-g)) ≫ biprod.fst = (d ≫ biprod.lift f (-g)) ≫ biprod.fst
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
ψ₁ ψ₂ : LeftHomologyMapData φ h₁ h₂
hK : ψ₁.φK = ψ₂.φK
hH : ψ₁.φH = ψ₂.φH
⊢ ψ₁ = ψ₂

Tactic:
cases ψ₁

Goal state after:
case mk
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
ψ₂ : LeftHomologyMapData φ h₁ h₂
φK✝ : h₁.K ⟶ h₂.K
φH✝ : h₁.H ⟶ h₂.H
commi✝ : φK✝ ≫ h₂.i = h₁.i ≫ φ.τ₂
commf'✝ : h₁.f' ≫ φK✝ = φ.τ₁ ≫ h₂.f'
commπ✝ : h₁.π ≫ φH✝ = φK✝ ≫ h₂.π
hK : { φK := φK✝, φH := φH✝, commi := commi✝, commf' := commf'✝, commπ := commπ✝ }.φK = ψ₂.φK
hH : { φK := φK✝, φH := φH✝, commi := commi✝, commf' := commf'✝, commπ := commπ✝ }.φH = ψ₂.φH
⊢ { φK := φK✝, φH := φH✝, commi := commi✝, commf' := commf'✝, commπ := commπ✝ } = ψ₂
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₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
ψ₁ ψ₂ : RightHomologyMapData φ h₁ h₂
hQ : ψ₁.φQ = ψ₂.φQ
hH : ψ₁.φH = ψ₂.φH
⊢ ψ₁ = ψ₂

Tactic:
cases ψ₁

Goal state after:
case mk
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
ψ₂ : RightHomologyMapData φ h₁ h₂
φQ✝ : h₁.Q ⟶ h₂.Q
φH✝ : h₁.H ⟶ h₂.H
commp✝ : h₁.p ≫ φQ✝ = φ.τ₂ ≫ h₂.p
commg'✝ : φQ✝ ≫ h₂.g' = h₁.g' ≫ φ.τ₃
commι✝ : φH✝ ≫ h₂.ι = h₁.ι ≫ φQ✝
hQ : { φQ := φQ✝, φH := φH✝, commp := commp✝, commg' := commg'✝, commι := commι✝ }.φQ = ψ₂.φQ
hH : { φQ := φQ✝, φH := φH✝, commp := commp✝, commg' := commg'✝, commι := commι✝ }.φH = ψ₂.φH
⊢ { φQ := φQ✝, φH := φH✝, commp := commp✝, commg' := commg'✝, commι := commι✝ } = ψ₂
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₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ φ.τ₁ ≫ S₂.f ≫ h₂.p = 0

Tactic:
h₂.wp,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ φ.τ₁ ≫ 0 = 0
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
⊢ S.homologyπ ≫ S.homologyι = S.iCycles ≫ S.pOpcycles

Tactic:
dsimp only [homologyπ, homologyι]
  simpa only [assoc, S.leftRightHomologyComparison_fac] using S.π_leftRightHomologyComparison_ι

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₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : S₁.RightHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ S₂.RightHomologyData

Tactic:
by
  haveI : Epi (opMap φ).τ₁ := by dsimp; infer_instance
  haveI : IsIso (opMap φ).τ₂ := by dsimp; infer_instance
  haveI : Mono (opMap φ).τ₃ := by dsimp; infer_instance
  exact (LeftHomologyData.ofEpiOfIsIsoOfMono' (opMap φ) h.op).unop

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
A : C
hf : S.f = 0
inst✝ : S.HasHomology
⊢ S.cycles ≅ S.homology

Tactic:
have := S.isIso_homologyπ hf

Goal state after:
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
A : C
hf : S.f = 0
inst✝ : S.HasHomology
this : IsIso S.homologyπ
⊢ S.cycles ≅ S.homology
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
A : C
hf : S.f = 0
inst✝ : S.HasHomology
this : IsIso S.homologyπ
⊢ S.cycles ≅ S.homology

Tactic:
exact asIso S.homologyπ

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 : ShortComplex C
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst✝ : S.HasRightHomology
⊢ h.opcyclesIso.hom ≫ h.descQ k hk = S.descOpcycles k hk

Tactic:
← h.opcyclesIso_inv_comp_descOpcycles,

Goal state after:
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
hk : S.f ≫ k = 0
inst✝ : S.HasRightHomology
⊢ h.opcyclesIso.hom ≫ h.opcyclesIso.inv ≫ S.descOpcycles k hk = S.descOpcycles k hk
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 b : S₁ ⟶ S₂
⊢ (a + b).τ₁ = (b + a).τ₁

Tactic:
apply add_comm

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

Tactic:
apply add_comm

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 b : S₁ ⟶ S₂
⊢ (a + b).τ₃ = (b + a).τ₃

Tactic:
apply add_comm

Goal state after: