awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
s : Set A
H :
  ∀ t ⊆ s,
    t.Finite → AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ t }) R (Subtype.val (p := fun (x : A) ↦ x ∈ t))
p : MvPolynomial A R
hp : Membership.mem (γ := Subalgebra R (MvPolynomial A R)) (supported R s) p
⊢ Membership.mem (γ := Subalgebra R (MvPolynomial A R)) (supported R (↑p.vars : Set A)) p

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
H : ∀ (t : Set ι), t.Finite → AlgebraicIndependent.{u, u_2, v} R (A := A) fun (i : (↑t : Type u)) ↦ x (↑i : ι)
⊢ AlgebraicIndependent R x

Tactic:
(injective_iff_map_eq_zero _).mpr fun p ↦
    algebraicIndependent_comp_subtype.1 (H _ p.vars.finite_toSet) _ p.mem_supported_vars

Premises used: Iff.mpr, AlgebraicIndependent, MvPolynomial.vars, MvPolynomial.mem_supported_vars, SetLike.coe, injective_iff_map_eq_zero, Iff.mp, Finset.finite_toSet, algebraicIndependent_comp_subtype
-- 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
ι : Type u_3
ι' : Type u_4
s : Set ι
f : ι → ι'
g : ι' → A
hs : AlgebraicIndependent.{u_3, u_2, v} R (A := A) fun (x : (↑s : Type u_3)) ↦ g (f (↑x : ι))
⊢ Nontrivial R

Tactic:
nontriviality R
-- 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
ι : Type u_3
ι' : Type u_4
s : Set ι
f : ι → ι'
g : ι' → A
hs : AlgebraicIndependent.{u_3, u_2, v} R (A := A) fun (x : (↑s : Type u_3)) ↦ g (f (↑x : ι))
h : Nontrivial R
⊢ InjOn f s

Tactic:
have : InjOn f s := injOn_iff_injective.2 hs.injective.of_comp
-- 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
ι : Type u_3
ι' : Type u_4
s : Set ι
f : ι → ι'
g : ι' → A
hs : AlgebraicIndependent.{u_3, u_2, v} R (A := A) fun (x : (↑s : Type u_3)) ↦ g (f (↑x : ι))
h : Nontrivial R
this : InjOn f s
⊢ AlgebraicIndependent.{u_4, u_2, v} R (A := A) fun (x : (↑(f '' s) : Type u_4)) ↦ g (↑x : ι')

Tactic:
(algebraicIndependent_equiv' (Equiv.Set.imageOfInjOn f s this) rfl).1 hs

Premises used: algebraicIndependent_equiv', Equiv.Set.imageOfInjOn, Iff.mp, rfl
-- 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
ι : Type u_3
s : Set ι
f : ι → A
hs : AlgebraicIndependent.{u_3, u_2, v} R (A := A) fun (x : (↑s : Type u_3)) ↦ f (↑x : ι)
⊢ AlgebraicIndependent R (A := A) fun (x : (↑(f '' s) : Type v)) ↦ _root_.id (↑x : A)

Tactic:
AlgebraicIndependent.image_of_comp s f id hs

Premises used: id, AlgebraicIndependent.image_of_comp
-- 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
ι : Type u_3
s : Set ι
f : ι → A
hs : AlgebraicIndependent.{u_3, u_2, v} R (A := A) fun (x : (↑s : Type u_3)) ↦ f (↑x : ι)
⊢ AlgebraicIndependent R (A := A) fun (x : (↑(f '' s) : Type v)) ↦ (↑x : A)

Tactic:
convert! AlgebraicIndependent.image_of_comp s f id hs

Premises used: id, AlgebraicIndependent.image_of_comp
-- 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
η : Type u_3
inst_3 : Nonempty η
s : η → Set A
hs : Directed (fun (x1 x2 : Set A) ↦ x1 ⊆ x2) s
h : ∀ (i : η), AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ s i }) R (Subtype.val (p := fun (x : A) ↦ x ∈ s i))
⊢ AlgebraicIndependent.{v, u_2, v} (ι := { x : A // Membership.mem (γ := Set A) (⋃ (i : η), s i) x }) R
    (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Set A) (⋃ (i : η), s i) x))

Tactic:
algebraicIndependent_of_finite (⋃ i, s i) fun t ht ft => ?_

Premises used: algebraicIndependent_of_finite, Set.iUnion
-- 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
η : Type u_3
inst_3 : Nonempty η
s : η → Set A
hs : Directed (fun (x1 x2 : Set A) ↦ x1 ⊆ x2) s
h : ∀ (i : η), AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ s i }) R (Subtype.val (p := fun (x : A) ↦ x ∈ s i))
refine :
  ∀ (t : Set A) (ht : t ⊆ ⋃ (i : η), s i) (ft : t.Finite),
    AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ t }) R (Subtype.val (p := fun (x : A) ↦ x ∈ t))
⊢ AlgebraicIndependent.{v, u_2, v} (ι := { x : A // Membership.mem (γ := Set A) (⋃ (i : η), s i) x }) R
    (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Set A) (⋃ (i : η), s i) x))

Tactic:
refine algebraicIndependent_of_finite (⋃ i, s i) fun t ht ft => ?_

Premises used: algebraicIndependent_of_finite, Set.iUnion
-- 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
η : Type u_3
inst_3 : Nonempty η
s : η → Set A
hs : Directed (fun (x1 x2 : Set A) ↦ x1 ⊆ x2) s
h : ∀ (i : η), AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ s i }) R (Subtype.val (p := fun (x : A) ↦ x ∈ s i))
t : Set A
ht : t ⊆ ⋃ (i : η), s i
ft : t.Finite
rcases :
  ∀ (I : Set η) (fi : I.Finite) (hI : t ⊆ ⋃ i ∈ I, s i),
    AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ t }) R (Subtype.val (p := fun (x : A) ↦ x ∈ t))
⊢ AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ t }) R (Subtype.val (p := fun (x : A) ↦ x ∈ t))

Tactic:
rcases finite_subset_iUnion ft ht with ⟨I, fi, hI⟩

Premises used: Set.finite_subset_iUnion
-- 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
η : Type u_3
inst_3 : Nonempty η
s : η → Set A
hs : Directed (fun (x1 x2 : Set A) ↦ x1 ⊆ x2) s
h : ∀ (i : η), AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ s i }) R (Subtype.val (p := fun (x : A) ↦ x ∈ s i))
t : Set A
ht : t ⊆ ⋃ (i : η), s i
ft : t.Finite
I : Set η
fi : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
rcases :
  ∀ (i : η) (hi : ∀ i_1 ∈ fi.toFinset (s := I), s i_1 ⊆ s i),
    AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ t }) R (Subtype.val (p := fun (x : A) ↦ x ∈ t))
⊢ AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ t }) R (Subtype.val (p := fun (x : A) ↦ x ∈ t))

Tactic:
rcases hs.finset_le fi.toFinset with ⟨i, hi⟩

Premises used: Set.Finite.toFinset, Directed.finset_le
-- 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
η : Type u_3
inst_3 : Nonempty η
s : η → Set A
hs : Directed (fun (x1 x2 : Set A) ↦ x1 ⊆ x2) s
h : ∀ (i : η), AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ s i }) R (Subtype.val (p := fun (x : A) ↦ x ∈ s i))
t : Set A
ht : t ⊆ ⋃ (i : η), s i
ft : t.Finite
I : Set η
fi : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
i : η
hi : ∀ i_1 ∈ fi.toFinset (s := I), s i_1 ⊆ s i
⊢ AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ t }) R (Subtype.val (p := fun (x : A) ↦ x ∈ t))

Tactic:
(h i).mono (Subset.trans hI <| iUnion₂_subset fun j hj => hi j (fi.mem_toFinset.2 hj))

Premises used: Iff.mpr, Set.iUnion₂_subset, Set.Subset.trans, Set.Finite.mem_toFinset, AlgebraicIndependent.mono
-- 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
η : Type u_3
inst_3 : Nonempty η
s : η → Set A
hs : Directed (fun (x1 x2 : Set A) ↦ x1 ⊆ x2) s
h : ∀ (i : η), AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ s i }) R (Subtype.val (p := fun (x : A) ↦ x ∈ s i))
t : Set A
ht : t ⊆ ⋃ (i : η), s i
ft : t.Finite
I : Set η
fi : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
i : η
hi : ∀ i_1 ∈ fi.toFinset (s := I), s i_1 ⊆ s i
⊢ AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ t }) R (Subtype.val (p := fun (x : A) ↦ x ∈ t))

Tactic:
exact (h i).mono (Subset.trans hI <| iUnion₂_subset fun j hj => hi j (fi.mem_toFinset.2 hj))

Premises used: Iff.mpr, Set.iUnion₂_subset, Set.Subset.trans, Set.Finite.mem_toFinset, AlgebraicIndependent.mono
-- 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
s : Set (Set A)
hsn : s.Nonempty
hs : DirectedOn (fun (x1 x2 : Set A) ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ a }) R (Subtype.val (p := fun (x : A) ↦ x ∈ a))
this : Nonempty.{v + 1} (↑s : Type v) := ⋯
rw :
  AlgebraicIndependent.{v, u_2, v} (ι :=
    { x : A // Membership.mem (γ := Set A) (⋃ (i : (↑s : Type v)), (↑i : Set A)) x }) R
    (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Set A) (⋃ (i : (↑s : Type v)), (↑i : Set A)) x))
⊢ AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ ⋃₀ s }) R (Subtype.val (p := fun (x : A) ↦ x ∈ ⋃₀ s))

Tactic:
rw [sUnion_eq_iUnion]

Premises used: Set.sUnion_eq_iUnion
-- 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
s : Set (Set A)
hsn : s.Nonempty
hs : DirectedOn (fun (x1 x2 : Set A) ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ a }) R (Subtype.val (p := fun (x : A) ↦ x ∈ a))
this : Nonempty.{v + 1} (↑s : Type v) := ⋯
⊢ ∀ (i : (↑s : Type v)),
    AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ (↑i : Set A) }) R
      (Subtype.val (p := fun (x : A) ↦ x ∈ (↑i : Set A)))

Tactic:
simpa using 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
s : Set (Set A)
hsn : s.Nonempty
hs : DirectedOn (fun (x1 x2 : Set A) ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ a }) R (Subtype.val (p := fun (x : A) ↦ x ∈ a))
this : Nonempty.{v + 1} (↑s : Type v) := ⋯
⊢ AlgebraicIndependent.{v, u_2, v} (ι :=
    { x : A // Membership.mem (γ := Set A) (⋃ (i : (↑s : Type v)), (↑i : Set A)) x }) R
    (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Set A) (⋃ (i : (↑s : Type v)), (↑i : Set A)) x))

Tactic:
exact algebraicIndependent_iUnion_of_directed hs.directed_val (by simpa using h)

Premises used: algebraicIndependent_iUnion_of_directed, DirectedOn.directed_val
-- 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
s t : Set A
hst : s ⊆ t
hs : AlgebraicIndepOn R _root_.id s
⊢ ∃ (u : Set A), s ⊆ u ∧ Maximal (fun (x : Set A) ↦ AlgebraicIndepOn R _root_.id x ∧ x ⊆ t) u

Tactic:
zorn_subset_nonempty { u : Set A | AlgebraicIndependent R ((↑) : u → A) ∧ u ⊆ t}
    (fun c hc chainc hcn ↦ ⟨⋃₀ c, ⟨?_, ?_⟩, fun _ ↦ subset_sUnion_of_mem⟩) s ⟨hs, hst⟩

Premises used: AlgebraicIndependent, Set.Mem, setOf, Set.sUnion, HasSubset.Subset, And, zorn_subset_nonempty, And.intro, Exists.intro, Set.subset_sUnion_of_mem, Subtype.val
-- 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
s t : Set A
hst : s ⊆ t
hs : AlgebraicIndepOn R _root_.id s
refine_1 :
  ∀ (c : Set (Set A))
    (hc :
      c ⊆
        {u : Set A |
          AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ u }) R (Subtype.val (p := fun (x : A) ↦ x ∈ u)) ∧
            u ⊆ t})
    (chainc : IsChain (fun (x1 x2 : Set A) ↦ x1 ⊆ x2) c) (hcn : c.Nonempty),
    AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ ⋃₀ c }) R (Subtype.val (p := fun (x : A) ↦ x ∈ ⋃₀ c))
refine_2 :
  ∀ (c : Set (Set A))
    (hc :
      c ⊆
        {u : Set A |
          AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ u }) R (Subtype.val (p := fun (x : A) ↦ x ∈ u)) ∧
            u ⊆ t})
    (chainc : IsChain (fun (x1 x2 : Set A) ↦ x1 ⊆ x2) c) (hcn : c.Nonempty), ⋃₀ c ⊆ t
⊢ ∃ (u : Set A), s ⊆ u ∧ Maximal (fun (x : Set A) ↦ AlgebraicIndepOn R _root_.id x ∧ x ⊆ t) u

Tactic:
refine zorn_subset_nonempty { u : Set A | AlgebraicIndependent R ((↑) : u → A) ∧ u ⊆ t}
    (fun c hc chainc hcn ↦ ⟨⋃₀ c, ⟨?_, ?_⟩, fun _ ↦ subset_sUnion_of_mem⟩) s ⟨hs, hst⟩

