-- Mathlib/FieldTheory/Galois/Basic.lean
theorem of_card_aut_eq_finrank [FiniteDimensional F E]
    (h : Fintype.card (E ≃ₐ[F] E) = finrank F E) : IsGalois F E

Proof state:
case h
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
h : Fintype.card (E ≃ₐ[F] E) = finrank F E
p : 0 < finrank (↥(fixedField ⊤)) E
⊢ fixedField ⊤ = ⊥

Tactic:
classical
rw [← IntermediateField.finrank_eq_one_iff, ← mul_left_inj' (ne_of_lt p).symm,
  finrank_mul_finrank, ← h, one_mul, IntermediateField.finrank_fixedField_eq_card]
apply Fintype.card_congr
exact
  { toFun := fun g => ⟨g, Subgroup.mem_top g⟩
    invFun := (↑)
    left_inv := fun g => rfl
    right_inv := fun _ => by ext; rfl }

Result:
no goals

Proof state:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
h : Fintype.card (E ≃ₐ[F] E) = finrank F E
⊢ IsGalois F E

Tactic:
apply of_fixedField_eq_bot

Result:
case h
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
h : Fintype.card (E ≃ₐ[F] E) = finrank F E
⊢ fixedField ⊤ = ⊥

Proof state:
case h
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
h : Fintype.card (E ≃ₐ[F] E) = finrank F E
p : 0 < finrank (↥(fixedField ⊤)) E
⊢ Fintype.card (E ≃ₐ[F] E) = Fintype.card ↥⊤

Tactic:
apply Fintype.card_congr

Result:
case h.f
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
h : Fintype.card (E ≃ₐ[F] E) = finrank F E
p : 0 < finrank (↥(fixedField ⊤)) E
⊢ (E ≃ₐ[F] E) ≃ ↥⊤

Proof state:
case h
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
h : Fintype.card (E ≃ₐ[F] E) = finrank F E
p : 0 < finrank (↥(fixedField ⊤)) E
⊢ fixedField ⊤ = ⊥

Tactic:
rw [← IntermediateField.finrank_eq_one_iff, ← mul_left_inj' (ne_of_lt p).symm,
  finrank_mul_finrank, ← h, one_mul, IntermediateField.finrank_fixedField_eq_card]

Result:
case h
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
h : Fintype.card (E ≃ₐ[F] E) = finrank F E
p : 0 < finrank (↥(fixedField ⊤)) E
⊢ Fintype.card (E ≃ₐ[F] E) = Fintype.card ↥⊤

Proof state:
case h.f
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
h : Fintype.card (E ≃ₐ[F] E) = finrank F E
p : 0 < finrank (↥(fixedField ⊤)) E
⊢ (E ≃ₐ[F] E) ≃ ↥⊤

Tactic:
exact
  { toFun := fun g => ⟨g, Subgroup.mem_top g⟩
    invFun := (↑)
    left_inv := fun g => rfl
    right_inv := fun _ => by ext; rfl }

Result:
no goals

Proof state:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
h : Fintype.card (E ≃ₐ[F] E) = finrank F E
p : 0 < finrank (↥(fixedField ⊤)) E
x✝ : ↥⊤
⊢ (fun g => ⟨g, ⋯⟩) ↑x✝ = x✝

Tactic:
ext

Result:
case a.h
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
h : Fintype.card (E ≃ₐ[F] E) = finrank F E
p : 0 < finrank (↥(fixedField ⊤)) E
x✝ : ↥⊤
a✝ : E
⊢ ↑((fun g => ⟨g, ⋯⟩) ↑x✝) a✝ = ↑x✝ a✝

Proof state:
case a.h
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
h : Fintype.card (E ≃ₐ[F] E) = finrank F E
p : 0 < finrank (↥(fixedField ⊤)) E
x✝ : ↥⊤
a✝ : E
⊢ ↑((fun g => ⟨g, ⋯⟩) ↑x✝) a✝ = ↑x✝ a✝

Tactic:
rfl

Result:
no goals

Proof state:
case h
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
h : Fintype.card (E ≃ₐ[F] E) = finrank F E
⊢ fixedField ⊤ = ⊥

Tactic:
have p : 0 < finrank (IntermediateField.fixedField (⊤ : Subgroup (E ≃ₐ[F] E))) E := finrank_pos

Result:
case h
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
h : Fintype.card (E ≃ₐ[F] E) = finrank F E
p : 0 < finrank (↥(fixedField ⊤)) E
⊢ fixedField ⊤ = ⊥