awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
⊢ ∃! p : ℕ, ∃ (x : Fact (Nat.Prime p)), f.IsEquiv (padic p)
have obtain : ∀ (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),
  ∃! p : ℕ, ∃ (x : Fact (Nat.Prime p)), f.IsEquiv (padic p)
Tactic: obtain ⟨p, hfp, hmin⟩ := exists_minimal_nat_zero_lt_and_lt_one hf_nontriv bdd
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (hypothesis)
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
⊢ ∃! p : ℕ, ∃ (x : Fact (Nat.Prime p)), f.IsEquiv (padic p)
have hprime : Nat.Prime p
Tactic: have hprime := is_prime_of_minimal_nat_zero_lt_and_lt_one hfp.1 hfp.2 hmin
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (hypothesis)
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
⊢ ∃! p : ℕ, ∃ (x : Fact (Nat.Prime p)), f.IsEquiv (padic p)
have hprime_fact : Fact (Nat.Prime p)
Tactic: have hprime_fact : Fact p.Prime := ⟨hprime⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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)
⊢ ∃! p : ℕ, ∃ (x : Fact (Nat.Prime p)), f.IsEquiv (padic p)
have obtain : ∀ (t : ℝ) (h : 0 < t ∧ (f : (a : ℚ) → ℝ) (↑p : ℚ) = HPow.hPow (α := ℝ) (↑p : ℝ) (-t)),
  ∃! p : ℕ, ∃ (x : Fact (Nat.Prime p)), f.IsEquiv (padic p)
Tactic: obtain ⟨t, h⟩ := exists_pos_eq_pow_neg hfp.1 hfp.2 hmin
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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 : ℕ, ∃ (x : Fact (Nat.Prime p)), f.IsEquiv (padic p)
have simp_rw : ∃! p : ℕ,
  ∃ (h : Fact (Nat.Prime p)) (c : ℝ),
    0 < c ∧ ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (padic p : (a : ℚ) → ℝ) (↑n : ℚ)
Tactic: simp_rw [← exists_nat_rpow_iff_isEquiv]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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 : ℚ)
have refine_1 : ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) t⁻¹ = (padic p : (a : ℚ) → ℝ) (↑n : ℚ)
Tactic: refine ⟨p, ⟨hprime_fact, t⁻¹, inv_pos_of_pos h.1, fun n ↦ ?_⟩, fun q ⟨hq_prime, h_equiv⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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 : ℚ)
⊢ ∃! p : ℕ,
    ∃ (h : Fact (Nat.Prime p)) (c : ℝ),
      0 < c ∧ ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (padic p : (a : ℚ) → ℝ) (↑n : ℚ)
have 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
Tactic: refine ⟨p, ⟨hprime_fact, t⁻¹, inv_pos_of_pos h.1, fun n ↦ ?_⟩, fun q ⟨hq_prime, h_equiv⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (hypothesis)
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 : ℕ
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) t⁻¹ = (padic p : (a : ℚ) → ℝ) (↑n : ℚ)
have ht : t⁻¹ ≠ 0
Tactic: have ht : t⁻¹ ≠ 0 := inv_ne_zero h.1.ne'
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) t⁻¹ = (padic p : (a : ℚ) → ℝ) (↑n : ℚ)
have refine_1 : HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑0 : ℚ) : ℝ) t⁻¹ = (padic p : (a : ℚ) → ℝ) (↑0 : ℚ)
Tactic: rcases eq_or_ne n 0 with rfl | hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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 : ℚ)
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) t⁻¹ = (padic p : (a : ℚ) → ℝ) (↑n : ℚ)
have refine_1₁ : ∀ (hn : n ≠ 0), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) t⁻¹ = (padic p : (a : ℚ) → ℝ) (↑n : ℚ)
Tactic: rcases eq_or_ne n 0 with rfl | hn
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) t⁻¹ = (padic p : (a : ℚ) → ℝ) (↑n : ℚ)
have 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) : ℚ)
Tactic: rcases Nat.exists_eq_pow_mul_and_not_dvd hn p hprime.ne_one with ⟨e, m, hpm, rfl⟩
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(p ^ e * m) : ℚ) : ℝ) t⁻¹ = (padic p : (a : ℚ) → ℝ) (↑(p ^ e * m) : ℚ)
have refine_1 : (HPow.hPow (α := ℝ) (↑p : ℝ) (-t) ^ e * 1) ^ t⁻¹ = (HPow.hPow (α := ℝ) (↑p : ℝ) e)⁻¹ * (↑(padicNorm p (↑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]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (hypothesis)
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
⊢ (HPow.hPow (α := ℝ) (↑p : ℝ) (-t) ^ e * 1) ^ t⁻¹ = (HPow.hPow (α := ℝ) (↑p : ℝ) e)⁻¹ * (↑(padicNorm p (↑m : ℚ)) : ℝ)
have hpm₁ : padicNorm p (↑m : ℚ) = 1
Tactic: rw [← padicNorm.nat_eq_one_iff] at hpm
Cleared hypotheses: hpm, hn
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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 * 1) ^ t⁻¹ = (HPow.hPow (α := ℝ) (↑p : ℝ) e)⁻¹ * (↑(padicNorm p (↑m : ℚ)) : ℝ)
have refine_1 : HPow.hPow (α := ℝ) (↑p : ℝ) (-(t * (↑e : ℝ) * t⁻¹)) = HPow.hPow (α := ℝ) (β := ℝ) (↑p : ℝ) (-(↑e : ℝ))
Tactic: simp only [← rpow_natCast, p.cast_nonneg, ← rpow_mul, neg_mul, mul_one, ← rpow_neg, hpm,
        cast_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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 : ℚ)
⊢ q = p
have refine_2 : ∀ (hne : q ≠ p), False
Tactic: by_contra! hne
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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
⊢ False
have refine_2 : q = 1
Tactic: apply hq_prime.elim.ne_one
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (hypothesis)
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
⊢ q = 1
have hne₁ : ¬p ∣ q
Tactic: rw [ne_comm, ← Nat.coprime_primes hprime hq_prime.elim, hprime.coprime_iff_not_dvd] at hne
Cleared hypotheses: hne
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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
⊢ q = 1
have refine_2 : ∀ (c : ℝ),
  0 < c →
    ∀ (h_eq : ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (padic q : (a : ℚ) → ℝ) (↑n : ℚ)),
      q = 1
Tactic: rcases h_equiv with ⟨c, _, h_eq⟩
Cleared hypotheses: h_equiv
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (hypothesis)
Goal:
f : AbsoluteValue ℚ ℝ
n m : ℕ
hm : 1 < m
L : List ℕ := m.digits n
⊢ LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ)
    (List.sum (List.mapIdx (fun (i x : ℕ) ↦ (↑m : ℝ) * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) i) L) : ℝ)
