[GOAL]
α : Type u_1
⊢ LeftInverse toList ofList
[PROOFSTEP]
intro xs
[GOAL]
α : Type u_1
xs : List α
⊢ toList (ofList xs) = xs
[PROOFSTEP]
induction xs
[GOAL]
case nil
α : Type u_1
⊢ toList (ofList []) = []
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
head✝ : α
tail✝ : List α
tail_ih✝ : toList (ofList tail✝) = tail✝
⊢ toList (ofList (head✝ :: tail✝)) = head✝ :: tail✝
[PROOFSTEP]
simpa [ofList, toList]
[GOAL]
α : Type u_1
⊢ Function.RightInverse toList ofList
[PROOFSTEP]
intro xs
[GOAL]
α : Type u_1
xs : LazyList α
⊢ ofList (toList xs) = xs
[PROOFSTEP]
induction' xs using LazyList.rec with _ _ _ _ ih
[GOAL]
case nil
α : Type u_1
⊢ ofList (toList nil) = nil
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
xs : LazyList α
hd✝ : α
tl✝ : Thunk (LazyList α)
tl_ih✝ : ?m.1024 tl✝
⊢ ofList (toList (cons hd✝ tl✝)) = cons hd✝ tl✝
[PROOFSTEP]
simpa only [toList, ofList, cons.injEq, true_and]
[GOAL]
case mk
α : Type u_1
xs : LazyList α
fn✝ : Unit → LazyList α
ih : ∀ (a : Unit), ofList (toList (fn✝ a)) = fn✝ a
⊢ { fn := fun x => ofList (toList (Thunk.get { fn := fn✝ })) } = { fn := fn✝ }
[PROOFSTEP]
rw [Thunk.get, ih]
[GOAL]
α : Type u
inst✝ : DecidableEq α
x : α
xs : Thunk (LazyList α)
y : α
ys : Thunk (LazyList α)
h : x = y
h2 : ¬Thunk.get xs = Thunk.get ys
⊢ Decidable (cons x xs = cons y ys)
[PROOFSTEP]
apply isFalse
[GOAL]
case h
α : Type u
inst✝ : DecidableEq α
x : α
xs : Thunk (LazyList α)
y : α
ys : Thunk (LazyList α)
h : x = y
h2 : ¬Thunk.get xs = Thunk.get ys
⊢ ¬cons x xs = cons y ys
[PROOFSTEP]
simp only [cons.injEq, not_and]
[GOAL]
case h
α : Type u
inst✝ : DecidableEq α
x : α
xs : Thunk (LazyList α)
y : α
ys : Thunk (LazyList α)
h : x = y
h2 : ¬Thunk.get xs = Thunk.get ys
⊢ x = y → ¬xs = ys
[PROOFSTEP]
intro _ xs_ys
[GOAL]
case h
α : Type u
inst✝ : DecidableEq α
x : α
xs : Thunk (LazyList α)
y : α
ys : Thunk (LazyList α)
h : x = y
h2 : ¬Thunk.get xs = Thunk.get ys
a✝ : x = y
xs_ys : xs = ys
⊢ False
[PROOFSTEP]
apply h2
[GOAL]
case h
α : Type u
inst✝ : DecidableEq α
x : α
xs : Thunk (LazyList α)
y : α
ys : Thunk (LazyList α)
h : x = y
h2 : ¬Thunk.get xs = Thunk.get ys
a✝ : x = y
xs_ys : xs = ys
⊢ Thunk.get xs = Thunk.get ys
[PROOFSTEP]
rw [xs_ys]
[GOAL]
α : Type u
inst✝ : DecidableEq α
x : α
xs : Thunk (LazyList α)
y : α
ys : Thunk (LazyList α)
h : x = y
h2 : Thunk.get xs = Thunk.get ys
⊢ Decidable (cons x xs = cons y ys)
[PROOFSTEP]
apply isTrue
[GOAL]
case h
α : Type u
inst✝ : DecidableEq α
x : α
xs : Thunk (LazyList α)
y : α
ys : Thunk (LazyList α)
h : x = y
h2 : Thunk.get xs = Thunk.get ys
⊢ cons x xs = cons y ys
[PROOFSTEP]
congr
[GOAL]
case h.e_tl
α : Type u
inst✝ : DecidableEq α
x : α
xs : Thunk (LazyList α)
y : α
ys : Thunk (LazyList α)
h : x = y
h2 : Thunk.get xs = Thunk.get ys
⊢ xs = ys
[PROOFSTEP]
ext
[GOAL]
case h.e_tl.eq
α : Type u
inst✝ : DecidableEq α
x : α
xs : Thunk (LazyList α)
y : α
ys : Thunk (LazyList α)
h : x = y
h2 : Thunk.get xs = Thunk.get ys
⊢ Thunk.get xs = Thunk.get ys
[PROOFSTEP]
exact h2
[GOAL]
α : Type u
inst✝ : DecidableEq α
x : α
xs : Thunk (LazyList α)
y : α
ys : Thunk (LazyList α)
h : ¬x = y
⊢ Decidable (cons x xs = cons y ys)
[PROOFSTEP]
apply isFalse
[GOAL]
case h
α : Type u
inst✝ : DecidableEq α
x : α
xs : Thunk (LazyList α)
y : α
ys : Thunk (LazyList α)
h : ¬x = y
⊢ ¬cons x xs = cons y ys
[PROOFSTEP]
simp only [cons.injEq, not_and]
[GOAL]
case h
α : Type u
inst✝ : DecidableEq α
x : α
xs : Thunk (LazyList α)
y : α
ys : Thunk (LazyList α)
h : ¬x = y
⊢ x = y → ¬xs = ys
[PROOFSTEP]
intro
[GOAL]
case h
α : Type u
inst✝ : DecidableEq α
x : α
xs : Thunk (LazyList α)
y : α
ys : Thunk (LazyList α)
h : ¬x = y
a✝ : x = y
⊢ ¬xs = ys
[PROOFSTEP]
contradiction
[GOAL]
α : Type u
inst✝ : DecidableEq α
hd✝ : α
tl✝ : Thunk (LazyList α)
⊢ Decidable (nil = cons hd✝ tl✝)
[PROOFSTEP]
apply isFalse
[GOAL]
case h
α : Type u
inst✝ : DecidableEq α
hd✝ : α
tl✝ : Thunk (LazyList α)
⊢ ¬nil = cons hd✝ tl✝
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝ : DecidableEq α
hd✝ : α
tl✝ : Thunk (LazyList α)
⊢ Decidable (cons hd✝ tl✝ = nil)
[PROOFSTEP]
apply isFalse
[GOAL]
case h
α : Type u
inst✝ : DecidableEq α
hd✝ : α
tl✝ : Thunk (LazyList α)
⊢ ¬cons hd✝ tl✝ = nil
[PROOFSTEP]
simp
[GOAL]
⊢ LawfulTraversable LazyList
[PROOFSTEP]
apply Equiv.isLawfulTraversable' listEquivLazyList
[GOAL]
case h₀
⊢ ∀ {α β : Type ?u.19468} (f : α → β), Functor.map f = Equiv.map listEquivLazyList f
[PROOFSTEP]
intros
[GOAL]
case h₁
⊢ ∀ {α β : Type ?u.19468} (f : β), Functor.mapConst f = (Equiv.map listEquivLazyList ∘ const α) f
[PROOFSTEP]
intros
[GOAL]
case h₂
⊢ ∀ {F : Type ?u.19468 → Type ?u.19468} [inst : Applicative F] [inst_1 : LawfulApplicative F] {α β : Type ?u.19468}
    (f : α → F β), traverse f = Equiv.traverse listEquivLazyList f
[PROOFSTEP]
intros
[GOAL]
case h₀
α✝ β✝ : Type ?u.19468
f✝ : α✝ → β✝
⊢ Functor.map f✝ = Equiv.map listEquivLazyList f✝
[PROOFSTEP]
ext
[GOAL]
case h₁
α✝ β✝ : Type ?u.19468
f✝ : β✝
⊢ Functor.mapConst f✝ = (Equiv.map listEquivLazyList ∘ const α✝) f✝
[PROOFSTEP]
ext
[GOAL]
case h₂
F✝ : Type ?u.19468 → Type ?u.19468
inst✝¹ : Applicative F✝
inst✝ : LawfulApplicative F✝
α✝ β✝ : Type ?u.19468
f✝ : α✝ → F✝ β✝
⊢ traverse f✝ = Equiv.traverse listEquivLazyList f✝
[PROOFSTEP]
ext
[GOAL]
case h₀.h
α✝ β✝ : Type ?u.19468
f✝ : α✝ → β✝
x✝ : LazyList α✝
⊢ f✝ <$> x✝ = Equiv.map listEquivLazyList f✝ x✝
[PROOFSTEP]
rename_i f xs
[GOAL]
case h₁.h
α✝ β✝ : Type ?u.19468
f✝ : β✝
x✝ : LazyList α✝
⊢ Functor.mapConst f✝ x✝ = (Equiv.map listEquivLazyList ∘ const α✝) f✝ x✝
[PROOFSTEP]
rename_i f xs
[GOAL]
case h₂.h
F✝ : Type ?u.19468 → Type ?u.19468
inst✝¹ : Applicative F✝
inst✝ : LawfulApplicative F✝
α✝ β✝ : Type ?u.19468
f✝ : α✝ → F✝ β✝
x✝ : LazyList α✝
⊢ traverse f✝ x✝ = Equiv.traverse listEquivLazyList f✝ x✝
[PROOFSTEP]
rename_i f xs
[GOAL]
case h₀.h
α✝ β✝ : Type ?u.19468
f : α✝ → β✝
xs : LazyList α✝
⊢ f <$> xs = Equiv.map listEquivLazyList f xs
[PROOFSTEP]
induction' xs using LazyList.rec with _ _ _ _ ih
[GOAL]
case h₀.h.nil
α✝ β✝ : Type ?u.19468
f : α✝ → β✝
⊢ f <$> nil = Equiv.map listEquivLazyList f nil
[PROOFSTEP]
rfl
[GOAL]
case h₀.h.cons
α✝ β✝ : Type ?u.19468
f : α✝ → β✝
xs : LazyList α✝
hd✝ : α✝
tl✝ : Thunk (LazyList α✝)
tl_ih✝ : ?m.19696 tl✝
⊢ f <$> cons hd✝ tl✝ = Equiv.map listEquivLazyList f (cons hd✝ tl✝)
[PROOFSTEP]
simpa only [Equiv.map, Functor.map, listEquivLazyList, Equiv.coe_fn_symm_mk, Equiv.coe_fn_mk, LazyList.traverse,
  Seq.seq, toList, ofList, cons.injEq, true_and]
[GOAL]
case h₀.h.mk
α✝ β✝ : Type ?u.19468
f : α✝ → β✝
xs : LazyList α✝
fn✝ : Unit → LazyList α✝
ih : ∀ (a : Unit), f <$> fn✝ a = Equiv.map listEquivLazyList f (fn✝ a)
⊢ Thunk.pure (LazyList.traverse f (Thunk.get { fn := fn✝ })) =
    { fn := fun x => ofList (List.map f (toList (Thunk.get { fn := fn✝ }))) }
[PROOFSTEP]
ext
[GOAL]
case h₀.h.mk.eq
α✝ β✝ : Type ?u.19468
f : α✝ → β✝
xs : LazyList α✝
fn✝ : Unit → LazyList α✝
ih : ∀ (a : Unit), f <$> fn✝ a = Equiv.map listEquivLazyList f (fn✝ a)
⊢ Thunk.get (Thunk.pure (LazyList.traverse f (Thunk.get { fn := fn✝ }))) =
    Thunk.get { fn := fun x => ofList (List.map f (toList (Thunk.get { fn := fn✝ }))) }
