Theorem: Etch.Verification.Stream.Stream.mul_index' (Etch/StreamFusion/Proofs/StreamMul.lean)

State before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : (mul a b).σ
⊢ index' (mul a b) q = max (index' a q.1) (index' b q.2)
Tactic:
rw [Stream.index']
State after:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : (mul a b).σ
⊢ (if h : (mul a b).valid q = true then ↑((mul a b).index { val := q, property := h }) else ⊤) =
    max (index' a q.1) (index' b q.2)

State before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : (mul a b).σ
⊢ (if h : (mul a b).valid q = true then ↑((mul a b).index { val := q, property := h }) else ⊤) =
    max (index' a q.1) (index' b q.2)
Tactic:
split_ifs with h
State after:
case pos
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : (mul a b).σ
h : (mul a b).valid q = true
⊢ ↑((mul a b).index { val := q, property := h }) = max (index' a q.1) (index' b q.2)

case neg
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : (mul a b).σ
h : ¬(mul a b).valid q = true
⊢ ⊤ = max (index' a q.1) (index' b q.2)

State before:
case pos
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : (mul a b).σ
h : (mul a b).valid q = true
⊢ ↑((mul a b).index { val := q, property := h }) = max (index' a q.1) (index' b q.2)
Tactic:
simp at h
State after:
case pos
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : (mul a b).σ
h✝ : (mul a b).valid q = true
h : a.valid q.1 = true ∧ b.valid q.2 = true
⊢ ↑((mul a b).index { val := q, property := h✝ }) = max (index' a q.1) (index' b q.2)

State before:
case pos
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : (mul a b).σ
h✝ : (mul a b).valid q = true
h : a.valid q.1 = true ∧ b.valid q.2 = true
⊢ ↑((mul a b).index { val := q, property := h✝ }) = max (index' a q.1) (index' b q.2)
Tactic:
simp [index'_val' _ h.1, index'_val' _ h.2]
State after:
case pos
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : (mul a b).σ
h✝ : (mul a b).valid q = true
h : a.valid q.1 = true ∧ b.valid q.2 = true
⊢ max ↑(a.index (mul.valid.fst { val := q, property := h✝ })) ↑(b.index (mul.valid.snd { val := q, property := h✝ })) =
    max ↑(a.index { val := q.1, property := ⋯ }) ↑(b.index { val := q.2, property := ⋯ })

State before:
case pos
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : (mul a b).σ
h✝ : (mul a b).valid q = true
h : a.valid q.1 = true ∧ b.valid q.2 = true
⊢ max ↑(a.index (mul.valid.fst { val := q, property := h✝ })) ↑(b.index (mul.valid.snd { val := q, property := h✝ })) =
    max ↑(a.index { val := q.1, property := ⋯ }) ↑(b.index { val := q.2, property := ⋯ })
Tactic:
rfl
State after:
no goals

State before:
case neg
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : (mul a b).σ
h : ¬(mul a b).valid q = true
⊢ ⊤ = max (index' a q.1) (index' b q.2)
Tactic:
simp [-not_and, not_and_or] at h
State after:
case neg
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : (mul a b).σ
h : a.valid q.1 = false ∨ b.valid q.2 = false
⊢ ⊤ = max (index' a q.1) (index' b q.2)

State before:
case neg
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : Mul α
a b : Stream ι α
q : (mul a b).σ
h : a.valid q.1 = false ∨ b.valid q.2 = false
⊢ ⊤ = max (index' a q.1) (index' b q.2)
Tactic:
rcases h with h | h
<;> simp [index'_invalid h]
State after:
no goals