awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (goal)
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
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : Ne (α := L) ((f : (a : L) → L) x : L) ((g : (a : L) → L) x : L)
hφx : (φ : (a : L) → L) x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional.{u_1, u_2} K ↥E := ⋯
H : Subgroup Gal(L/K) := E.fixingSubgroup
h_basis : Membership.mem (γ := GroupFilterBasis Gal(L/K)) (galGroupBasis K L) (↑H : Set Gal(L/K))
h_nhds : ∃ t ⊆ (↑H : Set Gal(L/K)), IsOpen t ∧ 1 ∈ t
⊢ (fun (x y : Gal(L/K)) ↦ ∃ (u : Set Gal(L/K)) (v : Set Gal(L/K)), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v) f
    g
have rcases : ∀ (W : Set Gal(L/K)) (hWH : W ⊆ (↑H : Set Gal(L/K))) (hW_open : IsOpen W) (hW_1 : 1 ∈ W),
  (fun (x y : Gal(L/K)) ↦ ∃ (u : Set Gal(L/K)) (v : Set Gal(L/K)), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v) f
    g
Tactic: rcases h_nhds with ⟨W, hWH, hW_open, hW_1⟩
Cleared hypotheses: h_nhds
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (goal)
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
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : Ne (α := L) ((f : (a : L) → L) x : L) ((g : (a : L) → L) x : L)
hφx : (φ : (a : L) → L) x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional.{u_1, u_2} K ↥E := ⋯
H : Subgroup Gal(L/K) := E.fixingSubgroup
h_basis : Membership.mem (γ := GroupFilterBasis Gal(L/K)) (galGroupBasis K L) (↑H : Set Gal(L/K))
W : Set Gal(L/K)
hWH : W ⊆ (↑H : Set Gal(L/K))
hW_open : IsOpen W
hW_1 : 1 ∈ W
⊢ (fun (x y : Gal(L/K)) ↦ ∃ (u : Set Gal(L/K)) (v : Set Gal(L/K)), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v) f
    g
have refine : Disjoint (f • W) (g • W)
Tactic: refine ⟨f • W, g • W,
        ⟨hW_open.leftCoset f, hW_open.leftCoset g, ⟨1, hW_1, mul_one _⟩, ⟨1, hW_1, mul_one _⟩, ?_⟩⟩
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (goal)
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
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : Ne (α := L) ((f : (a : L) → L) x : L) ((g : (a : L) → L) x : L)
hφx : (φ : (a : L) → L) x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional.{u_1, u_2} K ↥E := ⋯
H : Subgroup Gal(L/K) := E.fixingSubgroup
h_basis : Membership.mem (γ := GroupFilterBasis Gal(L/K)) (galGroupBasis K L) (↑H : Set Gal(L/K))
W : Set Gal(L/K)
hWH : W ⊆ (↑H : Set Gal(L/K))
hW_open : IsOpen W
hW_1 : 1 ∈ W
⊢ Disjoint (f • W) (g • W)
have rw : ∀ ⦃a : Gal(L/K)⦄, a ∈ f • W → a ∉ g • W
Tactic: rw [Set.disjoint_left]
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (hypothesis)
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
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : Ne (α := L) ((f : (a : L) → L) x : L) ((g : (a : L) → L) x : L)
hφx : (φ : (a : L) → L) x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional.{u_1, u_2} K ↥E := ⋯
H : Subgroup Gal(L/K) := E.fixingSubgroup
h_basis : Membership.mem (γ := GroupFilterBasis Gal(L/K)) (galGroupBasis K L) (↑H : Set Gal(L/K))
W : Set Gal(L/K)
hWH : W ⊆ (↑H : Set Gal(L/K))
hW_open : IsOpen W
hW_1 : 1 ∈ W
w1 : Gal(L/K)
hw1 : w1 ∈ W
w2 : Gal(L/K)
hw2 : w2 ∈ W
h : f * w1 = g * w2
⊢ False
have h₁ : w1 * w2⁻¹ = f⁻¹ * g
Tactic: rw [eq_inv_mul_iff_mul_eq.symm, ← mul_assoc, mul_inv_eq_iff_eq_mul.symm] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (hypothesis)
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
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : Ne (α := L) ((f : (a : L) → L) x : L) ((g : (a : L) → L) x : L)
hφx : (φ : (a : L) → L) x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional.{u_1, u_2} K ↥E := ⋯
H : Subgroup Gal(L/K) := E.fixingSubgroup
h_basis : Membership.mem (γ := GroupFilterBasis Gal(L/K)) (galGroupBasis K L) (↑H : Set Gal(L/K))
W : Set Gal(L/K)
hWH : W ⊆ (↑H : Set Gal(L/K))
hW_open : IsOpen W
hW_1 : 1 ∈ W
w1 : Gal(L/K)
hw1 : w1 ∈ W
w2 : Gal(L/K)
hw2 : w2 ∈ W
h : w1 * w2⁻¹ = f⁻¹ * g
⊢ False
have h_in_H : w1 * w2⁻¹ ∈ H
Tactic: have h_in_H : w1 * w2⁻¹ ∈ H := H.mul_mem (hWH hw1) (H.inv_mem (hWH hw2))
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (hypothesis)
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
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : Ne (α := L) ((f : (a : L) → L) x : L) ((g : (a : L) → L) x : L)
hφx : (φ : (a : L) → L) x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional.{u_1, u_2} K ↥E := ⋯
H : Subgroup Gal(L/K) := E.fixingSubgroup
h_basis : Membership.mem (γ := GroupFilterBasis Gal(L/K)) (galGroupBasis K L) (↑H : Set Gal(L/K))
W : Set Gal(L/K)
hWH : W ⊆ (↑H : Set Gal(L/K))
hW_open : IsOpen W
hW_1 : 1 ∈ W
w1 : Gal(L/K)
hw1 : w1 ∈ W
w2 : Gal(L/K)
hw2 : w2 ∈ W
h : w1 * w2⁻¹ = f⁻¹ * g
h_in_H : w1 * w2⁻¹ ∈ H
⊢ False
have h_in_H₁ : f⁻¹ * g ∈ H
Tactic: rw [h] at h_in_H
Cleared hypotheses: h_in_H
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (hypothesis)
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
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : Ne (α := L) ((f : (a : L) → L) x : L) ((g : (a : L) → L) x : L)
hφx : (φ : (a : L) → L) x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional.{u_1, u_2} K ↥E := ⋯
H : Subgroup Gal(L/K) := E.fixingSubgroup
h_basis : Membership.mem (γ := GroupFilterBasis Gal(L/K)) (galGroupBasis K L) (↑H : Set Gal(L/K))
W : Set Gal(L/K)
hWH : W ⊆ (↑H : Set Gal(L/K))
hW_open : IsOpen W
hW_1 : 1 ∈ W
w1 : Gal(L/K)
hw1 : w1 ∈ W
w2 : Gal(L/K)
hw2 : w2 ∈ W
h : w1 * w2⁻¹ = f⁻¹ * g
h_in_H : φ ∈ E.fixingSubgroup
⊢ False
have h_in_H₁ : ∀ x ∈ E, (φ : (a : L) → L) x = x
Tactic: rw [IntermediateField.mem_fixingSubgroup_iff] at h_in_H
Cleared hypotheses: h_in_H
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (hypothesis)
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
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : Ne (α := L) ((f : (a : L) → L) x : L) ((g : (a : L) → L) x : L)
hφx : (φ : (a : L) → L) x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional.{u_1, u_2} K ↥E := ⋯
H : Subgroup Gal(L/K) := E.fixingSubgroup
h_basis : Membership.mem (γ := GroupFilterBasis Gal(L/K)) (galGroupBasis K L) (↑H : Set Gal(L/K))
W : Set Gal(L/K)
hWH : W ⊆ (↑H : Set Gal(L/K))
hW_open : IsOpen W
hW_1 : 1 ∈ W
w1 : Gal(L/K)
hw1 : w1 ∈ W
w2 : Gal(L/K)
hw2 : w2 ∈ W
h : w1 * w2⁻¹ = f⁻¹ * g
h_in_H : ∀ x ∈ E, (φ : (a : L) → L) x = x
⊢ False
have h_in_H₁ : x ∈ E → (φ : (a : L) → L) x = x
Tactic: specialize h_in_H x
Cleared hypotheses: h_in_H
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (goal)
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
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : Ne (α := L) ((f : (a : L) → L) x : L) ((g : (a : L) → L) x : L)
hφx : (φ : (a : L) → L) x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional.{u_1, u_2} K ↥E := ⋯
H : Subgroup Gal(L/K) := E.fixingSubgroup
h_basis : Membership.mem (γ := GroupFilterBasis Gal(L/K)) (galGroupBasis K L) (↑H : Set Gal(L/K))
W : Set Gal(L/K)
hWH : W ⊆ (↑H : Set Gal(L/K))
hW_open : IsOpen W
hW_1 : 1 ∈ W
w1 : Gal(L/K)
hw1 : w1 ∈ W
w2 : Gal(L/K)
hw2 : w2 ∈ W
h : w1 * w2⁻¹ = f⁻¹ * g
h_in_H : x ∈ E → (φ : (a : L) → L) x = x
⊢ x ∈ E
have a : Membership.mem (γ := Set L) {x} x
Tactic: apply IntermediateField.subset_adjoin
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (hypothesis)
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
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : Ne (α := L) ((f : (a : L) → L) x : L) ((g : (a : L) → L) x : L)
hφx : (φ : (a : L) → L) x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional.{u_1, u_2} K ↥E := ⋯
H : Subgroup Gal(L/K) := E.fixingSubgroup
h_basis : Membership.mem (γ := GroupFilterBasis Gal(L/K)) (galGroupBasis K L) (↑H : Set Gal(L/K))
W : Set Gal(L/K)
hWH : W ⊆ (↑H : Set Gal(L/K))
hW_open : IsOpen W
hW_1 : 1 ∈ W
w1 : Gal(L/K)
hw1 : w1 ∈ W
w2 : Gal(L/K)
hw2 : w2 ∈ W
h : w1 * w2⁻¹ = f⁻¹ * g
h_in_H : x ∈ E → (φ : (a : L) → L) x = x
⊢ False
have hxE : x ∈ E
Tactic: have hxE : x ∈ E := by
        apply IntermediateField.subset_adjoin
        apply Set.mem_singleton
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (goal)
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
⊢ TotallySeparatedSpace.{u_2} Gal(L/K)
have rw : Pairwise fun (x1 x2 : Gal(L/K)) ↦ ∃ (U : Set Gal(L/K)), IsClopen U ∧ x1 ∈ U ∧ x2 ∈ Uᶜ
Tactic: rw [totallySeparatedSpace_iff_exists_isClopen]
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (goal)
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
σ τ : Gal(L/K)
h_diff : σ ≠ τ
⊢ σ⁻¹ * τ ≠ 1
have rwa : ¬σ⁻¹ * τ = 1
Tactic: rwa [Ne, inv_mul_eq_one]
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (goal)
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
σ τ : Gal(L/K)
h_diff : σ ≠ τ
rwa : ¬σ⁻¹ * τ = 1
⊢ σ⁻¹ * τ ≠ 1
have rwa₁ : ¬σ = τ
Tactic: rwa [Ne, inv_mul_eq_one]
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (hypothesis)
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
σ τ : Gal(L/K)
h_diff : σ ≠ τ
⊢ ∃ (U : Set Gal(L/K)), IsClopen U ∧ σ ∈ U ∧ τ ∈ Uᶜ
have hστ : σ⁻¹ * τ ≠ 1
Tactic: have hστ : σ⁻¹ * τ ≠ 1 := by rwa [Ne, inv_mul_eq_one]
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (goal)
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
σ τ : Gal(L/K)
h_diff : σ ≠ τ
hστ : σ⁻¹ * τ ≠ 1
⊢ ∃ (U : Set Gal(L/K)), IsClopen U ∧ σ ∈ U ∧ τ ∈ Uᶜ
have rcases : ∀ (x : L) (hx : (σ⁻¹ * τ : (a : L) → L) x ≠ x), ∃ (U : Set Gal(L/K)), IsClopen U ∧ σ ∈ U ∧ τ ∈ Uᶜ
Tactic: rcases DFunLike.exists_ne hστ with ⟨x, hx : (σ⁻¹ * τ) x ≠ x⟩
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (hypothesis)
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
σ τ : Gal(L/K)
h_diff : σ ≠ τ
hστ : σ⁻¹ * τ ≠ 1
x : L
hx : (σ⁻¹ * τ : (a : L) → L) x ≠ x
E : IntermediateField K L := K⟮x⟯
⊢ ∃ (U : Set Gal(L/K)), IsClopen U ∧ σ ∈ U ∧ τ ∈ Uᶜ
have this : FiniteDimensional.{u_1, u_2} K ↥K⟮x⟯
Tactic: haveI := IntermediateField.adjoin.finiteDimensional
    (Algebra.IsIntegral.isIntegral (R := K) x)
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (goal)
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
σ τ : Gal(L/K)
h_diff : σ ≠ τ
hστ : σ⁻¹ * τ ≠ 1
x : L
hx : (σ⁻¹ * τ : (a : L) → L) x ≠ x
E : IntermediateField K L := K⟮x⟯
this : FiniteDimensional.{u_1, u_2} K ↥K⟮x⟯
⊢ ∃ (U : Set Gal(L/K)), IsClopen U ∧ σ ∈ U ∧ τ ∈ Uᶜ
have refine : τ ∈ (σ • (↑E.fixingSubgroup : Set Gal(L/K)))ᶜ
Tactic: refine ⟨σ • E.fixingSubgroup,
    ⟨E.fixingSubgroup_isClosed.leftCoset σ, E.fixingSubgroup_isOpen.leftCoset σ⟩,
    ⟨1, E.fixingSubgroup.one_mem', mul_one σ⟩, ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (goal)
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
σ τ : Gal(L/K)
h_diff : σ ≠ τ
hστ : σ⁻¹ * τ ≠ 1
x : L
hx : (σ⁻¹ * τ : (a : L) → L) x ≠ x
E : IntermediateField K L := K⟮x⟯
this : FiniteDimensional.{u_1, u_2} K ↥K⟮x⟯
⊢ τ ∈ (σ • (↑E.fixingSubgroup : Set Gal(L/K)))ᶜ
have simp : ∃ (x : L) (_ : x ∈ E), ¬(σ⁻¹ * τ : (a : L) → L) x = x
Tactic: simp only [Set.mem_compl_iff, mem_leftCoset_iff, SetLike.mem_coe,
    IntermediateField.mem_fixingSubgroup_iff, not_forall]
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (goal)
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
⊢ DiscreteTopology.{u_2} Gal(L/K)
have rw : IsOpen (X := Gal(L/K)) {1}
Tactic: rw [discreteTopology_iff_isOpen_singleton_one]
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (goal)
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 (↑⊥ : Set Gal(L/K))
have rw : IsOpen (↑(IntermediateField.fixingSubgroup ⊤) : Set Gal(L/K))
Tactic: rw [← IntermediateField.fixingSubgroup_top]
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (hypothesis)
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⟯
⊢ IsOpen (↑(MulAction.stabilizer Gal(L/K) x) : Set Gal(L/K))
have hL : FiniteDimensional.{u_1, u_2} K ↥E
Tactic: have hL : FiniteDimensional K E := adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral x)
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (goal)
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 (↑(MulAction.stabilizer Gal(L/K) x) : Set Gal(L/K))
have h : MulAction.stabilizer Gal(L/K) x = E.fixingSubgroup
Tactic: convert! fixingSubgroup_isOpen E
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (goal)
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
⊢ MulAction.stabilizer Gal(L/K) x = E.fixingSubgroup
have h : ∀ (g : Gal(L/K)), Membership.mem (γ := Subgroup Gal(L/K)) (MulAction.stabilizer Gal(L/K) x) g ↔ g ∈ E.fixingSubgroup
Tactic: ext g
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (goal)
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))
⊢ IsOpen (↑(MulAction.stabilizer Gal(L/K) x) : Set Gal(L/K))
have 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))
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
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (goal)
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))
⊢ IsOpen (↑(MulAction.stabilizer Gal(L/K) x) : Set Gal(L/K))
have h : let E : IntermediateField K L := K⟮x⟯;
∀ (hL : FiniteDimensional.{u_1, u_2} K ↥E), MulAction.stabilizer Gal(L/K) x = E.fixingSubgroup
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
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (goal)
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
⊢ IsOpen (↑(MulAction.stabilizer Gal(L/K) x) : Set Gal(L/K))
have 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
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
-- 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
⊢ Eq (α := Subgroup Gal(K/k)) (fixingSubgroup (map (IsScalarTower.toAlgHom k E K) L))
    (Subgroup.comap (AlgEquiv.restrictNormalHom E) L.fixingSubgroup)
have 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
Tactic: ext f
-- 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)
⊢ 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
have 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
Tactic: simp only [Subgroup.mem_comap, mem_fixingSubgroup_iff]
-- 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 : 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
have 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
Tactic: constructor
-- 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)
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
⊢ (∀ (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
have 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
Tactic: constructor
-- 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)
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
⊢ (((AlgEquiv.restrictNormalHom E : (a : Gal(K/k)) → Gal(E/k)) f : Gal(E/k)) : (a : E) → E) x = x
have h₁ : (f.restrictNormal E : (a : E) → E) x = x
Tactic: change f.restrictNormal E x = x
-- 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)
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
⊢ (f.restrictNormal E : (a : E) → E) x = x
have 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)
Tactic: apply_fun _ using (algebraMap E K).injective
-- 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)
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.{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)
have 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)
Tactic: rw [AlgEquiv.restrictNormal_commutes]
-- Lean 4 proof step from Mathlib.FieldTheory.KrullTopology (hypothesis)
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 (α := 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₁ : 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))
Cleared hypotheses: h