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

Goal state before:
pp: 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
⊢ map i (X ^ n - 1) = C (i a⁻¹) * (map i (X ^ n - C a)).comp (C b * X)

Tactic:
rw [Polynomial.map_sub, Polynomial.map_sub, Polynomial.map_pow, map_X, map_C,
      Polynomial.map_one, sub_comp, pow_comp, X_comp, C_comp, mul_pow, ← C_pow, hb, mul_sub, ←
      mul_assoc, C_mul_C, one_mul]

Goal state after:
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:
have hr : ϕ.onRelation r ∈ Set.range fun r : L.Relations n => ϕ.onRelation r := ⟨r, rfl⟩
    refine (dif_pos hr).trans ?_
    rw [h.onRelation hr.choose_spec]

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
α : Type u'
t : L.Term α
⊢ relabel id t = t

Tactic:
induction t with

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
α : Type u'
β : Type v'
γ : Type u_1
f : α → β
g : β → γ
t : L.Term α
⊢ relabel g (relabel f t) = relabel (g ∘ f) t

Tactic:
induction t with

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
t : L[[γ]].Term α
⊢ t.constantsToVars.varsToConstants = t

Tactic:
induction t with

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
t : L.Term (γ ⊕ α)
⊢ t.varsToConstants.constantsToVars = t

Tactic:
induction t with

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
α : Type u'
t : L.Term α
⊢ (LHom.id L).onTerm t = id t

Tactic:
induction t with

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
L' : Language
α : Type u'
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
t : L.Term α
⊢ (φ.comp ψ).onTerm t = (φ.onTerm ∘ ψ.onTerm) t

Tactic:
induction t with

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
t : L.Term α
g : α → β
v : β → M
⊢ realize v (relabel g t) = realize (v ∘ g) t

Tactic:
induction t with

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 y z : E
hx : x ∈ solvableByRad F E
hy : y ∈ solvableByRad F E
hz : z ∈ solvableByRad F E
hx' : Group.IsSolvable (minpoly F x).Gal
hy' : Group.IsSolvable (minpoly F y).Gal
hz' : z ∈ F⟮x, y⟯
⊢ Group.IsSolvable (minpoly F z).Gal

Tactic:
by
  let p := minpoly F x
  let q := minpoly F y
  have hpq := SplittingField.splits (p * q)
  rw [Polynomial.map_mul,
    splits_mul (map_ne_zero (minpoly.ne_zero (isIntegral_of_mem_solvableByRad hx)))
      (map_ne_zero (minpoly.ne_zero (isIntegral_of_mem_solvableByRad hy)))] at hpq
  have f : ↥F⟮x, y⟯ →ₐ[F] (p * q).SplittingField :=
    Classical.choice <| nonempty_algHom_adjoin_of_splits <| by
      rintro a (rfl | rfl)
      · exact ⟨isIntegral_of_mem_solvableByRad hx, hpq.1⟩
      · exact ⟨isIntegral_of_mem_solvableByRad hy, hpq.2⟩
  have key : minpoly F z = minpoly F (f ⟨z, hz'⟩) := by
    refine minpoly.eq_of_irreducible_of_monic
      (minpoly.irreducible (isIntegral_of_mem_solvableByRad hz)) ?_
      (minpoly.monic (isIntegral_of_mem_solvableByRad hz))
    rw [aeval_algHom_apply, map_eq_zero]
    apply (algebraMap (↥F⟮x, y⟯) E).injective
    simp [← aeval_algebraMap_apply]
  rw [key]
  refine gal_isSolvable_of_splits ⟨Normal.splits ?_ (f ⟨z, hz'⟩)⟩ (gal_mul_isSolvable hx' hy')
  infer_instance

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
t : L.Term α
tf : α → L.Term β
v : β → M
⊢ realize v (t.subst tf) = realize (fun a ↦ realize v (tf a)) t

Tactic:
induction t with

Goal state after:
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

Goal state after:
Module: Mathlib.ModelTheory.Quotients

Goal state before:
pp: L : Language
M : Type u_1
s : Setoid M
ps : L.Prestructure s
β : Type u_2
t : L.Term β
x : β → M
⊢ realize (fun i ↦ ⟦x i⟧) t = ⟦realize x t⟧

Tactic:
induction t with

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
γ : Type u_4
t : L.Term (α ⊕ γ)
f : ↥t.varFinsetLeft → β
xs : β ⊕ γ → M
xs' : α → M
hxs' : ∀ (a : ↥t.varFinsetLeft), xs (Sum.inl (f a)) = xs' ↑a
⊢ realize xs (t.restrictVarLeft f) = realize (Sum.elim xs' (xs ∘ Sum.inr)) t

Tactic:
induction t with

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
t : L[[α]].Term β
v : β → M
⊢ realize (Sum.elim (fun a ↦ ↑(L.con a)) v) t.constantsToVars = realize v t

Tactic:
induction t with

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
t : L.Term (α ⊕ β)
v : β → M
⊢ realize v t.varsToConstants = realize (Sum.elim (fun a ↦ ↑(L.con a)) v) t

Tactic:
induction t with

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
L' : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L'.Structure M
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
t : L.Term α
v : α → M
⊢ Term.realize v (φ.onTerm t) = Term.realize v t

Tactic:
induction t with

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
L' : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L'.Structure M
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
t : L.Term α
v : α → M
⊢ Term.realize v (φ.onTerm t) = Term.realize v t

Tactic:
by
  induction t with
  | var => rfl
  | func f ts ih => simp only [Term.realize, LHom.onTerm, LHom.map_onFunction, ih]

Goal state after:
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: case e'_3.e'_3
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → L.Structure (M a)
β : Type u_3
x : β → (a : α) → M a
t : L.Term β
a : α
⊢ Term.realize (fun i ↦ x i a) t = Term.realize x t a

Tactic:
induction t with

Goal state after:
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: case equal
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → L.Structure (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
n✝ : ℕ
t₁✝ t₂✝ : L.Term (β ⊕ Fin n✝)
v : Fin n✝ → (a : α) → M a
h2 : ∀ (a : α), (Sum.elim (fun i ↦ x i a) fun i ↦ v i a) = fun i ↦ Sum.elim x v i a
⊢ (Quotient.mk' fun a ↦ Term.realize (fun i ↦ Sum.elim x v i a) t₁✝) = Term.realize (Quotient.mk' ∘ Sum.elim x v) t₂✝ ↔
    ∀ᶠ (a : α) in ↑u, Term.realize (fun i ↦ Sum.elim x v i a) t₁✝ = Term.realize (fun i ↦ Sum.elim x v i a) t₂✝

Tactic:
term_realize_cast

Goal state after:
case equal
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → L.Structure (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
n✝ : ℕ
t₁✝ t₂✝ : L.Term (β ⊕ Fin n✝)
v : Fin n✝ → (a : α) → M a
h2 : ∀ (a : α), (Sum.elim (fun i ↦ x i a) fun i ↦ v i a) = fun i ↦ Sum.elim x v i a
⊢ ((Quotient.mk' fun a ↦ Term.realize (fun i ↦ Sum.elim x v i a) t₁✝) =
      Quotient.mk' fun a ↦ Term.realize (fun i ↦ Sum.elim x v i a) t₂✝) ↔
    ∀ᶠ (a : α) in ↑u, Term.realize (fun i ↦ Sum.elim x v i a) t₁✝ = Term.realize (fun i ↦ Sum.elim x v i a) t₂✝
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → L.Structure (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (β ⊕ Fin n✝)
v : Fin n✝ → (a : α) → M a
h2 : ∀ (a : α), (Sum.elim (fun i ↦ x i a) fun i ↦ v i a) = fun i ↦ Sum.elim x v i a
i : Fin l✝
| Term.realize (Quotient.mk' ∘ Sum.elim x v) (ts✝ i)

Tactic:
term_realize_cast

Goal state after:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → L.Structure (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (β ⊕ Fin n✝)
v : Fin n✝ → (a : α) → M a
h2 : ∀ (a : α), (Sum.elim (fun i ↦ x i a) fun i ↦ v i a) = fun i ↦ Sum.elim x v i a
i : Fin l✝
| Quotient.mk' fun a ↦ Term.realize (fun i ↦ Sum.elim x v i a) (ts✝ i)
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
S : L.Substructure M
α : Type u_3
t : L.Term α
xs : α → M
h : ∀ (a : α), xs a ∈ S
⊢ realize xs t ∈ S

Tactic:
induction t with

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: case succ
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝³ : L.Structure M
inst✝² : L.Structure N
inst✝¹ : L.Structure P
S : L.Substructure M
s : Set M
inst✝ : IsEmpty L.Constants
x✝ : M
n✝ : ℕ
f : L.Functions (n✝ + 1)
x : Fin (n✝ + 1) → M
hx : ∀ (i : Fin (n✝ + 1)), x i ∈ ∅
⊢ funMap f x ∈ ∅

Tactic:
simp only [mem_empty_iff_false, forall_const] at hx

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃[L] N
n : N
⊢ n ∈ f.toHom.range ↔ n ∈ ⊤

Tactic:
simp only [Hom.mem_range, coe_toHom, Substructure.mem_top, iff_true]

Goal state after:
L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃[L] N
n : N
⊢ ∃ y, f y = n
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝² : L.Structure M
α : Type u₁
L' : Language
inst✝¹ : L'.Structure M
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
ψ : L[[↑A]].Formula α
⊢ A.Definable L' (ofPred ψ.Realize)

Tactic:
refine ⟨(φ.addConstants A).onFormula ψ, ?_⟩

Goal state after:
M : Type w
A : Set M
L : Language
inst✝² : L.Structure M
α : Type u₁
L' : Language
inst✝¹ : L'.Structure M
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
ψ : L[[↑A]].Formula α
⊢ ofPred ψ.Realize = ofPred ((LHom.addConstants (↑A) φ).onFormula ψ).Realize
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: L : Language
⊢ #((n : ℕ) × (L.sum L.skolem₁).Functions n) = #((n : ℕ) × L.BoundedFormula Empty (n + 1))

Tactic:
simp only [card_functions_sum, skolem₁_Functions, mk_sigma, sum_add_distrib']

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

Goal state before:
pp: L : Language
⊢ ℵ₀ ≤ sum fun i ↦ #(L.BoundedFormula Empty (i + 1))

Tactic:
rw [← mk_sigma]
    exact infinite_iff.1 (Infinite.of_injective (fun n => ⟨n, ⊥⟩) fun x y xy =>
      (Sigma.mk.inj_iff.1 xy).1)

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
r : L.Relations 2
⊢ M ⊨ r.antisymmetric ↔ ∀ ⦃a b : M⦄, RelMap r ![a, b] → RelMap r ![b, a] → a = b

Tactic:
exact forall₂_congr fun _ _ ↦ imp_congr realize_rel₂ <| imp_congr realize_rel₂ .rfl

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

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

Tactic:
obtain ⟨NT, MNT, hNT⟩ := exists_elementarilyEquivalent_card_eq L MT κ h1 h2

Goal state after:
L : Language
κ : Cardinal.{w}
T : L.Theory
h : κ.Categorical T
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
hS : T.IsSatisfiable
hT : ∀ (M : T.ModelType), Infinite ↑M
φ : L.Sentence
w✝ : T.ModelType
h✝ : #↑w✝ = κ
MF : T.ModelType
hMF : ¬↑MF ⊨ φ
MT : T.ModelType
hMT : ↑MT ⊨ φ
this✝ : Infinite ↑MT
this : Infinite ↑MF
NT : Bundled L.Structure
MNT : ↑MT ≅[L] ↑NT
hNT : #↑NT = κ
⊢ ↑MF ⊨ φ
Module: Mathlib.GroupTheory.OreLocalization.Cardinality

Goal state before:
pp: R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite ↥S
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i = s ^ j
hlt : j < i
⊢ ∃ a, (fun x ↦ x /ₒ 1) a = x /ₒ s

Tactic:
use s ^ (i - (j + 1)) • x

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

Goal state before:
pp: R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite X
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i • x = s ^ j • x
hlt : j < i
⊢ ∃ a, (fun x ↦ x /ₒ 1) a = x /ₒ s

Tactic:
use s ^ (i - (j + 1)) • x

Goal state after:
case h
R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite X
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i • x = s ^ j • x
hlt : j < i
⊢ (fun x ↦ x /ₒ 1) (s ^ (i - (j + 1)) • x) = x /ₒ s
Module: Mathlib.FieldTheory.Finite.Extension

Goal state before:
pp: case inr.inr
k : Type u_1
inst✝ : Field k
f : k[X]
hi : Irreducible f
n : ℕ
h : f ∣ X ^ 0 - X
hn : n ≠ 0
h✝ : Infinite k
⊢ f.natDegree ∣ n

Tactic:
pow_zero,

Goal state after:
case inr.inr
k : Type u_1
inst✝ : Field k
f : k[X]
hi : Irreducible f
n : ℕ
h : f ∣ 1 - X
hn : n ≠ 0
h✝ : Infinite k
⊢ f.natDegree ∣ n
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ Multiset.count n (∏ n, (1 - (X n - C (c n)) ^ (Fintype.card K - 1))).degrees ≤ Fintype.card K - 1

Tactic:
refine le_trans (Multiset.count_le_of_le _ <| degrees_indicator _) (le_of_eq ?_)

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

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : DiscreteTopology X
x y : X
hxy : x ≠ y
⊢ False

Tactic:
rw [Ne, ← mem_singleton_iff, (isClopen_discrete _).eq_univ <| singleton_nonempty y] at hxy

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : DiscreteTopology X
x y : X
hxy : x ∉ univ
⊢ False
Module: Mathlib.FieldTheory.Differential.Liouville

Goal state before:
pp: case refine_2
F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Differential F
inst✝⁶ : Differential K
inst✝⁵ : Algebra F K
inst✝⁴ : DifferentialAlgebra F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
this : CharZero K
ffb : fixedField ⊤ = ⊥
⊢ (algebraMap F K) a =
    ∑ x, ↑(c x) / ↑(Fintype.card Gal(K/F)) * logDeriv (∏ x_1, x_1 (u x)) + (↑(Fintype.card Gal(K/F)))⁻¹ * (∑ x, x v)′

pp: case refine_2.h
F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Differential F
inst✝⁶ : Differential K
inst✝⁵ : Algebra F K
inst✝⁴ : DifferentialAlgebra F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
this : CharZero K
ffb : fixedField ⊤ = ⊥
⊢ (↑(Fintype.card Gal(K/F)))′ = 0

Tactic:
inv_mul_eq_div

Goal state after:
case refine_2
F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Differential F
inst✝⁶ : Differential K
inst✝⁵ : Algebra F K
inst✝⁴ : DifferentialAlgebra F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
this : CharZero K
ffb : fixedField ⊤ = ⊥
⊢ (algebraMap F K) a =
    ∑ x, ↑(c x) / ↑(Fintype.card Gal(K/F)) * logDeriv (∏ x_1, x_1 (u x)) + (∑ x, x v)′ / ↑(Fintype.card Gal(K/F))

case refine_2.h
F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Differential F
inst✝⁶ : Differential K
inst✝⁵ : Algebra F K
inst✝⁴ : DifferentialAlgebra F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
this : CharZero K
ffb : fixedField ⊤ = ⊥
⊢ (↑(Fintype.card Gal(K/F)))′ = 0
Module: Mathlib.FieldTheory.CardinalEmb

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

Tactic:
exact (Module.rank_lt_aleph0 _ _).trans_eq eq

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.ExtendRight

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Algebra K L
F : IntermediateField K L
M : Type u_3
inst✝⁸ : Field M
inst✝⁷ : Algebra K M
inst✝⁶ : Algebra L M
inst✝⁵ : IsScalarTower K L M
R : Type u_4
S : Type u_5
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra S ↥F
inst✝¹ : Algebra S M
inst✝ : IsScalarTower S (↥F) M
s : S
x : ↥(F.extendRight M)
⊢ ↑(s • x) = ↑(((algebraMap S M).codRestrict (F.extendRight M).toSubalgebra ⋯) s * x)

Tactic:
by
    convert_to! s • (x : M) = _
    rw [MulMemClass.coe_mul, RingHom.codRestrict_apply, ← Algebra.smul_def]

Goal state after:
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp : ¬1 < p
h : x = 0
⊢ x ^ p ^ 0 = 0

Tactic:
pow_zero,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp : ¬1 < p
h : x = 0
⊢ x ^ 1 = 0
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp✝ : ¬1 < p
x✝ : ∃ n, x ^ p ^ n = 0
n : ℕ
h : x ^ p ^ 0 = 0
hp : p = 0
hn : n = 0
⊢ x = 0

Tactic:
pow_zero,

Goal state after:
case pos
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp✝ : ¬1 < p
x✝ : ∃ n, x ^ p ^ n = 0
n : ℕ
h : x ^ 1 = 0
hp : p = 0
hn : n = 0
⊢ x = 0
Module: Mathlib.FieldTheory.Galois.Profinite

Goal state before:
pp: k✝ : Type u_1
K✝ : Type u_2
inst✝⁶ : Field k✝
inst✝⁵ : Field K✝
inst✝⁴ : Algebra k✝ K✝
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
g : ↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
x : K
L : FiniteGaloisIntermediateField k K := adjoin k {x, toAlgEquivAux g⁻¹ x}
⊢ toAlgEquivAux g (toAlgEquivAux g⁻¹ x) = x

Tactic:
have hx : x ∈ L.1 := subset_adjoin _ _ (Set.mem_insert x {toAlgEquivAux g⁻¹ x})

Goal state after:
k✝ : Type u_1
K✝ : Type u_2
inst✝⁶ : Field k✝
inst✝⁵ : Field K✝
inst✝⁴ : Algebra k✝ K✝
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
g : ↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
x : K
L : FiniteGaloisIntermediateField k K := adjoin k {x, toAlgEquivAux g⁻¹ x}
hx : x ∈ L.toIntermediateField
⊢ toAlgEquivAux g (toAlgEquivAux g⁻¹ x) = x
Module: Mathlib.FieldTheory.PerfectClosure

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

Tactic:
pow_zero,

Goal state after:
case zero
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℕ × K
⊢ 1 = mk K p (x.1, x.2 ^ 0)
Module: Mathlib.FieldTheory.PerfectClosure

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

Tactic:
pow_zero,

Goal state after:
case zero
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℕ × K
⊢ 1 = mk K p (x.1, 1)
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing K
inst✝⁷ : CommRing L
inst✝⁶ : CommRing M
inst✝⁵ : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
f : L →+* M
g : L →+* N
p : ℕ
inst✝⁴ : ExpChar M p
inst✝³ : ExpChar K p
inst✝² : PerfectRing M p
inst✝¹ : IsPRadical i p
inst✝ : ExpChar L p
⊢ i 0 = 0 ^ p ^ 0

Tactic:
pow_zero,

Goal state after:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing K
inst✝⁷ : CommRing L
inst✝⁶ : CommRing M
inst✝⁵ : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
f : L →+* M
g : L →+* N
p : ℕ
inst✝⁴ : ExpChar M p
inst✝³ : ExpChar K p
inst✝² : PerfectRing M p
inst✝¹ : IsPRadical i p
inst✝ : ExpChar L p
⊢ i 0 = 0 ^ 1
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic

Goal state before:
pp: A B C : ProfiniteGrp.{u}
f : A ⟶ B
g : B ⟶ C
a : ↑A.toProfinite.toTop
⊢ (Hom.hom (f ≫ g)) a = (Hom.hom g) ((Hom.hom f) a)

Tactic:
by
  simp only [hom_comp, ContinuousMonoidHom.comp_toFun]

Goal state after:
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ ProfiniteGrp.{max v u}
cone : Limits.Cone F
m : cone.pt ⟶ (limitCone F).pt
h : ∀ (j : J), m ≫ (limitCone F).π.app j = cone.π.app j
⊢ (forget₂ ProfiniteGrp.{max u v} Profinite).map m =
    (forget₂ ProfiniteGrp.{max u v} Profinite).map
      (ofHom
        (let __src :=
          TopCat.Hom.hom
            ((Profinite.limitConeIsLimit (F ⋙ forget₂ ProfiniteGrp.{max u v} Profinite)).lift
                ((forget₂ ProfiniteGrp.{max u v} Profinite).mapCone cone)).hom;
        { toFun := __src.toFun, map_one' := ⋯, map_mul' := ⋯, continuous_toFun := ⋯ }))

Tactic:
simpa using! (Profinite.limitConeIsLimit (F ⋙ (forget₂ ProfiniteGrp Profinite))).uniq
      ((forget₂ ProfiniteGrp Profinite).mapCone cone) ((forget₂ ProfiniteGrp Profinite).map m)
      (fun j ↦ congrArg (forget₂ ProfiniteGrp Profinite).map (h j))

Goal state after: