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

Goal state before:
pp: case neg
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (X ^ n - 1)).Splits
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
⊢ Group.IsSolvable (X ^ n - C a).Gal

Tactic:
have mem_range : ∀ {c : (X ^ n - C a).SplittingField},
      (c ^ n = 1 → (∃ d, algebraMap F (X ^ n - C a).SplittingField d = c)) := fun {c} hc =>
    RingHom.mem_range.mp (minpoly.mem_range_of_degree_eq_one F c
      (Splits.degree_eq_one_of_irreducible (h.of_dvd (map_ne_zero hn''')
        (minpoly.dvd F c (by rwa [map_id, map_sub, sub_eq_zero, aeval_X_pow, aeval_one])))
          (minpoly.irreducible ((SplittingField.instNormal (X ^ n - C a)).isIntegral c))))

Goal state after:
case neg
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (X ^ n - 1)).Splits
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c
⊢ Group.IsSolvable (X ^ n - C a).Gal
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν)) =
    map f (μ.singularPart ν) + (map f ν).withDensity ((map f μ).rnDeriv (map f ν))

Tactic:
← hf.map_withDensity_rnDeriv μ ν

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν)) =
    map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))
Module: Mathlib.RingTheory.Algebraic.Cardinality

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
L : Type u
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
inst✝² : Algebra R L
inst✝¹ : IsTorsionFree R L
inst✝ : Algebra.IsAlgebraic R L
⊢ #L ≤ max #R ℵ₀

Tactic:
by
  simpa only [lift_id] using lift_cardinalMk_le_max R L

Goal state after:
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
⊢ Function.Injective toEmbedding

Tactic:
intro _

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
a₁✝ : M ≃[L] N
⊢ ∀ ⦃a₂ : M ≃[L] N⦄, a₁✝.toEmbedding = a₂.toEmbedding → a₁✝ = a₂
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:
· exact ⟨(SplittingField.splits (p.comp (X ^ n))).of_dvd (map_ne_zero hp)
      ((map_dvd_map' _).mpr (minpoly.dvd F x (by rw [aeval_comp, aeval_X_pow, minpoly.aeval])))⟩

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.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:
· cases f
        · simp [constantsToVars, varsToConstants, ih]
        · simp [constantsToVars, varsToConstants, Constants.term, eq_iff_true_of_subsingleton]

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 rel
L : Language
α : Type u'
k n✝¹ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝¹)
m✝ n✝ : ℕ
km✝ : n✝¹ ≤ m✝
mn✝ : m✝ ≤ n✝
⊢ rel R✝ ((Term.relabel (Sum.map id (Fin.castLE mn✝)) ∘ Term.relabel (Sum.map id (Fin.castLE km✝))) ∘ ts✝) =
    rel R✝ (Term.relabel (Sum.map id (Fin.castLE ⋯)) ∘ ts✝)

Tactic:
Term.relabel_comp_relabel

Goal state after:
case rel
L : Language
α : Type u'
k n✝¹ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝¹)
m✝ n✝ : ℕ
km✝ : n✝¹ ≤ m✝
mn✝ : m✝ ≤ n✝
⊢ rel R✝ (Term.relabel (Sum.map id (Fin.castLE mn✝) ∘ Sum.map id (Fin.castLE km✝)) ∘ ts✝) =
    rel R✝ (Term.relabel (Sum.map id (Fin.castLE ⋯)) ∘ ts✝)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
φ ψ : L.BoundedFormula α l
v : α → M
xs : Fin l → M
⊢ (φ ⟹ ψ).Realize v xs ↔ φ.Realize v xs → ψ.Realize v xs

Tactic:
by
  simp only [Realize]

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case cons
L : Language
α : Type u'
h :
  ∀ (φ : (n : ℕ) × L.BoundedFormula α n) (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (φ.snd.listEncode ++ l') = φ :: listDecode l'
φ : (n : ℕ) × L.BoundedFormula α n
l : List ((n : ℕ) × L.BoundedFormula α n)
ih : listDecode (flatMap (fun φ ↦ φ.snd.listEncode) l) = l
⊢ listDecode (φ.snd.listEncode ++ flatMap (fun φ ↦ φ.snd.listEncode) l) = φ :: l

Tactic:
h φ _,

Goal state after:
case cons
L : Language
α : Type u'
h :
  ∀ (φ : (n : ℕ) × L.BoundedFormula α n) (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (φ.snd.listEncode ++ l') = φ :: listDecode l'
φ : (n : ℕ) × L.BoundedFormula α n
l : List ((n : ℕ) × L.BoundedFormula α n)
ih : listDecode (flatMap (fun φ ↦ φ.snd.listEncode) l) = l
⊢ φ :: listDecode (flatMap (fun φ ↦ φ.snd.listEncode) l) = φ :: l
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: case refine_2
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
h : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f s
h' : (closure L).toFun s = { carrier := s, fun_mem := ⋯ }
⊢ s ∈ (closure L).closed

Tactic:
exact congr_arg _ h'

Goal state after:
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: case refine_3
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (⇑f ∘ x) (f b))
n : ℕ
φ : L.BoundedFormula Empty n
⊢ ∀ {n l : ℕ} (R : L.Relations l) (ts : Fin l → L.Term (Empty ⊕ Fin n)) (xs : Fin n → M),
    (BoundedFormula.rel R ts).Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ (BoundedFormula.rel R ts).Realize default xs

Tactic:
intro _

Goal state after:
case refine_3
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (⇑f ∘ x) (f b))
n : ℕ
φ : L.BoundedFormula Empty n
n✝ : ℕ
⊢ ∀ {l : ℕ} (R : L.Relations l) (ts : Fin l → L.Term (Empty ⊕ Fin n✝)) (xs : Fin n✝ → M),
    (BoundedFormula.rel R ts).Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ (BoundedFormula.rel R ts).Realize default xs
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: case refine_3
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (⇑f ∘ x) (f b))
n : ℕ
φ : L.BoundedFormula Empty n
n✝ l✝ : ℕ
R : L.Relations l✝
⊢ ∀ (ts : Fin l✝ → L.Term (Empty ⊕ Fin n✝)) (xs : Fin n✝ → M),
    (BoundedFormula.rel R ts).Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ (BoundedFormula.rel R ts).Realize default xs

Tactic:
ts

Goal state after:
case refine_3
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (⇑f ∘ x) (f b))
n : ℕ
φ : L.BoundedFormula Empty n
n✝ l✝ : ℕ
R : L.Relations l✝
ts : Fin l✝ → L.Term (Empty ⊕ Fin n✝)
⊢ ∀ (xs : Fin n✝ → M),
    (BoundedFormula.rel R ts).Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ (BoundedFormula.rel R ts).Realize default xs
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: case refine_4
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (⇑f ∘ x) (f b))
n : ℕ
φ : L.BoundedFormula Empty n
⊢ ∀ {n : ℕ} (f₁ f₂ : L.BoundedFormula Empty n),
    (∀ (xs : Fin n → M), f₁.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ f₁.Realize default xs) →
      (∀ (xs : Fin n → M), f₂.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ f₂.Realize default xs) →
        ∀ (xs : Fin n → M), (f₁ ⟹ f₂).Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ (f₁ ⟹ f₂).Realize default xs

Tactic:
intro _

Goal state after:
case refine_4
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (⇑f ∘ x) (f b))
n : ℕ
φ : L.BoundedFormula Empty n
n✝ : ℕ
⊢ ∀ (f₁ f₂ : L.BoundedFormula Empty n✝),
    (∀ (xs : Fin n✝ → M), f₁.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ f₁.Realize default xs) →
      (∀ (xs : Fin n✝ → M), f₂.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ f₂.Realize default xs) →
        ∀ (xs : Fin n✝ → M), (f₁ ⟹ f₂).Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ (f₁ ⟹ f₂).Realize default xs
Module: Mathlib.ModelTheory.ElementarySubstructures

Goal state before:
pp: L : Language
M : Type u_1
inst✝ : L.Structure M
A : Set M
hA : MeetsDefinable A
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x : Fin n → ↥((closure L).toFun A)
a : M
hφ : φ.Realize default (Fin.snoc (Subtype.val ∘ x) a)
D : Set M := {y | φ.Realize default (Fin.snoc (Subtype.val ∘ x) y)}
hD_ne : D.Nonempty
⊢ ∃ φ, {x | x 0 ∈ D} = ofPred φ.Realize

Tactic:
refine ⟨((L.lhomWithConstants A).onBoundedFormula φ).toFormula.relabel
      (Sum.elim Empty.elim id) |>.subst fun i => Fin.lastCases (Term.var 0)
        (fun j => (L.con ⟨x j, by
        nth_rw 1 [← hA.closure_eq_self]
        simp only [Subtype.coe_prop]
        ⟩).term) i, ?_⟩

Goal state after:
L : Language
M : Type u_1
inst✝ : L.Structure M
A : Set M
hA : MeetsDefinable A
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x : Fin n → ↥((closure L).toFun A)
a : M
hφ : φ.Realize default (Fin.snoc (Subtype.val ∘ x) a)
D : Set M := {y | φ.Realize default (Fin.snoc (Subtype.val ∘ x) y)}
hD_ne : D.Nonempty
⊢ {x | x 0 ∈ D} =
    ofPred
      (Formula.Realize
        (BoundedFormula.subst
          (Formula.relabel (Sum.elim Empty.elim id) ((L.lhomWithConstants ↑A).onBoundedFormula φ).toFormula) fun i ↦
          Fin.lastCases (var 0) (fun j ↦ (L.con ⟨↑(x j), ⋯⟩).term) i))
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: L : Language
⊢ ((sum fun i ↦ #(L.BoundedFormula Empty (i + 1))) + sum fun i ↦ lift.{max u v, u} #(L.Functions i)) =
    sum fun i ↦ #(L.BoundedFormula Empty (i + 1))

Tactic:
add_eq_max,

Goal state after:
L : Language
⊢ max (sum fun i ↦ #(L.BoundedFormula Empty (i + 1))) (sum fun i ↦ lift.{max u v, u} #(L.Functions i)) =
    sum fun i ↦ #(L.BoundedFormula Empty (i + 1))

L : Language
⊢ ℵ₀ ≤ sum fun i ↦ #(L.BoundedFormula Empty (i + 1))
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: L : Language
⊢ #((n : ℕ) × L.BoundedFormula Empty n) ≤ max ℵ₀ L.card

Tactic:
· refine _root_.trans BoundedFormula.card_le (lift_le.{max u v}.1 ?_)
    simp only [mk_empty, lift_zero, lift_uzero, zero_add]
    rfl

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case all.mp
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
g : F
v : α → M
n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ {xs : Fin (n✝ + 1) → M}, f✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ f✝.Realize v xs
xs : Fin n✝ → M
⊢ (∀ (x : N), f✝.Realize (⇑g ∘ v) (snoc (⇑g ∘ xs) x)) → ∀ (x : M), f✝.Realize v (snoc xs x)

Tactic:
intro h a
      have h' := h (g a)
      rw [← Fin.comp_snoc, ih3] at h'
      exact h'

Goal state after:
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #↑(⇑Equiv.ulift '' s') = #↑s'
⊢ ℵ₀ ≤ #↑s' ∧
    lift.{max u v, w} #↑(s ∪ ⇑Equiv.ulift '' s') + lift.{w, max u v} #((i : ℕ) × (L.sum L.skolem₁).Functions i) ≤
      lift.{max u v, w} #↑(⇑Equiv.ulift '' s')

Tactic:
add_eq_max,

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #↑(⇑Equiv.ulift '' s') = #↑s'
⊢ ℵ₀ ≤ #↑s' ∧
    max (lift.{max u v, w} #↑(s ∪ ⇑Equiv.ulift '' s')) (lift.{w, max u v} #((i : ℕ) × (L.sum L.skolem₁).Functions i)) ≤
      lift.{max u v, w} #↑(⇑Equiv.ulift '' s')

L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #↑(⇑Equiv.ulift '' s') = #↑s'
⊢ ℵ₀ ≤ lift.{max u v, w} #↑(s ∪ ⇑Equiv.ulift '' s')
Module: Mathlib.ModelTheory.Algebra.Ring.Definability

Goal state before:
pp: ι : Type u_1
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
S : Finset (MvPolynomial ι K)
p' : ↥S → FreeCommRing ((i : ↥S) × ↥(↑i).support ⊕ ι) := genericPolyMap fun p ↦ (↑p).support
this✝ : DecidableEq ι := Classical.decEq ι
this : DecidableEq K := Classical.decEq K
⊢ ∃ φ, zeroLocus K (Ideal.span ↑S) = {v | φ.Realize (Sum.elim Subtype.val v)}

Tactic:
rw [MvPolynomial.zeroLocus_span]

Goal state after:
ι : Type u_1
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
S : Finset (MvPolynomial ι K)
p' : ↥S → FreeCommRing ((i : ↥S) × ↥(↑i).support ⊕ ι) := genericPolyMap fun p ↦ (↑p).support
this✝ : DecidableEq ι := Classical.decEq ι
this : DecidableEq K := Classical.decEq K
⊢ ∃ φ, {x | ∀ p ∈ ↑S, (aeval x) p = 0} = {v | φ.Realize (Sum.elim Subtype.val v)}
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: case inr
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h : ↑T0 ⊨ᵇ φ
p : ℕ
hp : p ∈ {q | Nat.Prime q}
q : ℕ
property✝ : Nat.Prime q
hq : ⟨q, property✝⟩ ∉ {⟨p, hp⟩}
K : Type
struc✝ : Language.ring.Structure K
is_model✝ : K ⊨ Theory.ACF ↑⟨q, property✝⟩
nonempty'✝ : Nonempty K
v✝ : Empty → ↑{ Carrier := K, struc := struc✝, is_model := is_model✝, nonempty' := nonempty'✝ }
xs✝ : Fin 0 → ↑{ Carrier := K, struc := struc✝, is_model := is_model✝, nonempty' := nonempty'✝ }
hqp : q ≠ p
x✝¹ : Field K := fieldOfModelACF q K
this✝ : K ⊨ Theory.field
x✝ : CompatibleRing K := compatibleRingOfModelField K
this : CharP K q
⊢ ¬CharP K p

Tactic:
intro _

Goal state after:
case inr
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h : ↑T0 ⊨ᵇ φ
p : ℕ
hp : p ∈ {q | Nat.Prime q}
q : ℕ
property✝ : Nat.Prime q
hq : ⟨q, property✝⟩ ∉ {⟨p, hp⟩}
K : Type
struc✝ : Language.ring.Structure K
is_model✝ : K ⊨ Theory.ACF ↑⟨q, property✝⟩
nonempty'✝ : Nonempty K
v✝ : Empty → ↑{ Carrier := K, struc := struc✝, is_model := is_model✝, nonempty' := nonempty'✝ }
xs✝ : Fin 0 → ↑{ Carrier := K, struc := struc✝, is_model := is_model✝, nonempty' := nonempty'✝ }
hqp : q ≠ p
x✝¹ : Field K := fieldOfModelACF q K
this✝ : K ⊨ Theory.field
x✝ : CompatibleRing K := compatibleRingOfModelField K
this : CharP K q
a✝ : CharP K p
⊢ False
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: case add
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
⊢ ∀ (p_1 q : MvPolynomial σ (ZMod p)),
    (frobenius (MvPolynomial σ (ZMod p)) p) p_1 = (expand p) p_1 →
      (frobenius (MvPolynomial σ (ZMod p)) p) q = (expand p) q →
        (frobenius (MvPolynomial σ (ZMod p)) p) p_1 + (frobenius (MvPolynomial σ (ZMod p)) p) q =
          (expand p) p_1 + (expand p) q

Tactic:
intro _

Goal state after:
case add
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f p✝ : MvPolynomial σ (ZMod p)
⊢ ∀ (q : MvPolynomial σ (ZMod p)),
    (frobenius (MvPolynomial σ (ZMod p)) p) p✝ = (expand p) p✝ →
      (frobenius (MvPolynomial σ (ZMod p)) p) q = (expand p) q →
        (frobenius (MvPolynomial σ (ZMod p)) p) p✝ + (frobenius (MvPolynomial σ (ZMod p)) p) q =
          (expand p) p✝ + (expand p) q
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: case mul_X
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
⊢ ∀ (p_1 : MvPolynomial σ (ZMod p)) (n : σ),
    (frobenius (MvPolynomial σ (ZMod p)) p) p_1 = (expand p) p_1 →
      (frobenius (MvPolynomial σ (ZMod p)) p) p_1 * (frobenius (MvPolynomial σ (ZMod p)) p) (X n) =
        (expand p) p_1 * X n ^ p

Tactic:
intro _

Goal state after:
case mul_X
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f p✝ : MvPolynomial σ (ZMod p)
⊢ ∀ (n : σ),
    (frobenius (MvPolynomial σ (ZMod p)) p) p✝ = (expand p) p✝ →
      (frobenius (MvPolynomial σ (ZMod p)) p) p✝ * (frobenius (MvPolynomial σ (ZMod p)) p) (X n) =
        (expand p) p✝ * X n ^ p
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 ∈ ⊤
n : σ → K
⊢ (evalₗ K σ) (∑ n, e n • indicator n) n = e n

Tactic:
simp only [evalₗ_apply, map_sum, smul_eval]

Goal state after:
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 ∈ ⊤
n : σ → K
⊢ ∑ x, e x * (eval n) (indicator x) = e n
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)
i : ι
e : Gal(K/F)
property✝ : e ∈ ⊤
⊢ ∏ x, e (x (u i)) = ∏ x, x (u i)

Tactic:
apply Fintype.prod_equiv (Equiv.mulLeft e)

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 := ⋯
u₁ : ι → K := ⋯
i : ι
e : Gal(K/F)
property✝ : e ∈ ⊤
⊢ ∀ (x : Gal(K/F)), e (x (u i)) = ((Equiv.mulLeft e) x) (u i)
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:
simp_rw [Equiv.coe_trans, Function.comp_apply, finCongr_apply, Equiv.ofBijective_apply,
    AlgEquiv.coe_pow, AdjoinRoot.powerBasis, AdjoinRoot.powerBasisAux, Basis.coe_mk,
    coe_comp, LinearEquiv.coe_coe, LinearMap.coe_restrictScalars]

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
⊢ (⇑(frobeniusAlgEquivOfAlgebraic K L))^[↑(Fin.cast ⋯ i)] x =
    (⇑(AEval'.of (frobeniusAlgHom K L).toLinearMap).symm ∘
        ⇑(liftQ (Ideal.span {X ^ finrank K L - 1})
            (toSpanSingleton K[X] (AEval' (frobeniusAlgHom K L).toLinearMap)
              ((AEval'.of (frobeniusAlgHom K L).toLinearMap) x))
            ⋯))
      (AdjoinRoot.root (X ^ finrank K L - C 1) ^ ↑i)
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: case neg
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
hi : IsSuccPrelimit i
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h : ¬Nonempty ↑(Iio i)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
apply AlgHom.ext

Goal state after:
case neg
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
hi : IsSuccPrelimit i
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h : ¬Nonempty ↑(Iio i)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)