mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.coe_ofBialgHom : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (f : A →ₐc[R] B) (g : B →ₐc[R] A) (h₁ : f.comp g = BialgHom.id R B) (h₂ : g.comp f = BialgHom.id R A),
  ↑(BialgEquiv.ofBialgHom f g h₁ h₂) = f
-- Mathlib.CategoryTheory.CodiscreteCategory
/-- For a category `C` and type `A`, there is an equivalence between functions `objects.obj C ⟶ A`
and functors `C ⥤ Codiscrete A`.  -/
CategoryTheory.Codiscrete.equivFunctorToCodiscrete : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : Type w} → (C → A) ≃ CategoryTheory.Functor C (CategoryTheory.Codiscrete A)
-- Lean.Meta.LazyDiscrTree
/-- Get the root key and rest of terms of an expression using the specified config.
 -/
Lean.Meta.LazyDiscrTree.rootKey : Lean.Expr → Lean.MetaM (Lean.Meta.LazyDiscrTree.Key × Array Lean.Expr)
-- Mathlib.Algebra.MonoidAlgebra.Module
AddMonoidAlgebra.symm_mapDomainLinearEquiv : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : Module R S] (e : M ≃ N),
  (AddMonoidAlgebra.mapDomainLinearEquiv R S e).symm = AddMonoidAlgebra.mapDomainLinearEquiv R S e.symm
-- Init.Data.SInt.Lemmas
instCommutativeInt64HAdd : Std.Commutative fun x1 x2 => x1 + x2
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
spectrum_subset_quasispectrum : ∀ (R : Type u_3) {A : Type u_4} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] (a : A),
  spectrum R a ⊆ quasispectrum R a
-- Init.Data.List.Sublist
List.isSublist.eq_3 : ∀ {α : Type u} [inst : BEq α] (hd₁ : α) (tl₁ : List α) (hd₂ : α) (tl₂ : List α),
  (hd₁ :: tl₁).isSublist (hd₂ :: tl₂) = if (hd₁ == hd₂) = true then tl₁.isSublist tl₂ else (hd₁ :: tl₁).isSublist tl₂
-- Mathlib.Data.TypeVec
TypeVec.split_dropFun_lastFun : ∀ {n : ℕ} {α : TypeVec.{u_1} (n + 1)} {α' : TypeVec.{u_2} (n + 1)} (f : α.Arrow α'),
  TypeVec.splitFun (TypeVec.dropFun f) (TypeVec.lastFun f) = f
-- Mathlib.Topology.ContinuousMap.CocompactMap
CocompactMap.coe_mk : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : C(α, β))
  (h : Filter.Tendsto (⇑f) (Filter.cocompact α) (Filter.cocompact β)),
  ⇑{ toContinuousMap := f, cocompact_tendsto' := h } = ⇑f
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instMul : {α : Type u_1} → [Mul α] → Mul (Lex α)
-- Mathlib.CategoryTheory.Functor.TypeValuedFlat
/-- Given a functor `F : C ⥤ Type w`, an object `X : C` and `x : F.obj X`,
this is the equivalence between the category of elements of `fromOverFunctor F x`
with the `Over` category of `x` considered as an object of `F.Elements`.  -/
CategoryTheory.FunctorToTypes.fromOverFunctorElementsEquivalence : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor C (Type w)) →
      {X : C} →
        (x : F.obj X) →
          (CategoryTheory.FunctorToTypes.fromOverFunctor F x).Elements ≌ CategoryTheory.Over (F.elementsMk X x)
-- Mathlib.ModelTheory.Fraisse
/-- A structure `M` is a Fraïssé limit for a class `K` if it is countably generated,
ultrahomogeneous, and has age `K`.  -/
FirstOrder.Language.IsFraisseLimit : {L : FirstOrder.Language} →
  Set (CategoryTheory.Bundled L.Structure) →
    (M : Type w) → [L.Structure M] → [Countable ((l : ℕ) × L.Functions l)] → [Countable M] → Prop
