mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.Differential.Liouville

Goal state before:
pp: case inj
F : Type u_1
K : Type u_2
inst✝¹² : Field F
inst✝¹¹ : Field K
inst✝¹⁰ : Differential F
inst✝⁹ : Differential K
inst✝⁸ : Algebra F K
inst✝⁷ : DifferentialAlgebra F K
A : Type u_3
inst✝⁶ : Field A
inst✝⁵ : Algebra K A
inst✝⁴ : Algebra F A
inst✝³ : Differential A
inst✝² : IsScalarTower F K A
inst✝¹ : ContainConstants F K
inst1 : IsLiouville F K
inst2 : IsLiouville K A
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc✝ : ∀ (x : ι), (c x)′ = 0
u : ι → A
v : A
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
ι₀ : Type
w✝ : Fintype ι₀
c₀✝ : ι₀ → K
hc₀ : ∀ (x : ι₀), (c₀✝ x)′ = 0
u₀ : ι₀ → K
v₀ : K
h₀ : ↑a = ∑ x, c₀✝ x * logDeriv (u₀ x) + v₀′
c₀ : ι₀ → F
hc : ∀ (x : ι₀), (algebraMap F K) (c₀ x) = c₀✝ x
x✝ : ι₀
⊢ Function.Injective Algebra.cast

Tactic:
·

Goal state after:
case inj
F : Type u_1
K : Type u_2
inst✝¹² : Field F
inst✝¹¹ : Field K
inst✝¹⁰ : Differential F
inst✝⁹ : Differential K
inst✝⁸ : Algebra F K
inst✝⁷ : DifferentialAlgebra F K
A : Type u_3
inst✝⁶ : Field A
inst✝⁵ : Algebra K A
inst✝⁴ : Algebra F A
inst✝³ : Differential A
inst✝² : IsScalarTower F K A
inst✝¹ : ContainConstants F K
inst1 : IsLiouville F K
inst2 : IsLiouville K A
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc✝ : ∀ (x : ι), (c x)′ = 0
u : ι → A
v : A
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
ι₀ : Type
w✝ : Fintype ι₀
c₀✝ : ι₀ → K
hc₀ : ∀ (x : ι₀), (c₀✝ x)′ = 0
u₀ : ι₀ → K
v₀ : K
h₀ : ↑a = ∑ x, c₀✝ x * logDeriv (u₀ x) + v₀′
c₀ : ι₀ → F
hc : ∀ (x : ι₀), (algebraMap F K) (c₀ x) = c₀✝ x
x✝ : ι₀
⊢ Function.Injective Algebra.cast
Module: Mathlib.FieldTheory.Differential.Liouville

Goal state before:
pp: case refine_1
F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Differential F
inst✝⁶ : Differential K
inst✝⁵ : Algebra F K
inst✝⁴ : DifferentialAlgebra F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
this : CharZero K
c₀ : ι → F := fun i ↦ c i / ↑(Fintype.card Gal(K/F))
u₁ : ι → K := fun i ↦ ∏ x, x (u i)
ffb : fixedField ⊤ = ⊥
u₀ : ι → F
hu₀ : ∀ (i : ι), (algebraMap F K) (u₀ i) = u₁ i
v₁ : K := (∑ x, x v) / ↑(Fintype.card Gal(K/F))
v₀ : F
hv₀ : (algebraMap F K) v₀ = v₁
⊢ ∀ (x : ι), (c₀ x)′ = 0

pp: case refine_2
F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Differential F
inst✝⁶ : Differential K
inst✝⁵ : Algebra F K
inst✝⁴ : DifferentialAlgebra F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
this : CharZero K
c₀ : ι → F := fun i ↦ c i / ↑(Fintype.card Gal(K/F))
u₁ : ι → K := fun i ↦ ∏ x, x (u i)
ffb : fixedField ⊤ = ⊥
u₀ : ι → F
hu₀ : ∀ (i : ι), (algebraMap F K) (u₀ i) = u₁ i
v₁ : K := (∑ x, x v) / ↑(Fintype.card Gal(K/F))
v₀ : F
hv₀ : (algebraMap F K) v₀ = v₁
⊢ a = ∑ x, c₀ x * logDeriv (u₀ x) + v₀′

