awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (goal)
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 : ι)
⊢ AlgebraicIndependent R x
have 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)) sorry) :
        (a_1 : (↑(t ∩ s ∪ insert a u) : Type u_1)) → (↑(insert a (t ∩ s ∪ u)) : Type u_1))
      x_1
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]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (goal)
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
⊢ AlgebraicIndependent R (Sum.elim y x) ↔ AlgebraicIndependent R x ∧ AlgebraicIndependent (↥(adjoin R (range x))) y
have pos : ∀ (hx : AlgebraicIndependent R x),
  AlgebraicIndependent R (Sum.elim y x) ↔ AlgebraicIndependent R x ∧ AlgebraicIndependent (↥(adjoin R (range x))) y
Tactic: by_cases hx : AlgebraicIndependent R x
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (goal)
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
⊢ AlgebraicIndependent R (Sum.elim y x) ↔ AlgebraicIndependent R x ∧ AlgebraicIndependent (↥(adjoin R (range x))) y
have neg : ∀ (hx : ¬AlgebraicIndependent R x),
  AlgebraicIndependent R (Sum.elim y x) ↔ AlgebraicIndependent R x ∧ AlgebraicIndependent (↥(adjoin R (range x))) y
Tactic: by_cases hx : AlgebraicIndependent R x
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (goal)
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))))
have 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)
Tactic: ext (_ | _)
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (goal)
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)
⊢ 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))))
have 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)
Tactic: ext (_ | _)
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (hypothesis)
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)
⊢ AlgebraicIndependent R (Sum.elim y x) ↔ AlgebraicIndependent R x ∧ AlgebraicIndependent (↥(adjoin R (range x))) y
have 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))))
Tactic: have : aeval (Sum.elim y x) = ((aeval y).restrictScalars R).comp e.toAlgHom := by
    ext (_ | _) <;> simp [e]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (goal)
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))))
⊢ AlgebraicIndependent R (Sum.elim y x) ↔ AlgebraicIndependent R x ∧ AlgebraicIndependent (↥(adjoin R (range x))) y
have 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)
Tactic: simp_rw [hx, AlgebraicIndependent, this]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (goal)
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 '' s = range fun (i : (↑s : Type u_1)) ↦ x (↑i : ι)
have h : ∀ (x_1 : A), x_1 ∈ x '' s ↔ Membership.mem (γ := Set A) (range fun (i : (↑s : Type u_1)) ↦ x (↑i : ι)) x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (goal)
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ᶜ
have 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ᶜ
Tactic: rw [show x '' s = range fun i : s ↦ x i by ext; simp]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (goal)
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 (range fun (i : (↑s : Type u_1)) ↦ x (↑i : ι)))) x sᶜ
have 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
Tactic: convert! ← sumElim_iff
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (goal)
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 R x
have 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 : ι))
Tactic: apply algebraicIndependent_equiv' ((Equiv.sumComm ..).trans (Equiv.Set.sumCompl ..))
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (goal)
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 R x
have 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 : ι))
Tactic: classical apply algebraicIndependent_equiv' ((Equiv.sumComm ..).trans (Equiv.Set.sumCompl ..))
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (goal)
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 ι
⊢ 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 : ι))
have 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)
Tactic: ext (_ | _)
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (goal)
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)
⊢ 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 : ι))
have 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)
Tactic: ext (_ | _)
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (goal)
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
have h : sᶜᶜ = s
Tactic: convert! ← iff_adjoin_image _
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (hypothesis)
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 ⋯)))
⊢ AlgebraicIndependent R (Sum.elim y x)
have this : IsScalarTower (↥Rx) S A
Tactic: have : IsScalarTower Rx S A := .of_algebraMap_eq fun x ↦ show _ = (e (e.symm _)).1 by simp
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (goal)
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)
have refine : Injective (α := ↥(adjoin R (range x))) (β := ↥(AlgHom.range (IsScalarTower.toAlgHom R S A)))
  (⇑(↑(Subalgebra.inclusion sorry) : ↥(adjoin R (range x)) →+* ↥(IsScalarTower.toAlgHom R S A).range) :
    (a : ↥(adjoin R (range x))) → ↥(IsScalarTower.toAlgHom R S A).range)
Tactic: refine hx.sumElim (hy.restrictScalars (e.symm.injective.comp ?_))
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (goal)
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
have 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
Tactic: refine ⟨fun ind ↦ of_not_not fun ndisj ↦ ?_, adjoin_of_disjoint hx⟩
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (goal)
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
⊢ False
have have : ∀ (i : ι) (hs : i ∈ s) (ht : i ∈ t), False
Tactic: have ⟨i, hs, ht⟩ := Set.not_disjoint_iff.mp ndisj
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (goal)
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
have refine : x (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i ht) : ι) ∈ x '' s
Tactic: refine ind.transcendental ⟨i, ht⟩ (isAlgebraic_algebraMap (⟨_, subset_adjoin ?_⟩ : adjoin R _))
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (goal)
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 : ι)) ↔
    Transcendental (↥(adjoin R (x '' s))) (x i)
have a : Transcendental (↥(adjoin R (x '' s)))
    (x (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i} x) i sorry) : ι)) ↔
  Transcendental (↥(adjoin R (x '' s))) (x i)
Tactic: rw [algebraicIndependent_singleton_iff ⟨i, rfl⟩]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (goal)
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 : ι
⊢ Transcendental (↥(adjoin R (x '' s))) (x i) ↔ i ∉ s
have rw : Transcendental (↥(adjoin R (x '' s))) (x i) ↔ Disjoint s {i}
Tactic: rw [← Set.disjoint_singleton_right]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (goal)
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 : ι
⊢ Transcendental (↥(adjoin R (x '' s))) (x i) ↔ Disjoint s {i}
have 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)
Tactic: convert! ← hx.adjoin_iff_disjoint (t := { i })
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (goal)
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 : ι)) ↔
    Transcendental (↥(adjoin R (x '' s))) (x i)
have h : Transcendental (↥(adjoin R (x '' s)))
    (x (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) {i} x) i sorry) : ι)) ↔
  Transcendental (↥(adjoin R (x '' s))) (x i)
Tactic: rw [algebraicIndependent_singleton_iff ⟨i, rfl⟩]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (goal)
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
⊢ lift.{v, u} (trdeg R S) + lift.{u, v} (trdeg S A) ≤ lift.{u, v} (trdeg R A)
have 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)
Tactic: simp_rw [trdeg, lift_iSup bddAbove_of_small]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (goal)
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
⊢ 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)
have 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))
Tactic: simp_rw [Cardinal.ciSup_add_ciSup _ bddAbove_of_small _ bddAbove_of_small,
    add_comm (lift.{v, u} _), ← mk_sum]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (goal)
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))
have 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)
Tactic: refine ciSup_le fun ⟨s, hs⟩ ↦ ciSup_le fun ⟨t, ht⟩ ↦ ?_