awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
H : Subgroup Gal(E/F)
inst_3 : FiniteDimensional F E
H_le : H ≤ (fixedField H).fixingSubgroup
⊢ Nat.card.{u_2} ↥H = Nat.card.{u_2} ↥(fixedField H).fixingSubgroup
have f : ↥H ≃ ↥(fixedField H).fixingSubgroup
Tactic: apply Nat.card_congr
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
H : Subgroup Gal(E/F)
inst_3 : FiniteDimensional F E
H_le : H ≤ (fixedField H).fixingSubgroup
⊢ ↥H ≃ ↥(fixedField H).fixingSubgroup
have f : (E →ₐ[↥(FixedPoints.subfield (↥H) E)] E) ≃ ↥(fixedField H).fixingSubgroup
Tactic: refine (FixedPoints.toAlgHomEquiv H E).trans ?_
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
H : Subgroup Gal(E/F)
inst_3 : FiniteDimensional F E
H_le : H ≤ (fixedField H).fixingSubgroup
⊢ (E →ₐ[↥(FixedPoints.subfield (↥H) E)] E) ≃ ↥(fixedField H).fixingSubgroup
have f : Gal(E/↥(fixedField H)) ≃ ↥(fixedField H).fixingSubgroup
Tactic: refine (algEquivEquivAlgHom (fixedField H) E).toEquiv.symm.trans ?_
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
H : Subgroup Gal(E/F)
inst_3 : FiniteDimensional F E
H_le : H ≤ (fixedField H).fixingSubgroup
⊢ (fixedField H).fixingSubgroup = H
have suffices : Nat.card.{u_2} ↥H = Nat.card.{u_2} ↥(fixedField H).fixingSubgroup
Tactic: classical
  suffices Nat.card H = Nat.card (fixingSubgroup (fixedField H)) by
    exact SetLike.coe_injective (Set.eq_of_inclusion_surjective
      ((Nat.bijective_iff_injective_and_card (Set.inclusion H_le)).mpr
        ⟨Set.inclusion_injective H_le, this⟩).2).symm
  apply Nat.card_congr
  refine (FixedPoints.toAlgHomEquiv H E).trans ?_
  refine (algEquivEquivAlgHom (fixedField H) E).toEquiv.symm.trans ?_
  exact (fixingSubgroupEquiv (fixedField H)).toEquiv.symm
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
H : Subgroup Gal(E/F)
inst_3 : FiniteDimensional F E
H_le : H ≤ (fixedField H).fixingSubgroup
suffices suffices₁ suffices₂ : Nat.card.{u_2} ↥H = Nat.card.{u_2} ↥(fixedField H).fixingSubgroup
⊢ (fixedField H).fixingSubgroup = H
have f : ↥H ≃ ↥(fixedField H).fixingSubgroup
Tactic: classical
  suffices Nat.card H = Nat.card (fixingSubgroup (fixedField H)) by
    exact SetLike.coe_injective (Set.eq_of_inclusion_surjective
      ((Nat.bijective_iff_injective_and_card (Set.inclusion H_le)).mpr
        ⟨Set.inclusion_injective H_le, this⟩).2).symm
  apply Nat.card_congr
  refine (FixedPoints.toAlgHomEquiv H E).trans ?_
  refine (algEquivEquivAlgHom (fixedField H) E).toEquiv.symm.trans ?_
  exact (fixingSubgroupEquiv (fixedField H)).toEquiv.symm
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
H : Subgroup Gal(E/F)
inst_3 : FiniteDimensional F E
H_le : H ≤ (fixedField H).fixingSubgroup
suffices suffices₁ suffices₂ : Nat.card.{u_2} ↥H = Nat.card.{u_2} ↥(fixedField H).fixingSubgroup
f : ↥H ≃ ↥(fixedField H).fixingSubgroup
⊢ (fixedField H).fixingSubgroup = H
have f₁ : (E →ₐ[↥(FixedPoints.subfield (↥H) E)] E) ≃ ↥(fixedField H).fixingSubgroup
Tactic: classical
  suffices Nat.card H = Nat.card (fixingSubgroup (fixedField H)) by
    exact SetLike.coe_injective (Set.eq_of_inclusion_surjective
      ((Nat.bijective_iff_injective_and_card (Set.inclusion H_le)).mpr
        ⟨Set.inclusion_injective H_le, this⟩).2).symm
  apply Nat.card_congr
  refine (FixedPoints.toAlgHomEquiv H E).trans ?_
  refine (algEquivEquivAlgHom (fixedField H) E).toEquiv.symm.trans ?_
  exact (fixingSubgroupEquiv (fixedField H)).toEquiv.symm
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
H : Subgroup Gal(E/F)
inst_3 : FiniteDimensional F E
H_le : H ≤ (fixedField H).fixingSubgroup
suffices suffices₁ suffices₂ : Nat.card.{u_2} ↥H = Nat.card.{u_2} ↥(fixedField H).fixingSubgroup
f : ↥H ≃ ↥(fixedField H).fixingSubgroup
f₁ : (E →ₐ[↥(FixedPoints.subfield (↥H) E)] E) ≃ ↥(fixedField H).fixingSubgroup
⊢ (fixedField H).fixingSubgroup = H
have f₂ : Gal(E/↥(fixedField H)) ≃ ↥(fixedField H).fixingSubgroup
Tactic: classical
  suffices Nat.card H = Nat.card (fixingSubgroup (fixedField H)) by
    exact SetLike.coe_injective (Set.eq_of_inclusion_surjective
      ((Nat.bijective_iff_injective_and_card (Set.inclusion H_le)).mpr
        ⟨Set.inclusion_injective H_le, this⟩).2).symm
  apply Nat.card_congr
  refine (FixedPoints.toAlgHomEquiv H E).trans ?_
  refine (algEquivEquivAlgHom (fixedField H) E).toEquiv.symm.trans ?_
  exact (fixingSubgroupEquiv (fixedField H)).toEquiv.symm
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
H : Subgroup Gal(E/F)
K : IntermediateField F E
x : ↥K
y : ↥(fixedField K.fixingSubgroup)
ϕ : ↥K.fixingSubgroup
⊢ ϕ • ((↑x : E) * (↑y : E)) = (↑x : E) * (↑y : E)
have rw : ϕ • (↑x : E) * ϕ • (↑y : E) = (↑x : E) * (↑y : E)
Tactic: rw [smul_mul', show ϕ • (x : E) = ↑x from ϕ.2 x, show ϕ • (y : E) = ↑y from y.2 ϕ]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
H : Subgroup Gal(E/F)
K : IntermediateField F E
x : ↥K
y : ↥(fixedField K.fixingSubgroup)
ϕ : ↥K.fixingSubgroup
rw : ϕ • (↑x : E) * ϕ • (↑y : E) = (↑x : E) * (↑y : E)
⊢ ϕ • ((↑x : E) * (↑y : E)) = (↑x : E) * (↑y : E)
have rw₁ : (↑x : E) * ϕ • (↑y : E) = (↑x : E) * (↑y : E)
Tactic: rw [smul_mul', show ϕ • (x : E) = ↑x from ϕ.2 x, show ϕ • (y : E) = ↑y from y.2 ϕ]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
H : Subgroup Gal(E/F)
K : IntermediateField F E
x : ↥K
y : ↥(fixedField K.fixingSubgroup)
ϕ : ↥K.fixingSubgroup
rw : ϕ • (↑x : E) * ϕ • (↑y : E) = (↑x : E) * (↑y : E)
rw₁ : (↑x : E) * ϕ • (↑y : E) = (↑x : E) * (↑y : E)
⊢ ϕ • ((↑x : E) * (↑y : E)) = (↑x : E) * (↑y : E)
have rw₂ : (↑x : E) * (↑y : E) = (↑x : E) * (↑y : E)
Tactic: rw [smul_mul', show ϕ • (x : E) = ↑x from ϕ.2 x, show ϕ • (y : E) = ↑y from y.2 ϕ]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (hypothesis)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : IntermediateField F E
inst_3 : FiniteDimensional F E
h : IsGalois F E
⊢ fixedField K.fixingSubgroup = K
have K_le : K ≤ fixedField K.fixingSubgroup
Tactic: have K_le : K ≤ IntermediateField.fixedField (IntermediateField.fixingSubgroup K) :=
    (IntermediateField.le_iff_le _ _).mpr le_rfl
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : IntermediateField F E
inst_3 : FiniteDimensional F E
h : IsGalois F E
K_le : K ≤ fixedField K.fixingSubgroup
⊢ fixedField K.fixingSubgroup = K
have finrank : finrank (↥K) E = finrank (↥(fixedField K.fixingSubgroup)) E
Tactic: suffices
    finrank K E = finrank (IntermediateField.fixedField (IntermediateField.fixingSubgroup K)) E by
    exact (IntermediateField.eq_of_le_of_finrank_eq' K_le this).symm
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : IntermediateField F E
inst_3 : FiniteDimensional F E
h : IsGalois F E
K_le : K ≤ fixedField K.fixingSubgroup
⊢ finrank (↥K) E = finrank (↥(fixedField K.fixingSubgroup)) E
have rw : finrank (↥K) E = Nat.card.{u_2} Gal(E/↥K)
Tactic: rw [IntermediateField.finrank_fixedField_eq_card,
    Nat.card_congr (IntermediateField.fixingSubgroupEquiv K).toEquiv]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : IntermediateField F E
inst_3 : FiniteDimensional F E
h : IsGalois F E
K_le : K ≤ fixedField K.fixingSubgroup
⊢ finrank (↥K) E = finrank (↥(fixedField K.fixingSubgroup)) E
have rw : finrank (↥K) E = Nat.card.{u_2} ↥K.fixingSubgroup
Tactic: classical
  rw [IntermediateField.finrank_fixedField_eq_card,
    Nat.card_congr (IntermediateField.fixingSubgroupEquiv K).toEquiv]
  exact (card_aut_eq_finrank K E).symm
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : IntermediateField F E
inst_3 : FiniteDimensional F E
h : IsGalois F E
K_le : K ≤ fixedField K.fixingSubgroup
rw : finrank (↥K) E = Nat.card.{u_2} ↥K.fixingSubgroup
⊢ finrank (↥K) E = finrank (↥(fixedField K.fixingSubgroup)) E
have rw₁ : finrank (↥K) E = Nat.card.{u_2} Gal(E/↥K)
Tactic: classical
  rw [IntermediateField.finrank_fixedField_eq_card,
    Nat.card_congr (IntermediateField.fixingSubgroupEquiv K).toEquiv]
  exact (card_aut_eq_finrank K E).symm
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsGalois F E
inst_4 : FiniteDimensional F E
⊢ Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥
have rw : Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField (IntermediateField.fixingSubgroup ⊥)) ⊥
Tactic: rw [← fixingSubgroup_bot, fixedField_fixingSubgroup]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsGalois F E
inst_4 : FiniteDimensional F E
rw : Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField (IntermediateField.fixingSubgroup ⊥)) ⊥
⊢ Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥
have rw₁ : Eq.{u_2 + 1} (α := IntermediateField F E) ⊥ ⊥
Tactic: rw [← fixingSubgroup_bot, fixedField_fixingSubgroup]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsGalois F E
inst_4 : FiniteDimensional F E
x : E
⊢ Membership.mem (γ := IntermediateField F E) ⊥ x ↔ ∀ (f : Gal(E/F)), (f : (a : E) → E) x = x
have rw : (∀ (f : Gal(E/F)), Membership.mem (γ := Subgroup Gal(E/F)) ⊤ f → (f : (a : E) → E) x = x) ↔
  ∀ (f : Gal(E/F)), (f : (a : E) → E) x = x
Tactic: rw [← fixedField_top, mem_fixedField_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : IntermediateField F E
inst_3 : FiniteDimensional F E
inst_4 : IsGalois F E
| finrank (↥K) E
have rw : Nat.card.{u_2} ↥K.fixingSubgroup
Tactic: rw [← fixedField_fixingSubgroup K, IntermediateField.finrank_fixedField_eq_card]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : IntermediateField F E
inst_3 : FiniteDimensional F E
inst_4 : IsGalois F E
⊢ Nat.card.{u_2} ↥K.fixingSubgroup = finrank (↥K) E
have conv_rhs : Nat.card.{u_2} ↥K.fixingSubgroup = finrank (↥K) E
Tactic: conv_rhs => rw [← fixedField_fixingSubgroup K, IntermediateField.finrank_fixedField_eq_card]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : IntermediateField F E
inst_3 : FiniteDimensional F E
inst_4 : IsGalois F E
conv_rhs : Nat.card.{u_2} ↥K.fixingSubgroup = finrank (↥K) E
⊢ Nat.card.{u_2} ↥K.fixingSubgroup = finrank (↥K) E
have conv_rhs₁ : Nat.card.{u_2} ↥K.fixingSubgroup = Nat.card.{u_2} ↥K.fixingSubgroup
Tactic: conv_rhs => rw [← fixedField_fixingSubgroup K, IntermediateField.finrank_fixedField_eq_card]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
H : Subgroup Gal(E/F)
K_1 : IntermediateField F E
inst_3 : FiniteDimensional F E
inst_4 : IsGalois F E
K L : IntermediateField F E
⊢ LE.le (α := (Subgroup Gal(E/F))ᵒᵈ)
      (({
              toFun :=
                (⇑OrderDual.toDual : (a : Subgroup Gal(E/F)) → (Subgroup Gal(E/F))ᵒᵈ) ∘
                  IntermediateField.fixingSubgroup,
              invFun := fixedField ∘ (⇑OrderDual.ofDual : (a : (Subgroup Gal(E/F))ᵒᵈ) → Subgroup Gal(E/F)),
              left_inv := ⋯, right_inv := ⋯ } :
            (a : IntermediateField F E) → (Subgroup Gal(E/F))ᵒᵈ)
          K :
        (Subgroup Gal(E/F))ᵒᵈ)
      (({
              toFun :=
                (⇑OrderDual.toDual : (a : Subgroup Gal(E/F)) → (Subgroup Gal(E/F))ᵒᵈ) ∘
                  IntermediateField.fixingSubgroup,
              invFun := fixedField ∘ (⇑OrderDual.ofDual : (a : (Subgroup Gal(E/F))ᵒᵈ) → Subgroup Gal(E/F)),
              left_inv := ⋯, right_inv := ⋯ } :
            (a : IntermediateField F E) → (Subgroup Gal(E/F))ᵒᵈ)
          L :
        (Subgroup Gal(E/F))ᵒᵈ) ↔
    K ≤ L
have rw : LE.le (α := (Subgroup Gal(E/F))ᵒᵈ)
    (({
            toFun :=
              (⇑OrderDual.toDual : (a : Subgroup Gal(E/F)) → (Subgroup Gal(E/F))ᵒᵈ) ∘ IntermediateField.fixingSubgroup,
            invFun := fixedField ∘ (⇑OrderDual.ofDual : (a : (Subgroup Gal(E/F))ᵒᵈ) → Subgroup Gal(E/F)), left_inv := sorry,
            right_inv := sorry } :
          (a : IntermediateField F E) → (Subgroup Gal(E/F))ᵒᵈ)
        K :
      (Subgroup Gal(E/F))ᵒᵈ)
    (({
            toFun :=
              (⇑OrderDual.toDual : (a : Subgroup Gal(E/F)) → (Subgroup Gal(E/F))ᵒᵈ) ∘ IntermediateField.fixingSubgroup,
            invFun := fixedField ∘ (⇑OrderDual.ofDual : (a : (Subgroup Gal(E/F))ᵒᵈ) → Subgroup Gal(E/F)), left_inv := sorry,
            right_inv := sorry } :
          (a : IntermediateField F E) → (Subgroup Gal(E/F))ᵒᵈ)
        L :
      (Subgroup Gal(E/F))ᵒᵈ) ↔
  L.fixingSubgroup ≤ K.fixingSubgroup
Tactic: rw [← fixedField_fixingSubgroup L, IntermediateField.le_iff_le, fixedField_fixingSubgroup L]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E_1 : Type u_2
inst_1 : Field E_1
inst_2 : Algebra F E_1
H_1 : Subgroup Gal(E_1/F)
K_1 : IntermediateField F E_1
K : Type u_3
L : Type u_4
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra K L
E : IntermediateField K L
inst_6 : IsGalois K L
H : Subgroup Gal(L/K)
hn : H.Normal
⊢ Normal.{u_3, u_4} K ↥(fixedField H)
have apply : ∀ (σ : Gal(L/K)), map (↑σ : L →ₐ[K] L) (fixedField H) ≤ fixedField H
Tactic: apply normal_iff_forall_map_le'.mpr
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E : IntermediateField K L
σ : Gal(L/K)
⊢ (map (↑σ : L →ₐ[K] L) E).fixingSubgroup =
    HSMul.hSMul (α := MulAut Gal(L/K)) ((MulAut.conj : (a : Gal(L/K)) → MulAut Gal(L/K)) σ : MulAut Gal(L/K))
      E.fixingSubgroup
have h : ∀ (τ : Gal(L/K)),
  τ ∈ (map (↑σ : L →ₐ[K] L) E).fixingSubgroup ↔
    τ ∈
      HSMul.hSMul (α := MulAut Gal(L/K)) ((MulAut.conj : (a : Gal(L/K)) → MulAut Gal(L/K)) σ : MulAut Gal(L/K))
        E.fixingSubgroup
Tactic: ext τ
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E : IntermediateField K L
σ τ : Gal(L/K)
⊢ τ ∈ (map (↑σ : L →ₐ[K] L) E).fixingSubgroup ↔
    τ ∈
      HSMul.hSMul (α := MulAut Gal(L/K)) ((MulAut.conj : (a : Gal(L/K)) → MulAut Gal(L/K)) σ : MulAut Gal(L/K))
        E.fixingSubgroup
have h : (∀ a ∈ E, (σ.symm : (a : L) → L) ((τ : (a : L) → L) ((σ : (a : L) → L) a : L) : L) = a) ↔
  ∀ y ∈ E,
    (HSMul.hSMul (α := MulAut Gal(L/K)) (((MulAut.conj : (a : Gal(L/K)) → MulAut Gal(L/K)) σ)⁻¹ : MulAut Gal(L/K)) τ :
          (a : L) → L)
        y =
      y
Tactic: simp only [coe_map, AlgEquiv.coe_algHom, Set.mem_image, SetLike.mem_coe, AlgEquiv.smul_def,
    forall_exists_index, and_imp, forall_apply_eq_imp_iff₂,
    Subgroup.mem_pointwise_smul_iff_inv_smul_mem, ← symm_apply_eq,
    IntermediateField.fixingSubgroup, mem_fixingSubgroup_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E_1 : Type u_2
inst_1 : Field E_1
inst_2 : Algebra F E_1
H : Subgroup Gal(E_1/F)
K_1 : IntermediateField F E_1
K : Type u_3
L : Type u_4
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra K L
E : IntermediateField K L
inst_6 : IsGalois K L
inst_7 : IsGalois.{u_3, u_4} K ↥E
⊢ E.fixingSubgroup.Normal
have apply : ∀ (σ : Gal(L/K)),
  HSMul.hSMul (α := MulAut Gal(L/K)) ((MulAut.conj : (a : Gal(L/K)) → MulAut Gal(L/K)) σ : MulAut Gal(L/K))
      E.fixingSubgroup =
    E.fixingSubgroup
Tactic: apply Subgroup.Normal.of_conjugate_fixed (fun σ ↦ ?_)
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E_1 : Type u_2
inst_1 : Field E_1
inst_2 : Algebra F E_1
H : Subgroup Gal(E_1/F)
K_1 : IntermediateField F E_1
K : Type u_3
L : Type u_4
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra K L
E : IntermediateField K L
inst_6 : IsGalois K L
inst_7 : IsGalois.{u_3, u_4} K ↥E
σ : Gal(L/K)
⊢ HSMul.hSMul (α := MulAut Gal(L/K)) ((MulAut.conj : (a : Gal(L/K)) → MulAut Gal(L/K)) σ : MulAut Gal(L/K))
      E.fixingSubgroup =
    E.fixingSubgroup
have rw : (map (↑σ : L →ₐ[K] L) E).fixingSubgroup = E.fixingSubgroup
Tactic: rw [← map_fixingSubgroup, normal_iff_forall_map_eq'.mp inferInstance σ]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E_1 : Type u_2
inst_1 : Field E_1
inst_2 : Algebra F E_1
H : Subgroup Gal(E_1/F)
K_1 : IntermediateField F E_1
K : Type u_3
L : Type u_4
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra K L
E : IntermediateField K L
inst_6 : IsGalois K L
inst_7 : IsGalois.{u_3, u_4} K ↥E
σ : Gal(L/K)
rw : (map (↑σ : L →ₐ[K] L) E).fixingSubgroup = E.fixingSubgroup
⊢ HSMul.hSMul (α := MulAut Gal(L/K)) ((MulAut.conj : (a : Gal(L/K)) → MulAut Gal(L/K)) σ : MulAut Gal(L/K))
      E.fixingSubgroup =
    E.fixingSubgroup
have rw₁ : E.fixingSubgroup = E.fixingSubgroup
Tactic: rw [← map_fixingSubgroup, normal_iff_forall_map_eq'.mp inferInstance σ]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
h : Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥
⊢ IsGalois F E
have rw : IsGalois (↥(fixedField ⊤)) E
Tactic: rw [← isGalois_iff_isGalois_bot, ← h]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
h : Nat.card.{u_2} Gal(E/F) = finrank F E
⊢ IsGalois F E
have h₁ : Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥
Tactic: apply of_fixedField_eq_bot
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (hypothesis)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
h : Nat.card.{u_2} Gal(E/F) = finrank F E
⊢ Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥
have p : 0 < finrank (↥(fixedField ⊤)) E
Tactic: have p : 0 < finrank (IntermediateField.fixedField (⊤ : Subgroup Gal(E/F))) E := finrank_pos
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
h : Nat.card.{u_2} Gal(E/F) = finrank F E
p : 0 < finrank (↥(fixedField ⊤)) E
⊢ Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥
have h₁ : Nat.card.{u_2} Gal(E/F) = Nat.card.{u_2} ↥⊤
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]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
h : Nat.card.{u_2} Gal(E/F) = finrank F E
p : 0 < finrank (↥(fixedField ⊤)) E
⊢ Nat.card.{u_2} Gal(E/F) = Nat.card.{u_2} ↥⊤
have h₁ : Gal(E/F) ≃ ↥⊤
Tactic: apply Nat.card_congr
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
h : Nat.card.{u_2} Gal(E/F) = finrank F E
p : 0 < finrank (↥(fixedField ⊤)) E
⊢ Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥
have h₁ : finrank.{u_1, u_2} F ↥(fixedField ⊤) = 1
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 Nat.card_congr
  exact { toFun := fun g => ⟨g, Subgroup.mem_top g⟩, invFun := (↑) }
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
h : Nat.card.{u_2} Gal(E/F) = finrank F E
p : 0 < finrank (↥(fixedField ⊤)) E
h₁ : finrank.{u_1, u_2} F ↥(fixedField ⊤) = 1
⊢ Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥
have h₂ : finrank.{u_1, u_2} F ↥(fixedField ⊤) * finrank (↥(fixedField ⊤)) E = 1 * finrank (↥(fixedField ⊤)) E
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 Nat.card_congr
  exact { toFun := fun g => ⟨g, Subgroup.mem_top g⟩, invFun := (↑) }
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
h : Nat.card.{u_2} Gal(E/F) = finrank F E
p : 0 < finrank (↥(fixedField ⊤)) E
h₁ : finrank.{u_1, u_2} F ↥(fixedField ⊤) = 1
h₂ : finrank.{u_1, u_2} F ↥(fixedField ⊤) * finrank (↥(fixedField ⊤)) E = 1 * finrank (↥(fixedField ⊤)) E
⊢ Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥
have h₃ : finrank F E = 1 * finrank (↥(fixedField ⊤)) E
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 Nat.card_congr
  exact { toFun := fun g => ⟨g, Subgroup.mem_top g⟩, invFun := (↑) }
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
h : Nat.card.{u_2} Gal(E/F) = finrank F E
p : 0 < finrank (↥(fixedField ⊤)) E
h₁ : finrank.{u_1, u_2} F ↥(fixedField ⊤) = 1
h₂ : finrank.{u_1, u_2} F ↥(fixedField ⊤) * finrank (↥(fixedField ⊤)) E = 1 * finrank (↥(fixedField ⊤)) E
h₃ : finrank F E = 1 * finrank (↥(fixedField ⊤)) E
⊢ Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥
have h₄ : Nat.card.{u_2} Gal(E/F) = 1 * finrank (↥(fixedField ⊤)) E
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 Nat.card_congr
  exact { toFun := fun g => ⟨g, Subgroup.mem_top g⟩, invFun := (↑) }
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
h : Nat.card.{u_2} Gal(E/F) = finrank F E
p : 0 < finrank (↥(fixedField ⊤)) E
h₁ : finrank.{u_1, u_2} F ↥(fixedField ⊤) = 1
h₂ : finrank.{u_1, u_2} F ↥(fixedField ⊤) * finrank (↥(fixedField ⊤)) E = 1 * finrank (↥(fixedField ⊤)) E
h₃ : finrank F E = 1 * finrank (↥(fixedField ⊤)) E
h₄ : Nat.card.{u_2} Gal(E/F) = 1 * finrank (↥(fixedField ⊤)) E
⊢ Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥
have h₅ : Nat.card.{u_2} Gal(E/F) = finrank (↥(fixedField ⊤)) E
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 Nat.card_congr
  exact { toFun := fun g => ⟨g, Subgroup.mem_top g⟩, invFun := (↑) }