Tactic:
·

Goal state after:
case refine_1
F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Differential F
inst✝⁶ : Differential K
inst✝⁵ : Algebra F K
inst✝⁴ : DifferentialAlgebra F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
this : CharZero K
c₀ : ι → F := fun i ↦ c i / ↑(Fintype.card Gal(K/F))
u₁ : ι → K := fun i ↦ ∏ x, x (u i)
ffb : fixedField ⊤ = ⊥
u₀ : ι → F
hu₀ : ∀ (i : ι), (algebraMap F K) (u₀ i) = u₁ i
v₁ : K := (∑ x, x v) / ↑(Fintype.card Gal(K/F))
v₀ : F
hv₀ : (algebraMap F K) v₀ = v₁
⊢ ∀ (x : ι), (c₀ x)′ = 0
Module: Mathlib.FieldTheory.Differential.Liouville

Goal state before:
pp: case refine_2
F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Differential F
inst✝⁶ : Differential K
inst✝⁵ : Algebra F K
inst✝⁴ : DifferentialAlgebra F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
this : CharZero K
c₀ : ι → F := fun i ↦ c i / ↑(Fintype.card Gal(K/F))
u₁ : ι → K := fun i ↦ ∏ x, x (u i)
ffb : fixedField ⊤ = ⊥
u₀ : ι → F
hu₀ : ∀ (i : ι), (algebraMap F K) (u₀ i) = u₁ i
v₁ : K := (∑ x, x v) / ↑(Fintype.card Gal(K/F))
v₀ : F
hv₀ : (algebraMap F K) v₀ = v₁
⊢ a = ∑ x, c₀ x * logDeriv (u₀ x) + v₀′

Tactic:
·

Goal state after:
case refine_2
F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Differential F
inst✝⁶ : Differential K
inst✝⁵ : Algebra F K
inst✝⁴ : DifferentialAlgebra F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
this : CharZero K
c₀ : ι → F := fun i ↦ c i / ↑(Fintype.card Gal(K/F))
u₁ : ι → K := fun i ↦ ∏ x, x (u i)
ffb : fixedField ⊤ = ⊥
u₀ : ι → F
hu₀ : ∀ (i : ι), (algebraMap F K) (u₀ i) = u₁ i
v₁ : K := (∑ x, x v) / ↑(Fintype.card Gal(K/F))
v₀ : F
hv₀ : (algebraMap F K) v₀ = v₁
⊢ a = ∑ x, c₀ x * logDeriv (u₀ x) + v₀′
Module: Mathlib.FieldTheory.Galois.NormalBasis

Goal state before:
pp: case inl
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
h : Finite K
⊢ ∃ x, LinearIndependent K fun σ ↦ σ x

pp: case inr
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
h : Infinite K
⊢ ∃ x, LinearIndependent K fun σ ↦ σ x

Tactic:
·

Goal state after:
case inl
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
h : Finite K
⊢ ∃ x, LinearIndependent K fun σ ↦ σ x
Module: Mathlib.FieldTheory.Differential.Liouville

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Differential F
inst✝⁶ : Differential K
inst✝⁵ : Algebra F K
inst✝⁴ : DifferentialAlgebra F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
this : CharZero K
ffb : fixedField ⊤ = ⊥
⊢ (algebraMap F K) a * ↑(Fintype.card Gal(K/F)) = ∑ x, ↑a

pp: F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Differential F
inst✝⁶ : Differential K
inst✝⁵ : Algebra F K
inst✝⁴ : DifferentialAlgebra F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
this : CharZero K
ffb : fixedField ⊤ = ⊥
⊢ ∑ x, ↑a = ∑ x, (∑ x_1, ↑(c x_1) * logDeriv (x (u x_1)) + (x v)′)

Tactic:
·

Goal state after:
F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Differential F
inst✝⁶ : Differential K
inst✝⁵ : Algebra F K
inst✝⁴ : DifferentialAlgebra F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
this : CharZero K
ffb : fixedField ⊤ = ⊥
⊢ (algebraMap F K) a * ↑(Fintype.card Gal(K/F)) = ∑ x, ↑a
Module: Mathlib.FieldTheory.Galois.NormalBasis

Goal state before:
pp: case inr
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
h : Infinite K
⊢ ∃ x, LinearIndependent K fun σ ↦ σ x

Tactic:
·

Goal state after:
case inr
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
h : Infinite K
⊢ ∃ x, LinearIndependent K fun σ ↦ σ x
Module: Mathlib.FieldTheory.Differential.Liouville

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Differential F
inst✝⁶ : Differential K
inst✝⁵ : Algebra F K
inst✝⁴ : DifferentialAlgebra F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
this : CharZero K
ffb : fixedField ⊤ = ⊥
⊢ ∑ x, ↑a = ∑ x, (∑ x_1, ↑(c x_1) * logDeriv (x (u x_1)) + (x v)′)

Tactic:
·

Goal state after:
F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Differential F
inst✝⁶ : Differential K
inst✝⁵ : Algebra F K
inst✝⁴ : DifferentialAlgebra F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
this : CharZero K
ffb : fixedField ⊤ = ⊥
⊢ ∑ x, ↑a = ∑ x, (∑ x_1, ↑(c x_1) * logDeriv (x (u x_1)) + (x v)′)
Module: Mathlib.FieldTheory.Differential.Liouville

Goal state before:
pp: case e'_5
F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Differential F
inst✝⁶ : Differential K
inst✝⁵ : Algebra F K
inst✝⁴ : DifferentialAlgebra F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
this : CharZero K
ffb : fixedField ⊤ = ⊥
e : Gal(K/F)
h : (algebraMap F K) a = ∑ x, (algebraMap F K) (c x) * e (logDeriv (u x)) + e v′
⊢ ∑ x, ↑(c x) * logDeriv (e (u x)) = ∑ x, (algebraMap F K) (c x) * e (logDeriv (u x))

pp: case e'_6
F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Differential F
inst✝⁶ : Differential K
inst✝⁵ : Algebra F K
inst✝⁴ : DifferentialAlgebra F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
this : CharZero K
ffb : fixedField ⊤ = ⊥
e : Gal(K/F)
h : (algebraMap F K) a = ∑ x, (algebraMap F K) (c x) * e (logDeriv (u x)) + e v′
⊢ (e v)′ = e v′

Tactic:
·

Goal state after:
case e'_5
F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Differential F
inst✝⁶ : Differential K
inst✝⁵ : Algebra F K
inst✝⁴ : DifferentialAlgebra F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
this : CharZero K
ffb : fixedField ⊤ = ⊥
e : Gal(K/F)
h : (algebraMap F K) a = ∑ x, (algebraMap F K) (c x) * e (logDeriv (u x)) + e v′
⊢ ∑ x, ↑(c x) * logDeriv (e (u x)) = ∑ x, (algebraMap F K) (c x) * e (logDeriv (u x))
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: case inl
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
ih : (y : (Module.rank F E).ord.ToType) → y < i → (Module.rank F E).ord.ToType
s : Set E := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this✝¹ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this✝ : Module.rank F ↥(adjoin F s) = Module.rank F ↥⊤
this : #↑(Iio i) < Module.rank F E
eq : ℵ₀ = Module.rank F E
⊢ Module.rank F ↥(adjoin F s) < Module.rank F E

pp: case inr
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
ih : (y : (Module.rank F E).ord.ToType) → y < i → (Module.rank F E).ord.ToType
s : Set E := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this✝¹ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this✝ : Module.rank F ↥(adjoin F s) = Module.rank F ↥⊤
this : #↑(Iio i) < Module.rank F E
lt : ℵ₀ < Module.rank F E
⊢ Module.rank F ↥(adjoin F s) < Module.rank F E

Tactic:
·

Goal state after:
case inl
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
ih : (y : (Module.rank F E).ord.ToType) → y < i → (Module.rank F E).ord.ToType
s : Set E := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this✝¹ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this✝ : Module.rank F ↥(adjoin F s) = Module.rank F ↥⊤
this : #↑(Iio i) < Module.rank F E
eq : ℵ₀ = Module.rank F E
⊢ Module.rank F ↥(adjoin F s) < Module.rank F E
Module: Mathlib.FieldTheory.Differential.Liouville

Goal state before:
pp: case e'_6
F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Differential F
inst✝⁶ : Differential K
inst✝⁵ : Algebra F K
inst✝⁴ : DifferentialAlgebra F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
this : CharZero K
ffb : fixedField ⊤ = ⊥
e : Gal(K/F)
h : (algebraMap F K) a = ∑ x, (algebraMap F K) (c x) * e (logDeriv (u x)) + e v′
⊢ (e v)′ = e v′

Tactic:
·

Goal state after:
case e'_6
F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Differential F
inst✝⁶ : Differential K
inst✝⁵ : Algebra F K
inst✝⁴ : DifferentialAlgebra F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
this : CharZero K
ffb : fixedField ⊤ = ⊥
e : Gal(K/F)
h : (algebraMap F K) a = ∑ x, (algebraMap F K) (c x) * e (logDeriv (u x)) + e v′
⊢ (e v)′ = e v′
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: case inr
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
ih : (y : (Module.rank F E).ord.ToType) → y < i → (Module.rank F E).ord.ToType
s : Set E := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this✝¹ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this✝ : Module.rank F ↥(adjoin F s) = Module.rank F ↥⊤
this : #↑(Iio i) < Module.rank F E
lt : ℵ₀ < Module.rank F E
⊢ Module.rank F ↥(adjoin F s) < Module.rank F E

Tactic:
·

Goal state after:
case inr
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
ih : (y : (Module.rank F E).ord.ToType) → y < i → (Module.rank F E).ord.ToType
s : Set E := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this✝¹ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this✝ : Module.rank F ↥(adjoin F s) = Module.rank F ↥⊤
this : #↑(Iio i) < Module.rank F E
lt : ℵ₀ < Module.rank F E
⊢ Module.rank F ↥(adjoin F s) < Module.rank F E
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: case inl
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i j : (Module.rank F E).ord.ToType
h : i < j
least : ∀ (i : (Module.rank F E).ord.ToType), IsLeast {k | b k ∉ adjoin F (⇑b ∘ φ '' Iio i)} (φ i)
this : φ j ≤ φ i
eq : φ j = φ i
⊢ False

pp: case inr
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i j : (Module.rank F E).ord.ToType
h : i < j
least : ∀ (i : (Module.rank F E).ord.ToType), IsLeast {k | b k ∉ adjoin F (⇑b ∘ φ '' Iio i)} (φ i)
this : φ j ≤ φ i
lt : φ j < φ i
⊢ False

Tactic:
·

Goal state after:
case inl
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i j : (Module.rank F E).ord.ToType
h : i < j
least : ∀ (i : (Module.rank F E).ord.ToType), IsLeast {k | b k ∉ adjoin F (⇑b ∘ φ '' Iio i)} (φ i)
this : φ j ≤ φ i
eq : φ j = φ i
⊢ False
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: case inr
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i j : (Module.rank F E).ord.ToType
h : i < j
least : ∀ (i : (Module.rank F E).ord.ToType), IsLeast {k | b k ∉ adjoin F (⇑b ∘ φ '' Iio i)} (φ i)
this : φ j ≤ φ i
lt : φ j < φ i
⊢ False

Tactic:
·

Goal state after:
case inr
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i j : (Module.rank F E).ord.ToType
h : i < j
least : ∀ (i : (Module.rank F E).ord.ToType), IsLeast {k | b k ∉ adjoin F (⇑b ∘ φ '' Iio i)} (φ i)
this : φ j ≤ φ i
lt : φ j < φ i
⊢ False
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: case refine_1
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
⊢ ⇑b ∘ φ '' Iio i ⊆ ⇑b '' Iio (φ i)

pp: case refine_2
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
⊢ ⇑b '' Iio (φ i) ⊆ ↑(adjoin F (⇑b ∘ φ '' Iio i))

Tactic:
·

Goal state after:
case refine_1
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
⊢ ⇑b ∘ φ '' Iio i ⊆ ⇑b '' Iio (φ i)
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: case refine_2
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
⊢ ⇑b '' Iio (φ i) ⊆ ↑(adjoin F (⇑b ∘ φ '' Iio i))

Tactic:
·

Goal state after:
case refine_2
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
⊢ ⇑b '' Iio (φ i) ⊆ ↑(adjoin F (⇑b ∘ φ '' Iio i))
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
⊢ range ⇑b ⊆ ↑(⨆ i, adjoin F (⇑b '' Iio (φ i)))

Tactic:
rintro _ ⟨i, rfl⟩

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
⊢ b i ∈ ↑(⨆ i, adjoin F (⇑b '' Iio (φ i)))
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: case top
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : WithTop (Module.rank F E).ord.ToType
h : i < ⊤
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

pp: case coe
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : WithTop (Module.rank F E).ord.ToType
a✝ : (Module.rank F E).ord.ToType
h : i < ↑a✝
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
·

Goal state after:
case top
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : WithTop (Module.rank F E).ord.ToType
h : i < ⊤
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: case coe
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : WithTop (Module.rank F E).ord.ToType
a✝ : (Module.rank F E).ord.ToType
h : i < ↑a✝
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
·

Goal state after:
case coe
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : WithTop (Module.rank F E).ord.ToType
a✝ : (Module.rank F E).ord.ToType
h : i < ↑a✝
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: case top
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
hi : IsSuccPrelimit ⊤
⊢ ⨆ j, filtration ↑j = filtration ⊤

pp: case coe
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
a✝ : (Module.rank F E).ord.ToType
hi : IsSuccPrelimit ↑a✝
⊢ ⨆ j, filtration ↑j = filtration ↑a✝

Tactic:
·

Goal state after:
case top
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
hi : IsSuccPrelimit ⊤
⊢ ⨆ j, filtration ↑j = filtration ⊤
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: case top
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
hi✝ : IsSuccPrelimit ⊤
hi : ¬Nonempty ↑(Iio ⊤)
⊢ filtration ⊤ = ⊥

pp: case coe
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
a✝ : (Module.rank F E).ord.ToType
hi✝ : IsSuccPrelimit ↑a✝
hi : ¬Nonempty ↑(Iio ↑a✝)
⊢ filtration ↑a✝ = ⊥

Tactic:
·

Goal state after:
case top
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
hi✝ : IsSuccPrelimit ⊤
hi : ¬Nonempty ↑(Iio ⊤)
⊢ filtration ⊤ = ⊥
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: case coe
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
a✝ : (Module.rank F E).ord.ToType
hi✝ : IsSuccPrelimit ↑a✝
hi : ¬Nonempty ↑(Iio ↑a✝)
⊢ filtration ↑a✝ = ⊥

Tactic:
·

Goal state after:
case coe
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
a✝ : (Module.rank F E).ord.ToType
hi✝ : IsSuccPrelimit ↑a✝
hi : ¬Nonempty ↑(Iio ↑a✝)
⊢ filtration ↑a✝ = ⊥