-- Mathlib/NumberTheory/WellApproximable.lean
theorem image_pow_subset_of_coprime (hm : 0 < m) (hmn : n.Coprime m) :
    (fun (y : A) => y ^ m) '' approxOrderOf A n δ ⊆ approxOrderOf A n (m * δ)

Proof state:
case h.e'_4
A : Type u_1
inst✝ : SeminormedCommGroup A
m n : ℕ
δ : ℝ
hm : 0 < m
hmn : n.Coprime m
a : A
ha : a ∈ approxOrderOf A n δ
b : A
hab : a ∈ ball b δ
hb : b ^ m ∈ {u | orderOf u = n}
⊢ ball (b ^ m) (↑m • δ) = ball (b ^ m) (m • δ)

Tactic:
simp only [nsmul_eq_mul, Algebra.id.smul_eq_mul]

Result:
no goals

Proof state:
A : Type u_1
inst✝ : SeminormedCommGroup A
m n : ℕ
δ : ℝ
hm : 0 < m
hmn : n.Coprime m
⊢ (fun y => y ^ m) '' approxOrderOf A n δ ⊆ approxOrderOf A n (↑m * δ)

Tactic:
rintro - ⟨a, ha, rfl⟩

Result:
case intro.intro
A : Type u_1
inst✝ : SeminormedCommGroup A
m n : ℕ
δ : ℝ
hm : 0 < m
hmn : n.Coprime m
a : A
ha : a ∈ approxOrderOf A n δ
⊢ (fun y => y ^ m) a ∈ approxOrderOf A n (↑m * δ)

Proof state:
case intro.intro.intro.intro.a
A : Type u_1
inst✝ : SeminormedCommGroup A
m n : ℕ
δ : ℝ
hm : 0 < m
hmn : n.Coprime m
a : A
ha : a ∈ approxOrderOf A n δ
b : A
hab : a ∈ ball b δ
hb : b ^ m ∈ {u | orderOf u = n}
⊢ (fun y => y ^ m) a ∈ ball (b ^ m) (↑m • δ)

Tactic:
convert pow_mem_ball hm hab using 1

Result:
case h.e'_4
A : Type u_1
inst✝ : SeminormedCommGroup A
m n : ℕ
δ : ℝ
hm : 0 < m
hmn : n.Coprime m
a : A
ha : a ∈ approxOrderOf A n δ
b : A
hab : a ∈ ball b δ
hb : b ^ m ∈ {u | orderOf u = n}
⊢ ball (b ^ m) (↑m • δ) = ball (b ^ m) (m • δ)

Proof state:
case intro.intro.intro.intro
A : Type u_1
inst✝ : SeminormedCommGroup A
m n : ℕ
δ : ℝ
hm : 0 < m
hmn : n.Coprime m
a : A
ha : a ∈ approxOrderOf A n δ
b : A
hab : a ∈ ball b δ
hb : b ^ m ∈ {u | orderOf u = n}
⊢ (fun y => y ^ m) a ∈ approxOrderOf A n (↑m * δ)

Tactic:
apply ball_subset_thickening hb ((m : ℝ) • δ)

Result:
case intro.intro.intro.intro.a
A : Type u_1
inst✝ : SeminormedCommGroup A
m n : ℕ
δ : ℝ
hm : 0 < m
hmn : n.Coprime m
a : A
ha : a ∈ approxOrderOf A n δ
b : A
hab : a ∈ ball b δ
hb : b ^ m ∈ {u | orderOf u = n}
⊢ (fun y => y ^ m) a ∈ ball (b ^ m) (↑m • δ)

Proof state:
A : Type u_1
inst✝ : SeminormedCommGroup A
m n : ℕ
δ : ℝ
hm : 0 < m
hmn : n.Coprime m
a : A
ha : a ∈ approxOrderOf A n δ
b : A
hb : orderOf b = n
hab : a ∈ ball b δ
⊢ b ^ m ∈ {u | orderOf u = n}

Tactic:
rw [← hb] at hmn ⊢

Result:
A : Type u_1
inst✝ : SeminormedCommGroup A
m n : ℕ
δ : ℝ
hm : 0 < m
a : A
ha : a ∈ approxOrderOf A n δ
b : A
hmn : (orderOf b).Coprime m
hb : orderOf b = n
hab : a ∈ ball b δ
⊢ b ^ m ∈ {u | orderOf u = orderOf b}

Proof state:
A : Type u_1
inst✝ : SeminormedCommGroup A
m n : ℕ
δ : ℝ
hm : 0 < m
a : A
ha : a ∈ approxOrderOf A n δ
b : A
hmn : (orderOf b).Coprime m
hb : orderOf b = n
hab : a ∈ ball b δ
⊢ b ^ m ∈ {u | orderOf u = orderOf b}

Tactic:
exact hmn.orderOf_pow

Result:
no goals

Proof state:
case intro.intro.intro.intro
A : Type u_1
inst✝ : SeminormedCommGroup A
m n : ℕ
δ : ℝ
hm : 0 < m
hmn : n.Coprime m
a : A
ha : a ∈ approxOrderOf A n δ
b : A
hb : orderOf b = n
hab : a ∈ ball b δ
⊢ (fun y => y ^ m) a ∈ approxOrderOf A n (↑m * δ)

Tactic:
replace hb : b ^ m ∈ {u : A | orderOf u = n} := by
  rw [← hb] at hmn ⊢; exact hmn.orderOf_pow

Result:
case intro.intro.intro.intro
A : Type u_1
inst✝ : SeminormedCommGroup A
m n : ℕ
δ : ℝ
hm : 0 < m
hmn : n.Coprime m
a : A
ha : a ∈ approxOrderOf A n δ
b : A
hab : a ∈ ball b δ
hb : b ^ m ∈ {u | orderOf u = n}
⊢ (fun y => y ^ m) a ∈ approxOrderOf A n (↑m * δ)

Proof state:
case intro.intro
A : Type u_1
inst✝ : SeminormedCommGroup A
m n : ℕ
δ : ℝ
hm : 0 < m
hmn : n.Coprime m
a : A
ha : a ∈ approxOrderOf A n δ
⊢ (fun y => y ^ m) a ∈ approxOrderOf A n (↑m * δ)

Tactic:
obtain ⟨b, hb, hab⟩ := mem_approxOrderOf_iff.mp ha

Result:
case intro.intro.intro.intro
A : Type u_1
inst✝ : SeminormedCommGroup A
m n : ℕ
δ : ℝ
hm : 0 < m
hmn : n.Coprime m
a : A
ha : a ∈ approxOrderOf A n δ
b : A
hb : orderOf b = n
hab : a ∈ ball b δ
⊢ (fun y => y ^ m) a ∈ approxOrderOf A n (↑m * δ)