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 • s' i = (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t i)
i j : ι
⊢ basicOpen (f * g i * g j) ≤ basicOpen (f * g i)

Tactic:
exact basicOpen_mul_le_left _ _

Goal state after:
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 • s' i = (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t i)
i j : ι
hfgigi : basicOpen (f * (g i * g j)) ≤ basicOpen (f * g i)
⊢ basicOpen (f * g j * g i) ≤ basicOpen (f * g j)

Tactic:
exact basicOpen_mul_le_left _ _

Goal state after:
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
X : P.Over ⊤ S
⊢ ∃ ι U f,
    Sieve.ofArrows (fun i ↦ (MorphismProperty.CostructuredArrow.toOver P Scheme.Spec S).obj (U i)) f ∈
      (smallGrothendieckTopology P S) X

Tactic:
let 𝒰 := affineOpenCover X.left
    let 𝒱 : Cover (precoverage P) X.left :=
      𝒰.openCover.changeProp (fun _ ↦ IsZariskiLocalAtSource.of_isOpenImmersion _)
    let _ (i : 𝒱.I₀) : (𝒱.X i).Over S := ⟨𝒰.f i ≫ X.hom⟩
    let : Cover.Over S 𝒱 := { isOver_map _ := ⟨rfl⟩ }
    refine ⟨𝒰.I₀, fun i ↦ affineOverMk (𝒰.f i ≫ X.hom)
      (P.comp_mem _ _ (IsZariskiLocalAtSource.of_isOpenImmersion (𝒰.f i)) X.prop),
      fun i ↦ CostructuredArrow.homMk (𝒰.f i) (by simp), ?_⟩
    rw [Scheme.mem_smallGrothendieckTopology]
    exact ⟨𝒱, inferInstance, fun i ↦ P.comp_mem _ _ (𝒱.map_prop i) X.prop,
      fun _ _ ⟨i⟩ ↦ (Sieve.mem_ofArrows_iff ..).mpr ⟨i, 𝟙 _, by cat_disch⟩⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: case h.succ
σ : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : SetLike σ A
inst✝⁸ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝⁷ : GradedRing 𝒜
O : Type u_3
inst✝⁶ : CommRing O
inst✝⁵ : IsDomain O
inst✝⁴ : ValuationRing O
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra O K
inst✝¹ : IsFractionRing O K
φ₀ : ↥(𝒜 0) →+* O
ι : Type u_5
inst✝ : Finite ι
x : ι → A
h2 : Algebra.adjoin (↥(𝒜 0)) (Set.range x) = ⊤
j : ι
φ : Away 𝒜 (x j) →+* K
hcomm : (algebraMap O K).comp φ₀ = φ.comp (fromZeroRingHom 𝒜 (Submonoid.powers (x j)))
d : ι → ℕ
hdi : ∀ (i : ι), 0 < d i
hxdi : ∀ (i : ι), x i ∈ 𝒜 (d i)
val✝ : Fintype ι
ψ : ι → ValueGroup O K := fun i ↦ (valuation O K) (φ (Away.isLocalizationElem ⋯ ⋯) ^ ∏ k ∈ Finset.univ.erase i, d k)
this✝² : Nonempty ι
Kmax : ValueGroup O K := (Finset.image ψ Finset.univ).max' ⋯
i₀ : ι
hi1 : ψ i₀ = Kmax
hi₀ : ∀ (j : ι), ψ j ≤ ψ i₀
hKmax : 0 < Kmax
this✝¹ : Algebra (Away 𝒜 (x j)) (Away 𝒜 (x j * x i₀)) := (awayMap 𝒜 ⋯ ⋯).toAlgebra
this✝ : IsLocalization.Away (Away.isLocalizationElem ⋯ ⋯) (Away 𝒜 (x j * x i₀))
hunit : IsUnit (φ (Away.isLocalizationElem ⋯ ⋯))
φ' : Away 𝒜 (x j * x i₀) →+* K := IsLocalization.Away.lift (Away.isLocalizationElem ⋯ ⋯) hunit
hφ'1 : ∀ (s : Away 𝒜 (x j)), φ' ((awayMap 𝒜 ⋯ ⋯) s) = φ s
sx : Away 𝒜 (x i₀)
a : ℕ
ai : ι → ℕ
hai✝ : ∑ i, ai i • d i = a • d i₀
hai : ∑ x, ai x * d x = a * d i₀
H : (∏ i, x i ^ ai i) * x i₀ ^ (a * (d j - 1)) ∈ 𝒜 ((a * d i₀) • d j)
this :
  (valuation O K)
      (φ (Away.mk 𝒜 ⋯ (a * d i₀) ((∏ i, x i ^ ai i) * x i₀ ^ (a * (d j - 1))) H) /
        φ (Away.isLocalizationElem ⋯ ⋯) ^ a) ≤
    1
n✝ : ℕ
h : d j = n✝ + 1
⊢ (x j * x i₀) ^ (a * d i₀) * ((∏ i, x i ^ ai i) * x j ^ a * (x i₀ ^ (n✝ + 1) * x i₀ ^ d i₀) ^ a) =
    (x j * x i₀) ^ a * ((x j * x i₀) ^ d i₀) ^ a * ((∏ i, x i ^ ai i) * x i₀ ^ (a * (n✝ + 1 - 1)) * x i₀ ^ (a * d i₀))

Tactic:
rw [Nat.add_sub_cancel]; ring

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

Goal state before:
pp: case refine_1
X : Scheme
W : X.Etale
ι : Type u_1
Z : ι → X.Etale
f : (i : ι) → Z i ⟶ W
hf : Sieve.ofArrows Z f ∈ X.smallEtaleTopology W
⊢ ⋃ i, Set.range ⇑(f i).left = Set.univ

pp: case refine_2
X : Scheme
W : X.Etale
ι : Type u_1
Z : ι → X.Etale
f : (i : ι) → Z i ⟶ W
hf : ⋃ i, Set.range ⇑(f i).left = Set.univ
⊢ ∃ 𝒰 x, ∃ (h : ∀ (j : 𝒰.I₀), Etale (𝒰.X j ↘ X)), 𝒰.toPresieveOverProp h ≤ (Sieve.ofArrows Z f).arrows

Tactic:
· obtain ⟨U, _, _, hU⟩ := (mem_smallGrothendieckTopology _ _).1 hf
    ext y
    simp only [Set.mem_iUnion, Set.mem_range, Set.mem_univ, iff_true]
    obtain ⟨i, ⟨u, rfl⟩⟩ := ((ofArrows_mem_precoverage_iff _).1 U.mem₀).1 y
    obtain ⟨_, b, _, ⟨j⟩, fac⟩ := hU _ _ ⟨i⟩
    replace fac : b.left ≫ (f j).left = U.f i :=
      (Etale.forget _ ⋙ CategoryTheory.Over.forget _).congr_map fac
    exact ⟨j, b.left u, by simp [← fac]⟩

Goal state after:
case refine_2
X : Scheme
W : X.Etale
ι : Type u_1
Z : ι → X.Etale
f : (i : ι) → Z i ⟶ W
hf : ⋃ i, Set.range ⇑(f i).left = Set.univ
⊢ ∃ 𝒰 x, ∃ (h : ∀ (j : 𝒰.I₀), Etale (𝒰.X j ↘ X)), 𝒰.toPresieveOverProp h ≤ (Sieve.ofArrows Z f).arrows
Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact

Goal state before:
pp: case refine_3.inr.refine_2
P : MorphismProperty Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
F : Schemeᵒᵖ ⥤ Type u_1
inst✝ : IsZariskiLocalAtSource P
x✝ :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
T : Scheme
𝒰 : Cover (propQCPrecoverage P) T
this : ∀ ⦃T : Scheme⦄ (𝒰 : Cover (propQCPrecoverage P) T), (∃ R, T = Spec R) → Presieve.IsSheafFor F 𝒰.presieve₀
hT : ¬∃ R, T = Spec R
i j : T.affineOneHypercover.I₀
k : T.affineOneHypercover.I₁ i j
⊢ Presieve.IsSeparatedFor F
    (Presieve.pullbackArrows (T.affineOneHypercover.p₁ k ≫ T.affineOneHypercover.f i) 𝒰.presieve₀)

Tactic:
apply Presieve.IsSheafFor.isSeparatedFor

Goal state after:
case refine_3.inr.refine_2
P : MorphismProperty Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
F : Schemeᵒᵖ ⥤ Type u_1
inst✝ : IsZariskiLocalAtSource P
x✝ :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
T : Scheme
𝒰 : Cover (propQCPrecoverage P) T
this : ∀ ⦃T : Scheme⦄ (𝒰 : Cover (propQCPrecoverage P) T), (∃ R, T = Spec R) → Presieve.IsSheafFor F 𝒰.presieve₀
hT : ¬∃ R, T = Spec R
i j : T.affineOneHypercover.I₀
k : T.affineOneHypercover.I₁ i j
⊢ Presieve.IsSheafFor F (Presieve.pullbackArrows (T.affineOneHypercover.p₁ k ≫ T.affineOneHypercover.f i) 𝒰.presieve₀)
Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
⊢ (Presieve.ofArrows X π).EffectiveEpimorphic ↔ EffectiveEpiFamily X π

Tactic:
constructor
  · intro (h : Nonempty _)
    rw [Sieve.generateFamily_eq] at h
    constructor
    apply Nonempty.map (effectiveEpiFamilyStructOfIsColimit _ _) h
  · rintro ⟨h⟩
    change Nonempty _
    rw [Sieve.generateFamily_eq]
    apply Nonempty.map (isColimitOfEffectiveEpiFamilyStruct _ _) h

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

Goal state before:
pp: case refine_2
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₄
sq : IsPushout t l r b
A₀ : C
z : A₀ ⟶ kernel b
A₁ : C
π₁ : A₁ ⟶ A₀
w✝ : Epi π₁
x₁ :
  A₁ ⟶
    { X₁ := X₁, X₂ := X₂ ⊞ X₃, X₃ := ⋯.cokernelCofork.pt, f := biprod.lift t (-l), g := Cofork.π ⋯.cokernelCofork,
        zero := ⋯ }.X₁
hx₁ :
  π₁ ≫ z ≫ kernel.ι b ≫ biprod.inr =
    x₁ ≫
      { X₁ := X₁, X₂ := X₂ ⊞ X₃, X₃ := ⋯.cokernelCofork.pt, f := biprod.lift t (-l), g := Cofork.π ⋯.cokernelCofork,
          zero := ⋯ }.f
⊢ (π₁ ≫ z) ≫ equalizer.ι b 0 = ((-kernel.lift t x₁ ⋯) ≫ kernel.map t b l r ⋯) ≫ equalizer.ι b 0

Tactic:
simpa using hx₁ =≫ biprod.snd

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

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
F : J ⥤ MonoOver X
inst✝ : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj.hom
this : Mono f
⊢ Subobject.mk f = ⨆ j, Subobject.mk (F.obj j).obj.hom

Tactic:
apply le_antisymm

Goal state after:
case a
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
F : J ⥤ MonoOver X
inst✝ : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj.hom
this : Mono f
⊢ Subobject.mk f ≤ ⨆ j, Subobject.mk (F.obj j).obj.hom

case a
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
F : J ⥤ MonoOver X
inst✝ : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj.hom
this : Mono f
⊢ ⨆ j, Subobject.mk (F.obj j).obj.hom ≤ Subobject.mk f
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: case e
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
h : Presieve.IsSheaf J (CategoryTheory.uliftYoneda.{v', v, u}.obj Y)
⊢ ⦃X : C⦄ → (CategoryTheory.yoneda.obj Y).obj (op X) ≃ (CategoryTheory.uliftYoneda.{v', v, u}.obj Y).obj (op X)

Tactic:
intro
      exact Equiv.ulift.symm

Goal state after:
Module: Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
c : AttachCells g f
α' : Type t'
A' B' : α' → C
g' : (i' : α') → A' i' ⟶ B' i'
a : α → α'
ha : (i : α) → Arrow.mk (g i) ≅ Arrow.mk (g' (a i))
e : (Discrete.functor fun i ↦ A (c.π i)) ≅ Discrete.functor fun i ↦ A' (a (c.π i)) :=
  Discrete.natIso fun x ↦
    match x with
    | { as := i } => Arrow.leftFunc.mapIso (ha (c.π i))
i : c.ι
⊢ c.cofan₁.inj i ≫ (Iso.refl c.cofan₁.pt).hom =
    Cofan.inj
      ((Cocone.precompose e.hom).obj
        (Cofan.mk c.cofan₁.pt fun i ↦ Arrow.leftFunc.map (ha (c.π i)).inv ≫ c.cofan₁.inj i))
      i

Tactic:
simp [Cocone.precompose, e, Cofan.inj]

Goal state after:
Module: Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
c : AttachCells g f
α' : Type t'
A' B' : α' → C
g' : (i' : α') → A' i' ⟶ B' i'
a : α → α'
ha : (i : α) → Arrow.mk (g i) ≅ Arrow.mk (g' (a i))
e : (Discrete.functor fun i ↦ B (c.π i)) ≅ Discrete.functor fun i ↦ B' (a (c.π i)) :=
  Discrete.natIso fun x ↦
    match x with
    | { as := i } => Arrow.rightFunc.mapIso (ha (c.π i))
i : c.ι
⊢ c.cofan₂.inj i ≫ (Iso.refl c.cofan₂.pt).hom =
    Cofan.inj
      ((Cocone.precompose e.hom).obj
        (Cofan.mk c.cofan₂.pt fun i ↦ Arrow.rightFunc.map (ha (c.π i)).inv ≫ c.cofan₂.inj i))
      i

Tactic:
simp [Cocone.precompose, e, Cofan.inj]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
⊢ IsSmall.{w, v, u} W ↔ ∃ ι A B f, W = ofHoms f

Tactic:
by
  constructor
  · intro
    refine ⟨Shrink.{w} W.toSet, _, _, fun i ↦ ((equivShrink _).symm i).1.hom, ?_⟩
    ext A B f
    rw [ofHoms_iff]
    constructor
    · intro hf
      exact ⟨equivShrink _ ⟨f, hf⟩, by simp⟩
    · rintro ⟨i, hi⟩
      simp only [← W.arrow_mk_mem_toSet_iff, hi, Arrow.mk_eq, Subtype.coe_prop]
  · rintro ⟨_, _, _, _, rfl⟩
    infer_instance

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
n d : ℤ
hqz : q ≠ 0
qdf : q = n /. d
hd : d ≠ 0
c : ℤ
hc1 : n = c * q.num
hc2 : d = c * ↑q.den
⊢ FiniteMultiplicity (↑p) (c * ↑q.den)

Tactic:
simpa [finite_int_prime_iff, hc2] using hd

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

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

Tactic:
· exact (lt_largerSubobject hG A hA).le

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
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator G
⊢ (generatingMonomorphisms G).rlp = (monomorphisms C).rlp

Tactic:
apply le_antisymm

Goal state after:
case a
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator G
⊢ (generatingMonomorphisms G).rlp ≤ (monomorphisms C).rlp

case a
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator G
⊢ (monomorphisms C).rlp ≤ (generatingMonomorphisms G).rlp
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
⊢ ¬padicValNat p n + 1 ≤ padicValNat p n

Tactic:
not_le

Goal state after:
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
⊢ padicValNat p n < padicValNat p n + 1
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p n : ℕ
hp : Fact (Prime p)
⊢ ¬log p (n + 1) ≤ log p n → log p (n + 1) ≤ padicValNat p (n + 1)

Tactic:
not_le

Goal state after:
p n : ℕ
hp : Fact (Prime p)
⊢ log p n < log p (n + 1) → log p (n + 1) ≤ padicValNat p (n + 1)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case coe
p : ℕ
hp : Fact (Nat.Prime p)
x : Multiplicative ℤ
⊢ ∃ a, (padicValuation p) a = ↑x

Tactic:
induction x with | ofAdd x

Goal state after:
case coe.ofAdd
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
⊢ ∃ a, (padicValuation p) a = ↑(Multiplicative.ofAdd x)
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n + k
⊢ k + n - (k + n) + ((p.digits n).sum + (p.digits k).sum) - (p.digits (k + n)).sum =
    (p.digits k).sum + (p.digits n).sum - (p.digits (k + n)).sum

Tactic:
Nat.sub_self (k + n),

Goal state after:
p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n + k
⊢ 0 + ((p.digits n).sum + (p.digits k).sum) - (p.digits (k + n)).sum =
    (p.digits k).sum + (p.digits n).sum - (p.digits (k + n)).sum
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ maximalIdeal ℤ_[p] = Ideal.span {↑p}

Tactic:
apply le_antisymm

Goal state after:
case a
p : ℕ
hp : Fact (Nat.Prime p)
⊢ maximalIdeal ℤ_[p] ≤ Ideal.span {↑p}

case a
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Ideal.span {↑p} ≤ maximalIdeal ℤ_[p]
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : ¬f ≈ 0
this✝² : ∃ ε > 0, ∃ N1, ∀ j ≥ N1, ε ≤ padicNorm p (↑f j)
ε : ℚ
hε : ε > 0
N1 : ℕ
hN1 : ∀ j ≥ N1, ε ≤ padicNorm p (↑f j)
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNorm p (↑f j - ↑f k) < ε
n m : ℕ
hn : max N1 N2 ≤ n
hm : max N1 N2 ≤ m
this✝¹ : padicNorm p (↑f n - ↑f m) < ε
this✝ : padicNorm p (↑f n - ↑f m) < padicNorm p (↑f n)
this : padicNorm p (↑f n - ↑f m) < max (padicNorm p (↑f n)) (padicNorm p (↑f m))
⊢ padicNorm p (↑f m) = padicNorm p (↑f n)

Tactic:
by_contra hne

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : ¬f ≈ 0
this✝² : ∃ ε > 0, ∃ N1, ∀ j ≥ N1, ε ≤ padicNorm p (↑f j)
ε : ℚ
hε : ε > 0
N1 : ℕ
hN1 : ∀ j ≥ N1, ε ≤ padicNorm p (↑f j)
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNorm p (↑f j - ↑f k) < ε
n m : ℕ
hn : max N1 N2 ≤ n
hm : max N1 N2 ≤ m
this✝¹ : padicNorm p (↑f n - ↑f m) < ε
this✝ : padicNorm p (↑f n - ↑f m) < padicNorm p (↑f n)
this : padicNorm p (↑f n - ↑f m) < max (padicNorm p (↑f n)) (padicNorm p (↑f m))
hne : ¬padicNorm p (↑f m) = padicNorm p (↑f n)
⊢ False
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℚ_[p]
hx : ¬0 ≤ x.valuation
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
⊢ x.valuation ≤ 0

Tactic:
not_le

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℚ_[p]
hx : x.valuation < 0
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
⊢ x.valuation ≤ 0
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℚ_[p]
hx : ¬‖x‖ ≤ 1
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
hn_coe : ↑n = -x.valuation
a : ℚ_[p] := x * ↑p ^ n
ha : a = x * ↑p ^ n
⊢ ‖a‖ = 1

Tactic:
have hx : x ≠ 0 := by
          intro h0
          rw [h0, norm_zero] at hx
          exact hx zero_le_one

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℚ_[p]
hx✝ : ¬‖x‖ ≤ 1
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
hn_coe : ↑n = -x.valuation
a : ℚ_[p] := x * ↑p ^ n
ha : a = x * ↑p ^ n
hx : x ≠ 0
⊢ ‖a‖ = 1
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
⊢ c.inl = c.inr → Epi f

Tactic:
· intro hf
    constructor
    intro Z g g' h
    obtain ⟨φ, rfl, rfl⟩ := PushoutCocone.IsColimit.desc' hc g g' h
    rw [hf]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
I : Type u_2
D : I → Type u_3
inst✝ : (i : I) → Category.{u_5, u_3} (D i)
F : (i : I) → C ⥤ D i
h : JointlyFaithful F
X Y : C
f : X ⟶ Y
x✝ : ∀ (i : I), Mono ((F i).map f)
Z : C
g₁ g₂ : Z ⟶ X
hg : g₁ ≫ f = g₂ ≫ f
i : I
⊢ (F i).map g₁ = (F i).map g₂

Tactic:
simp only [← cancel_mono ((F i).map f), ← Functor.map_comp, hg]

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

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

Tactic:
have : f + g ≈ f := show LimZero (f + g - f) by simpa only [add_sub_cancel_left, sub_zero]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : f.norm ≠ g.norm
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
this✝ : (g - 0).LimZero
this : f + g ≈ f
⊢ (f + g).norm = max f.norm g.norm
Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies

Goal state before:
pp: case pos
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : G.Additive
X : SimplicialObject C
q n m : ℕ
hnm : c.Rel m n
h✝ : n < q
⊢ 0 ≫ eqToHom ⋯ = G.map (0 ≫ eqToHom ⋯)

pp: case neg
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : G.Additive
X : SimplicialObject C
q n m : ℕ
hnm : c.Rel m n
h✝ : ¬n < q
⊢ ((-1) ^ (n - q) • (((whiskering C D).obj G).obj X).σ ⟨n - q, ⋯⟩) ≫ eqToHom ⋯ =
    G.map (((-1) ^ (n - q) • X.σ ⟨n - q, ⋯⟩) ≫ eqToHom ⋯)

Tactic:
· simp only [Functor.map_zero, zero_comp]

Goal state after:
case neg
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : G.Additive
X : SimplicialObject C
q n m : ℕ
hnm : c.Rel m n
h✝ : ¬n < q
⊢ ((-1) ^ (n - q) • (((whiskering C D).obj G).obj X).σ ⟨n - q, ⋯⟩) ≫ eqToHom ⋯ =
    G.map (((-1) ^ (n - q) • X.σ ⟨n - q, ⋯⟩) ≫ eqToHom ⋯)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case hbc.h₁.hbc.h₁
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
⊢ padicNormE (↑(limSeq f j) - ↑f j) < ε / 3

pp: case h₂
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
⊢ padicNormE (↑f j - ↑f (max N N2)) < ε / 3

Tactic:
· rw [padicNormE.map_sub]
          apply mod_cast hN j
          exact le_of_max_le_left hj

Goal state after:
case h₂
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
⊢ padicNormE (↑f j - ↑f (max N N2)) < ε / 3
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
⊢ ‖↑p‖ * 1 < 1

Tactic:
rw [mul_one, norm_p]
        exact inv_lt_one_of_one_lt₀ <| mod_cast hp.1.one_lt

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
⊢ (PInfty.f n).f = Y.p.app (op ⦋n⦌) ≫ PInfty.f n

Tactic:
let Y₃ := ((whiskering _ _).obj (toKaroubi C)).obj Y.X

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
⊢ (PInfty.f n).f = Y.p.app (op ⦋n⦌) ≫ PInfty.f n
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
⊢ min x.valuation y.valuation ≤ (x + y).valuation

Tactic:
have : ‖x + y‖ ≤ max ‖x‖ ‖y‖ := nonarchimedean x y

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
this : ‖x + y‖ ≤ max ‖x‖ ‖y‖
⊢ min x.valuation y.valuation ≤ (x + y).valuation
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ Valuation.comap (Int.castRingHom ℚ_[p]) mulValuation = Int.padicValuation p

Tactic:
by
  ext
  simp [← Rat.padicValuation_cast, ← comap_mulValuation_eq_padicValuation]

Goal state after: