mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.UInt.Lemmas
UInt8.sub_le : ∀ {a b : UInt8}, b ≤ a → a - b ≤ a
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ElabSimpArgsResult.mk.inj : ∀ {ctx : Lean.Meta.Simp.Context} {simprocs : Lean.Meta.Simp.SimprocsArray}
  {simpArgs : Array (Lean.Syntax × Lean.Elab.Tactic.ElabSimpArgResult)} {ctx_1 : Lean.Meta.Simp.Context}
  {simprocs_1 : Lean.Meta.Simp.SimprocsArray} {simpArgs_1 : Array (Lean.Syntax × Lean.Elab.Tactic.ElabSimpArgResult)},
  { ctx := ctx, simprocs := simprocs, simpArgs := simpArgs } =
      { ctx := ctx_1, simprocs := simprocs_1, simpArgs := simpArgs_1 } →
    ctx = ctx_1 ∧ simprocs = simprocs_1 ∧ simpArgs = simpArgs_1
-- Lean.Meta.ExprLens
/-- Returns the number of binders above a given subexpr position.  -/
Lean.Core.numBinders : {M : Type → Type} → [Monad M] → [Lean.MonadError M] → Lean.SubExpr.Pos → Lean.Expr → M ℕ
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
/-- A bundled absolute value is an absolute value.  -/
AbsoluteValue.isAbsoluteValue : ∀ {S : Type u_5} [inst : Semiring S] [inst_1 : PartialOrder S] {R : Type u_6} [inst_2 : Semiring R]
  (abv : AbsoluteValue R S), IsAbsoluteValue ⇑abv
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.Indep.rankPos_of_nonempty : ∀ {α : Type u_1} {M : Matroid α} {I : Set α}, M.Indep I → I.Nonempty → M.RankPos
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.hausdorffMeasure_smul : ∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] {α : Type u_4}
  [inst_3 : SMul α X] [IsIsometricSMul α X] {d : ℝ} (c : α),
  (0 ≤ d ∨ Function.Surjective fun x => c • x) →
    ∀ (s : Set X), (MeasureTheory.Measure.hausdorffMeasure d) (c • s) = (MeasureTheory.Measure.hausdorffMeasure d) s
-- Mathlib.Analysis.Meromorphic.Basic
MeromorphicAt.update : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : DecidableEq 𝕜] {f : 𝕜 → E} {z : 𝕜},
  MeromorphicAt f z → ∀ (w : 𝕜) (e : E), MeromorphicAt (Function.update f w e) z
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey!_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {k : α} {f : β → β},
  (t.modify k f).isEmpty = false → (t.modify k f).minKey! = if cmp t.minKey! k = Ordering.eq then k else t.minKey!
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
CategoryTheory.Limits.inl_inl_pushoutAssoc_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Z₁ Z₂ : C} (g₁ : Z₁ ⟶ X₁) (g₂ : Z₁ ⟶ X₂)
  (g₃ : Z₂ ⟶ X₂) (g₄ : Z₂ ⟶ X₃) [inst_1 : CategoryTheory.Limits.HasPushout g₁ g₂]
  [inst_2 : CategoryTheory.Limits.HasPushout g₃ g₄]
  [inst_3 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂))
      g₄]
  [inst_4 :
    CategoryTheory.Limits.HasPushout g₁
      (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))]
  {Z : C}
  (h :
    CategoryTheory.Limits.pushout g₁ (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄)) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl g₁ g₂)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pushout.inl
          (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂)) g₄)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).hom h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pushout.inl g₁
        (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄)))
      h
-- Std.Time.DateTime.PlainDateTime
Std.Time.PlainDateTime.mk.sizeOf_spec : ∀ (date : Std.Time.PlainDate) (time : Std.Time.PlainTime),
  sizeOf { date := date, time := time } = 1 + sizeOf date + sizeOf time
-- Mathlib.Topology.EMetricSpace.Weak
WithBot.isOpenEmbedding_some : ∀ {α : Type u} [t : TopologicalSpace α] [inst : LinearOrder α] [inst_1 : OrderTopology α],
  Topology.IsOpenEmbedding WithBot.some
