mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Preadditive.Yoneda.Limits
CategoryTheory.preservesLimits_preadditiveYoneda_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (X : C),
  CategoryTheory.Limits.PreservesLimits (CategoryTheory.preadditiveYoneda.obj X)
-- Mathlib.Data.Multiset.ZeroCons
Multiset.eq_zero_iff_forall_notMem : ∀ {α : Type u_1} {s : Multiset α}, s = 0 ↔ ∀ (a : α), a ∉ s
-- Mathlib.Dynamics.BirkhoffSum.Basic
Function.IsFixedPt.birkhoffSum_eq : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] {f : α → α} {x : α},
  Function.IsFixedPt f x → ∀ (g : α → M) (n : ℕ), birkhoffSum f g n x = n • g x
-- Init.Grind.Lemmas
Lean.Grind.eval_congr₂ : ∀ {α₁ : Sort u} {α₂ : Sort v} {β : Sort w} {f : α₁ → α₂ → β} {a₁ a₁' : α₁} {a₂ a₂' : α₂} {b : β},
  a₁ = a₁' → a₂ = a₂' → f a₁' a₂' = b → f a₁ a₂ = b
-- Mathlib.Data.List.Cycle
Cycle.toFinset_eq_nil : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Cycle α}, s.toFinset = ∅ ↔ s = Cycle.nil
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.LocalTimeType.mk.sizeOf_spec : ∀ (gmtOffset : ℤ) (isDst : Bool) (abbreviationIndex : UInt8),
  sizeOf { gmtOffset := gmtOffset, isDst := isDst, abbreviationIndex := abbreviationIndex } =
    1 + sizeOf gmtOffset + sizeOf isDst + sizeOf abbreviationIndex
-- Mathlib.Algebra.BigOperators.WithTop
/-- A sum is finite iff all terms are finite.  -/
WithTop.sum_lt_top : ∀ {ι : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] {s : Finset ι} {f : ι → WithTop M} [inst_1 : LT M],
  ∑ i ∈ s, f i < ⊤ ↔ ∀ i ∈ s, f i < ⊤
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
/-- Note that `0 : 0 →qᵢ Q` alone would not be well-typed as the RHS.  -/
QuadraticMap.Isometry.proj_comp_single_of_ne : ∀ {ι : Type u_1} {R : Type u_2} {P : Type u_7} {Mᵢ : ι → Type u_8} [inst : CommSemiring R]
  [inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)] [inst_2 : AddCommMonoid P] [inst_3 : (i : ι) → Module R (Mᵢ i)]
  [inst_4 : Module R P] [inst_5 : Fintype ι] [inst_6 : DecidableEq ι] {i j : ι} (h : i ≠ j)
  (Q : QuadraticMap R (Mᵢ i) P),
  (QuadraticMap.Isometry.proj i Q).comp (QuadraticMap.Isometry.single (Pi.single i Q) j) =
    QuadraticMap.Isometry.comp 0 (QuadraticMap.Isometry.ofEq ⋯)
-- Mathlib.Algebra.Ring.Defs
one_add_mul : ∀ {α : Type u} [inst : Add α] [inst_1 : MulOneClass α] [RightDistribClass α] (a b : α), (1 + a) * b = b + a * b
-- Mathlib.GroupTheory.Torsion
/-- The torsion submonoid of a commutative monoid.

(Note that by `IsMulTorsion.group` torsion monoids are truthfully groups.)
 -/
