mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Group.Basic
isClosedMap_div_left : ∀ {G : Type w} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] (a : G), IsClosedMap fun x => a / x
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.zero_def : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_2}
  [inst_2 : Zero X] [inst_3 : MulAction R X], 0 = 0 /ₒ 1
-- Mathlib.RingTheory.QuotSMulTop
/-- Reducing a module modulo `r` is the same as right tensoring with `R/(r)`.  -/
QuotSMulTop.equivTensorQuot : {R : Type u_2} →
  [inst : CommRing R] →
    (r : R) →
      (M : Type u_1) →
        [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → QuotSMulTop r M ≃ₗ[R] TensorProduct R M (R ⧸ Ideal.span {r})
-- Mathlib.RingTheory.Spectrum.Maximal.Topology
MaximalSpectrum.toPrimeSpectrum_continuous : ∀ {R : Type u} [inst : CommRing R], Continuous MaximalSpectrum.toPrimeSpectrum
-- Mathlib.Tactic.Determinant.Bird.Cert
/-- Certify the diagonal tail sum in one `BirdDet.stepEntry` application:

```
sumFrom n (i + 1) fun k => (stepEntry n A)^[t] F k k)
```
 -/
Mathlib.Tactic.Determinant.certDiag : {u : Lean.Level} →
  {α : Q(Type u)} →
    {rα : Q(CommRing «$α»)} → ℕ → ℕ → Mathlib.Tactic.Determinant.CertM rα (Mathlib.Tactic.Determinant.Cert rα)
-- Mathlib.Topology.Category.TopCat.Sphere
TopCat.instCompactSpaceCarrierDiskBoundary : ∀ (n : ℕ), CompactSpace ↑(TopCat.diskBoundary n)
-- Plausible.Testable
Plausible.Eq.printableProp : {α : Type u_1} → [Repr α] → {x y : α} → Plausible.PrintableProp (x = y)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coneUnopOfCocone_π : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} (c : CategoryTheory.Limits.Cocone F),
  (CategoryTheory.Limits.coneUnopOfCocone c).π = CategoryTheory.NatTrans.unop c.ι
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.Prod.braiding_unitIso : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D],
  (CategoryTheory.Prod.braiding C D).unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id (C × D))
-- Lean.Parser.Term
Lean.Parser.Term.typeAscription.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Module.Presentation.DirectSum
Module.Relations.directSum_relation : ∀ {A : Type u} [inst : Ring A] {ι : Type w} (relations : ι → Module.Relations A) (x : (i : ι) × (relations i).R),
  (Module.Relations.directSum relations).relation x =
    match x with
    | ⟨i, r⟩ => Finsupp.embDomain (Function.Embedding.sigmaMk i) ((relations i).relation r)
-- Mathlib.RingTheory.RingHom.Smooth
RingHom.FormallySmooth.localizationPreserves : RingHom.LocalizationPreserves @RingHom.FormallySmooth
-- Mathlib.RingTheory.Coalgebra.Basic
Coalgebra.mk : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid A] →
        [inst_2 : Module R A] →
          [toCoalgebraStruct : CoalgebraStruct R A] →
            ↑(TensorProduct.assoc R A A A) ∘ₗ LinearMap.rTensor A CoalgebraStruct.comul ∘ₗ CoalgebraStruct.comul =
                LinearMap.lTensor A CoalgebraStruct.comul ∘ₗ CoalgebraStruct.comul →
              LinearMap.rTensor A CoalgebraStruct.counit ∘ₗ CoalgebraStruct.comul = (TensorProduct.mk R R A) 1 →
                LinearMap.lTensor A CoalgebraStruct.counit ∘ₗ CoalgebraStruct.comul = (TensorProduct.mk R A R).flip 1 →
                  Coalgebra R A
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
AlgebraicGeometry.LocallyRingedSpace.instHasColimits : CategoryTheory.Limits.HasColimits AlgebraicGeometry.LocallyRingedSpace
-- Lean.Meta.Transform
Lean.instReprTransformStep : Repr Lean.TransformStep
-- Lean.Elab.Tactic.Omega.Core
Lean.Elab.Tactic.Omega.Justification.instToString : {s : Lean.Omega.Constraint} → {x : Lean.Omega.Coeffs} → ToString (Lean.Elab.Tactic.Omega.Justification s x)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
_private.Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer.0.CategoryTheory.Limits.MulticospanIndex.multicospanMapIso.match_1.splitter : {J : CategoryTheory.Limits.MulticospanShape} →
  (motive : CategoryTheory.Limits.WalkingMulticospan J → Sort u_3) →
    (i : CategoryTheory.Limits.WalkingMulticospan J) →
      ((a : J.L) → motive (CategoryTheory.Limits.WalkingMulticospan.left a)) →
        ((a : J.R) → motive (CategoryTheory.Limits.WalkingMulticospan.right a)) → motive i
-- Mathlib.Topology.ExtendFrom
extendFrom_extends : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T2Space Y] {f : X → Y}
  {A : Set X}, ContinuousOn f A → ∀ x ∈ A, extendFrom A f x = f x
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.infinite_iff : ∀ {α : Type u}, Infinite α ↔ Cardinal.aleph0 ≤ Cardinal.mk α
-- Mathlib.CategoryTheory.Abelian.LeftDerived
CategoryTheory.ProjectiveResolution.fromLeftDerivedZero'_naturality : ∀ {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} D] [inst_1 : CategoryTheory.Abelian D] {C : Type u_2}
  [inst_2 : CategoryTheory.Category.{v_2, u_2} C] [inst_3 : CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y)
  (P : CategoryTheory.ProjectiveResolution X) (Q : CategoryTheory.ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex),
  CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f →
    ∀ (F : CategoryTheory.Functor C D) [inst_4 : F.Additive],
      CategoryTheory.CategoryStruct.comp
          (HomologicalComplex.opcyclesMap ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ) 0)
          (Q.fromLeftDerivedZero' F) =
        CategoryTheory.CategoryStruct.comp (P.fromLeftDerivedZero' F) (F.map f)
-- Mathlib.SetTheory.Ordinal.Notation
ONote.repr_mul : ∀ (o₁ o₂ : ONote) [o₁.NF] [o₂.NF], (o₁ * o₂).repr = o₁.repr * o₂.repr
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_quot_mk : ∀ {α : Type u_1} [inst : MeasurableSpace α] {r : α → α → Prop}, Measurable (Quot.mk r)
-- Mathlib.Data.List.Basic
List.Disjoint.of_map : ∀ {α : Type u} {β : Type v} {f : α → β} {s t : List α}, (List.map f s).Disjoint (List.map f t) → s.Disjoint t
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.factor_comp_mk : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {p p' : Submodule R M}
  (H : p ≤ p'), Submodule.factor H ∘ₗ p.mkQ = p'.mkQ
-- Init.Data.BitVec.Lemmas
BitVec.msb_extractLsb' : ∀ {w start len : ℕ} {x : BitVec w},
  (BitVec.extractLsb' start len x).msb =
    (decide (0 < len) && (decide (start + len ≤ w) && x.getMsbD (w - (start + len))))
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.symm_dual_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Min α] [inst_1 : Top α] [inst_2 : Min β] [inst_3 : Top β]
  [inst_4 : Min γ] [inst_5 : Top γ] (g : SupBotHom βᵒᵈ γᵒᵈ) (f : SupBotHom αᵒᵈ βᵒᵈ),
  InfTopHom.dual.symm (g.comp f) = (InfTopHom.dual.symm g).comp (InfTopHom.dual.symm f)
-- Mathlib.Logic.Relation
flip_eq_iff : ∀ {α : Type u_1} {r : α → α → Prop}, flip r = r ↔ Std.Symm r
-- Init.Data.BitVec.Lemmas
BitVec.signExtend_xor : ∀ {w v : ℕ} {x y : BitVec w}, BitVec.signExtend v (x ^^^ y) = BitVec.signExtend v x ^^^ BitVec.signExtend v y
-- Mathlib.Topology.VectorBundle.Riemannian
Bundle.RiemannianMetric.symm : ∀ {B : Type u_4} {E : B → Type u_6} [inst : (b : B) → TopologicalSpace (E b)] [inst_1 : (b : B) → AddCommGroup (E b)]
  [inst_2 : (b : B) → Module ℝ (E b)] (self : Bundle.RiemannianMetric E) (b : B) (v w : E b),
  ((self.inner b) v) w = ((self.inner b) w) v
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.inftyRing : {I : Type u_5} →
  {B : I → Type u_6} → [inst : (i : I) → NormedRing (B i)] → [∀ (i : I), NormOneClass (B i)] → Ring ↥(lp B ⊤)
-- Mathlib.Algebra.Homology.Localization
ComplexShape.QFactorsThroughHomotopy.mk : ∀ {ι : Type u_3} {c : ComplexShape ι} {C : Type u_4} [inst : CategoryTheory.Category.{v_2, u_4} C]
  [inst_1 : CategoryTheory.Preadditive C] [inst_2 : CategoryTheory.CategoryWithHomology C],
  (∀ {K L : HomologicalComplex C c} {f g : K ⟶ L} (h : Homotopy f g),
      CategoryTheory.AreEqualizedByLocalization (HomologicalComplex.quasiIso C c) f g) →
    c.QFactorsThroughHomotopy C
-- Lean.Meta.Tactic.Grind.ProveEq
_private.Lean.Meta.Tactic.Grind.ProveEq.0.Lean.Meta.Grind.AbstractM.Context.mk.injEq : ∀ (offset offset_1 : ℕ), ({ offset := offset } = { offset := offset_1 }) = (offset = offset_1)
-- Mathlib.RingTheory.PowerBasis
PowerBasis.dim_le_natDegree_of_root : ∀ {S : Type u_2} [inst : Ring S] {A : Type u_4} [inst_1 : CommRing A] [inst_2 : Algebra A S] (pb : PowerBasis A S)
  {p : Polynomial A}, p ≠ 0 → (Polynomial.aeval pb.gen) p = 0 → pb.dim ≤ p.natDegree
-- Mathlib.Topology.Order.OrderClosed
IsClosed.hypograph : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder α] [t : OrderClosedTopology α]
  [inst_2 : TopologicalSpace β] {f : β → α} {s : Set β},
  IsClosed s → ContinuousOn f s → IsClosed {p | p.1 ∈ s ∧ p.2 ≤ f p.1}
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.Ext.mk₀_homEquiv₀_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (f : CategoryTheory.Abelian.Ext X Y 0),
  CategoryTheory.Abelian.Ext.mk₀ (CategoryTheory.Abelian.Ext.homEquiv₀ f) = f
-- Mathlib.Data.Nat.Log
/-- A version of `log_lt_of_lt_pow` that assumes `x ≠ 0` instead of `y ≠ 0`.  -/
Nat.log_lt_of_lt_pow' : ∀ {b x y : ℕ}, x ≠ 0 → y < b ^ x → Nat.log b y < x
-- Mathlib.Geometry.Convex.Set
Convexity.IsConvexSet.singleton : ∀ {R : Type u_3} {X : Type u_5} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X] {x : X}, Convexity.IsConvexSet R {x}
-- Mathlib.RingTheory.PowerSeries.Basic
Polynomial.coeff_coe : ∀ {R : Type u_1} [inst : Semiring R] (φ : Polynomial R) (n : ℕ), (PowerSeries.coeff n) ↑φ = φ.coeff n
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.AECover.integrable_of_integral_bounded_of_nonneg_ae : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι} [l.NeBot]
  [l.IsCountablyGenerated] {φ : ι → Set α},
  MeasureTheory.AECover μ l φ →
    ∀ {f : α → ℝ} (I : ℝ),
      (∀ (i : ι), MeasureTheory.IntegrableOn f (φ i) μ) →
        (∀ᵐ (x : α) ∂μ, 0 ≤ f x) → (∀ᶠ (i : ι) in l, ∫ (x : α) in φ i, f x ∂μ ≤ I) → MeasureTheory.Integrable f μ
-- Lean.Expr
/-- Similar to `getRevArg!` but skips `mdata`  -/
Lean.Expr.getRevArg!' : Lean.Expr → ℕ → Lean.Expr
-- Init.Data.Nat.Div.Basic
Nat.mod_lt_of_lt : ∀ {a b c : ℕ}, a < c → a % b < c
-- Mathlib.RingTheory.Noetherian.Orzech
/-- Any surjective endomorphism of a Noetherian module is injective.  -/
IsNoetherian.injective_of_surjective_endomorphism : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsNoetherian R M]
  (f : M →ₗ[R] M), Function.Surjective ⇑f → Function.Injective ⇑f
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Example.val : Lean.Expr → Lean.Meta.Match.Example
-- Init.Data.Nat.Div.Lemmas
Nat.div_eq_iff : ∀ {k x y : ℕ}, 0 < k → (x / k = y ↔ y * k ≤ x ∧ x ≤ y * k + k - 1)
-- Mathlib.ModelTheory.DirectLimit
FirstOrder.Language.DirectLimit.unify.eq_1 : ∀ {L : FirstOrder.Language} {ι : Type v} [inst : Preorder ι] {G : ι → Type w} [inst_1 : (i : ι) → L.Structure (G i)]
  (f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)) {α : Type u_1} (x : α → FirstOrder.Language.Structure.Sigma f)
  (i : ι) (h : i ∈ upperBounds (Set.range (Sigma.fst ∘ x))) (a : α),
  FirstOrder.Language.DirectLimit.unify f x i h a = (f (x a).fst i ⋯) (x a).snd
-- Init.Data.List.Count
List.count_erase_self : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {l : List α}, List.count a (l.erase a) = List.count a l - 1
-- Mathlib.CategoryTheory.ObjectProperty.Opposite
CategoryTheory.ObjectProperty.unop_inf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P Q : CategoryTheory.ObjectProperty Cᵒᵖ),
  (P ⊓ Q).unop = P.unop ⊓ Q.unop
-- Lean.ToExpr
Lean.instToExprISize : Lean.ToExpr ISize
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem!_diff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β],
  m₁.WF → m₂.WF → ∀ {k : α}, (m₁ \ m₂)[k]! = if k ∈ m₂ then default else m₁[k]!
-- Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
ExteriorAlgebra.liftAlternatingEquiv_symm_apply : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (F : ExteriorAlgebra R M →ₗ[R] N) (i : ℕ),
  ExteriorAlgebra.liftAlternatingEquiv.symm F i = F.compAlternatingMap (ExteriorAlgebra.ιMulti R i)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.anchorPrefixToString : ℕ → UInt64 → String
-- Init.Data.String.Search
/-- Interprets a string as the decimal representation of an integer, returning it. Panics if the string
does not contain a decimal integer.

A string can be interpreted as a decimal integer if it only consists of at least one decimal digit
and optionally `-` in front. Leading `+` characters are not allowed.

Use `String.isInt` to check whether `String.toInt!` would return a value.
`String.toInt?` is a safer alternative that returns `none` instead of panicking when the
string is not an integer.

Examples:

* `"0".toInt! = 0`

* `"5".toInt! = 5`

* `"587".toInt! = 587`

* `"-587".toInt! = -587`
 -/
String.toInt! : String → ℤ
-- Init.Data.UInt.Bitwise
instIdempotentOpUSizeHOr : Std.IdempotentOp fun x1 x2 => x1 ||| x2
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
cfcₙHom_real_eq_restrict : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : NonUnitalRing A] [inst_2 : StarRing A] [inst_3 : Module ℂ A]
  [inst_4 : IsScalarTower ℂ A A] [inst_5 : SMulCommClass ℂ A A] [T2Space A]
  [inst_7 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal] {a : A} (ha : IsSelfAdjoint a),
  cfcₙHom ha = QuasispectrumRestricts.nonUnitalStarAlgHom (cfcₙHom ⋯) ⋯
-- Mathlib.Order.Fin.Basic
Fin.instPartialOrder : {n : ℕ} → PartialOrder (Fin n)
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.nontrivial' : ∀ {ι : 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) [Nonempty ι]
  [NeZero 2], Nontrivial N
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.mem_adjoin_of_mem : ∀ {R : Type uR} {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {s : Set A} {x : A},
  x ∈ s → x ∈ Algebra.adjoin R s
-- Mathlib.Algebra.Order.Group.Finset
/-- Also see `Finset.sup'_add` that works for ordered groups.  -/
Finset.sup'_add' : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : LinearOrder M] [CanonicallyOrderedAdd M]
  [inst_3 : Sub M] [AddLeftReflectLE M] [OrderedSub M] (s : Finset ι) (f : ι → M) (a : M) (hs : s.Nonempty),
  s.sup' hs f + a = s.sup' hs fun i => f i + a
-- Mathlib.Order.Interval.Finset.Defs
WithTop.Icc_coe_coe : ∀ (α : Type u_1) [inst : PartialOrder α] [inst_1 : OrderTop α] [inst_2 : LocallyFiniteOrder α] (a b : α),
  Finset.Icc ↑a ↑b = Finset.map Function.Embedding.some (Finset.Icc a b)
-- Mathlib.Data.FunLike.IsApply
FunLike.coe_zero : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Zero F] [inst_2 : Zero β]
  [IsZeroApply F α β], ⇑0 = 0
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- For a finite place `w`, return a maximal ideal `v` such that `w = finite_place v` .  -/
NumberField.FinitePlace.maximalIdeal : {K : Type u_1} →
  [inst : Field K] →
    [inst_1 : NumberField K] →
      NumberField.FinitePlace K → IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.IsCircuit.isCocircuit : ∀ {α : Type u_1} {M : Matroid α} {C : Set α}, M.IsCircuit C → M✶.IsCocircuit C
-- Init.Data.String.Lemmas.FindPos
String.Pos.prev?_eq_none : ∀ {s : String} {p : s.Pos}, p = s.startPos → p.prev? = none
-- Mathlib.ModelTheory.Fraisse
FirstOrder.Language.Structure.FG.mem_age_of_equiv : ∀ {L : FirstOrder.Language} {M N : CategoryTheory.Bundled L.Structure},
  FirstOrder.Language.Structure.FG L ↑M → Nonempty (L.Equiv ↑M ↑N) → N ∈ L.age ↑M
-- Mathlib.RingTheory.Ideal.Prime
Ideal.isPrime_bot : ∀ {α : Type u} [inst : Semiring α] [Nontrivial α] [NoZeroDivisors α], ⊥.IsPrime
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestRevMatchAtChain.sliceFrom : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {startPos endPos : s.Pos}
  (h : String.Slice.Pattern.Model.IsLongestRevMatchAtChain pat startPos endPos) (p : s.Pos) (hp : p ≤ startPos),
  String.Slice.Pattern.Model.IsLongestRevMatchAtChain pat (p.sliceFrom startPos hp) (p.sliceFrom endPos ⋯)
-- Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
/-- Given a finite-dimensional space `E` and subspace `K`, the dimensions of `K` and `Kᗮ` add to
that of `E`.  -/
Submodule.finrank_add_finrank_orthogonal' : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [FiniteDimensional 𝕜 E] {K : Submodule 𝕜 E} {n : ℕ},
  Module.finrank 𝕜 ↥K + n = Module.finrank 𝕜 E → Module.finrank 𝕜 ↥Kᗮ = n
-- Mathlib.Data.ENNReal.Operations
ENNReal.lt_add_right : ∀ {a b : ENNReal}, a ≠ ⊤ → b ≠ 0 → a < a + b
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- If the affine span of a set is `⊤`, then the vector span of the same set is the `⊤`.  -/
AffineSubspace.vectorSpan_eq_top_of_affineSpan_eq_top : ∀ (k : Type u_1) (V : Type u_2) (P : Type u_3) [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {s : Set P}, affineSpan k s = ⊤ → vectorSpan k s = ⊤
-- Mathlib.Analysis.Normed.Module.Alternating.Curry
ContinuousAlternatingMap.curryLeft_compContinuousAlternatingMap : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [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] {n : ℕ} (g : F →L[𝕜] G) (f : E [⋀^Fin (n + 1)]→L[𝕜] F)
  (x : E), (g.compContinuousAlternatingMap f).curryLeft x = g.compContinuousAlternatingMap (f.curryLeft x)
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tprod_ite_eq' : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] (b : β)
  [inst_2 : DecidablePred fun x => b = x] (a : β → α)
  (L : optParam (SummationFilter β) (SummationFilter.unconditional β)) [L.LeAtTop],
  (∏'[L] (b' : β), if b = b' then a b' else 1) = a b
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- If the argument has associated syntax, returns it.  -/
Lean.PrettyPrinter.Delaborator.AppImplicitArg.syntax? : Lean.PrettyPrinter.Delaborator.AppImplicitArg → Option Lean.Syntax
-- Mathlib.Algebra.Order.Monovary
Monovary.sub_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : AddCommGroup β] [inst_2 : LinearOrder β]
  [IsOrderedAddMonoid β] {f : ι → α} {g₁ g₂ : ι → β}, Monovary f g₁ → Antivary f g₂ → Monovary f (g₁ - g₂)
-- Mathlib.Algebra.CharP.Lemmas
Commute.add_pow_prime_eq : ∀ {R : Type u_1} [inst : Semiring R] {p : ℕ},
  Nat.Prime p →
    ∀ {x y : R},
      Commute x y →
        (x + y) ^ p =
          x ^ p + y ^ p + ↑p * x * y * ∑ k ∈ Finset.Ioo 0 p, x ^ (k - 1) * y ^ (p - k - 1) * ↑(p.choose k / p)
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.iUnion_eq_empty : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I}, π₁.iUnion = ∅ ↔ π₁ = ⊥
-- Mathlib.Algebra.Colimit.Module
AddCommGroup.DirectLimit.congr_symm_apply_of : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} [inst_1 : (i : ι) → AddCommMonoid (G i)]
  {f : (i j : ι) → i ≤ j → G i →+ G j} [inst_2 : DecidableEq ι] {G' : ι → Type u_5}
  [inst_3 : (i : ι) → AddCommMonoid (G' i)] {f' : (i j : ι) → i ≤ j → G' i →+ G' j} (e : (i : ι) → G i ≃+ G' i)
  (he : ∀ (i j : ι) (h : i ≤ j), (e j).toAddMonoidHom.comp (f i j h) = (f' i j h).comp ↑(e i)) {i : ι} (g : G' i),
  (AddCommGroup.DirectLimit.congr e he).symm ((AddCommGroup.DirectLimit.of G' f' i) g) =
    (AddCommGroup.DirectLimit.of G f i) ((e i).symm g)
-- Init.Prelude
/-- A decidable relation.

A relation is decidable if the corresponding proposition is `Decidable` for all possible arguments.
 -/
DecidableRel : {α : Sort u} → {β : Sort v} → (α → β → Prop) → Sort (max (max 1 u) v)
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PathObject.trans_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {A : C}
  [inst_2 : HomotopicalAlgebra.IsFibrant A] (P P' : HomotopicalAlgebra.PathObject A) [inst_3 : P'.IsGood],
  (P.trans P').ι = CategoryTheory.Limits.pullback.lift P.ι P'.ι ⋯
-- Mathlib.RingTheory.Polynomial.Basic
Polynomial.mem_degreeLE : ∀ {R : Type u} [inst : Semiring R] {n : WithBot ℕ} {f : Polynomial R}, f ∈ Polynomial.degreeLE R n ↔ f.degree ≤ n
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
inv_le_div_iff_le_mul : ∀ {α : Type u} [inst : CommGroup α] [inst_1 : LE α] [MulLeftMono α] {a b c : α}, b⁻¹ ≤ a / c ↔ c ≤ a * b
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigOWith.weaken : ∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {c c' : ℝ}
  {f : α → E} {g' : α → F'} {l : Filter α}, Asymptotics.IsBigOWith c l f g' → c ≤ c' → Asymptotics.IsBigOWith c' l f g'
-- Mathlib.CategoryTheory.Sites.Closed
/-- A sieve `S` is covering for `J` if and only if the subobject classifier
is a sheaf for `S`.  -/
CategoryTheory.GrothendieckTopology.mem_iff_isSheafFor_closedSieves : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {X : C}
  (S : CategoryTheory.Sieve X),
  S ∈ J X ↔ CategoryTheory.Presieve.IsSheafFor (CategoryTheory.Functor.closedSieves J).toFunctor S.arrows
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.ediam_top : ∀ {α : Type u_1} [Nontrivial α], ⊤.ediam = 1
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.σ_comp_yonedaEquiv_symm : ∀ {X : SSet} {n : ℕ} (x : X.obj (Opposite.op { len := n })) (i : Fin (n + 1)),
  CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.σ i) (SSet.yonedaEquiv.symm x) =
    SSet.yonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ X i)) x)
-- Mathlib.Topology.Order.Basic
/-- A countable preordered set equipped with the order topology is second countable.  -/
instSecondCountableTopologyOfOrderTopologyOfCountable : ∀ {α : Type u} [ts : TopologicalSpace α] [inst : Preorder α] [OrderTopology α] [Countable α], SecondCountableTopology α
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_minKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = false → ∀ {fallback fallback' : α}, t.getKeyD (t.minKeyD fallback) fallback' = t.minKeyD fallback
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- Reformulation of equicontinuity at `x₀` comparing two variables near `x₀` instead of comparing
only one with `x₀`.  -/
equicontinuousAt_iff_pair : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {F : ι → X → α} {x₀ : X},
  EquicontinuousAt F x₀ ↔ ∀ U ∈ uniformity α, ∃ V ∈ nhds x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.self_mem_ae_restrict : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasurableSet s → s ∈ MeasureTheory.ae (μ.restrict s)
-- Std.Time.Format.Modifier
Std.Time.instInhabitedDayPeriod.default : Std.Time.DayPeriod
-- Std.Sat.CNF.Basic
Std.Sat.CNF.unsat_def : ∀ {α : Type u_1} (f : Std.Sat.CNF α), f.Unsat ↔ ∀ (a : α → Bool), Std.Sat.CNF.eval a f = false
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
borel_eq_generateFrom_Ici : ∀ (α : Type u_1) [inst : TopologicalSpace α] [SecondCountableTopology α] [inst_2 : LinearOrder α] [OrderTopology α],
  borel α = MeasurableSpace.generateFrom (Set.range Set.Ici)