awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
simp_rw₃ : (matroid R A).closure s = univ ↔ Algebra.IsAlgebraic (↥(adjoin R s)) A
⊢ (matroid R A).Spanning s ↔ Algebra.IsAlgebraic (↥(adjoin R s)) A
have simp_rw₄ : (∀ (x : A), x ∈ (matroid R A).closure 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]
-- 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
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
⊢ (matroid R A).Spanning s ↔ Algebra.IsAlgebraic (↥(adjoin R s)) A
have simp_rw₅ : (∀ (x : A), x ∈ (↑(algebraicClosure (↥(adjoin R s)) A) : Set A)) ↔ 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
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
⊢ (matroid R A).Spanning s ↔ Algebra.IsAlgebraic (↥(adjoin R s)) A
have simp_rw₆ : (∀ (x : A), Membership.mem (γ := Subalgebra (↥(adjoin R s)) A) (algebraicClosure (↥(adjoin R s)) A) x) ↔
  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
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
⊢ (matroid R A).Spanning s ↔ Algebra.IsAlgebraic (↥(adjoin R s)) A
have simp_rw₇ : (∀ (x : A), IsAlgebraic (↥(adjoin R s)) x) ↔ 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 : Subsingleton A
s : Set A
⊢ (matroid R A).IsFlat s
have simp_rw : ∀ ⦃I X : Set A⦄, I = s → I = X → X ⊆ s
Tactic: simp_rw [Matroid.isFlat_iff, matroid_e, subset_univ,
    and_true, matroid_isBasis_iff_of_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 : Set A
⊢ (matroid R A).closure s = s
have simp_rw : ⋂₀ {F : Set A | s ⊆ F} = s
Tactic: simp_rw [Matroid.closure, matroid_isFlat_of_subsingleton, true_and, matroid_e, inter_univ]
-- 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 : Set A
⊢ (matroid R A).Spanning s ↔ s = univ
have simp_rw : (matroid R A).closure s = (matroid R A).E ∧ s ⊆ (matroid R A).E ↔ s = univ
Tactic: simp_rw [Matroid.spanning_iff, matroid_closure_of_subsingleton, 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 : Subsingleton A
s : Set A
simp_rw : (matroid R A).closure s = (matroid R A).E ∧ s ⊆ (matroid R A).E ↔ s = univ
⊢ (matroid R A).Spanning s ↔ s = univ
have simp_rw₁ : s = (matroid R A).E ∧ s ⊆ (matroid R A).E ↔ s = univ
Tactic: simp_rw [Matroid.spanning_iff, matroid_closure_of_subsingleton, 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 : 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
⊢ (matroid R A).Spanning s ↔ s = univ
have simp_rw₂ : s = univ ∧ s ⊆ univ ↔ s = univ
Tactic: simp_rw [Matroid.spanning_iff, matroid_closure_of_subsingleton, 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 : 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
⊢ (matroid R A).Spanning s ↔ s = univ
have simp_rw₃ : s = univ ∧ True ↔ s = univ
Tactic: simp_rw [Matroid.spanning_iff, matroid_closure_of_subsingleton, matroid_e, subset_univ, and_true]
-- 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 : NoZeroDivisors A
s t : Set A
hst : s ⊆ t
hs : AlgebraicIndepOn R _root_.id s
ht : Algebra.IsAlgebraic (↥(adjoin R t)) A
⊢ ∃ (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))
have this : Nontrivial.{w} ↥(adjoin R t)
Tactic: have := ht.nontrivial
-- 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 : 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)
⊢ ∃ (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))
have this₁ : Nontrivial A
Tactic: have := Subtype.val_injective (p := (· ∈ adjoin R t)).nontrivial
-- 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 : 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
⊢ ∃ (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))
have this₁ : IsDomain A
Tactic: have := (isDomain_iff_noZeroDivisors_and_nontrivial A).mpr ⟨inferInstance, inferInstance⟩
-- 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 : 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
⊢ ∃ (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))
have this₁ : FaithfulSMul R A
Tactic: have := (faithfulSMul_iff_algebraMap_injective R A).mpr hs.algebraMap_injective
-- 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 : 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
⊢ ∃ (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))
have ht₁ : (matroid R A).Spanning t
Tactic: rw [← matroid_spanning_iff] at ht
Cleared hypotheses: ht
-- 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 : 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
⊢ ∃ (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))
have hs₁ : (matroid R A).Indep s
Tactic: rw [← matroid_indep_iff] at hs
Cleared hypotheses: hs, ht
-- 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 : 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
⊢ ∃ (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))
have 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))
Tactic: have ⟨B, base, hsB, hBt⟩ := hs.exists_isBase_subset_spanning ht hst
-- 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 : NoZeroDivisors A
inst_4 : FaithfulSMul R A
s : Set A
inst_5 : 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))
have 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))
Tactic: have ⟨t, _, ht⟩ := exists_isTranscendenceBasis_between ∅ s (empty_subset _)
    ((algebraicIndependent_empty_iff ..).mpr <| FaithfulSMul.algebraMap_injective R 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 : IsDomain A
inst_4 : FaithfulSMul R A
s : Set A
⊢ 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))
have simp_rw : (matroid R A).Spanning s ↔ ∃ (t : Set A), (matroid R A).IsBase t ∧ t ⊆ s
Tactic: simp_rw [← matroid_spanning_iff, ← matroid_isBase_iff, and_comm (a := _ ⊆ _)]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (hypothesis)
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
⊢ lift.{w, u} #ι = lift.{u, w} (trdeg R A)
have this : FaithfulSMul R A
Tactic: have := (faithfulSMul_iff_algebraMap_injective R A).mpr hx.1.algebraMap_injective
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
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
⊢ lift.{w, u} #ι = lift.{u, w} (trdeg R A)
have rw : lift.{w, u} #ι = lift.{u, w} (matroid R A).cRank
Tactic: rw [← matroid_cRank_eq, ← (matroid_isBase_iff.mpr hx.to_subtype_range).cardinalMk_eq_cRank,
    lift_mk_eq'.mpr ⟨.ofInjective _ hx.1.injective⟩]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
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
⊢ lift.{w, u} #ι = lift.{u, w} (trdeg R A)
have rw₁ : lift.{w, u} #ι = lift.{u, w} #(↑(range x) : Type w)
Tactic: rw [← matroid_cRank_eq, ← (matroid_isBase_iff.mpr hx.to_subtype_range).cardinalMk_eq_cRank,
    lift_mk_eq'.mpr ⟨.ofInjective _ hx.1.injective⟩]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
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)
⊢ lift.{w, u} #ι = lift.{u, w} (trdeg R A)
have rw₂ : lift.{u, w} #(↑(range x) : Type w) = lift.{u, w} #(↑(range x) : Type w)
Tactic: rw [← matroid_cRank_eq, ← (matroid_isBase_iff.mpr hx.to_subtype_range).cardinalMk_eq_cRank,
    lift_mk_eq'.mpr ⟨.ofInjective _ hx.1.injective⟩]
-- 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 : Nontrivial R
inst_4 : NoZeroDivisors A
ι : Type w
x : ι → A
hx : IsTranscendenceBasis R x
⊢ #ι = trdeg R A
have rw : lift.{w, w} #ι = trdeg R A
Tactic: rw [← lift_id #ι, lift_cardinalMk_eq_trdeg hx, lift_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 : Nontrivial R
inst_4 : NoZeroDivisors A
ι : Type w
x : ι → A
hx : IsTranscendenceBasis R x
rw : lift.{w, w} #ι = trdeg R A
⊢ #ι = trdeg R A
have rw₁ : lift.{w, w} (trdeg R A) = trdeg R A
Tactic: rw [← lift_id #ι, lift_cardinalMk_eq_trdeg hx, lift_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 : 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
⊢ #ι = trdeg R A
have rw₂ : trdeg R A = trdeg R A
Tactic: rw [← lift_id #ι, lift_cardinalMk_eq_trdeg hx, lift_id]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
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
⊢ lift.{u', u} #ι = lift.{u, u'} #ι'
have rw : lift.{w, max u u'} (lift.{u', u} #ι) = lift.{w, max 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]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
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'} #ι')
⊢ lift.{u', u} #ι = lift.{u, u'} #ι'
have rw₁ : lift.{max u' w, u} #ι = lift.{w, max 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]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
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'} #ι')
⊢ lift.{u', u} #ι = lift.{u, u'} #ι'
have rw₂ : lift.{max u' w, u} #ι = lift.{max u w, 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]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
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'} #ι'
⊢ lift.{u', u} #ι = lift.{u, u'} #ι'
have rw₃ : lift.{u', max w u} (lift.{w, u} #ι) = lift.{max u w, 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]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
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'} #ι'
⊢ lift.{u', u} #ι = lift.{u, u'} #ι'
have rw₄ : lift.{u', max w u} (lift.{u, w} (trdeg R A)) = lift.{max u w, 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]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
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'} #ι'
⊢ lift.{u', u} #ι = lift.{u, u'} #ι'
have rw₅ : lift.{u', max w u} (lift.{u, w} (trdeg R A)) = lift.{u, max w u'} (lift.{w, 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]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
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'} #ι')
⊢ lift.{u', u} #ι = lift.{u, u'} #ι'
have rw₆ : lift.{u', max w u} (lift.{u, w} (trdeg R A)) = lift.{u, max w u'} (lift.{u', w} (trdeg R A))
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]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
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))
⊢ lift.{u', u} #ι = lift.{u, u'} #ι'
have rw₇ : lift.{max u u', w} (trdeg R A) = lift.{u, max w u'} (lift.{u', w} (trdeg R A))
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]