-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
Goal:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Type u_3
B : Type u_4
FRS : Type u_5
FAB : Type u_6
inst_3 : CommRing S
inst_4 : CommRing B
inst_5 : Algebra S B
inst_6 : FunLike FRS R S
inst_7 : RingHomClass FRS R S
inst_8 : FunLike FAB A B
inst_9 : RingHomClass FAB A B
f : FRS
g : FAB
H :
  ∀ (p : MvPolynomial ι S),
    Eq.{u_4 + 1} (α := B) ((aeval ((⇑g : (a : A) → B) ∘ x) : (a : MvPolynomial ι S) → B) p : B) (0 : B) → p = 0
hf : Injective.{u_2 + 1, u_3 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h :
  Eq (α := R →+* B) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S B) (↑f : R →+* S))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : A →+* B) (algebraMap R A))
p : MvPolynomial ι R
hp : Eq.{v + 1} (α := A) ((aeval x : (a : MvPolynomial ι R) → A) p : A) (0 : A)
this :
  Eq.{u_4 + 1} (α := B) (((↑g : A →+* B) : (a : A) → B) ((aeval x : (a : MvPolynomial ι R) → A) p) : B)
    ((g : (a : A) → B) 0 : B)
rwa :
  ∀
    (this :
      Eq.{u_4 + 1} (α := B) (((↑g : A →+* B) : (a : A) → B) ((aeval x : (a : MvPolynomial ι R) → A) p) : B) (0 : B)),
    Eq.{u_4 + 1} (α := B)
      ((aeval ((⇑g : (a : A) → B) ∘ x) : (a : MvPolynomial ι S) → B)
          ((MvPolynomial.map (↑f : R →+* S) : (a : MvPolynomial ι R) → MvPolynomial ι S) p : MvPolynomial ι S) :
        B)
      (0 : B)
rwa₁ :
  ∀
    (this :
      Eq.{u_4 + 1} (α := B)
        ((eval₂Hom (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : A →+* B) (algebraMap R A)) fun (i : ι) ↦
                ((↑g : A →+* B) : (a : A) → B) (x i) :
              (a : MvPolynomial ι R) → B)
            p :
          B)
        (0 : B)),
    Eq.{u_4 + 1} (α := B)
      ((aeval ((⇑g : (a : A) → B) ∘ x) : (a : MvPolynomial ι S) → B)
          ((MvPolynomial.map (↑f : R →+* S) : (a : MvPolynomial ι R) → MvPolynomial ι S) p : MvPolynomial ι S) :
        B)
      (0 : B)
rwa₂ :
  ∀
    (this :
      Eq.{u_4 + 1} (α := B)
        ((eval₂Hom (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S B) (↑f : R →+* S)) fun (i : ι) ↦
                ((↑g : A →+* B) : (a : A) → B) (x i) :
              (a : MvPolynomial ι R) → B)
            p :
          B)
        (0 : B)),
    Eq.{u_4 + 1} (α := B)
      ((aeval ((⇑g : (a : A) → B) ∘ x) : (a : MvPolynomial ι S) → B)
          ((MvPolynomial.map (↑f : R →+* S) : (a : MvPolynomial ι R) → MvPolynomial ι S) p : MvPolynomial ι S) :
        B)
      (0 : B)
⊢ Eq.{u_4 + 1} (α := B)
    ((aeval ((⇑g : (a : A) → B) ∘ x) : (a : MvPolynomial ι S) → B)
        ((MvPolynomial.map (↑f : R →+* S) : (a : MvPolynomial ι R) → MvPolynomial ι S) p : MvPolynomial ι S) :
      B)
    (0 : B)
have rwa₃ : ∀
  (this :
    Eq.{u_4 + 1} (α := B)
      ((eval₂Hom (algebraMap S B) fun (i : ι) ↦ ((↑g : A →+* B) : (a : A) → B) (x i) : (a : MvPolynomial ι S) → B)
          ((MvPolynomial.map (↑f : R →+* S) : (a : MvPolynomial ι R) → MvPolynomial ι S) p : MvPolynomial ι S) :
        B)
      (0 : B)),
  Eq.{u_4 + 1} (α := B)
    ((aeval ((⇑g : (a : A) → B) ∘ x) : (a : MvPolynomial ι S) → B)
        ((MvPolynomial.map (↑f : R →+* S) : (a : MvPolynomial ι R) → MvPolynomial ι S) p : MvPolynomial ι S) :
      B)
    (0 : B)
Tactic: rwa [map_zero, map_aeval, ← h, ← eval₂Hom_map_hom, ← aeval_eq_eval₂Hom] at this
Cleared hypotheses: this