-- Mathlib/FieldTheory/Galois/Profinite.lean
lemma proj_of_le (L : FiniteGaloisIntermediateField k K)
    (g : limit (asProfiniteGaloisGroupFunctor k K)) (x : L)
    (L' : FiniteGaloisIntermediateField k K) (h : L ≤ L') :
    (proj L g x).val = (proj L' g ⟨x, h x.2⟩).val

Proof state:
case mk.mk
k : Type u_3
K : Type u_4
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
g : ↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
L : IntermediateField k K
finiteDimensional✝¹ : FiniteDimensional k ↥L
isGalois✝¹ : IsGalois k ↥L
x : ↥(FiniteGaloisIntermediateField.mk L).toIntermediateField
L' : IntermediateField k K
finiteDimensional✝ : FiniteDimensional k ↥L'
isGalois✝ : IsGalois k ↥L'
h : FiniteGaloisIntermediateField.mk L ≤ FiniteGaloisIntermediateField.mk L'
this✝ : Algebra ↥L ↥L' := (Subsemiring.inclusion h).toAlgebra
this : IsScalarTower k ↥L ↥L' := IsScalarTower.of_algebraMap_eq (congrFun rfl)
⊢ (algebraMap (↥L') K) ((algebraMap ↥L ↥L') ((((proj (FiniteGaloisIntermediateField.mk L')) g).restrictNormal ↥L) x)) =
    ↑(((proj (FiniteGaloisIntermediateField.mk L')) g) ⟨↑x, ⋯⟩)

Tactic:
rw [AlgEquiv.restrictNormal_commutes (proj (mk L') g) L]

Result:
case mk.mk
k : Type u_3
K : Type u_4
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
g : ↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
L : IntermediateField k K
finiteDimensional✝¹ : FiniteDimensional k ↥L
isGalois✝¹ : IsGalois k ↥L
x : ↥(FiniteGaloisIntermediateField.mk L).toIntermediateField
L' : IntermediateField k K
finiteDimensional✝ : FiniteDimensional k ↥L'
isGalois✝ : IsGalois k ↥L'
h : FiniteGaloisIntermediateField.mk L ≤ FiniteGaloisIntermediateField.mk L'
this✝ : Algebra ↥L ↥L' := (Subsemiring.inclusion h).toAlgebra
this : IsScalarTower k ↥L ↥L' := IsScalarTower.of_algebraMap_eq (congrFun rfl)
⊢ (algebraMap (↥L') K)
      (((proj (FiniteGaloisIntermediateField.mk L')) g)
        ((algebraMap ↥L ↥(FiniteGaloisIntermediateField.mk L').toIntermediateField) x)) =
    ↑(((proj (FiniteGaloisIntermediateField.mk L')) g) ⟨↑x, ⋯⟩)

Proof state:
case mk.mk
k : Type u_3
K : Type u_4
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
g : ↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
L : IntermediateField k K
finiteDimensional✝¹ : FiniteDimensional k ↥L
isGalois✝¹ : IsGalois k ↥L
x : ↥(FiniteGaloisIntermediateField.mk L).toIntermediateField
L' : IntermediateField k K
finiteDimensional✝ : FiniteDimensional k ↥L'
isGalois✝ : IsGalois k ↥L'
h : FiniteGaloisIntermediateField.mk L ≤ FiniteGaloisIntermediateField.mk L'
this✝ : Algebra ↥L ↥L' := (Subsemiring.inclusion h).toAlgebra
this : IsScalarTower k ↥L ↥L' := IsScalarTower.of_algebraMap_eq (congrFun rfl)
⊢ ↑(((ConcreteCategory.hom ((finGaloisGroupFunctor k K).map h.hom.op)) ((proj (FiniteGaloisIntermediateField.mk L')) g))
        x) =
    ↑(((proj (FiniteGaloisIntermediateField.mk L')) g) ⟨↑x, ⋯⟩)

Tactic:
show (algebraMap L' K (algebraMap L L' (AlgEquiv.restrictNormal (proj (mk L') g) L x))) = _

Result:
case mk.mk
k : Type u_3
K : Type u_4
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
g : ↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
L : IntermediateField k K
finiteDimensional✝¹ : FiniteDimensional k ↥L
isGalois✝¹ : IsGalois k ↥L
x : ↥(FiniteGaloisIntermediateField.mk L).toIntermediateField
L' : IntermediateField k K
finiteDimensional✝ : FiniteDimensional k ↥L'
isGalois✝ : IsGalois k ↥L'
h : FiniteGaloisIntermediateField.mk L ≤ FiniteGaloisIntermediateField.mk L'
this✝ : Algebra ↥L ↥L' := (Subsemiring.inclusion h).toAlgebra
this : IsScalarTower k ↥L ↥L' := IsScalarTower.of_algebraMap_eq (congrFun rfl)
⊢ (algebraMap (↥L') K) ((algebraMap ↥L ↥L') ((((proj (FiniteGaloisIntermediateField.mk L')) g).restrictNormal ↥L) x)) =
    ↑(((proj (FiniteGaloisIntermediateField.mk L')) g) ⟨↑x, ⋯⟩)

Proof state:
case mk.mk
k : Type u_3
K : Type u_4
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
g : ↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
L : IntermediateField k K
finiteDimensional✝¹ : FiniteDimensional k ↥L
isGalois✝¹ : IsGalois k ↥L
x : ↥(FiniteGaloisIntermediateField.mk L).toIntermediateField
L' : IntermediateField k K
finiteDimensional✝ : FiniteDimensional k ↥L'
isGalois✝ : IsGalois k ↥L'
h : FiniteGaloisIntermediateField.mk L ≤ FiniteGaloisIntermediateField.mk L'
this✝ : Algebra ↥L ↥L' := (Subsemiring.inclusion h).toAlgebra
this : IsScalarTower k ↥L ↥L' := IsScalarTower.of_algebraMap_eq (congrFun rfl)
⊢ (algebraMap (↥L') K)
      (((proj (FiniteGaloisIntermediateField.mk L')) g)
        ((algebraMap ↥L ↥(FiniteGaloisIntermediateField.mk L').toIntermediateField) x)) =
    ↑(((proj (FiniteGaloisIntermediateField.mk L')) g) ⟨↑x, ⋯⟩)

Tactic:
rfl

Result:
no goals

Proof state:
case mk.mk
k : Type u_3
K : Type u_4
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
g : ↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
L : IntermediateField k K
finiteDimensional✝¹ : FiniteDimensional k ↥L
isGalois✝¹ : IsGalois k ↥L
x : ↥(FiniteGaloisIntermediateField.mk L).toIntermediateField
L' : IntermediateField k K
finiteDimensional✝ : FiniteDimensional k ↥L'
isGalois✝ : IsGalois k ↥L'
h : FiniteGaloisIntermediateField.mk L ≤ FiniteGaloisIntermediateField.mk L'
this✝ : Algebra ↥L ↥L' := (Subsemiring.inclusion h).toAlgebra
this : IsScalarTower k ↥L ↥L' := IsScalarTower.of_algebraMap_eq (congrFun rfl)
⊢ ↑(((proj (FiniteGaloisIntermediateField.mk L)) g) x) = ↑(((proj (FiniteGaloisIntermediateField.mk L')) g) ⟨↑x, ⋯⟩)

Tactic:
rw [← finGaloisGroupFunctor_map_proj_eq_proj g h.hom]

Result:
case mk.mk
k : Type u_3
K : Type u_4
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
g : ↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
L : IntermediateField k K
finiteDimensional✝¹ : FiniteDimensional k ↥L
isGalois✝¹ : IsGalois k ↥L
x : ↥(FiniteGaloisIntermediateField.mk L).toIntermediateField
L' : IntermediateField k K
finiteDimensional✝ : FiniteDimensional k ↥L'
isGalois✝ : IsGalois k ↥L'
h : FiniteGaloisIntermediateField.mk L ≤ FiniteGaloisIntermediateField.mk L'
this✝ : Algebra ↥L ↥L' := (Subsemiring.inclusion h).toAlgebra
this : IsScalarTower k ↥L ↥L' := IsScalarTower.of_algebraMap_eq (congrFun rfl)
⊢ ↑(((ConcreteCategory.hom ((finGaloisGroupFunctor k K).map h.hom.op)) ((proj (FiniteGaloisIntermediateField.mk L')) g))
        x) =
    ↑(((proj (FiniteGaloisIntermediateField.mk L')) g) ⟨↑x, ⋯⟩)

Proof state:
case mk.mk
k : Type u_3
K : Type u_4
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
g : ↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
L : IntermediateField k K
finiteDimensional✝¹ : FiniteDimensional k ↥L
isGalois✝¹ : IsGalois k ↥L
x : ↥(FiniteGaloisIntermediateField.mk L).toIntermediateField
L' : IntermediateField k K
finiteDimensional✝ : FiniteDimensional k ↥L'
isGalois✝ : IsGalois k ↥L'
h : FiniteGaloisIntermediateField.mk L ≤ FiniteGaloisIntermediateField.mk L'
⊢ ↑(((proj (FiniteGaloisIntermediateField.mk L)) g) x) = ↑(((proj (FiniteGaloisIntermediateField.mk L')) g) ⟨↑x, ⋯⟩)

Tactic:
letI : Algebra L L' := RingHom.toAlgebra (Subsemiring.inclusion h)

Result:
case mk.mk
k : Type u_3
K : Type u_4
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
g : ↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
L : IntermediateField k K
finiteDimensional✝¹ : FiniteDimensional k ↥L
isGalois✝¹ : IsGalois k ↥L
x : ↥(FiniteGaloisIntermediateField.mk L).toIntermediateField
L' : IntermediateField k K
finiteDimensional✝ : FiniteDimensional k ↥L'
isGalois✝ : IsGalois k ↥L'
h : FiniteGaloisIntermediateField.mk L ≤ FiniteGaloisIntermediateField.mk L'
this : Algebra ↥L ↥L' := (Subsemiring.inclusion h).toAlgebra
⊢ ↑(((proj (FiniteGaloisIntermediateField.mk L)) g) x) = ↑(((proj (FiniteGaloisIntermediateField.mk L')) g) ⟨↑x, ⋯⟩)