internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Rew.nrel1
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₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
r : L.Rel 1
t : Semiterm L ξ₁ n₁
⊢ ω.hom (nrel r ![t]) = nrel r ![ω t]
Tactic:
simp[ω.nrel, Matrix.constant_eq_singleton]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.nrel2
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₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
r : L.Rel 2
t₁ t₂ : Semiterm L ξ₁ n₁
⊢ ω.hom (nrel r ![t₁, t₂]) = nrel r ![ω t₁, ω t₂]
Tactic:
simp[ω.nrel]
Proof state after:
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₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
r : L.Rel 2
t₁ t₂ : Semiterm L ξ₁ n₁
⊢ (fun i => ω (![t₁, t₂] i)) = ![ω t₁, ω t₂]
Theorem: LO.FirstOrder.Rew.nrel2
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₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
r : L.Rel 2
t₁ t₂ : Semiterm L ξ₁ n₁
⊢ (fun i => ω (![t₁, t₂] i)) = ![ω t₁, ω t₂]
Tactic:
funext i
Proof state after:
case h
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₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
r : L.Rel 2
t₁ t₂ : Semiterm L ξ₁ n₁
i : Fin 2
⊢ ω (![t₁, t₂] i) = ![ω t₁, ω t₂] i
Theorem: LO.FirstOrder.Rew.nrel2
Proof state before:
case h
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₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
r : L.Rel 2
t₁ t₂ : Semiterm L ξ₁ n₁
i : Fin 2
⊢ ω (![t₁, t₂] i) = ![ω t₁, ω t₂] i
Tactic:
induction i using Fin.induction <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.nrel3
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₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
r : L.Rel 3
t₁ t₂ t₃ : Semiterm L ξ₁ n₁
⊢ ω.hom (nrel r ![t₁, t₂, t₃]) = nrel r ![ω t₁, ω t₂, ω t₃]
Tactic:
simp[ω.nrel]
Proof state after:
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₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
r : L.Rel 3
t₁ t₂ t₃ : Semiterm L ξ₁ n₁
⊢ (fun i => ω (![t₁, t₂, t₃] i)) = ![ω t₁, ω t₂, ω t₃]
Theorem: LO.FirstOrder.Rew.nrel3
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₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
r : L.Rel 3
t₁ t₂ t₃ : Semiterm L ξ₁ n₁
⊢ (fun i => ω (![t₁, t₂, t₃] i)) = ![ω t₁, ω t₂, ω t₃]
Tactic:
funext i
Proof state after:
case h
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₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
r : L.Rel 3
t₁ t₂ t₃ : Semiterm L ξ₁ n₁
i : Fin 3
⊢ ω (![t₁, t₂, t₃] i) = ![ω t₁, ω t₂, ω t₃] i
Theorem: LO.FirstOrder.Rew.nrel3
Proof state before:
case h
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₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
r : L.Rel 3
t₁ t₂ t₃ : Semiterm L ξ₁ n₁
i : Fin 3
⊢ ω (![t₁, t₂, t₃] i) = ![ω t₁, ω t₂, ω t₃] i
Tactic:
induction' i using Fin.induction with i <;> simp
Proof state after:
case h.succ
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₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
r : L.Rel 3
t₁ t₂ t₃ : Semiterm L ξ₁ n₁
i : Fin 2
a✝ : ω (![t₁, t₂, t₃] i.castSucc) = ![ω t₁, ω t₂, ω t₃] i.castSucc
⊢ ω (![t₂, t₃] i) = ![ω t₂, ω t₃] i
Theorem: LO.FirstOrder.Rew.nrel3
Proof state before:
case h.succ
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₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
r : L.Rel 3
t₁ t₂ t₃ : Semiterm L ξ₁ n₁
i : Fin 2
a✝ : ω (![t₁, t₂, t₃] i.castSucc) = ![ω t₁, ω t₂, ω t₃] i.castSucc
⊢ ω (![t₂, t₃] i) = ![ω t₂, ω t₃] i
Tactic:
induction' i using Fin.induction with i <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.all
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₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
p : Semiformula L ξ₁ (n₁ + 1)
⊢ ω.hom (∀' p) = ∀' ω.q.hom p
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.ex
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₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
p : Semiformula L ξ₁ (n₁ + 1)
⊢ ω.hom (∃' p) = ∃' ω.q.hom p
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.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₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
p q : Semiformula L ξ₁ (n₁ + 1)
⊢ ω.hom (∀[p] q) = ∀[ω.q.hom p] ω.q.hom q
Tactic:
simp[ball_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.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₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
p q : Semiformula L ξ₁ (n₁ + 1)
⊢ ω.hom (∃[p] q) = ∃[ω.q.hom p] ω.q.hom q
Tactic:
simp[bex_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.complexity
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₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
p : Semiformula L ξ₁ n₁
⊢ (ω.hom p).complexity = p.complexity
Tactic:
induction p using Semiformula.rec' generalizing n₂ <;> simp[*, Rew.rel, Rew.nrel]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.hom_ext'
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₃ : ℕ
ω ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
h : ω₁ = ω₂
p : Semiformula L ξ₁ n₁
⊢ ω₁.hom p = ω₂.hom p
Tactic:
simp[h]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.hom_id_eq
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₃ : ℕ
⊢ Rew.id.hom = LogicalConnective.Hom.id
Tactic:
ext p
Proof state after:
case h
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
⊢ Rew.id.hom p = LogicalConnective.Hom.id p
Theorem: LO.FirstOrder.Rew.hom_id_eq
Proof state before:
case h
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
⊢ Rew.id.hom p = LogicalConnective.Hom.id p
Tactic:
induction p using Semiformula.rec' <;> simp[Rew.rel, Rew.nrel, *]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.hom_comp_eq
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₃ n₃ : ℕ
ω₂ : Rew L ξ₂ n₂ ξ₃ n₃
ω₁ : Rew L ξ₁ n₁ ξ₂ n₂
⊢ (ω₂.comp ω₁).hom = ω₂.hom.comp ω₁.hom
Tactic:
ext p
Proof state after:
case h
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₃ n₃ : ℕ
ω₂ : Rew L ξ₂ n₂ ξ₃ n₃
ω₁ : Rew L ξ₁ n₁ ξ₂ n₂
p : Semiformula L ξ₁ n₁
⊢ (ω₂.comp ω₁).hom p = (ω₂.hom.comp ω₁.hom) p
Theorem: LO.FirstOrder.Rew.hom_comp_eq
Proof state before:
case h
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₃ n₃ : ℕ
ω₂ : Rew L ξ₂ n₂ ξ₃ n₃
ω₁ : Rew L ξ₁ n₁ ξ₂ n₂
p : Semiformula L ξ₁ n₁
⊢ (ω₂.comp ω₁).hom p = (ω₂.hom.comp ω₁.hom) p
Tactic:
simp
Proof state after:
case h
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₃ n₃ : ℕ
ω₂ : Rew L ξ₂ n₂ ξ₃ n₃
ω₁ : Rew L ξ₁ n₁ ξ₂ n₂
p : Semiformula L ξ₁ n₁
⊢ (ω₂.comp ω₁).hom p = ω₂.hom (ω₁.hom p)
Theorem: LO.FirstOrder.Rew.hom_comp_eq
Proof state before:
case h
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₃ n₃ : ℕ
ω₂ : Rew L ξ₂ n₂ ξ₃ n₃
ω₁ : Rew L ξ₁ n₁ ξ₂ n₂
p : Semiformula L ξ₁ n₁
⊢ (ω₂.comp ω₁).hom p = ω₂.hom (ω₁.hom p)
Tactic:
induction p using Semiformula.rec' generalizing n₂ n₃ <;> simp[Rew.rel, Rew.nrel, comp_app, q_comp, *]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.hom_comp_app
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₃ n₃ : ℕ
ω₂ : Rew L ξ₂ n₂ ξ₃ n₃
ω₁ : Rew L ξ₁ n₁ ξ₂ n₂
p : Semiformula L ξ₁ n₁
⊢ (ω₂.comp ω₁).hom p = ω₂.hom (ω₁.hom p)
Tactic:
simp[hom_comp_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.mapl_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₃ x✝⁶ x✝⁵ : ℕ
ξ✝ : Type u_5
x✝⁴ : Type u_6
x✝³ : Fin x✝⁶ → Fin x✝⁵
x✝² : ξ✝ → x✝⁴
x✝¹ : Function.Injective x✝³
x✝ : Function.Injective x✝²
p : Semiformula L ξ✝ x✝⁶
⊢ (map x✝³ x✝²).hom ⊤ = (map x✝³ x✝²).hom p → ⊤ = p
Tactic:
cases p using cases' <;> simp[Rew.rel, Rew.nrel]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.mapl_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₃ x✝⁶ x✝⁵ : ℕ
ξ✝ : Type u_5
x✝⁴ : Type u_6
x✝³ : Fin x✝⁶ → Fin x✝⁵
x✝² : ξ✝ → x✝⁴
x✝¹ : Function.Injective x✝³
x✝ : Function.Injective x✝²
p : Semiformula L ξ✝ x✝⁶
⊢ (map x✝³ x✝²).hom ⊥ = (map x✝³ x✝²).hom p → ⊥ = p
Tactic:
cases p using cases' <;> simp[Rew.rel, Rew.nrel]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.mapl_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₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L ξ✝ x✝⁴
p : Semiformula L ξ✝ x✝⁴
⊢ (map x✝¹ x✝).hom (rel r v) = (map x✝¹ x✝).hom p → rel r v = p
Tactic:
cases p using cases' <;> simp[Rew.rel, Rew.nrel]
Proof state after:
case hrel
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₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L ξ✝ x✝⁴
k✝ : ℕ
r✝ : L.Rel k✝
v✝ : Fin k✝ → Semiterm L ξ✝ x✝⁴
⊢ arity✝ = k✝ →
    HEq r r✝ → (HEq (fun i => (map x✝¹ x✝) (v i)) fun i => (map x✝¹ x✝) (v✝ i)) → arity✝ = k✝ ∧ HEq r r✝ ∧ HEq v v✝
Theorem: LO.FirstOrder.Rew.mapl_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₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L ξ✝ x✝⁴
k✝ : ℕ
r✝ : L.Rel k✝
v✝ : Fin k✝ → Semiterm L ξ✝ x✝⁴
⊢ arity✝ = k✝ →
    HEq r r✝ → (HEq (fun i => (map x✝¹ x✝) (v i)) fun i => (map x✝¹ x✝) (v✝ i)) → arity✝ = k✝ ∧ HEq r r✝ ∧ HEq v v✝
Tactic:
case hrel =>
  rintro rfl; simp; rintro rfl h; simp
  funext i; exact map_inj hb hf (congr_fun h i)
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.mapl_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₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L ξ✝ x✝⁴
k✝ : ℕ
r✝ : L.Rel k✝
v✝ : Fin k✝ → Semiterm L ξ✝ x✝⁴
⊢ arity✝ = k✝ →
    HEq r r✝ → (HEq (fun i => (map x✝¹ x✝) (v i)) fun i => (map x✝¹ x✝) (v✝ i)) → arity✝ = k✝ ∧ HEq r r✝ ∧ HEq v v✝
Tactic:
rintro rfl
Proof state after:
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₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L ξ✝ x✝⁴
r✝ : L.Rel arity✝
v✝ : Fin arity✝ → Semiterm L ξ✝ x✝⁴
⊢ HEq r r✝ → (HEq (fun i => (map x✝¹ x✝) (v i)) fun i => (map x✝¹ x✝) (v✝ i)) → arity✝ = arity✝ ∧ HEq r r✝ ∧ HEq v v✝
Theorem: LO.FirstOrder.Rew.mapl_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₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L ξ✝ x✝⁴
r✝ : L.Rel arity✝
v✝ : Fin arity✝ → Semiterm L ξ✝ x✝⁴
⊢ HEq r r✝ → (HEq (fun i => (map x✝¹ x✝) (v i)) fun i => (map x✝¹ x✝) (v✝ i)) → arity✝ = arity✝ ∧ HEq r r✝ ∧ HEq v v✝
Tactic:
simp
Proof state after:
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₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L ξ✝ x✝⁴
r✝ : L.Rel arity✝
v✝ : Fin arity✝ → Semiterm L ξ✝ x✝⁴
⊢ r = r✝ → ((fun i => (map x✝¹ x✝) (v i)) = fun i => (map x✝¹ x✝) (v✝ i)) → r = r✝ ∧ v = v✝
Theorem: LO.FirstOrder.Rew.mapl_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₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L ξ✝ x✝⁴
r✝ : L.Rel arity✝
v✝ : Fin arity✝ → Semiterm L ξ✝ x✝⁴
⊢ r = r✝ → ((fun i => (map x✝¹ x✝) (v i)) = fun i => (map x✝¹ x✝) (v✝ i)) → r = r✝ ∧ v = v✝
Tactic:
rintro rfl h
Proof state after:
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₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
arity✝ : ℕ
r : L.Rel arity✝
v v✝ : Fin arity✝ → Semiterm L ξ✝ x✝⁴
h : (fun i => (map x✝¹ x✝) (v i)) = fun i => (map x✝¹ x✝) (v✝ i)
⊢ r = r ∧ v = v✝
Theorem: LO.FirstOrder.Rew.mapl_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₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
arity✝ : ℕ
r : L.Rel arity✝
v v✝ : Fin arity✝ → Semiterm L ξ✝ x✝⁴
h : (fun i => (map x✝¹ x✝) (v i)) = fun i => (map x✝¹ x✝) (v✝ i)
⊢ r = r ∧ v = v✝
Tactic:
simp
Proof state after:
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₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
arity✝ : ℕ
r : L.Rel arity✝
v v✝ : Fin arity✝ → Semiterm L ξ✝ x✝⁴
h : (fun i => (map x✝¹ x✝) (v i)) = fun i => (map x✝¹ x✝) (v✝ i)
⊢ v = v✝
Theorem: LO.FirstOrder.Rew.mapl_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₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
arity✝ : ℕ
r : L.Rel arity✝
v v✝ : Fin arity✝ → Semiterm L ξ✝ x✝⁴
h : (fun i => (map x✝¹ x✝) (v i)) = fun i => (map x✝¹ x✝) (v✝ i)
⊢ v = v✝
Tactic:
funext i
Proof state after:
case h
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₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
arity✝ : ℕ
r : L.Rel arity✝
v v✝ : Fin arity✝ → Semiterm L ξ✝ x✝⁴
h : (fun i => (map x✝¹ x✝) (v i)) = fun i => (map x✝¹ x✝) (v✝ i)
i : Fin arity✝
⊢ v i = v✝ i
Theorem: LO.FirstOrder.Rew.mapl_inj
Proof state before:
case h
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₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
arity✝ : ℕ
r : L.Rel arity✝
v v✝ : Fin arity✝ → Semiterm L ξ✝ x✝⁴
h : (fun i => (map x✝¹ x✝) (v i)) = fun i => (map x✝¹ x✝) (v✝ i)
i : Fin arity✝
⊢ v i = v✝ i
Tactic:
exact map_inj hb hf (congr_fun h i)
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.mapl_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₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L ξ✝ x✝⁴
p : Semiformula L ξ✝ x✝⁴
⊢ (map x✝¹ x✝).hom (nrel r v) = (map x✝¹ x✝).hom p → nrel r v = p
Tactic:
cases p using cases' <;> simp[Rew.rel, Rew.nrel]
Proof state after:
case hnrel
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₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L ξ✝ x✝⁴
k✝ : ℕ
r✝ : L.Rel k✝
v✝ : Fin k✝ → Semiterm L ξ✝ x✝⁴
⊢ arity✝ = k✝ →
    HEq r r✝ → (HEq (fun i => (map x✝¹ x✝) (v i)) fun i => (map x✝¹ x✝) (v✝ i)) → arity✝ = k✝ ∧ HEq r r✝ ∧ HEq v v✝
Theorem: LO.FirstOrder.Rew.mapl_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₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L ξ✝ x✝⁴
k✝ : ℕ
r✝ : L.Rel k✝
v✝ : Fin k✝ → Semiterm L ξ✝ x✝⁴
⊢ arity✝ = k✝ →
    HEq r r✝ → (HEq (fun i => (map x✝¹ x✝) (v i)) fun i => (map x✝¹ x✝) (v✝ i)) → arity✝ = k✝ ∧ HEq r r✝ ∧ HEq v v✝
Tactic:
case hnrel =>
  rintro rfl; simp; rintro rfl h; simp
  funext i; exact map_inj hb hf (congr_fun h i)
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.mapl_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₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
p q r : Semiformula L ξ✝ x✝⁴
⊢ (map x✝¹ x✝).hom (p ⋏ q) = (map x✝¹ x✝).hom r → p ⋏ q = r
Tactic:
cases r using cases' <;> simp[Rew.rel, Rew.nrel]
Proof state after:
case hand
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₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
p q p✝ q✝ : Semiformula L ξ✝ x✝⁴
⊢ (map x✝¹ x✝).hom p = (map x✝¹ x✝).hom p✝ → (map x✝¹ x✝).hom q = (map x✝¹ x✝).hom q✝ → p = p✝ ∧ q = q✝
Theorem: LO.FirstOrder.Rew.mapl_inj
Proof state before:
case hand
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₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
p q p✝ q✝ : Semiformula L ξ✝ x✝⁴
⊢ (map x✝¹ x✝).hom p = (map x✝¹ x✝).hom p✝ → (map x✝¹ x✝).hom q = (map x✝¹ x✝).hom q✝ → p = p✝ ∧ q = q✝
Tactic:
intro hp hq
Proof state after:
case hand
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₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
p q p✝ q✝ : Semiformula L ξ✝ x✝⁴
hp : (map x✝¹ x✝).hom p = (map x✝¹ x✝).hom p✝
hq : (map x✝¹ x✝).hom q = (map x✝¹ x✝).hom q✝
⊢ p = p✝ ∧ q = q✝
Theorem: LO.FirstOrder.Rew.mapl_inj
Proof state before:
case hand
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₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
p q p✝ q✝ : Semiformula L ξ✝ x✝⁴
hp : (map x✝¹ x✝).hom p = (map x✝¹ x✝).hom p✝
hq : (map x✝¹ x✝).hom q = (map x✝¹ x✝).hom q✝
⊢ p = p✝ ∧ q = q✝
Tactic:
exact ⟨mapl_inj hb hf hp, mapl_inj hb hf hq⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.mapl_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₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
p q r : Semiformula L ξ✝ x✝⁴
⊢ (map x✝¹ x✝).hom (p ⋎ q) = (map x✝¹ x✝).hom r → p ⋎ q = r
Tactic:
cases r using cases' <;> simp[Rew.rel, Rew.nrel]
Proof state after:
case hor
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₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
p q p✝ q✝ : Semiformula L ξ✝ x✝⁴
⊢ (map x✝¹ x✝).hom p = (map x✝¹ x✝).hom p✝ → (map x✝¹ x✝).hom q = (map x✝¹ x✝).hom q✝ → p = p✝ ∧ q = q✝
Theorem: LO.FirstOrder.Rew.mapl_inj
Proof state before:
case hor
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₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
p q p✝ q✝ : Semiformula L ξ✝ x✝⁴
⊢ (map x✝¹ x✝).hom p = (map x✝¹ x✝).hom p✝ → (map x✝¹ x✝).hom q = (map x✝¹ x✝).hom q✝ → p = p✝ ∧ q = q✝
Tactic:
intro hp hq
Proof state after:
case hor
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₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
p q p✝ q✝ : Semiformula L ξ✝ x✝⁴
hp : (map x✝¹ x✝).hom p = (map x✝¹ x✝).hom p✝
hq : (map x✝¹ x✝).hom q = (map x✝¹ x✝).hom q✝
⊢ p = p✝ ∧ q = q✝
Theorem: LO.FirstOrder.Rew.mapl_inj
Proof state before:
case hor
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₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
p q p✝ q✝ : Semiformula L ξ✝ x✝⁴
hp : (map x✝¹ x✝).hom p = (map x✝¹ x✝).hom p✝
hq : (map x✝¹ x✝).hom q = (map x✝¹ x✝).hom q✝
⊢ p = p✝ ∧ q = q✝
Tactic:
exact ⟨mapl_inj hb hf hp, mapl_inj hb hf hq⟩
Proof state after:
no goals