have hL' : 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'
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (hypothesis)
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)
⊢ LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ)
    (List.sum (List.mapIdx (fun (i x : ℕ) ↦ (↑m : ℝ) * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) i) L) : ℝ)
have hcoef : ∀ {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)
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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 : ℝ) : ℝ)
⊢ Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) ((f : (a : ℚ) → ℝ) (↑(ofDigits m L) : ℚ) : ℝ)
have rw : Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ)
Tactic: rw [Nat.ofDigits_digits m n]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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 : ℝ) : ℝ)
⊢ Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(ofDigits m L) : ℚ) : ℝ) ((f : (a : ℚ) → ℝ) L'.sum : ℝ)
have rw : Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(List.sum (List.mapIdx (fun (i a : ℕ) ↦ a * m ^ i) L)) : ℚ) : ℝ)
  ((f : (a : ℚ) → ℝ) L'.sum : ℝ)
Tactic: rw [Nat.ofDigits_eq_sum_mapIdx]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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 : ℝ) : ℝ)
⊢ Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(List.sum (List.mapIdx (fun (i a : ℕ) ↦ a * m ^ i) L)) : ℚ) : ℝ)
    ((f : (a : ℚ) → ℝ) L'.sum : ℝ)
have norm_cast : Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (List.sum (List.map Nat.cast (List.mapIdx (fun (i a : ℕ) ↦ a * m ^ i) L))) : ℝ)
  ((f : (a : ℚ) → ℝ) L'.sum : ℝ)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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 : ℚ) → ℝ) (↑n : ℚ) : ℝ)
    (List.sum (List.mapIdx (fun (i x : ℕ) ↦ (↑m : ℝ) * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) i) L) : ℝ)
have 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))
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 := ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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))
have simp : LE.le (α := ℝ)
  (List.sum
    (List.map (Function.comp (β := ℚ) (⇑f : (a : ℚ) → ℝ) (Nat.cast ∘ fun (x : ℕ × ℕ) ↦ x.1 * m ^ x.2)) L.zipIdx))
  (List.sum (List.map (fun (x : ℕ × ℕ) ↦ (↑m : ℝ) * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) x.2) L.zipIdx))
Tactic: simp only [hL', List.mapIdx_eq_zipIdx_map, List.map_map]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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 (Function.comp (β := ℚ) (⇑f : (a : ℚ) → ℝ) (Nat.cast ∘ fun (x : ℕ × ℕ) ↦ x.1 * m ^ x.2)) L.zipIdx))
    (List.sum
      (List.map (fun (x : ℕ × ℕ) ↦ (↑m : ℝ) * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) x.2) L.zipIdx))
have refine : ∀ (x : ℕ × ℕ) (a i : ℕ) (hia : (a, i) ∈ L.zipIdx),
  Function.comp (β := ℚ) (⇑f : (a : ℚ) → ℝ) (Nat.cast ∘ fun (x : ℕ × ℕ) ↦ x.1 * m ^ x.2) (a, i) ≤
    (↑m : ℝ) * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (a, i).2
Tactic: refine List.sum_le_sum fun ⟨a, i⟩ hia ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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 : ℝ) : ℝ)
x : ℕ × ℕ
a i : ℕ
hia : (a, i) ∈ L.zipIdx
⊢ Function.comp (β := ℚ) (⇑f : (a : ℚ) → ℝ) (Nat.cast ∘ fun (x : ℕ × ℕ) ↦ x.1 * m ^ x.2) (a, i) ≤
    (↑m : ℝ) * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (a, i).2
have dsimp : (f : (a : ℚ) → ℝ) (↑(a * m ^ i) : ℚ) ≤ (↑m : ℝ) * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) i
Tactic: dsimp only [Function.comp_apply, Function.uncurry_apply_pair]