CommMonoid.torsion : (G : Type u_1) → [inst : CommMonoid G] → Submonoid G
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instFunLike : {α : Type u_1} → {β : Type u_2} → [inst : MeasurableSpace α] → FunLike (MeasureTheory.SimpleFunc α β) α β
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.map_congr : ∀ {α : Type u} {β : Type v} (f : α → β) {s t : Stream'.WSeq α}, s ~ʷ t → Stream'.WSeq.map f s ~ʷ Stream'.WSeq.map f t
-- Mathlib.CategoryTheory.Presentable.Dense
CategoryTheory.IsCardinalAccessibleCategory.final_toCostructuredArrow : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {κ : Cardinal.{w}} [inst_1 : Fact κ.IsRegular] {J : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} J] [CategoryTheory.EssentiallySmall.{w, v', u'} J]
  [CategoryTheory.IsCardinalFiltered J κ] {X : C} (p : (CategoryTheory.isCardinalPresentable C κ).ColimitOfShape J X),
  p.toCostructuredArrow.Final
-- Mathlib.Data.Matrix.Composition
/-- `Matrix.comp` as `RingEquiv`  -/
Matrix.compRingEquiv : (I : Type u_1) →
  (J : Type u_2) →
    (R : Type u_5) →
      [inst : AddCommMonoid R] →
        [inst_1 : Mul R] →
          [inst_2 : Fintype I] → [inst_3 : Fintype J] → Matrix I I (Matrix J J R) ≃+* Matrix (I × J) (I × J) R
-- Mathlib.Data.Ordmap.Ordset
Ordset.Empty.instDecidablePred : {α : Type u_1} → [inst : Preorder α] → DecidablePred Ordset.Empty
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
/-- If `G.IsBipartiteWith s t` and `v ∈ s`, then the neighbor finset of `v` is the set of vertices
"above" `v` according to the adjacency relation of `G`.  -/
SimpleGraph.isBipartiteWith_bipartiteAbove : ∀ {V : Type u_1} {v : V} {G : SimpleGraph V} {s t : Finset V} [inst : Fintype ↑(G.neighborSet v)]
  [inst_1 : DecidableRel G.Adj], G.IsBipartiteWith ↑s ↑t → v ∈ s → G.neighborFinset v = Finset.bipartiteAbove G.Adj t v
-- Mathlib.Order.Filter.Map
Filter.comap_inf_principal_range : ∀ {α : Type u_1} {β : Type u_2} {g : Filter β} {m : α → β},
  Filter.comap m (g ⊓ Filter.principal (Set.range m)) = Filter.comap m g
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- Schwartz functions are dense in `Lp`.  -/
SchwartzMap.denseRange_toLpCLM : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] [inst_4 : MeasurableSpace E] [inst_5 : OpensMeasurableSpace E]
  [inst_6 : SecondCountableTopologyEither E F] [FiniteDimensional ℝ E] [BorelSpace E] {p : ENNReal},
  p ≠ ⊤ →
    ∀ [hp' : Fact (1 ≤ p)] {μ : MeasureTheory.Measure E} [hμ : μ.HasTemperateGrowth]
      [MeasureTheory.IsFiniteMeasureOnCompacts μ], DenseRange ⇑(SchwartzMap.toLpCLM ℝ F p μ)
-- Std.Time.Time.Unit.Millisecond
/-- `Ordinal` represents a bounded value for milliseconds, ranging from 0 to 999 milliseconds.
 -/
Std.Time.Millisecond.Ordinal : Type
-- Mathlib.Analysis.RCLike.ContinuousMap
ContinuousMap.spectrum_realToRCLike : ∀ {X : Type u_1} (𝕜 : Type u_2) [inst : TopologicalSpace X] [inst_1 : RCLike 𝕜] (f : C(X, ℝ)),
  spectrum ℝ (ContinuousMap.realToRCLike 𝕜 f) = spectrum ℝ f
-- Mathlib.Order.Hom.Basic
OrderIso.toRelIsoLT_symm : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β),
  e.symm.toRelIsoLT = e.toRelIsoLT.symm
-- Mathlib.Algebra.Group.Conj
ConjClasses.mk_bijective : ∀ {α : Type u} [inst : CommMonoid α], Function.Bijective ConjClasses.mk
-- Mathlib.Geometry.Manifold.IntegralCurve.Transform
isMIntegralCurveOn_comp_sub : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {γ : ℝ → M}
  {v : (x : M) → TangentSpace I x} {s : Set ℝ} {dt : ℝ},
  IsMIntegralCurveOn (γ ∘ fun x => x - dt) v {t | t - dt ∈ s} ↔ IsMIntegralCurveOn γ v s
-- Mathlib.Order.LatticeIntervals
Set.Icc.semilatticeSup : {α : Type u_1} → {a b : α} → [inst : SemilatticeSup α] → SemilatticeSup ↑(Set.Icc a b)
-- Mathlib.Analysis.Complex.Order
Complex.not_lt_iff : ∀ {z w : ℂ}, ¬z < w ↔ w.re ≤ z.re ∨ z.im ≠ w.im
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.ServerInfo.name : Lean.Lsp.ServerInfo → String
-- Init.Data.Array.Monadic
Array.mapM_unattach : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {P : α → Prop}
  {xs : Array (Subtype P)} {f : α → m β},
  Array.mapM f xs.unattach =
    Array.mapM
      (fun x =>
        match x with
        | ⟨x, h⟩ => binderNameHint x f (binderNameHint h () (f (wfParam x))))
      xs
-- Mathlib.Analysis.InnerProductSpace.LaxMilgram
IsCoercive.ker_eq_bot : ∀ {V : Type u} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : CompleteSpace V]
  {B : V →L[ℝ] V →L[ℝ] ℝ}, IsCoercive B → (↑(InnerProductSpace.continuousLinearMapOfBilin B)).ker = ⊥
-- Mathlib.Analysis.Calculus.DiffContOnCl
DiffContOnCl.mono : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s t : Set E},
  DiffContOnCl 𝕜 f s → t ⊆ s → DiffContOnCl 𝕜 f t
-- Std.Http.Data.URI.Encoding
Std.Http.URI.EncodedString.instRepr : {r : UInt8 → Bool} → Repr (Std.Http.URI.EncodedString r)
-- Mathlib.Topology.GDelta.Basic
IsNowhereDense.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] (s : Set X), IsNowhereDense s = (interior (closure s) = ∅)
-- Mathlib.Data.Fin.Tuple.NatAntidiagonal
List.Nat.antidiagonalTuple_zero_succ : ∀ (n : ℕ), List.Nat.antidiagonalTuple 0 (n + 1) = []
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.hasSum_norm : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)],
  0 < p.toReal → ∀ (f : ↥(lp E p)), HasSum (fun i => ‖↑f i‖ ^ p.toReal) (‖f‖ ^ p.toReal)
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.PollSources.mk : {α β : Type} →
  Option α →
    Option ℕ →
      Option (Std.Channel (Except IO.Error (Std.Http.Response β))) →
        Option β →
          Option Std.Http.Body.Stream →
            Std.Time.Millisecond.Offset →
              Option Std.Time.Millisecond.Offset →
                Option Std.Time.Timestamp → Std.CancellationContext → Std.Http.Server.Connection.PollSources✝ α β
-- Mathlib.Algebra.Field.Rat
NNRat.instZPow : Pow ℚ≥0 ℤ
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Set.prod.eq_1 : ∀ {α : Type u} {β : Type v} (s : Set α) (t : Set β), s.prod t = {p | p.1 ∈ s ∧ p.2 ∈ t}
-- Mathlib.Logic.Denumerable
Nat.Subtype.ofNat_range : ∀ {s : Set ℕ} [inst : Infinite ↑s] [inst_1 : DecidablePred fun x => x ∈ s], Set.range (Nat.Subtype.ofNat s) = Set.univ
-- Aesop.Stats.Basic
Aesop.instInhabitedGoalKind : Inhabited Aesop.GoalKind
-- Lean.Declaration
Lean.Declaration.axiomDecl.inj : ∀ {val val_1 : Lean.AxiomVal}, Lean.Declaration.axiomDecl val = Lean.Declaration.axiomDecl val_1 → val = val_1
-- Mathlib.LinearAlgebra.UnitaryGroup
Matrix.UnitaryGroup.toLin'_mul : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {α : Type v} [inst_2 : CommRing α] [inst_3 : StarRing α]
  (A B : ↥(Matrix.unitaryGroup n α)),
  Matrix.UnitaryGroup.toLin' (A * B) = Matrix.UnitaryGroup.toLin' A ∘ₗ Matrix.UnitaryGroup.toLin' B
-- Mathlib.GroupTheory.OreLocalization.OreSet
/-- Common factors on the right can be turned into common factors on the left, a weak form of
cancellability.  -/
OreLocalization.OreSet.ore_right_cancel : ∀ {R : Type u_1} {inst : Monoid R} {S : Submonoid R} [self : OreLocalization.OreSet S] (r₁ r₂ : R) (s : ↥S),
  r₁ * ↑s = r₂ * ↑s → ∃ s', ↑s' * r₁ = ↑s' * r₂
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.ext_iff : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {S : C} {x y : CategoryTheory.PreZeroHypercover S},
  x = y ↔ x.I₀ = y.I₀ ∧ x.X ≍ y.X ∧ x.f ≍ y.f
-- Mathlib.CategoryTheory.ConnectedComponents
/-- The disjoint union of `J`'s connected components, written explicitly as a sigma-type with the
category structure.
This category is equivalent to `J`.
 -/
CategoryTheory.Decomposed : (J : Type u₁) → [CategoryTheory.Category.{v₁, u₁} J] → Type u₁
-- Mathlib.CategoryTheory.CommSq
CategoryTheory.CommSq.flip : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z}
  {i : Y ⟶ Z}, CategoryTheory.CommSq f g h i → CategoryTheory.CommSq g f i h
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.map_dblY : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] {W' : WeierstrassCurve.Projective R} (f : R →+* S)
  (P : Fin 3 → R), (W'.map f).dblY (⇑f ∘ P) = f (W'.dblY P)
-- Init.Data.Array.OfFn
Array.ofFn_zero : ∀ {α : Type u_1} {f : Fin 0 → α}, Array.ofFn f = #[]
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ico_inter_Ico : ∀ {α : Type u_1} [inst : LinearOrder α] {a₁ a₂ b₁ b₂ : α},
  Set.Ico a₁ b₁ ∩ Set.Ico a₂ b₂ = Set.Ico (max a₁ a₂) (min b₁ b₂)
-- Init.Data.List.Sublist
List.isSublist.eq_1 : ∀ {α : Type u} [inst : BEq α] (x : List α), [].isSublist x = true
-- Init.Data.SInt.Bitwise
Int8.shiftLeft_or : ∀ {a b c : Int8}, (a ||| b) <<< c = a <<< c ||| b <<< c
-- Init.Data.List.Impl
/-- Auxiliary for `filterMap`: `filterMap.go f l = acc.toList ++ filterMap f l`  -/
List.filterMapTR.go : {α : Type u_1} → {β : Type u_2} → (α → Option β) → List α → Array β → List β
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_insertIfNew : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k a : α} {v : β k},
  Std.DTreeMap.Internal.Impl.contains a (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl =
    (compare k a == Ordering.eq || Std.DTreeMap.Internal.Impl.contains a t)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α],
  (↑m).WF →
    ∀ {l : List α} {k : α},
      m.contains k = false →
        l.contains k = false → (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l)).getKey! k = default
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddSubsemigroup.instPartialOrder.eq_1 : ∀ {M : Type u_1} [inst : Add M], AddSubsemigroup.instPartialOrder = PartialOrder.ofSetLike (AddSubsemigroup M) M
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.ratio_id : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α], Dilation.ratio (Dilation.id α) = 1
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.inr.eq_1 : ∀ (A : Type u_2) (B : Type u_3) [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B], ContinuousMonoidHom.inr A B = ContinuousMonoidHom.prod 1 (ContinuousMonoidHom.id B)
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.LocallyIntegrable.mono_enorm : ∀ {X : Type u_1} {ε : Type u_3} {ε' : Type u_4} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace ε] [inst_3 : ContinuousENorm ε] [inst_4 : TopologicalSpace ε']
  [inst_5 : ContinuousENorm ε'] {f : X → ε} {μ : MeasureTheory.Measure X},
  MeasureTheory.LocallyIntegrable f μ →
    ∀ {g : X → ε'},
      MeasureTheory.AEStronglyMeasurable g μ → (∀ᵐ (x : X) ∂μ, ‖g x‖ₑ ≤ ‖f x‖ₑ) → MeasureTheory.LocallyIntegrable g μ
-- Std.Sat.AIG.Lemmas
Std.Sat.AIG.Ref.denote_not : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {assign : α → Bool} {aig : Std.Sat.AIG α} {ref : aig.Ref},
  ⟦assign, { aig := aig, ref := ref.not }⟧ = !⟦assign, { aig := aig, ref := ref }⟧
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.root_isInv : ∀ {R : Type u_1} [inst : CommRing R] (r : R),
  (AdjoinRoot.of (Polynomial.C r * Polynomial.X - 1)) r * AdjoinRoot.root (Polynomial.C r * Polynomial.X - 1) = 1
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.inl_smul : ∀ {S : Type u_2} {R : Type u} (M : Type v) [inst : Monoid S] [inst_1 : AddMonoid M] [inst_2 : SMul S R]
  [inst_3 : DistribMulAction S M] (s : S) (r : R), TrivSqZeroExt.inl (s • r) = s • TrivSqZeroExt.inl r
-- Mathlib.Algebra.Lie.BaseChange
LieModule.toEnd_baseChange : ∀ (R : Type u_1) (A : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : LieAlgebra R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M]
  [inst_6 : LieModule R L M] [inst_7 : CommRing A] [inst_8 : Algebra R A] (x : L),
  (LieModule.toEnd A (TensorProduct R A L) (TensorProduct R A M)) (1 ⊗ₜ[R] x) =
    LinearMap.baseChange A ((LieModule.toEnd R L M) x)
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMul : ∀ {R : Type u} [inst : NonAssocSemiring R],
  CanLift (Set R) (Subsemiring R) SetLike.coe fun s =>
    0 ∈ s ∧ (∀ {x y : R}, x ∈ s → y ∈ s → x + y ∈ s) ∧ 1 ∈ s ∧ ∀ {x y : R}, x ∈ s → y ∈ s → x * y ∈ s
-- Init.MetaTypes
/-- Unfolds all constants except those tagged as `@[irreducible]`. Used for type checking
user-written terms where we expect the input to be correct and want to try hard.  -/
Lean.Meta.TransparencyMode.default : Lean.Meta.TransparencyMode
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.mem_of_mem_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α (fun x => Unit) cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp],
  t.WF → ∀ {l : List α} {k : α}, l.contains k = false → k ∈ Std.DTreeMap.Raw.Const.insertManyIfNewUnit t l → k ∈ t
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get!_alter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k k' : α}
  [inst : Inhabited β] {f : Option β → Option β},
  Std.DTreeMap.Const.get! (Std.DTreeMap.Const.alter t k f) k' =
    if cmp k k' = Ordering.eq then (f (Std.DTreeMap.Const.get? t k)).get! else Std.DTreeMap.Const.get! t k'
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
/-- The measurability of a set `A` is equivalent to the measurability of the indicator function
which takes a constant value `b ≠ 0` on a set `A` and `0` elsewhere.  -/
measurable_indicator_const_iff : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [inst : Zero β]
  [MeasurableSingletonClass β] (b : β) [NeZero b], Measurable (s.indicator fun x => b) ↔ MeasurableSet s
-- Mathlib.AlgebraicGeometry.Stalk
/-- **Alias** of `AlgebraicGeometry.Spec.fromSpecStalk_eq`. -/
AlgebraicGeometry.Scheme.Spec_fromSpecStalk : ∀ (R : CommRingCat) (x : ↥(AlgebraicGeometry.Spec R)),
  (AlgebraicGeometry.Spec R).fromSpecStalk x =
    AlgebraicGeometry.Spec.map
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso R).inv
        ((AlgebraicGeometry.Spec R).presheaf.germ ⊤ x trivial))
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
/-- Split the sum defining a Liouville number into the first `k` terms and the rest.  -/
LiouvilleNumber.partialSum_add_remainder : ∀ {m : ℝ}, 1 < m → ∀ (k : ℕ), LiouvilleNumber.partialSum m k + LiouvilleNumber.remainder m k = liouvilleNumber m
-- Lean.Elab.Tactic.Omega.MinNatAbs
Lean.Elab.Tactic.Omega.List.nonzeroMinimum_pos : ∀ {a : ℕ} {xs : List ℕ}, a ∈ xs → a ≠ 0 → 0 < Lean.Elab.Tactic.Omega.List.nonzeroMinimum xs
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.IsIndex.eq_of_isType₂_δ : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} {x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N} {d : ℕ}
  {hd : x.dim = d + 1} {l : Fin (d + 1)},
  SSet.prodStdSimplex.pairingCore.IsIndex x hd l.succ →
    ∀ {u : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N},
      SSet.prodStdSimplex.pairingCore.IsType₂ u →
        ∀ (i : Fin (d + 2)),
          { dim := u.dim, simplex := u.simplex } =
              { dim := d,
                simplex :=
                  (CategoryTheory.ConcreteCategory.hom
                      (CategoryTheory.SimplicialObject.δ
                        (CategoryTheory.MonoidalCategoryStruct.tensorObj (SSet.stdSimplex.obj { len := m + 1 })
                          (SSet.stdSimplex.obj { len := n }))
                        i))
                    (x.cast hd).simplex } →
            i = l.castSucc ∨ i = l.succ
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
/-- For a `WeierstrassCurve` defined over a field of characteristic = 3,
there is an explicit change of variables of it to `WeierstrassCurve.IsCharThreeNF`, that is,
`Y² = X³ + a₂X² + a₆` (`WeierstrassCurve.IsCharThreeJNeZeroNF`) or
`Y² = X³ + a₄X + a₆` (`WeierstrassCurve.IsShortNF`).
It is the composition of an explicit change of variables with
`WeierstrassCurve.toShortNFOfCharThree`.  -/
WeierstrassCurve.toCharThreeNF : {F : Type u_2} → [inst : Field F] → [CharP F 3] → WeierstrassCurve F → WeierstrassCurve.VariableChange F
-- Mathlib.Algebra.Ring.Subring.Defs
SubringClass.coe_subtype : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : SetLike S R] [hSR : SubringClass S R] (s : S),
  ⇑(SubringClass.subtype s) = Subtype.val
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.mem_toList_iff_get?_eq_some : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [Std.LawfulEqOrd α] {k : α} {v : β},
  t.WF → ((k, v) ∈ Std.DTreeMap.Internal.Impl.Const.toList t ↔ Std.DTreeMap.Internal.Impl.Const.get? t k = some v)
-- Mathlib.Order.Filter.Prod
/-- A technical lemma which is a generalization of `Filter.Eventually.trans_prod`.  -/
Filter.Eventually.eventually_prod_of_eventually_swap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Filter β} {h : Filter γ} [g.NeBot] {p : α → β → Prop}
  {q : β → γ → Prop} {r : α → γ → Prop},
  (∀ᶠ (x : α) in f, ∀ᶠ (y : β) in g, p x y) →
    (∀ᶠ (z : γ) in h, ∀ᶠ (y : β) in g, q y z) →
      (∀ (x : α) (y : β) (z : γ), p x y → q y z → r x z) → ∀ᶠ (xz : α × γ) in f ×ˢ h, r xz.1 xz.2
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
/-- If the coequalizer comparison map for `G` at `(f,g)` is an isomorphism, then `G` preserves the
coequalizer of `(f,g)`.
 -/
CategoryTheory.Limits.of_iso_comparison : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {X Y : C} (f g : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasCoequalizer f g]
  [inst_3 : CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)]
  [i : CategoryTheory.IsIso (CategoryTheory.Limits.coequalizerComparison f g G)],
  CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Rel.mul_zero : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R] {a : FreeAlgebra.Pre R X}, FreeAlgebra.Rel R X (a * 0) 0
