mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- Equality holds when `a ≠ 0`. See `inv_mul_cancel_left`.  -/
inv_mul_left_le : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : Preorder G₀] {a b : G₀}, 0 ≤ b → a⁻¹ * (a * b) ≤ b
-- Mathlib.Topology.Instances.NNReal.Lemmas
ContinuousMap.realToNNReal_apply : ⇑ContinuousMap.realToNNReal = Real.toNNReal
-- Mathlib.Topology.Instances.TrivSqZeroExt
TrivSqZeroExt.uniformContinuous_inr : ∀ {R : Type u_3} {M : Type u_4} [inst : UniformSpace R] [inst_1 : UniformSpace M] [inst_2 : Zero R],
  UniformContinuous TrivSqZeroExt.inr
-- Mathlib.Order.Disjoint
/-- **Alias** of `symm_disjoint`. -/
symmetric_disjoint : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α], Std.Symm Disjoint
-- Batteries.Recycling.RBTree.Alter
_private.Batteries.Recycling.RBTree.Alter.0.RBTree.RBMap.alter.adapt.match_3.eq_1 : ∀ {α : Type u_2} {β : Type u_1} (motive : Option (α × β) → Sort u_3) (h_1 : Unit → motive none)
  (h_2 : (k' : α) → (v' : β) → motive (some (k', v'))),
  (match none with
    | none => h_1 ()
    | some (k', v') => h_2 k' v') =
    h_1 ()
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
mvfderiv_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_8} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {x : M}, d% 0 x = 0
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.uniformEquiv_symm_apply : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : UniformSpace X] (val : X),
  Metric.Snowflaking.uniformEquiv.symm val = Metric.Snowflaking.toSnowflaking val
-- Std.Time.Date.Basic
Std.Time.instHSubOffsetOffset_7 : HSub Std.Time.Millisecond.Offset Std.Time.Second.Offset Std.Time.Millisecond.Offset
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.coe_smul : ∀ {R' : Type u'} {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (S : Subalgebra R A) [inst_3 : SMul R' R] [inst_4 : SMul R' A] [inst_5 : IsScalarTower R' R A] (r : R') (x : ↥S),
  ↑(r • x) = r • ↑x
-- Mathlib.Algebra.Group.Submonoid.Membership
AddSubmonoid.eq_bot_of_card_eq : ∀ {M : Type u_1} [inst : AddMonoid M] {S : AddSubmonoid M} [inst_1 : Fintype ↥S], Fintype.card ↥S = 1 → S = ⊥
-- Mathlib.CategoryTheory.EquivalenceRelation
/-- Standard transitive relations on types are internal transitive relations in the category of
types.  -/
TypeCat.TransitiveRelation.ofIsTrans : {X : Type w} →
  {φ : X → X → Prop} → IsTrans X φ → CategoryTheory.TransitiveRelation (TypeCat.p₁OfRel φ) (TypeCat.p₂OfRel φ)
-- Lean.Elab.Term
Lean.Elab.Term.expandDeclId : Lean.Name → List Lean.Name → Lean.Syntax → Lean.Elab.Modifiers → Lean.Elab.TermElabM Lean.Elab.ExpandDeclIdResult
-- Mathlib.Algebra.Group.UniqueProds.Basic
/-- Let `G` be a Type with addition. `TwoUniqueSums G` asserts that any two non-empty
finite subsets of `G`, at least one of which is not a singleton, possesses at least two pairs
of elements satisfying the `UniqueAdd` property.  -/
TwoUniqueSums : (G : Type u_1) → [Add G] → Prop
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
CategoryTheory.OrthogonalReflection.D₂.multispanShape_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (Z : C)
  [inst_1 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁]
  [inst_2 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂]
  [inst_3 : CategoryTheory.Limits.HasPushouts C] (x : CategoryTheory.OrthogonalReflection.D₂ W Z),
  (CategoryTheory.OrthogonalReflection.D₂.multispanShape W Z).fst x = ()
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get!_filterMap_of_getKey?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] [inst_1 : Inhabited γ] {f : α → β → Option γ} {k k' : α},
  t.getKey? k = some k' →
    Std.ExtDTreeMap.Const.get! (Std.ExtDTreeMap.filterMap f t) k = ((Std.ExtDTreeMap.Const.get? t k).bind (f k')).get!
-- Mathlib.Topology.Order.IsLocallyClosed
isLocallyClosed_Iic : ∀ {X : Type u_1} [inst : TopologicalSpace X] {a : X} [inst_1 : Preorder X] [ClosedIicTopology X],
  IsLocallyClosed (Set.Iic a)
-- Init.Data.List.Find
List.findSome?_cons_of_isSome : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {a : α} {l : List α},
  (f a).isSome = true → List.findSome? f (a :: l) = f a
-- Lean.Parser.Basic
Lean.Parser.instDecidableEqRecoveryContext : DecidableEq Lean.Parser.RecoveryContext
-- Mathlib.Tactic.NormNum.Basic
Mathlib.Meta.NormNum.isintCast : ∀ {R : Type u_1} [inst : Ring R] (n m : ℤ), Mathlib.Meta.NormNum.IsInt n m → Mathlib.Meta.NormNum.IsInt (↑n) m
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multifork.ofPiFork_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  {I : CategoryTheory.Limits.MulticospanIndex J C} {c : CategoryTheory.Limits.Fan I.left}
  {d : CategoryTheory.Limits.Fan I.right} {hd : CategoryTheory.Limits.IsLimit d}
  (a : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)),
  (CategoryTheory.Limits.Multifork.ofPiFork a).pt = a.pt
-- Mathlib.RingTheory.Nilpotent.Defs
/-- If `x` is nilpotent, the nilpotency class is the smallest natural number `k` such that
`x ^ k = 0`. If `x` is not nilpotent, the nilpotency class takes the junk value `0`.  -/
nilpotencyClass : {R : Type u_1} → R → [Zero R] → [Pow R ℕ] → ℕ
-- Mathlib.Analysis.InnerProductSpace.Spectrum
/-- Eigenvalues are sorted in decreasing order.  -/
LinearMap.IsSymmetric.eigenvalues_antitone : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E} [inst_3 : FiniteDimensional 𝕜 E] {n : ℕ} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n),
  Antitone (hT.eigenvalues hn)
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_castSucc_Ico_castSucc : ∀ {n : ℕ} (i j : Fin n), Fin.castSucc ⁻¹' Set.Ico i.castSucc j.castSucc = Set.Ico i j
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.getGTD_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] {k fallback : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getGTD k fallback = t₂.getGTD k fallback
-- Mathlib.Algebra.Order.BigOperators.Group.List
List.exists_le_of_sum_le : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddMonoid M] [inst_1 : LinearOrder M] [AddLeftStrictMono M] [AddLeftMono M]
  [AddRightStrictMono M] [AddRightMono M] {l : List ι},
  l ≠ [] → ∀ (f g : ι → M), (List.map f l).sum ≤ (List.map g l).sum → ∃ x ∈ l, f x ≤ g x
-- Mathlib.Order.Antisymmetrization
AntisymmRel.trans : ∀ {α : Type u_1} {a b c : α} {r : α → α → Prop} [IsTrans α r], AntisymmRel r a b → AntisymmRel r b c → AntisymmRel r a c
-- Init.Data.Bool
Bool.beq_not_self : ∀ (x : Bool), (x == !x) = false
-- Aesop.Stats.Basic
Aesop.GoalStats : Type
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem?_map : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [LawfulBEq α]
  {f : α → β → γ} {k : α}, m.WF → (Std.HashMap.Raw.map f m)[k]? = Option.map (f k) m[k]?
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.dist_lt_add_of_nonempty_ball_inter_closedBall : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α} {ε₁ ε₂ : ℝ},
  (Metric.ball x ε₁ ∩ Metric.closedBall y ε₂).Nonempty → dist x y < ε₁ + ε₂
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
_private.Mathlib.MeasureTheory.Measure.Typeclasses.SFinite.0.MeasureTheory.Measure.exists_ae_subset_biUnion_countable_of_isFiniteMeasure : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  {C : Set (Set α)}, (∀ s ∈ C, MeasurableSet s) → ∃ D ⊆ C, D.Countable ∧ ∀ s ∈ C, s ≤ᵐ[μ] ⋃₀ D
-- Mathlib.Algebra.Algebra.Spectrum.Basic
/-- **Alias** of the forward direction of `spectrum.inv₀_mem_inv_iff`. -/
spectrum.of_inv₀_mem_inv : ∀ {R : Type u} {A : Type v} [inst : Semifield R] [inst_1 : Ring A] [inst_2 : Algebra R A] {r : R} {a : Aˣ},
  r⁻¹ ∈ spectrum R ↑a⁻¹ → r ∈ spectrum R ↑a
-- Mathlib.GroupTheory.GroupAction.Defs
FixedPoints.mem_subgroup : ∀ (M : Type u) (α : Type v) [inst : Monoid M] [inst_1 : Group α] [inst_2 : MulDistribMulAction M α] (a : α),
  a ∈ FixedPoints.subgroup M α ↔ ∀ (m : M), m • a = a
-- Mathlib.RepresentationTheory.Basic
/-- Build a `Representation k G M` from a `[Module k[G] M]`.

This version is not always what we want, as it relies on an existing `[Module k M]` instance,
along with a `[IsScalarTower k k[G] M]` instance.

We remedy this below in `ofModule`
(with the tradeoff that the representation is defined
only on a type synonym of the original module.)
 -/
Representation.ofModule' : {k : Type u_1} →
  {G : Type u_2} →
    [inst : CommSemiring k] →
      [inst_1 : Monoid G] →
        (M : Type u_4) →
          [inst_2 : AddCommMonoid M] →
            [inst_3 : Module k M] →
              [inst_4 : Module (MonoidAlgebra k G) M] → [IsScalarTower k (MonoidAlgebra k G) M] → Representation k G M
-- Mathlib.RingTheory.ZariskisMainTheorem
_private.Mathlib.RingTheory.ZariskisMainTheorem.0.Algebra.ZariskisMainProperty.of_adjoin_eq_top : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal S) [inst_3 : p.IsPrime]
  [Algebra.WeaklyQuasiFiniteAt R p] (x : S), R[x] = ⊤ → Algebra.ZariskisMainProperty R p
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.instReprArgSpec : Repr Lean.Doc.ArgSpec✝
-- Mathlib.Algebra.Lie.Subalgebra
/-- A Lie algebra is equivalent to its range under an injective Lie algebra morphism.  -/
LieHom.equivRangeOfInjective : {R : Type u} →
  {L : Type v} →
    [inst : CommRing R] →
      [inst_1 : LieRing L] →
        [inst_2 : LieAlgebra R L] →
          {L₂ : Type w} →
            [inst_3 : LieRing L₂] →
              [inst_4 : LieAlgebra R L₂] → (f : L →ₗ⁅R⁆ L₂) → Function.Injective ⇑f → L ≃ₗ⁅R⁆ ↥f.range
-- Mathlib.Logic.Basic
dcongr_heq : ∀ {α₁ α₂ : Sort u} {β₁ : α₁ → Sort v} {β₂ : α₂ → Sort v} {f₁ : (a : α₁) → β₁ a} {f₂ : (a : α₂) → β₂ a} {a₁ : α₁}
  {a₂ : α₂}, a₁ ≍ a₂ → (∀ (t₁ : α₁) (t₂ : α₂), t₁ ≍ t₂ → β₁ t₁ = β₂ t₂) → (α₁ = α₂ → β₁ ≍ β₂ → f₁ ≍ f₂) → f₁ a₁ ≍ f₂ a₂
-- Std.Data.Iterators.Lemmas.Consumers.Set
_private.Std.Data.Iterators.Lemmas.Consumers.Set.0.Std.Iter.toExtHashSet.eq_1 : ∀ {α β : Type w} [inst : BEq β] [inst_1 : Hashable β] [inst_2 : EquivBEq β] [inst_3 : LawfulHashable β]
  [inst_4 : Std.Iterator α Id β] [inst_5 : Std.IteratorLoop α Id Id] (it : Std.Iter β),
  it.toExtHashSet = it.toIterM.toExtHashSet.run
-- Init.Data.UInt.Lemmas
UInt32.toUInt64_ofNatTruncate_of_le : ∀ {n : ℕ},
  UInt32.size ≤ n →
    (UInt32.ofNatClamp n).toUInt64 = UInt64.ofNatLT (UInt32.size - 1) UInt32.toUInt64_ofNatClamp_of_le._proof_1
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.mapRange.addEquiv_trans : ∀ {ι : Type u} {β : ι → Type v} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [inst : (i : ι) → AddZeroClass (β i)]
  [inst_1 : (i : ι) → AddZeroClass (β₁ i)] [inst_2 : (i : ι) → AddZeroClass (β₂ i)] (f : (i : ι) → β i ≃+ β₁ i)
  (f₂ : (i : ι) → β₁ i ≃+ β₂ i),
  (DFinsupp.mapRange.addEquiv fun i => (f i).trans (f₂ i)) =
    (DFinsupp.mapRange.addEquiv f).trans (DFinsupp.mapRange.addEquiv f₂)
-- Lean.Meta.Basic
Lean.Meta.instMonadLCtxMetaM : Lean.MonadLCtx Lean.MetaM
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.maxKey?_eq_maxKey? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {t : Std.DTreeMap.Internal.Impl α β}, t.Ordered → t.maxKey? = Std.Internal.List.maxKey? t.toListModel
-- Mathlib.Algebra.FreeAlgebra.Cardinality
FreeAlgebra.cardinalMk_eq : ∀ (R : Type u) [inst : CommSemiring R] (X : Type u) [IsEmpty X], Cardinal.mk (FreeAlgebra R X) = Cardinal.mk R
-- Mathlib.Tactic.Linter.FlexibleLinter
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.Stained.name.injEq : ∀ (a a_1 : Lean.Name), (Mathlib.Linter.Flexible.Stained.name✝ a = Mathlib.Linter.Flexible.Stained.name✝ a_1) = (a = a_1)
-- Mathlib.Data.ENNReal.Basic
/-- The set of numbers in `ℝ≥0∞` that are not equal to `∞` is equivalent to `ℝ≥0`.  -/
ENNReal.neTopEquivNNReal : ↑{a | a ≠ ⊤} ≃ NNReal
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- The **first isomorphism theorem for commutative rings**, computable version.  -/
RingHom.quotientKerEquivOfRightInverse : {R : Type u} →
  {S : Type v} →
    [inst : Ring R] →
      [inst_1 : Semiring S] → {f : R →+* S} → {g : S → R} → Function.RightInverse g ⇑f → R ⧸ RingHom.ker f ≃+* S
-- Mathlib.Order.Minimal
MaximalFor.maximal_of_strictMonoOn : ∀ {α : Type u_2} {β : Type u_3} {P : α → Prop} {x : α} [inst : Preorder α] [inst_1 : Preorder β] {g : α → β},
  StrictMonoOn g (Set.ofPred P) → MaximalFor P g x → Maximal P x
-- Mathlib.Data.Set.Prod
Set.uncurry_preimage_prod_pi : ∀ {ι : Type u_1} {κ : Type u_4} {α : Type u_5} (s : Set ι) (t : Set κ) (u : ι × κ → Set α),
  Function.uncurry ⁻¹' (s ×ˢ t).pi u = s.pi fun i => t.pi fun j => u (i, j)