-- Init.Data.Vector.Range
Vector.find?_range'_eq_some : ∀ {s n i : ℕ} {p : ℕ → Bool},
  Vector.find? p (Vector.range' s n) = some i ↔
    p i = true ∧ i ∈ Vector.range' s n ∧ ∀ (j : ℕ), s ≤ j → j < i → (!p j) = true
-- Mathlib.GroupTheory.GroupAction.Iwasawa
/-- The structure underlying the Iwasawa criterion  -/
MulAction.IwasawaStructure : (M : Type u_1) → [inst : Group M] → (α : Type u_2) → [MulAction M α] → Type (max u_1 u_2)
-- Std.Data.HashMap.Lemmas
Std.HashMap.isEmpty_toList : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  m.toList.isEmpty = m.isEmpty
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.isOrthogonal_iff_pairing_eq_zero : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} {i j : ι} [NeZero 2]
  [IsDomain R] [Module.IsTorsionFree R M], P.IsOrthogonal i j ↔ P.pairing i j = 0
-- Mathlib.Topology.MetricSpace.Antilipschitz
/-- The image of a proper space under an expanding onto map is proper.  -/
AntilipschitzWith.properSpace : ∀ {β : Type u_2} [inst : PseudoMetricSpace β] {α : Type u_4} [inst_1 : MetricSpace α] {K : NNReal} {f : α → β}
  [ProperSpace α], AntilipschitzWith K f → Continuous f → Function.Surjective f → ProperSpace β
-- Mathlib.Lean.Meta.Simp
/-- Return all propositions in the local context.  -/
Lean.Meta.Simp.getPropHyps : Lean.MetaM (Array Lean.FVarId)
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.up_size_toArray_eq_length : ∀ {m : Type w → Type u_1} {α β : Type w} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α m m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β},
  (fun x => { down := x.size }) <$> it.toArray = it.length
-- Mathlib.CategoryTheory.Monad.Algebra
/-- The underlying morphism associated to a morphism of coalgebras.  -/
CategoryTheory.Comonad.Coalgebra.Hom.f : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {G : CategoryTheory.Comonad C} → {A B : G.Coalgebra} → A.Hom B → (A.A ⟶ B.A)
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.mul_left_injective_of_inv : ∀ {l : Type u_1} {m : Type u} {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : Fintype m]
  [inst_2 : DecidableEq m] [inst_3 : CommRing α] (A : Matrix m n α) (B : Matrix n m α),
  A * B = 1 → Function.Injective fun x => x * A
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.sumMap_comp_inl : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {L₁ : FirstOrder.Language}
  {L₂ : FirstOrder.Language} (ψ : L₁ →ᴸ L₂),
  (ϕ.sumMap ψ).comp FirstOrder.Language.LHom.sumInl = FirstOrder.Language.LHom.sumInl.comp ϕ
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.grothendieckTypeToCat_inverse_obj_base : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) (X : G.Elements),
  ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).inverse.obj X).base = X.fst
-- Mathlib.Data.Finset.SDiff
Finset.sdiff_insert_of_notMem : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {x : α}, x ∉ s → ∀ (t : Finset α), s \ insert x t = s \ t
-- Mathlib.LinearAlgebra.RootSystem.BaseExists
/-- This lemma is usually established for root systems with coefficients `R` equal to `ℚ` or `ℝ`, in
which case one may take `S = R`. However our statement allows for more general coefficients such as
`R = ℂ` and `S = ℚ`.

This lemma is mostly a stepping stone en route to `RootPairing.linearIndepOn_root_baseOf` (where
linear independence is established over `R` rather than just `S`) except that this version does not
make the field assumption and so covers the case `S = R = ℤ` which the latter does not.  -/
RootPairing.linearIndepOn_root_baseOf' : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [inst : AddCommGroup M]
  [inst_1 : AddCommGroup N] [inst_2 : CommRing R] [inst_3 : Module R M] [inst_4 : Module R N] (P : RootPairing ι R M N)
  [IsDomain R] {S : Type u_6} [inst_6 : LinearOrder S] [inst_7 : CommRing S] [IsStrictOrderedRing S]
  [inst_9 : Algebra S R] [FaithfulSMul S R] [inst_11 : Module S M] [IsScalarTower S R M] [inst_13 : Module S N]
  [IsScalarTower S R N] [P.IsValuedIn S] [P.IsCrystallographic] (f : Module.Dual S M),
  (∀ (i : ι), f (P.root i) ≠ 0) → LinearIndepOn S (⇑P.root) (IsAddIndecomposable.baseOf ⇑P.root ↑f)
-- Mathlib.Algebra.Homology.DerivedCategory.Fractions
DerivedCategory.instHasRightCalculusOfFractionsHomotopyCategoryIntUpQuasiIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C],
  (HomotopyCategory.quasiIso C (ComplexShape.up ℤ)).HasRightCalculusOfFractions
-- Mathlib.Geometry.Euclidean.Triangle
/-- The least angle of a possibly degenerate triangle is less than `π / 3`, unless all angles are
equal.  -/
EuclideanGeometry.angle_lt_pi_div_three_of_le_of_le_of_ne : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P},
  EuclideanGeometry.angle p₁ p₂ p₃ ≤ EuclideanGeometry.angle p₂ p₃ p₁ →
    EuclideanGeometry.angle p₁ p₂ p₃ ≤ EuclideanGeometry.angle p₃ p₁ p₂ →
      EuclideanGeometry.angle p₁ p₂ p₃ ≠ EuclideanGeometry.angle p₂ p₃ p₁ ∨
          EuclideanGeometry.angle p₁ p₂ p₃ ≠ EuclideanGeometry.angle p₃ p₁ p₂ ∨
            EuclideanGeometry.angle p₂ p₃ p₁ ≠ EuclideanGeometry.angle p₃ p₁ p₂ →
        EuclideanGeometry.angle p₁ p₂ p₃ < Real.pi / 3
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Bicategory.leftZigzagIso_inv : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {a b : B} {f : a ⟶ b} {g : b ⟶ a}
  (η : CategoryTheory.CategoryStruct.id a ≅ CategoryTheory.CategoryStruct.comp f g)
  (ε : CategoryTheory.CategoryStruct.comp g f ≅ CategoryTheory.CategoryStruct.id b),
  (CategoryTheory.Bicategory.leftZigzagIso η ε).inv = CategoryTheory.Bicategory.rightZigzag ε.inv η.inv
-- Mathlib.Order.Defs.PartialOrder
instTransLT : {α : Type u_1} → [inst : Preorder α] → Trans LT.lt LT.lt LT.lt
-- Mathlib.Topology.Instances.AddCircle.Defs
/-- `toIocDiv` is continuous on the set of points
that aren't congruent to the endpoint modulo the period.  -/
continuousOn_toIocDiv : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  [inst_3 : Archimedean 𝕜] [inst_4 : TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a : 𝕜),
  ContinuousOn (toIocDiv hp a) {x | ¬x ≡ a [PMOD p]}
-- Mathlib.CategoryTheory.Abelian.Pseudoelements
CategoryTheory.Abelian.app.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q : C} (f : P ⟶ Q) (a : CategoryTheory.Over P),
  CategoryTheory.Abelian.app f a = CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.comp a.hom f)
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.AssociatorBimod.hom_left_act_hom' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C]
  [inst_3 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorLeft X)]
  [inst_4 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorRight X)]
  {R S T U : CategoryTheory.Mon C} (P : Bimod R S) (Q : Bimod S T) (L : Bimod T U),
  CategoryTheory.CategoryStruct.comp ((P.tensorBimod Q).tensorBimod L).actLeft (Bimod.AssociatorBimod.hom P Q L) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R.X (Bimod.AssociatorBimod.hom P Q L))
      (P.tensorBimod (Q.tensorBimod L)).actLeft
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s_comp_base_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (f : CategoryTheory.Arrow C)
  [inst_1 : ∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom]
  (S : CategoryTheory.SplitEpi f.hom) (n : ℕ) {Z : C} (h : f.right ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s f S n)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.base fun x => f.hom) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.base fun x => f.hom) h
-- Aesop.Tree.Data.ForwardRuleMatches
Aesop.ForwardRuleMatches.mk.sizeOf_spec : ∀ (normMatches safeMatches unsafeMatches : Lean.PHashSet Aesop.ForwardRuleMatch),
  sizeOf { normMatches := normMatches, safeMatches := safeMatches, unsafeMatches := unsafeMatches } =
    1 + sizeOf normMatches + sizeOf safeMatches + sizeOf unsafeMatches
