mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. (↑q.den * ↑r.den)
hq' : q.num /. ↑q.den ≠ 0
hr' : r.num /. ↑r.den ≠ 0
hp' : _root_.Prime ↑p
⊢ ↑(multiplicity (↑p) q.num) + ↑(multiplicity (↑p) r.num) - (↑(multiplicity ↑p ↑q.den) + ↑(multiplicity ↑p ↑r.den)) =
    ↑(multiplicity (↑p) q.num) - ↑(multiplicity ↑p ↑q.den) + (↑(multiplicity (↑p) r.num) - ↑(multiplicity ↑p ↑r.den))

pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. (↑q.den * ↑r.den)
hq' : q.num /. ↑q.den ≠ 0
hr' : r.num /. ↑r.den ≠ 0
hp' : _root_.Prime ↑p
⊢ FiniteMultiplicity (↑p) (↑q.den * ↑r.den)

pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. (↑q.den * ↑r.den)
hq' : q.num /. ↑q.den ≠ 0
hr' : r.num /. ↑r.den ≠ 0
hp' : _root_.Prime ↑p
⊢ FiniteMultiplicity (↑p) (q.num * r.num)

Tactic:
·

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. (↑q.den * ↑r.den)
hq' : q.num /. ↑q.den ≠ 0
hr' : r.num /. ↑r.den ≠ 0
hp' : _root_.Prime ↑p
⊢ ↑(multiplicity (↑p) q.num) + ↑(multiplicity (↑p) r.num) - (↑(multiplicity ↑p ↑q.den) + ↑(multiplicity ↑p ↑r.den)) =
    ↑(multiplicity (↑p) q.num) - ↑(multiplicity ↑p ↑q.den) + (↑(multiplicity (↑p) r.num) - ↑(multiplicity ↑p ↑r.den))
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. (↑q.den * ↑r.den)
hq' : q.num /. ↑q.den ≠ 0
hr' : r.num /. ↑r.den ≠ 0
hp' : _root_.Prime ↑p
⊢ FiniteMultiplicity (↑p) (↑q.den * ↑r.den)

pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. (↑q.den * ↑r.den)
hq' : q.num /. ↑q.den ≠ 0
hr' : r.num /. ↑r.den ≠ 0
hp' : _root_.Prime ↑p
⊢ FiniteMultiplicity (↑p) (q.num * r.num)

Tactic:
·

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. (↑q.den * ↑r.den)
hq' : q.num /. ↑q.den ≠ 0
hr' : r.num /. ↑r.den ≠ 0
hp' : _root_.Prime ↑p
⊢ FiniteMultiplicity (↑p) (↑q.den * ↑r.den)
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. (↑q.den * ↑r.den)
hq' : q.num /. ↑q.den ≠ 0
hr' : r.num /. ↑r.den ≠ 0
hp' : _root_.Prime ↑p
⊢ FiniteMultiplicity (↑p) (q.num * r.num)

Tactic:
·

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. (↑q.den * ↑r.den)
hq' : q.num /. ↑q.den ≠ 0
hr' : r.num /. ↑r.den ≠ 0
hp' : _root_.Prime ↑p
⊢ FiniteMultiplicity (↑p) (q.num * r.num)
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: case inl
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
⊢ padicValRat p (0 ^ k) = ↑k * padicValRat p 0

pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
k : ℕ
hq : q ≠ 0
⊢ padicValRat p (q ^ k) = ↑k * padicValRat p q

Tactic:
·

Goal state after:
case inl
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
⊢ padicValRat p (0 ^ k) = ↑k * padicValRat p 0
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: case pos
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q = 0
⊢ padicValRat p q⁻¹ = -padicValRat p q

pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : ¬q = 0
⊢ padicValRat p q⁻¹ = -padicValRat p q

Tactic:
·

Goal state after:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q = 0
⊢ padicValRat p q⁻¹ = -padicValRat p q
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : ¬q = 0
⊢ padicValRat p q⁻¹ = -padicValRat p q

Tactic:
·

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : ¬q = 0
⊢ padicValRat p q⁻¹ = -padicValRat p q
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: 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

pp: 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

Tactic:
·

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
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: 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

Tactic:
·

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
⊢ (monomorphisms C).rlp ≤ (generatingMonomorphisms G).rlp
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
⊢ (transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} (generatingMonomorphisms G)).pushouts).retracts ≤
    (transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} (monomorphisms C)).pushouts).retracts

