mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
CategoryTheory.whiskerRight_ι_colimitCompWhiskeringRightIsoColimitComp_inv_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  {J : Type u_4} [inst_3 : CategoryTheory.Category.{v_4, u_4} J] [inst_4 : CategoryTheory.Limits.HasColimitsOfShape J D]
  (F : CategoryTheory.Functor D E) [inst_5 : CategoryTheory.Limits.PreservesColimitsOfShape J F]
  (G : CategoryTheory.Functor J (CategoryTheory.Functor C D)) (j : J) {Z : CategoryTheory.Functor C E}
  (h : CategoryTheory.Limits.colimit (G.comp ((CategoryTheory.Functor.whiskeringRight C D E).obj F)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.Limits.colimit.ι G j) F)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.colimitCompWhiskeringRightIsoColimitComp F G).inv h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι (G.comp ((CategoryTheory.Functor.whiskeringRight C D E).obj F)) j) h
-- Mathlib.CategoryTheory.Category.Cat.Limit
CategoryTheory.Cat.HasLimits.comp_def : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CategoryTheory.Cat)
  {X Y Z : CategoryTheory.Limits.limit (F.comp CategoryTheory.Cat.objects)}
  (f : CategoryTheory.Limits.limit (CategoryTheory.Cat.HasLimits.homDiagram X Y))
  (g : CategoryTheory.Limits.limit (CategoryTheory.Cat.HasLimits.homDiagram Y Z)),
  CategoryTheory.CategoryStruct.comp f g =
    CategoryTheory.Limits.Types.Limit.mk (CategoryTheory.Cat.HasLimits.homDiagram X Z)
      (fun j =>
        CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.ConcreteCategory.hom
              (CategoryTheory.Limits.limit.π (CategoryTheory.Cat.HasLimits.homDiagram X Y) j))
            f)
          ((CategoryTheory.ConcreteCategory.hom
              (CategoryTheory.Limits.limit.π (CategoryTheory.Cat.HasLimits.homDiagram Y Z) j))
            g))
      ⋯
-- Mathlib.Algebra.Field.TransferInstance
/-- Transfer `Field` across an `Equiv`  -/
Equiv.field : {α : Type u_1} → {β : Type u_2} → α ≃ β → [Field β] → Field α
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.π_comp_H0Iso_hom : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.CategoryStruct.comp (groupHomology.π A 0) (groupHomology.H0Iso A).hom =
    CategoryTheory.CategoryStruct.comp (groupHomology.cyclesIso₀ A).hom ((Rep.coinvariantsMk k G).app A)
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
SSet.RelativeMorphism.Homotopy.ext : ∀ {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} {f g : SSet.RelativeMorphism A B φ}
  {x y : f.Homotopy g}, x.h = y.h → x = y
-- Mathlib.Data.Set.Prod
Set.graphOn_empty : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), Set.graphOn f ∅ = ∅
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.isPWO_iUnion_support_prod_mul : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} {β : Type u_6} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ]
  [inst_2 : IsOrderedCancelAddMonoid Γ] [inst_3 : Semiring R] {s : α → HahnSeries Γ R} {t : β → HahnSeries Γ R},
  (⋃ a, (s a).support).IsPWO → (⋃ b, (t b).support).IsPWO → (⋃ a, ((fun a => s a.1 * t a.2) a).support).IsPWO
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalCategory.tensorμ_natural_left_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X₁ X₂ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (Z₁ Z₂ : C) {Z : C}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₁ Z₁)
        (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₂ Z₂) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ f₂)
        (CategoryTheory.MonoidalCategoryStruct.tensorObj Z₁ Z₂))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ Y₁ Y₂ Z₁ Z₂) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ X₁ X₂ Z₁ Z₂)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f₁ Z₁)
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight f₂ Z₂))
        h)
-- Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
cyclotomicCharacter.toFun.congr_simp : ∀ {L : Type u} [inst : CommRing L] [inst_1 : IsDomain L] (p : ℕ) [inst_2 : Fact (Nat.Prime p)] (g g_1 : L ≃+* L),
  g = g_1 → cyclotomicCharacter.toFun p g = cyclotomicCharacter.toFun p g_1
-- Mathlib.Algebra.Order.Ring.Archimedean
_private.Mathlib.Algebra.Order.Ring.Archimedean.0.ArchimedeanClass.mk_mul_le_of_le : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : CommRing R] [inst_2 : IsStrictOrderedRing R] {x₁ y₁ x₂ y₂ : R},
  ArchimedeanClass.mk x₁ ≤ ArchimedeanClass.mk x₂ →
    ArchimedeanClass.mk y₁ ≤ ArchimedeanClass.mk y₂ → ArchimedeanClass.mk (x₁ * y₁) ≤ ArchimedeanClass.mk (x₂ * y₂)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.uniqueHomToTrivial.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (A : CategoryTheory.Grp C),
  A.uniqueHomToTrivial =
    (have this := CategoryTheory.InducedCategory.homEquiv;
      this).unique
-- Mathlib.Analysis.Calculus.FDeriv.Prod
fderivWithin_snd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {p : E × F}
  {s : Set (E × F)}, UniqueDiffWithinAt 𝕜 s p → fderivWithin 𝕜 Prod.snd s p = ContinuousLinearMap.snd 𝕜 E F
-- Mathlib.ModelTheory.Algebra.Field.Basic
_private.Mathlib.ModelTheory.Algebra.Field.Basic.0.FirstOrder.Field.FieldAxiom.toSentence.match_1.eq_9 : ∀ (motive : FirstOrder.Field.FieldAxiom → Sort u_1) (h_1 : Unit → motive FirstOrder.Field.FieldAxiom.addAssoc)
  (h_2 : Unit → motive FirstOrder.Field.FieldAxiom.zeroAdd)
  (h_3 : Unit → motive FirstOrder.Field.FieldAxiom.negAddCancel)
  (h_4 : Unit → motive FirstOrder.Field.FieldAxiom.mulAssoc) (h_5 : Unit → motive FirstOrder.Field.FieldAxiom.mulComm)
  (h_6 : Unit → motive FirstOrder.Field.FieldAxiom.oneMul) (h_7 : Unit → motive FirstOrder.Field.FieldAxiom.existsInv)
  (h_8 : Unit → motive FirstOrder.Field.FieldAxiom.leftDistrib)
  (h_9 : Unit → motive FirstOrder.Field.FieldAxiom.existsPairNE),
  (match FirstOrder.Field.FieldAxiom.existsPairNE with
    | FirstOrder.Field.FieldAxiom.addAssoc => h_1 ()
    | FirstOrder.Field.FieldAxiom.zeroAdd => h_2 ()
    | FirstOrder.Field.FieldAxiom.negAddCancel => h_3 ()
    | FirstOrder.Field.FieldAxiom.mulAssoc => h_4 ()
    | FirstOrder.Field.FieldAxiom.mulComm => h_5 ()
    | FirstOrder.Field.FieldAxiom.oneMul => h_6 ()
    | FirstOrder.Field.FieldAxiom.existsInv => h_7 ()
    | FirstOrder.Field.FieldAxiom.leftDistrib => h_8 ()
    | FirstOrder.Field.FieldAxiom.existsPairNE => h_9 ()) =
    h_9 ()
