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

Goal state before:
pp: R : Type u_1
A : Type u_2
C : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : Semiring C
inst✝¹ : Bialgebra R C
inst✝ : Algebra R A
f g : WithConv (C →ₐ[R] A)
c : C
⊢ (lmul' R).comp (Algebra.TensorProduct.map f.ofConv g.ofConv) = Algebra.TensorProduct.lift f.ofConv g.ofConv ⋯

Tactic:
ext <;> simp

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

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

Tactic:
rw [← cancel_mono (Monoidal.μIso _ _ _).inv]

Goal state after:
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✝² : BraidedCategory C
inst✝¹ : BraidedCategory D
F : C ⥤ D
inst✝ : PreservesFiniteProducts F
X Y : C
⊢ (μ F X Y ≫ F.map (β_ X Y).hom) ≫ (Monoidal.μIso F Y X).inv =
    ((β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X) ≫ (Monoidal.μIso F Y X).inv
Module: Mathlib.RingTheory.HopfAlgebra.Convolution

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

Tactic:
by simp [LinearMap.convMul_def]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
C : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring C
inst✝¹ : Bialgebra R C
inst✝ : HopfAlgebra R A
f : WithConv (A →ₐ[R] C)
⊢ (lmul' R).comp (Algebra.TensorProduct.map f.ofConv f.ofConv) = f.ofConv.comp (lmul' R)

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.DivisionRing

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : DivisionSemiring R
inst✝ : Module R M
f : M →ₗ[R] R
⊢ Function.Surjective ⇑f ↔ f ≠ 0

Tactic:
by
  refine ⟨ne_zero_of_surjective, fun hf z ↦ ?_⟩
  obtain ⟨y, hy⟩ : ∃ y, f y ≠ 0 := by simpa [Ne, LinearMap.ext_iff] using hf
  exact ⟨(z * (f y)⁻¹) • y, by simp [hy]⟩

Goal state after:
Module: Mathlib.Logic.Equiv.Finset

Goal state before:
pp: head✝¹ head✝ : ℕ
tail✝ : List ℕ
x✝ : ℕ
⊢ head✝¹ + x✝ < head✝ + (head✝¹ + x✝ + 1)

Tactic:
lia

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

Goal state before:
pp: R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ (∑ x ∈ f.support, b.toDual (f x • b x)) (b i) = f i

Tactic:
LinearMap.sum_apply

Goal state after:
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ ∑ d ∈ f.support, (b.toDual (f d • b d)) (b i) = f i
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: case intro
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
f : ι →₀ R
i : ι
val✝ : Fintype ι
⊢ (∑ i, f i • b.dualBasis i) (b i) = f i

pp: case intro.h
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
f : ι →₀ R
i : ι
val✝ : Fintype ι
⊢ ∀ (i : ι), 0 • b.dualBasis i = 0

Tactic:
LinearMap.sum_apply

Goal state after:
case intro
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
f : ι →₀ R
i : ι
val✝ : Fintype ι
⊢ ∑ d, (f d • b.dualBasis d) (b i) = f i

case intro.h
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
f : ι →₀ R
i : ι
val✝ : Fintype ι
⊢ ∀ (i : ι), 0 • b.dualBasis i = 0
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: case intro
R : Type uR
M : Type uM
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_1
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
⊢ (b.dualBasis.toDual ∘ₗ b.toDual).range = ⊤

Tactic:
range_comp,

Goal state after:
case intro
R : Type uR
M : Type uM
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_1
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
⊢ map b.dualBasis.toDual b.toDual.range = ⊤
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
i : ι
f : M
⊢ (b.dualBasis.coord i) (b.toDualEquiv f) = (b.coord i) f

Tactic:
simp [-toDualEquiv_apply, Basis.dualBasis]

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

Goal state before:
pp: R : Type u_1
M : Type u
M' : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M'
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : HasRankNullity.{v, u_1} R
f : M →ₗ[R] M'
p : Submodule R M
f' : M' ⧸ Submodule.map f p →ₗ[R] M' ⧸ f.range := factor ⋯
g : ↥f.range →ₗ[R] ↥f'.ker :=
  ↑(LinearEquiv.ofEq (Submodule.map (Submodule.map f p).mkQ f.range) f'.ker ⋯) ∘ₗ
    (Submodule.map f p).mkQ.submoduleMap f.range
g_surj : Surjective ⇑g
⊢ g.ker = Submodule.map f.rangeRestrict p

Tactic:
simp [g, submoduleMap, ker_restrict, map_codRestrict]

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

Goal state before:
pp: K : Type u
inst✝² : DivisionRing K
V : Type v
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
ι : Type v
b : Module.Basis ι K V
⊢ 1 < #K

Tactic:
one_lt_iff_nontrivial

Goal state after:
K : Type u
inst✝² : DivisionRing K
V : Type v
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
ι : Type v
b : Module.Basis ι K V
⊢ Nontrivial K
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: case refine_1
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
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (M ⧸ span R s)
ht : #↑t = Module.rank R (M ⧸ span R s)
ht' : LinearIndependent (ι := ↑t) R Subtype.val
sec : M ⧸ span R s → M
hsec : ∀ (b : M ⧸ span R s), (span R s).mkQ (sec b) = b
hsec' : ⇑(span R s).mkQ ∘ sec = _root_.id
hst : Disjoint s (sec '' t)
⊢ #↑(s ∪ sec '' t) = Module.rank R M

Tactic:
rw [Cardinal.mk_union_of_disjoint hst, Cardinal.mk_image_eq, ht,
      ← rank_quotient_add_rank (Submodule.span R s), add_comm, rank_span_set hs]
    exact HasLeftInverse.injective ⟨Submodule.Quotient.mk, hsec⟩

Goal state after:
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]

Goal state after:
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 ⧸ restrictScalars R N) + finrank R ↥(restrictScalars R N) - finrank R ↥N
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✝⁴ : IsDomain R
inst✝³ : IsTorsionFree R M
N : Type u_1
inst✝² : AddCommGroup N
inst✝¹ : Module R N
L : Submodule R M
inst✝ : Module.Finite R ↥L
f : M →ₗ[R] N
h : finrank R ↥L ≤ finrank R ↥(f.domRestrict L).range
this : finrank R ↥(f.domRestrict L).range + finrank R ↥(f.domRestrict L).ker = finrank R ↥L
⊢ finrank R ↥(f.domRestrict L).ker = 0

Tactic:
lia

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 (V ⧸ W) + finrank K ↥W + 0 = finrank K ↥W + 1
⊢ finrank K (V ⧸ W) = 1

Tactic:
lia

Goal state after:
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
h : finrank R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank R (M ⧸ N)
hs' : LinearIndependent R Subtype.val
v : M
hv : N.mkQ v ∈ s
r : R
hr : r ≠ 0
this :
  (Finsupp.linearCombination R Subtype.val) (Finsupp.single ⟨N.mkQ v, hv⟩ r) = 0 → Finsupp.single ⟨N.mkQ v, hv⟩ r = 0
⊢ r • v ∈ N → r = 0

Tactic:
rwa [Finsupp.linearCombination_single, Finsupp.single_eq_zero, ← map_smul,
    Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero] at this

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
inst✝ : FiniteDimensional K V₂
f : V →ₗ[K] V₂
h : finrank K V₂ < finrank K V
h₁ : finrank K ↥f.range + finrank K ↥f.ker = finrank K V
h₂ : finrank K ↥f.range ≤ finrank K V₂
⊢ 0 < finrank K ↥f.ker

Tactic:
lia

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

Goal state before:
pp: case mpr
K : Type u_13
K₁ : Type u_14
K₂ : Type u_15
V : Type u_16
V₁ : Type u_17
V₂ : Type u_18
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : Field K₁
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K₁ V₁
inst✝² : Field K₂
inst✝¹ : AddCommGroup V₂
inst✝ : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] V
x : V₁
y : V₂
a : K₁
ha : a ≠ 0
H : (B (a • x)) y = 0
⊢ (B x) y = 0

Tactic:
rw [map_smulₛₗ₂, smul_eq_zero] at H
    rcases H with H | H
    · rw [map_eq_zero I₁] at H
      trivial
    · exact H

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✝³ : HasCoequalizer f g
inst✝² : HasCoequalizer (G.map f) (G.map g)
inst✝¹ : PreservesColimit (parallelPair f g) G
X' Y' : D
f' g' : X' ⟶ Y'
inst✝ : HasCoequalizer f' g'
p : G.obj X ⟶ X'
q : G.obj Y ⟶ Y'
wf : G.map f ≫ q = p ≫ f'
wg : G.map g ≫ q = p ≫ g'
⊢ coequalizer.π (G.map f) (G.map g) ≫ colimMap (parallelPairHom (G.map f) (G.map g) f' g' p q wf wg) =
    q ≫ coequalizer.π f' g'

Tactic:
ι_colimMap,

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✝³ : HasCoequalizer f g
inst✝² : HasCoequalizer (G.map f) (G.map g)
inst✝¹ : PreservesColimit (parallelPair f g) G
X' Y' : D
f' g' : X' ⟶ Y'
inst✝ : HasCoequalizer f' g'
p : G.obj X ⟶ X'
q : G.obj Y ⟶ Y'
wf : G.map f ≫ q = p ≫ f'
wg : G.map g ≫ q = p ≫ g'
⊢ (parallelPairHom (G.map f) (G.map g) f' g' p q wf wg).app WalkingParallelPair.one ≫
      colimit.ι (parallelPair f' g') WalkingParallelPair.one =
    q ≫ coequalizer.π f' g'
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
W : Submodule R M
φ ψ : ↥W.dualAnnihilator
h : (fun φ ↦ ⇑↑φ) φ = (fun φ ↦ ⇑↑φ) ψ
⊢ φ = ψ

Tactic:
by
    ext
    simp only [funext_iff] at h
    exact h _

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

Goal state before:
pp: C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasLimit (pair X Y)
inst✝ : HasLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : X ⨯ Y ⟶ X := prod.fst
π₂ : X ⨯ Y ⟶ Y := prod.snd
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ X ⨯ Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)
⊢ (e ≫ π₁) ≫ f = (e ≫ π₂) ≫ g

Tactic:
rw [Category.assoc, equalizer.condition]
          simp [e]

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

Goal state before:
pp: K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst✝⁴ : Field K
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V₁ →ₗ[K] V₂
⊢ finrank K ↥(f.rangeRestrict.dualMap ∘ₗ f.range.subtype.dualMap).range = finrank K ↥f.range

Tactic:
range_comp,

Goal state after:
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst✝⁴ : Field K
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V₁ →ₗ[K] V₂
⊢ finrank K ↥(map f.rangeRestrict.dualMap f.range.subtype.dualMap.range) = finrank K ↥f.range
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 : C
f g : X ⟶ Y
⊢ (coprod.inl ≫ coprod.desc (𝟙 Y) g) ≫ pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g) =
    pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)

Tactic:
coprod.inl_desc,

Goal state after:
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 : C
f g : X ⟶ Y
⊢ 𝟙 Y ≫ pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g) =
    pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: case refine_1
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 : Mono f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
s : KernelFork (cokernel.π f)
⊢ (limit.lift (parallelPair (cokernel.π f) 0) s ≫ inv (imageMonoFactorisation f).e) ≫ Fork.ι (KernelFork.ofι f ⋯) =
    Fork.ι s

Tactic:
· simp only [KernelFork.ι_ofι, Category.assoc]
          convert! limit.lift_π s WalkingParallelPair.zero using 2
          rw [IsIso.inv_comp_eq, eq_comm]
          exact (imageMonoFactorisation f).fac

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
inst✝² : S₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ' : QuasiIso φ'
hφφ' : QuasiIso (φ ≫ φ')
⊢ QuasiIso φ

Tactic:
by
  rw [quasiIso_iff] at hφ' hφφ' ⊢
  rw [homologyMap_comp] at hφφ'
  exact IsIso.of_isIso_comp_right (homologyMap φ) (homologyMap φ')

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
h₂' : S₂.LeftHomologyData := LeftHomologyData.ofEpiOfIsIsoOfMono φ h₁
⊢ IsIso (leftHomologyMap' φ h₁ h₂')

Tactic:
(LeftHomologyMapData.ofEpiOfIsIsoOfMono φ h₁).leftHomologyMap'_eq

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₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
h₂' : S₂.LeftHomologyData := LeftHomologyData.ofEpiOfIsIsoOfMono φ h₁
⊢ IsIso (LeftHomologyMapData.ofEpiOfIsIsoOfMono φ h₁).φH
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 : ShortComplex C
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
F : C ⥤ D
inst✝⁷ : F.PreservesZeroMorphisms
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hl₁ : S₁.LeftHomologyData
hr₁ : S₁.RightHomologyData
hl₂ : S₂.LeftHomologyData
hr₂ : S₂.RightHomologyData
ψl : LeftHomologyMapData φ hl₁ hl₂
ψr : RightHomologyMapData φ hr₁ hr₂
inst✝⁶ : S₁.HasHomology
inst✝⁵ : S₂.HasHomology
inst✝⁴ : (F.mapShortComplex.obj S₁).HasHomology
inst✝³ : (F.mapShortComplex.obj S₂).HasHomology
inst✝² : F.PreservesRightHomologyOf S₁
inst✝¹ : F.PreservesRightHomologyOf S₂
inst✝ : QuasiIso φ
⊢ QuasiIso (F.mapShortComplex.map φ)

Tactic:
have γ : RightHomologyMapData φ S₁.rightHomologyData S₂.rightHomologyData := default
  have : IsIso γ.φH := by
    rw [← γ.quasiIso_iff]
    infer_instance
  rw [(γ.map F).quasiIso_iff, RightHomologyMapData.map_φH]
  infer_instance

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 : Homotopy φ₁ φ₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ leftHomologyMap' φ₁ h₁ h₂ = leftHomologyMap' φ₂ h₁ h₂

Tactic:
h.eq_add_nullHomotopic,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ leftHomologyMap' (φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯) h₁ h₂ = leftHomologyMap' φ₂ h₁ h₂
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 : Homotopy φ₁ φ₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ rightHomologyMap' φ₁ h₁ h₂ = rightHomologyMap' φ₂ h₁ h₂

Tactic:
h.eq_add_nullHomotopic,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ rightHomologyMap' (φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯) h₁ h₂ = rightHomologyMap' φ₂ h₁ h₂
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 : Homotopy φ₁ φ₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
⊢ homologyMap' φ₁ h₁ h₂ = homologyMap' φ₂ h₁ h₂

Tactic:
h.eq_add_nullHomotopic,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
⊢ homologyMap' (φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯) h₁ h₂ = homologyMap' φ₂ h₁ h₂
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
i : D ⥤ C
inst✝ : Reflective i
A B B' : C
h : B ⟶ B'
hB : i.essImage B
hB' : i.essImage B'
f : A ⟶ B
⊢ f ≫ h = (unitCompPartialBijective A hB).symm ((unitCompPartialBijective A hB) f) ≫ h

Tactic:
Equiv.symm_apply_apply

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
i : D ⥤ C
inst✝ : Reflective i
A B B' : C
h : B ⟶ B'
hB : i.essImage B
hB' : i.essImage B'
f : A ⟶ B
⊢ f ≫ h = f ≫ h
Module: Mathlib.CategoryTheory.Subobject.FactorThru

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Subobject X
h : P.Factors P.arrow
⊢ P.factorThru P.arrow h = 𝟙 (underlying.obj P)

Tactic:
ext
  simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ (mk f).factorThru f ⋯ = (underlyingIso f).inv

Tactic:
ext
  simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
P : Subobject Y
f : X ⟶ underlying.obj P
h : P.Factors (f ≫ P.arrow)
⊢ P.factorThru (f ≫ P.arrow) h = f

Tactic:
ext
  simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y Z : C
P Q : Subobject Y
f : Z ⟶ Y
h : P ≤ Q
w : P.Factors f
⊢ Q.factorThru f ⋯ = P.factorThru f w ≫ P.ofLE Q h

Tactic:
ext
  simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
X Y : C
P : Subobject Y
f g : X ⟶ Y
w : P.Factors (f + g)
wf : P.Factors f
wg : P.Factors g
⊢ P.factorThru (f + g) w = P.factorThru f wf + P.factorThru g wg

Tactic:
ext
  simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
X Y : C
P : Subobject Y
f g : X ⟶ Y
w : P.Factors (f + g)
wg : P.Factors g
⊢ P.factorThru (f + g) w - P.factorThru g wg = P.factorThru f ⋯

Tactic:
ext
  simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
X Y : C
P : Subobject Y
f g : X ⟶ Y
w : P.Factors (f + g)
wf : P.Factors f
⊢ P.factorThru (f + g) w - P.factorThru f wf = P.factorThru g ⋯

Tactic:
ext
  simp

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
B A₁ A₂ : C
f : A₁ ⟶ B
g : A₂ ⟶ B
inst✝¹ : Mono f
inst✝ : Mono g
h : mk f ≤ mk g
⊢ Mono (ofMkLEMk f g h)

Tactic:
by
  dsimp only [ofMkLEMk]
  infer_instance

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

Goal state before:
pp: case star
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type u₃
inst✝ : Category.{v₃, u₃} J
X : C
F : Over X
x✝ : (Over.isMono X).limitsOfShape J F
p : LimitPresentation J F
hp : ∀ (j : J), Over.isMono X (p.diag.obj j)
Z✝ : C
g h : Z✝ ⟶ F.left
e : g ≫ F.hom = h ≫ F.hom
⊢ g ≫ (WithTerminal.coneEquiv.functor.obj { pt := F, π := p.π }).π.app WithTerminal.star =
    h ≫ (WithTerminal.coneEquiv.functor.obj { pt := F, π := p.π }).π.app WithTerminal.star

Tactic:
exact e

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : HasKernel f
⊢ (kernelSubobjectIso f).hom ≫ kernel.ι f = (kernelSubobject f).arrow

Tactic:
simp [kernelSubobjectIso]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : HasKernel f
⊢ (kernelSubobjectIso f).inv ≫ (kernelSubobject f).arrow = kernel.ι f

Tactic:
simp [kernelSubobjectIso]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : HasKernel f
W : C
h : W ⟶ X
w : (kernelSubobject f).Factors h
⊢ (kernelSubobject f).factorThru h w ≫ (kernelSubobject f).arrow ≫ f = 0

Tactic:
kernelSubobject_arrow_comp,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : HasKernel f
W : C
h : W ⟶ X
w : (kernelSubobject f).Factors h
⊢ (kernelSubobject f).factorThru h w ≫ 0 = 0