Theorem: LO.FirstOrder.Rew.eq_bex_iff (Logic/FirstOrder/Basic/Syntax/Rew.lean)

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]
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

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
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'

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⟩
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

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⟩
State after:
no goals

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⟩
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'

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
State after:
no goals