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

Goal state before:
pp: α : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁹ : TopologicalSpace X
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
inst✝⁶ : R1Space X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace Y
inst✝³ : BorelSpace Y
inst✝² : R1Space Y
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
l : Filter α
f : α → C(X, Y)
g : C(X, Y)
s : Set Y
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν
hg : MeasurePreserving (⇑g) μ ν
hs : NullMeasurableSet s ν
hνs : ν s ≠ ∞
this : ν.InnerRegularCompactLTTop
ε : ℝ≥0∞
hε : ε > 0
⊢ ∀ᶠ (x : α) in l, μ ((⇑(f x) ⁻¹' s) ∆ (⇑g ⁻¹' s)) ≤ ε

Tactic:
wlog hso : IsOpen s generalizing s ε

Goal state after:
case inr
α : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁹ : TopologicalSpace X
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
inst✝⁶ : R1Space X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace Y
inst✝³ : BorelSpace Y
inst✝² : R1Space Y
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
l : Filter α
f : α → C(X, Y)
g : C(X, Y)
s : Set Y
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν
hg : MeasurePreserving (⇑g) μ ν
hs : NullMeasurableSet s ν
hνs : ν s ≠ ∞
this✝ : ν.InnerRegularCompactLTTop
ε : ℝ≥0∞
hε : ε > 0
this :
  ∀ {s : Set Y},
    NullMeasurableSet s ν → ν s ≠ ∞ → ∀ ε > 0, IsOpen[inst✝⁵] s → ∀ᶠ (x : α) in l, μ ((⇑(f x) ⁻¹' s) ∆ (⇑g ⁻¹' s)) ≤ ε
hso : ¬IsOpen[inst✝⁵] s
⊢ ∀ᶠ (x : α) in l, μ ((⇑(f x) ⁻¹' s) ∆ (⇑g ⁻¹' s)) ≤ ε

α : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁹ : TopologicalSpace X
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
inst✝⁶ : R1Space X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace Y
inst✝³ : BorelSpace Y
inst✝² : R1Space Y
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
l : Filter α
f : α → C(X, Y)
g : C(X, Y)
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν
hg : MeasurePreserving (⇑g) μ ν
this : ν.InnerRegularCompactLTTop
s : Set Y
hs : NullMeasurableSet s ν
hνs : ν s ≠ ∞
ε : ℝ≥0∞
hε : ε > 0
hso : IsOpen[inst✝⁵] s
⊢ ∀ᶠ (x : α) in l, μ ((⇑(f x) ⁻¹' s) ∆ (⇑g ⁻¹' s)) ≤ ε
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
hf : Continuous ⇑f
⊢ ∃ x, f x ≤ x + τ f

Tactic:
by_contra! H
    exact lt_irrefl _ (f.lt_translationNumber_of_forall_add_lt hf H)

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

Goal state before:
pp: case succ.refine_1
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : μ s ≠ 0
x : α
left✝ : x ∈ s
hx : {n | f^[n] x ∈ s}.Infinite
k : ℕ
hk : k ∈ {n | f^[n] x ∈ s}
l : ℕ
hl : l ∈ {n | f^[n] x ∈ s}
hkl : k < l
hn : k ≡ l [MOD n.succ]
m : ℕ := (l - k) / (n + 1)
this : (n + 1) * m = l - k
⊢ m ≠ 0

Tactic:
intro hm

Goal state after:
case succ.refine_1
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : μ s ≠ 0
x : α
left✝ : x ∈ s
hx : {n | f^[n] x ∈ s}.Infinite
k : ℕ
hk : k ∈ {n | f^[n] x ∈ s}
l : ℕ
hl : l ∈ {n | f^[n] x ∈ s}
hkl : k < l
hn : k ≡ l [MOD n.succ]
m : ℕ := (l - k) / (n + 1)
this : (n + 1) * m = l - k
hm : m = 0
⊢ False
Module: Mathlib.Topology.Order.CountableSeparating

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LinearOrder X
inst✝¹ : OrderTopology X
inst✝ : SecondCountableTopology X
s : Set X
⊢ ∃ S, S.Countable ∧ (∀ s ∈ S, s ∈ range Iio) ∧ ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y

