mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ S.LeftHomologyData

Tactic:
let e : Abelian.image S.f ≅ kernel γ :=
    IsLimit.conePointUniqueUpToIso S.abelianImageToKernelIsKernel (limit.isLimit _)

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))
⊢ 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 : ShortComplex C
hr : S.RightHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : S.HasRightHomology
inst✝ : F.PreservesRightHomologyOf S
⊢ S.mapOpcyclesIso F = (hr.map F).opcyclesIso ≪≫ F.mapIso hr.opcyclesIso.symm

Tactic:
by
  ext
  dsimp [mapOpcyclesIso, opcyclesIso]
  simp only [map_opcyclesMap', ← opcyclesMap'_comp, Functor.map_id, comp_id,
    Functor.mapShortComplex_obj]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : C
i : P ≅ Q
hP : Injective P
X✝ Y✝ : C
g : X✝ ⟶ Q
f : X✝ ⟶ Y✝
mono : Mono f
h : Y✝ ⟶ P
h_eq : f ≫ h = g ≫ i.inv
⊢ f ≫ h ≫ i.hom = g

Tactic:
rw [← Category.assoc, h_eq, Category.assoc, Iso.inv_hom_id, Category.comp_id]

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
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
S : ShortComplex C
hf : S.f = 0
inst✝ : PreservesLimit (parallelPair S.g 0) F
h : S.RightHomologyData
⊢ PreservesLimit (parallelPair h.g' 0) F

Tactic:
by
      have := h.isIso_p hf
      let e : parallelPair S.g 0 ≅ parallelPair h.g' 0 :=
        parallelPair.ext (asIso h.p) (Iso.refl _) (by simp) (by simp)
      exact Limits.preservesLimit_of_iso_diagram F e

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
⊢ (S₁.g ≫ h₂ ≫ H₂.p) ≫ H₂.g' = H₁.p ≫ H₁.g' ≫ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃

Tactic:
RightHomologyData.p_g'_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₁ : 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
⊢ (S₁.g ≫ h₂ ≫ H₂.p) ≫ H₂.g' = S₁.g ≫ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃
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
inst✝¹ : S.HasHomology
inst✝ : HasZeroObject C
h : IsZero S.homology
⊢ Nonempty (S.homology ≅ 0)

Tactic:
exact ⟨h.isoZero⟩

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✝¹ : Preadditive C
S : ShortComplex C
inst✝ : HasZeroObject C
hf : S.f = 0
this : S.HasHomology
h : IsZero S.homology
⊢ Mono S.g

Tactic:
have := S.isIso_pOpcycles hf

Goal state after:
case mp
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : HasZeroObject C
hf : S.f = 0
this✝ : S.HasHomology
h : IsZero S.homology
this : IsIso S.pOpcycles
⊢ Mono S.g
Module: Mathlib.CategoryTheory.Adjunction.Reflective

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
i : D ⥤ C
inst✝ : Reflective i
A B B' : C
h : B ⟶ B'
hB : i.essImage B
hB' : i.essImage B'
f : A ⟶ B
⊢ (unitCompPartialBijective A hB') (f ≫ h) = (unitCompPartialBijective A hB) f ≫ h

Tactic:
by
  rw [← Equiv.eq_symm_apply, unitCompPartialBijective_symm_natural A h hB, Equiv.symm_apply_apply]

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

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

Tactic:
by simp [ofLEMk]

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

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✝ : HasImages C
f g : Over X
k : f ⟶ g
⊢ imageMonoOver f.hom ⟶ imageMonoOver g.hom

Tactic:
apply (forget X).preimage _
    apply Over.homMk _ _
    · exact
        image.lift
          { I := Limits.image _
            m := image.ι g.hom
            e := k.left ≫ factorThruImage g.hom }
    · apply image.lift_fac

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
⊢ ∀ (a : MonoOver Y),
    (map g).obj ((pullback f).obj (Quotient.mk'' a)) = (pullback k).obj ((map h).obj (Quotient.mk'' a))

Tactic:
intro a

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver Y
⊢ (map g).obj ((pullback f).obj (Quotient.mk'' a)) = (pullback k).obj ((map h).obj (Quotient.mk'' a))
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✝⁶ : Preadditive C
inst✝⁵ : Preadditive D
F : C ⥤ D
inst✝⁴ : F.Additive
inst✝³ : F.PreservesHomology
inst✝² : HasZeroObject C
inst✝¹ : HasFiniteProducts C
inst✝ : HasKernels C
this✝¹ : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
this✝ : HasBinaryBiproducts C
this : HasEqualizers C
⊢ PreservesFiniteLimits F

Tactic:
have : HasZeroObject D :=
    ⟨F.obj 0, by rw [IsZero.iff_id_eq_zero, ← F.map_id, id_zero, F.map_zero]⟩

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
F : C ⥤ D
inst✝⁴ : F.Additive
inst✝³ : F.PreservesHomology
inst✝² : HasZeroObject C
inst✝¹ : HasFiniteProducts C
inst✝ : HasKernels C
this✝² : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
this✝¹ : HasBinaryBiproducts C
this✝ : HasEqualizers C
this : HasZeroObject D
⊢ PreservesFiniteLimits F
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✝⁶ : Preadditive C
inst✝⁵ : Preadditive D
F : C ⥤ D
inst✝⁴ : F.Additive
inst✝³ : F.PreservesHomology
inst✝² : HasZeroObject C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasCokernels C
this✝¹ : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
this✝ : HasBinaryBiproducts C
this : HasCoequalizers C
⊢ PreservesFiniteColimits F

Tactic:
have : HasZeroObject D :=
    ⟨F.obj 0, by rw [IsZero.iff_id_eq_zero, ← F.map_id, id_zero, F.map_zero]⟩

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
F : C ⥤ D
inst✝⁴ : F.Additive
inst✝³ : F.PreservesHomology
inst✝² : HasZeroObject C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasCokernels C
this✝² : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
this✝¹ : HasBinaryBiproducts C
this✝ : HasCoequalizers C
this : HasZeroObject D
⊢ PreservesFiniteColimits F
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y : C
P : Subobject Y
⊢ IsIso P.arrow ↔ P = ⊤

Tactic:
by
  rw [isIso_iff_mk_eq_top, mk_arrow]

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

Goal state before:
pp: case mp
C : Type u_1
H : Type u_3
D : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_3, u_3} H
inst✝ : Category.{v_4, u_4} D
F' F'' : D ⥤ H
e : F' ≅ F''
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : L.whiskerLeft e.hom ≫ α' = α
a✝ : F'.IsRightKanExtension α
⊢ F''.IsRightKanExtension α'

Tactic:
exact isRightKanExtension_of_iso e α α' comm

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 ≫ limit.π X✝ i ≫ f.app i

Tactic:
limitIsoOfIsRightKanExtension_hom_π_assoc,

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 =
    limit.π (L.ran.obj X✝) (L.obj i) ≫ (L.ranCounit.app X✝).app i ≫ f.app i
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'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
inst✝ : F'.IsLeftKanExtension α
c : Cocone F
hc : IsColimit c
s : Cocone F'
m : (F'.coconeOfIsLeftKanExtension α c).pt ⟶ s.pt
hm : ∀ (j : D), (F'.coconeOfIsLeftKanExtension α c).ι.app j ≫ m = s.ι.app j
j : C
⊢ c.ι.app j ≫ m = c.ι.app j ≫ hc.desc { pt := s.1, ι := α ≫ L.whiskerLeft s.ι }

Tactic:
have := hm (L.obj j)
    nth_rw 1 [← F'.descOfIsLeftKanExtension_fac_app α ((const D).obj c.pt)]
    dsimp at this ⊢
    rw [assoc, this, IsColimit.fac, NatTrans.comp_app, whiskerLeft_app]

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

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian C
inst✝¹ : Abelian D
inst✝ : IsGrothendieckAbelian.{w, v, u} C
α : C ≌ D
hasFilteredColimits : HasFilteredColimitsOfSize.{w, w, v₂, u₂} D
⊢ AB5OfSize.{w, w, v₂, u₂} D

Tactic:
refine ⟨fun _ _ _ => ?_⟩
    exact HasExactColimitsOfShape.of_codomain_equivalence _ α

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian C
inst✝¹ : Abelian D
inst✝ : IsGrothendieckAbelian.{w, v, u} C
α : C ≌ D
⊢ IsGrothendieckAbelian.{w, v₂, u₂} D

Tactic:
by
  have hasFilteredColimits : HasFilteredColimitsOfSize.{w, w, v₂, u₂} D :=
    ⟨fun _ _ _ => Adjunction.hasColimitsOfShape_of_equivalence α.inverse⟩
  refine ⟨?_, hasFilteredColimits, ?_, ?_⟩
  · exact locallySmall_of_faithful α.inverse
  · refine ⟨fun _ _ _ => ?_⟩
    exact HasExactColimitsOfShape.of_codomain_equivalence _ α
  · exact HasSeparator.of_equivalence α

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
I : Type v₁
inst✝ : SmallCategory I
F : I ⥤ C
c : Cocone (F ⋙ yoneda)
hc : IsColimit c
this :
  IsTerminal
    (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt))
⊢ IsTerminal
    ((overEquivPresheafCostructuredArrow c.pt).inverse.obj
      (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ yoneda)))

Tactic:
apply IsTerminal.ofIso this

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
I : Type v₁
inst✝ : SmallCategory I
F : I ⥤ C
c : Cocone (F ⋙ yoneda)
hc : IsColimit c
this :
  IsTerminal
    (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt))
⊢ colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt) ≅
    (overEquivPresheafCostructuredArrow c.pt).inverse.obj
      (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ yoneda))
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
inst✝ : HasColimitsOfShape F.Elementsᵒᵖ (Type w)
u : F.Elements
⊢ (ConcreteCategory.hom ((shrinkYonedaCompWhiskeringLeftObjπCompColimIso F).inv.app u.fst)) u.snd =
    (ConcreteCategory.hom (colimit.ι ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj u.fst) (op u)))
      (shrinkYonedaObjObjEquiv.symm (𝟙 (unop ((CategoryOfElements.π F).op.obj (op u)))))

Tactic:
by
  have :
      (coconeπOpCompShrinkYonedaObj F u.fst).ι.app (op u) ≫
        (shrinkYonedaCompWhiskeringLeftObjπCompColimIso F).inv.app u.fst =
      colimit.ι ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w}.obj u.fst) (op u) :=
    IsColimit.comp_coconePointUniqueUpToIso_inv (colimit.isColimit _) _ (op u)
  simpa using ConcreteCategory.congr_hom this (shrinkYonedaObjObjEquiv.symm (𝟙 _))

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.ModEq

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
a b p : G
⊢ a ≡ b [PMOD p] ↔ ↑a = ↑b

Tactic:
rw [modEq_comm]
  simp_rw [modEq_iff_eq_add_zsmul, QuotientAddGroup.eq_iff_sub_mem, AddSubgroup.mem_zmultiples_iff,
    eq_sub_iff_add_eq', eq_comm]

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p n = Fintype.card { k // k < n ∧ p k }

Tactic:
by
  rw [count_eq_card_filter_range, Fintype.card_of_subtype]
  simp

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:
intro a

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.Data.Nat.Factorization.Induction

Goal state before:
pp: case zero
motive : ℕ → Prop
zero : motive 0
one : motive 1
prime_mul : ∀ (p a : ℕ), Prime p → motive a → motive (p * a)
a p : ℕ
hp : Prime p
ha : motive a
⊢ motive (p ^ 0 * a)

Tactic:
| zero =>

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

Goal state before:
pp: case prime_pow
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
⊢ ∀ (p n : ℕ), Prime p → 0 < n → p ^ n ≠ 0 → f (p ^ n) = (p ^ n).factorization.prod fun p k ↦ f (p ^ k)

Tactic:
rintro p k hp - -
    simp [Prime.factorization_pow hp, Finsupp.prod_single_index _, hf]

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

Goal state before:
pp: case coprime
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
⊢ ∀ (a b : ℕ),
    1 < a →
      1 < b →
        a.Coprime b →
          (a ≠ 0 → f a = a.factorization.prod fun p k ↦ f (p ^ k)) →
            (b ≠ 0 → f b = b.factorization.prod fun p k ↦ f (p ^ k)) →
              a * b ≠ 0 → f (a * b) = (a * b).factorization.prod fun p k ↦ f (p ^ k)

Tactic:
intro a

Goal state after:
case coprime
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
a : ℕ
⊢ ∀ (b : ℕ),
    1 < a →
      1 < b →
        a.Coprime b →
          (a ≠ 0 → f a = a.factorization.prod fun p k ↦ f (p ^ k)) →
            (b ≠ 0 → f b = b.factorization.prod fun p k ↦ f (p ^ k)) →
              a * b ≠ 0 → f (a * b) = (a * b).factorization.prod fun p k ↦ f (p ^ k)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case zero
a k n : ℕ
a_ne_zero : a ≠ 0
⊢ #({x ∈ Ico k (k + (n % a + a * 0)) | a.Coprime x}) ≤ φ a * (0 + 1)

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Data.Set.Constructions

Goal state before:
pp: case refine_2
α : Type u_1
S : Set (Set α)
cond : FiniteInter S
F : Finset (Set α)
⊢ ∀ (a : Set α) (s : Finset (Set α)), a ∉ s → (↑s ⊆ S → ⋂₀ ↑s ∈ S) → ↑(insert a s) ⊆ S → ⋂₀ ↑(insert a s) ∈ S

Tactic:
intro a

Goal state after:
case refine_2
α : Type u_1
S : Set (Set α)
cond : FiniteInter S
F : Finset (Set α)
a : Set α
⊢ ∀ (s : Finset (Set α)), a ∉ s → (↑s ⊆ S → ⋂₀ ↑s ∈ S) → ↑(insert a s) ⊆ S → ⋂₀ ↑(insert a s) ∈ S
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: p : ℕ
hp : Prime p
n : ℕ
⊢ ∀ x < p ^ (n + 1), ¬p ∣ x ↔ ∀ (x_1 : ℕ), ¬(x_1 < p ^ n ∧ x_1 * p = x)

Tactic:
intro a

Goal state after:
p : ℕ
hp : Prime p
n a : ℕ
⊢ a < p ^ (n + 1) → (¬p ∣ a ↔ ∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = a))
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: β : Type u_4
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
⊢ ∀ (N : ℕ), ∃ n ≥ N, ∀ k < n, u k < u n

Tactic:
by
  intro N
  obtain ⟨k : ℕ, - : k ≤ N, hku : ∀ l ≤ N, u l ≤ u k⟩ : ∃ k ≤ N, ∀ l ≤ N, u l ≤ u k :=
    exists_max_image _ u (finite_le_nat N) ⟨N, le_refl N⟩
  have ex : ∃ n ≥ N, u k < u n := exists_lt_of_tendsto_atTop hu _ _
  obtain ⟨n : ℕ, hnN : n ≥ N, hnk : u k < u n, hn_min : ∀ m, m < n → N ≤ m → u m ≤ u k⟩ :
      ∃ n ≥ N, u k < u n ∧ ∀ m, m < n → N ≤ m → u m ≤ u k := by
    rcases Nat.findX ex with ⟨n, ⟨hnN, hnk⟩, hn_min⟩
    push Not at hn_min
    exact ⟨n, hnN, hnk, hn_min⟩
  use n, hnN
  grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
f : ι → Filter α
g : Set α → Set β
hg : ∀ {s t : Set α}, g (s ∩ t) = g s ∩ g t
hg' : g univ = univ
⊢ (𝓟 ∘ g) univ = ⊤

Tactic:
rw [Function.comp_apply, hg', principal_univ]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
⊢ frontier (s ∪ t) ⊆ frontier s ∩ closure tᶜ ∪ closure sᶜ ∩ frontier t

Tactic:
simpa only [frontier_compl, ← compl_union] using frontier_inter_subset sᶜ tᶜ

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 : α
⊢ toIcoMod hp 0 (b - a) + toIocMod hp 0 (a - b) = p

Tactic:
toIcoMod_add_toIocMod_zero

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ p = p
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ : α
h✝ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃
x₂' : α := toIcoMod hp x₁ x₂
x₃' : α := toIcoMod hp x₂' x₃
h : x₂' ≤ toIocMod hp x₁ x₃'
h₂₁ : x₂' < x₁ + p
h₃₂ : x₃' - p < x₂'
h₃₁ : x₃' ≤ x₁ + p
⊢ x₁ + p ≤ x₂' + p

Tactic:
by simp [x₂', left_le_toIcoMod]

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 c : α
this : min (toIcoMod hp 0 (a - b) + toIocMod hp 0 (b - c)) (toIcoMod hp 0 (c - b) + toIocMod hp 0 (b - a)) ≤ p
⊢ toIcoMod hp b a ≤ toIocMod hp b c ∨ toIcoMod hp b c ≤ toIocMod hp b a

Tactic:
min_le_iff

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
this : toIcoMod hp 0 (a - b) + toIocMod hp 0 (b - c) ≤ p ∨ toIcoMod hp 0 (c - b) + toIocMod hp 0 (b - a) ≤ p
⊢ toIcoMod hp b a ≤ toIocMod hp b c ∨ toIcoMod hp b c ≤ toIocMod hp b a
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : β → γ
f : α → β
s : Set β
hg : ContinuousOn g s
hf : Continuous[inst✝², inst✝¹] f
hs : ∀ (x : α), f x ∈ s
⊢ Continuous[inst✝², inst✝] (g ∘ f)

Tactic:
rw [← continuousOn_univ] at *
  exact hg.comp hf fun x _ => hs x

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
s : Set (α × β)
x : α × β
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt (fun x_1 ↦ f (x.1, x_1)) {b | (x.1, b) ∈ s} x.2

Tactic:
rw [← x.eta]; simp_rw [ContinuousWithinAt, nhdsWithin, nhds_prod_eq, nhds_discrete, pure_prod,
    ← map_inf_principal_preimage]; rfl

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
b : Set (Set α)
hb : IsTopologicalBasis b
s : Set α
⊢ (∀ (x : α), ∀ o ∈ b, x ∈ o → (o ∩ s).Nonempty) ↔ ∀ o ∈ b, o.Nonempty → (o ∩ s).Nonempty

Tactic:
exact ⟨fun h o hb ⟨a, ha⟩ => h a o hb ha, fun h a o hb ha => h o hb ⟨a, ha⟩⟩

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

Goal state before:
pp: X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
hf : IsInducing f
hg : IsInducing g
hFg : Disjoint (closure[inst✝] (range f)) (range g)
hfG : Disjoint (range f) (closure[inst✝] (range g))
⊢ IsInducing (Sum.elim f g)

Tactic:
by
  rw [← disjoint_principal_nhdsSet] at hFg
  rw [← disjoint_nhdsSet_principal] at hfG
  rw [isInducing_iff_nhds]
  intro x
  apply le_antisymm ((hf.continuous.sumElim hg.continuous).tendsto x).le_comap
  obtain x | x := x <;>
  simp only [comap_sumElim_eq, nhds_inl, nhds_inr, elim_inl, elim_inr, ← hf.nhds_eq_comap,
    ← hg.nhds_eq_comap, sup_le_iff, le_rfl, true_and, and_true] <;>
  convert! bot_le (α := Filter (X ⊕ Y)) <;>
  rw [map_eq_bot_iff, comap_eq_bot_iff_compl_range]
  · rw [← disjoint_principal_right]
    exact hfG.mono_left (nhds_le_nhdsSet (mem_range_self x))
  · rw [← disjoint_principal_left]
    exact hFg.mono_right (nhds_le_nhdsSet (mem_range_self x))

Goal state after: