awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
h₂ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}
⊢ IsSemilinearSet
    ({x : ℕ | x ∈ s ∧ x < k} ∪ ({x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p} + (↑(closure (↑{p} : Set ℕ)) : Set ℕ)))

Tactic:
(IsSemilinearSet.of_finite h₁).union (.add (.of_finite h₂) (.closure_finset { p }))

Premises used: IsSemilinearSet.closure_finset, IsSemilinearSet.of_finite, IsSemilinearSet.add, Singleton.singleton, IsSemilinearSet.union
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
h₂ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}
h : s = {x : ℕ | x ∈ s ∧ x < k} ∪ ({x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p} + (↑(closure (↑{p} : Set ℕ)) : Set ℕ))
⊢ IsSemilinearSet s

Tactic:
convert! (IsSemilinearSet.of_finite h₁).union (.add (.of_finite h₂) (.closure_finset { p }))

Premises used: IsSemilinearSet.closure_finset, IsSemilinearSet.of_finite, IsSemilinearSet.add, Singleton.singleton, IsSemilinearSet.union
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
h₂ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}
h :
  ∀ (x : ℕ),
    x ∈ s ↔ x ∈ {x : ℕ | x ∈ s ∧ x < k} ∪ ({x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p} + (↑(closure (↑{p} : Set ℕ)) : Set ℕ))
⊢ s = {x : ℕ | x ∈ s ∧ x < k} ∪ ({x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p} + (↑(closure (↑{p} : Set ℕ)) : Set ℕ))

Tactic:
ext x
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
h₂ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}
x : ℕ
h : x ∈ s ↔ x ∈ s ∧ x < k ∨ ∃ (x_1 : ℕ), ((x_1 ∈ s ∧ k ≤ x_1) ∧ x_1 ∈ s ∧ x_1 < k + p) ∧ ∃ (a : ℕ), x_1 + a * p = x
⊢ x ∈ s ↔ x ∈ {x : ℕ | x ∈ s ∧ x < k} ∪ ({x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p} + (↑(closure (↑{p} : Set ℕ)) : Set ℕ))

Tactic:
simp only [sep_and, Finset.coe_singleton, mem_union, mem_setOf_eq, mem_add, mem_inter_iff,
      SetLike.mem_coe, AddSubmonoid.mem_closure_singleton, smul_eq_mul, exists_exists_eq_and]

Premises used: Set.mem_union, Finset.coe_singleton, Set.mem_inter_iff, Set.mem_setOf_eq, exists_exists_eq_and, SetLike.mem_coe, smul_eq_mul, Set.sep_and, AddSubmonoid.mem_closure_singleton, Set.mem_add
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
h₂ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}
x : ℕ
h : x ∈ s → x ∈ s ∧ x < k ∨ ∃ (x_1 : ℕ), ((x_1 ∈ s ∧ k ≤ x_1) ∧ x_1 ∈ s ∧ x_1 < k + p) ∧ ∃ (a : ℕ), x_1 + a * p = x
h₃ : (x ∈ s ∧ x < k ∨ ∃ (x_1 : ℕ), ((x_1 ∈ s ∧ k ≤ x_1) ∧ x_1 ∈ s ∧ x_1 < k + p) ∧ ∃ (a : ℕ), x_1 + a * p = x) → x ∈ s
⊢ x ∈ s ↔ x ∈ s ∧ x < k ∨ ∃ (x_1 : ℕ), ((x_1 ∈ s ∧ k ≤ x_1) ∧ x_1 ∈ s ∧ x_1 < k + p) ∧ ∃ (a : ℕ), x_1 + a * p = x