-- Lean.Meta.Tactic.SplitIf
/-- Default `Simp.Context` for `simpIf` methods. It contains all congruence theorems, but
without rewriting rules. We use simprocs to reduce the if-then-else terms  -/
_private.Lean.Meta.Tactic.SplitIf.0.Lean.Meta.SplitIf.getSimpContext' : Lean.MetaM Lean.Meta.Simp.Context
-- Mathlib.CategoryTheory.Functor.TwoSquare
/-- Notation for the horizontal identity 2-square.  -/
CategoryTheory.TwoSquare.«term𝟙ₕ» : Lean.ParserDescr
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.le_normalizer_of_normal_subgroupOf : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} [hK : (H.subgroupOf K).Normal], H ≤ K → K ≤ Subgroup.normalizer ↑H
-- Mathlib.Topology.Sheaves.Stalks
/-- A variant of `germ_res` with `op V ⟶ op U`
so that the LHS is more general and simp fires more easier.  -/
TopCat.Presheaf.germ_res' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  (F : TopCat.Presheaf C X) {U V : TopologicalSpace.Opens ↑X} (i : Opposite.op V ⟶ Opposite.op U) (x : ↑X) (hx : x ∈ U),
  CategoryTheory.CategoryStruct.comp (F.map i) (F.germ U x hx) = F.germ V x ⋯
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sinOrderIso_apply : ∀ (x : ↑(Set.Icc (-(Real.pi / 2)) (Real.pi / 2))), Real.sinOrderIso x = ⟨Real.sin ↑x, ⋯⟩
-- Mathlib.ModelTheory.Substructures
/-- A dependent version of `Substructure.closure_induction`.  -/
FirstOrder.Language.Substructure.closure_induction' : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] (s : Set M)
  {p : (x : M) → x ∈ (FirstOrder.Language.Substructure.closure L).toFun s → Prop},
  (∀ (x : M) (h : x ∈ s), p x ⋯) →
    (∀ {n : ℕ} (f : L.Functions n),
        FirstOrder.Language.ClosedUnder f
          {x | ∃ (hx : x ∈ (FirstOrder.Language.Substructure.closure L).toFun s), p x hx}) →
      ∀ {x : M} (hx : x ∈ (FirstOrder.Language.Substructure.closure L).toFun s), p x hx
-- Mathlib.Algebra.Lie.Sl2
/-- The eigenvalue of a primitive vector must be a natural number if the representation is
finite-dimensional.  -/
IsSl2Triple.HasPrimitiveVectorWith.exists_nat : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [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] [LieModule R L M] {h e f : L} {m : M}
  {μ : R} {t : IsSl2Triple h e f},
  t.HasPrimitiveVectorWith m μ → ∀ [IsNoetherian R M] [Module.IsTorsionFree R M] [IsDomain R] [CharZero R], ∃ n, μ = ↑n
-- Mathlib.FieldTheory.Isaacs
Field.nonempty_algEquiv_of_range_minpoly_eq : ∀ {F : Type u_1} {E : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
  [inst_3 : Algebra F E] [inst_4 : Algebra F K] [alg : Algebra.IsAlgebraic F E],
  Set.range (minpoly F) = Set.range (minpoly F) → Nonempty (E ≃ₐ[F] K)
-- Mathlib.Order.Filter.Ker
/-- `Filter.principal` forms a Galois coinsertion with `Filter.ker`.  -/
Filter.giPrincipalKer : {α : Type u_2} → GaloisCoinsertion Filter.principal Filter.ker
-- Mathlib.RingTheory.PowerSeries.Basic
/-- The constant coefficient of a formal power series.  -/
PowerSeries.constantCoeff : {R : Type u_1} → [inst : Semiring R] → PowerSeries R →+* R
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.IsImage.mapsTo : ∀ {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β},
  e.IsImage s t → Set.MapsTo (↑e) (e.source ∩ s) (e.target ∩ t)
-- Lean.Setup
Lean.ImportArtifacts.ofArrays : Array (Array System.FilePath) → Lean.ImportArtifacts
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.mk.sizeOf_spec : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂] [inst_7 : SizeOf R]
  [inst_8 : SizeOf ι] [inst_9 : (a : ι) → SizeOf (M₁ a)] [inst_10 : SizeOf M₂]
  (toMultilinearMap : MultilinearMap R M₁ M₂) (cont : Continuous toMultilinearMap.toFun),
  sizeOf { toMultilinearMap := toMultilinearMap, cont := cont } = 1 + sizeOf toMultilinearMap + sizeOf cont
-- Mathlib.RingTheory.Extension.Basic
/-- The action of `P` on `P.Cotangent` for an extension `P → S`.  -/
Algebra.Extension.Cotangent.val_smul' : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  (r : P.Ring) (x : P.Cotangent), (r • x).val = r • x.val
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
/-- Auxiliary lemma for `condExp_indicator`.  -/
MeasureTheory.condExp_indicator_aux : ∀ {α : Type u_1} {E : Type u_2} {m m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [CompleteSpace E] {μ : MeasureTheory.Measure α} {f : α → E} {s : Set α},
  MeasurableSet s → f =ᵐ[μ.restrict sᶜ] 0 → μ[s.indicator f | m] =ᵐ[μ] s.indicator μ[f | m]
-- Mathlib.Analysis.Calculus.LHopital
deriv.lhopital_zero_right_on_Ioo : ∀ {a b : ℝ} {l : Filter ℝ} {f g : ℝ → ℝ},
  a < b →
    DifferentiableOn ℝ f (Set.Ioo a b) →
      (∀ x ∈ Set.Ioo a b, deriv g x ≠ 0) →
        Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds 0) →
          Filter.Tendsto g (nhdsWithin a (Set.Ioi a)) (nhds 0) →
            Filter.Tendsto (fun x => deriv f x / deriv g x) (nhdsWithin a (Set.Ioi a)) l →
              Filter.Tendsto (fun x => f x / g x) (nhdsWithin a (Set.Ioi a)) l
-- Mathlib.Topology.MetricSpace.PiNat
Metric.PiNatEmbed.isUniformEmbedding_embed : ∀ {ι : Type u_2} {X : Type u_3} {Y : ι → Type u_4} {f : (i : ι) → X → Y i} [inst : Encodable ι]
  [inst_1 : (i : ι) → EMetricSpace (Y i)],
  (Pairwise fun x y => ∃ i, f i x ≠ f i y) → IsUniformEmbedding (Metric.PiNatEmbed.embed X Y f)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.addZ_of_Z_eq_zero_left : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} [NoZeroDivisors R] {P Q : Fin 3 → R},
  W'.Equation P → P 2 = 0 → W'.addZ P Q = P 1 ^ 2 * Q 2 * Q 2
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
EReal.measurable_of_measurable_real : ∀ {α : Type u_1} {mα : MeasurableSpace α} {f : EReal → α}, (Measurable fun p => f ↑p) → Measurable f
-- Mathlib.Analysis.MeanInequalities
Real.summable_Lr_of_Lp_Lq_of_nonneg : ∀ {ι : Type u} {f g : ι → ℝ} {p q r : ℝ},
  p.HolderTriple q r →
    (∀ (i : ι), 0 ≤ f i) →
      (∀ (i : ι), 0 ≤ g i) →
        (Summable fun i => f i ^ p) → (Summable fun i => g i ^ q) → Summable fun i => (f i * g i) ^ r
-- Mathlib.Analysis.Normed.Group.Continuity
tendsto_norm_neg_add_self : ∀ {E : Type u_4} [inst : SeminormedAddGroup E] (x : E), Filter.Tendsto (fun a => ‖-a + x‖) (nhds x) (nhds 0)
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.IsMultiplicative.map_one : ∀ {R : Type u_1} [inst : MonoidWithZero R] {f : ArithmeticFunction R}, f.IsMultiplicative → f 1 = 1
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.eq_d₂₁_comp_inv_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) {Z : ModuleCat k}
  (h : ModuleCat.of k ((Fin 1 → G) →₀ ↑A) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupHomology.chainsIso₂ A).inv
      (CategoryTheory.CategoryStruct.comp
        (ChainComplex.of.d (fun n => ModuleCat.of k ((Fin n → G) →₀ ↑A))
          (fun n => groupHomology.inhomogeneousChains.d A n) 2 1)
        h) =
    CategoryTheory.CategoryStruct.comp (groupHomology.d₂₁ A)
      (CategoryTheory.CategoryStruct.comp (groupHomology.chainsIso₁ A).inv h)
