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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
p : α → Prop
h : ∀ᵐ (a : α) ∂μ, p a
⊢ ∀ᵐ (a : α) ∂ν, μ.rnDeriv ν a ≠ 0 → p a

Tactic:
rw [ν.haveLebesgueDecomposition_add μ, ae_add_measure_iff]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
p : α → Prop
h : ∀ᵐ (a : α) ∂μ, p a
⊢ (∀ᵐ (x : α) ∂ν.singularPart μ, μ.rnDeriv (ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)) x ≠ 0 → p x) ∧
    ∀ᵐ (x : α) ∂μ.withDensity (ν.rnDeriv μ), μ.rnDeriv (ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)) x ≠ 0 → p x
Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
⊢ coverEntropy T (φ '' F) ≤ coverEntropy (MapsTo.restrict S G G hG) (val ⁻¹' F)

Tactic:
have hφ : Semiconj (G.domRestrict φ) (hG.restrict S G G) T := by
    intro x
    rw [G.domRestrict_apply, G.domRestrict_apply, hG.val_restrict_apply, h.eq x]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
hφ : Semiconj (G.domRestrict φ) (MapsTo.restrict S G G hG) T
⊢ coverEntropy T (φ '' F) ≤ coverEntropy (MapsTo.restrict S G G hG) (val ⁻¹' F)
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

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

Tactic:
obtain ⟨h_meas, h_sing, hμν⟩ := Measure.haveLebesgueDecomposition_spec μ ν

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite κ
hνκ : ν ≪ κ
h_meas : Measurable (μ.rnDeriv ν)
h_sing : μ.singularPart ν ⟂ₘ ν
hμν : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
⊢ μ.rnDeriv ν * ν.rnDeriv κ =ᵐ[ν] μ.rnDeriv κ
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: case a
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ coverEntropyEntourage T F U ≤ ⨆ U ∈ 𝓤 X, netEntropyEntourage T F U

Tactic:
obtain ⟨V, V_uni, V_symm, V_comp_U⟩ := comp_symm_mem_uniformity_sets U_uni
    apply (coverEntropyEntourage_antitone T F V_comp_U).trans (le_iSup₂_of_le V V_uni _)
    have := isRefl_of_mem_uniformity V_uni
    exact coverEntropyEntourage_le_netEntropyEntourage T F

Goal state after:
Module: Mathlib.Dynamics.TopologicalEntropy.Subset

Goal state before:
pp: case inl
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
hF : coverMincard T F U n = ⊤
⊢ coverMincard T (F ∪ G) U n ≤ ⊤ + coverMincard T G U n

Tactic:
top_add

Goal state after:
case inl
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
hF : coverMincard T F U n = ⊤
⊢ coverMincard T (F ∪ G) U n ≤ ⊤
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (X ^ n - 1)).Splits
⊢ Group.IsSolvable (X ^ n - C a).Gal

Tactic:
by_cases ha : a = 0
  · rw [ha, C_0, sub_zero]
    exact gal_X_pow_isSolvable n
  have ha' : algebraMap F (X ^ n - C a).SplittingField a ≠ 0 :=
    mt ((injective_iff_map_eq_zero _).mp (RingHom.injective _) a) ha
  by_cases hn : n = 0
  · rw [hn, pow_zero, ← C_1, ← C_sub]
    exact gal_C_isSolvable (1 - a)
  have hn' : 0 < n := pos_iff_ne_zero.mpr hn
  have hn'' : X ^ n - C a ≠ 0 := X_pow_sub_C_ne_zero hn' a
  have hn''' : (X ^ n - 1 : F[X]) ≠ 0 := X_pow_sub_C_ne_zero hn' 1
  have mem_range : ∀ {c : (X ^ n - C a).SplittingField},
      (c ^ n = 1 → (∃ d, algebraMap F (X ^ n - C a).SplittingField d = c)) := fun {c} hc =>
    RingHom.mem_range.mp (minpoly.mem_range_of_degree_eq_one F c
      (Splits.degree_eq_one_of_irreducible (h.of_dvd (map_ne_zero hn''')
        (minpoly.dvd F c (by rwa [map_id, map_sub, sub_eq_zero, aeval_X_pow, aeval_one])))
          (minpoly.irreducible ((SplittingField.instNormal (X ^ n - C a)).isIntegral c))))
  apply Group.isSolvable_of_comm
  intro σ τ
  ext b hb
  rw [mem_rootSet_of_ne hn'', map_sub, aeval_X_pow, aeval_C, sub_eq_zero] at hb
  have hb' : b ≠ 0 := by
    intro hb'
    rw [hb', zero_pow hn] at hb
    exact ha' hb.symm
  have key : ∀ σ : (X ^ n - C a).Gal, ∃ c, σ b = b * algebraMap F _ c := by
    intro σ
    have key : (σ b / b) ^ n = 1 := by rw [div_pow, ← map_pow, hb, σ.commutes, div_self ha']
    obtain ⟨c, hc⟩ := mem_range key
    use c
    rw [hc, mul_div_cancel₀ (σ b) hb']
  obtain ⟨c, hc⟩ := key σ
  obtain ⟨d, hd⟩ := key τ
  rw [σ.mul_apply, τ.mul_apply, hc, map_mul, τ.commutes, hd, map_mul, σ.commutes, hc,
    mul_assoc, mul_assoc, mul_right_inj' hb', mul_comm]

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.Classification

Goal state before:
pp: K : Type u
L : Type v
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
t : Set L
ht : IsTranscendenceBasis ℤ Subtype.val
⊢ ℵ₀ < #L

Tactic:
rwa [← aleph0_lt_lift.{v, u}, ← lift_mk_eq'.2 hKL, aleph0_lt_lift]

Goal state after:
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: case mk.mk
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
toFun✝¹ : M → N
map_fun'✝¹ : ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toFun✝¹ (funMap f x) = funMap f (toFun✝¹ ∘ x)
map_rel'✝¹ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r x → RelMap r (toFun✝¹ ∘ x)
toFun✝ : M → N
map_fun'✝ : ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toFun✝ (funMap f x) = funMap f (toFun✝ ∘ x)
map_rel'✝ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r x → RelMap r (toFun✝ ∘ x)
h :
  { toFun := toFun✝¹, map_fun' := map_fun'✝¹, map_rel' := map_rel'✝¹ }.toFun =
    { toFun := toFun✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ }.toFun
⊢ { toFun := toFun✝¹, map_fun' := map_fun'✝¹, map_rel' := map_rel'✝¹ } =
    { toFun := toFun✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ }

Tactic:
cases h

Goal state after:
case mk.mk.refl
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
toFun✝ : M → N
map_fun'✝¹ : ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toFun✝ (funMap f x) = funMap f (toFun✝ ∘ x)
map_rel'✝¹ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r x → RelMap r (toFun✝ ∘ x)
map_fun'✝ : ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toFun✝ (funMap f x) = funMap f (toFun✝ ∘ x)
map_rel'✝ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r x → RelMap r (toFun✝ ∘ x)
⊢ { toFun := toFun✝, map_fun' := map_fun'✝¹, map_rel' := map_rel'✝¹ } =
    { toFun := toFun✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ }
Module: Mathlib.FieldTheory.IsAlgClosed.Classification

Goal state before:
pp: K : Type u
L : Type v
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : IsAlgClosed K
inst✝³ : IsAlgClosed L
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
this✝ : Algebra (ZMod p) K := ZMod.algebra K p
this : Algebra (ZMod p) L := ZMod.algebra L p
s : Set K
hs : IsTranscendenceBasis (ZMod p) Subtype.val
t : Set L
ht : IsTranscendenceBasis (ZMod p) Subtype.val
⊢ ℵ₀ < #L

Tactic:
rwa [← aleph0_lt_lift.{v, u}, ← lift_mk_eq'.2 hKL, aleph0_lt_lift]

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
a₁✝ a₂✝ : M ≃[L] N
h : a₁✝.toEmbedding = a₂✝.toEmbedding
⊢ ⇑a₁✝ = ⇑a₂✝

Tactic:
exact congr_arg (DFunLike.coe ∘ Embedding.toHom) h

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case var
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
γ : Type u_4
xs : β ⊕ γ → M
xs' : α → M
a : α ⊕ γ
f : ↥(var a).varFinsetLeft → β
hxs' : ∀ (a_1 : ↥(var a).varFinsetLeft), xs (Sum.inl (f a_1)) = xs' ↑a_1
⊢ realize xs ((var a).restrictVarLeft f) = realize (Sum.elim xs' (xs ∘ Sum.inr)) (var a)

Tactic:
cases a <;> simp [restrictVarLeft, hxs']

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case func
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
F : Type u_4
inst✝¹ : FunLike F M N
inst✝ : L.HomClass F M N
g : F
v : α → M
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
_ts_ih✝ : ∀ (a : Fin l✝), Term.realize (⇑g ∘ v) (_ts✝ a) = g (Term.realize v (_ts✝ a))
⊢ Term.realize (⇑g ∘ v) (func _f✝ _ts✝) = g (Term.realize v (func _f✝ _ts✝))

Tactic:
Term.realize,

Goal state after:
case func
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
F : Type u_4
inst✝¹ : FunLike F M N
inst✝ : L.HomClass F M N
g : F
v : α → M
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
_ts_ih✝ : ∀ (a : Fin l✝), Term.realize (⇑g ∘ v) (_ts✝ a) = g (Term.realize v (_ts✝ a))
⊢ (funMap _f✝ fun i ↦ Term.realize (⇑g ∘ v) (_ts✝ i)) = g (Term.realize v (func _f✝ _ts✝))
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case func
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
F : Type u_4
inst✝¹ : FunLike F M N
inst✝ : L.HomClass F M N
g : F
v : α → M
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
_ts_ih✝ : ∀ (a : Fin l✝), Term.realize (⇑g ∘ v) (_ts✝ a) = g (Term.realize v (_ts✝ a))
⊢ (funMap _f✝ fun i ↦ Term.realize (⇑g ∘ v) (_ts✝ i)) = g (Term.realize v (func _f✝ _ts✝))

Tactic:
Term.realize,

Goal state after:
case func
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
F : Type u_4
inst✝¹ : FunLike F M N
inst✝ : L.HomClass F M N
g : F
v : α → M
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
_ts_ih✝ : ∀ (a : Fin l✝), Term.realize (⇑g ∘ v) (_ts✝ a) = g (Term.realize v (_ts✝ a))
⊢ (funMap _f✝ fun i ↦ Term.realize (⇑g ∘ v) (_ts✝ i)) = g (funMap _f✝ fun i ↦ Term.realize v (_ts✝ i))
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → L.Structure (M a)
β : Type u_3
x : β → (a : α) → M a
t : L.Term β
⊢ Term.realize (fun i ↦ Quotient.mk' (x i)) t = Quotient.mk' fun a ↦ Term.realize (fun i ↦ x i a) t

Tactic:
convert!
    @Term.realize_quotient_mk' L _ ((u : Filter α).productSetoid M)
      (Ultraproduct.setoidPrestructure M u) _ t x using 2

Goal state after:
case e'_3.e'_3
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → L.Structure (M a)
β : Type u_3
x : β → (a : α) → M a
t : L.Term β
⊢ (fun a ↦ Term.realize (fun i ↦ x i a) t) = Term.realize x t
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
φ ψ : L.BoundedFormula α l
v : α → M
xs : Fin l → M
⊢ (∼φ ⟹ ψ).Realize v xs ↔ φ.Realize v xs ∨ ψ.Realize v xs

Tactic:
tauto

Goal state after:
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: case equal
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → L.Structure (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
n✝ : ℕ
t₁✝ t₂✝ : L.Term (β ⊕ Fin n✝)
v : Fin n✝ → (a : α) → M a
h2 : ∀ (a : α), (Sum.elim (fun i ↦ x i a) fun i ↦ v i a) = fun i ↦ Sum.elim x v i a
⊢ Term.realize (Sum.elim (fun i ↦ Quotient.mk' (x i)) fun i ↦ Quotient.mk' (v i)) t₁✝ =
      Term.realize (Sum.elim (fun i ↦ Quotient.mk' (x i)) fun i ↦ Quotient.mk' (v i)) t₂✝ ↔
    ∀ᶠ (a : α) in ↑u, Term.realize (fun i ↦ Sum.elim x v i a) t₁✝ = Term.realize (fun i ↦ Sum.elim x v i a) t₂✝

Tactic:
(Sum.comp_elim ((↑) : (∀ a, M a) → (u : Filter α).Product M) x v).symm,

Goal state after:
case equal
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → L.Structure (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
n✝ : ℕ
t₁✝ t₂✝ : L.Term (β ⊕ Fin n✝)
v : Fin n✝ → (a : α) → M a
h2 : ∀ (a : α), (Sum.elim (fun i ↦ x i a) fun i ↦ v i a) = fun i ↦ Sum.elim x v i a
⊢ Term.realize (Quotient.mk' ∘ Sum.elim x v) t₁✝ = Term.realize (Quotient.mk' ∘ Sum.elim x v) t₂✝ ↔
    ∀ᶠ (a : α) in ↑u, Term.realize (fun i ↦ Sum.elim x v i a) t₁✝ = Term.realize (fun i ↦ Sum.elim x v i a) t₂✝
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: L : Language
α : Type u'
n : ℕ
R : L.Relations n
k : ℕ
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
h : ∀ (i : Fin n), (List.map Sum.getLeft? l)[i]?.join.isSome = true
h' : ∀ (i : Fin n), ((List.map Sum.getLeft? l)[i]?.join.get ⋯).fst = k
i : Fin n
⊢ L.Term (α ⊕ Fin ((List.map Sum.getLeft? l)[i]?.join.get ⋯).fst) = L.Term (α ⊕ Fin k)

Tactic:
h' i

Goal state after:
L : Language
α : Type u'
n : ℕ
R : L.Relations n
k : ℕ
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
h : ∀ (i : Fin n), (List.map Sum.getLeft? l)[i]?.join.isSome = true
h' : ∀ (i : Fin n), ((List.map Sum.getLeft? l)[i]?.join.get ⋯).fst = k
i : Fin n
⊢ L.Term (α ⊕ Fin k) = L.Term (α ⊕ Fin k)
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 (x ∘ natAdd n) ↔ BoundedFormula.Realize φ x default

Tactic:
Subsingleton.elim (x ∘ (natAdd n : Fin 0 → Fin n)) default

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 default ↔ BoundedFormula.Realize φ x default
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: case succ
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝³ : L.Structure M
inst✝² : L.Structure N
inst✝¹ : L.Structure P
S : L.Substructure M
s : Set M
inst✝ : IsEmpty L.Constants
x : M
n✝ : ℕ
f : L.Functions (n✝ + 1)
⊢ ClosedUnder f ∅

Tactic:
· intro x hx
      simp only [mem_empty_iff_false, forall_const] at hx

Goal state after:
Module: Mathlib.ModelTheory.ElementarySubstructures

Goal state before:
pp: 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
hD : A.Definable₁ L D
b : M
hbD : b ∈ D
hbA : b ∈ A
⊢ ∃ b, φ.Realize default (Fin.snoc (Subtype.val ∘ x) ↑b)

Tactic:
exact ⟨⟨b, by rwa [← hA.closure_eq_self] at hbA⟩, hbD⟩

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type u_1
L : Language
inst✝ : L.Structure M
A : Set M
a : M
γ : Type u_4
ha : a ∈ A
⊢ DefinableFun L A fun x ↦ a

Tactic:
rw [definableFun_iff_empty_definableFun_with_params]

Goal state after:
M : Type u_1
L : Language
inst✝ : L.Structure M
A : Set M
a : M
γ : Type u_4
ha : a ∈ A
⊢ DefinableFun L[[↑A]] ∅ fun x ↦ a
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ Directed (fun x1 x2 ↦ x1 ⊆ x2) fun i ↦
    (L.lhomWithConstants α).onTheory T ∪
      L.distinctConstantsTheory ↑(Finset.map (Function.Embedding.subtype fun x ↦ x ∈ s) i)

Tactic:
· apply Monotone.directed_le
    refine monotone_const.union (monotone_distinctConstantsTheory.comp ?_)
    simp only [Finset.coe_map, Function.Embedding.coe_subtype]
    exact Monotone.comp (g := Set.image ((↑) : s → α)) (f := ((↑) : Finset s → Set s))
      Set.monotone_image fun _ _ => Finset.coe_subset.2

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case refine_1
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : T ⊨ᵇ φ
M : ((L.lhomWithConstants α).onTheory T).ModelType
this : L.Structure ↑M := (L.lhomWithConstants α).reduct ↑M
⊢ φ.Realize fun a ↦ ↑(L.con a)

Tactic:
have : M ⊨ T := (LHom.onTheory_model _ _).1 M.is_model

Goal state after:
case refine_1
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : T ⊨ᵇ φ
M : ((L.lhomWithConstants α).onTheory T).ModelType
this✝ : L.Structure ↑M := (L.lhomWithConstants α).reduct ↑M
this : ↑M ⊨ T
⊢ φ.Realize fun a ↦ ↑(L.con a)
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'
⊢ ∀ (v : α → ↑M) (xs : Fin 0 → ↑M), BoundedFormula.Realize φ v xs

Tactic:
let M' : ModelType T' := ⟨M⟩

Goal state after:
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
Module: Mathlib.FieldTheory.AxGrothendieck

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝³ : Finite α
K : Type u_3
inst✝² : Field K
inst✝¹ : CompatibleRing K
inst✝ : Finite ι
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
⊢ ∀ {S : Set (ι → K)} (f : (ι → K) → ι → K),
    (∀ ⦃x₁ : ι → K⦄, x₁ ∈ S → ∀ ⦃x₂ : ι → K⦄, x₂ ∈ S → f x₁ = f x₂ → x₁ = x₂) ↔
      ∀ (x y : ι → K), x ∈ S → y ∈ S → f x = f y → x = y

Tactic:
tauto

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

Goal state before:
pp: a : Cardinal.{u}
ha : ℵ₀ ≤ a
⊢ ¬Irreducible a

Tactic:
irreducible_iff,

Goal state after:
a : Cardinal.{u}
ha : ℵ₀ ≤ a
⊢ ¬(¬IsUnit a ∧ ∀ ⦃a_1 b : Cardinal.{u}⦄, a = a_1 * b → IsUnit a_1 ∨ IsUnit b)
Module: Mathlib.FieldTheory.AxGrothendieck

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

Tactic:
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.SetTheory.Cardinal.Divisibility

Goal state before:
pp: case neg
a : ℕ
h : ¬ℵ₀ ≤ ↑a
⊢ IsPrimePow ↑a ↔ ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Tactic:
isPrimePow_def

Goal state after:
case neg
a : ℕ
h : ¬ℵ₀ ≤ ↑a
⊢ (∃ p k, Prime p ∧ 0 < k ∧ p ^ k = ↑a) ↔ ∃ n, ↑a = ↑n ∧ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
Module: Mathlib.FieldTheory.Differential.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
a : R
h : a′ = 0
⊢ logDeriv a = 0

Tactic:
by unfold logDeriv at *; simp [h]

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

Goal state before:
pp: case hl
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]
this : 0 < p.natDegree
⊢ (derivative p).natDegree < p.natDegree

Tactic:
apply natDegree_derivative_lt

Goal state after:
case hl
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]
this : 0 < p.natDegree
⊢ p.natDegree ≠ 0
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
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
default : { _a // DifferentialAlgebra F K } := ⟨differentialFiniteDimensional F K, ⋯⟩
x✝ : { _a // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
| (fun x_1 ↦ (aeval x) (mapCoeffs (minpoly F x)) + (aeval x) (derivative (minpoly F x)) * x_1) x′

Tactic:
apply (deriv_aeval_eq ..).symm

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

Goal state before:
pp: case hl
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
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
default : { _a // DifferentialAlgebra F K } := ⋯
x✝ : { _a // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
this : 0 < (minpoly F x).natDegree
⊢ (derivative (minpoly F x)).natDegree < (minpoly F x).natDegree

Tactic:
apply natDegree_derivative_lt

Goal state after:
case hl
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
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
default : { _a // DifferentialAlgebra F K } := ⋯
x✝ : { _a // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
this : 0 < (minpoly F x).natDegree
⊢ (minpoly F x).natDegree ≠ 0
Module: Mathlib.FieldTheory.Galois.NormalBasis

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Infinite K
e : Module.Basis (Module.Free.ChooseBasisIndex K L) K L
M : Matrix Gal(L/K) Gal(L/K) (MvPolynomial (Module.Free.ChooseBasisIndex K L) L) :=
  Matrix.of fun i j ↦ ∑ k, i.symm (j (e k)) • MvPolynomial.X k
hq : Submodule.span L (Set.range fun k j ↦ j (e k)) = ⊤
c : Module.Free.ChooseBasisIndex K L → L
hc : (MvPolynomial.eval c) M.det = 1
hM : M.det ≠ 0
b : Module.Free.ChooseBasisIndex K L → K
hb : (M.map ⇑(MvPolynomial.eval (⇑(algebraMap K L) ∘ b))).det ≠ 0
a : Gal(L/K) → K
ha : ∑ i, a i • i (∑ k, b k • e k) = 0
i : Gal(L/K)
⊢ i ((M.map ⇑(MvPolynomial.eval (⇑(algebraMap K L) ∘ b))).mulVec (fun x ↦ (algebraMap K L) (a x)) i) = i (0 i)

Tactic:
simp_rw [M, Pi.zero_apply, map_zero, ← ha]

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Infinite K
e : Module.Basis (Module.Free.ChooseBasisIndex K L) K L
M : Matrix Gal(L/K) Gal(L/K) (MvPolynomial (Module.Free.ChooseBasisIndex K L) L) :=
  Matrix.of fun i j ↦ ∑ k, i.symm (j (e k)) • MvPolynomial.X k
hq : Submodule.span L (Set.range fun k j ↦ j (e k)) = ⊤
c : Module.Free.ChooseBasisIndex K L → L
hc : (MvPolynomial.eval c) M.det = 1
hM : M.det ≠ 0
b : Module.Free.ChooseBasisIndex K L → K
hb : (M.map ⇑(MvPolynomial.eval (⇑(algebraMap K L) ∘ b))).det ≠ 0
a : Gal(L/K) → K
ha : ∑ i, a i • i (∑ k, b k • e k) = 0
i : Gal(L/K)
⊢ i
      (((Matrix.of fun i j ↦ ∑ k, i.symm (j (e k)) • MvPolynomial.X k).map
            ⇑(MvPolynomial.eval (⇑(algebraMap K L) ∘ b))).mulVec
        (fun x ↦ (algebraMap K L) (a x)) i) =
    ∑ i, a i • i (∑ k, b k • e k)
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
f : ↑(limit (embFunctor F E) i)
j : ↑(Iio i)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
have := Nonempty.intro j

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 : WithTop (Module.rank F E).ord.ToType
hi : IsSuccPrelimit i
f : ↑(limit (embFunctor F E) i)
j : ↑(Iio i)
this : Nonempty ↑(Iio i)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)