-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Luroth (goal)
Goal:
K : Type u_1
inst : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ HMul.hMul (α := K⟮X⟯[X]) (β := K⟮X⟯[X])
        ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X]) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E)) : K⟮X⟯[X])
        (Polynomial.map
          (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥E) K⟮X⟯)
              (↑(inclusion ⋯) : ↥K⟮generator E⟯ →+* ↥E))
            (algebraMap K ↥K⟮generator E⟯))
          (generator E).num) -
      HMul.hMul (α := K⟮X⟯[X]) (β := K⟮X⟯[X])
        ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X])
            (HMul.hMul (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E) : K⟮X⟯)
              (↑(Subtype.mk (p := fun (x : K⟮X⟯) ↦
                    Membership.mem (γ := Subalgebra K K⟮X⟯)
                      K[HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯)
                          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (generator E).num : K⟮X⟯)
                          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (generator E).denom : K⟮X⟯)]
                      x)
                    (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯)
                      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (generator E).num : K⟮X⟯)
                      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (generator E).denom : K⟮X⟯))
                    ⋯) :
                K⟮X⟯)) :
          K⟮X⟯[X])
        (Polynomial.map
          (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥E) K⟮X⟯)
              (↑(inclusion ⋯) : ↥K⟮generator E⟯ →+* ↥E))
            (algebraMap K ↥K⟮generator E⟯))
          (generator E).denom) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)
have rw : HMul.hMul (α := K⟮X⟯[X]) (β := K⟮X⟯[X])
      ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X]) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E)) : K⟮X⟯[X])
      (Polynomial.map
        (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
          (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥E) K⟮X⟯)
            (↑(inclusion sorry) : ↥K⟮generator E⟯ →+* ↥E))
          (algebraMap K ↥K⟮generator E⟯))
        (generator E).num) -
    HMul.hMul (α := K⟮X⟯[X]) (β := K⟮X⟯[X])
      ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X]) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (generator E).num) : K⟮X⟯[X])
      (Polynomial.map
        (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
          (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥E) K⟮X⟯)
            (↑(inclusion sorry) : ↥K⟮generator E⟯ →+* ↥E))
          (algebraMap K ↥K⟮generator E⟯))
        (generator E).denom) =
  HMul.hMul (α := K⟮X⟯[X]) (β := K⟮X⟯[X])
      ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X]) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (g E)) : K⟮X⟯[X])
      (Polynomial.map (RingHom.comp (algebraMap K[X] K⟮X⟯) Polynomial.C) (f E)) -
    HMul.hMul (α := K⟮X⟯[X]) (β := K⟮X⟯[X])
      ((Polynomial.C : (a : K⟮X⟯) → K⟮X⟯[X]) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (f E)) : K⟮X⟯[X])
      (Polynomial.map (RingHom.comp (algebraMap K[X] K⟮X⟯) Polynomial.C) (g E))
Tactic: rw [mul_div_cancel₀ _ (algebraMap_ne_zero (generator E).denom_ne_zero), Polynomial.map_sub,
    Polynomial.map_mul, Polynomial.map_mul, map_C, map_C, Polynomial.map_map, Polynomial.map_map]