mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensityVec

Goal state before:
pp: X : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
mX : MeasurableSpace X
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
μ : VectorMeasure X F
f : X → E
B : E →L[ℝ] F →L[ℝ] G
inst✝ : CompleteSpace G
hf : μ.Integrable f
hB : ∀ (x : E) (y : F), ‖(B x) y‖₊ = ‖B.flip y‖₊ * ‖x‖₊
s : Set X
hs : MeasurableSet s
ε : NNReal
εpos : 0 < ε
δ : NNReal := ε / 3
δpos : 0 < δ
g : X →ₛ E
hg : eLpNorm (f - ⇑g) 1 (μ.transpose B).variation ≤ ↑δ
gmem : MemLp (⇑g) 1 μ.variation
I1 : ∫⁻ (a : X) in s, ‖f a‖ₑ ∂(μ.transpose B).variation ≤ ∫⁻ (a : X) in s, ‖g a‖ₑ ∂(μ.transpose B).variation + ↑δ
I2 :
  ∫⁻ (a : X) in s, ‖g a‖ₑ ∂(μ.transpose B).variation =
    ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i})
ρ : ℝ≥0∞
ρpos : ρ > 0
hρ : ∑ i ∈ g.range, ‖i‖ₑ * ρ ≤ ↑δ
P : E → Finset (Set X)
Pg : ∀ (i : E), ∀ t ∈ P i, t ⊆ ⇑g ⁻¹' {i}
Pdisj : ∀ (i : E), (↑(P i)).PairwiseDisjoint id
Pmeas : ∀ (i : E), ∀ t ∈ P i, MeasurableSet t
hP :
  ∀ (i : E),
    ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i}) ≤
      ‖i‖ₑ * (∑ p ∈ P i, ‖((μ.transpose B).restrict s) p‖ₑ + ρ)
I3 :
  ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i}) ≤
    ∑ i ∈ g.range.sigma P, ‖i.fst‖ₑ * ‖((μ.transpose B).restrict s) i.snd‖ₑ + ↑δ
⊢ ∑ i ∈ g.range.sigma P, ∫⁻ (x : X) in i.snd, ‖g x - f x‖ₑ ∂(μ.transpose B).variation +
      ∑ i ∈ g.range.sigma P, ‖∫ᵛ (x : X) in i.snd, f x ∂[B; μ.restrict s]‖ₑ =
    ∫⁻ (x : X) in ⋃ i ∈ g.range.sigma P, i.snd, ‖g x - f x‖ₑ ∂(μ.transpose B).variation +
      ∑ i ∈ g.range.sigma P, ‖∫ᵛ (x : X) in i.snd, f x ∂[B; μ.restrict s]‖ₑ

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
⊢ IsSemilinearSet hs.setOfFractNe

Tactic:
by

Goal state after:
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : DenselyOrdered β
inst✝¹ : NoMinOrder β
inst✝ : NoMaxOrder β
nonem : Nonempty β
S : Finset α
f : ↥S ↪o β
a : α
⊢ ∃ g, ⇑g ∘ Set.inclusion ⋯ = ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
⊢ ∀ x ∈ Finset.image Prod.snd ({p ∈ ↑f | p.1 < a}), ∀ y ∈ Finset.image Prod.snd ({p ∈ ↑f | a < p.1}), x < y

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensityVec

Goal state before:
pp: X : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
mX : MeasurableSpace X
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
μ : VectorMeasure X F
f : X → E
B : E →L[ℝ] F →L[ℝ] G
inst✝ : CompleteSpace G
hf : μ.Integrable f
hB : ∀ (x : E) (y : F), ‖(B x) y‖₊ = ‖B.flip y‖₊ * ‖x‖₊
s : Set X
hs : MeasurableSet s
ε : NNReal
εpos : 0 < ε
δ : NNReal := ε / 3
δpos : 0 < δ
g : X →ₛ E
hg : eLpNorm (f - ⇑g) 1 (μ.transpose B).variation ≤ ↑δ
gmem : MemLp (⇑g) 1 μ.variation
I1 : ∫⁻ (a : X) in s, ‖f a‖ₑ ∂(μ.transpose B).variation ≤ ∫⁻ (a : X) in s, ‖g a‖ₑ ∂(μ.transpose B).variation + ↑δ
I2 :
  ∫⁻ (a : X) in s, ‖g a‖ₑ ∂(μ.transpose B).variation =
    ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i})
