-- Mathlib/Topology/Bornology/BoundedOperation.lean
lemma isBounded_pow {R : Type*} [Bornology R] [Monoid R] [BoundedMul R] {s : Set R}
    (s_bdd : Bornology.IsBounded s) (n : ℕ) :
    Bornology.IsBounded ((fun x ↦ x ^ n) '' s)

Proof state:
case neg
R : Type u_2
inst✝² : Bornology R
inst✝¹ : Monoid R
inst✝ : BoundedMul R
s : Set R
s_bdd : Bornology.IsBounded s
s_empty : ¬s = ∅
⊢ Bornology.IsBounded ((fun x => x ^ 0) '' s)

Tactic:
simp_rw [← nonempty_iff_ne_empty] at s_empty

Result:
case neg
R : Type u_2
inst✝² : Bornology R
inst✝¹ : Monoid R
inst✝ : BoundedMul R
s : Set R
s_bdd : Bornology.IsBounded s
s_empty : s.Nonempty
⊢ Bornology.IsBounded ((fun x => x ^ 0) '' s)

Proof state:
R : Type u_2
inst✝² : Bornology R
inst✝¹ : Monoid R
inst✝ : BoundedMul R
s : Set R
s_bdd : Bornology.IsBounded s
n : ℕ
hn : Bornology.IsBounded ((fun x => x ^ n) '' s)
x : R
hx : ∃ x_1 ∈ s, x_1 ^ (n + 1) = x
⊢ x ∈ (fun x => x ^ n) '' s * s

Tactic:
obtain ⟨y, y_in_s, ypow_eq_x⟩ := hx

Result:
case intro.intro
R : Type u_2
inst✝² : Bornology R
inst✝¹ : Monoid R
inst✝ : BoundedMul R
s : Set R
s_bdd : Bornology.IsBounded s
n : ℕ
hn : Bornology.IsBounded ((fun x => x ^ n) '' s)
x y : R
y_in_s : y ∈ s
ypow_eq_x : y ^ (n + 1) = x
⊢ x ∈ (fun x => x ^ n) '' s * s

Proof state:
case intro.intro
R : Type u_2
inst✝² : Bornology R
inst✝¹ : Monoid R
inst✝ : BoundedMul R
s : Set R
s_bdd : Bornology.IsBounded s
n : ℕ
hn : Bornology.IsBounded ((fun x => x ^ n) '' s)
x y : R
y_in_s : y ∈ s
ypow_eq_x : y ^ (n + 1) = x
⊢ x ∈ (fun x => x ^ n) '' s * s

Tactic:
rw [← ypow_eq_x, pow_succ y n]

Result:
case intro.intro
R : Type u_2
inst✝² : Bornology R
inst✝¹ : Monoid R
inst✝ : BoundedMul R
s : Set R
s_bdd : Bornology.IsBounded s
n : ℕ
hn : Bornology.IsBounded ((fun x => x ^ n) '' s)
x y : R
y_in_s : y ∈ s
ypow_eq_x : y ^ (n + 1) = x
⊢ y ^ n * y ∈ (fun x => x ^ n) '' s * s

Proof state:
case zero
R : Type u_2
inst✝² : Bornology R
inst✝¹ : Monoid R
inst✝ : BoundedMul R
s : Set R
s_bdd : Bornology.IsBounded s
⊢ Bornology.IsBounded ((fun x => x ^ 0) '' s)

Tactic:
by_cases s_empty : s = ∅

Result:
case pos
R : Type u_2
inst✝² : Bornology R
inst✝¹ : Monoid R
inst✝ : BoundedMul R
s : Set R
s_bdd : Bornology.IsBounded s
s_empty : s = ∅
⊢ Bornology.IsBounded ((fun x => x ^ 0) '' s)

case neg
R : Type u_2
inst✝² : Bornology R
inst✝¹ : Monoid R
inst✝ : BoundedMul R
s : Set R
s_bdd : Bornology.IsBounded s
s_empty : ¬s = ∅
⊢ Bornology.IsBounded ((fun x => x ^ 0) '' s)

Proof state:
case succ
R : Type u_2
inst✝² : Bornology R
inst✝¹ : Monoid R
inst✝ : BoundedMul R
s : Set R
s_bdd : Bornology.IsBounded s
n : ℕ
hn : Bornology.IsBounded ((fun x => x ^ n) '' s)
obs : (fun x => x ^ (n + 1)) '' s ⊆ (fun x => x ^ n) '' s * s
⊢ Bornology.IsBounded ((fun x => x ^ (n + 1)) '' s)

Tactic:
exact (isBounded_mul hn s_bdd).subset obs

Result:
no goals

Proof state:
case pos
R : Type u_2
inst✝² : Bornology R
inst✝¹ : Monoid R
inst✝ : BoundedMul R
s : Set R
s_bdd : Bornology.IsBounded s
s_empty : s = ∅
⊢ Bornology.IsBounded ((fun x => x ^ 0) '' s)

Tactic:
simp [s_empty]

