mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.GroupAction.Basic
AddAction.stabilizerEquivStabilizer_trans : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {g h k : G} {a b c : α} (hg : b = g +ᵥ a)
  (hh : c = h +ᵥ b) (hk : c = k +ᵥ a),
  k = h + g →
    (AddAction.stabilizerEquivStabilizer hg).trans (AddAction.stabilizerEquivStabilizer hh) =
      AddAction.stabilizerEquivStabilizer hk
-- Mathlib.NumberTheory.NumberField.House
_private.Mathlib.NumberTheory.NumberField.House.0.NumberField.house.asiegel.eq_1 : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] {α : Type u_2} {β : Type u_3}
  (a : Matrix α β (NumberField.RingOfIntegers K)) (k : α × (K →+* ℂ)) (l : β × (K →+* ℂ)),
  NumberField.house.asiegel✝ K a k l = NumberField.house.a'✝ K a k.1 l.1 l.2 k.2
-- Mathlib.Order.Hom.Bounded
BoundedOrderHomClass.toBotHomClass : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : LE α] [inst_2 : LE β]
  [inst_3 : BoundedOrder α] [inst_4 : BoundedOrder β] [BoundedOrderHomClass F α β], BotHomClass F α β
-- Mathlib.GroupTheory.Congruence.Basic
Con.congr.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {c : Con M} {d : Con N} (e : M ≃* N)
  (h : c = Con.comap ⇑e ⋯ d), Con.congr e h = { toEquiv := Quotient.congr ↑e ⋯, map_mul' := ⋯ }
-- Mathlib.Data.Nat.Sqrt
Nat.le_sqrt : ∀ {m n : ℕ}, m ≤ n.sqrt ↔ m * m ≤ n
-- Std.Data.Iterators.Combinators.Monadic.Zip
Std.Iterators.Types.Zip.instFinite₂ : ∀ {m : Type w → Type w'} {α₁ β₁ : Type w} [inst : Std.Iterator α₁ m β₁] {α₂ β₂ : Type w} [inst_1 : Std.Iterator α₂ m β₂]
  [inst_2 : Monad m] [Std.Iterators.Productive α₁ m] [Std.Iterators.Finite α₂ m],
  Std.Iterators.Finite (Std.Iterators.Types.Zip α₁ m α₂ β₂) m
-- Init.Data.Order.Ord
Std.TransCmp.lt_of_eq_of_lt : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {a b c : α},
  cmp a b = Ordering.eq → cmp b c = Ordering.lt → cmp a c = Ordering.lt
-- Init.Data.List.Lemmas
List.insert_of_not_mem : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {l : List α}, a ∉ l → List.insert a l = a :: l
-- Init.Data.Int.Order
Int.lt_of_lt_of_le : ∀ {a b c : ℤ}, a < b → b ≤ c → a < c
-- Std.Http.Data.Body.Stream
/-- A single blocked consumer waiting for a producer.
 -/
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Channel.State.pendingConsumer : Std.Http.Body.Channel.State✝ → Option Std.Http.Body.Channel.Consumer✝
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Class
/-- A predicate that indicates whether a formula can soundly be passed into performRatAdd.  -/
Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRatAdd : {α : outParam (Type u)} →
  {β : outParam (Type v)} →
    {inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β} →
      {σ : Type w} →
        {inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ} →
          [self : Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ] → σ → Prop
-- Mathlib.Order.Interval.Set.Image
StrictMonoOn.mapsTo_Ioc : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : PartialOrder α] [inst_1 : Preorder β] {a b : α},
  StrictMonoOn f (Set.Icc a b) → Set.MapsTo f (Set.Ioc a b) (Set.Ioc (f a) (f b))
-- Mathlib.FieldTheory.Fixed
AlgHom.card_le : ∀ {F : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K]
  [inst_3 : FiniteDimensional F K], Fintype.card (K →ₐ[F] K) ≤ Module.finrank F K
-- Mathlib.CategoryTheory.Preadditive.Schur
/-- **Schur's lemma** for `𝕜`-linear categories:
if hom spaces are finite dimensional, then the hom space between simples is at most 1-dimensional.

See `finrank_hom_simple_simple_eq_one_iff` and `finrank_hom_simple_simple_eq_zero_iff` below
for the refinements when we know whether or not the simples are isomorphic.
 -/
CategoryTheory.finrank_hom_simple_simple_le_one : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (𝕜 : Type u_2)
  [inst_2 : Field 𝕜] [IsAlgClosed 𝕜] [inst_4 : CategoryTheory.Linear 𝕜 C] [CategoryTheory.Limits.HasKernels C] (X Y : C)
  [FiniteDimensional 𝕜 (X ⟶ X)] [CategoryTheory.Simple X] [CategoryTheory.Simple Y], Module.finrank 𝕜 (X ⟶ Y) ≤ 1
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Functor.isLeftAdjoint_comp_iff_right : ∀ {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) [F.IsEquivalence], (F.comp G).IsLeftAdjoint ↔ G.IsLeftAdjoint
-- Std.Time.Date.Unit.Week
Std.Time.Week.OfYear.instDecidableLeOrdinal : {x y : Std.Time.Week.OfYear.Ordinal} → Decidable (x ≤ y)
-- Lean.Meta.Tactic.Grind.Split
Lean.Meta.Grind.instHasAnchorSplitCandidateWithAnchor : Lean.Meta.Grind.HasAnchor Lean.Meta.Grind.SplitCandidateWithAnchor
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.firstReturn.eq_1 : ∀ (p : DyckWord),
  p.firstReturn =
    List.findIdx
      (fun i => decide (List.count DyckStep.U (List.take (i + 1) ↑p) = List.count DyckStep.D (List.take (i + 1) ↑p)))
      (List.range (↑p).length)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_inter!_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k fallback : α},
        Std.DTreeMap.Internal.Impl.contains k m₁ = false → (m₁.inter! m₂).getKeyD k fallback = fallback
