mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Continuous
Continuous.range_subset_closure_image_dense : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {f : X → Y},
  Continuous f → Dense s → Set.range f ⊆ closure (f '' s)
-- Init.Control.StateRef
/-- Replaces the mutable state with a new value.
 -/
StateRefT'.set : {ω σ : Type} → {m : Type → Type} → [MonadLiftT (ST ω) m] → σ → StateRefT' ω σ m PUnit.{1}
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.map_proj : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : C(X, Y)}
  {A : DiscreteQuotient X} {B : DiscreteQuotient Y} (cond : DiscreteQuotient.LEComap f A B) (x : X),
  DiscreteQuotient.map f cond (A.proj x) = B.proj (f x)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.WalkingMultispan.right.injEq : ∀ {J : CategoryTheory.Limits.MultispanShape} (a a_1 : J.R),
  (CategoryTheory.Limits.WalkingMultispan.right a = CategoryTheory.Limits.WalkingMultispan.right a_1) = (a = a_1)
-- Mathlib.Data.Fintype.Perm
_private.Mathlib.Data.Fintype.Perm.0.permsOfList.match_1.splitter : {α : Type u_1} →
  (motive : List α → Sort u_2) →
    (x : List α) → (Unit → motive []) → ((a : α) → (l : List α) → motive (a :: l)) → motive x
-- Lean.Data.Iterators.Producers.PersistentHashMap
_private.Lean.Data.Iterators.Producers.PersistentHashMap.0.Lean.PersistentHashMap.Zipper.step.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (it : Std.IterM Id (α × β)),
  Lean.PersistentHashMap.Zipper.step it =
    match it.internalState with
    | Lean.PersistentHashMap.Zipper.done => Std.IterStep.done
    | Lean.PersistentHashMap.Zipper.consEntries es z' =>
      if h : 0 < Std.Slice.size es then
        have z := Lean.PersistentHashMap.Zipper.consEntries (es.drop 1) z';
        match es[0] with
        | Lean.PersistentHashMap.Entry.null => Std.IterStep.skip { internalState := z }
        | Lean.PersistentHashMap.Entry.entry k v => Std.IterStep.yield { internalState := z } (k, v)
        | Lean.PersistentHashMap.Entry.ref node =>
          Std.IterStep.skip { internalState := Lean.PersistentHashMap.Zipper.prependNode node z }
      else Std.IterStep.skip { internalState := z' }
    | Lean.PersistentHashMap.Zipper.consCollision keys vals hsz z' =>
      if h : 0 < Std.Slice.size vals then
        Std.IterStep.yield
          { internalState := Lean.PersistentHashMap.Zipper.consCollision (keys.drop 1) (vals.drop 1) ⋯ z' }
          (keys[0], vals[0])
      else Std.IterStep.skip { internalState := z' }
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.Hom.α_hom.sizeOf_spec : ∀ {C : Type u} [inst : SizeOf C] (X Y Z : CategoryTheory.FreeMonoidalCategory C),
  sizeOf (CategoryTheory.FreeMonoidalCategory.Hom.α_hom X Y Z) = 1 + sizeOf X + sizeOf Y + sizeOf Z
-- Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
SchwartzMap.instFourierAdd : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_3} [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : FiniteDimensional ℝ V] [inst_5 : MeasurableSpace V]
  [inst_6 : BorelSpace V], FourierAdd (SchwartzMap V E) (SchwartzMap V E)
-- Mathlib.Tactic.Linter.UnusedTactic
/-- Accumulates the set of tactic syntaxes that should be evaluated at least once.  -/
_private.Mathlib.Tactic.Linter.UnusedTactic.0.Mathlib.Linter.UnusedTactic.getTactics : Lean.NameHashSet → (Lean.SyntaxNodeKind → Bool) → Lean.Syntax → Mathlib.Linter.UnusedTactic.M✝ Unit
-- Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
/-- A field `K` is totally complex if all of its infinite places are complex.
 -/
NumberField.IsTotallyComplex : (K : Type u_1) → [Field K] → Prop
-- Mathlib.Condensed.Light.TopCatAdjunction
LightCondSet.instSequentialSpaceCarrierObjTopCatLightCondSetToTopCat : ∀ (X : LightCondSet), SequentialSpace ↑(lightCondSetToTopCat.obj X)
-- Mathlib.Analysis.Normed.Operator.NNNorm
ContinuousLinearMap.le_opENorm : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NontriviallyNormedField 𝕜₂] [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂]
  (f : E →SL[σ₁₂] F) (x : E), ‖f x‖ₑ ≤ ‖f‖ₑ * ‖x‖ₑ
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
/-- Version of `HasProd.update` for `CommMonoid` rather than `CommGroup`.
Rather than showing that `f.update` has a specific product in terms of `HasProd`,
it gives a relationship between the products of `f` and `f.update` given that both exist.  -/
HasProd.update' : ∀ {β : Type u_2} {L : SummationFilter β} [L.LeAtTop] [L.NeBot] {α : Type u_4} [inst : TopologicalSpace α]
  [inst_1 : CommMonoid α] [T2Space α] [ContinuousMul α] [inst_4 : DecidableEq β] {f : β → α} {a a' : α},
  HasProd f a L → ∀ (b : β) (x : α), HasProd (Function.update f b x) a' L → a * x = a' * f b
-- Mathlib.Data.List.Defs
_private.Mathlib.Data.List.Defs.0.List.iterate.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.Algebra.Group.Conj
/-- The canonical quotient map from a monoid `α` into the `ConjClasses` of `α`  -/
ConjClasses.mk : {α : Type u_1} → [inst : Monoid α] → α → ConjClasses α
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.mem_zero : ∀ {α : Type u_2} [inst : Zero α] {a : α}, a ∈ 0 ↔ a = 0
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.norm_eq_nc_cert.eq_1 : ∀ (lhs rhs lhs' rhs' : Lean.Grind.CommRing.Expr),
  Lean.Grind.CommRing.norm_eq_nc_cert lhs rhs lhs' rhs' = (lhs.sub rhs).toPoly_nc.beq' (lhs'.sub rhs').toPoly_nc
-- Mathlib.Computability.TuringMachine.StackTuringMachine
StateTransition.Respects.eq_1 : ∀ {σ₁ : Type u_1} {σ₂ : Type u_2} (f₁ : σ₁ → Option σ₁) (f₂ : σ₂ → Option σ₂) (tr : σ₁ → σ₂ → Prop),
  StateTransition.Respects f₁ f₂ tr =
    ∀ ⦃a₁ : σ₁⦄ ⦃a₂ : σ₂⦄,
      tr a₁ a₂ →
        match f₁ a₁ with
        | some b₁ => ∃ b₂, tr b₁ b₂ ∧ StateTransition.Reaches₁ f₂ a₂ b₂
        | none => f₂ a₂ = none
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
SheafOfModules.pushforward_id_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D}
  {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat}
  [inst_2 : F.IsContinuous J K] (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R),
  SheafOfModules.pushforwardComp φ (CategoryTheory.CategoryStruct.id R) =
    CategoryTheory.Functor.isoWhiskerRight (SheafOfModules.pushforwardId R) (SheafOfModules.pushforward φ) ≪≫
      (SheafOfModules.pushforward φ).leftUnitor
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.image_ι_comp_eq_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y Z : C}
  {f : X ⟶ Y} {g : Y ⟶ Z} [inst_2 : CategoryTheory.Limits.HasImage f]
  [CategoryTheory.Epi (CategoryTheory.Limits.factorThruImage f)],
  CategoryTheory.CategoryStruct.comp f g = 0 →
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f) g = 0
-- Mathlib.Algebra.GCDMonoid.Multiset
Multiset.associated_gcd_map_mul : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (a : α) (s : Multiset α),
  Associated (Multiset.map (fun x => a * x) s).gcd (a * s.gcd)
