awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (hypothesis)
Goal:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
K : Type u_3
inst_3 : CommRing K
inst_4 : Algebra R K
inst_5 : Algebra K A
inst_6 : IsScalarTower R K A
hinj : Injective.{u_2 + 1, u_3 + 1} (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K)
ai : AlgebraicIndependent K x
⊢ AlgebraicIndependent R x
have this : Eq (α := MvPolynomial ι R →+* A)
  (RingHom.comp (β := MvPolynomial ι K) (AlgHom.toRingHom (aeval x)) (MvPolynomial.map (algebraMap R K)))
  (AlgHom.toRingHom (aeval x))
Tactic: have : (aeval x : MvPolynomial ι K →ₐ[K] A).toRingHom.comp (MvPolynomial.map (algebraMap R K)) =
      (aeval x : MvPolynomial ι R →ₐ[R] A).toRingHom := by
    ext <;> simp [algebraMap_eq_smul_one]
-- 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
K : Type u_3
inst_3 : CommRing K
inst_4 : Algebra R K
inst_5 : Algebra K A
inst_6 : IsScalarTower R K A
hinj : Injective.{u_2 + 1, u_3 + 1} (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K)
ai : AlgebraicIndependent K x
this :
  Eq (α := MvPolynomial ι R →+* A)
    (RingHom.comp (β := MvPolynomial ι K) (AlgHom.toRingHom (aeval x)) (MvPolynomial.map (algebraMap R K)))
    (AlgHom.toRingHom (aeval x))
⊢ AlgebraicIndependent R x
have change : Injective (α := MvPolynomial ι R) (β := A) (⇑(AlgHom.toRingHom (aeval x)) : (a : MvPolynomial ι R) → A)
Tactic: change Injective (aeval x).toRingHom
-- 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
K : Type u_3
inst_3 : CommRing K
inst_4 : Algebra R K
inst_5 : Algebra K A
inst_6 : IsScalarTower R K A
hinj : Injective.{u_2 + 1, u_3 + 1} (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K)
ai : AlgebraicIndependent K x
this :
  Eq (α := MvPolynomial ι R →+* A)
    (RingHom.comp (β := MvPolynomial ι K) (AlgHom.toRingHom (aeval x)) (MvPolynomial.map (algebraMap R K)))
    (AlgHom.toRingHom (aeval x))
⊢ Injective (α := MvPolynomial ι R) (β := A) (⇑(AlgHom.toRingHom (aeval x)) : (a : MvPolynomial ι R) → A)
have rw : Injective (α := MvPolynomial ι R) (β := A)
  (Function.comp (β := MvPolynomial ι K) (⇑(AlgHom.toRingHom (aeval x)) : (a : MvPolynomial ι K) → A)
    (⇑(MvPolynomial.map (algebraMap R K)) : (a : MvPolynomial ι R) → MvPolynomial ι K))
Tactic: rw [← this, RingHom.coe_comp]
-- 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 : AlgebraicIndependent.{u, u_3, u_4} S (A := B) ((⇑g : (a : A) → B) ∘ x)
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))
⊢ AlgebraicIndependent R x
have rw : ∀
  (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), Eq.{v + 1} (α := A) ((aeval x : (a : MvPolynomial ι R) → A) p : A) (0 : A) → p = 0
Tactic: rw [algebraicIndependent_iff] at H ⊢
Cleared hypotheses: H, hf, h
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (hypothesis)
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)
⊢ 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 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)
Tactic: have : (g : A →+* B) _ = _ := congr(g $hp)
-- 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)
⊢ 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) (((↑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)
Tactic: rwa [map_zero, map_aeval, ← h, ← eval₂Hom_map_hom, ← aeval_eq_eval₂Hom] at this
Cleared hypotheses: this
-- 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)
⊢ 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 (@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)
Tactic: rwa [map_zero, map_aeval, ← h, ← eval₂Hom_map_hom, ← aeval_eq_eval₂Hom] at this
Cleared hypotheses: this
-- 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)
⊢ 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 (@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)
Tactic: rwa [map_zero, map_aeval, ← h, ← eval₂Hom_map_hom, ← aeval_eq_eval₂Hom] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (hypothesis)
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)
⊢ p = 0
have this : Eq (α := MvPolynomial ι S)
  ((MvPolynomial.map (↑f : R →+* S) : (a : MvPolynomial ι R) → MvPolynomial ι S) p : MvPolynomial ι S)
  (0 : MvPolynomial ι S)
