mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.lintegral_biUnion : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : Set β} {s : β → Set α},
  t.Countable →
    (∀ i ∈ t, MeasurableSet (s i)) →
      t.PairwiseDisjoint s →
        ∀ (f : α → ENNReal), ∫⁻ (a : α) in ⋃ i ∈ t, s i, f a ∂μ = ∑' (i : ↑t), ∫⁻ (a : α) in s ↑i, f a ∂μ
-- Mathlib.Algebra.Star.NonUnitalSubsemiring
/-- Copy of a non-unital star subsemiring with a new `carrier` equal to the old one.
Useful to fix definitional equalities.  -/
NonUnitalStarSubsemiring.copy : {R : Type v} →
  [inst : NonUnitalNonAssocSemiring R] →
    [inst_1 : StarRing R] → (S : NonUnitalStarSubsemiring R) → (s : Set R) → s = ↑S → NonUnitalStarSubsemiring R
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cocycle.equivHomShift_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ} (a : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L),
  CochainComplex.HomComplex.Cocycle.equivHomShift a = (CochainComplex.HomComplex.Cocycle.ofHom a).rightUnshift n ⋯
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get!_erase : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : Inhabited α] [inst_1 : EquivBEq α]
  [inst_2 : LawfulHashable α] {k a : α}, (m.erase k).get! a = if (k == a) = true then default else m.get! a
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
AlgebraicGeometry.PresheafedSpace.GlueData.ι_image_preimage_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C)
  [inst_1 : CategoryTheory.Limits.HasLimits C] (i j : D.J) (U : TopologicalSpace.Opens ↑↑(D.U i)),
  (TopologicalSpace.Opens.map (D.ι j).base).obj (⋯.functor.obj U) =
    (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor (D.f j i)).obj
      ((TopologicalSpace.Opens.map (D.t j i).base).obj ((TopologicalSpace.Opens.map (D.f i j).base).obj U))
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.id_apply : ∀ {α : Type u_1} {mα : MeasurableSpace α} (a : α), ProbabilityTheory.Kernel.id a = MeasureTheory.Measure.dirac a
-- Batteries.Control.ForInStep.Lemmas
ForInStep.bindList_cons : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (f : α → β → m (ForInStep β))
  (s : ForInStep β) (a : α) (l : List α),
  ForInStep.bindList f (a :: l) s =
    s.bind fun b => do
      let x ← f a b
      ForInStep.bindList f l x
-- Mathlib.Data.Set.Card
Set.encard_le_one_iff_subsingleton : ∀ {α : Type u_1} {s : Set α}, s.encard ≤ 1 ↔ s.Subsingleton
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.getKey? : {α : Type u} → {β : α → Type v} → [Ord α] → Std.DTreeMap.Internal.Impl α β → α → Option α
-- Mathlib.RingTheory.Extension.Cotangent.Basis
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.hgmem : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type u_4}
  {P : Algebra.Generators R S ι} {σ : Type u_5} {b : Module.Basis σ S P.toExtension.Cotangent}
  (self : Algebra.Generators.PresentationOfFreeCotangent.Aux✝ P b),
  Algebra.Generators.PresentationOfFreeCotangent.Aux.g✝ self - 1 ∈ P.ker
-- Mathlib.Algebra.Quandle
Shelf.mk : {α : Type u} → (act : α → α → α) → (∀ {x y z : α}, act x (act y z) = act (act x y) (act x z)) → Shelf α
-- Mathlib.Combinatorics.SimpleGraph.Ends.Defs
SimpleGraph.ComponentCompl.notMem_of_mem : ∀ {V : Type u} {G : SimpleGraph V} {K : Set V} {C : G.ComponentCompl K} {c : V}, c ∈ C → c ∉ K
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
CategoryTheory.Limits.pushoutCoconeOfRightIso_ι_app_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
  [inst_1 : CategoryTheory.IsIso g],
  (CategoryTheory.Limits.pushoutCoconeOfRightIso f g).ι.app CategoryTheory.Limits.WalkingSpan.right =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.inv g) f
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
DihedralGroup.r_mul_sr : ∀ {n : ℕ} (i j : ZMod n), DihedralGroup.r i * DihedralGroup.sr j = DihedralGroup.sr (j - i)
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.unopComp_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} E] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ)
  (G : CategoryTheory.Functor Dᵒᵖ Eᵒᵖ) (X : C),
  (F.unopComp G).inv.app X = CategoryTheory.CategoryStruct.id (Opposite.unop (G.obj (F.obj (Opposite.op X))))
