case allEq
G : Type u
α : Type v
β : Type w
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : Normal ↑P
⊢ ∀ (a b : Sylow p G), a = b
G : Type u
α : Type v
β : Type w
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : Normal ↑P
⊢ Subsingleton (Sylow p G)
apply Subsingleton.intro
case allEq
G : Type u
α : Type v
β : Type w
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : Normal ↑P
Q R : Sylow p G
⊢ Q = R
case allEq
G : Type u
α : Type v
β : Type w
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : Normal ↑P
⊢ ∀ (a b : Sylow p G), a = b
intro Q R
case allEq.intro
G : Type u
α : Type v
β : Type w
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : Normal ↑P
Q R : Sylow p G
x : G
h1 : x • P = Q
⊢ Q = R
case allEq
G : Type u
α : Type v
β : Type w
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : Normal ↑P
Q R : Sylow p G
⊢ Q = R
obtain ⟨x, h1⟩ := exists_smul_eq G P Q
case allEq.intro.intro
G : Type u
α : Type v
β : Type w
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : Normal ↑P
Q R : Sylow p G
x✝ : G
h1 : x✝ • P = Q
x : G
h2 : x • P = R
⊢ Q = R
case allEq.intro
G : Type u
α : Type v
β : Type w
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : Normal ↑P
Q R : Sylow p G
x : G
h1 : x • P = Q
⊢ Q = R
obtain ⟨x, h2⟩ := exists_smul_eq G P R
case allEq.intro.intro
G : Type u
α : Type v
β : Type w
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : Normal ↑P
Q R : Sylow p G
x✝ : G
h1 : P = Q
x : G
h2 : P = R
⊢ Q = R
case allEq.intro.intro
G : Type u
α : Type v
β : Type w
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : Normal ↑P
Q R : Sylow p G
x✝ : G
h1 : x✝ • P = Q
x : G
h2 : x • P = R
⊢ Q = R
rw [Sylow.smul_eq_of_normal] at h1 h2
no goals
case allEq.intro.intro
G : Type u
α : Type v
β : Type w
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : Normal ↑P
Q R : Sylow p G
x✝ : G
h1 : P = Q
x : G
h2 : P = R
⊢ Q = R
rw [← h1, ← h2]