awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
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
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
⊢ (((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:
simp_rw [matroid_indep_iff, ← and_assoc, matroid_e, subset_univ, and_true]

Premises used: AlgebraicIndependent.matroid_indep_iff, and_true, Set.subset_univ, and_assoc, AlgebraicIndependent.matroid_e
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
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
rwa rwa₁ rwa₂ rwa₃ : Transcendental (↥(adjoin R s)) (_root_.id a)
⊢ Transcendental (↥(adjoin R (_root_.id '' s))) (_root_.id a)

Tactic:
rwa [image_id]

Premises used: Set.image_id
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
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
rw : IsAlgebraic (↥(adjoin R s)) (_root_.id a)
⊢ IsAlgebraic (↥(adjoin R (_root_.id '' s))) (_root_.id a)

Tactic:
rw [image_id]

Premises used: Set.image_id
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
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 s)) (_root_.id a)

Tactic:
alg _ <| h.2 <| mem_insert ..

Premises used: And.right, Set.mem_insert
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
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 s)) (_root_.id a)

Tactic:
exact alg _ <| h.2 <| mem_insert ..

Premises used: And.right, Set.mem_insert
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
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
⊢ ((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:
exact and_congr_right fun h ↦ ⟨fun max a ha ↦ of_not_not fun tr ↦ max _
    (fun ha ↦ tr (isAlgebraic_algebraMap (⟨a, subset_adjoin ha⟩ : adjoin R s)))
      ⟨.insert h.1 (by rwa [image_id]), insert_subset ha h.2⟩,
    fun alg a ha h ↦ ((AlgebraicIndepOn.insert_iff ha).mp h.1).2 <| by
      rw [image_id]; exact alg _ <| h.2 <| mem_insert ..⟩

Premises used: and_congr_right, Iff.intro
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
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
⊢ Subsingleton R

Tactic:
have := (FaithfulSMul.algebraMap_injective R A).subsingleton
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
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
simp_rw₇ : Maximal (fun (A_1 : Set A) ↦ A_1 ≤ t) s ↔ s = t
⊢ (matroid R A).IsBasis s t ↔ 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]

Premises used: AlgebraicIndependent.matroid_indep_iff, and_true, Set.subset_univ, AlgebraicIndependent.matroid_e, AlgebraicIndependent.of_subsingleton, Set.le_iff_subset, Matroid.IsBasis, maximal_le_iff, true_and
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
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)
inr : Nontrivial A → (IsAlgebraic (↥(adjoin R s)) a ↔ IsAlgebraic (↥(adjoin R t)) a)
⊢ IsAlgebraic (↥(adjoin R s)) a ↔ IsAlgebraic (↥(adjoin R t)) a

Tactic:
cases subsingleton_or_nontrivial A

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
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
inl₁ : ¬IsAlgebraic (↥(adjoin R t)) a
⊢ IsAlgebraic (↥(adjoin R s)) a ↔ IsAlgebraic (↥(adjoin R t)) a

Tactic:
apply iff_of_false

Premises used: iff_of_false
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
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

Tactic:
apply is_transcendental_of_subsingleton

Premises used: is_transcendental_of_subsingleton
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
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 t)) a

Tactic:
apply is_transcendental_of_subsingleton

Premises used: is_transcendental_of_subsingleton
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
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
⊢ IsDomain A

Tactic:
have := (isDomain_iff_noZeroDivisors_and_nontrivial A).mpr ⟨inferInstance, inferInstance⟩
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
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
this : IsDomain A
⊢ IsAlgebraic (↥(adjoin R s)) a ↔ IsAlgebraic (↥(adjoin R t)) a

Tactic:
⟨(·.adjoin_of_forall_isAlgebraic fun x hx ↦ (hx.2 <| h.1.1.2 hx.1).elim),
    (·.adjoin_of_forall_isAlgebraic fun x hx ↦ (matroid_isBasis_iff.mp h).2.2 _ hx.1)⟩

Premises used: AlgebraicIndependent.matroid_isBasis_iff, False.elim, IsAlgebraic.adjoin_of_forall_isAlgebraic, And.right, And.left, Iff.intro, Iff.mp
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
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
this : IsDomain A
⊢ IsAlgebraic (↥(adjoin R s)) a ↔ IsAlgebraic (↥(adjoin R t)) a

Tactic:
exact ⟨(·.adjoin_of_forall_isAlgebraic fun x hx ↦ (hx.2 <| h.1.1.2 hx.1).elim),
    (·.adjoin_of_forall_isAlgebraic fun x hx ↦ (matroid_isBasis_iff.mp h).2.2 _ hx.1)⟩
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
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
have :
  ∀ (B : Set A) (hB : (matroid R A).IsBasis B s),
    (matroid R A).closure s = (↑(algebraicClosure (↥(adjoin R s)) A) : Set A)
⊢ (matroid R A).closure s = (↑(algebraicClosure (↥(adjoin R s)) A) : Set A)

Tactic:
have ⟨B, hB⟩ := (matroid R A).exists_isBasis s
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
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
simp_rw :
  ∀ (x : A), (IsAlgebraic (↥(adjoin R B)) x ∧ ∀ x ∈ B, IsAlgebraic (↥(adjoin R B)) x) ↔ IsAlgebraic (↥(adjoin R B)) x
⊢ (matroid R A).closure s = (↑(algebraicClosure (↥(adjoin R s)) A) : Set A)

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]

Premises used: Set.forall_mem_insert, Subalgebra.mem_algebraicClosure, AlgebraicIndependent.matroid_indep_iff, AlgebraicIndependent.matroid_isBasis_iff, AlgebraicIndependent.isAlgebraic_adjoin_iff_of_matroid_isBasis, Matroid.Indep.closure_eq_setOf_isBasis_insert, Set.mem_setOf, And.left, SetLike.mem_coe, Set.ext_iff, Set.subset_insert, true_and, Matroid.IsBasis.closure_eq_closure
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
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
⊢ ∀ (x : A), (IsAlgebraic (↥(adjoin R B)) x ∧ ∀ x ∈ B, IsAlgebraic (↥(adjoin R B)) x) ↔ IsAlgebraic (↥(adjoin R B)) x

Tactic:
fun _ ↦ and_iff_left fun x hx ↦ isAlgebraic_algebraMap (⟨x, subset_adjoin hx⟩ : adjoin R B)

Premises used: Algebra.subset_adjoin, and_iff_left, Subtype.mk, isAlgebraic_algebraMap
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
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
⊢ ∀ (x : A), (IsAlgebraic (↥(adjoin R B)) x ∧ ∀ x ∈ B, IsAlgebraic (↥(adjoin R B)) x) ↔ IsAlgebraic (↥(adjoin R B)) x

Tactic:
exact fun _ ↦ and_iff_left fun x hx ↦ isAlgebraic_algebraMap (⟨x, subset_adjoin hx⟩ : adjoin R B)

Premises used: Algebra.subset_adjoin, and_iff_left, Subtype.mk, isAlgebraic_algebraMap
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
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
rw :
  (↑(algebraicClosure (↥(adjoin R s)) A) : Set A) = s ↔
    ∃ (S : Subalgebra R A), (↑S : Set A) = s ∧ ∀ (a : A), IsAlgebraic (↥S) a → a ∈ s
⊢ (matroid R A).IsFlat 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]

Premises used: Matroid.isFlat_iff_closure_eq, AlgebraicIndependent.matroid_closure_eq
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
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
set :
  let 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
⊢ (↑(algebraicClosure (↥(adjoin R s)) A) : Set A) = s ↔
    ∃ (S : Subalgebra R A), (↑S : Set A) = s ∧ ∀ (a : A), IsAlgebraic (↥S) a → a ∈ s

Tactic:
set S := algebraicClosure (adjoin R s) A

Premises used: Algebra.adjoin, Membership.mem, Subtype, Subalgebra.algebraicClosure
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
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

Tactic:
⟨fun eq ↦ ⟨S.restrictScalars R, eq, fun a (h : IsAlgebraic S _) ↦ ?_⟩, ?_⟩

Premises used: And.intro, Iff.intro, Exists.intro, Subalgebra.restrictScalars
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
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
refine_2 : (∃ (S : Subalgebra R A), (↑S : Set A) = s ∧ ∀ (a : A), IsAlgebraic (↥S) a → a ∈ s) → (↑S : Set A) = s
⊢ (↑S : Set A) = s ↔ ∃ (S : Subalgebra R A), (↑S : Set A) = s ∧ ∀ (a : A), IsAlgebraic (↥S) a → a ∈ s

Tactic:
refine ⟨fun eq ↦ ⟨S.restrictScalars R, eq, fun a (h : IsAlgebraic S _) ↦ ?_⟩, ?_⟩
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
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
refine_1 : a ∈ (↑S : Set A)
⊢ a ∈ s

Tactic:
rw [← eq]
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
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 : Set A)

Tactic:
h.restrictScalars (adjoin R s)

Premises used: IsAlgebraic, IsAlgebraic.restrictScalars, Set.Mem, setOf, Algebra.adjoin, Membership.mem, Subtype
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
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 : Set A)

Tactic:
exact h.restrictScalars (adjoin R s)

Premises used: IsAlgebraic.restrictScalars, Algebra.adjoin, Membership.mem, Subtype
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
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)

Tactic:
Set.ext fun a ↦ ⟨(hs _ <| adjoin_eq s ▸ ·), fun h ↦ ?_⟩

Premises used: Set.ext, Eq.rec, Iff.intro, Algebra.adjoin_eq
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
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)
refine_2 : ∀ (a : A) (h : a ∈ (↑s : Set A)), a ∈ (↑S : Set A)
⊢ (↑S : Set A) = (↑s : Set A)

Tactic:
refine Set.ext fun a ↦ ⟨(hs _ <| adjoin_eq s ▸ ·), fun h ↦ ?_⟩

Premises used: Set.ext, Eq.rec, Iff.intro, Algebra.adjoin_eq
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
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)
a : A
h : a ∈ (↑s : Set A)
⊢ ↥(adjoin R (↑s : Set A))

Tactic:
exact (⟨a, subset_adjoin h⟩ : adjoin R s)

Premises used: Algebra.subset_adjoin, Subtype.mk
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
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)
a : A
h : a ∈ (↑s : Set A)
⊢ a ∈ (↑S : Set A)

Tactic:
exact isAlgebraic_algebraMap (A := A) (by exact (⟨a, subset_adjoin h⟩ : adjoin R s))

Premises used: isAlgebraic_algebraMap
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
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
simp_rw₃ : (matroid R A).closure s = univ ↔ Algebra.IsAlgebraic (↥(adjoin R s)) A
simp_rw₄ : (∀ (x : A), x ∈ (matroid R A).closure s) ↔ Algebra.IsAlgebraic (↥(adjoin R s)) A
simp_rw₅ : (∀ (x : A), x ∈ (↑(algebraicClosure (↥(adjoin R s)) A) : Set A)) ↔ Algebra.IsAlgebraic (↥(adjoin R s)) A
simp_rw₆ :
  (∀ (x : A), Membership.mem (γ := Subalgebra (↥(adjoin R s)) A) (algebraicClosure (↥(adjoin R s)) A) x) ↔
    Algebra.IsAlgebraic (↥(adjoin R s)) A
simp_rw₇ : (∀ (x : A), IsAlgebraic (↥(adjoin R s)) x) ↔ Algebra.IsAlgebraic (↥(adjoin R s)) A
⊢ (matroid R A).Spanning s ↔ 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]

Premises used: Subalgebra.mem_algebraicClosure, and_true, Set.subset_univ, Set.eq_univ_iff_forall, Matroid.spanning_iff, Algebra.isAlgebraic_def, SetLike.mem_coe, AlgebraicIndependent.matroid_e, AlgebraicIndependent.matroid_closure_eq
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
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 : Set A
simp_rw : ∀ ⦃I X : Set A⦄, I = s → I = X → X ⊆ s
⊢ (matroid R A).IsFlat s

Tactic:
simp_rw [Matroid.isFlat_iff, matroid_e, subset_univ,
    and_true, matroid_isBasis_iff_of_subsingleton]

Premises used: and_true, Set.subset_univ, AlgebraicIndependent.matroid_e, AlgebraicIndependent.matroid_isBasis_iff_of_subsingleton, Matroid.isFlat_iff
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
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 : Set A
⊢ ∀ ⦃I X : Set A⦄, I = s → I = X → X ⊆ s

Tactic:
fun I X hIs hIX ↦ (hIX.symm.trans hIs).subset

Premises used: Eq.subset, Eq.symm, Eq.trans
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
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 : Set A
⊢ ∀ ⦃I X : Set A⦄, I = s → I = X → X ⊆ s

Tactic:
exact fun I X hIs hIX ↦ (hIX.symm.trans hIs).subset
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
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 : Set A
simp_rw : ⋂₀ {F : Set A | s ⊆ F} = s
⊢ (matroid R A).closure s = s

Tactic:
simp_rw [Matroid.closure, matroid_isFlat_of_subsingleton, true_and, matroid_e, inter_univ]

Premises used: AlgebraicIndependent.matroid_isFlat_of_subsingleton, Set.inter_univ, AlgebraicIndependent.matroid_e, Matroid.closure, true_and
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
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 : Set A
⊢ ⋂₀ {F : Set A | s ⊆ F} = s

Tactic:
subset_antisymm (sInter_subset_of_mem <| subset_refl s) (subset_sInter fun _ ↦ id)

Premises used: id, subset_antisymm, subset_refl, Set.sInter_subset_of_mem, Set.subset_sInter
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
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 : Set A
⊢ ⋂₀ {F : Set A | s ⊆ F} = s

Tactic:
exact subset_antisymm (sInter_subset_of_mem <| subset_refl s) (subset_sInter fun _ ↦ id)

Premises used: id, subset_antisymm, subset_refl, Set.sInter_subset_of_mem, Set.subset_sInter
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
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 : Set A
simp_rw : (matroid R A).closure s = (matroid R A).E ∧ s ⊆ (matroid R A).E ↔ s = univ
simp_rw₁ : s = (matroid R A).E ∧ s ⊆ (matroid R A).E ↔ s = univ
simp_rw₂ : s = univ ∧ s ⊆ univ ↔ s = univ
simp_rw₃ : s = univ ∧ True ↔ s = univ
⊢ (matroid R A).Spanning s ↔ s = univ

Tactic:
simp_rw [Matroid.spanning_iff, matroid_closure_of_subsingleton, matroid_e, subset_univ, and_true]

Premises used: and_true, Set.subset_univ, Matroid.spanning_iff, AlgebraicIndependent.matroid_e, AlgebraicIndependent.matroid_closure_of_subsingleton
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : NoZeroDivisors A
s t : Set A
hst : s ⊆ t
hs : AlgebraicIndepOn R _root_.id s
ht : Algebra.IsAlgebraic (↥(adjoin R t)) A
⊢ Nontrivial.{w} ↥(adjoin R t)

Tactic:
have := ht.nontrivial
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : NoZeroDivisors A
s t : Set A
hst : s ⊆ t
hs : AlgebraicIndepOn R _root_.id s
ht : Algebra.IsAlgebraic (↥(adjoin R t)) A
this : Nontrivial.{w} ↥(adjoin R t)
⊢ Nontrivial A

Tactic:
have := Subtype.val_injective (p := (· ∈ adjoin R t)).nontrivial
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : NoZeroDivisors A
s t : Set A
hst : s ⊆ t
hs : AlgebraicIndepOn R _root_.id s
ht : Algebra.IsAlgebraic (↥(adjoin R t)) A
this_1 : Nontrivial.{w} ↥(adjoin R t)
this : Nontrivial A
⊢ IsDomain A

Tactic:
have := (isDomain_iff_noZeroDivisors_and_nontrivial A).mpr ⟨inferInstance, inferInstance⟩
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : NoZeroDivisors A
s t : Set A
hst : s ⊆ t
hs : AlgebraicIndepOn R _root_.id s
ht : Algebra.IsAlgebraic (↥(adjoin R t)) A
this_1 : Nontrivial.{w} ↥(adjoin R t)
this_2 : Nontrivial A
this : IsDomain A
⊢ FaithfulSMul R A

Tactic:
have := (faithfulSMul_iff_algebraMap_injective R A).mpr hs.algebraMap_injective