mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceHomFullSubcategoryCofibrantObjectsIBifibrantResolutionObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  (X : HomotopicalAlgebra.CofibrantObject C), HomotopicalAlgebra.WeakEquivalence X.iBifibrantResolutionObj.hom
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.upcrossingsBefore_zero : ∀ {Ω : Type u_1} {a b : ℝ} {f : ℕ → Ω → ℝ} {ω : Ω}, MeasureTheory.upcrossingsBefore a b f 0 ω = 0
-- Mathlib.Algebra.Homology.Embedding.RestrictionHomology
HomologicalComplex.restrictionOpcyclesIso.congr_simp : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsRelIff] (i i_1 : ι) (e_i : i = i_1) (j : ι)
  (hi : c.prev j = i) {i' i'_1 : ι'} (e_i' : i' = i'_1) {j' : ι'} (hi' : e.f i = i') (hj' : e.f j = j')
  (hi'' : c'.prev j' = i') [inst_3 : K.HasHomology j'] [inst_4 : (K.restriction e).HasHomology j],
  K.restrictionOpcyclesIso e i j hi hi' hj' hi'' = K.restrictionOpcyclesIso e i_1 j ⋯ ⋯ hj' ⋯
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.testAgainstNN.eq_1 : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω)
  (f : BoundedContinuousFunction Ω NNReal), μ.testAgainstNN f = (∫⁻ (ω : Ω), ↑(f ω) ∂↑μ).toNNReal
-- Mathlib.Data.List.Defs
List.iterate.eq_2 : ∀ {α : Type u_1} (f : α → α) (a : α) (n : ℕ), List.iterate f a n.succ = a :: List.iterate f (f a) n
-- Mathlib.Analysis.Polynomial.Order
Polynomial.zero_lt_eval_of_roots_lt_of_leadingCoeff_nonneg : ∀ {P : Polynomial ℝ} {x : ℝ}, (∀ (y : ℝ), P.IsRoot y → y < x) → 0 ≤ P.leadingCoeff → 0 < Polynomial.eval x P
-- Mathlib.RingTheory.WittVector.Defs
/-- These instances are not needed for the rest of the development,
but it is interesting to establish early on that `WittVector p` is a lawful functor.  -/
WittVector.instFunctor : (p : ℕ) → Functor (WittVector p)
-- Mathlib.Topology.Category.UniformSpace
UniformSpaceCat.completionHom_val : ∀ (X : UniformSpaceCat) (x : X.carrier), (CategoryTheory.ConcreteCategory.hom X.completionHom) x = ↑x
-- Mathlib.Algebra.Group.Subgroup.Basic
AddCommGroup.normalizer_eq_top : ∀ {G : Type u_5} [inst : AddCommGroup G] (s : Set G), AddSubgroup.normalizer s = ⊤
-- Mathlib.Analysis.Normed.Group.Basic
enorm'_eq_iff_norm_eq : ∀ {E : Type u_5} {F : Type u_6} [inst : SeminormedGroup E] [inst_1 : SeminormedGroup F] {x : E} {y : F},
  ‖x‖ₑ = ‖y‖ₑ ↔ ‖x‖ = ‖y‖
-- Mathlib.Topology.Category.TopCat.Limits.Products
/-- The second projection from the product.  -/
TopCat.prodSnd : {X Y : TopCat} → TopCat.of (↑X × ↑Y) ⟶ Y
-- Mathlib.CategoryTheory.Monoidal.FunctorCategory
/-- When `C` is any category, and `D` is a braided monoidal category,
the natural pointwise monoidal structure on the functor category `C ⥤ D`
is also braided.
 -/
CategoryTheory.Monoidal.functorCategoryBraided : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.MonoidalCategory D] →
          [CategoryTheory.BraidedCategory D] → CategoryTheory.BraidedCategory (CategoryTheory.Functor C D)
-- Mathlib.Analysis.Convex.Strict
strictConvex_Ioo : ∀ {𝕜 : Type u_1} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : TopologicalSpace β]
  [inst_3 : AddCommMonoid β] [inst_4 : LinearOrder β] [IsOrderedCancelAddMonoid β] [OrderTopology β]
  [inst_7 : Module 𝕜 β] [PosSMulStrictMono 𝕜 β] (r s : β), StrictConvex 𝕜 (Set.Ioo r s)
-- Mathlib.CategoryTheory.FiberedCategory.HasFibers
/-- The induced functor from `Fib S` to the fiber of `𝒳 ⥤ 𝒮` over `S` is an equivalence.  -/
HasFibers.equiv : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} {inst : CategoryTheory.Category.{v₁, u₁} 𝒮} {inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳}
  {p : CategoryTheory.Functor 𝒳 𝒮} [self : HasFibers p] (S : 𝒮),
  (CategoryTheory.Functor.Fiber.inducedFunctor ⋯).IsEquivalence
-- Mathlib.Probability.Decision.Risk.Defs
ProbabilityTheory.minimaxRisk_of_isEmpty : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} {P : ProbabilityTheory.Kernel Θ 𝓧} [IsEmpty 𝓧],
  ProbabilityTheory.minimaxRisk ℓ P = 0
-- Init.Data.Nat.Lemmas
Nat.one_lt_pow : ∀ {n a : ℕ}, n ≠ 0 → 1 < a → 1 < a ^ n
-- Init.Data.SInt.Lemmas
Int32.toUInt32_neg : ∀ (a : Int32), (-a).toUInt32 = -a.toUInt32
-- Lean.Elab.Term.TermElabM
/-- The binders syntax for the declaration, used for docstring elaboration.  -/
Lean.Elab.Term.LetRecToLift.binders : Lean.Elab.Term.LetRecToLift → Lean.Syntax
-- Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap
ContinuousLinearMap.instBorelSpace : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_4} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F],
  BorelSpace (E →L[𝕜] F)
-- Init.Data.String.Lemmas.Splits
String.Pos.splits_empty_right_iff : ∀ {s : String} {p : s.Pos} {t : String}, p.Splits t "" ↔ p = s.endPos ∧ t = s
-- Mathlib.Topology.Compactness.CompactlyCoherentSpace
/-- The compact sets of a topological space and its compact coherentification agree.  -/
CompactCoherentification.isCompact_image_mk_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {K : Set X},
  IsCompact (⇑(CompactCoherentification.mk X) '' K) ↔ IsCompact K
-- Init.Data.BitVec.Lemmas
BitVec.shiftLeft_ushiftRight : ∀ {w : ℕ} {x : BitVec w} {n : ℕ}, x >>> n <<< n = x &&& BitVec.allOnes w <<< n
-- Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence
/-- Close the goal of the form `η.hom = θ.hom`, where `η` and `θ` are 2-isomorphisms made up only of
associators, unitors, and identities.
```lean
example {B : Type} [Bicategory B] {a : B} :
  (λ_ (𝟙 a)).hom = (ρ_ (𝟙 a)).hom := by
  bicategory_coherence
```
 -/
Mathlib.Tactic.Bicategory.tacticBicategory_coherence : Lean.ParserDescr
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.ofList_map : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (xs : List α),
  FreeMonoid.ofList (List.map f xs) = (FreeMonoid.map f) (FreeMonoid.ofList xs)
-- Mathlib.Logic.Small.Basic
small_sum : ∀ {α : Type u_1} {β : Type u_2} [Small.{w, u_1} α] [Small.{w, u_2} β], Small.{w, max u_2 u_1} (α ⊕ β)
-- Std.Http.Data.Method
Std.Http.Method.head.sizeOf_spec : sizeOf Std.Http.Method.head = 1
-- Mathlib.Geometry.Euclidean.NinePointCircle
Affine.Simplex.faceOppositeCentroid_mem_ninePointCircle : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)),
  s.faceOppositeCentroid i ∈ s.ninePointCircle
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.instInhabited : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Field α] →
      [inst_1 : LinearOrder α] →
        [inst_2 : IsStrictOrderedRing α] →
          [inst_3 : Ring β] → {abv : β → α} → [IsAbsoluteValue abv] → Inhabited (CauSeq β abv)
