case intro
M : Type u
inst✝⁹ : Monoid M
G✝ : Type u
inst✝⁸ : Group G✝
F✝ : Type v
inst✝⁷ : Field F✝
inst✝⁶ : MulSemiringAction M F✝
inst✝⁵ : MulSemiringAction G✝ F✝
m : M
G : Type u
F : Type v
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : Finite G
inst✝¹ : MulSemiringAction G F
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Function.Bijective (MulSemiringAction.toAlgHom { x // x ∈ subfield G F } F)
M : Type u
inst✝⁹ : Monoid M
G✝ : Type u
inst✝⁸ : Group G✝
F✝ : Type v
inst✝⁷ : Field F✝
inst✝⁶ : MulSemiringAction M F✝
inst✝⁵ : MulSemiringAction G✝ F✝
m : M
G : Type u
F : Type v
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : Finite G
inst✝¹ : MulSemiringAction G F
inst✝ : FaithfulSMul G F
⊢ Function.Bijective (MulSemiringAction.toAlgHom { x // x ∈ subfield G F } F)
cases nonempty_fintype G
case intro
M : Type u
inst✝⁹ : Monoid M
G✝ : Type u
inst✝⁸ : Group G✝
F✝ : Type v
inst✝⁷ : Field F✝
inst✝⁶ : MulSemiringAction M F✝
inst✝⁵ : MulSemiringAction G✝ F✝
m : M
G : Type u
F : Type v
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : Finite G
inst✝¹ : MulSemiringAction G F
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Function.Injective (MulSemiringAction.toAlgHom { x // x ∈ subfield G F } F) ∧
    Fintype.card G = Fintype.card (F →ₐ[{ x // x ∈ subfield G F }] F)
case intro
M : Type u
inst✝⁹ : Monoid M
G✝ : Type u
inst✝⁸ : Group G✝
F✝ : Type v
inst✝⁷ : Field F✝
inst✝⁶ : MulSemiringAction M F✝
inst✝⁵ : MulSemiringAction G✝ F✝
m : M
G : Type u
F : Type v
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : Finite G
inst✝¹ : MulSemiringAction G F
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Function.Bijective (MulSemiringAction.toAlgHom { x // x ∈ subfield G F } F)
rw [Fintype.bijective_iff_injective_and_card]
case intro.left
M : Type u
inst✝⁹ : Monoid M
G✝ : Type u
inst✝⁸ : Group G✝
F✝ : Type v
inst✝⁷ : Field F✝
inst✝⁶ : MulSemiringAction M F✝
inst✝⁵ : MulSemiringAction G✝ F✝
m : M
G : Type u
F : Type v
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : Finite G
inst✝¹ : MulSemiringAction G F
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Function.Injective (MulSemiringAction.toAlgHom { x // x ∈ subfield G F } F)

case intro.right
M : Type u
inst✝⁹ : Monoid M
G✝ : Type u
inst✝⁸ : Group G✝
F✝ : Type v
inst✝⁷ : Field F✝
inst✝⁶ : MulSemiringAction M F✝
inst✝⁵ : MulSemiringAction G✝ F✝
m : M
G : Type u
F : Type v
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : Finite G
inst✝¹ : MulSemiringAction G F
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Fintype.card G = Fintype.card (F →ₐ[{ x // x ∈ subfield G F }] F)
case intro
M : Type u
inst✝⁹ : Monoid M
G✝ : Type u
inst✝⁸ : Group G✝
F✝ : Type v
inst✝⁷ : Field F✝
inst✝⁶ : MulSemiringAction M F✝
inst✝⁵ : MulSemiringAction G✝ F✝
m : M
G : Type u
F : Type v
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : Finite G
inst✝¹ : MulSemiringAction G F
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Function.Injective (MulSemiringAction.toAlgHom { x // x ∈ subfield G F } F) ∧
    Fintype.card G = Fintype.card (F →ₐ[{ x // x ∈ subfield G F }] F)
constructor
no goals
case intro.left
M : Type u
inst✝⁹ : Monoid M
G✝ : Type u
inst✝⁸ : Group G✝
F✝ : Type v
inst✝⁷ : Field F✝
inst✝⁶ : MulSemiringAction M F✝
inst✝⁵ : MulSemiringAction G✝ F✝
m : M
G : Type u
F : Type v
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : Finite G
inst✝¹ : MulSemiringAction G F
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Function.Injective (MulSemiringAction.toAlgHom { x // x ∈ subfield G F } F)
exact MulSemiringAction.toAlgHom_injective _ F
case intro.right.a
M : Type u
inst✝⁹ : Monoid M
G✝ : Type u
inst✝⁸ : Group G✝
F✝ : Type v
inst✝⁷ : Field F✝
inst✝⁶ : MulSemiringAction M F✝
inst✝⁵ : MulSemiringAction G✝ F✝
m : M
G : Type u
F : Type v
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : Finite G
inst✝¹ : MulSemiringAction G F
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Fintype.card G ≤ Fintype.card (F →ₐ[{ x // x ∈ subfield G F }] F)

case intro.right.a
M : Type u
inst✝⁹ : Monoid M
G✝ : Type u
inst✝⁸ : Group G✝
F✝ : Type v
inst✝⁷ : Field F✝
inst✝⁶ : MulSemiringAction M F✝
inst✝⁵ : MulSemiringAction G✝ F✝
m : M
G : Type u
F : Type v
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : Finite G
inst✝¹ : MulSemiringAction G F
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Fintype.card (F →ₐ[{ x // x ∈ subfield G F }] F) ≤ Fintype.card G
case intro.right
M : Type u
inst✝⁹ : Monoid M
G✝ : Type u
inst✝⁸ : Group G✝
F✝ : Type v
inst✝⁷ : Field F✝
inst✝⁶ : MulSemiringAction M F✝
inst✝⁵ : MulSemiringAction G✝ F✝
m : M
G : Type u
F : Type v
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : Finite G
inst✝¹ : MulSemiringAction G F
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Fintype.card G = Fintype.card (F →ₐ[{ x // x ∈ subfield G F }] F)
apply le_antisymm
no goals
case intro.right.a
M : Type u
inst✝⁹ : Monoid M
G✝ : Type u
inst✝⁸ : Group G✝
F✝ : Type v
inst✝⁷ : Field F✝
inst✝⁶ : MulSemiringAction M F✝
inst✝⁵ : MulSemiringAction G✝ F✝
m : M
G : Type u
F : Type v
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : Finite G
inst✝¹ : MulSemiringAction G F
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Fintype.card G ≤ Fintype.card (F →ₐ[{ x // x ∈ subfield G F }] F)
exact Fintype.card_le_of_injective _ (MulSemiringAction.toAlgHom_injective _ F)
case intro.right.a
M : Type u
inst✝⁹ : Monoid M
G✝ : Type u
inst✝⁸ : Group G✝
F✝ : Type v
inst✝⁷ : Field F✝
inst✝⁶ : MulSemiringAction M F✝
inst✝⁵ : MulSemiringAction G✝ F✝
m : M
G : Type u
F : Type v
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : Finite G
inst✝¹ : MulSemiringAction G F
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Fintype.card (F →ₐ[{ x // x ∈ subfield G F }] F) ≤ finrank { x // x ∈ subfield G F } F
case intro.right.a
M : Type u
inst✝⁹ : Monoid M
G✝ : Type u
inst✝⁸ : Group G✝
F✝ : Type v
inst✝⁷ : Field F✝
inst✝⁶ : MulSemiringAction M F✝
inst✝⁵ : MulSemiringAction G✝ F✝
m : M
G : Type u
F : Type v
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : Finite G
inst✝¹ : MulSemiringAction G F
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Fintype.card (F →ₐ[{ x // x ∈ subfield G F }] F) ≤ Fintype.card G
rw [← finrank_eq_card G F]
no goals
case intro.right.a
M : Type u
inst✝⁹ : Monoid M
G✝ : Type u
inst✝⁸ : Group G✝
F✝ : Type v
inst✝⁷ : Field F✝
inst✝⁶ : MulSemiringAction M F✝
inst✝⁵ : MulSemiringAction G✝ F✝
m : M
G : Type u
F : Type v
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : Finite G
inst✝¹ : MulSemiringAction G F
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Fintype.card (F →ₐ[{ x // x ∈ subfield G F }] F) ≤ finrank { x // x ∈ subfield G F } F
exact LE.le.trans_eq (finrank_algHom _ F) (finrank_linear_map' _ _ _)