mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Dynamics.Ergodic.RadonNikodym

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hsm : MeasurableSet s
hνs : ν s = 0
hμs : (μ.singularPart ν) sᶜ = 0
⊢ (μ.singularPart ν) s = (μ.singularPart ν) univ

Tactic:
by
        rw [← measure_add_measure_compl hsm, hμs, add_zero]

Goal state after:
Module: Mathlib.Dynamics.Ergodic.RadonNikodym

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ✝ ν : Measure X
inst✝¹ : IsFiniteMeasure ν
f : X → X
hfν : MeasurePreserving f ν ν
μ : Measure X
inst✝ : IsFiniteMeasure μ
hfμ : MeasurePreserving f μ μ
hμν : μ ≪ ν
c : ENNReal
s : Set X := {a | μ.rnDeriv ν a < c}
hsm : MeasurableSet s
⊢ μ (f ⁻¹' s ∩ s) ≠ ⊤

Tactic:
finiteness

Goal state after:
Module: Mathlib.Dynamics.Ergodic.RadonNikodym

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ✝ ν : Measure X
inst✝¹ : IsFiniteMeasure ν
f : X → X
hfν : MeasurePreserving f ν ν
μ : Measure X
inst✝ : IsFiniteMeasure μ
hfμ : MeasurePreserving f μ μ
hμν : μ ≪ ν
c : ENNReal
s : Set X := {a | μ.rnDeriv ν a < c}
hsm : MeasurableSet s
hμ_sdiff : μ (f ⁻¹' s \ s) = μ (s \ f ⁻¹' s)
⊢ ν (f ⁻¹' s ∩ s) ≠ ⊤

Tactic:
finiteness

Goal state after:
Module: Mathlib.Dynamics.Ergodic.RadonNikodym

Goal state before:
pp: case hfi
X : Type u_1
m : MeasurableSpace X
μ✝ ν : Measure X
inst✝¹ : IsFiniteMeasure ν
f : X → X
hfν : MeasurePreserving f ν ν
μ : Measure X
inst✝ : IsFiniteMeasure μ
hfμ : MeasurePreserving f μ μ
hμν : μ ≪ ν
c : ENNReal
s : Set X := {a | μ.rnDeriv ν a < c}
hsm : MeasurableSet s
hν_sdiff : ν (f ⁻¹' s \ s) = ν (s \ f ⁻¹' s)
h₀ : ν (f ⁻¹' s \ s) ≠ 0
⊢ μ (s \ f ⁻¹' s) ≠ ⊤

Tactic:
finiteness

Goal state after:
Module: Mathlib.Dynamics.Ergodic.Extreme

Goal state before:
pp: case refine_1
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
this✝ : IsFiniteMeasure μ
S : Set (Measure X) := {ν | MeasurePreserving f ν ν ∧ ν univ = c}
h : μ ∈ extremePoints ℝ≥0∞ S
this : ∀ {s : Set X}, MeasurableSet s → f ⁻¹' s = s → μ s ≠ 0 → c • μ[|s] ∈ S
s : Set X
hsm : MeasurableSet s
hfs : f ⁻¹' s = s
H : ¬EventuallyConst s (ae μ)
hs : μ s ≠ 0
hs' : μ sᶜ ≠ 0
⊢ μ s / c + μ sᶜ / c = 1

Tactic:
rw [← ENNReal.add_div, measure_add_measure_compl hsm, h.1.2, ENNReal.div_self hc₀ hc]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν'
inst✝ : SigmaFinite ν'
h✝ : μ ⟂ₘ ν
hνν' : ν ≪ ν'
t : Set α := h✝.nullSet
ht : MeasurableSet t
h : (μ.restrict t).rnDeriv ν' =ᵐ[ν] t.indicator (μ.rnDeriv ν')
x : α
hx : (μ.restrict t).rnDeriv ν' x = t.indicator (μ.rnDeriv ν') x
hxt : x ∈ t
⊢ μ.rnDeriv ν' x = t.indicator (μ.rnDeriv ν') x

Tactic:
Set.indicator_of_mem hxt

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν'
inst✝ : SigmaFinite ν'
h✝ : μ ⟂ₘ ν
hνν' : ν ≪ ν'
t : Set α := h✝.nullSet
ht : MeasurableSet t
h : (μ.restrict t).rnDeriv ν' =ᵐ[ν] t.indicator (μ.rnDeriv ν')
x : α
hx : (μ.restrict t).rnDeriv ν' x = t.indicator (μ.rnDeriv ν') x
hxt : x ∈ t
⊢ μ.rnDeriv ν' x = μ.rnDeriv ν' x
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
⊢ netMaxcard T F U n < ⊤ ↔ ∃ s, IsDynNetIn T F U n ↑s ∧ ↑s.card = netMaxcard T F U n

Tactic:
apply Iff.intro <;> intro h
  · obtain ⟨k, k_max⟩ := ENat.ne_top_iff_exists.mp h.ne
    rw [← k_max]
    simp only [Nat.cast_inj]
    -- The criterion we want to use is `Nat.sSup_mem`. We rewrite `netMaxcard` with an `sSup`,
    -- then check its `BddAbove` and `Nonempty` hypotheses.
    have : netMaxcard T F U n
      = sSup (WithTop.some '' Finset.card '' {s : Finset X | IsDynNetIn T F U n s}) := by
      rw [netMaxcard, ← image_comp, sSup_image]
      simp only [mem_ofPred_eq, ENat.some_eq_natCast, Function.comp_apply]
      exact biSup_congr (fun _ _ ↦ rfl)
    rw [this] at k_max
    have h_bdda : BddAbove (Finset.card '' {s : Finset X | IsDynNetIn T F U n s}) := by
      refine ⟨k, mem_upperBounds.2 ?_⟩
      simp only [mem_image, mem_ofPred_eq, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
      intro s h
      rw [← ENat.natCast_le_natCast, k_max]
      apply le_sSup
      exact Filter.frequently_principal.mp fun a ↦ a (by simpa using ⟨_, h, rfl⟩) rfl
    have h_nemp : (Finset.card '' {s : Finset X | IsDynNetIn T F U n s}).Nonempty := by
      refine ⟨0, ?_⟩
      simp only [mem_image, mem_ofPred_eq, Finset.card_eq_zero, exists_eq_right, Finset.coe_empty]
      exact isDynNetIn_empty
    rw [← WithTop.coe_sSup' h_bdda] at k_max
    have key := Nat.sSup_mem h_nemp h_bdda
    rw [← Nat.cast_inj.mp k_max, mem_image] at key
    simp only [mem_ofPred_eq] at key
    exact key
  · obtain ⟨s, _, s_card⟩ := h
    rw [← s_card]
    exact WithTop.coe_lt_top s.card

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

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

Tactic:
rw [ha, C_0, sub_zero]

Goal state after:
case pos
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (X ^ n - 1)).Splits
ha : a = 0
⊢ Group.IsSolvable (X ^ n).Gal
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : (map i (X ^ n - C a)).Splits
ha' : i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : (X ^ n - C a).degree ≠ 0
b : E
hb : b ^ n = i a
hb' : b ≠ 0
s : Multiset E := (map i (X ^ n - C a)).roots
hs : map i (X ^ n - C a) = (Multiset.map (fun x ↦ X - C x) s).prod
hs' : s.card = n
⊢ C (i (a⁻¹ * a)) = 1

Tactic:
inv_mul_cancel₀ ha,

Goal state after:
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : (map i (X ^ n - C a)).Splits
ha' : i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : (X ^ n - C a).degree ≠ 0
b : E
hb : b ^ n = i a
hb' : b ≠ 0
s : Multiset E := (map i (X ^ n - C a)).roots
hs : map i (X ^ n - C a) = (Multiset.map (fun x ↦ X - C x) s).prod
hs' : s.card = n
⊢ C (i 1) = 1
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case all
L : Language
α : Type u'
k n✝¹ : ℕ
f✝ : L.BoundedFormula α (n✝¹ + 1)
ih3 : ∀ {m n : ℕ} (km : n✝¹ + 1 ≤ m) (mn : m ≤ n), castLE mn (castLE km f✝) = castLE ⋯ f✝
m✝ n✝ : ℕ
km✝ : n✝¹ ≤ m✝
mn✝ : m✝ ≤ n✝
⊢ castLE mn✝ (castLE km✝ f✝.all) = castLE ⋯ f✝.all

Tactic:
simp only [castLE, ih3]

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case equal
L : Language
L' : Language
α : Type u'
β : Type v'
γ : Type u_1
L'' : Language
ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin n)
fr : (n : ℕ) → L.Relations n → L'.Relations n
ft' : (n : ℕ) → L'.Term (β ⊕ Fin n) → L''.Term (γ ⊕ Fin n)
fr' : (n : ℕ) → L'.Relations n → L''.Relations n
n n✝ : ℕ
t₁✝ t₂✝ : L.Term (α ⊕ Fin n✝)
⊢ mapTermRel ft' fr' (fun x ↦ id) (mapTermRel ft fr (fun x ↦ id) (equal t₁✝ t₂✝)) =
    mapTermRel (fun x ↦ ft' x ∘ ft x) (fun x ↦ fr' x ∘ fr x) (fun x ↦ id) (equal t₁✝ t₂✝)

