-- Mathlib/FieldTheory/CardinalEmb.lean
theorem cardinal_eq_two_pow_rank [Algebra.IsSeparable F E]
    (rank_inf : ℵ₀ ≤ Module.rank F E) : #(Field.Emb F E) = 2 ^ Module.rank F E

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
rank_inf : ℵ₀ ≤ Module.rank F E
this : Fact (ℵ₀ ≤ Module.rank F E)
⊢ #(Emb F E) = 2 ^ Module.rank F E

Tactic:
rw [Emb.Cardinal.embEquivPi.cardinal_eq, mk_pi]

Result:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
rank_inf : ℵ₀ ≤ Module.rank F E
this : Fact (ℵ₀ ≤ Module.rank F E)
⊢ (Cardinal.prod fun i => #(Cardinal.factor ↑i)) = 2 ^ Module.rank F E

Proof state:
case a
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
rank_inf : ℵ₀ ≤ Module.rank F E
this : Fact (ℵ₀ ≤ Module.rank F E)
⊢ (Cardinal.prod fun i => #(Cardinal.factor ↑i)) ≤ Cardinal.prod fun x => ℵ₀

Tactic:
exact prod_le_prod _ _ fun i ↦ (Emb.Cardinal.deg_lt_aleph0 _).le

Result:
no goals

Proof state:
case a
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
rank_inf : ℵ₀ ≤ Module.rank F E
this : Fact (ℵ₀ ≤ Module.rank F E)
⊢ (Cardinal.prod fun x => 2) ≤ Cardinal.prod fun i => #(Cardinal.factor ↑i)

Tactic:
exact prod_le_prod _ _ Emb.Cardinal.two_le_deg

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
rank_inf : ℵ₀ ≤ Module.rank F E
this : Fact (ℵ₀ ≤ Module.rank F E)
⊢ (Cardinal.prod fun i => #(Cardinal.factor ↑i)) = 2 ^ Module.rank F E

Tactic:
apply le_antisymm

Result:
case a
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
rank_inf : ℵ₀ ≤ Module.rank F E
this : Fact (ℵ₀ ≤ Module.rank F E)
⊢ (Cardinal.prod fun i => #(Cardinal.factor ↑i)) ≤ 2 ^ Module.rank F E

case a
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
rank_inf : ℵ₀ ≤ Module.rank F E
this : Fact (ℵ₀ ≤ Module.rank F E)
⊢ 2 ^ Module.rank F E ≤ Cardinal.prod fun i => #(Cardinal.factor ↑i)

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
rank_inf : ℵ₀ ≤ Module.rank F E
⊢ #(Emb F E) = 2 ^ Module.rank F E

Tactic:
haveI := Fact.mk rank_inf

Result:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
rank_inf : ℵ₀ ≤ Module.rank F E
this : Fact (ℵ₀ ≤ Module.rank F E)
⊢ #(Emb F E) = 2 ^ Module.rank F E

Proof state:
case a
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
rank_inf : ℵ₀ ≤ Module.rank F E
this : Fact (ℵ₀ ≤ Module.rank F E)
⊢ (Cardinal.prod fun i => #(Cardinal.factor ↑i)) ≤ 2 ^ Module.rank F E

Tactic:
rw [← power_eq_two_power rank_inf (nat_lt_aleph0 2).le rank_inf]

Result:
case a
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
rank_inf : ℵ₀ ≤ Module.rank F E
this : Fact (ℵ₀ ≤ Module.rank F E)
⊢ (Cardinal.prod fun i => #(Cardinal.factor ↑i)) ≤ ℵ₀ ^ Module.rank F E

Proof state:
case a
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
rank_inf : ℵ₀ ≤ Module.rank F E
this : Fact (ℵ₀ ≤ Module.rank F E)
⊢ (Cardinal.prod fun i => #(Cardinal.factor ↑i)) ≤ ℵ₀ ^ Module.rank F E

Tactic:
conv_rhs => rw [← mk_ord_toType (Module.rank F E), ← prod_const']

Result:
case a
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
rank_inf : ℵ₀ ≤ Module.rank F E
this : Fact (ℵ₀ ≤ Module.rank F E)
⊢ (Cardinal.prod fun i => #(Cardinal.factor ↑i)) ≤ Cardinal.prod fun x => ℵ₀

Proof state:
case a
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
rank_inf : ℵ₀ ≤ Module.rank F E
this : Fact (ℵ₀ ≤ Module.rank F E)
⊢ 2 ^ Module.rank F E ≤ Cardinal.prod fun i => #(Cardinal.factor ↑i)

Tactic:
conv_lhs => rw [← mk_ord_toType (Module.rank F E), ← prod_const']

Result:
case a
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
rank_inf : ℵ₀ ≤ Module.rank F E
this : Fact (ℵ₀ ≤ Module.rank F E)
⊢ (Cardinal.prod fun x => 2) ≤ Cardinal.prod fun i => #(Cardinal.factor ↑i)