awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (hypothesis)
Goal:
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x : ι → A
y : ι' → 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
inst_7 : FaithfulSMul R A
inst_8 : NoZeroDivisors A
I B : Set A
I_ind : AlgebraicIndepOn R _root_.id I
B_base : IsTranscendenceBasis.{w, u_1, w} (ι := { x : A // x ∈ B }) R (Subtype.val (p := fun (x : A) ↦ x ∈ B))
h : ∀ (x : A) (_ : x ∈ B \ I), ¬AlgebraicIndepOn R _root_.id (insert x I)
h_1 : Nontrivial R
⊢ Algebra.IsAlgebraic (↥(adjoin R (range fun (i : (↑I : Type w)) ↦ _root_.id (↑i : A)))) A
have B_base₁ : Algebra.IsAlgebraic (↥(adjoin R (range (ι := { x : A // x ∈ B }) (Subtype.val (p := fun (x : A) ↦ x ∈ B))))) A
Tactic: replace B_base := B_base.isAlgebraic
Cleared hypotheses: B_base
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x : ι → A
y : ι' → 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
inst_7 : FaithfulSMul R A
inst_8 : NoZeroDivisors A
I B : Set A
I_ind : AlgebraicIndepOn R _root_.id I
h : ∀ (x : A) (_ : x ∈ B \ I), ¬AlgebraicIndepOn R _root_.id (insert x I)
h_1 : Nontrivial R
B_base : Algebra.IsAlgebraic (↥(adjoin R (range (ι := { x : A // x ∈ B }) (Subtype.val (p := fun (x : A) ↦ x ∈ B))))) A
⊢ Algebra.IsAlgebraic (↥(adjoin R (range fun (i : (↑I : Type w)) ↦ (↑i : A)))) A
have inr : ∀ (B_base : Algebra.IsAlgebraic (↥(adjoin R B)) A), Algebra.IsAlgebraic (↥(adjoin R I)) A
Tactic: rw [Subtype.range_val] at B_base ⊢
Cleared hypotheses: B_base
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x : ι → A
y : ι' → 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
inst_7 : FaithfulSMul R A
inst_8 : NoZeroDivisors A
I B : Set A
I_ind : AlgebraicIndepOn R _root_.id I
h : ∀ (x : A) (_ : x ∈ B \ I), ¬AlgebraicIndepOn R _root_.id (insert x I)
h_1 : Nontrivial R
B_base : Algebra.IsAlgebraic (↥(adjoin R B)) A
⊢ Algebra.IsAlgebraic (↥(adjoin R I)) A
have inr : ∀ (a x : A) (hx : x ∈ B \ I), IsAlgebraic (↥(adjoin R I)) x
Tactic: refine ⟨fun a ↦ (B_base.1 a).adjoin_of_forall_isAlgebraic fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x_1 : ι → A
y : ι' → 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
inst_7 : FaithfulSMul R A
inst_8 : NoZeroDivisors A
I B : Set A
I_ind : AlgebraicIndepOn R _root_.id I
h : ∀ (x : A) (_ : x ∈ B \ I), ¬AlgebraicIndepOn R _root_.id (insert x I)
h_1 : Nontrivial R
B_base : Algebra.IsAlgebraic (↥(adjoin R B)) A
a x : A
hx : x ∈ B \ I
⊢ IsAlgebraic (↥(adjoin R I)) x
have inr : ∀ (h : ¬IsAlgebraic (↥(adjoin R I)) x), ∃ x ∈ B \ I, AlgebraicIndepOn R _root_.id (insert x I)
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x_1 : ι → A
y : ι' → 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
inst_7 : FaithfulSMul R A
inst_8 : NoZeroDivisors A
I B : Set A
I_ind : AlgebraicIndepOn R _root_.id I
h_1 : Nontrivial R
B_base : Algebra.IsAlgebraic (↥(adjoin R B)) A
a x : A
hx : x ∈ B \ I
h : ¬IsAlgebraic (↥(adjoin R I)) x
⊢ Transcendental (↥(adjoin R (_root_.id '' I))) (_root_.id x)
have rwa : Transcendental (↥(adjoin R I)) (_root_.id x)
Tactic: rwa [image_id]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x : ι → A
y : ι' → 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
inst_7 : FaithfulSMul R A
inst_8 : NoZeroDivisors A
B : Set A
⊢ (fun (s : Set A) ↦
        IsTranscendenceBasis.{w, u_1, w} (ι := { x : A // x ∈ s }) R (Subtype.val (p := fun (x : A) ↦ x ∈ s)))
      B ↔
    (indepMatroid R A).matroid.IsBase B
have simp_rw : Maximal (AlgebraicIndepOn R _root_.id) B ↔ Maximal (indepMatroid R A).matroid.Indep B
Tactic: simp_rw [Matroid.isBase_iff_maximal_indep, isTranscendenceBasis_iff_maximal]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
inst_4 : IsDomain A
s t : Set A
⊢ (matroid R A).IsBasis s t ↔ AlgebraicIndepOn R _root_.id s ∧ s ⊆ t ∧ ∀ a ∈ t, IsAlgebraic (↥(adjoin R s)) a
have rw : (((matroid R A).Indep s ∧ s ⊆ t) ∧ ∀ x ∉ s, ¬((matroid R A).Indep (insert x s) ∧ insert x s ⊆ t)) ∧
    t ⊆ (matroid R A).E ↔
  AlgebraicIndepOn R _root_.id s ∧ s ⊆ t ∧ ∀ a ∈ t, IsAlgebraic (↥(adjoin R s)) a
Tactic: rw [Matroid.IsBasis, maximal_iff_forall_insert fun s t h hst ↦ ⟨h.1.subset hst, hst.trans h.2⟩]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
inst_4 : IsDomain A
s t : Set A
⊢ (((matroid R A).Indep s ∧ s ⊆ t) ∧ ∀ x ∉ s, ¬((matroid R A).Indep (insert x s) ∧ insert x s ⊆ t)) ∧
      t ⊆ (matroid R A).E ↔
    AlgebraicIndepOn R _root_.id s ∧ s ⊆ t ∧ ∀ a ∈ t, IsAlgebraic (↥(adjoin R s)) a
have simp_rw : ((AlgebraicIndepOn R _root_.id s ∧ s ⊆ t) ∧ ∀ x ∉ s, ¬(AlgebraicIndepOn R _root_.id (insert x s) ∧ insert x s ⊆ t)) ↔
  (AlgebraicIndepOn R _root_.id s ∧ s ⊆ t) ∧ ∀ a ∈ t, IsAlgebraic (↥(adjoin R s)) a
Tactic: simp_rw [matroid_indep_iff, ← and_assoc, matroid_e, subset_univ, and_true]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
inst_4 : IsDomain A
s t : Set A
h : AlgebraicIndepOn R _root_.id s ∧ s ⊆ t
max : ∀ x ∉ s, ¬(AlgebraicIndepOn R _root_.id (insert x s) ∧ insert x s ⊆ t)
a : A
ha : a ∈ t
tr : ¬IsAlgebraic (↥(adjoin R s)) a
⊢ Transcendental (↥(adjoin R (_root_.id '' s))) (_root_.id a)
have rwa : Transcendental (↥(adjoin R s)) (_root_.id a)
Tactic: rwa [image_id]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
inst_4 : IsDomain A
s t : Set A
h_1 : AlgebraicIndepOn R _root_.id s ∧ s ⊆ t
alg : ∀ a ∈ t, IsAlgebraic (↥(adjoin R s)) a
a : A
ha : a ∉ s
h : AlgebraicIndepOn R _root_.id (insert a s) ∧ insert a s ⊆ t
⊢ IsAlgebraic (↥(adjoin R (_root_.id '' s))) (_root_.id a)
have rw : IsAlgebraic (↥(adjoin R s)) (_root_.id a)
Tactic: rw [image_id]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (hypothesis)
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
inst_4 : Subsingleton A
s t : Set A
⊢ (matroid R A).IsBasis s t ↔ s = t
have this : Subsingleton R
Tactic: have := (FaithfulSMul.algebraMap_injective R A).subsingleton
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
inst_4 : Subsingleton A
s t : Set A
this : Subsingleton R
⊢ (matroid R A).IsBasis s t ↔ s = t
have simp_rw : Maximal (fun (A_1 : Set A) ↦ (matroid R A).Indep A_1 ∧ A_1 ⊆ t) s ∧ t ⊆ (matroid R A).E ↔ s = t
Tactic: simp_rw [Matroid.IsBasis, matroid_indep_iff, of_subsingleton, true_and,
    matroid_e, subset_univ, and_true, ← le_iff_subset, maximal_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
inst_4 : Subsingleton A
s t : Set A
this : Subsingleton R
simp_rw : Maximal (fun (A_1 : Set A) ↦ (matroid R A).Indep A_1 ∧ A_1 ⊆ t) s ∧ t ⊆ (matroid R A).E ↔ s = t
⊢ (matroid R A).IsBasis s t ↔ s = t
have simp_rw₁ : Maximal (fun (A_1 : Set A) ↦ AlgebraicIndepOn R _root_.id A_1 ∧ A_1 ⊆ t) s ∧ t ⊆ (matroid R A).E ↔ s = t
Tactic: simp_rw [Matroid.IsBasis, matroid_indep_iff, of_subsingleton, true_and,
    matroid_e, subset_univ, and_true, ← le_iff_subset, maximal_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
inst_4 : Subsingleton A
s t : Set A
this : Subsingleton R
simp_rw : Maximal (fun (A_1 : Set A) ↦ (matroid R A).Indep A_1 ∧ A_1 ⊆ t) s ∧ t ⊆ (matroid R A).E ↔ s = t
simp_rw₁ : Maximal (fun (A_1 : Set A) ↦ AlgebraicIndepOn R _root_.id A_1 ∧ A_1 ⊆ t) s ∧ t ⊆ (matroid R A).E ↔ s = t
⊢ (matroid R A).IsBasis s t ↔ s = t
have simp_rw₂ : Maximal (fun (A_1 : Set A) ↦ True ∧ A_1 ⊆ t) s ∧ t ⊆ (matroid R A).E ↔ s = t
Tactic: simp_rw [Matroid.IsBasis, matroid_indep_iff, of_subsingleton, true_and,
    matroid_e, subset_univ, and_true, ← le_iff_subset, maximal_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
inst_4 : Subsingleton A
s t : Set A
this : Subsingleton R
simp_rw : Maximal (fun (A_1 : Set A) ↦ (matroid R A).Indep A_1 ∧ A_1 ⊆ t) s ∧ t ⊆ (matroid R A).E ↔ s = t
simp_rw₁ : Maximal (fun (A_1 : Set A) ↦ AlgebraicIndepOn R _root_.id A_1 ∧ A_1 ⊆ t) s ∧ t ⊆ (matroid R A).E ↔ s = t
simp_rw₂ : Maximal (fun (A_1 : Set A) ↦ True ∧ A_1 ⊆ t) s ∧ t ⊆ (matroid R A).E ↔ s = t
⊢ (matroid R A).IsBasis s t ↔ s = t
have simp_rw₃ : Maximal (fun (A_1 : Set A) ↦ A_1 ⊆ t) s ∧ t ⊆ (matroid R A).E ↔ s = t
Tactic: simp_rw [Matroid.IsBasis, matroid_indep_iff, of_subsingleton, true_and,
    matroid_e, subset_univ, and_true, ← le_iff_subset, maximal_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
inst_4 : Subsingleton A
s t : Set A
this : Subsingleton R
simp_rw : Maximal (fun (A_1 : Set A) ↦ (matroid R A).Indep A_1 ∧ A_1 ⊆ t) s ∧ t ⊆ (matroid R A).E ↔ s = t
simp_rw₁ : Maximal (fun (A_1 : Set A) ↦ AlgebraicIndepOn R _root_.id A_1 ∧ A_1 ⊆ t) s ∧ t ⊆ (matroid R A).E ↔ s = t
simp_rw₂ : Maximal (fun (A_1 : Set A) ↦ True ∧ A_1 ⊆ t) s ∧ t ⊆ (matroid R A).E ↔ s = t
simp_rw₃ : Maximal (fun (A_1 : Set A) ↦ A_1 ⊆ t) s ∧ t ⊆ (matroid R A).E ↔ s = t
⊢ (matroid R A).IsBasis s t ↔ s = t
have simp_rw₄ : Maximal (fun (A_1 : Set A) ↦ A_1 ⊆ t) s ∧ t ⊆ univ ↔ s = t
Tactic: simp_rw [Matroid.IsBasis, matroid_indep_iff, of_subsingleton, true_and,
    matroid_e, subset_univ, and_true, ← le_iff_subset, maximal_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
inst_4 : Subsingleton A
s t : Set A
this : Subsingleton R
simp_rw : Maximal (fun (A_1 : Set A) ↦ (matroid R A).Indep A_1 ∧ A_1 ⊆ t) s ∧ t ⊆ (matroid R A).E ↔ s = t
simp_rw₁ : Maximal (fun (A_1 : Set A) ↦ AlgebraicIndepOn R _root_.id A_1 ∧ A_1 ⊆ t) s ∧ t ⊆ (matroid R A).E ↔ s = t
simp_rw₂ : Maximal (fun (A_1 : Set A) ↦ True ∧ A_1 ⊆ t) s ∧ t ⊆ (matroid R A).E ↔ s = t
simp_rw₃ : Maximal (fun (A_1 : Set A) ↦ A_1 ⊆ t) s ∧ t ⊆ (matroid R A).E ↔ s = t
simp_rw₄ : Maximal (fun (A_1 : Set A) ↦ A_1 ⊆ t) s ∧ t ⊆ univ ↔ s = t
⊢ (matroid R A).IsBasis s t ↔ s = t
have simp_rw₅ : Maximal (fun (A_1 : Set A) ↦ A_1 ⊆ t) s ∧ True ↔ s = t
Tactic: simp_rw [Matroid.IsBasis, matroid_indep_iff, of_subsingleton, true_and,
    matroid_e, subset_univ, and_true, ← le_iff_subset, maximal_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
inst_4 : Subsingleton A
s t : Set A
this : Subsingleton R
simp_rw : Maximal (fun (A_1 : Set A) ↦ (matroid R A).Indep A_1 ∧ A_1 ⊆ t) s ∧ t ⊆ (matroid R A).E ↔ s = t
simp_rw₁ : Maximal (fun (A_1 : Set A) ↦ AlgebraicIndepOn R _root_.id A_1 ∧ A_1 ⊆ t) s ∧ t ⊆ (matroid R A).E ↔ s = t
simp_rw₂ : Maximal (fun (A_1 : Set A) ↦ True ∧ A_1 ⊆ t) s ∧ t ⊆ (matroid R A).E ↔ s = t
simp_rw₃ : Maximal (fun (A_1 : Set A) ↦ A_1 ⊆ t) s ∧ t ⊆ (matroid R A).E ↔ s = t
simp_rw₄ : Maximal (fun (A_1 : Set A) ↦ A_1 ⊆ t) s ∧ t ⊆ univ ↔ s = t
simp_rw₅ : Maximal (fun (A_1 : Set A) ↦ A_1 ⊆ t) s ∧ True ↔ s = t
⊢ (matroid R A).IsBasis s t ↔ s = t
have simp_rw₆ : Maximal (fun (A_1 : Set A) ↦ A_1 ⊆ t) s ↔ s = t
Tactic: simp_rw [Matroid.IsBasis, matroid_indep_iff, of_subsingleton, true_and,
    matroid_e, subset_univ, and_true, ← le_iff_subset, maximal_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
inst_4 : Subsingleton A
s t : Set A
this : Subsingleton R
simp_rw : Maximal (fun (A_1 : Set A) ↦ (matroid R A).Indep A_1 ∧ A_1 ⊆ t) s ∧ t ⊆ (matroid R A).E ↔ s = t
simp_rw₁ : Maximal (fun (A_1 : Set A) ↦ AlgebraicIndepOn R _root_.id A_1 ∧ A_1 ⊆ t) s ∧ t ⊆ (matroid R A).E ↔ s = t
simp_rw₂ : Maximal (fun (A_1 : Set A) ↦ True ∧ A_1 ⊆ t) s ∧ t ⊆ (matroid R A).E ↔ s = t
simp_rw₃ : Maximal (fun (A_1 : Set A) ↦ A_1 ⊆ t) s ∧ t ⊆ (matroid R A).E ↔ s = t
simp_rw₄ : Maximal (fun (A_1 : Set A) ↦ A_1 ⊆ t) s ∧ t ⊆ univ ↔ s = t
simp_rw₅ : Maximal (fun (A_1 : Set A) ↦ A_1 ⊆ t) s ∧ True ↔ s = t
simp_rw₆ : Maximal (fun (A_1 : Set A) ↦ A_1 ⊆ t) s ↔ s = t
⊢ (matroid R A).IsBasis s t ↔ s = t
have simp_rw₇ : Maximal (fun (A_1 : Set A) ↦ A_1 ≤ t) s ↔ s = t
Tactic: simp_rw [Matroid.IsBasis, matroid_indep_iff, of_subsingleton, true_and,
    matroid_e, subset_univ, and_true, ← le_iff_subset, maximal_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
inst_4 : NoZeroDivisors A
s t : Set A
a : A
h : (matroid R A).IsBasis s t
⊢ IsAlgebraic (↥(adjoin R s)) a ↔ IsAlgebraic (↥(adjoin R t)) a
have inl : Subsingleton A → (IsAlgebraic (↥(adjoin R s)) a ↔ IsAlgebraic (↥(adjoin R t)) a)
Tactic: cases subsingleton_or_nontrivial A
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
inst_4 : NoZeroDivisors A
s t : Set A
a : A
h : (matroid R A).IsBasis s t
inl : Subsingleton A → (IsAlgebraic (↥(adjoin R s)) a ↔ IsAlgebraic (↥(adjoin R t)) a)
⊢ IsAlgebraic (↥(adjoin R s)) a ↔ IsAlgebraic (↥(adjoin R t)) a
have inr : Nontrivial A → (IsAlgebraic (↥(adjoin R s)) a ↔ IsAlgebraic (↥(adjoin R t)) a)
Tactic: cases subsingleton_or_nontrivial A
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
inst_4 : NoZeroDivisors A
s t : Set A
a : A
h : (matroid R A).IsBasis s t
h_1 : Subsingleton A
⊢ IsAlgebraic (↥(adjoin R s)) a ↔ IsAlgebraic (↥(adjoin R t)) a
have inl : ¬IsAlgebraic (↥(adjoin R s)) a
Tactic: apply iff_of_false
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
inst_4 : NoZeroDivisors A
s t : Set A
a : A
h : (matroid R A).IsBasis s t
h_1 : Subsingleton A
inl : ¬IsAlgebraic (↥(adjoin R s)) a
⊢ IsAlgebraic (↥(adjoin R s)) a ↔ IsAlgebraic (↥(adjoin R t)) a
have inl₁ : ¬IsAlgebraic (↥(adjoin R t)) a
Tactic: apply iff_of_false
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (hypothesis)
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
inst_4 : NoZeroDivisors A
s t : Set A
a : A
h : (matroid R A).IsBasis s t
h_1 : Nontrivial A
⊢ IsAlgebraic (↥(adjoin R s)) a ↔ IsAlgebraic (↥(adjoin R t)) a
have this : IsDomain A
Tactic: have := (isDomain_iff_noZeroDivisors_and_nontrivial A).mpr ⟨inferInstance, inferInstance⟩
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
inst_4 : IsDomain A
s : Set A
⊢ (matroid R A).closure s = (↑(algebraicClosure (↥(adjoin R s)) A) : Set A)
have have : ∀ (B : Set A) (hB : (matroid R A).IsBasis B s),
  (matroid R A).closure s = (↑(algebraicClosure (↥(adjoin R s)) A) : Set A)
Tactic: have ⟨B, hB⟩ := (matroid R A).exists_isBasis s
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
inst_4 : IsDomain A
s B : Set A
hB : (matroid R A).IsBasis B s
⊢ (matroid R A).closure s = (↑(algebraicClosure (↥(adjoin R s)) A) : Set A)
have simp_rw : ∀ (x : A), (IsAlgebraic (↥(adjoin R B)) x ∧ ∀ x ∈ B, IsAlgebraic (↥(adjoin R B)) x) ↔ IsAlgebraic (↥(adjoin R B)) x
Tactic: simp_rw [← hB.closure_eq_closure, hB.1.1.1.closure_eq_setOf_isBasis_insert, Set.ext_iff,
    mem_setOf, matroid_isBasis_iff, ← matroid_indep_iff, hB.1.1.1, subset_insert, true_and,
    SetLike.mem_coe, mem_algebraicClosure, ← isAlgebraic_adjoin_iff_of_matroid_isBasis hB,
    forall_mem_insert]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
inst_4 : IsDomain A
s : Set A
⊢ (matroid R A).IsFlat s ↔ ∃ (S : Subalgebra R A), (↑S : Set A) = s ∧ ∀ (a : A), IsAlgebraic (↥S) a → a ∈ s
have rw : (↑(algebraicClosure (↥(adjoin R s)) A) : Set A) = s ↔
  ∃ (S : Subalgebra R A), (↑S : Set A) = s ∧ ∀ (a : A), IsAlgebraic (↥S) a → a ∈ s
Tactic: rw [Matroid.isFlat_iff_closure_eq, matroid_closure_eq]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
inst_4 : IsDomain A
s : Set A
S : Subalgebra (↥(adjoin R s)) A := algebraicClosure (↥(adjoin R s)) A
⊢ (↑S : Set A) = s ↔ ∃ (S : Subalgebra R A), (↑S : Set A) = s ∧ ∀ (a : A), IsAlgebraic (↥S) a → a ∈ s
have refine_1 : ∀ (eq : (↑S : Set A) = s) (a : A) (h : IsAlgebraic (↥S) a), a ∈ s
Tactic: refine ⟨fun eq ↦ ⟨S.restrictScalars R, eq, fun a (h : IsAlgebraic S _) ↦ ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
inst_4 : IsDomain A
s : Set A
S : Subalgebra (↥(adjoin R s)) A := algebraicClosure (↥(adjoin R s)) A
refine_1 : ∀ (eq : (↑S : Set A) = s) (a : A) (h : IsAlgebraic (↥S) a), a ∈ s
⊢ (↑S : Set A) = s ↔ ∃ (S : Subalgebra R A), (↑S : Set A) = s ∧ ∀ (a : A), IsAlgebraic (↥S) a → a ∈ s
have refine_2 : (∃ (S : Subalgebra R A), (↑S : Set A) = s ∧ ∀ (a : A), IsAlgebraic (↥S) a → a ∈ s) → (↑S : Set A) = s
Tactic: refine ⟨fun eq ↦ ⟨S.restrictScalars R, eq, fun a (h : IsAlgebraic S _) ↦ ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
inst_4 : IsDomain A
s : Set A
S : Subalgebra (↥(adjoin R s)) A := algebraicClosure (↥(adjoin R s)) A
eq : (↑S : Set A) = s
a : A
h : IsAlgebraic (↥S) a
⊢ a ∈ s
have refine_1 : a ∈ (↑S : Set A)
Tactic: rw [← eq]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
inst_4 : IsDomain A
s : Subalgebra R A
S : Subalgebra (↥(adjoin R (↑s : Set A))) A := algebraicClosure (↥(adjoin R (↑s : Set A))) A
hs : ∀ (a : A), IsAlgebraic (↥s) a → a ∈ (↑s : Set A)
⊢ (↑S : Set A) = (↑s : Set A)
have refine_2 : ∀ (a : A) (h : a ∈ (↑s : Set A)), a ∈ (↑S : Set A)
Tactic: refine Set.ext fun a ↦ ⟨(hs _ <| adjoin_eq s ▸ ·), fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
inst_4 : IsDomain A
s : Set A
⊢ (matroid R A).Spanning s ↔ Algebra.IsAlgebraic (↥(adjoin R s)) A
have simp_rw : (matroid R A).closure s = (matroid R A).E ∧ s ⊆ (matroid R A).E ↔ Algebra.IsAlgebraic (↥(adjoin R s)) A
Tactic: simp_rw [Matroid.spanning_iff, matroid_e, subset_univ, and_true, eq_univ_iff_forall,
    matroid_closure_eq, SetLike.mem_coe, mem_algebraicClosure, Algebra.isAlgebraic_def]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
inst_4 : IsDomain A
s : Set A
simp_rw : (matroid R A).closure s = (matroid R A).E ∧ s ⊆ (matroid R A).E ↔ Algebra.IsAlgebraic (↥(adjoin R s)) A
⊢ (matroid R A).Spanning s ↔ Algebra.IsAlgebraic (↥(adjoin R s)) A
have simp_rw₁ : (matroid R A).closure s = univ ∧ s ⊆ univ ↔ Algebra.IsAlgebraic (↥(adjoin R s)) A
Tactic: simp_rw [Matroid.spanning_iff, matroid_e, subset_univ, and_true, eq_univ_iff_forall,
    matroid_closure_eq, SetLike.mem_coe, mem_algebraicClosure, Algebra.isAlgebraic_def]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
inst_4 : IsDomain A
s : Set A
simp_rw : (matroid R A).closure s = (matroid R A).E ∧ s ⊆ (matroid R A).E ↔ Algebra.IsAlgebraic (↥(adjoin R s)) A
simp_rw₁ : (matroid R A).closure s = univ ∧ s ⊆ univ ↔ Algebra.IsAlgebraic (↥(adjoin R s)) A
⊢ (matroid R A).Spanning s ↔ Algebra.IsAlgebraic (↥(adjoin R s)) A
have simp_rw₂ : (matroid R A).closure s = univ ∧ True ↔ Algebra.IsAlgebraic (↥(adjoin R s)) A
Tactic: simp_rw [Matroid.spanning_iff, matroid_e, subset_univ, and_true, eq_univ_iff_forall,
    matroid_closure_eq, SetLike.mem_coe, mem_algebraicClosure, Algebra.isAlgebraic_def]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
inst_4 : IsDomain A
s : Set A
simp_rw : (matroid R A).closure s = (matroid R A).E ∧ s ⊆ (matroid R A).E ↔ Algebra.IsAlgebraic (↥(adjoin R s)) A
simp_rw₁ : (matroid R A).closure s = univ ∧ s ⊆ univ ↔ Algebra.IsAlgebraic (↥(adjoin R s)) A
simp_rw₂ : (matroid R A).closure s = univ ∧ True ↔ Algebra.IsAlgebraic (↥(adjoin R s)) A
⊢ (matroid R A).Spanning s ↔ Algebra.IsAlgebraic (↥(adjoin R s)) A
have simp_rw₃ : (matroid R A).closure s = univ ↔ Algebra.IsAlgebraic (↥(adjoin R s)) A
Tactic: simp_rw [Matroid.spanning_iff, matroid_e, subset_univ, and_true, eq_univ_iff_forall,
    matroid_closure_eq, SetLike.mem_coe, mem_algebraicClosure, Algebra.isAlgebraic_def]