internlm/Lean-Github huggingface dataset:
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
b : Fin x✝² → Fin x✝¹
e : ξ✝ → x✝
hb : Function.Injective b
hf : Function.Injective e
p : Semiformula L ξ✝ (x✝² + 1)
q : Semiformula L ξ✝ x✝²
⊢ (map b e).hom (∀' p) = (map b e).hom q → ∀' p = q
Tactic:
cases q using cases' <;> simp[Rew.rel, Rew.nrel, q_map]
Proof state after:
case hall
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
b : Fin x✝² → Fin x✝¹
e : ξ✝ → x✝
hb : Function.Injective b
hf : Function.Injective e
p p✝ : Semiformula L ξ✝ (x✝² + 1)
⊢ (map (0 :> Fin.succ ∘ b) e).hom p = (map (0 :> Fin.succ ∘ b) e).hom p✝ → p = p✝
Theorem: LO.FirstOrder.Rew.mapl_inj
Proof state before:
case hall
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
b : Fin x✝² → Fin x✝¹
e : ξ✝ → x✝
hb : Function.Injective b
hf : Function.Injective e
p p✝ : Semiformula L ξ✝ (x✝² + 1)
⊢ (map (0 :> Fin.succ ∘ b) e).hom p = (map (0 :> Fin.succ ∘ b) e).hom p✝ → p = p✝
Tactic:
intro h
Proof state after:
case hall
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
b : Fin x✝² → Fin x✝¹
e : ξ✝ → x✝
hb : Function.Injective b
hf : Function.Injective e
p p✝ : Semiformula L ξ✝ (x✝² + 1)
h : (map (0 :> Fin.succ ∘ b) e).hom p = (map (0 :> Fin.succ ∘ b) e).hom p✝
⊢ p = p✝
Theorem: LO.FirstOrder.Rew.mapl_inj
Proof state before:
case hall
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
b : Fin x✝² → Fin x✝¹
e : ξ✝ → x✝
hb : Function.Injective b
hf : Function.Injective e
p p✝ : Semiformula L ξ✝ (x✝² + 1)
h : (map (0 :> Fin.succ ∘ b) e).hom p = (map (0 :> Fin.succ ∘ b) e).hom p✝
⊢ p = p✝
Tactic:
exact mapl_inj (b := 0 :> Fin.succ ∘ b)
(Matrix.injective_vecCons ((Fin.succ_injective _).comp hb) (fun _ => (Fin.succ_ne_zero _).symm)) hf h
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
b : Fin x✝² → Fin x✝¹
e : ξ✝ → x✝
hb : Function.Injective b
hf : Function.Injective e
p : Semiformula L ξ✝ (x✝² + 1)
q : Semiformula L ξ✝ x✝²
⊢ (map b e).hom (∃' p) = (map b e).hom q → ∃' p = q
Tactic:
cases q using cases' <;> simp[Rew.rel, Rew.nrel, q_map]
Proof state after:
case hex
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
b : Fin x✝² → Fin x✝¹
e : ξ✝ → x✝
hb : Function.Injective b
hf : Function.Injective e
p p✝ : Semiformula L ξ✝ (x✝² + 1)
⊢ (map (0 :> Fin.succ ∘ b) e).hom p = (map (0 :> Fin.succ ∘ b) e).hom p✝ → p = p✝
Theorem: LO.FirstOrder.Rew.mapl_inj
Proof state before:
case hex
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
b : Fin x✝² → Fin x✝¹
e : ξ✝ → x✝
hb : Function.Injective b
hf : Function.Injective e
p p✝ : Semiformula L ξ✝ (x✝² + 1)
⊢ (map (0 :> Fin.succ ∘ b) e).hom p = (map (0 :> Fin.succ ∘ b) e).hom p✝ → p = p✝
Tactic:
intro h
Proof state after:
case hex
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
b : Fin x✝² → Fin x✝¹
e : ξ✝ → x✝
hb : Function.Injective b
hf : Function.Injective e
p p✝ : Semiformula L ξ✝ (x✝² + 1)
h : (map (0 :> Fin.succ ∘ b) e).hom p = (map (0 :> Fin.succ ∘ b) e).hom p✝
⊢ p = p✝
Theorem: LO.FirstOrder.Rew.mapl_inj
Proof state before:
case hex
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
b : Fin x✝² → Fin x✝¹
e : ξ✝ → x✝
hb : Function.Injective b
hf : Function.Injective e
p p✝ : Semiformula L ξ✝ (x✝² + 1)
h : (map (0 :> Fin.succ ∘ b) e).hom p = (map (0 :> Fin.succ ∘ b) e).hom p✝
⊢ p = p✝
Tactic:
exact mapl_inj (b := 0 :> Fin.succ ∘ b)
(Matrix.injective_vecCons ((Fin.succ_injective _).comp hb) (fun _ => (Fin.succ_ne_zero _).symm)) hf h
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.emb.hom_injective
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₃ : ℕ
o : Type u_5
e : IsEmpty o
⊢ Function.Injective ⇑emb.hom
Tactic:
simp[emb]
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₃ : ℕ
o : Type u_5
e : IsEmpty o
⊢ Function.Injective ⇑(map id fun a => e.elim a).hom
Theorem: LO.FirstOrder.Rew.emb.hom_injective
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₃ : ℕ
o : Type u_5
e : IsEmpty o
⊢ Function.Injective ⇑(map id fun a => e.elim a).hom
Tactic:
exact mapl_inj Function.injective_id (fun x => IsEmpty.elim e x)
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.shift.hom_injective
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₃ : ℕ
⊢ Function.Injective ⇑(hom ⇑)
Tactic:
simp[shift]
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₃ : ℕ
⊢ Function.Injective ⇑(map id Nat.succ).hom
Theorem: LO.FirstOrder.Rew.shift.hom_injective
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₃ : ℕ
⊢ Function.Injective ⇑(map id Nat.succ).hom
Tactic:
exact mapl_inj Function.injective_id Nat.succ_injective
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.hom_fix_free
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 : SyntacticSemiformula L (n + 1)
⊢ (hom fix) ((hom free) p) = p
Tactic:
simp[←hom_comp_app]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.hom_free_fix
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 : SyntacticSemiformula L n
⊢ (hom free) ((hom fix) p) = p
Tactic:
simp[←hom_comp_app]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.hom_substs_mbar_zero_comp_shift_eq_free
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 : SyntacticSemiformula L 1
⊢ [→ &0].hom ((hom ⇑) p) = (hom free) p
Tactic:
simp[←hom_comp_app, substs_mbar_zero_comp_shift_eq_free]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.emb_univClosure
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₃ : ℕ
o : Type u_5
e : IsEmpty o
σ : Semiformula L o n
⊢ emb.hom (∀* σ) = ∀* emb.hom σ
Tactic:
induction n <;> simp[*, univClosure_succ]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_top_iff
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 = ⊤ ↔ p = ⊤
Tactic:
cases p using Semiformula.rec' <;> simp[Rew.rel, Rew.nrel]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_bot_iff
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 = ⊥ ↔ p = ⊥
Tactic:
cases p using Semiformula.rec' <;> simp[Rew.rel, Rew.nrel]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_rel_iff
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₁
k : ℕ
r : L.Rel k
v : Fin k → Semiterm L ξ₂ n₂
⊢ ω.hom p = rel r v ↔ ∃ v', ⇑ω ∘ v' = v ∧ p = rel r v'
Tactic:
cases p using Semiformula.rec' <;> 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₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
r : L.Rel k
v : Fin k → Semiterm L ξ₂ n₂
k✝ : ℕ
r✝ : L.Rel k✝
v✝ : Fin k✝ → Semiterm L ξ₁ n₁
⊢ k✝ = k ∧ HEq r✝ r ∧ HEq (fun i => ω (v✝ i)) v ↔ ∃ v', ⇑ω ∘ v' = v ∧ k✝ = k ∧ HEq r✝ r ∧ HEq v✝ v'
Theorem: LO.FirstOrder.Rew.eq_rel_iff
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₂
k : ℕ
r : L.Rel k
v✝ : Fin k → Semiterm L ξ₂ n₂
k' : ℕ
r' : L.Rel k'
v : Fin k' → Semiterm L ξ₁ n₁
⊢ k' = k ∧ HEq r' r ∧ HEq (fun i => ω (v i)) v✝ ↔ ∃ v', ⇑ω ∘ v' = v✝ ∧ k' = k ∧ HEq r' r ∧ HEq v v'
Tactic:
case hrel k' r' v =>
  by_cases hk : k' = k <;> simp[hk]; rcases hk with rfl; simp
  by_cases hr : r' = r <;> simp[hr, Function.funext_iff]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_rel_iff
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₂
k : ℕ
r : L.Rel k
v✝ : Fin k → Semiterm L ξ₂ n₂
k' : ℕ
r' : L.Rel k'
v : Fin k' → Semiterm L ξ₁ n₁
⊢ k' = k ∧ HEq r' r ∧ HEq (fun i => ω (v i)) v✝ ↔ ∃ v', ⇑ω ∘ v' = v✝ ∧ k' = k ∧ HEq r' r ∧ HEq v v'
Tactic:
by_cases hk : k' = k <;> simp[hk]
Proof state after:
case pos
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₂
k : ℕ
r : L.Rel k
v✝ : Fin k → Semiterm L ξ₂ n₂
k' : ℕ
r' : L.Rel k'
v : Fin k' → Semiterm L ξ₁ n₁
hk : k' = k
⊢ HEq r' r ∧ HEq (fun i => ω (v i)) v✝ ↔ ∃ v', ⇑ω ∘ v' = v✝ ∧ HEq r' r ∧ HEq v v'
Theorem: LO.FirstOrder.Rew.eq_rel_iff
Proof state before:
case pos
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₂
k : ℕ
r : L.Rel k
v✝ : Fin k → Semiterm L ξ₂ n₂
k' : ℕ
r' : L.Rel k'
v : Fin k' → Semiterm L ξ₁ n₁
hk : k' = k
⊢ HEq r' r ∧ HEq (fun i => ω (v i)) v✝ ↔ ∃ v', ⇑ω ∘ v' = v✝ ∧ HEq r' r ∧ HEq v v'
Tactic:
rcases hk with rfl
Proof state after:
case pos
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₂
k' : ℕ
r' : L.Rel k'
v✝ : Fin k' → Semiterm L ξ₁ n₁
r : L.Rel k'
v : Fin k' → Semiterm L ξ₂ n₂
⊢ HEq r' r ∧ HEq (fun i => ω (v✝ i)) v ↔ ∃ v', ⇑ω ∘ v' = v ∧ HEq r' r ∧ HEq v✝ v'
Theorem: LO.FirstOrder.Rew.eq_rel_iff
Proof state before:
case pos
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₂
k' : ℕ
r' : L.Rel k'
v✝ : Fin k' → Semiterm L ξ₁ n₁
r : L.Rel k'
v : Fin k' → Semiterm L ξ₂ n₂
⊢ HEq r' r ∧ HEq (fun i => ω (v✝ i)) v ↔ ∃ v', ⇑ω ∘ v' = v ∧ HEq r' r ∧ HEq v✝ v'
Tactic:
simp
Proof state after:
case pos
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₂
k' : ℕ
r' : L.Rel k'
v✝ : Fin k' → Semiterm L ξ₁ n₁
r : L.Rel k'
v : Fin k' → Semiterm L ξ₂ n₂
⊢ r' = r ∧ (fun i => ω (v✝ i)) = v ↔ ⇑ω ∘ v✝ = v ∧ r' = r
Theorem: LO.FirstOrder.Rew.eq_rel_iff
Proof state before:
case pos
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₂
k' : ℕ
r' : L.Rel k'
v✝ : Fin k' → Semiterm L ξ₁ n₁
r : L.Rel k'
v : Fin k' → Semiterm L ξ₂ n₂
⊢ r' = r ∧ (fun i => ω (v✝ i)) = v ↔ ⇑ω ∘ v✝ = v ∧ r' = r
Tactic:
by_cases hr : r' = r <;> simp[hr, Function.funext_iff]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_nrel_iff
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₁
k : ℕ
r : L.Rel k
v : Fin k → Semiterm L ξ₂ n₂
⊢ ω.hom p = nrel r v ↔ ∃ v', ⇑ω ∘ v' = v ∧ p = nrel r v'
Tactic:
cases p using Semiformula.rec' <;> 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₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
r : L.Rel k
v : Fin k → Semiterm L ξ₂ n₂
k✝ : ℕ
r✝ : L.Rel k✝
v✝ : Fin k✝ → Semiterm L ξ₁ n₁
⊢ k✝ = k ∧ HEq r✝ r ∧ HEq (fun i => ω (v✝ i)) v ↔ ∃ v', ⇑ω ∘ v' = v ∧ k✝ = k ∧ HEq r✝ r ∧ HEq v✝ v'
Theorem: LO.FirstOrder.Rew.eq_nrel_iff
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₂
k : ℕ
r : L.Rel k
v✝ : Fin k → Semiterm L ξ₂ n₂
k' : ℕ
r' : L.Rel k'
v : Fin k' → Semiterm L ξ₁ n₁
⊢ k' = k ∧ HEq r' r ∧ HEq (fun i => ω (v i)) v✝ ↔ ∃ v', ⇑ω ∘ v' = v✝ ∧ k' = k ∧ HEq r' r ∧ HEq v v'
Tactic:
case hnrel k' r' v =>
  by_cases hk : k' = k <;> simp[hk]; rcases hk with rfl; simp
  by_cases hr : r' = r <;> simp[hr, Function.funext_iff]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_nrel_iff
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₂
k : ℕ
r : L.Rel k
v✝ : Fin k → Semiterm L ξ₂ n₂
k' : ℕ
r' : L.Rel k'
v : Fin k' → Semiterm L ξ₁ n₁
⊢ k' = k ∧ HEq r' r ∧ HEq (fun i => ω (v i)) v✝ ↔ ∃ v', ⇑ω ∘ v' = v✝ ∧ k' = k ∧ HEq r' r ∧ HEq v v'
Tactic:
by_cases hk : k' = k <;> simp[hk]
Proof state after:
case pos
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₂
k : ℕ
r : L.Rel k
v✝ : Fin k → Semiterm L ξ₂ n₂
k' : ℕ
r' : L.Rel k'
v : Fin k' → Semiterm L ξ₁ n₁
hk : k' = k
⊢ HEq r' r ∧ HEq (fun i => ω (v i)) v✝ ↔ ∃ v', ⇑ω ∘ v' = v✝ ∧ HEq r' r ∧ HEq v v'
Theorem: LO.FirstOrder.Rew.eq_nrel_iff
Proof state before:
case pos
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₂
k : ℕ
r : L.Rel k
v✝ : Fin k → Semiterm L ξ₂ n₂
k' : ℕ
r' : L.Rel k'
v : Fin k' → Semiterm L ξ₁ n₁
hk : k' = k
⊢ HEq r' r ∧ HEq (fun i => ω (v i)) v✝ ↔ ∃ v', ⇑ω ∘ v' = v✝ ∧ HEq r' r ∧ HEq v v'
Tactic:
rcases hk with rfl
Proof state after:
case pos
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₂
k' : ℕ
r' : L.Rel k'
v✝ : Fin k' → Semiterm L ξ₁ n₁
r : L.Rel k'
v : Fin k' → Semiterm L ξ₂ n₂
⊢ HEq r' r ∧ HEq (fun i => ω (v✝ i)) v ↔ ∃ v', ⇑ω ∘ v' = v ∧ HEq r' r ∧ HEq v✝ v'
Theorem: LO.FirstOrder.Rew.eq_nrel_iff
Proof state before:
case pos
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₂
k' : ℕ
r' : L.Rel k'
v✝ : Fin k' → Semiterm L ξ₁ n₁
r : L.Rel k'
v : Fin k' → Semiterm L ξ₂ n₂
⊢ HEq r' r ∧ HEq (fun i => ω (v✝ i)) v ↔ ∃ v', ⇑ω ∘ v' = v ∧ HEq r' r ∧ HEq v✝ v'
Tactic:
simp
Proof state after:
case pos
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₂
k' : ℕ
r' : L.Rel k'
v✝ : Fin k' → Semiterm L ξ₁ n₁
r : L.Rel k'
v : Fin k' → Semiterm L ξ₂ n₂
⊢ r' = r ∧ (fun i => ω (v✝ i)) = v ↔ ⇑ω ∘ v✝ = v ∧ r' = r
Theorem: LO.FirstOrder.Rew.eq_nrel_iff
Proof state before:
case pos
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₂
k' : ℕ
r' : L.Rel k'
v✝ : Fin k' → Semiterm L ξ₁ n₁
r : L.Rel k'
v : Fin k' → Semiterm L ξ₂ n₂
⊢ r' = r ∧ (fun i => ω (v✝ i)) = v ↔ ⇑ω ∘ v✝ = v ∧ r' = r
Tactic:
by_cases hr : r' = r <;> simp[hr, Function.funext_iff]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_and_iff
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₁
q₁ q₂ : Semiformula L ξ₂ n₂
⊢ ω.hom p = q₁ ⋏ q₂ ↔ ∃ p₁ p₂, ω.hom p₁ = q₁ ∧ ω.hom p₂ = q₂ ∧ p = p₁ ⋏ p₂
Tactic:
cases p using Semiformula.rec' <;> simp[Rew.rel, Rew.nrel]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_or_iff
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₁
q₁ q₂ : Semiformula L ξ₂ n₂
⊢ ω.hom p = q₁ ⋎ q₂ ↔ ∃ p₁ p₂, ω.hom p₁ = q₁ ∧ ω.hom p₂ = q₂ ∧ p = p₁ ⋎ p₂
Tactic:
cases p using Semiformula.rec' <;> simp[Rew.rel, Rew.nrel]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_all_iff
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₁
q : Semiformula L ξ₂ (n₂ + 1)
⊢ ω.hom p = ∀' q ↔ ∃ p', ω.q.hom p' = q ∧ p = ∀' p'
Tactic:
cases p using Semiformula.rec' <;> simp[Rew.rel, Rew.nrel]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_ex_iff
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₁
q : Semiformula L ξ₂ (n₂ + 1)
⊢ ω.hom p = ∃' q ↔ ∃ p', ω.q.hom p' = q ∧ p = ∃' p'
Tactic:
cases p using Semiformula.rec' <;> simp[Rew.rel, Rew.nrel]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_neg_iff
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₁
q₁ q₂ : Semiformula L ξ₂ n₂
⊢ ω.hom p = q₁ ⟶ q₂ ↔ ∃ p₁ p₂, ω.hom p₁ = q₁ ∧ ω.hom p₂ = q₂ ∧ p = p₁ ⟶ p₂
Tactic:
simp[imp_eq]
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₂
p : Semiformula L ξ₁ n₁
q₁ q₂ : Semiformula L ξ₂ n₂
⊢ (∃ p₁, ω.hom p₁ = ~q₁ ∧ ∃ x, ω.hom x = q₂ ∧ p = p₁ ⋎ x) ↔ ∃ p₁, ω.hom p₁ = q₁ ∧ ∃ x, ω.hom x = q₂ ∧ p = ~p₁ ⋎ x
Theorem: LO.FirstOrder.Rew.eq_neg_iff
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₁
q₁ q₂ : Semiformula L ξ₂ n₂
⊢ (∃ p₁, ω.hom p₁ = ~q₁ ∧ ∃ x, ω.hom x = q₂ ∧ p = p₁ ⋎ x) ↔ ∃ p₁, ω.hom p₁ = q₁ ∧ ∃ x, ω.hom x = q₂ ∧ p = ~p₁ ⋎ x
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₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
p : Semiformula L ξ₁ n₁
q₁ q₂ : Semiformula L ξ₂ n₂
⊢ (∃ p₁, ω.hom p₁ = ~q₁ ∧ ∃ x, ω.hom x = q₂ ∧ p = p₁ ⋎ x) → ∃ p₁, ω.hom p₁ = q₁ ∧ ∃ x, ω.hom x = q₂ ∧ p = ~p₁ ⋎ x

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₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
p : Semiformula L ξ₁ n₁
q₁ q₂ : Semiformula L ξ₂ n₂
⊢ (∃ p₁, ω.hom p₁ = q₁ ∧ ∃ x, ω.hom x = q₂ ∧ p = ~p₁ ⋎ x) → ∃ p₁, ω.hom p₁ = ~q₁ ∧ ∃ x, ω.hom x = q₂ ∧ p = p₁ ⋎ x
Theorem: LO.FirstOrder.Rew.eq_neg_iff
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₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
p : Semiformula L ξ₁ n₁
q₁ q₂ : Semiformula L ξ₂ n₂
⊢ (∃ p₁, ω.hom p₁ = ~q₁ ∧ ∃ x, ω.hom x = q₂ ∧ p = p₁ ⋎ x) → ∃ p₁, ω.hom p₁ = q₁ ∧ ∃ x, ω.hom x = q₂ ∧ p = ~p₁ ⋎ x
Tactic:
rintro ⟨p₁, hp₁, q₂, rfl, rfl⟩
Proof state after:
case mp.intro.intro.intro.intro
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₂
q₁ : Semiformula L ξ₂ n₂
p₁ : Semiformula L ξ₁ n₁
hp₁ : ω.hom p₁ = ~q₁
q₂ : Semiformula L ξ₁ n₁
⊢ ∃ p₁_1, ω.hom p₁_1 = q₁ ∧ ∃ x, ω.hom x = ω.hom q₂ ∧ p₁ ⋎ q₂ = ~p₁_1 ⋎ x
Theorem: LO.FirstOrder.Rew.eq_neg_iff
Proof state before:
case mp.intro.intro.intro.intro
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₂
q₁ : Semiformula L ξ₂ n₂
p₁ : Semiformula L ξ₁ n₁
hp₁ : ω.hom p₁ = ~q₁
q₂ : Semiformula L ξ₁ n₁
⊢ ∃ p₁_1, ω.hom p₁_1 = q₁ ∧ ∃ x, ω.hom x = ω.hom q₂ ∧ p₁ ⋎ q₂ = ~p₁_1 ⋎ x
Tactic:
exact ⟨~p₁, by simp[hp₁]⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_neg_iff
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₂
q₁ : Semiformula L ξ₂ n₂
p₁ : Semiformula L ξ₁ n₁
hp₁ : ω.hom p₁ = ~q₁
q₂ : Semiformula L ξ₁ n₁
⊢ ω.hom (~p₁) = q₁ ∧ ∃ x, ω.hom x = ω.hom q₂ ∧ p₁ ⋎ q₂ = ~~p₁ ⋎ x
Tactic:
simp[hp₁]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_neg_iff
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₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
p : Semiformula L ξ₁ n₁
q₁ q₂ : Semiformula L ξ₂ n₂
⊢ (∃ p₁, ω.hom p₁ = q₁ ∧ ∃ x, ω.hom x = q₂ ∧ p = ~p₁ ⋎ x) → ∃ p₁, ω.hom p₁ = ~q₁ ∧ ∃ x, ω.hom x = q₂ ∧ p = p₁ ⋎ x
Tactic:
rintro ⟨p₁, rfl, p₂, rfl, rfl⟩
Proof state after:
case mpr.intro.intro.intro.intro
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₁ p₂ : Semiformula L ξ₁ n₁
⊢ ∃ p₁_1, ω.hom p₁_1 = ~ω.hom p₁ ∧ ∃ x, ω.hom x = ω.hom p₂ ∧ ~p₁ ⋎ p₂ = p₁_1 ⋎ x
Theorem: LO.FirstOrder.Rew.eq_neg_iff
Proof state before:
case mpr.intro.intro.intro.intro
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₁ p₂ : Semiformula L ξ₁ n₁
⊢ ∃ p₁_1, ω.hom p₁_1 = ~ω.hom p₁ ∧ ∃ x, ω.hom x = ω.hom p₂ ∧ ~p₁ ⋎ p₂ = p₁_1 ⋎ x
Tactic:
exact ⟨~p₁, by simp, p₂, by simp⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_neg_iff
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₁ p₂ : Semiformula L ξ₁ n₁
⊢ ω.hom (~p₁) = ~ω.hom p₁
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_neg_iff
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₁ p₂ : Semiformula L ξ₁ n₁
⊢ ω.hom p₂ = ω.hom p₂ ∧ ~p₁ ⋎ p₂ = ~p₁ ⋎ p₂
Tactic:
simp
Proof state after:
no goals