mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Subobject.Limits

Goal state before:
pp: case refine_2
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
⊢ (equalizerSubobject f g).Factors ((equalizerSubobject (h ≫ f) (h ≫ g)).arrow ≫ h)

Tactic:
apply equalizerSubobject_factors

Goal state after:
case refine_2
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
⊢ ((equalizerSubobject (h ≫ f) (h ≫ g)).arrow ≫ h) ≫ f = ((equalizerSubobject (h ≫ f) (h ≫ g)).arrow ≫ h) ≫ g
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✝¹ : HasImages C
inst✝ : HasBinaryCoproducts C
A : C
f g : MonoOver A
⊢ coprod.inl ≫
      factorThruImage ((Functor.uncurry.obj Over.coprod).obj (((forget A).prod (forget A)).obj (f, g))).hom ≫
        ((sup.obj f).obj g).arrow =
    f.arrow

Tactic:
image.fac,

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
inst✝ : HasBinaryCoproducts C
A : C
f g : MonoOver A
⊢ coprod.inl ≫ ((Functor.uncurry.obj Over.coprod).obj (((forget A).prod (forget A)).obj (f, g))).hom = f.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✝¹ : HasImages C
inst✝ : HasBinaryCoproducts C
A : C
f g : MonoOver A
⊢ coprod.inr ≫
      factorThruImage ((Functor.uncurry.obj Over.coprod).obj (((forget A).prod (forget A)).obj (f, g))).hom ≫
        ((sup.obj f).obj g).arrow =
    g.arrow

Tactic:
image.fac,

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
inst✝ : HasBinaryCoproducts C
A : C
f g : MonoOver A
⊢ coprod.inr ≫ ((Functor.uncurry.obj Over.coprod).obj (((forget A).prod (forget A)).obj (f, g))).hom = g.arrow
Module: Mathlib.CategoryTheory.Subobject.Limits

Goal state before:
pp: case refine_1
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f✝ : X✝ ⟶ Y
inst✝¹ : HasKernel f✝
inst✝ : HasKernels C
X : C
A B : Cᵒᵖ
f : A ⟶ op X
g : B ⟶ op X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ kernel.ι f.unop ≫ g.unop = 0

Tactic:
rw [← Subobject.ofMkLEMk_comp h, unop_comp, kernel.condition_assoc, zero_comp]

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
cg : KernelFork S.g
hg : IsLimit cg
cf : CokernelCofork S.f
hf : IsColimit cf
e₁ : (Fork.ofι (kernel.ι S.g) ⋯).pt ≅ cg.pt := (kernelIsKernel S.g).conePointUniqueUpToIso hg
e₂ : (Cofork.ofπ (cokernel.π S.f) ⋯).pt ≅ cf.pt := (cokernelIsCokernel S.f).coconePointUniqueUpToIso hf
eq₁ : ((kernelIsKernel S.g).conePointUniqueUpToIso hg).inv ≫ kernel.ι S.g = Fork.ι cg
eq₂ : cokernel.π S.f ≫ ((cokernelIsCokernel S.f).coconePointUniqueUpToIso hf).hom = Cofork.π cf
⊢ (((kernelIsKernel S.g).conePointUniqueUpToIso hg).inv ≫ kernel.ι S.g) ≫ Cofork.π cf =
    e₁.inv ≫ kernel.ι S.g ≫ cokernel.π S.f ≫ e₂.hom

Tactic:
← eq₂,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
cg : KernelFork S.g
hg : IsLimit cg
cf : CokernelCofork S.f
hf : IsColimit cf
e₁ : (Fork.ofι (kernel.ι S.g) ⋯).pt ≅ cg.pt := (kernelIsKernel S.g).conePointUniqueUpToIso hg
e₂ : (Cofork.ofπ (cokernel.π S.f) ⋯).pt ≅ cf.pt := (cokernelIsCokernel S.f).coconePointUniqueUpToIso hf
eq₁ : ((kernelIsKernel S.g).conePointUniqueUpToIso hg).inv ≫ kernel.ι S.g = Fork.ι cg
eq₂ : cokernel.π S.f ≫ ((cokernelIsCokernel S.f).coconePointUniqueUpToIso hf).hom = Cofork.π cf
⊢ (((kernelIsKernel S.g).conePointUniqueUpToIso hg).inv ≫ kernel.ι S.g) ≫
      cokernel.π S.f ≫ ((cokernelIsCokernel S.f).coconePointUniqueUpToIso hf).hom =
    e₁.inv ≫ kernel.ι S.g ≫ cokernel.π S.f ≫ e₂.hom
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : F.Faithful
S : ShortComplex C
hS : (S.map F).Exact
⊢ S.Exact

Tactic:
rw [ShortComplex.exact_iff_kernel_ι_comp_cokernel_π_zero] at hS ⊢

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : F.Faithful
S : ShortComplex C
hS : kernel.ι (S.map F).g ≫ cokernel.π (S.map F).f = 0
⊢ kernel.ι S.g ≫ cokernel.π S.f = 0
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
⊢ HasBinaryCoproduct (op A) (op B)

Tactic:
change HasCoproduct _

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
⊢ HasCoproduct fun j ↦ WalkingPair.casesOn j (op A) (op B)
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
⊢ (prod.lift coprod.inl.unop coprod.inr.unop).op ≫ coprod.desc prod.fst.op prod.snd.op = 𝟙 (op (A ⨯ B))

Tactic:
apply Quiver.Hom.unop_inj
    ext <;>
    · simp only
      apply Quiver.Hom.op_inj
      simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
α : Type w
inst✝² : HasFiniteCoproducts C
inst✝¹ : HasColimitsOfShape (Finset (Discrete α)) C
inst✝ : HasColimitsOfShape (Discrete α) C
X✝ Y✝ : Discrete α ⥤ C
β : X✝ ⟶ Y✝
J : Finset (Discrete α)
j : ↥J
⊢ Sigma.ι (fun x ↦ X✝.obj ↑x) j ≫
      colimit.ι ((liftToFinset C α).obj X✝) J ≫
        colimMap ((liftToFinset C α).map β) ≫ (colimit.isoColimitCocone (liftToFinsetColimitCocone Y✝)).inv =
    Sigma.ι (fun x ↦ X✝.obj ↑x) j ≫
      colimit.ι ((liftToFinset C α).obj X✝) J ≫
        (colimit.isoColimitCocone (liftToFinsetColimitCocone X✝)).inv ≫ colimMap β

Tactic:
simp [liftToFinset, liftToFinsetColimIso_aux, liftToFinsetColimIso_aux_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
s : yoneda.obj X ⟶ A
p : OverArrows (yonedaCollectionPresheafToA F) s
⊢ YonedaCollection.fst p.val = s

Tactic:
by
  simpa [YonedaCollection.yonedaEquivFst_eq] using p.app_val

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

Goal state before:
pp: C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} 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' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
α : F₀ ⟶ L ⋙ F₁
inst✝ : F₁.IsLeftKanExtension α
F₂ : D' ⥤ H
L'' : C ⥤ D'
e : L ⋙ L' ≅ L''
β : F₁ ⟶ L' ⋙ F₂
γ : F₀ ⟶ L'' ⋙ F₂
hγ : α ≫ L.whiskerLeft β ≫ (L.associator L' F₂).inv ≫ whiskerRight e.hom F₂ = γ
Ψ : (L ⋙ L').LeftExtension F₀ ≌ L''.LeftExtension F₀ := leftExtensionEquivalenceOfIso₁ e F₀
hα : StructuredArrow.IsUniversal (LeftExtension.mk F₁ α)
x✝ : F₂.IsLeftKanExtension β
h : StructuredArrow.IsUniversal (LeftExtension.mk F₂ β)
this : StructuredArrow.IsUniversal ((LeftExtension.precomp₂ L' α).obj (LeftExtension.mk F₂ β))
⊢ StructuredArrow.hom ((LeftExtension.precomp₂ L' α).obj (LeftExtension.mk F₂ β)) ≫
      ((whiskeringLeft C D' H).obj (L ⋙ L')).map
        (NatIso.ofComponents
            (fun x ↦
              Iso.refl ((StructuredArrow.right ((LeftExtension.precomp₂ L' α).obj (LeftExtension.mk F₂ β))).obj x))
            ⋯).hom =
    StructuredArrow.hom (Ψ.inverse.obj (LeftExtension.mk F₂ γ))

Tactic:
ext x
        simp [Ψ, ← congr_app hγ x, ← Functor.map_comp]

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'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
inst✝ : F'.IsRightKanExtension α
c : Cone F
hc : IsLimit c
s : Cone F'
⊢ ∀ (j : D), hc.lift { pt := s.1, π := L.whiskerLeft s.π ≫ α } ≫ (F'.coneOfIsRightKanExtension α c).π.app j = s.π.app j

Tactic:
have : (Functor.const _).map (hc.lift (Cone.mk _ (whiskerLeft L s.π ≫ α))) ≫
        F'.liftOfIsRightKanExtension α ((const D).obj c.pt) c.π = s.π :=
      F'.hom_ext_of_isRightKanExtension α _ _ (by cat_disch)

Goal state after:
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
α : L ⋙ F' ⟶ F
inst✝ : F'.IsRightKanExtension α
c : Cone F
hc : IsLimit c
s : Cone F'
this :
  (const D).map (hc.lift { pt := s.1, π := L.whiskerLeft s.π ≫ α }) ≫
      F'.liftOfIsRightKanExtension α ((const D).obj c.pt) c.π =
    s.π
⊢ ∀ (j : D), hc.lift { pt := s.1, π := L.whiskerLeft s.π ≫ α } ≫ (F'.coneOfIsRightKanExtension α c).π.app j = s.π.app j
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
this✝⁴ : HasFiniteLimits C
this✝³ : HasProductsOfShape (Subtype P) C
this✝² : ∀ (A : C), HasProductsOfShape (StructuredArrow A P.ι) C
this✝¹ : CompleteLattice (Subobject (∏ᶜ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ᶜ Subtype.val))
this✝ : ∀ (X : C) [inst : HasProduct (P.productToFamily X)], Mono (P.productTo X)
A : C
f g : Subobject.underlying.obj ⊥ ⟶ A
this : IsSplitEpi (equalizer.ι f g)
⊢ f = g

Tactic:
by exact eq_of_epi_equalizer

Goal state after:
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
iX : limit X ≅ AddCommGrpCat.of ((i : J) → ↑(X.obj { as := i })) :=
  (Pi.isoLimit X).symm ≪≫
    (limit.isLimit (Discrete.functor fun j ↦ X.obj { as := j })).conePointUniqueUpToIso
      (AddCommGrpCat.HasLimit.productLimitCone fun j ↦ X.obj { as := j }).isLimit
iY : limit Y ≅ AddCommGrpCat.of ((i : J) → ↑(Y.obj { as := i })) :=
  (Pi.isoLimit Y).symm ≪≫
    (limit.isLimit (Discrete.functor fun j ↦ Y.obj { as := j })).conePointUniqueUpToIso
      (AddCommGrpCat.HasLimit.productLimitCone fun j ↦ Y.obj { as := j }).isLimit
this :
  (Pi.map fun i ↦ ⇑(ConcreteCategory.hom (f.app { as := i }))) = ⇑(ConcreteCategory.hom (iX.inv ≫ lim.map f ≫ iY.hom))
⊢ Function.Surjective (Pi.map fun i ↦ ⇑(ConcreteCategory.hom (f.app { as := i })))

Tactic:
simp_rw [CategoryTheory.NatTrans.epi_iff_epi_app, AddCommGrpCat.epi_iff_surjective] at hf

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
X Y : Discrete J ⥤ AddCommGrpCat
f : X ⟶ Y
iX : limit X ≅ AddCommGrpCat.of ((i : J) → ↑(X.obj { as := i })) :=
  (Pi.isoLimit X).symm ≪≫
    (limit.isLimit (Discrete.functor fun j ↦ X.obj { as := j })).conePointUniqueUpToIso
      (AddCommGrpCat.HasLimit.productLimitCone fun j ↦ X.obj { as := j }).isLimit
iY : limit Y ≅ AddCommGrpCat.of ((i : J) → ↑(Y.obj { as := i })) :=
  (Pi.isoLimit Y).symm ≪≫
    (limit.isLimit (Discrete.functor fun j ↦ Y.obj { as := j })).conePointUniqueUpToIso
      (AddCommGrpCat.HasLimit.productLimitCone fun j ↦ Y.obj { as := j }).isLimit
this :
  (Pi.map fun i ↦ ⇑(ConcreteCategory.hom (f.app { as := i }))) = ⇑(ConcreteCategory.hom (iX.inv ≫ lim.map f ≫ iY.hom))
hf : ∀ (k : Discrete J), Function.Surjective ⇑(ConcreteCategory.hom (f.app k))
⊢ Function.Surjective (Pi.map fun i ↦ ⇑(ConcreteCategory.hom (f.app { as := i })))
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: case mpr.refine_3
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
x : (pair X Y).obj { as := right }
y : X
e : (ConcreteCategory.hom c.inl) y = (ConcreteCategory.hom c.inr) x
⊢ (ConcreteCategory.hom f)
      ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inl)) h₁).symm ⟨(ConcreteCategory.hom c.inr) x, ⋯⟩) =
    (ConcreteCategory.hom g) x

Tactic:
have : c.inr x ∈ Set.range c.inl ⊓ Set.range c.inr := ⟨⟨_, e⟩, ⟨_, rfl⟩⟩

Goal state after:
case mpr.refine_3
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
x : (pair X Y).obj { as := right }
y : X
e : (ConcreteCategory.hom c.inl) y = (ConcreteCategory.hom c.inr) x
this :
  (ConcreteCategory.hom c.inr) x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) ⊓ Set.range ⇑(ConcreteCategory.hom c.inr)
⊢ (ConcreteCategory.hom f)
      ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inl)) h₁).symm ⟨(ConcreteCategory.hom c.inr) x, ⋯⟩) =
    (ConcreteCategory.hom g) x
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 s _ h1 h2
    suffices a ∩ ⋂₀ ↑s ∈ S by simpa
    exact
      cond.inter_mem (h2 (Finset.mem_insert_self a s))
        (h1 fun x hx => h2 <| Finset.mem_insert_of_mem hx)

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

Goal state before:
pp: p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x ↦ x * p
h2 : image (fun x ↦ x * p) (range (p ^ n)) ⊆ range (p ^ (n + 1))
⊢ p ^ (n + 1) - p ^ n = p ^ n * (p - 1)

Tactic:
←
        one_mul (p ^ n),

Goal state after:
p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x ↦ x * p
h2 : image (fun x ↦ x * p) (range (p ^ n)) ⊆ range (p ^ (n + 1))
⊢ p ^ (n + 1) - 1 * p ^ n = 1 * p ^ n * (p - 1)
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: α : Type u_3
f : Filter α
s : ℕ → Set α
hs : f.HasAntitoneBasis s
r : ℕ → ℕ → Prop
hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n
φ : ℕ → ℕ
hφ : StrictMono φ
hrφ : ∀ (m n : ℕ), m < n → r (φ m) (φ n)
⊢ ∃ φ, StrictMono φ ∧ (∀ ⦃m n : ℕ⦄, m < n → r (φ m) (φ n)) ∧ f.HasAntitoneBasis (s ∘ φ)

Tactic:
exact ⟨φ, hφ, hrφ, hs.comp_strictMono hφ⟩

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

Goal state before:
pp: p k : ℕ
hp : Prime p
hk : 0 < k
h : p ^ (k - 1) ≤ k * (p ^ (k - 1) * (p - 1))
⊢ (p ^ k) ^ (p ^ (k - 1) * (p - 1)) / p ^ p ^ (k - 1) = p ^ (p ^ (k - 1) * ((p - 1) * k - 1))

Tactic:
← pow_mul

Goal state after:
p k : ℕ
hp : Prime p
hk : 0 < k
h : p ^ (k - 1) ≤ k * (p ^ (k - 1) * (p - 1))
⊢ p ^ (k * (p ^ (k - 1) * (p - 1))) / p ^ p ^ (k - 1) = p ^ (p ^ (k - 1) * ((p - 1) * k - 1))
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 : α
⊢ (c ∈ Set.Ico a (a + p) ∧ ∃ z, b = c + z • p) → toIcoMod hp a b = c

Tactic:
← @sub_eq_iff_eq_add

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ (c ∈ Set.Ico a (a + p) ∧ ∃ z, b - z • p = c) → toIcoMod hp a b = c
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 : α
⊢ (c ∈ Set.Ioc a (a + p) ∧ ∃ z, b = c + z • p) → toIocMod hp a b = c

Tactic:
← @sub_eq_iff_eq_add

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ (c ∈ Set.Ioc a (a + p) ∧ ∃ z, b - z • p = c) → toIocMod hp a b = c
Module: Mathlib.Algebra.Order.ToIntervalMod

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

Tactic:
by
  refine toIocDiv_eq_of_sub_zsmul_mem_Ioc _ ?_
  rw [sub_smul, ← sub_add, add_right_comm]
  simpa using sub_toIocDiv_zsmul_mem_Ioc hp a b

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 - p) = toIocDiv hp a b - 1

Tactic:
simpa only [one_zsmul] using toIocDiv_sub_zsmul hp a b 1

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

Tactic:
apply toIocDiv_eq_of_sub_zsmul_mem_Ioc

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ b - c - toIocDiv hp (a + c) b • p ∈ Set.Ioc a (a + 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
a b : α
⊢ toIocDiv hp (-(a + p)) b = -toIcoDiv hp a (-b)

Tactic:
apply toIocDiv_eq_of_sub_zsmul_mem_Ioc

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ b - -toIcoDiv hp a (-b) • p ∈ Set.Ioc (-(a + p)) (-(a + p) + p)
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: case refine_2
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
z : ℤ
hz : c = z • p + b
⊢ toIcoMod hp a b = toIcoMod hp a c

Tactic:
hz,

Goal state after:
case refine_2
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
z : ℤ
hz : c = z • p + b
⊢ toIcoMod hp a b = toIcoMod hp a (z • p + b)
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: case refine_2
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
z : ℤ
hz : c = z • p + b
⊢ toIocMod hp a b = toIocMod hp a c

Tactic:
hz,

Goal state after:
case refine_2
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
z : ℤ
hz : c = z • p + b
⊢ toIocMod hp a b = toIocMod hp a (z • p + b)
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ x ∈ closure[inst✝] s ↔ (comap Subtype.val (𝓝 x)).NeBot

Tactic:
mem_closure_iff_nhds,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ (∀ t ∈ 𝓝 x, (t ∩ s).Nonempty) ↔ (comap Subtype.val (𝓝 x)).NeBot
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a ≤ b - toIcoDiv hp a b • p
hr : b - toIcoDiv hp a b • p < a + p
⊢ ∃ i, b ∈ Ico (a + i • p) (a + (i + 1) • p)

Tactic:
refine ⟨toIcoDiv hp a b, ⟨le_sub_iff_add_le.mp hl, ?_⟩⟩

Goal state after:
α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a ≤ b - toIcoDiv hp a b • p
hr : b - toIcoDiv hp a b • p < a + p
⊢ b < a + (toIcoDiv hp a b + 1) • p
Module: Mathlib.Topology.Separation.SeparatedNhds

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hst' : IsOpen[inst✝] (s ∪ t)
u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hsu : s ⊆ u
htv : t ⊆ v
huv : Disjoint u v
⊢ s = (s ∪ t) ∩ u

Tactic:
rw [union_inter_distrib_right, (huv.symm.mono_left htv).inter_eq, union_empty,
    inter_eq_left.2 hsu]

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 : IsOpenMap f
x : X
l : Filter Y
h : ClusterPt (f x) l
⊢ (map ?f (𝓝 x ⊓ comap f l)).NeBot

pp: case f
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenMap f
x : X
l : Filter Y
h : ClusterPt (f x) l
⊢ X → ?m.18

pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenMap f
x : X
l : Filter Y
h : ClusterPt (f x) l
⊢ Type ?u.31

Tactic:
Filter.push_pull

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenMap f
x : X
l : Filter Y
h : ClusterPt (f x) l
⊢ (map f (𝓝 x) ⊓ l).NeBot
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
⊢ u ×ˢ ⋃₀ t = Prod.fst ⁻¹' u

Tactic:
ht,

Goal state after:
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
⊢ u ×ˢ univ = Prod.fst ⁻¹' u
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
Y : Type v
Z : Type u_1
W : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : IndiscreteTopology X
hY : IndiscreteTopology Y
⊢ induced fst inst✝¹ = ⊤ ∧ induced snd inst✝ = ⊤

Tactic:
by simp [h.eq_top, hY.eq_top]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: ι : Type u_5
X : ι → Type u_6
inst✝ : (i : ι) → TopologicalSpace (X i)
I : Set ι
s : (i : ι) → Set (X i)
x : (i : ι) → X i
⊢ 𝓝[I.pi s] x = ⊥ ↔ ∃ i ∈ I, 𝓝[s i] x i = ⊥

Tactic:
simp only [nhdsWithin, nhds_pi, pi_inf_principal_pi_eq_bot]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
𝔖 : Set (Set ι)
⊢ induced (⋃₀ 𝔖).domRestrict topologicalSpace = ⨅ S ∈ 𝔖, induced S.domRestrict topologicalSpace

Tactic:
Pi.induced_domRestrict,

Goal state after:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
𝔖 : Set (Set ι)
⊢ ⨅ i ∈ ⋃₀ 𝔖, induced (eval i) (T i) = ⨅ S ∈ 𝔖, ⨅ i ∈ S, induced (eval i) (T i)
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case refine_1.refine_2
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
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
⊢ ((↑I).pi fun a_1 ↦ eval a_1 '' (↑I).pi fun a_2 ↦ ⋯.choose) ⊆ s

Tactic:
exact Subset.trans
        (pi_mono fun i hi => (eval_image_pi_subset hi).trans (h1 i).choose_spec.1) h2

Goal state after: