Documentation

Foundation.Vorspiel.Vorspiel

def Nat.cases {α : Sort u} (hzero : α 0) (hsucc : (n : ) → α (n + 1)) (n : ) :
α n
Equations
  • (hzero :>ₙ hsucc) x = match x with | 0 => hzero | n.succ => hsucc n
Instances For
    @[simp]
    theorem Nat.cases_zero {α : Sort u} (hzero : α 0) (hsucc : (n : ) → α (n + 1)) :
    (hzero :>ₙ hsucc) 0 = hzero
    @[simp]
    theorem Nat.cases_succ {α : Sort u} (hzero : α 0) (hsucc : (n : ) → α (n + 1)) (n : ) :
    (hzero :>ₙ hsucc) (n + 1) = hsucc n
    @[simp]
    theorem Nat.ne_step_max (n : ) (m : ) :
    n max n m + 1
    @[simp]
    theorem Nat.ne_step_max' (n : ) (m : ) :
    n max m n + 1
    theorem Nat.rec_eq {α : Sort u_1} (a : α) (f₁ : αα) (f₂ : αα) (n : ) (H : m < n, ∀ (a : α), f₁ m a = f₂ m a) :
    Nat.rec a f₁ n = Nat.rec a f₂ n
    theorem Nat.least_number (P : Prop) (hP : ∃ (x : ), P x) :
    ∃ (x : ), P x z < x, ¬P z
    def Nat.toFin (n : ) :
    Option (Fin n)
    Equations
    • n.toFin x = if hx : x < n then some x, hx else none
    Instances For
      theorem eq_finZeroElim {α : Sort u} (x : Fin 0α) :
      x = finZeroElim
      @[simp]
      theorem Matrix.vecCons_zero :
      ∀ {α : Type u_1} {a : α} {n : } {s : Fin nα}, (a :> s) 0 = a
      @[simp]
      theorem Matrix.vecCons_succ {n : } :
      ∀ {α : Type u_1} {a : α} {s : Fin nα} (i : Fin n), (a :> s) i.succ = s i
      @[simp]
      theorem Matrix.vecCons_last {n : } {C : Type u_1} (a : C) (s : Fin (n + 1)C) :
      (a :> s) (Fin.last (n + 1)) = s (Fin.last n)
      def Matrix.vecConsLast {α : Type u} {n : } (t : Fin nα) (h : α) :
      Fin n.succα
      Equations
      Instances For
        @[simp]
        theorem Matrix.cons_app_one {α : Type u} {n : } (a : α) (s : Fin n.succα) :
        (a :> s) 1 = s 0
        @[simp]
        theorem Matrix.cons_app_two {α : Type u} {n : } (a : α) (s : Fin n.succ.succα) :
        (a :> s) 2 = s 1
        @[simp]
        theorem Matrix.cons_app_three {α : Type u} {n : } (a : α) (s : Fin n.succ.succ.succα) :
        (a :> s) 3 = s 2
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem Matrix.rightConcat_last {n : } :
            ∀ {α : Type u_1} {s : Fin nα} {a : α}, (s <: a) (Fin.last n) = a
            @[simp]
            theorem Matrix.rightConcat_castSucc {n : } :
            ∀ {α : Type u_1} {s : Fin nα} {a : α} (i : Fin n), (s <: a) i.castSucc = s i
            @[simp]
            theorem Matrix.rightConcat_zero {n : } {α : Type u} (a : α) (s : Fin n.succα) :
            (s <: a) 0 = s 0
            @[simp]
            theorem Matrix.zero_succ_eq_id {n : } :
            0 :> Fin.succ = id
            @[simp]
            theorem Matrix.zero_cons_succ_eq_self {n : } {α : Type u} (f : Fin (n + 1)α) :
            (f 0 :> fun (x : Fin n) => f x.succ) = f
            theorem Matrix.eq_vecCons {n : } {C : Type u_1} (s : Fin (n + 1)C) :
            s = s 0 :> s Fin.succ
            @[simp]
            theorem Matrix.vecCons_ext {n : } {α : Type u} (a₁ : α) (a₂ : α) (s₁ : Fin nα) (s₂ : Fin nα) :
            a₁ :> s₁ = a₂ :> s₂ a₁ = a₂ s₁ = s₂
            theorem Matrix.vecCons_assoc {n : } {α : Type u} (a : α) (b : α) (s : Fin nα) :
            a :> s <: b = (a :> s) <: b
            def Matrix.decVec {α : Type u_1} {n : } (v : Fin nα) (w : Fin nα) :
            ((i : Fin n) → Decidable (v i = w i))Decidable (v = w)
            Equations
            Instances For
              theorem Matrix.comp_vecCons {n : } {α : Type u} {β : Type u_1} (f : αβ) (a : α) (s : Fin nα) :
              (fun (x : Fin n.succ) => f ((a :> s) x)) = f a :> f s
              theorem Matrix.comp_vecCons' {n : } {α : Type u} {β : Type u_1} (f : αβ) (a : α) (s : Fin nα) :
              (fun (x : Fin n.succ) => f ((a :> s) x)) = f a :> fun (i : Fin n) => f (s i)
              theorem Matrix.comp_vecCons'' {n : } {α : Type u} {β : Type u_1} (f : αβ) (a : α) (s : Fin nα) :
              f (a :> s) = f a :> f s
              @[simp]
              theorem Matrix.comp₀ {α : Type u} :
              ∀ {δ : Type u_1} {f : αδ}, f ![] = ![]
              @[simp]
              theorem Matrix.comp₁ {α : Type u} :
              ∀ {δ : Type u_1} {f : αδ} (a : α), f ![a] = ![f a]
              @[simp]
              theorem Matrix.comp₂ {α : Type u} :
              ∀ {δ : Type u_1} {f : αδ} (a₁ a₂ : α), f ![a₁, a₂] = ![f a₁, f a₂]
              @[simp]
              theorem Matrix.comp₃ {α : Type u} :
              ∀ {δ : Type u_1} {f : αδ} (a₁ a₂ a₃ : α), f ![a₁, a₂, a₃] = ![f a₁, f a₂, f a₃]
              theorem Matrix.comp_vecConsLast {n : } {α : Type u} {β : Type u_1} (f : αβ) (a : α) (s : Fin nα) :
              (fun (x : Fin n.succ) => f ((s <: a) x)) = f s <: f a
              @[simp]
              theorem Matrix.vecHead_comp {n : } {α : Type u} {β : Type u_1} (f : αβ) (v : Fin (n + 1)α) :
              @[simp]
              theorem Matrix.vecTail_comp {n : } {α : Type u} {β : Type u_1} (f : αβ) (v : Fin (n + 1)α) :
              theorem Matrix.vecConsLast_vecEmpty {α : Type u} {s : Fin 0α} (a : α) :
              s <: a = ![a]
              theorem Matrix.constant_eq_singleton {α : Type u} {a : α} :
              (fun (x : Fin (Nat.succ 0)) => a) = ![a]
              theorem Matrix.constant_eq_singleton' {α : Type u} {v : Fin 1α} :
              v = ![v 0]
              theorem Matrix.constant_eq_vec₂ {α : Type u} {a : α} :
              (fun (x : Fin (Nat.succ 0).succ) => a) = ![a, a]
              theorem Matrix.fun_eq_vec₂ {α : Type u} {v : Fin 2α} :
              v = ![v 0, v 1]
              theorem Matrix.injective_vecCons {n : } {α : Type u} {f : Fin nα} (h : Function.Injective f) {a : α} (ha : ∀ (i : Fin n), a f i) :
              def Matrix.toList {α : Type u_1} {n : } :
              (Fin nα)List α
              Equations
              Instances For
                @[simp]
                theorem Matrix.toList_zero {α : Type u_1} (v : Fin 0α) :
                @[simp]
                theorem Matrix.toList_succ {α : Type u_1} {n : } (v : Fin (n + 1)α) :
                Matrix.toList v = v 0 :: Matrix.toList (v Fin.succ)
                @[simp]
                theorem Matrix.toList_length {α : Type u_1} {n : } (v : Fin nα) :
                (Matrix.toList v).length = n
                @[simp]
                theorem Matrix.mem_toList_iff {α : Type u_1} {n : } {v : Fin nα} {a : α} :
                a Matrix.toList v ∃ (i : Fin n), v i = a
                def Matrix.toOptionVec {α : Type u_1} {n : } :
                (Fin nOption α)Option (Fin nα)
                Equations
                Instances For
                  @[simp]
                  theorem Matrix.toOptionVec_some {α : Type u_1} {n : } (v : Fin nα) :
                  (Matrix.toOptionVec fun (i : Fin n) => some (v i)) = some v
                  @[simp]
                  theorem Matrix.toOptionVec_zero {α : Type u_1} (v : Fin 0Option α) :
                  @[simp]
                  theorem Matrix.toOptionVec_eq_none_iff {α : Type u_1} {n : } {v : Fin nOption α} :
                  Matrix.toOptionVec v = none ∃ (i : Fin n), v i = none
                  @[simp]
                  theorem Matrix.toOptionVec_eq_some_iff {α : Type u_1} {n : } {w : Fin nα} {v : Fin nOption α} :
                  Matrix.toOptionVec v = some w ∀ (i : Fin n), v i = some (w i)
                  def Matrix.getM {m : Type u → Type v} [Monad m] {n : } {β : Fin nType u} :
                  ((i : Fin n) → m (β i))m ((i : Fin n) → β i)
                  Equations
                  Instances For
                    theorem Matrix.getM_pure {m : Type u → Type v} [Monad m] [LawfulMonad m] {n : } {β : Fin nType u} (v : (i : Fin n) → β i) :
                    (Matrix.getM fun (i : Fin n) => pure (v i)) = pure v
                    @[simp]
                    theorem Matrix.getM_some {n : } {β : Fin nType u} (v : (i : Fin n) → β i) :
                    (Matrix.getM fun (i : Fin n) => some (v i)) = some v
                    def Matrix.appendr {α : Type w} {n : } {m : } (v : Fin nα) (w : Fin mα) :
                    Fin (m + n)α
                    Equations
                    Instances For
                      @[simp]
                      theorem Matrix.appendr_nil {α : Type w} {m : } (w : Fin mα) :
                      @[simp]
                      theorem Matrix.appendr_cons {α : Type w} {m : } {n : } (x : α) (v : Fin nα) (w : Fin mα) :
                      def Matrix.vecToNat {n : } :
                      (Fin n)
                      Equations
                      Instances For
                        @[simp]
                        theorem Matrix.vecToNat_empty (v : Fin 0) :
                        @[simp]
                        theorem Matrix.encode_succ {n : } (x : ) (v : Fin n) :
                        def DMatrix.vecEmpty {α : Sort u_1} :
                        Fin 0α
                        Equations
                        • DMatrix.vecEmpty = Fin.elim0
                        Instances For
                          def DMatrix.vecCons {n : } {α : Fin (n + 1)Type u_1} (h : α 0) (t : (i : Fin n) → α i.succ) (i : Fin n.succ) :
                          α i
                          Equations
                          Instances For
                            @[simp]
                            theorem DMatrix.vecCons_zero {n : } {α : Fin (n + 1)Type u_1} (h : α 0) (t : (i : Fin n) → α i.succ) :
                            (h ::> t) 0 = h
                            @[simp]
                            theorem DMatrix.vecCons_succ {n : } {α : Fin (n + 1)Type u_1} (h : α 0) (t : (i : Fin n) → α i.succ) (i : Fin n) :
                            (h ::> t) i.succ = t i
                            theorem DMatrix.eq_vecCons {n : } {α : Fin (n + 1)Type u_1} (s : (i : Fin (n + 1)) → α i) :
                            s = s 0 ::> fun (i : Fin n) => s i.succ
                            @[simp]
                            theorem DMatrix.vecCons_ext {n : } {α : Fin (n + 1)Type u_1} (a₁ : α 0) (a₂ : α 0) (s₁ : (i : Fin n) → α i.succ) (s₂ : (i : Fin n) → α i.succ) :
                            a₁ ::> s₁ = a₂ ::> s₂ a₁ = a₂ s₁ = s₂
                            def DMatrix.decVec {n : } {α : Fin nType u_2} (v : (i : Fin n) → α i) (w : (i : Fin n) → α i) (h : (i : Fin n) → Decidable (v i = w i)) :
                            Decidable (v = w)
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              theorem Option.pure_eq_some {α : Type u_1} (a : α) :
                              pure a = some a
                              @[simp]
                              theorem Option.toList_eq_iff {α : Type u_1} {o : Option α} {a : α} :
                              o.toList = [a] o = some a
                              def Nat.natToVec :
                              (n : ) → Option (Fin n)
                              Equations
                              Instances For
                                @[simp]
                                theorem Nat.natToVec_vecToNat {n : } (v : Fin n) :
                                (Matrix.vecToNat v).natToVec n = some v
                                theorem Nat.lt_of_eq_natToVec {n : } {e : } {v : Fin n} (h : e.natToVec n = some v) (i : Fin n) :
                                v i < e
                                theorem Nat.one_le_of_bodd {n : } (h : n.bodd = true) :
                                1 n
                                theorem Nat.pair_le_pair_of_le {a₁ : } {a₂ : } {b₁ : } {b₂ : } (ha : a₁ a₂) (hb : b₁ b₂) :
                                Nat.pair a₁ b₁ Nat.pair a₂ b₂
                                theorem Fin.pos_of_coe_ne_zero {n : } {i : Fin (n + 1)} (h : i 0) :
                                0 < i
                                @[simp]
                                theorem Fin.one_pos'' {n : } :
                                0 < 1
                                @[simp]
                                theorem Fin.two_pos {n : } :
                                0 < 2
                                @[simp]
                                theorem Fin.three_pos {n : } :
                                0 < 3
                                @[simp]
                                theorem Fin.four_pos {n : } :
                                0 < 4
                                @[simp]
                                theorem Fin.five_pos {n : } :
                                0 < 5
                                def Fintype.sup {ι : Type u_1} [Fintype ι] {α : Type u_2} [SemilatticeSup α] [OrderBot α] (f : ια) :
                                α
                                Equations
                                Instances For
                                  @[simp]
                                  theorem Fintype.elem_le_sup {ι : Type u_2} [Fintype ι] {α : Type u_1} [SemilatticeSup α] [OrderBot α] (f : ια) (i : ι) :
                                  theorem Fintype.le_sup {ι : Type u_2} [Fintype ι] {α : Type u_1} [SemilatticeSup α] [OrderBot α] {a : α} {f : ια} (i : ι) (le : a f i) :
                                  @[simp]
                                  theorem Fintype.sup_le_iff {ι : Type u_2} [Fintype ι] {α : Type u_1} [SemilatticeSup α] [OrderBot α] {f : ια} {a : α} :
                                  Fintype.sup f a ∀ (i : ι), f i a
                                  @[simp]
                                  theorem Fintype.finsup_eq_0_of_empty {ι : Type u_1} [Fintype ι] {α : Type u_2} [SemilatticeSup α] [OrderBot α] [IsEmpty ι] (f : ια) :
                                  def Fintype.decideEqPi {ι : Type u_2} [Fintype ι] {β : ιType u_1} (a : (i : ι) → β i) (b : (i : ι) → β i) :
                                  ((i : ι) → Decidable (a i = b i))Decidable (a = b)
                                  Equations
                                  Instances For
                                    def String.vecToStr {n : } :
                                    (Fin nString)String
                                    Equations
                                    Instances For
                                      theorem Empty.eq_elim {α : Sort u} (f : Emptyα) :
                                      f = Empty.elim
                                      theorem IsEmpty.eq_elim {o : Sort u} (h : IsEmpty o) {α : Sort u_1} (f : oα) :
                                      f = h.elim'
                                      def Function.funEqOn {α : Type u} {β : Type v} (p : αProp) (f : αβ) (g : αβ) :
                                      Equations
                                      Instances For
                                        theorem Function.funEqOn.of_subset {α : Type u} {β : Type v} {p : αProp} {q : αProp} {f : αβ} {g : αβ} (e : Function.funEqOn p f g) (h : ∀ (a : α), q ap a) :
                                        theorem Quotient.inductionOnVec {α : Type u} [s : Setoid α] {n : } {p : (Fin nQuotient s)Prop} (v : Fin nQuotient s) (h : ∀ (v : Fin nα), p fun (i : Fin n) => v i) :
                                        p v
                                        def Quotient.liftVec {α : Type u} [s : Setoid α] {β : Sort v} {n : } (f : (Fin nα)β) :
                                        (∀ (v₁ v₂ : Fin nα), (∀ (n : Fin n), v₁ n v₂ n)f v₁ = f v₂)(Fin nQuotient s)β
                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        • Quotient.liftVec f x_4 x_5 = f ![]
                                        Instances For
                                          @[simp]
                                          theorem Quotient.liftVec_zero {α : Type u} [s : Setoid α] {β : Sort v} (f : (Fin 0α)β) (h : ∀ (v₁ v₂ : Fin 0α), (∀ (n : Fin 0), v₁ n v₂ n)f v₁ = f v₂) (v : Fin 0Quotient s) :
                                          Quotient.liftVec f h v = f ![]
                                          theorem Quotient.liftVec_mk {α : Type u} [s : Setoid α] {β : Sort v} {n : } (f : (Fin nα)β) (h : ∀ (v₁ v₂ : Fin nα), (∀ (n : Fin n), v₁ n v₂ n)f v₁ = f v₂) (v : Fin nα) :
                                          @[simp]
                                          theorem Quotient.liftVec_mk₁ {α : Type u} [s : Setoid α] {β : Sort v} (f : (Fin 1α)β) (h : ∀ (v₁ v₂ : Fin 1α), (∀ (n : Fin 1), v₁ n v₂ n)f v₁ = f v₂) (a : α) :
                                          Quotient.liftVec f h ![a] = f ![a]
                                          @[simp]
                                          theorem Quotient.liftVec_mk₂ {α : Type u} [s : Setoid α] {β : Sort v} (f : (Fin 2α)β) (h : ∀ (v₁ v₂ : Fin 2α), (∀ (n : Fin 2), v₁ n v₂ n)f v₁ = f v₂) (a₁ : α) (a₂ : α) :
                                          Quotient.liftVec f h ![a₁, a₂] = f ![a₁, a₂]
                                          def List.subsetSet {α : Type u_1} (l : List α) (s : Set α) [DecidablePred s] :
                                          Equations
                                          Instances For
                                            Equations
                                            • [].upper = 0
                                            • (n :: ns).upper = max (n + 1) ns.upper
                                            Instances For
                                              @[simp]
                                              theorem List.upper_nil :
                                              [].upper = 0
                                              @[simp]
                                              theorem List.upper_cons (n : ) (ns : List ) :
                                              (n :: ns).upper = max (n + 1) ns.upper
                                              theorem List.lt_upper (l : List ) {n : } (h : n l) :
                                              n < l.upper
                                              theorem List.toFinset_map {α : Type u} [DecidableEq α] {β : Type v} [DecidableEq β] {f : αβ} (l : List α) :
                                              (List.map f l).toFinset = Finset.image f l.toFinset
                                              theorem List.toFinset_mono {α : Type u} [DecidableEq α] {l : List α} {l' : List α} (h : l l') :
                                              l.toFinset l'.toFinset
                                              def List.sup {α : Type u} [SemilatticeSup α] [OrderBot α] :
                                              List αα
                                              Equations
                                              Instances For
                                                @[simp]
                                                theorem List.sup_nil {α : Type u} [SemilatticeSup α] [OrderBot α] :
                                                [].sup =
                                                @[simp]
                                                theorem List.sup_cons {α : Type u} [SemilatticeSup α] [OrderBot α] (a : α) (as : List α) :
                                                (a :: as).sup = a as.sup
                                                theorem List.le_sup {α : Type u} [SemilatticeSup α] [OrderBot α] {a : α} {l : List α} :
                                                a la l.sup
                                                theorem List.getI_map_range {α : Type u} {i : } {n : } [Inhabited α] (f : α) (h : i < n) :
                                                (List.map f (List.range n)).getI i = f i
                                                theorem List.sup_ofFn {α : Type u} [SemilatticeSup α] [OrderBot α] {n : } (f : Fin nα) :
                                                (List.ofFn f).sup = Finset.univ.sup f
                                                theorem List.ofFn_get_eq_map_cast {α : Type u} {β : Type v} {n : } (g : αβ) (as : List α) {h : n = as.length} :
                                                (List.ofFn fun (i : Fin n) => g (as.get (Fin.cast h i))) = List.map g as
                                                theorem List.take_map_range {α : Type u} {n : } {m : } (f : α) :
                                                theorem List.bind_toList_some {α : Type u} {β : Type v} {f : βOption α} {g : βα} {bs : List β} (h : xbs, f x = some (g x)) :
                                                (bs.bind fun (i : β) => (f i).toList) = List.map g bs
                                                theorem List.mapM'_eq_none_iff {α : Type u_2} {β : Type u_1} {f : αOption β} {l : List α} :
                                                mapM' f l = none al, f a = none
                                                theorem List.length_mapM' {α : Type u_2} {β : Type u_1} {bs : List β} {f : αOption β} {as : List α} :
                                                mapM' f as = some bsbs.length = as.length
                                                theorem List.mapM'_mem_inversion {α : Type u_2} {β : Type u_1} {bs : List β} {b : β} {f : αOption β} {as : List α} (h : mapM' f as = some bs) (hb : b bs) :
                                                ∃ (a : α), f a = some b
                                                theorem List.mapM'_eq_mapM'_of_eq {m : Type u_3 → Type u_2} {α : Type u_1} {β : Type u_3} [Monad m] {f : αm β} {g : αm β} (l : List α) (hf : al, f a = g a) :
                                                mapM' f l = mapM' g l
                                                theorem List.mapM'_option_map {α : Type u_3} {β : Type u_2} {γ : Type u_1} {f : αOption β} {g : βγ} (as : List α) :
                                                mapM' (fun (a : α) => Option.map g (f a)) as = Option.map (fun (bs : List β) => List.map g bs) (mapM' f as)
                                                def List.allSome' {α : Type u_1} :
                                                List (Option α)Option (List α)
                                                Equations
                                                Instances For
                                                  @[simp]
                                                  theorem List.mapM_eq_map {α : Type u_1} {β : Type u_2} (l : List α) (f : αβ) :
                                                  mapM' (fun (x : α) => some (f x)) l = some (List.map f l)
                                                  theorem List.mapM_map {α : Type u_2} {β : Type u_3} {γ : Type u_1} (as : List α) (f : αOption β) (g : Option βOption γ) :
                                                  mapM' g (List.map f as) = mapM' (g f) as
                                                  @[simp]
                                                  theorem List.allSome_map_some {α : Type u_1} {β : Type u_2} (l : List α) (f : αβ) :
                                                  (List.map (fun (x : α) => some (f x)) l).allSome' = some (List.map f l)
                                                  theorem List.append_subset_append {α : Type u_1} {l₁ : List α} {l₂ : List α} {l : List α} (h : l₁ l₂) :
                                                  l₁ ++ l l₂ ++ l
                                                  theorem List.subset_of_eq {α : Type u_1} {l₁ : List α} {l₂ : List α} (e : l₁ = l₂) :
                                                  l₁ l₂
                                                  theorem List.nil_iff {α : Type u_1} {l : List α} :
                                                  l = [] ∀ (a : α), al
                                                  def List.remove {α : Type u_1} [DecidableEq α] (a : α) :
                                                  List αList α
                                                  Equations
                                                  Instances For
                                                    @[simp]
                                                    theorem List.remove_nil {α : Type u_1} [DecidableEq α] (a : α) :
                                                    List.remove a [] = []
                                                    @[simp]
                                                    theorem List.eq_remove_cons {α : Type u_1} [DecidableEq α] {q : α} {l : List α} :
                                                    @[simp]
                                                    theorem List.remove_singleton_of_ne {α : Type u_1} [DecidableEq α] {p : α} {q : α} (h : p q) :
                                                    List.remove q [p] = [p]
                                                    theorem List.mem_remove_iff {α : Type u_1} [DecidableEq α] {b : α} {a : α} {l : List α} :
                                                    b List.remove a l b l b a
                                                    theorem List.mem_of_mem_remove {α : Type u_1} [DecidableEq α] {a : α} {b : α} {l : List α} (h : b List.remove a l) :
                                                    b l
                                                    @[simp]
                                                    theorem List.remove_cons_self {α : Type u_1} [DecidableEq α] (l : List α) (a : α) :
                                                    theorem List.remove_cons_of_ne {α : Type u_1} [DecidableEq α] (l : List α) {a : α} {b : α} (ne : a b) :
                                                    List.remove b (a :: l) = a :: List.remove b l
                                                    theorem List.remove_subset {α : Type u_1} [DecidableEq α] (a : α) (l : List α) :
                                                    theorem List.remove_subset_remove {α : Type u_1} [DecidableEq α] (a : α) {l₁ : List α} {l₂ : List α} (h : l₁ l₂) :
                                                    theorem List.remove_cons_subset_cons_remove {α : Type u_1} [DecidableEq α] (a : α) (b : α) (l : List α) :
                                                    theorem List.remove_map_substet_map_remove {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (f : αβ) (l : List α) (a : α) :
                                                    theorem Mathlib.Vector.get_mk_eq_get {α : Type u_1} {n : } (l : List α) (h : l.length = n) (i : Fin n) :
                                                    Mathlib.Vector.get l, h i = l.get (Fin.cast i)
                                                    theorem Mathlib.Vector.get_one {α : Type u_2} {n : } (v : Mathlib.Vector α (n + 2)) :
                                                    v.get 1 = v.tail.head
                                                    theorem Mathlib.Vector.ofFn_vecCons {α : Type u_1} {n : } (a : α) (v : Fin nα) :
                                                    noncomputable def Finset.rangeOfFinite {α : Type u} {ι : Sort v} [Finite ι] (f : ια) :
                                                    Equations
                                                    Instances For
                                                      theorem Finset.mem_rangeOfFinite_iff {α : Type u} {ι : Sort v} [Finite ι] {f : ια} {a : α} :
                                                      a Finset.rangeOfFinite f ∃ (i : ι), f i = a
                                                      noncomputable def Finset.imageOfFinset {α : Type u} {β : Type v} [DecidableEq β] (s : Finset α) (f : (a : α) → a sβ) :
                                                      Equations
                                                      Instances For
                                                        theorem Finset.mem_imageOfFinset_iff {α : Type u} {β : Type v} [DecidableEq β] {s : Finset α} {f : (a : α) → a sβ} {b : β} :
                                                        b s.imageOfFinset f ∃ (a : α) (ha : a s), f a ha = b
                                                        @[simp]
                                                        theorem Finset.mem_imageOfFinset {α : Type u} {β : Type v} [DecidableEq β] {s : Finset α} (f : (a : α) → a sβ) (a : α) (ha : a s) :
                                                        f a ha s.imageOfFinset f
                                                        theorem Finset.erase_union {α : Type u} [DecidableEq α] {a : α} {s : Finset α} {t : Finset α} :
                                                        (s t).erase a = s.erase a t.erase a
                                                        @[simp]
                                                        theorem Finset.equiv_univ {α : Type u_1} {α' : Type u_2} [Fintype α] [Fintype α'] [DecidableEq α'] (e : α α') :
                                                        Finset.image (e) Finset.univ = Finset.univ
                                                        @[simp]
                                                        theorem Finset.sup_univ_equiv {β : Type v} {α : Type u_1} {α' : Type u_2} [DecidableEq α] [Fintype α] [Fintype α'] [SemilatticeSup β] [OrderBot β] (f : αβ) (e : α' α) :
                                                        (Finset.univ.sup fun (i : α') => f (e i)) = Finset.univ.sup f
                                                        theorem Finset.sup_univ_list_eq_sup_map {σ : Type u_1} {α : Type u_2} [SemilatticeSup α] [OrderBot α] (l : List σ) (f : σα) :
                                                        (Finset.univ.sup fun (i : Fin l.length) => f l[i]) = (List.map f l).sup
                                                        theorem Finset.sup_univ_cast {α : Type u_1} [SemilatticeSup α] [OrderBot α] {n : } (f : Fin nα) (n' : ) {h : n' = n} :
                                                        (Finset.univ.sup fun (i : Fin n') => f (Fin.cast h i)) = Finset.univ.sup f
                                                        @[irreducible]
                                                        theorem Denumerable.lt_of_mem_list (n : ) (i : ) :
                                                        @[simp]
                                                        theorem Part.mem_vector_mOfFn {α : Type u_1} {n : } {w : Mathlib.Vector α n} {v : Fin n →. α} :
                                                        w Mathlib.Vector.mOfFn v ∀ (i : Fin n), w.get i v i
                                                        theorem Set.subset_mem_chain_of_finite {α : Type u_1} (c : Set (Set α)) (hc : c.Nonempty) (hchain : IsChain (fun (x x_1 : Set α) => x x_1) c) {s : Set α} (hfin : s.Finite) :
                                                        s ⋃₀ ctc, s t
                                                        class Exp (α : Type u_1) :
                                                        Type u_1
                                                        • exp : αα
                                                        Instances
                                                          @[simp]
                                                          theorem Set.subset_triunion₁ {F : Type u_1} (s₁ : Set F) (s₂ : Set F) (s₃ : Set F) :
                                                          s₁ s₁ s₂ s₃
                                                          @[simp]
                                                          theorem Set.subset_triunion₂ {F : Type u_1} (s₁ : Set F) (s₂ : Set F) (s₃ : Set F) :
                                                          s₂ s₁ s₂ s₃
                                                          @[simp]
                                                          theorem Set.subset_triunion₃ {F : Type u_1} (s₁ : Set F) (s₂ : Set F) (s₃ : Set F) :
                                                          s₃ s₁ s₂ s₃
                                                          @[simp]
                                                          theorem Set.subset_tetraunion₁ {F : Type u_1} (s₁ : Set F) (s₂ : Set F) (s₃ : Set F) (s₄ : Set F) :
                                                          s₁ s₁ s₂ s₃ s₄
                                                          @[simp]
                                                          theorem Set.subset_tetraunion₂ {F : Type u_1} (s₁ : Set F) (s₂ : Set F) (s₃ : Set F) (s₄ : Set F) :
                                                          s₂ s₁ s₂ s₃ s₄
                                                          @[simp]
                                                          theorem Set.subset_tetraunion₃ {F : Type u_1} (s₁ : Set F) (s₂ : Set F) (s₃ : Set F) (s₄ : Set F) :
                                                          s₃ s₁ s₂ s₃ s₄
                                                          @[simp]
                                                          theorem Set.subset_tetraunion₄ {F : Type u_1} (s₁ : Set F) (s₂ : Set F) (s₃ : Set F) (s₄ : Set F) :
                                                          s₄ s₁ s₂ s₃ s₄
                                                          class Atleast (n : ℕ+) (α : Sort u_1) :

                                                          Class for α has at least n elements

                                                          Instances
                                                            theorem Atleast.mapping {n : ℕ+} {α : Sort u_1} [self : Atleast n α] :
                                                            ∃ (f : Fin nα), Function.HasLeftInverse f