internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Semiterm.Operator.numeral_succ
Proof state before:
case succ
L : Language
hz✝ : Operator.Zero L
ho : Operator.One L
ha : Operator.Add L
z : ℕ
hz : z + 1 ≠ 0
⊢ op(+).foldr op(1) (List.replicate (z + 1) op(1)) =
    op(+).comp
      ![match z + 1 with
        | 0 => op(0)
        | n.succ => op(+).foldr op(1) (List.replicate n op(1)),
        op(1)]
Tactic:
simp [Operator.foldr]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.Operator.numeral_add_two
Proof state before:
L : Language
hz : Operator.Zero L
ho : Operator.One L
ha : Operator.Add L
z : ℕ
⊢ z + 1 ≠ 0
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.Operator.Add.positive_iff
Proof state before:
L : Language
ξ : Type u_1
n : ℕ
inst✝ : L.Add
t u : Semiterm L ξ (n + 1)
⊢ (op(+).operator ![t, u]).Positive ↔ t.Positive ∧ u.Positive
Tactic:
simp [positive_operator_iff, Add.term_eq, bv_func]
Proof state after:
L : Language
ξ : Type u_1
n : ℕ
inst✝ : L.Add
t u : Semiterm L ξ (n + 1)
⊢ (∀ (i : Fin 2), (![t, u] i).Positive) ↔ t.Positive ∧ u.Positive
Theorem: LO.FirstOrder.Semiterm.Operator.Add.positive_iff
Proof state before:
L : Language
ξ : Type u_1
n : ℕ
inst✝ : L.Add
t u : Semiterm L ξ (n + 1)
⊢ (∀ (i : Fin 2), (![t, u] i).Positive) ↔ t.Positive ∧ u.Positive
Tactic:
exact ⟨by intro h; exact ⟨h 0, h 1⟩,
  by intro h i; cases i using Fin.cases <;> simp [Fin.eq_zero, *]⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.Operator.Add.positive_iff
Proof state before:
L : Language
ξ : Type u_1
n : ℕ
inst✝ : L.Add
t u : Semiterm L ξ (n + 1)
⊢ (∀ (i : Fin 2), (![t, u] i).Positive) → t.Positive ∧ u.Positive
Tactic:
intro h
Proof state after:
L : Language
ξ : Type u_1
n : ℕ
inst✝ : L.Add
t u : Semiterm L ξ (n + 1)
h : ∀ (i : Fin 2), (![t, u] i).Positive
⊢ t.Positive ∧ u.Positive
Theorem: LO.FirstOrder.Semiterm.Operator.Add.positive_iff
Proof state before:
L : Language
ξ : Type u_1
n : ℕ
inst✝ : L.Add
t u : Semiterm L ξ (n + 1)
h : ∀ (i : Fin 2), (![t, u] i).Positive
⊢ t.Positive ∧ u.Positive
Tactic:
exact ⟨h 0, h 1⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.Operator.Add.positive_iff
Proof state before:
L : Language
ξ : Type u_1
n : ℕ
inst✝ : L.Add
t u : Semiterm L ξ (n + 1)
⊢ t.Positive ∧ u.Positive → ∀ (i : Fin 2), (![t, u] i).Positive
Tactic:
intro h i
Proof state after:
L : Language
ξ : Type u_1
n : ℕ
inst✝ : L.Add
t u : Semiterm L ξ (n + 1)
h : t.Positive ∧ u.Positive
i : Fin 2
⊢ (![t, u] i).Positive
Theorem: LO.FirstOrder.Semiterm.Operator.Add.positive_iff
Proof state before:
L : Language
ξ : Type u_1
n : ℕ
inst✝ : L.Add
t u : Semiterm L ξ (n + 1)
h : t.Positive ∧ u.Positive
i : Fin 2
⊢ (![t, u] i).Positive
Tactic:
cases i using Fin.cases <;> simp [Fin.eq_zero, *]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.Operator.Mul.positive_iff
Proof state before:
L : Language
ξ : Type u_1
n : ℕ
inst✝ : L.Mul
t u : Semiterm L ξ (n + 1)
⊢ (op(*).operator ![t, u]).Positive ↔ t.Positive ∧ u.Positive
Tactic:
simp [positive_operator_iff, Mul.term_eq, bv_func]
Proof state after:
L : Language
ξ : Type u_1
n : ℕ
inst✝ : L.Mul
t u : Semiterm L ξ (n + 1)
⊢ (∀ (i : Fin 2), (![t, u] i).Positive) ↔ t.Positive ∧ u.Positive
Theorem: LO.FirstOrder.Semiterm.Operator.Mul.positive_iff
Proof state before:
L : Language
ξ : Type u_1
n : ℕ
inst✝ : L.Mul
t u : Semiterm L ξ (n + 1)
⊢ (∀ (i : Fin 2), (![t, u] i).Positive) ↔ t.Positive ∧ u.Positive
Tactic:
exact ⟨by intro h; exact ⟨h 0, h 1⟩,
  by intro h i; cases i using Fin.cases <;> simp [Fin.eq_zero, *]⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.Operator.Mul.positive_iff
Proof state before:
L : Language
ξ : Type u_1
n : ℕ
inst✝ : L.Mul
t u : Semiterm L ξ (n + 1)
⊢ (∀ (i : Fin 2), (![t, u] i).Positive) → t.Positive ∧ u.Positive
Tactic:
intro h
Proof state after:
L : Language
ξ : Type u_1
n : ℕ
inst✝ : L.Mul
t u : Semiterm L ξ (n + 1)
h : ∀ (i : Fin 2), (![t, u] i).Positive
⊢ t.Positive ∧ u.Positive
Theorem: LO.FirstOrder.Semiterm.Operator.Mul.positive_iff
Proof state before:
L : Language
ξ : Type u_1
n : ℕ
inst✝ : L.Mul
t u : Semiterm L ξ (n + 1)
h : ∀ (i : Fin 2), (![t, u] i).Positive
⊢ t.Positive ∧ u.Positive
Tactic:
exact ⟨h 0, h 1⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.Operator.Mul.positive_iff
Proof state before:
L : Language
ξ : Type u_1
n : ℕ
inst✝ : L.Mul
t u : Semiterm L ξ (n + 1)
⊢ t.Positive ∧ u.Positive → ∀ (i : Fin 2), (![t, u] i).Positive
Tactic:
intro h i
Proof state after:
L : Language
ξ : Type u_1
n : ℕ
inst✝ : L.Mul
t u : Semiterm L ξ (n + 1)
h : t.Positive ∧ u.Positive
i : Fin 2
⊢ (![t, u] i).Positive
Theorem: LO.FirstOrder.Semiterm.Operator.Mul.positive_iff
Proof state before:
L : Language
ξ : Type u_1
n : ℕ
inst✝ : L.Mul
t u : Semiterm L ξ (n + 1)
h : t.Positive ∧ u.Positive
i : Fin 2
⊢ (![t, u] i).Positive
Tactic:
cases i using Fin.cases <;> simp [Fin.eq_zero, *]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.Operator.Exp.positive_iff
Proof state before:
L : Language
ξ : Type u_1
n : ℕ
inst✝ : L.Exp
t : Semiterm L ξ (n + 1)
⊢ (exp.operator ![t]).Positive ↔ t.Positive
Tactic:
simp [positive_operator_iff, Exp.term_eq, bv_func]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.Operator.npow_succ
Proof state before:
L : Language
inst✝¹ : Operator.One L
inst✝ : Operator.Mul L
n : ℕ
⊢ npow L (n + 1) = op(*).comp ![npow L n, bvar 0]
Tactic:
simp [npow, foldr]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.Operator.npow_positive_iff
Proof state before:
L : Language
ξ : Type u_1
n : ℕ
inst✝¹ : Operator.One L
inst✝ : L.Mul
t : Semiterm L ξ (n + 1)
k : ℕ
⊢ ((npow L k).operator ![t]).Positive ↔ k = 0 ∨ t.Positive
Tactic:
cases k <;> simp [positive_operator_iff, operator_comp, npow_zero, npow_succ]
Proof state after:
case succ
L : Language
ξ : Type u_1
n : ℕ
inst✝¹ : Operator.One L
inst✝ : L.Mul
t : Semiterm L ξ (n + 1)
n✝ : ℕ
⊢ (∀ i ∈ op(*).term.bv, ∀ i_1 ∈ (![npow L n✝, bvar 0] i).term.bv, t.Positive) ↔ t.Positive
Theorem: LO.FirstOrder.Semiterm.Operator.npow_positive_iff
Proof state before:
L : Language
ξ : Type u_1
n : ℕ
inst✝ : Operator.One L
k : L.Mul
t : Semiterm L ξ (n + 1)
n✝ : ℕ
⊢ (∀ i ∈ op(*).term.bv, ∀ i_1 ∈ (![npow L n✝, bvar 0] i).term.bv, t.Positive) ↔ t.Positive
Tactic:
simp [Mul.term_eq, bv_func]
Proof state after:
L : Language
ξ : Type u_1
n : ℕ
inst✝ : Operator.One L
k : L.Mul
t : Semiterm L ξ (n + 1)
n✝ : ℕ
⊢ (∀ (i : Fin 2), ∀ i_1 ∈ (![npow L n✝, bvar 0] i).term.bv, t.Positive) ↔ t.Positive
Theorem: LO.FirstOrder.Semiterm.Operator.npow_positive_iff
Proof state before:
L : Language
ξ : Type u_1
n : ℕ
inst✝ : Operator.One L
k : L.Mul
t : Semiterm L ξ (n + 1)
n✝ : ℕ
⊢ (∀ (i : Fin 2), ∀ i_1 ∈ (![npow L n✝, bvar 0] i).term.bv, t.Positive) ↔ t.Positive
Tactic:
constructor
Proof state after:
case mp
L : Language
ξ : Type u_1
n : ℕ
inst✝ : Operator.One L
k : L.Mul
t : Semiterm L ξ (n + 1)
n✝ : ℕ
⊢ (∀ (i : Fin 2), ∀ i_1 ∈ (![npow L n✝, bvar 0] i).term.bv, t.Positive) → t.Positive

case mpr
L : Language
ξ : Type u_1
n : ℕ
inst✝ : Operator.One L
k : L.Mul
t : Semiterm L ξ (n + 1)
n✝ : ℕ
⊢ t.Positive → ∀ (i : Fin 2), ∀ i_1 ∈ (![npow L n✝, bvar 0] i).term.bv, t.Positive
Theorem: LO.FirstOrder.Semiterm.Operator.npow_positive_iff
Proof state before:
case mp
L : Language
ξ : Type u_1
n : ℕ
inst✝ : Operator.One L
k : L.Mul
t : Semiterm L ξ (n + 1)
n✝ : ℕ
⊢ (∀ (i : Fin 2), ∀ i_1 ∈ (![npow L n✝, bvar 0] i).term.bv, t.Positive) → t.Positive
Tactic:
intro h
Proof state after:
case mp
L : Language
ξ : Type u_1
n : ℕ
inst✝ : Operator.One L
k : L.Mul
t : Semiterm L ξ (n + 1)
n✝ : ℕ
h : ∀ (i : Fin 2), ∀ i_1 ∈ (![npow L n✝, bvar 0] i).term.bv, t.Positive
⊢ t.Positive
Theorem: LO.FirstOrder.Semiterm.Operator.npow_positive_iff
Proof state before:
case mp
L : Language
ξ : Type u_1
n : ℕ
inst✝ : Operator.One L
k : L.Mul
t : Semiterm L ξ (n + 1)
n✝ : ℕ
h : ∀ (i : Fin 2), ∀ i_1 ∈ (![npow L n✝, bvar 0] i).term.bv, t.Positive
⊢ t.Positive
Tactic:
exact h 1 0 (by simp [bvar])
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.Operator.npow_positive_iff
Proof state before:
L : Language
ξ : Type u_1
n : ℕ
inst✝ : Operator.One L
k : L.Mul
t : Semiterm L ξ (n + 1)
n✝ : ℕ
h : ∀ (i : Fin 2), ∀ i_1 ∈ (![npow L n✝, bvar 0] i).term.bv, t.Positive
⊢ 0 ∈ (![npow L n✝, bvar 0] 1).term.bv
Tactic:
simp [bvar]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.Operator.npow_positive_iff
Proof state before:
case mpr
L : Language
ξ : Type u_1
n : ℕ
inst✝ : Operator.One L
k : L.Mul
t : Semiterm L ξ (n + 1)
n✝ : ℕ
⊢ t.Positive → ∀ (i : Fin 2), ∀ i_1 ∈ (![npow L n✝, bvar 0] i).term.bv, t.Positive
Tactic:
intro h _ _ _
Proof state after:
case mpr
L : Language
ξ : Type u_1
n : ℕ
inst✝ : Operator.One L
k : L.Mul
t : Semiterm L ξ (n + 1)
n✝ : ℕ
h : t.Positive
i✝¹ : Fin 2
i✝ : Fin 1
a✝ : i✝ ∈ (![npow L n✝, bvar 0] i✝¹).term.bv
⊢ t.Positive
Theorem: LO.FirstOrder.Semiterm.Operator.npow_positive_iff
Proof state before:
case mpr
L : Language
ξ : Type u_1
n : ℕ
inst✝ : Operator.One L
k : L.Mul
t : Semiterm L ξ (n + 1)
n✝ : ℕ
h : t.Positive
i✝¹ : Fin 2
i✝ : Fin 1
a✝ : i✝ ∈ (![npow L n✝, bvar 0] i✝¹).term.bv
⊢ t.Positive
Tactic:
exact h
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.complexity_zero
Proof state before:
L✝ : Language
L : Language
inst✝³ : L.Zero
inst✝² : L.One
inst✝¹ : L.Add
inst✝ : L.Mul
ξ : Type u_1
n : ℕ
⊢ (Operator.const op(0)).complexity = 1
Tactic:
simp [Operator.const, Operator.operator, Operator.numeral, Operator.Zero.term_eq, complexity_func]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.complexity_one
Proof state before:
L✝ : Language
L : Language
inst✝³ : L.Zero
inst✝² : L.One
inst✝¹ : L.Add
inst✝ : L.Mul
ξ : Type u_1
n : ℕ
⊢ (Operator.const op(1)).complexity = 1
Tactic:
simp [Operator.const, Operator.operator, Operator.numeral, Operator.One.term_eq, complexity_func]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.complexity_add
Proof state before:
L✝ : Language
L : Language
inst✝³ : L.Zero
inst✝² : L.One
inst✝¹ : L.Add
inst✝ : L.Mul
ξ : Type u_1
n : ℕ
t u : Semiterm L ξ n
⊢ (op(+).operator ![t, u]).complexity = max t.complexity u.complexity + 1
Tactic:
simp [Operator.const, Operator.operator, Operator.numeral, Operator.Add.term_eq, complexity_func, Rew.func]
Proof state after:
L✝ : Language
L : Language
inst✝³ : L.Zero
inst✝² : L.One
inst✝¹ : L.Add
inst✝ : L.Mul
ξ : Type u_1
n : ℕ
t u : Semiterm L ξ n
⊢ (Finset.univ.sup fun i => (![t, u] i).complexity) = max t.complexity u.complexity
Theorem: LO.FirstOrder.Semiterm.complexity_add
Proof state before:
L✝ : Language
L : Language
inst✝³ : L.Zero
inst✝² : L.One
inst✝¹ : L.Add
inst✝ : L.Mul
ξ : Type u_1
n : ℕ
t u : Semiterm L ξ n
⊢ (Finset.univ.sup fun i => (![t, u] i).complexity) = max t.complexity u.complexity
Tactic:
rw [show (Finset.univ : Finset (Fin 2)) = {0, 1} from by ext i; cases i using Fin.cases <;> simp [Fin.eq_zero]]
Proof state after:
L✝ : Language
L : Language
inst✝³ : L.Zero
inst✝² : L.One
inst✝¹ : L.Add
inst✝ : L.Mul
ξ : Type u_1
n : ℕ
t u : Semiterm L ξ n
⊢ ({0, 1}.sup fun i => (![t, u] i).complexity) = max t.complexity u.complexity
Theorem: LO.FirstOrder.Semiterm.complexity_add
Proof state before:
L✝ : Language
L : Language
inst✝³ : L.Zero
inst✝² : L.One
inst✝¹ : L.Add
inst✝ : L.Mul
ξ : Type u_1
n : ℕ
t u : Semiterm L ξ n
⊢ ({0, 1}.sup fun i => (![t, u] i).complexity) = max t.complexity u.complexity
Tactic:
simp [sup_eq_max]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.complexity_add
Proof state before:
L✝ : Language
L : Language
inst✝³ : L.Zero
inst✝² : L.One
inst✝¹ : L.Add
inst✝ : L.Mul
ξ : Type u_1
n : ℕ
t u : Semiterm L ξ n
⊢ Finset.univ = {0, 1}
Tactic:
ext i
Proof state after:
case a
L✝ : Language
L : Language
inst✝³ : L.Zero
inst✝² : L.One
inst✝¹ : L.Add
inst✝ : L.Mul
ξ : Type u_1
n : ℕ
t u : Semiterm L ξ n
i : Fin 2
⊢ i ∈ Finset.univ ↔ i ∈ {0, 1}
Theorem: LO.FirstOrder.Semiterm.complexity_add
Proof state before:
case a
L✝ : Language
L : Language
inst✝³ : L.Zero
inst✝² : L.One
inst✝¹ : L.Add
inst✝ : L.Mul
ξ : Type u_1
n : ℕ
t u : Semiterm L ξ n
i : Fin 2
⊢ i ∈ Finset.univ ↔ i ∈ {0, 1}
Tactic:
cases i using Fin.cases <;> simp [Fin.eq_zero]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.complexity_mul
Proof state before:
L✝ : Language
L : Language
inst✝³ : L.Zero
inst✝² : L.One
inst✝¹ : L.Add
inst✝ : L.Mul
ξ : Type u_1
n : ℕ
t u : Semiterm L ξ n
⊢ (op(*).operator ![t, u]).complexity = max t.complexity u.complexity + 1
Tactic:
simp [Operator.const, Operator.operator, Operator.numeral, Operator.Mul.term_eq, complexity_func, Rew.func]
Proof state after:
L✝ : Language
L : Language
inst✝³ : L.Zero
inst✝² : L.One
inst✝¹ : L.Add
inst✝ : L.Mul
ξ : Type u_1
n : ℕ
t u : Semiterm L ξ n
⊢ (Finset.univ.sup fun i => (![t, u] i).complexity) = max t.complexity u.complexity
Theorem: LO.FirstOrder.Semiterm.complexity_mul
Proof state before:
L✝ : Language
L : Language
inst✝³ : L.Zero
inst✝² : L.One
inst✝¹ : L.Add
inst✝ : L.Mul
ξ : Type u_1
n : ℕ
t u : Semiterm L ξ n
⊢ (Finset.univ.sup fun i => (![t, u] i).complexity) = max t.complexity u.complexity
Tactic:
rw [show (Finset.univ : Finset (Fin 2)) = {0, 1} from by ext i; cases i using Fin.cases <;> simp [Fin.eq_zero]]
Proof state after:
L✝ : Language
L : Language
inst✝³ : L.Zero
inst✝² : L.One
inst✝¹ : L.Add
inst✝ : L.Mul
ξ : Type u_1
n : ℕ
t u : Semiterm L ξ n
⊢ ({0, 1}.sup fun i => (![t, u] i).complexity) = max t.complexity u.complexity
Theorem: LO.FirstOrder.Semiterm.complexity_mul
Proof state before:
L✝ : Language
L : Language
inst✝³ : L.Zero
inst✝² : L.One
inst✝¹ : L.Add
inst✝ : L.Mul
ξ : Type u_1
n : ℕ
t u : Semiterm L ξ n
⊢ ({0, 1}.sup fun i => (![t, u] i).complexity) = max t.complexity u.complexity
Tactic:
simp [sup_eq_max]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.complexity_mul
Proof state before:
L✝ : Language
L : Language
inst✝³ : L.Zero
inst✝² : L.One
inst✝¹ : L.Add
inst✝ : L.Mul
ξ : Type u_1
n : ℕ
t u : Semiterm L ξ n
⊢ Finset.univ = {0, 1}
Tactic:
ext i
Proof state after:
case a
L✝ : Language
L : Language
inst✝³ : L.Zero
inst✝² : L.One
inst✝¹ : L.Add
inst✝ : L.Mul
ξ : Type u_1
n : ℕ
t u : Semiterm L ξ n
i : Fin 2
⊢ i ∈ Finset.univ ↔ i ∈ {0, 1}
Theorem: LO.FirstOrder.Semiterm.complexity_mul
Proof state before:
case a
L✝ : Language
L : Language
inst✝³ : L.Zero
inst✝² : L.One
inst✝¹ : L.Add
inst✝ : L.Mul
ξ : Type u_1
n : ℕ
t u : Semiterm L ξ n
i : Fin 2
⊢ i ∈ Finset.univ ↔ i ∈ {0, 1}
Tactic:
cases i using Fin.cases <;> simp [Fin.eq_zero]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.val_operator
Proof state before:
L : Language
M : Type w
s : Structure L M
n✝ : ℕ
e : Fin n✝ → M
ξ✝ : Type u_1
ε : ξ✝ → M
k : ℕ
o : Operator L k
v : Fin k → Semiterm L ξ✝ n✝
⊢ val s e ε (o.operator v) = o.val fun x => val s e ε (v x)
Tactic:
simp [Operator.operator, val_substs]
Proof state after:
L : Language
M : Type w
s : Structure L M
n✝ : ℕ
e : Fin n✝ → M
ξ✝ : Type u_1
ε : ξ✝ → M
k : ℕ
o : Operator L k
v : Fin k → Semiterm L ξ✝ n✝
⊢ val s (fun x => val s e ε (v x)) (fun a => instIsEmptyEmpty.elim a) o.term = o.val fun x => val s e ε (v x)
Theorem: LO.FirstOrder.Semiterm.val_operator
Proof state before:
L : Language
M : Type w
s : Structure L M
n✝ : ℕ
e : Fin n✝ → M
ξ✝ : Type u_1
ε : ξ✝ → M
k : ℕ
o : Operator L k
v : Fin k → Semiterm L ξ✝ n✝
⊢ val s (fun x => val s e ε (v x)) (fun a => instIsEmptyEmpty.elim a) o.term = o.val fun x => val s e ε (v x)
Tactic:
congr
Proof state after:
case e_ε
L : Language
M : Type w
s : Structure L M
n✝ : ℕ
e : Fin n✝ → M
ξ✝ : Type u_1
ε : ξ✝ → M
k : ℕ
o : Operator L k
v : Fin k → Semiterm L ξ✝ n✝
⊢ (fun a => instIsEmptyEmpty.elim a) = Empty.elim
Theorem: LO.FirstOrder.Semiterm.val_operator
Proof state before:
case e_ε
L : Language
M : Type w
s : Structure L M
n✝ : ℕ
e : Fin n✝ → M
ξ✝ : Type u_1
ε : ξ✝ → M
k : ℕ
o : Operator L k
v : Fin k → Semiterm L ξ✝ n✝
⊢ (fun a => instIsEmptyEmpty.elim a) = Empty.elim
Tactic:
funext x
Proof state after:
case e_ε.h
L : Language
M : Type w
s : Structure L M
n✝ : ℕ
e : Fin n✝ → M
ξ✝ : Type u_1
ε : ξ✝ → M
k : ℕ
o : Operator L k
v : Fin k → Semiterm L ξ✝ n✝
x : Empty
⊢ instIsEmptyEmpty.elim x = x.elim
Theorem: LO.FirstOrder.Semiterm.val_operator
Proof state before:
case e_ε.h
L : Language
M : Type w
s : Structure L M
n✝ : ℕ
e : Fin n✝ → M
ξ✝ : Type u_1
ε : ξ✝ → M
k : ℕ
o : Operator L k
v : Fin k → Semiterm L ξ✝ n✝
x : Empty
⊢ instIsEmptyEmpty.elim x = x.elim
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.val_const
Proof state before:
L : Language
M : Type w
s : Structure L M
n✝ : ℕ
e : Fin n✝ → M
μ✝ : Type u_1
ε : μ✝ → M
o : Const L
⊢ val s e ε (Operator.const o) = Operator.val o ![]
Tactic:
simp [Operator.const, val_operator, Matrix.empty_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.val_operator₀
Proof state before:
L : Language
M : Type w
s : Structure L M
n✝ : ℕ
e : Fin n✝ → M
ξ✝ : Type u_1
ε : ξ✝ → M
v : Fin 0 → Semiterm L ξ✝ n✝
o : Const L
⊢ val s e ε (Operator.operator o v) = Operator.val o ![]
Tactic:
simp [val_operator, Matrix.empty_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.val_operator₁
Proof state before:
L : Language
M : Type w
s : Structure L M
n✝ : ℕ
e : Fin n✝ → M
ξ✝ : Type u_1
ε : ξ✝ → M
t : Semiterm L ξ✝ n✝
o : Operator L 1
⊢ val s e ε (o.operator ![t]) = o.val ![val s e ε t]
Tactic:
simp [val_operator, Matrix.empty_eq]
Proof state after:
L : Language
M : Type w
s : Structure L M
n✝ : ℕ
e : Fin n✝ → M
ξ✝ : Type u_1
ε : ξ✝ → M
t : Semiterm L ξ✝ n✝
o : Operator L 1
⊢ (o.val fun x => val s e ε t) = o.val ![val s e ε t]
Theorem: LO.FirstOrder.Semiterm.val_operator₁
Proof state before:
L : Language
M : Type w
s : Structure L M
n✝ : ℕ
e : Fin n✝ → M
ξ✝ : Type u_1
ε : ξ✝ → M
t : Semiterm L ξ✝ n✝
o : Operator L 1
⊢ (o.val fun x => val s e ε t) = o.val ![val s e ε t]
Tactic:
congr
Proof state after:
case e_v
L : Language
M : Type w
s : Structure L M
n✝ : ℕ
e : Fin n✝ → M
ξ✝ : Type u_1
ε : ξ✝ → M
t : Semiterm L ξ✝ n✝
o : Operator L 1
⊢ (fun x => val s e ε t) = ![val s e ε t]
Theorem: LO.FirstOrder.Semiterm.val_operator₁
Proof state before:
case e_v
L : Language
M : Type w
s : Structure L M
n✝ : ℕ
e : Fin n✝ → M
ξ✝ : Type u_1
ε : ξ✝ → M
t : Semiterm L ξ✝ n✝
o : Operator L 1
⊢ (fun x => val s e ε t) = ![val s e ε t]
Tactic:
funext i
Proof state after:
case e_v.h
L : Language
M : Type w
s : Structure L M
n✝ : ℕ
e : Fin n✝ → M
ξ✝ : Type u_1
ε : ξ✝ → M
t : Semiterm L ξ✝ n✝
o : Operator L 1
i : Fin 1
⊢ val s e ε t = ![val s e ε t] i
Theorem: LO.FirstOrder.Semiterm.val_operator₁
Proof state before:
case e_v.h
L : Language
M : Type w
s : Structure L M
n✝ : ℕ
e : Fin n✝ → M
ξ✝ : Type u_1
ε : ξ✝ → M
t : Semiterm L ξ✝ n✝
o : Operator L 1
i : Fin 1
⊢ val s e ε t = ![val s e ε t] i
Tactic:
cases' i using Fin.cases with i <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.val_operator₂
Proof state before:
L : Language
M : Type w
s : Structure L M
n✝ : ℕ
e : Fin n✝ → M
ξ✝ : Type u_1
ε : ξ✝ → M
o : Operator L 2
t u : Semiterm L ξ✝ n✝
⊢ val s e ε (o.operator ![t, u]) = o.val ![val s e ε t, val s e ε u]
Tactic:
simp [val_operator]
Proof state after:
L : Language
M : Type w
s : Structure L M
n✝ : ℕ
e : Fin n✝ → M
ξ✝ : Type u_1
ε : ξ✝ → M
o : Operator L 2
t u : Semiterm L ξ✝ n✝
⊢ (o.val fun x => val s e ε (![t, u] x)) = o.val ![val s e ε t, val s e ε u]
Theorem: LO.FirstOrder.Semiterm.val_operator₂
Proof state before:
L : Language
M : Type w
s : Structure L M
n✝ : ℕ
e : Fin n✝ → M
ξ✝ : Type u_1
ε : ξ✝ → M
o : Operator L 2
t u : Semiterm L ξ✝ n✝
⊢ (o.val fun x => val s e ε (![t, u] x)) = o.val ![val s e ε t, val s e ε u]
Tactic:
congr
Proof state after:
case e_v
L : Language
M : Type w
s : Structure L M
n✝ : ℕ
e : Fin n✝ → M
ξ✝ : Type u_1
ε : ξ✝ → M
o : Operator L 2
t u : Semiterm L ξ✝ n✝
⊢ (fun x => val s e ε (![t, u] x)) = ![val s e ε t, val s e ε u]
Theorem: LO.FirstOrder.Semiterm.val_operator₂
Proof state before:
case e_v
L : Language
M : Type w
s : Structure L M
n✝ : ℕ
e : Fin n✝ → M
ξ✝ : Type u_1
ε : ξ✝ → M
o : Operator L 2
t u : Semiterm L ξ✝ n✝
⊢ (fun x => val s e ε (![t, u] x)) = ![val s e ε t, val s e ε u]
Tactic:
funext i
Proof state after:
case e_v.h
L : Language
M : Type w
s : Structure L M
n✝ : ℕ
e : Fin n✝ → M
ξ✝ : Type u_1
ε : ξ✝ → M
o : Operator L 2
t u : Semiterm L ξ✝ n✝
i : Fin 2
⊢ val s e ε (![t, u] i) = ![val s e ε t, val s e ε u] i
Theorem: LO.FirstOrder.Semiterm.val_operator₂
Proof state before:
case e_v.h
L : Language
M : Type w
s : Structure L M
n✝ : ℕ
e : Fin n✝ → M
ξ✝ : Type u_1
ε : ξ✝ → M
o : Operator L 2
t u : Semiterm L ξ✝ n✝
i : Fin 2
⊢ val s e ε (![t, u] i) = ![val s e ε t, val s e ε u] i
Tactic:
cases' i using Fin.cases with i <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.Operator.val_comp
Proof state before:
L : Language
M : Type w
s : Structure L M
k m : ℕ
o₁ : Operator L k
o₂ : Fin k → Operator L m
v : Fin m → M
⊢ (o₁.comp o₂).val v = o₁.val fun i => (o₂ i).val v
Tactic:
simp [comp, val, val_operator]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.Operator.val_bvar
Proof state before:
L : Language
M : Type w
s : Structure L M
n : ℕ
x : Fin n
v : Fin n → M
⊢ (bvar x).val v = v x
Tactic:
simp [Operator.bvar, Operator.val]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.Operator.operator_comp
Proof state before:
L : Language
k l : ℕ
ξ : Type u_1
n : ℕ
o : Operator L k
w : Fin k → Semiterm.Operator L l
v : Fin l → Semiterm L ξ n
⊢ (o.comp w).operator v = o.operator fun x => (w x).operator v
Tactic:
simp [operator, comp, ←Rew.hom_comp_app]
Proof state after:
L : Language
k l : ℕ
ξ : Type u_1
n : ℕ
o : Operator L k
w : Fin k → Semiterm.Operator L l
v : Fin l → Semiterm L ξ n
⊢ ((Rew.substs v).comp (Rew.emb.comp (Rew.substs fun x => (w x).term))).hom o.sentence =
    ((Rew.substs fun x => (w x).operator v).comp Rew.emb).hom o.sentence
Theorem: LO.FirstOrder.Semiformula.Operator.operator_comp
Proof state before:
L : Language
k l : ℕ
ξ : Type u_1
n : ℕ
o : Operator L k
w : Fin k → Semiterm.Operator L l
v : Fin l → Semiterm L ξ n
⊢ ((Rew.substs v).comp (Rew.emb.comp (Rew.substs fun x => (w x).term))).hom o.sentence =
    ((Rew.substs fun x => (w x).operator v).comp Rew.emb).hom o.sentence
Tactic:
congr 2
Proof state after:
case e_a.e_ω
L : Language
k l : ℕ
ξ : Type u_1
n : ℕ
o : Operator L k
w : Fin k → Semiterm.Operator L l
v : Fin l → Semiterm L ξ n
⊢ (Rew.substs v).comp (Rew.emb.comp (Rew.substs fun x => (w x).term)) =
    (Rew.substs fun x => (w x).operator v).comp Rew.emb
Theorem: LO.FirstOrder.Semiformula.Operator.operator_comp
Proof state before:
case e_a.e_ω
L : Language
k l : ℕ
ξ : Type u_1
n : ℕ
o : Operator L k
w : Fin k → Semiterm.Operator L l
v : Fin l → Semiterm L ξ n
⊢ (Rew.substs v).comp (Rew.emb.comp (Rew.substs fun x => (w x).term)) =
    (Rew.substs fun x => (w x).operator v).comp Rew.emb
Tactic:
ext <;> simp [Rew.comp_app]
Proof state after:
case e_a.e_ω.hb
L : Language
k l : ℕ
ξ : Type u_1
n : ℕ
o : Operator L k
w : Fin k → Semiterm.Operator L l
v : Fin l → Semiterm L ξ n
x✝ : Fin k
⊢ (Rew.substs v) (Rew.emb (w x✝).term) = (w x✝).operator v

case e_a.e_ω.hf
L : Language
k l : ℕ
ξ : Type u_1
n : ℕ
o : Operator L k
w : Fin k → Semiterm.Operator L l
v : Fin l → Semiterm L ξ n
x✝ : Empty
⊢ (Rew.substs v) (Rew.emb &x✝) = (Rew.substs fun x => (w x).operator v) (Rew.emb &x✝)
Theorem: LO.FirstOrder.Semiformula.Operator.operator_comp
Proof state before:
case e_a.e_ω.hb
L : Language
k l : ℕ
ξ : Type u_1
n : ℕ
o : Operator L k
w : Fin k → Semiterm.Operator L l
v : Fin l → Semiterm L ξ n
x✝ : Fin k
⊢ (Rew.substs v) (Rew.emb (w x✝).term) = (w x✝).operator v
Tactic:
congr
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.Operator.operator_comp
Proof state before:
case e_a.e_ω.hf
L : Language
k l : ℕ
ξ : Type u_1
n : ℕ
o : Operator L k
w : Fin k → Semiterm.Operator L l
v : Fin l → Semiterm L ξ n
x✝ : Empty
⊢ (Rew.substs v) (Rew.emb &x✝) = (Rew.substs fun x => (w x).operator v) (Rew.emb &x✝)
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.Operator.operator_and
Proof state before:
L : Language
k : ℕ
ξ : Type u_1
n : ℕ
o₁ o₂ : Operator L k
v : Fin k → Semiterm L ξ n
⊢ (o₁.and o₂).operator v = o₁.operator v ⋏ o₂.operator v
Tactic:
simp [operator, and]
Proof state after:
no goals