[PROOFSTEP]
apply ih
[GOAL]
case h₁.h
α✝ β✝ : Type ?u.19468
f : β✝
xs : LazyList α✝
⊢ Functor.mapConst f xs = (Equiv.map listEquivLazyList ∘ const α✝) f xs
[PROOFSTEP]
simp only [Equiv.map, listEquivLazyList, Equiv.coe_fn_symm_mk, Equiv.coe_fn_mk, comp, Functor.mapConst]
[GOAL]
case h₁.h
α✝ β✝ : Type ?u.19468
f : β✝
xs : LazyList α✝
⊢ LazyList.traverse (const α✝ f) xs = ofList (const α✝ f <$> toList xs)
[PROOFSTEP]
induction' xs using LazyList.rec with _ _ _ _ ih
[GOAL]
case h₁.h.nil
α✝ β✝ : Type ?u.19468
f : β✝
⊢ LazyList.traverse (const α✝ f) nil = ofList (const α✝ f <$> toList nil)
[PROOFSTEP]
rfl
[GOAL]
case h₁.h.cons
α✝ β✝ : Type ?u.19468
f : β✝
xs : LazyList α✝
hd✝ : α✝
tl✝ : Thunk (LazyList α✝)
tl_ih✝ : ?m.21260 tl✝
⊢ LazyList.traverse (const α✝ f) (cons hd✝ tl✝) = ofList (const α✝ f <$> toList (cons hd✝ tl✝))
[PROOFSTEP]
simpa only [toList, ofList, LazyList.traverse, Seq.seq, Functor.map, cons.injEq, true_and]
[GOAL]
case h₁.h.mk
α✝ β✝ : Type ?u.19468
f : β✝
xs : LazyList α✝
fn✝ : Unit → LazyList α✝
ih : ∀ (a : Unit), LazyList.traverse (const α✝ f) (fn✝ a) = ofList (const α✝ f <$> toList (fn✝ a))
⊢ Thunk.pure (LazyList.traverse (const α✝ f) (Thunk.get { fn := fn✝ })) =
    { fn := fun x => ofList (List.map (const α✝ f) (toList (Thunk.get { fn := fn✝ }))) }
[PROOFSTEP]
congr
[GOAL]
case h₁.h.mk.e_a
α✝ β✝ : Type ?u.19468
f : β✝
xs : LazyList α✝
fn✝ : Unit → LazyList α✝
ih : ∀ (a : Unit), LazyList.traverse (const α✝ f) (fn✝ a) = ofList (const α✝ f <$> toList (fn✝ a))
⊢ LazyList.traverse (const α✝ f) (Thunk.get { fn := fn✝ }) =
    ofList (List.map (const α✝ f) (toList (Thunk.get { fn := fn✝ })))
[PROOFSTEP]
apply ih
[GOAL]
case h₂.h
F✝ : Type ?u.19468 → Type ?u.19468
inst✝¹ : Applicative F✝
inst✝ : LawfulApplicative F✝
α✝ β✝ : Type ?u.19468
f : α✝ → F✝ β✝
xs : LazyList α✝
⊢ traverse f xs = Equiv.traverse listEquivLazyList f xs
[PROOFSTEP]
simp only [traverse, Equiv.traverse, listEquivLazyList, Equiv.coe_fn_mk, Equiv.coe_fn_symm_mk]
[GOAL]
case h₂.h
F✝ : Type ?u.19468 → Type ?u.19468
inst✝¹ : Applicative F✝
inst✝ : LawfulApplicative F✝
α✝ β✝ : Type ?u.19468
f : α✝ → F✝ β✝
xs : LazyList α✝
⊢ LazyList.traverse f xs = ofList <$> List.traverse f (toList xs)
[PROOFSTEP]
induction' xs using LazyList.rec with _ tl ih _ ih
[GOAL]
case h₂.h.nil
F✝ : Type ?u.19468 → Type ?u.19468
inst✝¹ : Applicative F✝
inst✝ : LawfulApplicative F✝
α✝ β✝ : Type ?u.19468
f : α✝ → F✝ β✝
⊢ LazyList.traverse f nil = ofList <$> List.traverse f (toList nil)
[PROOFSTEP]
simp only [List.traverse, map_pure]
[GOAL]
case h₂.h.nil
F✝ : Type ?u.19468 → Type ?u.19468
inst✝¹ : Applicative F✝
inst✝ : LawfulApplicative F✝
α✝ β✝ : Type ?u.19468
f : α✝ → F✝ β✝
⊢ LazyList.traverse f nil = pure (ofList [])
[PROOFSTEP]
rfl
[GOAL]
case h₂.h.cons
F✝ : Type ?u.19468 → Type ?u.19468
inst✝¹ : Applicative F✝
inst✝ : LawfulApplicative F✝
α✝ β✝ : Type ?u.19468
f : α✝ → F✝ β✝
xs : LazyList α✝
hd✝ : α✝
tl : Thunk (LazyList α✝)
ih : ?m.22684 tl
⊢ LazyList.traverse f (cons hd✝ tl) = ofList <$> List.traverse f (toList (cons hd✝ tl))
[PROOFSTEP]
have : tl.get.traverse f = ofList <$> tl.get.toList.traverse f := ih
[GOAL]
case h₂.h.cons
F✝ : Type ?u.19468 → Type ?u.19468
inst✝¹ : Applicative F✝
inst✝ : LawfulApplicative F✝
α✝ β✝ : Type ?u.19468
f : α✝ → F✝ β✝
xs : LazyList α✝
hd✝ : α✝
tl : Thunk (LazyList α✝)
ih this : LazyList.traverse f (Thunk.get tl) = ofList <$> List.traverse f (toList (Thunk.get tl))
⊢ LazyList.traverse f (cons hd✝ tl) = ofList <$> List.traverse f (toList (cons hd✝ tl))
[PROOFSTEP]
simp only [traverse._eq_2, ih, Functor.map_map, seq_map_assoc, toList, List.traverse, map_seq]
[GOAL]
case h₂.h.cons
F✝ : Type ?u.19468 → Type ?u.19468
inst✝¹ : Applicative F✝
inst✝ : LawfulApplicative F✝
α✝ β✝ : Type ?u.19468
f : α✝ → F✝ β✝
xs : LazyList α✝
hd✝ : α✝
tl : Thunk (LazyList α✝)
ih this : LazyList.traverse f (Thunk.get tl) = ofList <$> List.traverse f (toList (Thunk.get tl))
⊢ (Seq.seq (((fun x => x ∘ Thunk.pure ∘ ofList) ∘ cons) <$> f hd✝) fun x => List.traverse f (toList (Thunk.get tl))) =
    Seq.seq (((fun x => ofList ∘ x) ∘ List.cons) <$> f hd✝) fun x => List.traverse f (toList (Thunk.get tl))
[PROOFSTEP]
rfl
[GOAL]
case h₂.h.mk
F✝ : Type ?u.19468 → Type ?u.19468
inst✝¹ : Applicative F✝
inst✝ : LawfulApplicative F✝
α✝ β✝ : Type ?u.19468
f : α✝ → F✝ β✝
xs : LazyList α✝
fn✝ : Unit → LazyList α✝
ih : ∀ (a : Unit), LazyList.traverse f (fn✝ a) = ofList <$> List.traverse f (toList (fn✝ a))
⊢ LazyList.traverse f (Thunk.get { fn := fn✝ }) = ofList <$> List.traverse f (toList (Thunk.get { fn := fn✝ }))
[PROOFSTEP]
apply ih
[GOAL]
α : Type u_1
xs : LazyList α
⊢ append xs (Thunk.pure nil) = xs
[PROOFSTEP]
induction' xs using LazyList.rec with _ _ _ _ ih
[GOAL]
case nil
α : Type u_1
⊢ append nil (Thunk.pure nil) = nil
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
xs : LazyList α
hd✝ : α
tl✝ : Thunk (LazyList α)
tl_ih✝ : ?m.62141 tl✝
⊢ append (cons hd✝ tl✝) (Thunk.pure nil) = cons hd✝ tl✝
[PROOFSTEP]
simpa only [append, cons.injEq, true_and]
[GOAL]
case mk
α : Type u_1
xs : LazyList α
fn✝ : Unit → LazyList α
ih : ∀ (a : Unit), append (fn✝ a) (Thunk.pure nil) = fn✝ a
⊢ { fn := fun x => append (Thunk.get { fn := fn✝ }) (Thunk.pure nil) } = { fn := fn✝ }
[PROOFSTEP]
ext
[GOAL]
case mk.eq
α : Type u_1
xs : LazyList α
fn✝ : Unit → LazyList α
ih : ∀ (a : Unit), append (fn✝ a) (Thunk.pure nil) = fn✝ a
⊢ Thunk.get { fn := fun x => append (Thunk.get { fn := fn✝ }) (Thunk.pure nil) } = Thunk.get { fn := fn✝ }
[PROOFSTEP]
apply ih
[GOAL]
α : Type u_1
xs ys zs : LazyList α
⊢ append (append xs { fn := fun x => ys }) { fn := fun x => zs } =
    append xs { fn := fun x => append ys { fn := fun x => zs } }
[PROOFSTEP]
induction' xs using LazyList.rec with _ _ _ _ ih
[GOAL]
case nil
α : Type u_1
ys zs : LazyList α
⊢ append (append nil { fn := fun x => ys }) { fn := fun x => zs } =
    append nil { fn := fun x => append ys { fn := fun x => zs } }
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
xs ys zs : LazyList α
hd✝ : α
tl✝ : Thunk (LazyList α)
tl_ih✝ : ?m.65384 tl✝
⊢ append (append (cons hd✝ tl✝) { fn := fun x => ys }) { fn := fun x => zs } =
    append (cons hd✝ tl✝) { fn := fun x => append ys { fn := fun x => zs } }
[PROOFSTEP]
simpa only [append, cons.injEq, true_and]
[GOAL]
case mk
α : Type u_1
xs ys zs : LazyList α
fn✝ : Unit → LazyList α
ih :
  ∀ (a : Unit),
    append (append (fn✝ a) { fn := fun x => ys }) { fn := fun x => zs } =
      append (fn✝ a) { fn := fun x => append ys { fn := fun x => zs } }
⊢ {
      fn := fun x =>
        append (Thunk.get { fn := fun x => append (Thunk.get { fn := fn✝ }) { fn := fun x => ys } })
          { fn := fun x => zs } } =
    { fn := fun x => append (Thunk.get { fn := fn✝ }) { fn := fun x => append ys { fn := fun x => zs } } }
[PROOFSTEP]
ext
[GOAL]
case mk.eq
α : Type u_1
xs ys zs : LazyList α
fn✝ : Unit → LazyList α
ih :
  ∀ (a : Unit),
    append (append (fn✝ a) { fn := fun x => ys }) { fn := fun x => zs } =
      append (fn✝ a) { fn := fun x => append ys { fn := fun x => zs } }
⊢ Thunk.get
      {
        fn := fun x =>
          append (Thunk.get { fn := fun x => append (Thunk.get { fn := fn✝ }) { fn := fun x => ys } })
            { fn := fun x => zs } } =
    Thunk.get { fn := fun x => append (Thunk.get { fn := fn✝ }) { fn := fun x => append ys { fn := fun x => zs } } }
[PROOFSTEP]
apply ih
[GOAL]
α : Type u_1
β : Type u_2
xs : LazyList α
ys : Thunk (LazyList α)
f : α → LazyList β
⊢ LazyList.bind (append xs ys) f = append (LazyList.bind xs f) { fn := fun x => LazyList.bind (Thunk.get ys) f }
[PROOFSTEP]
match xs with
| LazyList.nil => rfl
| LazyList.cons x xs =>
  simp only [append, Thunk.get, LazyList.bind]
  have := append_bind xs.get ys f
  simp only [Thunk.get] at this
  rw [this, append_assoc]
[GOAL]
α : Type u_1
β : Type u_2
xs : LazyList α
ys : Thunk (LazyList α)
f : α → LazyList β
⊢ LazyList.bind (append nil ys) f = append (LazyList.bind nil f) { fn := fun x => LazyList.bind (Thunk.get ys) f }
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
xs✝ : LazyList α
ys : Thunk (LazyList α)
f : α → LazyList β
x : α
xs : Thunk (LazyList α)
⊢ LazyList.bind (append (cons x xs) ys) f =
    append (LazyList.bind (cons x xs) f) { fn := fun x => LazyList.bind (Thunk.get ys) f }
[PROOFSTEP]
simp only [append, Thunk.get, LazyList.bind]
[GOAL]
α : Type u_1
β : Type u_2
xs✝ : LazyList α
ys : Thunk (LazyList α)
f : α → LazyList β
x : α
xs : Thunk (LazyList α)
⊢ append (f x) { fn := fun x => LazyList.bind (append (Thunk.fn xs ()) ys) f } =
    append (append (f x) { fn := fun x => LazyList.bind (Thunk.fn xs ()) f })
      { fn := fun x => LazyList.bind (Thunk.fn ys ()) f }
[PROOFSTEP]
have := append_bind xs.get ys f
[GOAL]
α : Type u_1
β : Type u_2
xs✝ : LazyList α
ys : Thunk (LazyList α)
f : α → LazyList β
x : α
xs : Thunk (LazyList α)
this :
  LazyList.bind (append (Thunk.get xs) ys) f =
    append (LazyList.bind (Thunk.get xs) f) { fn := fun x => LazyList.bind (Thunk.get ys) f }
⊢ append (f x) { fn := fun x => LazyList.bind (append (Thunk.fn xs ()) ys) f } =
    append (append (f x) { fn := fun x => LazyList.bind (Thunk.fn xs ()) f })
      { fn := fun x => LazyList.bind (Thunk.fn ys ()) f }
[PROOFSTEP]
simp only [Thunk.get] at this
[GOAL]
α : Type u_1
β : Type u_2
xs✝ : LazyList α
ys : Thunk (LazyList α)
f : α → LazyList β
x : α
xs : Thunk (LazyList α)
this :
  LazyList.bind (append (Thunk.fn xs ()) ys) f =
    append (LazyList.bind (Thunk.fn xs ()) f) { fn := fun x => LazyList.bind (Thunk.fn ys ()) f }
⊢ append (f x) { fn := fun x => LazyList.bind (append (Thunk.fn xs ()) ys) f } =
    append (append (f x) { fn := fun x => LazyList.bind (Thunk.fn xs ()) f })
      { fn := fun x => LazyList.bind (Thunk.fn ys ()) f }
[PROOFSTEP]
rw [this, append_assoc]
[GOAL]
⊢ ∀ {α : Type ?u.75696} (x : LazyList α), id <$> x = x
[PROOFSTEP]
intro _ xs
[GOAL]
α✝ : Type ?u.75696
xs : LazyList α✝
⊢ id <$> xs = xs
[PROOFSTEP]
induction' xs using LazyList.rec with _ _ _ _ ih
[GOAL]
case nil
α✝ : Type ?u.75696
⊢ id <$> nil = nil
[PROOFSTEP]
rfl
[GOAL]
case cons
α✝ : Type ?u.75696
xs : LazyList α✝
hd✝ : α✝
tl✝ : Thunk (LazyList α✝)
tl_ih✝ : ?m.75815 tl✝
⊢ id <$> cons hd✝ tl✝ = cons hd✝ tl✝
[PROOFSTEP]
simpa only [Functor.map, traverse._eq_2, id_eq, Id.map_eq, Seq.seq, cons.injEq, true_and]
[GOAL]
case mk
α✝ : Type ?u.75696
xs : LazyList α✝
fn✝ : Unit → LazyList α✝
ih : ∀ (a : Unit), id <$> fn✝ a = fn✝ a
⊢ Thunk.pure (LazyList.traverse id (Thunk.get { fn := fn✝ })) = { fn := fn✝ }
[PROOFSTEP]
ext
[GOAL]
case mk.eq
α✝ : Type ?u.75696
xs : LazyList α✝
fn✝ : Unit → LazyList α✝
ih : ∀ (a : Unit), id <$> fn✝ a = fn✝ a
⊢ Thunk.get (Thunk.pure (LazyList.traverse id (Thunk.get { fn := fn✝ }))) = Thunk.get { fn := fn✝ }
[PROOFSTEP]
apply ih
[GOAL]
⊢ ∀ {α β : Type ?u.75696} (x : α) (f : α → LazyList β), pure x >>= f = f x
[PROOFSTEP]
intros
[GOAL]
α✝ β✝ : Type ?u.75696
x✝ : α✝
f✝ : α✝ → LazyList β✝
⊢ pure x✝ >>= f✝ = f✝ x✝
[PROOFSTEP]
simp only [bind, pure, singleton, LazyList.bind]
[GOAL]
α✝ β✝ : Type ?u.75696
x✝ : α✝
f✝ : α✝ → LazyList β✝
⊢ append (f✝ x✝) { fn := fun x => LazyList.bind (Thunk.get (Thunk.pure nil)) f✝ } = f✝ x✝
[PROOFSTEP]
apply append_nil
[GOAL]
⊢ ∀ {α β γ : Type ?u.75696} (x : LazyList α) (f : α → LazyList β) (g : β → LazyList γ),
    x >>= f >>= g = x >>= fun x => f x >>= g
[PROOFSTEP]
intro _ _ _ xs _ _
[GOAL]
α✝ β✝ γ✝ : Type ?u.75696
xs : LazyList α✝
f✝ : α✝ → LazyList β✝
g✝ : β✝ → LazyList γ✝
⊢ xs >>= f✝ >>= g✝ = xs >>= fun x => f✝ x >>= g✝
[PROOFSTEP]
induction' xs using LazyList.rec with _ _ _ _ ih
[GOAL]
case nil
α✝ β✝ γ✝ : Type ?u.75696
f✝ : α✝ → LazyList β✝
g✝ : β✝ → LazyList γ✝
⊢ nil >>= f✝ >>= g✝ = nil >>= fun x => f✝ x >>= g✝
[PROOFSTEP]
rfl
[GOAL]
case cons
α✝ β✝ γ✝ : Type ?u.75696
xs : LazyList α✝
f✝ : α✝ → LazyList β✝
g✝ : β✝ → LazyList γ✝
hd✝ : α✝
tl✝ : Thunk (LazyList α✝)
tl_ih✝ : ?m.76333 tl✝
⊢ cons hd✝ tl✝ >>= f✝ >>= g✝ = cons hd✝ tl✝ >>= fun x => f✝ x >>= g✝
[PROOFSTEP]
simp only [bind, LazyList.bind, append_bind]
[GOAL]
case cons
α✝ β✝ γ✝ : Type ?u.75696
xs : LazyList α✝
f✝ : α✝ → LazyList β✝
g✝ : β✝ → LazyList γ✝
hd✝ : α✝
tl✝ : Thunk (LazyList α✝)
tl_ih✝ : ?m.76333 tl✝
⊢ append (LazyList.bind (f✝ hd✝) g✝)
      { fn := fun x => LazyList.bind (Thunk.get { fn := fun x => LazyList.bind (Thunk.get tl✝) f✝ }) g✝ } =
    append (LazyList.bind (f✝ hd✝) g✝) { fn := fun x => LazyList.bind (Thunk.get tl✝) fun x => LazyList.bind (f✝ x) g✝ }
[PROOFSTEP]
congr
[GOAL]
case mk
α✝ β✝ γ✝ : Type ?u.75696
xs : LazyList α✝
f✝ : α✝ → LazyList β✝
g✝ : β✝ → LazyList γ✝
fn✝ : Unit → LazyList α✝
ih : ∀ (a : Unit), fn✝ a >>= f✝ >>= g✝ = fn✝ a >>= fun x => f✝ x >>= g✝
⊢ { fn := fun x => LazyList.bind (Thunk.get { fn := fun x => LazyList.bind (Thunk.get { fn := fn✝ }) f✝ }) g✝ } =
    { fn := fun x => LazyList.bind (Thunk.get { fn := fn✝ }) fun x => LazyList.bind (f✝ x) g✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.e_fn
α✝ β✝ γ✝ : Type ?u.75696
xs : LazyList α✝
f✝ : α✝ → LazyList β✝
g✝ : β✝ → LazyList γ✝
fn✝ : Unit → LazyList α✝
ih : ∀ (a : Unit), fn✝ a >>= f✝ >>= g✝ = fn✝ a >>= fun x => f✝ x >>= g✝
⊢ (fun x => LazyList.bind (Thunk.get { fn := fun x => LazyList.bind (Thunk.get { fn := fn✝ }) f✝ }) g✝) = fun x =>
    LazyList.bind (Thunk.get { fn := fn✝ }) fun x => LazyList.bind (f✝ x) g✝
[PROOFSTEP]
funext
[GOAL]
case mk.e_fn.h
α✝ β✝ γ✝ : Type ?u.75696
xs : LazyList α✝
f✝ : α✝ → LazyList β✝
g✝ : β✝ → LazyList γ✝
fn✝ : Unit → LazyList α✝
ih : ∀ (a : Unit), fn✝ a >>= f✝ >>= g✝ = fn✝ a >>= fun x => f✝ x >>= g✝
x✝ : Unit
⊢ LazyList.bind (Thunk.get { fn := fun x => LazyList.bind (Thunk.get { fn := fn✝ }) f✝ }) g✝ =
    LazyList.bind (Thunk.get { fn := fn✝ }) fun x => LazyList.bind (f✝ x) g✝
[PROOFSTEP]
apply ih
[GOAL]
⊢ ∀ {α β : Type ?u.75696} (f : α → β) (x : LazyList α),
    (do
        let y ← x
        pure (f y)) =
      f <$> x
[PROOFSTEP]
intro _ _ f xs
[GOAL]
α✝ β✝ : Type ?u.75696
f : α✝ → β✝
xs : LazyList α✝
⊢ (do
      let y ← xs
      pure (f y)) =
    f <$> xs
[PROOFSTEP]
simp only [bind, Functor.map, pure, singleton]
[GOAL]
α✝ β✝ : Type ?u.75696
f : α✝ → β✝
xs : LazyList α✝
⊢ (LazyList.bind xs fun y => cons (f y) (Thunk.pure nil)) = LazyList.traverse f xs
[PROOFSTEP]
induction' xs using LazyList.rec with _ _ _ _ ih
[GOAL]
case nil
α✝ β✝ : Type ?u.75696
f : α✝ → β✝
⊢ (LazyList.bind nil fun y => cons (f y) (Thunk.pure nil)) = LazyList.traverse f nil
[PROOFSTEP]
rfl
[GOAL]
case cons
α✝ β✝ : Type ?u.75696
f : α✝ → β✝
xs : LazyList α✝
hd✝ : α✝
tl✝ : Thunk (LazyList α✝)
tl_ih✝ : ?m.77095 tl✝
⊢ (LazyList.bind (cons hd✝ tl✝) fun y => cons (f y) (Thunk.pure nil)) = LazyList.traverse f (cons hd✝ tl✝)
[PROOFSTEP]
simp only [bind._eq_2, append, traverse._eq_2, Id.map_eq, cons.injEq, true_and]
[GOAL]
case cons
α✝ β✝ : Type ?u.75696
f : α✝ → β✝
xs : LazyList α✝
hd✝ : α✝
tl✝ : Thunk (LazyList α✝)
tl_ih✝ : ?m.77095 tl✝
⊢ cons (f hd✝)
      {
        fn := fun x =>
          append (Thunk.get (Thunk.pure nil))
            { fn := fun x => LazyList.bind (Thunk.get tl✝) fun y => cons (f y) (Thunk.pure nil) } } =
    Seq.seq (cons (f hd✝)) fun x => Thunk.pure (LazyList.traverse f (Thunk.get tl✝))
[PROOFSTEP]
congr
[GOAL]
case mk
α✝ β✝ : Type ?u.75696
f : α✝ → β✝
xs : LazyList α✝
fn✝ : Unit → LazyList α✝
ih : ∀ (a : Unit), (LazyList.bind (fn✝ a) fun y => cons (f y) (Thunk.pure nil)) = LazyList.traverse f (fn✝ a)
⊢ {
      fn := fun x =>
        append (Thunk.get (Thunk.pure nil))
          { fn := fun x => LazyList.bind (Thunk.get { fn := fn✝ }) fun y => cons (f y) (Thunk.pure nil) } } =
    (fun x => Thunk.pure (LazyList.traverse f (Thunk.get { fn := fn✝ }))) ()
[PROOFSTEP]
ext
[GOAL]
case mk.eq
α✝ β✝ : Type ?u.75696
f : α✝ → β✝
xs : LazyList α✝
fn✝ : Unit → LazyList α✝
ih : ∀ (a : Unit), (LazyList.bind (fn✝ a) fun y => cons (f y) (Thunk.pure nil)) = LazyList.traverse f (fn✝ a)
⊢ Thunk.get
      {
        fn := fun x =>
          append (Thunk.get (Thunk.pure nil))
            { fn := fun x => LazyList.bind (Thunk.get { fn := fn✝ }) fun y => cons (f y) (Thunk.pure nil) } } =
    Thunk.get ((fun x => Thunk.pure (LazyList.traverse f (Thunk.get { fn := fn✝ }))) ())
[PROOFSTEP]
apply ih
[GOAL]
α : Type ?u.93639
inst✝ : DecidableEq α
x : α
⊢ Decidable (x ∈ nil)
[PROOFSTEP]
apply Decidable.isFalse
[GOAL]
case h
α : Type ?u.93639
inst✝ : DecidableEq α
x : α
⊢ ¬x ∈ nil
[PROOFSTEP]
simp [Membership.mem, LazyList.Mem]
[GOAL]
α : Type ?u.93639
inst✝ : DecidableEq α
x y : α
ys : Thunk (LazyList α)
h : x = y
⊢ Decidable (x ∈ cons y ys)
[PROOFSTEP]
apply Decidable.isTrue
[GOAL]
case h
α : Type ?u.93639
inst✝ : DecidableEq α
x y : α
ys : Thunk (LazyList α)
h : x = y
⊢ x ∈ cons y ys
[PROOFSTEP]
simp only [Membership.mem, LazyList.Mem]
[GOAL]
case h
α : Type ?u.93639
inst✝ : DecidableEq α
x y : α
ys : Thunk (LazyList α)
h : x = y
⊢ x = y ∨ LazyList.Mem x (Thunk.get ys)
[PROOFSTEP]
exact Or.inl h
[GOAL]
α : Type ?u.93639
inst✝ : DecidableEq α
x y : α
ys : Thunk (LazyList α)
h : ¬x = y
⊢ Decidable (x ∈ cons y ys)
[PROOFSTEP]
have := Mem.decidable x ys.get
[GOAL]
α : Type ?u.93639
inst✝ : DecidableEq α
x y : α
ys : Thunk (LazyList α)
h : ¬x = y
this : Decidable (x ∈ Thunk.get ys)
⊢ Decidable (x ∈ cons y ys)
[PROOFSTEP]
have : (x ∈ ys.get) ↔ (x ∈ cons y ys) := by simp [(· ∈ ·), LazyList.Mem, h]
[GOAL]
α : Type ?u.93639
inst✝ : DecidableEq α
x y : α
ys : Thunk (LazyList α)
h : ¬x = y
this : Decidable (x ∈ Thunk.get ys)
⊢ x ∈ Thunk.get ys ↔ x ∈ cons y ys
[PROOFSTEP]
simp [(· ∈ ·), LazyList.Mem, h]
[GOAL]
α : Type ?u.93639
inst✝ : DecidableEq α
x y : α
ys : Thunk (LazyList α)
h : ¬x = y
this✝ : Decidable (x ∈ Thunk.get ys)
this : x ∈ Thunk.get ys ↔ x ∈ cons y ys
⊢ Decidable (x ∈ cons y ys)
[PROOFSTEP]
exact decidable_of_decidable_of_iff this
[GOAL]
α : Type u_1
x y : α
ys : Thunk (LazyList α)
⊢ x ∈ cons y ys ↔ x = y ∨ x ∈ Thunk.get ys
[PROOFSTEP]
simp [Membership.mem, LazyList.Mem]
[GOAL]
α : Type u_1
p : α → Prop
a : α
l : Thunk (LazyList α)
⊢ (∀ (x : α), x ∈ cons a l → p x) ↔ p a ∧ ∀ (x : α), x ∈ Thunk.get l → p x
[PROOFSTEP]
simp only [Membership.mem, LazyList.Mem, or_imp, forall_and, forall_eq]


[GOAL]
R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A B : Matrix n n (DualNumber R)
⊢ Equiv.toFun
      { toFun := fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j)),
        invFun := fun d => ↑of fun i j => (fst d i j, snd d i j),
        left_inv :=
          (_ :
            ∀ (A : Matrix n n (DualNumber R)),
              (fun d => ↑of fun i j => (fst d i j, snd d i j))
                  ((fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j))) A) =
                A),
        right_inv :=
          (_ :
            ∀ (d : DualNumber (Matrix n n R)),
              (fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j)))
                  ((fun d => ↑of fun i j => (fst d i j, snd d i j)) d) =
                d) }
      (A * B) =
    Equiv.toFun
        { toFun := fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j)),
          invFun := fun d => ↑of fun i j => (fst d i j, snd d i j),
          left_inv :=
            (_ :
              ∀ (A : Matrix n n (DualNumber R)),
                (fun d => ↑of fun i j => (fst d i j, snd d i j))
                    ((fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j))) A) =
                  A),
          right_inv :=
            (_ :
              ∀ (d : DualNumber (Matrix n n R)),
                (fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j)))
                    ((fun d => ↑of fun i j => (fst d i j, snd d i j)) d) =
                  d) }
        A *
      Equiv.toFun
        { toFun := fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j)),
          invFun := fun d => ↑of fun i j => (fst d i j, snd d i j),
          left_inv :=
            (_ :
              ∀ (A : Matrix n n (DualNumber R)),
                (fun d => ↑of fun i j => (fst d i j, snd d i j))
                    ((fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j))) A) =
                  A),
          right_inv :=
            (_ :
              ∀ (d : DualNumber (Matrix n n R)),
                (fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j)))
                    ((fun d => ↑of fun i j => (fst d i j, snd d i j)) d) =
                  d) }
        B
[PROOFSTEP]
ext
[GOAL]
case h1.a.h
R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A B : Matrix n n (DualNumber R)
i✝ x✝ : n
⊢ fst
      (Equiv.toFun
        { toFun := fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j)),
          invFun := fun d => ↑of fun i j => (fst d i j, snd d i j),
          left_inv :=
            (_ :
              ∀ (A : Matrix n n (DualNumber R)),
                (fun d => ↑of fun i j => (fst d i j, snd d i j))
                    ((fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j))) A) =
                  A),
          right_inv :=
            (_ :
              ∀ (d : DualNumber (Matrix n n R)),
                (fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j)))
                    ((fun d => ↑of fun i j => (fst d i j, snd d i j)) d) =
                  d) }
        (A * B))
      i✝ x✝ =
    fst
      (Equiv.toFun
          { toFun := fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j)),
            invFun := fun d => ↑of fun i j => (fst d i j, snd d i j),
            left_inv :=
              (_ :
                ∀ (A : Matrix n n (DualNumber R)),
                  (fun d => ↑of fun i j => (fst d i j, snd d i j))
                      ((fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j))) A) =
                    A),
            right_inv :=
              (_ :
                ∀ (d : DualNumber (Matrix n n R)),
                  (fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j)))
                      ((fun d => ↑of fun i j => (fst d i j, snd d i j)) d) =
                    d) }
          A *
        Equiv.toFun
          { toFun := fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j)),
            invFun := fun d => ↑of fun i j => (fst d i j, snd d i j),
            left_inv :=
              (_ :
                ∀ (A : Matrix n n (DualNumber R)),
                  (fun d => ↑of fun i j => (fst d i j, snd d i j))
                      ((fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j))) A) =
                    A),
            right_inv :=
              (_ :
                ∀ (d : DualNumber (Matrix n n R)),
                  (fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j)))
                      ((fun d => ↑of fun i j => (fst d i j, snd d i j)) d) =
                    d) }
          B)
      i✝ x✝
[PROOFSTEP]
dsimp [mul_apply]
[GOAL]
case h1.a.h
R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A B : Matrix n n (DualNumber R)
i✝ x✝ : n
⊢ fst (Finset.sum Finset.univ fun j => A i✝ j * B j x✝) = Finset.sum Finset.univ fun j => fst (A i✝ j) * fst (B j x✝)
[PROOFSTEP]
simp_rw [fst_sum]
[GOAL]
case h1.a.h
R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A B : Matrix n n (DualNumber R)
i✝ x✝ : n
⊢ (Finset.sum Finset.univ fun i => fst (A i✝ i * B i x✝)) = Finset.sum Finset.univ fun j => fst (A i✝ j) * fst (B j x✝)
[PROOFSTEP]
rfl
[GOAL]
case h2.a.h
R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A B : Matrix n n (DualNumber R)
i✝ x✝ : n
⊢ snd
      (Equiv.toFun
        { toFun := fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j)),
          invFun := fun d => ↑of fun i j => (fst d i j, snd d i j),
          left_inv :=
            (_ :
              ∀ (A : Matrix n n (DualNumber R)),
                (fun d => ↑of fun i j => (fst d i j, snd d i j))
                    ((fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j))) A) =
                  A),
          right_inv :=
            (_ :
              ∀ (d : DualNumber (Matrix n n R)),
                (fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j)))
                    ((fun d => ↑of fun i j => (fst d i j, snd d i j)) d) =
                  d) }
        (A * B))
      i✝ x✝ =
    snd
      (Equiv.toFun
          { toFun := fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j)),
            invFun := fun d => ↑of fun i j => (fst d i j, snd d i j),
            left_inv :=
              (_ :
                ∀ (A : Matrix n n (DualNumber R)),
                  (fun d => ↑of fun i j => (fst d i j, snd d i j))
                      ((fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j))) A) =
                    A),
            right_inv :=
              (_ :
                ∀ (d : DualNumber (Matrix n n R)),
                  (fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j)))
                      ((fun d => ↑of fun i j => (fst d i j, snd d i j)) d) =
                    d) }
          A *
        Equiv.toFun
          { toFun := fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j)),
            invFun := fun d => ↑of fun i j => (fst d i j, snd d i j),
            left_inv :=
              (_ :
                ∀ (A : Matrix n n (DualNumber R)),
                  (fun d => ↑of fun i j => (fst d i j, snd d i j))
                      ((fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j))) A) =
                    A),
            right_inv :=
              (_ :
                ∀ (d : DualNumber (Matrix n n R)),
                  (fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j)))
                      ((fun d => ↑of fun i j => (fst d i j, snd d i j)) d) =
                    d) }
          B)
      i✝ x✝
[PROOFSTEP]
simp_rw [snd_mul, smul_eq_mul, op_smul_eq_mul]
[GOAL]
case h2.a.h
R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A B : Matrix n n (DualNumber R)
i✝ x✝ : n
⊢ snd (↑of fun i j => fst ((A * B) i j), ↑of fun i j => snd ((A * B) i j)) i✝ x✝ =
    (fst (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j)) *
          snd (↑of fun i j => fst (B i j), ↑of fun i j => snd (B i j)) +
        snd (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j)) *
          fst (↑of fun i j => fst (B i j), ↑of fun i j => snd (B i j)))
      i✝ x✝
[PROOFSTEP]
simp [mul_apply, snd_sum, snd_mul]
[GOAL]
case h2.a.h
R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A B : Matrix n n (DualNumber R)
i✝ x✝ : n
⊢ (Finset.sum Finset.univ fun x => fst (A i✝ x) * snd (B x x✝) + snd (A i✝ x) * fst (B x x✝)) =
    (Finset.sum Finset.univ fun x => fst (A i✝ x) * snd (B x x✝)) +
      Finset.sum Finset.univ fun x => snd (A i✝ x) * fst (B x x✝)
[PROOFSTEP]
rw [← Finset.sum_add_distrib]
[GOAL]
R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
r : R
⊢ Equiv.toFun
      { toFun := fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j)),
        invFun := fun d => ↑of fun i j => (fst d i j, snd d i j),
        left_inv :=
          (_ :
            ∀ (A : Matrix n n (DualNumber R)),
              (fun d => ↑of fun i j => (fst d i j, snd d i j))
                  ((fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j))) A) =
                A),
        right_inv :=
          (_ :
            ∀ (d : DualNumber (Matrix n n R)),
              (fun A => (↑of fun i j => fst (A i j), ↑of fun i j => snd (A i j)))
                  ((fun d => ↑of fun i j => (fst d i j, snd d i j)) d) =
                d) }
      (↑(algebraMap R (Matrix n n (DualNumber R))) r) =
    ↑(algebraMap R (DualNumber (Matrix n n R))) r
[PROOFSTEP]
simp_rw [algebraMap_eq_inl', algebraMap_eq_diagonal, Pi.algebraMap_def, Algebra.id.map_eq_self, algebraMap_eq_inl, ←
  diagonal_map (inl_zero R), map_apply, fst_inl, snd_inl]
[GOAL]
R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
r : R
⊢ (↑of fun i j => diagonal (fun m => r) i j, ↑of fun i j => 0) = inl (diagonal fun m => r)
[PROOFSTEP]
rfl


[GOAL]
m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring α
A : Matrix n n α
B : Matrix n m α
inst✝ : Invertible A
⊢ ⅟A * (A * B) = B
[PROOFSTEP]
rw [← Matrix.mul_assoc, invOf_mul_self, Matrix.one_mul]
[GOAL]
m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring α
A : Matrix n n α
B : Matrix n m α
inst✝ : Invertible A
⊢ A * (⅟A * B) = B
[PROOFSTEP]
rw [← Matrix.mul_assoc, mul_invOf_self, Matrix.one_mul]
[GOAL]
m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring α
A : Matrix m n α
B : Matrix n n α
inst✝ : Invertible B
⊢ A * ⅟B * B = A
[PROOFSTEP]
rw [Matrix.mul_assoc, invOf_mul_self, Matrix.mul_one]
[GOAL]
m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring α
A : Matrix m n α
B : Matrix n n α
inst✝ : Invertible B
⊢ A * B * ⅟B = A
[PROOFSTEP]
rw [Matrix.mul_assoc, mul_invOf_self, Matrix.mul_one]