R : Type ?u.1134170
S : Type u_2
T : Type ?u.1134176
inst✝⁵ : CommRing S
K : Type u_1
L : Type u_3
F : Type ?u.1134188
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K S
inst✝ : Algebra K L
pb : PowerBasis K S
h_sep : Separable (minpoly K pb.gen)
h_splits : Splits (algebraMap K L) (minpoly K pb.gen)
s : Finset L := Multiset.toFinset (roots (Polynomial.map (algebraMap K L) (minpoly K pb.gen)))
⊢ Fintype.card (S →ₐ[K] L) = pb.dim
R : Type ?u.1134170
S : Type u_2
T : Type ?u.1134176
inst✝⁵ : CommRing S
K : Type u_1
L : Type u_3
F : Type ?u.1134188
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K S
inst✝ : Algebra K L
pb : PowerBasis K S
h_sep : Separable (minpoly K pb.gen)
h_splits : Splits (algebraMap K L) (minpoly K pb.gen)
⊢ Fintype.card (S →ₐ[K] L) = pb.dim
let s := ((minpoly K pb.gen).map (algebraMap K L)).roots.toFinset
R : Type ?u.1134170
S : Type u_2
T : Type ?u.1134176
inst✝⁵ : CommRing S
K : Type u_1
L : Type u_3
F : Type ?u.1134188
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K S
inst✝ : Algebra K L
pb : PowerBasis K S
h_sep : Separable (minpoly K pb.gen)
h_splits : Splits (algebraMap K L) (minpoly K pb.gen)
s : Finset L := Multiset.toFinset (roots (Polynomial.map (algebraMap K L) (minpoly K pb.gen)))
x✝ : Fintype (S →ₐ[K] L) := PowerBasis.AlgHom.fintype pb
⊢ Fintype.card (S →ₐ[K] L) = pb.dim
R : Type ?u.1134170
S : Type u_2
T : Type ?u.1134176
inst✝⁵ : CommRing S
K : Type u_1
L : Type u_3
F : Type ?u.1134188
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K S
inst✝ : Algebra K L
pb : PowerBasis K S
h_sep : Separable (minpoly K pb.gen)
h_splits : Splits (algebraMap K L) (minpoly K pb.gen)
s : Finset L := Multiset.toFinset (roots (Polynomial.map (algebraMap K L) (minpoly K pb.gen)))
⊢ Fintype.card (S →ₐ[K] L) = pb.dim
let _ := (PowerBasis.AlgHom.fintype pb : Fintype (S →ₐ[K] L))
R : Type ?u.1134170
S : Type u_2
T : Type ?u.1134176
inst✝⁵ : CommRing S
K : Type u_1
L : Type u_3
F : Type ?u.1134188
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K S
inst✝ : Algebra K L
pb : PowerBasis K S
h_sep : Separable (minpoly K pb.gen)
h_splits : Splits (algebraMap K L) (minpoly K pb.gen)
s : Finset L := Multiset.toFinset (roots (Polynomial.map (algebraMap K L) (minpoly K pb.gen)))
x✝ : Fintype (S →ₐ[K] L) := PowerBasis.AlgHom.fintype pb
⊢ Multiset.Nodup (roots (Polynomial.map (algebraMap K L) (minpoly K pb.gen)))
R : Type ?u.1134170
S : Type u_2
T : Type ?u.1134176
inst✝⁵ : CommRing S
K : Type u_1
L : Type u_3
F : Type ?u.1134188
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K S
inst✝ : Algebra K L
pb : PowerBasis K S
h_sep : Separable (minpoly K pb.gen)
h_splits : Splits (algebraMap K L) (minpoly K pb.gen)
s : Finset L := Multiset.toFinset (roots (Polynomial.map (algebraMap K L) (minpoly K pb.gen)))
x✝ : Fintype (S →ₐ[K] L) := PowerBasis.AlgHom.fintype pb
⊢ Fintype.card (S →ₐ[K] L) = pb.dim
rw [Fintype.card_congr pb.liftEquiv', Fintype.card_of_subtype s (fun x => Multiset.mem_toFinset),
  ← pb.natDegree_minpoly, natDegree_eq_card_roots h_splits, Multiset.toFinset_card_of_nodup]
no goals
R : Type ?u.1134170
S : Type u_2
T : Type ?u.1134176
inst✝⁵ : CommRing S
K : Type u_1
L : Type u_3
F : Type ?u.1134188
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K S
inst✝ : Algebra K L
pb : PowerBasis K S
h_sep : Separable (minpoly K pb.gen)
h_splits : Splits (algebraMap K L) (minpoly K pb.gen)
s : Finset L := Multiset.toFinset (roots (Polynomial.map (algebraMap K L) (minpoly K pb.gen)))
x✝ : Fintype (S →ₐ[K] L) := PowerBasis.AlgHom.fintype pb
⊢ Multiset.Nodup (roots (Polynomial.map (algebraMap K L) (minpoly K pb.gen)))
exact nodup_roots ((separable_map (algebraMap K L)).mpr h_sep)