-- Module: Mathlib.FieldTheory.RatFunc.Luroth
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
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
rwa₆ :
  ∀ (this : 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
rwa₇ rwa₈ rwa₉ rwa₁₀ :
  ∀ (this : 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
⊢ 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

Premises used: Iff.mpr, Polynomial.natDegree_mul, Polynomial.natDegree_C, zero_add, Polynomial.Bivariate.swap_C_C, map_mul, Polynomial.Bivariate.swap, AlgEquiv.injective, map_ne_zero_iff, Polynomial.natDegree_neg, Polynomial.map_C, _private.0.RatFunc.Luroth.swap_θ, _private.0.RatFunc.Luroth.Φ_ne_zero, Polynomial.C_ne_zero