-- Mathlib.Topology.Algebra.Module.Basic
Submodule.isOpenQuotientMap_mkQ : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : TopologicalSpace M] (S : Submodule R M) [ContinuousAdd M], IsOpenQuotientMap ⇑S.mkQ
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.valuation_lt_symm_orderMonoidIso : ∀ {R : Type u_2} {Γ : Type u_3} [inst : Ring R] [inst_1 : ValuativeRel R] [inst_2 : LinearOrderedCommGroupWithZero Γ]
  (v : Valuation R Γ) [inst_3 : v.Compatible] (γ : (MonoidWithZeroHom.ofClass v).ValueGroup₀) (x : R),
  (ValuativeRel.valuation R) x < (ValuativeRel.ValueGroupWithZero.orderMonoidIso v).symm γ ↔ v.restrict x < γ
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.attachCodeDecls.go.eq_def : ∀ {pu : Lean.Compiler.LCNF.Purity} (decls : Array (Lean.Compiler.LCNF.CodeDecl pu)) (i : ℕ)
  (code : Lean.Compiler.LCNF.Code pu),
  Lean.Compiler.LCNF.attachCodeDecls.go✝ decls i code =
    if i > 0 then
      match decls[i - 1]! with
      | Lean.Compiler.LCNF.CodeDecl.let decl =>
        Lean.Compiler.LCNF.attachCodeDecls.go✝ decls (i - 1) (Lean.Compiler.LCNF.Code.let decl code)
      | Lean.Compiler.LCNF.CodeDecl.fun decl h =>
        Lean.Compiler.LCNF.attachCodeDecls.go✝ decls (i - 1) (Lean.Compiler.LCNF.Code.fun decl code h)
      | Lean.Compiler.LCNF.CodeDecl.jp decl =>
        Lean.Compiler.LCNF.attachCodeDecls.go✝ decls (i - 1) (Lean.Compiler.LCNF.Code.jp decl code)
      | Lean.Compiler.LCNF.CodeDecl.oset fvarId idx y h =>
        Lean.Compiler.LCNF.attachCodeDecls.go✝ decls (i - 1) (Lean.Compiler.LCNF.Code.oset fvarId idx y code h)
      | Lean.Compiler.LCNF.CodeDecl.uset fvarId idx y h =>
        Lean.Compiler.LCNF.attachCodeDecls.go✝ decls (i - 1) (Lean.Compiler.LCNF.Code.uset fvarId idx y code h)
      | Lean.Compiler.LCNF.CodeDecl.sset fvarId idx offset y ty h =>
        Lean.Compiler.LCNF.attachCodeDecls.go✝ decls (i - 1)
          (Lean.Compiler.LCNF.Code.sset fvarId idx offset y ty code h)
      | Lean.Compiler.LCNF.CodeDecl.setTag fvarId cidx h =>
        Lean.Compiler.LCNF.attachCodeDecls.go✝ decls (i - 1) (Lean.Compiler.LCNF.Code.setTag fvarId cidx code h)
      | Lean.Compiler.LCNF.CodeDecl.inc fvarId n check persistent h =>
        Lean.Compiler.LCNF.attachCodeDecls.go✝ decls (i - 1)
          (Lean.Compiler.LCNF.Code.inc fvarId n check persistent code h)
      | Lean.Compiler.LCNF.CodeDecl.dec fvarId n check persistent objs? h =>
        Lean.Compiler.LCNF.attachCodeDecls.go✝ decls (i - 1)
          (Lean.Compiler.LCNF.Code.dec fvarId n check persistent objs? code h)
      | Lean.Compiler.LCNF.CodeDecl.del fvarId h =>
        Lean.Compiler.LCNF.attachCodeDecls.go✝ decls (i - 1) (Lean.Compiler.LCNF.Code.del fvarId code h)
    else code
-- Mathlib.Data.Int.GCD
Nat.exists_mul_mod_eq_gcd : ∀ {k n : ℕ}, n.gcd k < k → ∃ m < k, n * m % k = n.gcd k
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- Continuity from above: the measure of the intersection of an increasing sequence of measurable
sets is the limit of the measures.  -/
MeasureTheory.tendsto_measure_iInter_atBot : ∀ {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : Preorder ι]
  [Filter.atBot.IsCountablyGenerated] {s : ι → Set α},
  (∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ) →
    Monotone s → (∃ i, μ (s i) ≠ ⊤) → Filter.Tendsto (⇑μ ∘ s) Filter.atBot (nhds (μ (⋂ n, s n)))
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.upperCrossingTime_le_lowerCrossingTime : ∀ {Ω : Type u_1} {ι : Type u_2} [inst : ConditionallyCompleteLinearOrderBot ι] {a b : ℝ} {f : ι → Ω → ℝ} {N : ι} {n : ℕ}
  {ω : Ω}, MeasureTheory.upperCrossingTime a b f N n ω ≤ MeasureTheory.lowerCrossingTime a b f N n ω
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getKey!_alterKey : ∀ {α : Type u} [inst : BEq α] {β : Type v} [EquivBEq α] [inst_2 : Inhabited α] {k k' : α} {f : Option β → Option β}
  (l : List ((_ : α) × β)),
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getKey! k' (Std.Internal.List.Const.alterKey k f l) =
      if (k == k') = true then if (f (Std.Internal.List.getValue? k l)).isSome = true then k else default
      else Std.Internal.List.getKey! k' l
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.simplicialToCosimplicialAugmented_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (X : (CategoryTheory.SimplicialObject.Augmented C)ᵒᵖ),
  (CategoryTheory.simplicialToCosimplicialAugmented C).obj X = (Opposite.unop X).rightOp
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Matrix.isHyperbolic_conj_iff : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : Preorder R] {m : Matrix (Fin 2) (Fin 2) R} (g : GL (Fin 2) R),
  (↑g * m * (↑g)⁻¹).IsHyperbolic ↔ m.IsHyperbolic
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
_private.Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctorNatTransOfLE.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b),
  CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctorNatTransOfLE✝ t a b h =
    CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctorNatTransOfLE✝ t a b h
-- Mathlib.Order.Filter.Pointwise
/-- `Filter α` is a `Monoid` under pointwise operations if `α` is.  -/
Filter.monoid : {α : Type u_2} → [Monoid α] → Monoid (Filter α)
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.X.instDecidableEq : {q : ℕ} → DecidableEq (LucasLehmer.X q)
-- Mathlib.RingTheory.Extension.Cotangent.Free
/-- To show a pre-submersive presentation with kernel `I = (fᵢ)` is submersive, it suffices to show
that the images of the `fᵢ` form a basis of `I/I²` and that the restricted
cotangent complex `I/I² → S ⊗[R] (Ω[R[Xᵢ]⁄R]) = ⊕ᵢ S → ⊕ⱼ S` is bijective.  -/
Algebra.PreSubmersivePresentation.isUnit_jacobian_of_cotangentRestrict_bijective : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type u_3}
  {σ : Type u_4} (P : Algebra.PreSubmersivePresentation R S ι σ) [inst_3 : Finite σ]
  (b : Module.Basis σ S P.toExtension.Cotangent),
  (∀ (r : σ), b r = Algebra.Extension.Cotangent.mk ⟨P.relation r, ⋯⟩) →
    Function.Bijective ⇑(P.cotangentRestrict ⋯) → IsUnit P.jacobian
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.liftIco.eq_1 : ∀ {𝕜 : Type u_1} {B : Type u_2} [inst : AddCommGroup 𝕜] (p : 𝕜) [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  [hp : Fact (0 < p)] (a : 𝕜) [inst_3 : Archimedean 𝕜] (f : 𝕜 → B),
  AddCircle.liftIco p a f = (Set.Ico a (a + p)).domRestrict f ∘ ⇑(AddCircle.equivIco p a)
-- Mathlib.Algebra.Lie.Weights.Linear
LieModule.weightSpace.congr_simp : ∀ {R : Type u_2} {L : Type u_3} (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  (χ χ_1 : L → R), χ = χ_1 → LieModule.weightSpace M χ = LieModule.weightSpace M χ_1
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.core : Lean.Expr →
  Lean.Meta.Grind.Arith.Linear.LinExpr →
    Lean.Meta.Grind.Arith.Linear.LinExpr → Lean.Meta.Grind.Arith.Linear.IneqCnstrProof
-- Init.Data.List.Monadic
List.flatMapM_nil : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] {f : α → m (List β)},
  List.flatMapM f [] = pure []
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomMulAct.instR0Space : ∀ {M : Type u_1} [inst : TopologicalSpace M] [R0Space M], R0Space Mᵈᵐᵃ
-- Mathlib.Order.Lattice
sup_sup_sup_comm : ∀ {α : Type u} [inst : SemilatticeSup α] (a b c d : α), a ⊔ b ⊔ (c ⊔ d) = a ⊔ c ⊔ (b ⊔ d)
-- Init.Data.Int.DivMod.Lemmas
Int.eq_tdiv_of_mul_eq_right : ∀ {a b c : ℤ}, a ≠ 0 → a * b = c → b = c.tdiv a
-- Init.Data.SInt.Lemmas
Int8.toNatClampNeg_ofIntLE : ∀ {n : ℤ} (h₁ : Int8.minValue.toInt ≤ n) (h₂ : n ≤ Int8.maxValue.toInt), (Int8.ofIntLE n h₁ h₂).toNatClampNeg = n.toNat
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.disjUnion_tag_of_mem_right : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.TaggedPrepartition I}
  (h : Disjoint π₁.iUnion π₂.iUnion), J ∈ π₂ → (π₁.disjUnion π₂ h).tag J = π₂.tag J
-- Mathlib.Algebra.Category.ModuleCat.Semi
/-- Reinterpreting a linear map in the category of `R`-modules  -/
SemimoduleCat.«term↟_» : Lean.ParserDescr
-- Lean.Server.References
/-- Gets the direct imports of `mod`.
The current imports in a file worker take precedence over those in .ilean files.
 -/
Lean.Server.References.getDirectImports? : Lean.Server.References → Lean.Name → Option Lean.Server.DirectImports
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
/-- The action of `torsion K` on `integerSet K`.  -/
NumberField.mixedEmbedding.fundamentalCone.integerSetTorsionSMul : {K : Type u_1} →
  [inst : Field K] →
    [inst_1 : NumberField K] →
      SMul ↥(NumberField.Units.torsion K) ↑(NumberField.mixedEmbedding.fundamentalCone.integerSet K)
-- Mathlib.Topology.Order.ScottTopology
Topology.IsScott.monotone_of_continuous : ∀ {α : Type u_1} {β : Type u_2} {D : Set (Set α)} [inst : Preorder α] [inst_1 : TopologicalSpace α]
  [inst_2 : Preorder β] [inst_3 : TopologicalSpace β] [Topology.IsScott β Set.univ] {f : α → β} [Topology.IsScott α D],
  Continuous f → Monotone f
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.Equiv.symm : ∀ {α : Type u} {m₁ m₂ : Std.HashSet.Raw α}, m₁.Equiv m₂ → m₂.Equiv m₁
-- Mathlib.Algebra.BigOperators.Group.List.Defs
List.prod_induction : ∀ {M : Type u_2} [inst : Mul M] [inst_1 : One M] {l : List M} (p : M → Prop),
  (∀ (a b : M), p a → p b → p (a * b)) → p 1 → (∀ x ∈ l, p x) → p l.prod
-- Mathlib.CategoryTheory.ConcreteCategory.Basic
CategoryTheory.ConcreteCategory.coe_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {X Y Z : C}
  (f : X ⟶ Y) (g : Y ⟶ Z),
  ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) =
    ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM0to1.tr.match_1.congr_eq_1 : ∀ {Γ : Type u_1} {Λ : Type u_2} (motive : Option (Λ × Turing.TM0.Stmt Γ) → Sort u_3)
  (x : Option (Λ × Turing.TM0.Stmt Γ)) (h_1 : Unit → motive none)
  (h_2 : (q' : Λ) → (s : Turing.TM0.Stmt Γ) → motive (some (q', s))),
  x = none →
    (match x with
      | none => h_1 ()
      | some (q', s) => h_2 q' s) ≍
      h_1 ()
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.setBlack.eq_1 : ∀ {α : Type u_1}, RBTree.RBNode.nil.setBlack = RBTree.RBNode.nil
-- Init.Data.SInt.Lemmas
Int32.sub_mul : ∀ {a b c : Int32}, (a - b) * c = a * c - b * c
-- Mathlib.MeasureTheory.Function.ConvergenceInDistribution
MeasureTheory.tendstoInDistribution_const : ∀ {ι : Type u_1} {E : Type u_2} {Ω' : Type u_3} {m' : MeasurableSpace Ω'} {μ' : MeasureTheory.Measure Ω'}
  [inst : MeasureTheory.IsProbabilityMeasure μ'] {mE : MeasurableSpace E} {Z : Ω' → E} {l : Filter ι}
  [inst_1 : TopologicalSpace E] [inst_2 : OpensMeasurableSpace E],
  AEMeasurable Z μ' → MeasureTheory.TendstoInDistribution (fun x => Z) l Z (fun x => μ') μ'
-- Lean.Elab.DeprecatedArg
Lean.Elab.linter.deprecated.arg : Lean.Option Bool
-- Lean.MetavarContext
/-- `MkBinding` and `elimMVarDepsAux` are mutually recursive, but `cache` is only used at `elimMVarDepsAux`.
We use a single state object for convenience.

We have a `NameGenerator` because we need to generate fresh auxiliary metavariables.  -/
Lean.MetavarContext.MkBinding.State : Type
-- Mathlib.Data.Finset.Insert
Finset.singleton_inj : ∀ {α : Type u_1} {a b : α}, {a} = {b} ↔ a = b
-- Mathlib.Analysis.InnerProductSpace.Continuous
DenseRange.eq_of_inner_left : ∀ {E : Type u_4} {ι : Type u_6} (𝕜 : Type u_7) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] {x y : E} {f : ι → E},
  DenseRange f → (∀ (i : ι), inner 𝕜 x (f i) = inner 𝕜 y (f i)) → x = y
-- Mathlib.MeasureTheory.Function.AEEqFun
/-- The `AddHom` from the group of continuous maps from `α` to `β` to the group of
equivalence classes of `μ`-almost-everywhere measurable functions.  -/
ContinuousMap.toAEEqFunAddHom : {α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] →
      (μ : MeasureTheory.Measure α) →
        [inst_1 : TopologicalSpace α] →
          [BorelSpace α] →
            [inst_3 : TopologicalSpace β] →
              [SecondCountableTopologyEither α β] →
                [TopologicalSpace.PseudoMetrizableSpace β] →
                  [inst_6 : AddGroup β] → [inst_7 : IsTopologicalAddGroup β] → C(α, β) →+ α →ₘ[μ] β
-- Mathlib.Combinatorics.Additive.Convolution
Finset.addConvolution_eq_zero : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] {A B : Finset G} {x : G},
  A.addConvolution B x = 0 ↔ x ∉ A + B
-- Init.SizeOf
Lean.Macro.Exception.unsupportedSyntax.sizeOf_spec : sizeOf Lean.Macro.Exception.unsupportedSyntax = 1
-- Mathlib.GroupTheory.Sylow
Sylow.mem_fixedPoints_mul_left_cosets_iff_mem_normalizer : ∀ {G : Type u} [inst : Group G] {H : Subgroup G} [Finite ↑↑H] {x : G},
  ↑x ∈ MulAction.fixedPoints (↥H) (G ⧸ H) ↔ x ∈ Subgroup.normalizer ↑H
-- Mathlib.GroupTheory.Coprod.Basic
MulEquiv.coprodComm.eq_1 : ∀ (M : Type u_1) (N : Type u_2) [inst : MulOneClass M] [inst_1 : MulOneClass N],
  MulEquiv.coprodComm M N = (Monoid.Coprod.swap M N).toMulEquiv (Monoid.Coprod.swap N M) ⋯ ⋯
-- Mathlib.Topology.Algebra.InfiniteSum.Ring
HasSum.mul_right : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : NonUnitalNonAssocSemiring α]
  [inst_1 : TopologicalSpace α] [IsTopologicalSemiring α] {f : ι → α} {a₁ : α} (a₂ : α),
  HasSum f a₁ L → HasSum (fun i => f i * a₂) (a₁ * a₂) L
-- Lean.Util.LeanOptions
/-- The option's value.  -/
Lean.LeanOption.value : Lean.LeanOption → Lean.LeanOptionValue
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
WithBot.coe_biSup : ∀ {ι : Type u_5} {s : Set ι},
  s.Nonempty → ∀ {α : Type u_6} [inst : CompleteLattice α] (f : ι → α), ↑(⨆ i ∈ s, f i) = ⨆ i ∈ s, ↑(f i)
-- Lean.Message
/-- A `SerialMessage` is a `Message` whose `MessageData` has been eagerly
serialized and is thus appropriate for use in pure contexts where the effectful
`MessageData.toString` cannot be used.  -/
Lean.SerialMessage : Type
-- Std.Sync.Semaphore
_private.Std.Sync.Semaphore.0.Std.SemaphoreState.mk.sizeOf_spec : ∀ (permits : ℕ) (waiters : Std.Queue (IO.Promise Unit)),
  sizeOf { permits := permits, waiters := waiters } = 1 + sizeOf permits + sizeOf waiters
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Projection
EuclideanGeometry.angle_orthogonalProjection_self : ∀ {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} {s : AffineSubspace ℝ P}
  [inst_4 : s.direction.HasOrthogonalProjection] (h : p' ∈ s),
  EuclideanGeometry.angle p' (↑((EuclideanGeometry.orthogonalProjection s) p)) p = Real.pi / 2
-- Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Algebra.TensorProduct.algEquivIncludeRange_symm_toAlgHom : ∀ (R : Type u_1) (S : Type u_2) (T : Type u_3) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  [inst_3 : CommSemiring T] [inst_4 : Algebra R T],
  ↑(Algebra.TensorProduct.algEquivIncludeRange R S T).symm =
    Algebra.TensorProduct.includeLeft.range.mulMap Algebra.TensorProduct.includeRight.range
-- Mathlib.Algebra.Algebra.Unitization
Unitization.lift_symm_apply : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A] {C : Type u_5} [inst_5 : Semiring C]
  [inst_6 : Algebra R C] (φ : Unitization R A →ₐ[R] C),
  Unitization.lift.symm φ = (NonUnitalAlgHomClass.toNonUnitalAlgHom φ).comp (Unitization.inrNonUnitalAlgHom R A)
-- Mathlib.Algebra.Order.Kleene
kstar_mul_kstar : ∀ {α : Type u_1} [inst : KleeneAlgebra α] (a : α), KStar.kstar a * KStar.kstar a = KStar.kstar a
-- Mathlib.Data.Rat.Cast.Defs
Rat.cast_divInt_of_ne_zero : ∀ {α : Type u_3} [inst : DivisionRing α] (a : ℤ) {b : ℤ}, ↑b ≠ 0 → ↑(Rat.divInt a b) = ↑a / ↑b
-- Mathlib.LinearAlgebra.Eigenspace.Basic
/-- All generalized eigenvalues are eigenvalues.  -/
Module.End.hasEigenvalue_of_hasGenEigenvalue : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R} {k : ℕ}, f.HasGenEigenvalue μ k → f.HasEigenvalue μ
-- Mathlib.GroupTheory.Congruence.Defs
conGen.eq_1 : ∀ {M : Type u_1} [inst : Mul M] (r : M → M → Prop), conGen r = { r := ConGen.Rel r, iseqv := ⋯, mul' := ⋯ }