awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
ι : Type u
R : Type u_1
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FaithfulSMul R S
inst_4 : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj_1 : j ∈ insert i s
H₁ : IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑s : Type u)) ↦ v (↑x : ι)
this_1 : Nontrivial.{v} ↥(adjoin R (v '' (insert i s \ {j})))
this_2 : Nontrivial S
this_3 : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
hi : i ∉ s
eq : v i = v j
h :
  ∀ (x : ι) (hxj : x ∉ {j}) (hj_2 : j ∈ insert x s) (this : Nontrivial.{v} ↥(adjoin R (v '' (insert x s \ {j}))))
    (H₂ : v j ∈ (matroid R S).closure (v '' (insert x s \ {j}))) (hi : x ∉ s) (eq : v x = v j),
    v (↑(Subtype.mk (p := fun (x_1 : ι) ↦ x_1 ∈ insert x s \ {j}) x ⋯) : ι) =
      Function.comp (α := (↑(insert x s \ {j}) : Type u)) (fun (x : (↑s : Type u)) ↦ v (↑x : ι))
        (⇑((Equiv.image (Equiv.swap j x) s).trans
                (Equiv.setCongr (s := (⇑(Equiv.swap j x) : (a : ι) → ι) '' s) (t := insert x s \ {j}) ⋯)).symm :
          (a : (↑(insert x s \ {j}) : Type u)) → (↑s : Type u))
        (Subtype.mk (p := fun (x_1 : ι) ↦ x_1 ∈ insert x s \ {j}) x ⋯)
⊢ IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑(insert i s \ {j}) : Type u)) ↦ v (↑x : ι)
have h₁ : ∀ (x : ι) (hxj : x ∉ {j}) (hxi : x ∈ s),
  v (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ insert i s \ {j}) x sorry) : ι) =
    Function.comp (α := (↑(insert i s \ {j}) : Type u)) (fun (x : (↑s : Type u)) ↦ v (↑x : ι))
      (⇑((Equiv.image (Equiv.swap j i) s).trans
              (Equiv.setCongr (s := (⇑(Equiv.swap j i) : (a : ι) → ι) '' s) (t := insert i s \ {j}) sorry)).symm :
        (a : (↑(insert i s \ {j}) : Type u)) → (↑s : Type u))
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ insert i s \ {j}) x sorry)
Tactic: convert!
      H₁.comp_equiv <|
        .symm <|
          ((Equiv.swap j i).image s).trans <|
            .setCongr <| Equiv.image_swap_of_mem_of_notMem hj hi with
      ⟨x, rfl | hxi, hxj⟩
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
ι : Type u
R : Type u_1
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FaithfulSMul R S
inst_4 : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj_1 : j ∈ insert i s
H₁ : IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑s : Type u)) ↦ v (↑x : ι)
this_1 : Nontrivial.{v} ↥(adjoin R (v '' (insert i s \ {j})))
this_2 : Nontrivial S
this_3 : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
hi : i ∉ s
eq : v i = v j
⊢ IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑(insert i s \ {j}) : Type u)) ↦ v (↑x : ι)
have h : ∀ (x : ι) (hxj : x ∉ {j}) (hj_2 : j ∈ insert x s) (this : Nontrivial.{v} ↥(adjoin R (v '' (insert x s \ {j}))))
  (H₂ : v j ∈ (matroid R S).closure (v '' (insert x s \ {j}))) (hi : x ∉ s) (eq : v x = v j),
  v (↑(Subtype.mk (p := fun (x_1 : ι) ↦ x_1 ∈ insert x s \ {j}) x sorry) : ι) =
    Function.comp (α := (↑(insert x s \ {j}) : Type u)) (fun (x : (↑s : Type u)) ↦ v (↑x : ι))
      (⇑((Equiv.image (Equiv.swap j x) s).trans
              (Equiv.setCongr (s := (⇑(Equiv.swap j x) : (a : ι) → ι) '' s) (t := insert x s \ {j}) sorry)).symm :
        (a : (↑(insert x s \ {j}) : Type u)) → (↑s : Type u))
      (Subtype.mk (p := fun (x_1 : ι) ↦ x_1 ∈ insert x s \ {j}) x sorry)
Tactic: classical
    convert!
      H₁.comp_equiv <|
        .symm <|
          ((Equiv.swap j i).image s).trans <|
            .setCongr <| Equiv.image_swap_of_mem_of_notMem hj hi with
      ⟨x, rfl | hxi, hxj⟩
    · simp [eq]
    · simp [Equiv.swap_apply_of_ne_of_ne hxj (ne_of_mem_of_not_mem hxi hi)]
Cleared hypotheses: i, hj_1, this_1, H₂, hi, eq
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
ι : Type u
R : Type u_1
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FaithfulSMul R S
inst_4 : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj_1 : j ∈ insert i s
H₁ : IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑s : Type u)) ↦ v (↑x : ι)
this_1 : Nontrivial.{v} ↥(adjoin R (v '' (insert i s \ {j})))
this_2 : Nontrivial S
this_3 : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
hi : i ∉ s
eq : v i = v j
h :
  ∀ (x : ι) (hxj : x ∉ {j}) (hj_2 : j ∈ insert x s) (this : Nontrivial.{v} ↥(adjoin R (v '' (insert x s \ {j}))))
    (H₂ : v j ∈ (matroid R S).closure (v '' (insert x s \ {j}))) (hi : x ∉ s) (eq : v x = v j),
    v (↑(Subtype.mk (p := fun (x_1 : ι) ↦ x_1 ∈ insert x s \ {j}) x ⋯) : ι) =
      Function.comp (α := (↑(insert x s \ {j}) : Type u)) (fun (x : (↑s : Type u)) ↦ v (↑x : ι))
        (⇑((Equiv.image (Equiv.swap j x) s).trans
                (Equiv.setCongr (s := (⇑(Equiv.swap j x) : (a : ι) → ι) '' s) (t := insert x s \ {j}) ⋯)).symm :
          (a : (↑(insert x s \ {j}) : Type u)) → (↑s : Type u))
        (Subtype.mk (p := fun (x_1 : ι) ↦ x_1 ∈ insert x s \ {j}) x ⋯)
⊢ IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑(insert i s \ {j}) : Type u)) ↦ v (↑x : ι)
have h₁ : ∀ (x : ι) (hxj : x ∉ {j}) (hxi : x ∈ s),
  v (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ insert i s \ {j}) x sorry) : ι) =
    Function.comp (α := (↑(insert i s \ {j}) : Type u)) (fun (x : (↑s : Type u)) ↦ v (↑x : ι))
      (⇑((Equiv.image (Equiv.swap j i) s).trans
              (Equiv.setCongr (s := (⇑(Equiv.swap j i) : (a : ι) → ι) '' s) (t := insert i s \ {j}) sorry)).symm :
        (a : (↑(insert i s \ {j}) : Type u)) → (↑s : Type u))
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ insert i s \ {j}) x sorry)
Tactic: classical
    convert!
      H₁.comp_equiv <|
        .symm <|
          ((Equiv.swap j i).image s).trans <|
            .setCongr <| Equiv.image_swap_of_mem_of_notMem hj hi with
      ⟨x, rfl | hxi, hxj⟩
    · simp [eq]
    · simp [Equiv.swap_apply_of_ne_of_ne hxj (ne_of_mem_of_not_mem hxi hi)]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
ι : Type u
R : Type u_1
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FaithfulSMul R S
inst_4 : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj_1 : j ∈ insert i s
H₁ : IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑s : Type u)) ↦ v (↑x : ι)
this_1 : Nontrivial.{v} ↥(adjoin R (v '' (insert i s \ {j})))
this_2 : Nontrivial S
this_3 : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
hi : i ∉ s
ne : v i ≠ v j
his : v i ∈ v '' s
⊢ v j ∈ (matroid R S).closure (v '' s \ {v j})
have refine : v '' (insert i s \ {j}) ⊆ v '' s \ {v j}
Tactic: refine Matroid.closure_subset_closure _ ?_ H₂
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (hypothesis)
Goal:
ι : Type u
R : Type u_1
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FaithfulSMul R S
inst_4 : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj_1 : j ∈ insert i s
H₁ : IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑s : Type u)) ↦ v (↑x : ι)
this_1 : Nontrivial.{v} ↥(adjoin R (v '' (insert i s \ {j})))
this_2 : Nontrivial S
this_3 : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
hi : i ∉ s
ne : v i ≠ v j
⊢ IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑(insert i s \ {j}) : Type u)) ↦ v (↑x : ι)
have hi' : v i ∉ v '' s
Tactic: have hi' : v i ∉ v '' s := fun his ↦ Hj <| by
    refine Matroid.closure_subset_closure _ ?_ H₂
    rintro x ⟨k, ⟨rfl | hks, hkj⟩, rfl⟩
    · exact ⟨his, ne⟩
    · exact ⟨⟨k, hks, rfl⟩, inj.ne hks hj hkj⟩
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (hypothesis)
Goal:
ι : Type u
R : Type u_1
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FaithfulSMul R S
inst_4 : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj_1 : j ∈ insert i s
H₁ : IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑s : Type u)) ↦ v (↑x : ι)
this_1 : Nontrivial.{v} ↥(adjoin R (v '' (insert i s \ {j})))
this_2 : Nontrivial S
this_3 : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
hi : i ∉ s
ne : v i ≠ v j
hi' : v i ∉ v '' s
⊢ IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑(insert i s \ {j}) : Type u)) ↦ v (↑x : ι)
have this₁ : InjOn v (insert i s)
Tactic: have : (insert i s).InjOn v := (injOn_insert hi).mpr ⟨inj, hi'⟩
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
ι : Type u
R : Type u_1
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FaithfulSMul R S
inst_4 : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj_1 : j ∈ insert i s
H₁ : IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑s : Type u)) ↦ v (↑x : ι)
this_1 : Nontrivial.{v} ↥(adjoin R (v '' (insert i s \ {j})))
this_2 : Nontrivial S
this_3 : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this_4 : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
hi : i ∉ s
ne : v i ≠ v j
hi' : v i ∉ v '' s
this : InjOn v (insert i s)
⊢ IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑(insert i s \ {j}) : Type u)) ↦ v (↑x : ι)
have inr : (matroid R S).IsBase (v '' (insert i s \ {j}))
Tactic: rw [← isTranscendenceBasis_subtype_range (by exact injOn_iff_injective.1 (this.mono diff_subset)),
    ← matroid_isBase_iff, ← image_eq_range]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
ι : Type u
R : Type u_1
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FaithfulSMul R S
inst_4 : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj_1 : j ∈ insert i s
H₁ : IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑s : Type u)) ↦ v (↑x : ι)
this_1 : Nontrivial.{v} ↥(adjoin R (v '' (insert i s \ {j})))
this_2 : Nontrivial S
this_3 : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this_4 : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
hi : i ∉ s
ne : v i ≠ v j
hi' : v i ∉ v '' s
this : InjOn v (insert i s)
⊢ (matroid R S).IsBase (v '' (insert i s \ {j}))
have inr : ∀ (H₂ : v j ∈ (matroid R S).closure (insert (v i) (v '' s) \ {v j})) (this : Nontrivial R) (inj : InjOn v s)
  (H' : (matroid R S).IsBase (v '' s)) (hj : j ∈ s) (Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})) (hi : i ∉ s)
  (ne : v i ≠ v j) (hi' : v i ∉ v '' s) (this : InjOn v (insert i s)),
  (matroid R S).IsBase (insert (v i) (v '' s) \ {v j})
Tactic: rw [this.image_diff_subset (singleton_subset_iff.mpr (.inr hj)), image_singleton,
    image_insert_eq] at H₂ ⊢
Cleared hypotheses: H₂, this_4, inj, H', hj, Hj, hi, ne, hi', this
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
ι : Type u
R : Type u_1
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FaithfulSMul R S
inst_4 : NoZeroDivisors S
i j : ι
v : ι → S
H₁ : IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : { x : ι // x ≠ i }) ↦ v (↑x : ι)
H₂ : IsAlgebraic (↥(adjoin R (v '' {j}ᶜ))) (v j)
⊢ IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : { x : ι // x ≠ j }) ↦ v (↑x : ι)
have inl : ∀ (H₁ : IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : { x : ι // x ≠ j }) ↦ v (↑x : ι)),
  IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : { x : ι // x ≠ j }) ↦ v (↑x : ι)
Tactic: obtain rfl | ne := eq_or_ne j i
Cleared hypotheses: i, H₁
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
ι : Type u
R : Type u_1
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FaithfulSMul R S
inst_4 : NoZeroDivisors S
i j : ι
v : ι → S
H₁ : IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : { x : ι // x ≠ i }) ↦ v (↑x : ι)
H₂ : IsAlgebraic (↥(adjoin R (v '' {j}ᶜ))) (v j)
inl :
  ∀ (H₁ : IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : { x : ι // x ≠ j }) ↦ v (↑x : ι)),
    IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : { x : ι // x ≠ j }) ↦ v (↑x : ι)
⊢ IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : { x : ι // x ≠ j }) ↦ v (↑x : ι)
have inr : ∀ (ne : j ≠ i), IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : { x : ι // x ≠ j }) ↦ v (↑x : ι)
Tactic: obtain rfl | ne := eq_or_ne j i
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (hypothesis)
Goal:
ι : Type u
R : Type u_1
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FaithfulSMul R S
inst_4 : NoZeroDivisors S
i j : ι
v : ι → S
H₁ : IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : { x : ι // x ≠ i }) ↦ v (↑x : ι)
H₂ : IsAlgebraic (↥(adjoin R (v '' {j}ᶜ))) (v j)
ne : j ≠ i
⊢ IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : { x : ι // x ≠ j }) ↦ v (↑x : ι)
have this : ∀ (H₂ : IsAlgebraic (↥(adjoin R (v '' (insert i {i}ᶜ \ {j})))) (v j)),
  IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑(insert i {i}ᶜ \ {j}) : Type u)) ↦ v (↑x : ι)
Tactic: have := H₁.of_isAlgebraic_adjoin_insert_diff {i}ᶜ i j v (.inr ne)
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (hypothesis)
Goal:
ι : Type u
R : Type u_1
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FaithfulSMul R S
inst_4 : NoZeroDivisors S
i j : ι
v : ι → S
H₁ : IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : { x : ι // x ≠ i }) ↦ v (↑x : ι)
H₂ : IsAlgebraic (↥(adjoin R (v '' {j}ᶜ))) (v j)
ne : j ≠ i
this :
  ∀ (H₂ : IsAlgebraic (↥(adjoin R (v '' (insert i {i}ᶜ \ {j})))) (v j)),
    IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑(insert i {i}ᶜ \ {j}) : Type u)) ↦ v (↑x : ι)
⊢ IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : { x : ι // x ≠ j }) ↦ v (↑x : ι)
have this₁ : ∀ (H₂ : IsAlgebraic (↥(adjoin R (v '' {j}ᶜ))) (v j)),
  IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑{j}ᶜ : Type u)) ↦ v (↑x : ι)
Tactic: rw [compl_eq_univ_diff, insert_diff_self_of_mem (mem_univ _), ← compl_eq_univ_diff] at this
Cleared hypotheses: 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
inst_3 : Unique ι
⊢ AlgebraicIndependent R x ↔ Transcendental R (x default)
have rw : Injective (α := MvPolynomial ι R) (β := A) (⇑(aeval x) : (a : MvPolynomial ι R) → A) ↔
  Injective.{u_3 + 1, v + 1} (α := Polynomial R) (β := A) (⇑(Polynomial.aeval (x default)) : (a : Polynomial R) → A)
Tactic: rw [transcendental_iff_injective, algebraicIndependent_iff_injective_aeval]
-- 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
inst_3 : Unique ι
i : MvPolynomial ι R ≃ₐ[R] Polynomial R := uniqueAlgEquiv R ι
⊢ Eq (α := MvPolynomial ι R →ₐ[R] A) (aeval x)
    (AlgHom.comp (Polynomial.aeval (x default)) (↑i : MvPolynomial ι R →ₐ[R] Polynomial R))
have hf : ∀ (y : ι),
  Eq.{v + 1} (α := A) ((aeval x : (a : MvPolynomial ι R) → A) (X y) : A)
    ((AlgHom.comp (Polynomial.aeval (x default)) (↑i : MvPolynomial ι R →ₐ[R] Polynomial R) :
          (a : MvPolynomial ι R) → A)
        (X y) :
      A)
Tactic: ext y
-- 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
inst_3 : Unique ι
i : MvPolynomial ι R ≃ₐ[R] Polynomial R := uniqueAlgEquiv R ι
⊢ Injective (α := MvPolynomial ι R) (β := A) (⇑(aeval x) : (a : MvPolynomial ι R) → A) ↔
    Injective.{u_3 + 1, v + 1} (α := Polynomial R) (β := A) (⇑(Polynomial.aeval (x default)) : (a : Polynomial R) → A)
have key : Eq (α := MvPolynomial ι R →ₐ[R] A) (aeval x)
  (AlgHom.comp (Polynomial.aeval (x default)) (↑i : MvPolynomial ι R →ₐ[R] Polynomial R))
Tactic: have key : aeval (R := R) x = (Polynomial.aeval (R := R) (x default)).comp i := by
    ext y
    simp [i, Subsingleton.elim y default]
-- 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
hx : AlgebraicIndependent R x
i : ι
⊢ Transcendental R (x i)
have this : AlgebraicIndependent R (x ∘ ![i])
Tactic: have := hx.comp ![i] (Function.injective_of_subsingleton _)
-- 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
i : ι
this : AlgebraicIndependent R (x ∘ ![i])
⊢ AlgebraicIndependent R ![x i]
have rwa : ∀ (this : AlgebraicIndependent R (FinVec.map x ![i])), AlgebraicIndependent R ![x i]
Tactic: rwa [← FinVec.map_eq] at this
Cleared hypotheses: this
-- 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
hx : AlgebraicIndependent R x
i : ι
this : AlgebraicIndependent R (x ∘ ![i])
⊢ Transcendental R (x i)
have this₁ : AlgebraicIndependent R ![x i]
Tactic: have : AlgebraicIndependent R ![x i] := by rwa [← FinVec.map_eq] at 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
hx : AlgebraicIndependent R x
inst_3 : Algebra.IsAlgebraic R A
⊢ IsEmpty ι
have inl : ∀ (h : IsEmpty ι), IsEmpty ι
Tactic: rcases isEmpty_or_nonempty ι with h | ⟨⟨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 : Algebra.IsAlgebraic R A
inl : ∀ (h : IsEmpty ι), IsEmpty ι
⊢ IsEmpty ι
have inr : ∀ (i : ι), IsEmpty ι
Tactic: rcases isEmpty_or_nonempty ι with h | ⟨⟨i⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (goal)
Goal:
R : Type u_3
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
⊢ trdeg R A = 0 ↔ Algebra.IsAlgebraic R A
have pos : ∀ (h : Algebra.IsAlgebraic R A), trdeg R A = 0 ↔ Algebra.IsAlgebraic R A
Tactic: by_cases h : Algebra.IsAlgebraic R A
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (goal)
Goal:
R : Type u_3
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
pos : ∀ (h : Algebra.IsAlgebraic R A), trdeg R A = 0 ↔ Algebra.IsAlgebraic R A
⊢ trdeg R A = 0 ↔ Algebra.IsAlgebraic R A
have neg : ∀ (h : ¬Algebra.IsAlgebraic R A), trdeg R A = 0 ↔ Algebra.IsAlgebraic R A
Tactic: by_cases h : Algebra.IsAlgebraic R A
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (goal)
Goal:
R : Type u_3
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
h : ¬Algebra.IsAlgebraic R A
⊢ trdeg R A = 0 ↔ Algebra.IsAlgebraic R A
have neg : ¬trdeg R A = 0 ↔ ¬Algebra.IsAlgebraic R A
Tactic: rw [← not_iff_not]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (goal)
Goal:
R : Type u_3
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
h : ¬Algebra.IsAlgebraic R A
⊢ ¬trdeg R A = 0 ↔ ¬Algebra.IsAlgebraic R A
have neg : ∀ (h : Algebra.Transcendental R A), ¬trdeg R A = 0 ↔ Algebra.Transcendental R A
Tactic: rw [← Algebra.transcendental_iff_not_isAlgebraic] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (goal)
Goal:
R : Type u_3
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
⊢ trdeg R A ≠ 0 ↔ Algebra.Transcendental R A
have rw : trdeg R A ≠ 0 ↔ ¬Algebra.IsAlgebraic R A
Tactic: rw [Algebra.transcendental_iff_not_isAlgebraic, Ne, trdeg_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (goal)
Goal:
R : Type u_3
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
rw : trdeg R A ≠ 0 ↔ ¬Algebra.IsAlgebraic R A
⊢ trdeg R A ≠ 0 ↔ Algebra.Transcendental R A
have rw₁ : ¬trdeg R A = 0 ↔ ¬Algebra.IsAlgebraic R A
Tactic: rw [Algebra.transcendental_iff_not_isAlgebraic, Ne, trdeg_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.Transcendental (goal)
Goal:
R : Type u_3
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
rw : trdeg R A ≠ 0 ↔ ¬Algebra.IsAlgebraic R A
rw₁ : ¬trdeg R A = 0 ↔ ¬Algebra.IsAlgebraic R A
⊢ trdeg R A ≠ 0 ↔ Algebra.Transcendental R A
have rw₂ : ¬Algebra.IsAlgebraic R A ↔ ¬Algebra.IsAlgebraic R A
Tactic: rw [Algebra.transcendental_iff_not_isAlgebraic, Ne, trdeg_eq_zero_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
hx : AlgebraicIndependent R x
a : A
⊢ (AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (o : Option ι) ↦ o.elim a x) ↔
    Transcendental (↥(adjoin R (range x))) a
have rw : Injective (α := MvPolynomial.{u_1, u_3} (Option ι) R) (β := A)
    (Function.comp (β := Polynomial ↥(adjoin R (range x)))
      (⇑(↑(Polynomial.aeval a) : Polynomial ↥(adjoin R (range x)) →+* A) : (a : Polynomial ↥(adjoin R (range x))) → A)
      (⇑hx.mvPolynomialOptionEquivPolynomialAdjoin.toRingHom :
        (a : MvPolynomial (Option ι) R) → Polynomial ↥(adjoin R (range x)))) ↔
  Injective (α := Polynomial ↥(adjoin R (range x))) (β := A)
    (⇑(Polynomial.aeval a) : (a : Polynomial ↥(adjoin R (range x))) → A)
Tactic: rw [algebraicIndependent_iff_injective_aeval, transcendental_iff_injective,
    ← AlgHom.coe_toRingHom, ← hx.aeval_comp_mvPolynomialOptionEquivPolynomialAdjoin,
    RingHom.coe_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
s : Set ι
i : ι
h : i ∉ s
⊢ AlgebraicIndepOn R x (insert i s) ↔ AlgebraicIndepOn R x s ∧ Transcendental (↥(adjoin R (x '' s))) (x i)
have simp_rw : AlgebraicIndependent.{u_1, u_3, v} (ι := Option { i : ι // i ∈ s }) R (A := A)
    ((fun (i_1 : (↑(insert i s) : Type u_1)) ↦ x (↑i_1 : ι)) ∘
      (⇑(subtypeInsertEquivOption (t := s) h).symm :
        (a : Option { i : ι // i ∈ s }) → { i_1 : ι // i_1 ∈ insert i s })) ↔
  (AlgebraicIndependent.{u_1, u_3, v} R (A := A) fun (i : (↑s : Type u_1)) ↦ x (↑i : ι)) ∧
    Transcendental (↥(adjoin R (x '' s))) (x i)
Tactic: simp_rw [← algebraicIndependent_equiv (subtypeInsertEquivOption h).symm,
    AlgebraicIndepOn]