Theorem: Etch.Verification.coeLex_injective (Etch/StreamFusion/Proofs/StreamProof.lean)

State before:
ι : Type
α : Type ?u.7590
a b s : Stream ι α
x₁ : ι
y₁ : Bool
x₂ : ι
y₂ : Bool
⊢ coeLex (x₁, y₁) = coeLex (x₂, y₂) → (x₁, y₁) = (x₂, y₂)
Tactic:
rw [Prod.mk.injEq .., Prod.mk.injEq ..]
State after:
ι : Type
α : Type ?u.7590
a b s : Stream ι α
x₁ : ι
y₁ : Bool
x₂ : ι
y₂ : Bool
⊢ ↑(x₁, y₁).1 = ↑(x₂, y₂).1 ∧ (x₁, y₁).2 = (x₂, y₂).2 → x₁ = x₂ ∧ y₁ = y₂

State before:
ι : Type
α : Type ?u.7590
a b s : Stream ι α
x₁ : ι
y₁ : Bool
x₂ : ι
y₂ : Bool
⊢ ↑(x₁, y₁).1 = ↑(x₂, y₂).1 ∧ (x₁, y₁).2 = (x₂, y₂).2 → x₁ = x₂ ∧ y₁ = y₂
Tactic:
simp
State after:
no goals