mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : IsStablyFiniteRing R
inst✝ : Nontrivial R
n m : ℕ
f : (Fin n → R) →ₗ[R] Fin m → R
hf : Surjective ⇑f
⊢ m ≤ n

Tactic:
by
    by_contra! lt
    let p : (Fin m → R) →ₗ[R] Fin n → R := funLeft R R (Fin.castLE lt.le)
    have hp : Surjective p := funLeft_surjective_of_injective _ _ _ (Fin.castLE_injective lt.le)
    have : Injective p := .of_comp_right
      (Module.End.injective_of_surjective_fin (f := p ∘ₗ f) (hp.comp hf)) hf
    have ⟨⟨i, lt⟩, eq⟩ := injective_comp_right_iff_surjective.mp this ⟨n, lt⟩
    exact lt.ne congr($eq)

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
inst✝ : FiniteDimensional K V
s t : Submodule K V
hdisjoint : Disjoint s t
⊢ finrank K ↥s + finrank K ↥t ≤ finrank K V

Tactic:
rw [← Submodule.finrank_sup_add_finrank_inf_eq s t, hdisjoint.eq_bot, finrank_bot, add_zero]

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
s t : Submodule K V
hdisjoint : Disjoint s t
⊢ finrank K ↥(s ⊔ t) ≤ finrank K V
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: R : Type u_1
M : Type u
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : HasRankNullity.{u, u_1} R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
⊢ finrank R (M ⧸ N) + finrank R ↥N = finrank R M

Tactic:
rw [← Nat.cast_inj (R := Cardinal), Module.finrank_eq_rank, Nat.cast_add, Module.finrank_eq_rank,
    Submodule.finrank_eq_rank]
  exact HasRankNullity.rank_quotient_add_rank _

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
inst✝ : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : W ⊔ K ∙ v = ⊤
this : W ⊓ K ∙ v = ⊥
hv₀ : v ≠ 0
aux : finrank K ↥⊤ + finrank K ↥(W ⊓ K ∙ v) = finrank K ↥W + 1
⊢ finrank K (V ⧸ W) = 1

Tactic:
this,

Goal state after:
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 = ⊥
hv₀ : v ≠ 0
aux : finrank K ↥⊤ + finrank K ↥⊥ = finrank K ↥W + 1
⊢ finrank K (V ⧸ W) = 1
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: case right
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.Surjective ⇑(dualTensorHom R M N ∘ₗ rTensor N g.dualMap)

Tactic:
dualTensorHom_comp_rTensor_dualMap,

Goal state after:
case right
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.Surjective ⇑(lcomp R N g ∘ₗ dualTensorHom R (Fin n → R) N)
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] P
g : P →ₗ[R] N
comp_eq_id : g ∘ₗ f = LinearMap.id
h : Function.Bijective ⇑(dualTensorHom R M P)
⊢ Function.Surjective (⇑(dualTensorHom R M N) ∘ ⇑(lTensor (Dual R M) g))

Tactic:
by
    rw [← coe_comp, dualTensorHom_comp_lTensor, coe_comp]
    refine (surjective_of_comp_eq_id (f.compRight R) _ ?_).comp h.2
    ext; exact congr($comp_eq_id _)

Goal state after:
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₁
I I' : R →+* R
B : M →ₛₗ[I] M →ₛₗ[I'] M₁
inst✝ : Nontrivial R
v : Basis n R M
h : B.IsOrthoᵢ ⇑v
hB : B.SeparatingLeft
i : n
ho : (B (v i)) (v i) = 0
vi : n →₀ R
j : n
this : (B (v i)) (v j) = 0
⊢ I' (vi j) • (B (v i)) (v j) = 0

Tactic:
this,

Goal state after:
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₁
I I' : R →+* R
B : M →ₛₗ[I] M →ₛₗ[I'] M₁
inst✝ : Nontrivial R
v : Basis n R M
h : B.IsOrthoᵢ ⇑v
hB : B.SeparatingLeft
i : n
ho : (B (v i)) (v i) = 0
vi : n →₀ R
j : n
this : (B (v i)) (v j) = 0
⊢ I' (vi j) • 0 = 0
Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers

Goal state before:
pp: case h₁
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPushouts C
F : WalkingParallelPair ⥤ C
c : Cocone F
m : (coequalizerCocone F).pt ⟶ c.pt
J : ∀ (j : WalkingParallelPair), (coequalizerCocone F).ι.app j ≫ m = c.ι.app j
J1 : pushoutInl F ≫ m = c.ι.app WalkingParallelPair.one
⊢ pushout.inr (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
        (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right)) ≫
      m =
    (PushoutCocone.mk (c.ι.app WalkingParallelPair.one) (c.ι.app WalkingParallelPair.one) ⋯).ι.app WalkingSpan.right

Tactic:
← pushoutInl_eq_pushout_inr

Goal state after:
case h₁
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPushouts C
F : WalkingParallelPair ⥤ C
c : Cocone F
m : (coequalizerCocone F).pt ⟶ c.pt
J : ∀ (j : WalkingParallelPair), (coequalizerCocone F).ι.app j ≫ m = c.ι.app j
J1 : pushoutInl F ≫ m = c.ι.app WalkingParallelPair.one
⊢ pushoutInl F ≫ m =
    (PushoutCocone.mk (c.ι.app WalkingParallelPair.one) (c.ι.app WalkingParallelPair.one) ⋯).ι.app WalkingSpan.right
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
⊢ dualDistribInvOfBasis b c ∘ₗ dualDistrib R M N = LinearMap.id

Tactic:
by
  apply (b.dualBasis.tensorProduct c.dualBasis).ext
  rintro ⟨i, j⟩
  simp only [Basis.tensorProduct_apply, Basis.coe_dualBasis, coe_comp, Function.comp_apply,
    dualDistribInvOfBasis_apply, dualDistrib_apply, Basis.coord_apply, Basis.repr_self,
    id_coe, id_eq]
  rw [Finset.sum_eq_single i, Finset.sum_eq_single j]
  · simp
  all_goals { intros; simp [*] at * }

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 ≠ ⊥
this : finrank K ↥(LinearMap.ker f ⊔ p) = finrank K ↥(LinearMap.ker f) + finrank K ↥p
⊢ finrank K V₁ ≤ finrank K ↥(LinearMap.ker f ⊔ p)

Tactic:
this,

Goal state after:
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 ≠ ⊥
this : finrank K ↥(LinearMap.ker f ⊔ p) = finrank K ↥(LinearMap.ker f) + finrank K ↥p
⊢ finrank K V₁ ≤ finrank K ↥(LinearMap.ker f) + finrank K ↥p
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) ⋯ =
    G.map (cokernel.map f g p q hpq) ≫ (PreservesCokernel.iso G g).hom

Tactic:
by
  rw [← Iso.comp_inv_eq, Category.assoc, ← Iso.eq_inv_comp, PreservesCokernel.iso_inv,
    cokernel_map_comp_cokernelComparison, PreservesCokernel.iso_inv]

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
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 ≫ f' = f ≫ Arrow.Hom.right e.hom
⊢ g ≫ Arrow.Hom.left e.hom ≫ f' = 0

Tactic:
this,

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 ≫ f' = f ≫ Arrow.Hom.right e.hom
⊢ g ≫ f ≫ Arrow.Hom.right e.hom = 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✝⁴ : HasFiniteProducts C
inst✝³ : HasKernels C
inst✝² : IsNormalMonoCategory C
X Y Z : C
a : X ⟶ Z
b : Y ⟶ Z
inst✝¹ : Mono a
inst✝ : Mono b
P : C
f : Z ⟶ P
haf : a ≫ f = 0
i : IsLimit (KernelFork.ofι a haf)
Q : C
g : Z ⟶ Q
hbg : b ≫ g = 0
i' : IsLimit (KernelFork.ofι b hbg)
a' : kernel (prod.lift f g) ⟶ (KernelFork.ofι a haf).pt
ha' : a' ≫ Fork.ι (KernelFork.ofι a haf) = kernel.ι (prod.lift f g)
b' : kernel (prod.lift f g) ⟶ (KernelFork.ofι b hbg).pt
hb' : b' ≫ Fork.ι (KernelFork.ofι b hbg) = kernel.ι (prod.lift f g)
s : PullbackCone a b
⊢ s.snd ≫ b ≫ g = s.snd ≫ 0

Tactic:
hbg

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroMorphisms C
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasKernels C
inst✝² : IsNormalMonoCategory C
X Y Z : C
a : X ⟶ Z
b : Y ⟶ Z
inst✝¹ : Mono a
inst✝ : Mono b
P : C
f : Z ⟶ P
haf : a ≫ f = 0
i : IsLimit (KernelFork.ofι a haf)
Q : C
g : Z ⟶ Q
hbg : b ≫ g = 0
i' : IsLimit (KernelFork.ofι b hbg)
a' : kernel (prod.lift f g) ⟶ (KernelFork.ofι a haf).pt
ha' : a' ≫ Fork.ι (KernelFork.ofι a haf) = kernel.ι (prod.lift f g)
b' : kernel (prod.lift f g) ⟶ (KernelFork.ofι b hbg).pt
hb' : b' ≫ Fork.ι (KernelFork.ofι b hbg) = kernel.ι (prod.lift f g)
s : PullbackCone a b
⊢ s.snd ≫ 0 = s.snd ≫ 0
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
f : X ⟶ Y
⊢ diag X ≫ prod.map f f ≫ σ = 0

Tactic:
prod.diag_map_assoc,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
f : X ⟶ Y
⊢ f ≫ diag Y ≫ σ = 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
⊢ e = biprod.inr ≫ biprod.desc 0 e

Tactic:
biprod.inr_desc

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
⊢ e = e
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
⊢ (-g) ≫ d = (biprod.inr ≫ biprod.desc f (-g)) ≫ d

Tactic:
biprod.inr_desc

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
⊢ (-g) ≫ d = (-g) ≫ d
Module: Mathlib.Algebra.Category.Grp.EpiMono

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

Tactic:
rw [← y.2.choose_spec, leftCoset_assoc]

Goal state after:
A B : GrpCat
f : A ⟶ B
b : ↑B
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ { toFun := fun x ↦ 1 • x, invFun := fun x ↦ 1⁻¹ • x, left_inv := ⋯, right_inv := ⋯ } x✝ = 1 x✝

Tactic:
simp [one_smul]

Goal state after:
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
⊢ e = biprod.lift 0 e ≫ biprod.snd

Tactic:
rw [biprod.lift_snd]

Goal state after:
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
⊢ d ≫ (-g) = d ≫ biprod.lift f (-g) ≫ biprod.snd

Tactic:
rw [biprod.lift_snd]

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

Goal state before:
pp: A B : GrpCat
f✝ : A ⟶ B
X✝ Y✝ : GrpCat
f : X✝ ⟶ Y✝
e : Function.Injective ⇑(ConcreteCategory.hom f)
⊢ Mono ((forget GrpCat).map f)

Tactic:
← CategoryTheory.ofHom_mono_iff_injective

Goal state after:
A B : GrpCat
f✝ : A ⟶ B
X✝ Y✝ : GrpCat
f : X✝ ⟶ Y✝
e : Mono (↾⇑(ConcreteCategory.hom f))
⊢ Mono ((forget GrpCat).map f)
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: A B : CommGrpCat
f✝ : A ⟶ B
X✝ Y✝ : CommGrpCat
f : X✝ ⟶ Y✝
e : Function.Injective ⇑(ConcreteCategory.hom f)
⊢ Mono ((forget CommGrpCat).map f)

Tactic:
← CategoryTheory.ofHom_mono_iff_injective

Goal state after:
A B : CommGrpCat
f✝ : A ⟶ B
X✝ Y✝ : CommGrpCat
f : X✝ ⟶ Y✝
e : Mono (↾⇑(ConcreteCategory.hom f))
⊢ Mono ((forget CommGrpCat).map f)
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₃ : ShortComplex C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
h₃ : S₃.LeftHomologyData
γ₁ : LeftHomologyMapData φ₁ h₁ h₂ := leftHomologyMapData φ₁ h₁ h₂
γ₂ : LeftHomologyMapData φ₂ h₂ h₃ := leftHomologyMapData φ₂ h₂ h₃
⊢ leftHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = γ₁.φH ≫ γ₂.φH

Tactic:
(γ₁.comp γ₂).leftHomologyMap'_eq,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
h₃ : S₃.LeftHomologyData
γ₁ : LeftHomologyMapData φ₁ h₁ h₂ := leftHomologyMapData φ₁ h₁ h₂
γ₂ : LeftHomologyMapData φ₂ h₂ h₃ := leftHomologyMapData φ₂ h₂ h₃
⊢ (γ₁.comp γ₂).φH = γ₁.φH ≫ γ₂.φH
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
⊢ h₁.π ≫ leftRightHomologyComparison' h₁ h₂ ≫ h₂.ι = h₁.i ≫ h₂.p

Tactic:
by
  simp only [leftRightHomologyComparison'_eq_liftH,
    RightHomologyData.liftH_ι, LeftHomologyData.π_descH]

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 : ShortComplex C
h₁ h₁' : S.LeftHomologyData
h₂ h₂' : S.RightHomologyData
⊢ leftRightHomologyComparison' h₁ h₂ =
    leftHomologyMap' (𝟙 S) h₁ h₁' ≫ leftRightHomologyComparison' h₁' h₂' ≫ rightHomologyMap' (𝟙 S) h₂' h₂

Tactic:
rw [leftRightHomologyComparison'_naturality_assoc (𝟙 S) h₁ h₂ h₁' h₂',
    ← rightHomologyMap'_comp, comp_id, rightHomologyMap'_id, comp_id]

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 : ShortComplex C
h : S.HomologyData
inst✝ : S.HasHomology
this : h.iso = h.left.homologyIso.symm ≪≫ h.right.homologyIso
⊢ h.right.homologyIso = h.left.homologyIso ≪≫ h.iso

Tactic:
this,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
inst✝ : S.HasHomology
this : h.iso = h.left.homologyIso.symm ≪≫ h.right.homologyIso
⊢ h.right.homologyIso = h.left.homologyIso ≪≫ h.left.homologyIso.symm ≪≫ h.right.homologyIso
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₁ S₂ : ShortComplex C
h : S.LeftHomologyData
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : h.IsPreservedBy F
this✝ : PreservesLimit (parallelPair S.g 0) F
this : PreservesColimit (parallelPair h.f' 0) F
wi : F.map h.i ≫ F.map S.g = 0
hi : IsLimit ((KernelFork.ofι h.i ⋯).map F)
f' : F.obj S.X₁ ⟶ F.obj h.K := hi.lift (KernelFork.ofι (S.map F).f ⋯)
⊢ Fork.ι (KernelFork.ofι (S.map F).f ⋯) = F.map h.f' ≫ Fork.ι ((KernelFork.ofι h.i ⋯).map F)

Tactic:
simp only [KernelFork.map_ι, Fork.ι_ofι, map_f, ← F.map_comp, f'_i]

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
⊢ (rightHomologyMap' φ h₁ h₂).op = leftHomologyMap' (opMap φ) h₂.op h₁.op

Tactic:
let γ : RightHomologyMapData φ h₁ h₂ := rightHomologyMapData φ h₁ h₂
  simp only [γ.rightHomologyMap'_eq, γ.op.leftHomologyMap'_eq,
    RightHomologyMapData.op_φH]

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
⊢ (rightHomologyMap φ).op = S₂.leftHomologyOpIso.inv ≫ leftHomologyMap (opMap φ) ≫ S₁.leftHomologyOpIso.hom

Tactic:
by
  dsimp [leftHomologyOpIso, LeftHomologyData.leftHomologyIso, leftHomologyMap,
    rightHomologyMap]
  simp only [← leftHomologyMap'_comp, comp_id, id_comp, rightHomologyMap'_op]

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₁ S₂ : ShortComplex C
h : S.RightHomologyData
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : h.IsPreservedBy F
this✝ : PreservesColimit (parallelPair S.f 0) F
this : PreservesLimit (parallelPair h.g' 0) F
wp : F.map S.f ≫ F.map h.p = 0
hp : IsColimit ((CokernelCofork.ofπ h.p ⋯).map F)
g' : F.obj h.Q ⟶ F.obj S.X₃ := hp.desc (CokernelCofork.ofπ (S.map F).g ⋯)
⊢ Cofork.π (CokernelCofork.ofπ (S.map F).g ⋯) = Cofork.π ((CokernelCofork.ofπ h.p ⋯).map F) ≫ F.map h.g'

Tactic:
simp only [Cofork.π_ofπ, CokernelCofork.map_π, map_g, ← F.map_comp, p_g']

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₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ opcyclesMap' (-φ) h₁ h₂ = -opcyclesMap' φ h₁ h₂

Tactic:
have γ : RightHomologyMapData φ h₁ h₂ := default
  simp only [γ.opcyclesMap'_eq, γ.neg.opcyclesMap'_eq, RightHomologyMapData.neg_φQ]

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
g' : cokernel S.f ⟶ S.X₃ := cokernel.desc S.f S.g ⋯
hg' : g' = cokernel.π γ ≫ cokernel.desc γ g' ⋯
⊢ S.RightHomologyData

Tactic:
have wι : kernel.ι (cokernel.π γ) ≫ g' = 0 := by rw [hg', kernel.condition_assoc, zero_comp]

Goal state after:
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
g' : cokernel S.f ⟶ S.X₃ := cokernel.desc S.f S.g ⋯
hg' : g' = cokernel.π γ ≫ cokernel.desc γ g' ⋯
wι : kernel.ι (cokernel.π γ) ≫ g' = 0
⊢ S.RightHomologyData
Module: Mathlib.Algebra.Homology.ShortComplex.Limits

Goal state before:
pp: case h₂
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
j : J
⊢ (c.ι.app j ≫
        { τ₁ := h₁.desc (π₁.mapCocone s), τ₂ := h₂.desc (π₂.mapCocone s), τ₃ := h₃.desc (π₃.mapCocone s), comm₁₂ := ⋯,
          comm₂₃ := ⋯ }).τ₂ =
    (s.ι.app j).τ₂

pp: case h₃
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
j : J
⊢ (c.ι.app j ≫
        { τ₁ := h₁.desc (π₁.mapCocone s), τ₂ := h₂.desc (π₂.mapCocone s), τ₃ := h₃.desc (π₃.mapCocone s), comm₁₂ := ⋯,
          comm₂₃ := ⋯ }).τ₃ =
    (s.ι.app j).τ₃

Tactic:
· apply IsColimit.fac h₂

Goal state after:
case h₃
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
j : J
⊢ (c.ι.app j ≫
        { τ₁ := h₁.desc (π₁.mapCocone s), τ₂ := h₂.desc (π₂.mapCocone s), τ₃ := h₃.desc (π₃.mapCocone s), comm₁₂ := ⋯,
          comm₂₃ := ⋯ }).τ₃ =
    (s.ι.app j).τ₃