mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.castLE.eq_4 : ∀ {L : FirstOrder.Language} {α : Type u'} (x x_1 : ℕ) (x_2 : x ≤ x_1) (f₁ f₂ : L.BoundedFormula α x),
  FirstOrder.Language.BoundedFormula.castLE x_2 (f₁.imp f₂) =
    (FirstOrder.Language.BoundedFormula.castLE x_2 f₁).imp (FirstOrder.Language.BoundedFormula.castLE x_2 f₂)
-- Mathlib.Tactic.Widget.CommDiag
/-- Presenter for a commutative triangle  -/
Mathlib.Tactic.Widget.commutativeTrianglePresenter : ProofWidgets.ExprPresenter
-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.SplitIterator.instIteratorIdSubslice.match_3.eq_2 : ∀ {σ : String.Slice → Type} [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)]
  {s : String.Slice} (searcher : Std.Iter (String.Slice.Pattern.SearchStep s)) (motive : searcher.Step → Sort u_1)
  (searcher' : Std.Iter (String.Slice.Pattern.SearchStep s)) (startPos endPos : s.Pos)
  (hps :
    searcher.IsPlausibleStep (Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.rejected startPos endPos)))
  (h_1 :
    (searcher'_1 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
      (startPos_1 endPos_1 : s.Pos) →
        (hps_1 :
            searcher.IsPlausibleStep
              (Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.matched startPos_1 endPos_1))) →
          ⟨Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.rejected startPos endPos), hps⟩ =
              ⟨Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.matched startPos_1 endPos_1), hps_1⟩ →
            motive
              ⟨Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.matched startPos_1 endPos_1), hps_1⟩)
  (h_2 :
    (searcher'_1 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
      (startPos_1 endPos_1 : s.Pos) →
        (hps_1 :
            searcher.IsPlausibleStep
              (Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.rejected startPos_1 endPos_1))) →
          ⟨Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.rejected startPos endPos), hps⟩ =
              ⟨Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.rejected startPos_1 endPos_1), hps_1⟩ →
            motive
              ⟨Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.rejected startPos_1 endPos_1), hps_1⟩)
  (h_3 :
    (searcher'_1 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
      (hps_1 : searcher.IsPlausibleStep (Std.IterStep.skip searcher'_1)) →
        ⟨Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.rejected startPos endPos), hps⟩ =
            ⟨Std.IterStep.skip searcher'_1, hps_1⟩ →
          motive ⟨Std.IterStep.skip searcher'_1, hps_1⟩)
  (h_4 :
    (property : searcher.IsPlausibleStep Std.IterStep.done) →
      ⟨Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.rejected startPos endPos), hps⟩ =
          ⟨Std.IterStep.done, property⟩ →
        motive ⟨Std.IterStep.done, property⟩),
  (match h : ⟨Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.rejected startPos endPos), hps⟩ with
    | ⟨Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.matched startPos_1 endPos_1), hps_1⟩ =>
      h_1 searcher'_1 startPos_1 endPos_1 hps_1 h
    | ⟨Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.rejected startPos_1 endPos_1), hps_1⟩ =>
      h_2 searcher'_1 startPos_1 endPos_1 hps_1 h
    | ⟨Std.IterStep.skip searcher'_1, hps_1⟩ => h_3 searcher'_1 hps_1 h
    | ⟨Std.IterStep.done, property⟩ => h_4 property h) =
    h_2 searcher' startPos endPos hps ⋯
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.OrderHom.omegaCompletePartialOrder_ωSup_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β]
  (c : OmegaCompletePartialOrder.Chain (α →o β)) (a : α),
  (OmegaCompletePartialOrder.ωSup c) a = OmegaCompletePartialOrder.ωSup (c.map (OrderHom.apply a))
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.coe_coeAddHom : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} [inst : AddMonoid M], ⇑(Filter.Germ.coeAddHom l) = Filter.Germ.ofFun
-- Mathlib.Algebra.Order.Monoid.Lex
/-- Given ordered monoids M, N, the natural inclusion ordered homomorphism from M to the
lexicographic M ×ₗ N.  -/
OrderMonoidHom.inlₗ : (α : Type u_1) →
  (β : Type u_2) →
    [inst : Monoid α] → [inst_1 : PartialOrder α] → [inst_2 : Monoid β] → [inst_3 : Preorder β] → α →*o Lex (α × β)
-- Mathlib.Analysis.Normed.Group.Indicator
norm_indicator_le_norm_self : ∀ {α : Type u_1} {E : Type u_2} [inst : SeminormedAddGroup E] {s : Set α} (f : α → E) (a : α), ‖s.indicator f a‖ ≤ ‖f a‖
-- Lean.Meta.Tactic.Grind.EMatchTheoremPtr
Lean.Meta.Grind.instHashableEMatchTheoremPtr : Hashable Lean.Meta.Grind.EMatchTheoremPtr
-- Mathlib.Algebra.Lie.Weights.RootSystem
/-- If `β - qα ... β ... β + rα` is the `α`-chain through `β`, then
`β (coroot α) = q - r`. In particular, it is an integer.  -/
LieAlgebra.IsKilling.apply_coroot_eq_cast : ∀ {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 : LieAlgebra.IsKilling K L] [inst_5 : FiniteDimensional K L] {H : LieSubalgebra K L}
  [inst_6 : H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (α β : LieModule.Weight K (↥H) L),
  β (LieAlgebra.IsKilling.coroot α) = ↑(↑(LieModule.chainBotCoeff (⇑α) β) - ↑(LieModule.chainTopCoeff (⇑α) β))
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.Cotrident.IsColimit.homIso_apply_coe : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [inst_1 : Nonempty J]
  {t : CategoryTheory.Limits.Cotrident f} (ht : CategoryTheory.Limits.IsColimit t) (Z : C) (k : t.pt ⟶ Z),
  ↑((CategoryTheory.Limits.Cotrident.IsColimit.homIso ht Z) k) = CategoryTheory.CategoryStruct.comp t.π k
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.instSetLike : {α : Type u_1} → [inst : LE α] → SetLike (LowerSet α) α
-- Mathlib.RepresentationTheory.Intertwining
/-- `IntertwiningMap.toLinearMap` as a linear map.  -/
Representation.IntertwiningMap.toLinearMapl : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : CommSemiring A] →
          [inst_1 : Monoid G] →
            [inst_2 : AddCommMonoid V] →
              [inst_3 : AddCommMonoid W] →
                [inst_4 : Module A V] →
                  [inst_5 : Module A W] →
                    (ρ : Representation A G V) → (σ : Representation A G W) → ρ.IntertwiningMap σ →ₗ[A] V →ₗ[A] W
-- Mathlib.Combinatorics.Young.SemistandardTableau
/-- Copy of an `SemistandardYoungTableau μ` with a new `entry` equal to the old one. Useful to fix
definitional equalities.  -/
SemistandardYoungTableau.copy : {μ : YoungDiagram} → (T : SemistandardYoungTableau μ) → (entry' : ℕ → ℕ → ℕ) → entry' = ⇑T → SemistandardYoungTableau μ
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
/-- The **boundary** of a manifold `M` is the set of its boundary points.  -/
ModelWithCorners.boundary : {𝕜 : 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 : TopologicalSpace M] → [ChartedSpace H M] → Set M
-- Mathlib.Topology.ContinuousMap.Interval
ContinuousMap.IccExtendCM_of_mem : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α] {a b : α}
  [inst_3 : Fact (a ≤ b)] {E : Type u_2} [inst_4 : TopologicalSpace E] {f : C(↑(Set.Icc a b), E)} {x : α}
  (hx : x ∈ Set.Icc a b), (ContinuousMap.IccExtendCM f) x = f ⟨x, hx⟩
-- Mathlib.Order.Defs.LinearOrder
eq_max : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, a ≤ c → b ≤ c → (∀ {d : α}, a ≤ d → b ≤ d → c ≤ d) → c = max a b
-- Mathlib.LinearAlgebra.Dimension.Localization
IsBaseChange.lift_rank_eq_of_le_nonZeroDivisors : ∀ {R : Type uR} (S : Type uS) {M : Type uM} {N : Type uN} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Algebra R S]
  [inst_7 : Module S N] [IsScalarTower R S N] {p : Submonoid R} [IsLocalization p S] (f : M →ₗ[R] N)
  [IsLocalizedModule p f],
  p ≤ nonZeroDivisors R →
    ∀ [Module.Free S N] [StrongRankCondition S] {T : Type uT} [inst_13 : CommRing T] [inst_14 : Algebra R T],
      Algebra.algebraMapSubmonoid T p ≤ nonZeroDivisors T →
        ∀ [StrongRankCondition (TensorProduct R S T)] {P : Type uP} [inst_16 : AddCommGroup P] [inst_17 : Module R P]
          [inst_18 : Module T P] [inst_19 : IsScalarTower R T P] {g : M →ₗ[R] P},
          IsBaseChange T g → Cardinal.lift.{uM, uP} (Module.rank T P) = Cardinal.lift.{uP, uM} (Module.rank R M)
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.braiding_leftUnitor_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : C) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (β_ X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom h
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- The `Submodule.LinearDisjoint.not_linearIndependent_pair_of_commute_of_flat`
for commutative rings.  -/
Submodule.LinearDisjoint.not_linearIndependent_pair_of_flat : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {M N : Submodule R S},
  M.LinearDisjoint N →
    ∀ [Nontrivial R], Module.Flat R ↥M ∨ Module.Flat R ↥N → ∀ (a b : ↥(M ⊓ N)), ¬LinearIndependent R ![a, b]
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.mul_logb : ∀ {a b c : ℝ}, b ≠ 0 → b ≠ 1 → b ≠ -1 → Real.logb a b * Real.logb b c = Real.logb a c
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {k a : α}
  {h₁ : a ∈ t.insert k}, (t.insert k).get a h₁ = if h₂ : cmp k a = Ordering.eq ∧ k ∉ t then k else t.get a ⋯
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.instIsLocalAtTargetIsomorphismsZariskiPrecoverage : (CategoryTheory.MorphismProperty.isomorphisms AlgebraicGeometry.Scheme).IsLocalAtTarget
  AlgebraicGeometry.Scheme.zariskiPrecoverage
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
/-- The natural isomorphism
`F.mapShortComplex ⋙ opcyclesFunctor D ≅ opcyclesFunctor C ⋙ F`
for a functor `F : C ⥤ D` which preserves homology.  -/
CategoryTheory.ShortComplex.opcyclesFunctorIso : {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] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            (F : CategoryTheory.Functor C D) →
              [inst_4 : F.PreservesZeroMorphisms] →
                [inst_5 : CategoryTheory.Limits.HasKernels C] →
                  [inst_6 : CategoryTheory.Limits.HasCokernels C] →
                    [inst_7 : CategoryTheory.Limits.HasKernels D] →
                      [inst_8 : CategoryTheory.Limits.HasCokernels D] →
                        [F.PreservesHomology] →
                          F.mapShortComplex.comp (CategoryTheory.ShortComplex.opcyclesFunctor D) ≅
                            (CategoryTheory.ShortComplex.opcyclesFunctor C).comp F
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
CategoryTheory.Localization.Preadditive.comp_add' : ∀ {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] [inst_2 : CategoryTheory.Preadditive C]
  {L : CategoryTheory.Functor C D} (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  [inst_4 : W.HasLeftCalculusOfFractions] {X Y Z : C} (f : L.obj X ⟶ L.obj Y) (g₁ g₂ : L.obj Y ⟶ L.obj Z),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.Localization.Preadditive.add' W g₁ g₂) =
    CategoryTheory.Localization.Preadditive.add' W (CategoryTheory.CategoryStruct.comp f g₁)
      (CategoryTheory.CategoryStruct.comp f g₂)
-- Aesop.Percent
Aesop.Percent.mk : Float → Aesop.Percent
-- Mathlib.Order.Filter.AtTopBot.Field
Filter.tendsto_const_mul_pow_atBot_iff : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {c : α} {n : ℕ},
  Filter.Tendsto (fun x => c * x ^ n) Filter.atTop Filter.atBot ↔ n ≠ 0 ∧ c < 0
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
MonoidHom.compLeftContinuousBounded.eq_1 : ∀ {β : Type v} {γ : Type w} (α : Type u_3) [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
  [inst_2 : Monoid β] [inst_3 : BoundedMul β] [inst_4 : ContinuousMul β] [inst_5 : PseudoMetricSpace γ]
  [inst_6 : Monoid γ] [inst_7 : BoundedMul γ] [inst_8 : ContinuousMul γ] (g : β →* γ) {C : NNReal}
  (hg : LipschitzWith C ⇑g),
  MonoidHom.compLeftContinuousBounded α g hg =
    { toFun := fun f => BoundedContinuousFunction.comp (⇑g) hg f, map_one' := ⋯, map_mul' := ⋯ }
-- Lean.Data.Json.FromToJson.Basic
Lean.instToJsonString : Lean.ToJson String
-- Mathlib.CategoryTheory.SingleObj
MulEquiv.toSingleObjEquiv_counitIso_inv : ∀ {M : Type u} {N : Type v} [inst : Monoid M] [inst_1 : Monoid N] (e : M ≃* N),
  e.toSingleObjEquiv.counitIso.inv = CategoryTheory.eqToHom ⋯
-- Init.Data.Slice.List.Lemmas
ListSlice.toArray_mkSlice_roi_eq_toArray_mkSlice_roo : ∀ {α : Type u_1} {xs : ListSlice α} {lo : ℕ},
  Std.Slice.toArray (Std.Roi.Sliceable.mkSlice xs lo<...*) =
    Std.Slice.toArray (Std.Roo.Sliceable.mkSlice xs lo<...Std.Slice.size xs)
-- Lean.Meta.Tactic.Contradiction
/-- Try to close the goal using "contradictions" such as
- Contradictory hypotheses `h₁ : p` and `h₂ : ¬ p`.
- Contradictory disequality `h : x ≠ x`.
- Contradictory bit mask test: `h : Nat.hasNotBit mask i` where that bit is set
- Contradictory equality between different constructors, e.g., `h : List.nil = List.cons x xs`.
- Empty inductive types, e.g., `x : Fin 0`.
- Decidable propositions that evaluate to false, i.e., a hypothesis `h : p` s.t. `decide p` reduces to `false`.
  This is only tried if `Config.useDecide = true`.

Throw exception if goal failed to be closed.
 -/
Lean.MVarId.contradiction : Lean.MVarId → optParam Lean.Meta.Contradiction.Config { } → Lean.MetaM Unit
-- Mathlib.Topology.Covering.Basic
/-- If `f : E → X` is a closed map between topological spaces with `E` Hausdorff, such that the
fiber over a point `x : X` is finite and `f` restricts to a homeomorphism on a neighborhood of
every point of the fiber, then `x` admits an evenly covered neighborhood.  -/
IsClosedMap.isEvenlyCovered_of_openPartialHomeomorph : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} [T2Space E]
  {x : X},
  IsClosedMap f → (f ⁻¹' {x}).Finite → (∀ e ∈ f ⁻¹' {x}, ∃ φ, e ∈ φ.source ∧ ↑φ = f) → IsEvenlyCovered f x ↑(f ⁻¹' {x})
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.toAddMonoid.eq_1 : ∀ {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] [inst_1 : DecidableEq ι] {γ : Type u₁}
  [inst_2 : AddCommMonoid γ] (φ : (i : ι) → β i →+ γ), DirectSum.toAddMonoid φ = DFinsupp.liftAddHom φ
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.diagramIsoPair_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C)
  (X : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair),
  (CategoryTheory.Limits.diagramIsoPair F).hom.app X =
    (match X with
      | { as := CategoryTheory.Limits.WalkingPair.left } =>
        CategoryTheory.Iso.refl (F.obj { as := CategoryTheory.Limits.WalkingPair.left })
      | { as := CategoryTheory.Limits.WalkingPair.right } =>
        CategoryTheory.Iso.refl (F.obj { as := CategoryTheory.Limits.WalkingPair.right })).hom
-- Mathlib.Analysis.Distribution.TemperedDistribution
SchwartzMap.instCoeToTemperedDistribution : {E : Type u_3} →
  {F : Type u_4} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        [inst_2 : NormedAddCommGroup F] →
          [inst_3 : NormedSpace ℂ F] →
            [inst_4 : MeasureTheory.MeasureSpace E] →
              [BorelSpace E] →
                [SecondCountableTopology E] →
                  [MeasureTheory.volume.HasTemperateGrowth] → Coe (SchwartzMap E F) (TemperedDistribution E F)
-- Mathlib.Topology.UniformSpace.UniformEmbedding
uniformly_extend_of_ind : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : UniformSpace α] [inst_1 : UniformSpace β]
  [inst_2 : UniformSpace γ] {e : β → α} (h_e : IsUniformInducing e) (h_dense : DenseRange e) {f : β → γ},
  UniformContinuous f → ∀ [T0Space γ] (b : β), ⋯.extend f (e b) = f b
-- Mathlib.SetTheory.Lists
Lists.Equiv.below : {α : Type u_1} →
  {motive_1 : (a a_1 : Lists α) → a.Equiv a_1 → Prop} →
    {motive_2 : (a a_1 : Lists' α true) → a.Subset a_1 → Prop} → {a a_1 : Lists α} → a.Equiv a_1 → Prop
-- Mathlib.Algebra.Group.Ideal
/-- In an additive monoid, the semigroup ideal generated by `s` is `Set.univ + s`.  -/
AddSemigroupIdeal.mem_closure'' : ∀ {M : Type u_1} [inst : AddMonoid M] {s : Set M} {x : M}, x ∈ AddSemigroupIdeal.closure s ↔ ∃ y, ∃ z ∈ s, y + z = x
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
NumberField.Units.dirichletUnitTheorem.seq.congr_simp : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (w₁ w₁_1 : NumberField.InfinitePlace K),
  w₁ = w₁_1 →
    ∀ {B B_1 : ℕ} (e_B : B = B_1)
      (hB : NumberField.mixedEmbedding.minkowskiBound K 1 < ↑(NumberField.mixedEmbedding.convexBodyLTFactor K) * ↑B)
      (a a_1 : ℕ),
      a = a_1 →
        NumberField.Units.dirichletUnitTheorem.seq K w₁ hB a = NumberField.Units.dirichletUnitTheorem.seq K w₁_1 ⋯ a_1
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.zero_notMem_neg_add_iff : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddGroup α] {s t : Finset α}, 0 ∉ -t + s ↔ Disjoint s t
-- Mathlib.RingTheory.SimpleRing.DivisionRing
DivisionRing.nonempty_linearEquiv_of_isSimpleModule : ∀ (S : Type u_2) [inst : DivisionRing S] (N : Type u_3) [inst_1 : AddCommGroup N] [inst_2 : Module S N]
  [IsSimpleModule S N], Nonempty (N ≃ₗ[S] S)
-- Mathlib.CategoryTheory.Limits.Creates
/-- If `F` reflects isomorphisms and we can lift a single limit cone to a limit cone, then `F`
creates limits. Note that unlike `createsLimitOfReflectsIso`, to apply this result it is
necessary to know that `K ⋙ F` actually has a limit.  -/
CategoryTheory.createsLimitOfReflectsIso' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            {K : CategoryTheory.Functor J C} →
              {F : CategoryTheory.Functor C D} →
                [F.ReflectsIsomorphisms] →
                  {c : CategoryTheory.Limits.Cone (K.comp F)} →
                    (hc : CategoryTheory.Limits.IsLimit c) →
                      CategoryTheory.LiftsToLimit K F c hc → CategoryTheory.CreatesLimit K F
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.IsImage.lift_ι_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  [inst_1 : CategoryTheory.Limits.HasImage f] {F : CategoryTheory.Limits.MonoFactorisation f}
  (hF : CategoryTheory.Limits.IsImage F) {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (hF.lift (CategoryTheory.Limits.Image.monoFactorisation f))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f) h) =
    CategoryTheory.CategoryStruct.comp F.m h
-- Mathlib.Topology.ContinuousOn
Topology.IsOpenEmbedding.map_nhdsWithin_preimage_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
  Topology.IsOpenEmbedding f → ∀ (s : Set β) (x : α), Filter.map f (nhdsWithin x (f ⁻¹' s)) = nhdsWithin (f x) s
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_def'_assoc : ∀ {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] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {x₁ y₁ : C} {x₂ y₂ : D} (f : x₁ ⟶ y₁) (g : x₂ ⟶ y₂)
  {Z : D} (h : CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj y₁ y₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom f g) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight x₁ g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f y₂)
        h)
-- Mathlib.Analysis.Convex.Function
OrderIso.strictConvexOn_symm : ∀ {𝕜 : Type u_1} {α : Type u_4} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid α]
  [inst_3 : PartialOrder α] [inst_4 : SMul 𝕜 α] [inst_5 : AddCommMonoid β] [inst_6 : PartialOrder β] [inst_7 : SMul 𝕜 β]
  (f : α ≃o β), StrictConcaveOn 𝕜 Set.univ ⇑f → StrictConvexOn 𝕜 Set.univ ⇑f.symm
-- Mathlib.Tactic.Polynomial.Core
Mathlib.Tactic.Polynomial.PolynomialExt.mk : (Lean.Expr → Lean.MetaM Lean.Expr) → Mathlib.Tactic.Polynomial.PolynomialExt
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.toTree_ofTree : ∀ (t : BinaryTree Unit), (DyckWord.ofTree t).toTree = t
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.isIso_of_isOpenImmersion_of_opensRange_eq_top : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f],
  AlgebraicGeometry.Scheme.Hom.opensRange f = ⊤ → CategoryTheory.IsIso f
-- Init.Data.SInt.Lemmas
Int32.le_of_eq : ∀ {a b : Int32}, a = b → a ≤ b
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.homQuotientZPowOfHom_comp_of_rightInverse : ∀ {A B : Type u} [inst : CommGroup A] [inst_1 : CommGroup B] (f : A →* B) (g : B →* A) (n : ℤ),
  Function.RightInverse ⇑g ⇑f →
    (QuotientGroup.homQuotientZPowOfHom f n).comp (QuotientGroup.homQuotientZPowOfHom g n) =
      MonoidHom.id (B ⧸ (zpowGroupHom n).range)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- **Fundamental theorem of calculus-1**, strict differentiability in the left endpoint.

If `f : ℝ → E` is integrable on `a..b` and `f x` has a finite limit `c` almost surely at `a`, then
`u ↦ ∫ x in u..b, f x` has derivative `-c` at `a` in the sense of strict differentiability.  -/
intervalIntegral.integral_hasStrictDerivAt_of_tendsto_ae_left : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {c : E}
  {a b : ℝ},
  IntervalIntegrable f MeasureTheory.volume a b →
    StronglyMeasurableAtFilter f (nhds a) MeasureTheory.volume →
      Filter.Tendsto f (nhds a ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds c) →
        HasStrictDerivAt (fun u => ∫ (x : ℝ) in u..b, f x) (-c) a
-- Mathlib.Algebra.Divisibility.Basic
RightDvd.rfl : ∀ {α : Type u_1} [inst : Monoid α] {a : α}, a ∣ᵣ a
-- Lean.Attributes
/-- Return the name of all registered attributes.  -/
Lean.getBuiltinAttributeNames : IO (List Lean.Name)
-- Mathlib.Analysis.SpecialFunctions.CompareExp
Complex.IsExpCmpFilter.of_isBigO_im_re_pow : ∀ {l : Filter ℂ},
  Filter.Tendsto Complex.re l Filter.atTop → ∀ (n : ℕ), (Complex.im =O[l] fun z => z.re ^ n) → Complex.IsExpCmpFilter l
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.truncLTι_comp_truncGEπ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ),
  CategoryTheory.CategoryStruct.comp (t.truncLTι n) (t.truncGEπ n) = 0