internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Rew.func3
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
f : L.Func 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
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
f : L.Func 3
t₁ t₂ t₃ : Semiterm L ξ₁ n₁
i : Fin 3
⊢ ω (![t₁, t₂, t₃] i) = ![ω t₁, ω t₂, ω t₃] i
Theorem: LO.FirstOrder.Rew.func3
Proof state before:
case h
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
f : L.Func 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
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
f : L.Func 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.func3
Proof state before:
case h.succ
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
f : L.Func 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.ext
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
hb : ∀ (x : Fin n₁), ω₁ #x = ω₂ #x
hf : ∀ (x : ξ₁), ω₁ &x = ω₂ &x
⊢ ω₁ = ω₂
Tactic:
apply DFunLike.ext ω₁ ω₂
Proof state after:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
hb : ∀ (x : Fin n₁), ω₁ #x = ω₂ #x
hf : ∀ (x : ξ₁), ω₁ &x = ω₂ &x
⊢ ∀ (x : Semiterm L ξ₁ n₁), ω₁ x = ω₂ x
Theorem: LO.FirstOrder.Rew.ext
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
hb : ∀ (x : Fin n₁), ω₁ #x = ω₂ #x
hf : ∀ (x : ξ₁), ω₁ &x = ω₂ &x
⊢ ∀ (x : Semiterm L ξ₁ n₁), ω₁ x = ω₂ x
Tactic:
intro t
Proof state after:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
hb : ∀ (x : Fin n₁), ω₁ #x = ω₂ #x
hf : ∀ (x : ξ₁), ω₁ &x = ω₂ &x
t : Semiterm L ξ₁ n₁
⊢ ω₁ t = ω₂ t
Theorem: LO.FirstOrder.Rew.ext
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
hb : ∀ (x : Fin n₁), ω₁ #x = ω₂ #x
hf : ∀ (x : ξ₁), ω₁ &x = ω₂ &x
t : Semiterm L ξ₁ n₁
⊢ ω₁ t = ω₂ t
Tactic:
induction t <;> simp[*, ω₁.func, ω₂.func]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.ext'
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
h : ω₁ = ω₂
t : Semiterm L ξ₁ n₁
⊢ ω₁ t = ω₂ t
Tactic:
simp[h]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.id_comp
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
⊢ Rew.id.comp ω = ω
Tactic:
ext <;> simp[comp_app]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.comp_id
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ ω : Rew L ξ₁ n₁ ξ₂ n₂
⊢ ω.comp Rew.id = ω
Tactic:
ext <;> simp[comp_app]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_id_of_eq
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ : Rew L ξ₁ n₁ ξ₂ n₂
ω : Rew L ξ n ξ n
hb : ∀ (x : Fin n), ω #x = #x
he : ∀ (x : ξ), ω &x = &x
t : Semiterm L ξ n
⊢ ω t = t
Tactic:
have : ω = Rew.id := by ext <;> simp[*]
Proof state after:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ : Rew L ξ₁ n₁ ξ₂ n₂
ω : Rew L ξ n ξ n
hb : ∀ (x : Fin n), ω #x = #x
he : ∀ (x : ξ), ω &x = &x
t : Semiterm L ξ n
this : ω = Rew.id
⊢ ω t = t
Theorem: LO.FirstOrder.Rew.eq_id_of_eq
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ : Rew L ξ₁ n₁ ξ₂ n₂
ω : Rew L ξ n ξ n
hb : ∀ (x : Fin n), ω #x = #x
he : ∀ (x : ξ), ω &x = &x
t : Semiterm L ξ n
this : ω = Rew.id
⊢ ω t = t
Tactic:
simp[this]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_id_of_eq
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ : Rew L ξ₁ n₁ ξ₂ n₂
ω : Rew L ξ n ξ n
hb : ∀ (x : Fin n), ω #x = #x
he : ∀ (x : ξ), ω &x = &x
t : Semiterm L ξ n
⊢ ω = Rew.id
Tactic:
ext <;> simp[*]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_bind
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ : Rew L ξ₁ n₁ ξ₂ n₂
b : Fin n₁ → Semiterm L ξ₂ n₂
e : ξ₁ → Semiterm L ξ₂ n₂
ω : Rew L ξ₁ n₁ ξ₂ n₂
⊢ ω = bind (⇑ω ∘ bvar) (⇑ω ∘ fvar)
Tactic:
ext t
Proof state after:
case hb
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ : Rew L ξ₁ n₁ ξ₂ n₂
b : Fin n₁ → Semiterm L ξ₂ n₂
e : ξ₁ → Semiterm L ξ₂ n₂
ω : Rew L ξ₁ n₁ ξ₂ n₂
t : Fin n₁
⊢ ω #t = (bind (⇑ω ∘ bvar) (⇑ω ∘ fvar)) #t

case hf
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ : Rew L ξ₁ n₁ ξ₂ n₂
b : Fin n₁ → Semiterm L ξ₂ n₂
e : ξ₁ → Semiterm L ξ₂ n₂
ω : Rew L ξ₁ n₁ ξ₂ n₂
t : ξ₁
⊢ ω &t = (bind (⇑ω ∘ bvar) (⇑ω ∘ fvar)) &t
Theorem: LO.FirstOrder.Rew.eq_bind
Proof state before:
case hb
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ : Rew L ξ₁ n₁ ξ₂ n₂
b : Fin n₁ → Semiterm L ξ₂ n₂
e : ξ₁ → Semiterm L ξ₂ n₂
ω : Rew L ξ₁ n₁ ξ₂ n₂
t : Fin n₁
⊢ ω #t = (bind (⇑ω ∘ bvar) (⇑ω ∘ fvar)) #t

case hf
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ : Rew L ξ₁ n₁ ξ₂ n₂
b : Fin n₁ → Semiterm L ξ₂ n₂
e : ξ₁ → Semiterm L ξ₂ n₂
ω : Rew L ξ₁ n₁ ξ₂ n₂
t : ξ₁
⊢ ω &t = (bind (⇑ω ∘ bvar) (⇑ω ∘ fvar)) &t
Tactic:
induction t
Proof state after:
case hb.mk
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ : Rew L ξ₁ n₁ ξ₂ n₂
b : Fin n₁ → Semiterm L ξ₂ n₂
e : ξ₁ → Semiterm L ξ₂ n₂
ω : Rew L ξ₁ n₁ ξ₂ n₂
val✝ : ℕ
isLt✝ : val✝ < n₁
⊢ ω #⟨val✝, isLt✝⟩ = (bind (⇑ω ∘ bvar) (⇑ω ∘ fvar)) #⟨val✝, isLt✝⟩

case hf
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ : Rew L ξ₁ n₁ ξ₂ n₂
b : Fin n₁ → Semiterm L ξ₂ n₂
e : ξ₁ → Semiterm L ξ₂ n₂
ω : Rew L ξ₁ n₁ ξ₂ n₂
t : ξ₁
⊢ ω &t = (bind (⇑ω ∘ bvar) (⇑ω ∘ fvar)) &t
Theorem: LO.FirstOrder.Rew.eq_bind
Proof state before:
case hb.mk
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ : Rew L ξ₁ n₁ ξ₂ n₂
b : Fin n₁ → Semiterm L ξ₂ n₂
e : ξ₁ → Semiterm L ξ₂ n₂
ω : Rew L ξ₁ n₁ ξ₂ n₂
val✝ : ℕ
isLt✝ : val✝ < n₁
⊢ ω #⟨val✝, isLt✝⟩ = (bind (⇑ω ∘ bvar) (⇑ω ∘ fvar)) #⟨val✝, isLt✝⟩

case hf
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ : Rew L ξ₁ n₁ ξ₂ n₂
b : Fin n₁ → Semiterm L ξ₂ n₂
e : ξ₁ → Semiterm L ξ₂ n₂
ω : Rew L ξ₁ n₁ ξ₂ n₂
t : ξ₁
⊢ ω &t = (bind (⇑ω ∘ bvar) (⇑ω ∘ fvar)) &t
Tactic:
simp[Rew.func'']
Proof state after:
case hf
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ : Rew L ξ₁ n₁ ξ₂ n₂
b : Fin n₁ → Semiterm L ξ₂ n₂
e : ξ₁ → Semiterm L ξ₂ n₂
ω : Rew L ξ₁ n₁ ξ₂ n₂
t : ξ₁
⊢ ω &t = (bind (⇑ω ∘ bvar) (⇑ω ∘ fvar)) &t
Theorem: LO.FirstOrder.Rew.eq_bind
Proof state before:
case hf
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω✝ : Rew L ξ₁ n₁ ξ₂ n₂
b : Fin n₁ → Semiterm L ξ₂ n₂
e : ξ₁ → Semiterm L ξ₂ n₂
ω : Rew L ξ₁ n₁ ξ₂ n₂
t : ξ₁
⊢ ω &t = (bind (⇑ω ∘ bvar) (⇑ω ∘ fvar)) &t
Tactic:
simp[*]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.bind_eq_id_of_zero
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b : Fin n₁ → Semiterm L ξ₂ n₂
e : ξ₁ → Semiterm L ξ₂ n₂
f : Fin 0 → Semiterm L ξ₂ 0
⊢ bind f fvar = Rew.id
Tactic:
ext x <;> simp
Proof state after:
case hb
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b : Fin n₁ → Semiterm L ξ₂ n₂
e : ξ₁ → Semiterm L ξ₂ n₂
f : Fin 0 → Semiterm L ξ₂ 0
x : Fin 0
⊢ f x = #x
Theorem: LO.FirstOrder.Rew.bind_eq_id_of_zero
Proof state before:
case hb
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b : Fin n₁ → Semiterm L ξ₂ n₂
e : ξ₁ → Semiterm L ξ₂ n₂
f : Fin 0 → Semiterm L ξ₂ 0
x : Fin 0
⊢ f x = #x
Tactic:
exact Fin.elim0 x
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.map_id
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
⊢ map id id = Rew.id
Tactic:
ext <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.map_inj
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
x : Fin n₁
t : Semiterm L ξ₁ n₁
⊢ (map b e) #x = (map b e) t → #x = t
Tactic:
cases t <;> simp[Rew.func]
Proof state after:
case bvar
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
x a✝ : Fin n₁
⊢ b x = b a✝ → x = a✝
Theorem: LO.FirstOrder.Rew.map_inj
Proof state before:
case bvar
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
x a✝ : Fin n₁
⊢ b x = b a✝ → x = a✝
Tactic:
intro h
Proof state after:
case bvar
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
x a✝ : Fin n₁
h : b x = b a✝
⊢ x = a✝
Theorem: LO.FirstOrder.Rew.map_inj
Proof state before:
case bvar
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
x a✝ : Fin n₁
h : b x = b a✝
⊢ x = a✝
Tactic:
exact hb h
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.map_inj
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
x : ξ₁
t : Semiterm L ξ₁ n₁
⊢ (map b e) &x = (map b e) t → &x = t
Tactic:
cases t <;> simp[Rew.func]
Proof state after:
case fvar
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
x a✝ : ξ₁
⊢ e x = e a✝ → x = a✝
Theorem: LO.FirstOrder.Rew.map_inj
Proof state before:
case fvar
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
x a✝ : ξ₁
⊢ e x = e a✝ → x = a✝
Tactic:
intro h
Proof state after:
case fvar
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
x a✝ : ξ₁
h : e x = e a✝
⊢ x = a✝
Theorem: LO.FirstOrder.Rew.map_inj
Proof state before:
case fvar
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
x a✝ : ξ₁
h : e x = e a✝
⊢ x = a✝
Tactic:
exact he h
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.map_inj
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ₁ n₁
t : Semiterm L ξ₁ n₁
⊢ (map b e) (func f v) = (map b e) t → func f v = t
Tactic:
cases t <;> simp[*, Rew.func]
Proof state after:
case func
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ₁ n₁
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → Semiterm L ξ₁ n₁
⊢ k = arity✝ →
    HEq f a✝¹ → (HEq (fun i => (map b e) (v i)) fun i => (map b e) (a✝ i)) → k = arity✝ ∧ HEq f a✝¹ ∧ HEq v a✝
Theorem: LO.FirstOrder.Rew.map_inj
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ₁ n₁
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → Semiterm L ξ₁ n₁
⊢ k = arity✝ →
    HEq f a✝¹ → (HEq (fun i => (map b e) (v i)) fun i => (map b e) (a✝ i)) → k = arity✝ ∧ HEq f a✝¹ ∧ HEq v a✝
Tactic:
case func =>
  rintro rfl; simp; rintro rfl h; simp
  funext i; exact map_inj hb he (congr_fun h i)
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.map_inj
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ₁ n₁
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → Semiterm L ξ₁ n₁
⊢ k = arity✝ →
    HEq f a✝¹ → (HEq (fun i => (map b e) (v i)) fun i => (map b e) (a✝ i)) → k = arity✝ ∧ HEq f a✝¹ ∧ HEq v a✝
Tactic:
rintro rfl
Proof state after:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ₁ n₁
a✝¹ : L.Func k
a✝ : Fin k → Semiterm L ξ₁ n₁
⊢ HEq f a✝¹ → (HEq (fun i => (map b e) (v i)) fun i => (map b e) (a✝ i)) → k = k ∧ HEq f a✝¹ ∧ HEq v a✝
Theorem: LO.FirstOrder.Rew.map_inj
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ₁ n₁
a✝¹ : L.Func k
a✝ : Fin k → Semiterm L ξ₁ n₁
⊢ HEq f a✝¹ → (HEq (fun i => (map b e) (v i)) fun i => (map b e) (a✝ i)) → k = k ∧ HEq f a✝¹ ∧ HEq v a✝
Tactic:
simp
Proof state after:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ₁ n₁
a✝¹ : L.Func k
a✝ : Fin k → Semiterm L ξ₁ n₁
⊢ f = a✝¹ → ((fun i => (map b e) (v i)) = fun i => (map b e) (a✝ i)) → f = a✝¹ ∧ v = a✝
Theorem: LO.FirstOrder.Rew.map_inj
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ₁ n₁
a✝¹ : L.Func k
a✝ : Fin k → Semiterm L ξ₁ n₁
⊢ f = a✝¹ → ((fun i => (map b e) (v i)) = fun i => (map b e) (a✝ i)) → f = a✝¹ ∧ v = a✝
Tactic:
rintro rfl h
Proof state after:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
k : ℕ
f : L.Func k
v a✝ : Fin k → Semiterm L ξ₁ n₁
h : (fun i => (map b e) (v i)) = fun i => (map b e) (a✝ i)
⊢ f = f ∧ v = a✝
Theorem: LO.FirstOrder.Rew.map_inj
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
k : ℕ
f : L.Func k
v a✝ : Fin k → Semiterm L ξ₁ n₁
h : (fun i => (map b e) (v i)) = fun i => (map b e) (a✝ i)
⊢ f = f ∧ v = a✝
Tactic:
simp
Proof state after:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
k : ℕ
f : L.Func k
v a✝ : Fin k → Semiterm L ξ₁ n₁
h : (fun i => (map b e) (v i)) = fun i => (map b e) (a✝ i)
⊢ v = a✝
Theorem: LO.FirstOrder.Rew.map_inj
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
k : ℕ
f : L.Func k
v a✝ : Fin k → Semiterm L ξ₁ n₁
h : (fun i => (map b e) (v i)) = fun i => (map b e) (a✝ i)
⊢ v = a✝
Tactic:
funext i
Proof state after:
case h
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
k : ℕ
f : L.Func k
v a✝ : Fin k → Semiterm L ξ₁ n₁
h : (fun i => (map b e) (v i)) = fun i => (map b e) (a✝ i)
i : Fin k
⊢ v i = a✝ i
Theorem: LO.FirstOrder.Rew.map_inj
Proof state before:
case h
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
k : ℕ
f : L.Func k
v a✝ : Fin k → Semiterm L ξ₁ n₁
h : (fun i => (map b e) (v i)) = fun i => (map b e) (a✝ i)
i : Fin k
⊢ v i = a✝ i
Tactic:
exact map_inj hb he (congr_fun h i)
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.rewrite_comp_rewrite
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
f : ξ₁ → Semiterm L ξ₂ n
v : ξ₂ → Semiterm L ξ₃ n
w : ξ₁ → Semiterm L ξ₂ n
⊢ (rewrite v).comp (rewrite w) = rewrite (⇑(rewrite v) ∘ w)
Tactic:
ext <;> simp[comp_app]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.rewrite_eq_id
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
f : ξ₁ → Semiterm L ξ₂ n
⊢ rewrite fvar = Rew.id
Tactic:
ext <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.rewriteMap_id
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
e : ξ₁ → ξ₂
⊢ rewriteMap id = Rew.id
Tactic:
ext <;> simp
Proof state after:
no goals