-- Mathlib/LinearAlgebra/Basis/Basic.lean
theorem groupSMul_span_eq_top {G : Type*} [Group G] [DistribMulAction G R] [DistribMulAction G M]
    [IsScalarTower G R M] {v : ι → M} (hv : Submodule.span R (Set.range v) = ⊤) {w : ι → G} :
    Submodule.span R (Set.range (w • v)) = ⊤

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_7
inst✝³ : Group G
inst✝² : DistribMulAction G R
inst✝¹ : DistribMulAction G M
inst✝ : IsScalarTower G R M
v : ι → M
hv : span R (range v) = ⊤
w : ι → G
⊢ ⊤ ≤ span R (range (w • v))

Tactic:
intro j hj

Result:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_7
inst✝³ : Group G
inst✝² : DistribMulAction G R
inst✝¹ : DistribMulAction G M
inst✝ : IsScalarTower G R M
v : ι → M
hv : span R (range v) = ⊤
w : ι → G
j : M
hj : j ∈ ⊤
⊢ j ∈ span R (range (w • v))

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_7
inst✝³ : Group G
inst✝² : DistribMulAction G R
inst✝¹ : DistribMulAction G M
inst✝ : IsScalarTower G R M
v : ι → M
hv : span R (range v) = ⊤
w : ι → G
j : M
hj : ∀ (p : Submodule R M), range v ⊆ ↑p → j ∈ p
p : Submodule R M
hp : range (w • v) ⊆ ↑p
u : M
hu : u ∈ range v
⊢ u ∈ ↑p

Tactic:
obtain ⟨i, rfl⟩ := hu

Result:
case intro
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_7
inst✝³ : Group G
inst✝² : DistribMulAction G R
inst✝¹ : DistribMulAction G M
inst✝ : IsScalarTower G R M
v : ι → M
hv : span R (range v) = ⊤
w : ι → G
j : M
hj : ∀ (p : Submodule R M), range v ⊆ ↑p → j ∈ p
p : Submodule R M
hp : range (w • v) ⊆ ↑p
i : ι
⊢ v i ∈ ↑p

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_7
inst✝³ : Group G
inst✝² : DistribMulAction G R
inst✝¹ : DistribMulAction G M
inst✝ : IsScalarTower G R M
v : ι → M
hv : span R (range v) = ⊤
w : ι → G
⊢ span R (range (w • v)) = ⊤

Tactic:
rw [eq_top_iff]

Result:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_7
inst✝³ : Group G
inst✝² : DistribMulAction G R
inst✝¹ : DistribMulAction G M
inst✝ : IsScalarTower G R M
v : ι → M
hv : span R (range v) = ⊤
w : ι → G
⊢ ⊤ ≤ span R (range (w • v))

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_7
inst✝³ : Group G
inst✝² : DistribMulAction G R
inst✝¹ : DistribMulAction G M
inst✝ : IsScalarTower G R M
v : ι → M
hv : span R (range v) = ⊤
w : ι → G
j : M
hj : ∀ (p : Submodule R M), range v ⊆ ↑p → j ∈ p
⊢ ∀ (p : Submodule R M), range (w • v) ⊆ ↑p → j ∈ p

Tactic:
refine fun p hp => hj p fun u hu => ?_

Result:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_7
inst✝³ : Group G
inst✝² : DistribMulAction G R
inst✝¹ : DistribMulAction G M
inst✝ : IsScalarTower G R M
v : ι → M
hv : span R (range v) = ⊤
w : ι → G
j : M
hj : ∀ (p : Submodule R M), range v ⊆ ↑p → j ∈ p
p : Submodule R M
hp : range (w • v) ⊆ ↑p
u : M
hu : u ∈ range v
⊢ u ∈ ↑p

Proof state:
case intro
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_7
inst✝³ : Group G
inst✝² : DistribMulAction G R
inst✝¹ : DistribMulAction G M
inst✝ : IsScalarTower G R M
v : ι → M
hv : span R (range v) = ⊤
w : ι → G
j : M
hj : ∀ (p : Submodule R M), range v ⊆ ↑p → j ∈ p
p : Submodule R M
hp : range (w • v) ⊆ ↑p
i : ι
⊢ v i ∈ ↑p

Tactic:
have : ((w i)⁻¹ • (1 : R)) • w i • v i ∈ p := p.smul_mem ((w i)⁻¹ • (1 : R)) (hp ⟨i, rfl⟩)

Result:
case intro
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_7
inst✝³ : Group G
inst✝² : DistribMulAction G R
inst✝¹ : DistribMulAction G M
inst✝ : IsScalarTower G R M
v : ι → M
hv : span R (range v) = ⊤
w : ι → G
j : M
hj : ∀ (p : Submodule R M), range v ⊆ ↑p → j ∈ p
p : Submodule R M
hp : range (w • v) ⊆ ↑p
i : ι
this : ((w i)⁻¹ • 1) • w i • v i ∈ p
⊢ v i ∈ ↑p

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_7
inst✝³ : Group G
inst✝² : DistribMulAction G R
inst✝¹ : DistribMulAction G M
inst✝ : IsScalarTower G R M
v : ι → M
hv : span R (range v) = ⊤
w : ι → G
j : M
hj : j ∈ span R (range v)
⊢ j ∈ span R (range (w • v))

Tactic:
rw [Submodule.mem_span] at hj ⊢

Result:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_7
inst✝³ : Group G
inst✝² : DistribMulAction G R
inst✝¹ : DistribMulAction G M
inst✝ : IsScalarTower G R M
v : ι → M
hv : span R (range v) = ⊤
w : ι → G
j : M
hj : ∀ (p : Submodule R M), range v ⊆ ↑p → j ∈ p
⊢ ∀ (p : Submodule R M), range (w • v) ⊆ ↑p → j ∈ p

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_7
inst✝³ : Group G
inst✝² : DistribMulAction G R
inst✝¹ : DistribMulAction G M
inst✝ : IsScalarTower G R M
v : ι → M
hv : span R (range v) = ⊤
w : ι → G
j : M
hj : j ∈ ⊤
⊢ j ∈ span R (range (w • v))

Tactic:
rw [← hv] at hj

Result:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_7
inst✝³ : Group G
inst✝² : DistribMulAction G R
inst✝¹ : DistribMulAction G M
inst✝ : IsScalarTower G R M
v : ι → M
hv : span R (range v) = ⊤
w : ι → G
j : M
hj : j ∈ span R (range v)
⊢ j ∈ span R (range (w • v))

Proof state:
case intro
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_7
inst✝³ : Group G
inst✝² : DistribMulAction G R
inst✝¹ : DistribMulAction G M
inst✝ : IsScalarTower G R M
v : ι → M
hv : span R (range v) = ⊤
w : ι → G
j : M
hj : ∀ (p : Submodule R M), range v ⊆ ↑p → j ∈ p
p : Submodule R M
hp : range (w • v) ⊆ ↑p
i : ι
this : ((w i)⁻¹ • 1) • w i • v i ∈ p
⊢ v i ∈ ↑p

Tactic:
rwa [smul_one_smul, inv_smul_smul] at this

Result:
no goals