ρ : ℝ≥0∞
ρpos : ρ > 0
hρ : ∑ i ∈ g.range, ‖i‖ₑ * ρ ≤ ↑δ
P : E → Finset (Set X)
Pg : ∀ (i : E), ∀ t ∈ P i, t ⊆ ⇑g ⁻¹' {i}
Pdisj : ∀ (i : E), (↑(P i)).PairwiseDisjoint id
Pmeas : ∀ (i : E), ∀ t ∈ P i, MeasurableSet t
hP :
  ∀ (i : E),
    ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i}) ≤
      ‖i‖ₑ * (∑ p ∈ P i, ‖((μ.transpose B).restrict s) p‖ₑ + ρ)
I3 :
  ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i}) ≤
    ∑ i ∈ g.range.sigma P, ‖i.fst‖ₑ * ‖((μ.transpose B).restrict s) i.snd‖ₑ + ↑δ
⊢ ∫⁻ (x : X) in ⋃ i ∈ g.range.sigma P, i.snd, ‖g x - f x‖ₑ ∂(μ.transpose B).variation +
      ∑ i ∈ g.range.sigma P, ‖∫ᵛ (x : X) in i.snd, f x ∂[B; μ.restrict s]‖ₑ ≤
    ∑ i ∈ g.range.sigma P, ‖∫ᵛ (x : X) in i.snd, f x ∂[B; μ.restrict s]‖ₑ +
      ∫⁻ (x : X), ‖g x - f x‖ₑ ∂(μ.transpose B).variation

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: L : Language
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
⊢ L.age (DirectLimit G f) = ⋃ i, L.age (G i)

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: L : Language
K : Set (Bundled L.Structure)
hn : K.Nonempty
hc : (Quotient.mk' '' K).Countable
fg : ∀ M ∈ K, Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF : ∀ (a : Bundled L.Structure), (∃ x ∈ K, (Quotient.mk' x).out ≈ a) ↔ ∃ y, (F y).out ≈ a
⊢ ∀ (n : ℕ), (F n).out ∈ K

Tactic:
by

Goal state after:
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
⊢ ∃ b, ∀ p ∈ ↑f, cmp p.1 a = cmp p.2 b

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensityVec

Goal state before:
pp: X : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
mX : MeasurableSpace X
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
μ : VectorMeasure X F
f : X → E
B : E →L[ℝ] F →L[ℝ] G
inst✝ : CompleteSpace G
hf : μ.Integrable f
hB : ∀ (x : E) (y : F), ‖(B x) y‖₊ = ‖B.flip y‖₊ * ‖x‖₊
s : Set X
hs : MeasurableSet s
ε : NNReal
εpos : 0 < ε
δ : NNReal := ε / 3
δpos : 0 < δ
g : X →ₛ E
hg : eLpNorm (f - ⇑g) 1 (μ.transpose B).variation ≤ ↑δ
gmem : MemLp (⇑g) 1 μ.variation
I1 : ∫⁻ (a : X) in s, ‖f a‖ₑ ∂(μ.transpose B).variation ≤ ∫⁻ (a : X) in s, ‖g a‖ₑ ∂(μ.transpose B).variation + ↑δ
I2 :
  ∫⁻ (a : X) in s, ‖g a‖ₑ ∂(μ.transpose B).variation =
    ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i})
ρ : ℝ≥0∞
ρpos : ρ > 0
hρ : ∑ i ∈ g.range, ‖i‖ₑ * ρ ≤ ↑δ
P : E → Finset (Set X)
Pg : ∀ (i : E), ∀ t ∈ P i, t ⊆ ⇑g ⁻¹' {i}
Pdisj : ∀ (i : E), (↑(P i)).PairwiseDisjoint id
Pmeas : ∀ (i : E), ∀ t ∈ P i, MeasurableSet t
hP :
  ∀ (i : E),
    ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i}) ≤
      ‖i‖ₑ * (∑ p ∈ P i, ‖((μ.transpose B).restrict s) p‖ₑ + ρ)
