awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Infinite (goal)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
H : ClosedSubgroup Gal(K/k)
inst_3 : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField (↑H : Subgroup Gal(K/k))).fixingSubgroup
h : σ ∉ (↑H : Subgroup Gal(K/k))
b : Set Gal(K/k)
sub : b ⊆ (fun (y : Gal(K/k)) ↦ σ * y) ⁻¹' (↑H : Subgroup Gal(K/k)).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq : (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) L.fixingSubgroup = b
hL : Membership.mem (γ := Set (IntermediateField k K)) (finiteExts k K) L
eq' : L.fixingSubgroup = gp
this : FiniteDimensional.{u_1, u_2} k ↥L
L' : FiniteGaloisIntermediateField k K :=
  let __src : IntermediateField k K := normalClosure k (↥L) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
compl : σ • L'.fixingSubgroup.carrier ⊆ (↑H : Subgroup Gal(K/k)).carrierᶜ
fix :
  ∀ (x : K),
    Membership.mem (γ := IntermediateField k K)
        (lift (F := L'.toIntermediateField)
          (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) (↑H : Subgroup Gal(K/k)))))
        x →
      (σ : (a : K) → K) x = x
⊢ Membership.mem (α := Gal(↥L'.toIntermediateField/k)) (γ := Subgroup Gal(↥L'.toIntermediateField/k))
    (IntermediateField.fixingSubgroup
      (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) (↑H : Subgroup Gal(K/k)))))
    ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) σ :
      Gal(↥L'.toIntermediateField/k))
have apply : ∀
  y ∈
    (↑(fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) (↑H : Subgroup Gal(K/k)))) :
      Set ↥L'.toIntermediateField),
  HSMul.hSMul (α := Gal(↥L'.toIntermediateField/k))
      ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) σ :
        Gal(↥L'.toIntermediateField/k))
      y =
    y
Tactic: apply (mem_fixingSubgroup_iff (L' ≃ₐ[k] L')).mpr
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Infinite (goal)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
H : ClosedSubgroup Gal(K/k)
inst_3 : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField (↑H : Subgroup Gal(K/k))).fixingSubgroup
h : σ ∉ (↑H : Subgroup Gal(K/k))
b : Set Gal(K/k)
sub : b ⊆ (fun (y : Gal(K/k)) ↦ σ * y) ⁻¹' (↑H : Subgroup Gal(K/k)).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq : (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) L.fixingSubgroup = b
hL : Membership.mem (γ := Set (IntermediateField k K)) (finiteExts k K) L
eq' : L.fixingSubgroup = gp
this : FiniteDimensional.{u_1, u_2} k ↥L
L' : FiniteGaloisIntermediateField k K :=
  let __src : IntermediateField k K := normalClosure k (↥L) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
compl : σ • L'.fixingSubgroup.carrier ⊆ (↑H : Subgroup Gal(K/k)).carrierᶜ
fix :
  ∀ (x : K),
    Membership.mem (γ := IntermediateField k K)
        (lift (F := L'.toIntermediateField)
          (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) (↑H : Subgroup Gal(K/k)))))
        x →
      (σ : (a : K) → K) x = x
y : ↥L'.toIntermediateField
hy :
  y ∈
    (↑(fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) (↑H : Subgroup Gal(K/k)))) :
      Set ↥L'.toIntermediateField)
⊢ HSMul.hSMul (α := Gal(↥L'.toIntermediateField/k))
      ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) σ :
        Gal(↥L'.toIntermediateField/k))
      y =
    y
have a : (↑(HSMul.hSMul (α := Gal(↥L'.toIntermediateField/k))
        ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) σ :
          Gal(↥L'.toIntermediateField/k))
        y) :
    K) =
  (↑y : K)
Tactic: apply Subtype.val_injective
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Infinite (hypothesis)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
H : ClosedSubgroup Gal(K/k)
inst_3 : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField (↑H : Subgroup Gal(K/k))).fixingSubgroup
h : σ ∉ (↑H : Subgroup Gal(K/k))
b : Set Gal(K/k)
sub : b ⊆ (fun (y : Gal(K/k)) ↦ σ * y) ⁻¹' (↑H : Subgroup Gal(K/k)).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq : (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) L.fixingSubgroup = b
hL : Membership.mem (γ := Set (IntermediateField k K)) (finiteExts k K) L
eq' : L.fixingSubgroup = gp
this : FiniteDimensional.{u_1, u_2} k ↥L
L' : FiniteGaloisIntermediateField k K :=
  let __src : IntermediateField k K := normalClosure k (↥L) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
compl : σ • L'.fixingSubgroup.carrier ⊆ (↑H : Subgroup Gal(K/k)).carrierᶜ
fix :
  ∀ (x : K),
    Membership.mem (γ := IntermediateField k K)
        (lift (F := L'.toIntermediateField)
          (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) (↑H : Subgroup Gal(K/k)))))
        x →
      (σ : (a : K) → K) x = x
⊢ False
have this₁ : Membership.mem (α := Gal(↥L'.toIntermediateField/k)) (γ := Subgroup Gal(↥L'.toIntermediateField/k))
  (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) (↑H : Subgroup Gal(K/k)))
  ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) σ :
    Gal(↥L'.toIntermediateField/k))
Tactic: have : (restrictNormalHom L') σ ∈ (Subgroup.map (restrictNormalHom L') H.1) := by
    rw [← IntermediateField.fixingSubgroup_fixedField (Subgroup.map (restrictNormalHom L') H.1)]
    apply (mem_fixingSubgroup_iff (L' ≃ₐ[k] L')).mpr
    intro y hy
    apply Subtype.val_injective
    simp only [AlgEquiv.smul_def, restrictNormalHom_apply L'.1 σ y,
      fix y.1 ((IntermediateField.mem_lift y).mpr hy)]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Infinite (goal)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
H : ClosedSubgroup Gal(K/k)
inst_3 : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField (↑H : Subgroup Gal(K/k))).fixingSubgroup
h : σ ∉ (↑H : Subgroup Gal(K/k))
b : Set Gal(K/k)
sub : b ⊆ (fun (y : Gal(K/k)) ↦ σ * y) ⁻¹' (↑H : Subgroup Gal(K/k)).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq : (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) L.fixingSubgroup = b
hL : Membership.mem (γ := Set (IntermediateField k K)) (finiteExts k K) L
eq' : L.fixingSubgroup = gp
this_1 : FiniteDimensional.{u_1, u_2} k ↥L
L' : FiniteGaloisIntermediateField k K :=
  let __src : IntermediateField k K := normalClosure k (↥L) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
compl : σ • L'.fixingSubgroup.carrier ⊆ (↑H : Subgroup Gal(K/k)).carrierᶜ
fix :
  ∀ (x : K),
    Membership.mem (γ := IntermediateField k K)
        (lift (F := L'.toIntermediateField)
          (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) (↑H : Subgroup Gal(K/k)))))
        x →
      (σ : (a : K) → K) x = x
this :
  Membership.mem (α := Gal(↥L'.toIntermediateField/k)) (γ := Subgroup Gal(↥L'.toIntermediateField/k))
    (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) (↑H : Subgroup Gal(K/k)))
    ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) σ :
      Gal(↥L'.toIntermediateField/k))
⊢ False
have rcases : ∀ (h : Gal(K/k)) (mem : h ∈ (↑(↑H : Subgroup Gal(K/k)) : Set Gal(K/k)))
  (eq :
    Eq (α := Gal(↥L'.toIntermediateField/k))
      ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) h :
        Gal(↥L'.toIntermediateField/k))
      ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) σ :
        Gal(↥L'.toIntermediateField/k))),
  False
Tactic: rcases this with ⟨h, mem, eq⟩
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Infinite (goal)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
H : ClosedSubgroup Gal(K/k)
inst_3 : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField (↑H : Subgroup Gal(K/k))).fixingSubgroup
h_1 : σ ∉ (↑H : Subgroup Gal(K/k))
b : Set Gal(K/k)
sub : b ⊆ (fun (y : Gal(K/k)) ↦ σ * y) ⁻¹' (↑H : Subgroup Gal(K/k)).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq_1 : (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) L.fixingSubgroup = b
hL : Membership.mem (γ := Set (IntermediateField k K)) (finiteExts k K) L
eq' : L.fixingSubgroup = gp
this : FiniteDimensional.{u_1, u_2} k ↥L
L' : FiniteGaloisIntermediateField k K :=
  let __src : IntermediateField k K := normalClosure k (↥L) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
compl : σ • L'.fixingSubgroup.carrier ⊆ (↑H : Subgroup Gal(K/k)).carrierᶜ
fix :
  ∀ (x : K),
    Membership.mem (γ := IntermediateField k K)
        (lift (F := L'.toIntermediateField)
          (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) (↑H : Subgroup Gal(K/k)))))
        x →
      (σ : (a : K) → K) x = x
h : Gal(K/k)
mem : h ∈ (↑(↑H : Subgroup Gal(K/k)) : Set Gal(K/k))
eq :
  Eq (α := Gal(↥L'.toIntermediateField/k))
    ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) h :
      Gal(↥L'.toIntermediateField/k))
    ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) σ :
      Gal(↥L'.toIntermediateField/k))
⊢ h ∈ σ • L'.fixingSubgroup.carrier
have h₁ : σ⁻¹ * h ∈ L'.fixingSubgroup.carrier ∧ (fun (x : Gal(K/k)) ↦ σ • x) (σ⁻¹ * h) = h
Tactic: use σ⁻¹ * h
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Infinite (goal)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
H : ClosedSubgroup Gal(K/k)
inst_3 : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField (↑H : Subgroup Gal(K/k))).fixingSubgroup
h_1 : σ ∉ (↑H : Subgroup Gal(K/k))
b : Set Gal(K/k)
sub : b ⊆ (fun (y : Gal(K/k)) ↦ σ * y) ⁻¹' (↑H : Subgroup Gal(K/k)).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq_1 : (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) L.fixingSubgroup = b
hL : Membership.mem (γ := Set (IntermediateField k K)) (finiteExts k K) L
eq' : L.fixingSubgroup = gp
this : FiniteDimensional.{u_1, u_2} k ↥L
L' : FiniteGaloisIntermediateField k K :=
  let __src : IntermediateField k K := normalClosure k (↥L) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
compl : σ • L'.fixingSubgroup.carrier ⊆ (↑H : Subgroup Gal(K/k)).carrierᶜ
fix :
  ∀ (x : K),
    Membership.mem (γ := IntermediateField k K)
        (lift (F := L'.toIntermediateField)
          (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) (↑H : Subgroup Gal(K/k)))))
        x →
      (σ : (a : K) → K) x = x
h : Gal(K/k)
mem : h ∈ (↑(↑H : Subgroup Gal(K/k)) : Set Gal(K/k))
eq :
  Eq (α := Gal(↥L'.toIntermediateField/k))
    ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) h :
      Gal(↥L'.toIntermediateField/k))
    ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) σ :
      Gal(↥L'.toIntermediateField/k))
⊢ σ⁻¹ * h ∈ L'.fixingSubgroup.carrier ∧ (fun (x : Gal(K/k)) ↦ σ • x) (σ⁻¹ * h) = h
have h₁ : σ⁻¹ * h ∈ L'.fixingSubgroup
Tactic: simp only [Subsemigroup.mem_carrier, Submonoid.mem_toSubsemigroup, Subgroup.mem_toSubmonoid,
      smul_eq_mul, mul_inv_cancel_left, and_true]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Infinite (goal)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
H : ClosedSubgroup Gal(K/k)
inst_3 : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField (↑H : Subgroup Gal(K/k))).fixingSubgroup
h_1 : σ ∉ (↑H : Subgroup Gal(K/k))
b : Set Gal(K/k)
sub : b ⊆ (fun (y : Gal(K/k)) ↦ σ * y) ⁻¹' (↑H : Subgroup Gal(K/k)).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq_1 : (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) L.fixingSubgroup = b
hL : Membership.mem (γ := Set (IntermediateField k K)) (finiteExts k K) L
eq' : L.fixingSubgroup = gp
this : FiniteDimensional.{u_1, u_2} k ↥L
L' : FiniteGaloisIntermediateField k K :=
  let __src : IntermediateField k K := normalClosure k (↥L) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
compl : σ • L'.fixingSubgroup.carrier ⊆ (↑H : Subgroup Gal(K/k)).carrierᶜ
fix :
  ∀ (x : K),
    Membership.mem (γ := IntermediateField k K)
        (lift (F := L'.toIntermediateField)
          (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) (↑H : Subgroup Gal(K/k)))))
        x →
      (σ : (a : K) → K) x = x
h : Gal(K/k)
mem : h ∈ (↑(↑H : Subgroup Gal(K/k)) : Set Gal(K/k))
eq :
  Eq (α := Gal(↥L'.toIntermediateField/k))
    ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) h :
      Gal(↥L'.toIntermediateField/k))
    ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) σ :
      Gal(↥L'.toIntermediateField/k))
⊢ σ⁻¹ * h ∈ L'.fixingSubgroup
have h₁ : ∀ y ∈ (↑L'.toIntermediateField : Set K), (σ⁻¹ * h) • y = y
Tactic: apply (mem_fixingSubgroup_iff Gal(K/k)).mpr
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Infinite (goal)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
H : ClosedSubgroup Gal(K/k)
inst_3 : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField (↑H : Subgroup Gal(K/k))).fixingSubgroup
h_1 : σ ∉ (↑H : Subgroup Gal(K/k))
b : Set Gal(K/k)
sub : b ⊆ (fun (y : Gal(K/k)) ↦ σ * y) ⁻¹' (↑H : Subgroup Gal(K/k)).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq_1 : (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) L.fixingSubgroup = b
hL : Membership.mem (γ := Set (IntermediateField k K)) (finiteExts k K) L
eq' : L.fixingSubgroup = gp
this : FiniteDimensional.{u_1, u_2} k ↥L
L' : FiniteGaloisIntermediateField k K :=
  let __src : IntermediateField k K := normalClosure k (↥L) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
compl : σ • L'.fixingSubgroup.carrier ⊆ (↑H : Subgroup Gal(K/k)).carrierᶜ
fix :
  ∀ (x : K),
    Membership.mem (γ := IntermediateField k K)
        (lift (F := L'.toIntermediateField)
          (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) (↑H : Subgroup Gal(K/k)))))
        x →
      (σ : (a : K) → K) x = x
h : Gal(K/k)
mem : h ∈ (↑(↑H : Subgroup Gal(K/k)) : Set Gal(K/k))
eq :
  Eq (α := Gal(↥L'.toIntermediateField/k))
    ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) h :
      Gal(↥L'.toIntermediateField/k))
    ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) σ :
      Gal(↥L'.toIntermediateField/k))
y : K
hy : y ∈ (↑L'.toIntermediateField : Set K)
⊢ (σ⁻¹ * h) • y = y
have h₁ : (σ⁻¹ : (a : K) → K) ((h : (a : K) → K) y : K) = y
Tactic: simp only [AlgEquiv.smul_def, AlgEquiv.mul_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Infinite (goal)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
H : ClosedSubgroup Gal(K/k)
inst_3 : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField (↑H : Subgroup Gal(K/k))).fixingSubgroup
h_1 : σ ∉ (↑H : Subgroup Gal(K/k))
b : Set Gal(K/k)
sub : b ⊆ (fun (y : Gal(K/k)) ↦ σ * y) ⁻¹' (↑H : Subgroup Gal(K/k)).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq_1 : (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) L.fixingSubgroup = b
hL : Membership.mem (γ := Set (IntermediateField k K)) (finiteExts k K) L
eq' : L.fixingSubgroup = gp
this : FiniteDimensional.{u_1, u_2} k ↥L
L' : FiniteGaloisIntermediateField k K :=
  let __src : IntermediateField k K := normalClosure k (↥L) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
compl : σ • L'.fixingSubgroup.carrier ⊆ (↑H : Subgroup Gal(K/k)).carrierᶜ
fix :
  ∀ (x : K),
    Membership.mem (γ := IntermediateField k K)
        (lift (F := L'.toIntermediateField)
          (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) (↑H : Subgroup Gal(K/k)))))
        x →
      (σ : (a : K) → K) x = x
h : Gal(K/k)
mem : h ∈ (↑(↑H : Subgroup Gal(K/k)) : Set Gal(K/k))
eq :
  Eq (α := Gal(↥L'.toIntermediateField/k))
    ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) h :
      Gal(↥L'.toIntermediateField/k))
    ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) σ :
      Gal(↥L'.toIntermediateField/k))
y : K
hy : y ∈ (↑L'.toIntermediateField : Set K)
⊢ Eq.{u_2 + 1} (α := K)
    (↑((((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) h :
              Gal(↥L'.toIntermediateField/k)) :
            (a : ↥L'.toIntermediateField) → ↥L'.toIntermediateField)
          (Subtype.mk (p := fun (x : K) ↦ x ∈ L'.toIntermediateField) y hy)) :
      K)
    (↑((((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) σ :
              Gal(↥L'.toIntermediateField/k)) :
            (a : ↥L'.toIntermediateField) → ↥L'.toIntermediateField)
          (Subtype.mk (p := fun (x : K) ↦ x ∈ L'.toIntermediateField) y hy)) :
      K)
have rw : Eq.{u_2 + 1} (α := K)
  (↑((((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) σ :
            Gal(↥L'.toIntermediateField/k)) :
          (a : ↥L'.toIntermediateField) → ↥L'.toIntermediateField)
        (Subtype.mk (p := fun (x : K) ↦ x ∈ L'.toIntermediateField) y hy)) :
    K)
  (↑((((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) σ :
            Gal(↥L'.toIntermediateField/k)) :
          (a : ↥L'.toIntermediateField) → ↥L'.toIntermediateField)
        (Subtype.mk (p := fun (x : K) ↦ x ∈ L'.toIntermediateField) y hy)) :
    K)
Tactic: rw [eq]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Infinite (hypothesis)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
H : ClosedSubgroup Gal(K/k)
inst_3 : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField (↑H : Subgroup Gal(K/k))).fixingSubgroup
h_1 : σ ∉ (↑H : Subgroup Gal(K/k))
b : Set Gal(K/k)
sub : b ⊆ (fun (y : Gal(K/k)) ↦ σ * y) ⁻¹' (↑H : Subgroup Gal(K/k)).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq_1 : (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) L.fixingSubgroup = b
hL : Membership.mem (γ := Set (IntermediateField k K)) (finiteExts k K) L
eq' : L.fixingSubgroup = gp
this : FiniteDimensional.{u_1, u_2} k ↥L
L' : FiniteGaloisIntermediateField k K :=
  let __src : IntermediateField k K := normalClosure k (↥L) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
compl : σ • L'.fixingSubgroup.carrier ⊆ (↑H : Subgroup Gal(K/k)).carrierᶜ
fix :
  ∀ (x : K),
    Membership.mem (γ := IntermediateField k K)
        (lift (F := L'.toIntermediateField)
          (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) (↑H : Subgroup Gal(K/k)))))
        x →
      (σ : (a : K) → K) x = x
h : Gal(K/k)
mem : h ∈ (↑(↑H : Subgroup Gal(K/k)) : Set Gal(K/k))
eq :
  Eq (α := Gal(↥L'.toIntermediateField/k))
    ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) h :
      Gal(↥L'.toIntermediateField/k))
    ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) σ :
      Gal(↥L'.toIntermediateField/k))
y : K
hy : y ∈ (↑L'.toIntermediateField : Set K)
⊢ (σ⁻¹ : (a : K) → K) ((h : (a : K) → K) y : K) = y
have this₁ : Eq.{u_2 + 1} (α := K)
  (↑((((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) h :
            Gal(↥L'.toIntermediateField/k)) :
          (a : ↥L'.toIntermediateField) → ↥L'.toIntermediateField)
        (Subtype.mk (p := fun (x : K) ↦ x ∈ L'.toIntermediateField) y hy)) :
    K)
  (↑((((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) σ :
            Gal(↥L'.toIntermediateField/k)) :
          (a : ↥L'.toIntermediateField) → ↥L'.toIntermediateField)
        (Subtype.mk (p := fun (x : K) ↦ x ∈ L'.toIntermediateField) y hy)) :
    K)
Tactic: have : ((restrictNormalHom L') h ⟨y,hy⟩).1 = ((restrictNormalHom L') σ ⟨y,hy⟩).1 := by rw [eq]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Infinite (hypothesis)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
H : ClosedSubgroup Gal(K/k)
inst_3 : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField (↑H : Subgroup Gal(K/k))).fixingSubgroup
h_1 : σ ∉ (↑H : Subgroup Gal(K/k))
b : Set Gal(K/k)
sub : b ⊆ (fun (y : Gal(K/k)) ↦ σ * y) ⁻¹' (↑H : Subgroup Gal(K/k)).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq_1 : (fun (g : Subgroup Gal(K/k)) ↦ g.carrier) L.fixingSubgroup = b
hL : Membership.mem (γ := Set (IntermediateField k K)) (finiteExts k K) L
eq' : L.fixingSubgroup = gp
this_1 : FiniteDimensional.{u_1, u_2} k ↥L
L' : FiniteGaloisIntermediateField k K :=
  let __src : IntermediateField k K := normalClosure k (↥L) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
compl : σ • L'.fixingSubgroup.carrier ⊆ (↑H : Subgroup Gal(K/k)).carrierᶜ
fix :
  ∀ (x : K),
    Membership.mem (γ := IntermediateField k K)
        (lift (F := L'.toIntermediateField)
          (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) (↑H : Subgroup Gal(K/k)))))
        x →
      (σ : (a : K) → K) x = x
h : Gal(K/k)
mem : h ∈ (↑(↑H : Subgroup Gal(K/k)) : Set Gal(K/k))
eq :
  Eq (α := Gal(↥L'.toIntermediateField/k))
    ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) h :
      Gal(↥L'.toIntermediateField/k))
    ((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) σ :
      Gal(↥L'.toIntermediateField/k))
y : K
hy : y ∈ (↑L'.toIntermediateField : Set K)
this :
  Eq.{u_2 + 1} (α := K)
    (↑((((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) h :
              Gal(↥L'.toIntermediateField/k)) :
            (a : ↥L'.toIntermediateField) → ↥L'.toIntermediateField)
          (Subtype.mk (p := fun (x : K) ↦ x ∈ L'.toIntermediateField) y hy)) :
      K)
    (↑((((restrictNormalHom ↥L'.toIntermediateField : (a : Gal(K/k)) → Gal(↥L'.toIntermediateField/k)) σ :
              Gal(↥L'.toIntermediateField/k)) :
            (a : ↥L'.toIntermediateField) → ↥L'.toIntermediateField)
          (Subtype.mk (p := fun (x : K) ↦ x ∈ L'.toIntermediateField) y hy)) :
      K)
⊢ (σ⁻¹ : (a : K) → K) ((h : (a : K) → K) y : K) = y
have this₁ : Eq (α := K) ((h : (a : K) → K) (↑(Subtype.mk (p := fun (x : K) ↦ x ∈ L'.toIntermediateField) y hy) : K) : K)
  ((σ : (a : K) → K) (↑(Subtype.mk (p := fun (x : K) ↦ x ∈ L'.toIntermediateField) y hy) : K) : K)
Tactic: rw [restrictNormalHom_apply L'.1 h ⟨y, hy⟩, restrictNormalHom_apply L'.1 σ ⟨y, hy⟩] at this
Cleared hypotheses: this