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

Goal state before:
pp: case refine_2
L : Language
L' : Language
ϕ : L →ᴸ L'
inst✝³ : (n : ℕ) → (f : L'.Functions n) → Decidable (f ∈ Set.range fun f ↦ ϕ.onFunction f)
inst✝² : (n : ℕ) → (r : L'.Relations n) → Decidable (r ∈ Set.range fun r ↦ ϕ.onRelation r)
h : ϕ.Injective
M : Type u_1
inst✝¹ : Inhabited M
inst✝ : L.Structure M
this : L'.Structure M := ϕ.defaultExpansion M
n : ℕ
r : L.Relations n
xs : Fin n → M
⊢ RelMap (ϕ.onRelation r) xs = RelMap r xs

Tactic:
·

Goal state after:
case refine_2
L : Language
L' : Language
ϕ : L →ᴸ L'
inst✝³ : (n : ℕ) → (f : L'.Functions n) → Decidable (f ∈ Set.range fun f ↦ ϕ.onFunction f)
inst✝² : (n : ℕ) → (r : L'.Relations n) → Decidable (r ∈ Set.range fun r ↦ ϕ.onRelation r)
h : ϕ.Injective
M : Type u_1
inst✝¹ : Inhabited M
inst✝ : L.Structure M
this : L'.Structure M := ϕ.defaultExpansion M
n : ℕ
r : L.Relations n
xs : Fin n → M
⊢ RelMap (ϕ.onRelation r) xs = RelMap r xs
Module: Mathlib.FieldTheory.IsAlgClosed.Classification

Goal state before:
pp: K : Type u
L : Type v
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : IsAlgClosed K
inst✝³ : IsAlgClosed L
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
this✝ : Algebra (ZMod p) K := ZMod.algebra K p
this : Algebra (ZMod p) L := ZMod.algebra L p
s : Set K
hs : IsTranscendenceBasis (ZMod p) Subtype.val
t : Set L
ht : IsTranscendenceBasis (ZMod p) Subtype.val
hL : ℵ₀ < #L
⊢ Cardinal.lift.{v, u} #↑s = Cardinal.lift.{u, v} #↑t

Tactic:
rw [← lift_injective (cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _
        hs (le_of_lt (lt_aleph0_of_finite _)) hK),
      ← lift_injective (cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _
        ht (le_of_lt (lt_aleph0_of_finite _)) hL)]

Goal state after:
K : Type u
L : Type v
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : IsAlgClosed K
inst✝³ : IsAlgClosed L
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
this✝ : Algebra (ZMod p) K := ZMod.algebra K p
this : Algebra (ZMod p) L := ZMod.algebra L p
s : Set K
hs : IsTranscendenceBasis (ZMod p) Subtype.val
t : Set L
ht : IsTranscendenceBasis (ZMod p) Subtype.val
hL : ℵ₀ < #L
⊢ Cardinal.lift.{v, u} #K = Cardinal.lift.{u, v} #L
Module: Mathlib.FieldTheory.IsAlgClosed.Classification

Goal state before:
pp: case inl
K : Type u
L : Type v
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
p : ℕ
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
hp : Nat.Prime p
⊢ Nonempty (K ≃+* L)

pp: case inr
K : Type u
L : Type v
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
p : ℕ
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
hp : p = 0
⊢ Nonempty (K ≃+* L)

Tactic:
·

Goal state after:
case inl
K : Type u
L : Type v
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
p : ℕ
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
hp : Nat.Prime p
⊢ Nonempty (K ≃+* L)
Module: Mathlib.FieldTheory.IsAlgClosed.Classification

Goal state before:
pp: case inr
K : Type u
L : Type v
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
p : ℕ
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
hp : p = 0
⊢ Nonempty (K ≃+* L)

Tactic:
·

Goal state after:
case inr
K : Type u
L : Type v
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
p : ℕ
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
hp : p = 0
⊢ Nonempty (K ≃+* L)
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: case refine_1
L : Language
L' : Language
M : Type w
inst✝² : L.Structure M
α : Type u_1
inst✝¹ : (constantsOn α).Structure M
A B : Set M
h : A ⊆ B
N : Type w'
inst✝ : L.Structure N
f : M ↪[L] N
⊢ ∀ {n : ℕ} (f_1 : L[[↑A]].Functions n) (x : Fin n → M), f.toFun (funMap f_1 x) = funMap f_1 (f.toFun ∘ x)

pp: case refine_2
L : Language
L' : Language
M : Type w
inst✝² : L.Structure M
α : Type u_1
inst✝¹ : (constantsOn α).Structure M
A B : Set M
h : A ⊆ B
N : Type w'
inst✝ : L.Structure N
f : M ↪[L] N
⊢ ∀ {n : ℕ} (r : L[[↑A]].Relations n) (x : Fin n → M), RelMap r (f.toFun ∘ x) ↔ RelMap r x

Tactic:
·

Goal state after:
case refine_1
L : Language
L' : Language
M : Type w
inst✝² : L.Structure M
α : Type u_1
inst✝¹ : (constantsOn α).Structure M
A B : Set M
h : A ⊆ B
N : Type w'
inst✝ : L.Structure N
f : M ↪[L] N
⊢ ∀ {n : ℕ} (f_1 : L[[↑A]].Functions n) (x : Fin n → M), f.toFun (funMap f_1 x) = funMap f_1 (f.toFun ∘ x)
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: case refine_1.inl
L : Language
L' : Language
M : Type w
inst✝² : L.Structure M
α : Type u_1
inst✝¹ : (constantsOn α).Structure M
A B : Set M
h : A ⊆ B
N : Type w'
inst✝ : L.Structure N
f : M ↪[L] N
n : ℕ
x : Fin n → M
g : L.Functions n
⊢ f.toFun (funMap (Sum.inl g) x) = funMap (Sum.inl g) (f.toFun ∘ x)

Tactic:
exact f.map_fun' g x

Goal state after:
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: case refine_2
L : Language
L' : Language
M : Type w
inst✝² : L.Structure M
α : Type u_1
inst✝¹ : (constantsOn α).Structure M
A B : Set M
h : A ⊆ B
N : Type w'
inst✝ : L.Structure N
f : M ↪[L] N
⊢ ∀ {n : ℕ} (r : L[[↑A]].Relations n) (x : Fin n → M), RelMap r (f.toFun ∘ x) ↔ RelMap r x

Tactic:
·

Goal state after:
case refine_2
L : Language
L' : Language
M : Type w
inst✝² : L.Structure M
α : Type u_1
inst✝¹ : (constantsOn α).Structure M
A B : Set M
h : A ⊆ B
N : Type w'
inst✝ : L.Structure N
f : M ↪[L] N
⊢ ∀ {n : ℕ} (r : L[[↑A]].Relations n) (x : Fin n → M), RelMap r (f.toFun ∘ x) ↔ RelMap r x
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case pos
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : x = 0
⊢ Group.IsSolvable (X ^ n - C x).Gal

pp: case neg
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : ¬x = 0
⊢ Group.IsSolvable (X ^ n - C x).Gal

Tactic:
·

Goal state after:
case pos
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : x = 0
⊢ Group.IsSolvable (X ^ n - C x).Gal
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case neg.hpq
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : ¬x = 0
⊢ (map (algebraMap F (X ^ n - C x).SplittingField) (X ^ n - 1)).Splits

pp: case neg.hp
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : ¬x = 0
⊢ Group.IsSolvable (X ^ n - 1).Gal

pp: case neg.hq
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : ¬x = 0
⊢ Group.IsSolvable (map (algebraMap F (X ^ n - 1).SplittingField) (X ^ n - C x)).Gal

Tactic:
·

Goal state after:
case neg.hpq
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : ¬x = 0
⊢ (map (algebraMap F (X ^ n - C x).SplittingField) (X ^ n - 1)).Splits
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case neg.hp
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : ¬x = 0
⊢ Group.IsSolvable (X ^ n - 1).Gal

pp: case neg.hq
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : ¬x = 0
⊢ Group.IsSolvable (map (algebraMap F (X ^ n - 1).SplittingField) (X ^ n - C x)).Gal

Tactic:
·

Goal state after:
case neg.hp
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : ¬x = 0
⊢ Group.IsSolvable (X ^ n - 1).Gal
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case neg.hq
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : ¬x = 0
⊢ Group.IsSolvable (map (algebraMap F (X ^ n - 1).SplittingField) (X ^ n - C x)).Gal

Tactic:
·

Goal state after:
case neg.hq
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : ¬x = 0
⊢ Group.IsSolvable (map (algebraMap F (X ^ n - 1).SplittingField) (X ^ n - C x)).Gal
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case refine_1
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
n : ℕ
hn : n ≠ 0
p : F[X]
h1 : p ≠ 0
h2 : (aeval (x ^ n)) p = 0
h : p.comp (X ^ n) = 0
⊢ p.leadingCoeff = 0

pp: case refine_2
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
n : ℕ
hn : n ≠ 0
p : F[X]
h1 : p ≠ 0
h2 : (aeval (x ^ n)) p = 0
⊢ (aeval x) (p.comp (X ^ n)) = 0

Tactic:
·

Goal state after:
case refine_1
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
n : ℕ
hn : n ≠ 0
p : F[X]
h1 : p ≠ 0
h2 : (aeval (x ^ n)) p = 0
h : p.comp (X ^ n) = 0
⊢ p.leadingCoeff = 0
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case refine_2
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
n : ℕ
hn : n ≠ 0
p : F[X]
h1 : p ≠ 0
h2 : (aeval (x ^ n)) p = 0
⊢ (aeval x) (p.comp (X ^ n)) = 0

Tactic:
·

Goal state after:
case refine_2
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
n : ℕ
hn : n ≠ 0
p : F[X]
h1 : p ≠ 0
h2 : (aeval (x ^ n)) p = 0
⊢ (aeval x) (p.comp (X ^ n)) = 0
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case inl
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
hx : x ∈ solvableByRad F E
n : ℕ
hn : n ≠ 0
hα : Group.IsSolvable (minpoly F (x ^ n)).Gal
p : F[X] := minpoly F (x ^ n)
h : p.comp (X ^ n) = 0
h' : p = 0
⊢ False

pp: case inr
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
hx : x ∈ solvableByRad F E
n : ℕ
hn : n ≠ 0
hα : Group.IsSolvable (minpoly F (x ^ n)).Gal
p : F[X] := minpoly F (x ^ n)
h : p.comp (X ^ n) = 0
h' : eval ((X ^ n).coeff 0) p = 0 ∧ X ^ n = C ((X ^ n).coeff 0)
⊢ False

Tactic:
·

Goal state after:
case inl
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
hx : x ∈ solvableByRad F E
n : ℕ
hn : n ≠ 0
hα : Group.IsSolvable (minpoly F (x ^ n)).Gal
p : F[X] := minpoly F (x ^ n)
h : p.comp (X ^ n) = 0
h' : p = 0
⊢ False
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case inr
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
hx : x ∈ solvableByRad F E
n : ℕ
hn : n ≠ 0
hα : Group.IsSolvable (minpoly F (x ^ n)).Gal
p : F[X] := minpoly F (x ^ n)
h : p.comp (X ^ n) = 0
h' : eval ((X ^ n).coeff 0) p = 0 ∧ X ^ n = C ((X ^ n).coeff 0)
⊢ False

Tactic:
·

Goal state after:
case inr
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
hx : x ∈ solvableByRad F E
n : ℕ
hn : n ≠ 0
hα : Group.IsSolvable (minpoly F (x ^ n)).Gal
p : F[X] := minpoly F (x ^ n)
h : p.comp (X ^ n) = 0
h' : eval ((X ^ n).coeff 0) p = 0 ∧ X ^ n = C ((X ^ n).coeff 0)
⊢ False
Module: Mathlib.ModelTheory.Algebra.Ring.Basic

Goal state before:
pp: case inl
α : Type u_1
fst✝ : ℕ
f : ring.Functions fst✝
⊢ Sum.inl ⟨fst✝, f⟩ ∈
    { val := ↑[Sum.inl ⟨2, add⟩, Sum.inl ⟨2, mul⟩, Sum.inl ⟨1, neg⟩, Sum.inl ⟨0, zero⟩, Sum.inl ⟨0, one⟩],
      nodup := instFintypeSymbolsRing._proof_1 }

pp: case inr
α : Type u_1
fst✝ : ℕ
f : ring.Relations fst✝
⊢ Sum.inr ⟨fst✝, f⟩ ∈
    { val := ↑[Sum.inl ⟨2, add⟩, Sum.inl ⟨2, mul⟩, Sum.inl ⟨1, neg⟩, Sum.inl ⟨0, zero⟩, Sum.inl ⟨0, one⟩],
      nodup := instFintypeSymbolsRing._proof_1 }

Tactic:
·

Goal state after:
case inl
α : Type u_1
fst✝ : ℕ
f : ring.Functions fst✝
⊢ Sum.inl ⟨fst✝, f⟩ ∈
    { val := ↑[Sum.inl ⟨2, add⟩, Sum.inl ⟨2, mul⟩, Sum.inl ⟨1, neg⟩, Sum.inl ⟨0, zero⟩, Sum.inl ⟨0, one⟩],
      nodup := instFintypeSymbolsRing._proof_1 }
Module: Mathlib.ModelTheory.Algebra.Ring.Basic

Goal state before:
pp: case inr
α : Type u_1
fst✝ : ℕ
f : ring.Relations fst✝
⊢ Sum.inr ⟨fst✝, f⟩ ∈
    { val := ↑[Sum.inl ⟨2, add⟩, Sum.inl ⟨2, mul⟩, Sum.inl ⟨1, neg⟩, Sum.inl ⟨0, zero⟩, Sum.inl ⟨0, one⟩],
      nodup := instFintypeSymbolsRing._proof_1 }

Tactic:
·

Goal state after:
case inr
α : Type u_1
fst✝ : ℕ
f : ring.Relations fst✝
⊢ Sum.inr ⟨fst✝, f⟩ ∈
    { val := ↑[Sum.inl ⟨2, add⟩, Sum.inl ⟨2, mul⟩, Sum.inl ⟨1, neg⟩, Sum.inl ⟨0, zero⟩, Sum.inl ⟨0, one⟩],
      nodup := instFintypeSymbolsRing._proof_1 }
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case x
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
hx : x ∈ solvableByRad F E
n : ℕ
hn : n ≠ 0
hα : Group.IsSolvable (minpoly F (x ^ n)).Gal
p : F[X] := ⋯
hp : p.comp (X ^ n) ≠ 0
⊢ Fact (map (algebraMap F (SplittingField ?q)) (minpoly F x)).Splits

pp: case hq
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
hx : x ∈ solvableByRad F E
n : ℕ
hn : n ≠ 0
hα : Group.IsSolvable (minpoly F (x ^ n)).Gal
p : F[X] := ⋯
hp : p.comp (X ^ n) ≠ 0
⊢ Group.IsSolvable (Gal ?q)

pp: case q
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
hx : x ∈ solvableByRad F E
n : ℕ
hn : n ≠ 0
hα : Group.IsSolvable (minpoly F (x ^ n)).Gal
p : F[X] := ⋯
hp : p.comp (X ^ n) ≠ 0
⊢ F[X]

Tactic:
·

Goal state after:
case x
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
hx : x ∈ solvableByRad F E
n : ℕ
hn : n ≠ 0
hα : Group.IsSolvable (minpoly F (x ^ n)).Gal
p : F[X] := ⋯
hp : p.comp (X ^ n) ≠ 0
⊢ Fact (map (algebraMap F (SplittingField ?q)) (minpoly F x)).Splits
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case hq
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
hx : x ∈ solvableByRad F E
n : ℕ
hn : n ≠ 0
hα : Group.IsSolvable (minpoly F (x ^ n)).Gal
p : F[X] := ⋯
hp : p.comp (X ^ n) ≠ 0
⊢ Group.IsSolvable (p.comp (X ^ n)).Gal

Tactic:
·

Goal state after:
case hq
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
hx : x ∈ solvableByRad F E
n : ℕ
hn : n ≠ 0
hα : Group.IsSolvable (minpoly F (x ^ n)).Gal
p : F[X] := ⋯
hp : p.comp (X ^ n) ≠ 0
⊢ Group.IsSolvable (p.comp (X ^ n)).Gal
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case hq.refine_1
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
hx : x ∈ solvableByRad F E
n : ℕ
hn : n ≠ 0
hα : Group.IsSolvable (minpoly F (x ^ n)).Gal
p : F[X] := minpoly F (x ^ n)
hp : p.comp (X ^ n) ≠ 0
⊢ (map (algebraMap F (p.comp (X ^ n)).SplittingField) p).Splits

pp: case hq.refine_2
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
hx : x ∈ solvableByRad F E
n : ℕ
hn : n ≠ 0
hα : Group.IsSolvable (minpoly F (x ^ n)).Gal
p : F[X] := minpoly F (x ^ n)
hp : p.comp (X ^ n) ≠ 0
⊢ Group.IsSolvable (map (algebraMap F p.SplittingField) (p.comp (X ^ n))).Gal

Tactic:
·

Goal state after:
case hq.refine_1
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
hx : x ∈ solvableByRad F E
n : ℕ
hn : n ≠ 0
hα : Group.IsSolvable (minpoly F (x ^ n)).Gal
p : F[X] := minpoly F (x ^ n)
hp : p.comp (X ^ n) ≠ 0
⊢ (map (algebraMap F (p.comp (X ^ n)).SplittingField) p).Splits
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case hq.refine_2
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
hx : x ∈ solvableByRad F E
n : ℕ
hn : n ≠ 0
hα : Group.IsSolvable (minpoly F (x ^ n)).Gal
p : F[X] := minpoly F (x ^ n)
hp : p.comp (X ^ n) ≠ 0
⊢ Group.IsSolvable (map (algebraMap F p.SplittingField) (p.comp (X ^ n))).Gal

Tactic:
·

Goal state after:
case hq.refine_2
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
hx : x ∈ solvableByRad F E
n : ℕ
hn : n ≠ 0
hα : Group.IsSolvable (minpoly F (x ^ n)).Gal
p : F[X] := minpoly F (x ^ n)
hp : p.comp (X ^ n) ≠ 0
⊢ Group.IsSolvable (map (algebraMap F p.SplittingField) (p.comp (X ^ n))).Gal
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case func.zero
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
f : L[[γ]].Functions 0
_ts✝ : Fin 0 → L[[γ]].Term α
ih : ∀ (a : Fin 0), (_ts✝ a).constantsToVars.varsToConstants = _ts✝ a
⊢ (func f _ts✝).constantsToVars.varsToConstants = func f _ts✝

pp: case func.succ
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n✝ : ℕ
f : L[[γ]].Functions (n✝ + 1)
_ts✝ : Fin (n✝ + 1) → L[[γ]].Term α
ih : ∀ (a : Fin (n✝ + 1)), (_ts✝ a).constantsToVars.varsToConstants = _ts✝ a
⊢ (func f _ts✝).constantsToVars.varsToConstants = func f _ts✝

Tactic:
·

Goal state after:
case func.zero
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
f : L[[γ]].Functions 0
_ts✝ : Fin 0 → L[[γ]].Term α
ih : ∀ (a : Fin 0), (_ts✝ a).constantsToVars.varsToConstants = _ts✝ a
⊢ (func f _ts✝).constantsToVars.varsToConstants = func f _ts✝
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case func.zero.inl
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
_ts✝ : Fin 0 → L[[γ]].Term α
ih : ∀ (a : Fin 0), (_ts✝ a).constantsToVars.varsToConstants = _ts✝ a
val✝ : L.Functions 0
⊢ (func (Sum.inl val✝) _ts✝).constantsToVars.varsToConstants = func (Sum.inl val✝) _ts✝

pp: case func.zero.inr
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
_ts✝ : Fin 0 → L[[γ]].Term α
ih : ∀ (a : Fin 0), (_ts✝ a).constantsToVars.varsToConstants = _ts✝ a
val✝ : (constantsOn γ).Functions 0
⊢ (func (Sum.inr val✝) _ts✝).constantsToVars.varsToConstants = func (Sum.inr val✝) _ts✝

Tactic:
·

Goal state after:
case func.zero.inl
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
_ts✝ : Fin 0 → L[[γ]].Term α
ih : ∀ (a : Fin 0), (_ts✝ a).constantsToVars.varsToConstants = _ts✝ a
val✝ : L.Functions 0
⊢ (func (Sum.inl val✝) _ts✝).constantsToVars.varsToConstants = func (Sum.inl val✝) _ts✝
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case func.zero.inr
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
_ts✝ : Fin 0 → L[[γ]].Term α
ih : ∀ (a : Fin 0), (_ts✝ a).constantsToVars.varsToConstants = _ts✝ a
val✝ : (constantsOn γ).Functions 0
⊢ (func (Sum.inr val✝) _ts✝).constantsToVars.varsToConstants = func (Sum.inr val✝) _ts✝

Tactic:
·

Goal state after:
case func.zero.inr
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
_ts✝ : Fin 0 → L[[γ]].Term α
ih : ∀ (a : Fin 0), (_ts✝ a).constantsToVars.varsToConstants = _ts✝ a
val✝ : (constantsOn γ).Functions 0
⊢ (func (Sum.inr val✝) _ts✝).constantsToVars.varsToConstants = func (Sum.inr val✝) _ts✝
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case func.succ
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n✝ : ℕ
f : L[[γ]].Functions (n✝ + 1)
_ts✝ : Fin (n✝ + 1) → L[[γ]].Term α
ih : ∀ (a : Fin (n✝ + 1)), (_ts✝ a).constantsToVars.varsToConstants = _ts✝ a
⊢ (func f _ts✝).constantsToVars.varsToConstants = func f _ts✝

Tactic:
·

Goal state after:
case func.succ
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n✝ : ℕ
f : L[[γ]].Functions (n✝ + 1)
_ts✝ : Fin (n✝ + 1) → L[[γ]].Term α
ih : ∀ (a : Fin (n✝ + 1)), (_ts✝ a).constantsToVars.varsToConstants = _ts✝ a
⊢ (func f _ts✝).constantsToVars.varsToConstants = func f _ts✝
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case func.succ.inl
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n✝ : ℕ
_ts✝ : Fin (n✝ + 1) → L[[γ]].Term α
ih : ∀ (a : Fin (n✝ + 1)), (_ts✝ a).constantsToVars.varsToConstants = _ts✝ a
val✝ : L.Functions (n✝ + 1)
⊢ (func (Sum.inl val✝) _ts✝).constantsToVars.varsToConstants = func (Sum.inl val✝) _ts✝

pp: case func.succ.inr
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n✝ : ℕ
_ts✝ : Fin (n✝ + 1) → L[[γ]].Term α
ih : ∀ (a : Fin (n✝ + 1)), (_ts✝ a).constantsToVars.varsToConstants = _ts✝ a
f : (constantsOn γ).Functions (n✝ + 1)
⊢ (func (Sum.inr f) _ts✝).constantsToVars.varsToConstants = func (Sum.inr f) _ts✝

Tactic:
·

Goal state after:
case func.succ.inl
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n✝ : ℕ
_ts✝ : Fin (n✝ + 1) → L[[γ]].Term α
ih : ∀ (a : Fin (n✝ + 1)), (_ts✝ a).constantsToVars.varsToConstants = _ts✝ a
val✝ : L.Functions (n✝ + 1)
⊢ (func (Sum.inl val✝) _ts✝).constantsToVars.varsToConstants = func (Sum.inl val✝) _ts✝
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case func.succ.inr
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n✝ : ℕ
_ts✝ : Fin (n✝ + 1) → L[[γ]].Term α
ih : ∀ (a : Fin (n✝ + 1)), (_ts✝ a).constantsToVars.varsToConstants = _ts✝ a
f : (constantsOn γ).Functions (n✝ + 1)
⊢ (func (Sum.inr f) _ts✝).constantsToVars.varsToConstants = func (Sum.inr f) _ts✝

Tactic:
·

Goal state after:
case func.succ.inr
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n✝ : ℕ
_ts✝ : Fin (n✝ + 1) → L[[γ]].Term α
ih : ∀ (a : Fin (n✝ + 1)), (_ts✝ a).constantsToVars.varsToConstants = _ts✝ a
f : (constantsOn γ).Functions (n✝ + 1)
⊢ (func (Sum.inr f) _ts✝).constantsToVars.varsToConstants = func (Sum.inr f) _ts✝
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case func.zero
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
f : L.Functions 0
_ts✝ : Fin 0 → L.Term (γ ⊕ α)
ih : ∀ (a : Fin 0), (_ts✝ a).varsToConstants.constantsToVars = _ts✝ a
⊢ (func f _ts✝).varsToConstants.constantsToVars = func f _ts✝

Tactic:
·

Goal state after:
case func.zero
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
f : L.Functions 0
_ts✝ : Fin 0 → L.Term (γ ⊕ α)
ih : ∀ (a : Fin 0), (_ts✝ a).varsToConstants.constantsToVars = _ts✝ a
⊢ (func f _ts✝).varsToConstants.constantsToVars = func f _ts✝
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case func.succ
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n✝ : ℕ
f : L.Functions (n✝ + 1)
_ts✝ : Fin (n✝ + 1) → L.Term (γ ⊕ α)
ih : ∀ (a : Fin (n✝ + 1)), (_ts✝ a).varsToConstants.constantsToVars = _ts✝ a
⊢ (func f _ts✝).varsToConstants.constantsToVars = func f _ts✝

Tactic:
·

Goal state after:
case func.succ
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n✝ : ℕ
f : L.Functions (n✝ + 1)
_ts✝ : Fin (n✝ + 1) → L.Term (γ ⊕ α)
ih : ∀ (a : Fin (n✝ + 1)), (_ts✝ a).varsToConstants.constantsToVars = _ts✝ a
⊢ (func f _ts✝).varsToConstants.constantsToVars = func f _ts✝
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case var
L : Language
α : Type u'
a✝ : α
⊢ ((var a✝).substFunc fun {n} ↦ Functions.term) = var a✝

pp: case func
L : Language
α : Type u'
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
_ts_ih✝ : ∀ (a : Fin l✝), ((_ts✝ a).substFunc fun {n} ↦ Functions.term) = _ts✝ a
⊢ ((func _f✝ _ts✝).substFunc fun {n} ↦ Functions.term) = func _f✝ _ts✝

Tactic:
·

Goal state after:
case var
L : Language
α : Type u'
a✝ : α
⊢ ((var a✝).substFunc fun {n} ↦ Functions.term) = var a✝
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case func
L : Language
α : Type u'
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
_ts_ih✝ : ∀ (a : Fin l✝), ((_ts✝ a).substFunc fun {n} ↦ Functions.term) = _ts✝ a
⊢ ((func _f✝ _ts✝).substFunc fun {n} ↦ Functions.term) = func _f✝ _ts✝

Tactic:
·

Goal state after:
case func
L : Language
α : Type u'
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
_ts_ih✝ : ∀ (a : Fin l✝), ((_ts✝ a).substFunc fun {n} ↦ Functions.term) = _ts✝ a
⊢ ((func _f✝ _ts✝).substFunc fun {n} ↦ Functions.term) = func _f✝ _ts✝