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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite κ
hνκ : ν ≪ κ
h_meas : Measurable (μ.rnDeriv ν)
h_sing : μ.singularPart ν ⟂ₘ ν
hμν : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
x : α
⊢ (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x =
      ((μ.singularPart ν).rnDeriv κ + (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ) x →
    (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x = μ.rnDeriv ν x * ν.rnDeriv κ x →
      (μ.singularPart ν).rnDeriv κ x = 0 x → (μ.rnDeriv ν * ν.rnDeriv κ) x = μ.rnDeriv κ x

Tactic:
hx1

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite κ
hνκ : ν ≪ κ
h_meas : Measurable (μ.rnDeriv ν)
h_sing : μ.singularPart ν ⟂ₘ ν
hμν : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
x : α
hx1 :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x =
    ((μ.singularPart ν).rnDeriv κ + (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ) x
⊢ (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x = μ.rnDeriv ν x * ν.rnDeriv κ x →
    (μ.singularPart ν).rnDeriv κ x = 0 x → (μ.rnDeriv ν * ν.rnDeriv κ) x = μ.rnDeriv κ x
Module: Mathlib.Dynamics.TopologicalEntropy.Subset

Goal state before:
pp: X : Type u_1
T : X → X
F : Set X
inst✝ : UniformSpace X
h : Continuous T
U : Set (X × X)
U_uni : U ∈ 𝓤 X
V : Set (X × X)
V_uni : V ∈ 𝓤 X
V_U : V ○ V ⊆ U
⊢ coverEntropyInfEntourage T (closure F) U ≤ coverEntropyInf T F

Tactic:
exact le_iSup₂_of_le V V_uni ((coverEntropyInfEntourage_antitone T (closure F) V_U).trans
    (coverEntropyInfEntourage_closure h F V V_uni))

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

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

Tactic:
· exact (hf.rnDeriv_map_aux (withDensity_absolutelyContinuous _ _)).symm

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case inl
M : Type w
α : Type u'
β : Type v'
n m : ℕ
g : α → β ⊕ Fin n
v : β → M
xs : Fin (n + m) → M
x : α
⊢ Sum.elim v xs (Sum.map id (⇑finSumFinEquiv) ((Equiv.sumAssoc β (Fin n) (Fin m)) (Sum.inl (g x)))) =
    Sum.elim v (xs ∘ castAdd m) (g x)

Tactic:
rcases g x with l | r

Goal state after:
case inl.inl
M : Type w
α : Type u'
β : Type v'
n m : ℕ
g : α → β ⊕ Fin n
v : β → M
xs : Fin (n + m) → M
x : α
l : β
⊢ Sum.elim v xs (Sum.map id (⇑finSumFinEquiv) ((Equiv.sumAssoc β (Fin n) (Fin m)) (Sum.inl (Sum.inl l)))) =
    Sum.elim v (xs ∘ castAdd m) (Sum.inl l)

case inl.inr
M : Type w
α : Type u'
β : Type v'
n m : ℕ
g : α → β ⊕ Fin n
v : β → M
xs : Fin (n + m) → M
x : α
r : Fin n
⊢ Sum.elim v xs (Sum.map id (⇑finSumFinEquiv) ((Equiv.sumAssoc β (Fin n) (Fin m)) (Sum.inl (Sum.inr r)))) =
    Sum.elim v (xs ∘ castAdd m) (Sum.inr r)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
t : L.Term α
f : ↥t.varFinset → β
v : β → M
v' : α → M
hv' : ∀ (a : ↥t.varFinset), v (f a) = v' ↑a
⊢ realize v (t.restrictVar f) = realize v' t

Tactic:
induction t with
  | var => simp [restrictVar, hv']
  | func _ _ ih =>
    exact congr rfl (funext fun i => ih i ((by simp [Function.comp_apply, hv'])))

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Field.CharP

Goal state before:
pp: case pos
p : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
hp0 : p = 0
⊢ K ⊨ (fun q ↦ ∼(eqZero q)) '' {q | Nat.Prime q} ↔ CharP K p

Tactic:
subst hp0
    simp only [Theory.model_iff, Set.mem_image, Set.mem_ofPred_eq, Sentence.Realize,
      forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, Formula.realize_not,
      realize_eqZero, ← CharZero.charZero_iff_forall_prime_ne_zero]
    exact ⟨fun _ => CharP.ofCharZero _, fun _ => CharP.charP_to_charZero K⟩

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
α : Type u'
n : ℕ
f : L.BoundedFormula α n
⊢ (LHom.id L).onBoundedFormula f = id f

Tactic:
induction f with

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
L' : Language
α : Type u'
n : ℕ
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
f : L.BoundedFormula α n
⊢ (φ.comp ψ).onBoundedFormula f = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) f

Tactic:
induction f with

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: 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))

Tactic:
lift_add,

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

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
inst✝² : L.Structure M
inst✝¹ : L.Structure N
inst✝ : N ⊨ L.completeTheory M
φ : L.Sentence
h : ¬M ⊨ φ
⊢ ¬N ⊨ φ

Tactic:
rw [← Sentence.realize_not] at *

Goal state after:
L : Language
M : Type w
N : Type u_1
inst✝² : L.Structure M
inst✝¹ : L.Structure N
inst✝ : N ⊨ L.completeTheory M
φ : L.Sentence
h : M ⊨ Formula.not φ
⊢ N ⊨ Formula.not φ
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case imp
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 : ∀ (v : α ⊕ Fin n✝ → M), f₁✝.toFormula.Realize v ↔ f₁✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
ih2 : ∀ (v : α ⊕ Fin n✝ → M), f₂✝.toFormula.Realize v ↔ f₂✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n✝ → M
⊢ (f₁✝.toFormula ⟹ f₂✝.toFormula).Realize v default ↔ (f₁✝ ⟹ f₂✝).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)

Tactic:
realize_imp,

Goal state after:
case imp
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 : ∀ (v : α ⊕ Fin n✝ → M), f₁✝.toFormula.Realize v ↔ f₁✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
ih2 : ∀ (v : α ⊕ Fin n✝ → M), f₂✝.toFormula.Realize v ↔ f₂✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n✝ → M
⊢ Realize f₁✝.toFormula v default → Realize f₂✝.toFormula v default ↔ (f₁✝ ⟹ f₂✝).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: L : Language
α : Type u'
⊢ max ℵ₀
      (lift.{max (max u v) (max u u') v, u'} #α +
        (lift.{max (max u' v) (max u u') v, u} #((i : ℕ) × L.Functions i) +
          lift.{max (max u u') v, v} #((n : ℕ) × L.Relations n))) ≤
    max ℵ₀
      (lift.{max (max u v) (max u u') v, u'} #α +
        lift.{max u' (max u u') v, max u v}
          (lift.{v, u} #((l : ℕ) × L.Functions l) + lift.{u, v} #((l : ℕ) × L.Relations l)))

Tactic:
lift_add,

Goal state after:
L : Language
α : Type u'
⊢ max ℵ₀
      (lift.{max (max u v) (max u u') v, u'} #α +
        (lift.{max (max u' v) (max u u') v, u} #((i : ℕ) × L.Functions i) +
          lift.{max (max u u') v, v} #((n : ℕ) × L.Relations n))) ≤
    max ℵ₀
      (lift.{max (max u v) (max u u') v, u'} #α +
        (lift.{max (max u u') v, max u v} (lift.{v, u} #((l : ℕ) × L.Functions l)) +
          lift.{max (max u u') v, max u v} (lift.{u, v} #((l : ℕ) × L.Relations l))))
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : DecidableEq α
inst✝ : Nonempty M
φ : L.Formula α
v : α → M
hv : M ⊨ equivSentence φ
⊢ BoundedFormula.Realize φ v default

Tactic:
simpa [Formula.Realize]
          using (realize_equivSentence_symm M (Formula.equivSentence φ) v).2 hv

Goal state after:
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: case refine_1
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.{?u.120, w} (#↑s + #↑(⇑Equiv.ulift '' s')) ≤ lift.{?u.120, w} #↑(⇑Equiv.ulift '' s')

Tactic:
lift_add,

Goal state after:
case refine_1
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.{?u.121, w} #↑s + lift.{?u.121, w} #↑(⇑Equiv.ulift '' s') ≤ lift.{?u.121, w} #↑(⇑Equiv.ulift '' s')
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst✝² : Nonempty M
inst✝¹ : L.Structure M
inst✝ : M ⊨ T
h : Nonempty (↑s ↪ M)
this✝ : Inhabited M
this : (constantsOn α).Structure M := constantsOn.structure (Function.extend Subtype.val (⇑h.some) default)
a : α
as : a ∈ s
b : α
bs : b ∈ s
ab : (fun i ↦ ↑(L.con i)) a = (fun i ↦ ↑(L.con i)) b
⊢ ⟨a, as⟩ = ⟨b, bs⟩

Tactic:
exact
      h.some.injective
        ((Subtype.coe_injective.extend_apply h.some default ⟨a, as⟩).symm.trans
          (ab.trans (Subtype.coe_injective.extend_apply h.some default ⟨b, bs⟩)))

Goal state after:
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
⊢ (∼(eqZero p)).Realize v✝ xs✝

Tactic:
have := charP_of_model_fieldOfChar q K

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
⊢ (∼(eqZero p)).Realize v✝ xs✝
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: case intro
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
⊢ Submodule.map (evalₗ K σ) (restrictDegree σ K (Fintype.card K - 1)) = ⊤

Tactic:
refine top_unique (SetLike.le_def.2 fun e _ => mem_map.2 ?_)

Goal state after:
case intro
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
e : (σ → K) → K
x✝ : e ∈ ⊤
⊢ ∃ y ∈ restrictDegree σ K (Fintype.card K - 1), (evalₗ K σ) y = e
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Finite σ
⊢ (evalᵢ σ K).range = ⊤

Tactic:
rw [evalᵢ, LinearMap.range_comp, range_subtype]
  exact map_restrict_dom_evalₗ K σ

Goal state after:
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
⊢ Submodule.span L (Set.range fun k j ↦ j (e k)) = ⊤

Tactic:
apply span_flip_eq_top_iff_linearIndependent.mpr <|
      ((linearIndependent_algHom_toLinearMap K L L).comp _
        (algEquivEquivAlgHom K L).injective).map' _ (e.constr L).symm.ker

Goal state after:
Module: Mathlib.FieldTheory.CardinalEmb

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

Tactic:
exact (Subalgebra.equivOfEq _ _ <| adjoin_toSubalgebra_of_isAlgebraic
          fun x _ ↦ IsAlgebraic.isAlgebraic x) |>.toLinearEquiv.rank_eq.trans_lt <|
          (Algebra.rank_adjoin_le _).trans_lt (max_lt (mk_range_le.trans_lt this) lt)

Goal state after:
Module: Mathlib.FieldTheory.Galois.Profinite

Goal state before:
pp: case op.op.op
k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
L₁ L₂ : FiniteGaloisIntermediateField k K
f : op L₁ ⟶ op L₂
L₃ : FiniteGaloisIntermediateField k K
g : op L₂ ⟶ op L₃
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g

Tactic:
| _ L₃ =>

Goal state after:
case op.op.op
k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
L₁ L₂ : FiniteGaloisIntermediateField k K
f : op L₁ ⟶ op L₂
L₃ : FiniteGaloisIntermediateField k K
g : op L₂ ⟶ op L₃
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g
Module: Mathlib.FieldTheory.Galois.Profinite

Goal state before:
pp: case op.op.op.mk.mk.mk
k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
L₁ : IntermediateField k K
finiteDimensional✝² : FiniteDimensional k ↥L₁
isGalois✝² : IsGalois k ↥L₁
L₂ : IntermediateField k K
finiteDimensional✝¹ : FiniteDimensional k ↥L₂
isGalois✝¹ : IsGalois k ↥L₂
f :
  op { toIntermediateField := L₁, finiteDimensional := finiteDimensional✝², isGalois := isGalois✝² } ⟶
    op { toIntermediateField := L₂, finiteDimensional := finiteDimensional✝¹, isGalois := isGalois✝¹ }
L₃ : IntermediateField k K
finiteDimensional✝ : FiniteDimensional k ↥L₃
isGalois✝ : IsGalois k ↥L₃
g :
  op { toIntermediateField := L₂, finiteDimensional := finiteDimensional✝¹, isGalois := isGalois✝¹ } ⟶
    op { toIntermediateField := L₃, finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ }
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g

Tactic:
| _ L₃ =>

Goal state after:
case op.op.op.mk.mk.mk
k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
L₁ : IntermediateField k K
finiteDimensional✝² : FiniteDimensional k ↥L₁
isGalois✝² : IsGalois k ↥L₁
L₂ : IntermediateField k K
finiteDimensional✝¹ : FiniteDimensional k ↥L₂
isGalois✝¹ : IsGalois k ↥L₂
f :
  op { toIntermediateField := L₁, finiteDimensional := finiteDimensional✝², isGalois := isGalois✝² } ⟶
    op { toIntermediateField := L₂, finiteDimensional := finiteDimensional✝¹, isGalois := isGalois✝¹ }
L₃ : IntermediateField k K
finiteDimensional✝ : FiniteDimensional k ↥L₃
isGalois✝ : IsGalois k ↥L₃
g :
  op { toIntermediateField := L₂, finiteDimensional := finiteDimensional✝¹, isGalois := isGalois✝¹ } ⟶
    op { toIntermediateField := L₃, finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ }
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x1 x2 y : ℕ × K
H : R K p x1 x2
n : ℕ
x : K
⊢ R K p ((n, x).1 + y.1, (⇑(frobenius K p))^[y.1] (n, x).2 + (⇑(frobenius K p))^[(n, x).1] y.2)
    ((n + 1, (frobenius K p) x).1 + y.1,
      (⇑(frobenius K p))^[y.1] (n + 1, (frobenius K p) x).2 + (⇑(frobenius K p))^[(n + 1, (frobenius K p) x).1] y.2)

Tactic:
rw [← iterate_succ_apply, iterate_succ_apply', iterate_succ_apply', ← map_add,
        Nat.succ_add]

Goal state after:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x1 x2 y : ℕ × K
H : R K p x1 x2
n : ℕ
x : K
⊢ R K p ((n, x).1 + y.1, (⇑(frobenius K p))^[y.1] (n, x).2 + (⇑(frobenius K p))^[(n, x).1] y.2)
    ((n + y.1).succ, (frobenius K p) ((⇑(frobenius K p))^[y.1] x + (⇑(frobenius K p))^[n] y.2))
Module: Mathlib.FieldTheory.Galois.Profinite

Goal state before:
pp: k : Type u_3
K : Type u_4
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
L : FiniteGaloisIntermediateField k K
g : ↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
x : ↥L.toIntermediateField
L' : FiniteGaloisIntermediateField k K
h : L ≤ L'
⊢ ↑(((proj L) g) x) = ↑(((proj L') g) ⟨↑x, ⋯⟩)

Tactic:
induction L with

Goal state after:
case mk
k : Type u_3
K : Type u_4
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
g : ↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
L' : FiniteGaloisIntermediateField k K
L : IntermediateField k K
finiteDimensional✝ : FiniteDimensional k ↥L
isGalois✝ : IsGalois k ↥L
x : ↥{ toIntermediateField := L, finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ }.toIntermediateField
h : { toIntermediateField := L, finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ } ≤ L'
⊢ ↑(((proj { toIntermediateField := L, finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ }) g) x) =
    ↑(((proj L') g) ⟨↑x, ⋯⟩)
Module: Mathlib.RingTheory.Algebraic.LinearIndependent

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
H : ∀ (p : F[X]), (aeval x) p = 0 → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), x - (algebraMap F E) a ≠ 0
b : E := ∏ j ∈ s, (x - (algebraMap F E) j)
h1 : ∀ i ∈ s, m i • (b * (x - (algebraMap F E) i)⁻¹) = m i • ∏ j ∈ s.erase i, (x - (algebraMap F E) j)
hm : ∑ x_1 ∈ s, m x_1 • ∏ j ∈ s.erase x_1, (x - (algebraMap F E) j) = 0
p : F[X] := ∑ i ∈ s, C (m i) * ∏ j ∈ s.erase i, (X - C j)
⊢ ∑ x_1 ∈ s, (aeval x) (C (m x_1)) * ∏ x_2 ∈ s.erase x_1, ((aeval x) X - (aeval x) (C x_2)) =
    ∑ x_1 ∈ s, m x_1 • ∏ j ∈ s.erase x_1, (x - (algebraMap F E) j)

Tactic:
aeval_X,

Goal state after:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
H : ∀ (p : F[X]), (aeval x) p = 0 → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), x - (algebraMap F E) a ≠ 0
b : E := ∏ j ∈ s, (x - (algebraMap F E) j)
h1 : ∀ i ∈ s, m i • (b * (x - (algebraMap F E) i)⁻¹) = m i • ∏ j ∈ s.erase i, (x - (algebraMap F E) j)
hm : ∑ x_1 ∈ s, m x_1 • ∏ j ∈ s.erase x_1, (x - (algebraMap F E) j) = 0
p : F[X] := ∑ i ∈ s, C (m i) * ∏ j ∈ s.erase i, (X - C j)
⊢ ∑ x_1 ∈ s, (aeval x) (C (m x_1)) * ∏ x_2 ∈ s.erase x_1, (x - (aeval x) (C x_2)) =
    ∑ x_1 ∈ s, m x_1 • ∏ j ∈ s.erase x_1, (x - (algebraMap F E) j)
Module: Mathlib.RingTheory.Algebraic.LinearIndependent

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
H : ∀ (p : F[X]), (aeval x) p = 0 → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), x - (algebraMap F E) a ≠ 0
b : E := ∏ j ∈ s, (x - (algebraMap F E) j)
h1 : ∀ i ∈ s, m i • (b * (x - (algebraMap F E) i)⁻¹) = m i • ∏ j ∈ s.erase i, (x - (algebraMap F E) j)
p : F[X] := ∑ i ∈ s, C (m i) * ∏ j ∈ s.erase i, (X - C j)
h2 : ∀ j ∈ s.erase i, m j * ∏ x ∈ s.erase j, (i - x) = 0
hm : ∑ x ∈ s, (aeval i) (C (m x)) * ∏ x ∈ s.erase x, ((aeval i) X - (aeval i) (C x)) = 0
⊢ m i = 0

Tactic:
aeval_X,

Goal state after:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
H : ∀ (p : F[X]), (aeval x) p = 0 → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), x - (algebraMap F E) a ≠ 0
b : E := ∏ j ∈ s, (x - (algebraMap F E) j)
h1 : ∀ i ∈ s, m i • (b * (x - (algebraMap F E) i)⁻¹) = m i • ∏ j ∈ s.erase i, (x - (algebraMap F E) j)
p : F[X] := ∑ i ∈ s, C (m i) * ∏ j ∈ s.erase i, (X - C j)
h2 : ∀ j ∈ s.erase i, m j * ∏ x ∈ s.erase j, (i - x) = 0
hm : ∑ x ∈ s, (aeval i) (C (m x)) * ∏ x ∈ s.erase x, (i - (aeval i) (C x)) = 0
⊢ m i = 0
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝ : Field K
n : ℕ
ζ : K
hζ : IsPrimitiveRoot ζ n
α a : K
hn : 0 < n
e : α ^ n = a
⊢ X ^ n - C a = ∏ i ∈ Finset.range n, (X - C (ζ ^ i * α))

Tactic:
rw [(X_pow_sub_C_splits_of_isPrimitiveRoot hζ e).eq_prod_roots_of_monic
    (monic_X_pow_sub_C _ hn.ne'), ← nthRoots, hζ.nthRoots_eq e, Multiset.map_map]
  rfl

Goal state after:
Module: Mathlib.FieldTheory.JacobsonNoether

Goal state before:
pp: D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
H : k ≠ ⊤
p : ℕ
hp : ExpChar D p
insep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
a : D
ha : a ∉ k
ha₀ : a ≠ 0
b : D
hb1 : ((ad (↥k) D) a) b ≠ 0
n : ℕ
hn : 0 < n
c : D := (⇑((ad (↥k) D) a))^[n] b
hb : c ≠ 0 ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0
hc_def : c = (⇑((ad (↥k) D) a))^[n] b
x✝ : Invertible c := { invOf := c⁻¹, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }
hc : a * c = c * a
d : D := c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b
hd_def : d = c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b
hc' : c⁻¹ * a = a * c⁻¹
c_eq : a * (⇑((ad (↥k) D) a))^[n - 1] b - (⇑((ad (↥k) D) a))^[n - 1] b * a = c
eq1 : c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b - c⁻¹ * (⇑((ad (↥k) D) a))^[n - 1] b * a = 1
⊢ a * (c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b) - c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b * a = a * 1

Tactic:
← eq1,

Goal state after:
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
H : k ≠ ⊤
p : ℕ
hp : ExpChar D p
insep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
a : D
ha : a ∉ k
ha₀ : a ≠ 0
b : D
hb1 : ((ad (↥k) D) a) b ≠ 0
n : ℕ
hn : 0 < n
c : D := (⇑((ad (↥k) D) a))^[n] b
hb : c ≠ 0 ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0
hc_def : c = (⇑((ad (↥k) D) a))^[n] b
x✝ : Invertible c := { invOf := c⁻¹, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }
hc : a * c = c * a
d : D := c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b
hd_def : d = c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b
hc' : c⁻¹ * a = a * c⁻¹
c_eq : a * (⇑((ad (↥k) D) a))^[n - 1] b - (⇑((ad (↥k) D) a))^[n - 1] b * a = c
eq1 : c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b - c⁻¹ * (⇑((ad (↥k) D) a))^[n - 1] b * a = 1
⊢ a * (c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b) - c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b * a =
    a * (c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b - c⁻¹ * (⇑((ad (↥k) D) a))^[n - 1] b * a)
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
η : ↥(rootsOfUnity n K)
this : ↑↑η ^ n = 1
⊢ (aeval (↑↑η • root (X ^ n - C a))) X ^ n - (algebraMap K K[n√a]) a = 0

Tactic:
aeval_X,

Goal state after:
K : Type u
inst✝ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
η : ↥(rootsOfUnity n K)
this : ↑↑η ^ n = 1
⊢ (↑↑η • root (X ^ n - C a)) ^ n - (algebraMap K K[n√a]) a = 0