awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FaithfulSMul R S
inst_4 : NoZeroDivisors S
i j : ι
v : ι → S
H₁ : IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : { x : ι // x ≠ i }) ↦ v (↑x : ι)
H₂ : IsAlgebraic (↥(adjoin R (v '' {j}ᶜ))) (v j)
ne : j ≠ i
this :
  ∀ (H₂ : IsAlgebraic (↥(adjoin R (v '' (insert i {i}ᶜ \ {j})))) (v j)),
    IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑(insert i {i}ᶜ \ {j}) : Type u)) ↦ v (↑x : ι)
⊢ ∀ (H₂ : IsAlgebraic (↥(adjoin R (v '' {j}ᶜ))) (v j)),
    IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑{j}ᶜ : Type u)) ↦ v (↑x : ι)

Tactic:
rw [compl_eq_univ_diff, insert_diff_self_of_mem (mem_univ _), ← compl_eq_univ_diff] at this

Premises used: Set.compl_eq_univ_diff, Set.mem_univ, Set.insert_diff_self_of_mem
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FaithfulSMul R S
inst_4 : NoZeroDivisors S
i j : ι
v : ι → S
H₁ : IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : { x : ι // x ≠ i }) ↦ v (↑x : ι)
H₂ : IsAlgebraic (↥(adjoin R (v '' {j}ᶜ))) (v j)
ne : j ≠ i
this :
  ∀ (H₂ : IsAlgebraic (↥(adjoin R (v '' {j}ᶜ))) (v j)),
    IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑{j}ᶜ : Type u)) ↦ v (↑x : ι)
⊢ IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : { x : ι // x ≠ j }) ↦ v (↑x : ι)

Tactic:
this H₂

Premises used: Set.Mem, setOf, Set.singleton, Not
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FaithfulSMul R S
inst_4 : NoZeroDivisors S
i j : ι
v : ι → S
H₁ : IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : { x : ι // x ≠ i }) ↦ v (↑x : ι)
H₂ : IsAlgebraic (↥(adjoin R (v '' {j}ᶜ))) (v j)
ne : j ≠ i
this :
  ∀ (H₂ : IsAlgebraic (↥(adjoin R (v '' {j}ᶜ))) (v j)),
    IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑{j}ᶜ : Type u)) ↦ v (↑x : ι)
