awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
rw : IsOpen (↑(IntermediateField.fixingSubgroup ⊤) : Set Gal(L/K))
⊢ IsOpen (↑⊥ : Set Gal(L/K))

Tactic:
rw [← IntermediateField.fixingSubgroup_top]

Premises used: IntermediateField.fixingSubgroup_top
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
⊢ IsOpen (↑(IntermediateField.fixingSubgroup ⊤) : Set Gal(L/K))

Tactic:
IntermediateField.fixingSubgroup_isOpen ⊤

Premises used: IntermediateField.fixingSubgroup_isOpen, Top.top
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
⊢ IsOpen (↑(IntermediateField.fixingSubgroup ⊤) : Set Gal(L/K))

Tactic:
exact IntermediateField.fixingSubgroup_isOpen ⊤

Premises used: IntermediateField.fixingSubgroup_isOpen, Top.top
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsIntegral K L
x : L
E : IntermediateField K L := K⟮x⟯
⊢ FiniteDimensional.{u_1, u_2} K ↥E

Tactic:
have hL : FiniteDimensional K E := adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral x)
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsIntegral K L
x : L
E : IntermediateField K L := K⟮x⟯
hL : FiniteDimensional.{u_1, u_2} K ↥E
⊢ IsOpen (↑E.fixingSubgroup : Set Gal(L/K))

Tactic:
fixingSubgroup_isOpen E

Premises used: IntermediateField.fixingSubgroup_isOpen
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsIntegral K L
x : L
E : IntermediateField K L := K⟮x⟯
hL : FiniteDimensional.{u_1, u_2} K ↥E
h : MulAction.stabilizer Gal(L/K) x = E.fixingSubgroup
⊢ IsOpen (↑(MulAction.stabilizer Gal(L/K) x) : Set Gal(L/K))

Tactic:
convert! fixingSubgroup_isOpen E
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsIntegral K L
x : L
E : IntermediateField K L := K⟮x⟯
hL : FiniteDimensional.{u_1, u_2} K ↥E
h : ∀ (g : Gal(L/K)), Membership.mem (γ := Subgroup Gal(L/K)) (MulAction.stabilizer Gal(L/K) x) g ↔ g ∈ E.fixingSubgroup
⊢ MulAction.stabilizer Gal(L/K) x = E.fixingSubgroup

Tactic:
ext g
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsIntegral K L
x : L
E : IntermediateField K L := K⟮x⟯
hL : FiniteDimensional.{u_1, u_2} K ↥E
g : Gal(L/K)
⊢ Membership.mem (γ := Subgroup Gal(L/K)) (MulAction.stabilizer Gal(L/K) x) g ↔ g ∈ E.fixingSubgroup

Tactic:
simpa using (forall_mem_adjoin_smul_eq_self_iff K (S := {x}) g).symm
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsIntegral K L
x : L
open open₁ open₂ : IsOpen (↑(MulAction.stabilizer Gal(L/K) x) : Set Gal(L/K))
open₃ :
  let E : IntermediateField K L := K⟮x⟯;
  ∀ (hL : FiniteDimensional.{u_1, u_2} K ↥E), IsOpen (↑(MulAction.stabilizer Gal(L/K) x) : Set Gal(L/K))
h :
  let E : IntermediateField K L := K⟮x⟯;
  ∀ (hL : FiniteDimensional.{u_1, u_2} K ↥E), MulAction.stabilizer Gal(L/K) x = E.fixingSubgroup
h₁ :
  let E : IntermediateField K L := K⟮x⟯;
  ∀ (hL : FiniteDimensional.{u_1, u_2} K ↥E) (g : Gal(L/K)),
    Membership.mem (γ := Subgroup Gal(L/K)) (MulAction.stabilizer Gal(L/K) x) g ↔ g ∈ E.fixingSubgroup
⊢ IsOpen (↑(MulAction.stabilizer Gal(L/K) x) : Set Gal(L/K))

Tactic:
open IntermediateField in
  let E := adjoin K {x}
  have hL : FiniteDimensional K E := adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral x)
  convert! fixingSubgroup_isOpen E
  ext g
  simpa using (forall_mem_adjoin_smul_eq_self_iff K (S := {x}) g).symm

Premises used: IntermediateField
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
k : Type u_1
E : Type u_2
K : Type u_3
inst : Field k
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra k E
inst_4 : Algebra k K
inst_5 : Algebra E K
inst_6 : IsScalarTower k E K
L : IntermediateField k E
inst_7 : Normal k E
h :
  ∀ (f : Gal(K/k)),
    Membership.mem (γ := Subgroup Gal(K/k)) (fixingSubgroup (map (IsScalarTower.toAlgHom k E K) L)) f ↔
      Membership.mem (γ := Subgroup Gal(K/k)) (Subgroup.comap (AlgEquiv.restrictNormalHom E) L.fixingSubgroup) f
⊢ Eq (α := Subgroup Gal(K/k)) (fixingSubgroup (map (IsScalarTower.toAlgHom k E K) L))
    (Subgroup.comap (AlgEquiv.restrictNormalHom E) L.fixingSubgroup)

Tactic:
ext f
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
k : Type u_1
E : Type u_2
K : Type u_3
inst : Field k
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra k E
inst_4 : Algebra k K
inst_5 : Algebra E K
inst_6 : IsScalarTower k E K
L : IntermediateField k E
inst_7 : Normal k E
f : Gal(K/k)
h :
  (∀ (x : K),
      Membership.mem (γ := IntermediateField k K) (map (IsScalarTower.toAlgHom k E K) L) x → (f : (a : K) → K) x = x) ↔
    ∀ x ∈ L, (((AlgEquiv.restrictNormalHom E : (a : Gal(K/k)) → Gal(E/k)) f : Gal(E/k)) : (a : E) → E) x = x
⊢ Membership.mem (γ := Subgroup Gal(K/k)) (fixingSubgroup (map (IsScalarTower.toAlgHom k E K) L)) f ↔
    Membership.mem (γ := Subgroup Gal(K/k)) (Subgroup.comap (AlgEquiv.restrictNormalHom E) L.fixingSubgroup) f

Tactic:
simp only [Subgroup.mem_comap, mem_fixingSubgroup_iff]

Premises used: Subgroup.mem_comap, IntermediateField.mem_fixingSubgroup_iff
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
k : Type u_1
E : Type u_2
K : Type u_3
inst : Field k
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra k E
inst_4 : Algebra k K
inst_5 : Algebra E K
inst_6 : IsScalarTower k E K
L : IntermediateField k E
inst_7 : Normal k E
f : Gal(K/k)
h :
  (∀ (x : K),
      Membership.mem (γ := IntermediateField k K) (map (IsScalarTower.toAlgHom k E K) L) x → (f : (a : K) → K) x = x) →
    ∀ x ∈ L, (((AlgEquiv.restrictNormalHom E : (a : Gal(K/k)) → Gal(E/k)) f : Gal(E/k)) : (a : E) → E) x = x
h₁ :
  (∀ x ∈ L, (((AlgEquiv.restrictNormalHom E : (a : Gal(K/k)) → Gal(E/k)) f : Gal(E/k)) : (a : E) → E) x = x) →
    ∀ (x : K),
      Membership.mem (γ := IntermediateField k K) (map (IsScalarTower.toAlgHom k E K) L) x → (f : (a : K) → K) x = x
⊢ (∀ (x : K),
      Membership.mem (γ := IntermediateField k K) (map (IsScalarTower.toAlgHom k E K) L) x → (f : (a : K) → K) x = x) ↔
    ∀ x ∈ L, (((AlgEquiv.restrictNormalHom E : (a : Gal(K/k)) → Gal(E/k)) f : Gal(E/k)) : (a : E) → E) x = x

Tactic:
constructor
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
k : Type u_1
E : Type u_2
K : Type u_3
inst : Field k
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra k E
inst_4 : Algebra k K
inst_5 : Algebra E K
inst_6 : IsScalarTower k E K
L : IntermediateField k E
inst_7 : Normal k E
f : Gal(K/k)
h :
  ∀ (x : K),
    Membership.mem (γ := IntermediateField k K) (map (IsScalarTower.toAlgHom k E K) L) x → (f : (a : K) → K) x = x
x : E
hx : x ∈ L
h₁ : (f.restrictNormal E : (a : E) → E) x = x
⊢ (((AlgEquiv.restrictNormalHom E : (a : Gal(K/k)) → Gal(E/k)) f : Gal(E/k)) : (a : E) → E) x = x

Tactic:
change f.restrictNormal E x = x

Premises used: AlgEquiv.restrictNormal, DFunLike.coe
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
k : Type u_1
E : Type u_2
K : Type u_3
inst : Field k
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra k E
inst_4 : Algebra k K
inst_5 : Algebra E K
inst_6 : IsScalarTower k E K
L : IntermediateField k E
inst_7 : Normal k E
f : Gal(K/k)
h :
  ∀ (x : K),
    Membership.mem (γ := IntermediateField k K) (map (IsScalarTower.toAlgHom k E K) L) x → (f : (a : K) → K) x = x
x : E
hx : x ∈ L
⊢ Function.Injective.{u_2 + 1, u_3 + 1} (α := E) (β := K) (⇑(algebraMap E K : E →+* K) : (a : E) → K)

Tactic:
(algebraMap E K).injective

Premises used: Algebra.algebraMap, RingHom.injective
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
k : Type u_1
E : Type u_2
K : Type u_3
inst : Field k
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra k E
inst_4 : Algebra k K
inst_5 : Algebra E K
inst_6 : IsScalarTower k E K
L : IntermediateField k E
inst_7 : Normal k E
f : Gal(K/k)
h :
  ∀ (x : K),
    Membership.mem (γ := IntermediateField k K) (map (IsScalarTower.toAlgHom k E K) L) x → (f : (a : K) → K) x = x
x : E
hx : x ∈ L
h₁ :
  Eq.{u_3 + 1} (α := K) (((algebraMap E K : E →+* K) : (a : E) → K) ((f.restrictNormal E : (a : E) → E) x : E) : K)
    (((algebraMap E K : E →+* K) : (a : E) → K) x : K)
⊢ (f.restrictNormal E : (a : E) → E) x = x

Tactic:
apply_fun _ using (algebraMap E K).injective

Premises used: Algebra.algebraMap, RingHom.injective
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
k : Type u_1
E : Type u_2
K : Type u_3
inst : Field k
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra k E
inst_4 : Algebra k K
inst_5 : Algebra E K
inst_6 : IsScalarTower k E K
L : IntermediateField k E
inst_7 : Normal k E
f : Gal(K/k)
h :
  ∀ (x : K),
    Membership.mem (γ := IntermediateField k K) (map (IsScalarTower.toAlgHom k E K) L) x → (f : (a : K) → K) x = x
x : E
hx : x ∈ L
h₁ :
  Eq (α := K) ((f : (a : K) → K) ((algebraMap E K : (a : E) → K) x : K) : K)
    (((algebraMap E K : E →+* K) : (a : E) → K) x : K)
⊢ Eq.{u_3 + 1} (α := K) (((algebraMap E K : E →+* K) : (a : E) → K) ((f.restrictNormal E : (a : E) → E) x : E) : K)
    (((algebraMap E K : E →+* K) : (a : E) → K) x : K)

Tactic:
rw [AlgEquiv.restrictNormal_commutes]

Premises used: AlgEquiv.restrictNormal_commutes
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
k : Type u_1
E : Type u_2
K : Type u_3
inst : Field k
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra k E
inst_4 : Algebra k K
inst_5 : Algebra E K
inst_6 : IsScalarTower k E K
L : IntermediateField k E
inst_7 : Normal k E
f : Gal(K/k)
h :
  ∀ (x : K),
    Membership.mem (γ := IntermediateField k K) (map (IsScalarTower.toAlgHom k E K) L) x → (f : (a : K) → K) x = x
x : E
hx : x ∈ L
⊢ Eq (α := K) ((f : (a : K) → K) ((algebraMap E K : (a : E) → K) x : K) : K)
    (((algebraMap E K : E →+* K) : (a : E) → K) x : K)

Tactic:
h _ ⟨x, hx, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
k : Type u_1
E : Type u_2
K : Type u_3
inst : Field k
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra k E
inst_4 : Algebra k K
inst_5 : Algebra E K
inst_6 : IsScalarTower k E K
L : IntermediateField k E
inst_7 : Normal k E
f : Gal(K/k)
h :
  ∀ (x : K),
    Membership.mem (γ := IntermediateField k K) (map (IsScalarTower.toAlgHom k E K) L) x → (f : (a : K) → K) x = x
x : E
hx : x ∈ L
⊢ Eq (α := K) ((f : (a : K) → K) ((algebraMap E K : (a : E) → K) x : K) : K)
    (((algebraMap E K : E →+* K) : (a : E) → K) x : K)

Tactic:
exact h _ ⟨x, hx, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
k : Type u_1
E : Type u_2
K : Type u_3
inst : Field k
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra k E
inst_4 : Algebra k K
inst_5 : Algebra E K
inst_6 : IsScalarTower k E K
L : IntermediateField k E
inst_7 : Normal k E
f : Gal(K/k)
h : ∀ x ∈ L, (((AlgEquiv.restrictNormalHom E : (a : Gal(K/k)) → Gal(E/k)) f : Gal(E/k)) : (a : E) → E) x = x
x : E
hx : x ∈ (↑L.toSubsemiring : Set E)
⊢ Eq.{u_3 + 1} (α := K) ((algebraMap E K : (a : E) → K) ((f.restrictNormal E : (a : E) → E) x : E) : K)
    ((algebraMap E K : (a : E) → K) x : K)

Tactic:
replace h := congr(algebraMap E K $(show f.restrictNormal E x = x from h x hx))
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
k : Type u_1
E : Type u_2
K : Type u_3
inst : Field k
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra k E
inst_4 : Algebra k K
inst_5 : Algebra E K
inst_6 : IsScalarTower k E K
L : IntermediateField k E
inst_7 : Normal k E
f : Gal(K/k)
x : E
hx : x ∈ (↑L.toSubsemiring : Set E)
h :
  Eq.{u_3 + 1} (α := K) ((algebraMap E K : (a : E) → K) ((f.restrictNormal E : (a : E) → E) x : E) : K)
    ((algebraMap E K : (a : E) → K) x : K)
h₁ h₂ h₃ h₄ :
  ∀
    (h :
      Eq (α := K) ((f : (a : K) → K) ((algebraMap E K : (a : E) → K) x : K) : K)
        ((algebraMap E K : (a : E) → K) x : K)),
    Eq (α := K) ((f : (a : K) → K) (((↑(IsScalarTower.toAlgHom k E K) : E →+* K) : (a : E) → K) x : K) : K)
      (((↑(IsScalarTower.toAlgHom k E K) : E →+* K) : (a : E) → K) x : K)
⊢ Eq (α := K) ((f : (a : K) → K) (((↑(IsScalarTower.toAlgHom k E K) : E →+* K) : (a : E) → K) x : K) : K)
    (((↑(IsScalarTower.toAlgHom k E K) : E →+* K) : (a : E) → K) x : K)

Tactic:
rwa [AlgEquiv.restrictNormal_commutes] at h

Premises used: AlgEquiv.restrictNormal_commutes
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
k : Type u_1
E : Type u_2
K : Type u_3
inst : Field k
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra k E
inst_4 : Algebra k K
inst_5 : Algebra E K
inst_6 : IsScalarTower k E K
L : IntermediateField k E
inst_7 : Normal k E
inst_8 : Normal k K
rw :
  Subgroup.index.{u_3} (G := Gal(K/k)) (Subgroup.comap (AlgEquiv.restrictNormalHom E) L.fixingSubgroup) =
    L.fixingSubgroup.index
rw₁ rw₂ : L.fixingSubgroup.index = L.fixingSubgroup.index
⊢ Subgroup.index (G := Gal(K/k)) (fixingSubgroup (map (IsScalarTower.toAlgHom k E K) L)) = L.fixingSubgroup.index

Tactic:
rw [L.map_fixingSubgroup K, L.fixingSubgroup.index_comap_of_surjective
    (AlgEquiv.restrictNormalHom_surjective _)]

Premises used: AlgEquiv.restrictNormalHom_surjective, IntermediateField.map_fixingSubgroup, IntermediateField.fixingSubgroup, Subgroup.index_comap_of_surjective
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
k : Type u_1
K : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
inr :
  ∀
    (this :
      ∀ (L : IntermediateField k K) (hnfd : FiniteDimensional.{u_1, u_3} k ↥L),
        Module.finrank.{u_1, u_3} k ↥L = L.fixingSubgroup.index)
    (hnfd : ¬FiniteDimensional.{u_1, u_3} k ↥L), Module.finrank.{u_1, u_3} k ↥L = L.fixingSubgroup.index
wlog :
  ∀ (L : IntermediateField k K) (hnfd : FiniteDimensional.{u_1, u_3} k ↥L),
    Module.finrank.{u_1, u_3} k ↥L = L.fixingSubgroup.index
⊢ Module.finrank.{u_1, u_3} k ↥L = L.fixingSubgroup.index

Tactic:
wlog hnfd : FiniteDimensional k L generalizing L

Premises used: Membership.mem, Subtype, FiniteDimensional
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
k : Type u_1
K : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
this :
  ∀ (L : IntermediateField k K) (hnfd : FiniteDimensional.{u_1, u_3} k ↥L),
    Module.finrank.{u_1, u_3} k ↥L = L.fixingSubgroup.index
hnfd : ¬FiniteDimensional.{u_1, u_3} k ↥L
inr : 0 = L.fixingSubgroup.index
⊢ Module.finrank.{u_1, u_3} k ↥L = L.fixingSubgroup.index

Tactic:
rw [Module.finrank_of_infinite_dimensional hnfd]

Premises used: Module.finrank_of_infinite_dimensional
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
k : Type u_1
K : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
this :
  ∀ (L : IntermediateField k K) (hnfd : FiniteDimensional.{u_1, u_3} k ↥L),
    Module.finrank.{u_1, u_3} k ↥L = L.fixingSubgroup.index
hnfd : ¬FiniteDimensional.{u_1, u_3} k ↥L
inr : ∀ (h : 0 ≠ L.fixingSubgroup.index), False
⊢ 0 = L.fixingSubgroup.index

Tactic:
by_contra! h
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
k : Type u_1
K : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
this :
  ∀ (L : IntermediateField k K) (hnfd : FiniteDimensional.{u_1, u_3} k ↥L),
    Module.finrank.{u_1, u_3} k ↥L = L.fixingSubgroup.index
hnfd : ¬FiniteDimensional.{u_1, u_3} k ↥L
h : 0 ≠ L.fixingSubgroup.index
⊢ L.fixingSubgroup.FiniteIndex

Tactic:
replace h : L.fixingSubgroup.FiniteIndex := ⟨h.symm⟩
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
k : Type u_1
K : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
this :
  ∀ (L : IntermediateField k K) (hnfd : FiniteDimensional.{u_1, u_3} k ↥L),
    Module.finrank.{u_1, u_3} k ↥L = L.fixingSubgroup.index
hnfd : ¬FiniteDimensional.{u_1, u_3} k ↥L
h : L.fixingSubgroup.FiniteIndex
inr :
  ∀ (L' : IntermediateField k ↥L) (hfd : FiniteDimensional.{u_1, u_3} k ↥L')
    (hL' : L.fixingSubgroup.index < Module.finrank.{u_1, u_3} k ↥L'), False
⊢ False

Tactic:
obtain ⟨L', hfd, hL'⟩ :=
      exists_lt_finrank_of_infinite_dimensional hnfd L.fixingSubgroup.index

Premises used: IntermediateField.fixingSubgroup, Subgroup.index, IntermediateField.exists_lt_finrank_of_infinite_dimensional
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
k : Type u_1
K : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
this :
  ∀ (L : IntermediateField k K) (hnfd : FiniteDimensional.{u_1, u_3} k ↥L),
    Module.finrank.{u_1, u_3} k ↥L = L.fixingSubgroup.index
hnfd : ¬FiniteDimensional.{u_1, u_3} k ↥L
h : L.fixingSubgroup.FiniteIndex
L' : IntermediateField k ↥L
hfd : FiniteDimensional.{u_1, u_3} k ↥L'
hL' : L.fixingSubgroup.index < Module.finrank.{u_1, u_3} k ↥L'
i : ↥L' ≃ₗ[k] ↥(lift L') := (↑(liftAlgEquiv L') : ↥L' ≃ₗ[k] ↥(lift L'))
⊢ FiniteDimensional.{u_1, u_3} k ↥(lift L')

Tactic:
replace hfd := i.finiteDimensional
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
k : Type u_1
K : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
this :
  ∀ (L : IntermediateField k K) (hnfd : FiniteDimensional.{u_1, u_3} k ↥L),
    Module.finrank.{u_1, u_3} k ↥L = L.fixingSubgroup.index
hnfd : ¬FiniteDimensional.{u_1, u_3} k ↥L
h : L.fixingSubgroup.FiniteIndex
L' : IntermediateField k ↥L
hL' : L.fixingSubgroup.index < Module.finrank.{u_1, u_3} k ↥L'
i : ↥L' ≃ₗ[k] ↥(lift L') := (↑(liftAlgEquiv L') : ↥L' ≃ₗ[k] ↥(lift L'))
hfd : FiniteDimensional.{u_1, u_3} k ↥(lift L')
⊢ L.fixingSubgroup.index < (lift L').fixingSubgroup.index

Tactic:
rw [i.finrank_eq, this _ hfd] at hL'

Premises used: LinearEquiv.finrank_eq
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
k : Type u_1
K : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
this :
  ∀ (L : IntermediateField k K) (hnfd : FiniteDimensional.{u_1, u_3} k ↥L),
    Module.finrank.{u_1, u_3} k ↥L = L.fixingSubgroup.index
hnfd : ¬FiniteDimensional.{u_1, u_3} k ↥L
h : L.fixingSubgroup.FiniteIndex
L' : IntermediateField k ↥L
hL' : L.fixingSubgroup.index < Module.finrank.{u_1, u_3} k ↥L'
i : ↥L' ≃ₗ[k] ↥(lift L') := (↑(liftAlgEquiv L') : ↥L' ≃ₗ[k] ↥(lift L'))
hfd : FiniteDimensional.{u_1, u_3} k ↥(lift L')
hL'₁ : L.fixingSubgroup.index < (lift L').fixingSubgroup.index
⊢ FiniteDimensional.{u_1, u_3} k ↥(lift L')

Tactic:
rw [i.finrank_eq, this _ hfd] at hL'

Premises used: LinearEquiv.finrank_eq
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
k : Type u_1
K : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
this :
  ∀ (L : IntermediateField k K) (hnfd : FiniteDimensional.{u_1, u_3} k ↥L),
    Module.finrank.{u_1, u_3} k ↥L = L.fixingSubgroup.index
hnfd : ¬FiniteDimensional.{u_1, u_3} k ↥L
h : L.fixingSubgroup.FiniteIndex
L' : IntermediateField k ↥L
hL' : L.fixingSubgroup.index < (lift L').fixingSubgroup.index
i : ↥L' ≃ₗ[k] ↥(lift L') := (↑(liftAlgEquiv L') : ↥L' ≃ₗ[k] ↥(lift L'))
hfd : FiniteDimensional.{u_1, u_3} k ↥(lift L')
⊢ False

Tactic:
(Subgroup.index_antitone <| fixingSubgroup_le <|
      IntermediateField.lift_le L').not_gt hL'

Premises used: IntermediateField.lift_le, IntermediateField.fixingSubgroup_le, LE.le.not_gt, Subgroup.index_antitone
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
k : Type u_1
K : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
this :
  ∀ (L : IntermediateField k K) (hnfd : FiniteDimensional.{u_1, u_3} k ↥L),
    Module.finrank.{u_1, u_3} k ↥L = L.fixingSubgroup.index
hnfd : ¬FiniteDimensional.{u_1, u_3} k ↥L
h : L.fixingSubgroup.FiniteIndex
L' : IntermediateField k ↥L
hL' : L.fixingSubgroup.index < (lift L').fixingSubgroup.index
i : ↥L' ≃ₗ[k] ↥(lift L') := (↑(liftAlgEquiv L') : ↥L' ≃ₗ[k] ↥(lift L'))
hfd : FiniteDimensional.{u_1, u_3} k ↥(lift L')
⊢ False

Tactic:
exact (Subgroup.index_antitone <| fixingSubgroup_le <|
      IntermediateField.lift_le L').not_gt hL'

Premises used: IntermediateField.lift_le, IntermediateField.fixingSubgroup_le, LE.le.not_gt, Subgroup.index_antitone
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
k : Type u_1
K : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : IsGalois k K
L : IntermediateField k K
hnfd : FiniteDimensional.{u_1, u_3} k ↥L
E : IntermediateField k K := normalClosure k (↥L) K
⊢ L ≤ E

Tactic:
simpa only [fieldRange_val] using L.val.fieldRange_le_normalClosure

Premises used: AlgHom.fieldRange_le_normalClosure, IntermediateField.val, IntermediateField.fieldRange_val
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
k : Type u_1
K : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : IsGalois k K
L : IntermediateField k K
hnfd : FiniteDimensional.{u_1, u_3} k ↥L
E : IntermediateField k K := normalClosure k (↥L) K
⊢ L ≤ E

Tactic:
have hle : L ≤ E := by simpa only [fieldRange_val] using L.val.fieldRange_le_normalClosure
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
k : Type u_1
K : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : IsGalois k K
L : IntermediateField k K
hnfd : FiniteDimensional.{u_1, u_3} k ↥L
E : IntermediateField k K := normalClosure k (↥L) K
hle : L ≤ E
L' : IntermediateField k ↥E := restrict hle
⊢ Module.finrank.{u_1, u_3} k ↥L' * Module.finrank.{u_3, u_3} ↥L' ↥E = Module.finrank.{u_1, u_3} k ↥E

Tactic:
have h := Module.finrank_mul_finrank k ↥L' ↥E
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
k : Type u_1
K : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : IsGalois k K
L : IntermediateField k K
hnfd : FiniteDimensional.{u_1, u_3} k ↥L
E : IntermediateField k K := normalClosure k (↥L) K
hle : L ≤ E
L' : IntermediateField k ↥E := restrict hle
h : Module.finrank.{u_1, u_3} k ↥L' * Module.finrank.{u_3, u_3} ↥L' ↥E = Module.finrank.{u_1, u_3} k ↥E
⊢ Module.finrank.{u_1, u_3} k ↥L' * Nat.card.{u_3} ↥L'.fixingSubgroup = Nat.card.{u_3} Gal(↥E/k)

Tactic:
rw [← IsGalois.card_fixingSubgroup_eq_finrank L', ← IsGalois.card_aut_eq_finrank k E] at h

Premises used: IsGalois.card_aut_eq_finrank, IsGalois.card_fixingSubgroup_eq_finrank, Membership.mem, Subtype
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
k : Type u_1
K : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : IsGalois k K
L : IntermediateField k K
hnfd : FiniteDimensional.{u_1, u_3} k ↥L
E : IntermediateField k K := normalClosure k (↥L) K
hle : L ≤ E
L' : IntermediateField k ↥E := restrict hle
h : Module.finrank.{u_1, u_3} k ↥L' * Nat.card.{u_3} ↥L'.fixingSubgroup = Nat.card.{u_3} Gal(↥E/k)
⊢ Module.finrank.{u_1, u_3} k ↥L' = L'.fixingSubgroup.index

Tactic:
rw [← L'.fixingSubgroup.index_mul_card, Nat.mul_left_inj Finite.card_pos.ne'] at h

Premises used: Subgroup.index_mul_card, IntermediateField.fixingSubgroup, Finite.card_pos, LT.lt.ne', Nat.mul_left_inj
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
k : Type u_1
K : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : IsGalois k K
L : IntermediateField k K
hnfd : FiniteDimensional.{u_1, u_3} k ↥L
E : IntermediateField k K := normalClosure k (↥L) K
hle : L ≤ E
L' : IntermediateField k ↥E := restrict hle
h : Module.finrank.{u_1, u_3} k ↥L' = L'.fixingSubgroup.index
rw : Subgroup.index (G := Gal(K/k)) (fixingSubgroup (map (IsScalarTower.toAlgHom k (↥E) K) L')) = L.fixingSubgroup.index
⊢ Module.finrank.{u_1, u_3} k ↥L = L.fixingSubgroup.index

Tactic:
rw [(restrict_algEquiv hle).toLinearEquiv.finrank_eq, h, ← L'.map_fixingSubgroup_index K]

Premises used: LinearEquiv.finrank_eq, IntermediateField.map_fixingSubgroup_index, AlgEquiv.toLinearEquiv, IntermediateField.restrict_algEquiv