pp: C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator G
⊢ (transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} (monomorphisms C)).pushouts).retracts ≤ monomorphisms C

Tactic:
·

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator G
⊢ (transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} (generatingMonomorphisms G)).pushouts).retracts ≤
    (transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} (monomorphisms C)).pushouts).retracts
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
⊢ (transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} (monomorphisms C)).pushouts).retracts ≤ monomorphisms C

Tactic:
·

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator G
⊢ (transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} (monomorphisms C)).pushouts).retracts ≤ monomorphisms C
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: case inl
p : ℕ
hp : Fact (Nat.Prime p)
⊢ padicNorm p ↑0 ≤ 1

pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
hz : z ≠ 0
⊢ padicNorm p ↑z ≤ 1

Tactic:
·

Goal state after:
case inl
p : ℕ
hp : Fact (Nat.Prime p)
⊢ padicNorm p ↑0 ≤ 1
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
hz : z ≠ 0
⊢ padicNorm p ↑z ≤ 1

Tactic:
·

Goal state after:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
hz : z ≠ 0
⊢ padicNorm p ↑z ≤ 1
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: case ha
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
⊢ 1 ≤ ↑p

pp: case hmn
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
⊢ -padicValRat p (q + r) ≤ -padicValRat p q

Tactic:
·

Goal state after:
case ha
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
⊢ 1 ≤ ↑p
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: case hmn
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
⊢ -padicValRat p (q + r) ≤ -padicValRat p q

Tactic:
·

Goal state after:
case hmn
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
⊢ -padicValRat p (q + r) ≤ -padicValRat p q
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
this : ∀ {q r : ℚ}, padicValRat p q ≤ padicValRat p r → padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
hle : ¬padicValRat p q ≤ padicValRat p r
⊢ padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)

pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hle : padicValRat p q ≤ padicValRat p r
⊢ padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)

Tactic:
·

Goal state after:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
this : ∀ {q r : ℚ}, padicValRat p q ≤ padicValRat p r → padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
hle : ¬padicValRat p q ≤ padicValRat p r
⊢ padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ↑z = 0
⊢ ↑(p ^ n) ∣ z ↔ 0 ≤ ↑p ^ (-↑n)

pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ ↑(p ^ n) ∣ z ↔ ↑p ^ (-padicValRat p ↑z) ≤ ↑p ^ (-↑n)

Tactic:
·

Goal state after:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ↑z = 0
⊢ ↑(p ^ n) ∣ z ↔ 0 ≤ ↑p ^ (-↑n)
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ ↑(p ^ n) ∣ z ↔ ↑p ^ (-padicValRat p ↑z) ≤ ↑p ^ (-↑n)

Tactic:
·

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ ↑(p ^ n) ∣ z ↔ ↑p ^ (-padicValRat p ↑z) ≤ ↑p ^ (-↑n)
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ ↑(p ^ n) ∣ z ↔ ↑n ≤ ↑(multiplicity (↑p) z)

pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ z ≠ 0

pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ 1 < ↑p

Tactic:
·

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ ↑(p ^ n) ∣ z ↔ ↑n ≤ ↑(multiplicity (↑p) z)
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ ↑(p ^ n) ∣ z ↔ ↑p ^ n ∣ z

pp: case neg.hf
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ FiniteMultiplicity (↑p) z

Tactic:
·

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ ↑(p ^ n) ∣ z ↔ ↑p ^ n ∣ z
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: case neg.hf
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ FiniteMultiplicity (↑p) z

Tactic:
·

Goal state after:
case neg.hf
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ FiniteMultiplicity (↑p) z
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ z ≠ 0

pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ 1 < ↑p

Tactic:
·

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ z ≠ 0
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ 1 < ↑p

Tactic:
·

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ 1 < ↑p
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: case mp
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
⊢ padicNorm p ↑m = 1 → (↑p)⁻¹ < padicNorm p ↑m

pp: case mpr
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
⊢ (↑p)⁻¹ < padicNorm p ↑m → padicNorm p ↑m = 1

Tactic:
·

Goal state after:
case mp
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
⊢ padicNorm p ↑m = 1 → (↑p)⁻¹ < padicNorm p ↑m
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: case mp
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : padicNorm p ↑m = 1
⊢ 1 < p

pp: case mp
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : padicNorm p ↑m = 1
⊢ 0 < p

Tactic:
·

Goal state after:
case mp
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : padicNorm p ↑m = 1
⊢ 1 < p
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: case mp
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : padicNorm p ↑m = 1
⊢ 0 < p

Tactic:
·

Goal state after:
case mp
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : padicNorm p ↑m = 1
⊢ 0 < p
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: case mpr
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
⊢ (↑p)⁻¹ < padicNorm p ↑m → padicNorm p ↑m = 1

Tactic:
·

Goal state after:
case mpr
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
⊢ (↑p)⁻¹ < padicNorm p ↑m → padicNorm p ↑m = 1
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: case pos
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ↑m = 0
⊢ (↑p)⁻¹ < 0 → 0 = 1

pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ¬↑m = 0
⊢ (↑p)⁻¹ < ↑p ^ (-padicValRat p ↑m) → ↑p ^ (-padicValRat p ↑m) = 1

Tactic:
·

Goal state after:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ↑m = 0
⊢ (↑p)⁻¹ < 0 → 0 = 1
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ¬↑m = 0
⊢ (↑p)⁻¹ < ↑p ^ (-padicValRat p ↑m) → ↑p ^ (-padicValRat p ↑m) = 1

Tactic:
·

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ¬↑m = 0
⊢ (↑p)⁻¹ < ↑p ^ (-padicValRat p ↑m) → ↑p ^ (-padicValRat p ↑m) = 1
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: case pos
p : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
d : ℕ
hd : (∀ i < d, 0 < padicValRat p (F i)) → ∑ i ∈ Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i ∈ Finset.range d, F i)
hF : ∀ i < d + 1, 0 < padicValRat p (F i)
hn0 : ∑ x ∈ Finset.range d, F x + F d ≠ 0
h : ∑ x ∈ Finset.range d, F x = 0
⊢ 0 < padicValRat p (∑ x ∈ Finset.range d, F x + F d)

pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
d : ℕ
hd : (∀ i < d, 0 < padicValRat p (F i)) → ∑ i ∈ Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i ∈ Finset.range d, F i)
hF : ∀ i < d + 1, 0 < padicValRat p (F i)
hn0 : ∑ x ∈ Finset.range d, F x + F d ≠ 0
h : ¬∑ x ∈ Finset.range d, F x = 0
⊢ 0 < padicValRat p (∑ x ∈ Finset.range d, F x + F d)

Tactic:
·

Goal state after:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
d : ℕ
hd : (∀ i < d, 0 < padicValRat p (F i)) → ∑ i ∈ Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i ∈ Finset.range d, F i)
hF : ∀ i < d + 1, 0 < padicValRat p (F i)
hn0 : ∑ x ∈ Finset.range d, F x + F d ≠ 0
h : ∑ x ∈ Finset.range d, F x = 0
⊢ 0 < padicValRat p (∑ x ∈ Finset.range d, F x + F d)
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
d : ℕ
hd : (∀ i < d, 0 < padicValRat p (F i)) → ∑ i ∈ Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i ∈ Finset.range d, F i)
hF : ∀ i < d + 1, 0 < padicValRat p (F i)
hn0 : ∑ x ∈ Finset.range d, F x + F d ≠ 0
h : ¬∑ x ∈ Finset.range d, F x = 0
⊢ 0 < padicValRat p (∑ x ∈ Finset.range d, F x + F d)

Tactic:
·

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
d : ℕ
hd : (∀ i < d, 0 < padicValRat p (F i)) → ∑ i ∈ Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i ∈ Finset.range d, F i)
hF : ∀ i < d + 1, 0 < padicValRat p (F i)
hn0 : ∑ x ∈ Finset.range d, F x + F d ≠ 0
h : ¬∑ x ∈ Finset.range d, F x = 0
⊢ 0 < padicValRat p (∑ x ∈ Finset.range d, F x + F d)
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: case inl
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
ht : 0 < t
hF : ∀ i ∈ ∅, padicNorm p (F i) < t
⊢ padicNorm p (∑ i ∈ ∅, F i) < t

pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
hF : ∀ i ∈ s, padicNorm p (F i) < t
ht : 0 < t
hs : s.Nonempty
⊢ padicNorm p (∑ i ∈ s, F i) < t

Tactic:
·

Goal state after:
case inl
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
ht : 0 < t
hF : ∀ i ∈ ∅, padicNorm p (F i) < t
⊢ padicNorm p (∑ i ∈ ∅, F i) < t
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
hF : ∀ i ∈ s, padicNorm p (F i) < t
ht : 0 < t
hs : s.Nonempty
⊢ padicNorm p (∑ i ∈ s, F i) < t

Tactic:
·

Goal state after:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
hF : ∀ i ∈ s, padicNorm p (F i) < t
ht : 0 < t
hs : s.Nonempty
⊢ padicNorm p (∑ i ∈ s, F i) < t
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: case inl
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
ht : 0 ≤ t
hF : ∀ i ∈ ∅, padicNorm p (F i) ≤ t
⊢ padicNorm p (∑ i ∈ ∅, F i) ≤ t

pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
hF : ∀ i ∈ s, padicNorm p (F i) ≤ t
ht : 0 ≤ t
hs : s.Nonempty
⊢ padicNorm p (∑ i ∈ s, F i) ≤ t

Tactic:
·

Goal state after:
case inl
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
ht : 0 ≤ t
hF : ∀ i ∈ ∅, padicNorm p (F i) ≤ t
⊢ padicNorm p (∑ i ∈ ∅, F i) ≤ t
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
hF : ∀ i ∈ s, padicNorm p (F i) ≤ t
ht : 0 ≤ t
hs : s.Nonempty
⊢ padicNorm p (∑ i ∈ s, F i) ≤ t

Tactic:
·

Goal state after:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
hF : ∀ i ∈ s, padicNorm p (F i) ≤ t
ht : 0 ≤ t
hs : s.Nonempty
⊢ padicNorm p (∑ i ∈ s, F i) ≤ t
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: case inl
p b : ℕ
hp : Fact (Nat.Prime p)
h : b ∣ 0
⊢ padicValNat p (0 / b) = padicValNat p 0 - padicValNat p b

pp: case inr
p a b : ℕ
hp : Fact (Nat.Prime p)
h : b ∣ a
ha : a ≠ 0
⊢ padicValNat p (a / b) = padicValNat p a - padicValNat p b

Tactic:
·

Goal state after:
case inl
p b : ℕ
hp : Fact (Nat.Prime p)
h : b ∣ 0
⊢ padicValNat p (0 / b) = padicValNat p 0 - padicValNat p b
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℤ_[p]
h : ‖z1 + z2‖ < ‖z1‖
hne : ¬‖z1‖ = ‖z2‖
⊢ ‖z1‖ ≤ ‖z1 + z2‖

Tactic:
by rw [norm_add_eq_max_of_ne hne]; apply le_max_left

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

Goal state before:
pp: case inl
p : ℕ
hp : p ≠ 1
n : ℕ
⊢ p ^ n ∣ 0 ↔ 0 = 0 ∨ n ≤ padicValNat p 0

pp: case inr
p : ℕ
hp : p ≠ 1
n a : ℕ
ha : a ≠ 0
⊢ p ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValNat p a

Tactic:
·

Goal state after:
case inl
p : ℕ
hp : p ≠ 1
n : ℕ
⊢ p ^ n ∣ 0 ↔ 0 = 0 ∨ n ≤ padicValNat p 0
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: case inr
p : ℕ
hp : p ≠ 1
n a : ℕ
ha : a ≠ 0
⊢ p ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValNat p a

Tactic:
·

Goal state after:
case inr
p : ℕ
hp : p ≠ 1
n a : ℕ
ha : a ≠ 0
⊢ p ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValNat p a
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: case h
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ ε⁻¹ < (↑p ^ (-↑k))⁻¹

pp: p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ 0 < ↑p

Tactic:
·

Goal state after:
case h
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ ε⁻¹ < (↑p ^ (-↑k))⁻¹
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: case zero
p : ℕ
⊢ padicValNat p 0 ≤ log p 0

pp: case succ
p n : ℕ
⊢ padicValNat p (n + 1) ≤ log p (n + 1)

Tactic:
·

Goal state after:
case zero
p : ℕ
⊢ padicValNat p 0 ≤ log p 0
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ 0 < ↑p

Tactic:
·

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ 0 < ↑p
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: case succ.zero
n : ℕ
⊢ padicValNat 0 (n + 1) ≤ log 0 (n + 1)

pp: case succ.succ.zero
n : ℕ
⊢ padicValNat (0 + 1) (n + 1) ≤ log (0 + 1) (n + 1)

pp: case succ.succ.succ
n p : ℕ
⊢ padicValNat (p + 1 + 1) (n + 1) ≤ log (p + 1 + 1) (n + 1)

Tactic:
·

Goal state after:
case succ.zero
n : ℕ
⊢ padicValNat 0 (n + 1) ≤ log 0 (n + 1)
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: case succ.succ.zero
n : ℕ
⊢ padicValNat (0 + 1) (n + 1) ≤ log (0 + 1) (n + 1)

pp: case succ.succ.succ
n p : ℕ
⊢ padicValNat (p + 1 + 1) (n + 1) ≤ log (p + 1 + 1) (n + 1)

Tactic:
·

Goal state after:
case succ.succ.zero
n : ℕ
⊢ padicValNat (0 + 1) (n + 1) ≤ log (0 + 1) (n + 1)
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: case pos
p a : ℕ
hp : Fact (Nat.Prime p)
ha : p < a
dvd : p ∣ a
⊢ padicValNat p a + p ≤ a

pp: case neg
p a : ℕ
hp : Fact (Nat.Prime p)
ha : p < a
dvd : ¬p ∣ a
⊢ padicValNat p a + p ≤ a

Tactic:
·

Goal state after:
case pos
p a : ℕ
hp : Fact (Nat.Prime p)
ha : p < a
dvd : p ∣ a
⊢ padicValNat p a + p ≤ a
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p a : ℕ
hp : Fact (Nat.Prime p)
ha : p < a
k : ℕ
hk : a = p * k
⊢ k ≠ 0

Tactic:
by lia

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

Goal state before:
pp: p a : ℕ
hp : Fact (Nat.Prime p)
ha : p < a
k : ℕ
hk : a = p * k
this : padicValNat p k < k
⊢ p ≠ 0

Tactic:
by lia

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

Goal state before:
pp: p a : ℕ
hp : Fact (Nat.Prime p)
ha : p < a
k : ℕ
hk : a = p * k
this : padicValNat p k < k
⊢ k ≠ 0

Tactic:
by lia

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

Goal state before:
pp: p a : ℕ
hp : Fact (Nat.Prime p)
ha : p < a
k : ℕ
hk : a = p * k
this : padicValNat p k < k
⊢ 1 + padicValNat p k + p ≤ p + k

Tactic:
by lia

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

Goal state before:
pp: p a : ℕ
hp : Fact (Nat.Prime p)
ha : p < a
k : ℕ
hk : a = p * k
this : padicValNat p k < k
⊢ 2 ≤ k

Tactic:
by lia

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

Goal state before:
pp: case neg
p a : ℕ
hp : Fact (Nat.Prime p)
ha : p < a
dvd : ¬p ∣ a
⊢ padicValNat p a + p ≤ a

Tactic:
·

Goal state after:
case neg
p a : ℕ
hp : Fact (Nat.Prime p)
ha : p < a
dvd : ¬p ∣ a
⊢ padicValNat p a + p ≤ a
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
⊢ n ≠ 0

Tactic:
by lia

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

Goal state before:
pp: case inl
p : ℕ
hp : Fact (Nat.Prime p)
⊢ 0 ≤ (↑0).valuation

pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ 0 ≤ (↑x).valuation

Tactic:
·

Goal state after:
case inl
p : ℕ
hp : Fact (Nat.Prime p)
⊢ 0 ≤ (↑0).valuation
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p n : ℕ
hn : n ≠ 0
k : ℕ
hk : k < padicValNat p n + 1
⊢ k ≤ padicValNat p n

Tactic:
by lia

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

Goal state before:
pp: case inl
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Finset.image (fun t ↦ p ^ (t + 1)) (Finset.range (padicValNat p 0)) ⊆ (divisors 0).erase 1

pp: case inr
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
⊢ Finset.image (fun t ↦ p ^ (t + 1)) (Finset.range (padicValNat p n)) ⊆ n.divisors.erase 1

Tactic:
·

Goal state after:
case inl
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Finset.image (fun t ↦ p ^ (t + 1)) (Finset.range (padicValNat p 0)) ⊆ (divisors 0).erase 1
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ ↑x = ↑x * ↑p ^ (-↑x.valuation + ↑x.valuation)

pp: case ha
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ ↑p ≠ 0

Tactic:
·

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ ↑x = ↑x * ↑p ^ (-↑x.valuation + ↑x.valuation)
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: case ha
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ ↑p ≠ 0

Tactic:
·

Goal state after:
case ha
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ ↑p ≠ 0