mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: case h₁
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ ((lift (fst (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (fst f' g') i₁)
            (snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (snd f' g') i₂) ⋯ ≫
          lift (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (fst f g) ⋯) (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (snd f g) ⋯) ⋯) ≫
        fst (fst (fst f' g') i₁) (fst (snd f' g') i₂)) ≫
      snd (fst f' g') i₁ =
    (𝟙 (pullback (fst (fst f' g') i₁) (fst (snd f' g') i₂)) ≫ fst (fst (fst f' g') i₁) (fst (snd f' g') i₂)) ≫
      snd (fst f' g') i₁

Tactic:
· simp only [Category.assoc, lift_snd, lift_fst, Category.id_comp]

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

Goal state before:
pp: case h₁.h₀.h₀
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ fst (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (fst f' g') i₁ ≫ i₁ =
    snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ fst (snd f' g') i₂ ≫ fst f' g'

Tactic:
← condition_assoc,

Goal state after:
case h₁.h₀.h₀
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ fst (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (fst f' g') i₁ ≫ i₁ =
    fst (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ fst (fst f' g') i₁ ≫ fst f' g'
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
⊢ P.isoClosure.colimitsOfShape J = P.colimitsOfShape J

Tactic:
by
  refine le_antisymm ?_ (colimitsOfShape_monotone _ (P.le_isoClosure))
  intro X ⟨h⟩
  choose obj h₁ h₂ using h.prop_diag_obj
  exact
   ⟨{ toColimitPresentation := h.changeDiag (h.diag.isoCopyObj obj (fun j ↦ (h₂ j).some)).symm
      prop_diag_obj := h₁ }⟩

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

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
P : ObjectProperty C
J : Type u'
inst✝² : Category.{v', u'} J
J' : Type u''
inst✝¹ : Category.{v'', u''} J'
inst✝ : Nonempty J
⊢ ⊥.colimitsOfShape J ≤ ⊥

Tactic:
colimitsOfShape_bot

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
P : ObjectProperty C
J : Type u'
inst✝² : Category.{v', u'} J
J' : Type u''
inst✝¹ : Category.{v'', u''} J'
inst✝ : Nonempty J
⊢ ⊥ ≤ ⊥
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

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
P : ObjectProperty C
J : Type u'
inst✝² : Category.{v', u'} J
J' : Type u''
inst✝¹ : Category.{v'', u''} J'
Q : ObjectProperty Cᵒᵖ
inst✝ : Q.IsClosedUnderColimitsOfShape J
⊢ Q.unop.IsClosedUnderLimitsOfShape Jᵒᵖ

Tactic:
← isClosedUnderColimitsOfShape_iff_unop

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
P : ObjectProperty C
J : Type u'
inst✝² : Category.{v', u'} J
J' : Type u''
inst✝¹ : Category.{v'', u''} J'
Q : ObjectProperty Cᵒᵖ
inst✝ : Q.IsClosedUnderColimitsOfShape J
⊢ Q.IsClosedUnderColimitsOfShape J
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
M N : Mon C
inst✝ : IsCommMonObj N.X
f : M ⟶ N
n : ℕ
⊢ (f ^ n).hom = f.hom ^ n

Tactic:
induction n <;> simp [pow_succ, *]

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

Goal state before:
pp: C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
inst✝ : P.IsClosedUnderLimitsOfShape (Discrete WalkingPair)
X Y : P.FullSubcategory
⊢ (ObjectProperty.homMk (fst X.obj Y.obj)).hom =
    (X ◁ (IsTerminal.ofUniqueHom (fun X ↦ ObjectProperty.homMk (toUnit X.obj)) ⋯).from Y ≫ (ρ_ X).hom).hom

Tactic:
exact fst_def X.1 Y.1

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✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
inst✝² : AddCommMonoid C
inst✝¹ : Module R C
inst✝ : Coalgebra R C
f : WithConv (C →ₗ[R] A)
⊢ 1 * f = f

Tactic:
ext; simp [convOne_def, ← map_comp_rTensor]

Goal state after:
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 A
inst✝¹ : Bialgebra R C
inst✝ : IsCocomm R C
f : WithConv (C →ₐc[R] A)
n : ℕ
⊢ toConv (f ^ (n + 1)).ofConv.toLinearMap = toConv f.ofConv.toLinearMap ^ (n + 1)

Tactic:
simp only [convPow_succ, pow_succ, toLinearMap_convMul, toLinearMap_convPow]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
A B X Y : C
inst✝¹ : Closed A
inst✝ : Closed B
f : Y ⟶ (ihom A).obj X
g : B ⟶ A
⊢ curry (uncurry (f ≫ (pre g).app X)) = curry (g ▷ Y ≫ uncurry f)

Tactic:
rw [curry_uncurry, ← curry_pre_app, curry_uncurry]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
w x y z : C
inst✝² : Closed w
inst✝¹ : Closed x
inst✝ : Closed y
⊢ w ◁ (α_ ((ihom w).obj x) ((ihom x).obj y) ((ihom y).obj z)).inv ≫
      (α_ w ((ihom w).obj x ⊗ (ihom x).obj y) ((ihom y).obj z)).inv ≫
        (w ◁
              curry
                ((α_ w ((ihom w).obj x) ((ihom x).obj y)).inv ≫
                  (ihom.ev w).app x ▷ (ihom x).obj y ≫ (ihom.ev x).app y)) ▷
            (ihom y).obj z ≫
          (ihom.ev w).app y ▷ (ihom y).obj z ≫ (ihom.ev y).app z =
    w ◁
        (ihom w).obj x ◁
          curry
            ((α_ x ((ihom x).obj y) ((ihom y).obj z)).inv ≫ (ihom.ev x).app y ▷ (ihom y).obj z ≫ (ihom.ev y).app z) ≫
      (α_ w ((ihom w).obj x) ((ihom x).obj z)).inv ≫ (ihom.ev w).app x ▷ (ihom x).obj z ≫ (ihom.ev x).app z

Tactic:
← comp_whiskerRight_assoc

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
w x y z : C
inst✝² : Closed w
inst✝¹ : Closed x
inst✝ : Closed y
⊢ w ◁ (α_ ((ihom w).obj x) ((ihom x).obj y) ((ihom y).obj z)).inv ≫
      (α_ w ((ihom w).obj x ⊗ (ihom x).obj y) ((ihom y).obj z)).inv ≫
        (w ◁
                curry
                  ((α_ w ((ihom w).obj x) ((ihom x).obj y)).inv ≫
                    (ihom.ev w).app x ▷ (ihom x).obj y ≫ (ihom.ev x).app y) ≫
              (ihom.ev w).app y) ▷
            (ihom y).obj z ≫
          (ihom.ev y).app z =
    w ◁
        (ihom w).obj x ◁
          curry
            ((α_ x ((ihom x).obj y) ((ihom y).obj z)).inv ≫ (ihom.ev x).app y ▷ (ihom y).obj z ≫ (ihom.ev y).app z) ≫
      (α_ w ((ihom w).obj x) ((ihom x).obj z)).inv ≫ (ihom.ev w).app x ▷ (ihom x).obj z ≫ (ihom.ev x).app z
Module: Mathlib.Data.W.Cardinal

Goal state before:
pp: α : Type u
β : α → Type v
⊢ (sum fun i ↦ lift.{v, max u v} #(WType β) ^ lift.{max u v, v} #(β i)) = sum fun a ↦ #(WType β) ^ lift.{u, v} #(β a)

Tactic:
lift_id'.{v, u},

Goal state after:
α : Type u
β : α → Type v
⊢ (sum fun i ↦ #(WType β) ^ lift.{max u v, v} #(β i)) = sum fun a ↦ #(WType β) ^ lift.{u, v} #(β a)
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 j : ι
⊢ ((b.dualBasis.toDual ∘ₗ b.toDual) (b i)) (b.dualBasis j) = ((Dual.eval R M) (b i)) (b.dualBasis j)

Tactic:
rw [LinearMap.comp_apply, toDual_apply_left, coe_toDual_self, ← coe_dualBasis,
    Dual.eval_apply, Basis.repr_self, Finsupp.single_apply, dualBasis_apply_self]

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
⊢ finrank R (M ⧸ N) + finrank R ↥N = finrank R M

Tactic:
← Nat.cast_inj (R := Cardinal),

Goal state after:
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)
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
s : Finset V
hs : s.Nonempty
lin_ind : LinearIndependent K Subtype.val
card_eq : s.card = finrank K V
⊢ ⇑(finsetBasisOfLinearIndependentOfCardEqFinrank hs lin_ind card_eq) = Subtype.val

Tactic:
by
  have : Nonempty s := ⟨⟨hs.choose, hs.choose_spec⟩⟩
  simp [finsetBasisOfLinearIndependentOfCardEqFinrank]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y : C
inst✝¹ : HasRightDual X
inst✝ : HasRightDual Y
f : X ⟶ Y
⊢ fᘁ ▷ X ≫ ε_ X Xᘁ = Yᘁ ◁ f ≫ ε_ Y Yᘁ

Tactic:
apply_fun tensorRightHomEquiv _ X (Xᘁ) _
  simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Products

Goal state before:
pp: R : Type u
inst✝ : Ring R
ι : Type v
Z : ι → ModuleCat R
s : Cone (Discrete.functor Z)
m : s.pt ⟶ (productCone Z).pt
w : ∀ (j : Discrete ι), m ≫ (productCone Z).π.app j = s.π.app j
x : ↑s.pt
⊢ (Hom.hom m) x = (Hom.hom (↟(LinearMap.pi fun j ↦ Hom.hom (s.π.app { as := j })))) x

Tactic:
funext i

Goal state after:
R : Type u
inst✝ : Ring R
ι : Type v
Z : ι → ModuleCat R
s : Cone (Discrete.functor Z)
m : s.pt ⟶ (productCone Z).pt
w : ∀ (j : Discrete ι), m ≫ (productCone Z).π.app j = s.π.app j
x : ↑s.pt
i : ι
⊢ (Hom.hom m) x i = (Hom.hom (↟(LinearMap.pi fun j ↦ Hom.hom (s.π.app { as := j })))) x i
Module: Mathlib.LinearAlgebra.Contraction

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

Tactic:
rw [← LinearEquiv.coe_toLinearMap, lTensorHomEquivHomLTensor_toLinearMap]

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module R P
inst✝⁴ : Module R Q
inst✝³ : Projective R M
inst✝² : Module.Finite R M
inst✝¹ : Projective R N
inst✝ : Module.Finite R N
x : (M →ₗ[R] P) ⊗[R] (N →ₗ[R] Q)
⊢ (homTensorHomEquiv R M N P Q) x = (homTensorHomMap (RingHom.id R) M N P Q) x

Tactic:
rw [← LinearEquiv.coe_toLinearMap, homTensorHomEquiv_toLinearMap]

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

Goal state before:
pp: V : Type uV
inst✝³ : AddCommMonoid V
R : Type u_1
inst✝² : Semiring R
inst✝¹ : Module R V
inst✝ : Projective R V
v : V
⊢ (∀ (φ : Dual R V), φ v = 0) ↔ v = 0

Tactic:
by
  refine ⟨fun h ↦ ?_, fun hv ↦ by simp [hv]⟩
  contrapose! h
  exact Projective.exists_dual_ne_zero R 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)
⊢ ∀ (s : PullbackCone f g),
    equalizer.lift (prod.lift (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right)) ⋯ ≫ e ≫ π₁ = s.fst

Tactic:
by 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 ↥(map f.rangeRestrict.dualMap f.range.subtype.dualMap.range) = finrank K ↥f.range

Tactic:
range_eq_top.mpr (dualMap_surjective_of_injective (range f).injective_subtype),

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 ⊤) = finrank K ↥f.range
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.IsEquivalence
X Y : C
f : X ⟶ Y
hf : NormalMono (F.map f)
W : D
h : NormalMono.Z (F.map f) ⟶ W
⊢ (F.map f ≫ NormalMono.g) ≫ h = 0 ≫ h

Tactic:
eq_whisker hf.w

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.IsEquivalence
X Y : C
f : X ⟶ Y
hf : NormalMono (F.map f)
W : D
h : NormalMono.Z (F.map f) ⟶ W
⊢ 0 ≫ h = 0 ≫ h
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
⊢ Mono (r A)

Tactic:
let hl : IsLimit (KernelFork.ofι (diag A) (cokernel.condition (diag A))) :=
    monoIsKernelOfCokernel _ (colimit.isColimit _)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hl : IsLimit (KernelFork.ofι (diag A) ⋯) :=
  monoIsKernelOfCokernel (colimit.cocone (parallelPair (diag A) 0)) (colimit.isColimit (parallelPair (diag A) 0))
⊢ Mono (r A)
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 : Mono f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
aux :
  ∀ (s : KernelFork (cokernel.π f)),
    (limit.lift (parallelPair (cokernel.π f) 0) s ≫ inv (imageMonoFactorisation f).e) ≫ Fork.ι (KernelFork.ofι f ⋯) =
      Fork.ι s
⊢ ∀ (s : KernelFork (cokernel.π f)) (m_1 : s.pt ⟶ (KernelFork.ofι f ⋯).pt),
    m_1 ≫ Fork.ι (KernelFork.ofι f ⋯) = Fork.ι s →
      m_1 = limit.lift (parallelPair (cokernel.π f) 0) s ≫ inv (imageMonoFactorisation f).e

Tactic:
intro A

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 : Mono f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
aux :
  ∀ (s : KernelFork (cokernel.π f)),
    (limit.lift (parallelPair (cokernel.π f) 0) s ≫ inv (imageMonoFactorisation f).e) ≫ Fork.ι (KernelFork.ofι f ⋯) =
      Fork.ι s
A : KernelFork (cokernel.π f)
⊢ ∀ (m_1 : A.pt ⟶ (KernelFork.ofι f ⋯).pt),
    m_1 ≫ Fork.ι (KernelFork.ofι f ⋯) = Fork.ι A →
      m_1 = limit.lift (parallelPair (cokernel.π f) 0) A ≫ inv (imageMonoFactorisation f).e
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
⊢ ∀ (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

Tactic:
intro A

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
A : CokernelCofork (kernel.ι f)
⊢ ∀ (m_1 : (CokernelCofork.ofπ f ⋯).pt ⟶ A.pt),
    Cofork.π (CokernelCofork.ofπ f ⋯) ≫ m_1 = Cofork.π A →
      m_1 =
        inv (imageMonoFactorisation f).m ≫ inv (coimageImageComparison f) ≫ colimit.desc (parallelPair (kernel.ι f) 0) A
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
        haveI : HasEqualizers C := Preadditive.hasEqualizers_of_hasKernels
        haveI : HasZeroObject C := Limits.hasZeroObject_of_hasFiniteBiproducts _
        have aux (s : CokernelCofork (kernel.ι f)) :
            Cofork.π (CokernelCofork.ofπ _ (kernel.condition f)) ≫
              inv (imageMonoFactorisation f).m ≫ inv (Abelian.coimageImageComparison f) ≫
                colimit.desc (parallelPair (kernel.ι f) 0) s = Cofork.π s := ?_
        · refine isColimitAux _ (fun A => inv (imageMonoFactorisation f).m ≫
                  inv (Abelian.coimageImageComparison f) ≫ colimit.desc _ _) aux ?_
          intro A g hg
          rw [CokernelCofork.π_ofπ] at hg
          rw [← cancel_epi f, hg, ← aux, CokernelCofork.π_ofπ]
        · simp only [CokernelCofork.π_ofπ, ← Category.assoc]
          convert! colimit.ι_desc s WalkingParallelPair.one using 2
          rw [IsIso.comp_inv_eq, IsIso.comp_inv_eq, eq_comm, ← imageMonoFactorisation_e']
          exact (imageMonoFactorisation f).fac

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
f✝ : X ⟶ Y
Z : C
g✝ : Y ⟶ Z
f g : Arrow C
u : f ⟶ g
⊢ kernel.ι f.hom ≫ Arrow.Hom.left u ≫ coimage.π g.hom = 0

Tactic:
simp [← Category.assoc, coimage.comp_π_eq_zero]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
f✝ : X ⟶ Y
Z : C
g✝ : Y ⟶ Z
f g : Arrow C
u : f ⟶ g
⊢ (kernel.ι f.hom ≫ Arrow.Hom.left u) ≫ g.hom = 0
Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso

Goal state before:
pp: case mpr
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:
· intro
    exact quasiIso_comp φ φ'

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

Goal state before:
pp: case mpr
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:
· intro
    exact quasiIso_comp φ φ'

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

Goal state before:
pp: case mp
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
⊢ IsIso (h₁.homologyIso.hom ≫ γ.φH ≫ h₂.homologyIso.inv) → IsIso γ.φH

Tactic:
intro h
    have : IsIso (γ.φH ≫ (RightHomologyData.homologyIso h₂).inv) :=
      IsIso.of_isIso_comp_left (RightHomologyData.homologyIso h₁).hom _
    exact IsIso.of_isIso_comp_right _ (RightHomologyData.homologyIso h₂).inv

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
hf : S.f = 0
⊢ S.f ≫ 𝟙 S.X₂ = 0

Tactic:
by rw [hf, comp_id]

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
hf : S.f = 0
c : KernelFork S.g
hc : IsLimit c
T : C
φ : S.X₂ ⟶ T
⊢ (ofIsLimitKernelFork S hf c hc).p ≫ (ofIsLimitKernelFork S hf c hc).descQ φ ⋯ = (ofIsLimitKernelFork S hf c hc).p ≫ φ

Tactic:
p_descQ

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
hf : S.f = 0
c : KernelFork S.g
hc : IsLimit c
T : C
φ : S.X₂ ⟶ T
⊢ φ = (ofIsLimitKernelFork S hf c hc).p ≫ φ
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
φK : h₁.K ⟶ h₂.K := h₂.liftK (h₁.i ≫ φ.τ₂) ⋯
commf' : h₁.f' ≫ φK = φ.τ₁ ≫ h₂.f'
⊢ LeftHomologyMapData φ h₁ h₂

Tactic:
let φH : h₁.H ⟶ h₂.H := h₁.descH (φK ≫ h₂.π)
    (by rw [reassoc_of% commf', h₂.f'_π, comp_zero])

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
φK : h₁.K ⟶ h₂.K := h₂.liftK (h₁.i ≫ φ.τ₂) ⋯
commf' : h₁.f' ≫ φK = φ.τ₁ ≫ h₂.f'
φH : h₁.H ⟶ h₂.H := h₁.descH (φK ≫ h₂.π) ⋯
⊢ LeftHomologyMapData φ h₁ h₂
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasLeftHomology
inst✝ : S₂.HasLeftHomology
⊢ leftHomologyMap φ = h₁.leftHomologyIso.hom ≫ γ.φH ≫ h₂.leftHomologyIso.inv

Tactic:
dsimp [LeftHomologyData.leftHomologyIso, leftHomologyMapIso']
  rw [← γ.leftHomologyMap'_eq, ← leftHomologyMap'_comp,
    ← leftHomologyMap'_comp, id_comp, comp_id]
  rfl

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
h₂ : S₂.RightHomologyData
φQ : h₁.Q ⟶ h₂.Q := h₁.descQ (φ.τ₂ ≫ h₂.p) ⋯
commg' : φQ ≫ h₂.g' = h₁.g' ≫ φ.τ₃
φH : h₁.H ⟶ h₂.H := h₂.liftH (h₁.ι ≫ φQ) ⋯
⊢ h₁.p ≫ φQ = φ.τ₂ ≫ h₂.p

Tactic:
by simp [φQ]

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.HasHomology
⊢ (S.rightHomologyIso.inv ≫ S.rightHomologyι) ≫ S.fromOpcycles = 0

Tactic:
simp only [assoc, rightHomologyι_comp_fromOpcycles, comp_zero]

Goal state after: