mathlib-initiative/mathlib-tactics huggingface dataset:
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) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap (s ⊔ t).subtype t) +
      Module.rank R ↥(s ⊓ t) =
    Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap s.subtype s ⊓ comap s.subtype t) +
      Module.rank R ↥((s ⊔ t) ⊓ t)

Tactic:
← comap_inf,

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) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap (s ⊔ t).subtype t) +
      Module.rank R ↥(s ⊓ t) =
    Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap s.subtype (s ⊓ t)) +
      Module.rank R ↥((s ⊔ t) ⊓ t)
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : X ⟶ Z ⊗ Y'
⊢ (fun f ↦ (ρ_ X).inv ≫ X ◁ η_ Y Y' ≫ (α_ X Y Y').inv ≫ f ▷ Y')
      ((fun f ↦ f ▷ Y ≫ (α_ Z Y' Y).hom ≫ Z ◁ ε_ Y Y' ≫ (ρ_ Z).hom) f) =
    f

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

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 Y' Z Z' : C
inst✝ : ExactPairing Y Y'
f : Y' ⊗ X ⟶ Z
g : Z ⟶ Z'
⊢ (tensorLeftHomEquiv X Y Y' Z') (f ≫ g) = (tensorLeftHomEquiv X Y Y' Z) f ≫ Y ◁ g

Tactic:
simp [tensorLeftHomEquiv]

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 X' Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : X ⟶ X'
g : X' ⟶ Y ⊗ Z
⊢ (tensorLeftHomEquiv X Y Y' Z).symm (f ≫ g) = Y' ◁ f ≫ (tensorLeftHomEquiv X' Y Y' Z).symm g

Tactic:
simp [tensorLeftHomEquiv]

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 X' Y : C
inst✝ : ExactPairing X' Y
i : X ≅ X'
⊢ Y ◁ η_ X' Y ≫ Y ◁ (i.inv ≫ i.hom) ▷ Y ⊗≫ ε_ X' Y ▷ Y = Y ◁ η_ X' Y ⊗≫ ε_ X' Y ▷ Y

Tactic:
rw [Iso.inv_hom_id]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X X' Y : C
inst✝ : ExactPairing X' Y
i : X ≅ X'
⊢ Y ◁ η_ X' Y ≫ Y ◁ 𝟙 X' ▷ Y ⊗≫ ε_ X' Y ▷ Y = Y ◁ η_ X' Y ⊗≫ ε_ X' Y ▷ Y
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

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

Tactic:
rw [Iso.inv_hom_id]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y Y' : C
inst✝ : ExactPairing X Y'
i : Y ≅ Y'
⊢ η_ X Y' ▷ X ⊗≫ X ◁ 𝟙 Y' ▷ X ≫ X ◁ ε_ X Y' = η_ X Y' ▷ X ⊗≫ X ◁ ε_ X Y'
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 : C
f g : X ⟶ Y
inst✝² : HasCoequalizer f g
inst✝¹ : HasCoequalizer (G.map f) (G.map g)
inst✝ : PreservesColimit (parallelPair f g) G
W : D
k : G.obj Y ⟶ W
wk : G.map f ≫ k = G.map g ≫ k
⊢ G.map (coequalizer.π f g) ≫ (PreservesCoequalizer.iso G f g).inv ≫ coequalizer.desc k wk = k

Tactic:
rw [← Category.assoc, map_π_preserves_coequalizer_inv, coequalizer.π_desc]

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

Goal state before:
pp: case of_equiv
K : Type u_1
V₁ : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
α β : Type u_4
h : α ≃ β
hyp : ∀ (W : α → Subspace K V₁), dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)
W : β → Subspace K V₁
⊢ dualAnnihilator (⨅ x, W (h x)) = ⨆ i, dualAnnihilator (W i)

Tactic:
hyp _,

Goal state after:
case of_equiv
K : Type u_1
V₁ : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
α β : Type u_4
h : α ≃ β
hyp : ∀ (W : α → Subspace K V₁), dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)
W : β → Subspace K V₁
⊢ ⨆ i, dualAnnihilator (W (h i)) = ⨆ i, dualAnnihilator (W i)
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set ι
v : ι → V
hli : LinearIndepOn K id (v '' s)
b : Basis (↑(hli.extend ⋯)) K V := Basis.mk ⋯ ⋯
i : ι
hi : v i ∈ hli.extend ⋯
ri : ↑(hli.extend ⋯) := ⟨v i, hi⟩
this : b ri = v i
⊢ ((b.constr K) 1) (v i) = 1

Tactic:
simp [← this]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
w : Dual R N ⊗[R] Dual R M
z : M ⊗[R] N
⊢ ((dualDistrib R N M) w) ((TensorProduct.comm R M N) z) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) w)) z

Tactic:
by
  induction w <;> induction z <;> simp_all [mul_comm]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteCoproducts C
inst✝¹ : HasCokernels C
inst✝ : IsNormalEpiCategory C
X Y : C
f g : X ⟶ Y
huv : pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g) = pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)
⊢ (coprod.inr ≫ coprod.desc (𝟙 Y) g) ≫ pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g) =
    g ≫ pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)

Tactic:
by rw [coprod.inr_desc]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (biprod.desc f (-g)) 0
⊢ (s.ι ≫ biprod.fst) ≫ f - (s.ι ≫ biprod.snd) ≫ g = 0

Tactic:
rw [Category.assoc, Category.assoc, ← comp_sub, sub_eq_add_neg, ← comp_neg, ←
            biprod.desc_eq, KernelFork.condition s]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Category.{v_3, u_3} E
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
inst✝ : HasZeroMorphisms E
S S₁ S₂ S₃ : ShortComplex C
e₁ : S₁.X₁ ≅ S₂.X₁
e₂ : S₁.X₂ ≅ S₂.X₂
e₃ : S₁.X₃ ≅ S₂.X₃
comm₁₂ : e₁.hom ≫ S₂.f = S₁.f ≫ e₂.hom
comm₂₃ : e₂.hom ≫ S₂.g = S₁.g ≫ e₃.hom
⊢ e₁.inv ≫ e₁.hom ≫ S₂.f = S₂.f

Tactic:
e₁.inv_hom_id_assoc

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Category.{v_3, u_3} E
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
inst✝ : HasZeroMorphisms E
S S₁ S₂ S₃ : ShortComplex C
e₁ : S₁.X₁ ≅ S₂.X₁
e₂ : S₁.X₂ ≅ S₂.X₂
e₃ : S₁.X₃ ≅ S₂.X₃
comm₁₂ : e₁.hom ≫ S₂.f = S₁.f ≫ e₂.hom
comm₂₃ : e₂.hom ≫ S₂.g = S₁.g ≫ e₃.hom
⊢ S₂.f = S₂.f
Module: Mathlib.Algebra.Category.Grp.EpiMono

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

Tactic:
simpa [g_apply_fromCoset, «h», tau, g_apply_infinity] using r

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
ψ₁ ψ₂ : LeftHomologyMapData φ h₁ h₂
⊢ ψ₁.φK = ψ₂.φK

Tactic:
← cancel_mono h₂.i,

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
ψ₁ ψ₂ : LeftHomologyMapData φ h₁ h₂
⊢ ψ₁.φK ≫ h₂.i = ψ₂.φK ≫ h₂.i
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 ≫ φ.τ₂) ⋯
⊢ h₁.f' ≫ φK = φ.τ₁ ≫ h₂.f'

Tactic:
← cancel_mono h₂.i,

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 ≫ φ.τ₂) ⋯
⊢ (h₁.f' ≫ φK) ≫ h₂.i = (φ.τ₁ ≫ h₂.f') ≫ h₂.i
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
inst✝ : S.HasHomology
this : h.iso = h.left.homologyIso.symm ≪≫ h.right.homologyIso
⊢ h.right.homologyIso = h.left.homologyIso ≪≫ h.iso

Tactic:
by
    rw [this, Iso.self_symm_id_assoc]

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
inst✝ : S.HasLeftHomology
⊢ S.op.pOpcycles ≫ S.opcyclesOpIso.hom = S.iCycles.op

Tactic:
by
  dsimp [opcyclesOpIso]
  rw [← S.leftHomologyData.op.p_comp_opcyclesIso_inv, assoc,
    Iso.inv_hom_id, comp_id]
  rfl

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

Goal state before:
pp: case refine_1
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 φ)
⊢ homologyMap φ ≫ S₂.homologyι ≫ inv (opcyclesMap φ) = S₁.homologyι

Tactic:
homologyι_naturality_assoc,

Goal state after:
case refine_1
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ι ≫ opcyclesMap φ ≫ inv (opcyclesMap φ) = S₁.homologyι
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ S₄ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
A : C
hf : S.f = 0
inst✝ : S.HasHomology
⊢ S.cycles ≅ S.homology

Tactic:
by
  have := S.isIso_homologyπ hf
  exact asIso S.homologyπ

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 : S₁ ⟶ S₂
⊢ 0 + a = a

Tactic:
ext <;> apply zero_add

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
S : ShortComplex C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasZeroMorphisms D
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst✝¹ : Epi π
inst✝ : Mono ι
⊢ S.toCycles ≫ S.homologyπ = 0

Tactic:
toCycles_comp_homologyπ

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
S : ShortComplex C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasZeroMorphisms D
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst✝¹ : Epi π
inst✝ : Mono ι
⊢ 0 = 0
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
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
inst✝² : S.HasHomology
inst✝¹ : F.PreservesLeftHomologyOf S
inst✝ : F.PreservesRightHomologyOf S
⊢ (S.mapHomologyIso' F).hom = (S.mapHomologyIso F).hom

Tactic:
rw [S.homologyData.left.mapHomologyIso_eq F, S.homologyData.right.mapHomologyIso'_eq F]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : HasZeroMorphisms C
inst✝⁴ : HasZeroMorphisms D
S : ShortComplex C
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
inst✝² : S.HasHomology
inst✝¹ : F.PreservesLeftHomologyOf S
inst✝ : F.PreservesRightHomologyOf S
⊢ ((S.homologyData.right.map F).homologyIso ≪≫ F.mapIso S.homologyData.right.homologyIso.symm).hom =
    ((S.homologyData.left.map F).homologyIso ≪≫ F.mapIso S.homologyData.left.homologyIso.symm).hom
Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic

Goal state before:
pp: case h₁
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
P Q : C
inst✝³ : HasZeroMorphisms C
inst✝² : HasBinaryBiproduct P Q
inst✝¹ : Injective P
inst✝ : Injective Q
X✝ Y✝ : C
g : X✝ ⟶ P ⊞ Q
f : X✝ ⟶ Y✝
mono : Mono f
⊢ (f ≫ biprod.lift (factorThru (g ≫ biprod.fst) f) (factorThru (g ≫ biprod.snd) f)) ≫ biprod.snd = g ≫ biprod.snd

Tactic:
simp only [Category.assoc, biprod.lift_snd, comp_factorThru]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : EnoughInjectives C
X : C
⊢ ∃ p, IsZero X → IsZero p.J

Tactic:
by_cases h : IsZero X

Goal state after:
case pos
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : EnoughInjectives C
X : C
h : IsZero X
⊢ ∃ p, IsZero X → IsZero p.J

case neg
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : EnoughInjectives C
X : C
h : ¬IsZero X
⊢ ∃ p, IsZero X → IsZero p.J
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
h : S.Exact
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : F.PreservesLeftHomologyOf S
inst✝ : (S.map F).HasHomology
⊢ (S.map F).Exact

Tactic:
by
  have := h.hasHomology
  rw [S.leftHomologyData.exact_iff, IsZero.iff_id_eq_zero] at h
  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: case mpr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : HasZeroObject C
hg : S.g = 0
⊢ Epi S.f → S.Exact

Tactic:
intro
    rw [(HomologyData.ofIsColimitCokernelCofork S hg _
      (CokernelCofork.IsColimit.ofEpiOfIsZero (CokernelCofork.ofπ (0 : S.X₂ ⟶ 0) comp_zero)
        inferInstance (isZero_zero C))).exact_iff]
    exact isZero_zero C

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
B A : C
X Y : Subobject B
f : A ⟶ B
inst✝ : Mono f
h₁ : X ≤ Y
h₂ : Y ≤ mk f
⊢ X.ofLE Y h₁ ≫ Y.ofLEMk f h₂ = X.ofLEMk f ⋯

Tactic:
simp only [ofLEMk, ofLE, ← Functor.map_comp_assoc underlying]
  congr 1

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

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 : C
f g : MonoOver X
h₁ h₂ : f ⟶ g
⊢ Over.Hom.left h₁.hom = Over.Hom.left h₂.hom

Tactic:
← cancel_mono g.arrow,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
f g : MonoOver X
h₁ h₂ : f ⟶ g
⊢ Over.Hom.left h₁.hom ≫ g.arrow = Over.Hom.left h₂.hom ≫ g.arrow
Module: Mathlib.CategoryTheory.Subobject.Basic

Goal state before:
pp: case g
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver Y
⊢ (MonoOver.pullback k).obj ((MonoOver.map h).obj a) ⟶ (MonoOver.map g).obj ((MonoOver.pullback f).obj a)

Tactic:
· refine MonoOver.homMk (pullback.lift (pullback.fst _ _)
      (PullbackCone.IsLimit.lift t (pullback.fst _ _ ≫ a.arrow) (pullback.snd _ _) _)
      (PullbackCone.IsLimit.lift_fst _ _ _ ?_).symm) ?_
    · rw [← pullback.condition, assoc]
      rfl
    · dsimp
      rw [pullback.lift_snd_assoc]
      apply PullbackCone.IsLimit.lift_snd

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

Goal state before:
pp: case refine_4
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
A : C
f g : Subobject A
x✝² : PullbackCone f.arrow g.arrow
x✝¹ : x✝².pt ⟶ underlying.obj (f ⊓ g)
h : x✝¹ ≫ (f ⊓ g).ofLE f ⋯ = x✝².fst
x✝ : x✝¹ ≫ (f ⊓ g).ofLE g ⋯ = x✝².snd
⊢ x✝¹ = (f ⊓ g).factorThru (x✝².fst ≫ f.arrow) ⋯

Tactic:
· ext
    simp [← h]

Goal state after:
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
E : L.LeftExtension F
E' : ?m.13
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
Y₁ Y₂ : D
φ : Y₁ ⟶ Y₂
X : CostructuredArrow L Y₁
⊢ (E.coconeAt Y₁).ι.app X ≫ (StructuredArrow.right E).map φ ≫ (h Y₂).desc (G.coconeAt Y₂) =
    (E.coconeAt Y₁).ι.app X ≫ (h Y₁).desc (G.coconeAt Y₁) ≫ (StructuredArrow.right G).map φ

Tactic:
by
        rw [(h Y₁).fac_assoc (coconeAt G Y₁) X]
        simpa using (h Y₂).fac (coconeAt G Y₂) ((CostructuredArrow.map φ).obj X)

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✝³ : L.Full
inst✝² : L.Faithful
F : C ⥤ H
inst✝¹ : L.HasPointwiseRightKanExtension F
inst✝ : ∀ (F : C ⥤ H), L.HasRightKanExtension F
⊢ IsIso ((L.ranAdjunction H).counit.app F)

Tactic:
by
  rw [ranAdjunction_counit]
  infer_instance

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
α : F ⟶ L ⋙ F'
α' : F ⟶ L ⋙ F''
comm : α ≫ L.whiskerLeft e.hom = α'
⊢ F''.IsLeftKanExtension α' → F'.IsLeftKanExtension α

Tactic:
intro
    refine isLeftKanExtension_of_iso e.symm α' α ?_
    rw [← comm, assoc, ← whiskerLeft_comp, Iso.symm_hom, e.hom_inv_id, whiskerLeft_id', comp_id]

Goal state after:
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 ⋙ L.pointwiseLeftKanExtension F).map f

Tactic:
simp only [comp_map,
      pointwiseLeftKanExtension_map, colimit.ι_desc, CostructuredArrow.map_mk]

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.obj X₁) ≫ L.map f))
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
inst✝ : Balanced C
hP : P.IsSeparating
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
Z✝ : C
g h : Z✝ ⟶ X
hgh : g ≫ f = h ≫ f
G : C
hG : P G
i : G ⟶ Z✝
t : G ⟶ X
ht : ∀ (y : G ⟶ X), (fun h' ↦ h' ≫ f = i ≫ g ≫ f) y → y = t
⊢ i ≫ g = i ≫ h

Tactic:
rw [ht (i ≫ g) (Category.assoc _ _ _), ht (i ≫ h) (hgh.symm ▸ Category.assoc _ _ _)]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
β : Type w
f : β → C
hf : (ObjectProperty.ofObj f).IsSeparating
c : Cofan f
hc : IsColimit c
⊢ IsSeparator c.pt

Tactic:
by
  rw [isSeparator_def]
  refine fun _ _ _ _ huv ↦ hf _ _ (fun _ h g ↦ ?_)
  obtain ⟨b⟩ := h
  classical simpa using c.inj b ≫= huv (hc.desc (Cofan.mk _ (Pi.single b g)))

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
I : Type v₁
inst✝ : SmallCategory I
F : I ⥤ C
c : Cocone (F ⋙ yoneda)
hc : IsColimit c
this :
  IsTerminal
    (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt))
⊢ IsTerminal (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ yoneda))

Tactic:
apply IsTerminal.isTerminalOfObj (overEquivPresheafCostructuredArrow c.pt).inverse

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
I : Type v₁
inst✝ : SmallCategory I
F : I ⥤ C
c : Cocone (F ⋙ yoneda)
hc : IsColimit c
this :
  IsTerminal
    (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt))
⊢ IsTerminal
    ((overEquivPresheafCostructuredArrow c.pt).inverse.obj
      (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ yoneda)))
Module: Mathlib.Algebra.Ring.NegOnePow

Goal state before:
pp: n : ℤ
⊢ n.negOnePow = 1 ↔ Even n

Tactic:
by
  constructor
  · intro h
    rw [← Int.not_odd_iff_even]
    intro h'
    simp only [negOnePow_odd _ h'] at h
    contradiction
  · exact negOnePow_even n

Goal state after:
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f g : α → β
c c₁ c₂ x✝ : α
inst✝ : AddGroup α
h : Periodic f c
x : α ⧸ AddSubgroup.zmultiples c
a b : α
h' : (QuotientAddGroup.leftRel (AddSubgroup.zmultiples c)) a b
⊢ f a = f b

Tactic:
rw [QuotientAddGroup.leftRel_apply] at h'
    obtain ⟨k, hk⟩ := h'
    exact (h.zsmul k _).symm.trans (congr_arg f (add_eq_of_eq_neg_add hk))

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Group

Goal state before:
pp: case inl
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
x dx y dy : α
h : dy < dx
hx : 0 < dx
h' : x < y
⊢ Nonempty ↑(Ico x (x + dx) \ Ico y (y + dy))

Tactic:
use x

Goal state after:
case property
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
x dx y dy : α
h : dy < dx
hx : 0 < dx
h' : x < y
⊢ x ∈ Ico x (x + dx) \ Ico y (y + dy)