mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
MeasurableSet.image_inclusion : ∀ {α : Type u_1} {m : MeasurableSpace α} {s t : Set α} (h : s ⊆ t) {u : Set ↑s},
  MeasurableSet s → MeasurableSet u → MeasurableSet (Set.inclusion h '' u)
-- Mathlib.Order.ConditionallyCompleteLattice.Defs
ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder : {α : Type u_5} → [self : ConditionallyCompleteLinearOrderBot α] → ConditionallyCompleteLinearOrder α
-- Mathlib.CategoryTheory.Monoidal.Transport
/-- The unit isomorphism upgrades to a monoidal isomorphism.  -/
CategoryTheory.Monoidal.instIsMonoidalUnitTransportedEquivalenceTransported : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D),
  CategoryTheory.NatTrans.IsMonoidal (CategoryTheory.Monoidal.equivalenceTransported e).unit
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.counitIso_hom_inv_id_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) (Y : D),
  CategoryTheory.CategoryStruct.comp (e.counit.app Y) (e.counitInv.app Y) =
    CategoryTheory.CategoryStruct.id (e.functor.obj (e.inverse.obj Y))
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
Multipliable.tprod_sum : ∀ {α : Type u_4} {β : Type u_5} {M : Type u_6} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] [ContinuousMul M]
  [T2Space M] {f : α ⊕ β → M},
  Multipliable (f ∘ Sum.inl) →
    Multipliable (f ∘ Sum.inr) → ∏' (i : α ⊕ β), f i = (∏' (i : α), f (Sum.inl i)) * ∏' (i : β), f (Sum.inr i)
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.sup_eq_left : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {a b : CauSeq α abs},
  b ≤ a → a ⊔ b ≈ a
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.instCoeFunForall : {𝕜 : 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] → CoeFun (ModelWithCorners 𝕜 E H) fun x => H → E
-- Mathlib.Data.Finset.Grade
Finset.isAtom_singleton : ∀ {α : Type u_1} (a : α), IsAtom {a}
-- Mathlib.Order.Filter.AtTopBot.Defs
Filter.eventually_gt_atTop : ∀ {α : Type u_3} [inst : Preorder α] [NoTopOrder α] (a : α), ∀ᶠ (x : α) in Filter.atTop, a < x
-- Lean.Meta.AbstractMVars
Lean.Meta.AbstractMVars.State.lmap : Lean.Meta.AbstractMVars.State → Std.HashMap Lean.LMVarId Lean.Level
-- Batteries.Tactic.Lint.Basic
/-- The linter declaration name  -/
Batteries.Tactic.Lint.NamedLinter.declName : Batteries.Tactic.Lint.NamedLinter → Lean.Name
-- Mathlib.Combinatorics.Quiver.Cast
Quiver.Path.cast_eq_cast : ∀ {U : Type u_1} [inst : Quiver U] {u v u' v' : U} (hu : u = u') (hv : v = v') (p : Quiver.Path u v),
  Quiver.Path.cast hu hv p = cast ⋯ p
-- Mathlib.Probability.Kernel.Integral
ProbabilityTheory.Kernel.IsMarkovKernel.integrable : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μ : MeasureTheory.Measure α)
  [MeasureTheory.IsFiniteMeasure μ] (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel κ] {s : Set β},
  MeasurableSet s → MeasureTheory.Integrable (fun x => (κ x).real s) μ
-- Std.Http.Transport
_private.Std.Http.Transport.0.Std.Http.Internal.Mock.Client.mk.sizeOf_spec : ∀ (shared : Std.Http.Internal.Mock.SharedState✝), sizeOf { shared := shared } = 1 + sizeOf shared
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.μ_inv_natural_left : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.Monoidal.μ L W ε X₁ Y).inv
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).map f)
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y)) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).map
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y))
      (CategoryTheory.Localization.Monoidal.μ L W ε X₂ Y).inv
-- Init.Data.UInt.Lemmas
UInt64.toFin.ofNat : ∀ {n : ℕ}, (UInt64.ofNat n).toFin = Fin.ofNat UInt64.size n
-- Mathlib.RingTheory.Ideal.Quotient.Operations
RingHom.lift_injective_of_ker_le_ideal : ∀ {R : Type u} {S : Type v} [inst : Ring R] [inst_1 : Semiring S] (I : Ideal R) [inst_2 : I.IsTwoSided] {f : R →+* S}
  (H : ∀ a ∈ I, f a = 0), RingHom.ker f ≤ I → Function.Injective ⇑(Ideal.Quotient.lift I f H)
-- Init.Data.Nat.Simproc
Nat.Simproc.add_eq_gt : ∀ (a : ℕ) {b c : ℕ}, b > c → (a + b = c) = False
-- Mathlib.Algebra.Lie.Basis.Base
LieAlgebra.Basis.coe_linearMap_baseSupp' : ∀ {ι : Type u_1} {K : Type u_2} {L : Type u_3} [inst : Fintype ι] [inst_1 : Field K] [inst_2 : CharZero K]
  [inst_3 : LieRing L] [inst_4 : LieAlgebra K L] [inst_5 : FiniteDimensional K L] {H : LieSubalgebra K L}
  (b : LieAlgebra.Basis ι H) (i : ι), LieModule.Weight.toLinear K (↥H) L ↑(b.baseSupp' i) = b.baseSupp i
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.comap_equiv_eq_map_symm : ∀ {N : Type u_2} [inst : MulOneClass N] {M : Type u_5} [inst_1 : MulOneClass M] (f : N ≃* M) (K : Submonoid M),
  Submonoid.comap f K = Submonoid.map f.symm K
-- Lean.Elab.Tactic.Omega.Core
/-- Is the Fourier-Motzkin elimination known to be exact?  -/
Lean.Elab.Tactic.Omega.Problem.FourierMotzkinData.exact : Lean.Elab.Tactic.Omega.Problem.FourierMotzkinData → Bool
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
PiTensorProduct.tprodL_coe : ∀ {ι : Type u_1} [inst : Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)],
  (PiTensorProduct.tprodL 𝕜).toMultilinearMap = PiTensorProduct.tprod 𝕜
-- Mathlib.Analysis.Calculus.Implicit
/-- An open partial homeomorphism between `E` and `F × f'.ker` sending level surfaces of `f`
to vertical subspaces.  -/
HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          [CompleteSpace E] →
            {F : Type u_3} →
              [inst_4 : NormedAddCommGroup F] →
                [inst_5 : NormedSpace 𝕜 F] →
                  [CompleteSpace F] →
                    (f : E → F) →
                      (f' : E →L[𝕜] F) →
                        {a : E} →
                          HasStrictFDerivAt f f' a →
                            (↑f').range = ⊤ → (↑f').ker.ClosedComplemented → OpenPartialHomeomorph E (F × ↥(↑f').ker)
-- Batteries.Tactic.Lemma
/-- Check whether `lang.lemmaCmd` option is enabled  -/
Batteries.Tactic.Lemma.checkLangLemmaCmd : Lean.Options → Bool
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.Closeds.instDiscreteUniformity : ∀ {α : Type u_1} [inst : UniformSpace α] [DiscreteUniformity α], DiscreteUniformity (TopologicalSpace.Closeds α)
-- Init.Data.List.Impl
List.findSomeRev?_eq_findSomeRev?TR : @List.findSomeRev? = @List.findSomeRev?TR
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.size_eq : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → m₁.Equiv m₂ → m₁.size = m₂.size
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.instDistribMulActionOfSMulCommClassOfContinuousConstSMul : {R : Type u_1} →
  {V : Type u_2} →
    {W : Type u_3} →
      {P : Type u_4} →
        [inst : Ring R] →
          [inst_1 : AddCommGroup V] →
            [inst_2 : Module R V] →
              [inst_3 : TopologicalSpace P] →
                [inst_4 : AddTorsor V P] →
                  [inst_5 : AddCommGroup W] →
                    [inst_6 : Module R W] →
                      {S : Type u_10} →
                        [inst_7 : TopologicalSpace W] →
                          [inst_8 : IsTopologicalAddGroup W] →
                            [inst_9 : Monoid S] →
                              [inst_10 : DistribMulAction S W] →
                                [SMulCommClass R S W] → [ContinuousConstSMul S W] → DistribMulAction S (P →ᴬ[R] W)
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Final.extendCocone_map_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [inst_2 : F.Final] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  {G : CategoryTheory.Functor D E} {X Y : CategoryTheory.Limits.Cocone (F.comp G)} (f : X ⟶ Y),
  (CategoryTheory.Functor.Final.extendCocone.map f).hom = f.hom
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.refl_restr_target : ∀ {α : Type u_1} (s : Set α), ((PartialEquiv.refl α).restr s).target = s
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem_filter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool} {k : α} {h' : k ∈ Std.ExtTreeMap.filter f t}, (Std.ExtTreeMap.filter f t)[k] = t[k]
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PrepathObject.symm_p₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (P : HomotopicalAlgebra.PrepathObject A),
  P.symm.p₀ = P.p₁
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKey_alter_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] [Inhabited α] {k : α} {f : Option β → Option β} {h : k ∈ Std.DHashMap.Const.alter m k f},
  (Std.DHashMap.Const.alter m k f).getKey k h = k
-- Init.Omega.IntList
Lean.Omega.IntList.dot.eq_1 : ∀ (xs ys : Lean.Omega.IntList), xs.dot ys = (xs * ys).sum
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_rev_uIoo : ∀ {n : ℕ} (i j : Fin n), Fin.rev ⁻¹' Set.uIoo i j = Set.uIoo i.rev j.rev
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.incidenceSetFintype : {V : Type u_1} →
  (G : SimpleGraph V) → (v : V) → [Fintype ↑(G.neighborSet v)] → [DecidableEq V] → Fintype ↑(G.incidenceSet v)
-- Std.Do.PostCond
Std.Do.ExceptConds.false.eq_1 : ∀ {ps : Std.Do.PostShape}, Std.Do.ExceptConds.false = Std.Do.ExceptConds.const False
-- Lean.Elab.Arg
Lean.Elab.Term.NamedArg.mk.inj : ∀ {ref : Lean.Syntax} {name : Lean.Name} {val : Lean.Elab.Term.Arg} {numImplicitParams : ℕ} {ref_1 : Lean.Syntax}
  {name_1 : Lean.Name} {val_1 : Lean.Elab.Term.Arg} {numImplicitParams_1 : ℕ},
  { ref := ref, name := name, val := val, numImplicitParams := numImplicitParams } =
      { ref := ref_1, name := name_1, val := val_1, numImplicitParams := numImplicitParams_1 } →
    ref = ref_1 ∧ name = name_1 ∧ val = val_1 ∧ numImplicitParams = numImplicitParams_1
-- Mathlib.Data.Set.Image
Function.Injective.compl_image_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Injective f → ∀ (s : Set α), (f '' s)ᶜ = f '' sᶜ ∪ (Set.range f)ᶜ
-- Batteries.Data.Char.AsciiCasing
Char.toUpper_eq_of_not_isLower : ∀ {c : Char}, ¬c.isLower = true → c.toUpper = c
-- Mathlib.Data.Analysis.Filter
/-- A `CFilter` realizes the filter it generates.  -/
CFilter.toRealizer : {α : Type u_1} → {σ : Type u_3} → (F : CFilter (Set α) σ) → F.toFilter.Realizer
-- Aesop.Search.ExpandSafePrefix
Aesop.SafeExpansionM.State : Type
-- Mathlib.MeasureTheory.Integral.Lebesgue.Sub
/-- **Monotone convergence theorem** for nonincreasing sequences of functions.  -/
MeasureTheory.lintegral_iInf_ae : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : ℕ → α → ENNReal},
  (∀ (n : ℕ), Measurable (f n)) →
    (∀ (n : ℕ), f n.succ ≤ᵐ[μ] f n) → ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤ → ∫⁻ (a : α), ⨅ n, f n a ∂μ = ⨅ n, ∫⁻ (a : α), f n a ∂μ
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonHoverParams : Lean.FromJson Lean.Lsp.HoverParams
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.pentagon_hom_hom_inv_hom_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {W X Y Z Z_1 : C}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj W
        (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z) ⟶
      Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj W X) Y Z).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.associator W X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).hom
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W
            (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv)
          h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.associator W X Y).hom
        Z)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.associator W (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).hom
        h)
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.Integrable.mono : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
  {l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤}
  {l' : BoxIntegral.IntegrationParams}, BoxIntegral.Integrable I l f vol → l' ≤ l → BoxIntegral.Integrable I l' f vol
-- Init.Data.Nat.Bitwise.Lemmas
Nat.toNat_testBit : ∀ (x i : ℕ), (x.testBit i).toNat = x / 2 ^ i % 2
-- Lean.ReducibilityAttrs
Lean.instInhabitedReducibilityStatus.default : Lean.ReducibilityStatus
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.tendsto_integral_approxOn_of_measurable : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [CompleteSpace E] [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] {f : α → E}
  {s : Set E} [inst_5 : TopologicalSpace.SeparableSpace ↑s],
  MeasureTheory.Integrable f μ →
    ∀ (hfm : Measurable f),
      (∀ᵐ (x : α) ∂μ, f x ∈ closure s) →
        ∀ {y₀ : E} (h₀ : y₀ ∈ s),
          MeasureTheory.Integrable (fun x => y₀) μ →
            Filter.Tendsto
              (fun n => MeasureTheory.SimpleFunc.integral μ (MeasureTheory.SimpleFunc.approxOn f hfm s y₀ h₀ n))
              Filter.atTop (nhds (∫ (x : α), f x ∂μ))
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.OneTruncation₂.reflQuiver_id : ∀ (S : SSet.Truncated 2) (x : S.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge._proof_1 })),
  CategoryTheory.ReflQuiver.id x = SSet.Truncated.Edge.id x
-- Mathlib.Order.Interval.Finset.Basic
Set.Infinite.not_bddBelow : ∀ {α : Type u_2} [inst : Preorder α] [LocallyFiniteOrderTop α] {s : Set α}, s.Infinite → ¬BddBelow s
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.toMonComonObj_mon_mul_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M : CategoryTheory.Bimon C),
  CategoryTheory.MonObj.mul.hom = CategoryTheory.MonObj.mul
-- Mathlib.Topology.Algebra.Group.Basic
isClosedMap_sub_left : ∀ {G : Type w} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] (a : G),
  IsClosedMap fun x => a - x
-- Mathlib.Data.Finset.Sigma
Finset.sigma_eq_empty : ∀ {ι : Type u_1} {α : ι → Type u_2} {s : Finset ι} {t : (i : ι) → Finset (α i)}, s.sigma t = ∅ ↔ ∀ i ∈ s, t i = ∅
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_finset_mem : ∀ {α : Type u_1} (a : α), Measurable fun s => a ∈ s
-- LeanSearchClient.LoogleSyntax
LeanSearchClient.loogleCmdImpl : Lean.Elab.Command.CommandElab
-- Mathlib.Algebra.Order.Group.Multiset
Multiset.instAddLeftReflectLE : ∀ {α : Type u_1}, AddLeftReflectLE (Multiset α)
-- Mathlib.Data.Rat.Cast.Order
NNRat.cast_min : ∀ {K : Type u_5} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] (p q : ℚ≥0),
  ↑(min p q) = min ↑p ↑q
-- Mathlib.Order.WithBot
WithBot.instWellFoundedGT : ∀ {α : Type u_1} [inst : LT α] [WellFoundedGT α], WellFoundedGT (WithBot α)
-- Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives
/-- The equivalence between `CochainComplex.Plus (InjectiveObject C)`
and the category of fibrant object in `CochainComplex.Plus C` for the
Quillen model category structure.  -/
CochainComplex.Plus.fibrantObjectEquivalence : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      CochainComplex.Plus (CategoryTheory.InjectiveObject C) ≌ HomotopicalAlgebra.FibrantObject (CochainComplex.Plus C)
-- Mathlib.RingTheory.Localization.Defs
Localization.mkAddMonoidHom_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} (b : ↥M) (a : R),
  (Localization.mkAddMonoidHom b) a = Localization.mk a b
-- Mathlib.Data.EReal.Basic
EReal.range_coe_eq_Ioo : Set.range Real.toEReal = Set.Ioo ⊥ ⊤
-- Mathlib.Topology.OmegaCompletePartialOrder
/-- The characteristic function of open sets is monotone and preserves
the limits of chains.  -/
Scott.IsOpen : (α : Type u) → [OmegaCompletePartialOrder α] → Set α → Prop
-- Mathlib.Data.Nat.ModEq
Dvd.dvd.zero_modEq_nat : ∀ {n a : ℕ}, n ∣ a → 0 ≡ a [MOD n]
-- Mathlib.Analysis.Normed.Group.Basic
norm_abs_zsmul : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (a : E) (n : ℤ), ‖|n| • a‖ = ‖n • a‖
-- Init.Data.Option.Lemmas
Option.max_eq_or : ∀ {α : Type u_1} [LE α] [inst : Max α], (∀ (x y : α), x ⊔ y = x ∨ x ⊔ y = y) → ∀ {a b : Option α}, a ⊔ b = a ∨ a ⊔ b = b
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.addCommMonoid : {α : Type u} → [AddCommMonoid α] → AddCommMonoid (WithBot α)
-- Mathlib.Data.List.Sigma
List.keys.eq_1 : ∀ {α : Type u} {β : α → Type v}, List.keys = List.map Sigma.fst
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.NumDenSameDeg.instSMul : {ι : Type u_1} →
  {A : Type u_2} →
    {σ : Type u_3} →
      [inst : CommRing A] →
        [inst_1 : SetLike σ A] →
          {𝒜 : ι → σ} →
            (x : Submonoid A) →
              {α : Type u_4} →
                [inst_2 : SMul α A] → [SMulMemClass σ α A] → SMul α (HomogeneousLocalization.NumDenSameDeg 𝒜 x)
-- Mathlib.FieldTheory.IsAlgClosed.Basic
/-- Typeclass for an extension being an algebraic closure.  -/
IsAlgClosure : (R : Type u) →
  (K : Type v) → [inst : CommRing R] → [inst_1 : Field K] → [inst_2 : Algebra R K] → [Module.IsTorsionFree R K] → Prop
-- Mathlib.CategoryTheory.Triangulated.Basic
/-- the third morphism in a triangle morphism  -/
CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C} →
        CategoryTheory.Pretriangulated.TriangleMorphism T₁ T₂ → (T₁.obj₃ ⟶ T₂.obj₃)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Polynomial.Chebyshev.integral_eval_T_real_mul_eval_T_real_measureT : ∀ (n m : ℤ),
  ∫ (x : ℝ),
      Polynomial.eval x (Polynomial.Chebyshev.T ℝ n) *
        Polynomial.eval x (Polynomial.Chebyshev.T ℝ m) ∂Polynomial.Chebyshev.measureT =
    (∫ (x : ℝ), Polynomial.eval x (Polynomial.Chebyshev.T ℝ (n + m)) ∂Polynomial.Chebyshev.measureT +
        ∫ (x : ℝ), Polynomial.eval x (Polynomial.Chebyshev.T ℝ (n - m)) ∂Polynomial.Chebyshev.measureT) /
      2
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.eraseLead_C_mul_X : ∀ {R : Type u_1} [inst : Semiring R] (r : R), (Polynomial.C r * Polynomial.X).eraseLead = 0
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- There exists a path of maximal length in a non-empty graph on finite edges.  -/
SimpleGraph.Walk.exists_isPath_forall_isPath_length_le_length : ∀ {V : Type u} (G : SimpleGraph V) [N : Nonempty V] [Finite ↑G.edgeSet],
  ∃ u v p, ∃ (_ : p.IsPath), ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsPath → p'.length ≤ p.length
-- Mathlib.LinearAlgebra.StdBasis
Module.piEquiv_apply_apply : ∀ (ι : Type u_5) (R : Type u_6) (M : Type u_7) [inst : Fintype ι] [inst_1 : CommSemiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (v : ι → M) (w : ι → R), ((Module.piEquiv ι R M) v) w = ∑ i, w i • v i
-- Init.Data.List.Perm
List.Perm.symm : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Perm l₂ → l₂.Perm l₁
-- Mathlib.Data.Quot
/-- Note that this provides `DecidableRel (Quot.Lift₂ f ha hb)` when `α = β`.  -/
Quot.lift₂.decidablePred : {α : Sort u_1} →
  {β : Sort u_2} →
    (r : α → α → Prop) →
      (s : β → β → Prop) →
        (f : α → β → Prop) →
          (ha : ∀ (a : α) (b₁ b₂ : β), s b₁ b₂ → f a b₁ = f a b₂) →
            (hb : ∀ (a₁ a₂ : α) (b : β), r a₁ a₂ → f a₁ b = f a₂ b) →
              [hf : (a : α) → DecidablePred (f a)] → (q₁ : Quot r) → DecidablePred (Quot.lift₂ f ha hb q₁)
-- Init.Data.Iterators.Consumers.Monadic.Access
Std.IterM.IsPlausibleNthOutputStep.below : {α β : Type w} →
  {m : Type w → Type w'} →
    [inst : Std.Iterator α m β] →
      {motive :
          (a : ℕ) →
            (a_1 : Std.IterM m β) →
              (a_2 : Std.IterStep (Std.IterM m β) β) → Std.IterM.IsPlausibleNthOutputStep a a_1 a_2 → Prop} →
        {a : ℕ} →
          {a_1 : Std.IterM m β} →
            {a_2 : Std.IterStep (Std.IterM m β) β} → Std.IterM.IsPlausibleNthOutputStep a a_1 a_2 → Prop
-- Lean.Meta.Basic
/-- When the following flag is set,
`isDefEq` throws the exception `Exception.isDefEqStuck`
whenever it encounters a constraint `?m ... =?= t` where
`?m` is read only.
This feature is useful for type class resolution where
we may want to notify the caller that the TC problem may be solvable
later after it assigns `?m`.  -/
Lean.Meta.Config.isDefEqStuckEx : Lean.Meta.Config → Bool
-- Mathlib.Data.List.TakeDrop
/-- Applying `tail` to a list `n` times is equivalent to dropping `n` elements.  -/
List.tail_iterate : ∀ {α : Type u} (l : List α) (n : ℕ), List.tail^[n] l = List.drop n l
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.instMonad.eq_1 : WithZero.instMonad =
  { map := @WithZero.instMonad._aux_1, mapConst := @WithZero.instMonad._aux_3, pure := @WithZero.instMonad._aux_5,
    seq := @WithZero.instMonad._aux_7, seqLeft := @WithZero.instMonad._aux_9, seqRight := @WithZero.instMonad._aux_11,
    bind := @WithZero.instMonad._aux_13 }
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.instIsSMulApplyℂ : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {α : Type u_1} [inst : SMul α ℂ] [inst_1 : IsScalarTower α ℂ ℂ]
  [inst_2 : Γ.HasDetOne], IsSMulApply α (ModularForm Γ k) UpperHalfPlane ℂ
-- Mathlib.LinearAlgebra.Matrix.WithConv
instMonoidWithConvMatrix : {m : Type u_1} → {n : Type u_2} → {α : Type u_3} → [Monoid α] → Monoid (WithConv (Matrix m n α))
-- Init.Core
Quotient.decidableEq : {α : Sort u} → {s : Setoid α} → [d : (a b : α) → Decidable (a ≈ b)] → DecidableEq (Quotient s)
-- Lean.Elab.Tactic.Config
Lean.Elab.Tactic.ConfigItemView.option : Lean.Elab.Tactic.ConfigItemView → Lean.Ident
-- Mathlib.GroupTheory.Coprod.Basic
MulEquiv.coprodAssoc_apply_inr : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Monoid M] [inst_1 : Monoid N] [inst_2 : Monoid P] (x : P),
  (MulEquiv.coprodAssoc M N P) (Monoid.Coprod.inr x) = Monoid.Coprod.inr (Monoid.Coprod.inr x)
-- Mathlib.CategoryTheory.Generator.Preadditive
CategoryTheory.Preadditive.isSeparating_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (P : CategoryTheory.ObjectProperty C),
  P.IsSeparating ↔
    ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (G : C), P G → ∀ (h : G ⟶ X), CategoryTheory.CategoryStruct.comp h f = 0) → f = 0