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

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

Tactic:
ext

Result:
case h
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : C ≤ A
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 : C ≤ A
y : G
hy : y ∈ ↑B
z : G
hz : z ∈ ↑C
hyz : y * z ∈ ↑A
⊢ y * z * z⁻¹ ∈ A

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

Result:
no goals

Proof state:
case h.mpr.intro.intro.intro.intro.intro
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : C ≤ A
y : G
hy : y ∈ ↑B
z : G
hz : z ∈ ↑C
hyz : y * z ∈ ↑A
⊢ ∃ x, (x ∈ ↑A ∧ x ∈ ↑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 : C ≤ A
y : G
hy : y ∈ ↑B
z : G
hz : z ∈ ↑C
hyz : y * z ∈ ↑A
⊢ y ∈ ↑A

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

Tactic:
constructor

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

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

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

Tactic:
suffices y * z * z⁻¹ ∈ A by simpa

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

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

Tactic:
rintro ⟨hyz, 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 : C ≤ A
y : G
hy : y ∈ ↑B
z : G
hz : z ∈ ↑C
hyz : y * z ∈ ↑A
⊢ ∃ x, (x ∈ ↑A ∧ x ∈ ↑B) ∧ ∃ y_1 ∈ ↑C, x * y_1 = y * z

Proof state:
case h
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : C ≤ A
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 : C ≤ A
x✝ : G
⊢ (∃ x, (x ∈ ↑A ∧ x ∈ ↑B) ∧ ∃ y ∈ ↑C, x * y = x✝) ↔ x✝ ∈ ↑A ∧ ∃ x ∈ ↑B, ∃ y ∈ ↑C, x * y = x✝

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

Tactic:
rintro ⟨y, ⟨hyA, hyB⟩, z, hz, rfl⟩

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

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

Tactic:
exact ⟨y, hyB, z, hz, rfl⟩

Result:
no goals

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

Tactic:
refine ⟨A.mul_mem hyA (h hz), ?_⟩

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

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

Tactic:
simpa

Result:
no goals