mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.LocalSourceTargetProperty
/-- If `P` is monotone w.r.t. restricting `domChart` and closed under congruence,
if `f` has property `P` at `x` and `f` and `g` are eventually equal near `x`,
then `g` has property `P` at `x`.  -/
Manifold.LiftSourceTargetPropertyAt.congr_of_eventuallyEq : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_4} {H : Type u_6} {G : Type u_8} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : TopologicalSpace H] [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G}
  {M : Type u_10} {N : Type u_12} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f g : M → N} {x : M}
  {P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop},
  Manifold.IsLocalSourceTargetProperty P →
    Manifold.LiftSourceTargetPropertyAt I J n f x P → f =ᶠ[nhds x] g → Manifold.LiftSourceTargetPropertyAt I J n g x P
-- Init.Data.List.TakeDrop
List.dropWhile.eq_1 : ∀ {α : Type u} (p : α → Bool), List.dropWhile p [] = []
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.join_mono : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P P' Q Q' : l},
  Lean.Order.PartialOrder.rel P P' →
    Lean.Order.PartialOrder.rel Q Q' → Lean.Order.PartialOrder.rel (Lean.Order.join P Q) (Lean.Order.join P' Q')
-- Mathlib.MeasureTheory.Measure.Tilted
MeasureTheory.tilted_zero : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ],
  μ.tilted 0 = μ
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.AreEqualizedByLocalization.map_eq_of_isInvertedBy : ∀ {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] {W : CategoryTheory.MorphismProperty C} {X Y : C} {f g : X ⟶ Y},
  CategoryTheory.AreEqualizedByLocalization W f g →
    ∀ (F : CategoryTheory.Functor C D), W.IsInvertedBy F → F.map f = F.map g
-- Mathlib.Algebra.Ring.GeomSum
Odd.nat_add_dvd_pow_add_pow : ∀ (x y : ℕ) {n : ℕ}, Odd n → x + y ∣ x ^ n + y ^ n
-- Mathlib.Data.Finsupp.Basic
/-- Given `l`, a finitely supported function from the sigma type `Σ i, αs i` to `β` and
an `ι`-indexed family `g` of functions from `(αs i →₀ β)` to `γ`, `split_comp` defines a
finitely supported function from the index type `ι` to `γ` given by composing `g i` with
`split l i`.  -/
Finsupp.splitComp : {ι : Type u_4} →
  {M : Type u_5} →
    {N : Type u_6} →
      {αs : ι → Type u_12} →
        [inst : Zero M] →
          ((i : ι) × αs i →₀ M) →
            [inst_1 : Zero N] →
              (g : (i : ι) → (αs i →₀ M) → N) → (∀ (i : ι) (x : αs i →₀ M), x = 0 ↔ g i x = 0) → ι →₀ N
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
AEMeasurable.dist : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α]
  [inst_3 : MeasurableSpace β] [SecondCountableTopology α] {f g : β → α} {μ : MeasureTheory.Measure β},
  AEMeasurable f μ → AEMeasurable g μ → AEMeasurable (fun b => dist (f b) (g b)) μ
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.isCoprime_x_y : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : FermatLastTheoremForThreeGen.Solution✝ hζ)
  [inst_1 : NumberField K] [inst_2 : IsCyclotomicExtension {3} ℚ K],
  IsCoprime (FermatLastTheoremForThreeGen.Solution.x✝ S) (FermatLastTheoremForThreeGen.Solution.y✝ S)
-- Mathlib.Combinatorics.Graph.Simple
Graph.loopless_iff_forall_ne_of_adj : ∀ {α : Type u_1} {β : Type u_2} {G : Graph α β}, G.Loopless ↔ ∀ (u v : α), G.Adj u v → u ≠ v
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
/-- Interval integrability is invariant when functions change along discrete sets.  -/
IntervalIntegrable.congr_codiscreteWithin : ∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] [TopologicalSpace.PseudoMetrizableSpace ε]
  {f : ℝ → ε} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {g : ℝ → ε} [MeasureTheory.NullSingletonClass μ],
  f =ᶠ[Filter.codiscreteWithin (Set.uIoc a b)] g → IntervalIntegrable f μ a b → IntervalIntegrable g μ a b
-- Mathlib.Tactic.IntervalCases
Mathlib.Tactic.IntervalCases.of_not_le_left : ∀ {α : Type u_1} {a b a' : α} [inst : LE α], ¬a ≤ b → a = a' → ¬a' ≤ b
-- Lean.Expr
Lean.Expr.appFn! : Lean.Expr → Lean.Expr
-- Init.Data.String.Defs
String.instDecidableIsAtEnd_1 : {s : String.Slice} → {pos : s.Pos} → Decidable pos.IsAtEnd
-- Mathlib.Analysis.Normed.Group.Constructions
/-- Product of normed groups, using the sup norm.  -/
Prod.normedAddCommGroup : {E : Type u_2} → {F : Type u_3} → [NormedAddCommGroup E] → [NormedAddCommGroup F] → NormedAddCommGroup (E × F)
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.comap_le_comap_iff_of_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F},
  Function.Surjective ⇑f → ∀ {S T : AddSubmonoid N}, AddSubmonoid.comap f S ≤ AddSubmonoid.comap f T ↔ S ≤ T
-- Mathlib.Tactic.Linter.MinImports
/-- The minimal imports needed to build the file up to the current command.  -/
_private.Mathlib.Tactic.Linter.MinImports.0.Mathlib.Linter.ImportState.minImports : Mathlib.Linter.ImportState✝ → Lean.NameSet
-- Mathlib.RingTheory.MvPolynomial.Ideal
MvPolynomial.idealOfVars_fg : ∀ (σ : Type u_1) (R : Type u_2) [inst : CommSemiring R] [Finite σ], (MvPolynomial.idealOfVars σ R).FG
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Eta-expanded form of `HasStrictFDerivAt.neg` -/
HasStrictFDerivAt.fun_neg : ∀ {𝕜 : 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} {x : E}, HasStrictFDerivAt f f' x → HasStrictFDerivAt (fun i => -f i) (-f') x
-- Mathlib.Algebra.Homology.Embedding.Basic
ComplexShape.instIsTruncLEEmbeddingDown'Add : ∀ {A : Type u_3} [inst : AddCommSemigroup A] [inst_1 : IsRightCancelAdd A] (a b : A),
  (ComplexShape.embeddingDown'Add a b).IsTruncLE
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
/-- `rieszContent` gives a `Content` from `Λ : C_c(X, ℝ≥0) →ₗ[ℝ≥0] ℝ≥0`. Here `rieszContent Λ` is
promoted to a measure. It will be later shown that
`∫ (x : X), f x ∂(rieszMeasure Λ hΛ) = Λ f` for all `f : C_c(X, ℝ≥0)`.  -/
NNRealRMK.rieszMeasure : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    (CompactlySupportedContinuousMap X NNReal →ₗ[NNReal] NNReal) →
      [T2Space X] → [LocallyCompactSpace X] → [inst_3 : MeasurableSpace X] → [BorelSpace X] → MeasureTheory.Measure X
-- Mathlib.CategoryTheory.FiberedCategory.Fiber
/-- Given a functor `F : C ⥤ 𝒳` such that `F ⋙ p` is constant at some `S : 𝒮`, then
we get a natural isomorphism between `inducedFunctor _ ⋙ fiberInclusion` and `F`.  -/
CategoryTheory.Functor.Fiber.inducedFunctorCompIsoSelf : {𝒮 : Type u₁} →
  {𝒳 : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳] →
        {p : CategoryTheory.Functor 𝒳 𝒮} →
          {S : 𝒮} →
            {C : Type u₃} →
              [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
                {F : CategoryTheory.Functor C 𝒳} →
                  (hF : F.comp p = (CategoryTheory.Functor.const C).obj S) →
                    (CategoryTheory.Functor.Fiber.inducedFunctor hF).comp CategoryTheory.Functor.Fiber.fiberInclusion ≅
                      F
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_union!_iff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        Std.DTreeMap.Internal.Impl.contains k (m₁.union! m₂) = true ↔
          Std.DTreeMap.Internal.Impl.contains k m₁ = true ∨ Std.DTreeMap.Internal.Impl.contains k m₂ = true
-- Mathlib.Order.RelIso.Set
Equiv.subtypeUnivEquiv.congr_simp : ∀ {α : Sort u_9} {p : α → Prop} (h : ∀ (x : α), p x), Equiv.subtypeUnivEquiv h = Equiv.subtypeUnivEquiv h
-- Init.System.IO
IO.FS.instReprDirEntry.repr : IO.FS.DirEntry → ℕ → Std.Format
-- Mathlib.Order.BoundedOrder.Basic
eq_top_of_top_eq_bot : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : BoundedOrder α], ⊤ = ⊥ → ∀ (x : α), x = ⊤
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_Icc_castSucc : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a b : Fin n),
  ∑ i ∈ Finset.Icc a.castSucc b.castSucc, f i = ∑ i ∈ Finset.Icc a b, f i.castSucc
-- Mathlib.CategoryTheory.Equivalence
/-- `Equivalence.mk'` is the dual of `Equivalence.mk`, which we need for `to_dual`.
Please avoid using this directly.  -/
CategoryTheory.Equivalence.mk'' : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (functor : CategoryTheory.Functor C D) →
          (inverse : CategoryTheory.Functor D C) →
            (unitIso : CategoryTheory.Functor.id C ≅ functor.comp inverse) →
              (counitIso : inverse.comp functor ≅ CategoryTheory.Functor.id D) →
                (∀ (X : C),
                    CategoryTheory.CategoryStruct.comp (counitIso.inv.app (functor.obj X))
                        (functor.map (unitIso.inv.app X)) =
                      CategoryTheory.CategoryStruct.id (functor.obj X)) →
                  (C ≌ D)
-- Mathlib.Algebra.Polynomial.Smeval
Polynomial.smeval_commute : ∀ (R : Type u_1) [inst : Semiring R] (p q : Polynomial R) {S : Type u_2} [inst_1 : Semiring S] [inst_2 : Module R S]
  [IsScalarTower R S S] [SMulCommClass R S S] {x y : S}, Commute x y → Commute (p.smeval x) (q.smeval y)
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
LinearMap.BilinMap.toQuadraticMap_add : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (B₁ B₂ : LinearMap.BilinMap R M N),
  (B₁ + B₂).toQuadraticMap = B₁.toQuadraticMap + B₂.toQuadraticMap
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_insert_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {k : α} {v : β k},
  (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.get? k = some v
-- Mathlib.Data.Sigma.Interval
Sigma.card_Ioo : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → Preorder (α i)]
  [inst_2 : (i : ι) → LocallyFiniteOrder (α i)] (a b : (i : ι) × α i),
  (Finset.Ioo a b).card = if h : a.fst = b.fst then (Finset.Ioo (h ▸ a.snd) b.snd).card else 0
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
CategoryTheory.Functor.isInitialConst_to_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {X : D} (hX : CategoryTheory.Limits.IsInitial X)
  (F : CategoryTheory.Functor C D) (Y : C), ((CategoryTheory.Functor.isInitialConst C hX).to F).app Y = hX.to (F.obj Y)
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.map_obj_right : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {A' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] {B' : Type u₅} [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  {T' : Type u₆} [inst_5 : CategoryTheory.Category.{v₆, u₆} T'] {L : CategoryTheory.Functor A T}
  {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'}
  {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'}
  (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') (X : CategoryTheory.Comma L R),
  ((CategoryTheory.Comma.map α β).obj X).right = F₂.obj X.right
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
/-- `f` is right homotopic to `g` iff `g` is right homotopic to `f`.  -/
CategoryTheory.Arrow.RightHomotopy.symm : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    [inst_1 : CategoryTheory.Preadditive V] →
      {u v : CategoryTheory.Arrow V} →
        {f g : u ⟶ v} → CategoryTheory.Arrow.RightHomotopy f g → CategoryTheory.Arrow.RightHomotopy g f
-- Init.Data.String.Defs
String.bytes : String → ByteArray
-- Mathlib.Topology.Algebra.UniformConvergence
instOneUniformFun.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : One β], instOneUniformFun = { one := instOneUniformFun._aux_1 }
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
AlgebraicGeometry.universallyClosed_respectsIso : CategoryTheory.MorphismProperty.RespectsIso @AlgebraicGeometry.UniversallyClosed
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.succ_le_succ_iff : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α]
  [inst_2 : Std.PRange.InfinitelyUpwardEnumerable α] [Std.PRange.LinearlyUpwardEnumerable α] {a b : α},
  Std.PRange.UpwardEnumerable.LE (Std.PRange.succ a) (Std.PRange.succ b) ↔ Std.PRange.UpwardEnumerable.LE a b
-- Mathlib.Data.Rat.Sqrt
Rat.sqrt.eq_1 : ∀ (q : ℚ), Rat.sqrt q = mkRat (Int.sqrt q.num) q.den.sqrt
-- Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Matrix.Represents.eq : ∀ {ι : Type u_1} [inst : Fintype ι] {M : Type u_2} [inst_1 : AddCommGroup M] {R : Type u_3} [inst_2 : CommRing R]
  [inst_3 : Module R M] {b : ι → M} [inst_4 : DecidableEq ι],
  Submodule.span R (Set.range b) = ⊤ →
    ∀ {A : Matrix ι ι R} {f f' : Module.End R M}, Matrix.Represents b A f → Matrix.Represents b A f' → f = f'
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.isValidRevSearchFrom_cast_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s t : String.Slice} (hst : s.copy = t.copy)
  {pos : s.Pos} {l : List (String.Slice.Pattern.SearchStep t)},
  String.Slice.Pattern.Model.IsValidRevSearchFrom pat (pos.cast hst) l ↔
    String.Slice.Pattern.Model.IsValidRevSearchFrom pat pos
      (List.map (fun x => String.Slice.Pattern.SearchStep.cast ⋯ x) l)
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
/-- The equivalence of `fixingSubgroup M t` with `fixingSubgroup M s`
when `s` is a translate of `t`.  -/
SubAddAction.fixingAddSubgroupEquivFixingAddSubgroup : {M : Type u_1} →
  {α : Type u_2} →
    [inst : AddGroup M] →
      [inst_1 : AddAction M α] →
        {s t : Set α} → {g : M} → g +ᵥ t = s → ↥(fixingAddSubgroup M t) ≃+ ↥(fixingAddSubgroup M s)
-- Mathlib.Algebra.Module.Congruence.Defs
SMulCon.instSMulWithZeroQuotient : {S : Type u_2} →
  (M : Type u_3) →
    [inst : Zero S] →
      [inst_1 : Zero M] → [inst_2 : SMulWithZero S M] → (c : SMulCon S M) → SMulWithZero S (SMulCon.Quotient M c)
-- Mathlib.CategoryTheory.Presentable.SharplyLT.Basic
_private.Mathlib.CategoryTheory.Presentable.SharplyLT.Basic.0.Cardinal.SharplyLT.existsIsCardinalFilteredSetOfExistsCofinal.le_φ : ∀ {κ₁ κ₂ : Cardinal.{w}} [Fact κ₁.IsRegular] {X : Type w}
  (Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (CategoryTheory.CardinalDirectedPoset.SetCardinalLT κ₁ ↑B)),
  (∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), IsCofinal (Y B hB)) →
    ∀
      (m :
        (B : Set X) →
          (hB : HasCardinalLT (↑B) κ₂) →
            (C : CategoryTheory.CardinalDirectedPoset.SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X)
      (B : Set X), B ⊆ Cardinal.SharplyLT.existsIsCardinalFilteredSetOfExistsCofinal.φ✝ Y m B
-- Init.Data.Nat.Div.Lemmas
Nat.ext_div_mod : ∀ {n a b : ℕ}, a / n = b / n → a % n = b % n → a = b
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.erasePTR.go.eq_2 : ∀ {α : Type u_1} (p : α → Bool) (l : List α) (a : Array α) (a_1 : α) (as : List α),
  List.erasePTR.go✝ p l (a_1 :: as) a = bif p a_1 then a.toListAppend as else List.erasePTR.go✝ p l as (a.push a_1)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.card_singleton_mul : ∀ {α : Type u_2} [inst : Mul α] [IsLeftCancelMul α] [inst_2 : DecidableEq α] (a : α) (t : Finset α),
  ({a} * t).card = t.card
-- Mathlib.Algebra.Module.ZLattice.Basic
/-- A version of `ZSpan.isAddFundamentalDomain` for `AddSubgroup`.  -/
ZSpan.isAddFundamentalDomain' : ∀ {E : Type u_1} {ι : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (b : Module.Basis ι ℝ E)
  [Finite ι] [inst_3 : MeasurableSpace E] [OpensMeasurableSpace E] (μ : MeasureTheory.Measure E),
  MeasureTheory.IsAddFundamentalDomain (↥(Submodule.span ℤ (Set.range ⇑b)).toAddSubgroup) (ZSpan.fundamentalDomain b) μ
-- Mathlib.MeasureTheory.Measure.MutuallySingular
MeasureTheory.Measure.mutuallySingular_tfae : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α},
  [μ.MutuallySingular ν, Disjoint μ ν, Disjoint (MeasureTheory.ae μ) (MeasureTheory.ae ν)].TFAE
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PullbackObjObj.ofIsInitial_π : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  (G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₃ Y₃ : C₃}
  (f₃ : X₃ ⟶ Y₃)
  [inst_3 : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (G.flip.obj X₃)]
  [inst_4 : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (G.flip.obj Y₃)]
  (h : CategoryTheory.Limits.IsInitial X₁),
  (CategoryTheory.Functor.PullbackObjObj.ofIsInitial G f₁ f₃ h).π = (G.obj (Opposite.op Y₁)).map f₃
-- Mathlib.Topology.MetricSpace.CoveringNumbers
Metric.externalCoveringNumber_le_one_of_ediam_le : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {A : Set X} {ε : NNReal},
  Metric.ediam A ≤ ↑ε → Metric.externalCoveringNumber ε A ≤ 1
-- Mathlib.LinearAlgebra.Matrix.Hermitian
/-- Note this is more general than `IsSelfAdjoint.conjugate'` as `B` can be rectangular.  -/
Matrix.isHermitian_conjTranspose_mul_mul : ∀ {α : Type u_1} {m : Type u_3} {n : Type u_4} [inst : NonUnitalSemiring α] [inst_1 : StarRing α] [inst_2 : Fintype m]
  {A : Matrix m m α} (B : Matrix m n α), A.IsHermitian → (B.conjTranspose * A * B).IsHermitian
-- Mathlib.Data.Fin.Tuple.Basic
Fin.insertNth_removeNth : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u_1} (p : Fin (n + 1)) (x : α p) (f : (j : Fin (n + 1)) → α j),
  p.insertNth x (p.removeNth f) = Function.update f p x
-- Mathlib.Computability.StateTransition
/-- The transitive closure of a state transition function. `Reaches₁ f a b` means there is a
nonempty finite sequence of steps `f a = some a₁`, `f a₁ = some a₂`, ... such that `aₙ = b`.
This relation does not permit zero steps of the state transition function.  -/
StateTransition.Reaches₁ : {σ : Type u_1} → (σ → Option σ) → σ → σ → Prop
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.algebraMap_exp_comm : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕂] [inst_1 : CharZero 𝕂] [ContinuousSMul ℚ 𝕂]
  [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝕂] (x : 𝕂),
  (algebraMap 𝕂 𝔸) (NormedSpace.exp x) = NormedSpace.exp ((algebraMap 𝕂 𝔸) x)
-- Mathlib.Data.List.Rotate
List.isRotated_reverse_comm_iff : ∀ {α : Type u} {l l' : List α}, l.reverse ~r l' ↔ l ~r l'.reverse
-- Mathlib.CategoryTheory.Sums.Products
/-- Composing the forward direction of `functorEquiv` with the first projection is the same as
precomposition with `inl_ A A'`.  -/
CategoryTheory.Sum.functorEquivFunctorCompFstIso : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    {A' : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] →
        {B : Type u} →
          [inst_2 : CategoryTheory.Category.{v, u} B] →
            (CategoryTheory.Sum.functorEquiv A A' B).functor.comp
                (CategoryTheory.Prod.fst (CategoryTheory.Functor A B) (CategoryTheory.Functor A' B)) ≅
              (CategoryTheory.Functor.whiskeringLeft A (A ⊕ A') B).obj (CategoryTheory.Sum.inl_ A A')
-- Init.Data.Range.Polymorphic.IntLemmas
Int.map_add_toArray_roc : ∀ {m n k : ℤ}, Array.map (fun x => x + k) (m<...=n).toArray = ((m + k)<...=n + k).toArray
-- Mathlib.GroupTheory.Focal
Subgroup.instIsMulCommutativeQuotientSubtypeMemFocalSubgroupOf : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), IsMulCommutative (↥H ⧸ H.focalSubgroupOf)
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.mem_iff_norm_starProjection : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (U : Submodule 𝕜 E) [inst_3 : U.HasOrthogonalProjection] (v : E), v ∈ U ↔ ‖U.starProjection v‖ = ‖v‖
-- Mathlib.Algebra.Module.ZLattice.Covolume
/-- A version of `ZLattice.covolume.tendsto_card_div_pow` for the `InnerProductSpace` case;
see the `Naming convention` section in the introduction.  -/
ZLattice.covolume.tendsto_card_div_pow' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] (L : Submodule ℤ E) [inst_5 : DiscreteTopology ↥L]
  [IsZLattice ℝ L] {s : Set E},
  Bornology.IsBounded s →
    MeasurableSet s →
      MeasureTheory.volume (frontier s) = 0 →
        Filter.Tendsto (fun n => ↑(Nat.card ↑(s ∩ (↑n)⁻¹ • ↑L)) / ↑n ^ Module.finrank ℝ E) Filter.atTop
          (nhds (MeasureTheory.volume.real s / ZLattice.covolume L MeasureTheory.volume))
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.equalizerSubobject_of_self : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.Limits.equalizerSubobject f f = ⊤
-- Init.Data.Nat.Lemmas
Nat.eq_zero_of_add_eq_zero_right : ∀ {n m : ℕ}, n + m = 0 → n = 0
-- Mathlib.Order.Hom.Lattice
InfHom.coe_copy : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : Min β] (f : InfHom α β) (f' : α → β) (h : f' = ⇑f),
  ⇑(f.copy f' h) = f'
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
range_cfc_nnreal_subset : ∀ {A : Type u_1} [inst : Ring A] [inst_1 : StarRing A] [inst_2 : Algebra ℝ A] [inst_3 : TopologicalSpace A]
  [inst_4 : IsTopologicalRing A] [T2Space A] [inst_6 : PartialOrder A] [inst_7 : NonnegSpectrumClass ℝ A]
  [inst_8 : StarOrderedRing A] [inst_9 : ContinuousStar A] [inst_10 : StarModule ℝ A]
  [inst_11 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A),
  autoParam (0 ≤ a) range_cfc_nnreal_subset._auto_1 →
    (Set.range fun x => cfc x a) ⊆ {x | x ∈ StarAlgebra.elemental ℝ a ∧ 0 ≤ x}
-- Init.Data.BitVec.Bitblast
/-- Adding bitvectors that are zero in complementary positions equals concatenation.  -/
BitVec.zero_append_add_append_zero : ∀ {v w : ℕ} {x : BitVec v} {y : BitVec w}, 0#v ++ y + (x ++ 0#w) = x ++ y
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.SimpleFunc.integral_mono_measure : ∀ {α : Type u_1} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [inst_2 : PartialOrder F] [IsOrderedAddMonoid F] [IsOrderedModule ℝ F]
  {ν : MeasureTheory.Measure α} {f : MeasureTheory.SimpleFunc α F},
  0 ≤ᵐ[ν] ⇑f →
    μ ≤ ν →
      MeasureTheory.Integrable (⇑f) ν → MeasureTheory.SimpleFunc.integral μ f ≤ MeasureTheory.SimpleFunc.integral ν f
-- Mathlib.AlgebraicTopology.SimplexCategory.Defs
/-- Homs in `SimplexCategory` are equivalent to order-preserving functions of finite linear
orders.  -/
SimplexCategory.homEquivOrderHom : {a b : SimplexCategory} → (a ⟶ b) ≃ (Fin (a.len + 1) →o Fin (b.len + 1))
-- Mathlib.RingTheory.Congruence.Hom
RingCon.coe_comapQuotientEquivRange_mk : ∀ {M : Type u_1} {N : Type u_2} [inst : Ring M] [inst_1 : Ring N] (c : RingCon M) (f : N →+* M) {d : RingCon N}
  (hcd : d = c.comap f) (x : N), ↑((c.comapQuotientEquivRange f hcd) ↑x) = ↑(f x)