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

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