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

Proof state:
case intro.intro.intro.refine_2.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)
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)
hne : ¬p ∣ q
c : ℝ
left✝ : 0 < c
h_eq : ∀ (n : ℕ), f ↑n ^ c = (padic q) ↑n
h_eq' : f ↑q ^ c = (padic q) ↑q
⊢ q = 1

Tactic:
simp only [eq_one_of_not_dvd bdd hfp.1 hfp.2 hmin hne, one_rpow, padic_eq_padicNorm,
  padicNorm.padicNorm_p_of_prime, cast_inv, cast_natCast, eq_comm, inv_eq_one] at h_eq'

Result:
case intro.intro.intro.refine_2.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)
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)
hne : ¬p ∣ q
c : ℝ
left✝ : 0 < c
h_eq : ∀ (n : ℕ), f ↑n ^ c = (padic q) ↑n
h_eq' : ↑q = 1
⊢ 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 * t⁻¹)) = ↑p ^ (-↑e)

Tactic:
congr

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

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
⊢ f ↑(p ^ e * m) ^ t⁻¹ = (padic p) ↑(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]

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 : ¬p ∣ m
hn : p ^ e * m ≠ 0
⊢ ((↑p ^ (-t)) ^ e * 1) ^ t⁻¹ = (↑p ^ e)⁻¹ * ↑(padicNorm p ↑m)

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 : ¬p ∣ q
⊢ q = 1

Tactic:
rcases h_equiv with ⟨c, _, h_eq⟩

Result:
case intro.intro.intro.refine_2.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)
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)
hne : ¬p ∣ q
c : ℝ
left✝ : 0 < c
h_eq : ∀ (n : ℕ), f ↑n ^ c = (padic q) ↑n
⊢ q = 1