-- Mathlib/NumberTheory/Ostrowski.lean
theorem equiv_padic_of_bounded :
    ∃! p, ∃ (_ : Fact p.Prime), f ≈ (padic p)

Proof state:
case intro.intro.intro.refine_2
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hfp : 0 < f ↑p ∧ f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
hprime : Nat.Prime p
hprime_fact : Fact (Nat.Prime p)
t : ℝ
h : 0 < t ∧ f ↑p = ↑p ^ (-t)
q : ℕ
x✝ : (fun p => ∃ (h : Fact (Nat.Prime p)), ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = (padic p) ↑n) q
hq_prime : Fact (Nat.Prime q)
h_equiv : ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = (padic q) ↑n
hne : q ≠ p
⊢ False

Tactic:
apply hq_prime.elim.prime.ne_one

Result:
case intro.intro.intro.refine_2
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hfp : 0 < f ↑p ∧ f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
hprime : Nat.Prime p
hprime_fact : Fact (Nat.Prime p)
t : ℝ
h : 0 < t ∧ f ↑p = ↑p ^ (-t)
q : ℕ
x✝ : (fun p => ∃ (h : Fact (Nat.Prime p)), ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = (padic p) ↑n) q
hq_prime : Fact (Nat.Prime q)
h_equiv : ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = (padic q) ↑n
hne : q ≠ p
⊢ q = 1

Proof state:
case intro.intro.intro.refine_1.inr.intro.intro.intro
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hfp : 0 < f ↑p ∧ f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
hprime : Nat.Prime p
hprime_fact : Fact (Nat.Prime p)
t : ℝ
h : 0 < t ∧ f ↑p = ↑p ^ (-t)
ht : t⁻¹ ≠ 0
e m : ℕ
hpm : ¬p ∣ m
hn : p ^ e * m ≠ 0
⊢ ((↑p ^ (-t)) ^ e * 1) ^ t⁻¹ = (↑p ^ e)⁻¹ * ↑(padicNorm p ↑m)

Tactic:
rw [← padicNorm.nat_eq_one_iff] at hpm

Result:
case intro.intro.intro.refine_1.inr.intro.intro.intro
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hfp : 0 < f ↑p ∧ f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
hprime : Nat.Prime p
hprime_fact : Fact (Nat.Prime p)
t : ℝ
h : 0 < t ∧ f ↑p = ↑p ^ (-t)
ht : t⁻¹ ≠ 0
e m : ℕ
hpm : padicNorm p ↑m = 1
hn : p ^ e * m ≠ 0
⊢ ((↑p ^ (-t)) ^ e * 1) ^ t⁻¹ = (↑p ^ e)⁻¹ * ↑(padicNorm p ↑m)

Proof state:
case intro.intro.intro.refine_1.inr.intro.intro.intro.e_a.e_a
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hfp : 0 < f ↑p ∧ f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
hprime : Nat.Prime p
hprime_fact : Fact (Nat.Prime p)
t : ℝ
h : 0 < t ∧ f ↑p = ↑p ^ (-t)
ht : t⁻¹ ≠ 0
e m : ℕ
hpm : padicNorm p ↑m = 1
hn : p ^ e * m ≠ 0
⊢ t * ↑e * t⁻¹ = ↑e

Tactic:
field_simp [h.1.ne']

Result:
no goals

Proof state:
case intro.intro.intro.refine_2
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hfp : 0 < f ↑p ∧ f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
hprime : Nat.Prime p
hprime_fact : Fact (Nat.Prime p)
t : ℝ
h : 0 < t ∧ f ↑p = ↑p ^ (-t)
q : ℕ
x✝ : (fun p => ∃ (h : Fact (Nat.Prime p)), ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = (padic p) ↑n) q
hq_prime : Fact (Nat.Prime q)
h_equiv : ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = (padic q) ↑n
hne : q ≠ p
⊢ q = 1

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

Result:
case intro.intro.intro.refine_2
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hfp : 0 < f ↑p ∧ f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
hprime : Nat.Prime p
hprime_fact : Fact (Nat.Prime p)
t : ℝ
h : 0 < t ∧ f ↑p = ↑p ^ (-t)
q : ℕ
x✝ : (fun p => ∃ (h : Fact (Nat.Prime p)), ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = (padic p) ↑n) q
hq_prime : Fact (Nat.Prime q)
h_equiv : ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = (padic q) ↑n
hne : ¬p ∣ q
⊢ q = 1

Proof state:
case intro.intro.intro.refine_1.inr.intro.intro.intro
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hfp : 0 < f ↑p ∧ f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
hprime : Nat.Prime p
hprime_fact : Fact (Nat.Prime p)
t : ℝ
h : 0 < t ∧ f ↑p = ↑p ^ (-t)
ht : t⁻¹ ≠ 0
e m : ℕ
hpm : padicNorm p ↑m = 1
hn : p ^ e * m ≠ 0
⊢ ((↑p ^ (-t)) ^ e * 1) ^ t⁻¹ = (↑p ^ e)⁻¹ * ↑(padicNorm p ↑m)

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

Result:
case intro.intro.intro.refine_1.inr.intro.intro.intro
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hfp : 0 < f ↑p ∧ f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
hprime : Nat.Prime p
hprime_fact : Fact (Nat.Prime p)
t : ℝ
h : 0 < t ∧ f ↑p = ↑p ^ (-t)
ht : t⁻¹ ≠ 0
e m : ℕ
hpm : padicNorm p ↑m = 1
hn : p ^ e * m ≠ 0
⊢ ↑p ^ (-(t * ↑e * t⁻¹)) = ↑p ^ (-↑e)

Proof state:
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
⊢ ∃! p, ∃ (x : Fact (Nat.Prime p)), f ≈ padic p

Tactic:
obtain ⟨p, hfp, hmin⟩ := exists_minimal_nat_zero_lt_and_lt_one hf_nontriv bdd

Result:
case intro.intro
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hfp : 0 < f ↑p ∧ f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
⊢ ∃! p, ∃ (x : Fact (Nat.Prime p)), f ≈ padic p

Proof state:
case intro.intro
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hfp : 0 < f ↑p ∧ f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
⊢ ∃! p, ∃ (x : Fact (Nat.Prime p)), f ≈ padic p

Tactic:
have hprime := is_prime_of_minimal_nat_zero_lt_and_lt_one hfp.1 hfp.2 hmin

Result:
case intro.intro
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hfp : 0 < f ↑p ∧ f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
hprime : Nat.Prime p
⊢ ∃! p, ∃ (x : Fact (Nat.Prime p)), f ≈ padic p

Proof state:
case intro.intro.intro
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hfp : 0 < f ↑p ∧ f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
hprime : Nat.Prime p
hprime_fact : Fact (Nat.Prime p)
t : ℝ
h : 0 < t ∧ f ↑p = ↑p ^ (-t)
⊢ ∃! p, ∃ (x : Fact (Nat.Prime p)), f ≈ padic p

Tactic:
simp_rw [← equiv_on_nat_iff_equiv]

Result:
case intro.intro.intro
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hfp : 0 < f ↑p ∧ f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
hprime : Nat.Prime p
hprime_fact : Fact (Nat.Prime p)
t : ℝ
h : 0 < t ∧ f ↑p = ↑p ^ (-t)
⊢ ∃! p, ∃ (h : Fact (Nat.Prime p)), ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = (padic p) ↑n

Proof state:
case intro.intro
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hfp : 0 < f ↑p ∧ f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
hprime : Nat.Prime p
hprime_fact : Fact (Nat.Prime p)
⊢ ∃! p, ∃ (x : Fact (Nat.Prime p)), f ≈ padic p

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

Result:
case intro.intro.intro
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hfp : 0 < f ↑p ∧ f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
hprime : Nat.Prime p
hprime_fact : Fact (Nat.Prime p)
t : ℝ
h : 0 < t ∧ f ↑p = ↑p ^ (-t)
⊢ ∃! p, ∃ (x : Fact (Nat.Prime p)), f ≈ padic p