mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKeyD_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α}
  {k fallback : α}, k ∈ m → (m.insertManyIfNewUnit l).getKeyD k fallback = m.getKeyD k fallback
-- Mathlib.MeasureTheory.Function.L2Space
_private.Mathlib.MeasureTheory.Function.L2Space.0.MeasureTheory.L2.smul_left' : ∀ {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [inst : RCLike 𝕜] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (f g : ↥(MeasureTheory.Lp E 2 μ)) (r : 𝕜),
  inner 𝕜 (r • f) g = (starRingEnd 𝕜) r * inner 𝕜 f g
-- Lean.Meta.CongrTheorems
Lean.Meta.mkHCongr : Lean.Expr → Lean.MetaM Lean.Meta.CongrTheorem
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- The oriented angle between two vectors is zero or `π` if and only if the first vector is zero
or the second is a multiple of the first.  -/
Orientation.oangle_eq_zero_or_eq_pi_iff_right_eq_smul : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = 0 ∨ o.oangle x y = ↑Real.pi ↔ x = 0 ∨ ∃ r, y = r • x
-- Mathlib.Condensed.Discrete.LocallyConstant
/-- This is an auxiliary definition, the details do not matter. What's important is that this map exists
so that the lemma `incl_comap` works.
 -/
CompHausLike.LocallyConstant.componentHom : {P : TopCat → Prop} →
  [inst : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)] →
    {S : CompHausLike P} →
      {Y : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w))} →
        [inst_1 : CompHausLike.HasProp P PUnit.{u + 1}] →
          (f : LocallyConstant (↑S.toTop) (Y.obj (Opposite.op (CompHausLike.of P PUnit.{u + 1})))) →
            {T : CompHausLike P} →
              (g : T ⟶ S) →
                (a : Function.Fiber ⇑(LocallyConstant.comap (TopCat.Hom.hom g.hom) f)) →
                  CompHausLike.LocallyConstant.fiber (LocallyConstant.comap (TopCat.Hom.hom g.hom) f) a ⟶
                    CompHausLike.LocallyConstant.fiber f
                      (Function.Fiber.mk (⇑f)
                        ((CategoryTheory.ConcreteCategory.hom g)
                          (Function.Fiber.preimage (⇑(LocallyConstant.comap (TopCat.Hom.hom g.hom) f)) a)))
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Methods.mk.injEq : ∀ (pre post : Lean.Meta.Simp.Simproc) (dpre dpost : Lean.Meta.Simp.DSimproc)
  (discharge? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr)) (wellBehavedDischarge : Bool)
  (pre_1 post_1 : Lean.Meta.Simp.Simproc) (dpre_1 dpost_1 : Lean.Meta.Simp.DSimproc)
  (discharge?_1 : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr)) (wellBehavedDischarge_1 : Bool),
  ({ pre := pre, post := post, dpre := dpre, dpost := dpost, discharge? := discharge?,
        wellBehavedDischarge := wellBehavedDischarge } =
      { pre := pre_1, post := post_1, dpre := dpre_1, dpost := dpost_1, discharge? := discharge?_1,
        wellBehavedDischarge := wellBehavedDischarge_1 }) =
    (pre = pre_1 ∧
      post = post_1 ∧
        dpre = dpre_1 ∧ dpost = dpost_1 ∧ discharge? = discharge?_1 ∧ wellBehavedDischarge = wellBehavedDischarge_1)
-- Mathlib.Algebra.FreeAbelianGroup.Finsupp
Finsupp.toFreeAbelianGroup_single : ∀ {X : Type u_1} (x : X) (n : ℤ), (Finsupp.toFreeAbelianGroup fun₀ | x => n) = n • FreeAbelianGroup.of x
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.counitIso_inv_app_hom_hom : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : CategoryTheory.CommMon C),
  ((CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.counitIso C).inv.app X).hom.hom =
    CategoryTheory.CategoryStruct.id X.X
-- Mathlib.Algebra.Lie.SkewAdjoint
Matrix.lie_transpose : ∀ {R : Type u} {n : Type w} [inst : CommRing R] [inst_1 : Fintype n] (A B : Matrix n n R),
  ⁅A, B⁆.transpose = ⁅B.transpose, A.transpose⁆
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Path.Homotopy.reflTransSymmAux.eq_1 : ∀ (x : ↑unitInterval × ↑unitInterval),
  Path.Homotopy.reflTransSymmAux x = if ↑x.2 ≤ 1 / 2 then ↑x.1 * 2 * ↑x.2 else ↑x.1 * (2 - 2 * ↑x.2)
-- Mathlib.Order.Types.Defs
/-- **Alias** of `OrderType.type_congr`. -/
OrderIso.type_congr : ∀ {α β : Type u} [inst : LinearOrder α] [inst_1 : LinearOrder β] (h : α ≃o β), OrderType.type α = OrderType.type β
-- Mathlib.Topology.Order.LeftRight
continuousWithinAt_inter_Iio_iff_Iic : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : PartialOrder α] [inst_2 : TopologicalSpace β]
  {a : α} {f : α → β} {s : Set α}, ContinuousWithinAt f (s ∩ Set.Iio a) a ↔ ContinuousWithinAt f (s ∩ Set.Iic a) a
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.setIntegral_congr_fun : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F} {f g : X → E}
  {s : Set X} [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G},
  Set.EqOn f g s → ∫ᵛ (x : X) in s, f x ∂[B; μ] = ∫ᵛ (x : X) in s, g x ∂[B; μ]
-- Mathlib.Algebra.Order.Ring.Abs
_private.Mathlib.Algebra.Order.Ring.Abs.0.geomSum : {α : Type u_1} → [CommRing α] → α → α → ℕ → α
-- Mathlib.AlgebraicGeometry.StructureSheaf
_private.Mathlib.AlgebraicGeometry.StructureSheaf.0.AlgebraicGeometry.StructureSheaf.toStalkₗ'_stalkToFiberRingHom : ∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toStalkₗ'✝ R M x)
      (AlgebraicGeometry.StructureSheaf.stalkToLocalizationₗ✝ R M x) =
    ModuleCat.ofHom (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M)
-- Mathlib.Topology.Continuous
nonempty_preimage_closure_image : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Continuous f → ∀ (t : Set X), t.Nonempty → (f ⁻¹' closure (f '' t)).Nonempty
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.top_meet : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P : l}, Lean.Order.meet Lean.Order.top P = P
-- Aesop.RuleSet
Aesop.LocalRuleSet.mk.inj : ∀ {toBaseRuleSet : Aesop.BaseRuleSet} {simpTheoremsArray : Array (Lean.Name × Lean.Meta.SimpTheorems)}
  {simpTheoremsArrayNonempty : 0 < simpTheoremsArray.size} {simprocsArray : Array (Lean.Name × Lean.Meta.Simprocs)}
  {simprocsArrayNonempty : 0 < simprocsArray.size} {localNormSimpRules : Array Aesop.LocalNormSimpRule}
  {toBaseRuleSet_1 : Aesop.BaseRuleSet} {simpTheoremsArray_1 : Array (Lean.Name × Lean.Meta.SimpTheorems)}
  {simpTheoremsArrayNonempty_1 : 0 < simpTheoremsArray_1.size}
  {simprocsArray_1 : Array (Lean.Name × Lean.Meta.Simprocs)} {simprocsArrayNonempty_1 : 0 < simprocsArray_1.size}
  {localNormSimpRules_1 : Array Aesop.LocalNormSimpRule},
  { toBaseRuleSet := toBaseRuleSet, simpTheoremsArray := simpTheoremsArray,
        simpTheoremsArrayNonempty := simpTheoremsArrayNonempty, simprocsArray := simprocsArray,
        simprocsArrayNonempty := simprocsArrayNonempty, localNormSimpRules := localNormSimpRules } =
      { toBaseRuleSet := toBaseRuleSet_1, simpTheoremsArray := simpTheoremsArray_1,
        simpTheoremsArrayNonempty := simpTheoremsArrayNonempty_1, simprocsArray := simprocsArray_1,
        simprocsArrayNonempty := simprocsArrayNonempty_1, localNormSimpRules := localNormSimpRules_1 } →
    toBaseRuleSet = toBaseRuleSet_1 ∧
      simpTheoremsArray = simpTheoremsArray_1 ∧
        simprocsArray = simprocsArray_1 ∧ localNormSimpRules = localNormSimpRules_1
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Feature.builderOption : Aesop.Frontend.BuilderOption → Aesop.Frontend.Feature
-- Batteries.Tactic.Init
/-- `by_contra_core` is the component of `by_contra` that turns the goal into the form `p → False`.
`by_contra h` is defined as `by_contra_core` followed by `rintro h`.
* If the goal is a negation `¬q`, the goal becomes `q → False`.
* If the goal has a `Decidable` instance, it uses `Decidable.byContradiction` instead of
  `Classical.byContradiction`.
 -/
Batteries.Tactic.tacticBy_contra_core : Lean.ParserDescr
-- Mathlib.SetTheory.Cardinal.Finite
/-- **Alias** of the reverse direction of `Set.natCard_pos`. -/
Set.Nonempty.natCard_pos : ∀ {α : Type u_1} {s : Set α}, s.Finite → s.Nonempty → 0 < Nat.card ↑s
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.neg_def : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : Nonempty ι]
  [inst_5 : (i : ι) → AddGroup (G i)] [inst_6 : ∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] (i : ι)
  (x : G i), -⟦⟨i, x⟩⟧ = ⟦⟨i, -x⟩⟧
-- Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso
/-- The forwards and backwards edge of `coherentIso` compose to the identity.  -/
SSet.coherentIso.homInvId : SSet.coherentIso.hom.CompStruct SSet.coherentIso.inv (SSet.Edge.id SSet.coherentIso.x₀)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.instToStringLVal.levelsToString : List Lean.Level → String
-- Mathlib.Analysis.Complex.Periodic
Function.Periodic.cuspFunction_eq_of_nonzero : ∀ (h : ℝ) (f : ℂ → ℂ) {q : ℂ}, q ≠ 0 → Function.Periodic.cuspFunction h f q = f (Function.Periodic.invQParam h q)
-- Mathlib.Algebra.Category.ModuleCat.Stalk
PresheafOfModules.instModuleCarrierStalkRingCatCarrierAbPresheafOpensCarrier : {X : TopCat} →
  {R : TopCat.Presheaf RingCat X} →
    (M : PresheafOfModules R) → (x : ↑X) → Module ↑(R.stalk x) ↑(TopCat.Presheaf.stalk M.presheaf x)
-- Mathlib.Analysis.Distribution.Support
Distribution.IsVanishingOn.mono : ∀ {α : Type u_2} {β : Type u_3} {F : Type u_6} {V : Type u_10} [inst : FunLike F α β] [inst_1 : TopologicalSpace α]
  [inst_2 : Zero β] {f : F → V} [inst_3 : Zero V] ⦃s₁ s₂ : Set α⦄,
  s₂ ⊆ s₁ → Distribution.IsVanishingOn f s₁ → Distribution.IsVanishingOn f s₂
-- Mathlib.Topology.MetricSpace.Dilation
/-- **Alias** of `Dilation.mapsTo_closedEBall`.

---

A dilation maps closed balls to closed balls and scales the radius by `ratio f`.  -/
Dilation.mapsTo_emetric_closedBall : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : FunLike F α β] [inst_3 : DilationClass F α β] (f : F) (x : α) (r' : ENNReal),
  Set.MapsTo (⇑f) (Metric.closedEBall x r') (Metric.closedEBall (f x) (↑(Dilation.ratio f) * r'))
-- Mathlib.Order.Filter.AtTopBot.Prod
/-- **Alias** of `Filter.tendsto_finsetProd_atTop`. -/
Filter.tendsto_finset_prod_atTop : ∀ {ι : Type u_1} {ι' : Type u_2}, Filter.Tendsto (fun p => p.1 ×ˢ p.2) Filter.atTop Filter.atTop
-- Init.Data.Dyadic.Basic
Dyadic.instIsLinearOrder : Std.IsLinearOrder Dyadic
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.PreservesRightKanExtension.preserves : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} {inst : CategoryTheory.Category.{v_1, u_1} A}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} B} {inst_2 : CategoryTheory.Category.{v_3, u_3} C}
  {inst_3 : CategoryTheory.Category.{v_4, u_4} D} {G : CategoryTheory.Functor B D} {F : CategoryTheory.Functor A B}
  {L : CategoryTheory.Functor A C} [self : G.PreservesRightKanExtension F L] (F' : CategoryTheory.Functor C B)
  (α : L.comp F' ⟶ F) [F'.IsRightKanExtension α],
  (F'.comp G).IsRightKanExtension
    (CategoryTheory.CategoryStruct.comp (L.associator F' G).inv (CategoryTheory.Functor.whiskerRight α G))
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurableSet_eq_of_countable_range : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : PartialOrder ι] {τ : Ω → WithTop ι}
  {f : MeasureTheory.Filtration ι m},
  MeasureTheory.IsStoppingTime f τ → (Set.range τ).Countable → ∀ (i : ι), MeasurableSet {ω | τ ω = ↑i}
-- Mathlib.CategoryTheory.Comma.Basic
/-- If `F` is an equivalence, then so is `post L R F`.  -/
CategoryTheory.Comma.isEquivalence_post : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T)
  (F : CategoryTheory.Functor T C) [F.IsEquivalence], (CategoryTheory.Comma.post L R F).IsEquivalence
-- Mathlib.LinearAlgebra.RootSystem.Defs
/-- Push forward a root pairing along linear equivalences, also reindexing the (co)roots.  -/
RootPairing.map : {ι : 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} →
                    {ι₂ : Type u_5} →
                      {M₂ : Type u_6} →
                        {N₂ : Type u_7} →
                          [inst_5 : AddCommGroup M₂] →
                            [inst_6 : Module R M₂] →
                              [inst_7 : AddCommGroup N₂] →
                                [inst_8 : Module R N₂] → ι ≃ ι₂ → (M ≃ₗ[R] M₂) → (N ≃ₗ[R] N₂) → RootPairing ι₂ R M₂ N₂
-- Std.Http.Data.Version
/-- Converts `String` to the corresponding `Version`.
 -/
Std.Http.Version.ofString? : String → Option Std.Http.Version
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
/-- In the presence of zero morphisms, coprojections into a coproduct are (split) monomorphisms.  -/
CategoryTheory.Limits.isSplitMono_sigma_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {β : Type u'} [CategoryTheory.Limits.HasZeroMorphisms C]
  (f : β → C) [inst_2 : CategoryTheory.Limits.HasColimit (CategoryTheory.Discrete.functor f)] (b : β),
  CategoryTheory.IsSplitMono (CategoryTheory.Limits.Sigma.ι f b)
-- Mathlib.Data.ENNReal.Basic
ENNReal.natCast_ne_top : ∀ (n : ℕ), ↑n ≠ ⊤
-- Lean.Compiler.IR.Basic
Lean.IR.LitVal : Type
-- Mathlib.Order.Filter.Basic
Filter.join_principal_eq_sSup : ∀ {α : Type u} {s : Set (Filter α)}, (Filter.principal s).join = sSup s
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.unitOfList_cons : ∀ {α : Type u} {cmp : α → α → Ordering} {hd : α} {tl : List α},
  Std.DTreeMap.Const.unitOfList (hd :: tl) cmp = Std.DTreeMap.Const.insertManyIfNewUnit (∅.insertIfNew hd ()) tl
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKeyD_eq_of_contains : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α],
  m.WF → ∀ {k fallback : α}, m.contains k = true → m.getKeyD k fallback = k
-- Mathlib.Data.List.Sort
List.sublist_of_subperm_of_sortedGE : ∀ {α : Type u_1} [inst : PartialOrder α] {l₁ l₂ : List α}, l₁.Subperm l₂ → l₁.SortedGE → l₂.SortedGE → l₁.Sublist l₂
-- Mathlib.Order.UpperLower.Basic
/-- **Alias** of the reverse direction of `isUpperSet_preimage_toDual_iff`. -/
IsLowerSet.ofDual : ∀ {α : Type u_1} [inst : LE α] {s : Set αᵒᵈ}, IsLowerSet s → IsUpperSet (⇑OrderDual.toDual ⁻¹' s)
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.symm_trans_apply : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Mul P] (e₁ : M ≃* N)
  (e₂ : N ≃* P) (p : P), (e₁.trans e₂).symm p = e₁.symm (e₂.symm p)
-- Mathlib.Combinatorics.Enumerative.Schroder
Nat.two_mul_smallSchroder_succ : ∀ {n : ℕ}, n ≠ 0 → 2 * (n + 1).smallSchroder = n.largeSchroder
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
/-- The natural transformation `𝟭 C ⟶ t.truncGE n` when `t` is a t-structure
on a category `C` and `n : ℤ`.  -/
CategoryTheory.Triangulated.TStructure.truncGEπ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              (t : CategoryTheory.Triangulated.TStructure C) → (n : ℤ) → CategoryTheory.Functor.id C ⟶ t.truncGE n
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.Hom.inv_hom_id_toNatTrans : ∀ {X Y : CategoryTheory.Cat} {F G : X ⟶ Y} (e : F ≅ G),
  CategoryTheory.CategoryStruct.comp e.inv.toNatTrans e.hom.toNatTrans = CategoryTheory.CategoryStruct.id G.toFunctor
-- Mathlib.GroupTheory.PGroup
IsPGroup.to_inf_right : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] {H K : Subgroup G}, IsPGroup p ↥K → IsPGroup p ↥(H ⊓ K)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mod
/-- The morphism `(m, x) ↦ (m • x, x)` is an isomorphism if and only if the induced
action is pointwise simply transitive.  -/
CategoryTheory.ModObj.isIso_leftSMul_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.MonObj M] {X : C} [inst_3 : CategoryTheory.ModObj M X],
  CategoryTheory.IsIso (CategoryTheory.ModObj.leftSMul M X) ↔ ∀ (Z : C) (x y : Z ⟶ X), ∃! m, m • x = y
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Functor.IsRightAdjoint.exists_leftAdjoint : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {right : CategoryTheory.Functor D C} [self : right.IsRightAdjoint], ∃ left, Nonempty (left ⊣ right)
-- Mathlib.RingTheory.Etale.Locus
Algebra.exists_etale_of_isEtaleAt : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Algebra.FinitePresentation R A] (P : Ideal A) [inst_4 : P.IsPrime] [Algebra.IsEtaleAt R P],
  ∃ f ∉ P, Algebra.Etale R (Localization.Away f)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.dblX_eq' : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} {P : Fin 3 → R},
  W'.Equation P →
    W'.dblX P * P 2 =
      ((MvPolynomial.eval P) W'.polynomialX ^ 2 -
              W'.a₁ * (MvPolynomial.eval P) W'.polynomialX * P 2 * (P 1 - W'.negY P) -
            W'.a₂ * P 2 ^ 2 * (P 1 - W'.negY P) ^ 2 -
          2 * P 0 * P 2 * (P 1 - W'.negY P) ^ 2) *
        (P 1 - W'.negY P)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.GrpObj.div_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G H X : C} [inst_2 : CategoryTheory.GrpObj G] [inst_3 : CategoryTheory.GrpObj H] (f g : X ⟶ G) (h : G ⟶ H)
  [CategoryTheory.IsMonHom h],
  CategoryTheory.CategoryStruct.comp (f / g) h =
    CategoryTheory.CategoryStruct.comp f h / CategoryTheory.CategoryStruct.comp g h
-- Mathlib.InformationTheory.Hamming
Hamming.dist_eq_hammingDist : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)] (x y : Hamming β),
  dist x y = ↑(hammingDist (Hamming.ofHamming x) (Hamming.ofHamming y))
-- Mathlib.Algebra.Category.Ring.Adjunctions
CommRingCat.monoidAlgebra_map : ∀ (R : CommRingCat) {X Y : CommMonCat} (f : X ⟶ Y),
  R.monoidAlgebra.map f =
    CategoryTheory.Under.homMk (CommRingCat.ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom f))) ⋯