Tactic:
simp [mapTermRel]

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case rel
L : Language
L' : Language
α : Type u'
β : Type v'
γ : Type u_1
L'' : Language
ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin n)
fr : (n : ℕ) → L.Relations n → L'.Relations n
ft' : (n : ℕ) → L'.Term (β ⊕ Fin n) → L''.Term (γ ⊕ Fin n)
fr' : (n : ℕ) → L'.Relations n → L''.Relations n
n n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝)
⊢ mapTermRel ft' fr' (fun x ↦ id) (mapTermRel ft fr (fun x ↦ id) (rel R✝ ts✝)) =
    mapTermRel (fun x ↦ ft' x ∘ ft x) (fun x ↦ fr' x ∘ fr x) (fun x ↦ id) (rel R✝ ts✝)

Tactic:
simp [mapTermRel]

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case equal
L : Language
α : Type u'
n n✝ : ℕ
t₁✝ t₂✝ : L.Term (α ⊕ Fin n✝)
⊢ mapTermRel (fun x ↦ id) (fun x ↦ id) (fun x ↦ id) (equal t₁✝ t₂✝) = equal t₁✝ t₂✝

Tactic:
simp [mapTermRel]

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case rel
L : Language
α : Type u'
n n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝)
⊢ mapTermRel (fun x ↦ id) (fun x ↦ id) (fun x ↦ id) (rel R✝ ts✝) = rel R✝ ts✝

Tactic:
simp [mapTermRel]

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'
g : α → β
v : β → M
l✝ : ℕ
f : L.Functions l✝
ts : Fin l✝ → L.Term α
ih : ∀ (a : Fin l✝), realize v (relabel g (ts a)) = realize (v ∘ g) (ts a)
⊢ realize v (relabel g (func f ts)) = realize (v ∘ g) (func f ts)

Tactic:
| func f ts ih =>

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case func
L : Language
L' : Language
M : Type w
inst✝¹ : L.Structure M
β : Type v'
inst✝ : L'.Structure M
c : {n : ℕ} → L.Functions n → L'.Term (Fin n)
hc : ∀ {n : ℕ} (g : L.Functions n) (y : Fin n → M), realize y g.term = realize y (c g)
v : β → M
l✝ : ℕ
f : L.Functions l✝
ts : Fin l✝ → L.Term β
ih : ∀ (a : Fin l✝), realize v ((ts a).substFunc fun {n} ↦ c) = realize v (ts a)
⊢ realize v ((func f ts).substFunc fun {n} ↦ c) = realize v (func f ts)

Tactic:
| func f ts ih =>

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Field.CharP

Goal state before:
pp: case pos
p : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
hp0 : p = 0
⊢ K ⊨ (fun q ↦ ∼(eqZero q)) '' {q | Nat.Prime q} ↔ CharP K p

Tactic:
subst hp0

Goal state after:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
⊢ K ⊨ (fun q ↦ ∼(eqZero q)) '' {q | Nat.Prime q} ↔ CharP K 0
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
l✝ : ℕ
f : L.Functions l✝
ts : Fin l✝ → L.Term (α ⊕ β)
ih : ∀ (a : Fin l✝), realize v (ts a).varsToConstants = realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (ts a)
⊢ realize v (func f ts).varsToConstants = realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (func f ts)

Tactic:
| func f ts ih =>

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case func
L : Language
L' : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L'.Structure M
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
v : α → M
l✝ : ℕ
f : L.Functions l✝
ts : Fin l✝ → L.Term α
ih : ∀ (a : Fin l✝), Term.realize v (φ.onTerm (ts a)) = Term.realize v (ts a)
⊢ Term.realize v (φ.onTerm (func f ts)) = Term.realize v (func f ts)

Tactic:
| func f ts ih =>

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)
n : ℕ
f : L.Functions n
x y : Fin n → (a : α) → M a
xy : x ≈ y
⊢ funMap f x ≈ funMap f y

Tactic:
by
      refine mem_of_superset (iInter_mem.2 xy) fun a ha => ?_
      simp only [Set.mem_iInter, Set.mem_ofPred_eq] at ha
      simp only [Set.mem_ofPred_eq, ha]

