mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: case mp
M : Type u_1
N : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
s : Set M
F : Type u_6
inst✝¹ : EquivLike F M N
inst✝ : AddEquivClass F M N
f : F
⊢ IsSemilinearSet (⇑f '' s) → IsSemilinearSet s

pp: case mpr
M : Type u_1
N : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
s : Set M
F : Type u_6
inst✝¹ : EquivLike F M N
inst✝ : AddEquivClass F M N
f : F
⊢ IsSemilinearSet s → IsSemilinearSet (⇑f '' s)

Tactic:
<;>

Goal state after:
case mp
M : Type u_1
N : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
s : Set M
F : Type u_6
inst✝¹ : EquivLike F M N
inst✝ : AddEquivClass F M N
f : F
⊢ IsSemilinearSet (⇑f '' s) → IsSemilinearSet s

case mpr
M : Type u_1
N : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
s : Set M
F : Type u_6
inst✝¹ : EquivLike F M N
inst✝ : AddEquivClass F M N
f : F
⊢ IsSemilinearSet s → IsSemilinearSet (⇑f '' s)
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: case pos
X : Type u_2
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
β : Type u_8
f : β → X → E
s : Set β
b : β
hb : b ∈ s
⊢ ∫ᵛ (y : X), s.indicator (fun x ↦ f x y) b ∂[B; μ] = s.indicator (fun x ↦ ∫ᵛ (y : X), f x y ∂[B; μ]) b

pp: case neg
X : Type u_2
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
β : Type u_8
f : β → X → E
s : Set β
b : β
hb : b ∉ s
⊢ ∫ᵛ (y : X), s.indicator (fun x ↦ f x y) b ∂[B; μ] = s.indicator (fun x ↦ ∫ᵛ (y : X), f x y ∂[B; μ]) b

Tactic:
<;>

Goal state after:
case pos
X : Type u_2
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
β : Type u_8
f : β → X → E
s : Set β
b : β
hb : b ∈ s
⊢ ∫ᵛ (y : X), s.indicator (fun x ↦ f x y) b ∂[B; μ] = s.indicator (fun x ↦ ∫ᵛ (y : X), f x y ∂[B; μ]) b

case neg
X : Type u_2
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
β : Type u_8
f : β → X → E
s : Set β
b : β
hb : b ∉ s
⊢ ∫ᵛ (y : X), s.indicator (fun x ↦ f x y) b ∂[B; μ] = s.indicator (fun x ↦ ∫ᵛ (y : X), f x y ∂[B; μ]) b
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability

Goal state before:
pp: case e'_8.last
α : Type u_1
A : Set ℕ
inst✝ : Finite α
n✝ : ℕ
this : Fintype α
n : ℕ
φ : presburger[[↑A]].BoundedFormula α (n + 1)
e : (α ⊕ Fin n) ⊕ Fin 1 ≃ α ⊕ Fin (n + 1) :=
  (Equiv.sumAssoc α (Fin n) (Fin 1)).trans ((_root_.Equiv.refl α).sumCongr finSumFinEquiv)
ih : IsSemilinearSet (⇑(LinearEquiv.funCongrLeft ℕ ℕ e) '' {v | φ.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)})
x✝ : α ⊕ Fin n → ℕ
a✝ : ℕ
⊢ Fin.snoc (x✝ ∘ Sum.inr) a✝ (Fin.last n) = ((Sum.elim x✝ (Fin.cons a✝ finZeroElim) ∘ ⇑e.symm) ∘ Sum.inr) (Fin.last n)

pp: case e'_8.cast
α : Type u_1
A : Set ℕ
inst✝ : Finite α
n✝ : ℕ
this : Fintype α
n : ℕ
φ : presburger[[↑A]].BoundedFormula α (n + 1)
e : (α ⊕ Fin n) ⊕ Fin 1 ≃ α ⊕ Fin (n + 1) :=
  (Equiv.sumAssoc α (Fin n) (Fin 1)).trans ((_root_.Equiv.refl α).sumCongr finSumFinEquiv)
ih : IsSemilinearSet (⇑(LinearEquiv.funCongrLeft ℕ ℕ e) '' {v | φ.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)})
x✝ : α ⊕ Fin n → ℕ
a✝ : ℕ
i✝ : Fin n
⊢ Fin.snoc (x✝ ∘ Sum.inr) a✝ i✝.castSucc = ((Sum.elim x✝ (Fin.cons a✝ finZeroElim) ∘ ⇑e.symm) ∘ Sum.inr) i✝.castSucc

