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

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
F_inv : MapsTo T F F
inst✝ : U.IsSymm
n_pos : n ≠ 0
s : Finset X
h : IsDynCoverOf T F U n ↑s
⊢ coverEntropyEntourage T F (U ○ U) ≤ (↑(#s)).log / ↑n

Tactic:
apply (coverEntropyEntourage_le_log_coverMincard_div F_inv n_pos).trans
  apply monotone_div_right_of_nonneg n.cast_nonneg' (log_monotone _)
  exact_mod_cast coverMincard_le_card h

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

Goal state before:
pp: G : Type u_3
inst✝⁶ : Group G
mG : MeasurableSpace G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ : Measure G
inst✝³ : μ.IsMulLeftInvariant
inst✝² : SFinite μ
ν₁ ν₂ : Measure G
inst✝¹ : ν₁.HaveLebesgueDecomposition μ
inst✝ : ν₂.HaveLebesgueDecomposition μ
hν₁ : ν₁ ≪ μ
hν₂ : ν₂ ≪ μ
⊢ ν₁ ∗ₘ ν₂ = μ.withDensity (ν₁.rnDeriv μ ⋆ₘₗ[μ] ν₂.rnDeriv μ)

Tactic:
← mconv_withDensity_eq_mlconvolution (by fun_prop) (by fun_prop),

Goal state after:
G : Type u_3
inst✝⁶ : Group G
mG : MeasurableSpace G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ : Measure G
inst✝³ : μ.IsMulLeftInvariant
inst✝² : SFinite μ
ν₁ ν₂ : Measure G
inst✝¹ : ν₁.HaveLebesgueDecomposition μ
inst✝ : ν₂.HaveLebesgueDecomposition μ
hν₁ : ν₁ ≪ μ
hν₂ : ν₂ ≪ μ
⊢ ν₁ ∗ₘ ν₂ = μ.withDensity (ν₁.rnDeriv μ) ∗ₘ μ.withDensity (ν₂.rnDeriv μ)
Module: Mathlib.FieldTheory.IsAlgClosed.Classification

Goal state before:
pp: R : Type u
K : Type v
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsAlgClosed K
ι : Type w
v : ι → K
hv : IsTranscendenceBasis R v
⊢ max (Cardinal.lift.{max v u w, max u w} #(MvPolynomial ι R)) ℵ₀ =
    Cardinal.lift.{v, max u w} (max #(MvPolynomial ι R) ℵ₀)

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

Goal state after:
R : Type u
K : Type v
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsAlgClosed K
ι : Type w
v : ι → K
hv : IsTranscendenceBasis R v
⊢ max (Cardinal.lift.{max v u w, max u w} #(MvPolynomial ι R)) (Cardinal.lift.{max u v w, max u w} ℵ₀) =
    Cardinal.lift.{v, max u w} (max #(MvPolynomial ι R) ℵ₀)
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: L : Language
L' : Language
ϕ : L →ᴸ L'
inst✝³ : (n : ℕ) → (f : L'.Functions n) → Decidable (f ∈ Set.range fun f ↦ ϕ.onFunction f)
inst✝² : (n : ℕ) → (r : L'.Relations n) → Decidable (r ∈ Set.range fun r ↦ ϕ.onRelation r)
h : ϕ.Injective
M : Type u_1
inst✝¹ : Inhabited M
inst✝ : L.Structure M
this : L'.Structure M := ϕ.defaultExpansion M
⊢ ϕ.IsExpansionOn M

Tactic:
refine ⟨fun {n} f xs => ?_, fun {n} r xs => ?_⟩

Goal state after:
case refine_1
L : Language
L' : Language
ϕ : L →ᴸ L'
inst✝³ : (n : ℕ) → (f : L'.Functions n) → Decidable (f ∈ Set.range fun f ↦ ϕ.onFunction f)
inst✝² : (n : ℕ) → (r : L'.Relations n) → Decidable (r ∈ Set.range fun r ↦ ϕ.onRelation r)
h : ϕ.Injective
M : Type u_1
inst✝¹ : Inhabited M
inst✝ : L.Structure M
this : L'.Structure M := ϕ.defaultExpansion M
n : ℕ
f : L.Functions n
xs : Fin n → M
⊢ funMap (ϕ.onFunction f) xs = funMap f xs

case refine_2
L : Language
L' : Language
ϕ : L →ᴸ L'
inst✝³ : (n : ℕ) → (f : L'.Functions n) → Decidable (f ∈ Set.range fun f ↦ ϕ.onFunction f)
inst✝² : (n : ℕ) → (r : L'.Relations n) → Decidable (r ∈ Set.range fun r ↦ ϕ.onRelation r)
h : ϕ.Injective
M : Type u_1
inst✝¹ : Inhabited M
inst✝ : L.Structure M
this : L'.Structure M := ϕ.defaultExpansion M
n : ℕ
r : L.Relations n
xs : Fin n → M
⊢ RelMap (ϕ.onRelation r) xs = RelMap r xs
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
motive : (x : E) → x ∈ solvableByRad F E → Prop
mem : ∀ (x : F), motive ((algebraMap F E) x) ⋯
add :
  ∀ (x y : E) (hx : x ∈ solvableByRad F E) (hy : y ∈ solvableByRad F E), motive x hx → motive y hy → motive (x + y) ⋯
mul :
  ∀ (x y : E) (hx : x ∈ solvableByRad F E) (hy : y ∈ solvableByRad F E), motive x hx → motive y hy → motive (x * y) ⋯
rad : ∀ (n : ℕ) (x : E) (hn : n ≠ 0) (hx : x ^ n ∈ solvableByRad F E), motive (x ^ n) hx → motive x ⋯
x : E
hx : x ∈ solvableByRad F E
⊢ motive x hx

Tactic:
by
  let s : Subalgebra F E :=
  { carrier := {x | ∃ hx : x ∈ solvableByRad F E, motive x hx}
    algebraMap_mem' a := ⟨algebraMap_mem _ a, mem a⟩
    add_mem' := fun ⟨ha, ha'⟩ ⟨hb, hb'⟩ ↦ ⟨add_mem ha hb, add _ _ ha hb ha' hb'⟩
    mul_mem' := fun ⟨ha, ha'⟩ ⟨hb, hb'⟩ ↦ ⟨mul_mem ha hb, mul _ _ ha hb ha' hb'⟩ }
  let t : IntermediateField F E := Subalgebra.IsAlgebraic.toIntermediateField (S := s) <| by
    rintro x ⟨hx, hx'⟩
    apply isAlgebraic_solvableByRad
    exact hx
  have ht (x n) (hn : n ≠ 0) : x ^ n ∈ t → x ∈ t := by
    rintro ⟨hx, hx'⟩
    exact ⟨rad_mem hn hx, rad _ _ hn hx hx'⟩
  obtain ⟨_, h⟩ := solvableByRad_le (s := t) ht hx
  exact h

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (x : ring.Symbols),
    x ∈
      { val := ↑[Sum.inl ⟨2, add⟩, Sum.inl ⟨2, mul⟩, Sum.inl ⟨1, neg⟩, Sum.inl ⟨0, zero⟩, Sum.inl ⟨0, one⟩],
        nodup := instFintypeSymbolsRing._proof_1 }

Tactic:
intro x
    dsimp [Language.Symbols]
    rcases x with ⟨_, f⟩ | ⟨_, f⟩
    · cases f <;> decide
    · cases f

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

Goal state before:
pp: α : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : NonAssocRing R
inst✝² : NonAssocRing S
inst✝¹ : CompatibleRing R
inst✝ : CompatibleRing S
f : R ≃[ring] S
⊢ ∀ (x y : R), f.toFun (x * y) = f.toFun x * f.toFun y

Tactic:
by
        intro x y
        simpa using! f.map_fun mulFunc ![x, y]

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case func
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n : ℕ
f : L[[γ]].Functions n
_ts✝ : Fin n → L[[γ]].Term α
ih : ∀ (a : Fin n), (_ts✝ a).constantsToVars.varsToConstants = _ts✝ a
⊢ (func f _ts✝).constantsToVars.varsToConstants = func f _ts✝

Tactic:
cases n

Goal state after:
case func.zero
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
f : L[[γ]].Functions 0
_ts✝ : Fin 0 → L[[γ]].Term α
ih : ∀ (a : Fin 0), (_ts✝ a).constantsToVars.varsToConstants = _ts✝ a
⊢ (func f _ts✝).constantsToVars.varsToConstants = func f _ts✝

case func.succ
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n✝ : ℕ
f : L[[γ]].Functions (n✝ + 1)
_ts✝ : Fin (n✝ + 1) → L[[γ]].Term α
ih : ∀ (a : Fin (n✝ + 1)), (_ts✝ a).constantsToVars.varsToConstants = _ts✝ a
⊢ (func f _ts✝).constantsToVars.varsToConstants = func f _ts✝
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case func
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n : ℕ
f : L.Functions n
_ts✝ : Fin n → L.Term (γ ⊕ α)
ih : ∀ (a : Fin n), (_ts✝ a).varsToConstants.constantsToVars = _ts✝ a
⊢ (func f _ts✝).varsToConstants.constantsToVars = func f _ts✝

Tactic:
cases n

Goal state after:
case func.zero
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
f : L.Functions 0
_ts✝ : Fin 0 → L.Term (γ ⊕ α)
ih : ∀ (a : Fin 0), (_ts✝ a).varsToConstants.constantsToVars = _ts✝ a
⊢ (func f _ts✝).varsToConstants.constantsToVars = func f _ts✝

case func.succ
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n✝ : ℕ
f : L.Functions (n✝ + 1)
_ts✝ : Fin (n✝ + 1) → L.Term (γ ⊕ α)
ih : ∀ (a : Fin (n✝ + 1)), (_ts✝ a).varsToConstants.constantsToVars = _ts✝ a
⊢ (func f _ts✝).varsToConstants.constantsToVars = func f _ts✝
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
α : Type u'
β : Type v'
n : ℕ
g : α → β ⊕ Fin n
k : ℕ
φ : L.BoundedFormula α (k + 1)
⊢ mapTermRel (fun x t ↦ Term.relabel (relabelAux g x) t) (fun x ↦ id) (fun x ↦ castLE ⋯) φ.all = (relabel g φ).all

Tactic:
mapTermRel,

Goal state after:
L : Language
α : Type u'
β : Type v'
n : ℕ
g : α → β ⊕ Fin n
k : ℕ
φ : L.BoundedFormula α (k + 1)
⊢ (castLE ⋯ (mapTermRel (fun x t ↦ Term.relabel (relabelAux g x) t) (fun x ↦ id) (fun x ↦ castLE ⋯) φ)).all =
    (relabel g φ).all
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

Goal state after:
case func.zero
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
f : L[[α]].Functions 0
ts : Fin 0 → L[[α]].Term β
ih : ∀ (a : Fin 0), 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)

case func.succ
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✝ + 1)
ts : Fin (n✝ + 1) → L[[α]].Term β
ih : ∀ (a : Fin (n✝ + 1)), 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)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case func.zero
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
f : L[[α]].Functions 0
ts : Fin 0 → L[[α]].Term β
ih : ∀ (a : Fin 0), 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)

pp: case func.succ
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✝ + 1)
ts : Fin (n✝ + 1) → L[[α]].Term β
ih : ∀ (a : Fin (n✝ + 1)), 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 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

Goal state after:
case func.succ
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✝ + 1)
ts : Fin (n✝ + 1) → L[[α]].Term β
ih : ∀ (a : Fin (n✝ + 1)), 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)
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)) = funMap _f✝ (⇑g ∘ fun i ↦ Term.realize v (_ts✝ i))

Tactic:
refine congr rfl ?_

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))
⊢ (fun i ↦ Term.realize (⇑g ∘ v) (_ts✝ i)) = ⇑g ∘ 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)
n : ℕ
f : L.Functions n
x y : Fin n → (a : α) → M a
xy : x ≈ y
a : α
ha : a ∈ ⋂ i, {x_1 | (fun a ↦ x i a = y i a) x_1}
⊢ a ∈ {x_1 | (fun a ↦ funMap f x a = funMap f y a) x_1}

Tactic:
simp only [Set.mem_iInter, Set.mem_ofPred_eq] at ha

Goal state after:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → L.Structure (M a)
n : ℕ
f : L.Functions n
x y : Fin n → (a : α) → M a
xy : x ≈ y
a : α
ha : ∀ (i : Fin n), x i a = y i a
⊢ a ∈ {x_1 | (fun a ↦ funMap f x a = funMap f y a) x_1}
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
L' : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : L'.Structure M
k : ℕ
ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin (k + n))
fr : (n : ℕ) → L.Relations n → L'.Relations n
n : ℕ
φ : L.BoundedFormula α n
v : {n : ℕ} → (Fin (k + n) → M) → α → M
v' : β → M
xs : Fin (k + n) → M
h1 :
  ∀ (n : ℕ) (t : L.Term (α ⊕ Fin n)) (xs' : Fin (k + n) → M),
    realize (Sum.elim v' xs') (ft n t) = realize (Sum.elim (v xs') (xs' ∘ natAdd k)) t
h2 : ∀ (n : ℕ) (R : L.Relations n) (x : Fin n → M), RelMap (fr n R) x = RelMap R x
hv : ∀ (n : ℕ) (xs : Fin (k + n) → M) (x : M), v (snoc xs x) = v xs
⊢ (mapTermRel ft fr (fun x ↦ castLE ⋯) φ).Realize v' xs ↔ φ.Realize (v xs) (xs ∘ natAdd k)

Tactic:
by
  induction φ with
  | falsum => rfl
  | equal => simp [mapTermRel, Realize, h1]
  | rel => simp [mapTermRel, Realize, h1, h2]
  | imp _ _ ih1 ih2 => simp [mapTermRel, Realize, ih1, ih2]
  | all _ ih => simp [mapTermRel, Realize, ih, hv]

Goal state after:
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)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
φ : L.Formula β
x : β → (a : α) → M a
⊢ BoundedFormula.Realize φ (fun i ↦ Quotient.mk' (x i)) default =
    BoundedFormula.Realize φ (fun i ↦ Quotient.mk' (x i)) fun i ↦ Quotient.mk' fun a ↦ default i

Tactic:
exact congr rfl (Subsingleton.elim _ _)

Goal state after:
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)
inst✝ : ∀ (a : α), Nonempty (M a)
φ : L.Sentence
⊢ Formula.Realize φ default = Formula.Realize φ fun i ↦ Quotient.mk' fun a ↦ default i

Tactic:
exact congr rfl (Subsingleton.elim _ _)

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case refine_1
L : Language
α : Type u'
⊢ ⨆ i, #(L.Term (α ⊕ Fin i)) ≠ 0

Tactic:
rw [← Cardinal.one_le_iff_ne_zero]

Goal state after:
case refine_1
L : Language
α : Type u'
⊢ 1 ≤ ⨆ i, #(L.Term (α ⊕ Fin i))
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
⊢ s ∈ (closure L).closed ↔ ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f s

Tactic:
refine ⟨fun h n f => ?_, fun h => ?_⟩

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

case refine_2
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
h : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f s
⊢ s ∈ (closure L).closed
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: 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
⊢ ClosedUnder f ∅

Tactic:
cases n

Goal state after:
case zero
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
f : L.Functions 0
⊢ ClosedUnder f ∅

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 ∅
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
φ : L.Formula α
⊢ M ⊨ equivSentence φ ↔ φ.Realize fun a ↦ ↑(L.con a)

Tactic:
← realize_equivSentence_symm_con M (equivSentence φ),

Goal state after:
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
φ : L.Formula α
⊢ ((equivSentence.symm (equivSentence φ)).Realize fun a ↦ ↑(L.con a)) ↔ φ.Realize fun a ↦ ↑(L.con a)
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: case inr
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✝ S : L.Substructure M
A : Set M
h : A ⊆ ↑S
n : ℕ
f : (constantsOn ↑A).Functions n
⊢ ClosedUnder (Sum.inr f) ↑S

Tactic:
cases n

Goal state after:
case inr.zero
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✝ S : L.Substructure M
A : Set M
h : A ⊆ ↑S
f : (constantsOn ↑A).Functions 0
⊢ ClosedUnder (Sum.inr f) ↑S

case inr.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✝ S : L.Substructure M
A : Set M
h : A ⊆ ↑S
n✝ : ℕ
f : (constantsOn ↑A).Functions (n✝ + 1)
⊢ ClosedUnder (Sum.inr f) ↑S
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
⊢ ∅ = ofPred ⊥.Realize

Tactic:
ext
    simp

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
⊢ univ = ofPred ⊤.Realize

Tactic:
ext
    simp

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
f g : Set (α → M)
φ : L[[↑A]].Formula α
hφ : f = ofPred φ.Realize
θ : L[[↑A]].Formula α
hθ : g = ofPred θ.Realize
⊢ A.Definable L (f ∪ g)

Tactic:
refine ⟨φ ⊔ θ, ?_⟩

Goal state after:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
f g : Set (α → M)
φ : L[[↑A]].Formula α
hφ : f = ofPred φ.Realize
θ : L[[↑A]].Formula α
hθ : g = ofPred θ.Realize
⊢ f ∪ g = ofPred (φ ⊔ θ).Realize
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝³ : L.Structure M
α : Type u'
inst✝² : DecidableEq α
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
φ : L.Formula α
h : M ⊨ equivSentence φ
⊢ M ⊨ φ.exClosure

Tactic:
rw [Formula.realize_exClosure]
  exists fun a => (L.con (a : α) : M)
  simpa [Formula.Realize, BoundedFormula.realize_restrictFreeVar] using h

Goal state after:
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)
a : α
as : a ∈ s
b : α
bs : b ∈ s
ab : (fun i ↦ ↑(L.con i)) a = (fun i ↦ ↑(L.con i)) b
⊢ ↑⟨a, as⟩ = b

Tactic:
← Subtype.coe_mk b bs,

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 : α
as : a ∈ s
b : α
bs : b ∈ s
ab : (fun i ↦ ↑(L.con i)) a = (fun i ↦ ↑(L.con i)) b
⊢ ↑⟨a, as⟩ = ↑⟨b, bs⟩
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
f : (α → M) → M
h : A.TermDefinable L f
⊢ A.Definable L (Function.tupleGraph f)

Tactic:
obtain ⟨φ, rfl⟩ := h
  use (φ.relabel some).equal (Term.var none)
  ext
  simp [Function.tupleGraph]

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
φ : L.Sentence
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
h : ¬M ⊨ φ
⊢ ¬M ⊨ φ ∧ ∀ a ∈ T, M ⊨ a

Tactic:
rw [← model_iff]

Goal state after:
L : Language
T : L.Theory
φ : L.Sentence
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
h : ¬M ⊨ φ
⊢ ¬M ⊨ φ ∧ M ⊨ T
Module: Mathlib.FieldTheory.Differential.Basic

Goal state before:
pp: R : Type u_1
inst✝⁶ : Field R
inst✝⁵ : Differential R
a b : R
F : Type u_2
inst✝⁴ : Field F
inst✝³ : Differential F
inst✝² : CharZero F
p : F[X]
inst✝¹ : Fact (Irreducible p)
inst✝ : Fact p.Monic
x : F[X]
hx : p ∣ x
⊢ p ∣
    (implicitDeriv
        ((AdjoinRoot.modByMonicHom ⋯)
          (-(aeval (AdjoinRoot.root p)) (mapCoeffs p) / (aeval (AdjoinRoot.root p)) (derivative p))))
      x

Tactic:
obtain ⟨q, rfl⟩ := hx

Goal state after:
R : Type u_1
inst✝⁶ : Field R
inst✝⁵ : Differential R
a b : R
F : Type u_2
inst✝⁴ : Field F
inst✝³ : Differential F
inst✝² : CharZero F
p : F[X]
inst✝¹ : Fact (Irreducible p)
inst✝ : Fact p.Monic
q : F[X]
⊢ p ∣
    (implicitDeriv
        ((AdjoinRoot.modByMonicHom ⋯)
          (-(aeval (AdjoinRoot.root p)) (mapCoeffs p) / (aeval (AdjoinRoot.root p)) (derivative p))))
      (p * q)
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 : (Module.rank F E).ord.ToType
ih : (y : (Module.rank F E).ord.ToType) → y < i → (Module.rank F E).ord.ToType
s : Set E := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : adjoin F s = ⊤
⊢ False

Tactic:
apply_fun Module.rank F at this

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 : (Module.rank F E).ord.ToType
ih : (y : (Module.rank F E).ord.ToType) → y < i → (Module.rank F E).ord.ToType
s : Set E := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : Module.rank F ↥(adjoin F s) = Module.rank F ↥⊤
⊢ False
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
p : ℕ
inst✝¹ : ExpChar M p
inst✝ : IsPRadical i p
h : pNilradical M p = ⊥
f g : L →+* M
heq : (fun f ↦ f.comp i) f = (fun f ↦ f.comp i) g
x : L
n : ℕ
y : K
hx : i y = x ^ p ^ n
⊢ f x = g x

Tactic:
apply_fun _ using pow_expChar_pow_inj_of_pNilradical_eq_bot M p h n

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
p : ℕ
inst✝¹ : ExpChar M p
inst✝ : IsPRadical i p
h : pNilradical M p = ⊥
f g : L →+* M
heq : (fun f ↦ f.comp i) f = (fun f ↦ f.comp i) g
x : L
n : ℕ
y : K
hx : i y = x ^ p ^ n
⊢ f x ^ p ^ n = g x ^ p ^ n