mathlib-initiative/mathlib-tactics huggingface dataset:
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 ν))
⊢ (fun x ↦ (map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x)) =ᵐ[ν]
    (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν

Tactic:
have : SigmaFinite (map f (ν.withDensity (μ.rnDeriv ν))) := hf.sigmaFinite_map

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 ν)))
⊢ (fun x ↦ (map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x)) =ᵐ[ν]
    (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
Module: Mathlib.RingTheory.Algebraic.Cardinality

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
L : Type v
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
inst✝² : Algebra R L
inst✝¹ : IsTorsionFree R L
inst✝ : Algebra.IsAlgebraic R L
⊢ max (max (lift.{v, u} #R[X]) ℵ₀) ℵ₀ ≤ max (max (lift.{v, u} (max #R ℵ₀)) ℵ₀) ℵ₀

Tactic:
gcongr

Goal state after:
case h₁
R : Type u
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
L : Type v
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
inst✝² : Algebra R L
inst✝¹ : IsTorsionFree R L
inst✝ : Algebra.IsAlgebraic R L
⊢ lift.{v, u} #R[X] ≤ lift.{v, u} (max #R ℵ₀)
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
f : M ≃[L] N
n : ℕ
f' : L.Functions n
x : Fin n → N
⊢ funMap f' x = funMap f' ((f.toFun ∘ ⇑f.symm) ∘ x)

Tactic:
Equiv.toFun_as_coe,

Goal state after:
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
f : M ≃[L] N
n : ℕ
f' : L.Functions n
x : Fin n → N
⊢ funMap f' x = funMap f' ((⇑f.toEquiv ∘ ⇑f.symm) ∘ x)
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
f : M ≃[L] N
n : ℕ
r : L.Relations n
x : Fin n → N
⊢ RelMap r ((f.toFun ∘ ⇑f.symm) ∘ x) ↔ RelMap r x

Tactic:
Equiv.toFun_as_coe,

Goal state after:
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
f : M ≃[L] N
n : ℕ
r : L.Relations n
x : Fin n → N
⊢ RelMap r ((⇑f.toEquiv ∘ ⇑f.symm) ∘ x) ↔ RelMap r x
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
M : Type u_1
N : Type u_2
inst✝ : L.Structure M
e : M ≃ N
⊢ M ≃[L] N

Tactic:
by
  letI : L.Structure N := inducedStructure e
  exact
  { e with
    map_fun' := @fun n f x => by simp [← Function.comp_assoc e.symm e x]
    map_rel' := @fun n r x => by simp [← Function.comp_assoc e.symm e x] }

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case inl
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
y z : E
hy : y ∈ solvableByRad F E
hz : z ∈ solvableByRad F E
hy' : Group.IsSolvable (minpoly F y).Gal
q : F[X] := minpoly F y
a : E
hx : a ∈ solvableByRad F E
hx' : Group.IsSolvable (minpoly F a).Gal
hz' : z ∈ F⟮a, y⟯
p : F[X] := minpoly F a
hpq :
  (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F a)).Splits ∧
    (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F y)).Splits
⊢ IsIntegral F a ∧ (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F a)).Splits

Tactic:
exact ⟨isIntegral_of_mem_solvableByRad hx, hpq.1⟩

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n _m _n : ℕ
h : _m ≤ _n
f : L.BoundedFormula α (_m + 1)
⊢ _m + 1 ≤ _n + 1

Tactic:
gcongr

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case all
L : Language
α : Type u'
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : (LHom.id L).onBoundedFormula f✝ = id f✝
⊢ ((LHom.id L).onBoundedFormula f✝).all = id f✝.all

Tactic:
ih3,

Goal state after:
case all
L : Language
α : Type u'
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : (LHom.id L).onBoundedFormula f✝ = id f✝
⊢ (id f✝).all = id f✝.all
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
α : Type u'
s t : Set α
h : s ⊆ t
⊢ (fun ab ↦ ((L.con ab.1).term.equal (L.con ab.2).term).not) '' (s ×ˢ s ∩ (diagonal α)ᶜ) ⊆
    (fun ab ↦ ((L.con ab.1).term.equal (L.con ab.2).term).not) '' (t ×ˢ t ∩ (diagonal α)ᶜ)

Tactic:
gcongr

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case func
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
n : ℕ
f : L[[α]].Functions n
ts : Fin n → L[[α]].Term β
ih : ∀ (a : Fin n), realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (ts a).constantsToVars = realize v (ts a)
⊢ realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (func f ts).constantsToVars = realize v (func f ts)

Tactic:
cases n
    · cases f
      · simp only [realize, ih, constantsOn, constantsOnFunc, constantsToVars]
        -- Porting note: below lemma does not work with simp for some reason
        rw [withConstants_funMap_sumInl]
      · simp only [realize, constantsToVars, Sum.elim_inl, funMap_eq_coe_constants]
        rfl
    · obtain - | f := f
      · simp only [realize, ih, constantsOn, constantsOnFunc, constantsToVars]
        -- Porting note: below lemma does not work with simp for some reason
        rw [withConstants_funMap_sumInl]
      · exact isEmptyElim f

Goal state after:
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: case refine_1
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → L.Structure (M a)
n : ℕ
r : L.Relations n
x y : Fin n → (a : α) → M a
xy : x ≈ y
hx : ∀ᶠ (a : α) in ↑u, RelMap r fun i ↦ x i a
a : α
ha1 : RelMap r fun i ↦ x i a
ha2 : ∀ (i : Fin n), x i a = y i a
⊢ RelMap r fun i ↦ y i a

Tactic:
rw [← funext ha2]

Goal state after:
case refine_1
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → L.Structure (M a)
n : ℕ
r : L.Relations n
x y : Fin n → (a : α) → M a
xy : x ≈ y
hx : ∀ᶠ (a : α) in ↑u, RelMap r fun i ↦ x i a
a : α
ha1 : RelMap r fun i ↦ x i a
ha2 : ∀ (i : Fin n), x i a = y i a
⊢ RelMap r fun x_1 ↦ x x_1 a
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: L : Language
α : Type u'
l : List (L.Term α)
⊢ listDecode (flatMap listEncode l) = l

Tactic:
suffices h : ∀ (t : L.Term α) (l : List (α ⊕ (Σ i, L.Functions i))),
      listDecode (t.listEncode ++ l) = t::listDecode l by
    induction l with
    | nil => rfl
    | cons t l lih => rw [flatMap_cons, h t (l.flatMap listEncode), lih]

Goal state after:
L : Language
α : Type u'
l : List (L.Term α)
⊢ ∀ (t : L.Term α) (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode (t.listEncode ++ l) = t :: listDecode l
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 : α ≃ β
⊢ A.Definable L ((fun g ↦ g ∘ ⇑f) '' s)

Tactic:
by
  refine (congr rfl ?_).mp (h.preimage_comp f.symm)
  rw [image_eq_preimage_of_inverse]
  · intro i
    ext b
    simp only [Function.comp_apply, Equiv.apply_symm_apply]
  · intro i
    ext a
    simp

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case h₁.e__v
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
i y : γ → M
x : α ⊕ γ
⊢ Sum.elim (Sum.elim v i) y (Sum.elim (fun x ↦ Sum.inl (Sum.inl x)) Sum.inr x) = Sum.elim v y x

Tactic:
cases x <;> simp

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: 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
⊢ DefinableFun L A fun v ↦ f (g v)

Tactic:
let G : (Option β → M) → Option α → M := fun w j =>
    match j with
    | none => w none
    | some i => g (w ∘ some) i
  have hG : A.DefinableMap L G := by
    intro i
    cases i with
    | none => fun_prop
    | some j =>
      simpa [tupleGraph] using!
        ((hg j).preimage_comp fun | none => none | some i => some (some i))
  simpa [DefinableFun, G, tupleGraph] using! hf.preimage_map hG

Goal state after:
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: case refine_2
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'
⊢ lift.{max (max u v) w, w'} κ ≤ lift.{max (max u v) w', w} #↑(⇑Equiv.ulift '' s')

Tactic:
← lift_lift.{w, max u v},

Goal state after:
case refine_2
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'
⊢ lift.{max u v, max w w'} (lift.{w, w'} κ) ≤ lift.{max (max u v) w', w} #↑(⇑Equiv.ulift '' s')
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
ι : Type u_1
T : ι → L.Theory
⊢ IsSatisfiable (⋃ i, T i) ↔ ∀ (s : Finset ι), IsSatisfiable (⋃ i ∈ s, T i)

Tactic:
refine
    ⟨fun h s => h.mono (Set.iUnion_mono fun _ => Set.iUnion_subset_iff.2 fun _ => refl _),
      fun h => ?_⟩

Goal state after:
L : Language
ι : Type u_1
T : ι → L.Theory
h : ∀ (s : Finset ι), IsSatisfiable (⋃ i ∈ s, T i)
⊢ IsSatisfiable (⋃ i, T i)
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: p : ℕ
κ : Cardinal.{u_2}
hκ : ℵ₀ < κ
M : Type u_2
struc✝¹ : Language.ring.Structure M
is_model✝¹ : M ⊨ Theory.ACF p
nonempty'✝¹ : Nonempty M
N : Type u_2
struc✝ : Language.ring.Structure N
is_model✝ : N ⊨ Theory.ACF p
nonempty'✝ : Nonempty N
hM : #↑{ Carrier := M, struc := struc✝¹, is_model := is_model✝¹, nonempty' := nonempty'✝¹ } = κ
hN : #↑{ Carrier := N, struc := struc✝, is_model := is_model✝, nonempty' := nonempty'✝ } = κ
x✝³ : Field M := fieldOfModelACF p M
this✝² : M ⊨ Theory.field
x✝² : CompatibleRing M := compatibleRingOfModelField M
this✝¹ : IsAlgClosed M
this✝ : CharP M p
x✝¹ : Field N := fieldOfModelACF p N
this : N ⊨ Theory.field
x✝ : CompatibleRing N := compatibleRingOfModelField N
⊢ Nonempty
    (↑{ Carrier := M, struc := struc✝¹, is_model := is_model✝¹, nonempty' := nonempty'✝¹ } ≃[Language.ring]
      ↑{ Carrier := N, struc := struc✝, is_model := is_model✝, nonempty' := nonempty'✝ })

Tactic:
have := isAlgClosed_of_model_ACF p N

Goal state after:
p : ℕ
κ : Cardinal.{u_2}
hκ : ℵ₀ < κ
M : Type u_2
struc✝¹ : Language.ring.Structure M
is_model✝¹ : M ⊨ Theory.ACF p
nonempty'✝¹ : Nonempty M
N : Type u_2
struc✝ : Language.ring.Structure N
is_model✝ : N ⊨ Theory.ACF p
nonempty'✝ : Nonempty N
hM : #↑{ Carrier := M, struc := struc✝¹, is_model := is_model✝¹, nonempty' := nonempty'✝¹ } = κ
hN : #↑{ Carrier := N, struc := struc✝, is_model := is_model✝, nonempty' := nonempty'✝ } = κ
x✝³ : Field M := fieldOfModelACF p M
this✝³ : M ⊨ Theory.field
x✝² : CompatibleRing M := compatibleRingOfModelField M
this✝² : IsAlgClosed M
this✝¹ : CharP M p
x✝¹ : Field N := fieldOfModelACF p N
this✝ : N ⊨ Theory.field
x✝ : CompatibleRing N := compatibleRingOfModelField N
this : IsAlgClosed N
⊢ Nonempty
    (↑{ Carrier := M, struc := struc✝¹, is_model := is_model✝¹, nonempty' := nonempty'✝¹ } ≃[Language.ring]
      ↑{ Carrier := N, struc := struc✝, is_model := is_model✝, nonempty' := nonempty'✝ })
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
φ : L.Sentence
M : T.ModelType
h : ↑M ⊨ Formula.not φ
ψ : L.Sentence
hψ : ψ ∈ T ∪ {Formula.not φ}
h' : ψ ∈ {Formula.not φ}
⊢ ↑M ⊨ ψ

Tactic:
rw [Set.mem_singleton_iff.1 h']

Goal state after:
L : Language
T : L.Theory
φ : L.Sentence
M : T.ModelType
h : ↑M ⊨ Formula.not φ
ψ : L.Sentence
hψ : ψ ∈ T ∪ {Formula.not φ}
h' : ψ ∈ {Formula.not φ}
⊢ ↑M ⊨ Formula.not φ
Module: Mathlib.ModelTheory.Satisfiability

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

Tactic:
Theory.models_sentence_iff,

Goal state after:
L : Language
κ : Cardinal.{w}
T : L.Theory
h : κ.Categorical T
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
hS : T.IsSatisfiable
hT : ∀ (M : T.ModelType), Infinite ↑M
φ : L.Sentence
w✝ : T.ModelType
h✝ : #↑w✝ = κ
⊢ (∀ (M : T.ModelType), ↑M ⊨ φ) ∨ T ⊨ᵇ Formula.not φ
Module: Mathlib.FieldTheory.AxGrothendieck

Goal state before:
pp: case intro
ι : 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
⊢ v ∈ (fun v i ↦ (eval v) (ps i)) '' S

Tactic:
have := isNoetherian_adjoin_finset s fun x _ => is_int x

Goal state after:
case intro
ι : 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)
⊢ v ∈ (fun v i ↦ (eval v) (ps i)) '' S
Module: Mathlib.GroupTheory.OreLocalization.Cardinality

Goal state before:
pp: R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite X
⊢ Surjective fun x ↦ x /ₒ 1

Tactic:
by
  refine OreLocalization.ind fun x s ↦ ?_
  obtain ⟨i, j, hne, heq⟩ := Finite.exists_ne_map_eq_of_infinite (α := ℕ) (s ^ · • x)
  wlog! hlt : j < i generalizing i j
  · exact this j i hne.symm heq.symm (hne.lt_of_le hlt)
  use s ^ (i - (j + 1)) • x
  rw [oreDiv_eq_iff]
  refine ⟨s ^ j, (s ^ (j + 1)).1, ?_, ?_⟩
  · change s ^ j • x = s ^ (j + 1) • s ^ (i - (j + 1)) • x
    rw [← mul_smul, ← pow_add, Nat.add_sub_cancel' hlt, heq]
  · simp_rw [SubmonoidClass.coe_pow, OneMemClass.coe_one, mul_one, pow_succ]

Goal state after:
Module: Mathlib.RingTheory.Localization.Cardinality

Goal state before:
pp: R : Type u
inst✝ : CommRing R
S : Submonoid R
hS : S ≤ R⁰
⊢ #(Localization S) = #R

Tactic:
by
  apply OreLocalization.cardinalMk
  rwa [nonZeroDivisorsLeft_eq_nonZeroDivisors]

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

Goal state before:
pp: case refine_2.inr.inr.inl
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this : ∀ {a : Cardinal.{u}}, ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : c ≤ b
⊢ a ∣ b ∨ a ∣ c

Tactic:
solve_by_elim

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

Goal state before:
pp: case refine_1
n : ℕ
⊢ ¬IsUnit ↑n ↔ ¬IsUnit n

Tactic:
simp only [isUnit_iff, Nat.isUnit_iff]
    exact mod_cast Iff.rfl

Goal state after:
Module: Mathlib.FieldTheory.AxGrothendieck

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

pp: case inr
ι : Type u_1
α : Type u_2
inst✝¹ : Finite α
inst✝ : Finite ι
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
⊢ Theory.ACF 0 ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons

Tactic:
· exact ACF_models_genericPolyMapSurjOnOfInjOn_of_prime hp φ mons

Goal state after:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : Finite α
inst✝ : Finite ι
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
⊢ Theory.ACF 0 ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons
Module: Mathlib.FieldTheory.AxGrothendieck

Goal state before:
pp: K : Type u_1
ι : Type u_2
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : Finite ι
I : Ideal (MvPolynomial ι K)
p : ι → MvPolynomial ι K
this : CompatibleRing K := compatibleRingOfRing K
S : Set (ι → K) := zeroLocus K I
⊢ Set.MapsTo (fun v i ↦ (eval v) (p i)) S S →
    Set.InjOn (fun v i ↦ (eval v) (p i)) S → Set.SurjOn (fun v i ↦ (eval v) (p i)) S S

Tactic:
obtain ⟨s, rfl⟩ : I.FG := IsNoetherian.noetherian I

Goal state after:
K : Type u_1
ι : Type u_2
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : Finite ι
p : ι → MvPolynomial ι K
this : CompatibleRing K := compatibleRingOfRing K
s : Finset (MvPolynomial ι K)
S : Set (ι → K) := zeroLocus K (Ideal.span ↑s)
⊢ Set.MapsTo (fun v i ↦ (eval v) (p i)) S S →
    Set.InjOn (fun v i ↦ (eval v) (p i)) S → Set.SurjOn (fun v i ↦ (eval v) (p i)) S S
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
g : Gal(Extension k p n/k)
⊢ ∃ i < n, frob k p n ^ i = g

Tactic:
let := Fintype.ofFinite k
  obtain ⟨⟨i, hi⟩, rfl⟩ := (FiniteField.bijective_frobeniusAlgEquivOfAlgebraic_pow k
    (Extension k p n)).2 g
  refine ⟨i, ?_, by ext; simp [frob]⟩
  rwa [finrank_extension] at hi

Goal state after:
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
⊢ Nonempty (l ≃ₐ[k] Extension k p n)

Tactic:
have : Fintype l := .ofFinite _

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
⊢ Nonempty (l ≃ₐ[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 : σ
⊢ ∑ x, (Fintype.card K - 1) * Multiset.count n {x} = ?m.62

pp: K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ ?m.62 = Fintype.card K - 1

pp: K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ ℕ

Tactic:
· refine Finset.sum_eq_single n ?_ ?_
    · intro b _ ne
      simp [ne, eqComm]
    · intro h; exact (h <| Finset.mem_univ _).elim

Goal state after:
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
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, adjoin F (⇑b ∘ φ '' Iio i) = ⊤

Tactic:
adjoin_image_leastExt,

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, adjoin F (⇑b '' Iio (φ i)) = ⊤
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 : WithTop (Module.rank F E).ord.ToType
hi✝ : IsSuccPrelimit i
hi : ¬Nonempty ↑(Iio i)
⊢ filtration i = ⊥

Tactic:
by
  cases i
  · have := mk_ne_zero_iff.mp (rank_pos.trans_eq (mk_ord_toType <| Module.rank F E).symm).ne'
    rw [← range_coe] at hi; exact (hi inferInstance).elim
  · exact bot_unique <| adjoin_le_iff.mpr fun _ ⟨j, hj, _⟩ ↦ (hi ⟨j, coe_lt_coe.mpr hj⟩).elim

Goal state after:
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
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : WithTop (Module.rank F E).ord.ToType
hi : IsSuccPrelimit i
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h : ¬Nonempty ↑(Iio i)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [((equivOfEq (eq_bot_of_not_nonempty hi h)).trans <| botEquiv F E).forall_congr_left]

Goal state after:
case neg
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 : WithTop (Module.rank F E).ord.ToType
hi : IsSuccPrelimit i
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h : ¬Nonempty ↑(Iio i)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
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
⊢ #(Emb F E) = Module.rank F E

Tactic:
← Module.finrank_eq_rank,

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
⊢ #(Emb F E) = ↑(finrank F E)
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : ℕ
⊢ pNilradical R p ≤ nilradical R

Tactic:
by_cases hp : 1 < p
  · rw [pNilradical, if_pos hp]
  simp_rw [pNilradical, if_neg hp, bot_le]

Goal state after:
Module: Mathlib.FieldTheory.Galois.Profinite

Goal state before:
pp: case h.left
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)
L' : IntermediateField k ↥L
left✝ : FiniteDimensional k ↥L'
hO : ↑L'.fixingSubgroup ⊆ N
this✝ : Module.Finite k ↥(IntermediateField.lift L')
x : Gal(K/k)
hx : ∀ x_1 ∈ IntermediateField.lift L', x x_1 = x_1
y : ↥L
hy : y ∈ L'
this : (algebraMap (↥L) K) ((x.restrictNormal ↥L) y) = x ((algebraMap (↥L) K) y)
⊢ ((AlgEquiv.restrictNormalHom ↥L) x) y = y

Tactic:
dsimp at this

Goal state after:
case h.left
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)
L' : IntermediateField k ↥L
left✝ : FiniteDimensional k ↥L'
hO : ↑L'.fixingSubgroup ⊆ N
this✝ : Module.Finite k ↥(IntermediateField.lift L')
x : Gal(K/k)
hx : ∀ x_1 ∈ IntermediateField.lift L', x x_1 = x_1
y : ↥L
hy : y ∈ L'
this : ↑((x.restrictNormal ↥L) y) = x ↑y
⊢ ((AlgEquiv.restrictNormalHom ↥L) x) y = y