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

Goal state before:
pp: case inr
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : SetRel Y Y
n : ℕ
h' : coverMincard S F (map φ φ ⁻¹' V) n < ⊤
s : Finset X
s_cover : IsDynCoverOf S F (map φ φ ⁻¹' V) n ↑s
s_card : ↑s.card = coverMincard S F (map φ φ ⁻¹' V) n
this : IsDynCoverOf T (φ '' F) V n (φ '' ↑s)
⊢ coverMincard T (φ '' F) V n ≤ ↑s.card

Tactic:
rw [← s.coe_image] at this

Goal state after:
case inr
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
V : SetRel Y Y
n : ℕ
h' : coverMincard S F (map φ φ ⁻¹' V) n < ⊤
s : Finset X
s_cover : IsDynCoverOf S F (map φ φ ⁻¹' V) n ↑s
s_card : ↑s.card = coverMincard S F (map φ φ ⁻¹' V) n
this : IsDynCoverOf T (φ '' F) V n ↑(Finset.image φ s)
⊢ coverMincard T (φ '' F) V n ≤ ↑s.card
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
⊢ μ.rnDeriv ν =ᵐ[ν] 1 ↔ μ = ν

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ h ▸ ν.rnDeriv_self⟩
  rw [← withDensity_rnDeriv_eq _ _ hμν, withDensity_congr_ae h, withDensity_one]

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

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

Tactic:
have h_add := Measure.rnDeriv_add' ((μ.singularPart ν).map f)
    ((ν.withDensity (μ.rnDeriv ν)).map f) (ν.map f)

Goal state after:
α : 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 :
  (map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) =ᵐ[map f ν]
    (map f (μ.singularPart ν)).rnDeriv (map f ν) + (map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν)
⊢ (fun x ↦ (map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x)) =ᵐ[ν]
    (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite μ
f : α → E
hμν : μ ≪ ν
s : Set α
hs : MeasurableSet s
⊢ ∫ (x : α) in s, (μ.rnDeriv ν x).toReal • f x ∂ν = ∫ (x : α) in s, f x ∂μ

Tactic:
← setIntegral_withDensity_eq_setIntegral_toReal_smul,

Goal state after:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite μ
f : α → E
hμν : μ ≪ ν
s : Set α
hs : MeasurableSet s
⊢ (∫ (x : α) in s, f x ∂ν.withDensity fun x ↦ μ.rnDeriv ν x) = ∫ (x : α) in s, f x ∂μ

case hf
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite μ
f : α → E
hμν : μ ≪ ν
s : Set α
hs : MeasurableSet s
⊢ Measurable (μ.rnDeriv ν)

case hf_top
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite μ
f : α → E
hμν : μ ≪ ν
s : Set α
hs : MeasurableSet s
⊢ ∀ᵐ (x : α) ∂ν.restrict s, μ.rnDeriv ν x < ∞

case hs
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite μ
f : α → E
hμν : μ ≪ ν
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet s
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: case refine_2.inl
L : Language
L' : Language
M : Type w
inst✝² : L.Structure M
α : Type u_1
inst✝¹ : (constantsOn α).Structure M
A B : Set M
h : A ⊆ B
N : Type w'
inst✝ : L.Structure N
f : M ↪[L] N
n : ℕ
x : Fin n → M
R : L.Relations n
⊢ RelMap (Sum.inl R) (f.toFun ∘ x) ↔ RelMap (Sum.inl R) x

Tactic:
exact f.map_rel' R x

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

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : CompatibleRing R
p : FreeCommRing α
v : α → R
| (FreeCommRing.lift v) p

Tactic:
← Classical.choose_spec (exists_term_realize_eq_freeCommRing p)

Goal state after:
α : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : CompatibleRing R
p : FreeCommRing α
v : α → R
| (FreeCommRing.lift v) (Term.realize FreeCommRing.of (Classical.choose ⋯))
Module: Mathlib.ModelTheory.Syntax

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

Tactic:
ext t

Goal state after:
L : Language
α : Type u'
t : L.Term α
⊢ (LHom.id L).onTerm t = id t
Module: Mathlib.ModelTheory.Syntax

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

Tactic:
ext t

Goal state after:
L : Language
L' : Language
α : Type u'
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
t : L.Term α
⊢ (φ.comp ψ).onTerm t = (φ.onTerm ∘ ψ.onTerm) t
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⟯
p : F[X] := minpoly F x
q : F[X] := minpoly F y
hpq :
  (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F x)).Splits ∧
    (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F y)).Splits
⊢ ∀ s ∈ {x, y}, IsIntegral F s ∧ (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F s)).Splits

Tactic:
by
      rintro a (rfl | rfl)
      · exact ⟨isIntegral_of_mem_solvableByRad hx, hpq.1⟩
      · exact ⟨isIntegral_of_mem_solvableByRad hy, hpq.2⟩

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
R : L.Relations 2
t₁ t₂ : L.Term (α ⊕ Fin l)
⊢ (R.boundedFormula₂ t₁ t₂).Realize v xs ↔ RelMap R ![realize (Sum.elim v xs) t₁, realize (Sum.elim v xs) t₂]

Tactic:
by
  rw [Relations.boundedFormula₂, realize_rel, iff_eq_eq]
  refine congr rfl (funext (Fin.cases ?_ ?_))
  · simp only [Matrix.cons_val_zero]
  · simp only [Matrix.cons_val_succ, Matrix.cons_val_fin_one, forall_const]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
T T' : L.Theory
h : M ⊨ T
h' : M ⊨ T'
⊢ M ⊨ T ∪ T'

Tactic:
simp only [model_iff, Set.mem_union] at *

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
T T' : L.Theory
h : ∀ φ ∈ T, M ⊨ φ
h' : ∀ φ ∈ T', M ⊨ φ
⊢ ∀ (φ : L.Sentence), φ ∈ T ∨ φ ∈ T' → M ⊨ φ
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
s : Set (β → M)
h✝ : A.Definable L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  A.Definable L
    ((fun g ↦ g ∘ rangeSplitting f) ⁻¹'
      (fun g ↦ g ∘ Sum.inl) ''
        (fun g ↦ g ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          (fun g ↦ g ∘ ⇑(Equiv.Set.sumCompl (range f))) '' s)
h' : ∀ (a : α), A.Definable L {x | x a = x (rangeSplitting f (rangeFactorization f a))}
⊢ A.Definable L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}

Tactic:
refine (congr rfl (ext ?_)).mp (definable_biInter_finset h' Finset.univ)

Goal state after:
M : Type w
A : Set M
L : Language
inst✝² : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h✝ : A.Definable L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  A.Definable L
    ((fun g ↦ g ∘ rangeSplitting f) ⁻¹'
      (fun g ↦ g ∘ Sum.inl) ''
        (fun g ↦ g ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          (fun g ↦ g ∘ ⇑(Equiv.Set.sumCompl (range f))) '' s)
h' : ∀ (a : α), A.Definable L {x | x a = x (rangeSplitting f (rangeFactorization f a))}
⊢ ∀ (x : α → M),
    x ∈ ⋂ i ∈ Finset.univ, {x | x i = x (rangeSplitting f (rangeFactorization f i))} ↔
      x ∈ {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
h : T.IsFinitelySatisfiable
M : Finset ↑T → Type (max u v) := fun T0 ↦ ↑(Nonempty.some ⋯)
M' : Type (max u v) := (↑(Ultrafilter.of Filter.atTop)).Product M
φ : L.Sentence
hφ : φ ∈ T
s : Finset ↑T
h' : {⟨φ, hφ⟩} ⊆ s
⊢ ∃ (x : φ ∈ T), ⟨φ, ⋯⟩ ∈ s

Tactic:
exact ⟨hφ, h' (Finset.mem_singleton_self _)⟩

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: case some
M : Type u_1
L : Language
inst✝¹ : L.Structure M
α : Type u_2
β : Type u_3
A : Set M
f : (α → M) → M
inst✝ : Finite α
g : (β → M) → α → M
hg : DefinableMap L A g
hf : DefinableFun L A f
G : (Option β → M) → Option α → M :=
  fun w j ↦
    match j with
    | none => w none
    | some i => g (w ∘ some) i
j : α
⊢ DefinableFun L A fun x ↦ G x (some j)

Tactic:
simpa [tupleGraph] using!
        ((hg j).preimage_comp fun | none => none | some i => some (some i))

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
g : α → (β → M) → M
φ : L[[↑A]].Term α
ψ : α → L[[↑A]].Term β
hψ : ∀ (i : α), g i = fun v ↦ Term.realize v (ψ i)
⊢ A.TermDefinable L fun b ↦ (fun v ↦ Term.realize v φ) fun x ↦ g x b

Tactic:
use φ.subst ψ

Goal state after:
case h
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
β : Type u_1
g : α → (β → M) → M
φ : L[[↑A]].Term α
ψ : α → L[[↑A]].Term β
hψ : ∀ (i : α), g i = fun v ↦ Term.realize v (ψ i)
⊢ (fun b ↦ (fun v ↦ Term.realize v φ) fun x ↦ g x b) = fun v ↦ Term.realize v (φ.subst ψ)
Module: Mathlib.RingTheory.MvPolynomial.FreeCommRing

Goal state before:
pp: ι : Type u_1
κ : Type u_2
R : Type u_3
inst✝² : DecidableEq κ
inst✝¹ : CommRing R
inst✝ : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
f : (i : ι) × ↥(monoms i) ⊕ κ → R
i : ι
⊢ ∑ x ∈ (monoms i).attach, f (Sum.inl ⟨i, x⟩) * (lift f) ((↑x).prod fun j n ↦ of (Sum.inr j) ^ n) =
    ∑ a ∈ monoms i,
      if ∃ (h : a ∈ monoms i), ¬f (Sum.inl ⟨i, ⟨a, ⋯⟩⟩) = 0 then
        (if h : a ∈ monoms i then f (Sum.inl ⟨i, ⟨a, ⋯⟩⟩) else 0) * ∏ x ∈ a.support, f (Sum.inr x) ^ a x
      else 0

Tactic:
conv_rhs => rw [← Finset.sum_attach]

Goal state after:
ι : Type u_1
κ : Type u_2
R : Type u_3
inst✝² : DecidableEq κ
inst✝¹ : CommRing R
inst✝ : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
f : (i : ι) × ↥(monoms i) ⊕ κ → R
i : ι
⊢ ∑ x ∈ (monoms i).attach, f (Sum.inl ⟨i, x⟩) * (lift f) ((↑x).prod fun j n ↦ of (Sum.inr j) ^ n) =
    ∑ x ∈ (monoms i).attach,
      if ∃ (h : ↑x ∈ monoms i), ¬f (Sum.inl ⟨i, ⟨↑x, ⋯⟩⟩) = 0 then
        (if h : ↑x ∈ monoms i then f (Sum.inl ⟨i, ⟨↑x, ⋯⟩⟩) else 0) * ∏ x_1 ∈ (↑x).support, f (Sum.inr x_1) ^ ↑x x_1
      else 0
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h : ↑T0 ⊨ᵇ φ
⊢ (ψ : Language.ring.Sentence) → ψ ∈ Theory.ACF 0 → { s // ∀ q ∉ s, Theory.ACF ↑q ⊨ᵇ ψ }

Tactic:
intro ψ hψ

Goal state after:
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h : ↑T0 ⊨ᵇ φ
ψ : Language.ring.Sentence
hψ : ψ ∈ Theory.ACF 0
⊢ { s // ∀ q ∉ s, Theory.ACF ↑q ⊨ᵇ ψ }
Module: Mathlib.FieldTheory.Differential.Basic

Goal state before:
pp: R : Type u_1
inst✝⁶ : Field R
inst✝⁵ : Differential R
a b : R
F : Type u_2
inst✝⁴ : Field F
inst✝³ : Differential F
inst✝² : CharZero F
p : F[X]
inst✝¹ : Fact (Irreducible p)
inst✝ : Fact p.Monic
q : F[X]
⊢ (AdjoinRoot.mk p)
      ((mapCoeffs +
          (AdjoinRoot.modByMonicHom ⋯)
              (-(aeval (AdjoinRoot.root p)) (mapCoeffs p) / (aeval (AdjoinRoot.root p)) (derivative p)) •
            Derivation.restrictScalars ℤ derivative')
        p) =
    0

Tactic:
simp only [AdjoinRoot.aeval_eq, Derivation.coe_add, Derivation.coe_smul, Pi.add_apply,
        Pi.smul_apply, Derivation.restrictScalars_apply, derivative'_apply, smul_eq_mul, map_add,
        map_mul, AdjoinRoot.mk_leftInverse Fact.out _]

Goal state after:
R : Type u_1
inst✝⁶ : Field R
inst✝⁵ : Differential R
a b : R
F : Type u_2
inst✝⁴ : Field F
inst✝³ : Differential F
inst✝² : CharZero F
p : F[X]
inst✝¹ : Fact (Irreducible p)
inst✝ : Fact p.Monic
q : F[X]
⊢ (AdjoinRoot.mk p) (mapCoeffs p) +
      -(AdjoinRoot.mk p) (mapCoeffs p) / (AdjoinRoot.mk p) (derivative p) * (AdjoinRoot.mk p) (derivative p) =
    0
Module: Mathlib.FieldTheory.Finite.Extension

Goal state before:
pp: k : Type u_1
inst✝ : Field k
f : k[X]
hi : Irreducible f
n : ℕ
h : f ∣ X ^ Nat.card k ^ n - X
⊢ f.natDegree ∣ n

Tactic:
rcases eq_or_ne n 0 with rfl | hn
  · simp
  cases finite_or_infinite k; swap
  · rw [Nat.card_eq_zero_of_infinite, zero_pow hn, pow_zero, ← dvd_neg, neg_sub] at h
    rw [((Splits.X_sub_C 1).of_dvd (X_sub_C_ne_zero 1) h).natDegree_eq_one_of_irreducible hi]
    exact one_dvd n
  let ⟨p, hp⟩ := CharP.exists k
  have : Fact (Nat.Prime p) := ⟨CharP.char_is_prime k p⟩
  have : NeZero n := ⟨hn⟩
  rw [← finrank_extension k p n]
  apply Irreducible.natDegree_dvd_finrank hi
  refine Splits.of_dvd ?_ ?_ (map_dvd (algebraMap _ (Extension _ p n)) h)
  · apply IsSplittingField.splits
  · exact map_ne_zero (X_pow_card_pow_sub_X_ne_zero _ hn Finite.one_lt_card)

Goal state after:
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
⊢ indicator c ∈ restrictDegree σ K (Fintype.card K - 1)

Tactic:
mem_restrictDegree_iff_sup,

Goal state after:
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
⊢ ∀ (i : σ), Multiset.count i (indicator c).degrees ≤ Fintype.card K - 1
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
e f g : PerfectClosure K p
x✝² : ℕ × K
m : ℕ
x : K
x✝¹ : ℕ × K
n : ℕ
y : K
x✝ : ℕ × K
s : ℕ
z : K
⊢ Quot.mk (R K p) (m, x) * Quot.mk (R K p) (n, y) * Quot.mk (R K p) (s, z) =
    Quot.mk (R K p) (m, x) * (Quot.mk (R K p) (n, y) * Quot.mk (R K p) (s, z))

Tactic:
apply congr_arg (Quot.mk _)

Goal state after:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
e f g : PerfectClosure K p
x✝² : ℕ × K
m : ℕ
x : K
x✝¹ : ℕ × K
n : ℕ
y : K
x✝ : ℕ × K
s : ℕ
z : K
⊢ (((m, x).1 + (n, y).1, (⇑(frobenius K p))^[(n, y).1] (m, x).2 * (⇑(frobenius K p))^[(m, x).1] (n, y).2).1 + (s, z).1,
      (⇑(frobenius K p))^[(s, z).1]
          ((m, x).1 + (n, y).1, (⇑(frobenius K p))^[(n, y).1] (m, x).2 * (⇑(frobenius K p))^[(m, x).1] (n, y).2).2 *
        (⇑(frobenius K
                p))^[((m, x).1 + (n, y).1,
                (⇑(frobenius K p))^[(n, y).1] (m, x).2 * (⇑(frobenius K p))^[(m, x).1] (n, y).2).1]
          (s, z).2) =
    ((m, x).1 +
        ((n, y).1 + (s, z).1, (⇑(frobenius K p))^[(s, z).1] (n, y).2 * (⇑(frobenius K p))^[(n, y).1] (s, z).2).1,
      (⇑(frobenius K
                p))^[((n, y).1 + (s, z).1,
                (⇑(frobenius K p))^[(s, z).1] (n, y).2 * (⇑(frobenius K p))^[(n, y).1] (s, z).2).1]
          (m, x).2 *
        (⇑(frobenius K p))^[(m, x).1]
          ((n, y).1 + (s, z).1, (⇑(frobenius K p))^[(s, z).1] (n, y).2 * (⇑(frobenius K p))^[(n, y).1] (s, z).2).2)
Module: Mathlib.FieldTheory.IsPerfectClosure

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

Tactic:
refine ⟨fun h ↦ ⟨0, by rw [pow_zero, pow_one, h]⟩, fun ⟨n, h⟩ ↦ ?_⟩

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

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
e f g : PerfectClosure K p
x✝² : ℕ × K
m : ℕ
x : K
x✝¹ : ℕ × K
n : ℕ
y : K
x✝ : ℕ × K
s : ℕ
z : K
⊢ Quot.mk (R K p) (m, x) + Quot.mk (R K p) (n, y) + Quot.mk (R K p) (s, z) =
    Quot.mk (R K p) (m, x) + (Quot.mk (R K p) (n, y) + Quot.mk (R K p) (s, z))

Tactic:
apply congr_arg (Quot.mk _)

Goal state after:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
e f g : PerfectClosure K p
x✝² : ℕ × K
m : ℕ
x : K
x✝¹ : ℕ × K
n : ℕ
y : K
x✝ : ℕ × K
s : ℕ
z : K
⊢ (((m, x).1 + (n, y).1, (⇑(frobenius K p))^[(n, y).1] (m, x).2 + (⇑(frobenius K p))^[(m, x).1] (n, y).2).1 + (s, z).1,
      (⇑(frobenius K p))^[(s, z).1]
          ((m, x).1 + (n, y).1, (⇑(frobenius K p))^[(n, y).1] (m, x).2 + (⇑(frobenius K p))^[(m, x).1] (n, y).2).2 +
        (⇑(frobenius K
                p))^[((m, x).1 + (n, y).1,
                (⇑(frobenius K p))^[(n, y).1] (m, x).2 + (⇑(frobenius K p))^[(m, x).1] (n, y).2).1]
          (s, z).2) =
    ((m, x).1 +
        ((n, y).1 + (s, z).1, (⇑(frobenius K p))^[(s, z).1] (n, y).2 + (⇑(frobenius K p))^[(n, y).1] (s, z).2).1,
      (⇑(frobenius K
                p))^[((n, y).1 + (s, z).1,
                (⇑(frobenius K p))^[(s, z).1] (n, y).2 + (⇑(frobenius K p))^[(n, y).1] (s, z).2).1]
          (m, x).2 +
        (⇑(frobenius K p))^[(m, x).1]
          ((n, y).1 + (s, z).1, (⇑(frobenius K p))^[(s, z).1] (n, y).2 + (⇑(frobenius K p))^[(n, y).1] (s, z).2).2)
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
⊢ ∃ i, ⟨α, hα⟩ ∈ ↑(M i)

Tactic:
have ⟨β, hβ⟩ := h α
      let ϕ : F⟮α⟯ →ₐ[F] K' := (IsScalarTower.toAlgHom _ _ _).comp
        ((AdjoinRoot.liftAlgHom _ _ _ hβ).comp
        (adjoinRootEquivAdjoin F <| (alg.isIntegral).1 _).symm.toAlgHom)
      have ⟨ω, hω⟩ := exists_algHom_adjoin_of_splits
        (fun s hs ↦ ⟨(alg.isIntegral).1 _, splits s hs⟩) ϕ (adjoin_simple_le_iff.mpr hα)
      refine ⟨ω, β, ((DFunLike.congr_fun hω <| AdjoinSimple.gen F α).trans ?_).symm⟩
      rw [AlgHom.comp_apply, AlgHom.comp_apply, AlgEquiv.coe_toAlgHom,
        adjoinRootEquivAdjoin_symm_apply_gen, AdjoinRoot.liftAlgHom_root]
      rfl

Goal state after:
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case ind
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 : ∀ (y : G), y • ↑(H j) ⊆ ⋃ i ∈ {x ∈ s | H x ≠ H j}, (y * x⁻¹ * g i) • ↑(H i)
κ : Type u_2 := ↥({x ∈ s | H x ≠ H j}) × Option ↥({x ∈ s | H x = H j})
f : κ → G :=
  fun x_1 ↦
    match x_1 with
    | (k₁, some k₂) => g ↑k₂ * x⁻¹ * g ↑k₁
    | (k₁, none) => g ↑k₁
K : κ → Subgroup G := fun k ↦ H ↑k.1
hK' : ∀ (k : κ), K k ∈ (Finset.image H s).erase (H j)
⊢ ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex

Tactic:
have hK (k : κ) : K k ≠ H j := ((Finset.mem_erase.mp (hK' k)).left ·)

Goal state after:
case ind
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 : ∀ (y : G), y • ↑(H j) ⊆ ⋃ i ∈ {x ∈ s | H x ≠ H j}, (y * x⁻¹ * g i) • ↑(H i)
κ : Type u_2 := ↥({x ∈ s | H x ≠ H j}) × Option ↥({x ∈ s | H x = H j})
f : κ → G :=
  fun x_1 ↦
    match x_1 with
    | (k₁, some k₂) => g ↑k₂ * x⁻¹ * g ↑k₁
    | (k₁, none) => g ↑k₁
K : κ → Subgroup G := fun k ↦ H ↑k.1
hK' : ∀ (k : κ), K k ∈ (Finset.image H s).erase (H j)
hK : ∀ (k : κ), K k ≠ H j
⊢ ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
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 ∉ k, ¬IsSeparable (↥k) x
⊢ False

Tactic:
replace insep : ∀ x : D, IsSeparable k x → x ∈ k :=
    fun x h ↦ Classical.byContradiction fun hx ↦ insep x hx h

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
⊢ False
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: K : Type u_1
L : Type u_2
S : Type u_3
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Field S
inst✝³ : Algebra K L
inst✝² : Algebra K S
inst✝¹ : Algebra L S
inst✝ : IsScalarTower K L S
c : ConjRootClass K L
⊢ - -c = c

Tactic:
by induction c; rw [mk_neg, mk_neg, neg_neg]

Goal state after: