awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hx : AlgebraicIndependent R x
this :
  Eq (α := (ι →₀ R) →ₗ[R] A) (Finsupp.linearCombination R x : (ι →₀ R) →ₗ[R] A)
    (AlgHom.toLinearMap (aeval x) ∘ₗ Finsupp.linearCombination R X : (ι →₀ R) →ₗ[R] A)
⊢ Injective (α := ι →₀ R) (β := A)
    (⇑(AlgHom.toLinearMap (aeval x) ∘ₗ Finsupp.linearCombination R X : (ι →₀ R) →ₗ[R] A) : (a : ι →₀ R) → A)

Tactic:
(algebraicIndependent_iff_injective_aeval.mp hx).comp ?_

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂, algebraicIndependent_iff_injective_aeval, Function.Injective.comp, Iff.mp, Finset.sum
-- 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
hx : AlgebraicIndependent R x
this :
  Eq (α := (ι →₀ R) →ₗ[R] A) (Finsupp.linearCombination R x : (ι →₀ R) →ₗ[R] A)
    (AlgHom.toLinearMap (aeval x) ∘ₗ Finsupp.linearCombination R X : (ι →₀ R) →ₗ[R] A)
refine :
  Injective (α := ι →₀ R) (β := MvPolynomial ι R) (⇑(Finsupp.linearCombination R X) : (a : ι →₀ R) → MvPolynomial ι R)
⊢ Injective (α := ι →₀ R) (β := A)
    (⇑(AlgHom.toLinearMap (aeval x) ∘ₗ Finsupp.linearCombination R X : (ι →₀ R) →ₗ[R] A) : (a : ι →₀ R) → A)

Tactic:
refine (algebraicIndependent_iff_injective_aeval.mp hx).comp ?_

Premises used: algebraicIndependent_iff_injective_aeval, Function.Injective.comp, Iff.mp
-- 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
hx : AlgebraicIndependent R x
this :
  Eq (α := (ι →₀ R) →ₗ[R] A) (Finsupp.linearCombination R x : (ι →₀ R) →ₗ[R] A)
    (AlgHom.toLinearMap (aeval x) ∘ₗ Finsupp.linearCombination R X : (ι →₀ R) →ₗ[R] A)
⊢ LinearIndependent (ι := ι) R (M := MvPolynomial ι R) X

Tactic:
linearIndependent_X _ _

Premises used: MvPolynomial.linearIndependent_X
-- 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
hx : AlgebraicIndependent R x
this :
  Eq (α := (ι →₀ R) →ₗ[R] A) (Finsupp.linearCombination R x : (ι →₀ R) →ₗ[R] A)
    (AlgHom.toLinearMap (aeval x) ∘ₗ Finsupp.linearCombination R X : (ι →₀ R) →ₗ[R] A)
⊢ LinearIndependent (ι := ι) R (M := MvPolynomial ι R) X

Tactic:
exact linearIndependent_X _ _

Premises used: MvPolynomial.linearIndependent_X
-- 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
hx : AlgebraicIndependent R x
inst_3 : Nontrivial R
⊢ Injective x

Tactic:
hx.linearIndependent.injective

Premises used: LinearIndependent.injective, AlgebraicIndependent.linearIndependent
-- 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
hx : AlgebraicIndependent R x
inst_3 : Nontrivial R
i : ι
⊢ x i ≠ 0

Tactic:
hx.linearIndependent.ne_zero i

Premises used: LinearIndependent.ne_zero, AlgebraicIndependent.linearIndependent
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
ι : Type u
R : Type u_2
A : Type v
A' : Type v'
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
hx : AlgebraicIndependent R x
f : A →ₐ[R] A'
hf_inj : InjOn.{v, v'} (β := A') (⇑f : (a : A) → A') (↑(adjoin R (range x)) : Set A)
hf :
  ∀ (i : ι),
    Eq.{v' + 1} (α := A') ((aeval ((⇑f : (a : A) → A') ∘ x) : (a : MvPolynomial ι R) → A') (X i) : A')
      ((f.comp (aeval x) : (a : MvPolynomial ι R) → A') (X i) : A')
⊢ aeval ((⇑f : (a : A) → A') ∘ x) = f.comp (aeval x)

Tactic:
ext
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
ι : Type u
R : Type u_2
A : Type v
A' : Type v'
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
hx : AlgebraicIndependent R x
f : A →ₐ[R] A'
hf_inj : InjOn.{v, v'} (β := A') (⇑f : (a : A) → A') (↑(adjoin R (range x)) : Set A)
i : ι
⊢ Eq.{v' + 1} (α := A') ((aeval ((⇑f : (a : A) → A') ∘ x) : (a : MvPolynomial ι R) → A') (X i) : A')
    ((f.comp (aeval x) : (a : MvPolynomial ι R) → A') (X i) : A')

Tactic:
simp
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
ι : Type u
R : Type u_2
A : Type v
A' : Type v'
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
hx : AlgebraicIndependent R x
f : A →ₐ[R] A'
hf_inj : InjOn.{v, v'} (β := A') (⇑f : (a : A) → A') (↑(adjoin R (range x)) : Set A)
⊢ aeval ((⇑f : (a : A) → A') ∘ x) = f.comp (aeval x)

Tactic:
have : aeval (f ∘ x) = f.comp (aeval x) := by ext; simp
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
ι : Type u
R : Type u_2
A : Type v
A' : Type v'
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
hx : AlgebraicIndependent R x
f : A →ₐ[R] A'
hf_inj : InjOn.{v, v'} (β := A') (⇑f : (a : A) → A') (↑(adjoin R (range x)) : Set A)
this : aeval ((⇑f : (a : A) → A') ∘ x) = f.comp (aeval x)
p : MvPolynomial ι R
rw :
  ∃ (x_1 : MvPolynomial.{v, u_2} { x_1 : A // x_1 ∈ range x } R),
    Eq.{v + 1} (α := A)
      ((aeval (Subtype.val (p := fun (x_2 : A) ↦ x_2 ∈ range x)) :
            (a : MvPolynomial { x_2 : A // x_2 ∈ range x } R) → A)
          x_1 :
        A)
      ((aeval x : (a : MvPolynomial ι R) → A) p : A)
⊢ Membership.mem.{v, v} (α := A) (γ := Subalgebra R A)
    (AlgHom.range (A := MvPolynomial.{v, u_2} { x_1 : A // x_1 ∈ range x } R)
      (aeval (Subtype.val (p := fun (x_1 : A) ↦ x_1 ∈ range x))))
    ((aeval x : (a : MvPolynomial ι R) → A) p : A)

Tactic:
rw [AlgHom.mem_range]

Premises used: AlgHom.mem_range
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
ι : Type u
R : Type u_2
A : Type v
A' : Type v'
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
hx : AlgebraicIndependent R x
f : A →ₐ[R] A'
hf_inj : InjOn.{v, v'} (β := A') (⇑f : (a : A) → A') (↑(adjoin R (range x)) : Set A)
this : aeval ((⇑f : (a : A) → A') ∘ x) = f.comp (aeval x)
p : MvPolynomial ι R
refine :
  Eq.{v + 1} (α := A)
    ((aeval (Subtype.val (p := fun (x_1 : A) ↦ x_1 ∈ range x)) : (a : MvPolynomial { x_1 : A // x_1 ∈ range x } R) → A)
        ((rename (codRestrict x (range x) ⋯) : (a : MvPolynomial ι R) → MvPolynomial (↑(range x) : Type v) R) p :
          MvPolynomial.{v, u_2} (↑(range x) : Type v) R) :
      A)
    ((aeval x : (a : MvPolynomial ι R) → A) p : A)
⊢ ∃ (x_1 : MvPolynomial.{v, u_2} { x_1 : A // x_1 ∈ range x } R),
    Eq.{v + 1} (α := A)
      ((aeval (Subtype.val (p := fun (x_2 : A) ↦ x_2 ∈ range x)) :
            (a : MvPolynomial { x_2 : A // x_2 ∈ range x } R) → A)
          x_1 :
        A)
      ((aeval x : (a : MvPolynomial ι R) → A) p : A)

Tactic:
refine ⟨MvPolynomial.rename (codRestrict x (range x) mem_range_self) p, ?_⟩
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
ι : Type u
R : Type u_2
A : Type v
A' : Type v'
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
hx : AlgebraicIndependent R x
f : A →ₐ[R] A'
hf_inj : InjOn.{v, v'} (β := A') (⇑f : (a : A) → A') (↑(adjoin R (range x)) : Set A)
this : aeval ((⇑f : (a : A) → A') ∘ x) = f.comp (aeval x)
p : MvPolynomial ι R
⊢ Eq.{v + 1} (α := A)
    ((aeval (Subtype.val (p := fun (x_1 : A) ↦ x_1 ∈ range x)) : (a : MvPolynomial { x_1 : A // x_1 ∈ range x } R) → A)
        ((rename (codRestrict x (range x) ⋯) : (a : MvPolynomial ι R) → MvPolynomial (↑(range x) : Type v) R) p :
          MvPolynomial.{v, u_2} (↑(range x) : Type v) R) :
      A)
    ((aeval x : (a : MvPolynomial ι R) → A) p : A)

Tactic:
simp [Function.comp_def, aeval_rename]

Premises used: Function.comp_def, MvPolynomial.aeval_rename
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
ι : Type u
R : Type u_2
A : Type v
A' : Type v'
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
hx : AlgebraicIndependent R x
f : A →ₐ[R] A'
hf_inj : InjOn.{v, v'} (β := A') (⇑f : (a : A) → A') (↑(adjoin R (range x)) : Set A)
this : aeval ((⇑f : (a : A) → A') ∘ x) = f.comp (aeval x)
⊢ ∀ (p : MvPolynomial ι R),
    Membership.mem.{v, v} (α := A) (γ := Subalgebra R A)
      (AlgHom.range (A := MvPolynomial.{v, u_2} { x_1 : A // x_1 ∈ range x } R)
        (aeval (Subtype.val (p := fun (x_1 : A) ↦ x_1 ∈ range x))))
      ((aeval x : (a : MvPolynomial ι R) → A) p : A)

Tactic:
have h : ∀ p : MvPolynomial ι R, aeval x p ∈ (@aeval R _ _ _ _ _ ((↑) : range x → A)).range := by
    intro p
    rw [AlgHom.mem_range]
    refine ⟨MvPolynomial.rename (codRestrict x (range x) mem_range_self) p, ?_⟩
    simp [Function.comp_def, aeval_rename]
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
ι : Type u
R : Type u_2
A : Type v
A' : Type v'
x_1 : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
hx : AlgebraicIndependent R x_1
f : A →ₐ[R] A'
hf_inj : InjOn.{v, v'} (β := A') (⇑f : (a : A) → A') (↑(adjoin R (range x_1)) : Set A)
this : aeval ((⇑f : (a : A) → A') ∘ x_1) = f.comp (aeval x_1)
h :
  ∀ (p : MvPolynomial ι R),
    Membership.mem.{v, v} (α := A) (γ := Subalgebra R A)
      (AlgHom.range (A := MvPolynomial.{v, u_2} { x : A // x ∈ range x_1 } R)
        (aeval (Subtype.val (p := fun (x : A) ↦ x ∈ range x_1))))
      ((aeval x_1 : (a : MvPolynomial ι R) → A) p : A)
x y : MvPolynomial ι R
hxy :
  Eq.{v' + 1} (α := A') ((aeval ((⇑f : (a : A) → A') ∘ x_1) : (a : MvPolynomial ι R) → A') x : A')
    ((aeval ((⇑f : (a : A) → A') ∘ x_1) : (a : MvPolynomial ι R) → A') y : A')
⊢ Eq.{v' + 1} (α := A') ((f.comp (aeval x_1) : (a : MvPolynomial ι R) → A') x : A')
    ((f.comp (aeval x_1) : (a : MvPolynomial ι R) → A') y : A')

Tactic:
rw [this] at hxy
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
ι : Type u
R : Type u_2
A : Type v
A' : Type v'
x_1 : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
hx : AlgebraicIndependent R x_1
f : A →ₐ[R] A'
hf_inj : InjOn.{v, v'} (β := A') (⇑f : (a : A) → A') (↑(adjoin R (range x_1)) : Set A)
this : aeval ((⇑f : (a : A) → A') ∘ x_1) = f.comp (aeval x_1)
h :
  ∀ (p : MvPolynomial ι R),
    Membership.mem.{v, v} (α := A) (γ := Subalgebra R A)
      (AlgHom.range (A := MvPolynomial.{v, u_2} { x : A // x ∈ range x_1 } R)
        (aeval (Subtype.val (p := fun (x : A) ↦ x ∈ range x_1))))
      ((aeval x_1 : (a : MvPolynomial ι R) → A) p : A)
x y : MvPolynomial ι R
hxy :
  Eq.{v' + 1} (α := A') ((f.comp (aeval x_1) : (a : MvPolynomial ι R) → A') x : A')
    ((f.comp (aeval x_1) : (a : MvPolynomial ι R) → A') y : A')
rw :
  ∀
    (hf_inj :
      InjOn.{v, v'} (β := A') (⇑f : (a : A) → A')
        (↑(AlgHom.range (A := MvPolynomial.{v, u_2} { x : A // x ∈ range x_1 } R)
              (aeval (Subtype.val (p := fun (x : A) ↦ x ∈ range x_1)))) :
          Set A))
    (this : aeval ((⇑f : (a : A) → A') ∘ x_1) = f.comp (aeval x_1))
    (h :
      ∀ (p : MvPolynomial ι R),
        Membership.mem.{v, v} (α := A) (γ := Subalgebra R A)
          (AlgHom.range (A := MvPolynomial.{v, u_2} { x : A // x ∈ range x_1 } R)
            (aeval (Subtype.val (p := fun (x : A) ↦ x ∈ range x_1))))
          ((aeval x_1 : (a : MvPolynomial ι R) → A) p : A))
    ⦃x y : MvPolynomial ι R⦄
    (hxy :
      Eq.{v' + 1} (α := A') ((f.comp (aeval x_1) : (a : MvPolynomial ι R) → A') x : A')
        ((f.comp (aeval x_1) : (a : MvPolynomial ι R) → A') y : A')),
    x = y
⊢ x = y

Tactic:
rw [adjoin_eq_range] at hf_inj

Premises used: Algebra.adjoin_eq_range
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
ι : Type u
R : Type u_2
A : Type v
A' : Type v'
x_1 : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
hx : AlgebraicIndependent R x_1
f : A →ₐ[R] A'
hf_inj :
  InjOn.{v, v'} (β := A') (⇑f : (a : A) → A')
    (↑(AlgHom.range (A := MvPolynomial.{v, u_2} { x : A // x ∈ range x_1 } R)
          (aeval (Subtype.val (p := fun (x : A) ↦ x ∈ range x_1)))) :
      Set A)
this : aeval ((⇑f : (a : A) → A') ∘ x_1) = f.comp (aeval x_1)
h :
  ∀ (p : MvPolynomial ι R),
    Membership.mem.{v, v} (α := A) (γ := Subalgebra R A)
      (AlgHom.range (A := MvPolynomial.{v, u_2} { x : A // x ∈ range x_1 } R)
        (aeval (Subtype.val (p := fun (x : A) ↦ x ∈ range x_1))))
      ((aeval x_1 : (a : MvPolynomial ι R) → A) p : A)
x y : MvPolynomial ι R
hxy :
  Eq.{v' + 1} (α := A') ((f.comp (aeval x_1) : (a : MvPolynomial ι R) → A') x : A')
    ((f.comp (aeval x_1) : (a : MvPolynomial ι R) → A') y : A')
⊢ x = y

Tactic:
hx (hf_inj (h x) (h y) hxy)
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
ι : Type u
R : Type u_2
A : Type v
A' : Type v'
x_1 : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
hx : AlgebraicIndependent R x_1
f : A →ₐ[R] A'
hf_inj :
  InjOn.{v, v'} (β := A') (⇑f : (a : A) → A')
    (↑(AlgHom.range (A := MvPolynomial.{v, u_2} { x : A // x ∈ range x_1 } R)
          (aeval (Subtype.val (p := fun (x : A) ↦ x ∈ range x_1)))) :
      Set A)
this : aeval ((⇑f : (a : A) → A') ∘ x_1) = f.comp (aeval x_1)
h :
  ∀ (p : MvPolynomial ι R),
    Membership.mem.{v, v} (α := A) (γ := Subalgebra R A)
      (AlgHom.range (A := MvPolynomial.{v, u_2} { x : A // x ∈ range x_1 } R)
        (aeval (Subtype.val (p := fun (x : A) ↦ x ∈ range x_1))))
      ((aeval x_1 : (a : MvPolynomial ι R) → A) p : A)
x y : MvPolynomial ι R
hxy :
  Eq.{v' + 1} (α := A') ((f.comp (aeval x_1) : (a : MvPolynomial ι R) → A') x : A')
    ((f.comp (aeval x_1) : (a : MvPolynomial ι R) → A') y : A')
⊢ x = y

Tactic:
exact hx (hf_inj (h x) (h y) hxy)
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
ι : Type u
R : Type u_2
A : Type v
A' : Type v'
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
hx : AlgebraicIndependent R x
f : A →ₐ[R] A'
hf_inj : Injective.{v + 1, v' + 1} (α := A) (β := A') (⇑f : (a : A) → A')
⊢ AlgebraicIndependent.{u, u_2, v'} R (A := A') ((⇑f : (a : A) → A') ∘ x)

Tactic:
hx.map hf_inj.injOn

Premises used: Function.Injective.injOn, AlgebraicIndependent.map
-- 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
hx : AlgebraicIndependent R x
f : ι → MvPolynomial ι R
hf : AlgebraicIndependent R f
rw :
  ∀ (hx : ∀ (p : MvPolynomial ι R), Eq.{v + 1} (α := A) ((aeval x : (a : MvPolynomial ι R) → A) p : A) (0 : A) → p = 0)
    {f : ι → MvPolynomial ι R}
    (hf :
      ∀ (p : MvPolynomial ι R),
        Eq (α := MvPolynomial ι R) ((aeval f : (a : MvPolynomial ι R) → MvPolynomial ι R) p : MvPolynomial ι R)
            (0 : MvPolynomial ι R) →
          p = 0)
    (p : MvPolynomial ι R),
    Eq.{v + 1} (α := A)
        ((aeval fun (i : ι) ↦ (aeval x : (a : MvPolynomial ι R) → A) (f i) : (a : MvPolynomial ι R) → A) p : A)
        (0 : A) →
      p = 0
⊢ AlgebraicIndependent.{u, u_2, v} R (A := A) fun (i : ι) ↦ (aeval x : (a : MvPolynomial ι R) → A) (f i)

Tactic:
rw [algebraicIndependent_iff] at hx hf ⊢

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
hx : ∀ (p : MvPolynomial ι R), Eq.{v + 1} (α := A) ((aeval x : (a : MvPolynomial ι R) → A) p : A) (0 : A) → p = 0
f : ι → MvPolynomial ι R
hf :
  ∀ (p : MvPolynomial ι R),
    Eq (α := MvPolynomial ι R) ((aeval f : (a : MvPolynomial ι R) → MvPolynomial ι R) p : MvPolynomial ι R)
        (0 : MvPolynomial ι R) →
      p = 0
p : MvPolynomial ι R
hp :
  Eq.{v + 1} (α := A)
    ((aeval fun (i : ι) ↦ (aeval x : (a : MvPolynomial ι R) → A) (f i) : (a : MvPolynomial ι R) → A) p : A) (0 : A)
rwa :
  ∀ (hp : Eq.{v + 1} (α := A) ((AlgHom.comp (aeval x) (bind₁ f) : (a : MvPolynomial ι R) → A) p : A) (0 : A)),
    Eq.{v + 1} (α := A)
      ((aeval x : (a : MvPolynomial ι R) → A)
          ((aeval f : (a : MvPolynomial ι R) → MvPolynomial ι R) p : MvPolynomial ι R) :
        A)
      (0 : A)
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀
    (hp :
      Eq.{v + 1} (α := A)
        ((aeval x : (a : MvPolynomial ι R) → A)
            ((bind₁ f : (a : MvPolynomial ι R) → MvPolynomial ι R) p : MvPolynomial ι R) :
          A)
        (0 : A)),
    Eq.{v + 1} (α := A)
      ((aeval x : (a : MvPolynomial ι R) → A)
          ((aeval f : (a : MvPolynomial ι R) → MvPolynomial ι R) p : MvPolynomial ι R) :
        A)
      (0 : A)
⊢ Eq.{v + 1} (α := A)
    ((aeval x : (a : MvPolynomial ι R) → A)
        ((aeval f : (a : MvPolynomial ι R) → MvPolynomial ι R) p : MvPolynomial ι R) :
      A)
    (0 : A)

Tactic:
rwa [← aeval_comp_bind₁, AlgHom.comp_apply] at hp

Premises used: AlgHom.comp_apply, MvPolynomial.aeval_comp_bind₁
-- 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
hx : ∀ (p : MvPolynomial ι R), Eq.{v + 1} (α := A) ((aeval x : (a : MvPolynomial ι R) → A) p : A) (0 : A) → p = 0
f : ι → MvPolynomial ι R
hf :
  ∀ (p : MvPolynomial ι R),
    Eq (α := MvPolynomial ι R) ((aeval f : (a : MvPolynomial ι R) → MvPolynomial ι R) p : MvPolynomial ι R)
        (0 : MvPolynomial ι R) →
      p = 0
p : MvPolynomial ι R
hp :
  Eq.{v + 1} (α := A)
    ((aeval fun (i : ι) ↦ (aeval x : (a : MvPolynomial ι R) → A) (f i) : (a : MvPolynomial ι R) → A) p : A) (0 : A)
⊢ p = 0

Tactic:
exact hf _ (hx _ (by rwa [← aeval_comp_bind₁, AlgHom.comp_apply] at 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
f : ι → MvPolynomial ι R
H : AlgebraicIndependent.{u, u_2, v} R (A := A) fun (i : ι) ↦ (aeval x : (a : MvPolynomial ι R) → A) (f i)
rw :
  ∀
    (H :
      ∀ (p : MvPolynomial ι R),
        Eq.{v + 1} (α := A)
            ((aeval fun (i : ι) ↦ (aeval x : (a : MvPolynomial ι R) → A) (f i) : (a : MvPolynomial ι R) → A) p : A)
            (0 : A) →
          p = 0)
    (p : MvPolynomial ι R),
    Eq (α := MvPolynomial ι R) ((aeval f : (a : MvPolynomial ι R) → MvPolynomial ι R) p : MvPolynomial ι R)
        (0 : MvPolynomial ι R) →
      p = 0
⊢ AlgebraicIndependent R f

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
f : ι → MvPolynomial ι R
H :
  ∀ (p : MvPolynomial ι R),
    Eq.{v + 1} (α := A)
        ((aeval fun (i : ι) ↦ (aeval x : (a : MvPolynomial ι R) → A) (f i) : (a : MvPolynomial ι R) → A) p : A)
        (0 : A) →
      p = 0
p : MvPolynomial ι R
hp :
  Eq (α := MvPolynomial ι R) ((aeval f : (a : MvPolynomial ι R) → MvPolynomial ι R) p : MvPolynomial ι R)
    (0 : MvPolynomial ι R)
rw : Eq.{v + 1} (α := A) ((AlgHom.comp (aeval x) (bind₁ f) : (a : MvPolynomial ι R) → A) p : A) (0 : A)
rw₁ :
  Eq.{v + 1} (α := A)
    ((aeval x : (a : MvPolynomial ι R) → A)
        ((bind₁ f : (a : MvPolynomial ι R) → MvPolynomial ι R) p : MvPolynomial ι R) :
      A)
    (0 : A)
rw₂ :
  Eq.{v + 1} (α := A)
    ((aeval x : (a : MvPolynomial ι R) → A)
        ((aeval f : (a : MvPolynomial ι R) → MvPolynomial ι R) p : MvPolynomial ι R) :
      A)
    (0 : A)
rw₃ : Eq.{v + 1} (α := A) ((aeval x : (a : MvPolynomial ι R) → A) 0 : A) (0 : A)
rw₄ rw₅ : Eq.{v + 1} (α := A) 0 0
⊢ Eq.{v + 1} (α := A)
    ((aeval fun (i : ι) ↦ (aeval x : (a : MvPolynomial ι R) → A) (f i) : (a : MvPolynomial ι R) → A) p : A) (0 : A)

Tactic:
rw [← aeval_comp_bind₁, AlgHom.comp_apply, bind₁, hp, map_zero]

Premises used: AlgHom.comp_apply, map_zero, MvPolynomial.bind₁, MvPolynomial.aeval_comp_bind₁
-- 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
f : ι → MvPolynomial ι R
H :
  ∀ (p : MvPolynomial ι R),
    Eq.{v + 1} (α := A)
        ((aeval fun (i : ι) ↦ (aeval x : (a : MvPolynomial ι R) → A) (f i) : (a : MvPolynomial ι R) → A) p : A)
        (0 : A) →
      p = 0
p : MvPolynomial ι R
hp :
  Eq (α := MvPolynomial ι R) ((aeval f : (a : MvPolynomial ι R) → MvPolynomial ι R) p : MvPolynomial ι R)
    (0 : MvPolynomial ι R)
⊢ p = 0

Tactic:
exact H p (by rw [← aeval_comp_bind₁, AlgHom.comp_apply, bind₁, hp, map_zero])
-- 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
h : ¬Injective.{u_2 + 1, v + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
⊢ IsEmpty.{v + 1} { s : Set A // AlgebraicIndepOn R _root_.id s }

Tactic:
have := isEmpty_algebraicIndependent h
-- 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
h : ¬Injective.{u_2 + 1, v + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
this : IsEmpty.{v + 1} { s : Set A // AlgebraicIndepOn R _root_.id s }
rw :
  Eq.{v + 2} (α := Cardinal.{v})
    (⨆ (ι : { s : Set A // AlgebraicIndepOn R _root_.id s }), Cardinal.mk (↑(↑ι : Set A) : Type v)) 0
rw₁ : Eq.{v + 2} (α := Cardinal.{v}) ⊥ 0
rw₂ rw₃ : Eq.{v + 2} (α := Cardinal.{v}) 0 0
⊢ trdeg R A = 0

Tactic:
rw [trdeg, ciSup_of_empty, bot_eq_zero]

Premises used: Algebra.trdeg, ciSup_of_empty, bot_eq_zero
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
σ : Type u_3
R : Type u_4
inst : CommRing R
rw :
  Injective (α := MvPolynomial σ R) (β := MvPolynomial σ R)
    (⇑(AlgHom.id R (MvPolynomial σ R)) : (a : MvPolynomial σ R) → MvPolynomial σ R)
⊢ AlgebraicIndependent (ι := σ) R (A := MvPolynomial σ R) X

Tactic:
rw [AlgebraicIndependent, aeval_X_left]

Premises used: MvPolynomial.aeval_X_left, AlgebraicIndependent
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
σ : Type u_3
R : Type u_4
inst : CommRing R
⊢ Injective (α := MvPolynomial σ R) (β := MvPolynomial σ R)
    (⇑(AlgHom.id R (MvPolynomial σ R)) : (a : MvPolynomial σ R) → MvPolynomial σ R)

Tactic:
injective_id

Premises used: Function.injective_id
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
σ : Type u_3
R : Type u_4
inst : CommRing R
⊢ Injective (α := MvPolynomial σ R) (β := MvPolynomial σ R)
    (⇑(AlgHom.id R (MvPolynomial σ R)) : (a : MvPolynomial σ R) → MvPolynomial σ R)

Tactic:
exact injective_id

Premises used: Function.injective_id
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Basic
Goal:
ι : Type u
R : Type u_2
A : Type v
A' : Type v'
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
f : A →ₐ[R] A'
hf : Injective.{v + 1, v' + 1} (α := A) (β := A') (⇑f : (a : A) → A')
⊢ AlgebraicIndependent.{u, u_2, v'} R (A := A') ((⇑f : (a : A) → A') ∘ x) ↔ AlgebraicIndependent R x

Tactic:
⟨fun h => h.of_comp f, fun h => h.map hf.injOn⟩

Premises used: Function.Injective.injOn, AlgebraicIndependent.map, Iff.intro, 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
inst_3 : Subsingleton R
⊢ AlgebraicIndependent R x

Tactic:
algebraicIndependent_iff.2 fun _ _ => Subsingleton.elim _ _

Premises used: Iff.mpr, algebraicIndependent_iff, Subsingleton.elim, OfNat.ofNat
-- 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
⊢ Subsingleton A

Tactic:
have := Module.subsingleton R A