mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If twice the oriented angles between two triples of points are equal, one triple is affinely
independent if and only if the other is.  -/
EuclideanGeometry.affineIndependent_iff_of_two_zsmul_oangle_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ p₄ p₅ p₆ : P},
  2 • EuclideanGeometry.oangle p₁ p₂ p₃ = 2 • EuclideanGeometry.oangle p₄ p₅ p₆ →
    (AffineIndependent ℝ ![p₁, p₂, p₃] ↔ AffineIndependent ℝ ![p₄, p₅, p₆])
-- Mathlib.GroupTheory.Coset.Card
AddSubgroup.card_add_eq_card_addSubgroup_add_card_quotient : ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) (t : Set α),
  Nat.card ↑(t + ↑s) = Nat.card ↥s * Nat.card ↑(QuotientAddGroup.mk '' t)
-- Init.Data.ByteArray.Bootstrap
List.toByteArray_append' : ∀ {l l' : List UInt8}, (l ++ l').toByteArray = l.toByteArray.append l'.toByteArray
-- Mathlib.Data.TypeVec
TypeVec.lastFun_subtypeVal : ∀ {n : ℕ} {α : TypeVec.{u_1} (n + 1)} (p : α.Arrow (TypeVec.repeat (n + 1) Prop)),
  TypeVec.lastFun (TypeVec.subtypeVal p) = Subtype.val
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
/-- Mapping from `Expr` to a variable representing it.  -/
Lean.Meta.Grind.Arith.Cutsat.State.varMap : Lean.Meta.Grind.Arith.Cutsat.State → Lean.PHashMap Lean.Meta.Sym.ExprPtr Int.Internal.Linear.Var
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get_insertMany_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {l : List (α × β)} {k k' : α},
      cmp k k' = Ordering.eq →
        ∀ {v : β},
          List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
            (k, v) ∈ l →
              ∀ {h' : k' ∈ Std.DTreeMap.Raw.Const.insertMany t l},
                Std.DTreeMap.Raw.Const.get (Std.DTreeMap.Raw.Const.insertMany t l) k' h' = v
-- Mathlib.Algebra.Order.Module.Defs
PosSMulReflectLE_iff_posSMulReflectLT : ∀ {α : Type u_1} {β : Type u_2} [inst : Semiring α] [inst_1 : AddCommGroup β] [inst_2 : Module α β] [IsDomain α]
  [Module.IsTorsionFree α β] [inst_5 : PartialOrder α] [inst_6 : PartialOrder β],
  PosSMulReflectLE α β ↔ PosSMulReflectLT α β
-- Mathlib.Algebra.Group.Subgroup.Order
/-- A subgroup of an ordered group is an ordered group.  -/
Subgroup.toIsOrderedMonoid : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : Preorder G] [IsOrderedMonoid G] (H : Subgroup G), IsOrderedMonoid ↥H
-- Mathlib.Topology.Algebra.InfiniteSum.Group
multipliable_iff_of_multipliable_div : ∀ {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [inst : CommGroup α] [inst_1 : TopologicalSpace α]
  [IsTopologicalGroup α] {f g : β → α}, Multipliable (fun b => f b / g b) L → (Multipliable f L ↔ Multipliable g L)
-- Init.Data.SInt.Bitwise
Int64.not_and_self : ∀ {a : Int64}, ~~~a &&& a = 0
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.gcd_dvd_right : ∀ {R : Type u} [inst : EuclideanDomain R] [inst_1 : DecidableEq R] (a b : R), EuclideanDomain.gcd a b ∣ b
-- Init.Data.SInt.Lemmas
Int8.toInt64_ofBitVec : ∀ (b : BitVec 8), (Int8.ofBitVec b).toInt64 = Int64.ofBitVec (BitVec.signExtend 64 b)
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupNorm.instMax.eq_1 : ∀ {E : Type u_3} [inst : Group E],
  GroupNorm.instMax =
    {
      max := fun p q =>
        let __src := p.toGroupSeminorm ⊔ q.toGroupSeminorm;
        { toGroupSeminorm := __src, eq_one_of_map_eq_zero' := ⋯ } }
-- Mathlib.NumberTheory.SmoothNumbers
/-- Membership in `Nat.smoothNumbers n` is decidable.  -/
Nat.instDecidablePredMemSetSmoothNumbers : (n : ℕ) → DecidablePred fun x => x ∈ n.smoothNumbers
-- Init.Notation
Lean.instCoeSyntaxTSyntaxConsSyntaxNodeKindMkStr1Nil : Coe Lean.Syntax (Lean.TSyntax `rawStx)
-- Mathlib.CategoryTheory.Monoidal.Category
/-- Tensoring on the right with a fixed object, as a functor.  -/
CategoryTheory.MonoidalCategory.tensorRight : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.MonoidalCategory C] → C → CategoryTheory.Functor C C
-- Mathlib.Topology.Separation.Basic
isClosed_setOfPred_inseparable : ∀ {X : Type u_1} [inst : TopologicalSpace X] [R1Space X], IsClosed {p | Inseparable p.1 p.2}
-- Mathlib.Order.Filter.Bases.Basic
/-- The set of filter basis sets is directed downwards.  -/
FilterBasis.inter_sets : ∀ {α : Type u_6} (self : FilterBasis α) {x y : Set α}, x ∈ self.sets → y ∈ self.sets → ∃ z ∈ self.sets, z ⊆ x ∩ y
-- ProofWidgets.Cancellable
ProofWidgets.CancellableTask.mk.injEq : ∀ (task : Task (Except Lean.Server.RequestError (ProofWidgets.LazyEncodable Lean.Json))) (cancel : IO Unit)
  (task_1 : Task (Except Lean.Server.RequestError (ProofWidgets.LazyEncodable Lean.Json))) (cancel_1 : IO Unit),
  ({ task := task, cancel := cancel } = { task := task_1, cancel := cancel_1 }) = (task = task_1 ∧ cancel = cancel_1)
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.aeval_comp_toMvPolynomial : ∀ {R : Type u_1} {S : Type u_2} {σ : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  (f : σ → S) (i : σ), (MvPolynomial.aeval f).comp (Polynomial.toMvPolynomial i) = Polynomial.aeval (f i)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.cyclesMap'_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData),
  CategoryTheory.ShortComplex.cyclesMap' 0 h₁ h₂ = 0
-- Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
/-- Characterize the forward direction of the isomorphism
`PreservesColimit₂.isoColimitUncurryWhiskeringLeft₂` w.r.t. the canonical maps to the colimit.  -/
CategoryTheory.Limits.PreservesColimit₂.map_ι_comp_isoColimitUncurryWhiskeringLeft₂_inv : ∀ {J₁ : Type u_1} {J₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} J₂] {C₁ : Type u_3} {C₂ : Type u_4} {C : Type u_5}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₁] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₂]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C] (K₁ : CategoryTheory.Functor J₁ C₁)
  (K₂ : CategoryTheory.Functor J₂ C₂) (G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C))
  [inst_5 : CategoryTheory.Limits.PreservesColimit₂ K₁ K₂ G] [inst_6 : CategoryTheory.Limits.HasColimit K₁]
  [inst_7 : CategoryTheory.Limits.HasColimit K₂] (j : J₁ × J₂),
  CategoryTheory.CategoryStruct.comp ((G.map (CategoryTheory.Limits.colimit.ι K₁ j.1)).app (K₂.obj j.2))
      (CategoryTheory.CategoryStruct.comp
        ((G.obj (CategoryTheory.Limits.colimit K₁)).map (CategoryTheory.Limits.colimit.ι K₂ j.2))
        (CategoryTheory.Limits.PreservesColimit₂.isoColimitUncurryWhiskeringLeft₂ K₁ K₂ G).inv) =
    CategoryTheory.Limits.colimit.ι
      (CategoryTheory.Functor.uncurry.obj ((((CategoryTheory.Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G)) j
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.dblX_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} [inst_1 : DecidableEq F] {P Q : Fin 3 → F},
  W.Equation P →
    W.Equation Q →
      P 2 ≠ 0 →
        Q 2 ≠ 0 →
          P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2 →
            P 1 * Q 2 ^ 3 ≠ W.negY Q * P 2 ^ 3 →
              W.dblX P / W.dblZ P ^ 2 =
                W.toAffine.addX (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2)
                  (W.toAffine.slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3))
-- Mathlib.Algebra.Group.Submonoid.Finite
Submonoid.pi_mem_of_mulSingle_mem_aux : ∀ {η : Type u_1} {f : η → Type u_2} [inst : (i : η) → MulOneClass (f i)] {S : Type u_3}
  [inst_1 : SetLike S ((i : η) → f i)] [SubmonoidClass S ((i : η) → f i)] [inst_3 : DecidableEq η] (I : Finset η)
  {H : S} (x : (i : η) → f i), (∀ i ∉ I, x i = 1) → (∀ i ∈ I, Pi.mulSingle i (x i) ∈ H) → x ∈ H
-- Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
AlgebraicTopology.AlternatingFaceMapComplex.ε_app_f_succ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (X : CategoryTheory.SimplicialObject.Augmented C) (n : ℕ),
  (AlgebraicTopology.AlternatingFaceMapComplex.ε.app X).f (n + 1) = 0
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryLE?_eq_map : ∀ {α : Type u} {β : Type v} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α fun x => β} {k : α},
  Std.DTreeMap.Internal.Impl.Const.getEntryLE? k t =
    Option.map (fun x => (x.fst, x.snd)) (Std.DTreeMap.Internal.Impl.getEntryLE? k t)
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.typein_surjOn : ∀ {α : Type u} (r : α → α → Prop) [inst : IsWellOrder α r],
  Set.SurjOn (⇑(Ordinal.typein r).toRelEmbedding) Set.univ (Set.Iio (Ordinal.type r))
-- Mathlib.RingTheory.Localization.Basic
IsLocalization.algEquivOfAlgEquiv.congr_simp : ∀ {A : Type u_4} [inst : CommSemiring A] {R : Type u_5} [inst_1 : CommSemiring R] [inst_2 : Algebra A R]
  {M M_1 : Submonoid R} (e_M : M = M_1) (S : Type u_6) [inst_3 : CommSemiring S] [inst_4 : Algebra A S]
  [inst_5 : Algebra R S] [inst_6 : IsScalarTower A R S] [inst_7 : IsLocalization M S] {P : Type u_7}
  [inst_8 : CommSemiring P] [inst_9 : Algebra A P] {T T_1 : Submonoid P} (e_T : T = T_1) (Q : Type u_8)
  [inst_10 : CommSemiring Q] [inst_11 : Algebra A Q] [inst_12 : Algebra P Q] [inst_13 : IsScalarTower A P Q]
  [inst_14 : IsLocalization T Q] (h h_1 : R ≃ₐ[A] P) (e_h : h = h_1) (H : Submonoid.map h M = T),
  IsLocalization.algEquivOfAlgEquiv S Q h H = IsLocalization.algEquivOfAlgEquiv S Q h_1 ⋯
-- Mathlib.Topology.MetricSpace.Bounded
/-- If a family of complete sets with diameter tending to `0` is such that each finite intersection
is nonempty, then the total intersection is also nonempty.  -/
IsComplete.nonempty_iInter_of_nonempty_biInter : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : ℕ → Set α},
  IsComplete (s 0) →
    (∀ (n : ℕ), IsClosed (s n)) →
      (∀ (n : ℕ), Bornology.IsBounded (s n)) →
        (∀ (N : ℕ), (⋂ n, ⋂ (_ : n ≤ N), s n).Nonempty) →
          Filter.Tendsto (fun n => Metric.diam (s n)) Filter.atTop (nhds 0) → (⋂ n, s n).Nonempty
-- Mathlib.Algebra.Lie.Nilpotent
LieModule.iterate_toEnd_mem_lowerCentralSeries₂ : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M] (x y : L)
  (m : M) (k : ℕ),
  (⇑((LieModule.toEnd R L M) x ∘ₗ (LieModule.toEnd R L M) y))^[k] m ∈ LieModule.lowerCentralSeries R L M (2 * k)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.mem_of_mem_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k a : α} {v : β},
  a ∈ t.insert k v → cmp k a ≠ Ordering.eq → a ∈ t
-- Mathlib.FieldTheory.Relrank
IntermediateField.relrank_self : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (A : IntermediateField F E),
  A.relrank A = 1
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.instAddCancelCommMonoidLocalization : {M : Type u_3} → [inst : AddCancelCommMonoid M] → (S : AddSubmonoid M) → AddCancelCommMonoid (AddLocalization S)
-- Init.Data.List.Zip
List.getElem?_zipWith_eq_some : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {l₁ : List α} {l₂ : List β} {z : γ} {i : ℕ},
  (List.zipWith f l₁ l₂)[i]? = some z ↔ ∃ x y, l₁[i]? = some x ∧ l₂[i]? = some y ∧ f x y = z
-- Mathlib.Topology.Compactness.Compact
/-- A filter `l` is disjoint with the neighborhood filter of a compact set if and only if it is
disjoint with the neighborhood filter of each point of this set.  -/
IsCompact.disjoint_nhdsSet_right : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {l : Filter X},
  IsCompact s → (Disjoint l (nhdsSet s) ↔ ∀ x ∈ s, Disjoint l (nhds x))
-- Mathlib.Data.Multiset.Powerset
Multiset.nodup_powerset : ∀ {α : Type u_1} {s : Multiset α}, s.powerset.Nodup ↔ s.Nodup
-- Lean.Util.PPExt
Lean.ppLevel : Lean.PPContext → Lean.Level → BaseIO Std.Format
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for `shiftLeftZeroExtend` on `BitVec`s.  -/
BitVec.reduceShiftLeftZeroExtend : Lean.Meta.Simp.DSimproc
-- Batteries.Data.String.Legacy
/-- Returns the first character in `s`. If `s = ""`, returns `(default : Char)`.

This is an old implementation, preserved here for users of the lemmas in
`Batteries.Data.String.Lemmas`. Its runtime behavior is equivalent to that of `String.front`.

Examples:
* `"abc".front = 'a'`
* `"".front = (default : Char)`
 -/
String.Legacy.front : String → Char
-- Mathlib.CategoryTheory.Bicategory.Opposites
Bicategory.Opposite.op2_id : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} {f : a ⟶ b},
  Bicategory.Opposite.op2 (CategoryTheory.CategoryStruct.id f) = CategoryTheory.CategoryStruct.id f.op
-- Mathlib.Data.Fintype.Defs
Ordering.fintype : Fintype Ordering
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.rightOp : C ⥤ Dᵒᵖ` reflects limits, then `F : Cᵒᵖ ⥤ D` reflects colimits.  -/
CategoryTheory.Limits.reflectsColimits_of_rightOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.ReflectsLimits F.rightOp],
  CategoryTheory.Limits.ReflectsColimits F
-- Mathlib.Algebra.Homology.SpectralObject.Homology
CategoryTheory.Abelian.SpectralObject.map_fourδ₁Toδ₀_EMap_fourδ₄Toδ₃_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {i₁ i₂ i₃ i₄ i₅ i₆ : ι} (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₆ : i₅ ⟶ i₆) (f₂₃ : i₁ ⟶ i₃)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (f₅₆ : i₄ ⟶ i₆)
  (h₅₆ : CategoryTheory.CategoryStruct.comp f₅ f₆ = f₅₆) (n₁ n₂ n₃ : ℤ)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.map_fourδ₁Toδ₀_EMap_fourδ₄Toδ₃._auto_1)
  (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.map_fourδ₁Toδ₀_EMap_fourδ₄Toδ₃._auto_3) {Z : C}
  (h : X.E f₃ f₄ f₅₆ n₁ n₂ n₃ ⋯ ⋯ ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (CategoryTheory.ComposableArrows.fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ ⋯) n₁ n₂ n₃ ⋯ ⋯)
      (CategoryTheory.CategoryStruct.comp
        (X.map f₃ f₄ f₅ f₃ f₄ f₅₆ (CategoryTheory.ComposableArrows.fourδ₄Toδ₃ f₃ f₄ f₅ f₆ f₅₆ ⋯) n₁ n₂ n₃ ⋯ ⋯) h) =
    CategoryTheory.CategoryStruct.comp
      (X.map f₂₃ f₄ f₅ f₂₃ f₄ f₅₆ (CategoryTheory.ComposableArrows.fourδ₄Toδ₃ f₂₃ f₄ f₅ f₆ f₅₆ ⋯) n₁ n₂ n₃ ⋯ ⋯)
      (CategoryTheory.CategoryStruct.comp
        (X.map f₂₃ f₄ f₅₆ f₃ f₄ f₅₆ (CategoryTheory.ComposableArrows.fourδ₁Toδ₀ f₂ f₃ f₄ f₅₆ f₂₃ ⋯) n₁ n₂ n₃ ⋯ ⋯) h)
-- Init.Data.BitVec.Lemmas
BitVec.zero_smod : ∀ {w : ℕ} {x : BitVec w}, (0#w).smod x = 0#w
-- Lean.Server.Rpc.Basic
Lean.Lsp.instToJsonRpcWireFormat.toJson : Lean.Lsp.RpcWireFormat → Lean.Json
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cochain.fromSingleMk_sub : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f g : X ⟶ K.X q) {n : ℤ}
  (h : p + n = q),
  CochainComplex.HomComplex.Cochain.fromSingleMk (f - g) h =
    CochainComplex.HomComplex.Cochain.fromSingleMk f h - CochainComplex.HomComplex.Cochain.fromSingleMk g h
-- Mathlib.Tactic.NormNum.DivMod
/-- The `norm_num` extension which identifies expressions of the form `Int.emod a b`,
such that `norm_num` successfully recognises both `a` and `b`.  -/
Mathlib.Meta.NormNum.evalIntMod : Mathlib.Meta.NormNum.NormNumExt
-- Init.Data.SInt.Lemmas
Int64.toISize_ofIntTruncate : ∀ {n : ℤ}, -2 ^ 63 ≤ n → n < 2 ^ 63 → (Int64.ofIntClamp n).toISize = ISize.ofInt n
-- Mathlib.CategoryTheory.Sites.LocalSite
/-- On any locally `w`-small local site, the global sections functor to any category with colimits
and products of size `w` is a left adjoint. A variant of this without the universe parameter `w`
is registered as an instance.  -/
CategoryTheory.GrothendieckTopology.IsLocalSite.Γ_isLeftAdjoint : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [CategoryTheory.LocallySmall.{w, v, u} C] [inst_2 : J.IsLocalSite] (A : Type u')
  [inst_3 : CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A]
  [CategoryTheory.Limits.HasProducts A] [inst_6 : CategoryTheory.HasWeakSheafify J A],
  (CategoryTheory.Sheaf.Γ J A).IsLeftAdjoint
-- Mathlib.GroupTheory.Finiteness
Submonoid.FG.eq_1 : ∀ {M : Type u_1} [inst : Monoid M] (P : Submonoid M), P.FG = ∃ S, Submonoid.closure ↑S = P
-- Mathlib.NumberTheory.GaussSum
mul_gaussSum_inv_eq_gaussSum : ∀ {R : Type u} [inst : Field R] [inst_1 : Fintype R] {R' : Type v} [inst_2 : CommRing R'] (χ : MulChar R R')
  (ψ : AddChar R R'), χ (-1) * gaussSum χ ψ⁻¹ = gaussSum χ ψ
-- Mathlib.Data.Fin.SuccPred
Fin.le_pred_castSucc_iff : ∀ {n : ℕ} {a b : Fin (n + 1)} (ha : a.castSucc ≠ 0), b ≤ a.castSucc.pred ha ↔ b < a
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddMod.Hom.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  {A : C} [inst_4 : CategoryTheory.AddMonObj A] {M N : CategoryTheory.AddMod D A} [inst_5 : SizeOf C]
  [inst_6 : SizeOf D] (hom : M.X ⟶ N.X) [isAddModHom : CategoryTheory.IsAddModHom A hom],
  sizeOf { hom := hom, isAddModHom := isAddModHom } = 1 + sizeOf hom + sizeOf isAddModHom
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.Pi.ι.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {β : Type w} [inst_2 : DecidableEq β] (f : β → C) [inst_3 : CategoryTheory.Limits.HasProduct f] (b : β),
  CategoryTheory.Limits.Pi.ι f b =
    CategoryTheory.Limits.Pi.lift (Function.update (fun x => 0) b (CategoryTheory.CategoryStruct.id (f b)))
-- Lean.Util.Trace
Lean.instInhabitedTraceElem : Inhabited Lean.TraceElem
-- Mathlib.Probability.Process.Stopping
MeasureTheory.measurableSet_preimage_stoppedValue_inter : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Nonempty ι] {u : ι → Ω → β}
  {τ : Ω → WithTop ι} [inst_1 : LinearOrder ι] [inst_2 : MeasurableSpace ι] [inst_3 : TopologicalSpace ι]
  [OrderTopology ι] [SecondCountableTopology ι] [BorelSpace ι] [inst_7 : TopologicalSpace β]
  {f : MeasureTheory.Filtration ι m} [TopologicalSpace.PseudoMetrizableSpace β] [inst_9 : MeasurableSpace β]
  [BorelSpace β],
  MeasureTheory.IsStronglyProgressive f u →
    MeasureTheory.IsStoppingTime f τ →
      ∀ {t : Set β}, MeasurableSet t → ∀ (i : ι), MeasurableSet (MeasureTheory.stoppedValue u τ ⁻¹' t ∩ {ω | τ ω ≤ ↑i})
-- Mathlib.Order.Interval.Set.Basic
Set.Ici_inter_Iio : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ici a ∩ Set.Iio b = Set.Ico a b
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne
/-- Given `i : Fin (n + 2)`, this is the `n`-simplex of `Δ[1]` which corresponds
to the monotone map `Fin (n + 1) → Fin 2` which takes `i` times the value `0`.  -/
SSet.stdSimplex.objMk₁ : {n : ℕ} → Fin (n + 2) → (SSet.stdSimplex.obj { len := 1 }).obj (Opposite.op { len := n })
-- Init.Data.SInt.Lemmas
Int16.toInt_ofInt : ∀ {n : ℤ}, (Int16.ofInt n).toInt = n.bmod Int16.size
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanImportKind.metaKind : Lean.Lsp.LeanImportKind → Lean.Lsp.LeanImportMetaKind
-- Init.Data.Int.DivMod.Lemmas
Int.eq_one_of_mul_eq_one_left : ∀ {a b : ℤ}, 0 ≤ b → a * b = 1 → b = 1
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
/-- If `‖v‖^n * ‖f v‖` is integrable for all `n ≤ N`, then the Fourier transform of `f` is `C^N`.  -/
VectorFourier.contDiff_fourierIntegral : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_2} {W : Type u_3}
  [inst_2 : NormedAddCommGroup V] [inst_3 : NormedSpace ℝ V] [inst_4 : NormedAddCommGroup W] [inst_5 : NormedSpace ℝ W]
  (L : V →L[ℝ] W →L[ℝ] ℝ) {f : V → E} [inst_6 : MeasurableSpace V] [BorelSpace V] {μ : MeasureTheory.Measure V}
  [SecondCountableTopology V] {N : ℕ∞},
  (∀ (n : ℕ), ↑n ≤ N → MeasureTheory.Integrable (fun v => ‖v‖ ^ n * ‖f v‖) μ) →
    ContDiff ℝ (↑N) (VectorFourier.fourierIntegral Real.fourierChar μ (ContinuousLinearMap.toLinearMap₁₂ L) f)
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ Dᵒᵖ` preserves colimits, then `F.leftOp : Cᵒᵖ ⥤ D` preserves limits.  -/
CategoryTheory.Limits.preservesLimitsOfSize_leftOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.leftOp
-- Mathlib.Analysis.Calculus.ContDiff.Deriv
ContDiffAt.derivWithin : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {m n : WithTop ℕ∞} {f : 𝕜 → F} {x : 𝕜},
  ContDiffAt 𝕜 n f x → m + 1 ≤ n → ContDiffAt 𝕜 m (deriv f) x
-- Aesop.RuleSet.Filter
Aesop.RuleSetNameFilter.mk.sizeOf_spec : ∀ (ns : Array Aesop.RuleSetName), sizeOf { ns := ns } = 1 + sizeOf ns
-- Mathlib.Algebra.Category.Semigrp.Basic
Semigrp.ofHom_id : ∀ {X : Type u} [inst : Semigroup X], Semigrp.ofHom (MulHom.id X) = CategoryTheory.CategoryStruct.id (Semigrp.of X)
-- Mathlib.Geometry.Euclidean.Sphere.Basic
/-- Two points are cospherical.  -/
EuclideanGeometry.cospherical_pair : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [NormedSpace ℝ V] [inst_2 : MetricSpace P]
  [NormedAddTorsor V P] (p₁ p₂ : P), EuclideanGeometry.Cospherical {p₁, p₂}
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.hasCoeToOplax : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.Pseudofunctor B C} →
          Coe (F.StrongTrans G) (CategoryTheory.Oplax.StrongTrans F.toOplax G.toOplax)
-- Mathlib.Topology.Order.WithTop
WithTop.continuous_coe : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι],
  Continuous WithTop.some
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rio_eq_toList_rco : ∀ {n : ℕ}, (*...n).toList = (0...n).toList
-- Mathlib.CategoryTheory.Limits.Chosen.End
CategoryTheory.Limits.chosenEnd.map.eq_1 : ∀ {J : Type u_3} {C : Type u_4} [inst : CategoryTheory.Category.{v_3, u_4} C]
  [inst_1 : CategoryTheory.Category.{v_4, u_3} J] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)}
  [inst_2 : CategoryTheory.Limits.ChosenEndsOfShape J C] {G : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)}
  (f : F ⟶ G),
  CategoryTheory.Limits.chosenEnd.map f =
    CategoryTheory.Limits.chosenEnd.lift
      (fun x =>
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.chosenEnd.π F x) ((f.app (Opposite.op x)).app x))
      ⋯
-- Init.Data.String.Lemmas.Order
String.Pos.le_sliceTo_iff : ∀ {s : String} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} {h : q ≤ p₀},
  p ≤ p₀.sliceTo q h ↔ String.Pos.ofSliceTo p ≤ q
-- Init.Classical
Classical.decidableInhabited : (a : Prop) → Inhabited (Decidable a)
-- Aesop.Rule
Aesop.LocalNormSimpRule.mk.inj : ∀ {id : Lean.Name} {simpTheorem : Lean.Term} {id_1 : Lean.Name} {simpTheorem_1 : Lean.Term},
  { id := id, simpTheorem := simpTheorem } = { id := id_1, simpTheorem := simpTheorem_1 } →
    id = id_1 ∧ simpTheorem = simpTheorem_1