mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Pointwise.Set.BigOperators
/-- A special case of `Set.image_finsetSum_pi` for `Finset.univ`.  -/
Set.image_fintype_sum_pi : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : Fintype ι] (S : ι → Set α),
  (fun f => ∑ i, f i) '' Set.univ.pi S = ∑ i, S i
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.SeparatingRight.toMatrix' : ∀ {R₂ : Type u_3} [inst : CommRing R₂] {ι : Type u_6} [inst_1 : DecidableEq ι] [inst_2 : Fintype ι]
  {B : LinearMap.BilinForm R₂ (ι → R₂)}, LinearMap.SeparatingRight B → (LinearMap.BilinForm.toMatrix' B).SeparatingRight
-- Mathlib.Data.Finset.Image
Finset.map_ssubset_map : ∀ {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s t : Finset α}, Finset.map f s ⊂ Finset.map f t ↔ s ⊂ t
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.Lift.aux.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Group β] (f : α → β) (L : List (α × Bool)),
  FreeGroup.Lift.aux f L = (List.map (fun x => bif x.2 then f x.1 else (f x.1)⁻¹) L).prod
-- Mathlib.AlgebraicGeometry.Sites.AffineEtale
/-- The `Spec` functor from the small affine étale site of `S` to the small étale site of `S`.  -/
AlgebraicGeometry.Scheme.AffineEtale.Spec : (S : AlgebraicGeometry.Scheme) → CategoryTheory.Functor S.AffineEtale S.Etale
-- Mathlib.LinearAlgebra.BilinearForm.Properties
/-- A bilinear form is positive semidefinite if and only if it is positive semidefinite
as a sesquilinear form.  -/
LinearMap.BilinForm.isPosSemidef_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : LE R]
  {B : LinearMap.BilinForm R M}, B.IsPosSemidef ↔ LinearMap.IsPosSemidef B
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.transvection_mulVec_single_other : ∀ {ι : Type u_1} {F : Type u_2} [inst : DecidableEq ι] [inst_1 : Fintype ι] [inst_2 : CommRing F] {i j : ι}
  (hij : i ≠ j) (b : F),
  (↑(Matrix.SpecialLinearGroup.transvection hij b)).mulVec (Pi.single j 1) = Pi.single j 1 + b • Pi.single i 1
-- Lean.Data.Lsp.Workspace
Lean.Lsp.instFromJsonWorkspaceFolder.fromJson : Lean.Json → Except String Lean.Lsp.WorkspaceFolder
-- Mathlib.Order.LiminfLimsup
Filter.frequently_lt_of_lt_limsup : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLinearOrder β] {f : Filter α} {u : α → β} {b : β},
  autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) Filter.frequently_lt_of_lt_limsup._auto_1 →
    b < Filter.limsup u f → ∃ᶠ (x : α) in f, b < u x
-- Mathlib.Order.Antisymmetrization
antisymmetrization_fibration : ∀ {α : Type u_1} [inst : Preorder α],
  Relation.Fibration (fun x1 x2 => x1 < x2) (fun x1 x2 => x1 < x2) (toAntisymmetrization fun x1 x2 => x1 ≤ x2)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.not_isReal_of_mk_isComplex : ∀ {K : Type u_1} [inst : Field K] {φ : K →+* ℂ},
  (NumberField.InfinitePlace.mk φ).IsComplex → ¬NumberField.ComplexEmbedding.IsReal φ
-- Mathlib.CategoryTheory.Sites.Sheafification
/-- The sheafification of a presheaf `P`.  -/
CategoryTheory.sheafify : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {D : Type u_1} →
        [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
          [CategoryTheory.HasWeakSheafify J D] → CategoryTheory.Functor Cᵒᵖ D → CategoryTheory.Functor Cᵒᵖ D
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.instMin.eq_1 : ∀ {α : Type u_1} [inst : LE α], UpperSet.instMin = { min := fun s t => { carrier := ↑s ∪ ↑t, upper' := ⋯ } }
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
/-- Copy of a non-unital star subalgebra with a new `carrier` equal to the old one.
Useful to fix definitional equalities.  -/
NonUnitalStarSubalgebra.copy : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring A] →
        [inst_2 : Module R A] →
          [inst_3 : Star A] → (S : NonUnitalStarSubalgebra R A) → (s : Set A) → s = ↑S → NonUnitalStarSubalgebra R A
-- Batteries.Data.MLList.Basic
/-- Gives the monadic lazy list consisting all of folds of a function on a given initial element.
Thus `[a₀, a₁, ...].foldsM f b` will give `[b, ← f b a₀, ← f (← f b a₀) a₁, ...]`.  -/
MLList.foldsM : {m : Type u_1 → Type u_1} → {β α : Type u_1} → [Monad m] → (β → α → m β) → β → MLList m α → MLList m β
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.card_pow_le : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Monoid α] {s : Finset α} {n : ℕ}, (s ^ n).card ≤ s.card ^ n
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.isSheafFor_singleton : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X Y : C}
  {f : X ⟶ Y},
  CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Presieve.singleton f) ↔
    ∀ (x : P.obj (Opposite.op X)),
      (∀ {Z : C} (p₁ p₂ : Z ⟶ X),
          CategoryTheory.CategoryStruct.comp p₁ f = CategoryTheory.CategoryStruct.comp p₂ f →
            (CategoryTheory.ConcreteCategory.hom (P.map p₁.op)) x =
              (CategoryTheory.ConcreteCategory.hom (P.map p₂.op)) x) →
        ∃! y, (CategoryTheory.ConcreteCategory.hom (P.map f.op)) y = x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_insert : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited β] (h : t.WF) {k a : α} {v : β},
  Std.DTreeMap.Internal.Impl.Const.get! (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl a =
    if compare k a = Ordering.eq then v else Std.DTreeMap.Internal.Impl.Const.get! t a
-- Mathlib.Topology.Instances.CantorSet
/-- The preCantor sets are closed.  -/
isClosed_preCantorSet : ∀ (n : ℕ), IsClosed (preCantorSet n)
-- Mathlib.CategoryTheory.Limits.Types.Pushouts
CategoryTheory.Limits.Types.instHasPushoutsType : CategoryTheory.Limits.HasPushouts (Type u)
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.inr_v_desc_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ}
  (α : CochainComplex.HomComplex.Cochain K M 0) (β : CochainComplex.HomComplex.Cocycle L M 1)
  (hαβ : CochainComplex.HomComplex.δ 0 1 α + (CochainComplex.HomComplex.Cochain.ofHom φ).comp ↑β ⋯ = 0) (p q : ℤ)
  (hpq : p + 1 = q),
  CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCocone.inr φ)).v p q hpq)
      ((CochainComplex.mappingCocone.desc φ α β hαβ).f q) =
    (↑β).v p q hpq
-- Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
/-- Given the data of a basic constructible set `s = V(g₁, ..., gₙ) \ V(f)`, return `n`.  -/
PrimeSpectrum.BasicConstructibleSetData.n : {R : Type u_1} → PrimeSpectrum.BasicConstructibleSetData R → ℕ
-- Init.Data.Nat.Lemmas
Nat.pos_of_lt_add_left : ∀ {n k : ℕ}, n < k + n → 0 < k
-- Mathlib.Algebra.GroupWithZero.Basic
isNilpotent_of_subsingleton : ∀ {R : Type u_3} {x : R} [inst : Zero R] [inst_1 : Pow R ℕ] [Subsingleton R], IsNilpotent x
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.IsUpperSet.monotone_iff_continuous : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : TopologicalSpace α]
  [inst_3 : TopologicalSpace β] [Topology.IsUpperSet α] [Topology.IsUpperSet β] {f : α → β}, Monotone f ↔ Continuous f
-- Mathlib.Logic.Equiv.Set
EquivLike.range_eq_univ : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} [inst : EquivLike E α β] (e : E), Set.range ⇑e = Set.univ
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.floor_lt' : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] {a : R} {n : ℕ}
  [IsStrictOrderedRing R], n ≠ 0 → (⌊a⌋₊ < n ↔ a < ↑n)
-- Mathlib.RingTheory.Lasker
Submodule.IsMinimalPrimaryDecomposition.primary : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {N : Submodule R M} {t : Finset (Submodule R M)},
  N.IsMinimalPrimaryDecomposition t → ∀ ⦃J : Submodule R M⦄, J ∈ t → J.IsPrimary
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.IsImage.fac_lift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  {F : CategoryTheory.Limits.MonoFactorisation f} (hF : CategoryTheory.Limits.IsImage F)
  (F' : CategoryTheory.Limits.MonoFactorisation f), CategoryTheory.CategoryStruct.comp F.e (hF.lift F') = F'.e
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp₁.str : (self : SemiNormedGrp₁) → SeminormedAddCommGroup self.carrier
-- Mathlib.Analysis.LocallyConvex.WeakSpace
/-- The weak topology on a space with separating dual is T2 (Hausdorff).  -/
instT2SpaceWeakSpaceOfSeparatingDual : ∀ {R : Type u_4} {V : Type u_5} [inst : CommRing R] [inst_1 : TopologicalSpace R] [T2Space R] [inst_3 : ContinuousAdd R]
  [inst_4 : ContinuousConstSMul R R] [inst_5 : AddCommGroup V] [inst_6 : Module R V] [inst_7 : TopologicalSpace V]
  [SeparatingDual R V], T2Space (WeakSpace R V)
-- Mathlib.Algebra.Group.Subsemigroup.Defs
MulMemClass.toSemigroup.eq_1 : ∀ {M : Type u_4} [inst : Semigroup M] {A : Type u_5} [inst_1 : SetLike A M] [inst_2 : MulMemClass A M] (S : A),
  MulMemClass.toSemigroup S = { toMul := MulMemClass.mul S, mul_assoc := ⋯ }
-- Mathlib.Topology.PartitionOfUnity
PartitionOfUnity.instFunLikeContinuousMapReal : {ι : Type u} → {X : Type v} → [inst : TopologicalSpace X] → {s : Set X} → FunLike (PartitionOfUnity ι X s) ι C(X, ℝ)
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.addSubgroupOfEquivOfLe_symm_apply_coe_coe : ∀ {G : Type u_7} [inst : AddGroup G] {H K : AddSubgroup G} (h : H ≤ K) (g : ↥H),
  ↑↑((AddSubgroup.addSubgroupOfEquivOfLe h).symm g) = ↑g
-- Mathlib.Algebra.Notation.Pi.Basic
/-- On non-dependent functions, `Pi.single` can be expressed as an `ite`  -/
Pi.single_apply : ∀ {ι : Type u_1} [inst : DecidableEq ι] {M : Type u_9} [inst_1 : Zero M] (i : ι) (x : M) (i' : ι),
  Pi.single i x i' = if i' = i then x else 0
-- Aesop.Forward.State
/-- Context for the `AddM` monad.  -/
Aesop.ClusterState.AddM.Context : Type
-- Lean.Elab.Match
Lean.Elab.Term.PatternVarDecl.fvarId : Lean.Elab.Term.PatternVarDecl → Lean.FVarId
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
/-- If an alternating map satisfies an inequality `‖f m‖ ≤ C * ∏ i, ‖m i‖`,
then it is continuous.  -/
AlternatingMap.continuous_of_bound : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : Fintype ι] (f : E [⋀^ι]→ₗ[𝕜] F) (C : ℝ),
  (∀ (m : ι → E), ‖f m‖ ≤ C * ∏ i, ‖m i‖) → Continuous ⇑f
-- Mathlib.CategoryTheory.Monad.Limits
/-- For `D : J ⥤ Algebra T`, `D ⋙ forget T` has a colimit, then `D` has a colimit provided colimits
of shape `J` are preserved by `T`.
 -/
CategoryTheory.Monad.forget_creates_colimits_of_monad_preserves : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u}
  [inst_1 : CategoryTheory.Category.{v, u} J] [CategoryTheory.Limits.PreservesColimitsOfShape J T.toFunctor]
  (D : CategoryTheory.Functor J T.Algebra) [CategoryTheory.Limits.HasColimit (D.comp T.forget)],
  CategoryTheory.Limits.HasColimit D
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.map_polynomialZ : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Jacobian R) {S : Type s} [inst_1 : CommRing S] (f : R →+* S),
  (W'.map f).polynomialZ = (MvPolynomial.map f) W'.polynomialZ
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.snd_comp_swap : ∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : AddMonoid N],
  AddMonoid.Coprod.snd.comp (AddMonoid.Coprod.swap M N) = AddMonoid.Coprod.fst
-- Mathlib.Algebra.Module.SpanRankOperations
IsLocalRing.spanFinrank_eq_finrank_quotient : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : IsLocalRing R] (N : Submodule R M),
  N.FG → N.spanFinrank = Module.finrank (R ⧸ IsLocalRing.maximalIdeal R) (↥N ⧸ IsLocalRing.maximalIdeal R • ⊤)
-- Std.Data.HashSet.Raw
/-- Computes the union of the given hash sets.

This function always merges the smaller set into the larger set, so the expected runtime is
`O(min(m₁.size, m₂.size))`.
 -/
Std.HashSet.Raw.union : {α : Type u} → [BEq α] → [Hashable α] → Std.HashSet.Raw α → Std.HashSet.Raw α → Std.HashSet.Raw α
-- Std.Http.Data.Method
/-- Create a link relationship between resources.
Source: https://www.rfc-editor.org/rfc/rfc2068#section-19.6.1.2
 -/
Std.Http.Method.link : Std.Http.Method
-- Lean.Meta.Tactic.Simp.Types
_private.Lean.Meta.Tactic.Simp.Types.0.Lean.Meta.Simp.MethodsRefPointed : NonemptyType
-- Mathlib.Algebra.Group.Basic
add_sub_add_right_eq_sub : ∀ {G : Type u_3} [inst : AddGroup G] (a b c : G), a + c - (b + c) = a - b
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
DihedralGroup.instIsKleinFourOfNatNat : IsKleinFour (DihedralGroup 2)
-- Mathlib.Computability.Primrec.Basic
Primrec.option_some_iff : ∀ {α : Type u_1} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable σ] {f : α → σ},
  (Primrec fun a => some (f a)) ↔ Primrec f
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.Functor.CommShift.id_commShiftIso_inv_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u_4} [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (x : A) (X : C),
  (CategoryTheory.Functor.commShiftIso (CategoryTheory.Functor.id C) x).inv.app X =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.shiftFunctor C x).obj X)
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsFundamentalDomain.measure_set_eq : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s t : Set α}
  {μ : MeasureTheory.Measure α} [MeasurableConstSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G],
  MeasureTheory.IsFundamentalDomain G s μ →
    MeasureTheory.IsFundamentalDomain G t μ →
      ∀ {A : Set α}, MeasurableSet A → (∀ (g : G), (fun x => g • x) ⁻¹' A = A) → μ (A ∩ s) = μ (A ∩ t)
-- Mathlib.Order.Filter.Ultrafilter.Basic
Filter.atBot_eq_pure_of_isBot : ∀ {α : Type u} [inst : PartialOrder α] {x : α}, IsBot x → Filter.atBot = pure x
-- Mathlib.Data.List.DropRight
List.rdropWhile_last_not : ∀ {α : Type u_1} (p : α → Bool) (l : List α) (hl : List.rdropWhile p l ≠ []),
  ¬p ((List.rdropWhile p l).getLast hl) = true
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.lift_f_fst_v_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ}
  (α : CochainComplex.HomComplex.Cocycle K F 1) (β : CochainComplex.HomComplex.Cochain K G 0)
  (eq : CochainComplex.HomComplex.δ 0 1 β + (↑α).comp (CochainComplex.HomComplex.Cochain.ofHom φ) ⋯ = 0) (p q : ℤ)
  (hpq : p + 1 = q) {Z : C} (h : F.X q ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.lift φ α β eq).f p)
      (CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCone.fst φ)).v p q hpq) h) =
    CategoryTheory.CategoryStruct.comp ((↑α).v p q hpq) h
-- Mathlib.Order.Filter.CountableSeparatingOn
Filter.exists_subsingleton_mem_of_forall_separating : ∀ {α : Type u_1} {l : Filter α} [CountableInterFilter l] (p : Set α → Prop) [HasCountableSeparatingOn α p Set.univ],
  (∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l) → ∃ s, s.Subsingleton ∧ s ∈ l
-- Init.Data.SInt.Lemmas
Int16.ofInt_int8ToInt : ∀ (x : Int8), Int16.ofInt x.toInt = x.toInt16
-- Mathlib.Order.UpperLower.Principal
UpperSet.mem_Ici_iff : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, b ∈ UpperSet.Ici a ↔ a ≤ b
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
/-- Constructor for `SmallShiftedHom`.  -/
CategoryTheory.Localization.SmallShiftedHom.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (W : CategoryTheory.MorphismProperty C) →
      {M : Type w'} →
        [inst_1 : AddMonoid M] →
          [inst_2 : CategoryTheory.HasShift C M] →
            {X Y : C} →
              {m : M} →
                [inst_3 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y] →
                  CategoryTheory.ShiftedHom X Y m → CategoryTheory.Localization.SmallShiftedHom W X Y m
-- Mathlib.RingTheory.TensorProduct.Quotient
/-- The tensor product of an `S`-algebra `A` over `R` with the quotient of `T` by an ideal `I`
is isomorphic (as an `S`-algebra) to the quotient of `A ⊗[R] T` by the extended ideal.  -/
Algebra.TensorProduct.tensorQuotientEquiv : {R : Type u_1} →
  (S : Type u_2) →
    (T : Type u_3) →
      (A : Type u_4) →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              [inst_3 : CommRing T] →
                [inst_4 : Algebra R T] →
                  [inst_5 : CommRing A] →
                    [inst_6 : Algebra R A] →
                      [inst_7 : Algebra S A] →
                        [inst_8 : IsScalarTower R S A] →
                          (I : Ideal T) →
                            TensorProduct R A (T ⧸ I) ≃ₐ[S]
                              TensorProduct R A T ⧸ Ideal.map Algebra.TensorProduct.includeRight I
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryLE.congr_simp : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k k_1 : α) (e_k : k = k_1)
  (t t_1 : Std.DTreeMap.Internal.Impl α fun x => β) (e_t : t = t_1) (ho : t.Ordered)
  (he : ∃ a ∈ t, (compare a k).isLE = true),
  Std.DTreeMap.Internal.Impl.Const.getEntryLE k t ho he = Std.DTreeMap.Internal.Impl.Const.getEntryLE k_1 t_1 ⋯ ⋯
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- Cached `getDecLevel type`  -/
Lean.Meta.Grind.Arith.Linear.NatStruct.u : Lean.Meta.Grind.Arith.Linear.NatStruct → Lean.Level
-- Qq.Macro
Qq.Impl.withUnquotedLCtx : {m : Type → Type u_1} →
  {α : Type} → [MonadControlT Lean.MetaM m] → [Monad m] → [MonadLiftT Qq.Impl.QuoteM m] → m α → m α
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Hom.range_eq_top : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] {f : L.Hom M N},
  f.range = ⊤ ↔ Function.Surjective ⇑f
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Multiset.stronglyMeasurable_sum : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] [ContinuousAdd M]
  {m : MeasurableSpace α} (l : Multiset (α → M)),
  (∀ f ∈ l, MeasureTheory.StronglyMeasurable f) → MeasureTheory.StronglyMeasurable l.sum
-- Mathlib.MeasureTheory.Measure.Haar.Unique
/-- **Uniqueness of Haar measures**:
Given two additive Haar measures, they coincide in the following sense: they give the same value to
open sets, up to the multiplicative constant `addHaarScalarFactor μ' μ`.  -/
MeasureTheory.Measure.measure_isAddHaarMeasure_eq_smul_of_isOpen : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [LocallyCompactSpace G] (μ' μ : MeasureTheory.Measure G)
  [inst_6 : μ.IsAddHaarMeasure] [inst_7 : μ'.IsAddHaarMeasure] {s : Set G},
  IsOpen s → μ' s = μ'.addHaarScalarFactor μ • μ s
-- Mathlib.AlgebraicGeometry.Sites.Pretopology
AlgebraicGeometry.Scheme.Cover.mem_pretopology : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.IsStableUnderBaseChange]
  [inst_1 : P.IsMultiplicative] {X : AlgebraicGeometry.Scheme}
  {𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X},
  CategoryTheory.Presieve.ofArrows 𝒰.X 𝒰.f ∈ (AlgebraicGeometry.Scheme.pretopology P).coverings X
-- Lean.Meta.Basic
/-- A mapping `(s, t) ↦ isDefEq s t`.
TODO: consider more efficient representations (e.g., a proper set) and caching policies (e.g., imperfect cache).
We should also investigate the impact on memory consumption.
 -/
Lean.Meta.DefEqCache : Type
-- Mathlib.CategoryTheory.Abelian.CommSq
CategoryTheory.IsPullback.exact_shortComplex' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X₁ X₂ X₃ X₄ : C}
  {t : X₁ ⟶ X₂} {l : X₁ ⟶ X₃} {r : X₂ ⟶ X₄} {b : X₃ ⟶ X₄} (h : CategoryTheory.IsPullback t l r b), ⋯.shortComplex'.Exact
-- Mathlib.CategoryTheory.IsConnected
/-- `J` is connected if: given any function `F : J → α` which is constant for any
`j₁, j₂` for which there is a morphism `j₁ ⟶ j₂`, then `F` is constant.
This can be thought of as a local-to-global property.

The converse of `constant_of_preserves_morphisms`.
 -/
CategoryTheory.IsConnected.of_constant_of_preserves_morphisms : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] [Nonempty J],
  (∀ {α : Type u₁} (F : J → α), (∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂) → ∀ (j j' : J), F j = F j') →
    CategoryTheory.IsConnected J
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Sinc
Real.integrable_sinc : ∀ {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure μ], MeasureTheory.Integrable Real.sinc μ
-- Mathlib.AlgebraicGeometry.Restrict
/-- The restriction of a scheme to an open subset.  -/
AlgebraicGeometry.Scheme.Opens.ι : {X : AlgebraicGeometry.Scheme} → (U : X.Opens) → ↑U ⟶ X
-- Mathlib.AlgebraicGeometry.Morphisms.Immersion
AlgebraicGeometry.IsImmersion.isLocallyClosed_range : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : AlgebraicGeometry.IsImmersion f], IsLocallyClosed (Set.range ⇑f)
-- Mathlib.NumberTheory.AlmostPrime
Nat.isAlmostPrime_zero_iff : ∀ {n : ℕ}, Nat.IsAlmostPrime 0 n ↔ n = 1
-- Mathlib.Topology.UniformSpace.Completion
CauchyFilter.mem_uniformity' : ∀ {α : Type u} [inst : UniformSpace α] {s : Set (CauchyFilter α × CauchyFilter α)},
  s ∈ uniformity (CauchyFilter α) ↔ ∃ t ∈ uniformity α, ∀ (f g : CauchyFilter α), t ∈ ↑f ×ˢ ↑g → (f, g) ∈ s
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.lift₂Expand.eq_1 : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_3}
  [inst_2 : MulAction R X] {C : Sort u_2} (P : X → ↥S → X → ↥S → C)
  (hP :
    ∀ (r₁ : X) (t₁ : R) (s₁ : ↥S) (ht₁ : t₁ * ↑s₁ ∈ S) (r₂ : X) (t₂ : R) (s₂ : ↥S) (ht₂ : t₂ * ↑s₂ ∈ S),
      P r₁ s₁ r₂ s₂ = P (t₁ • r₁) ⟨t₁ * ↑s₁, ht₁⟩ (t₂ • r₂) ⟨t₂ * ↑s₂, ht₂⟩),
  OreLocalization.lift₂Expand P hP = OreLocalization.liftExpand (fun r₁ s₁ => OreLocalization.liftExpand (P r₁ s₁) ⋯) ⋯
-- Init.Data.Int.Order
Int.sub_lt_sub_left : ∀ {a b : ℤ}, a < b → ∀ (c : ℤ), c - b < c - a
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.exact_map_iff_of_faithful : ∀ {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.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (S : CategoryTheory.ShortComplex C) [S.HasHomology]
  (F : CategoryTheory.Functor C D) [inst_5 : F.PreservesZeroMorphisms] [F.PreservesLeftHomologyOf S]
  [F.PreservesRightHomologyOf S] [F.Faithful], (S.map F).Exact ↔ S.Exact
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
DifferentiableAt.comp_mdifferentiableWithinAt : ∀ {𝕜 : 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] {F : Type u_8} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {F' : Type u_11} [inst_8 : NormedAddCommGroup F'] [inst_9 : NormedSpace 𝕜 F'] {g : F → F'}
  {f : M → F} {s : Set M} {x : M}, DifferentiableAt 𝕜 g (f x) → MDiffAt[s] f x → MDiffAt[s] (g ∘ f) x