case refine'_1
M : Type u_1
N : Type ?u.95294
P : Type ?u.95297
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.95318
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Set M
x✝¹ : { x // x ∈ ↑(closure s) }
x : M
hx : x ∈ ↑(closure s)
x✝ : { val := x, property := hx } ∈ ⊤
⊢ { val := 1, property := (_ : 1 ∈ closure s) } ∈ closure (Subtype.val ⁻¹' s)

case refine'_2
M : Type u_1
N : Type ?u.95294
P : Type ?u.95297
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.95318
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Set M
x✝¹ : { x // x ∈ ↑(closure s) }
x : M
hx : x ∈ ↑(closure s)
x✝ : { val := x, property := hx } ∈ ⊤
g₁ : M
g₂ : g₁ ∈ closure s
hg₁ : M
hg₂ : hg₁ ∈ closure s
⊢ { val := g₁, property := g₂ } ∈ closure (Subtype.val ⁻¹' s) →
    { val := hg₁, property := hg₂ } ∈ closure (Subtype.val ⁻¹' s) →
      { val := g₁ * hg₁, property := (_ : g₁ * hg₁ ∈ closure s) } ∈ closure (Subtype.val ⁻¹' s)
M : Type u_1
N : Type ?u.95294
P : Type ?u.95297
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.95318
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Set M
x✝¹ : { x // x ∈ ↑(closure s) }
x : M
hx : x ∈ ↑(closure s)
x✝ : { val := x, property := hx } ∈ ⊤
⊢ { val := x, property := hx } ∈ closure (Subtype.val ⁻¹' s)
refine' closure_induction' _ (fun g hg => subset_closure hg) _ (fun g₁ g₂ hg₁ hg₂ => _) hx
no goals
case refine'_1
M : Type u_1
N : Type ?u.95294
P : Type ?u.95297
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.95318
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Set M
x✝¹ : { x // x ∈ ↑(closure s) }
x : M
hx : x ∈ ↑(closure s)
x✝ : { val := x, property := hx } ∈ ⊤
⊢ { val := 1, property := (_ : 1 ∈ closure s) } ∈ closure (Subtype.val ⁻¹' s)
exact Submonoid.one_mem _
no goals
case refine'_2
M : Type u_1
N : Type ?u.95294
P : Type ?u.95297
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.95318
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
s : Set M
x✝¹ : { x // x ∈ ↑(closure s) }
x : M
hx : x ∈ ↑(closure s)
x✝ : { val := x, property := hx } ∈ ⊤
g₁ : M
g₂ : g₁ ∈ closure s
hg₁ : M
hg₂ : hg₁ ∈ closure s
⊢ { val := g₁, property := g₂ } ∈ closure (Subtype.val ⁻¹' s) →
    { val := hg₁, property := hg₂ } ∈ closure (Subtype.val ⁻¹' s) →
      { val := g₁ * hg₁, property := (_ : g₁ * hg₁ ∈ closure s) } ∈ closure (Subtype.val ⁻¹' s)
exact Submonoid.mul_mem _