Premises used: AlgebraicIndependent, setOf, Set.sUnion, HasSubset.Subset, And, zorn_subset_nonempty, And.intro, Exists.intro, Set.subset_sUnion_of_mem, Subtype.val
-- 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
s t : Set A
hst : s ⊆ t
hs : AlgebraicIndepOn R _root_.id s
c : Set (Set A)
hc :
  c ⊆
    {u : Set A |
      AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ u }) R (Subtype.val (p := fun (x : A) ↦ x ∈ u)) ∧ u ⊆ t}
chainc : IsChain (fun (x1 x2 : Set A) ↦ x1 ⊆ x2) c
hcn : c.Nonempty
⊢ AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ ⋃₀ c }) R (Subtype.val (p := fun (x : A) ↦ x ∈ ⋃₀ c))

Tactic:
algebraicIndependent_sUnion_of_directed hcn chainc.directedOn (fun x hxc ↦ (hc hxc).1)

Premises used: algebraicIndependent_sUnion_of_directed, IsChain.directedOn, And.left
-- 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
s t : Set A
hst : s ⊆ t
hs : AlgebraicIndepOn R _root_.id s
c : Set (Set A)
hc :
  c ⊆
    {u : Set A |
      AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ u }) R (Subtype.val (p := fun (x : A) ↦ x ∈ u)) ∧ u ⊆ t}
chainc : IsChain (fun (x1 x2 : Set A) ↦ x1 ⊆ x2) c
hcn : c.Nonempty
⊢ AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ ⋃₀ c }) R (Subtype.val (p := fun (x : A) ↦ x ∈ ⋃₀ c))

Tactic:
exact algebraicIndependent_sUnion_of_directed hcn chainc.directedOn (fun x hxc ↦ (hc hxc).1)

Premises used: algebraicIndependent_sUnion_of_directed, IsChain.directedOn, And.left
-- 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
s t : Set A
hst : s ⊆ t
hs : AlgebraicIndepOn R _root_.id s
c : Set (Set A)
hc :
  c ⊆
    {u : Set A |
      AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ u }) R (Subtype.val (p := fun (x : A) ↦ x ∈ u)) ∧ u ⊆ t}
chainc : IsChain (fun (x1 x2 : Set A) ↦ x1 ⊆ x2) c
hcn : c.Nonempty
⊢ ⋃₀ c ⊆ t

Tactic:
fun x ⟨w, hyc, hwy⟩ ↦ (hc hyc).2 hwy

Premises used: Membership.mem, Set.Subset, _private.0.exists_maximal_algebraicIndependent.match_1, And.right
-- 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
s t : Set A
hst : s ⊆ t
hs : AlgebraicIndepOn R _root_.id s
c : Set (Set A)
hc :
  c ⊆
    {u : Set A |
      AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ u }) R (Subtype.val (p := fun (x : A) ↦ x ∈ u)) ∧ u ⊆ t}
chainc : IsChain (fun (x1 x2 : Set A) ↦ x1 ⊆ x2) c
hcn : c.Nonempty
⊢ ⋃₀ c ⊆ t

Tactic:
exact fun x ⟨w, hyc, hwy⟩ ↦ (hc hyc).2 hwy
-- 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
⊢ Eq (α := Ideal ↥(adjoin R (range x)))
    (RingHom.ker (F := ↥(adjoin R (range x)) →+* MvPolynomial ι R)
      (↑hx.repr : ↥(adjoin R (range x)) →+* MvPolynomial ι R))
    ⊥

Tactic:
(RingHom.injective_iff_ker_eq_bot _).1 (AlgEquiv.injective _)

Premises used: Subsemiring.mk', Subsemiring.closure, Set.Mem, RingHom.injective_iff_ker_eq_bot, Iff.mp, AlgEquiv.injective
-- 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
y : MvPolynomial.{u, u_2} (Option ι) R
⊢ Eq.{v + 1} (α := Polynomial ↥(adjoin R (range x)))
    ((hx.mvPolynomialOptionEquivPolynomialAdjoin : (a : MvPolynomial (Option ι) R) → Polynomial ↥(adjoin R (range x)))
        y :
      Polynomial ↥(adjoin R (range x)))
    (Polynomial.map (↑hx.aevalEquiv : MvPolynomial ι R →+* ↥(adjoin R (range x)))
        ((aeval fun (o : Option ι) ↦
              o.elim Polynomial.X fun (s : ι) ↦
                (Polynomial.C : (a : MvPolynomial ι R) → Polynomial (MvPolynomial ι R)) (X s) :
            (a : MvPolynomial (Option ι) R) → Polynomial (MvPolynomial ι R))
          y) :
      Polynomial ↥(adjoin R (range x)))

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂, AlgebraicIndependent.aevalEquiv, MonoidHomClass.toMonoidHom, AlgEquiv.trans, RingHomClass.toRingHom, Polynomial.map, Finset.sum, 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
hx : AlgebraicIndependent R x
r : R
h :
  Eq.{v + 1} (α := ↥(adjoin R (range x)))
    ((hx.aevalEquiv : (a : MvPolynomial ι R) → ↥(adjoin R (range x))) ((C : (a : R) → MvPolynomial ι R) r) :
      ↥(adjoin R (range x)))
    ((algebraMap R ↥(adjoin R (range x)) : (a : R) → ↥(adjoin R (range x))) r : ↥(adjoin R (range x)))
⊢ Eq.{v + 1} (α := Polynomial ↥(adjoin R (range x)))
    ((Polynomial.C : (a : ↥(adjoin R (range x))) → Polynomial ↥(adjoin R (range x)))
        ((hx.aevalEquiv : (a : MvPolynomial ι R) → ↥(adjoin R (range x))) ((C : (a : R) → MvPolynomial ι R) r)) :
      Polynomial ↥(adjoin R (range x)))
    ((Polynomial.C : (a : ↥(adjoin R (range x))) → Polynomial ↥(adjoin R (range x)))
        ((algebraMap R ↥(adjoin R (range x)) : (a : R) → ↥(adjoin R (range x))) r) :
      Polynomial ↥(adjoin R (range x)))

Tactic:
congr
-- 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
r : R
⊢ Injective.{max 1 (v + 1), v + 1} (α := ↥(adjoin R (range x)))
    (Subtype.val (p := fun (x_1 : A) ↦ Membership.mem (γ := Subalgebra R A) (adjoin R (range x)) x_1))

Tactic:
Subtype.val_injective

Premises used: Subtype.val_injective
-- 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
r : R
h :
  Eq.{v + 1} (α := A)
    (↑((hx.aevalEquiv : (a : MvPolynomial ι R) → ↥(adjoin R (range x))) ((C : (a : R) → MvPolynomial ι R) r)) : A)
    (↑((algebraMap R ↥(adjoin R (range x)) : (a : R) → ↥(adjoin R (range x))) r) : A)
⊢ Eq.{v + 1} (α := ↥(adjoin R (range x)))
    ((hx.aevalEquiv : (a : MvPolynomial ι R) → ↥(adjoin R (range x))) ((C : (a : R) → MvPolynomial ι R) r) :
      ↥(adjoin R (range x)))
    ((algebraMap R ↥(adjoin R (range x)) : (a : R) → ↥(adjoin R (range x))) r : ↥(adjoin R (range x)))

Tactic:
apply_fun Subtype.val using Subtype.val_injective

Premises used: Subtype.val_injective, Subtype.val
-- 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
r : R
⊢ Eq.{v + 1} (α := A)
    (↑((hx.aevalEquiv : (a : MvPolynomial ι R) → ↥(adjoin R (range x))) ((C : (a : R) → MvPolynomial ι R) r)) : A)
    (↑((algebraMap R ↥(adjoin R (range x)) : (a : R) → ↥(adjoin R (range x))) r) : A)

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
hx : AlgebraicIndependent R x
r : R
⊢ Eq.{v + 1} (α := Polynomial ↥(adjoin R (range x)))
    ((hx.mvPolynomialOptionEquivPolynomialAdjoin : (a : MvPolynomial (Option ι) R) → Polynomial ↥(adjoin R (range x)))
        ((C : (a : R) → MvPolynomial (Option ι) R) r) :
      Polynomial ↥(adjoin R (range x)))
    ((Polynomial.C : (a : ↥(adjoin R (range x))) → Polynomial ↥(adjoin R (range x)))
        ((algebraMap R ↥(adjoin R (range x)) : (a : R) → ↥(adjoin R (range x))) r) :
      Polynomial ↥(adjoin R (range x)))

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
hx : AlgebraicIndependent R x
rw :
  Eq (α := Polynomial ↥(adjoin R (range x)))
    (Polynomial.map (↑hx.aevalEquiv : MvPolynomial ι R →+* ↥(adjoin R (range x)))
      ((aeval fun (o : Option ι) ↦
            o.elim Polynomial.X fun (s : ι) ↦
              (Polynomial.C : (a : MvPolynomial ι R) → Polynomial (MvPolynomial ι R)) (X s) :
          (a : MvPolynomial (Option ι) R) → Polynomial (MvPolynomial ι R))
        (X none)))
    Polynomial.X