-- Mathlib.CategoryTheory.PathCategory.Basic
/-- Two functors out of a path category are equal when they agree on singleton paths.  -/
CategoryTheory.Paths.ext_functor : ∀ {V : Type u₁} [inst : Quiver V] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  {F G : CategoryTheory.Functor (CategoryTheory.Paths V) C} (h_obj : F.obj = G.obj),
  (∀ (a b : V) (e : a ⟶ b),
      F.map e.toPath =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
          (CategoryTheory.CategoryStruct.comp (G.map e.toPath) (CategoryTheory.eqToHom ⋯))) →
    F = G
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.range_finite : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [CompactSpace X] (f : LocallyConstant X Y),
  (Set.range ⇑f).Finite
-- Mathlib.Algebra.Homology.ComplexShapeSigns
ComplexShape.ε_zero : ∀ {I : Type u_7} [inst : AddMonoid I] (c : ComplexShape I) [inst_1 : c.TensorSigns], c.ε 0 = 1
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.id_toCoalgHom : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : CoalgebraStruct R A], ↑(BialgHom.id R A) = CoalgHom.id R A
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.Splitting.instFunLike : {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) → FunLike S.Splitting G E
-- Mathlib.Order.Bounded
Set.bounded_gt_inter_not_gt : ∀ {α : Type u_1} {s : Set α} [inst : SemilatticeInf α] (a : α),
  Set.Bounded (fun x1 x2 => x1 > x2) (s ∩ {b | ¬a < b}) ↔ Set.Bounded (fun x1 x2 => x1 > x2) s
-- Mathlib.Combinatorics.SimpleGraph.Walk.Counting
SimpleGraph.fintypeSubtypeWalkLength : {V : Type u} →
  (G : SimpleGraph V) → [DecidableEq V] → [G.LocallyFinite] → (u v : V) → (n : ℕ) → Fintype { p // p.length = n }
-- Mathlib.NumberTheory.LucasLehmer
/-- The Lucas-Lehmer residue is `s p (p-2)` in `ZMod (2^p - 1)`.  -/
LucasLehmer.lucasLehmerResidue : (p : ℕ) → ZMod (2 ^ p - 1)
-- Mathlib.Analysis.Convex.Function
ConcaveOn.left_le_of_le_right : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : LinearOrder β] [IsOrderedCancelAddMonoid β] [inst_6 : SMul 𝕜 E]
  [inst_7 : Module 𝕜 β] [PosSMulStrictMono 𝕜 β] {s : Set E} {f : E → β},
  ConcaveOn 𝕜 s f → ∀ {x y z : E}, x ∈ s → y ∈ s → z ∈ openSegment 𝕜 x y → f z ≤ f y → f x ≤ f z
-- Mathlib.Data.Set.Card
Set.ncard_le_ncard_sdiff_add_ncard : ∀ {α : Type u_1} (s t : Set α),
  autoParam t.Finite Set.ncard_le_ncard_sdiff_add_ncard._auto_1 → s.ncard ≤ (s \ t).ncard + t.ncard
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- the tensorator of a lax monoidal functor  -/
CategoryTheory.Functor.LaxMonoidal.μ : {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 D} →
            (F : CategoryTheory.Functor C D) →
              [self : F.LaxMonoidal] →
                (X Y : C) →
                  CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y) ⟶
                    F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.left : Nat.Partrec.Code