Goal state after:
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: case all.h₂.refine_1
α : 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
k : ℕ
φ : L.BoundedFormula β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (φ.Realize (fun i ↦ Quotient.mk' (x i)) fun i ↦ Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, φ.Realize (fun i ↦ x i a) fun i ↦ v i a
v : Fin k → (a : α) → M a
h' : ∀ (m : (a : α) → M a) (a : α), (fun i ↦ Fin.snoc v m i a) = Fin.snoc (fun i ↦ v i a) (m a)
h : ∀ (m : (a : α) → M a), ∀ᶠ (a : α) in ↑u, φ.Realize (fun i ↦ x i a) (Fin.snoc (fun i ↦ v i a) (m a))
⊢ ∀ᶠ (a : α) in ↑u, ∀ (x_1 : M a), φ.Realize (fun i ↦ x i a) (Fin.snoc (fun i ↦ v i a) x_1)

pp: case all.h₂.refine_2
α : 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
k : ℕ
φ : L.BoundedFormula β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (φ.Realize (fun i ↦ Quotient.mk' (x i)) fun i ↦ Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, φ.Realize (fun i ↦ x i a) fun i ↦ v i a
v : Fin k → (a : α) → M a
h' : ∀ (m : (a : α) → M a) (a : α), (fun i ↦ Fin.snoc v m i a) = Fin.snoc (fun i ↦ v i a) (m a)
h : ∀ᶠ (a : α) in ↑u, ∀ (x_1 : M a), φ.Realize (fun i ↦ x i a) (Fin.snoc (fun i ↦ v i a) x_1)
m : (a : α) → M a
⊢ ∀ᶠ (a : α) in ↑u, φ.Realize (fun i ↦ x i a) (Fin.snoc (fun i ↦ v i a) (m a))

Tactic:
· contrapose! h
      refine
        ⟨fun a : α =>
          Classical.epsilon fun m : M a =>
            ¬φ.Realize (fun i => x i a) (Fin.snoc (fun i => v i a) m),
          ?_⟩
      exact Filter.mem_of_superset h fun a ha => Classical.epsilon_spec ha

Goal state after:
case all.h₂.refine_2
α : 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
k : ℕ
φ : L.BoundedFormula β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (φ.Realize (fun i ↦ Quotient.mk' (x i)) fun i ↦ Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, φ.Realize (fun i ↦ x i a) fun i ↦ v i a
v : Fin k → (a : α) → M a
h' : ∀ (m : (a : α) → M a) (a : α), (fun i ↦ Fin.snoc v m i a) = Fin.snoc (fun i ↦ v i a) (m a)
h : ∀ᶠ (a : α) in ↑u, ∀ (x_1 : M a), φ.Realize (fun i ↦ x i a) (Fin.snoc (fun i ↦ v i a) x_1)
m : (a : α) → M a
⊢ ∀ᶠ (a : α) in ↑u, φ.Realize (fun i ↦ x i a) (Fin.snoc (fun i ↦ v i a) (m a))
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
⊢ (↑u).Product M ⊨ φ ↔ ∀ᶠ (a : α) in ↑u, M a ⊨ φ

Tactic:
simp_rw [Sentence.Realize]

Goal state after:
α : 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 ↔ ∀ᶠ (a : α) in ↑u, Formula.Realize φ default
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n' m : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin (n + n') → M
hmn : m ≤ n
⊢ (liftAt n' m φ).Realize v xs ↔ φ.Realize v (xs ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n')

Tactic:
rw [liftAt]

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n' m : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin (n + n') → M
hmn : m ≤ n
⊢ (mapTermRel (fun x t ↦ Term.liftAt n' m t) (fun x ↦ id) (fun x ↦ castLE ⋯) φ).Realize v xs ↔
    φ.Realize v (xs ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n')
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case refine_2.refine_2.inr.inr
L : Language
α : Type u'
a b : (i : ℕ) × L.Functions i
h : a.fst = b.fst ∧ a.snd ≍ b.snd ∧ (fun x ↦ var (Sum.inr 0)) ≍ fun x ↦ var (Sum.inr 0)
⊢ Sum.inr a = Sum.inr b

Tactic:
Sigma.ext_iff.2 ⟨h.1, h.2.1⟩

Goal state after:
case refine_2.refine_2.inr.inr
L : Language
α : Type u'
a b : (i : ℕ) × L.Functions i
h : a.fst = b.fst ∧ a.snd ≍ b.snd ∧ (fun x ↦ var (Sum.inr 0)) ≍ fun x ↦ var (Sum.inr 0)
⊢ Sum.inr b = Sum.inr b
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: case func
L : Language
M : Type w
inst✝ : L.Structure M
S : L.Substructure M
α : Type u_3
xs : α → M
h : ∀ (a : α), xs a ∈ S
l✝ : ℕ
f : L.Functions l✝
ts : Fin l✝ → L.Term α
ih : ∀ (a : Fin l✝), realize xs (ts a) ∈ S
⊢ realize xs (func f ts) ∈ S

Tactic:
| func f ts ih =>

Goal state after:
Module: Mathlib.ModelTheory.Semantics

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

Tactic:
rw [Formula.iAlls]

Goal state after:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
⊢ (relabel (fun a ↦ Sum.map id (⇑(Classical.choice ⋯)) a) φ).alls.Realize v ↔
    ∀ (i : β → M), φ.Realize fun a ↦ Sum.elim v i a
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type u_1
L : Language
inst✝ : L.Structure M
α : Type u_2
t : L.Term α
⊢ DefinableFun L ∅ fun v ↦ Term.realize v t

Tactic:
rw [empty_definableFun_iff]

Goal state after:
M : Type u_1
L : Language
inst✝ : L.Structure M
α : Type u_2
t : L.Term α
⊢ ∃ φ, (tupleGraph fun v ↦ Term.realize v t) = ofPred φ.Realize
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case refine_2
L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
xs : Nonempty (Fin n ↪ M)
⊢ ∀ (φ : L.BoundedFormula Empty n) (x x_1 : Fin n),
    (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize default ⇑xs.some

Tactic:
rintro _ i j ij rfl

Goal state after:
case refine_2
L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
xs : Nonempty (Fin n ↪ M)
i j : Fin n
ij : (decide ¬i = j) = true
⊢ (∼(var (Sum.inr i) =' var (Sum.inr j))).Realize default ⇑xs.some
Module: Mathlib.RingTheory.MvPolynomial.FreeCommRing

Goal state before:
pp: ι : Type u_1
κ : Type u_2
R : Type u_3
inst✝² : DecidableEq κ
inst✝¹ : CommRing R
inst✝ : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
p : { p // ∀ (i : ι), (p i).support ⊆ monoms i }
⊢ (fun p ↦
        ⟨fun i ↦
          AddMonoidAlgebra.ofCoeff
            { support := {m ∈ monoms i | ∃ (hm : m ∈ monoms i), p ⟨i, ⟨m, hm⟩⟩ ≠ 0},
              toFun := fun m ↦ if hm : m ∈ monoms i then p ⟨i, ⟨m, hm⟩⟩ else 0, mem_support_toFun := ⋯ },
          ⋯⟩)
      ((fun p i ↦ coeff (↑i.snd) (↑p i.fst)) p) =
    p

Tactic:
ext i m

Goal state after:
ι : Type u_1
κ : Type u_2
R : Type u_3
inst✝² : DecidableEq κ
inst✝¹ : CommRing R
inst✝ : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
p : { p // ∀ (i : ι), (p i).support ⊆ monoms i }
i : ι
m : κ →₀ ℕ
⊢ coeff m
      (↑((fun p ↦
              ⟨fun i ↦
                AddMonoidAlgebra.ofCoeff
                  { support := {m ∈ monoms i | ∃ (hm : m ∈ monoms i), p ⟨i, ⟨m, hm⟩⟩ ≠ 0},
                    toFun := fun m ↦ if hm : m ∈ monoms i then p ⟨i, ⟨m, hm⟩⟩ else 0, mem_support_toFun := ⋯ },
                ⋯⟩)
            ((fun p i ↦ coeff (↑i.snd) (↑p i.fst)) p))
        i) =
    coeff m (↑p i)
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case inr
L : Language
T : L.Theory
h : T.IsComplete
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
φ : L.BoundedFormula Empty 0
h_realize : M ⊨ φ
hT : T ⊨ᵇ Formula.not φ
this : M ⊨ ∼φ
⊢ T ⊨ᵇ φ

Tactic:
rw [Sentence.realize_not] at this

Goal state after:
case inr
L : Language
T : L.Theory
h : T.IsComplete
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
φ : L.BoundedFormula Empty 0
h_realize : M ⊨ φ
hT : T ⊨ᵇ Formula.not φ
this : ¬M ⊨ φ
⊢ T ⊨ᵇ φ
Module: Mathlib.ModelTheory.Satisfiability

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

Tactic:
left

Goal state after:
case pos
L : Language
T : L.Theory
h : ∀ (M N : T.ModelType), ↑M ≅[L] ↑N
φ : L.Sentence
M : T.ModelType
hφ : ↑M ⊨ φ
⊢ T ⊨ᵇ φ
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: φ : Language.ring.Sentence
h : Theory.ACF 0 ⊨ᵇ φ
⊢ {p | ¬Theory.ACF ↑p ⊨ᵇ φ}.Finite

Tactic:
rw [Theory.models_iff_finset_models] at h
  rcases h with ⟨T0, hT0, h⟩
  have f : ∀ ψ ∈ Theory.ACF 0,
      { s : Finset Nat.Primes // ∀ q : Nat.Primes, q ∉ s → Theory.ACF q ⊨ᵇ ψ } := by
    intro ψ hψ
    rw [Theory.ACF, Theory.fieldOfChar, Set.union_right_comm, Set.mem_union, if_pos rfl,
      Set.mem_image] at hψ
    apply Classical.choice
    rcases hψ with h | ⟨p, hp, rfl⟩
    · refine ⟨⟨∅, ?_⟩⟩
      intro q _
      exact Theory.models_sentence_of_mem
        (by rw [Theory.ACF, Theory.fieldOfChar, Set.union_right_comm];
            exact Set.mem_union_left _ h)
    · refine ⟨⟨{⟨p, hp⟩}, ?_⟩⟩
      rintro ⟨q, _⟩ hq ⟨K⟩ _ _
      have hqp : q ≠ p := by simpa [← Nat.Primes.coe_nat_inj] using hq
      let _ := fieldOfModelACF q K
      have := modelField_of_modelACF q K
      let _ := compatibleRingOfModelField K
      have := charP_of_model_fieldOfChar q K
      simp only [eqZero, Term.equal, BoundedFormula.realize_not, BoundedFormula.realize_bdEqual,
        Term.realize_relabel, Sum.elim_comp_inl, realize_termOfFreeCommRing, map_natCast,
        realize_zero, ← CharP.charP_iff_prime_eq_zero hp]
      intro _
      exact hqp <| CharP.eq K this inferInstance
  let s : Finset Nat.Primes := T0.attach.biUnion (fun φ => f φ.1 (hT0 φ.2))
  have hs : ∀ (p : Nat.Primes) ψ, ψ ∈ T0 → p ∉ s → Theory.ACF p ⊨ᵇ ψ := by
    intro p ψ hψ hpψ
    simp only [s, Finset.mem_biUnion, Finset.mem_attach, true_and,
      Subtype.exists, not_exists] at hpψ
    exact (f ψ (hT0 hψ)).2 p (hpψ _ hψ)
  refine Set.Finite.subset (Finset.finite_toSet s) (Set.compl_subset_comm.2 ?_)
  intro p hp
  exact Theory.models_of_models_theory (fun ψ hψ => hs p ψ hψ hp) h

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
h : T.IsMaximal
φ : L.Sentence
hφ : ¬(T ∪ {Formula.not φ}).IsSatisfiable
con : Formula.not φ ∈ T
⊢ False

Tactic:
Set.union_singleton,

Goal state after:
L : Language
T : L.Theory
h : T.IsMaximal
φ : L.Sentence
hφ : ¬IsSatisfiable (insert (Formula.not φ) T)
con : Formula.not φ ∈ T
⊢ False
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: a✝ a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
h : c ≤ b
⊢ a ∣ b ∨ a ∣ c

Tactic:
left

Goal state after:
a✝ a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
h : c ≤ b
⊢ a ∣ b
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✝ : IsGalois K L
e : Gal(L/K)
⊢ (basisOfLinearIndependentOfCardEqFinrank ⋯ ⋯) e = e ((basisOfLinearIndependentOfCardEqFinrank ⋯ ⋯) 1)

Tactic:
coe_basisOfLinearIndependentOfCardEqFinrank,

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✝ : IsGalois K L
e : Gal(L/K)
⊢ e ⋯.choose = e (1 ⋯.choose)
Module: Mathlib.FieldTheory.Galois.Profinite

Goal state before:
pp: k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
g : ↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
x : K
L : FiniteGaloisIntermediateField k K
hx : x ∈ L.toIntermediateField
⊢ toAlgEquivAux g x = (((proj L) g).liftNormal K) x

Tactic:
by
  rw [toAlgEquivAux_eq_proj_of_mem g x L hx]
  exact (AlgEquiv.liftNormal_commutes (proj L g) _ ⟨x, hx⟩).symm

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝¹ : PerfectClosure K p
x : ℕ × K
x✝ : IsNilpotent (mk K p x)
n : ℕ
h : mk K p x ^ n = 0
⊢ mk K p x = 0

Tactic:
replace h : mk K p x ^ p ^ n = 0 := by
      rw [← Nat.sub_add_cancel ((n.lt_pow_self (Fact.out : p.Prime).one_lt).le),
        pow_add, h, mul_zero]

Goal state after:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝¹ : PerfectClosure K p
x : ℕ × K
x✝ : IsNilpotent (mk K p x)
n : ℕ
h : mk K p x ^ p ^ n = 0
⊢ mk K p x = 0
Module: Mathlib.FieldTheory.Laurent

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
r : R
inst✝ : IsDomain R
x : R
⊢ (laurent r) (C x) = C x

Tactic:
rw [← algebraMap_C, laurent_algebraMap, taylor_C]

Goal state after: