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

Goal state before:
pp: ι : Type u_1
R : Type u_3
inst✝ : CommRing R
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x : ι → MvPolynomial ι R := fun i ↦ (Polynomial.aeval (X i)) (f i)
t : Set ι
x✝¹ : t.Finite
x✝ : AlgebraicIndependent R fun i ↦ x ↑i
i : ι
hi : i ∉ t
⊢ adjoin R (x '' t) ≤ supported R t

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
inst✝ : CommRing R
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
⊢ AlgebraicIndependent R fun i ↦ (Polynomial.aeval (X i)) (f i)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
S : Set α
hS : S ⊆ M.E
⊢ ¬M.Spanning S ↔ M.closure S ⊂ M.E

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
⊢ AlgebraicIndependent R fun i ↦ (Polynomial.aeval (x i)) (f i)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
S T : Set α
hS : M.Spanning S
hST : S ⊆ T
hT : T ⊆ M.E
⊢ M.E ⊆ M.closure T

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
S T : Set α
hS : M.Spanning S
hST : S ⊆ T
⊢ M.closure T = M.E

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
S : Set α
⊢ M.Spanning S ↔ (∃ B, M.IsBase B ∧ B ⊆ S) ∧ S ⊆ M.E

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
S : Set α
hS : S ⊆ M.E
⊢ M.Spanning S ↔ ∃ B, M.IsBase B ∧ B ⊆ S

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
S : Set α
hS : M.Spanning S
⊢ ∃ B, M.IsBase B ∧ B ⊆ S

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.SeparableDegree

Goal state before:
pp: F : Type u_1
inst✝ : CommSemiring F
q : ℕ
f g : F[X]
hf : IsSeparableContraction q f g
⊢ ∃ m, g.natDegree * q ^ m = f.natDegree

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.SeparableDegree

Goal state before:
pp: F : Type u_1
inst✝ : CommSemiring F
f : F[X]
hf : HasSeparableContraction 1 f
⊢ hf.degree = f.natDegree

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.SeparableDegree

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
f : F[X]
irred : Irreducible f
inst✝ : CharZero F
⊢ (expand F (1 ^ 0)) f = f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.SeparableDegree

Goal state before:
pp: F : Type u_1
inst✝ : Field F
q : ℕ
hF : ExpChar F q
f : F[X]
irred : Irreducible f
⊢ HasSeparableContraction q f

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
hI : I ⊆ M.E
⊢ M.Coindep I ↔ M.Spanning (M.E \ I)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
S : Set α
hS : S ⊆ M.E
⊢ M.Spanning S ↔ M.Coindep (M.E \ S)

Tactic:
by

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

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
S : Type u_3
B : Type u_4
FRS : Type u_5
FAB : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : CommRing B
inst✝⁴ : Algebra S B
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
H : ∀ (p : MvPolynomial ι R), (aeval x) p = 0 → p = 0
hf : Surjective ⇑f
hg : Injective ⇑g
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
q : MvPolynomial ι R
hp : (aeval (⇑g ∘ x)) ((MvPolynomial.map ↑f) q) = 0
⊢ g ((aeval x) q) = g 0

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X : Set α
hK : X ⊆ M.E
⊢ M.Coindep X ↔ M.closure (M.E \ X) = M.E

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
hIs : M.Spanning I
⊢ M.IsBase I

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X I : Set α
hIX : M.IsBasis I X
⊢ M.Spanning I ↔ M.Spanning X

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
S B : Set α
hS : M.Spanning S
h : M.IsBasis B S
⊢ M.Spanning B

Tactic:
by

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

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
S : Type u_3
B : Type u_4
FRS : Type u_5
FAB : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : CommRing B
inst✝⁴ : Algebra S B
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
H : AlgebraicIndependent R x
hf : Surjective ⇑f
hg : Injective ⇑g
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
⊢ AlgebraicIndependent S (⇑g ∘ x)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
S B : Set α
hS : M.Spanning S
⊢ (M ↾ S).IsBase B ↔ M.IsBase B ∧ B ⊆ S

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
S : Set α
hS : M.Spanning S
⊢ M.Coindep (M.E \ S)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X I : Set α
hIX : M.IsBasis I X
hX : M.Spanning X
⊢ M.Spanning I

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
S I : Set α
hI : M.Indep I
hS : M.Spanning S
hIS : I ⊆ S
⊢ ∃ B, M.IsBase B ∧ I ⊆ B ∧ B ⊆ S

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
B : Set α
N : Matroid α
hR : N ≤r M
hN : M.Spanning N.E
⊢ N.IsBase B ↔ M.IsBase B ∧ B ⊆ N.E

Tactic:
by

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

Goal state before:
pp: R : Type u_2
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
x : ↥(Finset.map (Embedding.subtype fun x ↦ x ∈ s) t)
⊢ ↑x ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
S : Set α
hSE : S ⊆ M.E
⊢ M.Spanning S ↔ M'.Spanning S

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
⊢ M.Spanning = M'.Spanning

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.SeparableDegree

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
q : ℕ
hq : NeZero q
inst✝ : CharP F q
g g' : F[X]
m m' : ℕ
h_expand : (expand F (q ^ m)) g = (expand F (q ^ m')) g'
hg : g.Separable
hg' : g'.Separable
⊢ g.natDegree = g'.natDegree

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.SeparableDegree

Goal state before:
pp: F : Type u_1
inst✝ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
g : F[X]
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
hg : g.Separable
m : ℕ
hm : (expand F (q ^ m)) g = f
g' : F[X] := Classical.choose hf
hg' : (Classical.choose hf).Separable
m' : ℕ
hm' : (expand F (q ^ m')) (Classical.choose hf) = f
⊢ Nat.Prime q

Tactic:
by

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

Goal state before:
pp: R : Type u_2
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
⊢ AlgebraicIndependent R Subtype.val

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.SeparableDegree

Goal state before:
pp: F : Type u_1
inst✝ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
hF : ExpChar F q
g : F[X]
hg : IsSeparableContraction q f g
⊢ g.natDegree = hf.degree

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
⊢ M = M'

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X B : Set α
hB : M.IsBase B
hX : M.Spanning X
hXB : X ⊆ B
B' : Set α
hB' : M.IsBase B'
hB'X : B' ⊆ X
⊢ B ⊆ X

Tactic:
by

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

Goal state before:
pp: R : Type u_2
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
n : ℕ
H : ∀ (s : Finset A), (AlgebraicIndependent R fun i ↦ ↑i) → s.card ≤ n
⊢ ∀ (s : Set A), AlgebraicIndependent R Subtype.val → Cardinal.mk ↑s ≤ ↑n

Tactic:
by

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

Goal state before:
pp: R : Type u_2
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ AlgebraicIndependent R Subtype.val ↔ Injective ⇑(algebraMap R A)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
B : Set α
⊢ M.IsBase B ↔ Minimal M.Spanning B

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X : Set α
hX : M.Spanning X
h : ∀ ⦃Y : Set α⦄, M.Spanning Y → Y ⊆ X → X = Y
⊢ M.IsBase X

Tactic:
by

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

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
⊢ AlgebraicIndependent R Subtype.val

Tactic:
by

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

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : IsTranscendenceBasis R x
⊢ IsTranscendenceBasis R Subtype.val

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X R : Set α
⊢ (M ↾ R).closure X = M.closure (X ∩ R) ∩ R ∪ R \ M.E

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
X R : Set α
M : Matroid α
hXR : X ⊆ R
hR : R ⊆ M.E
⊢ (M ↾ R).closure X = M.closure X ∩ R

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
E X : Set α
⊢ (loopyOn E).closure X = E

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
X E : Set α
⊢ (loopyOn E).Spanning X ↔ X ⊆ E

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
E X : Set α
⊢ (freeOn E).closure X = X ∩ E

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
I E X : Set α
⊢ (uniqueBaseOn I E).closure X = X ∩ I ∩ E ∪ E \ I

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
h : M = loopyOn M.E
⊢ M.closure ∅ = M.E

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
h : M.closure ∅ = M.E
X : Set α
⊢ M.closure X ⊆ (loopyOn M.E).closure X

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
⊢ M.closure ∅ = M.E ↔ M = loopyOn M.E

Tactic:
by

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

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
A' : Type v'
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
x : ι → A
f : A →ₐ[R] A'
h : Injective ⇑f
H : IsTranscendenceBasis R (⇑f ∘ x)
s : Set A
hs : AlgebraicIndepOn R _root_.id s
hs' : range x ⊆ s
⊢ range (⇑f ∘ x) ⊆ ⇑f '' s

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
β : Type u_3
M : Matroid β
f : α → β
X : Set α
⊢ (M.comap f).closure X = f ⁻¹' M.closure (f '' X)

Tactic:
by

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

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
A' : Type v'
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
x : ι → A
f : A →ₐ[R] A'
h : Injective ⇑f
H : IsTranscendenceBasis R (⇑f ∘ x)
⊢ IsTranscendenceBasis R x

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
aux : ∀ ⦃I : Set α⦄, M.Indep I → (M.map f hf).closure (f '' I) = f '' M.closure I
⊢ (M.map f hf).closure X = f '' M.closure (f ⁻¹' X)

Tactic:
by

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

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
A' : Type v'
x : ι → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
e : A ≃ₐ[R] A'
hx : IsTranscendenceBasis R x
⊢ IsTranscendenceBasis R (⇑↑e.symm ∘ ⇑e ∘ x)

Tactic:
convert! hx; ext; simp

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

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
A' : Type v'
x : ι → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
e : A ≃ₐ[R] A'
hx : IsTranscendenceBasis R x
⊢ IsTranscendenceBasis R (⇑↑e.symm ∘ ⇑e ∘ x)

Tactic:
by

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

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
A' : Type v'
x : ι → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
e : A ≃ₐ[R] A'
hx : IsTranscendenceBasis R (⇑e ∘ x)
⊢ IsTranscendenceBasis R x

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
⊢ (M.map f hf).closure X = f '' M.closure (f ⁻¹' X)

Tactic:
by

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

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
hx : AlgebraicIndependent R x
⊢ lift.{v, u} #ι ≤ lift.{u, v} (trdeg R A)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
R S : Set α
hSR : S ⊆ R
hR : R ⊆ M.E
⊢ (M ↾ R).Spanning S ↔ R ⊆ M.closure S

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
R S : Set α
⊢ (M ↾ R).Spanning S ↔ R ∩ M.E ⊆ M.closure S ∧ S ⊆ R

Tactic:
by

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

Goal state before:
pp: R : Type u_2
A : Type v
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
ι : Type v
x : ι → A
hx : AlgebraicIndependent R x
⊢ #ι ≤ trdeg R A

Tactic:
by

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

Goal state before:
pp: R : Type u_2
A : Type v
A' : Type v'
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
f : A →ₐ[R] A'
hf : Injective ⇑f
⊢ lift.{v', v} (trdeg R A) ≤ lift.{v, v'} (trdeg R A')

Tactic:
by

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

Goal state before:
pp: R : Type u_2
A : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
A' : Type v
inst✝¹ : CommRing A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
hf : Injective ⇑f
⊢ lift.{v, v} (trdeg R A) ≤ lift.{v, v} (trdeg R A')

Tactic:
exact lift_trdeg_le_of_injective f hf

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

Goal state before:
pp: R : Type u_2
A : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
A' : Type v
inst✝¹ : CommRing A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
hf : Injective ⇑f
⊢ trdeg R A ≤ trdeg R A'

Tactic:
by

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

Goal state before:
pp: R : Type u_2
A : Type v
A' : Type v'
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
f : A →ₐ[R] A'
hf : Surjective ⇑f
⊢ lift.{v, v'} (trdeg R A') ≤ lift.{v', v} (trdeg R A)

Tactic:
by

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

Goal state before:
pp: R : Type u_2
A : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
A' : Type v
inst✝¹ : CommRing A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
hf : Surjective ⇑f
⊢ trdeg R A' ≤ trdeg R A

Tactic:
by

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

Goal state before:
pp: R : Type u_2
A : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
A' : Type v
inst✝¹ : CommRing A'
inst✝ : Algebra R A'
e : A ≃ₐ[R] A'
⊢ trdeg R A = trdeg R A'

Tactic:
by

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

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
⊢ aeval (x ∘ Subtype.val) = (aeval x).comp (rename Subtype.val)

Tactic:
by

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

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
⊢ AlgebraicIndependent R (x ∘ Subtype.val) ↔ ∀ p ∈ supported R s, (aeval x) p = 0 → p = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_2
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
⊢ AlgebraicIndependent R Subtype.val ↔ ∀ p ∈ supported R s, (aeval _root_.id) p = 0 → p = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_2
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
H : ∀ t ⊆ s, t.Finite → AlgebraicIndependent R Subtype.val
p : MvPolynomial A R
hp : p ∈ supported R s
⊢ p ∈ supported R ↑p.vars

Tactic:
by

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

Goal state before:
pp: R : Type u_2
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
ι : Type u_3
ι' : Type u_4
s : Set ι
f : ι → ι'
g : ι' → A
hs : AlgebraicIndependent R fun x ↦ g (f ↑x)
⊢ AlgebraicIndependent R fun x ↦ g ↑x

Tactic:
by

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

Goal state before:
pp: R : Type u_2
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
ι : Type u_3
s : Set ι
f : ι → A
hs : AlgebraicIndependent R fun x ↦ f ↑x
⊢ AlgebraicIndependent R fun x ↦ ↑x

Tactic:
by

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

Goal state before:
pp: R : Type u_2
A : Type v
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
η : Type u_3
inst✝ : Nonempty η
s : η → Set A
hs : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ (i : η), AlgebraicIndependent R Subtype.val
⊢ AlgebraicIndependent R Subtype.val

Tactic:
by

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

Goal state before:
pp: R : Type u_2
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set (Set A)
hsn : s.Nonempty
hs : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, AlgebraicIndependent R Subtype.val
this : Nonempty ↑s := Nonempty.to_subtype hsn
⊢ ∀ (i : ↑s), AlgebraicIndependent R Subtype.val

Tactic:
by

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

Goal state before:
pp: R : Type u_2
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set (Set A)
hsn : s.Nonempty
hs : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, AlgebraicIndependent R Subtype.val
⊢ AlgebraicIndependent R Subtype.val

Tactic:
by

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

Goal state before:
pp: R : Type u_2
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s t : Set A
hst : s ⊆ t
hs : AlgebraicIndepOn R _root_.id s
⊢ ∃ u, s ⊆ u ∧ Maximal (fun x ↦ AlgebraicIndepOn R _root_.id x ∧ x ⊆ t) u

Tactic:
by

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

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
r : R
⊢ Polynomial.C (hx.aevalEquiv (C r)) = Polynomial.C ((algebraMap R ↥(adjoin R (range x))) r)

Tactic:
by

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

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
r : R
⊢ hx.mvPolynomialOptionEquivPolynomialAdjoin (C r) = Polynomial.C ((algebraMap R ↥(adjoin R (range x))) r)

Tactic:
by

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

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
⊢ hx.mvPolynomialOptionEquivPolynomialAdjoin (X none) = Polynomial.X

Tactic:
by

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

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
i : ι
⊢ hx.mvPolynomialOptionEquivPolynomialAdjoin (X (some i)) = Polynomial.C (hx.aevalEquiv (X i))

Tactic:
by

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

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
a : A
⊢ (↑(Polynomial.aeval a)).comp hx.mvPolynomialOptionEquivPolynomialAdjoin.toRingHom = ↑(aeval fun o ↦ o.elim a x)

Tactic:
by

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

Goal state before:
pp: ι : Type u
A : Type v
x : ι → A
inst✝⁴ : CommRing A
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra K A
inst✝¹ : IsEmpty ι
inst✝ : Nontrivial A
⊢ AlgebraicIndependent K x

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.AlgebraicClosure

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K : Type u_3
inst✝¹ : Field K
inst✝ : Algebra F K
i : E →ₐ[F] K
x : E
⊢ i x ∈ algebraicClosure F K ↔ x ∈ algebraicClosure F E

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.AlgebraicClosure

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K : Type u_3
inst✝¹ : Field K
inst✝ : Algebra F K
i : E →ₐ[F] K
⊢ comap i (algebraicClosure F K) = algebraicClosure F E

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.AlgebraicClosure

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
h : algebraicClosure E K = ⊥
⊢ IntermediateField.map (IsScalarTower.toAlgHom F E K) (algebraicClosure F E) = algebraicClosure F K

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.AlgebraicClosure

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K : Type u_3
inst✝¹ : Field K
inst✝ : Algebra F K
i : E ≃ₐ[F] K
x : K
h : x ∈ algebraicClosure F K
⊢ ↑↑i (↑i.symm x) = x

Tactic:
by

Goal state after: