mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
R : C
g : Q ⟶ R
h : f ≫ g = 0
⊢ Abelian.factorThruImage f ≫ image.ι f ≫ g = 0

Tactic:
by simp [h]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
R : C
g : Q ⟶ R
h : f ≫ g = 0
⊢ (f ≫ coimage.π g) ≫ Abelian.factorThruCoimage g = 0

Tactic:
by simp [h]

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
F : C ⥤ D
inst✝ : F.PreservesZeroMorphisms
⊢ F.map S.f ≫ F.map S.g = 0

Tactic:
rw [← F.map_comp, S.zero, F.map_zero]

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

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

Tactic:
by
  change ((τ).symm.trans (g x)).trans τ _ = _
  simp only [tau, Equiv.coe_trans, Function.comp_apply]
  rw [Equiv.symm_swap,
    @Equiv.swap_apply_of_ne_of_ne X' _ (fromCoset ⟨f.hom.range, 1, one_leftCoset _⟩) ∞
      (fromCoset ⟨b • ↑f.hom.range, b, rfl⟩) (fromCoset_ne_of_nin_range _ hb) (by simp)]
  simp only [g_apply_fromCoset, leftCoset_assoc]
  refine Equiv.swap_apply_of_ne_of_ne (fromCoset_ne_of_nin_range _ fun r => hb ?_) (by simp)
  convert! Subgroup.mul_mem _ (Subgroup.inv_mem _ hx) r
  rw [← mul_assoc, inv_mul_cancel, one_mul]

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

Goal state before:
pp: case refine_1.fromCoset
A B : GrpCat
f : A ⟶ B
a : ↑A
y : ↑B
⊢ (h ((ConcreteCategory.hom f) a)) (fromCoset ⟨(fun x ↦ x • ↑(Hom.hom f).range) y, ⋯⟩) =
    (g ((ConcreteCategory.hom f) a)) (fromCoset ⟨(fun x ↦ x • ↑(Hom.hom f).range) y, ⋯⟩)

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_fromCoset]
      by_cases m : y ∈ f.hom.range
      · rw [h_apply_fromCoset' _ _ _ m, fromCoset_eq_of_mem_range _ m]
        change fromCoset _ = fromCoset ⟨f a • (y • _), _⟩
        simp only [← fromCoset_eq_of_mem_range _ (Subgroup.mul_mem _ ⟨a, rfl⟩ m), smul_smul]
      · rw [h_apply_fromCoset_nin_range f (f a) ⟨_, rfl⟩ _ m]
        simp only [leftCoset_assoc]

Goal state after:
case refine_1.infinity
A B : GrpCat
f : A ⟶ B
a : ↑A
⊢ (h ((ConcreteCategory.hom f) a)) ∞ = (g ((ConcreteCategory.hom f) a)) ∞
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
⊢ f ≫ ofHom g = f ≫ ofHom h

Tactic:
ext a

Goal state after:
A B : GrpCat
f : A ⟶ B
a : ↑A
x✝ : X'
⊢ ((Hom.hom (f ≫ ofHom g)) a) x✝ = ((Hom.hom (f ≫ ofHom h)) a) x✝
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₁ S₂ : ShortComplex C
h : S.LeftHomologyData
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : h.IsPreservedBy F
this✝ : PreservesLimit (parallelPair S.g 0) F
this : PreservesColimit (parallelPair h.f' 0) F
⊢ F.map h.i ≫ F.map S.g = 0

Tactic:
rw [← F.map_comp, h.wi, F.map_zero]

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 ι
⊢ ι ≫ hcc.desc (CokernelCofork.ofπ S.g ⋯) = 0

Tactic:
g'_eq,

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 ι
⊢ ι ≫ (S.isoOpcyclesOfIsColimit hcc).hom ≫ S.fromOpcycles = 0
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₃ ⟶ S₁
⊢ ψ.τ₂ ≫ S₁.g ≫ h.h₂ + ψ.τ₂ ≫ h.h₁ ≫ S₂.f + ψ.τ₂ ≫ φ₂.τ₂ = S₃.g ≫ ψ.τ₃ ≫ h.h₂ + ψ.τ₂ ≫ h.h₁ ≫ S₂.f + ψ.τ₂ ≫ φ₂.τ₂

Tactic:
ψ.comm₂₃_assoc

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 φ₁ φ₂
ψ : S₃ ⟶ S₁
⊢ S₃.g ≫ ψ.τ₃ ≫ h.h₂ + ψ.τ₂ ≫ h.h₁ ≫ S₂.f + ψ.τ₂ ≫ φ₂.τ₂ = S₃.g ≫ ψ.τ₃ ≫ h.h₂ + ψ.τ₂ ≫ h.h₁ ≫ S₂.f + ψ.τ₂ ≫ φ₂.τ₂
Module: Mathlib.Algebra.Homology.ShortComplex.Abelian

Goal state before:
pp: case refine_2
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 ι
⊢ (Cone.postcompose
          (parallelPair.ext (S.isoOpcyclesOfIsColimit hcc)
              (Iso.refl
                ((parallelPair ((hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) ⋯)).desc (CokernelCofork.ofπ S.g ⋯))
                      0).obj
                  WalkingParallelPair.one))
              ⋯ ⋯).hom).obj
      (KernelFork.ofι ι ⋯) ≅
    KernelFork.ofι S.homologyι ⋯

Tactic:
· exact Fork.ext (isoHomology S hkf hcc fac) (by simp [Fork.ι])

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✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
this : S.HasHomology
eq : h.left.π ≫ h.iso.hom ≫ h.right.ι = 0
⊢ IsZero h.left.H

Tactic:
simp only [IsZero.iff_id_eq_zero, ← cancel_mono h.iso.hom, id_comp, ← cancel_mono h.right.ι,
      ← cancel_epi h.left.π, eq, zero_comp, comp_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 : S.Exact
hg : S.g = 0
this✝¹ : S.HasHomology
this✝ : Mono S.fromOpcycles
this : S.pOpcycles = 0
⊢ Epi S.f

Tactic:
apply Preadditive.epi_of_cancel_zero

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hg : S.g = 0
this✝¹ : S.HasHomology
this✝ : Mono S.fromOpcycles
this : S.pOpcycles = 0
⊢ ∀ {R : C} (g : S.X₂ ⟶ R), S.f ≫ g = 0 → g = 0
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 S₁ S₂ : ShortComplex C
s : S₁.Splitting
e : S₁ ≅ S₂
eq : e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂ = e.inv.τ₂ ≫ 𝟙 S₁.X₂ ≫ e.hom.τ₂
⊢ (e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁) ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ = 𝟙 S₂.X₂

Tactic:
rw [id_comp, ← comp_τ₂, e.inv_hom_id, id_τ₂] at eq

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✝ : Preadditive D
S S₁ S₂ : ShortComplex C
s : S₁.Splitting
e : S₁ ≅ S₂
eq : e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂ = 𝟙 S₂.X₂
⊢ (e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁) ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ = 𝟙 S₂.X₂
Module: Mathlib.CategoryTheory.Subobject.Limits

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
⊢ equalizerSubobject f f = ⊤

Tactic:
by
  apply mk_eq_top_of_isIso

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

Goal state before:
pp: case hf₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
⊢ S₁.g.op = 0

Tactic:
rw [hg₁, op_zero]

Goal state after:
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✝ : HasPullbacks C
A : C
X✝ Y✝ : MonoOver A
k : X✝ ⟶ Y✝
g : MonoOver A
⊢ pullback.snd ((forget A).obj g).hom X✝.arrow ≫ X✝.arrow =
    pullback.snd ((forget A).obj g).hom X✝.arrow ≫ Over.Hom.left k.hom ≫ Y✝.arrow

Tactic:
w k

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
A : C
X✝ Y✝ : MonoOver A
k : X✝ ⟶ Y✝
g : MonoOver A
⊢ pullback.snd ((forget A).obj g).hom X✝.arrow ≫ X✝.arrow = pullback.snd ((forget A).obj g).hom X✝.arrow ≫ X✝.arrow
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✝ : HasPullbacks C
A : C
X✝ Y✝ : MonoOver A
k : X✝ ⟶ Y✝
g : MonoOver A
⊢ pullback.snd g.obj.hom X✝.arrow ≫ Over.Hom.left k.hom ≫ Y✝.arrow = pullback.snd g.obj.hom X✝.arrow ≫ X✝.arrow

Tactic:
w k

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
A : C
X✝ Y✝ : MonoOver A
k : X✝ ⟶ Y✝
g : MonoOver A
⊢ pullback.snd g.obj.hom X✝.arrow ≫ X✝.arrow = pullback.snd g.obj.hom X✝.arrow ≫ X✝.arrow
Module: Mathlib.CategoryTheory.Subobject.Limits

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : HasImage f
inst✝ : Epi (factorThruImageSubobject f)
h : f ≫ g = 0
⊢ factorThruImageSubobject f ≫ (imageSubobject f).arrow ≫ g = 0

Tactic:
by simp [h]

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 : f = 0
⊢ (isoZeroOfMonoEqZero h ≪≫ HasZeroObject.zeroIsoInitial).hom ≫ initial.to Y = f

Tactic:
by simp [h]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ α.app X =
    cokernel.π ((kernel.ι α).app X) ≫
      cokernelComparison (kernel.ι α) ((evaluation C D).obj X) ≫
        (coimageImageComparison α).app X ≫ ((evaluation C D).obj X).map (kernel.ι (cokernel.π α))

Tactic:
erw [π_comp_cokernelComparison_assoc _ ((evaluation C D).obj X)]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ α.app X =
    ((evaluation C D).obj X).map (cokernel.π (kernel.ι α)) ≫
      (coimageImageComparison α).app X ≫ ((evaluation C D).obj X).map (kernel.ι (cokernel.π α))
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: case f.refine_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, g ≤ f
⊢ (Sigma.desc fun b ↦ Subtype.casesOn b fun g m ↦ underlying.map (homOfLE ⋯)) ≫ f.arrow = smallCoproductDesc s

Tactic:
ext
      dsimp [smallCoproductDesc]
      simp

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 : D ≌ D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
inst✝ : L.HasPointwiseLeftKanExtensionAt F Y
⊢ L'.HasPointwiseLeftKanExtensionAt F Y'

Tactic:
by
  rw [← hasPointwiseLeftKanExtensionAt_iff_of_natIso_left F eL,
    hasPointwiseLeftKanExtensionAt_iff_of_iso _ F e.symm]
  let Φ := CostructuredArrow.post L E.functor Y
  have : HasColimit ((asEquivalence Φ).functor ⋙
    CostructuredArrow.proj (L ⋙ E.functor) (E.functor.obj Y) ⋙ F) :=
    (inferInstance : HasPointwiseLeftKanExtensionAt L F Y)
  exact hasColimit_of_equivalence_comp (asEquivalence Φ)

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✝.HasRightKanExtension F
L : C ⥤ D
inst✝² : ∀ (G : C ⥤ H), L.HasRightKanExtension G
inst✝¹ : HasLimitsOfShape C H
inst✝ : HasLimitsOfShape D H
X✝ Y✝ : C ⥤ H
f : X✝ ⟶ Y✝
i : C
⊢ limMap (L.ran.map f) ≫ ((L.ran.obj Y✝).limitIsoOfIsRightKanExtension (L.ranCounit.app Y✝)).hom ≫ limit.π Y✝ i =
    ((L.ran.obj X✝).limitIsoOfIsRightKanExtension (L.ranCounit.app X✝)).hom ≫ limMap f ≫ limit.π Y✝ i

Tactic:
limMap_π,

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
L✝ : C ⥤ D
H : Type u_3
inst✝⁴ : Category.{v_3, u_3} H
inst✝³ : ∀ (F : C ⥤ H), L✝.HasRightKanExtension F
L : C ⥤ D
inst✝² : ∀ (G : C ⥤ H), L.HasRightKanExtension G
inst✝¹ : HasLimitsOfShape C H
inst✝ : HasLimitsOfShape D H
X✝ Y✝ : C ⥤ H
f : X✝ ⟶ Y✝
i : C
⊢ limMap (L.ran.map f) ≫ ((L.ran.obj Y✝).limitIsoOfIsRightKanExtension (L.ranCounit.app Y✝)).hom ≫ limit.π Y✝ i =
    ((L.ran.obj X✝).limitIsoOfIsRightKanExtension (L.ranCounit.app X✝)).hom ≫ limit.π X✝ i ≫ f.app i
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:
ranAdjunction_counit

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
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.ranCounit.app F)
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.HasPointwiseRightKanExtension F
Y₁ Y₂ : D
f : Y₁ ⟶ Y₂
g₁ g₂ : StructuredArrow Y₂ L
φ : g₁ ⟶ g₂
⊢ ((const (StructuredArrow Y₂ L)).obj (limit (StructuredArrow.proj Y₁ L ⋙ F))).map φ ≫
      limit.π (StructuredArrow.proj Y₁ L ⋙ F) ((StructuredArrow.map f).obj g₂) =
    limit.π (StructuredArrow.proj Y₁ L ⋙ F) ((StructuredArrow.map f).obj g₁) ≫ (StructuredArrow.proj Y₂ L ⋙ F).map φ

Tactic:
simpa using (limit.w (StructuredArrow.proj Y₁ L ⋙ F)
              ((StructuredArrow.map f).map φ)).symm

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsSeparating
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (g₁ g₂ : G ⟶ X), g₁ ≫ f = g₂ ≫ f → g₁ = g₂
Z✝ : C
g₁ g₂ : Z✝ ⟶ X
h : g₁ ≫ f = g₂ ≫ f
G : C
hG : P G
h' : G ⟶ Z✝
⊢ (h' ≫ g₁) ≫ f = (h' ≫ g₂) ≫ f

Tactic:
by simp [h]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : HasPullbacks C
𝒢 : ObjectProperty C
inst✝¹ : ObjectProperty.Small.{w, v₁, u₁} 𝒢
inst✝ : LocallySmall.{w, v₁, u₁} C
h𝒢 : 𝒢.IsDetecting
X : C
P Q : Subobject X
h : (fun P ↦ {f | P.Factors f.snd}) P = (fun P ↦ {f | P.Factors f.snd}) Q
⊢ ∀ (G : C), 𝒢 G → ∀ {f : G ⟶ X}, P.Factors f ↔ Q.Factors f

Tactic:
simpa [Set.ext_iff, Sigma.forall] using h

Goal state after:
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:
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.GroupTheory.Divisible

Goal state before:
pp: 𝕜 : Type ?u.3
inst✝¹ : DivisionRing 𝕜
inst✝ : CharZero 𝕜
n : ℤ
q : 𝕜
hn : n ≠ 0
⊢ n • (q / ↑n) = q

Tactic:
by
    rw [zsmul_eq_mul, (Int.cast_commute n _).eq, div_mul_cancel₀ q (Int.cast_ne_zero.mpr hn)]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
m : ℤ
⊢ ∀ ⦃j : ℤ⦄, m ≠ j → (fun x y ↦ Ioc (a * b ^ x) (a * b ^ (x + 1)) ∩ Ioc (a * b ^ y) (a * b ^ (y + 1)) ⊆ ∅) m j

Tactic:
n

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
m n : ℤ
⊢ m ≠ n → (fun x y ↦ Ioc (a * b ^ x) (a * b ^ (x + 1)) ∩ Ioc (a * b ^ y) (a * b ^ (y + 1)) ⊆ ∅) m n
Module: Mathlib.Algebra.Order.Interval.Set.Group

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
m : ℤ
⊢ ∀ ⦃j : ℤ⦄, m ≠ j → (fun x y ↦ Ico (a * b ^ x) (a * b ^ (x + 1)) ∩ Ico (a * b ^ y) (a * b ^ (y + 1)) ⊆ ∅) m j

Tactic:
n

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
m n : ℤ
⊢ m ≠ n → (fun x y ↦ Ico (a * b ^ x) (a * b ^ (x + 1)) ∩ Ico (a * b ^ y) (a * b ^ (y + 1)) ⊆ ∅) m n
Module: Mathlib.Data.Nat.Count

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
⊢ count p 1 = if p 0 then 1 else 0

Tactic:
by simp [count_succ]

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: a✝ b m n p✝ : ℕ
motive : ℕ → Sort u_1
prime_pow : (p n : ℕ) → Prime p → 0 < n → motive (p ^ n)
zero : motive 0
one : motive 1
coprime : (a b : ℕ) → 1 < a → 1 < b → a.Coprime b → motive a → motive b → motive (a * b)
a p : ℕ
⊢ (n : ℕ) → Prime p → ¬p ∣ a → 0 < n → motive a → motive (p ^ n * a)

Tactic:
n

Goal state after:
a✝ b m n✝ p✝ : ℕ
motive : ℕ → Sort u_1
prime_pow : (p n : ℕ) → Prime p → 0 < n → motive (p ^ n)
zero : motive 0
one : motive 1
coprime : (a b : ℕ) → 1 < a → 1 < b → a.Coprime b → motive a → motive b → motive (a * b)
a p n : ℕ
⊢ Prime p → ¬p ∣ a → 0 < n → motive a → motive (p ^ n * a)
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: α : Type u_1
β : Type u_2
g : Set α → Filter β
⊢ ⊤.lift g = g univ

Tactic:
by simp [Filter.lift]

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 : α
⊢ toIocDiv hp a (-b) = -(toIcoDiv hp (-a) b + 1)

Tactic:
by
  rw [← neg_neg b, toIcoDiv_neg, neg_neg, neg_neg, neg_add', neg_neg, add_sub_cancel_right]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen s
⊢ frontier s = closure s \ s

Tactic:
by
  rw [frontier, hs.interior_eq]

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
x : X
g : X → Y
h : f =ᶠ[𝓝 x] g
⊢ ContinuousAt f x ↔ ContinuousAt g x

Tactic:
by
  simp only [ContinuousAt, tendsto_congr' h, h.eq_of_nhds]

Goal state after:
Module: Mathlib.Topology.Maps.OpenQuotient

Goal state before:
pp: case mp.mp
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
U : Set C
V : Set B
hV : IsOpen[inst✝¹] V
e : f ⁻¹' V = p ⁻¹' U
x : A
y : B
hy : y ∈ V
e' : q y = g (p x)
⊢ p x ∈ U

Tactic:
obtain ⟨y, rfl⟩ := H ⟨_, ⟨x, rfl⟩, (e'.trans (congr_fun h x)).symm⟩

Goal state after:
case mp.mp
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
U : Set C
V : Set B
hV : IsOpen[inst✝¹] V
e : f ⁻¹' V = p ⁻¹' U
x y : A
hy : f y ∈ V
e' : q (f y) = g (p x)
⊢ p x ∈ U
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
s : Set (Set α)
t : Set α
ht : GenerateOpen s t
⊢ ∀ s_1 ∈ insert t s, IsOpen[generateFrom s] s_1

Tactic:
rintro t (rfl | h)

Goal state after:
case inl
α : Type u_1
s : Set (Set α)
t : Set α
ht : GenerateOpen s t
⊢ IsOpen[generateFrom s] t

case inr
α : Type u_1
s : Set (Set α)
t✝ : Set α
ht : GenerateOpen s t✝
t : Set α
h : t ∈ s
⊢ IsOpen[generateFrom s] t
Module: Mathlib.Topology.Homeomorph.Defs

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
s : Set X
⊢ IsOpen[inst✝] (⇑h '' s) ↔ IsOpen[inst✝¹] s

Tactic:
rw [← preimage_symm, isOpen_preimage]

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
f : α → β
t : TopologicalSpace α
b : Set (Set β)
⊢ Continuous[t, generateFrom b] f ↔ ∀ s ∈ b, IsOpen[t] (f ⁻¹' s)

Tactic:
rw [continuous_iff_coinduced_le, le_generateFrom_iff_subset_isOpen]

Goal state after:
α : Type u
β : Type v
f : α → β
t : TopologicalSpace α
b : Set (Set β)
⊢ b ⊆ {s | IsOpen[coinduced f t] s} ↔ ∀ s ∈ b, IsOpen[t] (f ⁻¹' s)
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hg : IsOpenMap g
hf : IsOpenMap f
s : Set X
hs : IsOpen[inst✝²] s
⊢ IsOpen[inst✝] (g '' f '' s)

Tactic:
exact hg _ (hf _ hs)

Goal state after:
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
h : ∀ (x : X) (l : Filter Y), ClusterPt (f x) l → ClusterPt x (comap f l)
x : X
s : Set X
hs : f x ∉ interior (f '' s)
⊢ x ∉ interior s

Tactic:
mem_interior_iff_not_clusterPt_compl,

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : ∀ (x : X) (l : Filter Y), ClusterPt (f x) l → ClusterPt x (comap f l)
x : X
s : Set X
hs : ¬¬ClusterPt (f x) (𝓟 (f '' s)ᶜ)
⊢ ¬¬ClusterPt x (𝓟 sᶜ)
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hg : IsClosedMap g
hf : IsClosedMap f
s : Set X
hs : IsClosed[inst✝²] s
⊢ IsClosed[inst✝] (g '' f '' s)

Tactic:
exact hg _ (hf _ hs)

Goal state after:
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
hf : IsClosedEmbedding f
s : Set X
h : IsClosed[inst✝] (f '' s)
⊢ IsClosed[inst✝¹] s

Tactic:
← preimage_image_eq s hf.injective

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsClosedEmbedding f
s : Set X
h : IsClosed[inst✝] (f '' s)
⊢ IsClosed[inst✝¹] (f ⁻¹' f '' s)
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
f : β → α
a : α
s : Set α
l : Filter β
h : Tendsto f l (𝓝[s] a)
⊢ ∀ᶠ (i : β) in l, f i ∈ s

Tactic:
simp_rw [nhdsWithin_eq, tendsto_iInf, mem_ofPred_eq, tendsto_principal, mem_inter_iff,
    eventually_and] at h
  exact (h univ ⟨mem_univ a, isOpen_univ⟩).2

Goal state after: