mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Flat.Stability
/-- If `S` is a flat `R`-algebra, then any flat `S`-Module is also `R`-flat.  -/
Module.Flat.trans : ∀ (R : Type u) (S : Type v) (M : Type w) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module S M] [IsScalarTower R S M] [Module.Flat R S]
  [Module.Flat S M], Module.Flat R M
-- Mathlib.Topology.OmegaCompletePartialOrder
/-- `x` is an `ω`-Sup of a chain `c` if it is the least upper bound of the range of `c`.  -/
Scott.IsωSup : {α : Type u} → [inst : Preorder α] → OmegaCompletePartialOrder.Chain α → α → Prop
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.monotone_rpow_of_base_ge_one : ∀ {b : ℝ}, 1 ≤ b → Monotone fun x => b ^ x
-- Mathlib.Combinatorics.Digraph.Orientation
Digraph.toSimpleGraphStrict_bot : ∀ {V : Type u_1}, ⊥.toSimpleGraphStrict = ⊥
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBase.subset_ground : ∀ {α : Type u_1} {M : Matroid α} {B : Set α}, M.IsBase B → B ⊆ M.E
-- Mathlib.Data.PFunctor.Multivariate.M
MvPFunctor.mvfunctorM : {n : ℕ} → (P : MvPFunctor.{u} (n + 1)) → MvFunctor P.M
-- Init.Data.UInt.Basic
/-- Negation of word-sized unsigned integers, computed modulo `USize.size`.

This function is overridden at runtime with an efficient implementation.
 -/
USize.neg : USize → USize
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.ofArray : {n : ℕ} →
  Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) →
    Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)
-- Mathlib.Topology.Semicontinuity.Defs
lowerSemicontinuousWithinAt_const : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder β] {x : α} {s : Set α} {z : β},
  LowerSemicontinuousWithinAt (fun _x => z) s x
-- Mathlib.LinearAlgebra.InvariantBasisNumber
le_of_fin_surjective : ∀ (R : Type u) [inst : Semiring R] [RankCondition R] {n m : ℕ} (f : (Fin n → R) →ₗ[R] Fin m → R),
  Function.Surjective ⇑f → m ≤ n
-- Mathlib.CategoryTheory.ObjectProperty.Opposite
CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsUnopOfOpposite : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty Cᵒᵖ)
  [P.IsClosedUnderIsomorphisms], P.unop.IsClosedUnderIsomorphisms
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.addSubmonoidComap_surjective_of_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (f : M →+ N) (N' : AddSubmonoid N),
  Function.Surjective ⇑f → Function.Surjective ⇑(f.addSubmonoidComap N')
-- Mathlib.Util.Notation3
/-- The binders accumulated while matching a `scoped` expression.  -/
Mathlib.Notation3.MatchState.scopeState : Mathlib.Notation3.MatchState → Option (Array (Lean.TSyntax `Batteries.ExtendedBinder.extBinderParenthesized))
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.CoPolarization_apply : ∀ {ι : 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) [inst_5 : Fintype ι]
  (x : N), P.CoPolarization x = ∑ i, (P.root' i) x • P.root i
-- Mathlib.Order.BoundedOrder.Basic
Prod.instOrderBot : (α : Type u) → (β : Type v) → [inst : LE α] → [inst_1 : LE β] → [OrderBot α] → [OrderBot β] → OrderBot (α × β)
-- Lean.Meta.Tactic.Grind.EqResolution
_private.Lean.Meta.Tactic.Grind.EqResolution.0.Lean.Meta.Grind.topsortMVars?.go : Array Lean.Expr → Lean.Meta.Grind.TopSortM Unit
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.ofList_singleton : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {k : α}
  {v : β k}, Std.ExtDHashMap.ofList [⟨k, v⟩] = ∅.insert k v
-- Mathlib.Data.Finsupp.NeLocus
Finsupp.neLocus.eq_1 : ∀ {α : Type u_1} {N : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq N] [inst_2 : Zero N] (f g : α →₀ N),
  f.neLocus g = {x ∈ f.support ∪ g.support | f x ≠ g x}
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.Mk₁.obj.eq_1 : ∀ {C : Type u_1} (X₀ X₁ : C) (isLt : 0 < 2), CategoryTheory.ComposableArrows.Mk₁.obj X₀ X₁ ⟨0, isLt⟩ = X₀
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.AddGrp.instIsAddMonHom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {G H : CategoryTheory.AddGrp C}
  [inst_3 : CategoryTheory.IsCommAddMonObj H.X] [inst_4 : CategoryTheory.IsCommAddMonObj G.X] (f : G ⟶ H),
  CategoryTheory.IsAddMonHom f
-- Mathlib.Tactic.Ring.Basic
/-- The comparisons on the basetype used to compare normalized ring expressions.  -/
Mathlib.Tactic.Ring.ringCompare : {u : Lean.Level} → {α : Q(Type u)} → Mathlib.Tactic.Ring.Common.RingCompare Mathlib.Tactic.Ring.RatCoeff
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.coe_zero : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} [inst : Zero M], ↑0 = 0
-- Mathlib.SetTheory.Ordinal.Notation
ONote.mul.eq_1 : ∀ (x : ONote), ONote.zero.mul x = 0
-- Mathlib.Logic.Encodable.Basic
Encodable.Subtype.encode_eq : ∀ {α : Type u_1} {P : α → Prop} [encA : Encodable α] [decP : DecidablePred P] (a : Subtype P),
  Encodable.encode a = Encodable.encode ↑a
-- Mathlib.Order.Filter.Pointwise
Filter.map_sub : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : SubtractionMonoid β]
  [inst_2 : FunLike F α β] [AddMonoidHomClass F α β] (m : F) {f g : Filter α},
  Filter.map (⇑m) (f - g) = Filter.map (⇑m) f - Filter.map (⇑m) g
-- Mathlib.Order.Atoms
IsCoatomistic.mk : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderTop α],
  (∀ (b : α), ∃ s, IsGLB s b ∧ ∀ a ∈ s, IsCoatom a) → IsCoatomistic α
-- Mathlib.Order.CompleteSublattice
/-- The natural complete lattice hom from a complete sublattice to the original lattice.  -/
CompleteSublattice.subtype : {α : Type u_1} → [inst : CompleteLattice α] → (L : CompleteSublattice α) → CompleteLatticeHom (↥L) α
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instAddRightCancelMonoid : {α : Type u_1} → [AddRightCancelMonoid α] → AddRightCancelMonoid (Lex α)
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.id.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (a : C),
  (CategoryTheory.WithTerminal.of a).id = CategoryTheory.CategoryStruct.id a
-- Lean.Declaration
Lean.ConstantInfo.thmInfo.sizeOf_spec : ∀ (val : Lean.TheoremVal), sizeOf (Lean.ConstantInfo.thmInfo val) = 1 + sizeOf val
-- Mathlib.Algebra.Order.Star.Basic
/-- When `R` is a non-unital ring, to construct a `StarOrderedRing` instance it suffices to
show that the nonnegative elements are precisely those elements of the form `star s * s`
for `s : R`.

This is provided for convenience because it holds in many common scenarios (e.g.,`ℝ`, `ℂ`, or
any C⋆-algebra), and obviates the hassle of `AddSubmonoid.closure_induction` when creating those
instances.  -/
StarOrderedRing.of_nonneg_iff' : ∀ {R : Type u_1} [inst : NonUnitalRing R] [inst_1 : PartialOrder R] [inst_2 : StarRing R],
  (∀ {x y : R}, x ≤ y → ∀ (z : R), z + x ≤ z + y) → (∀ (x : R), 0 ≤ x ↔ ∃ s, x = star s * s) → StarOrderedRing R
-- Mathlib.Data.Matrix.Composition
Matrix.comp_symm_apply : ∀ (I : Type u_1) (J : Type u_2) (K : Type u_3) (L : Type u_4) (R : Type u_5) (n : Matrix (I × K) (J × L) R) (i : I)
  (j : J) (k : K) (l : L), (Matrix.comp I J K L R).symm n i j k l = n (i, k) (j, l)
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_actionHomRight : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction Cᵒᵖ Dᵒᵖ] (c : C) {d d' : D} (f : d ⟶ d'),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c f =
    (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight (Opposite.op c) f.op).unop
-- Init.Data.Vector.Lex
Vector.instTransLt : {α : Type u_1} →
  {n : ℕ} →
    [inst : LT α] →
      [Trans (fun x1 x2 => x1 < x2) (fun x1 x2 => x1 < x2) fun x1 x2 => x1 < x2] →
        Trans (fun x1 x2 => x1 < x2) (fun x1 x2 => x1 < x2) fun x1 x2 => x1 < x2
-- Mathlib.Data.Sum.Interval
Sum.Ioo_inl_inr : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] (a₁ : α) (b₂ : β), Finset.Ioo (Sum.inl a₁) (Sum.inr b₂) = ∅
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
/-- The centered arcs `centeredArc (π / 2 ^ (n + 1))` form a neighborhood basis at `1`.
This basis is useful because multiplying two sufficiently small arcs stays inside an earlier arc.  -/
Circle.hasBasis_centeredArc_div_two_pow : (nhds 1).HasBasis (fun x => True) fun n => Circle.centeredArc (Real.pi / 2 ^ (n + 1))
-- Mathlib.Analysis.Normed.Field.Krasner
/-- Krasner's lemma assuming `Normal K L`.  -/
IsKrasner.of_completeSpace_of_normal : ∀ (K : Type u_1) (L : Type u_2) [inst : NormedField L] [inst_1 : NontriviallyNormedField K] [CompleteSpace K]
  [IsUltrametricDist K] [inst_4 : NormedAlgebra K L] [Normal K L], IsKrasner K L
-- Init.Data.Array.Attach
/-- If we fold over `l.attach` with a function that ignores the membership predicate,
we get the same results as folding over `l` directly.

This is useful when we need to use `attach` to show termination.

Unfortunately this can't be applied by `simp` because of the higher order unification problem,
and even when rewriting we need to specify the function explicitly.
See however `foldr_subtype` below.
 -/
Array.foldr_attach : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → β → β} {b : β},
  Array.foldr (fun t acc => f (↑t) acc) b xs.attach = Array.foldr f b xs
-- Mathlib.Probability.ProbabilityMassFunction.Basic
/-- Construct an `OuterMeasure` from a `PMF`, by assigning measure to each set `s : Set α` equal
to the sum of `p x` for each `x ∈ α`.  -/
PMF.toOuterMeasure : {α : Type u_1} → PMF α → MeasureTheory.OuterMeasure α
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.mapL_add_left : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [inst : RCLike 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F]
  [inst_4 : InnerProductSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G]
  [inst_7 : NormedAddCommGroup H] [inst_8 : InnerProductSpace 𝕜 H] (f₁ f₂ : E →L[𝕜] F) (g : G →L[𝕜] H),
  TensorProduct.mapL (f₁ + f₂) g = TensorProduct.mapL f₁ g + TensorProduct.mapL f₂ g
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.hasArrayLitPattern : Lean.Meta.Match.Problem → Bool
-- Batteries.Data.List.Lemmas
List.le_getElem_idxsOf : ∀ {α : Type u_1} {i : ℕ} {xs : List α} {x : α} {s : ℕ} [inst : BEq α] (h : i < (List.idxsOf x xs s).length),
  s ≤ (List.idxsOf x xs s)[i]
-- Mathlib.CategoryTheory.Adjunction.Triple
/-- For an adjoint triple `F ⊣ G ⊣ H` where `G` is fully faithful and `H` preserves epimorphisms
(which is for example the case if `H` has a further right adjoint), the components of the natural
transformation `H ⟶ F` are epic iff the respective components of the natural transformation
`H ⋙ G ⟶ F ⋙ G` obtained from the units and counits of the adjunctions are.  -/
CategoryTheory.Adjunction.Triple.epi_rightToLeft_app_iff : ∀ {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 : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  {H : CategoryTheory.Functor C D} (t : CategoryTheory.Adjunction.Triple F G H) [inst_2 : G.Full] [inst_3 : G.Faithful]
  [H.PreservesEpimorphisms] {X : C},
  CategoryTheory.Epi (t.rightToLeft.app X) ↔
    CategoryTheory.Epi (CategoryTheory.CategoryStruct.comp (t.adj₂.counit.app X) (t.adj₁.unit.app X))
-- Std.Time.Zoned.Database.TzIf
/-- Represents a TZif file, which can be either version 1 or version 2.
 -/
Std.Time.TimeZone.TZif.TZif : Type
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.discreteTopology_iff : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y),
  DiscreteTopology X ↔ DiscreteTopology Y
-- Mathlib.LinearAlgebra.AffineSpace.Slope
/-- `slope f a b` is an affine combination of `slope f a (lineMap a b r)` and
`slope f (lineMap a b r) b`. We use `lineMap` to express this property.  -/
lineMap_slope_lineMap_slope_lineMap : ∀ {k : Type u_1} {E : Type u_2} {PE : Type u_3} [inst : Field k] [inst_1 : AddCommGroup E] [inst_2 : Module k E]
  [inst_3 : AddTorsor E PE] (f : k → PE) (a b r : k),
  (AffineMap.lineMap (slope f ((AffineMap.lineMap a b) r) b) (slope f a ((AffineMap.lineMap a b) r))) r = slope f a b
-- Std.Do.PredTrans
/-- The predicate transformer is conjunctive: `t (Q₁ ∧ₚ Q₂) ⊣⊢ₛ t Q₁ ∧ t Q₂`.
So the stronger the postcondition, the stronger the resulting precondition.
 -/
Std.Do.PredTrans.conjunctive : ∀ {ps : Std.Do.PostShape} {α : Type u} (t : Std.Do.PredTrans ps α), Std.Do.PredTrans.Conjunctive t.apply
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
/-- When a function has a limit at infinity, and its derivative is nonpositive, then the derivative
is automatically integrable on `(a, +∞)`. Version assuming differentiability
on `[a, +∞)`.  -/
MeasureTheory.integrableOn_Ioi_deriv_of_nonpos' : ∀ {g g' : ℝ → ℝ} {a l : ℝ},
  (∀ x ∈ Set.Ici a, HasDerivAt g (g' x) x) →
    (∀ x ∈ Set.Ioi a, g' x ≤ 0) →
      Filter.Tendsto g Filter.atTop (nhds l) → MeasureTheory.IntegrableOn g' (Set.Ioi a) MeasureTheory.volume
-- Mathlib.CategoryTheory.Preadditive.Injective.LiftingProperties
CategoryTheory.Injective.hasLiftingProperty_of_isZero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B I Z : C} (i : A ⟶ B) [CategoryTheory.Mono i]
  [CategoryTheory.Injective I] (p : I ⟶ Z), CategoryTheory.Limits.IsZero Z → CategoryTheory.HasLiftingProperty i p
-- Mathlib.Algebra.Polynomial.Div
Polynomial.leadingCoeff_divByMonic_X_sub_C : ∀ {R : Type u} [inst : CommRing R] [IsDomain R] (p : Polynomial R),
  p.degree ≠ 0 → ∀ (a : R), (p /ₘ (Polynomial.X - Polynomial.C a)).leadingCoeff = p.leadingCoeff
-- Init.Omega.LinearCombo
Lean.Omega.LinearCombo.mul.eq_1 : ∀ (l₁ l₂ : Lean.Omega.LinearCombo), l₁.mul l₂ = l₂.const * l₁ + l₁.const * l₂ - { const := l₁.const * l₂.const }
-- Mathlib.LinearAlgebra.PerfectPairing.Restrict
_private.Mathlib.LinearAlgebra.PerfectPairing.Restrict.0.LinearMap.restrict_aux : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (p : M →ₗ[R] N →ₗ[R] R) [inst_5 : p.IsPerfPair] {M' : Type u_4}
  {N' : Type u_5} [inst_6 : AddCommGroup M'] [inst_7 : Module R M'] [inst_8 : AddCommGroup N'] [inst_9 : Module R N']
  (i : M' →ₗ[R] M) (j : N' →ₗ[R] N),
  Function.Injective ⇑i → Function.Injective ⇑j → p.IsPerfectCompl i.range j.range → Function.Bijective ⇑(p.compl₁₂ i j)
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.map_toTransfiniteCompositionOfShape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {J : Type w} [inst_2 : LinearOrder J] [inst_3 : SuccOrder J] [inst_4 : OrderBot J] [inst_5 : WellFoundedLT J]
  {X Y : C} {f : X ⟶ Y} {W : CategoryTheory.MorphismProperty D} {F : CategoryTheory.Functor C D}
  [inst_6 : CategoryTheory.Limits.PreservesWellOrderContinuousOfShape J F]
  [inst_7 : CategoryTheory.Limits.PreservesColimitsOfShape J F]
  (h : (W.inverseImage F).TransfiniteCompositionOfShape J f), h.map.toTransfiniteCompositionOfShape = h.map F
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.size_alter_eq_add_one : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {f : Option (β k) → Option (β k)},
  k ∉ t → (f (t.get? k)).isSome = true → (t.alter k f).size = t.size + 1
-- Mathlib.RingTheory.ZMod
/-- Two ring homomorphisms into `ZMod n` with equal kernels are equal.  -/
ZMod.ringHom_eq_of_ker_eq : ∀ {n : ℕ} {R : Type u_1} [inst : Ring R] (f g : R →+* ZMod n), RingHom.ker f = RingHom.ker g → f = g
-- Mathlib.Geometry.Manifold.MFDeriv.Defs
/-- Property in the model space of a model with corners of being differentiable within a set at a
point, when read in the model vector space. This property will be lifted to manifolds to define
differentiable functions between manifolds.  -/
DifferentiableWithinAtProp : {𝕜 : 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] →
              ModelWithCorners 𝕜 E H →
                {E' : Type u_5} →
                  [inst_4 : NormedAddCommGroup E'] →
                    [inst_5 : NormedSpace 𝕜 E'] →
                      {H' : Type u_6} →
                        [inst_6 : TopologicalSpace H'] → ModelWithCorners 𝕜 E' H' → (H → H') → Set H → H → Prop
-- Mathlib.Topology.Algebra.Valued.LocallyCompact
Valued.integer.totallyBounded_iff_finite_residueField : ∀ {K : Type u_1} {Γ₀ : Type u_2} [inst : Field K] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [inst_2 : Valued K Γ₀]
  [Valued.v.RankOne] [IsDiscreteValuationRing ↥(Valued.integer K)],
  TotallyBounded Set.univ ↔ Finite (Valued.ResidueField K)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- The continuous homomorphism given by the diagonal embedding.  -/
ContinuousAddMonoidHom.diag : (A : Type u_2) → [inst : AddMonoid A] → [inst_1 : TopologicalSpace A] → A →ₜ+ A × A
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Multiplying the first vector passed to `oangle` by a nonzero real does not change twice the
angle.  -/
Orientation.two_zsmul_oangle_smul_left_of_ne_zero : ∀ {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) {r : ℝ}, r ≠ 0 → 2 • o.oangle (r • x) y = 2 • o.oangle x y
-- Mathlib.InformationTheory.KullbackLeibler.Basic
InformationTheory.mul_log_le_klDiv : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν],
  ENNReal.ofReal (μ.real Set.univ * Real.log (μ.real Set.univ / ν.real Set.univ) + ν.real Set.univ - μ.real Set.univ) ≤
    InformationTheory.klDiv μ ν
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.normSq_lt_one : ∀ (z : Complex.UnitDisc), Complex.normSq ↑z < 1
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
NumberField.mixedEmbedding.polarCoord_target_eq_polarCoordReal_target : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  (NumberField.mixedEmbedding.polarCoord K).target = (NumberField.mixedEmbedding.polarCoordReal K).target
-- Mathlib.Algebra.Group.Even
Even.add : ∀ {α : Type u_2} [inst : AddCommSemigroup α] {a b : α}, Even a → Even b → Even (a + b)
-- Mathlib.MeasureTheory.MeasurableSpace.Prod
MeasurableEmbedding.prodMk_left : ∀ {α : Type u_1} [inst : MeasurableSpace α] {β : Type u_3} {γ : Type u_4} [MeasurableSingletonClass α]
  {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (x : α) {f : γ → β},
  MeasurableEmbedding f → MeasurableEmbedding fun y => (x, f y)
-- Mathlib.Analysis.SpecificLimits.Basic
/-- A series whose terms are bounded by the terms of a converging geometric series converges.  -/
summable_one_div_pow_of_le : ∀ {m : ℝ} {f : ℕ → ℕ}, 1 < m → (∀ (i : ℕ), i ≤ f i) → Summable fun i => 1 / m ^ f i
-- Init.Grind.PP
Lean.Grind.NodeDef.unit.sizeOf_spec : sizeOf Lean.Grind.NodeDef.unit = 1
-- Mathlib.Topology.Sober
IsGenericPoint.disjoint_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {S U : Set α},
  IsGenericPoint x S → IsOpen U → (Disjoint S U ↔ x ∉ U)
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.any_eq_match_step : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Std.IteratorLoop α Id Id]
  [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β} {p : β → Bool},
  Std.Iter.any p it =
    match ↑it.step with
    | Std.IterStep.yield it' x => if p x = true then true else Std.Iter.any p it'
    | Std.IterStep.skip it' => Std.Iter.any p it'
    | Std.IterStep.done => false
-- Mathlib.Algebra.Group.Hom.Defs
MulHom.coe_coe : ∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : Mul M] [inst_1 : Mul N] [inst_2 : FunLike F M N]
  [inst_3 : MulHomClass F M N] (f : F), ⇑↑f = ⇑f
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.contains_iff_mem : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] {a : α},
  m.contains a = true ↔ a ∈ m
-- Init.Data.Int.Gcd
Int.gcd_eq_right : ∀ {b a : ℤ}, 0 ≤ b → b ∣ a → ↑(a.gcd b) = b
-- Mathlib.RingTheory.Ideal.Operations
Ideal.IsPrime.inf_le' : ∀ {R : Type u} {ι : Type u_1} [inst : CommSemiring R] {s : Finset ι} {f : ι → Ideal R} {P : Ideal R},
  P.IsPrime → (s.inf f ≤ P ↔ ∃ i ∈ s, f i ≤ P)
-- Mathlib.Algebra.Ring.Nat
Nat.instDistrib : Distrib ℕ
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.untopD_one : ∀ {α : Type u} [inst : One α] (d : α), WithTop.untopD d 1 = 1
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
/-- All functions in the tail of a well-formed basis are little-o of the basis' head.  -/
Tactic.ComputeAsymptotics.WellFormedBasis.tail_isLittleO_head : ∀ {hd : ℝ → ℝ} {tl : Tactic.ComputeAsymptotics.Basis},
  Tactic.ComputeAsymptotics.WellFormedBasis (hd :: tl) →
    ∀ {f : ℝ → ℝ}, f ∈ tl → (Real.log ∘ f) =o[Filter.atTop] (Real.log ∘ hd)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.filter_eq_self_iff : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Bool},
  Std.ExtHashMap.filter f m = m ↔ ∀ (k : α) (h : k ∈ m), f (m.getKey k h) m[k] = true
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.WithUpperSet.instTopologicalSpace : {α : Type u_1} → [Preorder α] → TopologicalSpace (Topology.WithUpperSet α)
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.range_toSubmodule : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  (ρ : Representation A G V) (σ : Representation A G W) (f : ρ.IntertwiningMap σ),
  (Representation.IntertwiningMap.range ρ σ f).toSubmodule = f.range
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ico_filter_le_of_right_le : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b : α} [inst_2 : DecidablePred fun x => b ≤ x],
  {x ∈ Finset.Ico a b | b ≤ x} = ∅
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.Kernel.HasSubgaussianMGF.memLp_exp_mul : ∀ {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'}
  {κ : ProbabilityTheory.Kernel Ω' Ω} {X : Ω → ℝ} {c : NNReal},
  ProbabilityTheory.Kernel.HasSubgaussianMGF X c κ ν →
    ∀ (t : ℝ) (p : NNReal), MeasureTheory.MemLp (fun ω => Real.exp (t * X ω)) (↑p) (ν.bind ⇑κ)
-- Mathlib.Algebra.Group.Int.Even
Int.instDecidablePredEven : DecidablePred Even
-- Mathlib.CategoryTheory.Category.Factorisation
CategoryTheory.Factorisation.terminalHom_h : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (d : CategoryTheory.Factorisation f),
  d.terminalHom.h = d.π
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHom.id_comp : ∀ {M : Type u_4} {N : Type u_5} [inst : AddZero M] [inst_1 : AddZero N] (f : M →+ N), (AddMonoidHom.id N).comp f = f
-- Mathlib.Data.Rat.Lemmas
Rat.den_div_natCast_eq_one_iff : ∀ (m n : ℕ), n ≠ 0 → ((↑m / ↑n).den = 1 ↔ n ∣ m)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_le_rpow_left_iff_of_base_lt_one : ∀ {x y z : ℝ}, 0 < x → x < 1 → (x ^ y ≤ x ^ z ↔ z ≤ y)
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.or_congr_l : ∀ {σs : List (Type u)} {P P' Q : Std.Do.SPred σs}, (P ⊣⊢ₛ P') → P ∨ Q ⊣⊢ₛ P' ∨ Q