-- Mathlib.Topology.EMetricSpace.Defs
/-- The ambient topology on `α` matches the `edist` topology on eballs.  -/
WeakPseudoEMetricSpace.topology_eq_on_restrict : ∀ {α : Type u} {τ : TopologicalSpace α} [self : WeakPseudoEMetricSpace α] (x : α) (r : ENNReal),
  IsOpen (Subtype.val ⁻¹' Metric.eball x r)
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the mapping for the given key, returning `fallback` if no such mapping is present.

Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 -/
Std.DTreeMap.Const.getD : {α : Type u} → {cmp : α → α → Ordering} → {β : Type v} → Std.DTreeMap α (fun x => β) cmp → α → β → β
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardStringSearcher.instNoSuffixPatternModel : ∀ {pat : String}, String.Slice.Pattern.Model.NoSuffixPatternModel pat
-- Mathlib.Data.List.Sort
/-- **Alias** of the forward direction of `List.sortedGE_map_toDual`. -/
List.SortedGE.map_toDual : ∀ {α : Type u_1} [inst : Preorder α] {l : List α}, (List.map (⇑OrderDual.toDual) l).SortedGE → l.SortedLE
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey?_beq : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → ∀ {a : α}, Option.all (fun x => x == a) (m.getKey? a) = true
-- Init.Data.String.Basic
_private.Init.Data.String.Basic.0.String.Slice.Pos.prevAuxGo_le_self.elim : ∀ (P : String.Pos.Raw → Prop) {h : False}, P h.elim
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxi.Iterator.next : {α : Type u} → Std.Rxi.Iterator α → Option α
-- Mathlib.GroupTheory.GroupAction.Blocks
AddAction.IsBlock.not_vadd_set_ssubset_vadd_set : ∀ {G : Type u_1} {X : Type u_2} [inst : VAdd G X] {B : Set X} {g₁ g₂ : G}, AddAction.IsBlock G B → ¬g₁ +ᵥ B ⊂ g₂ +ᵥ B
-- Std.Data.HashSet.Lemmas
Std.HashSet.get?_eq_some_getD_of_contains : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {a fallback : α},
  m.contains a = true → m.get? a = some (m.getD a fallback)
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
/-- Auxiliary definition for `AlgebraicGeometry.PresheafedSpace.instHasColimits`.
 -/
AlgebraicGeometry.PresheafedSpace.colimitCoconeIsColimit : {J : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J TopCat] →
          [inst_3 : ∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)] →
            [CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ C] →
              (F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C)) →
                CategoryTheory.Limits.IsColimit (AlgebraicGeometry.PresheafedSpace.colimitCocone F)
-- Init.Data.Nat.Lcm
Nat.lcm_dvd_mul_self_left_iff_dvd_mul : ∀ {k n m : ℕ}, k.lcm n ∣ k * m ↔ n ∣ k * m
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- If two affine subspaces have a point in common, the direction of their inf equals the inf of
their directions.  -/
AffineSubspace.direction_inf_of_mem : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {s₁ s₂ : AffineSubspace k P} {p : P},
  p ∈ s₁ → p ∈ s₂ → (s₁ ⊓ s₂).direction = s₁.direction ⊓ s₂.direction
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor_obj_left_as : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor D T) (Y : T) (X : D)
  (Y_1 : CategoryTheory.StructuredArrow X (CategoryTheory.StructuredArrow.proj Y F)),
  ((CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor F Y X).obj Y_1).left.as = PUnit.unit
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
/-- If `f ≫ g` and `g` are closed immersions, then `f` is a closed immersion.
Also see `IsClosedImmersion.of_comp` for the general version
where `g` is only required to be separated.
 -/
AlgebraicGeometry.IsClosedImmersion.of_comp_isClosedImmersion : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.IsClosedImmersion g]
  [AlgebraicGeometry.IsClosedImmersion (CategoryTheory.CategoryStruct.comp f g)], AlgebraicGeometry.IsClosedImmersion f
-- Mathlib.Analysis.Polynomial.MahlerMeasure
Polynomial.logMahlerMeasure_monomial : ∀ (n : ℕ) (z : ℂ), ((Polynomial.monomial n) z).logMahlerMeasure = Real.log ‖z‖
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentSymbolParams.mk.inj : ∀ {textDocument textDocument_1 : Lean.Lsp.TextDocumentIdentifier},
  { textDocument := textDocument } = { textDocument := textDocument_1 } → textDocument = textDocument_1
-- Mathlib.Topology.GDelta.MetrizableSpace
instPerfectlyNormalSpaceOfPseudoMetrizableSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [TopologicalSpace.PseudoMetrizableSpace X], PerfectlyNormalSpace X
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.find?_some_eq_eq : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x y : α} {t : RBTree.RBSet α cmp}, t.find? x = some y → cmp x y = Ordering.eq
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.toFun_smul : ∀ {R : Type u} {M : Type v} {N : Type w} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (self : QuadraticMap R M N) (a : R) (x : M),
  self.toFun (a • x) = (a * a) • self.toFun x
-- Mathlib.Algebra.GroupWithZero.Units.Fintype
UnitsInt.univ : Finset.univ = {1, -1}
-- Lean.Compiler.ImplementedByAttr
Lean.setImplementedBy : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → [Lean.MonadError m] → Lean.Name → Lean.Name → m Unit
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.ExprInfo.mk : Lean.Expr →
  List Lean.FVarId → Lean.LocalContext → Lean.LocalInstances → Lean.Meta.Config → Lean.Meta.RefinedDiscrTree.ExprInfo
-- Mathlib.Topology.Separation.Basic
Finset.isClosed : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] (s : Finset X), IsClosed ↑s
-- Mathlib.Algebra.Group.Shrink
Shrink.instDiv : {α : Type u_2} → [inst : Small.{v, u_2} α] → [Div α] → Div (Shrink.{v, u_2} α)
-- Mathlib.CategoryTheory.Limits.ExactFunctor
/-- Turn an exact functor into an object of the category `ExactFunctor C D`.  -/
CategoryTheory.ExactFunctor.of : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [CategoryTheory.Limits.PreservesFiniteLimits F] → [CategoryTheory.Limits.PreservesFiniteColimits F] → C ⥤ₑ D
-- Mathlib.Algebra.Homology.Additive
CategoryTheory.Equivalence.mapHomologicalComplex_counitIso : ∀ {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [inst : CategoryTheory.Category.{v_2, u_3} W₁]
  [inst_1 : CategoryTheory.Category.{v_3, u_4} W₂] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms W₁]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms W₂] (e : W₁ ≌ W₂) [inst_4 : e.functor.PreservesZeroMorphisms]
  (c : ComplexShape ι),
  (e.mapHomologicalComplex c).counitIso =
    CategoryTheory.NatIso.mapHomologicalComplex e.counitIso c ≪≫ CategoryTheory.Functor.mapHomologicalComplexIdIso W₂ c
-- Mathlib.Computability.Reduce
ManyOneDegree.ind_on : ∀ {C : ManyOneDegree → Prop} (d : ManyOneDegree), (∀ (p : Set ℕ), C (ManyOneDegree.of p)) → C d
-- Mathlib.LinearAlgebra.Dual.Basis
Module.Basis.toDual_eq_repr : ∀ {R : Type uR} {M : Type uM} {ι : Type uι} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : DecidableEq ι] (b : Module.Basis ι R M) (m : M) (i : ι), (b.toDual m) (b i) = (b.repr m) i
-- Mathlib.Data.Finset.Card
Finset.exists_subset_or_subset_of_two_mul_lt_card : ∀ {α : Type u_1} [inst : DecidableEq α] {X Y : Finset α} {n : ℕ},
  2 * n < (X ∪ Y).card → ∃ C, n < C.card ∧ (C ⊆ X ∨ C ⊆ Y)
