internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Semiformula.neg_inj
Proof state before:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p q : Semiformula L ξ n
⊢ ~p = ~q ↔ p = q
Tactic:
constructor
Proof state after:
case mp
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p q : Semiformula L ξ n
⊢ ~p = ~q → p = q

case mpr
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p q : Semiformula L ξ n
⊢ p = q → ~p = ~q
Theorem: LO.FirstOrder.Semiformula.neg_inj
Proof state before:
case mp
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p q : Semiformula L ξ n
⊢ ~p = ~q → p = q
Tactic:
intro h
Proof state after:
case mp
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p q : Semiformula L ξ n
h : ~p = ~q
⊢ p = q
Theorem: LO.FirstOrder.Semiformula.neg_inj
Proof state before:
case mpr
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p q : Semiformula L ξ n
⊢ p = q → ~p = ~q
Tactic:
exact congr_arg _
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.neg_ball
Proof state before:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p q : Semiformula L ξ (n + 1)
⊢ ~(∀[p] q) = ∃[p] ~q
Tactic:
simp[LogicalConnective.ball, LogicalConnective.bex, imp_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.neg_bex
Proof state before:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p q : Semiformula L ξ (n + 1)
⊢ ~(∃[p] q) = ∀[p] ~q
Tactic:
simp[LogicalConnective.ball, LogicalConnective.bex, imp_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.and_inj
Proof state before:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p₁ q₁ p₂ q₂ : Semiformula L ξ n
⊢ p₁ ⋏ p₂ = q₁ ⋏ q₂ ↔ p₁ = q₁ ∧ p₂ = q₂
Tactic:
simp[Wedge.wedge]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.or_inj
Proof state before:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p₁ q₁ p₂ q₂ : Semiformula L ξ n
⊢ p₁ ⋎ p₂ = q₁ ⋎ q₂ ↔ p₁ = q₁ ∧ p₂ = q₂
Tactic:
simp[Vee.vee]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.all_inj
Proof state before:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p q : Semiformula L ξ (n + 1)
⊢ ∀' p = ∀' q ↔ p = q
Tactic:
simp[UnivQuantifier.univ]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.ex_inj
Proof state before:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p q : Semiformula L ξ (n + 1)
⊢ ∃' p = ∃' q ↔ p = q
Tactic:
simp[ExQuantifier.ex]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.univClosure_inj
Proof state before:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p q : Semiformula L ξ n
⊢ ∀* p = ∀* q ↔ p = q
Tactic:
induction n <;> simp [*, univClosure_succ]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.exClosure_inj
Proof state before:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p q : Semiformula L ξ n
⊢ ∃* p = ∃* q ↔ p = q
Tactic:
induction n <;> simp [*, exClosure_succ]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.univItr_inj
Proof state before:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ k : ℕ
p q : Semiformula L ξ (n + k)
⊢ ∀^[k] p = ∀^[k] q ↔ p = q
Tactic:
induction k <;> simp [*, univItr_succ]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.exItr_inj
Proof state before:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ k : ℕ
p q : Semiformula L ξ (n + k)
⊢ ∃^[k] p = ∃^[k] q ↔ p = q
Tactic:
induction k <;> simp [*, exItr_succ]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.imp_inj
Proof state before:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p₁ p₂ q₁ q₂ : Semiformula L ξ n
⊢ p₁ ⟶ p₂ = q₁ ⟶ q₂ ↔ p₁ = q₁ ∧ p₂ = q₂
Tactic:
simp [imp_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.complexity_neg
Proof state before:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p : Semiformula L ξ n
⊢ (~p).complexity = p.complexity
Tactic:
induction p using rec' <;> simp[*]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.fv_not
Proof state before:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
inst✝ : DecidableEq ξ
p : Semiformula L ξ n
⊢ (~p).fv = p.fv
Tactic:
induction p using rec' <;> simp [*, fv_rel, fv_nrel]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.fv_imp
Proof state before:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
inst✝ : DecidableEq ξ
p q : Semiformula L ξ n
⊢ (p ⟶ q).fv = p.fv ∪ q.fv
Tactic:
simp [imp_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.qr_neg
Proof state before:
L : Language
ξ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p : Semiformula L ξ n
⊢ (~p).qr = p.qr
Tactic:
induction' p using rec' <;> simp[*]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.qr_imply
Proof state before:
L : Language
ξ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p q : Semiformula L ξ n
⊢ (p ⟶ q).qr = max p.qr q.qr
Tactic:
simp[imp_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.qr_iff
Proof state before:
L : Language
ξ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p q : Semiformula L ξ n
⊢ (p ⟷ q).qr = max p.qr q.qr
Tactic:
simp[iff_eq, total_of]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.open_and
Proof state before:
L : Language
ξ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p q : Semiformula L ξ n
⊢ (p ⋏ q).Open ↔ p.Open ∧ q.Open
Tactic:
simp[Open]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.open_or
Proof state before:
L : Language
ξ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p q : Semiformula L ξ n
⊢ (p ⋎ q).Open ↔ p.Open ∧ q.Open
Tactic:
simp[Open]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.not_open_all
Proof state before:
L : Language
ξ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p : Semiformula L ξ (n + 1)
⊢ ¬(∀' p).Open
Tactic:
simp[Open]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.not_open_ex
Proof state before:
L : Language
ξ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p : Semiformula L ξ (n + 1)
⊢ ¬(∃' p).Open
Tactic:
simp[Open]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.open_neg
Proof state before:
L : Language
ξ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p : Semiformula L ξ n
⊢ (~p).Open ↔ p.Open
Tactic:
simp[Open]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.open_imply
Proof state before:
L : Language
ξ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p q : Semiformula L ξ n
⊢ (p ⟶ q).Open ↔ p.Open ∧ q.Open
Tactic:
simp[Open]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.open_iff
Proof state before:
L : Language
ξ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p q : Semiformula L ξ n
⊢ (p ⟷ q).Open ↔ p.Open ∧ q.Open
Tactic:
simp[Open]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.fvarList_neg
Proof state before:
L : Language
ξ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p : Semiformula L ξ n
⊢ (~p).fvarList = p.fvarList
Tactic:
induction p using rec' <;> simp[*, fvarList, ←neg_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.fvarList_sentence
Proof state before:
L : Language
ξ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
o : Type u_2
inst✝ : IsEmpty o
p : Semiformula L o n
⊢ p.fvarList = []
Tactic:
induction p using rec' <;> simp[*, fvarList, ←neg_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.not_fvar?_of_lt_upper
Proof state before:
L : Language
ξ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p : SyntacticSemiformula L n
h : upper p ≤ m
⊢ ¬fvar? p m
Tactic:
simp[upper, Nat.add_one_le_iff, fvar?] at h ⊢
Proof state after:
L : Language
ξ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p : SyntacticSemiformula L n
h : (fvarList p).toFinset.sup id < m
⊢ m ∉ fvarList p
Theorem: LO.FirstOrder.Semiformula.not_fvar?_of_lt_upper
Proof state before:
L : Language
ξ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p : SyntacticSemiformula L n
h : (fvarList p).toFinset.sup id < m
⊢ m ∉ fvarList p
Tactic:
intro hm
Proof state after:
L : Language
ξ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p : SyntacticSemiformula L n
h : (fvarList p).toFinset.sup id < m
hm : m ∈ fvarList p
⊢ False
Theorem: LO.FirstOrder.Semiformula.not_fvar?_of_lt_upper
Proof state before:
L : Language
ξ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p : SyntacticSemiformula L n
h : (fvarList p).toFinset.sup id < m
hm : m ∈ fvarList p
⊢ False
Tactic:
have : m ≤ Finset.sup p.fvarList.toFinset id :=
  Finset.le_sup (s := p.fvarList.toFinset) (b := m) (f := id) (by simpa using hm)
Proof state after:
L : Language
ξ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p : SyntacticSemiformula L n
h : (fvarList p).toFinset.sup id < m
hm : m ∈ fvarList p
this : m ≤ (fvarList p).toFinset.sup id
⊢ False
Theorem: LO.FirstOrder.Semiformula.not_fvar?_of_lt_upper
Proof state before:
L : Language
ξ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p : SyntacticSemiformula L n
h : (fvarList p).toFinset.sup id < m
hm : m ∈ fvarList p
this : m ≤ (fvarList p).toFinset.sup id
⊢ False
Tactic:
exact irrefl_of _ _ $ lt_of_lt_of_le h this
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.not_fvar?_of_lt_upper
Proof state before:
L : Language
ξ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p : SyntacticSemiformula L n
h : (fvarList p).toFinset.sup id < m
hm : m ∈ fvarList p
⊢ m ∈ (fvarList p).toFinset
Tactic:
simpa using hm
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.not_fvar?_upper
Proof state before:
L : Language
ξ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p : SyntacticSemiformula L n
⊢ upper p ≤ upper p
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.ne_of_ne_complexity
Proof state before:
L : Language
ξ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p q : Semiformula L ξ n
h : p.complexity ≠ q.complexity
⊢ p ≠ q
Tactic:
rintro rfl
Proof state after:
L : Language
ξ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p : Semiformula L ξ n
h : p.complexity ≠ p.complexity
⊢ False
Theorem: LO.FirstOrder.Semiformula.ne_of_ne_complexity
Proof state before:
L : Language
ξ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p : Semiformula L ξ n
h : p.complexity ≠ p.complexity
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.ne_or_left
Proof state before:
L : Language
ξ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p q : Semiformula L ξ n
⊢ p.complexity ≠ (p ⋎ q).complexity
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.ne_or_right
Proof state before:
L : Language
ξ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p q : Semiformula L ξ n
⊢ q.complexity ≠ (p ⋎ q).complexity
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.lMapAux_neg
Proof state before:
L✝ : Language
ξ✝ : Type u_1
n✝ n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
n : ℕ
p : Semiformula L₁ ξ n
⊢ lMapAux Φ (~p) = ~lMapAux Φ p
Tactic:
induction p using Semiformula.rec' <;> simp[*, lMapAux, ←Semiformula.neg_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.lMap_rel₀
Proof state before:
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
r : L₁.Rel 0
v : Fin 0 → Semiterm L₁ ξ n
⊢ (lMap Φ) (rel r v) = rel (Φ.rel r) ![]
Tactic:
simp[lMap_rel, Matrix.empty_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.lMap_rel₁
Proof state before:
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
r : L₁.Rel 1
t : Semiterm L₁ ξ n
⊢ (lMap Φ) (rel r ![t]) = rel (Φ.rel r) ![Semiterm.lMap Φ t]
Tactic:
simp[lMap_rel, Matrix.constant_eq_singleton]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.lMap_rel₂
Proof state before:
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
r : L₁.Rel 2
t₁ t₂ : Semiterm L₁ ξ n
⊢ (lMap Φ) (rel r ![t₁, t₂]) = rel (Φ.rel r) ![Semiterm.lMap Φ t₁, Semiterm.lMap Φ t₂]
Tactic:
simp[lMap_rel]
Proof state after:
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
r : L₁.Rel 2
t₁ t₂ : Semiterm L₁ ξ n
⊢ (fun i => Semiterm.lMap Φ (![t₁, t₂] i)) = ![Semiterm.lMap Φ t₁, Semiterm.lMap Φ t₂]
Theorem: LO.FirstOrder.Semiformula.lMap_rel₂
Proof state before:
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
r : L₁.Rel 2
t₁ t₂ : Semiterm L₁ ξ n
⊢ (fun i => Semiterm.lMap Φ (![t₁, t₂] i)) = ![Semiterm.lMap Φ t₁, Semiterm.lMap Φ t₂]
Tactic:
funext i
Proof state after:
case h
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
r : L₁.Rel 2
t₁ t₂ : Semiterm L₁ ξ n
i : Fin 2
⊢ Semiterm.lMap Φ (![t₁, t₂] i) = ![Semiterm.lMap Φ t₁, Semiterm.lMap Φ t₂] i
Theorem: LO.FirstOrder.Semiformula.lMap_rel₂
Proof state before:
case h
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
r : L₁.Rel 2
t₁ t₂ : Semiterm L₁ ξ n
i : Fin 2
⊢ Semiterm.lMap Φ (![t₁, t₂] i) = ![Semiterm.lMap Φ t₁, Semiterm.lMap Φ t₂] i
Tactic:
induction i using Fin.induction <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.lMap_nrel₀
Proof state before:
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
r : L₁.Rel 0
v : Fin 0 → Semiterm L₁ ξ n
⊢ (lMap Φ) (nrel r v) = nrel (Φ.rel r) ![]
Tactic:
simp[lMap_nrel, Matrix.empty_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.lMap_nrel₁
Proof state before:
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
r : L₁.Rel 1
t : Semiterm L₁ ξ n
⊢ (lMap Φ) (nrel r ![t]) = nrel (Φ.rel r) ![Semiterm.lMap Φ t]
Tactic:
simp[lMap_nrel, Matrix.constant_eq_singleton]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.lMap_nrel₂
Proof state before:
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
r : L₁.Rel 2
t₁ t₂ : Semiterm L₁ ξ n
⊢ (lMap Φ) (nrel r ![t₁, t₂]) = nrel (Φ.rel r) ![Semiterm.lMap Φ t₁, Semiterm.lMap Φ t₂]
Tactic:
simp[lMap_nrel]
Proof state after:
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
r : L₁.Rel 2
t₁ t₂ : Semiterm L₁ ξ n
⊢ (fun i => Semiterm.lMap Φ (![t₁, t₂] i)) = ![Semiterm.lMap Φ t₁, Semiterm.lMap Φ t₂]
Theorem: LO.FirstOrder.Semiformula.lMap_nrel₂
Proof state before:
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
r : L₁.Rel 2
t₁ t₂ : Semiterm L₁ ξ n
⊢ (fun i => Semiterm.lMap Φ (![t₁, t₂] i)) = ![Semiterm.lMap Φ t₁, Semiterm.lMap Φ t₂]
Tactic:
funext i
Proof state after:
case h
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
r : L₁.Rel 2
t₁ t₂ : Semiterm L₁ ξ n
i : Fin 2
⊢ Semiterm.lMap Φ (![t₁, t₂] i) = ![Semiterm.lMap Φ t₁, Semiterm.lMap Φ t₂] i
Theorem: LO.FirstOrder.Semiformula.lMap_nrel₂
Proof state before:
case h
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
r : L₁.Rel 2
t₁ t₂ : Semiterm L₁ ξ n
i : Fin 2
⊢ Semiterm.lMap Φ (![t₁, t₂] i) = ![Semiterm.lMap Φ t₁, Semiterm.lMap Φ t₂] i
Tactic:
induction i using Fin.induction <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.lMap_ball
Proof state before:
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
p q : Semiformula L₁ ξ (n + 1)
⊢ (lMap Φ) (∀[p] q) = ∀[(lMap Φ) p] (lMap Φ) q
Tactic:
simp [LogicalConnective.ball]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.lMap_bex
Proof state before:
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
p q : Semiformula L₁ ξ (n + 1)
⊢ (lMap Φ) (∃[p] q) = ∃[(lMap Φ) p] (lMap Φ) q
Tactic:
simp [LogicalConnective.bex]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.lMap_univClosure
Proof state before:
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
p : Semiformula L₁ ξ n
⊢ (lMap Φ) (∀* p) = ∀* (lMap Φ) p
Tactic:
induction n <;> simp [*, univClosure_succ]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.lMap_exClosure
Proof state before:
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
p : Semiformula L₁ ξ n
⊢ (lMap Φ) (∃* p) = ∃* (lMap Φ) p
Tactic:
induction n <;> simp [*, exClosure_succ]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.lMap_univItr
Proof state before:
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
k : ℕ
p : Semiformula L₁ ξ (n + k)
⊢ (lMap Φ) (∀^[k] p) = ∀^[k] (lMap Φ) p
Tactic:
induction k <;> simp [*, univItr_succ]
Proof state after:
case succ
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
n✝ : ℕ
a✝ : ∀ (p : Semiformula L₁ ξ (n + n✝)), (lMap Φ) (∀^[n✝] p) = ∀^[n✝] (lMap Φ) p
p : Semiformula L₁ ξ (n + (n✝ + 1))
⊢ (lMap Φ) p = (lMap Φ) p
Theorem: LO.FirstOrder.Semiformula.lMap_univItr
Proof state before:
case succ
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
n✝ : ℕ
a✝ : ∀ (p : Semiformula L₁ ξ (n + n✝)), (lMap Φ) (∀^[n✝] p) = ∀^[n✝] (lMap Φ) p
p : Semiformula L₁ ξ (n + (n✝ + 1))
⊢ (lMap Φ) p = (lMap Φ) p
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.lMap_exItr
Proof state before:
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
k : ℕ
p : Semiformula L₁ ξ (n + k)
⊢ (lMap Φ) (∃^[k] p) = ∃^[k] (lMap Φ) p
Tactic:
induction k <;> simp [*, exItr_succ]
Proof state after:
case succ
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
n✝ : ℕ
a✝ : ∀ (p : Semiformula L₁ ξ (n + n✝)), (lMap Φ) (∃^[n✝] p) = ∃^[n✝] (lMap Φ) p
p : Semiformula L₁ ξ (n + (n✝ + 1))
⊢ (lMap Φ) p = (lMap Φ) p
Theorem: LO.FirstOrder.Semiformula.lMap_exItr
Proof state before:
case succ
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
n✝ : ℕ
a✝ : ∀ (p : Semiformula L₁ ξ (n + n✝)), (lMap Φ) (∃^[n✝] p) = ∃^[n✝] (lMap Φ) p
p : Semiformula L₁ ξ (n + (n✝ + 1))
⊢ (lMap Φ) p = (lMap Φ) p
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.fvarList_lMap
Proof state before:
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ✝ Φ : L₁ →ᵥ L₂
p : Semiformula L₁ ξ n
⊢ ((lMap Φ) p).fvarList = p.fvarList
Tactic:
induction p using Semiformula.rec' <;> try simp [lMap_rel, lMap_nrel, *]
Proof state after:
case hrel
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ✝ Φ : L₁ →ᵥ L₂
n✝ k✝ : ℕ
r✝ : L₁.Rel k✝
v✝ : Fin k✝ → Semiterm L₁ ξ n✝
⊢ (rel (Φ.rel r✝) fun i => Semiterm.lMap Φ (v✝ i)).fvarList = (rel r✝ v✝).fvarList

case hnrel
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ✝ Φ : L₁ →ᵥ L₂
n✝ k✝ : ℕ
r✝ : L₁.Rel k✝
v✝ : Fin k✝ → Semiterm L₁ ξ n✝
⊢ (nrel (Φ.rel r✝) fun i => Semiterm.lMap Φ (v✝ i)).fvarList = (nrel r✝ v✝).fvarList
Theorem: LO.FirstOrder.Semiformula.fvarList_lMap
Proof state before:
L✝ : Language
ξ✝ : Type u_1
n✝ n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ✝ Φ : L₁ →ᵥ L₂
n k : ℕ
r : L₁.Rel k
v : Fin k → Semiterm L₁ ξ n
⊢ (rel (Φ.rel r) fun i => Semiterm.lMap Φ (v i)).fvarList = (rel r v).fvarList
Tactic:
case hrel n k r v => simp [fvarList]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.fvarList_lMap
Proof state before:
L✝ : Language
ξ✝ : Type u_1
n✝ n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ✝ Φ : L₁ →ᵥ L₂
n k : ℕ
r : L₁.Rel k
v : Fin k → Semiterm L₁ ξ n
⊢ (nrel (Φ.rel r) fun i => Semiterm.lMap Φ (v i)).fvarList = (nrel r v).fvarList
Tactic:
case hnrel n k r v => simp [fvarList]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.fvarList_lMap
Proof state before:
case hex
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ✝ Φ : L₁ →ᵥ L₂
n✝ : ℕ
p✝ : Semiformula L₁ ξ (n✝ + 1)
a✝ : ((lMap Φ) p✝).fvarList = p✝.fvarList
⊢ ((lMap Φ) (∃' p✝)).fvarList = (∃' p✝).fvarList
Tactic:
simp [lMap_rel, lMap_nrel, *]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.fvarList_lMap
Proof state before:
L✝ : Language
ξ✝ : Type u_1
n✝ n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ✝ Φ : L₁ →ᵥ L₂
n k : ℕ
r : L₁.Rel k
v : Fin k → Semiterm L₁ ξ n
⊢ (rel (Φ.rel r) fun i => Semiterm.lMap Φ (v i)).fvarList = (rel r v).fvarList
Tactic:
simp [fvarList]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.fvarList_lMap
Proof state before:
L✝ : Language
ξ✝ : Type u_1
n✝ n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ✝ Φ : L₁ →ᵥ L₂
n k : ℕ
r : L₁.Rel k
v : Fin k → Semiterm L₁ ξ n
⊢ (nrel (Φ.rel r) fun i => Semiterm.lMap Φ (v i)).fvarList = (nrel r v).fvarList
Tactic:
simp [fvarList]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.fvEnumInv_fvEnum
Proof state before:
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
inst✝¹ : DecidableEq ξ
inst✝ : Inhabited ξ
p : Semiformula L ξ n
x : ξ
hx : x ∈ p.fvarList
⊢ p.fvEnumInv (p.fvEnum x) = x
Tactic:
simp [fvEnumInv, fvEnum]
Proof state after:
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
inst✝¹ : DecidableEq ξ
inst✝ : Inhabited ξ
p : Semiformula L ξ n
x : ξ
hx : x ∈ p.fvarList
⊢ p.fvarList.length ≤ List.indexOf x p.fvarList → default = x