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

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
norm_denom_lt : ‖↑r.den‖ < 1
⊢ ‖↑r * ↑r.den‖ = ‖↑r.num‖

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
norm_denom_lt : ‖↑r.den‖ < 1
hr : ‖↑r‖ * ‖↑r.den‖ = ‖↑r.num‖
⊢ ‖↑r.num‖ < 1

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
⊢ (p - 1) * padicValNat p n ! < n

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
norm_denom_lt : ‖↑r.den‖ < 1
hr : ‖↑r‖ * ‖↑r.den‖ = ‖↑r.num‖
key : ‖↑r.num‖ < 1
⊢ ↑p ∣ r.num ∧ ↑p ∣ ↑r.den

Tactic:
by

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ∀ (x y : ℚ),
    (if x + y = 0 then 0 else exp (-padicValRat p (x + y))) ≤
      max (if x = 0 then 0 else exp (-padicValRat p x)) (if y = 0 then 0 else exp (-padicValRat p y))

Tactic:
by

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℚ
⊢ (padicValuation p) x = 0 ↔ x = 0

Tactic:
by

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℤ
⊢ (padicValuation p) x = 0 ↔ x = 0

Tactic:
by

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ (padicValuation p) ↑p = exp (-1)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℤ
h✝ : ¬x = 0
⊢ exp (-↑(padicValInt p x)) ≤ 1

Tactic:
← le_log_iff_exp_le

Goal state after:
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℤ
h✝ : ¬x = 0
⊢ -↑(padicValInt p x) ≤ log 1

case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℤ
h✝ : ¬x = 0
⊢ 1 ≠ 0
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℤ
⊢ (padicValuation p) x ≤ 1

Tactic:
by

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℤ
⊢ (padicValuation p) x = 1 ↔ ¬↑p ∣ x

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ padicValNat p n ! ≤ n

Tactic:
by

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℤ
⊢ (padicValuation p) x < 1 ↔ ↑p ∣ x

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
⊢ IsUnit ↑r.den

Tactic:
by

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

Goal state before:
pp: p n k b : ℕ
hp : Fact (Nat.Prime p)
hkn : k ≤ n
hnb : log p n < b
⊢ padicValNat p (n.choose k) = #({i ∈ Finset.Ico 1 b | p ^ i ≤ k % p ^ i + (n - k) % p ^ i})

Tactic:
by

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

Goal state before:
pp: p n k b : ℕ
hp : Fact (Nat.Prime p)
hnb : log p (n + k) < b
⊢ padicValNat p ((n + k).choose k) = #({i ∈ Finset.Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i})

Tactic:
by

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

Goal state before:
pp: p k n : ℕ
hp : Fact (Nat.Prime p)
⊢ k ≤ n + k

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ ‖x‖ ≤ ↑p ^ (-↑n) ↔ n ≤ x.valuation

Tactic:
rw [norm_eq_zpow_neg_valuation hx, zpow_le_zpow_iff_right₀, neg_le_neg_iff, Nat.cast_le]
  exact mod_cast hp.out.one_lt

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ ‖x‖ ≤ ↑p ^ (-↑n) ↔ n ≤ x.valuation

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hx : ↑p ^ n * c ≠ 0
this : c ≠ 0
⊢ n ≤ (↑p ^ n * c).valuation

Tactic:
by

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

Goal state before:
pp: case mp
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hx : ↑p ^ n * c ≠ 0
⊢ c ≠ 0

Tactic:
contrapose hx

Goal state after:
case mp
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hx : c = 0
⊢ ↑p ^ n * c = 0
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ x ∈ Ideal.span {↑p ^ n} ↔ n ≤ x.valuation

Tactic:
by

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℚ
⊢ (padicValuation p) x ≤ 1 ↔ ¬p ∣ x.den

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℤ
⊢ ‖↑x‖ ≤ ↑p ^ n ↔ ‖↑x‖ < ↑p ^ (n + 1)

Tactic:
exact Padic.norm_le_pow_iff_norm_lt_pow_add_one _ _

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℤ
⊢ ‖x‖ ≤ ↑p ^ n ↔ ‖x‖ < ↑p ^ (n + 1)

Tactic:
by

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

Goal state before:
pp: p k n : ℕ
hp : Fact (Nat.Prime p)
⊢ (p - 1) * padicValNat p ((n + k).choose k) = (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ Function.Surjective ⇑(padicValuation p)

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℤ
⊢ ‖x‖ < ↑p ^ n ↔ ‖x‖ ≤ ↑p ^ (n - 1)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : p ≠ 1
n : ℕ
a : ℤ
⊢ ↑p ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValInt p a

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ‖x‖ < 1 ↔ ↑p ∣ x

Tactic:
by

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

Goal state before:
pp: p : ℕ
a : ℤ
⊢ ↑p ^ padicValInt p a ∣ a

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
⊢ ∀ (a b : ℤ_[p]), a ∈ nonunits ℤ_[p] → b ∈ nonunits ℤ_[p] → a + b ∈ nonunits ℤ_[p]

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ ↑p ∈ nonunits ℤ_[p]

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
a b : ℤ
ha : a ≠ 0
hb : b ≠ 0
⊢ padicValInt p (a * b) = padicValInt p a + padicValInt p b

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
ha : a ≠ 0
⊢ padicValInt p (a * ↑p) = padicValInt p a + 1

Tactic:
by

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

Goal state before:
pp: X : Scheme
⊢ IsGrothendieckAbelian.{u + 1, u + 1, u + 2} (Sheaf (ProEt.topology X) Ab)

Tactic:
by

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

Goal state before:
pp: X : Scheme
ℓ : ℕ
inst✝¹ : Fact (Nat.Prime ℓ)
inst✝ : IsEmpty ↥X
n : ℕ
⊢ Subsingleton (X.EllAdicCohomology ℓ n)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ Prime ↑p

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.SheafCohomology.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
F G : Sheaf J AddCommGrpCat
f : F ⟶ G
x : F.H 0
⊢ Ext.addEquiv₀ ((map f 0) x) = Ext.addEquiv₀ x ≫ f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.SheafCohomology.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
T : C
hT : Limits.IsTerminal T
F G : Sheaf J AddCommGrpCat
f : F ⟶ G
x : F.H 0
⊢ (ConcreteCategory.hom (f.hom.app (op T))) ((equiv₀ F hT) x) = (equiv₀ G hT) ((map f 0) x)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.SheafCohomology.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
T : C
hT : Limits.IsTerminal T
F G : Sheaf J AddCommGrpCat
f : F ⟶ G
x : ↑(F.obj.obj (op T))
⊢ (map f 0) ((equiv₀ F hT).symm x) = (equiv₀ G hT).symm ((ConcreteCategory.hom (f.hom.app (op T))) x)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.SheafCohomology.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
F : Sheaf J AddCommGrpCat
n : ℕ
x : F.H n
⊢ (map (𝟙 F) n) x = x

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.SheafCohomology.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
F G : Sheaf J AddCommGrpCat
f : F ⟶ G
n : ℕ
G' : Sheaf J AddCommGrpCat
g : G ⟶ G'
x : F.H n
⊢ (map (f ≫ g) n) x = (map g n) ((map f n) x)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.SheafCohomology.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
F G : Sheaf J AddCommGrpCat
n : ℕ
f g : F ⟶ G
x : F.H n
⊢ (map (f + g) n) x = (map f n) x + (map g n) x

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.SheafCohomology.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
F : Sheaf J AddCommGrpCat
h : Limits.IsZero F
n : ℕ
⊢ Subsingleton (F.H n)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
Φ : J.Point
⊢ presheafFiber (𝟙 Φ) = 𝟙 Φ.presheafFiber

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
Φ₁ Φ₂ Φ₃ : J.Point
f : Φ₁ ⟶ Φ₂
g : Φ₂ ⟶ Φ₃
⊢ presheafFiber (f ≫ g) = presheafFiber g ≫ presheafFiber f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
Φ : J.Point
⊢ sheafFiber (𝟙 Φ) = 𝟙 Φ.sheafFiber

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
Φ₁ Φ₂ Φ₃ : J.Point
f : Φ₁ ⟶ Φ₂
g : Φ₂ ⟶ Φ₃
⊢ sheafFiber (f ≫ g) = sheafFiber g ≫ sheafFiber f

Tactic:
by

Goal state after:
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
⊢ padicNorm p (↑f m) = padicNorm p (↑f n)

Tactic:
by

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

Goal state before:
pp: case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ ↑p ^ (-↑m)
x' : CauSeq ℤ_[p] norm := ⟨x, ⋯⟩
⊢ ∃ L, ∀ (n : ℕ), ‖x n - L‖ ≤ ↑p ^ (-↑n)

Tactic:
· refine ⟨x'.lim, fun n => ?_⟩
      have : (0 : ℝ) < (p : ℝ) ^ (-n : ℤ) := zpow_pos (mod_cast hp.out.pos) _
      obtain ⟨i, hi⟩ := equiv_def₃ (equiv_lim x') this
      by_cases! hin : i ≤ n
      · exact (hi i le_rfl n hin).le
      · specialize hi i le_rfl i le_rfl
        specialize hx hin.le
        have := nonarchimedean (x n - x i : ℤ_[p]) (x i - x'.lim)
        rw [sub_add_sub_cancel] at this
        exact this.trans (max_le_iff.mpr ⟨hx, hi.le⟩)

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → x m ≡ x n [SMOD maximalIdeal ℤ_[p] ^ m • ⊤]
⊢ ∃ L, ∀ (n : ℕ), x n ≡ L [SMOD maximalIdeal ℤ_[p] ^ n • ⊤]

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x✝¹ y : ℤ_[p]
x✝ : ↥(nonZeroDivisors ℤ_[p])
x : ℤ_[p]
hx : x ∈ nonZeroDivisors ℤ_[p]
⊢ IsUnit ((algebraMap ℤ_[p] ℚ_[p]) ↑⟨x, hx⟩)

Tactic:
by

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
⊢ f.norm = 0 ↔ f ≈ 0

Tactic:
by

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)
hf : f ≈ 0
ε : ℚ
hε : ε > 0
i : ℕ
hi : ∀ j ≥ i, padicNorm p (↑(f - 0) j) < ε
j : ℕ
hj : j ≥ i
⊢ padicNorm p (↑(g - 0) j) < ε

Tactic:
by

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
⊢ f.norm = padicNorm p (↑f (stationaryPoint hf))

Tactic:
by

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
heq : f.norm = padicNorm p (↑f (stationaryPoint hf))
h : ↑f (stationaryPoint hf) = 0
⊢ f.norm = 0

Tactic:
by

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
h : (const (padicNorm p) q - 0).LimZero
⊢ (const (padicNorm p) q).LimZero

Tactic:
by

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : f ≈ 0
⊢ 0 ≤ f.norm

Tactic:
by

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
⊢ 0 ≤ f.norm

Tactic:
by

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
⊢ 0 ≤ f.norm

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.TypeValuedFlat

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Type w
inst✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits F
X : C
x : F.obj X
Y : C
y : F.obj Y
h : IsLimit (BinaryFan.mk (F.map prod.fst) (F.map prod.snd)) :=
  mapIsLimitOfPreservesOfIsLimit F prod.fst prod.snd (prodIsProd X Y)
h' : IsLimit (Types.binaryProductCone (F.obj X) (F.obj Y)) := Types.binaryProductLimit (F.obj X) (F.obj Y)
⊢ True

Tactic:
by

Goal state after:
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
⊢ 0 ≤ -x.valuation

Tactic:
rw [Right.nonneg_neg_iff]

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
⊢ x.valuation ≤ 0
Module: Mathlib.CategoryTheory.Functor.TypeValuedFlat

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Type w
inst✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits F
⊢ ∀ (X Y : F.Elements), ∃ W x x, True

Tactic:
by

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v2 v3 : ℕ
⊢ padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑f (max (stationaryPoint hf) (max v2 v3)))

Tactic:
by

Goal state after:
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
⊢ ↑n = -x.valuation

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.TypeValuedFlat

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Type w
inst✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits F
X : C
x : F.obj X
Y : C
y : F.obj Y
f : X ⟶ Y
hf✝ : (ConcreteCategory.hom (F.map f)) x = y
g : X ⟶ Y
hf : (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map g)) x
hg : (ConcreteCategory.hom (F.map g)) x = y
h : IsLimit (Fork.ofι (F.map (equalizer.ι f g)) ⋯) := isLimitForkMapOfIsLimit F ⋯ (equalizerIsEqualizer f g)
h' : IsLimit Types.equalizerLimit.cone := Types.equalizerLimit.isLimit
⊢ ⟨equalizer.ι f g, ⋯⟩ ≫ ⟨f, hf✝⟩ = ⟨equalizer.ι f g, ⋯⟩ ≫ ⟨g, hg⟩

Tactic:
by

Goal state after:
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
⊢ x ≠ 0

Tactic:
by

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v3 : ℕ
⊢ padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑f (max v1 (max (stationaryPoint hf) v3)))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.TypeValuedFlat

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Type w
inst✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits F
⊢ ∀ ⦃X Y : F.Elements⦄ (f g : X ⟶ Y), ∃ W h, h ≫ f = h ≫ g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.TypeValuedFlat

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
X : C
x : F.obj X
U✝ V✝ : Over X
x✝² : U✝ ⟶ V✝
x✝¹ : (Over.forget X ⋙ F).obj U✝
x✝ : x✝¹ ∈ ⇑(ConcreteCategory.hom (F.map U✝.hom)) ⁻¹' {x}
⊢ x✝¹ ∈ ⇑(ConcreteCategory.hom ((Over.forget X ⋙ F).map x✝²)) ⁻¹' ⇑(ConcreteCategory.hom (F.map V✝.hom)) ⁻¹' {x}

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.TypeValuedFlat

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
X : C
x : F.obj X
X✝ Y✝ : Over (F.elementsMk X x)
f : X✝ ⟶ Y✝
⊢ (ConcreteCategory.hom ((fromOverFunctor F x).map (Over.homMk ↑(Over.Hom.left f) ⋯)))
      ((fromOverFunctor F x).elementsMk (Over.mk ↑X✝.hom) ⟨X✝.left.snd, ⋯⟩).snd =
    ((fromOverFunctor F x).elementsMk (Over.mk ↑Y✝.hom) ⟨Y✝.left.snd, ⋯⟩).snd

Tactic:
by

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v2 : ℕ
⊢ padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑f (max v1 (max v2 (stationaryPoint hf))))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.TypeValuedFlat

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
X✝ : C
x : F.obj X✝
X : (fromOverFunctor F x).Elements
⊢ { obj := fun u ↦ Over.mk (homMk (F.elementsMk u.fst.left ↑u.snd) (F.elementsMk X✝ x) u.fst.hom ⋯),
            map := fun {X Y} f ↦
              Over.homMk
                (homMk (Over.mk (homMk (F.elementsMk X.fst.left ↑X.snd) (F.elementsMk X✝ x) X.fst.hom ⋯)).left
                  (Over.mk (homMk (F.elementsMk Y.fst.left ↑Y.snd) (F.elementsMk X✝ x) Y.fst.hom ⋯)).left
                  (Over.Hom.left ↑f) ⋯)
                ⋯,
            map_id := ⋯, map_comp := ⋯ }.map
        ((Iso.refl (𝟭 (fromOverFunctor F x).Elements)).hom.app X) ≫
      (Iso.refl
              ({ obj := fun u ↦ (fromOverFunctor F x).elementsMk (Over.mk ↑u.hom) ⟨u.left.snd, ⋯⟩,
                  map := fun {X Y} f ↦
                    homMk ((fromOverFunctor F x).elementsMk (Over.mk ↑X.hom) ⟨X.left.snd, ⋯⟩)
                      ((fromOverFunctor F x).elementsMk (Over.mk ↑Y.hom) ⟨Y.left.snd, ⋯⟩)
                      (Over.homMk ↑(Over.Hom.left f) ⋯) ⋯,
                  map_id := ⋯, map_comp := ⋯ } ⋙
                { obj := fun u ↦ Over.mk (homMk (F.elementsMk u.fst.left ↑u.snd) (F.elementsMk X✝ x) u.fst.hom ⋯),
                  map := fun {X Y} f ↦
                    Over.homMk
                      (homMk (Over.mk (homMk (F.elementsMk X.fst.left ↑X.snd) (F.elementsMk X✝ x) X.fst.hom ⋯)).left
                        (Over.mk (homMk (F.elementsMk Y.fst.left ↑Y.snd) (F.elementsMk X✝ x) Y.fst.hom ⋯)).left
                        (Over.Hom.left ↑f) ⋯)
                      ⋯,
                  map_id := ⋯, map_comp := ⋯ })).hom.app
        ({ obj := fun u ↦ Over.mk (homMk (F.elementsMk u.fst.left ↑u.snd) (F.elementsMk X✝ x) u.fst.hom ⋯),
              map := fun {X Y} f ↦
                Over.homMk
                  (homMk (Over.mk (homMk (F.elementsMk X.fst.left ↑X.snd) (F.elementsMk X✝ x) X.fst.hom ⋯)).left
                    (Over.mk (homMk (F.elementsMk Y.fst.left ↑Y.snd) (F.elementsMk X✝ x) Y.fst.hom ⋯)).left
                    (Over.Hom.left ↑f) ⋯)
                  ⋯,
              map_id := ⋯, map_comp := ⋯ }.obj
          X) =
    𝟙
      ({ obj := fun u ↦ Over.mk (homMk (F.elementsMk u.fst.left ↑u.snd) (F.elementsMk X✝ x) u.fst.hom ⋯),
            map := fun {X Y} f ↦
              Over.homMk
                (homMk (Over.mk (homMk (F.elementsMk X.fst.left ↑X.snd) (F.elementsMk X✝ x) X.fst.hom ⋯)).left
                  (Over.mk (homMk (F.elementsMk Y.fst.left ↑Y.snd) (F.elementsMk X✝ x) Y.fst.hom ⋯)).left
                  (Over.Hom.left ↑f) ⋯)
                ⋯,
            map_id := ⋯, map_comp := ⋯ }.obj
        X)

Tactic:
by

Goal state after: