mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ (fun x ↦ (map f μ).rnDeriv (map f ν) (f x)) =ᵐ[ν] μ.rnDeriv ν

Tactic:
refine ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite ?_ ?_ (fun s _ _ ↦ ?_)
  · exact (Measure.measurable_rnDeriv _ _).comp hf.measurable
  · exact Measure.measurable_rnDeriv _ _
  rw [← hf.lintegral_map, Measure.setLIntegral_rnDeriv hμν]
  have hs_eq : s = f ⁻¹' f '' s := by rw [hf.injective.preimage_image]
  have : SigmaFinite (ν.map f) := hf.sigmaFinite_map
  rw [hs_eq, ← hf.restrict_map, Measure.setLIntegral_rnDeriv (hf.absolutelyContinuous_map hμν),
    hf.map_apply]

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case h
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : (map i (X ^ n - C a)).Splits
ha' : i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : (X ^ n - C a).degree ≠ 0
b : E
hb : b ^ n = i a
hb' : b ≠ 0
s : Multiset E := (map i (X ^ n - C a)).roots
hs : map i (X ^ n - C a) = (Multiset.map (fun x ↦ X - C x) s).prod
hs' : s.card = n
C_mul_C : C (i a⁻¹) * C (i a) = 1
key1 : map i (X ^ n - 1) = C (i a⁻¹) * (map i (X ^ n - C a)).comp (C b * X)
key2 : ((fun q ↦ q.comp (C b * X)) ∘ fun c ↦ X - C c) = fun c ↦ C b * (X - C (c / b))
⊢ C (i a⁻¹) * (Multiset.map (fun x ↦ X - C x) s).prod.comp (C b * X) =
    (Multiset.map ((fun x ↦ X - C x) ∘ fun c ↦ c / b) s).prod

Tactic:
multiset_prod_comp,

Goal state after:
case h
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : (map i (X ^ n - C a)).Splits
ha' : i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : (X ^ n - C a).degree ≠ 0
b : E
hb : b ^ n = i a
hb' : b ≠ 0
s : Multiset E := (map i (X ^ n - C a)).roots
hs : map i (X ^ n - C a) = (Multiset.map (fun x ↦ X - C x) s).prod
hs' : s.card = n
C_mul_C : C (i a⁻¹) * C (i a) = 1
key1 : map i (X ^ n - 1) = C (i a⁻¹) * (map i (X ^ n - C a)).comp (C b * X)
key2 : ((fun q ↦ q.comp (C b * X)) ∘ fun c ↦ X - C c) = fun c ↦ C b * (X - C (c / b))
⊢ C (i a⁻¹) * (Multiset.map (fun p ↦ p.comp (C b * X)) (Multiset.map (fun x ↦ X - C x) s)).prod =
    (Multiset.map ((fun x ↦ X - C x) ∘ fun c ↦ c / b) s).prod
Module: Mathlib.FieldTheory.AbelRuffini

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

Tactic:
map_id

Goal state after:
case neg.hq
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : ¬x = 0
⊢ (X ^ n - 1).Splits
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃[L] N
⊢ f.toEmbedding.comp f.symm.toEmbedding = Embedding.refl L N

Tactic:
by
  rw [← comp_toEmbedding, self_comp_symm, refl_toEmbedding]

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: 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
⊢ (aeval (x ^ n)) p = 0

Tactic:
minpoly.aeval

Goal state after:
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
⊢ 0 = 0
Module: Mathlib.ModelTheory.Syntax

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

Tactic:
cases n <;> · simp [varsToConstants, constantsToVars, ih]

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
α : Type u'
k m n : ℕ
km : k ≤ m
mn : m ≤ n
φ : L.BoundedFormula α k
⊢ castLE mn (castLE km φ) = castLE ⋯ φ

Tactic:
revert m n
  induction φ with
  | falsum => intros; rfl
  | equal => simp
  | rel =>
    intros
    simp only [castLE]
    rw [← Function.comp_assoc, Term.relabel_comp_relabel]
    simp
  | imp _ _ ih1 ih2 => simp [ih1, ih2]
  | all _ ih3 => intros; simp only [castLE, ih3]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
f : L.Functions 1
t : L.Term α
v : α → M
⊢ realize v (f.apply₁ t) = funMap f ![realize v t]

