Theorem: LO.FirstOrder.Rew.eq_ball_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.ball, eq_all_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