mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey?_modify_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k : α} {f : β k → β k}, m.WF → (m.modify k f).getKey? k = if k ∈ m then some k else none
-- Mathlib.Algebra.Module.Submodule.Bilinear
Submodule.map₂_le_map₂_right : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] {f : M →ₗ[R] N →ₗ[R] P} {p : Submodule R M} {q₁ q₂ : Submodule R N},
  q₁ ≤ q₂ → Submodule.map₂ f p q₁ ≤ Submodule.map₂ f p q₂
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.cocycles₂_map_one_snd : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u_1, u, u} k G} (f : ↥(groupCohomology.cocycles₂ A))
  (g : G), f (g, 1) = (A.ρ g) (f (1, 1))
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.findSomeRevM?.find.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (r : Option β) → ((val : β) → motive (some val)) → (Unit → motive none) → motive r
-- Mathlib.MeasureTheory.Measure.Haar.DistribChar
MeasureTheory.addHaarScalarFactor_smul_eq_distribHaarChar : ∀ {G : Type u_1} {A : Type u_2} [inst : Group G] [inst_1 : AddCommGroup A] [inst_2 : DistribMulAction G A]
  [inst_3 : TopologicalSpace A] [inst_4 : IsTopologicalAddGroup A] [inst_5 : LocallyCompactSpace A]
  [inst_6 : ContinuousConstSMul G A] [inst_7 : MeasurableSpace A] [inst_8 : BorelSpace A] (μ : MeasureTheory.Measure A)
  [inst_9 : μ.IsAddHaarMeasure] (g : G),
  (DomMulAct.mk g • μ).addHaarScalarFactor μ = (MeasureTheory.distribHaarChar A) g
-- Mathlib.Algebra.Homology.ShortComplex.Exact
/-- The obvious splitting of the short complex `X₁ ⟶ X₁ ⊞ X₂ ⟶ X₂`.  -/
CategoryTheory.ShortComplex.Splitting.ofHasBinaryBiproduct : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (X₁ X₂ : C) →
        [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X₁ X₂] →
          { X₁ := X₁, X₂ := X₁ ⊞ X₂, X₃ := X₂, f := CategoryTheory.Limits.biprod.inl,
              g := CategoryTheory.Limits.biprod.snd, zero := ⋯ }.Splitting
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
/-- This is the internal hom `A ⟶[C] -`.
 -/
CategoryTheory.ihom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → (A : C) → [CategoryTheory.Closed A] → CategoryTheory.Functor C C
-- Mathlib.Analysis.Complex.Order
Complex.not_le_zero_iff : ∀ {z : ℂ}, ¬z ≤ 0 ↔ 0 < z.re ∨ z.im ≠ 0
-- Mathlib.Algebra.Symmetrized
SymAlg.sym_unsym : ∀ {α : Type u_1} (a : α), SymAlg.sym (SymAlg.unsym a) = a
-- Lean.Meta.Tactic.Grind.Types
/-- Number of elements in the equivalence class, this field is meaningless if node is not the root.  -/
Lean.Meta.Grind.ENode.size : Lean.Meta.Grind.ENode → ℕ
-- Mathlib.Probability.Process.LocalProperty
ProbabilityTheory.Locally.isLocalizingSequence_localSeq : ∀ {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω}
  [inst : LinearOrder ι] {𝓕 : MeasureTheory.Filtration ι mΩ} {X : ι → Ω → E} {p : (ι → Ω → E) → Prop}
  [inst_1 : OrderBot ι] [inst_2 : TopologicalSpace ι] [inst_3 : OrderTopology ι] [inst_4 : Zero E]
  (hX : ProbabilityTheory.Locally p 𝓕 X P), ProbabilityTheory.IsLocalizingSequence 𝓕 hX.localSeq P
-- Lean.Meta.Tactic.Grind.Arith.FieldNormNum
_private.Lean.Meta.Tactic.Grind.Arith.FieldNormNum.0.Lean.Meta.Grind.Arith.FieldNormNum.Context : Type
-- Mathlib.Dynamics.Ergodic.Ergodic
/-- See also `Ergodic.ae_empty_or_univ_of_preimage_ae_le`.  -/
Ergodic.ae_empty_or_univ_of_preimage_ae_le' : ∀ {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {f : α → α} {μ : MeasureTheory.Measure α},
  Ergodic f μ → MeasureTheory.NullMeasurableSet s μ → f ⁻¹' s ≤ᵐ[μ] s → μ s ≠ ⊤ → s =ᵐ[μ] ∅ ∨ s =ᵐ[μ] Set.univ
-- Mathlib.Analysis.Normed.Group.Real
Real.nnnorm_of_nonneg : ∀ {r : ℝ} (hr : 0 ≤ r), ‖r‖₊ = NNReal.mk r hr
-- Mathlib.Analysis.SpecialFunctions.Log.Deriv
DifferentiableOn.log : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {s : Set E},
  DifferentiableOn ℝ f s → (∀ x ∈ s, f x ≠ 0) → DifferentiableOn ℝ (fun x => Real.log (f x)) s
-- Mathlib.Algebra.Homology.HomologicalComplex
_private.Mathlib.Algebra.Homology.HomologicalComplex.0.ChainComplex.mkAux.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_pi_div_four : Real.cos (Real.pi / 4) = √2 / 2
-- Mathlib.Order.Filter.Lift
Filter.lift'_lift'_assoc : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Set α → Set β} {h : Set β → Set γ},
  Monotone g → Monotone h → (f.lift' g).lift' h = f.lift' fun s => h (g s)
-- Mathlib.RingTheory.WittVector.Identities
WittVector.iterate_verschiebung_coeff : ∀ {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [inst : CommRing R] (x : WittVector p R) (n k : ℕ),
  ((⇑WittVector.verschiebung)^[n] x).coeff (k + n) = x.coeff k
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- A regular epi category is a category in which every epimorphism is regular.  -/
CategoryTheory.IsRegularEpiCategory : (C : Type u₁) → [CategoryTheory.Category.{v₁, u₁} C] → Prop
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiable.prodMk_space : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {E'' : Type u_8} [inst_8 : NormedAddCommGroup E''] [inst_9 : NormedSpace 𝕜 E'']
  {f : M → E'} {g : M → E''}, MDiff f → MDiff g → MDiff fun x => (f x, g x)
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.tr_copy : ∀ (q : Turing.PartrecToTM2.Λ'),
  Turing.PartrecToTM2.tr q.copy =
    Turing.PartrecToTM2.pop' Turing.PartrecToTM2.K'.rev
      (Turing.TM2.Stmt.branch Option.isSome
        (Turing.PartrecToTM2.push' Turing.PartrecToTM2.K'.main
          (Turing.PartrecToTM2.push' Turing.PartrecToTM2.K'.stack (Turing.TM2.Stmt.goto fun x => q.copy)))
        (Turing.TM2.Stmt.goto fun x => q))
-- Mathlib.Order.Heyting.Basic
HeytingAlgebra.mk : {α : Type u_4} →
  [toGeneralizedHeytingAlgebra : GeneralizedHeytingAlgebra α] →
    [toOrderBot : OrderBot α] → [toCompl : Compl α] → (∀ (a : α), a ⇨ ⊥ = aᶜ) → HeytingAlgebra α
-- Init.Data.Nat.Div.Lemmas
Nat.mod_add_mod_lt : ∀ (a b : ℕ) {c : ℕ}, 0 < c → a % c + b % c < 2 * c - 1
-- Mathlib.Analysis.SpecialFunctions.Exp
Real.continuous_exp : Continuous Real.exp
-- Mathlib.LinearAlgebra.Matrix.Notation
/-- Updating a column then removing it is the same as removing it.  -/
Matrix.submatrix_updateCol_succAbove : ∀ {α : Type u} {n : ℕ} {m' : Type uₘ} {o' : Type uₒ} (A : Matrix m' (Fin n.succ) α) (v : m' → α) (f : o' → m')
  (i : Fin n.succ), (A.updateCol i v).submatrix f i.succAbove = A.submatrix f i.succAbove
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.Coloring.colorClasses.eq_1 : ∀ {V : Type u} {G : SimpleGraph V} {α : Type u_2} (C : G.Coloring α), C.colorClasses = (Setoid.ker ⇑C).classes
-- Mathlib.Topology.SeparatedMap
Function.Injective.IsLocallyInjective : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {f : X → Y}, Function.Injective f → IsLocallyInjective f
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
CategoryTheory.Limits.terminalIsoIsTerminal_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasTerminal C] {P : C}
  (t : CategoryTheory.Limits.IsTerminal P), (CategoryTheory.Limits.terminalIsoIsTerminal t).hom = t.from (⊤_ C)
-- Lean.Meta.Tactic.Simp.Arith.Int.Basic
Lean.Meta.Simp.Arith.Int.leCnstr? : Lean.Expr → Lean.MetaM (Option (Int.Internal.Linear.Expr × Int.Internal.Linear.Expr × Array Lean.Expr))
-- Mathlib.Topology.Algebra.Nonarchimedean.Basic
/-- If a topological group embeds into a nonarchimedean group, then it is nonarchimedean.  -/
NonarchimedeanGroup.nonarchimedean_of_emb : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [NonarchimedeanGroup G] {H : Type u_2}
  [inst_3 : Group H] [inst_4 : TopologicalSpace H] [IsTopologicalGroup H] (f : G →* H),
  Topology.IsOpenEmbedding ⇑f → NonarchimedeanGroup H
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.ExtendScalars.map_tmul : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) {M M' : ModuleCat R} (g : M ⟶ M')
  (s : S) (m : ↑M),
  (CategoryTheory.ConcreteCategory.hom ((ModuleCat.extendScalars f).map g)) (s ⊗ₜ[R] m) =
    s ⊗ₜ[R] (CategoryTheory.ConcreteCategory.hom g) m
-- Mathlib.Algebra.FreeMonoid.Basic
/-- An induction principle on free monoids, with cases for `1`, `FreeMonoid.of` and `*`.  -/
FreeMonoid.inductionOn : ∀ {α : Type u_1} {motive : FreeMonoid α → Prop} (z : FreeMonoid α),
  motive 1 →
    (∀ (x : α), motive (FreeMonoid.of x)) → (∀ (x y : FreeMonoid α), motive x → motive y → motive (x * y)) → motive z
-- Mathlib.Data.Fin.Basic
Fin.intCast_val_sub_eq_sub_add_ite : ∀ {n : ℕ} (a b : Fin n), ↑↑(a - b) = ↑↑a - ↑↑b + ↑(if b ≤ a then 0 else n)
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.coe_injective : ∀ {K : Type u_5} [inst : Field K] {f : Polynomial K}, f.degree ≠ 0 → Function.Injective ⇑(AdjoinRoot.of f)
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
/-- `F : D ⥤ K ⥤ C` preserves all colimits of shape `J` if it does for each `k : K`.  -/
CategoryTheory.Limits.preservesColimitsOfShape_of_evaluation : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K]
  (F : CategoryTheory.Functor D (CategoryTheory.Functor K C)) (J : Type u_1)
  [inst_3 : CategoryTheory.Category.{v_1, u_1} J],
  (∀ (k : K), CategoryTheory.Limits.PreservesColimitsOfShape J (F.comp ((CategoryTheory.evaluation K C).obj k))) →
    CategoryTheory.Limits.PreservesColimitsOfShape J F
-- Mathlib.Data.Set.Constructions
FiniteInter.finiteInterClosure.basic : ∀ {α : Type u_1} {S : Set (Set α)} {s : Set α}, s ∈ S → FiniteInter.finiteInterClosure S s
-- Std.Data.DTreeMap.Internal.Balanced
/-- Predicate that states that the stored size information in a tree is correct and that it is
balanced.
 -/
Std.DTreeMap.Internal.Impl.Balanced : {α : Type u} → {β : α → Type v} → Std.DTreeMap.Internal.Impl α β → Prop
-- Mathlib.RingTheory.Polynomial.ContentIdeal
Polynomial.contentIdeal_eq_top_of_contentIdeal_mul_eq_top : ∀ {R : Type u_3} [inst : CommSemiring R] {p q : Polynomial R}, (p * q).contentIdeal = ⊤ → p.contentIdeal = ⊤
-- Lean.Elab.BuiltinCommand
Lean.Elab.Command.elabExit : Lean.Elab.Command.CommandElab
-- Mathlib.Analysis.RCLike.Basic
RCLike.inv_def : ∀ {K : Type u_1} [inst : RCLike K] (z : K), z⁻¹ = (starRingEnd K) z * ↑(‖z‖ ^ 2)⁻¹
-- Aesop.Forward.Match.Types
/-- A complete match contains complete matches for each slot cluster. This means
there is one match for each slot cluster and each such match contains a
hypothesis for each of the slots.  -/
Aesop.CompleteMatch : Type
-- Mathlib.Algebra.Lie.Basis.Prod
_private.Mathlib.Algebra.Lie.Basis.Prod.0.LieAlgebra.Basis.prodSymmEquiv_symm_apply : ∀ {ι₁ : Type u_1} {ι₂ : Type u_2} {L₁ : Type u_3} {L₂ : Type u_4} [inst : Finite ι₁] [inst_1 : Finite ι₂] (eι : ι₁ ≃ ι₂)
  [inst_2 : LieRing L₁] [inst_3 : LieRing L₂] {R : Type u_5} [inst_4 : CommRing R] [inst_5 : LieAlgebra R L₁]
  {H₁ : LieSubalgebra R L₁} (b₁ : LieAlgebra.Basis ι₁ H₁) [inst_6 : LieAlgebra R L₂] {H₂ : LieSubalgebra R L₂}
  (b₂ : LieAlgebra.Basis ι₂ H₂) {y : ↥(LieAlgebra.Basis.prod✝ eι b₁ b₂)},
  (LieAlgebra.Basis.prodSymmEquiv✝ eι b₁ b₂).symm y = ⟨((↑y).2, (↑y).1), ⋯⟩
-- Mathlib.LinearAlgebra.FreeProduct.Basic
/-- The free tensor algebra and its representation as an infinite direct sum
of tensor powers are (noncomputably) equivalent as `R`-algebras.  -/
LinearAlgebra.FreeProduct.powerAlgebraEquivFreeTensorAlgebra : {I : Type u} →
  (R : Type v) →
    [inst : CommSemiring R] →
      (A : I → Type w) →
        [inst_1 : (i : I) → Semiring (A i)] →
          [inst_2 : (i : I) → Algebra R (A i)] →
            LinearAlgebra.FreeProduct.PowerAlgebra R A ≃ₐ[R] LinearAlgebra.FreeProduct.FreeTensorAlgebra R A
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getD_toList_rcc_eq_fallback : ∀ {m n i fallback : ℕ}, n + 1 ≤ i + m → (m...=n).toList.getD i fallback = fallback
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_eq_default_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {a : α}, t.contains a = false → t.getKey! a = default
-- Std.Http.Protocol.H1.Reader
/-- The input byte array.
 -/
Std.Http.Protocol.H1.Reader.input : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Reader dir → ByteArray.Iterator
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
/-- Given homology map data for morphisms `φ` and `φ'`, this is the induced homology
map data for `φ + φ'`.  -/
CategoryTheory.ShortComplex.HomologyMapData.add : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        {φ φ' : S₁ ⟶ S₂} →
          {h₁ : S₁.HomologyData} →
            {h₂ : S₂.HomologyData} →
              CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂ →
                CategoryTheory.ShortComplex.HomologyMapData φ' h₁ h₂ →
                  CategoryTheory.ShortComplex.HomologyMapData (φ + φ') h₁ h₂
-- Mathlib.Probability.BrownianMotion.Basic
/-- A modification of a pre-Brownian process is pre-Brownian.  -/
ProbabilityTheory.IsPreBrownianReal.congr : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {B : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω} {C : NNReal → Ω → ℝ},
  ProbabilityTheory.IsPreBrownianReal B P → (∀ (t : NNReal), B t =ᵐ[P] C t) → ProbabilityTheory.IsPreBrownianReal C P
-- Mathlib.CategoryTheory.ShrinkYoneda
/-- The Yoneda embedding `C ⥤ Cᵒᵖ ⥤ Type w` for a locally `w`-small category `C`.  -/
CategoryTheory.shrinkYoneda : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.LocallySmall.{w, v, u} C] → CategoryTheory.Functor C (CategoryTheory.Functor Cᵒᵖ (Type w))
-- Mathlib.Data.List.Lookmap
List.lookmap_none : ∀ {α : Type u_1} (l : List α), List.lookmap (fun x => none) l = l
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.floor_lt_ceil_of_lt_of_pos : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] [IsStrictOrderedRing R]
  {a b : R}, a < b → 0 < b → ⌊a⌋₊ < ⌈b⌉₊
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapLeftComp.eq_1 : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T)
  {L₁ L₂ L₃ : CategoryTheory.Functor A T} (l : L₁ ⟶ L₂) (l' : L₂ ⟶ L₃),
  CategoryTheory.Comma.mapLeftComp R l l' =
    CategoryTheory.NatIso.ofComponents
      (fun X =>
        CategoryTheory.Comma.isoMk
          (CategoryTheory.Iso.refl
            ((CategoryTheory.Comma.mapLeft R (CategoryTheory.CategoryStruct.comp l l')).obj X).left)
          (CategoryTheory.Iso.refl
            ((CategoryTheory.Comma.mapLeft R (CategoryTheory.CategoryStruct.comp l l')).obj X).right)
          ⋯)
      ⋯
-- Batteries.Data.BinomialHeap.Basic
_private.Batteries.Data.BinomialHeap.Basic.0.Batteries.BinomialHeap.Imp.Heap.merge.match_3.splitter : {α : Type u_1} →
  (motive : Batteries.BinomialHeap.Imp.Heap α → Batteries.BinomialHeap.Imp.Heap α → Sort u_2) →
    (x x_1 : Batteries.BinomialHeap.Imp.Heap α) →
      ((h : Batteries.BinomialHeap.Imp.Heap α) → motive Batteries.BinomialHeap.Imp.Heap.nil h) →
        ((h : Batteries.BinomialHeap.Imp.Heap α) →
            (h = Batteries.BinomialHeap.Imp.Heap.nil → False) → motive h Batteries.BinomialHeap.Imp.Heap.nil) →
          ((r₁ : ℕ) →
              (a₁ : α) →
                (n₁ : Batteries.BinomialHeap.Imp.HeapNode α) →
                  (t₁ : Batteries.BinomialHeap.Imp.Heap α) →
                    (r₂ : ℕ) →
                      (a₂ : α) →
                        (n₂ : Batteries.BinomialHeap.Imp.HeapNode α) →
                          (t₂ : Batteries.BinomialHeap.Imp.Heap α) →
                            motive (Batteries.BinomialHeap.Imp.Heap.cons r₁ a₁ n₁ t₁)
                              (Batteries.BinomialHeap.Imp.Heap.cons r₂ a₂ n₂ t₂)) →
            motive x x_1
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.CategoryWithWeakEquivalences.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.MorphismProperty C → HomotopicalAlgebra.CategoryWithWeakEquivalences C
-- Mathlib.Order.Interval.Set.Image
Set.image_subtype_val_Iic_Iic : ∀ {α : Type u_1} [inst : Preorder α] {a : α} (b : ↑(Set.Iic a)), Subtype.val '' Set.Iic b = Set.Iic ↑b
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided
CategoryTheory.MonoidalCategory.DayConvolution.braiding_naturality_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.BraidedCategory C]
  [inst_4 : CategoryTheory.MonoidalCategory V] [inst_5 : CategoryTheory.BraidedCategory V]
  {F G : CategoryTheory.Functor C V} (η : F ⟶ G) (H : CategoryTheory.Functor C V)
  [inst_6 : CategoryTheory.MonoidalCategory.DayConvolution F H]
  [inst_7 : CategoryTheory.MonoidalCategory.DayConvolution H F]
  [inst_8 : CategoryTheory.MonoidalCategory.DayConvolution G H]
  [inst_9 : CategoryTheory.MonoidalCategory.DayConvolution H G],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.DayConvolution.map η (CategoryTheory.CategoryStruct.id H))
      (CategoryTheory.MonoidalCategory.DayConvolution.braiding G H).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.braiding F H).hom
      (CategoryTheory.MonoidalCategory.DayConvolution.map (CategoryTheory.CategoryStruct.id H) η)
-- Mathlib.Topology.Category.Locale
/-- The category of locales.  -/
Locale : Type (u_1 + 1)
-- Mathlib.Topology.ContinuousOn
continuousWithinAt_const : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {b : β} {s : Set α} {x : α},
  ContinuousWithinAt (fun x => b) s x
-- Mathlib.LinearAlgebra.BilinearMap
/-- Restricting a bilinear map in the second entry  -/
LinearMap.domRestrict₂ : {R : Type u_1} →
  {R₂ : Type u_2} →
    {S : Type u_3} →
      {S₂ : Type u_4} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            [inst_2 : Semiring S] →
              [inst_3 : Semiring S₂] →
                {M : Type u_5} →
                  {N : Type u_7} →
                    {P : Type u_9} →
                      [inst_4 : AddCommMonoid M] →
                        [inst_5 : AddCommMonoid N] →
                          [inst_6 : AddCommMonoid P] →
                            [inst_7 : Module R M] →
                              [inst_8 : Module S N] →
                                [inst_9 : Module R₂ P] →
                                  [inst_10 : Module S₂ P] →
                                    [inst_11 : SMulCommClass S₂ R₂ P] →
                                      {ρ₁₂ : R →+* R₂} →
                                        {σ₁₂ : S →+* S₂} →
                                          (M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) → (q : Submodule S N) → M →ₛₗ[ρ₁₂] ↥q →ₛₗ[σ₁₂] P
-- Mathlib.CategoryTheory.Limits.Types.Pushouts
CategoryTheory.Limits.Types.Pushout.inl_rel'_inr_iff : ∀ {S X₁ X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) (x₁ : X₁) (x₂ : X₂),
  CategoryTheory.Limits.Types.Pushout.Rel' f g (Sum.inl x₁) (Sum.inr x₂) ↔
    ∃ s, x₁ = (CategoryTheory.ConcreteCategory.hom f) s ∧ x₂ = (CategoryTheory.ConcreteCategory.hom g) s
-- Mathlib.Algebra.Order.BigOperators.Group.Multiset
Multiset.le_sum_of_mem : ∀ {α : Type u_2} [inst : AddCommMonoid α] {m : Multiset α} {a : α},
  a ∈ m → ∀ [inst_1 : Preorder α] [CanonicallyOrderedAdd α], a ≤ m.sum
-- Mathlib.Order.Booleanisation
/-- The inclusion `a ↦ aᶜ` from a generalized Boolean algebra to its generated Boolean algebra.  -/
Booleanisation.comp : {α : Type u_1} → α → Booleanisation α
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than the given key,
returning `fallback` if no such pair exists.
 -/
Std.DTreeMap.Raw.getEntryLTD : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → α → (a : α) × β a → (a : α) × β a
-- Mathlib.Data.Finset.NoncommProd
Finset.noncommSum_empty : ∀ {α : Type u_3} {β : Type u_4} [inst : AddMonoid β] (f : α → β) (h : (↑∅).Pairwise (Function.onFun AddCommute f)),
  ∅.noncommSum f h = 0
-- Init.Data.Vector.Lemmas
Vector.findM?_toList : ∀ {m : Type → Type} {α : Type} {n : ℕ} [inst : Monad m] [LawfulMonad m] {p : α → m Bool} {xs : Vector α n},
  List.findM? p xs.toList = Vector.findM? p xs
-- Std.Http.Protocol.H1.Parser
/-- Parses a backslash-escaped character inside a quoted-string.

`quoted-pair = "\" ( HTAB / SP / VCHAR )` — strict ASCII-only (no obs-text).
 -/
_private.Std.Http.Protocol.H1.Parser.0.Std.Http.Protocol.H1.parseQuotedPair : Std.Internal.Parsec.ByteArray.Parser UInt8
-- Mathlib.Analysis.Convex.Jensen
/-- **Minimum principle** for concave functions. If a function `f` is concave on the convex hull of
`s`, then the eventual minimum of `f` on `convexHull 𝕜 s` lies in `s`.  -/
ConcaveOn.exists_le_of_mem_convexHull : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup β] [inst_5 : LinearOrder β] [IsOrderedAddMonoid β]
  [inst_7 : Module 𝕜 E] [inst_8 : Module 𝕜 β] [IsStrictOrderedModule 𝕜 β] {s : Set E} {f : E → β} {x : E} {t : Set E},
  ConcaveOn 𝕜 s f → t ⊆ s → x ∈ (convexHull 𝕜) t → ∃ y ∈ t, f y ≤ f x
-- Mathlib.Algebra.Lie.SemiDirect
LieAlgebra.SemiDirectSum.prod_iso_invFun_right : ∀ (R : Type u_1) [inst : CommRing R] (K : Type u_2) [inst_1 : LieRing K] [inst_2 : LieAlgebra R K] (L : Type u_3)
  [inst_3 : LieRing L] [inst_4 : LieAlgebra R L] (a : K × L),
  ((LieAlgebra.SemiDirectSum.prod_iso R K L).invFun a).right = a.2
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.lift_comp : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [inst_4 : IsLocalization M S] {g : R →+* P}
  (hg : ∀ (y : ↥M), IsUnit (g ↑y)), (IsLocalization.lift hg).comp (algebraMap R S) = g
-- Mathlib.GroupTheory.Nilpotent
/-- The lower central series commutes with images under a group homomorphism.  -/
Subgroup.map_lowerCentralSeries : ∀ {G : Type u_1} [inst : Group G] (S : Subgroup G) {K : Type u_2} [inst_1 : Group K] (f : G →* K) (n : ℕ),
  Subgroup.map f (S.lowerCentralSeries n) = (Subgroup.map f S).lowerCentralSeries n
-- Mathlib.Topology.Metrizable.Basic
TopologicalSpace.metrizableSpace_pi : ∀ {ι : Type u_1} {A : ι → Type u_4} [Finite ι] [inst : (i : ι) → TopologicalSpace (A i)]
  [∀ (i : ι), TopologicalSpace.MetrizableSpace (A i)], TopologicalSpace.MetrizableSpace ((i : ι) → A i)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- The tangent of an angle in a right-angled triangle multiplied by the adjacent side equals
the opposite side.  -/
Orientation.tan_oangle_add_right_mul_norm_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑(Real.pi / 2) → (o.oangle x (x + y)).tan * ‖x‖ = ‖y‖
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.instMul.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : Mul M],
  MonoidAlgebra.instMul = { mul := MonoidAlgebra.mul' }