mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Filter.Pointwise
Filter.instMul.eq_1 : ∀ {α : Type u_2} [inst : Mul α],
  Filter.instMul =
    {
      mul := fun f g =>
        let __src := Filter.map₂ (fun x1 x2 => x1 * x2) f g;
        { sets := {s | ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ * t₂ ⊆ s}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ } }
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionIdentifier.fvar.inj : ∀ {id id_1 : Lean.FVarId}, Lean.Lsp.CompletionIdentifier.fvar id = Lean.Lsp.CompletionIdentifier.fvar id_1 → id = id_1
-- Mathlib.Algebra.Order.GroupWithZero.Defs
/-- Typeclass for strict reverse monotonicity of multiplication by nonnegative elements on
the left, namely `b * a₁ < b * a₂ → a₁ < a₂` if `0 ≤ b`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`IsStrictOrderedRing`.  -/
PosMulReflectLT : (α : Type u_1) → [Mul α] → [Zero α] → [Preorder α] → Prop
-- Mathlib.Topology.Algebra.Group.Basic
Filter.Tendsto.const_sub : ∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : Sub G] [ContinuousSub G] (b : G) {c : G} {f : α → G}
  {l : Filter α}, Filter.Tendsto f l (nhds c) → Filter.Tendsto (fun x => b - f x) l (nhds (b - c))
-- Mathlib.RepresentationTheory.Basic
Representation.ofQuotient_coe_apply : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : Semiring k] [inst_1 : Group G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module k V] (ρ : Representation k G V) (S : Subgroup G) [inst_4 : S.Normal]
  [inst_5 : Representation.IsTrivial (MonoidHom.comp ρ S.subtype)] (g : G) (x : V), ((ρ.ofQuotient S) ↑g) x = (ρ g) x
-- Init.Data.Bool
Bool.bne_assoc : ∀ (x y z : Bool), ((x != y) != z) = (x != (y != z))
-- Mathlib.MeasureTheory.Function.SimpleFunc
/-- To prove something for an arbitrary measurable function into `ℝ≥0∞`, it suffices to show
that the property holds for (multiples of) characteristic functions and is closed under addition
and supremum of increasing sequences of functions.

It is possible to make the hypotheses in the induction steps a bit stronger, and such conditions
can be added once we need them (for example in `h_add` it is only necessary to consider the sum of
a simple function with a multiple of a characteristic function and that the intersection
of their images is a subset of `{0}`).  -/
Measurable.ennreal_induction : ∀ {α : Type u_1} {mα : MeasurableSpace α} {motive : (α → ENNReal) → Prop},
  (∀ (c : ENNReal) ⦃s : Set α⦄, MeasurableSet s → motive (s.indicator fun x => c)) →
    (∀ ⦃f g : α → ENNReal⦄,
        Disjoint (Function.support f) (Function.support g) →
          Measurable f → Measurable g → motive f → motive g → motive (f + g)) →
      (∀ ⦃f : ℕ → α → ENNReal⦄,
          (∀ (n : ℕ), Measurable (f n)) → Monotone f → (∀ (n : ℕ), motive (f n)) → motive fun x => ⨆ n, f n x) →
        ∀ ⦃f : α → ENNReal⦄, Measurable f → motive f
-- Mathlib.Data.Nat.Choose.Basic
/-- Show that for small values of the right argument, the middle value is largest.  -/
_private.Mathlib.Data.Nat.Choose.Basic.0.Nat.choose_le_middle_of_le_half_left : ∀ {n r : ℕ}, r ≤ n / 2 → n.choose r ≤ n.choose (n / 2)
-- Mathlib.Analysis.Normed.Group.Basic
norm_lt_of_mem_ball : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] {a b : E} {r : ℝ}, b ∈ Metric.ball a r → ‖b‖ < ‖a‖ + r
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.ofSubmodules_apply : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid M₂] [inst_5 : TopologicalSpace M₂]
  {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
  {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃SL[σ₁₂] M₂) {p : Submodule R M} {q : Submodule R₂ M₂}
  (h : Submodule.map (↑↑e) p = q) (x : ↥p), ↑((e.ofSubmodules p q h) x) = e ↑x
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.isGE_truncGT_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} 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) (X : C) (a b : ℤ),
  autoParam (b ≤ a + 1) CategoryTheory.Triangulated.TStructure.isGE_truncGT_obj._auto_1 → t.IsGE ((t.truncGT a).obj X) b
-- Lean.Meta.TryThis
/-- Pretty-prints a `SuggestionText` as a `String` and wraps with respect to the pane width,
indentation, and column, via `Format.prettyExtra`. If `w := none`, then
`w := getInputWidth (← getOptions)` is used. Raw `String`s are returned as-is.  -/
Lean.Meta.Tactic.TryThis.SuggestionText.prettyExtra : Lean.Meta.Tactic.TryThis.SuggestionText → optParam (Option ℕ) none → optParam ℕ 0 → optParam ℕ 0 → Lean.CoreM String
-- Lean.Structure
Lean.instInhabitedStructureFieldInfo.default : Lean.StructureFieldInfo
-- Mathlib.Data.ENNReal.Basic
ENNReal.instCompleteLinearOrder : CompleteLinearOrder ENNReal
-- Mathlib.CategoryTheory.Preadditive.Projective.Basic
CategoryTheory.Projective.projective_iff_preservesEpimorphisms_coyoneda_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : C),
  CategoryTheory.Projective P ↔ (CategoryTheory.coyoneda.obj (Opposite.op P)).PreservesEpimorphisms
-- Mathlib.Data.Nat.Cast.Order.Basic
Nat.ofNat_le : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α]
  {m n : ℕ} [inst_5 : n.AtLeastTwo] [inst_6 : m.AtLeastTwo],
  OfNat.ofNat m ≤ OfNat.ofNat n ↔ OfNat.ofNat m ≤ OfNat.ofNat n
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso_hom_desc_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} {r s : CategoryTheory.Limits.Cocone G} {t : CategoryTheory.Limits.Cocone F}
  (P : CategoryTheory.Limits.IsColimit t) (Q : CategoryTheory.Limits.IsColimit s) (w : F ≅ G) {Z : C} (h : r.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp (P.coconePointsIsoOfNatIso Q w).hom
      (CategoryTheory.CategoryStruct.comp (Q.desc r) h) =
    CategoryTheory.CategoryStruct.comp (P.map r w.hom) h
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
/-- The left fraction from `X` to `Y` given by a morphism `s : Y ⟶ X` such that `W s`.  -/
CategoryTheory.MorphismProperty.LeftFraction.ofInv : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} → {X Y : C} → (s : Y ⟶ X) → W s → W.LeftFraction X Y
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mapPair_map_inclRight : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {E' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E'] (Fₗ : CategoryTheory.Functor C E) (Fᵣ : CategoryTheory.Functor D E')
  {d d' : D} (f : d ⟶ d'),
  (CategoryTheory.Join.mapPair Fₗ Fᵣ).map ((CategoryTheory.Join.inclRight C D).map f) =
    (CategoryTheory.Join.inclRight E E').map (Fᵣ.map f)
-- Mathlib.MeasureTheory.Measure.Restrict
piecewise_ae_eq_restrict_compl : ∀ {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {f g : α → β}
  [inst_1 : DecidablePred fun x => x ∈ s], MeasurableSet s → s.piecewise f g =ᵐ[μ.restrict sᶜ] g
-- Init.Data.String.Basic
String.extract_eq_copy_slice : ∀ {s : String} (p₀ p₁ : s.Pos) (h : p₀ ≤ p₁), String.extract p₀ p₁ = (s.slice p₀ p₁ h).copy
-- Init.Data.String.Lemmas.Basic
String.sliceFrom_eq_toSlice_iff : ∀ {s : String} {p : s.Pos}, s.sliceFrom p = s.toSlice ↔ p = s.startPos
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.tendsto_eapprox : ∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → ENNReal},
  Measurable f → ∀ (a : α), Filter.Tendsto (fun n => (MeasureTheory.SimpleFunc.eapprox f n) a) Filter.atTop (nhds (f a))
-- Mathlib.Order.Interval.Set.Basic
Set.notMem_Icc_of_gt : ∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, a < c → c ∉ Set.Icc b a
-- Mathlib.Order.Interval.Basic
Interval.lattice : {α : Type u_1} → [inst : Lattice α] → [DecidableLE α] → Lattice (Interval α)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
/-- If `M` is a commutative monoid object, then `Hom(X, M)` has a commutative monoid structure.  -/
CategoryTheory.Hom.commMonoid : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {M X : C} →
        [inst_2 : CategoryTheory.MonObj M] →
          [inst_3 : CategoryTheory.BraidedCategory C] → [CategoryTheory.IsCommMonObj M] → CommMonoid (X ⟶ M)
-- Lean.Server.RequestCancellation
Lean.Server.CancellableT.run : {m : Type → Type u_1} →
  {α : Type} →
    Lean.Server.RequestCancellationToken → Lean.Server.CancellableT m α → m (Except Lean.Server.RequestCancellation α)
-- Mathlib.Order.CountableSupClosed
CountableInfClosed.isGLB_mem : ∀ {α : Type u_2} [inst : LE α] {s : Set α},
  CountableInfClosed s → ∀ t ⊆ s, t.Nonempty → t.Countable → ∀ (x : α), IsGLB t x → x ∈ s
-- Mathlib.Analysis.Normed.Group.Uniform
LipschitzWith.norm_inv_mul_le_of_le : ∀ {E : Type u_2} {F : Type u_3} [inst : SeminormedGroup E] [inst_1 : SeminormedGroup F] {a b : E} {r : ℝ} {f : E → F}
  {C : NNReal}, LipschitzWith C f → ‖a⁻¹ * b‖ ≤ r → ‖(f a)⁻¹ * f b‖ ≤ ↑C * r
-- Mathlib.Data.List.NatAntidiagonal
/-- The length of the antidiagonal of `n` is `n + 1`.  -/
List.Nat.length_antidiagonal : ∀ (n : ℕ), (List.Nat.antidiagonal n).length = n + 1
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.approxDefEqImp : {α : Type} → Lean.MetaM α → Lean.MetaM α
-- Mathlib.RingTheory.DedekindDomain.Different
/-- The different ideal of an extension of integral domains `B/A` is the inverse of the dual of `A`
as an ideal of `B`. See `coeIdeal_differentIdeal` and `coeSubmodule_differentIdeal`.  -/
differentIdeal : (A : Type u_1) →
  (B : Type u_3) →
    [inst : CommRing A] →
      [inst_1 : CommRing B] →
        [inst_2 : Algebra A B] → [IsDomain A] → [IsDedekindDomain B] → [Module.IsTorsionFree A B] → Ideal B
-- Mathlib.CategoryTheory.Sites.LocallyFullyFaithful
CategoryTheory.Sieve.equalizer_apply : ∀ {C : Type uC} [inst : CategoryTheory.Category.{vC, uC} C] {U V : C} (f₁ f₂ : U ⟶ V) (x : C) (i : x ⟶ U),
  (CategoryTheory.Sieve.equalizer f₁ f₂).arrows i =
    (CategoryTheory.CategoryStruct.comp i f₁ = CategoryTheory.CategoryStruct.comp i f₂)
-- Mathlib.Algebra.Category.Grp.EpiMono
GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity : {A B : GrpCat} → {f : A ⟶ B} → GrpCat.SurjectiveOfEpiAuxs.XWithInfinity f
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.coe_coeCLE : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] (e : A ≃A[R] B), ⇑↑e = ⇑e
-- Mathlib.Algebra.Notation.Lemmas
ite_le_one : ∀ {α : Type u_1} [inst : One α] {p : Prop} [inst_1 : Decidable p] {a b : α} [inst_2 : LE α],
  a ≤ 1 → b ≤ 1 → (if p then a else b) ≤ 1
-- Mathlib.GroupTheory.GroupAction.ConjAct
val_unitsCentralizerEquiv_apply_coe : ∀ (M : Type u_2) [inst : Monoid M] (x : Mˣ) (a : (↥(Submonoid.centralizer {↑x}))ˣ),
  ↑↑((unitsCentralizerEquiv M x) a) = ↑↑a
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.toBoundedContinuousFunctionCLM_eq_of_scalars : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} (𝕜' : Type u_5)
  [inst_7 : NontriviallyNormedField 𝕜'] [inst_8 : NormedSpace 𝕜' F] [inst_9 : SMulCommClass ℝ 𝕜' F],
  ⇑(ContDiffMapSupportedIn.toBoundedContinuousFunctionCLM 𝕜) =
    ⇑(ContDiffMapSupportedIn.toBoundedContinuousFunctionCLM 𝕜')
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get?_eq_some_getD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {a fallback : α},
  a ∈ t → t.get? a = some (t.getD a fallback)
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.ext_iff : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p q : MvPolynomial σ R},
  p = q ↔ ∀ (m : σ →₀ ℕ), MvPolynomial.coeff m p = MvPolynomial.coeff m q
-- Std.Time.Date.Basic
Std.Time.instHAddOffset_1 : HAdd Std.Time.Millisecond.Offset Std.Time.Millisecond.Offset Std.Time.Millisecond.Offset
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftComm_hom_comp : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddCommMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] {X Y : C} (f : X ⟶ Y) (i j : A),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.shiftComm X i j).hom
      ((CategoryTheory.shiftFunctor C i).map ((CategoryTheory.shiftFunctor C j).map f)) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C j).map ((CategoryTheory.shiftFunctor C i).map f))
      (CategoryTheory.shiftComm Y i j).hom
-- Lean.Parser.Basic
Lean.Parser.checkWsBeforeFn : String → Lean.Parser.ParserFn
-- Init.Grind.Norm
Lean.Grind.forall_true : ∀ (p : True → Prop), (∀ (h : True), p h) = p True.intro
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of the reverse direction of `Set.disjoint_compl_right_iff_subset`. -/
HasSubset.Subset.disjoint_compl_right : ∀ {α : Type u_1} {s t : Set α}, s ⊆ t → Disjoint s tᶜ
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_maxKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {fallback fallback' : α}, t.getKeyD (t.maxKeyD fallback) fallback' = t.maxKeyD fallback
-- Init.Data.UInt.Lemmas
UInt16.ofNatClamp_finVal : ∀ (n : Fin UInt16.size), UInt16.ofNatClamp ↑n = UInt16.ofFin n
-- Mathlib.Data.List.Sort
OrderEmbedding.sortedGT_listMap : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ↪o β) {l : List α},
  (List.map (⇑e) l).SortedGT ↔ l.SortedGT
-- Mathlib.Tactic.Attr.Register
/-- Simplification rules for ghost equations.  -/
Parser.Attr.ghost_simps : Lean.ParserDescr
-- Init.Grind.AC
Lean.Grind.AC.Seq.cons.sizeOf_spec : ∀ (x : Lean.Grind.AC.Var) (s : Lean.Grind.AC.Seq), sizeOf (Lean.Grind.AC.Seq.cons x s) = 1 + sizeOf x + sizeOf s
-- Mathlib.Data.Set.Function
Set.exists_subset_bijOn : ∀ {α : Type u_1} {β : Type u_2} (s : Set α) (f : α → β), ∃ s' ⊆ s, Set.BijOn f s' (f '' s)
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_neg_one_pow : ∀ (R : Type u_3) [inst : Ring R] (m : ℕ), ∑ n, (-1) ^ ↑n = if Even m then 0 else 1
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
/-- `s.closedInterior` is the set of points that can be expressed as an affine combination
of the vertices with weights between 0 and 1 inclusive. This is equivalent to the convex hull of
the vertices or the closure of the interior.  -/
Affine.Simplex.closedInterior : {k : Type u_1} →
  {V : Type u_2} →
    {P : Type u_4} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V] →
          [inst_2 : Module k V] → [inst_3 : AddTorsor V P] → [PartialOrder k] → {n : ℕ} → Affine.Simplex k P n → Set P
-- Mathlib.RingTheory.Finiteness.Basic
Module.Finite.instMulOpposite : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Finite R M], Module.Finite R Mᵐᵒᵖ
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- If the product comparison morphism is an iso, its inverse is natural.  -/
CategoryTheory.Limits.prodComparison_inv_natural : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{w, u₂} D]
  (F : CategoryTheory.Functor C D) {A A' B B' : C} [inst_2 : CategoryTheory.Limits.HasBinaryProduct A B]
  [inst_3 : CategoryTheory.Limits.HasBinaryProduct A' B']
  [inst_4 : CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)]
  [inst_5 : CategoryTheory.Limits.HasBinaryProduct (F.obj A') (F.obj B')] (f : A ⟶ A') (g : B ⟶ B')
  [inst_6 : CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison F A B)]
  [inst_7 : CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison F A' B')],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.prodComparison F A B))
      (F.map (CategoryTheory.Limits.prod.map f g)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (F.map f) (F.map g))
      (CategoryTheory.inv (CategoryTheory.Limits.prodComparison F A' B'))
-- Mathlib.RingTheory.WittVector.Defs
WittVector.wittZero_eq_zero : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ), WittVector.wittZero p n = 0
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.fibrations_llp : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [inst_2 : HomotopicalAlgebra.CategoryWithCofibrations C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  [(HomotopicalAlgebra.trivialCofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.fibrations C)],
  (HomotopicalAlgebra.fibrations C).llp = HomotopicalAlgebra.trivialCofibrations C
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.toModuleCat : {R : Type u} → [inst : Ring R] → [inst_1 : TopologicalSpace R] → TopModuleCat R → ModuleCat R
-- Mathlib.Logic.Equiv.Basic
Equiv.subtypeQuotientEquivQuotientSubtype_symm_mk : ∀ {α : Sort u_1} (p₁ : α → Prop) [s₁ : Setoid α] [s₂ : Setoid (Subtype p₁)] (p₂ : Quotient s₁ → Prop)
  (hp₂ : ∀ (a : α), p₁ a ↔ p₂ ⟦a⟧) (h : ∀ (x y : Subtype p₁), s₂ x y ↔ ↑x ≈ ↑y) (x : Subtype p₁),
  (Equiv.subtypeQuotientEquivQuotientSubtype p₁ p₂ hp₂ h).symm ⟦x⟧ = ⟨⟦↑x⟧, ⋯⟩
-- Init.Data.Rat.Lemmas
Rat.add_right_cancel : ∀ {a b : ℚ} (c : ℚ), a + c = b + c → a = b
-- Init.Data.Array.Zip
Array.zipWithAll_map : ∀ {γ : Type u_1} {δ : Type u_2} {α : Type u_1} {β : Type u_2} {μ : Type u_3} {f : Option γ → Option δ → μ} {g : α → γ}
  {h : β → δ} {as : Array α} {bs : Array β},
  Array.zipWithAll f (Array.map g as) (Array.map h bs) = Array.zipWithAll (fun a b => f (g <$> a) (h <$> b)) as bs
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.parallelPairDiagramOfIsLimit_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) (c : CategoryTheory.Limits.Fan I.left)
  {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d)
  {X Y : CategoryTheory.Limits.WalkingParallelPair} (h : X ⟶ Y),
  (I.parallelPairDiagramOfIsLimit c hd).map h =
    CategoryTheory.Limits.parallelPair.parallelPairHom (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd) h
-- Mathlib.Data.EReal.Inv
EReal.sign_neg : ∀ (x : EReal), SignType.sign (-x) = -SignType.sign x
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.meet_top : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P : l}, Lean.Order.meet P Lean.Order.top = P
-- Mathlib.Algebra.Order.Nonneg.Field
Nonneg.val_inv_unitsEquivPos_symm_apply_coe : ∀ (R : Type u_2) [inst : DivisionSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : PosMulReflectLT R] (r : { r // 0 < r }), ↑↑((Nonneg.unitsEquivPos R).symm r)⁻¹ = (↑r)⁻¹
-- Mathlib.RingTheory.Extension.Presentation.Submersive
_private.Mathlib.RingTheory.Extension.Presentation.Submersive.0.Algebra.PreSubmersivePresentation.jacobiMatrix_comp_₂₂_det : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_1} {σ' : Type u_2} {T : Type u_3} [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T] (Q : Algebra.PreSubmersivePresentation S T ι' σ')
  (P : Algebra.PreSubmersivePresentation R S ι σ) [inst_7 : Fintype σ] [inst_8 : Fintype σ'],
  (MvPolynomial.aeval (Q.comp P).val) (Q.comp P).jacobiMatrix.toBlocks₂₂.det = (algebraMap S T) P.jacobian
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Term.realize_relabel : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {β : Type v'} {t : L.Term α} {g : α → β}
  {v : β → M},
  FirstOrder.Language.Term.realize v (FirstOrder.Language.Term.relabel g t) = FirstOrder.Language.Term.realize (v ∘ g) t
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
MulRingSeminorm.instInhabited : {R : Type u_1} →
  [inst : NonAssocRing R] → [DecidableEq R] → [NoZeroDivisors R] → [Nontrivial R] → Inhabited (MulRingSeminorm R)
-- Std.Net.Addr
Std.Net.SocketAddress.v4 : Std.Net.SocketAddressV4 → Std.Net.SocketAddress
-- Mathlib.Order.Filter.Lift
/-- **Alias** of `Filter.mem_prod_self_iff`. -/
Filter.mem_prod_same_iff : ∀ {α : Type u_1} {la : Filter α} {s : Set (α × α)}, s ∈ la ×ˢ la ↔ ∃ t ∈ la, t ×ˢ t ⊆ s
-- Mathlib.Geometry.Manifold.Algebra.Structures
ContMDiffRing.toLieAddGroup : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {n : WithTop ℕ∞} (I : ModelWithCorners 𝕜 E H)
  (R : Type u_4) [inst_4 : Ring R] [inst_5 : TopologicalSpace R] [inst_6 : ChartedSpace H R] [ContMDiffRing I n R],
  LieAddGroup I n R
-- Mathlib.Analysis.Normed.Field.Basic
norm_inv : ∀ {α : Type u_2} [inst : NormedDivisionRing α] (a : α), ‖a⁻¹‖ = ‖a‖⁻¹
-- Lean.Meta.Tactic.Grind.EMatch
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.ematchOnly.go : Array Lean.Meta.Grind.EMatchTheorem → Lean.Meta.Grind.EMatch.M Unit
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get?_of_isEmpty : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {a : α},
  t.isEmpty = true → t.get? a = none
-- Mathlib.Algebra.Group.Int.Units
Int.eq_one_or_neg_one_of_mul_eq_one : ∀ {u v : ℤ}, u * v = 1 → u = 1 ∨ u = -1
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.linearGrowthInf_bot : LinearGrowth.linearGrowthInf ⊥ = ⊥
-- Mathlib.Order.Atoms
isStronglyAtomic_iff : ∀ (α : Type u_5) [inst : Preorder α], IsStronglyAtomic α ↔ ∀ (a b : α), a < b → ∃ x, a ⋖ x ∧ x ≤ b
-- Mathlib.CategoryTheory.Subobject.Basic
/-- Use choice to pick a representative `MonoOver X` for each `Subobject X`.
 -/
CategoryTheory.Subobject.representative : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} → CategoryTheory.Functor (CategoryTheory.Subobject X) (CategoryTheory.MonoOver X)
-- Mathlib.Algebra.Regular.Prod
Prod.isAddRightRegular_mk : ∀ {R : Type u_2} {S : Type u_3} [inst : Add R] [inst_1 : Add S] {a : R} {b : S},
  IsAddRightRegular (a, b) ↔ IsAddRightRegular a ∧ IsAddRightRegular b
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.flipEquivalence_inverse : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.Square.flipEquivalence.inverse = CategoryTheory.Square.flipFunctor
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
_private.Mathlib.Algebra.BigOperators.Group.Finset.Defs.0.BigOperators.FinsetFilterResult.mk.sizeOf_spec : ∀ (finset : BigOperators.FinsetResult✝) (filter : Option Lean.Term),
  sizeOf { finset := finset, filter := filter } = 1 + sizeOf finset + sizeOf filter
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
/-- Reinterpret a `LinearIsometryEquiv` as a `ContinuousLinearEquiv`.  -/
LinearIsometryEquiv.instCoeTCContinuousLinearEquiv : {R : Type u_1} →
  {R₂ : Type u_2} →
    {E : Type u_5} →
      {E₂ : Type u_6} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            {σ₁₂ : R →+* R₂} →
              {σ₂₁ : R₂ →+* R} →
                [inst_2 : RingHomInvPair σ₁₂ σ₂₁] →
                  [inst_3 : RingHomInvPair σ₂₁ σ₁₂] →
                    [inst_4 : SeminormedAddCommGroup E] →
                      [inst_5 : SeminormedAddCommGroup E₂] →
                        [inst_6 : Module R E] → [inst_7 : Module R₂ E₂] → CoeTC (E ≃ₛₗᵢ[σ₁₂] E₂) (E ≃SL[σ₁₂] E₂)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.instAddMonoid : {k : Type u_1} → {G : Type u_2} → [inst : AddMonoid k] → AddMonoid (SkewMonoidAlgebra k G)