[GOAL]
α : Type u_3
n : ℕ
β : Type u_2
σ₁ : Type
γ : Type u_1
σ₂ : Type
xs : Vector α n
f₁ : β → σ₁ → σ₁ × γ
f₂ : α → σ₂ → σ₂ × β
s₂ : σ₂
s₁ : σ₁
⊢ mapAccumr f₁ (mapAccumr f₂ xs s₂).snd s₁ =
    let m :=
      mapAccumr
        (fun x s =>
          let r₂ := f₂ x s.snd;
          let r₁ := f₁ r₂.snd s.fst;
          ((r₁.fst, r₂.fst), r₁.snd))
        xs (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
induction xs using Vector.revInductionOn generalizing s₁ s₂
[GOAL]
case nil
α : Type u_3
n : ℕ
β : Type u_2
σ₁ : Type
γ : Type u_1
σ₂ : Type
xs : Vector α n
f₁ : β → σ₁ → σ₁ × γ
f₂ : α → σ₂ → σ₂ × β
s₂ : σ₂
s₁ : σ₁
⊢ mapAccumr f₁ (mapAccumr f₂ nil s₂).snd s₁ =
    let m :=
      mapAccumr
        (fun x s =>
          let r₂ := f₂ x s.snd;
          let r₁ := f₁ r₂.snd s.fst;
          ((r₁.fst, r₂.fst), r₁.snd))
        nil (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
simp_all
[GOAL]
case snoc
α : Type u_3
n : ℕ
β : Type u_2
σ₁ : Type
γ : Type u_1
σ₂ : Type
xs : Vector α n
f₁ : β → σ₁ → σ₁ × γ
f₂ : α → σ₂ → σ₂ × β
n✝ : ℕ
xs✝ : Vector α n✝
x✝ : α
a✝ :
  ∀ {s₂ : σ₂} {s₁ : σ₁},
    mapAccumr f₁ (mapAccumr f₂ xs✝ s₂).snd s₁ =
      let m :=
        mapAccumr
          (fun x s =>
            let r₂ := f₂ x s.snd;
            let r₁ := f₁ r₂.snd s.fst;
            ((r₁.fst, r₂.fst), r₁.snd))
          xs✝ (s₁, s₂);
      (m.fst.fst, m.snd)
s₂ : σ₂
s₁ : σ₁
⊢ mapAccumr f₁ (mapAccumr f₂ (snoc xs✝ x✝) s₂).snd s₁ =
    let m :=
      mapAccumr
        (fun x s =>
          let r₂ := f₂ x s.snd;
          let r₁ := f₁ r₂.snd s.fst;
          ((r₁.fst, r₂.fst), r₁.snd))
        (snoc xs✝ x✝) (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
simp_all
[GOAL]
α : Type u_3
n : ℕ
β : Type u_2
σ₁ : Type
γ : Type u_1
σ₂ : Type ?u.3222
xs : Vector α n
f₁ : β → σ₁ → σ₁ × γ
f₂✝ : α → σ₂ → σ₂ × β
s : σ₁
f₂ : α → β
⊢ mapAccumr f₁ (map f₂ xs) s = mapAccumr (fun x s => f₁ (f₂ x) s) xs s
[PROOFSTEP]
induction xs using Vector.revInductionOn generalizing s
[GOAL]
case nil
α : Type u_3
n : ℕ
β : Type u_2
σ₁ : Type
γ : Type u_1
σ₂ : Type ?u.3222
xs : Vector α n
f₁ : β → σ₁ → σ₁ × γ
f₂✝ : α → σ₂ → σ₂ × β
f₂ : α → β
s : σ₁
⊢ mapAccumr f₁ (map f₂ nil) s = mapAccumr (fun x s => f₁ (f₂ x) s) nil s
[PROOFSTEP]
simp_all
[GOAL]
case snoc
α : Type u_3
n : ℕ
β : Type u_2
σ₁ : Type
γ : Type u_1
σ₂ : Type ?u.3222
xs : Vector α n
f₁ : β → σ₁ → σ₁ × γ
f₂✝ : α → σ₂ → σ₂ × β
f₂ : α → β
n✝ : ℕ
xs✝ : Vector α n✝
x✝ : α
a✝ : ∀ {s : σ₁}, mapAccumr f₁ (map f₂ xs✝) s = mapAccumr (fun x s => f₁ (f₂ x) s) xs✝ s
s : σ₁
⊢ mapAccumr f₁ (map f₂ (snoc xs✝ x✝)) s = mapAccumr (fun x s => f₁ (f₂ x) s) (snoc xs✝ x✝) s
[PROOFSTEP]
simp_all
[GOAL]
α : Type u_3
n : ℕ
β : Type u_2
σ₁ : Type ?u.4482
γ : Type u_1
σ₂ : Type
xs : Vector α n
f₁✝ : β → σ₁ → σ₁ × γ
f₂ : α → σ₂ → σ₂ × β
s : σ₂
f₁ : β → γ
⊢ map f₁ (mapAccumr f₂ xs s).snd =
    (mapAccumr
        (fun x s =>
          let r := f₂ x s;
          (r.fst, f₁ r.snd))
        xs s).snd
[PROOFSTEP]
induction xs using Vector.revInductionOn generalizing s
[GOAL]
case nil
α : Type u_3
n : ℕ
β : Type u_2
σ₁ : Type ?u.4482
γ : Type u_1
σ₂ : Type
xs : Vector α n
f₁✝ : β → σ₁ → σ₁ × γ
f₂ : α → σ₂ → σ₂ × β
f₁ : β → γ
s : σ₂
⊢ map f₁ (mapAccumr f₂ nil s).snd =
    (mapAccumr
        (fun x s =>
          let r := f₂ x s;
          (r.fst, f₁ r.snd))
        nil s).snd
[PROOFSTEP]
simp_all
[GOAL]
case snoc
α : Type u_3
n : ℕ
β : Type u_2
σ₁ : Type ?u.4482
γ : Type u_1
σ₂ : Type
xs : Vector α n
f₁✝ : β → σ₁ → σ₁ × γ
f₂ : α → σ₂ → σ₂ × β
f₁ : β → γ
n✝ : ℕ
xs✝ : Vector α n✝
x✝ : α
a✝ :
  ∀ {s : σ₂},
    map f₁ (mapAccumr f₂ xs✝ s).snd =
      (mapAccumr
          (fun x s =>
            let r := f₂ x s;
            (r.fst, f₁ r.snd))
          xs✝ s).snd
s : σ₂
⊢ map f₁ (mapAccumr f₂ (snoc xs✝ x✝) s).snd =
    (mapAccumr
        (fun x s =>
          let r := f₂ x s;
          (r.fst, f₁ r.snd))
        (snoc xs✝ x✝) s).snd
[PROOFSTEP]
simp_all
[GOAL]
α : Type u_3
n : ℕ
β : Type u_2
σ₁ : Type ?u.6822
γ : Type u_1
σ₂ : Type ?u.6830
xs : Vector α n
f₁✝ : β → σ₁ → σ₁ × γ
f₂✝ : α → σ₂ → σ₂ × β
f₁ : β → γ
f₂ : α → β
⊢ map f₁ (map f₂ xs) = map (fun x => f₁ (f₂ x)) xs
[PROOFSTEP]
induction xs using Vector.inductionOn
[GOAL]
case h_nil
α : Type u_3
n : ℕ
β : Type u_2
σ₁ : Type ?u.6822
γ : Type u_1
σ₂ : Type ?u.6830
xs : Vector α n
f₁✝ : β → σ₁ → σ₁ × γ
f₂✝ : α → σ₂ → σ₂ × β
f₁ : β → γ
f₂ : α → β
⊢ map f₁ (map f₂ nil) = map (fun x => f₁ (f₂ x)) nil
[PROOFSTEP]
simp_all
[GOAL]
case h_cons
α : Type u_3
n : ℕ
β : Type u_2
σ₁ : Type ?u.6822
γ : Type u_1
σ₂ : Type ?u.6830
xs : Vector α n
f₁✝ : β → σ₁ → σ₁ × γ
f₂✝ : α → σ₂ → σ₂ × β
f₁ : β → γ
f₂ : α → β
n✝ : ℕ
x✝ : α
w✝ : Vector α n✝
a✝ : map f₁ (map f₂ w✝) = map (fun x => f₁ (f₂ x)) w✝
⊢ map f₁ (map f₂ (x✝ ::ᵥ w✝)) = map (fun x => f₁ (f₂ x)) (x✝ ::ᵥ w✝)
[PROOFSTEP]
simp_all
[GOAL]
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
γ σ₁ ζ σ₂ : Type
s₂ : σ₂
s₁ : σ₁
f₁ : γ → β → σ₁ → σ₁ × ζ
f₂ : α → σ₂ → σ₂ × γ
⊢ mapAccumr₂ f₁ (mapAccumr f₂ xs s₂).snd ys s₁ =
    let m :=
      mapAccumr₂
        (fun x y s =>
          let r₂ := f₂ x s.snd;
          let r₁ := f₁ r₂.snd y s.fst;
          ((r₁.fst, r₂.fst), r₁.snd))
        xs ys (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂
[GOAL]
case nil
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
γ σ₁ ζ σ₂ : Type
f₁ : γ → β → σ₁ → σ₁ × ζ
f₂ : α → σ₂ → σ₂ × γ
s₂ : σ₂
s₁ : σ₁
⊢ mapAccumr₂ f₁ (mapAccumr f₂ nil s₂).snd nil s₁ =
    let m :=
      mapAccumr₂
        (fun x y s =>
          let r₂ := f₂ x s.snd;
          let r₁ := f₁ r₂.snd y s.fst;
          ((r₁.fst, r₂.fst), r₁.snd))
        nil nil (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
simp_all
[GOAL]
case snoc
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
γ σ₁ ζ σ₂ : Type
f₁ : γ → β → σ₁ → σ₁ × ζ
f₂ : α → σ₂ → σ₂ × γ
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ :
  ∀ {s₂ : σ₂} {s₁ : σ₁},
    mapAccumr₂ f₁ (mapAccumr f₂ xs✝ s₂).snd ys✝ s₁ =
      let m :=
        mapAccumr₂
          (fun x y s =>
            let r₂ := f₂ x s.snd;
            let r₁ := f₁ r₂.snd y s.fst;
            ((r₁.fst, r₂.fst), r₁.snd))
          xs✝ ys✝ (s₁, s₂);
      (m.fst.fst, m.snd)
s₂ : σ₂
s₁ : σ₁
⊢ mapAccumr₂ f₁ (mapAccumr f₂ (snoc xs✝ x✝) s₂).snd (snoc ys✝ y✝) s₁ =
    let m :=
      mapAccumr₂
        (fun x y s =>
          let r₂ := f₂ x s.snd;
          let r₁ := f₁ r₂.snd y s.fst;
          ((r₁.fst, r₂.fst), r₁.snd))
        (snoc xs✝ x✝) (snoc ys✝ y✝) (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
simp_all
[GOAL]
α : Type u_4
n : ℕ
β : Type u_3
xs : Vector α n
ys : Vector β n
γ : Type u_1
ζ : Type u_2
f₁ : γ → β → ζ
f₂ : α → γ
⊢ map₂ f₁ (map f₂ xs) ys = map₂ (fun x y => f₁ (f₂ x) y) xs ys
[PROOFSTEP]
induction xs, ys using Vector.revInductionOn₂
[GOAL]
case nil
α : Type u_4
n : ℕ
β : Type u_3
xs : Vector α n
ys : Vector β n
γ : Type u_1
ζ : Type u_2
f₁ : γ → β → ζ
f₂ : α → γ
⊢ map₂ f₁ (map f₂ nil) nil = map₂ (fun x y => f₁ (f₂ x) y) nil nil
[PROOFSTEP]
simp_all
[GOAL]
case snoc
α : Type u_4
n : ℕ
β : Type u_3
xs : Vector α n
ys : Vector β n
γ : Type u_1
ζ : Type u_2
f₁ : γ → β → ζ
f₂ : α → γ
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ : map₂ f₁ (map f₂ xs✝) ys✝ = map₂ (fun x y => f₁ (f₂ x) y) xs✝ ys✝
⊢ map₂ f₁ (map f₂ (snoc xs✝ x✝)) (snoc ys✝ y✝) = map₂ (fun x y => f₁ (f₂ x) y) (snoc xs✝ x✝) (snoc ys✝ y✝)
[PROOFSTEP]
simp_all
[GOAL]
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
γ σ₁ ζ σ₂ : Type
s₂ : σ₂
s₁ : σ₁
f₁ : α → γ → σ₁ → σ₁ × ζ
f₂ : β → σ₂ → σ₂ × γ
⊢ mapAccumr₂ f₁ xs (mapAccumr f₂ ys s₂).snd s₁ =
    let m :=
      mapAccumr₂
        (fun x y s =>
          let r₂ := f₂ y s.snd;
          let r₁ := f₁ x r₂.snd s.fst;
          ((r₁.fst, r₂.fst), r₁.snd))
        xs ys (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂
[GOAL]
case nil
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
γ σ₁ ζ σ₂ : Type
f₁ : α → γ → σ₁ → σ₁ × ζ
f₂ : β → σ₂ → σ₂ × γ
s₂ : σ₂
s₁ : σ₁
⊢ mapAccumr₂ f₁ nil (mapAccumr f₂ nil s₂).snd s₁ =
    let m :=
      mapAccumr₂
        (fun x y s =>
          let r₂ := f₂ y s.snd;
          let r₁ := f₁ x r₂.snd s.fst;
          ((r₁.fst, r₂.fst), r₁.snd))
        nil nil (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
simp_all
[GOAL]
case snoc
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
γ σ₁ ζ σ₂ : Type
f₁ : α → γ → σ₁ → σ₁ × ζ
f₂ : β → σ₂ → σ₂ × γ
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ :
  ∀ {s₂ : σ₂} {s₁ : σ₁},
    mapAccumr₂ f₁ xs✝ (mapAccumr f₂ ys✝ s₂).snd s₁ =
      let m :=
        mapAccumr₂
          (fun x y s =>
            let r₂ := f₂ y s.snd;
            let r₁ := f₁ x r₂.snd s.fst;
            ((r₁.fst, r₂.fst), r₁.snd))
          xs✝ ys✝ (s₁, s₂);
      (m.fst.fst, m.snd)
s₂ : σ₂
s₁ : σ₁
⊢ mapAccumr₂ f₁ (snoc xs✝ x✝) (mapAccumr f₂ (snoc ys✝ y✝) s₂).snd s₁ =
    let m :=
      mapAccumr₂
        (fun x y s =>
          let r₂ := f₂ y s.snd;
          let r₁ := f₁ x r₂.snd s.fst;
          ((r₁.fst, r₂.fst), r₁.snd))
        (snoc xs✝ x✝) (snoc ys✝ y✝) (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
simp_all
[GOAL]
α : Type u_3
n : ℕ
β : Type u_4
xs : Vector α n
ys : Vector β n
γ : Type u_1
ζ : Type u_2
f₁ : α → γ → ζ
f₂ : β → γ
⊢ map₂ f₁ xs (map f₂ ys) = map₂ (fun x y => f₁ x (f₂ y)) xs ys
[PROOFSTEP]
induction xs, ys using Vector.revInductionOn₂
[GOAL]
case nil
α : Type u_3
n : ℕ
β : Type u_4
xs : Vector α n
ys : Vector β n
γ : Type u_1
ζ : Type u_2
f₁ : α → γ → ζ
f₂ : β → γ
⊢ map₂ f₁ nil (map f₂ nil) = map₂ (fun x y => f₁ x (f₂ y)) nil nil
[PROOFSTEP]
simp_all
[GOAL]
case snoc
α : Type u_3
n : ℕ
β : Type u_4
xs : Vector α n
ys : Vector β n
γ : Type u_1
ζ : Type u_2
f₁ : α → γ → ζ
f₂ : β → γ
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ : map₂ f₁ xs✝ (map f₂ ys✝) = map₂ (fun x y => f₁ x (f₂ y)) xs✝ ys✝
⊢ map₂ f₁ (snoc xs✝ x✝) (map f₂ (snoc ys✝ y✝)) = map₂ (fun x y => f₁ x (f₂ y)) (snoc xs✝ x✝) (snoc ys✝ y✝)
[PROOFSTEP]
simp_all
[GOAL]
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
γ σ₁ ζ σ₂ : Type
s₂ : σ₂
s₁ : σ₁
f₁ : γ → σ₁ → σ₁ × ζ
f₂ : α → β → σ₂ → σ₂ × γ
⊢ mapAccumr f₁ (mapAccumr₂ f₂ xs ys s₂).snd s₁ =
    let m :=
      mapAccumr₂
        (fun x y s =>
          let r₂ := f₂ x y s.snd;
          let r₁ := f₁ r₂.snd s.fst;
          ((r₁.fst, r₂.fst), r₁.snd))
        xs ys (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂
[GOAL]
case nil
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
γ σ₁ ζ σ₂ : Type
f₁ : γ → σ₁ → σ₁ × ζ
f₂ : α → β → σ₂ → σ₂ × γ
s₂ : σ₂
s₁ : σ₁
⊢ mapAccumr f₁ (mapAccumr₂ f₂ nil nil s₂).snd s₁ =
    let m :=
      mapAccumr₂
        (fun x y s =>
          let r₂ := f₂ x y s.snd;
          let r₁ := f₁ r₂.snd s.fst;
          ((r₁.fst, r₂.fst), r₁.snd))
        nil nil (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
simp_all
[GOAL]
case snoc
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
γ σ₁ ζ σ₂ : Type
f₁ : γ → σ₁ → σ₁ × ζ
f₂ : α → β → σ₂ → σ₂ × γ
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ :
  ∀ {s₂ : σ₂} {s₁ : σ₁},
    mapAccumr f₁ (mapAccumr₂ f₂ xs✝ ys✝ s₂).snd s₁ =
      let m :=
        mapAccumr₂
          (fun x y s =>
            let r₂ := f₂ x y s.snd;
            let r₁ := f₁ r₂.snd s.fst;
            ((r₁.fst, r₂.fst), r₁.snd))
          xs✝ ys✝ (s₁, s₂);
      (m.fst.fst, m.snd)
s₂ : σ₂
s₁ : σ₁
⊢ mapAccumr f₁ (mapAccumr₂ f₂ (snoc xs✝ x✝) (snoc ys✝ y✝) s₂).snd s₁ =
    let m :=
      mapAccumr₂
        (fun x y s =>
          let r₂ := f₂ x y s.snd;
          let r₁ := f₁ r₂.snd s.fst;
          ((r₁.fst, r₂.fst), r₁.snd))
        (snoc xs✝ x✝) (snoc ys✝ y✝) (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
simp_all
[GOAL]
α : Type u_3
n : ℕ
β : Type u_4
xs : Vector α n
ys : Vector β n
γ : Type u_1
ζ : Type u_2
f₁ : γ → ζ
f₂ : α → β → γ
⊢ map f₁ (map₂ f₂ xs ys) = map₂ (fun x y => f₁ (f₂ x y)) xs ys
[PROOFSTEP]
induction xs, ys using Vector.revInductionOn₂
[GOAL]
case nil
α : Type u_3
n : ℕ
β : Type u_4
xs : Vector α n
ys : Vector β n
γ : Type u_1
ζ : Type u_2
f₁ : γ → ζ
f₂ : α → β → γ
⊢ map f₁ (map₂ f₂ nil nil) = map₂ (fun x y => f₁ (f₂ x y)) nil nil
[PROOFSTEP]
simp_all
[GOAL]
case snoc
α : Type u_3
n : ℕ
β : Type u_4
xs : Vector α n
ys : Vector β n
γ : Type u_1
ζ : Type u_2
f₁ : γ → ζ
f₂ : α → β → γ
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ : map f₁ (map₂ f₂ xs✝ ys✝) = map₂ (fun x y => f₁ (f₂ x y)) xs✝ ys✝
⊢ map f₁ (map₂ f₂ (snoc xs✝ x✝) (snoc ys✝ y✝)) = map₂ (fun x y => f₁ (f₂ x y)) (snoc xs✝ x✝) (snoc ys✝ y✝)
[PROOFSTEP]
simp_all
[GOAL]
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
γ σ₁ φ σ₂ : Type
s₂ : σ₂
s₁ : σ₁
f₁ : γ → α → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
⊢ mapAccumr₂ f₁ (mapAccumr₂ f₂ xs ys s₂).snd xs s₁ =
    let m :=
      mapAccumr₂
        (fun x y x_1 =>
          match x_1 with
          | (s₁, s₂) =>
            let r₂ := f₂ x y s₂;
            let r₁ := f₁ r₂.snd x s₁;
            ((r₁.fst, r₂.fst), r₁.snd))
        xs ys (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂
[GOAL]
case nil
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
γ σ₁ φ σ₂ : Type
f₁ : γ → α → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
s₂ : σ₂
s₁ : σ₁
⊢ mapAccumr₂ f₁ (mapAccumr₂ f₂ nil nil s₂).snd nil s₁ =
    let m :=
      mapAccumr₂
        (fun x y x_1 =>
          match x_1 with
          | (s₁, s₂) =>
            let r₂ := f₂ x y s₂;
            let r₁ := f₁ r₂.snd x s₁;
            ((r₁.fst, r₂.fst), r₁.snd))
        nil nil (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
simp_all
[GOAL]
case snoc
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
γ σ₁ φ σ₂ : Type
f₁ : γ → α → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ :
  ∀ {s₂ : σ₂} {s₁ : σ₁},
    mapAccumr₂ f₁ (mapAccumr₂ f₂ xs✝ ys✝ s₂).snd xs✝ s₁ =
      let m :=
        mapAccumr₂
          (fun x y x_1 =>
            match x_1 with
            | (s₁, s₂) =>
              let r₂ := f₂ x y s₂;
              let r₁ := f₁ r₂.snd x s₁;
              ((r₁.fst, r₂.fst), r₁.snd))
          xs✝ ys✝ (s₁, s₂);
      (m.fst.fst, m.snd)
s₂ : σ₂
s₁ : σ₁
⊢ mapAccumr₂ f₁ (mapAccumr₂ f₂ (snoc xs✝ x✝) (snoc ys✝ y✝) s₂).snd (snoc xs✝ x✝) s₁ =
    let m :=
      mapAccumr₂
        (fun x y x_1 =>
          match x_1 with
          | (s₁, s₂) =>
            let r₂ := f₂ x y s₂;
            let r₁ := f₁ r₂.snd x s₁;
            ((r₁.fst, r₂.fst), r₁.snd))
        (snoc xs✝ x✝) (snoc ys✝ y✝) (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
simp_all
[GOAL]
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
γ σ₁ φ σ₂ : Type
s₂ : σ₂
s₁ : σ₁
f₁ : γ → β → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
⊢ mapAccumr₂ f₁ (mapAccumr₂ f₂ xs ys s₂).snd ys s₁ =
    let m :=
      mapAccumr₂
        (fun x y x_1 =>
          match x_1 with
          | (s₁, s₂) =>
            let r₂ := f₂ x y s₂;
            let r₁ := f₁ r₂.snd y s₁;
            ((r₁.fst, r₂.fst), r₁.snd))
        xs ys (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂
[GOAL]
case nil
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
γ σ₁ φ σ₂ : Type
f₁ : γ → β → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
s₂ : σ₂
s₁ : σ₁
⊢ mapAccumr₂ f₁ (mapAccumr₂ f₂ nil nil s₂).snd nil s₁ =
    let m :=
      mapAccumr₂
        (fun x y x_1 =>
          match x_1 with
          | (s₁, s₂) =>
            let r₂ := f₂ x y s₂;
            let r₁ := f₁ r₂.snd y s₁;
            ((r₁.fst, r₂.fst), r₁.snd))
        nil nil (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
simp_all
[GOAL]
case snoc
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
γ σ₁ φ σ₂ : Type
f₁ : γ → β → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ :
  ∀ {s₂ : σ₂} {s₁ : σ₁},
    mapAccumr₂ f₁ (mapAccumr₂ f₂ xs✝ ys✝ s₂).snd ys✝ s₁ =
      let m :=
        mapAccumr₂
          (fun x y x_1 =>
            match x_1 with
            | (s₁, s₂) =>
              let r₂ := f₂ x y s₂;
              let r₁ := f₁ r₂.snd y s₁;
              ((r₁.fst, r₂.fst), r₁.snd))
          xs✝ ys✝ (s₁, s₂);
      (m.fst.fst, m.snd)
s₂ : σ₂
s₁ : σ₁
⊢ mapAccumr₂ f₁ (mapAccumr₂ f₂ (snoc xs✝ x✝) (snoc ys✝ y✝) s₂).snd (snoc ys✝ y✝) s₁ =
    let m :=
      mapAccumr₂
        (fun x y x_1 =>
          match x_1 with
          | (s₁, s₂) =>
            let r₂ := f₂ x y s₂;
            let r₁ := f₁ r₂.snd y s₁;
            ((r₁.fst, r₂.fst), r₁.snd))
        (snoc xs✝ x✝) (snoc ys✝ y✝) (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
simp_all
[GOAL]
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
γ σ₁ φ σ₂ : Type
s₂ : σ₂
s₁ : σ₁
f₁ : α → γ → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
⊢ mapAccumr₂ f₁ xs (mapAccumr₂ f₂ xs ys s₂).snd s₁ =
    let m :=
      mapAccumr₂
        (fun x y x_1 =>
          match x_1 with
          | (s₁, s₂) =>
            let r₂ := f₂ x y s₂;
            let r₁ := f₁ x r₂.snd s₁;
            ((r₁.fst, r₂.fst), r₁.snd))
        xs ys (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂
[GOAL]
case nil
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
γ σ₁ φ σ₂ : Type
f₁ : α → γ → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
s₂ : σ₂
s₁ : σ₁
⊢ mapAccumr₂ f₁ nil (mapAccumr₂ f₂ nil nil s₂).snd s₁ =
    let m :=
      mapAccumr₂
        (fun x y x_1 =>
          match x_1 with
          | (s₁, s₂) =>
            let r₂ := f₂ x y s₂;
            let r₁ := f₁ x r₂.snd s₁;
            ((r₁.fst, r₂.fst), r₁.snd))
        nil nil (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
simp_all
[GOAL]
case snoc
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
γ σ₁ φ σ₂ : Type
f₁ : α → γ → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ :
  ∀ {s₂ : σ₂} {s₁ : σ₁},
    mapAccumr₂ f₁ xs✝ (mapAccumr₂ f₂ xs✝ ys✝ s₂).snd s₁ =
      let m :=
        mapAccumr₂
          (fun x y x_1 =>
            match x_1 with
            | (s₁, s₂) =>
              let r₂ := f₂ x y s₂;
              let r₁ := f₁ x r₂.snd s₁;
              ((r₁.fst, r₂.fst), r₁.snd))
          xs✝ ys✝ (s₁, s₂);
      (m.fst.fst, m.snd)
s₂ : σ₂
s₁ : σ₁
⊢ mapAccumr₂ f₁ (snoc xs✝ x✝) (mapAccumr₂ f₂ (snoc xs✝ x✝) (snoc ys✝ y✝) s₂).snd s₁ =
    let m :=
      mapAccumr₂
        (fun x y x_1 =>
          match x_1 with
          | (s₁, s₂) =>
            let r₂ := f₂ x y s₂;
            let r₁ := f₁ x r₂.snd s₁;
            ((r₁.fst, r₂.fst), r₁.snd))
        (snoc xs✝ x✝) (snoc ys✝ y✝) (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
simp_all
[GOAL]
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
γ σ₁ φ σ₂ : Type
s₂ : σ₂
s₁ : σ₁
f₁ : β → γ → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
⊢ mapAccumr₂ f₁ ys (mapAccumr₂ f₂ xs ys s₂).snd s₁ =
    let m :=
      mapAccumr₂
        (fun x y x_1 =>
          match x_1 with
          | (s₁, s₂) =>
            let r₂ := f₂ x y s₂;
            let r₁ := f₁ y r₂.snd s₁;
            ((r₁.fst, r₂.fst), r₁.snd))
        xs ys (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂
[GOAL]
case nil
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
γ σ₁ φ σ₂ : Type
f₁ : β → γ → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
s₂ : σ₂
s₁ : σ₁
⊢ mapAccumr₂ f₁ nil (mapAccumr₂ f₂ nil nil s₂).snd s₁ =
    let m :=
      mapAccumr₂
        (fun x y x_1 =>
          match x_1 with
          | (s₁, s₂) =>
            let r₂ := f₂ x y s₂;
            let r₁ := f₁ y r₂.snd s₁;
            ((r₁.fst, r₂.fst), r₁.snd))
        nil nil (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
simp_all
[GOAL]
case snoc
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
γ σ₁ φ σ₂ : Type
f₁ : β → γ → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ :
  ∀ {s₂ : σ₂} {s₁ : σ₁},
    mapAccumr₂ f₁ ys✝ (mapAccumr₂ f₂ xs✝ ys✝ s₂).snd s₁ =
      let m :=
        mapAccumr₂
          (fun x y x_1 =>
            match x_1 with
            | (s₁, s₂) =>
              let r₂ := f₂ x y s₂;
              let r₁ := f₁ y r₂.snd s₁;
              ((r₁.fst, r₂.fst), r₁.snd))
          xs✝ ys✝ (s₁, s₂);
      (m.fst.fst, m.snd)
s₂ : σ₂
s₁ : σ₁
⊢ mapAccumr₂ f₁ (snoc ys✝ y✝) (mapAccumr₂ f₂ (snoc xs✝ x✝) (snoc ys✝ y✝) s₂).snd s₁ =
    let m :=
      mapAccumr₂
        (fun x y x_1 =>
          match x_1 with
          | (s₁, s₂) =>
            let r₂ := f₂ x y s₂;
            let r₁ := f₁ y r₂.snd s₁;
            ((r₁.fst, r₂.fst), r₁.snd))
        (snoc xs✝ x✝) (snoc ys✝ y✝) (s₁, s₂);
    (m.fst.fst, m.snd)
[PROOFSTEP]
simp_all
[GOAL]
α : Type u_2
n : ℕ
xs : Vector α n
σ₁ : Type
β : Type u_1
σ₂ : Type
f₁ : α → σ₁ → σ₁ × β
f₂ : α → σ₂ → σ₂ × β
s₁ : σ₁
s₂ : σ₂
R : σ₁ → σ₂ → Prop
h₀ : R s₁ s₂
hR : ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).fst (f₂ a q).fst ∧ (f₁ a s).snd = (f₂ a q).snd
⊢ R (mapAccumr f₁ xs s₁).fst (mapAccumr f₂ xs s₂).fst ∧ (mapAccumr f₁ xs s₁).snd = (mapAccumr f₂ xs s₂).snd
[PROOFSTEP]
induction xs using Vector.revInductionOn generalizing s₁ s₂
[GOAL]
case nil
α : Type u_2
n : ℕ
xs : Vector α n
σ₁ : Type
β : Type u_1
σ₂ : Type
f₁ : α → σ₁ → σ₁ × β
f₂ : α → σ₂ → σ₂ × β
R : σ₁ → σ₂ → Prop
hR : ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).fst (f₂ a q).fst ∧ (f₁ a s).snd = (f₂ a q).snd
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
⊢ R (mapAccumr f₁ nil s₁).fst (mapAccumr f₂ nil s₂).fst ∧ (mapAccumr f₁ nil s₁).snd = (mapAccumr f₂ nil s₂).snd
case snoc
α : Type u_2
n : ℕ
xs : Vector α n
σ₁ : Type
β : Type u_1
σ₂ : Type
f₁ : α → σ₁ → σ₁ × β
f₂ : α → σ₂ → σ₂ × β
R : σ₁ → σ₂ → Prop
hR : ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).fst (f₂ a q).fst ∧ (f₁ a s).snd = (f₂ a q).snd
n✝ : ℕ
xs✝ : Vector α n✝
x✝ : α
a✝ :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    R s₁ s₂ →
      R (mapAccumr f₁ xs✝ s₁).fst (mapAccumr f₂ xs✝ s₂).fst ∧ (mapAccumr f₁ xs✝ s₁).snd = (mapAccumr f₂ xs✝ s₂).snd
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
⊢ R (mapAccumr f₁ (snoc xs✝ x✝) s₁).fst (mapAccumr f₂ (snoc xs✝ x✝) s₂).fst ∧
    (mapAccumr f₁ (snoc xs✝ x✝) s₁).snd = (mapAccumr f₂ (snoc xs✝ x✝) s₂).snd
[PROOFSTEP]
next => exact ⟨h₀, rfl⟩
[GOAL]
α : Type u_2
n : ℕ
xs : Vector α n
σ₁ : Type
β : Type u_1
σ₂ : Type
f₁ : α → σ₁ → σ₁ × β
f₂ : α → σ₂ → σ₂ × β
R : σ₁ → σ₂ → Prop
hR : ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).fst (f₂ a q).fst ∧ (f₁ a s).snd = (f₂ a q).snd
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
⊢ R (mapAccumr f₁ nil s₁).fst (mapAccumr f₂ nil s₂).fst ∧ (mapAccumr f₁ nil s₁).snd = (mapAccumr f₂ nil s₂).snd
[PROOFSTEP]
exact ⟨h₀, rfl⟩
[GOAL]
case snoc
α : Type u_2
n : ℕ
xs : Vector α n
σ₁ : Type
β : Type u_1
σ₂ : Type
f₁ : α → σ₁ → σ₁ × β
f₂ : α → σ₂ → σ₂ × β
R : σ₁ → σ₂ → Prop
hR : ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).fst (f₂ a q).fst ∧ (f₁ a s).snd = (f₂ a q).snd
n✝ : ℕ
xs✝ : Vector α n✝
x✝ : α
a✝ :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    R s₁ s₂ →
      R (mapAccumr f₁ xs✝ s₁).fst (mapAccumr f₂ xs✝ s₂).fst ∧ (mapAccumr f₁ xs✝ s₁).snd = (mapAccumr f₂ xs✝ s₂).snd
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
⊢ R (mapAccumr f₁ (snoc xs✝ x✝) s₁).fst (mapAccumr f₂ (snoc xs✝ x✝) s₂).fst ∧
    (mapAccumr f₁ (snoc xs✝ x✝) s₁).snd = (mapAccumr f₂ (snoc xs✝ x✝) s₂).snd
[PROOFSTEP]
next xs x ih =>
  rcases(hR x h₀) with ⟨hR, _⟩
  simp only [mapAccumr_snoc, ih hR, true_and]
  congr 1
[GOAL]
α : Type u_2
n : ℕ
xs✝ : Vector α n
σ₁ : Type
β : Type u_1
σ₂ : Type
f₁ : α → σ₁ → σ₁ × β
f₂ : α → σ₂ → σ₂ × β
R : σ₁ → σ₂ → Prop
hR : ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).fst (f₂ a q).fst ∧ (f₁ a s).snd = (f₂ a q).snd
n✝ : ℕ
xs : Vector α n✝
x : α
ih :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    R s₁ s₂ → R (mapAccumr f₁ xs s₁).fst (mapAccumr f₂ xs s₂).fst ∧ (mapAccumr f₁ xs s₁).snd = (mapAccumr f₂ xs s₂).snd
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
⊢ R (mapAccumr f₁ (snoc xs x) s₁).fst (mapAccumr f₂ (snoc xs x) s₂).fst ∧
    (mapAccumr f₁ (snoc xs x) s₁).snd = (mapAccumr f₂ (snoc xs x) s₂).snd
[PROOFSTEP]
rcases(hR x h₀) with ⟨hR, _⟩
[GOAL]
case intro
α : Type u_2
n : ℕ
xs✝ : Vector α n
σ₁ : Type
β : Type u_1
σ₂ : Type
f₁ : α → σ₁ → σ₁ × β
f₂ : α → σ₂ → σ₂ × β
R : σ₁ → σ₂ → Prop
hR✝ : ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).fst (f₂ a q).fst ∧ (f₁ a s).snd = (f₂ a q).snd
n✝ : ℕ
xs : Vector α n✝
x : α
ih :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    R s₁ s₂ → R (mapAccumr f₁ xs s₁).fst (mapAccumr f₂ xs s₂).fst ∧ (mapAccumr f₁ xs s₁).snd = (mapAccumr f₂ xs s₂).snd
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
hR : R (f₁ x s₁).fst (f₂ x s₂).fst
right✝ : (f₁ x s₁).snd = (f₂ x s₂).snd
⊢ R (mapAccumr f₁ (snoc xs x) s₁).fst (mapAccumr f₂ (snoc xs x) s₂).fst ∧
    (mapAccumr f₁ (snoc xs x) s₁).snd = (mapAccumr f₂ (snoc xs x) s₂).snd
[PROOFSTEP]
simp only [mapAccumr_snoc, ih hR, true_and]
[GOAL]
case intro
α : Type u_2
n : ℕ
xs✝ : Vector α n
σ₁ : Type
β : Type u_1
σ₂ : Type
f₁ : α → σ₁ → σ₁ × β
f₂ : α → σ₂ → σ₂ × β
R : σ₁ → σ₂ → Prop
hR✝ : ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).fst (f₂ a q).fst ∧ (f₁ a s).snd = (f₂ a q).snd
n✝ : ℕ
xs : Vector α n✝
x : α
ih :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    R s₁ s₂ → R (mapAccumr f₁ xs s₁).fst (mapAccumr f₂ xs s₂).fst ∧ (mapAccumr f₁ xs s₁).snd = (mapAccumr f₂ xs s₂).snd
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
hR : R (f₁ x s₁).fst (f₂ x s₂).fst
right✝ : (f₁ x s₁).snd = (f₂ x s₂).snd
⊢ snoc (mapAccumr f₂ xs (f₂ x s₂).fst).snd (f₁ x s₁).snd = snoc (mapAccumr f₂ xs (f₂ x s₂).fst).snd (f₂ x s₂).snd
[PROOFSTEP]
congr 1
[GOAL]
α : Type u_2
n : ℕ
xs : Vector α n
σ₁ : Type
β : Type u_1
σ₂ : Type
f₁ : α → σ₁ → σ₁ × β
f₂ : α → σ₂ → σ₂ × β
s₁ : σ₁
s₂ : σ₂
h : ∃ R, R s₁ s₂ ∧ ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).fst (f₂ a q).fst ∧ (f₁ a s).snd = (f₂ a q).snd
⊢ (mapAccumr f₁ xs s₁).snd = (mapAccumr f₂ xs s₂).snd
[PROOFSTEP]
rcases h with ⟨R, h₀, hR⟩
[GOAL]
case intro.intro
α : Type u_2
n : ℕ
xs : Vector α n
σ₁ : Type
β : Type u_1
σ₂ : Type
f₁ : α → σ₁ → σ₁ × β
f₂ : α → σ₂ → σ₂ × β
s₁ : σ₁
s₂ : σ₂
R : σ₁ → σ₂ → Prop
h₀ : R s₁ s₂
hR : ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).fst (f₂ a q).fst ∧ (f₁ a s).snd = (f₂ a q).snd
⊢ (mapAccumr f₁ xs s₁).snd = (mapAccumr f₂ xs s₂).snd
[PROOFSTEP]
exact (mapAccumr_bisim R h₀ hR).2
[GOAL]
α : Type
n : ℕ
xs : Vector α n
β σ₁ γ σ₂ : Type
ys : Vector β n
f₁ : α → β → σ₁ → σ₁ × γ
f₂ : α → β → σ₂ → σ₂ × γ
s₁ : σ₁
s₂ : σ₂
R : σ₁ → σ₂ → Prop
h₀ : R s₁ s₂
hR : ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).fst (f₂ a b q).fst ∧ (f₁ a b s).snd = (f₂ a b q).snd
⊢ R (mapAccumr₂ f₁ xs ys s₁).fst (mapAccumr₂ f₂ xs ys s₂).fst ∧
    (mapAccumr₂ f₁ xs ys s₁).snd = (mapAccumr₂ f₂ xs ys s₂).snd
[PROOFSTEP]
induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂
[GOAL]
case nil
α : Type
n : ℕ
xs : Vector α n
β σ₁ γ σ₂ : Type
f₁ : α → β → σ₁ → σ₁ × γ
f₂ : α → β → σ₂ → σ₂ × γ
R : σ₁ → σ₂ → Prop
hR : ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).fst (f₂ a b q).fst ∧ (f₁ a b s).snd = (f₂ a b q).snd
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
⊢ R (mapAccumr₂ f₁ nil nil s₁).fst (mapAccumr₂ f₂ nil nil s₂).fst ∧
    (mapAccumr₂ f₁ nil nil s₁).snd = (mapAccumr₂ f₂ nil nil s₂).snd
case snoc
α : Type
n : ℕ
xs : Vector α n
β σ₁ γ σ₂ : Type
f₁ : α → β → σ₁ → σ₁ × γ
f₂ : α → β → σ₂ → σ₂ × γ
R : σ₁ → σ₂ → Prop
hR : ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).fst (f₂ a b q).fst ∧ (f₁ a b s).snd = (f₂ a b q).snd
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    R s₁ s₂ →
      R (mapAccumr₂ f₁ xs✝ ys✝ s₁).fst (mapAccumr₂ f₂ xs✝ ys✝ s₂).fst ∧
        (mapAccumr₂ f₁ xs✝ ys✝ s₁).snd = (mapAccumr₂ f₂ xs✝ ys✝ s₂).snd
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
⊢ R (mapAccumr₂ f₁ (snoc xs✝ x✝) (snoc ys✝ y✝) s₁).fst (mapAccumr₂ f₂ (snoc xs✝ x✝) (snoc ys✝ y✝) s₂).fst ∧
    (mapAccumr₂ f₁ (snoc xs✝ x✝) (snoc ys✝ y✝) s₁).snd = (mapAccumr₂ f₂ (snoc xs✝ x✝) (snoc ys✝ y✝) s₂).snd
[PROOFSTEP]
next => exact ⟨h₀, rfl⟩
[GOAL]
α : Type
n : ℕ
xs : Vector α n
β σ₁ γ σ₂ : Type
f₁ : α → β → σ₁ → σ₁ × γ
f₂ : α → β → σ₂ → σ₂ × γ
R : σ₁ → σ₂ → Prop
hR : ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).fst (f₂ a b q).fst ∧ (f₁ a b s).snd = (f₂ a b q).snd
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
⊢ R (mapAccumr₂ f₁ nil nil s₁).fst (mapAccumr₂ f₂ nil nil s₂).fst ∧
    (mapAccumr₂ f₁ nil nil s₁).snd = (mapAccumr₂ f₂ nil nil s₂).snd
[PROOFSTEP]
exact ⟨h₀, rfl⟩
[GOAL]
case snoc
α : Type
n : ℕ
xs : Vector α n
β σ₁ γ σ₂ : Type
f₁ : α → β → σ₁ → σ₁ × γ
f₂ : α → β → σ₂ → σ₂ × γ
R : σ₁ → σ₂ → Prop
hR : ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).fst (f₂ a b q).fst ∧ (f₁ a b s).snd = (f₂ a b q).snd
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    R s₁ s₂ →
      R (mapAccumr₂ f₁ xs✝ ys✝ s₁).fst (mapAccumr₂ f₂ xs✝ ys✝ s₂).fst ∧
        (mapAccumr₂ f₁ xs✝ ys✝ s₁).snd = (mapAccumr₂ f₂ xs✝ ys✝ s₂).snd
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
⊢ R (mapAccumr₂ f₁ (snoc xs✝ x✝) (snoc ys✝ y✝) s₁).fst (mapAccumr₂ f₂ (snoc xs✝ x✝) (snoc ys✝ y✝) s₂).fst ∧
    (mapAccumr₂ f₁ (snoc xs✝ x✝) (snoc ys✝ y✝) s₁).snd = (mapAccumr₂ f₂ (snoc xs✝ x✝) (snoc ys✝ y✝) s₂).snd
[PROOFSTEP]
next xs ys x y ih =>
  rcases(hR x y h₀) with ⟨hR, _⟩
  simp only [mapAccumr₂_snoc, ih hR, true_and]
  congr 1
[GOAL]
α : Type
n : ℕ
xs✝ : Vector α n
β σ₁ γ σ₂ : Type
f₁ : α → β → σ₁ → σ₁ × γ
f₂ : α → β → σ₂ → σ₂ × γ
R : σ₁ → σ₂ → Prop
hR : ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).fst (f₂ a b q).fst ∧ (f₁ a b s).snd = (f₂ a b q).snd
n✝ : ℕ
xs : Vector α n✝
ys : Vector β n✝
x : α
y : β
ih :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    R s₁ s₂ →
      R (mapAccumr₂ f₁ xs ys s₁).fst (mapAccumr₂ f₂ xs ys s₂).fst ∧
        (mapAccumr₂ f₁ xs ys s₁).snd = (mapAccumr₂ f₂ xs ys s₂).snd
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
⊢ R (mapAccumr₂ f₁ (snoc xs x) (snoc ys y) s₁).fst (mapAccumr₂ f₂ (snoc xs x) (snoc ys y) s₂).fst ∧
    (mapAccumr₂ f₁ (snoc xs x) (snoc ys y) s₁).snd = (mapAccumr₂ f₂ (snoc xs x) (snoc ys y) s₂).snd
[PROOFSTEP]
rcases(hR x y h₀) with ⟨hR, _⟩
[GOAL]
case intro
α : Type
n : ℕ
xs✝ : Vector α n
β σ₁ γ σ₂ : Type
f₁ : α → β → σ₁ → σ₁ × γ
f₂ : α → β → σ₂ → σ₂ × γ
R : σ₁ → σ₂ → Prop
hR✝ : ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).fst (f₂ a b q).fst ∧ (f₁ a b s).snd = (f₂ a b q).snd
n✝ : ℕ
xs : Vector α n✝
ys : Vector β n✝
x : α
y : β
ih :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    R s₁ s₂ →
      R (mapAccumr₂ f₁ xs ys s₁).fst (mapAccumr₂ f₂ xs ys s₂).fst ∧
        (mapAccumr₂ f₁ xs ys s₁).snd = (mapAccumr₂ f₂ xs ys s₂).snd
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
hR : R (f₁ x y s₁).fst (f₂ x y s₂).fst
right✝ : (f₁ x y s₁).snd = (f₂ x y s₂).snd
⊢ R (mapAccumr₂ f₁ (snoc xs x) (snoc ys y) s₁).fst (mapAccumr₂ f₂ (snoc xs x) (snoc ys y) s₂).fst ∧
    (mapAccumr₂ f₁ (snoc xs x) (snoc ys y) s₁).snd = (mapAccumr₂ f₂ (snoc xs x) (snoc ys y) s₂).snd
[PROOFSTEP]
simp only [mapAccumr₂_snoc, ih hR, true_and]
[GOAL]
case intro
α : Type
n : ℕ
xs✝ : Vector α n
β σ₁ γ σ₂ : Type
f₁ : α → β → σ₁ → σ₁ × γ
f₂ : α → β → σ₂ → σ₂ × γ
R : σ₁ → σ₂ → Prop
hR✝ : ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).fst (f₂ a b q).fst ∧ (f₁ a b s).snd = (f₂ a b q).snd
n✝ : ℕ
xs : Vector α n✝
ys : Vector β n✝
x : α
y : β
ih :
  ∀ {s₁ : σ₁} {s₂ : σ₂},
    R s₁ s₂ →
      R (mapAccumr₂ f₁ xs ys s₁).fst (mapAccumr₂ f₂ xs ys s₂).fst ∧
        (mapAccumr₂ f₁ xs ys s₁).snd = (mapAccumr₂ f₂ xs ys s₂).snd
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
hR : R (f₁ x y s₁).fst (f₂ x y s₂).fst
right✝ : (f₁ x y s₁).snd = (f₂ x y s₂).snd
⊢ snoc (mapAccumr₂ f₂ xs ys (f₂ x y s₂).fst).snd (f₁ x y s₁).snd =
    snoc (mapAccumr₂ f₂ xs ys (f₂ x y s₂).fst).snd (f₂ x y s₂).snd
[PROOFSTEP]
congr 1
[GOAL]
α : Type
n : ℕ
xs : Vector α n
β σ₁ γ σ₂ : Type
ys : Vector β n
f₁ : α → β → σ₁ → σ₁ × γ
f₂ : α → β → σ₂ → σ₂ × γ
s₁ : σ₁
s₂ : σ₂
h :
  ∃ R,
    R s₁ s₂ ∧
      ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).fst (f₂ a b q).fst ∧ (f₁ a b s).snd = (f₂ a b q).snd
⊢ (mapAccumr₂ f₁ xs ys s₁).snd = (mapAccumr₂ f₂ xs ys s₂).snd
[PROOFSTEP]
rcases h with ⟨R, h₀, hR⟩
[GOAL]
case intro.intro
α : Type
n : ℕ
xs : Vector α n
β σ₁ γ σ₂ : Type
ys : Vector β n
f₁ : α → β → σ₁ → σ₁ × γ
f₂ : α → β → σ₂ → σ₂ × γ
s₁ : σ₁
s₂ : σ₂
R : σ₁ → σ₂ → Prop
h₀ : R s₁ s₂
hR : ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).fst (f₂ a b q).fst ∧ (f₁ a b s).snd = (f₂ a b q).snd
⊢ (mapAccumr₂ f₁ xs ys s₁).snd = (mapAccumr₂ f₂ xs ys s₂).snd
[PROOFSTEP]
exact (mapAccumr₂_bisim R h₀ hR).2
[GOAL]
α : Type u_2
n : ℕ
β : Type ?u.34261
xs : Vector α n
ys : Vector β n
α✝ : Type u_1
f : α → α✝
⊢ map f xs = (mapAccumr (fun x x_1 => ((), f x)) xs ()).snd
[PROOFSTEP]
clear ys
[GOAL]
α : Type u_2
n : ℕ
β : Type ?u.34261
xs : Vector α n
α✝ : Type u_1
f : α → α✝
⊢ map f xs = (mapAccumr (fun x x_1 => ((), f x)) xs ()).snd
[PROOFSTEP]
induction xs using Vector.revInductionOn
[GOAL]
case nil
α : Type u_2
n : ℕ
β : Type ?u.34261
xs : Vector α n
α✝ : Type u_1
f : α → α✝
⊢ map f nil = (mapAccumr (fun x x_1 => ((), f x)) nil ()).snd
[PROOFSTEP]
simp_all
[GOAL]
case snoc
α : Type u_2
n : ℕ
β : Type ?u.34261
xs : Vector α n
α✝ : Type u_1
f : α → α✝
n✝ : ℕ
xs✝ : Vector α n✝
x✝ : α
a✝ : map f xs✝ = (mapAccumr (fun x x_1 => ((), f x)) xs✝ ()).snd
⊢ map f (snoc xs✝ x✝) = (mapAccumr (fun x x_1 => ((), f x)) (snoc xs✝ x✝) ()).snd
[PROOFSTEP]
simp_all
[GOAL]
α : Type u_2
n : ℕ
β : Type u_1
xs : Vector α n
ys : Vector β n
σ : Type
f : α → σ → σ × β
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α) (s : σ), s ∈ S → (f a s).fst ∈ S
out : ∀ (a : α) (s s' : σ), s ∈ S → s' ∈ S → (f a s).snd = (f a s').snd
⊢ (mapAccumr f xs s₀).snd = map (fun x => (f x s₀).snd) xs
[PROOFSTEP]
rw [Vector.map_eq_mapAccumr]
[GOAL]
α : Type u_2
n : ℕ
β : Type u_1
xs : Vector α n
ys : Vector β n
σ : Type
f : α → σ → σ × β
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α) (s : σ), s ∈ S → (f a s).fst ∈ S
out : ∀ (a : α) (s s' : σ), s ∈ S → s' ∈ S → (f a s).snd = (f a s').snd
⊢ (mapAccumr f xs s₀).snd = (mapAccumr (fun x x_1 => ((), (f x s₀).snd)) xs ()).snd
[PROOFSTEP]
apply mapAccumr_bisim_tail
[GOAL]
case h
α : Type u_2
n : ℕ
β : Type u_1
xs : Vector α n
ys : Vector β n
σ : Type
f : α → σ → σ × β
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α) (s : σ), s ∈ S → (f a s).fst ∈ S
out : ∀ (a : α) (s s' : σ), s ∈ S → s' ∈ S → (f a s).snd = (f a s').snd
⊢ ∃ R,
    R s₀ () ∧
      ∀ {s : σ} {q : Unit} (a : α), R s q → R (f a s).fst ((), (f a s₀).snd).fst ∧ (f a s).snd = ((), (f a s₀).snd).snd
[PROOFSTEP]
use fun s _ => s ∈ S, h₀
[GOAL]
case right
α : Type u_2
n : ℕ
β : Type u_1
xs : Vector α n
ys : Vector β n
σ : Type
f : α → σ → σ × β
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α) (s : σ), s ∈ S → (f a s).fst ∈ S
out : ∀ (a : α) (s s' : σ), s ∈ S → s' ∈ S → (f a s).snd = (f a s').snd
⊢ ∀ {s : σ} {q : Unit} (a : α), s ∈ S → (f a s).fst ∈ S ∧ (f a s).snd = ((), (f a s₀).snd).snd
[PROOFSTEP]
exact @fun s _q a h => ⟨closure a s h, out a s s₀ h h₀⟩
[GOAL]
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
α✝ : Type
f : α → β → α✝
⊢ map₂ f xs ys = (mapAccumr₂ (fun x y x_1 => ((), f x y)) xs ys ()).snd
[PROOFSTEP]
induction xs, ys using Vector.revInductionOn₂
[GOAL]
case nil
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
α✝ : Type
f : α → β → α✝
⊢ map₂ f nil nil = (mapAccumr₂ (fun x y x_1 => ((), f x y)) nil nil ()).snd
[PROOFSTEP]
simp_all
[GOAL]
case snoc
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
α✝ : Type
f : α → β → α✝
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ : map₂ f xs✝ ys✝ = (mapAccumr₂ (fun x y x_1 => ((), f x y)) xs✝ ys✝ ()).snd
⊢ map₂ f (snoc xs✝ x✝) (snoc ys✝ y✝) = (mapAccumr₂ (fun x y x_1 => ((), f x y)) (snoc xs✝ x✝) (snoc ys✝ y✝) ()).snd
[PROOFSTEP]
simp_all
[GOAL]
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
f : α → β → σ → σ × γ
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α) (b : β) (s : σ), s ∈ S → (f a b s).fst ∈ S
out : ∀ (a : α) (b : β) (s s' : σ), s ∈ S → s' ∈ S → (f a b s).snd = (f a b s').snd
⊢ (mapAccumr₂ f xs ys s₀).snd = map₂ (fun x x_1 => (f x x_1 s₀).snd) xs ys
[PROOFSTEP]
rw [Vector.map₂_eq_mapAccumr₂]
[GOAL]
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
f : α → β → σ → σ × γ
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α) (b : β) (s : σ), s ∈ S → (f a b s).fst ∈ S
out : ∀ (a : α) (b : β) (s s' : σ), s ∈ S → s' ∈ S → (f a b s).snd = (f a b s').snd
⊢ (mapAccumr₂ f xs ys s₀).snd = (mapAccumr₂ (fun x y x_1 => ((), (f x y s₀).snd)) xs ys ()).snd
[PROOFSTEP]
apply mapAccumr₂_bisim_tail
[GOAL]
case h
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
f : α → β → σ → σ × γ
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α) (b : β) (s : σ), s ∈ S → (f a b s).fst ∈ S
out : ∀ (a : α) (b : β) (s s' : σ), s ∈ S → s' ∈ S → (f a b s).snd = (f a b s').snd
⊢ ∃ R,
    R s₀ () ∧
      ∀ {s : σ} {q : Unit} (a : α) (b : β),
        R s q → R (f a b s).fst ((), (f a b s₀).snd).fst ∧ (f a b s).snd = ((), (f a b s₀).snd).snd
[PROOFSTEP]
use fun s _ => s ∈ S, h₀
[GOAL]
case right
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
f : α → β → σ → σ × γ
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α) (b : β) (s : σ), s ∈ S → (f a b s).fst ∈ S
out : ∀ (a : α) (b : β) (s s' : σ), s ∈ S → s' ∈ S → (f a b s).snd = (f a b s').snd
⊢ ∀ {s : σ} {q : Unit} (a : α) (b : β), s ∈ S → (f a b s).fst ∈ S ∧ (f a b s).snd = ((), (f a b s₀).snd).snd
[PROOFSTEP]
exact @fun s _q a b h => ⟨closure a b s h, out a b s s₀ h h₀⟩
[GOAL]
α : Type u_2
n : ℕ
β : Type u_1
xs : Vector α n
ys : Vector β n
σ : Type
f : α → σ → σ × β
s : σ
h : ∀ (a : α), (f a s).fst = s
⊢ mapAccumr f xs s = (s, map (fun x => (f x s).snd) xs)
[PROOFSTEP]
clear ys
[GOAL]
α : Type u_2
n : ℕ
β : Type u_1
xs : Vector α n
σ : Type
f : α → σ → σ × β
s : σ
h : ∀ (a : α), (f a s).fst = s
⊢ mapAccumr f xs s = (s, map (fun x => (f x s).snd) xs)
[PROOFSTEP]
induction xs using revInductionOn
[GOAL]
case nil
α : Type u_2
n : ℕ
β : Type u_1
xs : Vector α n
σ : Type
f : α → σ → σ × β
s : σ
h : ∀ (a : α), (f a s).fst = s
⊢ mapAccumr f nil s = (s, map (fun x => (f x s).snd) nil)
[PROOFSTEP]
simp_all
[GOAL]
case snoc
α : Type u_2
n : ℕ
β : Type u_1
xs : Vector α n
σ : Type
f : α → σ → σ × β
s : σ
h : ∀ (a : α), (f a s).fst = s
n✝ : ℕ
xs✝ : Vector α n✝
x✝ : α
a✝ : mapAccumr f xs✝ s = (s, map (fun x => (f x s).snd) xs✝)
⊢ mapAccumr f (snoc xs✝ x✝) s = (s, map (fun x => (f x s).snd) (snoc xs✝ x✝))
[PROOFSTEP]
simp_all
[GOAL]
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
f : α → β → σ → σ × γ
s : σ
h : ∀ (a : α) (b : β), (f a b s).fst = s
⊢ mapAccumr₂ f xs ys s = (s, map₂ (fun x y => (f x y s).snd) xs ys)
[PROOFSTEP]
induction xs, ys using revInductionOn₂
[GOAL]
case nil
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
f : α → β → σ → σ × γ
s : σ
h : ∀ (a : α) (b : β), (f a b s).fst = s
⊢ mapAccumr₂ f nil nil s = (s, map₂ (fun x y => (f x y s).snd) nil nil)
[PROOFSTEP]
simp_all
[GOAL]
case snoc
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
f : α → β → σ → σ × γ
s : σ
h : ∀ (a : α) (b : β), (f a b s).fst = s
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ : mapAccumr₂ f xs✝ ys✝ s = (s, map₂ (fun x y => (f x y s).snd) xs✝ ys✝)
⊢ mapAccumr₂ f (snoc xs✝ x✝) (snoc ys✝ y✝) s = (s, map₂ (fun x y => (f x y s).snd) (snoc xs✝ x✝) (snoc ys✝ y✝))
[PROOFSTEP]
simp_all
[GOAL]
α : Type u_2
n : ℕ
β : Type u_1
xs : Vector α n
ys : Vector β n
σ : Type
s : σ
f : α → σ × σ → (σ × σ) × β
h : ∀ (x : α) (s : σ), (f x (s, s)).fst.fst = (f x (s, s)).fst.snd
⊢ ∃ R,
    R (s, s) s ∧
      ∀ {s : σ × σ} {q : σ} (a : α),
        R s q →
          R (f a s).fst ((f a (q, q)).fst.fst, (f a (q, q)).snd).fst ∧
            (f a s).snd = ((f a (q, q)).fst.fst, (f a (q, q)).snd).snd
[PROOFSTEP]
use fun (s₁, s₂) s => s₂ = s ∧ s₁ = s
[GOAL]
case h
α : Type u_2
n : ℕ
β : Type u_1
xs : Vector α n
ys : Vector β n
σ : Type
s : σ
f : α → σ × σ → (σ × σ) × β
h : ∀ (x : α) (s : σ), (f x (s, s)).fst.fst = (f x (s, s)).fst.snd
⊢ (match (s, s) with
    | (s₁, s₂) => s₂ = s ∧ s₁ = s) ∧
    ∀ {s : σ × σ} {q : σ} (a : α),
      (match s with
        | (s₁, s₂) => s₂ = q ∧ s₁ = q) →
        (match (f a s).fst with
          | (s₁, s₂) =>
            s₂ = ((f a (q, q)).fst.fst, (f a (q, q)).snd).fst ∧ s₁ = ((f a (q, q)).fst.fst, (f a (q, q)).snd).fst) ∧
          (f a s).snd = ((f a (q, q)).fst.fst, (f a (q, q)).snd).snd
[PROOFSTEP]
simp_all
[GOAL]
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
s : σ
f : α → β → σ × σ → (σ × σ) × γ
h :
  ∀ (x : α) (y : β) (s : σ),
    let s' := (f x y (s, s)).fst;
    s'.fst = s'.snd
⊢ ∃ R,
    R (s, s) s ∧
      ∀ {s : σ × σ} {q : σ} (a : α) (b : β),
        R s q →
          R (f a b s).fst ((f a b (q, q)).fst.fst, (f a b (q, q)).snd).fst ∧
            (f a b s).snd = ((f a b (q, q)).fst.fst, (f a b (q, q)).snd).snd
[PROOFSTEP]
use fun (s₁, s₂) s => s₂ = s ∧ s₁ = s
[GOAL]
case h
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
s : σ
f : α → β → σ × σ → (σ × σ) × γ
h :
  ∀ (x : α) (y : β) (s : σ),
    let s' := (f x y (s, s)).fst;
    s'.fst = s'.snd
⊢ (match (s, s) with
    | (s₁, s₂) => s₂ = s ∧ s₁ = s) ∧
    ∀ {s : σ × σ} {q : σ} (a : α) (b : β),
      (match s with
        | (s₁, s₂) => s₂ = q ∧ s₁ = q) →
        (match (f a b s).fst with
          | (s₁, s₂) =>
            s₂ = ((f a b (q, q)).fst.fst, (f a b (q, q)).snd).fst ∧
              s₁ = ((f a b (q, q)).fst.fst, (f a b (q, q)).snd).fst) ∧
          (f a b s).snd = ((f a b (q, q)).fst.fst, (f a b (q, q)).snd).snd
[PROOFSTEP]
simp_all
[GOAL]
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
s : σ
inst✝ : Inhabited α
f : α → β → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f default b s = f a b s
⊢ mapAccumr₂ f xs ys s = mapAccumr (fun b s => f default b s) ys s
[PROOFSTEP]
induction xs, ys using Vector.revInductionOn₂ generalizing s
[GOAL]
case nil
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
inst✝ : Inhabited α
f : α → β → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f default b s = f a b s
s : σ
⊢ mapAccumr₂ f nil nil s = mapAccumr (fun b s => f default b s) nil s
case snoc
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
inst✝ : Inhabited α
f : α → β → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f default b s = f a b s
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ : ∀ {s : σ}, mapAccumr₂ f xs✝ ys✝ s = mapAccumr (fun b s => f default b s) ys✝ s
s : σ
⊢ mapAccumr₂ f (snoc xs✝ x✝) (snoc ys✝ y✝) s = mapAccumr (fun b s => f default b s) (snoc ys✝ y✝) s
[PROOFSTEP]
case nil => rfl
[GOAL]
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
inst✝ : Inhabited α
f : α → β → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f default b s = f a b s
s : σ
⊢ mapAccumr₂ f nil nil s = mapAccumr (fun b s => f default b s) nil s
[PROOFSTEP]
case nil => rfl
[GOAL]
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
inst✝ : Inhabited α
f : α → β → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f default b s = f a b s
s : σ
⊢ mapAccumr₂ f nil nil s = mapAccumr (fun b s => f default b s) nil s
[PROOFSTEP]
rfl
[GOAL]
case snoc
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
inst✝ : Inhabited α
f : α → β → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f default b s = f a b s
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ : ∀ {s : σ}, mapAccumr₂ f xs✝ ys✝ s = mapAccumr (fun b s => f default b s) ys✝ s
s : σ
⊢ mapAccumr₂ f (snoc xs✝ x✝) (snoc ys✝ y✝) s = mapAccumr (fun b s => f default b s) (snoc ys✝ y✝) s
[PROOFSTEP]
case snoc xs ys x y ih => simp [h x y s, ih]
[GOAL]
α : Type
n : ℕ
β : Type
xs✝ : Vector α n
ys✝ : Vector β n
σ γ : Type
inst✝ : Inhabited α
f : α → β → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f default b s = f a b s
n✝ : ℕ
xs : Vector α n✝
ys : Vector β n✝
x : α
y : β
ih : ∀ {s : σ}, mapAccumr₂ f xs ys s = mapAccumr (fun b s => f default b s) ys s
s : σ
⊢ mapAccumr₂ f (snoc xs x) (snoc ys y) s = mapAccumr (fun b s => f default b s) (snoc ys y) s
[PROOFSTEP]
case snoc xs ys x y ih => simp [h x y s, ih]
[GOAL]
α : Type
n : ℕ
β : Type
xs✝ : Vector α n
ys✝ : Vector β n
σ γ : Type
inst✝ : Inhabited α
f : α → β → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f default b s = f a b s
n✝ : ℕ
xs : Vector α n✝
ys : Vector β n✝
x : α
y : β
ih : ∀ {s : σ}, mapAccumr₂ f xs ys s = mapAccumr (fun b s => f default b s) ys s
s : σ
⊢ mapAccumr₂ f (snoc xs x) (snoc ys y) s = mapAccumr (fun b s => f default b s) (snoc ys y) s
[PROOFSTEP]
simp [h x y s, ih]
[GOAL]
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
s : σ
inst✝ : Inhabited β
f : α → β → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f a default s = f a b s
⊢ mapAccumr₂ f xs ys s = mapAccumr (fun a s => f a default s) xs s
[PROOFSTEP]
induction xs, ys using Vector.revInductionOn₂ generalizing s
[GOAL]
case nil
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
inst✝ : Inhabited β
f : α → β → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f a default s = f a b s
s : σ
⊢ mapAccumr₂ f nil nil s = mapAccumr (fun a s => f a default s) nil s
case snoc
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
inst✝ : Inhabited β
f : α → β → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f a default s = f a b s
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ : ∀ {s : σ}, mapAccumr₂ f xs✝ ys✝ s = mapAccumr (fun a s => f a default s) xs✝ s
s : σ
⊢ mapAccumr₂ f (snoc xs✝ x✝) (snoc ys✝ y✝) s = mapAccumr (fun a s => f a default s) (snoc xs✝ x✝) s
[PROOFSTEP]
case nil => rfl
[GOAL]
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
inst✝ : Inhabited β
f : α → β → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f a default s = f a b s
s : σ
⊢ mapAccumr₂ f nil nil s = mapAccumr (fun a s => f a default s) nil s
[PROOFSTEP]
case nil => rfl
[GOAL]
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
inst✝ : Inhabited β
f : α → β → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f a default s = f a b s
s : σ
⊢ mapAccumr₂ f nil nil s = mapAccumr (fun a s => f a default s) nil s
[PROOFSTEP]
rfl
[GOAL]
case snoc
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
inst✝ : Inhabited β
f : α → β → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f a default s = f a b s
n✝ : ℕ
xs✝ : Vector α n✝
ys✝ : Vector β n✝
x✝ : α
y✝ : β
a✝ : ∀ {s : σ}, mapAccumr₂ f xs✝ ys✝ s = mapAccumr (fun a s => f a default s) xs✝ s
s : σ
⊢ mapAccumr₂ f (snoc xs✝ x✝) (snoc ys✝ y✝) s = mapAccumr (fun a s => f a default s) (snoc xs✝ x✝) s
[PROOFSTEP]
case snoc xs ys x y ih => simp [h x y s, ih]
[GOAL]
α : Type
n : ℕ
β : Type
xs✝ : Vector α n
ys✝ : Vector β n
σ γ : Type
inst✝ : Inhabited β
f : α → β → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f a default s = f a b s
n✝ : ℕ
xs : Vector α n✝
ys : Vector β n✝
x : α
y : β
ih : ∀ {s : σ}, mapAccumr₂ f xs ys s = mapAccumr (fun a s => f a default s) xs s
s : σ
⊢ mapAccumr₂ f (snoc xs x) (snoc ys y) s = mapAccumr (fun a s => f a default s) (snoc xs x) s
[PROOFSTEP]
case snoc xs ys x y ih => simp [h x y s, ih]
[GOAL]
α : Type
n : ℕ
β : Type
xs✝ : Vector α n
ys✝ : Vector β n
σ γ : Type
inst✝ : Inhabited β
f : α → β → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f a default s = f a b s
n✝ : ℕ
xs : Vector α n✝
ys : Vector β n✝
x : α
y : β
ih : ∀ {s : σ}, mapAccumr₂ f xs ys s = mapAccumr (fun a s => f a default s) xs s
s : σ
⊢ mapAccumr₂ f (snoc xs x) (snoc ys y) s = mapAccumr (fun a s => f a default s) (snoc xs x) s
[PROOFSTEP]
simp [h x y s, ih]
[GOAL]
α : Type u_2
n : ℕ
xs ys : Vector α n
β : Type u_1
f : α → α → β
comm : ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁
⊢ map₂ f xs ys = map₂ f ys xs
[PROOFSTEP]
induction xs, ys using Vector.inductionOn₂
[GOAL]
case nil
α : Type u_2
n : ℕ
xs ys : Vector α n
β : Type u_1
f : α → α → β
comm : ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁
⊢ map₂ f nil nil = map₂ f nil nil
[PROOFSTEP]
simp_all
[GOAL]
case cons
α : Type u_2
n : ℕ
xs ys : Vector α n
β : Type u_1
f : α → α → β
comm : ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁
n✝ : ℕ
a✝¹ b✝ : α
x✝ y✝ : Vector α n✝
a✝ : map₂ f x✝ y✝ = map₂ f y✝ x✝
⊢ map₂ f (a✝¹ ::ᵥ x✝) (b✝ ::ᵥ y✝) = map₂ f (b✝ ::ᵥ y✝) (a✝¹ ::ᵥ x✝)
[PROOFSTEP]
simp_all
[GOAL]
α : Type
n : ℕ
xs ys : Vector α n
σ γ : Type
s : σ
f : α → α → σ → σ × γ
comm : ∀ (a₁ a₂ : α) (s : σ), f a₁ a₂ s = f a₂ a₁ s
⊢ mapAccumr₂ f xs ys s = mapAccumr₂ f ys xs s
[PROOFSTEP]
induction xs, ys using Vector.inductionOn₂ generalizing s
[GOAL]
case nil
α : Type
n : ℕ
xs ys : Vector α n
σ γ : Type
f : α → α → σ → σ × γ
comm : ∀ (a₁ a₂ : α) (s : σ), f a₁ a₂ s = f a₂ a₁ s
s : σ
⊢ mapAccumr₂ f nil nil s = mapAccumr₂ f nil nil s
[PROOFSTEP]
simp_all
[GOAL]
case cons
α : Type
n : ℕ
xs ys : Vector α n
σ γ : Type
f : α → α → σ → σ × γ
comm : ∀ (a₁ a₂ : α) (s : σ), f a₁ a₂ s = f a₂ a₁ s
n✝ : ℕ
a✝¹ b✝ : α
x✝ y✝ : Vector α n✝
a✝ : ∀ {s : σ}, mapAccumr₂ f x✝ y✝ s = mapAccumr₂ f y✝ x✝ s
s : σ
⊢ mapAccumr₂ f (a✝¹ ::ᵥ x✝) (b✝ ::ᵥ y✝) s = mapAccumr₂ f (b✝ ::ᵥ y✝) (a✝¹ ::ᵥ x✝) s
[PROOFSTEP]
simp_all
[GOAL]
α : Type u_2
n : ℕ
β : Type u_3
xs : Vector α n
ys : Vector β n
γ : Type u_1
f : α → β → γ
⊢ map₂ f xs ys = map₂ (flip f) ys xs
[PROOFSTEP]
induction xs, ys using Vector.inductionOn₂
[GOAL]
case nil
α : Type u_2
n : ℕ
β : Type u_3
xs : Vector α n
ys : Vector β n
γ : Type u_1
f : α → β → γ
⊢ map₂ f nil nil = map₂ (flip f) nil nil
[PROOFSTEP]
simp_all [flip]
[GOAL]
case cons
α : Type u_2
n : ℕ
β : Type u_3
xs : Vector α n
ys : Vector β n
γ : Type u_1
f : α → β → γ
n✝ : ℕ
a✝¹ : α
b✝ : β
x✝ : Vector α n✝
y✝ : Vector β n✝
a✝ : map₂ f x✝ y✝ = map₂ (flip f) y✝ x✝
⊢ map₂ f (a✝¹ ::ᵥ x✝) (b✝ ::ᵥ y✝) = map₂ (flip f) (b✝ ::ᵥ y✝) (a✝¹ ::ᵥ x✝)
[PROOFSTEP]
simp_all [flip]
[GOAL]
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
s : σ
f : α → β → σ → σ × γ
⊢ mapAccumr₂ f xs ys s = mapAccumr₂ (flip f) ys xs s
[PROOFSTEP]
induction xs, ys using Vector.inductionOn₂
[GOAL]
case nil
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
s : σ
f : α → β → σ → σ × γ
⊢ mapAccumr₂ f nil nil s = mapAccumr₂ (flip f) nil nil s
[PROOFSTEP]
simp_all [flip]
[GOAL]
case cons
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ γ : Type
s : σ
f : α → β → σ → σ × γ
n✝ : ℕ
a✝¹ : α
b✝ : β
x✝ : Vector α n✝
y✝ : Vector β n✝
a✝ : mapAccumr₂ f x✝ y✝ s = mapAccumr₂ (flip f) y✝ x✝ s
⊢ mapAccumr₂ f (a✝¹ ::ᵥ x✝) (b✝ ::ᵥ y✝) s = mapAccumr₂ (flip f) (b✝ ::ᵥ y✝) (a✝¹ ::ᵥ x✝) s
[PROOFSTEP]
simp_all [flip]


[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
a b : α
⊢ b • stdBasisMatrix i j a = stdBasisMatrix i j (b • a)
[PROOFSTEP]
unfold stdBasisMatrix
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
a b : α
⊢ (b • fun i' j' => if i = i' ∧ j = j' then a else 0) = fun i' j' => if i = i' ∧ j = j' then b • a else 0
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
a b : α
i✝ : m
x✝ : n
⊢ (b • fun i' j' => if i = i' ∧ j = j' then a else 0) i✝ x✝ = if i = i✝ ∧ j = x✝ then b • a else 0
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
⊢ stdBasisMatrix i j 0 = 0
[PROOFSTEP]
unfold stdBasisMatrix
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
⊢ (fun i' j' => if i = i' ∧ j = j' then 0 else 0) = 0
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
i✝ : m
x✝ : n
⊢ (if i = i✝ ∧ j = x✝ then 0 else 0) = OfNat.ofNat 0 i✝ x✝
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
a b : α
⊢ stdBasisMatrix i j (a + b) = stdBasisMatrix i j a + stdBasisMatrix i j b
[PROOFSTEP]
unfold stdBasisMatrix
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
a b : α
⊢ (fun i' j' => if i = i' ∧ j = j' then a + b else 0) =
    (fun i' j' => if i = i' ∧ j = j' then a else 0) + fun i' j' => if i = i' ∧ j = j' then b else 0
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
a b : α
i✝ : m
x✝ : n
⊢ (if i = i✝ ∧ j = x✝ then a + b else 0) =
    ((fun i' j' => if i = i' ∧ j = j' then a else 0) + fun i' j' => if i = i' ∧ j = j' then b else 0) i✝ x✝
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
a b : α
i✝ : m
x✝ : n
h : i = i✝ ∧ j = x✝
⊢ a + b = ((fun i' j' => if i = i' ∧ j = j' then a else 0) + fun i' j' => if i = i' ∧ j = j' then b else 0) i✝ x✝
[PROOFSTEP]
simp [h]
[GOAL]
case neg
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
a b : α
i✝ : m
x✝ : n
h : ¬(i = i✝ ∧ j = x✝)
⊢ 0 = ((fun i' j' => if i = i' ∧ j = j' then a else 0) + fun i' j' => if i = i' ∧ j = j' then b else 0) i✝ x✝
[PROOFSTEP]
simp [h]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
x : Matrix m n α
⊢ x = ∑ i : m, ∑ j : n, stdBasisMatrix i j (x i j)
[PROOFSTEP]
ext i j
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
x : Matrix m n α
i : m
j : n
⊢ x i j = Finset.sum Finset.univ (fun i => ∑ j : n, stdBasisMatrix i j (x i j)) i j
[PROOFSTEP]
symm
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
x : Matrix m n α
i : m
j : n
⊢ Finset.sum Finset.univ (fun i => ∑ j : n, stdBasisMatrix i j (x i j)) i j = x i j
[PROOFSTEP]
iterate 2
  rw [Finset.sum_apply]
    -- Porting note: was `convert`
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
x : Matrix m n α
i : m
j : n
⊢ Finset.sum Finset.univ (fun i => ∑ j : n, stdBasisMatrix i j (x i j)) i j = x i j
[PROOFSTEP]
rw [Finset.sum_apply]
  -- Porting note: was `convert`
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
x : Matrix m n α
i : m
j : n
⊢ Finset.sum Finset.univ (fun c => Finset.sum Finset.univ (fun j => stdBasisMatrix c j (x c j)) i) j = x i j
[PROOFSTEP]
rw [Finset.sum_apply]
  -- Porting note: was `convert`
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
x : Matrix m n α
i : m
j : n
⊢ ∑ c : m, Finset.sum Finset.univ (fun j => stdBasisMatrix c j (x c j)) i j = x i j
[PROOFSTEP]
refine (Fintype.sum_eq_single i ?_).trans ?_
[GOAL]
case a.h.refine_1
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
x : Matrix m n α
i : m
j : n
⊢ ∀ (x_1 : m), x_1 ≠ i → Finset.sum Finset.univ (fun j => stdBasisMatrix x_1 j (x x_1 j)) i j = 0
case a.h.refine_2
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
x : Matrix m n α
i : m
j : n
⊢ Finset.sum Finset.univ (fun j => stdBasisMatrix i j (x i j)) i j = x i j
[PROOFSTEP]
swap
[GOAL]
case a.h.refine_2
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
x : Matrix m n α
i : m
j : n
⊢ Finset.sum Finset.univ (fun j => stdBasisMatrix i j (x i j)) i j = x i j
[PROOFSTEP]
simp only [stdBasisMatrix]
[GOAL]
case a.h.refine_2
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
x : Matrix m n α
i : m
j : n
⊢ Finset.sum Finset.univ (fun x_1 i' j' => if i = i' ∧ x_1 = j' then x i x_1 else 0) i j = x i j
[PROOFSTEP]
rw [Fintype.sum_apply, Fintype.sum_apply]
[GOAL]
case a.h.refine_2
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
x : Matrix m n α
i : m
j : n
⊢ (∑ c : n, if i = i ∧ c = j then x i c else 0) = x i j
[PROOFSTEP]
simp
[GOAL]
case a.h.refine_1
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
x : Matrix m n α
i : m
j : n
⊢ ∀ (x_1 : m), x_1 ≠ i → Finset.sum Finset.univ (fun j => stdBasisMatrix x_1 j (x x_1 j)) i j = 0
[PROOFSTEP]
intro j' hj'
[GOAL]
case a.h.refine_1
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
x : Matrix m n α
i : m
j : n
j' : m
hj' : j' ≠ i
⊢ Finset.sum Finset.univ (fun j => stdBasisMatrix j' j (x j' j)) i j = 0
[PROOFSTEP]
simp only [stdBasisMatrix]
[GOAL]
case a.h.refine_1
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
x : Matrix m n α
i : m
j : n
j' : m
hj' : j' ≠ i
⊢ Finset.sum Finset.univ (fun x_1 i' j'_1 => if j' = i' ∧ x_1 = j'_1 then x j' x_1 else 0) i j = 0
[PROOFSTEP]
rw [Fintype.sum_apply, Fintype.sum_apply]
[GOAL]
case a.h.refine_1
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
x : Matrix m n α
i : m
j : n
j' : m
hj' : j' ≠ i
⊢ (∑ c : n, if j' = i ∧ c = j then x j' c else 0) = 0
[PROOFSTEP]
simp [hj']
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
⊢ stdBasisMatrix i j 1 = vecMulVec (fun i' => if i = i' then 1 else 0) fun j' => if j = j' then 1 else 0
[PROOFSTEP]
ext i' j'
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
i' : m
j' : n
⊢ stdBasisMatrix i j 1 i' j' = vecMulVec (fun i' => if i = i' then 1 else 0) (fun j' => if j = j' then 1 else 0) i' j'
[PROOFSTEP]
simp only [stdBasisMatrix, vecMulVec, mul_ite, mul_one, mul_zero, of_apply]
  -- Porting note: added next line
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
i' : m
j' : n
⊢ (if i = i' ∧ j = j' then 1 else 0) = if j = j' then if i = i' then 1 else 0 else 0
[PROOFSTEP]
simp_rw [@and_comm (i = i')]
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
i' : m
j' : n
⊢ (if j = j' ∧ i = i' then 1 else 0) = if j = j' then if i = i' then 1 else 0 else 0
[PROOFSTEP]
exact ite_and _ _ _ _
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (stdBasisMatrix i j x)
⊢ P M
[PROOFSTEP]
rw [matrix_eq_sum_std_basis M, ← Finset.sum_product']
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (stdBasisMatrix i j x)
⊢ P (∑ x in Finset.univ ×ˢ Finset.univ, stdBasisMatrix x.fst x.snd (M x.fst x.snd))
[PROOFSTEP]
apply Finset.sum_induction _ _ h_add h_zero
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (stdBasisMatrix i j x)
⊢ ∀ (x : m × n), x ∈ Finset.univ ×ˢ Finset.univ → P (stdBasisMatrix x.fst x.snd (M x.fst x.snd))
[PROOFSTEP]
intros
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (stdBasisMatrix i j x)
x✝ : m × n
a✝ : x✝ ∈ Finset.univ ×ˢ Finset.univ
⊢ P (stdBasisMatrix x✝.fst x✝.snd (M x✝.fst x✝.snd))
[PROOFSTEP]
apply h_std_basis
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁷ : DecidableEq l
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq n
inst✝⁴ : Semiring α
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : Nonempty m
inst✝ : Nonempty n
P : Matrix m n α → Prop
M : Matrix m n α
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (stdBasisMatrix i j x)
⊢ P 0
[PROOFSTEP]
inhabit m
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁷ : DecidableEq l
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq n
inst✝⁴ : Semiring α
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : Nonempty m
inst✝ : Nonempty n
P : Matrix m n α → Prop
M : Matrix m n α
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (stdBasisMatrix i j x)
inhabited_h : Inhabited m
⊢ P 0
[PROOFSTEP]
inhabit n
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁷ : DecidableEq l
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq n
inst✝⁴ : Semiring α
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : Nonempty m
inst✝ : Nonempty n
P : Matrix m n α → Prop
M : Matrix m n α
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (stdBasisMatrix i j x)
inhabited_h✝ : Inhabited m
inhabited_h : Inhabited n
⊢ P 0
[PROOFSTEP]
simpa using h_std_basis default default 0
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
c : α
i' : m
j' : n
h : ¬(i = i' ∧ j = j')
⊢ stdBasisMatrix i j c i' j' = 0
[PROOFSTEP]
simp only [stdBasisMatrix, and_imp, ite_eq_right_iff]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
c : α
i' : m
j' : n
h : ¬(i = i' ∧ j = j')
⊢ i = i' → j = j' → c = 0
[PROOFSTEP]
tauto
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i✝ : m
j✝ : n
c : α
i'✝ : m
j'✝ : n
i i' : m
hi : i ≠ i'
j j' : n
a : α
⊢ stdBasisMatrix i j a i' j' = 0
[PROOFSTEP]
simp [hi]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i✝ : m
j✝ : n
c : α
i'✝ : m
j'✝ : n
i i' : m
j j' : n
hj : j ≠ j'
a : α
⊢ stdBasisMatrix i j a i' j' = 0
[PROOFSTEP]
simp [hj]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i j : n
c : α
i' j' : n
⊢ diag (stdBasisMatrix i i c) = Pi.single i c
[PROOFSTEP]
ext j
[GOAL]
case h
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i j✝ : n
c : α
i' j' j : n
⊢ diag (stdBasisMatrix i i c) j = Pi.single i c j
[PROOFSTEP]
by_cases hij : i = j
[GOAL]
case pos
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i j✝ : n
c : α
i' j' j : n
hij : i = j
⊢ diag (stdBasisMatrix i i c) j = Pi.single i c j
[PROOFSTEP]
try rw [hij]
[GOAL]
case pos
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i j✝ : n
c : α
i' j' j : n
hij : i = j
⊢ diag (stdBasisMatrix i i c) j = Pi.single i c j
[PROOFSTEP]
rw [hij]
[GOAL]
case neg
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i j✝ : n
c : α
i' j' j : n
hij : ¬i = j
⊢ diag (stdBasisMatrix i i c) j = Pi.single i c j
[PROOFSTEP]
try rw [hij]
[GOAL]
case neg
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i j✝ : n
c : α
i' j' j : n
hij : ¬i = j
⊢ diag (stdBasisMatrix i i c) j = Pi.single i c j
[PROOFSTEP]
rw [hij]
[GOAL]
case pos
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i j✝ : n
c : α
i' j' j : n
hij : i = j
⊢ diag (stdBasisMatrix j j c) j = Pi.single j c j
[PROOFSTEP]
simp [hij]
[GOAL]
case neg
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i j✝ : n
c : α
i' j' j : n
hij : ¬i = j
⊢ diag (stdBasisMatrix i i c) j = Pi.single i c j
[PROOFSTEP]
simp [hij]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
h : j ≠ i
⊢ trace (stdBasisMatrix i j c) = 0
[PROOFSTEP]
simp [trace, -diag_apply, h]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
⊢ trace (stdBasisMatrix i i c) = c
[PROOFSTEP]
simp [trace, -diag_apply]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
b : n
M : Matrix n n α
⊢ (stdBasisMatrix i j c * M) i b = c * M j b
[PROOFSTEP]
simp [mul_apply, stdBasisMatrix]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
a : n
M : Matrix n n α
⊢ (M * stdBasisMatrix i j c) a j = M a i * c
[PROOFSTEP]
simp [mul_apply, stdBasisMatrix, mul_comm]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
a b : n
h : a ≠ i
M : Matrix n n α
⊢ (stdBasisMatrix i j c * M) a b = 0
[PROOFSTEP]
simp [mul_apply, h.symm]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
a b : n
hbj : b ≠ j
M : Matrix n n α
⊢ (M * stdBasisMatrix i j c) a b = 0
[PROOFSTEP]
simp [mul_apply, hbj.symm]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
k : n
d : α
⊢ stdBasisMatrix i j c * stdBasisMatrix j k d = stdBasisMatrix i k (c * d)
[PROOFSTEP]
ext a b
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
k : n
d : α
a b : n
⊢ (stdBasisMatrix i j c * stdBasisMatrix j k d) a b = stdBasisMatrix i k (c * d) a b
[PROOFSTEP]
simp only [mul_apply, stdBasisMatrix, boole_mul]
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
k : n
d : α
a b : n
⊢ (∑ j_1 : n, (if i = a ∧ j = j_1 then c else 0) * if j = j_1 ∧ k = b then d else 0) =
    if i = a ∧ k = b then c * d else 0
[PROOFSTEP]
by_cases h₁ : i = a
[GOAL]
case pos
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
k : n
d : α
a b : n
h₁ : i = a
⊢ (∑ j_1 : n, (if i = a ∧ j = j_1 then c else 0) * if j = j_1 ∧ k = b then d else 0) =
    if i = a ∧ k = b then c * d else 0
[PROOFSTEP]
by_cases h₂ : k = b
[GOAL]
case neg
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
k : n
d : α
a b : n
h₁ : ¬i = a
⊢ (∑ j_1 : n, (if i = a ∧ j = j_1 then c else 0) * if j = j_1 ∧ k = b then d else 0) =
    if i = a ∧ k = b then c * d else 0
[PROOFSTEP]
by_cases h₂ : k = b
[GOAL]
case pos
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
k : n
d : α
a b : n
h₁ : i = a
h₂ : k = b
⊢ (∑ j_1 : n, (if i = a ∧ j = j_1 then c else 0) * if j = j_1 ∧ k = b then d else 0) =
    if i = a ∧ k = b then c * d else 0
[PROOFSTEP]
simp [h₁, h₂]
[GOAL]
case neg
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
k : n
d : α
a b : n
h₁ : i = a
h₂ : ¬k = b
⊢ (∑ j_1 : n, (if i = a ∧ j = j_1 then c else 0) * if j = j_1 ∧ k = b then d else 0) =
    if i = a ∧ k = b then c * d else 0
[PROOFSTEP]
simp [h₁, h₂]
[GOAL]
case pos
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
k : n
d : α
a b : n
h₁ : ¬i = a
h₂ : k = b
⊢ (∑ j_1 : n, (if i = a ∧ j = j_1 then c else 0) * if j = j_1 ∧ k = b then d else 0) =
    if i = a ∧ k = b then c * d else 0
[PROOFSTEP]
simp [h₁, h₂]
[GOAL]
case neg
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
k : n
d : α
a b : n
h₁ : ¬i = a
h₂ : ¬k = b
⊢ (∑ j_1 : n, (if i = a ∧ j = j_1 then c else 0) * if j = j_1 ∧ k = b then d else 0) =
    if i = a ∧ k = b then c * d else 0
[PROOFSTEP]
simp [h₁, h₂]
[GOAL]
l✝ : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l✝
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
k l : n
h : j ≠ k
d : α
⊢ stdBasisMatrix i j c * stdBasisMatrix k l d = 0
[PROOFSTEP]
ext a b
[GOAL]
case a.h
l✝ : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l✝
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
k l : n
h : j ≠ k
d : α
a b : n
⊢ (stdBasisMatrix i j c * stdBasisMatrix k l d) a b = OfNat.ofNat 0 a b
[PROOFSTEP]
simp only [mul_apply, boole_mul, stdBasisMatrix]
[GOAL]
case a.h
l✝ : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l✝
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
k l : n
h : j ≠ k
d : α
a b : n
⊢ (∑ j_1 : n, (if i = a ∧ j = j_1 then c else 0) * if k = j_1 ∧ l = b then d else 0) = OfNat.ofNat 0 a b
[PROOFSTEP]
by_cases h₁ : i = a
[GOAL]
case pos
l✝ : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l✝
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
k l : n
h : j ≠ k
d : α
a b : n
h₁ : i = a
⊢ (∑ j_1 : n, (if i = a ∧ j = j_1 then c else 0) * if k = j_1 ∧ l = b then d else 0) = OfNat.ofNat 0 a b
[PROOFSTEP]
simp only [h₁, true_and, mul_ite, ite_mul, zero_mul, mul_zero, ← ite_and, zero_apply]
[GOAL]
case pos
l✝ : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l✝
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
k l : n
h : j ≠ k
d : α
a b : n
h₁ : i = a
⊢ (∑ x : n, if (k = x ∧ l = b) ∧ j = x then c * d else 0) = 0
[PROOFSTEP]
refine Finset.sum_eq_zero (fun x _ => ?_)
[GOAL]
case pos
l✝ : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l✝
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
k l : n
h : j ≠ k
d : α
a b : n
h₁ : i = a
x : n
x✝ : x ∈ Finset.univ
⊢ (if (k = x ∧ l = b) ∧ j = x then c * d else 0) = 0
[PROOFSTEP]
apply if_neg
[GOAL]
case pos.hnc
l✝ : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l✝
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
k l : n
h : j ≠ k
d : α
a b : n
h₁ : i = a
x : n
x✝ : x ∈ Finset.univ
⊢ ¬((k = x ∧ l = b) ∧ j = x)
[PROOFSTEP]
rintro ⟨⟨rfl, rfl⟩, h⟩
[GOAL]
case pos.hnc.intro.intro
l✝ : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l✝
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
k l : n
h✝ : j ≠ k
d : α
a : n
h₁ : i = a
x✝ : k ∈ Finset.univ
h : j = k
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case neg
l✝ : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l✝
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
k l : n
h : j ≠ k
d : α
a b : n
h₁ : ¬i = a
⊢ (∑ j_1 : n, (if i = a ∧ j = j_1 then c else 0) * if k = j_1 ∧ l = b then d else 0) = OfNat.ofNat 0 a b
[PROOFSTEP]
simp only [h₁, false_and, ite_false, mul_ite, zero_mul, mul_zero, ite_self, Finset.sum_const_zero, zero_apply]


[GOAL]
n : Type u_1
inst✝⁴ : Fintype n
R : Type u_2
inst✝³ : Ring R
inst✝² : DecidableEq n
inst✝¹ : Nonempty n
p : ℕ
inst✝ : CharP R p
⊢ ∀ (x : ℕ), ↑x = 0 ↔ p ∣ x
[PROOFSTEP]
intro k
[GOAL]
n : Type u_1
inst✝⁴ : Fintype n
R : Type u_2
inst✝³ : Ring R
inst✝² : DecidableEq n
inst✝¹ : Nonempty n
p : ℕ
inst✝ : CharP R p
k : ℕ
⊢ ↑k = 0 ↔ p ∣ k
[PROOFSTEP]
rw [← CharP.cast_eq_zero_iff R p k, ← Nat.cast_zero, ← map_natCast <| scalar n]
[GOAL]
n : Type u_1
inst✝⁴ : Fintype n
R : Type u_2
inst✝³ : Ring R
inst✝² : DecidableEq n
inst✝¹ : Nonempty n
p : ℕ
inst✝ : CharP R p
k : ℕ
⊢ ↑(scalar n) ↑k = ↑0 ↔ ↑k = 0
[PROOFSTEP]
convert @scalar_inj n _ _ _ _ _ (@Nat.cast R NonAssocSemiring.toNatCast k) 0
[GOAL]
case h.e'_1.h.e'_3
n : Type u_1
inst✝⁴ : Fintype n
R : Type u_2
inst✝³ : Ring R
inst✝² : DecidableEq n
inst✝¹ : Nonempty n
p : ℕ
inst✝ : CharP R p
k : ℕ
⊢ ↑0 = ↑(scalar n) 0
[PROOFSTEP]
simp


[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
m : Type u_4
n : Type u_5
R : Type u_6
A B C : Matrix m n α
inst✝¹ : DecidableEq n
inst✝ : MulZeroOneClass α
M : Matrix n n α
⊢ M ⊙ 1 = diagonal fun i => M i i
[PROOFSTEP]
ext i j
[GOAL]
case a.h
α : Type u_1
β : Type u_2
γ : Type u_3
m : Type u_4
n : Type u_5
R : Type u_6
A B C : Matrix m n α
inst✝¹ : DecidableEq n
inst✝ : MulZeroOneClass α
M : Matrix n n α
i j : n
⊢ (M ⊙ 1) i j = diagonal (fun i => M i i) i j
[PROOFSTEP]
by_cases h : i = j
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
m : Type u_4
n : Type u_5
R : Type u_6
A B C : Matrix m n α
inst✝¹ : DecidableEq n
inst✝ : MulZeroOneClass α
M : Matrix n n α
i j : n
h : i = j
⊢ (M ⊙ 1) i j = diagonal (fun i => M i i) i j
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
m : Type u_4
n : Type u_5
R : Type u_6
A B C : Matrix m n α
inst✝¹ : DecidableEq n
inst✝ : MulZeroOneClass α
M : Matrix n n α
i j : n
h : ¬i = j
⊢ (M ⊙ 1) i j = diagonal (fun i => M i i) i j
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
m : Type u_4
n : Type u_5
R : Type u_6
A B C : Matrix m n α
inst✝¹ : DecidableEq n
inst✝ : MulZeroOneClass α
M : Matrix n n α
⊢ 1 ⊙ M = diagonal fun i => M i i
[PROOFSTEP]
ext i j
[GOAL]
case a.h
α : Type u_1
β : Type u_2
γ : Type u_3
m : Type u_4
n : Type u_5
R : Type u_6
A B C : Matrix m n α
inst✝¹ : DecidableEq n
inst✝ : MulZeroOneClass α
M : Matrix n n α
i j : n
⊢ (1 ⊙ M) i j = diagonal (fun i => M i i) i j
[PROOFSTEP]
by_cases h : i = j
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
m : Type u_4
n : Type u_5
R : Type u_6
A B C : Matrix m n α
inst✝¹ : DecidableEq n
inst✝ : MulZeroOneClass α
M : Matrix n n α
i j : n
h : i = j
⊢ (1 ⊙ M) i j = diagonal (fun i => M i i) i j
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
m : Type u_4
n : Type u_5
R : Type u_6
A B C : Matrix m n α
inst✝¹ : DecidableEq n
inst✝ : MulZeroOneClass α
M : Matrix n n α
i j : n
h : ¬i = j
⊢ (1 ⊙ M) i j = diagonal (fun i => M i i) i j
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
m : Type u_4
n : Type u_5
R : Type u_6
A B C : Matrix m n α
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Semiring α
inst✝³ : Semiring R
inst✝² : Module R α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
v : m → α
w : n → α
⊢ vecMul v (A ⊙ B) ⬝ᵥ w = trace (diagonal v * A * (B * diagonal w)ᵀ)
[PROOFSTEP]
rw [← sum_hadamard_eq, Finset.sum_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
m : Type u_4
n : Type u_5
R : Type u_6
A B C : Matrix m n α
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Semiring α
inst✝³ : Semiring R
inst✝² : Module R α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
v : m → α
w : n → α
⊢ vecMul v (A ⊙ B) ⬝ᵥ w = ∑ y : n, ∑ x : m, ((diagonal v * A) ⊙ (B * diagonal w)) x y
[PROOFSTEP]
simp [dotProduct, vecMul, Finset.sum_mul, mul_assoc]