mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.hf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.IsGrothendieckAbelian.{w, v, u} C] {X : C} {J : Type w}
  [inst_3 : CategoryTheory.SmallCategory J] {Y : CategoryTheory.Functor J C} {j₀ : J} (y : X ⟶ Y.obj j₀)
  (j : CategoryTheory.Under j₀),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι
        (CategoryTheory.Limits.kernel (CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.g y)) j)
      (CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.f y) =
    (CategoryTheory.Limits.kernel.ι (CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.g y)).app j
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey!_inter_of_mem_right : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {k : α}, k ∈ m₂ → (m₁ ∩ m₂).getKey! k = m₁.getKey! k
-- Init.Data.Option.Lemmas
Option.pbind_eq_some_iff : ∀ {α : Type u_1} {β : Type u_2} {o : Option α} {f : (a : α) → o = some a → Option β} {b : β},
  o.pbind f = some b ↔ ∃ a, ∃ (h : o = some a), f a h = some b
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
hasSum_ite_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] (b : β)
  [inst_2 : DecidablePred fun x => x = b] (a : α) (L : optParam (SummationFilter β) (SummationFilter.unconditional β))
  [L.LeAtTop], HasSum (fun b' => if b' = b then a else 0) a L
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.updateCol.congr_simp : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {inst : DecidableEq n} [inst_1 : DecidableEq n] (M M_1 : Matrix m n α),
  M = M_1 →
    ∀ (j j_1 : n),
      j = j_1 →
        ∀ (b b_1 : m → α),
          b = b_1 →
            ∀ (a a_1 : m), a = a_1 → ∀ (a_2 a_3 : n), a_2 = a_3 → M.updateCol j b a a_2 = M_1.updateCol j_1 b_1 a_1 a_3
-- Lean.Meta.Tactic.Grind.AC.Types
/-- Disequalities.  -/
Lean.Meta.Grind.AC.Struct.diseqs : Lean.Meta.Grind.AC.Struct → Lean.PArray Lean.Meta.Grind.AC.DiseqCnstr
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.pullback_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X},
  CategoryTheory.Sieve.pullback (CategoryTheory.CategoryStruct.id X) S = S
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.map₂Iso_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {A : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] {L : D} {R : CategoryTheory.Functor C D} {L' : B}
  {R' : CategoryTheory.Functor A B} {F : C ≌ A} {G : D ≌ B} (α : L' ⟶ G.functor.obj L) (α' : L ⟶ G.inverse.obj L')
  (β : R.comp G.functor ⟶ F.functor.comp R') (β' : R'.comp G.inverse ⟶ F.inverse.comp R)
  (hαα' : CategoryTheory.CategoryStruct.comp α (G.functor.map α') = G.counitIso.inv.app L')
  (hα'α : CategoryTheory.CategoryStruct.comp α' (G.inverse.map α) = G.unitIso.hom.app L)
  (hββ' :
    CategoryTheory.CategoryStruct.comp R.rightUnitor.hom
        (CategoryTheory.CategoryStruct.comp R.leftUnitor.inv
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight F.unitIso.hom R)
            (F.functor.associator F.inverse R).hom)) =
      CategoryTheory.CategoryStruct.comp (R.whiskerLeft G.unitIso.hom)
        (CategoryTheory.CategoryStruct.comp (R.associator G.functor G.inverse).inv
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight β G.inverse)
            (CategoryTheory.CategoryStruct.comp (F.functor.associator R' G.inverse).hom (F.functor.whiskerLeft β')))))
  (hβ'β :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight β' G.functor)
        (CategoryTheory.CategoryStruct.comp (F.inverse.associator R G.functor).hom
          (CategoryTheory.CategoryStruct.comp (F.inverse.whiskerLeft β)
            (CategoryTheory.CategoryStruct.comp (F.inverse.associator F.functor R').inv
              (CategoryTheory.Functor.whiskerRight F.counitIso.hom R')))) =
      CategoryTheory.CategoryStruct.comp (R'.associator G.inverse G.functor).hom
        (CategoryTheory.CategoryStruct.comp (R'.whiskerLeft G.counitIso.hom)
          (CategoryTheory.CategoryStruct.comp R'.rightUnitor.hom R'.leftUnitor.inv))),
  (CategoryTheory.StructuredArrow.map₂Iso α α' β β' hαα' hα'α hββ' hβ'β).inverse =
    CategoryTheory.StructuredArrow.map₂ α' β'
-- Mathlib.Algebra.Order.Ring.Defs
IsOrderedRing.mk : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [toIsOrderedAddMonoid : IsOrderedAddMonoid R]
  [toZeroLEOneClass : ZeroLEOneClass R] [toPosMulMono : PosMulMono R] [toMulPosMono : MulPosMono R], IsOrderedRing R
-- Mathlib.Algebra.Group.ForwardDiff
fwdDiff_iter_finsetSum : ∀ {M : Type u_1} {G : Type u_2} [inst : AddCommMonoid M] [inst_1 : AddCommGroup G] (h : M) {α : Type u_3} (s : Finset α)
  (f : α → M → G) (n : ℕ), (fwdDiff h)^[n] (∑ k ∈ s, f k) = ∑ k ∈ s, (fwdDiff h)^[n] (f k)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.forIn_eq_forIn : ∀ {α : Type u} {m : Std.HashSet.Raw α} {δ : Type v} {m' : Type v → Type w} [inst : Monad m'] [LawfulMonad m']
  {f : α → δ → m' (ForInStep δ)} {init : δ}, Std.HashSet.Raw.forIn f init m = forIn m init f
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
/-- Represents a permutation as product of disjoint cycles:
```
#eval (c[0, 1, 2, 3] : Perm (Fin 4))
-- c[0, 1, 2, 3]

#eval (c[3, 1] * c[0, 2] : Perm (Fin 4))
-- c[0, 2] * c[1, 3]

#eval (c[1, 2, 3] * c[0, 1, 2] : Perm (Fin 4))
-- c[0, 2] * c[1, 3]

#eval (c[1, 2, 3] * c[0, 1, 2] * c[3, 1] * c[0, 2] : Perm (Fin 4))
-- 1
```
 -/
Equiv.Perm.instRepr : {α : Type u_1} → [Fintype α] → [DecidableEq α] → [Repr α] → Repr (Equiv.Perm α)
-- Init.Tactics
/-- Applies the first constructor when
the goal is an inductive type with exactly two constructors, or fails otherwise.
```
example : True ∨ False := by
  left
  trivial
```
 -/
Lean.Parser.Tactic.left : Lean.ParserDescr
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.updateAllBuckets.eq_1 : ∀ {α : Type u} {β : α → Type v} {δ : α → Type w} (self : Array (Std.DHashMap.Internal.AssocList α β))
  (f : Std.DHashMap.Internal.AssocList α β → Std.DHashMap.Internal.AssocList α δ),
  Std.DHashMap.Internal.updateAllBuckets self f = Array.map f self
-- Mathlib.Algebra.Order.SuccPred
Order.IsSuccPrelimit.add_one_lt : ∀ {α : Type u_1} {x y : α} [inst : PartialOrder α] [inst_1 : Add α] [inst_2 : One α] [SuccAddOrder α],
  Order.IsSuccPrelimit x → y < x → y + 1 < x
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.Truncated.mapHomotopyCategory_obj : ∀ {V W : SSet.Truncated 2} (f : V ⟶ W)
  (x : V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 })),
  (SSet.Truncated.mapHomotopyCategory f).obj (SSet.Truncated.HomotopyCategory.mk x) =
    SSet.Truncated.HomotopyCategory.mk
      ((CategoryTheory.ConcreteCategory.hom
          (f.app (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 })))
        x)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get?_eq_get? : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.LawfulEqCmp cmp] [inst_1 : Std.TransCmp cmp] {a : α}, Std.ExtDTreeMap.Const.get? t a = t.get? a
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.negAt_apply_isReal_and_mem : ∀ {K : Type u_1} [inst : Field K] {s : Set { w // w.IsReal }} (x : NumberField.mixedEmbedding.mixedSpace K)
  {w : { w // w.IsReal }}, w ∈ s → ((NumberField.mixedEmbedding.negAt s) x).1 w = -x.1 w
-- Mathlib.Analysis.CStarAlgebra.Module.Defs
CStarModule.toInner : {A : Type u_1} →
  {E : Type u_2} →
    {inst : NonUnitalSemiring A} →
      {inst_1 : StarRing A} →
        {inst_2 : Module ℂ A} →
          {inst_3 : AddCommGroup E} →
            {inst_4 : Module ℂ E} →
              {inst_5 : PartialOrder A} →
                {inst_6 : SMul A E} → {inst_7 : Norm A} → {inst_8 : Norm E} → [self : CStarModule A E] → Inner A E
-- Std.Data.DTreeMap.Raw.Basic
/-- If there is no mapping for the given key, inserts the given mapping into the map. Otherwise,
returns the map unaltered.
 -/
Std.DTreeMap.Raw.insertIfNew : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → (a : α) → β a → Std.DTreeMap.Raw α β cmp
-- Mathlib.Analysis.BoxIntegral.Partition.Split
BoxIntegral.Prepartition.iUnion_splitMany : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι) (s : Finset (ι × ℝ)), (BoxIntegral.Prepartition.splitMany I s).iUnion = ↑I
-- Mathlib.Data.Fintype.Card
Fintype.card_lex : ∀ (α : Type u_4) [inst : Fintype α], Fintype.card (Lex α) = Fintype.card α
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
extChartAt_target_mem_nhdsWithin : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} [inst_5 : ChartedSpace H M] (x : M),
  (extChartAt I x).target ∈ nhdsWithin (↑(extChartAt I x) x) (Set.range ↑I)
-- Mathlib.Order.Heyting.Boundary
Coheyting.boundary_eq_bot : ∀ {α : Type u_1} [inst : BooleanAlgebra α] (a : α), Coheyting.boundary a = ⊥
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- An anisotropic quadratic map is zero only on zero vectors.  -/
QuadraticMap.Anisotropic : {R : Type u_3} →
  {M : Type u_4} →
    {N : Type u_5} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid N] → [inst_3 : Module R M] → [inst_4 : Module R N] → QuadraticMap R M N → Prop
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mk : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    {B : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
        {T : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} T] →
            {L : CategoryTheory.Functor A T} →
              {R : CategoryTheory.Functor B T} →
                {P : CategoryTheory.MorphismProperty T} →
                  {Q : CategoryTheory.MorphismProperty A} →
                    {W : CategoryTheory.MorphismProperty B} →
                      (toComma : CategoryTheory.Comma L R) →
                        P toComma.hom → CategoryTheory.MorphismProperty.Comma L R P Q W
-- Lean.Structure
Lean.StructureParentInfo.mk.sizeOf_spec : ∀ (structName : Lean.Name) (subobject : Bool) (projFn : Lean.Name),
  sizeOf { structName := structName, subobject := subobject, projFn := projFn } =
    1 + sizeOf structName + sizeOf subobject + sizeOf projFn
-- Init.Data.Vector.Perm
Vector.Perm.of_toList_perm : ∀ {α : Type u_1} {n : ℕ} {as bs : Vector α n}, as.toList.Perm bs.toList → as.Perm bs
-- Init.Data.Array.Sort.Lemmas
_private.Init.Data.Array.Sort.Lemmas.0.List.mergeSort.match_1.splitter : {α : Type u_1} →
  (motive : List α → (α → α → Bool) → Sort u_2) →
    (x : List α) →
      (x_1 : α → α → Bool) →
        ((x : α → α → Bool) → motive [] x) →
          ((a : α) → (x : α → α → Bool) → motive [a] x) →
            ((a b : α) → (xs : List α) → (le : α → α → Bool) → motive (a :: b :: xs) le) → motive x x_1
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.DiseqCnstrProof.simp_prefix.inj : ∀ {lhs : Bool} {s : Lean.Grind.AC.Seq} {c₁ : Lean.Meta.Grind.AC.EqCnstr} {c₂ : Lean.Meta.Grind.AC.DiseqCnstr}
  {lhs_1 : Bool} {s_1 : Lean.Grind.AC.Seq} {c₁_1 : Lean.Meta.Grind.AC.EqCnstr} {c₂_1 : Lean.Meta.Grind.AC.DiseqCnstr},
  Lean.Meta.Grind.AC.DiseqCnstrProof.simp_prefix lhs s c₁ c₂ =
      Lean.Meta.Grind.AC.DiseqCnstrProof.simp_prefix lhs_1 s_1 c₁_1 c₂_1 →
    lhs = lhs_1 ∧ s = s_1 ∧ c₁ = c₁_1 ∧ c₂ = c₂_1
-- Init.Data.List.MinMaxOn
List.max_eq_min : ∀ {α : Type u_1} {max : Max α} {xs : List α} {h : xs ≠ []}, xs.max h = xs.min h
-- Mathlib.CategoryTheory.Limits.Cones
/-- `mapCocone` is the left inverse to `mapCoconeInv`.  -/
CategoryTheory.Functor.mapCoconeMapCoconeInv : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {D : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} D] →
            {F : CategoryTheory.Functor J D} →
              (H : CategoryTheory.Functor D C) →
                [inst_3 : H.IsEquivalence] →
                  (c : CategoryTheory.Limits.Cocone (F.comp H)) → H.mapCocone (H.mapCoconeInv c) ≅ c
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_unitOfList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α},
  Std.DHashMap.Const.get? (Std.DHashMap.Const.unitOfList l) k = if l.contains k = true then some () else none
-- Init.Prelude
/-- Lifts a fully-polymorphic transformation of `m` into `n`.
 -/
MonadFunctor.monadMap : {m : semiOutParam (Type u → Type v)} →
  {n : Type u → Type w} → [self : MonadFunctor m n] → {α : Type u} → ({β : Type u} → m β → m β) → n α → n α
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.rightUnitor_inv_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X X' : C}
  (f : X ⟶ X') {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X' (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ⟶ Z),
  CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X').inv h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight f (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) h)
-- Init.Data.ToString.Basic
instToStringSubtype : {α : Type u} → {p : α → Prop} → [ToString α] → ToString (Subtype p)
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.Approx.CofixA.intro.hcongr_4 : ∀ (F F' : PFunctor.{uA, uB}),
  F = F' →
    ∀ (n n' : ℕ),
      n = n' →
        ∀ (a : F.A) (a' : F'.A),
          a ≍ a' →
            ∀ (a_1 : F.B a → PFunctor.Approx.CofixA F n) (a'_1 : F'.B a' → PFunctor.Approx.CofixA F' n'),
              a_1 ≍ a'_1 → PFunctor.Approx.CofixA.intro a a_1 ≍ PFunctor.Approx.CofixA.intro a' a'_1
-- Mathlib.GroupTheory.GroupExtension.Defs
/-- See Note [custom simps projection].  -/
AddGroupExtension.Equiv.Simps.symm_apply : {N : Type u_1} →
  {E : Type u_2} →
    {G : Type u_3} →
      [inst : AddGroup N] →
        [inst_1 : AddGroup E] →
          [inst_2 : AddGroup G] →
            {S : AddGroupExtension N E G} →
              {E' : Type u_4} → [inst_3 : AddGroup E'] → {S' : AddGroupExtension N E' G} → S.Equiv S' → E' → E
-- Mathlib.MeasureTheory.Order.Lattice
/-- Eta-expanded form of `AEMeasurable.sup` -/
AEMeasurable.fun_sup : ∀ {M : Type u_1} [inst : MeasurableSpace M] {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f g : α → M} [inst_1 : Max M] [MeasurableSup₂ M],
  AEMeasurable f μ → AEMeasurable g μ → AEMeasurable (fun i => f i ⊔ g i) μ
-- Mathlib.RingTheory.Ideal.Maps
Ideal.comap_comap : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {T : Type u_3} [inst_2 : Semiring T] {I : Ideal T}
  (f : R →+* S) (g : S →+* T), Ideal.comap f (Ideal.comap g I) = Ideal.comap (g.comp f) I
-- Mathlib.Data.PNat.Xgcd
/-- Final value of `w`  -/
PNat.gcdW : ℕ+ → ℕ+ → ℕ+
-- Mathlib.AlgebraicGeometry.Cover.Directed
/-- If `𝒰` is a directed cover of `X`, this is the cover of `𝒰ᵢ ×[X] 𝒰ⱼ` by `{𝒰ₖ}` where
`k ≤ i` and `k ≤ j`.  -/
AlgebraicGeometry.Scheme.Cover.intersectionOfLocallyDirected : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  {X : AlgebraicGeometry.Scheme} →
    (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) →
      [inst : CategoryTheory.Category.{v_1, u_1} 𝒰.I₀] →
        [𝒰.LocallyDirected] →
          [P.IsStableUnderBaseChange] →
            [P.HasOfPostcompProperty P] →
              (i j : 𝒰.I₀) →
                AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P)
                  (CategoryTheory.Limits.pullback (𝒰.f i) (𝒰.f j))
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.zero_vlt_iff : ∀ {K : Type u_2} [inst : DivisionRing K] [inst_1 : ValuativeRel K] {a : K}, 0 <ᵥ a ↔ a ≠ 0
-- Mathlib.Order.Filter.AtTopBot.Field
/-- If a function `f` tends to negative infinity along a filter, then `f` divided by
a positive constant also tends to negative infinity.  -/
Filter.Tendsto.atBot_div_const : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {l : Filter β}
  {f : β → α} {r : α}, 0 < r → Filter.Tendsto f l Filter.atBot → Filter.Tendsto (fun x => f x / r) l Filter.atBot
-- Mathlib.Algebra.BigOperators.GroupWithZero.Action
Multiset.smul_prod' : ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : CommMonoid N] [inst_2 : MulDistribMulAction M N] {r : M}
  {s : Multiset N}, r • s.prod = (Multiset.map (fun x => r • x) s).prod
-- Mathlib.Analysis.Normed.Unbundled.FiniteExtension
/-- For any `K`-basis `B` of `L` containing `1`, `B.norm` extends the norm on `K`.  -/
Module.Basis.norm_extends : ∀ {K : Type u_1} {L : Type u_2} [inst : NormedField K] [inst_1 : Ring L] [inst_2 : Algebra K L] {ι : Type u_3}
  [inst_3 : Fintype ι] [inst_4 : Nonempty ι] {B : Module.Basis ι K L} {i : ι},
  B i = 1 → ∀ (x : K), B.norm ((algebraMap K L) x) = ‖x‖
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Parser.builder_nameDefault : Lean.ParserDescr
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.Const.isHashSelf_alterₘ : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] [inst_2 : Hashable α] [LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β),
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ (a : α) (f : Option β → Option β),
      Std.DHashMap.Internal.IsHashSelf (↑(Std.DHashMap.Internal.Raw₀.Const.alterₘ m a f)).buckets
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get_filter : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] {f : α → Bool} {k : α} {h' : k ∈ Std.HashSet.Raw.filter f m} (h : m.WF),
  (Std.HashSet.Raw.filter f m).get k h' = m.get k ⋯
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.ExactPairing.tensor_coevaluation : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X₁ X₂ Y₁ Y₂ : C} [inst_2 : CategoryTheory.ExactPairing X₁ Y₁] [inst_3 : CategoryTheory.ExactPairing X₂ Y₂],
  η_ (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂) (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₂ Y₁) =
    CategoryTheory.monoidalComp (η_ X₁ Y₁)
      (CategoryTheory.monoidalComp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁ (η_ X₂ Y₂)) Y₁)
        (CategoryTheory.CategoryStruct.id
          (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂)
            (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₂ Y₁))))
-- Mathlib.Analysis.Calculus.FDeriv.Add
hasFDerivAt_comp_add_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {x : E} (a : E), HasFDerivAt (fun x => f (a + x)) f' x ↔ HasFDerivAt f f' (a + x)
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron'.triangleMorphism₂_hom₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  (comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃) {v₁₂ : Z₁₂ ⟶ X₁}
  {w₁₂ : X₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₂}
  (h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  {v₂₃ : Z₂₃ ⟶ X₂} {w₂₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₂₃}
  (h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  {v₁₃ : Z₁₃ ⟶ X₁} {w₁₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₃}
  (h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  (h : CategoryTheory.Triangulated.Octahedron' comm h₁₂ h₂₃ h₁₃),
  (CategoryTheory.Triangulated.Octahedron'.triangleMorphism₂ comm h₁₂ h₂₃ h₁₃ h).hom₁ = h.m₃
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey_modify_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] [Inhabited α] {k : α} {f : β k → β k} {hc : k ∈ t.modify k f},
  (t.modify k f).getKey k hc = k
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- The sum of a monotone function and a strictly monotone function is
strictly monotone.  -/
MonotoneOn.add_strictMono : ∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] {s : Set β}
  [AddLeftStrictMono α] [AddRightMono α] {f g : β → α},
  MonotoneOn f s → StrictMonoOn g s → StrictMonoOn (fun x => f x + g x) s
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
/-- The constructed pointwise right Kan extension
when `HasPointwiseRightKanExtension L F` holds.  -/
CategoryTheory.Functor.pointwiseRightKanExtension : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} H] →
            (L : CategoryTheory.Functor C D) →
              (F : CategoryTheory.Functor C H) → [L.HasPointwiseRightKanExtension F] → CategoryTheory.Functor D H
-- Mathlib.Probability.Martingale.BorelCantelli
/-- This lemma is superseded by `Submartingale.bddAbove_iff_exists_tendsto`.  -/
MeasureTheory.Submartingale.exists_tendsto_of_abs_bddAbove_aux : ∀ {Ω : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0}
  {f : ℕ → Ω → ℝ} {R : NNReal} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.Submartingale f ℱ μ →
    f 0 = 0 →
      (∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R) →
        ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) → ∃ c, Filter.Tendsto (fun n => f n ω) Filter.atTop (nhds c)
-- Mathlib.Analysis.Normed.Lp.LpEquiv
/-- The canonical `LinearIsometryEquiv` between `lp E p` and `PiLp p E` when `E : α → Type u`
with `[Fintype α]` and `[Fact (1 ≤ p)]`.  -/
lpPiLpₗᵢ : {α : Type u_1} →
  (E : α → Type u_2) →
    [inst : (i : α) → NormedAddCommGroup (E i)] →
      {p : ENNReal} →
        [inst_1 : Fintype α] →
          (𝕜 : Type u_3) →
            [inst_2 : NontriviallyNormedField 𝕜] →
              [inst_3 : (i : α) → NormedSpace 𝕜 (E i)] → [inst_4 : Fact (1 ≤ p)] → ↥(lp E p) ≃ₗᵢ[𝕜] PiLp p E
-- Init.Data.Fin.Lemmas
/-- Proves a statement by induction on the underlying `Nat` value in a `Fin (n + 1)`.

For the induction:
 * `zero` is the base case, demonstrating `motive 0`.
 * `succ` is the inductive step, assuming the motive for `i : Fin n` (lifted to `Fin (n + 1)` with
   `Fin.castSucc`) and demonstrating it for `i.succ`.

`Fin.induction` is a version of this induction principle that takes the `Fin` as its last
parameter.
 -/
Fin.inductionOn : {n : ℕ} →
  (i : Fin (n + 1)) →
    {motive : Fin (n + 1) → Sort u_1} → motive 0 → ((i : Fin n) → motive i.castSucc → motive i.succ) → motive i