case refine'_1
G : Type u_1
G' : Type ?u.207006
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.207015
inst✝ : AddGroup A
H K : Subgroup G
k✝ k : Set G
x✝¹ : { x // x ∈ ↑(closure k) }
x : G
hx : x ∈ ↑(closure k)
x✝ : { val := x, property := hx } ∈ ⊤
g : G
hg : g ∈ k
⊢ { val := g, property := (_ : g ∈ ↑(closure k)) } ∈ closure (Subtype.val ⁻¹' k)

case refine'_2
G : Type u_1
G' : Type ?u.207006
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.207015
inst✝ : AddGroup A
H K : Subgroup G
k✝ k : Set G
x✝¹ : { x // x ∈ ↑(closure k) }
x : G
hx : x ∈ ↑(closure k)
x✝ : { val := x, property := hx } ∈ ⊤
⊢ { val := 1, property := (_ : 1 ∈ closure k) } ∈ closure (Subtype.val ⁻¹' k)

case refine'_3
G : Type u_1
G' : Type ?u.207006
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.207015
inst✝ : AddGroup A
H K : Subgroup G
k✝ k : Set G
x✝¹ : { x // x ∈ ↑(closure k) }
x : G
hx : x ∈ ↑(closure k)
x✝ : { val := x, property := hx } ∈ ⊤
g₁ : G
g₂ : g₁ ∈ closure k
hg₁ : G
hg₂ : hg₁ ∈ closure k
⊢ { val := g₁, property := g₂ } ∈ closure (Subtype.val ⁻¹' k) →
    { val := hg₁, property := hg₂ } ∈ closure (Subtype.val ⁻¹' k) →
      { val := g₁ * hg₁, property := (_ : g₁ * hg₁ ∈ closure k) } ∈ closure (Subtype.val ⁻¹' k)

case refine'_4
G : Type u_1
G' : Type ?u.207006
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.207015
inst✝ : AddGroup A
H K : Subgroup G
k✝ k : Set G
x✝¹ : { x // x ∈ ↑(closure k) }
x : G
hx : x ∈ ↑(closure k)
x✝ : { val := x, property := hx } ∈ ⊤
g : G
hg : g ∈ closure k
⊢ { val := g, property := hg } ∈ closure (Subtype.val ⁻¹' k) →
    { val := g⁻¹, property := (_ : g⁻¹ ∈ closure k) } ∈ closure (Subtype.val ⁻¹' k)
G : Type u_1
G' : Type ?u.207006
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.207015
inst✝ : AddGroup A
H K : Subgroup G
k✝ k : Set G
x✝¹ : { x // x ∈ ↑(closure k) }
x : G
hx : x ∈ ↑(closure k)
x✝ : { val := x, property := hx } ∈ ⊤
⊢ { val := x, property := hx } ∈ closure (Subtype.val ⁻¹' k)
refine' closure_induction' (fun g hg => _) _ (fun g₁ g₂ hg₁ hg₂ => _) (fun g hg => _) hx
no goals
case refine'_1
G : Type u_1
G' : Type ?u.207006
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.207015
inst✝ : AddGroup A
H K : Subgroup G
k✝ k : Set G
x✝¹ : { x // x ∈ ↑(closure k) }
x : G
hx : x ∈ ↑(closure k)
x✝ : { val := x, property := hx } ∈ ⊤
g : G
hg : g ∈ k
⊢ { val := g, property := (_ : g ∈ ↑(closure k)) } ∈ closure (Subtype.val ⁻¹' k)
exact subset_closure hg
no goals
case refine'_2
G : Type u_1
G' : Type ?u.207006
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.207015
inst✝ : AddGroup A
H K : Subgroup G
k✝ k : Set G
x✝¹ : { x // x ∈ ↑(closure k) }
x : G
hx : x ∈ ↑(closure k)
x✝ : { val := x, property := hx } ∈ ⊤
⊢ { val := 1, property := (_ : 1 ∈ closure k) } ∈ closure (Subtype.val ⁻¹' k)
exact one_mem _
no goals
case refine'_3
G : Type u_1
G' : Type ?u.207006
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.207015
inst✝ : AddGroup A
H K : Subgroup G
k✝ k : Set G
x✝¹ : { x // x ∈ ↑(closure k) }
x : G
hx : x ∈ ↑(closure k)
x✝ : { val := x, property := hx } ∈ ⊤
g₁ : G
g₂ : g₁ ∈ closure k
hg₁ : G
hg₂ : hg₁ ∈ closure k
⊢ { val := g₁, property := g₂ } ∈ closure (Subtype.val ⁻¹' k) →
    { val := hg₁, property := hg₂ } ∈ closure (Subtype.val ⁻¹' k) →
      { val := g₁ * hg₁, property := (_ : g₁ * hg₁ ∈ closure k) } ∈ closure (Subtype.val ⁻¹' k)
exact mul_mem
no goals
case refine'_4
G : Type u_1
G' : Type ?u.207006
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.207015
inst✝ : AddGroup A
H K : Subgroup G
k✝ k : Set G
x✝¹ : { x // x ∈ ↑(closure k) }
x : G
hx : x ∈ ↑(closure k)
x✝ : { val := x, property := hx } ∈ ⊤
g : G
hg : g ∈ closure k
⊢ { val := g, property := hg } ∈ closure (Subtype.val ⁻¹' k) →
    { val := g⁻¹, property := (_ : g⁻¹ ∈ closure k) } ∈ closure (Subtype.val ⁻¹' k)
exact inv_mem