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

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

Tactic:
obtain ⟨b, hb : orderOf b = n * m, hab : a ∈ ball b δ⟩ := mem_approxOrderOf_iff.mp ha

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

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

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

Tactic:
simp only [nsmul_eq_mul]

Result:
no goals

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

Proof state:
A : Type u_1
inst✝ : SeminormedCommGroup A
m : ℕ
δ : ℝ
n : ℕ
hm : 0 < m
⊢ (fun y => y ^ m) '' approxOrderOf A (n * m) δ ⊆ 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
a : A
ha : a ∈ approxOrderOf A (n * m) δ
⊢ (fun y => y ^ m) a ∈ approxOrderOf A n (↑m * δ)

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

Tactic:
replace hb : b ^ m ∈ {y : A | orderOf y = n} := by
  rw [mem_setOf_eq, orderOf_pow' b hm.ne', hb, Nat.gcd_mul_left_left, n.mul_div_cancel hm]

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

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

Tactic:
rw [mem_setOf_eq, orderOf_pow' b hm.ne', hb, Nat.gcd_mul_left_left, n.mul_div_cancel hm]

Result:
no goals