mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.LineDeriv.Measurable
stronglyMeasurable_lineDeriv_uncurry : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [LocallyCompactSpace 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : MeasurableSpace E] [OpensMeasurableSpace E]
  {F : Type u_3} [inst_6 : NormedAddCommGroup F] [inst_7 : NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F}
  [SecondCountableTopology E], Continuous f → MeasureTheory.StronglyMeasurable fun p => lineDeriv 𝕜 f p.1 p.2
-- Mathlib.CategoryTheory.Discrete.Basic
/-- `piEquivalenceFunctorDiscrete` is compatible with `evaluation`.  -/
CategoryTheory.piEquivalenceFunctorDiscreteCompEvaluationIso : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {J : Type u_2} →
      (j : J) →
        (CategoryTheory.piEquivalenceFunctorDiscrete J C).functor.comp
            ((CategoryTheory.evaluation (CategoryTheory.Discrete J) C).obj { as := j }) ≅
          CategoryTheory.Pi.eval (fun a => C) j
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardSliceSearcher.isRevMatch_iff : ∀ {pat s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsRevMatch pat pos ↔ (s.sliceFrom pos).copy = pat.copy
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
SimpleGraph.completeMultipartiteGraph.isCompleteMultipartite : ∀ {ι : Type u_1} (V : ι → Type u_2), (SimpleGraph.completeMultipartiteGraph V).IsCompleteMultipartite
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.range_zero : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N], AddMonoidHom.range 0 = ⊥
-- Mathlib.Data.PEquiv
PEquiv.symm_single : ∀ {α : Type u} {β : Type v} [inst : DecidableEq α] [inst_1 : DecidableEq β] (a : α) (b : β),
  (PEquiv.single a b).symm = PEquiv.single b a
-- Mathlib.Tactic.Linter.HashCommandLinter
/-- Checks that no command beginning with `#` is present in 'Mathlib',
except for the ones in `allowed_commands`.

If `warningAsError` is `true`, then the linter logs an info (rather than a warning).
This means that CI will eventually fail on `#`-commands, but does not stop it from continuing.

However, in order to avoid local clutter, when `warningAsError` is `false`, the linter
logs a warning only for the `#`-commands that do not already emit a message.  -/
_private.Mathlib.Tactic.Linter.HashCommandLinter.0.Mathlib.Linter.HashCommandLinter.hashCommandLinter : Lean.Linter
-- Mathlib.InformationTheory.KullbackLeibler.KLFun
InformationTheory.klFun_zero : InformationTheory.klFun 0 = 1
-- Lean.Parser.Types
Lean.Parser.ParserModuleContext.options : Lean.Parser.ParserModuleContext → Lean.Options
-- Init.Data.List.Impl
List.foldr_eq_foldrTR : @List.foldr = @List.foldrTR
-- Mathlib.Data.Finset.SDiff
Finset.sdiff_sdiff_eq_self : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, t ⊆ s → s \ (s \ t) = t
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.hasLimit_rightOp_of_hasColimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor Jᵒᵖ C) [CategoryTheory.Limits.HasColimit F], CategoryTheory.Limits.HasLimit F.rightOp
-- Mathlib.Algebra.GroupWithZero.InjSurj
/-- Push forward a `SemigroupWithZero` along a surjective function.
See note [reducible non-instances].  -/
Function.Surjective.semigroupWithZero : {M₀ : Type u_1} →
  {M₀' : Type u_3} →
    [inst : SemigroupWithZero M₀] →
      [inst_1 : Zero M₀'] →
        [inst_2 : Mul M₀'] →
          (f : M₀ → M₀') →
            Function.Surjective f → f 0 = 0 → (∀ (x y : M₀), f (x * y) = f x * f y) → SemigroupWithZero M₀'
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.le_arcsin_iff_sin_le' : ∀ {x y : ℝ}, x ∈ Set.Ioc (-(Real.pi / 2)) (Real.pi / 2) → (x ≤ Real.arcsin y ↔ Real.sin x ≤ y)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.Stmt.load.sizeOf_spec : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [inst : SizeOf K] [inst_1 : (a : K) → SizeOf (Γ a)]
  [inst_2 : SizeOf Λ] [inst_3 : SizeOf σ] (a : σ → σ) (a_1 : Turing.TM2.Stmt Γ Λ σ),
  sizeOf (Turing.TM2.Stmt.load a a_1) = 1 + sizeOf a_1
-- Mathlib.Combinatorics.Graph.Basic
/-- `V(G)` denotes the `vertexSet` of a graph `G`.  -/
Graph.«termV(_)» : Lean.ParserDescr
-- Mathlib.Data.Finset.Insert
Finset.mem_of_mem_cons_of_ne : ∀ {α : Type u_1} {s : Finset α} {a : α} {has : a ∉ s} {i : α}, i ∈ Finset.cons a s has → i ≠ a → i ∈ s
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.opOpEquivalence_counitIso : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C],
  (CategoryTheory.opOpEquivalence C).counitIso =
    CategoryTheory.Iso.refl ((CategoryTheory.opOp C).comp (CategoryTheory.unopUnop C))
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.ConnectionState.requiresData : {β : Type} → Std.Http.Server.Connection.ConnectionState✝ β → Bool
-- Mathlib.Algebra.Quaternion
Quaternion.instRatCast : {R : Type u_1} → [inst : Field R] → RatCast (Quaternion R)
-- Mathlib.Order.RelIso.Basic
RelIso.toEquiv : {α : Type u_5} → {β : Type u_6} → {r : α → α → Prop} → {s : β → β → Prop} → r ≃r s → α ≃ β
-- Mathlib.Data.Set.Lattice.Image
Set.image_sUnion : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set (Set α)}, f '' ⋃₀ s = ⋃₀ (Set.image f '' s)
-- Mathlib.Topology.Covering.Basic
IsCoveringMap.homeomorph_comp_iff : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {Y : Type u_3}
  [inst_2 : TopologicalSpace Y] (g : X ≃ₜ Y), IsCoveringMap (⇑g ∘ f) ↔ IsCoveringMap f
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.orthogonalProjectionOnto_orthogonal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} [inst_3 : K.HasOrthogonalProjection] (u : E),
  Kᗮ.orthogonalProjectionOnto u = ⟨u - K.starProjection u, ⋯⟩
-- Mathlib.CategoryTheory.IsConnected
CategoryTheory.IsPreconnected.prod : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  [CategoryTheory.IsPreconnected J] [CategoryTheory.IsPreconnected K], CategoryTheory.IsPreconnected (J × K)
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.volume_pi_Ioc : ∀ {ι : Type u_1} [inst : Fintype ι] {a b : ι → ℝ},
  MeasureTheory.volume (Set.univ.pi fun i => Set.Ioc (a i) (b i)) = ∏ i, ENNReal.ofReal (b i - a i)
-- Mathlib.Analysis.SpecialFunctions.Log.Deriv
/-- Compute the derivative of the difference between $\frac{1}{2} * \log(\frac{1+x}{1-x})$ and its
Taylor series at `0` up to order `n`. This is an auxiliary lemma for
`sum_range_sub_log_div_le` and `sum_range_le_log_div`.
Note that thanks to the geometric series, the derivative has a particularly simple form, and means
that it is more convenient to avoid Taylor's theorem.
 -/
Real.hasDerivAt_half_log_one_add_div_one_sub_sub_sum_range : ∀ {y : ℝ} (n : ℕ),
  -1 < y →
    y < 1 →
      HasDerivAt (fun x => 1 / 2 * Real.log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (2 * ↑i + 1))
        ((y ^ 2) ^ n / (1 - y ^ 2)) y
-- Mathlib.Data.Fin.Rev
Fin.rev_add_cast : ∀ {n : ℕ} (j : Fin (n + 1)), ↑j.rev + ↑j = n
-- Init.Core
/-- Lifts a function from an underlying type to a function on a quotient, requiring that it respects the
quotient's equivalence relation.

Given `s : Setoid α` and a quotient `Quotient s`, applying a function `f : α → β` requires a proof
`h` that `f` respects the equivalence relation `s.r`. In this case, the function
`Quotient.lift f h : Quotient s → β` computes the same values as `f`.

`Quotient.liftOn` is a version of this operation that takes the quotient value as its first explicit
parameter.
 -/
Quotient.lift : {α : Sort u} → {β : Sort v} → {s : Setoid α} → (f : α → β) → (∀ (a b : α), a ≈ b → f a = f b) → Quotient s → β
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.pseudofunctor_toPrelaxFunctor : CategoryTheory.WithInitial.pseudofunctor.toPrelaxFunctor = CategoryTheory.WithInitial.prelaxfunctor
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.map_coe_toMulEquiv : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_5}
  [inst_2 : EquivLike F M N] [inst_3 : MulEquivClass F M N] (f : F) (S : Submonoid M),
  Submonoid.map (↑f) S = Submonoid.map f S
