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

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
W : C
ι : W ⟶ X
q : IsSplitEqualizer f g ι
F : C ⥤ D
⊢ F.map (q.leftRetraction ≫ ι) = F.map q.leftRetraction ≫ F.map ι

Tactic:
F.map_comp

Goal state after:
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
W : C
ι : W ⟶ X
q : IsSplitEqualizer f g ι
F : C ⥤ D
⊢ F.map q.leftRetraction ≫ F.map ι = F.map q.leftRetraction ≫ F.map ι
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:
by
  rw [← Category.assoc, map_π_preserves_coequalizer_inv, coequalizer.π_desc]

Goal state after:
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:
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
inst✝ : FiniteDimensional K V
Φ : Subspace K (Dual K V)
⊢ finrank K ↥(dualCoannihilator Φ) = finrank K ↥(dualAnnihilator Φ)

Tactic:
rw [Submodule.dualCoannihilator, ← Module.evalEquiv_toLinearMap]

Goal state after:
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
Φ : Subspace K (Dual K V)
⊢ finrank K ↥(comap (↑(evalEquiv K V)) (dualAnnihilator Φ)) = finrank K ↥(dualAnnihilator Φ)
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
W : Submodule R M
φ : Dual R M
⊢ (∃ y, W.mkQ.dualMap y = φ) → φ ∈ W.dualAnnihilator

Tactic:
rintro ⟨ψ, rfl⟩

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
W : Submodule R M
ψ : Dual R (M ⧸ W)
⊢ W.mkQ.dualMap ψ ∈ W.dualAnnihilator
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 := ∐ K.obj
Q : C := ∐ fun f ↦ K.obj f.fst.1
s : Q ⟶ P := Sigma.desc fun f ↦ K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f ↦ colimit.ι (Discrete.functor K.obj) { as := f.fst.1 }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
⊢ PreservesColimit K G

Tactic:
apply preservesColimit_of_preserves_colimit_cocone
        (buildIsColimit s t (by simp [P, s]) (by simp [P, t]) (colimit.isColimit _)
          (colimit.isColimit _) (colimit.isColimit _))

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✝⁵ : 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 (G.mapCocone (buildColimit s t ⋯ ⋯ (colimit.cocone (parallelPair s t))))
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: ι : Type u_1
α : Type u_2
F : Type u_3
inst✝¹ : Finite ι
inst✝ : Field F
f : ι → α → F
⊢ span F (Set.range (flip f)) = ⊤ ↔ LinearIndependent F f

Tactic:
rw [linearIndependent_iff_ker, ← Submodule.map_eq_top_iff (e := Finsupp.llift F F F ι),
    ← Subspace.dualCoannihilator_dualAnnihilator_eq (W := map ..), dualAnnihilator_eq_top_iff]
  congr!
  rw [SetLike.ext'_iff, map_span, Submodule.coe_dualCoannihilator_span, ← Set.range_comp]
  ext
  simp [funext_iff, Finsupp.linearCombination, Finsupp.sum, Finset.sum_apply, flip]

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 Z : C
a : X ⟶ Y
b : X ⟶ Z
inst✝¹ : Epi a
inst✝ : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
a' : (CokernelCofork.ofπ a hfa).pt ⟶ cokernel (coprod.desc f g)
ha' : Cofork.π (CokernelCofork.ofπ a hfa) ≫ a' = cokernel.π (coprod.desc f g)
b' : (CokernelCofork.ofπ b hgb).pt ⟶ cokernel (coprod.desc f g)
hb' : Cofork.π (CokernelCofork.ofπ b hgb) ≫ b' = cokernel.π (coprod.desc f g)
s : PushoutCocone a b
⊢ g ≫ b ≫ s.inr = 0 ≫ s.inr

Tactic:
by rw [← Category.assoc, eq_whisker hgb]

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
s : Cofork (biprod.lift f (-g)) 0
⊢ Cofork.π (biproductToPushoutCofork f g) ≫ pushout.desc (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯ = s.π

Tactic:
apply biprod.hom_ext' <;> simp

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
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi f
R : C
e : Y ⟶ R
h : pullback.snd f g ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc 0 e
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this✝¹ : IsColimit (CokernelCofork.ofπ (biprod.desc f (-g)) ⋯)
d : Z ⟶ R
hd : biprod.desc f (-g) ≫ d = biprod.desc 0 e
this✝ : f ≫ d = 0
this : d = 0
⊢ biprod.inr ≫ biprod.desc f (-g) ≫ d = biprod.inr ≫ biprod.desc f (-g) ≫ 0

Tactic:
rw [this]

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
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi g
R : C
e : X ⟶ R
h : pullback.fst f g ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc e 0
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this✝¹ : IsColimit (CokernelCofork.ofπ (biprod.desc f (-g)) ⋯)
d : Z ⟶ R
hd : biprod.desc f (-g) ≫ d = biprod.desc e 0
this✝ : (-g) ≫ d = 0
this : d = 0
⊢ biprod.inl ≫ biprod.desc f (-g) ≫ d = biprod.inl ≫ biprod.desc f (-g) ≫ 0

Tactic:
rw [this]

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

Goal state before:
pp: case refine_1.infinity
A B : GrpCat
f : A ⟶ B
a : ↑A
⊢ (h ((ConcreteCategory.hom f) a)) ∞ = (g ((ConcreteCategory.hom f) a)) ∞

Tactic:
rw [g_apply_infinity, h_apply_infinity f (f a) ⟨_, rfl⟩]

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
⊢ (d ≫ biprod.lift f (-g)) ≫ biprod.snd = (0 ≫ biprod.lift f (-g)) ≫ biprod.snd

Tactic:
rw [this]

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

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
a : ↑A
x✝ : X'
this : (ConcreteCategory.hom f) a ∈ {b | h b = g b}
⊢ (g ((Hom.hom f) a)) x✝ = (h ((Hom.hom f) a)) x✝

Tactic:
rw [this]

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 g
R : C
e : R ⟶ Y
h : e ≫ pushout.inl f g = 0
u : R ⟶ Y ⊞ Z := biprod.lift e 0
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 e 0
this✝ : d ≫ (-g) = 0
this : d = 0
⊢ (d ≫ biprod.lift f (-g)) ≫ biprod.fst = (0 ≫ biprod.lift f (-g)) ≫ biprod.fst

Tactic:
rw [this]

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
g₁ : X ⟶ W
inst✝¹ : Epi g₁
g₂ : W ⟶ Z
inst✝ : Mono g₂
hg : g₁ ≫ g₂ = g
f' : W ⟶ Y
hf : g₁ ≫ f' = f
t : PushoutCocone f g
ht : IsColimit t
⊢ Mono t.inl

Tactic:
apply mono_inl_of_isColimit _ _ (PushoutCocone.isColimitOfFactors _ _ _ _ _ hf hg t ht)

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₂ S₃ S₄ : ShortComplex C
inst✝³ : S₁.HasHomology
inst✝² : S₂.HasHomology
inst✝¹ : S₃.HasHomology
inst✝ : S₄.HasHomology
φ : S₁ ⟶ S₂
φ' : S₃ ⟶ S₄
e : Arrow.mk φ ≅ Arrow.mk φ'
hφ : QuasiIso φ
α : S₃ ⟶ S₁ := Arrow.Hom.left e.inv
β : S₂ ⟶ S₄ := Arrow.Hom.right e.hom
this : φ' = α ≫ φ ≫ β
⊢ QuasiIso φ'

Tactic:
rw [this]

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroMorphisms C
S₁ S₂ S₃ S₄ : ShortComplex C
inst✝³ : S₁.HasHomology
inst✝² : S₂.HasHomology
inst✝¹ : S₃.HasHomology
inst✝ : S₄.HasHomology
φ : S₁ ⟶ S₂
φ' : S₃ ⟶ S₄
e : Arrow.mk φ ≅ Arrow.mk φ'
hφ : QuasiIso φ
α : S₃ ⟶ S₁ := Arrow.Hom.left e.inv
β : S₂ ⟶ S₄ := Arrow.Hom.right e.hom
this : φ' = α ≫ φ ≫ β
⊢ QuasiIso (α ≫ φ ≫ β)
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
hf : S.f = 0
c : KernelFork S.g
hc : IsLimit c
⊢ (ofIsLimitKernelFork S hf c hc).f' = 0

Tactic:
by
  rw [← cancel_mono (ofIsLimitKernelFork S hf c hc).i, f'_i, hf, zero_comp]

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₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
γ' : HomologyMapData φ S₁.homologyData S₂.homologyData
⊢ leftHomologyMap' φ S₁.homologyData.left S₂.homologyData.left =
    ((S₁.homologyData.iso.hom ≫ rightHomologyMap' (𝟙 S₁) S₁.homologyData.right S₁.rightHomologyData) ≫
        rightHomologyMap' (𝟙 S₁) S₁.rightHomologyData h₁) ≫
      γ.φH ≫
        rightHomologyMap' (𝟙 S₂) h₂ S₂.rightHomologyData ≫
          rightHomologyMap' (𝟙 S₂) S₂.rightHomologyData S₂.homologyData.right ≫ S₂.homologyData.iso.inv

Tactic:
simp only [← γ.rightHomologyMap'_eq, assoc, ← rightHomologyMap'_comp_assoc,
    id_comp, comp_id, γ'.left.leftHomologyMap'_eq, γ'.right.rightHomologyMap'_eq, ← γ'.comm_assoc,
    Iso.hom_inv_id]

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
inst✝ : S.HasLeftHomology
⊢ h.cyclesIso.inv ≫ S.iCycles = h.i

Tactic:
simp only [← h.cyclesIso_hom_comp_i, Iso.inv_hom_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.HasRightHomology
⊢ S.rightHomologyData.op.cyclesIso.inv ≫ S.op.iCycles = S.pOpcycles.op

Tactic:
rw [← S.rightHomologyData.op.cyclesIso_hom_comp_i, Iso.inv_hom_id_assoc]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasRightHomology
⊢ S.rightHomologyData.op.i = S.pOpcycles.op
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₂
hr₁ : S₁.RightHomologyData
hr₂ : S₂.RightHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : hr₁.IsPreservedBy F
inst✝ : hr₂.IsPreservedBy F
⊢ F.map (opcyclesMap' φ hr₁ hr₂) = opcyclesMap' (F.mapShortComplex.map φ) (hr₁.map F) (hr₂.map F)

Tactic:
have γ : ShortComplex.RightHomologyMapData φ hr₁ hr₂ := default

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₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hr₁ : S₁.RightHomologyData
hr₂ : S₂.RightHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : hr₁.IsPreservedBy F
inst✝ : hr₂.IsPreservedBy F
γ : RightHomologyMapData φ hr₁ hr₂
⊢ F.map (opcyclesMap' φ hr₁ hr₂) = opcyclesMap' (F.mapShortComplex.map φ) (hr₁.map F) (hr₂.map F)
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₂
hr₁ : S₁.RightHomologyData
hr₂ : S₂.RightHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : hr₁.IsPreservedBy F
inst✝ : hr₂.IsPreservedBy F
⊢ F.map (rightHomologyMap' φ hr₁ hr₂) = rightHomologyMap' (F.mapShortComplex.map φ) (hr₁.map F) (hr₂.map F)

Tactic:
have γ : ShortComplex.RightHomologyMapData φ hr₁ hr₂ := default

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₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hr₁ : S₁.RightHomologyData
hr₂ : S₂.RightHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : hr₁.IsPreservedBy F
inst✝ : hr₂.IsPreservedBy F
γ : RightHomologyMapData φ hr₁ hr₂
⊢ F.map (rightHomologyMap' φ hr₁ hr₂) = rightHomologyMap' (F.mapShortComplex.map φ) (hr₁.map F) (hr₂.map F)
Module: Mathlib.CategoryTheory.Subobject.Basic

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

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

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P Q : MonoOver X
f : P ⟶ Q
⊢ IsIso f ↔ Subobject.mk P.obj.hom = Subobject.mk Q.obj.hom

Tactic:
rw [isIso_iff_isIso_hom_left, isIso_hom_left_iff_subobjectMk_eq]

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✝ : Balanced C
S : ShortComplex C
hS : S.Exact
r : S.X₂ ⟶ S.X₁
f_r : S.f ≫ r = 𝟙 S.X₁
hg : Epi S.g
⊢ S.f ≫ (𝟙 S.X₂ - r ≫ S.f) = 0

Tactic:
simp [reassoc_of% f_r]

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

Goal state before:
pp: case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
inst✝ : HasBinaryCoproducts C
A : C
f g h : MonoOver A
k₁ : f ⟶ h
k₂ : g ⟶ h
⊢ coprod.inr ≫ coprod.desc (Over.Hom.left k₁.hom) (Over.Hom.left k₂.hom) ≫ h.arrow =
    coprod.inr ≫ ((Functor.uncurry.obj Over.coprod).obj (((forget A).prod (forget A)).obj (f, g))).hom

Tactic:
simp [w k₂]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
α : Type w
inst✝² : HasFiniteCoproducts C
inst✝¹ : HasColimitsOfShape (Finset (Discrete α)) C
inst✝ : HasColimitsOfShape (Discrete α) C
F : Discrete α ⥤ C
J : Finset (Discrete α)
j : ↥J
⊢ Sigma.ι (fun x ↦ F.obj ↑x) j ≫
      colimit.ι (liftToFinsetObj F) J ≫ (colimit.isoColimitCocone (liftToFinsetColimitCocone F)).inv =
    colimit.ι F ↑j

Tactic:
simp [colimit.isoColimitCocone, IsColimit.coconePointUniqueUpToIso]

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
G : D ⥤ H
f : F₁ ⟶ F₂
α : F₂ ⟶ ((whiskeringLeft C D H).obj L).obj G
⊢ L.lanUnit.app F₁ ≫ L.whiskerLeft (((L.lan.obj F₁).homEquivOfIsLeftKanExtension (L.lanUnit.app F₁) G).symm (f ≫ α)) =
    L.lanUnit.app F₁ ≫
      L.whiskerLeft (L.lan.map f ≫ ((L.lan.obj F₂).homEquivOfIsLeftKanExtension (L.lanUnit.app F₂) G).symm α)

Tactic:
by
          ext X
          dsimp [homEquivOfIsLeftKanExtension]
          rw [descOfIsLeftKanExtension_fac_app, NatTrans.comp_app, ← assoc]
          have h := congr_app (L.lanUnit.naturality f) X
          dsimp at h ⊢
          rw [← h, assoc, descOfIsLeftKanExtension_fac_app]

Goal state after:
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
P : ObjectProperty C
inst✝¹ : ObjectProperty.Small.{v₁, v₁, u₁} P
inst✝ : LocallySmall.{v₁, v₂, u₂} D
this : P.inverseImage (proj S T) = ObjectProperty.ofObj fun f ↦ mk f.snd
⊢ ObjectProperty.Small.{v₁, v₁, max u₁ v₂} (P.inverseImage (proj S T))

Tactic:
rw [this]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : D
T : C ⥤ D
P : ObjectProperty C
inst✝¹ : ObjectProperty.Small.{v₁, v₁, u₁} P
inst✝ : LocallySmall.{v₁, v₂, u₂} D
this : P.inverseImage (proj S T) = ObjectProperty.ofObj fun f ↦ mk f.snd
⊢ ObjectProperty.Small.{v₁, v₁, max u₁ v₂} (ObjectProperty.ofObj fun f ↦ mk f.snd)
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 : C ⥤ D
T : D
P : ObjectProperty C
inst✝¹ : ObjectProperty.Small.{v₁, v₁, u₁} P
inst✝ : LocallySmall.{v₁, v₂, u₂} D
this : P.inverseImage (proj S T) = ObjectProperty.ofObj fun f ↦ mk f.snd
⊢ ObjectProperty.Small.{v₁, v₁, max u₁ v₂} (P.inverseImage (proj S T))

Tactic:
rw [this]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
P : ObjectProperty C
inst✝¹ : ObjectProperty.Small.{v₁, v₁, u₁} P
inst✝ : LocallySmall.{v₁, v₂, u₂} D
this : P.inverseImage (proj S T) = ObjectProperty.ofObj fun f ↦ mk f.snd
⊢ ObjectProperty.Small.{v₁, v₁, max u₁ v₂} (ObjectProperty.ofObj fun f ↦ mk f.snd)
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)
j₁ j₂ : J
t : Trident f
⊢ t.ι ≫ f j₁ = t.ι ≫ f j₂

Tactic:
t.app_zero,

Goal state after:
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
j₁ j₂ : J
t : Trident f
⊢ t.π.app one = t.ι ≫ f j₂
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
G : C
inst✝ : ∀ (A : C), HasProduct fun x ↦ G
⊢ IsCoseparator G ↔ ∀ (A : C), Mono (Pi.lift fun f ↦ f)

Tactic:
by
  rw [isCoseparator_def]
  refine ⟨fun h A => ⟨fun u v huv => h _ _ fun i => ?_⟩, fun h X Y f g hh => ?_⟩
  · simpa using huv =≫ Pi.π _ i
  · have := h Y
    refine (cancel_mono (Pi.lift fun f : Y ⟶ G => f)).1 (limit.hom_ext fun j => ?_)
    simpa using hh j.as

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

Goal state before:
pp: case e'_2.mp.inl
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
⊢ ∃ i, WalkingPair.rec G H i = G

pp: case e'_2.mp.inr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
⊢ ∃ i, WalkingPair.rec G H i = H

Tactic:
exacts [⟨.left, rfl⟩, ⟨.right, rfl⟩]

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

Goal state before:
pp: case e'_2.mp.inl
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryProduct G H
⊢ ∃ i, WalkingPair.rec G H i = G

pp: case e'_2.mp.inr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryProduct G H
⊢ ∃ i, WalkingPair.rec G H i = H

Tactic:
exacts [⟨.left, rfl⟩, ⟨.right, rfl⟩]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C : Type u
F : C → Type v
X Y : Type u
f : X ⟶ Y
inst✝ : Mono f
⊢ Set.range ⇑(ConcreteCategory.hom (BinaryCofan.mk f (↾Subtype.val)).inr) =
    (Set.range ⇑(ConcreteCategory.hom (BinaryCofan.mk f (↾Subtype.val)).inl))ᶜ

Tactic:
exact Subtype.range_val

Goal state after:
Module: Mathlib.Data.ZMod.IntUnitsPower

Goal state before:
pp: z₁ z₂ : ZMod 2
au : Additive ℤˣ
⊢ Additive.toMul ((z₁ * z₂) • au) = Additive.toMul (z₁ • z₂ • au)

Tactic:
dsimp only [ZMod.smul_units_def, toMul_nsmul]
    rw [← pow_mul, ZMod.val_mul, ← Int.units_pow_eq_pow_mod_two, mul_comm]

Goal state after:
Module: Mathlib.GroupTheory.Divisible

Goal state before:
pp: A : Type u_1
α : Type u_2
inst✝² : Monoid A
inst✝¹ : Pow A α
inst✝ : Zero α
H : ∀ {n : α}, n ≠ 0 → Function.Surjective fun a ↦ a ^ n
n✝ : α
a : A
hn : n✝ ≠ 0
⊢ (if x : n✝ = 0 then 1 else ⋯.choose) ^ n✝ = a

Tactic:
dsimp only
    rw [dif_neg hn]
    exact (H hn a).choose_spec

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddGroup α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
k : ℤ
⊢ -f x = -1 • f x

Tactic:
neg_zsmul,

Goal state after:
case inr
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddGroup α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
k : ℤ
⊢ -f x = -(1 • f x)
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
x : ↥(supExtensionOfMaxSingleton i f y)
r : R
a : N
ha : a ∈ (extensionOfMax i f).domain
eq1 : ↑(fst i x) + snd i x • y - (a + r • y) = 0
⊢ ↑(fst i x) - a = (r - snd i x) • y

Tactic:
← sub_sub_sub_eq,

Goal state after:
R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
x : ↥(supExtensionOfMaxSingleton i f y)
r : R
a : N
ha : a ∈ (extensionOfMax i f).domain
eq1 : ↑(fst i x) - a - (r • y - snd i x • y) = 0
⊢ ↑(fst i x) - a = (r - snd i x) • y
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: a k n : ℕ
a_ne_zero : a ≠ 0
| #({x ∈ Ico k (k + n) | a.Coprime x})

Tactic:
rw [← Nat.mod_add_div n a]

Goal state after:
a k n : ℕ
a_ne_zero : a ≠ 0
| #({x ∈ Ico k (k + (n % a + a * (n / a))) | a.Coprime x})