mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.Drop
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.Drop.0.Std.Iterators.Types.Drop.instIterator.match_3.eq_2 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] (it : Std.IterM m β)
  (motive : it.internalState.inner.Step → Sort u_3) (it' : Std.IterM m β)
  (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.skip it'))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) →
        (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out)) →
          motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 :
    (it' : Std.IterM m β) →
      (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.internalState.inner.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.skip it', h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_2 it' h
-- Mathlib.RingTheory.DedekindDomain.Basic
Ring.DimensionLEOne.principal_ideal_ring : ∀ (A : Type u_2) [inst : CommRing A] [IsDomain A] [IsPrincipalIdealRing A], Ring.DimensionLEOne A
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.Subgraph.IsMatching.eq_1 : ∀ {V : Type u_1} {G : SimpleGraph V} (M : G.Subgraph), M.IsMatching = ∀ ⦃v : V⦄, v ∈ M.verts → ∃! w, M.Adj v w
-- Mathlib.Data.Nat.GCD.Prime
Nat.Prime.dvd_or_dvd_of_dvd_lcm : ∀ {p a b : ℕ}, Nat.Prime p → p ∣ a.lcm b → p ∣ a ∨ p ∣ b
-- Mathlib.Data.Finsupp.Multiset
Finsupp.toMultiset_single : ∀ {α : Type u_1} (a : α) (n : ℕ), (Finsupp.toMultiset fun₀ | a => n) = n • {a}
-- Std.Data.ExtDTreeMap.Basic
Std.ExtDTreeMap.instCoeTypeForall : {α : Type u} → Coe (Type v) (α → Type v)
-- Mathlib.CategoryTheory.FiberedCategory.HasFibers
/-- A version of fullness of the functor `Fib S ⥤ Fiber p S` that can be used inside the category
`𝒳`.  -/
HasFibers.Fib.homMk : {𝒮 : Type u₁} →
  {𝒳 : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳] →
        {p : CategoryTheory.Functor 𝒳 𝒮} →
          [inst_2 : HasFibers p] →
            {S : 𝒮} →
              {a b : HasFibers.Fib p S} →
                (φ : (HasFibers.ι S).obj a ⟶ (HasFibers.ι S).obj b) →
                  [p.IsHomLift (CategoryTheory.CategoryStruct.id S) φ] → a ⟶ b
-- Mathlib.Algebra.GroupWithZero.Associated
Associated.comm : ∀ {M : Type u_1} [inst : Monoid M] {x y : M}, Associated x y ↔ Associated y x
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.isTheta_norm_right : ∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {f : α → E}
  {g' : α → F'} {l : Filter α}, (f =Θ[l] fun x => ‖g' x‖) ↔ f =Θ[l] g'
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get?_filter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {f : (a : α) → β a → Bool} {k : α}, m.WF → (Std.DHashMap.Raw.filter f m).get? k = Option.filter (f k) (m.get? k)
-- Mathlib.Data.Seq.Computation
Computation.instCoeTC : {α : Type u} → CoeTC α (Computation α)
-- Mathlib.CategoryTheory.Sites.Continuous
/-- The composition of two pushforward functors on sheaves identifies to
the pushforward for the composition of the two functors.  -/
CategoryTheory.Functor.sheafPushforwardContinuousComp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            (F : CategoryTheory.Functor C D) →
              (G : CategoryTheory.Functor D E) →
                (A : Type u) →
                  [inst_3 : CategoryTheory.Category.{t, u} A] →
                    (J : CategoryTheory.GrothendieckTopology C) →
                      (K : CategoryTheory.GrothendieckTopology D) →
                        (L : CategoryTheory.GrothendieckTopology E) →
                          [inst_4 : F.IsContinuous J K] →
                            [inst_5 : G.IsContinuous K L] →
                              (G.sheafPushforwardContinuous A K L).comp (F.sheafPushforwardContinuous A J K) ≅
                                (F.comp G).sheafPushforwardContinuous A J L
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
/-- The morphism `Π F.obj (U i) ⟶ Π F.obj (U i) ⊓ (U j)` whose components
are given by the restriction maps from `U i` to `U i ⊓ U j`.
 -/
TopCat.Presheaf.SheafConditionEqualizerProducts.leftRes : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasProducts C] →
      {X : TopCat} →
        (F : TopCat.Presheaf C X) →
          {ι : Type v'} →
            (U : ι → TopologicalSpace.Opens ↑X) →
              TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens F U ⟶
                TopCat.Presheaf.SheafConditionEqualizerProducts.piInters F U
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
CategoryTheory.DerivedCategory.map_triangleOfSESδ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.Additive] [inst_5 : CategoryTheory.Limits.PreservesFiniteLimits F]
  [inst_6 : CategoryTheory.Limits.PreservesFiniteColimits F] [inst_7 : HasDerivedCategory C]
  [inst_8 : HasDerivedCategory D] {S : CategoryTheory.ShortComplex (CochainComplex C ℤ)} (hS : S.ShortExact),
  F.mapDerivedCategory.map (DerivedCategory.triangleOfSESδ hS) =
    CategoryTheory.CategoryStruct.comp (F.mapDerivedCategoryFactors.hom.app S.X₃)
      (CategoryTheory.CategoryStruct.comp (DerivedCategory.triangleOfSESδ ⋯)
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.shiftFunctor (DerivedCategory D) 1).map (F.mapDerivedCategoryFactors.inv.app S.X₁))
          ((CategoryTheory.Functor.commShiftIso F.mapDerivedCategory 1).inv.app (DerivedCategory.Q.obj S.X₁))))
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.root.eq_1 : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRoot S f), h.root = h.map Polynomial.X
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.or_congr_r : ∀ {σs : List (Type u)} {P Q Q' : Std.Do.SPred σs}, (Q ⊣⊢ₛ Q') → P ∨ Q ⊣⊢ₛ P ∨ Q'
-- Mathlib.Order.Hom.Bounded
BoundedOrderHom.id_apply : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : BoundedOrder α] (a : α), (BoundedOrderHom.id α) a = a
-- Mathlib.Order.InitialSeg
/-- Restrict the codomain of an initial segment  -/
InitialSeg.codRestrict : {α : Type u_1} →
  {β : Type u_2} →
    {r : α → α → Prop} →
      {s : β → β → Prop} →
        (p : Set β) → (f : InitialSeg r s) → (∀ (a : α), f a ∈ p) → InitialSeg r (Subrel s fun x => x ∈ p)
-- Mathlib.Condensed.Discrete.Module
CondensedMod.LocallyConstant.instFullSheafCompHausCoherentTopologyTypeConstantSheaf : (CategoryTheory.constantSheaf (CategoryTheory.coherentTopology CompHaus) (Type (u + 1))).Full
-- Init.Data.Float.Float
/-- Computes the base-2 exponential `2^x` of a floating-point number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`exp2`.
 -/
Float.exp2 : Float → Float
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- The main loop of `isMVarSwap`. Returning `none` corresponds to a failure.  -/
_private.Mathlib.Tactic.Widget.LibraryRewrite.0.Mathlib.Tactic.LibraryRewrite.isMVarSwap.go : Lean.Expr → Lean.Expr → List (Lean.MVarId × Lean.MVarId) → Option (List (Lean.MVarId × Lean.MVarId))
-- Mathlib.Topology.MetricSpace.HausdorffDimension
Real.dimH_of_mem_nhds : ∀ {E : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {x : E} {s : Set E},
  s ∈ nhds x → dimH s = ↑(Module.finrank ℝ E)
-- Init.Data.Array.Attach
Array.count_attach : ∀ {α : Type u_1} [inst : BEq α] {xs : Array α} {a : { x // x ∈ xs }}, Array.count a xs.attach = Array.count (↑a) xs
-- Mathlib.Tactic.Widget.Calc
CalcParams.mk : SelectInsertParams → Bool → ℕ → CalcParams
-- Mathlib.Order.Filter.Basic
Filter.mem_biInf_of_directed : ∀ {α : Type u} {β : Type v} {f : β → Filter α} {s : Set β},
  DirectedOn (f ⁻¹'o fun x1 x2 => x1 ≥ x2) s → s.Nonempty → ∀ {t : Set α}, t ∈ ⨅ i ∈ s, f i ↔ ∃ i ∈ s, t ∈ f i
-- Mathlib.RingTheory.PowerSeries.Restricted
PowerSeries.isRestricted_abs_iff : ∀ {R : Type u_1} [inst : NormedRing R] (c : ℝ) (f : PowerSeries R),
  PowerSeries.IsRestricted |c| f ↔ PowerSeries.IsRestricted c f
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.toCoalgEquiv_eq_coe : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (f : A ≃ₐc[R] B), f.toCoalgEquiv = ↑f
-- Mathlib.Topology.Instances.CantorSet
cantorToTernary.eq_1 : ∀ (x : ℝ), cantorToTernary x = Stream'.map (fun x => bif x then 2 else 0) (cantorToBinary x)
-- Mathlib.CategoryTheory.Monoidal.Internal.Module
/-- The equivalence `Mon (ModuleCat R) ≌ AlgCat R`
is naturally compatible with the forgetful functors to `ModuleCat R`.
 -/
ModuleCat.monModuleEquivalenceAlgebraForget : {R : Type u} →
  [inst : CommRing R] →
    ModuleCat.MonModuleEquivalenceAlgebra.functor.comp (CategoryTheory.forget₂ (AlgCat R) (ModuleCat R)) ≅
      CategoryTheory.Mon.forget (ModuleCat R)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.commRingNorm : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr →
  Lean.Meta.Grind.Arith.CommRing.RingExpr → Lean.Grind.CommRing.Poly → Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof
-- Init.Data.List.Nat.Basic
List.le_max?_get_of_mem : ∀ {l : List ℕ} {a : ℕ} (h : a ∈ l), a ≤ l.max?.get ⋯
-- Mathlib.Data.Set.Sups
Set.empty_sups : ∀ {α : Type u_2} [inst : SemilatticeSup α] {t : Set α}, ∅ ⊻ t = ∅
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.Functor.OplaxMonoidal.η_of_cartesianMonoidalCategory : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.OplaxMonoidal],
  CategoryTheory.Functor.OplaxMonoidal.η F = CategoryTheory.CartesianMonoidalCategory.terminalComparison F
-- Mathlib.Algebra.BigOperators.Intervals
Finset.sum_fin_Icc_eq_sum_nat_Icc : ∀ {α : Type u_1} [inst : AddCommMonoid α] {n : ℕ} (a b : Fin n) (f : Fin n → α),
  ∑ i ∈ Finset.Icc a b, f i = ∑ i ∈ Finset.Icc ↑a ↑b, if h : i < n then f ⟨i, h⟩ else 0
-- Mathlib.CategoryTheory.Preadditive.Mat
/-- The identity functor induces the identity functor on matrix categories.
 -/
CategoryTheory.Functor.mapMatId : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (CategoryTheory.Functor.id C).mapMat_ ≅ CategoryTheory.Functor.id (CategoryTheory.Mat_ C)
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Measurable.sqrt : ∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → ℝ}, Measurable f → Measurable fun x => √(f x)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.nil_append_iff : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk u v} {q : G.Walk v w}, (p.append q).Nil ↔ p.Nil ∧ q.Nil
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.WithLowerSet.ofLowerSet_inj : ∀ {α : Type u_1} {a b : Topology.WithLowerSet α},
  Topology.WithLowerSet.ofLowerSet a = Topology.WithLowerSet.ofLowerSet b ↔ a = b
-- Mathlib.CategoryTheory.Monoidal.Internal.Limits
CategoryTheory.Mon.limitConeIsLimit_lift_hom : ∀ {J : Type w} [inst : CategoryTheory.Category.{v_1, w} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (F : CategoryTheory.Functor J (CategoryTheory.Mon C))
  (c : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Mon.forget C))) (hc : CategoryTheory.Limits.IsLimit c)
  (s : CategoryTheory.Limits.Cone F),
  ((CategoryTheory.Mon.limitConeIsLimit F c hc).lift s).hom = hc.lift ((CategoryTheory.Mon.forget C).mapCone s)
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
complEDS_even : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R) (k m : ℤ),
  complEDS b c d k (2 * m) = complEDS b c d k m * complEDS₂ b c d (m * k)
-- Mathlib.LinearAlgebra.ExteriorPower.Basis
/-- If `b` is a basis of `M` indexed by a linearly ordered type `I` and `B` is the corresponding
basis of the `n`th exterior power of `M`, indexed by the set of finsets `s` of `I` of cardinality
`n`, then the coordinate function of `B` at `s` is the linear form on the `n`th exterior power
defined by `b` and `s` in `exteriorPower.ιMultiDual`.  -/
exteriorPower.basis_coord : ∀ (R : Type u_1) {M : Type u_3} (n : ℕ) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {I : Type u_5} [inst_3 : LinearOrder I] (b : Module.Basis I R M) (s : ↑(Set.powersetCard I n)),
  (Module.Basis.exteriorPower n b).coord s = exteriorPower.ιMultiDual R n b s
-- Lean.Environment
Lean.ConstantKind.opaque : Lean.ConstantKind
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- Inner loop for `delabParams`, collecting binders.
Invariants:
- The current expression is a forall.
- It has a name that's not inaccessible.
- It has a name that hasn't been used yet.
 -/
_private.Lean.PrettyPrinter.Delaborator.Builtins.0.Lean.PrettyPrinter.Delaborator.delabForallParamsWithSignature.delabParamsAux : {α : Type} →
  (Lean.TSyntaxArray `Lean.Parser.Term.bracketedBinder → Lean.Term → Lean.PrettyPrinter.Delaborator.DelabM α) →
    Lean.NameSet →
      Lean.TSyntaxArray `Lean.Parser.Term.bracketedBinder → Array Lean.Ident → Lean.PrettyPrinter.Delaborator.DelabM α
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.compl_mem_iff : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {L : BooleanSubalgebra α} {a : α}, aᶜ ∈ L ↔ a ∈ L
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.descOpcycles.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) {A : C} (k k_1 : S.X₂ ⟶ A) (e_k : k = k_1)
  (hk : CategoryTheory.CategoryStruct.comp S.f k = 0) [inst_2 : S.HasRightHomology],
  S.descOpcycles k hk = S.descOpcycles k_1 ⋯
-- Mathlib.AlgebraicGeometry.ValuativeCriterion
/-- The **valuative criterion** for proper morphisms.  -/
AlgebraicGeometry.IsProper.of_valuativeCriterion : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.QuasiCompact f] [AlgebraicGeometry.QuasiSeparated f]
  [AlgebraicGeometry.LocallyOfFiniteType f], AlgebraicGeometry.ValuativeCriterion f → AlgebraicGeometry.IsProper f
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.refl_trans : ∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
  {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂),
  (LinearEquiv.refl R M).trans e = e
-- Mathlib.Order.Minimal
MinimalFor.minimal_of_strictMonoOn : ∀ {α : Type u_2} {β : Type u_3} {P : α → Prop} {x : α} [inst : Preorder α] [inst_1 : Preorder β] {g : α → β},
  StrictMonoOn g (Set.ofPred P) → MinimalFor P g x → Minimal P x
-- Mathlib.Data.Fintype.Basic
Unit.fintype : Fintype Unit
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
_private.Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme.0.AlgebraicGeometry.Scheme.IdealSheafData.range_glueData_ι : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens),
  Set.range ⇑(I.glueData.ι U) = ↑((TopologicalSpace.Opens.map I.gluedTo.base).obj ↑U)
-- Mathlib.Topology.Clopen
isClopen_of_disjoint_cover_open : ∀ {X : Type u} [inst : TopologicalSpace X] {a b : Set X},
  Set.univ ⊆ a ∪ b → IsOpen a → IsOpen b → Disjoint a b → IsClopen a
-- Mathlib.Algebra.Order.Star.Basic
star_lt_star_iff : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  {x y : R}, star x < star y ↔ x < y
-- Mathlib.Topology.Algebra.Module.Equiv
/-- Equivalence given by a block lower diagonal matrix. `e` and `e'` are diagonal square blocks,
and `f` is a rectangular block below the diagonal.  -/
ContinuousLinearEquiv.skewProd : {R : Type u_1} →
  [inst : Semiring R] →
    {M : Type u_2} →
      [inst_1 : TopologicalSpace M] →
        [inst_2 : AddCommGroup M] →
          {M₂ : Type u_3} →
            [inst_3 : TopologicalSpace M₂] →
              [inst_4 : AddCommGroup M₂] →
                {M₃ : Type u_4} →
                  [inst_5 : TopologicalSpace M₃] →
                    [inst_6 : AddCommGroup M₃] →
                      {M₄ : Type u_5} →
                        [inst_7 : TopologicalSpace M₄] →
                          [inst_8 : AddCommGroup M₄] →
                            [inst_9 : Module R M] →
                              [inst_10 : Module R M₂] →
                                [inst_11 : Module R M₃] →
                                  [inst_12 : Module R M₄] →
                                    [IsTopologicalAddGroup M₄] →
                                      (M ≃L[R] M₂) → (M₃ ≃L[R] M₄) → (M →L[R] M₄) → (M × M₃) ≃L[R] M₂ × M₄
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.preΨ_zero : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R), W.preΨ 0 = 0
-- Mathlib.Topology.Algebra.Group.Basic
AddUnits.instLocallyCompactSpaceOfT1SpaceOfContinuousAdd : ∀ {α : Type u} [inst : AddMonoid α] [inst_1 : TopologicalSpace α] [T1Space α] [ContinuousAdd α] [LocallyCompactSpace α],
  LocallyCompactSpace (AddUnits α)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isEmpty_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α Unit cmp} [Std.TransCmp cmp],
  t.WF → ∀ {l : List α}, (t.insertManyIfNewUnit l).isEmpty = (t.isEmpty && l.isEmpty)
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.le_def : ∀ {ι : Type u_1} (I J : BoxIntegral.Box ι), I ≤ J ↔ ∀ x ∈ I, x ∈ J
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
CategoryTheory.Limits.inr_inr_pushoutRightPushoutInlIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (f' : Y ⟶ W)
  [inst_1 : CategoryTheory.Limits.HasPushout f g]
  [inst_2 : CategoryTheory.Limits.HasPushout f' (CategoryTheory.Limits.pushout.inl f g)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f' (CategoryTheory.Limits.pushout.inl f g))
        (CategoryTheory.Limits.pushoutRightPushoutInlIso f g f').hom) =
    CategoryTheory.Limits.pushout.inr (CategoryTheory.CategoryStruct.comp f f') g
-- Mathlib.RepresentationTheory.Continuous.Basic
/-- A continuous intertwining map between two continuous representations is an intertwining map
which is also continuous.  -/
ContIntertwiningMap : {R : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Monoid G] →
          [inst_1 : Ring R] →
            [inst_2 : AddCommGroup V] →
              [inst_3 : TopologicalSpace V] →
                [inst_4 : IsTopologicalAddGroup V] →
                  [inst_5 : Module R V] →
                    [inst_6 : AddCommGroup W] →
                      [inst_7 : TopologicalSpace W] →
                        [inst_8 : IsTopologicalAddGroup W] →
                          [inst_9 : Module R W] →
                            ContRepresentation R G V → ContRepresentation R G W → Type (max u_3 u_4)
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
/-- If `G.IsBipartiteWith s t` and `w ∈ t`, then the neighbor set of `w` is the set of vertices in
`s` adjacent to `w` in `G`.  -/
SimpleGraph.isBipartiteWith_neighborSet' : ∀ {V : Type u_1} {w : V} {G : SimpleGraph V} {s t : Set V},
  G.IsBipartiteWith s t → w ∈ t → G.neighborSet w = {v | v ∈ s ∧ G.Adj v w}
-- Init.Data.UInt.Lemmas
UInt32.ofNat_le_iff : ∀ {n : UInt32} {m : ℕ}, m < UInt32.size → (UInt32.ofNat m ≤ n ↔ m ≤ n.toNat)
-- Mathlib.Order.SymmDiff
symmDiff_symmDiff_right : ∀ {α : Type u_2} [inst : GeneralizedBooleanAlgebra α] (a b c : α),
  symmDiff a (symmDiff b c) = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ c \ (a ⊔ b) ⊔ a ⊓ b ⊓ c
-- Mathlib.NumberTheory.WellApproximable
approxOrderOf.image_pow_subset : ∀ {A : Type u_1} [inst : SeminormedCommGroup A] {m : ℕ} (δ : ℝ) (n : ℕ),
  0 < m → (fun y => y ^ m) '' approxOrderOf A (n * m) δ ⊆ approxOrderOf A n (↑m * δ)
-- Mathlib.Geometry.Manifold.VectorBundle.Hom
/-- Consider `C^n` maps `v : M → E₁` and `w : M → E₂` to vector bundles, over a base map
`b : M → B`, and bilinear maps `ψ m : E₁ (b m) → E₂ (b m) → E₃ (b m)` depending smoothly on `m`.
One can apply `ψ  m` to `v m` and `w m`, and the resulting map is `C^n`.

We give here a version of this statement at a point.  -/
ContMDiffAt.clm_bundle_apply₂ : ∀ {𝕜 : Type u_1} {B : Type u_2} {F₁ : Type u_3} {F₂ : Type u_4} {F₃ : Type u_5} {M : Type u_6}
  [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {E₁ : B → Type u_7} [inst_1 : (x : B) → AddCommGroup (E₁ x)]
  [inst_2 : (x : B) → Module 𝕜 (E₁ x)] [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁]
  [inst_5 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [inst_6 : (x : B) → TopologicalSpace (E₁ x)] {E₂ : B → Type u_8}
  [inst_7 : (x : B) → AddCommGroup (E₂ x)] [inst_8 : (x : B) → Module 𝕜 (E₂ x)] [inst_9 : NormedAddCommGroup F₂]
  [inst_10 : NormedSpace 𝕜 F₂] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_12 : (x : B) → TopologicalSpace (E₂ x)] {E₃ : B → Type u_9} [inst_13 : (x : B) → AddCommGroup (E₃ x)]
  [inst_14 : (x : B) → Module 𝕜 (E₃ x)] [inst_15 : NormedAddCommGroup F₃] [inst_16 : NormedSpace 𝕜 F₃]
  [inst_17 : TopologicalSpace (Bundle.TotalSpace F₃ E₃)] [inst_18 : (x : B) → TopologicalSpace (E₃ x)] {EB : Type u_10}
  [inst_19 : NormedAddCommGroup EB] [inst_20 : NormedSpace 𝕜 EB] {HB : Type u_11} [inst_21 : TopologicalSpace HB]
  {IB : ModelWithCorners 𝕜 EB HB} [inst_22 : TopologicalSpace B] [inst_23 : ChartedSpace HB B] {EM : Type u_12}
  [inst_24 : NormedAddCommGroup EM] [inst_25 : NormedSpace 𝕜 EM] {HM : Type u_13} [inst_26 : TopologicalSpace HM]
  {IM : ModelWithCorners 𝕜 EM HM} [inst_27 : TopologicalSpace M] [inst_28 : ChartedSpace HM M]
  [inst_29 : FiberBundle F₁ E₁] [inst_30 : VectorBundle 𝕜 F₁ E₁] [inst_31 : FiberBundle F₂ E₂]
  [inst_32 : VectorBundle 𝕜 F₂ E₂] [inst_33 : FiberBundle F₃ E₃] [inst_34 : ⋯], ⋯
-- Lean.Parser.Types
Lean.Parser.ParserCache.mk.injEq : ∀ (tokenCache : Lean.Parser.TokenCacheEntry)
  (parserCache : Std.HashMap Lean.Parser.ParserCacheKey Lean.Parser.ParserCacheEntry)
  (tokenCache_1 : Lean.Parser.TokenCacheEntry)
  (parserCache_1 : Std.HashMap Lean.Parser.ParserCacheKey Lean.Parser.ParserCacheEntry),
  ({ tokenCache := tokenCache, parserCache := parserCache } =
      { tokenCache := tokenCache_1, parserCache := parserCache_1 }) =
    (tokenCache = tokenCache_1 ∧ parserCache = parserCache_1)
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIsTerminalIso'_hom_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.MonoidalClosed C]
  (X : CategoryTheory.Arrow C) {I : C} (i : CategoryTheory.Limits.IsInitial I) {T : C}
  (t : CategoryTheory.Limits.IsTerminal T),
  (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIsTerminalIso' X i t).hom.right =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.right
        (CategoryTheory.SemiCartesianMonoidalCategory.isTerminalTensorUnit.from T))
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.right).hom