awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
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)
have 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')
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (hypothesis)
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)
⊢ AlgebraicIndependent.{u, u_2, v'} R (A := A') ((⇑f : (a : A) → A') ∘ x)
have this : aeval ((⇑f : (a : A) → A') ∘ x) = f.comp (aeval x)
Tactic: have : aeval (f ∘ x) = f.comp (aeval x) := by ext; simp
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
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)
have 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)
Tactic: rw [AlgHom.mem_range]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
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
⊢ ∃ (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)
have 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) sorry) : (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: refine ⟨MvPolynomial.rename (codRestrict x (range x) mem_range_self) p, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (hypothesis)
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)
⊢ AlgebraicIndependent.{u, u_2, v'} R (A := A') ((⇑f : (a : A) → A') ∘ x)
have h : ∀ (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]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (hypothesis)
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')
⊢ x = y
have 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')
Tactic: rw [this] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
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')
⊢ x = y
have 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
Tactic: rw [adjoin_eq_range] at hf_inj
Cleared hypotheses: hf_inj, this, h, x, y, hxy
-- 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
hx : AlgebraicIndependent R x
f : ι → MvPolynomial ι R
hf : AlgebraicIndependent R f
⊢ AlgebraicIndependent.{u, u_2, v} R (A := A) fun (i : ι) ↦ (aeval x : (a : MvPolynomial ι R) → A) (f i)
have 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
Tactic: rw [algebraicIndependent_iff] at hx hf ⊢
Cleared hypotheses: hx, f, hf
-- 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
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)
⊢ Eq.{v + 1} (α := A)
    ((aeval x : (a : MvPolynomial ι R) → A)
        ((aeval f : (a : MvPolynomial ι R) → MvPolynomial ι R) p : MvPolynomial ι R) :
      A)
    (0 : A)
have 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)
Tactic: rwa [← aeval_comp_bind₁, AlgHom.comp_apply] at hp
Cleared hypotheses: 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
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)
⊢ Eq.{v + 1} (α := A)
    ((aeval x : (a : MvPolynomial ι R) → A)
        ((aeval f : (a : MvPolynomial ι R) → MvPolynomial ι R) p : MvPolynomial ι R) :
      A)
    (0 : A)
have 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)
Tactic: rwa [← aeval_comp_bind₁, AlgHom.comp_apply] at hp
Cleared hypotheses: 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
f : ι → MvPolynomial ι R
H : AlgebraicIndependent.{u, u_2, v} R (A := A) fun (i : ι) ↦ (aeval x : (a : MvPolynomial ι R) → A) (f i)
⊢ AlgebraicIndependent R f
have 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
Tactic: rw [algebraicIndependent_iff] at H ⊢
Cleared hypotheses: 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
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)
⊢ Eq.{v + 1} (α := A)
    ((aeval fun (i : ι) ↦ (aeval x : (a : MvPolynomial ι R) → A) (f i) : (a : MvPolynomial ι R) → A) p : A) (0 : A)
have rw : Eq.{v + 1} (α := A) ((AlgHom.comp (aeval x) (bind₁ f) : (a : MvPolynomial ι R) → A) p : A) (0 : A)
Tactic: rw [← aeval_comp_bind₁, AlgHom.comp_apply, bind₁, hp, map_zero]
-- 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
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)
⊢ Eq.{v + 1} (α := A)
    ((aeval fun (i : ι) ↦ (aeval x : (a : MvPolynomial ι R) → A) (f i) : (a : MvPolynomial ι R) → A) p : A) (0 : A)
have rw₁ : Eq.{v + 1} (α := A)
  ((aeval x : (a : MvPolynomial ι R) → A) ((bind₁ f : (a : MvPolynomial ι R) → MvPolynomial ι R) p : MvPolynomial ι R) :
    A)
  (0 : A)
Tactic: rw [← aeval_comp_bind₁, AlgHom.comp_apply, bind₁, hp, map_zero]
-- 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
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)
⊢ Eq.{v + 1} (α := A)
    ((aeval fun (i : ι) ↦ (aeval x : (a : MvPolynomial ι R) → A) (f i) : (a : MvPolynomial ι R) → A) p : A) (0 : A)
have rw₂ : Eq.{v + 1} (α := A)
  ((aeval x : (a : MvPolynomial ι R) → A) ((aeval f : (a : MvPolynomial ι R) → MvPolynomial ι R) p : MvPolynomial ι R) :
    A)
  (0 : A)
Tactic: rw [← aeval_comp_bind₁, AlgHom.comp_apply, bind₁, hp, map_zero]
-- 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
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)
⊢ Eq.{v + 1} (α := A)
    ((aeval fun (i : ι) ↦ (aeval x : (a : MvPolynomial ι R) → A) (f i) : (a : MvPolynomial ι R) → A) p : A) (0 : A)
have rw₃ : Eq.{v + 1} (α := A) ((aeval x : (a : MvPolynomial ι R) → A) 0 : A) (0 : A)
Tactic: rw [← aeval_comp_bind₁, AlgHom.comp_apply, bind₁, hp, map_zero]
-- 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
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)
⊢ Eq.{v + 1} (α := A)
    ((aeval fun (i : ι) ↦ (aeval x : (a : MvPolynomial ι R) → A) (f i) : (a : MvPolynomial ι R) → A) p : A) (0 : A)
have rw₄ : Eq.{v + 1} (α := A) 0 0
Tactic: rw [← aeval_comp_bind₁, AlgHom.comp_apply, bind₁, hp, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (hypothesis)
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)
⊢ trdeg R A = 0
have this : IsEmpty.{v + 1} { s : Set A // AlgebraicIndepOn R _root_.id s }
Tactic: have := isEmpty_algebraicIndependent h
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
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 }
⊢ trdeg R A = 0
have rw : Eq.{v + 2} (α := Cardinal.{v})
  (⨆ (ι : { s : Set A // AlgebraicIndepOn R _root_.id s }), Cardinal.mk (↑(↑ι : Set A) : Type v)) 0
Tactic: rw [trdeg, ciSup_of_empty, bot_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
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
⊢ trdeg R A = 0
have rw₁ : Eq.{v + 2} (α := Cardinal.{v}) ⊥ 0
Tactic: rw [trdeg, ciSup_of_empty, bot_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
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
⊢ trdeg R A = 0
have rw₂ : Eq.{v + 2} (α := Cardinal.{v}) 0 0
Tactic: rw [trdeg, ciSup_of_empty, bot_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
Goal:
σ : Type u_3
R : Type u_4
inst : CommRing R
⊢ AlgebraicIndependent (ι := σ) R (A := MvPolynomial σ R) X
have rw : Injective (α := MvPolynomial σ R) (β := MvPolynomial σ R)
  (⇑(AlgHom.id R (MvPolynomial σ R)) : (a : MvPolynomial σ R) → MvPolynomial σ R)
Tactic: rw [AlgebraicIndependent, aeval_X_left]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (hypothesis)
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
⊢ IsTranscendenceBasis R x ↔ Nonempty ι
have this : Subsingleton A
Tactic: have := Module.subsingleton R A
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
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 ι
have refine : ∀ (h : IsTranscendenceBasis R x), Nonempty ι
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ⟨.of_subsingleton, fun s hs hx ↦
    hx.antisymm fun a _ ↦ ⟨Classical.arbitrary _, Subsingleton.elim ..⟩⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
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
⊢ Nonempty ι
have by_contra! : ∀ (hι : IsEmpty ι), False
Tactic: by_contra! hι
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (hypothesis)
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 ι
⊢ False
have this₁ : range x ⊆ {0} → range x = {0}
Tactic: have := h.2 {0} .of_subsingleton
-- 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
⊢ Eq (α := MvPolynomial ι R →+* A)
    (RingHom.comp (β := MvPolynomial ι K) (AlgHom.toRingHom (aeval x)) (MvPolynomial.map (algebraMap R K)))
    (AlgHom.toRingHom (aeval x))
have 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)
Tactic: ext
-- 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
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)
⊢ Eq (α := MvPolynomial ι R →+* A)
    (RingHom.comp (β := MvPolynomial ι K) (AlgHom.toRingHom (aeval x)) (MvPolynomial.map (algebraMap R K)))
    (AlgHom.toRingHom (aeval x))
have 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)
Tactic: ext