-- Mathlib.GroupTheory.Commutator.Basic
closureCommutatorRepresentatives.eq_1 : ∀ (G : Type u_1) [inst : Group G],
  closureCommutatorRepresentatives G =
    Subgroup.closure (Prod.fst '' commutatorRepresentatives G ∪ Prod.snd '' commutatorRepresentatives G)
-- Init.Grind.Ring.Basic
Lean.Grind.Ring.intCast_zero : ∀ {α : Type u} [inst : Lean.Grind.Ring α], ↑0 = 0
-- Std.Async.System
/-- Gets the current user by using `passwd`.

On Windows systems, `userId`, `groupId` and `shell` are set to none
 -/
Std.Async.System.getCurrentUser : IO Std.Async.System.SystemUser
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.Nonempty.of_smul_left : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] {s : Finset α} {t : Finset β},
  (s • t).Nonempty → s.Nonempty
-- Mathlib.Algebra.Group.Irreducible.Indecomposable
IsAddIndecomposable.baseOf_subset_pos : ∀ {ι : Type u_1} {M : Type u_2} {S : Type u_4} [inst : AddMonoid M] [inst_1 : LinearOrder S] [inst_2 : AddMonoid S]
  (v : ι → M) (f : M →+ S), IsAddIndecomposable.baseOf v f ⊆ {i | 0 < f (v i)}
-- Mathlib.Analysis.Complex.Basic
Filter.tendsto_ofReal_iff' : ∀ {α : Type u_2} {𝕜 : Type u_3} [inst : RCLike 𝕜] {l : Filter α} {f : α → ℝ} {x : ℝ},
  Filter.Tendsto (fun x => ↑(f x)) l (nhds ↑x) ↔ Filter.Tendsto f l (nhds x)
-- Mathlib.Order.SuccPred.Archimedean
lt_or_le_of_codirected : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] [IsSuccArchimedean α] {r v₁ v₂ : α},
  r ≤ v₁ → r ≤ v₂ → v₁ < v₂ ∨ v₂ ≤ v₁
-- Mathlib.SetTheory.Ordinal.FundamentalSequence
/-- A fundamental sequence for `o` is a strictly monotonic function `Iio o.cof.ord → Iio o` with
cofinal range. We provide `a = o.cof.ord` explicitly to avoid type rewrites.  -/
Ordinal.IsFundamentalSeq : {a o : Ordinal.{u_1}} → (↑(Set.Iio a) → ↑(Set.Iio o)) → Prop
-- Lean.Meta.Sym.Simp.SimpM
Lean.Meta.Sym.Simp.Result.rfl.injEq : ∀ (done contextDependent done_1 contextDependent_1 : Bool),
  (Lean.Meta.Sym.Simp.Result.rfl done contextDependent = Lean.Meta.Sym.Simp.Result.rfl done_1 contextDependent_1) =
    (done = done_1 ∧ contextDependent = contextDependent_1)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point.0.WeierstrassCurve.Affine.Point.toClass.match_1.eq_1 : ∀ {F : Type u_1} [inst : Field F] {W : WeierstrassCurve.Affine F} (motive : W.Point → Sort u_2)
  (h_1 : Unit → motive WeierstrassCurve.Affine.Point.zero)
  (h_2 : (x y : F) → (h : W.Nonsingular x y) → motive (WeierstrassCurve.Affine.Point.some x y h)),
  (match WeierstrassCurve.Affine.Point.zero with
    | WeierstrassCurve.Affine.Point.zero => h_1 ()
    | WeierstrassCurve.Affine.Point.some x y h => h_2 x y h) =
    h_1 ()
-- Mathlib.Order.Types.Defs
OrderType.lift_type_eq_iff : ∀ {α β : Type u} [inst : LinearOrder α] [inst_1 : LinearOrder β],
  OrderType.lift.{u_1, u} (OrderType.type α) = OrderType.lift.{u_1, u} (OrderType.type β) ↔ Nonempty (α ≃o β)
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.primitiveCharacter_apply_of_isCoprime : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) {a : ℤ},
  IsCoprime a ↑n → χ.primitiveCharacter ↑a = χ ↑a
-- Mathlib.Topology.Category.TopPair
TopPair.proj₁AdjDiag_unit_app : ∀ (X : TopPair),
  TopPair.proj₁AdjDiag.unit.app X = TopPair.ofHom (CategoryTheory.CategoryStruct.id TopPair.fst) TopPair.map ⋯
-- Lean.Data.Json.Elab
/-- Json array syntax.  -/
Lean.Json.«json[_]» : Lean.ParserDescr
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.adjoin_insert_adjoin : ∀ (R : Type uR) {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (s : Set A) (x : A),
  Algebra.adjoin R (insert x ↑(Algebra.adjoin R s)) = Algebra.adjoin R (insert x s)
-- Mathlib.Algebra.Category.Grp.Limits
/-- A choice of limit cone for a functor into `GrpCat`.
(Generally, you'll just want to use `limit F`.)  -/
GrpCat.limitCone : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J GrpCat) →
      [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget GrpCat)).sections] → CategoryTheory.Limits.Cone F
-- Mathlib.Analysis.MeanInequalities
/-- For `1 ≤ p`, the `p`-th power of the sum of `f i` is bounded above by a constant times the
sum of the `p`-th powers of `f i`. Version for sums over finite sets, with nonnegative `ℝ`-valued
functions.  -/
Real.rpow_sum_le_const_mul_sum_rpow_of_nonneg : ∀ {ι : Type u} (s : Finset ι) {f : ι → ℝ} {p : ℝ},
  1 ≤ p → (∀ i ∈ s, 0 ≤ f i) → (∑ i ∈ s, f i) ^ p ≤ ↑s.card ^ (p - 1) * ∑ i ∈ s, f i ^ p
-- Mathlib.AlgebraicGeometry.Geometrically.Integral
AlgebraicGeometry.instSurjectiveOfGeometricallyIntegral : ∀ {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.GeometricallyIntegral f],
  AlgebraicGeometry.Surjective f
-- Init.Data.String.PosRaw
String.Pos.Raw.byteIdx_add_string : ∀ {p : String.Pos.Raw} {s : String}, (p + s).byteIdx = p.byteIdx + s.utf8ByteSize
-- Lean.Setup
Lean.ModuleSetup.mk : Lean.Name →
  Option Lean.PkgId →
    Bool →
      Option (Array Lean.Import) →
        Lean.NameMap Lean.ImportArtifacts →
          Array System.FilePath → Array Lean.Plugin → Lean.LeanOptions → Lean.ModuleSetup
-- Mathlib.CategoryTheory.WithTerminal.Cone
instHasColimitsOfShapeUnderOfWithInitial : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  (X : C) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.WithInitial J) C],
  CategoryTheory.Limits.HasColimitsOfShape J (CategoryTheory.Under X)
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
/-- Curried `C^n` functions are `C^n` in the first coordinate.  -/
ContMDiffAt.curry_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {F : Type u_8}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_9} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {n : WithTop ℕ∞} {f : M → M' → N} {x : M} {y : M'},
  ContMDiffAt (I.prod I') J n (Function.uncurry f) (x, y) → ContMDiffAt I J n (fun x => f x y) x
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.degree_zero : ∀ {R : Type u_1} [inst : Semiring R], LaurentPolynomial.degree 0 = ⊥
-- Std.Tactic.BVDecide.LRAT.Internal.CompactLRATCheckerSound
_private.Std.Tactic.BVDecide.LRAT.Internal.CompactLRATCheckerSound.0.Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker.go.match_1.splitter : {n : ℕ} →
  (motive : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n × Bool → Sort u_1) →
    (x : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n × Bool) →
      ((fst : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) →
          (checkSuccess : Bool) → motive (fst, checkSuccess)) →
        motive x
-- Mathlib.Data.PNat.Factors
PNat.factorMultiset.eq_1 : ∀ (n : ℕ+), n.factorMultiset = PrimeMultiset.ofNatList (↑n).primeFactorsList ⋯
-- Mathlib.CategoryTheory.Bicategory.Functor.Cat.ObjectProperty
CategoryTheory.Pseudofunctor.ObjectProperty.map_map_hom : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat}
  (P : F.ObjectProperty) [inst_1 : P.IsClosedUnderMapObj] {X Y : B} (f : X ⟶ Y) {X_1 Y_1 : P.Obj X} (f_1 : X_1 ⟶ Y_1),
  ((P.map f).map f_1).hom = (F.map f).toFunctor.map f_1.hom
-- Mathlib.Condensed.TopComparison
ContinuousMap.comp.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] (f : C(β, γ)) (g : C(α, β)), f.comp g = { toFun := ⇑f ∘ ⇑g, continuous_toFun := ⋯ }
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.map_inf_comap_of_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] {f : F},
  Function.Surjective ⇑f → ∀ (S T : Submonoid N), Submonoid.map f (Submonoid.comap f S ⊓ Submonoid.comap f T) = S ⊓ T
-- Mathlib.Analysis.CStarAlgebra.Module.Defs
CStarModule.inner_zero_left : ∀ {A : Type u_1} {E : Type u_2} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : AddCommGroup E]
  [inst_3 : Module ℂ A] [inst_4 : Module ℂ E] [inst_5 : PartialOrder A] [inst_6 : SMul A E] [inst_7 : Norm A]
  [inst_8 : Norm E] [inst_9 : CStarModule A E] [StarModule ℂ A] {x : E}, inner A 0 x = 0
-- Lean.Parser.Extension
Lean.Parser.parserAliases2infoRef : IO.Ref (Lean.NameMap Lean.Parser.ParserAliasInfo)
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.mem_comap : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N]
  {S : L.Substructure N} {f : L.Hom M N} {x : M}, x ∈ FirstOrder.Language.Substructure.comap f S ↔ f x ∈ S
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.BindStruct.hf : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Presieve X}
  {R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → CategoryTheory.Presieve Y} {Z : C} {h : Z ⟶ X} (self : S.BindStruct R h), S self.f
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- The sine of an angle in a right-angled triangle multiplied by the hypotenuse equals the
opposite side.  -/
EuclideanGeometry.sin_oangle_right_mul_dist_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P},
  EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) → (EuclideanGeometry.oangle p₂ p₃ p₁).sin * dist p₁ p₃ = dist p₁ p₂
-- Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
Algebra.Generators.compLocalizationAwayAlgHom_relation_eq_zero : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} {ι : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T] (g : S) [inst_7 : IsLocalization.Away g T] (P : Algebra.Generators R S ι),
  (Algebra.Generators.compLocalizationAwayAlgHom T g P)
      ((MvPolynomial.rename Sum.inr) (P.σ g) * MvPolynomial.X (Sum.inl ()) - 1) =
    0
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
/-- The adjunction between n-truncation and the n-coskeleton.  -/
SSet.coskAdj : (n : ℕ) → SSet.truncation n ⊣ SSet.Truncated.cosk n
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.d_fst_v' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] (i j : ℤ) (hij : i + 1 = j),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone φ).d (i - 1) i)
      ((↑(CochainComplex.mappingCone.fst φ)).v i j hij) =
    -CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCone.fst φ)).v (i - 1) i ⋯) (F.d i j)
-- Mathlib.Analysis.Normed.Group.Basic
enorm_ne_zero : ∀ {E : Type u_8} [inst : TopologicalSpace E] [inst_1 : ENormedAddMonoid E] {a : E}, ‖a‖ₑ ≠ 0 ↔ a ≠ 0
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.AddGrp.Hom.hom_add : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {G H : CategoryTheory.AddGrp C}
  [inst_3 : CategoryTheory.IsCommAddMonObj H.X] (f g : G ⟶ H), (f + g).hom = f.hom + g.hom