⊢ IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : { x : ι // x ≠ j }) ↦ v (↑x : ι)

Tactic:
exact this H₂
-- 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
inst_3 : Unique ι
rw :
  Injective (α := MvPolynomial ι R) (β := A) (⇑(aeval x) : (a : MvPolynomial ι R) → A) ↔
    Injective.{u_3 + 1, v + 1} (α := Polynomial R) (β := A) (⇑(Polynomial.aeval (x default)) : (a : Polynomial R) → A)
⊢ AlgebraicIndependent R x ↔ Transcendental R (x default)

Tactic:
rw [transcendental_iff_injective, algebraicIndependent_iff_injective_aeval]

Premises used: transcendental_iff_injective, algebraicIndependent_iff_injective_aeval
-- 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
inst_3 : Unique ι
i : MvPolynomial ι R ≃ₐ[R] Polynomial R := uniqueAlgEquiv R ι
hf :
  ∀ (y : ι),
    Eq.{v + 1} (α := A) ((aeval x : (a : MvPolynomial ι R) → A) (X y) : A)
      ((AlgHom.comp (Polynomial.aeval (x default)) (↑i : MvPolynomial ι R →ₐ[R] Polynomial R) :
            (a : MvPolynomial ι R) → A)
          (X y) :
        A)
⊢ Eq (α := MvPolynomial ι R →ₐ[R] A) (aeval x)
    (AlgHom.comp (Polynomial.aeval (x default)) (↑i : MvPolynomial ι R →ₐ[R] Polynomial R))

Tactic:
ext y
-- 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
inst_3 : Unique ι
i : MvPolynomial ι R ≃ₐ[R] Polynomial R := uniqueAlgEquiv R ι
y : ι
⊢ Eq.{v + 1} (α := A) ((aeval x : (a : MvPolynomial ι R) → A) (X y) : A)
    ((AlgHom.comp (Polynomial.aeval (x default)) (↑i : MvPolynomial ι R →ₐ[R] Polynomial R) :
          (a : MvPolynomial ι R) → A)
        (X y) :
      A)

Tactic:
simp [i, Subsingleton.elim y default]

Premises used: Inhabited.default, Subsingleton.elim
-- 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
inst_3 : Unique ι
i : MvPolynomial ι R ≃ₐ[R] Polynomial R := uniqueAlgEquiv R ι
⊢ Eq (α := MvPolynomial ι R →ₐ[R] A) (aeval x)
    (AlgHom.comp (Polynomial.aeval (x default)) (↑i : MvPolynomial ι R →ₐ[R] Polynomial R))

Tactic:
have key : aeval (R := R) x = (Polynomial.aeval (R := R) (x default)).comp i := by
    ext y
    simp [i, Subsingleton.elim y default]
-- 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
inst_3 : Unique ι
i : MvPolynomial ι R ≃ₐ[R] Polynomial R := uniqueAlgEquiv R ι
key :
  Eq (α := MvPolynomial ι R →ₐ[R] A) (aeval x)
    (AlgHom.comp (Polynomial.aeval (x default)) (↑i : MvPolynomial ι R →ₐ[R] Polynomial R))
⊢ Injective (α := MvPolynomial ι R) (β := A) (⇑(aeval x) : (a : MvPolynomial ι R) → A) ↔
    Injective.{u_3 + 1, v + 1} (α := Polynomial R) (β := A) (⇑(Polynomial.aeval (x default)) : (a : Polynomial R) → A)

Tactic:
simp [key]
-- 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
inst_3 : Subsingleton ι
i : ι
⊢ AlgebraicIndependent R x ↔ Transcendental R (x i)

Tactic:
letI := uniqueOfSubsingleton i
  algebraicIndependent_unique_type_iff

Premises used: algebraicIndependent_unique_type_iff
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
R : Type u_3
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
x : A
⊢ AlgebraicIndependent R ![x] ↔ Transcendental R x

Tactic:
simp
-- 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
i : ι
⊢ AlgebraicIndependent R (x ∘ ![i])

Tactic:
have := hx.comp ![i] (Function.injective_of_subsingleton _)
-- 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
i : ι
this : AlgebraicIndependent R (x ∘ ![i])
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : AlgebraicIndependent R (FinVec.map x ![i])), AlgebraicIndependent R ![x i]
⊢ AlgebraicIndependent R ![x i]

Tactic:
rwa [← FinVec.map_eq] at this

Premises used: FinVec.map_eq
-- 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
i : ι
this : AlgebraicIndependent R (x ∘ ![i])
⊢ AlgebraicIndependent R ![x i]

Tactic:
have : AlgebraicIndependent R ![x i] := by rwa [← FinVec.map_eq] at this
-- 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
i : ι
this_1 : AlgebraicIndependent R (x ∘ ![i])
this rwa rwa₁ rwa₂ rwa₃ : AlgebraicIndependent R ![x i]
⊢ Transcendental R (x i)

Tactic:
rwa [← algebraicIndependent_iff_transcendental]

Premises used: algebraicIndependent_iff_transcendental
-- 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 : Algebra.IsAlgebraic R A
inl : ∀ (h : IsEmpty ι), IsEmpty ι
inr : ∀ (i : ι), IsEmpty ι
⊢ IsEmpty ι

Tactic:
rcases isEmpty_or_nonempty ι with h | ⟨⟨i⟩⟩

Premises used: isEmpty_or_nonempty
-- 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 : Algebra.IsAlgebraic R A
h : IsEmpty ι
⊢ IsEmpty ι

Tactic:
h
-- 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 : Algebra.IsAlgebraic R A
h : IsEmpty ι
⊢ IsEmpty ι

Tactic:
exact h
-- 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 : Algebra.IsAlgebraic R A
i : ι
⊢ IsEmpty ι

Tactic:
False.elim (hx.transcendental i (Algebra.IsAlgebraic.isAlgebraic _))

Premises used: Algebra.IsAlgebraic.isAlgebraic, False.elim, AlgebraicIndependent.transcendental
-- 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 : Algebra.IsAlgebraic R A
i : ι
⊢ IsEmpty ι

