k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
h✝ : E₁ ≤ E₂
h : ∃ h, ∀ (x : { x // x ∈ E₁.carrier }), ↑E₂.emb (↑(inclusion h) x) = ↑E₁.emb x
⊢ ∀ (x : { x // x ∈ E₁.carrier }), ↑E₂.emb (↑(inclusion (_ : E₁.carrier ≤ E₂.carrier)) x) = ↑E₁.emb x
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
h : E₁ ≤ E₂
⊢ ∀ (x : { x // x ∈ E₁.carrier }), ↑E₂.emb (↑(inclusion (_ : E₁.carrier ≤ E₂.carrier)) x) = ↑E₁.emb x
rw [le_def] at h
case intro
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
h : E₁ ≤ E₂
w✝ : E₁.carrier ≤ E₂.carrier
h✝ : ∀ (x : { x // x ∈ E₁.carrier }), ↑E₂.emb (↑(inclusion w✝) x) = ↑E₁.emb x
⊢ ∀ (x : { x // x ∈ E₁.carrier }), ↑E₂.emb (↑(inclusion (_ : E₁.carrier ≤ E₂.carrier)) x) = ↑E₁.emb x
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
h✝ : E₁ ≤ E₂
h : ∃ h, ∀ (x : { x // x ∈ E₁.carrier }), ↑E₂.emb (↑(inclusion h) x) = ↑E₁.emb x
⊢ ∀ (x : { x // x ∈ E₁.carrier }), ↑E₂.emb (↑(inclusion (_ : E₁.carrier ≤ E₂.carrier)) x) = ↑E₁.emb x
cases h
no goals
case intro
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
h : E₁ ≤ E₂
w✝ : E₁.carrier ≤ E₂.carrier
h✝ : ∀ (x : { x // x ∈ E₁.carrier }), ↑E₂.emb (↑(inclusion w✝) x) = ↑E₁.emb x
⊢ ∀ (x : { x // x ∈ E₁.carrier }), ↑E₂.emb (↑(inclusion (_ : E₁.carrier ≤ E₂.carrier)) x) = ↑E₁.emb x
assumption