-- Mathlib/FieldTheory/Galois/Infinite.lean
/-- For a subgroup `H` of `Gal(K/k)`, the fixed field of the image of `H` under the restriction to
a normal intermediate field `E` is equal to the fixed field of `H` in `K` intersecting with `E`. -/
lemma restrict_fixedField (H : Subgroup (K ≃ₐ[k] K)) (L : IntermediateField k K) [Normal k L] :
    fixedField H ⊓ L = lift (fixedField (Subgroup.map (restrictNormalHom L) H))

Proof state:
case h.h.refine_2
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : Subgroup (K ≃ₐ[k] K)
L : IntermediateField k K
inst✝ : Normal k ↥L
x : K
xL : x ∈ L
h : ∀ a ∈ H, ((restrictNormalHom ↥L) a) ⟨x, xL⟩ = ⟨x, xL⟩
σ : K ≃ₐ[k] K
hσ : σ ∈ H
this : ↑(((restrictNormalHom ↥L) σ) ⟨x, xL⟩) = x
⊢ σ x = x

Tactic:
nth_rw 2 [← this]

Result:
case h.h.refine_2
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : Subgroup (K ≃ₐ[k] K)
L : IntermediateField k K
inst✝ : Normal k ↥L
x : K
xL : x ∈ L
h : ∀ a ∈ H, ((restrictNormalHom ↥L) a) ⟨x, xL⟩ = ⟨x, xL⟩
σ : K ≃ₐ[k] K
hσ : σ ∈ H
this : ↑(((restrictNormalHom ↥L) σ) ⟨x, xL⟩) = x
⊢ σ x = ↑(((restrictNormalHom ↥L) σ) ⟨x, xL⟩)

Proof state:
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : Subgroup (K ≃ₐ[k] K)
L : IntermediateField k K
inst✝ : Normal k ↥L
⊢ fixedField H ⊓ L = lift (fixedField (Subgroup.map (restrictNormalHom ↥L) H))

Tactic:
apply SetLike.ext'

Result:
case h
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : Subgroup (K ≃ₐ[k] K)
L : IntermediateField k K
inst✝ : Normal k ↥L
⊢ ↑(fixedField H ⊓ L) = ↑(lift (fixedField (Subgroup.map (restrictNormalHom ↥L) H)))

Proof state:
case h.h.refine_1
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : Subgroup (K ≃ₐ[k] K)
L : IntermediateField k K
inst✝ : Normal k ↥L
x : K
h : x ∈ ↑(fixedField H ⊓ L)
xL : x ∈ (fun x => ↑x) L
⊢ ⟨x, xL⟩ ∈ fixedField (Subgroup.map (restrictNormalHom ↥L) H)

Tactic:
simp only [mem_fixedField_iff, Subgroup.mem_map, forall_exists_index, and_imp,
  forall_apply_eq_imp_iff₂]

Result:
case h.h.refine_1
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : Subgroup (K ≃ₐ[k] K)
L : IntermediateField k K
inst✝ : Normal k ↥L
x : K
h : x ∈ ↑(fixedField H ⊓ L)
xL : x ∈ (fun x => ↑x) L
⊢ ∀ a ∈ H, ((restrictNormalHom ↥L) a) ⟨x, xL⟩ = ⟨x, xL⟩

Proof state:
case h.h.refine_2
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : Subgroup (K ≃ₐ[k] K)
L : IntermediateField k K
inst✝ : Normal k ↥L
x : K
h : x ∈ ↑(lift (fixedField (Subgroup.map (restrictNormalHom ↥L) H)))
xL : x ∈ L
⊢ x ∈ ↑(fixedField H ⊓ L)

Tactic:
apply (mem_lift (⟨x, xL⟩ : L)).mp at h

Result:
case h.h.refine_2
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : Subgroup (K ≃ₐ[k] K)
L : IntermediateField k K
inst✝ : Normal k ↥L
x : K
xL : x ∈ L
h : ⟨x, xL⟩ ∈ fixedField (Subgroup.map (restrictNormalHom ↥L) H)
⊢ x ∈ ↑(fixedField H ⊓ L)

Proof state:
case h
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : Subgroup (K ≃ₐ[k] K)
L : IntermediateField k K
inst✝ : Normal k ↥L
⊢ ↑(fixedField H ⊓ L) = ↑(lift (fixedField (Subgroup.map (restrictNormalHom ↥L) H)))

Tactic:
ext x

Result:
case h.h
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : Subgroup (K ≃ₐ[k] K)
L : IntermediateField k K
inst✝ : Normal k ↥L
x : K
⊢ x ∈ ↑(fixedField H ⊓ L) ↔ x ∈ ↑(lift (fixedField (Subgroup.map (restrictNormalHom ↥L) H)))

Proof state:
case h.h.refine_1.a
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : Subgroup (K ≃ₐ[k] K)
L : IntermediateField k K
inst✝ : Normal k ↥L
x : K
h : x ∈ ↑(fixedField H ⊓ L)
xL : x ∈ (fun x => ↑x) L
σ : K ≃ₐ[k] K
hσ : σ ∈ H
⊢ ↑(((restrictNormalHom ↥L) σ) ⟨x, xL⟩) = x

Tactic:
nth_rw 2 [← (h.out.1 ⟨σ, hσ⟩)]

Result:
case h.h.refine_1.a
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : Subgroup (K ≃ₐ[k] K)
L : IntermediateField k K
inst✝ : Normal k ↥L
x : K
h : x ∈ ↑(fixedField H ⊓ L)
xL : x ∈ (fun x => ↑x) L
σ : K ≃ₐ[k] K
hσ : σ ∈ H
⊢ ↑(((restrictNormalHom ↥L) σ) ⟨x, xL⟩) = ⟨σ, hσ⟩ • x

Proof state:
case h.h.refine_2
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : Subgroup (K ≃ₐ[k] K)
L : IntermediateField k K
inst✝ : Normal k ↥L
x : K
xL : x ∈ L
h : ∀ a ∈ H, ((restrictNormalHom ↥L) a) ⟨x, xL⟩ = ⟨x, xL⟩
σ : K ≃ₐ[k] K
hσ : σ ∈ H
⊢ σ x = x

Tactic:
have : ((restrictNormalHom L σ) ⟨x, xL⟩).1 = x := by rw [h σ hσ]

Result:
case h.h.refine_2
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : Subgroup (K ≃ₐ[k] K)
L : IntermediateField k K
inst✝ : Normal k ↥L
x : K
xL : x ∈ L
h : ∀ a ∈ H, ((restrictNormalHom ↥L) a) ⟨x, xL⟩ = ⟨x, xL⟩
σ : K ≃ₐ[k] K
hσ : σ ∈ H
this : ↑(((restrictNormalHom ↥L) σ) ⟨x, xL⟩) = x
⊢ σ x = x

Proof state:
case h.h.refine_2
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : Subgroup (K ≃ₐ[k] K)
L : IntermediateField k K
inst✝ : Normal k ↥L
x : K
xL : x ∈ L
h : ∀ a ∈ H, ((restrictNormalHom ↥L) a) ⟨x, xL⟩ = ⟨x, xL⟩
⊢ ∀ f ∈ H, f x = x

Tactic:
intro σ hσ

Result:
case h.h.refine_2
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : Subgroup (K ≃ₐ[k] K)
L : IntermediateField k K
inst✝ : Normal k ↥L
x : K
xL : x ∈ L
h : ∀ a ∈ H, ((restrictNormalHom ↥L) a) ⟨x, xL⟩ = ⟨x, xL⟩
σ : K ≃ₐ[k] K
hσ : σ ∈ H
⊢ σ x = x