Tactic:
exact False.elim (hx.transcendental i (Algebra.IsAlgebraic.isAlgebraic _))

Premises used: Algebra.IsAlgebraic.isAlgebraic, False.elim, AlgebraicIndependent.transcendental
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
R : Type u_3
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Algebra.IsAlgebraic R A
⊢ trdeg R A = 0

Tactic:
bot_unique <| ciSup_le' fun s ↦ have := s.2.isEmpty_of_isAlgebraic; (Cardinal.mk_eq_zero _).le

Premises used: Cardinal.mk_eq_zero, Set.Elem, Eq.le, ciSup_le', AlgebraicIndependent.isEmpty_of_isAlgebraic, bot_unique, Subtype.val, Subtype.property
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
R : Type u_3
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Algebra.Transcendental R A
x : A
hx : Transcendental R x
⊢ 1 ≤ Cardinal.mk (↑(↑(Subtype.mk (p := fun (s : Set A) ↦ AlgebraicIndepOn R _root_.id s) {x} ⋯) : Set A) : Type v)

Tactic:
simp
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
R : Type u_3
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
pos : ∀ (h : Algebra.IsAlgebraic R A), trdeg R A = 0 ↔ Algebra.IsAlgebraic R A
neg : ∀ (h : ¬Algebra.IsAlgebraic R A), trdeg R A = 0 ↔ Algebra.IsAlgebraic R A
⊢ trdeg R A = 0 ↔ Algebra.IsAlgebraic R A

Tactic:
by_cases h : Algebra.IsAlgebraic R A

Premises used: Algebra.IsAlgebraic
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
R : Type u_3
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
h : Algebra.IsAlgebraic R A
⊢ trdeg R A = 0 ↔ Algebra.IsAlgebraic R A

Tactic:
iff_of_true trdeg_eq_zero h

Premises used: trdeg_eq_zero, iff_of_true
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
R : Type u_3
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
h : Algebra.IsAlgebraic R A
⊢ trdeg R A = 0 ↔ Algebra.IsAlgebraic R A

Tactic:
exact iff_of_true trdeg_eq_zero h

Premises used: trdeg_eq_zero, iff_of_true
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
R : Type u_3
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
h : ¬Algebra.IsAlgebraic R A
neg : ¬trdeg R A = 0 ↔ ¬Algebra.IsAlgebraic R A
⊢ trdeg R A = 0 ↔ Algebra.IsAlgebraic R A

Tactic:
rw [← not_iff_not]

Premises used: not_iff_not
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
R : Type u_3
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
h : ¬Algebra.IsAlgebraic R A
neg : ∀ (h : Algebra.Transcendental R A), ¬trdeg R A = 0 ↔ Algebra.Transcendental R A
⊢ ¬trdeg R A = 0 ↔ ¬Algebra.IsAlgebraic R A

Tactic:
rw [← Algebra.transcendental_iff_not_isAlgebraic] at h ⊢

Premises used: Algebra.transcendental_iff_not_isAlgebraic
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
R : Type u_3
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
h : Algebra.Transcendental R A
⊢ ¬trdeg R A = 0 ↔ Algebra.Transcendental R A

Tactic:
iff_of_true (trdeg_pos R A).ne' h

Premises used: LT.lt.ne', trdeg_pos, iff_of_true
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
R : Type u_3
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
h : Algebra.Transcendental R A
⊢ ¬trdeg R A = 0 ↔ Algebra.Transcendental R A

Tactic:
exact iff_of_true (trdeg_pos R A).ne' h

Premises used: LT.lt.ne', trdeg_pos, iff_of_true
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
R : Type u_3
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
rw : trdeg R A ≠ 0 ↔ ¬Algebra.IsAlgebraic R A
rw₁ : ¬trdeg R A = 0 ↔ ¬Algebra.IsAlgebraic R A
rw₂ rw₃ : ¬Algebra.IsAlgebraic R A ↔ ¬Algebra.IsAlgebraic R A
⊢ trdeg R A ≠ 0 ↔ Algebra.Transcendental R A

Tactic:
rw [Algebra.transcendental_iff_not_isAlgebraic, Ne, trdeg_eq_zero_iff]

Premises used: Ne, Algebra.transcendental_iff_not_isAlgebraic, trdeg_eq_zero_iff
-- 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
a : A
rw :
  Injective (α := MvPolynomial.{u_1, u_3} (Option ι) R) (β := A)
      (Function.comp (β := Polynomial ↥(adjoin R (range x)))
        (⇑(↑(Polynomial.aeval a) : Polynomial ↥(adjoin R (range x)) →+* A) : (a : Polynomial ↥(adjoin R (range x))) → A)
        (⇑hx.mvPolynomialOptionEquivPolynomialAdjoin.toRingHom :
          (a : MvPolynomial (Option ι) R) → Polynomial ↥(adjoin R (range x)))) ↔
    Injective (α := Polynomial ↥(adjoin R (range x))) (β := A)
      (⇑(Polynomial.aeval a) : (a : Polynomial ↥(adjoin R (range x))) → A)
⊢ (AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (o : Option ι) ↦ o.elim a x) ↔
    Transcendental (↥(adjoin R (range x))) a

Tactic:
rw [algebraicIndependent_iff_injective_aeval, transcendental_iff_injective,
    ← AlgHom.coe_toRingHom, ← hx.aeval_comp_mvPolynomialOptionEquivPolynomialAdjoin,
    RingHom.coe_comp]

Premises used: AlgHom.coe_toRingHom, AlgebraicIndependent.aeval_comp_mvPolynomialOptionEquivPolynomialAdjoin, transcendental_iff_injective, algebraicIndependent_iff_injective_aeval, RingHom.coe_comp
-- 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
a : A
⊢ Injective (α := MvPolynomial.{u_1, u_3} (Option ι) R) (β := A)
      (Function.comp (β := Polynomial ↥(adjoin R (range x)))
        (⇑(↑(Polynomial.aeval a) : Polynomial ↥(adjoin R (range x)) →+* A) : (a : Polynomial ↥(adjoin R (range x))) → A)
        (⇑hx.mvPolynomialOptionEquivPolynomialAdjoin.toRingHom :
          (a : MvPolynomial (Option ι) R) → Polynomial ↥(adjoin R (range x)))) ↔
    Injective (α := Polynomial ↥(adjoin R (range x))) (β := A)
      (⇑(Polynomial.aeval a) : (a : Polynomial ↥(adjoin R (range x))) → A)

Tactic:
Injective.of_comp_iff' (Polynomial.aeval a)
    (mvPolynomialOptionEquivPolynomialAdjoin hx).bijective

Premises used: Subsemiring.mk', Subsemiring.closure, Set.Mem, Function.Injective.of_comp_iff', Polynomial.aeval, RingEquiv.bijective, DFunLike.coe, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin
-- 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
a : A
⊢ Injective (α := MvPolynomial.{u_1, u_3} (Option ι) R) (β := A)
      (Function.comp (β := Polynomial ↥(adjoin R (range x)))
        (⇑(↑(Polynomial.aeval a) : Polynomial ↥(adjoin R (range x)) →+* A) : (a : Polynomial ↥(adjoin R (range x))) → A)
        (⇑hx.mvPolynomialOptionEquivPolynomialAdjoin.toRingHom :
          (a : MvPolynomial (Option ι) R) → Polynomial ↥(adjoin R (range x)))) ↔
    Injective (α := Polynomial ↥(adjoin R (range x))) (β := A)
      (⇑(Polynomial.aeval a) : (a : Polynomial ↥(adjoin R (range x))) → A)

Tactic:
exact Injective.of_comp_iff' (Polynomial.aeval a)
    (mvPolynomialOptionEquivPolynomialAdjoin hx).bijective

Premises used: Function.Injective.of_comp_iff', Polynomial.aeval, RingEquiv.bijective, DFunLike.coe, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin
-- 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
a : A
⊢ (AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (o : Option ι) ↦ o.elim a x) ↔
    AlgebraicIndependent R x ∧ Transcendental (↥(adjoin R (range x))) a

Tactic:
⟨fun h ↦ have := h.comp _ (Option.some_injective _); ⟨this,
    (this.option_iff_transcendental _).mp h⟩, fun h ↦ (h.1.option_iff_transcendental _).mpr h.2⟩

Premises used: Iff.mpr, AlgebraicIndependent.comp, Option.some, AlgebraicIndependent.option_iff_transcendental, And.right, And.left, And.intro, Iff.intro, Iff.mp, Option.some_injective
-- 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
s : Set ι
i : ι
h : i ∉ s
simp_rw :
  AlgebraicIndependent.{u_1, u_3, v} (ι := Option { i : ι // i ∈ s }) R (A := A)
      ((fun (i_1 : (↑(insert i s) : Type u_1)) ↦ x (↑i_1 : ι)) ∘
        (⇑(subtypeInsertEquivOption (t := s) h).symm :
          (a : Option { i : ι // i ∈ s }) → { i_1 : ι // i_1 ∈ insert i s })) ↔
    (AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑s : Type u_1)) ↦ x (↑i : ι)) ∧
      Transcendental (↥(adjoin R (x '' s))) (x i)
⊢ AlgebraicIndepOn R x (insert i s) ↔ AlgebraicIndepOn R x s ∧ Transcendental (↥(adjoin R (x '' s))) (x i)

Tactic:
simp_rw [← algebraicIndependent_equiv (subtypeInsertEquivOption h).symm,
    AlgebraicIndepOn]

Premises used: AlgebraicIndepOn, algebraicIndependent_equiv, Equiv.symm, Set.subtypeInsertEquivOption
-- 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
s : Set ι
i : ι
h : i ∉ s
classical :
  AlgebraicIndependent.{u_1, u_3, v} (ι := Option { i : ι // i ∈ s }) R (A := A)
      ((fun (i_1 : (↑(insert i s) : Type u_1)) ↦ x (↑i_1 : ι)) ∘
        (⇑(subtypeInsertEquivOption (t := s) h).symm :
          (a : Option { i : ι // i ∈ s }) → { i_1 : ι // i_1 ∈ insert i s })) ↔
    (AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑s : Type u_1)) ↦ x (↑i : ι)) ∧
      Transcendental (↥(adjoin R (x '' s))) (x i)
⊢ AlgebraicIndepOn R x (insert i s) ↔ AlgebraicIndepOn R x s ∧ Transcendental (↥(adjoin R (x '' s))) (x i)

Tactic:
classical simp_rw [← algebraicIndependent_equiv (subtypeInsertEquivOption h).symm,
    AlgebraicIndepOn]

Premises used: AlgebraicIndepOn
-- 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
s : Set ι
i : ι
h : i ∉ s
⊢ (AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (o : Option (↑s : Type u_1)) ↦
      o.elim (x i) fun (i : (↑s : Type u_1)) ↦ x (↑i : ι)) ↔
    (AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑s : Type u_1)) ↦ x (↑i : ι)) ∧
      Transcendental (↥(adjoin R (range fun (i : (↑s : Type u_1)) ↦ x (↑i : ι)))) (x i)

Tactic:
option_iff (x := fun i : s ↦ x i) (a := x i)

Premises used: AlgebraicIndependent.option_iff
-- 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
s : Set ι
i : ι
h : i ∉ s
h₁ :
  Eq (α := Option { i : ι // i ∈ s } → A)
    ((fun (i_1 : (↑(insert i s) : Type u_1)) ↦ x (↑i_1 : ι)) ∘
      (⇑(subtypeInsertEquivOption (t := s) h).symm : (a : Option { i : ι // i ∈ s }) → { i_1 : ι // i_1 ∈ insert i s }))
    fun (o : Option (↑s : Type u_1)) ↦ o.elim (x i) fun (i : (↑s : Type u_1)) ↦ x (↑i : ι)
h₂ :
  Transcendental (↥(adjoin R (x '' s))) (x i) ↔
    Transcendental (↥(adjoin R (range fun (i : (↑s : Type u_1)) ↦ x (↑i : ι)))) (x i)
⊢ AlgebraicIndependent.{u_1, u_3, v} (ι := Option { i : ι // i ∈ s }) R (A := A)
      ((fun (i_1 : (↑(insert i s) : Type u_1)) ↦ x (↑i_1 : ι)) ∘
        (⇑(subtypeInsertEquivOption (t := s) h).symm :
          (a : Option { i : ι // i ∈ s }) → { i_1 : ι // i_1 ∈ insert i s })) ↔
    (AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑s : Type u_1)) ↦ x (↑i : ι)) ∧
      Transcendental (↥(adjoin R (x '' s))) (x i)

Tactic:
convert! option_iff (x := fun i : s ↦ x i) (a := x i) using 2

Premises used: AlgebraicIndependent.option_iff
-- 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
s : Set ι
i : ι
h : i ∉ s
h₁ :
  Function.comp (α := Option { i : ι // i ∈ s }) (fun (i_1 : (↑(insert i s) : Type u_1)) ↦ x (↑i_1 : ι))
      (⇑(subtypeInsertEquivOption (t := s) h).symm : (a : Option { i : ι // i ∈ s }) → { i_1 : ι // i_1 ∈ insert i s })
      none =
    Option.elim none (x i) fun (i : (↑s : Type u_1)) ↦ x (↑i : ι)
h₂ :
  ∀ (val : { i : ι // i ∈ s }),
    ((fun (i_1 : (↑(insert i s) : Type u_1)) ↦ x (↑i_1 : ι)) ∘
          (⇑(subtypeInsertEquivOption (t := s) h).symm :
            (a : Option { i : ι // i ∈ s }) → { i_1 : ι // i_1 ∈ insert i s }))
        (some val) =
      (some val).elim (x i) fun (i : (↑s : Type u_1)) ↦ x (↑i : ι)
⊢ Eq (α := Option { i : ι // i ∈ s } → A)
    ((fun (i_1 : (↑(insert i s) : Type u_1)) ↦ x (↑i_1 : ι)) ∘
      (⇑(subtypeInsertEquivOption (t := s) h).symm : (a : Option { i : ι // i ∈ s }) → { i_1 : ι // i_1 ∈ insert i s }))
    fun (o : Option (↑s : Type u_1)) ↦ o.elim (x i) fun (i : (↑s : Type u_1)) ↦ x (↑i : ι)

Tactic:
ext (_ | _)
-- 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
s : Set ι
i : ι
h : i ∉ s
⊢ Function.comp (α := Option { i : ι // i ∈ s }) (fun (i_1 : (↑(insert i s) : Type u_1)) ↦ x (↑i_1 : ι))
      (⇑(subtypeInsertEquivOption (t := s) h).symm : (a : Option { i : ι // i ∈ s }) → { i_1 : ι // i_1 ∈ insert i s })
      none =
    Option.elim none (x i) fun (i : (↑s : Type u_1)) ↦ x (↑i : ι)

Tactic:
rfl
-- 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
s : Set ι
i : ι
h : i ∉ s
val : { i : ι // i ∈ s }
⊢ ((fun (i_1 : (↑(insert i s) : Type u_1)) ↦ x (↑i_1 : ι)) ∘
        (⇑(subtypeInsertEquivOption (t := s) h).symm :
          (a : Option { i : ι // i ∈ s }) → { i_1 : ι // i_1 ∈ insert i s }))
      (some val) =
    (some val).elim (x i) fun (i : (↑s : Type u_1)) ↦ x (↑i : ι)

Tactic:
rfl
-- 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
s : Set ι
i : ι
h : i ∉ s
h₁ h₂ :
  Transcendental (↥(adjoin R (range fun (x_1 : (↑s : Type u_1)) ↦ x (↑x_1 : ι)))) (x i) ↔
    Transcendental (↥(adjoin R (range fun (i : (↑s : Type u_1)) ↦ x (↑i : ι)))) (x i)
⊢ Transcendental (↥(adjoin R (x '' s))) (x i) ↔
    Transcendental (↥(adjoin R (range fun (i : (↑s : Type u_1)) ↦ x (↑i : ι)))) (x i)

Tactic:
rw [Set.image_eq_range]

Premises used: Set.image_eq_range
-- 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
s : Set ι
i : ι
hs : AlgebraicIndepOn R x s
hi : Transcendental (↥(adjoin R (x '' s))) (x i)
⊢ Nontrivial R

Tactic:
nontriviality R
-- 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
s : Set ι
i : ι
hs : AlgebraicIndepOn R x s
hi : Transcendental (↥(adjoin R (x '' s))) (x i)
h : Nontrivial R
⊢ Nontrivial A

Tactic:
have := hs.algebraMap_injective.nontrivial