mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.Haar.Unique
MeasureTheory.Measure.mul_addHaarScalarFactor_smul : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [LocallyCompactSpace G] (μ' μ : MeasureTheory.Measure G)
  [inst_6 : μ.IsAddHaarMeasure] [inst_7 : MeasureTheory.IsFiniteMeasureOnCompacts μ'] [inst_8 : μ'.IsAddLeftInvariant]
  {c : NNReal} (hc : c ≠ 0), c * μ'.addHaarScalarFactor (c • μ) = μ'.addHaarScalarFactor μ
-- Init.Data.Int.Order
Int.instCommutativeMax : Std.Commutative max
-- Mathlib.Topology.Connected.Basic
IsPreconnected.mapsTo_Ioi_or_Iio : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] {s : Set α} [inst_1 : LinearOrder β]
  [inst_2 : TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {b : β},
  IsPreconnected s → ContinuousOn f s → (∀ x ∈ s, f x ≠ b) → Set.MapsTo f s (Set.Ioi b) ∨ Set.MapsTo f s (Set.Iio b)
-- Batteries.Util.ProofWanted
_private.Batteries.Util.ProofWanted.0.theoremWantedCmd : WantedCmdKind✝
-- Init.Data.Array.Lemmas
Array.toArray_eq : ∀ {α : Type u_1} {as : List α} {xs : Array α}, as.toArray = xs ↔ as = xs.toList
-- Mathlib.Order.WellFounded
/-- Let `r` be a well-founded relation on `α`, let `f : α → β` be a function,
let `C : β → Prop`, and let `bot : α`.
This induction principle shows that `C (f bot)` holds, given that
* some `a` satisfies `C (f a)`, and
* for each `b` such that `f b ≠ f bot` and `C (f b)` holds, there is `c`
  satisfying `r c b` and `C (f c)`.  -/
WellFounded.induction_bot' : ∀ {α : Sort u_4} {β : Sort u_5} {r : α → α → Prop},
  WellFounded r →
    ∀ {a bot : α} {C : β → Prop} {f : α → β},
      (∀ (b : α), f b ≠ f bot → C (f b) → ∃ c, r c b ∧ C (f c)) → C (f a) → C (f bot)
-- Mathlib.FieldTheory.IsSepClosed
/-- A separably closed field is its separable closure.  -/
IsSepClosure.self_of_isSepClosed : ∀ (k : Type u) [inst : Field k] [IsSepClosed k], IsSepClosure k k
-- Mathlib.Topology.Order.LeftRightNhds
/-- A set is a neighborhood of `a` within `(-∞, a]` if and only if it contains an interval `[l, a]`
with `l < a`.  -/
mem_nhdsLE_iff_exists_Icc_subset : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [NoMinOrder α]
  [DenselyOrdered α] {a : α} {s : Set α}, s ∈ nhdsWithin a (Set.Iic a) ↔ ∃ l < a, Set.Icc l a ⊆ s
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.BimonObj.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {M : C} →
          [toMonObj : CategoryTheory.MonObj M] →
            [toComonObj : CategoryTheory.ComonObj M] →
              autoParam
                  (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul CategoryTheory.ComonObj.comul =
                    CategoryTheory.CategoryStruct.comp
                      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.ComonObj.comul
                        CategoryTheory.ComonObj.comul)
                      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M M M M)
                        (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul
                          CategoryTheory.MonObj.mul)))
                  CategoryTheory.BimonObj.mul_comul._autoParam →
                autoParam
                    (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one CategoryTheory.ComonObj.comul =
                      CategoryTheory.MonObj.one)
                    CategoryTheory.BimonObj.one_comul._autoParam →
                  autoParam
                      (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul CategoryTheory.ComonObj.counit =
                        CategoryTheory.ComonObj.counit)
                      CategoryTheory.BimonObj.mul_counit._autoParam →
                    autoParam
                        (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one CategoryTheory.ComonObj.counit =
                          CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
                        CategoryTheory.BimonObj.one_counit._autoParam →
                      CategoryTheory.BimonObj M
-- Mathlib.Data.List.MinMax
List.le_maximum_of_length_pos_of_mem : ∀ {α : Type u_1} [inst : LinearOrder α] {l : List α} {a : α},
  a ∈ l → ∀ (w : 0 < l.length), a ≤ List.maximum_of_length_pos w
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.argEquiv_apply_coe : ∀ (z : Circle), ↑(Circle.argEquiv z) = (↑z).arg
-- Init.Data.Order.Factories
/-- Creates a `Max α` instance from `LE α` and `DecidableLE α` so that `max a b` is either `a` or `b`,
preferring `a` over `b` when in doubt.

Has a `LawfulOrderLeftLeaningMax α` instance.
 -/
Max.leftLeaningOfLE : (α : Type u) → [inst : LE α] → [DecidableLE α] → Max α
-- Mathlib.RingTheory.LaurentSeries
/-- The valuation of a Laurent series is the order of the first non-zero coefficient.  -/
LaurentSeries.valuation_le_iff_coeff_lt_eq_zero : ∀ (K : Type u_2) [inst : Field K] {D : ℤ} {f : LaurentSeries K}, Valued.v f ≤ WithZero.exp (-D) ↔ ∀ n < D, f.coeff n = 0
-- Mathlib.MeasureTheory.Constructions.UnitInterval
unitInterval.volume_uIoc : ∀ (x y : ↑unitInterval), MeasureTheory.volume (Set.uIoc x y) = edist y x
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.mapDomain_zero : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] (f : M → N), MonoidAlgebra.mapDomain f 0 = 0
-- Init.Data.UInt.Lemmas
UInt16.toFin_ofBitVec : ∀ {b : BitVec 16}, { toBitVec := b }.toFin = b.toFin
-- Lean.Meta.Tactic.Grind.Types
/-- Exists-propagator.  -/
Lean.Meta.Grind.SplitSource.existsProp : Lean.Expr → Lean.Meta.Grind.SplitSource
-- Mathlib.SetTheory.Cardinal.Finite
Nat.card_eq_finsetCard : ∀ {α : Type u_1} (s : Finset α), Nat.card ↥s = s.card
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.leadingCoeff_eq_sum : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {v : ι → F},
  Set.InjOn v ↑s →
    ∀ {P : Polynomial F},
      ↑s.card = P.degree + 1 → P.leadingCoeff = ∑ i ∈ s, Polynomial.eval (v i) P / ∏ j ∈ s.erase i, (v i - v j)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- If the oriented angle between two vectors is `-π / 2`, the inner product of those vectors
is zero.  -/
Orientation.inner_eq_zero_of_oangle_eq_neg_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑(-Real.pi / 2) → inner ℝ x y = 0
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.trailingDegree_eq_top : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.trailingDegree = ⊤ ↔ p = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
CategoryTheory.Square.IsPushout.iff_of_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {sq₁ sq₂ : CategoryTheory.Square C} (e : sq₁ ≅ sq₂),
  sq₁.IsPushout ↔ sq₂.IsPushout
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.AffineScheme.instIsEquivalenceOppositeCommRingCatRightOpΓ : AlgebraicGeometry.AffineScheme.Γ.rightOp.IsEquivalence
-- Lean.Parser.Do
Lean.Parser.Term.doCatch.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Analysis.Analytic.IteratedFDeriv
/-- If the `n`-th term in a power series is zero, then the `n`-th derivative of the corresponding
function vanishes.  -/
HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_zero : ∀ {𝕜 : 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}
  {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal},
  HasFPowerSeriesWithinOnBall f p s x r →
    AnalyticOn 𝕜 f s → UniqueDiffOn 𝕜 s → x ∈ s → ∀ {n : ℕ}, p n = 0 → iteratedFDerivWithin 𝕜 n f s x = 0
-- Lean.Elab.Do.Control
Lean.Elab.Do.ControlStack.base : Lean.Elab.Do.MonadInfo → Lean.Elab.Do.ControlStack
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.maxEntry!_eq_get!_maxEntry? : ∀ {α : Type u} {β : α → Type v} [inst : Inhabited ((a : α) × β a)] {l : Std.DTreeMap.Internal.Impl α β},
  l.maxEntry! = l.maxEntry?.get!
-- Mathlib.Topology.Algebra.GroupWithZero
continuousAt_zpow₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : TopologicalSpace G₀] [ContinuousInv₀ G₀] [ContinuousMul G₀]
  (x : G₀) (m : ℤ), x ≠ 0 ∨ 0 ≤ m → ContinuousAt (fun x => x ^ m) x
-- Mathlib.Data.Countable.Basic
countable_iff_nonempty_embedding : ∀ {α : Sort u}, Countable α ↔ Nonempty (α ↪ ℕ)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- If a finset `u` is contained in the product of two sets `s * t`, we can find two finsets `s'`,
`t'` such that `s' ⊆ s`, `t' ⊆ t` and `u ⊆ s' * t'`.  -/
Finset.subset_mul : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α] {u : Finset α} {s t : Set α},
  ↑u ⊆ s * t → ∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' * t'
-- Mathlib.CategoryTheory.Limits.Preserves.Presheaf
CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.iso_hom : ∀ {C : Type u} [inst : CategoryTheory.SmallCategory C] [inst_1 : CategoryTheory.Limits.HasFiniteColimits C]
  (A : CategoryTheory.Functor Cᵒᵖ (Type u)) {J : Type} [inst_2 : CategoryTheory.SmallCategory J]
  [inst_3 : CategoryTheory.FinCategory J] (K : CategoryTheory.Functor J Cᵒᵖ)
  [inst_4 : CategoryTheory.IsFiltered (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)],
  (CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.iso A K).hom =
    CategoryTheory.Limits.limit.post K A
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
CategoryTheory.ObjectProperty.hom_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory}
  (f : X ⟶ Y) [inst_1 : CategoryTheory.IsIso f], (CategoryTheory.inv f).hom = CategoryTheory.inv f.hom
-- Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
/-- If `f ≫ g` is a strong monomorphism, then so is `f`.  -/
CategoryTheory.strongMono_of_strongMono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {R Q P : C} (f : P ⟶ Q) (g : Q ⟶ R)
  [CategoryTheory.StrongMono (CategoryTheory.CategoryStruct.comp f g)], CategoryTheory.StrongMono f
-- Mathlib.Algebra.GCDMonoid.Basic
/-- Maps an element of `Associates` back to the normalized element of its associate class  -/
Associates.out : {α : Type u_1} → [inst : MonoidWithZero α] → [NormalizationMonoid α] → Associates α → α
-- Mathlib.Condensed.Discrete.Basic
/-- The discrete light condensed object associated to an object of `C` is the constant sheaf at that
object.
 -/
LightCondensed.discrete : (C : Type w) →
  [inst : CategoryTheory.Category.{u, w} C] →
    [CategoryTheory.HasSheafify (CategoryTheory.coherentTopology LightProfinite) C] →
      CategoryTheory.Functor C (LightCondensed C)
-- Mathlib.Topology.Convenient.Category
/-- The functor `GeneratedByTopCat X ⥤ ContinuousGeneratedByCat X` which is
part of the equivalence `ContinuousGeneratedByCat.equivalence`. It sends
an `X`-generated topological space `Y` to the topological space `Y`, considered as
an object of `ContinuousGeneratedByCat X`.  -/
ContinuousGeneratedByCat.fromGeneratedByTopCat : {ι : Type t} →
  {X : ι → Type u} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      CategoryTheory.Functor (GeneratedByTopCat X) (ContinuousGeneratedByCat X)
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.instInhabitedAnswer.default : Lean.Meta.SynthInstance.Answer
-- Mathlib.RingTheory.Ideal.IsPrimary
Ideal.IsPrime.isPrimary : ∀ {R : Type u_1} [inst : CommSemiring R] {I : Ideal R}, I.IsPrime → I.IsPrimary
-- Mathlib.GroupTheory.Abelianization.Defs
Abelianization.commGroup : (G : Type u) → [inst : Group G] → CommGroup (Abelianization G)
-- Std.Tactic.BVDecide.Reflect
Std.Tactic.BVDecide.Reflect.BitVec.cpop_congr : ∀ (w : ℕ) (x x' : BitVec w), x = x' → x'.cpop = x.cpop
-- Mathlib.Order.TypeTags
WithBot.some.eq_1 : ∀ {α : Type u_1}, WithBot.some = some
-- Lean.Parser.Extra
Lean.Parser.decQuotDepth.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.foldrM_eq_foldrM_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : α → δ → m δ} {init : δ},
  Std.TreeMap.foldrM (fun a x d => f a d) init t = List.foldrM f init t.keys
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.addBottom_nth_succ_fst : ∀ {K : Type u_1} {Γ : K → Type u_2} (L : Turing.ListBlank ((k : K) → Option (Γ k))) (n : ℕ),
  ((Turing.TM2to1.addBottom L).nth (n + 1)).1 = false
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
/-- Structure recording good behavior of a property of a triple `(f, s, x)` where `f` is a function,
`s` a set and `x` a point. Good behavior here means locality and invariance under given groupoids
(both in the source and in the target). Given such a good behavior, the lift of this property
to charted spaces admitting these groupoids will inherit the good behavior.  -/
StructureGroupoid.LocalInvariantProp : {H : Type u_1} →
  {H' : Type u_3} →
    [inst : TopologicalSpace H] →
      [inst_1 : TopologicalSpace H'] → StructureGroupoid H → StructureGroupoid H' → ((H → H') → Set H → H → Prop) → Prop
-- Mathlib.LinearAlgebra.AffineSpace.Basis
AffineBasis.mk.injEq : ∀ {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : Ring k] [inst_3 : Module k V] (toFun : ι → P) (ind' : AffineIndependent k toFun)
  (tot' : affineSpan k (Set.range toFun) = ⊤) (toFun_1 : ι → P) (ind'_1 : AffineIndependent k toFun_1)
  (tot'_1 : affineSpan k (Set.range toFun_1) = ⊤),
  ({ toFun := toFun, ind' := ind', tot' := tot' } = { toFun := toFun_1, ind' := ind'_1, tot' := tot'_1 }) =
    (toFun = toFun_1)
-- Batteries.Recycling.RBTree.Basic
/-- `O(n)`. Fold a monadic function on the values from left to right (in increasing order).  -/
RBTree.RBSet.foldlM : {m : Type u_1 → Type u_2} →
  {σ : Type u_1} → {α : Type u_3} → {cmp : α → α → Ordering} → [Monad m] → (σ → α → m σ) → σ → RBTree.RBSet α cmp → m σ
-- Mathlib.Order.Hom.WithTopBot
OrderHom.withTopMap.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α →o β),
  f.withTopMap = { toFun := WithTop.map ⇑f, monotone' := ⋯ }
-- Mathlib.RingTheory.Valuation.Basic
/-- A `≤`-preserving group homomorphism `Γ₀ → Γ'₀` induces a map `Valuation R Γ₀ → Valuation R Γ'₀`.
 -/
Valuation.map : {R : Type u_3} →
  {Γ₀ : Type u_4} →
    {Γ'₀ : Type u_5} →
      [inst : Ring R] →
        [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] →
          [inst_2 : LinearOrderedCommMonoidWithZero Γ'₀] →
            (f : Γ₀ →*₀ Γ'₀) → Monotone ⇑f → Valuation R Γ₀ → Valuation R Γ'₀
-- Mathlib.Data.List.Zip
List.zipWith_congr : ∀ {α : Type u} {β : Type u_1} {γ : Type u_2} (f g : α → β → γ) (la : List α) (lb : List β),
  List.Forall₂ (fun a b => f a b = g a b) la lb → List.zipWith f la lb = List.zipWith g la lb
-- Mathlib.Algebra.Module.Submodule.Pointwise
Submodule.stabilizer_coe : ∀ {R : Type u_4} {G : Type u_5} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Group G] [inst_4 : DistribMulAction G M] [inst_5 : SMulCommClass G R M] {S : Submodule R M},
  MulAction.stabilizer G S = MulAction.stabilizer G ↑S
-- Mathlib.GroupTheory.Congruence.Defs
/-- Definition of the function on the quotient by an additive
congruence relation `c` induced by a function that is constant on `c`'s equivalence classes.  -/
AddCon.liftOn_coe : ∀ {M : Type u_1} [inst : Add M] {β : Sort u_4} (c : AddCon M) (f : M → β) (h : ∀ (a b : M), c a b → f a = f b) (x : M),
  AddCon.liftOn (↑x) f h = f x
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.sum_apply_eq_zero : ∀ {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} [Countable ι] {μ : ι → MeasureTheory.Measure α} {s : Set α},
  (MeasureTheory.Measure.sum μ) s = 0 ↔ ∀ (i : ι), (μ i) s = 0
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMapClass.map_sub_ofNat' : ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {b : H} [inst_1 : AddGroupWithOne G]
  [inst_2 : AddGroup H] [AddConstMapClass F G H 1 b] (f : F) (x : G) (n : ℕ) [inst_4 : n.AtLeastTwo],
  f (x - OfNat.ofNat n) = f x - OfNat.ofNat n • b
-- Init.Data.String.Pattern.Pred
String.Slice.Pattern.CharPred.instToBackwardSearcherForallCharBoolDefaultBackwardSearcher : {p : Char → Bool} →
  String.Slice.Pattern.ToBackwardSearcher p (String.Slice.Pattern.ToBackwardSearcher.DefaultBackwardSearcher p)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- `biproduct.bicone F` is a colimit cocone.  -/
CategoryTheory.Limits.biproduct.isColimit : {J : Type w} →
  {C : Type uC} →
    [inst : CategoryTheory.Category.{uC', uC} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        (F : J → C) →
          [inst_2 : CategoryTheory.Limits.HasBiproduct F] →
            CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.biproduct.bicone F).toCocone
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.ext : ∀ {𝕜 : 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} {x y : ModelWithCorners 𝕜 E H},
  ↑x.toPartialEquiv = ↑y.toPartialEquiv → x.invFun = y.invFun → x.source = y.source → x.target = y.target → x = y
-- Mathlib.Algebra.Homology.Homotopy
CategoryTheory.Functor.mapHomotopyEquiv_inv : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} {W : Type u_2} [inst_2 : CategoryTheory.Category.{v_1, u_2} W]
  [inst_3 : CategoryTheory.Preadditive W] (F : CategoryTheory.Functor V W) [inst_4 : F.Additive]
  (h : HomotopyEquiv C D), (F.mapHomotopyEquiv h).inv = (F.mapHomologicalComplex c).map h.inv
-- Mathlib.Algebra.Opposites
MulOpposite.unop_sub : ∀ {α : Type u_1} [inst : Sub α] (x y : αᵐᵒᵖ), MulOpposite.unop (x - y) = MulOpposite.unop x - MulOpposite.unop y
-- Mathlib.Algebra.Module.ZLattice.Covolume
ZLattice.covolume_pos : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [inst_5 : DiscreteTopology ↥L] [IsZLattice ℝ L]
  (μ : autoParam (MeasureTheory.Measure E) _auto_25✝) [μ.IsAddHaarMeasure], 0 < ZLattice.covolume L μ
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.instIsMulRightInvariantCount : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul G],
  MeasureTheory.Measure.count.IsMulRightInvariant
-- Mathlib.RingTheory.AdicCompletion.Functoriality
AdicCompletion.piEquivFin_apply : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (n : ℕ) (x : AdicCompletion I (Fin n → R)),
  (AdicCompletion.piEquivFin I n) x = (AdicCompletion.pi I fun x => R) x
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.CorepresentableBy.homEquiv_eq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C (Type v)} {X : C}
  (e : F.CorepresentableBy X) {Y : C} (f : X ⟶ Y),
  e.homEquiv f = (CategoryTheory.ConcreteCategory.hom (F.map f)) (e.homEquiv (CategoryTheory.CategoryStruct.id X))
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.Weight.isNonZero_iff_ne_zero : ∀ {R : Type u_2} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [inst_8 : Nontrivial ↥(LieModule.genWeightSpace M 0)] {χ : LieModule.Weight R L M},
  χ.IsNonZero ↔ χ ≠ 0
-- Std.Data.HashMap.Raw
/-- Well-formedness predicate for hash maps. Users of `HashMap` will not need to interact with this.
Users of `HashMap.Raw` will need to provide proofs of `WF` to lemmas and should use lemmas
`WF.empty` and `WF.insert` (which are always named exactly like the operations they are about) to
show that map operations preserve well-formedness.
 -/
Std.HashMap.Raw.WF : {α : Type u} → {β : Type v} → [BEq α] → [Hashable α] → Std.HashMap.Raw α β → Prop
-- Mathlib.Analysis.Fourier.AddCircle
/-- The monomials `fourier n` are an orthonormal set with respect to normalised Haar measure.  -/
orthonormal_fourier : ∀ {T : ℝ} [hT : Fact (0 < T)], Orthonormal ℂ (fourierLp 2)
-- Mathlib.CategoryTheory.Category.ULift
CategoryTheory.AsSmall.equiv_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  CategoryTheory.AsSmall.equiv.functor = CategoryTheory.AsSmall.up
-- Mathlib.Computability.NFA
/-- `M.accepts` is the language of `x` such that there is an accept state in `M.eval x`.  -/
NFA.accepts : {α : Type u} → {σ : Type v} → NFA α σ → Language α
-- Mathlib.Topology.Metrizable.Basic
TopologicalSpace.MetrizableSpace.toT0Space : ∀ {X : Type u_5} {t : TopologicalSpace X} [self : TopologicalSpace.MetrizableSpace X], T0Space X
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
_private.Lean.Meta.Tactic.Grind.Arith.Cutsat.Util.0.Int.Internal.Linear.Poly.updateOccs.go : Int.Internal.Linear.Var → Int.Internal.Linear.Poly → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Data.ENNReal.Operations
ENNReal.iSup_add_iSup : ∀ {ι : Sort u_1} {f g : ι → ENNReal}, (∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k) → iSup f + iSup g = ⨆ i, f i + g i
-- Mathlib.GroupTheory.GroupExtension.Basic
AddGroupExtension.Section.add_neg_add_add_mem_range_inl : ∀ {N : Type u_1} {G : Type u_2} [inst : AddGroup N] [inst_1 : AddGroup G] {E : Type u_3} [inst_2 : AddGroup E]
  {S : AddGroupExtension N E G} (σ : S.Section) (g₁ g₂ : G), -σ (g₁ + g₂) + σ g₁ + σ g₂ ∈ S.inl.range
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Real.deriv_qaryEntropy : ∀ {q : ℕ} {p : ℝ}, p ≠ 0 → p ≠ 1 → deriv (Real.qaryEntropy q) p = Real.log (↑q - 1) + Real.log (1 - p) - Real.log p
-- Mathlib.LinearAlgebra.RootSystem.WeylGroup
RootPairing.range_weylGroup_weightHom : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N),
  ((RootPairing.Equiv.weightHom P).domRestrict P.weylGroup).range = Subgroup.closure (Set.range P.reflection)
-- Lean.Server.Completion.CompletionItemCompression
_private.Lean.Server.Completion.CompletionItemCompression.0.Lean.Lsp.ResolvableCompletionList.compressCompletionTagsFast : String → Array Lean.Lsp.CompletionItemTag → ℕ → String
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.sumAddHom_add : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddZeroClass (β i)]
  [inst_2 : AddCommMonoid γ] (g h : (i : ι) → β i →+ γ),
  (DFinsupp.sumAddHom fun i => g i + h i) = DFinsupp.sumAddHom g + DFinsupp.sumAddHom h
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.toLinearMap_apply_PolarizationIn : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (S : Type u_5)
  [inst_5 : CommRing S] [inst_6 : Algebra S R] [inst_7 : FaithfulSMul S R] [inst_8 : Module S M]
  [inst_9 : IsScalarTower S R M] [inst_10 : Module S N] [IsScalarTower S R N] [inst_12 : P.IsValuedIn S]
  [inst_13 : Fintype ι] (x y : ↥(P.rootSpan S)),
  (P.toLinearMap ↑y) ((P.PolarizationIn S) x) = (algebraMap S R) (((P.RootFormIn S) x) y)
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.lintegral_withDensity_le_lintegral_mul : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) {f : α → ENNReal},
  Measurable f → ∀ (g : α → ENNReal), ∫⁻ (a : α), g a ∂μ.withDensity f ≤ ∫⁻ (a : α), (f * g) a ∂μ
-- Mathlib.Logic.Godel.GodelBetaFunction
Nat.beta.eq_1 : ∀ (n i : ℕ), n.beta i = (Nat.unpair n).1 % ((i + 1) * (Nat.unpair n).2 + 1)