mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.minD_le_minD_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  (t.erase k).isEmpty = false → ∀ {fallback : α}, (cmp (t.minD fallback) ((t.erase k).minD fallback)).isLE = true
-- Mathlib.Analysis.Normed.Module.WeakDual
WeakDual.toStrongDual_extendRCLikeL_apply : ∀ {𝕜 : Type u_5} {F : Type u_7} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [inst_3 : TopologicalSpace F] [inst_4 : ContinuousConstSMul 𝕜 F] [inst_5 : Module ℝ F] [inst_6 : IsScalarTower ℝ 𝕜 F]
  (f : WeakDual ℝ F), WeakDual.toStrongDual (WeakDual.extendRCLikeL f) = StrongDual.extendRCLikeₗ f
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.lt_upperBound? : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x y z : α} {t : RBTree.RBSet α cmp} [Std.TransCmp cmp],
  t.upperBound? x = some y → z ∈ t → (cmp z y = Ordering.lt ↔ cmp z x = Ordering.lt)
-- Mathlib.Analysis.Convex.Side
Function.Injective.sSameSide_map_iff : ∀ {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [inst : CommRing R]
  [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V]
  [inst_5 : AddTorsor V P] [inst_6 : AddCommGroup V'] [inst_7 : Module R V'] [inst_8 : AddTorsor V' P']
  {s : AffineSubspace R P} {x y : P} {f : P →ᵃ[R] P'},
  Function.Injective ⇑f → ((AffineSubspace.map f s).SSameSide (f x) (f y) ↔ s.SSameSide x y)
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.get.eq_1 : ∀ {α : Type u} {β : Type v} [inst : BEq α] (a k : α) (v : β) (es : Std.DHashMap.Internal.AssocList α fun x => β)
  (h : Std.DHashMap.Internal.AssocList.contains a (Std.DHashMap.Internal.AssocList.cons k v es) = true),
  Std.DHashMap.Internal.AssocList.get a (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.MeasureTheory.Function.LpSpace.Indicator
MeasureTheory.norm_indicatorConstLp_top : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  {s : Set α} {hs : MeasurableSet s} {hμs : μ s ≠ ⊤} {c : E},
  μ s ≠ 0 → ‖MeasureTheory.indicatorConstLp ⊤ hs hμs c‖ = ‖c‖
-- Mathlib.Order.Interval.Set.OrdConnected
Set.ordConnected_iff_uIcc_subset : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α},
  s.OrdConnected ↔ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → Set.uIcc x y ⊆ s
-- Mathlib.Algebra.Ring.Submonoid.Pointwise
/-- A `MulOneClass` structure on additive submonoids of a (possibly, non-associative) semiring.  -/
AddSubmonoid.mulOneClass : {R : Type u_2} → [inst : NonAssocSemiring R] → MulOneClass (AddSubmonoid R)
-- Init.Data.Option.Lemmas
Option.eq_some_of_isSome : ∀ {α : Type u_1} {o : Option α} (h : o.isSome = true), o = some (o.get h)
-- Mathlib.AlgebraicGeometry.Morphisms.Affine
/-- [Stacks Tag 01QF](https://stacks.math.columbia.edu/tag/01QF) -/
AlgebraicGeometry.isAffine_of_isAffineOpen_basicOpen : ∀ {X : AlgebraicGeometry.Scheme} (s : Set ↑(X.presheaf.obj (Opposite.op ⊤))),
  Ideal.span s = ⊤ → (∀ i ∈ s, AlgebraicGeometry.IsAffineOpen (X.basicOpen i)) → AlgebraicGeometry.IsAffine X
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toList_roc_eq_none_iff : ∀ {m n i : ℕ}, (m<...=n).toList[i]? = none ↔ n ≤ i + m
-- Lean.Meta.LetToHave
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.State : Type
-- Mathlib.Order.Interval.Set.ProjIcc
Set.IciExtend_coe : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] {a : α} (f : ↑(Set.Ici a) → β) (x : ↑(Set.Ici a)),
  Set.IciExtend f ↑x = f x
-- Mathlib.FieldTheory.IsAlgClosed.Spectrum
/-- A specialization of `spectrum.subset_polynomial_aeval` to monic monomials for convenience.  -/
spectrum.pow_image_subset : ∀ {𝕜 : Type u} {A : Type v} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] (a : A) (n : ℕ),
  (fun x => x ^ n) '' spectrum 𝕜 a ⊆ spectrum 𝕜 (a ^ n)
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.instFaithfulKaroubiToKaroubi : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C], (CategoryTheory.Idempotents.toKaroubi C).Faithful
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.coe_inj : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : Zero R] {x y : R}, ↑x = ↑y ↔ x = y
-- Mathlib.Algebra.Group.Action.Defs
IsCancelSMul.right_cancel' : ∀ {G : Type u_9} {P : Type u_10} {inst : SMul G P} [self : IsCancelSMul G P] (a b : G) (c : P), a • c = b • c → a = b
-- Mathlib.Data.Finset.Card
Finset.card_le_four : ∀ {α : Type u_1} [inst : DecidableEq α] {a b c d : α}, {a, b, c, d}.card ≤ 4
-- Init.Sym.Lemmas
Lean.Sym.BitVec.le_eq_true : ∀ {n : ℕ} (a b : BitVec n), decide (a ≤ b) = true → (a ≤ b) = True
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.lintegral_withDensity_eq_lintegral_mul₀ : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  AEMeasurable f μ → ∀ {g : α → ENNReal}, AEMeasurable g μ → ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ
-- Mathlib.Order.Category.PartOrd
/-- The ulift functor `PartOrd.{u} ⥤ PartOrd.{max u v}`.  -/
PartOrd.uliftFunctor : CategoryTheory.Functor PartOrd PartOrd
-- Mathlib.Algebra.Homology.HomotopyCategory
HomotopyCategory.eq_of_homotopy : ∀ {ι : Type u_2} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} (f g : C ⟶ D) (h : Homotopy f g),
  (HomotopyCategory.quotient V c).map f = (HomotopyCategory.quotient V c).map g