-- Init.Data.Int.DivMod.Lemmas
Int.fmod_eq_emod : ∀ {a b : ℤ}, a.fmod b = a % b + if 0 ≤ b ∨ b ∣ a then 0 else b
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.toLinearEquiv : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : Semiring S] →
        {σ : R →+* S} →
          {σ' : S →+* R} →
            [inst_2 : RingHomInvPair σ σ'] →
              [inst_3 : RingHomInvPair σ' σ] →
                {M : Type u_3} →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : AddCommMonoid M] →
                      {M₂ : Type u_4} →
                        [inst_6 : TopologicalSpace M₂] →
                          [inst_7 : AddCommMonoid M₂] →
                            [inst_8 : Module R M] → [inst_9 : Module S M₂] → (M ≃SL[σ] M₂) → M ≃ₛₗ[σ] M₂
-- ProofWidgets.Component.Basic
ProofWidgets.MarkdownDisplay.Props.mk : String → ProofWidgets.MarkdownDisplay.Props
-- Std.Http.Protocol.H1.Reader
Std.Http.Protocol.H1.Reader.State.complete.sizeOf_spec : ∀ {dir : Std.Http.Protocol.H1.Direction}, sizeOf Std.Http.Protocol.H1.Reader.State.complete = 1
-- Mathlib.CategoryTheory.Sites.Sieves
/-- Given a presieve on `X`, we can define a presieve on `F(X)` (which is actually a sieve)
by taking the sieve generated by the image via `F`.
 -/
CategoryTheory.Presieve.functorPushforward : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) → {X : C} → CategoryTheory.Presieve X → CategoryTheory.Presieve (F.obj X)
-- Mathlib.AlgebraicTopology.SimplexCategory.Defs
SimplexCategory.Truncated.Hom.tr_id : ∀ {n : ℕ} (a : SimplexCategory) (ha : autoParam (a.len ≤ n) SimplexCategory.Truncated.Hom.tr_id._auto_1),
  SimplexCategory.Truncated.Hom.tr (CategoryTheory.CategoryStruct.id a) ha ha =
    CategoryTheory.CategoryStruct.id { obj := a, property := ha }
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.densityProcess_empty : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] (κ : ProbabilityTheory.Kernel α (γ × β))
  (ν : ProbabilityTheory.Kernel α γ) (n : ℕ) (a : α) (x : γ), κ.densityProcess ν n a x ∅ = 0
-- Mathlib.Order.Filter.Lift
Filter.lift_principal2 : ∀ {α : Type u_1} {f : Filter α}, f.lift Filter.principal = f
-- Lean.Elab.InfoTree.Types
Lean.Elab.FVarAliasInfo.mk : Lean.Name → Lean.FVarId → Lean.FVarId → Lean.Elab.FVarAliasInfo
-- Mathlib.Order.Iterate
Monotone.seq_pos_lt_seq_of_le_of_lt : ∀ {α : Type u_1} [inst : Preorder α] {f : α → α} {x y : ℕ → α},
  Monotone f →
    ∀ {n : ℕ}, 0 < n → x 0 ≤ y 0 → (∀ k < n, x (k + 1) ≤ f (x k)) → (∀ k < n, f (y k) < y (k + 1)) → x n < y n
-- Mathlib.Algebra.Group.Commute.Defs
Commute.pow_pow_self : ∀ {M : Type u_2} [inst : Monoid M] (a : M) (m n : ℕ), Commute (a ^ m) (a ^ n)
-- Init.Data.Int.Order
Int.natAbs_eq_iff : ∀ {a : ℤ} {n : ℕ}, a.natAbs = n ↔ a = ↑n ∨ a = -↑n
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂.whiskerLeft.inj : ∀ {e : Lean.Expr} {isoLift? : Option Mathlib.Tactic.BicategoryLike.IsoLift} {f g h : Mathlib.Tactic.BicategoryLike.Mor₁}
  {η : Mathlib.Tactic.BicategoryLike.Mor₂} {e_1 : Lean.Expr} {isoLift?_1 : Option Mathlib.Tactic.BicategoryLike.IsoLift}
  {f_1 g_1 h_1 : Mathlib.Tactic.BicategoryLike.Mor₁} {η_1 : Mathlib.Tactic.BicategoryLike.Mor₂},
  Mathlib.Tactic.BicategoryLike.Mor₂.whiskerLeft e isoLift? f g h η =
      Mathlib.Tactic.BicategoryLike.Mor₂.whiskerLeft e_1 isoLift?_1 f_1 g_1 h_1 η_1 →
    e = e_1 ∧ isoLift? = isoLift?_1 ∧ f = f_1 ∧ g = g_1 ∧ h = h_1 ∧ η = η_1
-- Std.Data.DHashMap.Internal.Model
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.filterₘ : {α : Type u} →
  {β : α → Type v} → Std.DHashMap.Internal.Raw₀ α β → ((a : α) → β a → Bool) → Std.DHashMap.Internal.Raw₀ α β
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.setToL1'.congr_simp : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} (𝕜 : Type u_6) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_4 : NormedRing 𝕜] [inst_5 : Module 𝕜 E] [inst_6 : Module 𝕜 F] [inst_7 : IsBoundedSMul 𝕜 E]
  [inst_8 : IsBoundedSMul 𝕜 F] [inst_9 : CompleteSpace F] {T T_1 : Set α → E →L[ℝ] F} (e_T : T = T_1) {C C_1 : ℝ}
  (e_C : C = C_1) (hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
  (h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x),
  MeasureTheory.L1.setToL1' 𝕜 hT h_smul = MeasureTheory.L1.setToL1' 𝕜 ⋯ ⋯
-- Mathlib.LinearAlgebra.RootSystem.CartanMatrix
RootPairing.Base.cartanMatrixIn_mul_diagonal_eq : ∀ {ι : 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] (S : Type u_5) [inst_5 : CommRing S]
  [inst_6 : Algebra S R] {P : RootPairing ι R M N} [inst_7 : P.IsRootSystem] [inst_8 : P.IsValuedIn S]
  (B : P.InvariantForm) (b : P.Base) [inst_9 : DecidableEq ι],
  ((RootPairing.Base.cartanMatrixIn S b).map ⇑(algebraMap S R) *
      Matrix.diagonal fun i => (B.form (P.root ↑i)) (P.root ↑i)) =
    2 • (LinearMap.BilinForm.toMatrix b.toWeightBasis) B.form
-- Aesop.RuleSet
Aesop.LocalRuleSet.forwardRulePatternSubstsInLocalDecl : Aesop.LocalRuleSet → Lean.LocalDecl → Aesop.BaseM (Array (Aesop.ForwardRule × Aesop.Substitution))
-- Mathlib.Algebra.Ring.Hom.Defs
RingHom.coe_inj : ∀ {α : Type u_2} {β : Type u_3} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} ⦃f g : α →+* β⦄, ⇑f = ⇑g → f = g
-- Mathlib.Order.OmegaCompletePartialOrder
/-- See note [partially-applied ext lemmas].  -/
OmegaCompletePartialOrder.Chain.ext : ∀ {α : Type u_2} [inst : Preorder α] ⦃f g : OmegaCompletePartialOrder.Chain α⦄, ⇑f = ⇑g → f = g
-- Mathlib.Data.Int.Basic
Int.strongRec.eq_1 : ∀ {m : ℤ} {motive : ℤ → Sort u_1} (lt : (n : ℤ) → n < m → motive n)
  (ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → motive k) → motive n) (n : ℤ),
  Int.strongRec lt ge n =
    if hnm : n < m then lt n hnm
    else
      ge n ⋯
        (Int.inductionOn' (motive := fun x => (k : ℤ) → k < x → motive k) n m lt
          (fun _n a ih l a_1 => if hlm : l < m then lt l hlm else ge l ⋯ fun k x => ih k ⋯) fun n x hn l x_1 => hn l ⋯)
-- Mathlib.Order.Defs.PartialOrder
/-- `CovBy a b` means that `b` covers `a`. This means that `a < b` and there is no element in
between. This is denoted `a ⋖ b`.  -/
CovBy : {α : Type u_2} → [LT α] → α → α → Prop
-- Mathlib.Data.Nat.BinaryRec
Nat.log2_eq_succ_log2_shiftRight : ∀ {n : ℕ}, n >>> 1 ≠ 0 → n.log2 = (n >>> 1).log2.succ
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
/-- Alternative formulation of `covariant_sequence_exact₃`  -/
CategoryTheory.Abelian.Ext.covariant_sequence_exact₃' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] (X : C) {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (n₀ n₁ : ℕ)
  (h : n₀ + 1 = n₁),
  { X₁ := AddCommGrpCat.of (CategoryTheory.Abelian.Ext X S.X₂ n₀),
      X₂ := AddCommGrpCat.of (CategoryTheory.Abelian.Ext X S.X₃ n₀),
      X₃ := AddCommGrpCat.of (CategoryTheory.Abelian.Ext X S.X₁ n₁),
      f := AddCommGrpCat.ofHom ((CategoryTheory.Abelian.Ext.mk₀ S.g).postcomp X ⋯),
      g := AddCommGrpCat.ofHom (hS.extClass.postcomp X h), zero := ⋯ }.Exact