mathlib-initiative/mathlib-tactics huggingface dataset:
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
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : CartesianMonoidalCategory D
F : C ⥤ D
E : Type u₂
inst✝¹ : Category.{v₂, u₂} E
inst✝ : CartesianMonoidalCategory E
G : D ⥤ E
A B A' B' x y : C
f : x ⟶ y
⊢ (curriedTensor C ⋙ (Functor.whiskeringRight C C D).obj F).map f ≫ prodComparisonNatTrans F y =
    prodComparisonNatTrans F x ≫ (F ⋙ curriedTensor D ⋙ (Functor.whiskeringLeft C D D).obj F).map f

Tactic:
ext z

Goal state after:
C✝ : Type u
inst✝⁶ : Category.{v, u} C✝
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : CartesianMonoidalCategory C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : CartesianMonoidalCategory D
F : C ⥤ D
E : Type u₂
inst✝¹ : Category.{v₂, u₂} E
inst✝ : CartesianMonoidalCategory E
G : D ⥤ E
A B A' B' x y : C
f : x ⟶ y
z : C
⊢ ((curriedTensor C ⋙ (Functor.whiskeringRight C C D).obj F).map f ≫ prodComparisonNatTrans F y).app z =
    (prodComparisonNatTrans F x ≫ (F ⋙ curriedTensor D ⋙ (Functor.whiskeringLeft C D D).obj F).map f).app z
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
F : C ⥤ D
A B : C
inst✝ : IsIso (prodComparison F A B)
⊢ PreservesLimit (pair A B) F

Tactic:
apply preservesLimit_of_preserves_limit_cone (tensorProductIsBinaryProduct A B)
  refine IsLimit.equivOfNatIsoOfIso (pairComp A B F) _
    ((BinaryFan.mk (fst (F.obj A) (F.obj B)) (snd _ _)).extend (prodComparison F A B))
      (BinaryFan.ext (by exact Iso.refl _) ?_ ?_) |>.invFun
      (IsLimit.extendIso _ (tensorProductIsBinaryProduct (F.obj A) (F.obj B)))
  · dsimp only [BinaryFan.fst]
    simp [pairComp]
  · dsimp only [BinaryFan.snd]
    simp [pairComp]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
ι : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalSemiring A
inst✝⁵ : Module R A
inst✝⁴ : SMulCommClass R A A
inst✝³ : IsScalarTower R A A
inst✝² : AddCommMonoid C
inst✝¹ : Module R C
inst✝ : Coalgebra R C
f g h : WithConv (C →ₗ[R] A)
⊢ mul' R A ∘ₗ ((f * g).ofConv ⊗ₘ h.ofConv) ∘ₗ δ =
    (mul' R A ∘ₗ rTensor A (mul' R A)) ∘ₗ
      (((f.ofConv ⊗ₘ g.ofConv) ⊗ₘ h.ofConv) ∘ₗ ↑(TensorProduct.assoc R C C C).symm) ∘ₗ lTensor C δ ∘ₗ δ

Tactic:
by
      ext; simp [comp_assoc, coassoc_symm, convMul_def]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
s : PullbackCone μ μ
⊢ lift (s.snd ≫ fst A A ≫ ι) (s.fst ≫ fst A A) ≫ μ = lift (s.snd ≫ snd A A) (s.fst ≫ snd A A ≫ ι) ≫ μ

Tactic:
rw [← assoc s.fst, eq_lift_inv_right, lift_lift_assoc, ← assoc s.snd, lift_inv_left_eq,
          lift_comp_fst_snd, lift_comp_fst_snd, s.condition]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : Y ⟶ Z
⊢ (ρ_ (X ⊗ (ihom X).obj Y)).inv ≫
      (α_ X ((ihom X).obj Y) (𝟙_ C)).hom ≫
        (α_ X ((ihom X).obj Y) (𝟙_ C)).inv ≫
          (ρ_ (X ⊗ (ihom X).obj Y)).hom ≫ (ihom.ev X).app Y ≫ (ρ_ Y).inv ≫ (ρ_ Y).hom ≫ f =
    (ihom.ev X).app Y ≫ f

Tactic:
Iso.inv_hom_id_assoc,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : Y ⟶ Z
⊢ (ρ_ (X ⊗ (ihom X).obj Y)).inv ≫
      (α_ X ((ihom X).obj Y) (𝟙_ C)).hom ≫
        (α_ X ((ihom X).obj Y) (𝟙_ C)).inv ≫ (ρ_ (X ⊗ (ihom X).obj Y)).hom ≫ (ihom.ev X).app Y ≫ f =
    (ihom.ev X).app Y ≫ f
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : X ⟶ Y
g : Y ⟶ Z
⊢ curry' (f ≫ g) =
    (λ_ (𝟙_ C)).inv ≫
      (ρ_ (𝟙_ C)).hom ≫ curry' f ≫ (ρ_ ((ihom X).obj Y)).inv ≫ (ρ_ ((ihom X).obj Y)).hom ≫ (ihom X).map g

Tactic:
Iso.inv_hom_id_assoc,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : X ⟶ Y
g : Y ⟶ Z
⊢ curry' (f ≫ g) = (λ_ (𝟙_ C)).inv ≫ (ρ_ (𝟙_ C)).hom ≫ curry' f ≫ (ihom X).map g
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : X ⟶ Y
g : Y ⟶ Z
⊢ curry' (f ≫ g) = (λ_ (𝟙_ C)).inv ≫ (λ_ (𝟙_ C)).hom ≫ curry' f ≫ (ihom X).map g

Tactic:
Iso.inv_hom_id_assoc,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : X ⟶ Y
g : Y ⟶ Z
⊢ curry' (f ≫ g) = curry' f ≫ (ihom X).map g
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed

Goal state before:
pp: R : Type u
inst✝ : CommRing R
M X'✝ X✝ Y✝ : ModuleCat R
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ ((linearCoyoneda R (ModuleCat R)).obj (op M)).obj Y✝
⊢ ∀ (x : ↑M) (y : ↑X'✝),
    (Hom.hom ((M.monoidalClosedHomEquiv X'✝ Y✝).symm (f✝ ≫ g✝))) (x ⊗ₜ[R] y) =
      (Hom.hom ((MonoidalCategory.tensorLeft M).map f✝ ≫ (M.monoidalClosedHomEquiv X✝ Y✝).symm g✝)) (x ⊗ₜ[R] y)

Tactic:
intro m n

Goal state after:
R : Type u
inst✝ : CommRing R
M X'✝ X✝ Y✝ : ModuleCat R
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ ((linearCoyoneda R (ModuleCat R)).obj (op M)).obj Y✝
m : ↑M
n : ↑X'✝
⊢ (Hom.hom ((M.monoidalClosedHomEquiv X'✝ Y✝).symm (f✝ ≫ g✝))) (m ⊗ₜ[R] n) =
    (Hom.hom ((MonoidalCategory.tensorLeft M).map f✝ ≫ (M.monoidalClosedHomEquiv X✝ Y✝).symm g✝)) (m ⊗ₜ[R] n)
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: case e'_4.inl
α : Type u
s : Set α
inst✝ : DivisionRing α
this : lift.{u, 0} #(Fin 6) < ℵ₀
h : #↑s < ℵ₀
⊢ max #↑s ℵ₀ = max (lift.{u, 0} #(Fin 6) + #↑s) ℵ₀

pp: case e'_4.inr
α : Type u
s : Set α
inst✝ : DivisionRing α
this : lift.{u, 0} #(Fin 6) < ℵ₀
h : ℵ₀ ≤ #↑s
⊢ max #↑s ℵ₀ = max (lift.{u, 0} #(Fin 6) + #↑s) ℵ₀

Tactic:
· rw [max_eq_right h.le, max_eq_right]
        exact (add_lt_aleph0 this h).le

Goal state after:
case e'_4.inr
α : Type u
s : Set α
inst✝ : DivisionRing α
this : lift.{u, 0} #(Fin 6) < ℵ₀
h : ℵ₀ ≤ #↑s
⊢ max #↑s ℵ₀ = max (lift.{u, 0} #(Fin 6) + #↑s) ℵ₀
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: case convert_3.inl
α : Type u
s : Set α
inst✝ : DivisionRing α
n : Fin 6
⊢ Finite (Operands s (Sum.inl n))

pp: case convert_3.inr
α : Type u
s : Set α
inst✝ : DivisionRing α
val✝ : ↑s
⊢ Finite (Operands s (Sum.inr val✝))

Tactic:
· fin_cases n <;> (dsimp only [id_eq]; infer_instance)

Goal state after:
case convert_3.inr
α : Type u
s : Set α
inst✝ : DivisionRing α
val✝ : ↑s
⊢ Finite (Operands s (Sum.inr val✝))
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
H : Set ι
x : M
hmem : x ∈ span R (e '' H)
i : ι
⊢ (ε i) x ≠ 0 → i ∈ H

Tactic:
hi

Goal state after:
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
H : Set ι
x : M
hmem : x ∈ span R (e '' H)
i : ι
hi : (ε i) x ≠ 0
⊢ i ∈ H
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: case refine_2
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)
⊢ LinearIndepOn R (⇑(span R s).mkQ) (sec '' t)

Tactic:
linearIndepOn_iff_image (hsec'.symm ▸ injective_id).injOn.image_of_comp,

Goal state after:
case refine_2
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)
⊢ LinearIndepOn R _root_.id (⇑(span R s).mkQ '' sec '' t)
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 ↥(map f L)
⊢ finrank R ↥(f.domRestrict L).ker = 0

Tactic:
← LinearMap.range_domRestrict

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✝⁴ : 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
⊢ finrank R ↥(f.domRestrict L).ker = 0
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: K : Type u_13
K₁ : Type u_14
V : Type u_16
V₁ : Type u_17
n : Type u_19
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Field K₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K₁ V₁
I₁ I₁' : K₁ →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V
v : n → V₁
hv₁ : B.IsOrthoᵢ v
hv₂ : ∀ (i : n), (B (v i)) (v i) ≠ 0
s : Finset n
w : n → K₁
hs : ∑ i ∈ s, w i • v i = 0
i : n
⊢ i ∈ s → w i = 0

Tactic:
hi

Goal state after:
K : Type u_13
K₁ : Type u_14
V : Type u_16
V₁ : Type u_17
n : Type u_19
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Field K₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K₁ V₁
I₁ I₁' : K₁ →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V
v : n → V₁
hv₁ : B.IsOrthoᵢ v
hv₂ : ∀ (i : n), (B (v i)) (v i) ≠ 0
s : Finset n
w : n → K₁
hs : ∑ i ∈ s, w i • v i = 0
i : n
hi : i ∈ s
⊢ w i = 0
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

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

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

Tactic:
· ext x y
    rw [comp_apply, compl₂_apply]
    exact h x y

Goal state after:
case mpr
R : Type u_1
M : Type u_5
M₁ : Type u_6
M₃ : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
I : R →+* R
B : M →ₗ[R] M →ₛₗ[I] M₃
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃
f : M →ₗ[R] M₁
g : M₁ →ₗ[R] M
h : B' ∘ₗ f = B.compl₂ g
⊢ B.IsAdjointPair B' ⇑f ⇑g
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)
x✝¹ : M →ₗ[R] N
x✝ : M
⊢ ((compRight R g ∘ₗ compRight R f) x✝¹) x✝ = (LinearMap.id x✝¹) x✝

Tactic:
exact congr($comp_eq_id _)

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
⊢ (dualAnnihilator W).dualCoannihilator = W

Tactic:
by
  refine le_antisymm (fun v ↦ Function.mtr ?_) (le_dualAnnihilator_dualCoannihilator _)
  simp only [mem_dualAnnihilator, mem_dualCoannihilator]
  rw [← Quotient.mk_eq_zero W, ← Module.forall_dual_apply_eq_zero_iff K]
  push Not
  refine fun ⟨φ, hφ⟩ ↦ ⟨φ.comp W.mkQ, fun w hw ↦ ?_, hφ⟩
  rw [comp_apply, mkQ_apply, (Quotient.mk_eq_zero W).mpr hw, φ.map_zero]

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

Goal state before:
pp: case neg
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ¬FiniteDimensional K V
⊢ ∀ (s : Finset V) (a : Basis (↑↑s) K V), False

pp: case neg
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ¬FiniteDimensional K V
⊢ ∀ (s : Finset (Dual K V)) (a : Basis (↑↑s) K (Dual K V)), False

Tactic:
· exact fun _ b ↦ h (Module.Finite.of_basis b)

Goal state after:
case neg
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ¬FiniteDimensional K V
⊢ ∀ (s : Finset (Dual K V)) (a : Basis (↑↑s) K (Dual K V)), False
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'
f : M →ₗ[R] M'
hf : Function.Surjective ⇑f.range.subtype.dualMap
⊢ f.dualMap.range = f.ker.dualAnnihilator

Tactic:
have rr_surj : Function.Surjective f.rangeRestrict := by
    rw [← range_eq_top, range_rangeRestrict]
  have := range_dualMap_eq_dualAnnihilator_ker_of_surjective f.rangeRestrict rr_surj
  convert! this using 1
  · calc
      _ = range ((range f).subtype.comp f.rangeRestrict).dualMap := by simp
      _ = _ := ?_
    rw [← dualMap_comp_dualMap, range_comp_of_range_eq_top]
    rwa [range_eq_top]
  · apply congr_arg
    exact (ker_rangeRestrict f).symm

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₂
⊢ Function.Injective ⇑f.dualMap ∧ Function.Injective ⇑f ↔ Function.Injective ⇑f ∧ Function.Surjective ⇑f

Tactic:
dualMap_injective_iff,

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₂
⊢ Function.Surjective ⇑f ∧ Function.Injective ⇑f ↔ Function.Injective ⇑f ∧ Function.Surjective ⇑f
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)
reassoc' : ∀ {W : C} (h' : R ⟶ W), NormalEpi.g ≫ g ≫ h' = 0 ≫ h'
⊢ (NormalEpi.g ≫ f) ≫ h = 0

Tactic:
rw [Category.assoc, comm, reassoc', zero_comp]

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

Goal state before:
pp: 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
⊢ IsLimit (KernelFork.ofι f ⋯)

Tactic:
haveI : Limits.HasImages C := hasImages

Goal state after:
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
⊢ IsLimit (KernelFork.ofι f ⋯)
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: 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
⊢ IsColimit (CokernelCofork.ofπ f ⋯)

Tactic:
haveI : Limits.HasImages C := hasImages

Goal state after:
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
⊢ IsColimit (CokernelCofork.ofπ f ⋯)
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono g
s : PushoutCocone f g
hs : IsColimit s
⊢ Mono s.inl

Tactic:
have : Mono (NatTrans.app (colimit.cocone (span f g)).ι WalkingCospan.left) :=
    Abelian.mono_pushout_of_mono_g f g

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono g
s : PushoutCocone f g
hs : IsColimit s
this : Mono ((colimit.cocone (span f g)).ι.app WalkingCospan.left)
⊢ Mono s.inl
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 φ'
⊢ QuasiIso (φ ≫ φ') ↔ QuasiIso φ

Tactic:
by
  constructor
  · intro
    exact quasiIso_of_comp_right φ φ'
  · intro
    exact quasiIso_comp φ φ'

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
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₂.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₂.f ⋯)
hf' : φ.τ₁ ≫ f' = h.f'
wπ : f' ≫ h.π = 0
hπ : IsColimit (CokernelCofork.ofπ h.π wπ)
⊢ S₂.LeftHomologyData

Tactic:
exact ⟨h.K, h.H, i, h.π, wi, hi, wπ, hπ⟩

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
inst✝¹ : S.HasLeftHomology
inst✝ : S.HasRightHomology
h : IsIso S.leftRightHomologyComparison
⊢ S.HasHomology

Tactic:
by
  have : IsIso (leftRightHomologyComparison' S.leftHomologyData S.rightHomologyData) := h
  exact hasHomology_of_isIso_leftRightHomologyComparison' S.leftHomologyData S.rightHomologyData

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₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ h₁.homologyIso.inv ≫ h₁.homologyIso.hom ≫ rightHomologyMap' φ h₁ h₂ =
    h₁.homologyIso.inv ≫ homologyMap φ ≫ h₂.homologyIso.hom

Tactic:
Iso.inv_hom_id_assoc,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ rightHomologyMap' φ h₁ h₂ = h₁.homologyIso.inv ≫ homologyMap φ ≫ h₂.homologyIso.hom
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
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₁.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₁.f ⋯)
hf' : f' ≫ i = S₁.f
hf'' : f' = φ.τ₁ ≫ h.f'
wπ : f' ≫ h.π = 0
hπ : IsColimit (CokernelCofork.ofπ h.π wπ)
⊢ S₁.LeftHomologyData

Tactic:
exact ⟨h.K, h.H, i, h.π, wi, hi, wπ, 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
⊢ cyclesMap (opMap φ) ≫ S₁.cyclesOpIso.hom = S₂.cyclesOpIso.hom ≫ (opcyclesMap φ).op

Tactic:
by
  rw [← cancel_mono (S₁.cyclesOpIso).inv, assoc, assoc, Iso.hom_inv_id, comp_id,
    cyclesOpIso_inv_naturality, Iso.hom_inv_id_assoc]

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
⊢ Abelian.image.ι S.f ≫ S.g = 0

Tactic:
by simp only [← cancel_epi (Abelian.factorThruImage S.f),
      kernel.lift_ι_assoc, zero, comp_zero]

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

Tactic:
by rw [h.comm₃, neg_comp]; abel

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
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst✝¹ : Epi π
inst✝ : Mono ι
⊢ S.toCycles ≫ (S.isoCyclesOfIsLimit hkf).inv ≫ (S.isoCyclesOfIsLimit hkf).hom ≫ S.homologyπ = 0

Tactic:
Iso.inv_hom_id_assoc,

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
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst✝¹ : Epi π
inst✝ : Mono ι
⊢ S.toCycles ≫ S.homologyπ = 0
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
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst✝¹ : Epi π
inst✝ : Mono ι
⊢ S.homologyι ≫ (S.isoOpcyclesOfIsColimit hcc).inv ≫ (S.isoOpcyclesOfIsColimit hcc).hom ≫ S.fromOpcycles = 0

Tactic:
Iso.inv_hom_id_assoc,

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
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst✝¹ : Epi π
inst✝ : Mono ι
⊢ S.homologyι ≫ S.fromOpcycles = 0
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

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.Exact
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : F.PreservesRightHomologyOf S
inst✝ : (S.map F).HasHomology
⊢ (S.map F).Exact

Tactic:
have : S.HasHomology := h.hasHomology

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 : ShortComplex C
h : S.Exact
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : F.PreservesRightHomologyOf S
inst✝ : (S.map F).HasHomology
this : S.HasHomology
⊢ (S.map F).Exact