awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
p : ℕ
hfp : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      p ≤ m
hprime : Nat.Prime p
hprime_fact : Fact (Nat.Prime p)
obtain :
  ∀ (t : ℝ) (h : 0 < t ∧ (f : (a : ℚ) → ℝ) (↑p : ℚ) = HPow.hPow (α := ℝ) (↑p : ℝ) (-t)),
    ∃! p : ℕ, ∃ (x : Fact (Nat.Prime p)), f.IsEquiv (padic p)
⊢ ∃! p : ℕ, ∃ (x : Fact (Nat.Prime p)), f.IsEquiv (padic p)

Tactic:
obtain ⟨t, h⟩ := exists_pos_eq_pow_neg hfp.1 hfp.2 hmin

Premises used: Rat.AbsoluteValue.exists_pos_eq_pow_neg, And.right, And.left
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
p : ℕ
hfp : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      p ≤ m
hprime : Nat.Prime p
hprime_fact : Fact (Nat.Prime p)
t : ℝ
h : 0 < t ∧ (f : (a : ℚ) → ℝ) (↑p : ℚ) = HPow.hPow (α := ℝ) (↑p : ℝ) (-t)
simp_rw :
  ∃! p : ℕ,
    ∃ (h : Fact (Nat.Prime p)) (c : ℝ),
      0 < c ∧ ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (padic p : (a : ℚ) → ℝ) (↑n : ℚ)
⊢ ∃! p : ℕ, ∃ (x : Fact (Nat.Prime p)), f.IsEquiv (padic p)

Tactic:
simp_rw [← exists_nat_rpow_iff_isEquiv]

Premises used: Rat.AbsoluteValue.exists_nat_rpow_iff_isEquiv
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
p : ℕ
hfp : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      p ≤ m
hprime : Nat.Prime p
hprime_fact : Fact (Nat.Prime p)
t : ℝ
h : 0 < t ∧ (f : (a : ℚ) → ℝ) (↑p : ℚ) = HPow.hPow (α := ℝ) (↑p : ℝ) (-t)
⊢ ∃! p : ℕ,
    ∃ (h : Fact (Nat.Prime p)) (c : ℝ),
      0 < c ∧ ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (padic p : (a : ℚ) → ℝ) (↑n : ℚ)

Tactic:
⟨p, ⟨hprime_fact, t⁻¹, inv_pos_of_pos h.1, fun n ↦ ?_⟩, fun q ⟨hq_prime, h_equiv⟩ ↦ ?_⟩

Premises used: _private.0.Rat.AbsoluteValue.equiv_padic_of_bounded.match_1, inv_pos_of_pos, Inv.inv, And.left, ExistsUnique, And.intro, Exists.intro, Eq
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
p : ℕ
hfp : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      p ≤ m
hprime : Nat.Prime p
hprime_fact : Fact (Nat.Prime p)
t : ℝ
h : 0 < t ∧ (f : (a : ℚ) → ℝ) (↑p : ℚ) = HPow.hPow (α := ℝ) (↑p : ℝ) (-t)
refine_1 : ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) t⁻¹ = (padic p : (a : ℚ) → ℝ) (↑n : ℚ)
refine_2 :
  ∀ (q : ℕ),
    (fun (p : ℕ) ↦
          ∃ (h : Fact (Nat.Prime p)) (c : ℝ),
            0 < c ∧ ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (padic p : (a : ℚ) → ℝ) (↑n : ℚ))
        q →
      ∀ (hq_prime : Fact (Nat.Prime q))
        (h_equiv :
          ∃ (c : ℝ),
            0 < c ∧
              ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (padic q : (a : ℚ) → ℝ) (↑n : ℚ)),
        q = p
⊢ ∃! p : ℕ,
    ∃ (h : Fact (Nat.Prime p)) (c : ℝ),
      0 < c ∧ ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (padic p : (a : ℚ) → ℝ) (↑n : ℚ)

Tactic:
refine ⟨p, ⟨hprime_fact, t⁻¹, inv_pos_of_pos h.1, fun n ↦ ?_⟩, fun q ⟨hq_prime, h_equiv⟩ ↦ ?_⟩
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
p : ℕ
hfp : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      p ≤ m
hprime : Nat.Prime p
hprime_fact : Fact (Nat.Prime p)
t : ℝ
h : 0 < t ∧ (f : (a : ℚ) → ℝ) (↑p : ℚ) = HPow.hPow (α := ℝ) (↑p : ℝ) (-t)
n : ℕ
⊢ t⁻¹ ≠ 0

Tactic:
have ht : t⁻¹ ≠ 0 := inv_ne_zero h.1.ne'
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
p : ℕ
hfp : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      p ≤ m
hprime : Nat.Prime p
hprime_fact : Fact (Nat.Prime p)
t : ℝ
h : 0 < t ∧ (f : (a : ℚ) → ℝ) (↑p : ℚ) = HPow.hPow (α := ℝ) (↑p : ℝ) (-t)
n : ℕ
ht : t⁻¹ ≠ 0
refine_1 : HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑0 : ℚ) : ℝ) t⁻¹ = (padic p : (a : ℚ) → ℝ) (↑0 : ℚ)
refine_1₁ : ∀ (hn : n ≠ 0), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) t⁻¹ = (padic p : (a : ℚ) → ℝ) (↑n : ℚ)
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) t⁻¹ = (padic p : (a : ℚ) → ℝ) (↑n : ℚ)

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
p : ℕ
hfp : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      p ≤ m
hprime : Nat.Prime p
hprime_fact : Fact (Nat.Prime p)
t : ℝ
h : 0 < t ∧ (f : (a : ℚ) → ℝ) (↑p : ℚ) = HPow.hPow (α := ℝ) (↑p : ℝ) (-t)
ht : t⁻¹ ≠ 0
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑0 : ℚ) : ℝ) t⁻¹ = (padic p : (a : ℚ) → ℝ) (↑0 : ℚ)

Tactic:
simp [ht]
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
p : ℕ
hfp : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      p ≤ m
hprime : Nat.Prime p
hprime_fact : Fact (Nat.Prime p)
t : ℝ
h : 0 < t ∧ (f : (a : ℚ) → ℝ) (↑p : ℚ) = HPow.hPow (α := ℝ) (↑p : ℝ) (-t)
n : ℕ
ht : t⁻¹ ≠ 0
hn : n ≠ 0
refine_1 :
  ∀ (e m : ℕ) (hpm : ¬p ∣ m) (hn : p ^ e * m ≠ 0),
    HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(p ^ e * m) : ℚ) : ℝ) t⁻¹ = (padic p : (a : ℚ) → ℝ) (↑(p ^ e * m) : ℚ)
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) t⁻¹ = (padic p : (a : ℚ) → ℝ) (↑n : ℚ)

Tactic:
rcases Nat.exists_eq_pow_mul_and_not_dvd hn p hprime.ne_one with ⟨e, m, hpm, rfl⟩

Premises used: Nat.Prime.ne_one, Nat.exists_eq_pow_mul_and_not_dvd, rfl
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
p : ℕ
hfp : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      p ≤ m
hprime : Nat.Prime p
hprime_fact : Fact (Nat.Prime p)
t : ℝ
h : 0 < t ∧ (f : (a : ℚ) → ℝ) (↑p : ℚ) = HPow.hPow (α := ℝ) (↑p : ℝ) (-t)
ht : t⁻¹ ≠ 0
e m : ℕ
hpm : ¬p ∣ m
hn : p ^ e * m ≠ 0
refine_1 :
  (HPow.hPow (α := ℝ) (↑p : ℝ) (-t) ^ e * 1) ^ t⁻¹ = (HPow.hPow (α := ℝ) (↑p : ℝ) e)⁻¹ * (↑(padicNorm p (↑m : ℚ)) : ℝ)
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(p ^ e * m) : ℚ) : ℝ) t⁻¹ = (padic p : (a : ℚ) → ℝ) (↑(p ^ e * m) : ℚ)

Tactic:
simp only [Nat.cast_mul, Nat.cast_pow, map_mul, map_pow, h.2,
        eq_one_of_not_dvd bdd hfp.1 hfp.2 hmin hpm, padic_eq_padicNorm,
        padicNorm.padicNorm_p_of_prime, cast_inv, cast_natCast, inv_pow]

Premises used: Rat.AbsoluteValue.eq_one_of_not_dvd, padicNorm.padicNorm_p_of_prime, Rat.AbsoluteValue.padic_eq_padicNorm, map_pow, inv_pow, map_mul, Rat.cast_inv, Nat.cast_mul, And.right, And.left, Rat.cast_natCast, Nat.cast_pow
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
p : ℕ
hfp : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      p ≤ m
hprime : Nat.Prime p
hprime_fact : Fact (Nat.Prime p)
t : ℝ
h : 0 < t ∧ (f : (a : ℚ) → ℝ) (↑p : ℚ) = HPow.hPow (α := ℝ) (↑p : ℝ) (-t)
ht : t⁻¹ ≠ 0
e m : ℕ
hpm : ¬p ∣ m
hn : p ^ e * m ≠ 0
⊢ padicNorm p (↑m : ℚ) = 1

Tactic:
rw [← padicNorm.nat_eq_one_iff] at hpm

Premises used: padicNorm.nat_eq_one_iff
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
p : ℕ
hfp : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      p ≤ m
hprime : Nat.Prime p
hprime_fact : Fact (Nat.Prime p)
t : ℝ
h : 0 < t ∧ (f : (a : ℚ) → ℝ) (↑p : ℚ) = HPow.hPow (α := ℝ) (↑p : ℝ) (-t)
ht : t⁻¹ ≠ 0
e m : ℕ
hpm : ¬p ∣ m
hn : p ^ e * m ≠ 0
hpm₁ : padicNorm p (↑m : ℚ) = 1
⊢ p ^ e * m ≠ 0

Tactic:
rw [← padicNorm.nat_eq_one_iff] at hpm

Premises used: padicNorm.nat_eq_one_iff
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
p : ℕ
hfp : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      p ≤ m
hprime : Nat.Prime p
hprime_fact : Fact (Nat.Prime p)
t : ℝ
h : 0 < t ∧ (f : (a : ℚ) → ℝ) (↑p : ℚ) = HPow.hPow (α := ℝ) (↑p : ℝ) (-t)
ht : t⁻¹ ≠ 0
e m : ℕ
hpm : padicNorm p (↑m : ℚ) = 1
hn : p ^ e * m ≠ 0
refine_1 : HPow.hPow (α := ℝ) (↑p : ℝ) (-(t * (↑e : ℝ) * t⁻¹)) = HPow.hPow (α := ℝ) (β := ℝ) (↑p : ℝ) (-(↑e : ℝ))
⊢ (HPow.hPow (α := ℝ) (↑p : ℝ) (-t) ^ e * 1) ^ t⁻¹ = (HPow.hPow (α := ℝ) (↑p : ℝ) e)⁻¹ * (↑(padicNorm p (↑m : ℚ)) : ℝ)

Tactic:
simp only [← rpow_natCast, p.cast_nonneg, ← rpow_mul, neg_mul, mul_one, ← rpow_neg, hpm,
        cast_one]

Premises used: Nat.cast_nonneg, neg_mul, mul_one, Real.rpow_mul, Real.rpow_neg, Real.rpow_natCast, Rat.cast_one
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
p : ℕ
hfp : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      p ≤ m
hprime : Nat.Prime p
hprime_fact : Fact (Nat.Prime p)
t : ℝ
h : 0 < t ∧ (f : (a : ℚ) → ℝ) (↑p : ℚ) = HPow.hPow (α := ℝ) (↑p : ℝ) (-t)
ht : t⁻¹ ≠ 0
e m : ℕ
hpm : padicNorm p (↑m : ℚ) = 1
hn : p ^ e * m ≠ 0
⊢ HPow.hPow (α := ℝ) (↑p : ℝ) (-(t * (↑e : ℝ) * t⁻¹)) = HPow.hPow (α := ℝ) (β := ℝ) (↑p : ℝ) (-(↑e : ℝ))

Tactic:
field_simp [h.1.ne']

Premises used: LT.lt.ne', And.left
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
p : ℕ
hfp : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      p ≤ m
hprime : Nat.Prime p
hprime_fact : Fact (Nat.Prime p)
t : ℝ
h : 0 < t ∧ (f : (a : ℚ) → ℝ) (↑p : ℚ) = HPow.hPow (α := ℝ) (↑p : ℝ) (-t)
q : ℕ
h_1 :
  (fun (p : ℕ) ↦
      ∃ (h : Fact (Nat.Prime p)) (c : ℝ),
        0 < c ∧ ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (padic p : (a : ℚ) → ℝ) (↑n : ℚ))
    q
hq_prime : Fact (Nat.Prime q)
h_equiv :
  ∃ (c : ℝ), 0 < c ∧ ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (padic q : (a : ℚ) → ℝ) (↑n : ℚ)
refine_2 : ∀ (hne : q ≠ p), False
⊢ q = p

Tactic:
by_contra! hne
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
p : ℕ
hfp : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      p ≤ m
hprime : Nat.Prime p
hprime_fact : Fact (Nat.Prime p)
t : ℝ
h : 0 < t ∧ (f : (a : ℚ) → ℝ) (↑p : ℚ) = HPow.hPow (α := ℝ) (↑p : ℝ) (-t)
q : ℕ
h_1 :
  (fun (p : ℕ) ↦
      ∃ (h : Fact (Nat.Prime p)) (c : ℝ),
        0 < c ∧ ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (padic p : (a : ℚ) → ℝ) (↑n : ℚ))
    q
hq_prime : Fact (Nat.Prime q)
h_equiv :
  ∃ (c : ℝ), 0 < c ∧ ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (padic q : (a : ℚ) → ℝ) (↑n : ℚ)
hne : q ≠ p
refine_2 : q = 1
⊢ False

Tactic:
apply hq_prime.elim.ne_one

Premises used: Nat.Prime.ne_one, Fact.elim
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
p : ℕ
hfp : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      p ≤ m
hprime : Nat.Prime p
hprime_fact : Fact (Nat.Prime p)
t : ℝ
h : 0 < t ∧ (f : (a : ℚ) → ℝ) (↑p : ℚ) = HPow.hPow (α := ℝ) (↑p : ℝ) (-t)
q : ℕ
h_1 :
  (fun (p : ℕ) ↦
      ∃ (h : Fact (Nat.Prime p)) (c : ℝ),
        0 < c ∧ ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (padic p : (a : ℚ) → ℝ) (↑n : ℚ))
    q
hq_prime : Fact (Nat.Prime q)
h_equiv :
  ∃ (c : ℝ), 0 < c ∧ ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (padic q : (a : ℚ) → ℝ) (↑n : ℚ)
hne : q ≠ p
⊢ ¬p ∣ q

Tactic:
rw [ne_comm, ← Nat.coprime_primes hprime hq_prime.elim, hprime.coprime_iff_not_dvd] at hne

Premises used: Fact.elim, ne_comm, Nat.Prime.coprime_iff_not_dvd, Nat.coprime_primes
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
p : ℕ
hfp : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      p ≤ m
hprime : Nat.Prime p
hprime_fact : Fact (Nat.Prime p)
t : ℝ
h : 0 < t ∧ (f : (a : ℚ) → ℝ) (↑p : ℚ) = HPow.hPow (α := ℝ) (↑p : ℝ) (-t)
q : ℕ
h_1 :
  (fun (p : ℕ) ↦
      ∃ (h : Fact (Nat.Prime p)) (c : ℝ),
        0 < c ∧ ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (padic p : (a : ℚ) → ℝ) (↑n : ℚ))
    q
hq_prime : Fact (Nat.Prime q)
h_equiv :
  ∃ (c : ℝ), 0 < c ∧ ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (padic q : (a : ℚ) → ℝ) (↑n : ℚ)
hne : ¬p ∣ q
refine_2 :
  ∀ (c : ℝ),
    0 < c →
      ∀ (h_eq : ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (padic q : (a : ℚ) → ℝ) (↑n : ℚ)),
        q = 1
⊢ q = 1

Tactic:
rcases h_equiv with ⟨c, _, h_eq⟩
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
p : ℕ
hfp : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      p ≤ m
hprime : Nat.Prime p
hprime_fact : Fact (Nat.Prime p)
t : ℝ
h : 0 < t ∧ (f : (a : ℚ) → ℝ) (↑p : ℚ) = HPow.hPow (α := ℝ) (↑p : ℝ) (-t)
q : ℕ
h_1 :
  (fun (p : ℕ) ↦
      ∃ (h : Fact (Nat.Prime p)) (c : ℝ),
        0 < c ∧ ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (padic p : (a : ℚ) → ℝ) (↑n : ℚ))
    q
hq_prime : Fact (Nat.Prime q)
hne : ¬p ∣ q
c : ℝ
left : 0 < c
h_eq : ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (padic q : (a : ℚ) → ℝ) (↑n : ℚ)
⊢ q = 1

Tactic:
simpa [eq_one_of_not_dvd bdd hfp.1 hfp.2 hmin hne] using h_eq q

Premises used: Rat.AbsoluteValue.eq_one_of_not_dvd, And.right, And.left
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f g : AbsoluteValue ℚ ℝ
x y : ℚ
⊢ |(↑(x * y) : ℝ)| = HMul.hMul (α := ℝ) |(↑x : ℝ)| |(↑y : ℝ)|

Tactic:
simp
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f g : AbsoluteValue ℚ ℝ
x : ℚ
⊢ LE.le (α := ℝ) 0 |(↑x : ℝ)|

Tactic:
simp
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f g : AbsoluteValue ℚ ℝ
x : ℚ
⊢ Eq (α := ℝ) |(↑x : ℝ)| 0 ↔ x = 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f g : AbsoluteValue ℚ ℝ
x y : ℚ
⊢ |(↑(x + y) : ℝ)| ≤ HAdd.hAdd (α := ℝ) |(↑x : ℝ)| |(↑y : ℝ)|

Tactic:
simpa using abs_add_le (x : ℝ) (y : ℝ)

Premises used: Rat.cast, abs_add_le
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
r : ℚ
⊢ Eq (α := ℝ) ((real : (a : ℚ) → ℝ) r : ℝ) ((↑|r| : ℝ) : ℝ)

Tactic:
(cast_abs r).symm

Premises used: abs, Rat.cast_abs, Eq.symm
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
n m : ℕ
hm : 1 < m
set :
  let L := m.digits n;
  LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ)
    (List.sum (List.mapIdx (fun (i x : ℕ) ↦ (↑m : ℝ) * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) i) L) : ℝ)
⊢ LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ)
    (List.sum
        (List.mapIdx (fun (i x : ℕ) ↦ (↑m : ℝ) * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) i) (m.digits n)) :
      ℝ)

Tactic:
set L := Nat.digits m n

Premises used: Nat.digits
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
n m : ℕ
hm : 1 < m
L : List ℕ := m.digits n
⊢ let L' : List ℚ := List.map Nat.cast (List.mapIdx (fun (i a : ℕ) ↦ a * m ^ i) L);
  L' = List.map Nat.cast (List.mapIdx (fun (i a : ℕ) ↦ a * m ^ i) L)

Tactic:
set L' : List ℚ := List.map Nat.cast (L.mapIdx fun i a ↦ (a * m ^ i)) with hL'

Premises used: List.mapIdx, HMul.hMul, List.map, Rat, Nat.cast, List, HPow.hPow
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
n m : ℕ
hm : 1 < m
L : List ℕ := m.digits n
L' : List ℚ := List.map Nat.cast (List.mapIdx (fun (i a : ℕ) ↦ a * m ^ i) L)
hL' : L' = List.map Nat.cast (List.mapIdx (fun (i a : ℕ) ↦ a * m ^ i) L)
⊢ ∀ {c : ℕ} (hc : c ∈ m.digits n), LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑c : ℚ) : ℝ) ((↑m : ℝ) : ℝ)

Tactic:
have hcoef {c : ℕ} (hc : c ∈ Nat.digits m n) : f c < m :=
    lt_of_le_of_lt (f.apply_nat_le_self c) (mod_cast Nat.digits_lt_base hm hc)
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
n m : ℕ
hm : 1 < m
L : List ℕ := m.digits n
L' : List ℚ := List.map Nat.cast (List.mapIdx (fun (i a : ℕ) ↦ a * m ^ i) L)
hL' : L' = List.map Nat.cast (List.mapIdx (fun (i a : ℕ) ↦ a * m ^ i) L)
hcoef : ∀ {c : ℕ} (hc : c ∈ m.digits n), LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑c : ℚ) : ℝ) ((↑m : ℝ) : ℝ)
rw rw₁ : Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ)
⊢ Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) ((f : (a : ℚ) → ℝ) (↑(ofDigits m L) : ℚ) : ℝ)

Tactic:
rw [Nat.ofDigits_digits m n]

