mathlib-initiative/mathlib-tactics huggingface dataset:
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✝¹ : SigmaFinite μ
f : α → E
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
s : Set α
⊢ ∫ (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✝¹ : SigmaFinite μ
f : α → E
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
s : Set α
⊢ ∫ (x : α) in s, f x ∂ν.withDensity (μ.rnDeriv ν) = ∫ (x : α) in s, f x ∂μ

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

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

Goal state before:
pp: case refine_2
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 : ℕ
R : L[[↑A]].Relations n
x : Fin n → M
⊢ RelMap R (f.toFun ∘ x) ↔ RelMap R x

Tactic:
cases R with
    | inl R => exact f.map_rel' R x
    | inr r => exact isEmptyElim r

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 : M ≃[L] N
⊢ (refl L M).toEmbedding = Embedding.refl L M

Tactic:
refl_toEmbedding

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃[L] N
⊢ Embedding.refl L M = Embedding.refl L M
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 : M ≃[L] N
⊢ (refl L N).toEmbedding = Embedding.refl L N

Tactic:
refl_toEmbedding

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃[L] N
⊢ Embedding.refl L N = Embedding.refl L N
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case refine_3
L : Language
α : Type u'
s : Set α
i j : α
t : Finset ↑s
is : i ∈ s
h✝¹ : ⟨i, ⋯⟩ ∈ t
js : j ∈ s
h✝ : ⟨j, ⋯⟩ ∈ t
⊢ i ∈ s ∧ j ∈ s

Tactic:
exact ⟨is, js⟩

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case e_v
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
n : ℕ
t : L[[α]].Term (β ⊕ Fin n)
v : β → M
xs : Fin n → M
x : α ⊕ β ⊕ Fin n
⊢ (Sum.elim (Sum.elim (fun a ↦ ↑(L.con a)) v) xs ∘ ⇑(Equiv.sumAssoc α β (Fin n)).symm) x =
    Sum.elim (fun a ↦ ↑(L.con a)) (Sum.elim v xs) x

Tactic:
rcases x with (a | (b | i)) <;> simp

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case inr
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
n✝ : ℕ
φ : L[[α]].BoundedFormula β n✝
v : β → M
xs✝ : Fin n✝ → M
n : ℕ
xs : Fin n → M
R : (constantsOn α).Relations n
⊢ RelMap
      ((L.lhomWithConstants α).onRelation ((Equiv.sumEmpty (L.Relations n) ((constantsOn α).Relations n)) (Sum.inr R)))
      xs ↔
    RelMap (Sum.inr R) xs

Tactic:
exact isEmptyElim R

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: case refine_1
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
h : s ∈ (closure L).closed
n : ℕ
f : L.Functions n
⊢ ClosedUnder f ↑((closure L).toFun s)

Tactic:
exact Substructure.fun_mem _ _

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
φ : L.Formula α
g : α → β
v : β → M
⊢ (relabel g φ).Realize v ↔ φ.Realize (v ∘ g)

Tactic:
by
  rw [Realize, Realize, relabel, BoundedFormula.realize_relabel, iff_eq_eq, Fin.castAdd_zero]
  exact congr rfl (funext finZeroElim)

Goal state after:
Module: Mathlib.ModelTheory.ElementarySubstructures

Goal state before:
pp: case e'_8
L : Language
M : Type u_1
inst✝ : L.Structure M
A : Set M
hA : MeetsDefinable A
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x : Fin n → ↥((closure L).toFun A)
a : M
hφ : φ.Realize default (Fin.snoc (Subtype.val ∘ x) a)
D : Set M := {y | φ.Realize default (Fin.snoc (Subtype.val ∘ x) y)}
hD_ne : D.Nonempty
v : Fin 1 → M
i : Fin (n + 1)
⊢ Fin.snoc (Subtype.val ∘ x) (v 0) i =
    ((Sum.elim (fun a ↦ Term.realize v (Fin.lastCases (var 0) (fun j ↦ (L.con ⟨↑(x j), ⋯⟩).term) a)) default ∘
          Sum.inl ∘ Sum.elim Empty.elim id) ∘
        Sum.inr)
      i

Tactic:
cases i using Fin.lastCases <;> simp

Goal state after:
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: case refine_1
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #↑(⇑Equiv.ulift '' s') = #↑s'
⊢ #↑s' + lift.{w', w} #↑s ≤ #↑s'

Tactic:
add_eq_max h1

Goal state after:
case refine_1
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #↑(⇑Equiv.ulift '' s') = #↑s'
⊢ max (#↑s') (lift.{w', w} #↑s) ≤ #↑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 : lift.{w', w} #↑s ≤ lift.{w, w'} #M
⊢ ((L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s).IsSatisfiable

Tactic:
have : Inhabited M := Classical.inhabited_of_nonempty inferInstance
  rw [Cardinal.lift_mk_le'] at h
  let : (constantsOn α).Structure M := constantsOn.structure (Function.extend (↑) h.some default)
  have : M ⊨ (L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s := by
    refine ((LHom.onTheory_model _ _).2 inferInstance).union ?_
    rw [model_distinctConstantsTheory]
    intro a as b bs ab
    rw [← Subtype.coe_mk a as, ← Subtype.coe_mk b bs, ← Subtype.ext_iff]
    exact
      h.some.injective
        ((Subtype.coe_injective.extend_apply h.some default ⟨a, as⟩).symm.trans
          (ab.trans (Subtype.coe_injective.extend_apply h.some default ⟨b, bs⟩)))
  exact Model.isSatisfiable M

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

Tactic:
refine ⟨h1, (mk_union_le _ _).trans ?_, (lift_le.2 card_functions_sum_skolem₁_le).trans ?_⟩
    · rw [← lift_le, lift_add, h, add_comm, add_eq_max h1]
      exact max_le le_rfl h2
    · rw [lift_max, lift_aleph0, max_le_iff, aleph0_le_lift, and_comm, ← lift_le.{w'},
        lift_lift, lift_lift, ← aleph0_le_lift, h]
      refine ⟨?_, h1⟩
      rw [← lift_lift.{w', w}]
      refine _root_.trans (lift_le.{w}.2 h3) ?_
      rw [lift_lift, ← lift_lift.{w, max u v}, ← hs', ← h, lift_lift]

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
ι : Type u_1
T : ι → L.Theory
h : ∀ (s : Finset ι), IsSatisfiable (⋃ i ∈ s, T i)
s : Finset L.Sentence
hs : ↑s ⊆ ⋃ t, ⋃ i ∈ t, T i
⊢ Directed (fun x1 x2 ↦ x1 ⊆ x2) fun i ↦ ⋃ i_1 ∈ i, T i_1

Tactic:
by
    exact Monotone.directed_le fun t1 t2 (h : ∀ ⦃x⦄, x ∈ t1 → x ∈ t2) =>
      Set.iUnion_mono fun _ => Set.iUnion_mono' fun h1 => ⟨h h1, refl _⟩

Goal state after:
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} κ
this : Small.{w, w'} ↥S
⊢ lift.{w', w} #↑(Equiv.bundledInduced L (equivShrink ↥S)) = lift.{w, w'} #↥S

Tactic:
simp only [Equiv.bundledInduced_α, lift_mk_shrink']

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
T' : L.Theory
h : ∀ φ ∈ T', T ⊨ᵇ φ
φ : L.Formula α
hφ : T' ⊨ᵇ φ
M : T.ModelType
hM : ↑M ⊨ T'
M' : T'.ModelType := { Carrier := ↑M, struc := M.struc, is_model := hM, nonempty' := ⋯ }
⊢ ∀ (v : α → ↑M) (xs : Fin 0 → ↑M), BoundedFormula.Realize φ v xs

Tactic:
exact hφ M'

Goal state after:
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
inst✝¹ : IsAlgClosed K
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
⊢ vanishingIdeal k (zeroLocus K I) ≤ I.radical

Tactic:
I.radical_eq_jacobson

Goal state after:
k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
σ : Type u_3
inst✝¹ : IsAlgClosed K
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
⊢ vanishingIdeal k (zeroLocus K I) ≤ I.jacobson
Module: Mathlib.LinearAlgebra.FreeAlgebra

Goal state before:
pp: case inr
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : Set S
h✝ : Nontrivial R
⊢ lift.{u, v} #(List { x // x ∈ s }) ≤ lift.{u, v} (max #↑s ℵ₀)

Tactic:
lift_le,

Goal state after:
case inr
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : Set S
h✝ : Nontrivial R
⊢ #(List { x // x ∈ s }) ≤ max #↑s ℵ₀
Module: Mathlib.LinearAlgebra.FreeAlgebra

Goal state before:
pp: case inr
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : Set S
h✝ : Nontrivial R
⊢ #(List { x // x ∈ s }) ≤ max ℵ₀ #↑s

Tactic:
exact mk_list_le_max _

Goal state after:
Module: Mathlib.FieldTheory.AxGrothendieck

Goal state before:
pp: ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
S : Set (ι → R)
hm : Set.MapsTo (fun v i ↦ (eval v) (ps i)) S S
hinj : Set.InjOn (fun v i ↦ (eval v) (ps i)) S
is_int : ∀ (x : R), IsIntegral K x
v : ι → R
hvS : v ∈ S
val✝ : Fintype ι
s : Finset R := (univ.biUnion fun i ↦ image (fun x ↦ coeff x (ps i)) (ps i).support) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι), ∀ k ∈ (ps i).support, coeff k (ps i) ∈ Algebra.adjoin K ↑s
this✝ : IsNoetherian K ↥(Algebra.adjoin K ↑s)
this : Finite ↥(Algebra.adjoin K ↑s)
S' : Set (ι → ↥(Algebra.adjoin K ↑s)) := (fun v ↦ Subtype.val ∘ v) ⁻¹' S
res : ↑S' → ↑S' := fun x ↦ ⟨fun i ↦ ⟨(eval fun j ↦ ↑(↑x j)) (ps i), ⋯⟩, ⋯⟩
⊢ Function.Surjective res

Tactic:
← Finite.injective_iff_surjective

Goal state after:
ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
S : Set (ι → R)
hm : Set.MapsTo (fun v i ↦ (eval v) (ps i)) S S
hinj : Set.InjOn (fun v i ↦ (eval v) (ps i)) S
is_int : ∀ (x : R), IsIntegral K x
v : ι → R
hvS : v ∈ S
val✝ : Fintype ι
s : Finset R := (univ.biUnion fun i ↦ image (fun x ↦ coeff x (ps i)) (ps i).support) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι), ∀ k ∈ (ps i).support, coeff k (ps i) ∈ Algebra.adjoin K ↑s
this✝ : IsNoetherian K ↥(Algebra.adjoin K ↑s)
this : Finite ↥(Algebra.adjoin K ↑s)
S' : Set (ι → ↥(Algebra.adjoin K ↑s)) := (fun v ↦ Subtype.val ∘ v) ⁻¹' S
res : ↑S' → ↑S' := fun x ↦ ⟨fun i ↦ ⟨(eval fun j ↦ ↑(↑x j)) (ps i), ⋯⟩, ⋯⟩
⊢ Function.Injective res
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: case refine_3.inl.inr.inr
n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : b * c < ℵ₀
hb : b < ℵ₀
hc : c < ℵ₀
⊢ ↑n ∣ b ∨ ↑n ∣ c

Tactic:
lift b to ℕ using hb

Goal state after:
case refine_3.inl.inr.inr
n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
c : Cardinal.{u_1}
hc : c < ℵ₀
b : ℕ
hbc : ↑n ∣ ↑b * c
h' : ↑b * c < ℵ₀
⊢ ↑n ∣ ↑b ∨ ↑n ∣ c
Module: Mathlib.FieldTheory.AxGrothendieck

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : Finite α
inst✝ : Finite ι
p : ℕ
hp : Nat.Prime p
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
this✝ : Fact (Nat.Prime p)
this : CompatibleRing (AlgebraicClosure (ZMod p)) := compatibleRingOfRing (AlgebraicClosure (ZMod p))
⊢ AlgebraicClosure (ZMod p) ⊨ genericPolyMapSurjOnOfInjOn φ mons

Tactic:
realize_genericPolyMapSurjOnOfInjOn

Goal state after:
ι : Type u_1
α : Type u_2
inst✝¹ : Finite α
inst✝ : Finite ι
p : ℕ
hp : Nat.Prime p
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
this✝ : Fact (Nat.Prime p)
this : CompatibleRing (AlgebraicClosure (ZMod p)) := compatibleRingOfRing (AlgebraicClosure (ZMod p))
⊢ ∀ (v : α → AlgebraicClosure (ZMod p)) (p_1 : { p_1 // ∀ (i : ι), (p_1 i).support ⊆ mons i }),
    have f := fun v i ↦ (eval v) (↑p_1 i);
    have S := {x | φ.Realize (Sum.elim v x)};
    Set.MapsTo f S S → Set.InjOn f S → Set.SurjOn f S S
Module: Mathlib.FieldTheory.AxGrothendieck

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : Finite α
inst✝ : Finite ι
p : ℕ
hp : Nat.Prime p ∨ p = 0
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
⊢ Theory.ACF p ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons

Tactic:
by
  rcases hp with hp | rfl
  · exact ACF_models_genericPolyMapSurjOnOfInjOn_of_prime hp φ mons
  · rw [ACF_zero_realize_iff_infinite_ACF_prime_realize]
    convert! Set.infinite_univ (α := Nat.Primes)
    rw [Set.eq_univ_iff_forall]
    intro ⟨p, hp⟩
    exact ACF_models_genericPolyMapSurjOnOfInjOn_of_prime hp φ mons

Goal state after:
Module: Mathlib.FieldTheory.AxGrothendieck

Goal state before:
pp: K : Type u_1
ι : Type u_2
inst✝³ : Field K
inst✝² : IsAlgClosed K
inst✝¹ : Finite ι
inst✝ : CompatibleRing K
c✝ : Set K
S : Set (ι → K)
ps : ι → MvPolynomial ι K
this✝ : Fintype ι := Fintype.ofFinite ι
p : ℕ := ringChar K
c : Finset K
left✝ : ↑c ⊆ c✝
φ : ring.Formula (↑↑c ⊕ ι)
hφ : S = {v | φ.Realize (Sum.elim Subtype.val v)}
this : K ⊨ genericPolyMapSurjOnOfInjOn φ fun i ↦ (ps i).support
⊢ Set.MapsTo (fun v i ↦ (eval v) (ps i)) {v | φ.Realize (Sum.elim Subtype.val v)}
      {v | φ.Realize (Sum.elim Subtype.val v)} →
    Set.InjOn (fun v i ↦ (eval v) (ps i)) {v | φ.Realize (Sum.elim Subtype.val v)} →
      Set.SurjOn (fun v i ↦ (eval v) (ps i)) {v | φ.Realize (Sum.elim Subtype.val v)}
        {v | φ.Realize (Sum.elim Subtype.val v)}

Tactic:
realize_genericPolyMapSurjOnOfInjOn

Goal state after:
K : Type u_1
ι : Type u_2
inst✝³ : Field K
inst✝² : IsAlgClosed K
inst✝¹ : Finite ι
inst✝ : CompatibleRing K
c✝ : Set K
S : Set (ι → K)
ps : ι → MvPolynomial ι K
this✝ : Fintype ι := Fintype.ofFinite ι
p : ℕ := ringChar K
c : Finset K
left✝ : ↑c ⊆ c✝
φ : ring.Formula (↑↑c ⊕ ι)
hφ : S = {v | φ.Realize (Sum.elim Subtype.val v)}
this :
  ∀ (v : ↑↑c → K) (p : { p // ∀ (i : ι), (p i).support ⊆ (ps i).support }),
    have f := fun v i ↦ (eval v) (↑p i);
    have S := {x | φ.Realize (Sum.elim v x)};
    Set.MapsTo f S S → Set.InjOn f S → Set.SurjOn f S S
⊢ Set.MapsTo (fun v i ↦ (eval v) (ps i)) {v | φ.Realize (Sum.elim Subtype.val v)}
      {v | φ.Realize (Sum.elim Subtype.val v)} →
    Set.InjOn (fun v i ↦ (eval v) (ps i)) {v | φ.Realize (Sum.elim Subtype.val v)} →
      Set.SurjOn (fun v i ↦ (eval v) (ps i)) {v | φ.Realize (Sum.elim Subtype.val v)}
        {v | φ.Realize (Sum.elim Subtype.val v)}
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
this : Fintype (Extension k p n)
⊢ Nat.card k ^ n = Nat.card (Extension k p n)

Tactic:
natCard_extension

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
this : Fintype (Extension k p n)
⊢ Nat.card k ^ n = Nat.card k ^ 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
a : σ → K
⊢ (eval a) (indicator a) = 1

Tactic:
nontriviality

Goal state after:
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
a : σ → K
a✝ : Nontrivial K
⊢ (eval a) (indicator a) = 1
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
inst✝ : Algebra.IsSeparable F E
i : (Module.rank F E).ord.ToType
⊢ 2 ≤ toNat #(Emb ↥(adjoin F (⇑b ∘ φ '' Iio i)) ↥(↥(adjoin F (⇑b ∘ φ '' Iio i)))⟮b (φ i)⟯)

Tactic:
← Nat.card,

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
inst✝ : Algebra.IsSeparable F E
i : (Module.rank F E).ord.ToType
⊢ 2 ≤ Nat.card (Emb ↥(adjoin F (⇑b ∘ φ '' Iio i)) ↥(↥(adjoin F (⇑b ∘ φ '' Iio i)))⟮b (φ i)⟯)
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: case neg
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
h : IsNoetherian F E
⊢ toNat #(Emb F E) = finrank F E

Tactic:
← Nat.card,

Goal state after:
case neg
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
h : IsNoetherian F E
⊢ Nat.card (Emb F E) = finrank F E
Module: Mathlib.FieldTheory.IsRealClosed.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
k : ℤ
hk : Odd k
⊢ ∃ r, x = r ^ k

Tactic:
rcases k.eq_nat_or_neg with ⟨n, rfl | rfl⟩

Goal state after:
case inl
R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
n : ℕ
hk : Odd ↑n
⊢ ∃ r, x = r ^ ↑n

case inr
R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
n : ℕ
hk : Odd (-↑n)
⊢ ∃ r, x = r ^ (-↑n)
Module: Mathlib.FieldTheory.IsRealClosed.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
hx : IsSquare x
k : ℤ
hk : k ≠ 0
⊢ ∃ r, x = r ^ k

Tactic:
rcases k.eq_nat_or_neg with ⟨n, rfl | rfl⟩

Goal state after:
case inl
R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
hx : IsSquare x
n : ℕ
hk : ↑n ≠ 0
⊢ ∃ r, x = r ^ ↑n

case inr
R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
hx : IsSquare x
n : ℕ
hk : -↑n ≠ 0
⊢ ∃ r, x = r ^ (-↑n)
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁹ : CommRing K
inst✝⁸ : CommRing L
inst✝⁷ : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst✝⁶ : ExpChar M p
inst✝⁵ : ExpChar K p
inst✝⁴ : ExpChar L p
inst✝³ : PerfectRing L p
inst✝² : IsPerfectClosure i p
inst✝¹ : PerfectRing M p
inst✝ : IsPerfectClosure j p
x : L
⊢ (equiv j i p) ((equiv i j p) x) = x

Tactic:
equiv_comp_equiv_apply,

Goal state after:
K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁹ : CommRing K
inst✝⁸ : CommRing L
inst✝⁷ : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst✝⁶ : ExpChar M p
inst✝⁵ : ExpChar K p
inst✝⁴ : ExpChar L p
inst✝³ : PerfectRing L p
inst✝² : IsPerfectClosure i p
inst✝¹ : PerfectRing M p
inst✝ : IsPerfectClosure j p
x : L
⊢ (equiv i i p) x = x
Module: Mathlib.FieldTheory.JacobsonNoether

Goal state before:
pp: case pos
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
m : ℕ
hm2 : ∀ (n : ℕ), p ^ m ≤ n → (⇑((ad (↥k) D) a))^[n] = 0
h_exist : ∃ n, 0 < n ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0
t : ℕ := Nat.find h_exist - 1
ht : t = Nat.find h_exist - 1
h_pos : 0 < t
⊢ (⇑((ad (↥k) D) a))^[Nat.find h_exist] b ≠ 0

Tactic:
convert! (ne_eq _ _) ▸ not_and.mp (Nat.find_min h_exist (m := t) (by lia)) h_pos
      lia

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
inst✝ : Algebra.Transcendental F E
⊢ Module.rank F E = #E

Tactic:
obtain ⟨ι, x, hx⟩ := exists_isTranscendenceBasis' F E
  have := hx.nonempty_iff_transcendental.2 ‹_›
  simpa [← hx.lift_cardinalMk_eq_max_lift] using hx.lift_rank_eq_max_lift

Goal state after:
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case neg
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
j : ι
hj : j ∈ s
hcovers' : ¬⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) = Set.univ
⊢ ∃ k ∈ s, (H k).FiniteIndex

Tactic:
have ⟨i, hi, _, hfi⟩ :=
      exists_finiteIndex_of_leftCoset_cover_aux hcovers j hj hcovers'

Goal state after:
case neg
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
j : ι
hj : j ∈ s
hcovers' : ¬⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) = Set.univ
i : ι
hi : i ∈ s
left✝ : H i ≠ H j
hfi : (H i).FiniteIndex
⊢ ∃ k ∈ s, (H k).FiniteIndex
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
ι : Type u_1
a : Basis ι R ↥A
H : (Submodule.mulLeftMap (toSubmodule B) ⇑a).ker = ⊥
⊢ A.LinearDisjoint B

Tactic:
exact Submodule.LinearDisjoint.of_basis_left _ _ a H

Goal state after:
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case inr
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
h : ∀ i ∈ s, (H i).FiniteIndex → s.card < (H i).index
hs : s.Nonempty
hs' : 0 < s.card
hlt : ∀ i ∈ s, (↑(H i).index)⁻¹ < (↑s.card)⁻¹
⊢ ↑s.card * (↑s.card)⁻¹ = 1

Tactic:
mul_inv_cancel₀ (Nat.cast_ne_zero.mpr hs'.ne')

Goal state after:
case inr
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
h : ∀ i ∈ s, (H i).FiniteIndex → s.card < (H i).index
hs : s.Nonempty
hs' : 0 < s.card
hlt : ∀ i ∈ s, (↑(H i).index)⁻¹ < (↑s.card)⁻¹
⊢ 1 = 1
Module: Mathlib.FieldTheory.NormalizedTrace

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F K
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
f : E →ₐ[F] K
a : E
⊢ normalizedTraceAux F K (f a) = normalizedTraceAux F E a

Tactic:
let e := (F⟮a⟯.equivMap f).trans (equivOfEq <| Set.image_singleton ▸ adjoin_map F {a} f)
  simp_rw [normalizedTraceAux, ← LinearEquiv.finrank_eq e.toLinearEquiv]
  congr
  exact trace_eq_of_algEquiv e <| AdjoinSimple.gen F a

Goal state after: