awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
rw₇ : lift.{max u 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.{max u' 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
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
⊢ #ι = #ι'
have rw : lift.{u, u} #ι = #ι'
Tactic: rw [← lift_id #ι, lift_cardinalMk_eq hx hy, lift_id]
-- 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
ι' : Type u
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis R y
rw : lift.{u, u} #ι = #ι'
⊢ #ι = #ι'
have rw₁ : lift.{u, u} #ι' = #ι'
Tactic: rw [← lift_id #ι, lift_cardinalMk_eq hx hy, lift_id]
-- 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
ι' : Type u
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis R y
rw : lift.{u, u} #ι = #ι'
rw₁ : lift.{u, u} #ι' = #ι'
⊢ #ι = #ι'
have rw₂ : #ι' = #ι'
Tactic: rw [← lift_id #ι, lift_cardinalMk_eq hx hy, lift_id]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (hypothesis)
Goal:
ι : Type u
S : Type v
inst : CommRing S
inst_1 : IsDomain S
⊢ trdeg S (MvPolynomial ι S) = lift.{v, u} #ι
have this : lift.{u, max u v} (trdeg S (MvPolynomial ι S)) = lift.{max u v, u} #ι
Tactic: have := (IsTranscendenceBasis.mvPolynomial ι S).lift_cardinalMk_eq_trdeg.symm
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
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} #ι
⊢ trdeg S (MvPolynomial ι S) = lift.{v, u} #ι
have rwa : ∀ (this : trdeg S (MvPolynomial ι S) = lift.{max u v, u} #ι), trdeg S (MvPolynomial ι S) = lift.{v, u} #ι
Tactic: rwa [lift_id', ← lift_lift.{u}, lift_id] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
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} #ι
⊢ trdeg S (MvPolynomial ι S) = lift.{v, u} #ι
have rwa₁ : ∀ (this : trdeg S (MvPolynomial ι S) = lift.{v, u} (lift.{u, u} #ι)), trdeg S (MvPolynomial ι S) = lift.{v, u} #ι
Tactic: rwa [lift_id', ← lift_lift.{u}, lift_id] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
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} #ι
⊢ trdeg S (MvPolynomial ι S) = lift.{v, u} #ι
have rwa₂ : ∀ (this : 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
Cleared hypotheses: this
-- 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
s : Set A
inst_3 : NoZeroDivisors A
alg : Algebra.IsAlgebraic (↥(adjoin R s)) A
⊢ trdeg R A ≤ #(↑s : Type w)
have pos : ∀ (h : Injective.{u_1 + 1, w + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)), trdeg R A ≤ #(↑s : Type w)
Tactic: by_cases h : Injective (algebraMap 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
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)
⊢ trdeg R A ≤ #(↑s : Type w)
have neg : ∀ (h : ¬Injective.{u_1 + 1, w + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)), trdeg R A ≤ #(↑s : Type w)
Tactic: by_cases h : Injective (algebraMap R A)
-- 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
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)
have this : IsDomain A
Tactic: have := isDomain_of_adjoin_range R s
-- 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
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
⊢ trdeg R A ≤ #(↑s : Type w)
have this₁ : FaithfulSMul R A
Tactic: have := (faithfulSMul_iff_algebraMap_injective R A).mpr 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
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
⊢ trdeg R A ≤ #(↑s : Type w)
have pos : ∀ (alg : (matroid R A).Spanning s), (matroid R A).cRank ≤ #(↑s : Type w)
Tactic: rw [← matroid_spanning_iff, ← matroid_cRank_eq] at *
Cleared hypotheses: alg
-- 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 : 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)
⊢ IsTranscendenceBasis R x
have have : ∀ (toFun : ι → (↑(range x) : Type w)) (h : Injective toFun), IsTranscendenceBasis R x
Tactic: have ⟨_, h⟩ := lift_mk_le'.mp (le.trans <| lift_le.mpr <| trdeg_le_cardinalMk R (range x))
-- 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 : 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
⊢ IsTranscendenceBasis R x
have this : Bijective (rangeFactorization x)
Tactic: have := rangeFactorization_surjective.bijective_of_nat_card_le (Nat.card_le_card_of_injective _ h)
-- 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 : 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
have 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))
Tactic: refine .of_subtype_range (fun _ _ ↦ (this.1 <| Subtype.ext ·)) ?_
-- 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 : 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.{w, u_1, w} (ι := { x_1 : A // x_1 ∈ range x }) R
    (Subtype.val (p := fun (x_1 : A) ↦ x_1 ∈ range x))
have this₁ : IsDomain A
Tactic: have := isDomain_of_adjoin_range R (range x)
-- 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 : 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
⊢ IsTranscendenceBasis.{w, u_1, w} (ι := { x_1 : A // x_1 ∈ range x }) R
    (Subtype.val (p := fun (x_1 : A) ↦ x_1 ∈ range x))
have 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))
Tactic: rw [← matroid_spanning_iff, ← matroid_cRank_eq] at *
Cleared hypotheses: alg, le, toFun, h, this_1, this
-- 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
ι : Type w
inst_5 : Finite ι
x : ι → A
inst_6 : Algebra.IsAlgebraic (↥(adjoin R (range x))) A
le : #ι ≤ trdeg R A
⊢ lift.{w, w} #ι ≤ lift.{w, w} (trdeg R A)
have rwa : #ι ≤ lift.{w, w} (trdeg R A)
Tactic: rwa [lift_id, 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 : 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
⊢ lift.{w, w} #ι ≤ lift.{w, w} (trdeg R A)
have rwa : #ι ≤ lift.{w, w} (trdeg R A)
Tactic: rwa [lift_id, lift_id]
-- 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 : AlgebraicIndependent R x
fin : trdeg R A < ℵ₀
le : lift.{u, w} (trdeg R A) ≤ lift.{w, u} #ι
⊢ IsTranscendenceBasis R x
have this : FaithfulSMul R A
Tactic: have := (faithfulSMul_iff_algebraMap_injective R A).mpr hx.algebraMap_injective
-- 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 : AlgebraicIndependent R x
fin : trdeg R A < ℵ₀
le : lift.{u, w} (trdeg R A) ≤ lift.{w, u} #ι
this : FaithfulSMul R A
⊢ IsTranscendenceBasis R x
have fin₁ : (matroid R A).RankFinite
Tactic: rw [← matroid_cRank_eq, ← Matroid.rankFinite_iff_cRank_lt_aleph0] at fin
Cleared hypotheses: fin
-- 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 : AlgebraicIndependent R x
fin : trdeg R A < ℵ₀
le : trdeg R A ≤ #ι
⊢ lift.{w, w} (trdeg R A) ≤ lift.{w, w} #ι
have rwa : trdeg R A ≤ lift.{w, w} #ι
Tactic: rwa [lift_id, 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
inst_5 : Finite ι
x : ι → A
hx : AlgebraicIndependent R x
le : trdeg R A ≤ #ι
⊢ lift.{w, w} (trdeg R A) ≤ lift.{w, w} #ι
have rwa : trdeg R A ≤ lift.{w, w} #ι
Tactic: rwa [lift_id, lift_id]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
R : Type u_1
S : Type v
A : Type w
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 : Nontrivial R
inst_8 : NoZeroDivisors A
inst_9 : FaithfulSMul R S
inst_10 : FaithfulSMul S A
⊢ lift.{w, v} (trdeg R S) + lift.{v, w} (trdeg S A) = lift.{v, w} (trdeg R A)
have have : ∀ (s : Set S)
  (hs : IsTranscendenceBasis.{v, u_1, v} (ι := { x : S // x ∈ s }) R (Subtype.val (p := fun (x : S) ↦ x ∈ s))),
  lift.{w, v} (trdeg R S) + lift.{v, w} (trdeg S A) = lift.{v, w} (trdeg R A)
Tactic: have ⟨s, hs⟩ := exists_isTranscendenceBasis R S
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
R : Type u_1
S : Type v
A : Type w
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 : Nontrivial R
inst_8 : NoZeroDivisors A
inst_9 : FaithfulSMul R S
inst_10 : FaithfulSMul S A
s : Set S
hs : IsTranscendenceBasis.{v, u_1, v} (ι := { x : S // x ∈ s }) R (Subtype.val (p := fun (x : S) ↦ x ∈ s))
⊢ lift.{w, v} (trdeg R S) + lift.{v, w} (trdeg S A) = lift.{v, w} (trdeg R A)
have have : ∀ (t : Set A)
  (ht : IsTranscendenceBasis.{w, v, w} (ι := { x : A // x ∈ t }) S (Subtype.val (p := fun (x : A) ↦ x ∈ t))),
  lift.{w, v} (trdeg R S) + lift.{v, w} (trdeg S A) = lift.{v, w} (trdeg R A)
Tactic: have ⟨t, ht⟩ := exists_isTranscendenceBasis S A
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (hypothesis)
Goal:
R : Type u_1
S : Type v
A : Type w
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 : Nontrivial R
inst_8 : NoZeroDivisors A
inst_9 : FaithfulSMul R S
inst_10 : FaithfulSMul S A
s : Set S
hs : IsTranscendenceBasis.{v, u_1, v} (ι := { x : S // x ∈ s }) R (Subtype.val (p := fun (x : S) ↦ x ∈ s))
t : Set A
ht : IsTranscendenceBasis.{w, v, w} (ι := { x : A // x ∈ t }) S (Subtype.val (p := fun (x : A) ↦ x ∈ t))
⊢ lift.{w, v} (trdeg R S) + lift.{v, w} (trdeg S A) = lift.{v, w} (trdeg R A)
have this : NoZeroDivisors S
Tactic: have := (FaithfulSMul.algebraMap_injective S A).noZeroDivisors _ (map_zero _) (map_mul _)
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (hypothesis)
Goal:
R : Type u_1
S : Type v
A : Type w
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 : Nontrivial R
inst_8 : NoZeroDivisors A
inst_9 : FaithfulSMul R S
inst_10 : FaithfulSMul S A
s : Set S
hs : IsTranscendenceBasis.{v, u_1, v} (ι := { x : S // x ∈ s }) R (Subtype.val (p := fun (x : S) ↦ x ∈ s))
t : Set A
ht : IsTranscendenceBasis.{w, v, w} (ι := { x : A // x ∈ t }) S (Subtype.val (p := fun (x : A) ↦ x ∈ t))
this : NoZeroDivisors S
⊢ lift.{w, v} (trdeg R S) + lift.{v, w} (trdeg S A) = lift.{v, w} (trdeg R A)
have this₁ : Nontrivial S
Tactic: have := (FaithfulSMul.algebraMap_injective R S).nontrivial
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
R : Type u_1
S : Type v
A : Type w
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 : Nontrivial R
inst_8 : NoZeroDivisors A
inst_9 : FaithfulSMul R S
inst_10 : FaithfulSMul S A
s : Set S
hs : IsTranscendenceBasis.{v, u_1, v} (ι := { x : S // x ∈ s }) R (Subtype.val (p := fun (x : S) ↦ x ∈ s))
t : Set A
ht : IsTranscendenceBasis.{w, v, w} (ι := { x : A // x ∈ t }) S (Subtype.val (p := fun (x : A) ↦ x ∈ t))
this_1 : NoZeroDivisors S
this : Nontrivial S
⊢ lift.{w, v} (trdeg R S) + lift.{v, w} (trdeg S A) = lift.{v, w} (trdeg R A)
have rw : lift.{w, v} #{ x : S // x ∈ s } + lift.{v, w} (trdeg S A) = lift.{v, w} (trdeg R A)
Tactic: rw [← hs.cardinalMk_eq_trdeg, ← ht.cardinalMk_eq_trdeg, ← lift_umax.{w}, add_comm,
    ← (hs.sumElim_comp ht).lift_cardinalMk_eq_trdeg, mk_sum, lift_add, lift_lift, lift_lift]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
R : Type u_1
S : Type v
A : Type w
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 : Nontrivial R
inst_8 : NoZeroDivisors A
inst_9 : FaithfulSMul R S
inst_10 : FaithfulSMul S A
s : Set S
hs : IsTranscendenceBasis.{v, u_1, v} (ι := { x : S // x ∈ s }) R (Subtype.val (p := fun (x : S) ↦ x ∈ s))
t : Set A
ht : IsTranscendenceBasis.{w, v, w} (ι := { x : A // x ∈ t }) S (Subtype.val (p := fun (x : A) ↦ x ∈ t))
this_1 : NoZeroDivisors S
this : Nontrivial S
rw : lift.{w, v} #{ x : S // x ∈ s } + lift.{v, w} (trdeg S A) = lift.{v, w} (trdeg R A)
⊢ lift.{w, v} (trdeg R S) + lift.{v, w} (trdeg S A) = lift.{v, w} (trdeg R A)
have rw₁ : lift.{w, v} #{ x : S // x ∈ s } + lift.{v, w} #{ x : A // x ∈ t } = lift.{v, w} (trdeg R A)
Tactic: rw [← hs.cardinalMk_eq_trdeg, ← ht.cardinalMk_eq_trdeg, ← lift_umax.{w}, add_comm,
    ← (hs.sumElim_comp ht).lift_cardinalMk_eq_trdeg, mk_sum, lift_add, lift_lift, lift_lift]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
R : Type u_1
S : Type v
A : Type w
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 : Nontrivial R
inst_8 : NoZeroDivisors A
inst_9 : FaithfulSMul R S
inst_10 : FaithfulSMul S A
s : Set S
hs : IsTranscendenceBasis.{v, u_1, v} (ι := { x : S // x ∈ s }) R (Subtype.val (p := fun (x : S) ↦ x ∈ s))
t : Set A
ht : IsTranscendenceBasis.{w, v, w} (ι := { x : A // x ∈ t }) S (Subtype.val (p := fun (x : A) ↦ x ∈ t))
this_1 : NoZeroDivisors S
this : Nontrivial S
rw : lift.{w, v} #{ x : S // x ∈ s } + lift.{v, w} (trdeg S A) = lift.{v, w} (trdeg R A)
rw₁ : lift.{w, v} #{ x : S // x ∈ s } + lift.{v, w} #{ x : A // x ∈ t } = lift.{v, w} (trdeg R A)
⊢ lift.{w, v} (trdeg R S) + lift.{v, w} (trdeg S A) = lift.{v, w} (trdeg R A)
have rw₂ : lift.{w, v} #{ x : S // x ∈ s } + lift.{max w v, w} #{ x : A // x ∈ t } = lift.{max w v, w} (trdeg R A)
Tactic: rw [← hs.cardinalMk_eq_trdeg, ← ht.cardinalMk_eq_trdeg, ← lift_umax.{w}, add_comm,
    ← (hs.sumElim_comp ht).lift_cardinalMk_eq_trdeg, mk_sum, lift_add, lift_lift, lift_lift]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
R : Type u_1
S : Type v
A : Type w
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 : Nontrivial R
inst_8 : NoZeroDivisors A
inst_9 : FaithfulSMul R S
inst_10 : FaithfulSMul S A
s : Set S
hs : IsTranscendenceBasis.{v, u_1, v} (ι := { x : S // x ∈ s }) R (Subtype.val (p := fun (x : S) ↦ x ∈ s))
t : Set A
ht : IsTranscendenceBasis.{w, v, w} (ι := { x : A // x ∈ t }) S (Subtype.val (p := fun (x : A) ↦ x ∈ t))
this_1 : NoZeroDivisors S
this : Nontrivial S
rw : lift.{w, v} #{ x : S // x ∈ s } + lift.{v, w} (trdeg S A) = lift.{v, w} (trdeg R A)
rw₁ : lift.{w, v} #{ x : S // x ∈ s } + lift.{v, w} #{ x : A // x ∈ t } = lift.{v, w} (trdeg R A)
rw₂ : lift.{w, v} #{ x : S // x ∈ s } + lift.{max w v, w} #{ x : A // x ∈ t } = lift.{max w v, w} (trdeg R A)
⊢ lift.{w, v} (trdeg R S) + lift.{v, w} (trdeg S A) = lift.{v, w} (trdeg R A)
have rw₃ : lift.{max w v, w} #{ x : A // x ∈ t } + lift.{w, v} #{ x : S // x ∈ s } = lift.{max w v, w} (trdeg R A)
Tactic: rw [← hs.cardinalMk_eq_trdeg, ← ht.cardinalMk_eq_trdeg, ← lift_umax.{w}, add_comm,
    ← (hs.sumElim_comp ht).lift_cardinalMk_eq_trdeg, mk_sum, lift_add, lift_lift, lift_lift]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
Goal:
R : Type u_1
S : Type v
A : Type w
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 : Nontrivial R
inst_8 : NoZeroDivisors A
inst_9 : FaithfulSMul R S
inst_10 : FaithfulSMul S A
s : Set S
hs : IsTranscendenceBasis.{v, u_1, v} (ι := { x : S // x ∈ s }) R (Subtype.val (p := fun (x : S) ↦ x ∈ s))
t : Set A
ht : IsTranscendenceBasis.{w, v, w} (ι := { x : A // x ∈ t }) S (Subtype.val (p := fun (x : A) ↦ x ∈ t))
this_1 : NoZeroDivisors S
this : Nontrivial S
rw : lift.{w, v} #{ x : S // x ∈ s } + lift.{v, w} (trdeg S A) = lift.{v, w} (trdeg R A)
rw₁ : lift.{w, v} #{ x : S // x ∈ s } + lift.{v, w} #{ x : A // x ∈ t } = lift.{v, w} (trdeg R A)
rw₂ : lift.{w, v} #{ x : S // x ∈ s } + lift.{max w v, w} #{ x : A // x ∈ t } = lift.{max w v, w} (trdeg R A)
rw₃ : lift.{max w v, w} #{ x : A // x ∈ t } + lift.{w, v} #{ x : S // x ∈ s } = lift.{max w v, w} (trdeg R A)
⊢ lift.{w, v} (trdeg R S) + lift.{v, w} (trdeg S A) = lift.{v, w} (trdeg R A)
have rw₄ : lift.{max w v, w} #{ x : A // x ∈ t } + lift.{w, v} #{ x : S // x ∈ s } =
  lift.{w, max v w} #(Sum.{w, v} { x : A // x ∈ t } { x : S // x ∈ s })
Tactic: rw [← hs.cardinalMk_eq_trdeg, ← ht.cardinalMk_eq_trdeg, ← lift_umax.{w}, add_comm,
    ← (hs.sumElim_comp ht).lift_cardinalMk_eq_trdeg, mk_sum, lift_add, lift_lift, lift_lift]