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

Goal state before:
pp: case _2
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : {x | x ∈ s ∧ x < k}.Finite
h₂ : {x | x ∈ s ∧ k ≤ x ∧ x < k + p}.Finite
x : ℕ
hx : x ∈ s
hx' : k ≤ x
⊢ k ≤ k + (x - k) % p

Tactic:
grind

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

Goal state before:
pp: case mpr.inr.zero
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : {x | x ∈ s ∧ x < k}.Finite
h₂ : {x | x ∈ s ∧ k ≤ x ∧ x < k + p}.Finite
x : ℕ
right✝ : x ∈ s ∧ x < k + p
hx : x ∈ s
hx' : k ≤ x
⊢ x + 0 * p ∈ s

Tactic:
grind

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

Goal state before:
pp: case mpr.inr.succ
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : {x | x ∈ s ∧ x < k}.Finite
h₂ : {x | x ∈ s ∧ k ≤ x ∧ x < k + p}.Finite
x : ℕ
right✝ : x ∈ s ∧ x < k + p
hx : x ∈ s
hx' : k ≤ x
n✝ : ℕ
a✝ : x + n✝ * p ∈ s
⊢ x + (n✝ + 1) * p ∈ s

Tactic:
grind

Goal state after:
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability

Goal state before:
pp: case func.inl.one
α : Type u_1
A : Set ℕ
inst✝ : Fintype α
ts : Fin 0 → presburger[[↑A]].Term α
k : Fin 0 → ℕ
u : Fin 0 → α → ℕ
ih : ∀ (a : Fin 0) (v : α → ℕ), Term.realize v (ts a) = k a + u a ⬝ᵥ v
⊢ ∃ k u, ∀ (v : α → ℕ), (Structure.funMap (Sum.inl presburgerFunc.one) fun i ↦ Term.realize v (ts i)) = k + u ⬝ᵥ v

Tactic:
refine ⟨1, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInl]
        simp [ih]

Goal state after:
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability

Goal state before:
pp: case func.inr.zero
α : Type u_1
A : Set ℕ
inst✝ : Fintype α
ts : Fin 0 → presburger[[↑A]].Term α
ih : ∀ (a : Fin 0), ∃ k u, ∀ (v : α → ℕ), Term.realize v (ts a) = k + u ⬝ᵥ v
f : (constantsOn ↑A).Functions 0
v : α → ℕ
⊢ ↑(presburger.con f) = ↑f

Tactic:
rfl

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

Goal state before:
pp: M : Type u_1
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : CanonicallyOrderedAdd M
s : Set M
hs : IsSlice s
hs' : s.Nonempty
f : M → AddSubmonoid M :=
  fun x ↦ if hx : x ∈ s then { carrier := {y | x + y ∈ s}, add_mem' := ⋯, zero_mem' := ⋯ } else ⊥
hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s
g : M → AddSemigroupIdeal M := fun x ↦ AddSemigroupIdeal.closure (↑(f x) \ {0})
hg : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y
a : M
ha : MaximalFor (fun x ↦ x ∈ s) g a
x : M
⊢ (x ∈ s ∧ ∃ c, x = a + c) ↔ ∃ y, a + y ∈ s ∧ a + y = x

Tactic:
grind

Goal state after:
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability

Goal state before:
pp: α : 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)})
⊢ {v | ∀ (x : ℕ), φ.Realize (v ∘ Sum.inl) (Fin.snoc (v ∘ Sum.inr) x)} =
    {a |
      ∀ (a_1 : ℕ),
        (LinearEquiv.funCongrLeft ℕ ℕ e.symm) (Sum.elim a (Fin.cons a_1 finZeroElim)) ∈
          {v | φ.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)}}

Tactic:
mem_ofPred,

Goal state after:
α : 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)})
⊢ {v | ∀ (x : ℕ), φ.Realize (v ∘ Sum.inl) (Fin.snoc (v ∘ Sum.inr) x)} =
    {a |
      ∀ (a_1 : ℕ),
        φ.Realize ((LinearEquiv.funCongrLeft ℕ ℕ e.symm) (Sum.elim a (Fin.cons a_1 finZeroElim)) ∘ Sum.inl)
          ((LinearEquiv.funCongrLeft ℕ ℕ e.symm) (Sum.elim a (Fin.cons a_1 finZeroElim)) ∘ Sum.inr)}
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability

Goal state before:
pp: case pos
A : Set ℕ
hmul : A.Definable presburger {v | v 0 = v 1 * v 2}
k p : ℕ
hp : p > 0
x : ℕ
h₁ : x * x = max k p * max k p + p
h₂ : x * x ≤ max k p * max k p
⊢ False

Tactic:
grind

Goal state after:
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability

Goal state before:
pp: case neg
A : Set ℕ
hmul : A.Definable presburger {v | v 0 = v 1 * v 2}
k p : ℕ
hp : p > 0
x : ℕ
h₁ : x * x = max k p * max k p + p
h₂ : (max k p + 1) * (max k p + 1) ≤ x * x
⊢ False

Tactic:
grind

Goal state after:
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: L : Language
M : Type u_1
inst✝ : L.Structure M
s : L.Substructure M
h : Finite ↥s
⊢ (closure L).toFun ↑(Finite.toFinset h) = s

Tactic:
simp only [Finite.coe_toFinset, closure_eq]

Goal state after:
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: case mp
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
⊢ (∃ S, S.Countable ∧ (closure L).toFun S = N) → ↑N = ∅ ∨ ∃ s, (closure L).toFun (range s) = N

Tactic:
rintro ⟨S, Scount, hS⟩
    rcases eq_empty_or_nonempty (N : Set M) with h | h
    · exact Or.intro_left _ h
    obtain ⟨f, h'⟩ :=
      (Scount.union (Set.countable_singleton h.some)).exists_eq_range
        (singleton_nonempty h.some).inr
    refine Or.intro_right _ ⟨f, ?_⟩
    rw [← h', closure_union, hS, sup_eq_left, closure_le]
    exact singleton_subset_iff.2 h.some_mem

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

Goal state before:
pp: ι : Type u_1
inst✝ : Finite ι
t : Finset ι
ih : ∀ t_1 ⊂ t, ∀ {s : Set (ι → ℕ)}, IsSlice s → ∀ (a : ι → ℕ), (∀ x ∈ s, ∀ i ∉ t_1, x i = a i) → IsSemilinearSet s
s : Set (ι → ℕ)
hs : IsSlice s
a : ι → ℕ
ht : ∀ x ∈ s, ∀ i ∉ t, x i = a i
hs' : s.Nonempty
x : ι → ℕ
hx : x ∈ s
hx' : IsSemilinearSet {y | y ∈ s ∧ x ≤ y}
y : ι → ℕ
⊢ y ∈ s ↔ (y ∈ s ∧ ∀ (i : ι), x i ≤ y i) ∨ ∃ i, ∃ (_ : i ∈ t), ∃ i_1, ∃ (_ : i_1 < x i), y ∈ s ∧ y i = i_1

Tactic:
grind

Goal state after:
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: case falsum
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst✝⁴ : L.Structure M
N : Type u_2
inst✝³ : L.Structure N
F : Type u_3
inst✝² : FunLike F M N
inst✝¹ : EmbeddingLike F M N
inst✝ : L.StrongHomClass F M N
φ : L.BoundedFormula α n
f : F
v : α → M
xs : Fin n → M
⊢ BoundedFormula.falsum.Realize (⇑f ∘ v) (⇑f ∘ xs) ↔ BoundedFormula.falsum.Realize v xs

Tactic:
rfl

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

Goal state before:
pp: ι : Type u_3
inst✝ : Finite ι
this : Fintype ι
u : ι → ℕ
n : ℕ
A : Matrix ι (Fin n) ℕ
v : ι → ℕ
m : ℕ
B : Matrix ι (Fin m) ℕ
⊢ IsSemilinearSet ({x | ∃ x_1, u + A *ᵥ x_1 = x} ∩ {x | ∃ x_1, v + B *ᵥ x_1 = x})

Tactic:
simp_rw [← ofPred_and, exists_and_exists_comm]

Goal state after:
ι : Type u_3
inst✝ : Finite ι
this : Fintype ι
u : ι → ℕ
n : ℕ
A : Matrix ι (Fin n) ℕ
v : ι → ℕ
m : ℕ
B : Matrix ι (Fin m) ℕ
⊢ IsSemilinearSet {a | ∃ a_1 b, u + A *ᵥ a_1 = a ∧ v + B *ᵥ b = a}
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
dom_le_dom : f.dom ≤ g.dom
le_cod : f.cod ≤ g.cod
h_eq : ∀ (x : ↥f.dom), (inclusion le_cod) (f.toEquiv x) = g.toEquiv ((inclusion dom_le_dom) x)
x✝ : ↥f.dom
⊢ g.cod.subtype ((inclusion le_cod) (f.toEquiv x✝)) = (f.cod.subtype.comp f.toEquiv.toEmbedding) x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: L : Language
ι : Type v
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝² : IsDirectedOrder ι
inst✝¹ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝ : Nonempty ι
n : ℕ
F : L.Functions n
i : ι
x : Fin n → G i
k : ι
ik : i ≤ k
jk : Classical.choose ⋯ ≤ k
⊢ (setoid G f) (funMap F fun i_1 ↦ Structure.Sigma.mk f i (x i_1)) (Structure.Sigma.mk f i (funMap F x))

Tactic:
refine ⟨k, jk, ik, ?_⟩

Goal state after:
L : Language
ι : Type v
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝² : IsDirectedOrder ι
inst✝¹ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝ : Nonempty ι
n : ℕ
F : L.Functions n
i : ι
x : Fin n → G i
k : ι
ik : i ≤ k
jk : Classical.choose ⋯ ≤ k
⊢ (f (Classical.choose ⋯) k jk) (funMap F (unify f (fun i_1 ↦ Structure.Sigma.mk f i (x i_1)) (Classical.choose ⋯) ⋯)) =
    (f i k ik) (funMap F x)
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: L : Language
ι : Type v
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝² : IsDirectedOrder ι
inst✝¹ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝ : Nonempty ι
n : ℕ
F : L.Functions n
i : ι
x : Fin n → G i
k : ι
ik : i ≤ k
jk : Classical.choose ⋯ ≤ k
⊢ funMap F (unify f (fun i_1 ↦ Structure.Sigma.mk f i (x i_1)) k ⋯) = funMap F (⇑(f i k ik) ∘ x)

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: L : Language
ι : Type v
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝² : IsDirectedOrder ι
inst✝¹ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝ : Nonempty ι
i : ι
n✝ : ℕ
F : L.Functions n✝
x : Fin n✝ → G i
⊢ (funMap F fun a ↦ ⟦Structure.Sigma.mk f i (x a)⟧) = funMap F ((fun a ↦ ⟦Structure.Sigma.mk f i a⟧) ∘ x)

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
A : L.Substructure M
hf : f.dom ≤ A
hg : A ≤ g.dom
hfg : f ≤ g
⊢ (g.domRestrict hg).cod.subtype.comp ((g.domRestrict hg).toEquiv.toEmbedding.comp (inclusion hf)) =
    g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion ⋯))

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: case refl
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
m : M
cod : L.Substructure N
g : ↥{ carrier := Set.univ, fun_mem := ⋯ } ≃[L] ↥cod
⊢ (toEmbeddingOfEqTop ⋯) m =
    ↑({ dom := { carrier := Set.univ, fun_mem := ⋯ }, cod := cod, toEquiv := g }.toEquiv ⟨m, ⋯⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: case refl.refl
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : ↥{ carrier := Set.univ, fun_mem := ⋯ } ≃[L] ↥{ carrier := Set.univ, fun_mem := ⋯ }
⊢ (toEquivOfEqTop ⋯ ⋯).toEmbedding = toEmbeddingOfEqTop ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: case refl.a
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
cod✝ : L.Substructure N
toEquiv✝ : ↥{ carrier := Set.univ, fun_mem := ⋯ } ≃[L] ↥cod✝
x✝ : M
h✝ : x✝ ∈ (PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.dom
⊢ (PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.cod.subtype
      ((PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.toEquiv ⟨x✝, h✝⟩) =
    { dom := { carrier := Set.univ, fun_mem := ⋯ }, cod := cod✝, toEquiv := toEquiv✝ }.cod.subtype
      ({ dom := { carrier := Set.univ, fun_mem := ⋯ }, cod := cod✝, toEquiv := toEquiv✝ }.toEquiv ⟨x✝, ⋯⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: case refl.h_dom
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
cod✝ : L.Substructure N
toEquiv✝ : ↥{ carrier := Set.univ, fun_mem := ⋯ } ≃[L] ↥cod✝
⊢ (PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.dom =
    { dom := { carrier := Set.univ, fun_mem := ⋯ }, cod := cod✝, toEquiv := toEquiv✝ }.dom

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
inst✝ : Countable M
g : L.FGEquiv M M → (U : { S // S.FG }) × (↥↑U →[L] M) :=
  fun f ↦ ⟨⟨(↑f).dom, ⋯⟩, (↑f).cod.subtype.toHom.comp (↑f).toEquiv.toHom⟩
f f' : L.FGEquiv M M
cod_f : L.Substructure M
equiv_f : ↥(↑f').1 ≃[L] ↥cod_f
f_fin : { dom := (↑f').1, cod := cod_f, toEquiv := equiv_f }.dom.FG
h : g ⟨{ dom := (↑f').1, cod := cod_f, toEquiv := equiv_f }, f_fin⟩ = g f'
⊢ (↑⟨{ dom := (↑f').1, cod := cod_f, toEquiv := equiv_f }, f_fin⟩).dom = (↑f').dom

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: L : Language
ι : Type v
inst✝⁵ : Preorder ι
G : ι → Type w
inst✝⁴ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝³ : IsDirectedOrder ι
inst✝² : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝¹ : Nonempty ι
P : Type u₁
inst✝ : L.Structure P
g : (i : ι) → G i ↪[L] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
n✝ : ℕ
F : L.Functions n✝
i : ι
y : Fin n✝ → G i
⊢ funMap F (⇑(g i) ∘ y) = funMap F ((fun x ↦ (g x.fst) x.snd) ∘ Structure.Sigma.mk f i ∘ y)

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: L : Language
ι : Type v
inst✝⁵ : Preorder ι
G : ι → Type w
inst✝⁴ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝³ : IsDirectedOrder ι
inst✝² : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝¹ : Nonempty ι
P : Type u₁
inst✝ : L.Structure P
g : (i : ι) → G i ↪[L] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
n✝ : ℕ
R : L.Relations n✝
i : ι
y : Fin n✝ → G i
⊢ RelMap R ((fun x ↦ (g x.fst) x.snd) ∘ Structure.Sigma.mk f i ∘ y) ↔ RelMap R (⇑(g i) ∘ y)

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: L : Language
ι : Type v
inst✝⁵ : Preorder ι
G : ι → Type w
inst✝⁴ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝³ : IsDirectedOrder ι
inst✝² : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝¹ : Nonempty ι
P : Type u₁
inst✝ : L.Structure P
F : DirectLimit G f ↪[L] P
x✝ : DirectLimit G f
i : ι
x : G i
⊢ F ((of L ι G f i) x) = (F.comp (of L ι G f i)) x

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: L : Language
ι : Type v
inst✝⁵ : Preorder ι
G : ι → Type w
inst✝⁴ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝³ : IsDirectedOrder ι
inst✝² : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝¹ : Nonempty ι
P : Type u₁
inst✝ : L.Structure P
g : (i : ι) → G i ↪[L] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
⊢ ⨆ i, Substructure.map ((lift L ι G f g Hg).toHom.comp (of L ι G f i).toHom) ⊤ = ⨆ i, Substructure.map (g i).toHom ⊤

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: case h
L : Language
ι : Type v
inst✝⁷ : Preorder ι
G : ι → Type w
inst✝⁶ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝⁵ : IsDirectedOrder ι
inst✝⁴ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝³ : Nonempty ι
P : Type u₁
inst✝² : L.Structure P
g✝ : (i : ι) → G i ↪[L] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g✝ j) ((f i j hij) x) = (g✝ i) x
G' : ι → Type w'
inst✝¹ : (i : ι) → L.Structure (G' i)
f' : (i j : ι) → i ≤ j → G' i ↪[L] G' j
g : (i : ι) → G i ≃[L] G' i
inst✝ : DirectedSystem G' fun i j h ↦ ⇑(f' i j h)
H_commuting : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (f' i j hij) ((g i) x)
U : (i : ι) → G i ↪[L] DirectLimit G' f' := fun i ↦ (of L ι G' f' i).comp (g i).toEmbedding
F : DirectLimit G f ↪[L] DirectLimit G' f' := lift L ι G f U ⋯
x : DirectLimit G' f'
i : ι
pre_x : G' i
⊢ (of L ι G' f' i) pre_x = Quot.mk ⇑(setoid G' f') ⟨i, pre_x⟩

Tactic:
rfl

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 : E
p : Set X
j : E
q : Set X
hijpq : ⟨i, p⟩ ≠ ⟨j, q⟩
hi : (∃ y, g y = i) ∧ p ∈ P i
hj : (∃ y, g y = j) ∧ q ∈ P j
hij : i ≠ j
⊢ Disjoint (⇑g ⁻¹' {i}) (⇑g ⁻¹' {j})

Tactic:
grind

Goal state after:
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: L : Language
ι : Type v
inst✝³ : Preorder ι
inst✝² : Nonempty ι
inst✝¹ : IsDirectedOrder ι
M : Type u_1
inst✝ : L.Structure M
S : ι →o L.Substructure M
i : ι
x : ↥(S i)
⊢ (Substructure.inclusion ⋯) x = (Equiv_iSup S) ((of L ι (fun x ↦ ↥(S x)) (fun x x_1 h ↦ Substructure.inclusion ⋯) i) x)

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Graph

Goal state before:
pp: V : Type u
⊢ graphRel.adj = graphRel.adj

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Graph

Goal state before:
pp: V : Type u
G : SimpleGraph V
x✝¹ x✝ : V
⊢ (Language.simpleGraphOfStructure V).Adj x✝¹ x✝ ↔ G.Adj x✝¹ x✝

Tactic:
rfl

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 α β
b : β
a_b : ∀ p ∈ ↑f, cmp p.1 a = cmp p.2 b
p : α × β
hp : p = (a, b) ∨ p ∈ ↑f
q : α × β
hq : q = (a, b) ∨ q ∈ ↑f
⊢ cmp p.1 q.1 = cmp p.2 q.2

Tactic:
rcases hp with (rfl | pf) <;> rcases hq with (rfl | qf)

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

case inl.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
q : α × β
qf : q ∈ ↑f
⊢ cmp (a, b).1 q.1 = cmp (a, b).2 q.2

case inr.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
p : α × β
pf : p ∈ ↑f
⊢ cmp p.1 (a, b).1 = cmp p.2 (a, b).2

case inr.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 : α × β
pf : p ∈ ↑f
qf : q ∈ ↑f
⊢ cmp p.1 q.1 = cmp p.2 q.2
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: case h
L : Language
M : Type w
inst✝ : L.Structure M
M_CG : Structure.CG L M
h : L.IsExtensionPair M M
S : L.Substructure M
S_FG : S.FG
f : ↥S ↪[L] M
g : M ≃[L] M
dom_le_dom :
  (↑⟨{ dom := S, cod := f.toHom.range, toEquiv := f.equivRange }, S_FG⟩).dom ≤ g.toEmbedding.toPartialEquiv.dom
eq :
  g.toEmbedding.toPartialEquiv.cod.subtype.comp
      (g.toEmbedding.toPartialEquiv.toEquiv.toEmbedding.comp (Substructure.inclusion dom_le_dom)) =
    f
x✝ : ↥S
⊢ (g.toEmbedding.toPartialEquiv.cod.subtype.comp
        (g.toEmbedding.toPartialEquiv.toEquiv.toEmbedding.comp (Substructure.inclusion dom_le_dom)))
      x✝ =
    (g.toEmbedding.comp S.subtype) x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
α : Type w
M : Type w'
⊢ orderRel.le = orderRel.le

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
h : L.IsUltrahomogeneous M
N P Q : Bundled L.Structure
NP : ↑N ↪[L] ↑P
NQ : ↑N ↪[L] ↑Q
Nfg : Structure.FG L ↑N
Pfg : Structure.FG L ↑P
PM : ↑P ↪[L] M
Qfg : Structure.FG L ↑Q
QM : ↑Q ↪[L] M
g : M ≃[L] M
hg : (QM.comp NQ).comp (PM.comp NP).equivRange.symm.toEmbedding = g.toEmbedding.comp (PM.comp NP).toHom.range.subtype
⊢ ∃ Q_1 NQ_1 PQ, Q_1 ∈ L.age M ∧ NQ_1.comp NP = PQ.comp NQ

Tactic:
let s := (g.toHom.comp PM.toHom).range ⊔ QM.toHom.range

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
h : L.IsUltrahomogeneous M
N P Q : Bundled L.Structure
NP : ↑N ↪[L] ↑P
NQ : ↑N ↪[L] ↑Q
Nfg : Structure.FG L ↑N
Pfg : Structure.FG L ↑P
PM : ↑P ↪[L] M
Qfg : Structure.FG L ↑Q
QM : ↑Q ↪[L] M
g : M ≃[L] M
hg : (QM.comp NQ).comp (PM.comp NP).equivRange.symm.toEmbedding = g.toEmbedding.comp (PM.comp NP).toHom.range.subtype
s : L.Substructure M := (g.toHom.comp PM.toHom).range ⊔ QM.toHom.range
⊢ ∃ Q_1 NQ_1 PQ, Q_1 ∈ L.age M ∧ NQ_1.comp NP = PQ.comp NQ
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
α : Type w
M : Type w'
n : ℕ
inst✝¹ : L.IsOrdered
inst✝ : L.Structure M
this : LE M := L.leOfStructure M
a✝¹ a✝ : M
⊢ RelMap leSymb (Fin.cons a✝¹ (Fin.cons a✝ finZeroElim)) ↔ a✝¹ ≤ Fin.cons a✝¹ (Fin.cons a✝ finZeroElim) 1

Tactic:
rfl

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

Goal state before:
pp: ι : Type u_3
inst✝ : Finite ι
s : Set (ι → ℕ)
hs : IsProperLinearSet s
x✝ : ι → ℕ
⊢ ¬(hs.fract x✝ = hs.base ∧ ∀ (i : ↑hs.basisSet), 0 ≤ hs.floor x✝ i ∧ (↑i ∉ hs.periods → hs.floor x✝ i = 0)) ↔
    hs.fract x✝ ≠ hs.base ∨
      (hs.fract x✝ = hs.base ∧ ∃ i, hs.floor x✝ i < 0) ∨
        hs.fract x✝ = hs.base ∧ ∃ i, ↑i ∉ hs.periods ∧ 0 < hs.floor x✝ i

Tactic:
grind

Goal state after:
Module: Mathlib.Topology.Baire.LocallyCompactRegular

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
s : Set X
inst✝¹ : R1Space X
inst✝ : LocallyCompactSpace X
hG : IsGδ s
this✝¹ : LocallyCompactSpace ↑(closure s)
this✝ : BaireSpace ↑(closure s)
this : BaireSpace ↑(Subtype.val ⁻¹' s)
⊢ Function.LeftInverse (fun x ↦ ⟨⟨↑x, ⋯⟩, ⋯⟩) fun x ↦ ⟨↑↑x, ⋯⟩

Tactic:
grind

Goal state after:
Module: Mathlib.Topology.Baire.LocallyCompactRegular

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
s : Set X
inst✝¹ : R1Space X
inst✝ : LocallyCompactSpace X
hG : IsGδ s
this✝¹ : LocallyCompactSpace ↑(closure s)
this✝ : BaireSpace ↑(closure s)
this : BaireSpace ↑(Subtype.val ⁻¹' s)
⊢ Function.RightInverse (fun x ↦ ⟨⟨↑x, ⋯⟩, ⋯⟩) fun x ↦ ⟨↑↑x, ⋯⟩

Tactic:
grind

Goal state after:
Module: Mathlib.ModelTheory.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
φ : L[[α]].Sentence
p : T.CompleteType α
⊢ p ∈ T.typesWith φ ↔ φ ∈ p

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
M : ModelType ↑p
φ : L[[α]].Sentence
⊢ ↑(ModelType.reduct (L.lhomWithConstants α) (M.subtheoryModel ⋯)) ⊨ φ ↔ ↑M ⊨ φ

Tactic:
rfl

Goal state after: