mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.forIn'_ric : ∀ {α β : Type u} {m : Type u → Type v} {ps : Std.Do.PostShape} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps]
  [inst_2 : Std.PRange.Least? α] [inst_3 : LE α] [inst_4 : DecidableLE α] [inst_5 : Std.PRange.UpwardEnumerable α]
  [inst_6 : Std.Rxc.IsAlwaysFinite α] [inst_7 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_8 : Std.PRange.LawfulUpwardEnumerableLeast? α] [inst_9 : Std.PRange.LawfulUpwardEnumerableLE α] {xs : Std.Ric α}
  {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)} (inv : Std.Do.Invariant xs.toList β ps),
  (∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
      ⦃inv.1 ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄
        f cur ⋯ b ⦃(fun r =>
          match r with
          | ForInStep.yield b' => inv.1 ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
          | ForInStep.done b' => inv.1 ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'),
          inv.2)⦄) →
    ⦃inv.1 ({ «prefix» := [], suffix := xs.toList, property := ⋯ }, init)⦄
      forIn' xs init f ⦃(fun b => inv.1 ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b), inv.2)⦄
-- Init.Data.BitVec.Lemmas
BitVec.sshiftRight'_ofNat_eq_sshiftRight : ∀ {w : ℕ} {x : BitVec w} {k : ℕ}, x.sshiftRight' (BitVec.ofNat w k) = x.sshiftRight (k % 2 ^ w)
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- If two functions agree in a neighborhood within `s`, then so do their Taylor series.  -/
Filter.EventuallyEq.ftaylorSeriesWithin : ∀ (𝕜 : Type u) [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f f₁ : E → F} {x : E},
  f₁ =ᶠ[nhdsWithin x s] f → ftaylorSeriesWithin 𝕜 f₁ s =ᶠ[nhdsWithin x s] ftaylorSeriesWithin 𝕜 f s
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
curveIntegrable_cast_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b c d : E}
  {ω : E → E →L[𝕜] F} {γ : Path a b} (hc : c = a) (hd : d = b), CurveIntegrable ω (γ.cast hc hd) ↔ CurveIntegrable ω γ
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.piFinset_eq_comap_restrict : ∀ {ι : Type u_4} {X : ι → Type u_5} [inst : (i : ι) → MeasurableSpace (X i)] (s : Finset ι),
  ↑MeasureTheory.Filtration.piFinset s = MeasurableSpace.comap (↑s).domRestrict MeasurableSpace.pi
-- Mathlib.Order.Filter.Pointwise
/-- Negation is involutive on `Filter α` if it is on `α`.  -/
Filter.instInvolutiveNeg : {α : Type u_2} → [InvolutiveNeg α] → InvolutiveNeg (Filter α)
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBSet.isEmpty.match_1.splitter : {α : Type u_1} →
  {cmp : α → α → Ordering} →
    (motive : RBTree.RBSet α cmp → Sort u_2) →
      (x : RBTree.RBSet α cmp) →
        ((property : RBTree.RBNode.WF cmp RBTree.RBNode.nil) → motive ⟨RBTree.RBNode.nil, property⟩) →
          ((x : RBTree.RBSet α cmp) →
              (∀ (property : RBTree.RBNode.WF cmp RBTree.RBNode.nil), x = ⟨RBTree.RBNode.nil, property⟩ → False) →
                motive x) →
            motive x
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.limitCompWhiskeringLeftIsoCompLimit_hom_whiskerLeft_π_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {J : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂}
  [inst_3 : CategoryTheory.Category.{v₂, u₂} K] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C))
  (G : CategoryTheory.Functor D K) [inst_4 : CategoryTheory.Limits.HasLimitsOfShape J C] (j : J)
  {Z : CategoryTheory.Functor D C} (h : G.comp (F.obj j) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitCompWhiskeringLeftIsoCompLimit F G).hom
      (CategoryTheory.CategoryStruct.comp (G.whiskerLeft (CategoryTheory.Limits.limit.π F j)) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.limit.π (F.comp ((CategoryTheory.Functor.whiskeringLeft D K C).obj G)) j) h
-- Mathlib.NumberTheory.NumberField.Units.Regulator
NumberField.Units.regulator_eq_det' : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.Units.regulator K =
    |(Matrix.of fun i =>
          (NumberField.Units.logEmbedding K)
            (Additive.ofMul (NumberField.Units.fundSystem K ((NumberField.Units.equivFinRank K).symm i)))).det|
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
right_lt_lineMap_iff_lt : ∀ {k : Type u_1} {E : Type u_2} [inst : Ring k] [inst_1 : PartialOrder k] [IsOrderedRing k] [inst_3 : AddCommGroup E]
  [inst_4 : PartialOrder E] [IsOrderedAddMonoid E] [inst_6 : Module k E] [IsStrictOrderedModule k E] {a b : E} {r : k}
  [PosSMulReflectLT k E], r < 1 → (b < (AffineMap.lineMap a b) r ↔ b < a)
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
/-- The characteristic function of a measure is a product of
characteristic functions if and only if it is a product measure.
This is the version for Banach spaces, see `charFun_eq_prod_iff`
for the Hilbert space version.  -/
MeasureTheory.charFunDual_eq_prod_iff : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {mE : MeasurableSpace E}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {mF : MeasurableSpace F} {μ : MeasureTheory.Measure E}
  {ν : MeasureTheory.Measure F} [BorelSpace E] [SecondCountableTopology E] [BorelSpace F] [SecondCountableTopology F]
  [CompleteSpace E] [CompleteSpace F] {ξ : MeasureTheory.Measure (E × F)} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν] [MeasureTheory.IsFiniteMeasure ξ],
  (∀ (L : StrongDual ℝ (E × F)),
      MeasureTheory.charFunDual ξ L =
        MeasureTheory.charFunDual μ (L ∘SL ContinuousLinearMap.inl ℝ E F) *
          MeasureTheory.charFunDual ν (L ∘SL ContinuousLinearMap.inr ℝ E F)) ↔
    ξ = μ.prod ν
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
/-- If an additive group satisfies the universal property of an additive free group with respect to
a given type, then it admits an additive free group basis based on this type. Here, the universal
property is expressed as in `IsFreeAddGroup.lift` and its properties.  -/
FreeAddGroupBasis.ofLift : {G : Type u} →
  [inst : AddGroup G] →
    (X : Type u) →
      (of : X → G) →
        (lift : {H : Type u} → [inst_1 : AddGroup H] → (X → H) ≃ (G →+ H)) →
          (∀ {H : Type u} [inst_1 : AddGroup H] (f : X → H) (a : X), (lift f) (of a) = f a) → FreeAddGroupBasis X G
-- Mathlib.Algebra.Homology.HomologicalComplex
CochainComplex.of.d.eq_1 : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  {α : Type u_2} [inst_2 : AddRightCancelSemigroup α] [inst_3 : One α] [inst_4 : DecidableEq α] (X : α → V)
  (d : (n : α) → X n ⟶ X (n + 1)) (i j : α),
  CochainComplex.of.d X d i j =
    if h : i + 1 = j then CategoryTheory.CategoryStruct.comp (d i) (CategoryTheory.eqToHom ⋯) else 0
-- Batteries.Data.Nat.Bitwise.Lemmas
Nat.or_self_right : ∀ (a b : ℕ), a ||| b ||| b = a ||| b
-- Mathlib.RingTheory.Spectrum.Maximal.Localization
PrimeSpectrum.mapPiLocalization_id : ∀ {R : Type u_1} [inst : CommSemiring R],
  PrimeSpectrum.mapPiLocalization (RingHom.id R) = RingHom.id (PrimeSpectrum.PiLocalization R)
-- Mathlib.Data.Int.Interval
Int.instLocallyFiniteOrder : LocallyFiniteOrder ℤ
-- Lean.Data.Format
Lean.instToFormatProdNameDataValue : Std.ToFormat (Lean.Name × Lean.DataValue)
-- Mathlib.CategoryTheory.Opposites
/-- The opposite of a natural transformation.  -/
CategoryTheory.NatTrans.op : {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} → (F ⟶ G) → (G.op ⟶ F.op)
-- Lean.Server.References
/-- Additional `InfoTree` information for this reference.  -/
Lean.Server.Reference.info : Lean.Server.Reference → Lean.Elab.Info
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
/-- If there is a pointwise right Kan extension of `F` along `L`, and if `G` preserves them,
then `G` preserves right Kan extensions of `F` along `L`.  -/
CategoryTheory.Functor.preservesPointwiseRKEOfHasPointwiseAndPreservesPointwise : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) [L.HasPointwiseRightKanExtension F] [G.PreservesPointwiseRightKanExtension F L],
  G.PreservesRightKanExtension F L
-- Mathlib.Algebra.Order.CompleteField
/-- Preparatory lemma for `inducedOrderRingHom`.  -/
ConditionallyCompleteLinearOrderedField.exists_mem_cutMap_mul_self_of_lt_inducedMap_mul_self : ∀ {α : Type u_2} {β : Type u_3} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : Field β]
  [inst_4 : ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] {a : α},
  0 < a →
    ∀
      b <
        ConditionallyCompleteLinearOrderedField.inducedMap α β a *
          ConditionallyCompleteLinearOrderedField.inducedMap α β a,
      ∃ c ∈ LinearOrderedField.cutMap β (a * a), b < c
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
PiTensorProduct.projectiveSeminormAux_nonneg : ∀ {ι : Type u_1} [inst : Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)]
  [inst_2 : NormedField 𝕜] (p : FreeAddMonoid (𝕜 × ((i : ι) → E i))), 0 ≤ PiTensorProduct.projectiveSeminormAux p
-- Mathlib.Algebra.GroupWithZero.Semiconj
SemiconjBy.zero_left : ∀ {G₀ : Type u_1} [inst : MulZeroClass G₀] (x y : G₀), SemiconjBy 0 x y
-- Mathlib.Analysis.Complex.UnitDisc.Basic
/-- Real part of a point of the unit disc.  -/
Complex.UnitDisc.re : Complex.UnitDisc → ℝ
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
/-- If we know `f = 0`,
it requires a little work to conclude `image.ι f = 0`,
because `f = g` only implies `image f ≅ image g`.
 -/
CategoryTheory.Limits.image.ι_zero' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasEqualizers C] {X Y : C} {f : X ⟶ Y},
  f = 0 → ∀ [inst_4 : CategoryTheory.Limits.HasImage f], CategoryTheory.Limits.image.ι f = 0
-- Mathlib.Analysis.Convex.Cone.InnerDual
Submodule.topologicalClosure.eq_1 : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : ContinuousConstSMul R M] [inst_5 : ContinuousAdd M] (s : Submodule R M),
  s.topologicalClosure = { toAddSubmonoid := s.topologicalClosure, smul_mem' := ⋯ }
-- Mathlib.Data.Finset.Card
/-- Given a function `f` which sends the finite set `s` to itself, the sequence of images of `s` under
iterates of `f` is eventually constant. Furthermore, the sequence of images stabilises in fewer
than `#s` steps.
 -/
Finset.image_iterate_stabilises_lt_card : ∀ {α : Type u_1} [inst : DecidableEq α] {f : α → α} {s : Finset α},
  Set.MapsTo f ↑s ↑s → s.Nonempty → ∃ n < s.card, ∀ (m : ℕ), n ≤ m → Finset.image f^[m] s = Finset.image f^[n] s
-- Mathlib.Analysis.Complex.Circle
Circle.instContinuousNeg : ContinuousNeg Circle
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_empty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {a : α} [inst_1 : Inhabited α],
  ∅.getKey! a = default
-- Mathlib.AlgebraicGeometry.Scheme
/-- We define `Scheme` as an `X : LocallyRingedSpace`,
along with a proof that every point has an open neighbourhood `U`
so that the restriction of `X` to `U` is isomorphic,
as a locally ringed space, to `Spec.toLocallyRingedSpace.obj (op R)`
for some `R : CommRingCat`.
 -/
AlgebraicGeometry.Scheme : Type (u_1 + 1)
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_quotient_mk' : ∀ {α : Type u_1} [inst : MeasurableSpace α] [s : Setoid α], Measurable Quotient.mk'
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Append
Std.Tactic.BVDecide.BVExpr.bitblast.AppendTarget.rhs : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} →
        {combined : ℕ} → (self : Std.Tactic.BVDecide.BVExpr.bitblast.AppendTarget aig combined) → aig.RefVec self.rw
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
/-- A global presentation of a sheaf of modules `M` consists of a family `generators.s`
of sections `s` which generate `M`, and a family of sections which generate
the kernel of the morphism `generators.π : free (generators.I) ⟶ M`.  -/
SheafOfModules.Presentation : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [CategoryTheory.HasWeakSheafify J AddCommGrpCat] →
          [J.WEqualsLocallyBijective AddCommGrpCat] → SheafOfModules R → Type (max (u + 1) u₁)
-- Mathlib.Algebra.Group.Finsupp
Finsupp.instIsRightCancelAdd : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddZeroClass M] [IsRightCancelAdd M], IsRightCancelAdd (ι →₀ M)
-- Mathlib.Analysis.Normed.Ring.Units
/-- An ideal which contains an element within `1` of `1 : R` is the unit ideal.  -/
Ideal.eq_top_of_norm_lt_one : ∀ {R : Type u_1} [inst : NormedRing R] [HasSummableGeomSeries R] (I : Ideal R) {x : R}, x ∈ I → ‖1 - x‖ < 1 → I = ⊤
-- Mathlib.Analysis.Calculus.FDeriv.Mul
differentiableOn_inv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {R : Type u_5} [inst_1 : NormedDivisionRing R]
  [inst_2 : NormedAlgebra 𝕜 R], DifferentiableOn 𝕜 (fun x => x⁻¹) {x | x ≠ 0}
-- Init.Data.List.ToArray
List.takeWhile_toArray : ∀ {α : Type u_1} (p : α → Bool) (l : List α), Array.takeWhile p l.toArray = (List.takeWhile p l).toArray
-- Mathlib.Data.List.DropRight
List.rtake.eq_1 : ∀ {α : Type u_1} (l : List α) (n : ℕ), l.rtake n = List.drop (l.length - n) l
-- Mathlib.CategoryTheory.Subobject.Types
Types.monoOverEquivalenceSet_functor_obj : ∀ (α : Type u) (f : CategoryTheory.MonoOver α),
  (Types.monoOverEquivalenceSet α).functor.obj f = Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.obj.hom)
-- Mathlib.Order.InitialSeg
/-- Construct an initial segment embedding `r ≼i s` by "filling in the gaps". That is, each
subsequent element in `α` is mapped to the least element in `β` that hasn't been used yet.

This construction is guaranteed to work as long as there exists some relation embedding `r ↪r s`.  -/
RelEmbedding.collapse : {α : Type u_1} → {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → [IsWellOrder β s] → r ↪r s → InitialSeg r s
-- Mathlib.RingTheory.Polynomial.Quotient
Polynomial.quotientSpanXSubCAlgEquiv_mk : ∀ {R : Type u_1} [inst : CommRing R] (x : R) (p : Polynomial R),
  (Polynomial.quotientSpanXSubCAlgEquiv x) ((Ideal.Quotient.mk (Ideal.span {Polynomial.X - Polynomial.C x})) p) =
    Polynomial.eval x p
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.IsImage.iff_preimage_eq : ∀ {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β},
  e.IsImage s t ↔ e.source ∩ ↑e ⁻¹' t = e.source ∩ s
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- A natural isomorphism `S ≅ S'` induces an equivalence
`CostrucutredArrow S T ≌ CostructuredArrow S' T`.  -/
CategoryTheory.CostructuredArrow.mapNatIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {T : D} →
          {S S' : CategoryTheory.Functor C D} →
            (S ≅ S') → (CategoryTheory.CostructuredArrow S T ≌ CategoryTheory.CostructuredArrow S' T)
-- Mathlib.Order.Monotone.Monovary
monovary_self : ∀ {ι : Type u_1} {α : Type u_3} [inst : Preorder α] (f : ι → α), Monovary f f
-- Mathlib.FieldTheory.IsAlgClosed.Basic
IsAlgClosed.card_roots_map_eq_natDegree_of_injective : ∀ {A : Type u_1} {B : Type u_2} [inst : Semiring A] [inst_1 : Field B] [IsAlgClosed B] {f : A →+* B} (p : Polynomial A),
  Function.Injective ⇑f → (Polynomial.map f p).roots.card = p.natDegree
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.rcons_inj : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] [inst_1 : (i : ι) → DecidableEq (M i)] {i : ι},
  Function.Injective Monoid.CoprodI.Word.rcons
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.isCompl_toSubmodule : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {N N' : LieSubmodule R L M}, IsCompl ↑N ↑N' ↔ IsCompl N N'
-- Mathlib.Order.RelSeries
RelSeries.smash_succ_castAdd : ∀ {α : Type u_1} {r : SetRel α α} {p q : RelSeries r} (h : p.last = q.head) (i : Fin p.length),
  (p.smash q h).toFun (Fin.castAdd q.length i).succ = p.toFun i.succ
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.symm_comp_self : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] (e : A ≃A[R] B), ⇑e.symm ∘ ⇑e = id
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- `b.localFrame e i` is indeed a local frame on `e.baseSet`  -/
Bundle.Trivialization.isLocalFrameOn_localFrame_baseSet : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] (n : WithTop ℕ∞) {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] [inst_13 : VectorBundle 𝕜 F V]
  [ContMDiffVectorBundle n F V I] {ι : Type u_7} (e : Bundle.Trivialization F Bundle.TotalSpace.proj)
  [inst_15 : MemTrivializationAtlas e] (b : Module.Basis ι 𝕜 F), IsLocalFrameOn I F n (e.localFrame b) e.baseSet
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.PositiveCompacts.carrier_eq_coe : ∀ {α : Type u_1} [inst : TopologicalSpace α] (s : TopologicalSpace.PositiveCompacts α), s.carrier = ↑s
-- Mathlib.Algebra.Group.Defs
CommMonoid.mk : {M : Type u} → [toMonoid : Monoid M] → (∀ (a b : M), a * b = b * a) → CommMonoid M
-- Init.Data.Array.Lemmas
Array.all_reverse : ∀ {α : Type u_1} {f : α → Bool} {xs : Array α}, xs.reverse.all f = xs.all f
-- Mathlib.Analysis.Normed.Ring.Basic
Real.normedCommRing : NormedCommRing ℝ
-- Mathlib.MeasureTheory.Group.Prod
MeasureTheory.quasiMeasurePreserving_neg : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G)
  [MeasureTheory.SFinite μ] [MeasurableNeg G] [μ.IsAddLeftInvariant],
  MeasureTheory.Measure.QuasiMeasurePreserving Neg.neg μ μ
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.coe_inf : ∀ {G : Type u_1} [inst : Group G] (p p' : Subgroup G), ↑(p ⊓ p') = ↑p ∩ ↑p'
-- Mathlib.MeasureTheory.PiSystem
/-- A Dynkin system is closed under countable union of pairwise disjoint sets. Use a more general
`MeasurableSpace.DynkinSystem.has_iUnion` instead.  -/
MeasurableSpace.DynkinSystem.has_iUnion_nat : ∀ {α : Type u_4} (self : MeasurableSpace.DynkinSystem α) {f : ℕ → Set α},
  Pairwise (Function.onFun Disjoint f) → (∀ (i : ℕ), self.Has (f i)) → self.Has (⋃ i, f i)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.le_maxD_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  k ∈ t → ∀ {fallback : α}, (cmp k (t.maxD fallback)).isLE = true
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.coe_transEquiv : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : PartialEquiv α β} {g : β ≃ γ}, ↑(f.transEquiv g) = ⇑g ∘ ↑f
-- Mathlib.Topology.FiberBundle.Basic
memTrivializationAtlas_iff : ∀ {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {E : B → Type u_5}
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_3 : (b : B) → TopologicalSpace (E b)]
  [inst_4 : FiberBundle F E] (e : Bundle.Trivialization F Bundle.TotalSpace.proj),
  MemTrivializationAtlas e ↔ e ∈ trivializationAtlas F E
-- Mathlib.Algebra.Group.Indicator
Set.indicator_add : ∀ {α : Type u_1} {M : Type u_4} [inst : AddZeroClass M] (s : Set α) (f g : α → M),
  (s.indicator fun a => f a + g a) = fun a => s.indicator f a + s.indicator g a
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.mk.inj : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_5} {inst : Ring k} {inst_1 : AddCommGroup V} {inst_2 : Module k V}
  {inst_3 : AddTorsor V P} {n : ℕ} {points : Fin (n + 1) → P} {independent : AffineIndependent k points}
  {points_1 : Fin (n + 1) → P} {independent_1 : AffineIndependent k points_1},
  { points := points, independent := independent } = { points := points_1, independent := independent_1 } →
    points = points_1
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
FundamentalGroupoid.instNonempty : ∀ (X : Type u_3) [Nonempty X], Nonempty (FundamentalGroupoid X)
-- Mathlib.RingTheory.Flat.Basic
/-- If `A`, `B` are `R`-algebras, `R` injects into `B`,
and `A` is a nontrivial flat `R`-algebra, then `A ⊗[R] B` is nontrivial.  -/
Algebra.TensorProduct.nontrivial_of_algebraMap_injective_of_flat_left : ∀ (R : Type u_1) [inst : CommSemiring R] (A : Type u_2) (B : Type u_3) [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B],
  Function.Injective ⇑(algebraMap R B) → ∀ [Module.Flat R A] [Nontrivial A], Nontrivial (TensorProduct R A B)
-- Mathlib.LinearAlgebra.Matrix.IsDiag
Matrix.isDiag_conjTranspose_iff : ∀ {α : Type u_1} {n : Type u_4} [inst : NonUnitalNonAssocSemiring α] [inst_1 : StarRing α] {A : Matrix n n α},
  A.conjTranspose.IsDiag ↔ A.IsDiag
-- Init.Data.Vector.Lemmas
Vector.swapIfInBounds_mk : ∀ {α : Type u_1} {n : ℕ} {xs : Array α} (h : xs.size = n) {i j : ℕ},
  (Vector.mk xs h).swapIfInBounds i j = Vector.mk (xs.swapIfInBounds i j) ⋯
-- Mathlib.Order.Directed
/-- An antitone function on a downwards-directed type is directed.  -/
directed_of_isDirected_ge : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [IsCodirectedOrder α] {f : α → β} {r : β → β → Prop},
  (∀ ⦃j i : α⦄, j ≤ i → r (f i) (f j)) → Directed r f
-- Mathlib.Algebra.Order.Hom.Basic
le_map_add_map_div' : ∀ {F : Type u_2} {α : Type u_3} {β : Type u_4} [inst : FunLike F α β] [inst_1 : Group α] [inst_2 : AddCommMonoid β]
  [inst_3 : PartialOrder β] [GroupSeminormClass F α β] (f : F) (x y : α), f x ≤ f y + f (y / x)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CallHierarchyOutgoingCall.mk.sizeOf_spec : ∀ («to» : Lean.Lsp.CallHierarchyItem) (fromRanges : Array Lean.Lsp.Range),
  sizeOf { «to» := «to», fromRanges := fromRanges } = 1 + sizeOf «to» + sizeOf fromRanges
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.isSome_minKey?_of_isSome_minKey?_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, (t.erase k).minKey?.isSome = true → t.minKey?.isSome = true
-- Mathlib.Order.Interval.Set.Image
Set.image_subtype_val_Ioi_subset : ∀ {α : Type u_1} [inst : Preorder α] {p : α → Prop} (a : { x // p x }), Subtype.val '' Set.Ioi a ⊆ Set.Ioi ↑a
-- Mathlib.Algebra.Module.Congruence.Defs
ModuleCon.instSMulWithZeroQuotient : {S : Type u_2} →
  (M : Type u_3) →
    [inst : Zero S] →
      [inst_1 : Zero M] →
        [inst_2 : Add M] → [inst_3 : SMulWithZero S M] → (c : ModuleCon S M) → SMulWithZero S (ModuleCon.Quotient M c)
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.quotientMapSubgroupOfOfLe.eq_1 : ∀ {G : Type u} [inst : Group G] {A' A B' B : Subgroup G} [_hAN : (A'.subgroupOf A).Normal]
  [_hBN : (B'.subgroupOf B).Normal] (h' : A' ≤ B') (h : A ≤ B),
  QuotientGroup.quotientMapSubgroupOfOfLe h' h =
    QuotientGroup.map (A'.subgroupOf A) (B'.subgroupOf B) (Subgroup.inclusion h) ⋯