-- Init.Data.List.Attach
wfParam.eq_1 : ∀ {α : Sort u} (a : α), wfParam a = a
-- Mathlib.Order.SymmDiff
symmDiff_symmDiff_right' : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (a b c : α),
  symmDiff a (symmDiff b c) = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ aᶜ ⊓ b ⊓ cᶜ ⊔ aᶜ ⊓ bᶜ ⊓ c
-- Batteries.Data.List.Lemmas
List.findIdxNth_cons_succ_of_pos : ∀ {α : Type u_1} {p : α → Bool} {xs : List α} {n : ℕ} {a : α},
  p a = true → List.findIdxNth p (a :: xs) (n + 1) = List.findIdxNth p xs n + 1
-- Mathlib.Analysis.CStarAlgebra.Matrix
Matrix.l2_opNorm_mulVec : ∀ {𝕜 : Type u_1} {m : Type u_2} {n : Type u_3} [inst : RCLike 𝕜] [inst_1 : Fintype m] [inst_2 : Fintype n]
  [inst_3 : DecidableEq n] (A : Matrix m n 𝕜) (x : EuclideanSpace 𝕜 n),
  ‖(EuclideanSpace.equiv m 𝕜).symm (A.mulVec x.ofLp)‖ ≤ ‖A‖ * ‖x‖
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.contains_eq_isSome_get?ₘ : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α}
  {t : Std.DTreeMap.Internal.Impl α fun x => β},
  t.Ordered → Std.DTreeMap.Internal.Impl.contains k t = (Std.DTreeMap.Internal.Impl.Const.get?ₘ t k).isSome
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.prod_le_prod : ∀ {ι : Type u_1} (f g : ι → Cardinal.{u_2}), (∀ (i : ι), f i ≤ g i) → Cardinal.prod f ≤ Cardinal.prod g
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
/-- Pull an opposite subsemigroup back to a subsemigroup along `MulOpposite.op`  -/
Subsemigroup.unop : {M : Type u_2} → [inst : Mul M] → Subsemigroup Mᵐᵒᵖ → Subsemigroup M
-- Mathlib.Topology.UniformSpace.Equicontinuity
Set.EquicontinuousAt.continuousAt_of_mem : ∀ {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {H : Set (X → α)} {x₀ : X},
  H.EquicontinuousAt x₀ → ∀ {f : X → α}, f ∈ H → ContinuousAt f x₀
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.instSMul.eq_1 : ∀ (p : ENNReal) (K : Type u_1) (V : Type u_4) [inst : SMul K V], WithLp.instSMul p K V = Equiv.smul K (WithLp.equiv p V)
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_left_le_size_union : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  m₁.size ≤ (m₁ ∪ m₂).size
-- Mathlib.Control.Functor
/-- Extract the element of `α` from the `Const` functor.  -/
Functor.Const.run : {α : Type u_1} → {β : Type u_2} → Functor.Const α β → α
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.map_reindex : ∀ {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7}
  [inst_1 : (i : ι) → AddCommMonoid (s i)] [inst_2 : (i : ι) → Module R (s i)] {t : ι → Type u_11}
  [inst_3 : (i : ι) → AddCommMonoid (t i)] [inst_4 : (i : ι) → Module R (t i)] (f : (i : ι) → s i →ₗ[R] t i)
  (e : ι ≃ ι₂) (x : PiTensorProduct R fun i => s i),
  (PiTensorProduct.map fun i => f (e.symm i)) ((PiTensorProduct.reindex R s e) x) =
    (PiTensorProduct.reindex R t e) ((PiTensorProduct.map f) x)
-- Lean.Util.LeanOptions
/-- Restriction of `DataValue` that covers exactly those cases that Lean is able to handle when passed via the `-D` flag.  -/
Lean.LeanOptionValue : Type
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Extract
Std.Tactic.BVDecide.BVExpr.bitblast.ExtractTarget.mk.injEq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {len w : ℕ} (vec : aig.RefVec w)
  (start w_1 : ℕ) (vec_1 : aig.RefVec w_1) (start_1 : ℕ),
  ({ w := w, vec := vec, start := start } = { w := w_1, vec := vec_1, start := start_1 }) =
    (w = w_1 ∧ vec ≍ vec_1 ∧ start = start_1)
-- Mathlib.Analysis.Normed.Group.Ultra
IsUltrametricDist.norm_mul_le_max : ∀ {S : Type u_1} [inst : SeminormedGroup S] [IsUltrametricDist S] (x y : S), ‖x * y‖ ≤ max ‖x‖ ‖y‖
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
/-- A probability distribution with weight `s` on `x` and weight `t` on `y`.  -/
Convexity.StdSimplex.duple : {R : Type u} →
  [inst : PartialOrder R] →
    [inst_1 : Semiring R] →
      {M : Type u_9} →
        [IsStrictOrderedRing R] → M → M → {s t : R} → 0 ≤ s → 0 ≤ t → s + t = 1 → Convexity.StdSimplex R M
-- Init.Data.SInt.Lemmas
Int8.zero_sub : ∀ (a : Int8), 0 - a = -a
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_throw_ReaderT_lift_apply_eq : ∀ {Pred : Type u_1} {EPred : Type u_2} {ε : Type u_3} {m : Type u → Type v} [inst : Monad m]
  [inst_1 : Std.Internal.Do.Assertion Pred] [inst_2 : Std.Internal.Do.Assertion EPred]
  [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] [inst_4 : MonadExceptOf ε m] {ρ α : Type u} {post : α → ρ → Pred}
  {epost : EPred} (err : ε),
  Std.Internal.Do.wp (MonadExceptOf.throw err) post epost =
    Std.Internal.Do.wp (MonadLift.monadLift (MonadExceptOf.throw err)) post epost
-- Mathlib.CategoryTheory.Sites.Monoidal
/-- The monoidal category structure on `Sheaf J A` obtained in `Sheaf.monoidalCategory` is
symmetric when `A` is symmetric.  -/
CategoryTheory.Sheaf.symmetricCategory : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (A : Type u₃) →
        [inst_1 : CategoryTheory.Category.{v₃, u₃} A] →
          [inst_2 : CategoryTheory.MonoidalCategory A] →
            [inst_3 : J.W.IsMonoidal] →
              [inst_4 : CategoryTheory.HasWeakSheafify J A] →
                [CategoryTheory.SymmetricCategory A] → CategoryTheory.SymmetricCategory (CategoryTheory.Sheaf J A)
-- Mathlib.Algebra.WithConv
/-- This prevents `toConv x` being printed as `{ ofConv := x }` by `delabStructureInstance`.  -/
WithConv.delabToConv : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Analysis.Convex.Gauge
/-- If `s` is a convex neighborhood of the origin in a topological real vector space, then `gauge s`
is continuous. If the ambient space is a normed space, then `gauge s` is Lipschitz continuous, see
`Convex.lipschitz_gauge`.  -/
continuous_gauge : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} [inst_2 : TopologicalSpace E]
  [IsTopologicalAddGroup E] [ContinuousSMul ℝ E], Convex ℝ s → s ∈ nhds 0 → Continuous (gauge s)
-- Init.Data.UInt.Lemmas
UInt8.toUSize_neg : ∀ (a : UInt8), (-a).toUSize = -a.toUSize % 256
-- Mathlib.Data.Nat.Bits
/-- `bits n` returns a list of Bools which correspond to the binary representation of n, where
the head of the list represents the least significant bit  -/
Nat.bits : ℕ → List Bool
-- Mathlib.Analysis.Calculus.Deriv.Basic
derivWithin_zero : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (s : Set 𝕜), derivWithin 0 s = 0
-- Mathlib.MeasureTheory.Group.Prod
/-- Left invariant Borel measures on an additive measurable group are unique (up to a scalar).  -/
MeasureTheory.measure_eq_sub_vadd : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd₂ G] {s : Set G} [MeasurableNeg G]
  (μ' ν' : MeasureTheory.Measure G) [MeasureTheory.SigmaFinite μ'] [MeasureTheory.SigmaFinite ν']
  [μ'.IsAddLeftInvariant] [ν'.IsAddLeftInvariant], ν' s ≠ 0 → ν' s ≠ ⊤ → μ' = (μ' s / ν' s) • ν'
-- Mathlib.ModelTheory.ElementaryMaps
/-- The identity elementary embedding from a structure to itself  -/
FirstOrder.Language.ElementaryEmbedding.refl : (L : FirstOrder.Language) → (M : Type u_1) → [inst : L.Structure M] → L.ElementaryEmbedding M M
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.Splitting.rightHom_splitting : ∀ {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} (s : S.Splitting) (g : G), S.rightHom (s g) = g
-- Mathlib.Algebra.Group.Basic
eq_iff_eq_of_mul_eq_mul : ∀ {α : Type u_1} [inst : CancelCommMonoid α] {a b c d : α}, a * b = c * d → (a = c ↔ b = d)
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'₀₁₃_inv : ∀ {B : Type u₁} {C : Type u₂} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  [inst_2 : CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁)
  (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃)
  (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
  (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv)
      (F.mapComp' f₀₁ f₁₃ f hf).inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv (F.map f₂₃))
        (F.mapComp' f₀₂ f₂₃ f ⋯).inv)
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.norm_sq_eq_add_norm_sq_starProjection : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x : E) (S : Submodule 𝕜 E) [inst_3 : S.HasOrthogonalProjection],
  ‖x‖ ^ 2 = ‖S.starProjection x‖ ^ 2 + ‖Sᗮ.starProjection x‖ ^ 2
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- When the second map `S.g` is zero, this is the homology data on `S` given by
the chosen `cokernel S.f`  -/
CategoryTheory.ShortComplex.HomologyData.ofHasCokernel : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) → S.g = 0 → [CategoryTheory.Limits.HasCokernel S.f] → S.HomologyData
-- Mathlib.Order.Filter.Tendsto
Filter.Tendsto.congr' : ∀ {α : Type u_1} {β : Type u_2} {f₁ f₂ : α → β} {l₁ : Filter α} {l₂ : Filter β},
  f₁ =ᶠ[l₁] f₂ → Filter.Tendsto f₁ l₁ l₂ → Filter.Tendsto f₂ l₁ l₂
-- Init.Data.Range.Polymorphic.Fin
Fin.pRangeSuccMany?_eq : ∀ {n m : ℕ}, Std.PRange.succMany? m = fun x => x.addNat? m
-- Std.Internal.UV.System
/-- Sets the value of an environment variable.
 -/
Std.Internal.UV.System.osSetenv : String → String → IO Unit
-- Mathlib.MeasureTheory.MeasurableSpace.Invariants
MeasurableSpace.invariants_id : ∀ {α : Type u_1} [inst : MeasurableSpace α], MeasurableSpace.invariants id = inst
-- Lean.Expr
Lean.Expr.sortLevel! : Lean.Expr → Lean.Level
-- Mathlib.Algebra.Lie.Classical
LieAlgebra.Orthogonal.indefiniteDiagonal.congr_simp : ∀ (p : Type u_2) (q : Type u_3) (R : Type u₂) {inst : DecidableEq p} [inst_1 : DecidableEq p] {inst_2 : DecidableEq q}
  [inst_3 : DecidableEq q] [inst_4 : CommRing R] (a a_1 : p ⊕ q),
  a = a_1 →
    ∀ (a_2 a_3 : p ⊕ q),
      a_2 = a_3 →
        LieAlgebra.Orthogonal.indefiniteDiagonal p q R a a_2 = LieAlgebra.Orthogonal.indefiniteDiagonal p q R a_1 a_3
-- Mathlib.Algebra.Group.Subgroup.Map
AddEquiv.comapAddSubgroup_apply : ∀ {G : Type u_1} [inst : AddGroup G] {H : Type u_5} [inst_1 : AddGroup H] (f : G ≃+ H) (H_1 : AddSubgroup H),
  f.comapAddSubgroup H_1 = AddSubgroup.comap (↑f) H_1
-- Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart
CStarAlgebra.exists_sum_four_nonneg : ∀ {A : Type u_2} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] (a : A),
  ∃ x, (∀ (i : Fin 4), 0 ≤ x i) ∧ (∀ (i : Fin 4), ‖x i‖ ≤ ‖a‖) ∧ a = ∑ i, Complex.I ^ ↑i • x i
-- Mathlib.Data.Fintype.Defs
Lex.fintype : (α : Type u_4) → [Fintype α] → Fintype (Lex α)
-- Mathlib.NumberTheory.Dioph
Dioph.diophFn_vec : ∀ {n : ℕ} (f : Vector3 ℕ n → ℕ), Dioph.DiophFn f ↔ Dioph {v | f (v ∘ Fin2.fs) = v Fin2.fz}