Result:
no goals

Proof state:
R : Type u_2
inst✝² : Bornology R
inst✝¹ : Monoid R
inst✝ : BoundedMul R
s : Set R
s_bdd : Bornology.IsBounded s
n : ℕ
hn : Bornology.IsBounded ((fun x => x ^ n) '' s)
x y : R
y_in_s : y ∈ s
ypow_eq_x : y ^ (n + 1) = x
⊢ y ^ n ∈ (fun x => x ^ n) '' s

Tactic:
use y

Result:
no goals

Proof state:
case succ
R : Type u_2
inst✝² : Bornology R
inst✝¹ : Monoid R
inst✝ : BoundedMul R
s : Set R
s_bdd : Bornology.IsBounded s
n : ℕ
hn : Bornology.IsBounded ((fun x => x ^ n) '' s)
⊢ Bornology.IsBounded ((fun x => x ^ (n + 1)) '' s)

Tactic:
have obs : ((fun x ↦ x ^ (n + 1)) '' s) ⊆ ((fun x ↦ x ^ n) '' s) * s := by
  intro x hx
  simp only [mem_image] at hx
  obtain ⟨y, y_in_s, ypow_eq_x⟩ := hx
  rw [← ypow_eq_x, pow_succ y n]
  apply Set.mul_mem_mul _ y_in_s
  use y

Result:
case succ
R : Type u_2
inst✝² : Bornology R
inst✝¹ : Monoid R
inst✝ : BoundedMul R
s : Set R
s_bdd : Bornology.IsBounded s
n : ℕ
hn : Bornology.IsBounded ((fun x => x ^ n) '' s)
obs : (fun x => x ^ (n + 1)) '' s ⊆ (fun x => x ^ n) '' s * s
⊢ Bornology.IsBounded ((fun x => x ^ (n + 1)) '' s)

Proof state:
R : Type u_2
inst✝² : Bornology R
inst✝¹ : Monoid R
inst✝ : BoundedMul R
s : Set R
s_bdd : Bornology.IsBounded s
n : ℕ
hn : Bornology.IsBounded ((fun x => x ^ n) '' s)
x : R
hx : x ∈ (fun x => x ^ (n + 1)) '' s
⊢ x ∈ (fun x => x ^ n) '' s * s

Tactic:
simp only [mem_image] at hx

Result:
R : Type u_2
inst✝² : Bornology R
inst✝¹ : Monoid R
inst✝ : BoundedMul R
s : Set R
s_bdd : Bornology.IsBounded s
n : ℕ
hn : Bornology.IsBounded ((fun x => x ^ n) '' s)
x : R
hx : ∃ x_1 ∈ s, x_1 ^ (n + 1) = x
⊢ x ∈ (fun x => x ^ n) '' s * s

Proof state:
case intro.intro
R : Type u_2
inst✝² : Bornology R
inst✝¹ : Monoid R
inst✝ : BoundedMul R
s : Set R
s_bdd : Bornology.IsBounded s
n : ℕ
hn : Bornology.IsBounded ((fun x => x ^ n) '' s)
x y : R
y_in_s : y ∈ s
ypow_eq_x : y ^ (n + 1) = x
⊢ y ^ n * y ∈ (fun x => x ^ n) '' s * s

Tactic:
apply Set.mul_mem_mul _ y_in_s

Result:
R : Type u_2
inst✝² : Bornology R
inst✝¹ : Monoid R
inst✝ : BoundedMul R
s : Set R
s_bdd : Bornology.IsBounded s
n : ℕ
hn : Bornology.IsBounded ((fun x => x ^ n) '' s)
x y : R
y_in_s : y ∈ s
ypow_eq_x : y ^ (n + 1) = x
⊢ y ^ n ∈ (fun x => x ^ n) '' s

Proof state:
case neg
R : Type u_2
inst✝² : Bornology R
inst✝¹ : Monoid R
inst✝ : BoundedMul R
s : Set R
s_bdd : Bornology.IsBounded s
s_empty : s.Nonempty
⊢ Bornology.IsBounded ((fun x => x ^ 0) '' s)

Tactic:
simp [s_empty]

Result:
no goals

Proof state:
R : Type u_2
inst✝² : Bornology R
inst✝¹ : Monoid R
inst✝ : BoundedMul R
s : Set R
s_bdd : Bornology.IsBounded s
n : ℕ
hn : Bornology.IsBounded ((fun x => x ^ n) '' s)
⊢ (fun x => x ^ (n + 1)) '' s ⊆ (fun x => x ^ n) '' s * s

Tactic:
intro x hx

Result:
R : Type u_2
inst✝² : Bornology R
inst✝¹ : Monoid R
inst✝ : BoundedMul R
s : Set R
s_bdd : Bornology.IsBounded s
n : ℕ
hn : Bornology.IsBounded ((fun x => x ^ n) '' s)
x : R
hx : x ∈ (fun x => x ^ (n + 1)) '' s
⊢ x ∈ (fun x => x ^ n) '' s * s