-- Mathlib.CategoryTheory.Monoidal.CommMon_
/-- Implementation of `CommMon.equivLaxBraidedFunctorPUnit`.  -/
CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        CategoryTheory.CommMon C → CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u + 1}) C
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.instInhabited : (M : Type u_1) → [inst : TopologicalSpace M] → [inst_1 : Mul M] → Inhabited (M ≃ₜ* M)
-- Mathlib.CategoryTheory.Sites.LeftExact
CategoryTheory.GrothendieckTopology.coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation_π_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{t, w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  {X : C} {K : Type s} [inst_3 : CategoryTheory.SmallCategory K]
  {F : CategoryTheory.Functor K (CategoryTheory.Functor Cᵒᵖ D)} {W : J.Cover X} (i : W.Arrow)
  (E :
    CategoryTheory.Limits.Cone
      (F.comp ((J.diagramFunctor D X).comp ((CategoryTheory.evaluation (J.Cover X)ᵒᵖ D).obj (Opposite.op W)))))
  (k : K),
  (CategoryTheory.GrothendieckTopology.coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation i E).π.app k =
    CategoryTheory.CategoryStruct.comp (E.π.app k) (CategoryTheory.Limits.Multiequalizer.ι (W.index (F.obj k)) i)
-- Mathlib.Topology.Algebra.ConstMulAction
/-- **Alias** of the reverse direction of `smul_mem_nhds_smul_iff₀`.

---

Scalar multiplication by a nonzero scalar preserves neighborhoods.  -/
smul_mem_nhds_smul₀ : ∀ {α : Type u_2} {G₀ : Type u_6} [inst : GroupWithZero G₀] [inst_1 : MulAction G₀ α] [inst_2 : TopologicalSpace α]
  [ContinuousConstSMul G₀ α] {c : G₀} {s : Set α} {x : α}, c ≠ 0 → s ∈ nhds x → c • s ∈ nhds (c • x)
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.toWeakDualBCNN_apply : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
  (μ : MeasureTheory.FiniteMeasure Ω) (f : BoundedContinuousFunction Ω NNReal),
  μ.toWeakDualBCNN f = (∫⁻ (x : Ω), ↑(f x) ∂↑μ).toNNReal
-- Mathlib.Data.ENNReal.Inv
ENNReal.zero_div : ∀ {a : ENNReal}, 0 / a = 0
-- Mathlib.Data.Num.Lemmas
Num.cmp_eq : ∀ (m n : Num), m.cmp n = Ordering.eq ↔ m = n
-- Mathlib.Topology.Algebra.Monoid
/-- If addition is continuous in `α`, then it also is in `αᵃᵒᵖ`.  -/
AddOpposite.instContinuousAdd : ∀ {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : Add α] [ContinuousAdd α], ContinuousAdd αᵃᵒᵖ
-- Std.Data.TreeSet.Basic
/-- Tries to retrieve the smallest element of the tree set, returning `fallback` if the tree set is empty.
 -/
Std.TreeSet.minD : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet α cmp → α → α
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.FullyFaithful.instSubsingleton : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D}, Subsingleton F.FullyFaithful
-- Lean.DocString.Extension
Lean.VersoModuleDocs.mk : Lean.PersistentArray Lean.VersoModuleDocs.Snippet → Lean.VersoModuleDocs
-- Init.Data.UInt.Lemmas
UInt16.toBitVec_pow : ∀ (a : UInt16) (n : ℕ), (a ^ n).toBitVec = a.toBitVec ^ n