-- Mathlib.Order.Interval.Set.ProjIcc
Set.IciExtend_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] {a : α} (f : ↑(Set.Ici a) → β) (x : α),
  Set.IciExtend f x = f ⟨max a x, ⋯⟩
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
/-- Like `Submodule.map_mul`, but with the multiplication reversed.  -/
CliffordAlgebra.submodule_map_mul_reverse : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (p q : Submodule R (CliffordAlgebra Q)),
  Submodule.map CliffordAlgebra.reverse (p * q) =
    Submodule.map CliffordAlgebra.reverse q * Submodule.map CliffordAlgebra.reverse p
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Option.elim.match_1.eq_2 : ∀ {α : Type u_1} {β : Sort u_3} (motive : Option α → β → (α → β) → Sort u_2) (y : β) (x : α → β)
  (h_1 : (x : α) → (x_1 : β) → (f : α → β) → motive (some x) x_1 f) (h_2 : (y : β) → (x : α → β) → motive none y x),
  (match none, y, x with
    | some x, x_1, f => h_1 x x_1 f
    | none, y, x => h_2 y x) =
    h_2 y x
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Hom.indexEquiv_one : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N),
  RootPairing.Hom.indexEquiv 1 = Equiv.refl ι
-- Mathlib.Analysis.Normed.Operator.NormedSpace
LinearMap.bound_of_shell : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_3} {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →ₛₗ[σ₁₂] F)
  {ε C : ℝ},
  0 < ε → ∀ {c : 𝕜}, 1 < ‖c‖ → (∀ (x : E), ε / ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖) → ∀ (x : E), ‖f x‖ ≤ C * ‖x‖
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.preOmega_omega0 : Ordinal.preOmega Ordinal.omega0 = Ordinal.omega0
-- Init.Data.UInt.Lemmas
UInt64.lt_of_le_of_lt : ∀ {a b c : UInt64}, a ≤ b → b < c → a < c
-- Mathlib.Algebra.Order.Group.Nat
Nat.instOrderedSub : OrderedSub ℕ
-- Mathlib.Algebra.Homology.Linear
HomologicalComplex.instLinear : {R : Type u_1} →
  [inst : Semiring R] →
    {C : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_1, u_2} C] →
        [inst_2 : CategoryTheory.Preadditive C] →
          [CategoryTheory.Linear R C] →
            {ι : Type u_4} → {c : ComplexShape ι} → CategoryTheory.Linear R (HomologicalComplex C c)
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.botEquiv_symm_apply : ∀ (F : Type u_1) (R : Type u_2) [inst : Field F] [inst_1 : Semiring R] [inst_2 : Nontrivial R] [inst_3 : Algebra F R]
  (a : F), (Algebra.botEquiv F R).symm a = (algebraMap F ↥⊥) a
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Functor.strongMono_map_iff_strongMono_of_isEquivalence : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {A B : C} (f : B ⟶ A)
  [F.IsEquivalence], CategoryTheory.StrongMono (F.map f) ↔ CategoryTheory.StrongMono f
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_congr_fun : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f g : X → E} {s : Set X} {μ : MeasureTheory.Measure X},
  MeasurableSet s → Set.EqOn f g s → ∫ (x : X) in s, f x ∂μ = ∫ (x : X) in s, g x ∂μ
-- Mathlib.Topology.Algebra.Star
instContinuousStarForall : ∀ {ι : Type u_3} {C : ι → Type u_4} [inst : (i : ι) → TopologicalSpace (C i)] [inst_1 : (i : ι) → Star (C i)]
  [∀ (i : ι), ContinuousStar (C i)], ContinuousStar ((i : ι) → C i)
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.cof_ne_zero : ∀ {o : Ordinal.{u_1}}, o.cof ≠ 0 ↔ o ≠ 0
-- Mathlib.Algebra.Group.TypeTags.Basic
isLeftRegular_ofAdd : ∀ {α : Type u} [inst : AddMonoid α] {a : α}, IsLeftRegular (Multiplicative.ofAdd a) ↔ IsAddLeftRegular a
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.cospanOp_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
  (X_1 : CategoryTheory.Limits.WalkingCospan),
  (CategoryTheory.Limits.cospanOp f g).inv.app X_1 =
    (match X_1 with
      | none => CategoryTheory.Iso.refl (Opposite.op X)
      | some CategoryTheory.Limits.WalkingPair.left => CategoryTheory.Iso.refl (Opposite.op Y)
      | some CategoryTheory.Limits.WalkingPair.right => CategoryTheory.Iso.refl (Opposite.op Z)).inv
-- Mathlib.Algebra.CharP.Frobenius
LinearMap.frobenius_def : ∀ (R : Type u_1) [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] (p : ℕ) [inst_2 : ExpChar R p]
  [inst_3 : ExpChar S p] [inst_4 : Algebra R S] (x : S), (LinearMap.frobenius R S p) x = x ^ p
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.formatCommand : Lean.Syntax → Lean.CoreM Std.Format
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.toFractionRingRingEquiv_symm_eq : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K],
  (RatFunc.toFractionRingRingEquiv K).symm =
    (IsLocalization.algEquiv (nonZeroDivisors (Polynomial K)) (FractionRing (Polynomial K)) (RatFunc K)).toRingEquiv
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.normal_comap_iff_of_surjective : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {f : G →* N},
  Function.Surjective ⇑f → ∀ {H : Subgroup N}, (Subgroup.comap f H).Normal ↔ H.Normal
-- Mathlib.SetTheory.Cardinal.ToNat
Cardinal.toNat_lift_add_lift : ∀ {a : Cardinal.{u}} {b : Cardinal.{v}},
  a < Cardinal.aleph0 →
    b < Cardinal.aleph0 →
      Cardinal.toNat (Cardinal.lift.{v, u} a + Cardinal.lift.{u, v} b) = Cardinal.toNat a + Cardinal.toNat b
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- Given a colimit cocone for the family `f : J → (X ⟶ Y)`, for any `Z`, morphisms from the cocone
point to `Z` are in bijection with morphisms `h : Z ⟶ X` such that
`∀ j₁ j₂, f j₁ ≫ h = f j₂ ≫ h`.  Further, this bijection is natural in `Z`: see
`Cotrident.IsColimit.homIso_natural`.
 -/
CategoryTheory.Limits.Cotrident.IsColimit.homIso : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {X Y : C} →
        {f : J → (X ⟶ Y)} →
          [Nonempty J] →
            {t : CategoryTheory.Limits.Cotrident f} →
              CategoryTheory.Limits.IsColimit t →
                (Z : C) →
                  (t.pt ⟶ Z) ≃
                    { h //
                      ∀ (j₁ j₂ : J),
                        CategoryTheory.CategoryStruct.comp (f j₁) h = CategoryTheory.CategoryStruct.comp (f j₂) h }
-- Mathlib.Algebra.Order.Ring.Int
/-- If the gcd of two natural numbers `p` and `q` divides a third natural number `n`,
and if `n` is at least `(p - 1) * (q - 1)`, then `n` can be represented as an `ℕ`-linear
combination of `p` and `q`.

TODO: show that if `p.gcd q = 1` and `0 ≤ n ≤ (p - 1) * (q - 1) - 1 = N`, then `n` is
representable iff `N - n` is not. In particular `N` is not representable, solving the
coin problem for two coins: https://en.wikipedia.org/wiki/Coin_problem#n_=_2.  -/
Nat.exists_add_mul_eq_of_gcd_dvd_of_mul_pred_le : ∀ (p q n : ℕ), p.gcd q ∣ n → p.pred * q.pred ≤ n → ∃ a b, a * p + b * q = n
-- Mathlib.Analysis.Distribution.TemperedDistribution
/-- The distributional Fourier transform and the classical Fourier transform coincide on
`𝓢(E, F)`.  -/
TemperedDistribution.fourier_toTemperedDistributionCLM_eq : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E]
  [inst_2 : FiniteDimensional ℝ E] [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace ℂ F] [CompleteSpace F] (f : SchwartzMap E F),
  FourierTransform.fourier ((SchwartzMap.toTemperedDistributionCLM E F MeasureTheory.volume) f) =
    (SchwartzMap.toTemperedDistributionCLM E F MeasureTheory.volume) (FourierTransform.fourier f)
-- Mathlib.Analysis.Calculus.Deriv.Star
deriv.star' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] [inst_1 : StarRing 𝕜] {F : Type v} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace 𝕜 F] [inst_4 : StarAddMonoid F] [StarModule 𝕜 F] [ContinuousStar F] {f : 𝕜 → F} [TrivialStar 𝕜],
  (deriv fun y => star (f y)) = fun x => star (deriv f x)
-- Lean.Elab.InfoTree.Main
Lean.Elab.PartialContextInfo.format : Lean.Elab.PartialContextInfo → Std.Format
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPullback.hom_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z}
  {g : Y ⟶ Z},
  CategoryTheory.IsPullback fst snd f g →
    ∀ {W : C} {k l : W ⟶ P},
      CategoryTheory.CategoryStruct.comp k fst = CategoryTheory.CategoryStruct.comp l fst →
        CategoryTheory.CategoryStruct.comp k snd = CategoryTheory.CategoryStruct.comp l snd → k = l
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.GrothendieckTopology.OneHypercover.IsPreservedBy.mem₀ : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {J : CategoryTheory.GrothendieckTopology C} {X : C} {E : J.OneHypercover X} {F : CategoryTheory.Functor C D}
  {K : CategoryTheory.GrothendieckTopology D} [self : E.IsPreservedBy F K], (E.map F).sieve₀ ∈ K (F.obj X)
-- Mathlib.Analysis.Normed.Module.Dual
NormedSpace.polar_closure : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (s : Set E), StrongDual.polar 𝕜 (closure s) = StrongDual.polar 𝕜 s
-- Mathlib.CategoryTheory.Functor.Flat
CategoryTheory.Functor.lanUnit.eq_1 : ∀ {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] (L : CategoryTheory.Functor C D) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H]
  [inst_3 : ∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension F],
  L.lanUnit = { app := fun F => L.leftKanExtensionUnit F, naturality := ⋯ }
-- Mathlib.Data.Fintype.Card
Fintype.card_orderDual : ∀ (α : Type u_4) [inst : Fintype α], Fintype.card αᵒᵈ = Fintype.card α
-- Init.Data.UInt.Bitwise
instIdempotentOpUInt16HOr : Std.IdempotentOp fun x1 x2 => x1 ||| x2
-- Lean.Compiler.InlineAttrs
Lean.Compiler.InlineAttributeKind.noinline.sizeOf_spec : sizeOf Lean.Compiler.InlineAttributeKind.noinline = 1
-- Mathlib.Algebra.Order.Group.Abs
abs_sub_le_of_le_of_le : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] {a b lb ub : G},
  lb ≤ a → a ≤ ub → lb ≤ b → b ≤ ub → |a - b| ≤ ub - lb
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.prodFunctorToFunctorProd_map : ∀ (A : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} A] (B : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  (C : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor A B × CategoryTheory.Functor A C} (f : F ⟶ G),
  (CategoryTheory.prodFunctorToFunctorProd A B C).map f = CategoryTheory.NatTrans.prod' f.1 f.2
-- Mathlib.Geometry.Polygon.Basic
/-- The polygon obtained from a triangle has nondegenerate vertices.  -/
Affine.Triangle.toPolygon_hasNondegenerateVertices : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  [inst_3 : AddTorsor V P] (t : Affine.Triangle R P), Polygon.HasNondegenerateVertices R (Affine.Triangle.toPolygon t)
-- Mathlib.Algebra.Group.Prod
MulEquiv.uniqueProd.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : Unique N],
  MulEquiv.uniqueProd = { toEquiv := Equiv.uniqueProd M N, map_mul' := ⋯ }
-- Init.Data.String.Pattern.Basic
/-- The subslice starting at `startPos` and ending at `endPos` matches the pattern.
   -/
String.Slice.Pattern.SearchStep.matched : {s : String.Slice} → s.Pos → s.Pos → String.Slice.Pattern.SearchStep s
-- Mathlib.Order.PFilter
Order.PFilter.instInhabited : {P : Type u_1} → [inst : Preorder P] → [Inhabited P] → Inhabited (Order.PFilter P)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMon.uniqueHomToTrivial_default_hom : ∀ {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} D] [inst_1 : CategoryTheory.SemiCartesianMonoidalCategory D]
  (A : CategoryTheory.AddMon D), default.hom = CategoryTheory.SemiCartesianMonoidalCategory.toUnit A.X
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.minKey?_modify : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} {f : β → β},
      (Std.DTreeMap.Internal.Impl.Const.modify k f t).minKey? =
        Option.map (fun km => if compare km k = Ordering.eq then k else km) t.minKey?
-- Mathlib.Algebra.Lie.Weights.Cartan
LieAlgebra.rootSpace.congr_simp : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (H : LieSubalgebra R L) [inst_3 : LieRing.IsNilpotent ↥H] (χ χ_1 : ↥H → R),
  χ = χ_1 → LieAlgebra.rootSpace H χ = LieAlgebra.rootSpace H χ_1
-- Std.Sat.AIG.Basic
/-- A cache for reusing elements from `decls` if they are available.
 -/
Std.Sat.AIG.Cache : (α : Type) → [DecidableEq α] → [Hashable α] → Array (Std.Sat.AIG.Decl α) → Type
-- Mathlib.MeasureTheory.Integral.Lebesgue.Sub
MeasureTheory.lintegral_sub' : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → ENNReal},
  AEMeasurable g μ →
    ∫⁻ (a : α), g a ∂μ ≠ ⊤ → g ≤ᵐ[μ] f → ∫⁻ (a : α), f a - g a ∂μ = ∫⁻ (a : α), f a ∂μ - ∫⁻ (a : α), g a ∂μ
-- Mathlib.RingTheory.PolynomialLaw.Basic
/-- The identity as a polynomial law  -/
PolynomialLaw.id : {R : Type u} →
  [inst : CommSemiring R] → {M : Type u_1} → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → M →ₚₗ[R] M
-- Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
/-- If `0 < c`, then `(fun t : ℝ ↦ t ^ a)` is integrable on `(c, ∞)` for all `a < -1`.  -/
integrableOn_Ioi_rpow_of_lt : ∀ {a c : ℝ}, a < -1 → 0 < c → MeasureTheory.IntegrableOn (fun t => t ^ a) (Set.Ioi c) MeasureTheory.volume
-- Batteries.Data.PairingHeap
/-- Or there is exactly one tree.  -/
Batteries.PairingHeapImp.Heap.NoSibling.node : ∀ {α : Type u_1} (a : α) (c : Batteries.PairingHeapImp.Heap α),
  (Batteries.PairingHeapImp.Heap.node a c Batteries.PairingHeapImp.Heap.nil).NoSibling
-- Lean.Elab.MutualInductive
Lean.Elab.Command.InductiveView.mk : Lean.Syntax →
  Lean.Syntax →
    Lean.Elab.Modifiers →
      Bool →
        Bool →
          Bool →
            Lean.Name →
              Lean.Name →
                List Lean.Name →
                  Lean.Syntax →
                    Option Lean.Syntax →
                      Array Lean.Elab.Command.CtorView →
                        Array Lean.Elab.Command.ComputedFieldView →
                          Array Lean.Elab.DerivingClassView →
                            Option (Lean.TSyntax `Lean.Parser.Command.docComment) →
                              Bool → Lean.Elab.Command.InductiveView
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [inst_2 : Std.LawfulBEqCmp cmp] (h : t.WF) {l : List (α × β)} {k : α}
  (contains_eq_false : (List.map Prod.fst l).contains k = false) {h' : k ∈ t.insertMany l},
  (t.insertMany l).getKey k h' = t.getKey k ⋯
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.foldlM_filterMap.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (x : Option β) → ((b : β) → motive (some b)) → (Unit → motive none) → motive x
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- A quadratic form on a module.  -/
QuadraticForm : (R : Type u) → (M : Type v) → [inst : CommSemiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → Type (max u v)
-- Mathlib.Algebra.Group.Equiv.Basic
MulEquiv.monoidHomCongrRight_apply : ∀ {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} [inst : MulOneClass M] [inst_1 : CommMonoid N₁]
  [inst_2 : CommMonoid N₂] (e : N₁ ≃* N₂) (hmn : M →* N₁), e.monoidHomCongrRight hmn = (↑e).comp hmn
-- Mathlib.Geometry.Convex.Hull
/-- **Alias** of the reverse direction of `Convexity.convexHull_nonempty`. -/
Convexity.Set.Nonempty.convexHull' : ∀ {R : Type u_1} {X : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X] {s : Set X}, s.Nonempty → ((Convexity.convexHull R) s).Nonempty