[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s✝ S : Set G
s : G
hs : s ∈ S⁻¹
⊢ s ∈ ↑(closure S)
[PROOFSTEP]
rw [SetLike.mem_coe, ← Subgroup.inv_mem_iff]
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s✝ S : Set G
s : G
hs : s ∈ S⁻¹
⊢ s⁻¹ ∈ closure S
[PROOFSTEP]
exact subset_closure (mem_inv.mp hs)
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s S : Set G
⊢ (closure S).toSubmonoid = Submonoid.closure (S ∪ S⁻¹)
[PROOFSTEP]
refine le_antisymm (fun x hx => ?_) (Submonoid.closure_le.2 ?_)
[GOAL]
case refine_1
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s S : Set G
x : G
hx : x ∈ (closure S).toSubmonoid
⊢ x ∈ Submonoid.closure (S ∪ S⁻¹)
[PROOFSTEP]
refine'
  closure_induction hx (fun x hx => Submonoid.closure_mono (subset_union_left S S⁻¹) (Submonoid.subset_closure hx))
    (Submonoid.one_mem _) (fun x y hx hy => Submonoid.mul_mem _ hx hy) fun x hx => _
[GOAL]
case refine_1
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s S : Set G
x✝ : G
hx✝ : x✝ ∈ (closure S).toSubmonoid
x : G
hx : x ∈ Submonoid.closure (S ∪ S⁻¹)
⊢ x⁻¹ ∈ Submonoid.closure (S ∪ S⁻¹)
[PROOFSTEP]
rwa [← Submonoid.mem_closure_inv, Set.union_inv, inv_inv, Set.union_comm]
[GOAL]
case refine_2
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s S : Set G
⊢ S ∪ S⁻¹ ⊆ ↑(closure S).toSubmonoid
[PROOFSTEP]
simp only [true_and_iff, coe_toSubmonoid, union_subset_iff, subset_closure, inv_subset_closure]
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s✝ s : Set G
⊢ closure s⁻¹ = closure s
[PROOFSTEP]
simp only [← toSubmonoid_eq, closure_toSubmonoid, inv_inv, union_comm]
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x : G
hx : x ∈ ⨆ (i : ι), S i
hp : ∀ (i : ι) (x : G), x ∈ S i → C x
h1 : C 1
hmul : ∀ (x y : G), C x → C y → C (x * y)
⊢ C x
[PROOFSTEP]
rw [iSup_eq_closure] at hx 
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x : G
hx : x ∈ closure (⋃ (i : ι), ↑(S i))
hp : ∀ (i : ι) (x : G), x ∈ S i → C x
h1 : C 1
hmul : ∀ (x y : G), C x → C y → C (x * y)
⊢ C x
[PROOFSTEP]
refine' closure_induction'' hx (fun x hx => _) (fun x hx => _) h1 hmul
[GOAL]
case refine'_1
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x✝ : G
hx✝ : x✝ ∈ closure (⋃ (i : ι), ↑(S i))
hp : ∀ (i : ι) (x : G), x ∈ S i → C x
h1 : C 1
hmul : ∀ (x y : G), C x → C y → C (x * y)
x : G
hx : x ∈ ⋃ (i : ι), ↑(S i)
⊢ C x
[PROOFSTEP]
obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx
[GOAL]
case refine'_1.intro
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x✝ : G
hx✝ : x✝ ∈ closure (⋃ (i : ι), ↑(S i))
hp : ∀ (i : ι) (x : G), x ∈ S i → C x
h1 : C 1
hmul : ∀ (x y : G), C x → C y → C (x * y)
x : G
hx : x ∈ ⋃ (i : ι), ↑(S i)
i : ι
hi : x ∈ ↑(S i)
⊢ C x
[PROOFSTEP]
exact hp _ _ hi
[GOAL]
case refine'_2
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x✝ : G
hx✝ : x✝ ∈ closure (⋃ (i : ι), ↑(S i))
hp : ∀ (i : ι) (x : G), x ∈ S i → C x
h1 : C 1
hmul : ∀ (x y : G), C x → C y → C (x * y)
x : G
hx : x ∈ ⋃ (i : ι), ↑(S i)
⊢ C x⁻¹
[PROOFSTEP]
obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx
[GOAL]
case refine'_2.intro
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x✝ : G
hx✝ : x✝ ∈ closure (⋃ (i : ι), ↑(S i))
hp : ∀ (i : ι) (x : G), x ∈ S i → C x
h1 : C 1
hmul : ∀ (x y : G), C x → C y → C (x * y)
x : G
hx : x ∈ ⋃ (i : ι), ↑(S i)
i : ι
hi : x ∈ ↑(S i)
⊢ C x⁻¹
[PROOFSTEP]
exact hp _ _ (inv_mem hi)
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → x ∈ ⨆ (i : ι), S i → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : G) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i),
    C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ (i : ι), S i)
x : G
hx : x ∈ ⨆ (i : ι), S i
⊢ C x hx
[PROOFSTEP]
suffices : ∃ h, C x h
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → x ∈ ⨆ (i : ι), S i → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : G) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i),
    C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ (i : ι), S i)
x : G
hx : x ∈ ⨆ (i : ι), S i
this : ∃ h, C x h
⊢ C x hx
case this
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → x ∈ ⨆ (i : ι), S i → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : G) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i),
    C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ (i : ι), S i)
x : G
hx : x ∈ ⨆ (i : ι), S i
⊢ ∃ h, C x h
[PROOFSTEP]
exact this.snd
[GOAL]
case this
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → x ∈ ⨆ (i : ι), S i → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : G) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i),
    C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ (i : ι), S i)
x : G
hx : x ∈ ⨆ (i : ι), S i
⊢ ∃ h, C x h
[PROOFSTEP]
refine' iSup_induction S (C := fun x => ∃ h, C x h) hx (fun i x hx => _) _ fun x y => _
[GOAL]
case this.refine'_1
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → x ∈ ⨆ (i : ι), S i → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : G) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i),
    C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ (i : ι), S i)
x✝ : G
hx✝ : x✝ ∈ ⨆ (i : ι), S i
i : ι
x : G
hx : x ∈ S i
⊢ (fun x => ∃ h, C x h) x
[PROOFSTEP]
exact ⟨_, hp i _ hx⟩
[GOAL]
case this.refine'_2
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → x ∈ ⨆ (i : ι), S i → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : G) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i),
    C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ (i : ι), S i)
x : G
hx : x ∈ ⨆ (i : ι), S i
⊢ (fun x => ∃ h, C x h) 1
[PROOFSTEP]
exact ⟨_, h1⟩
[GOAL]
case this.refine'_3
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → x ∈ ⨆ (i : ι), S i → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : G) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i),
    C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ (i : ι), S i)
x✝ : G
hx : x✝ ∈ ⨆ (i : ι), S i
x y : G
⊢ (fun x => ∃ h, C x h) x → (fun x => ∃ h, C x h) y → (fun x => ∃ h, C x h) (x * y)
[PROOFSTEP]
rintro ⟨_, Cx⟩ ⟨_, Cy⟩
[GOAL]
case this.refine'_3.intro.intro
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → x ∈ ⨆ (i : ι), S i → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : G) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i),
    C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ (i : ι), S i)
x✝ : G
hx : x✝ ∈ ⨆ (i : ι), S i
x y : G
w✝¹ : x ∈ ⨆ (i : ι), S i
Cx : C x w✝¹
w✝ : y ∈ ⨆ (i : ι), S i
Cy : C y w✝
⊢ ∃ h, C (x * y) h
[PROOFSTEP]
refine' ⟨_, hmul _ _ _ _ Cx Cy⟩
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H K : Subgroup G
⊢ closure ↑H ⊔ closure ↑K ≤ H ⊔ K
[PROOFSTEP]
rw [closure_eq, closure_eq]
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s✝ s : Set G
N : Subgroup G
hN : Normal N
⊢ s * ↑N = ↑N * s
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s✝ s : Set G
N : Subgroup G
hN : Normal N
x : G
⊢ x ∈ s * ↑N ↔ x ∈ ↑N * s
[PROOFSTEP]
refine (exists_congr fun y => ?_).trans exists_swap
[GOAL]
case h
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s✝ s : Set G
N : Subgroup G
hN : Normal N
x y : G
⊢ (∃ b, y ∈ s ∧ b ∈ ↑N ∧ (fun x x_1 => x * x_1) y b = x) ↔ ∃ y_1, y_1 ∈ ↑N ∧ y ∈ s ∧ (fun x x_1 => x * x_1) y_1 y = x
[PROOFSTEP]
simp only [exists_and_left, @and_left_comm _ (y ∈ s), ← eq_inv_mul_iff_mul_eq (b := y), ←
  eq_mul_inv_iff_mul_eq (c := y), exists_eq_right, SetLike.mem_coe, hN.mem_comm_iff]
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H N : Subgroup G
hN : Normal N
⊢ ↑(H ⊔ N) = ↑H * ↑N
[PROOFSTEP]
rw [sup_eq_closure]
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H N : Subgroup G
hN : Normal N
⊢ ↑(closure (↑H * ↑N)) = ↑H * ↑N
[PROOFSTEP]
refine Set.Subset.antisymm (fun x hx => ?_) subset_closure
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H N : Subgroup G
hN : Normal N
x : G
hx : x ∈ ↑(closure (↑H * ↑N))
⊢ x ∈ ↑H * ↑N
[PROOFSTEP]
refine closure_induction'' (p := fun x => x ∈ (H : Set G) * (N : Set G)) hx ?_ ?_ ?_ ?_
[GOAL]
case refine_1
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H N : Subgroup G
hN : Normal N
x : G
hx : x ∈ ↑(closure (↑H * ↑N))
⊢ ∀ (x : G), x ∈ ↑H * ↑N → (fun x => x ∈ ↑H * ↑N) x
[PROOFSTEP]
rintro _ ⟨x, y, hx, hy, rfl⟩
[GOAL]
case refine_1.intro.intro.intro.intro
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H N : Subgroup G
hN : Normal N
x✝ : G
hx✝ : x✝ ∈ ↑(closure (↑H * ↑N))
x y : G
hx : x ∈ ↑H
hy : y ∈ ↑N
⊢ (fun x x_1 => x * x_1) x y ∈ ↑H * ↑N
[PROOFSTEP]
exact mul_mem_mul hx hy
[GOAL]
case refine_2
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H N : Subgroup G
hN : Normal N
x : G
hx : x ∈ ↑(closure (↑H * ↑N))
⊢ ∀ (x : G), x ∈ ↑H * ↑N → (fun x => x ∈ ↑H * ↑N) x⁻¹
[PROOFSTEP]
rintro _ ⟨x, y, hx, hy, rfl⟩
[GOAL]
case refine_2.intro.intro.intro.intro
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H N : Subgroup G
hN : Normal N
x✝ : G
hx✝ : x✝ ∈ ↑(closure (↑H * ↑N))
x y : G
hx : x ∈ ↑H
hy : y ∈ ↑N
⊢ ((fun x x_1 => x * x_1) x y)⁻¹ ∈ ↑H * ↑N
[PROOFSTEP]
simpa only [mul_inv_rev, mul_assoc, inv_inv, inv_mul_cancel_left] using
  mul_mem_mul (inv_mem hx) (hN.conj_mem _ (inv_mem hy) x)
[GOAL]
case refine_3
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H N : Subgroup G
hN : Normal N
x : G
hx : x ∈ ↑(closure (↑H * ↑N))
⊢ (fun x => x ∈ ↑H * ↑N) 1
[PROOFSTEP]
exact ⟨1, 1, one_mem _, one_mem _, mul_one 1⟩
[GOAL]
case refine_4
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H N : Subgroup G
hN : Normal N
x : G
hx : x ∈ ↑(closure (↑H * ↑N))
⊢ ∀ (x y : G), (fun x => x ∈ ↑H * ↑N) x → (fun x => x ∈ ↑H * ↑N) y → (fun x => x ∈ ↑H * ↑N) (x * y)
[PROOFSTEP]
rintro _ _ ⟨x, y, hx, hy, rfl⟩ ⟨x', y', hx', hy', rfl⟩
[GOAL]
case refine_4.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H N : Subgroup G
hN : Normal N
x✝ : G
hx✝ : x✝ ∈ ↑(closure (↑H * ↑N))
x y : G
hx : x ∈ ↑H
hy : y ∈ ↑N
x' y' : G
hx' : x' ∈ ↑H
hy' : y' ∈ ↑N
⊢ (fun x x_1 => x * x_1) x y * (fun x x_1 => x * x_1) x' y' ∈ ↑H * ↑N
[PROOFSTEP]
refine ⟨x * x', x'⁻¹ * y * x' * y', mul_mem hx hx', mul_mem ?_ hy', ?_⟩
[GOAL]
case refine_4.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H N : Subgroup G
hN : Normal N
x✝ : G
hx✝ : x✝ ∈ ↑(closure (↑H * ↑N))
x y : G
hx : x ∈ ↑H
hy : y ∈ ↑N
x' y' : G
hx' : x' ∈ ↑H
hy' : y' ∈ ↑N
⊢ x'⁻¹ * y * x' ∈ N
[PROOFSTEP]
simpa using hN.conj_mem _ hy x'⁻¹
[GOAL]
case refine_4.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H N : Subgroup G
hN : Normal N
x✝ : G
hx✝ : x✝ ∈ ↑(closure (↑H * ↑N))
x y : G
hx : x ∈ ↑H
hy : y ∈ ↑N
x' y' : G
hx' : x' ∈ ↑H
hy' : y' ∈ ↑N
⊢ (fun x x_1 => x * x_1) (x * x') (x'⁻¹ * y * x' * y') = (fun x x_1 => x * x_1) x y * (fun x x_1 => x * x_1) x' y'
[PROOFSTEP]
simp only [mul_assoc, mul_inv_cancel_left]
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝² : Group G
inst✝¹ : AddGroup A
s : Set G
N H : Subgroup G
inst✝ : Normal N
⊢ ↑(N ⊔ H) = ↑N * ↑H
[PROOFSTEP]
rw [← set_mul_normal_comm, sup_comm, mul_normal]
[GOAL]
α : Type u_1
G : Type u_2
A✝ : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A✝
s : Set G
A B C : Subgroup G
h : A ≤ C
⊢ ↑A * ↑(B ⊓ C) = ↑A * ↑B ⊓ ↑C
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
G : Type u_2
A✝ : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A✝
s : Set G
A B C : Subgroup G
h : A ≤ C
x✝ : G
⊢ x✝ ∈ ↑A * ↑(B ⊓ C) ↔ x✝ ∈ ↑A * ↑B ⊓ ↑C
[PROOFSTEP]
simp only [coe_inf, Set.inf_eq_inter, Set.mem_mul, Set.mem_inter_iff]
[GOAL]
case h
α : Type u_1
G : Type u_2
A✝ : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A✝
s : Set G
A B C : Subgroup G
h : A ≤ C
x✝ : G
⊢ (∃ x y, x ∈ ↑A ∧ (y ∈ ↑B ∧ y ∈ ↑C) ∧ x * y = x✝) ↔ (∃ x y, x ∈ ↑A ∧ y ∈ ↑B ∧ x * y = x✝) ∧ x✝ ∈ ↑C
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
G : Type u_2
A✝ : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A✝
s : Set G
A B C : Subgroup G
h : A ≤ C
x✝ : G
⊢ (∃ x y, x ∈ ↑A ∧ (y ∈ ↑B ∧ y ∈ ↑C) ∧ x * y = x✝) → (∃ x y, x ∈ ↑A ∧ y ∈ ↑B ∧ x * y = x✝) ∧ x✝ ∈ ↑C
[PROOFSTEP]
rintro ⟨y, z, hy, ⟨hzB, hzC⟩, rfl⟩
[GOAL]
case h.mp.intro.intro.intro.intro.intro
α : Type u_1
G : Type u_2
A✝ : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A✝
s : Set G
A B C : Subgroup G
h : A ≤ C
y z : G
hy : y ∈ ↑A
hzB : z ∈ ↑B
hzC : z ∈ ↑C
⊢ (∃ x y_1, x ∈ ↑A ∧ y_1 ∈ ↑B ∧ x * y_1 = y * z) ∧ y * z ∈ ↑C
[PROOFSTEP]
refine' ⟨_, mul_mem (h hy) hzC⟩
[GOAL]
case h.mp.intro.intro.intro.intro.intro
α : Type u_1
G : Type u_2
A✝ : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A✝
s : Set G
A B C : Subgroup G
h : A ≤ C
y z : G
hy : y ∈ ↑A
hzB : z ∈ ↑B
hzC : z ∈ ↑C
⊢ ∃ x y_1, x ∈ ↑A ∧ y_1 ∈ ↑B ∧ x * y_1 = y * z
[PROOFSTEP]
exact ⟨y, z, hy, hzB, rfl⟩
[GOAL]
case h.mpr
α : Type u_1
G : Type u_2
A✝ : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A✝
s : Set G
A B C : Subgroup G
h : A ≤ C
x✝ : G
⊢ (∃ x y, x ∈ ↑A ∧ y ∈ ↑B ∧ x * y = x✝) ∧ x✝ ∈ ↑C → ∃ x y, x ∈ ↑A ∧ (y ∈ ↑B ∧ y ∈ ↑C) ∧ x * y = x✝
[PROOFSTEP]
rintro ⟨⟨y, z, hy, hz, rfl⟩, hyz⟩
[GOAL]
case h.mpr.intro.intro.intro.intro.intro
α : Type u_1
G : Type u_2
A✝ : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A✝
s : Set G
A B C : Subgroup G
h : A ≤ C
y z : G
hy : y ∈ ↑A
hz : z ∈ ↑B
hyz : y * z ∈ ↑C
⊢ ∃ x y_1, x ∈ ↑A ∧ (y_1 ∈ ↑B ∧ y_1 ∈ ↑C) ∧ x * y_1 = y * z
[PROOFSTEP]
refine' ⟨y, z, hy, ⟨hz, _⟩, rfl⟩
[GOAL]
case h.mpr.intro.intro.intro.intro.intro
α : Type u_1
G : Type u_2
A✝ : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A✝
s : Set G
A B C : Subgroup G
h : A ≤ C
y z : G
hy : y ∈ ↑A
hz : z ∈ ↑B
hyz : y * z ∈ ↑C
⊢ z ∈ ↑C
[PROOFSTEP]
suffices y⁻¹ * (y * z) ∈ C by simpa
[GOAL]
α : Type u_1
G : Type u_2
A✝ : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A✝
s : Set G
A B C : Subgroup G
h : A ≤ C
y z : G
hy : y ∈ ↑A
hz : z ∈ ↑B
hyz : y * z ∈ ↑C
this : y⁻¹ * (y * z) ∈ C
⊢ z ∈ ↑C
[PROOFSTEP]
simpa
[GOAL]
case h.mpr.intro.intro.intro.intro.intro
α : Type u_1
G : Type u_2
A✝ : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A✝
s : Set G
A B C : Subgroup G
h : A ≤ C
y z : G
hy : y ∈ ↑A
hz : z ∈ ↑B
hyz : y * z ∈ ↑C
⊢ y⁻¹ * (y * z) ∈ C
[PROOFSTEP]
exact mul_mem (inv_mem (h hy)) hyz
[GOAL]
α : Type u_1
G : Type u_2
A✝ : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A✝
s : Set G
A B C : Subgroup G
h : C ≤ A
⊢ ↑(A ⊓ B) * ↑C = ↑A ⊓ ↑B * ↑C
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
G : Type u_2
A✝ : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A✝
s : Set G
A B C : Subgroup G
h : C ≤ A
x✝ : G
⊢ x✝ ∈ ↑(A ⊓ B) * ↑C ↔ x✝ ∈ ↑A ⊓ ↑B * ↑C
[PROOFSTEP]
simp only [coe_inf, Set.inf_eq_inter, Set.mem_mul, Set.mem_inter_iff]
[GOAL]
case h
α : Type u_1
G : Type u_2
A✝ : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A✝
s : Set G
A B C : Subgroup G
h : C ≤ A
x✝ : G
⊢ (∃ x y, (x ∈ ↑A ∧ x ∈ ↑B) ∧ y ∈ ↑C ∧ x * y = x✝) ↔ x✝ ∈ ↑A ∧ ∃ x y, x ∈ ↑B ∧ y ∈ ↑C ∧ x * y = x✝
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
G : Type u_2
A✝ : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A✝
s : Set G
A B C : Subgroup G
h : C ≤ A
x✝ : G
⊢ (∃ x y, (x ∈ ↑A ∧ x ∈ ↑B) ∧ y ∈ ↑C ∧ x * y = x✝) → x✝ ∈ ↑A ∧ ∃ x y, x ∈ ↑B ∧ y ∈ ↑C ∧ x * y = x✝
[PROOFSTEP]
rintro ⟨y, z, ⟨hyA, hyB⟩, hz, rfl⟩
[GOAL]
case h.mp.intro.intro.intro.intro.intro
α : Type u_1
G : Type u_2
A✝ : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A✝
s : Set G
A B C : Subgroup G
h : C ≤ A
y z : G
hyA : y ∈ ↑A
hyB : y ∈ ↑B
hz : z ∈ ↑C
⊢ y * z ∈ ↑A ∧ ∃ x y_1, x ∈ ↑B ∧ y_1 ∈ ↑C ∧ x * y_1 = y * z
[PROOFSTEP]
refine' ⟨A.mul_mem hyA (h hz), _⟩
[GOAL]
case h.mp.intro.intro.intro.intro.intro
α : Type u_1
G : Type u_2
A✝ : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A✝
s : Set G
A B C : Subgroup G
h : C ≤ A
y z : G
hyA : y ∈ ↑A
hyB : y ∈ ↑B
hz : z ∈ ↑C
⊢ ∃ x y_1, x ∈ ↑B ∧ y_1 ∈ ↑C ∧ x * y_1 = y * z
[PROOFSTEP]
exact ⟨y, z, hyB, hz, rfl⟩
[GOAL]
case h.mpr
α : Type u_1
G : Type u_2
A✝ : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A✝
s : Set G
A B C : Subgroup G
h : C ≤ A
x✝ : G
⊢ (x✝ ∈ ↑A ∧ ∃ x y, x ∈ ↑B ∧ y ∈ ↑C ∧ x * y = x✝) → ∃ x y, (x ∈ ↑A ∧ x ∈ ↑B) ∧ y ∈ ↑C ∧ x * y = x✝
[PROOFSTEP]
rintro ⟨hyz, y, z, hy, hz, rfl⟩
[GOAL]
case h.mpr.intro.intro.intro.intro.intro
α : Type u_1
G : Type u_2
A✝ : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A✝
s : Set G
A B C : Subgroup G
h : C ≤ A
y z : G
hy : y ∈ ↑B
hz : z ∈ ↑C
hyz : y * z ∈ ↑A
⊢ ∃ x y_1, (x ∈ ↑A ∧ x ∈ ↑B) ∧ y_1 ∈ ↑C ∧ x * y_1 = y * z
[PROOFSTEP]
refine' ⟨y, z, ⟨_, hy⟩, hz, rfl⟩
[GOAL]
case h.mpr.intro.intro.intro.intro.intro
α : Type u_1
G : Type u_2
A✝ : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A✝
s : Set G
A B C : Subgroup G
h : C ≤ A
y z : G
hy : y ∈ ↑B
hz : z ∈ ↑C
hyz : y * z ∈ ↑A
⊢ y ∈ ↑A
[PROOFSTEP]
suffices y * z * z⁻¹ ∈ A by simpa
[GOAL]
α : Type u_1
G : Type u_2
A✝ : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A✝
s : Set G
A B C : Subgroup G
h : C ≤ A
y z : G
hy : y ∈ ↑B
hz : z ∈ ↑C
hyz : y * z ∈ ↑A
this : y * z * z⁻¹ ∈ A
⊢ y ∈ ↑A
[PROOFSTEP]
simpa
[GOAL]
case h.mpr.intro.intro.intro.intro.intro
α : Type u_1
G : Type u_2
A✝ : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A✝
s : Set G
A B C : Subgroup G
h : C ≤ A
y z : G
hy : y ∈ ↑B
hz : z ∈ ↑C
hyz : y * z ∈ ↑A
⊢ y * z * z⁻¹ ∈ A
[PROOFSTEP]
exact mul_mem hyz (inv_mem (h hz))
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H K : Subgroup G
hH : Normal H
hK : Normal K
n : G
hmem : n ∈ H ⊔ K
g : G
⊢ g * n * g⁻¹ ∈ H ⊔ K
[PROOFSTEP]
rw [← SetLike.mem_coe, normal_mul] at hmem ⊢
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H K : Subgroup G
hH : Normal H
hK : Normal K
n : G
hmem : n ∈ ↑H * ↑K
g : G
⊢ g * n * g⁻¹ ∈ ↑H * ↑K
[PROOFSTEP]
rcases hmem with ⟨h, k, hh, hk, rfl⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H K : Subgroup G
hH : Normal H
hK : Normal K
g h k : G
hh : h ∈ ↑H
hk : k ∈ ↑K
⊢ g * (fun x x_1 => x * x_1) h k * g⁻¹ ∈ ↑H * ↑K
[PROOFSTEP]
refine ⟨g * h * g⁻¹, g * k * g⁻¹, hH.conj_mem h hh g, hK.conj_mem k hk g, ?_⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H K : Subgroup G
hH : Normal H
hK : Normal K
g h k : G
hh : h ∈ ↑H
hk : k ∈ ↑K
⊢ (fun x x_1 => x * x_1) (g * h * g⁻¹) (g * k * g⁻¹) = g * (fun x x_1 => x * x_1) h k * g⁻¹
[PROOFSTEP]
simp only [mul_assoc, inv_mul_cancel_left]
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s✝ : Set G
g : G
h : Gᵐᵒᵖ
s : Set G
⊢ (fun y => h • y) '' ((fun x => g * x) ⁻¹' s) = (fun x => g * x) ⁻¹' ((fun y => h • y) '' s)
[PROOFSTEP]
simp [preimage_preimage, mul_assoc]
  -- porting note: deprecate?
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝³ : Group G
inst✝² : AddGroup A
s : Set G
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction α G
S : Subgroup G
⊢ 1 • S = S
[PROOFSTEP]
change S.map _ = S
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝³ : Group G
inst✝² : AddGroup A
s : Set G
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction α G
S : Subgroup G
⊢ map (↑(MulDistribMulAction.toMonoidEnd α G) 1) S = S
[PROOFSTEP]
simpa only [map_one] using S.map_id
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝³ : Group G
inst✝² : AddGroup A
s : Set G
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction α G
P H : Subgroup G
hP : P ≤ H
h : { x // x ∈ H }
⊢ ↑MulAut.conj ↑h • P ≤ H
[PROOFSTEP]
rintro - ⟨g, hg, rfl⟩
[GOAL]
case intro.intro
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝³ : Group G
inst✝² : AddGroup A
s : Set G
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction α G
P H : Subgroup G
hP : P ≤ H
h : { x // x ∈ H }
g : G
hg : g ∈ ↑P
⊢ ↑(↑(MulDistribMulAction.toMonoidEnd ((fun x => MulAut G) ↑h) G) (↑MulAut.conj ↑h)) g ∈ H
[PROOFSTEP]
exact H.mul_mem (H.mul_mem h.2 (hP hg)) (H.inv_mem h.2)
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝³ : Group G
inst✝² : AddGroup A
s : Set G
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction α G
P H : Subgroup G
hP : P ≤ H
h : { x // x ∈ H }
⊢ ↑MulAut.conj h • subgroupOf P H = subgroupOf (↑MulAut.conj ↑h • P) H
[PROOFSTEP]
refine' le_antisymm _ _
[GOAL]
case refine'_1
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝³ : Group G
inst✝² : AddGroup A
s : Set G
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction α G
P H : Subgroup G
hP : P ≤ H
h : { x // x ∈ H }
⊢ ↑MulAut.conj h • subgroupOf P H ≤ subgroupOf (↑MulAut.conj ↑h • P) H
[PROOFSTEP]
rintro - ⟨g, hg, rfl⟩
[GOAL]
case refine'_1.intro.intro
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝³ : Group G
inst✝² : AddGroup A
s : Set G
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction α G
P H : Subgroup G
hP : P ≤ H
h g : { x // x ∈ H }
hg : g ∈ ↑(subgroupOf P H)
⊢ ↑(↑(MulDistribMulAction.toMonoidEnd ((fun x => MulAut { x // x ∈ H }) h) { x // x ∈ H }) (↑MulAut.conj h)) g ∈
    subgroupOf (↑MulAut.conj ↑h • P) H
[PROOFSTEP]
exact ⟨g, hg, rfl⟩
[GOAL]
case refine'_2
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝³ : Group G
inst✝² : AddGroup A
s : Set G
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction α G
P H : Subgroup G
hP : P ≤ H
h : { x // x ∈ H }
⊢ subgroupOf (↑MulAut.conj ↑h • P) H ≤ ↑MulAut.conj h • subgroupOf P H
[PROOFSTEP]
rintro p ⟨g, hg, hp⟩
[GOAL]
case refine'_2.intro.intro
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝³ : Group G
inst✝² : AddGroup A
s : Set G
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction α G
P H : Subgroup G
hP : P ≤ H
h p : { x // x ∈ H }
g : G
hg : g ∈ ↑P
hp : ↑(↑(MulDistribMulAction.toMonoidEnd ((fun x => MulAut G) ↑h) G) (↑MulAut.conj ↑h)) g = ↑(Subgroup.subtype H) p
⊢ p ∈ ↑MulAut.conj h • subgroupOf P H
[PROOFSTEP]
exact ⟨⟨g, hP hg⟩, hg, Subtype.ext hp⟩
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝³ : Group G
inst✝² : AddGroup A
s : Set G
inst✝¹ : Group α
inst✝ : MulDistribMulAction α G
a : α
S T : Subgroup G
⊢ a • (S ⊓ T) = a • S ⊓ a • T
[PROOFSTEP]
simp [SetLike.ext_iff, mem_pointwise_smul_iff_inv_smul_mem]
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝³ : Group G
inst✝² : AddGroup A
s : Set G
inst✝¹ : Group α
inst✝ : MulDistribMulAction α G
H : Subgroup G
h : G
hh : h ∈ H
this : {x | x ∈ H} = ↑H
⊢ ↑H * {h} = ↑H
[PROOFSTEP]
simpa [preimage, mul_mem_cancel_right (inv_mem hh)]
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝³ : Group G
inst✝² : AddGroup A
s : Set G
inst✝¹ : Group α
inst✝ : MulDistribMulAction α G
H : Subgroup G
h : G
hh : h ∈ H
this : {x | x ∈ H} = ↑H
⊢ {h} * ↑H = ↑H
[PROOFSTEP]
simpa [preimage, mul_mem_cancel_left (inv_mem hh)]
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝³ : Group G
inst✝² : AddGroup A
s : Set G
inst✝¹ : Monoid α
inst✝ : DistribMulAction α A
S : AddSubgroup A
⊢ 1 • S = S
[PROOFSTEP]
change S.map _ = S
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝³ : Group G
inst✝² : AddGroup A
s : Set G
inst✝¹ : Monoid α
inst✝ : DistribMulAction α A
S : AddSubgroup A
⊢ map (↑(DistribMulAction.toAddMonoidEnd α A) 1) S = S
[PROOFSTEP]
simpa only [map_one] using S.map_id
