mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case inr
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x : ι → A
y : ι' → A
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : FaithfulSMul R A
inst✝ : NoZeroDivisors A
I B : Set A
I_ind : AlgebraicIndepOn R _root_.id I
h : ∀ x ∈ B \ I, ¬AlgebraicIndepOn R _root_.id (insert x I)
h✝ : Nontrivial R
B_base : Algebra.IsAlgebraic (↥(adjoin R B)) A
⊢ Algebra.IsAlgebraic (↥(adjoin R I)) A

Tactic:
]

Goal state after:
case inr
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x : ι → A
y : ι' → A
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : FaithfulSMul R A
inst✝ : NoZeroDivisors A
I B : Set A
I_ind : AlgebraicIndepOn R _root_.id I
h : ∀ x ∈ B \ I, ¬AlgebraicIndepOn R _root_.id (insert x I)
h✝ : Nontrivial R
B_base : Algebra.IsAlgebraic (↥(adjoin R B)) A
⊢ Algebra.IsAlgebraic (↥(adjoin R I)) A
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x✝ : ι → A
y : ι' → A
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : FaithfulSMul R A
inst✝ : NoZeroDivisors A
I B : Set A
I_ind : AlgebraicIndepOn R _root_.id I
h✝ : Nontrivial R
B_base : Algebra.IsAlgebraic (↥(adjoin R B)) A
a x : A
hx : x ∈ B \ I
h : ¬IsAlgebraic (↥(adjoin R I)) x
⊢ Transcendental (↥(adjoin R I)) (_root_.id x)

Tactic:
]

Goal state after:
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x✝ : ι → A
y : ι' → A
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : FaithfulSMul R A
inst✝ : NoZeroDivisors A
I B : Set A
I_ind : AlgebraicIndepOn R _root_.id I
h✝ : Nontrivial R
B_base : Algebra.IsAlgebraic (↥(adjoin R B)) A
a x : A
hx : x ∈ B \ I
h : ¬IsAlgebraic (↥(adjoin R I)) x
⊢ Transcendental (↥(adjoin R I)) (_root_.id x)
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : IsDomain A
s t : Set A
⊢ (((matroid R A).Indep s ∧ s ⊆ t) ∧ ∀ x ∉ s, ¬((matroid R A).Indep (insert x s) ∧ insert x s ⊆ t)) ∧
      t ⊆ (matroid R A).E ↔
    AlgebraicIndepOn R _root_.id s ∧ s ⊆ t ∧ ∀ a ∈ t, IsAlgebraic (↥(adjoin R s)) a

Tactic:
]

Goal state after:
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : IsDomain A
s t : Set A
⊢ (((matroid R A).Indep s ∧ s ⊆ t) ∧ ∀ x ∉ s, ¬((matroid R A).Indep (insert x s) ∧ insert x s ⊆ t)) ∧
      t ⊆ (matroid R A).E ↔
    AlgebraicIndepOn R _root_.id s ∧ s ⊆ t ∧ ∀ a ∈ t, IsAlgebraic (↥(adjoin R s)) a
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : IsDomain A
s t : Set A
h : AlgebraicIndepOn R _root_.id s ∧ s ⊆ t
max : ∀ x ∉ s, ¬(AlgebraicIndepOn R _root_.id (insert x s) ∧ insert x s ⊆ t)
a : A
ha : a ∈ t
tr : ¬IsAlgebraic (↥(adjoin R s)) a
⊢ Transcendental (↥(adjoin R s)) (_root_.id a)

Tactic:
]

Goal state after:
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : IsDomain A
s t : Set A
h : AlgebraicIndepOn R _root_.id s ∧ s ⊆ t
max : ∀ x ∉ s, ¬(AlgebraicIndepOn R _root_.id (insert x s) ∧ insert x s ⊆ t)
a : A
ha : a ∈ t
tr : ¬IsAlgebraic (↥(adjoin R s)) a
⊢ Transcendental (↥(adjoin R s)) (_root_.id a)
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : IsDomain A
s t : Set A
h✝ : 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:
]

Goal state after:
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : IsDomain A
s t : Set A
h✝ : 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)
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : IsDomain A
s : Set A
⊢ ↑(algebraicClosure (↥(adjoin R s)) A) = s ↔ ∃ S, ↑S = s ∧ ∀ (a : A), IsAlgebraic (↥S) a → a ∈ s

Tactic:
]

Goal state after:
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : IsDomain A
s : Set A
⊢ ↑(algebraicClosure (↥(adjoin R s)) A) = s ↔ ∃ S, ↑S = s ∧ ∀ (a : A), IsAlgebraic (↥S) a → a ∈ s
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case refine_1
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : IsDomain A
s : Set A
S : Subalgebra (↥(adjoin R s)) A := algebraicClosure (↥(adjoin R s)) A
eq : ↑S = s
a : A
h : IsAlgebraic (↥S) a
⊢ a ∈ ↑S

Tactic:
]

Goal state after:
case refine_1
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : IsDomain A
s : Set A
S : Subalgebra (↥(adjoin R s)) A := algebraicClosure (↥(adjoin R s)) A
eq : ↑S = s
a : A
h : IsAlgebraic (↥S) a
⊢ a ∈ ↑S
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
A : Type w
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : NoZeroDivisors A
s t : Set A
hst : s ⊆ t
hs : AlgebraicIndepOn R _root_.id s
this✝² : Nontrivial ↥(adjoin R t)
this✝¹ : Nontrivial A
this✝ : IsDomain A
this : FaithfulSMul R A
ht : (matroid R A).Spanning t
⊢ ∃ u, s ⊆ u ∧ u ⊆ t ∧ IsTranscendenceBasis R Subtype.val

Tactic:
]

Goal state after:
R : Type u_1
A : Type w
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : NoZeroDivisors A
s t : Set A
hst : s ⊆ t
hs : AlgebraicIndepOn R _root_.id s
this✝² : Nontrivial ↥(adjoin R t)
this✝¹ : Nontrivial A
this✝ : IsDomain A
this : FaithfulSMul R A
ht : (matroid R A).Spanning t
⊢ ∃ u, s ⊆ u ∧ u ⊆ t ∧ IsTranscendenceBasis R Subtype.val
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
A : Type w
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : NoZeroDivisors A
s t : Set A
hst : s ⊆ t
this✝² : Nontrivial ↥(adjoin R t)
this✝¹ : Nontrivial A
this✝ : IsDomain A
this : FaithfulSMul R A
hs : (matroid R A).Indep s
ht : (matroid R A).Spanning t
⊢ ∃ u, s ⊆ u ∧ u ⊆ t ∧ IsTranscendenceBasis R Subtype.val

Tactic:
]

Goal state after:
R : Type u_1
A : Type w
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : NoZeroDivisors A
s t : Set A
hst : s ⊆ t
this✝² : Nontrivial ↥(adjoin R t)
this✝¹ : Nontrivial A
this✝ : IsDomain A
this : FaithfulSMul R A
hs : (matroid R A).Indep s
ht : (matroid R A).Spanning t
⊢ ∃ u, s ⊆ u ∧ u ⊆ t ∧ IsTranscendenceBasis R Subtype.val
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors A
hx : IsTranscendenceBasis R x
this : FaithfulSMul R A
⊢ lift.{u, w} #↑(range x) = lift.{u, w} #↑(range x)

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors A
ι : Type w
x : ι → A
hx : IsTranscendenceBasis R x
⊢ trdeg R A = trdeg R A

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
ι' : Type u'
R : Type u_1
A : Type w
x : ι → A
y : ι' → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis R y
⊢ lift.{max u u', w} (trdeg R A) = lift.{max u' u, w} (trdeg R A)

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors A
ι' : Type u
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis R y
⊢ #ι' = #ι'

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
S : Type v
inst✝¹ : CommRing S
inst✝ : IsDomain S
this : trdeg S (MvPolynomial ι S) = lift.{v, u} #ι
⊢ trdeg S (MvPolynomial ι S) = lift.{v, u} #ι

Tactic:
]

Goal state after:
ι : Type u
S : Type v
inst✝¹ : CommRing S
inst✝ : IsDomain S
this : trdeg S (MvPolynomial ι S) = lift.{v, u} #ι
⊢ trdeg S (MvPolynomial ι S) = lift.{v, u} #ι
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case pos
R : Type u_1
A : Type w
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
s : Set A
inst✝ : NoZeroDivisors A
h : Injective ⇑(algebraMap R A)
this✝ : IsDomain A
this : FaithfulSMul R A
alg : (matroid R A).Spanning s
⊢ (matroid R A).cRank ≤ #↑s

