Theorem: TP_eq_iff (Pdl/Unfold.lean)

State before:
α : Program
ℓ ℓ' : TP α
⊢ ℓ = ℓ' ↔ ∀ τ ∈ (testsOfProgram α).attach, ℓ τ = ℓ' τ
Tactic:
constructor
State after:
case mp
α : Program
ℓ ℓ' : TP α
⊢ ℓ = ℓ' → ∀ τ ∈ (testsOfProgram α).attach, ℓ τ = ℓ' τ

case mpr
α : Program
ℓ ℓ' : TP α
⊢ (∀ τ ∈ (testsOfProgram α).attach, ℓ τ = ℓ' τ) → ℓ = ℓ'

State before:
case mp
α : Program
ℓ ℓ' : TP α
⊢ ℓ = ℓ' → ∀ τ ∈ (testsOfProgram α).attach, ℓ τ = ℓ' τ
Tactic:
intro ℓ_eq_ℓ _ _
State after:
case mp
α : Program
ℓ ℓ' : TP α
ℓ_eq_ℓ : ℓ = ℓ'
τ✝ : { x // x ∈ testsOfProgram α }
a✝ : τ✝ ∈ (testsOfProgram α).attach
⊢ ℓ τ✝ = ℓ' τ✝

State before:
case mp
α : Program
ℓ ℓ' : TP α
ℓ_eq_ℓ : ℓ = ℓ'
τ✝ : { x // x ∈ testsOfProgram α }
a✝ : τ✝ ∈ (testsOfProgram α).attach
⊢ ℓ τ✝ = ℓ' τ✝
Tactic:
simp_all
State after:
no goals

State before:
case mpr
α : Program
ℓ ℓ' : TP α
⊢ (∀ τ ∈ (testsOfProgram α).attach, ℓ τ = ℓ' τ) → ℓ = ℓ'
Tactic:
intro rhs
State after:
case mpr
α : Program
ℓ ℓ' : TP α
rhs : ∀ τ ∈ (testsOfProgram α).attach, ℓ τ = ℓ' τ
⊢ ℓ = ℓ'

State before:
case mpr
α : Program
ℓ ℓ' : TP α
rhs : ∀ τ ∈ (testsOfProgram α).attach, ℓ τ = ℓ' τ
⊢ ℓ = ℓ'
Tactic:
simp_all
State after:
case mpr
α : Program
ℓ ℓ' : TP α
rhs : ∀ (a : Formula) (b : a ∈ testsOfProgram α), ℓ ⟨a, b⟩ = ℓ' ⟨a, b⟩
⊢ ℓ = ℓ'

State before:
case mpr
α : Program
ℓ ℓ' : TP α
rhs : ∀ (a : Formula) (b : a ∈ testsOfProgram α), ℓ ⟨a, b⟩ = ℓ' ⟨a, b⟩
⊢ ℓ = ℓ'
Tactic:
unfold TP at *
State after:
case mpr
α : Program
ℓ ℓ' : { τ // τ ∈ testsOfProgram α } → Bool
rhs : ∀ (a : Formula) (b : a ∈ testsOfProgram α), ℓ ⟨a, b⟩ = ℓ' ⟨a, b⟩
⊢ ℓ = ℓ'

State before:
case mpr
α : Program
ℓ ℓ' : { τ // τ ∈ testsOfProgram α } → Bool
rhs : ∀ (a : Formula) (b : a ∈ testsOfProgram α), ℓ ⟨a, b⟩ = ℓ' ⟨a, b⟩
⊢ ℓ = ℓ'
Tactic:
ext τ
State after:
case mpr.h
α : Program
ℓ ℓ' : { τ // τ ∈ testsOfProgram α } → Bool
rhs : ∀ (a : Formula) (b : a ∈ testsOfProgram α), ℓ ⟨a, b⟩ = ℓ' ⟨a, b⟩
τ : { τ // τ ∈ testsOfProgram α }
⊢ ℓ τ = ℓ' τ

State before:
case mpr.h
α : Program
ℓ ℓ' : { τ // τ ∈ testsOfProgram α } → Bool
rhs : ∀ (a : Formula) (b : a ∈ testsOfProgram α), ℓ ⟨a, b⟩ = ℓ' ⟨a, b⟩
τ : { τ // τ ∈ testsOfProgram α }
⊢ ℓ τ = ℓ' τ
Tactic:
apply rhs
State after:
no goals