internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Rew.eq_ball_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₂ + 1)
⊢ (ω.hom p = ∀[q₁] q₂) ↔ ∃ p₁ p₂, ω.q.hom p₁ = q₁ ∧ ω.q.hom p₂ = q₂ ∧ p = ∀[p₁] p₂
Tactic:
simp[LogicalConnective.ball, eq_all_iff]
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₂ + 1)
⊢ (∃ p', (∃ p₁, ω.q.hom p₁ = q₁ ∧ ∃ x, ω.q.hom x = q₂ ∧ p' = p₁ ⟶ x) ∧ p = ∀' p') ↔
    ∃ p₁, ω.q.hom p₁ = q₁ ∧ ∃ x, ω.q.hom x = q₂ ∧ p = ∀' (p₁ ⟶ x)
Theorem: LO.FirstOrder.Rew.eq_ball_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₂ + 1)
⊢ (∃ p', (∃ p₁, ω.q.hom p₁ = q₁ ∧ ∃ x, ω.q.hom x = q₂ ∧ p' = p₁ ⟶ x) ∧ p = ∀' p') ↔
    ∃ p₁, ω.q.hom p₁ = q₁ ∧ ∃ x, ω.q.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₂ + 1)
⊢ (∃ p', (∃ p₁, ω.q.hom p₁ = q₁ ∧ ∃ x, ω.q.hom x = q₂ ∧ p' = p₁ ⟶ x) ∧ p = ∀' p') →
    ∃ p₁, ω.q.hom p₁ = q₁ ∧ ∃ x, ω.q.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₂ + 1)
⊢ (∃ p₁, ω.q.hom p₁ = q₁ ∧ ∃ x, ω.q.hom x = q₂ ∧ p = ∀' (p₁ ⟶ x)) →
    ∃ p', (∃ p₁, ω.q.hom p₁ = q₁ ∧ ∃ x, ω.q.hom x = q₂ ∧ p' = p₁ ⟶ x) ∧ p = ∀' p'
Theorem: LO.FirstOrder.Rew.eq_ball_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₂ + 1)
⊢ (∃ p', (∃ p₁, ω.q.hom p₁ = q₁ ∧ ∃ x, ω.q.hom x = q₂ ∧ p' = p₁ ⟶ x) ∧ p = ∀' p') →
    ∃ p₁, ω.q.hom p₁ = q₁ ∧ ∃ x, ω.q.hom x = q₂ ∧ p = ∀' (p₁ ⟶ x)
Tactic:
rintro ⟨p', ⟨p₁, rfl, p₂, rfl, rfl⟩, rfl⟩
Proof state after:
case mp.intro.intro.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₁ + 1)
⊢ ∃ p₁_1, ω.q.hom p₁_1 = ω.q.hom p₁ ∧ ∃ x, ω.q.hom x = ω.q.hom p₂ ∧ ∀' (p₁ ⟶ p₂) = ∀' (p₁_1 ⟶ x)
Theorem: LO.FirstOrder.Rew.eq_ball_iff
Proof state before:
case mp.intro.intro.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₁ + 1)
⊢ ∃ p₁_1, ω.q.hom p₁_1 = ω.q.hom p₁ ∧ ∃ x, ω.q.hom x = ω.q.hom p₂ ∧ ∀' (p₁ ⟶ p₂) = ∀' (p₁_1 ⟶ x)
Tactic:
exact ⟨p₁, rfl, p₂, rfl, rfl⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_ball_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₂ + 1)
⊢ (∃ p₁, ω.q.hom p₁ = q₁ ∧ ∃ x, ω.q.hom x = q₂ ∧ p = ∀' (p₁ ⟶ x)) →
    ∃ p', (∃ p₁, ω.q.hom p₁ = q₁ ∧ ∃ x, ω.q.hom x = q₂ ∧ p' = p₁ ⟶ x) ∧ p = ∀' p'
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₁ + 1)
⊢ ∃ p', (∃ p₁_1, ω.q.hom p₁_1 = ω.q.hom p₁ ∧ ∃ x, ω.q.hom x = ω.q.hom p₂ ∧ p' = p₁_1 ⟶ x) ∧ ∀' (p₁ ⟶ p₂) = ∀' p'
Theorem: LO.FirstOrder.Rew.eq_ball_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₁ + 1)
⊢ ∃ p', (∃ p₁_1, ω.q.hom p₁_1 = ω.q.hom p₁ ∧ ∃ x, ω.q.hom x = ω.q.hom p₂ ∧ p' = p₁_1 ⟶ x) ∧ ∀' (p₁ ⟶ p₂) = ∀' p'
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_bex_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₂ + 1)
⊢ (ω.hom p = ∃[q₁] q₂) ↔ ∃ p₁ p₂, ω.q.hom p₁ = q₁ ∧ ω.q.hom p₂ = q₂ ∧ p = ∃[p₁] p₂
Tactic:
simp[LogicalConnective.bex, eq_ex_iff]
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₂ + 1)
⊢ (∃ p', (∃ p₁, ω.q.hom p₁ = q₁ ∧ ∃ x, ω.q.hom x = q₂ ∧ p' = p₁ ⋏ x) ∧ p = ∃' p') ↔
    ∃ p₁, ω.q.hom p₁ = q₁ ∧ ∃ x, ω.q.hom x = q₂ ∧ p = ∃' p₁ ⋏ x
Theorem: LO.FirstOrder.Rew.eq_bex_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₂ + 1)
⊢ (∃ p', (∃ p₁, ω.q.hom p₁ = q₁ ∧ ∃ x, ω.q.hom x = q₂ ∧ p' = p₁ ⋏ x) ∧ p = ∃' p') ↔
    ∃ p₁, ω.q.hom p₁ = q₁ ∧ ∃ x, ω.q.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₂ + 1)
⊢ (∃ p', (∃ p₁, ω.q.hom p₁ = q₁ ∧ ∃ x, ω.q.hom x = q₂ ∧ p' = p₁ ⋏ x) ∧ p = ∃' p') →
    ∃ p₁, ω.q.hom p₁ = q₁ ∧ ∃ x, ω.q.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₂ + 1)
⊢ (∃ p₁, ω.q.hom p₁ = q₁ ∧ ∃ x, ω.q.hom x = q₂ ∧ p = ∃' p₁ ⋏ x) →
    ∃ p', (∃ p₁, ω.q.hom p₁ = q₁ ∧ ∃ x, ω.q.hom x = q₂ ∧ p' = p₁ ⋏ x) ∧ p = ∃' p'
Theorem: LO.FirstOrder.Rew.eq_bex_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₂ + 1)
⊢ (∃ p', (∃ p₁, ω.q.hom p₁ = q₁ ∧ ∃ x, ω.q.hom x = q₂ ∧ p' = p₁ ⋏ x) ∧ p = ∃' p') →
    ∃ p₁, ω.q.hom p₁ = q₁ ∧ ∃ x, ω.q.hom x = q₂ ∧ p = ∃' p₁ ⋏ x
Tactic:
rintro ⟨p', ⟨p₁, rfl, p₂, rfl, rfl⟩, rfl⟩
Proof state after:
case mp.intro.intro.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₁ + 1)
⊢ ∃ p₁_1, ω.q.hom p₁_1 = ω.q.hom p₁ ∧ ∃ x, ω.q.hom x = ω.q.hom p₂ ∧ ∃' p₁ ⋏ p₂ = ∃' p₁_1 ⋏ x
Theorem: LO.FirstOrder.Rew.eq_bex_iff
Proof state before:
case mp.intro.intro.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₁ + 1)
⊢ ∃ p₁_1, ω.q.hom p₁_1 = ω.q.hom p₁ ∧ ∃ x, ω.q.hom x = ω.q.hom p₂ ∧ ∃' p₁ ⋏ p₂ = ∃' p₁_1 ⋏ x
Tactic:
exact ⟨p₁, rfl, p₂, rfl, rfl⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_bex_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₂ + 1)
⊢ (∃ p₁, ω.q.hom p₁ = q₁ ∧ ∃ x, ω.q.hom x = q₂ ∧ p = ∃' p₁ ⋏ x) →
    ∃ p', (∃ p₁, ω.q.hom p₁ = q₁ ∧ ∃ x, ω.q.hom x = q₂ ∧ p' = p₁ ⋏ x) ∧ p = ∃' p'
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₁ + 1)
⊢ ∃ p', (∃ p₁_1, ω.q.hom p₁_1 = ω.q.hom p₁ ∧ ∃ x, ω.q.hom x = ω.q.hom p₂ ∧ p' = p₁_1 ⋏ x) ∧ ∃' p₁ ⋏ p₂ = ∃' p'
Theorem: LO.FirstOrder.Rew.eq_bex_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₁ + 1)
⊢ ∃ p', (∃ p₁_1, ω.q.hom p₁_1 = ω.q.hom p₁ ∧ ∃ x, ω.q.hom x = ω.q.hom p₂ ∧ p' = p₁_1 ⋏ x) ∧ ∃' p₁ ⋏ p₂ = ∃' p'
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
h : Function.funEqOn (fun x => x ∈ ⊤.fv) f g
⊢ (rewriteMap f).hom ⊤ = (rewriteMap g).hom ⊤
Tactic:
case hverum => simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
h : Function.funEqOn (fun x => x ∈ ⊥.fv) f g
⊢ (rewriteMap f).hom ⊥ = (rewriteMap g).hom ⊥
Tactic:
case hfalsum => simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (rel r v).fv) f g
⊢ (rewriteMap f).hom (rel r v) = (rewriteMap g).hom (rel r v)
Tactic:
case hrel r v =>
  simp [Rew.rel]; funext i
  exact eq_rewriteMap_of_funEqOn_fv (v i) f g (by intro x (hx : x ∈ (v i).fv); exact h _ (by simp [fv_rel]; exact ⟨i, hx⟩))
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (nrel r v).fv) f g
⊢ (rewriteMap f).hom (nrel r v) = (rewriteMap g).hom (nrel r v)
Tactic:
case hnrel r v =>
  simp [Rew.nrel]; funext i
  exact eq_rewriteMap_of_funEqOn_fv (v i) f g (by intro x (hx : x ∈ (v i).fv); exact h _ (by simp [fv_nrel]; exact ⟨i, hx⟩))
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p q : Semiformula L ξ₁ n✝
ihp : Function.funEqOn (fun x => x ∈ p.fv) f g → (rewriteMap f).hom p = (rewriteMap g).hom p
ihq : Function.funEqOn (fun x => x ∈ q.fv) f g → (rewriteMap f).hom q = (rewriteMap g).hom q
h : Function.funEqOn (fun x => x ∈ (p ⋏ q).fv) f g
⊢ (rewriteMap f).hom (p ⋏ q) = (rewriteMap g).hom (p ⋏ q)
Tactic:
case hand p q ihp ihq =>
  simp; exact ⟨ihp (by intro x (hx : x ∈ p.fv); exact h _ (by simp [hx])), ihq (by intro x (hx : x ∈ q.fv); exact h _ (by simp [hx]))⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p q : Semiformula L ξ₁ n✝
ihp : Function.funEqOn (fun x => x ∈ p.fv) f g → (rewriteMap f).hom p = (rewriteMap g).hom p
ihq : Function.funEqOn (fun x => x ∈ q.fv) f g → (rewriteMap f).hom q = (rewriteMap g).hom q
h : Function.funEqOn (fun x => x ∈ (p ⋎ q).fv) f g
⊢ (rewriteMap f).hom (p ⋎ q) = (rewriteMap g).hom (p ⋎ q)
Tactic:
case hor p q ihp ihq =>
  simp; exact ⟨ihp (by intro x (hx : x ∈ p.fv); exact h _ (by simp [hx])), ihq (by intro x (hx : x ∈ q.fv); exact h _ (by simp [hx]))⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p : Semiformula L ξ₁ (n✝ + 1)
