R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid 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)
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid 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
suffices Multiplicative.ofAdd m ∈ Submonoid.closure (Multiplicative.toAdd ⁻¹' S) by
  simpa [← toSubmonoid_closure]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid 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)
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid 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)
let S' := @Submonoid.closure (Multiplicative M) Multiplicative.mulOneClass S
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid 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)
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid 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)
have h' : Submonoid.map (of R M) S' = Submonoid.closure ((fun x : M => (of R M) x) '' S) :=
  MonoidHom.map_mclosure _ _
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid 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)
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid 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)
rw [Set.image_congr' (show ∀ x, of' R M x = of R M x from fun x => of'_eq_of x), ← h'] at h
no goals
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid 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)
simpa using of'_mem_span.1 h
no goals
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid 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
simpa [← toSubmonoid_closure]