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

State before:
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : Mul α
β : Type u_1
inst✝¹ : Mul α
inst✝ : Mul β
a b : Stream ι α
f : α → β
hf : ∀ (x y : α), f (x * y) = f x * f y
⊢ map f (mul a b) = mul (map f a) (map f b)
Tactic:
ext <;> try rfl
State after:
case value
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : Mul α
β : Type u_1
inst✝¹ : Mul α
inst✝ : Mul β
a b : Stream ι α
f : α → β
hf : ∀ (x y : α), f (x * y) = f x * f y
⊢ HEq (map f (mul a b)).value (mul (map f a) (map f b)).value

State before:
case value
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : Mul α
β : Type u_1
inst✝¹ : Mul α
inst✝ : Mul β
a b : Stream ι α
f : α → β
hf : ∀ (x y : α), f (x * y) = f x * f y
⊢ HEq (map f (mul a b)).value (mul (map f a) (map f b)).value
Tactic:
simp only [heq_iff_eq]
State after:
case value
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : Mul α
β : Type u_1
inst✝¹ : Mul α
inst✝ : Mul β
a b : Stream ι α
f : α → β
hf : ∀ (x y : α), f (x * y) = f x * f y
⊢ (map f (mul a b)).value = (mul (map f a) (map f b)).value

State before:
case value
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : Mul α
β : Type u_1
inst✝¹ : Mul α
inst✝ : Mul β
a b : Stream ι α
f : α → β
hf : ∀ (x y : α), f (x * y) = f x * f y
⊢ (map f (mul a b)).value = (mul (map f a) (map f b)).value
Tactic:
ext q₁
State after:
case value.h
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : Mul α
β : Type u_1
inst✝¹ : Mul α
inst✝ : Mul β
a b : Stream ι α
f : α → β
hf : ∀ (x y : α), f (x * y) = f x * f y
q₁ : { x // (map f (mul a b)).ready x = true }
⊢ (map f (mul a b)).value q₁ = (mul (map f a) (map f b)).value q₁

State before:
case value.h
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : Mul α
β : Type u_1
inst✝¹ : Mul α
inst✝ : Mul β
a b : Stream ι α
f : α → β
hf : ∀ (x y : α), f (x * y) = f x * f y
q₁ : { x // (map f (mul a b)).ready x = true }
⊢ (map f (mul a b)).value q₁ = (mul (map f a) (map f b)).value q₁
Tactic:
simp [map, hf]
State after:
case value.h
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : Mul α
β : Type u_1
inst✝¹ : Mul α
inst✝ : Mul β
a b : Stream ι α
f : α → β
hf : ∀ (x y : α), f (x * y) = f x * f y
q₁ : { x // (map f (mul a b)).ready x = true }
⊢ f (a.value (mul.ready.fst q₁)) * f (b.value (mul.ready.snd q₁)) =
    f (a.value (mul.ready.fst q₁)) * f (b.value (mul.ready.snd q₁))

State before:
case value.h
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : Mul α
β : Type u_1
inst✝¹ : Mul α
inst✝ : Mul β
a b : Stream ι α
f : α → β
hf : ∀ (x y : α), f (x * y) = f x * f y
q₁ : { x // (map f (mul a b)).ready x = true }
⊢ f (a.value (mul.ready.fst q₁)) * f (b.value (mul.ready.snd q₁)) =
    f (a.value (mul.ready.fst q₁)) * f (b.value (mul.ready.snd q₁))
Tactic:
rfl
State after:
no goals

State before:
case ready
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : Mul α
β : Type u_1
inst✝¹ : Mul α
inst✝ : Mul β
a b : Stream ι α
f : α → β
hf : ∀ (x y : α), f (x * y) = f x * f y
⊢ HEq (map f (mul a b)).ready (mul (map f a) (map f b)).ready
Tactic:
rfl
State after:
no goals