ih : Function.funEqOn (fun x => x ∈ p.fv) f g → (rewriteMap f).hom p = (rewriteMap g).hom p
h : Function.funEqOn (fun x => x ∈ (∀' p).fv) f g
⊢ (rewriteMap f).hom (∀' p) = (rewriteMap g).hom (∀' p)
Tactic:
case hall p ih => simp; exact ih (by intro x (hx : x ∈ fv p); exact h _ (by simp [hx]))
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p : Semiformula L ξ₁ (n✝ + 1)
ih : Function.funEqOn (fun x => x ∈ p.fv) f g → (rewriteMap f).hom p = (rewriteMap g).hom p
h : Function.funEqOn (fun x => x ∈ (∃' p).fv) f g
⊢ (rewriteMap f).hom (∃' p) = (rewriteMap g).hom (∃' p)
Tactic:
case hex p ih => simp; exact ih (by intro x (hx : x ∈ fv p); exact h _ (by simp [hx]))
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
h : Function.funEqOn (fun x => x ∈ ⊤.fv) f g
⊢ (rewriteMap f).hom ⊤ = (rewriteMap g).hom ⊤
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
h : Function.funEqOn (fun x => x ∈ ⊥.fv) f g
⊢ (rewriteMap f).hom ⊥ = (rewriteMap g).hom ⊥
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (rel r v).fv) f g
⊢ (rewriteMap f).hom (rel r v) = (rewriteMap g).hom (rel r v)
Tactic:
simp [Rew.rel]
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (rel r v).fv) f g
⊢ (fun i => (rewriteMap f) (v i)) = fun i => (rewriteMap g) (v i)
Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (rel r v).fv) f g
⊢ (fun i => (rewriteMap f) (v i)) = fun i => (rewriteMap g) (v i)
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (rel r v).fv) f g
i : Fin k✝
⊢ (rewriteMap f) (v i) = (rewriteMap g) (v i)
Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (rel r v).fv) f g
i : Fin k✝
⊢ (rewriteMap f) (v i) = (rewriteMap g) (v i)
Tactic:
exact eq_rewriteMap_of_funEqOn_fv (v i) f g (by intro x (hx : x ∈ (v i).fv); exact h _ (by simp [fv_rel]; exact ⟨i, hx⟩))
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (rel r v).fv) f g
i : Fin k✝
⊢ Function.funEqOn (fun x => x ∈ (v i).fv) f g
Tactic:
intro x (hx : x ∈ (v i).fv)
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (rel r v).fv) f g
i : Fin k✝
x : ξ₁
hx : x ∈ (v i).fv
⊢ f x = g x
Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (rel r v).fv) f g
i : Fin k✝
x : ξ₁
hx : x ∈ (v i).fv
⊢ f x = g x
Tactic:
exact h _ (by simp [fv_rel]; exact ⟨i, hx⟩)
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (rel r v).fv) f g
i : Fin k✝
x : ξ₁
hx : x ∈ (v i).fv
⊢ (fun x => x ∈ (rel r v).fv) x
Tactic:
simp [fv_rel]
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (rel r v).fv) f g
i : Fin k✝
x : ξ₁
hx : x ∈ (v i).fv
⊢ ∃ a, x ∈ (v a).fv
Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (rel r v).fv) f g
i : Fin k✝
x : ξ₁
hx : x ∈ (v i).fv
⊢ ∃ a, x ∈ (v a).fv
Tactic:
exact ⟨i, hx⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (nrel r v).fv) f g
⊢ (rewriteMap f).hom (nrel r v) = (rewriteMap g).hom (nrel r v)
Tactic:
simp [Rew.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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (nrel r v).fv) f g
⊢ (fun i => (rewriteMap f) (v i)) = fun i => (rewriteMap g) (v i)
Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (nrel r v).fv) f g
⊢ (fun i => (rewriteMap f) (v i)) = fun i => (rewriteMap g) (v i)
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (nrel r v).fv) f g
i : Fin k✝
⊢ (rewriteMap f) (v i) = (rewriteMap g) (v i)
Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (nrel r v).fv) f g
i : Fin k✝
⊢ (rewriteMap f) (v i) = (rewriteMap g) (v i)
Tactic:
exact eq_rewriteMap_of_funEqOn_fv (v i) f g (by intro x (hx : x ∈ (v i).fv); exact h _ (by simp [fv_nrel]; exact ⟨i, hx⟩))
Proof state after:
no goals