Tactic:
rw [Functions.apply₁, Term.realize]
  refine congr rfl (funext fun i => ?_)
  simp only [Matrix.cons_val_fin_one]

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case mul
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x y z : E
hy : y ∈ solvableByRad F E
hz : z ∈ solvableByRad F E
hy' : Group.IsSolvable (minpoly F y).Gal
hz' : Group.IsSolvable (minpoly F z).Gal
⊢ Group.IsSolvable (minpoly F (y * z)).Gal

Tactic:
apply induction_step hy hz (mul_mem hy hz) hy' hz' (mul_mem ..)

Goal state after:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x y z : E
hy : y ∈ solvableByRad F E
hz : z ∈ solvableByRad F E
hy' : Group.IsSolvable (minpoly F y).Gal
hz' : Group.IsSolvable (minpoly F z).Gal
⊢ y ∈ F⟮y, z⟯

F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x y z : E
hy : y ∈ solvableByRad F E
hz : z ∈ solvableByRad F E
hy' : Group.IsSolvable (minpoly F y).Gal
hz' : Group.IsSolvable (minpoly F z).Gal
⊢ z ∈ F⟮y, z⟯
Module: Mathlib.ModelTheory.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
⊢ ∀ φ ∈ Theory.field, K ⊨ φ

Tactic:
simp only [Theory.field, Set.mem_range, exists_imp]
      rintro φ a rfl
      rw [a.realize_toSentence_iff_toProp (K := K)]
      cases a with
      | existsPairNE => exact exists_pair_ne K
      | existsInv => exact fun x hx0 => ⟨x⁻¹, mul_inv_cancel₀ hx0⟩
      | addAssoc => exact add_assoc
      | zeroAdd => exact zero_add
      | negAddCancel => exact neg_add_cancel
      | mulAssoc => exact mul_assoc
      | mulComm => exact mul_comm
      | oneMul => exact one_mul
      | leftDistrib => exact mul_add

Goal state after:
Module: Mathlib.ModelTheory.Quotients

Goal state before:
pp: L : Language
M : Type u_1
s : Setoid M
ps : L.Prestructure s
n : ℕ
f : L.Functions n
x : Fin n → M
⊢ Quotient.map (funMap f) ⋯ (Quotient.finChoice fun i ↦ ⟦x i⟧) = ⟦funMap f x⟧

Tactic:
Quotient.finChoice_eq,

Goal state after:
L : Language
M : Type u_1
s : Setoid M
ps : L.Prestructure s
n : ℕ
f : L.Functions n
x : Fin n → M
⊢ Quotient.map (funMap f) ⋯ ⟦x⟧ = ⟦funMap f x⟧
Module: Mathlib.ModelTheory.Quotients

Goal state before:
pp: L : Language
M : Type u_1
s : Setoid M
ps : L.Prestructure s
n : ℕ
r : L.Relations n
x : Fin n → M
⊢ Quotient.lift (RelMap r) ⋯ (Quotient.finChoice fun i ↦ ⟦x i⟧) ↔ RelMap r x

Tactic:
Quotient.finChoice_eq,

Goal state after:
L : Language
M : Type u_1
s : Setoid M
ps : L.Prestructure s
n : ℕ
r : L.Relations n
x : Fin n → M
⊢ Quotient.lift (RelMap r) ⋯ ⟦x⟧ ↔ RelMap r x
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
m n : ℕ
φ : L.BoundedFormula α n
g : α → β ⊕ Fin m
v : β → M
xs : Fin (m + n) → M
⊢ (relabel g φ).Realize v xs ↔ φ.Realize (Sum.elim v (xs ∘ castAdd n) ∘ g) (xs ∘ natAdd m)

Tactic:
apply realize_mapTermRel_add_castLe

Goal state after:
case h1
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
m n : ℕ
φ : L.BoundedFormula α n
g : α → β ⊕ Fin m
v : β → M
xs : Fin (m + n) → M
⊢ ∀ (n : ℕ) (t : L.Term (α ⊕ Fin n)) (xs' : Fin (m + n) → M),
    realize (Sum.elim v xs') (Term.relabel (relabelAux g n) t) =
      realize (Sum.elim (Sum.elim v (xs' ∘ castAdd n) ∘ g) (xs' ∘ natAdd m)) t

case h2
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
m n : ℕ
φ : L.BoundedFormula α n
g : α → β ⊕ Fin m
v : β → M
xs : Fin (m + n) → M
⊢ ∀ (n : ℕ) (R : L.Relations n) (x : Fin n → M), RelMap (id R) x = RelMap R x

case hv
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
m n : ℕ
φ : L.BoundedFormula α n
g : α → β ⊕ Fin m
v : β → M
xs : Fin (m + n) → M
⊢ ∀ (n : ℕ) (xs : Fin (m + n) → M) (x : M),
    Sum.elim v (snoc xs x ∘ castAdd (n + 1)) ∘ g = Sum.elim v (xs ∘ castAdd n) ∘ g
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case all.refine_1
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
k : ℕ
f✝ : L.BoundedFormula α (k + 1)
ih3 :
  ∀ {xs : Fin (k + 1 + n') → M},
    m ≤ k + 1 →
      ((mapTermRel (fun x t ↦ Term.liftAt n' m t) (fun x ↦ id) (fun x ↦ castLE ⋯) f✝).Realize v xs ↔
        f✝.Realize v (xs ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n'))
xs : Fin (k + n') → M
hmn : m ≤ k
h : k + 1 + n' = k + n' + 1
x : M
⊢ ↑(Fin.cast h (if k < m then castAdd n' (last k) else (last k).addNat n')) = ↑(last (k + n'))

Tactic:
split_ifs <;> dsimp

Goal state after:
case pos
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
k : ℕ
f✝ : L.BoundedFormula α (k + 1)
ih3 :
  ∀ {xs : Fin (k + 1 + n') → M},
    m ≤ k + 1 →
      ((mapTermRel (fun x t ↦ Term.liftAt n' m t) (fun x ↦ id) (fun x ↦ castLE ⋯) f✝).Realize v xs ↔
        f✝.Realize v (xs ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n'))
xs : Fin (k + n') → M
hmn : m ≤ k
h : k + 1 + n' = k + n' + 1
x : M
h✝ : k < m
⊢ k = k + n'
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case refine_1
L : Language
α : Type u'
i : ℕ
⊢ lift.{u, u'} (lift.{0, u'} #α + lift.{u', 0} #(Fin i)) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))

Tactic:
add_comm (Cardinal.lift #α),

Goal state after:
case refine_1
L : Language
α : Type u'
i : ℕ
⊢ lift.{u, u'} (lift.{u', 0} #(Fin i) + lift.{0, u'} #α) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
Module: Mathlib.ModelTheory.ElementarySubstructures

Goal state before:
pp: L : Language
M : Type u_1
inst✝ : L.Structure M
A : Set M
hA : MeetsDefinable A
⊢ ((closure L).toFun A).IsElementary

Tactic:
refine isElementary_of_exists ((closure L).toFun A) ?_
  intro n φ x a hφ
  let D : Set M := {y : M | φ.Realize default (Fin.snoc (Subtype.val ∘ x) y)}
  have hD_ne : D.Nonempty := ⟨a,hφ⟩
  have hD : A.Definable₁ L D := by
    simp only [Definable₁, Definable, Fin.isValue]
    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, ?_⟩
    ext v
    simp only [Fin.isValue, mem_ofPred_eq, Formula.relabel, Formula.Realize,
      BoundedFormula.realize_subst, BoundedFormula.realize_relabel, Nat.add_zero, Fin.castAdd_zero,
      Fin.cast_refl, Function.comp_id, Fin.natAdd_zero, D]
    rw [← Formula.Realize, BoundedFormula.realize_toFormula, LHom.realize_onBoundedFormula]
    congr! 1
    ext i; cases i using Fin.lastCases <;> simp
  obtain ⟨b, hbD, hbA⟩ := hA D hD_ne hD
  exact ⟨⟨b, by rwa [← hA.closure_eq_self] at hbA⟩, hbD⟩

Goal state after:
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: case h
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : L.Structure M
S : (L.sum L.skolem₁).Substructure M
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x : Fin n → ↥(LHom.sumInl.substructureReduct S)
a : M
h : φ.Realize default (Fin.snoc (Subtype.val ∘ x) a)
φ' : (L.sum L.skolem₁).Functions n := ⋯
⊢ φ.Realize default (Fin.snoc (Subtype.val ∘ x) ↑⟨funMap φ' (Subtype.val ∘ x), ?w⟩)

Tactic:
exact Classical.epsilon_spec (p := fun a => BoundedFormula.Realize φ default
          (Fin.snoc (Subtype.val ∘ x) a)) ⟨a, h⟩

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case refine_1
L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
xs : Fin n → M
h :
  ∀ (φ : L.BoundedFormula Empty n) (x x_1 : Fin n),
    (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize default xs
⊢ Nonempty (Fin n ↪ M)

Tactic:
refine ⟨⟨xs, fun i j ij => ?_⟩⟩

Goal state after:
case refine_1
L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
xs : Fin n → M
h :
  ∀ (φ : L.BoundedFormula Empty n) (x x_1 : Fin n),
    (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize default xs
i j : Fin n
ij : xs i = xs j
⊢ i = j
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case refine_2
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : (L.lhomWithConstants α).onTheory T ⊨ᵇ Formula.equivSentence φ
M : T.ModelType
v : α → ↑M
⊢ φ.Realize v

Tactic:
· let : (constantsOn α).Structure M := constantsOn.structure v
    have : M ⊨ (L.lhomWithConstants α).onTheory T := (LHom.onTheory_model _ _).2 inferInstance
    exact (Formula.realize_equivSentence _ _).1 (h.realize_sentence M)

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
h : T.IsComplete
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
φ : L.BoundedFormula Empty 0
h_realize : M ⊨ φ
⊢ T ⊨ᵇ φ

Tactic:
cases h.2 φ with
  | inl hT => exact hT
  | inr hT =>
      have : M ⊨ φ.not := hT.realize_sentence M
      rw [Sentence.realize_not] at this
      contradiction

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
⊢ T.IsComplete ↔ T.IsSatisfiable ∧ ∀ (M N : T.ModelType), ↑M ≅[L] ↑N

Tactic:
by
  constructor
  · intro hcomp
    refine ⟨hcomp.1, ?_⟩
    intro M N
    rw [ElementarilyEquivalent, ← hcomp.eq_complete_theory, ← hcomp.eq_complete_theory]
  · rintro ⟨hsat, h⟩
    refine ⟨hsat, ?_⟩
    intro φ
    obtain ⟨M⟩ := hsat
    by_cases hφ : M ⊨ φ
    · left
      exact models_sentence_iff.2 fun N => (elementarilyEquivalent_iff.1 (h M N) φ).1 hφ
    · right
      exact models_sentence_iff.2 fun N => (Sentence.realize_not N).2
        (mt (elementarilyEquivalent_iff.1 (h M N) φ).2 hφ)

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
h : T.IsComplete
M : Type u_1
N : Type u_2
inst✝⁵ : L.Structure M
inst✝⁴ : L.Structure N
inst✝³ : M ⊨ T
inst✝² : N ⊨ T
inst✝¹ : Nonempty M
inst✝ : Nonempty N
⊢ {φ | T ⊨ᵇ φ} = L.completeTheory N

Tactic:
← h.eq_complete_theory

Goal state after:
L : Language
T : L.Theory
h : T.IsComplete
M : Type u_1
N : Type u_2
inst✝⁵ : L.Structure M
inst✝⁴ : L.Structure N
inst✝³ : M ⊨ T
inst✝² : N ⊨ T
inst✝¹ : Nonempty M
inst✝ : Nonempty N
⊢ {φ | T ⊨ᵇ φ} = {φ | T ⊨ᵇ φ}
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: case refine_3
n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
⊢ ↑n ∣ b ∨ ↑n ∣ c

Tactic:
rcases lt_or_ge (b * c) ℵ₀ with h' | h'

Goal state after:
case refine_3.inl
n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : b * c < ℵ₀
⊢ ↑n ∣ b ∨ ↑n ∣ c

case refine_3.inr
n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
⊢ ↑n ∣ b ∨ ↑n ∣ c
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: K : Type u_1
σ : Type u_2
inst✝ : CommSemiring K
p q : MvPolynomial σ K
⊢ (fun e ↦ (eval e) (p + q)) = (fun e ↦ (eval e) p) + fun e ↦ (eval e) q

Tactic:
ext x; simp

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

Goal state before:
pp: case a
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′
| ∑ x, ↑(c x) * logDeriv ↑(u x)

pp: case a
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′
| (↑v)′

Tactic:
· rhs
        intro x
        rhs
        apply logDeriv_algebraMap (u x)

Goal state after:
case a
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′
| (↑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)
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 : ι₀), (c₀ x)′ = 0), ∃ u₀ v₀, a = ∑ x, c₀ x * logDeriv (u₀ x) + v₀′

Tactic:
exists ι, inferInstance, c₀, ?_, u₀, v₀

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

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.PerfectClosure

Goal state before:
pp: case succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℕ × K
n : ℕ
ih : mk K p x ^ n = mk K p (x.1, x.2 ^ n)
⊢ mk K p x ^ (n + 1) = mk K p (x.1, x.2 ^ (n + 1))

Tactic:
rw [pow_succ, pow_succ, ih, mk_mul_mk, mk_eq_iff]
    exact ⟨0, by simp_rw [iterate_frobenius, add_zero, mul_pow, ← pow_mul,
      ← pow_add, mul_assoc, ← pow_add]⟩

Goal state after:
Module: Mathlib.FieldTheory.Isaacs

Goal state before:
pp: F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ y, (aeval y) (minpoly F x) = 0
S : Finset E
p : K[X] := ∏ x ∈ S, Polynomial.map (algebraMap F K) (minpoly F x)
K' : Type u_3 := p.SplittingField
splits : ∀ s ∈ S, (Polynomial.map (algebraMap F K') (minpoly F s)).Splits
K₀ : IntermediateField F K' := restrictScalars F ⊥
FS : IntermediateField F E := adjoin F ↑S
Ω : Type (max u_2 u_3) := ↥FS →ₐ[F] K'
this : FiniteDimensional F ↥(adjoin F ↑S)
M : Ω → Submodule F ↥FS := fun ω ↦ Subalgebra.toSubmodule (comap ω K₀).toSubalgebra
x✝ : ↥FS
α : E
hα : α ∈ FS
β : K
hβ : (aeval β) (minpoly F α) = 0
ϕ : ↥F⟮α⟯ →ₐ[F] K' :=
  (IsScalarTower.toAlgHom F K K').comp
    ((AdjoinRoot.liftAlgHom (minpoly F α) (Algebra.ofId F K) β hβ).comp ↑(adjoinRootEquivAdjoin F ⋯).symm)
ω : ↥(adjoin F ↑S) →ₐ[F] K'
hω : ω.comp (inclusion ⋯) = ϕ
⊢ ϕ (AdjoinSimple.gen F α) = (Algebra.ofId K K').toRingHom β

Tactic:
AlgHom.comp_apply,

Goal state after:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ y, (aeval y) (minpoly F x) = 0
S : Finset E
p : K[X] := ∏ x ∈ S, Polynomial.map (algebraMap F K) (minpoly F x)
K' : Type u_3 := p.SplittingField
splits : ∀ s ∈ S, (Polynomial.map (algebraMap F K') (minpoly F s)).Splits
K₀ : IntermediateField F K' := restrictScalars F ⊥
FS : IntermediateField F E := adjoin F ↑S
Ω : Type (max u_2 u_3) := ↥FS →ₐ[F] K'
this : FiniteDimensional F ↥(adjoin F ↑S)
M : Ω → Submodule F ↥FS := fun ω ↦ Subalgebra.toSubmodule (comap ω K₀).toSubalgebra
x✝ : ↥FS
α : E
hα : α ∈ FS
β : K
hβ : (aeval β) (minpoly F α) = 0
ϕ : ↥F⟮α⟯ →ₐ[F] K' :=
  (IsScalarTower.toAlgHom F K K').comp
    ((AdjoinRoot.liftAlgHom (minpoly F α) (Algebra.ofId F K) β hβ).comp ↑(adjoinRootEquivAdjoin F ⋯).symm)
ω : ↥(adjoin F ↑S) →ₐ[F] K'
hω : ω.comp (inclusion ⋯) = ϕ
⊢ (IsScalarTower.toAlgHom F K K')
      (((AdjoinRoot.liftAlgHom (minpoly F α) (Algebra.ofId F K) β hβ).comp ↑(adjoinRootEquivAdjoin F ⋯).symm)
        (AdjoinSimple.gen F α)) =
    (Algebra.ofId K K').toRingHom β