mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
n : ℕ
⊢ ∀ (i : Finset X), IsDynNetIn T ∅ U n ↑i → ↑i.card = ⊥

Tactic:
intro s s_net

Goal state after:
X : Type u_1
T : X → X
U : SetRel X X
n : ℕ
s : Finset X
s_net : IsDynNetIn T ∅ U n ↑s
⊢ ↑s.card = ⊥
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: 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
⊢ ϕ.IsExpansionOn M

Tactic:
let := ϕ.defaultExpansion M
  refine ⟨fun {n} f xs => ?_, fun {n} r xs => ?_⟩
  · have hf : ϕ.onFunction f ∈ Set.range fun f : L.Functions n => ϕ.onFunction f := ⟨f, rfl⟩
    refine (dif_pos hf).trans ?_
    rw [h.onFunction hf.choose_spec]
  · 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.Basic

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f f' : M ↪[L] N
h : (fun x ↦ x.toHom) f = (fun x ↦ x.toHom) f'
x✝ : M
⊢ f x✝ = f' x✝

Tactic:
exact congr_fun (congr_arg (↑) h) _

Goal state after:
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: M : Type w
α : Type u'
β : Type v'
f : α → β
fα : α → M
fβ : β → M
h : fβ ∘ f = fα
⊢ (LHom.constantsOnMap f).IsExpansionOn M

Tactic:
by
  let := constantsOn.structure fα
  let := constantsOn.structure fβ
  exact
    ⟨fun {n} => Nat.casesOn n (fun F _x => (congr_fun h F :)) fun n F => isEmptyElim F, fun R =>
      isEmptyElim R⟩

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) (p.comp (X ^ n)) = 0

Tactic:
by rw [aeval_comp, aeval_X_pow, minpoly.aeval]

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Ring.FreeCommRing

Goal state before:
pp: α : Type u_1
p : FreeCommRing α
a : α
⊢ Term.realize FreeCommRing.of (var a) = FreeCommRing.of a

Tactic:
by simp [Term.realize]

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

Goal state before:
pp: case leftDistrib
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
⊢ toProp K leftDistrib

Tactic:
exact mul_add