rw₁ :
  Eq (α := Polynomial ↥(adjoin R (range x)))
    (Polynomial.map (↑hx.aevalEquiv : MvPolynomial ι R →+* ↥(adjoin R (range x)))
      (Option.elim none Polynomial.X fun (s : ι) ↦
        (Polynomial.C : (a : MvPolynomial ι R) → Polynomial (MvPolynomial ι R)) (X s)))
    Polynomial.X
rw₂ :
  Eq (α := Polynomial ↥(adjoin R (range x)))
    (Polynomial.map (↑hx.aevalEquiv : MvPolynomial ι R →+* ↥(adjoin R (range x))) Polynomial.X) Polynomial.X
rw₃ rw₄ : Eq.{v + 1} (α := Polynomial ↥(adjoin R (range x))) Polynomial.X Polynomial.X
⊢ Eq.{v + 1} (α := Polynomial ↥(adjoin R (range x)))
    ((hx.mvPolynomialOptionEquivPolynomialAdjoin : (a : MvPolynomial (Option ι) R) → Polynomial ↥(adjoin R (range x)))
        (X none) :
      Polynomial ↥(adjoin R (range x)))
    (Polynomial.X : Polynomial ↥(adjoin R (range x)))

Tactic:
rw [AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply, aeval_X, Option.elim,
    Polynomial.map_X]

Premises used: MvPolynomial.aeval_X, Polynomial.map_X, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply, Option.elim
-- 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
a : A
⊢ Eq (α := MvPolynomial.{u, u_2} (Option ι) R →+* A)
    (RingHom.comp (↑(Polynomial.aeval a) : Polynomial ↥(adjoin R (range x)) →+* A)
      hx.mvPolynomialOptionEquivPolynomialAdjoin.toRingHom)
    (↑(aeval fun (o : Option ι) ↦ o.elim a x) : MvPolynomial (Option ι) R →+* A)

Tactic:
MvPolynomial.ringHom_ext ?_ ?_

Premises used: MvPolynomial.ringHom_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
hx : AlgebraicIndependent R x
a : A
refine_1 :
  ∀ (r : R),
    Eq.{v + 1} (α := A)
      ((RingHom.comp (↑(Polynomial.aeval a) : Polynomial ↥(adjoin R (range x)) →+* A)
              hx.mvPolynomialOptionEquivPolynomialAdjoin.toRingHom :
            (a : MvPolynomial (Option ι) R) → A)
          ((C : (a : R) → MvPolynomial (Option ι) R) r : MvPolynomial.{u, u_2} (Option ι) R) :
        A)
      (((↑(aeval fun (o : Option ι) ↦ o.elim a x) : MvPolynomial (Option ι) R →+* A) :
            (a : MvPolynomial (Option ι) R) → A)
          ((C : (a : R) → MvPolynomial (Option ι) R) r : MvPolynomial.{u, u_2} (Option ι) R) :
        A)
refine_2 :
  ∀ (i : Option ι),
    Eq.{v + 1} (α := A)
      ((RingHom.comp (↑(Polynomial.aeval a) : Polynomial ↥(adjoin R (range x)) →+* A)
              hx.mvPolynomialOptionEquivPolynomialAdjoin.toRingHom :
            (a : MvPolynomial (Option ι) R) → A)
          (X i) :
        A)
      (((↑(aeval fun (o : Option ι) ↦ o.elim a x) : MvPolynomial (Option ι) R →+* A) :
            (a : MvPolynomial (Option ι) R) → A)
          (X i) :
        A)
⊢ Eq (α := MvPolynomial.{u, u_2} (Option ι) R →+* A)
    (RingHom.comp (↑(Polynomial.aeval a) : Polynomial ↥(adjoin R (range x)) →+* A)
      hx.mvPolynomialOptionEquivPolynomialAdjoin.toRingHom)
    (↑(aeval fun (o : Option ι) ↦ o.elim a x) : MvPolynomial (Option ι) R →+* A)

Tactic:
refine MvPolynomial.ringHom_ext ?_ ?_

Premises used: MvPolynomial.ringHom_ext