awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
ι : Type u
R : Type u_2
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Subsingleton R
x : ι → A
this : Subsingleton A
⊢ IsTranscendenceBasis R x ↔ Nonempty ι

Tactic:
⟨fun h ↦ ?_, fun h ↦ ⟨.of_subsingleton, fun s hs hx ↦
    hx.antisymm fun a _ ↦ ⟨Classical.arbitrary _, Subsingleton.elim ..⟩⟩⟩

Premises used: HasSubset.Subset.antisymm, And.intro, Iff.intro, Exists.intro, Classical.arbitrary, AlgebraicIndependent.of_subsingleton, Subsingleton.elim
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
ι : Type u
R : Type u_2
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Subsingleton R
x : ι → A
this : Subsingleton A
refine : ∀ (h : IsTranscendenceBasis R x), Nonempty ι
⊢ IsTranscendenceBasis R x ↔ Nonempty ι

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ⟨.of_subsingleton, fun s hs hx ↦
    hx.antisymm fun a _ ↦ ⟨Classical.arbitrary _, Subsingleton.elim ..⟩⟩⟩
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
ι : Type u
R : Type u_2
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Subsingleton R
x : ι → A
this : Subsingleton A
h : IsTranscendenceBasis R x
by_contra! : ∀ (hι : IsEmpty ι), False
⊢ Nonempty ι

Tactic:
by_contra! hι
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
ι : Type u
R : Type u_2
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Subsingleton R
x : ι → A
this : Subsingleton A
h : IsTranscendenceBasis R x
hι : IsEmpty ι
⊢ range x ⊆ {0} → range x = {0}

Tactic:
have := h.2 {0} .of_subsingleton
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
ι : Type u
R : Type u_2
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Subsingleton R
x : ι → A
this_1 : Subsingleton A
h : IsTranscendenceBasis R x
hι : IsEmpty ι
this : range x ⊆ {0} → range x = {0}
⊢ False

Tactic:
simp [range_eq_empty, eq_comm (a := ∅)] at this

Premises used: eq_comm, Set.range_eq_empty
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Subsingleton R
inst_4 : Nonempty ι
⊢ IsTranscendenceBasis R x

Tactic:
(isTranscendenceBasis_iff_of_subsingleton x).mpr ‹_›

Premises used: Iff.mpr, isTranscendenceBasis_iff_of_subsingleton
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
R : Type u_2
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Subsingleton R
this : Subsingleton A
s : { s : Set A // AlgebraicIndepOn R _root_.id s }
⊢ Cardinal.mk (↑(↑s : Set A) : Type v) ≤ 1

Tactic:
simpa using Set.subsingleton_of_subsingleton

Premises used: Set.subsingleton_of_subsingleton
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
R : Type u_2
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Subsingleton R
this : Subsingleton A
⊢ 1 ≤ Cardinal.mk (↑(↑(Subtype.mk (p := fun (s : Set A) ↦ AlgebraicIndepOn R _root_.id s) {0} ⋯) : Set A) : Type v)

Tactic:
simp
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hs : AlgebraicIndependent R x
⊢ AlgebraicIndependent.{u, u_2, v} R (A := ↥(adjoin R (range x))) fun (i : ι) ↦
    Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R (range x)) x_1) (x i) ⋯

Tactic:
AlgebraicIndependent.of_comp (adjoin R (range x)).val hs

Premises used: Subalgebra.val, Algebra.adjoin, Set.range, AlgebraicIndependent.of_comp
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
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
hC :
  ∀ (x_1 : R),
    Eq.{v + 1} (α := A)
      ((RingHom.comp
              (RingHom.comp (β := MvPolynomial ι K) (AlgHom.toRingHom (aeval x)) (MvPolynomial.map (algebraMap R K)))
              C :
            (a : R) → A)
          x_1 :
        A)
      ((RingHom.comp (AlgHom.toRingHom (aeval x)) C : (a : R) → A) x_1 : A)
hX :
  ∀ (i : ι),
    Eq.{v + 1} (α := A)
      ((RingHom.comp (β := MvPolynomial ι K) (AlgHom.toRingHom (aeval x)) (MvPolynomial.map (algebraMap R K)) :
            (a : MvPolynomial ι R) → A)
          (X i) :
        A)
      ((AlgHom.toRingHom (aeval x) : (a : MvPolynomial ι R) → A) (X i) : A)
⊢ Eq (α := MvPolynomial ι R →+* A)
    (RingHom.comp (β := MvPolynomial ι K) (AlgHom.toRingHom (aeval x)) (MvPolynomial.map (algebraMap R K)))
    (AlgHom.toRingHom (aeval x))

Tactic:
ext
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
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
x_1 : R
⊢ Eq.{v + 1} (α := A)
    ((RingHom.comp
            (RingHom.comp (β := MvPolynomial ι K) (AlgHom.toRingHom (aeval x)) (MvPolynomial.map (algebraMap R K))) C :
          (a : R) → A)
        x_1 :
      A)
    ((RingHom.comp (AlgHom.toRingHom (aeval x)) C : (a : R) → A) x_1 : A)

Tactic:
simp [algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
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
i : ι
⊢ Eq.{v + 1} (α := A)
    ((RingHom.comp (β := MvPolynomial ι K) (AlgHom.toRingHom (aeval x)) (MvPolynomial.map (algebraMap R K)) :
          (a : MvPolynomial ι R) → A)
        (X i) :
      A)
    ((AlgHom.toRingHom (aeval x) : (a : MvPolynomial ι R) → A) (X i) : A)

Tactic:
simp [algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
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
⊢ 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]
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
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))
change : Injective (α := MvPolynomial ι R) (β := A) (⇑(AlgHom.toRingHom (aeval x)) : (a : MvPolynomial ι R) → A)
⊢ AlgebraicIndependent R x

Tactic:
change Injective (aeval x).toRingHom

Premises used: MvPolynomial.aeval, AlgHom.toRingHom, Function.Injective, DFunLike.coe
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
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))
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))
⊢ Injective (α := MvPolynomial ι R) (β := A) (⇑(AlgHom.toRingHom (aeval x)) : (a : MvPolynomial ι R) → A)

Tactic:
rw [← this, RingHom.coe_comp]

Premises used: RingHom.coe_comp
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
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)
    (Function.comp (β := MvPolynomial ι K) (⇑(AlgHom.toRingHom (aeval x)) : (a : MvPolynomial ι K) → A)
      (⇑(MvPolynomial.map (algebraMap R K)) : (a : MvPolynomial ι R) → MvPolynomial ι K))

Tactic:
Injective.comp ai (MvPolynomial.map_injective _ hinj)

Premises used: MvPolynomial.map_injective, Function.Injective.comp
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
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)
    (Function.comp (β := MvPolynomial ι K) (⇑(AlgHom.toRingHom (aeval x)) : (a : MvPolynomial ι K) → A)
      (⇑(MvPolynomial.map (algebraMap R K)) : (a : MvPolynomial ι R) → MvPolynomial ι K))

Tactic:
exact Injective.comp ai (MvPolynomial.map_injective _ hinj)

Premises used: MvPolynomial.map_injective, Function.Injective.comp
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
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))
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
⊢ AlgebraicIndependent R x

Tactic:
rw [algebraicIndependent_iff] at H ⊢

Premises used: algebraicIndependent_iff
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
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) (((↑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)
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
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 (α := 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
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
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 (α := MvPolynomial ι S)
    ((MvPolynomial.map (↑f : R →+* S) : (a : MvPolynomial ι R) → MvPolynomial ι S) p : MvPolynomial ι S)
    (0 : MvPolynomial ι S)
rwa rwa₁ rwa₂ rwa₃ :
  Eq (α := MvPolynomial ι S)
    ((MvPolynomial.map (↑f : R →+* S) : (a : MvPolynomial ι R) → MvPolynomial ι S) p : MvPolynomial ι S)
    (0 : MvPolynomial ι S)
⊢ Eq (α := MvPolynomial ι S)
    ((MvPolynomial.map (↑f : R →+* S) : (a : MvPolynomial ι R) → MvPolynomial ι S) p : MvPolynomial ι S)
    ((MvPolynomial.map (↑f : R →+* S) : (a : MvPolynomial ι R) → MvPolynomial ι S) 0 : MvPolynomial ι S)

Tactic:
rwa [map_zero]

Premises used: map_zero
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
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 (α := MvPolynomial ι S)
    ((MvPolynomial.map (↑f : R →+* S) : (a : MvPolynomial ι R) → MvPolynomial ι S) p : MvPolynomial ι S)
    (0 : MvPolynomial ι S)
⊢ p = 0

Tactic:
exact map_injective (f : R →+* S) hf (by rwa [map_zero])

Premises used: MvPolynomial.map_injective, RingHomClass.toRingHom
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
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))
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
⊢ AlgebraicIndependent.{u, u_3, u_4} S (A := B) ((⇑g : (a : A) → B) ∘ x)

Tactic:
rw [algebraicIndependent_iff] at H ⊢

Premises used: algebraicIndependent_iff
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
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)
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)
⊢ p = 0

Tactic:
obtain ⟨q, rfl⟩ := map_surjective (f : R →+* S) hf p

Premises used: RingHomClass.toRingHom, MvPolynomial.map_surjective, rfl
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
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)
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)
rwa₄ :
  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) q : MvPolynomial ι S) :
      B)
    (0 : B)
rwa₅ rwa₆ rwa₇ rwa₈ :
  Eq.{u_4 + 1} (α := B)
    ((aeval fun (i : ι) ↦ ((↑g : A →+* B) : (a : A) → B) (x i) : (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)

Tactic:
rwa [map_zero, ← RingHom.coe_coe g, map_aeval, ← h, ← eval₂Hom_map_hom,
    ← aeval_eq_eval₂Hom]

Premises used: MvPolynomial.map_aeval, RingHom.coe_coe, map_zero, MvPolynomial.eval₂Hom_map_hom, MvPolynomial.aeval_eq_eval₂Hom