-- Mathlib.GroupTheory.Coset.Card
AddSubgroup.card_dvd_of_injective : ∀ {α : Type u_1} [inst : AddGroup α] {H : Type u_2} [inst_1 : AddGroup H] (f : α →+ H),
  Function.Injective ⇑f → Nat.card α ∣ Nat.card H
-- Mathlib.Algebra.Opposites
AddOpposite.forall : ∀ {α : Type u_1} {p : αᵃᵒᵖ → Prop}, (∀ (a : αᵃᵒᵖ), p a) ↔ ∀ (a : α), p (AddOpposite.op a)
-- Mathlib.Order.Hom.Basic
/-- Function application `fun f => f a` (for fixed `a`) is a monotone function from the
monotone function space `α →o β` to `β`. See also `Pi.evalOrderHom`.  -/
OrderHom.apply : {α : Type u_2} → {β : Type u_3} → [inst : Preorder α] → [inst_1 : Preorder β] → α → (α →o β) →o β
-- Mathlib.Order.CompleteBooleanAlgebra
CompleteDistribLattice.toHNot : {α : Type u_1} → [self : CompleteDistribLattice α] → HNot α
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepSets.piiUnionInter_of_notMem : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {π : ι → Set (Set Ω)} {a : ι}
  {S : Finset ι}, ProbabilityTheory.iIndepSets π μ → a ∉ S → ProbabilityTheory.IndepSets (piiUnionInter π ↑S) (π a) μ
-- Lean.Language.Lean.Types
Lean.Language.Lean.CommandParsedSnapshot.brecOn_3.eq : ∀ {motive_1 : Lean.Language.Lean.CommandParsedSnapshot → Sort u}
  {motive_2 : Option (Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot) → Sort u}
  {motive_3 : Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot → Sort u}
  {motive_4 : Task Lean.Language.Lean.CommandParsedSnapshot → Sort u}
  (t : Task Lean.Language.Lean.CommandParsedSnapshot)
  (F_1 : (t : Lean.Language.Lean.CommandParsedSnapshot) → t.below → motive_1 t)
  (F_2 :
    (t : Option (Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot)) →
      Lean.Language.Lean.CommandParsedSnapshot.below_1 t → motive_2 t)
  (F_3 :
    (t : Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot) →
      Lean.Language.Lean.CommandParsedSnapshot.below_2 t → motive_3 t)
  (F_4 :
    (t : Task Lean.Language.Lean.CommandParsedSnapshot) →
      Lean.Language.Lean.CommandParsedSnapshot.below_3 t → motive_4 t),
  Lean.Language.Lean.CommandParsedSnapshot.brecOn_3 t F_1 F_2 F_3 F_4 =
    F_4 t (Lean.Language.Lean.CommandParsedSnapshot.brecOn_3.go t F_1 F_2 F_3 F_4).2
-- Std.Http.Internal.String
_private.Std.Http.Internal.String.0.Std.Http.Internal.UnquoteState.done : String → Std.Http.Internal.UnquoteState✝
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.piFinSuccAbove_apply : ∀ {n : ℕ} (α : Fin (n + 1) → Type u_8) [inst : (i : Fin (n + 1)) → MeasurableSpace (α i)] (i : Fin (n + 1)),
  ⇑(MeasurableEquiv.piFinSuccAbove α i) = ⇑(Fin.insertNthEquiv α i).symm
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_zero : ∀ {b : ℝ}, Real.logb b 0 = 0
-- Mathlib.Algebra.Lie.Solvable
LieAlgebra.radical_eq_top_of_isSolvable : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [LieAlgebra.IsSolvable L], LieAlgebra.radical R L = ⊤
-- Batteries.Data.String.Lemmas
String.all_iff : ∀ (s : String) (p : Char → Bool), String.Legacy.all s p = true ↔ ∀ c ∈ s.toList, p c = true
-- Init.Data.String.Substring
/-- {}
Copies the region of the underlying string pointed to by a substring into a fresh string.
 -/
Substring.Raw.toString : Substring.Raw → String
-- Lean.Meta.Sym.SymM
/-- Restores the `SymM` invariants enabled in the current configuration.
The final `unfoldReducible` is needed because `foldProjs` can introduce fresh reducible
constants: `mkProjection` recovers structure parameters from `inferType`, and those types
come from environment signatures that were never preprocessed.
 -/
_private.Lean.Meta.Sym.SymM.0.Lean.Meta.Sym.repairShareViolation : Lean.Expr → Lean.Meta.Sym.SymM Lean.Expr
-- Lean.Parser.Basic
Lean.Parser.antiquotExpr : Lean.Parser.Parser
-- Mathlib.SetTheory.ZFC.VonNeumann
ZFSet.vonNeumann_subset_vonNeumann_iff : ∀ {a b : Ordinal.{u}}, ZFSet.vonNeumann a ⊆ ZFSet.vonNeumann b ↔ a ≤ b
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
ContMDiffAt.eq_1 : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H')
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] (n : WithTop ℕ∞) (f : M → M') (x : M),
  ContMDiffAt I I' n f x = ContMDiffWithinAt I I' n f Set.univ x
-- Mathlib.MeasureTheory.Measure.Real
/-- **Alias** of `MeasureTheory.measureReal_eq_measureReal_smaller_of_between_null_sdiff`. -/
MeasureTheory.measureReal_eq_measureReal_smaller_of_between_null_diff : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ s₃ : Set α},
  s₁ ⊆ s₂ →
    s₂ ⊆ s₃ →
      μ.real (s₃ \ s₁) = 0 →
        autoParam (μ (s₃ \ s₁) ≠ ⊤) MeasureTheory.measureReal_eq_measureReal_smaller_of_between_null_sdiff._auto_1 →
          μ.real s₁ = μ.real s₂
