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

Tactic:
(insert_iff fun h ↦ hi <| isAlgebraic_algebraMap
    (⟨_, subset_adjoin ⟨i, h, rfl⟩⟩ : adjoin R (x '' s))).mpr ⟨hs, hi⟩

Premises used: Iff.mpr, Algebra.subset_adjoin, Subtype.mk, AlgebraicIndepOn.insert_iff, And.intro, Exists.intro, isAlgebraic_algebraMap, 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 : ι
hs : AlgebraicIndepOn R x s
hi : Transcendental (↥(adjoin R (x '' s))) (x i)
h : Nontrivial R
this : Nontrivial A
⊢ AlgebraicIndepOn R x (insert i s)

Tactic:
exact (insert_iff fun h ↦ hi <| isAlgebraic_algebraMap
    (⟨_, subset_adjoin ⟨i, h, rfl⟩⟩ : adjoin R (x '' s))).mpr ⟨hs, hi⟩

Premises used: Iff.mpr, Algebra.subset_adjoin, Subtype.mk, AlgebraicIndepOn.insert_iff, And.intro, Exists.intro, isAlgebraic_algebraMap, 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 ι
ind : AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑s : Type u_1)) ↦ x (↑i : ι)
H :
  ∀ (t : Set ι),
    t.Finite →
      (AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑t : Type u_1)) ↦ x (↑i : ι)) →
        ∀ i ∉ s, i ∉ t → Transcendental (↥(adjoin R (x '' t))) (x i)
⊢ AlgebraicIndependent R x

Tactic:
algebraicIndependent_of_finite_type fun t hfin ↦ ?_

Premises used: algebraicIndependent_of_finite_type
-- 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 ι
ind : AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑s : Type u_1)) ↦ x (↑i : ι)
H :
  ∀ (t : Set ι),
    t.Finite →
      (AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑t : Type u_1)) ↦ x (↑i : ι)) →
        ∀ i ∉ s, i ∉ t → Transcendental (↥(adjoin R (x '' t))) (x i)
refine :
  ∀ (t : Set ι) (hfin : t.Finite), AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑t : Type u_1)) ↦ x (↑i : ι)
⊢ AlgebraicIndependent R x

Tactic:
refine algebraicIndependent_of_finite_type fun t hfin ↦ ?_

Premises used: algebraicIndependent_of_finite_type
-- 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 ι
ind : AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑s : Type u_1)) ↦ x (↑i : ι)
H :
  ∀ (t : Set ι),
    t.Finite →
      (AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑t : Type u_1)) ↦ x (↑i : ι)) →
        ∀ i ∉ s, i ∉ t → Transcendental (↥(adjoin R (x '' t))) (x i)
t : Set ι
hfin : t.Finite
suffices : AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑(t ∩ s ∪ t \ s) : Type u_1)) ↦ x (↑i : ι)
⊢ AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑t : Type u_1)) ↦ x (↑i : ι)

Tactic:
suffices AlgebraicIndependent R fun i : ↥(t ∩ s ∪ t \ s) ↦ x i from
    this.comp (Equiv.setCongr (t.inter_union_diff s).symm) (Equiv.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 ι
ind : AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑s : Type u_1)) ↦ x (↑i : ι)
H :
  ∀ (t : Set ι),
    t.Finite →
      (AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑t : Type u_1)) ↦ x (↑i : ι)) →
        ∀ i ∉ s, i ∉ t → Transcendental (↥(adjoin R (x '' t))) (x i)
t : Set ι
hfin : t.Finite
⊢ t ∩ s ∪ ∅ ⊆ s

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 ι
ind : AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑s : Type u_1)) ↦ x (↑i : ι)
H :
  ∀ (t : Set ι),
    t.Finite →
      (AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑t : Type u_1)) ↦ x (↑i : ι)) →
        ∀ i ∉ s, i ∉ t → Transcendental (↥(adjoin R (x '' t))) (x i)
t : Set ι
hfin : t.Finite
refine :
  ∀ {a : ι} {u : Set ι} (ha : a ∈ t \ s) (hu : u ⊆ t \ s) (ha' : a ∉ u)
    (h : AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑(t ∩ s ∪ u) : Type u_1)) ↦ x (↑i : ι)),
    AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑(t ∩ s ∪ insert a u) : Type u_1)) ↦ x (↑i : ι)
⊢ AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑(t ∩ s ∪ t \ s) : Type u_1)) ↦ x (↑i : ι)

Tactic:
refine hfin.diff.induction_on_subset _ (ind.comp (inclusion <| by simp) (inclusion_injective _))
    fun {a u} ha hu ha' 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
s : Set ι
ind : AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑s : Type u_1)) ↦ x (↑i : ι)
H :
  ∀ (t : Set ι),
    t.Finite →
      (AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑t : Type u_1)) ↦ x (↑i : ι)) →
        ∀ i ∉ s, i ∉ t → Transcendental (↥(adjoin R (x '' t))) (x i)
t : Set ι
hfin : t.Finite
a : ι
u : Set ι
ha : a ∈ t \ s
hu : u ⊆ t \ s
ha' : a ∉ u
h : AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑(t ∩ s ∪ u) : Type u_1)) ↦ x (↑i : ι)
⊢ a ∉ t ∩ s ∪ u

Tactic:
have : a ∉ t ∩ s ∪ u := (·.elim (ha.2 ·.2) ha')
-- 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 ι
ind : AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑s : Type u_1)) ↦ x (↑i : ι)
H :
  ∀ (t : Set ι),
    t.Finite →
      (AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑t : Type u_1)) ↦ x (↑i : ι)) →
        ∀ i ∉ s, i ∉ t → Transcendental (↥(adjoin R (x '' t))) (x i)
t : Set ι
hfin : t.Finite
a : ι
u : Set ι
ha : a ∈ t \ s
hu : u ⊆ t \ s
ha' : a ∉ u
h : AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑(t ∩ s ∪ u) : Type u_1)) ↦ x (↑i : ι)
this : a ∉ t ∩ s ∪ u
h₁ :
  ∀ (x_1 : (↑(t ∩ s ∪ insert a u) : Type u_1)),
    x (↑x_1 : ι) =
      Function.comp (β := { i : ι // i ∈ insert a (t ∩ s ∪ u) })
        ((fun (o : Option (↑(t ∩ s ∪ u) : Type u_1)) ↦ o.elim (x a) fun (i : (↑(t ∩ s ∪ u) : Type u_1)) ↦ x (↑i : ι)) ∘
          (⇑(subtypeInsertEquivOption (t := t ∩ s ∪ u) this) :
            (a : { i : ι // i ∈ insert a (t ∩ s ∪ u) }) → Option { i : ι // i ∈ t ∩ s ∪ u }))
        (⇑(Equiv.setCongr (s := t ∩ s ∪ insert a u) (t := insert a (t ∩ s ∪ u)) ⋯) :
          (a_1 : (↑(t ∩ s ∪ insert a u) : Type u_1)) → (↑(insert a (t ∩ s ∪ u)) : Type u_1))
        x_1
⊢ AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑(t ∩ s ∪ insert a u) : Type u_1)) ↦ x (↑i : ι)

Tactic:
convert!
    (((image_eq_range .. ▸ h.option_iff_transcendental <| x a).2 <|
              H _ (hfin.subset (union_subset inter_subset_left <| hu.trans diff_subset)) h a ha.2
                this).comp
          _ (subtypeInsertEquivOption this).injective).comp
      (Equiv.setCongr union_insert) (Equiv.injective _) with
    x
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
ι : Type u_1
R : Type u_3
A : Type v
x_1 : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
s : Set ι
ind : AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑s : Type u_1)) ↦ x_1 (↑i : ι)
H :
  ∀ (t : Set ι),
    t.Finite →
      (AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑t : Type u_1)) ↦ x_1 (↑i : ι)) →
        ∀ i ∉ s, i ∉ t → Transcendental (↥(adjoin R (x_1 '' t))) (x_1 i)
t : Set ι
hfin : t.Finite
a : ι
u : Set ι
ha : a ∈ t \ s
hu : u ⊆ t \ s
ha' : a ∉ u
h : AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑(t ∩ s ∪ u) : Type u_1)) ↦ x_1 (↑i : ι)
this : a ∉ t ∩ s ∪ u
x : (↑(t ∩ s ∪ insert a u) : Type u_1)
pos :
  ∀ (h : (↑x : ι) = a),
    x_1 (↑x : ι) =
      Function.comp (β := { i : ι // i ∈ insert a (t ∩ s ∪ u) })
        ((fun (o : Option (↑(t ∩ s ∪ u) : Type u_1)) ↦
            o.elim (x_1 a) fun (i : (↑(t ∩ s ∪ u) : Type u_1)) ↦ x_1 (↑i : ι)) ∘
          (⇑(subtypeInsertEquivOption (t := t ∩ s ∪ u) this) :
            (a : { i : ι // i ∈ insert a (t ∩ s ∪ u) }) → Option { i : ι // i ∈ t ∩ s ∪ u }))
        (⇑(Equiv.setCongr (s := t ∩ s ∪ insert a u) (t := insert a (t ∩ s ∪ u)) ⋯) :
          (a_1 : (↑(t ∩ s ∪ insert a u) : Type u_1)) → (↑(insert a (t ∩ s ∪ u)) : Type u_1))
        x
neg :
  ∀ (h : ¬(↑x : ι) = a),
    x_1 (↑x : ι) =
      Function.comp (β := { i : ι // i ∈ insert a (t ∩ s ∪ u) })
        ((fun (o : Option (↑(t ∩ s ∪ u) : Type u_1)) ↦
            o.elim (x_1 a) fun (i : (↑(t ∩ s ∪ u) : Type u_1)) ↦ x_1 (↑i : ι)) ∘
          (⇑(subtypeInsertEquivOption (t := t ∩ s ∪ u) this) :
            (a : { i : ι // i ∈ insert a (t ∩ s ∪ u) }) → Option { i : ι // i ∈ t ∩ s ∪ u }))
        (⇑(Equiv.setCongr (s := t ∩ s ∪ insert a u) (t := insert a (t ∩ s ∪ u)) ⋯) :
          (a_1 : (↑(t ∩ s ∪ insert a u) : Type u_1)) → (↑(insert a (t ∩ s ∪ u)) : Type u_1))
        x
⊢ x_1 (↑x : ι) =
    Function.comp (β := { i : ι // i ∈ insert a (t ∩ s ∪ u) })
      ((fun (o : Option (↑(t ∩ s ∪ u) : Type u_1)) ↦
          o.elim (x_1 a) fun (i : (↑(t ∩ s ∪ u) : Type u_1)) ↦ x_1 (↑i : ι)) ∘
        (⇑(subtypeInsertEquivOption (t := t ∩ s ∪ u) this) :
          (a : { i : ι // i ∈ insert a (t ∩ s ∪ u) }) → Option { i : ι // i ∈ t ∩ s ∪ u }))
      (⇑(Equiv.setCongr (s := t ∩ s ∪ insert a u) (t := insert a (t ∩ s ∪ u)) ⋯) :
        (a_1 : (↑(t ∩ s ∪ insert a u) : Type u_1)) → (↑(insert a (t ∩ s ∪ u)) : Type u_1))
      x

Tactic:
by_cases h : ↑x = a
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
ι : Type u_1
R : Type u_3
A : Type v
x_1 : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
s : Set ι
ind : AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑s : Type u_1)) ↦ x_1 (↑i : ι)
H :
  ∀ (t : Set ι),
    t.Finite →
      (AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑t : Type u_1)) ↦ x_1 (↑i : ι)) →
        ∀ i ∉ s, i ∉ t → Transcendental (↥(adjoin R (x_1 '' t))) (x_1 i)
t : Set ι
hfin : t.Finite
a : ι
u : Set ι
ha : a ∈ t \ s
hu : u ⊆ t \ s
ha' : a ∉ u
h_1 : AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑(t ∩ s ∪ u) : Type u_1)) ↦ x_1 (↑i : ι)
this : a ∉ t ∩ s ∪ u
x : (↑(t ∩ s ∪ insert a u) : Type u_1)
h : (↑x : ι) = a
⊢ x_1 (↑x : ι) =
    Function.comp (β := { i : ι // i ∈ insert a (t ∩ s ∪ u) })
      ((fun (o : Option (↑(t ∩ s ∪ u) : Type u_1)) ↦
          o.elim (x_1 a) fun (i : (↑(t ∩ s ∪ u) : Type u_1)) ↦ x_1 (↑i : ι)) ∘
        (⇑(subtypeInsertEquivOption (t := t ∩ s ∪ u) this) :
          (a : { i : ι // i ∈ insert a (t ∩ s ∪ u) }) → Option { i : ι // i ∈ t ∩ s ∪ u }))
      (⇑(Equiv.setCongr (s := t ∩ s ∪ insert a u) (t := insert a (t ∩ s ∪ u)) ⋯) :
        (a_1 : (↑(t ∩ s ∪ insert a u) : Type u_1)) → (↑(insert a (t ∩ s ∪ u)) : Type u_1))
      x

Tactic:
simp [h, Set.subtypeInsertEquivOption]

Premises used: Set.subtypeInsertEquivOption
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
ι : Type u_1
R : Type u_3
A : Type v
x_1 : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
s : Set ι
ind : AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑s : Type u_1)) ↦ x_1 (↑i : ι)
H :
  ∀ (t : Set ι),
    t.Finite →
      (AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑t : Type u_1)) ↦ x_1 (↑i : ι)) →
        ∀ i ∉ s, i ∉ t → Transcendental (↥(adjoin R (x_1 '' t))) (x_1 i)
t : Set ι
hfin : t.Finite
a : ι
u : Set ι
ha : a ∈ t \ s
hu : u ⊆ t \ s
ha' : a ∉ u
h_1 : AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑(t ∩ s ∪ u) : Type u_1)) ↦ x_1 (↑i : ι)
this : a ∉ t ∩ s ∪ u
x : (↑(t ∩ s ∪ insert a u) : Type u_1)
h : ¬(↑x : ι) = a
⊢ x_1 (↑x : ι) =
    Function.comp (β := { i : ι // i ∈ insert a (t ∩ s ∪ u) })
      ((fun (o : Option (↑(t ∩ s ∪ u) : Type u_1)) ↦
          o.elim (x_1 a) fun (i : (↑(t ∩ s ∪ u) : Type u_1)) ↦ x_1 (↑i : ι)) ∘
        (⇑(subtypeInsertEquivOption (t := t ∩ s ∪ u) this) :
          (a : { i : ι // i ∈ insert a (t ∩ s ∪ u) }) → Option { i : ι // i ∈ t ∩ s ∪ u }))
      (⇑(Equiv.setCongr (s := t ∩ s ∪ insert a u) (t := insert a (t ∩ s ∪ u)) ⋯) :
        (a_1 : (↑(t ∩ s ∪ insert a u) : Type u_1)) → (↑(insert a (t ∩ s ∪ u)) : Type u_1))
      x

Tactic:
simp [h, Set.subtypeInsertEquivOption]

Premises used: 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 ι
ind : AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑s : Type u_1)) ↦ x (↑i : ι)
H :
  ∀ (t : Set ι),
    t.Finite →
      (AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑t : Type u_1)) ↦ x (↑i : ι)) →
        ∀ i ∉ s, i ∉ t → Transcendental (↥(adjoin R (x '' t))) (x i)
refine :
  ∀ (t : Set ι) (hfin : t.Finite), AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑t : Type u_1)) ↦ x (↑i : ι)
refine₁ :
  ∀ (t : Set ι) (hfin : t.Finite),
    AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑(t ∩ s ∪ t \ s) : Type u_1)) ↦ x (↑i : ι)
refine₂ :
  ∀ (t : Set ι) (hfin : t.Finite) {a : ι} {u : Set ι} (ha : a ∈ t \ s) (hu : u ⊆ t \ s) (ha' : a ∉ u)
    (h : AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑(t ∩ s ∪ u) : Type u_1)) ↦ x (↑i : ι)),
    AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑(t ∩ s ∪ insert a u) : Type u_1)) ↦ x (↑i : ι)
refine₃ :
  ∀ (t : Set ι) (hfin : t.Finite) {a : ι} {u : Set ι} (ha : a ∈ t \ s) (hu : u ⊆ t \ s) (ha' : a ∉ u)
    (h : AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑(t ∩ s ∪ u) : Type u_1)) ↦ x (↑i : ι))
    (this : a ∉ t ∩ s ∪ u),
    AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑(t ∩ s ∪ insert a u) : Type u_1)) ↦ x (↑i : ι)
h :
  ∀ (t : Set ι) (hfin : t.Finite) {a : ι} {u : Set ι} (ha : a ∈ t \ s) (hu : u ⊆ t \ s) (ha' : a ∉ u)
    (h : AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑(t ∩ s ∪ u) : Type u_1)) ↦ x (↑i : ι))
    (this : a ∉ t ∩ s ∪ u) (x_1 : (↑(t ∩ s ∪ insert a u) : Type u_1)),
    x (↑x_1 : ι) =
      Function.comp (β := { i : ι // i ∈ insert a (t ∩ s ∪ u) })
        ((fun (o : Option (↑(t ∩ s ∪ u) : Type u_1)) ↦ o.elim (x a) fun (i : (↑(t ∩ s ∪ u) : Type u_1)) ↦ x (↑i : ι)) ∘
          (⇑(subtypeInsertEquivOption (t := t ∩ s ∪ u) this) :
            (a : { i : ι // i ∈ insert a (t ∩ s ∪ u) }) → Option { i : ι // i ∈ t ∩ s ∪ u }))
        (⇑(Equiv.setCongr (s := t ∩ s ∪ insert a u) (t := insert a (t ∩ s ∪ u)) ⋯) :
          (a_1 : (↑(t ∩ s ∪ insert a u) : Type u_1)) → (↑(insert a (t ∩ s ∪ u)) : Type u_1))
        x_1
⊢ AlgebraicIndependent R x

Tactic:
classical
  refine algebraicIndependent_of_finite_type fun t hfin ↦ ?_
  suffices AlgebraicIndependent R fun i : ↥(t ∩ s ∪ t \ s) ↦ x i from
    this.comp (Equiv.setCongr (t.inter_union_diff s).symm) (Equiv.injective _)
  refine hfin.diff.induction_on_subset _ (ind.comp (inclusion <| by simp) (inclusion_injective _))
    fun {a u} ha hu ha' h ↦ ?_
  have : a ∉ t ∩ s ∪ u := (·.elim (ha.2 ·.2) ha')
  convert!
    (((image_eq_range .. ▸ h.option_iff_transcendental <| x a).2 <|
              H _ (hfin.subset (union_subset inter_subset_left <| hu.trans diff_subset)) h a ha.2
                this).comp
          _ (subtypeInsertEquivOption this).injective).comp
      (Equiv.setCongr union_insert) (Equiv.injective _) with
    x
  by_cases h : ↑x = a <;> simp [h, Set.subtypeInsertEquivOption]

Premises used: algebraicIndependent_of_finite_type, 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
hinj : Injective.{u_3 + 1, v + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
H :
  ∀ (t : Set ι),
    t.Finite →
      (AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑t : Type u_1)) ↦ x (↑i : ι)) →
        ∀ i ∉ t, Transcendental (↥(adjoin R (x '' t))) (x i)
⊢ AlgebraicIndependent R x

Tactic:
algebraicIndependent_of_set_of_finite ∅ (algebraicIndependent_empty_type_iff.mpr hinj)
    fun t ht ind i _ ↦ H t ht ind i

Premises used: Iff.mpr, algebraicIndependent_of_set_of_finite, EmptyCollection.emptyCollection, algebraicIndependent_empty_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
s : Set A
hinj : Injective.{u_3 + 1, v + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
H :
  ∀ t ⊆ s,
    t.Finite →
      AlgebraicIndependent.{v, u_3, v} (ι := { x : A // x ∈ t }) R (Subtype.val (p := fun (x : A) ↦ x ∈ t)) →
        ∀ a ∈ s, a ∉ t → Transcendental (↥(adjoin R t)) a
t : Set { x : A // x ∈ s }
hfin : t.Finite
h : AlgebraicIndependent R (A := A) fun (i : (↑t : Type v)) ↦ (↑(↑i : { x : A // x ∈ s }) : A)
i : { x : A // x ∈ s }
hi : i ∉ t
x : { x : A // x ∈ s }
left : x ∈ t
⊢ (↑x : A) ∈ s

Tactic:
x.2

Premises used: 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
s : Set A
hinj : Injective.{u_3 + 1, v + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
H :
  ∀ t ⊆ s,
    t.Finite →
      AlgebraicIndependent.{v, u_3, v} (ι := { x : A // x ∈ t }) R (Subtype.val (p := fun (x : A) ↦ x ∈ t)) →
        ∀ a ∈ s, a ∉ t → Transcendental (↥(adjoin R t)) a
t : Set { x : A // x ∈ s }
hfin : t.Finite
h : AlgebraicIndependent R (A := A) fun (i : (↑t : Type v)) ↦ (↑(↑i : { x : A // x ∈ s }) : A)
i : { x : A // x ∈ s }
hi : i ∉ t
x : { x : A // x ∈ s }
left : x ∈ t
⊢ (↑x : A) ∈ s

Tactic:
exact x.2

Premises used: Subtype.property
-- 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
pos :
  ∀ (hx : AlgebraicIndependent R x),
    AlgebraicIndependent R (Sum.elim y x) ↔ AlgebraicIndependent R x ∧ AlgebraicIndependent (↥(adjoin R (range x))) y
neg :
  ∀ (hx : ¬AlgebraicIndependent R x),
    AlgebraicIndependent R (Sum.elim y x) ↔ AlgebraicIndependent R x ∧ AlgebraicIndependent (↥(adjoin R (range x))) y
⊢ AlgebraicIndependent R (Sum.elim y x) ↔ AlgebraicIndependent R x ∧ AlgebraicIndependent (↥(adjoin R (range x))) y

Tactic:
by_cases hx : AlgebraicIndependent R x

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
h : AlgebraicIndependent R (Sum.elim y x)
⊢ AlgebraicIndependent R x

Tactic:
apply h.comp _ Sum.inr_injective

Premises used: AlgebraicIndependent.comp, Sum.inr_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
ι' : Type u_4
y : ι' → A
hx : ¬AlgebraicIndependent R x
⊢ AlgebraicIndependent R (Sum.elim y x) ↔ AlgebraicIndependent R x ∧ AlgebraicIndependent (↥(adjoin R (range x))) y

Tactic:
exact ⟨fun h ↦ (hx <| by apply h.comp _ Sum.inr_injective).elim, fun h ↦ (hx h.1).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
ι' : 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)
hf :
  ∀ (val : ι'),
    Eq.{v + 1} (α := A) ((aeval (Sum.elim y x) : (a : MvPolynomial (ι' ⊕ ι) R) → A) (X (Sum.inl val)) : A)
      ((AlgHom.comp (AlgHom.restrictScalars R (aeval y))
              (↑e : MvPolynomial (ι' ⊕ ι) R →ₐ[R] MvPolynomial ι' ↥(adjoin R (range x))) :
            (a : MvPolynomial (ι' ⊕ ι) R) → A)
          (X (Sum.inl val)) :
        A)
hf₁ :
  ∀ (val : ι),
    Eq.{v + 1} (α := A) ((aeval (Sum.elim y x) : (a : MvPolynomial (ι' ⊕ ι) R) → A) (X (Sum.inr val)) : A)
      ((AlgHom.comp (AlgHom.restrictScalars R (aeval y))
              (↑e : MvPolynomial (ι' ⊕ ι) R →ₐ[R] MvPolynomial ι' ↥(adjoin R (range x))) :
            (a : MvPolynomial (ι' ⊕ ι) R) → A)
          (X (Sum.inr val)) :
        A)
⊢ 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))))

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
ι' : 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)
val : ι'
⊢ Eq.{v + 1} (α := A) ((aeval (Sum.elim y x) : (a : MvPolynomial (ι' ⊕ ι) R) → A) (X (Sum.inl val)) : A)
    ((AlgHom.comp (AlgHom.restrictScalars R (aeval y))
            (↑e : MvPolynomial (ι' ⊕ ι) R →ₐ[R] MvPolynomial ι' ↥(adjoin R (range x))) :
          (a : MvPolynomial (ι' ⊕ ι) R) → A)
        (X (Sum.inl val)) :
      A)

Tactic:
simp [e]
-- 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)
val : ι
⊢ Eq.{v + 1} (α := A) ((aeval (Sum.elim y x) : (a : MvPolynomial (ι' ⊕ ι) R) → A) (X (Sum.inr val)) : A)
    ((AlgHom.comp (AlgHom.restrictScalars R (aeval y))
            (↑e : MvPolynomial (ι' ⊕ ι) R →ₐ[R] MvPolynomial ι' ↥(adjoin R (range x))) :
          (a : MvPolynomial (ι' ⊕ ι) R) → A)
        (X (Sum.inr val)) :
      A)

Tactic:
simp [e]
-- 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)
⊢ 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))))

Tactic:
have : aeval (Sum.elim y x) = ((aeval y).restrictScalars R).comp e.toAlgHom := by
    ext (_ | _) <;> simp [e]