-- Mathlib.CategoryTheory.Sites.Whiskering
/-- If `F : A ⥤ B` is fully faithful, then `sheafCompose J F ⋙ sheafToPresheaf J B` is fully
faithful.  -/
CategoryTheory.fullyFaithfulSheafComposeCompSheafToPresheaf : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
        {B : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} B] →
            (J : CategoryTheory.GrothendieckTopology C) →
              {F : CategoryTheory.Functor A B} →
                [inst_3 : J.HasSheafCompose F] →
                  F.FullyFaithful →
                    ((CategoryTheory.sheafCompose J F).comp (CategoryTheory.sheafToPresheaf J B)).FullyFaithful
-- Aesop.Check
Aesop.Check : Type
-- Lean.ScopedEnvExtension
Lean.pushScope : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → [MonadLiftT (ST IO.RealWorld) m] → m Unit
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get_union_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} (not_mem : k ∉ m₂) {h' : k ∈ m₁.union m₂},
  Std.ExtDHashMap.Const.get (m₁.union m₂) k h' = Std.ExtDHashMap.Const.get m₁ k ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.map_inr_inv_coprodComparison_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{w, u₂} D]
  (F : CategoryTheory.Functor C D) {A B : C} [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct A B]
  [inst_3 : CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)]
  [inst_4 : CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison F A B)] {Z : D} (h : F.obj A ⨿ F.obj B ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.coprod.inr)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.coprodComparison F A B)) h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr h
-- Init.Data.List.Nat.Basic
/-- The length of the List returned by `List.leftpad n a l` is equal
to the larger of `n` and `l.length`  -/
List.length_leftpad : ∀ {α : Type u_1} {n : ℕ} {a : α} {l : List α}, (List.leftpad n a l).length = max n l.length
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
AlternatingMap.measure_parallelepiped : ∀ {G : Type u_3} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] [inst_2 : MeasurableSpace G]
  [inst_3 : BorelSpace G] [inst_4 : FiniteDimensional ℝ G] {n : ℕ} [_i : Fact (Module.finrank ℝ G = n)]
  (ω : G [⋀^Fin n]→ₗ[ℝ] ℝ) (v : Fin n → G), ω.measure (parallelepiped v) = ENNReal.ofReal |ω v|
-- Init.Omega.Coeffs
/-- Shim for `IntList.add`.  -/
Lean.Omega.Coeffs.add : Lean.Omega.Coeffs → Lean.Omega.Coeffs → Lean.Omega.Coeffs
-- Mathlib.Algebra.MonoidAlgebra.Module
/-- Interpret `Finsupp.restrictSupportEquiv` as a linear equivalence between
`supported M R s` and `s →₀ M`.  -/
MonoidAlgebra.supportedEquivFinsupp : {R : Type u_1} →
  {S : Type u_2} →
    {M : Type u_3} →
      [inst : Semiring R] →
        [inst_1 : Semiring S] → [inst_2 : Module R S] → (s : Set M) → ↥(MonoidAlgebra.supported R S s) ≃ₗ[R] ↑s →₀ S
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- Fundamental theorem of calculus: if `f : ℝ → E` is integrable on `a..b` and `f x` has a finite
limit `c` almost surely as `x` tends to `a` from the right or from the left, then the right
(resp., left) derivative of `u ↦ ∫ x in u..b, f x` at `a` equals `-c`.  -/
intervalIntegral.derivWithin_integral_of_tendsto_ae_left : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {c : E}
  {a b : ℝ},
  IntervalIntegrable f MeasureTheory.volume a b →
    ∀ {s t : Set ℝ} [intervalIntegral.FTCFilter a (nhdsWithin a s) (nhdsWithin a t)],
      StronglyMeasurableAtFilter f (nhdsWithin a t) MeasureTheory.volume →
        Filter.Tendsto f (nhdsWithin a t ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds c) →
          autoParam (UniqueDiffWithinAt ℝ s a) intervalIntegral.derivWithin_integral_of_tendsto_ae_left._auto_1 →
            derivWithin (fun u => ∫ (x : ℝ) in u..b, f x) s a = -c
-- Std.Http.Test.Helpers
/-- Minimal GET request. `extra` is appended as raw header lines (each ending with `\x0d\n`)
before the blank line.
 -/
Std.Http.Internal.Test.mkGet : optParam String "/" → optParam String "" → String
-- Init.Data.Option.Basic
Option.isSome_some : ∀ {α : Type u_1} {a : α}, (some a).isSome = true