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
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
⊢ e = 0

Tactic:
have :=
      monoIsKernelOfCokernel _
        (BiproductToPushoutIsCokernel.isColimitBiproductToPushout f g)

Goal state after:
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)) ⋯)
⊢ e = 0
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
inst✝ : Epi f
b : ↑B
hb : ∀ (a : ↑A), (ConcreteCategory.hom f) a ≠ b
⊢ False

Tactic:
exact
    SurjectiveOfEpiAuxs.g_ne_h f b (fun ⟨c, hc⟩ => hb _ hc)
      (congr_arg GrpCat.Hom.hom ((cancel_epi f).1 (SurjectiveOfEpiAuxs.comp_eq f)))

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
inst✝¹ : S.HasLeftHomology
inst✝ : HasKernel S.g
h : S.LeftHomologyData := S.leftHomologyData
this : HasColimit (parallelPair h.f' 0)
e : parallelPair (kernel.lift S.g S.f ⋯) 0 ≅ parallelPair h.f' 0 :=
  parallelPair.ext (Iso.refl ((parallelPair (kernel.lift S.g S.f ⋯) 0).obj WalkingParallelPair.zero))
    ((kernelIsKernel S.g).conePointUniqueUpToIso h.hi) ⋯ ⋯
⊢ HasCokernel (kernel.lift S.g S.f ⋯)

Tactic:
exact hasColimit_of_iso e

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
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
f' : S.X₁ ⟶ kernel S.g := kernel.lift S.g S.f ⋯
hf' : f' = kernel.lift γ f' ⋯ ≫ kernel.ι γ
wπ : f' ≫ cokernel.π (kernel.ι γ) = 0
e : Abelian.image S.f ≅ kernel γ :=
  S.abelianImageToKernelIsKernel.conePointUniqueUpToIso (limit.isLimit (parallelPair (kernel.ι S.g ≫ cokernel.π S.f) 0))
⊢ S.LeftHomologyData

Tactic:
have he : e.hom ≫ kernel.ι γ = S.abelianImageToKernel :=
    IsLimit.conePointUniqueUpToIso_hom_comp _ _ WalkingParallelPair.zero

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
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
f' : S.X₁ ⟶ kernel S.g := kernel.lift S.g S.f ⋯
hf' : f' = kernel.lift γ f' ⋯ ≫ kernel.ι γ
wπ : f' ≫ cokernel.π (kernel.ι γ) = 0
e : Abelian.image S.f ≅ kernel γ :=
  S.abelianImageToKernelIsKernel.conePointUniqueUpToIso (limit.isLimit (parallelPair (kernel.ι S.g ≫ cokernel.π S.f) 0))
he : e.hom ≫ kernel.ι γ = S.abelianImageToKernel
⊢ S.LeftHomologyData
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₂
hl₁ : S₁.LeftHomologyData
hl₂ : S₂.LeftHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : hl₁.IsPreservedBy F
inst✝ : hl₂.IsPreservedBy F
⊢ F.map (cyclesMap' φ hl₁ hl₂) = cyclesMap' (F.mapShortComplex.map φ) (hl₁.map F) (hl₂.map F)

Tactic:
by
  have γ : ShortComplex.LeftHomologyMapData φ hl₁ hl₂ := default
  rw [γ.cyclesMap'_eq, (γ.map F).cyclesMap'_eq, ShortComplex.LeftHomologyMapData.map_φK]

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
X✝ Y✝ : ShortComplex C
i : X✝ ⟶ Y✝
x✝ : Mono i
⊢ NormalMono i

Tactic:
by
  refine NormalMono.mk _ (cokernel.π i) (cokernel.condition _)
    (isLimitOfIsLimitπ _ ?_ ?_ ?_)
  all_goals apply Abelian.isLimitMapConeOfKernelForkOfι

Goal state after:
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₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasRightHomology
inst✝² : S₂.HasRightHomology
inst✝¹ : F.PreservesRightHomologyOf S₁
inst✝ : F.PreservesRightHomologyOf S₂
⊢ F.map (rightHomologyMap φ) ≫ (S₂.mapRightHomologyIso F).inv =
    (S₁.mapRightHomologyIso F).inv ≫ rightHomologyMap (F.mapShortComplex.map φ)

Tactic:
by
  rw [← cancel_epi (S₁.mapRightHomologyIso F).hom, ← mapRightHomologyIso_hom_naturality_assoc,
    Iso.hom_inv_id, comp_id, Iso.hom_inv_id_assoc]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Type u₁
⊢ Mono (↾WithBot.some)

Tactic:
rw [mono_iff_injective]
          exact WithBot.coe_injective

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✝¹ : Preadditive D
S : ShortComplex C
inst✝ : HasZeroObject C
s : S.Splitting
hp : IsColimit (CokernelCofork.ofπ S.g ⋯)
g' : (CokernelCofork.ofπ S.g ⋯).pt ⟶ (CokernelCofork.ofπ S.g ⋯).pt := hp.desc (CokernelCofork.ofπ S.g ⋯)
hg' : g' = 𝟙 (CokernelCofork.ofπ S.g ⋯).pt
wι : 0 ≫ g' = 0
⊢ Mono g'

Tactic:
rw [hg']

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 : ShortComplex C
inst✝ : HasZeroObject C
s : S.Splitting
hp : IsColimit (CokernelCofork.ofπ S.g ⋯)
g' : (CokernelCofork.ofπ S.g ⋯).pt ⟶ (CokernelCofork.ofπ S.g ⋯).pt := hp.desc (CokernelCofork.ofπ S.g ⋯)
hg' : g' = 𝟙 (CokernelCofork.ofπ S.g ⋯).pt
wι : 0 ≫ g' = 0
⊢ Mono (𝟙 (CokernelCofork.ofπ S.g ⋯).pt)
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.τ₂ ≫ e.hom.τ₂
⊢ (e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁) ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ = 𝟙 S₂.X₂

Tactic:
← comp_τ₂,

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.τ₂ = (e.inv ≫ e.hom).τ₂
⊢ (e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁) ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ = 𝟙 S₂.X₂
Module: Mathlib.CategoryTheory.Subobject.Basic

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

Tactic:
simp only [ofMkLE, ofLE, ← Functor.map_comp underlying,
    assoc]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
B A₁ : C
f : A₁ ⟶ B
inst✝ : Mono f
X Y : Subobject B
h₁ : mk f ≤ X
h₂ : X ≤ Y
⊢ (underlyingIso f).inv ≫ underlying.map (h₁.hom ≫ h₂.hom) = (underlyingIso f).inv ≫ underlying.map ⋯.hom
Module: Mathlib.CategoryTheory.Subobject.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y W : C
f : X ⟶ Y
inst✝ : HasPullbacks C
y : Subobject Y
h : W ⟶ X
⊢ ((Subobject.pullback f).obj y).Factors h ↔ y.Factors (h ≫ f)

Tactic:
refine ⟨fun hf ↦ ?_, fun hF ↦ pullback_factors f y h hF⟩
  rw [factors_iff]
  use Subobject.factorThru _ _ hf ≫ Subobject.pullbackπ f y
  simp [(Subobject.isPullback f y).w]

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

Goal state before:
pp: case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
f : MonoOver X
⊢ (map (𝟙 X)).obj (Quotient.mk'' f) = Quotient.mk'' f

Tactic:
exact Quotient.sound ⟨(MonoOver.mapId _).app f⟩

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ Epi (kernel.lift S.g S.f ⋯) ↔ Epi (imageToKernel' S.f S.g ⋯)

Tactic:
have : factorThruImage S.f ≫ imageToKernel' S.f S.g S.zero = kernel.lift S.g S.f S.zero := by
    simp only [← cancel_mono (kernel.ι _), kernel.lift_ι, imageToKernel',
      Category.assoc, image.fac]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
this : factorThruImage S.f ≫ imageToKernel' S.f S.g ⋯ = kernel.lift S.g S.f ⋯
⊢ Epi (kernel.lift S.g S.f ⋯) ↔ Epi (imageToKernel' S.f S.g ⋯)
Module: Mathlib.CategoryTheory.Subobject.Limits

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
inst✝² : HasImage f
g : Y ⟶ Z
inst✝¹ : HasImage g
sq : Arrow.mk f ⟶ Arrow.mk g
inst✝ : HasImageMap sq
⊢ (imageSubobjectIso (Arrow.mk f).hom).hom ≫ image.map sq = imageSubobjectMap sq ≫ (imageSubobjectIso g).hom

Tactic:
by
  simp [imageSubobjectMap]

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 ⋙ E.functor).HasPointwiseLeftKanExtensionAt F Y'

Tactic:
hasPointwiseLeftKanExtensionAt_iff_of_iso _ F e.symm

Goal state after:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} D'
inst✝¹ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E : D ≌ D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
inst✝ : L.HasPointwiseLeftKanExtensionAt F Y
⊢ (L ⋙ E.functor).HasPointwiseLeftKanExtensionAt F (E.functor.obj Y)
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
J : Type u'
inst✝² : Category.{v', u'} J
inst✝¹ : HasLimitsOfShape J C
inst✝ : lim.PreservesEpimorphisms
⊢ PreservesFiniteColimits lim

Tactic:
apply +allowSynthFailures preservesFiniteColimits_of_preservesHomology
    · exact preservesHomology_of_preservesEpis_and_kernels _
    · exact additive_of_preservesBinaryBiproducts _

Goal state after:
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)
s : Trident f
j : J
⊢ s.π.app zero ≫ f j = s.π.app one

Tactic:
← s.w (line j),

Goal state after:
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
s : Trident f
j : J
⊢ s.π.app zero ≫ f j = s.π.app zero ≫ (parallelFamily f).map (line j)
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)
s : Cotrident f
j : J
⊢ f j ≫ s.ι.app one = s.ι.app zero

Tactic:
← s.w (line j),

Goal state after:
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
s : Cotrident f
j : J
⊢ f j ≫ s.ι.app one = (parallelFamily f).map (line j) ≫ s.ι.app one
Module: Mathlib.Algebra.Category.Grp.AB

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
X Y : Discrete J ⥤ AddCommGrpCat
f : X ⟶ Y
hf : Epi f
⊢ Epi (lim.map f)

Tactic:
by
      let iX : limit X ≅ AddCommGrpCat.of ((i : J) → X.obj ⟨i⟩) := (Pi.isoLimit X).symm ≪≫
        (limit.isLimit _).conePointUniqueUpToIso (AddCommGrpCat.HasLimit.productLimitCone _).isLimit
      let iY : limit Y ≅ AddCommGrpCat.of ((i : J) → Y.obj ⟨i⟩) := (Pi.isoLimit Y).symm ≪≫
        (limit.isLimit _).conePointUniqueUpToIso (AddCommGrpCat.HasLimit.productLimitCone _).isLimit
      have : Pi.map (fun i ↦ f.app ⟨i⟩) = iX.inv ≫ lim.map f ≫ iY.hom := by
        simp only [Discrete.functor_obj_eq_as, Discrete.mk_as, Pi.isoLimit,
          IsLimit.conePointUniqueUpToIso, limit.cone, AddCommGrpCat.HasLimit.productLimitCone,
          Iso.trans_inv, Functor.mapIso_inv, IsLimit.uniqueUpToIso_inv, Cone.forget_map,
          IsLimit.liftConeMorphism_hom, limit.isLimit_lift, Iso.symm_inv, Functor.mapIso_hom,
          IsLimit.uniqueUpToIso_hom, lim_map, Iso.trans_hom, Iso.symm_hom,
          AddCommGrpCat.HasLimit.lift, Category.assoc, limit.lift_map_assoc, iX, iY]
        ext g j
        change _ = (_ ≫ limit.π (Discrete.functor fun j ↦ Y.obj { as := j }) ⟨j⟩) _
        simp only [Discrete.functor_obj_eq_as, productIsProduct', limit.lift_π,
          Fan.mk_π_app, Pi.map_apply]
        change _ = (_ ≫ _ ≫ limit.π Y ⟨j⟩) _
        simp
      suffices Epi (iX.hom ≫ (iX.inv ≫ lim.map f ≫ iY.hom) ≫ iY.inv) by simpa using this
      suffices Epi (iX.inv ≫ lim.map f ≫ iY.hom) from inferInstance
      rw [AddCommGrpCat.epi_iff_surjective, ← this]
      simp_rw [CategoryTheory.NatTrans.epi_iff_epi_app, AddCommGrpCat.epi_iff_surjective] at hf
      refine fun b ↦ ⟨fun i ↦ (hf ⟨i⟩ (b i)).choose, ?_⟩
      funext i
      exact (hf ⟨i⟩ (b i)).choose_spec

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

Goal state before:
pp: case mpr.refine_2
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective ⇑(ConcreteCategory.hom c.inl)
h₂ : Injective ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (Set.range ⇑(ConcreteCategory.hom c.inl)) (Set.range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : (fun X ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })),
    x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ Set.range ⇑(ConcreteCategory.hom c.inr)
⊢ ∀ {T : Type u} (f : X ⟶ T) (g : Y ⟶ T),
    (c.inl ≫
        ↾fun x ↦
          if h : x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) then
            (ConcreteCategory.hom f) ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inl)) h₁).symm ⟨x, h⟩)
          else (ConcreteCategory.hom g) ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inr)) h₂).symm ⟨x, ⋯⟩)) =
      f

Tactic:
intro T f g
        ext x
        simp

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

Goal state before:
pp: C : Type u
F✝ : C → Type v
J : Type v
F : J → Type (max v u)
s : Cocone (Discrete.functor F)
m :
  { pt := (j : J) × F j,
        ι :=
          Discrete.natTrans fun x ↦
            match x with
            | { as := j } => ↾fun x ↦ ⟨j, x⟩ }.pt ⟶
    s.pt
w :
  ∀ (j : Discrete J),
    { pt := (j : J) × F j,
                ι :=
                  Discrete.natTrans fun x ↦
                    match x with
                    | { as := j } => ↾fun x ↦ ⟨j, x⟩ }.ι.app
          j ≫
        m =
      s.ι.app j
⊢ m = ↾fun x ↦ (ConcreteCategory.hom (s.ι.app { as := x.fst })) x.snd

Tactic:
ext ⟨j, x⟩

Goal state after:
C : Type u
F✝ : C → Type v
J : Type v
F : J → Type (max v u)
s : Cocone (Discrete.functor F)
m :
  { pt := (j : J) × F j,
        ι :=
          Discrete.natTrans fun x ↦
            match x with
            | { as := j } => ↾fun x ↦ ⟨j, x⟩ }.pt ⟶
    s.pt
w :
  ∀ (j : Discrete J),
    { pt := (j : J) × F j,
                ι :=
                  Discrete.natTrans fun x ↦
                    match x with
                    | { as := j } => ↾fun x ↦ ⟨j, x⟩ }.ι.app
          j ≫
        m =
      s.ι.app j
j : J
x : F j
⊢ (ConcreteCategory.hom m).toFun ⟨j, x⟩ =
    (ConcreteCategory.hom (↾fun x ↦ (ConcreteCategory.hom (s.ι.app { as := x.fst })) x.snd)).toFun ⟨j, x⟩
Module: Mathlib.Algebra.Category.Grp.Injective

Goal state before:
pp: case inl
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
g : ↥(ℤ ∙ 0) →ₗ[ℤ] A
⊢ ∃ g', ∀ (x : ℤ) (mem : x ∈ ℤ ∙ 0), g' x = g ⟨x, mem⟩

Tactic:
refine ⟨0, fun n hn ↦ ?_⟩
    rw [Submodule.span_zero_singleton] at hn
    subst hn
    exact (map_zero g).symm

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

Goal state before:
pp: case convert_1
a b m n✝ p✝ : ℕ
motive : ℕ → Sort u_1
zero : motive 0
one : motive 1
prime_pow_mul : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → motive a → motive (p ^ n * a)
n k : ℕ
hk : (m : ℕ) → m < k + 2 → motive m
p : ℕ := (k + 2).minFac
hp : Prime p
t : ℕ := (k + 2).factorization p
hpt : p ^ t ∣ k + 2
htp : 0 < t
⊢ ¬p ∣ (k + 2) / p ^ t

Tactic:
rw [Nat.dvd_div_iff_mul_dvd hpt, ← Nat.pow_succ]
        exact pow_succ_factorization_not_dvd (k + 1).succ_ne_zero hp

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: case e'_4
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) ≤ 2 * (c ^ 2 + d + 1) + d'
c0 : c > 0
⊢ (2 * (c ^ 2 + d + 1) + d' - d)! = (c ^ 2 + (c ^ 2 + d' + d + 1) + 1)!

pp: case inr
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) ≤ 2 * (c ^ 2 + d + 1) + d'
c0 : c > 0
⊢ (c ^ 2) ^ (c ^ 2 + d' + d + 1) < (c ^ 2 + (c ^ 2 + d' + d + 1) + 1)!

Tactic:
· congr 1
    lia

Goal state after:
case inr
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) ≤ 2 * (c ^ 2 + d + 1) + d'
c0 : c > 0
⊢ (c ^ 2) ^ (c ^ 2 + d' + d + 1) < (c ^ 2 + (c ^ 2 + d' + d + 1) + 1)!
Module: Mathlib.Topology.Basic

Goal state before:
pp: case empty
X : Type u
inst✝ : TopologicalSpace X
s : Set (Set X)
h : ∀ t ∈ ∅, IsOpen[inst✝] t
⊢ IsOpen[inst✝] univ

Tactic:
exact isOpen_univ

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Set α → Filter β
hg : Monotone g
⊢ ⋂₀ {s | s ∈ f.lift g} = ⋂ s ∈ f, ⋂₀ {t | t ∈ g s}

Tactic:
by
  simp only [sInter_eq_biInter, mem_ofPred_eq, mem_lift_sets hg, iInter_exists,
    iInter_and, @iInter_comm _ (Set β)]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: case mp
X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ Dense {x}ᶜ → ¬IsOpen {x}

Tactic:
intro hd

Goal state after:
case mp
X : Type u
inst✝ : TopologicalSpace X
x : X
hd : Dense {x}ᶜ
⊢ ¬IsOpen {x}
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: case H.H.H
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
hp' : Fact (0 < p)
z✝² z✝¹ z✝ : α
h : btw ↑z✝² ↑z✝¹ ↑z✝
⊢ btw ↑z✝¹ ↑z✝ ↑z✝²

Tactic:
simp_rw [btw_coe_iff] at h ⊢

Goal state after:
case H.H.H
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
hp' : Fact (0 < p)
z✝² z✝¹ z✝ : α
h : toIcoMod ⋯ z✝² z✝¹ ≤ toIocMod ⋯ z✝² z✝
⊢ toIcoMod ⋯ z✝¹ z✝ ≤ toIocMod ⋯ z✝¹ z✝²
Module: Mathlib.Topology.Maps.OpenQuotient

Goal state before:
pp: case mp.mpr
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
⊢ p x ∈ U → p x ∈ g ⁻¹' q '' V

Tactic:
· intro H
      exact ⟨f x, e.ge H, congr_fun h.symm x⟩

Goal state after:
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 Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Z
hf : IsInducing f
x : X
h : range f ∈ 𝓝 (f x)
⊢ map (g ∘ f) (𝓝 x) ≤ 𝓝 ((g ∘ f) x) ↔ map (g ∘ f) (𝓝 x) ≤ 𝓝 (g (f x))

Tactic:
comp

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
hs : ∀ (s : Set X), f '' interior s ⊆ interior (f '' s)
u : Set X
hu : IsOpen[inst✝¹] u
⊢ f '' u ⊆ interior (f '' u)

Tactic:
by simpa only [hu.interior_eq] using hs u

Goal state after:
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u_5
Y : Type u_6
s : Set (Set X)
t : Set (Set Y)
hs : ⋃₀ s = univ
ht : ⋃₀ t = univ
G : TopologicalSpace (X × Y) := generateFrom (image2 (fun x1 x2 ↦ x1 ×ˢ x2) s t)
u : Set X
hu : u ∈ s
⊢ ⋃ v ∈ t, u ×ˢ v = Prod.fst ⁻¹' u

Tactic:
by
            simp_rw [← prod_iUnion, ← sUnion_eq_biUnion, ht, prod_univ]

Goal state after:
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : IsInducing f
hg : IsInducing g
x✝ : X × Z
x : X
z : Z
⊢ 𝓝 x ×ˢ 𝓝 z = comap (fun p ↦ (f p.1, g p.2)) (𝓝 (f x) ×ˢ 𝓝 (g z))

Tactic:
hf.nhds_eq_comap,

Goal state after:
X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : IsInducing f
hg : IsInducing g
x✝ : X × Z
x : X
z : Z
⊢ comap f (𝓝 (f x)) ×ˢ 𝓝 z = comap (fun p ↦ (f p.1, g p.2)) (𝓝 (f x) ×ˢ 𝓝 (g z))
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
x : α
⊢ ContinuousWithinAt f {x}ᶜ x ↔ ContinuousAt f x

Tactic:
by
  rw [compl_eq_univ_sdiff, continuousWithinAt_sdiff_self, continuousWithinAt_univ]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
t u : Set ↑s
⊢ u ∈ 𝓝ˢ t ↔ Subtype.val '' u ∈ 𝓝ˢ[s] (Subtype.val '' t)

Tactic:
by
  rw [← map_nhdsSet_subtype_val, image_mem_map_iff Subtype.val_injective]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
⊢ IsOpen[t] s ↔ ∀ a ∈ s, ∃ t ∈ b, a ∈ t ∧ t ⊆ s

Tactic:
simp [isOpen_iff_mem_nhds, hb.mem_nhds_iff]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case intro.refine_1
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst✝ : Finite ι
s : Set ((a : ι) → A a)
val✝ : Fintype ι
a : (a : ι) → A a
x✝ : a ∈ s
I : Finset ι
t : (i : ι) → Set (A i)
h1 : ∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1
h2 : (↑I).pi t ⊆ s
⊢ ∃ u, (∀ (a_1 : ι), IsOpen[T a_1] (u a_1) ∧ a a_1 ∈ u a_1) ∧ univ.pi u ⊆ s

Tactic:
refine
      ⟨fun i => (h1 i).choose,
        ⟨fun i => (h1 i).choose_spec.2,
          (pi_mono fun i _ => (h1 i).choose_spec.1).trans (Subset.trans ?_ h2)⟩⟩

Goal state after:
case intro.refine_1
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst✝ : Finite ι
s : Set ((a : ι) → A a)
val✝ : Fintype ι
a : (a : ι) → A a
x✝ : a ∈ s
I : Finset ι
t : (i : ι) → Set (A i)
h1 : ∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1
h2 : (↑I).pi t ⊆ s
⊢ univ.pi t ⊆ (↑I).pi t
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
I : Set ι
s : (i : ι) → Set (A i)
a : (i : ι) → A i
hs : I.pi s ∈ Filter.pi fun i ↦ 𝓝 (a i)
i : ι
hi : i ∈ I
⊢ s i ∈ 𝓝 (a i)

Tactic:
exact mem_of_pi_mem_pi hs hi

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case neg
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
i : ι
U : (i : ι) → Set (X i)
s : Finset ι
hU : ∀ i ∈ s, U i ∈ {U | IsOpen[inst✝ i] U}
h : ((↑s).pi U).Nonempty
hi : i ∉ s
⊢ IsOpen[inst✝ i] univ

Tactic:
exact isOpen_univ

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
b : Set (Set α)
hb₁ : b.Countable
hb₂ : t = generateFrom b
⊢ ∃ b, b.Countable ∧ ∅ ∉ b ∧ IsTopologicalBasis b

Tactic:
refine ⟨_, ?_, notMem_sdiff_of_mem ?_, (isTopologicalBasis_of_subbasis hb₂).sdiff_empty⟩

Goal state after:
case refine_1
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
b : Set (Set α)
hb₁ : b.Countable
hb₂ : t = generateFrom b
⊢ ((fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ b} \ {∅}).Countable

case refine_2
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
b : Set (Set α)
hb₁ : b.Countable
hb₂ : t = generateFrom b
⊢ ∅ ∈ {∅}