case mk
p : ℕ
G : Type u_1
inst✝ : Group G
Q : Sylow p G
toSubgroup✝ : Subgroup G
isPGroup'✝ : IsPGroup p { x // x ∈ toSubgroup✝ }
is_maximal'✝ : ∀ {Q : Subgroup G}, IsPGroup p { x // x ∈ Q } → toSubgroup✝ ≤ Q → Q = toSubgroup✝
h : ↑{ toSubgroup := toSubgroup✝, isPGroup' := isPGroup'✝, is_maximal' := is_maximal'✝ } = ↑Q
⊢ { toSubgroup := toSubgroup✝, isPGroup' := isPGroup'✝, is_maximal' := is_maximal'✝ } = Q
p : ℕ
G : Type u_1
inst✝ : Group G
P Q : Sylow p G
h : ↑P = ↑Q
⊢ P = Q
cases P
case mk.mk
p : ℕ
G : Type u_1
inst✝ : Group G
toSubgroup✝¹ : Subgroup G
isPGroup'✝¹ : IsPGroup p { x // x ∈ toSubgroup✝¹ }
is_maximal'✝¹ : ∀ {Q : Subgroup G}, IsPGroup p { x // x ∈ Q } → toSubgroup✝¹ ≤ Q → Q = toSubgroup✝¹
toSubgroup✝ : Subgroup G
isPGroup'✝ : IsPGroup p { x // x ∈ toSubgroup✝ }
is_maximal'✝ : ∀ {Q : Subgroup G}, IsPGroup p { x // x ∈ Q } → toSubgroup✝ ≤ Q → Q = toSubgroup✝
h :
  ↑{ toSubgroup := toSubgroup✝¹, isPGroup' := isPGroup'✝¹, is_maximal' := is_maximal'✝¹ } =
    ↑{ toSubgroup := toSubgroup✝, isPGroup' := isPGroup'✝, is_maximal' := is_maximal'✝ }
⊢ { toSubgroup := toSubgroup✝¹, isPGroup' := isPGroup'✝¹, is_maximal' := is_maximal'✝¹ } =
    { toSubgroup := toSubgroup✝, isPGroup' := isPGroup'✝, is_maximal' := is_maximal'✝ }
case mk
p : ℕ
G : Type u_1
inst✝ : Group G
Q : Sylow p G
toSubgroup✝ : Subgroup G
isPGroup'✝ : IsPGroup p { x // x ∈ toSubgroup✝ }
is_maximal'✝ : ∀ {Q : Subgroup G}, IsPGroup p { x // x ∈ Q } → toSubgroup✝ ≤ Q → Q = toSubgroup✝
h : ↑{ toSubgroup := toSubgroup✝, isPGroup' := isPGroup'✝, is_maximal' := is_maximal'✝ } = ↑Q
⊢ { toSubgroup := toSubgroup✝, isPGroup' := isPGroup'✝, is_maximal' := is_maximal'✝ } = Q
cases Q
no goals
case mk.mk
p : ℕ
G : Type u_1
inst✝ : Group G
toSubgroup✝¹ : Subgroup G
isPGroup'✝¹ : IsPGroup p { x // x ∈ toSubgroup✝¹ }
is_maximal'✝¹ : ∀ {Q : Subgroup G}, IsPGroup p { x // x ∈ Q } → toSubgroup✝¹ ≤ Q → Q = toSubgroup✝¹
toSubgroup✝ : Subgroup G
isPGroup'✝ : IsPGroup p { x // x ∈ toSubgroup✝ }
is_maximal'✝ : ∀ {Q : Subgroup G}, IsPGroup p { x // x ∈ Q } → toSubgroup✝ ≤ Q → Q = toSubgroup✝
h :
  ↑{ toSubgroup := toSubgroup✝¹, isPGroup' := isPGroup'✝¹, is_maximal' := is_maximal'✝¹ } =
    ↑{ toSubgroup := toSubgroup✝, isPGroup' := isPGroup'✝, is_maximal' := is_maximal'✝ }
⊢ { toSubgroup := toSubgroup✝¹, isPGroup' := isPGroup'✝¹, is_maximal' := is_maximal'✝¹ } =
    { toSubgroup := toSubgroup✝, isPGroup' := isPGroup'✝, is_maximal' := is_maximal'✝ }
congr