-- Mathlib.RingTheory.OreLocalization.Basic
/-- Auxiliary definition for addition on the Ore localization, with one argument fixed.  -/
_private.Mathlib.RingTheory.OreLocalization.Basic.0.OreLocalization.add' : {R : Type u_1} →
  [inst : Monoid R] →
    {S : Submonoid R} →
      [inst_1 : OreLocalization.OreSet S] →
        {X : Type u_2} →
          [inst_2 : AddMonoid X] → [inst_3 : DistribMulAction R X] → X → ↥S → OreLocalization S X → OreLocalization S X
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.nodal_monic : ∀ {R : Type u_1} [inst : CommRing R] {ι : Type u_2} {s : Finset ι} {v : ι → R}, (Lagrange.nodal s v).Monic
-- Mathlib.RingTheory.Localization.Ideal
/-- The prime spectrum of the localization of a ring at a submonoid `M` are in
order-preserving bijection with subset of the prime spectrum of the ring consisting of
prime ideals disjoint from `M`.  -/
IsLocalization.primeSpectrumOrderIso : {R : Type u_1} →
  [inst : CommSemiring R] →
    (M : Submonoid R) →
      (S : Type u_2) →
        [inst_1 : CommSemiring S] →
          [inst_2 : Algebra R S] → [IsLocalization M S] → PrimeSpectrum S ≃o { p // Disjoint ↑M ↑p.asIdeal }
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.productTriangle_obj₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] {J : Type u_1}
  (T : J → CategoryTheory.Pretriangulated.Triangle C) [inst_2 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₁]
  [inst_3 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₂]
  [inst_4 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₃]
  [inst_5 : CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁],
  (CategoryTheory.Pretriangulated.productTriangle T).obj₂ = ∏ᶜ fun j => (T j).obj₂
-- Mathlib.Algebra.BigOperators.Intervals
Finset.prod_Ico_div : ∀ {M : Type u_4} (f : ℕ → M) {m n : ℕ} [inst : CommGroup M], m ≤ n → ∏ i ∈ Finset.Ico m n, f (i + 1) / f i = f n / f m
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Pretopology.toGrothendieck_toCoverage : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  (J : CategoryTheory.Pretopology C), J.toCoverage.toGrothendieck = J.toGrothendieck
-- Mathlib.LinearAlgebra.Prod
LinearMap.prodMap_one : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂], LinearMap.prodMap 1 1 = 1
-- Mathlib.Order.Nucleus
/-- A nucleus is idempotent.

Do not use this directly. Instead use `NucleusClass.idempotent`.  -/
Nucleus.idempotent' : ∀ {X : Type u_2} [inst : SemilatticeInf X] (self : Nucleus X) (x : X), self.toFun (self.toFun x) ≤ self.toFun x
-- Mathlib.Order.CompleteLattice.Defs
/-- Every set has a greatest lower bound.  -/
CompleteSemilatticeInf.isGLB_sInf : ∀ {α : Type u_8} [self : CompleteSemilatticeInf α] (s : Set α), IsGLB s (sInf s)
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsFundamentalDomain.integral_eq_tsum : ∀ {G : Type u_1} {α : Type u_3} {E : Type u_5} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α]
  [inst_3 : NormedAddCommGroup E] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableConstSMul G α]
  [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] [inst_7 : NormedSpace ℝ E],
  MeasureTheory.IsFundamentalDomain G s μ →
    ∀ (f : α → E), MeasureTheory.Integrable f μ → ∫ (x : α), f x ∂μ = ∑' (g : G), ∫ (x : α) in g • s, f x ∂μ
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.FullyFaithful.mapAddGrp.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {F : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] (hF : F.FullyFaithful),
  hF.mapAddGrp =
    { preimage := fun {X Y} f => CategoryTheory.AddGrp.homMk' (hF.mapAddMon.preimage f.hom), map_preimage := ⋯,
      preimage_map := ⋯ }
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.rank_one : ∀ {n : Type un} {R : Type uR} [inst : Fintype n] [inst_1 : CommSemiring R] [inst_2 : DecidableEq n]
  [StrongRankCondition R], Matrix.rank 1 = Fintype.card n
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- Left map, from `J.L` to `C`  -/
CategoryTheory.Limits.MultispanIndex.left : {J : CategoryTheory.Limits.MultispanShape} →
  {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Limits.MultispanIndex J C → J.L → C
-- Init.Data.Nat.Lemmas
Nat.pow_self_pos : ∀ {n : ℕ}, 0 < n ^ n
-- Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
MeasureTheory.eLpNorm_sub_le' : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} [inst : NormedAddCommGroup E] {μ : MeasureTheory.Measure α}
  {f g : α → E},
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable g μ →
      ∀ (p : ENNReal),
        MeasureTheory.eLpNorm (f - g) p μ ≤ p.LpAddConst * (MeasureTheory.eLpNorm f p μ + MeasureTheory.eLpNorm g p μ)
-- Lean.Util.CollectMVars
Lean.CollectMVars.visit : Lean.Expr → Lean.CollectMVars.Visitor
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.length_toList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α], (↑m).WF → (Std.DHashMap.Raw.Const.toList ↑m).length = (↑m).size
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get?_emptyc : ∀ {α : Type u} {cmp : α → α → Ordering} {a : α}, ∅.get? a = none
-- Init.WFTactics
/-- Variant of `decreasing_trivial` that does not use `omega`, intended to be used in core modules
before `omega` is available.
 -/
tacticDecreasing_trivial_pre_omega : Lean.ParserDescr
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.sum_neg : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Preorder M] [IsOrderedCancelAddMonoid M] {f : ι → M}
  {s : Finset ι} [AddLeftStrictMono M], (∀ i ∈ s, f i < 0) → s.Nonempty → ∑ i ∈ s, f i < 0
-- Mathlib.Analysis.Complex.Basic
Complex.uniformContinuous_im : UniformContinuous Complex.im
-- Mathlib.Order.Interval.Set.ProjIcc
Set.IicExtend.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] {b : α} (f : ↑(Set.Iic b) → β),
  Set.IicExtend f = f ∘ Set.projIic b
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
CategoryTheory.LaxFunctor.map₂_rightUnitor_hom : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.LaxFunctor B C) {a b : B} (f : a ⟶ b),
  (CategoryTheory.Bicategory.rightUnitor (F.map f)).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapId b))
      (CategoryTheory.CategoryStruct.comp (F.mapComp f (CategoryTheory.CategoryStruct.id b))
        (F.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom))
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_map_of_preserves : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (J : Type w) [inst_2 : LinearOrder J] [inst_3 : SuccOrder J] [inst_4 : OrderBot J] [inst_5 : WellFoundedLT J]
  (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesWellOrderContinuousOfShape J G] {X Y : C} (f : X ⟶ Y)
  {P : CategoryTheory.MorphismProperty D} [CategoryTheory.Limits.PreservesColimitsOfShape J G],
  (P.inverseImage G).transfiniteCompositionsOfShape J f → P.transfiniteCompositionsOfShape J (G.map f)
-- Mathlib.Topology.Sheaves.LocalPredicate
/-- The sheaf of continuous functions on `X` with values in a space `T`.
 -/
TopCat.sheafToTop : {X : TopCat} → TopCat → TopCat.Sheaf (Type u_2) X
-- Lean.Parser.Command
/-- `set_option <id> <value>` sets the option `<id>` to `<value>`. Depending on the type of the option,
the value can be `true`, `false`, a string, or a numeral. Options are used to configure behavior of
Lean as well as user-defined extensions. The setting is active until the end of the current `section`
or `namespace` or the end of the file.
Auto-completion is available for `<id>` to list available options.

`set_option <id> <value> in <command>` sets the option for just a single command:
```
set_option pp.all true in
#check 1 + 1
```
Similarly, `set_option <id> <value> in` can also be used inside terms and tactics to set an option
only in a single term or tactic.
 -/
Lean.Parser.Command.set_option : Lean.Parser.Parser
-- Mathlib.FieldTheory.RatFunc.Defs
/-- `RatFunc K` is `K(X)`, the field of rational functions over `K`.

The inclusion of polynomials into `RatFunc` is `algebraMap K[X] K⟮X⟯`,
the maps between `K⟮X⟯` and another field of fractions of `K[X]`,
especially `FractionRing K[X]`, are given by `IsLocalization.algEquiv`.
 -/
RatFunc : (K : Type u) → [CommRing K] → Type u
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.IsPresentation.mk : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] {solution : relations.Solution M},
  Function.Bijective ⇑solution.fromQuotient → solution.IsPresentation
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
/-- Evaluates expressions of the form `a ^ b` when `a` and `b` are both reals.
Works if `a`, `b`, and `a ^ b` are in fact rational numbers,
except for the case `a < 0`, `b` isn't integer.

TODO: simplify terms like  `(-a : ℝ) ^ (b / 3 : ℝ)` and `(-a : ℝ) ^ (b / 2 : ℝ)` too,
possibly after first considering changing the junk value.  -/
Mathlib.Meta.NormNum.evalRPow : Mathlib.Meta.NormNum.NormNumExt
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get?_eq_some_get!_of_contains : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  [inst_4 : Inhabited α], m.WF → ∀ {a : α}, m.contains a = true → m.get? a = some (m.get! a)
-- Mathlib.Algebra.Category.Semigrp.Basic
AddSemigrp.ofHom_apply : ∀ {X Y : Type u} [inst : AddSemigroup X] [inst_1 : AddSemigroup Y] (f : X →ₙ+ Y) (x : X),
  (CategoryTheory.ConcreteCategory.hom (AddSemigrp.ofHom f)) x = f x
-- Aesop.RuleTac.Cases
Aesop.CasesTarget'.decl.sizeOf_spec : ∀ (decl : Lean.Name), sizeOf (Aesop.CasesTarget'.decl decl) = 1 + sizeOf decl
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.fst_intCast : ∀ {R : Type u} {M : Type v} [inst : AddGroupWithOne R] [inst_1 : AddGroup M] (z : ℤ), (↑z).fst = ↑z
-- Mathlib.Order.SuccPred.Basic
Order.pred_lt_iff : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {a b : α} [NoMinOrder α], Order.pred b < a ↔ b ≤ a
-- Init.SizeOfLemmas
UInt8.sizeOf : ∀ (a : UInt8), sizeOf a = a.toNat + 3
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- If A ≠ B and C ≠ B then ∠ABC = π if and only if (dist A C) = (dist A B) + (dist B C).  -/
EuclideanGeometry.dist_eq_add_dist_iff_angle_eq_pi : ∀ {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},
  p₁ ≠ p₂ → p₃ ≠ p₂ → (dist p₁ p₃ = dist p₁ p₂ + dist p₃ p₂ ↔ EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi)
-- Mathlib.Data.ENNReal.Operations
ENNReal.mul_right_inj : ∀ {a b c : ENNReal}, a ≠ 0 → a ≠ ⊤ → (a * b = a * c ↔ b = c)
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.associatorNatIsoMiddleCat_hom_toNatTrans_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) (h : c ⟶ d)
  (X : ↑(CategoryTheory.Cat.of (b ⟶ c))),
  (CategoryTheory.Bicategory.associatorNatIsoMiddleCat f h).hom.toNatTrans.app X =
    (CategoryTheory.Bicategory.associator f X h).hom
-- Mathlib.GroupTheory.GroupAction.SubMulAction
/-- Multiplication by a scalar on an element of the set remains in the set.  -/
SMulMemClass.smul_mem : ∀ {S : Type u_1} {R : outParam (Type u_2)} {M : Type u_3} {inst : SMul R M} {inst_1 : SetLike S M}
  [self : SMulMemClass S R M] {s : S} (r : R) {m : M}, m ∈ s → r • m ∈ s
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.natDegree_U_natCast : ∀ (R : Type u_1) [inst : CommRing R] [IsDomain R] [NeZero 2] (n : ℕ), (Polynomial.Chebyshev.U R ↑n).natDegree = n
-- Init.System.IO
/-- The stream should be attached to a pipe.  -/
IO.Process.Stdio.piped : IO.Process.Stdio
-- Init.Data.BitVec.Lemmas
BitVec.eq_of_zero_length : ∀ {w : ℕ}, w = 0 → ∀ {x y : BitVec w}, x = y
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem?_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false → (t.insertMany l)[k]? = t[k]?
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.glue.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (sz : ℕ) (k : α) (v : β k) (l' r' : Std.DTreeMap.Internal.Impl α β)
  (motive :
    (r : Std.DTreeMap.Internal.Impl α β) →
      r.Balanced →
        Std.DTreeMap.Internal.Impl.BalancedAtRoot (Std.DTreeMap.Internal.Impl.inner sz k v l' r').size r.size →
          Sort u_3)
  (hr : Std.DTreeMap.Internal.Impl.leaf.Balanced)
  (hlr :
    Std.DTreeMap.Internal.Impl.BalancedAtRoot (Std.DTreeMap.Internal.Impl.inner sz k v l' r').size
      Std.DTreeMap.Internal.Impl.leaf.size)
  (h_1 :
    (hr : Std.DTreeMap.Internal.Impl.leaf.Balanced) →
      (hlr :
          Std.DTreeMap.Internal.Impl.BalancedAtRoot (Std.DTreeMap.Internal.Impl.inner sz k v l' r').size
            Std.DTreeMap.Internal.Impl.leaf.size) →
        motive Std.DTreeMap.Internal.Impl.leaf hr hlr)
  (h_2 :
    (sz' : ℕ) →
      (k' : α) →
        (v' : β k') →
          (l'' r'' : Std.DTreeMap.Internal.Impl α β) →
            (hr : (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'').Balanced) →
              (hlr :
                  Std.DTreeMap.Internal.Impl.BalancedAtRoot (Std.DTreeMap.Internal.Impl.inner sz k v l' r').size
                    (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'').size) →
                motive (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'') hr hlr),
  (match Std.DTreeMap.Internal.Impl.leaf, hr, hlr with
    | Std.DTreeMap.Internal.Impl.leaf, hr, hlr => h_1 hr hlr
    | Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'', hr, hlr => h_2 sz' k' v' l'' r'' hr hlr) =
    h_1 hr hlr
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- The cokernel of a zero morphism is an isomorphism  -/
CategoryTheory.Limits.cokernel.π_of_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f : X ⟶ Y} [inst_2 : CategoryTheory.Limits.HasCokernel f],
  f = 0 → CategoryTheory.IsIso (CategoryTheory.Limits.cokernel.π f)
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTranspose_inv_intCast_smul : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [inst : DivisionRing R] [inst_1 : AddCommGroup α]
  [inst_2 : StarAddMonoid α] [inst_3 : Module R α] (c : ℤ) (M : Matrix m n α),
  ((↑c)⁻¹ • M).conjTranspose = (↑c)⁻¹ • M.conjTranspose
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.skeleton.eq_1 : ∀ (X : SSet), X.skeleton = { toFun := fun n => ⨆ i, ⨆ x, SSet.Subcomplex.ofSimplex ↑x, monotone' := ⋯ }
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.linearIndependent_cols_iff_isUnit : ∀ {m : Type u} [inst : DecidableEq m] {K : Type u_3} [inst_1 : Field K] [inst_2 : Fintype m] {A : Matrix m m K},
  LinearIndependent K A.col ↔ IsUnit A
-- Mathlib.Data.Complex.Basic
Complex.ofReal_ne_zero : ∀ {z : ℝ}, ↑z ≠ 0 ↔ z ≠ 0
-- Mathlib.Data.Finsupp.Order
Finsupp.embDomain_lt_embDomain_iff_lt : ∀ {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [inst : Zero α] [inst_1 : Preorder α] (f : ι ↪ κ) (g₁ g₂ : ι →₀ α),
  Finsupp.embDomain f g₁ < Finsupp.embDomain f g₂ ↔ g₁ < g₂
-- Mathlib.CategoryTheory.Shift.Basic
/-- compatibility with the associativity  -/
CategoryTheory.ShiftMkCore.assoc_hom_app_assoc : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
  (self : CategoryTheory.ShiftMkCore C A) (m₁ m₂ m₃ : A) (X : C) {Z : C}
  (h : (self.F m₃).obj ((self.F m₂).obj ((self.F m₁).obj X)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((self.add (m₁ + m₂) m₃).hom.app X)
      (CategoryTheory.CategoryStruct.comp ((self.F m₃).map ((self.add m₁ m₂).hom.app X)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp ((self.add m₁ (m₂ + m₃)).hom.app X)
        (CategoryTheory.CategoryStruct.comp ((self.add m₂ m₃).hom.app ((self.F m₁).obj X)) h))
-- Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
CliffordAlgebra.EquivEven.e0_mul_v_mul_e0 : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (m : M),
  CliffordAlgebra.EquivEven.e0 Q * (CliffordAlgebra.EquivEven.v Q) m * CliffordAlgebra.EquivEven.e0 Q =
    (CliffordAlgebra.EquivEven.v Q) m
-- Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
BoundedContinuousFunction.integrable : ∀ {X : Type u_1} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] (μ : MeasureTheory.Measure X) {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [OpensMeasurableSpace X] [SecondCountableTopology E] [inst_5 : MeasurableSpace E]
  [BorelSpace E] [MeasureTheory.IsFiniteMeasure μ] (f : BoundedContinuousFunction X E), MeasureTheory.Integrable (⇑f) μ
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.WithUpper.isOpen_def : ∀ {α : Type u_1} [inst : Preorder α] {s : Set (Topology.WithUpper α)},
  IsOpen s ↔ TopologicalSpace.IsOpen (⇑Topology.WithUpper.toUpper ⁻¹' s)
-- Std.Http.Data.Version
Std.Http.Version.noConfusionType : Sort v✝ → Std.Http.Version → Std.Http.Version → Sort v✝
-- Lean.Meta.Tactic.Grind.AC.Types
/-- State for all associative operators detected by `grind`.  -/
Lean.Meta.Grind.AC.State : Type
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.HasAffineProperty.eq_targetAffineLocally' : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  {Q : outParam AlgebraicGeometry.AffineTargetMorphismProperty} [self : AlgebraicGeometry.HasAffineProperty P Q],
  P = AlgebraicGeometry.targetAffineLocally Q
-- Mathlib.Algebra.Category.MonCat.Adjunctions
AddCommMonCat.free_map : ∀ {X Y : Type u} (f : X ⟶ Y),
  AddCommMonCat.free.map f =
    AddCommMonCat.ofHom (Finsupp.mapDomain.addMonoidHom ⇑(CategoryTheory.ConcreteCategory.hom f))