mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Format.Basic
_private.Init.Data.Format.Basic.0.Std.Format.pushGroup : {m : Type → Type} →
  Std.Format.FlattenBehavior →
    List Std.Format.WorkItem✝ →
      List Std.Format.WorkGroup✝ → ℕ → [Monad m] → [Std.Format.MonadPrettyFormat m] → m (List Std.Format.WorkGroup✝)
-- Mathlib.Order.RelSeries
RelSeries.getLast_toList : ∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r), p.toList.getLast ⋯ = p.last
-- Mathlib.Analysis.Normed.Module.Ball.Action
isScalarTower_sphere_sphere_sphere : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : NormedField 𝕜']
  [inst_2 : SeminormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜' E] {r : ℝ}
  [inst_5 : NormedAlgebra 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' E],
  IsScalarTower ↑(Metric.sphere 0 1) ↑(Metric.sphere 0 1) ↑(Metric.sphere 0 r)
-- Mathlib.AlgebraicTopology.ModelCategory.Basic
HomotopicalAlgebra.ModelCategory.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (categoryWithFibrations :
        autoParam (HomotopicalAlgebra.CategoryWithFibrations C)
          HomotopicalAlgebra.ModelCategory.categoryWithFibrations._autoParam) →
      (categoryWithCofibrations :
          autoParam (HomotopicalAlgebra.CategoryWithCofibrations C)
            HomotopicalAlgebra.ModelCategory.categoryWithCofibrations._autoParam) →
        (categoryWithWeakEquivalences :
            autoParam (HomotopicalAlgebra.CategoryWithWeakEquivalences C)
              HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences._autoParam) →
          autoParam (CategoryTheory.Limits.HasFiniteLimits C) HomotopicalAlgebra.ModelCategory.cm1a._autoParam →
            autoParam (CategoryTheory.Limits.HasFiniteColimits C) HomotopicalAlgebra.ModelCategory.cm1b._autoParam →
              autoParam (HomotopicalAlgebra.weakEquivalences C).HasTwoOutOfThreeProperty
                  HomotopicalAlgebra.ModelCategory.cm2._autoParam →
                autoParam (HomotopicalAlgebra.weakEquivalences C).IsStableUnderRetracts
                    HomotopicalAlgebra.ModelCategory.cm3a._autoParam →
                  autoParam (HomotopicalAlgebra.fibrations C).IsStableUnderRetracts
                      HomotopicalAlgebra.ModelCategory.cm3b._autoParam →
                    autoParam (HomotopicalAlgebra.cofibrations C).IsStableUnderRetracts
                        HomotopicalAlgebra.ModelCategory.cm3c._autoParam →
                      autoParam
                          (∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [HomotopicalAlgebra.Cofibration i]
                            [HomotopicalAlgebra.WeakEquivalence i] [HomotopicalAlgebra.Fibration p],
                            CategoryTheory.HasLiftingProperty i p)
                          HomotopicalAlgebra.ModelCategory.cm4a._autoParam →
                        autoParam
                            (∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [HomotopicalAlgebra.Cofibration i]
                              [HomotopicalAlgebra.Fibration p] [HomotopicalAlgebra.WeakEquivalence p],
                              CategoryTheory.HasLiftingProperty i p)
                            HomotopicalAlgebra.ModelCategory.cm4b._autoParam →
                          autoParam
                              ((HomotopicalAlgebra.trivialCofibrations C).HasFactorization
                                (HomotopicalAlgebra.fibrations C))
                              HomotopicalAlgebra.ModelCategory.cm5a._autoParam →
                            autoParam
                                ((HomotopicalAlgebra.cofibrations C).HasFactorization
                                  (HomotopicalAlgebra.trivialFibrations C))
                                HomotopicalAlgebra.ModelCategory.cm5b._autoParam →
                              HomotopicalAlgebra.ModelCategory C
-- Mathlib.Data.DFinsupp.Encodable
instCountableDFinsupp : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] [Countable ι] [∀ (i : ι), Countable (α i)],
  Countable (Π₀ (i : ι), α i)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- **Alias** of `ValuativeRel.not_vlt_of_veq`. -/
ValuativeRel.veq.not_vlt : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x y : R}, x =ᵥ y → ¬x <ᵥ y
-- Mathlib.Combinatorics.Enumerative.Composition
/-- Equivalence between the disjoint union of the blocks (each of them seen as
`Fin (c.blocksFun i)`) with `Fin n`.  -/
Composition.blocksFinEquiv : {n : ℕ} → (c : Composition n) → (i : Fin c.length) × Fin (c.blocksFun i) ≃ Fin n
-- Lean.Meta.MethodSpecs
_private.Lean.Meta.MethodSpecs.0.Lean.MethodSpecTheorem.levelParams : Lean.MethodSpecTheorem✝ → List Lean.Name
-- Plausible.Testable
/-- Count the number of times the test procedure gave up.  -/
Plausible.giveUp : {p : Prop} → ℕ → Plausible.TestResult p → Plausible.TestResult p
-- Aesop.Stats.Basic
Aesop.RuleStatsTotals.mk.injEq : ∀ (numSuccessful numFailed : ℕ) (elapsedSuccessful elapsedFailed : Aesop.Nanos) (numSuccessful_1 numFailed_1 : ℕ)
  (elapsedSuccessful_1 elapsedFailed_1 : Aesop.Nanos),
  ({ numSuccessful := numSuccessful, numFailed := numFailed, elapsedSuccessful := elapsedSuccessful,
        elapsedFailed := elapsedFailed } =
      { numSuccessful := numSuccessful_1, numFailed := numFailed_1, elapsedSuccessful := elapsedSuccessful_1,
        elapsedFailed := elapsedFailed_1 }) =
    (numSuccessful = numSuccessful_1 ∧
      numFailed = numFailed_1 ∧ elapsedSuccessful = elapsedSuccessful_1 ∧ elapsedFailed = elapsedFailed_1)
-- Mathlib.Topology.MetricSpace.Isometry
IsometryClass.continuous : ∀ {F : Type u_1} {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : FunLike F α β] [IsometryClass F α β] (f : F), Continuous ⇑f
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKeyD_empty : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {a fallback : α}, ∅.getKeyD a fallback = fallback
-- Mathlib.Algebra.Order.Monovary
antivary_inv : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α]
  [inst_3 : CommGroup β] [inst_4 : PartialOrder β] [IsOrderedMonoid β] {f : ι → α} {g : ι → β},
  Antivary f⁻¹ g⁻¹ ↔ Antivary f g
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.structureInstances : Lean.Option Bool
-- Lean.Meta.Tactic.Grind.Types
/-- Returns the anchor references (if any) being used to restrict the search.  -/
Lean.Meta.Grind.getAnchorRefs : Lean.Meta.Grind.GrindM (Option (Array Lean.Meta.Grind.AnchorRef))
-- Mathlib.Algebra.CharP.Subring
CharP.subring' : ∀ (R : Type u) [inst : CommRing R] (p : ℕ) [CharP R p] (S : Subring R), CharP (↥S) p
-- Mathlib.Geometry.Convex.Cone.Face.Basic
/-- The projection of a face of a product cone onto the first component is a face of the
projection of the product cone onto the first component.  -/
PointedCone.IsFaceOf.fst : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : DivisionRing R] [inst_1 : LinearOrder R]
  [inst_2 : IsOrderedRing R] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : AddCommGroup N]
  [inst_6 : Module R N] {C₁ : PointedCone R M} {C₂ : PointedCone R N} {F : PointedCone R (M × N)},
  F.IsFaceOf (Submodule.prod C₁ C₂) → (PointedCone.map (LinearMap.fst R M N) F).IsFaceOf C₁
-- Init.Data.SInt.Lemmas
ISize.toInt64_lt : ∀ {a b : ISize}, a.toInt64 < b.toInt64 ↔ a < b
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_empty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {a : α}, ∅.getKey? a = none
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.measurableSet_support : ∀ {α : Type u_1} {β : Type u_2} [inst : Zero β] [inst_1 : MeasurableSpace α] (f : MeasureTheory.SimpleFunc α β),
  MeasurableSet (Function.support ⇑f)
-- Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
/-- The proximity function of a sum of functions at `⊤` is less than or equal to the sum of the
proximity functions of the summand, plus `log` of the number of summands.
 -/
ValueDistribution.proximity_sum_top_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {α : Type u_2} (s : Finset α) (f : α → ℂ → E),
  (∀ a ∈ s, Meromorphic (f a)) →
    ValueDistribution.proximity (∑ a ∈ s, f a) ⊤ ≤
      ∑ a ∈ s, ValueDistribution.proximity (f a) ⊤ + fun x => Real.log ↑s.card
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
AddMonoidHom.compLeftContinuousBounded_apply : ∀ {β : Type v} {γ : Type w} (α : Type u_3) [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
  [inst_2 : AddMonoid β] [inst_3 : BoundedAdd β] [inst_4 : ContinuousAdd β] [inst_5 : PseudoMetricSpace γ]
  [inst_6 : AddMonoid γ] [inst_7 : BoundedAdd γ] [inst_8 : ContinuousAdd γ] (g : β →+ γ) {C : NNReal}
  (hg : LipschitzWith C ⇑g) (f : BoundedContinuousFunction α β),
  (AddMonoidHom.compLeftContinuousBounded α g hg) f = BoundedContinuousFunction.comp (⇑g) hg f
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.leftKanExtensionUniqueOfIso_inv : ∀ {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') [inst_3 : F'.IsLeftKanExtension α] {G : CategoryTheory.Functor C H} (i : F ≅ G)
  (G' : CategoryTheory.Functor D H) (β : G ⟶ L.comp G') [inst_4 : G'.IsLeftKanExtension β],
  (F'.leftKanExtensionUniqueOfIso α i G' β).inv =
    G'.descOfIsLeftKanExtension β F' (CategoryTheory.CategoryStruct.comp i.inv α)
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.withDensity_apply_eq_zero : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} {s : Set α},
  Measurable f → ((μ.withDensity f) s = 0 ↔ μ ({x | f x ≠ 0} ∩ s) = 0)
-- Mathlib.Analysis.MeanInequalities
/-- **Young's inequality**, `ℝ≥0` version. We use `{p q : ℝ≥0}` in order to avoid constructing
witnesses of `0 ≤ p` and `0 ≤ q` for the denominators.  -/
NNReal.young_inequality : ∀ (a b : NNReal) {p q : NNReal}, p.HolderConjugate q → a * b ≤ a ^ ↑p / p + b ^ ↑q / q
-- Mathlib.Topology.Path
Path.truncate_const_continuous_family : ∀ {X : Type u_1} [inst : TopologicalSpace X] {a b : X} (γ : Path a b) (t : ℝ), Continuous ↿(γ.truncate t)
-- Mathlib.Combinatorics.Matroid.Sum
Matroid.disjointSigma_indep_iff : ∀ {α : Type u_1} {ι : Type u_2} {M : ι → Matroid α} {h : Pairwise (Function.onFun Disjoint fun i => (M i).E)}
  {I : Set α}, (Matroid.disjointSigma M h).Indep I ↔ (∀ (i : ι), (M i).Indep (I ∩ (M i).E)) ∧ I ⊆ ⋃ i, (M i).E
-- Mathlib.Data.Finset.Fold
Finset.fold_max_le : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {b : β} {s : Finset α} [inst : LinearOrder β] (c : β),
  Finset.fold max b f s ≤ c ↔ b ≤ c ∧ ∀ x ∈ s, f x ≤ c
-- Mathlib.Order.ModularLattice
/-- **Alias** of `inf_covBy_of_covBy_sup_of_covBy_sup_right`. -/
CovBy.inf_of_sup_of_sup_right : ∀ {α : Type u_1} [inst : Lattice α] [IsWeakLowerModularLattice α] {a b : α}, a ⋖ a ⊔ b → b ⋖ a ⊔ b → a ⊓ b ⋖ b
-- Init.Data.String.Lemmas.Pattern.TakeDrop.String
String.skipPrefix?_slice_of_isEmpty : ∀ {pat : String.Slice} {s : String}, pat.isEmpty = true → s.skipPrefix? pat = some s.startPos
-- Mathlib.Data.Quot
Quotient.choice_eq : ∀ {ι : Type u_3} {α : ι → Type u_4} {S : (i : ι) → Setoid (α i)} (f : (i : ι) → α i),
  (Quotient.choice fun i => ⟦f i⟧) = ⟦f⟧
-- Mathlib.RingTheory.Ideal.IsPrincipal
Ideal.associatesEquivIsPrincipal_apply : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] (x : R),
  ↑((Ideal.associatesEquivIsPrincipal R) (Associates.mk x)) = Ideal.span {x}
-- Mathlib.Tactic.TacticAnalysis.Declarations
_private.Mathlib.Tactic.TacticAnalysis.Declarations.0.Mathlib.TacticAnalysis.TerminalReplacementOutcome.error : Lean.TSyntax `tactic → Lean.MessageData → Mathlib.TacticAnalysis.TerminalReplacementOutcome✝
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.re_mul : ∀ {d : ℤ} (z w : ℤ√d), (z * w).re = z.re * w.re + d * z.im * w.im
-- Mathlib.Algebra.Homology.HomologicalComplex
ChainComplex.mk_d_2_1 : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (X₀ X₁ X₂ : V) (d₀ : X₁ ⟶ X₀) (d₁ : X₂ ⟶ X₁) (s : CategoryTheory.CategoryStruct.comp d₁ d₀ = 0)
  (succ :
    (S : CategoryTheory.ShortComplex V) →
      (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' CategoryTheory.CategoryStruct.comp d₂ S.f = 0),
  (ChainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ).d 2 1 = d₁
-- Mathlib.CategoryTheory.Preadditive.EndoFunctor
CategoryTheory.Endofunctor.algebraPreadditive_homGroup_add_f : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C]
  (F : CategoryTheory.Functor C C) [inst_2 : F.Additive] (A₁ A₂ : CategoryTheory.Endofunctor.Algebra F) (α β : A₁ ⟶ A₂),
  (α + β).f = α.f + β.f
-- Init.Control.Basic
/-- An `Alternative` functor is an `Applicative` functor that can "fail" or be "empty"
and a binary operation `<|>` that “collects values” or finds the “left-most success”.

Important instances include
* `Option`, where `failure := none` and `<|>` returns the left-most `some`.
* Parser combinators typically provide an `Applicative` instance for error-handling and
  backtracking.

Error recovery and state can interact subtly. For example, the implementation of `Alternative` for `OptionT (StateT σ Id)` keeps modifications made to the state while recovering from failure, while `StateT σ (OptionT Id)` discards them.
 -/
Alternative : (Type u → Type v) → Type (max (u + 1) v)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKeyD_inter_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k fallback : α}, k ∉ m₂ → (m₁ ∩ m₂).getKeyD k fallback = fallback
-- Lean.Meta.Sym.DSimp.DSimpM
Lean.Meta.Sym.DSimp.instInhabitedMethods.default : Lean.Meta.Sym.DSimp.Methods
-- Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
/-- If for any `g ∈ A` the integrals with respect to two finite measures `P, P'` coincide, then the
difference of the integrals of `mulExpNegMulSq ε ∘ g` with respect to `P, P'` is bounded by
`6 * √ε`.  -/
dist_integral_mulExpNegMulSq_comp_le : ∀ {ε : ℝ} {E : Type u_2} [inst : MeasurableSpace E] [inst_1 : PseudoEMetricSpace E] [BorelSpace E] [CompleteSpace E]
  [SecondCountableTopology E] {P P' : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure P]
  [MeasureTheory.IsFiniteMeasure P'] (f : BoundedContinuousFunction E ℝ)
  {A : Subalgebra ℝ (BoundedContinuousFunction E ℝ)},
  (Subalgebra.map (BoundedContinuousFunction.toContinuousMapₐ ℝ) A).SeparatesPoints →
    (∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P') →
      0 < ε → |∫ (x : E), ε.mulExpNegMulSq (f x) ∂P - ∫ (x : E), ε.mulExpNegMulSq (f x) ∂P'| ≤ 6 * √ε
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.toSpecΓ_isoSpec_inv_assoc : ∀ (X : AlgebraicGeometry.Scheme) [inst : AlgebraicGeometry.IsAffine X] {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp X.toSpecΓ (CategoryTheory.CategoryStruct.comp X.isoSpec.inv h) = h
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {he : t ≠ ∅}, t.maxKey he ∈ t
-- Init.Data.BitVec.Lemmas
BitVec.getMsbD_rotateLeftAux_of_lt : ∀ {w : ℕ} {x : BitVec w} {r i : ℕ}, i < w - r → (x.rotateLeftAux r).getMsbD i = x.getMsbD (r + i)