case h
α : Type ?u.39028
G : Type u_1
A✝ : Type ?u.39034
S : Type ?u.39037
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
α : Type ?u.39028
G : Type u_1
A✝ : Type ?u.39034
S : Type ?u.39037
inst✝¹ : Group G
inst✝ : AddGroup A✝
s : Set G
A B C : Subgroup G
h : C ≤ A
⊢ ↑(A ⊓ B) * ↑C = ↑A ⊓ ↑B * ↑C
ext
case h
α : Type ?u.39028
G : Type u_1
A✝ : Type ?u.39034
S : Type ?u.39037
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✝
case h
α : Type ?u.39028
G : Type u_1
A✝ : Type ?u.39034
S : Type ?u.39037
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
simp only [coe_inf, Set.inf_eq_inter, Set.mem_mul, Set.mem_inter_iff]
case h.mp
α : Type ?u.39028
G : Type u_1
A✝ : Type ?u.39034
S : Type ?u.39037
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✝

case h.mpr
α : Type ?u.39028
G : Type u_1
A✝ : Type ?u.39034
S : Type ?u.39037
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✝
case h
α : Type ?u.39028
G : Type u_1
A✝ : Type ?u.39034
S : Type ?u.39037
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✝
constructor
case h.mpr.intro.intro.intro.intro.intro
α : Type ?u.39028
G : Type u_1
A✝ : Type ?u.39034
S : Type ?u.39037
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
case h.mpr
α : Type ?u.39028
G : Type u_1
A✝ : Type ?u.39034
S : Type ?u.39037
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✝
rintro ⟨hyz, y, z, hy, hz, rfl⟩
case h.mpr.intro.intro.intro.intro.intro
α : Type ?u.39028
G : Type u_1
A✝ : Type ?u.39034
S : Type ?u.39037
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
case h.mpr.intro.intro.intro.intro.intro
α : Type ?u.39028
G : Type u_1
A✝ : Type ?u.39034
S : Type ?u.39037
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
refine' ⟨y, z, ⟨_, hy⟩, hz, rfl⟩
case h.mpr.intro.intro.intro.intro.intro
α : Type ?u.39028
G : Type u_1
A✝ : Type ?u.39034
S : Type ?u.39037
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
case h.mpr.intro.intro.intro.intro.intro
α : Type ?u.39028
G : Type u_1
A✝ : Type ?u.39034
S : Type ?u.39037
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
suffices y * z * z⁻¹ ∈ A by simpa
no goals
case h.mpr.intro.intro.intro.intro.intro
α : Type ?u.39028
G : Type u_1
A✝ : Type ?u.39034
S : Type ?u.39037
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
exact mul_mem hyz (inv_mem (h hz))
case h.mp.intro.intro.intro.intro.intro
α : Type ?u.39028
G : Type u_1
A✝ : Type ?u.39034
S : Type ?u.39037
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
case h.mp
α : Type ?u.39028
G : Type u_1
A✝ : Type ?u.39034
S : Type ?u.39037
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✝
rintro ⟨y, z, ⟨hyA, hyB⟩, hz, rfl⟩
case h.mp.intro.intro.intro.intro.intro
α : Type ?u.39028
G : Type u_1
A✝ : Type ?u.39034
S : Type ?u.39037
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
case h.mp.intro.intro.intro.intro.intro
α : Type ?u.39028
G : Type u_1
A✝ : Type ?u.39034
S : Type ?u.39037
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
refine' ⟨A.mul_mem hyA (h hz), _⟩
no goals
case h.mp.intro.intro.intro.intro.intro
α : Type ?u.39028
G : Type u_1
A✝ : Type ?u.39034
S : Type ?u.39037
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
exact ⟨y, z, hyB, hz, rfl⟩
no goals
α : Type ?u.39028
G : Type u_1
A✝ : Type ?u.39034
S : Type ?u.39037
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
simpa