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

Goal state before:
pp: case refine_2.some
ι : 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
i : ι
⊢ x i = x i

Tactic:
]

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
⊢ Injective ⇑(algebraMap K A)

Tactic:
]

Goal state after:
ι : 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
⊢ Injective ⇑(algebraMap K A)
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
hx : AlgebraicIndependent R x
alg : Algebra.IsAlgebraic R S
t : Set ι
fin : t.Finite
ind : AlgebraicIndependent S fun i ↦ x ↑i
i : ι
hi : i ∉ t
Rt : Subalgebra R A := adjoin R (x '' t)
St : Subalgebra S A := adjoin S (x '' t)
x✝¹ : Algebra ↥Rt ↥St := (Subalgebra.inclusion ⋯).toAlgebra
this✝¹ : IsScalarTower (↥Rt) (↥St) A
this✝ : NoZeroDivisors ↥St
this : NoZeroDivisors ↥Rt
x✝ : ↥St
y : A
hy : y ∈ St
⊢ IsAlgebraic (↥Rt) ((IsScalarTower.toAlgHom (↥Rt) (↥St) A) ⟨y, hy⟩)

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
hx : AlgebraicIndependent R x
alg : Algebra.IsAlgebraic R S
t : Set ι
fin : t.Finite
ind : AlgebraicIndependent S fun i ↦ x ↑i
i : ι
hi : i ∉ t
Rt : Subalgebra R A := adjoin R (x '' t)
St : Subalgebra S A := adjoin S (x '' t)
x✝¹ : Algebra ↥Rt ↥St := (Subalgebra.inclusion ⋯).toAlgebra
this✝¹ : IsScalarTower (↥Rt) (↥St) A
this✝ : NoZeroDivisors ↥St
this : NoZeroDivisors ↥Rt
x✝ : ↥St
y : A
hy : y ∈ St
⊢ IsAlgebraic (↥Rt) ((IsScalarTower.toAlgHom (↥Rt) (↥St) A) ⟨y, hy⟩)
Module: Mathlib.GroupTheory.GroupAction.FixedPoints

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
x✝ : α
⊢ g • x✝ = x✝ ↔ g • x✝ = x✝

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.FixedPoints

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
g : G
⊢ g • a = a ↔ a ∈ fixedBy α g

Tactic:
]

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

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
g : G
⊢ a ∈ fixedBy α g ↔ a ∈ fixedBy α g

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.FixedPoints

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
h : a ∈ fixedBy α g
j : ℤ
⊢ 1 ∣ j

Tactic:
]

Goal state after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
h : a ∈ fixedBy α g
j : ℤ
⊢ 1 ∣ j
Module: Mathlib.GroupTheory.GroupAction.FixedPoints

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M α
m₁ m₂ : M
a : α
h₁ : a ∈ fixedBy α m₁
h₂ : a ∈ fixedBy α m₂
⊢ a = a

Tactic:
]

Goal state after:
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_ss_fixedBy : s ⊆ fixedBy α g
⊢ s ∈ fixedBy (Set α) g⁻¹

Tactic:
]

Goal state after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
s_ss_fixedBy : s ⊆ fixedBy α g
⊢ s ∈ fixedBy (Set α) g⁻¹
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_ss_fixedBy : s ⊆ fixedBy α 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_ss_fixedBy : s ⊆ fixedBy α g
x : α
⊢ g • x ∈ s ↔ x ∈ s
Module: Mathlib.GroupTheory.GroupAction.FixedPoints

Goal state before:
pp: case xs
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
s_ss_fixedBy : s ⊆ fixedBy α g⁻¹
x : α
gxs : g • x ∈ s
⊢ x ∈ s

Tactic:
]

Goal state after:
case xs
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
s_ss_fixedBy : s ⊆ fixedBy α g⁻¹
x : α
gxs : g • x ∈ s
⊢ x ∈ s
Module: Mathlib.GroupTheory.GroupAction.FixedPoints

Goal state before:
pp: case xs
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
s_ss_fixedBy : s ⊆ fixedBy α g⁻¹
x : α
gxs : x ∈ s
⊢ x ∈ s

Tactic:
]

Goal state after:
case xs
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
s_ss_fixedBy : s ⊆ fixedBy α g⁻¹
x : α
gxs : x ∈ s
⊢ x ∈ s
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_subset : (fixedBy α g)ᶜ ⊆ s
⊢ s ∈ fixedBy (Set α) g⁻¹

Tactic:
]

Goal state after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
s_subset : (fixedBy α g)ᶜ ⊆ s
⊢ s ∈ fixedBy (Set α) g⁻¹
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_subset : (fixedBy α g)ᶜ ⊆ s
a : α
⊢ g • a ∈ s ↔ a ∈ s

Tactic:
]

Goal state after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
s_subset : (fixedBy α g)ᶜ ⊆ s
a : α
⊢ g • a ∈ s ↔ a ∈ s
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_subset : (fixedBy α g)ᶜ ⊆ s
a : α
a_fixed : a ∈ fixedBy α g
⊢ a ∈ s ↔ a ∈ s

Tactic:
]

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

Goal state before:
pp: case mp
ι : Type u
R : Type u_1
A : Type w
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
κ : Type w
w : κ → A
i' : AlgebraicIndependent R w
j : ι → κ
i : AlgebraicIndependent R (w ∘ j)
p✝ : IsTranscendenceBasis R (w ∘ j)
p : w '' range j = w '' univ
⊢ Surjective j

Tactic:
]

Goal state after:
case mp
ι : Type u
R : Type u_1
A : Type w
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
κ : Type w
w : κ → A
i' : AlgebraicIndependent R w
j : ι → κ
i : AlgebraicIndependent R (w ∘ j)
p✝ : IsTranscendenceBasis R (w ∘ j)
p : w '' range j = w '' univ
⊢ Surjective j
Module: Mathlib.GroupTheory.GroupAction.FixedPoints

Goal state before:
pp: case mpr
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
s_subset : (fixedBy α g)ᶜ ⊆ s
a : α
a_moved : a ∉ fixedBy α g
a✝ : a ∈ s
⊢ a ∉ fixedBy α g

Tactic:
]

Goal state after:
case mpr
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
s_subset : (fixedBy α g)ᶜ ⊆ s
a : α
a_moved : a ∉ fixedBy α g
a✝ : a ∈ s
⊢ a ∉ fixedBy α g
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
comm : Commute g h
x : α
⊢ g • x = x ↔ g • x = x

Tactic:
]

Goal state after:
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
comm : Commute g h
⊢ (fixedBy α g)ᶜ = (fixedBy α g)ᶜ

Tactic:
]

Goal state after:
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, ⋯⟩
q : (fun x_1 ↦ ↑⟨x x_1, ⋯⟩) '' univ = Subtype.val '' univ
⊢ range x = w

Tactic:
]

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 : (fun x_1 ↦ ↑⟨x x_1, ⋯⟩) '' univ = 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.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
hx : IsTranscendenceBasis R x
a : A
⊢ ¬AlgebraicIndependent R fun o ↦ o.elim a 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
hx : IsTranscendenceBasis R x
a : A
⊢ ¬AlgebraicIndependent R fun o ↦ o.elim a x
Module: Mathlib.GroupTheory.GroupAction.FixedPoints

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : FaithfulSMul G α
g h : G
disjoint : g = 1
comm : Commute g h
⊢ g = 1

Tactic:
]

Goal state after:
α : Type u_1
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : FaithfulSMul G α
g h : G
disjoint : g = 1
comm : Commute g h
⊢ g = 1
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
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent R fun o ↦ o.elim a x
h₁ : range x ⊆ range fun o ↦ o.elim a x
h : range x = range fun o ↦ o.elim a x
⊢ a ∈ range fun o ↦ o.elim a 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
hx : IsTranscendenceBasis R x
a : A
ai : AlgebraicIndependent R fun o ↦ o.elim a x
h₁ : range x ⊆ range fun o ↦ o.elim a x
h : range x = range fun o ↦ o.elim a x
⊢ a ∈ range fun o ↦ o.elim a x
Module: Mathlib.GroupTheory.GroupAction.FixingSubgroup

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Monoid M
inst✝ : MulAction M α
s : Set α
x y : M
hx : x ∈ {ϕ | ∀ (x : ↑s), ϕ • ↑x = ↑x}
hy : y ∈ {ϕ | ∀ (x : ↑s), ϕ • ↑x = ↑x}
z : ↑s
⊢ ↑z = ↑z

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.FixingSubgroup

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
x✝ : M
hx : x✝ ∈ (fixingSubmonoid M s).carrier
z : ↑s
⊢ ↑z = ↑z

Tactic:
]

Goal state after:
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
⊢ (fixedBy α m)ᶜ ⊆ s ↔ (fixedBy α m)ᶜ ⊆ s

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.FixingSubgroup

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
a : α
a_in_s : a ∈ s
b : α
b_in_orbit : b ∈ orbit (↥(fixingSubgroup M sᶜ)) a
g : M
g_fixing : g ∈ fixingSubgroup M sᶜ
g_eq : g • a = b
⊢ b ∈ s

Tactic:
]

Goal state after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
a : α
a_in_s : a ∈ s
b : α
b_in_orbit : b ∈ orbit (↥(fixingSubgroup M sᶜ)) a
g : M
g_fixing : g ∈ fixingSubgroup M sᶜ
g_eq : g • a = b
⊢ b ∈ s
Module: Mathlib.GroupTheory.GroupAction.FixingSubgroup

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
a : α
a_in_s : a ∈ s
b : α
b_in_orbit : b ∈ orbit (↥(fixingSubgroup M sᶜ)) a
g : M
g_fixing : (fixedBy α g)ᶜ ⊆ s
g_eq : g • a = b
⊢ b ∈ s

Tactic:
]

Goal state after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
a : α
a_in_s : a ∈ s
b : α
b_in_orbit : b ∈ orbit (↥(fixingSubgroup M sᶜ)) a
g : M
g_fixing : (fixedBy α g)ᶜ ⊆ s
g_eq : g • a = b
⊢ b ∈ s
Module: Mathlib.GroupTheory.GroupAction.FixingSubgroup

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
a : α
a_in_s : a ∈ s
b : α
b_in_orbit : b ∈ orbit (↥(fixingSubgroup M sᶜ)) a
g : M
g_fixing : (fixedBy α g)ᶜ ⊆ s
g_eq : g • a = b
⊢ a ∈ s

Tactic:
]

Goal state after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
a : α
a_in_s : a ∈ s
b : α
b_in_orbit : b ∈ orbit (↥(fixingSubgroup M sᶜ)) a
g : M
g_fixing : (fixedBy α g)ᶜ ⊆ s
g_eq : g • a = b
⊢ a ∈ 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✝ : Nontrivial R
ind : AlgebraicIndependent R x
alg : Algebra.IsAlgebraic (↥(adjoin R (range x))) A
s : Set A
ind_s : AlgebraicIndepOn R _root_.id s
hxs : range x ⊆ s
hxs' : ¬range x = s
this : ¬s ⊆ range x
a : A
has : a ∈ s
hax : a ∉ range x
⊢ range x = range x

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
ind : AlgebraicIndependent R x
s : Set A
ind_s : AlgebraicIndepOn R _root_.id s
hxs : range x ⊆ s
alg : Algebra.IsAlgebraic (↥(adjoin R (Subtype.val '' range (Set.inclusion hxs)))) A
hxs' : ¬range x = s
this : ¬s ⊆ range x
a : A
has : a ∈ s
hax : a ∉ range x
⊢ False

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
ind : AlgebraicIndependent R x
s : Set A
ind_s : AlgebraicIndepOn R _root_.id s
hxs : range x ⊆ s
alg : Algebra.IsAlgebraic (↥(adjoin R (Subtype.val '' range (Set.inclusion hxs)))) A
hxs' : ¬range x = s
this : ¬s ⊆ range x
a : A
has : a ∈ s
hax : a ∉ range x
⊢ False
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
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 S
inst✝¹ : Algebra.IsAlgebraic S A
inst✝ : FaithfulSMul S A
x : ι → S
hx : IsTranscendenceBasis R x
f : S →ₐ[R] A := IsScalarTower.toAlgHom R S A
⊢ Algebra.IsAlgebraic (↥(Subalgebra.map f (adjoin R (range x)))) A

Tactic:
]

Goal state after:
ι : Type u
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 S
inst✝¹ : Algebra.IsAlgebraic S A
inst✝ : FaithfulSMul S A
x : ι → S
hx : IsTranscendenceBasis R x
f : S →ₐ[R] A := IsScalarTower.toAlgHom R S A
⊢ Algebra.IsAlgebraic (↥(Subalgebra.map f (adjoin R (range x)))) A
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✝¹ : IsDomain S
inst✝ : NoZeroDivisors A
ι : Type u_2
v : ι → A
hv : IsTranscendenceBasis R v
H : ∀ (i : ι), IsAlgebraic S (v i)
Rv : Subalgebra R A := adjoin R (range v)
Sv : Subalgebra S A := adjoin S (range v)
this : Algebra.IsAlgebraic S ↥Sv
⊢ Rv ≤ (IsScalarTower.toAlgHom R S A).range ⊔ adjoin R (range v)

Tactic:
]

Goal state after:
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✝¹ : IsDomain S
inst✝ : NoZeroDivisors A
ι : Type u_2
v : ι → A
hv : IsTranscendenceBasis R v
H : ∀ (i : ι), IsAlgebraic S (v i)
Rv : Subalgebra R A := adjoin R (range v)
Sv : Subalgebra S A := adjoin S (range v)
this : Algebra.IsAlgebraic S ↥Sv
⊢ Rv ≤ (IsScalarTower.toAlgHom R S A).range ⊔ adjoin R (range v)
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ Algebra.IsAlgebraic (↥⊤) (MvPolynomial ι R)

Tactic:
]

Goal state after:
ι : Type u
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ Algebra.IsAlgebraic (↥⊤) (MvPolynomial ι R)
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case inl
ι : Type u
ι' : Type u'
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✝ : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : Nonempty ι
hy : IsTranscendenceBasis S y
h✝ : Subsingleton R
⊢ Nonempty (ι' ⊕ ι)

Tactic:
]

Goal state after:
case inl
ι : Type u
ι' : Type u'
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✝ : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : Nonempty ι
hy : IsTranscendenceBasis S y
h✝ : Subsingleton R
⊢ Nonempty (ι' ⊕ ι)
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
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 A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h✝ : Nontrivial R
⊢ Algebra.IsAlgebraic (↥(adjoin R (range (Sum.elim y (⇑(algebraMap S A) ∘ x))))) A

Tactic:
]

Goal state after:
case inr
ι : Type u
ι' : Type u'
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✝ : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h✝ : Nontrivial R
⊢ Algebra.IsAlgebraic (↥(adjoin R (range (Sum.elim y (⇑(algebraMap S A) ∘ x))))) A
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
ι' : Type u'
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✝ : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h✝ : Nontrivial R
Rx : Subalgebra R S := adjoin R (range x)
Rxy : Subalgebra (↥Rx) A := adjoin (↥Rx) (range y)
⊢ adjoin R (⇑(algebraMap S A) '' range x ∪ range y) = adjoin R (⇑(algebraMap S A) '' range x ∪ range y)

Tactic:
]

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
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 A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h✝ : Nontrivial R
Rx : Subalgebra R S := adjoin R (range x)
Rxy : Subalgebra (↥Rx) A := adjoin (↥Rx) (range y)
⊢ Algebra.IsAlgebraic (↥(Subalgebra.restrictScalars R Rxy)) A

Tactic:
]

Goal state after:
case inr
ι : Type u
ι' : Type u'
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✝ : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h✝ : Nontrivial R
Rx : Subalgebra R S := adjoin R (range x)
Rxy : Subalgebra (↥Rx) A := adjoin (↥Rx) (range y)
⊢ Algebra.IsAlgebraic (↥(Subalgebra.restrictScalars R Rxy)) 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
hx : IsTranscendenceBasis R x
x✝ : IsEmpty ι
this : Algebra.IsAlgebraic (↥⊥) A
⊢ Algebra.IsAlgebraic R A

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
hx : IsTranscendenceBasis R x
x✝ : IsEmpty ι
this : Algebra.IsAlgebraic (↥⊥) A
⊢ Algebra.IsAlgebraic 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
hx : IsTranscendenceBasis R x
⊢ ¬Algebra.IsAlgebraic R A ↔ ¬Algebra.IsAlgebraic R A

Tactic:
]

Goal state after:
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
B_base : IsTranscendenceBasis R Subtype.val
h : ∀ x ∈ B \ I, ¬AlgebraicIndepOn R _root_.id (insert x I)
⊢ IsTranscendenceBasis R Subtype.val

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
B_base : IsTranscendenceBasis R Subtype.val
h : ∀ x ∈ B \ I, ¬AlgebraicIndepOn R _root_.id (insert x I)
⊢ IsTranscendenceBasis R Subtype.val
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case inl
ι : 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
B_base : Nonempty { x // x ∈ B }
h : ∀ x ∈ B \ I, ¬AlgebraicIndepOn R _root_.id (insert x I)
h✝ : Subsingleton R
⊢ Nonempty { x // x ∈ I }

Tactic:
]

Goal state after:
case inl
ι : 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
B_base : Nonempty { x // x ∈ B }
h : ∀ x ∈ B \ I, ¬AlgebraicIndepOn R _root_.id (insert x I)
h✝ : Subsingleton R
⊢ Nonempty { x // x ∈ I }