[GOAL]
n : ℕ
α : Type u_1
v : List α
hv : List.length v = n
w : List α
hw : List.length w = n
h : ∀ (m : Fin n), get { val := v, property := hv } m = get { val := w, property := hw } m
⊢ List.length ↑{ val := v, property := hv } = List.length ↑{ val := w, property := hw }
[PROOFSTEP]
rw [hv, hw]
[GOAL]
n : ℕ
α : Type u_1
a : α
v : Vector α (Nat.succ n)
v' : Vector α n
h : head v = a ∧ tail v = v'
⊢ head v ::ᵥ tail v = a ::ᵥ v'
[PROOFSTEP]
rw [h.1, h.2]
[GOAL]
n : ℕ
α : Type u_1
a : α
v : Vector α (Nat.succ n)
v' : Vector α n
⊢ v ≠ a ::ᵥ v' ↔ head v ≠ a ∨ tail v ≠ v'
[PROOFSTEP]
rw [Ne.def, eq_cons_iff a v v', not_and_or]
[GOAL]
n✝ : ℕ
α : Type u_1
n : ℕ
f : Fin (n + 1) → α
⊢ toList (ofFn f) = List.ofFn f
[PROOFSTEP]
rw [ofFn, List.ofFn_succ, toList_cons, toList_ofFn]
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
v : Vector α n
f : α → β
⊢ toList (map f v) = List.map f (toList v)
[PROOFSTEP]
cases v
[GOAL]
case mk
n : ℕ
α : Type u_1
β : Type u_2
f : α → β
val✝ : List α
property✝ : List.length val✝ = n
⊢ toList (map f { val := val✝, property := property✝ }) = List.map f (toList { val := val✝, property := property✝ })
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
v : Vector α (n + 1)
f : α → β
⊢ head (map f v) = f (head v)
[PROOFSTEP]
obtain ⟨a, v', h⟩ := Vector.exists_eq_cons v
[GOAL]
case intro.intro
n : ℕ
α : Type u_1
β : Type u_2
v : Vector α (n + 1)
f : α → β
a : α
v' : Vector α n
h : v = a ::ᵥ v'
⊢ head (map f v) = f (head v)
[PROOFSTEP]
rw [h, map_cons, head_cons, head_cons]
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
v : Vector α (n + 1)
f : α → β
⊢ tail (map f v) = map f (tail v)
[PROOFSTEP]
obtain ⟨a, v', h⟩ := Vector.exists_eq_cons v
[GOAL]
case intro.intro
n : ℕ
α : Type u_1
β : Type u_2
v : Vector α (n + 1)
f : α → β
a : α
v' : Vector α n
h : v = a ::ᵥ v'
⊢ tail (map f v) = map f (tail v)
[PROOFSTEP]
rw [h, map_cons, tail_cons, tail_cons]
[GOAL]
n : ℕ
α : Type u_1
v : Vector α n
i : Fin n
⊢ ↑i < List.length (toList v)
[PROOFSTEP]
rw [toList_length]
[GOAL]
n : ℕ
α : Type u_1
v : Vector α n
i : Fin n
⊢ ↑i < n
[PROOFSTEP]
exact i.2
[GOAL]
n : ℕ
α : Type u_1
a : α
i : Fin n
⊢ get (replicate n a) i = a
[PROOFSTEP]
apply List.get_replicate
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
v : Vector α n
f : α → β
i : Fin n
⊢ get (map f v) i = f (get v i)
[PROOFSTEP]
cases v
[GOAL]
case mk
n : ℕ
α : Type u_1
β : Type u_2
f : α → β
i : Fin n
val✝ : List α
property✝ : List.length val✝ = n
⊢ get (map f { val := val✝, property := property✝ }) i = f (get { val := val✝, property := property✝ } i)
[PROOFSTEP]
simp [Vector.map, get_eq_get]
[GOAL]
case mk
n : ℕ
α : Type u_1
β : Type u_2
f : α → β
i : Fin n
val✝ : List α
property✝ : List.length val✝ = n
⊢ f (List.get val✝ { val := ↑i, isLt := (_ : ↑i < List.length val✝) }) =
    f (List.get val✝ (↑(Fin.castIso (_ : n = List.length (toList { val := val✝, property := property✝ }))) i))
[PROOFSTEP]
rfl
[GOAL]
n✝ : ℕ
α : Type u_1
n : ℕ
f : Fin n → α
i : Fin n
⊢ get (ofFn f) i = f i
[PROOFSTEP]
conv_rhs => erw [← List.get_ofFn f ⟨i, by simp⟩]
[GOAL]
n✝ : ℕ
α : Type u_1
n : ℕ
f : Fin n → α
i : Fin n
| f i
[PROOFSTEP]
erw [← List.get_ofFn f ⟨i, by simp⟩]
[GOAL]
n✝ : ℕ
α : Type u_1
n : ℕ
f : Fin n → α
i : Fin n
| f i
[PROOFSTEP]
erw [← List.get_ofFn f ⟨i, by simp⟩]
[GOAL]
n✝ : ℕ
α : Type u_1
n : ℕ
f : Fin n → α
i : Fin n
| f i
[PROOFSTEP]
erw [← List.get_ofFn f ⟨i, by simp⟩]
[GOAL]
n✝ : ℕ
α : Type u_1
n : ℕ
f : Fin n → α
i : Fin n
⊢ ↑i < List.length (List.ofFn f)
[PROOFSTEP]
simp
[GOAL]
n✝ : ℕ
α : Type u_1
n : ℕ
f : Fin n → α
i : Fin n
⊢ get (ofFn f) i = List.get (List.ofFn f) { val := ↑i, isLt := (_ : ↑i < List.length (List.ofFn f)) }
[PROOFSTEP]
simp only [get_eq_get]
[GOAL]
n✝ : ℕ
α : Type u_1
n : ℕ
f : Fin n → α
i : Fin n
⊢ List.get (toList (ofFn f)) (↑(Fin.castIso (_ : n = List.length (toList (ofFn f)))) i) =
    List.get (List.ofFn f) { val := ↑i, isLt := (_ : ↑i < List.length (List.ofFn f)) }
[PROOFSTEP]
congr
[GOAL]
case h.e_2.h
n✝ : ℕ
α : Type u_1
n : ℕ
f : Fin n → α
i : Fin n
⊢ toList (ofFn f) = List.ofFn f
[PROOFSTEP]
simp [Fin.heq_ext_iff]
[GOAL]
case h.e_3
n✝ : ℕ
α : Type u_1
n : ℕ
f : Fin n → α
i : Fin n
⊢ HEq (↑(Fin.castIso (_ : n = List.length (toList (ofFn f)))) i)
    { val := ↑i, isLt := (_ : ↑i < List.length (List.ofFn f)) }
[PROOFSTEP]
simp [Fin.heq_ext_iff]
[GOAL]
n : ℕ
α : Type u_1
v : Vector α n
⊢ ofFn (get v) = v
[PROOFSTEP]
rcases v with ⟨l, rfl⟩
[GOAL]
case mk
α : Type u_1
l : List α
⊢ ofFn (get { val := l, property := (_ : List.length l = List.length l) }) =
    { val := l, property := (_ : List.length l = List.length l) }
[PROOFSTEP]
apply toList_injective
[GOAL]
case mk.a
α : Type u_1
l : List α
⊢ toList (ofFn (get { val := l, property := (_ : List.length l = List.length l) })) =
    toList { val := l, property := (_ : List.length l = List.length l) }
[PROOFSTEP]
dsimp
[GOAL]
case mk.a
α : Type u_1
l : List α
⊢ toList (ofFn (get { val := l, property := (_ : List.length l = List.length l) })) = l
[PROOFSTEP]
simpa only [toList_ofFn] using List.ofFn_get _
[GOAL]
n : ℕ
α : Type u_1
x : Vector α n
i : Fin (n - 1)
⊢ get (tail x) i = get x { val := ↑i + 1, isLt := (_ : ↑i + 1 < n) }
[PROOFSTEP]
cases' i with i ih
[GOAL]
case mk
n : ℕ
α : Type u_1
x : Vector α n
i : ℕ
ih : i < n - 1
⊢ get (tail x) { val := i, isLt := ih } =
    get x { val := ↑{ val := i, isLt := ih } + 1, isLt := (_ : ↑{ val := i, isLt := ih } + 1 < n) }
[PROOFSTEP]
dsimp
[GOAL]
case mk
n : ℕ
α : Type u_1
x : Vector α n
i : ℕ
ih : i < n - 1
⊢ get (tail x) { val := i, isLt := ih } = get x { val := i + 1, isLt := (_ : i + 1 < n) }
[PROOFSTEP]
rcases x with ⟨_ | _, h⟩
[GOAL]
case mk.mk.nil
n : ℕ
α : Type u_1
i : ℕ
ih : i < n - 1
h : List.length [] = n
⊢ get (tail { val := [], property := h }) { val := i, isLt := ih } =
    get { val := [], property := h } { val := i + 1, isLt := (_ : i + 1 < n) }
[PROOFSTEP]
try rfl
[GOAL]
case mk.mk.nil
n : ℕ
α : Type u_1
i : ℕ
ih : i < n - 1
h : List.length [] = n
⊢ get (tail { val := [], property := h }) { val := i, isLt := ih } =
    get { val := [], property := h } { val := i + 1, isLt := (_ : i + 1 < n) }
[PROOFSTEP]
rfl
[GOAL]
case mk.mk.cons
n : ℕ
α : Type u_1
i : ℕ
ih : i < n - 1
head✝ : α
tail✝ : List α
h : List.length (head✝ :: tail✝) = n
⊢ get (tail { val := head✝ :: tail✝, property := h }) { val := i, isLt := ih } =
    get { val := head✝ :: tail✝, property := h } { val := i + 1, isLt := (_ : i + 1 < n) }
[PROOFSTEP]
try rfl
[GOAL]
case mk.mk.cons
n : ℕ
α : Type u_1
i : ℕ
ih : i < n - 1
head✝ : α
tail✝ : List α
h : List.length (head✝ :: tail✝) = n
⊢ get (tail { val := head✝ :: tail✝, property := h }) { val := i, isLt := ih } =
    get { val := head✝ :: tail✝, property := h } { val := i + 1, isLt := (_ : i + 1 < n) }
[PROOFSTEP]
rfl
[GOAL]
case mk.mk.nil
n : ℕ
α : Type u_1
i : ℕ
ih : i < n - 1
h : List.length [] = n
⊢ get (tail { val := [], property := h }) { val := i, isLt := ih } =
    get { val := [], property := h } { val := i + 1, isLt := (_ : i + 1 < n) }
[PROOFSTEP]
rw [List.length] at h
[GOAL]
case mk.mk.nil
n : ℕ
α : Type u_1
i : ℕ
ih : i < n - 1
h✝ : List.length [] = n
h : 0 = n
⊢ get (tail { val := [], property := h✝ }) { val := i, isLt := ih } =
    get { val := [], property := h✝ } { val := i + 1, isLt := (_ : i + 1 < n) }
[PROOFSTEP]
rw [← h] at ih
[GOAL]
case mk.mk.nil
n : ℕ
α : Type u_1
i : ℕ
ih✝ : i < n - 1
ih : i < 0 - 1
h✝ : List.length [] = n
h : 0 = n
⊢ get (tail { val := [], property := h✝ }) { val := i, isLt := ih✝ } =
    get { val := [], property := h✝ } { val := i + 1, isLt := (_ : i + 1 < n) }
[PROOFSTEP]
contradiction
[GOAL]
n : ℕ
α : Type u_1
a : α
l : List α
e : List.length (a :: l) = Nat.succ n
i : ℕ
h : i < n
⊢ get (tail { val := a :: l, property := e }) { val := i, isLt := h } =
    get { val := a :: l, property := e } (Fin.succ { val := i, isLt := h })
[PROOFSTEP]
simp [get_eq_get]
[GOAL]
n : ℕ
α : Type u_1
a : α
l : List α
e : List.length (a :: l) = Nat.succ n
i : ℕ
h : i < n
⊢ List.get (toList (tail { val := a :: l, property := e }))
      { val := i, isLt := (_ : i < List.length (toList (tail { val := a :: l, property := e }))) } =
    List.get l { val := i, isLt := (_ : i < List.length l) }
[PROOFSTEP]
rfl
[GOAL]
n✝ : ℕ
α : Type u_1
n : ℕ
f : Fin (Nat.succ n) → α
⊢ ofFn (get (tail (ofFn f))) = ofFn fun i => f (Fin.succ i)
[PROOFSTEP]
congr
[GOAL]
case e_a
n✝ : ℕ
α : Type u_1
n : ℕ
f : Fin (Nat.succ n) → α
⊢ get (tail (ofFn f)) = fun i => f (Fin.succ i)
[PROOFSTEP]
funext i
[GOAL]
case e_a.h
n✝ : ℕ
α : Type u_1
n : ℕ
f : Fin (Nat.succ n) → α
i : Fin (Nat.succ n - 1)
⊢ get (tail (ofFn f)) i = f (Fin.succ i)
[PROOFSTEP]
rw [get_tail, get_ofFn]
[GOAL]
case e_a.h
n✝ : ℕ
α : Type u_1
n : ℕ
f : Fin (Nat.succ n) → α
i : Fin (Nat.succ n - 1)
⊢ f { val := ↑i + 1, isLt := (_ : ↑i + 1 < Nat.succ n) } = f (Fin.succ i)
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
α : Type u_1
v : Vector α 1
⊢ toList v = [head v]
[PROOFSTEP]
rw [← v.cons_head_tail]
[GOAL]
n : ℕ
α : Type u_1
v : Vector α 1
⊢ toList (head v ::ᵥ tail v) = [head (head v ::ᵥ tail v)]
[PROOFSTEP]
simp only [toList_cons, toList_nil, head_cons, eq_self_iff_true, and_self_iff, singleton_tail]
[GOAL]
n : ℕ
α : Type u_1
v : Vector α (n + 1)
⊢ ¬List.isEmpty (toList v) = true
[PROOFSTEP]
simp only [empty_toList_eq_ff, Bool.coe_sort_false, not_false_iff]
[GOAL]
n✝ : ℕ
α : Type u_1
n : ℕ
v : Vector α n
⊢ toList (map id v) = toList v
[PROOFSTEP]
simp only [List.map_id, Vector.toList_map]
[GOAL]
n : ℕ
α : Type u_1
v : Vector α n
⊢ List.Nodup (toList v) ↔ Function.Injective (get v)
[PROOFSTEP]
cases' v with l hl
[GOAL]
case mk
n : ℕ
α : Type u_1
l : List α
hl : List.length l = n
⊢ List.Nodup (toList { val := l, property := hl }) ↔ Function.Injective (get { val := l, property := hl })
[PROOFSTEP]
subst hl
[GOAL]
case mk
α : Type u_1
l : List α
⊢ List.Nodup (toList { val := l, property := (_ : List.length l = List.length l) }) ↔
    Function.Injective (get { val := l, property := (_ : List.length l = List.length l) })
[PROOFSTEP]
exact List.nodup_iff_injective_get
[GOAL]
n : ℕ
α : Type u_1
v : Vector α n
⊢ List.length (List.reverse (toList v)) = n
[PROOFSTEP]
simp
[GOAL]
n : ℕ
α : Type u_1
v : Vector α n
⊢ reverse (reverse v) = v
[PROOFSTEP]
cases v
[GOAL]
case mk
n : ℕ
α : Type u_1
val✝ : List α
property✝ : List.length val✝ = n
⊢ reverse (reverse { val := val✝, property := property✝ }) = { val := val✝, property := property✝ }
[PROOFSTEP]
simp [Vector.reverse]
[GOAL]
n✝ : ℕ
α : Type u_1
n : ℕ
f : Fin (Nat.succ n) → α
⊢ head (ofFn f) = f 0
[PROOFSTEP]
rw [← get_zero, get_ofFn]
[GOAL]
n : ℕ
α : Type u_1
a : α
v : Vector α n
⊢ get (a ::ᵥ v) 0 = a
[PROOFSTEP]
simp [get_zero]
[GOAL]
n : ℕ
α : Type u_1
a : α
v : Vector α n
i : Fin n
⊢ get (a ::ᵥ v) (Fin.succ i) = get v i
[PROOFSTEP]
rw [← get_tail_succ, tail_cons]
[GOAL]
n : ℕ
α : Type u_1
v : Vector α (n + 1)
⊢ head (reverse v) = last v
[PROOFSTEP]
rw [← get_zero, last_def, get_eq_get, get_eq_get]
[GOAL]
n : ℕ
α : Type u_1
v : Vector α (n + 1)
⊢ List.get (toList (reverse v)) (↑(Fin.castIso (_ : Nat.succ n = List.length (toList (reverse v)))) 0) =
    List.get (toList v) (↑(Fin.castIso (_ : n + 1 = List.length (toList v))) (Fin.last n))
[PROOFSTEP]
simp_rw [toList_reverse]
[GOAL]
n : ℕ
α : Type u_1
v : Vector α (n + 1)
⊢ List.get (List.reverse (toList v)) (↑(Fin.castIso (_ : Nat.succ n = List.length (toList (reverse v)))) 0) =
    List.get (toList v) (↑(Fin.castIso (_ : n + 1 = List.length (toList v))) (Fin.last n))
[PROOFSTEP]
rw [← Option.some_inj, ← List.get?_eq_get, ← List.get?_eq_get, List.get?_reverse]
[GOAL]
n : ℕ
α : Type u_1
v : Vector α (n + 1)
⊢ List.get? (toList v)
      (List.length (toList v) - 1 - ↑(↑(Fin.castIso (_ : Nat.succ n = List.length (toList (reverse v)))) 0)) =
    List.get? (toList v) ↑(↑(Fin.castIso (_ : n + 1 = List.length (toList v))) (Fin.last n))
[PROOFSTEP]
congr
[GOAL]
case e_a
n : ℕ
α : Type u_1
v : Vector α (n + 1)
⊢ List.length (toList v) - 1 - ↑(↑(Fin.castIso (_ : Nat.succ n = List.length (toList (reverse v)))) 0) =
    ↑(↑(Fin.castIso (_ : n + 1 = List.length (toList v))) (Fin.last n))
[PROOFSTEP]
simp
[GOAL]
case h
n : ℕ
α : Type u_1
v : Vector α (n + 1)
⊢ ↑(↑(Fin.castIso (_ : Nat.succ n = List.length (toList (reverse v)))) 0) < List.length (toList v)
[PROOFSTEP]
simp
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
f : β → α → β
b : β
v : Vector α n
⊢ List.length (List.scanl f b (toList v)) = n + 1
[PROOFSTEP]
rw [List.length_scanl, toList_length]
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
f : β → α → β
b : β
v : Vector α n
x : α
⊢ scanl f b (x ::ᵥ v) = b ::ᵥ scanl f (f b x) v
[PROOFSTEP]
simp only [scanl, toList_cons, List.scanl]
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
f : β → α → β
b : β
v : Vector α n
x : α
⊢ { val := b :: List.scanl f (f b x) ↑v,
      property := (_ : (fun l => List.length l = Nat.succ n + 1) (b :: List.scanl f (f b x) ↑v)) } =
    b ::ᵥ
      { val := List.scanl f (f b x) (toList v),
        property := (_ : List.length (List.scanl f (f b x) (toList v)) = n + 1) }
[PROOFSTEP]
dsimp
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
f : β → α → β
b : β
v : Vector α n
x : α
⊢ { val := b :: List.scanl f (f b x) ↑v,
      property := (_ : List.length (List.scanl f b (toList (x ::ᵥ v))) = Nat.succ n + 1) } =
    b ::ᵥ
      { val := List.scanl f (f b x) (toList v),
        property := (_ : List.length (List.scanl f (f b x) (toList v)) = n + 1) }
[PROOFSTEP]
simp only [cons]
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
f : β → α → β
b : β
v : Vector α n
x : α
⊢ { val := b :: List.scanl f (f b x) ↑v,
      property := (_ : List.length (List.scanl f b (toList (x ::ᵥ v))) = Nat.succ n + 1) } =
    { val := b :: List.scanl f (f b x) (toList v),
      property := (_ : Nat.succ (List.length (List.scanl f (f b x) (toList v))) = Nat.succ (n + 1)) }
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
f : β → α → β
b : β
v✝ : Vector α n
v : Vector α 1
⊢ scanl f b v = b ::ᵥ f b (head v) ::ᵥ nil
[PROOFSTEP]
rw [← cons_head_tail v]
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
f : β → α → β
b : β
v✝ : Vector α n
v : Vector α 1
⊢ scanl f b (head v ::ᵥ tail v) = b ::ᵥ f b (head (head v ::ᵥ tail v)) ::ᵥ nil
[PROOFSTEP]
simp only [scanl_cons, scanl_nil, head_cons, singleton_tail]
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
f : β → α → β
b : β
v : Vector α n
⊢ head (scanl f b v) = b
[PROOFSTEP]
cases n
[GOAL]
case zero
α : Type u_1
β : Type u_2
f : β → α → β
b : β
v : Vector α Nat.zero
⊢ head (scanl f b v) = b
[PROOFSTEP]
have : v = nil := by simp only [Nat.zero_eq, eq_iff_true_of_subsingleton]
[GOAL]
α : Type u_1
β : Type u_2
f : β → α → β
b : β
v : Vector α Nat.zero
⊢ v = nil
[PROOFSTEP]
simp only [Nat.zero_eq, eq_iff_true_of_subsingleton]
[GOAL]
case zero
α : Type u_1
β : Type u_2
f : β → α → β
b : β
v : Vector α Nat.zero
this : v = nil
⊢ head (scanl f b v) = b
[PROOFSTEP]
simp only [this, scanl_nil, head_cons]
[GOAL]
case succ
α : Type u_1
β : Type u_2
f : β → α → β
b : β
n✝ : ℕ
v : Vector α (Nat.succ n✝)
⊢ head (scanl f b v) = b
[PROOFSTEP]
rw [← cons_head_tail v]
[GOAL]
case succ
α : Type u_1
β : Type u_2
f : β → α → β
b : β
n✝ : ℕ
v : Vector α (Nat.succ n✝)
⊢ head (scanl f b (head v ::ᵥ tail v)) = b
[PROOFSTEP]
simp only [← get_zero, get_eq_get, toList_scanl, toList_cons, List.scanl, Fin.val_zero, List.get]
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
f : β → α → β
b : β
v : Vector α n
i : Fin n
⊢ get (scanl f b v) (Fin.succ i) = f (get (scanl f b v) (Fin.castSucc i)) (get v i)
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
α : Type u_1
β : Type u_2
f : β → α → β
b : β
v : Vector α Nat.zero
i : Fin Nat.zero
⊢ get (scanl f b v) (Fin.succ i) = f (get (scanl f b v) (Fin.castSucc i)) (get v i)
[PROOFSTEP]
exact i.elim0
[GOAL]
case succ
α : Type u_1
β : Type u_2
f : β → α → β
b : β
n : ℕ
v : Vector α (Nat.succ n)
i : Fin (Nat.succ n)
⊢ get (scanl f b v) (Fin.succ i) = f (get (scanl f b v) (Fin.castSucc i)) (get v i)
[PROOFSTEP]
induction' n with n hn generalizing b
[GOAL]
case succ.zero
α : Type u_1
β : Type u_2
f : β → α → β
b✝ : β
n : ℕ
v✝ : Vector α (Nat.succ n)
i✝ : Fin (Nat.succ n)
b : β
v : Vector α (Nat.succ Nat.zero)
i : Fin (Nat.succ Nat.zero)
⊢ get (scanl f b v) (Fin.succ i) = f (get (scanl f b v) (Fin.castSucc i)) (get v i)
[PROOFSTEP]
have i0 : i = 0 := Fin.eq_zero _
[GOAL]
case succ.zero
α : Type u_1
β : Type u_2
f : β → α → β
b✝ : β
n : ℕ
v✝ : Vector α (Nat.succ n)
i✝ : Fin (Nat.succ n)
b : β
v : Vector α (Nat.succ Nat.zero)
i : Fin (Nat.succ Nat.zero)
i0 : i = 0
⊢ get (scanl f b v) (Fin.succ i) = f (get (scanl f b v) (Fin.castSucc i)) (get v i)
[PROOFSTEP]
simp [scanl_singleton, i0, get_zero]
[GOAL]
case succ.zero
α : Type u_1
β : Type u_2
f : β → α → β
b✝ : β
n : ℕ
v✝ : Vector α (Nat.succ n)
i✝ : Fin (Nat.succ n)
b : β
v : Vector α (Nat.succ Nat.zero)
i : Fin (Nat.succ Nat.zero)
i0 : i = 0
⊢ get (b ::ᵥ f b (head v) ::ᵥ nil) 1 = f b (head v)
[PROOFSTEP]
simp [get_eq_get]
[GOAL]
case succ.succ
α : Type u_1
β : Type u_2
f : β → α → β
b✝ : β
n✝ : ℕ
v✝ : Vector α (Nat.succ n✝)
i✝ : Fin (Nat.succ n✝)
n : ℕ
hn :
  ∀ (b : β) (v : Vector α (Nat.succ n)) (i : Fin (Nat.succ n)),
    get (scanl f b v) (Fin.succ i) = f (get (scanl f b v) (Fin.castSucc i)) (get v i)
b : β
v : Vector α (Nat.succ (Nat.succ n))
i : Fin (Nat.succ (Nat.succ n))
⊢ get (scanl f b v) (Fin.succ i) = f (get (scanl f b v) (Fin.castSucc i)) (get v i)
[PROOFSTEP]
rw [← cons_head_tail v, scanl_cons, get_cons_succ]
[GOAL]
case succ.succ
α : Type u_1
β : Type u_2
f : β → α → β
b✝ : β
n✝ : ℕ
v✝ : Vector α (Nat.succ n✝)
i✝ : Fin (Nat.succ n✝)
n : ℕ
hn :
  ∀ (b : β) (v : Vector α (Nat.succ n)) (i : Fin (Nat.succ n)),
    get (scanl f b v) (Fin.succ i) = f (get (scanl f b v) (Fin.castSucc i)) (get v i)
b : β
v : Vector α (Nat.succ (Nat.succ n))
i : Fin (Nat.succ (Nat.succ n))
⊢ get (scanl f (f b (head v)) (tail v)) i =
    f (get (b ::ᵥ scanl f (f b (head v)) (tail v)) (Fin.castSucc i)) (get (head v ::ᵥ tail v) i)
[PROOFSTEP]
refine' Fin.cases _ _ i
[GOAL]
case succ.succ.refine'_1
α : Type u_1
β : Type u_2
f : β → α → β
b✝ : β
n✝ : ℕ
v✝ : Vector α (Nat.succ n✝)
i✝ : Fin (Nat.succ n✝)
n : ℕ
hn :
  ∀ (b : β) (v : Vector α (Nat.succ n)) (i : Fin (Nat.succ n)),
    get (scanl f b v) (Fin.succ i) = f (get (scanl f b v) (Fin.castSucc i)) (get v i)
b : β
v : Vector α (Nat.succ (Nat.succ n))
i : Fin (Nat.succ (Nat.succ n))
⊢ get (scanl f (f b (head v)) (tail v)) 0 =
    f (get (b ::ᵥ scanl f (f b (head v)) (tail v)) (Fin.castSucc 0)) (get (head v ::ᵥ tail v) 0)
[PROOFSTEP]
simp only [get_zero, scanl_head, Fin.castSucc_zero, head_cons]
[GOAL]
case succ.succ.refine'_2
α : Type u_1
β : Type u_2
f : β → α → β
b✝ : β
n✝ : ℕ
v✝ : Vector α (Nat.succ n✝)
i✝ : Fin (Nat.succ n✝)
n : ℕ
hn :
  ∀ (b : β) (v : Vector α (Nat.succ n)) (i : Fin (Nat.succ n)),
    get (scanl f b v) (Fin.succ i) = f (get (scanl f b v) (Fin.castSucc i)) (get v i)
b : β
v : Vector α (Nat.succ (Nat.succ n))
i : Fin (Nat.succ (Nat.succ n))
⊢ ∀ (i : Fin (n + 1)),
    get (scanl f (f b (head v)) (tail v)) (Fin.succ i) =
      f (get (b ::ᵥ scanl f (f b (head v)) (tail v)) (Fin.castSucc (Fin.succ i))) (get (head v ::ᵥ tail v) (Fin.succ i))
[PROOFSTEP]
intro i'
[GOAL]
case succ.succ.refine'_2
α : Type u_1
β : Type u_2
f : β → α → β
b✝ : β
n✝ : ℕ
v✝ : Vector α (Nat.succ n✝)
i✝ : Fin (Nat.succ n✝)
n : ℕ
hn :
  ∀ (b : β) (v : Vector α (Nat.succ n)) (i : Fin (Nat.succ n)),
    get (scanl f b v) (Fin.succ i) = f (get (scanl f b v) (Fin.castSucc i)) (get v i)
b : β
v : Vector α (Nat.succ (Nat.succ n))
i : Fin (Nat.succ (Nat.succ n))
i' : Fin (n + 1)
⊢ get (scanl f (f b (head v)) (tail v)) (Fin.succ i') =
    f (get (b ::ᵥ scanl f (f b (head v)) (tail v)) (Fin.castSucc (Fin.succ i'))) (get (head v ::ᵥ tail v) (Fin.succ i'))
[PROOFSTEP]
simp only [hn, Fin.castSucc_fin_succ, get_cons_succ]
[GOAL]
n✝ : ℕ
α✝ : Type u_1
m : Type u_2 → Type u_3
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_2
n : ℕ
f : Fin (n + 1) → α
⊢ (mOfFn fun i => pure (f i)) = pure (ofFn f)
[PROOFSTEP]
rw [mOfFn, @mOfFn_pure m _ _ _ n _, ofFn]
[GOAL]
n✝ : ℕ
α✝ : Type u_1
m : Type u_2 → Type u_3
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_2
n : ℕ
f : Fin (n + 1) → α
⊢ (do
      let a ← pure (f 0)
      let v ← pure (ofFn fun i => f (Fin.succ i))
      pure (a ::ᵥ v)) =
    pure (f 0 ::ᵥ ofFn fun i => f (Fin.succ i))
[PROOFSTEP]
simp
[GOAL]
n✝ : ℕ
α : Type u_1
C : {n : ℕ} → Vector α n → Sort u_2
n : ℕ
v : Vector α n
h_nil : C nil
h_cons : {n : ℕ} → {x : α} → {w : Vector α n} → C w → C (x ::ᵥ w)
⊢ C v
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
n✝ : ℕ
α : Type u_1
C : {n : ℕ} → Vector α n → Sort u_2
n : ℕ
v✝ : Vector α n
h_nil : C nil
h_cons : {n : ℕ} → {x : α} → {w : Vector α n} → C w → C (x ::ᵥ w)
v : Vector α Nat.zero
⊢ C v
[PROOFSTEP]
rcases v with ⟨_ | ⟨-, -⟩, - | -⟩
[GOAL]
case zero.mk.nil.refl
n✝ : ℕ
α : Type u_1
C : {n : ℕ} → Vector α n → Sort u_2
n : ℕ
v : Vector α n
h_nil : C nil
h_cons : {n : ℕ} → {x : α} → {w : Vector α n} → C w → C (x ::ᵥ w)
⊢ C { val := [], property := (_ : List.length [] = List.length []) }
[PROOFSTEP]
exact h_nil
[GOAL]
case succ
n✝¹ : ℕ
α : Type u_1
C : {n : ℕ} → Vector α n → Sort u_2
n✝ : ℕ
v✝ : Vector α n✝
h_nil : C nil
h_cons : {n : ℕ} → {x : α} → {w : Vector α n} → C w → C (x ::ᵥ w)
n : ℕ
ih : (v : Vector α n) → C v
v : Vector α (Nat.succ n)
⊢ C v
[PROOFSTEP]
rcases v with ⟨_ | ⟨a, v⟩, v_property⟩
[GOAL]
case succ.mk.nil
n✝¹ : ℕ
α : Type u_1
C : {n : ℕ} → Vector α n → Sort u_2
n✝ : ℕ
v : Vector α n✝
h_nil : C nil
h_cons : {n : ℕ} → {x : α} → {w : Vector α n} → C w → C (x ::ᵥ w)
n : ℕ
ih : (v : Vector α n) → C v
v_property : List.length [] = Nat.succ n
⊢ C { val := [], property := v_property }
case succ.mk.cons
n✝¹ : ℕ
α : Type u_1
C : {n : ℕ} → Vector α n → Sort u_2
n✝ : ℕ
v✝ : Vector α n✝
h_nil : C nil
h_cons : {n : ℕ} → {x : α} → {w : Vector α n} → C w → C (x ::ᵥ w)
n : ℕ
ih : (v : Vector α n) → C v
a : α
v : List α
v_property : List.length (a :: v) = Nat.succ n
⊢ C { val := a :: v, property := v_property }
[PROOFSTEP]
cases v_property
[GOAL]
case succ.mk.cons
n✝¹ : ℕ
α : Type u_1
C : {n : ℕ} → Vector α n → Sort u_2
n✝ : ℕ
v✝ : Vector α n✝
h_nil : C nil
h_cons : {n : ℕ} → {x : α} → {w : Vector α n} → C w → C (x ::ᵥ w)
n : ℕ
ih : (v : Vector α n) → C v
a : α
v : List α
v_property : List.length (a :: v) = Nat.succ n
⊢ C { val := a :: v, property := v_property }
[PROOFSTEP]
apply @h_cons n _ ⟨v, (add_left_inj 1).mp v_property⟩
[GOAL]
case succ.mk.cons
n✝¹ : ℕ
α : Type u_1
C : {n : ℕ} → Vector α n → Sort u_2
n✝ : ℕ
v✝ : Vector α n✝
h_nil : C nil
h_cons : {n : ℕ} → {x : α} → {w : Vector α n} → C w → C (x ::ᵥ w)
n : ℕ
ih : (v : Vector α n) → C v
a : α
v : List α
v_property : List.length (a :: v) = Nat.succ n
⊢ C { val := v, property := (_ : List.length v = n) }
[PROOFSTEP]
apply ih
[GOAL]
n : ℕ
α : Type u_1
v : Vector α n
⊢ True
[PROOFSTEP]
induction v using Vector.inductionOn
[GOAL]
case h_nil
n : ℕ
α : Type u_1
⊢ True
[PROOFSTEP]
trivial
[GOAL]
case h_cons
n : ℕ
α : Type u_1
n✝ : ℕ
x✝ : α
w✝ : Vector α n✝
a✝ : True
⊢ True
[PROOFSTEP]
trivial
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Sort u_4
v : Vector α n
w : Vector β n
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
⊢ C v w
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Sort u_4
v✝ : Vector α n
w✝ : Vector β n
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
v : Vector α Nat.zero
w : Vector β Nat.zero
⊢ C v w
[PROOFSTEP]
rcases v with ⟨_ | ⟨-, -⟩, - | -⟩
[GOAL]
case zero.mk.nil.refl
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Sort u_4
v : Vector α n
w✝ : Vector β n
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
w : Vector β Nat.zero
⊢ C { val := [], property := (_ : List.length [] = List.length []) } w
[PROOFSTEP]
rcases w with ⟨_ | ⟨-, -⟩, - | -⟩
[GOAL]
case zero.mk.nil.refl.mk.nil.refl
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Sort u_4
v : Vector α n
w : Vector β n
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
⊢ C { val := [], property := (_ : List.length [] = List.length []) }
    { val := [], property := (_ : List.length [] = List.length []) }
[PROOFSTEP]
exact nil
[GOAL]
case succ
n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Sort u_4
v✝ : Vector α n✝
w✝ : Vector β n✝
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
n : ℕ
ih : (v : Vector α n) → (w : Vector β n) → C v w
v : Vector α (Nat.succ n)
w : Vector β (Nat.succ n)
⊢ C v w
[PROOFSTEP]
rcases v with ⟨_ | ⟨a, v⟩, v_property⟩
[GOAL]
case succ.mk.nil
n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Sort u_4
v : Vector α n✝
w✝ : Vector β n✝
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
n : ℕ
ih : (v : Vector α n) → (w : Vector β n) → C v w
w : Vector β (Nat.succ n)
v_property : List.length [] = Nat.succ n
⊢ C { val := [], property := v_property } w
case succ.mk.cons
n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Sort u_4
v✝ : Vector α n✝
w✝ : Vector β n✝
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
n : ℕ
ih : (v : Vector α n) → (w : Vector β n) → C v w
w : Vector β (Nat.succ n)
a : α
v : List α
v_property : List.length (a :: v) = Nat.succ n
⊢ C { val := a :: v, property := v_property } w
[PROOFSTEP]
cases v_property
[GOAL]
case succ.mk.cons
n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Sort u_4
v✝ : Vector α n✝
w✝ : Vector β n✝
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
n : ℕ
ih : (v : Vector α n) → (w : Vector β n) → C v w
w : Vector β (Nat.succ n)
a : α
v : List α
v_property : List.length (a :: v) = Nat.succ n
⊢ C { val := a :: v, property := v_property } w
[PROOFSTEP]
rcases w with ⟨_ | ⟨b, w⟩, w_property⟩
[GOAL]
case succ.mk.cons.mk.nil
n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Sort u_4
v✝ : Vector α n✝
w : Vector β n✝
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
n : ℕ
ih : (v : Vector α n) → (w : Vector β n) → C v w
a : α
v : List α
v_property : List.length (a :: v) = Nat.succ n
w_property : List.length [] = Nat.succ n
⊢ C { val := a :: v, property := v_property } { val := [], property := w_property }
case succ.mk.cons.mk.cons
n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Sort u_4
v✝ : Vector α n✝
w✝ : Vector β n✝
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
n : ℕ
ih : (v : Vector α n) → (w : Vector β n) → C v w
a : α
v : List α
v_property : List.length (a :: v) = Nat.succ n
b : β
w : List β
w_property : List.length (b :: w) = Nat.succ n
⊢ C { val := a :: v, property := v_property } { val := b :: w, property := w_property }
[PROOFSTEP]
cases w_property
[GOAL]
case succ.mk.cons.mk.cons
n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Sort u_4
v✝ : Vector α n✝
w✝ : Vector β n✝
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
n : ℕ
ih : (v : Vector α n) → (w : Vector β n) → C v w
a : α
v : List α
v_property : List.length (a :: v) = Nat.succ n
b : β
w : List β
w_property : List.length (b :: w) = Nat.succ n
⊢ C { val := a :: v, property := v_property } { val := b :: w, property := w_property }
[PROOFSTEP]
apply @cons n _ _ ⟨v, (add_left_inj 1).mp v_property⟩ ⟨w, (add_left_inj 1).mp w_property⟩
[GOAL]
case succ.mk.cons.mk.cons
n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Sort u_4
v✝ : Vector α n✝
w✝ : Vector β n✝
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
n : ℕ
ih : (v : Vector α n) → (w : Vector β n) → C v w
a : α
v : List α
v_property : List.length (a :: v) = Nat.succ n
b : β
w : List β
w_property : List.length (b :: w) = Nat.succ n
⊢ C { val := v, property := (_ : List.length v = n) } { val := w, property := (_ : List.length w = n) }
[PROOFSTEP]
apply ih
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_4
u : Vector α n
v : Vector β n
w : Vector γ n
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
⊢ C u v w
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_4
u✝ : Vector α n
v✝ : Vector β n
w✝ : Vector γ n
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
u : Vector α Nat.zero
v : Vector β Nat.zero
w : Vector γ Nat.zero
⊢ C u v w
[PROOFSTEP]
rcases u with ⟨_ | ⟨-, -⟩, - | -⟩
[GOAL]
case zero.mk.nil.refl
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_4
u : Vector α n
v✝ : Vector β n
w✝ : Vector γ n
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
v : Vector β Nat.zero
w : Vector γ Nat.zero
⊢ C { val := [], property := (_ : List.length [] = List.length []) } v w
[PROOFSTEP]
rcases v with ⟨_ | ⟨-, -⟩, - | -⟩
[GOAL]
case zero.mk.nil.refl.mk.nil.refl
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_4
u : Vector α n
v : Vector β n
w✝ : Vector γ n
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
w : Vector γ Nat.zero
⊢ C { val := [], property := (_ : List.length [] = List.length []) }
    { val := [], property := (_ : List.length [] = List.length []) } w
[PROOFSTEP]
rcases w with ⟨_ | ⟨-, -⟩, - | -⟩
[GOAL]
case zero.mk.nil.refl.mk.nil.refl.mk.nil.refl
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_4
u : Vector α n
v : Vector β n
w : Vector γ n
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
⊢ C { val := [], property := (_ : List.length [] = List.length []) }
    { val := [], property := (_ : List.length [] = List.length []) }
    { val := [], property := (_ : List.length [] = List.length []) }
[PROOFSTEP]
exact nil
[GOAL]
case succ
n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_4
u✝ : Vector α n✝
v✝ : Vector β n✝
w✝ : Vector γ n✝
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
n : ℕ
ih : (u : Vector α n) → (v : Vector β n) → (w : Vector γ n) → C u v w
u : Vector α (Nat.succ n)
v : Vector β (Nat.succ n)
w : Vector γ (Nat.succ n)
⊢ C u v w
[PROOFSTEP]
rcases u with ⟨_ | ⟨a, u⟩, u_property⟩
[GOAL]
case succ.mk.nil
n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_4
u : Vector α n✝
v✝ : Vector β n✝
w✝ : Vector γ n✝
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
n : ℕ
ih : (u : Vector α n) → (v : Vector β n) → (w : Vector γ n) → C u v w
v : Vector β (Nat.succ n)
w : Vector γ (Nat.succ n)
u_property : List.length [] = Nat.succ n
⊢ C { val := [], property := u_property } v w
case succ.mk.cons
n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_4
u✝ : Vector α n✝
v✝ : Vector β n✝
w✝ : Vector γ n✝
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
n : ℕ
ih : (u : Vector α n) → (v : Vector β n) → (w : Vector γ n) → C u v w
v : Vector β (Nat.succ n)
w : Vector γ (Nat.succ n)
a : α
u : List α
u_property : List.length (a :: u) = Nat.succ n
⊢ C { val := a :: u, property := u_property } v w
[PROOFSTEP]
cases u_property
[GOAL]
case succ.mk.cons
n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_4
u✝ : Vector α n✝
v✝ : Vector β n✝
w✝ : Vector γ n✝
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
n : ℕ
ih : (u : Vector α n) → (v : Vector β n) → (w : Vector γ n) → C u v w
v : Vector β (Nat.succ n)
w : Vector γ (Nat.succ n)
a : α
u : List α
u_property : List.length (a :: u) = Nat.succ n
⊢ C { val := a :: u, property := u_property } v w
[PROOFSTEP]
rcases v with ⟨_ | ⟨b, v⟩, v_property⟩
[GOAL]
case succ.mk.cons.mk.nil
n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_4
u✝ : Vector α n✝
v : Vector β n✝
w✝ : Vector γ n✝
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
n : ℕ
ih : (u : Vector α n) → (v : Vector β n) → (w : Vector γ n) → C u v w
w : Vector γ (Nat.succ n)
a : α
u : List α
u_property : List.length (a :: u) = Nat.succ n
v_property : List.length [] = Nat.succ n
⊢ C { val := a :: u, property := u_property } { val := [], property := v_property } w
case succ.mk.cons.mk.cons
n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_4
u✝ : Vector α n✝
v✝ : Vector β n✝
w✝ : Vector γ n✝
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
n : ℕ
ih : (u : Vector α n) → (v : Vector β n) → (w : Vector γ n) → C u v w
w : Vector γ (Nat.succ n)
a : α
u : List α
u_property : List.length (a :: u) = Nat.succ n
b : β
v : List β
v_property : List.length (b :: v) = Nat.succ n
⊢ C { val := a :: u, property := u_property } { val := b :: v, property := v_property } w
[PROOFSTEP]
cases v_property
[GOAL]
case succ.mk.cons.mk.cons
n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_4
u✝ : Vector α n✝
v✝ : Vector β n✝
w✝ : Vector γ n✝
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
n : ℕ
ih : (u : Vector α n) → (v : Vector β n) → (w : Vector γ n) → C u v w
w : Vector γ (Nat.succ n)
a : α
u : List α
u_property : List.length (a :: u) = Nat.succ n
b : β
v : List β
v_property : List.length (b :: v) = Nat.succ n
⊢ C { val := a :: u, property := u_property } { val := b :: v, property := v_property } w
[PROOFSTEP]
rcases w with ⟨_ | ⟨c, w⟩, w_property⟩
[GOAL]
case succ.mk.cons.mk.cons.mk.nil
n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_4
u✝ : Vector α n✝
v✝ : Vector β n✝
w : Vector γ n✝
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
n : ℕ
ih : (u : Vector α n) → (v : Vector β n) → (w : Vector γ n) → C u v w
a : α
u : List α
u_property : List.length (a :: u) = Nat.succ n
b : β
v : List β
v_property : List.length (b :: v) = Nat.succ n
w_property : List.length [] = Nat.succ n
⊢ C { val := a :: u, property := u_property } { val := b :: v, property := v_property }
    { val := [], property := w_property }
case succ.mk.cons.mk.cons.mk.cons
n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_4
u✝ : Vector α n✝
v✝ : Vector β n✝
w✝ : Vector γ n✝
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
n : ℕ
ih : (u : Vector α n) → (v : Vector β n) → (w : Vector γ n) → C u v w
a : α
u : List α
u_property : List.length (a :: u) = Nat.succ n
b : β
v : List β
v_property : List.length (b :: v) = Nat.succ n
c : γ
w : List γ
w_property : List.length (c :: w) = Nat.succ n
⊢ C { val := a :: u, property := u_property } { val := b :: v, property := v_property }
    { val := c :: w, property := w_property }
[PROOFSTEP]
cases w_property
[GOAL]
case succ.mk.cons.mk.cons.mk.cons
n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_4
u✝ : Vector α n✝
v✝ : Vector β n✝
w✝ : Vector γ n✝
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
n : ℕ
ih : (u : Vector α n) → (v : Vector β n) → (w : Vector γ n) → C u v w
a : α
u : List α
u_property : List.length (a :: u) = Nat.succ n
b : β
v : List β
v_property : List.length (b :: v) = Nat.succ n
c : γ
w : List γ
w_property : List.length (c :: w) = Nat.succ n
⊢ C { val := a :: u, property := u_property } { val := b :: v, property := v_property }
    { val := c :: w, property := w_property }
[PROOFSTEP]
apply
  @cons n _ _ _ ⟨u, (add_left_inj 1).mp u_property⟩ ⟨v, (add_left_inj 1).mp v_property⟩
    ⟨w, (add_left_inj 1).mp w_property⟩
[GOAL]
case succ.mk.cons.mk.cons.mk.cons
n✝ : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_4
u✝ : Vector α n✝
v✝ : Vector β n✝
w✝ : Vector γ n✝
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
n : ℕ
ih : (u : Vector α n) → (v : Vector β n) → (w : Vector γ n) → C u v w
a : α
u : List α
u_property : List.length (a :: u) = Nat.succ n
b : β
v : List β
v_property : List.length (b :: v) = Nat.succ n
c : γ
w : List γ
w_property : List.length (c :: w) = Nat.succ n
⊢ C { val := u, property := (_ : List.length u = n) } { val := v, property := (_ : List.length v = n) }
    { val := w, property := (_ : List.length w = n) }
[PROOFSTEP]
apply ih
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
xs : List α
property✝ : List.length xs = n
⊢ Array α = Array α
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ a : α
i : Fin (n + 1)
v : Vector α n
⊢ List.length (List.insertNth (↑i) a ↑v) = n + 1
[PROOFSTEP]
rw [List.length_insertNth, v.2]
[GOAL]
case a
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ a : α
i : Fin (n + 1)
v : Vector α n
⊢ ↑i ≤ List.length ↑v
[PROOFSTEP]
rw [v.2, ← Nat.succ_le_succ_iff]
[GOAL]
case a
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ a : α
i : Fin (n + 1)
v : Vector α n
⊢ Nat.succ ↑i ≤ Nat.succ n
[PROOFSTEP]
exact i.2
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
⊢ removeNth (Fin.succAbove { val := j, isLt := hj } { val := i, isLt := hi }) (insertNth a { val := j, isLt := hj } v) =
    insertNth a (Fin.predAbove { val := i, isLt := hi } { val := j, isLt := hj }) (removeNth { val := i, isLt := hi } v)
[PROOFSTEP]
dsimp [insertNth, removeNth, Fin.succAbove, Fin.predAbove]
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
⊢ {
      val :=
        List.removeNth (List.insertNth j a ↑v)
          ↑(if i < j then { val := i, isLt := (_ : i < Nat.succ (n + 1)) }
            else { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ (n + 1)) }),
      property :=
        (_ :
          List.length
              (List.removeNth (List.insertNth j a ↑v)
                ↑(if i < j then { val := i, isLt := (_ : i < Nat.succ (n + 1)) }
                  else { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ (n + 1)) })) =
            n + 1 + 1 - 1) } =
    {
      val :=
        List.insertNth
          (↑(if h : { val := i, isLt := (_ : i < Nat.succ (n + 1)) } < { val := j, isLt := hj } then
              Fin.pred { val := j, isLt := hj } (_ : { val := j, isLt := hj } ≠ 0)
            else { val := j, isLt := (_ : ↑{ val := j, isLt := hj } < n + 1) }))
          a
          ↑(match v with
            | { val := l, property := p } =>
              { val := List.removeNth l i,
                property := (_ : List.length (List.removeNth l ↑{ val := i, isLt := hi }) = n + 1 - 1) }),
      property :=
        (_ :
          List.length
              (List.insertNth
                (↑(if h : { val := i, isLt := (_ : i < Nat.succ (n + 1)) } < { val := j, isLt := hj } then
                    Fin.pred { val := j, isLt := hj } (_ : { val := j, isLt := hj } ≠ 0)
                  else { val := j, isLt := (_ : ↑{ val := j, isLt := hj } < n + 1) }))
                a
                ↑(match v with
                  | { val := l, property := p } =>
                    { val := List.removeNth l i,
                      property := (_ : List.length (List.removeNth l ↑{ val := i, isLt := hi }) = n + 1 - 1) })) =
            n + 1) }
[PROOFSTEP]
rw [Subtype.mk_eq_mk]
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
⊢ List.removeNth (List.insertNth j a ↑v)
      ↑(if i < j then { val := i, isLt := (_ : i < Nat.succ (n + 1)) }
        else { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ (n + 1)) }) =
    List.insertNth
      (↑(if h : { val := i, isLt := (_ : i < Nat.succ (n + 1)) } < { val := j, isLt := hj } then
          Fin.pred { val := j, isLt := hj } (_ : { val := j, isLt := hj } ≠ 0)
        else { val := j, isLt := (_ : ↑{ val := j, isLt := hj } < n + 1) }))
      a
      ↑(match v with
        | { val := l, property := p } =>
          { val := List.removeNth l i,
            property := (_ : List.length (List.removeNth l ↑{ val := i, isLt := hi }) = n + 1 - 1) })
[PROOFSTEP]
simp only [Fin.lt_iff_val_lt_val]
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
⊢ List.removeNth (List.insertNth j a ↑v)
      ↑(if i < j then { val := i, isLt := (_ : i < Nat.succ (n + 1)) }
        else { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ (n + 1)) }) =
    List.insertNth
      (↑(if h : i < j then Fin.pred { val := j, isLt := hj } (_ : { val := j, isLt := hj } ≠ 0)
        else { val := j, isLt := (_ : ↑{ val := j, isLt := hj } < n + 1) }))
      a
      ↑(match v with
        | { val := l, property := p } =>
          { val := List.removeNth l i,
            property := (_ : List.length (List.removeNth l ↑{ val := i, isLt := hi }) = n + 1 - 1) })
[PROOFSTEP]
split_ifs with hij
[GOAL]
case pos
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : i < j
⊢ List.removeNth (List.insertNth j a ↑v) ↑{ val := i, isLt := (_ : i < Nat.succ (n + 1)) } =
    List.insertNth (↑(Fin.pred { val := j, isLt := hj } (_ : { val := j, isLt := hj } ≠ 0))) a
      ↑(match v with
        | { val := l, property := p } =>
          { val := List.removeNth l i,
            property := (_ : List.length (List.removeNth l ↑{ val := i, isLt := hi }) = n + 1 - 1) })
[PROOFSTEP]
rcases Nat.exists_eq_succ_of_ne_zero (Nat.pos_iff_ne_zero.1 (lt_of_le_of_lt (Nat.zero_le _) hij)) with ⟨j, rfl⟩
[GOAL]
case pos.intro
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : Nat.succ j < n + 2
hij : i < Nat.succ j
⊢ List.removeNth (List.insertNth (Nat.succ j) a ↑v) ↑{ val := i, isLt := (_ : i < Nat.succ (n + 1)) } =
    List.insertNth (↑(Fin.pred { val := Nat.succ j, isLt := hj } (_ : { val := Nat.succ j, isLt := hj } ≠ 0))) a
      ↑(match v with
        | { val := l, property := p } =>
          { val := List.removeNth l i,
            property := (_ : List.length (List.removeNth l ↑{ val := i, isLt := hi }) = n + 1 - 1) })
[PROOFSTEP]
rw [← List.insertNth_removeNth_of_ge]
[GOAL]
case pos.intro
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : Nat.succ j < n + 2
hij : i < Nat.succ j
⊢ List.insertNth j a (List.removeNth ↑v ↑{ val := i, isLt := (_ : i < Nat.succ (n + 1)) }) =
    List.insertNth (↑(Fin.pred { val := Nat.succ j, isLt := hj } (_ : { val := Nat.succ j, isLt := hj } ≠ 0))) a
      ↑(match v with
        | { val := l, property := p } =>
          { val := List.removeNth l i,
            property := (_ : List.length (List.removeNth l ↑{ val := i, isLt := hi }) = n + 1 - 1) })
[PROOFSTEP]
simp
[GOAL]
case pos.intro
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : Nat.succ j < n + 2
hij : i < Nat.succ j
⊢ List.insertNth j a (List.removeNth (↑v) i) =
    List.insertNth j a
      ↑(match v with
        | { val := l, property := p } =>
          { val := List.removeNth l i,
            property := (_ : List.length (List.removeNth l ↑{ val := i, isLt := hi }) = n + 1 - 1) })
[PROOFSTEP]
rfl
[GOAL]
case pos.intro.a
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : Nat.succ j < n + 2
hij : i < Nat.succ j
⊢ ↑{ val := i, isLt := (_ : i < Nat.succ (n + 1)) } < List.length ↑v
[PROOFSTEP]
simpa
[GOAL]
case pos.intro.a
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : Nat.succ j < n + 2
hij : i < Nat.succ j
⊢ ↑{ val := i, isLt := (_ : i < Nat.succ (n + 1)) } ≤ j
[PROOFSTEP]
simpa [Nat.lt_succ_iff] using hij
[GOAL]
case neg
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ List.removeNth (List.insertNth j a ↑v) ↑{ val := i + 1, isLt := (_ : Nat.succ i < Nat.succ (n + 1)) } =
    List.insertNth (↑{ val := j, isLt := (_ : ↑{ val := j, isLt := hj } < n + 1) }) a
      ↑(match v with
        | { val := l, property := p } =>
          { val := List.removeNth l i,
            property := (_ : List.length (List.removeNth l ↑{ val := i, isLt := hi }) = n + 1 - 1) })
[PROOFSTEP]
dsimp
[GOAL]
case neg
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ List.removeNth (List.insertNth j a ↑v) (i + 1) =
    List.insertNth j a
      ↑(match v with
        | { val := l, property := p } =>
          { val := List.removeNth l i,
            property := (_ : List.length (List.removeNth l ↑{ val := i, isLt := hi }) = n + 1 - 1) })
[PROOFSTEP]
rw [← List.insertNth_removeNth_of_le i j _ _ _]
[GOAL]
case neg
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ List.insertNth j a (List.removeNth (↑v) i) =
    List.insertNth j a
      ↑(match v with
        | { val := l, property := p } =>
          { val := List.removeNth l i,
            property := (_ : List.length (List.removeNth l ↑{ val := i, isLt := hi }) = n + 1 - 1) })
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ i < List.length ↑v
[PROOFSTEP]
simpa
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ j ≤ i
[PROOFSTEP]
simpa [not_lt] using hij
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : List.length l = n
⊢ insertNth b (Fin.succ j) (insertNth a i { val := l, property := hl }) =
    insertNth a (Fin.castSucc i) (insertNth b j { val := l, property := hl })
[PROOFSTEP]
refine' Subtype.eq _
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : List.length l = n
⊢ ↑(insertNth b (Fin.succ j) (insertNth a i { val := l, property := hl })) =
    ↑(insertNth a (Fin.castSucc i) (insertNth b j { val := l, property := hl }))
[PROOFSTEP]
simp only [insertNth_val, Fin.val_succ, Fin.castSucc, Fin.coe_castAdd]
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : List.length l = n
⊢ List.insertNth (↑j + 1) b (List.insertNth (↑i) a l) = List.insertNth (↑i) a (List.insertNth (↑j) b l)
[PROOFSTEP]
apply List.insertNth_comm
[GOAL]
case x
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : List.length l = n
⊢ ↑i ≤ ↑j
[PROOFSTEP]
assumption
[GOAL]
case x
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : List.length l = n
⊢ ↑j ≤ List.length l
[PROOFSTEP]
rw [hl]
[GOAL]
case x
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a✝ a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : List.length l = n
⊢ ↑j ≤ n
[PROOFSTEP]
exact Nat.le_of_succ_le_succ j.2
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
v : Vector α n
i : Fin n
a : α
⊢ List.length (List.set (↑v) (↑i) a) = n
[PROOFSTEP]
simp
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
v : Vector α n
i : Fin n
a : α
⊢ get (set v i a) i = a
[PROOFSTEP]
cases v
[GOAL]
case mk
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
i : Fin n
a : α
val✝ : List α
property✝ : List.length val✝ = n
⊢ get (set { val := val✝, property := property✝ } i a) i = a
[PROOFSTEP]
cases i
[GOAL]
case mk.mk
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
val✝¹ : List α
property✝ : List.length val✝¹ = n
val✝ : ℕ
isLt✝ : val✝ < n
⊢ get (set { val := val✝¹, property := property✝ } { val := val✝, isLt := isLt✝ } a) { val := val✝, isLt := isLt✝ } = a
[PROOFSTEP]
simp [Vector.set, get_eq_get]
[GOAL]
case mk.mk
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
val✝¹ : List α
property✝ : List.length val✝¹ = n
val✝ : ℕ
isLt✝ : val✝ < n
⊢ List.get (List.set val✝¹ val✝ a)
      (↑(Fin.castIso
            (_ :
              n =
                List.length
                  (toList
                    { val := List.set val✝¹ val✝ a,
                      property :=
                        (_ :
                          List.length
                              (List.set (↑{ val := val✝¹, property := property✝ }) (↑{ val := val✝, isLt := isLt✝ })
                                a) =
                            n) })))
        { val := val✝, isLt := isLt✝ }) =
    a
[PROOFSTEP]
dsimp
[GOAL]
case mk.mk
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
val✝¹ : List α
property✝ : List.length val✝¹ = n
val✝ : ℕ
isLt✝ : val✝ < n
⊢ List.get (List.set val✝¹ val✝ a)
      (↑(Fin.castIso (_ : n = List.length (List.set val✝¹ val✝ a))) { val := val✝, isLt := isLt✝ }) =
    a
[PROOFSTEP]
exact List.get_set_eq _ _ _ _
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
v : Vector α n
i j : Fin n
h : i ≠ j
a : α
⊢ get (set v i a) j = get v j
[PROOFSTEP]
cases v
[GOAL]
case mk
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
i j : Fin n
h : i ≠ j
a : α
val✝ : List α
property✝ : List.length val✝ = n
⊢ get (set { val := val✝, property := property✝ } i a) j = get { val := val✝, property := property✝ } j
[PROOFSTEP]
cases i
[GOAL]
case mk.mk
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
j : Fin n
a : α
val✝¹ : List α
property✝ : List.length val✝¹ = n
val✝ : ℕ
isLt✝ : val✝ < n
h : { val := val✝, isLt := isLt✝ } ≠ j
⊢ get (set { val := val✝¹, property := property✝ } { val := val✝, isLt := isLt✝ } a) j =
    get { val := val✝¹, property := property✝ } j
[PROOFSTEP]
cases j
[GOAL]
case mk.mk.mk
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
val✝² : List α
property✝ : List.length val✝² = n
val✝¹ : ℕ
isLt✝¹ : val✝¹ < n
val✝ : ℕ
isLt✝ : val✝ < n
h : { val := val✝¹, isLt := isLt✝¹ } ≠ { val := val✝, isLt := isLt✝ }
⊢ get (set { val := val✝², property := property✝ } { val := val✝¹, isLt := isLt✝¹ } a) { val := val✝, isLt := isLt✝ } =
    get { val := val✝², property := property✝ } { val := val✝, isLt := isLt✝ }
[PROOFSTEP]
simp [Vector.set, Vector.get_eq_get, List.get_set_of_ne (Fin.vne_of_ne h)]
[GOAL]
case mk.mk.mk
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
val✝² : List α
property✝ : List.length val✝² = n
val✝¹ : ℕ
isLt✝¹ : val✝¹ < n
val✝ : ℕ
isLt✝ : val✝ < n
h : { val := val✝¹, isLt := isLt✝¹ } ≠ { val := val✝, isLt := isLt✝ }
⊢ List.get (List.set val✝² val✝¹ a)
      (↑(Fin.castIso
            (_ :
              n =
                List.length
                  (toList
                    { val := List.set val✝² val✝¹ a,
                      property :=
                        (_ :
                          List.length
                              (List.set (↑{ val := val✝², property := property✝ }) (↑{ val := val✝¹, isLt := isLt✝¹ })
                                a) =
                            n) })))
        { val := val✝, isLt := isLt✝ }) =
    List.get val✝²
      (↑(Fin.castIso (_ : n = List.length (toList { val := val✝², property := property✝ })))
        { val := val✝, isLt := isLt✝ })
[PROOFSTEP]
rw [List.get_set_of_ne]
[GOAL]
case mk.mk.mk
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
val✝² : List α
property✝ : List.length val✝² = n
val✝¹ : ℕ
isLt✝¹ : val✝¹ < n
val✝ : ℕ
isLt✝ : val✝ < n
h : { val := val✝¹, isLt := isLt✝¹ } ≠ { val := val✝, isLt := isLt✝ }
⊢ List.get val✝²
      {
        val :=
          ↑(↑(Fin.castIso
                  (_ :
                    n =
                      List.length
                        (toList
                          { val := List.set val✝² val✝¹ a,
                            property :=
                              (_ :
                                List.length
                                    (List.set (↑{ val := val✝², property := property✝ })
                                      (↑{ val := val✝¹, isLt := isLt✝¹ }) a) =
                                  n) })))
              { val := val✝, isLt := isLt✝ }),
        isLt :=
          (_ :
            ↑(↑(Fin.castIso
                      (_ :
                        n =
                          List.length
                            (toList
                              { val := List.set val✝² val✝¹ a,
                                property :=
                                  (_ :
                                    List.length
                                        (List.set (↑{ val := val✝², property := property✝ })
                                          (↑{ val := val✝¹, isLt := isLt✝¹ }) a) =
                                      n) })))
                  { val := val✝, isLt := isLt✝ }) <
              List.length val✝²) } =
    List.get val✝²
      (↑(Fin.castIso (_ : n = List.length (toList { val := val✝², property := property✝ })))
        { val := val✝, isLt := isLt✝ })
[PROOFSTEP]
rfl
[GOAL]
case mk.mk.mk.h
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
val✝² : List α
property✝ : List.length val✝² = n
val✝¹ : ℕ
isLt✝¹ : val✝¹ < n
val✝ : ℕ
isLt✝ : val✝ < n
h : { val := val✝¹, isLt := isLt✝¹ } ≠ { val := val✝, isLt := isLt✝ }
⊢ val✝¹ ≠
    ↑(↑(Fin.castIso
            (_ :
              n =
                List.length
                  (toList
                    { val := List.set val✝² val✝¹ a,
                      property :=
                        (_ :
                          List.length
                              (List.set (↑{ val := val✝², property := property✝ }) (↑{ val := val✝¹, isLt := isLt✝¹ })
                                a) =
                            n) })))
        { val := val✝, isLt := isLt✝ })
[PROOFSTEP]
simpa using h
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
v : Vector α n
i j : Fin n
a : α
⊢ get (set v i a) j = if i = j then a else get v j
[PROOFSTEP]
split_ifs
[GOAL]
case pos
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
v : Vector α n
i j : Fin n
a : α
h✝ : i = j
⊢ get (set v i a) j = a
[PROOFSTEP]
try simp [*]
[GOAL]
case pos
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
v : Vector α n
i j : Fin n
a : α
h✝ : i = j
⊢ get (set v i a) j = a
[PROOFSTEP]
simp [*]
[GOAL]
case neg
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
v : Vector α n
i j : Fin n
a : α
h✝ : ¬i = j
⊢ get (set v i a) j = get v j
[PROOFSTEP]
try simp [*]
[GOAL]
case neg
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
v : Vector α n
i j : Fin n
a : α
h✝ : ¬i = j
⊢ get (set v i a) j = get v j
[PROOFSTEP]
simp [*]
[GOAL]
case neg
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
v : Vector α n
i j : Fin n
a : α
h✝ : ¬i = j
⊢ get (set v i a) j = get v j
[PROOFSTEP]
rwa [get_set_of_ne]
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Monoid α
v : Vector α n
i : Fin n
a : α
⊢ List.prod (toList (set v i a)) = List.prod (toList (take (↑i) v)) * a * List.prod (toList (drop (↑i + 1) v))
[PROOFSTEP]
refine' (List.prod_set v.toList i a).trans _
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Monoid α
v : Vector α n
i : Fin n
a : α
⊢ (List.prod (List.take (↑i) (toList v)) * if ↑i < List.length (toList v) then a else 1) *
      List.prod (List.drop (↑i + 1) (toList v)) =
    List.prod (toList (take (↑i) v)) * a * List.prod (toList (drop (↑i + 1) v))
[PROOFSTEP]
simp_all
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CommGroup α
v : Vector α n
i : Fin n
a : α
⊢ List.prod (toList (set v i a)) = List.prod (toList v) * (get v i)⁻¹ * a
[PROOFSTEP]
refine' (List.prod_set' v.toList i a).trans _
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CommGroup α
v : Vector α n
i : Fin n
a : α
⊢ (List.prod (toList v) * if hn : ↑i < List.length (toList v) then (List.nthLe (toList v) (↑i) hn)⁻¹ * a else 1) =
    List.prod (toList v) * (get v i)⁻¹ * a
[PROOFSTEP]
simp [get_eq_get, mul_assoc]
[GOAL]
n : ℕ
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CommGroup α
v : Vector α n
i : Fin n
a : α
⊢ List.nthLe (toList v) ↑i (_ : ↑i < List.length (toList v)) =
    List.get (toList v) (↑(Fin.castIso (_ : n = List.length (toList v))) i)
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
F G : Type u → Type u
inst✝¹ : Applicative F
inst✝ : Applicative G
α β : Type u
f : α → F β
v : List α
Hv : List.length v = n
⊢ F (Vector β (List.length v)) = F (Vector β n)
[PROOFSTEP]
rw [Hv]
[GOAL]
n : ℕ
F G : Type u → Type u
inst✝¹ : Applicative F
inst✝ : Applicative G
α β : Type u
f : α → F β
x : α
⊢ ∀ (xs : Vector α n), Vector.traverse f (x ::ᵥ xs) = Seq.seq (cons <$> f x) fun x => Vector.traverse f xs
[PROOFSTEP]
rintro ⟨xs, rfl⟩
[GOAL]
case mk
F G : Type u → Type u
inst✝¹ : Applicative F
inst✝ : Applicative G
α β : Type u
f : α → F β
x : α
xs : List α
⊢ Vector.traverse f (x ::ᵥ { val := xs, property := (_ : List.length xs = List.length xs) }) =
    Seq.seq (cons <$> f x) fun x => Vector.traverse f { val := xs, property := (_ : List.length xs = List.length xs) }
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
F G : Type u → Type u
inst✝¹ : Applicative F
inst✝ : Applicative G
α β : Type u
⊢ ∀ (x : Vector α n), Vector.traverse pure x = x
[PROOFSTEP]
rintro ⟨x, rfl⟩
[GOAL]
case mk
F G : Type u → Type u
inst✝¹ : Applicative F
inst✝ : Applicative G
α β : Type u
x : List α
⊢ Vector.traverse pure { val := x, property := (_ : List.length x = List.length x) } =
    { val := x, property := (_ : List.length x = List.length x) }
[PROOFSTEP]
dsimp [Vector.traverse, cast]
[GOAL]
case mk
F G : Type u → Type u
inst✝¹ : Applicative F
inst✝ : Applicative G
α β : Type u
x : List α
⊢ Vector.traverseAux pure x = { val := x, property := (_ : List.length x = List.length x) }
[PROOFSTEP]
induction' x with x xs IH
[GOAL]
case mk.nil
F G : Type u → Type u
inst✝¹ : Applicative F
inst✝ : Applicative G
α β : Type u
⊢ Vector.traverseAux pure [] = { val := [], property := (_ : List.length [] = List.length []) }
[PROOFSTEP]
rfl
[GOAL]
case mk.cons
F G : Type u → Type u
inst✝¹ : Applicative F
inst✝ : Applicative G
α β : Type u
x : α
xs : List α
IH : Vector.traverseAux pure xs = { val := xs, property := (_ : List.length xs = List.length xs) }
⊢ Vector.traverseAux pure (x :: xs) =
    { val := x :: xs, property := (_ : List.length (x :: xs) = List.length (x :: xs)) }
[PROOFSTEP]
simp! [IH]
[GOAL]
case mk.cons
F G : Type u → Type u
inst✝¹ : Applicative F
inst✝ : Applicative G
α β : Type u
x : α
xs : List α
IH : Vector.traverseAux pure xs = { val := xs, property := (_ : List.length xs = List.length xs) }
⊢ (Seq.seq (cons x) fun x => { val := xs, property := (_ : List.length xs = List.length xs) }) =
    { val := x :: xs, property := (_ : List.length (x :: xs) = List.length (x :: xs)) }
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
x : Vector α n
⊢ Vector.traverse (Comp.mk ∘ Functor.map f ∘ g) x = Comp.mk (Vector.traverse f <$> Vector.traverse g x)
[PROOFSTEP]
induction' x using Vector.inductionOn with n x xs ih
[GOAL]
case h_nil
n : ℕ
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
⊢ Vector.traverse (Comp.mk ∘ Functor.map f ∘ g) nil = Comp.mk (Vector.traverse f <$> Vector.traverse g nil)
case h_cons
n✝ : ℕ
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
n : ℕ
x : α
xs : Vector α n
ih : Vector.traverse (Comp.mk ∘ Functor.map f ∘ g) xs = Comp.mk (Vector.traverse f <$> Vector.traverse g xs)
⊢ Vector.traverse (Comp.mk ∘ Functor.map f ∘ g) (x ::ᵥ xs) =
    Comp.mk (Vector.traverse f <$> Vector.traverse g (x ::ᵥ xs))
[PROOFSTEP]
simp! [cast, *, functor_norm]
[GOAL]
case h_nil
n : ℕ
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
⊢ pure nil = Comp.mk (pure (pure nil))
[PROOFSTEP]
rfl
[GOAL]
case h_cons
n✝ : ℕ
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
n : ℕ
x : α
xs : Vector α n
ih : Vector.traverse (Comp.mk ∘ Functor.map f ∘ g) xs = Comp.mk (Vector.traverse f <$> Vector.traverse g xs)
⊢ Vector.traverse (Comp.mk ∘ Functor.map f ∘ g) (x ::ᵥ xs) =
    Comp.mk (Vector.traverse f <$> Vector.traverse g (x ::ᵥ xs))
[PROOFSTEP]
rw [Vector.traverse_def, ih]
[GOAL]
case h_cons
n✝ : ℕ
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
n : ℕ
x : α
xs : Vector α n
ih : Vector.traverse (Comp.mk ∘ Functor.map f ∘ g) xs = Comp.mk (Vector.traverse f <$> Vector.traverse g xs)
⊢ (Seq.seq (cons <$> (Comp.mk ∘ Functor.map f ∘ g) x) fun x => Comp.mk (Vector.traverse f <$> Vector.traverse g xs)) =
    Comp.mk (Vector.traverse f <$> Vector.traverse g (x ::ᵥ xs))
[PROOFSTEP]
simp [functor_norm, (· ∘ ·)]
[GOAL]
n : ℕ
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α✝ β✝ γ : Type u
α β : Type u_1
f : α → β
⊢ ∀ (x : Vector α n), Vector.traverse (pure ∘ f) x = pure (map f x)
[PROOFSTEP]
rintro ⟨x, rfl⟩
[GOAL]
case mk
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α✝ β✝ γ : Type u
α β : Type u_1
f : α → β
x : List α
⊢ Vector.traverse (pure ∘ f) { val := x, property := (_ : List.length x = List.length x) } =
    pure (map f { val := x, property := (_ : List.length x = List.length x) })
[PROOFSTEP]
simp!
[GOAL]
case mk
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α✝ β✝ γ : Type u
α β : Type u_1
f : α → β
x : List α
⊢ Vector.traverseAux (pure ∘ f) x =
    { val := List.map f x, property := (_ : List.length (List.map f x) = List.length x) }
[PROOFSTEP]
induction x
[GOAL]
case mk.nil
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α✝ β✝ γ : Type u
α β : Type u_1
f : α → β
⊢ Vector.traverseAux (pure ∘ f) [] =
    { val := List.map f [], property := (_ : List.length (List.map f []) = List.length []) }
[PROOFSTEP]
simp! [*, functor_norm]
[GOAL]
case mk.cons
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α✝ β✝ γ : Type u
α β : Type u_1
f : α → β
head✝ : α
tail✝ : List α
tail_ih✝ :
  Vector.traverseAux (pure ∘ f) tail✝ =
    { val := List.map f tail✝, property := (_ : List.length (List.map f tail✝) = List.length tail✝) }
⊢ Vector.traverseAux (pure ∘ f) (head✝ :: tail✝) =
    { val := List.map f (head✝ :: tail✝),
      property := (_ : List.length (List.map f (head✝ :: tail✝)) = List.length (head✝ :: tail✝)) }
[PROOFSTEP]
simp! [*, functor_norm]
[GOAL]
case mk.nil
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α✝ β✝ γ : Type u
α β : Type u_1
f : α → β
⊢ nil = { val := [], property := (_ : (fun l => List.length l = List.length []) []) }
[PROOFSTEP]
rfl
[GOAL]
case mk.cons
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α✝ β✝ γ : Type u
α β : Type u_1
f : α → β
head✝ : α
tail✝ : List α
tail_ih✝ :
  Vector.traverseAux (pure ∘ f) tail✝ =
    { val := List.map f tail✝, property := (_ : List.length (List.map f tail✝) = List.length tail✝) }
⊢ (Seq.seq (cons (f head✝)) fun x =>
      { val := List.map f tail✝, property := (_ : List.length (List.map f tail✝) = List.length tail✝) }) =
    { val := f head✝ :: List.map f tail✝,
      property := (_ : (fun l => List.length l = List.length (head✝ :: tail✝)) (f head✝ :: List.map f tail✝)) }
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α✝ β✝ γ : Type u
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
x : Vector α n
⊢ (fun {α} => ApplicativeTransformation.app η α) (Vector.traverse f x) =
    Vector.traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) x
[PROOFSTEP]
induction' x using Vector.inductionOn with n x xs ih
[GOAL]
case h_nil
n : ℕ
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α✝ β✝ γ : Type u
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
⊢ (fun {α} => ApplicativeTransformation.app η α) (Vector.traverse f nil) =
    Vector.traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) nil
[PROOFSTEP]
simp! [functor_norm, cast, η.preserves_pure]
[GOAL]
case h_cons
n✝ : ℕ
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α✝ β✝ γ : Type u
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
n : ℕ
x : α
xs : Vector α n
ih :
  (fun {α} => ApplicativeTransformation.app η α) (Vector.traverse f xs) =
    Vector.traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) xs
⊢ (fun {α} => ApplicativeTransformation.app η α) (Vector.traverse f (x ::ᵥ xs)) =
    Vector.traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) (x ::ᵥ xs)
[PROOFSTEP]
rw [Vector.traverse_def, Vector.traverse_def, ← ih, η.preserves_seq, η.preserves_map]
[GOAL]
case h_cons
n✝ : ℕ
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α✝ β✝ γ : Type u
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
n : ℕ
x : α
xs : Vector α n
ih :
  (fun {α} => ApplicativeTransformation.app η α) (Vector.traverse f xs) =
    Vector.traverse ((fun {α} => ApplicativeTransformation.app η α) ∘ f) xs
⊢ (Seq.seq (cons <$> (fun {α} => ApplicativeTransformation.app η α) (f x)) fun x =>
      (fun {α} => ApplicativeTransformation.app η α) (Vector.traverse f xs)) =
    Seq.seq (cons <$> ((fun {α} => ApplicativeTransformation.app η α) ∘ f) x) fun x =>
      (fun {α} => ApplicativeTransformation.app η α) (Vector.traverse f xs)
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
⊢ ∀ {α : Type u} (x : flip Vector n α), id <$> x = x
[PROOFSTEP]
intro _ x
[GOAL]
n : ℕ
α✝ : Type u
x : flip Vector n α✝
⊢ id <$> x = x
[PROOFSTEP]
cases x
[GOAL]
case mk
n : ℕ
α✝ : Type u
val✝ : List α✝
property✝ : List.length val✝ = n
⊢ id <$> { val := val✝, property := property✝ } = { val := val✝, property := property✝ }
[PROOFSTEP]
simp! [(· <$> ·)]
[GOAL]
n : ℕ
⊢ ∀ {α β γ : Type u} (g : α → β) (h : β → γ) (x : flip Vector n α), (h ∘ g) <$> x = h <$> g <$> x
[PROOFSTEP]
intro _ _ _ _ _ x
[GOAL]
n : ℕ
α✝ β✝ γ✝ : Type u
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x : flip Vector n α✝
⊢ (h✝ ∘ g✝) <$> x = h✝ <$> g✝ <$> x
[PROOFSTEP]
cases x
[GOAL]
case mk
n : ℕ
α✝ β✝ γ✝ : Type u
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
val✝ : List α✝
property✝ : List.length val✝ = n
⊢ (h✝ ∘ g✝) <$> { val := val✝, property := property✝ } = h✝ <$> g✝ <$> { val := val✝, property := property✝ }
[PROOFSTEP]
simp! [(· <$> ·)]
[GOAL]
α : Type ?u.94018
m n : ℕ
xs : Vector α n
ys : Vector α m
x : α
⊢ 0 < Nat.succ n + m
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
m n : ℕ
xs : Vector α n
ys : Vector α m
⊢ append xs nil = xs
[PROOFSTEP]
cases xs
[GOAL]
case mk
α : Type u_1
m n : ℕ
ys : Vector α m
val✝ : List α
property✝ : List.length val✝ = n
⊢ append { val := val✝, property := property✝ } nil = { val := val✝, property := property✝ }
[PROOFSTEP]
simp [append]
[GOAL]
α : Type u_2
β : Type u_3
n : ℕ
xs : Vector α n
ys : Vector β n
γ : Type u_1
v₁ : Vector α n
v₂ : Vector β n
f : α → β → γ
i : Fin n
⊢ get (map₂ f v₁ v₂) i = f (get v₁ i) (get v₂ i)
[PROOFSTEP]
clear * - v₁ v₂
[GOAL]
α : Type u_2
β : Type u_3
n : ℕ
γ : Type u_1
v₁ : Vector α n
v₂ : Vector β n
f : α → β → γ
i : Fin n
⊢ get (map₂ f v₁ v₂) i = f (get v₁ i) (get v₂ i)
[PROOFSTEP]
induction v₁, v₂ using inductionOn₂
[GOAL]
case nil
α : Type u_2
β : Type u_3
n : ℕ
γ : Type u_1
f : α → β → γ
i : Fin 0
⊢ get (map₂ f nil nil) i = f (get nil i) (get nil i)
case cons
α : Type u_2
β : Type u_3
n : ℕ
γ : Type u_1
f : α → β → γ
n✝ : ℕ
a✝¹ : α
b✝ : β
x✝ : Vector α n✝
y✝ : Vector β n✝
a✝ : ∀ (i : Fin n✝), get (map₂ f x✝ y✝) i = f (get x✝ i) (get y✝ i)
i : Fin (Nat.succ n✝)
⊢ get (map₂ f (a✝¹ ::ᵥ x✝) (b✝ ::ᵥ y✝)) i = f (get (a✝¹ ::ᵥ x✝) i) (get (b✝ ::ᵥ y✝) i)
[PROOFSTEP]
case nil => exact Fin.elim0 i
[GOAL]
α : Type u_2
β : Type u_3
n : ℕ
γ : Type u_1
f : α → β → γ
i : Fin 0
⊢ get (map₂ f nil nil) i = f (get nil i) (get nil i)
[PROOFSTEP]
case nil => exact Fin.elim0 i
[GOAL]
α : Type u_2
β : Type u_3
n : ℕ
γ : Type u_1
f : α → β → γ
i : Fin 0
⊢ get (map₂ f nil nil) i = f (get nil i) (get nil i)
[PROOFSTEP]
exact Fin.elim0 i
[GOAL]
case cons
α : Type u_2
β : Type u_3
n : ℕ
γ : Type u_1
f : α → β → γ
n✝ : ℕ
a✝¹ : α
b✝ : β
x✝ : Vector α n✝
y✝ : Vector β n✝
a✝ : ∀ (i : Fin n✝), get (map₂ f x✝ y✝) i = f (get x✝ i) (get y✝ i)
i : Fin (Nat.succ n✝)
⊢ get (map₂ f (a✝¹ ::ᵥ x✝) (b✝ ::ᵥ y✝)) i = f (get (a✝¹ ::ᵥ x✝) i) (get (b✝ ::ᵥ y✝) i)
[PROOFSTEP]
case cons x xs y ys ih =>
  rw [map₂_cons]
  cases i using Fin.cases
  · simp only [get_zero, head_cons]
  · simp only [get_cons_succ, ih]
[GOAL]
α : Type u_2
β : Type u_3
n : ℕ
γ : Type u_1
f : α → β → γ
n✝ : ℕ
x : α
xs : β
y : Vector α n✝
ys : Vector β n✝
ih : ∀ (i : Fin n✝), get (map₂ f y ys) i = f (get y i) (get ys i)
i : Fin (Nat.succ n✝)
⊢ get (map₂ f (x ::ᵥ y) (xs ::ᵥ ys)) i = f (get (x ::ᵥ y) i) (get (xs ::ᵥ ys) i)
[PROOFSTEP]
case cons x xs y ys ih =>
  rw [map₂_cons]
  cases i using Fin.cases
  · simp only [get_zero, head_cons]
  · simp only [get_cons_succ, ih]
[GOAL]
α : Type u_2
β : Type u_3
n : ℕ
γ : Type u_1
f : α → β → γ
n✝ : ℕ
x : α
xs : β
y : Vector α n✝
ys : Vector β n✝
ih : ∀ (i : Fin n✝), get (map₂ f y ys) i = f (get y i) (get ys i)
i : Fin (Nat.succ n✝)
⊢ get (map₂ f (x ::ᵥ y) (xs ::ᵥ ys)) i = f (get (x ::ᵥ y) i) (get (xs ::ᵥ ys) i)
[PROOFSTEP]
rw [map₂_cons]
[GOAL]
α : Type u_2
β : Type u_3
n : ℕ
γ : Type u_1
f : α → β → γ
n✝ : ℕ
x : α
xs : β
y : Vector α n✝
ys : Vector β n✝
ih : ∀ (i : Fin n✝), get (map₂ f y ys) i = f (get y i) (get ys i)
i : Fin (Nat.succ n✝)
⊢ get (f x xs ::ᵥ map₂ f y ys) i = f (get (x ::ᵥ y) i) (get (xs ::ᵥ ys) i)
[PROOFSTEP]
cases i using Fin.cases
[GOAL]
case zero
α : Type u_2
β : Type u_3
n : ℕ
γ : Type u_1
f : α → β → γ
n✝ : ℕ
x : α
xs : β
y : Vector α n✝
ys : Vector β n✝
ih : ∀ (i : Fin n✝), get (map₂ f y ys) i = f (get y i) (get ys i)
⊢ get (f x xs ::ᵥ map₂ f y ys) 0 = f (get (x ::ᵥ y) 0) (get (xs ::ᵥ ys) 0)
[PROOFSTEP]
simp only [get_zero, head_cons]
[GOAL]
case succ
α : Type u_2
β : Type u_3
n : ℕ
γ : Type u_1
f : α → β → γ
n✝ : ℕ
x : α
xs : β
y : Vector α n✝
ys : Vector β n✝
ih : ∀ (i : Fin n✝), get (map₂ f y ys) i = f (get y i) (get ys i)
i✝ : Fin n✝
⊢ get (f x xs ::ᵥ map₂ f y ys) (Fin.succ i✝) = f (get (x ::ᵥ y) (Fin.succ i✝)) (get (xs ::ᵥ ys) (Fin.succ i✝))
[PROOFSTEP]
simp only [get_cons_succ, ih]


[GOAL]
r : ℝ
hr : 0 ≤ r
⊢ Real.toNNReal r = { val := r, property := hr }
[PROOFSTEP]
simp_rw [Real.toNNReal, max_eq_left hr]
[GOAL]
⊢ Zero ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ One ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ Add ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ Sub ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ Mul ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ Inv ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ Div ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ LE ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ Bot ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ Inhabited ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ Nontrivial ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
r₁ r₂ : ℝ≥0
h : r₂ ≤ r₁
⊢ ↑r₂ ≤ ↑r₁ - 0
[PROOFSTEP]
simp [show (r₂ : ℝ) ≤ r₁ from h]
[GOAL]
r : ℝ≥0
⊢ ↑r = 0 ↔ r = 0
[PROOFSTEP]
rw [← NNReal.coe_zero, NNReal.coe_eq]
[GOAL]
r : ℝ≥0
⊢ ↑r = 1 ↔ r = 1
[PROOFSTEP]
rw [← NNReal.coe_one, NNReal.coe_eq]
[GOAL]
⊢ CommSemiring ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra ℝ A
r : ℝ≥0
x : (fun x => A) r
⊢ ↑(RingHom.comp (algebraMap ℝ A) toRealHom) r * x = x * ↑(RingHom.comp (algebraMap ℝ A) toRealHom) r
[PROOFSTEP]
simp [Algebra.commutes]
[GOAL]
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra ℝ A
r : ℝ≥0
x : (fun x => A) r
⊢ r • x = ↑(RingHom.comp (algebraMap ℝ A) toRealHom) r * x
[PROOFSTEP]
simp [← Algebra.smul_def (r : ℝ) x, smul_def]
[GOAL]
⊢ Algebra ℝ≥0 ℝ
[PROOFSTEP]
infer_instance
[GOAL]
⊢ DistribMulAction ℝ≥0ˣ ℝ
[PROOFSTEP]
infer_instance
[GOAL]
⊢ MonoidWithZero ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ CommMonoidWithZero ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ CommGroupWithZero ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ (a : α), a ∈ s → 0 ≤ f a
⊢ Real.toNNReal (∑ a in s, f a) = ∑ a in s, Real.toNNReal (f a)
[PROOFSTEP]
rw [← NNReal.coe_eq, NNReal.coe_sum, Real.coe_toNNReal _ (Finset.sum_nonneg hf)]
[GOAL]
α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ (a : α), a ∈ s → 0 ≤ f a
⊢ ∑ i in s, f i = ∑ a in s, ↑(Real.toNNReal (f a))
[PROOFSTEP]
exact Finset.sum_congr rfl fun x hxs => by rw [Real.coe_toNNReal _ (hf x hxs)]
[GOAL]
α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ (a : α), a ∈ s → 0 ≤ f a
x : α
hxs : x ∈ s
⊢ f x = ↑(Real.toNNReal (f x))
[PROOFSTEP]
rw [Real.coe_toNNReal _ (hf x hxs)]
[GOAL]
α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ (a : α), a ∈ s → 0 ≤ f a
⊢ Real.toNNReal (∏ a in s, f a) = ∏ a in s, Real.toNNReal (f a)
[PROOFSTEP]
rw [← NNReal.coe_eq, NNReal.coe_prod, Real.coe_toNNReal _ (Finset.prod_nonneg hf)]
[GOAL]
α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ (a : α), a ∈ s → 0 ≤ f a
⊢ ∏ i in s, f i = ∏ a in s, ↑(Real.toNNReal (f a))
[PROOFSTEP]
exact Finset.prod_congr rfl fun x hxs => by rw [Real.coe_toNNReal _ (hf x hxs)]
[GOAL]
α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ (a : α), a ∈ s → 0 ≤ f a
x : α
hxs : x ∈ s
⊢ f x = ↑(Real.toNNReal (f x))
[PROOFSTEP]
rw [Real.coe_toNNReal _ (hf x hxs)]
[GOAL]
⊢ LinearOrder ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
n : ℕ
⊢ ↑(Real.toNNReal ↑n) = ↑↑n
[PROOFSTEP]
simp [Real.coe_toNNReal]
[GOAL]
⊢ OrderBot ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ PartialOrder ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ CanonicallyLinearOrderedAddMonoid ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ LinearOrderedAddCommMonoid ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ DistribLattice ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ SemilatticeInf ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ SemilatticeSup ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ LinearOrderedSemiring ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ OrderedCommSemiring ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ LinearOrderedCommMonoid ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ LinearOrderedCommMonoidWithZero ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ LinearOrderedCommGroupWithZero ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ CanonicallyOrderedCommSemiring ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ DenselyOrdered ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
⊢ NoMaxOrder ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
ι : Sort u_1
s : ι → ℝ≥0
⊢ ↑(⨆ (i : ι), s i) = ⨆ (i : ι), ↑(s i)
[PROOFSTEP]
rw [iSup, iSup, coe_sSup, ← Set.range_comp]
[GOAL]
ι : Sort u_1
s : ι → ℝ≥0
⊢ sSup (Set.range (toReal ∘ fun i => s i)) = sSup (Set.range fun i => ↑(s i))
[PROOFSTEP]
rfl
[GOAL]
⊢ sInf ∅ = 0
[PROOFSTEP]
rw [← NNReal.coe_eq_zero, coe_sInf, Set.image_empty, Real.sInf_empty]
[GOAL]
ι : Sort u_1
s : ι → ℝ≥0
⊢ ↑(⨅ (i : ι), s i) = ⨅ (i : ι), ↑(s i)
[PROOFSTEP]
rw [iInf, iInf, coe_sInf, ← Set.range_comp]
[GOAL]
ι : Sort u_1
s : ι → ℝ≥0
⊢ sInf (Set.range (toReal ∘ fun i => s i)) = sInf (Set.range fun i => ↑(s i))
[PROOFSTEP]
rfl
[GOAL]
ι : Sort u_1
ι' : Sort u_2
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
f : ι → ℝ≥0
g : ι' → ℝ≥0
a : ℝ≥0
h : ∀ (i : ι) (j : ι'), a ≤ f i + g j
⊢ a ≤ (⨅ (i : ι), f i) + ⨅ (j : ι'), g j
[PROOFSTEP]
rw [← NNReal.coe_le_coe, NNReal.coe_add, coe_iInf, coe_iInf]
[GOAL]
ι : Sort u_1
ι' : Sort u_2
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
f : ι → ℝ≥0
g : ι' → ℝ≥0
a : ℝ≥0
h : ∀ (i : ι) (j : ι'), a ≤ f i + g j
⊢ ↑a ≤ (⨅ (i : ι), ↑(f i)) + ⨅ (i : ι'), ↑(g i)
[PROOFSTEP]
exact le_ciInf_add_ciInf h
[GOAL]
⊢ Archimedean ℝ≥0
[PROOFSTEP]
infer_instance
  -- porting note: TODO: remove?
[GOAL]
a b : ℝ≥0
h : ↑a < ↑b
q : ℚ
haq : ↑a < ↑q
hqb : ↑q < ↑b
this : 0 ≤ ↑q
⊢ a < Real.toNNReal ↑q ∧ Real.toNNReal ↑q < b
[PROOFSTEP]
simp [Real.coe_toNNReal _ this, NNReal.coe_lt_coe.symm, haq, hqb]
[GOAL]
α : Type u_1
f : α → ℝ≥0
s : Finset α
r : ℝ≥0
⊢ Finset.sup s f / r = Finset.sup s fun a => f a / r
[PROOFSTEP]
simp only [div_eq_inv_mul, mul_finset_sup]
[GOAL]
r : ℝ
⊢ 0 < toNNReal r ↔ 0 < r
[PROOFSTEP]
simp [← NNReal.coe_lt_coe, lt_irrefl]
[GOAL]
r : ℝ
⊢ toNNReal r = 0 ↔ r ≤ 0
[PROOFSTEP]
simpa [-toNNReal_pos] using not_iff_not.2 (@toNNReal_pos r)
[GOAL]
r p : ℝ
hp : 0 ≤ p
⊢ toNNReal r ≤ toNNReal p ↔ r ≤ p
[PROOFSTEP]
simp [← NNReal.coe_le_coe, hp]
[GOAL]
r p : ℝ
hr : 0 ≤ r
hp : 0 ≤ p
⊢ toNNReal r = toNNReal p ↔ r = p
[PROOFSTEP]
simp [← NNReal.coe_eq, coe_toNNReal, hr, hp]
[GOAL]
r p : ℝ
hr : 0 ≤ r
hp : 0 ≤ p
⊢ ↑(toNNReal (r + p)) = ↑(toNNReal r + toNNReal p)
[PROOFSTEP]
simp [hr, hp, add_nonneg]
[GOAL]
r : ℝ≥0
p : ℝ
hp : 0 ≤ p
⊢ r ≤ toNNReal p ↔ ↑r ≤ p
[PROOFSTEP]
rw [← NNReal.coe_le_coe, Real.coe_toNNReal p hp]
[GOAL]
r : ℝ≥0
p : ℝ
hr : 0 < r
hp : p < 0
⊢ r ≤ toNNReal p ↔ ↑r ≤ p
[PROOFSTEP]
simp only [(hp.trans_le r.coe_nonneg).not_le, toNNReal_eq_zero.2 hp.le, hr.not_le]
[GOAL]
r : ℝ
p : ℝ≥0
ha : 0 ≤ r
⊢ toNNReal r < p ↔ r < ↑p
[PROOFSTEP]
rw [← NNReal.coe_lt_coe, Real.coe_toNNReal r ha]
[GOAL]
x : ℝ
hx : 0 ≤ x
n : ℕ
⊢ toNNReal (x ^ n) = toNNReal x ^ n
[PROOFSTEP]
rw [← NNReal.coe_eq, NNReal.coe_pow, Real.coe_toNNReal _ (pow_nonneg hx _), Real.coe_toNNReal x hx]
[GOAL]
p q : ℝ
hp : 0 ≤ p
⊢ ↑(toNNReal (p * q)) = ↑(toNNReal p * toNNReal q)
[PROOFSTEP]
simp [mul_max_of_nonneg, hp]
[GOAL]
a b c : ℝ≥0
h : a ≠ 0
⊢ a * b = a * c ↔ b = c
[PROOFSTEP]
rw [mul_eq_mul_left_iff, or_iff_left h]
[GOAL]
a b : ℝ≥0
ha : 0 < a
hb : b < 1
⊢ ∃ n, b ^ n < a
[PROOFSTEP]
simpa only [← coe_pow, NNReal.coe_lt_coe] using exists_pow_lt_of_lt_one (NNReal.coe_pos.2 ha) (NNReal.coe_lt_coe.2 hb)
[GOAL]
⊢ OrderedSub ℝ≥0
[PROOFSTEP]
infer_instance
[GOAL]
r p : ℝ≥0
h : r ≠ 0
⊢ r⁻¹ ≤ p ↔ 1 ≤ r * p
[PROOFSTEP]
rw [← mul_le_mul_left (pos_iff_ne_zero.2 h), mul_inv_cancel h]
[GOAL]
r p : ℝ≥0
h : 1 ≤ r * p
⊢ r⁻¹ ≤ p
[PROOFSTEP]
by_cases r = 0
[GOAL]
r p : ℝ≥0
h : 1 ≤ r * p
⊢ r⁻¹ ≤ p
[PROOFSTEP]
by_cases r = 0
[GOAL]
case pos
r p : ℝ≥0
h✝ : 1 ≤ r * p
h : r = 0
⊢ r⁻¹ ≤ p
[PROOFSTEP]
simp [*, inv_le]
[GOAL]
case neg
r p : ℝ≥0
h✝ : 1 ≤ r * p
h : ¬r = 0
⊢ r⁻¹ ≤ p
[PROOFSTEP]
simp [*, inv_le]
[GOAL]
r p : ℝ≥0
h : p ≠ 0
⊢ r ≤ p⁻¹ ↔ r * p ≤ 1
[PROOFSTEP]
rw [← mul_le_mul_left (pos_iff_ne_zero.2 h), mul_inv_cancel h, mul_comm]
[GOAL]
r p : ℝ≥0
h : p ≠ 0
⊢ r < p⁻¹ ↔ r * p < 1
[PROOFSTEP]
rw [← mul_lt_mul_left (pos_iff_ne_zero.2 h), mul_inv_cancel h, mul_comm]
[GOAL]
a b r : ℝ≥0
hr : r ≠ 0
⊢ r * a ≤ b ↔ a ≤ r⁻¹ * b
[PROOFSTEP]
have : 0 < r := lt_of_le_of_ne (zero_le r) hr.symm
[GOAL]
a b r : ℝ≥0
hr : r ≠ 0
this : 0 < r
⊢ r * a ≤ b ↔ a ≤ r⁻¹ * b
[PROOFSTEP]
rw [← mul_le_mul_left (inv_pos.mpr this), ← mul_assoc, inv_mul_cancel hr, one_mul]
[GOAL]
a b c : ℝ≥0
h : a ≤ b * c
h0 : c = 0
⊢ a / c ≤ b
[PROOFSTEP]
simp [h0]
[GOAL]
a b r : ℝ≥0
h : a < b / r
hr : r = 0
⊢ False
[PROOFSTEP]
simp [hr] at h
[GOAL]
x y : ℝ≥0
h : ∀ (a : ℝ≥0), a < 1 → a * x ≤ y
a : ℝ≥0
ha : a < x
⊢ a ≤ y
[PROOFSTEP]
have hx : x ≠ 0 := pos_iff_ne_zero.1 (lt_of_le_of_lt (zero_le _) ha)
[GOAL]
x y : ℝ≥0
h : ∀ (a : ℝ≥0), a < 1 → a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
⊢ a ≤ y
[PROOFSTEP]
have hx' : x⁻¹ ≠ 0 := by rwa [Ne.def, inv_eq_zero]
[GOAL]
x y : ℝ≥0
h : ∀ (a : ℝ≥0), a < 1 → a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
⊢ x⁻¹ ≠ 0
[PROOFSTEP]
rwa [Ne.def, inv_eq_zero]
[GOAL]
x y : ℝ≥0
h : ∀ (a : ℝ≥0), a < 1 → a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
⊢ a ≤ y
[PROOFSTEP]
have : a * x⁻¹ < 1 := by rwa [← lt_inv_iff_mul_lt hx', inv_inv]
[GOAL]
x y : ℝ≥0
h : ∀ (a : ℝ≥0), a < 1 → a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
⊢ a * x⁻¹ < 1
[PROOFSTEP]
rwa [← lt_inv_iff_mul_lt hx', inv_inv]
[GOAL]
x y : ℝ≥0
h : ∀ (a : ℝ≥0), a < 1 → a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
this : a * x⁻¹ < 1
⊢ a ≤ y
[PROOFSTEP]
have : a * x⁻¹ * x ≤ y := h _ this
[GOAL]
x y : ℝ≥0
h : ∀ (a : ℝ≥0), a < 1 → a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
this✝ : a * x⁻¹ < 1
this : a * x⁻¹ * x ≤ y
⊢ a ≤ y
[PROOFSTEP]
rwa [mul_assoc, inv_mul_cancel hx, mul_one] at this
[GOAL]
a b : ℝ≥0
h : a < b
⊢ a / b < 1
[PROOFSTEP]
rwa [div_lt_iff, one_mul]
[GOAL]
a b : ℝ≥0
h : a < b
⊢ b ≠ 0
[PROOFSTEP]
exact ne_of_gt (lt_of_le_of_lt (zero_le _) h)
[GOAL]
x : ℝ
⊢ toNNReal x⁻¹ = (toNNReal x)⁻¹
[PROOFSTEP]
cases' le_total 0 x with hx hx
[GOAL]
case inl
x : ℝ
hx : 0 ≤ x
⊢ toNNReal x⁻¹ = (toNNReal x)⁻¹
[PROOFSTEP]
nth_rw 1 [← Real.coe_toNNReal x hx]
[GOAL]
case inl
x : ℝ
hx : 0 ≤ x
⊢ toNNReal (↑(toNNReal x))⁻¹ = (toNNReal x)⁻¹
[PROOFSTEP]
rw [← NNReal.coe_inv, Real.toNNReal_coe]
[GOAL]
case inr
x : ℝ
hx : x ≤ 0
⊢ toNNReal x⁻¹ = (toNNReal x)⁻¹
[PROOFSTEP]
rw [toNNReal_eq_zero.mpr hx, inv_zero, toNNReal_eq_zero.mpr (inv_nonpos.mpr hx)]
[GOAL]
x y : ℝ
hx : 0 ≤ x
⊢ toNNReal (x / y) = toNNReal x / toNNReal y
[PROOFSTEP]
rw [div_eq_mul_inv, div_eq_mul_inv, ← Real.toNNReal_inv, ← Real.toNNReal_mul hx]
[GOAL]
x y : ℝ
hy : 0 ≤ y
⊢ toNNReal (x / y) = toNNReal x / toNNReal y
[PROOFSTEP]
rw [div_eq_inv_mul, div_eq_inv_mul, Real.toNNReal_mul (inv_nonneg.2 hy), Real.toNNReal_inv]
[GOAL]
x : ℝ≥0
hx : x ≠ 0
⊢ x⁻¹ < 1 ↔ 1 < x
[PROOFSTEP]
rw [← one_div, div_lt_iff hx, one_mul]
[GOAL]
ι : Sort u_1
f : ι → ℝ≥0
s : Set ℝ≥0
hs : ¬BddAbove s
⊢ sSup s = 0
[PROOFSTEP]
rw [← bddAbove_coe] at hs
[GOAL]
ι : Sort u_1
f : ι → ℝ≥0
s : Set ℝ≥0
hs : ¬BddAbove (toReal '' s)
⊢ sSup s = 0
[PROOFSTEP]
rw [← NNReal.coe_eq, coe_sSup, NNReal.coe_zero]
[GOAL]
ι : Sort u_1
f : ι → ℝ≥0
s : Set ℝ≥0
hs : ¬BddAbove (toReal '' s)
⊢ sSup (toReal '' s) = 0
[PROOFSTEP]
exact sSup_of_not_bddAbove hs
[GOAL]
ι : Sort u_1
f✝ : ι → ℝ≥0
inst✝ : IsEmpty ι
f : ι → ℝ≥0
⊢ ⨅ (i : ι), f i = 0
[PROOFSTEP]
rw [iInf_of_empty', sInf_empty]
[GOAL]
ι : Sort u_1
f : ι → ℝ≥0
α : Sort u_2
⊢ ⨅ (x : α), 0 = 0
[PROOFSTEP]
rw [← NNReal.coe_eq, coe_iInf]
[GOAL]
ι : Sort u_1
f : ι → ℝ≥0
α : Sort u_2
⊢ ⨅ (i : α), ↑0 = ↑0
[PROOFSTEP]
exact Real.ciInf_const_zero
[GOAL]
ι : Sort u_1
f✝ f : ι → ℝ≥0
a : ℝ≥0
⊢ iInf f * a = ⨅ (i : ι), f i * a
[PROOFSTEP]
rw [← NNReal.coe_eq, NNReal.coe_mul, coe_iInf, coe_iInf]
[GOAL]
ι : Sort u_1
f✝ f : ι → ℝ≥0
a : ℝ≥0
⊢ (⨅ (i : ι), ↑(f i)) * ↑a = ⨅ (i : ι), ↑(f i * a)
[PROOFSTEP]
exact Real.iInf_mul_of_nonneg (NNReal.coe_nonneg _) _
[GOAL]
ι : Sort u_1
f✝ f : ι → ℝ≥0
a : ℝ≥0
⊢ a * iInf f = ⨅ (i : ι), a * f i
[PROOFSTEP]
simpa only [mul_comm] using iInf_mul f a
[GOAL]
ι : Sort u_1
f✝ f : ι → ℝ≥0
a : ℝ≥0
⊢ a * ⨆ (i : ι), f i = ⨆ (i : ι), a * f i
[PROOFSTEP]
rw [← NNReal.coe_eq, NNReal.coe_mul, NNReal.coe_iSup, NNReal.coe_iSup]
[GOAL]
ι : Sort u_1
f✝ f : ι → ℝ≥0
a : ℝ≥0
⊢ ↑a * ⨆ (i : ι), ↑(f i) = ⨆ (i : ι), ↑(a * f i)
[PROOFSTEP]
exact Real.mul_iSup_of_nonneg (NNReal.coe_nonneg _) _
[GOAL]
ι : Sort u_1
f✝ f : ι → ℝ≥0
a : ℝ≥0
⊢ (⨆ (i : ι), f i) * a = ⨆ (i : ι), f i * a
[PROOFSTEP]
rw [mul_comm, mul_iSup]
[GOAL]
ι : Sort u_1
f✝ f : ι → ℝ≥0
a : ℝ≥0
⊢ ⨆ (i : ι), a * f i = ⨆ (i : ι), f i * a
[PROOFSTEP]
simp_rw [mul_comm]
[GOAL]
ι : Sort u_1
f✝ f : ι → ℝ≥0
a : ℝ≥0
⊢ (⨆ (i : ι), f i) / a = ⨆ (i : ι), f i / a
[PROOFSTEP]
simp only [div_eq_mul_inv, iSup_mul]
[GOAL]
ι : Sort u_1
f : ι → ℝ≥0
a g : ℝ≥0
h : ι → ℝ≥0
H : ∀ (j : ι), g * h j ≤ a
⊢ g * iSup h ≤ a
[PROOFSTEP]
rw [mul_iSup]
[GOAL]
ι : Sort u_1
f : ι → ℝ≥0
a g : ℝ≥0
h : ι → ℝ≥0
H : ∀ (j : ι), g * h j ≤ a
⊢ ⨆ (i : ι), g * h i ≤ a
[PROOFSTEP]
exact ciSup_le' H
[GOAL]
ι : Sort u_1
f : ι → ℝ≥0
a : ℝ≥0
g : ι → ℝ≥0
h : ℝ≥0
H : ∀ (i : ι), g i * h ≤ a
⊢ iSup g * h ≤ a
[PROOFSTEP]
rw [iSup_mul]
[GOAL]
ι : Sort u_1
f : ι → ℝ≥0
a : ℝ≥0
g : ι → ℝ≥0
h : ℝ≥0
H : ∀ (i : ι), g i * h ≤ a
⊢ ⨆ (i : ι), g i * h ≤ a
[PROOFSTEP]
exact ciSup_le' H
[GOAL]
ι : Sort u_1
f : ι → ℝ≥0
inst✝ : Nonempty ι
a g : ℝ≥0
h : ι → ℝ≥0
H : ∀ (j : ι), a ≤ g * h j
⊢ a ≤ g * iInf h
[PROOFSTEP]
rw [mul_iInf]
[GOAL]
ι : Sort u_1
f : ι → ℝ≥0
inst✝ : Nonempty ι
a g : ℝ≥0
h : ι → ℝ≥0
H : ∀ (j : ι), a ≤ g * h j
⊢ a ≤ ⨅ (i : ι), g * h i
[PROOFSTEP]
exact le_ciInf H
[GOAL]
ι : Sort u_1
f : ι → ℝ≥0
inst✝ : Nonempty ι
a : ℝ≥0
g : ι → ℝ≥0
h : ℝ≥0
H : ∀ (i : ι), a ≤ g i * h
⊢ a ≤ iInf g * h
[PROOFSTEP]
rw [iInf_mul]
[GOAL]
ι : Sort u_1
f : ι → ℝ≥0
inst✝ : Nonempty ι
a : ℝ≥0
g : ι → ℝ≥0
h : ℝ≥0
H : ∀ (i : ι), a ≤ g i * h
⊢ a ≤ ⨅ (i : ι), g i * h
[PROOFSTEP]
exact le_ciInf H
[GOAL]
s : Set ℝ
t : Set ℝ≥0
h : OrdConnected s
⊢ OrdConnected (toNNReal '' s)
[PROOFSTEP]
refine' ⟨ball_image_iff.2 fun x hx => ball_image_iff.2 fun y hy z hz => _⟩
[GOAL]
s : Set ℝ
t : Set ℝ≥0
h : OrdConnected s
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
z : ℝ≥0
hz : z ∈ Icc (toNNReal x) (toNNReal y)
⊢ z ∈ toNNReal '' s
[PROOFSTEP]
cases' le_total y 0 with hy₀ hy₀
[GOAL]
case inl
s : Set ℝ
t : Set ℝ≥0
h : OrdConnected s
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
z : ℝ≥0
hz : z ∈ Icc (toNNReal x) (toNNReal y)
hy₀ : y ≤ 0
⊢ z ∈ toNNReal '' s
[PROOFSTEP]
rw [mem_Icc, Real.toNNReal_of_nonpos hy₀, nonpos_iff_eq_zero] at hz
[GOAL]
case inl
s : Set ℝ
t : Set ℝ≥0
h : OrdConnected s
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
z : ℝ≥0
hz : toNNReal x ≤ z ∧ z = 0
hy₀ : y ≤ 0
⊢ z ∈ toNNReal '' s
[PROOFSTEP]
exact ⟨y, hy, (toNNReal_of_nonpos hy₀).trans hz.2.symm⟩
[GOAL]
case inr
s : Set ℝ
t : Set ℝ≥0
h : OrdConnected s
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
z : ℝ≥0
hz : z ∈ Icc (toNNReal x) (toNNReal y)
hy₀ : 0 ≤ y
⊢ z ∈ toNNReal '' s
[PROOFSTEP]
lift y to ℝ≥0 using hy₀
[GOAL]
case inr.intro
s : Set ℝ
t : Set ℝ≥0
h : OrdConnected s
x : ℝ
hx : x ∈ s
z y : ℝ≥0
hy : ↑y ∈ s
hz : z ∈ Icc (toNNReal x) (toNNReal ↑y)
⊢ z ∈ toNNReal '' s
[PROOFSTEP]
rw [toNNReal_coe] at hz
[GOAL]
case inr.intro
s : Set ℝ
t : Set ℝ≥0
h : OrdConnected s
x : ℝ
hx : x ∈ s
z y : ℝ≥0
hy : ↑y ∈ s
hz : z ∈ Icc (toNNReal x) y
⊢ z ∈ toNNReal '' s
[PROOFSTEP]
exact ⟨z, h.out hx hy ⟨toNNReal_le_iff_le_coe.1 hz.1, hz.2⟩, toNNReal_coe⟩
[GOAL]
⊢ (fun x => { val := |x|, property := (_ : 0 ≤ |x|) }) 0 = 0
[PROOFSTEP]
ext
[GOAL]
case a
⊢ ↑((fun x => { val := |x|, property := (_ : 0 ≤ |x|) }) 0) = ↑0
[PROOFSTEP]
simp
[GOAL]
⊢ ZeroHom.toFun
      { toFun := fun x => { val := |x|, property := (_ : 0 ≤ |x|) },
        map_zero' := (_ : (fun x => { val := |x|, property := (_ : 0 ≤ |x|) }) 0 = 0) }
      1 =
    1
[PROOFSTEP]
ext
[GOAL]
case a
⊢ ↑(ZeroHom.toFun
        { toFun := fun x => { val := |x|, property := (_ : 0 ≤ |x|) },
          map_zero' := (_ : (fun x => { val := |x|, property := (_ : 0 ≤ |x|) }) 0 = 0) }
        1) =
    ↑1
[PROOFSTEP]
simp
[GOAL]
x y : ℝ
⊢ ZeroHom.toFun
      { toFun := fun x => { val := |x|, property := (_ : 0 ≤ |x|) },
        map_zero' := (_ : (fun x => { val := |x|, property := (_ : 0 ≤ |x|) }) 0 = 0) }
      (x * y) =
    ZeroHom.toFun
        { toFun := fun x => { val := |x|, property := (_ : 0 ≤ |x|) },
          map_zero' := (_ : (fun x => { val := |x|, property := (_ : 0 ≤ |x|) }) 0 = 0) }
        x *
      ZeroHom.toFun
        { toFun := fun x => { val := |x|, property := (_ : 0 ≤ |x|) },
          map_zero' := (_ : (fun x => { val := |x|, property := (_ : 0 ≤ |x|) }) 0 = 0) }
        y
[PROOFSTEP]
ext
[GOAL]
case a
x y : ℝ
⊢ ↑(ZeroHom.toFun
        { toFun := fun x => { val := |x|, property := (_ : 0 ≤ |x|) },
          map_zero' := (_ : (fun x => { val := |x|, property := (_ : 0 ≤ |x|) }) 0 = 0) }
        (x * y)) =
    ↑(ZeroHom.toFun
          { toFun := fun x => { val := |x|, property := (_ : 0 ≤ |x|) },
            map_zero' := (_ : (fun x => { val := |x|, property := (_ : 0 ≤ |x|) }) 0 = 0) }
          x *
        ZeroHom.toFun
          { toFun := fun x => { val := |x|, property := (_ : 0 ≤ |x|) },
            map_zero' := (_ : (fun x => { val := |x|, property := (_ : 0 ≤ |x|) }) 0 = 0) }
          y)
[PROOFSTEP]
simp [abs_mul]
[GOAL]
x : ℝ
h : 0 ≤ x
⊢ ↑nnabs x = toNNReal x
[PROOFSTEP]
ext
[GOAL]
case a
x : ℝ
h : 0 ≤ x
⊢ ↑(↑nnabs x) = ↑(toNNReal x)
[PROOFSTEP]
rw [coe_toNNReal x h, coe_nnabs, abs_of_nonneg h]
[GOAL]
x : ℝ≥0
⊢ ↑nnabs ↑x = x
[PROOFSTEP]
simp
[GOAL]
n : ℤ
⊢ ↑(Int.natAbs n) = ↑nnabs ↑n
[PROOFSTEP]
ext
[GOAL]
case a
n : ℤ
⊢ ↑↑(Int.natAbs n) = ↑(↑nnabs ↑n)
[PROOFSTEP]
rw [NNReal.coe_nat_cast, Int.cast_natAbs, Real.coe_nnabs, Int.cast_abs]


[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : Fintype o
α : m → n → Type v
M N : DMatrix m n α
h : M = N
⊢ ∀ (i : m) (j : n), M i j = N i j
[PROOFSTEP]
simp [h]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : Fintype o
α : m → n → Type v
M : DMatrix m n α
β : m → n → Type w
γ : m → n → Type z
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j → β i j
g : ⦃i : m⦄ → ⦃j : n⦄ → β i j → γ i j
⊢ map (map M f) g = map M fun i j x => g (f x)
[PROOFSTEP]
ext
[GOAL]
case a
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : Fintype o
α : m → n → Type v
M : DMatrix m n α
β : m → n → Type w
γ : m → n → Type z
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j → β i j
g : ⦃i : m⦄ → ⦃j : n⦄ → β i j → γ i j
i✝ : m
j✝ : n
⊢ map (map M f) g i✝ j✝ = map M (fun i j x => g (f x)) i✝ j✝
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : Fintype o
α : m → n → Type v
inst✝ : ∀ (i : m) (j : n), Subsingleton (α i j)
⊢ Subsingleton (DMatrix m n α)
[PROOFSTEP]
constructor
[GOAL]
case allEq
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : Fintype o
α : m → n → Type v
inst✝ : ∀ (i : m) (j : n), Subsingleton (α i j)
⊢ ∀ (a b : DMatrix m n α), a = b
[PROOFSTEP]
simp only [DMatrix, eq_iff_true_of_subsingleton, implies_true]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
α : m → n → Type v
inst✝¹ : (i : m) → (j : n) → Zero (α i j)
β : m → n → Type w
inst✝ : (i : m) → (j : n) → Zero (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j → β i j
h : ∀ (i : m) (j : n), f 0 = 0
⊢ map 0 f = 0
[PROOFSTEP]
ext
[GOAL]
case a
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
α : m → n → Type v
inst✝¹ : (i : m) → (j : n) → Zero (α i j)
β : m → n → Type w
inst✝ : (i : m) → (j : n) → Zero (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j → β i j
h : ∀ (i : m) (j : n), f 0 = 0
i✝ : m
j✝ : n
⊢ map 0 f i✝ j✝ = OfNat.ofNat 0 i✝ j✝
[PROOFSTEP]
simp [h]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
α : m → n → Type v
inst✝¹ : (i : m) → (j : n) → AddMonoid (α i j)
β : m → n → Type w
inst✝ : (i : m) → (j : n) → AddMonoid (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j →+ β i j
M N : DMatrix m n α
⊢ (map (M + N) fun i j => ↑f) = (map M fun i j => ↑f) + map N fun i j => ↑f
[PROOFSTEP]
ext
[GOAL]
case a
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
α : m → n → Type v
inst✝¹ : (i : m) → (j : n) → AddMonoid (α i j)
β : m → n → Type w
inst✝ : (i : m) → (j : n) → AddMonoid (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j →+ β i j
M N : DMatrix m n α
i✝ : m
j✝ : n
⊢ map (M + N) (fun i j => ↑f) i✝ j✝ = ((map M fun i j => ↑f) + map N fun i j => ↑f) i✝ j✝
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
α : m → n → Type v
inst✝¹ : (i : m) → (j : n) → AddGroup (α i j)
β : m → n → Type w
inst✝ : (i : m) → (j : n) → AddGroup (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j →+ β i j
M N : DMatrix m n α
⊢ (map (M - N) fun i j => ↑f) = (map M fun i j => ↑f) - map N fun i j => ↑f
[PROOFSTEP]
ext
[GOAL]
case a
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
α : m → n → Type v
inst✝¹ : (i : m) → (j : n) → AddGroup (α i j)
β : m → n → Type w
inst✝ : (i : m) → (j : n) → AddGroup (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j →+ β i j
M N : DMatrix m n α
i✝ : m
j✝ : n
⊢ map (M - N) (fun i j => ↑f) i✝ j✝ = ((map M fun i j => ↑f) - map N fun i j => ↑f) i✝ j✝
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : Fintype o
α : m → n → Type v
inst✝ : IsEmpty m
M N : DMatrix m n α
⊢ M = N
[PROOFSTEP]
ext i
[GOAL]
case a
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : Fintype o
α : m → n → Type v
inst✝ : IsEmpty m
M N : DMatrix m n α
i : m
j✝ : n
⊢ M i j✝ = N i j✝
[PROOFSTEP]
exact isEmptyElim i
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : Fintype o
α : m → n → Type v
inst✝ : IsEmpty n
M N : DMatrix m n α
⊢ M = N
[PROOFSTEP]
ext i j
[GOAL]
case a
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
inst✝⁴ : Fintype l
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : Fintype o
α : m → n → Type v
inst✝ : IsEmpty n
M N : DMatrix m n α
i : m
j : n
⊢ M i j = N i j
[PROOFSTEP]
exact isEmptyElim j
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
α : m → n → Type v
inst✝¹ : (i : m) → (j : n) → AddMonoid (α i j)
β : m → n → Type w
inst✝ : (i : m) → (j : n) → AddMonoid (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j →+ β i j
⊢ (fun M => DMatrix.map M fun i j => ↑f) 0 = 0
[PROOFSTEP]
simp