-- Mathlib.Algebra.Order.Nonneg.Basic
Nonneg.coe_mul : ∀ {α : Type u_1} [inst : MulZeroClass α] [inst_1 : Preorder α] [inst_2 : PosMulMono α] (a b : { x // 0 ≤ x }),
  ↑(a * b) = ↑a * ↑b
-- Batteries.Data.List.Matcher
List.Matcher.mk.injEq : ∀ {α : Type u_1} (toMatcher : Array.Matcher α) (pattern : List α) (toMatcher_1 : Array.Matcher α) (pattern_1 : List α),
  ({ toMatcher := toMatcher, pattern := pattern } = { toMatcher := toMatcher_1, pattern := pattern_1 }) =
    (toMatcher = toMatcher_1 ∧ pattern = pattern_1)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.contains_keysArray : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → ∀ {k : α}, (↑m).keysArray.contains k = m.contains k
-- Mathlib.Order.SymmDiff
inf_symmDiff_distrib_right : ∀ {α : Type u_2} [inst : GeneralizedBooleanAlgebra α] (a b c : α), symmDiff a b ⊓ c = symmDiff (a ⊓ c) (b ⊓ c)
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.instDivInvOneMonoid : {α : Type u_1} → [DivInvOneMonoid α] → DivInvOneMonoid (WithZero α)
-- Init.Data.SInt.Basic
/-- Converts a 32-bit signed integer to an 16-bit signed integer by truncating its bitvector
representation.

This function is overridden at runtime with an efficient implementation.
 -/
Int32.toInt16 : Int32 → Int16
-- Mathlib.Data.Finset.Sups
Finset.disjSups_inter_subset_left : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] [inst_2 : OrderBot α]
  [inst_3 : DecidableRel Disjoint] {s₁ s₂ t : Finset α}, (s₁ ∩ s₂).disjSups t ⊆ s₁.disjSups t ∩ s₂.disjSups t
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If the oriented angle between three points is `-π / 2`, the unoriented angle (reversed) is
`π / 2`.  -/
EuclideanGeometry.angle_rev_eq_pi_div_two_of_oangle_eq_neg_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P}, EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(-Real.pi / 2) → EuclideanGeometry.angle p₃ p₂ p₁ = Real.pi / 2
-- Mathlib.Analysis.Seminorm
Seminorm.instLattice : {𝕜 : Type u_3} →
  {E : Type u_7} → [inst : NormedField 𝕜] → [inst_1 : AddCommGroup E] → [inst_2 : Module 𝕜 E] → Lattice (Seminorm 𝕜 E)
-- Mathlib.Data.Sigma.Lex
PSigma.Lex.decidable : {ι : Sort u_1} →
  {α : ι → Sort u_2} →
    (r : ι → ι → Prop) →
      (s : (i : ι) → α i → α i → Prop) →
        [DecidableEq ι] → [DecidableRel r] → [(i : ι) → DecidableRel (s i)] → DecidableRel (PSigma.Lex r s)
-- Mathlib.Algebra.Group.Subgroup.Map
AddEquiv.symm_comapAddSubgroup : ∀ {G : Type u_1} [inst : AddGroup G] {H : Type u_5} [inst_1 : AddGroup H] (e : G ≃+ H),
  e.comapAddSubgroup.symm = e.symm.comapAddSubgroup
-- Lean.Data.Lsp.Basic
Lean.Lsp.ResolveSupport.mk.sizeOf_spec : ∀ (properties : Array String), sizeOf { properties := properties } = 1 + sizeOf properties
-- Init.Internal.Order.Basic
Lean.Order.FlatOrder.inner_mk : ∀ {α : Sort u} {b x : α}, (Lean.Order.FlatOrder.mk b x).inner = x
-- Mathlib.Topology.Category.Profinite.Extend
Profinite.Extend.functor_map : ∀ {I : Type u} [inst : CategoryTheory.SmallCategory I] {F : CategoryTheory.Functor I FintypeCat}
  (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toProfinite)) {X Y : I} (f : X ⟶ Y),
  (Profinite.Extend.functor c).map f = CategoryTheory.StructuredArrow.homMk (F.map f) ⋯
-- Mathlib.Data.FunLike.IsApply
/-- `IsMulApply F α β` states for all `f g : F` and `x : α`, `(f * g) x = f x * g x`.  -/
IsMulApply : (F : Type u_1) → (α : outParam (Type u_2)) → (β : outParam (Type u_3)) → [FunLike F α β] → [Mul β] → [Mul F] → Prop
-- Mathlib.SetTheory.Ordinal.Basic
/-- **Alias** of `Cardinal.mk_Iio_toType_ord_lt`. -/
Cardinal.mk_Iio_ord_toType : ∀ {c : Cardinal.{u_1}} (i : c.ord.ToType), Cardinal.mk ↑(Set.Iio i) < c
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.succ_pos : ∀ (o : Ordinal.{u_1}), 0 < Order.succ o
-- Mathlib.Computability.Encoding
/-- An encoding function of `Bool` in `Bool`.  -/
Computability.encodeBool : Bool → List Bool
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
/-- If `D` is already an enriched ordinary category, there is a canonical functor from `D` to
`ForgetEnrichment V D`.  -/
CategoryTheory.ForgetEnrichment.equivInverse : (V : Type u') →
  [inst : CategoryTheory.Category.{v', u'} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      (D : Type u'') →
        [inst_2 : CategoryTheory.Category.{v'', u''} D] →
          [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V D] →
            CategoryTheory.Functor D (CategoryTheory.ForgetEnrichment V D)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
le_neg_iff_add_nonpos_right : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddRightMono α] {a b : α}, a ≤ -b ↔ a + b ≤ 0
-- Mathlib.Algebra.DirectSum.Module
DirectSum.IsInternal.collectedBasis_coe : ∀ {R : Type u} [inst : Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] {A : ι → Submodule R M} (h : DirectSum.IsInternal A) {α : ι → Type u_2}
  (v : (i : ι) → Module.Basis (α i) R ↥(A i)), ⇑(h.collectedBasis v) = fun a => ↑((v a.fst) a.snd)
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
/-- The (unique) isomorphism between any terminal object and the zero object.  -/
CategoryTheory.Limits.IsZero.isoIsTerminal : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → CategoryTheory.Limits.IsZero X → CategoryTheory.Limits.IsTerminal Y → (X ≅ Y)
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.map_eq_toIter_map_toIterM : ∀ {α β γ : Type w} [inst : Std.Iterator α Id β] {it : Std.Iter β} {f : β → γ},
  Std.Iter.map f it = (Std.IterM.map f it.toIterM).toIter
-- Std.Sat.AIG.RelabelNat
Std.Sat.AIG.Entrypoint.relabelNat.eq_1 : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] (entry : Std.Sat.AIG.Entrypoint α),
  entry.relabelNat =
    { aig := entry.aig.relabelNat,
      ref :=
        let __src := entry.ref;
        { gate := __src.gate, invert := __src.invert, hgate := ⋯ } }
-- Mathlib.Analysis.InnerProductSpace.Calculus
contDiffAt_norm : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
  [inst : NormedSpace ℝ E] {n : WithTop ℕ∞} {x : E}, x ≠ 0 → ContDiffAt ℝ n norm x
-- Mathlib.LinearAlgebra.Projection
LinearMap.IsProj.isIdempotentElem : ∀ {S : Type u_5} [inst : Semiring S] {M : Type u_6} [inst_1 : AddCommMonoid M] [inst_2 : Module S M] {m : Submodule S M}
  {f : M →ₗ[S] M}, LinearMap.IsProj m f → IsIdempotentElem f
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
_private.Std.Tactic.BVDecide.LRAT.Internal.Clause.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.ofArray.folder.match_6.eq_2 : ∀ {n : ℕ} (motive : Option (Std.HashMap (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) Bool) → Sort u_1)
  (map : Std.HashMap (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) Bool) (h_1 : Unit → motive none)
  (h_2 : (map : Std.HashMap (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) Bool) → motive (some map)),
  (match some map with
    | none => h_1 ()
    | some map => h_2 map) =
    h_2 map
-- Mathlib.Analysis.Normed.Group.Basic
norm_sub_le_of_le : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] {a₁ a₂ : E} {r₁ r₂ : ℝ}, ‖a₁‖ ≤ r₁ → ‖a₂‖ ≤ r₂ → ‖a₁ - a₂‖ ≤ r₁ + r₂
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.Arrow.mapCechConerve_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C}
  [inst_1 : ∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom]
  [inst_2 : ∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout g.left (fun x => g.right) fun x => g.hom] (F : f ⟶ g)
  (n : SimplexCategory),
  (CategoryTheory.Arrow.mapCechConerve F).app n =
    CategoryTheory.Limits.WidePushout.desc
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left F)
        (CategoryTheory.Limits.WidePushout.head fun x => g.hom))
      (fun i =>
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right F)
          (CategoryTheory.Limits.WidePushout.ι (fun x => g.hom) i))
      ⋯
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cocycle.equivHomShift_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ} {K' : CochainComplex C ℤ} (g : K' ⟶ K)
  (f : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L),
  CochainComplex.HomComplex.Cocycle.equivHomShift (CategoryTheory.CategoryStruct.comp g f) =
    (CochainComplex.HomComplex.Cocycle.equivHomShift f).precomp g
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.Hom₂.ofNatTrans : {C D : CategoryTheory.Cat} → {F G : C ⟶ D} → (F.toFunctor ⟶ G.toFunctor) → CategoryTheory.Cat.Hom₂ F G
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.Extension.getMatcherInfo? : Lean.Environment → Lean.Name → Option Lean.Meta.MatcherInfo