-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
r : R
hf : f ≠ 0
hg : g ≠ 0
inr :
  ∀ (R : Type u_1) [inst : Field R] (f : R[X]) (hf' : f.Splits) (g : R[X]) (r : R) (hf : f ≠ 0) (hg : g ≠ 0),
    (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree =
      r ^ (f.natDegree * g.natDegree) * f.resultant g
inr₁ :
  ∀ (R S : Type u_1) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S)
    (hφ : Function.Injective (α := R) (β := S) (⇑φ : (a : R) → S)) (f : R[X])
    (IH :
      ∀ (g : S[X]) (r : S) (hf : map φ f ≠ 0) (hg : g ≠ 0),
        ((map φ f).scaleRoots r).resultant (g.scaleRoots r) (map φ f).natDegree g.natDegree =
          r ^ ((map φ f).natDegree * g.natDegree) * (map φ f).resultant g)
    (g : R[X]) (r : R) (hf : f ≠ 0) (hg : g ≠ 0),
    (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree =
      r ^ (f.natDegree * g.natDegree) * f.resultant g
⊢ (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g
have inr₂ : ∀ (R S : Type u_1) [inst : CommRing R] [inst_1 : CommRing S] (φ : R →+* S)
  (hφ : Function.Surjective (α := R) (β := S) (⇑φ : (a : R) → S)) (f : S[X])
  (IH :
    ∀ (q g : R[X]) (r : R) (hf : q ≠ 0) (hg : g ≠ 0),
      (q.scaleRoots r).resultant (g.scaleRoots r) q.natDegree g.natDegree =
        r ^ (q.natDegree * g.natDegree) * q.resultant g)
  (g : S[X]) (r : S) (hf : f ≠ 0) (hg : g ≠ 0),
  (f.scaleRoots r).resultant (g.scaleRoots r) f.natDegree g.natDegree = r ^ (f.natDegree * g.natDegree) * f.resultant g
Tactic: induction f using induction_of_Splits_of_injective_of_surjective with
  | Splits R f hf' =>
    by_cases hf0 : f.natDegree = 0
    · obtain ⟨a, rfl⟩ := natDegree_eq_zero.mp hf0; simp
    by_cases hg0 : g.natDegree = 0
    · obtain ⟨a, rfl⟩ := natDegree_eq_zero.mp hg0; simp
    obtain rfl | hr := eq_or_ne r 0
    · rw [scaleRoots_zero, scaleRoots_zero, Algebra.smul_def, Algebra.smul_def]
      simp [resultant_C_mul_right, resultant_X_pow_right, *, (Ne.symm hf0)]
    conv_lhs => rw [← natDegree_scaleRoots f r, ← natDegree_scaleRoots g r]
    rw [resultant_eq_prod_eval _ _ _ le_rfl hf',
      resultant_eq_prod_eval _ _ _ le_rfl (hf'.scaleRoots _),
      roots_scaleRoots _ (isUnit_iff_ne_zero.mpr hr)]
    simp only [Multiset.map_map, Function.comp_def, scaleRoots_eval_mul]
    simp only [leadingCoeff_scaleRoots, natDegree_scaleRoots, Multiset.prod_map_mul,
      Multiset.map_const', Multiset.prod_replicate, ← hf'.natDegree_eq_card_roots]
    ring
  | injective R S φ hφ f IH =>
    have := IH (g.map φ) (φ r) (by simpa using (map_injective _ hφ).ne hf)
      (by simpa using (map_injective _ hφ).ne hg)
    apply hφ
    rw [← map_scaleRoots, ← map_scaleRoots] at this
    · simpa [natDegree_map_eq_of_injective hφ] using this
    all_goals simpa [map_eq_zero_iff _ hφ]
  | surjective R S φ hφ f IH =>
    obtain ⟨f', hf', ef⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ f)
    obtain ⟨g', hg', eg⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ g)
    obtain ⟨r, rfl⟩ := hφ r
    have hfl : f.leadingCoeff = φ f'.leadingCoeff := by
      simp_rw [← coeff_natDegree, ← natDegree_eq_natDegree ef, ← hf', coeff_map]
    have hgl : g.leadingCoeff = φ g'.leadingCoeff := by
      simp_rw [← coeff_natDegree, ← natDegree_eq_natDegree eg, ← hg', coeff_map]
    rw [← hf', ← map_scaleRoots _ _ _ (by simpa [← hfl]), ← hg',
      ← map_scaleRoots _ _ _ (by simpa [← hgl]), hf', hg',
      ← natDegree_eq_natDegree ef, ← natDegree_eq_natDegree eg,
      resultant_map_map, IH f' g' r (by aesop) (by aesop)]
    rw [← hf', ← hg', resultant_map_map]
    simp
Cleared hypotheses: f, g, r, hf, hg