case h.e'_6
R : Type u
S : Type ?u.153899
A : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Ring A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R S
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
B : Type u_1
inst✝¹ : Ring B
inst✝ : Algebra R B
e : A ≃ₐ[R] B
h : Algebra.IsAlgebraic R A
b : B
⊢ ↑↑e ?m.156705 = b

R : Type u
S : Type ?u.153899
A : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Ring A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R S
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
B : Type u_1
inst✝¹ : Ring B
inst✝ : Algebra R B
e : A ≃ₐ[R] B
h : Algebra.IsAlgebraic R A
b : B
⊢ A
R : Type u
S : Type ?u.153899
A : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Ring A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R S
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
B : Type u_1
inst✝¹ : Ring B
inst✝ : Algebra R B
e : A ≃ₐ[R] B
h : Algebra.IsAlgebraic R A
b : B
⊢ IsAlgebraic R b
convert← isAlgebraic_algHom_of_isAlgebraic e.toAlgHom (h _)
no goals
case h.e'_6
R : Type u
S : Type ?u.153899
A : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Ring A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R S
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
B : Type u_1
inst✝¹ : Ring B
inst✝ : Algebra R B
e : A ≃ₐ[R] B
h : Algebra.IsAlgebraic R A
b : B
⊢ ↑↑e ?m.156705 = b

R : Type u
S : Type ?u.153899
A : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Ring A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R S
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
B : Type u_1
inst✝¹ : Ring B
inst✝ : Algebra R B
e : A ≃ₐ[R] B
h : Algebra.IsAlgebraic R A
b : B
⊢ A
refine e.apply_symm_apply ?_