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
ι' : Type u_4
y : ι' → A
hx : AlgebraicIndependent R x
e : MvPolynomial (ι' ⊕ ι) R ≃ₐ[R] MvPolynomial.{u_4, v} ι' ↥(adjoin R (range x)) :=
  AlgEquiv.trans (sumAlgEquiv R ι' ι) (mapAlgEquiv ι' hx.aevalEquiv)
this :
  Eq (α := MvPolynomial (ι' ⊕ ι) R →ₐ[R] A) (aeval (Sum.elim y x))
    (AlgHom.comp (AlgHom.restrictScalars R (aeval y))
      (↑e : MvPolynomial (ι' ⊕ ι) R →ₐ[R] MvPolynomial ι' ↥(adjoin R (range x))))
pos :
  Injective (α := MvPolynomial (ι' ⊕ ι) R) (β := A)
      (⇑(AlgHom.comp (AlgHom.restrictScalars R (aeval y))
            (↑e : MvPolynomial (ι' ⊕ ι) R →ₐ[R] MvPolynomial ι' ↥(adjoin R (range x)))) :
        (a : MvPolynomial (ι' ⊕ ι) R) → A) ↔
    True ∧
      Injective (α := MvPolynomial.{u_4, v} ι' ↥(adjoin R (range x))) (β := A)
        (⇑(aeval y) : (a : MvPolynomial ι' ↥(adjoin R (range x))) → A)
⊢ AlgebraicIndependent R (Sum.elim y x) ↔ AlgebraicIndependent R x ∧ AlgebraicIndependent (↥(adjoin R (range x))) y

Tactic:
simp_rw [hx, AlgebraicIndependent, this]

Premises used: 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
ι' : Type u_4
y : ι' → A
hx : AlgebraicIndependent R x
e : MvPolynomial (ι' ⊕ ι) R ≃ₐ[R] MvPolynomial.{u_4, v} ι' ↥(adjoin R (range x)) :=
  AlgEquiv.trans (sumAlgEquiv R ι' ι) (mapAlgEquiv ι' hx.aevalEquiv)
this :
  Eq (α := MvPolynomial (ι' ⊕ ι) R →ₐ[R] A) (aeval (Sum.elim y x))
    (AlgHom.comp (AlgHom.restrictScalars R (aeval y))
      (↑e : MvPolynomial (ι' ⊕ ι) R →ₐ[R] MvPolynomial ι' ↥(adjoin R (range x))))
⊢ Injective (α := MvPolynomial (ι' ⊕ ι) R) (β := A)
      (⇑(AlgHom.comp (AlgHom.restrictScalars R (aeval y))
            (↑e : MvPolynomial (ι' ⊕ ι) R →ₐ[R] MvPolynomial ι' ↥(adjoin R (range x)))) :
        (a : MvPolynomial (ι' ⊕ ι) R) → A) ↔
    True ∧
      Injective (α := MvPolynomial.{u_4, v} ι' ↥(adjoin R (range x))) (β := A)
        (⇑(aeval y) : (a : MvPolynomial ι' ↥(adjoin R (range x))) → A)

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
s : Set ι
h : ∀ (x_1 : A), x_1 ∈ x '' s ↔ Membership.mem (γ := Set A) (range fun (i : (↑s : Type u_1)) ↦ x (↑i : ι)) x_1
⊢ x '' s = range 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 ι
x_1 : A
⊢ x_1 ∈ x '' s ↔ Membership.mem (γ := Set A) (range fun (i : (↑s : Type u_1)) ↦ x (↑i : ι)) x_1

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
s : Set ι
rw :
  AlgebraicIndependent R x ↔
    (AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑s : Type u_1)) ↦ x (↑i : ι)) ∧
      AlgebraicIndepOn (↥(adjoin R (range fun (i : (↑s : Type u_1)) ↦ x (↑i : ι)))) x sᶜ
⊢ AlgebraicIndependent R x ↔
    (AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑s : Type u_1)) ↦ x (↑i : ι)) ∧
      AlgebraicIndepOn (↥(adjoin R (x '' s))) x sᶜ

Tactic:
rw [show x '' s = range fun i : s ↦ x i by ext; 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
s : Set ι
⊢ AlgebraicIndependent.{u_1, u_3, v} (ι := (↑sᶜ : Type u_1) ⊕ (↑s : Type u_1)) R (A := A)
      (Sum.elim (fun (i : (↑sᶜ : Type u_1)) ↦ 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 : ι)) ∧
      AlgebraicIndependent.{u_1, v, v} ↥(adjoin R (range fun (i : (↑s : Type u_1)) ↦ x (↑i : ι))) (A := A)
        fun (i : (↑sᶜ : Type u_1)) ↦ x (↑i : ι)

Tactic:
sumElim_iff

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

Tactic:
convert! ← sumElim_iff

Premises used: AlgebraicIndependent.sumElim_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 ι
h :
  Eq (α := (↑sᶜ : Type u_1) ⊕ (↑s : Type u_1) → A)
    (x ∘
      (⇑(Equiv.trans (Equiv.sumComm (↑sᶜ : Type u_1) (↑s : Type u_1)) (Equiv.Set.sumCompl s)) :
        (a : (↑sᶜ : Type u_1) ⊕ (↑s : Type u_1)) → ι))
    (Sum.elim (fun (i : (↑sᶜ : Type u_1)) ↦ x (↑i : ι)) fun (i : (↑s : Type u_1)) ↦ x (↑i : ι))
⊢ AlgebraicIndependent.{u_1, u_3, v} (ι := (↑sᶜ : Type u_1) ⊕ (↑s : Type u_1)) R (A := A)
      (Sum.elim (fun (i : (↑sᶜ : Type u_1)) ↦ x (↑i : ι)) fun (i : (↑s : Type u_1)) ↦ x (↑i : ι)) ↔
    AlgebraicIndependent R x

Tactic:
apply algebraicIndependent_equiv' ((Equiv.sumComm ..).trans (Equiv.Set.sumCompl ..))

Premises used: Equiv.trans, Equiv.sumComm, Equiv.Set.sumCompl, algebraicIndependent_equiv'
-- 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 ι
h :
  Eq (α := (↑sᶜ : Type u_1) ⊕ (↑s : Type u_1) → A)
    (x ∘
      (⇑(Equiv.trans (Equiv.sumComm (↑sᶜ : Type u_1) (↑s : Type u_1)) (Equiv.Set.sumCompl s)) :
        (a : (↑sᶜ : Type u_1) ⊕ (↑s : Type u_1)) → ι))
    (Sum.elim (fun (i : (↑sᶜ : Type u_1)) ↦ x (↑i : ι)) fun (i : (↑s : Type u_1)) ↦ x (↑i : ι))
⊢ AlgebraicIndependent.{u_1, u_3, v} (ι := (↑sᶜ : Type u_1) ⊕ (↑s : Type u_1)) R (A := A)
      (Sum.elim (fun (i : (↑sᶜ : Type u_1)) ↦ x (↑i : ι)) fun (i : (↑s : Type u_1)) ↦ x (↑i : ι)) ↔
    AlgebraicIndependent R x

Tactic:
classical apply algebraicIndependent_equiv' ((Equiv.sumComm ..).trans (Equiv.Set.sumCompl ..))

Premises used: Equiv.trans, Equiv.sumComm, Equiv.Set.sumCompl, algebraicIndependent_equiv'
-- 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 ι
h :
  ∀ (val : (↑sᶜ : Type u_1)),
    Function.comp (α := (↑sᶜ : Type u_1) ⊕ (↑s : Type u_1)) x
        (⇑(Equiv.trans (Equiv.sumComm (↑sᶜ : Type u_1) (↑s : Type u_1)) (Equiv.Set.sumCompl s)) :
          (a : (↑sᶜ : Type u_1) ⊕ (↑s : Type u_1)) → ι)
        (Sum.inl val) =
      Sum.elim (fun (i : (↑sᶜ : Type u_1)) ↦ x (↑i : ι)) (fun (i : (↑s : Type u_1)) ↦ x (↑i : ι)) (Sum.inl val)
h₁ :
  ∀ (val : (↑s : Type u_1)),
    Function.comp (α := (↑sᶜ : Type u_1) ⊕ (↑s : Type u_1)) x
        (⇑(Equiv.trans (Equiv.sumComm (↑sᶜ : Type u_1) (↑s : Type u_1)) (Equiv.Set.sumCompl s)) :
          (a : (↑sᶜ : Type u_1) ⊕ (↑s : Type u_1)) → ι)
        (Sum.inr val) =
      Sum.elim (fun (i : (↑sᶜ : Type u_1)) ↦ x (↑i : ι)) (fun (i : (↑s : Type u_1)) ↦ x (↑i : ι)) (Sum.inr val)
⊢ Eq (α := (↑sᶜ : Type u_1) ⊕ (↑s : Type u_1) → A)
    (x ∘
      (⇑(Equiv.trans (Equiv.sumComm (↑sᶜ : Type u_1) (↑s : Type u_1)) (Equiv.Set.sumCompl s)) :
        (a : (↑sᶜ : Type u_1) ⊕ (↑s : Type u_1)) → ι))
    (Sum.elim (fun (i : (↑sᶜ : Type u_1)) ↦ 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 ι
val : (↑sᶜ : Type u_1)
⊢ Function.comp (α := (↑sᶜ : Type u_1) ⊕ (↑s : Type u_1)) x
      (⇑(Equiv.trans (Equiv.sumComm (↑sᶜ : Type u_1) (↑s : Type u_1)) (Equiv.Set.sumCompl s)) :
        (a : (↑sᶜ : Type u_1) ⊕ (↑s : Type u_1)) → ι)
      (Sum.inl val) =
    Sum.elim (fun (i : (↑sᶜ : Type u_1)) ↦ x (↑i : ι)) (fun (i : (↑s : Type u_1)) ↦ x (↑i : ι)) (Sum.inl val)

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 ι
val : (↑s : Type u_1)
⊢ Function.comp (α := (↑sᶜ : Type u_1) ⊕ (↑s : Type u_1)) x
      (⇑(Equiv.trans (Equiv.sumComm (↑sᶜ : Type u_1) (↑s : Type u_1)) (Equiv.Set.sumCompl s)) :
        (a : (↑sᶜ : Type u_1) ⊕ (↑s : Type u_1)) → ι)
      (Sum.inr val) =
    Sum.elim (fun (i : (↑sᶜ : Type u_1)) ↦ x (↑i : ι)) (fun (i : (↑s : Type u_1)) ↦ x (↑i : ι)) (Sum.inr val)

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 ι
⊢ AlgebraicIndependent R x ↔
    (AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑sᶜ : Type u_1)) ↦ x (↑i : ι)) ∧
      AlgebraicIndepOn (↥(adjoin R (x '' sᶜ))) x sᶜᶜ

Tactic:
iff_adjoin_image _

Premises used: AlgebraicIndependent.iff_adjoin_image
-- 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 ι
h : sᶜᶜ = s
⊢ AlgebraicIndependent R x ↔
    (AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑sᶜ : Type u_1)) ↦ x (↑i : ι)) ∧
      AlgebraicIndepOn (↥(adjoin R (x '' sᶜ))) x s

Tactic:
convert! ← iff_adjoin_image _

Premises used: AlgebraicIndependent.iff_adjoin_image
-- 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 ι
⊢ sᶜᶜ = s

Tactic:
apply compl_compl

Premises used: compl_compl
-- 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
i : ι
⊢ AlgebraicIndependent R x ↔
    (AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (j : { j : ι // j ≠ i }) ↦ x (↑j : ι)) ∧
      Transcendental (↥(adjoin R (x '' {i}ᶜ))) (x i)

Tactic:
(iff_adjoin_image_compl _).trans <| and_congr_right
    fun _ ↦ algebraicIndependent_unique_type_iff (ι := {j // j = i})

Premises used: AlgebraicIndependent.iff_adjoin_image_compl, and_congr_right, Iff.trans, algebraicIndependent_unique_type_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
ι' : Type u_4
y : ι' → A
hy : AlgebraicIndependent (↥(adjoin R (range x))) y
⊢ AlgebraicIndependent R (Sum.elim y x)

Tactic:
sumElim_iff.mpr ⟨hx, hy⟩

Premises used: Iff.mpr, AlgebraicIndependent.sumElim_iff, And.intro
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
ι : Type u_1
R : Type u_3
S : Type u
A : Type v
x_1 : ι → A
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
hx : AlgebraicIndependent R x_1
ι' : Type u_4
y : ι' → A
hxS : range x_1 ⊆ range.{v, u + 1} (ι := S) (⇑(algebraMap S A) : (a : S) → A)
hy : AlgebraicIndependent S y
e : AlgEquiv.{u_3, u, v} R S ↥(AlgHom.range (IsScalarTower.toAlgHom R S A)) :=
  AlgEquiv.ofInjective (IsScalarTower.toAlgHom R S A) ⋯
Rx : Subalgebra R A := adjoin R (range x_1)
x_2 : Algebra.{v, u} (↥Rx) S :=
  RingHom.toAlgebra
    (AlgHom.toRingHom ((↑e.symm : ↥(IsScalarTower.toAlgHom R S A).range →ₐ[R] S).comp (Subalgebra.inclusion ⋯)))
x : ↥Rx
⊢ Eq (α := A) ((algebraMap (↥Rx) A : (a : ↥Rx) → A) x : A)
    ((↑((e : (a : S) → ↥(IsScalarTower.toAlgHom R S A).range)
            ((e.symm : (a : ↥(IsScalarTower.toAlgHom R S A).range) → S)
              (((↑(Subalgebra.inclusion ⋯) : ↥(adjoin R (range x_1)) →+* ↥(IsScalarTower.toAlgHom R S A).range) :
                    (a : ↥(adjoin R (range x_1))) → ↥(IsScalarTower.toAlgHom R S A).range)
                  x :
                ↥(AlgHom.range (IsScalarTower.toAlgHom R S A))))) :
        A) :
      A)

Tactic:
simp
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
ι : Type u_1
R : Type u_3
S : Type u
A : Type v
x : ι → A
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
hx : AlgebraicIndependent R x
ι' : Type u_4
y : ι' → A
hxS : range x ⊆ range.{v, u + 1} (ι := S) (⇑(algebraMap S A) : (a : S) → A)
hy : AlgebraicIndependent S y
e : AlgEquiv.{u_3, u, v} R S ↥(AlgHom.range (IsScalarTower.toAlgHom R S A)) :=
  AlgEquiv.ofInjective (IsScalarTower.toAlgHom R S A) ⋯
Rx : Subalgebra R A := adjoin R (range x)
x_1 : Algebra.{v, u} (↥Rx) S :=
  RingHom.toAlgebra
    (AlgHom.toRingHom ((↑e.symm : ↥(IsScalarTower.toAlgHom R S A).range →ₐ[R] S).comp (Subalgebra.inclusion ⋯)))
⊢ IsScalarTower (↥Rx) S A

Tactic:
have : IsScalarTower Rx S A := .of_algebraMap_eq fun x ↦ show _ = (e (e.symm _)).1 by simp
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
ι : Type u_1
R : Type u_3
S : Type u
A : Type v
x : ι → A
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
hx : AlgebraicIndependent R x
ι' : Type u_4
y : ι' → A
hxS : range x ⊆ range.{v, u + 1} (ι := S) (⇑(algebraMap S A) : (a : S) → A)
hy : AlgebraicIndependent S y
e : AlgEquiv.{u_3, u, v} R S ↥(AlgHom.range (IsScalarTower.toAlgHom R S A)) :=
  AlgEquiv.ofInjective (IsScalarTower.toAlgHom R S A) ⋯
Rx : Subalgebra R A := adjoin R (range x)
x_1 : Algebra.{v, u} (↥Rx) S :=
  RingHom.toAlgebra
    (AlgHom.toRingHom ((↑e.symm : ↥(IsScalarTower.toAlgHom R S A).range →ₐ[R] S).comp (Subalgebra.inclusion ⋯)))
this : IsScalarTower (↥Rx) S A
⊢ AlgebraicIndependent R (Sum.elim y x)

Tactic:
hx.sumElim (hy.restrictScalars (e.symm.injective.comp ?_))

Premises used: AlgEquiv.symm, AlgebraicIndependent.sumElim, Function.Injective.comp, AlgebraicIndependent.restrictScalars, AlgEquiv.injective
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
ι : Type u_1
R : Type u_3
S : Type u
A : Type v
x : ι → A
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
hx : AlgebraicIndependent R x
ι' : Type u_4
y : ι' → A
hxS : range x ⊆ range.{v, u + 1} (ι := S) (⇑(algebraMap S A) : (a : S) → A)
hy : AlgebraicIndependent S y
e : AlgEquiv.{u_3, u, v} R S ↥(AlgHom.range (IsScalarTower.toAlgHom R S A)) :=
  AlgEquiv.ofInjective (IsScalarTower.toAlgHom R S A) ⋯
Rx : Subalgebra R A := adjoin R (range x)
x_1 : Algebra.{v, u} (↥Rx) S :=
  RingHom.toAlgebra
    (AlgHom.toRingHom ((↑e.symm : ↥(IsScalarTower.toAlgHom R S A).range →ₐ[R] S).comp (Subalgebra.inclusion ⋯)))
this : IsScalarTower (↥Rx) S A
refine :
  Injective (α := ↥(adjoin R (range x))) (β := ↥(AlgHom.range (IsScalarTower.toAlgHom R S A)))
    (⇑(↑(Subalgebra.inclusion ⋯) : ↥(adjoin R (range x)) →+* ↥(IsScalarTower.toAlgHom R S A).range) :
      (a : ↥(adjoin R (range x))) → ↥(IsScalarTower.toAlgHom R S A).range)
⊢ AlgebraicIndependent R (Sum.elim y x)

Tactic:
refine hx.sumElim (hy.restrictScalars (e.symm.injective.comp ?_))

Premises used: AlgEquiv.symm, AlgebraicIndependent.sumElim, Function.Injective.comp, AlgebraicIndependent.restrictScalars, AlgEquiv.injective
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
ι : Type u_1
R : Type u_3
S : Type u
A : Type v
x : ι → A
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
hx : AlgebraicIndependent R x
ι' : Type u_4
y : ι' → A
hxS : range x ⊆ range.{v, u + 1} (ι := S) (⇑(algebraMap S A) : (a : S) → A)
hy : AlgebraicIndependent S y
e : AlgEquiv.{u_3, u, v} R S ↥(AlgHom.range (IsScalarTower.toAlgHom R S A)) :=
  AlgEquiv.ofInjective (IsScalarTower.toAlgHom R S A) ⋯
Rx : Subalgebra R A := adjoin R (range x)
x_1 : Algebra.{v, u} (↥Rx) S :=
  RingHom.toAlgebra
    (AlgHom.toRingHom ((↑e.symm : ↥(IsScalarTower.toAlgHom R S A).range →ₐ[R] S).comp (Subalgebra.inclusion ⋯)))
this : IsScalarTower (↥Rx) S A
⊢ Injective (α := ↥(adjoin R (range x))) (β := ↥(AlgHom.range (IsScalarTower.toAlgHom R S A)))
    (⇑(↑(Subalgebra.inclusion ⋯) : ↥(adjoin R (range x)) →+* ↥(IsScalarTower.toAlgHom R S A).range) :
      (a : ↥(adjoin R (range x))) → ↥(IsScalarTower.toAlgHom R S A).range)

Tactic:
simpa only [AlgHom.coe_toRingHom] using Subalgebra.inclusion_injective _

Premises used: AlgHom.coe_toRingHom, Subalgebra.inclusion_injective
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
ι : Type u_1
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
ι' : Type u_4
x : ι → S
y : ι' → A
hx : AlgebraicIndependent R x
hy : AlgebraicIndependent S y
⊢ AlgebraicIndependent R (Sum.elim y ((⇑(algebraMap S A) : (a : S) → A) ∘ x))

Tactic:
(hx.map' (f := IsScalarTower.toAlgHom R S A) hy.algebraMap_injective).sumElim_of_tower
    (range_comp_subset_range ..) hy

Premises used: Set.range_comp_subset_range, AlgebraicIndependent.map', AlgebraicIndependent.algebraMap_injective, AlgebraicIndependent.sumElim_of_tower
-- 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
s t : Set ι
h : Disjoint s t
⊢ AlgebraicIndependent.{u_1, v, v} ↥(adjoin R (x '' s)) (A := A) fun (i : (↑t : Type u_1)) ↦ x (↑i : ι)

Tactic:
((iff_adjoin_image s).mp hx).2.comp (inclusion _) (inclusion_injective h.subset_compl_left)

Premises used: AlgebraicIndependent.comp, And.right, Disjoint.subset_compl_left, Set.inclusion_injective, Iff.mp, Set.inclusion, AlgebraicIndependent.iff_adjoin_image
-- 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 t : Set ι
⊢ (AlgebraicIndependent.{u_1, v, v} ↥(adjoin R (x '' s)) (A := A) fun (i : (↑t : Type u_1)) ↦ x (↑i : ι)) ↔ Disjoint s t

Tactic:
⟨fun ind ↦ of_not_not fun ndisj ↦ ?_, adjoin_of_disjoint hx⟩

Premises used: AlgebraicIndependent.adjoin_of_disjoint, Iff.intro, of_not_not
-- 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 t : Set ι
refine :
  ∀ (ind : AlgebraicIndependent.{u_1, v, v} ↥(adjoin R (x '' s)) (A := A) fun (i : (↑t : Type u_1)) ↦ x (↑i : ι))
    (ndisj : ¬Disjoint s t), False
⊢ (AlgebraicIndependent.{u_1, v, v} ↥(adjoin R (x '' s)) (A := A) fun (i : (↑t : Type u_1)) ↦ x (↑i : ι)) ↔ Disjoint s t

Tactic:
refine ⟨fun ind ↦ of_not_not fun ndisj ↦ ?_, adjoin_of_disjoint hx⟩
-- 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 t : Set ι
ind : AlgebraicIndependent.{u_1, v, v} ↥(adjoin R (x '' s)) (A := A) fun (i : (↑t : Type u_1)) ↦ x (↑i : ι)
ndisj : ¬Disjoint s t
have : ∀ (i : ι) (hs : i ∈ s) (ht : i ∈ t), False
⊢ False

Tactic:
have ⟨i, hs, ht⟩ := Set.not_disjoint_iff.mp ndisj
-- 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 t : Set ι
ind : AlgebraicIndependent.{u_1, v, v} ↥(adjoin R (x '' s)) (A := A) fun (i : (↑t : Type u_1)) ↦ x (↑i : ι)
ndisj : ¬Disjoint s t
i : ι
hs : i ∈ s
ht : i ∈ t
⊢ False

Tactic:
ind.transcendental ⟨i, ht⟩ (isAlgebraic_algebraMap (⟨_, subset_adjoin ?_⟩ : adjoin R _))

Premises used: Algebra.subset_adjoin, Subtype.mk, AlgebraicIndependent.transcendental, isAlgebraic_algebraMap
-- 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 t : Set ι
ind : AlgebraicIndependent.{u_1, v, v} ↥(adjoin R (x '' s)) (A := A) fun (i : (↑t : Type u_1)) ↦ x (↑i : ι)
ndisj : ¬Disjoint s t
i : ι
hs : i ∈ s
ht : i ∈ t
refine : x (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i ht) : ι) ∈ x '' s
⊢ False

Tactic:
refine ind.transcendental ⟨i, ht⟩ (isAlgebraic_algebraMap (⟨_, subset_adjoin ?_⟩ : adjoin R _))

Premises used: Algebra.subset_adjoin, Subtype.mk, AlgebraicIndependent.transcendental, isAlgebraic_algebraMap
-- 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 t : Set ι
ind : AlgebraicIndependent.{u_1, v, v} ↥(adjoin R (x '' s)) (A := A) fun (i : (↑t : Type u_1)) ↦ x (↑i : ι)
ndisj : ¬Disjoint s t
i : ι
hs : i ∈ s
ht : i ∈ t
⊢ x (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i ht) : ι) ∈ x '' s

Tactic:
⟨i, hs, rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image, 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
hx : AlgebraicIndependent R x
inst_3 : Nontrivial A
s t : Set ι
ind : AlgebraicIndependent.{u_1, v, v} ↥(adjoin R (x '' s)) (A := A) fun (i : (↑t : Type u_1)) ↦ x (↑i : ι)
ndisj : ¬Disjoint s t
i : ι
hs : i ∈ s
ht : i ∈ t
⊢ x (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i ht) : ι) ∈ x '' s

Tactic:
exact ⟨i, hs, 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
hx : AlgebraicIndependent R x
s : Set ι
i : ι
hi : i ∉ s
⊢ AlgebraicIndependent.{u_1, v, v} ↥(adjoin R (x '' s)) (A := A) fun (i_1 : (↑{i} : Type u_1)) ↦ x (↑i_1 : ι)

Tactic:
hx.adjoin_of_disjoint (Set.disjoint_singleton_right.mpr hi)

Premises used: Iff.mpr, Set.disjoint_singleton_right, AlgebraicIndependent.adjoin_of_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
s : Set ι
i : ι
hi : i ∉ s
a a₁ :
  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:
ι : 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 : ι
rw : Transcendental (↥(adjoin R (x '' s))) (x i) ↔ Disjoint s {i}
⊢ Transcendental (↥(adjoin R (x '' s))) (x i) ↔ i ∉ s

Tactic:
rw [← Set.disjoint_singleton_right]

Premises used: Set.disjoint_singleton_right