mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.homMk_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} {F G : CategoryTheory.ComposableArrows C n}
  (app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i)
  (w :
    ∀ (i : ℕ) (hi : i < n),
      CategoryTheory.CategoryStruct.comp (F.map' i (i + 1) ⋯ hi) (app ⟨i + 1, ⋯⟩) =
        CategoryTheory.CategoryStruct.comp (app ⟨i, ⋯⟩) (G.map' i (i + 1) ⋯ hi))
  (i : Fin (n + 1)), (CategoryTheory.ComposableArrows.homMk app w).app i = app i
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `1` and `*` is a right cancel monoid, if it admits an injective map that
preserves `1` and `*` to a right cancel monoid. See note [reducible non-instances].  -/
Function.Injective.rightCancelMonoid : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Mul M₁] →
      [inst_1 : One M₁] →
        [inst_2 : Pow M₁ ℕ] →
          [inst_3 : RightCancelMonoid M₂] →
            (f : M₁ → M₂) →
              Function.Injective f →
                f 1 = 1 →
                  (∀ (x y : M₁), f (x * y) = f x * f y) →
                    (∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) → RightCancelMonoid M₁
-- Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent
/-- The ideal sheaf data associated to an irreducible component of a Noetherian scheme.  -/
AlgebraicGeometry.Scheme.irreducibleComponentIdeal : (X : AlgebraicGeometry.Scheme) →
  (Z : Set ↥X) → Z ∈ irreducibleComponents ↥X → [AlgebraicGeometry.IsNoetherian X] → X.IdealSheafData
-- Mathlib.AlgebraicGeometry.Restrict
/-- If `U ≤ V`, then `U` is also a subscheme of `V`.  -/
AlgebraicGeometry.Scheme.homOfLE : (X : AlgebraicGeometry.Scheme) → {U V : X.Opens} → U ≤ V → (↑U ⟶ ↑V)
-- Init.Data.Order.Ord
Std.TransCmp.eq_trans : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {a b c : α},
  cmp a b = Ordering.eq → cmp b c = Ordering.eq → cmp a c = Ordering.eq
-- Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
/-- A limit can be realised as a subobject of a product.  -/
CategoryTheory.Limits.limitSubobjectProduct : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.SmallCategory J] →
        [inst_2 : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v, u} C] →
          (F : CategoryTheory.Functor J C) → CategoryTheory.Limits.limit F ⟶ ∏ᶜ fun j => F.obj j
-- Std.Tactic.Do.Syntax
/-- In induction alternative, which can have 1 or more cases on the left
and `_`, `?_`, or a tactic sequence after the `=>`.
 -/
Lean.Parser.Tactic.vcAlt : Lean.ParserDescr
-- Mathlib.Topology.OpenPartialHomeomorph.Continuity
/-- An open partial homeomorphism is continuous at any point of its source  -/
OpenPartialHomeomorph.continuousAt : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {x : X}, x ∈ e.source → ContinuousAt (↑e) x
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.instAddMonoidOfContinuousAdd : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : AddMonoid β] → [ContinuousAdd β] → AddMonoid (CompactlySupportedContinuousMap α β)
-- Mathlib.Order.RelClasses
/-- A version of `Std.le_refl` that works with `Std.Refl (· ≥ ·)`.
This is needed for `to_dual` translations because `Std.le_refl` requires `Std.Refl (· ≤ ·)`,
but after translation `instReflLe` becomes `instReflGe : Std.Refl (· ≥ ·)`.  -/
Std.ge_refl : ∀ {α : Type u_1} [inst : LE α] [inst_1 : Std.Refl fun x1 x2 => x1 ≥ x2] (a : α), a ≤ a
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.map_add : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x y : E), e (x + y) = e x + e y
-- Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
/-- If `S : K → J` is a family of objects of cardinality `< κ` in a `κ`-filtered category,
this is a choice of objects in `J` which is the target of a map from any of
the objects `S k`.  -/
CategoryTheory.IsCardinalFiltered.max : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {κ : Cardinal.{w}} →
      [hκ : Fact κ.IsRegular] →
        [CategoryTheory.IsCardinalFiltered J κ] → {K : Type u'} → (K → J) → HasCardinalLT K κ → J
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.map_mul : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Add M] (f : R →+* S)
  (x y : AddMonoidAlgebra R M),
  AddMonoidAlgebra.map (↑f) (x * y) = AddMonoidAlgebra.map (↑f) x * AddMonoidAlgebra.map (↑f) y
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.any_eq_true_iff_exists_mem_getElem : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α]
  {p : α → β → Bool}, m.WF → (m.any p = true ↔ ∃ a, ∃ (h : a ∈ m), p a m[a] = true)
-- Mathlib.RingTheory.HahnSeries.Multiplication
/-- Extending the domain of Hahn series is a ring homomorphism.  -/
HahnSeries.embDomainRingHom : {Γ : Type u_1} →
  {R : Type u_3} →
    [inst : AddCommMonoid Γ] →
      [inst_1 : PartialOrder Γ] →
        [inst_2 : IsOrderedCancelAddMonoid Γ] →
          {Γ' : Type u_6} →
            [inst_3 : AddCommMonoid Γ'] →
              [inst_4 : PartialOrder Γ'] →
                [inst_5 : IsOrderedCancelAddMonoid Γ'] →
                  [inst_6 : NonAssocSemiring R] →
                    (f : Γ →+ Γ') →
                      Function.Injective ⇑f → (∀ (g g' : Γ), f g ≤ f g' ↔ g ≤ g') → HahnSeries Γ R →+* HahnSeries Γ' R
-- Mathlib.Data.Set.Image
Set.inclusion.congr_simp : ∀ {α : Type u_1} {s t : Set α} (h : s ⊆ t) (a a_1 : ↑s), a = a_1 → Set.inclusion h a = Set.inclusion h a_1
-- Lean.Meta.Tactic.Grind.EMatch
/-- Helper function for E-match theorems containing universe metavariables that do not occur
in any of their parameters. This is a very rare case, but it does occur in practice.
Example:
```lean
@[simp, grind =] theorem down_pure {φ : Prop} : (⌜φ⌝ : SPred []).down = φ := rfl
```

The parameter `us` contains the unassigned universe metavariables.

Recall that when we collect patterns for a theorem, we check coverage only for regular
parameters, not universe parameters. This function attempts to instantiate the universe
parameters using the following heuristic:

* Collect all constants `C` in `prop` that contain universe metavariables.
* Create a collection `P` of pairs `(c, cs)` where `c ∈ C` and `cs` are instances of `c` in the current goal.
* Sort `P` by the size of `cs`, prioritizing constants with fewer occurrences.
* Perform a backtracking search to unify each `c` with its occurrences. Stop as soon as all universe parameters are instantiated.

We expect this function not to be a performance bottleneck in practice because:

1. Very few theorems contain universe metavariables not covered by any parameters.
2. These theorems usually involve only a small number of universe levels and universe polymorphic constants.
3. Goals rarely contain constants instantiated with many different universe variables.

If this does become a performance issue, we will need to add support for assigning universe levels
during E-matching and check for universe-level coverage when collecting patterns.

The result is a collection of pairs `(proof', prop')` where `proof'` and `prop'` are `proof` and `prop`
with all universe metavariables instantiated.
 -/
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.assignUnassignedLevelMVars : Array Lean.LMVarId → Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM (Array (Lean.Expr × Lean.Expr))
-- Mathlib.Algebra.Order.Floor.Ring
Int.fract_mul_natCast : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (a : R) (b : ℕ),
  ∃ z, Int.fract a * ↑b - Int.fract (a * ↑b) = ↑z
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.InjectiveInfo.mk : List Lean.Level → Lean.Expr → Lean.Expr → Lean.Expr → Option (Lean.Expr × Lean.Expr) → Lean.Meta.Grind.InjectiveInfo
-- Mathlib.CategoryTheory.Category.Cat.Limit
/-- Auxiliary definition: the universal morphism to the proposed limit cone.  -/
CategoryTheory.Cat.HasLimits.limitConeLift : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J CategoryTheory.Cat) →
      (s : CategoryTheory.Limits.Cone F) → s.pt ⟶ CategoryTheory.Cat.HasLimits.limitConeX F
-- Mathlib.RingTheory.Ideal.Quotient.Operations
DoubleQuot.quotLeftToQuotSup.eq_1 : ∀ {R : Type u} [inst : CommRing R] (I J : Ideal R), DoubleQuot.quotLeftToQuotSup I J = Ideal.Quotient.factor ⋯
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
/-- `ofFunction` of a set `s` is the infimum of `∑ᵢ, m (tᵢ)` for all collections of sets
`tᵢ` that cover `s`.  -/
MeasureTheory.OuterMeasure.ofFunction_apply : ∀ {α : Type u_1} (m : Set α → ENNReal) (m_empty : m ∅ = 0) (s : Set α),
  (MeasureTheory.OuterMeasure.ofFunction m m_empty) s = ⨅ t, ⨅ (_ : s ⊆ Set.iUnion t), ∑' (n : ℕ), m (t n)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.self_le_maxKeyD_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β} {fallback : α}, (cmp k ((t.insert k v).maxKeyD fallback)).isLE = true
-- Mathlib.GroupTheory.Coxeter.Matrix
CoxeterMatrix.mk : {B : Type u_1} →
  (M : Matrix B B ℕ) →
    autoParam M.IsSymm CoxeterMatrix.isSymm._autoParam →
      autoParam (∀ (i : B), M i i = 1) CoxeterMatrix.diagonal._autoParam →
        autoParam (∀ (i i' : B), i ≠ i' → M i i' ≠ 1) CoxeterMatrix.off_diagonal._autoParam → CoxeterMatrix B
-- Mathlib.Algebra.GroupWithZero.Units.Basic
eq_zero_of_zpow_eq_zero : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀} {n : ℤ}, a ^ n = 0 → a = 0
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.NatIso.ofComponents'.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (app app_1 : (X : C) → F.obj X ≅ G.obj X) (e_app : app = app_1)
  (naturality :
    ∀ {X Y : C} (f : Y ⟶ X),
      CategoryTheory.CategoryStruct.comp (app Y).inv (F.map f) =
        CategoryTheory.CategoryStruct.comp (G.map f) (app X).inv),
  CategoryTheory.NatIso.ofComponents' app naturality = CategoryTheory.NatIso.ofComponents' app_1 ⋯
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- A subgroup of a group inherits an integer power.  -/
SubgroupClass.instZPow : {M : Type u_5} →
  {S : Type u_6} → [inst : DivInvMonoid M] → [inst_1 : SetLike S M] → [SubgroupClass S M] → {H : S} → Pow ↥H ℤ
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
/-- The action on objects of the `EnrichedCategory Cat` coherences proves the category axioms.  -/
CategoryTheory.CatEnriched.instCategory : {C : Type u_1} →
  [CategoryTheory.EnrichedCategory CategoryTheory.Cat C] →
    CategoryTheory.Category.{u_2, u_1} (CategoryTheory.CatEnriched C)
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.gaussianReal_map_neg : ∀ {μ : ℝ} {v : NNReal},
  MeasureTheory.Measure.map (fun x => -x) (ProbabilityTheory.gaussianReal μ v) = ProbabilityTheory.gaussianReal (-μ) v
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop.0.Std.IterM.first?.eq_1 : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α m β] [inst_2 : Std.IteratorLoop α m m]
  (it : Std.IterM m β),
  it.first? =
    Std.IteratorLoop.forIn (fun x x_1 => flip bind) (Option β) (fun b x s => s = ForInStep.done (some b)) it none
      fun b x x_1 => pure ⟨ForInStep.done (some b), ⋯⟩
-- Mathlib.Logic.Basic
Classical.some_spec₂ : ∀ {α : Sort u_2} {p : α → Prop} {h : ∃ a, p a} (q : α → Prop), (∀ (a : α), p a → q a) → q (Classical.choose h)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
/-- If `f` and `g` are two functions that are interval integrable on `a..b`, `a ≤ b`,
`f x ≤ g x` for a.e. `x ∈ Set.Ioc a b`, and `f x < g x` on a subset of `Set.Ioc a b`
of nonzero measure, then `∫ x in a..b, f x ∂μ < ∫ x in a..b, g x ∂μ`.  -/
intervalIntegral.integral_lt_integral_of_ae_le_of_measure_setOfPred_lt_ne_zero : ∀ {f g : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ},
  a ≤ b →
    IntervalIntegrable f μ a b →
      IntervalIntegrable g μ a b →
        f ≤ᵐ[μ.restrict (Set.Ioc a b)] g →
          (μ.restrict (Set.Ioc a b)) {x | f x < g x} ≠ 0 → ∫ (x : ℝ) in a..b, f x ∂μ < ∫ (x : ℝ) in a..b, g x ∂μ
-- Mathlib.Tactic.Linter.Style
/-- Whether a given piece of syntax is a `set_option` command, tactic or term.  -/
Mathlib.Linter.Style.setOption.isSetOption : Lean.Syntax → Bool
-- Mathlib.RingTheory.PowerSeries.Trunc
PowerSeries.coeff_mul_eq_coeff_trunc_mul_trunc : ∀ {R : Type u_2} [inst : CommSemiring R] {d n : ℕ} (f g : PowerSeries R),
  d < n →
    (PowerSeries.coeff d) (f * g) = (PowerSeries.coeff d) (↑((PowerSeries.trunc n) f) * ↑((PowerSeries.trunc n) g))
-- Mathlib.Lean.Meta.CongrTheorems
/-- Given a type that is a bunch of equalities implying a goal (for example, a basic
congruence lemma), prove it if possible. Basic congruence lemmas should be provable by this.
There are some extra tricks for handling arguments to richer congruence lemmas.  -/
_private.Mathlib.Lean.Meta.CongrTheorems.0.Lean.Meta.mkRichHCongr.trySolveCore : Lean.MVarId → Lean.MetaM Unit
-- Init.Grind.Ordered.Field
_private.Init.Grind.Ordered.Field.0.Lean.Grind.Field.IsOrdered.mul_inv_lt_of_mul_lt : ∀ {R : Type u} [inst : Lean.Grind.Field R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsLinearOrder R] [Lean.Grind.OrderedRing R] {a b c : R}, b < 0 → a * b < c → c * b⁻¹ < a
-- Mathlib.Data.Nat.Factorization.Defs
/-- The support of `n.factorization` is exactly `n.primeFactors`.  -/
Nat.support_factorization : ∀ (n : ℕ), n.factorization.support = n.primeFactors
-- Mathlib.Topology.Homotopy.Path
Path.Homotopy.eval_apply : ∀ {X : Type u} [inst : TopologicalSpace X] {x₀ x₁ : X} {p₀ p₁ : Path x₀ x₁} (F : p₀.Homotopy p₁) (t a : ↑unitInterval),
  (F.eval t) a = (F.curry t) a
-- Lean.Environment
_private.Lean.Environment.0.Lean.EnvExtension.modifyState.unsafe_impl_5 : {σ : Type} → Lean.EnvExtension σ → Lean.Environment → (σ → σ) → Array Lean.EnvExtensionState
-- Init.Data.String.Basic
String.Pos.offset_sliceTo : ∀ {s : String} {p₀ pos : s.Pos} {h : pos ≤ p₀}, (p₀.sliceTo pos h).offset = pos.offset
-- Mathlib.Data.Finset.Sum
Finset.card_toRight_le : ∀ {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)}, u.toRight.card ≤ u.card
-- Mathlib.Algebra.Notation.Indicator
Set.indicator_univ : ∀ {α : Type u_1} {M : Type u_3} [inst : Zero M] (f : α → M), Set.univ.indicator f = f
-- Mathlib.Algebra.GroupWithZero.Associated
/-- Two elements of a `Monoid` are `Associated` if one of them is another one
multiplied by a unit on the right.  -/
Associated : {M : Type u_1} → [Monoid M] → M → M → Prop
-- Mathlib.Data.List.Cycle
_private.Mathlib.Data.List.Cycle.0.Cycle.decidableNontrivialCoe.match_1.splitter : {α : Type u_1} →
  (motive : List α → Sort u_2) →
    (x : List α) →
      (Unit → motive []) → ((x : α) → motive [x]) → ((x y : α) → (l : List α) → motive (x :: y :: l)) → motive x
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.codExtend_target : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace Z] {s : Set B} (hs : IsOpen s) (nonempty : s.Nonempty) {proj : Z → ↑s}
  (e : Bundle.Trivialization F proj),
  (Bundle.Trivialization.codExtend hs nonempty e).target = Prod.map Subtype.val id '' e.toPretrivialization.target
-- Mathlib.RingTheory.ZMod.UnitsCyclic
ZMod.exists_one_add_mul_pow_prime_eq : ∀ {R : Type u_1} [inst : CommSemiring R] {u v : R} {p : ℕ},
  Nat.Prime p → v ∣ u → ↑p * u * v ∣ u ^ p → ∀ (x : R), ∃ y, (1 + u * x) ^ p = 1 + ↑p * u * (x + v * y)
-- Lean.Meta.Basic
/-- `whnf` with instances transparency. -/
Lean.Meta.whnfI : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral
/-- The continuous functional calculus commutes with integration.
This version assumes joint continuity of `f`, see `cfcₙ_integral'` for a statement
with weaker assumptions.  -/
cfcₙ_integral : ∀ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : MeasurableSpace X]
  {μ : MeasureTheory.Measure X} [inst_2 : NonUnitalNormedRing A] [inst_3 : StarRing A] [inst_4 : NormedSpace 𝕜 A]
  [inst_5 : IsScalarTower 𝕜 A A] [inst_6 : SMulCommClass 𝕜 A A] [inst_7 : NonUnitalContinuousFunctionalCalculus 𝕜 A p]
  [CompleteSpace A] [inst_9 : NormedSpace ℝ A] [inst_10 : TopologicalSpace X] [OpensMeasurableSpace X] (f : X → 𝕜 → 𝕜)
  (bound : X → ℝ) (a : A) [SecondCountableTopologyEither X C(↑(quasispectrum 𝕜 a), 𝕜)],
  ContinuousOn (Function.uncurry f) (Set.univ ×ˢ quasispectrum 𝕜 a) →
    (∀ᵐ (x : X) ∂μ, f x 0 = 0) →
      (∀ᵐ (x : X) ∂μ, ∀ z ∈ quasispectrum 𝕜 a, ‖f x z‖ ≤ bound x) →
        MeasureTheory.HasFiniteIntegral bound μ →
          autoParam (p a) cfcₙ_integral._auto_1 → cfcₙ (fun r => ∫ (x : X), f x r ∂μ) a = ∫ (x : X), cfcₙ (f x) a ∂μ
-- Mathlib.Analysis.InnerProductSpace.PiL2
DirectSum.IsInternal.collectedOrthonormalBasis.congr_simp : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] {A : ι → Submodule 𝕜 E}
  (hV : OrthogonalFamily 𝕜 (fun i => ↥(A i)) fun i => (A i).subtypeₗᵢ) [inst_4 : DecidableEq ι]
  (hV_sum : DirectSum.IsInternal fun i => A i) {α : ι → Type u_7} [inst_5 : (i : ι) → Fintype (α i)]
  (v_family v_family_1 : (i : ι) → OrthonormalBasis (α i) 𝕜 ↥(A i)),
  v_family = v_family_1 →
    DirectSum.IsInternal.collectedOrthonormalBasis hV hV_sum v_family =
      DirectSum.IsInternal.collectedOrthonormalBasis hV hV_sum v_family_1
-- Mathlib.Combinatorics.SimpleGraph.Metric
/-- This bundles and abstracts some facts about the first three vertices of a shortest walk
of length at least two: the first and third nodes are different and not connected.  -/
SimpleGraph.Walk.exists_adj_adj_not_adj_ne : ∀ {V : Type u_1} {G : SimpleGraph V} {v w : V} {p : G.Walk v w},
  p.length = G.dist v w → 1 < G.dist v w → ∃ x a b, G.Adj x a ∧ G.Adj a b ∧ ¬G.Adj x b ∧ x ≠ b
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get!_erase_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited β] {k : α}, Std.DHashMap.Const.get! (m.erase k) k = default
-- Mathlib.Data.Fin.Basic
Fin.val_add_one_of_lt' : ∀ {n : ℕ} {i : Fin n}, ↑i + 1 < n → ↑(i + 1) = ↑i + 1
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsCoverDense.Types.naturality : ∀ {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] {K : CategoryTheory.GrothendieckTopology D}
  {G : CategoryTheory.Functor C D} {ℱ : CategoryTheory.Functor Dᵒᵖ (Type v)} {ℱ' : CategoryTheory.Sheaf K (Type v)}
  (α : G.op.comp ℱ ⟶ G.op.comp ℱ'.obj) [G.IsLocallyFull K] {X Y : C} (i : G.obj X ⟶ G.obj Y),
  CategoryTheory.CategoryStruct.comp (α.app (Opposite.op Y)) (ℱ'.obj.map i.op) =
    CategoryTheory.CategoryStruct.comp (ℱ.map i.op) (α.app (Opposite.op X))
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.p_g'_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData) {Z : C} (h_1 : S.X₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp h.p (CategoryTheory.CategoryStruct.comp h.g' h_1) =
    CategoryTheory.CategoryStruct.comp S.g h_1
-- Mathlib.Algebra.Homology.Augment
CochainComplex.truncateAugment_inv_f : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (C : CochainComplex V ℕ) {X : V} (f : X ⟶ C.X 0) (w : CategoryTheory.CategoryStruct.comp f (C.d 0 1) = 0) (i : ℕ),
  (C.truncateAugment f w).inv.f i = CategoryTheory.CategoryStruct.id ((CochainComplex.truncate.obj (C.augment f w)).X i)
-- Lean.Meta.Match.MatcherApp.Transform
/-- `Match.forallAltTelescope` lifted to a monad transformer
(and only passing those arguments that we care about below)
 -/
_private.Lean.Meta.Match.MatcherApp.Transform.0.Lean.Meta.MatcherApp.forallAltTelescope' : {n : Type → Type u_1} →
  [Monad n] →
    [MonadControlT Lean.MetaM n] →
      {α : Type} → Lean.Expr → Lean.Meta.Match.AltParamInfo → (Array Lean.Expr → Array Lean.Expr → n α) → n α
-- Mathlib.LinearAlgebra.RootSystem.Base
/-- Interchanging roots and coroots, one still has a base of a root pairing.  -/
RootPairing.Base.flip : {ι : 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} → P.Base → P.flip.Base
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.LaxBraidedFunctor.forget_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.MonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  {X Y :
    CategoryTheory.InducedCategory (CategoryTheory.LaxMonoidalFunctor C D)
      CategoryTheory.LaxBraidedFunctor.toLaxMonoidalFunctor}
  (f : X ⟶ Y), CategoryTheory.LaxBraidedFunctor.forget.map f = f.hom
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Feature.phase.sizeOf_spec : ∀ (p : Aesop.PhaseName), sizeOf (Aesop.Frontend.Feature.phase p) = 1 + sizeOf p
-- Mathlib.Analysis.InnerProductSpace.PiL2
finrank_euclideanSpace : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] [inst_1 : Fintype ι],
  Module.finrank 𝕜 (EuclideanSpace 𝕜 ι) = Fintype.card ι
-- Mathlib.Topology.Category.UniformSpace
UniformSpaceCat.extension_comp_hom : ∀ {X : UniformSpaceCat} {Y : CpltSepUniformSpace}
  (f : (CpltSepUniformSpace.of (UniformSpace.Completion X.carrier)).toUniformSpace ⟶ Y.toUniformSpace),
  (UniformSpaceCat.extensionHom (CategoryTheory.CategoryStruct.comp X.completionHom f)).hom = f
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
/-- The left homotopy that is deduced from a right homotopy in the opposite category.  -/
HomotopicalAlgebra.PrepathObject.RightHomotopy.unop : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : Cᵒᵖ} →
      {P : HomotopicalAlgebra.PrepathObject Y} → {f g : X ⟶ Y} → P.RightHomotopy f g → P.unop.LeftHomotopy f.unop g.unop
-- Init.Data.String.Lemmas.Order
String.Pos.sliceTo_le_iff : ∀ {s : String} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} {h : q ≤ p₀},
  p₀.sliceTo q h ≤ p ↔ q ≤ String.Pos.ofSliceTo p
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.indepFun_finset₀ : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : ι → Type u_8}
  {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ω → β i} (S T : Finset ι),
  Disjoint S T →
    ProbabilityTheory.Kernel.iIndepFun f κ μ →
      (∀ (i : ι), AEMeasurable (f i) (μ.bind ⇑κ)) →
        ProbabilityTheory.Kernel.IndepFun (fun a i => f (↑i) a) (fun a i => f (↑i) a) κ μ
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.neighborSet_sup : ∀ {V : Type u} {G : SimpleGraph V} {H H' : G.Subgraph} (v : V),
  (H ⊔ H').neighborSet v = H.neighborSet v ∪ H'.neighborSet v
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
/-- Any linearly ordered group with zero is isomorphic to adjoining `0` to the units of itself.  -/
OrderMonoidIso.withZeroUnits : {α : Type u_6} → [inst : LinearOrderedCommGroupWithZero α] → [DecidablePred fun a => a = 0] → WithZero αˣ ≃*o α