-- Init.Data.Array.Lemmas
Array.toList_reverse : ∀ {α : Type u_1} {xs : Array α}, xs.reverse.toList = xs.toList.reverse
-- Mathlib.Topology.Algebra.Group.Basic
Filter.Tendsto.div_const' : ∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : Div G] [ContinuousDiv G] {c : G} {f : α → G}
  {l : Filter α}, Filter.Tendsto f l (nhds c) → ∀ (b : G), Filter.Tendsto (fun x => f x / b) l (nhds (c / b))
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.kahler_comp_rightAngleRotation : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) (x y : E), (o.kahler (o.rightAngleRotation x)) (o.rightAngleRotation y) = (o.kahler x) y
-- Mathlib.Order.BooleanAlgebra.Set
Set.sdiff_univ : ∀ {α : Type u_1} (s : Set α), s \ Set.univ = ∅
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKeyD.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtDTreeMap α β cmp),
  t = t_1 → ∀ (fallback fallback_1 : α), fallback = fallback_1 → t.minKeyD fallback = t_1.minKeyD fallback_1
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.vadd_set_subset_iff_subset_neg_vadd_set : ∀ {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : AddAction α β] {A B : Set β} {a : α},
  a +ᵥ A ⊆ B ↔ A ⊆ -a +ᵥ B
-- Mathlib.Order.KonigLemma
GradeMinOrder.exists_nat_orderEmbedding_of_forall_covby_finite : ∀ {α : Type u_1} [inst : PartialOrder α] [IsStronglyAtomic α] [inst_2 : GradeMinOrder ℕ α] [inst_3 : OrderBot α]
  [Infinite α],
  (∀ (a : α), {x | a ⋖ x}.Finite) → ∃ f, f 0 = ⊥ ∧ (∀ (i : ℕ), f i ⋖ f (i + 1)) ∧ ∀ (i : ℕ), grade ℕ (f i) = i
-- Mathlib.CategoryTheory.Groupoid
/-- `inv f` composed `f` is the identity  -/
CategoryTheory.Groupoid.inv_comp : ∀ {obj : Type u} [self : CategoryTheory.Groupoid obj] {X Y : obj} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Groupoid.inv f) f = CategoryTheory.CategoryStruct.id Y
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.ExtTheorems : Type
-- Mathlib.CategoryTheory.Monoidal.Internal.Limits
CategoryTheory.Mon.limit_X : ∀ {J : Type w} [inst : CategoryTheory.Category.{v_1, w} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (F : CategoryTheory.Functor J (CategoryTheory.Mon C))
  (c : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Mon.forget C))) (hc : CategoryTheory.Limits.IsLimit c),
  (CategoryTheory.Mon.limit F c hc).X = c.pt
-- Mathlib.AlgebraicGeometry.Sites.Small
AlgebraicGeometry.Scheme.Cover.toPresieveOver_le_arrows_iff : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {S : AlgebraicGeometry.Scheme}
  [inst : P.IsStableUnderBaseChange] {X : CategoryTheory.Over S} (R : CategoryTheory.Sieve X)
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X.left)
  [inst_1 : AlgebraicGeometry.Scheme.Cover.Over S 𝒰],
  𝒰.toPresieveOver ≤ R.arrows ↔ CategoryTheory.Presieve.ofArrows 𝒰.X 𝒰.f ≤ ((CategoryTheory.Sieve.overEquiv X) R).arrows
-- Lean.Meta.Tactic.SplitIf
Lean.Meta.FindSplitImpl.Context.mk.inj : ∀ {exceptionSet : Lean.ExprSet} {kind : Lean.Meta.SplitKind} {exceptionSet_1 : Lean.ExprSet}
  {kind_1 : Lean.Meta.SplitKind},
  { exceptionSet := exceptionSet, kind := kind } = { exceptionSet := exceptionSet_1, kind := kind_1 } →
    exceptionSet = exceptionSet_1 ∧ kind = kind_1
-- Init.Data.UInt.Lemmas
mod_uInt64Size_uSizeSize : ∀ (n : ℕ), n % UInt64.size % USize.size = n % USize.size
-- Init.Data.List.TakeDrop
List.take_append_getElem : ∀ {α : Type u_1} {l : List α} {i : ℕ} (h : i < l.length), List.take i l ++ [l[i]] = List.take (i + 1) l
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.fromArrowArrowFunctor_obj_f₂₄ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)),
  (CategoryTheory.Square.fromArrowArrowFunctor.obj f).f₂₄ = f.right.hom
-- Aesop.Frontend.Saturate
Aesop.Frontend.elabForwardRuleSet : Option (Lean.TSyntax `Aesop.Frontend.Parser.usingRuleSets) →
  Option (Lean.TSyntax `Aesop.Frontend.Parser.additionalRules) → Aesop.Options' → Aesop.ElabM Aesop.LocalRuleSet
-- Mathlib.RingTheory.Congruence.Defs
RingCon.instInhabited : {R : Type u_1} → [inst : Add R] → [inst_1 : Mul R] → Inhabited (RingCon R)
-- Init.System.IO
IO.FS.FileType.other.sizeOf_spec : sizeOf IO.FS.FileType.other = 1
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
/-- A category has coequalizers of reflexive pairs if and only if it has all colimits indexed by the
walking reflexive pair.  -/
CategoryTheory.Limits.hasReflexiveCoequalizers_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.Limits.HasColimitsOfShape CategoryTheory.Limits.WalkingReflexivePair C ↔
    CategoryTheory.Limits.HasReflexiveCoequalizers C
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.ComonadHom.mk.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {M N : CategoryTheory.Comonad C}
  (toNatTrans toNatTrans_1 : CategoryTheory.NatTrans M.toFunctor N.toFunctor) (e_toNatTrans : toNatTrans = toNatTrans_1)
  (app_ε : ∀ (X : C), CategoryTheory.CategoryStruct.comp (toNatTrans.app X) (N.ε.app X) = M.ε.app X)
  (app_δ :
    ∀ (X : C),
      CategoryTheory.CategoryStruct.comp (toNatTrans.app X) (N.δ.app X) =
        CategoryTheory.CategoryStruct.comp (M.δ.app X)
          (CategoryTheory.CategoryStruct.comp (toNatTrans.app (M.obj X)) (N.map (toNatTrans.app X)))),
  { toNatTrans := toNatTrans, app_ε := app_ε, app_δ := app_δ } = { toNatTrans := toNatTrans_1, app_ε := ⋯, app_δ := ⋯ }
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.bijective : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂), Function.Bijective ⇑e
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.instFintypeSubtypeMemTop : {R : Type u_1} → [inst : NonAssocRing R] → [Fintype R] → Fintype ↥⊤
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.compare_minKey?_modify_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp] (h : t.WF)
  {k : α} {f : β → β} {km kmm : α} (hkm : t.minKey? = some km),
  (t.modify k f).minKey?.get ⋯ = kmm → cmp kmm km = Ordering.eq
-- Init.Data.List.Lemmas
List.sum_eq_foldl : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : Add α] [Std.Associative fun x1 x2 => x1 + x2]
  [Std.LawfulIdentity (fun x1 x2 => x1 + x2) 0] {xs : List α}, xs.sum = List.foldl (fun x1 x2 => x1 + x2) 0 xs
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
PresheafOfModules.Sheafify.SMulCandidate.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} {α : R₀ ⟶ R.obj}
  {M₀ : PresheafOfModules R₀} {A : CategoryTheory.Sheaf J AddCommGrpCat} {φ : M₀.presheaf ⟶ A.obj} {X : Cᵒᵖ}
  {r : ↑(R.obj.obj X)} {m : ↑(A.obj.obj X)} (x : ↑(A.obj.obj X))
  (h :
    ∀ ⦃Y : Cᵒᵖ⦄ (f : X ⟶ Y) (r₀ : ↑(R₀.obj Y)),
      (CategoryTheory.ConcreteCategory.hom (α.app Y)) r₀ = (CategoryTheory.ConcreteCategory.hom (R.obj.map f)) r →
        ∀ (m₀ : ↑(M₀.obj Y)),
          (CategoryTheory.ConcreteCategory.hom (φ.app Y)) m₀ = (CategoryTheory.ConcreteCategory.hom (A.obj.map f)) m →
            (CategoryTheory.ConcreteCategory.hom (A.obj.map f)) x =
              (CategoryTheory.ConcreteCategory.hom (φ.app Y)) (r₀ • m₀))
  (x_1 : ↑(A.obj.obj X))
  (h_1 :
    ∀ ⦃Y : Cᵒᵖ⦄ (f : X ⟶ Y) (r₀ : ↑(R₀.obj Y)),
      (CategoryTheory.ConcreteCategory.hom (α.app Y)) r₀ = (CategoryTheory.ConcreteCategory.hom (R.obj.map f)) r →
        ∀ (m₀ : ↑(M₀.obj Y)),
          (CategoryTheory.ConcreteCategory.hom (φ.app Y)) m₀ = (CategoryTheory.ConcreteCategory.hom (A.obj.map f)) m →
            (CategoryTheory.ConcreteCategory.hom (A.obj.map f)) x_1 =
              (CategoryTheory.ConcreteCategory.hom (φ.app Y)) (r₀ • m₀)),
  ({ x := x, h := h } = { x := x_1, h := h_1 }) = (x = x_1)
-- Mathlib.Data.Nat.Nth
Nat.lt_nth_iff_count_lt : ∀ {p : ℕ → Prop} [inst : DecidablePred p], (Set.ofPred p).Infinite → ∀ {a b : ℕ}, a < Nat.count p b ↔ Nat.nth p a < b
-- Mathlib.Analysis.InnerProductSpace.Defs
InnerProductSpace.Core.inner_sub_sub_self : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [c : PreInnerProductSpace.Core 𝕜 F] (x y : F),
  inner 𝕜 (x - y) (x - y) = inner 𝕜 x x - inner 𝕜 x y - inner 𝕜 y x + inner 𝕜 y y
-- Mathlib.Data.List.Sublists
List.pairwise_sublists : ∀ {α : Type u} {R : α → α → Prop} {l : List α},
  List.Pairwise R l → List.Pairwise (Function.onFun (List.Lex R) List.reverse) l.sublists
-- Mathlib.AlgebraicGeometry.Fiber
/-- A point `x` as a point in the fiber of `f` at `f x`.  -/
AlgebraicGeometry.Scheme.Hom.asFiber : {X Y : AlgebraicGeometry.Scheme} → (f : X ⟶ Y) → (x : ↥X) → ↥(AlgebraicGeometry.Scheme.Hom.fiber f (f x))
-- Lean.Elab.ConfigEval.Types
/-- Evaluation of an elaborated expression.
If the expression is not recognizable, then the instance may throw an exception.
They can throw `ConfigEval.throwUnsupportedExpr` to signal that a generic error should be reported.

The provided expression does not contain expression metavariables or `sorry`, but
level metavariables may be present. We assume these do not affect evaluation.
If `expectedType?` is provided, then the expression is coerced as necessary to have this type.
 -/
Lean.Elab.ConfigEval.EvalExpr.evalExpr : {α : Type} → [self : Lean.Elab.ConfigEval.EvalExpr α] → Lean.Expr → Lean.MetaM α
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.main : Lean.Expr → ℕ → Lean.MetaM (Option Lean.Meta.AbstractMVarsResult)
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.neg_hom₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C} [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (f : T₁ ⟶ T₂), (-f).hom₂ = -f.hom₂
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for signed remainder of `BitVec`s.  -/
BitVec.reduceSRem : Lean.Meta.Simp.DSimproc
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
Fintype.linearIndependent_iff : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {v : ι → M} [inst_3 : Fintype ι], LinearIndependent R v ↔ ∀ (g : ι → R), ∑ i, g i • v i = 0 → ∀ (i : ι), g i = 0
-- Mathlib.Topology.Separation.Regular
/-- A regular space is R₁.  -/
instR1Space : ∀ {X : Type u_1} [inst : TopologicalSpace X] [RegularSpace X], R1Space X
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
/-- Variant of `le_mul_of_one_le_left` for `b` non-positive instead of non-negative.  -/
mul_le_of_one_le_left : ∀ {R : Type u} [inst : Semiring R] [inst_1 : Preorder R] {a b : R} [ExistsAddOfLE R] [MulPosMono R] [AddRightMono R]
  [AddRightReflectLE R], b ≤ 0 → 1 ≤ a → a * b ≤ b
-- Mathlib.CategoryTheory.Idempotents.FunctorCategories
CategoryTheory.Idempotents.app_comp_p : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C]
  {P Q : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Functor J C)} (f : P ⟶ Q) (X : J),
  CategoryTheory.CategoryStruct.comp (f.f.app X) (Q.p.app X) = f.f.app X
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.deriv_norm_ne_zero : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F : Polynomial R} {a : ℤ_[p]},
  ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 →
    ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ≠ 0
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.subsingleton_of_finrank_adjoin_eq_one : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E],
  (∀ (x : E), Module.finrank F ↥F⟮x⟯ = 1) → Subsingleton (IntermediateField F E)
-- Mathlib.CategoryTheory.Category.ULift
CategoryTheory.ULiftHom.down_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (A : CategoryTheory.ULiftHom C),
  CategoryTheory.ULiftHom.down.obj A = A.objDown
-- Mathlib.Data.Multiset.Powerset
Multiset.powerset_eq_singleton_zero_iff : ∀ {α : Type u_1} (s : Multiset α), s.powerset = {0} ↔ s = 0
-- Init.Data.String.PosRaw
String.Pos.Raw.byteIdx_offsetBy : ∀ {p offset : String.Pos.Raw}, (p.offsetBy offset).byteIdx = offset.byteIdx + p.byteIdx
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PushoutObjObj.ofHasPushout_inl : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₂ Y₂ : C₂} (f₂ : X₂ ⟶ Y₂)
  [inst_3 : CategoryTheory.Limits.HasPushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂)],
  (CategoryTheory.Functor.PushoutObjObj.ofHasPushout F f₁ f₂).inl =
    CategoryTheory.Limits.pushout.inl ((F.map f₁).app X₂) ((F.obj X₁).map f₂)
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.restoreAssignments_performRupCheck : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n),
  f.assignments.size = n →
    ∀ (rupHints : Array ℕ),
      Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.restoreAssignments (f.performRupCheck rupHints).1.assignments
          (f.performRupCheck rupHints).2.1 =
        f.assignments
-- Mathlib.AlgebraicTopology.SimplexCategory.Truncated
SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one : CategoryTheory.CategoryStruct.comp
    (SimplexCategory.Truncated.δ₂ 0 SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_1
      SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_2)
    (SimplexCategory.Truncated.σ₂ 1 SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_2
      SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_1) =
  CategoryTheory.CategoryStruct.comp
    (SimplexCategory.Truncated.σ₂ 0 SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_3
      SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_4)
    (SimplexCategory.Truncated.δ₂ 0 SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_4
      SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_3)
-- Init.Data.BitVec.Bitblast
BitVec.intMin_eq_neg_two_pow : ∀ {w : ℕ}, BitVec.intMin w = BitVec.ofInt w (-2 ^ (w - 1))
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEmbedding.equivRange_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : α → β}
  (hf : MeasurableEmbedding f) (x : α), hf.equivRange x = ⟨f x, ⋯⟩
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
OpenPartialHomeomorph.MDifferentiable.comp_symm_deriv : ∀ {𝕜 : 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'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {e : OpenPartialHomeomorph M M'},
  OpenPartialHomeomorph.MDifferentiable I I' e →
    ∀ {x : M'},
      x ∈ e.target → mfderiv% ↑e (↑e.symm x) ∘SL mfderiv% ↑e.symm x = ContinuousLinearMap.id 𝕜 (TangentSpace I' x)
-- Mathlib.Order.Defs.LinearOrder
/-- A linear order is total.  -/
LinearOrder.le_total : ∀ {α : Type u_2} [self : LinearOrder α] (a b : α), a ≤ b ∨ b ≤ a