mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Algebra.Subalgebra.Directed
Subalgebra.instIsMulCommutative_iSup : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {ι : Type u_4}
  [Nonempty ι] [inst_4 : Preorder ι] [IsDirectedOrder ι] {S : ι →o Subalgebra R A}
  [hS : ∀ (i : ι), IsMulCommutative ↥(S i)], IsMulCommutative ↥(⨆ i, S i)
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
MeasureTheory.Measure.compProd_sum_left : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  {ι : Type u_3} [Countable ι] {μ : ι → MeasureTheory.Measure α} [∀ (i : ι), MeasureTheory.SFinite (μ i)],
  (MeasureTheory.Measure.sum μ).compProd κ = MeasureTheory.Measure.sum fun i => (μ i).compProd κ
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.Spanning.exists_isBase_subset : ∀ {α : Type u_2} {M : Matroid α} {S : Set α}, M.Spanning S → ∃ B, M.IsBase B ∧ B ⊆ S
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey_alter_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  [Inhabited α] {k : α} {f : Option (β k) → Option (β k)} {h : k ∈ m.alter k f}, (m.alter k f).getKey k h = k
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- The inverse functor of `ofDiagEquivalence.functor`.  -/
CategoryTheory.StructuredArrow.ofDiagEquivalence.inverse : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    (X : T × T) →
      CategoryTheory.Functor (CategoryTheory.StructuredArrow X.2 (CategoryTheory.Under.forget X.1))
        (CategoryTheory.StructuredArrow X (CategoryTheory.Functor.diag T))
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.forIn_filterMapWithPostcondition.match_1.eq_2 : ∀ {β₂ : Type u_1} (motive : Option β₂ → Sort u_2) (h_1 : (c : β₂) → motive (some c)) (h_2 : Unit → motive none),
  (match none with
    | some c => h_1 c
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.equivLaxBraidedFunctorPUnit_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.CommMon.equivLaxBraidedFunctorPUnit.inverse =
    CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided C
-- Init.Data.List.Basic
List.decidableLE : {α : Type u} → [DecidableEq α] → [inst : LT α] → [DecidableLT α] → (l₁ l₂ : List α) → Decidable (l₁ ≤ l₂)
-- Mathlib.Algebra.Order.BigOperators.Group.List
List.sum_min_le : ∀ {α : Type u_2} {M : Type u_3} [inst : AddMonoid M] [inst_1 : LinearOrder M] [AddLeftMono M] [AddRightMono M]
  (l : List α) (f g : α → M), (List.map (fun i => min (f i) (g i)) l).sum ≤ min (List.map f l).sum (List.map g l).sum
-- Mathlib.Analysis.Normed.Operator.NNNorm
ContinuousLinearMap.exists_lt_apply_of_lt_opNorm : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : NormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : DenselyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F)
  {r : ℝ}, r < ‖f‖ → ∃ x, ‖x‖ < 1 ∧ r < ‖f x‖
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.map_neg_eq_self : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Neg G] (μ : MeasureTheory.Measure G) [μ.IsNegInvariant],
  MeasureTheory.Measure.map Neg.neg μ = μ
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- If the product of `X` and `Y` exists, then every pair of morphisms `f : W ⟶ X` and `g : W ⟶ Y`
induces a morphism `prod.lift f g : W ⟶ X ⨯ Y`.  -/
CategoryTheory.Limits.prod.lift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W X Y : C} → [inst_1 : CategoryTheory.Limits.HasBinaryProduct X Y] → (W ⟶ X) → (W ⟶ Y) → (W ⟶ X ⨯ Y)
-- Init.Data.Int.Order
Int.le.intro : ∀ {a b : ℤ} (n : ℕ), a + ↑n = b → a ≤ b
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomLeft_action : ∀ {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 x' : C} (f : x ⟶ x') (y : C) (z : D),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj y z) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso x y z).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight f y) z)
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso x' y z).hom)
-- Mathlib.Topology.Algebra.UniformConvergence
instAddMonoidUniformOnFun.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [inst : AddMonoid β],
  instAddMonoidUniformOnFun =
    { toAdd := instAddUniformOnFun, add_assoc := ⋯, toZero := instZeroUniformOnFun, zero_add := ⋯, add_zero := ⋯,
      toNSMul := NSMul.ofSMul, nsmul_zero := ⋯, nsmul_succ := ⋯ }
-- Mathlib.CategoryTheory.Limits.Over
CategoryTheory.Under.liftCone_pt : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) {X : C} (f : X ⟶ c.pt),
  (CategoryTheory.Under.liftCone c f).pt = CategoryTheory.Under.mk f
-- Mathlib.Order.Filter.Finite
/-- **Alias** of `Set.Finite.eventuallyLE_iInter`. -/
Filter.EventuallyLE.biInter : ∀ {α : Type u} {l : Filter α} {ι : Type u_2} {s : Set ι},
  s.Finite → ∀ {f g : ι → Set α}, (∀ i ∈ s, f i ≤ᶠ[l] g i) → ⋂ i ∈ s, f i ≤ᶠ[l] ⋂ i ∈ s, g i
-- Mathlib.Data.NNRat.Defs
Mathlib.Tactic.Qify.nnratCast_lt : ∀ (a b : ℚ≥0), a < b ↔ ↑a < ↑b
-- Mathlib.Topology.Category.LightProfinite.Basic
instIsEquivalenceLightDiagramLightProfiniteLightDiagramToLightProfinite : lightDiagramToLightProfinite.IsEquivalence
-- Mathlib.Algebra.GCDMonoid.Basic
lcm_eq_of_associated_right : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {m n : α},
  Associated m n → ∀ (k : α), lcm k m = lcm k n
-- Std.Data.ByteSlice
_private.Std.Data.ByteSlice.0.ByteSlice.foldrM.loop : {β : Type v} → {m : Type v → Type w} → [Monad m] → (UInt8 → β → m β) → ByteSlice → ℕ → β → m β
-- Mathlib.CategoryTheory.Monoidal.Arrow
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.leftUnitor_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] [inst_3 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalClosed C] [inst_5 : CategoryTheory.BraidedCategory C] (X : CategoryTheory.Arrow C),
  CategoryTheory.MonoidalCategoryStruct.leftUnitor X = CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.leftUnitor X
-- Mathlib.CategoryTheory.Adjunction.Limits
/-- A left adjoint preserves colimits.  -/
CategoryTheory.Adjunction.leftAdjoint_preservesColimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G),
  CategoryTheory.Limits.PreservesColimitsOfSize.{v, u, v₁, v₂, u₁, u₂} F
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap
WeierstrassCurve.Affine.Point.sym2x_ne_zero : ∀ {R : Type u_1} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} [Nontrivial R] (P Q : W'.Point), P.sym2x Q ≠ 0
-- Mathlib.RingTheory.MvPolynomial.Basic
/-- The `R`-module `MvPolynomial σ R` is free.  -/
MvPolynomial.instFree : ∀ (σ : Type u) (R : Type v) [inst : CommSemiring R], Module.Free R (MvPolynomial σ R)
-- Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
arithGeom_zero_eq_mul_div : ∀ {R : Type u_1} {a b : R} [inst : Field R], a ≠ 1 → ∀ (n : ℕ), arithGeom a b 0 n = b * (a ^ n - 1) / (a - 1)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Subgraph.induce_union_connected : ∀ {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} {s t : Set V},
  (H.induce s).Preconnected → (H.induce t).Preconnected → (s ⊓ t).Nonempty → (H.induce (s ∪ t)).Connected
-- Init.Data.AC
Lean.Data.AC.Variable.mk.injEq : ∀ {α : Sort u} {op : α → α → α} (value : α) (neutral : Option (PLift (Std.LawfulIdentity op value))) (value_1 : α)
  (neutral_1 : Option (PLift (Std.LawfulIdentity op value_1))),
  ({ value := value, neutral := neutral } = { value := value_1, neutral := neutral_1 }) =
    (value = value_1 ∧ neutral ≍ neutral_1)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.equiv_empty_iff_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp},
  t.Equiv Std.TreeMap.empty ↔ t.isEmpty = true
-- Mathlib.Analysis.Normed.Group.Uniform
dist_self_div_left : ∀ {E : Type u_2} [inst : SeminormedCommGroup E] (a b : E), dist (a / b) a = ‖b‖
-- Mathlib.RingTheory.Multiplicity
emultiplicity_of_unit_right : ∀ {α : Type u_1} [inst : CommMonoid α] {a : α}, ¬IsUnit a → ∀ (u : αˣ), emultiplicity a ↑u = 0
-- Std.Data.DTreeMap.Raw.AdditionalOperations
Std.DTreeMap.Raw.instCoeTypeForall : {α : Type u} → Coe (Type v) (α → Type v)
-- Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
/-- For an adjunction `f ⊣ u`, `f` is an absolute left Kan lift of the identity along `u`.
The unit of this Kan lift is given by the unit of the adjunction.  -/
CategoryTheory.Bicategory.Adjunction.isAbsoluteLeftKanLift : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} →
      {f : a ⟶ b} →
        {u : b ⟶ a} →
          (adj : CategoryTheory.Bicategory.Adjunction f u) → (CategoryTheory.Bicategory.LeftLift.mk f adj.unit).IsAbsKan
-- Init.Core
/-- The default priority for spawned tasks, also the lowest priority: `0`.  -/
Task.Priority.default : Task.Priority
-- Mathlib.GroupTheory.FiniteAbelian.Basic
Module.finite_of_fg_torsion : ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : Module ℤ M] [Module.Finite ℤ M], Module.IsTorsion ℤ M → Finite M
-- Mathlib.Analysis.Analytic.Order
analyticOrderAt_of_not_analyticAt : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜}, ¬AnalyticAt 𝕜 f z₀ → analyticOrderAt f z₀ = 0
-- Mathlib.Tactic.ITauto
/-- Add `A` to the context `Γ` with proof `p`. This version of `Context.add` takes a continuation
and a target proposition `B`, so that in the case that `⊥` is found we can skip the continuation
and just prove `B` outright.  -/
Mathlib.Tactic.ITauto.Context.withAdd : Mathlib.Tactic.ITauto.Context →
  Mathlib.Tactic.ITauto.IProp →
    Mathlib.Tactic.ITauto.Proof →
      Mathlib.Tactic.ITauto.IProp →
        (Mathlib.Tactic.ITauto.Context → Mathlib.Tactic.ITauto.IProp → StateM ℕ (Bool × Mathlib.Tactic.ITauto.Proof)) →
          StateM ℕ (Bool × Mathlib.Tactic.ITauto.Proof)
-- Mathlib.Analysis.Convex.StrictConvexBetween
Isometry.coe_affineIsometryOfStrictConvexSpace : ∀ {E : Type u_3} {F : Type u_4} {PE : Type u_5} {PF : Type u_6} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ E] [inst_3 : NormedSpace ℝ F] [inst_4 : StrictConvexSpace ℝ E]
  [inst_5 : MetricSpace PE] [inst_6 : MetricSpace PF] [inst_7 : NormedAddTorsor E PE] [inst_8 : NormedAddTorsor F PF]
  {f : PF → PE} (hi : Isometry f), ⇑hi.affineIsometryOfStrictConvexSpace = f
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosDef.conjTranspose_mul_self : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
  [inst_3 : Fintype n] [inst_4 : Fintype m] [StarOrderedRing R] [NoZeroDivisors R] (A : Matrix m n R),
  Function.Injective A.mulVec → (A.conjTranspose * A).PosDef
-- Lean.Elab.ConfigEval.Instances
Lean.Elab.ConfigEval.EvalTerm.instNat : Lean.Elab.ConfigEval.EvalTerm ℕ
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Subtype.instMeasurableSpace : {α : Type u_6} → {p : α → Prop} → [m : MeasurableSpace α] → MeasurableSpace (Subtype p)
-- Mathlib.Algebra.Homology.Homotopy
_private.Mathlib.Algebra.Homology.Homotopy.0.Homotopy.mkInductiveAux₁.match_1.eq_3 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (n : ℕ) → motive n.succ.succ),
  (match n.succ.succ with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | n.succ.succ => h_3 n) =
    h_3 n
-- Mathlib.Data.Multiset.Count
Multiset.countP_cons : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (b : α) (s : Multiset α),
  Multiset.countP p (b ::ₘ s) = Multiset.countP p s + if p b then 1 else 0
-- Mathlib.ModelTheory.Syntax
_private.Mathlib.ModelTheory.Syntax.0.FirstOrder.Language.BoundedFormula.castLE.match_1.eq_3 : ∀ {L : FirstOrder.Language} {α : Type u_3} (motive : (x x_1 : ℕ) → x ≤ x_1 → L.BoundedFormula α x → Sort u_4)
  (_m _n : ℕ) (h : _m ≤ _n) (l : ℕ) (R : L.Relations l) (ts : Fin l → L.Term (α ⊕ Fin _m))
  (h_1 : (_m _n : ℕ) → (_h : _m ≤ _n) → motive _m _n _h FirstOrder.Language.BoundedFormula.falsum)
  (h_2 :
    (_m _n : ℕ) →
      (h : _m ≤ _n) → (t₁ t₂ : L.Term (α ⊕ Fin _m)) → motive _m _n h (FirstOrder.Language.BoundedFormula.equal t₁ t₂))
  (h_3 :
    (_m _n : ℕ) →
      (h : _m ≤ _n) →
        (l : ℕ) →
          (R : L.Relations l) →
            (ts : Fin l → L.Term (α ⊕ Fin _m)) → motive _m _n h (FirstOrder.Language.BoundedFormula.rel R ts))
  (h_4 : (_m _n : ℕ) → (h : _m ≤ _n) → (f₁ f₂ : L.BoundedFormula α _m) → motive _m _n h (f₁.imp f₂))
  (h_5 : (_m _n : ℕ) → (h : _m ≤ _n) → (f : L.BoundedFormula α (_m + 1)) → motive _m _n h f.all),
  (match _m, _n, h, FirstOrder.Language.BoundedFormula.rel R ts with
    | _m, _n, _h, FirstOrder.Language.BoundedFormula.falsum => h_1 _m _n _h
    | _m, _n, h, FirstOrder.Language.BoundedFormula.equal t₁ t₂ => h_2 _m _n h t₁ t₂
    | _m, _n, h, FirstOrder.Language.BoundedFormula.rel R ts => h_3 _m _n h l R ts
    | _m, _n, h, f₁.imp f₂ => h_4 _m _n h f₁ f₂
    | _m, _n, h, f.all => h_5 _m _n h f) =
    h_3 _m _n h l R ts
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.toEquiv_symm : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B] (e : A ≃ₗc[R] B), e.symm.toEquiv = e.toEquiv.symm
-- Mathlib.CategoryTheory.Monoidal.Transport
CategoryTheory.Monoidal.transportStruct_rightUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X : D),
  CategoryTheory.MonoidalCategoryStruct.rightUnitor X =
    e.functor.mapIso
        (CategoryTheory.MonoidalCategory.whiskerLeftIso (e.inverse.obj X)
            (e.unitIso.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).symm ≪≫
          CategoryTheory.MonoidalCategoryStruct.rightUnitor (e.inverse.obj X)) ≪≫
      e.counitIso.app X
-- Lean.Environment
/-- Default access mode. Like `local` but panics when trying to modify the state on anything but the
main environment branch. For extensions that fulfill this requirement, all modes functionally
coincide with `local` but this is the safest and most efficient choice in that case, preventing
accidental misuse.

This mode is suitable for extensions that are modified only at the command elaboration level
before any environment forks in the command, and in particular for extensions that are modified
only at the very beginning of the file.
 -/
Lean.EnvExtension.AsyncMode.mainOnly : Lean.EnvExtension.AsyncMode
-- Mathlib.LinearAlgebra.QuadraticForm.Radical
QuadraticMap.polarBilin.eq_1 : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticMap R M N),
  Q.polarBilin = LinearMap.mk₂ R (QuadraticMap.polar ⇑Q) ⋯ ⋯ ⋯ ⋯
-- Mathlib.Probability.Process.LocalProperty
ProbabilityTheory.IsLocalizingSequence.isPrelocalizingSequence_inf_extraction : ∀ {ι : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω}
  [inst : ConditionallyCompleteLinearOrderBot ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι]
  {𝓕 : MeasureTheory.Filtration ι mΩ} [SecondCountableTopology ι] [MeasureTheory.IsFiniteMeasure P] [NoMaxOrder ι]
  {τ : ℕ → Ω → WithTop ι} {σ : ℕ → ℕ → Ω → WithTop ι},
  ProbabilityTheory.IsLocalizingSequence 𝓕 τ P →
    (∀ (n : ℕ), ProbabilityTheory.IsLocalizingSequence 𝓕 (σ n) P) →
      ∃ nk, StrictMono nk ∧ ProbabilityTheory.IsPreLocalizingSequence 𝓕 (fun i ω => min (τ i ω) (σ i (nk i) ω)) P
-- Mathlib.Data.ENNReal.Operations
ENNReal.sub_add_eq_add_sub : ∀ {a b c : ENNReal}, b ≤ a → b ≠ ⊤ → a - b + c = a + c - b
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.toContinuousMapLinearMap_apply : ∀ (α : Type u) (β : Type v) (𝕜 : Type u_2) [inst : PseudoMetricSpace 𝕜] [inst_1 : TopologicalSpace α]
  [inst_2 : PseudoMetricSpace β] [inst_3 : Semiring 𝕜] [inst_4 : AddCommMonoid β] [inst_5 : Module 𝕜 β]
  [inst_6 : IsBoundedSMul 𝕜 β] [inst_7 : BoundedAdd β] [inst_8 : ContinuousAdd β]
  (self : BoundedContinuousFunction α β),
  (BoundedContinuousFunction.toContinuousMapLinearMap α β 𝕜) self = self.toContinuousMap
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.SubgroupNormal.mem_comm : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G},
  H ≤ K → ∀ [hN : (H.subgroupOf K).Normal] {a b : G}, b ∈ K → a * b ∈ H → b * a ∈ H
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.singleton_mul_inter : ∀ {α : Type u_2} [inst : Mul α] [IsLeftCancelMul α] [inst_2 : DecidableEq α] (a : α) (s t : Finset α),
  {a} * (s ∩ t) = {a} * s ∩ ({a} * t)
-- Mathlib.Analysis.Calculus.ContDiff.Defs
/-- **Alias** of `contDiffWithinAt_sdiff_singleton`. -/
contDiffWithinAt_diff_singleton : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {x : E} {n : WithTop ℕ∞} {y : E}, ContDiffWithinAt 𝕜 n f (s \ {y}) x ↔ ContDiffWithinAt 𝕜 n f s x
-- Mathlib.Algebra.Order.Module.PositiveLinearMap
PositiveLinearMap.instFunLike : {R : Type u_1} →
  {E₁ : Type u_2} →
    {E₂ : Type u_3} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid E₁] →
          [inst_2 : PartialOrder E₁] →
            [inst_3 : AddCommMonoid E₂] →
              [inst_4 : PartialOrder E₂] → [inst_5 : Module R E₁] → [inst_6 : Module R E₂] → FunLike (E₁ →ₚ[R] E₂) E₁ E₂
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- The action by a subsemiring is the action by the underlying semiring.  -/
Subsemiring.mulActionWithZero : {R' : Type u_1} →
  {α : Type u_2} →
    [inst : Semiring R'] →
      [inst_1 : Zero α] → [MulActionWithZero R' α] → (S : Subsemiring R') → MulActionWithZero (↥S) α
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.toEquiv_uniformEquivProd : ∀ (p : ENNReal) (α : Type u_2) (β : Type u_3) [inst : UniformSpace α] [inst_1 : UniformSpace β],
  (WithLp.uniformEquivProd p α β).toEquiv = WithLp.equiv p (α × β)
-- Mathlib.CategoryTheory.Category.TwoP
TwoP.swapEquiv_functor_obj_X : ∀ (X : TwoP), (TwoP.swapEquiv.functor.obj X).X = X.X
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.zero_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] (x : ↥⊤), ↑0 x = 0
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.zero_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Zero β] (x : α),
  0 x = 0
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.eq_pellZd : ∀ {a : ℕ} (a1 : 1 < a) (b : ℤ√↑(Pell.d✝ a1)), 1 ≤ b → Pell.IsPell b → ∃ n, b = Pell.pellZd a1 n
-- Mathlib.Analysis.Convex.Strict
strictConvex_Iio : ∀ {𝕜 : Type u_1} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : TopologicalSpace β]
  [inst_3 : AddCommMonoid β] [inst_4 : LinearOrder β] [IsOrderedCancelAddMonoid β] [OrderTopology β]
  [inst_7 : Module 𝕜 β] [PosSMulStrictMono 𝕜 β] (r : β), StrictConvex 𝕜 (Set.Iio r)
-- Init.Data.Nat.Basic
Nat.instTransLtLe : Trans (fun x1 x2 => x1 < x2) (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 < x2
-- Mathlib.CategoryTheory.ConcreteCategory.EpiMono
CategoryTheory.ConcreteCategory.surjective_of_epi_of_preservesPushout : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {X Y : C}
  (f : X ⟶ Y) [CategoryTheory.Epi f]
  [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingSpan (CategoryTheory.forget C)],
  Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Init.Data.SInt.Bitwise
Int64.ofBitVec_and : ∀ (a b : BitVec 64), Int64.ofBitVec (a &&& b) = Int64.ofBitVec a &&& Int64.ofBitVec b
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero
SSet.π₀.comp_fromChainComplexXZero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) (R : C) (x : X.obj (Opposite.op { len := 0 })),
  CategoryTheory.CategoryStruct.comp (X.ιChainComplex x) (SSet.π₀.fromChainComplexXZero X R) =
    CategoryTheory.Limits.Sigma.ι (fun x => R) (SSet.π₀.mk x)
-- Mathlib.Data.Nat.Sqrt
/-- There are no perfect squares strictly between m² and (m+1)²  -/
Nat.not_exists_sq : ∀ {m n : ℕ}, m * m < n → n < (m + 1) * (m + 1) → ¬∃ t, t * t = n
-- Mathlib.Data.Nat.Cast.Defs
Nat.cast_one : ∀ {R : Type u_1} [inst : AddMonoidWithOne R], ↑1 = 1
-- Init.Data.SInt.Lemmas
ISize.le_iff_lt_or_eq : ∀ {a b : ISize}, a ≤ b ↔ a < b ∨ a = b
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData_left_K : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  (r r' : ℤ) (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq pq' pq'' : κ) (hpq : (c r).prev pq' = pq)
  (hpq' : (c r).next pq' = pq'') (i₀' i₀ i₁ i₂ i₃ i₃' : ι) (hi₀' : i₀' = data.i₀ r' pq' ⋯) (hi₀ : i₀ = data.i₀ r pq' ⋯)
  (hi₁ : i₁ = data.i₁ pq') (hi₂ : i₂ = data.i₂ pq') (hi₃ : i₃ = data.i₃ r pq' ⋯) (hi₃' : i₃' = data.i₃ r' pq' ⋯)
  (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq') [inst_3 : X.HasSpectralSequence data]
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData._auto_3),
  (CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData X data r r' hrr' hr pq pq' pq'' hpq hpq' i₀' i₀
          i₁ i₂ i₃ i₃' hi₀' hi₀ hi₁ hi₂ hi₃ hi₃' n₀ n₁ n₂ hn₁' hn₁ hn₂).left.K =
    X.E (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯
-- Std.Time.DateTime.Timestamp
Std.Time.Timestamp.instHAddDuration : HAdd Std.Time.Timestamp Std.Time.Duration Std.Time.Timestamp
-- Mathlib.Algebra.Lie.Weights.RootSystem
LieAlgebra.IsKilling.instIsReducedSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem : ∀ {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] [inst_7 : LieModule.IsTriangularizable K (↥H) L],
  (LieAlgebra.IsKilling.rootSystem H).IsReduced
-- Mathlib.Order.Heyting.Basic
compl_sup : ∀ {α : Type u_2} [inst : HeytingAlgebra α] {a b : α}, (a ⊔ b)ᶜ = aᶜ ⊓ bᶜ
-- Mathlib.Analysis.Normed.Algebra.QuaternionExponential
Quaternion.re_exp : ∀ (q : Quaternion ℝ), (NormedSpace.exp q).re = NormedSpace.exp q.re * Real.cos ‖q - ↑q.re‖