-- Batteries.Data.List.Lemmas
List.sum_concat : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Zero α] [Std.LawfulIdentity (fun x1 x2 => x1 + x2) 0]
  [Std.Associative fun x1 x2 => x1 + x2] {l : List α} {a : α}, (l.concat a).sum = l.sum + a
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.mem_of_mem_filter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool} {k : α}, k ∈ Std.ExtTreeMap.filter f t → k ∈ t
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.getEntryGTD_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {fallback : (a : α) × β a}, t₁.Equiv t₂ → t₁.getEntryGTD k fallback = t₂.getEntryGTD k fallback
-- Mathlib.Order.Quotient
Quotient.lift_monotone : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] {s : Setoid α} [inst_1 : Preorder β] (f : α → β),
  Monotone f → ∀ (H : ∀ (x₁ x₂ : α), x₁ ≈ x₂ → f x₁ = f x₂), Monotone (Quotient.lift f H)
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.shortComplexOfDistTriangleIsoOfIso_hom_τ₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C]
  {T T' : CategoryTheory.Pretriangulated.Triangle C} (e : T ≅ T')
  (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles),
  (CategoryTheory.Pretriangulated.shortComplexOfDistTriangleIsoOfIso e hT).hom.τ₁ = e.hom.hom₁
-- Mathlib.RingTheory.Localization.Away.Basic
/-- `AlgHom` version of `IsLocalization.Away.lift`.  -/
IsLocalization.Away.liftAlgHom : {R : Type u_1} →
  [inst : CommSemiring R] →
    {S : Type u_2} →
      [inst_1 : CommSemiring S] →
        [inst_2 : Algebra R S] →
          {P : Type u_3} →
            [inst_3 : CommSemiring P] →
              (x : R) →
                [IsLocalization.Away x S] →
                  {A : Type u_4} →
                    [inst_5 : CommSemiring A] →
                      [inst_6 : Algebra A R] →
                        [inst_7 : Algebra A S] →
                          [inst_8 : Algebra A P] → [IsScalarTower A R S] → {f : R →ₐ[A] P} → IsUnit (f x) → S →ₐ[A] P
-- Mathlib.Topology.UniformSpace.AbstractCompletion
AbstractCompletion.inseparable_extend_coe : ∀ {α : Type uα} [inst : UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {β : Type uβ} [inst_1 : UniformSpace β]
  {f : α → β}, UniformContinuous f → ∀ (x : α), Inseparable (pkg.extend f (pkg.coe x)) (f x)
-- Mathlib.Topology.Algebra.Valued.ValuativeRel
_private.Mathlib.Topology.Algebra.Valued.ValuativeRel.0.IsValuativeTopology.termV : Lean.ParserDescr
-- Mathlib.CategoryTheory.ObjectProperty.Comma
CategoryTheory.ObjectProperty.instIsStableUnderRetractsCommaComma : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D]
  (F₁ : CategoryTheory.Functor C₁ D) (F₂ : CategoryTheory.Functor C₂ D) (P₁ : CategoryTheory.ObjectProperty C₁)
  (P₂ : CategoryTheory.ObjectProperty C₂) [P₁.IsStableUnderRetracts] [P₂.IsStableUnderRetracts],
  (CategoryTheory.ObjectProperty.comma F₁ F₂ P₁ P₂).IsStableUnderRetracts
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst.sizeOf_spec : ∀ (n : ℕ), sizeOf (Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst n) = 1 + sizeOf n
-- Mathlib.Data.List.NodupEquivFin
/-- Alternative phrasing of `List.Nodup.getEquivOfForallMemList` using `List.count`.  -/
List.getEquivOfForallCountEqOne : {α : Type u_1} → [inst : DecidableEq α] → (l : List α) → (∀ (x : α), List.count x l = 1) → Fin l.length ≃ α
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
ApproximatesLinearOn.mono_set : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {s t : Set E} {c : NNReal}, s ⊆ t → ApproximatesLinearOn f f' t c → ApproximatesLinearOn f f' s c
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKey!_ofList_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp]
  [inst_2 : Inhabited α] {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false → (Std.DTreeMap.Raw.Const.ofList l cmp).getKey! k = default
-- Mathlib.GroupTheory.Perm.Fin
cycleType_finRotate_of_le : ∀ {n : ℕ}, 2 ≤ n → (finRotate n).cycleType = {n}
-- Mathlib.Algebra.Module.Defs
two_smul : ∀ (R : Type u_1) {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x : M),
  2 • x = x + x
-- Init.Data.UInt.Lemmas
UInt64.ofNat.eq_1 : ∀ (n : ℕ), UInt64.ofNat n = { toBitVec := BitVec.ofNat 64 n }
-- Std.Data.TreeMap.Basic
/-- Returns `true` if there is a mapping for the given key `a` or a key that is equal to `a` according
to the comparator `cmp`. There is also a `Prop`-valued version
of this: `a ∈ t` is equivalent to `t.contains a = true`.

Observe that this is different behavior than for lists: for lists, `∈` uses `=` and `contains` uses
`==` for equality checks, while for tree maps, both use the given comparator `cmp`.
 -/
Std.TreeMap.contains : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → α → Bool
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric
_private.Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric.0.«term⟪_,_⟫» : Lean.ParserDescr
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.combine'.match_3.congr_eq_2 : ∀ (motive : ℕ → Sort u_1) (fuel : ℕ) (h_1 : Unit → motive 0) (h_2 : (fuel : ℕ) → motive fuel.succ) (fuel_1 : ℕ),
  fuel = fuel_1.succ →
    (match fuel with
      | 0 => h_1 ()
      | fuel.succ => h_2 fuel) ≍
      h_2 fuel_1
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
CategoryTheory.Functor.partialLeftAdjointHomEquiv_map_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor D C) {X X' : F.PartialLeftAdjointSource} {Y : D} (f : X ⟶ X')
  (g : F.partialLeftAdjointObj X' ⟶ Y),
  F.partialLeftAdjointHomEquiv (CategoryTheory.CategoryStruct.comp (F.partialLeftAdjointMap f) g) =
    CategoryTheory.CategoryStruct.comp f.hom (F.partialLeftAdjointHomEquiv g)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.sum_congr : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {f : SkewMonoidAlgebra k G} {M : Type u_3}
  [inst_1 : AddCommMonoid M] {g₁ g₂ : G → k → M},
  (∀ x ∈ f.support, g₁ x (f.coeff x) = g₂ x (f.coeff x)) → f.sum g₁ = f.sum g₂
-- Lean.Data.PersistentArray
Lean.PersistentArray.popLeaf : {α : Type u} → Lean.PersistentArrayNode α → Option (Array α) × Array (Lean.PersistentArrayNode α)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
/-- The additive equivalence `Cocycle K L n ≃+ Cocycle K⟦a⟧ L n'` when `n + a = n'`.  -/
CochainComplex.HomComplex.Cocycle.leftShiftAddEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {K L : CochainComplex C ℤ} →
        (n a n' : ℤ) →
          n + a = n' →
            CochainComplex.HomComplex.Cocycle K L n ≃+
              CochainComplex.HomComplex.Cocycle ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'
-- Lean.Meta.CongrTheorems
Lean.Meta.CongrArgKind.noConfusionType : Sort v✝ → Lean.Meta.CongrArgKind → Lean.Meta.CongrArgKind → Sort v✝
-- Aesop.Tree.Data
Aesop.NodeState.proven : Aesop.NodeState
-- Mathlib.Analysis.Normed.Module.Bases
/-- The projections converge pointwise to the identity.  -/
SchauderBasis.RankOneDecomposition.proj_tendsto : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {X : Type u_2} [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] (self : SchauderBasis.RankOneDecomposition 𝕜 X) (x : X),
  Filter.Tendsto (fun n => (self.P n) x) Filter.atTop (nhds x)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.liftEquiv_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {T X Y : C} (f : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X Y),
  CategoryTheory.CartesianMonoidalCategory.liftEquiv.symm f =
    (CategoryTheory.CategoryStruct.comp f (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y),
      CategoryTheory.CategoryStruct.comp f (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y))
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.mapA.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (a : α) (as : List α) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (as : List α) → motive (a :: as)),
  (match a :: as with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_2 a as
-- Lean.Data.FuzzyMatching
/-- Represents the type of a single character.  -/
Lean.FuzzyMatching.CharType : Type
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.StrongTrans.Modification.whiskerLeft_naturality : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} (Γ : CategoryTheory.Oplax.StrongTrans.Modification η θ)
  {b c : B} {a' : C} (f : a' ⟶ F.obj b) (g : b ⟶ c),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft (F.map g) (Γ.app c)))
      (CategoryTheory.Bicategory.whiskerLeft f (θ.naturality g).hom) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (η.naturality g).hom)
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight (Γ.app b) (G.map g)))
-- Init.Data.Int.Order
Int.lt.intro : ∀ {a b : ℤ} {n : ℕ}, a + (↑n + 1) = b → a < b
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.isIso_iff_isIso_stalkMap : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  CategoryTheory.IsIso f ↔
    CategoryTheory.IsIso f.base ∧ ∀ (x : ↥X), CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.stalkMap f x)
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.neg_hom₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C} [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (f : T₁ ⟶ T₂), (-f).hom₃ = -f.hom₃
-- Mathlib.Util.Notation3
Mathlib.Notation3.BoundValueType.foldr.sizeOf_spec : sizeOf Mathlib.Notation3.BoundValueType.foldr = 1
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.summable_toNNReal_of_tsum_ne_top : ∀ {α : Type u_4} {f : α → ENNReal}, ∑' (i : α), f i ≠ ⊤ → Summable (ENNReal.toNNReal ∘ f)
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.findM?.eq_1 : ∀ {m : Type → Type u_1} {α : Type} [inst : Monad m] (p : α → m Bool) (as : Array α),
  Array.findM? p as = do
    let __s ←
      forIn as (none, ()) fun a __s => do
          let __do_lift ← p a
          if __do_lift = true then pure (ForInStep.done (some (some a), ())) else pure (ForInStep.yield (none, ()))
    have __r : Option (Option α) × Unit := __s
    match __r.1 with
      | some r => pure r
      | none => pure none
-- Mathlib.Algebra.Homology.ShortComplex.ShortExact
/-- A short complex `S` is short exact if it is exact, `S.f` is a mono and `S.g` is an epi.  -/
CategoryTheory.ShortComplex.ShortExact : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → CategoryTheory.ShortComplex C → Prop
-- Mathlib.Tactic.ProdAssoc
Lean.Expr.ProdTree.prod : Lean.Expr.ProdTree → Lean.Expr.ProdTree → Lean.Level → Lean.Level → Lean.Expr.ProdTree
-- Mathlib.Algebra.BigOperators.Ring.List
List.prod_map_neg : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : HasDistribNeg M] (l : List M),
  (List.map Neg.neg l).prod = (-1) ^ l.length * l.prod
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.comp_neg : ∀ {R : Type u_1} [inst : Ring R] {R₂ : Type u_2} [inst_1 : Ring R₂] {R₃ : Type u_3} [inst_2 : Ring R₃] {M : Type u_4}
  [inst_3 : TopologicalSpace M] [inst_4 : AddCommGroup M] {M₂ : Type u_5} [inst_5 : TopologicalSpace M₂]
  [inst_6 : AddCommGroup M₂] {M₃ : Type u_6} [inst_7 : TopologicalSpace M₃] [inst_8 : AddCommGroup M₃]
  [inst_9 : Module R M] [inst_10 : Module R₂ M₂] [inst_11 : Module R₃ M₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃}
  {σ₁₃ : R →+* R₃} [inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_13 : IsTopologicalAddGroup M₂]
  [inst_14 : IsTopologicalAddGroup M₃] (g : M₂ →SL[σ₂₃] M₃) (f : M →SL[σ₁₂] M₂), g ∘SL (-f) = -g ∘SL f
-- Std.Data.HashMap.Lemmas
Std.HashMap.get!_emptyWithCapacity : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : Inhabited β] {a : α} {c : ℕ},
  (Std.HashMap.emptyWithCapacity c).get! a = default
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.is3Clique_iff : ∀ {α : Type u_1} {G : SimpleGraph α} {s : Finset α} [inst : DecidableEq α],
  G.IsNClique 3 s ↔ ∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.map_map_zero_le : ∀ (f g : CircleDeg1Lift), f (g 0) ≤ f 0 + ↑⌈g 0⌉
-- Mathlib.FieldTheory.RatFunc.Luroth
RatFunc.Luroth.generator_ne_zero : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)}, E ≠ ⊥ → RatFunc.Luroth.generator E ≠ 0
-- Init.Data.SInt.Lemmas
Int8.toInt16_ne_neg_one : ∀ (a : Int8), a ≠ -1 → a.toInt16 ≠ -1
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.hom_ext₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {F G : CategoryTheory.ComposableArrows C 1}
  {φ φ' : F ⟶ G},
  CategoryTheory.ComposableArrows.app' φ 0 CategoryTheory.ComposableArrows.homMk₁._proof_4 =
      CategoryTheory.ComposableArrows.app' φ' 0 CategoryTheory.ComposableArrows.homMk₁._proof_4 →
    CategoryTheory.ComposableArrows.app' φ 1 CategoryTheory.ComposableArrows.homMk₁._proof_5 =
        CategoryTheory.ComposableArrows.app' φ' 1 CategoryTheory.ComposableArrows.homMk₁._proof_5 →
      φ = φ'
-- Lean.Util.Trace
Lean.trace.profiler.output : Lean.Option String
-- Mathlib.RingTheory.Valuation.Basic
AddValuation.ext_iff : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀]
  {v₁ v₂ : AddValuation R Γ₀}, v₁ = v₂ ↔ ∀ (r : R), v₁ r = v₂ r
-- Mathlib.Topology.Semicontinuity.Defs
Semicontinuous.semicontinuousWithinAt : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {r : α → β → Prop},
  Semicontinuous r → ∀ (s : Set α) (x : α), SemicontinuousWithinAt r s x
-- Qq.ForLean.ReduceEval
Lean.Meta.instReduceEvalMVarId_qq : Lean.Meta.ReduceEval Lean.MVarId
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.hom_ext : ∀ {R : Type u_1} [inst : NonAssocRing R] {d : ℤ} (f g : ℤ√d →+* R), f Zsqrtd.sqrtd = g Zsqrtd.sqrtd → f = g
-- Mathlib.CategoryTheory.Shift.Opposite
/-- Given a `CommShift` structure on `OppositeShift.functor F` (for the naive shifts on the opposite
categories), this is the corresponding `CommShift` structure on `F`.
 -/
CategoryTheory.Functor.commShiftUnop : {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] →
        (A : Type u_3) →
          [inst_2 : AddMonoid A] →
            [inst_3 : CategoryTheory.HasShift C A] →
              [inst_4 : CategoryTheory.HasShift D A] →
                (F : CategoryTheory.Functor C D) →
                  [(CategoryTheory.OppositeShift.functor A F).CommShift A] → F.CommShift A
-- Init.Data.SInt.Bitwise
Int64.not_zero : ~~~0 = -1