Tactic:
constructor
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
h₂ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}
x : ℕ
hx : x ∈ s
pos :
  ∀ (hx' : x < k),
    x ∈ s ∧ x < k ∨ ∃ (x_1 : ℕ), ((x_1 ∈ s ∧ k ≤ x_1) ∧ x_1 ∈ s ∧ x_1 < k + p) ∧ ∃ (a : ℕ), x_1 + a * p = x
neg :
  ∀ (hx' : ¬x < k),
    x ∈ s ∧ x < k ∨ ∃ (x_1 : ℕ), ((x_1 ∈ s ∧ k ≤ x_1) ∧ x_1 ∈ s ∧ x_1 < k + p) ∧ ∃ (a : ℕ), x_1 + a * p = x
⊢ x ∈ s ∧ x < k ∨ ∃ (x_1 : ℕ), ((x_1 ∈ s ∧ k ≤ x_1) ∧ x_1 ∈ s ∧ x_1 < k + p) ∧ ∃ (a : ℕ), x_1 + a * p = x

Tactic:
by_cases hx' : x < k
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
h₂ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}
x : ℕ
hx : x ∈ s
hx' : x < k
⊢ x ∈ s ∧ x < k ∨ ∃ (x_1 : ℕ), ((x_1 ∈ s ∧ k ≤ x_1) ∧ x_1 ∈ s ∧ x_1 < k + p) ∧ ∃ (a : ℕ), x_1 + a * p = x

Tactic:
Or.inl ⟨hx, hx'⟩

Premises used: And.intro, Or.inl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
h₂ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}
x : ℕ
hx : x ∈ s
hx' : x < k
⊢ x ∈ s ∧ x < k ∨ ∃ (x_1 : ℕ), ((x_1 ∈ s ∧ k ≤ x_1) ∧ x_1 ∈ s ∧ x_1 < k + p) ∧ ∃ (a : ℕ), x_1 + a * p = x

Tactic:
exact Or.inl ⟨hx, hx'⟩

Premises used: Or.inl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
h₂ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}
x : ℕ
hx : x ∈ s
hx' : ¬x < k
⊢ k ≤ x

Tactic:
rw [not_lt] at hx'

Premises used: not_lt
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
h₂ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}
x : ℕ
hx : x ∈ s
hx' : k ≤ x
⊢ x ∈ s ∧ x < k ∨ ∃ (x_1 : ℕ), ((x_1 ∈ s ∧ k ≤ x_1) ∧ x_1 ∈ s ∧ x_1 < k + p) ∧ ∃ (a : ℕ), x_1 + a * p = x

Tactic:
Or.inr ⟨k + (x - k) % p, ⟨⟨?_1, ?_2⟩, ?_1, ?_3⟩, (x - k) / p, ?_4⟩

Premises used: HSub.hSub, HDiv.hDiv, HMod.hMod, HAdd.hAdd, And.intro, Exists.intro, Or.inr
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
h₂ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}
x : ℕ
hx : x ∈ s
hx' : k ≤ x
_1 : k + (x - k) % p ∈ s
_2 : k ≤ k + (x - k) % p
_3 : k + (x - k) % p < k + p
_4 : k + (x - k) % p + (x - k) / p * p = x
⊢ x ∈ s ∧ x < k ∨ ∃ (x_1 : ℕ), ((x_1 ∈ s ∧ k ≤ x_1) ∧ x_1 ∈ s ∧ x_1 < k + p) ∧ ∃ (a : ℕ), x_1 + a * p = x

Tactic:
refine Or.inr ⟨k + (x - k) % p, ⟨⟨?_1, ?_2⟩, ?_1, ?_3⟩, (x - k) / p, ?_4⟩

Premises used: Or.inr
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
h₂ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}
x : ℕ
hx : x ∈ s
hx' : k ≤ x
⊢ k + (x - k) % p + (x - k) / p * p ∈ s

Tactic:
rw [← add_tsub_cancel_of_le hx', ← Nat.mod_add_div' (x - k) p, ← add_assoc] at hx

Premises used: add_assoc, HSub.hSub, add_tsub_cancel_of_le, Nat.mod_add_div'
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
h₂ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}
x : ℕ
hx : x ∈ s
hx' : k ≤ x
hx₁ : k + (x - k) % p + (x - k) / p * p ∈ s
⊢ k ≤ x

Tactic:
rw [← add_tsub_cancel_of_le hx', ← Nat.mod_add_div' (x - k) p, ← add_assoc] at hx

