awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
Goal:
ι : Type u
R : Type u_2
A : Type v
A' : Type v'
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
x : ι → A
f : A →ₐ[R] A'
h : Injective.{v + 1, v' + 1} (α := A) (β := A') (⇑f : (a : A) → A')
H : IsTranscendenceBasis.{u, u_2, v'} R (A := A') ((⇑f : (a : A) → A') ∘ x)
s : Set A
hs : AlgebraicIndepOn R _root_.id s
hs' : range x ⊆ s
this : Eq.{v' + 1} (α := Set A') (range ((⇑f : (a : A) → A') ∘ x)) ((⇑f : (a : A) → A') '' s)
⊢ range x = s
have rwa : ∀ (this : Eq.{v' + 1} (α := Set A') ((⇑f : (a : A) → A') '' range x) ((⇑f : (a : A) → A') '' s)), range x = s
Tactic: rwa [Set.range_comp, (Set.image_injective.mpr h).eq_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
Goal:
ι : Type u
R : Type u_2
A : Type v
A' : Type v'
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
x : ι → A
f : A →ₐ[R] A'
h : Injective.{v + 1, v' + 1} (α := A) (β := A') (⇑f : (a : A) → A')
H : IsTranscendenceBasis.{u, u_2, v'} R (A := A') ((⇑f : (a : A) → A') ∘ x)
s : Set A
hs : AlgebraicIndepOn R _root_.id s
hs' : range x ⊆ s
this : Eq.{v' + 1} (α := Set A') (range ((⇑f : (a : A) → A') ∘ x)) ((⇑f : (a : A) → A') '' s)
rwa : ∀ (this : Eq.{v' + 1} (α := Set A') ((⇑f : (a : A) → A') '' range x) ((⇑f : (a : A) → A') '' s)), range x = s
⊢ range x = s
have rwa₁ : ∀ (this : range x = s), range x = s
Tactic: rwa [Set.range_comp, (Set.image_injective.mpr h).eq_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
Goal:
ι : Type u
R : Type u_2
A : Type v
A' : Type v'
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
e : A ≃ₐ[R] A'
hx : IsTranscendenceBasis R x
⊢ IsTranscendenceBasis.{u, u_2, v} R (A := A)
    (Function.comp.{u + 1, v' + 1, v + 1} (β := A') (⇑(↑e.symm : A' →ₐ[R] A) : (a : A') → A) ((⇑e : (a : A) → A') ∘ x))
have h : Function.comp.{u + 1, v' + 1, v + 1} (β := A') (⇑(↑e.symm : A' →ₐ[R] A) : (a : A') → A) ((⇑e : (a : A) → A') ∘ x) = x
Tactic: convert! hx
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
Goal:
ι : Type u
R : Type u_2
A : Type v
A' : Type v'
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
e : A ≃ₐ[R] A'
hx : IsTranscendenceBasis R x
⊢ Function.comp.{u + 1, v' + 1, v + 1} (β := A') (⇑(↑e.symm : A' →ₐ[R] A) : (a : A') → A) ((⇑e : (a : A) → A') ∘ x) = x
have h : ∀ (x_1 : ι),
  Function.comp.{u + 1, v' + 1, v + 1} (β := A') (⇑(↑e.symm : A' →ₐ[R] A) : (a : A') → A) ((⇑e : (a : A) → A') ∘ x)
      x_1 =
    x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
Goal:
ι : Type u
R : Type u_2
A : Type v
A' : Type v'
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
e : A ≃ₐ[R] A'
hx : IsTranscendenceBasis.{u, u_2, v'} R (A := A') ((⇑e : (a : A) → A') ∘ x)
⊢ IsTranscendenceBasis R x
have h : x = Function.comp.{u + 1, v' + 1, v + 1} (β := A') (⇑e.symm : (a : A') → A) ((⇑e : (a : A) → A') ∘ x)
Tactic: convert! e.symm.isTranscendenceBasis hx
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
Goal:
ι : Type u
R : Type u_2
A : Type v
A' : Type v'
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
e : A ≃ₐ[R] A'
hx : IsTranscendenceBasis.{u, u_2, v'} R (A := A') ((⇑e : (a : A) → A') ∘ x)
⊢ x = Function.comp.{u + 1, v' + 1, v + 1} (β := A') (⇑e.symm : (a : A') → A) ((⇑e : (a : A) → A') ∘ x)
have h : ∀ (x_1 : ι),
  x x_1 = Function.comp.{u + 1, v' + 1, v + 1} (β := A') (⇑e.symm : (a : A') → A) ((⇑e : (a : A) → A') ∘ x) x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
Goal:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
hx : AlgebraicIndependent R x
⊢ lift.{v, u} #ι ≤ lift.{u, v} (trdeg R A)
have rw : #(↑(range x) : Type v) ≤ trdeg R A
Tactic: rw [lift_mk_eq'.mpr ⟨.ofInjective _ hx.injective⟩, lift_le]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
Goal:
R : Type u_2
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
ι : Type v
x : ι → A
hx : AlgebraicIndependent R x
⊢ #ι ≤ trdeg R A
have rw : lift.{v, v} #ι ≤ lift.{v, v} (trdeg R A)
Tactic: rw [← (#ι).lift_id, ← (trdeg R A).lift_id]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (hypothesis)
Goal:
R : Type u_2
A : Type v
A' : Type v'
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
f : A →ₐ[R] A'
hf : Injective.{v + 1, v' + 1} (α := A) (β := A') (⇑f : (a : A) → A')
⊢ lift.{v', v} (trdeg R A) ≤ lift.{v, v'} (trdeg R A')
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
Goal:
R : Type u_2
A : Type v
A' : Type v'
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
f : A →ₐ[R] A'
hf : Injective.{v + 1, v' + 1} (α := A) (β := A') (⇑f : (a : A) → A')
h : Nontrivial R
⊢ lift.{v', v} (trdeg R A) ≤ lift.{v, v'} (trdeg R A')
have rw : ⨆ (i : { s : Set A // AlgebraicIndepOn R _root_.id s }), lift.{v', v} #(↑(↑i : Set A) : Type v) ≤
  lift.{v, v'} (trdeg R A')
Tactic: rw [trdeg, lift_iSup bddAbove_of_small]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
Goal:
R : Type u_2
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
A' : Type v
inst_3 : CommRing A'
inst_4 : Algebra R A'
f : A →ₐ[R] A'
hf : Injective (α := A) (β := A') (⇑f : (a : A) → A')
⊢ trdeg R A ≤ trdeg R A'
have rw : lift.{v, v} (trdeg R A) ≤ lift.{v, v} (trdeg R A')
Tactic: rw [← (trdeg R A).lift_id, ← (trdeg R A').lift_id]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (hypothesis)
Goal:
R : Type u_2
A : Type v
A' : Type v'
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
f : A →ₐ[R] A'
hf : Surjective.{v + 1, v' + 1} (α := A) (β := A') (⇑f : (a : A) → A')
⊢ lift.{v, v'} (trdeg R A') ≤ lift.{v', v} (trdeg R A)
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
Goal:
R : Type u_2
A : Type v
A' : Type v'
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
f : A →ₐ[R] A'
hf : Surjective.{v + 1, v' + 1} (α := A) (β := A') (⇑f : (a : A) → A')
h : Nontrivial R
⊢ lift.{v, v'} (trdeg R A') ≤ lift.{v', v} (trdeg R A)
have rw : ⨆ (i : { s : Set A' // AlgebraicIndepOn R _root_.id s }), lift.{v, v'} #(↑(↑i : Set A') : Type v') ≤
  lift.{v', v} (trdeg R A)
Tactic: rw [trdeg, lift_iSup bddAbove_of_small]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
Goal:
R : Type u_2
A : Type v
A' : Type v'
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
f : A →ₐ[R] A'
hf : Surjective.{v + 1, v' + 1} (α := A) (β := A') (⇑f : (a : A) → A')
h : Nontrivial R
⊢ ⨆ (i : { s : Set A' // AlgebraicIndepOn R _root_.id s }), lift.{v, v'} #(↑(↑i : Set A') : Type v') ≤
    lift.{v', v} (trdeg R A)
have refine : ∀ (i : { s : Set A' // AlgebraicIndepOn R _root_.id s }),
  AlgebraicIndependent.{v', u_2, v'} (ι := (↑(↑i : Set A') : Type v')) R (A := A')
    (Function.comp.{v' + 1, v + 1, v' + 1} (β := A) (⇑f : (a : A) → A') fun (a : (↑(↑i : Set A') : Type v')) ↦
      invFun (⇑f : (a : A) → A') (↑a : A'))
Tactic: refine ciSup_le' fun i ↦ (lift_cardinalMk_le_trdeg (x := fun a : i.1 ↦ (⇑f).invFun a) <|
    of_comp f ?_)
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
Goal:
R : Type u_2
A : Type v
A' : Type v'
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing A'
inst_3 : Algebra R A
inst_4 : Algebra R A'
f : A →ₐ[R] A'
hf : Surjective.{v + 1, v' + 1} (α := A) (β := A') (⇑f : (a : A) → A')
h : Nontrivial R
i : { s : Set A' // AlgebraicIndepOn R _root_.id s }
⊢ AlgebraicIndependent.{v', u_2, v'} (ι := (↑(↑i : Set A') : Type v')) R (A := A')
    (Function.comp.{v' + 1, v + 1, v' + 1} (β := A) (⇑f : (a : A) → A') fun (a : (↑(↑i : Set A') : Type v')) ↦
      invFun (⇑f : (a : A) → A') (↑a : A'))
have h : ∀ (x : (↑(↑i : Set A') : Type v')),
  Function.comp.{v' + 1, v + 1, v' + 1} (β := A) (⇑f : (a : A) → A')
      (fun (a : (↑(↑i : Set A') : Type v')) ↦ invFun (⇑f : (a : A) → A') (↑a : A')) x =
    _root_.id (↑x : A')
Tactic: convert! i.2
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
Goal:
R : Type u_2
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
A' : Type v
inst_3 : CommRing A'
inst_4 : Algebra R A'
f : A →ₐ[R] A'
hf : Surjective (α := A) (β := A') (⇑f : (a : A) → A')
⊢ trdeg R A' ≤ trdeg R A
have rw : lift.{v, v} (trdeg R A') ≤ lift.{v, v} (trdeg R A)
Tactic: rw [← (trdeg R A).lift_id, ← (trdeg R A').lift_id]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
Goal:
R : Type u_2
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
A' : Type v
inst_3 : CommRing A'
inst_4 : Algebra R A'
e : A ≃ₐ[R] A'
⊢ trdeg R A = trdeg R A'
have rw : lift.{v, v} (trdeg R A) = trdeg R A'
Tactic: rw [← (trdeg R A).lift_id, e.lift_trdeg_eq, lift_id]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
Goal:
R : Type u_2
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
A' : Type v
inst_3 : CommRing A'
inst_4 : Algebra R A'
e : A ≃ₐ[R] A'
rw : lift.{v, v} (trdeg R A) = trdeg R A'
⊢ trdeg R A = trdeg R A'
have rw₁ : lift.{v, v} (trdeg R A') = trdeg R A'
Tactic: rw [← (trdeg R A).lift_id, e.lift_trdeg_eq, lift_id]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
Goal:
R : Type u_2
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
A' : Type v
inst_3 : CommRing A'
inst_4 : Algebra R A'
e : A ≃ₐ[R] A'
rw : lift.{v, v} (trdeg R A) = trdeg R A'
rw₁ : lift.{v, v} (trdeg R A') = trdeg R A'
⊢ trdeg R A = trdeg R A'
have rw₂ : trdeg R A' = trdeg R A'
Tactic: rw [← (trdeg R A).lift_id, e.lift_trdeg_eq, lift_id]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
Goal:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
s : Set ι
⊢ Eq (α := MvPolynomial.{u, u_2} (↑s : Type u) R →ₐ[R] A) (aeval (x ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)))
    (AlgHom.comp (aeval x) (rename (Subtype.val (p := fun (x : ι) ↦ x ∈ s))))
have hf : ∀ (i : (↑s : Type u)),
  Eq.{v + 1} (α := A)
    ((aeval (x ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) : (a : MvPolynomial (↑s : Type u) R) → A) (X i) : A)
    ((AlgHom.comp (aeval x) (rename (Subtype.val (p := fun (x : ι) ↦ x ∈ s))) : (a : MvPolynomial (↑s : Type u) R) → A)
        (X i) :
      A)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (hypothesis)
Goal:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
s : Set ι
⊢ AlgebraicIndependent (ι := (↑s : Type u)) R (x ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) ↔
    ∀ (p : MvPolynomial ι R),
      Membership.mem (γ := Subalgebra R (MvPolynomial ι R)) (supported R s) p →
        Eq.{v + 1} (α := A) ((aeval x : (a : MvPolynomial ι R) → A) p : A) (0 : A) → p = 0
have this : Eq (α := MvPolynomial.{u, u_2} (↑s : Type u) R →ₐ[R] A) (aeval (x ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)))
  (AlgHom.comp (aeval x) (rename (Subtype.val (p := fun (x : ι) ↦ x ∈ s))))
Tactic: have : (aeval (x ∘ (↑) : s → A) : _ →ₐ[R] _) = (aeval x).comp (rename (↑)) := by ext; simp
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (hypothesis)
Goal:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
s : Set ι
this :
  Eq (α := MvPolynomial.{u, u_2} (↑s : Type u) R →ₐ[R] A) (aeval (x ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)))
    (AlgHom.comp (aeval x) (rename (Subtype.val (p := fun (x : ι) ↦ x ∈ s))))
⊢ AlgebraicIndependent (ι := (↑s : Type u)) R (x ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) ↔
    ∀ (p : MvPolynomial ι R),
      Membership.mem (γ := Subalgebra R (MvPolynomial ι R)) (supported R s) p →
        Eq.{v + 1} (α := A) ((aeval x : (a : MvPolynomial ι R) → A) p : A) (0 : A) → p = 0
have this₁ : ∀ (p : MvPolynomial.{u, u_2} (↑s : Type u) R),
  Eq (α := MvPolynomial ι R)
      ((rename (Subtype.val (p := fun (x : ι) ↦ x ∈ s)) : (a : MvPolynomial { x : ι // x ∈ s } R) → MvPolynomial ι R)
          p :
        MvPolynomial ι R)
      (0 : MvPolynomial ι R) ↔
    p = 0
Tactic: have : ∀ p : MvPolynomial s R, rename ((↑) : s → ι) p = 0 ↔ p = 0 :=
    (injective_iff_map_eq_zero' (rename ((↑) : s → ι) : MvPolynomial s R →ₐ[R] _).toRingHom).1
      (rename_injective _ Subtype.val_injective)
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (hypothesis)
Goal:
R : Type u_2
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
ι : Type u_3
ι' : Type u_4
s : Set ι
f : ι → ι'
g : ι' → A
hs : AlgebraicIndependent.{u_3, u_2, v} R (A := A) fun (x : (↑s : Type u_3)) ↦ g (f (↑x : ι))
⊢ AlgebraicIndependent.{u_4, u_2, v} R (A := A) fun (x : (↑(f '' s) : Type u_4)) ↦ g (↑x : ι')
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (hypothesis)
Goal:
R : Type u_2
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
ι : Type u_3
ι' : Type u_4
s : Set ι
f : ι → ι'
g : ι' → A
hs : AlgebraicIndependent.{u_3, u_2, v} R (A := A) fun (x : (↑s : Type u_3)) ↦ g (f (↑x : ι))
h : Nontrivial R
⊢ AlgebraicIndependent.{u_4, u_2, v} R (A := A) fun (x : (↑(f '' s) : Type u_4)) ↦ g (↑x : ι')
have this : InjOn f s
Tactic: have : InjOn f s := injOn_iff_injective.2 hs.injective.of_comp
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
Goal:
R : Type u_2
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
η : Type u_3
inst_3 : Nonempty η
s : η → Set A
hs : Directed (fun (x1 x2 : Set A) ↦ x1 ⊆ x2) s
h : ∀ (i : η), AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ s i }) R (Subtype.val (p := fun (x : A) ↦ x ∈ s i))
⊢ AlgebraicIndependent.{v, u_2, v} (ι := { x : A // Membership.mem (γ := Set A) (⋃ (i : η), s i) x }) R
    (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Set A) (⋃ (i : η), s i) x))
have refine : ∀ (t : Set A) (ht : t ⊆ ⋃ (i : η), s i) (ft : t.Finite),
  AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ t }) R (Subtype.val (p := fun (x : A) ↦ x ∈ t))
Tactic: refine algebraicIndependent_of_finite (⋃ i, s i) fun t ht ft => ?_
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
Goal:
R : Type u_2
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
η : Type u_3
inst_3 : Nonempty η
s : η → Set A
hs : Directed (fun (x1 x2 : Set A) ↦ x1 ⊆ x2) s
h : ∀ (i : η), AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ s i }) R (Subtype.val (p := fun (x : A) ↦ x ∈ s i))
t : Set A
ht : t ⊆ ⋃ (i : η), s i
ft : t.Finite
⊢ AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ t }) R (Subtype.val (p := fun (x : A) ↦ x ∈ t))
have rcases : ∀ (I : Set η) (fi : I.Finite) (hI : t ⊆ ⋃ i ∈ I, s i),
  AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ t }) R (Subtype.val (p := fun (x : A) ↦ x ∈ t))
Tactic: rcases finite_subset_iUnion ft ht with ⟨I, fi, hI⟩
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
Goal:
R : Type u_2
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
η : Type u_3
inst_3 : Nonempty η
s : η → Set A
hs : Directed (fun (x1 x2 : Set A) ↦ x1 ⊆ x2) s
h : ∀ (i : η), AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ s i }) R (Subtype.val (p := fun (x : A) ↦ x ∈ s i))
t : Set A
ht : t ⊆ ⋃ (i : η), s i
ft : t.Finite
I : Set η
fi : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
⊢ AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ t }) R (Subtype.val (p := fun (x : A) ↦ x ∈ t))
have rcases : ∀ (i : η) (hi : ∀ i_1 ∈ fi.toFinset (s := I), s i_1 ⊆ s i),
  AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ t }) R (Subtype.val (p := fun (x : A) ↦ x ∈ t))
Tactic: rcases hs.finset_le fi.toFinset with ⟨i, hi⟩
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
Goal:
R : Type u_2
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
s : Set (Set A)
hsn : s.Nonempty
hs : DirectedOn (fun (x1 x2 : Set A) ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ a }) R (Subtype.val (p := fun (x : A) ↦ x ∈ a))
this : Nonempty.{v + 1} (↑s : Type v) := ⋯
⊢ AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ ⋃₀ s }) R (Subtype.val (p := fun (x : A) ↦ x ∈ ⋃₀ s))
have rw : AlgebraicIndependent.{v, u_2, v} (ι := { x : A // Membership.mem (γ := Set A) (⋃ (i : (↑s : Type v)), (↑i : Set A)) x })
  R (Subtype.val (p := fun (x : A) ↦ Membership.mem (γ := Set A) (⋃ (i : (↑s : Type v)), (↑i : Set A)) x))
Tactic: rw [sUnion_eq_iUnion]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
Goal:
R : Type u_2
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
s t : Set A
hst : s ⊆ t
hs : AlgebraicIndepOn R _root_.id s
⊢ ∃ (u : Set A), s ⊆ u ∧ Maximal (fun (x : Set A) ↦ AlgebraicIndepOn R _root_.id x ∧ x ⊆ t) u
have refine_1 : ∀ (c : Set (Set A))
  (hc :
    c ⊆
      {u : Set A |
        AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ u }) R (Subtype.val (p := fun (x : A) ↦ x ∈ u)) ∧ u ⊆ t})
  (chainc : IsChain (fun (x1 x2 : Set A) ↦ x1 ⊆ x2) c) (hcn : c.Nonempty),
  AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ ⋃₀ c }) R (Subtype.val (p := fun (x : A) ↦ x ∈ ⋃₀ c))
Tactic: refine zorn_subset_nonempty { u : Set A | AlgebraicIndependent R ((↑) : u → A) ∧ u ⊆ t}
    (fun c hc chainc hcn ↦ ⟨⋃₀ c, ⟨?_, ?_⟩, fun _ ↦ subset_sUnion_of_mem⟩) s ⟨hs, hst⟩
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
Goal:
R : Type u_2
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
s t : Set A
hst : s ⊆ t
hs : AlgebraicIndepOn R _root_.id s
refine_1 :
  ∀ (c : Set (Set A))
    (hc :
      c ⊆
        {u : Set A |
          AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ u }) R (Subtype.val (p := fun (x : A) ↦ x ∈ u)) ∧
            u ⊆ t})
    (chainc : IsChain (fun (x1 x2 : Set A) ↦ x1 ⊆ x2) c) (hcn : c.Nonempty),
    AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ ⋃₀ c }) R (Subtype.val (p := fun (x : A) ↦ x ∈ ⋃₀ c))
⊢ ∃ (u : Set A), s ⊆ u ∧ Maximal (fun (x : Set A) ↦ AlgebraicIndepOn R _root_.id x ∧ x ⊆ t) u
have refine_2 : ∀ (c : Set (Set A))
  (hc :
    c ⊆
      {u : Set A |
        AlgebraicIndependent.{v, u_2, v} (ι := { x : A // x ∈ u }) R (Subtype.val (p := fun (x : A) ↦ x ∈ u)) ∧ u ⊆ t})
  (chainc : IsChain (fun (x1 x2 : Set A) ↦ x1 ⊆ x2) c) (hcn : c.Nonempty), ⋃₀ c ⊆ t
Tactic: refine zorn_subset_nonempty { u : Set A | AlgebraicIndependent R ((↑) : u → A) ∧ u ⊆ t}
    (fun c hc chainc hcn ↦ ⟨⋃₀ c, ⟨?_, ?_⟩, fun _ ↦ subset_sUnion_of_mem⟩) s ⟨hs, hst⟩
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
Goal:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hx : AlgebraicIndependent R x
r : R
⊢ Eq.{v + 1} (α := Polynomial ↥(adjoin R (range x)))
    ((Polynomial.C : (a : ↥(adjoin R (range x))) → Polynomial ↥(adjoin R (range x)))
        ((hx.aevalEquiv : (a : MvPolynomial ι R) → ↥(adjoin R (range x))) ((C : (a : R) → MvPolynomial ι R) r)) :
      Polynomial ↥(adjoin R (range x)))
    ((Polynomial.C : (a : ↥(adjoin R (range x))) → Polynomial ↥(adjoin R (range x)))
        ((algebraMap R ↥(adjoin R (range x)) : (a : R) → ↥(adjoin R (range x))) r) :
      Polynomial ↥(adjoin R (range x)))
have h : Eq.{v + 1} (α := ↥(adjoin R (range x)))
  ((hx.aevalEquiv : (a : MvPolynomial ι R) → ↥(adjoin R (range x))) ((C : (a : R) → MvPolynomial ι R) r) :
    ↥(adjoin R (range x)))
  ((algebraMap R ↥(adjoin R (range x)) : (a : R) → ↥(adjoin R (range x))) r : ↥(adjoin R (range x)))
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
Goal:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hx : AlgebraicIndependent R x
r : R
⊢ Eq.{v + 1} (α := ↥(adjoin R (range x)))
    ((hx.aevalEquiv : (a : MvPolynomial ι R) → ↥(adjoin R (range x))) ((C : (a : R) → MvPolynomial ι R) r) :
      ↥(adjoin R (range x)))
    ((algebraMap R ↥(adjoin R (range x)) : (a : R) → ↥(adjoin R (range x))) r : ↥(adjoin R (range x)))
have h : Eq.{v + 1} (α := A)
  (↑((hx.aevalEquiv : (a : MvPolynomial ι R) → ↥(adjoin R (range x))) ((C : (a : R) → MvPolynomial ι R) r)) : A)
  (↑((algebraMap R ↥(adjoin R (range x)) : (a : R) → ↥(adjoin R (range x))) r) : A)
Tactic: apply_fun Subtype.val using Subtype.val_injective
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
Goal:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hx : AlgebraicIndependent R x
⊢ Eq.{v + 1} (α := Polynomial ↥(adjoin R (range x)))
    ((hx.mvPolynomialOptionEquivPolynomialAdjoin : (a : MvPolynomial (Option ι) R) → Polynomial ↥(adjoin R (range x)))
        (X none) :
      Polynomial ↥(adjoin R (range x)))
    (Polynomial.X : Polynomial ↥(adjoin R (range x)))
have rw : Eq (α := Polynomial ↥(adjoin R (range x)))
  (Polynomial.map (↑hx.aevalEquiv : MvPolynomial ι R →+* ↥(adjoin R (range x)))
    ((aeval fun (o : Option ι) ↦
          o.elim Polynomial.X fun (s : ι) ↦
            (Polynomial.C : (a : MvPolynomial ι R) → Polynomial (MvPolynomial ι R)) (X s) :
        (a : MvPolynomial (Option ι) R) → Polynomial (MvPolynomial ι R))
      (X none)))
  Polynomial.X
Tactic: rw [AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply, aeval_X, Option.elim,
    Polynomial.map_X]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Basic (goal)
Goal:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hx : AlgebraicIndependent R x
rw :
  Eq (α := Polynomial ↥(adjoin R (range x)))
    (Polynomial.map (↑hx.aevalEquiv : MvPolynomial ι R →+* ↥(adjoin R (range x)))
      ((aeval fun (o : Option ι) ↦
            o.elim Polynomial.X fun (s : ι) ↦
              (Polynomial.C : (a : MvPolynomial ι R) → Polynomial (MvPolynomial ι R)) (X s) :
          (a : MvPolynomial (Option ι) R) → Polynomial (MvPolynomial ι R))
        (X none)))
    Polynomial.X
⊢ Eq.{v + 1} (α := Polynomial ↥(adjoin R (range x)))
    ((hx.mvPolynomialOptionEquivPolynomialAdjoin : (a : MvPolynomial (Option ι) R) → Polynomial ↥(adjoin R (range x)))
        (X none) :
      Polynomial ↥(adjoin R (range x)))
    (Polynomial.X : Polynomial ↥(adjoin R (range x)))
have rw₁ : Eq (α := Polynomial ↥(adjoin R (range x)))
  (Polynomial.map (↑hx.aevalEquiv : MvPolynomial ι R →+* ↥(adjoin R (range x)))
    (Option.elim none Polynomial.X fun (s : ι) ↦
      (Polynomial.C : (a : MvPolynomial ι R) → Polynomial (MvPolynomial ι R)) (X s)))
  Polynomial.X
Tactic: rw [AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply, aeval_X, Option.elim,
    Polynomial.map_X]