mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.AbsolutelyContinuous
/-- Eta-expanded form of `AbsolutelyContinuousOnInterval.neg` -/
AbsolutelyContinuousOnInterval.fun_neg : ∀ {F : Type u_2} [inst : SeminormedAddCommGroup F] {a b : ℝ} {f : ℝ → F},
  AbsolutelyContinuousOnInterval f a b → AbsolutelyContinuousOnInterval (fun i => -f i) a b
-- Mathlib.RingTheory.Polynomial.GaussNorm
_private.Mathlib.RingTheory.Polynomial.GaussNorm.0.Polynomial.sup'_nonneg_of_ne_zero : ∀ {R : Type u_1} {F : Type u_2} [inst : Semiring R] [inst_1 : FunLike F R ℝ] (v : F) {c : ℝ} [NonnegHomClass F R ℝ]
  {p : Polynomial R} (h : p.support.Nonempty), 0 ≤ c → 0 ≤ p.support.sup' h fun i => v (p.coeff i) * c ^ i
-- Mathlib.Analysis.Normed.Group.Quotient
/-- The norm of the image of `m : M` in the quotient by a closed subgroup `S` is zero
if and only if `m ∈ S`.  -/
QuotientAddGroup.norm_mk_eq_zero : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] {S : AddSubgroup M} {m : M} [hS : IsClosed ↑S], ‖↑m‖ = 0 ↔ m ∈ S
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.pointwiseRightKanExtension_lift_app : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [inst_3 : L.HasPointwiseRightKanExtension F]
  (G : CategoryTheory.Functor D H) (α : L.comp G ⟶ F) (Y : D),
  ((L.pointwiseRightKanExtension F).liftOfIsRightKanExtension (L.pointwiseRightKanExtensionCounit F) G α).app Y =
    CategoryTheory.Limits.limit.lift ((CategoryTheory.StructuredArrow.proj Y L).comp F)
      (L.structuredArrowMapCone F G α Y)
-- Mathlib.Algebra.Group.Irreducible.Lemmas
addIrreducible_addUnits_add : ∀ {M : Type u_2} [inst : AddMonoid M] {y : M} (u : AddUnits M), AddIrreducible (↑u + y) ↔ AddIrreducible y
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.contSupp_fix : ∀ (f : Turing.ToPartrec.Code) (k : Turing.PartrecToTM2.Cont'),
  Turing.PartrecToTM2.contSupp (Turing.PartrecToTM2.Cont'.fix f k) =
    Turing.PartrecToTM2.codeSupp f (Turing.PartrecToTM2.Cont'.fix f k)
-- Mathlib.Analysis.Seminorm
Seminorm.finset_sup_le_sum : ∀ {𝕜 : Type u_3} {E : Type u_7} {ι : Type u_11} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] (p : ι → Seminorm 𝕜 E) (s : Finset ι), s.sup p ≤ ∑ i ∈ s, p i
-- Std.Tactic.BVDecide.LRAT.Internal.LRATCheckerSound
_private.Std.Tactic.BVDecide.LRAT.Internal.LRATCheckerSound.0.Std.Tactic.BVDecide.LRAT.Internal.lratChecker.match_3.eq_5 : ∀ {α : Type u_1} {β : Type u_2} (motive : List (Std.Tactic.BVDecide.LRAT.Action β α) → Sort u_3) (ids : Array ℕ)
  (restPrf : List (Std.Tactic.BVDecide.LRAT.Action β α)) (h_1 : Unit → motive [])
  (h_2 :
    (id : ℕ) →
      (rupHints : Array ℕ) →
        (tail : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
          motive (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints :: tail))
  (h_3 :
    (id : ℕ) →
      (c : β) →
        (rupHints : Array ℕ) →
          (restPrf : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
            motive (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints :: restPrf))
  (h_4 :
    (id : ℕ) →
      (c : β) →
        (pivot : Std.Sat.Literal α) →
          (rupHints : Array ℕ) →
            (ratHints : Array (ℕ × Array ℕ)) →
              (restPrf : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
                motive (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints :: restPrf))
  (h_5 :
    (ids : Array ℕ) →
      (restPrf : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
        motive (Std.Tactic.BVDecide.LRAT.Action.del ids :: restPrf)),
  (match Std.Tactic.BVDecide.LRAT.Action.del ids :: restPrf with
    | [] => h_1 ()
    | Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints :: tail => h_2 id rupHints tail
    | Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints :: restPrf => h_3 id c rupHints restPrf
    | Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints :: restPrf =>
      h_4 id c pivot rupHints ratHints restPrf
    | Std.Tactic.BVDecide.LRAT.Action.del ids :: restPrf => h_5 ids restPrf) =
    h_5 ids restPrf
-- Mathlib.Analysis.Real.OfDigits
Real.ofDigitsTerm_nonneg : ∀ {b : ℕ} {digits : ℕ → Fin b} {n : ℕ}, 0 ≤ Real.ofDigitsTerm digits n
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.LeftExtension.mk_right : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : F ⟶ L.comp F'), (CategoryTheory.Functor.LeftExtension.mk F' α).right = F'
-- Init.Data.Option.Instances
/-- Given an optional value and a function that can be applied when the value is `some`, returns the
result of applying the function if this is possible.

The function `f` is _partial_ because it is only defined for the values `a : α` such that
`o = some a`. This restriction allows the function to use the fact that it can only be called when
`o` is not `none`: it can relate its argument to the optional value `o`. Its runtime behavior is
equivalent to that of `Option.bind`.

Examples:
```lean example
def attach (v : Option α) : Option { y : α // v = some y } :=
  v.pbind fun x h => some ⟨x, h⟩
```
```lean example
#reduce attach (some 3)
```
```output
some ⟨3, ⋯⟩
```
```lean example
#reduce attach none
```
```output
none
```
 -/
Option.pbind : {α : Type u_1} → {β : Type u_2} → (o : Option α) → ((a : α) → o = some a → Option β) → Option β
-- Mathlib.Algebra.Group.UniqueProds.VectorSpace
/-- Any `ℚ`-vector space has `TwoUniqueSums`, because it is isomorphic to some
`(Basis.ofVectorSpaceIndex ℚ G) →₀ ℚ` by choosing a basis, and `ℚ` already has
`TwoUniqueSums` because it's ordered.  -/
instTwoUniqueSumsOfModuleRat : ∀ {G : Type u_1} [inst : AddCommGroup G] [Module ℚ G], TwoUniqueSums G
-- Mathlib.CategoryTheory.Category.ReflQuiv
/-- Constructor for morphisms in `FreeRefl`.  -/
CategoryTheory.Cat.FreeRefl.homMk : {V : Type u_1} →
  [inst : CategoryTheory.ReflQuiver V] →
    {v w : V} → (v ⟶ w) → (CategoryTheory.Cat.FreeRefl.mk v ⟶ CategoryTheory.Cat.FreeRefl.mk w)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.map_toNonUnitalSubalgebra : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B] [inst_5 : Module R B] [inst_6 : Star B]
  [inst_7 : FunLike F A B] [inst_8 : NonUnitalAlgHomClass F R A B] [inst_9 : StarHomClass F A B]
  {S : NonUnitalStarSubalgebra R A} {f : F},
  (NonUnitalStarSubalgebra.map f S).toNonUnitalSubalgebra = NonUnitalSubalgebra.map f S.toNonUnitalSubalgebra
-- Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
CategoryTheory.EffectiveEpiFamilyStruct.desc.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {B : C} {α : Type u_2} {X : α → C}
  {π : (a : α) → X a ⟶ B} (self self_1 : CategoryTheory.EffectiveEpiFamilyStruct X π),
  self = self_1 →
    ∀ {W : C} (e e_1 : (a : α) → X a ⟶ W) (e_e : e = e_1)
      (a :
        ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
          CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) →
            CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂)),
      self.desc e a = self_1.desc e_1 ⋯
-- Mathlib.Data.Fintype.Perm
nodup_permsOfList : ∀ {α : Type u_1} [inst : DecidableEq α] {l : List α}, l.Nodup → (permsOfList l).Nodup
-- Mathlib.Topology.Sheaves.LocalPredicate
/-- Given a `P : PrelocalPredicate`, we can always construct a `LocalPredicate`
by asking that the condition from `P` holds locally near every point.
 -/
TopCat.PrelocalPredicate.sheafify : {X : TopCat} → {T : ↑X → Type u_2} → TopCat.PrelocalPredicate T → TopCat.LocalPredicate T
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm_mono_nnnorm : ∀ {α : Type u_1} {F : Type u_5} {G : Type u_6} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup F] [inst_1 : NormedAddCommGroup G] {f : α → F} {g : α → G},
  (∀ (x : α), ‖f x‖₊ ≤ ‖g x‖₊) → MeasureTheory.eLpNorm f p μ ≤ MeasureTheory.eLpNorm g p μ
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
HasDerivWithinAt.cos : ∀ {f : ℝ → ℝ} {f' x : ℝ} {s : Set ℝ},
  HasDerivWithinAt f f' s x → HasDerivWithinAt (fun x => Real.cos (f x)) (-Real.sin (f x) * f') s x
-- Mathlib.Tactic.SuppressCompilation
/-- The command `unsuppress_compilation in def foo : ...` makes sure that the definition is
compiled to executable code, even if `suppress_compilation` is active.  -/
commandUnsuppress_compilationIn_ : Lean.ParserDescr
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.infDegree_withTop_some_comp : ∀ {R : Type u_1} {A : Type u_3} {T : Type u_4} [inst : Semiring R] [inst_1 : SemilatticeInf T] [inst_2 : OrderTop T]
  {D : A → T} {s : AddMonoidAlgebra R A},
  s.coeff.support.Nonempty → AddMonoidAlgebra.infDegree (WithTop.some ∘ D) s = ↑(AddMonoidAlgebra.infDegree D s)
-- Mathlib.Combinatorics.Graph.Simple
Graph.instSimpleBot : ∀ {α : Type u_1} {β : Type u_2}, ⊥.Simple
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
add_tsub_tsub_cancel : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α], c ≤ a → a + b - (a - c) = b + c
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.MeasurePreserving.integral_comp : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {β : Type u_6} {x : MeasurableSpace β} {f : α → β} {ν : MeasureTheory.Measure β},
  MeasureTheory.MeasurePreserving f μ ν →
    MeasurableEmbedding f → ∀ (g : β → G), ∫ (x : α), g (f x) ∂μ = ∫ (y : β), g y ∂ν
-- Mathlib.CategoryTheory.Preadditive.Comma
CategoryTheory.CommaMorphism.sub_left : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Preadditive A] {B : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} B] [inst_3 : CategoryTheory.Preadditive B] {T : Type u₃}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} T] [inst_5 : CategoryTheory.Preadditive T] (L : CategoryTheory.Functor A T)
  [inst_6 : L.Additive] (R : CategoryTheory.Functor B T) [inst_7 : R.Additive] {u v : CategoryTheory.Comma L R}
  (α β : u ⟶ v), (α - β).left = α.left - β.left
-- Init.PropLemmas
Decidable.iff_congr_right : ∀ {P Q R : Prop} [Decidable P] [Decidable Q] [Decidable R], ((P ↔ Q) ↔ (P ↔ R)) ↔ (Q ↔ R)
-- Init.Data.SInt.Lemmas
Int8.toInt.inj : ∀ {x y : Int8}, x.toInt = y.toInt → x = y
-- Mathlib.Algebra.Algebra.Spectrum.Basic
_private.Mathlib.Algebra.Algebra.Spectrum.Basic.0.spectrum.«term↑ₐ_1» : Lean.ParserDescr
-- Mathlib.Data.Multiset.Range
Multiset.range.eq_1 : ∀ (n : ℕ), Multiset.range n = ↑(List.range n)
-- Mathlib.Algebra.Order.GroupWithZero.Finset
Finset.mul_inf_le_inf_mul_of_nonneg : ∀ {ι : Type u_1} {M₀ : Type u_2} [inst : MonoidWithZero M₀] {s : Finset ι} {a b : ι → M₀} [inst_1 : SemilatticeInf M₀]
  [inst_2 : OrderTop M₀] [PosMulMono M₀] [MulPosMono M₀],
  (∀ i ∈ s, 0 ≤ a i) → (∀ i ∈ s, 0 ≤ b i) → s.inf a * s.inf b ≤ s.inf (a * b)
-- Mathlib.Algebra.Algebra.Hom
Algebra.algebraMapSubmonoid_le_comap : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (M : Submonoid R)
  {B : Type w} [inst_3 : Semiring B] [inst_4 : Algebra R B] (f : A →ₐ[R] B),
  Algebra.algebraMapSubmonoid A M ≤ Submonoid.comap f.toRingHom (Algebra.algebraMapSubmonoid B M)
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.RingCompare.mk : {u : Lean.Level} →
  {α : Q(Type u)} →
    {BaseType : Q(«$α») → Type} →
      ({x y : Q(«$α»)} → BaseType x → BaseType y → Bool) →
        ({x y : Q(«$α»)} → BaseType x → BaseType y → Ordering) → Mathlib.Tactic.Ring.Common.RingCompare BaseType
-- Init.Data.Fin.Lemmas
Fin.castSucc_eq_zero_iff : ∀ {n : ℕ} [inst : NeZero n] {a : Fin n}, a.castSucc = 0 ↔ a = 0
-- Init.Data.UInt.Bitwise
UInt16.and_assoc : ∀ (a b c : UInt16), a &&& b &&& c = a &&& (b &&& c)
-- Mathlib.Algebra.WithConv
WithConv.toConv.injEq : ∀ {A : Sort u_1} (ofConv ofConv_1 : A), (WithConv.toConv ofConv = WithConv.toConv ofConv_1) = (ofConv = ofConv_1)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instMul : {α : Type u_1} → {β : Type u_2} → [inst : MeasurableSpace α] → [Mul β] → Mul (MeasureTheory.SimpleFunc α β)
-- Mathlib.Order.Filter.IsBounded
/-- A bounded above function `u` is in particular eventually bounded above.  -/
BddAbove.isBoundedUnder_of_range : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] {f : Filter β} {u : β → α},
  BddAbove (Set.range u) → Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
/-- An odd function is interval integrable (with respect to the volume measure) on every interval
of the form `0..x` if it is interval integrable (with respect to the volume measure) on every
interval of the form `0..x`, for positive `x`.

See `intervalIntegrable_of_odd` for a stronger result.  -/
intervalIntegrable_of_odd₀ : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] {f : ℝ → E},
  (∀ (x : ℝ), -f x = f (-x)) →
    (∀ (x : ℝ), 0 < x → IntervalIntegrable f MeasureTheory.volume 0 x) →
      ∀ {t : ℝ},
        autoParam (‖f (min 0 t)‖ₑ ≠ ⊤) intervalIntegrable_of_odd₀._auto_1 →
          IntervalIntegrable f MeasureTheory.volume 0 t
-- Lean.Elab.PreDefinition.MkInhabitant
/-- Find an inhabitant while doing delta unfolding.
 -/
_private.Lean.Elab.PreDefinition.MkInhabitant.0.Lean.Elab.mkInhabitantForAux? : Array Lean.Expr → Array Lean.Expr → Lean.Expr → Bool → Lean.MetaM (Option Lean.Expr)
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.sumEmpty_apply_inl : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_5} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_9}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {n : WithTop ℕ∞} {M' : Type u_13}
  [inst_6 : TopologicalSpace M'] [inst_7 : ChartedSpace H M'] [inst_8 : IsEmpty M'] (x : M),
  (Diffeomorph.sumEmpty I M n) (Sum.inl x) = x
-- Std.Data.DHashMap.Raw
/-- Creates a new empty hash map. The optional parameter `capacity` can be supplied to presize the
map so that it can hold the given number of mappings without reallocating. It is also possible to
use the empty collection notations `∅` and `{}` to create an empty hash map with the default
capacity.
 -/
Std.DHashMap.Raw.emptyWithCapacity : {α : Type u} → {β : α → Type v} → optParam ℕ 8 → Std.DHashMap.Raw α β
-- Lean.Meta.Match.Basic
Lean.Meta.Match.instInhabitedProblem.default : Lean.Meta.Match.Problem
-- Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
CategoryTheory.monoidalOfHasFiniteCoproducts.associator_hom : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasInitial C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] (X Y Z : C),
  (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom =
    CategoryTheory.Limits.coprod.desc
      (CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inl
        (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr))
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inr)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Arrow.w : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q W : CategoryTheory.MorphismProperty T}
  [inst_1 : Q.IsMultiplicative] [inst_2 : W.IsMultiplicative] {A B : P.Arrow Q W} (f : A ⟶ B),
  CategoryTheory.CategoryStruct.comp f.left B.hom = CategoryTheory.CategoryStruct.comp A.hom f.right
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instDivInvMonoid.eq_1 : ∀ {α : Type u_1} [inst : DivInvMonoid α],
  Colex.instDivInvMonoid =
    { toMonoid := Colex.instMonoid, toInv := Colex.instInv, toDiv := Colex.instDiv, toZPow := ZPow.ofPow,
      div_eq_mul_inv := ⋯, zpow_zero' := ⋯, zpow_succ' := ⋯, zpow_neg' := ⋯ }
-- Init.Data.Array.Lemmas
Array.setIfInBounds_append_left : ∀ {α : Type u_1} {xs ys : Array α} {i : ℕ} {x : α},
  i < xs.size → (xs ++ ys).setIfInBounds i x = xs.setIfInBounds i x ++ ys
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.instInhabitedAndKind : Inhabited Mathlib.Tactic.ITauto.AndKind
-- Mathlib.Data.EReal.Operations
/-- Induct on two ereals by performing case splits on the sign of one whenever the other is
infinite. This version eliminates some cases by assuming that `P` is symmetric and `P x y` implies
`P (-x) y` for all `x`, `y`.  -/
EReal.induction₂_symm_neg : ∀ {P : EReal → EReal → Prop},
  (∀ {x y : EReal}, P x y → P y x) →
    (∀ {x y : EReal}, P x y → P (-x) y) →
      P ⊤ ⊤ → (∀ (x : ℝ), 0 < x → P ⊤ ↑x) → P ⊤ 0 → (∀ (x y : ℝ), P ↑x ↑y) → ∀ (x y : EReal), P x y
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.instConcreteCategoryMonoidHomCarrier.eq_1 : MonCat.instConcreteCategoryMonoidHomCarrier =
  { hom := fun {X Y} => MonCat.Hom.hom', ofHom := fun {X Y} => MonCat.Hom.mk✝,
    hom_ofHom := @MonCat.instConcreteCategoryMonoidHomCarrier._proof_1,
    ofHom_hom := @MonCat.instConcreteCategoryMonoidHomCarrier._proof_2,
    id_apply := @MonCat.instConcreteCategoryMonoidHomCarrier._proof_3,
    comp_apply := @MonCat.instConcreteCategoryMonoidHomCarrier._proof_4 }
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKeyD_unitOfList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {l : List α}
  {k k' fallback : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (Std.ExtDHashMap.Const.unitOfList l).getKeyD k' fallback = k
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.isSFiniteKernel_prodMkRight_unit : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β},
  ProbabilityTheory.IsSFiniteKernel (ProbabilityTheory.Kernel.prodMkRight Unit κ) ↔ ProbabilityTheory.IsSFiniteKernel κ
-- Mathlib.Topology.Spectral.Hom
IsSpectralMap.mk : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
  Continuous f → (∀ ⦃s : Set β⦄, IsOpen s → IsCompact s → IsCompact (f ⁻¹' s)) → IsSpectralMap f
-- Init.Control.Except
/-- Returns the value `a` without throwing exceptions or having any other effect.
 -/
ExceptT.pure : {ε : Type u} → {m : Type u → Type v} → [Monad m] → {α : Type u} → α → ExceptT ε m α
-- Mathlib.Combinatorics.Matroid.Circuit
/-- **Alias** of `Matroid.IsCircuit.subset_closure_sdiff_singleton`. -/
Matroid.IsCircuit.subset_closure_diff_singleton : ∀ {α : Type u_1} {M : Matroid α} {C : Set α}, M.IsCircuit C → ∀ (e : α), C ⊆ M.closure (C \ {e})
-- Mathlib.Analysis.Calculus.FDeriv.Prod
hasStrictFDerivAt_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {ι : Type u_6} {F' : ι → Type u_7}
  [inst_1 : (i : ι) → NormedAddCommGroup (F' i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (F' i)] (i : ι) (f : (i : ι) → F' i),
  HasStrictFDerivAt (fun f => f i) (ContinuousLinearMap.proj i) f
-- Init.Data.String.Termination
String.Pos.prev_induction : ∀ {s : String} {C : s.Pos → Prop} (p : s.Pos),
  (∀ (x : s.Pos) (h : x ≠ s.startPos), C (x.prev h) → C x) → C s.startPos → C p
-- Mathlib.LinearAlgebra.Dual.Lemmas
/-- Taking duals distributes over products.  -/
Module.dualProdDualEquivDual : (R : Type u_1) →
  (M : Type u_3) →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          (M' : Type u_4) →
            [inst_3 : AddCommMonoid M'] →
              [inst_4 : Module R M'] → (Module.Dual R M × Module.Dual R M') ≃ₗ[R] Module.Dual R (M × M')
-- Mathlib.Topology.Separation.Basic
R1Space.mk : ∀ {X : Type u_3} [inst : TopologicalSpace X], (∀ (x y : X), x ⤳ y ∨ Disjoint (nhds x) (nhds y)) → R1Space X
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.any_eq_true_iff_exists_contains_get : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  {p : (a : α) → β a → Bool}, m.WF → (m.any p = true ↔ ∃ a, ∃ (h : m.contains a = true), p a (m.get a h) = true)
-- Init.Data.List.Attach
List.unattach_flatten : ∀ {α : Type u_1} {p : α → Prop} {l : List (List { x // p x })}, l.flatten.unattach = (List.map List.unattach l).flatten
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.numbering.go : List Lean.Doc.Parser.OrderedListType → Lean.Parser.ParserFn
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.or_comm : ∀ {σs : List (Type u)} {P Q : Std.Do.SPred σs}, P ∨ Q ⊣⊢ₛ Q ∨ P
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.get.eq_def : ∀ {α : Type u} {β : Type v} [inst : BEq α] (a : α) (x : Std.DHashMap.Internal.AssocList α fun x => β)
  (x_1 : Std.DHashMap.Internal.AssocList.contains a x = true),
  Std.DHashMap.Internal.AssocList.get a x x_1 =
    match x, x_1 with
    | Std.DHashMap.Internal.AssocList.cons k v es, h =>
      if hka : (k == a) = true then v else Std.DHashMap.Internal.AssocList.get a es ⋯
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
OpenPartialHomeomorph.lift_openEmbedding_trans_apply : ∀ {X : Type u_7} {X' : Type u_8} {Z : Type u_9} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace X']
  [inst_2 : TopologicalSpace Z] [inst_3 : Nonempty Z] {f : X → X'} (e e' : OpenPartialHomeomorph X Z)
  (hf : Topology.IsOpenEmbedding f) (z : Z),
  ↑((e.lift_openEmbedding hf).symm.trans (e'.lift_openEmbedding hf)) z = ↑(e.symm.trans e') z
-- Mathlib.Order.DirSupClosed
dirSupClosedOn_Iic : ∀ {α : Type u_1} {D : Set (Set α)} [inst : Preorder α] (a : α), DirSupClosedOn D (Set.Iic a)
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.inner_rightAngleRotation_right : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) (x y : E), inner ℝ x (o.rightAngleRotation y) = -(o.areaForm x) y
-- Mathlib.MeasureTheory.Measure.Haar.OfBasis
Module.Basis.addHaar_self : ∀ {ι : Type u_1} {E : Type u_3} [inst : Fintype ι] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] (b : Module.Basis ι ℝ E), b.addHaar (parallelepiped ⇑b) = 1
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.t'_fst_fst_snd_assoc : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g]
  (i j k : 𝒰.I₀) {Z_1 : AlgebraicGeometry.Scheme} (h : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j k)
          (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j i))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pullback.fst
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f j) f) g) (𝒰.f j))
            (𝒰.f k))
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (𝒰.f j) f) g) h))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j)
        (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i k))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) (𝒰.f i))
          (𝒰.f j))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) h))