Premises used: add_assoc, HSub.hSub, add_tsub_cancel_of_le, Nat.mod_add_div'
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
h₂ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}
x : ℕ
hx : k + (x - k) % p + (x - k) / p * p ∈ s
hx' : k ≤ x
_1 : ∀ (m : ℕ) (hx : k + (x - k) % p + m * p ∈ s), k + (x - k) % p ∈ s
⊢ k + (x - k) % p ∈ s

Tactic:
generalize (x - k) / p = m at hx

Premises used: HSub.hSub
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
h₂ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}
x : ℕ
hx' : k ≤ x
hx : k + (x - k) % p + 0 * p ∈ s
⊢ k + (x - k) % p ∈ s

Tactic:
grind
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
h₂ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}
x : ℕ
hx' : k ≤ x
n : ℕ
h : ∀ (hx : k + (x - k) % p + n * p ∈ s), k + (x - k) % p ∈ s
hx : k + (x - k) % p + (n + 1) * p ∈ s
⊢ k + (x - k) % p ∈ s

Tactic:
grind
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
h₂ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}
x : ℕ
hx' : k ≤ x
m : ℕ
hx : k + (x - k) % p + m * p ∈ s
_1 : ∀ (hx : k + (x - k) % p + 0 * p ∈ s), k + (x - k) % p ∈ s
_1₁ :
  ∀ (n : ℕ),
    (∀ (hx : k + (x - k) % p + n * p ∈ s), k + (x - k) % p ∈ s) →
      ∀ (hx : k + (x - k) % p + (n + 1) * p ∈ s), k + (x - k) % p ∈ s
⊢ k + (x - k) % p ∈ s

Tactic:
induction m with grind
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
h₂ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}
x : ℕ
hx : x ∈ s
hx' : k ≤ x
⊢ k ≤ k + (x - k) % p

Tactic:
grind
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
h₂ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}
x : ℕ
hx : x ∈ s
hx' : k ≤ x
⊢ k + (x - k) % p < k + p

Tactic:
Nat.add_lt_add_left (Nat.mod_lt _ hp) _

Premises used: Nat.mod_lt, Nat.add_lt_add_left
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
h₂ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}
x : ℕ
hx : x ∈ s
hx' : k ≤ x
⊢ k + (x - k) % p < k + p

Tactic:
exact Nat.add_lt_add_left (Nat.mod_lt _ hp) _

Premises used: Nat.mod_lt, Nat.add_lt_add_left
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
h₂ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}
x : ℕ
hx : x ∈ s
hx' : k ≤ x
_4 : k + ((x - k) % p + (x - k) / p * p) = x
_4₁ : k + (x - k) = x
_4₂ _4₃ : x = x
⊢ k + (x - k) % p + (x - k) / p * p = x

Tactic:
rw [add_assoc, Nat.mod_add_div', add_tsub_cancel_of_le hx']

Premises used: add_assoc, add_tsub_cancel_of_le, Nat.mod_add_div'
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
h₂ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}
x : ℕ
hx : x ∈ s
hx' : x < k
⊢ x ∈ s

Tactic:
hx
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
h₂ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}
x : ℕ
hx : x ∈ s
hx' : x < k
⊢ x ∈ s

Tactic:
exact hx
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
h₂ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}
x : ℕ
right : x ∈ s ∧ x < k + p
hx : x ∈ s
hx' : k ≤ x
⊢ x + 0 * p ∈ s

Tactic:
grind
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
h₂ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}
x : ℕ
right : x ∈ s ∧ x < k + p
hx : x ∈ s
hx' : k ≤ x
n : ℕ
h : x + n * p ∈ s
⊢ x + (n + 1) * p ∈ s

Tactic:
grind
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
h₂ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}
x : ℕ
right : x ∈ s ∧ x < k + p
hx : x ∈ s
hx' : k ≤ x
m : ℕ
h : x + 0 * p ∈ s
h₃ : ∀ (n : ℕ), x + n * p ∈ s → x + (n + 1) * p ∈ s
⊢ x + m * p ∈ s

Tactic:
induction m with grind
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
⊢ L.card = (sum fun (l : ℕ) ↦ lift.{v, u} #(L.Functions l)) + sum fun (l : ℕ) ↦ lift.{u, v} #(L.Relations l)

Tactic:
simp only [card, mk_sum, mk_sigma, lift_sum]

Premises used: FirstOrder.Language.card, Cardinal.lift_sum, Cardinal.mk_sigma, Cardinal.mk_sum
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
L' : Language
inst : L.IsRelational
inst_1 : L'.IsRelational
⊢ (L.sum L').IsRelational

Tactic:
fun _ => instIsEmptySum

Premises used: instIsEmptySum
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
L' : Language
inst : L.IsAlgebraic
inst_1 : L'.IsAlgebraic
⊢ (L.sum L').IsAlgebraic

Tactic:
fun _ => instIsEmptySum

Premises used: instIsEmptySum
-- Module: Mathlib.ModelTheory.Basic
Goal:
⊢ Language.empty.card = 0

Tactic:
simp only [card, mk_sum, mk_sigma, mk_eq_zero,
  sum_const, mk_eq_aleph0, lift_id', mul_zero, add_zero]

Premises used: Cardinal.mk_eq_zero, FirstOrder.Language.card, Cardinal.lift_id', Cardinal.mk_eq_aleph0, MulZeroClass.mul_zero, Cardinal.mk_sigma, Cardinal.mk_sum, add_zero, Cardinal.sum_const
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
L' : Language
simp : (∀ (a : ℕ), IsEmpty (Language.empty.Functions a)) ∧ ∀ (a : ℕ), IsEmpty (Language.empty.Relations a)
⊢ IsEmpty Language.empty.Symbols

Tactic:
simp only [Language.Symbols, isEmpty_sum, isEmpty_sigma]

Premises used: isEmpty_sigma, isEmpty_sum, FirstOrder.Language.Symbols
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
L' : Language
⊢ (∀ (a : ℕ), IsEmpty (Language.empty.Functions a)) ∧ ∀ (a : ℕ), IsEmpty (Language.empty.Relations a)

Tactic:
⟨fun _ => inferInstance, fun _ => inferInstance⟩

Premises used: inferInstance, And.intro
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
L' : Language
⊢ (∀ (a : ℕ), IsEmpty (Language.empty.Functions a)) ∧ ∀ (a : ℕ), IsEmpty (Language.empty.Relations a)

Tactic:
exact ⟨fun _ => inferInstance, fun _ => inferInstance⟩
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
L' : Language
h : Countable L.Symbols
⊢ Countable.{max (u + 1) 1} ((l : ℕ) × L.Functions l)

Tactic:
@Function.Injective.countable _ _ h _ Sum.inl_injective

Premises used: Function.Injective.countable, Sum.inl_injective
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
L' : Language
i : ℕ
⊢ #((L.sum L').Functions i) = lift.{u', u} #(L.Functions i) + lift.{u, u'} #(L'.Functions i)

Tactic:
simp [Language.sum]

Premises used: FirstOrder.Language.sum
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
L' : Language
i : ℕ
⊢ #((L.sum L').Relations i) = lift.{v', v} #(L.Relations i) + lift.{v, v'} #(L'.Relations i)

Tactic:
simp [Language.sum]

Premises used: FirstOrder.Language.sum
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
L' : Language
⊢ (L.sum L').card = lift.{max u' v', max u v} L.card + lift.{max u v, max u' v'} L'.card

Tactic:
simp only [card, mk_sum, mk_sigma, card_functions_sum, sum_add_distrib', lift_add, lift_sum,
    lift_lift, card_relations_sum, add_assoc,
    add_comm (Cardinal.sum fun i => (#(L'.Functions i)).lift)]

Premises used: FirstOrder.Language.card, Cardinal.lift_lift, add_assoc, Cardinal.lift, Cardinal.mk, Cardinal.lift_sum, Cardinal.sum_add_distrib', add_comm, FirstOrder.Language.Functions, Cardinal.mk_sigma, Cardinal.mk_sum, FirstOrder.Language.card_functions_sum, Cardinal.lift_add, FirstOrder.Language.card_relations_sum, Cardinal.sum
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type w
inst : L.Structure M
c : L.Constants
x : Fin 0 → M
⊢ funMap c x = (↑c : M)

Tactic:
congr rfl (funext finZeroElim)

Premises used: finZeroElim, funext, congr, FirstOrder.Language.constantMap, rfl
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type w
inst : L.Structure M
h : Nonempty.{u + 1} L.Constants
⊢ Nonempty M

Tactic:
h.map (↑)

Premises used: Nonempty.map
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
F : Type u_3
M : Type u_4
N : Type u_5
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : FunLike F M N
inst_3 : L.HomClass F M N
φ : F
c : L.Constants
⊢ Eq.{u_5 + 1} (α := N) ((φ : (a : M) → N) (↑c : M) : N) ((↑c : N) : N)

Tactic:
(HomClass.map_fun φ c default).trans (congr rfl (funext default))

Premises used: Inhabited.default, funext, congr, FirstOrder.Language.constantMap, FirstOrder.Language.HomClass.map_fun, rfl, Eq.trans
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
f g : M →[L] N
h : f.toFun = g.toFun
mk :
  ∀ (toFun : M → N)
    (map_fun' : ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toFun (funMap f x) = funMap f (toFun ∘ x))
    (map_rel' : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r x → RelMap r (toFun ∘ x))
    (h : { toFun := toFun, map_fun' := @map_fun', map_rel' := @map_rel' : M →[L] N }.toFun = g.toFun),
    { toFun := toFun, map_fun' := @map_fun', map_rel' := @map_rel' : M →[L] N } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
g : M →[L] N
toFun : M → N
map_fun' : ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toFun (funMap f x) = funMap f (toFun ∘ x)
map_rel' : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r x → RelMap r (toFun ∘ x)
h : { toFun := toFun, map_fun' := @map_fun', map_rel' := @map_rel' : M →[L] N }.toFun = g.toFun
mk :
  ∀ (toFun_1 : M → N)
    (map_fun'_1 : ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toFun_1 (funMap f x) = funMap f (toFun_1 ∘ x))
    (map_rel'_1 : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r x → RelMap r (toFun_1 ∘ x))
    (h :
      { toFun := toFun, map_fun' := @map_fun', map_rel' := @map_rel' : M →[L] N }.toFun =
        { toFun := toFun_1, map_fun' := @map_fun'_1, map_rel' := @map_rel'_1 : M →[L] N }.toFun),
    { toFun := toFun, map_fun' := @map_fun', map_rel' := @map_rel' : M →[L] N } =
      { toFun := toFun_1, map_fun' := @map_fun'_1, map_rel' := @map_rel'_1 }
⊢ { toFun := toFun, map_fun' := @map_fun', map_rel' := @map_rel' : M →[L] N } = g

Tactic:
cases g
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
toFun : M → N
map_fun' : ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toFun (funMap f x) = funMap f (toFun ∘ x)
map_rel' : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r x → RelMap r (toFun ∘ x)
toFun_1 : M → N
map_fun'_1 : ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toFun_1 (funMap f x) = funMap f (toFun_1 ∘ x)
map_rel'_1 : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r x → RelMap r (toFun_1 ∘ x)
h :
  { toFun := toFun, map_fun' := @map_fun', map_rel' := @map_rel' : M →[L] N }.toFun =
    { toFun := toFun_1, map_fun' := @map_fun'_1, map_rel' := @map_rel'_1 : M →[L] N }.toFun
mk :
  ∀ (map_fun'_2 : ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toFun (funMap f x) = funMap f (toFun ∘ x))
    (map_rel'_2 : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r x → RelMap r (toFun ∘ x)),
    { toFun := toFun, map_fun' := @map_fun', map_rel' := @map_rel' : M →[L] N } =
      { toFun := toFun, map_fun' := @map_fun'_2, map_rel' := @map_rel'_2 }
⊢ { toFun := toFun, map_fun' := @map_fun', map_rel' := @map_rel' : M →[L] N } =
    { toFun := toFun_1, map_fun' := @map_fun'_1, map_rel' := @map_rel'_1 }

Tactic:
cases h
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
toFun : M → N
map_fun' : ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toFun (funMap f x) = funMap f (toFun ∘ x)
map_rel' : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r x → RelMap r (toFun ∘ x)
map_fun'_1 : ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toFun (funMap f x) = funMap f (toFun ∘ x)
map_rel'_1 : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r x → RelMap r (toFun ∘ x)
⊢ { toFun := toFun, map_fun' := @map_fun', map_rel' := @map_rel' : M →[L] N } =
    { toFun := toFun, map_fun' := @map_fun'_1, map_rel' := @map_rel'_1 }

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
inst_4 : L.IsAlgebraic
⊢ L.StrongHomClass (M →[L] N) M N

Tactic:
HomClass.strongHomClassOfIsAlgebraic

Premises used: FirstOrder.Language.HomClass.strongHomClassOfIsAlgebraic
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f : M →[L] N
⊢ f.toFun = (⇑f : (a : M) → N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f g : M →[L] N
h : ∀ (x : M), Eq.{w' + 1} (α := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N)
⊢ f = g

Tactic:
DFunLike.ext f g h

Premises used: DFunLike.ext
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
φ : M →[L] N
n : ℕ
f : L.Functions n
x : Fin n → M
⊢ Eq.{w' + 1} (α := N) ((φ : (a : M) → N) (funMap f x) : N) (funMap f ((⇑φ : (a : M) → N) ∘ x) : N)

Tactic:
HomClass.map_fun φ f x

Premises used: FirstOrder.Language.HomClass.map_fun
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
φ : M →[L] N
c : L.Constants
⊢ Eq.{w' + 1} (α := N) ((φ : (a : M) → N) (↑c : M) : N) ((↑c : N) : N)

Tactic:
HomClass.map_constants φ c

Premises used: FirstOrder.Language.HomClass.map_constants
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
φ : M →[L] N
n : ℕ
r : L.Relations n
x : Fin n → M
⊢ RelMap r x → RelMap.{u, v, w'} (M := N) r ((⇑φ : (a : M) → N) ∘ x)

Tactic:
HomClass.map_rel φ r x

Premises used: FirstOrder.Language.HomClass.map_rel
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
M : Type w
inst : L.Structure M
x : M
⊢ (id L M : (a : M) → M) x = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
hnp : N →[L] P
hmn : M →[L] N
n : ℕ
x : L.Functions n
x_1 : Fin n → M
simp :
  Eq.{u_1 + 1} (α := P)
    (funMap x (Function.comp.{1, w' + 1, u_1 + 1} (β := N) (⇑hnp : (a : N) → P) ((⇑hmn : (a : M) → N) ∘ x_1)))
    (funMap x (Function.comp.{w + 1, w' + 1, u_1 + 1} (β := N) (⇑hnp : (a : N) → P) (⇑hmn : (a : M) → N) ∘ x_1))
⊢ Eq.{u_1 + 1} (α := P)
    (Function.comp.{w + 1, w' + 1, u_1 + 1} (β := N) (⇑hnp : (a : N) → P) (⇑hmn : (a : M) → N) (funMap x x_1))
    (funMap x (Function.comp.{w + 1, w' + 1, u_1 + 1} (β := N) (⇑hnp : (a : N) → P) (⇑hmn : (a : M) → N) ∘ x_1))

Tactic:
simp
-- Module: Mathlib.ModelTheory.Basic
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
hnp : N →[L] P
hmn : M →[L] N
n : ℕ
x : L.Functions n
x_1 : Fin n → M
⊢ Eq.{u_1 + 1} (α := P)
    (funMap x (Function.comp.{1, w' + 1, u_1 + 1} (β := N) (⇑hnp : (a : N) → P) ((⇑hmn : (a : M) → N) ∘ x_1)))
    (funMap x (Function.comp.{w + 1, w' + 1, u_1 + 1} (β := N) (⇑hnp : (a : N) → P) (⇑hmn : (a : M) → N) ∘ x_1))

Tactic:
rfl