Premises used: Nat.ofDigits_digits
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
n m : ℕ
hm : 1 < m
L : List ℕ := m.digits n
L' : List ℚ := List.map Nat.cast (List.mapIdx (fun (i a : ℕ) ↦ a * m ^ i) L)
hL' : L' = List.map Nat.cast (List.mapIdx (fun (i a : ℕ) ↦ a * m ^ i) L)
hcoef : ∀ {c : ℕ} (hc : c ∈ m.digits n), LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑c : ℚ) : ℝ) ((↑m : ℝ) : ℝ)
rw :
  Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(List.sum (List.mapIdx (fun (i a : ℕ) ↦ a * m ^ i) L)) : ℚ) : ℝ)
    ((f : (a : ℚ) → ℝ) L'.sum : ℝ)
⊢ Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(ofDigits m L) : ℚ) : ℝ) ((f : (a : ℚ) → ℝ) L'.sum : ℝ)

Tactic:
rw [Nat.ofDigits_eq_sum_mapIdx]

Premises used: Nat.ofDigits_eq_sum_mapIdx
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
n m : ℕ
hm : 1 < m
L : List ℕ := m.digits n
L' : List ℚ := List.map Nat.cast (List.mapIdx (fun (i a : ℕ) ↦ a * m ^ i) L)
hL' : L' = List.map Nat.cast (List.mapIdx (fun (i a : ℕ) ↦ a * m ^ i) L)
hcoef : ∀ {c : ℕ} (hc : c ∈ m.digits n), LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑c : ℚ) : ℝ) ((↑m : ℝ) : ℝ)
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (List.sum (List.map Nat.cast (List.mapIdx (fun (i a : ℕ) ↦ a * m ^ i) L))) : ℝ)
    ((f : (a : ℚ) → ℝ) L'.sum : ℝ)
⊢ Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(List.sum (List.mapIdx (fun (i a : ℕ) ↦ a * m ^ i) L)) : ℚ) : ℝ)
    ((f : (a : ℚ) → ℝ) L'.sum : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
n m : ℕ
hm : 1 < m
L : List ℕ := m.digits n
L' : List ℚ := List.map Nat.cast (List.mapIdx (fun (i a : ℕ) ↦ a * m ^ i) L)
hL' : L' = List.map Nat.cast (List.mapIdx (fun (i a : ℕ) ↦ a * m ^ i) L)
hcoef : ∀ {c : ℕ} (hc : c ∈ m.digits n), LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑c : ℚ) : ℝ) ((↑m : ℝ) : ℝ)
⊢ LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) L'.sum : ℝ) (List.sum (List.map (⇑f : (a : ℚ) → ℝ) L') : ℝ)

Tactic:
listSum_le f L'

Premises used: AbsoluteValue.listSum_le
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
n m : ℕ
hm : 1 < m
L : List ℕ := m.digits n
L' : List ℚ := List.map Nat.cast (List.mapIdx (fun (i a : ℕ) ↦ a * m ^ i) L)
hL' : L' = List.map Nat.cast (List.mapIdx (fun (i a : ℕ) ↦ a * m ^ i) L)
hcoef : ∀ {c : ℕ} (hc : c ∈ m.digits n), LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑c : ℚ) : ℝ) ((↑m : ℝ) : ℝ)
⊢ LE.le (α := ℝ) (List.sum (List.map (⇑f : (a : ℚ) → ℝ) L'))
    (List.sum (List.mapIdx (fun (i x : ℕ) ↦ (↑m : ℝ) * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) i) L))

Tactic:
?_
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
n m : ℕ
hm : 1 < m
L : List ℕ := m.digits n
L' : List ℚ := List.map Nat.cast (List.mapIdx (fun (i a : ℕ) ↦ a * m ^ i) L)
hL' : L' = List.map Nat.cast (List.mapIdx (fun (i a : ℕ) ↦ a * m ^ i) L)
hcoef : ∀ {c : ℕ} (hc : c ∈ m.digits n), LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑c : ℚ) : ℝ) ((↑m : ℝ) : ℝ)
f₁ :
  LE.le (α := ℝ) (List.sum (List.map (⇑f : (a : ℚ) → ℝ) L'))
    (List.sum (List.mapIdx (fun (i x : ℕ) ↦ (↑m : ℝ) * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) i) L))
⊢ LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ)
    (List.sum (List.mapIdx (fun (i x : ℕ) ↦ (↑m : ℝ) * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) i) L) : ℝ)

Tactic:
calc
  f n = f ((Nat.ofDigits m L : ℕ) : ℚ) := by rw [Nat.ofDigits_digits m n]
    _ = f L'.sum := by rw [Nat.ofDigits_eq_sum_mapIdx]; norm_cast
    _ ≤ (L'.map f).sum := listSum_le f L'
    _ ≤ (L.mapIdx fun i _ ↦ m * (f m) ^ i).sum := ?_

Premises used: List.mapIdx, HMul.hMul, List.map, Nat.ofDigits, List.sum, Nat.cast, HPow.hPow, AbsoluteValue.listSum_le, DFunLike.coe