-- 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:
k : Type u_3
K : Type u_4
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
L : FiniteGaloisIntermediateField k K
g : ↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
x : ↥L.toIntermediateField
L' : FiniteGaloisIntermediateField k K
h : L ≤ L'
⊢ ↑(((proj L) g) x) = ↑(((proj L') g) ⟨↑x, ⋯⟩)

Tactic:
induction L with | _ L => ?_

Result:
case 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' : FiniteGaloisIntermediateField k K
L : IntermediateField k K
finiteDimensional✝ : FiniteDimensional k ↥L
isGalois✝ : IsGalois k ↥L
x : ↥(FiniteGaloisIntermediateField.mk L).toIntermediateField
h : FiniteGaloisIntermediateField.mk L ≤ L'
⊢ ↑(((proj (FiniteGaloisIntermediateField.mk L)) g) x) = ↑(((proj 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
⊢ ↑(((proj (FiniteGaloisIntermediateField.mk L)) g) x) = ↑(((proj (FiniteGaloisIntermediateField.mk L')) g) ⟨↑x, ⋯⟩)

Tactic:
letI : IsScalarTower k L L' := IsScalarTower.of_algebraMap_eq (congrFun rfl)

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)
⊢ ↑(((proj (FiniteGaloisIntermediateField.mk L)) g) x) = ↑(((proj (FiniteGaloisIntermediateField.mk L')) g) ⟨↑x, ⋯⟩)

Proof state:
case 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' : FiniteGaloisIntermediateField k K
L : IntermediateField k K
finiteDimensional✝ : FiniteDimensional k ↥L
isGalois✝ : IsGalois k ↥L
x : ↥(FiniteGaloisIntermediateField.mk L).toIntermediateField
h : FiniteGaloisIntermediateField.mk L ≤ L'
⊢ ↑(((proj (FiniteGaloisIntermediateField.mk L)) g) x) = ↑(((proj L') g) ⟨↑x, ⋯⟩)

Tactic:
induction L' with | _ 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'
⊢ ↑(((proj (FiniteGaloisIntermediateField.mk L)) g) x) = ↑(((proj (FiniteGaloisIntermediateField.mk L')) g) ⟨↑x, ⋯⟩)