mathlib-initiative/mathlib-tactics huggingface dataset:
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) (lift (s.snd ≫ fst A A ≫ ι) (s.fst ≫ fst A A) ≫ μ)) (s.fst ≫ snd A A) ≫
        (α_ A A A).hom ≫ A ◁ μ) ≫
      snd A A =
    s.snd ≫ snd A A

Tactic:
simp only [lift_lift_associator_hom_assoc, lift_whiskerLeft, lift_snd]

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.fst ≫ fst A A) ≫ μ) (s.fst ≫ snd A A) ≫ μ = s.snd ≫ snd A A
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
A Y Y' : C
inst✝ : Closed A
g : Y ⟶ Y'
⊢ (ihom A).map g = 𝟙 ((ihom A).obj Y) ≫ (ihom A).map g

Tactic:
id_comp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
A Y Y' : C
inst✝ : Closed A
g : Y ⟶ Y'
⊢ (ihom A).map g = (ihom A).map 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₁
x✝ : ∃ a, a • x = z
w : R
hw : w • x = z
⊢ ∃ y, f y • x = z

Tactic:
obtain ⟨y, rfl⟩ := hf w

Goal state after:
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₁
x✝ : ∃ a, a • x = z
y : M
hw : f y • x = z
⊢ ∃ y, f y • x = z
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Goal state before:
pp: case e_a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasLeftDual X
inst✝¹ : HasLeftDual Y
inst✝ : HasLeftDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ η_ (ᘁY) Y ≫ ((λ_ ᘁY).inv ≫ η_ (ᘁX) X ▷ ᘁY ≫ (ᘁX ◁ f) ▷ ᘁY ≫ (α_ (ᘁX) Y ᘁY).hom ≫ ᘁX ◁ ε_ (ᘁY) Y ≫ (ρ_ ᘁX).hom ⊗ₘ g) =
    η_ (ᘁX) X ≫ ᘁX ◁ f ≫ ᘁX ◁ g

Tactic:
calc
    _ = 𝟙 _ ⊗≫ ((𝟙_ C) ◁ η_ (ᘁY) Y ≫ η_ (ᘁX) X ▷ ((ᘁY) ⊗ Y)) ⊗≫ (ᘁX) ◁ f ▷ (ᘁY) ▷ Y ⊗≫
        (ᘁX) ◁ ε_ (ᘁY) Y ▷ Y ⊗≫ (ᘁX) ◁ g := by
      rw [tensorHom_def]; monoidal
    _ = η_ (ᘁX) X ⊗≫ (((ᘁX) ⊗ X) ◁ η_ (ᘁY) Y ≫ ((ᘁX) ◁ f) ▷ ((ᘁY) ⊗ Y)) ⊗≫
        (ᘁX) ◁ ε_ (ᘁY) Y ▷ Y ⊗≫ (ᘁX) ◁ g := by
      rw [whisker_exchange]; monoidal
    _ = η_ (ᘁX) X ⊗≫ ((ᘁX) ◁ f) ⊗≫ (ᘁX) ◁ (Y ◁ η_ (ᘁY) Y ⊗≫ ε_ (ᘁY) Y ▷ Y) ⊗≫ (ᘁX) ◁ g := by
      rw [whisker_exchange]; monoidal
    _ = η_ (ᘁX) X ≫ (ᘁX) ◁ f ≫ (ᘁX) ◁ g := by
      rw [coevaluation_evaluation'']; monoidal

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
s t : Submodule R M
⊢ Module.rank R ↥(s ⊔ t) ≤ Module.rank R ↥s + Module.rank R ↥t

Tactic:
← Submodule.rank_sup_add_rank_inf_eq

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
s t : Submodule R M
⊢ Module.rank R ↥(s ⊔ t) ≤ Module.rank R ↥(s ⊔ t) + Module.rank R ↥(s ⊓ t)
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

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

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
⊢ B.flip.SeparatingLeft ↔ ∀ (y : M₂), B.flip y = 0 → y = 0

Tactic:
separatingLeft_iff_linear_nontrivial

Goal state after:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
⊢ (∀ (x : M₂), B.flip x = 0 → x = 0) ↔ ∀ (y : M₂), B.flip y = 0 → y = 0
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f✝ g✝ : X ⟶ Y
h : Y ⟶ Z
w : f✝ ≫ h = g✝ ≫ h
inst✝³ : HasCoequalizer f✝ g✝
inst✝² : HasCoequalizer (G.map f✝) (G.map g✝)
inst✝¹ : PreservesColimit (parallelPair f✝ g✝) G
f g : X ⟶ Y
inst✝ : HasSplitEqualizer f g
⊢ PreservesLimit (parallelPair f g) G

Tactic:
by
  apply
    preservesLimit_of_preserves_limit_cone
      (HasSplitEqualizer.isSplitEqualizer f g).isEqualizer
  apply
    (isLimitMapConeForkEquiv G _).symm
      ((HasSplitEqualizer.isSplitEqualizer f g).map G).isEqualizer

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 W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')
this : F.ker = W ⊓ W'
x : Dual K ((V₁ ⧸ W) × V₁ ⧸ W')
⊢ ∃ y ∈ dualAnnihilator W, ∃ z ∈ dualAnnihilator W', y + z = F.dualMap x

Tactic:
obtain ⟨⟨a, b⟩, rfl⟩ := (dualProdDualEquivDual K (V₁ ⧸ W) (V₁ ⧸ W')).surjective x

Goal state after:
K : Type u_1
V₁ : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')
this : F.ker = W ⊓ W'
a : Dual K (V₁ ⧸ W)
b : Dual K (V₁ ⧸ W')
⊢ ∃ y ∈ dualAnnihilator W,
    ∃ z ∈ dualAnnihilator W', y + z = F.dualMap ((dualProdDualEquivDual K (V₁ ⧸ W) (V₁ ⧸ W')) (a, b))
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✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ⋯
Q : C := ⋯
s : Q ⟶ P := ⋯
t : Q ⟶ P := ⋯
I : C := ⋯
i : P ⟶ I := ⋯
⊢ IsColimit (Cofork.ofπ (G.map i) ⋯)

Tactic:
apply isColimitCoforkMapOfIsColimit
      apply coequalizerIsCoequalizer

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

Goal state before:
pp: case a.f
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
| a ≫ 𝟙 Y

pp: case a.g
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
| 0

pp: case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
| σ

Tactic:
case a.g => rw [show 0 = a ≫ (0 : Y ⟶ Y) by simp]

Goal state after:
case a.f
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
| a ≫ 𝟙 Y

case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
| σ
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
X Y : C
f : X ⟶ Y
inst✝ : IsIso (coimageImageComparison f)
F : MonoFactorisation f
⊢ inv (coimageImageComparison f) ≫ cokernel.desc (kernel.ι f) F.e ⋯ ≫ F.m = kernel.ι (cokernel.π f)

Tactic:
IsIso.inv_comp_eq

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasKernels C
inst✝¹ : HasCokernels C
X Y : C
f : X ⟶ Y
inst✝ : IsIso (coimageImageComparison f)
F : MonoFactorisation f
⊢ cokernel.desc (kernel.ι f) F.e ⋯ ≫ F.m = coimageImageComparison f ≫ kernel.ι (cokernel.π f)
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c : X ⟶ Y
⊢ a - b + c = a - (b - c)

Tactic:
rw [add_def, neg_def, sub_sub_sub, sub_zero]

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✝
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : HasZeroMorphisms D
X Y : D
i : X ⟶ Y
inst✝³ : HasCokernel i
F : D ⥤ C
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : Mono (F.map i)
inst✝ : PreservesColimit (parallelPair i 0) F
⊢ IsLimit (F.mapCone (KernelFork.ofι i ⋯))

Tactic:
let e : parallelPair (cokernel.π (F.map i)) 0 ≅ parallelPair (cokernel.π i) 0 ⋙ F :=
    parallelPair.ext (Iso.refl _) (asIso (cokernelComparison i F)) (by simp) (by simp)
  refine IsLimit.postcomposeInvEquiv e _ ?_
  let hi := Abelian.monoIsKernelOfCokernel _ (cokernelIsCokernel (F.map i))
  refine IsLimit.ofIsoLimit hi (Fork.ext (Iso.refl _) ?_)
  change 𝟙 _ ≫ F.map i ≫ 𝟙 _ = F.map i
  rw [Category.comp_id, Category.id_comp]

Goal state after:
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
β : ↑B
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ β • β⁻¹ • x = x

Tactic:
rw [← mul_smul, mul_inv_cancel, one_smul]

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₂
⊢ QuasiIso φ ↔ IsIso (homologyMap φ)

Tactic:
constructor
  · intro h
    infer_instance
  · intro h
    exact ⟨h⟩

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 : ShortComplex C
h : S.LeftHomologyData
hg : S.g = 0
⊢ 𝟙 S.X₂ ≫ 0 = 0

Tactic:
id_comp

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.LeftHomologyData
hg : S.g = 0
⊢ 0 = 0
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
hg : S.g = 0
φ : h.Q ⟶ (KernelFork.ofι h.ι ⋯).pt
hφ : φ ≫ h.ι = 𝟙 h.Q
⊢ h.ι = 𝟙 h.H ≫ h.ι

Tactic:
id_comp

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.RightHomologyData
hg : S.g = 0
φ : h.Q ⟶ (KernelFork.ofι h.ι ⋯).pt
hφ : φ ≫ h.ι = 𝟙 h.Q
⊢ h.ι = h.ι
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
⊢ S.g = 𝟙 S.X₂ ≫ S.g

Tactic:
id_comp

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
⊢ S.g = S.g
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']

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₁ ≫ γ.φ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 : ShortComplex C
inst✝ : S.HasLeftHomology
⊢ S.f = 𝟙 S.X₁ ≫ S.f

Tactic:
id_comp

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasLeftHomology
⊢ S.f = S.f
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: case refine_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
h₁ : IsIso (opcyclesMap φ)
h₂ : Mono φ.τ₃
h : (S₂.homologyι ≫ inv (opcyclesMap φ)) ≫ S₁.fromOpcycles = 0
z : S₂.homology ⟶ (KernelFork.ofι S₁.homologyι ⋯).pt
hz : z ≫ S₁.homologyι = S₂.homologyι ≫ inv (opcyclesMap φ)
⊢ S₂.homologyι = 𝟙 S₂.homology ≫ S₂.homologyι

Tactic:
id_comp

Goal state after:
case refine_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
h₁ : IsIso (opcyclesMap φ)
h₂ : Mono φ.τ₃
h : (S₂.homologyι ≫ inv (opcyclesMap φ)) ≫ S₁.fromOpcycles = 0
z : S₂.homology ⟶ (KernelFork.ofι S₁.homologyι ⋯).pt
hz : z ≫ S₁.homologyι = S₂.homologyι ≫ inv (opcyclesMap φ)
⊢ S₂.homologyι = S₂.homologyι
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₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasRightHomology
inst✝² : S₂.HasRightHomology
inst✝¹ : F.PreservesRightHomologyOf S₁
inst✝ : F.PreservesRightHomologyOf S₂
⊢ opcyclesMap' (F.mapShortComplex.map φ) (F.mapShortComplex.obj S₁).rightHomologyData
        (F.mapShortComplex.obj S₂).rightHomologyData ≫
      opcyclesMap' (𝟙 (S₂.map F)) (S₂.map F).rightHomologyData (S₂.rightHomologyData.map F) =
    opcyclesMap' (𝟙 (S₁.map F)) (S₁.map F).rightHomologyData (S₁.rightHomologyData.map F) ≫
      F.map (opcyclesMap' φ S₁.rightHomologyData S₂.rightHomologyData)

Tactic:
simp only [RightHomologyData.map_opcyclesMap', Functor.mapShortComplex_obj, ← opcyclesMap'_comp,
    comp_id, id_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 : ShortComplex C
inst✝ : S.HasLeftHomology
A : C
k k' : A ⟶ S.X₂
hk : k ≫ S.g = 0
hk' : k' ≫ S.g = 0
⊢ S.liftCycles k hk - S.liftCycles k' hk' = S.liftCycles (k - k') ⋯

Tactic:
simp only [← cancel_mono S.iCycles, liftCycles_i, sub_comp]

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✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : F.PreservesLeftHomologyOf S
inst✝ : (S.map F).HasHomology
this : S.HasHomology
h : 𝟙 S.leftHomologyData.H = 0
⊢ (S.map F).Exact

Tactic:
rw [S.leftHomologyData.exact_map_iff F, IsZero.iff_id_eq_zero,
    ← F.map_id, h, F.map_zero]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : IsLimit (KernelFork.ofι S.f ⋯)
inst✝ : S.HasHomology
⊢ hS.lift (KernelFork.ofι S.iCycles ⋯) ≫ S.f = 𝟙 S.cycles ≫ S.iCycles

Tactic:
id_comp

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : IsLimit (KernelFork.ofι S.f ⋯)
inst✝ : S.HasHomology
⊢ hS.lift (KernelFork.ofι S.iCycles ⋯) ≫ S.f = S.iCycles
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
s : S.Splitting
F : C ⥤ D
inst✝ : F.Additive
⊢ (S.map F).f ≫ F.map s.r = 𝟙 (S.map F).X₁

Tactic:
by
    dsimp [ShortComplex.map]
    rw [← F.map_comp, f_r, F.map_id]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
B A₁ A₂ : C
f : A₁ ⟶ B
g : A₂ ⟶ B
inst✝¹ : Mono f
inst✝ : Mono g
h : mk f ≤ mk g
⊢ ofMkLEMk f g h ≫ g = f

Tactic:
by simp [ofMkLEMk]

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

Goal state before:
pp: case mpr.refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h₁ : { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ }.Exact
h₂ : Mono φ.τ₂
⊢ φ.τ₂ = 𝟙 S₁.X₂ ≫ φ.τ₂

Tactic:
id_comp

Goal state after:
case mpr.refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h₁ : { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ }.Exact
h₂ : Mono φ.τ₂
⊢ φ.τ₂ = φ.τ₂
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: case mpr.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h₁ : { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ }.Exact
h₂ : Mono φ.τ₂
⊢ S₂.iCycles = 𝟙 S₂.cycles ≫ S₂.iCycles

Tactic:
id_comp

Goal state after:
case mpr.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h₁ : { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ }.Exact
h₂ : Mono φ.τ₂
⊢ S₂.iCycles = S₂.iCycles
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✝ : Balanced C
S : ShortComplex C
hS : S.Exact
s : S.X₃ ⟶ S.X₂
s_g : s ≫ S.g = 𝟙 S.X₃
hf : Mono S.f
⊢ S.f = 𝟙 S.X₁ ≫ S.f

Tactic:
id_comp

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✝¹ : Preadditive C
inst✝ : Balanced C
S : ShortComplex C
hS : S.Exact
s : S.X₃ ⟶ S.X₂
s_g : s ≫ S.g = 𝟙 S.X₃
hf : Mono S.f
⊢ S.f = S.f
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasInitial C
inst✝ : InitialMonoClass C
X : C
f : MonoOver X
⊢ Quotient.mk'' ⊥ ≤ Quotient.mk'' f

Tactic:
exact ⟨MonoOver.botLE f⟩

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasImages C
inst✝² : HasBinaryCoproducts C
inst✝¹ : HasInitial C
inst✝ : InitialMonoClass C
I : Type u_1
A B : C
s : Finset I
P : I → Subobject B
f : A ⟶ B
h : ∃ i ∈ s, (P i).Factors f
⊢ (s.sup P).Factors f

Tactic:
revert h
  induction s using Finset.induction_on with
  | empty => rintro ⟨_, ⟨⟨⟩, _⟩⟩
  | insert _ _ _ ih =>
    rintro ⟨j, ⟨m, h⟩⟩
    simp only [Finset.sup_insert]
    simp only [Finset.mem_insert] at m
    rcases m with (rfl | m)
    · exact sup_factors_of_factors_left h
    · exact sup_factors_of_factors_right (ih ⟨j, ⟨m, h⟩⟩)

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

Goal state before:
pp: case f
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : LocallySmall.{w, v₁, u₁} C
inst✝¹ : WellPowered.{w, v₁, u₁} C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
⊢ underlying.obj (sInf s) ⟶ underlying.obj f

Tactic:
exact (underlyingIso _).hom ≫
      Limits.limit.π (wideCospan s)
        (some ⟨equivShrink (Subobject A) f,
          Set.mem_image_of_mem (equivShrink (Subobject A)) hf⟩) ≫
      eqToHom (congr_arg (fun X : Subobject A => (X : C)) (Equiv.symm_apply_apply _ _))

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
F₁ F₂ : C ⥤ H
φ : F₁ ⟶ F₂
⊢ (𝟭 (C ⥤ H)).map φ ≫ L.leftKanExtensionUnit F₂ =
    L.leftKanExtensionUnit F₁ ≫ (L.lan ⋙ (whiskeringLeft C D H).obj L).map φ

Tactic:
ext; simp [lan]

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

Goal state before:
pp: case mpr
C : Type u_1
H : Type u_3
D : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_3, u_3} H
inst✝ : Category.{v_4, u_4} D
F' F'' : D ⥤ H
e : F' ≅ F''
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : L.whiskerLeft e.hom ≫ α' = α
a✝ : F''.IsRightKanExtension α'
⊢ 𝟙 (L ⋙ F'') ≫ α' = α'

Tactic:
id_comp

Goal state after:
case mpr
C : Type u_1
H : Type u_3
D : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_3, u_3} H
inst✝ : Category.{v_4, u_4} D
F' F'' : D ⥤ H
e : F' ≅ F''
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : L.whiskerLeft e.hom ≫ α' = α
a✝ : F''.IsRightKanExtension α'
⊢ α' = α'
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} D'
inst✝¹ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
inst✝ : L.HasPointwiseLeftKanExtension F
X₁ X₂ : C
f : X₁ ⟶ X₂
⊢ F.map f ≫ colimit.ι (CostructuredArrow.proj L (L.obj X₂) ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj X₂))) =
    colimit.ι (CostructuredArrow.proj L (L.obj X₂) ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj X₁) ≫ L.map f))

Tactic:
id_comp

Goal state after:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} D'
inst✝¹ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
inst✝ : L.HasPointwiseLeftKanExtension F
X₁ X₂ : C
f : X₁ ⟶ X₂
⊢ F.map f ≫ colimit.ι (CostructuredArrow.proj L (L.obj X₂) ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj X₂))) =
    colimit.ι (CostructuredArrow.proj L (L.obj X₂) ⋙ F) (CostructuredArrow.mk (L.map f))
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Small

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : D
T : C ⥤ D
inst✝¹ : EssentiallySmall.{w, v₁, u₁} C
inst✝ : LocallySmall.{w, v₂, u₂} D
⊢ EssentiallySmall.{w, v₁, max u₁ v₂} (StructuredArrow S T)

Tactic:
rw [← essentiallySmall_congr
    (StructuredArrow.pre S (equivSmallModel.{w} C).inverse T).asEquivalence]
  exact essentiallySmall_of_small_of_locallySmall _

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

Goal state before:
pp: J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
t : Cotrident f
desc : (s : Cotrident f) → t.pt ⟶ s.pt
fac : ∀ (s : Cotrident f), t.π ≫ desc s = s.π
uniq : ∀ (s : Cotrident f) (m : t.pt ⟶ s.pt), (∀ (j : WalkingParallelFamily J), t.ι.app j ≫ m = s.ι.app j) → m = desc s
s : Cocone (parallelFamily f)
j : WalkingParallelFamily J
⊢ t.ι.app zero ≫ desc s = s.ι.app zero

Tactic:
by rw [← t.w_assoc (line (Classical.arbitrary J)), fac, s.w]

Goal state after: