awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (goal)
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)
⊢ 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)
have 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)
Tactic: rwa [AlgEquiv.restrictNormal_commutes] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (goal)
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
⊢ Subgroup.index (G := Gal(K/k)) (fixingSubgroup (map (IsScalarTower.toAlgHom k E K) L)) = L.fixingSubgroup.index
have rw : Subgroup.index.{u_3} (G := Gal(K/k)) (Subgroup.comap (AlgEquiv.restrictNormalHom E) L.fixingSubgroup) =
  L.fixingSubgroup.index
Tactic: rw [L.map_fixingSubgroup K, L.fixingSubgroup.index_comap_of_surjective
    (AlgEquiv.restrictNormalHom_surjective _)]
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (goal)
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
⊢ Subgroup.index (G := Gal(K/k)) (fixingSubgroup (map (IsScalarTower.toAlgHom k E K) L)) = L.fixingSubgroup.index
have rw₁ : L.fixingSubgroup.index = L.fixingSubgroup.index
Tactic: rw [L.map_fixingSubgroup K, L.fixingSubgroup.index_comap_of_surjective
    (AlgEquiv.restrictNormalHom_surjective _)]
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (goal)
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
⊢ Module.finrank.{u_1, u_3} k ↥L = L.fixingSubgroup.index
have 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
Tactic: wlog hnfd : FiniteDimensional k L generalizing L
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (goal)
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
⊢ Module.finrank.{u_1, u_3} k ↥L = L.fixingSubgroup.index
have wlog : ∀ (L : IntermediateField k K) (hnfd : FiniteDimensional.{u_1, u_3} k ↥L),
  Module.finrank.{u_1, u_3} k ↥L = L.fixingSubgroup.index
Tactic: wlog hnfd : FiniteDimensional k L generalizing L
Cleared hypotheses: L
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (goal)
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
⊢ Module.finrank.{u_1, u_3} k ↥L = L.fixingSubgroup.index
have inr : 0 = L.fixingSubgroup.index
Tactic: rw [Module.finrank_of_infinite_dimensional hnfd]
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (goal)
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
⊢ 0 = L.fixingSubgroup.index
have inr : ∀ (h : 0 ≠ L.fixingSubgroup.index), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (hypothesis)
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
⊢ False
have h₁ : L.fixingSubgroup.FiniteIndex
Tactic: replace h : L.fixingSubgroup.FiniteIndex := ⟨h.symm⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (goal)
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
⊢ False
have 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
Tactic: obtain ⟨L', hfd, hL'⟩ :=
      exists_lt_finrank_of_infinite_dimensional hnfd L.fixingSubgroup.index
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (hypothesis)
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'))
⊢ False
have hfd₁ : FiniteDimensional.{u_1, u_3} k ↥(lift L')
Tactic: replace hfd := i.finiteDimensional
Cleared hypotheses: hfd
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (hypothesis)
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')
⊢ False
have hL'₁ : L.fixingSubgroup.index < (lift L').fixingSubgroup.index
Tactic: rw [i.finrank_eq, this _ hfd] at hL'
Cleared hypotheses: hL', i, hfd
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (hypothesis)
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
⊢ Module.finrank.{u_1, u_3} k ↥L = L.fixingSubgroup.index
have hle : L ≤ E
Tactic: have hle : L ≤ E := by simpa only [fieldRange_val] using L.val.fieldRange_le_normalClosure
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (hypothesis)
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 = L.fixingSubgroup.index
have 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
Tactic: have h := Module.finrank_mul_finrank k ↥L' ↥E
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (hypothesis)
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 = L.fixingSubgroup.index
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (hypothesis)
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
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (goal)
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
⊢ Module.finrank.{u_1, u_3} k ↥L = L.fixingSubgroup.index
have rw : Subgroup.index (G := Gal(K/k)) (fixingSubgroup (map (IsScalarTower.toAlgHom k (↥E) K) L')) = L.fixingSubgroup.index
Tactic: rw [(restrict_algEquiv hle).toLinearEquiv.finrank_eq, h, ← L'.map_fixingSubgroup_index K]
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (goal)
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
⊢ Subgroup.index (G := Gal(K/k)) (fixingSubgroup (map (IsScalarTower.toAlgHom k (↥E) K) L')) = L.fixingSubgroup.index
have e_H : map (IsScalarTower.toAlgHom k (↥E) K) L' = L
Tactic: congr 2
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (goal)
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 = L.fixingSubgroup.index
have rw : ∀ (h : Module.finrank.{u_1, u_3} k ↥L' * Nat.card.{u_3} ↥L'.fixingSubgroup = Module.finrank.{u_1, u_3} k ↥E),
  Module.finrank.{u_1, u_3} k ↥L = L.fixingSubgroup.index
Tactic: classical
  rw [← IsGalois.card_fixingSubgroup_eq_finrank L', ← IsGalois.card_aut_eq_finrank k E] at h
  rw [← L'.fixingSubgroup.index_mul_card, Nat.mul_left_inj Finite.card_pos.ne'] at h
  rw [(restrict_algEquiv hle).toLinearEquiv.finrank_eq, h, ← L'.map_fixingSubgroup_index K]
  congr 2
  exact lift_restrict hle
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (goal)
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
rw :
  ∀ (h : Module.finrank.{u_1, u_3} k ↥L' * Nat.card.{u_3} ↥L'.fixingSubgroup = Module.finrank.{u_1, u_3} k ↥E),
    Module.finrank.{u_1, u_3} k ↥L = L.fixingSubgroup.index
⊢ Module.finrank.{u_1, u_3} k ↥L = L.fixingSubgroup.index
have rw₁ : ∀ (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: classical
  rw [← IsGalois.card_fixingSubgroup_eq_finrank L', ← IsGalois.card_aut_eq_finrank k E] at h
  rw [← L'.fixingSubgroup.index_mul_card, Nat.mul_left_inj Finite.card_pos.ne'] at h
  rw [(restrict_algEquiv hle).toLinearEquiv.finrank_eq, h, ← L'.map_fixingSubgroup_index K]
  congr 2
  exact lift_restrict hle
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (goal)
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
rw :
  ∀ (h : Module.finrank.{u_1, u_3} k ↥L' * Nat.card.{u_3} ↥L'.fixingSubgroup = Module.finrank.{u_1, u_3} k ↥E),
    Module.finrank.{u_1, u_3} k ↥L = L.fixingSubgroup.index
rw₁ rw₂ rw₃ :
  ∀ (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
⊢ Module.finrank.{u_1, u_3} k ↥L = L.fixingSubgroup.index
have rw₄ : ∀ (h : Module.finrank.{u_1, u_3} k ↥L' = L'.fixingSubgroup.index),
  Module.finrank.{u_1, u_3} k ↥L = L.fixingSubgroup.index
Tactic: classical
  rw [← IsGalois.card_fixingSubgroup_eq_finrank L', ← IsGalois.card_aut_eq_finrank k E] at h
  rw [← L'.fixingSubgroup.index_mul_card, Nat.mul_left_inj Finite.card_pos.ne'] at h
  rw [(restrict_algEquiv hle).toLinearEquiv.finrank_eq, h, ← L'.map_fixingSubgroup_index K]
  congr 2
  exact lift_restrict hle
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (goal)
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
rw :
  ∀ (h : Module.finrank.{u_1, u_3} k ↥L' * Nat.card.{u_3} ↥L'.fixingSubgroup = Module.finrank.{u_1, u_3} k ↥E),
    Module.finrank.{u_1, u_3} k ↥L = L.fixingSubgroup.index
rw₁ rw₂ rw₃ :
  ∀ (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
rw₄ :
  ∀ (h : Module.finrank.{u_1, u_3} k ↥L' = L'.fixingSubgroup.index),
    Module.finrank.{u_1, u_3} k ↥L = L.fixingSubgroup.index
⊢ Module.finrank.{u_1, u_3} k ↥L = L.fixingSubgroup.index
have rw₅ : ∀ (h : Module.finrank.{u_1, u_3} k ↥L' = L'.fixingSubgroup.index),
  Subgroup.index (G := Gal(K/k)) (fixingSubgroup (map (IsScalarTower.toAlgHom k (↥E) K) L')) = L.fixingSubgroup.index
Tactic: classical
  rw [← IsGalois.card_fixingSubgroup_eq_finrank L', ← IsGalois.card_aut_eq_finrank k E] at h
  rw [← L'.fixingSubgroup.index_mul_card, Nat.mul_left_inj Finite.card_pos.ne'] at h
  rw [(restrict_algEquiv hle).toLinearEquiv.finrank_eq, h, ← L'.map_fixingSubgroup_index K]
  congr 2
  exact lift_restrict hle
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (goal)
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
rw :
  ∀ (h : Module.finrank.{u_1, u_3} k ↥L' * Nat.card.{u_3} ↥L'.fixingSubgroup = Module.finrank.{u_1, u_3} k ↥E),
    Module.finrank.{u_1, u_3} k ↥L = L.fixingSubgroup.index
rw₁ rw₂ rw₃ :
  ∀ (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
rw₄ :
  ∀ (h : Module.finrank.{u_1, u_3} k ↥L' = L'.fixingSubgroup.index),
    Module.finrank.{u_1, u_3} k ↥L = L.fixingSubgroup.index
rw₅ :
  ∀ (h : Module.finrank.{u_1, u_3} k ↥L' = L'.fixingSubgroup.index),
    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
have e_H : ∀ (h : Module.finrank.{u_1, u_3} k ↥L' = L'.fixingSubgroup.index), map (IsScalarTower.toAlgHom k (↥E) K) L' = L
Tactic: classical
  rw [← IsGalois.card_fixingSubgroup_eq_finrank L', ← IsGalois.card_aut_eq_finrank k E] at h
  rw [← L'.fixingSubgroup.index_mul_card, Nat.mul_left_inj Finite.card_pos.ne'] at h
  rw [(restrict_algEquiv hle).toLinearEquiv.finrank_eq, h, ← L'.map_fixingSubgroup_index K]
  congr 2
  exact lift_restrict hle
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
Goal:
K : Type u
inst : Field K
n : ℕ
ζ : K
hζ : IsPrimitiveRoot ζ n
α a : K
e : α ^ n = a
hn : n > 0
⊢ (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])).Splits
have inr : (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])).roots.card =
  (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])).natDegree
Tactic: rw [splits_iff_card_roots, ← nthRoots, hζ.card_nthRoots, natDegree_X_pow_sub_C, if_pos ⟨α, e⟩]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
Goal:
K : Type u
inst : Field K
n : ℕ
ζ : K
hζ : IsPrimitiveRoot ζ n
α a : K
e : α ^ n = a
hn : n > 0
inr :
  (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])).roots.card =
    (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])).natDegree
⊢ (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])).Splits
have inr₁ : (nthRoots n a).card = (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])).natDegree
Tactic: rw [splits_iff_card_roots, ← nthRoots, hζ.card_nthRoots, natDegree_X_pow_sub_C, if_pos ⟨α, e⟩]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
Goal:
K : Type u
inst : Field K
n : ℕ
ζ : K
hζ : IsPrimitiveRoot ζ n
α a : K
e : α ^ n = a
hn : n > 0
inr :
  (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])).roots.card =
    (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])).natDegree
inr₁ :
  (nthRoots n a).card = (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])).natDegree
⊢ (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])).Splits
have inr₂ : (if ∃ (α : K), α ^ n = a then n else 0) =
  (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])).natDegree
Tactic: rw [splits_iff_card_roots, ← nthRoots, hζ.card_nthRoots, natDegree_X_pow_sub_C, if_pos ⟨α, e⟩]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
Goal:
K : Type u
inst : Field K
n : ℕ
ζ : K
hζ : IsPrimitiveRoot ζ n
α a : K
e : α ^ n = a
hn : n > 0
inr :
  (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])).roots.card =
    (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])).natDegree
inr₁ :
  (nthRoots n a).card = (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])).natDegree
inr₂ :
  (if ∃ (α : K), α ^ n = a then n else 0) =
    (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])).natDegree
⊢ (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])).Splits
have inr₃ : (if ∃ (α : K), α ^ n = a then n else 0) = n
Tactic: rw [splits_iff_card_roots, ← nthRoots, hζ.card_nthRoots, natDegree_X_pow_sub_C, if_pos ⟨α, e⟩]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
Goal:
K : Type u
inst : Field K
n : ℕ
ζ : K
hζ : IsPrimitiveRoot ζ n
α a : K
e : α ^ n = a
hn : n > 0
inr :
  (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])).roots.card =
    (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])).natDegree
inr₁ :
  (nthRoots n a).card = (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])).natDegree
inr₂ :
  (if ∃ (α : K), α ^ n = a then n else 0) =
    (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])).natDegree
inr₃ : (if ∃ (α : K), α ^ n = a then n else 0) = n
⊢ (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])).Splits
have inr₄ : n = n
Tactic: rw [splits_iff_card_roots, ← nthRoots, hζ.card_nthRoots, natDegree_X_pow_sub_C, if_pos ⟨α, e⟩]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (hypothesis)
Goal:
K : Type u
inst : Field K
n : ℕ
ζ : K
hζ : IsPrimitiveRoot ζ n
α a : K
e : α ^ n = a
⊢ (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])).Splits
have x : n = 0 ∨ n > 0
Tactic: cases n.eq_zero_or_pos with
  | inl hn =>
    simp only [hn, pow_zero, ← C.map_one, ← map_sub, Splits.C]
  | inr hn =>
    rw [splits_iff_card_roots, ← nthRoots, hζ.card_nthRoots, natDegree_X_pow_sub_C, if_pos ⟨α, e⟩]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (goal)
Goal:
K : Type u
inst : Field K
n : ℕ
ζ : K
hζ : IsPrimitiveRoot ζ n
α a : K
hn : 0 < n
e : α ^ n = a
⊢ HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X]) =
    ∏ i ∈ Finset.range n, HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) (ζ ^ i * α) : K[X])
have rw : Eq.{u + 1} (α := K[X])
  (Multiset.prod
    (Multiset.map
      ((fun (x : K) ↦ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])) ∘ fun (x : ℕ) ↦ ζ ^ x * α)
      (Multiset.range n)))
  (∏ i ∈ Finset.range n, HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) (ζ ^ i * α) : K[X]))
Tactic: rw [(X_pow_sub_C_splits_of_isPrimitiveRoot hζ e).eq_prod_roots_of_monic
    (monic_X_pow_sub_C _ hn.ne'), ← nthRoots, hζ.nthRoots_eq e, Multiset.map_map]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerExtension (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
hn : 0 < n
e : α ^ n = a
K : Type u_1 := FractionRing R
i : R →+* K := algebraMap R K
⊢ HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X]) =
    ∏ i ∈ Finset.range n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (ζ ^ i * α) : R[X])
have h : Function.Injective (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K)
Tactic: have h := FaithfulSMul.algebraMap_injective R K