Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case e'_1.inl
G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
u : ℤˣ
hu : ¬u = 1
x✝ : G
h✝ : u = 1
⊢ toSubgroup A B u = B

pp: case e'_1.inr
G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
u : ℤˣ
hu : ¬u = 1
x✝ : G
h✝ : u = -1
⊢ toSubgroup A B u = B

pp: case e'_2.inl
G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
u : ℤˣ
hu : ¬u = 1
x✝ : G
h✝ : u = 1
⊢ toSubgroup A B (-u) = A

pp: case e'_2.inr
G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
u : ℤˣ
hu : ¬u = 1
x✝ : G
h✝ : u = -1
⊢ toSubgroup A B (-u) = A

pp: case e'_3.inl
G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
u : ℤˣ
hu : ¬u = 1
e_1✝ : ↥(toSubgroup A B u) = ↥B
h✝ : u = 1
⊢ toSubgroup A B u = B

pp: case e'_3.inr
G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
u : ℤˣ
hu : ¬u = 1
e_1✝ : ↥(toSubgroup A B u) = ↥B
h✝ : u = -1
⊢ toSubgroup A B u = B

pp: case e'_4.inl
G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
u : ℤˣ
hu : ¬u = 1
e_2✝ : ↥(toSubgroup A B (-u)) = ↥A
h✝ : u = 1
⊢ toSubgroup A B (-u) = A

pp: case e'_4.inr
G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
u : ℤˣ
hu : ¬u = 1
e_2✝ : ↥(toSubgroup A B (-u)) = ↥A
h✝ : u = -1
⊢ toSubgroup A B (-u) = A

Tactic:
<;>

Goal state after:
case e'_1.inl
G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
u : ℤˣ
hu : ¬u = 1
x✝ : G
h✝ : u = 1
⊢ toSubgroup A B u = B

case e'_1.inr
G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
u : ℤˣ
hu : ¬u = 1
x✝ : G
h✝ : u = -1
⊢ toSubgroup A B u = B

case e'_2.inl
G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
u : ℤˣ
hu : ¬u = 1
x✝ : G
h✝ : u = 1
⊢ toSubgroup A B (-u) = A

case e'_2.inr
G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
u : ℤˣ
hu : ¬u = 1
x✝ : G
h✝ : u = -1
⊢ toSubgroup A B (-u) = A

case e'_3.inl
G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
u : ℤˣ
hu : ¬u = 1
e_1✝ : ↥(toSubgroup A B u) = ↥B
h✝ : u = 1
⊢ toSubgroup A B u = B

case e'_3.inr
G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
u : ℤˣ
hu : ¬u = 1
e_1✝ : ↥(toSubgroup A B u) = ↥B
h✝ : u = -1
⊢ toSubgroup A B u = B

case e'_4.inl
G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
u : ℤˣ
hu : ¬u = 1
e_2✝ : ↥(toSubgroup A B (-u)) = ↥A
h✝ : u = 1
⊢ toSubgroup A B (-u) = A

case e'_4.inr
G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
u : ℤˣ
hu : ¬u = 1
e_2✝ : ↥(toSubgroup A B (-u)) = ↥A
h✝ : u = -1
⊢ toSubgroup A B (-u) = A