Tactic: have := H (p.map f) <| by
    have : (g : A →+* B) _ = _ := congr(g $hp)
    rwa [map_zero, map_aeval, ← h, ← eval₂Hom_map_hom, ← aeval_eq_eval₂Hom] at this
-- 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 : AlgebraicIndependent R x
hf : Surjective.{u_2 + 1, u_3 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
hg : Injective.{v + 1, u_4 + 1} (α := A) (β := B) (⇑g : (a : A) → B)
h :
  Eq (α := R →+* B) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S B) (↑f : R →+* S))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : A →+* B) (algebraMap R A))
⊢ AlgebraicIndependent.{u, u_3, u_4} S (A := B) ((⇑g : (a : A) → B) ∘ x)
have rw : ∀ (H : ∀ (p : MvPolynomial ι R), Eq.{v + 1} (α := A) ((aeval x : (a : MvPolynomial ι R) → A) p : A) (0 : A) → p = 0)
  (hf : Surjective.{u_2 + 1, u_3 + 1} (α := R) (β := S) (⇑f : (a : R) → S))
  (hg : Injective.{v + 1, u_4 + 1} (α := A) (β := B) (⇑g : (a : A) → B))
  (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 ι S),
  Eq.{u_4 + 1} (α := B) ((aeval ((⇑g : (a : A) → B) ∘ x) : (a : MvPolynomial ι S) → B) p : B) (0 : B) → p = 0
Tactic: rw [algebraicIndependent_iff] at H ⊢
Cleared hypotheses: H, hf, hg, h
-- 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 ι R), Eq.{v + 1} (α := A) ((aeval x : (a : MvPolynomial ι R) → A) p : A) (0 : A) → p = 0
hf : Surjective.{u_2 + 1, u_3 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
hg : Injective.{v + 1, u_4 + 1} (α := A) (β := B) (⇑g : (a : A) → B)
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 ι S
hp : Eq.{u_4 + 1} (α := B) ((aeval ((⇑g : (a : A) → B) ∘ x) : (a : MvPolynomial ι S) → B) p : B) (0 : B)
⊢ p = 0
have obtain : ∀ (q : MvPolynomial ι R)
  (hp :
    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) q : MvPolynomial ι S) :
        B)
      (0 : B)),
  Eq (α := MvPolynomial ι S)
    ((MvPolynomial.map (↑f : R →+* S) : (a : MvPolynomial ι R) → MvPolynomial ι S) q : MvPolynomial ι S)
    (0 : MvPolynomial ι S)
Tactic: obtain ⟨q, rfl⟩ := map_surjective (f : R →+* S) hf p
Cleared hypotheses: p, hp
-- 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 ι R), Eq.{v + 1} (α := A) ((aeval x : (a : MvPolynomial ι R) → A) p : A) (0 : A) → p = 0
hf : Surjective.{u_2 + 1, u_3 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
hg : Injective.{v + 1, u_4 + 1} (α := A) (β := B) (⇑g : (a : A) → B)
h :
  Eq (α := R →+* B) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S B) (↑f : R →+* S))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : A →+* B) (algebraMap R A))
q : MvPolynomial ι R
hp :
  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) q : MvPolynomial ι S) :
      B)
    (0 : B)
⊢ Eq.{u_4 + 1} (α := B) ((g : (a : A) → B) ((aeval x : (a : MvPolynomial ι R) → A) q : A) : B) ((g : (a : A) → B) 0 : B)
have rwa : Eq.{u_4 + 1} (α := B) ((g : (a : A) → B) ((aeval x : (a : MvPolynomial ι R) → A) q : A) : B) (0 : B)
Tactic: rwa [map_zero, ← RingHom.coe_coe g, map_aeval, ← h, ← eval₂Hom_map_hom,
    ← aeval_eq_eval₂Hom]
-- 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 ι R), Eq.{v + 1} (α := A) ((aeval x : (a : MvPolynomial ι R) → A) p : A) (0 : A) → p = 0
hf : Surjective.{u_2 + 1, u_3 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
hg : Injective.{v + 1, u_4 + 1} (α := A) (β := B) (⇑g : (a : A) → B)
h :
  Eq (α := R →+* B) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S B) (↑f : R →+* S))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : A →+* B) (algebraMap R A))
q : MvPolynomial ι R
hp :
  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) q : MvPolynomial ι S) :
      B)
    (0 : B)
rwa : Eq.{u_4 + 1} (α := B) ((g : (a : A) → B) ((aeval x : (a : MvPolynomial ι R) → A) q : A) : B) (0 : B)
⊢ Eq.{u_4 + 1} (α := B) ((g : (a : A) → B) ((aeval x : (a : MvPolynomial ι R) → A) q : A) : B) ((g : (a : A) → B) 0 : B)
have rwa₁ : Eq.{u_4 + 1} (α := B) (((↑g : A →+* B) : (a : A) → B) ((aeval x : (a : MvPolynomial ι R) → A) q : A) : B) (0 : B)
Tactic: rwa [map_zero, ← RingHom.coe_coe g, map_aeval, ← h, ← eval₂Hom_map_hom,
    ← aeval_eq_eval₂Hom]
-- 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 ι R), Eq.{v + 1} (α := A) ((aeval x : (a : MvPolynomial ι R) → A) p : A) (0 : A) → p = 0
hf : Surjective.{u_2 + 1, u_3 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
hg : Injective.{v + 1, u_4 + 1} (α := A) (β := B) (⇑g : (a : A) → B)
h :
  Eq (α := R →+* B) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S B) (↑f : R →+* S))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : A →+* B) (algebraMap R A))
q : MvPolynomial ι R
hp :
  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) q : MvPolynomial ι S) :
      B)
    (0 : B)
rwa : Eq.{u_4 + 1} (α := B) ((g : (a : A) → B) ((aeval x : (a : MvPolynomial ι R) → A) q : A) : B) (0 : B)
rwa₁ : Eq.{u_4 + 1} (α := B) (((↑g : A →+* B) : (a : A) → B) ((aeval x : (a : MvPolynomial ι R) → A) q : A) : B) (0 : B)
⊢ Eq.{u_4 + 1} (α := B) ((g : (a : A) → B) ((aeval x : (a : MvPolynomial ι R) → A) q : A) : B) ((g : (a : A) → B) 0 : B)
have rwa₂ : 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)
      q :
    B)
  (0 : B)
Tactic: rwa [map_zero, ← RingHom.coe_coe g, map_aeval, ← h, ← eval₂Hom_map_hom,
    ← aeval_eq_eval₂Hom]
-- 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 ι R), Eq.{v + 1} (α := A) ((aeval x : (a : MvPolynomial ι R) → A) p : A) (0 : A) → p = 0
hf : Surjective.{u_2 + 1, u_3 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
hg : Injective.{v + 1, u_4 + 1} (α := A) (β := B) (⇑g : (a : A) → B)
h :
  Eq (α := R →+* B) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S B) (↑f : R →+* S))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : A →+* B) (algebraMap R A))
q : MvPolynomial ι R
hp :
  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) q : MvPolynomial ι S) :
      B)
    (0 : B)
rwa : Eq.{u_4 + 1} (α := B) ((g : (a : A) → B) ((aeval x : (a : MvPolynomial ι R) → A) q : A) : B) (0 : B)
rwa₁ : Eq.{u_4 + 1} (α := B) (((↑g : A →+* B) : (a : A) → B) ((aeval x : (a : MvPolynomial ι R) → A) q : A) : B) (0 : B)
rwa₂ :
  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)
        q :
      B)
    (0 : B)
⊢ Eq.{u_4 + 1} (α := B) ((g : (a : A) → B) ((aeval x : (a : MvPolynomial ι R) → A) q : A) : B) ((g : (a : A) → B) 0 : B)
have rwa₃ : 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)
      q :
    B)
  (0 : B)
Tactic: rwa [map_zero, ← RingHom.coe_coe g, map_aeval, ← h, ← eval₂Hom_map_hom,
    ← aeval_eq_eval₂Hom]