case refine'_1
α : Type ?u.11742
G : Type ?u.11745
M : Type u_2
R : Type ?u.11751
A : Type ?u.11754
inst✝⁴ : Monoid M
inst✝³ : AddMonoid A
s✝ t u : Set M
N : Type u_1
inst✝² : CommMonoid N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
r : M
s : Set N
x : N
hx : x ∈ closure s
⊢ ∀ (x : N), x ∈ s → (fun x => ∃ n, r ^ n • x ∈ closure (r • s)) x

case refine'_2
α : Type ?u.11742
G : Type ?u.11745
M : Type u_2
R : Type ?u.11751
A : Type ?u.11754
inst✝⁴ : Monoid M
inst✝³ : AddMonoid A
s✝ t u : Set M
N : Type u_1
inst✝² : CommMonoid N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
r : M
s : Set N
x : N
hx : x ∈ closure s
⊢ (fun x => ∃ n, r ^ n • x ∈ closure (r • s)) 1

case refine'_3
α : Type ?u.11742
G : Type ?u.11745
M : Type u_2
R : Type ?u.11751
A : Type ?u.11754
inst✝⁴ : Monoid M
inst✝³ : AddMonoid A
s✝ t u : Set M
N : Type u_1
inst✝² : CommMonoid N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
r : M
s : Set N
x : N
hx : x ∈ closure s
⊢ ∀ (x y : N),
    (fun x => ∃ n, r ^ n • x ∈ closure (r • s)) x →
      (fun x => ∃ n, r ^ n • x ∈ closure (r • s)) y → (fun x => ∃ n, r ^ n • x ∈ closure (r • s)) (x * y)
α : Type ?u.11742
G : Type ?u.11745
M : Type u_2
R : Type ?u.11751
A : Type ?u.11754
inst✝⁴ : Monoid M
inst✝³ : AddMonoid A
s✝ t u : Set M
N : Type u_1
inst✝² : CommMonoid N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
r : M
s : Set N
x : N
hx : x ∈ closure s
⊢ ∃ n, r ^ n • x ∈ closure (r • s)
refine' @closure_induction N _ s (fun x : N => ∃ n : ℕ, r ^ n • x ∈ closure (r • s)) _ hx _ _ _
case refine'_1
α : Type ?u.11742
G : Type ?u.11745
M : Type u_2
R : Type ?u.11751
A : Type ?u.11754
inst✝⁴ : Monoid M
inst✝³ : AddMonoid A
s✝ t u : Set M
N : Type u_1
inst✝² : CommMonoid N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
r : M
s : Set N
x✝ : N
hx✝ : x✝ ∈ closure s
x : N
hx : x ∈ s
⊢ ∃ n, r ^ n • x ∈ closure (r • s)
case refine'_1
α : Type ?u.11742
G : Type ?u.11745
M : Type u_2
R : Type ?u.11751
A : Type ?u.11754
inst✝⁴ : Monoid M
inst✝³ : AddMonoid A
s✝ t u : Set M
N : Type u_1
inst✝² : CommMonoid N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
r : M
s : Set N
x : N
hx : x ∈ closure s
⊢ ∀ (x : N), x ∈ s → (fun x => ∃ n, r ^ n • x ∈ closure (r • s)) x
intro x hx
no goals
case refine'_1
α : Type ?u.11742
G : Type ?u.11745
M : Type u_2
R : Type ?u.11751
A : Type ?u.11754
inst✝⁴ : Monoid M
inst✝³ : AddMonoid A
s✝ t u : Set M
N : Type u_1
inst✝² : CommMonoid N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
r : M
s : Set N
x✝ : N
hx✝ : x✝ ∈ closure s
x : N
hx : x ∈ s
⊢ ∃ n, r ^ n • x ∈ closure (r • s)
exact ⟨1, subset_closure ⟨_, hx, by rw [pow_one]⟩⟩
no goals
α : Type ?u.11742
G : Type ?u.11745
M : Type u_2
R : Type ?u.11751
A : Type ?u.11754
inst✝⁴ : Monoid M
inst✝³ : AddMonoid A
s✝ t u : Set M
N : Type u_1
inst✝² : CommMonoid N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
r : M
s : Set N
x✝ : N
hx✝ : x✝ ∈ closure s
x : N
hx : x ∈ s
⊢ (fun x => r • x) x = r ^ 1 • x
rw [pow_one]
no goals
case refine'_2
α : Type ?u.11742
G : Type ?u.11745
M : Type u_2
R : Type ?u.11751
A : Type ?u.11754
inst✝⁴ : Monoid M
inst✝³ : AddMonoid A
s✝ t u : Set M
N : Type u_1
inst✝² : CommMonoid N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
r : M
s : Set N
x : N
hx : x ∈ closure s
⊢ (fun x => ∃ n, r ^ n • x ∈ closure (r • s)) 1
exact ⟨0, by simpa using one_mem _⟩
no goals
α : Type ?u.11742
G : Type ?u.11745
M : Type u_2
R : Type ?u.11751
A : Type ?u.11754
inst✝⁴ : Monoid M
inst✝³ : AddMonoid A
s✝ t u : Set M
N : Type u_1
inst✝² : CommMonoid N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
r : M
s : Set N
x : N
hx : x ∈ closure s
⊢ r ^ 0 • 1 ∈ closure (r • s)
simpa using one_mem _
case refine'_3.intro.intro
α : Type ?u.11742
G : Type ?u.11745
M : Type u_2
R : Type ?u.11751
A : Type ?u.11754
inst✝⁴ : Monoid M
inst✝³ : AddMonoid A
s✝ t u : Set M
N : Type u_1
inst✝² : CommMonoid N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
r : M
s : Set N
x✝ : N
hx✝ : x✝ ∈ closure s
x y : N
nx : ℕ
hx : r ^ nx • x ∈ closure (r • s)
ny : ℕ
hy : r ^ ny • y ∈ closure (r • s)
⊢ ∃ n, r ^ n • (x * y) ∈ closure (r • s)
case refine'_3
α : Type ?u.11742
G : Type ?u.11745
M : Type u_2
R : Type ?u.11751
A : Type ?u.11754
inst✝⁴ : Monoid M
inst✝³ : AddMonoid A
s✝ t u : Set M
N : Type u_1
inst✝² : CommMonoid N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
r : M
s : Set N
x : N
hx : x ∈ closure s
⊢ ∀ (x y : N),
    (fun x => ∃ n, r ^ n • x ∈ closure (r • s)) x →
      (fun x => ∃ n, r ^ n • x ∈ closure (r • s)) y → (fun x => ∃ n, r ^ n • x ∈ closure (r • s)) (x * y)
rintro x y ⟨nx, hx⟩ ⟨ny, hy⟩
case refine'_3.intro.intro
α : Type ?u.11742
G : Type ?u.11745
M : Type u_2
R : Type ?u.11751
A : Type ?u.11754
inst✝⁴ : Monoid M
inst✝³ : AddMonoid A
s✝ t u : Set M
N : Type u_1
inst✝² : CommMonoid N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
r : M
s : Set N
x✝ : N
hx✝ : x✝ ∈ closure s
x y : N
nx : ℕ
hx : r ^ nx • x ∈ closure (r • s)
ny : ℕ
hy : r ^ ny • y ∈ closure (r • s)
⊢ r ^ (ny + nx) • (x * y) ∈ closure (r • s)
case refine'_3.intro.intro
α : Type ?u.11742
G : Type ?u.11745
M : Type u_2
R : Type ?u.11751
A : Type ?u.11754
inst✝⁴ : Monoid M
inst✝³ : AddMonoid A
s✝ t u : Set M
N : Type u_1
inst✝² : CommMonoid N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
r : M
s : Set N
x✝ : N
hx✝ : x✝ ∈ closure s
x y : N
nx : ℕ
hx : r ^ nx • x ∈ closure (r • s)
ny : ℕ
hy : r ^ ny • y ∈ closure (r • s)
⊢ ∃ n, r ^ n • (x * y) ∈ closure (r • s)
use ny + nx
case refine'_3.intro.intro
α : Type ?u.11742
G : Type ?u.11745
M : Type u_2
R : Type ?u.11751
A : Type ?u.11754
inst✝⁴ : Monoid M
inst✝³ : AddMonoid A
s✝ t u : Set M
N : Type u_1
inst✝² : CommMonoid N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
r : M
s : Set N
x✝ : N
hx✝ : x✝ ∈ closure s
x y : N
nx : ℕ
hx : r ^ nx • x ∈ closure (r • s)
ny : ℕ
hy : r ^ ny • y ∈ closure (r • s)
⊢ r ^ ny • y * r ^ nx • x ∈ closure (r • s)
case refine'_3.intro.intro
α : Type ?u.11742
G : Type ?u.11745
M : Type u_2
R : Type ?u.11751
A : Type ?u.11754
inst✝⁴ : Monoid M
inst✝³ : AddMonoid A
s✝ t u : Set M
N : Type u_1
inst✝² : CommMonoid N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
r : M
s : Set N
x✝ : N
hx✝ : x✝ ∈ closure s
x y : N
nx : ℕ
hx : r ^ nx • x ∈ closure (r • s)
ny : ℕ
hy : r ^ ny • y ∈ closure (r • s)
⊢ r ^ (ny + nx) • (x * y) ∈ closure (r • s)
rw [pow_add, mul_smul, ← smul_mul_assoc, mul_comm, ← smul_mul_assoc]
no goals
case refine'_3.intro.intro
α : Type ?u.11742
G : Type ?u.11745
M : Type u_2
R : Type ?u.11751
A : Type ?u.11754
inst✝⁴ : Monoid M
inst✝³ : AddMonoid A
s✝ t u : Set M
N : Type u_1
inst✝² : CommMonoid N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
r : M
s : Set N
x✝ : N
hx✝ : x✝ ∈ closure s
x y : N
nx : ℕ
hx : r ^ nx • x ∈ closure (r • s)
ny : ℕ
hy : r ^ ny • y ∈ closure (r • s)
⊢ r ^ ny • y * r ^ nx • x ∈ closure (r • s)
exact mul_mem hy hx