-- Mathlib.CategoryTheory.Presentable.Limits
CategoryTheory.Functor.Accessible.Limits.isColimitMapCocone.injective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} K]
  {F : CategoryTheory.Functor K (CategoryTheory.Functor C (Type w'))} (c : CategoryTheory.Limits.Cone F)
  (hc : (Y : C) → CategoryTheory.Limits.IsLimit (((CategoryTheory.evaluation C (Type w')).obj Y).mapCone c))
  (κ : Cardinal.{w}) [inst_2 : Fact κ.IsRegular],
  HasCardinalLT (CategoryTheory.Arrow K) κ →
    ∀ {J : Type w} [inst_3 : CategoryTheory.SmallCategory J] [CategoryTheory.IsCardinalFiltered J κ]
      {X : CategoryTheory.Functor J C} (cX : CategoryTheory.Limits.Cocone X)
      (hF : (k : K) → CategoryTheory.Limits.IsColimit ((F.obj k).mapCocone cX)) (j : J) (x₁ x₂ : c.pt.obj (X.obj j)),
      (CategoryTheory.ConcreteCategory.hom (c.pt.map (cX.ι.app j))) x₁ =
          (CategoryTheory.ConcreteCategory.hom (c.pt.map (cX.ι.app j))) x₂ →
        ∃ j' α,
          (CategoryTheory.ConcreteCategory.hom (c.pt.map (X.map α))) x₁ =
            (CategoryTheory.ConcreteCategory.hom (c.pt.map (X.map α))) x₂
-- Mathlib.RingTheory.Kaehler.Basic
KaehlerDifferential.map_D : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (A : Type u_2)
  (B : Type u_3) [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra R A] [inst_6 : Algebra A B]
  [inst_7 : Algebra S B] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R A B] [inst_10 : IsScalarTower R S B]
  [inst_11 : SMulCommClass S A B] (x : A),
  (KaehlerDifferential.map R S A B) ((KaehlerDifferential.D R A) x) = (KaehlerDifferential.D S B) ((algebraMap A B) x)
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.SymmetricCategory.toBraidedCategory : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {inst_1 : CategoryTheory.MonoidalCategory C} →
      [self : CategoryTheory.SymmetricCategory C] → CategoryTheory.BraidedCategory C
-- Mathlib.RingTheory.WittVector.Compare
/-- `fromPadicInt` uses `WittVector.lift` to lift `TruncatedWittVector.zmodEquivTrunc`
composed with `PadicInt.toZModPow` to a ring hom `ℤ_[p] →+* 𝕎 (ZMod p)`.
 -/
WittVector.fromPadicInt : (p : ℕ) → [hp : Fact (Nat.Prime p)] → ℤ_[p] →+* WittVector p (ZMod p)
-- Mathlib.Algebra.Lie.Weights.IsSimple
_private.Mathlib.Algebra.Lie.Weights.IsSimple.0.LieAlgebra.IsKilling.chi_not_in_q_aux : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [inst_4 : FiniteDimensional K L] [inst_5 : LieAlgebra.IsKilling K L] {H : LieSubalgebra K L}
  [inst_6 : H.IsCartanSubalgebra] [inst_7 : LieModule.IsTriangularizable K (↥H) L] (q : Submodule K (Module.Dual K ↥H)),
  (∀ (i : ↥LieSubalgebra.root), q ∈ Module.End.invtSubmodule ↑((LieAlgebra.IsKilling.rootSystem H).reflection i)) →
    ∀ (χ : LieModule.Weight K (↥H) L) (x_χ m_α : L),
      x_χ ∈ LieModule.genWeightSpace L ⇑χ →
        ∀ (α : LieModule.Weight K (↥H) L),
          LieModule.Weight.toLinear K (↥H) L α ∈ q →
            α.IsNonZero →
              LieModule.Weight.toLinear K (↥H) L χ + LieModule.Weight.toLinear K (↥H) L α ≠ 0 →
                LieModule.Weight.toLinear K (↥H) L χ - LieModule.Weight.toLinear K (↥H) L α ≠ 0 →
                  LieModule.Weight.toLinear K (↥H) L χ ≠ 0 →
                    ∀ (m_pos m_neg : L),
                      ∀ y ∈ LieAlgebra.corootSpace ⇑α,
                        ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, ↑y⁆ →
                          ⁅x_χ, m_pos⁆ ∈ LieModule.genWeightSpace L (⇑χ + ⇑α) →
                            ⁅x_χ, m_neg⁆ ∈ LieModule.genWeightSpace L (⇑χ - ⇑α) →
                              LieModule.Weight.toLinear K (↥H) L χ ∉ q →
                                ⁅x_χ, m_α⁆ ∈ ⨆ α, LieAlgebra.IsKilling.sl2SubmoduleOfRoot ⋯
-- Mathlib.CategoryTheory.MorphismProperty.Ind
/-- **Alias** of `CategoryTheory.MorphismProperty.PreIndSpreads.exists_isPushout`. -/
CategoryTheory.MorphismProperty.exists_isPushout_of_isFiltered : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.MorphismProperty C}
  [self : P.PreIndSpreads] {J : Type w} [inst_1 : CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J]
  {D : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone D} (x : CategoryTheory.Limits.IsColimit c) {T : C}
  (f : c.pt ⟶ T), P f → ∃ j T' f' g, CategoryTheory.IsPushout (c.ι.app j) f' f g ∧ P f'
-- Mathlib.Data.Sum.Basic
Sum.LiftRel.isRight_right : ∀ {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : α → γ → Prop} {s : β → δ → Prop} {y : γ ⊕ δ} {b : β},
  Sum.LiftRel r s (Sum.inr b) y → y.isRight = true
-- Mathlib.Data.Seq.Basic
Stream'.Seq.set_cons_zero : ∀ {α : Type u} (hd : α) (tl : Stream'.Seq α) (hd' : α), (Stream'.Seq.cons hd tl).set 0 hd' = Stream'.Seq.cons hd' tl
-- Init.Data.SInt.Lemmas
Int8.neg_sub : ∀ {a b : Int8}, -(a - b) = b - a
-- Mathlib.LinearAlgebra.Prod
LinearMap.comap_prod_prod : ∀ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module R M₂]
  [inst_6 : Module R M₃] (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) (p : Submodule R M₂) (q : Submodule R M₃),
  Submodule.comap (f.prod g) (p.prod q) = Submodule.comap f p ⊓ Submodule.comap g q
-- Mathlib.Topology.MetricSpace.Thickening
/-- For the equality, see `thickening_thickening`.  -/
Metric.thickening_thickening_subset : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (ε δ : ℝ) (s : Set α),
  Metric.thickening ε (Metric.thickening δ s) ⊆ Metric.thickening (ε + δ) s
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.inv_rpow : ∀ (x : ENNReal) (y : ℝ), x⁻¹ ^ y = (x ^ y)⁻¹
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.instNontrivial : ∀ {σ : Type u_1} {R : Type u_2} [Nontrivial R], Nontrivial (MvPowerSeries σ R)
-- Mathlib.CategoryTheory.Monoidal.NaturalTransformation
CategoryTheory.NatTrans.IsMonoidal.instHomFunctorAssociator : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] {E : Type u₃}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.MonoidalCategory E] {E' : Type u₄}
  [inst_6 : CategoryTheory.Category.{v₄, u₄} E'] [inst_7 : CategoryTheory.MonoidalCategory E']
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) (H : CategoryTheory.Functor E E')
  [inst_8 : F.LaxMonoidal] [inst_9 : G.LaxMonoidal] [inst_10 : H.LaxMonoidal],
  CategoryTheory.NatTrans.IsMonoidal (F.associator G H).hom
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.base_affine_hasPullback : ∀ {C : CommRingCat} {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec C)
  (g : Y ⟶ AlgebraicGeometry.Spec C), CategoryTheory.Limits.HasPullback f g
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.instCategory : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor A B} →
              {G : CategoryTheory.Functor C B} →
                (X : Type u₄) →
                  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] →
                    CategoryTheory.Category.{max (max u₄ v₃) v₁, max (max (max (max (max (max u₄ u₃) u₁) v₄) v₃) v₂) v₁}
                      (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instInhabitedEMatchDiagNode.default : Lean.Meta.Grind.EMatchDiagNode
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.apply_skipSuffixWhile_bool_eq_false : ∀ {p : Char → Bool} {s : String} {h : s.skipSuffixWhile p ≠ s.startPos},
  p (((s.skipSuffixWhile p).prev h).get ⋯) = false
-- Lean.Meta.Sym.Canon
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.instReprShouldCanonResult : Repr Lean.Meta.Sym.Canon.ShouldCanonResult✝
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.sigmaConst_obj_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C] (X : C)
  {X_1 Y : Type w} (f : X_1 ⟶ Y),
  (CategoryTheory.Limits.sigmaConst.obj X).map f =
    CategoryTheory.Limits.Sigma.map' ⇑(CategoryTheory.ConcreteCategory.hom f) fun x =>
      CategoryTheory.CategoryStruct.id X
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.coe_incl' : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (L' : LieSubalgebra R L),
  ⇑L'.incl' = Subtype.val
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get_insertMany_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    ∀ {v : β},
      List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
        (k, v) ∈ l →
          ∀ {h' : k' ∈ Std.ExtDTreeMap.Const.insertMany t l},
            Std.ExtDTreeMap.Const.get (Std.ExtDTreeMap.Const.insertMany t l) k' h' = v
-- Mathlib.RingTheory.Kaehler.Basic
KaehlerDifferential.linearCombination_surjective : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  Function.Surjective ⇑(Finsupp.linearCombination S ⇑(KaehlerDifferential.D R S))
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.refl_symm : ∀ {α : Type u} [inst : UniformSpace α], (UniformEquiv.refl α).symm = UniformEquiv.refl α
-- Init.Data.Order.Ord
Option.instTransOrd : ∀ {α : Type u_1} [inst : Ord α] [Std.TransOrd α], Std.TransOrd (Option α)
-- Mathlib.Topology.PartialHomeomorph.Basic
Topology.IsEmbedding.toPartialHomeomorph_source : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y)
  (h : Topology.IsEmbedding f) [inst_2 : Nonempty X], (Topology.IsEmbedding.toPartialHomeomorph f h).source = Set.univ
-- Init.Data.List.Pairwise
List.Nodup.count : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {a : α} {l : List α},
  l.Nodup → List.count a l = if a ∈ l then 1 else 0
-- Mathlib.Data.Fin.SuccPred
Fin.coe_castPred : ∀ {n : ℕ} (i : Fin (n + 1)) (h : i ≠ Fin.last n), ↑(i.castPred h) = ↑i
-- Mathlib.RingTheory.NormalClosure
Ring.instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsDomain R] [inst_3 : IsDomain S]
  [inst_4 : Algebra R S] [inst_5 : Module.IsTorsionFree R S],
  IsScalarTower S (FractionRing S)
    ↥(IntermediateField.normalClosure (FractionRing R) (FractionRing S) (AlgebraicClosure (FractionRing S)))
-- Init.Data.Fin.Basic
Fin.instSub : {n : ℕ} → Sub (Fin n)
-- Std.Data.TreeMap.Basic
/-- Modifies in place the value associated with a given key,
allowing creating new values and deleting values via an `Option` valued replacement function.

This function ensures that the value is used linearly.
 -/
Std.TreeMap.alter : {α : Type u} →
  {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → α → (Option β → Option β) → Std.TreeMap α β cmp
-- Mathlib.Topology.MetricSpace.Holder
HolderOnWith.ediam_image_le_of_subset_of_le : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {C r : NNReal} {f : X → Y}
  {s t : Set X},
  HolderOnWith C r f s → t ⊆ s → ∀ {d : ENNReal}, Metric.ediam t ≤ d → Metric.ediam (f '' t) ≤ ↑C * d ^ ↑r
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.StrongTrans.isoMk_inv_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} (app : (a : B) → η.app a ≅ θ.app a)
  (naturality :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b).hom)
            (θ.naturality f).hom =
          CategoryTheory.CategoryStruct.comp (η.naturality f).hom
            (CategoryTheory.Bicategory.whiskerRight (app a).hom (G.map f)))
      CategoryTheory.Oplax.StrongTrans.isoMk._auto_1)
  (a : B), (CategoryTheory.Oplax.StrongTrans.isoMk app naturality).inv.as.app a = (app a).inv
-- Mathlib.Topology.Bornology.Basic
Bornology.IsBounded.disjoint_cobounded : ∀ {α : Type u_2} [inst : Bornology α] {l : Filter α} {s : Set α},
  Bornology.IsBounded s → s ∈ l → Disjoint l (Bornology.cobounded α)
-- Mathlib.Topology.UniformSpace.Closeds
/-- **Alias** of `UniformSpace.hausdorff.isClosed_setOfPred_totallyBounded`. -/
UniformSpace.hausdorff.isClosed_setOf_totallyBounded : ∀ {α : Type u_1} [inst : UniformSpace α], IsClosed {s | TotallyBounded s}
-- Mathlib.Topology.Algebra.Module.Multilinear.Bounded
/-- The image of a von Neumann bounded set under a continuous multilinear map
is von Neumann bounded.

This version assumes that the codomain is a topological vector space.
 -/
Bornology.IsVonNBounded.image_multilinear : ∀ {ι : Type u_1} {𝕜 : Type u_2} {F : Type u_3} {E : ι → Type u_4} [inst : NormedField 𝕜]
  [inst_1 : (i : ι) → AddCommGroup (E i)] [inst_2 : (i : ι) → Module 𝕜 (E i)]
  [inst_3 : (i : ι) → TopologicalSpace (E i)] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] [ContinuousSMul 𝕜 F] {s : Set ((i : ι) → E i)},
  Bornology.IsVonNBounded 𝕜 s → ∀ (f : ContinuousMultilinearMap 𝕜 E F), Bornology.IsVonNBounded 𝕜 (⇑f '' s)