mathlib-initiative/mathlib-tactics huggingface dataset:
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
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional K V
b : ι → V
lin_ind : LinearIndependent K b
card_eq : Fintype.card ι = finrank K V
⊢ span K (Set.range b) = ⊤

Tactic:
by_contra ne_top
  rw [← finrank_span_eq_card lin_ind] at card_eq
  exact ne_of_lt (Submodule.finrank_lt ne_top) card_eq

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
Y Z : C
inst✝ : HasLeftDual Z
f : Y ⟶ ᘁZ
⊢ 𝟙 Y ⊗≫ (η_ (ᘁZ) Z ▷ Y ≫ (ᘁZ ⊗ Z) ◁ f) ⊗≫ ᘁZ ◁ ε_ (ᘁZ) Z = f ⊗≫ η_ (ᘁZ) Z ▷ ᘁZ ⊗≫ ᘁZ ◁ ε_ (ᘁZ) Z

Tactic:
rw [← whisker_exchange]; monoidal

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

Goal state before:
pp: K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
h_contra : ∀ x ≤ finrank K V, ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ x.succ)
h_le_ker_pow : ∀ n ≤ (finrank K V).succ, n ≤ finrank K ↥(LinearMap.ker (f ^ n))
⊢ False

Tactic:
have h_any_n_lt : ∀ n, n ≤ (finrank K V).succ → n ≤ finrank K V := fun n hn =>
    (h_le_ker_pow n hn).trans (Submodule.finrank_le _)

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
h_contra : ∀ x ≤ finrank K V, ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ x.succ)
h_le_ker_pow : ∀ n ≤ (finrank K V).succ, n ≤ finrank K ↥(LinearMap.ker (f ^ n))
h_any_n_lt : ∀ n ≤ (finrank K V).succ, n ≤ finrank K V
⊢ False
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X X' Y : C
inst✝ : ExactPairing X' Y
i : X ≅ X'
⊢ η_ X' Y ▷ X ⊗≫ (i.inv ▷ (Y ⊗ X) ≫ X ◁ Y ◁ i.hom) ⊗≫ X ◁ ε_ X' Y =
    𝟙 (𝟙_ C ⊗ X) ⊗≫ (η_ X' Y ▷ X ≫ (X' ⊗ Y) ◁ i.hom) ⊗≫ (i.inv ▷ (Y ⊗ X') ≫ X ◁ ε_ X' Y) ⊗≫ 𝟙 (X ⊗ 𝟙_ C)

Tactic:
rw [← whisker_exchange]; monoidal

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

Goal state before:
pp: case mpr.inl
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 : I₁ a = 0
⊢ (B x) y = 0

pp: case mpr.inr
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 x) y = 0
⊢ (B x) y = 0

Tactic:
· rw [map_eq_zero I₁] at H
      trivial

Goal state after:
case mpr.inr
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 x) y = 0
⊢ (B x) y = 0
Module: Mathlib.Algebra.Category.FGModuleCat.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
V : FGModuleCat K
⊢ FGModuleCatDual K V ◁ FGModuleCatCoevaluation K V ≫
      (α_ (FGModuleCatDual K V) V (FGModuleCatDual K V)).inv ≫ FGModuleCatEvaluation K V ▷ FGModuleCatDual K V =
    (ρ_ (FGModuleCatDual K V)).hom ≫ (λ_ (FGModuleCatDual K V)).inv

Tactic:
by
  ext : 1
  apply contractLeft_assoc_coevaluation K V

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

Goal state before:
pp: n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M
inst✝¹ : Module R M₁
I I' : R →+* R
B : M →ₛₗ[I] M →ₛₗ[I'] M₁
inst✝ : Nontrivial R
v : Basis n R M
h : B.IsOrthoᵢ ⇑v
hB : B.SeparatingLeft
i : n
ho : (B (v i)) (v i) = 0
vi : n →₀ R
j : n
⊢ (B (v i)) (vi j • v j) = 0

Tactic:
rw [map_smulₛₗ]

Goal state after:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M
inst✝¹ : Module R M₁
I I' : R →+* R
B : M →ₛₗ[I] M →ₛₗ[I'] M₁
inst✝ : Nontrivial R
v : Basis n R M
h : B.IsOrthoᵢ ⇑v
hB : B.SeparatingLeft
i : n
ho : (B (v i)) (v i) = 0
vi : n →₀ R
j : n
⊢ I' (vi j) • (B (v i)) (v j) = 0
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
x : M
⊢ (B x) x = 0 ↔ x ∈ ker B

Tactic:
LinearMap.mem_ker

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
x : M
⊢ (B x) x = 0 ↔ B x = 0
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: case e'_2
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, (L i).ker ≤ K.ker
x✝¹ : Fintype ι
φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi L
p : Submodule 𝕜 E := ⨅ i, (L i).ker
p_eq : p = φ.ker
ψ : E ⧸ p →ₗ[𝕜] ι → 𝕜 := p.liftQ φ ⋯
x✝ : FiniteDimensional 𝕜 (E ⧸ p)
L' : ι → E ⧸ p →ₗ[𝕜] 𝕜 := fun i ↦ p.liftQ (L i) ⋯
K' : E ⧸ p →ₗ[𝕜] 𝕜 := p.liftQ K h
this : ⨅ i, (L' i).ker ≤ K'.ker
c : ι → 𝕜
hK' : ∑ i, c i • L' i = K'
x : E
⊢ (∑ i, c i • p.liftQ (L i) ⋯ ∘ₗ p.mkQ) x = (∑ i, c i • L' i) (p.mkQ x)

Tactic:
simp only [L', LinearMap.coe_sum, Finset.sum_apply, smul_apply, coe_comp, Function.comp_apply,
    smul_eq_mul]

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

Goal state before:
pp: K : Type u_1
V₁ : Type u_2
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
inst✝ : FiniteDimensional K V₁
f g : Dual K V₁
x : V₁
h : LinearMap.ker f = LinearMap.ker g
h' : f x = g x
hx : f x ≠ 0
p : Submodule K V₁ := K ∙ x
hp : p ≠ ⊥
hpf : Disjoint (LinearMap.ker f) p
hf : f ≠ 0
y : V₁
hy : y ∈ LinearMap.ker f
z : V₁
hz : z ∈ p
hy' : g y = 0
⊢ f y = 0

Tactic:
LinearMap.mem_ker

Goal state after:
K : Type u_1
V₁ : Type u_2
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
inst✝ : FiniteDimensional K V₁
f g : Dual K V₁
x : V₁
h : LinearMap.ker f = LinearMap.ker g
h' : f x = g x
hx : f x ≠ 0
p : Submodule K V₁ := K ∙ x
hp : p ≠ ⊥
hpf : Disjoint (LinearMap.ker f) p
hf : f ≠ 0
y : V₁
hy : f y = 0
z : V₁
hz : z ∈ p
hy' : g y = 0
⊢ f y = 0
Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasEqualizers C
inst✝² : HasFiniteProducts C
G : C ⥤ D
inst✝¹ : PreservesLimitsOfShape WalkingParallelPair G
inst✝ : PreservesFiniteProducts G
⊢ ∀ (J : Type) [inst : SmallCategory J] [FinCategory J], PreservesLimitsOfShape J G

Tactic:
intros
    apply preservesLimit_of_preservesEqualizers_and_product

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

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : SmallCategory J
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : J ⥤ C
c₁ : Cofan fun f ↦ F.obj f.fst.1
c₂ : Cofan F.obj
s t : c₁.pt ⟶ c₂.pt
hs : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), c₁.ι.app { as := f } ≫ s = F.map f.snd ≫ c₂.ι.app { as := f.fst.2 }
ht : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), c₁.ι.app { as := f } ≫ t = c₂.ι.app { as := f.fst.1 }
i : Cofork s t
t₁ : IsColimit c₁
t₂ : IsColimit c₂
hi : IsColimit i
q : Cocone F
⊢ c₂.pt ⟶ q.1

Tactic:
refine t₂.desc (Cofan.mk _ fun j => ?_)
      apply q.ι.app j

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
⊢ G.map (Fork.ι c ≫ f) = 0

Tactic:
c.condition,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
⊢ G.map 0 = 0
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : CokernelCofork f
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
⊢ G.map (f ≫ Cofork.π c) = 0

Tactic:
c.condition,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : CokernelCofork f
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
⊢ G.map 0 = 0
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
⊢ leftHomologyMap' (𝟙 S) S.homologyData.left S.leftHomologyData ≫
      leftHomologyMap' (𝟙 S) S.leftHomologyData S.leftHomologyData =
    leftHomologyMap' (𝟙 S) S.homologyData.left S.leftHomologyData

Tactic:
← leftHomologyMap'_comp,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
⊢ leftHomologyMap' (𝟙 S ≫ 𝟙 S) S.homologyData.left S.leftHomologyData =
    leftHomologyMap' (𝟙 S) S.homologyData.left S.leftHomologyData
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
e : S₁ ≅ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ leftHomologyMap' e.hom h₁ h₂ ≫ leftHomologyMap' e.inv h₂ h₁ = 𝟙 h₁.H

Tactic:
← leftHomologyMap'_comp,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
e : S₁ ≅ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ leftHomologyMap' (e.hom ≫ e.inv) h₁ h₁ = 𝟙 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₁ S₂ S₃ : ShortComplex C
e : S₁ ≅ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ leftHomologyMap' e.inv h₂ h₁ ≫ leftHomologyMap' e.hom h₁ h₂ = 𝟙 h₂.H

Tactic:
← leftHomologyMap'_comp,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
e : S₁ ≅ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ leftHomologyMap' (e.inv ≫ e.hom) h₂ h₂ = 𝟙 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 φ =
    leftHomologyMap' (𝟙 S₁) S₁.leftHomologyData h₁ ≫
      leftHomologyMap' φ h₁ h₂ ≫ leftHomologyMap' (𝟙 S₂) h₂ S₂.leftHomologyData

Tactic:
← leftHomologyMap'_comp,

Goal state after:
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 φ =
    leftHomologyMap' (𝟙 S₁) S₁.leftHomologyData h₁ ≫ leftHomologyMap' (φ ≫ 𝟙 S₂) h₁ S₂.leftHomologyData
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 φ =
    leftHomologyMap' (𝟙 S₁) S₁.leftHomologyData h₁ ≫ leftHomologyMap' (φ ≫ 𝟙 S₂) h₁ S₂.leftHomologyData

Tactic:
← leftHomologyMap'_comp,

Goal state after:
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 φ = leftHomologyMap' (𝟙 S₁ ≫ φ ≫ 𝟙 S₂) S₁.leftHomologyData S₂.leftHomologyData
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
inst✝ : S.HasRightHomology
⊢ Epi S.pOpcycles

Tactic:
by
  dsimp only [pOpcycles]
  infer_instance

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
h : S.RightHomologyData
⊢ h.homologyIso.inv ≫ S.homologyι = h.ι ≫ h.opcyclesIso.inv

Tactic:
dsimp only [homologyι, homologyIso]
  simp only [Iso.trans_inv, Iso.symm_inv, assoc, Iso.hom_inv_id_assoc,
    rightHomologyIso_inv_comp_rightHomologyι]

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
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst✝ : S.HasRightHomology
A' : C
α : A ⟶ A'
⊢ S.descOpcycles k hk ≫ α = S.descOpcycles (k ≫ α) ⋯

Tactic:
simp only [← cancel_epi S.pOpcycles, p_descOpcycles_assoc, p_descOpcycles]

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

Tactic:
by rw [neg_τ₂, neg_τ₂, h.comm₂, neg_add_rev, comp_neg, neg_comp]; abel

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : HasZeroMorphisms C
inst✝⁴ : HasZeroMorphisms D
S : ShortComplex C
hr : S.RightHomologyData
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
inst✝² : S.HasHomology
inst✝¹ : (S.map F).HasHomology
inst✝ : F.PreservesRightHomologyOf S
⊢ (((S.map F).homologyData.iso.hom ≫
          rightHomologyMap' (𝟙 (S.map F)) (S.map F).homologyData.right (S.map F).rightHomologyData) ≫
        rightHomologyMap' (𝟙 (S.map F)) (S.map F).rightHomologyData (S.homologyData.right.map F)) ≫
      F.map
        (rightHomologyMap' (𝟙 S) S.homologyData.right S.rightHomologyData ≫
          rightHomologyMap' (𝟙 S) S.rightHomologyData S.homologyData.right ≫ S.homologyData.iso.inv) =
    (((S.map F).homologyData.iso.hom ≫
          rightHomologyMap' (𝟙 (S.map F)) (S.map F).homologyData.right (S.map F).rightHomologyData) ≫
        rightHomologyMap' (𝟙 (S.map F)) (S.map F).rightHomologyData (hr.map F)) ≫
      F.map
        (rightHomologyMap' (𝟙 S) hr S.rightHomologyData ≫
          rightHomologyMap' (𝟙 S) S.rightHomologyData S.homologyData.right ≫ S.homologyData.iso.inv)

Tactic:
simp only [assoc, F.map_comp, map_rightHomologyMap', ← rightHomologyMap'_comp_assoc]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
e : S₁ ≅ S₂
⊢ S₁.ShortExact ↔ S₂.ShortExact

Tactic:
by
  constructor
  · exact shortExact_of_iso e
  · exact shortExact_of_iso e.symm

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✝⁴ : HasFiniteCoproducts C
inst✝³ : HasCoequalizers C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroObject D
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
this✝² : PreservesColimitsOfShape WalkingParallelPair F := preservesCoequalizers_of_preservesCokernels F
this✝¹ : PreservesColimit (empty C) F := preservesInitialObject_of_preservesZeroMorphisms F
this✝ : PreservesColimitsOfShape (Discrete PEmpty.{1}) F := preservesColimitsOfShape_pempty_of_preservesInitial F
this : PreservesFiniteCoproducts F :=
  { preserves := fun x ↦ PreservesFiniteCoproducts.of_preserves_binary_and_initial F (Fin x) }
⊢ PreservesFiniteColimits F

Tactic:
exact preservesFiniteColimits_of_preservesCoequalizers_and_finiteCoproducts F

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
P : Subobject Y
f : X ⟶ Y
⊢ ∀ (a b : MonoOver Y), (isIsomorphicSetoid (MonoOver Y)) a b → a.Factors f = b.Factors f

Tactic:
rintro P Q ⟨h⟩
      apply propext
      constructor
      · rintro ⟨i, w⟩
        exact ⟨i ≫ h.hom.hom.left, by rw [Category.assoc, Over.w h.hom.hom, w]⟩
      · rintro ⟨i, w⟩
        exact ⟨i ≫ h.inv.hom.left, by rw [Category.assoc, Over.w h.inv.hom, w]⟩

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:
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.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
⊢ (kernelSubobject f).arrow ≫ f = 0

Tactic:
rw [← kernelSubobject_arrow]

Goal state after:
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) ≫ f = 0
Module: Mathlib.CategoryTheory.Limits.Filtered

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ IsFiltered C ↔
    ∀ {J : Type v} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ C), ∃ X, Nonempty (limit (F.op ⋙ yoneda.obj X))

Tactic:
by
  rw [IsFiltered.iff_cocone_nonempty.{v}]
  refine ⟨fun h J _ _ F => ?_, fun h J _ _ F => ?_⟩
  · obtain ⟨c⟩ := h F
    exact ⟨c.pt, ⟨(limitCompYonedaIsoCocone F c.pt).inv c.ι⟩⟩
  · obtain ⟨pt, ⟨ι⟩⟩ := h F
    exact ⟨⟨pt, (limitCompYonedaIsoCocone F pt).hom ι⟩⟩

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
hX : IsInitial X
A : C
i : A ⟶ X
w✝ : Mono i
fac : hX.to A ≫ i = 𝟙 X
⊢ i ≫ hX.to A = 𝟙 A

Tactic:
← cancel_mono i,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
hX : IsInitial X
A : C
i : A ⟶ X
w✝ : Mono i
fac : hX.to A ≫ i = 𝟙 X
⊢ (i ≫ hX.to A) ≫ i = 𝟙 A ≫ i
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A B : C
inst✝ : HasBinaryProduct A B
⊢ (opProdIsoCoprod A B).hom.unop ≫ prod.fst = coprod.inl.unop

Tactic:
by
  simp [opProdIsoCoprod]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A B : C
inst✝ : HasBinaryProduct A B
⊢ (opProdIsoCoprod A B).hom.unop ≫ prod.snd = coprod.inr.unop

Tactic:
by
  simp [opProdIsoCoprod]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A F G : Cᵒᵖ ⥤ Type v
η : F ⟶ A
μ : G ⟶ A
ε : F ⟶ G
hε : ε ≫ μ = η
X : C
s : yoneda.obj X ⟶ A
u : F.obj (op X)
h : MakesOverArrow η s u
⊢ (ConcreteCategory.hom (μ.app (op X))) ((ConcreteCategory.hom (ε.app (op X))) u) = yonedaEquiv s

Tactic:
by rw [← comp_apply, ← NatTrans.comp_app, hε, h.app]

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
⊢ colimit.ι X✝ i ≫ colim.map f ≫ ((L.lan.obj Y✝).colimitIsoOfIsLeftKanExtension (L.lanUnit.app Y✝)).symm.hom =
    colimit.ι X✝ i ≫ ((L.lan.obj X✝).colimitIsoOfIsLeftKanExtension (L.lanUnit.app X✝)).symm.hom ≫ (L.lan ⋙ colim).map f

Tactic:
dsimp
      rw [ι_colimMap_assoc, ι_colimitIsoOfIsLeftKanExtension_inv,
        ι_colimitIsoOfIsLeftKanExtension_inv_assoc, ι_colimMap, ← assoc, ← assoc]
      congr 1
      exact congr_app (L.lanUnit.naturality f) i

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory

Goal state before:
pp: C✝ : Type u₁
inst✝⁸ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁷ : Category.{v₂, u₂} D✝
E✝ : Type u₃
inst✝⁶ : Category.{v₃, u₃} E✝
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
J : Type u_4
inst✝² : Category.{v_4, u_4} J
inst✝¹ : HasLimitsOfShape J D
F : D ⥤ E
inst✝ : PreservesLimitsOfShape J F
K : J ⥤ C ⥤ D
c : Cone K
hc : IsLimit c
⊢ IsLimit (((whiskeringRight C D E).obj F).mapCone c)

Tactic:
by
      apply evaluationJointlyReflectsLimits _ (fun k => ?_)
      change IsLimit (((evaluation _ _).obj k ⋙ F).mapCone c)
      exact isLimitOfPreserves _ hc

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝² : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
inst✝¹ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
e : A ≅ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
inst✝ :
  PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂, max (max (max u₁ v₁) v₂) w, v₂,
      max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂}
    L
⊢ L.IsLeftKanExtension e.hom

Tactic:
rw [isLeftKanExtension_along_uliftYoneda_iff]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝² : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
inst✝¹ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
e : A ≅ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
inst✝ :
  PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂, max (max (max u₁ v₁) v₂) w, v₂,
      max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂}
    L
⊢ IsIso e.hom ∧
    PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂, max (max (max u₁ v₁) v₂) w, v₂,
        max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂}
      L
Module: Mathlib.CategoryTheory.Subobject.Comma

Goal state before:
pp: case refine_1
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits T
A P Q : StructuredArrow S T
f : P ⟶ A
g : Q ⟶ A
hf : Mono f
hg : Mono g
h :
  { toFun := fun P ↦ ⟨projectSubobject P, ⋯⟩, invFun := fun P ↦ liftSubobject ↑P ⋯, left_inv := ⋯, right_inv := ⋯ }
      (Subobject.mk f) ≤
    { toFun := fun P ↦ ⟨projectSubobject P, ⋯⟩, invFun := fun P ↦ liftSubobject ↑P ⋯, left_inv := ⋯, right_inv := ⋯ }
      (Subobject.mk g)
⊢ P ⟶ Q

Tactic:
exact homMk (Subobject.ofMkLEMk _ _ h)
        ((cancel_mono (T.map g.right)).1 (by simp [← T.map_comp]))

Goal state after: