-- Mathlib/FieldTheory/Fixed.lean
theorem toAlgHom_bijective [Finite G] [FaithfulSMul G F] :
    Function.Bijective (MulSemiringAction.toAlgHom _ _ : G → F →ₐ[subfield G F] F)

Proof state:
case intro.right.a
G : Type u_1
F : Type u_2
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : MulSemiringAction G F
inst✝¹ : Finite G
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Fintype.card (F →ₐ[↥(subfield G F)] F) ≤ finrank (↥(subfield G F)) F

Tactic:
exact LE.le.trans_eq (finrank_algHom _ F) (finrank_linearMap_self _ _ _)

Result:
no goals

Proof state:
case intro
G : Type u_1
F : Type u_2
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : MulSemiringAction G F
inst✝¹ : Finite G
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Function.Bijective (MulSemiringAction.toAlgHom (↥(subfield G F)) F)

Tactic:
rw [Fintype.bijective_iff_injective_and_card]

Result:
case intro
G : Type u_1
F : Type u_2
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : MulSemiringAction G F
inst✝¹ : Finite G
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Function.Injective (MulSemiringAction.toAlgHom (↥(subfield G F)) F) ∧
    Fintype.card G = Fintype.card (F →ₐ[↥(subfield G F)] F)

Proof state:
G : Type u_1
F : Type u_2
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : MulSemiringAction G F
inst✝¹ : Finite G
inst✝ : FaithfulSMul G F
⊢ Function.Bijective (MulSemiringAction.toAlgHom (↥(subfield G F)) F)

Tactic:
cases nonempty_fintype G

Result:
case intro
G : Type u_1
F : Type u_2
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : MulSemiringAction G F
inst✝¹ : Finite G
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Function.Bijective (MulSemiringAction.toAlgHom (↥(subfield G F)) F)

Proof state:
case intro.right.a
G : Type u_1
F : Type u_2
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : MulSemiringAction G F
inst✝¹ : Finite G
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Fintype.card (F →ₐ[↥(subfield G F)] F) ≤ Fintype.card G

Tactic:
rw [← finrank_eq_card G F]

Result:
case intro.right.a
G : Type u_1
F : Type u_2
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : MulSemiringAction G F
inst✝¹ : Finite G
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Fintype.card (F →ₐ[↥(subfield G F)] F) ≤ finrank (↥(subfield G F)) F

Proof state:
case intro.right.a
G : Type u_1
F : Type u_2
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : MulSemiringAction G F
inst✝¹ : Finite G
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Fintype.card G ≤ Fintype.card (F →ₐ[↥(subfield G F)] F)

Tactic:
exact Fintype.card_le_of_injective _ (MulSemiringAction.toAlgHom_injective _ F)

Result:
no goals

Proof state:
case intro
G : Type u_1
F : Type u_2
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : MulSemiringAction G F
inst✝¹ : Finite G
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Function.Injective (MulSemiringAction.toAlgHom (↥(subfield G F)) F) ∧
    Fintype.card G = Fintype.card (F →ₐ[↥(subfield G F)] F)

Tactic:
constructor

Result:
case intro.left
G : Type u_1
F : Type u_2
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : MulSemiringAction G F
inst✝¹ : Finite G
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Function.Injective (MulSemiringAction.toAlgHom (↥(subfield G F)) F)

case intro.right
G : Type u_1
F : Type u_2
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : MulSemiringAction G F
inst✝¹ : Finite G
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Fintype.card G = Fintype.card (F →ₐ[↥(subfield G F)] F)

Proof state:
case intro.right
G : Type u_1
F : Type u_2
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : MulSemiringAction G F
inst✝¹ : Finite G
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Fintype.card G = Fintype.card (F →ₐ[↥(subfield G F)] F)

Tactic:
apply le_antisymm

Result:
case intro.right.a
G : Type u_1
F : Type u_2
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : MulSemiringAction G F
inst✝¹ : Finite G
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Fintype.card G ≤ Fintype.card (F →ₐ[↥(subfield G F)] F)

case intro.right.a
G : Type u_1
F : Type u_2
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : MulSemiringAction G F
inst✝¹ : Finite G
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Fintype.card (F →ₐ[↥(subfield G F)] F) ≤ Fintype.card G

Proof state:
case intro.left
G : Type u_1
F : Type u_2
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : MulSemiringAction G F
inst✝¹ : Finite G
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Function.Injective (MulSemiringAction.toAlgHom (↥(subfield G F)) F)

Tactic:
exact MulSemiringAction.toAlgHom_injective _ F

Result:
no goals