Theorem: SciLean.Rand.foobar.arg_acc.IsAffineMap (SciLean/Core/Rand/Distributions/ListSumTest.lean)

State before:
R : Type u_1
inst✝¹ : RealScalar R
inst✝ : ToString R
l : List R
⊢ _root_.IsAffineMap ℝ fun acc => foobar l acc
Tactic:
induction l <;> (simp[foobar]; fun_prop)
State after:
no goals

State before:
case cons
R : Type u_1
inst✝¹ : RealScalar R
inst✝ : ToString R
head✝ : R
tail✝ : List R
tail_ih✝ : _root_.IsAffineMap ℝ fun acc => foobar tail✝ acc
⊢ _root_.IsAffineMap ℝ fun acc => foobar (head✝ :: tail✝) acc
Tactic:
simp[foobar]
State after:
case cons
R : Type u_1
inst✝¹ : RealScalar R
inst✝ : ToString R
head✝ : R
tail✝ : List R
tail_ih✝ : _root_.IsAffineMap ℝ fun acc => foobar tail✝ acc
⊢ _root_.IsAffineMap ℝ fun acc => foobar tail✝ (acc + head✝)

State before:
case cons
R : Type u_1
inst✝¹ : RealScalar R
inst✝ : ToString R
head✝ : R
tail✝ : List R
tail_ih✝ : _root_.IsAffineMap ℝ fun acc => foobar tail✝ acc
⊢ _root_.IsAffineMap ℝ fun acc => foobar tail✝ (acc + head✝)
Tactic:
fun_prop
State after:
no goals