I3 :
  ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i}) ≤
    ∑ i ∈ g.range.sigma P, ‖i.fst‖ₑ * ‖((μ.transpose B).restrict s) i.snd‖ₑ + ↑δ
⊢ ∑ i ∈ g.range.sigma P, ‖∫ᵛ (x : X) in i.snd, f x ∂[B; μ.restrict s]‖ₑ +
      ∫⁻ (x : X), ‖g x - f x‖ₑ ∂(μ.transpose B).variation ≤
    ∑ i ∈ g.range.sigma P, ‖∫ᵛ (x : X) in i.snd, f x ∂[B; μ.restrict s]‖ₑ + ↑δ

Tactic:
by

Goal state after:
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : Finset (α × β)
hf : ∀ p ∈ f, ∀ q ∈ f, cmp p.1 q.1 = cmp p.2 q.2
p : β × α
hp : p ∈ Finset.image (⇑(Equiv.prodComm α β)) f
q : β × α
hq : q ∈ Finset.image (⇑(Equiv.prodComm α β)) f
⊢ (Equiv.prodComm α β).symm p ∈ f

Tactic:
by

Goal state after:
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : Finset (α × β)
hf : ∀ p ∈ f, ∀ q ∈ f, cmp p.1 q.1 = cmp p.2 q.2
p : β × α
hp : p ∈ Finset.image (⇑(Equiv.prodComm α β)) f
q : β × α
hq : q ∈ Finset.image (⇑(Equiv.prodComm α β)) f
⊢ (Equiv.prodComm α β).symm q ∈ f

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: case refine_2.succ
L : Language
K : Set (Bundled L.Structure)
hn : K.Nonempty
hc : (Quotient.mk' '' K).Countable
fg : ∀ M ∈ K, Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF : ∀ (a : Bundled L.Structure), (∃ x ∈ K, (Quotient.mk' x).out ≈ a) ↔ ∃ y, (F y).out ≈ a
hF' : ∀ (n : ℕ), (F n).out ∈ K
P : ↑K → ℕ → Bundled L.Structure
hPK : ∀ (N : ↑K) (n : ℕ), P N n ∈ K
hP : ∀ (N : ↑K) (n : ℕ), (fun M N ↦ Nonempty (↑M ↪[L] ↑N)) (↑N) (P N n)
hFP : ∀ (N : ↑K) (n : ℕ), (fun M N ↦ Nonempty (↑M ↪[L] ↑N)) (F (n + 1)).out (P N n)
G : ℕ → ↑K := Nat.rec ⟨(F 0).out, ⋯⟩ fun n N ↦ ⟨P N n, ⋯⟩
f : (i j : ℕ) → i ≤ j → ↑↑(G i) ↪[L] ↑↑(G j) := DirectedSystem.natLERec fun n ↦ Nonempty.some ⋯
N : Bundled L.Structure
KN : N ∈ K
this : (Quotient.mk' N).out ≈ N
n : ℕ
e : ↑(F (n + 1)).out ≃[L] ↑N
⊢ ↑(F (n + 1)).out ↪[L] ↑↑(G (n + 1))

Tactic:
dsimp [G]; exact (hFP _ n).some

Goal state after:
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: L : Language
K : Set (Bundled L.Structure)
hn : K.Nonempty
hc : (Quotient.mk' '' K).Countable
fg : ∀ M ∈ K, Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
⊢ ∃ M, Structure.CG L ↑M ∧ L.age ↑M = K

Tactic:
by

Goal state after:
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
a : α
f : PartialIso α β
⊢ ∃ y ∈ {f | ∃ b, (a, b) ∈ ↑f}, f ≤ y

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
⊢ IsSemilinearSet hs.setOfFloorNeg

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: L : Language
K : Set (Bundled L.Structure)
inst✝ : Countable ((l : ℕ) × L.Functions l)
⊢ (∃ M, Countable ↑M ∧ L.age ↑M = K) ↔
    K.Nonempty ∧
      (∀ (M N : Bundled L.Structure), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)) ∧
        (Quotient.mk' '' K).Countable ∧ (∀ M ∈ K, Structure.FG L ↑M) ∧ Hereditary K ∧ JointEmbedding K

Tactic:
by

Goal state after:
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered α
inst✝² : NoMinOrder α
inst✝¹ : NoMaxOrder α
inst✝ : Nonempty α
b : β
f : PartialIso α β
⊢ ∃ y ∈ {f | ∃ a, (a, b) ∈ ↑f}, f ≤ y

Tactic:
by

Goal state after:
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : Countable α
inst✝¹ : DenselyOrdered β
inst✝ : Nontrivial β
⊢ Nonempty (α ↪o β)

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: L : Language
M : Type w
inst✝² : L.Structure M
M_homog : L.IsUltrahomogeneous M
S : Type u_1
inst✝¹ : L.Structure S
S_FG : Structure.FG L S
T : Type u_2
inst✝ : L.Structure T
h : Nonempty (T ↪[L] M)
f : S ↪[L] M
g : S ↪[L] T
⊢ ∃ f', f = f'.comp g

Tactic:
by

Goal state after:
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹¹ : LinearOrder α
inst✝¹⁰ : LinearOrder β
inst✝⁹ : Countable α
inst✝⁸ : DenselyOrdered α
inst✝⁷ : NoMinOrder α
inst✝⁶ : NoMaxOrder α
inst✝⁵ : Nonempty α
inst✝⁴ : Countable β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
val✝¹ : Encodable α
val✝ : Encodable β
to_cofinal : α ⊕ β → Cofinal (PartialIso α β) := fun p ↦ Sum.recOn p (definedAtLeft β) (definedAtRight α)
our_ideal : Ideal (PartialIso α β) := idealOfCofinals default to_cofinal
F : (a : α) → { b // ∃ f ∈ our_ideal, (a, b) ∈ ↑f } := fun a ↦ funOfIdeal a our_ideal ⋯
G : (b : β) → { a // ∃ f ∈ our_ideal, (a, b) ∈ ↑f } := fun b ↦ invOfIdeal b our_ideal ⋯
a : α
b : β
⊢ cmp a ↑(G b) = cmp (↑(F a)) b

Tactic:
by

Goal state after:
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹¹ : LinearOrder α
inst✝¹⁰ : LinearOrder β
inst✝⁹ : Countable α
inst✝⁸ : DenselyOrdered α
inst✝⁷ : NoMinOrder α
inst✝⁶ : NoMaxOrder α
inst✝⁵ : Nonempty α
inst✝⁴ : Countable β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
⊢ Nonempty (α ≃o β)

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
M_CG : Structure.CG L M
⊢ L.IsUltrahomogeneous M ↔ L.IsExtensionPair M M

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
α : Type w
M : Type w'
n : ℕ
⊢ ∀ (a b : Language.order.Relations n), a = b

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
α : Type w
M : Type w'
n : ℕ
x : Language.order.Relations 0
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
α : Type w
M : Type w'
n : ℕ
⊢ ∀ (a : Language.order.Symbols), a = default

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: ⊢ Language.order.card = 1

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : L.IsOrdered
⊢ ∀ ⦃φ : L.Sentence⦄, φ ∈ L.preorderTheory → BoundedFormula.IsUniversal φ

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
α : Type w
M : Type w'
n : ℕ
inst✝⁵ : L.IsOrdered
inst✝⁴ : L.Structure M
inst✝³ : LE M
inst✝² : Language.order.Structure M
inst✝¹ : Language.order.OrderedStructure M
inst✝ : L.orderLHom.IsExpansionOn M
x : Fin 2 → M
⊢ RelMap leSymb x ↔ x 0 ≤ x 1

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
α : Type w
M : Type w'
n : ℕ
inst✝⁵ : L.IsOrdered
inst✝⁴ : L.Structure M
inst✝³ : LE M
inst✝² : L.OrderedStructure M
inst✝¹ : Language.order.Structure M
inst✝ : Language.order.OrderedStructure M
⊢ ∀ {n : ℕ} (R : Language.order.Relations n) (x : Fin n → M), RelMap (L.orderLHom.onRelation R) x = RelMap R x

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
α : Type w
M : Type w'
n : ℕ
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : LE M
inst✝ : L.OrderedStructure M
t₁ t₂ : L.Term (α ⊕ Fin n)
v : α → M
xs : Fin n → M
⊢ (t₁.le t₂).Realize v xs ↔ realize (Sum.elim v xs) t₁ ≤ realize (Sum.elim v xs) t₂

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
M : Type w'
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : LE M
inst✝ : L.OrderedStructure M
⊢ M ⊨ L.noTopOrderSentence ↔ NoTopOrder M

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
M : Type w'
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : LE M
inst✝ : L.OrderedStructure M
⊢ M ⊨ L.noBotOrderSentence ↔ NoBotOrder M

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
M : Type w'
inst✝⁴ : L.IsOrdered
inst✝³ : L.Structure M
inst✝² : LE M
inst✝¹ : L.OrderedStructure M
inst✝ : M ⊨ L.dlo
⊢ L.noTopOrderSentence ∈ L.dlo

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
M : Type w'
inst✝⁴ : L.IsOrdered
inst✝³ : L.Structure M
inst✝² : LE M
inst✝¹ : L.OrderedStructure M
inst✝ : M ⊨ L.dlo
⊢ L.noTopOrderSentence ∈ L.dlo

Tactic:
by
    simp only [dlo, Set.union_insert, Set.union_singleton, Set.mem_insert_iff, true_or]

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
M : Type w'
inst✝⁴ : L.IsOrdered
inst✝³ : L.Structure M
inst✝² : LE M
inst✝¹ : L.OrderedStructure M
inst✝ : M ⊨ L.dlo
⊢ L.noBotOrderSentence ∈ L.dlo

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
M : Type w'
inst✝⁴ : L.IsOrdered
inst✝³ : L.Structure M
inst✝² : LE M
inst✝¹ : L.OrderedStructure M
inst✝ : M ⊨ L.dlo
⊢ L.noBotOrderSentence ∈ L.dlo

Tactic:
by
    simp only [dlo, Set.union_insert, Set.union_singleton, Set.mem_insert_iff, true_or, or_true]

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
α : Type w
M : Type w'
n : ℕ
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : Preorder M
inst✝ : L.OrderedStructure M
⊢ M ⊨ L.preorderTheory

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
α : Type w
M : Type w'
n : ℕ
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : Preorder M
inst✝ : L.OrderedStructure M
t₁ t₂ : L.Term (α ⊕ Fin n)
v : α → M
xs : Fin n → M
⊢ (t₁.lt t₂).Realize v xs ↔ realize (Sum.elim v xs) t₁ < realize (Sum.elim v xs) t₂

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
M : Type w'
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : Preorder M
inst✝ : L.OrderedStructure M
⊢ M ⊨ L.denselyOrderedSentence ↔ DenselyOrdered M

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
M : Type w'
inst✝⁴ : L.IsOrdered
inst✝³ : L.Structure M
inst✝² : Preorder M
inst✝¹ : L.OrderedStructure M
inst✝ : M ⊨ L.dlo
⊢ L.denselyOrderedSentence ∈ L.dlo

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
M : Type w'
inst✝⁴ : L.IsOrdered
inst✝³ : L.Structure M
inst✝² : Preorder M
inst✝¹ : L.OrderedStructure M
inst✝ : M ⊨ L.dlo
⊢ L.denselyOrderedSentence ∈ L.dlo

Tactic:
by
    simp only [dlo, Set.union_insert, Set.union_singleton, Set.mem_insert_iff, true_or, or_true]

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
α : Type w
M : Type w'
n : ℕ
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : PartialOrder M
inst✝ : L.OrderedStructure M
⊢ M ⊨ L.partialOrderTheory

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
α : Type w
M : Type w'
n : ℕ
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : LinearOrder M
inst✝ : L.OrderedStructure M
⊢ M ⊨ L.linearOrderTheory

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
α : Type w
M : Type w'
n : ℕ
inst✝⁶ : L.IsOrdered
inst✝⁵ : L.Structure M
inst✝⁴ : LinearOrder M
inst✝³ : L.OrderedStructure M
inst✝² : DenselyOrdered M
inst✝¹ : NoTopOrder M
inst✝ : NoBotOrder M
⊢ M ⊨ L.dlo

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
α : Type w
M : Type w'
n : ℕ
inst✝¹ : L.IsOrdered
inst✝ : L.Structure M
⊢ L.OrderedStructure M

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
α : Type w
M : Type w'
n : ℕ
inst✝¹ : L.IsOrdered
inst✝ : L.Structure M
h : M ⊨ L.preorderTheory
⊢ leSymb.reflexive ∈ L.preorderTheory

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
α : Type w
M : Type w'
n : ℕ
inst✝¹ : L.IsOrdered
inst✝ : L.Structure M
h : M ⊨ L.preorderTheory
⊢ leSymb.transitive ∈ L.preorderTheory

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
α : Type w
M : Type w'
n : ℕ
inst✝¹ : L.IsOrdered
inst✝ : L.Structure M
h : M ⊨ L.partialOrderTheory
⊢ leSymb.antisymmetric ∈ L.partialOrderTheory

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
α : Type w
M : Type w'
n : ℕ
inst✝² : L.IsOrdered
inst✝¹ : L.Structure M
h : M ⊨ L.linearOrderTheory
inst✝ : DecidableRel fun a b ↦ RelMap leSymb ![a, b]
⊢ leSymb.total ∈ L.linearOrderTheory

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
α : Type w
M : Type w'
n : ℕ
inst✝⁷ : Language.order.Structure M
inst✝⁶ : LE M
inst✝⁵ : Language.order.OrderedStructure M
N : Type u_1
inst✝⁴ : Language.order.Structure N
inst✝³ : LE N
inst✝² : Language.order.OrderedStructure N
F : Type u_2
inst✝¹ : FunLike F M N
inst✝ : OrderHomClass F M N
⊢ ∀ (φ : F) {n : ℕ} (r : Language.order.Relations n) (x : Fin n → M), RelMap r x → RelMap r (⇑φ ∘ x)

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
α : Type w
M : Type w'
n : ℕ
inst✝⁵ : Language.order.Structure M
inst✝⁴ : LE M
inst✝³ : Language.order.OrderedStructure M
N : Type u_1
inst✝² : Language.order.Structure N
inst✝¹ : LE N
inst✝ : Language.order.OrderedStructure N
F : Type u_2
⊢ ∀ (φ : M ↪o N) {n : ℕ} (r : Language.order.Relations n) (x : Fin n → M), RelMap r (⇑φ ∘ x) ↔ RelMap r x

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
α : Type w
M : Type w'
n : ℕ
inst✝⁷ : Language.order.Structure M
inst✝⁶ : LE M
inst✝⁵ : Language.order.OrderedStructure M
N : Type u_1
inst✝⁴ : Language.order.Structure N
inst✝³ : LE N
inst✝² : Language.order.OrderedStructure N
F : Type u_2
inst✝¹ : EquivLike F M N
inst✝ : OrderIsoClass F M N
⊢ ∀ (φ : F) {n : ℕ} (r : Language.order.Relations n) (x : Fin n → M), RelMap r (⇑φ ∘ x) ↔ RelMap r x

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
M : Type w'
inst✝⁸ : L.IsOrdered
inst✝⁷ : L.Structure M
N : Type u_1
inst✝⁶ : L.Structure N
F : Type u_2
inst✝⁵ : FunLike F M N
inst✝⁴ : L.HomClass F M N
inst✝³ : Preorder M
inst✝² : L.OrderedStructure M
inst✝¹ : Preorder N
inst✝ : L.OrderedStructure N
f : F
a b : M
⊢ a ≤ b → f a ≤ f b

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
inst✝⁸ : L.IsOrdered
M : Type u_1
inst✝⁷ : L.Structure M
inst✝⁶ : LE M
inst✝⁵ : L.OrderedStructure M
N : Type u_2
inst✝⁴ : L.Structure N
inst✝³ : LE N
inst✝² : L.OrderedStructure N
F : Type u_3
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
f : F
a b : M
⊢ f a ≤ f b ↔ a ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
h : L.IsUltrahomogeneous M
⊢ Amalgamation (L.age M)

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
⊢ IsSemilinearSet hs.setOfFloorPos

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
inst✝ : Finite ι
s : Set (ι → ℕ)
hs : IsProperLinearSet s
⊢ IsSemilinearSet sᶜ

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
inst✝ : Finite ι
s : Set (ι → ℕ)
hs : IsSemilinearSet s
⊢ IsSemilinearSet sᶜ

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: M : Type w
inst✝⁴ : Language.order.Structure M
inst✝³ : M ⊨ Language.order.linearOrderTheory
N : Type w'
inst✝² : Language.order.Structure N
inst✝¹ : N ⊨ Language.order.dlo
inst✝ : Nonempty N
S : Language.order.Substructure M
S_fg : S.FG
f : ↥S ↪[Language.order] N
m : M
this✝⁵ : LinearOrder M := Language.order.linearOrderOfModels M
this✝⁴ : LinearOrder N := Language.order.linearOrderOfModels N
this✝³ : DenselyOrdered N
this✝² : NoBotOrder N
this✝¹ : NoTopOrder N
this✝ : NoMinOrder N
this : NoMaxOrder N
hS : (↑S).Finite
g : ↥(insert m hS.toFinset) ↪o N
hg :
  ⇑g ∘ Set.inclusion ⋯ =
    ⇑(RelEmbedding.trans (OrderIso.setCongr ↑hS.toFinset ↑S ⋯).toOrderEmbedding (OrderEmbedding.ofStrictMono ⇑f ⋯))
⊢ ↑((Substructure.closure Language.order).toFun {m} ⊔ S) = ↑(insert m hS.toFinset)

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: L : Language
K : Set (Bundled L.Structure)
M : Type w
inst✝⁴ : L.Structure M
N : Type w
inst✝³ : L.Structure N
inst✝² : Countable ((l : ℕ) × L.Functions l)
inst✝¹ : Countable M
inst✝ : Countable N
hM : IsFraisseLimit K M
hN : IsFraisseLimit K N
f : M ≃ₚ[L] N
f_FG : f.dom.FG
m : M
S : L.Substructure M := f.dom ⊔ (closure L).toFun {m}
S_FG : S.FG
⊢ { α := ↥S, str := inferInstance } ∈ L.age N

Tactic:
by

Goal state after: