mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: case h
M : Type w
A : Set M
L : Language
L' : Language
inst✝¹ : L.Structure M
inst✝ : L'.Structure M
β : Type u_1
x : L[[↑A]].Term β
c : {n : ℕ} → L[[↑A]].Functions n → L'[[↑A]].Term (Fin n)
hc : ∀ {n : ℕ} (g : L[[↑A]].Functions n) (x : Fin n → M), Term.realize x g.term = Term.realize x (c g)
⊢ (fun v ↦ Term.realize v x) = fun v ↦ Term.realize v (x.substFunc fun {n} ↦ c)

Tactic:
[

Goal state after:
case h
M : Type w
A : Set M
L : Language
L' : Language
inst✝¹ : L.Structure M
inst✝ : L'.Structure M
β : Type u_1
x : L[[↑A]].Term β
c : {n : ℕ} → L[[↑A]].Functions n → L'[[↑A]].Term (Fin n)
hc : ∀ {n : ℕ} (g : L[[↑A]].Functions n) (x : Fin n → M), Term.realize x g.term = Term.realize x (c g)
⊢ (fun v ↦ Term.realize v x) = fun v ↦ Term.realize v (x.substFunc fun {n} ↦ c)
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: case refine_2
p : ℕ
κ : Cardinal.{u_2}
hκ : ℵ₀ < κ
M : Type u_2
struc✝¹ : Language.ring.Structure M
is_model✝¹ : M ⊨ Theory.ACF p
nonempty'✝¹ : Nonempty M
N : Type u_2
struc✝ : Language.ring.Structure N
is_model✝ : N ⊨ Theory.ACF p
nonempty'✝ : Nonempty N
hM : #↑{ Carrier := M, struc := struc✝¹, is_model := is_model✝¹, nonempty' := nonempty'✝¹ } = κ
hN : #↑{ Carrier := N, struc := struc✝, is_model := is_model✝, nonempty' := nonempty'✝ } = κ
x✝³ : Field M := fieldOfModelACF p M
this✝⁴ : M ⊨ Theory.field
x✝² : CompatibleRing M := compatibleRingOfModelField M
this✝³ : IsAlgClosed M
this✝² : CharP M p
x✝¹ : Field N := fieldOfModelACF p N
this✝¹ : N ⊨ Theory.field
x✝ : CompatibleRing N := compatibleRingOfModelField N
this✝ : IsAlgClosed N
this : CharP N p
⊢ κ = #↑{ Carrier := N, struc := struc✝, is_model := is_model✝, nonempty' := nonempty'✝ }

Tactic:
hN

Goal state after:
case refine_2
p : ℕ
κ : Cardinal.{u_2}
hκ : ℵ₀ < κ
M : Type u_2
struc✝¹ : Language.ring.Structure M
is_model✝¹ : M ⊨ Theory.ACF p
nonempty'✝¹ : Nonempty M
N : Type u_2
struc✝ : Language.ring.Structure N
is_model✝ : N ⊨ Theory.ACF p
nonempty'✝ : Nonempty N
hM : #↑{ Carrier := M, struc := struc✝¹, is_model := is_model✝¹, nonempty' := nonempty'✝¹ } = κ
hN : #↑{ Carrier := N, struc := struc✝, is_model := is_model✝, nonempty' := nonempty'✝ } = κ
x✝³ : Field M := fieldOfModelACF p M
this✝⁴ : M ⊨ Theory.field
x✝² : CompatibleRing M := compatibleRingOfModelField M
this✝³ : IsAlgClosed M
this✝² : CharP M p
x✝¹ : Field N := fieldOfModelACF p N
this✝¹ : N ⊨ Theory.field
x✝ : CompatibleRing N := compatibleRingOfModelField N
this✝ : IsAlgClosed N
this : CharP N p
⊢ κ = κ
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
φ : L.Sentence
⊢ φ ∈ L.completeTheory M ∨ Formula.not φ ∈ L.completeTheory M

Tactic:
[

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
φ : L.Sentence
⊢ φ ∈ L.completeTheory M ∨ Formula.not φ ∈ L.completeTheory M
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
κ : Cardinal.{w}
T : L.Theory
h : κ.Categorical T
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
hS : T.IsSatisfiable
hT : ∀ (M : T.ModelType), Infinite ↑M
φ : L.Sentence
w✝ : T.ModelType
h✝ : #↑w✝ = κ
MF : T.ModelType
hMF : ¬↑MF ⊨ φ
MT : T.ModelType
hMT : ↑MT ⊨ φ
⊢ False

Tactic:
refine hMF ?_

Goal state after:
L : Language
κ : Cardinal.{w}
T : L.Theory
h : κ.Categorical T
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
hS : T.IsSatisfiable
hT : ∀ (M : T.ModelType), Infinite ↑M
φ : L.Sentence
w✝ : T.ModelType
h✝ : #↑w✝ = κ
MF : T.ModelType
hMF : ¬↑MF ⊨ φ
MT : T.ModelType
hMT : ↑MT ⊨ φ
⊢ ↑MF ⊨ φ
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: κ : Cardinal.{w}
T : Language.empty.Theory
M N : T.ModelType
hM : #↑M = κ
hN : #↑N = κ
⊢ lift.{w, w} κ = lift.{w, w} #↑N

Tactic:
hN

Goal state after:
κ : Cardinal.{w}
T : Language.empty.Theory
M N : T.ModelType
hM : #↑M = κ
hN : #↑N = κ
⊢ lift.{w, w} κ = lift.{w, w} κ
Module: Mathlib.LinearAlgebra.FreeAlgebra

Goal state before:
pp: case inr
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : Set S
h✝ : Nontrivial R
⊢ lift.{v, max u v} (Module.rank R (FreeAlgebra R { x // x ∈ s })) ≤ lift.{max u v, v} (max #↑s ℵ₀)

Tactic:
rw [FreeAlgebra.rank_eq, lift_id'.{v, u}, lift_umax.{v, u}, lift_le, max_comm]

Goal state after:
case inr
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : Set S
h✝ : Nontrivial R
⊢ #(List { x // x ∈ s }) ≤ max ℵ₀ #↑s
Module: Mathlib.GroupTheory.OreLocalization.Cardinality

Goal state before:
pp: case h.refine_2
R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite ↥S
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i = s ^ j
hlt : j < i
⊢ ↑(s ^ j) * ↑s = ↑(s ^ (j + 1)) * ↑1

Tactic:
[

Goal state after:
case h.refine_2
R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite ↥S
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i = s ^ j
hlt : j < i
⊢ ↑(s ^ j) * ↑s = ↑(s ^ (j + 1)) * ↑1
Module: Mathlib.GroupTheory.OreLocalization.Cardinality

Goal state before:
pp: case h.refine_2
R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite X
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i • x = s ^ j • x
hlt : j < i
⊢ ↑(s ^ j) * ↑s = ↑(s ^ (j + 1)) * ↑1

Tactic:
[

Goal state after:
case h.refine_2
R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite X
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i • x = s ^ j • x
hlt : j < i
⊢ ↑(s ^ j) * ↑s = ↑(s ^ (j + 1)) * ↑1
Module: Mathlib.GroupTheory.OreLocalization.Cardinality

Goal state before:
pp: case inl
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
h✝ : Finite X
⊢ #(OreLocalization S X) ≤ max (lift.{v, u} #↥S) (lift.{u, v} #X)

pp: case inr
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
h✝ : Infinite X
⊢ #(OreLocalization S X) ≤ max (lift.{v, u} #↥S) (lift.{u, v} #X)

Tactic:
· have := lift_mk_le_lift_mk_of_surjective (oreDiv_one_surjective_of_finite_right S X)
    rw [lift_umax.{v, u}, lift_id'] at this
    exact le_max_of_le_right this

Goal state after:
case inr
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
h✝ : Infinite X
⊢ #(OreLocalization S X) ≤ max (lift.{v, u} #↥S) (lift.{u, v} #X)
Module: Mathlib.GroupTheory.OreLocalization.Cardinality

Goal state before:
pp: R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
h✝¹ : Infinite X
h✝ : Infinite ↥S
⊢ lift.{v, u} #↥S * lift.{u, v} #X = max (lift.{v, u} #↥S) (lift.{u, v} #X)

Tactic:
refine mul_eq_max ?_ ?_ <;> simp

Goal state after:
Module: Mathlib.GroupTheory.OreLocalization.Cardinality

Goal state before:
pp: R : Type u
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
⊢ max (lift.{u, u} #↥S) (lift.{u, u} #R) = #R

Tactic:
[

Goal state after:
R : Type u
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
⊢ max (lift.{u, u} #↥S) (lift.{u, u} #R) = #R
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: a b : Cardinal.{u_1}
hb : b ≠ 0
hdiv : a ∣ b
⊢ a ≤ b

Tactic:
by
  obtain ⟨b, rfl⟩ := hdiv
  apply le_mul_right
  simp_all

Goal state after:
Module: Mathlib.FieldTheory.Differential.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
a b : R
ha : a ≠ 0
hb : b ≠ 0
⊢ logDeriv (a * b) = logDeriv a + logDeriv b

Tactic:
unfold logDeriv
  simp [field]
  ring

Goal state after:
Module: Mathlib.FieldTheory.FinTrdeg

Goal state before:
pp: case mp
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E : IntermediateField K L
fg : E.FG
alg : Algebra.IsAlgebraic (↥E) L
⊢ Algebra.trdeg K L < Cardinal.aleph0

Tactic:
rw [← trdeg_add_eq K E, trdeg_eq_zero_iff.2 alg, add_zero]

Goal state after:
case mp
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E : IntermediateField K L
fg : E.FG
alg : Algebra.IsAlgebraic (↥E) L
⊢ Algebra.trdeg K ↥E < Cardinal.aleph0
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: case C
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
a : ZMod p
⊢ C a ^ p = C a

Tactic:
← C_pow,

Goal state after:
case C
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
a : ZMod p
⊢ C (a ^ p) = C a
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ Multiset.count n (∑ s, (Fintype.card K - 1) • {s}) = Fintype.card K - 1

Tactic:
[

Goal state after:
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ Multiset.count n (∑ s, (Fintype.card K - 1) • {s}) = Fintype.card K - 1
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: case refine_1
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ ∀ b ∈ Finset.univ, b ≠ n → (Fintype.card K - 1) * Multiset.count n {b} = 0

pp: case refine_2
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ n ∉ Finset.univ → (Fintype.card K - 1) * Multiset.count n {n} = 0

Tactic:
· intro b _ ne
      simp [ne, eqComm]

Goal state after:
case refine_2
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ n ∉ Finset.univ → (Fintype.card K - 1) * Multiset.count n {n} = 0
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: case intro.refine_2
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
e : (σ → K) → K
x✝ : e ∈ ⊤
⊢ (evalₗ K σ) (∑ n, e n • indicator n) = e

Tactic:
ext n
    simp only [evalₗ_apply, map_sum, smul_eval]
    rw [Finset.sum_eq_single n] <;>
      aesop (add simp [eval_indicator_apply_eq_zero, eval_indicator_apply_eq_one, eq_comm])

Goal state after:
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
B : IntermediateField F K
inst✝¹ : FiniteDimensional F ↥B
inst : IsLiouville F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → ↥B
v : ↥B
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
⊢ ↑a = ∑ x, ↑(c x) * (algebraMap (↥B) K) (logDeriv (u x)) + (algebraMap (↥B) K) 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
B : IntermediateField F K
inst✝¹ : FiniteDimensional F ↥B
inst : IsLiouville F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → ↥B
v : ↥B
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
⊢ ↑a = ∑ x, ↑(c x) * (algebraMap (↥B) K) (logDeriv (u x)) + (algebraMap (↥B) K) v′
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
c₀ : ι → F := fun i ↦ c i / ↑(Fintype.card Gal(K/F))
u₁ : ι → K := fun i ↦ ∏ x, x (u i)
this : ∀ (i : ι), u₁ i ∈ fixedField ⊤
ffb : fixedField ⊤ = ⊥
⊢ ∃ ι₀ x c₀, ∃ (_ : ∀ (x : ι₀), (c₀ x)′ = 0), ∃ u₀ v₀, a = ∑ x, c₀ x * logDeriv (u₀ 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
c₀ : ι → F := fun i ↦ c i / ↑(Fintype.card Gal(K/F))
u₁ : ι → K := fun i ↦ ∏ x, x (u i)
this : ∀ (i : ι), u₁ i ∈ fixedField ⊤
ffb : fixedField ⊤ = ⊥
⊢ ∃ ι₀ x c₀, ∃ (_ : ∀ (x : ι₀), (c₀ x)′ = 0), ∃ u₀ v₀, a = ∑ x, c₀ x * logDeriv (u₀ x) + v₀′
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₁
⊢ (algebraMap F K) a = ∑ x, (algebraMap F K) (c₀ x) * logDeriv (u₁ x) + v₁′

Tactic:
unfold u₁ v₁ c₀

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₁
⊢ (algebraMap F K) a =
    ∑ x, (algebraMap F K) (c x / ↑(Fintype.card Gal(K/F))) * logDeriv (∏ x_1, x_1 (u x)) +
      ((∑ x, x v) / ↑(Fintype.card Gal(K/F)))′
Module: Mathlib.FieldTheory.Galois.NormalBasis

Goal state before:
pp: case e'_4
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Finite L
this✝ : Finite K
this : Fintype K
x : L
hx :
  Ideal.span {X ^ finrank K L - 1} =
    (toSpanSingleton K[X] (AEval' (frobeniusAlgHom K L).toLinearMap)
        ((AEval'.of (frobeniusAlgHom K L).toLinearMap) x)).ker
e_1✝ : Fin (X ^ finrank K L - C 1).natDegree = Fin (AdjoinRoot.powerBasis ⋯).dim
i : Fin (X ^ finrank K L - C 1).natDegree
⊢ ((fun σ ↦ σ x) ∘ ⇑((finCongr ⋯).trans (Equiv.ofBijective (fun n ↦ frobeniusAlgEquivOfAlgebraic K L ^ ↑n) ⋯))) i =
    (⇑(↑(AEval'.of (frobeniusAlgHom K L).toLinearMap).symm ∘ₗ
            ↑K
              (liftQ (Ideal.span {X ^ finrank K L - 1})
                (toSpanSingleton K[X] (AEval' (frobeniusAlgHom K L).toLinearMap)
                  ((AEval'.of (frobeniusAlgHom K L).toLinearMap) x))
                ⋯)) ∘
        ⇑(AdjoinRoot.powerBasis ⋯).basis)
      i

Tactic:
[

Goal state after:
case e'_4
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Finite L
this✝ : Finite K
this : Fintype K
x : L
hx :
  Ideal.span {X ^ finrank K L - 1} =
    (toSpanSingleton K[X] (AEval' (frobeniusAlgHom K L).toLinearMap)
        ((AEval'.of (frobeniusAlgHom K L).toLinearMap) x)).ker
e_1✝ : Fin (X ^ finrank K L - C 1).natDegree = Fin (AdjoinRoot.powerBasis ⋯).dim
i : Fin (X ^ finrank K L - C 1).natDegree
⊢ ((fun σ ↦ σ x) ∘ ⇑((finCongr ⋯).trans (Equiv.ofBijective (fun n ↦ frobeniusAlgEquivOfAlgebraic K L ^ ↑n) ⋯))) i =
    (⇑(↑(AEval'.of (frobeniusAlgHom K L).toLinearMap).symm ∘ₗ
            ↑K
              (liftQ (Ideal.span {X ^ finrank K L - 1})
                (toSpanSingleton K[X] (AEval' (frobeniusAlgHom K L).toLinearMap)
                  ((AEval'.of (frobeniusAlgHom K L).toLinearMap) x))
                ⋯)) ∘
        ⇑(AdjoinRoot.powerBasis ⋯).basis)
      i
Module: Mathlib.FieldTheory.Galois.NormalBasis

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Infinite K
e : Module.Basis (Module.Free.ChooseBasisIndex K L) K L
M : Matrix Gal(L/K) Gal(L/K) (MvPolynomial (Module.Free.ChooseBasisIndex K L) L) :=
  Matrix.of fun i j ↦ ∑ k, i.symm (j (e k)) • MvPolynomial.X k
hq : Submodule.span L (Set.range fun k j ↦ j (e k)) = ⊤
g : Module.Free.ChooseBasisIndex K L → L
hg : (∑ i, g i • fun j ↦ j (e i)) = Pi.single 1 1
⊢ ∃ c, (MvPolynomial.eval c) M.det = 1

Tactic:
[

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Infinite K
e : Module.Basis (Module.Free.ChooseBasisIndex K L) K L
M : Matrix Gal(L/K) Gal(L/K) (MvPolynomial (Module.Free.ChooseBasisIndex K L) L) :=
  Matrix.of fun i j ↦ ∑ k, i.symm (j (e k)) • MvPolynomial.X k
hq : Submodule.span L (Set.range fun k j ↦ j (e k)) = ⊤
g : Module.Free.ChooseBasisIndex K L → L
hg : (∑ i, g i • fun j ↦ j (e i)) = Pi.single 1 1
⊢ ∃ c, (MvPolynomial.eval c) M.det = 1
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
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)
⊢ False

Tactic:
[

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
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)
⊢ False
Module: Mathlib.FieldTheory.Galois.NormalBasis

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Infinite K
e : Module.Basis (Module.Free.ChooseBasisIndex K L) K L
M : Matrix Gal(L/K) Gal(L/K) (MvPolynomial (Module.Free.ChooseBasisIndex K L) L) :=
  Matrix.of fun i j ↦ ∑ k, i.symm (j (e k)) • MvPolynomial.X k
hq : Submodule.span L (Set.range fun k j ↦ j (e k)) = ⊤
c : Module.Free.ChooseBasisIndex K L → L
hc : (MvPolynomial.eval c) M.det = 1
hM : M.det ≠ 0
b : Module.Free.ChooseBasisIndex K L → K
hb : (MvPolynomial.eval (⇑(algebraMap K L) ∘ b)) M.det ≠ 0
a : Gal(L/K) → K
ha : ∑ i, a i • i (∑ k, b k • e k) = 0
⊢ ⇑(algebraMap K L) ∘ a = ⇑(algebraMap K L) ∘ fun i ↦ 0

Tactic:
[

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Infinite K
e : Module.Basis (Module.Free.ChooseBasisIndex K L) K L
M : Matrix Gal(L/K) Gal(L/K) (MvPolynomial (Module.Free.ChooseBasisIndex K L) L) :=
  Matrix.of fun i j ↦ ∑ k, i.symm (j (e k)) • MvPolynomial.X k
hq : Submodule.span L (Set.range fun k j ↦ j (e k)) = ⊤
c : Module.Free.ChooseBasisIndex K L → L
hc : (MvPolynomial.eval c) M.det = 1
hM : M.det ≠ 0
b : Module.Free.ChooseBasisIndex K L → K
hb : (MvPolynomial.eval (⇑(algebraMap K L) ∘ b)) M.det ≠ 0
a : Gal(L/K) → K
ha : ∑ i, a i • i (∑ k, b k • e k) = 0
⊢ ⇑(algebraMap K L) ∘ a = ⇑(algebraMap K L) ∘ fun i ↦ 0
Module: Mathlib.FieldTheory.Galois.NormalBasis

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Infinite K
e : Module.Basis (Module.Free.ChooseBasisIndex K L) K L
M : Matrix Gal(L/K) Gal(L/K) (MvPolynomial (Module.Free.ChooseBasisIndex K L) L) :=
  Matrix.of fun i j ↦ ∑ k, i.symm (j (e k)) • MvPolynomial.X k
hq : Submodule.span L (Set.range fun k j ↦ j (e k)) = ⊤
c : Module.Free.ChooseBasisIndex K L → L
hc : (MvPolynomial.eval c) M.det = 1
hM : M.det ≠ 0
b : Module.Free.ChooseBasisIndex K L → K
hb : (M.map ⇑(MvPolynomial.eval (⇑(algebraMap K L) ∘ b))).det ≠ 0
a : Gal(L/K) → K
ha : ∑ i, a i • i (∑ k, b k • e k) = 0
i : Gal(L/K)
⊢ i ((M.map ⇑(MvPolynomial.eval (⇑(algebraMap K L) ∘ b))).mulVec (fun x ↦ (algebraMap K L) (a x)) i) = i (0 i)

Tactic:
[

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Infinite K
e : Module.Basis (Module.Free.ChooseBasisIndex K L) K L
M : Matrix Gal(L/K) Gal(L/K) (MvPolynomial (Module.Free.ChooseBasisIndex K L) L) :=
  Matrix.of fun i j ↦ ∑ k, i.symm (j (e k)) • MvPolynomial.X k
hq : Submodule.span L (Set.range fun k j ↦ j (e k)) = ⊤
c : Module.Free.ChooseBasisIndex K L → L
hc : (MvPolynomial.eval c) M.det = 1
hM : M.det ≠ 0
b : Module.Free.ChooseBasisIndex K L → K
hb : (M.map ⇑(MvPolynomial.eval (⇑(algebraMap K L) ∘ b))).det ≠ 0
a : Gal(L/K) → K
ha : ∑ i, a i • i (∑ k, b k • e k) = 0
i : Gal(L/K)
⊢ i ((M.map ⇑(MvPolynomial.eval (⇑(algebraMap K L) ∘ b))).mulVec (fun x ↦ (algebraMap K L) (a x)) i) = i (0 i)
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
ffb : fixedField ⊤ = ⊥
⊢ (algebraMap F K) a * ↑(Fintype.card Gal(K/F)) = ∑ i, ↑(c i) * ∑ x, logDeriv (x (u i)) + ∑ x, (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
ffb : fixedField ⊤ = ⊥
⊢ (algebraMap F K) a * ↑(Fintype.card Gal(K/F)) = ∑ i, ↑(c i) * ∑ x, logDeriv (x (u i)) + ∑ x, (x v)′
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

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.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
⊢ ⨆ i, adjoin F (⇑b ∘ φ '' Iio i) = ⊤

Tactic:
[

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, adjoin F (⇑b ∘ φ '' Iio i) = ⊤