Tactic:
<;>

Goal state after:
case e'_8.last
α : Type u_1
A : Set ℕ
inst✝ : Finite α
n✝ : ℕ
this : Fintype α
n : ℕ
φ : presburger[[↑A]].BoundedFormula α (n + 1)
e : (α ⊕ Fin n) ⊕ Fin 1 ≃ α ⊕ Fin (n + 1) :=
  (Equiv.sumAssoc α (Fin n) (Fin 1)).trans ((_root_.Equiv.refl α).sumCongr finSumFinEquiv)
ih : IsSemilinearSet (⇑(LinearEquiv.funCongrLeft ℕ ℕ e) '' {v | φ.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)})
x✝ : α ⊕ Fin n → ℕ
a✝ : ℕ
⊢ Fin.snoc (x✝ ∘ Sum.inr) a✝ (Fin.last n) = ((Sum.elim x✝ (Fin.cons a✝ finZeroElim) ∘ ⇑e.symm) ∘ Sum.inr) (Fin.last n)

case e'_8.cast
α : Type u_1
A : Set ℕ
inst✝ : Finite α
n✝ : ℕ
this : Fintype α
n : ℕ
φ : presburger[[↑A]].BoundedFormula α (n + 1)
e : (α ⊕ Fin n) ⊕ Fin 1 ≃ α ⊕ Fin (n + 1) :=
  (Equiv.sumAssoc α (Fin n) (Fin 1)).trans ((_root_.Equiv.refl α).sumCongr finSumFinEquiv)
ih : IsSemilinearSet (⇑(LinearEquiv.funCongrLeft ℕ ℕ e) '' {v | φ.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)})
x✝ : α ⊕ Fin n → ℕ
a✝ : ℕ
i✝ : Fin n
⊢ Fin.snoc (x✝ ∘ Sum.inr) a✝ i✝.castSucc = ((Sum.elim x✝ (Fin.cons a✝ finZeroElim) ∘ ⇑e.symm) ∘ Sum.inr) i✝.castSucc
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: case neg
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
ψ : L.BoundedFormula α n
v : α → M
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsPrenex
ih :
  ∀ {φ : L.BoundedFormula α (n✝ + 1)},
    φ.IsQF → ∀ {xs : Fin (n✝ + 1) → M}, (φ.toPrenexImpRight φ✝).Realize v xs ↔ (φ ⟹ φ✝).Realize v xs
φ : L.BoundedFormula α n✝
hφ : φ.IsQF
xs : Fin n✝ → M
h' : φ.Realize v xs → ∃ a, φ✝.Realize v (snoc xs a)
h : ¬φ.Realize v xs
⊢ ∃ a, φ.Realize v xs → φ✝.Realize v (snoc xs a)

Tactic:
· inhabit M
        exact ⟨default, fun h'' => (h h'').elim⟩

Goal state after:
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: case mp.inr
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
S : Set M
Scount : S.Countable
hS : (closure L).toFun S = N
h : (↑N).Nonempty
f : ℕ → M
h' : S ∪ {h.some} = range f
⊢ {h.some} ⊆ ↑N

Tactic:
exact singleton_subset_iff.2 h.some_mem

Goal state after:
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: L : Language
M : Type u_1
inst✝ : L.Structure M
⊢ ⊤.FG ↔ ∃ S, S.Finite ∧ (closure L).toFun S = ⊤

Tactic:
Substructure.fg_def

Goal state after:
L : Language
M : Type u_1
inst✝ : L.Structure M
⊢ (∃ S, S.Finite ∧ (closure L).toFun S = ⊤) ↔ ∃ S, S.Finite ∧ (closure L).toFun S = ⊤
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case refine_1
ι : Type u_3
s : Set (ι → ℕ)
v : ι → ℕ
n : ℕ
x✝ : ∃ f, s = v +ᵥ range ⇑f
f : (Fin n → ℕ) →+ ι → ℕ
hf : s = v +ᵥ range ⇑f
⊢ s = {x | ∃ x_1, v + LinearMap.toMatrix' f.toNatLinearMap *ᵥ x_1 = x}

pp: case refine_2
ι : Type u_3
s : Set (ι → ℕ)
v : ι → ℕ
n : ℕ
x✝ : ∃ A, s = {x | ∃ x_1, v + A *ᵥ x_1 = x}
A : Matrix ι (Fin n) ℕ
hA : s = {x | ∃ x_1, v + A *ᵥ x_1 = x}
⊢ s = v +ᵥ range ⇑↑A.mulVecLin

Tactic:
<;>

Goal state after:
case refine_1
ι : Type u_3
s : Set (ι → ℕ)
v : ι → ℕ
n : ℕ
x✝ : ∃ f, s = v +ᵥ range ⇑f
f : (Fin n → ℕ) →+ ι → ℕ
hf : s = v +ᵥ range ⇑f
⊢ s = {x | ∃ x_1, v + LinearMap.toMatrix' f.toNatLinearMap *ᵥ x_1 = x}

case refine_2
ι : Type u_3
s : Set (ι → ℕ)
v : ι → ℕ
n : ℕ
x✝ : ∃ A, s = {x | ∃ x_1, v + A *ᵥ x_1 = x}
A : Matrix ι (Fin n) ℕ
hA : s = {x | ∃ x_1, v + A *ᵥ x_1 = x}
⊢ s = v +ᵥ range ⇑↑A.mulVecLin
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case refine_1
ι : Type u_3
s : Set (ι → ℕ)
v : ι → ℕ
n : ℕ
x✝¹ : ∃ f, s = v +ᵥ range ⇑f
f : (Fin n → ℕ) →+ ι → ℕ
hf : s = v +ᵥ range ⇑f
x✝ : ι → ℕ
⊢ x✝ ∈ s ↔ x✝ ∈ {x | ∃ x_1, v + LinearMap.toMatrix' f.toNatLinearMap *ᵥ x_1 = x}

pp: case refine_2
ι : Type u_3
s : Set (ι → ℕ)
v : ι → ℕ
n : ℕ
x✝¹ : ∃ A, s = {x | ∃ x_1, v + A *ᵥ x_1 = x}
A : Matrix ι (Fin n) ℕ
hA : s = {x | ∃ x_1, v + A *ᵥ x_1 = x}
x✝ : ι → ℕ
⊢ x✝ ∈ s ↔ x✝ ∈ v +ᵥ range ⇑↑A.mulVecLin

Tactic:
<;>

Goal state after:
case refine_1
ι : Type u_3
s : Set (ι → ℕ)
v : ι → ℕ
n : ℕ
x✝¹ : ∃ f, s = v +ᵥ range ⇑f
f : (Fin n → ℕ) →+ ι → ℕ
hf : s = v +ᵥ range ⇑f
x✝ : ι → ℕ
⊢ x✝ ∈ s ↔ x✝ ∈ {x | ∃ x_1, v + LinearMap.toMatrix' f.toNatLinearMap *ᵥ x_1 = x}

case refine_2
ι : Type u_3
s : Set (ι → ℕ)
v : ι → ℕ
n : ℕ
x✝¹ : ∃ A, s = {x | ∃ x_1, v + A *ᵥ x_1 = x}
A : Matrix ι (Fin n) ℕ
hA : s = {x | ∃ x_1, v + A *ᵥ x_1 = x}
x✝ : ι → ℕ
⊢ x✝ ∈ s ↔ x✝ ∈ v +ᵥ range ⇑↑A.mulVecLin
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: M : Type u_1
ι : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Finite ι
F : Type u_5
inst✝¹ : FunLike F (ι → ℕ) M
inst✝ : AddMonoidHomClass F (ι → ℕ) M
f : F
S : Set (Set M)
hS : S.Finite
hS' : ∀ t ∈ S, IsLinearSet t
⊢ IsSemilinearSet (⇑f ⁻¹' ⋃₀ S)

Tactic:
simp_rw [sUnion_eq_biUnion, preimage_iUnion]

Goal state after:
M : Type u_1
ι : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Finite ι
F : Type u_5
inst✝¹ : FunLike F (ι → ℕ) M
inst✝ : AddMonoidHomClass F (ι → ℕ) M
f : F
S : Set (Set M)
hS : S.Finite
hS' : ∀ t ∈ S, IsLinearSet t
⊢ IsSemilinearSet (⋃ i ∈ S, ⇑f ⁻¹' i)
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case refine_1
M : Type u_1
inst✝ : AddCommMonoid M
P₁ : AddSubmonoid M
s₁' : Set ↥P₁
hP₁ : P₁.FG
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val '' s₁')
P₂ : AddSubmonoid M
s₂' : Set ↥P₂
hP₂ : P₂.FG
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val '' s₂')
⊢ Subtype.val '' s₁' = Subtype.val '' ⇑(AddSubmonoid.inclusion ⋯) '' s₁'

pp: case refine_2
M : Type u_1
inst✝ : AddCommMonoid M
P₁ : AddSubmonoid M
s₁' : Set ↥P₁
hP₁ : P₁.FG
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val '' s₁')
P₂ : AddSubmonoid M
s₂' : Set ↥P₂
hP₂ : P₂.FG
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val '' s₂')
⊢ Subtype.val '' s₂' = Subtype.val '' ⇑(AddSubmonoid.inclusion ⋯) '' s₂'

Tactic:
<;>

Goal state after:
case refine_1
M : Type u_1
inst✝ : AddCommMonoid M
P₁ : AddSubmonoid M
s₁' : Set ↥P₁
hP₁ : P₁.FG
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val '' s₁')
P₂ : AddSubmonoid M
s₂' : Set ↥P₂
hP₂ : P₂.FG
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val '' s₂')
⊢ Subtype.val '' s₁' = Subtype.val '' ⇑(AddSubmonoid.inclusion ⋯) '' s₁'

case refine_2
M : Type u_1
inst✝ : AddCommMonoid M
P₁ : AddSubmonoid M
s₁' : Set ↥P₁
hP₁ : P₁.FG
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val '' s₁')
P₂ : AddSubmonoid M
s₂' : Set ↥P₂
hP₂ : P₂.FG
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val '' s₂')
⊢ Subtype.val '' s₂' = Subtype.val '' ⇑(AddSubmonoid.inclusion ⋯) '' s₂'
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case hs₁
M : Type u_1
inst✝ : AddCommMonoid M
P : AddSubmonoid M
s₁' s₂' : Set ↥P
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val '' s₂')
n : ℕ
f : (Fin n → ℕ) →+ ↥P
hf : Function.Surjective ⇑f
⊢ IsSemilinearSet (⇑f ⁻¹' s₁')

pp: case hs₂
M : Type u_1
inst✝ : AddCommMonoid M
P : AddSubmonoid M
s₁' s₂' : Set ↥P
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val '' s₂')
n : ℕ
f : (Fin n → ℕ) →+ ↥P
hf : Function.Surjective ⇑f
⊢ IsSemilinearSet (⇑f ⁻¹' s₂')

Tactic:
<;>

Goal state after:
case hs₁
M : Type u_1
inst✝ : AddCommMonoid M
P : AddSubmonoid M
s₁' s₂' : Set ↥P
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val '' s₂')
n : ℕ
f : (Fin n → ℕ) →+ ↥P
hf : Function.Surjective ⇑f
⊢ IsSemilinearSet (⇑f ⁻¹' s₁')

case hs₂
M : Type u_1
inst✝ : AddCommMonoid M
P : AddSubmonoid M
s₁' s₂' : Set ↥P
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val '' s₂')
n : ℕ
f : (Fin n → ℕ) →+ ↥P
hf : Function.Surjective ⇑f
⊢ IsSemilinearSet (⇑f ⁻¹' s₂')
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case hs₁
M : Type u_1
inst✝ : AddCommMonoid M
P : AddSubmonoid M
s₁' s₂' : Set ↥P
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val '' s₂')
n : ℕ
f : (Fin n → ℕ) →+ ↥P
hf : Function.Surjective ⇑f
⊢ IsSemilinearSet s₁'

pp: case hs₂
M : Type u_1
inst✝ : AddCommMonoid M
P : AddSubmonoid M
s₁' s₂' : Set ↥P
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val '' s₂')
n : ℕ
f : (Fin n → ℕ) →+ ↥P
hf : Function.Surjective ⇑f
⊢ IsSemilinearSet s₂'

Tactic:
<;>

Goal state after:
case hs₁
M : Type u_1
inst✝ : AddCommMonoid M
P : AddSubmonoid M
s₁' s₂' : Set ↥P
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val '' s₂')
n : ℕ
f : (Fin n → ℕ) →+ ↥P
hf : Function.Surjective ⇑f
⊢ IsSemilinearSet s₁'

case hs₂
M : Type u_1
inst✝ : AddCommMonoid M
P : AddSubmonoid M
s₁' s₂' : Set ↥P
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val '' s₂')
n : ℕ
f : (Fin n → ℕ) →+ ↥P
hf : Function.Surjective ⇑f
⊢ IsSemilinearSet s₂'
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x✝² : ι → ℚ
x✝¹ x✝ : ι
⊢ toRatVec ((Pi.basisFun ℕ ι) x✝¹) x✝ = (Pi.basisFun ℚ ι) x✝¹ x✝

Tactic:
simp [toRatVec, Pi.basisFun_apply, Pi.single_apply]

Goal state after:
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: case refl.le_fg
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : ↥g.1 ≃[L] ↥cod_f
h :
  ∀ (x : M) (h : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom),
    { dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype
        ({ dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv ⟨x, h⟩) =
      g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)
⊢ { dom := g.1, cod := cod_f, toEquiv := equiv_f } ≤ g

pp: case refl.le_gf
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : ↥g.1 ≃[L] ↥cod_f
h :
  ∀ (x : M) (h : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom),
    { dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype
        ({ dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv ⟨x, h⟩) =
      g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)
⊢ g ≤ { dom := g.1, cod := cod_f, toEquiv := equiv_f }

Tactic:
<;>

Goal state after:
case refl.le_fg
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : ↥g.1 ≃[L] ↥cod_f
h :
  ∀ (x : M) (h : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom),
    { dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype
        ({ dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv ⟨x, h⟩) =
      g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)
⊢ { dom := g.1, cod := cod_f, toEquiv := equiv_f } ≤ g

case refl.le_gf
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : ↥g.1 ≃[L] ↥cod_f
h :
  ∀ (x : M) (h : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom),
    { dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype
        ({ dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv ⟨x, h⟩) =
      g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)
⊢ g ≤ { dom := g.1, cod := cod_f, toEquiv := equiv_f }
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
x✝ : ↑hs.basisSet
| ⌊(hs.basis.repr (toRatVec x - toRatVec hs.base)) x✝⌋ • toRatVec ↑x✝

Tactic:
← Int.cast_smul_eq_zsmul ℚ

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
x✝ : ↑hs.basisSet
| ↑⌊(hs.basis.repr (toRatVec x - toRatVec hs.base)) x✝⌋ • toRatVec ↑x✝
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: case refine_1
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
⊢ L.IsExtensionPair M N → ∀ (f : L.FGEquiv N M) (m : M), ∃ g, m ∈ (↑g).cod ∧ f ≤ g

pp: case refine_2
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
⊢ (∀ (f : L.FGEquiv N M) (m : M), ∃ g, m ∈ (↑g).cod ∧ f ≤ g) → L.IsExtensionPair M N

Tactic:
<;>

Goal state after:
case refine_1
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
⊢ L.IsExtensionPair M N → ∀ (f : L.FGEquiv N M) (m : M), ∃ g, m ∈ (↑g).cod ∧ f ≤ g

case refine_2
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
⊢ (∀ (f : L.FGEquiv N M) (m : M), ∃ g, m ∈ (↑g).cod ∧ f ≤ g) → L.IsExtensionPair M N
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case e'_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
i : ι → ℕ
hi : i ∈ hs.fundamentalDomain \ {hs.base}
this : Fintype ι
x✝ : (ι ⊕ ι) ⊕ ι → ℕ
⊢ (x✝ ∘ Sum.inl) ∘ Sum.inl + x✝ ∘ Sum.inr = 0 + (fromCols 1 0).fromCols 1 *ᵥ x✝

pp: case e'_3
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
i : ι → ℕ
hi : i ∈ hs.fundamentalDomain \ {hs.base}
this : Fintype ι
x✝ : (ι ⊕ ι) ⊕ ι → ℕ
⊢ i + (x✝ ∘ Sum.inl) ∘ Sum.inr = i + (fromCols 0 1).fromCols 0 *ᵥ x✝

Tactic:
<;>

Goal state after:
case e'_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
i : ι → ℕ
hi : i ∈ hs.fundamentalDomain \ {hs.base}
this : Fintype ι
x✝ : (ι ⊕ ι) ⊕ ι → ℕ
⊢ (x✝ ∘ Sum.inl) ∘ Sum.inl + x✝ ∘ Sum.inr = 0 + (fromCols 1 0).fromCols 1 *ᵥ x✝

case e'_3
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
i : ι → ℕ
hi : i ∈ hs.fundamentalDomain \ {hs.base}
this : Fintype ι
x✝ : (ι ⊕ ι) ⊕ ι → ℕ
⊢ i + (x✝ ∘ Sum.inl) ∘ Sum.inr = i + (fromCols 0 1).fromCols 0 *ᵥ x✝
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 = ⟦a⟧) ↔ ∃ y, F y = ⟦a⟧
⊢ ∃ M, Structure.CG L ↑M ∧ L.age ↑M = K

Tactic:
Quotient.eq_mk_iff_out

Goal state after:
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
⊢ ∃ M, Structure.CG L ↑M ∧ L.age ↑M = K
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
a : α
f : PartialIso α β
b : β
a_b : ∀ p ∈ ↑f, cmp p.1 a = cmp p.2 b
q : α × β
hq : q = (a, b) ∨ q ∈ ↑f
⊢ cmp (a, b).1 q.1 = cmp (a, b).2 q.2

pp: case inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
a : α
f : PartialIso α β
b : β
a_b : ∀ p ∈ ↑f, cmp p.1 a = cmp p.2 b
p q : α × β
hq : q = (a, b) ∨ q ∈ ↑f
pf : p ∈ ↑f
⊢ cmp p.1 q.1 = cmp p.2 q.2

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
a : α
f : PartialIso α β
b : β
a_b : ∀ p ∈ ↑f, cmp p.1 a = cmp p.2 b
q : α × β
hq : q = (a, b) ∨ q ∈ ↑f
⊢ cmp (a, b).1 q.1 = cmp (a, b).2 q.2

case inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
a : α
f : PartialIso α β
b : β
a_b : ∀ p ∈ ↑f, cmp p.1 a = cmp p.2 b
p q : α × β
hq : q = (a, b) ∨ q ∈ ↑f
pf : p ∈ ↑f
⊢ cmp p.1 q.1 = cmp p.2 q.2
Module: Mathlib.Order.CountableDenseLinearOrder

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

Tactic:
simp only [cmp_self_eq_eq]

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

Goal state before:
pp: case e'_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
i : ↑hs.basisSet
this : Fintype ι
x✝ : ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ
⊢ ((x✝ ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inl + ↑i + ((x✝ ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inr + x✝ ∘ Sum.inr =
    ↑i + ((fromCols 1 1).fromCols 0).fromCols 1 *ᵥ x✝

pp: case e'_3
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
i : ↑hs.basisSet
this : Fintype ι
x✝ : ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ
⊢ hs.base + (x✝ ∘ Sum.inl) ∘ Sum.inr = hs.base + ((fromCols 0 0).fromCols 1).fromCols 0 *ᵥ x✝

Tactic:
<;>

Goal state after:
case e'_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
i : ↑hs.basisSet
this : Fintype ι
x✝ : ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ
⊢ ((x✝ ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inl + ↑i + ((x✝ ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inr + x✝ ∘ Sum.inr =
    ↑i + ((fromCols 1 1).fromCols 0).fromCols 1 *ᵥ x✝

case e'_3
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
i : ↑hs.basisSet
this : Fintype ι
x✝ : ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ
⊢ hs.base + (x✝ ∘ Sum.inl) ∘ Sum.inr = hs.base + ((fromCols 0 0).fromCols 1).fromCols 0 *ᵥ x✝
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case e'_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
i : ↑hs.basisSet
hi : i ∈ {i | ↑i ∉ hs.periods}
this : Fintype ι
x✝ : ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ
⊢ ((x✝ ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inl + x✝ ∘ Sum.inr = 0 + ((fromCols 1 0).fromCols 0).fromCols 1 *ᵥ x✝

pp: case e'_3
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
i : ↑hs.basisSet
hi : i ∈ {i | ↑i ∉ hs.periods}
this : Fintype ι
x✝ : ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ
⊢ hs.base + ↑i + ((x✝ ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inr + (x✝ ∘ Sum.inl) ∘ Sum.inr =
    hs.base + ↑i + ((fromCols 0 1).fromCols 1).fromCols 0 *ᵥ x✝

Tactic:
<;>

Goal state after:
case e'_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
i : ↑hs.basisSet
hi : i ∈ {i | ↑i ∉ hs.periods}
this : Fintype ι
x✝ : ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ
⊢ ((x✝ ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inl + x✝ ∘ Sum.inr = 0 + ((fromCols 1 0).fromCols 0).fromCols 1 *ᵥ x✝

case e'_3
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
i : ↑hs.basisSet
hi : i ∈ {i | ↑i ∉ hs.periods}
this : Fintype ι
x✝ : ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ
⊢ hs.base + ↑i + ((x✝ ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inr + (x✝ ∘ Sum.inl) ∘ Sum.inr =
    hs.base + ↑i + ((fromCols 0 1).fromCols 1).fromCols 0 *ᵥ x✝