Theorem: ex_1_2_5 (AlgebraI/Subgroups.lean)

State before:
G : Type u_1
inst✝ : Group G
A B : Set G
g : G
⊢ {x | ∃ x_1 ∈ A ∩ B, g * x_1 = x} = {x | ∃ x_1 ∈ A, g * x_1 = x} ∩ {x | ∃ x_1 ∈ B, g * x_1 = x}
Tactic:
ext y
State after:
case h
G : Type u_1
inst✝ : Group G
A B : Set G
g y : G
⊢ y ∈ {x | ∃ x_1 ∈ A ∩ B, g * x_1 = x} ↔ y ∈ {x | ∃ x_1 ∈ A, g * x_1 = x} ∩ {x | ∃ x_1 ∈ B, g * x_1 = x}

State before:
case h
G : Type u_1
inst✝ : Group G
A B : Set G
g y : G
⊢ y ∈ {x | ∃ x_1 ∈ A ∩ B, g * x_1 = x} ↔ y ∈ {x | ∃ x_1 ∈ A, g * x_1 = x} ∩ {x | ∃ x_1 ∈ B, g * x_1 = x}
Tactic:
simp only [Set.mem_inter, Set.mem_setOf_eq, exists_prop]
State after:
case h
G : Type u_1
inst✝ : Group G
A B : Set G
g y : G
⊢ (∃ x ∈ A ∩ B, g * x = y) ↔ y ∈ {x | ∃ x_1 ∈ A, g * x_1 = x} ∩ {x | ∃ x_1 ∈ B, g * x_1 = x}

State before:
case h
G : Type u_1
inst✝ : Group G
A B : Set G
g y : G
⊢ (∃ x ∈ A ∩ B, g * x = y) ↔ y ∈ {x | ∃ x_1 ∈ A, g * x_1 = x} ∩ {x | ∃ x_1 ∈ B, g * x_1 = x}
Tactic:
constructor
State after:
case h.mp
G : Type u_1
inst✝ : Group G
A B : Set G
g y : G
⊢ (∃ x ∈ A ∩ B, g * x = y) → y ∈ {x | ∃ x_1 ∈ A, g * x_1 = x} ∩ {x | ∃ x_1 ∈ B, g * x_1 = x}

case h.mpr
G : Type u_1
inst✝ : Group G
A B : Set G
g y : G
⊢ y ∈ {x | ∃ x_1 ∈ A, g * x_1 = x} ∩ {x | ∃ x_1 ∈ B, g * x_1 = x} → ∃ x ∈ A ∩ B, g * x = y

State before:
case h.mp
G : Type u_1
inst✝ : Group G
A B : Set G
g y : G
⊢ (∃ x ∈ A ∩ B, g * x = y) → y ∈ {x | ∃ x_1 ∈ A, g * x_1 = x} ∩ {x | ∃ x_1 ∈ B, g * x_1 = x}
Tactic:
rintro ⟨x, ⟨ha, hb⟩, hx⟩
State after:
case h.mp.intro.intro.intro
G : Type u_1
inst✝ : Group G
A B : Set G
g y x : G
hx : g * x = y
ha : x ∈ A
hb : x ∈ B
⊢ y ∈ {x | ∃ x_1 ∈ A, g * x_1 = x} ∩ {x | ∃ x_1 ∈ B, g * x_1 = x}

State before:
case h.mp.intro.intro.intro
G : Type u_1
inst✝ : Group G
A B : Set G
g y x : G
hx : g * x = y
ha : x ∈ A
hb : x ∈ B
⊢ y ∈ {x | ∃ x_1 ∈ A, g * x_1 = x} ∩ {x | ∃ x_1 ∈ B, g * x_1 = x}
Tactic:
exact ⟨⟨x, ha, hx⟩, ⟨x, hb, hx⟩⟩
State after:
no goals

State before:
case h.mpr
G : Type u_1
inst✝ : Group G
A B : Set G
g y : G
⊢ y ∈ {x | ∃ x_1 ∈ A, g * x_1 = x} ∩ {x | ∃ x_1 ∈ B, g * x_1 = x} → ∃ x ∈ A ∩ B, g * x = y
Tactic:
rintro ⟨⟨x, ha, hx⟩, ⟨x', hb, hx'⟩⟩
State after:
case h.mpr.intro.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
A B : Set G
g y x : G
ha : x ∈ A
hx : g * x = y
x' : G
hb : x' ∈ B
hx' : g * x' = y
⊢ ∃ x ∈ A ∩ B, g * x = y

State before:
case h.mpr.intro.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
A B : Set G
g y x : G
ha : x ∈ A
hx : g * x = y
x' : G
hb : x' ∈ B
hx' : g * x' = y
⊢ ∃ x ∈ A ∩ B, g * x = y
Tactic:
obtain rfl : x = x' := by rw [← mul_right_inj g, hx, hx']
State after:
case h.mpr.intro.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
A B : Set G
g y x : G
ha : x ∈ A
hx : g * x = y
hb : x ∈ B
hx' : g * x = y
⊢ ∃ x ∈ A ∩ B, g * x = y

State before:
case h.mpr.intro.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
A B : Set G
g y x : G
ha : x ∈ A
hx : g * x = y
hb : x ∈ B
hx' : g * x = y
⊢ ∃ x ∈ A ∩ B, g * x = y
Tactic:
exact ⟨x, ⟨ha, hb⟩, hx⟩
State after:
no goals

State before:
G : Type u_1
inst✝ : Group G
A B : Set G
g y x : G
ha : x ∈ A
hx : g * x = y
x' : G
hb : x' ∈ B
hx' : g * x' = y
⊢ x = x'
Tactic:
rw [← mul_right_inj g, hx, hx']
State after:
no goals