-- Mathlib.Analysis.Convex.Cone.Dual
ProperCone.dual_le_dual : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : TopologicalSpace R] [inst_4 : ClosedIciTopology R] [inst_5 : AddCommGroup M] [inst_6 : Module R M]
  [inst_7 : TopologicalSpace M] [inst_8 : AddCommGroup N] [inst_9 : Module R N] [inst_10 : TopologicalSpace N]
  {p : M →ₗ[R] N →ₗ[R] R} [inst_11 : p.IsContPerfPair] {s t : Set M}, t ⊆ s → ProperCone.dual p s ≤ ProperCone.dual p t
-- Mathlib.Order.Interval.Basic
NonemptyInterval.instPreorder : {α : Type u_1} → [inst : Preorder α] → Preorder (NonemptyInterval α)
-- Mathlib.Algebra.Category.Semigrp.Basic
/-- multiplicative equivalences between `Mul`s are the same as (isomorphic to) isomorphisms
in `MagmaCat`  -/
mulEquivIsoMagmaIso : {X Y : Type u} → [inst : Mul X] → [inst_1 : Mul Y] → X ≃* Y ≅ MagmaCat.of X ≅ MagmaCat.of Y
-- Mathlib.Lean.Meta.RefinedDiscrTree.Encode
/-- Auxiliary function for `evalLazyEntry`  -/
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Encode.0.Lean.Meta.RefinedDiscrTree.evalLazyEntryAux : Lean.Meta.RefinedDiscrTree.LazyEntry →
  Bool → Lean.MetaM (Option (List (Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry)))
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.isUnit_nonsing_inv_det : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α),
  IsUnit A.det → IsUnit A⁻¹.det
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
/-- Change of variables for continuous integrands. If `f` is continuous on `[a, b]` and has
continuous right-derivative `f'` in `(a, b)`, and `g` is continuous on `f '' [a, b]` then we can
substitute `u = f x` to get `∫ x in a..b, f' x • (g ∘ f) x = ∫ u in f a..f b, g u`.

If the function `f` is monotone or antitone, see also `integral_deriv_smul_comp_of_deriv_nonneg`
and `integral_deriv_smul_comp_of_deriv_nonpos` dropping all assumptions on `g`.  -/
intervalIntegral.integral_deriv_smul_comp'' : ∀ {a b : ℝ} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f f' : ℝ → ℝ} {g : ℝ → E},
  ContinuousOn f (Set.uIcc a b) →
    (∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Set.Ioi x) x) →
      ContinuousOn f' (Set.uIcc a b) →
        ContinuousOn g (f '' Set.uIcc a b) → ∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (u : ℝ) in f a..f b, g u
-- Mathlib.LinearAlgebra.TensorPower.Symmetric
/-- The canonical map from the `ι`-indexed tensor power to the symmetric tensor power.  -/
SymmetricPower.mk : (R ι : Type u) →
  [inst : CommSemiring R] →
    (M : Type v) →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → (PiTensorProduct R fun x => M) →ₗ[R] SymmetricPower R ι M