-- Mathlib/FieldTheory/Galois/Basic.lean
theorem fixingSubgroup_fixedField [FiniteDimensional F E] : fixingSubgroup (fixedField H) = H

Proof state:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
H : Subgroup (E ≃ₐ[F] E)
inst✝ : FiniteDimensional F E
⊢ (fixedField H).fixingSubgroup = H

Tactic:
have H_le : H ≤ fixingSubgroup (fixedField H) := (le_iff_le _ _).mp le_rfl

Result:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
H : Subgroup (E ≃ₐ[F] E)
inst✝ : FiniteDimensional F E
H_le : H ≤ (fixedField H).fixingSubgroup
⊢ (fixedField H).fixingSubgroup = H

Proof state:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
H : Subgroup (E ≃ₐ[F] E)
inst✝ : FiniteDimensional F E
H_le : H ≤ (fixedField H).fixingSubgroup
this : Fintype.card ↥H = Fintype.card ↥(fixedField H).fixingSubgroup
⊢ (fixedField H).fixingSubgroup = H

Tactic:
exact SetLike.coe_injective (Set.eq_of_inclusion_surjective
  ((Fintype.bijective_iff_injective_and_card (Set.inclusion H_le)).mpr
    ⟨Set.inclusion_injective H_le, this⟩).2).symm

Result:
no goals

Proof state:
case f
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
H : Subgroup (E ≃ₐ[F] E)
inst✝ : FiniteDimensional F E
H_le : H ≤ (fixedField H).fixingSubgroup
⊢ (E ≃ₐ[↥(fixedField H)] E) ≃ ↥(fixedField H).fixingSubgroup

Tactic:
exact (fixingSubgroupEquiv (fixedField H)).toEquiv.symm

Result:
no goals

Proof state:
case f
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
H : Subgroup (E ≃ₐ[F] E)
inst✝ : FiniteDimensional F E
H_le : H ≤ (fixedField H).fixingSubgroup
⊢ ↥H ≃ ↥(fixedField H).fixingSubgroup

Tactic:
refine (FixedPoints.toAlgHomEquiv H E).trans ?_

Result:
case f
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
H : Subgroup (E ≃ₐ[F] E)
inst✝ : FiniteDimensional F E
H_le : H ≤ (fixedField H).fixingSubgroup
⊢ (E →ₐ[↥(FixedPoints.subfield (↥H) E)] E) ≃ ↥(fixedField H).fixingSubgroup

Proof state:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
H : Subgroup (E ≃ₐ[F] E)
inst✝ : FiniteDimensional F E
H_le : H ≤ (fixedField H).fixingSubgroup
⊢ (fixedField H).fixingSubgroup = H

Tactic:
classical
suffices Fintype.card H = Fintype.card (fixingSubgroup (fixedField H)) by
  exact SetLike.coe_injective (Set.eq_of_inclusion_surjective
    ((Fintype.bijective_iff_injective_and_card (Set.inclusion H_le)).mpr
      ⟨Set.inclusion_injective H_le, this⟩).2).symm
apply Fintype.card_congr
refine (FixedPoints.toAlgHomEquiv H E).trans ?_
refine (algEquivEquivAlgHom (fixedField H) E).toEquiv.symm.trans ?_
exact (fixingSubgroupEquiv (fixedField H)).toEquiv.symm

Result:
no goals

Proof state:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
H : Subgroup (E ≃ₐ[F] E)
inst✝ : FiniteDimensional F E
H_le : H ≤ (fixedField H).fixingSubgroup
⊢ (fixedField H).fixingSubgroup = H

Tactic:
suffices Fintype.card H = Fintype.card (fixingSubgroup (fixedField H)) by
  exact SetLike.coe_injective (Set.eq_of_inclusion_surjective
    ((Fintype.bijective_iff_injective_and_card (Set.inclusion H_le)).mpr
      ⟨Set.inclusion_injective H_le, this⟩).2).symm

Result:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
H : Subgroup (E ≃ₐ[F] E)
inst✝ : FiniteDimensional F E
H_le : H ≤ (fixedField H).fixingSubgroup
⊢ Fintype.card ↥H = Fintype.card ↥(fixedField H).fixingSubgroup

Proof state:
case f
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
H : Subgroup (E ≃ₐ[F] E)
inst✝ : FiniteDimensional F E
H_le : H ≤ (fixedField H).fixingSubgroup
⊢ (E →ₐ[↥(FixedPoints.subfield (↥H) E)] E) ≃ ↥(fixedField H).fixingSubgroup

Tactic:
refine (algEquivEquivAlgHom (fixedField H) E).toEquiv.symm.trans ?_

Result:
case f
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
H : Subgroup (E ≃ₐ[F] E)
inst✝ : FiniteDimensional F E
H_le : H ≤ (fixedField H).fixingSubgroup
⊢ (E ≃ₐ[↥(fixedField H)] E) ≃ ↥(fixedField H).fixingSubgroup

Proof state:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
H : Subgroup (E ≃ₐ[F] E)
inst✝ : FiniteDimensional F E
H_le : H ≤ (fixedField H).fixingSubgroup
⊢ Fintype.card ↥H = Fintype.card ↥(fixedField H).fixingSubgroup

Tactic:
apply Fintype.card_congr

Result:
case f
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
H : Subgroup (E ≃ₐ[F] E)
inst✝ : FiniteDimensional F E
H_le : H ≤ (fixedField H).fixingSubgroup
⊢ ↥H ≃ ↥(fixedField H).fixingSubgroup