mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- A weighted sum may be split into a subtraction of such sums over two subsets.  -/
Finset.weightedVSub_sdiff_sub : ∀ {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] {ι : Type u_4} (s : Finset ι) [inst_3 : DecidableEq ι] {s₂ : Finset ι},
  s₂ ⊆ s → ∀ (w : ι → k) (p : ι → P), ((s \ s₂).weightedVSub p) w - (s₂.weightedVSub p) (-w) = (s.weightedVSub p) w
-- Mathlib.Topology.EMetricSpace.VariationOnFromTo
variationOnFromTo.antitoneOn : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {f : α → E} {s : Set α},
  LocallyBoundedVariationOn f s → ∀ {b : α}, b ∈ s → AntitoneOn (fun a => variationOnFromTo f s a b) s
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- **Alias** of `SimpleGraph.Walk.isTrail_mapLe`. -/
SimpleGraph.Walk.mapLe_isTrail : ∀ {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u v : V} {p : G.Walk u v},
  (SimpleGraph.Walk.mapLe h p).IsTrail ↔ p.IsTrail
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
HasSum.sigma_of_hasSum : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] [ContinuousAdd α] [T3Space α]
  {γ : β → Type u_4} {f : (b : β) × γ b → α} {g : β → α} {a : α},
  HasSum g a → (∀ (b : β), HasSum (fun c => f ⟨b, c⟩) (g b)) → Summable f → HasSum f a
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get!_eq_get! : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [inst_2 : LawfulBEq α] [inst_3 : Inhabited β],
  (↑m).WF → ∀ {a : α}, Std.DHashMap.Internal.Raw₀.Const.get! m a = m.get! a
-- Mathlib.Order.Circular.ZMod
Fin.btw_iff : ∀ {n : ℕ} {a b c : Fin n}, btw a b c ↔ a ≤ b ∧ b ≤ c ∨ b ≤ c ∧ c ≤ a ∨ c ≤ a ∧ a ≤ b
-- Mathlib.Data.Setoid.Partition
/-- The order-preserving bijection between equivalence relations on a type `α`, and
partitions of `α` into subsets.  -/
Setoid.Partition.orderIso : (α : Type u_1) → Setoid α ≃o Setoid.Partitions α
-- Mathlib.CategoryTheory.Dialectica.Basic
/-- The Dialectica category. An object of the category is a triple `⟨U, X, α ⊆ U × X⟩`,
and a morphism from `⟨U, X, α⟩` to `⟨V, Y, β⟩` is a pair `(f : U ⟶ V, F : U ⨯ Y ⟶ X)` such that
`{(u,y) | α(u, F(u, y))} ⊆ {(u,y) | β(f(u), y)}`. The subset `α` is actually encoded as an element
of `Subobject (U × X)`, and the above inequality is expressed using pullbacks.  -/
CategoryTheory.Dial : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Limits.HasFiniteProducts C] → Type (max u v)
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.latticeBasis_one : ∀ (L : PeriodPair), ↑(L.latticeBasis 1) = L.ω₂
-- Mathlib.LinearAlgebra.Eigenspace.Minpoly
/-- A variant of `Module.End.aeval_apply_of_hasEigenvector` which does not require `x ≠ 0`.  -/
Module.End.aeval_apply_of_mem_apply_eq_smul : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R} {x : M} {p : Polynomial R}, f x = μ • x → ((Polynomial.aeval f) p) x = Polynomial.eval μ p • x
-- Mathlib.Order.Filter.Basic
Filter.GenerateSets.below.univ : ∀ {α : Type u} {g : Set (Set α)} {motive : (a : Set α) → Filter.GenerateSets g a → Prop}, Filter.GenerateSets.below ⋯
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.ae_eq_top : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F}, MeasureTheory.ae μ = ⊤ ↔ ∀ (a : α), μ {a} ≠ 0
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pos.find?_char_eq_find?_beq : ∀ {c : Char} {s : String.Slice} {p : s.Pos}, p.find? c = p.find? fun x => x == c
-- Lean.Data.Iterators.Producers.PersistentHashMap
_private.Lean.Data.Iterators.Producers.PersistentHashMap.0.Lean.PersistentHashMap.Zipper.measure.eq_def : ∀ {α : Type u_1} {β : Type u_2} (x : Lean.PersistentHashMap.Zipper α β),
  x.measure =
    match x with
    | Lean.PersistentHashMap.Zipper.done => 0
    | Lean.PersistentHashMap.Zipper.consEntries es z' => Lean.PersistentHashMap.subarrayMeasure es + z'.measure + 1
    | Lean.PersistentHashMap.Zipper.consCollision keys vals a z' => Std.Slice.size vals + z'.measure + 1
-- Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
CategoryTheory.Limits.coconeFiberwiseColimitOfCocone_pt : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  {H : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} H]
  {G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H}
  [inst_2 :
    ∀ {X Y : C} (f : X ⟶ Y),
      CategoryTheory.Limits.HasColimit ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))]
  (c : CategoryTheory.Limits.Cocone G), (CategoryTheory.Limits.coconeFiberwiseColimitOfCocone c).pt = c.pt
-- Mathlib.GroupTheory.Perm.Centralizer
Equiv.Perm.Basis.mk : {α : Type u_1} →
  [inst : DecidableEq α] →
    [inst_1 : Fintype α] →
      {g : Equiv.Perm α} →
        (toFun : ↥g.cycleFactorsFinset → α) → (∀ (c : ↥g.cycleFactorsFinset), toFun c ∈ (↑c).support) → g.Basis
-- Mathlib.Topology.Order.UpperLowerSetTopology
/-- `ofUpperSet` is the identity function from the `WithUpperSet` of a type.  -/
Topology.WithUpperSet.ofUpperSet : {α : Type u_1} → Topology.WithUpperSet α ≃ α
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- A sum of a function over a `Finset` in a subtype equals a
sum in the main type of a function that agrees with the first
function on that `Finset`.  -/
Finset.sum_subtype_map_embedding : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] {p : ι → Prop} {s : Finset { x // p x }} {f : { x // p x } → M}
  {g : ι → M}, (∀ x ∈ s, g ↑x = f x) → ∑ x ∈ Finset.map (Function.Embedding.subtype fun x => p x) s, g x = ∑ x ∈ s, f x
-- Mathlib.Data.Sym.Sym2
Sym2.fromRel.congr_simp : ∀ {α : Type u_1} {r r_1 : α → α → Prop} (e_r : r = r_1) (sym : Std.Symm r) (a a_1 : Sym2 α),
  a = a_1 → Sym2.fromRel sym a = Sym2.fromRel ⋯ a_1
-- Batteries.Recycling.RBTree.Basic
/-- `O(log n)`. In-place replace an element found by `cut`.
This takes the element out of the tree while `f` runs,
so it uses the element linearly if `t` is unshared.

The `ModifyWF` assumption is required because `f` may change
the ordering properties of the element, which would break the invariants.
 -/
RBTree.RBSet.modifyP : {α : Type u_1} →
  {cmp : α → α → Ordering} →
    (t : RBTree.RBSet α cmp) → (cut : α → Ordering) → (f : α → α) → [wf : t.ModifyWF cut f] → RBTree.RBSet α cmp
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- If `F.cocones` is corepresented by `X`, the cocone corresponding to a morphism `f : Y ⟶ X` is
the colimit cocone extended by `f`.  -/
CategoryTheory.Limits.IsColimit.OfNatIso.coconeOfHom_fac : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {X : C} (h : F.cocones.CorepresentableBy X) {Y : C} (f : X ⟶ Y),
  CategoryTheory.Limits.IsColimit.OfNatIso.coconeOfHom h f =
    (CategoryTheory.Limits.IsColimit.OfNatIso.colimitCocone h).extend f
-- Std.Http.Data.Chunk
Std.Http.Chunk.instBEqExtensionName : BEq Std.Http.Chunk.ExtensionName
-- Init.Data.List.Lemmas
List.replace_append_left : ∀ {α : Type u_1} [inst : BEq α] {a b : α} [LawfulBEq α] {l₁ l₂ : List α},
  a ∈ l₁ → (l₁ ++ l₂).replace a b = l₁.replace a b ++ l₂
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.zero_le_restrict_subset : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddCommMonoid M]
  [inst_2 : PartialOrder M] (v : MeasureTheory.VectorMeasure α M) {i j : Set α},
  MeasurableSet i →
    j ⊆ i →
      MeasureTheory.VectorMeasure.restrict 0 i ≤ v.restrict i → MeasureTheory.VectorMeasure.restrict 0 j ≤ v.restrict j
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infiniteNeg_mul_of_infiniteNeg_not_infinitesimal_pos : ∀ {x y : ℝ*}, x.InfiniteNeg → ¬y.Infinitesimal → 0 < y → (x * y).InfiniteNeg
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.mono : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} {m' : MeasurableSpace α},
  m ≤ m' → MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.AEStronglyMeasurable f μ
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
Submodule.closure_eq' : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : Module R M] [inst_4 : ContinuousAdd M] [inst_5 : ContinuousConstSMul R M] {s : Submodule R M}
  (hs : IsClosed s.carrier), s.closure = { toSubmodule := s, isClosed' := hs }
-- Mathlib.Topology.Semicontinuity.Basic
lowerSemiContinuous_neg_iff : ∀ {α : Type u_4} [inst : TopologicalSpace α] {β : Type u_5} {f : α → β} [inst_1 : PartialOrder β]
  [inst_2 : AddCommGroup β] [IsOrderedAddMonoid β], LowerSemicontinuous (-f) ↔ UpperSemicontinuous f
-- Mathlib.Data.List.Permutation
List.perm_permutations'Aux_comm : ∀ {α : Type u_1} (a b : α) (l : List α),
  (List.flatMap (List.permutations'Aux b) (List.permutations'Aux a l)).Perm
    (List.flatMap (List.permutations'Aux a) (List.permutations'Aux b l))
-- Mathlib.RingTheory.Perfectoid.FontaineTheta
WittVector.fontaineThetaModPPow.eq_1 : ∀ (R : Type u) [inst : CommRing R] (p : ℕ) [inst_1 : Fact (Nat.Prime p)] [inst_2 : Fact ¬IsUnit ↑p] (n : ℕ),
  WittVector.fontaineThetaModPPow R p n =
    (WittVector.ghostComponentModPPow n).comp
      ((WittVector.map (PreTilt.coeff 0)).comp (WittVector.map (↑(frobeniusEquiv (PreTilt R p) p).symm ^ n)))
-- Mathlib.MeasureTheory.Integral.IntegrableOn
/-- **Alias** of `MeasureTheory.Measure.FiniteAtFilter.integrableAtFilter_of_tendsto`. -/
Filter.Tendsto.integrableAtFilter : ∀ {α : Type u_1} {E : Type u_5} {mα : MeasurableSpace α} [inst : NormedAddCommGroup E] {μ : MeasureTheory.Measure α}
  {f : α → E} {l : Filter α} [l.IsMeasurablyGenerated],
  StronglyMeasurableAtFilter f l μ →
    μ.FiniteAtFilter l → ∀ {b : E}, Filter.Tendsto f l (nhds b) → MeasureTheory.IntegrableAtFilter f l μ
-- Init.Data.Array.InsertIdx
Array.getElem?_insertIdx_self : ∀ {α : Type u} {xs : Array α} {x : α} {i : ℕ} (w : i ≤ xs.size), (xs.insertIdx i x w)[i]? = some x
-- Std.Async.Signal
Std.Async.Signal.sigint.sizeOf_spec : sizeOf Std.Async.Signal.sigint = 1
-- Mathlib.Analysis.Complex.CauchyIntegral
/-- **Cauchy integral formula** for the value at the center of a disc. If `f` is continuous on a
punctured closed disc of radius `R`, is differentiable at all but countably many points of the
interior of this disc, and has a limit `y` at the center of the disc, then the integral
$\oint_{‖z-c‖=R} \frac{f(z)}{z-c}\,dz$ is equal to `2πiy`.  -/
Complex.circleIntegral_sub_center_inv_smul_of_differentiable_on_off_countable_of_tendsto : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {c : ℂ} {R : ℝ},
  0 < R →
    ∀ {f : ℂ → E} {y : E} {s : Set ℂ},
      s.Countable →
        ContinuousOn f (Metric.closedBall c R \ {c}) →
          (∀ z ∈ (Metric.ball c R \ {c}) \ s, DifferentiableAt ℂ f z) →
            Filter.Tendsto f (nhdsWithin c {c}ᶜ) (nhds y) →
              ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z = (2 * ↑Real.pi * Complex.I) • y
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.linearGrowthSup_congr : ∀ {R : Type u_1} [inst : ConditionallyCompleteLattice R] [inst_1 : Div R] [inst_2 : NatCast R] {u v : ℕ → R},
  u =ᶠ[Filter.atTop] v → LinearGrowth.linearGrowthSup u = LinearGrowth.linearGrowthSup v
-- Mathlib.Geometry.Manifold.VectorField.Pullback
/-- The pullback of a vector field under a map between manifolds, within a set `s`. If the
derivative of the map within `s` is not invertible, then pullback is given the junk value zero.  -/
VectorField.mpullbackWithin : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {H : Type u_2} →
      [inst_1 : TopologicalSpace H] →
        {E : Type u_3} →
          [inst_2 : NormedAddCommGroup E] →
            [inst_3 : NormedSpace 𝕜 E] →
              (I : ModelWithCorners 𝕜 E H) →
                {M : Type u_4} →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] →
                      {H' : Type u_5} →
                        [inst_6 : TopologicalSpace H'] →
                          {E' : Type u_6} →
                            [inst_7 : NormedAddCommGroup E'] →
                              [inst_8 : NormedSpace 𝕜 E'] →
                                (I' : ModelWithCorners 𝕜 E' H') →
                                  {M' : Type u_7} →
                                    [inst_9 : TopologicalSpace M'] →
                                      [inst_10 : ChartedSpace H' M'] →
                                        (M → M') → ((x : M') → TangentSpace I' x) → Set M → (x : M) → TangentSpace I x
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.coe_add : ∀ {α : Type u_1} {_m : MeasurableSpace α} (μ₁ μ₂ : MeasureTheory.Measure α), ⇑(μ₁ + μ₂) = ⇑μ₁ + ⇑μ₂
-- Mathlib.Algebra.Group.Pi.Lemmas
Set.preimage_zero : ∀ {α : Type u_5} {β : Type u_6} [inst : Zero β] (s : Set β) [inst_1 : Decidable (0 ∈ s)],
  0 ⁻¹' s = if 0 ∈ s then Set.univ else ∅
-- Mathlib.Analysis.Normed.Module.Ball.Action
instSMulElemSphereOfNatRealClosedBall : {𝕜 : Type u_1} →
  {E : Type u_3} →
    [inst : NormedField 𝕜] →
      [inst_1 : SeminormedAddCommGroup E] →
        [NormedSpace 𝕜 E] → {r : ℝ} → SMul ↑(Metric.sphere 0 1) ↑(Metric.closedBall 0 r)
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncLT_obj_top : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C), t.eTruncLT.obj ⊤ = CategoryTheory.Functor.id C
-- Std.Data.DTreeMap.Internal.WF.Defs
Std.DTreeMap.Internal.Impl.eraseManyEntries.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {ρ : Type w} [inst_1 : ForIn Id ρ ((a : α) × β a)]
  (t : Std.DTreeMap.Internal.Impl α β) (l l_1 : ρ),
  l = l_1 → ∀ (h : t.Balanced), t.eraseManyEntries l h = t.eraseManyEntries l_1 h
-- Lean.ProjFns
Lean.instReprAuxParentProjectionInfo : Repr Lean.AuxParentProjectionInfo
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.Measure.completion.isComplete : ∀ {α : Type u_2} {_m : MeasurableSpace α} (μ : MeasureTheory.Measure α), μ.completion.IsComplete
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
/-- All `P_σ` are split epis as composition of such.  -/
SimplexCategoryGenRel.isSplitEpi_P_σ : ∀ {x y : SimplexCategoryGenRel} {e : x ⟶ y}, SimplexCategoryGenRel.P_σ e → CategoryTheory.IsSplitEpi e
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.L1.norm_eq_integral_norm : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {H : Type u_6} [inst : NormedAddCommGroup H]
  (f : ↥(MeasureTheory.Lp H 1 μ)), ‖f‖ = ∫ (a : α), ‖↑↑f a‖ ∂μ
-- Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived
CategoryTheory.Functor.isRightDerivedFunctor_iff_of_inverts : ∀ {C : Type u₁} {D : Type u₂} {H : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] [inst_2 : CategoryTheory.Category.{v₃, u₃} H]
  {L : CategoryTheory.Functor C D} {W : CategoryTheory.MorphismProperty C} [inst_3 : L.IsLocalization W]
  {F : CategoryTheory.Functor C H} (RF : CategoryTheory.Functor D H) (α : F ⟶ L.comp RF),
  W.IsInvertedBy F → (RF.IsRightDerivedFunctor α W ↔ CategoryTheory.IsIso α)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The codomain of a normalized 1-morphism.  -/
Mathlib.Tactic.BicategoryLike.NormalizedHom.tgt : Mathlib.Tactic.BicategoryLike.NormalizedHom → Mathlib.Tactic.BicategoryLike.Obj
-- Mathlib.Data.EReal.Basic
instPartialOrderEReal : PartialOrder EReal
-- Mathlib.LinearAlgebra.TensorProduct.Submodule
Submodule.lTensorOne'_one_tmul : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {N : Submodule R S}
  (n : ↥N), N.lTensorOne' (1 ⊗ₜ[R] n) = n
-- Init.Data.Order.Classes
Std.IsLinearPreorder.le_total : ∀ {α : Type u} {inst : LE α} [self : Std.IsLinearPreorder α] (a b : α), a ≤ b ∨ b ≤ a
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.binaryProductIso_inv_comp_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w)),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.FunctorToTypes.binaryProductIso F G).inv
      CategoryTheory.Limits.prod.fst =
    CategoryTheory.FunctorToTypes.prod.fst
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.toNonUnitalSubring_inj : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : NonUnitalRing A] [inst_2 : Module R A] [inst_3 : Star A]
  {S U : NonUnitalStarSubalgebra R A}, S.toNonUnitalSubring = U.toNonUnitalSubring ↔ S = U
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- Orthogonal projection onto the `Submodule.map` of a subspace.  -/
Submodule.starProjection_map_apply : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_4} {E' : Type u_5} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup E'] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 E'] (f : E ≃ₗᵢ[𝕜] E')
  (p : Submodule 𝕜 E) [inst_5 : p.HasOrthogonalProjection] (x : E'),
  (Submodule.map (↑f.toLinearEquiv) p).starProjection x = f (p.starProjection (f.symm x))
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Equivalence.instMonoidalInverseRefl : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → CategoryTheory.Equivalence.refl.inverse.Monoidal
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.ext_hom_hom : ∀ {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 c' : CategoryTheory.Limits.Cocone F} (φ : c.pt ≅ c'.pt)
  (w :
    autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp (c.ι.app j) φ.hom = c'.ι.app j)
      CategoryTheory.Limits.Cocone.ext._auto_1),
  (CategoryTheory.Limits.Cocone.ext φ w).hom.hom = φ.hom
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- If `T` and `T'` are terminal, they are isomorphic.  -/
CategoryTheory.Limits.IsTerminal.uniqueUpToIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T T' : C} → CategoryTheory.Limits.IsTerminal T → CategoryTheory.Limits.IsTerminal T' → (T ≅ T')
-- Init.Data.SInt.Lemmas
UInt32.toBitVec_toInt32 : ∀ (x : UInt32), x.toInt32.toBitVec = x.toBitVec
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape
CategoryTheory.TransfiniteCompositionOfShape.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : Type w) [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  {X Y : C} (f f_1 : X ⟶ Y),
  f = f_1 →
    ∀ [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J],
      CategoryTheory.TransfiniteCompositionOfShape J f = CategoryTheory.TransfiniteCompositionOfShape J f_1
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
/-- The ring norm underlying a multiplicative ring norm.  -/
MulRingNorm.toRingNorm : {R : Type u_1} → [inst : NonAssocRing R] → MulRingNorm R → RingNorm R
-- Mathlib.Tactic.CongrExclamation
/-- Tries to apply `lawful_beq_subsingleton` to prove that two `BEq` instances are equal
by synthesizing `LawfulBEq` instances for both.
 -/
Lean.MVarId.beqInst? : Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))
-- Mathlib.Topology.Algebra.Group.Basic
/-- The topological group isomorphism between the additive units of a product of two
additive monoids, and the product of the additive units of each additive monoid.  -/
Homeomorph.prodAddUnits : {α : Type u} →
  {β : Type v} →
    [inst : AddMonoid α] →
      [inst_1 : TopologicalSpace α] →
        [inst_2 : AddMonoid β] → [inst_3 : TopologicalSpace β] → AddUnits (α × β) ≃ₜ AddUnits α × AddUnits β
-- Mathlib.Probability.Process.FiniteDimensionalLaws
/-- If two processes are modifications of each other, then they have the same finite-dimensional
distributions.  -/
ProbabilityTheory.map_restrict_eq_of_forall_ae_eq : ∀ {T : Type u_1} {Ω : Type u_2} {𝓧 : T → Type u_3} {mΩ : MeasurableSpace Ω} {mα : (t : T) → MeasurableSpace (𝓧 t)}
  {X Y : (t : T) → Ω → 𝓧 t} {P : MeasureTheory.Measure Ω},
  (∀ (t : T), X t =ᵐ[P] Y t) →
    ∀ (I : Finset T),
      MeasureTheory.Measure.map (fun ω => I.restrict fun x => X x ω) P =
        MeasureTheory.Measure.map (fun ω => I.restrict fun x => Y x ω) P
-- Mathlib.Topology.Algebra.Support
hasCompactSupport_comp_left : ∀ {α : Type u_2} {β : Type u_4} {γ : Type u_5} [inst : TopologicalSpace α] [inst_1 : Zero β] [inst_2 : Zero γ]
  {g : β → γ} {f : α → β}, (∀ {x : β}, g x = 0 ↔ x = 0) → (HasCompactSupport (g ∘ f) ↔ HasCompactSupport f)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.size_le_size_insert : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} {v : β k}, m.size ≤ (m.insert k v).size
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Op
SSet.Subcomplex.Pairing.op_I : ∀ {X : SSet} {A : X.Subcomplex} (P : A.Pairing), P.op.I = ⇑SSet.Subcomplex.N.opEquiv ⁻¹' P.I
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
/-- A subgroupoid seen as a quiver on vertex set `C`  -/
CategoryTheory.Subgroupoid.asWideQuiver : {C : Type u} → [inst : CategoryTheory.Groupoid C] → CategoryTheory.Subgroupoid C → Quiver C
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
/-- Variant of `mul_lt_of_lt_one_left` for `b` negative instead of positive.  -/
lt_mul_of_lt_one_left : ∀ {R : Type u} [inst : Semiring R] [inst_1 : PartialOrder R] {a b : R} [ExistsAddOfLE R] [MulPosStrictMono R]
  [AddRightStrictMono R] [AddRightReflectLT R], b < 0 → a < 1 → b < a * b
-- Init.Data.Format.Basic
Std.Format.nest.sizeOf_spec : ∀ (indent : ℤ) (f : Std.Format), sizeOf (Std.Format.nest indent f) = 1 + sizeOf indent + sizeOf f
-- Mathlib.Logic.Equiv.Bool
Bool.not_hasRightInverse : Function.HasRightInverse not
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.opcyclesIsoCokernel_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasRightHomology] [inst_3 : CategoryTheory.Limits.HasCokernel S.f],
  S.opcyclesIsoCokernel.hom = S.descOpcycles (CategoryTheory.Limits.cokernel.π S.f) ⋯
-- Mathlib.Algebra.Category.BialgCat.Basic
BialgCat.hasForgetToAlgebra : {R : Type u} → [inst : CommRing R] → CategoryTheory.HasForget₂ (BialgCat R) (AlgCat R)
-- Mathlib.Algebra.Lie.TensorProduct
TensorProduct.LieModule.hasBracketAux.eq_1 : ∀ {R : Type u} [inst : CommRing R] {L : Type v} {M : Type w} {N : Type w₁} [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 : AddCommGroup N] [inst_8 : Module R N] [inst_9 : LieRingModule L N]
  [inst_10 : LieModule R L N] (x : L),
  TensorProduct.LieModule.hasBracketAux x =
    LinearMap.rTensor N ((LieModule.toEnd R L M) x) + LinearMap.lTensor M ((LieModule.toEnd R L N) x)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get?_diff_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∈ m₂ → Std.ExtDHashMap.Const.get? (m₁ \ m₂) k = none
-- Init.Data.SInt.Lemmas
ISize.neg_inj : ∀ {a b : ISize}, -a = -b ↔ a = b
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
/-- Thanks to `tensorUnit` being initial in `AugmentedSimplexCategory`, we get
a morphism `Δ ⟶ Δ ⊗ Δ'` for every pair of objects `Δ, Δ'`.  -/
AugmentedSimplexCategory.inl : (x y : AugmentedSimplexCategory) → x ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj x y
-- Mathlib.Data.Finmap
Multiset.coe_keys : ∀ {α : Type u} {β : α → Type v} {l : List (Sigma β)}, (↑l).keys = ↑l.keys