-- Mathlib/RingTheory/FiniteType.lean
theorem mem_closure_of_mem_span_closure [Nontrivial R] {m : M} {S : Set M}
    (h : of' R M m ∈ span R (Submonoid.closure (of' R M '' S) : Set R[M])) :
    m ∈ closure S

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddMonoid M
inst✝ : Nontrivial R
m : M
S : Set M
h : of' R M m ∈ span R ↑(Submonoid.closure (of' R M '' S))
S' : Submonoid (Multiplicative M) := Submonoid.closure S
h' : Submonoid.map (of R M) S' = Submonoid.closure ((fun x => (of R M) x) '' S)
⊢ Multiplicative.ofAdd m ∈ Submonoid.closure (⇑Multiplicative.toAdd ⁻¹' S)

Tactic:
rw [Set.image_congr' (show ∀ x, of' R M x = of R M x from fun x => of'_eq_of x), ← h'] at h

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddMonoid M
inst✝ : Nontrivial R
m : M
S : Set M
S' : Submonoid (Multiplicative M) := Submonoid.closure S
h : of' R M m ∈ span R ↑(Submonoid.map (of R M) S')
h' : Submonoid.map (of R M) S' = Submonoid.closure ((fun x => (of R M) x) '' S)
⊢ Multiplicative.ofAdd m ∈ Submonoid.closure (⇑Multiplicative.toAdd ⁻¹' S)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddMonoid M
inst✝ : Nontrivial R
m : M
S : Set M
h : of' R M m ∈ span R ↑(Submonoid.closure (of' R M '' S))
this : Multiplicative.ofAdd m ∈ Submonoid.closure (⇑Multiplicative.toAdd ⁻¹' S)
⊢ m ∈ closure S

Tactic:
simpa [← toSubmonoid_closure]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddMonoid M
inst✝ : Nontrivial R
m : M
S : Set M
h : of' R M m ∈ span R ↑(Submonoid.closure (of' R M '' S))
⊢ m ∈ closure S

Tactic:
suffices Multiplicative.ofAdd m ∈ Submonoid.closure (Multiplicative.toAdd ⁻¹' S) by
  simpa [← toSubmonoid_closure]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddMonoid M
inst✝ : Nontrivial R
m : M
S : Set M
h : of' R M m ∈ span R ↑(Submonoid.closure (of' R M '' S))
⊢ Multiplicative.ofAdd m ∈ Submonoid.closure (⇑Multiplicative.toAdd ⁻¹' S)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddMonoid M
inst✝ : Nontrivial R
m : M
S : Set M
h : of' R M m ∈ span R ↑(Submonoid.closure (of' R M '' S))
S' : Submonoid (Multiplicative M) := Submonoid.closure S
⊢ Multiplicative.ofAdd m ∈ Submonoid.closure (⇑Multiplicative.toAdd ⁻¹' S)

Tactic:
have h' : Submonoid.map (of R M) S' = Submonoid.closure ((fun x : M => (of R M) x) '' S) :=
  MonoidHom.map_mclosure _ _

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddMonoid M
inst✝ : Nontrivial R
m : M
S : Set M
h : of' R M m ∈ span R ↑(Submonoid.closure (of' R M '' S))
S' : Submonoid (Multiplicative M) := Submonoid.closure S
h' : Submonoid.map (of R M) S' = Submonoid.closure ((fun x => (of R M) x) '' S)
⊢ Multiplicative.ofAdd m ∈ Submonoid.closure (⇑Multiplicative.toAdd ⁻¹' S)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddMonoid M
inst✝ : Nontrivial R
m : M
S : Set M
h : of' R M m ∈ span R ↑(Submonoid.closure (of' R M '' S))
⊢ Multiplicative.ofAdd m ∈ Submonoid.closure (⇑Multiplicative.toAdd ⁻¹' S)

Tactic:
let S' := @Submonoid.closure (Multiplicative M) Multiplicative.mulOneClass S

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddMonoid M
inst✝ : Nontrivial R
m : M
S : Set M
h : of' R M m ∈ span R ↑(Submonoid.closure (of' R M '' S))
S' : Submonoid (Multiplicative M) := Submonoid.closure S
⊢ Multiplicative.ofAdd m ∈ Submonoid.closure (⇑Multiplicative.toAdd ⁻¹' S)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddMonoid M
inst✝ : Nontrivial R
m : M
S : Set M
S' : Submonoid (Multiplicative M) := Submonoid.closure S
h : of' R M m ∈ span R ↑(Submonoid.map (of R M) S')
h' : Submonoid.map (of R M) S' = Submonoid.closure ((fun x => (of R M) x) '' S)
⊢ Multiplicative.ofAdd m ∈ Submonoid.closure (⇑Multiplicative.toAdd ⁻¹' S)

Tactic:
simpa using of'_mem_span.1 h

Result:
no goals