awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hx : AlgebraicIndependent R x
inst_3 : Nontrivial A
s : Set ι
i : ι
⊢ (AlgebraicIndependent.{u_1, v, v} ↥(adjoin R (x '' s)) (A := A) fun (i_1 : (↑{i} : Type u_1)) ↦ x (↑i_1 : ι)) ↔
    Disjoint s {i}

Tactic:
hx.adjoin_iff_disjoint (t := { i })

Premises used: AlgebraicIndependent.adjoin_iff_disjoint
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hx : AlgebraicIndependent R x
inst_3 : Nontrivial A
s : Set ι
i : ι
h :
  (AlgebraicIndependent.{u_1, v, v} ↥(adjoin R (x '' s)) (A := A) fun (i_1 : (↑{i} : Type u_1)) ↦ x (↑i_1 : ι)) ↔
    Transcendental (↥(adjoin R (x '' s))) (x i)
⊢ Transcendental (↥(adjoin R (x '' s))) (x i) ↔ Disjoint s {i}

Tactic:
convert! ← hx.adjoin_iff_disjoint (t := { i })

Premises used: AlgebraicIndependent.adjoin_iff_disjoint
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hx : AlgebraicIndependent R x
inst_3 : Nontrivial A
s : Set ι
i : ι
h h₁ :
  Transcendental (↥(adjoin R (x '' s)))
      (x (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i} x) i ⋯) : ι)) ↔
    Transcendental (↥(adjoin R (x '' s))) (x i)
⊢ (AlgebraicIndependent.{u_1, v, v} ↥(adjoin R (x '' s)) (A := A) fun (i_1 : (↑{i} : Type u_1)) ↦ x (↑i_1 : ι)) ↔
    Transcendental (↥(adjoin R (x '' s))) (x i)

Tactic:
rw [algebraicIndependent_singleton_iff ⟨i, rfl⟩]

Premises used: algebraicIndependent_singleton_iff
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
R : Type u_3
S : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Nontrivial R
inst_8 : FaithfulSMul R S
inst_9 : FaithfulSMul S A
simp_rw :
  HAdd.hAdd (α := Cardinal.{max u v})
      (⨆ (i : { s : Set S // AlgebraicIndepOn R _root_.id s }), lift.{v, u} #(↑(↑i : Set S) : Type u))
      (⨆ (i : { s : Set A // AlgebraicIndepOn S _root_.id s }), lift.{u, v} #(↑(↑i : Set A) : Type v)) ≤
    ⨆ (i : { s : Set A // AlgebraicIndepOn R _root_.id s }), lift.{u, v} #(↑(↑i : Set A) : Type v)
⊢ lift.{v, u} (trdeg R S) + lift.{u, v} (trdeg S A) ≤ lift.{u, v} (trdeg R A)

Tactic:
simp_rw [trdeg, lift_iSup bddAbove_of_small]

Premises used: Cardinal.lift_iSup, Algebra.trdeg, Cardinal.bddAbove_of_small
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
R : Type u_3
S : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Nontrivial R
inst_8 : FaithfulSMul R S
inst_9 : FaithfulSMul S A
simp_rw :
  LE.le (α := Cardinal.{max u v})
    (⨆ (i : { s : Set S // AlgebraicIndepOn R _root_.id s }),
      ⨆ (j : { s : Set A // AlgebraicIndepOn S _root_.id s }),
        #(Sum.{v, u} (↑(↑j : Set A) : Type v) (↑(↑i : Set S) : Type u)))
    (⨆ (i : { s : Set A // AlgebraicIndepOn R _root_.id s }), lift.{u, v} #(↑(↑i : Set A) : Type v))
⊢ HAdd.hAdd (α := Cardinal.{max u v})
      (⨆ (i : { s : Set S // AlgebraicIndepOn R _root_.id s }), lift.{v, u} #(↑(↑i : Set S) : Type u))
      (⨆ (i : { s : Set A // AlgebraicIndepOn S _root_.id s }), lift.{u, v} #(↑(↑i : Set A) : Type v)) ≤
    ⨆ (i : { s : Set A // AlgebraicIndepOn R _root_.id s }), lift.{u, v} #(↑(↑i : Set A) : Type v)

Tactic:
simp_rw [Cardinal.ciSup_add_ciSup _ bddAbove_of_small _ bddAbove_of_small,
    add_comm (lift.{v, u} _), ← mk_sum]

Premises used: Cardinal.mk_sum, Cardinal.bddAbove_of_small, Cardinal.ciSup_add_ciSup
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
R : Type u_3
S : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Nontrivial R
inst_8 : FaithfulSMul R S
inst_9 : FaithfulSMul S A
⊢ LE.le (α := Cardinal.{max u v})
    (⨆ (i : { s : Set S // AlgebraicIndepOn R _root_.id s }),
      ⨆ (j : { s : Set A // AlgebraicIndepOn S _root_.id s }),
        #(Sum.{v, u} (↑(↑j : Set A) : Type v) (↑(↑i : Set S) : Type u)))
    (⨆ (i : { s : Set A // AlgebraicIndepOn R _root_.id s }), lift.{u, v} #(↑(↑i : Set A) : Type v))

Tactic:
ciSup_le fun ⟨s, hs⟩ ↦ ciSup_le fun ⟨t, ht⟩ ↦ ?_

Premises used: iSup, Cardinal.lift, Cardinal.mk, Set.Elem, Sum, _private.0.lift_trdeg_add_le.match_1, LE.le, Subtype.mk, Subtype.val, ciSup_le
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
R : Type u_3
S : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Nontrivial R
inst_8 : FaithfulSMul R S
inst_9 : FaithfulSMul S A
refine :
  ∀ (x : { s : Set S // AlgebraicIndepOn R _root_.id s }) (s : Set S) (hs : AlgebraicIndepOn R _root_.id s)
    (x : { s : Set A // AlgebraicIndepOn S _root_.id s }) (t : Set A) (ht : AlgebraicIndepOn S _root_.id t),
    #(Sum.{v, u} (↑(↑(Subtype.mk (p := fun (s : Set A) ↦ AlgebraicIndepOn S _root_.id s) t ht) : Set A) : Type v)
          (↑(↑(Subtype.mk (p := fun (s : Set S) ↦ AlgebraicIndepOn R _root_.id s) s hs) : Set S) : Type u)) ≤
      ⨆ (i : { s : Set A // AlgebraicIndepOn R _root_.id s }), lift.{u, v} #(↑(↑i : Set A) : Type v)
⊢ LE.le (α := Cardinal.{max u v})
    (⨆ (i : { s : Set S // AlgebraicIndepOn R _root_.id s }),
      ⨆ (j : { s : Set A // AlgebraicIndepOn S _root_.id s }),
        #(Sum.{v, u} (↑(↑j : Set A) : Type v) (↑(↑i : Set S) : Type u)))
    (⨆ (i : { s : Set A // AlgebraicIndepOn R _root_.id s }), lift.{u, v} #(↑(↑i : Set A) : Type v))

Tactic:
refine ciSup_le fun ⟨s, hs⟩ ↦ ciSup_le fun ⟨t, ht⟩ ↦ ?_

Premises used: ciSup_le
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
R : Type u_3
S : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Nontrivial R
inst_8 : FaithfulSMul R S
inst_9 : FaithfulSMul S A
x : { s : Set S // AlgebraicIndepOn R _root_.id s }
s : Set S
hs : AlgebraicIndepOn R _root_.id s
x_1 : { s : Set A // AlgebraicIndepOn S _root_.id s }
t : Set A
ht : AlgebraicIndepOn S _root_.id t
⊢ AlgebraicIndependent (ι := Sum.{v, u} (↑t : Type v) (↑s : Type u)) R (A := A)
    (Sum.elim (fun (i : (↑t : Type v)) ↦ _root_.id (↑i : A))
      (Function.comp (β := S) (⇑(algebraMap S A) : (a : S) → A) fun (i : (↑s : Type u)) ↦ _root_.id (↑i : S)))

Tactic:
have := hs.sumElim_comp ht
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
R : Type u_3
S : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Nontrivial R
inst_8 : FaithfulSMul R S
inst_9 : FaithfulSMul S A
x : { s : Set S // AlgebraicIndepOn R _root_.id s }
s : Set S
hs : AlgebraicIndepOn R _root_.id s
x_1 : { s : Set A // AlgebraicIndepOn S _root_.id s }
t : Set A
ht : AlgebraicIndepOn S _root_.id t
this :
  AlgebraicIndependent (ι := Sum.{v, u} (↑t : Type v) (↑s : Type u)) R (A := A)
    (Sum.elim (fun (i : (↑t : Type v)) ↦ _root_.id (↑i : A))
      (Function.comp (β := S) (⇑(algebraMap S A) : (a : S) → A) fun (i : (↑s : Type u)) ↦ _root_.id (↑i : S)))
⊢ #(Sum.{v, u} (↑(↑(Subtype.mk (p := fun (s : Set A) ↦ AlgebraicIndepOn S _root_.id s) t ht) : Set A) : Type v)
        (↑(↑(Subtype.mk (p := fun (s : Set S) ↦ AlgebraicIndepOn R _root_.id s) s hs) : Set S) : Type u)) ≤
    ⨆ (i : { s : Set A // AlgebraicIndepOn R _root_.id s }), lift.{u, v} #(↑(↑i : Set A) : Type v)

Tactic:
le_ciSup_of_le bddAbove_of_small ⟨_, this.to_subtype_range⟩ ?_

Premises used: le_ciSup_of_le, Subtype.mk, Cardinal.bddAbove_of_small, AlgebraicIndependent.to_subtype_range
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
R : Type u_3
S : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Nontrivial R
inst_8 : FaithfulSMul R S
inst_9 : FaithfulSMul S A
x : { s : Set S // AlgebraicIndepOn R _root_.id s }
s : Set S
hs : AlgebraicIndepOn R _root_.id s
x_1 : { s : Set A // AlgebraicIndepOn S _root_.id s }
t : Set A
ht : AlgebraicIndepOn S _root_.id t
this :
  AlgebraicIndependent (ι := Sum.{v, u} (↑t : Type v) (↑s : Type u)) R (A := A)
    (Sum.elim (fun (i : (↑t : Type v)) ↦ _root_.id (↑i : A))
      (Function.comp (β := S) (⇑(algebraMap S A) : (a : S) → A) fun (i : (↑s : Type u)) ↦ _root_.id (↑i : S)))
refine :
  #(Sum.{v, u} (↑(↑(Subtype.mk (p := fun (s : Set A) ↦ AlgebraicIndepOn S _root_.id s) t ht) : Set A) : Type v)
        (↑(↑(Subtype.mk (p := fun (s : Set S) ↦ AlgebraicIndepOn R _root_.id s) s hs) : Set S) : Type u)) ≤
    lift.{u, v}
      #(↑(↑(Subtype.mk (p := fun (s : Set A) ↦ AlgebraicIndepOn R _root_.id s)
                  (range (ι := Sum.{v, u} (↑t : Type v) (↑s : Type u))
                    (Sum.elim (fun (i : (↑t : Type v)) ↦ _root_.id (↑i : A))
                      (Function.comp (β := S) (⇑(algebraMap S A) : (a : S) → A) fun (i : (↑s : Type u)) ↦
                        _root_.id (↑i : S))))
                  ⋯) :
              Set A) :
          Type v)
⊢ #(Sum.{v, u} (↑(↑(Subtype.mk (p := fun (s : Set A) ↦ AlgebraicIndepOn S _root_.id s) t ht) : Set A) : Type v)
        (↑(↑(Subtype.mk (p := fun (s : Set S) ↦ AlgebraicIndepOn R _root_.id s) s hs) : Set S) : Type u)) ≤
    ⨆ (i : { s : Set A // AlgebraicIndepOn R _root_.id s }), lift.{u, v} #(↑(↑i : Set A) : Type v)

Tactic:
refine le_ciSup_of_le bddAbove_of_small ⟨_, this.to_subtype_range⟩ ?_

Premises used: le_ciSup_of_le, Cardinal.bddAbove_of_small
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
R : Type u_3
S : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Nontrivial R
inst_8 : FaithfulSMul R S
inst_9 : FaithfulSMul S A
x : { s : Set S // AlgebraicIndepOn R _root_.id s }
s : Set S
hs : AlgebraicIndepOn R _root_.id s
x_1 : { s : Set A // AlgebraicIndepOn S _root_.id s }
t : Set A
ht : AlgebraicIndepOn S _root_.id t
this :
  AlgebraicIndependent (ι := Sum.{v, u} (↑t : Type v) (↑s : Type u)) R (A := A)
    (Sum.elim (fun (i : (↑t : Type v)) ↦ _root_.id (↑i : A))
      (Function.comp (β := S) (⇑(algebraMap S A) : (a : S) → A) fun (i : (↑s : Type u)) ↦ _root_.id (↑i : S)))
rw :
  #(Sum.{v, u} (↑(↑(Subtype.mk (p := fun (s : Set A) ↦ AlgebraicIndepOn S _root_.id s) t ht) : Set A) : Type v)
        (↑(↑(Subtype.mk (p := fun (s : Set S) ↦ AlgebraicIndepOn R _root_.id s) s hs) : Set S) : Type u)) ≤
    lift.{max v u, v}
      #(↑(↑(Subtype.mk (p := fun (s : Set A) ↦ AlgebraicIndepOn R _root_.id s)
                  (range (ι := Sum.{v, u} (↑t : Type v) (↑s : Type u))
                    (Sum.elim (fun (i : (↑t : Type v)) ↦ _root_.id (↑i : A))
                      (Function.comp (β := S) (⇑(algebraMap S A) : (a : S) → A) fun (i : (↑s : Type u)) ↦
                        _root_.id (↑i : S))))
                  ⋯) :
              Set A) :
          Type v)
rw₁ :
  #(Sum.{v, u} (↑(↑(Subtype.mk (p := fun (s : Set A) ↦ AlgebraicIndepOn S _root_.id s) t ht) : Set A) : Type v)
        (↑(↑(Subtype.mk (p := fun (s : Set S) ↦ AlgebraicIndepOn R _root_.id s) s hs) : Set S) : Type u)) ≤
    lift.{v, max u v} #(Sum.{v, u} (↑t : Type v) (↑s : Type u))
rw₂ rw₃ :
  #(Sum.{v, u} (↑(↑(Subtype.mk (p := fun (s : Set A) ↦ AlgebraicIndepOn S _root_.id s) t ht) : Set A) : Type v)
        (↑(↑(Subtype.mk (p := fun (s : Set S) ↦ AlgebraicIndepOn R _root_.id s) s hs) : Set S) : Type u)) ≤
    #(Sum.{v, u} (↑(↑(Subtype.mk (p := fun (s : Set A) ↦ AlgebraicIndepOn S _root_.id s) t ht) : Set A) : Type v)
        (↑(↑(Subtype.mk (p := fun (s : Set S) ↦ AlgebraicIndepOn R _root_.id s) s hs) : Set S) : Type u))
⊢ #(Sum.{v, u} (↑(↑(Subtype.mk (p := fun (s : Set A) ↦ AlgebraicIndepOn S _root_.id s) t ht) : Set A) : Type v)
        (↑(↑(Subtype.mk (p := fun (s : Set S) ↦ AlgebraicIndepOn R _root_.id s) s hs) : Set S) : Type u)) ≤
    lift.{u, v}
      #(↑(↑(Subtype.mk (p := fun (s : Set A) ↦ AlgebraicIndepOn R _root_.id s)
                  (range (ι := Sum.{v, u} (↑t : Type v) (↑s : Type u))
                    (Sum.elim (fun (i : (↑t : Type v)) ↦ _root_.id (↑i : A))
                      (Function.comp (β := S) (⇑(algebraMap S A) : (a : S) → A) fun (i : (↑s : Type u)) ↦
                        _root_.id (↑i : S))))
                  ⋯) :
              Set A) :
          Type v)

Tactic:
rw [← lift_umax, mk_range_eq_of_injective this.injective, lift_id']

Premises used: Cardinal.mk_range_eq_of_injective, Cardinal.lift_id', Cardinal.lift_umax, AlgebraicIndependent.injective
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
R : Type u_3
S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Nontrivial R
A : Type u
inst_4 : CommRing A
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : FaithfulSMul R S
inst_8 : FaithfulSMul S A
inst_9 : IsScalarTower R S A
rw : Cardinal.lift.{u, u} (trdeg R S) + Cardinal.lift.{u, u} (trdeg S A) ≤ Cardinal.lift.{u, u} (trdeg R A)
⊢ trdeg R S + trdeg S A ≤ trdeg R A

Tactic:
rw [← (trdeg R S).lift_id, ← (trdeg S A).lift_id, ← (trdeg R A).lift_id]

Premises used: Algebra.trdeg, Cardinal.lift_id
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
R : Type u_3
S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Nontrivial R
A : Type u
inst_4 : CommRing A
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : FaithfulSMul R S
inst_8 : FaithfulSMul S A
inst_9 : IsScalarTower R S A
⊢ Cardinal.lift.{u, u} (trdeg R S) + Cardinal.lift.{u, u} (trdeg S A) ≤ Cardinal.lift.{u, u} (trdeg R A)

Tactic:
lift_trdeg_add_le

Premises used: lift_trdeg_add_le
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
R : Type u_3
S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Nontrivial R
A : Type u
inst_4 : CommRing A
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : FaithfulSMul R S
inst_8 : FaithfulSMul S A
inst_9 : IsScalarTower R S A
⊢ Cardinal.lift.{u, u} (trdeg R S) + Cardinal.lift.{u, u} (trdeg S A) ≤ Cardinal.lift.{u, u} (trdeg R A)

Tactic:
exact lift_trdeg_add_le

Premises used: lift_trdeg_add_le
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
ι : Type u_1
R : Type u_3
inst : CommRing R
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
set :
  let x : (i : ι) → MvPolynomial ι R := fun (i : ι) ↦
    (Polynomial.aeval (X i) : (a : Polynomial R) → MvPolynomial ι R) (f i);
  AlgebraicIndependent R x
⊢ AlgebraicIndependent R (A := MvPolynomial ι R) fun (i : ι) ↦
    (Polynomial.aeval (X i) : (a : Polynomial R) → MvPolynomial ι R) (f i)

Tactic:
set x := fun i ↦ Polynomial.aeval (X i : MvPolynomial ι R) (f i)

Premises used: MvPolynomial.X, Polynomial.aeval, DFunLike.coe
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
ι : Type u_1
R : Type u_3
inst : CommRing R
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x : (i : ι) → MvPolynomial ι R := fun (i : ι) ↦ (Polynomial.aeval (X i) : (a : Polynomial R) → MvPolynomial ι R) (f i)
⊢ AlgebraicIndependent R x

Tactic:
algebraicIndependent_of_finite_type' (C_injective _ _) fun t _ _ i hi ↦ ?_

Premises used: algebraicIndependent_of_finite_type', MvPolynomial.C_injective
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
ι : Type u_1
R : Type u_3
inst : CommRing R
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x : (i : ι) → MvPolynomial ι R := fun (i : ι) ↦ (Polynomial.aeval (X i) : (a : Polynomial R) → MvPolynomial ι R) (f i)
refine :
  ∀ (t : Set ι),
    t.Finite →
      (AlgebraicIndependent R (A := MvPolynomial ι R) fun (i : (↑t : Type u_1)) ↦ x (↑i : ι)) →
        ∀ (i : ι) (hi : i ∉ t), Transcendental (↥(adjoin R (x '' t))) (x i)
⊢ AlgebraicIndependent R x

Tactic:
refine algebraicIndependent_of_finite_type' (C_injective _ _) fun t _ _ i hi ↦ ?_

Premises used: algebraicIndependent_of_finite_type'
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
ι : Type u_1
R : Type u_3
inst : CommRing R
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x : (i : ι) → MvPolynomial ι R := fun (i : ι) ↦ (Polynomial.aeval (X i) : (a : Polynomial R) → MvPolynomial ι R) (f i)
t : Set ι
h : t.Finite
h_1 : AlgebraicIndependent R (A := MvPolynomial ι R) fun (i : (↑t : Type u_1)) ↦ x (↑i : ι)
i : ι
hi : i ∉ t
rw : t ⊆ x ⁻¹' (↑(supported R t) : Set (MvPolynomial ι R))
⊢ adjoin R (x '' t) ≤ supported R t

Tactic:
rw [Algebra.adjoin_le_iff, Set.image_subset_iff]

Premises used: Algebra.adjoin_le_iff, Set.image_subset_iff
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
ι : Type u_1
R : Type u_3
inst : CommRing R
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x : (i : ι) → MvPolynomial ι R := fun (i : ι) ↦ (Polynomial.aeval (X i) : (a : Polynomial R) → MvPolynomial ι R) (f i)
t : Set ι
h_1 : t.Finite
h_2 : AlgebraicIndependent R (A := MvPolynomial ι R) fun (i : (↑t : Type u_1)) ↦ x (↑i : ι)
i : ι
hi : i ∉ t
a : ι
h : a ∈ t
⊢ x a ∈ (↑(supported R t) : Set (MvPolynomial ι R))

Tactic:
Algebra.adjoin_mono ?_ (Polynomial.aeval_mem_adjoin_singleton R _)

Premises used: Set.Mem, setOf, Algebra.adjoin_mono, Polynomial.aeval_mem_adjoin_singleton
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
ι : Type u_1
R : Type u_3
inst : CommRing R
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x : (i : ι) → MvPolynomial ι R := fun (i : ι) ↦ (Polynomial.aeval (X i) : (a : Polynomial R) → MvPolynomial ι R) (f i)
t : Set ι
h_1 : t.Finite
h_2 : AlgebraicIndependent R (A := MvPolynomial ι R) fun (i : (↑t : Type u_1)) ↦ x (↑i : ι)
i : ι
hi : i ∉ t
a : ι
h : a ∈ t
refine : Subset (α := Set (MvPolynomial ι R)) {X a} (X '' t)
⊢ x a ∈ (↑(supported R t) : Set (MvPolynomial ι R))

Tactic:
refine Algebra.adjoin_mono ?_ (Polynomial.aeval_mem_adjoin_singleton R _)

Premises used: Algebra.adjoin_mono, Polynomial.aeval_mem_adjoin_singleton
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
ι : Type u_1
R : Type u_3
inst : CommRing R
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x : (i : ι) → MvPolynomial ι R := fun (i : ι) ↦ (Polynomial.aeval (X i) : (a : Polynomial R) → MvPolynomial ι R) (f i)
t : Set ι
h_1 : t.Finite
h_2 : AlgebraicIndependent R (A := MvPolynomial ι R) fun (i : (↑t : Type u_1)) ↦ x (↑i : ι)
i : ι
hi : i ∉ t
a : ι
h : a ∈ t
simp_rw : Membership.mem (γ := Set (MvPolynomial ι R)) (X '' t) (X a)
⊢ Subset (α := Set (MvPolynomial ι R)) {X a} (X '' t)

Tactic:
simp_rw [singleton_subset_iff, Set.mem_image_of_mem _ h]

Premises used: Set.singleton_subset_iff, Set.mem_image_of_mem
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
ι : Type u_1
R : Type u_3
inst : CommRing R
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x : (i : ι) → MvPolynomial ι R := fun (i : ι) ↦ (Polynomial.aeval (X i) : (a : Polynomial R) → MvPolynomial ι R) (f i)
t : Set ι
h : t.Finite
h_1 : AlgebraicIndependent R (A := MvPolynomial ι R) fun (i : (↑t : Type u_1)) ↦ x (↑i : ι)
i : ι
hi : i ∉ t
⊢ adjoin R (x '' t) ≤ supported R t

Tactic:
have hle : adjoin R (x '' t) ≤ supported R t := by
    rw [Algebra.adjoin_le_iff, Set.image_subset_iff]
    intro _ h
    rw [Set.mem_preimage]
    refine Algebra.adjoin_mono ?_ (Polynomial.aeval_mem_adjoin_singleton R _)
    simp_rw [singleton_subset_iff, Set.mem_image_of_mem _ h]
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
ι : Type u_1
R : Type u_3
inst : CommRing R
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x : (i : ι) → MvPolynomial ι R := fun (i : ι) ↦ (Polynomial.aeval (X i) : (a : Polynomial R) → MvPolynomial ι R) (f i)
t : Set ι
h : t.Finite
h_1 : AlgebraicIndependent R (A := MvPolynomial ι R) fun (i : (↑t : Type u_1)) ↦ x (↑i : ι)
i : ι
hi : i ∉ t
hle : adjoin R (x '' t) ≤ supported R t
⊢ Transcendental (↥(adjoin R (x '' t))) (x i)

Tactic:
(transcendental_supported_polynomial_aeval_X R hi (hf i)).of_tower_top_of_subalgebra_le hle

Premises used: Set.Mem, setOf, Transcendental.of_tower_top_of_subalgebra_le, MvPolynomial.transcendental_supported_polynomial_aeval_X
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
ι : Type u_1
R : Type u_3
inst : CommRing R
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x : (i : ι) → MvPolynomial ι R := fun (i : ι) ↦ (Polynomial.aeval (X i) : (a : Polynomial R) → MvPolynomial ι R) (f i)
t : Set ι
h : t.Finite
h_1 : AlgebraicIndependent R (A := MvPolynomial ι R) fun (i : (↑t : Type u_1)) ↦ x (↑i : ι)
i : ι
hi : i ∉ t
hle : adjoin R (x '' t) ≤ supported R t
⊢ Transcendental (↥(adjoin R (x '' t))) (x i)

Tactic:
exact (transcendental_supported_polynomial_aeval_X R hi (hf i)).of_tower_top_of_subalgebra_le hle

Premises used: Transcendental.of_tower_top_of_subalgebra_le, MvPolynomial.transcendental_supported_polynomial_aeval_X
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hx : AlgebraicIndependent R x
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
⊢ AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : ι) ↦
    (aeval x : (a : MvPolynomial ι R) → A)
      ((Polynomial.aeval (X i) : (a : Polynomial R) → MvPolynomial ι R) (f i) : MvPolynomial ι R)

Tactic:
aeval_of_algebraicIndependent hx (algebraicIndependent_polynomial_aeval_X _ hf)

Premises used: MvPolynomial.algebraicIndependent_polynomial_aeval_X, AlgebraicIndependent.aeval_of_algebraicIndependent
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hx : AlgebraicIndependent R x
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
h :
  ∀ (x_1 : ι),
    Eq.{v + 1} (α := A) ((Polynomial.aeval (x x_1) : (a : Polynomial R) → A) (f x_1) : A)
      ((aeval x : (a : MvPolynomial ι R) → A)
          ((Polynomial.aeval (X x_1) : (a : Polynomial R) → MvPolynomial ι R) (f x_1) : MvPolynomial ι R) :
        A)
⊢ AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : ι) ↦ (Polynomial.aeval (x i) : (a : Polynomial R) → A) (f i)

Tactic:
convert! aeval_of_algebraicIndependent hx (algebraicIndependent_polynomial_aeval_X _ hf)

Premises used: MvPolynomial.algebraicIndependent_polynomial_aeval_X, AlgebraicIndependent.aeval_of_algebraicIndependent
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hx : AlgebraicIndependent R x
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x_1 : ι
h :
  Eq.{v + 1} (α := A) ((Polynomial.aeval (x x_1) : (a : Polynomial R) → A) (f x_1) : A)
    ((AlgHom.comp (aeval x) (Polynomial.aeval (X x_1)) : (a : Polynomial R) → A) (f x_1) : A)
⊢ Eq.{v + 1} (α := A) ((Polynomial.aeval (x x_1) : (a : Polynomial R) → A) (f x_1) : A)
    ((aeval x : (a : MvPolynomial ι R) → A)
        ((Polynomial.aeval (X x_1) : (a : Polynomial R) → MvPolynomial ι R) (f x_1) : MvPolynomial ι R) :
      A)

Tactic:
rw [← AlgHom.comp_apply]

Premises used: AlgHom.comp_apply