Theorem: Interface.Subscheme.invEqType (Runtime/Interface.lean)

State before:
σ₁ σ₂ : Scheme
a : σ₁.vars
inst : Subscheme σ₁ σ₂
b✝ : σ₂.vars
h : inv b✝ = some a
⊢ Scheme.type σ₁ a = Scheme.type σ₂ b✝
Tactic:
rw [←inst.coeEqType (v := a), inst.invInj h (inst.coeInvId a)]
State after:
no goals