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 : 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_3 : IsDomain A
this : FaithfulSMul R A
⊢ (matroid R A).Spanning t

Tactic:
rw [← matroid_spanning_iff] at ht

Premises used: AlgebraicIndependent.matroid_spanning_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 : NoZeroDivisors A
s t : Set A
hst : s ⊆ t
hs : AlgebraicIndepOn R _root_.id s
this_1 : Nontrivial.{w} ↥(adjoin R t)
this_2 : Nontrivial A
this_3 : IsDomain A
this : FaithfulSMul R A
ht : (matroid R A).Spanning t
⊢ (matroid R A).Indep s

Tactic:
rw [← matroid_indep_iff] at hs

Premises used: AlgebraicIndependent.matroid_indep_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 : NoZeroDivisors A
s t : Set A
hst : s ⊆ t
hs : AlgebraicIndepOn R _root_.id s
this_1 : Nontrivial.{w} ↥(adjoin R t)
this_2 : Nontrivial A
this_3 : IsDomain A
this : FaithfulSMul R A
ht : (matroid R A).Spanning t
hs₁ : (matroid R A).Indep s
⊢ (matroid R A).Spanning t

Tactic:
rw [← matroid_indep_iff] at hs

Premises used: AlgebraicIndependent.matroid_indep_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 : NoZeroDivisors A
s t : Set A
hst : s ⊆ t
this_1 : Nontrivial.{w} ↥(adjoin R t)
this_2 : Nontrivial A
this_3 : IsDomain A
this : FaithfulSMul R A
hs : (matroid R A).Indep s
ht : (matroid R A).Spanning t
have :
  ∀ (B : Set A) (base : (matroid R A).IsBase B) (hsB : s ⊆ B) (hBt : B ⊆ t),
    ∃ (u : Set A),
      s ⊆ u ∧
        u ⊆ t ∧ IsTranscendenceBasis.{w, u_1, w} (ι := { x : A // x ∈ u }) R (Subtype.val (p := fun (x : A) ↦ x ∈ u))
⊢ ∃ (u : Set A),
    s ⊆ u ∧
      u ⊆ t ∧ IsTranscendenceBasis.{w, u_1, w} (ι := { x : A // x ∈ u }) R (Subtype.val (p := fun (x : A) ↦ x ∈ u))

Tactic:
have ⟨B, base, hsB, hBt⟩ := hs.exists_isBase_subset_spanning ht hst
-- 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
this_1 : Nontrivial.{w} ↥(adjoin R t)
this_2 : Nontrivial A
this_3 : IsDomain A
this : FaithfulSMul R A
hs : (matroid R A).Indep s
ht : (matroid R A).Spanning t
B : Set A
base : (matroid R A).IsBase B
hsB : s ⊆ B
hBt : B ⊆ t
⊢ ∃ (u : Set A),
    s ⊆ u ∧
      u ⊆ t ∧ IsTranscendenceBasis.{w, u_1, w} (ι := { x : A // x ∈ u }) R (Subtype.val (p := fun (x : A) ↦ x ∈ u))

Tactic:
⟨B, hsB, hBt, base⟩

Premises used: And.intro, Exists.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 : NoZeroDivisors A
s t : Set A
hst : s ⊆ t
this_1 : Nontrivial.{w} ↥(adjoin R t)
this_2 : Nontrivial A
this_3 : IsDomain A
this : FaithfulSMul R A
hs : (matroid R A).Indep s
ht : (matroid R A).Spanning t
B : Set A
base : (matroid R A).IsBase B
hsB : s ⊆ B
hBt : B ⊆ t
⊢ ∃ (u : Set A),
    s ⊆ u ∧
      u ⊆ t ∧ IsTranscendenceBasis.{w, u_1, w} (ι := { x : A // x ∈ u }) R (Subtype.val (p := fun (x : A) ↦ x ∈ u))

Tactic:
exact ⟨B, hsB, hBt, base⟩
-- 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
inst_4 : FaithfulSMul R A
s : Set A
inst_5 : Algebra.IsAlgebraic (↥(adjoin R s)) A
have :
  ∀ (t : Set A),
    ∅ ⊆ t →
      ∀
        (ht :
          t ⊆ s ∧
            IsTranscendenceBasis.{w, u_1, w} (ι := { x : A // x ∈ t }) R (Subtype.val (p := fun (x : A) ↦ x ∈ t))),
        ∃ t ⊆ s, IsTranscendenceBasis.{w, u_1, w} (ι := { x : A // x ∈ t }) R (Subtype.val (p := fun (x : A) ↦ x ∈ t))
⊢ ∃ t ⊆ s, IsTranscendenceBasis.{w, u_1, w} (ι := { x : A // x ∈ t }) R (Subtype.val (p := fun (x : A) ↦ x ∈ t))

Tactic:
have ⟨t, _, ht⟩ := exists_isTranscendenceBasis_between ∅ s (empty_subset _)
    ((algebraicIndependent_empty_iff ..).mpr <| FaithfulSMul.algebraMap_injective R A)
-- 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
inst_4 : FaithfulSMul R A
s : Set A
inst_5 : Algebra.IsAlgebraic (↥(adjoin R s)) A
t : Set A
left : ∅ ⊆ t
ht : t ⊆ s ∧ IsTranscendenceBasis.{w, u_1, w} (ι := { x : A // x ∈ t }) R (Subtype.val (p := fun (x : A) ↦ x ∈ t))
⊢ ∃ t ⊆ s, IsTranscendenceBasis.{w, u_1, w} (ι := { x : A // x ∈ t }) R (Subtype.val (p := fun (x : A) ↦ x ∈ t))

Tactic:
⟨t, ht⟩

Premises used: Exists.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 : NoZeroDivisors A
inst_4 : FaithfulSMul R A
s : Set A
inst_5 : Algebra.IsAlgebraic (↥(adjoin R s)) A
t : Set A
left : ∅ ⊆ t
ht : t ⊆ s ∧ IsTranscendenceBasis.{w, u_1, w} (ι := { x : A // x ∈ t }) R (Subtype.val (p := fun (x : A) ↦ x ∈ t))
⊢ ∃ t ⊆ s, IsTranscendenceBasis.{w, u_1, w} (ι := { x : A // x ∈ t }) R (Subtype.val (p := fun (x : A) ↦ x ∈ t))

Tactic:
exact ⟨t, ht⟩
-- 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 : IsDomain A
inst_4 : FaithfulSMul R A
s : Set A
simp_rw : (matroid R A).Spanning s ↔ ∃ (t : Set A), (matroid R A).IsBase t ∧ t ⊆ s
⊢ Algebra.IsAlgebraic (↥(adjoin R s)) A ↔
    ∃ t ⊆ s, IsTranscendenceBasis.{w, u_1, w} (ι := { x : A // x ∈ t }) R (Subtype.val (p := fun (x : A) ↦ x ∈ t))

Tactic:
simp_rw [← matroid_spanning_iff, ← matroid_isBase_iff, and_comm (a := _ ⊆ _)]

Premises used: AlgebraicIndependent.matroid_spanning_iff, and_comm, AlgebraicIndependent.matroid_isBase_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 : IsDomain A
inst_4 : FaithfulSMul R A
s : Set A
⊢ (matroid R A).Spanning s ↔ ∃ (t : Set A), (matroid R A).IsBase t ∧ t ⊆ s

Tactic:
Matroid.spanning_iff_exists_isBase_subset (subset_univ _)

Premises used: Matroid.spanning_iff_exists_isBase_subset, Set.subset_univ
-- 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 : IsDomain A
inst_4 : FaithfulSMul R A
s : Set A
⊢ (matroid R A).Spanning s ↔ ∃ (t : Set A), (matroid R A).IsBase t ∧ t ⊆ s

Tactic:
exact Matroid.spanning_iff_exists_isBase_subset (subset_univ _)

Premises used: Matroid.spanning_iff_exists_isBase_subset
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
inst_4 : NoZeroDivisors A
hx : IsTranscendenceBasis R x
⊢ FaithfulSMul R A

Tactic:
have := (faithfulSMul_iff_algebraMap_injective R A).mpr hx.1.algebraMap_injective
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
inst_4 : NoZeroDivisors A
hx : IsTranscendenceBasis R x
this : FaithfulSMul R A
rw : lift.{w, u} #ι = lift.{u, w} (matroid R A).cRank
rw₁ : lift.{w, u} #ι = lift.{u, w} #(↑(range x) : Type w)
rw₂ rw₃ : lift.{u, w} #(↑(range x) : Type w) = lift.{u, w} #(↑(range x) : Type w)
⊢ lift.{w, u} #ι = lift.{u, w} (trdeg R A)

Tactic:
rw [← matroid_cRank_eq, ← (matroid_isBase_iff.mpr hx.to_subtype_range).cardinalMk_eq_cRank,
    lift_mk_eq'.mpr ⟨.ofInjective _ hx.1.injective⟩]

Premises used: Iff.mpr, AlgebraicIndependent.matroid_cRank_eq, Matroid.IsBase.cardinalMk_eq_cRank, Cardinal.lift_mk_eq', Nonempty.intro, AlgebraicIndependent.matroid_isBase_iff, Equiv.ofInjective, And.left, IsTranscendenceBasis.to_subtype_range, AlgebraicIndependent.injective
-- 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 : Nontrivial R
inst_4 : NoZeroDivisors A
ι : Type w
x : ι → A
hx : IsTranscendenceBasis R x
rw : lift.{w, w} #ι = trdeg R A
rw₁ : lift.{w, w} (trdeg R A) = trdeg R A
rw₂ rw₃ : trdeg R A = trdeg R A
⊢ #ι = trdeg R A

Tactic:
rw [← lift_id #ι, lift_cardinalMk_eq_trdeg hx, lift_id]

Premises used: Cardinal.mk, IsTranscendenceBasis.lift_cardinalMk_eq_trdeg, Cardinal.lift_id
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
ι' : Type u'
R : Type u_1
A : Type w
x : ι → A
y : ι' → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
inst_4 : NoZeroDivisors A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis R y
rw : lift.{w, max u u'} (lift.{u', u} #ι) = lift.{w, max u u'} (lift.{u, u'} #ι')
rw₁ : lift.{max u' w, u} #ι = lift.{w, max u u'} (lift.{u, u'} #ι')
rw₂ : lift.{max u' w, u} #ι = lift.{max u w, u'} #ι'
rw₃ : lift.{u', max w u} (lift.{w, u} #ι) = lift.{max u w, u'} #ι'
rw₄ : lift.{u', max w u} (lift.{u, w} (trdeg R A)) = lift.{max u w, u'} #ι'
rw₅ : lift.{u', max w u} (lift.{u, w} (trdeg R A)) = lift.{u, max w u'} (lift.{w, u'} #ι')
rw₆ : lift.{u', max w u} (lift.{u, w} (trdeg R A)) = lift.{u, max w u'} (lift.{u', w} (trdeg R A))
rw₇ : lift.{max u u', w} (trdeg R A) = lift.{u, max w u'} (lift.{u', w} (trdeg R A))
rw₈ rw₉ : lift.{max u u', w} (trdeg R A) = lift.{max u' u, w} (trdeg R A)
⊢ lift.{u', u} #ι = lift.{u, u'} #ι'

Tactic:
rw [← lift_inj.{_, w}, lift_lift, lift_lift, ← lift_lift.{w, u'}, hx.lift_cardinalMk_eq_trdeg,
    ← lift_lift.{w, u}, hy.lift_cardinalMk_eq_trdeg, lift_lift, lift_lift]

Premises used: Cardinal.lift_lift, IsTranscendenceBasis.lift_cardinalMk_eq_trdeg
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
inst_4 : NoZeroDivisors A
ι' : Type u
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis R y
rw : lift.{u, u} #ι = #ι'
rw₁ : lift.{u, u} #ι' = #ι'
rw₂ rw₃ : #ι' = #ι'
⊢ #ι = #ι'

Tactic:
rw [← lift_id #ι, lift_cardinalMk_eq hx hy, lift_id]

Premises used: Cardinal.mk, IsTranscendenceBasis.lift_cardinalMk_eq, Cardinal.lift_id
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
S : Type v
inst : CommRing S
inst_1 : IsDomain S
⊢ lift.{u, max u v} (trdeg S (MvPolynomial ι S)) = lift.{max u v, u} #ι

Tactic:
have := (IsTranscendenceBasis.mvPolynomial ι S).lift_cardinalMk_eq_trdeg.symm
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
S : Type v
inst : CommRing S
inst_1 : IsDomain S
this : lift.{u, max u v} (trdeg S (MvPolynomial ι S)) = lift.{max u v, u} #ι
rwa : ∀ (this : trdeg S (MvPolynomial ι S) = lift.{max u v, u} #ι), trdeg S (MvPolynomial ι S) = lift.{v, u} #ι
rwa₁ : ∀ (this : trdeg S (MvPolynomial ι S) = lift.{v, u} (lift.{u, u} #ι)), trdeg S (MvPolynomial ι S) = lift.{v, u} #ι
rwa₂ rwa₃ rwa₄ rwa₅ :
  ∀ (this : trdeg S (MvPolynomial ι S) = lift.{v, u} #ι), trdeg S (MvPolynomial ι S) = lift.{v, u} #ι
⊢ trdeg S (MvPolynomial ι S) = lift.{v, u} #ι

Tactic:
rwa [lift_id', ← lift_lift.{u}, lift_id] at this

Premises used: Cardinal.lift_id', Cardinal.lift_id
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
⊢ trdeg R R[X] = 1

Tactic:
simpa using (IsTranscendenceBasis.polynomial Unit R).lift_cardinalMk_eq_trdeg.symm

Premises used: IsTranscendenceBasis.lift_cardinalMk_eq_trdeg, Unit, Eq.symm, IsTranscendenceBasis.polynomial
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
R : Type u_1
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain R
fin : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
surj : Surjective.{u_1 + 1, v + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
⊢ lift.{v, u_1} (trdeg R (MvPolynomial (Fin n) R)) < lift.{u_1, v} ℵ₀

Tactic:
simp
-- 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
s : Set A
inst_3 : NoZeroDivisors A
inst_4 : Algebra.IsAlgebraic (↥(adjoin R s)) A
⊢ IsDomain A

Tactic:
have := Algebra.IsAlgebraic.nontrivial (adjoin R s) A
  (isDomain_iff_noZeroDivisors_and_nontrivial _).mpr
    ⟨‹_›, (Subtype.val_injective (p := (· ∈ adjoin R s))).nontrivial⟩

Premises used: Iff.mpr, Subtype.val_injective, Function.Injective.nontrivial, Algebra.adjoin, Membership.mem, Subtype, Algebra.IsAlgebraic.nontrivial, And.intro, isDomain_iff_noZeroDivisors_and_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
s : Set A
inst_3 : NoZeroDivisors A
alg : Algebra.IsAlgebraic (↥(adjoin R s)) A
pos : ∀ (h : Injective.{u_1 + 1, w + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)), trdeg R A ≤ #(↑s : Type w)
neg :
  ∀ (h : ¬Injective.{u_1 + 1, w + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)), trdeg R A ≤ #(↑s : Type w)
⊢ trdeg R A ≤ #(↑s : Type w)

Tactic:
by_cases h : Injective (algebraMap R A)

Premises used: Algebra.algebraMap, Function.Injective, DFunLike.coe
-- 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
s : Set A
inst_3 : NoZeroDivisors A
alg : Algebra.IsAlgebraic (↥(adjoin R s)) A
h : ¬Injective.{u_1 + 1, w + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
⊢ trdeg R A ≤ #(↑s : Type w)

Tactic:
simp [trdeg_eq_zero_of_not_injective h]

Premises used: trdeg_eq_zero_of_not_injective
-- 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
s : Set A
inst_3 : NoZeroDivisors A
alg : Algebra.IsAlgebraic (↥(adjoin R s)) A
h : ¬Injective.{u_1 + 1, w + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
⊢ trdeg R A ≤ #(↑s : Type w)

Tactic:
on_goal 2 => simp [trdeg_eq_zero_of_not_injective h]

Premises used: trdeg_eq_zero_of_not_injective
-- 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
s : Set A
inst_3 : NoZeroDivisors A
alg : Algebra.IsAlgebraic (↥(adjoin R s)) A
h : Injective.{u_1 + 1, w + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
⊢ IsDomain A

Tactic:
have := isDomain_of_adjoin_range R 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
s : Set A
inst_3 : NoZeroDivisors A
alg : Algebra.IsAlgebraic (↥(adjoin R s)) A
h : Injective.{u_1 + 1, w + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
this : IsDomain A
⊢ FaithfulSMul R A

Tactic:
have := (faithfulSMul_iff_algebraMap_injective R A).mpr h
-- 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
s : Set A
inst_3 : NoZeroDivisors A
alg : Algebra.IsAlgebraic (↥(adjoin R s)) A
h : Injective.{u_1 + 1, w + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
this_1 : IsDomain A
this : FaithfulSMul R A
pos : ∀ (alg : (matroid R A).Spanning s), (matroid R A).cRank ≤ #(↑s : Type w)
⊢ trdeg R A ≤ #(↑s : Type w)

Tactic:
rw [← matroid_spanning_iff, ← matroid_cRank_eq] at *

Premises used: AlgebraicIndependent.matroid_spanning_iff, AlgebraicIndependent.matroid_cRank_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
s : Set A
inst_3 : NoZeroDivisors A
h : Injective.{u_1 + 1, w + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
this_1 : IsDomain A
this : FaithfulSMul R A
alg : (matroid R A).Spanning s
⊢ (matroid R A).cRank ≤ #(↑s : Type w)

Tactic:
alg.cRank_le_cardinalMk

Premises used: Matroid.Spanning.cRank_le_cardinalMk
-- 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
s : Set A
inst_3 : NoZeroDivisors A
h : Injective.{u_1 + 1, w + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
this_1 : IsDomain A
this : FaithfulSMul R A
alg : (matroid R A).Spanning s
⊢ (matroid R A).cRank ≤ #(↑s : Type w)

Tactic:
exact alg.cRank_le_cardinalMk

Premises used: Matroid.Spanning.cRank_le_cardinalMk
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : NoZeroDivisors A
inst_4 : FaithfulSMul R A
inst_5 : Finite ι
alg : Algebra.IsAlgebraic (↥(adjoin R (range x))) A
le : lift.{w, u} #ι ≤ lift.{u, w} (trdeg R A)
have : ∀ (toFun : ι → (↑(range x) : Type w)) (h : Injective toFun), IsTranscendenceBasis R x
⊢ IsTranscendenceBasis R x

Tactic:
have ⟨_, h⟩ := lift_mk_le'.mp (le.trans <| lift_le.mpr <| trdeg_le_cardinalMk R (range x))
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : NoZeroDivisors A
inst_4 : FaithfulSMul R A
inst_5 : Finite ι
alg : Algebra.IsAlgebraic (↥(adjoin R (range x))) A
le : lift.{w, u} #ι ≤ lift.{u, w} (trdeg R A)
toFun : ι → (↑(range x) : Type w)
h : Injective toFun
⊢ Bijective (rangeFactorization x)

Tactic:
have := rangeFactorization_surjective.bijective_of_nat_card_le (Nat.card_le_card_of_injective _ h)
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : NoZeroDivisors A
inst_4 : FaithfulSMul R A
inst_5 : Finite ι
alg : Algebra.IsAlgebraic (↥(adjoin R (range x))) A
le : lift.{w, u} #ι ≤ lift.{u, w} (trdeg R A)
toFun : ι → (↑(range x) : Type w)
h : Injective toFun
this : Bijective (rangeFactorization x)
⊢ IsTranscendenceBasis R x

Tactic:
.of_subtype_range (fun _ _ ↦ (this.1 <| Subtype.ext ·)) ?_

Premises used: IsTranscendenceBasis.of_subtype_range, And.left, Subtype.ext
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : NoZeroDivisors A
inst_4 : FaithfulSMul R A
inst_5 : Finite ι
alg : Algebra.IsAlgebraic (↥(adjoin R (range x))) A
le : lift.{w, u} #ι ≤ lift.{u, w} (trdeg R A)
toFun : ι → (↑(range x) : Type w)
h : Injective toFun
this : Bijective (rangeFactorization x)
refine :
  IsTranscendenceBasis.{w, u_1, w} (ι := { x_1 : A // x_1 ∈ range x }) R
    (Subtype.val (p := fun (x_1 : A) ↦ x_1 ∈ range x))
⊢ IsTranscendenceBasis R x

Tactic:
refine .of_subtype_range (fun _ _ ↦ (this.1 <| Subtype.ext ·)) ?_
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : NoZeroDivisors A
inst_4 : FaithfulSMul R A
inst_5 : Finite ι
alg : Algebra.IsAlgebraic (↥(adjoin R (range x))) A
le : lift.{w, u} #ι ≤ lift.{u, w} (trdeg R A)
toFun : ι → (↑(range x) : Type w)
h : Injective toFun
this : Bijective (rangeFactorization x)
⊢ IsDomain A

Tactic:
have := isDomain_of_adjoin_range R (range x)
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : NoZeroDivisors A
inst_4 : FaithfulSMul R A
inst_5 : Finite ι
alg : Algebra.IsAlgebraic (↥(adjoin R (range x))) A
le : lift.{w, u} #ι ≤ lift.{u, w} (trdeg R A)
toFun : ι → (↑(range x) : Type w)
h : Injective toFun
this_1 : Bijective (rangeFactorization x)
this : IsDomain A
rw :
  ∀ (le : lift.{w, u} #ι ≤ lift.{u, w} (matroid R A).cRank) (toFun : ι → (↑(range x) : Type w)) (h : Injective toFun)
    (this : Bijective (rangeFactorization x)) (this : IsDomain A) (alg : (matroid R A).Spanning (range x)),
    IsTranscendenceBasis.{w, u_1, w} (ι := { x_1 : A // x_1 ∈ range x }) R
      (Subtype.val (p := fun (x_1 : A) ↦ x_1 ∈ range x))
⊢ IsTranscendenceBasis.{w, u_1, w} (ι := { x_1 : A // x_1 ∈ range x }) R
    (Subtype.val (p := fun (x_1 : A) ↦ x_1 ∈ range x))

Tactic:
rw [← matroid_spanning_iff, ← matroid_cRank_eq] at *

Premises used: AlgebraicIndependent.matroid_spanning_iff, AlgebraicIndependent.matroid_cRank_eq
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : NoZeroDivisors A
inst_4 : FaithfulSMul R A
inst_5 : Finite ι
le : lift.{w, u} #ι ≤ lift.{u, w} (matroid R A).cRank
toFun : ι → (↑(range x) : Type w)
h : Injective toFun
this_1 : Bijective (rangeFactorization x)
this : IsDomain A
alg : (matroid R A).Spanning (range x)
⊢ IsTranscendenceBasis.{w, u_1, w} (ι := { x_1 : A // x_1 ∈ range x }) R
    (Subtype.val (p := fun (x_1 : A) ↦ x_1 ∈ range x))

Tactic:
alg.isBase_of_le_cRank_of_finite (lift_le.mp <| mk_range_le_lift.trans le) (finite_range x)

Premises used: Set.finite_range, IsTranscendenceBasis, Iff.mp, LE.le.trans, Matroid.Spanning.isBase_of_le_cRank_of_finite, Cardinal.mk_range_le_lift, Cardinal.lift_le
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : NoZeroDivisors A
inst_4 : FaithfulSMul R A
inst_5 : Finite ι
le : lift.{w, u} #ι ≤ lift.{u, w} (matroid R A).cRank
toFun : ι → (↑(range x) : Type w)
h : Injective toFun
this_1 : Bijective (rangeFactorization x)
this : IsDomain A
alg : (matroid R A).Spanning (range x)
⊢ IsTranscendenceBasis.{w, u_1, w} (ι := { x_1 : A // x_1 ∈ range x }) R
    (Subtype.val (p := fun (x_1 : A) ↦ x_1 ∈ range x))

Tactic:
exact alg.isBase_of_le_cRank_of_finite (lift_le.mp <| mk_range_le_lift.trans le) (finite_range x)

Premises used: Set.finite_range, Iff.mp, LE.le.trans, Matroid.Spanning.isBase_of_le_cRank_of_finite, Cardinal.mk_range_le_lift, Cardinal.lift_le
-- 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
inst_4 : FaithfulSMul R A
ι : Type w
inst_5 : Finite ι
x : ι → A
inst_6 : Algebra.IsAlgebraic (↥(adjoin R (range x))) A
le : #ι ≤ trdeg R A
rwa : #ι ≤ lift.{w, w} (trdeg R A)
rwa₁ rwa₂ rwa₃ rwa₄ : #ι ≤ trdeg R A
⊢ lift.{w, w} #ι ≤ lift.{w, w} (trdeg R A)

Tactic:
rwa [lift_id, lift_id]

Premises used: Cardinal.lift_id
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : NoZeroDivisors A
inst_4 : FaithfulSMul R A
inst_5 : Algebra.IsAlgebraic (↥(adjoin R (range x))) A
fin : trdeg R A < ℵ₀
le : lift.{w, u} #ι ≤ lift.{u, w} (trdeg R A)
⊢ lift.{u, w} ℵ₀ = lift.{w, u} ℵ₀

Tactic:
simp
-- 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
inst_4 : FaithfulSMul R A
ι : Type w
x : ι → A
inst_5 : Algebra.IsAlgebraic (↥(adjoin R (range x))) A
fin : trdeg R A < ℵ₀
le : #ι ≤ trdeg R A
rwa : #ι ≤ lift.{w, w} (trdeg R A)
rwa₁ rwa₂ rwa₃ rwa₄ : #ι ≤ trdeg R A
⊢ lift.{w, w} #ι ≤ lift.{w, w} (trdeg R A)

Tactic:
rwa [lift_id, lift_id]

Premises used: Cardinal.lift_id