mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Match.MatchEqsExt
Lean.Meta.Match.MatchEqns.mk.sizeOf_spec : ∀ (eqnNames : Array Lean.Name) (splitterName : Lean.Name) (splitterMatchInfo : Lean.Meta.MatcherInfo),
  sizeOf { eqnNames := eqnNames, splitterName := splitterName, splitterMatchInfo := splitterMatchInfo } =
    1 + sizeOf eqnNames + sizeOf splitterName + sizeOf splitterMatchInfo
-- Mathlib.Computability.PartrecBasis
Nat.Partrec'.of_part : ∀ {n : ℕ} {f : List.Vector ℕ n →. ℕ}, Partrec f → Nat.Partrec' f
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
/-- `condExpL2` verifies the equality of integrals defining the conditional expectation.  -/
MeasureTheory.integral_condExpL2_eq : ∀ {α : Type u_1} {E' : Type u_3} {𝕜 : Type u_7} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E']
  [inst_2 : InnerProductSpace 𝕜 E'] [inst_3 : CompleteSpace E'] [inst_4 : NormedSpace ℝ E'] {m m0 : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {s : Set α} (hm : m ≤ m0) (f : ↥(MeasureTheory.Lp E' 2 μ)),
  MeasurableSet s → μ s ≠ ⊤ → ∫ (x : α) in s, ↑↑↑((MeasureTheory.condExpL2 E' 𝕜 hm) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.iIndep : ∀ {Ω : Type u_1} {ι : Type u_2} {κ : ι → Type u_5} {x : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  {m : (i : ι) → MeasurableSpace (κ i)} {f : (x : ι) → Ω → κ x},
  ProbabilityTheory.iIndepFun f μ → ProbabilityTheory.iIndep (fun x => MeasurableSpace.comap (f x) (m x)) μ
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- The image of zero is zero.  -/
NonarchAddGroupSeminormClass.map_zero : ∀ {F : Type u_6} {α : outParam (Type u_7)} {inst : AddGroup α} {inst_1 : FunLike F α ℝ}
  [self : NonarchAddGroupSeminormClass F α] (f : F), f 0 = 0
-- Mathlib.Data.Finmap
Finmap.induction_on₃ : ∀ {α : Type u} {β : α → Type v} {C : Finmap β → Finmap β → Finmap β → Prop} (s₁ s₂ s₃ : Finmap β),
  (∀ (a₁ a₂ a₃ : AList β), C a₁.toFinmap a₂.toFinmap a₃.toFinmap) → C s₁ s₂ s₃
-- Lean.Compiler.IR.Basic
Lean.IR.instInhabitedLitVal.default : Lean.IR.LitVal
-- Mathlib.CategoryTheory.Category.Factorisation
/-- The unique morphism out of `Factorisation.initial f`.  -/
CategoryTheory.Factorisation.initialHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → {f : X ⟶ Y} → (d : CategoryTheory.Factorisation f) → CategoryTheory.Factorisation.initial.Hom d
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
/-- Two groups of the same prime cardinality are isomorphic.  -/
mulEquivOfPrimeCardEq : {G : Type u_2} →
  {G' : Type u_3} →
    {p : ℕ} → [inst : Group G] → [inst_1 : Group G'] → [Fact (Nat.Prime p)] → Nat.card G = p → Nat.card G' = p → G ≃* G'
-- Lean.Parser.Types
Lean.Parser.TokenCacheEntry.token : Lean.Parser.TokenCacheEntry → Lean.Syntax
-- Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Mathlib.Tactic.Monoidal.evalWhiskerRight_cons_of : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {f f' g h i : C}
  {α : f' ≅ g} {η : g ⟶ h} {ηs : h ⟶ i}
  {ηs₁ : CategoryTheory.MonoidalCategoryStruct.tensorObj h f ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj i f}
  {η₁ : CategoryTheory.MonoidalCategoryStruct.tensorObj g f ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj h f}
  {η₂ : CategoryTheory.MonoidalCategoryStruct.tensorObj g f ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj i f}
  {η₃ : CategoryTheory.MonoidalCategoryStruct.tensorObj f' f ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj i f},
  CategoryTheory.MonoidalCategoryStruct.whiskerRight ηs f = ηs₁ →
    CategoryTheory.MonoidalCategoryStruct.whiskerRight η f = η₁ →
      CategoryTheory.CategoryStruct.comp η₁ ηs₁ = η₂ →
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRightIso α f).hom η₂ = η₃ →
          CategoryTheory.MonoidalCategoryStruct.whiskerRight
              (CategoryTheory.CategoryStruct.comp α.hom (CategoryTheory.CategoryStruct.comp η ηs)) f =
            η₃
-- Aesop.Index.RulePattern
Aesop.RulePatternIndex.Entry.mk.injEq : ∀ (name : Aesop.RuleName) (pattern : Aesop.RulePattern) (name_1 : Aesop.RuleName) (pattern_1 : Aesop.RulePattern),
  ({ name := name, pattern := pattern } = { name := name_1, pattern := pattern_1 }) =
    (name = name_1 ∧ pattern = pattern_1)
-- Init.Data.Int.Order
Int.natAbs_cast : ∀ (n : ℕ), (↑n).natAbs = n
-- Mathlib.Topology.Category.Compactum
/-- The "free" Compactum functor.  -/
Compactum.free : CategoryTheory.Functor (Type u_1) Compactum
-- Mathlib.Geometry.Convex.Set
/-- Convexity of a set can be checked via binary combinations if the scalars form a field.  -/
Convexity.IsConvexSet.of_convexCombPair_mem : ∀ {K : Type u_4} {X : Type u_5} [inst : Field K] [inst_1 : LinearOrder K] [inst_2 : IsStrictOrderedRing K]
  [inst_3 : Convexity.ConvexSpace K X] {s : Set X},
  (∀ (a b : K) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1),
      ∀ x ∈ s, ∀ y ∈ s, Convexity.convexCombPair a b ha hb hab x y ∈ s) →
    Convexity.IsConvexSet K s
-- Init.Data.Array.Lemmas
List.contains_toArray : ∀ {α : Type u_1} [inst : BEq α] {l : List α} {a : α}, l.toArray.contains a = l.contains a
-- Init.Core
/-- Dependent pairs, in which the second element's type depends on the value of the first element. The
type `Sigma β` is typically written `Σ a : α, β a` or `(a : α) × β a`.

Although its values are pairs, `Sigma` is sometimes known as the *dependent sum type*, since it is
the type level version of an indexed summation.
 -/
Sigma : {α : Type u} → (α → Type v) → Type (max u v)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
MulLECancellable.Injective : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : PartialOrder α] {a : α},
  MulLECancellable a → Function.Injective fun x => a * x
-- Mathlib.Data.Fin.SuccPred
finCongr.congr_simp : ∀ {n m : ℕ} (eq : n = m), finCongr eq = finCongr eq
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Trivialization.mk_coordChangeL : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace B] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : AddCommMonoid F]
  [inst_5 : Module R F] [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module R (E x)]
  (e e' : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_8 : Bundle.Trivialization.IsLinear R e]
  [inst_9 : Bundle.Trivialization.IsLinear R e'] {b : B},
  b ∈ e.baseSet ∩ e'.baseSet → ∀ (y : F), (b, (Bundle.Trivialization.coordChangeL R e e' b) y) = ↑e' ⟨b, e.symm b y⟩
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.compMeasurePreserving_congr : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace γ] [inst_2 : MeasurableSpace β] {ν : MeasureTheory.Measure β} {f : α → β} (g : β →ₘ[ν] γ)
  (hf : MeasureTheory.MeasurePreserving f μ ν) {f' : α → β} (hf' : Measurable f') (h : f =ᵐ[μ] f'),
  g.compMeasurePreserving f hf = g.compMeasurePreserving f' ⋯
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.Substring.Raw.Legacy.any.eq_1 : ∀ (p : Char → Bool) (s_2 : String) (b e : String.Pos.Raw),
  Substring.Raw.Legacy.any { str := s_2, startPos := b, stopPos := e } p = String.Legacy.anyAux s_2 e p b
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.objEquiv_symm_apply : ∀ {n m : ℕ} (f : { len := m } ⟶ { len := n }) (i : Fin (m + 1)),
  (SSet.stdSimplex.objEquiv.symm f) i = (SimplexCategory.Hom.toOrderHom f) i
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.RightExtension.postcompose₂_obj_hom_app : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H)
  (G : CategoryTheory.Functor H D')
  (X : CategoryTheory.Comma ((CategoryTheory.Functor.whiskeringLeft C D H).obj L) (CategoryTheory.Functor.fromPUnit F))
  (X_1 : C), ((CategoryTheory.Functor.RightExtension.postcompose₂ L F G).obj X).hom.app X_1 = G.map (X.hom.app X_1)
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.instElemOrbit : {M : Type u_1} →
  {α : Type u_3} → [inst : AddMonoid M] → [inst_1 : AddAction M α] → {a : α} → AddAction M ↑(AddAction.orbit M a)
-- Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
/-- The property of objects in the functor category `J ⥤ C`
which preserves colimits of shape `K`.  -/
CategoryTheory.ObjectProperty.preservesColimitsOfShape : {J : Type u_1} →
  {C : Type u_3} →
    (K : Type u_5) →
      [CategoryTheory.Category.{v_1, u_5} K] →
        [inst : CategoryTheory.Category.{v_3, u_1} J] →
          [inst_1 : CategoryTheory.Category.{v_5, u_3} C] → CategoryTheory.ObjectProperty (CategoryTheory.Functor J C)
-- Mathlib.CategoryTheory.Adjunction.Triple
/-- Adjunction `F ⊣ G` of the adjoint triple `F ⊣ G ⊣ H`.  -/
CategoryTheory.Adjunction.Triple.adj₁ : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            {H : CategoryTheory.Functor C D} → CategoryTheory.Adjunction.Triple F G H → (F ⊣ G)
-- Mathlib.Data.Nat.Factorization.Basic
Nat.dvd_prod_primeFactors_pow_self : ∀ {n : ℕ}, n ≠ 0 → n ∣ (∏ p ∈ n.primeFactors, p) ^ n
-- Lean.Compiler.LCNF.Types
/-- Return `true` if `type` is an inductive datatype with 0 constructors.  -/
Lean.Compiler.LCNF.isInductiveWithNoCtors : Lean.Expr → Lean.CoreM Bool
-- Init.Data.String.Defs
String.Pos.Raw.offsetBy_rawEndPos_right : ∀ {p : String.Pos.Raw} {s : String}, p.offsetBy s.rawEndPos = s + p
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.HeapNode.brecOn.eq : ∀ {α : Type u} {motive : Batteries.BinomialHeap.Imp.HeapNode α → Sort u_1} (t : Batteries.BinomialHeap.Imp.HeapNode α)
  (F_1 : (t : Batteries.BinomialHeap.Imp.HeapNode α) → Batteries.BinomialHeap.Imp.HeapNode.below t → motive t),
  Batteries.BinomialHeap.Imp.HeapNode.brecOn t F_1 = F_1 t (Batteries.BinomialHeap.Imp.HeapNode.brecOn.go t F_1).2
-- Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
Mathlib.Tactic.Bicategory.instMkEvalCompBicategoryM : Mathlib.Tactic.BicategoryLike.MkEvalComp Mathlib.Tactic.Bicategory.BicategoryM
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Break.runK.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match none with
    | some a => h_1 a
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Algebra.Order.Monovary
AntivaryOn.mul_left₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : PartialOrder α] [IsOrderedRing α]
  [inst_3 : PartialOrder β] {s : Set ι} {f₁ f₂ : ι → α} {g : ι → β},
  (∀ i ∈ s, 0 ≤ f₁ i) → (∀ i ∈ s, 0 ≤ f₂ i) → AntivaryOn f₁ g s → AntivaryOn f₂ g s → AntivaryOn (f₁ * f₂) g s
-- Mathlib.Algebra.Algebra.NonUnitalHom
/-- The left injection into a product is a non-unital algebra homomorphism.  -/
NonUnitalAlgHom.inl : (R : Type u) →
  [inst : Monoid R] →
    (A : Type v) →
      (B : Type w) →
        [inst_1 : NonUnitalNonAssocSemiring A] →
          [inst_2 : DistribMulAction R A] →
            [inst_3 : NonUnitalNonAssocSemiring B] → [inst_4 : DistribMulAction R B] → A →ₙₐ[R] A × B
-- Mathlib.MeasureTheory.Measure.ResolventTransform
MeasureTheory.resolventTransform_zero_measure : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NormedField 𝕜] [inst_1 : NormedRing A] [inst_2 : NormedAlgebra ℝ A]
  [inst_3 : NormedAlgebra 𝕜 A] {m𝕜 : MeasurableSpace 𝕜}, MeasureTheory.resolventTransform 0 = 0
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
ContinuousAlternatingMap.toContinuousMultilinearMapCLM_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] [inst_7 : IsTopologicalAddGroup F] (R : Type u_5) [inst_8 : Semiring R]
  [inst_9 : Module R F] [inst_10 : ContinuousConstSMul R F] [inst_11 : SMulCommClass 𝕜 R F],
  ⇑(ContinuousAlternatingMap.toContinuousMultilinearMapCLM R) = ContinuousAlternatingMap.toContinuousMultilinearMap
-- Mathlib.Topology.Algebra.Group.Basic
isOpenMap_inv : ∀ (G : Type w) [inst : TopologicalSpace G] [inst_1 : InvolutiveInv G] [ContinuousInv G], IsOpenMap Inv.inv
-- Mathlib.Algebra.Colimit.Module
AddCommGroup.DirectLimit.lift_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 ι] (P : Type u_4) [inst_3 : AddCommMonoid P]
  (g : (i : ι) → G i →+ P) (Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x) (i : ι)
  (x : G i), (AddCommGroup.DirectLimit.lift G f P g Hg) ((AddCommGroup.DirectLimit.of G f i) x) = (g i) x
-- Mathlib.Algebra.Homology.HomotopyCategory.Plus
/-- The inclusion of the homotopy category of bounded below cochain complexes
in the homotopy category category of all cochain complexes.  -/
HomotopyCategory.Plus.ι : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      CategoryTheory.Functor (HomotopyCategory.Plus C) (HomotopyCategory C (ComplexShape.up ℤ))
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.roots_map_of_injective : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R} [inst_1 : IsDomain R] {S : Type u_4} [inst_2 : CommRing S]
  [inst_3 : IsDomain S],
  f.Splits → ∀ {i : R →+* S}, Function.Injective ⇑i → (Polynomial.map i f).roots = Multiset.map (⇑i) f.roots
-- Init.Data.Range.Polymorphic.Internal.SignedBitVec
_private.Init.Data.Range.Polymorphic.Internal.SignedBitVec.0.BitVec.Signed.intMaxSealed_eq_intMinSealed_add : ∀ {n : ℕ}, BitVec.Signed.intMaxSealed✝ n = BitVec.Signed.intMinSealed✝ n + ↑(2 ^ n - 1)
-- Mathlib.ModelTheory.Bundled
/-- Lifts a model to a particular universe.  -/
FirstOrder.Language.Theory.ModelType.ulift : {L : FirstOrder.Language} → {T : L.Theory} → T.ModelType → T.ModelType
-- Plausible.Gen
/-- Given a list of examples, choose one to create an example.  -/
Plausible.Gen.elements : {α : Type u} → (xs : List α) → 0 < xs.length → Plausible.Gen α
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey!_insert_le_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {k : α} {v : β}, (cmp (t.insert k v).minKey! k).isLE = true
-- Lean.Server.Utils
/-- Returns the document contents with all changes applied.  -/
Lean.Server.foldDocumentChanges : Array Lean.Lsp.TextDocumentContentChangeEvent → Lean.FileMap → Lean.FileMap
-- Mathlib.Algebra.Ring.Defs
/-- A non-associative commutative ring is a `NonAssocRing` with commutative multiplication.  -/
NonAssocCommRing : Type u → Type u
-- Mathlib.Data.Num.ZNum
Num.div_to_nat : ∀ (n d : Num), ↑(n / d) = ↑n / ↑d
-- Init.Data.String.Lemmas.Order
String.Pos.le_next : ∀ {s : String} {p : s.Pos} {h : p ≠ s.endPos}, p ≤ p.next h
-- Mathlib.Topology.Algebra.Module.FiniteDimension
/-- If `K` is a complete field and `V` is a finite-dimensional vector space over `K` (equipped with
any topology so that `V` is a topological `K`-module, meaning `[IsTopologicalAddGroup V]`
and `[ContinuousSMul K V]`), and `K` is locally compact, then `V` is locally compact.

This is not an instance because `K` cannot be inferred.  -/
LocallyCompactSpace.of_finiteDimensional_of_complete : ∀ (K : Type u_4) (V : Type u_5) [inst : NontriviallyNormedField K] [CompleteSpace K] [LocallyCompactSpace K]
  [inst_3 : AddCommGroup V] [inst_4 : TopologicalSpace V] [IsTopologicalAddGroup V] [inst_6 : Module K V]
  [ContinuousSMul K V] [FiniteDimensional K V], LocallyCompactSpace V
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- A cofan over `f : β → C` consists of a collection of maps from every `f b` to an object `P`.  -/
CategoryTheory.Limits.Cofan.mk : {β : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f : β → C} → (P : C) → ((b : β) → f b ⟶ P) → CategoryTheory.Limits.Cofan f
-- Lean.Elab.PreDefinition.FixedParams
Lean.Elab.FixedParamPerms.mk.sizeOf_spec : ∀ (numFixed : ℕ) (perms : Array Lean.Elab.FixedParamPerm) (revDeps : Array (Array (Array ℕ))),
  sizeOf { numFixed := numFixed, perms := perms, revDeps := revDeps } =
    1 + sizeOf numFixed + sizeOf perms + sizeOf revDeps
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
SSet.instIsMultiplicativeAnodyneExtensions : SSet.anodyneExtensions.IsMultiplicative
-- Lean.Data.Lsp.Workspace
Lean.Lsp.DidChangeWatchedFilesRegistrationOptions : Type
-- Mathlib.NumberTheory.NumberField.FractionalIdeal
NumberField.mem_span_basisOfFractionalIdeal : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  {I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ} {x : K},
  x ∈ Submodule.span ℤ (Set.range ⇑(NumberField.basisOfFractionalIdeal K I)) ↔ x ∈ ↑↑I
-- Mathlib.Topology.Algebra.UniformConvergence
instDivUniformFun : {α : Type u_1} → {β : Type u_2} → [Div β] → Div (UniformFun α β)
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.NF.eval_cons_eq_eval_of_eq_of_eq : ∀ {M : Type u_1} [inst : CommGroupWithZero M] (r : ℤ) (x : M) {t t' l' : Mathlib.Tactic.FieldSimp.NF M},
  t.eval = t'.eval → ((r, x) ::ᵣ t').eval = l'.eval → ((r, x) ::ᵣ t).eval = l'.eval
-- Mathlib.Algebra.Module.Lattice
Module.Basis.extendOfIsLattice.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra R K] {V : Type u_3}
  [inst_3 : AddCommGroup V] [inst_4 : Module K V] [inst_5 : Module R V] [inst_6 : IsScalarTower R K V]
  [inst_7 : IsFractionRing R K] {κ : Type u_4} {M : Submodule R V} [inst_8 : Submodule.IsLattice K M]
  (b : Module.Basis κ R ↥M), Module.Basis.extendOfIsLattice K b = Module.Basis.mk ⋯ ⋯
-- Mathlib.Algebra.Opposites
AddOpposite.op_inj : ∀ {α : Type u_1} {x y : α}, AddOpposite.op x = AddOpposite.op y ↔ x = y
-- Mathlib.Combinatorics.Matroid.Minor.Delete
Matroid.Coindep.delete_rankPos : ∀ {α : Type u_1} {M : Matroid α} {D : Set α} [M.RankPos], M.Coindep D → (M.delete D).RankPos
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.map_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] (f : β → γ) (g : α → β) (hf : Continuous f) (hg : Continuous g)
  (K : TopologicalSpace.Compacts α),
  TopologicalSpace.Compacts.map (f ∘ g) ⋯ K = TopologicalSpace.Compacts.map f hf (TopologicalSpace.Compacts.map g hg K)
-- Mathlib.AlgebraicGeometry.FunctionField
AlgebraicGeometry.genericPoint_eq_of_isOpenImmersion : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] [hX : IrreducibleSpace ↥X]
  [inst : IrreducibleSpace ↥Y], f (genericPoint ↥X) = genericPoint ↥Y
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.image_op_vadd : ∀ {α : Type u_2} [inst : Add α] {s t : Set α}, AddOpposite.op '' s +ᵥ t = t + s
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.convolutionExtensionUnit_comp_ι_map_tensorHom_app : ∀ (C : Type u₁) {inst : CategoryTheory.Category.{v₁, u₁} C} (V : Type u₂) {inst_1 : CategoryTheory.Category.{v₂, u₂} V}
  {inst_2 : CategoryTheory.MonoidalCategory C} {inst_3 : CategoryTheory.MonoidalCategory V} {D : Type u₃}
  {inst_4 : CategoryTheory.Category.{v₃, u₃} D} {inst_5 : CategoryTheory.MonoidalCategoryStruct D}
  [self : CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct C V D] {d₁ d₂ d₁' d₂' : D}
  (f₁ : d₁ ⟶ d₁') (f₂ : d₂ ⟶ d₂') (x y : C),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.convolutionExtensionUnit C V d₁
            d₂).app
        (x, y))
      (((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).map
            (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ f₂)).app
        (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom
        (((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).map f₁).app x)
        (((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).map f₂).app y))
      ((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.convolutionExtensionUnit C V d₁'
            d₂').app
        (x, y))
-- Mathlib.Analysis.Normed.Group.Pointwise
sphere_mul_singleton : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] (δ : ℝ) (x y : E), Metric.sphere x δ * {y} = Metric.sphere (x * y) δ
-- Mathlib.Topology.UniformSpace.UniformConvergence
tendstoUniformlyOn_univ : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι},
  TendstoUniformlyOn F f p Set.univ ↔ TendstoUniformly F f p
-- Mathlib.SetTheory.Ordinal.Principal
Ordinal.isPrincipal_add_iff_add_left_eq_self : ∀ {o : Ordinal.{u}}, Ordinal.IsPrincipal (fun x1 x2 => x1 + x2) o ↔ ∀ a < o, a + o = o
-- Mathlib.Topology.Sequences
/-- If the domain of a function `f : α → β` is a Fréchet-Urysohn space, then convergence
is equivalent to sequential convergence. See also `Filter.tendsto_iff_seq_tendsto` for a version
that works for any pair of filters assuming that the filter in the domain is countably generated.

This property is equivalent to the definition of `FrechetUrysohnSpace`, see
`FrechetUrysohnSpace.of_seq_tendsto_imp_tendsto`.  -/
tendsto_nhds_iff_seq_tendsto : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [FrechetUrysohnSpace X]
  {f : X → Y} {a : X} {b : Y},
  Filter.Tendsto f (nhds a) (nhds b) ↔
    ∀ (u : ℕ → X), Filter.Tendsto u Filter.atTop (nhds a) → Filter.Tendsto (f ∘ u) Filter.atTop (nhds b)
-- Mathlib.Algebra.Homology.Additive
HomologicalComplex.hasIntScalar : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] → {c : ComplexShape ι} → {C D : HomologicalComplex V c} → SMul ℤ (C ⟶ D)
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
/-- Bundles `fun x : ℝ≥0∞ => x ^ y` into an order isomorphism when `y : ℝ` is positive,
where the inverse is `fun x : ℝ≥0∞ => x ^ (1 / y)`.  -/
ENNReal.orderIsoRpow : (y : ℝ) → 0 < y → ENNReal ≃o ENNReal
-- Mathlib.Data.Set.Finite.Lattice
Finite.Set.finite_iUnion : ∀ {α : Type u} {ι : Sort w} [Finite ι] (f : ι → Set α) [∀ (i : ι), Finite ↑(f i)], Finite ↑(⋃ i, f i)
-- Mathlib.MeasureTheory.Measure.AEMeasurable
aemeasurable_of_subsingleton_codomain : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β}
  {μ : MeasureTheory.Measure α} [Subsingleton β], AEMeasurable f μ