mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Dynamics.Ergodic.MeasurePreserving
MeasureTheory.MeasurePreserving.aeconst_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μa : MeasureTheory.Measure α} {μb : MeasureTheory.Measure β}
  [MeasurableSingletonClass γ] {f : α → β},
  MeasureTheory.MeasurePreserving f μa μb →
    ∀ {g : β → γ},
      MeasureTheory.NullMeasurable g μb →
        (Filter.EventuallyConst (g ∘ f) (MeasureTheory.ae μa) ↔ Filter.EventuallyConst g (MeasureTheory.ae μb))
-- Mathlib.Algebra.Star.Basic
MulOpposite.instStarMul : {R : Type u} → [inst : Mul R] → [StarMul R] → StarMul Rᵐᵒᵖ
-- Mathlib.Topology.Sheaves.SheafOfFunctions
/-- The presheaf of not-necessarily-continuous functions to
a target type `T` satisfies the sheaf condition.
 -/
TopCat.Presheaf.toType_isSheaf : ∀ (X : TopCat) (T : Type u_1), (X.presheafToType T).IsSheaf
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.lowerBound?_mem_lb : ∀ {α : Type u_1} {cut : α → Ordering} {lb : Option α} {x : α} {t : RBTree.RBNode α},
  RBTree.RBNode.lowerBound? cut t lb = some x → x ∈ t ∨ lb = some x
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.mergeSortTR₂.run'.eq_2 : ∀ {α : Type u_1} (le : α → α → Bool) (a : α) (property : [a].length = 1),
  List.MergeSort.Internal.mergeSortTR₂.run'✝ le ⟨[a], property⟩ = [a]
-- Init.Data.BitVec.Lemmas
BitVec.ofBoolListBE.eq_2 : ∀ (b : Bool) (bs : List Bool), BitVec.ofBoolListBE (b :: bs) = BitVec.cons b (BitVec.ofBoolListBE bs)
-- Mathlib.Tactic.GCongr.Core
Mathlib.Tactic.GCongr.GCongrKey.mk.sizeOf_spec : ∀ (relName head : Lean.Name) (arity : ℕ),
  sizeOf { relName := relName, head := head, arity := arity } = 1 + sizeOf relName + sizeOf head + sizeOf arity
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.toCycles_moduleCatCyclesIso_hom : ∀ {R : Type u} [inst : Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)),
  CategoryTheory.CategoryStruct.comp S.toCycles S.moduleCatCyclesIso.hom = S.moduleCatLeftHomologyData.f'
-- Mathlib.Data.Opposite
Opposite.op_inj_iff : ∀ {α : Sort u} (x y : α), Opposite.op x = Opposite.op y ↔ x = y
-- Mathlib.Analysis.BoxIntegral.Basic
/-- A function `f` has Henstock (or `⊥`) integral over `I` is equal to the value of a box-additive
function `g` on `I` provided that `vol J (f x)` is sufficiently close to `g J` for sufficiently
small boxes `J ∋ x`. This lemma is useful to prove, e.g., to prove the Divergence theorem for
integral along `⊥`.

Let `l` be either `BoxIntegral.IntegrationParams.Henstock` or `⊥`. Let `g` a box-additive function
on subboxes of `I`. Suppose that there exists a nonnegative box-additive function `B` and a
countable set `s` with the following property.

For every `c : ℝ≥0`, a point `x ∈ I.Icc`, and a positive `ε` there exists `δ > 0` such that for any
box `J ≤ I` such that

- `x ∈ J.Icc ⊆ Metric.closedBall x δ`;
- if `l.bDistortion` (i.e., `l = ⊥`), then the distortion of `J` is less than or equal to `c`,

the distance between the term `vol J (f x)` of an integral sum corresponding to `J` and `g J` is
less than or equal to `ε` if `x ∈ s` and is less than or equal to `ε * B J` otherwise.

Then `f` is integrable on `I` along `l` with integral `g I`.  -/
BoxIntegral.HasIntegral.of_le_Henstock_of_forall_isLittleO : ∀ {ι : 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.Henstock →
    ∀ (B : BoxIntegral.BoxAdditiveMap ι ℝ ↑I),
      (∀ (J : BoxIntegral.Box ι), 0 ≤ B J) →
        ∀ (g : BoxIntegral.BoxAdditiveMap ι F ↑I) (s : Set (ι → ℝ)),
          s.Countable →
            (∀ (c : NNReal),
                ∀ x ∈ BoxIntegral.Box.Icc I ∩ s,
                  ∀ ε > 0,
                    ∃ δ > 0,
                      ∀ J ≤ I,
                        BoxIntegral.Box.Icc J ⊆ Metric.closedBall x δ →
                          x ∈ BoxIntegral.Box.Icc J →
                            (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε) →
              (∀ (c : NNReal),
                  ∀ x ∈ BoxIntegral.Box.Icc I \ s,
                    ∀ ε > 0,
                      ∃ δ > 0,
                        ∀ J ≤ I,
                          BoxIntegral.Box.Icc J ⊆ Metric.closedBall x δ →
                            x ∈ BoxIntegral.Box.Icc J →
                              (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε * B J) →
                BoxIntegral.HasIntegral I l f vol (g I)
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.nfp_zero_left : ∀ (a : Ordinal.{u_1}), Ordinal.nfp 0 a = a
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.FoldingRange.mk.injEq : ∀ (startLine endLine : ℕ) (kind? : Option Lean.Lsp.FoldingRangeKind) (startLine_1 endLine_1 : ℕ)
  (kind?_1 : Option Lean.Lsp.FoldingRangeKind),
  ({ startLine := startLine, endLine := endLine, kind? := kind? } =
      { startLine := startLine_1, endLine := endLine_1, kind? := kind?_1 }) =
    (startLine = startLine_1 ∧ endLine = endLine_1 ∧ kind? = kind?_1)
-- Mathlib.Computability.NFA
NFA.eval_nil : ∀ {α : Type u} {σ : Type v} (M : NFA α σ), M.eval [] = M.start
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.expMapBasis.eq_1 : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K],
  NumberField.mixedEmbedding.fundamentalCone.expMapBasis =
    (NumberField.mixedEmbedding.fundamentalCone.completeBasis K).equivFunL.symm.toHomeomorph.transOpenPartialHomeomorph
      NumberField.mixedEmbedding.fundamentalCone.expMap
-- Mathlib.Algebra.Notation.Indicator
Set.indicator_apply_eq_zero : ∀ {α : Type u_1} {M : Type u_3} [inst : Zero M] {s : Set α} {f : α → M} {a : α}, s.indicator f a = 0 ↔ a ∈ s → f a = 0
-- Lean.Language.Lean.Types
Lean.Language.Lean.CommandParsedSnapshot.mk.sizeOf_spec : ∀ (toSnapshot : Lean.Language.Snapshot) (stx : Lean.Syntax) (parserState : Lean.Parser.ModuleParserState)
  (elabSnap : Lean.Language.Lean.CommandElaboratingSnapshot)
  (nextCmdSnap? : Option (Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot)),
  sizeOf
      { toSnapshot := toSnapshot, stx := stx, parserState := parserState, elabSnap := elabSnap,
        nextCmdSnap? := nextCmdSnap? } =
    1 + sizeOf toSnapshot + sizeOf stx + sizeOf parserState + sizeOf elabSnap + sizeOf nextCmdSnap?
-- Mathlib.Data.Matrix.Basic
Equiv.mapMatrix_apply : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_11} {β : Type u_12} (f : α ≃ β) (M : Matrix m n α), f.mapMatrix M = M.map ⇑f
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.div2Shift : USize → USize → USize
-- Mathlib.GroupTheory.PushoutI
/-- The intersection of the images of the maps from any two distinct groups in the diagram
into the amalgamated product is the image of the map from the base group in the diagram.  -/
Monoid.PushoutI.inf_of_range_eq_base_range : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i},
  (∀ (i : ι), Function.Injective ⇑(φ i)) →
    ∀ {i j : ι}, i ≠ j → (Monoid.PushoutI.of i).range ⊓ (Monoid.PushoutI.of j).range = (Monoid.PushoutI.base φ).range
-- Mathlib.Algebra.Order.Floor.Ring
Int.ceil_le_floor_add_one : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] (a : R), ⌈a⌉ ≤ ⌊a⌋ + 1
-- Mathlib.Algebra.Group.Prod
Prod.instAddLeftCancelSemigroup.eq_1 : ∀ {G : Type u_1} {H : Type u_2} [inst : AddLeftCancelSemigroup G] [inst_1 : AddLeftCancelSemigroup H],
  Prod.instAddLeftCancelSemigroup = { toAddSemigroup := Prod.instAddSemigroup, toIsLeftCancelAdd := ⋯ }
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.vlt_of_vlt_of_veq : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x y z : R}, x <ᵥ y → y =ᵥ z → x <ᵥ z
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.natDegree_derivative_lt : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R},
  p.natDegree ≠ 0 → (Polynomial.derivative p).natDegree < p.natDegree
