M : Type u_1
N : Type ?u.47324
P : Type ?u.47327
σ : Type ?u.47330
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S : Subsemigroup M
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.47324
P : Type ?u.47327
σ : Type ?u.47330
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S : Subsemigroup M
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
M : Type u_1
N : Type ?u.47324
P : Type ?u.47327
σ : Type ?u.47330
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S : Subsemigroup M
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 Subsemigroup.mul_mem _