Goal state after:
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: case imp
α : 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✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula β n✝
ih :
  ∀ (v : Fin n✝ → (a : α) → M a),
    (f₁✝.Realize (fun i ↦ Quotient.mk' (x i)) fun i ↦ Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, f₁✝.Realize (fun i ↦ x i a) fun i ↦ v i a
ih' :
  ∀ (v : Fin n✝ → (a : α) → M a),
    (f₂✝.Realize (fun i ↦ Quotient.mk' (x i)) fun i ↦ Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, f₂✝.Realize (fun i ↦ x i a) fun i ↦ v i a
v : Fin n✝ → (a : α) → M a
⊢ ((f₁✝ ⟹ f₂✝).Realize (fun i ↦ Quotient.mk' (x i)) fun i ↦ Quotient.mk' (v i)) ↔
    ∀ᶠ (a : α) in ↑u, (f₁✝ ⟹ f₂✝).Realize (fun i ↦ x i a) fun i ↦ v i a

Tactic:
| imp _ _ ih ih' =>

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case refine_1
L : Language
α : Type u'
⊢ ℵ₀ ≤ max ℵ₀ #(α ⊕ (i : ℕ) × L.Functions i) ∧ ∀ (i : ℕ), #(L.Term (α ⊕ Fin i)) ≤ max ℵ₀ #(α ⊕ (i : ℕ) × L.Functions i)

Tactic:
refine ⟨le_max_left _ _, fun i => card_le.trans ?_⟩
      refine max_le (le_max_left _ _) ?_
      grw [← add_eq_max le_rfl, mk_sum, mk_sum, mk_sum, add_comm (Cardinal.lift #α), lift_add,
        add_assoc, lift_lift, lift_lift, mk_fin, lift_natCast, natCast_lt_aleph0]

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case refine_2.refine_1
L : Language
α : Type u'
i j : ℕ
ij : (fun i ↦ ⟨i + 1, var (Sum.inr (last i))⟩) i = (fun i ↦ ⟨i + 1, var (Sum.inr (last i))⟩) j
⊢ i = j

pp: case refine_2.refine_2
L : Language
α : Type u'
⊢ #(α ⊕ (i : ℕ) × L.Functions i) ≤ #((n : ℕ) × L.Term (α ⊕ Fin n))

Tactic:
· cases ij
      rfl

Goal state after:
case refine_2.refine_2
L : Language
α : Type u'
⊢ #(α ⊕ (i : ℕ) × L.Functions i) ≤ #((n : ℕ) × L.Term (α ⊕ Fin n))
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: 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
this : Small.{u, w} ↑∅
⊢ Small.{u, w} ↥((closure L).toFun ∅)

Tactic:
exact Substructure.small_closure

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: L : Language
α : Type u'
⊢ max (lift.{max (max u u') v, max (max u u') v} #((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) ℵ₀ ≤
    max ℵ₀ (lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card))

Tactic:
max_le_iff

Goal state after:
L : Language
α : Type u'
⊢ lift.{max (max u u') v, max (max u u') v} #((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ) ≤
      max ℵ₀ (lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card)) ∧
    ℵ₀ ≤ max ℵ₀ (lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card))
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: 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 := LHom.sumInr.onFunction φ
⊢ ∀ (i : Fin n), (Subtype.val ∘ x) i ∈ ↑S

Tactic:
by
      exact fun i => (x i).2

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝¹ : L.Structure M
α : Type u₁
β : Type u_1
inst✝ : Finite β
S : Set (α ⊕ β → M)
hS : A.Definable L S
⊢ A.Definable L {v | ∃ u, Sum.elim v u ∈ S}

Tactic:
by
  obtain ⟨φ, hφ⟩ := hS
  exists φ.iExs β
  ext v
  simp [hφ]

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
M : Type w'
inst✝ : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h2 : lift.{max w u v, w'} #M ≤ lift.{max w' u v, w} κ
N0 : (L.elementaryDiagram M).ModelType
hN0 : lift.{max (max u w') v w, w} κ ≤ #↑N0
⊢ max (lift.{max (max u v) w, w'} #M) (lift.{max w' w, max u v} L.card) ≤ lift.{max (max w' u) v, w} κ

Tactic:
max_le_iff

Goal state after:
L : Language
M : Type w'
inst✝ : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h2 : lift.{max w u v, w'} #M ≤ lift.{max w' u v, w} κ
N0 : (L.elementaryDiagram M).ModelType
hN0 : lift.{max (max u w') v w, w} κ ≤ #↑N0
⊢ lift.{max (max u v) w, w'} #M ≤ lift.{max (max w' u) v, w} κ ∧
    lift.{max w' w, max u v} L.card ≤ lift.{max (max w' u) v, w} κ
Module: Mathlib.RingTheory.Nullstellensatz

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
σ : Type u_3
x : σ → K
⊢ (vanishingIdeal k {x}).IsPrime

Tactic:
convert! RingHom.ker_isPrime (aeval (R := k) x)
  ext; simp

Goal state after:
Module: Mathlib.GroupTheory.OreLocalization.Cardinality

Goal state before:
pp: R : Type u
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
⊢ max (lift.{u, u} #↥S) (lift.{u, u} #R) = #R

Tactic:
simp_rw [lift_id, max_eq_right_iff, mk_subtype_le]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: case inr.ha
a : Cardinal.{u}
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : a * t = 1
⊢ 1 ≤ a

Tactic:
exact Cardinal.one_le_iff_ne_zero.mpr ha

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: n m : ℕ
⊢ ↑n ∣ ↑m ↔ n ∣ m

Tactic:
refine ⟨?_, fun ⟨h, ht⟩ => ⟨h, mod_cast ht⟩⟩

Goal state after:
n m : ℕ
⊢ ↑n ∣ ↑m → n ∣ m
Module: Mathlib.FieldTheory.Finite.Extension

Goal state before:
pp: k : Type u_1
inst✝⁶ : Field k
inst✝⁵ : Finite k
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP k p
n : ℕ
inst✝² : NeZero n
l : Type u_2
inst✝¹ : Field l
inst✝ : Algebra k l
h : Module.finrank k l = n
this✝² : Module.Finite k l
this✝¹ : Finite l
this✝ : Fintype l
this : IsSplittingField k l (X ^ Nat.card k ^ n - X)
⊢ Nonempty (l ≃ₐ[k] Extension k p n)

Tactic:
refine ⟨(IsSplittingField.algEquiv _ (X ^ (Nat.card k ^ n) - X)).trans ?_⟩

Goal state after:
k : Type u_1
inst✝⁶ : Field k
inst✝⁵ : Finite k
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP k p
n : ℕ
inst✝² : NeZero n
l : Type u_2
inst✝¹ : Field l
inst✝ : Algebra k l
h : Module.finrank k l = n
this✝² : Module.Finite k l
this✝¹ : Finite l
this✝ : Fintype l
this : IsSplittingField k l (X ^ Nat.card k ^ n - X)
⊢ (X ^ Nat.card k ^ n - X).SplittingField ≃ₐ[k] Extension k p 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 : σ
⊢ (Fintype.card K - 1) * Multiset.count n {n} = Fintype.card K - 1

Tactic:
· rw [Multiset.count_singleton_self, mul_one]

Goal state after:
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: 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
⊢ IsLeast {k | b k ∉ adjoin F (⇑b ∘ φ '' Iio i)} (φ i)

Tactic:
rw [image_eq_range, leastExt, wellFounded_lt.fix_eq]

Goal state after:
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
⊢ IsLeast
    {k |
      b k ∉
        adjoin F
          (range fun x ↦
            (⇑b ∘
                ⋯.fix fun i ih ↦
                  let s := range fun j ↦ b (ih ↑j ⋯);
                  ⋯.min {k | b k ∉ adjoin F s} ⋯)
              ↑x)}
    (let s :=
      range fun j ↦
        b
          ((fun y x ↦
              ⋯.fix
                (fun i ih ↦
                  let s := range fun j ↦ b (ih ↑j ⋯);
                  ⋯.min {k | b k ∉ adjoin F s} ⋯)
                y)
            ↑j ⋯);
    ⋯.min {k | b k ∉ adjoin F s} ⋯)
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 : IntermediateField k K
inst✝ : Normal k ↥L
N : Set Gal(↥L/k)
hN : N ∈ nhds 1
⊢ ⇑(AlgEquiv.restrictNormalHom ↥L) ⁻¹' N ∈ nhds 1

Tactic:
krullTopology_mem_nhds_one_iff

Goal state after:
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : Normal k ↥L
N : Set Gal(↥L/k)
hN : ∃ E, FiniteDimensional k ↥E ∧ ↑E.fixingSubgroup ⊆ N
⊢ ⇑(AlgEquiv.restrictNormalHom ↥L) ⁻¹' N ∈ nhds 1
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
n : ℕ
x : K
m : ℕ
ih : mk K p (n, x) = mk K p (m + n, (⇑(frobenius K p))^[m] x)
⊢ mk K p (n, x) = mk K p (m + 1 + n, (⇑(frobenius K p))^[m + 1] x)

Tactic:
rw [ih, Nat.succ_add, iterate_succ']
    apply Quot.sound
    apply R.intro

Goal state after:
Module: Mathlib.FieldTheory.IsRealClosed.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
n : ℕ
hn : Odd n
⊢ Odd (X ^ n - C x).natDegree

Tactic:
by simp [hn]

Goal state after:
Module: Mathlib.FieldTheory.IsRealClosed.Basic

Goal state before:
pp: case h.inl
R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
n : ℕ
ih : ∀ m < n, ∀ {x : R}, IsSquare x → m ≠ 0 → ∃ r, x = r ^ m
x : R
hn : n ≠ 0
m : ℕ
hm : n = m + m
s : R
hs : x = s * s
⊢ ∃ r, x = r ^ n

Tactic:
rcases isSquare_or_isSquare_neg s with (h | h) <;>
        rcases ih m (by lia) h (by lia) with ⟨r, hr⟩

Goal state after:
case h.inl.inl
R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
n : ℕ
ih : ∀ m < n, ∀ {x : R}, IsSquare x → m ≠ 0 → ∃ r, x = r ^ m
x : R
hn : n ≠ 0
m : ℕ
hm : n = m + m
s : R
hs : x = s * s
h : IsSquare s
r : R
hr : s = r ^ m
⊢ ∃ r, x = r ^ n

case h.inl.inr
R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
n : ℕ
ih : ∀ m < n, ∀ {x : R}, IsSquare x → m ≠ 0 → ∃ r, x = r ^ m
x : R
hn : n ≠ 0
m : ℕ
hm : n = m + m
s : R
hs : x = s * s
h : IsSquare (-s)
r : R
hr : -s = r ^ m
⊢ ∃ r, x = r ^ n
Module: Mathlib.FieldTheory.IsRealClosed.Basic

Goal state before:
pp: case h
R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
n : ℕ
ih : ∀ m < n, ∀ {x : R}, IsSquare x → m ≠ 0 → ∃ r, x = r ^ m
x : R
hx : IsSquare x
hn : n ≠ 0
⊢ ∃ r, x = r ^ n

Tactic:
| h n ih =>

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: case mk
K : Type u
inst✝⁵ : CommRing K
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP K p
L : Type v
inst✝² : CommSemiring L
inst✝¹ : CharP L p
inst✝ : PerfectRing L p
f : PerfectClosure K p →+* L
x✝ : PerfectClosure K p
n : ℕ
x : K
⊢ ((fun f ↦
          { toFun := fun e ↦ e.liftOn (fun x ↦ (⇑(frobeniusEquiv L p).symm)^[x.1] (f x.2)) ⋯, map_one' := ⋯,
            map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ })
        ((fun f ↦ f.comp (of K p)) f))
      (Quot.mk (R K p) (n, x)) =
    f (Quot.mk (R K p) (n, x))

Tactic:
simp only [quot_mk_eq_mk, RingHom.comp_apply, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,
      liftOn_mk]

Goal state after:
case mk
K : Type u
inst✝⁵ : CommRing K
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP K p
L : Type v
inst✝² : CommSemiring L
inst✝¹ : CharP L p
inst✝ : PerfectRing L p
f : PerfectClosure K p →+* L
x✝ : PerfectClosure K p
n : ℕ
x : K
⊢ (⇑(frobeniusEquiv L p).symm)^[n] (f ((of K p) x)) = f (mk K p (n, x))
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι},
      ⋃ i ∈ s, g i • ↑(H i) = Set.univ →
        ∀ j ∈ s,
          ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ →
            m = (Finset.image H s).card → ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
j : ι
hj : j ∈ s
hcovers' : ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ
hn : n = (Finset.image H s).card
x : G
hx : ∀ i ∈ s, H i = H j → ↑(g i) ≠ ↑x
y z : G
hz : z ∈ y • ↑(H j)
⊢ ∃ i ∈ s, x * (y⁻¹ * z) ∈ g i • ↑(H i)

Tactic:
simpa using Set.eq_univ_iff_forall.mp hcovers (x * (y⁻¹ * z))

Goal state after:
Module: Mathlib.FieldTheory.JacobsonNoether

Goal state before:
pp: D : Type u_1
inst✝² : DivisionRing D
inst✝¹ : Algebra.IsAlgebraic (↥k) D
p : ℕ
inst✝ : ExpChar D p
a : D
ha : a ∉ k
hinsep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
n : ℕ
hn : a ^ p ^ n ∈ k
nzero : n ≠ 0
⊢ ∃ n, 1 ≤ n ∧ a ^ p ^ n ∈ k

Tactic:
exact ⟨n, ⟨Nat.one_le_iff_ne_zero.mpr nzero, hn⟩⟩

Goal state after:
Module: Mathlib.FieldTheory.JacobsonNoether

Goal state before:
pp: D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
ha : a ∉ k
hinsep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
m : ℕ
hm : 1 ≤ m ∧ a ^ p ^ m ∈ k
n : ℕ
hn : p ^ m ≤ n
⊢ (⇑((ad (↥k) D) a))^[n] = 0

Tactic:
have inter : (ad k D a)^[p ^ m] = 0 := by
    ext x
    rw [ad_eq_lmul_left_sub_lmul_right, ← Module.End.pow_apply, Pi.sub_apply,
      sub_pow_expChar_pow_of_commute p m (commute_mulLeft_right a a), LinearMap.sub_apply,
      pow_mulLeft, mulLeft_apply, pow_mulRight, mulRight_apply, Pi.zero_apply,
      Subring.mem_center_iff.1 hm.2 x]
    exact sub_eq_zero_of_eq rfl

Goal state after:
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
ha : a ∉ k
hinsep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
m : ℕ
hm : 1 ≤ m ∧ a ^ p ^ m ∈ k
n : ℕ
hn : p ^ m ≤ n
inter : (⇑((ad (↥k) D) a))^[p ^ m] = 0
⊢ (⇑((ad (↥k) D) a))^[n] = 0
Module: Mathlib.FieldTheory.MvRatFunc.Rank

Goal state before:
pp: case refine_2
σ : Type u
F : Type v
inst✝¹ : Field F
inst✝ : Nonempty σ
R : Type (max v u) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
hinj : Function.Injective ⇑(algebraMap R K)
h1 : lift.{v, u} #(σ →₀ ℕ) ≤ Module.rank F K
⊢ max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))

Tactic:
mk_finsupp_nat,

Goal state after:
case refine_2
σ : Type u
F : Type v
inst✝¹ : Field F
inst✝ : Nonempty σ
R : Type (max v u) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
hinj : Function.Injective ⇑(algebraMap R K)
h1 : lift.{v, u} (max #σ ℵ₀) ≤ Module.rank F K
⊢ max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))
Module: Mathlib.FieldTheory.MvRatFunc.Rank

Goal state before:
pp: case refine_2
σ : Type u
F : Type v
inst✝¹ : Field F
inst✝ : Nonempty σ
R : Type (max v u) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
hinj : Function.Injective ⇑(algebraMap R K)
h1 : max (lift.{v, u} #σ) ℵ₀ ≤ Module.rank F K
⊢ max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))

Tactic:
max_le_iff

Goal state after:
case refine_2
σ : Type u
F : Type v
inst✝¹ : Field F
inst✝ : Nonempty σ
R : Type (max v u) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
hinj : Function.Injective ⇑(algebraMap R K)
h1 : lift.{v, u} #σ ≤ Module.rank F K ∧ ℵ₀ ≤ Module.rank F K
⊢ max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))
Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
ι : Type w
x : ι → E
inst✝ : Nonempty ι
hx : IsTranscendenceBasis F x
K : IntermediateField F E := IntermediateField.adjoin F (range x)
this : Algebra.IsAlgebraic (↥K) E
⊢ lift.{max u w, v} (Module.rank (↥K) E) ≠ 0

Tactic:
simp [rank_pos.ne']

Goal state after:
Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
ι : Type w
x : ι → E
inst✝ : Nonempty ι
hx : IsTranscendenceBasis F x
⊢ lift.{max u w, v} (Module.rank F E) = max (max (lift.{max v w, u} #F) (lift.{max u v, w} #ι)) ℵ₀

Tactic:
by
  let K := IntermediateField.adjoin F (Set.range x)
  have : Algebra.IsAlgebraic K E := hx.isAlgebraic_field
  rw [← rank_mul_rank F K E, lift_mul, ← hx.1.aevalEquivField.toLinearEquiv.lift_rank_eq,
    MvRatFunc.rank_eq_max_lift, lift_max, lift_max, lift_lift, lift_lift, lift_aleph0]
  refine mul_eq_left le_sup_right ((lift_le.2 ((rank_le_card K E).trans
    (Algebra.IsAlgebraic.cardinalMk_le_max K E))).trans_eq ?_) (by simp [rank_pos.ne'])
  simp [K, ← lift_mk_eq'.2 ⟨hx.1.aevalEquivField.toEquiv⟩]

Goal state after:
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
inst✝ : DecidablePred FiniteIndex
D : Subgroup G := ⨅ k ∈ {i ∈ s | (H i).FiniteIndex}, H k
hD : D.FiniteIndex
hD_le : ∀ {i : ι}, i ∈ s → (H i).FiniteIndex → D ≤ H i
t : (i : ι) → i ∈ s → (H i).FiniteIndex → Finset ↥(H i)
ht :
  ∀ (i : ι) (hi : i ∈ s) (hfi : (H i).FiniteIndex),
    IsComplement ↑(t i hi hfi) ↑(D.subgroupOf (H i)) ∧ ⋃ g ∈ t i hi hfi, ↑g • ↑D = ↑(H i)
κ : Type (max u_2 u_1) := (i : ↥s) × ↥(if h : (H ↑i).FiniteIndex then t ↑i ⋯ h else {1})
f : κ → G := fun k ↦ g ↑k.fst * ↑↑k.snd
K : κ → Subgroup G := fun k ↦ if (H ↑k.fst).FiniteIndex then D else H ↑k.fst
k : κ
hkfi : (H ↑k.fst).FiniteIndex
hk : K k = D
hcovers' : ⋃ i ∈ {x | K x = D}, f i • ↑D = Set.univ
hHD : ∀ (i : ι), ¬(H i).FiniteIndex → H i ≠ D
hdensity : ∑ i ∈ s, (↑(H i).index)⁻¹ = ↑{x | K x = D}.card * (↑D.index)⁻¹
h : {x | K x = D}.card = D.index
i✝ : ι
hi✝ : i✝ ∈ s ∧ (H i✝).FiniteIndex
j : ι
hj : j ∈ s ∧ (H j).FiniteIndex
hij : i✝ ≠ j
c : Set G
hi'✝ : c ⊆ (fun i ↦ g i • ↑(H i)) i✝
hj' : c ⊆ (fun i ↦ g i • ↑(H i)) j
x : G
hx : x ∈ c
hdisjoint : (↑{x | K x = D}).PairwiseDisjoint fun x ↦ f x • ↑D
i : ι
hi : i ∈ s ∧ (H i).FiniteIndex
hi' : c ⊆ g i • ⋃ g ∈ t i ⋯ ⋯, ↑g • ↑D
⊢ ∃ r ∈ t i ⋯ ⋯, x ∈ (g i * ↑r) • ↑D

Tactic:
simpa [Set.mem_smul_set_iff_inv_smul_mem, smul_eq_mul, mul_assoc] using! hi' hx

Goal state after:
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝³ : DivisionRing k
inst✝² : Infinite k
inst✝¹ : AddCommGroup E
inst✝ : Module k E
s : Finset (Subspace k E)
hs : ⊤ ∉ s
⊢ ⋃ p ∈ s, ↑p ≠ Set.univ

Tactic:
intro hcovers
  have ⟨p, hp, hfi⟩ := Submodule.exists_finiteIndex_of_cover hcovers
  have : Finite (E ⧸ p) := AddSubgroup.finite_quotient_of_finiteIndex
  have : Nontrivial (E ⧸ p) := Submodule.Quotient.nontrivial_iff.mpr (ne_of_mem_of_not_mem hp hs)
  have : Infinite (E ⧸ p) := Module.Free.infinite k (E ⧸ p)
  exact not_finite (E ⧸ p)

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsSeparable K L
c : ConjRootClass K L
inst✝ : Fintype ↑c.carrier
⊢ c.carrier.toFinset = { val := c.minpoly.aroots L, nodup := ⋯ }

Tactic:
by
  simp only [aroots_minpoly_eq_carrier_val]

Goal state after:
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
A : Type v
inst✝⁵ : CommRing A
B : Type w
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Flat R A
inst✝ : Flat R B
H : IsField (A ⊗[R] B)
h : Algebra.Transcendental R A ∧ Algebra.Transcendental R B
⊢ False

Tactic:
obtain ⟨_, _⟩ := h

Goal state after:
R : Type u
inst✝⁶ : CommRing R
A : Type v
inst✝⁵ : CommRing A
B : Type w
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Flat R A
inst✝ : Flat R B
H : IsField (A ⊗[R] B)
left✝ : Algebra.Transcendental R A
right✝ : Algebra.Transcendental R B
⊢ False
Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type w
inst✝³ : Field K
inst✝² : Algebra F K
p : ℕ
inst✝¹ : ExpChar E p
inst✝ : PerfectRing E p
x : ↥(perfectClosure F E)
this : ExpChar F p
x' : E
hx : x' ^ p = ↑x
n : ℕ
y : F
hy : (algebraMap F E) y = x' ^ (p * p ^ n)
⊢ ∃ a, (frobenius (↥(perfectClosure F E)) p) a = x

Tactic:
← pow_succ'

Goal state after:
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type w
inst✝³ : Field K
inst✝² : Algebra F K
p : ℕ
inst✝¹ : ExpChar E p
inst✝ : PerfectRing E p
x : ↥(perfectClosure F E)
this : ExpChar F p
x' : E
hx : x' ^ p = ↑x
n : ℕ
y : F
hy : (algebraMap F E) y = x' ^ p ^ (n + 1)
⊢ ∃ a, (frobenius (↥(perfectClosure F E)) p) a = x
Module: Mathlib.FieldTheory.PurelyInseparable.Tower

Goal state before:
pp: F : Type u
E : Type v
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
K : Type w
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra E K
inst✝² : IsScalarTower F E K
S : IntermediateField F K
inst✝¹ : Algebra.IsAlgebraic F ↥S
inst✝ : IsPurelyInseparable F E
⊢ Algebra.IsAlgebraic F ↥(adjoin F ↑S)

Tactic:
rwa [adjoin_self]

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Tower

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
f : F[X]
hsep : f.Separable
hirr : Irreducible f
inst✝ : IsPurelyInseparable F E
K : Type v := AlgebraicClosure E
x : K
hx : (aeval x) f = 0
this : IsUnit (C f.leadingCoeff⁻¹)
⊢ f * C f.leadingCoeff⁻¹ = minpoly F x

Tactic:
minpoly.eq_of_irreducible hirr hx

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
f : F[X]
hsep : f.Separable
hirr : Irreducible f
inst✝ : IsPurelyInseparable F E
K : Type v := AlgebraicClosure E
x : K
hx : (aeval x) f = 0
this : IsUnit (C f.leadingCoeff⁻¹)
⊢ minpoly F x = minpoly F x