-- Mathlib.Analysis.Calculus.Gradient.Basic
HasGradientWithinAt.congr_of_mem : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {f' x : F} {s : Set F} {f₁ : F → 𝕜},
  HasGradientWithinAt f f' s x → (∀ x ∈ s, f₁ x = f x) → x ∈ s → HasGradientWithinAt f₁ f' s x
-- Mathlib.Data.Semiquot
Semiquot.blur_eq_blur' : ∀ {α : Type u_1} (q : Semiquot α) (s : Set α) (h : q.s ⊆ s), Semiquot.blur s q = q.blur' h
-- Std.Data.DTreeMap.Internal.Balancing
/-- A double left rotation.  -/
Std.DTreeMap.Internal.Impl.doubleL : {α : Type u} →
  {β : α → Type v} →
    (k : α) →
      β k →
        Std.DTreeMap.Internal.Impl α β →
          (rk : α) →
            β rk →
              (rlk : α) →
                β rlk →
                  Std.DTreeMap.Internal.Impl α β →
                    Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β
-- Mathlib.Tactic.Sat.FromLRAT
/-- Asserts that `¬⟦f⟧_v` implies `p`.  -/
Sat.Fmla.reify : Sat.Valuation → Sat.Fmla → Prop → Prop
-- Mathlib.RingTheory.MatrixAlgebra
kroneckerTMulLinearEquiv_one : ∀ (m : Type u_2) (n : Type u_3) (R : Type u_5) (S : Type u_6) (A : Type u_7) {B : Type u_8} [inst : CommSemiring R]
  [inst_1 : Semiring S] [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] [inst_7 : Fintype m] [inst_8 : Fintype n] [inst_9 : DecidableEq m] [inst_10 : DecidableEq n]
  [inst_11 : Module S A] [inst_12 : IsScalarTower R S A], (kroneckerTMulLinearEquiv m m n n R S A B) 1 = 1
-- Mathlib.Analysis.InnerProductSpace.LinearPMap
LinearPMap.isSelfAdjoint_def : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] {A : E →ₗ.[𝕜] E}, IsSelfAdjoint A ↔ A.adjoint = A
-- Mathlib.Algebra.Star.Pointwise
Set.instInvolutiveStar : {α : Type u_1} → [InvolutiveStar α] → InvolutiveStar (Set α)
-- Init.Data.List.Sublist
List.IsPrefix.filterMap : ∀ {α : Type u_1} {β : Type u_2} (f : α → Option β) ⦃l₁ l₂ : List α⦄,
  l₁ <+: l₂ → List.filterMap f l₁ <+: List.filterMap f l₂
-- Mathlib.Topology.MetricSpace.Cover
Metric.IsCover.mono : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {ε : NNReal} {s N₁ N₂ : Set X},
  N₁ ⊆ N₂ → Metric.IsCover ε s N₁ → Metric.IsCover ε s N₂
-- Mathlib.Topology.Order.LowerUpperTopology
/-- The lower topology is the topology generated by the complements of the left-closed right-infinite
intervals.
 -/
Topology.lower : (α : Type u_1) → [Preorder α] → TopologicalSpace α
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.cokernelIsoOfEq_hom_comp_desc_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y Z : C}
  {f g : X ⟶ Y} [inst_2 : CategoryTheory.Limits.HasCokernel f] [inst_3 : CategoryTheory.Limits.HasCokernel g]
  (h : f = g) (e : Y ⟶ Z) (he : CategoryTheory.CategoryStruct.comp g e = 0) {Z_1 : C} (h_1 : Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernelIsoOfEq h).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.desc g e he) h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.desc f e ⋯) h_1
-- Mathlib.Order.SymmDiff
bihimp_bot : ∀ {α : Type u_2} [inst : HeytingAlgebra α] (a : α), bihimp a ⊥ = aᶜ
-- Init.Omega.LinearCombo
Lean.Omega.LinearCombo.sub_const : ∀ {l₁ l₂ : Lean.Omega.LinearCombo}, (l₁ - l₂).const = l₁.const - l₂.const
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.get?_union_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∉ t₂ → (t₁ ∪ t₂).get? k = t₁.get? k
-- Mathlib.Data.Finset.Image
Equiv.finsetSubtypeComm_apply_coe : ∀ {α : Type u_1} (p : α → Prop) (s : Finset { a // p a }),
  ↑((Equiv.finsetSubtypeComm p) s) = Finset.map { toFun := fun a => ↑a, inj' := ⋯ } s
-- Mathlib.Data.WSeq.Basic
/-- Turn a list into a weak sequence  -/
Stream'.WSeq.ofList : {α : Type u} → List α → Stream'.WSeq α
-- Mathlib.RingTheory.Etale.Finite
Algebra.TensorProduct.liftEquivRight.congr_simp : ∀ (R : Type uR) (S : Type uS) (B : Type uB) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (C : Type u_3) [inst_5 : CommRing C] [inst_6 : Algebra R C]
  [inst_7 : Algebra S C] [inst_8 : IsScalarTower R S C],
  Algebra.TensorProduct.liftEquivRight R S B C = Algebra.TensorProduct.liftEquivRight R S B C
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- An angle in a right-angled triangle expressed using `arctan`, version subtracting vectors.  -/
Orientation.oangle_sub_right_eq_arctan_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V},
  o.oangle x y = ↑(Real.pi / 2) → o.oangle y (y - x) = ↑(Real.arctan (‖x‖ / ‖y‖))
-- Mathlib.Topology.Algebra.Order.LiminfLimsup
le_limsup_mul : ∀ {ι : Type u_1} {f : Filter ι} {u v : ι → ℝ},
  (∃ᶠ (x : ι) in f, 0 ≤ u x) →
    Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u →
      0 ≤ᶠ[f] v →
        Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v →
          Filter.limsup u f * Filter.liminf v f ≤ Filter.limsup (u * v) f
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.contStack.eq_2 : ∀ (c : Turing.ToPartrec.Code) (a : List ℕ) (k : Turing.ToPartrec.Cont),
  Turing.PartrecToTM2.contStack (Turing.ToPartrec.Cont.cons₁ c a k) = a :: Turing.PartrecToTM2.contStack k
-- Lean.Meta.Tactic.Cleanup
/-- Auxiliary tactic for cleaning the local context. It removes local declarations (aka hypotheses) that are *not* relevant.
We say a variable `x` is "relevant" if
- It occurs in the `toPreserve` array, or
- It occurs in the target type, or
- There is a relevant variable `y` that depends on `x`, or
- If `indirectProps` is true, the type of `x` is a proposition and it depends on a relevant variable `y`.
- If `indirectProps` is true, `x` is a local declaration and its value mentions a relevant variable `y`.

By default, `toPreserve := #[]` and `indirectProps := true`. These settings are used in the mathlib tactic `extract_goal`
to give the user more control over which variables to include.
 -/
Lean.MVarId.cleanup : Lean.MVarId → optParam (Array Lean.FVarId) #[] → optParam Bool true → Lean.MetaM Lean.MVarId
-- Mathlib.Order.Interval.Finset.Nat
Nat.card_uIcc : ∀ (a b : ℕ), (Finset.uIcc a b).card = (↑b - ↑a).natAbs + 1
-- Mathlib.RingTheory.MvPowerSeries.GaussNorm
MvPowerSeries.Finset.Nonempty.map_sum_le_sup'_map : ∀ {α : Type u_5} {S : Type u_6} [inst : LinearOrder S] [inst_1 : AddCommMonoid α] (g : α → S) {ι : Type u_7}
  {s : Finset ι} (hs : s.Nonempty) (f : ι → α),
  (∀ (a b : α), g (a + b) ≤ max (g a) (g b)) → g (∑ i ∈ s, f i) ≤ s.sup' hs fun x => g (f x)
-- Mathlib.CategoryTheory.FiberedCategory.Grothendieck
CategoryTheory.Pseudofunctor.CoGrothendieck.ι_map_base : ∀ {𝒮 : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} 𝒮]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat) (S : 𝒮)
  {a b : ↑(F.obj { as := Opposite.op S })} (φ : a ⟶ b),
  ((CategoryTheory.Pseudofunctor.CoGrothendieck.ι F S).map φ).base = CategoryTheory.CategoryStruct.id S
-- Mathlib.Data.Finset.Sort
Finset.sort_nodup : ∀ {α : Type u_1} (s : Finset α) (r : α → α → Prop) [inst : DecidableRel r] [inst_1 : IsTrans α r]
  [inst_2 : Std.Antisymm r] [inst_3 : Std.Total r], (s.sort r).Nodup
-- Lean.Attributes
Lean.AttributeImplCore.mk.injEq : ∀ (ref : autoParam Lean.Name Lean.AttributeImplCore.ref._autoParam) (name : Lean.Name) (descr : String)
  (applicationTime : Lean.AttributeApplicationTime) (ref_1 : autoParam Lean.Name Lean.AttributeImplCore.ref._autoParam)
  (name_1 : Lean.Name) (descr_1 : String) (applicationTime_1 : Lean.AttributeApplicationTime),
  ({ ref := ref, name := name, descr := descr, applicationTime := applicationTime } =
      { ref := ref_1, name := name_1, descr := descr_1, applicationTime := applicationTime_1 }) =
    (ref = ref_1 ∧ name = name_1 ∧ descr = descr_1 ∧ applicationTime = applicationTime_1)
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.coeff_X : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : DecidableEq σ] (i : σ) (m : σ →₀ ℕ),
  MvPolynomial.coeff m (MvPolynomial.X i) = if (fun₀ | i => 1) = m then 1 else 0
-- Mathlib.Algebra.BigOperators.Intervals
Finset.prod_Ioc_consecutive : ∀ {M : Type u_3} [inst : CommMonoid M] (f : ℕ → M) {m n k : ℕ},
  m ≤ n → n ≤ k → (∏ i ∈ Finset.Ioc m n, f i) * ∏ i ∈ Finset.Ioc n k, f i = ∏ i ∈ Finset.Ioc m k, f i
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.Functor.instAdditiveObjWhiskeringRight : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : CategoryTheory.Preadditive D] [inst_4 : CategoryTheory.Preadditive E] (F : CategoryTheory.Functor D E)
  [F.Additive], ((CategoryTheory.Functor.whiskeringRight C D E).obj F).Additive
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.lift'_unique : ∀ {α : Type u_1} {β : Type u_2} [inst : MulOneClass α] [inst_1 : MulZeroOneClass β] (f : WithZero α →*₀ β),
  f = WithZero.lift' ((↑f).comp WithZero.coeMonoidHom)
-- Mathlib.CategoryTheory.Sites.Descent.Precoverage
_private.Mathlib.CategoryTheory.Sites.Descent.Precoverage.0.CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.comm_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat}
  {J : CategoryTheory.GrothendieckTopology C} [inst_1 : F.IsPrestack J] {ι : Type t} {S : C} {X : ι → C}
  {f : (i : ι) → X i ⟶ S} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S} {α : ι' → ι}
  {p' : (j : ι') → X' j ⟶ X (α j)} (w : ∀ (j : ι'), CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) = f' j)
  (hf' : CategoryTheory.Sieve.ofArrows X' f' ∈ J S) {D₁ D₂ : F.DescentData f}
  (φ :
    (CategoryTheory.Pseudofunctor.DescentData.pullFunctor F ⋯).obj D₁ ⟶
      (CategoryTheory.Pseudofunctor.DescentData.pullFunctor F ⋯).obj D₂)
  ⦃W : C⦄ (q : W ⟶ S) ⦃i₁ i₂ : ι⦄ (f₁ : W ⟶ X i₁) (f₂ : W ⟶ X i₂)
  (hf₁ :
    autoParam (CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q)
      CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.comm._auto_1✝)
  (hf₂ :
    autoParam (CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q)
      CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.comm._auto_3✝)
  {Z : ↑(F.obj { as := Opposite.op W })} (h : (F.map f₂.op.toLoc).toFunctor.obj (D₂.obj i₂) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      ((F.map f₁.op.toLoc).toFunctor.map (CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.hom✝ w hf' φ i₁))
      (CategoryTheory.CategoryStruct.comp (D₂.hom q f₁ f₂ ⋯ ⋯) h) =
    CategoryTheory.CategoryStruct.comp (D₁.hom q f₁ f₂ ⋯ ⋯)
      (CategoryTheory.CategoryStruct.comp
        ((F.map f₂.op.toLoc).toFunctor.map (CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.hom✝ w hf' φ i₂))
        h)
-- Mathlib.Order.GaloisConnection.Basic
GaloisInsertion.l_iInf_u : ∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  (gi : GaloisInsertion l u) {ι : Sort x} (f : ι → β), l (⨅ i, u (f i)) = ⨅ i, f i
-- Std.Data.HashSet.Basic
Std.HashSet.instMembership : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → Membership α (Std.HashSet α)
-- Lean.DeclarationRange
Lean.findDeclarationRanges? : {m : Type → Type} →
  [Monad m] → [Lean.MonadEnv m] → [MonadLiftT BaseIO m] → Lean.Name → m (Option Lean.DeclarationRanges)
-- Init.Data.List.Basic
List.lengthTRAux.eq_2 : ∀ {α : Type u_1} (x : ℕ) (head : α) (as : List α), (head :: as).lengthTRAux x = as.lengthTRAux x.succ
-- Mathlib.Computability.Primrec.Basic
PrimrecPred.and : ∀ {α : Type u_1} [inst : Primcodable α] {p q : α → Prop}, PrimrecPred p → PrimrecPred q → PrimrecPred fun a => p a ∧ q a
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRk_eq_eRk_of_subset_of_le : ∀ {α : Type u_1} {M : Matroid α} {X Y : Set α}, X ⊆ Y → M.eRk Y ≤ M.eRk X → M.eRk X = M.eRk Y
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.self_le_maxKey_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, (cmp k ((t.insert k v).maxKey ⋯)).isLE = true
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.hom_tensorHom : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G] {X₁ X₂ Y₁ Y₂ : Rep.{u, u, v} k G} (f : X₁ ⟶ Y₁)
  (g : X₂ ⟶ Y₂),
  Rep.Hom.hom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) = (Rep.Hom.hom f).tensor (Rep.Hom.hom g)
-- Init.GrindInstances.Ring.SInt
Lean.Grind.Int32.intCast_ofNat : ∀ (x : ℕ), ↑(OfNat.ofNat x) = OfNat.ofNat x
-- Mathlib.Topology.Category.DeltaGenerated
/-- The forgetful functor `DeltaGenerated ⥤ TopCat`  -/
DeltaGenerated.deltaGeneratedToTop : CategoryTheory.Functor DeltaGenerated TopCat
-- Init.Data.SInt.Lemmas
Int16.mul_add : ∀ {a b c : Int16}, a * (b + c) = a * b + a * c
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
differentiableAt_sigmoid : ∀ {x : ℝ}, DifferentiableAt ℝ Real.sigmoid x
-- Mathlib.CategoryTheory.IsoCat
CategoryTheory.Functor.objEquiv.congr_simp : ∀ {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] (F F_1 : CategoryTheory.Functor C D) (e_F : F = F_1)
  [inst_2 : F.IsIso], F.objEquiv = F_1.objEquiv
-- Mathlib.Computability.TuringMachine.Computable
Turing.TM2ComputableInTime.toTM2ComputableAux : {α β αΓ βΓ : Type} →
  {ea : α → List αΓ} →
    {eb : β → List βΓ} → {f : α → β} → Turing.TM2ComputableInTime ea eb f → Turing.TM2ComputableAux αΓ βΓ
-- Mathlib.RingTheory.Conductor
mem_conductor_iff : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {x y : S},
  y ∈ conductor R x ↔ ∀ (b : S), y * b ∈ R[x]
-- Mathlib.RingTheory.Regular.RegularSequence
RingTheory.Sequence.IsWeaklyRegular.isWeaklyRegular_rTensor : ∀ {R : Type u_1} {M : Type u_3} {M₂ : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] [Module.Flat R M₂] {rs : List R},
  RingTheory.Sequence.IsWeaklyRegular M rs → RingTheory.Sequence.IsWeaklyRegular (TensorProduct R M M₂) rs
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.instZero : (A : Type u_3) → (E : Type u_4) → [Zero E] → Zero (WithCStarModule A E)
-- Mathlib.Analysis.Analytic.Composition
FormalMultilinearSeries.comp_assoc : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [inst_7 : NormedAddCommGroup H] [inst_8 : NormedSpace 𝕜 H]
  (r : FormalMultilinearSeries 𝕜 G H) (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F),
  (r.comp q).comp p = r.comp (q.comp p)
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.F_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X : C} {J : Type w}
  [inst_2 : CategoryTheory.SmallCategory J] {Y : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone Y}
  (z : X ⟶ c.pt) [inst_3 : CategoryTheory.Mono c.ι] (j : J),
  (CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.F z).obj j =
    CategoryTheory.MonoOver.mk ((CategoryTheory.Limits.pullback.snd c.ι ((CategoryTheory.Functor.const J).map z)).app j)