mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M : (Spec R).Modules
V : (Spec R).Opens
ι : Type u_1
inst✝ : Finite ι
g : ι → ↑R
hg : V = ⨆ i, basicOpen (g i)
h₁ : ∀ (i : ι), Aux M (basicOpen (g i))
h₂ : ∀ (i j : ι), Aux M (basicOpen (g i * g j))
hgle : ∀ (i : ι), basicOpen (g i) ≤ V
hug : ∀ (i : ι) (m : ℕ), IsUnit ((algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ m))
f : ↑R
hf : basicOpen f ≤ V
s : ↑Γ(M, basicOpen f)
hfgi : ∀ (i : ι), basicOpen (f * g i) ≤ basicOpen (g i)
s' : (i : ι) → ↑Γ(M, basicOpen (f * g i)) := fun i ↦ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) s
n : ι → ℕ
t' : (i : ι) → ↑Γ(M, basicOpen (g i))
ht' : ∀ (i : ι), f ^ n i • s' i = (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t' i)
this : ∀ (i : ι), n i ≤ ⨆ i, n i
hN : ∀ (i : ι), ⨆ i, n i = (⨆ i, n i) - n i + n i
i : ι
⊢ (f ^ ⨆ i, n i) • s' i =
    (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) ((fun i ↦ f ^ ((⨆ i, n i) - n i) • t' i) i)

Tactic:
conv_lhs => rw [hN i]

Goal state after:
R : CommRingCat
M : (Spec R).Modules
V : (Spec R).Opens
ι : Type u_1
inst✝ : Finite ι
g : ι → ↑R
hg : V = ⨆ i, basicOpen (g i)
h₁ : ∀ (i : ι), Aux M (basicOpen (g i))
h₂ : ∀ (i j : ι), Aux M (basicOpen (g i * g j))
hgle : ∀ (i : ι), basicOpen (g i) ≤ V
hug : ∀ (i : ι) (m : ℕ), IsUnit ((algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ m))
f : ↑R
hf : basicOpen f ≤ V
s : ↑Γ(M, basicOpen f)
hfgi : ∀ (i : ι), basicOpen (f * g i) ≤ basicOpen (g i)
s' : (i : ι) → ↑Γ(M, basicOpen (f * g i)) := fun i ↦ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) s
n : ι → ℕ
t' : (i : ι) → ↑Γ(M, basicOpen (g i))
ht' : ∀ (i : ι), f ^ n i • s' i = (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t' i)
this : ∀ (i : ι), n i ≤ ⨆ i, n i
hN : ∀ (i : ι), ⨆ i, n i = (⨆ i, n i) - n i + n i
i : ι
⊢ f ^ ((⨆ i, n i) - n i + n i) • s' i =
    (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) ((fun i ↦ f ^ ((⨆ i, n i) - n i) • t' i) i)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↑(Proj.restrict ⋯).toTopCat
z : NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ ¬IsUnit ((mapId 𝒜 ⋯) (HomogeneousLocalization.mk z)) ↔
    HomogeneousLocalization.mk z ∈ ProjIsoSpecTopComponent.ToSpec.carrier x

Tactic:
rw [← HomogeneousLocalization.isUnit_iff_isUnit_val,
    ProjIsoSpecTopComponent.ToSpec.mk_mem_carrier, HomogeneousLocalization.map_mk,
    HomogeneousLocalization.val_mk, Localization.mk_eq_mk',
    IsLocalization.AtPrime.isUnit_mk'_iff]

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↑(Proj.restrict ⋯).toTopCat
z : NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ ↑{ deg := z.deg, num := ⟨(GradedRingHom.id 𝒜) ↑z.num, ⋯⟩, den := ⟨(GradedRingHom.id 𝒜) ↑z.den, ⋯⟩,
            den_mem := ⋯ }.num ∉
      (↑x).asHomogeneousIdeal.toIdeal.primeCompl ↔
    ↑z.num ∈ (↑x).asHomogeneousIdeal
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: P : MorphismProperty Scheme
S : Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
⊢ overGrothendieckTopology P S = (overPretopology P S).toGrothendieck

Tactic:
ext X R
  rw [GrothendieckTopology.mem_over_iff]
  constructor
  · intro hR
    obtain ⟨𝒰, hle⟩ := exists_cover_of_mem_grothendieckTopology hR
    rw [mem_grothendieckTopology_iff] at hR
    let (i : 𝒰.I₀) : (𝒰.X i).Over S := { hom := 𝒰.f i ≫ X.hom }
    let : 𝒰.Over S :=
      { over := inferInstance
        isOver_map := fun i ↦ ⟨rfl⟩ }
    use 𝒰.toPresieveOver, ⟨𝒰, inferInstance, rfl⟩
    rwa [Cover.toPresieveOver_le_arrows_iff]
  · rintro ⟨T, ⟨𝒰, h, rfl⟩, hT⟩
    rw [mem_grothendieckTopology_iff]
    use 𝒰
    rwa [Cover.toPresieveOver_le_arrows_iff] at hT

Goal state after:
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsSeparated f
S : ValuativeCommSq f
l₁ : Spec (CommRingCat.of S.R) ⟶ X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₁ = S.i₁
hl₁' : l₁ ≫ f = S.i₂
l₂ : Spec (CommRingCat.of S.R) ⟶ X
hl₂ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₂ = S.i₁
hl₂' : l₂ ≫ f = S.i₂
h : l₁ ≫ f = l₂ ≫ f
Z : Scheme := pullback (pullback.diagonal f) (pullback.lift l₁ l₂ h)
g : Z ⟶ Spec (CommRingCat.of S.R) := pullback.snd (pullback.diagonal f) (pullback.lift l₁ l₂ h)
this : IsClosedImmersion g
hZ : IsAffine Z
l : Spec (CommRingCat.of S.K) ⟶ Z := pullback.lift S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) ⋯
hg : l ≫ g = Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))
⊢ Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)))))

Tactic:
let e := arrowIsoΓSpecOfIsAffine (CommRingCat.ofHom <| algebraMap S.R S.K)

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsSeparated f
S : ValuativeCommSq f
l₁ : Spec (CommRingCat.of S.R) ⟶ X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₁ = S.i₁
hl₁' : l₁ ≫ f = S.i₂
l₂ : Spec (CommRingCat.of S.R) ⟶ X
hl₂ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₂ = S.i₁
hl₂' : l₂ ≫ f = S.i₂
h : l₁ ≫ f = l₂ ≫ f
Z : Scheme := pullback (pullback.diagonal f) (pullback.lift l₁ l₂ h)
g : Z ⟶ Spec (CommRingCat.of S.R) := pullback.snd (pullback.diagonal f) (pullback.lift l₁ l₂ h)
this : IsClosedImmersion g
hZ : IsAffine Z
l : Spec (CommRingCat.of S.K) ⟶ Z := pullback.lift S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) ⋯
hg : l ≫ g = Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))
e : Arrow.mk (CommRingCat.ofHom (algebraMap S.R S.K)) ≅
  Arrow.mk (Scheme.Hom.appTop (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)))) :=
  arrowIsoΓSpecOfIsAffine (CommRingCat.ofHom (algebraMap S.R S.K))
⊢ Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)))))
Module: Mathlib.CategoryTheory.Generator.Presheaf

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasCoproducts A
X : C
M : A
F G : Cᵒᵖ ⥤ A
α : M ⟶ F.obj (op X)
f : F ⟶ G
⊢ freeYonedaHomEquiv.symm α ≫ f = freeYonedaHomEquiv.symm (α ≫ f.app (op X))

Tactic:
apply freeYonedaHomEquiv.injective
  simp only [freeYonedaHomEquiv_comp, Equiv.apply_symm_apply]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.SubcanonicalOver

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X : C
E Z✝ : Over X
ι : Type (max u_1 v_1)
T : ι → Over X
g : (i : ι) → T i ⟶ Z✝
hR : Sieve.ofArrows T g ∈ (J.over X) Z✝
t : Presieve.FamilyOfElements (CategoryTheory.yoneda.obj E) (Sieve.ofArrows T g).arrows
ht : t.Compatible
i j : ι
Z : C
gi : Z ⟶ (T i).left
gj : Z ⟶ (T j).left
hgij : gi ≫ (fun i ↦ Over.Hom.left (g i)) i = gj ≫ (fun i ↦ Over.Hom.left (g i)) j
⊢ gj ≫ (T j).hom = (Over.mk (gi ≫ (T i).hom)).hom

Tactic:
dsimp; rw [← Over.w (g i), reassoc_of% hgij, ← Over.w (g j)]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : Type u'
inst✝⁴ : Category.{v', u'} J
X : J ⥤ C
inst✝³ : ∀ (j j' : J) (φ : j ⟶ j'), Mono (X.map φ)
c : Cocone X
hc : IsColimit c
inst✝² : IsFiltered J
j₀ : J
inst✝¹ : HasColimitsOfShape (Under j₀) C
inst✝ : colim.PreservesMonomorphisms
⊢ Mono (c.ι.app j₀)

Tactic:
let f : (Functor.const _).obj (X.obj j₀) ⟶ Under.forget j₀ ⋙ X :=
    { app j := X.map j.hom
      naturality _ _ g := by
        dsimp
        simp only [Category.id_comp, ← X.map_comp, Under.w] }
  have := NatTrans.mono_of_mono_app f
  exact colim.map_mono' f (isColimitConstCocone _ _)
    ((Functor.Final.isColimitWhiskerEquiv _ _).symm hc) (c.ι.app j₀) (by cat_disch)

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X X' : C
f : X' ⟶ X
F : Sheaf J (Type v)
x : F.obj.obj (op X)
⊢ J.yoneda.map f ≫ J.yonedaEquiv.symm x = J.yonedaEquiv.symm ((ConcreteCategory.hom (F.obj.map f.op)) x)

Tactic:
by
  apply J.yonedaEquiv.injective
  rw [yonedaEquiv_comp, yonedaEquiv_yoneda_map]
  simp
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : Cᵒᵖ
F : Sheaf J (Type (max v v'))
f : (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F
g : X ⟶ Y
⊢ (ConcreteCategory.hom (F.obj.map g)) (J.uliftYonedaEquiv f) = (ConcreteCategory.hom (f.hom.app Y)) { down := g.unop }

Tactic:
uliftYonedaEquiv_naturality',

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : Cᵒᵖ
F : Sheaf J (Type (max v v'))
f : (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F
g : X ⟶ Y
⊢ J.uliftYonedaEquiv ((uliftYoneda.{v', v, u} J).map g.unop ≫ f) =
    (ConcreteCategory.hom (f.hom.app Y)) { down := g.unop }
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : Cᵒᵖ
f : X ⟶ Y
F : Sheaf J (Type (max v v'))
u : (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F
⊢ J.uliftYonedaEquiv.symm ((ConcreteCategory.hom (F.obj.map f)) (J.uliftYonedaEquiv u)) =
    (uliftYoneda.{v', v, u} J).map f.unop ≫ J.uliftYonedaEquiv.symm (J.uliftYonedaEquiv u)

Tactic:
uliftYonedaEquiv_naturality',

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : Cᵒᵖ
f : X ⟶ Y
F : Sheaf J (Type (max v v'))
u : (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F
⊢ J.uliftYonedaEquiv.symm (J.uliftYonedaEquiv ((uliftYoneda.{v', v, u} J).map f.unop ≫ u)) =
    (uliftYoneda.{v', v, u} J).map f.unop ≫ J.uliftYonedaEquiv.symm (J.uliftYonedaEquiv u)
Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

Goal state before:
pp: case succ
C : Type u
inst✝⁵ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : WellFoundedLT J
X Y : C
f : X ⟶ Y
hf : W.TransfiniteCompositionOfShape J f
inst✝ : W.IsMultiplicative
hJ :
  ∀ (J : Type w) [inst : LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J], W.IsStableUnderColimitsOfShape J
j : J
hj : ¬IsMax j
hj' : W (hf.F.map (homOfLE ⋯))
⊢ W (hf.F.map (homOfLE ⋯) ≫ hf.F.map (homOfLE ⋯))

Tactic:
exact W.comp_mem _ _ hj' (hf.map_mem j hj)

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : WellFoundedLT J
X Y : C
f : X ⟶ Y
hf : W.TransfiniteCompositionOfShape J f
inst✝ : W.IsMultiplicative
hJ :
  ∀ (J : Type w) [inst : LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J], W.IsStableUnderColimitsOfShape J
j : J
⊢ W (hf.F.map (homOfLE ⋯))

Tactic:
induction j using SuccOrder.limitRecOn with
  | isMin j hj =>
    obtain rfl := hj.eq_bot
    simpa using W.id_mem _
  | succ j hj hj' =>
    rw [← homOfLE_comp bot_le (Order.le_succ j), hf.F.map_comp]
    exact W.comp_mem _ _ hj' (hf.map_mem j hj)
  | isSuccLimit j hj hj' =>
    let : OrderBot (Set.Iio j) :=
      { bot := ⟨⊥, Order.IsSuccLimit.bot_lt hj⟩
        bot_le j := bot_le }
    exact MorphismProperty.colimitsOfShape_le _
      (.of_isColimit (hf.F.isColimitOfIsWellOrderContinuous j hj) (fun k ↦ hj' _ k.2))

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : WellFoundedLT J
X Y : C
f : X ⟶ Y
hf : W.TransfiniteCompositionOfShape J f
inst✝ : W.IsMultiplicative
hJ :
  ∀ (J : Type w) [inst : LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J], W.IsStableUnderColimitsOfShape J
j : J
g : ⊥ ⟶ j
⊢ W (hf.F.map g)

Tactic:
obtain rfl : g = homOfLE bot_le := rfl
  induction j using SuccOrder.limitRecOn with
  | isMin j hj =>
    obtain rfl := hj.eq_bot
    simpa using W.id_mem _
  | succ j hj hj' =>
    rw [← homOfLE_comp bot_le (Order.le_succ j), hf.F.map_comp]
    exact W.comp_mem _ _ hj' (hf.map_mem j hj)
  | isSuccLimit j hj hj' =>
    let : OrderBot (Set.Iio j) :=
      { bot := ⟨⊥, Order.IsSuccLimit.bot_lt hj⟩
        bot_le j := bot_le }
    exact MorphismProperty.colimitsOfShape_le _
      (.of_isColimit (hf.F.isColimitOfIsWellOrderContinuous j hj) (fun k ↦ hj' _ k.2))

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
K : Type w
inst✝ : LinearOrder K
x : K
F G : ↑(Set.Iic x) ⥤ C
k : K
hk : k ≤ x
h : F.obj ⟨k, hk⟩ = G.obj ⟨k, hk⟩
⊢ MapEq F G k k ⋯ hk

Tactic:
rw [MapEq, arrowMap_refl, arrowMap_refl, h]

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: case succ
J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
i : J
hi : ¬IsMax i
hi' : Nonempty (d.Extension val₀ i)
⊢ Nonempty (d.Extension val₀ (Order.succ i))

Tactic:
exact ⟨hi'.some.succ hi⟩

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
f : Arrow C
j : κ.ord.ToType
this :
  𝟙 (((iterationFunctor I κ).obj j).obj f).right ≫ 𝟙 (((iterationFunctor I κ).obj j).obj f).right =
    Arrow.Hom.right (((iterationFunctor I κ).map (homOfLE ⋯)).app f) ≫
      Arrow.Hom.right (Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ f j).hom)
⊢ Arrow.Hom.right (Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ f j).hom) ≫
      Arrow.Hom.right (((iterationFunctor I κ).map (homOfLE ⋯)).app f) =
    𝟙 (((iterationFunctor I κ).obj (Order.succ j)).obj f).right

Tactic:
← cancel_epi (((iterationFunctor I κ).map (homOfLE (Order.le_succ j))).app f).right,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
f : Arrow C
j : κ.ord.ToType
this :
  𝟙 (((iterationFunctor I κ).obj j).obj f).right ≫ 𝟙 (((iterationFunctor I κ).obj j).obj f).right =
    Arrow.Hom.right (((iterationFunctor I κ).map (homOfLE ⋯)).app f) ≫
      Arrow.Hom.right (Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ f j).hom)
⊢ Arrow.Hom.right (((iterationFunctor I κ).map (homOfLE ⋯)).app f) ≫
      Arrow.Hom.right (Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ f j).hom) ≫
        Arrow.Hom.right (((iterationFunctor I κ).map (homOfLE ⋯)).app f) =
    Arrow.Hom.right (((iterationFunctor I κ).map (homOfLE ⋯)).app f) ≫
      𝟙 (((iterationFunctor I κ).obj (Order.succ j)).obj f).right
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
⊢ FiniteMultiplicity (↑p) a ↔ a ≠ 0

Tactic:
simp [Int.finiteMultiplicity_iff, hp.1.ne_one]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
G : C
inst✝ : Abelian C
hG : IsSeparator G
X : C
A : Subobject X
hA : ¬A = ⊤
⊢ ⋯.choose = largerSubobject hG A

Tactic:
by simp [largerSubobject, dif_neg hA]

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: p : ℕ
q : ℚ
hq : ¬q = 0
⊢ 0 ≤ ↑p ^ (-padicValRat p q)

Tactic:
apply zpow_nonneg

Goal state after:
p : ℕ
q : ℚ
hq : ¬q = 0
⊢ 0 ≤ ↑p
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hr : ¬r = 0
⊢ padicNorm p (q / r) * padicNorm p r = padicNorm p q

Tactic:
← padicNorm.mul,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hr : ¬r = 0
⊢ padicNorm p (q / r * r) = padicNorm p q
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: case cons
p j : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
S : Finset ℕ
hn1 : ∀ (i : ℕ), 0 < F i
s : ℕ
S' : Finset ℕ
Hnot : s ∉ S'
Hne : S'.Nonempty
Hind : (∀ i ∈ S', padicValRat p (F j) < padicValRat p (F i)) → padicValRat p (F j) < padicValRat p (∑ i ∈ S', F i)
hF : ∀ i ∈ Finset.cons s S' Hnot, padicValRat p (F j) < padicValRat p (F i)
⊢ padicValRat p (F j) < padicValRat p (∑ i ∈ Finset.cons s S' Hnot, F i)

Tactic:
rw [Finset.cons_eq_insert, Finset.sum_insert Hnot]
    exact padicValRat.lt_add_of_lt
      (ne_of_gt (add_pos (hn1 s) (Finset.sum_pos (fun i _ => hn1 i) Hne)))
      (hF _ (by simp [Finset.mem_insert, true_or]))
      (Hind (fun i hi => hF _ (by rw [Finset.cons_eq_insert, Finset.mem_insert]; exact Or.inr hi)))

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
this : ‖x‖ ≤ ↑p ^ (-↑1) ↔ x ∈ Ideal.span {↑p ^ 1}
⊢ ‖x‖ < 1 ↔ ↑p ∣ x

Tactic:
Ideal.mem_span_singleton,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
this : ‖x‖ ≤ ↑p ^ (-↑1) ↔ ↑p ^ 1 ∣ x
⊢ ‖x‖ < 1 ↔ ↑p ∣ x
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
a : ℤ
⊢ ↑(p ^ n) ∣ ↑a ↔ ↑a ∈ Ideal.span {↑p ^ n}

Tactic:
Ideal.mem_span_singleton,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
a : ℤ
⊢ ↑(p ^ n) ∣ ↑a ↔ ↑p ^ n ∣ ↑a
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: case a
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : ‖x‖ < 1
⊢ x ∈ Ideal.span {↑p}

Tactic:
Ideal.mem_span_singleton,

Goal state after:
case a
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : ‖x‖ < 1
⊢ ↑p ∣ x
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : f ≈ 0
hg : f * g ≈ 0
⊢ (f * g).norm = f.norm * g.norm

Tactic:
simp only [hf, hg, norm, dif_pos, zero_mul]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.Conservative

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝¹ : LocallySmall.{w, v, u} C
hP :
  ∀ ⦃X : C⦄ (S : Sieve X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X),
        ∃ Y g, ∃ (_ : S.arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x) →
      S ∈ J X
F₁ F₂ : Cᵒᵖ ⥤ Type w
f : F₁ ⟶ F₂
inst✝ : Mono f
hf : ∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))
this :
  ∀ {F₁ F₂ : Cᵒᵖ ⥤ Type w} (f : F₁ ⟶ F₂) [Mono f],
    (∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))) →
      (∃ U, F₂ = shrinkYoneda.{w, v, u}.obj U) → Presheaf.IsLocallySurjective J f
hF₂ : ¬∃ U, F₂ = shrinkYoneda.{w, v, u}.obj U
U : C
s : ToType (F₂.obj (op U))
f' : pullback f (shrinkYonedaEquiv.symm s) ⟶ shrinkYoneda.{w, v, u}.obj U := pullback.snd f (shrinkYonedaEquiv.symm s)
Φ : P.FullSubcategory
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f'))

Tactic:
replace hf := hf Φ

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝¹ : LocallySmall.{w, v, u} C
hP :
  ∀ ⦃X : C⦄ (S : Sieve X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X),
        ∃ Y g, ∃ (_ : S.arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x) →
      S ∈ J X
F₁ F₂ : Cᵒᵖ ⥤ Type w
f : F₁ ⟶ F₂
inst✝ : Mono f
this :
  ∀ {F₁ F₂ : Cᵒᵖ ⥤ Type w} (f : F₁ ⟶ F₂) [Mono f],
    (∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))) →
      (∃ U, F₂ = shrinkYoneda.{w, v, u}.obj U) → Presheaf.IsLocallySurjective J f
hF₂ : ¬∃ U, F₂ = shrinkYoneda.{w, v, u}.obj U
U : C
s : ToType (F₂.obj (op U))
f' : pullback f (shrinkYonedaEquiv.symm s) ⟶ shrinkYoneda.{w, v, u}.obj U := pullback.snd f (shrinkYonedaEquiv.symm s)
Φ : P.FullSubcategory
hf : Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f'))
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i ≥ N, ε ≤ (f - const (padicNorm p) (↑f i)).norm
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hne : ¬f - const (padicNorm p) (↑f i) ≈ 0
hge : ε ≤ padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint hne))
hngen : stationaryPoint hne ≤ N
⊢ padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint hne)) < ε

Tactic:
| inr hngen =>

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Projections

Goal state before:
pp: case neg
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ (P q).f (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
hqn : q ≤ n
a : ℕ
ha : q + a = n
hnaq : n = a + q
eq : φ ≫ X.δ ⟨a, ⋯⟩.succ = 0
⊢ (φ ≫ X.δ ⟨a + 1, ⋯⟩) ≫ X.σ ⟨a, ⋯⟩ = 0

Tactic:
simp only [Fin.succ_mk] at eq

Goal state after:
case neg
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ (P q).f (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
hqn : q ≤ n
a : ℕ
ha : q + a = n
hnaq : n = a + q
eq : φ ≫ X.δ ⟨a + 1, ⋯⟩ = 0
⊢ (φ ≫ X.δ ⟨a + 1, ⋯⟩) ≫ X.σ ⟨a, ⋯⟩ = 0
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case mpr
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
⊢ ↑p ∣ k → ‖↑k‖ < 1

Tactic:
· rintro ⟨x, rfl⟩
    push_cast
    rw [padicNormE.mul]
    calc
      _ ≤ ‖(p : ℚ_[p])‖ * 1 :=
        mul_le_mul le_rfl (by simpa using norm_int_le_one _) (norm_nonneg _) (norm_nonneg _)
      _ < 1 := by
        rw [mul_one, norm_p]
        exact inv_lt_one_of_one_lt₀ <| mod_cast hp.1.one_lt

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Representable

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝⁷ : HasBinaryProducts C
inst✝⁶ : HasPullbacks D
inst✝⁵ : HasBinaryProducts D
inst✝⁴ : HasTerminal D
inst✝³ : F.Full
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : HasPullbacks C
inst✝ : PreservesLimitsOfShape WalkingCospan F
X : D
h : ∀ ⦃a : C⦄ (g : F.obj a ⟶ X), F.relativelyRepresentable g
⊢ F.relativelyRepresentable (Limits.diag X)

Tactic:
rw [(by cat_disch : Limits.diag X = pullback.lift (𝟙 X) (𝟙 X) ≫ (prodIsoPullback X X).inv)]
  suffices F.relativelyRepresentable (pullback.lift (𝟙 _) (𝟙 _)) from
    (respectsIso F).toRespectsRight.postcomp _ (inferInstance : IsIso _) _ this
  intro a g
  obtain ⟨_, ⟨_, ⟨_, pbRepr⟩⟩⟩ := h (g ≫ pullback.fst _ _) (g ≫ pullback.snd _ _)
  obtain ⟨_, ⟨bot⟩⟩ := IsPullback.of_iso_pullback ⟨by rw [assoc]; simp [pullback.condition]⟩
    (pbRepr.isoPullback ≪≫ (pullbackDiagonalMapIdIso (g ≫ pullback.fst _ _) (g ≫ pullback.snd _ _)
      (terminal.from X)).symm) rfl rfl
  obtain ⟨_, ⟨_, ⟨topMap, top⟩⟩⟩ := (toPullbackTerminal g) <|
    (pbRepr.isoPullback ≪≫ (pullbackDiagonalMapIdIso (g ≫ pullback.fst _ _) (g ≫ pullback.snd _ _)
      (terminal.from X)).symm).hom ≫ pullback.snd
        (pullback.diagonal (terminal.from X))
        (pullback.map _ _ _ _ _ _ (𝟙 _) (by cat_disch) (by cat_disch))
  have hg : g = pullback.lift (𝟙 _) (𝟙 _) (by cat_disch) ≫ pullback.map
    ((g ≫ pullback.fst _ _) ≫ terminal.from X) ((g ≫ pullback.snd _ _) ≫ terminal.from X) _ _
      (g ≫ pullback.fst _ _) (g ≫ pullback.snd _ _) (𝟙 _) (by cat_disch) (by cat_disch) := by
    apply Limits.pullback.hom_ext <;> simp
  exact hg ▸ ⟨_, ⟨_, ⟨_, IsPullback.of_isLimit <| pasteVertIsPullback rfl bot
    (map_preimage F topMap ▸ top).flip.isLimit'.some⟩⟩⟩

Goal state after: