internlm/Lean-Github huggingface dataset:
Theorem: LO.Modal.Standard.AxiomSet.MultiGeach.subset
Proof state before:
case left.inr
α : Type u_1
Ax : AxiomSet α
a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
iha : ∀ {l₂ : List Axioms.Geach.Taple}, as ⊆ l₂ → 𝗚𝗲(as) ⊆ 𝗚𝗲(l₂)
b : Axioms.Geach.Taple
bs : List Axioms.Geach.Taple
ihb : a ∈ bs → as ⊆ bs → 𝗴𝗲(a) ⊆ 𝗚𝗲(bs)
h : (a = b ∨ a ∈ bs) ∧ as ⊆ b :: bs
h✝ : a ∈ bs
⊢ 𝗴𝗲(a) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs)
Tactic:
apply Set.subset_union_of_subset_right $ mem (by assumption)
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.MultiGeach.subset
Proof state before:
α : Type u_1
Ax : AxiomSet α
a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
iha : ∀ {l₂ : List Axioms.Geach.Taple}, as ⊆ l₂ → 𝗚𝗲(as) ⊆ 𝗚𝗲(l₂)
b : Axioms.Geach.Taple
bs : List Axioms.Geach.Taple
ihb : a ∈ bs → as ⊆ bs → 𝗴𝗲(a) ⊆ 𝗚𝗲(bs)
h : (a = b ∨ a ∈ bs) ∧ as ⊆ b :: bs
h✝ : a ∈ bs
⊢ a ∈ bs
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.MultiGeach.subset
Proof state before:
case right
α : Type u_1
Ax : AxiomSet α
a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
iha : ∀ {l₂ : List Axioms.Geach.Taple}, as ⊆ l₂ → 𝗚𝗲(as) ⊆ 𝗚𝗲(l₂)
b : Axioms.Geach.Taple
bs : List Axioms.Geach.Taple
ihb : a ∈ bs → as ⊆ bs → 𝗴𝗲(a) ⊆ 𝗚𝗲(bs)
h : (a = b ∨ a ∈ bs) ∧ as ⊆ b :: bs
⊢ 𝗚𝗲(as) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs)
Tactic:
simpa using (iha h.2)
Proof state after:
no goals
Theorem: LO.Modal.Standard.DeductionParameter.Geach.subset_axm
Proof state before:
α : Type u_1
Ax : AxiomSet α
l₁ l₂ : List Axioms.Geach.Taple
h : autoParam (l₁ ⊆ l₂) _auto✝
⊢ Ax(𝐆𝐞(l₁)) ⊆ Ax(𝐆𝐞(l₂))
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.Modal.Standard.DeductionParameter.IsGeach.eq_axiomset
Proof state before:
α : Type u_1
Ax : AxiomSet α
L : DeductionParameter α
geach : L.IsGeach
⊢ Ax(L) = 𝗚𝗲(taples L)
Tactic:
have := geach.char
Proof state after:
α : Type u_1
Ax : AxiomSet α
L : DeductionParameter α
geach : L.IsGeach
this : L = 𝐆𝐞(taples L)
⊢ Ax(L) = 𝗚𝗲(taples L)
Theorem: LO.Modal.Standard.DeductionParameter.IsGeach.eq_axiomset
Proof state before:
α : Type u_1
Ax : AxiomSet α
L : DeductionParameter α
geach : L.IsGeach
this : L = 𝐆𝐞(taples L)
⊢ Ax(L) = 𝗚𝗲(taples L)
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.Nat.numeral_eq
Proof state before:
n : ℕ
⊢ ORingSymbol.numeral (n + 2) = n + 2
Tactic:
simp[ORingSymbol.numeral, Nat.numeral_eq (n + 1)]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.oringEmb_zero
Proof state before:
L : Language
inst✝ : L.ORing
ξ : Type u_1
n : ℕ
⊢ lMap Language.oringEmb (Operator.const op(0)) = Operator.const op(0)
Tactic:
simp [Operator.const, lMap_func, Operator.operator, Operator.Zero.term_eq, Matrix.empty_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.oringEmb_one
Proof state before:
L : Language
inst✝ : L.ORing
ξ : Type u_1
n : ℕ
⊢ lMap Language.oringEmb (Operator.const op(1)) = Operator.const op(1)
Tactic:
simp [Operator.const, lMap_func, Operator.operator, Operator.One.term_eq, Matrix.empty_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.oringEmb_add
Proof state before:
L : Language
inst✝ : L.ORing
ξ : Type u_1
n : ℕ
v : Fin 2 → Semiterm ℒₒᵣ ξ n
⊢ lMap Language.oringEmb (op(+).operator v) = (‘(!!(lMap Language.oringEmb (v 0)) + !!(lMap Language.oringEmb (v 1)))’)
Tactic:
simp [lMap_func, Rew.func, Operator.operator, Operator.Add.term_eq, Matrix.empty_eq]
Proof state after:
L : Language
inst✝ : L.ORing
ξ : Type u_1
n : ℕ
v : Fin 2 → Semiterm ℒₒᵣ ξ n
⊢ (fun i => lMap Language.oringEmb (v i)) = fun i => ![lMap Language.oringEmb (v 0), lMap Language.oringEmb (v 1)] i
Theorem: LO.FirstOrder.Semiterm.oringEmb_add
Proof state before:
L : Language
inst✝ : L.ORing
ξ : Type u_1
n : ℕ
v : Fin 2 → Semiterm ℒₒᵣ ξ n
⊢ (fun i => lMap Language.oringEmb (v i)) = fun i => ![lMap Language.oringEmb (v 0), lMap Language.oringEmb (v 1)] i
Tactic:
funext i
Proof state after:
case h
L : Language
inst✝ : L.ORing
ξ : Type u_1
n : ℕ
v : Fin 2 → Semiterm ℒₒᵣ ξ n
i : Fin 2
⊢ lMap Language.oringEmb (v i) = ![lMap Language.oringEmb (v 0), lMap Language.oringEmb (v 1)] i
Theorem: LO.FirstOrder.Semiterm.oringEmb_add
Proof state before:
case h
L : Language
inst✝ : L.ORing
ξ : Type u_1
n : ℕ
v : Fin 2 → Semiterm ℒₒᵣ ξ n
i : Fin 2
⊢ lMap Language.oringEmb (v i) = ![lMap Language.oringEmb (v 0), lMap Language.oringEmb (v 1)] i
Tactic:
cases i using Fin.cases <;> simp [Fin.eq_zero]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.oringEmb_mul
Proof state before:
L : Language
inst✝ : L.ORing
ξ : Type u_1
n : ℕ
v : Fin 2 → Semiterm ℒₒᵣ ξ n
⊢ lMap Language.oringEmb (op(*).operator v) = ‘(!!(lMap Language.oringEmb (v 0)) * !!(lMap Language.oringEmb (v 1)))’
Tactic:
simp [lMap_func, Rew.func, Operator.operator, Operator.Mul.term_eq, Matrix.empty_eq]
Proof state after:
L : Language
inst✝ : L.ORing
ξ : Type u_1
n : ℕ
v : Fin 2 → Semiterm ℒₒᵣ ξ n
⊢ (fun i => lMap Language.oringEmb (v i)) = fun i => ![lMap Language.oringEmb (v 0), lMap Language.oringEmb (v 1)] i
Theorem: LO.FirstOrder.Semiterm.oringEmb_mul
Proof state before:
L : Language
inst✝ : L.ORing
ξ : Type u_1
n : ℕ
v : Fin 2 → Semiterm ℒₒᵣ ξ n
⊢ (fun i => lMap Language.oringEmb (v i)) = fun i => ![lMap Language.oringEmb (v 0), lMap Language.oringEmb (v 1)] i
Tactic:
funext i
Proof state after:
case h
L : Language
inst✝ : L.ORing
ξ : Type u_1
n : ℕ
v : Fin 2 → Semiterm ℒₒᵣ ξ n
i : Fin 2
⊢ lMap Language.oringEmb (v i) = ![lMap Language.oringEmb (v 0), lMap Language.oringEmb (v 1)] i
Theorem: LO.FirstOrder.Semiterm.oringEmb_mul
Proof state before:
case h
L : Language
inst✝ : L.ORing
ξ : Type u_1
n : ℕ
v : Fin 2 → Semiterm ℒₒᵣ ξ n
i : Fin 2
⊢ lMap Language.oringEmb (v i) = ![lMap Language.oringEmb (v 0), lMap Language.oringEmb (v 1)] i
Tactic:
cases i using Fin.cases <;> simp [Fin.eq_zero]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.oringEmb_numeral
Proof state before:
L : Language
inst✝ : L.ORing
ξ : Type u_1
n z : ℕ
⊢ lMap Language.oringEmb (‘0’) = ‘0’
Tactic:
exact oringEmb_zero
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.oringEmb_numeral
Proof state before:
L : Language
inst✝ : L.ORing
ξ : Type u_1
n z : ℕ
⊢ lMap Language.oringEmb (‘1’) = ‘1’
Tactic:
exact oringEmb_one
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.oringEmb_numeral
Proof state before:
L : Language
inst✝ : L.ORing
ξ : Type u_1
n z✝ z : ℕ
⊢ lMap Language.oringEmb (Operator.const (Operator.numeral ℒₒᵣ (z + 2))) = Operator.const (Operator.numeral L (z + 2))
Tactic:
simp [Operator.numeral_add_two]
Proof state after:
L : Language
inst✝ : L.ORing
ξ : Type u_1
n z✝ z : ℕ
⊢ (‘(!!(lMap Language.oringEmb (Operator.operator (Operator.numeral ℒₒᵣ (z + 1)) ![])) + !!(Operator.const op(1)))’) =
    op(+).operator fun x => (![Operator.numeral L (z + 1), op(1)] x).operator ![]
Theorem: LO.FirstOrder.Semiterm.oringEmb_numeral
Proof state before:
L : Language
inst✝ : L.ORing
ξ : Type u_1
n z✝ z : ℕ
⊢ (‘(!!(lMap Language.oringEmb (Operator.operator (Operator.numeral ℒₒᵣ (z + 1)) ![])) + !!(Operator.const op(1)))’) =
    op(+).operator fun x => (![Operator.numeral L (z + 1), op(1)] x).operator ![]
Tactic:
congr
Proof state after:
case e_v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n z✝ z : ℕ
⊢ ![lMap Language.oringEmb (Operator.operator (Operator.numeral ℒₒᵣ (z + 1)) ![]), Operator.const op(1)] = fun x =>
    (![Operator.numeral L (z + 1), op(1)] x).operator ![]
Theorem: LO.FirstOrder.Semiterm.oringEmb_numeral
Proof state before:
case e_v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n z✝ z : ℕ
⊢ ![lMap Language.oringEmb (Operator.operator (Operator.numeral ℒₒᵣ (z + 1)) ![]), Operator.const op(1)] = fun x =>
    (![Operator.numeral L (z + 1), op(1)] x).operator ![]
Tactic:
funext i
Proof state after:
case e_v.h
L : Language
inst✝ : L.ORing
ξ : Type u_1
n z✝ z : ℕ
i : Fin (Nat.succ 1)
⊢ ![lMap Language.oringEmb (Operator.operator (Operator.numeral ℒₒᵣ (z + 1)) ![]), Operator.const op(1)] i =
    (![Operator.numeral L (z + 1), op(1)] i).operator ![]
Theorem: LO.FirstOrder.Semiterm.oringEmb_numeral
Proof state before:
case e_v.h
L : Language
inst✝ : L.ORing
ξ : Type u_1
n z✝ z : ℕ
i : Fin (Nat.succ 1)
⊢ ![lMap Language.oringEmb (Operator.operator (Operator.numeral ℒₒᵣ (z + 1)) ![]), Operator.const op(1)] i =
    (![Operator.numeral L (z + 1), op(1)] i).operator ![]
Tactic:
cases i using Fin.cases
Proof state after:
case e_v.h.zero
L : Language
inst✝ : L.ORing
ξ : Type u_1
n z✝ z : ℕ
⊢ ![lMap Language.oringEmb (Operator.operator (Operator.numeral ℒₒᵣ (z + 1)) ![]), Operator.const op(1)] 0 =
    (![Operator.numeral L (z + 1), op(1)] 0).operator ![]

case e_v.h.succ
L : Language
inst✝ : L.ORing
ξ : Type u_1
n z✝ z : ℕ
i✝ : Fin 1
⊢ ![lMap Language.oringEmb (Operator.operator (Operator.numeral ℒₒᵣ (z + 1)) ![]), Operator.const op(1)] i✝.succ =
    (![Operator.numeral L (z + 1), op(1)] i✝.succ).operator ![]
Theorem: LO.FirstOrder.Semiterm.oringEmb_numeral
Proof state before:
case e_v.h.zero
L : Language
inst✝ : L.ORing
ξ : Type u_1
n z✝ z : ℕ
⊢ ![lMap Language.oringEmb (Operator.operator (Operator.numeral ℒₒᵣ (z + 1)) ![]), Operator.const op(1)] 0 =
    (![Operator.numeral L (z + 1), op(1)] 0).operator ![]
Tactic:
exact oringEmb_numeral (z + 1)
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.oringEmb_numeral
Proof state before:
case e_v.h.succ
L : Language
inst✝ : L.ORing
ξ : Type u_1
n z✝ z : ℕ
i✝ : Fin 1
⊢ ![lMap Language.oringEmb (Operator.operator (Operator.numeral ℒₒᵣ (z + 1)) ![]), Operator.const op(1)] i✝.succ =
    (![Operator.numeral L (z + 1), op(1)] i✝.succ).operator ![]
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.oringEmb_eq
Proof state before:
L : Language
inst✝ : L.ORing
ξ : Type u_1
n : ℕ
v : Fin 2 → Semiterm ℒₒᵣ ξ n
⊢ (lMap Language.oringEmb) (op(=).operator v) =
    (“!!(Semiterm.lMap Language.oringEmb (v 0)) = !!(Semiterm.lMap Language.oringEmb (v 1))”)
Tactic:
simp [lMap_rel, Rew.rel, Operator.operator, Operator.Eq.sentence_eq]
Proof state after:
L : Language
inst✝ : L.ORing
ξ : Type u_1
n : ℕ
v : Fin 2 → Semiterm ℒₒᵣ ξ n
⊢ (fun i => Semiterm.lMap Language.oringEmb (v i)) = fun i =>
    ![Semiterm.lMap Language.oringEmb (v 0), Semiterm.lMap Language.oringEmb (v 1)] i
Theorem: LO.FirstOrder.Semiformula.oringEmb_eq
Proof state before:
L : Language
inst✝ : L.ORing
ξ : Type u_1
n : ℕ
v : Fin 2 → Semiterm ℒₒᵣ ξ n
⊢ (fun i => Semiterm.lMap Language.oringEmb (v i)) = fun i =>
    ![Semiterm.lMap Language.oringEmb (v 0), Semiterm.lMap Language.oringEmb (v 1)] i
Tactic:
funext i
Proof state after:
case h
L : Language
inst✝ : L.ORing
ξ : Type u_1
n : ℕ
v : Fin 2 → Semiterm ℒₒᵣ ξ n
i : Fin 2
⊢ Semiterm.lMap Language.oringEmb (v i) =
    ![Semiterm.lMap Language.oringEmb (v 0), Semiterm.lMap Language.oringEmb (v 1)] i
Theorem: LO.FirstOrder.Semiformula.oringEmb_eq
Proof state before:
case h
L : Language
inst✝ : L.ORing
ξ : Type u_1
n : ℕ
v : Fin 2 → Semiterm ℒₒᵣ ξ n
i : Fin 2
⊢ Semiterm.lMap Language.oringEmb (v i) =
    ![Semiterm.lMap Language.oringEmb (v 0), Semiterm.lMap Language.oringEmb (v 1)] i
Tactic:
cases i using Fin.cases <;> simp [Fin.eq_zero]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.oringEmb_lt
Proof state before:
L : Language
inst✝ : L.ORing
ξ : Type u_1
n : ℕ
v : Fin 2 → Semiterm ℒₒᵣ ξ n
⊢ (lMap Language.oringEmb) (op(<).operator v) =
    (“!!(Semiterm.lMap Language.oringEmb (v 0)) < !!(Semiterm.lMap Language.oringEmb (v 1))”)
Tactic:
simp [lMap_rel, Rew.rel, Operator.operator, Operator.LT.sentence_eq]
Proof state after:
L : Language
inst✝ : L.ORing
ξ : Type u_1
n : ℕ
v : Fin 2 → Semiterm ℒₒᵣ ξ n
⊢ (fun i => Semiterm.lMap Language.oringEmb (v i)) = fun i =>
    ![Semiterm.lMap Language.oringEmb (v 0), Semiterm.lMap Language.oringEmb (v 1)] i
Theorem: LO.FirstOrder.Semiformula.oringEmb_lt
Proof state before:
L : Language
inst✝ : L.ORing
ξ : Type u_1
n : ℕ
v : Fin 2 → Semiterm ℒₒᵣ ξ n
⊢ (fun i => Semiterm.lMap Language.oringEmb (v i)) = fun i =>
    ![Semiterm.lMap Language.oringEmb (v 0), Semiterm.lMap Language.oringEmb (v 1)] i
Tactic:
funext i
Proof state after:
case h
L : Language
inst✝ : L.ORing
ξ : Type u_1
n : ℕ
v : Fin 2 → Semiterm ℒₒᵣ ξ n
i : Fin 2
⊢ Semiterm.lMap Language.oringEmb (v i) =
    ![Semiterm.lMap Language.oringEmb (v 0), Semiterm.lMap Language.oringEmb (v 1)] i
Theorem: LO.FirstOrder.Semiformula.oringEmb_lt
Proof state before:
case h
L : Language
inst✝ : L.ORing
ξ : Type u_1
n : ℕ
v : Fin 2 → Semiterm ℒₒᵣ ξ n
i : Fin 2
⊢ Semiterm.lMap Language.oringEmb (v i) =
    ![Semiterm.lMap Language.oringEmb (v 0), Semiterm.lMap Language.oringEmb (v 1)] i
Tactic:
cases i using Fin.cases <;> simp [Fin.eq_zero]
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.numeral_eq_numeral
Proof state before:
L : Language
inst✝¹¹ : Operator.Zero L
inst✝¹⁰ : Operator.One L
inst✝⁹ : Operator.Add L
M : Type u
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : Structure L M
inst✝² : Structure.Zero L M
inst✝¹ : Structure.One L M
inst✝ : Structure.Add L M
⊢ Semiterm.Operator.val 0 ![] = ORingSymbol.numeral 0
Tactic:
simp[ORingSymbol.numeral, Semiterm.Operator.numeral_zero]
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.numeral_eq_numeral
Proof state before:
L : Language
inst✝¹¹ : Operator.Zero L
inst✝¹⁰ : Operator.One L
inst✝⁹ : Operator.Add L
M : Type u
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : Structure L M
inst✝² : Structure.Zero L M
inst✝¹ : Structure.One L M
inst✝ : Structure.Add L M
⊢ Semiterm.Operator.val 1 ![] = ORingSymbol.numeral 1
Tactic:
simp[ORingSymbol.numeral, Semiterm.Operator.numeral_one]
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.numeral_eq_numeral
Proof state before:
L : Language
inst✝¹¹ : Operator.Zero L
inst✝¹⁰ : Operator.One L
inst✝⁹ : Operator.Add L
M : Type u
inst✝⁸ : Zero M
inst✝⁷ : One M
inst✝⁶ : Add M
inst✝⁵ : Mul M
inst✝⁴ : LT M
inst✝³ : Structure L M
inst✝² : Structure.Zero L M
inst✝¹ : Structure.One L M
inst✝ : Structure.Add L M
z : ℕ
⊢ Semiterm.Operator.val (Operator.numeral L (z + 2)) ![] = ORingSymbol.numeral (z + 2)
Tactic:
simp[ORingSymbol.numeral, Semiterm.Operator.numeral_add_two,
  Semiterm.Operator.val_comp, Matrix.fun_eq_vec₂, numeral_eq_numeral (z + 1)]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_ballLTSucc
Proof state before:
n : ℕ
L : Language
inst✝⁹ : L.LT
inst✝⁸ : L.Zero
inst✝⁷ : L.One
inst✝⁶ : L.Add
ξ : Type u_1
M : Type u_2
s : Structure L M
inst✝⁵ : LT M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Structure.LT L M
inst✝¹ : Structure.One L M
inst✝ : Structure.Add L M
t : Semiterm L ξ n
p : Semiformula L ξ (n + 1)
e : Fin n → M
ε : ξ → M
⊢ (Eval s e ε) (ballLTSucc t p) ↔ ∀ x < val s e ε t + 1, (Eval s (x :> e) ε) p
Tactic:
simp [ballLTSucc, Operator.numeral]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_bexLTSucc
Proof state before:
n : ℕ
L : Language
inst✝⁹ : L.LT
inst✝⁸ : L.Zero
inst✝⁷ : L.One
inst✝⁶ : L.Add
ξ : Type u_1
M : Type u_2
s : Structure L M
inst✝⁵ : LT M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Structure.LT L M
inst✝¹ : Structure.One L M
inst✝ : Structure.Add L M
t : Semiterm L ξ n
p : Semiformula L ξ (n + 1)
e : Fin n → M
ε : ξ → M
⊢ (Eval s e ε) (bexLTSucc t p) ↔ ∃ x < val s e ε t + 1, (Eval s (x :> e) ε) p
Tactic:
simp [bexLTSucc, Operator.numeral]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.consistent_of_sound
Proof state before:
L : Language
inst✝¹ : Structure L ℕ
T : Theory L
F : Set (Sentence L)
inst✝ : SoundOn T F
hF : ⊥ ∈ F
b : T ⊢! ⊥
⊢ False
Tactic:
simpa using SoundOn.sound hF b
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.Operator.operator_comp
Proof state before:
L : Language
k l : ℕ
ξ : Type u_1
n : ℕ
o : Operator L k
w : Fin k → 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.comp_app]
Proof state after:
L : Language
k l : ℕ
ξ : Type u_1
n : ℕ
o : Operator L k
w : Fin k → Operator L l
v : Fin l → Semiterm L ξ n
⊢ ((Rew.substs v).comp (Rew.emb.comp (Rew.substs fun x => (w x).term))) o.term =
    ((Rew.substs fun x => ((Rew.substs v).comp Rew.emb) (w x).term).comp Rew.emb) o.term
Theorem: LO.FirstOrder.Semiterm.Operator.operator_comp
Proof state before:
L : Language
k l : ℕ
ξ : Type u_1
n : ℕ
o : Operator L k
w : Fin k → Operator L l
v : Fin l → Semiterm L ξ n
⊢ ((Rew.substs v).comp (Rew.emb.comp (Rew.substs fun x => (w x).term))) o.term =
    ((Rew.substs fun x => ((Rew.substs v).comp Rew.emb) (w x).term).comp Rew.emb) o.term
Tactic:
congr 1
Proof state after:
case e_a
L : Language
k l : ℕ
ξ : Type u_1
n : ℕ
o : Operator L k
w : Fin k → 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 => ((Rew.substs v).comp Rew.emb) (w x).term).comp Rew.emb
Theorem: LO.FirstOrder.Semiterm.Operator.operator_comp
Proof state before:
case e_a
L : Language
k l : ℕ
ξ : Type u_1
n : ℕ
o : Operator L k
w : Fin k → 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 => ((Rew.substs v).comp Rew.emb) (w x).term).comp Rew.emb
Tactic:
ext <;> simp [Rew.comp_app]
Proof state after:
case e_a.hf
L : Language
k l : ℕ
ξ : Type u_1
n : ℕ
o : Operator L k
w : Fin k → Operator L l
v : Fin l → Semiterm L ξ n
x✝ : Empty
⊢ (Rew.substs v) (Rew.emb &x✝) = (Rew.substs fun x => (Rew.substs v) (Rew.emb (w x).term)) (Rew.emb &x✝)
Theorem: LO.FirstOrder.Semiterm.Operator.operator_comp
Proof state before:
case e_a.hf
L : Language
k l : ℕ
ξ : Type u_1
n : ℕ
o : Operator L k
w : Fin k → Operator L l
v : Fin l → Semiterm L ξ n
x✝ : Empty
⊢ (Rew.substs v) (Rew.emb &x✝) = (Rew.substs fun x => (Rew.substs v) (Rew.emb (w x).term)) (Rew.emb &x✝)
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.Operator.operator_bvar
Proof state before:
L : Language
k : ℕ
ξ : Type u_1
n : ℕ
x : Fin k
v : Fin k → Semiterm L ξ n
⊢ (bvar x).operator v = v x
Tactic:
simp [operator, bvar]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.Operator.bv_operator
Proof state before:
L : Language
ξ : Type u_1
n k : ℕ
o : Operator L k
v : Fin k → Semiterm L ξ (n + 1)
⊢ (o.operator v).bv = o.term.bv.biUnion fun i => (v i).bv
Tactic:
simp [operator]
Proof state after:
L : Language
ξ : Type u_1
n k : ℕ
o : Operator L k
v : Fin k → Semiterm L ξ (n + 1)
⊢ ((Rew.substs v) (Rew.emb o.term)).bv = o.term.bv.biUnion fun i => (v i).bv
Theorem: LO.FirstOrder.Semiterm.Operator.bv_operator
Proof state before:
L : Language
ξ : Type u_1
n k : ℕ
o : Operator L k
v : Fin k → Semiterm L ξ (n + 1)
⊢ ((Rew.substs v) (Rew.emb o.term)).bv = o.term.bv.biUnion fun i => (v i).bv
Tactic:
generalize o.term = s
Proof state after:
L : Language
ξ : Type u_1
n k : ℕ
o : Operator L k
v : Fin k → Semiterm L ξ (n + 1)
s : Semiterm L Empty k
⊢ ((Rew.substs v) (Rew.emb s)).bv = s.bv.biUnion fun i => (v i).bv
Theorem: LO.FirstOrder.Semiterm.Operator.bv_operator
Proof state before:
L : Language
ξ : Type u_1
n k : ℕ
o : Operator L k
v : Fin k → Semiterm L ξ (n + 1)
s : Semiterm L Empty k
⊢ ((Rew.substs v) (Rew.emb s)).bv = s.bv.biUnion fun i => (v i).bv
Tactic:
induction s <;> try simp [Rew.func, bv_func, Finset.biUnion_biUnion, *]
Proof state after:
case fvar
L : Language
ξ : Type u_1
n k : ℕ
o : Operator L k
v : Fin k → Semiterm L ξ (n + 1)
a✝ : Empty
⊢ ((Rew.substs v) (Rew.emb &a✝)).bv = ∅
Theorem: LO.FirstOrder.Semiterm.Operator.bv_operator
Proof state before:
L : Language
ξ : Type u_1
n k : ℕ
o : Operator L k
v : Fin k → Semiterm L ξ (n + 1)
a✝ : Empty
⊢ ((Rew.substs v) (Rew.emb &a✝)).bv = ∅
Tactic:
case fvar => contradiction
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.Operator.bv_operator
Proof state before:
case func
L : Language
ξ : Type u_1
n k : ℕ
o : Operator L k
v : Fin k → Semiterm L ξ (n + 1)
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → Semiterm L Empty k
a_ih✝ : ∀ (a : Fin arity✝), ((Rew.substs v) (Rew.emb (a✝ a))).bv = (a✝ a).bv.biUnion fun i => (v i).bv
⊢ ((Rew.substs v) (Rew.emb (func a✝¹ a✝))).bv = (func a✝¹ a✝).bv.biUnion fun i => (v i).bv
Tactic:
simp [Rew.func, bv_func, Finset.biUnion_biUnion, *]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.Operator.bv_operator
Proof state before:
L : Language
ξ : Type u_1
n k : ℕ
o : Operator L k
v : Fin k → Semiterm L ξ (n + 1)
a✝ : Empty
⊢ ((Rew.substs v) (Rew.emb &a✝)).bv = ∅
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.Operator.positive_operator_iff
Proof state before:
L : Language
ξ : Type u_1
n k : ℕ
o : Operator L k
v : Fin k → Semiterm L ξ (n + 1)
⊢ (o.operator v).Positive ↔ ∀ i ∈ o.term.bv, (v i).Positive
Tactic:
simp [Positive, bv_operator]
Proof state after:
L : Language
ξ : Type u_1
n k : ℕ
o : Operator L k
v : Fin k → Semiterm L ξ (n + 1)
⊢ (∀ (x : Fin (n + 1)), ∀ x_1 ∈ o.term.bv, x ∈ (v x_1).bv → 0 < x) ↔ ∀ i ∈ o.term.bv, ∀ x ∈ (v i).bv, 0 < x
Theorem: LO.FirstOrder.Semiterm.Operator.positive_operator_iff
Proof state before:
L : Language
ξ : Type u_1
n k : ℕ
o : Operator L k
v : Fin k → Semiterm L ξ (n + 1)
⊢ (∀ (x : Fin (n + 1)), ∀ x_1 ∈ o.term.bv, x ∈ (v x_1).bv → 0 < x) ↔ ∀ i ∈ o.term.bv, ∀ x ∈ (v i).bv, 0 < x
Tactic:
exact ⟨fun h i hi x hx ↦ h x i hi hx, fun h x i hi hx ↦ h i hi x hx⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.Operator.positive_const
Proof state before:
L : Language
ξ : Type u_1
n : ℕ
c : Const L
⊢ (const c).Positive
Tactic:
simp [const, positive_operator_iff]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.Operator.operator_foldr_cons
Proof state before:
L : Language
k : ℕ
ξ : Type u_1
n : ℕ
f : Operator L 2
z o : Operator L k
os : List (Operator L k)
v : Fin k → Semiterm L ξ n
⊢ (f.foldr z (o :: os)).operator v = f.operator ![(f.foldr z os).operator v, o.operator v]
Tactic:
simp [foldr, operator_comp, Matrix.fun_eq_vec₂]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.Operator.numeral_zero
Proof state before:
L : Language
hz : Operator.Zero L
ho : Operator.One L
ha : Operator.Add L
⊢ numeral L 0 = op(0)
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.Operator.numeral_one
Proof state before:
L : Language
hz : Operator.Zero L
ho : Operator.One L
ha : Operator.Add L
⊢ numeral L 1 = op(1)
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.Operator.numeral_succ
Proof state before:
L : Language
hz✝ : Operator.Zero L
ho : Operator.One L
ha : Operator.Add L
z : ℕ
hz : z ≠ 0
⊢ numeral L (z + 1) = op(+).comp ![numeral L z, op(1)]
Tactic:
simp [numeral]
Proof state after:
L : Language
hz✝ : Operator.Zero L
ho : Operator.One L
ha : Operator.Add L
z : ℕ
hz : z ≠ 0
⊢ op(+).foldr op(1) (List.replicate z op(1)) =
    op(+).comp
      ![match z with
        | 0 => op(0)
        | n.succ => op(+).foldr op(1) (List.replicate n op(1)),
        op(1)]
Theorem: LO.FirstOrder.Semiterm.Operator.numeral_succ
Proof state before:
L : Language
hz✝ : Operator.Zero L
ho : Operator.One L
ha : Operator.Add L
z : ℕ
hz : z ≠ 0
⊢ op(+).foldr op(1) (List.replicate z op(1)) =
    op(+).comp
      ![match z with
        | 0 => op(0)
        | n.succ => op(+).foldr op(1) (List.replicate n op(1)),
        op(1)]
Tactic:
cases' z with z
Proof state after:
case zero
L : Language
hz✝ : Operator.Zero L
ho : Operator.One L
ha : Operator.Add L
hz : 0 ≠ 0
⊢ op(+).foldr op(1) (List.replicate 0 op(1)) =
    op(+).comp
      ![match 0 with
        | 0 => op(0)
        | n.succ => op(+).foldr op(1) (List.replicate n op(1)),
        op(1)]

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)]
Theorem: LO.FirstOrder.Semiterm.Operator.numeral_succ
Proof state before:
case zero
L : Language
hz✝ : Operator.Zero L
ho : Operator.One L
ha : Operator.Add L
hz : 0 ≠ 0
⊢ op(+).foldr op(1) (List.replicate 0 op(1)) =
    op(+).comp
      ![match 0 with
        | 0 => op(0)
        | n.succ => op(+).foldr op(1) (List.replicate n op(1)),
        op(1)]
Tactic:
simp at hz
Proof state after:
no goals