Tactic:
rcases TopologicalSpace.exists_countable_dense X with ⟨s, hsc, hsd⟩

Goal state after:
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LinearOrder X
inst✝¹ : OrderTopology X
inst✝ : SecondCountableTopology X
s✝ s : Set X
hsc : s.Countable
hsd : Dense s
⊢ ∃ S, S.Countable ∧ (∀ s ∈ S, s ∈ range Iio) ∧ ∀ x ∈ s✝, ∀ y ∈ s✝, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
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:
← measure_add_measure_compl hsm,

Goal state after:
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 ν) s + (μ.singularPart ν) sᶜ
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Inhabited A
G : Type u_2
inst✝² : Monoid G
inst✝¹ : IsLeftCancelMul G
inst✝ : DiscreteTopology A
F : Set (Pattern A G)
⊢ IsClosed[Pi.topologicalSpace] (mulForbidden F)

Tactic:
mulForbidden

Goal state after:
A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Inhabited A
G : Type u_2
inst✝² : Monoid G
inst✝¹ : IsLeftCancelMul G
inst✝ : DiscreteTopology A
F : Set (Pattern A G)
⊢ IsClosed[Pi.topologicalSpace] {x | ∀ p ∈ F, ∀ (g : G), ¬p.mulOccursInAt x g}
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: A : Type u_3
G : Type u_4
inst✝¹ : Finite A
inst✝ : Inhabited A
U : Finset G
val✝ : Fintype A
f : ↥U → A
g : G
hg : g ∉ U
⊢ (if h : g ∈ U then f ⟨g, h⟩ else default) = default

Tactic:
simp [hg]

Goal state after:
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: case pos
A : Type u_3
G : Type u_4
inst✝¹ : Finite A
inst✝ : Inhabited A
val✝ : Fintype A
cfg : G → A
dom : Finset G
cond : ∀ g ∉ dom, cfg g = default
g : G
hg : g ∈ dom
⊢ (if h : g ∈ dom then cfg g else default) = cfg g

Tactic:
simp [hg]

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
this : μ.rnDeriv ν' =ᵐ[ν.restrict t] (μ.restrict t).rnDeriv ν'
⊢ (μ.restrict t).rnDeriv ν' =ᵐ[ν.restrict t] 0

Tactic:
simp only [t, MutuallySingular.restrict_nullSet]

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

Goal state before:
pp: τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : T2Space β
c : Set β
hc₁ : IsCompact c
hc₂ : ∀ᶠ (t : τ) in f, MapsTo (ϕ t) s c
n : Set β
hn₁ : IsOpen[inst✝¹] n
hn₂ : ω f ϕ s ⊆ n
⊢ ∀ᶠ (t : τ) in f, MapsTo (ϕ t) s n

Tactic:
by
  rcases eventually_closure_subset_of_isCompact_absorbing_of_isOpen_of_omegaLimit_subset f ϕ s hc₁
      hc₂ hn₁ hn₂ with
    ⟨u, hu_mem, hu⟩
  refine mem_of_superset hu_mem fun t ht x hx ↦ ?_
  exact hu (subset_closure <| mem_image2_of_mem ht hx)

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

Goal state before:
pp: case mp
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n < ⊤
k : ℕ
k_max : ↑k = netMaxcard T F U n
this : netMaxcard T F U n = sSup (WithTop.some '' Finset.card '' {s | IsDynNetIn T F U n ↑s})
⊢ ∃ s, IsDynNetIn T F U n ↑s ∧ s.card = k

Tactic:
rw [this] at k_max

Goal state after:
case mp
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n < ⊤
k : ℕ
k_max : ↑k = sSup (WithTop.some '' Finset.card '' {s | IsDynNetIn T F U n ↑s})
this : netMaxcard T F U n = sSup (WithTop.some '' Finset.card '' {s | IsDynNetIn T F U n ↑s})
⊢ ∃ s, IsDynNetIn T F U n ↑s ∧ s.card = k
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: case mpr
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : ∀ (k : ℕ), ∃ s, IsDynNetIn T F U n ↑s ∧ k ≤ s.card
k : ℕ
⊢ ↑k < netMaxcard T F U n

Tactic:
specialize h (k + 1)

Goal state after:
case mpr
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n k : ℕ
h : ∃ s, IsDynNetIn T F U n ↑s ∧ k + 1 ≤ s.card
⊢ ↑k < netMaxcard T F U n
Module: Mathlib.Dynamics.TopologicalEntropy.Subset

Goal state before:
pp: X : Type u_1
T : X → X
V : SetRel X X
inst✝ : UniformSpace X
h : Continuous T
F : Set X
U : SetRel X X
V_uni : V ∈ 𝓤 X
n : ℕ
⊢ coverMincard T (closure F) (V ○ U) n ≤ coverMincard T F U n

Tactic:
rcases eq_top_or_lt_top (coverMincard T F U n) with h' | h'
  · exact h' ▸ le_top
  obtain ⟨s, s_cover, s_coverMincard⟩ := (coverMincard_finite_iff T F U n).1 h'
  exact s_coverMincard ▸ (s_cover.closure h V_uni).coverMincard_le_card

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case neg
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (X ^ n - 1)).Splits
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
⊢ Group.IsSolvable (X ^ n - C a).Gal

Tactic:
have hn'' : X ^ n - C a ≠ 0 := X_pow_sub_C_ne_zero hn' a

Goal state after:
case neg
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (X ^ n - 1)).Splits
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
⊢ Group.IsSolvable (X ^ n - C a).Gal
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
toEquiv✝¹ : M ≃ N
map_fun'✝¹ :
  ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEquiv✝¹.toFun (funMap f x) = funMap f (toEquiv✝¹.toFun ∘ x)
map_rel'✝¹ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEquiv✝¹.toFun ∘ x) ↔ RelMap r x
toEquiv✝ : M ≃ N
map_fun'✝ : ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEquiv✝.toFun (funMap f x) = funMap f (toEquiv✝.toFun ∘ x)
map_rel'✝ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEquiv✝.toFun ∘ x) ↔ RelMap r x
h₁ :
  { toEquiv := toEquiv✝¹, map_fun' := map_fun'✝¹, map_rel' := map_rel'✝¹ }.toFun =
    { toEquiv := toEquiv✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ }.toFun
h₂ :
  { toEquiv := toEquiv✝¹, map_fun' := map_fun'✝¹, map_rel' := map_rel'✝¹ }.invFun =
    { toEquiv := toEquiv✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ }.invFun
x : M
⊢ toEquiv✝¹ x = toEquiv✝ x

Tactic:
exact funext_iff.1 h₁ x

Goal state after:
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: case refine_1
L : Language
L' : Language
M : Type w
inst✝² : L.Structure M
α : Type u_1
inst✝¹ : (constantsOn α).Structure M
A B : Set M
h : A ⊆ B
N : Type w'
inst✝ : L.Structure N
f : M ↪[L] N
⊢ ∀ {n : ℕ} (f_1 : L[[↑A]].Functions n) (x : Fin n → M), f.toFun (funMap f_1 x) = funMap f_1 (f.toFun ∘ x)

Tactic:
intro n g x
    cases g with
    | inl g => exact f.map_fun' g x
    | inr c =>
      cases n with
      | zero => rfl
      | succ n => exact isEmptyElim c

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

Goal state before:
pp: case inr
α : Type u_1
fst✝ : ℕ
f : ring.Relations fst✝
⊢ Sum.inr ⟨fst✝, f⟩ ∈
    { 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:
· cases f

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case hq.refine_2
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
hx : x ∈ solvableByRad F E
n : ℕ
hn : n ≠ 0
hα : Group.IsSolvable (minpoly F (x ^ n)).Gal
p : F[X] := ⋯
hp : p.comp (X ^ n) ≠ 0
s : Multiset p.SplittingField
hs :
  map (algebraMap F p.SplittingField) p =
    C (map (algebraMap F p.SplittingField) p).leadingCoeff * (Multiset.map (fun x ↦ X - C x) s).prod
⊢ Group.IsSolvable ((Multiset.map (fun x ↦ X - C x) s).prod.comp (X ^ n)).Gal

Tactic:
multiset_prod_comp

Goal state after:
case hq.refine_2
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
hx : x ∈ solvableByRad F E
n : ℕ
hn : n ≠ 0
hα : Group.IsSolvable (minpoly F (x ^ n)).Gal
p : F[X] := minpoly F (x ^ n)
hp : p.comp (X ^ n) ≠ 0
s : Multiset p.SplittingField
hs :
  map (algebraMap F p.SplittingField) p =
    C (map (algebraMap F p.SplittingField) p).leadingCoeff * (Multiset.map (fun x ↦ X - C x) s).prod
⊢ Group.IsSolvable (Multiset.map (fun p_1 ↦ p_1.comp (X ^ n)) (Multiset.map (fun x ↦ X - C x) s)).prod.Gal
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case inl
M : Type w
α : Type u'
β : Type v'
n m : ℕ
g : α → β ⊕ Fin n
v : β → M
xs : Fin (n + m) → M
x : α
⊢ (Sum.elim v xs ∘ relabelAux g m) (Sum.inl x) = Sum.elim (Sum.elim v (xs ∘ castAdd m) ∘ g) (xs ∘ natAdd n) (Sum.inl x)

Tactic:
simp only [BoundedFormula.relabelAux, Function.comp_apply, Sum.map_inl, Sum.elim_inl]

Goal state after:
case inl
M : Type w
α : Type u'
β : Type v'
n m : ℕ
g : α → β ⊕ Fin n
v : β → M
xs : Fin (n + m) → M
x : α
⊢ Sum.elim v xs (Sum.map id (⇑finSumFinEquiv) ((Equiv.sumAssoc β (Fin n) (Fin m)) (Sum.inl (g x)))) =
    Sum.elim v (xs ∘ castAdd m) (g x)
Module: Mathlib.ModelTheory.Algebra.Field.CharP

Goal state before:
pp: case inr
p : ℕ
K : Type u_1
inst✝² : Field K
inst✝¹ : CompatibleRing K
inst✝ : CharP K p
hp : p = 0
⊢ K ⊨ if p = 0 then (fun q ↦ ∼(eqZero q)) '' {q | Nat.Prime q} else if Nat.Prime p then {eqZero p} else {⊥}

Tactic:
| inr hp =>

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case cons
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n : ℕ
v : α → M
xs : Fin n → M
φ : L.BoundedFormula α n
l : List (L.BoundedFormula α n)
ih : (List.foldr (fun x1 x2 ↦ x1 ⊔ x2) ⊥ l).Realize v xs ↔ ∃ φ ∈ l, φ.Realize v xs
⊢ (φ.Realize v xs ∨ ∃ φ ∈ l, φ.Realize v xs) ↔ ∃ φ_1, φ_1 = φ ∧ φ_1.Realize v xs ∨ φ_1 ∈ l ∧ φ_1.Realize v xs

Tactic:
exists_or,

Goal state after:
case cons
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n : ℕ
v : α → M
xs : Fin n → M
φ : L.BoundedFormula α n
l : List (L.BoundedFormula α n)
ih : (List.foldr (fun x1 x2 ↦ x1 ⊔ x2) ⊥ l).Realize v xs ↔ ∃ φ ∈ l, φ.Realize v xs
⊢ (φ.Realize v xs ∨ ∃ φ ∈ l, φ.Realize v xs) ↔ (∃ x, x = φ ∧ x.Realize v xs) ∨ ∃ x ∈ l, x.Realize v xs
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: case rel
α : 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✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → 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
⊢ (RelMap R✝ fun i ↦ Term.realize (Sum.elim (fun i ↦ Quotient.mk' (x i)) fun i ↦ Quotient.mk' (v i)) (ts✝ i)) ↔
    ∀ᶠ (a : α) in ↑u, RelMap R✝ fun i ↦ Term.realize (fun i ↦ Sum.elim x v i a) (ts✝ i)

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

Goal state after:
case rel
α : 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✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → 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
⊢ (RelMap R✝ fun i ↦ Term.realize (Quotient.mk' ∘ Sum.elim x v) (ts✝ i)) ↔
    ∀ᶠ (a : α) in ↑u, RelMap R✝ fun i ↦ Term.realize (fun i ↦ Sum.elim x v i a) (ts✝ i)
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
x : M
⊢ x ∈ (closure L).toFun s ↔ ∃ t, Term.realize Subtype.val t = x

Tactic:
by
  rw [← SetLike.mem_coe, coe_closure_eq_range_term_realize, mem_range]

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: 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

pp: 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

Tactic:
· exact fun _ _ => h f.2

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

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
S : L.Substructure M
x : M
⊢ (∃ y, ↑y = x) ↔ x ∈ S

Tactic:
refine ⟨?_, fun h => ⟨⟨x, h⟩, rfl⟩⟩

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
S : L.Substructure M
x : M
⊢ (∃ y, ↑y = x) → x ∈ S
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: case intro.intro.mp
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 : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  A.Definable L
    ((fun g ↦ g ∘ rangeSplitting f) ⁻¹'
      (fun g ↦ g ∘ Sum.inl) ''
        (fun g ↦ g ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          (fun g ↦ g ∘ ⇑(Equiv.Set.sumCompl (range f))) '' s)
h' : A.Definable L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
x : α → M
⊢ ((∃ a ∈ s,
        ((a ∘ ⇑(Equiv.Set.sumCompl (range f))) ∘
              ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ∘
            Sum.inl =
          x ∘ rangeSplitting f) ∧
      ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))) →
    ∃ x_1 ∈ s, x_1 ∘ f = x

Tactic:
rintro ⟨⟨y, ys, hy⟩, hx⟩

Goal state after:
case intro.intro.mp
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 : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  A.Definable L
    ((fun g ↦ g ∘ rangeSplitting f) ⁻¹'
      (fun g ↦ g ∘ Sum.inl) ''
        (fun g ↦ g ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          (fun g ↦ g ∘ ⇑(Equiv.Set.sumCompl (range f))) '' s)
h' : A.Definable L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
x : α → M
hx : ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))
y : β → M
ys : y ∈ s
hy :
  ((y ∘ ⇑(Equiv.Set.sumCompl (range f))) ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ∘
      Sum.inl =
    x ∘ rangeSplitting f
⊢ ∃ x_1 ∈ s, x_1 ∘ f = x
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
r : L.Relations 2
⊢ M ⊨ r.irreflexive ↔ Std.Irrefl fun x y ↦ RelMap r ![x, y]

Tactic:
irrefl_def

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
r : L.Relations 2
⊢ M ⊨ r.irreflexive ↔ ∀ ⦃a : M⦄, ¬RelMap r ![a, a]
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: case inr
p : ℕ
hp : p = 0
⊢ (Theory.ACF p).IsSatisfiable

Tactic:
| inr hp =>

Goal state after:
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 }
i : ι
m : κ →₀ ℕ
⊢ m ∉ monoms i → 0 = (↑p i).coeff m

Tactic:
intro hm

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 : κ →₀ ℕ
hm : m ∉ monoms i
⊢ 0 = (↑p i).coeff m
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 (κ →₀ ℕ)
f : (i : ι) × ↥(monoms i) ⊕ κ → R
i : ι
m : ↥(monoms i)
a✝ : m ∈ (monoms i).attach
⊢ f (Sum.inl ⟨i, m⟩) * (lift f) ((↑m).prod fun j n ↦ of (Sum.inr j) ^ n) =
    if ∃ (h : ↑m ∈ monoms i), ¬f (Sum.inl ⟨i, ⟨↑m, ⋯⟩⟩) = 0 then
      (if h : ↑m ∈ monoms i then f (Sum.inl ⟨i, ⟨↑m, ⋯⟩⟩) else 0) * ∏ x ∈ (↑m).support, f (Sum.inr x) ^ ↑m x
    else 0

Tactic:
simp only [Finsupp.prod, map_prod, map_pow, lift_of, Subtype.coe_eta, Finset.coe_mem,
    exists_prop, true_and, dite_eq_ite, ite_true, ite_not]

Goal state after:
ι : Type u_1
κ : Type u_2
R : Type u_3
inst✝² : DecidableEq κ
inst✝¹ : CommRing R
inst✝ : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
f : (i : ι) × ↥(monoms i) ⊕ κ → R
i : ι
m : ↥(monoms i)
a✝ : m ∈ (monoms i).attach
⊢ f (Sum.inl ⟨i, m⟩) * ∏ x ∈ (↑m).support, f (Sum.inr x) ^ ↑m x =
    if f (Sum.inl ⟨i, m⟩) = 0 then 0 else f (Sum.inl ⟨i, m⟩) * ∏ x ∈ (↑m).support, f (Sum.inr x) ^ ↑m x
Module: Mathlib.ModelTheory.Algebra.Ring.Definability

Goal state before:
pp: ι : Type u_1
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
S : Finset (MvPolynomial ι K)
⊢ ∃ φ, zeroLocus K (Ideal.span ↑S) = {v | φ.Realize (Sum.elim Subtype.val v)}

Tactic:
let p' := genericPolyMap (fun p : S => p.1.support)

Goal state after:
ι : Type u_1
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
S : Finset (MvPolynomial ι K)
p' : ↥S → FreeCommRing ((i : ↥S) × ↥(↑i).support ⊕ ι) := genericPolyMap fun p ↦ (↑p).support
⊢ ∃ φ, zeroLocus K (Ideal.span ↑S) = {v | φ.Realize (Sum.elim Subtype.val v)}
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case inl
L : Language
M : Type w'
inst✝¹ : L.Structure M
inst✝ : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
N : Bundled L.Structure
hNκ : #↑N = κ
NM : Nonempty (↑N ↪ₑ[L] M)
⊢ ∃ N, (M ≅[L] ↑N) ∧ #↑N = κ

pp: case inr
L : Language
M : Type w'
inst✝¹ : L.Structure M
inst✝ : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
N : Bundled L.Structure
hNκ : #↑N = κ
MN : Nonempty (M ↪ₑ[L] ↑N)
⊢ ∃ N, (M ≅[L] ↑N) ∧ #↑N = κ

Tactic:
· exact ⟨N, NM.some.elementarilyEquivalent.symm, hNκ⟩

Goal state after:
case inr
L : Language
M : Type w'
inst✝¹ : L.Structure M
inst✝ : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
N : Bundled L.Structure
hNκ : #↑N = κ
MN : Nonempty (M ↪ₑ[L] ↑N)
⊢ ∃ N, (M ≅[L] ↑N) ∧ #↑N = κ
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
φ : L.Sentence
h : T ⊨ᵇ φ
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
⊢ M ⊨ φ

Tactic:
by
  rw [models_iff_not_satisfiable] at h
  contrapose h
  have : M ⊨ T ∪ {Formula.not φ} := by
    simp only [Set.union_singleton, model_iff, Set.mem_insert_iff, forall_eq_or_imp,
      Sentence.realize_not]
    rw [← model_iff]
    exact ⟨h, inferInstance⟩
  exact Model.isSatisfiable M

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case inr
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφn : T ⊨ᵇ Formula.not φ
hφ : T ⊨ᵇ φ
⊢ False

Tactic:
models_sentence_iff

Goal state after:
case inr
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφn : ∀ (M : T.ModelType), ↑M ⊨ Formula.not φ
hφ : ∀ (M : T.ModelType), ↑M ⊨ φ
⊢ False
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 φ
⊢ T ⊨ᵇ φ

Tactic:
| inr hT =>

Goal state after:
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
      exact models_sentence_iff.2 fun N => (elementarilyEquivalent_iff.1 (h M N) φ).1 hφ

Goal state after: