-- Mathlib/Algebra/Group/Subgroup/Pointwise.lean
theorem mul_inf_assoc (A B C : Subgroup G) (h : A ≤ C) :
    (A : Set G) * ↑(B ⊓ C) = (A : Set G) * (B : Set G) ∩ C

Proof state:
case h.mp.intro.intro.intro.intro.intro
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : A ≤ C
y : G
hy : y ∈ ↑A
z : G
hzB : z ∈ ↑B
hzC : z ∈ ↑C
⊢ (∃ x ∈ ↑A, ∃ y_1 ∈ ↑B, x * y_1 = y * z) ∧ y * z ∈ ↑C

Tactic:
refine ⟨?_, mul_mem (h hy) hzC⟩

Result:
case h.mp.intro.intro.intro.intro.intro
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : A ≤ C
y : G
hy : y ∈ ↑A
z : G
hzB : z ∈ ↑B
hzC : z ∈ ↑C
⊢ ∃ x ∈ ↑A, ∃ y_1 ∈ ↑B, x * y_1 = y * z

Proof state:
case h.mp
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : A ≤ C
x✝ : G
⊢ (∃ x ∈ ↑A, ∃ y, (y ∈ ↑B ∧ y ∈ ↑C) ∧ x * y = x✝) → (∃ x ∈ ↑A, ∃ y ∈ ↑B, x * y = x✝) ∧ x✝ ∈ ↑C

Tactic:
rintro ⟨y, hy, z, ⟨hzB, hzC⟩, rfl⟩

Result:
case h.mp.intro.intro.intro.intro.intro
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : A ≤ C
y : G
hy : y ∈ ↑A
z : G
hzB : z ∈ ↑B
hzC : z ∈ ↑C
⊢ (∃ x ∈ ↑A, ∃ y_1 ∈ ↑B, x * y_1 = y * z) ∧ y * z ∈ ↑C

Proof state:
case h.mpr.intro.intro.intro.intro.intro
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : A ≤ C
y : G
hy : y ∈ ↑A
z : G
hz : z ∈ ↑B
hyz : y * z ∈ ↑C
⊢ y⁻¹ * (y * z) ∈ C

Tactic:
exact mul_mem (inv_mem (h hy)) hyz

Result:
no goals

Proof state:
case h
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : A ≤ C
x✝ : G
⊢ (∃ x ∈ ↑A, ∃ y, (y ∈ ↑B ∧ y ∈ ↑C) ∧ x * y = x✝) ↔ (∃ x ∈ ↑A, ∃ y ∈ ↑B, x * y = x✝) ∧ x✝ ∈ ↑C

Tactic:
constructor

Result:
case h.mp
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : A ≤ C
x✝ : G
⊢ (∃ x ∈ ↑A, ∃ y, (y ∈ ↑B ∧ y ∈ ↑C) ∧ x * y = x✝) → (∃ x ∈ ↑A, ∃ y ∈ ↑B, x * y = x✝) ∧ x✝ ∈ ↑C

case h.mpr
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : A ≤ C
x✝ : G
⊢ (∃ x ∈ ↑A, ∃ y ∈ ↑B, x * y = x✝) ∧ x✝ ∈ ↑C → ∃ x ∈ ↑A, ∃ y, (y ∈ ↑B ∧ y ∈ ↑C) ∧ x * y = x✝

Proof state:
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : A ≤ C
y : G
hy : y ∈ ↑A
z : G
hz : z ∈ ↑B
hyz : y * z ∈ ↑C
this : y⁻¹ * (y * z) ∈ C
⊢ z ∈ ↑C

Tactic:
simpa

Result:
no goals

Proof state:
case h.mpr
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : A ≤ C
x✝ : G
⊢ (∃ x ∈ ↑A, ∃ y ∈ ↑B, x * y = x✝) ∧ x✝ ∈ ↑C → ∃ x ∈ ↑A, ∃ y, (y ∈ ↑B ∧ y ∈ ↑C) ∧ x * y = x✝

Tactic:
rintro ⟨⟨y, hy, z, hz, rfl⟩, hyz⟩

Result:
case h.mpr.intro.intro.intro.intro.intro
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : A ≤ C
y : G
hy : y ∈ ↑A
z : G
hz : z ∈ ↑B
hyz : y * z ∈ ↑C
⊢ ∃ x ∈ ↑A, ∃ y_1, (y_1 ∈ ↑B ∧ y_1 ∈ ↑C) ∧ x * y_1 = y * z

Proof state:
case h.mpr.intro.intro.intro.intro.intro
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : A ≤ C
y : G
hy : y ∈ ↑A
z : G
hz : z ∈ ↑B
hyz : y * z ∈ ↑C
⊢ ∃ x ∈ ↑A, ∃ y_1, (y_1 ∈ ↑B ∧ y_1 ∈ ↑C) ∧ x * y_1 = y * z

Tactic:
refine ⟨y, hy, z, ⟨hz, ?_⟩, rfl⟩

Result:
case h.mpr.intro.intro.intro.intro.intro
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : A ≤ C
y : G
hy : y ∈ ↑A
z : G
hz : z ∈ ↑B
hyz : y * z ∈ ↑C
⊢ z ∈ ↑C

Proof state:
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : A ≤ C
⊢ ↑A * ↑(B ⊓ C) = ↑A * ↑B ∩ ↑C

Tactic:
ext

Result:
case h
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : A ≤ C
x✝ : G
⊢ x✝ ∈ ↑A * ↑(B ⊓ C) ↔ x✝ ∈ ↑A * ↑B ∩ ↑C

Proof state:
case h.mpr.intro.intro.intro.intro.intro
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : A ≤ C
y : G
hy : y ∈ ↑A
z : G
hz : z ∈ ↑B
hyz : y * z ∈ ↑C
⊢ z ∈ ↑C

Tactic:
suffices y⁻¹ * (y * z) ∈ C by simpa

Result:
case h.mpr.intro.intro.intro.intro.intro
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : A ≤ C
y : G
hy : y ∈ ↑A
z : G
hz : z ∈ ↑B
hyz : y * z ∈ ↑C
⊢ y⁻¹ * (y * z) ∈ C

Proof state:
case h.mp.intro.intro.intro.intro.intro
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : A ≤ C
y : G
hy : y ∈ ↑A
z : G
hzB : z ∈ ↑B
hzC : z ∈ ↑C
⊢ ∃ x ∈ ↑A, ∃ y_1 ∈ ↑B, x * y_1 = y * z

Tactic:
exact ⟨y, hy, z, hzB, rfl⟩

Result:
no goals

Proof state:
case h
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : A ≤ C
x✝ : G
⊢ x✝ ∈ ↑A * ↑(B ⊓ C) ↔ x✝ ∈ ↑A * ↑B ∩ ↑C

Tactic:
simp only [coe_inf, Set.mem_mul, Set.mem_inter_iff]

Result:
case h
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : A ≤ C
x✝ : G
⊢ (∃ x ∈ ↑A, ∃ y, (y ∈ ↑B ∧ y ∈ ↑C) ∧ x * y = x✝) ↔ (∃ x ∈ ↑A, ∃ y ∈ ↑B, x * y = x✝) ∧ x✝ ∈ ↑C