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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasKernels C
inst✝³ : HasCokernels C
inst✝² : HasZeroObject C
X Y : C
f : X ⟶ Y
inst✝¹ : Mono f
inst✝ : IsIso (coimageImageComparison f)
⊢ IsIso (cokernel.π (kernel.ι f) ≫ coimageImageComparison f)

Tactic:
exact IsIso.comp_isIso

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

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

Tactic:
sub_self,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
⊢ a - 0 = a
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: case refine_1
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Epi f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
s : CokernelCofork (kernel.ι f)
⊢ Cofork.π (CokernelCofork.ofπ f ⋯) ≫
      inv (imageMonoFactorisation f).m ≫ inv (coimageImageComparison f) ≫ colimit.desc (parallelPair (kernel.ι f) 0) s =
    Cofork.π s

Tactic:
· simp only [CokernelCofork.π_ofπ, ← Category.assoc]
          convert! colimit.ι_desc s WalkingParallelPair.one using 2
          rw [IsIso.comp_inv_eq, IsIso.comp_inv_eq, eq_comm, ← imageMonoFactorisation_e']
          exact (imageMonoFactorisation f).fac

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

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

Tactic:
leftCoset_assoc

Goal state after:
A B : GrpCat
f : A ⟶ B
b : ↑B
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
⊢ QuasiIso φ ↔ IsIso (S₁.descOpcycles φ.τ₂ ⋯)

Tactic:
let H : RightHomologyMapData φ
      (RightHomologyData.ofIsColimitCokernelCofork S₁ hg₁ _ S₁.opcyclesIsCokernel)
        (RightHomologyData.ofZeros S₂ hf₂ hg₂) :=
    { φQ := S₁.descOpcycles φ.τ₂ (by rw [← φ.comm₁₂, hf₂, comp_zero])
      φH := S₁.descOpcycles φ.τ₂ (by rw [← φ.comm₁₂, hf₂, comp_zero]) }
  exact H.quasiIso_iff

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 : ShortComplex C
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
⊢ h₁.π ≫ leftRightHomologyComparison' h₁ h₂ ≫ h₂.ι = h₁.i ≫ h₂.p

Tactic:
simp only [leftRightHomologyComparison'_eq_liftH,
    RightHomologyData.liftH_ι, LeftHomologyData.π_descH]

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
⊢ S.leftHomologyData.π ≫ leftHomologyMap' (𝟙 S) S.leftHomologyData h = cyclesMap' (𝟙 S) S.leftHomologyData h ≫ h.π

Tactic:
rw [← leftHomologyπ_naturality']

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 : ShortComplex C
inst✝ : S.HasHomology
h : S.LeftHomologyData
⊢ h.π ≫ h.homologyIso.inv = h.cyclesIso.inv ≫ S.homologyπ

Tactic:
by
  dsimp only [homologyπ, homologyIso]
  simp only [Iso.trans_inv, Iso.symm_inv, π_comp_leftHomologyIso_inv_assoc]

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

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
j : J
eq₁ : ∀ (j : J), (π₁.mapCocone c).ι.app j ≫ h₁.desc (π₁.mapCocone s) = (π₁.mapCocone s).ι.app j
eq₂ : ∀ (j : J), (π₂.mapCocone c).ι.app j ≫ h₂.desc (π₂.mapCocone s) = (π₂.mapCocone s).ι.app j
eq₁₂ : ∀ (j : J), (c.ι.app j).τ₁ ≫ (((const J).obj c.pt).obj j).f = (F.obj j).f ≫ (c.ι.app j).τ₂
⊢ (π₁.mapCocone c).ι.app j ≫ h₁.desc (π₁.mapCocone s) ≫ s.pt.f =
    (π₁.mapCocone c).ι.app j ≫ c.pt.f ≫ h₂.desc (π₂.mapCocone s)

Tactic:
have eq₁₂' := fun j => (s.ι.app j).comm₁₂

Goal state after:
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
j : J
eq₁ : ∀ (j : J), (π₁.mapCocone c).ι.app j ≫ h₁.desc (π₁.mapCocone s) = (π₁.mapCocone s).ι.app j
eq₂ : ∀ (j : J), (π₂.mapCocone c).ι.app j ≫ h₂.desc (π₂.mapCocone s) = (π₂.mapCocone s).ι.app j
eq₁₂ : ∀ (j : J), (c.ι.app j).τ₁ ≫ (((const J).obj c.pt).obj j).f = (F.obj j).f ≫ (c.ι.app j).τ₂
eq₁₂' : ∀ (j : J), (s.ι.app j).τ₁ ≫ (((const J).obj s.pt).obj j).f = (F.obj j).f ≫ (s.ι.app j).τ₂
⊢ (π₁.mapCocone c).ι.app j ≫ h₁.desc (π₁.mapCocone s) ≫ s.pt.f =
    (π₁.mapCocone c).ι.app j ≫ c.pt.f ≫ h₂.desc (π₂.mapCocone s)
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
⊢ rightHomologyMap' (φ - φ') h₁ h₂ = rightHomologyMap' φ h₁ h₂ - rightHomologyMap' φ' h₁ h₂

Tactic:
by
  simp only [sub_eq_add_neg, rightHomologyMap'_add, rightHomologyMap'_neg]

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

Tactic:
h₂₃.comm₂,

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 φ₂ φ₃
⊢ S₁.g ≫ h₁₂.h₂ + h₁₂.h₁ ≫ S₂.f + (S₁.g ≫ h₂₃.h₂ + h₂₃.h₁ ≫ S₂.f + φ₃.τ₂) =
    S₁.g ≫ (h₁₂.h₂ + h₂₃.h₂) + (h₁₂.h₁ + h₂₃.h₁) ≫ S₂.f + φ₃.τ₂
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 ι
⊢ hkf.lift (KernelFork.ofι S.f ⋯) ≫ (S.isoCyclesOfIsLimit hkf).hom ≫ S.homologyπ = 0

Tactic:
f'_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.toCycles ≫ (S.isoCyclesOfIsLimit hkf).inv) ≫ (S.isoCyclesOfIsLimit hkf).hom ≫ S.homologyπ = 0
Module: Mathlib.Algebra.Homology.ShortComplex.Ab

Goal state before:
pp: S : ShortComplex Ab
x : ↥(AddCommGrpCat.Hom.hom S.g).ker
⊢ (ConcreteCategory.hom S.iCycles) ((ConcreteCategory.hom S.abCyclesIso.inv) x) = ↑x

Tactic:
dsimp only [abCyclesIso]
  rw [← ConcreteCategory.comp_apply, S.abLeftHomologyData.cyclesIso_inv_comp_iCycles]
  rfl

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

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
this : S.HasHomology
z : IsZero h.left.H
⊢ h.left.π ≫ h.iso.hom ≫ h.right.ι = 0

Tactic:
IsZero.eq_of_src z h.iso.hom 0,

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
this : S.HasHomology
z : IsZero h.left.H
⊢ h.left.π ≫ 0 ≫ h.right.ι = 0
Module: Mathlib.Algebra.Homology.ShortComplex.Ab

Goal state before:
pp: case mp
S : ShortComplex Ab
⊢ (AddCommGrpCat.Hom.hom S.g).ker ≤ (AddCommGrpCat.Hom.hom S.f).range →
    (AddCommGrpCat.Hom.hom S.f).range = (AddCommGrpCat.Hom.hom S.g).ker

Tactic:
intro h
    refine le_antisymm ?_ h
    rintro _ ⟨x₁, rfl⟩
    rw [AddMonoidHom.mem_ker, ← ConcreteCategory.comp_apply, S.zero]
    rfl

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

Goal state before:
pp: case mpr
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
inst✝⁴ : S.HasHomology
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
inst✝² : F.PreservesLeftHomologyOf S
inst✝¹ : F.PreservesRightHomologyOf S
inst✝ : F.Faithful
h : S.Exact
⊢ (S.map F).Exact

Tactic:
exact h.map F

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
inst✝⁴ : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.Exact
inst✝³ : Mono S₁.f
inst✝² : Mono S₂.f
inst✝¹ : Mono φ.τ₁
inst✝ : Mono φ.τ₃
A : C
x₂ : A ⟶ S₁.X₂
hx₂ : x₂ ≫ φ.τ₂ = 0
x₁ : A ⟶ S₁.X₁
hx₁ : x₁ ≫ S₁.f = x₂
⊢ x₂ = 0

Tactic:
suffices x₁ = 0 by rw [← hx₁, this, zero_comp]

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₁.Exact
inst✝³ : Mono S₁.f
inst✝² : Mono S₂.f
inst✝¹ : Mono φ.τ₁
inst✝ : Mono φ.τ₃
A : C
x₂ : A ⟶ S₁.X₂
hx₂ : x₂ ≫ φ.τ₂ = 0
x₁ : A ⟶ S₁.X₁
hx₁ : x₁ ≫ S₁.f = x₂
⊢ x₁ = 0
Module: Mathlib.CategoryTheory.Subobject.Limits

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
W : C
h : W ⟶ X
inst✝ : HasPullbacks C
⊢ (Subobject.pullback h).obj (equalizerSubobject f g) = equalizerSubobject (h ≫ f) (h ≫ g)

Tactic:
refine skeletal _ ⟨iso_of_both_ways (homOfFactors ?_) (homOfFactors ?_)⟩
  · apply equalizerSubobject_factors
    have := (Subobject.isPullback h (equalizerSubobject f g)).w
    rw [← reassoc_of% (Subobject.isPullback h (equalizerSubobject f g)).w,
      ← reassoc_of% (Subobject.isPullback h (equalizerSubobject f g)).w,
      equalizerSubobject_arrow_comp]
  · apply pullback_factors
    apply equalizerSubobject_factors
    rw [assoc, assoc, equalizerSubobject_arrow_comp]

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

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✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
tfae_1_to_3 : (∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact) → F.PreservesHomology
hF : ∀ (S : ShortComplex C), S.Exact → (S.map F).Exact
S : ShortComplex C
hS : S.ShortExact
⊢ (S.map F).ShortExact

Tactic:
have : Mono (S.map F).f := exact_iff_mono _ (by simp) |>.1 <|
      hF (.mk (0 : 0 ⟶ S.X₁) S.f <| by simp) (exact_iff_mono _ (by simp) |>.2 hS.mono_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✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
tfae_1_to_3 : (∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact) → F.PreservesHomology
hF : ∀ (S : ShortComplex C), S.Exact → (S.map F).Exact
S : ShortComplex C
hS : S.ShortExact
this : Mono (S.map F).f
⊢ (S.map F).ShortExact
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: case some
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : LocallySmall.{w, v₁, u₁} C
inst✝¹ : WellPowered.{w, v₁, u₁} C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
Z✝ : C
u v : Z✝ ⟶ widePullback s
h : u ≫ widePullbackι s = v ≫ widePullbackι s
val✝ : ↑(⇑(equivShrink (Subobject A)) '' s)
⊢ u ≫ limit.π (wideCospan s) (some val✝) = v ≫ limit.π (wideCospan s) (some val✝)

Tactic:
apply (cancel_mono ((equivShrink (Subobject A)).symm _).arrow).1

Goal state after:
case some
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : LocallySmall.{w, v₁, u₁} C
inst✝¹ : WellPowered.{w, v₁, u₁} C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
Z✝ : C
u v : Z✝ ⟶ widePullback s
h : u ≫ widePullbackι s = v ≫ widePullbackι s
val✝ : ↑(⇑(equivShrink (Subobject A)) '' s)
⊢ (u ≫ limit.π (wideCospan s) (some val✝)) ≫ ((equivShrink (Subobject A)).symm ↑val✝).arrow =
    (v ≫ limit.π (wideCospan s) (some val✝)) ≫ ((equivShrink (Subobject A)).symm ↑val✝).arrow
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
f : Fan Z
c : Cofan fun x ↦ op (Z x)
hf : IsLimit f
hc : IsColimit c
f' : Fan Z
x✝ : Discrete α
j : α
⊢ ((hf.lift f').op.unop ≫ f.π.app { as := j }).op =
    (((opProductIsoCoproduct' hf hc).hom ≫ hc.desc f'.op).unop ≫ f.π.app { as := j }).op

Tactic:
simp only [Discrete.functor_obj, unop_op, Quiver.Hom.unop_op, IsLimit.fac, Fan.op, unop_comp,
    Category.assoc, op_comp, op_unop, Quiver.Hom.op_unop]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
f : Fan Z
c : Cofan fun x ↦ op (Z x)
hf : IsLimit f
hc : IsColimit c
f' : Fan Z
x✝ : Discrete α
j : α
⊢ (f'.π.app { as := j }).op =
    (f.π.app { as := j }).op ≫ (opProductIsoCoproduct' hf hc).hom ≫ hc.desc (Cofan.mk (op f'.pt) fun a ↦ (f'.proj a).op)
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst✝ : HasBinaryProduct A B
this : HasProduct fun x ↦ WalkingPair.casesOn x A B
⊢ HasCoproduct fun j ↦ WalkingPair.casesOn j (op A) (op B)

Tactic:
convert! (inferInstance : HasCoproduct fun x ↦ op (WalkingPair.casesOn x A B : C)) with x

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst✝ : HasBinaryProduct A B
this : HasProduct fun x ↦ WalkingPair.casesOn x A B
x : WalkingPair
⊢ WalkingPair.rec (op A) (op B) x = op (WalkingPair.rec A B x)
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} C'
inst✝⁴ : Category.{v_3, u_3} H
inst✝³ : Category.{v_4, u_4} D
inst✝² : Category.{v_5, u_5} D'
L : C ⥤ D
L' : C ⥤ D'
G : D ⥤ D'
inst✝¹ : G.IsEquivalence
f : L ⋙ G ⟶ L'
inst✝ : IsIso f
F : C ⥤ H
⊢ (RightExtension.postcomp₁ G f F).IsEquivalence

Tactic:
by
  apply CostructuredArrow.isEquivalenceMap₂

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

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
L : C ⥤ D
F : C ⥤ H
F' : D ⥤ H
G : C' ⥤ C
inst✝ : G.IsEquivalence
⊢ (RightExtension.precomp L F G).IsEquivalence

Tactic:
by
  apply CostructuredArrow.isEquivalenceMap₂

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

Goal state before:
pp: case refine_1.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ op (cokernel (kernel.ι f.unop)) ⟶ A

Tactic:
exact (Abelian.epiDesc f.unop _ (cokernel.condition (kernel.ι f.unop))).op

Goal state after:
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
⊢ Hom.right (Subobject.ofMkLEMk f g h) ≫ Hom.right (MonoOver.mk g).arrow = Hom.right (MonoOver.mk f).arrow

Tactic:
exact congr_arg CommaMorphism.right (Subobject.ofMkLEMk_comp h)

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

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
hP : P.IsSeparating
⊢ (P.inverseImage (proj S T)).IsSeparating

Tactic:
by
  refine fun X Y f g hfg => ext _ _ (hP _ _ fun G hG h => ?_)
  exact congr_arg CommaMorphism.left (hfg (mk (S.map h ≫ X.hom)) hG (homMk h rfl))

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

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddMonoid α
h : Periodic f c
⊢ Periodic f (0 • c)

Tactic:
simp_all [add_nsmul, ← add_assoc]

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

Goal state before:
pp: case succ
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddMonoid α
h : Periodic f c
n✝ : ℕ
a✝ : Periodic f (n✝ • c)
⊢ Periodic f ((n✝ + 1) • c)

Tactic:
simp_all [add_nsmul, ← add_assoc]

Goal state after:
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: n : ℕ
hn : n > 0
⊢ n = ∑ d ∈ n.divisors, #({k ∈ range n | n.gcd k = d})

Tactic:
nth_rw 1 [← card_range n]

Goal state after:
n : ℕ
hn : n > 0
⊢ #(range n) = ∑ d ∈ n.divisors, #({k ∈ range n | n.gcd k = d})
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case mp
m n : ℕ
⊢ Even (φ m) ∧ Even (φ n) → ¬(φ m).Coprime (φ n)

Tactic:
even_iff_two_dvd

Goal state after:
case mp
m n : ℕ
⊢ 2 ∣ φ m ∧ 2 ∣ φ n → ¬(φ m).Coprime (φ n)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case pos
a b : ℕ
h : a ∣ b
h' : φ a = φ b
ha : a = 0
⊢ a = b ∨ 2 * a = b

Tactic:
rw [ha, totient_zero, eq_comm, totient_eq_zero] at h'

Goal state after:
case pos
a b : ℕ
h : a ∣ b
h' : b = 0
ha : a = 0
⊢ a = b ∨ 2 * a = b
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 : α
⊢ toIocMod hp a b - b = -toIocDiv hp a b • p

Tactic:
rw [toIocMod, sub_sub_cancel_left, neg_smul]

Goal state after:
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: α : Type u_1
β : Type u_2
h : Set α → Set β
hh : Monotone h
⊢ ⊥.lift' h = 𝓟 (h ∅)

Tactic:
← principal_empty,

Goal state after:
α : Type u_1
β : Type u_2
h : Set α → Set β
hh : Monotone h
⊢ (𝓟 ∅).lift' h = 𝓟 (h ∅)
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: α : Type u_1
β : Type u_2
h : Set α → Set β
hh : Monotone h
⊢ ⊥.lift' h = 𝓟 (h ∅)

Tactic:
rw [← principal_empty, lift'_principal hh]

Goal state after:
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: case mp
X : Type u
inst✝ : TopologicalSpace X
x : X
C : Set X
h : ClusterPt x (𝓟 C)
hc : x ∉ C ∧ ¬AccPt x (𝓟 C)
⊢ False

Tactic:
rw [accPt_principal_iff_clusterPt] at hc

Goal state after:
case mp
X : Type u
inst✝ : TopologicalSpace X
x : X
C : Set X
h : ClusterPt x (𝓟 C)
hc : x ∉ C ∧ ¬ClusterPt x (𝓟 (C \ {x}))
⊢ False
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ x ∈ interior s ↔ ¬ClusterPt x (𝓟 sᶜ)

Tactic:
by
  rw [← mem_closure_iff_clusterPt, closure_compl, mem_compl_iff, not_not]

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

Goal state before:
pp: α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Archimedean α
p : α
hp : 0 < p
⊢ ⋃ n, Ico (n • p) ((n + 1) • p) = univ

Tactic:
by
  simpa only [zero_add] using iUnion_Ico_add_zsmul hp 0

Goal state after:
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:
by
  rw [← preimage_symm, isOpen_preimage]

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
f : α → β
T : Set (TopologicalSpace α)
t₂ : TopologicalSpace β
⊢ Continuous[sSup T, t₂] f ↔ ∀ t ∈ T, Continuous[_, t₂] f

Tactic:
by
  simp only [continuous_iff_le_induced, sSup_le_iff]

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 : IsClosedMap f
p : X → Prop
y₀ : Y
H : ∀ x₀ ∈ f ⁻¹' {y₀}, ∀ᶠ (x : X) in 𝓝 x₀, ¬p x
⊢ ∀ᶠ (x : Y) in 𝓝 y₀, ∀ x_1 ∈ f ⁻¹' {x}, ¬p x_1

Tactic:
exact hf.eventually_nhds_fiber y₀ H

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t : Set α
⊢ 𝓝[s ∩ t] a = 𝓝[s] a ⊓ 𝓟 t

Tactic:
by
  delta nhdsWithin
  rw [← inf_principal, inf_assoc]

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
β : Type u_5
T : Set (Set β)
f : α → β
x : α
x✝ : x ∈ s
⊢ ContinuousWithinAt f s x ↔ ∀ t ∈ T, f x ∈ t → f ⁻¹' t ∈ 𝓝[s] x

Tactic:
by
    delta ContinuousWithinAt
    simp only [TopologicalSpace.nhds_generateFrom, tendsto_iInf, tendsto_principal, mem_ofPred_eq,
      and_imp]
    exact forall_congr' fun t => forall_comm

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hst : s ⊆ t
hs : IsOpen[instTopologicalSpaceSubtype] (t ↓∩ s)
⊢ IsOpen[instTopologicalSpaceSubtype] (range (inclusion hst))

Tactic:
rwa [range_inclusion]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hst : s ⊆ t
hs : IsClosed[instTopologicalSpaceSubtype] (t ↓∩ s)
⊢ IsClosed[instTopologicalSpaceSubtype] (range (inclusion hst))

Tactic:
rwa [range_inclusion]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case inr
α : Type u
β : Type u_1
t : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : SeparableSpace β
f : α → β
h : IsOpenMap f
h' : IsInducing f
h✝ : Nonempty α
s : Set β
s_cnt : s.Countable
s_dense : Dense s
x : α
U : Set β
hU : IsOpen[inst✝¹] U
hx : f x ∈ U
⊢ (U ∩ f '' invFun f '' s).Nonempty

Tactic:
obtain ⟨-, ⟨hx'U, x', rfl⟩, hx's⟩ :=
    s_dense.inter_open_nonempty (U ∩ range f) (hU.inter h.isOpen_range) ⟨f x, hx, mem_range_self _⟩

Goal state after:
case inr
α : Type u
β : Type u_1
t : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : SeparableSpace β
f : α → β
h : IsOpenMap f
h' : IsInducing f
h✝ : Nonempty α
s : Set β
s_cnt : s.Countable
s_dense : Dense s
x : α
U : Set β
hU : IsOpen[inst✝¹] U
hx : f x ∈ U
x' : α
hx's : f x' ∈ s
hx'U : f x' ∈ U
⊢ (U ∩ f '' invFun f '' s).Nonempty
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: case h₁
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
z : β
x x' : α
left✝ : x' ≤ x
hz : z ∈ s x'
⊢ ∃ i, z ∈ s i

Tactic:
exact ⟨x', hz⟩

Goal state after: