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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W₁ W₂ : MorphismProperty C
h : W₁ ≤ W₂
J : Type u_2
inst✝ : Category.{v_2, u_2} J
X Y : C
X₁✝ X₂✝ : J ⥤ C
c₁✝ : Cone X₁✝
c₂✝ : Cone X₂✝
h₁ : IsLimit c₁✝
h₂✝ : IsLimit c₂✝
f : X₁✝ ⟶ X₂✝
hf : W₁.functorCategory J f
⊢ W₂.limitsOfShape J (h₂✝.lift { pt := c₁✝.pt, π := c₁✝.π ≫ f })

Tactic:
exact ⟨_, _, _, _, h₁, _, f, fun j ↦ h _ (hf j)⟩

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
h : P ≤ Q
⊢ P.retractClosure ≤ Q.retractClosure

Tactic:
rintro X ⟨X', hX', ⟨e⟩⟩
  exact ⟨X', h _ hX', ⟨e⟩⟩

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
P : MorphismProperty C
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.RespectsIso
inst✝ : P.IsStableUnderBaseChange
X✝ Y✝ Z✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
h₁ : P.diagonal x✝¹
h₂ : P.diagonal x✝
⊢ P.diagonal (x✝¹ ≫ x✝)

Tactic:
rw [diagonal_iff, pullback.diagonal_comp]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
P : MorphismProperty C
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.RespectsIso
inst✝ : P.IsStableUnderBaseChange
X✝ Y✝ Z✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
h₁ : P.diagonal x✝¹
h₂ : P.diagonal x✝
⊢ P
    (pullback.diagonal x✝¹ ≫
      (pullbackDiagonalMapIdIso x✝¹ x✝¹ x✝).inv ≫
        pullback.snd (pullback.diagonal x✝) (pullback.map (x✝¹ ≫ x✝) (x✝¹ ≫ x✝) x✝ x✝ x✝¹ x✝¹ (𝟙 Z✝) ⋯ ⋯))
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 (lift (s.snd ≫ fst A A) (s.snd ≫ fst A A ≫ ι) ≫ μ) (s.fst ≫ fst A A) ≫ μ = s.fst ≫ fst A A

Tactic:
← assoc,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
s : PullbackCone μ μ
⊢ lift (lift (s.snd ≫ fst A A) ((s.snd ≫ fst A A) ≫ ι) ≫ μ) (s.fst ≫ fst A A) ≫ μ = s.fst ≫ fst A A
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 μ μ
this : lift (s.snd ≫ fst A A ≫ ι) (s.fst ≫ fst A A) ≫ μ = lift (s.snd ≫ snd A A) (s.fst ≫ snd A A ≫ ι) ≫ μ
⊢ lift (s.snd ≫ snd A A) (lift (s.fst ≫ snd A A ≫ ι) (s.fst ≫ snd A A) ≫ μ) ≫ μ = s.snd ≫ snd A A

Tactic:
← assoc,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
s : PullbackCone μ μ
this : lift (s.snd ≫ fst A A ≫ ι) (s.fst ≫ fst A A) ≫ μ = lift (s.snd ≫ snd A A) (s.fst ≫ snd A A ≫ ι) ≫ μ
⊢ lift (s.snd ≫ snd A A) (lift ((s.fst ≫ snd A A) ≫ ι) (s.fst ≫ snd A A) ≫ μ) ≫ μ = s.snd ≫ snd A A
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
s : PullbackCone μ μ
m : s.pt ⟶ (A ⊗ A) ⊗ A
hm₁ : m ≫ μ ▷ A = s.fst
hm₂ : m ≫ (α_ A A A).hom ≫ A ◁ μ = s.snd
h : m ≫ fst (A ⊗ A) A ≫ fst A A = s.snd ≫ fst A A
this : m ≫ fst (A ⊗ A) A ≫ μ = s.fst ≫ fst A A
⊢ m ≫ fst (A ⊗ A) A ≫ snd A A = lift (s.snd ≫ fst A A ≫ ι) (s.fst ≫ fst A A) ≫ μ

Tactic:
← assoc,

Goal state after:
case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
s : PullbackCone μ μ
m : s.pt ⟶ (A ⊗ A) ⊗ A
hm₁ : m ≫ μ ▷ A = s.fst
hm₂ : m ≫ (α_ A A A).hom ≫ A ◁ μ = s.snd
h : m ≫ fst (A ⊗ A) A ≫ fst A A = s.snd ≫ fst A A
this : (m ≫ fst (A ⊗ A) A) ≫ μ = s.fst ≫ fst A A
⊢ m ≫ fst (A ⊗ A) A ≫ snd A A = lift (s.snd ≫ fst A A ≫ ι) (s.fst ≫ fst A A) ≫ μ
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

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

Tactic:
MonoidalCategory.whiskerLeft_comp,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
A B : C
inst✝¹ : Closed A
inst✝ : Closed B
f : B ⟶ A
X Y : C
g : A ⊗ Y ⟶ X
⊢ (B ◁ curry g ≫ B ◁ (pre f).app X) ≫ (ihom.ev B).app X = f ▷ Y ≫ g
Module: Mathlib.Algebra.Module.LinearMap.DivisionRing

Goal state before:
pp: R : Type u_1
M : Type u_2
M₁ : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₁
inst✝² : Semiring R
inst✝¹ : Module R M
inst✝ : Module R M₁
f : M →ₗ[R] R
hf : Function.Surjective ⇑f
x z : M₁
⊢ z ∈ (f.smulRight x).range ↔ z ∈ R ∙ x

Tactic:
by
  simp_rw [mem_range, smulRight_apply, Submodule.mem_span_singleton]
  refine ⟨fun ⟨w, hw⟩ ↦ ⟨f w, hw ▸ rfl⟩, fun ⟨w, hw⟩ ↦ ?_⟩
  obtain ⟨y, rfl⟩ := hf w
  exact ⟨y, hw⟩

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
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_left h, add_eq_right h (this.le.trans h), max_eq_left h]

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

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Module.Basis ιK K (ι → K)
e : ℕ ↪ ι
this : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)
key : ℵ₀ ≤ Module.rank K (ι → K) ∧ lift.{v, u} #K ≤ Module.rank K (ι → K)
⊢ ℵ₀ ≤ #ιK

Tactic:
bK.mk_eq_rank''

Goal state after:
K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Module.Basis ιK K (ι → K)
e : ℕ ↪ ι
this : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)
key : ℵ₀ ≤ Module.rank K (ι → K) ∧ lift.{v, u} #K ≤ Module.rank K (ι → K)
⊢ ℵ₀ ≤ Module.rank K (ι → K)
Module: Mathlib.LinearAlgebra.Dimension.DivisionRing

Goal state before:
pp: K : Type u
V✝ V₁ V₂ V₃ : Type v
ι : Type w
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V✝
inst✝² : Module K V✝
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
V : Type u₀
x✝¹ : AddCommGroup V
x✝ : Module K V
b : Module.Basis (Module.Free.ChooseBasisIndex K V) K V := Module.Free.chooseBasis K V
⊢ lift.{?u.42, u₀} #↑(range ⇑b) = lift.{?u.42, u₀} (Module.rank K V)

Tactic:
mk_range_eq_of_injective b.injective,

Goal state after:
K : Type u
V✝ V₁ V₂ V₃ : Type v
ι : Type w
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V✝
inst✝² : Module K V✝
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
V : Type u₀
x✝¹ : AddCommGroup V
x✝ : Module K V
b : Module.Basis (Module.Free.ChooseBasisIndex K V) K V := Module.Free.chooseBasis K V
⊢ lift.{u₀, u₀} #(Module.Free.ChooseBasisIndex K V) = lift.{u₀, u₀} (Module.rank K V)
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
hB : IsSymm B
W : Submodule R M
hW : Disjoint W (ker B)
hB' : (domRestrict₁₂ B W W).IsRefl
x : M
hx : x ∈ W
h : ∀ (y : ↥W), ((domRestrict₁₂ B W W) ⟨x, hx⟩) y = 0
⊢ ⟨x, hx⟩ = 0

Tactic:
simp_rw [Subtype.forall, domRestrict₁₂_apply] at h

Goal state after:
R : Type u_1
M : Type u_5
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
hB : IsSymm B
W : Submodule R M
hW : Disjoint W (ker B)
hB' : (domRestrict₁₂ B W W).IsRefl
x : M
hx : x ∈ W
h : ∀ a ∈ W, (B x) a = 0
⊢ ⟨x, hx⟩ = 0
Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ∏ᶜ K.obj
⊢ PreservesLimit K G

Tactic:
let Q := ∏ᶜ fun f : Σ p : J × J, p.fst ⟶ p.snd => K.obj f.1.2

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ∏ᶜ K.obj
Q : C := ∏ᶜ fun f ↦ K.obj f.fst.2
⊢ PreservesLimit K G
Module: Mathlib.Algebra.Category.FGModuleCat.Colimits

Goal state before:
pp: J✝ : Type
inst✝⁴ : SmallCategory J✝
inst✝³ : FinCategory J✝
k : Type u
inst✝² : Ring k
J : Type
inst✝¹ : Finite J
Z : J → ModuleCat k
inst✝ : ∀ (j : J), Module.Finite k ↑(Z j)
⊢ Module.Finite k ↑(∐ fun j ↦ Z j)

Tactic:
by
  classical
exact (Module.Finite.equiv_iff (ModuleCat.coprodIsoDirectSum Z).toLinearEquiv).mpr inferInstance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
P Q : C
f : P ⟶ Q
I : C := Abelian.image f
p : P ⟶ Abelian.image f := Abelian.factorThruImage f
i : kernel (cokernel.π f) ⟶ Q := kernel.ι (cokernel.π f)
R : C
g : I ⟶ R
hpg : p ≫ g = 0
u : kernel g ⟶ Q := kernel.ι g ≫ i
hu : NormalMono u
h : Q ⟶ NormalMono.Z u := NormalMono.g
t : P ⟶ kernel g
ht : t ≫ kernel.ι g = p
fh : f ≫ h = 0
l : cokernel f ⟶ NormalMono.Z u
hl : cokernel.π f ≫ l = h
hih : i ≫ h = 0
s : kernel (cokernel.π f) ⟶ kernel g
hs : s ≫ u = i
hs' : (s ≫ kernel.ι g) ≫ i = 𝟙 I ≫ i
⊢ g = 0

Tactic:
have : Epi (kernel.ι g) := epi_of_epi_fac ((cancel_mono _).1 hs')

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
P Q : C
f : P ⟶ Q
I : C := Abelian.image f
p : P ⟶ Abelian.image f := Abelian.factorThruImage f
i : kernel (cokernel.π f) ⟶ Q := kernel.ι (cokernel.π f)
R : C
g : I ⟶ R
hpg : p ≫ g = 0
u : kernel g ⟶ Q := kernel.ι g ≫ i
hu : NormalMono u
h : Q ⟶ NormalMono.Z u := NormalMono.g
t : P ⟶ kernel g
ht : t ≫ kernel.ι g = p
fh : f ≫ h = 0
l : cokernel f ⟶ NormalMono.Z u
hl : cokernel.π f ≫ l = h
hih : i ≫ h = 0
s : kernel (cokernel.π f) ⟶ kernel g
hs : s ≫ u = i
hs' : (s ≫ kernel.ι g) ≫ i = 𝟙 I ≫ i
this : Epi (kernel.ι g)
⊢ g = 0
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
x : ↑B
⊢ (h x) (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) = fromCoset ⟨↑(Hom.hom f).range, ⋯⟩

Tactic:
by
  change ((τ).symm.trans (g x)).trans τ _ = _
  simp [-MonoidHom.coe_range, τ_symm_apply_fromCoset, g_apply_infinity, τ_apply_infinity]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
f : S₁ ⟶ S₂
⊢ IsIso f ↔ IsIso f.τ₁ ∧ IsIso f.τ₂ ∧ IsIso f.τ₃

Tactic:
by
  refine ⟨fun _ ↦ ⟨inferInstance, inferInstance, inferInstance⟩, ?_⟩
  rintro ⟨_, _, _⟩
  apply isIso_of_isIso

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 = 0

Tactic:
calc
      e = biprod.lift (0 : R ⟶ Y) e ≫ biprod.snd := by rw [biprod.lift_snd]
      _ = (d ≫ biprod.lift f (-g)) ≫ biprod.snd := by rw [← hd]
      _ = (0 ≫ biprod.lift f (-g)) ≫ biprod.snd := by rw [this]
      _ = 0 ≫ biprod.lift f (-g) ≫ biprod.snd := by rw [Category.assoc]
      _ = 0 := zero_comp

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₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
H : LeftHomologyMapData φ (LeftHomologyData.ofZeros S₁ hf₁ hg₁)
  (LeftHomologyData.ofIsLimitKernelFork S₂ hf₂ (KernelFork.ofι S₂.iCycles ⋯) S₂.cyclesIsKernel) :=
  { φK := S₂.liftCycles φ.τ₂ ⋯, φH := S₂.liftCycles φ.τ₂ ⋯, commi := ⋯, commf' := ⋯, commπ := ⋯ }
⊢ QuasiIso φ ↔ IsIso (S₂.liftCycles φ.τ₂ ⋯)

Tactic:
exact H.quasiIso_iff

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₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
H : RightHomologyMapData φ
  (RightHomologyData.ofIsColimitCokernelCofork S₁ hg₁ (CokernelCofork.ofπ S₁.pOpcycles ⋯) S₁.opcyclesIsCokernel)
  (RightHomologyData.ofZeros S₂ hf₂ hg₂) :=
  { φQ := S₁.descOpcycles φ.τ₂ ⋯, φH := S₁.descOpcycles φ.τ₂ ⋯, commp := ⋯, commg' := ⋯, commι := ⋯ }
⊢ QuasiIso φ ↔ IsIso (S₁.descOpcycles φ.τ₂ ⋯)

Tactic:
exact H.quasiIso_iff

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
h : S.RightHomologyData
A Q' H' : C
eQ : Q' ≅ h.Q
eH : H' ≅ h.H
⊢ S.f ≫ h.p ≫ eQ.inv = 0

Tactic:
← assoc,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : S.RightHomologyData
A Q' H' : C
eQ : Q' ≅ h.Q
eH : H' ≅ h.H
⊢ (S.f ≫ h.p) ≫ eQ.inv = 0
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
inst✝ : S.HasLeftHomology
hf : S.f = 0
⊢ S.cycles ≅ S.leftHomology

Tactic:
have := S.isIso_leftHomologyπ hf
  exact asIso S.leftHomologyπ

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
ψ₁ ψ₂ : RightHomologyMapData φ h₁ h₂
⊢ ψ₁ = ψ₂

Tactic:
have hQ : ψ₁.φQ = ψ₂.φQ := by rw [← cancel_epi h₁.p, commp, commp]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
ψ₁ ψ₂ : RightHomologyMapData φ h₁ h₂
hQ : ψ₁.φQ = ψ₂.φQ
⊢ ψ₁ = ψ₂
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
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst✝ : S.HasLeftHomology
A' : C
α : A' ⟶ A
⊢ (α ≫ k) ≫ S.g = 0

Tactic:
by rw [assoc, hk, 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
a b : S₁ ⟶ S₂
⊢ a + b = b + a

Tactic:
ext <;> apply add_comm

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 ι
⊢ H ≅ image (S.iCycles ≫ S.pOpcycles)

Tactic:
by
  have : ((S.isoCyclesOfIsLimit hkf).inv ≫ π) ≫ ι ≫
    (S.isoOpcyclesOfIsColimit hcc).hom = S.iCycles ≫ S.pOpcycles := by
    simp [← reassoc_of% fac]
  exact image.isoStrongEpiMono _ _ this

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

Goal state before:
pp: case mp
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : S.ShortExact
inst✝ : Balanced C
this✝¹ : HasZeroObject C
this✝ : Mono S.f
this : Epi S.g
⊢ IsIso S.f → IsZero S.X₃

Tactic:
intro hf
    simp only [IsZero.iff_id_eq_zero, ← cancel_epi S.g, ← cancel_epi S.f,
      S.zero_assoc, zero_comp]

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
inst✝¹ : S₁.HasRightHomology
inst✝ : S₂.HasRightHomology
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
⊢ rightHomologyMap (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) = 0

Tactic:
apply rightHomologyMap'_nullHomotopic

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₃ S : ShortComplex C
inst✝ : S.HasLeftHomology
A : C
k k' : A ⟶ S.X₂
hk : k ≫ S.g = 0
hk' : k' ≫ S.g = 0
⊢ (k - k') ≫ S.g = 0

Tactic:
rw [sub_comp, hk, hk', sub_zero]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.LeftExact

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : HasBinaryBiproducts C
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
⊢ PreservesLimit (parallelPair f g) F

Tactic:
let := preservesBinaryBiproducts_of_preservesBinaryProducts F

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : HasBinaryBiproducts C
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this : PreservesBinaryBiproducts F := preservesBinaryBiproducts_of_preservesBinaryProducts F
⊢ PreservesLimit (parallelPair f g) F
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: case mpr
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S : ShortComplex C
inst✝¹ : S.HasHomology
inst✝ : HasZeroObject C
e : S.homology ≅ 0
⊢ IsZero S.homology

Tactic:
exact IsZero.of_iso (isZero_zero C) e

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.LeftExact

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y Z : C
ι₁ : X ⟶ Z
ι₂ : Y ⟶ Z
inst✝ : PreservesColimit (parallelPair ι₂ 0) F
i : IsColimit (BinaryCofan.mk ι₁ ι₂)
⊢ IsColimit (F.mapCocone (BinaryCofan.mk ι₁ ι₂))

Tactic:
let bc := BinaryBicone.ofColimitCocone i

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y Z : C
ι₁ : X ⟶ Z
ι₂ : Y ⟶ Z
inst✝ : PreservesColimit (parallelPair ι₂ 0) F
i : IsColimit (BinaryCofan.mk ι₁ ι₂)
bc : BinaryBicone X Y := BinaryBicone.ofColimitCocone i
⊢ IsColimit (F.mapCocone (BinaryCofan.mk ι₁ ι₂))
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✝² : Preadditive C
inst✝¹ : Preadditive D
S : ShortComplex C
hS : S.Exact
inst✝ : HasZeroObject C
cc : CokernelCofork S.f
hcc : IsColimit cc
⊢ Mono ((hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) ⋯)).desc (CokernelCofork.ofπ S.g ⋯))

Tactic:
by
    have := hS.hasHomology
    refine ((MorphismProperty.monomorphisms C).arrow_mk_iso_iff ?_).2
      hS.mono_fromOpcycles
    refine Arrow.isoMk (IsColimit.coconePointUniqueUpToIso hcc S.opcyclesIsCokernel)
      (Iso.refl _) ?_
    apply Cofork.IsColimit.hom_ext hcc
    simp [IsColimit.coconePointUniqueUpToIso]

Goal state after:
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✝² : Preadditive C
inst✝¹ : Preadditive D
S : ShortComplex C
inst✝ : HasZeroObject C
s : S.Splitting
hi : IsLimit (KernelFork.ofι S.f ⋯)
f' : (KernelFork.ofι S.f ⋯).pt ⟶ (KernelFork.ofι S.f ⋯).pt := hi.lift (KernelFork.ofι S.f ⋯)
hf' : f' = 𝟙 (KernelFork.ofι S.f ⋯).pt
wπ : f' ≫ 0 = 0
⊢ Epi f'

Tactic:
rw [hf']; infer_instance

Goal state after:
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✝¹ : Preadditive C
inst✝ : Preadditive D
S : ShortComplex C
h : S.Splitting
⊢ (h.s.op ≫ S.op.f + S.op.g ≫ h.r.op).unop = (𝟙 S.op.X₂).unop

Tactic:
by
    simp only [op_X₂, Opposite.unop_op, op_X₁, op_f, op_X₃, op_g, unop_add, unop_comp,
      Quiver.Hom.unop_op, unop_id, ← h.id]
    abel

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
A : C
B : D
e : MonoOver A ≌ MonoOver B
⊢ lower e.inverse ⋙ lower e.functor ≅ 𝟭 (Subobject B)

Tactic:
apply eqToIso
    convert! ThinSkeleton.map_iso_eq e.counitIso
    · exact (ThinSkeleton.map_comp_eq _ _).symm
    · exact ThinSkeleton.map_id_eq.symm

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c c' : Cofan Z
f : Fan fun x ↦ op (Z x)
hc : IsColimit c
hc' : IsColimit c'
hf : IsLimit f
⊢ (opCoproductIsoProduct' hc hf).hom ≫ (opCoproductIsoProduct' hc' hf).inv = (hc.coconePointUniqueUpToIso hc').op.inv

Tactic:
by
  apply Quiver.Hom.unop_inj
  apply hc'.hom_ext
  intro ⟨j⟩
  change c'.inj _ ≫ _ = _
  simp only [unop_op, unop_comp, Discrete.functor_obj, Iso.op_inv,
    Quiver.Hom.unop_op, IsColimit.comp_coconePointUniqueUpToIso_inv]
  apply Quiver.Hom.op_inj
  simp only [op_comp, op_unop, Quiver.Hom.op_unop, Category.assoc,
    opCoproductIsoProduct'_inv_comp_inj]
  rw [← opCoproductIsoProduct'_inv_comp_inj hc hf]
  simp only [Iso.hom_inv_id_assoc]
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction

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
L : C ⥤ D
H : Type u_3
inst✝³ : Category.{v_3, u_3} H
inst✝² : ∀ (F : C ⥤ H), L.HasLeftKanExtension F
inst✝¹ : HasColimitsOfShape C H
inst✝ : HasColimitsOfShape D H
X✝ Y✝ : C ⥤ H
f : X✝ ⟶ Y✝
i : C
⊢ f.app i ≫ (L.lanUnit.app Y✝).app i ≫ colimit.ι (L.lan.obj Y✝) (L.obj i) =
    (L.lanUnit.app X✝).app i ≫ (L.lan.map f).app (L.obj i) ≫ colimit.ι (L.lan.obj Y✝) (L.obj i)

Tactic:
← assoc,

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
L : C ⥤ D
H : Type u_3
inst✝³ : Category.{v_3, u_3} H
inst✝² : ∀ (F : C ⥤ H), L.HasLeftKanExtension F
inst✝¹ : HasColimitsOfShape C H
inst✝ : HasColimitsOfShape D H
X✝ Y✝ : C ⥤ H
f : X✝ ⟶ Y✝
i : C
⊢ (f.app i ≫ (L.lanUnit.app Y✝).app i) ≫ colimit.ι (L.lan.obj Y✝) (L.obj i) =
    (L.lanUnit.app X✝).app i ≫ (L.lan.map f).app (L.obj i) ≫ colimit.ι (L.lan.obj Y✝) (L.obj i)
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
p : YonedaCollection F X
⊢ (map₁ η p).fst = p.fst

Tactic:
simp [map₁]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
p : YonedaCollection F X
⊢ (map₁ η p).snd =
    (ConcreteCategory.hom (G.map (eqToHom ⋯))) ((ConcreteCategory.hom (η.app (op (CostructuredArrow.mk p.fst)))) p.snd)

Tactic:
simp [map₁]

Goal state after: