mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
⊢ rightHomologyMap' (-φ) h₁ h₂ = -rightHomologyMap' φ h₁ h₂

Tactic:
simp only [γ.rightHomologyMap'_eq, γ.neg.rightHomologyMap'_eq, RightHomologyMapData.neg_φH]

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 φ₁ φ₂
h' : Homotopy φ₃ φ₄
⊢ (φ₁ - φ₃).τ₃ = h.h₃ - h'.h₃ + (h.h₂ - h'.h₂) ≫ S₂.g + (φ₂ - φ₄).τ₃

Tactic:
sub_τ₃,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h' : Homotopy φ₃ φ₄
⊢ φ₁.τ₃ - φ₃.τ₃ = h.h₃ - h'.h₃ + (h.h₂ - h'.h₂) ≫ S₂.g + (φ₂ - φ₄).τ₃
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 φ₁ φ₂
h' : Homotopy φ₃ φ₄
⊢ φ₁.τ₃ - φ₃.τ₃ = h.h₃ - h'.h₃ + (h.h₂ - h'.h₂) ≫ S₂.g + (φ₂ - φ₄).τ₃

Tactic:
sub_τ₃,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h' : Homotopy φ₃ φ₄
⊢ φ₁.τ₃ - φ₃.τ₃ = h.h₃ - h'.h₃ + (h.h₂ - h'.h₂) ≫ S₂.g + (φ₂.τ₃ - φ₄.τ₃)
Module: Mathlib.CategoryTheory.Abelian.Opposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (cokernel.π f).op ≫ f.op = 0

Tactic:
simp [← op_comp]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ ((cokernel.desc f (kernel.ι f.op).unop ⋯).op ≫ kernel.lift f.op (cokernel.π f).op ⋯) ≫ equalizer.ι f.op 0 =
    𝟙 (kernel f.op) ≫ equalizer.ι f.op 0

Tactic:
simp [← op_comp]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ f.op ≫ (kernel.ι f).op = 0

Tactic:
simp [← op_comp]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ coequalizer.π f.op 0 ≫ cokernel.desc f.op (kernel.ι f).op ⋯ ≫ (kernel.lift f (cokernel.π f.op).unop ⋯).op =
    coequalizer.π f.op 0 ≫ 𝟙 (cokernel f.op)

Tactic:
simp [← op_comp]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
A B : Cᵒᵖ
g : A ⟶ B
⊢ inv (𝟙 A) ≫ factorThruImage g = factorThruImage g

Tactic:
rw [IsIso.inv_id, Category.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₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
H₁ : S₁.RightHomologyData
H₂ : S₂.RightHomologyData
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
⊢ 0 ≫ H₂.ι = H₁.ι ≫ H₁.descQ (S₁.g ≫ h₂ ≫ H₂.p) ⋯

Tactic:
rw [H₁.ι_descQ_eq_zero_of_boundary (S₁.g ≫ h₂ ≫ H₂.p) (h₂ ≫ H₂.p) rfl, zero_comp]

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✝³ : Preadditive C
inst✝² : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
inst✝¹ : IsIso φ.τ₁
inst✝ : IsIso φ.τ₃
this✝ : Mono S₁.f
this : Mono S₂.f
⊢ IsIso φ.τ₂

Tactic:
have := h₁.epi_g

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
inst✝² : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
inst✝¹ : IsIso φ.τ₁
inst✝ : IsIso φ.τ₃
this✝¹ : Mono S₁.f
this✝ : Mono S₂.f
this : Epi S₁.g
⊢ IsIso φ.τ₂
Module: Mathlib.Algebra.Homology.ShortComplex.Ab

Goal state before:
pp: case mp
S : ShortComplex Ab
h : Function.Surjective ⇑S.abToCycles
x₂ : ↑S.X₂
hx₂ : (ConcreteCategory.hom S.g) x₂ = 0
x₁ : ↑S.X₁
hx₁ : S.abToCycles x₁ = ⟨x₂, hx₂⟩
⊢ ∃ x₁, (ConcreteCategory.hom S.f) x₁ = x₂

Tactic:
exact ⟨x₁, by simpa only [Subtype.ext_iff, abToCycles_apply_coe] using hx₁⟩

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Restrict

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
iC : C ⥤ C'
iD : D ⥤ D'
L' : C' ⥤ D'
R' : D' ⥤ C'
adj : L' ⊣ R'
hiC : iC.FullyFaithful
hiD : iD.FullyFaithful
L : C ⥤ D
R : D ⥤ C
comm1 : iC ⋙ L' ≅ L ⋙ iD
comm2 : iD ⋙ R' ≅ R ⋙ iC
X : C
Y' Y : D
f : L.obj X ⟶ Y'
g : Y' ⟶ Y
⊢ (Trans.trans
        (Trans.trans
          (Trans.trans (Trans.trans hiD.homEquiv ((comm1.symm.app X).homCongr (Iso.refl (iD.obj Y))))
            (adj.homEquiv (iC.obj X) (iD.obj Y)))
          ((Iso.refl (iC.obj X)).homCongr (comm2.app Y)))
        hiC.homEquiv.symm)
      (f ≫ g) =
    (Trans.trans
          (Trans.trans
            (Trans.trans (Trans.trans hiD.homEquiv ((comm1.symm.app X).homCongr (Iso.refl (iD.obj Y'))))
              (adj.homEquiv (iC.obj X) (iD.obj Y')))
            ((Iso.refl (iC.obj X)).homCongr (comm2.app Y')))
          hiC.homEquiv.symm)
        f ≫
      R.map g

Tactic:
apply hiC.map_injective

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
iC : C ⥤ C'
iD : D ⥤ D'
L' : C' ⥤ D'
R' : D' ⥤ C'
adj : L' ⊣ R'
hiC : iC.FullyFaithful
hiD : iD.FullyFaithful
L : C ⥤ D
R : D ⥤ C
comm1 : iC ⋙ L' ≅ L ⋙ iD
comm2 : iD ⋙ R' ≅ R ⋙ iC
X : C
Y' Y : D
f : L.obj X ⟶ Y'
g : Y' ⟶ Y
⊢ iC.map
      ((Trans.trans
          (Trans.trans
            (Trans.trans (Trans.trans hiD.homEquiv ((comm1.symm.app X).homCongr (Iso.refl (iD.obj Y))))
              (adj.homEquiv (iC.obj X) (iD.obj Y)))
            ((Iso.refl (iC.obj X)).homCongr (comm2.app Y)))
          hiC.homEquiv.symm)
        (f ≫ g)) =
    iC.map
      ((Trans.trans
            (Trans.trans
              (Trans.trans (Trans.trans hiD.homEquiv ((comm1.symm.app X).homCongr (Iso.refl (iD.obj Y'))))
                (adj.homEquiv (iC.obj X) (iD.obj Y')))
              ((Iso.refl (iC.obj X)).homCongr (comm2.app Y')))
            hiC.homEquiv.symm)
          f ≫
        R.map g)
Module: Mathlib.CategoryTheory.Adjunction.Restrict

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
iC : C ⥤ C'
iD : D ⥤ D'
L' : C' ⥤ D'
R' : D' ⥤ C'
adj : L' ⊣ R'
hiC : iC.FullyFaithful
hiD : iD.FullyFaithful
L : C ⥤ D
R : D ⥤ C
comm1 : iC ⋙ L' ≅ L ⋙ iD
comm2 : iD ⋙ R' ≅ R ⋙ iC
X : C
Y : D
f : L.obj X ⟶ Y
⊢ ((adj.restrictFullyFaithful hiC hiD comm1 comm2).homEquiv X Y) f =
    hiC.preimage (adj.unit.app (iC.obj X) ≫ R'.map (comm1.hom.app X) ≫ R'.map (iD.map f) ≫ comm2.hom.app Y)

Tactic:
apply hiC.map_injective

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
iC : C ⥤ C'
iD : D ⥤ D'
L' : C' ⥤ D'
R' : D' ⥤ C'
adj : L' ⊣ R'
hiC : iC.FullyFaithful
hiD : iD.FullyFaithful
L : C ⥤ D
R : D ⥤ C
comm1 : iC ⋙ L' ≅ L ⋙ iD
comm2 : iD ⋙ R' ≅ R ⋙ iC
X : C
Y : D
f : L.obj X ⟶ Y
⊢ iC.map (((adj.restrictFullyFaithful hiC hiD comm1 comm2).homEquiv X Y) f) =
    iC.map (hiC.preimage (adj.unit.app (iC.obj X) ≫ R'.map (comm1.hom.app X) ≫ R'.map (iD.map f) ≫ comm2.hom.app Y))
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
s : S.Splitting
⊢ s.r ≫ S.f = 𝟙 S.X₂ - S.g ≫ s.s

Tactic:
rw [← s.id, add_sub_cancel_right]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y : C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : Mono f
h : mk f = ⊥
⊢ f = 0

Tactic:
simpa [h, bot_factors_iff_zero] using mk_factors_self f

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

Goal state before:
pp: case insert.inr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
a✝¹ : I
s✝ : Finset I
a✝ : a✝¹ ∉ s✝
ih : ∀ i ∈ s✝, (P i).Factors (s✝.inf P).arrow
i✝ : I
m : i✝ ∈ s✝
⊢ (P i✝).Factors (P a✝¹ ⊓ s✝.inf P).arrow

Tactic:
← factorThru_arrow _ _ (inf_arrow_factors_right _ _)

Goal state after:
case insert.inr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
a✝¹ : I
s✝ : Finset I
a✝ : a✝¹ ∉ s✝
ih : ∀ i ∈ s✝, (P i).Factors (s✝.inf P).arrow
i✝ : I
m : i✝ ∈ s✝
⊢ (P i✝).Factors ((s✝.inf P).factorThru (P a✝¹ ⊓ s✝.inf P).arrow ⋯ ≫ (s✝.inf P).arrow)
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
⊢ prod.fst.op ≫
      { hom := (prod.lift coprod.inl.unop coprod.inr.unop).op, inv := coprod.desc prod.fst.op prod.snd.op,
          hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom =
    coprod.inl

Tactic:
← op_comp,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A B : C
inst✝ : HasBinaryProduct A B
⊢ (prod.lift coprod.inl.unop coprod.inr.unop ≫ prod.fst).op = coprod.inl
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
⊢ prod.snd.op ≫
      { hom := (prod.lift coprod.inl.unop coprod.inr.unop).op, inv := coprod.desc prod.fst.op prod.snd.op,
          hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom =
    coprod.inr

Tactic:
← op_comp,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A B : C
inst✝ : HasBinaryProduct A B
⊢ (prod.lift coprod.inl.unop coprod.inr.unop ≫ prod.snd).op = coprod.inr
Module: Mathlib.CategoryTheory.Abelian.Subobject

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
⊢ (kernelOrderHom X).comp (cokernelOrderHom X) = OrderHom.id

Tactic:
change (kernelOrderHom X).comp (cokernelOrderHom X) = _
    refine OrderHom.ext _ _ (funext (Subobject.ind _ ?_))
    intro A f hf
    dsimp only [OrderHom.comp_coe, Function.comp_apply, cokernelOrderHom_coe, Subobject.lift_mk,
      kernelOrderHom_coe, OrderHom.id_coe, id, unop_op, Quiver.Hom.unop_op]
    refine Subobject.mk_eq_mk_of_comm _ _ ⟨?_, ?_, ?_, ?_⟩ ?_
    · exact Abelian.monoLift f _ (kernel.condition (cokernel.π f))
    · exact kernel.lift _ _ (cokernel.condition f)
    · simp only [← cancel_mono (kernel.ι (cokernel.π f)), Category.assoc, image.fac, monoLift_comp,
        Category.id_comp]
    · simp only [← cancel_mono f, Category.assoc, monoLift_comp, image.fac, Category.id_comp]
    · simp only [monoLift_comp]

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

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✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits T
A P : StructuredArrow S T
⊢ ∀ ⦃B : StructuredArrow S T⦄ (f : P ⟶ A) (g : B ⟶ A) [inst : Mono f] [inst_1 : Mono g] (i : P ≅ B),
    i.hom ≫ g = f → Subobject.mk (Hom.right f) = Subobject.mk (Hom.right g)

Tactic:
Q

Goal state after:
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) [inst : Mono f] [inst_1 : Mono g] (i : P ≅ Q),
    i.hom ≫ g = f → Subobject.mk (Hom.right f) = Subobject.mk (Hom.right g)
Module: Mathlib.CategoryTheory.Subobject.Comma

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✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits T
A P : StructuredArrow S T
⊢ ∀ ⦃B : StructuredArrow S T⦄ (f : P ⟶ A) (g : B ⟶ A) [inst : Mono f] [inst_1 : Mono g],
    { 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) ↔
      Subobject.mk f ≤ Subobject.mk g

Tactic:
Q

Goal state after:
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) [inst : Mono f] [inst_1 : Mono g],
    { 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) ↔
      Subobject.mk f ≤ Subobject.mk g
Module: Mathlib.CategoryTheory.Subobject.Comma

Goal state before:
pp: case refine_3
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 : Subobject.mk f ≤ Subobject.mk g
⊢ { 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)

Tactic:
refine Subobject.mk_le_mk_of_comm (Subobject.ofMkLEMk _ _ h).right ?_
      exact congr_arg CommaMorphism.right (Subobject.ofMkLEMk_comp h)

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

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
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
⊢ ∀ ⦃B : (CostructuredArrow S T)ᵒᵖ⦄ (f : P ⟶ op A) (g : B ⟶ op A) [inst : Mono f] [inst_1 : Mono g] (i : P ≅ B),
    i.hom ≫ g = f → Subobject.mk f.unop.left.op = Subobject.mk g.unop.left.op

Tactic:
Q

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
⊢ ∀ (f : P ⟶ op A) (g : Q ⟶ op A) [inst : Mono f] [inst_1 : Mono g] (i : P ≅ Q),
    i.hom ≫ g = f → Subobject.mk f.unop.left.op = Subobject.mk g.unop.left.op
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 : Cotrident f
⊢ f j₁ ≫ t.π = f j₂ ≫ t.π

Tactic:
by
  rw [t.app_one, t.app_one]

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

Goal state before:
pp: case id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cotrident fun j ↦ F.map (line j)
j : WalkingParallelFamily J
⊢ F.map (Hom.id j) ≫ eqToHom ⋯ ≫ t.ι.app j =
    (eqToHom ⋯ ≫ t.ι.app j) ≫ ((Functor.const (WalkingParallelFamily J)).obj t.pt).map (Hom.id j)

Tactic:
simp [Cotrident.app_one t]

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

Goal state before:
pp: case line
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cotrident fun j ↦ F.map (line j)
a✝ : J
⊢ F.map (line a✝) ≫ eqToHom ⋯ ≫ t.ι.app one =
    (eqToHom ⋯ ≫ t.ι.app zero) ≫ ((Functor.const (WalkingParallelFamily J)).obj t.pt).map (line a✝)

Tactic:
simp [Cotrident.app_one t]

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

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
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
⊢ ∀ ⦃B : (CostructuredArrow S T)ᵒᵖ⦄ (f : P ⟶ op A) (g : B ⟶ op A) [inst : Mono f] [inst_1 : Mono g],
    { toFun := fun P ↦ ⟨projectQuotient P, ⋯⟩, invFun := fun P ↦ liftQuotient ↑P ⋯, left_inv := ⋯, right_inv := ⋯ }
          (Subobject.mk f) ≤
        { toFun := fun P ↦ ⟨projectQuotient P, ⋯⟩, invFun := fun P ↦ liftQuotient ↑P ⋯, left_inv := ⋯, right_inv := ⋯ }
          (Subobject.mk g) ↔
      Subobject.mk f ≤ Subobject.mk g

Tactic:
Q

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
⊢ ∀ (f : P ⟶ op A) (g : Q ⟶ op A) [inst : Mono f] [inst_1 : Mono g],
    { toFun := fun P ↦ ⟨projectQuotient P, ⋯⟩, invFun := fun P ↦ liftQuotient ↑P ⋯, left_inv := ⋯, right_inv := ⋯ }
          (Subobject.mk f) ≤
        { toFun := fun P ↦ ⟨projectQuotient P, ⋯⟩, invFun := fun P ↦ liftQuotient ↑P ⋯, left_inv := ⋯, right_inv := ⋯ }
          (Subobject.mk g) ↔
      Subobject.mk f ≤ Subobject.mk g
Module: Mathlib.Algebra.Category.Grp.AB

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
⊢ ∃ G, IsSeparator G

Tactic:
use AddCommGrpCat.of (ULift ℤ)

Goal state after:
case h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
⊢ IsSeparator (AddCommGrpCat.of (ULift.{u, 0} ℤ))
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: case mp
X Y : Type u
c : BinaryCofan X Y
h : IsColimit c
⊢ Injective ⇑(ConcreteCategory.hom c.inl) ∧
    Injective ⇑(ConcreteCategory.hom c.inr) ∧
      IsCompl (Set.range ⇑(ConcreteCategory.hom c.inl)) (Set.range ⇑(ConcreteCategory.hom c.inr))

Tactic:
← show _ = c.inl from
          h.comp_coconePointUniqueUpToIso_inv (binaryCoproductColimit X Y) ⟨WalkingPair.left⟩,

Goal state after:
case mp
X Y : Type u
c : BinaryCofan X Y
h : IsColimit c
⊢ Injective
      ⇑(ConcreteCategory.hom
          ((binaryCoproductCocone X Y).ι.app { as := left } ≫
            (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)) ∧
    Injective ⇑(ConcreteCategory.hom c.inr) ∧
      IsCompl
        (Set.range
          ⇑(ConcreteCategory.hom
              ((binaryCoproductCocone X Y).ι.app { as := left } ≫
                (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)))
        (Set.range ⇑(ConcreteCategory.hom c.inr))
Module: Mathlib.Algebra.Group.Nat.Range

Goal state before:
pp: a : ℕ
s : Finset ℕ
⊢ ∀ ⦃a_1 : ℕ⦄, a_1 < a → ¬∃ a_3 ∈ s, a + a_3 = a_1

Tactic:
rintro _ h ⟨l, -, rfl⟩

Goal state after:
a : ℕ
s : Finset ℕ
l : ℕ
h : a + l < a
⊢ False
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x ↦ x * p
a : ℕ
⊢ a ∈ image (fun x ↦ x * p) (range (p ^ n)) → a ∈ range (p ^ (n + 1))

Tactic:
by
        simp only [mem_image, mem_range, exists_imp]
        rintro b ⟨h, rfl⟩
        rw [Nat.pow_succ]
        exact (mul_lt_mul_iff_left₀ hp.pos).2 h

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIocDiv hp a (m • p + b) = m + toIocDiv hp a b

Tactic:
rw [add_comm, toIocDiv_add_zsmul, add_comm]

Goal state after:
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
α : Type u_1
inst✝ : TopologicalSpace X
hX : Nonempty X
f : Filter α
g : α → X
h : ¬∃ x, Tendsto g f (𝓝 x)
⊢ f.limUnder g = Classical.choice hX

Tactic:
Tendsto

Goal state after:
X : Type u
α : Type u_1
inst✝ : TopologicalSpace X
hX : Nonempty X
f : Filter α
g : α → X
h : ¬∃ x, map g f ≤ 𝓝 x
⊢ f.limUnder g = Classical.choice hX
Module: Mathlib.Topology.Continuous

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : X ≃ Y
⊢ Continuous[inst✝¹, inst✝] ⇑e.symm.symm ↔ Continuous[inst✝¹, inst✝] ⇑e

Tactic:
Equiv.symm_symm

Goal state after:
Module: Mathlib.Topology.Continuous

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous[inst✝¹, inst✝] f
t : Set Y
⊢ closure[inst✝¹] (f ⁻¹' t) ⊆ f ⁻¹' closure[inst✝] t

Tactic:
rw [← (isClosed_closure.preimage hf).closure_eq]
  exact closure_mono (preimage_mono subset_closure)

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
f : α → β
g : β → γ
t₁ : TopologicalSpace α
t₂ : TopologicalSpace γ
⊢ Continuous[coinduced f t₁, t₂] g ↔ Continuous[t₁, t₂] (g ∘ f)

Tactic:
by
  simp only [continuous_iff_coinduced_le, coinduced_compose]

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
f : α → β
a : α
l : Filter α
x✝ : TopologicalSpace β
⊢ Tendsto f l (𝓝 (f a)) ↔ map f l ≤ (fun t ↦ 𝓝 (f a)) x✝

Tactic:
Tendsto

Goal state after:
α : Type u
β : Type v
f : α → β
a : α
l : Filter α
x✝ : TopologicalSpace β
⊢ map f l ≤ 𝓝 (f a) ↔ map f l ≤ (fun t ↦ 𝓝 (f a)) x✝
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ IsClosedMap f ↔ ∀ {s : Set X}, kernImage f (interior s) ⊆ interior (kernImage f s)

Tactic:
by
  rw [isClosedMap_iff_closure_image, compl_surjective.forall]
  simp [kernImage_eq_compl]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
hf : ∀ (i : ι), DenseRange (f i)
⊢ DenseRange (Pi.map f)

Tactic:
rw [DenseRange, Set.range_piMap]

Goal state after:
ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
hf : ∀ (i : ι), DenseRange (f i)
⊢ Dense (univ.pi fun i ↦ range (f i))
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
g : β → γ
hg : IsInducing g
s : Set α
⊢ ContinuousOn f s ↔ ContinuousOn (g ∘ f) s

Tactic:
by
  simp_rw [ContinuousOn, hg.continuousWithinAt_iff]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case inl
ι : Type u_2
inst✝¹ : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst✝ : (i : ι) → TopologicalSpace (X i)
h : ∀ (i : ι), IsSeparable (s i)
he : univ.pi s = ∅
⊢ IsSeparable ∅

Tactic:
exact countable_empty.isSeparable

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case inr
ι : Type u_2
inst✝¹ : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst✝ : (i : ι) → TopologicalSpace (X i)
h : ∀ (i : ι), IsSeparable (s i)
f₀ : (i : ι) → X i
⊢ IsSeparable (univ.pi s)

Tactic:
· choose c c_count hc using h
    have := fun i ↦ (c_count i).to_subtype
    set g : (I : Finset ι) × ((i : I) → c i) → (i : ι) → X i := fun ⟨I, f⟩ i ↦
      if hi : i ∈ I then f ⟨i, hi⟩ else f₀ i
    refine ⟨range g, countable_range g, fun f hf ↦ mem_closure_iff.2 fun o ho hfo ↦ ?_⟩
    rcases isOpen_pi_iff.1 ho f hfo with ⟨I, u, huo, hI⟩
    rsuffices ⟨f, hf⟩ : ∃ f : (i : I) → c i, g ⟨I, f⟩ ∈ Set.pi I u
    · exact ⟨g ⟨I, f⟩, hI hf, mem_range_self (f := g) ⟨I, f⟩⟩
    suffices H : ∀ i ∈ I, (u i ∩ c i).Nonempty by
      choose f hfu hfc using H
      refine ⟨fun i ↦ ⟨f i i.2, hfc i i.2⟩, fun i (hi : i ∈ I) ↦ ?_⟩
      simpa only [g, dif_pos hi] using hfu i hi
    intro i hi
    exact mem_closure_iff.1 (hc i <| hf _ trivial) _ (huo i hi).1 (huo i hi).2

Goal state after: