mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: case hxj.convert_8
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
⊢ SetLike.GradedMonoid 𝒜

pp: case hxj.convert_12
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
⊢ x ∈ 𝒜 (d + e)

Tactic:
· infer_instance

Goal state after:
case hxj.convert_12
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
⊢ x ∈ 𝒜 (d + e)
Module: Mathlib.AlgebraicGeometry.Sites.Affine

Goal state before:
pp: S : Scheme
P : MorphismProperty Scheme
inst✝³ : P.IsMultiplicative
inst✝² : IsZariskiLocalAtSource P
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasOfPostcompProperty P
U : P.Over ⊤ S
𝒰 : Cover (precoverage P) U.left := Cover.changeProp U.left.affineCover ⋯
x✝² : (i : 𝒰.I₀) → (𝒰.X i).Over S := fun i ↦ { hom := 𝒰.f i ≫ U.hom }
x✝¹ : Cover.Over S 𝒰 := { over := inferInstance, isOver_map := ⋯ }
X : P.Over ⊤ S
f : X ⟶ U
x✝ : 𝒰.toPresieveOverProp ⋯ f
i : 𝒰.I₀
⊢ { arrows := Presieve.coverByImage (MorphismProperty.CostructuredArrow.toOver P Scheme.Spec S) U,
        downward_closed := ⋯ }.arrows
    (Hom.asOverProp (𝒰.f i) S)

Tactic:
exact ⟨⟨affineOverMk (𝒰.f i ≫ U.hom) (P.comp_mem _ _ (𝒰.map_prop i) U.prop),
      CostructuredArrow.homMk (𝟙 _) ⟨⟩ rfl, Over.homMk (𝒰.f i) (by simp) trivial,
      by cat_disch⟩⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case refine_1.refine_2
R : CommRingCat
M : (Spec R).Modules
φ : (f : ↑R) →
  ↑((modulesSpecToSheaf.obj M).obj.obj (op ⊤)) →ₗ[↑R] ↑((modulesSpecToSheaf.obj M).obj.obj (op (basicOpen f))) :=
  fun f ↦ ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (basicOpen f).leTop.op)
h : IsLocalizing (modulesSpecToSheaf.obj M)
hf : ∀ (f : ↑R), IsLocalizedModule.Away f (φ f)
f : ↑R
hle : basicOpen f ≤ ⊤
s : ↑Γ(M, ⊤)
hs : (ConcreteCategory.hom (M.presheaf.map (homOfLE hle).op)) s = 0
n : ℕ
hn : ⟨(fun x ↦ f ^ x) n, ⋯⟩ • s = 0
⊢ ∃ n, f ^ n • s = 0

Tactic:
use n, hn

Goal state after:
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case refine_4
R : CommRingCat
M : (Spec R).Modules
φ : (f : ↑R) →
  ↑((modulesSpecToSheaf.obj M).obj.obj (op ⊤)) →ₗ[↑R] ↑((modulesSpecToSheaf.obj M).obj.obj (op (basicOpen f))) :=
  fun f ↦ ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (basicOpen f).leTop.op)
h : Aux M ⊤
f : ↑R
x : ↑((modulesSpecToSheaf.obj M).obj.obj (op ⊤))
⊢ (ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (basicOpen f).leTop.op)) x = 0 → ∃ n, f ^ n • x = 0

Tactic:
hx

Goal state after:
case refine_4
R : CommRingCat
M : (Spec R).Modules
φ : (f : ↑R) →
  ↑((modulesSpecToSheaf.obj M).obj.obj (op ⊤)) →ₗ[↑R] ↑((modulesSpecToSheaf.obj M).obj.obj (op (basicOpen f))) :=
  fun f ↦ ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (basicOpen f).leTop.op)
h : Aux M ⊤
f : ↑R
x : ↑((modulesSpecToSheaf.obj M).obj.obj (op ⊤))
hx : (ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (basicOpen f).leTop.op)) x = 0
⊢ ∃ n, f ^ n • x = 0
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case refine_4
R : CommRingCat
M : (Spec R).Modules
φ : (f : ↑R) →
  ↑((modulesSpecToSheaf.obj M).obj.obj (op ⊤)) →ₗ[↑R] ↑((modulesSpecToSheaf.obj M).obj.obj (op (basicOpen f))) :=
  fun f ↦ ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (basicOpen f).leTop.op)
h : Aux M ⊤
f : ↑R
x : ↑((modulesSpecToSheaf.obj M).obj.obj (op ⊤))
hx : (ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (basicOpen f).leTop.op)) x = 0
n : ℕ
hn : f ^ n • x = 0
⊢ ∃ n, f ^ n • x = 0

Tactic:
use n, hn

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

Goal state before:
pp: C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
P : MorphismProperty C
S : C
inst✝⁸ : P.IsStableUnderComposition
K : Precoverage C
inst✝⁷ : K.HasIsos
inst✝⁶ : K.IsStableUnderBaseChange
inst✝⁵ : K.IsStableUnderComposition
inst✝⁴ : K.HasPullbacks
inst✝³ : HasFiniteWidePullbacks C
inst✝² : P.HasOfPostcompProperty P
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.ContainsIdentities
H : K ≤ P.precoverage
⊢ (Precoverage.comap (Over.forget P ⊤ S ⋙ CategoryTheory.Over.forget S) K).toGrothendieck =
    (Over.forget P ⊤ S).inducedTopology (K.toGrothendieck.over S)

Tactic:
by
  have := isContinuous_comap_forget (S := S) _ H
  refine (Functor.restrictedTopology_eq_inducedTopology_of_isContinuous ?_).symm
  rw [toGrothendieck_comap_forget_eq_restrictedTopology _ H]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst✝ : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
T₁ : C
π : T₁ ⟶ T₀
w✝ : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
hx₄ : 0 ≫ r' = 0
hx₂' : π ≫ x₄ = 0
⊢ x₄ = 0

Tactic:
rw [← cancel_epi π, hx₂', comp_zero]

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

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : J.Subcanonical
ι : Type u_1
X : ι → C
c : Cofan X
H : Sieve.ofArrows X c.inj ∈ J c.pt
inst✝ : ∀ (i : ι), Mono (c.inj i)
hempty : ∀ (Y : C) (a : IsInitial Y), ⊥ ∈ J Y
hdisj : ∀ {i j : ι}, i ≠ j → ∀ {Y : C} (a : Y ⟶ X i) (b : Y ⟶ X j), a ≫ c.inj i = b ≫ c.inj j → Nonempty (IsInitial Y)
heq :
  ∀ (s : Cofan fun i ↦ J.yoneda.obj (X i)) {Y : C} {i j : ι} (a : Y ⟶ X i) (b : Y ⟶ X j),
    a ≫ c.inj i = b ≫ c.inj j →
      (ConcreteCategory.hom ((s.inj i).hom.app (op Y))) a = (ConcreteCategory.hom ((s.inj j).hom.app (op Y))) b
s : Cofan fun i ↦ J.yoneda.obj (X i)
j : ι
u : (j : ι) → CategoryTheory.yoneda.obj (X j) ⟶ (Sieve.ofArrows X c.inj).functor :=
  fun j ↦ (Sieve.ofArrows X c.inj).toFunctor (c.inj j) ⋯
this : ∀ (j : ι), u j ≫ (Sieve.ofArrows X c.inj).functorInclusion = CategoryTheory.yoneda.map (c.inj j)
⊢ CategoryTheory.yoneda.map (c.inj j) ≫
      ⋯.extend
        { app := fun Y ↦ ↾fun g ↦ (ConcreteCategory.hom ((s.inj (Sieve.ofArrows.i ⋯)).hom.app Y)) (Sieve.ofArrows.h ⋯),
          naturality := ⋯ } =
    (s.inj j).hom

Tactic:
simp only [← this, Category.assoc, Presieve.IsSheafFor.functorInclusion_comp_extend]

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : J.Subcanonical
ι : Type u_1
X : ι → C
c : Cofan X
H : Sieve.ofArrows X c.inj ∈ J c.pt
inst✝ : ∀ (i : ι), Mono (c.inj i)
hempty : ∀ (Y : C) (a : IsInitial Y), ⊥ ∈ J Y
hdisj : ∀ {i j : ι}, i ≠ j → ∀ {Y : C} (a : Y ⟶ X i) (b : Y ⟶ X j), a ≫ c.inj i = b ≫ c.inj j → Nonempty (IsInitial Y)
heq :
  ∀ (s : Cofan fun i ↦ J.yoneda.obj (X i)) {Y : C} {i j : ι} (a : Y ⟶ X i) (b : Y ⟶ X j),
    a ≫ c.inj i = b ≫ c.inj j →
      (ConcreteCategory.hom ((s.inj i).hom.app (op Y))) a = (ConcreteCategory.hom ((s.inj j).hom.app (op Y))) b
s : Cofan fun i ↦ J.yoneda.obj (X i)
j : ι
u : (j : ι) → CategoryTheory.yoneda.obj (X j) ⟶ (Sieve.ofArrows X c.inj).functor :=
  fun j ↦ (Sieve.ofArrows X c.inj).toFunctor (c.inj j) ⋯
this : ∀ (j : ι), u j ≫ (Sieve.ofArrows X c.inj).functorInclusion = CategoryTheory.yoneda.map (c.inj j)
⊢ u j ≫
      { app := fun Y ↦ ↾fun g ↦ (ConcreteCategory.hom ((s.inj (Sieve.ofArrows.i ⋯)).hom.app Y)) (Sieve.ofArrows.h ⋯),
        naturality := ⋯ } =
    (s.inj j).hom
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝² : SmallCategory J
Y : J ⥤ C
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝¹ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
inst✝ : ∀ (j j' : J) (φ : j ⟶ j'), Mono (Y.map φ)
c : Cocone Y
hc : IsColimit c
⊢ IsColimit ((coyoneda.obj (op X)).mapCocone c)

Tactic:
by
    have := isFiltered_of_isCardinalFiltered J κ
    exact Types.FilteredColimit.isColimitOf' _ _
      (surjectivity hc hXκ) (injectivity hc hXκ)

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v', u_1} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.IsContinuous J K
inst✝ : K.Subcanonical
Y : C
⊢ Presieve.IsSheaf K (CategoryTheory.uliftYoneda.{v, v', u_1}.obj (F.obj Y))

Tactic:
apply GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable

Goal state after:
Module: Mathlib.Order.Interval.Set.SuccOrder

Goal state before:
pp: J : Type u_1
inst✝¹ : PartialOrder J
inst✝ : SuccOrder J
j : J
i : ↑(Iic j)
hi : ¬IsMax i
⊢ ↑(Order.succ i) = Order.succ ↑i

Tactic:
rw [coe_succ_of_mem]

Goal state after:
J : Type u_1
inst✝¹ : PartialOrder J
inst✝ : SuccOrder J
j : J
i : ↑(Iic j)
hi : ¬IsMax i
⊢ Order.succ ↑i ∈ Iic j
Module: Mathlib.Order.Shrink

Goal state before:
pp: α : Type u_1
inst✝¹ : Small.{u, u_1} α
inst✝ : Preorder α
a b : α
⊢ (equivShrink α) a ≤ (equivShrink α) b ↔ a ≤ b

Tactic:
obtain ⟨a, rfl⟩ := (equivShrink.{u} α).symm.surjective a

Goal state after:
α : Type u_1
inst✝¹ : Small.{u, u_1} α
inst✝ : Preorder α
b : α
a : Shrink.{u, u_1} α
⊢ (equivShrink α) ((equivShrink α).symm a) ≤ (equivShrink α) b ↔ (equivShrink α).symm a ≤ b
Module: Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
⊢ ¬↑⟨Order.succ j, ⋯⟩ ≤ j

Tactic:
by simpa only [Order.succ_le_iff_isMax] using hj

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
⊢ ¬Order.succ j ≤ j

Tactic:
by simpa only [Order.succ_le_iff_isMax] using hj

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
hi : Order.succ j ≤ Order.succ j
h₁ : ¬Order.succ j ≤ j
⊢ ¬Order.succ j ≤ j

Tactic:
by simpa only [Order.succ_le_iff_isMax] using hj

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
Φ : SuccStruct C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i₁ i₂ : J
h₁₂ : i₁ ≤ i₂
j : J
iter : Φ.Iteration j
hj : i₂ ≤ j
⊢ Arrow.mk ((Φ.iterationFunctor J).map (homOfLE h₁₂)) = Arrow.mk (iter.F.map (homOfLE h₁₂))

Tactic:
by
  dsimp [iterationFunctor]
  rw [Iteration.arrow_mk_mapObj]
  exact Arrow.ext (Iteration.congr_obj _ _ _ _ _)
    (Iteration.congr_obj _ _ _ _ _) (Iteration.congr_map _ _ _ _ _)

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : i < j
k : J
iter' : Φ.Iteration k
hk : i ≤ k
⊢ (ofCocone (colimit.cocone (inductiveSystem iter))).obj ⟨i, ⋯⟩ = iter'.F.obj ⟨i, hk⟩

Tactic:
ofCocone_obj_eq _ _ hi

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : i < j
k : J
iter' : Φ.Iteration k
hk : i ≤ k
⊢ (inductiveSystem iter).obj ⟨i, hi⟩ = iter'.F.obj ⟨i, hk⟩
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

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
⊢ W.llp.IsStableUnderTransfiniteCompositionOfShape J

Tactic:
by
  rw [isStableUnderTransfiniteCompositionOfShape_iff]
  rintro X Y f ⟨h⟩
  have : W.llp (h.incl.app ⊥) := fun _ _ p hp ↦
    HasLiftingProperty.transfiniteComposition.hasLiftingProperty_ι_app_bot
      (hc := h.isColimit) (fun j hj ↦ h.map_mem j hj _ hp)
  exact (MorphismProperty.arrow_mk_iso_iff _
    (Arrow.isoMk h.isoBot.symm (Iso.refl _))).2 this

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
⊢ padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)

Tactic:
by
  wlog hle : padicValRat p q ≤ padicValRat p r generalizing q r
  · rw [add_comm, max_comm]
    exact this (le_of_not_ge hle)
  exact nonarchimedean_aux hle

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p j : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
S : Finset ℕ
hS : S.Nonempty
hF : ∀ i ∈ S, padicValRat p (F j) < padicValRat p (F i)
hn1 : ∀ (i : ℕ), 0 < F i
⊢ padicValRat p (F j) < padicValRat p (∑ i ∈ S, F i)

Tactic:
induction hS using Finset.Nonempty.cons_induction with
  | singleton k =>
    rw [Finset.sum_singleton]
    exact hF k (by simp)
  | cons s S' Hnot Hne Hind =>
    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.PadicVal.Basic

Goal state before:
pp: p n : ℕ
hp : 1 ≤ padicValNat p n
h : ¬p ∣ n
⊢ False

Tactic:
padicValNat.eq_zero_of_not_dvd h

Goal state after:
p n : ℕ
hp : 1 ≤ 0
h : ¬p ∣ n
⊢ False
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case coe.ofAdd.inl
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
hx : 0 ≤ x
⊢ ∃ a,
    { toFun := fun x ↦ if x = 0 then 0 else ↑(Multiplicative.ofAdd (-padicValRat p x)), map_zero' := ⋯ } a =
      ↑(Multiplicative.ofAdd x)

pp: case coe.ofAdd.inr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
hx : x < 0
⊢ ∃ a,
    { toFun := fun x ↦ if x = 0 then 0 else ↑(Multiplicative.ofAdd (-padicValRat p x)), map_zero' := ⋯ } a =
      ↑(Multiplicative.ofAdd x)

Tactic:
· exact ⟨(p ^ x.natAbs)⁻¹, by simp [hp.out.ne_zero, hx]⟩

Goal state after:
case coe.ofAdd.inr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
hx : x < 0
⊢ ∃ a,
    { toFun := fun x ↦ if x = 0 then 0 else ↑(Multiplicative.ofAdd (-padicValRat p x)), map_zero' := ⋯ } a =
      ↑(Multiplicative.ofAdd x)
Module: Mathlib.NumberTheory.Padics.PadicIntegers

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

Tactic:
Nat.cast_pow

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]
⊢ x ∈ maximalIdeal ℤ_[p] → x ∈ Ideal.span {↑p}

Tactic:
hx

Goal state after:
case a
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ∈ maximalIdeal ℤ_[p]
⊢ x ∈ Ideal.span {↑p}
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ (maximalIdeal ℤ_[p]).IsPrime

pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ ↑p ≠ 0

Tactic:
· infer_instance

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ↑p ≠ 0
Module: Mathlib.CategoryTheory.Limits.EpiMono

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
a✝ : IsIso c.fst
φ : X ⟶ c.pt
hφ₁ : φ ≫ c.fst = 𝟙 X
hφ₂ : φ ≫ c.snd = 𝟙 X
⊢ c.fst ≫ φ ≫ c.fst = c.fst

Tactic:
hφ₁,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
a✝ : IsIso c.fst
φ : X ⟶ c.pt
hφ₁ : φ ≫ c.fst = 𝟙 X
hφ₂ : φ ≫ c.snd = 𝟙 X
⊢ c.fst ≫ 𝟙 X = c.fst
Module: Mathlib.CategoryTheory.Limits.EpiMono

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
a✝ : IsIso c.fst
φ : X ⟶ c.pt
hφ₁ : φ ≫ c.fst = 𝟙 X
hφ₂ : φ ≫ c.snd = 𝟙 X
this : IsSplitEpi φ
⊢ φ ≫ c.fst = φ ≫ c.snd

Tactic:
hφ₁,

Goal state after:
case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
a✝ : IsIso c.fst
φ : X ⟶ c.pt
hφ₁ : φ ≫ c.fst = 𝟙 X
hφ₂ : φ ≫ c.snd = 𝟙 X
this : IsSplitEpi φ
⊢ 𝟙 X = φ ≫ c.snd
Module: Mathlib.CategoryTheory.Limits.EpiMono

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
a✝ : IsIso c.inl
φ : c.pt ⟶ Y
hφ₁ : c.inl ≫ φ = 𝟙 Y
hφ₂ : c.inr ≫ φ = 𝟙 Y
this : IsSplitMono φ
⊢ c.inl ≫ φ = c.inr ≫ φ

Tactic:
hφ₁,

Goal state after:
case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
a✝ : IsIso c.inl
φ : c.pt ⟶ Y
hφ₁ : c.inl ≫ φ = 𝟙 Y
hφ₂ : c.inr ≫ φ = 𝟙 Y
this : IsSplitMono φ
⊢ 𝟙 Y = c.inr ≫ φ
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : (g - 0).LimZero
⊢ f + g ≈ f

Tactic:
change LimZero (f + g - f)

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : (g - 0).LimZero
⊢ LimZero (f + g - f)
Module: Mathlib.AlgebraicGeometry.Sites.EtalePoint

Goal state before:
pp: case mk
S : Scheme
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
X : Scheme
f : X ⟶ S
x✝ : Etale f
R : Sieve (Etale.mk f)
hR : R ∈ S.smallEtaleTopology (Etale.mk f)
φ : Spec (CommRingCat.of Ω) ⟶ X
𝒰 : Cover (precoverage @Etale) (Etale.mk f).left
h : Cover.Over S 𝒰
w✝ : ∀ (j : 𝒰.I₀), Etale (𝒰.X j ↘ S)
le : 𝒰.toPresieveOverProp w✝ ≤ R.arrows
i : 𝒰.I₀
y : ↥(𝒰.X i)
hy : (𝒰.f i) y = φ default
l : Spec (CommRingCat.of Ω) ⟶ 𝒰.X i
hl₁ : l ≫ 𝒰.f i = φ
hl₂ : l default = y
this : 𝒰.f i ≫ f = 𝒰.X i ↘ S
⊢ ∃ Y f_1,
    ∃ (_ : R.arrows f_1),
      ∃ y, (ConcreteCategory.hom ((Etale.forget S ⋙ coyoneda.obj (op (Over.mk (φ ≫ f)))).map f_1)) y = Over.homMk φ ⋯

Tactic:
exact ⟨(𝒰.X i).asOverProp S inferInstance,
      MorphismProperty.Over.homMk (𝒰.f i), le _ _ ⟨i⟩, Over.homMk l, by cat_disch⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.EtalePoint

Goal state before:
pp: S : Scheme
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
s : Spec (CommRingCat.of Ω) ⟶ S
s₀ : ↥S
hs₀ : s default = s₀
X : S.Etale
y : ↥(Hom.fiber X.hom s₀)
⊢ ∃ a, pointSmallEtaleFiberObjToPreimage s hs₀ a = (Hom.fiberHomeo X.hom s₀) y

Tactic:
obtain ⟨⟨t, a⟩, rfl⟩ := (Scheme.SpecToEquivOfField Ω _).symm.surjective s

Goal state after:
S : Scheme
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
s₀ : ↥S
X : S.Etale
y : ↥(Hom.fiber X.hom s₀)
t : ↥S
a : S.residueField t ⟶ CommRingCat.of Ω
hs₀ : ((SpecToEquivOfField Ω S).symm ⟨t, a⟩) default = s₀
⊢ ∃ a_1, pointSmallEtaleFiberObjToPreimage ((SpecToEquivOfField Ω S).symm ⟨t, a⟩) hs₀ a_1 = (Hom.fiberHomeo X.hom s₀) y
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
X Y Y' X' : D
f : X ⟶ X'
g : Y ⟶ X'
f' : Y' ⟶ Y
g' : Y' ⟶ X
P₁ : IsPullback f' g' g f
hg : F.relativelyRepresentable g
a : C
h : F.obj a ⟶ X
⊢ hg.fst (h ≫ f) ≫ g = (F.map (hg.snd (h ≫ f)) ≫ h) ≫ f

Tactic:
simpa using hg.w (h ≫ f)

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)
P₁ : K[Y₁] ⟶ K[Y₁] := PInfty
P₂ : K[Y₂] ⟶ K[Y₂] := PInfty
P₃ : K[Y₃] ⟶ K[Y₃] := PInfty
P₄ : K[Y₄] ⟶ K[Y₄] := PInfty
h₃₂ : (P₃.f n).f = P₂.f n
h₄₃ : P₄.f n = P₃.f n
h₁₄ :
  (𝟙 (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C) ◫ natTransPInfty_f (Karoubi C) n).app Y =
    (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
            alternatingFaceMapComplex (Karoubi C) ⋙ HomologicalComplex.eval (Karoubi C) (ComplexShape.down ℕ) n).map
        Y.decompId_i ≫
      (𝟙 (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C) ◫ natTransPInfty_f (Karoubi C) n).app
          { X := Y.X, p := 𝟙 Y.X, idem := ⋯ } ≫
        (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
              alternatingFaceMapComplex (Karoubi C) ⋙ HomologicalComplex.eval (Karoubi C) (ComplexShape.down ℕ) n).map
          Y.decompId_p
⊢ (P₁.f n).f = Y.p.app (op ⦋n⦌) ≫ P₂.f n

Tactic:
dsimp [natTransPInfty_f] at h₁₄

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)
P₁ : K[Y₁] ⟶ K[Y₁] := PInfty
P₂ : K[Y₂] ⟶ K[Y₂] := PInfty
P₃ : K[Y₃] ⟶ K[Y₃] := PInfty
P₄ : K[Y₄] ⟶ K[Y₄] := PInfty
h₃₂ : (P₃.f n).f = P₂.f n
h₄₃ : P₄.f n = P₃.f n
h₁₄ :
  (𝟙 (KaroubiFunctorCategoryEmbedding.obj Y _⦋n⦌) ≫ PInfty.f n) ≫ 𝟙 (KaroubiFunctorCategoryEmbedding.obj Y _⦋n⦌) =
    (KaroubiFunctorCategoryEmbedding.map Y.decompId_i).app (op ⦋n⦌) ≫
      ((𝟙 (KaroubiFunctorCategoryEmbedding.obj { X := Y.X, p := 𝟙 Y.X, idem := ⋯ } _⦋n⦌) ≫ PInfty.f n) ≫
          𝟙 (KaroubiFunctorCategoryEmbedding.obj { X := Y.X, p := 𝟙 Y.X, idem := ⋯ } _⦋n⦌)) ≫
        (KaroubiFunctorCategoryEmbedding.map Y.decompId_p).app (op ⦋n⦌)
⊢ (P₁.f n).f = Y.p.app (op ⦋n⦌) ≫ P₂.f n
Module: Mathlib.AlgebraicTopology.DoldKan.Faces

Goal state before:
pp: case neg.h.hj₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
j : Fin (n + 1)
⊢ j.succ.succ.pred ⋯ ≠ 0

Tactic:
simp [Fin.succ_ne_zero]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ addValuationDef 0 = ⊤

Tactic:
rw [addValuationDef, if_pos rfl]

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

Goal state before:
pp: case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
K : ChainComplex C ℕ
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
h✝¹ : ¬Δ = Δ'
h✝ : Isδ₀ i
⊢ K.X Δ.len ⟶ K.X Δ'.len

Tactic:
exact K.d Δ.len Δ'.len

Goal state after: