mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMonObj.zero_comp_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M N X : C} [inst_2 : CategoryTheory.AddMonObj M] [inst_3 : CategoryTheory.AddMonObj N] (f : M ⟶ N)
  [CategoryTheory.IsAddMonHom f] {Z : C} (h : N ⟶ Z),
  CategoryTheory.CategoryStruct.comp 0 (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp 0 h
-- Aesop.Tree.Data
Aesop.Goal.state : Aesop.Goal → Aesop.GoalState
-- Mathlib.AlgebraicGeometry.PointsPi
AlgebraicGeometry.pointsPi_injective : ∀ {ι : Type u} (R : ι → CommRingCat) (X : AlgebraicGeometry.Scheme) [QuasiSeparatedSpace ↥X],
  Function.Injective (AlgebraicGeometry.pointsPi R X)
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.maxKey.eq_def : ∀ {α : Type u} {β : α → Type v} (x : Std.DTreeMap.Internal.Impl α β) (x_1 : x.isEmpty = false),
  x.maxKey x_1 =
    match x, x_1 with
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x => k
    | Std.DTreeMap.Internal.Impl.inner size k v l l_1@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_2 r), h_1 =>
      l_1.maxKey ⋯
-- Init.Data.String.Lemmas.Basic
String.Slice.sliceFrom_eq_self_iff : ∀ {s : String.Slice} {p : s.Pos}, s.sliceFrom p = s ↔ p = s.startPos
-- Mathlib.Analysis.Calculus.FDeriv.Prod
DifferentiableOn.prodMk : ∀ {𝕜 : 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] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f₁ : E → F} {s : Set E} {f₂ : E → G},
  DifferentiableOn 𝕜 f₁ s → DifferentiableOn 𝕜 f₂ s → DifferentiableOn 𝕜 (fun x => (f₁ x, f₂ x)) s
-- Mathlib.CategoryTheory.Preadditive.LeftExact
/-- A kernel-preserving functor between preadditive categories preserves any pair being a limit.  -/
CategoryTheory.Functor.preservesBinaryProduct_of_preservesKernels : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D)
  [F.PreservesZeroMorphisms]
  [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F] {X Y : C},
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair X Y) F
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateSetTagImp : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.Code pu → Lean.FVarId → ℕ → Lean.Compiler.LCNF.Code pu → Lean.Compiler.LCNF.Code pu
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback.LiftStruct.w_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S}
  {h : CategoryTheory.Limits.ChosenPullback f₁ f₂} {Y : C} {g₁ : Y ⟶ X₁} {g₂ : Y ⟶ X₂} {b : Y ⟶ S}
  (l : h.LiftStruct g₁ g₂ b) {Z : C} (h : S ⟶ Z),
  CategoryTheory.CategoryStruct.comp g₁ (CategoryTheory.CategoryStruct.comp f₁ h) =
    CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.CategoryStruct.comp f₂ h)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Map
MeasureTheory.MeasurePreserving.setLIntegral_comp_preimage_emb : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} {g : α → β},
  MeasureTheory.MeasurePreserving g μ ν →
    MeasurableEmbedding g → ∀ (f : β → ENNReal) (s : Set β), ∫⁻ (a : α) in g ⁻¹' s, f (g a) ∂μ = ∫⁻ (b : β) in s, f b ∂ν
-- Mathlib.Tactic.Sat.FromLRAT
Sat.Literal.pos.injEq : ∀ (a a_1 : ℕ), (Sat.Literal.pos a = Sat.Literal.pos a_1) = (a = a_1)
-- Mathlib.Algebra.Category.MonCat.ForgetCorepresentable
MonCat.forget_isCorepresentable : (CategoryTheory.forget MonCat).IsCorepresentable
-- Mathlib.Algebra.Homology.Monoidal
/-- As a graded object, the single complex `(single C c 0).obj (𝟙_ C)` identifies
to the unit `(GradedObject.single₀ I).obj (𝟙_ C)` of the tensor product of graded objects.  -/
HomologicalComplex.tensorUnitIso : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.Preadditive C] →
        [inst_3 : CategoryTheory.Limits.HasZeroObject C] →
          {I : Type u_2} →
            [inst_4 : AddMonoid I] →
              (c : ComplexShape I) →
                [inst_5 : DecidableEq I] →
                  (CategoryTheory.GradedObject.single₀ I).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅
                    (HomologicalComplex.tensorUnit C c).X
-- Mathlib.CategoryTheory.Sites.Whiskering
CategoryTheory.instFaithfulSheafSheafCompose : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {B : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} B] (J : CategoryTheory.GrothendieckTopology C)
  (F : CategoryTheory.Functor A B) [inst_3 : J.HasSheafCompose F] [F.Faithful],
  (CategoryTheory.sheafCompose J F).Faithful
-- Mathlib.NumberTheory.Modular
/-- Second Fundamental Domain Lemma: if both `z` and `g • z` are in the open domain `𝒟ᵒ`,
where `z : ℍ` and `g : SL(2, ℤ)`, then `g = ±1`.  -/
ModularGroup.eq_one_or_neg_one_of_mem_fdo_mem_fdo : ∀ {g : Matrix.SpecialLinearGroup (Fin 2) ℤ} {z : UpperHalfPlane},
  z ∈ ModularGroup.fdo → g • z ∈ ModularGroup.fdo → g = 1 ∨ g = -1
-- Mathlib.CategoryTheory.Sites.GlobalSections
CategoryTheory.Sheaf.ΓObjEquivSections_naturality_symm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : CategoryTheory.HasWeakSheafify J (Type w)] [inst_2 : CategoryTheory.HasGlobalSectionsFunctor J (Type w)]
  {F G : CategoryTheory.Sheaf J (Type w)} (f : F ⟶ G) (x : ↑F.obj.sections),
  (CategoryTheory.Sheaf.ΓObjEquivSections J G).symm
      ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Functor.sectionsFunctor Cᵒᵖ).map f.hom)) x) =
    (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Sheaf.Γ J (Type w)).map f))
      ((CategoryTheory.Sheaf.ΓObjEquivSections J F).symm x)
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
UniformConvergenceCLM.isUniformEmbedding_postcomp : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3}
  {F : Type u_4} {G : Type u_5} [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : TopologicalSpace E]
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜₂ F] [inst_7 : AddCommGroup G] [inst_8 : UniformSpace G]
  [inst_9 : IsUniformAddGroup G] {𝕜₃ : Type u_6} [inst_10 : NormedField 𝕜₃] [inst_11 : Module 𝕜₃ G] {τ : 𝕜₂ →+* 𝕜₃}
  {ρ : 𝕜₁ →+* 𝕜₃} [inst_12 : RingHomCompTriple σ τ ρ] [inst_13 : UniformSpace F] [inst_14 : IsUniformAddGroup F]
  (g : F →SL[τ] G), IsUniformEmbedding ⇑g → ∀ (𝔖 : Set (Set E)), IsUniformEmbedding g.comp
-- Mathlib.Order.PiLex
Pi.instBoundedOrderLexForallOfWellFoundedLT : {ι : Type u_1} →
  {β : ι → Type u_2} →
    [inst : LinearOrder ι] →
      [WellFoundedLT ι] →
        [inst_2 : (a : ι) → PartialOrder (β a)] → [(a : ι) → BoundedOrder (β a)] → BoundedOrder (Lex ((a : ι) → β a))
-- Init.Data.UInt.Lemmas
UInt16.ofBitVec_neg : ∀ (b : BitVec 16), { toBitVec := -b } = -{ toBitVec := b }
-- Mathlib.RingTheory.HahnSeries.Lex
OrderIso.ofHomInv.congr_simp : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f f_1 : α →o β) (e_f : f = f_1)
  (g g_1 : β →o α) (e_g : g = g_1) (h₁ : f.comp g = OrderHom.id) (h₂ : g.comp f = OrderHom.id),
  OrderIso.ofHomInv f g h₁ h₂ = OrderIso.ofHomInv f_1 g_1 ⋯ ⋯
-- Mathlib.Algebra.Group.Basic
mul_zpow : ∀ {α : Type u_1} [inst : DivisionCommMonoid α] (a b : α) (n : ℤ), (a * b) ^ n = a ^ n * b ^ n
-- Mathlib.Order.Bounds.Image
image2_lowerBounds_lowerBounds_subset_lowerBounds_image2 : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {f : α → β → γ}
  {s : Set α} {t : Set β},
  (∀ (b : β), Antitone (Function.swap f b)) →
    (∀ (a : α), Antitone (f a)) → Set.image2 f (upperBounds s) (upperBounds t) ⊆ lowerBounds (Set.image2 f s t)
-- Mathlib.RingTheory.Valuation.Integers
Valuation.mem_leSubmodule_iff : ∀ {R : Type u} {Γ₀ : Type v} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {v : Valuation R Γ₀} {γ : Γ₀}
  {x : R}, x ∈ v.leSubmodule γ ↔ v x ≤ γ
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem_inter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} {h_mem : k ∈ m₁ ∩ m₂}, (m₁ ∩ m₂)[k] = m₁[k]
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.model_completeTheory : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M], M ⊨ L.completeTheory M
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shift_shiftFunctorCompIsoId_add_neg_cancel_inv_app : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddGroup A]
  [inst_2 : CategoryTheory.HasShift C A] (n : A) (X : C),
  (CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctorCompIsoId C n (-n) ⋯).inv.app X) =
    (CategoryTheory.shiftFunctorCompIsoId C (-n) n ⋯).inv.app ((CategoryTheory.shiftFunctor C n).obj X)
-- Mathlib.Data.List.Basic
/-- Composing a `List.map` with another `List.map` is equal to
a single `List.map` of composed functions.
 -/
List.map_comp_map : ∀ {α : Type u} {β : Type v} {γ : Type w} (g : β → γ) (f : α → β), List.map g ∘ List.map f = List.map (g ∘ f)
-- Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
/-- The class of morphisms `f : X ⟶ Y` between schemes such that
`𝒪_{Y, f x} ⟶ 𝒪_{X, x}` is surjective for all `x : X`.  -/
AlgebraicGeometry.SurjectiveOnStalks : {X Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → Prop
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionAssocIso_hom_naturality_assoc : ∀ {C : Type u_1} {D : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} {inst_2 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] {d₁ d₂ : D} {c₁ c₂ c₃ c₄ : C} (f : d₁ ⟶ d₂)
  (g : c₁ ⟶ c₂) (h : c₃ ⟶ c₄) {Z : D}
  (h_1 :
    CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d₂ c₂) c₄ ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom f
        (CategoryTheory.MonoidalCategoryStruct.tensorHom g h))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d₂ c₂ c₄).hom h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d₁ c₁ c₃).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom
          (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom f g) h)
        h_1)
-- Mathlib.RingTheory.WittVector.StructurePolynomial
wittStructureInt.congr_simp : ∀ (p p_1 : ℕ) (e_p : p = p_1) {idx : Type u_2} [hp : Fact (Nat.Prime p)] (Φ Φ_1 : MvPolynomial idx ℤ),
  Φ = Φ_1 → ∀ (n n_1 : ℕ), n = n_1 → wittStructureInt p Φ n = wittStructureInt p_1 Φ_1 n_1
-- Mathlib.CategoryTheory.Adhesive.Basic
CategoryTheory.Adhesive.hasPullback_of_mono_left : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Adhesive C] {X Y S : C} (f : X ⟶ S)
  (g : Y ⟶ S) [CategoryTheory.Mono f], CategoryTheory.Limits.HasPullback f g
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.mono'_enorm : ∀ {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace ε]
  [inst_1 : ContinuousENorm ε] {f : α → ε} {g : α → ENNReal},
  MeasureTheory.Integrable g μ →
    MeasureTheory.AEStronglyMeasurable f μ → (∀ᵐ (a : α) ∂μ, ‖f a‖ₑ ≤ g a) → MeasureTheory.Integrable f μ
-- Mathlib.Algebra.Order.Monoid.Submonoid
/-- The submonoid of elements that are at least `1`.  -/
Submonoid.oneLE : (M : Type u_1) → [inst : Monoid M] → [inst_1 : Preorder M] → [MulLeftMono M] → Submonoid M
-- Mathlib.RingTheory.Extension.Presentation.Basic
Algebra.Presentation.ofAlgEquiv_relation : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Presentation R S ι σ) {T : Type u_1} [inst_3 : CommRing T] [inst_4 : Algebra R T] (e : S ≃ₐ[R] T)
  (i : σ), (P.ofAlgEquiv e).relation i = P.relation i
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Subsemigroup.opEquiv.eq_1 : ∀ {M : Type u_2} [inst : Mul M],
  Subsemigroup.opEquiv =
    { toFun := Subsemigroup.op, invFun := Subsemigroup.unop, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.FinMeasAdditive.add_measure : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} {T T' : Set α → β}
  [inst : AddCommMonoid β] {ν : MeasureTheory.Measure α},
  MeasureTheory.FinMeasAdditive μ T →
    MeasureTheory.FinMeasAdditive ν T' → MeasureTheory.FinMeasAdditive (μ + ν) (T + T')
-- Mathlib.NumberTheory.GaussSum
gaussSum.eq_1 : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Fintype R] {R' : Type v} [inst_2 : CommRing R'] (χ : MulChar R R')
  (ψ : AddChar R R'), gaussSum χ ψ = ∑ a, χ a * ψ a
-- Mathlib.Data.Rat.Cast.Order
Rat.castOrderEmbedding_apply : ∀ {K : Type u_5} [inst : Field K] [inst_1 : LinearOrder K] [inst_2 : IsStrictOrderedRing K] (a : ℚ),
  Rat.castOrderEmbedding a = ↑a
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback₃.p₁₃_p_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S}
  {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃}
  {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} (h : CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃) {Z : C}
  (h_1 : S ⟶ Z),
  CategoryTheory.CategoryStruct.comp h.p₁₃ (CategoryTheory.CategoryStruct.comp h₁₃.p h_1) =
    CategoryTheory.CategoryStruct.comp h.p h_1
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Hom.isoOpensRange.eq_1 : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f],
  AlgebraicGeometry.Scheme.Hom.isoOpensRange f =
    AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq f (AlgebraicGeometry.Scheme.Hom.opensRange f).ι ⋯
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.fix.inj : ∀ {a a_1 : Turing.ToPartrec.Code}, a.fix = a_1.fix → a = a_1
-- Lean.Elab.PreDefinition.FixedParams
Lean.Elab.FixedParams.Info.graph : Lean.Elab.FixedParams.Info → Array (Array (Option (Array (Option ℕ))))
-- Mathlib.GroupTheory.PGroup
IsPGroup.bot_lt_center : ∀ {p : ℕ} {G : Type u_1} [inst : Group G],
  IsPGroup p G → ∀ [hp : Fact (Nat.Prime p)] [Nontrivial G] [Finite G], ⊥ < Subgroup.center G
-- Mathlib.Analysis.Meromorphic.Basic
/-- Finprods of meromorphic functions are meromorphic.  -/
MeromorphicAt.finprod : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {ι : Type u_5} {F : ι → 𝕜 → 𝕜'} {x : 𝕜},
  (∀ (i : ι), MeromorphicAt (F i) x) → MeromorphicAt (∏ᶠ (i : ι), F i) x
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.hom_ext₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 2}
  {φ φ' : f ⟶ g},
  CategoryTheory.ComposableArrows.app' φ 0 _proof_245✝ = CategoryTheory.ComposableArrows.app' φ' 0 _proof_245✝ →
    CategoryTheory.ComposableArrows.app' φ 1 _proof_246✝ = CategoryTheory.ComposableArrows.app' φ' 1 _proof_246✝ →
      CategoryTheory.ComposableArrows.app' φ 2 _proof_247✝ = CategoryTheory.ComposableArrows.app' φ' 2 _proof_247✝ →
        φ = φ'
-- Init.Control.EState
EStateM.instToStringResult : {ε σ α : Type u} → [ToString ε] → [ToString α] → ToString (EStateM.Result ε σ α)
-- Mathlib.Algebra.CharP.Two
CharTwo.multiset_sum_sq : ∀ {R : Type u_1} [inst : CommSemiring R] [CharP R 2] (l : Multiset R), l.sum ^ 2 = (Multiset.map (fun x => x ^ 2) l).sum
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.LaxBraidedFunctor.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.MonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D] [inst_6 : SizeOf C]
  [inst_7 : SizeOf D] (toFunctor : CategoryTheory.Functor C D)
  (laxBraided : autoParam toFunctor.LaxBraided CategoryTheory.LaxBraidedFunctor.laxBraided._autoParam),
  sizeOf { toFunctor := toFunctor, laxBraided := laxBraided } = 1 + sizeOf toFunctor + sizeOf laxBraided
-- Mathlib.Data.Nat.Factorization.Root
/-- The RHS is a noncomputable version of `Nat.floorRoot` with better order-theoretic
properties.  -/
Nat.floorRoot_def : ∀ {a n : ℕ}, n.floorRoot a = if n = 0 ∨ a = 0 then 0 else (a.factorization ⌊/⌋ n).prod fun x1 x2 => x1 ^ x2
-- Mathlib.Combinatorics.Quiver.ConnectedComponent
/-- The weakly connected component corresponding to a vertex.  -/
Quiver.WeaklyConnectedComponent.mk : {V : Type u_1} → [inst : Quiver V] → V → Quiver.WeaklyConnectedComponent V
-- Lean.Elab.Deriving.Basic
/-- Delta deriving handler. Creates an instance of class `classStx` for `decl`.
The elaborated class expression may be underapplied (e.g. `Decidable` instead of `Decidable _`),
and may be `decl`.
If unfolding `decl` results in an underapplied lambda, then this enters the body of the lambda.
We prevent `classStx` from referring to these local variables; instead it's expected that one uses section variables.

This function can handle being run from within a nontrivial local context,
and it uses `mkValueTypeClosure` to construct the final instance.
 -/
Lean.Elab.Term.processDefDeriving : Lean.Elab.DerivingClassView →
  Lean.Expr → optParam Bool false → optParam (Option Lean.Syntax) none → Lean.Elab.TermElabM Unit
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.addXYZ_of_Z_eq_zero_right : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} [NoZeroDivisors R] {P Q : Fin 3 → R},
  W'.Equation Q → Q 2 = 0 → W'.addXYZ P Q = -(Q 1 ^ 2 * P 2) • P
-- Mathlib.Order.UpperLower.Principal
LowerSet.Iio_bot : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderBot α], LowerSet.Iio ⊥ = ⊥
-- Mathlib.CategoryTheory.Sites.LocalSite
/-- The right adjoint to the global sections functor that exists over any local site. This is
implemented as the skyscraper functor associated to `point.{w} J`, but can be thought of
as taking any object `X : A` to the sheaf that sends each `Y : C` to the product over copies of `A`
indexed by the points `⊤_ C ⟶ Y` of `Y`.

Note this takes in an extra universe parameter `w` that does not appear in the output type
`A ⥤ Sheaf J A` but is required for the construction; it should always be given explicitly when
referring to this functor, as in e.g. `coconstantSheaf.{w} J A`.  -/
CategoryTheory.GrothendieckTopology.IsLocalSite.coconstantSheaf : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      [CategoryTheory.LocallySmall.{w, v, u} C] →
        [J.IsLocalSite] →
          (A : Type u') →
            [inst_3 : CategoryTheory.Category.{v', u'} A] →
              [CategoryTheory.Limits.HasProducts A] → CategoryTheory.Functor A (CategoryTheory.Sheaf J A)
-- Batteries.Data.Nat.Bisect
Nat.start_le_bisect : ∀ {start stop : ℕ} {p : ℕ → Bool} (h : start < stop) (hstart : p start = true) (hstop : p stop = false),
  start ≤ Nat.bisect h hstart hstop
-- Std.Data.DTreeMap.Slice
Std.DTreeMap.toList_roc : ∀ {α : Type u} {β : α → Type v} (cmp : autoParam (α → α → Ordering) Std.DTreeMap.toList_roc._auto_1) [Std.TransCmp cmp]
  {t : Std.DTreeMap α β cmp} {lowerBound upperBound : α},
  Std.Slice.toList (Std.Roc.Sliceable.mkSlice t lowerBound<...=upperBound) =
    List.filter (fun e => decide ((cmp e.fst lowerBound).isGT = true ∧ (cmp e.fst upperBound).isLE = true)) t.toList
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.foldr_eq_foldr_toList : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {δ : Type w}
  {f : (a : α) → β a → δ → δ} {init : δ},
  Std.DTreeMap.foldr f init t = List.foldr (fun a b => f a.fst a.snd b) init t.toList
-- Lean.Data.Json.Printer
Lean.Json.compress : Lean.Json → String
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
/-- The tensor product of two objects with left duals has a left dual,
given by the tensor product of the duals in the opposite order.  -/
CategoryTheory.hasLeftDualTensor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {X Y : C} →
        [CategoryTheory.HasLeftDual X] →
          [CategoryTheory.HasLeftDual Y] →
            CategoryTheory.HasLeftDual (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
-- Mathlib.Analysis.Normed.Ring.InfiniteSum
summable_mul_of_summable_norm' : ∀ {R : Type u_1} {ι : Type u_2} {ι' : Type u_3} [inst : NormedRing R] {f : ι → R} {g : ι' → R},
  (Summable fun x => ‖f x‖) → Summable f → (Summable fun x => ‖g x‖) → Summable g → Summable fun x => f x.1 * g x.2
-- Lean.Compiler.LCNF.Types
_private.Lean.Compiler.LCNF.Types.0.Lean.Compiler.LCNF.toLCNFType.visitForall.match_9.eq_2 : ∀ (motive : Lean.Expr → Sort u_1) (x : Lean.Expr)
  (h_1 : (n : Lean.Name) → (d b : Lean.Expr) → (bi : Lean.BinderInfo) → motive (Lean.Expr.forallE n d b bi))
  (h_2 : (x : Lean.Expr) → motive x),
  (∀ (n : Lean.Name) (d b : Lean.Expr) (bi : Lean.BinderInfo), x = Lean.Expr.forallE n d b bi → False) →
    (match x with
      | Lean.Expr.forallE n d b bi => h_1 n d b bi
      | x => h_2 x) =
      h_2 x
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
CochainComplex.shiftFunctorObjXIso.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : CochainComplex C ℤ) (n i m : ℤ) (hm : m = i + n),
  K.shiftFunctorObjXIso n i m hm = HomologicalComplex.XIsoOfEq K ⋯
-- Mathlib.Combinatorics.Enumerative.DyckWord
_private.Mathlib.Combinatorics.Enumerative.DyckWord.0.DyckWord.ofTree.match_1.eq_1 : ∀ (motive : BinaryTree Unit → Sort u_1) (h_1 : Unit → motive BinaryTree.nil)
  (h_2 : (value : Unit) → (l r : BinaryTree Unit) → motive (BinaryTree.node value l r)),
  (match BinaryTree.nil with
    | BinaryTree.nil => h_1 ()
    | BinaryTree.node value l r => h_2 value l r) =
    h_1 ()
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.StrongEpiMonoFactorisation.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {f : X ⟶ Y} →
        (toMonoFactorisation : CategoryTheory.Limits.MonoFactorisation f) →
          [e_strong_epi : CategoryTheory.StrongEpi toMonoFactorisation.e] →
            CategoryTheory.Limits.StrongEpiMonoFactorisation f
-- Mathlib.Data.Ordmap.Ordset
Ordset.empty_iff : ∀ {α : Type u_1} [inst : Preorder α] {s : Ordset α}, s = ∅ ↔ (↑s).empty = true
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
/-- If `G` is an additive group with measurable addition, then addition of `g : G`
on the right is a measurable automorphism of `G`.  -/
MeasurableEquiv.addRight : {G : Type u_1} → [inst : AddGroup G] → [inst_1 : MeasurableSpace G] → [MeasurableAdd G] → G → G ≃ᵐ G
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.comap_upperCentralSeries : ∀ {G : Type u_1} [inst : AddGroup G] {H : Type u_2} [inst_1 : AddGroup H] (e : H ≃+ G) (n : ℕ),
  AddSubgroup.comap (↑e) (AddSubgroup.upperCentralSeries G n) = AddSubgroup.upperCentralSeries H n
-- Init.Data.UInt.Lemmas
UInt32.sub_eq_add_neg : ∀ (a b : UInt32), a - b = a + -b
-- Lean.Server.Rpc.Basic
Lean.Server.instRpcEncodableWithRpcRefOfTypeName.rpcEncode : {α : Type} → [TypeName α] → Lean.Server.WithRpcRef α → StateM Lean.Server.RpcObjectStore Lean.Json