-- 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 ≠ ⊥
this :
  natDegree.{u_1} (R := K[X])
      ((Bivariate.swap : (a : K[X][Y]) → K[X][Y])
        (Polynomial.map Polynomial.C ((Polynomial.C : (a : K) → K[X]) (Q₃ h)) * Φ E)) =
    natDegree.{u_1} (R := K[X]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (θ E))
rwa :
  ∀
    (this :
      (HMul.hMul (α := K[X][Y]) (β := K[X][Y])
            ((Bivariate.swap : (a : K[X][Y]) → K[X][Y])
                (Polynomial.map Polynomial.C ((Polynomial.C : (a : K) → K[X]) (Q₃ h))) :
              K[X][Y])
            ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Φ E) : K[X][Y])).natDegree =
        natDegree.{u_1} (R := K[X]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (θ E))),
    natDegree.{u_1} (R := K[X]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Φ E)) = (θ E).natDegree
rwa₁ :
  ∀
    (this :
      (HMul.hMul (α := K[X][Y]) (β := K[X][Y])
            ((Bivariate.swap : (a : K[X][Y]) → K[X][Y])
                ((Polynomial.C : (a : K[X]) → K[X][Y]) ((Polynomial.C : (a : K) → K[X]) (Q₃ h))) :
              K[X][Y])
            ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Φ E) : K[X][Y])).natDegree =
        natDegree.{u_1} (R := K[X]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (θ E))),
    natDegree.{u_1} (R := K[X]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Φ E)) = (θ E).natDegree
rwa₂ :
  ∀
    (this :
      (HMul.hMul (α := K[X][Y]) (β := K[X][Y])
            ((Polynomial.C : (a : K[X]) → K[X][Y]) ((Polynomial.C : (a : K) → K[X]) (Q₃ h)) : K[X][Y])
            ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Φ E) : K[X][Y])).natDegree =
        natDegree.{u_1} (R := K[X]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (θ E))),
    natDegree.{u_1} (R := K[X]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Φ E)) = (θ E).natDegree
rwa₃ :
  ∀
    (this :
      natDegree.{u_1} (R := K[X]) ((Polynomial.C : (a : K[X]) → K[X][Y]) ((Polynomial.C : (a : K) → K[X]) (Q₃ h))) +
          natDegree.{u_1} (R := K[X]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Φ E)) =
        natDegree.{u_1} (R := K[X]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (θ E))),
    natDegree.{u_1} (R := K[X]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Φ E)) = (θ E).natDegree
rwa₄ :
  ∀
    (this :
      0 + natDegree.{u_1} (R := K[X]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Φ E)) =
        natDegree.{u_1} (R := K[X]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (θ E))),
    natDegree.{u_1} (R := K[X]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Φ E)) = (θ E).natDegree
⊢ natDegree.{u_1} (R := K[X]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Φ E)) = (θ E).natDegree
have rwa₅ : ∀
  (this :
    natDegree.{u_1} (R := K[X]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Φ E)) =
      natDegree.{u_1} (R := K[X]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (θ E))),
  natDegree.{u_1} (R := K[X]) ((Bivariate.swap : (a : K[X][Y]) → K[X][Y]) (Φ E)) = (θ E).natDegree
Tactic: rwa [map_mul, Polynomial.map_C, Bivariate.swap_C_C,
    natDegree_mul (C_ne_zero.mpr (Q₃_map h ▸ Q₂_ne_zero h))
      ((map_ne_zero_iff _ Bivariate.swap.injective).mpr (Φ_ne_zero h)),
    natDegree_C, zero_add, swap_θ, natDegree_neg] at this
Cleared hypotheses: this