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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
h : μ.rnDeriv ν ≤ᵐ[ν] 1
s : Set α
⊢ ∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν ≤ ∫⁻ (x : α) in s, 1 ∂ν

Tactic:
exact setLIntegral_mono_ae aemeasurable_const (h.mono fun _ hh _ ↦ hh)

Goal state after:
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: case refine_1.inr.zero
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
x : Fin 0 → M
c : (constantsOn ↑A).Functions 0
⊢ f.toFun (funMap (Sum.inr c) x) = funMap (Sum.inr c) (f.toFun ∘ x)

Tactic:
| zero =>

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
n : ℕ
hn : n ≠ 0
hx : x ^ n ∈ algebraicClosure F E
⊢ x ∈ algebraicClosure F E

Tactic:
rw [mem_algebraicClosure_iff] at hx ⊢

Goal state after:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
n : ℕ
hn : n ≠ 0
hx : IsAlgebraic F (x ^ n)
⊢ IsAlgebraic F x
Module: Mathlib.ModelTheory.Algebra.Ring.Basic

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝⁵ : Add R
inst✝⁴ : Mul R
inst✝³ : Neg R
inst✝² : One R
inst✝¹ : Zero R
inst✝ : CompatibleRing R
x y : ring.Term α
v : α → R
⊢ Term.realize v (x * y) = Term.realize v x * Term.realize v y

Tactic:
simp [mul_def, funMap_mul]

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case hq.refine_2
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
s : Multiset p.SplittingField
hs :
  map (algebraMap F p.SplittingField) p =
    C (map (algebraMap F p.SplittingField) p).leadingCoeff * (Multiset.map (fun x ↦ X - C x) s).prod
q : p.SplittingField[X]
hq : q ∈ Multiset.map (fun p_1 ↦ p_1.comp (X ^ n)) (Multiset.map (fun x ↦ X - C x) s)
⊢ Group.IsSolvable q.Gal

Tactic:
Multiset.mem_map

Goal state after:
case hq.refine_2
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
s : Multiset p.SplittingField
hs :
  map (algebraMap F p.SplittingField) p =
    C (map (algebraMap F p.SplittingField) p).leadingCoeff * (Multiset.map (fun x ↦ X - C x) s).prod
q : p.SplittingField[X]
hq : ∃ a ∈ Multiset.map (fun x ↦ X - C x) s, a.comp (X ^ n) = q
⊢ Group.IsSolvable q.Gal
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case hq.refine_2
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
s : Multiset p.SplittingField
hs :
  map (algebraMap F p.SplittingField) p =
    C (map (algebraMap F p.SplittingField) p).leadingCoeff * (Multiset.map (fun x ↦ X - C x) s).prod
q : p.SplittingField[X]
hq : q ∈ Multiset.map (fun x ↦ X - C x) s
⊢ Group.IsSolvable (q.comp (X ^ n)).Gal

Tactic:
Multiset.mem_map

Goal state after:
case hq.refine_2
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
s : Multiset p.SplittingField
hs :
  map (algebraMap F p.SplittingField) p =
    C (map (algebraMap F p.SplittingField) p).leadingCoeff * (Multiset.map (fun x ↦ X - C x) s).prod
q : p.SplittingField[X]
hq : ∃ a ∈ s, X - C a = q
⊢ Group.IsSolvable (q.comp (X ^ n)).Gal
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
h :
  (φ.restrictFreeVar id).Realize (((↑f ∘ Sum.elim (v ∘ Subtype.val) xs) ∘ id) ∘ Sum.inl)
      (((↑f ∘ Sum.elim (v ∘ Subtype.val) xs) ∘ id) ∘ Sum.inr) ↔
    (φ.restrictFreeVar id).Realize
      (((Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n)).symm) ∘
          ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n))) ∘
        Sum.inl)
      (((Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n)).symm) ∘
          ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n))) ∘
        Sum.inr)
⊢ (φ.restrictFreeVar id).Realize ((⇑f ∘ v) ∘ Subtype.val) (⇑f ∘ xs) ↔ φ.Realize v xs

Tactic:
Function.comp_id,

Goal state after:
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
h :
  (φ.restrictFreeVar id).Realize ((↑f ∘ Sum.elim (v ∘ Subtype.val) xs) ∘ Sum.inl)
      ((↑f ∘ Sum.elim (v ∘ Subtype.val) xs) ∘ Sum.inr) ↔
    (φ.restrictFreeVar id).Realize
      (((Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n)).symm) ∘
          ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n))) ∘
        Sum.inl)
      (((Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n)).symm) ∘
          ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n))) ∘
        Sum.inr)
⊢ (φ.restrictFreeVar id).Realize ((⇑f ∘ v) ∘ Subtype.val) (⇑f ∘ xs) ↔ φ.Realize v xs
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
h :
  (φ.restrictFreeVar id).Realize ((↑f ∘ v) ∘ Subtype.val) (↑f ∘ xs) ↔
    (φ.restrictFreeVar id).Realize
      (((Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n)).symm) ∘
          ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n))) ∘
        Sum.inl)
      (((Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n)).symm) ∘
          ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n))) ∘
        Sum.inr)
⊢ (φ.restrictFreeVar id).Realize ((Sum.elim (v ∘ Subtype.val) xs ∘ id) ∘ Sum.inl)
      ((Sum.elim (v ∘ Subtype.val) xs ∘ id) ∘ Sum.inr) ↔
    φ.Realize v xs

Tactic:
Function.comp_id,

Goal state after:
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
h :
  (φ.restrictFreeVar id).Realize ((↑f ∘ v) ∘ Subtype.val) (↑f ∘ xs) ↔
    (φ.restrictFreeVar id).Realize
      (((Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n)).symm) ∘
          ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n))) ∘
        Sum.inl)
      (((Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n)).symm) ∘
          ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n))) ∘
        Sum.inr)
⊢ (φ.restrictFreeVar id).Realize (Sum.elim (v ∘ Subtype.val) xs ∘ Sum.inl) (Sum.elim (v ∘ Subtype.val) xs ∘ Sum.inr) ↔
    φ.Realize v xs
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
φ : L.Formula (Fin n)
v : Empty → M
x : Fin n → M
⊢ BoundedFormula.Realize φ (x ∘ id) (x ∘ natAdd n) ↔ BoundedFormula.Realize φ x default

Tactic:
Function.comp_id,

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
φ : L.Formula (Fin n)
v : Empty → M
x : Fin n → M
⊢ BoundedFormula.Realize φ x (x ∘ natAdd n) ↔ BoundedFormula.Realize φ x default
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case zero
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n : ℕ
v : α → M
φ : L.BoundedFormula α 0
⊢ φ.alls.Realize v ↔ ∀ (xs : Fin 0 → M), φ.Realize v xs

Tactic:
| zero =>

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case zero
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n : ℕ
v : α → M
φ : L.BoundedFormula α 0
⊢ φ.exs.Realize v ↔ ∃ xs, φ.Realize v xs

Tactic:
| zero =>

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
p : (x : M) → x ∈ (closure L).toFun s → Prop
Hs : ∀ (x : M) (h : x ∈ s), p x ⋯
Hfun : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f {x | ∃ (hx : x ∈ (closure L).toFun s), p x hx}
x : M
hx : x ∈ (closure L).toFun s
⊢ ∃ (x_1 : x ∈ (closure L).toFun s), p x x_1

Tactic:
exact closure_induction hx (fun x hx => ⟨subset_closure hx, Hs x hx⟩) @Hfun

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
A s : Set M
⊢ A ⊆ ↑((closure L[[↑A]]).toFun s)

Tactic:
intro a

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
A s : Set M
a : M
⊢ a ∈ A → a ∈ ↑((closure L[[↑A]]).toFun s)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
v' : Fin 0 → M
⊢ Realize (Formula.iAlls β φ) v v' ↔ ∀ (i : β → M), φ.Realize fun a ↦ Sum.elim v i a

Tactic:
rw [← Formula.realize_iAlls, iff_iff_eq]

Goal state after:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
v' : Fin 0 → M
⊢ Realize (Formula.iAlls β φ) v v' = (Formula.iAlls β φ).Realize v
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case all.e__v
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ (v : α ⊕ Fin (n✝ + 1) → M), f✝.toFormula.Realize v ↔ f✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n✝ → M
a : M
h :
  f✝.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)) ↔ f✝.Realize (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)
x : α ⊕ Fin (n✝ + 1)
⊢ Sum.elim v (fun x ↦ snoc default a (castAdd 0 x))
      (Sum.elim (fun x ↦ Sum.inl (Sum.inl x)) (fun x ↦ Sum.map Sum.inr id (finSumFinEquiv.symm x)) x) =
    Sum.elim (fun x ↦ v (Sum.inl x)) (snoc (fun x ↦ v (Sum.inr x)) a) x

Tactic:
rcases x with _ | x
      · simp
      · refine Fin.lastCases ?_ ?_ x
        · simp [Fin.snoc]
        · simp only [castSucc, Sum.elim_inr,
            finSumFinEquiv_symm_apply_castAdd, Sum.map_inl, Sum.elim_inl]
          rw [← castSucc]
          simp

Goal state after:
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: 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'
⊢ #↥((closure (L.sum L.skolem₁)).toFun (s ∪ ⇑Equiv.ulift '' s')) = #↑(⇑Equiv.ulift '' s')

Tactic:
refine
    le_antisymm (lift_le.1 (lift_card_closure_le.trans ?_))
      (mk_le_mk_of_subset ((s.subset_union_right).trans subset_closure))

Goal state after:
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'
⊢ max ℵ₀ (lift.{max u v, w} #↑(s ∪ ⇑Equiv.ulift '' s') + lift.{w, max u v} #((i : ℕ) × (L.sum L.skolem₁).Functions i)) ≤
    lift.{max u v, 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)
⊢ Set.InjOn (fun i ↦ ↑(L.con i)) s

Tactic:
intro a

Goal state after:
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 : α
⊢ a ∈ s → ∀ ⦃x₂ : α⦄, x₂ ∈ s → (fun i ↦ ↑(L.con i)) a = (fun i ↦ ↑(L.con i)) x₂ → a = x₂
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
κ : Cardinal.{w}
M : Type w'
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ ∃ N, lift.{max u v w, w} κ ≤ #↑N

Tactic:
obtain ⟨N⟩ :=
    isSatisfiable_union_distinctConstantsTheory_of_infinite T (Set.univ : Set κ.out) M

Goal state after:
L : Language
T : L.Theory
κ : Cardinal.{w}
M : Type w'
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ((L.lhomWithConstants (Quotient.out κ)).onTheory T ∪ L.distinctConstantsTheory Set.univ).ModelType
⊢ ∃ N, lift.{max u v w, w} κ ≤ #↑N
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
M : Type w'
inst✝ : L.Structure M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h3 : lift.{w', w} κ ≤ lift.{w, w'} #M
S : L.ElementarySubstructure M
left✝ : ∅ ⊆ ↑S
hS : lift.{w, w'} #↥S = lift.{w', w} κ
⊢ Small.{w, w'} ↥S

Tactic:
rw [← lift_inj.{_, w + 1}, lift_lift, lift_lift] at hS

Goal state after:
L : Language
M : Type w'
inst✝ : L.Structure M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h3 : lift.{w', w} κ ≤ lift.{w, w'} #M
S : L.ElementarySubstructure M
left✝ : ∅ ⊆ ↑S
hS : lift.{w + 1, w'} #↥S = lift.{max w' (w + 1), w} κ
⊢ Small.{w, w'} ↥S
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case mpr
L : Language
T : L.Theory
hsat : T.IsSatisfiable
h : ∀ (M N : T.ModelType), ↑M ≅[L] ↑N
⊢ ∀ (φ : L.Sentence), T ⊨ᵇ φ ∨ T ⊨ᵇ Formula.not φ

Tactic:
intro φ

Goal state after:
case mpr
L : Language
T : L.Theory
hsat : T.IsSatisfiable
h : ∀ (M N : T.ModelType), ↑M ≅[L] ↑N
φ : L.Sentence
⊢ T ⊨ᵇ φ ∨ T ⊨ᵇ Formula.not φ
Module: Mathlib.RingTheory.Localization.Cardinality

Goal state before:
pp: R : Type u
inst✝³ : CommSemiring R
L : Type v
inst✝² : CommSemiring L
inst✝¹ : Algebra R L
S : Submonoid R
inst✝ : IsLocalization S L
this : #(Localization S) ≤ #R
⊢ Cardinal.lift.{u, v} #L ≤ Cardinal.lift.{v, u} #R

Tactic:
← lift_le.{v},

Goal state after:
R : Type u
inst✝³ : CommSemiring R
L : Type v
inst✝² : CommSemiring L
inst✝¹ : Algebra R L
S : Submonoid R
inst✝ : IsLocalization S L
this : Cardinal.lift.{v, u} #(Localization S) ≤ Cardinal.lift.{v, u} #R
⊢ Cardinal.lift.{u, v} #L ≤ Cardinal.lift.{v, u} #R
Module: Mathlib.FieldTheory.Differential.Basic

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
a : R
⊢ logDeriv (a ^ 0) = ↑0 * logDeriv a

Tactic:
| zero =>

Goal state after:
Module: Mathlib.FieldTheory.Finite.Extension

Goal state before:
pp: case zero
k : Type u_1
inst✝⁴ : Field k
inst✝³ : Finite k
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP k p
n : ℕ
inst✝ : NeZero n
x : Extension k p n
⊢ (frob k p n ^ 0) x = x ^ Nat.card k ^ 0

Tactic:
| zero =>

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

Goal state before:
pp: F : Type u_2
inst✝⁵ : Field F
inst✝⁴ : Differential F
inst✝³ : CharZero F
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
k : K := ⋯.choose
h : F⟮k⟯ = ⊤
this✝ : Fact (minpoly F k).Monic
this : Fact (Irreducible (minpoly F k))
⊢ DifferentialAlgebra F K

Tactic:
apply DifferentialAlgebra.equiv

Goal state after:
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: case C
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
⊢ ∀ (a : ZMod p), (frobenius (MvPolynomial σ (ZMod p)) p) (C a) = (expand p) (C a)

Tactic:
intro a

Goal state after:
case C
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
a : ZMod p
⊢ (frobenius (MvPolynomial σ (ZMod p)) p) (C a) = (expand p) (C a)
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: case refine_2
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
⊢ ⇑b '' Iio (φ i) ⊆ ↑(adjoin F (⇑b ∘ φ '' Iio i))

Tactic:
· rintro _ ⟨j, hj, rfl⟩; contrapose hj; exact ((isLeast_leastExt i).2 hj).not_gt

Goal state after:
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
⊢ mk K p (0, 0) = 0

Tactic:
| zero =>

Goal state after:
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
n : ℕ
x : K
⊢ mk K p (n, x) = mk K p (0 + n, (⇑(frobenius K p))^[0] x)

Tactic:
| zero =>

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

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

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

Tactic:
| zero =>

Goal state after:
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 : ℕ
⊢ ↑x = mk K p (0, ↑x)

Tactic:
| zero =>

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

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

Tactic:
rw [ih]; apply Quot.sound
    suffices R K p (n, (x : K)) (Nat.succ n, frobenius K p (x : K)) by
      rwa [map_natCast] at this
    apply R.intro

Goal state after:
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
⊢ (⇑(frobenius (PerfectClosure K p) p))^[0] (mk K p (0, x)) = (of K p) x

Tactic:
| zero =>

Goal state after:
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ
hind : H.index = s.card
this : Fintype (G ⧸ H)
⊢ (↑s).PairwiseDisjoint fun x ↦ g x • ↑H

Tactic:
suffices Function.Bijective (g · : s → G ⧸ H) by
    intro i hi j hj h' c hi' hj' x hx
    specialize hi' hx
    specialize hj' hx
    rw [mem_leftCoset_iff, SetLike.mem_coe, ← QuotientGroup.eq] at hi' hj'
    rw [ne_eq, ← Subtype.mk.injEq (p := (· ∈ (s : Set ι))) i hi j hj] at h'
    exact h' <| this.injective <| by simp only [hi', hj']

Goal state after:
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ
hind : H.index = s.card
this : Fintype (G ⧸ H)
⊢ Function.Bijective fun x ↦ ↑(g ↑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 : ι
hi : i ∈ s
hmem : ↑(g i) = ↑(x * (y⁻¹ * z))
⊢ ∃ i, ∃ (_ : i ∈ s ∧ H i ≠ H j), z ∈ (y * x⁻¹ * g i) • ↑(H i)

Tactic:
refine ⟨i, ⟨hi, fun hij => hx i hi hij ?_⟩, ?_⟩

Goal state after:
case refine_1
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 : ι
hi : i ∈ s
hmem : ↑(g i) = ↑(x * (y⁻¹ * z))
hij : H i = H j
⊢ ↑(g i) = ↑x

case refine_2
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 : ι
hi : i ∈ s
hmem : ↑(g i) = ↑(x * (y⁻¹ * z))
⊢ z ∈ (y * x⁻¹ * g i) • ↑(H i)
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 := ⋯ }
⊢ (⇑((ad (↥k) D) a))^[n.succ] b = 0

Tactic:
hb.2

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 := ⋯ }
⊢ 0 = 0
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} (max #↥K ℵ₀) = max (max (lift.{max w v, u} #F) (lift.{max u v, w} #ι)) ℵ₀

Tactic:
simp [K, ← lift_mk_eq'.2 ⟨hx.1.aevalEquivField.toEquiv⟩]

Goal state after:
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case zero
K : Type u
inst✝ : Field K
hn : Odd 0
a : K
ha : ∀ (p : ℕ), Nat.Prime p → p ∣ 0 → ∀ (b : K), b ^ p ≠ a
⊢ Irreducible (X ^ 0 - C a)

Tactic:
| zero =>

Goal state after: