-- 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_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 ∈ ↑(lift (fixedField (Subgroup.map (restrictNormalHom ↥L) H)))

Tactic:
apply (mem_lift (⟨x, xL⟩ : L)).mpr

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
⊢ ⟨x, xL⟩ ∈ fixedField (Subgroup.map (restrictNormalHom ↥L) H)

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
x : K
xL : x ∈ L
h : ∀ a ∈ H, ((restrictNormalHom ↥L) a) ⟨x, xL⟩ = ⟨x, xL⟩
σ : K ≃ₐ[k] K
hσ : σ ∈ H
⊢ ↑(((restrictNormalHom ↥L) σ) ⟨x, xL⟩) = x

Tactic:
rw [h σ hσ]

Result:
no goals

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⟩) = ⟨σ, hσ⟩ • x

Tactic:
exact AlgEquiv.restrictNormal_commutes σ L ⟨x, xL⟩

Result:
no goals

Proof state:
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)))

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

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)
⊢ x ∈ ↑(lift (fixedField (Subgroup.map (restrictNormalHom ↥L) H)))

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)))
⊢ x ∈ ↑(fixedField H ⊓ L)

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)))
⊢ x ∈ ↑(fixedField H ⊓ L)

Tactic:
have xL := lift_le _ 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
h : x ∈ ↑(lift (fixedField (Subgroup.map (restrictNormalHom ↥L) H)))
xL : x ∈ L
⊢ x ∈ ↑(fixedField H ⊓ L)

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)
⊢ x ∈ ↑(lift (fixedField (Subgroup.map (restrictNormalHom ↥L) H)))

Tactic:
have xL := h.out.2

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
⊢ x ∈ ↑(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 = ↑(((restrictNormalHom ↥L) σ) ⟨x, xL⟩)

Tactic:
exact (AlgEquiv.restrictNormal_commutes σ L ⟨x, xL⟩).symm

Result:
no goals

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⟩
⊢ x ∈ ↑(fixedField H ⊓ L)

Tactic:
simp only [coe_inf, Set.mem_inter_iff, SetLike.mem_coe, mem_fixedField_iff, xL, and_true]

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⟩
⊢ ∀ f ∈ H, f x = x

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
σ : K ≃ₐ[k] K
hσ : σ ∈ H
⊢ ((restrictNormalHom ↥L) σ) ⟨x, xL⟩ = ⟨x, xL⟩

Tactic:
apply Subtype.val_injective

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⟩) = ↑⟨x, xL⟩

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, xL⟩

Tactic:
dsimp only

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⟩) = 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 : ⟨x, xL⟩ ∈ fixedField (Subgroup.map (restrictNormalHom ↥L) H)
⊢ x ∈ ↑(fixedField H ⊓ L)

Tactic:
simp only [mem_fixedField_iff, Subgroup.mem_map, forall_exists_index, and_imp,
  forall_apply_eq_imp_iff₂] 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 : ∀ a ∈ H, ((restrictNormalHom ↥L) a) ⟨x, xL⟩ = ⟨x, xL⟩
⊢ x ∈ ↑(fixedField H ⊓ L)

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
⊢ ∀ a ∈ H, ((restrictNormalHom ↥L) a) ⟨x, xL⟩ = ⟨x, xL⟩

Tactic:
intro σ hσ

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
σ : K ≃ₐ[k] K
hσ : σ ∈ H
⊢ ((restrictNormalHom ↥L) σ) ⟨x, xL⟩ = ⟨x, xL⟩