Theorem: Etch.Verification.Stream.LawfulModifiable.get_update' (Etch/StreamFusion/Proofs/OfStream.lean)

State before:
ι : Type
inst✝⁴ : LinearOrder ι
β : Type u_1
m : Type u_2
α : Type u_3
inst✝³ : Zero β
inst✝² : Zero m
inst✝¹ : DecidableEq α
m₀ : m
x t : α
v : β → β
inst✝ : LawfulModifiable α β m
⊢ Readable.get (Modifiable.update m₀ x v) t = if x = t then v (Readable.get m₀ t) else Readable.get m₀ t
Tactic:
split_ifs with h
State after:
case pos
ι : Type
inst✝⁴ : LinearOrder ι
β : Type u_1
m : Type u_2
α : Type u_3
inst✝³ : Zero β
inst✝² : Zero m
inst✝¹ : DecidableEq α
m₀ : m
x t : α
v : β → β
inst✝ : LawfulModifiable α β m
h : x = t
⊢ Readable.get (Modifiable.update m₀ x v) t = v (Readable.get m₀ t)

case neg
ι : Type
inst✝⁴ : LinearOrder ι
β : Type u_1
m : Type u_2
α : Type u_3
inst✝³ : Zero β
inst✝² : Zero m
inst✝¹ : DecidableEq α
m₀ : m
x t : α
v : β → β
inst✝ : LawfulModifiable α β m
h : ¬x = t
⊢ Readable.get (Modifiable.update m₀ x v) t = Readable.get m₀ t

State before:
case pos
ι : Type
inst✝⁴ : LinearOrder ι
β : Type u_1
m : Type u_2
α : Type u_3
inst✝³ : Zero β
inst✝² : Zero m
inst✝¹ : DecidableEq α
m₀ : m
x t : α
v : β → β
inst✝ : LawfulModifiable α β m
h : x = t
⊢ Readable.get (Modifiable.update m₀ x v) t = v (Readable.get m₀ t)
Tactic:
rw [← h, LawfulModifiable.get_update]
State after:
no goals

State before:
case neg
ι : Type
inst✝⁴ : LinearOrder ι
β : Type u_1
m : Type u_2
α : Type u_3
inst✝³ : Zero β
inst✝² : Zero m
inst✝¹ : DecidableEq α
m₀ : m
x t : α
v : β → β
inst✝ : LawfulModifiable α β m
h : ¬x = t
⊢ Readable.get (Modifiable.update m₀ x v) t = Readable.get m₀ t
Tactic:
rw [LawfulModifiable.get_update_ne _ _ _ _ h]
State after:
no goals