mathlib-initiative/mathlib-tactics huggingface dataset:
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
this : Finsupp.linearCombination R x = (aeval x).toLinearMap ∘ₗ Finsupp.linearCombination R X
⊢ Injective ⇑(Finsupp.linearCombination R x)

Tactic:
this

Goal state after:
ι : 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
this : Finsupp.linearCombination R x = (aeval x).toLinearMap ∘ₗ Finsupp.linearCombination R X
⊢ Injective ⇑((aeval x).toLinearMap ∘ₗ Finsupp.linearCombination R X)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
ι : Type u_4
hI : M.Indep I
X : ι → Set α
A : Set ι
hA : A.Nonempty
h : ∀ i ∈ A, M.IsBasis (X i ∩ I) (X i)
⊢ ⋂ i ∈ A, X i ⊆ M.closure ((⋂ i ∈ A, X i) ∩ I)

Tactic:
[

Goal state after:
α : Type u_2
M : Matroid α
I : Set α
ι : Type u_4
hI : M.Indep I
X : ι → Set α
A : Set ι
hA : A.Nonempty
h : ∀ i ∈ A, M.IsBasis (X i ∩ I) (X i)
⊢ ⋂ i ∈ A, X i ⊆ M.closure ((⋂ i ∈ A, X i) ∩ I)
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'
hx : AlgebraicIndependent R x✝
f : A →ₐ[R] A'
hf_inj : InjOn ⇑f ↑(adjoin R (range x✝))
this : aeval (⇑f ∘ x✝) = f.comp (aeval x✝)
h : ∀ (p : MvPolynomial ι R), (aeval x✝) p ∈ (aeval Subtype.val).range
x y : MvPolynomial ι R
hxy : (aeval (⇑f ∘ x✝)) x = (aeval (⇑f ∘ x✝)) y
⊢ x = y

Tactic:
this

Goal state after:
ι : 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'
hx : AlgebraicIndependent R x✝
f : A →ₐ[R] A'
hf_inj : InjOn ⇑f ↑(adjoin R (range x✝))
this : aeval (⇑f ∘ x✝) = f.comp (aeval x✝)
h : ∀ (p : MvPolynomial ι R), (aeval x✝) p ∈ (aeval Subtype.val).range
x y : MvPolynomial ι R
hxy : (f.comp (aeval x✝)) x = (f.comp (aeval x✝)) y
⊢ x = y
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: case refine_2
α : Type u
M : Matroid α
h : M.cRank < ℵ₀
B : Set α
hB : M.IsBase B
⊢ ∃ B, M.IsBase B ∧ B.Finite

Tactic:
[

Goal state after:
case refine_2
α : Type u
M : Matroid α
h : M.cRank < ℵ₀
B : Set α
hB : M.IsBase B
⊢ ∃ B, M.IsBase B ∧ B.Finite
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
s : Set ι
i : ι
h : i ∉ s
⊢ AlgebraicIndepOn R x (insert i s) ↔ AlgebraicIndepOn R x s ∧ Transcendental (↥(adjoin R (x '' s))) (x i)

Tactic:
[

Goal state after:
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
i : ι
h : i ∉ s
⊢ AlgebraicIndepOn R x (insert i s) ↔ AlgebraicIndepOn R x s ∧ Transcendental (↥(adjoin R (x '' s))) (x i)
Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental

Goal state before:
pp: case pos
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
ι' : Type u_4
y : ι' → A
hx : AlgebraicIndependent R x
e : MvPolynomial (ι' ⊕ ι) R ≃ₐ[R] MvPolynomial ι' ↥(adjoin R (range x)) :=
  (sumAlgEquiv R ι' ι).trans (mapAlgEquiv ι' hx.aevalEquiv)
this : aeval (Sum.elim y x) = (AlgHom.restrictScalars R (aeval y)).comp ↑e
⊢ AlgebraicIndependent R (Sum.elim y x) ↔ AlgebraicIndependent R x ∧ AlgebraicIndependent (↥(adjoin R (range x))) y

Tactic:
[

Goal state after:
case pos
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
ι' : Type u_4
y : ι' → A
hx : AlgebraicIndependent R x
e : MvPolynomial (ι' ⊕ ι) R ≃ₐ[R] MvPolynomial ι' ↥(adjoin R (range x)) :=
  (sumAlgEquiv R ι' ι).trans (mapAlgEquiv ι' hx.aevalEquiv)
this : aeval (Sum.elim y x) = (AlgHom.restrictScalars R (aeval y)).comp ↑e
⊢ AlgebraicIndependent R (Sum.elim y x) ↔ AlgebraicIndependent R x ∧ AlgebraicIndependent (↥(adjoin R (range x))) y
Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental

Goal state before:
pp: case pos
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
ι' : Type u_4
y : ι' → A
hx : AlgebraicIndependent R x
e : MvPolynomial (ι' ⊕ ι) R ≃ₐ[R] MvPolynomial ι' ↥(adjoin R (range x)) :=
  (sumAlgEquiv R ι' ι).trans (mapAlgEquiv ι' hx.aevalEquiv)
this : aeval (Sum.elim y x) = (AlgHom.restrictScalars R (aeval y)).comp ↑e
⊢ Injective ⇑(aeval (Sum.elim y x)) ↔ True ∧ Injective ⇑(aeval y)

Tactic:
this

Goal state after:
case pos
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
ι' : Type u_4
y : ι' → A
hx : AlgebraicIndependent R x
e : MvPolynomial (ι' ⊕ ι) R ≃ₐ[R] MvPolynomial ι' ↥(adjoin R (range x)) :=
  (sumAlgEquiv R ι' ι).trans (mapAlgEquiv ι' hx.aevalEquiv)
this : aeval (Sum.elim y x) = (AlgHom.restrictScalars R (aeval y)).comp ↑e
⊢ Injective ⇑((AlgHom.restrictScalars R (aeval y)).comp ↑e) ↔ True ∧ Injective ⇑(aeval y)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
⊢ M.Indep (I ∪ J) ↔ ∀ e ∈ I \ J, e ∉ M.closure (I \ {e} ∪ J)

Tactic:
[

Goal state after:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
⊢ M.Indep (I ∪ J) ↔ ∀ e ∈ I \ J, e ∉ M.closure (I \ {e} ∪ J)
Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental

Goal state before:
pp: R : Type u_3
S : Type u
A : Type v
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✝¹ : FaithfulSMul R S
inst✝ : FaithfulSMul S A
⊢ lift.{v, u} (trdeg R S) + lift.{u, v} (trdeg S A) ≤ lift.{u, v} (trdeg R A)

Tactic:
[

Goal state after:
R : Type u_3
S : Type u
A : Type v
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✝¹ : FaithfulSMul R S
inst✝ : FaithfulSMul S A
⊢ lift.{v, u} (trdeg R S) + lift.{u, v} (trdeg S A) ≤ lift.{u, v} (trdeg R A)
Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental

Goal state before:
pp: R : Type u_3
S : Type u
A : Type v
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✝¹ : FaithfulSMul R S
inst✝ : FaithfulSMul S A
⊢ (⨆ i, lift.{v, u} #↑↑i) + ⨆ i, lift.{u, v} #↑↑i ≤ ⨆ i, lift.{u, v} #↑↑i

Tactic:
[

Goal state after:
R : Type u_3
S : Type u
A : Type v
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✝¹ : FaithfulSMul R S
inst✝ : FaithfulSMul S A
⊢ (⨆ i, lift.{v, u} #↑↑i) + ⨆ i, lift.{u, v} #↑↑i ≤ ⨆ i, lift.{u, v} #↑↑i
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M₁ M₂ : Matroid α
h : ∀ (X : Set α), M₁.closure X = M₂.closure X
x✝¹ : Set α
x✝ : x✝¹ ⊆ M₁.E
⊢ M₁.Indep x✝¹ ↔ M₂.Indep x✝¹

Tactic:
[

Goal state after:
α : Type u_2
M₁ M₂ : Matroid α
h : ∀ (X : Set α), M₁.closure X = M₂.closure X
x✝¹ : Set α
x✝ : x✝¹ ⊆ M₁.E
⊢ M₁.Indep x✝¹ ↔ M₂.Indep x✝¹
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
a✝ : ι
h : a✝ ∈ t
⊢ {X a✝} ⊆ X '' t

Tactic:
[

Goal state after:
ι : 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
a✝ : ι
h : a✝ ∈ t
⊢ {X a✝} ⊆ X '' t
Module: Mathlib.Combinatorics.Matroid.Closure

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

Tactic:
[

Goal state after:
α : Type u_2
β : Type u_3
M : Matroid β
f : α → β
X I : Set α
hI : (M.comap f).IsBasis' I X
hI' : M.IsBasis' (f '' I) (f '' X)
hIinj : InjOn f I
⊢ (M.comap f).closure X = f ⁻¹' M.closure (f '' X)
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:
[

Goal state after:
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
Module: Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : Type u_4
x : ι → A
S : Type u_5
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✝² : NoZeroDivisors S
inst✝¹ : FaithfulSMul R S
inst✝ : Algebra.IsIntegral R S
⊢ IsTranscendenceBasis R x ↔ IsTranscendenceBasis S x

Tactic:
[

Goal state after:
ι : Type u_1
R : Type u_2
A : Type u_4
x : ι → A
S : Type u_5
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✝² : NoZeroDivisors S
inst✝¹ : FaithfulSMul R S
inst✝ : Algebra.IsIntegral R S
⊢ IsTranscendenceBasis R x ↔ IsTranscendenceBasis S x
Module: Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : Type u_4
x : ι → A
S : Type u_5
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✝² : NoZeroDivisors S
inst✝¹ : FaithfulSMul R S
inst✝ : Algebra.IsAlgebraic R S
⊢ IsTranscendenceBasis R x ↔ IsTranscendenceBasis S x

Tactic:
[

Goal state after:
ι : Type u_1
R : Type u_2
A : Type u_4
x : ι → A
S : Type u_5
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✝² : NoZeroDivisors S
inst✝¹ : FaithfulSMul R S
inst✝ : Algebra.IsAlgebraic R S
⊢ IsTranscendenceBasis R x ↔ IsTranscendenceBasis S x
Module: Mathlib.GroupTheory.GroupAction.FixedPoints

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g h : G
a : α
⊢ a ∈ h • fixedBy α g ↔ a ∈ fixedBy α (h * g * h⁻¹)

Tactic:
[

Goal state after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g h : G
a : α
⊢ a ∈ h • fixedBy α g ↔ a ∈ fixedBy α (h * g * h⁻¹)
Module: Mathlib.GroupTheory.GroupAction.FixedPoints

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
⊢ s ∈ fixedBy (Set α) g ↔ ∀ (x : α), g • x ∈ s ↔ x ∈ s

Tactic:
[

Goal state after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
⊢ s ∈ fixedBy (Set α) g ↔ ∀ (x : α), g • x ∈ s ↔ x ∈ s
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case right
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
i : AlgebraicIndependent R x
w : Set A
i' : AlgebraicIndepOn R _root_.id w
h : range x ⊆ w
p : Surjective fun i ↦ ⟨x i, ⋯⟩
⊢ range x = w

Tactic:
have q := congr_arg (fun s => ((↑) : w → A) '' s) p.range_eq

Goal state after:
case right
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
i : AlgebraicIndependent R x
w : Set A
i' : AlgebraicIndepOn R _root_.id w
h : range x ⊆ w
p : Surjective fun i ↦ ⟨x i, ⋯⟩
q : (Subtype.val '' range fun i ↦ ⟨x i, ⋯⟩) = Subtype.val '' univ
⊢ range x = w
Module: Mathlib.GroupTheory.GroupAction.FixedPoints

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝² : Monoid M
inst✝¹ : MulAction M α
inst✝ : FaithfulSMul M α
m : M
⊢ (∀ (x : α), x ∈ fixedBy α m) ↔ (fun x2 ↦ m • x2) = fun x2 ↦ 1 • x2

Tactic:
[

Goal state after:
α : Type u_1
M : Type u_3
inst✝² : Monoid M
inst✝¹ : MulAction M α
inst✝ : FaithfulSMul M α
m : M
⊢ (∀ (x : α), x ∈ fixedBy α m) ↔ (fun x2 ↦ m • x2) = fun x2 ↦ 1 • x2
Module: Mathlib.GroupTheory.GroupAction.FixingSubgroup

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
m : M
⊢ m ∈ fixingSubgroup M s ↔ s ⊆ fixedBy α m

Tactic:
[

Goal state after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
m : M
⊢ m ∈ fixingSubgroup M s ↔ s ⊆ fixedBy α m
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nonempty ι
⊢ IsTranscendenceBasis R X

Tactic:
nontriviality R; exact .mvPolynomial ι R

Goal state after:
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 (range Subtype.val))) A
⊢ Algebra.IsAlgebraic (↥(adjoin R (range fun i ↦ _root_.id ↑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 (range Subtype.val))) A
⊢ Algebra.IsAlgebraic (↥(adjoin R (range fun i ↦ _root_.id ↑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
B : Set A
⊢ IsTranscendenceBasis R Subtype.val ↔ (indepMatroid R A).matroid.IsBase B

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
B : Set A
⊢ IsTranscendenceBasis R Subtype.val ↔ (indepMatroid R A).matroid.IsBase B
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
⊢ (((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:
matroid_indep_iff,

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
⊢ ((AlgebraicIndepOn R _root_.id s ∧ s ⊆ t) ∧ ∀ x ∉ s, ¬(AlgebraicIndepOn R _root_.id (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✝ : Subsingleton A
s t : Set A
this : Subsingleton R
⊢ (matroid R A).IsBasis s t ↔ s = t

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✝ : Subsingleton A
s t : Set A
this : Subsingleton R
⊢ (matroid R A).IsBasis s t ↔ s = t
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✝ : Subsingleton A
s t : Set A
this : Subsingleton R
⊢ Maximal (fun A_1 ↦ (matroid R A).Indep A_1 ∧ A_1 ⊆ t) s ∧ t ⊆ (matroid R A).E ↔ s = t

Tactic:
matroid_indep_iff,

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✝ : Subsingleton A
s t : Set A
this : Subsingleton R
⊢ Maximal (fun A_1 ↦ AlgebraicIndepOn R _root_.id A_1 ∧ A_1 ⊆ t) s ∧ t ⊆ (matroid R A).E ↔ s = t
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 B : Set A
hB : (matroid R A).IsBasis B s
⊢ (matroid R A).closure s = ↑(algebraicClosure (↥(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 B : Set A
hB : (matroid R A).IsBasis B s
⊢ (matroid R A).closure s = ↑(algebraicClosure (↥(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 : Set A
⊢ (matroid R A).Spanning s ↔ Algebra.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 : Set A
⊢ (matroid R A).Spanning s ↔ Algebra.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✝ : Subsingleton A
s : Set A
⊢ (matroid R A).IsFlat 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✝ : Subsingleton A
s : Set A
⊢ (matroid R A).IsFlat 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✝¹ : FaithfulSMul R A
inst✝ : Subsingleton A
s : Set A
⊢ (matroid R A).closure s = 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✝ : Subsingleton A
s : Set A
⊢ (matroid R A).closure s = 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✝¹ : FaithfulSMul R A
inst✝ : Subsingleton A
s : Set A
⊢ (matroid R A).Spanning s ↔ s = univ

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✝ : Subsingleton A
s : Set A
⊢ (matroid R A).Spanning s ↔ s = univ
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✝¹ : IsDomain A
inst✝ : FaithfulSMul R A
s : Set A
⊢ Algebra.IsAlgebraic (↥(adjoin R s)) A ↔ ∃ t ⊆ s, 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✝¹ : IsDomain A
inst✝ : FaithfulSMul R A
s : Set A
⊢ Algebra.IsAlgebraic (↥(adjoin R s)) A ↔ ∃ t ⊆ s, IsTranscendenceBasis R Subtype.val
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f : F[X]
hf : f ≠ 0
⊢ f.natSepDegree = f.natDegree ↔ f.Separable

Tactic:
[

Goal state after:
F : Type u
inst✝ : Field F
f : F[X]
hf : f ≠ 0
⊢ f.natSepDegree = f.natDegree ↔ f.Separable
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: E : Type v
inst✝¹ : Field E
K : Type w
inst✝ : Field K
f : E[X]
i : E →+* K
x✝ : Algebra E K := i.toAlgebra
⊢ (map i f).natSepDegree = f.natSepDegree

Tactic:
[

Goal state after:
E : Type v
inst✝¹ : Field E
K : Type w
inst✝ : Field K
f : E[X]
i : E →+* K
x✝ : Algebra E K := i.toAlgebra
⊢ (map i f).natSepDegree = f.natSepDegree
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
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
hi : i ∈ s
⊢ v j ∈ (matroid R S).closure (v '' s \ {v j})

Tactic:
← image_singleton,

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
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
hi : i ∈ s
⊢ v j ∈ (matroid R S).closure (v '' s \ v '' {j})
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f : F[X]
n : ℕ
hn : n ≠ 0
⊢ (f ^ n).natSepDegree = f.natSepDegree

Tactic:
[

Goal state after:
F : Type u
inst✝ : Field F
f : F[X]
n : ℕ
hn : n ≠ 0
⊢ (f ^ n).natSepDegree = f.natSepDegree
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case neg
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f * g = 0
⊢ (f * g).natSepDegree ≤ f.natSepDegree + g.natSepDegree

Tactic:
[

Goal state after:
case neg
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f * g = 0
⊢ (f * g).natSepDegree ≤ f.natSepDegree + g.natSepDegree