Tactic:
]

Goal state after:
case pos
R : Type u_1
A : Type w
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
s : Set A
inst✝ : NoZeroDivisors A
h : Injective ⇑(algebraMap R A)
this✝ : IsDomain A
this : FaithfulSMul R A
alg : (matroid R A).Spanning s
⊢ (matroid R A).cRank ≤ #↑s
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : NoZeroDivisors A
inst✝¹ : FaithfulSMul R A
inst✝ : Finite ι
le : lift.{w, u} #ι ≤ lift.{u, w} (matroid R A).cRank
toFun✝ : ι → ↑(range x)
h : Injective toFun✝
this✝ : Bijective (rangeFactorization x)
this : IsDomain A
alg : (matroid R A).Spanning (range x)
⊢ IsTranscendenceBasis R Subtype.val

Tactic:
]

Goal state after:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : NoZeroDivisors A
inst✝¹ : FaithfulSMul R A
inst✝ : Finite ι
le : lift.{w, u} #ι ≤ lift.{u, w} (matroid R A).cRank
toFun✝ : ι → ↑(range x)
h : Injective toFun✝
this✝ : Bijective (rangeFactorization x)
this : IsDomain A
alg : (matroid R A).Spanning (range x)
⊢ IsTranscendenceBasis R Subtype.val
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
A : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
inst✝³ : NoZeroDivisors A
inst✝² : FaithfulSMul R A
ι : Type w
inst✝¹ : Finite ι
x : ι → A
inst✝ : Algebra.IsAlgebraic (↥(adjoin R (range x))) A
le : #ι ≤ trdeg R A
⊢ #ι ≤ trdeg R A

Tactic:
]

Goal state after:
R : Type u_1
A : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
inst✝³ : NoZeroDivisors A
inst✝² : FaithfulSMul R A
ι : Type w
inst✝¹ : Finite ι
x : ι → A
inst✝ : Algebra.IsAlgebraic (↥(adjoin R (range x))) A
le : #ι ≤ trdeg R A
⊢ #ι ≤ trdeg R A
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
A : Type w
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : NoZeroDivisors A
inst✝¹ : FaithfulSMul R A
ι : Type w
x : ι → A
inst✝ : Algebra.IsAlgebraic (↥(adjoin R (range x))) A
fin : trdeg R A < ℵ₀
le : #ι ≤ trdeg R A
⊢ #ι ≤ trdeg R A

Tactic:
]

Goal state after:
R : Type u_1
A : Type w
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : NoZeroDivisors A
inst✝¹ : FaithfulSMul R A
ι : Type w
x : ι → A
inst✝ : Algebra.IsAlgebraic (↥(adjoin R (range x))) A
fin : trdeg R A < ℵ₀
le : #ι ≤ trdeg R A
⊢ #ι ≤ trdeg R A
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors A
hx : AlgebraicIndependent R x
le : lift.{u, w} (trdeg R A) ≤ lift.{w, u} #ι
this : FaithfulSMul R A
fin : (matroid R A).RankFinite
⊢ IsTranscendenceBasis R x

Tactic:
]

Goal state after:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors A
hx : AlgebraicIndependent R x
le : lift.{u, w} (trdeg R A) ≤ lift.{w, u} #ι
this : FaithfulSMul R A
fin : (matroid R A).RankFinite
⊢ IsTranscendenceBasis R x
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors A
ι : Type w
x : ι → A
hx : AlgebraicIndependent R x
fin : trdeg R A < ℵ₀
le : trdeg R A ≤ #ι
⊢ trdeg R A ≤ #ι

Tactic:
]

Goal state after:
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors A
ι : Type w
x : ι → A
hx : AlgebraicIndependent R x
fin : trdeg R A < ℵ₀
le : trdeg R A ≤ #ι
⊢ trdeg R A ≤ #ι
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
A : Type w
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Nontrivial R
inst✝¹ : NoZeroDivisors A
ι : Type w
inst✝ : Finite ι
x : ι → A
hx : AlgebraicIndependent R x
le : trdeg R A ≤ #ι
⊢ trdeg R A ≤ #ι

Tactic:
]

Goal state after:
R : Type u_1
A : Type w
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Nontrivial R
inst✝¹ : NoZeroDivisors A
ι : Type w
inst✝ : Finite ι
x : ι → A
hx : AlgebraicIndependent R x
le : trdeg R A ≤ #ι
⊢ trdeg R A ≤ #ι
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
i : E ≃ₐ[F] K
x✝ : Algebra E K := (↑i).toAlgebra
x : K
h : IsAlgebraic E (↑i (↑i.symm x))
⊢ IsAlgebraic E x

Tactic:
]

Goal state after:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
i : E ≃ₐ[F] K
x✝ : Algebra E K := (↑i).toAlgebra
x : K
h : IsAlgebraic E (↑i (↑i.symm x))
⊢ IsAlgebraic E x
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
⊢ Subsingleton (Emb F F) ∧ Nonempty (Emb F F)

Tactic:
]

Goal state after:
F : Type u
inst✝ : Field F
⊢ Subsingleton (Emb F F) ∧ Nonempty (Emb F F)
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
⊢ Subsingleton (Emb F F) ∧ Nonempty (Emb F F)

Tactic:
constructor <;> infer_instance

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
S : Type v
A : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
inst✝³ : Nontrivial R
inst✝² : NoZeroDivisors A
inst✝¹ : FaithfulSMul R S
inst✝ : FaithfulSMul S A
s : Set S
hs : IsTranscendenceBasis R Subtype.val
t : Set A
ht : IsTranscendenceBasis S Subtype.val
this✝ : NoZeroDivisors S
this : Nontrivial S
⊢ lift.{max w v, w} #{ x // x ∈ t } + lift.{w, v} #{ x // x ∈ s } =
    lift.{max v w, w} #{ x // x ∈ t } + lift.{w, v} #{ x // x ∈ s }

Tactic:
]

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
H : Algebra.Transcendental F E
ι : Type v
x : ι → E
hx : IsTranscendenceBasis F x
this : Algebra.IsAlgebraic (↥(adjoin F (Set.range x))) E
⊢ Infinite (Emb F ↥(adjoin F (Set.range x)) × Emb (↥(adjoin F (Set.range x))) E)

Tactic:
]

Goal state after:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
H : Algebra.Transcendental F E
ι : Type v
x : ι → E
hx : IsTranscendenceBasis F x
this : Algebra.IsAlgebraic (↥(adjoin F (Set.range x))) E
⊢ Infinite (Emb F ↥(adjoin F (Set.range x)) × Emb (↥(adjoin F (Set.range x))) E)
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
H : Algebra.Transcendental F E
ι : Type v
x : ι → E
hx : IsTranscendenceBasis F x
this : Algebra.IsAlgebraic (↥(adjoin F (Set.range x))) E
⊢ Infinite (Emb F (FractionRing (MvPolynomial ι F)))

Tactic:
]

Goal state after:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
H : Algebra.Transcendental F E
ι : Type v
x : ι → E
hx : IsTranscendenceBasis F x
this : Algebra.IsAlgebraic (↥(adjoin F (Set.range x))) E
⊢ Infinite (Emb F (FractionRing (MvPolynomial ι F)))
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : Nontrivial R
A : Type v
inst✝⁶ : CommRing A
inst✝⁵ : NoZeroDivisors A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : FaithfulSMul R S
inst✝¹ : FaithfulSMul S A
inst✝ : IsScalarTower R S A
⊢ lift.{v, v} (trdeg R S) + lift.{v, v} (trdeg S A) = lift.{v, v} (trdeg R A)

Tactic:
]

Goal state after:
R : Type u_1
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : Nontrivial R
A : Type v
inst✝⁶ : CommRing A
inst✝⁵ : NoZeroDivisors A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : FaithfulSMul R S
inst✝¹ : FaithfulSMul S A
inst✝ : IsScalarTower R S A
⊢ lift.{v, v} (trdeg R S) + lift.{v, v} (trdeg S A) = lift.{v, v} (trdeg R A)
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K✝ : Type w
inst✝¹ : Field K✝
inst✝ : Algebra F K✝
H : Algebra.Transcendental F E
ι : Type v
x : ι → E
hx : IsTranscendenceBasis F x
this : Algebra.IsAlgebraic (↥(adjoin F (Set.range x))) E
i : ι
K : Type (max u v) := FractionRing (MvPolynomial ι F)
i1 : MvPolynomial ι F →ₐ[F] AlgebraicClosure K := IsScalarTower.toAlgHom F (MvPolynomial ι F) (AlgebraicClosure K)
⊢ Function.Injective ⇑((algebraMap K (AlgebraicClosure K)).comp (algebraMap (MvPolynomial ι F) K))

Tactic:
]

Goal state after:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K✝ : Type w
inst✝¹ : Field K✝
inst✝ : Algebra F K✝
H : Algebra.Transcendental F E
ι : Type v
x : ι → E
hx : IsTranscendenceBasis F x
this : Algebra.IsAlgebraic (↥(adjoin F (Set.range x))) E
i : ι
K : Type (max u v) := FractionRing (MvPolynomial ι F)
i1 : MvPolynomial ι F →ₐ[F] AlgebraicClosure K := IsScalarTower.toAlgHom F (MvPolynomial ι F) (AlgebraicClosure K)
⊢ Function.Injective ⇑((algebraMap K (AlgebraicClosure K)).comp (algebraMap (MvPolynomial ι F) K))
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj : j ∈ insert i s
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝² : Nontrivial ↥(adjoin R (v '' (insert i s \ {j})))
this✝¹ : Nontrivial S
this✝ : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this : Nontrivial R
⊢ IsTranscendenceBasis R fun x ↦ v ↑x

Tactic:
]

Goal state after:
ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj : j ∈ insert i s
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝² : Nontrivial ↥(adjoin R (v '' (insert i s \ {j})))
this✝¹ : Nontrivial S
this✝ : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this : Nontrivial R
⊢ IsTranscendenceBasis R fun x ↦ v ↑x
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f : F[X]
this : (f.aroots f.SplittingField).card ≤ f.natDegree
⊢ f.natSepDegree ≤ f.natDegree

Tactic:
]

Goal state after:
F : Type u
inst✝ : Field F
f : F[X]
this : (f.aroots f.SplittingField).card ≤ f.natDegree
⊢ f.natSepDegree ≤ f.natDegree
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f : F[X]
h : f.natDegree ≠ 0
⊢ (f.aroots f.SplittingField).toFinset.Nonempty

Tactic:
]

Goal state after:
F : Type u
inst✝ : Field F
f : F[X]
h : f.natDegree ≠ 0
⊢ (f.aroots f.SplittingField).toFinset.Nonempty
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f : F[X]
h : f.natDegree ≠ 0
⊢ f.natDegree ≠ Zero.zero

Tactic:
]

Goal state after:
F : Type u
inst✝ : Field F
f : F[X]
h : f.natDegree ≠ 0
⊢ f.natDegree ≠ Zero.zero
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case h
F : Type u
inst✝ : Field F
f : F[X]
h : f.natDegree ≠ 0
⊢ f ≠ 0 ∧ (aeval (rootOfSplits ⋯ ⋯)) f = 0

Tactic:
]

Goal state after:
case h
F : Type u
inst✝ : Field F
f : F[X]
h : f.natDegree ≠ 0
⊢ f ≠ 0 ∧ (aeval (rootOfSplits ⋯ ⋯)) f = 0
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case inl.refl
ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
i : ι
v : ι → S
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝² : Nontrivial S
this✝¹ : IsDomain S
this✝ : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : i ∈ insert i s
this : Nontrivial ↥(adjoin R (v '' (insert i s \ {i})))
H₂ : v i ∈ (matroid R S).closure (v '' (insert i s \ {i}))
hj' : i ∉ s
⊢ IsTranscendenceBasis R fun x ↦ v ↑x

Tactic:
]

Goal state after:
case inl.refl
ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
i : ι
v : ι → S
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝² : Nontrivial S
this✝¹ : IsDomain S
this✝ : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : i ∈ insert i s
this : Nontrivial ↥(adjoin R (v '' (insert i s \ {i})))
H₂ : v i ∈ (matroid R S).closure (v '' (insert i s \ {i}))
hj' : i ∉ s
⊢ IsTranscendenceBasis R fun x ↦ v ↑x
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
f : F[X]
inst✝ : DecidableEq E
h : (map (algebraMap F E) f).Splits
⊢ (f.aroots f.SplittingField).toFinset.card = (map (algebraMap F f.SplittingField) f).roots.toFinset.card

Tactic:
]

Goal state after: