mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousMultilinearMap.alternatization_apply_toAlternatingMap : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommGroup N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N] [inst_7 : IsTopologicalAddGroup N] [inst_8 : Fintype ι] [inst_9 : DecidableEq ι]
  (f : ContinuousMultilinearMap R (fun x => M) N),
  (ContinuousMultilinearMap.alternatization f).toAlternatingMap = MultilinearMap.alternatization f.toMultilinearMap
-- Mathlib.Topology.Algebra.Group.Basic
topologicalGroup_induced : ∀ {G : Type w} {H : Type x} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] {F : Type u_1}
  [inst_3 : Group H] [inst_4 : FunLike F H G] [MonoidHomClass F H G] (f : F), IsTopologicalGroup H
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.coe_one : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), ↑1 = 1
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.mulSingle_inj : ∀ {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [inst : (i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i)
  [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → One (G i)] [inst_3 : ∀ (i : ι), OneMemClass (S i) (G i)] (i : ι)
  {x y : G i}, RestrictedProduct.mulSingle A i x = RestrictedProduct.mulSingle A i y ↔ x = y
-- Init.Prelude
instSubNat : Sub ℕ
-- Mathlib.Data.List.TakeWhile
List.find?_not_eq_head_dropWhile : ∀ {α : Type u_1} {p : α → Bool} {l : List α} (h : ∃ x ∈ l, ¬p x = true),
  List.find? (fun x => !p x) l = some ((List.dropWhile p l).head ⋯)
-- Lean.Parser.Term
Lean.Parser.Term.explicitUnivSuffix.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Analysis.BoxIntegral.Partition.Split
/-- If `x ∉ (I.lower i, I.upper i)`, then the hyperplane `{y | y i = x}` does not split `I`.  -/
BoxIntegral.Prepartition.split_of_notMem_Ioo : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {i : ι} {x : ℝ},
  x ∉ Set.Ioo (I.lower i) (I.upper i) → BoxIntegral.Prepartition.split I i x = ⊤
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.ofCoeff_inj : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {x y : ℕ →₀ M},
  { coeff := x } = { coeff := y } ↔ x = y
-- Mathlib.Data.Finset.Sort
Finset.map_sort : ∀ {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : Finset α) (r : α → α → Prop) [inst : DecidableRel r]
  [inst_1 : IsTrans α r] [inst_2 : Std.Antisymm r] [inst_3 : Std.Total r] (r' : β → β → Prop) [inst_4 : DecidableRel r']
  [inst_5 : IsTrans β r'] [inst_6 : Std.Antisymm r'] [inst_7 : Std.Total r'],
  (∀ a ∈ s, ∀ b ∈ s, r a b ↔ r' (f a) (f b)) → List.map (⇑f) (s.sort r) = (Finset.map f s).sort r'
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- Given an affinely independent family of points, an affine combination (with sum of weights 1)
equals the line map of two affine combination points if and only if its weights are given pointwise
by the line map of the corresponding weights.  -/
AffineIndependent.affineCombination_eq_lineMap_iff_weight_lineMap : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} {p : ι → P},
  AffineIndependent k p →
    ∀ {w w₁ w₂ : ι → k} {s : Finset ι},
      ∑ i ∈ s, w i = 1 →
        ∑ i ∈ s, w₁ i = 1 →
          ∑ i ∈ s, w₂ i = 1 →
            ∀ (c : k),
              (Finset.affineCombination k s p) w =
                  (AffineMap.lineMap ((Finset.affineCombination k s p) w₁) ((Finset.affineCombination k s p) w₂)) c ↔
                ∀ i ∈ s, w i = (AffineMap.lineMap (w₁ i) (w₂ i)) c
-- Aesop.Rule.Name
Aesop.instHashableDisplayRuleName : Hashable Aesop.DisplayRuleName
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
/-- `extremalNumber (card V) H` is at most `x` if and only if every `H`-free simple graph `G` has
at most `x` edges.  -/
SimpleGraph.extremalNumber_le_iff_of_nonneg : ∀ {V : Type u_1} {W : Type u_2} [inst : Fintype V] {R : Type u_3} [inst_1 : Semiring R] [inst_2 : LinearOrder R]
  [FloorSemiring R] (H : SimpleGraph W) {m : R},
  0 ≤ m →
    (↑(SimpleGraph.extremalNumber (Fintype.card V) H) ≤ m ↔
      ∀ ⦃G : SimpleGraph V⦄ [inst_4 : DecidableRel G.Adj], H.Free G → ↑G.edgeFinset.card ≤ m)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVBinOp.xor.sizeOf_spec : sizeOf Std.Tactic.BVDecide.BVBinOp.xor = 1
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.univ_eq_empty_iff : ∀ {α : Type u_1} [inst : Fintype α], Finset.univ = ∅ ↔ IsEmpty α
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.ofFaithful.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cocone F} {D : Type u₄}
  [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (G : CategoryTheory.Functor C D) [inst_3 : G.Faithful]
  (ht : CategoryTheory.Limits.IsColimit (G.mapCocone t)) (lift : (s : CategoryTheory.Limits.Cocone F) → t.pt ⟶ s.pt)
  (h : ∀ (s : CategoryTheory.Limits.Cocone F), G.map (lift s) = ht.desc (G.mapCocone s)),
  CategoryTheory.Limits.IsColimit.ofFaithful G ht lift h = { desc := lift, fac := ⋯, uniq := ⋯ }
-- Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence
_private.Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence.0.AlgebraicTopology.DoldKan.homotopyPToId.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((q : ℕ) → motive q.succ) → motive x
-- Mathlib.Order.Atoms
/-- A lattice is coatomistic iff every element is an `sInf` of a set of coatoms.  -/
IsCoatomistic : (α : Type u_2) → [inst : PartialOrder α] → [OrderTop α] → Prop
-- Mathlib.Data.Num.Lemmas
_private.Mathlib.Data.Num.Lemmas.0.PosNum.cmp.match_1.splitter : (motive : PosNum → PosNum → Sort u_1) →
  (x x_1 : PosNum) →
    (Unit → motive PosNum.one PosNum.one) →
      ((x : PosNum) → (x = PosNum.one → False) → motive x PosNum.one) →
        ((x : PosNum) → (x = PosNum.one → False) → motive PosNum.one x) →
          ((a b : PosNum) → motive a.bit0 b.bit0) →
            ((a b : PosNum) → motive a.bit0 b.bit1) →
              ((a b : PosNum) → motive a.bit1 b.bit0) → ((a b : PosNum) → motive a.bit1 b.bit1) → motive x x_1
-- Mathlib.Computability.Language
Language.mem_kstar_iff_exists_nonempty : ∀ {α : Type u_1} {l : Language α} {x : List α}, x ∈ KStar.kstar l ↔ ∃ S, x = S.flatten ∧ ∀ y ∈ S, y ∈ l ∧ y ≠ []
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.star_subset_adjoin : ∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A] (s : Set A), star s ⊆ ↑(NonUnitalStarAlgebra.adjoin R s)
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.coe_refl : ∀ {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁], ⇑(ContinuousAffineEquiv.refl k P₁) = id
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- In a preadditive category, any finite bicone which is a colimit cocone is in fact a bilimit
bicone.  -/
CategoryTheory.Limits.isBilimitOfIsColimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {J : Type u_1} →
        [Fintype J] →
          {f : J → C} → (t : CategoryTheory.Limits.Bicone f) → CategoryTheory.Limits.IsColimit t.toCocone → t.IsBilimit
-- Mathlib.Algebra.Group.Idempotent
IsIdempotentElem.pow_eq : ∀ {M : Type u_1} [inst : Monoid M] {a : M}, IsIdempotentElem a → ∀ {n : ℕ}, n ≠ 0 → a ^ n = a
-- Mathlib.RingTheory.PowerBasis
PowerBasis.lift_gen : ∀ {S : Type u_2} [inst : Ring S] {A : Type u_4} [inst_1 : CommRing A] [inst_2 : Algebra A S] {S' : Type u_7}
  [inst_3 : Ring S'] [inst_4 : Algebra A S'] (pb : PowerBasis A S) (y : S')
  (hy : (Polynomial.aeval y) (minpoly A pb.gen) = 0), (pb.lift y hy) pb.gen = y
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coconeLeftOpOfCone.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J Cᵒᵖ} (c : CategoryTheory.Limits.Cone F),
  CategoryTheory.Limits.coconeLeftOpOfCone c = { pt := Opposite.unop c.pt, ι := CategoryTheory.NatTrans.leftOp c.π }
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey?_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {km : α},
  t.minKey? = some km → km ∈ t
-- Mathlib.Logic.Equiv.Defs
Equiv.funUnique_apply : ∀ (α : Sort u) (β : Sort u_1) [inst : Unique α], ⇑(Equiv.funUnique α β) = fun f => f default
-- Std.Do.WP.SimpLemmas
Std.Do.WP.orElse_EStateM : ∀ {ε σ δ α : Type u_1} {x : EStateM ε σ α} {h : Unit → EStateM ε σ α}
  {Q : Std.Do.PostCond α (Std.Do.PostShape.except ε (Std.Do.PostShape.arg σ Std.Do.PostShape.pure))}
  [inst : EStateM.Backtrackable δ σ],
  (Std.Do.wp (OrElse.orElse x h)).apply Q = fun s =>
    (Std.Do.wp x).apply
      (Q.1, fun x s' => (Std.Do.wp (h ())).apply Q (EStateM.Backtrackable.restore s' (EStateM.Backtrackable.save s)),
        Q.2.2)
      s
-- Init.Grind.AC
Lean.Grind.AC.Seq.brecOn.go : {motive : Lean.Grind.AC.Seq → Sort u} →
  (t : Lean.Grind.AC.Seq) →
    ((t : Lean.Grind.AC.Seq) → Lean.Grind.AC.Seq.below t → motive t) → motive t ×' Lean.Grind.AC.Seq.below t
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.vanishingIdeal_anti_mono : ∀ {R : Type u} [inst : CommSemiring R] {s t : Set (PrimeSpectrum R)},
  s ⊆ t → PrimeSpectrum.vanishingIdeal t ≤ PrimeSpectrum.vanishingIdeal s
-- Mathlib.LinearAlgebra.AffineSpace.Independent
exists_nontrivial_relation_sum_zero_of_not_affine_ind : ∀ {k : Type u_1} {V : Type u_2} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] {t : Finset V},
  ¬AffineIndependent k Subtype.val → ∃ f, ∑ e ∈ t, f e • e = 0 ∧ ∑ e ∈ t, f e = 0 ∧ ∃ x ∈ t, f x ≠ 0
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
_private.Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite.0.SimpleGraph.IsPathGraph3Compl.pathGraph3ComplEmbedding.match_1.eq_2 : ∀ (motive : Fin 3 → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : Unit → motive 2),
  (match 1 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | 2 => h_3 ()) =
    h_2 ()
-- Mathlib.ModelTheory.Syntax
_private.Mathlib.ModelTheory.Syntax.0.FirstOrder.Language.BoundedFormula.castLE.match_1.eq_2 : ∀ {L : FirstOrder.Language} {α : Type u_3} (motive : (x x_1 : ℕ) → x ≤ x_1 → L.BoundedFormula α x → Sort u_4)
  (_m _n : ℕ) (h : _m ≤ _n) (t₁ t₂ : L.Term (α ⊕ Fin _m))
  (h_1 : (_m _n : ℕ) → (_h : _m ≤ _n) → motive _m _n _h FirstOrder.Language.BoundedFormula.falsum)
  (h_2 :
    (_m _n : ℕ) →
      (h : _m ≤ _n) → (t₁ t₂ : L.Term (α ⊕ Fin _m)) → motive _m _n h (FirstOrder.Language.BoundedFormula.equal t₁ t₂))
  (h_3 :
    (_m _n : ℕ) →
      (h : _m ≤ _n) →
        (l : ℕ) →
          (R : L.Relations l) →
            (ts : Fin l → L.Term (α ⊕ Fin _m)) → motive _m _n h (FirstOrder.Language.BoundedFormula.rel R ts))
  (h_4 : (_m _n : ℕ) → (h : _m ≤ _n) → (f₁ f₂ : L.BoundedFormula α _m) → motive _m _n h (f₁.imp f₂))
  (h_5 : (_m _n : ℕ) → (h : _m ≤ _n) → (f : L.BoundedFormula α (_m + 1)) → motive _m _n h f.all),
  (match _m, _n, h, FirstOrder.Language.BoundedFormula.equal t₁ t₂ with
    | _m, _n, _h, FirstOrder.Language.BoundedFormula.falsum => h_1 _m _n _h
    | _m, _n, h, FirstOrder.Language.BoundedFormula.equal t₁ t₂ => h_2 _m _n h t₁ t₂
    | _m, _n, h, FirstOrder.Language.BoundedFormula.rel R ts => h_3 _m _n h l R ts
    | _m, _n, h, f₁.imp f₂ => h_4 _m _n h f₁ f₂
    | _m, _n, h, f.all => h_5 _m _n h f) =
    h_2 _m _n h t₁ t₂
-- Init.Data.SInt.Lemmas
Int16.toInt_bmod_size : ∀ (a : Int16), a.toInt.bmod Int16.size = a.toInt
-- Lean.Elab.Quotation
Lean.Elab.Term.Quotation.ArrayStxBuilder.append : Lean.Elab.Term.Quotation.ArrayStxBuilder →
  Lean.Syntax → optParam Lean.Name `Array.append → Lean.Elab.Term.Quotation.ArrayStxBuilder
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
AddCircle.scaled_exp_map_periodic : ∀ {T : ℝ}, Function.Periodic (fun x => Circle.exp (2 * Real.pi / T * x)) T
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs
_private.Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs.0.BirdDet.birdDet.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (A : Array R), BirdDet.birdDet 0 A = 1
-- Mathlib.CategoryTheory.Abelian.Pseudoelements
/-- If two elements are pseudo-equal, then their composition with a morphism is, too.  -/
CategoryTheory.Abelian.Pseudoelement.pseudoApply_aux : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q)
  (a b : CategoryTheory.Over P), a ≈ b → CategoryTheory.Abelian.app f a ≈ CategoryTheory.Abelian.app f b
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.mul_counit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M : C) [inst_3 : CategoryTheory.BimonObj M],
  CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul CategoryTheory.ComonObj.counit =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.ComonObj.counit CategoryTheory.ComonObj.counit)
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ D` reflects colimits of `K.op : Jᵒᵖ ⥤ Cᵒᵖ`, then `F.rightOp : C ⥤ Dᵒᵖ` reflects
limits of `K : J ⥤ C`.  -/
CategoryTheory.Limits.reflectsLimit_rightOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C)
  (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.ReflectsColimit K.op F],
  CategoryTheory.Limits.ReflectsLimit K F.rightOp
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Finset.tsum_subtype : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] (s : Finset β) (f : β → α),
  ∑' (x : ↥s), f ↑x = ∑ x ∈ s, f x
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.mapMon_obj_mon_one : ∀ {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) [inst_4 : F.LaxMonoidal] (A : CategoryTheory.Mon C),
  CategoryTheory.MonObj.one =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (F.map CategoryTheory.MonObj.one)
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
/-- The indexed infimum of two functions are comparable if the functions are pointwise comparable  -/
ciInf_mono : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] {f g : ι → α},
  BddBelow (Set.range f) → (∀ (x : ι), f x ≤ g x) → iInf f ≤ iInf g
-- Init.Data.List.Zip
List.map_zipWith : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → β} {g : γ → δ → α} {l : List γ} {l' : List δ},
  List.map f (List.zipWith g l l') = List.zipWith (fun x y => f (g x y)) l l'
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- The measurable superset `toMeasurable μ t` of `t` (which has the same measure as `t`)
satisfies, for any measurable set `s`, the equality `μ (toMeasurable μ t ∩ s) = μ (u ∩ s)`.
Here, we require that the measure of `t` is finite. The conclusion holds without this assumption
when the measure is s-finite (for example when it is σ-finite),
see `measure_toMeasurable_inter_of_sFinite`.  -/
MeasureTheory.Measure.measure_toMeasurable_inter : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasurableSet s → μ t ≠ ⊤ → μ (MeasureTheory.toMeasurable μ t ∩ s) = μ (t ∩ s)
-- Mathlib.CategoryTheory.Sites.LeftExact
/-- `plusPlus` is isomorphic to `sheafify`.  -/
CategoryTheory.plusPlusIsoSheafify : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (D : Type w) →
        [inst_1 : CategoryTheory.Category.{t, w} D] →
          [inst_2 :
              ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X),
                CategoryTheory.Limits.HasMultiequalizer (S.index P)] →
            [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] →
              {FD : D → D → Type u_1} →
                {CD : D → Type t} →
                  [inst_4 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] →
                    [inst_5 : CategoryTheory.ConcreteCategory D FD] →
                      [inst_6 :
                          ∀ (X : C),
                            CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] →
                        [inst_7 : (CategoryTheory.forget D).ReflectsIsomorphisms] →
                          [inst_8 :
                              ∀ {X : C} (S : J.Cover X),
                                CategoryTheory.Limits.PreservesLimitsOfShape
                                  (CategoryTheory.Limits.WalkingMulticospan S.shape) (CategoryTheory.forget D)] →
                            (P : CategoryTheory.Functor Cᵒᵖ D) → J.sheafify P ≅ CategoryTheory.sheafify J P
-- Mathlib.Analysis.Complex.UpperHalfPlane.Topology
UpperHalfPlane.continuous_im : Continuous UpperHalfPlane.im
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.coe_inf : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (L M : BooleanSubalgebra α), ↑(L ⊓ M) = ↑L ∩ ↑M
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- **Alias** of `Left.neg_of_mul_neg_right`. -/
neg_of_mul_neg_right : ∀ {α : Type u_1} [inst : MulZeroClass α] {a b : α} [inst_1 : LinearOrder α] [PosMulMono α], a * b < 0 → 0 ≤ a → b < 0
-- Mathlib.Data.EReal.Operations
EReal.toReal_neg_eq : ∀ {a : EReal}, (-a).toReal = -a.toReal
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
IsZLattice.congr_simp : ∀ (K : Type u_1) [inst : NormedField K] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace K E]
  (L L_1 : Submodule ℤ E) (e_L : L = L_1) [inst_3 : DiscreteTopology ↥L], IsZLattice K L = IsZLattice K L_1
-- Std.Http.Data.Body.Stream
Std.Http.Body.instCoeAsyncResponseStreamContextAsyncAny : Coe (Std.Async.Async (Std.Http.Response Std.Http.Body.Stream))
  (Std.Async.ContextAsync (Std.Http.Response Std.Http.Body.Any))
-- Mathlib.Data.Fintype.OfMap
/-- Construct a proof of `Fintype α` from a universal multiset  -/
Fintype.ofMultiset : {α : Type u_1} → [DecidableEq α] → (s : Multiset α) → (∀ (x : α), x ∈ s) → Fintype α
-- Mathlib.Tactic.Sat.FromLRAT
/-- Parse a list of natural numbers terminated by 0  -/
Mathlib.Tactic.Sat.Parser.parseNats : optParam (Array ℕ) #[] → Std.Internal.Parsec.String.Parser (Array ℕ)
-- Mathlib.Order.SuccPred.Tree
RootedTree.mk : (α : Type u_2) →
  [semilatticeInf : SemilatticeInf α] →
    [orderBot : OrderBot α] → [predOrder : PredOrder α] → [isPredArchimedean : IsPredArchimedean α] → RootedTree
-- Mathlib.Topology.Semicontinuity.Basic
/-- **Alias** of the forward direction of `lowerSemicontinuousOn_iff_le_liminf`. -/
LowerSemicontinuousOn.le_liminf : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {γ : Type u_4} [inst_1 : CompleteLinearOrder γ] {f : α → γ},
  LowerSemicontinuousOn f s → ∀ x ∈ s, f x ≤ Filter.liminf f (nhdsWithin x s)
-- Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
/-- The one-point compactification of a division ring `K` is equivalent to
the projectivization `ℙ K (Fin 2 → K)`.  -/
OnePoint.equivProjectivization : (K : Type u_1) → [inst : DivisionRing K] → [DecidableEq K] → OnePoint K ≃ Projectivization K (Fin 2 → K)
-- Mathlib.Data.List.Cycle
_private.Mathlib.Data.List.Cycle.0.List.nextOr.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → α → α → Sort u_2) (x default : α) (h_1 : (x default : α) → motive [] x default)
  (h_2 : (head x default : α) → motive [head] x default)
  (h_3 : (y z : α) → (xs : List α) → (x default : α) → motive (y :: z :: xs) x default),
  (match [], x, default with
    | [], x, default => h_1 x default
    | [head], x, default => h_2 head x default
    | y :: z :: xs, x, default => h_3 y z xs x default) =
    h_1 x default
-- Mathlib.Algebra.Ring.Periodic
/-- A periodic function `f : R → X` on a semiring (or, more generally, `AddZeroClass`)
of non-zero period is not injective.  -/
Function.Periodic.not_injective : ∀ {R : Type u_4} {X : Type u_5} [inst : AddZeroClass R] {f : R → X} {c : R},
  Function.Periodic f c → c ≠ 0 → ¬Function.Injective f
-- Mathlib.Geometry.Manifold.IsManifold.Basic
IsManifold.instLEInftyOfNatWithTopENat : ∀ (n : ℕ) [inst : n.AtLeastTwo], ENat.LEInfty (OfNat.ofNat n)
-- Lean.Meta.Tactic.Induction
Lean.Meta.AltVarNames.mk.injEq : ∀ (explicit : Bool) (varNames : List Lean.Name) (explicit_1 : Bool) (varNames_1 : List Lean.Name),
  ({ explicit := explicit, varNames := varNames } = { explicit := explicit_1, varNames := varNames_1 }) =
    (explicit = explicit_1 ∧ varNames = varNames_1)
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.centerEquivRootsOfUnity_invFun.congr_simp : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  [inst_3 : Module.Free R V] [inst_4 : Module.Finite R V] (r r_1 : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)),
  r = r_1 → SpecialLinearGroup.centerEquivRootsOfUnity_invFun r = SpecialLinearGroup.centerEquivRootsOfUnity_invFun r_1
-- Mathlib.Algebra.Homology.Monoidal
/-- The left unitor for the tensor product of homological complexes.  -/
HomologicalComplex.leftUnitor : {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] →
          [inst_4 : (CategoryTheory.MonoidalCategory.curriedTensor C).Additive] →
            [inst_5 : ∀ (X₁ : C), ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁).Additive] →
              {I : Type u_2} →
                [inst_6 : AddMonoid I] →
                  {c : ComplexShape I} →
                    [inst_7 : c.TensorSigns] →
                      (K : HomologicalComplex C c) →
                        [inst_8 : DecidableEq I] →
                          [inst_9 :
                              ∀ (X₂ : C),
                                CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C)
                                  ((CategoryTheory.MonoidalCategory.curriedTensor C).flip.obj X₂)] →
                            (HomologicalComplex.tensorUnit C c).tensorObj K ≅ K
-- Mathlib.Topology.Constructions
/-- **Alias** of `Pi.continuous_domRestrict₂_apply`. -/
Pi.continuous_restrict₂_apply : ∀ {X : Type u} {Z : Type u_1} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Z] {s t : Set X} (hst : s ⊆ t)
  {f : ↑t → Z}, Continuous f → Continuous (Set.domRestrict₂ hst f)
-- Mathlib.Analysis.InnerProductSpace.Dual
InnerProductSpace.toDual_symm_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] {x : E} {y : StrongDual 𝕜 E}, inner 𝕜 ((InnerProductSpace.toDual 𝕜 E).symm y) x = y x
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.whiskerLeft_comp : ∀ {B : Type u} [self : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) {g h i : b ⟶ c} (η : g ⟶ h) (θ : h ⟶ i),
  CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.CategoryStruct.comp η θ) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f η)
      (CategoryTheory.Bicategory.whiskerLeft f θ)
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.BackwardPattern.skipSuffix?_char_eq_skipSuffix?_beq : ∀ {c : Char} {s : String.Slice},
  String.Slice.Pattern.BackwardPattern.skipSuffix? c s =
    String.Slice.Pattern.BackwardPattern.skipSuffix? (fun x => x == c) s