mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Basic
div_mul_div_cancel : ∀ {G : Type u_3} [inst : Group G] (a b c : G), a / b * (b / c) = a / c
-- Mathlib.Algebra.GroupWithZero.Units.Basic
Ring.inverse_eq_inv' : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀], Ring.inverse = Inv.inv
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolTag.deprecated : Lean.Lsp.SymbolTag
-- Mathlib.GroupTheory.QuotientGroup.Defs
Con.subgroup_quotientGroupCon : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) [inst_1 : H.Normal], (QuotientGroup.con H).subgroup = H
-- Init.Prelude
Nat.instDiv : Div ℕ
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- If `f : ℝ≥0 → ℝ≥0` is continuous on a compact set `s` and `f 0 = 0` and `a : X → A` is
continuous at `x₀`, and eventually `0 ≤ a x` and has quasispectrum contained in `s`, then
`fun x ↦ cfcₙ f (a x)` is continuous at `x₀`.  -/
ContinuousAt.cfcₙ_nnreal : ∀ {X : Type u_1} {A : Type u_2} [inst : NonUnitalNormedRing A] [inst_1 : StarRing A] [inst_2 : NormedSpace ℝ A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : SMulCommClass ℝ A A] [ContinuousStar A]
  [inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A]
  [inst_8 : StarOrderedRing A] [inst_9 : NonnegSpectrumClass ℝ A] [T2Space A] [IsSemitopologicalRing A]
  [inst_12 : TopologicalSpace X] {s : Set NNReal},
  IsCompact s →
    ∀ (f : NNReal → NNReal) {a : X → A} {x₀ : X},
      ContinuousAt a x₀ →
        (∀ᶠ (x : X) in nhds x₀, quasispectrum NNReal (a x) ⊆ s) →
          (∀ᶠ (x : X) in nhds x₀, 0 ≤ a x) →
            autoParam (ContinuousOn f s) ContinuousAt.cfcₙ_nnreal._auto_1 →
              autoParam (f 0 = 0) ContinuousAt.cfcₙ_nnreal._auto_3 → ContinuousAt (fun x => cfcₙ f (a x)) x₀
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.map_preΨ₄ : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] (W : WeierstrassCurve R) (f : R →+* S),
  (W.map f).preΨ₄ = Polynomial.map f W.preΨ₄
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.d₁_eq' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂] [inst_4 : K.HasTotal c₁₂]
  {i₁ i₁' : I₁},
  c₁.Rel i₁ i₁' →
    ∀ (i₂ : I₂) (i₁₂ : I₁₂),
      K.d₁ c₁₂ i₁ i₂ i₁₂ =
        c₁.ε₁ c₂ c₁₂ (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂) (K.ιTotalOrZero c₁₂ i₁' i₂ i₁₂)
-- Mathlib.Algebra.Group.Defs
nsmulBinRec.go_spec : ∀ {M : Type u_2} [inst : AddSemigroup M] [inst_1 : Zero M] (k : ℕ) (m n : M),
  nsmulBinRec.go (k + 1) m n = m + nsmulRec' (k + 1) n
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.insertMany_list_equiv_foldl : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ : Std.TreeSet α cmp} {l : List α},
  (t₁.insertMany l).Equiv (List.foldl (fun acc a => acc.insert a) t₁ l)
-- Plausible.Testable
/-- Disable output.
 -/
Plausible.Configuration.quiet : Plausible.Configuration → Bool
-- Mathlib.FieldTheory.Fixed
FixedPoints.instAlgebraSubtypeMemSubfieldSubfield : (M : Type u) →
  [inst : Monoid M] →
    (F : Type v) → [inst_1 : Field F] → [inst_2 : MulSemiringAction M F] → Algebra (↥(FixedPoints.subfield M F)) F
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueD_filter_not_contains_of_contains_right : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l₁ : List ((_ : α) × β)} {l₂ : List α} {k : α} {fallback : β},
  Std.Internal.List.DistinctKeys l₁ →
    l₂.contains k = true →
      Std.Internal.List.getValueD k (List.filter (fun p => !l₂.contains p.fst) l₁) fallback = fallback
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.instFaithfulModuleCatCarrierModulesSpecOfFunctor : ∀ {R : CommRingCat}, (AlgebraicGeometry.tilde.functor R).Faithful
-- Mathlib.CategoryTheory.Monoidal.Transport
/-- A type synonym for `D`, which will carry the transported monoidal structure.  -/
CategoryTheory.Monoidal.Transported : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → (C ≌ D) → Type u₂
-- Mathlib.Algebra.Field.Defs
Rat.smul_def : ∀ {K : Type u_1} [inst : DivisionRing K] (a : ℚ) (x : K), a • x = ↑a * x
-- Mathlib.Data.Set.Lattice.Image
Set.mapsTo_iInter : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {s : Set α} {t : ι → Set β} {f : α → β},
  Set.MapsTo f s (⋂ i, t i) ↔ ∀ (i : ι), Set.MapsTo f s (t i)
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Equivalence.unitIso_hom_app_comp_inverse_map_η_functor_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] (e : C ≌ D)
  [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal] [e.IsMonoidal] {Z : C}
  (h : e.inverse.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (e.unitIso.hom.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
      (CategoryTheory.CategoryStruct.comp (e.inverse.map (CategoryTheory.Functor.OplaxMonoidal.η e.functor)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε e.inverse) h
-- Mathlib.Probability.Martingale.Centering
MeasureTheory.stronglyAdapted_predictablePart : ∀ {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {f : ℕ → Ω → E} {ℱ : MeasureTheory.Filtration ℕ m0},
  MeasureTheory.StronglyAdapted ℱ fun n => MeasureTheory.predictablePart f ℱ μ (n + 1)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.all_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α] {p : α → β → Bool},
  (↑m).WF →
    ((↑m).all p = false ↔
      ∃ a, ∃ (h : m.contains a = true), p (m.getKey a h) (Std.DHashMap.Internal.Raw₀.Const.get m a h) = false)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getD_eq_fallback : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a : α}
  {fallback : β a}, a ∉ m → m.getD a fallback = fallback
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
/-- This could be used in conjunction with `CategoryTheory.NatIso.isIso_of_isIso_app`.  -/
AlgebraicGeometry.PresheafedSpace.isIso_of_components : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y)
  [CategoryTheory.IsIso f.base] [CategoryTheory.IsIso f.c], CategoryTheory.IsIso f
-- Lean.Meta.Tactic.Grind.Types
/-- Backtrackable state for the `GrindM` monad.
 -/
Lean.Meta.Grind.SavedState : Type
-- Mathlib.Topology.Inseparable
/-- **Alias** of the reverse direction of `stableUnderGeneralization_compl_iff`. -/
StableUnderSpecialization.compl : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, StableUnderSpecialization s → StableUnderGeneralization sᶜ
-- Mathlib.MeasureTheory.Measure.Map
MeasureTheory.Measure.mapₗ_mk_apply_of_aemeasurable : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {f : α → β} (hf : AEMeasurable f μ),
  (MeasureTheory.Measure.mapₗ (AEMeasurable.mk f hf)) μ = MeasureTheory.Measure.map f μ
-- Mathlib.CategoryTheory.FintypeCat
FintypeCat.equivEquivIso_apply_inv : ∀ {A B : FintypeCat} (e : A.obj ≃ B.obj), (FintypeCat.equivEquivIso e).inv = FintypeCat.homMk ⇑e.symm
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.toLp_zero : ∀ (p : ENNReal) {V : Type u_4} [inst : AddCommGroup V], WithLp.toLp p 0 = 0
-- Mathlib.Topology.Algebra.Order.Support
HasCompactMulSupport.sup : ∀ {X : Type u_1} {M : Type u_2} [inst : TopologicalSpace X] [inst_1 : One M] [inst_2 : SemilatticeSup M] {f g : X → M},
  HasCompactMulSupport f → HasCompactMulSupport g → HasCompactMulSupport (f ⊔ g)
-- Mathlib.Algebra.Order.Group.Bounds
IsLUB.exists_between_sub_self' : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] {s : Set α} {a ε : α},
  IsLUB s a → a ∉ s → 0 < ε → ∃ b ∈ s, a - ε < b ∧ b < a
-- Mathlib.Order.CompleteLattice.PiLex
Pi.Colex.instCompleteLinearOrderColexForall : {ι : Type u_1} →
  {α : ι → Type u_2} →
    [inst : LinearOrder ι] →
      [(i : ι) → CompleteLinearOrder (α i)] → [WellFoundedGT ι] → CompleteLinearOrder (Colex ((i : ι) → α i))
-- Mathlib.Analysis.Calculus.SmoothSeries
fderiv_tsum_apply : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedAddCommGroup F] [CompleteSpace F]
  {u : α → ℝ} [inst_6 : NormedSpace 𝕜 F] {f : α → E → F} {x₀ : E},
  Summable u →
    (∀ (n : α), Differentiable 𝕜 (f n)) →
      (∀ (n : α) (x : E), ‖fderiv 𝕜 (f n) x‖ ≤ u n) →
        (Summable fun n => f n x₀) → ∀ (x : E), fderiv 𝕜 (fun y => ∑' (n : α), f n y) x = ∑' (n : α), fderiv 𝕜 (f n) x
-- Init.Data.Array.Find
_private.Init.Data.Array.Find.0.Array.idxOf?.eq_1 : ∀ {α : Type u} [inst : BEq α] (xs : Array α) (v : α), xs.idxOf? v = Option.map (fun x => ↑x) (xs.finIdxOf? v)
-- Mathlib.Algebra.DirectSum.Decomposition
DirectSum.decompose_of_mem_same : ∀ {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [inst : DecidableEq ι] [inst_1 : AddCommMonoid M] [inst_2 : SetLike σ M]
  [inst_3 : AddSubmonoidClass σ M] (ℳ : ι → σ) [inst_4 : DirectSum.Decomposition ℳ] {x : M} {i : ι},
  x ∈ ℳ i → ↑(((DirectSum.decompose ℳ) x) i) = x
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.Faithful.of_comp_eq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C D}
  {G : CategoryTheory.Functor D E} {H : CategoryTheory.Functor C E} [ℋ : H.Faithful], F.comp G = H → F.Faithful
-- Lean.Message
Lean.indentExpr : Lean.Expr → Lean.MessageData
-- Mathlib.Topology.Category.CompHausLike.SigmaComparison
CompHausLike.instHasPropSigma : ∀ {P : TopCat → Prop} [CompHausLike.HasExplicitFiniteCoproducts P] {α : Type u} [Finite α] (σ : α → Type u)
  [inst : (a : α) → TopologicalSpace (σ a)] [∀ (a : α), CompactSpace (σ a)] [∀ (a : α), T2Space (σ a)]
  [∀ (a : α), CompHausLike.HasProp P (σ a)], CompHausLike.HasProp P ((a : α) × σ a)
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim
/-- Assume that a functor `X : J ⥤ C` maps any morphism to a monomorphism,
that `J` is filtered. Then the "inclusion" map `c.ι.app j₀` of a colimit cocone for `X`
is a monomorphism if `colim : (Under j₀ ⥤ C) ⥤ C` preserves monomorphisms
(e.g. when `C` satisfies AB5).  -/
CategoryTheory.Limits.IsColimit.mono_ι_app_of_isFiltered : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} J]
  {X : CategoryTheory.Functor J C} [∀ (j j' : J) (φ : j ⟶ j'), CategoryTheory.Mono (X.map φ)]
  {c : CategoryTheory.Limits.Cocone X} (hc : CategoryTheory.Limits.IsColimit c) [CategoryTheory.IsFiltered J] (j₀ : J)
  [inst_4 : CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Under j₀) C]
  [CategoryTheory.Limits.colim.PreservesMonomorphisms], CategoryTheory.Mono (c.ι.app j₀)
-- Mathlib.Data.ZMod.QuotientGroup
/-- The orbit `(ℤ • a) +ᵥ b` is a cycle of order `minimalPeriod (a +ᵥ ·) b`.  -/
AddAction.orbitZMultiplesEquiv : {α : Type u_5} →
  {β : Type u_6} →
    [inst : AddGroup α] →
      (a : α) →
        [inst_1 : AddAction α β] →
          (b : β) →
            ↑(AddAction.orbit (↥(AddSubgroup.zmultiples a)) b) ≃ ZMod (Function.minimalPeriod (fun x => a +ᵥ x) b)
-- Lean.Elab.Tactic.Grind.Param
_private.Lean.Elab.Tactic.Grind.Param.0.Lean.Elab.Tactic.parseModifier : String → Lean.CoreM Lean.Meta.Grind.AttrKind
-- Mathlib.Algebra.Regular.Defs
/-- A regular element `c` is left-regular  -/
IsRegular.left : ∀ {R : Type u_1} [inst : Mul R] {c : R}, IsRegular c → IsLeftRegular c
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
CategoryTheory.InjectiveResolution.descHomotopyZeroSucc.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {Y Z : C}
  {I : CategoryTheory.InjectiveResolution Y} {J : CategoryTheory.InjectiveResolution Z}
  (f f_1 : I.cocomplex ⟶ J.cocomplex) (e_f : f = f_1) (n : ℕ) (g g_1 : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n)
  (e_g : g = g_1) (g' g'_1 : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)) (e_g' : g' = g'_1)
  (w :
    f.f (n + 1) =
      CategoryTheory.CategoryStruct.comp (I.cocomplex.d (n + 1) (n + 2)) g' +
        CategoryTheory.CategoryStruct.comp g (J.cocomplex.d n (n + 1))),
  CategoryTheory.InjectiveResolution.descHomotopyZeroSucc f n g g' w =
    CategoryTheory.InjectiveResolution.descHomotopyZeroSucc f_1 n g_1 g'_1 ⋯
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
nonneg_of_mul_nonneg_left : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] {a b : R} [MulPosStrictMono R], 0 ≤ a * b → 0 < b → 0 ≤ a
-- Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
CliffordAlgebra.ofEven_ι : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (x y : M × R),
  (CliffordAlgebra.ofEven Q) (((CliffordAlgebra.even.ι (CliffordAlgebra.EquivEven.Q' Q)).bilin x) y) =
    ((CliffordAlgebra.ι Q) x.1 + (algebraMap R (CliffordAlgebra Q)) x.2) *
      ((CliffordAlgebra.ι Q) y.1 - (algebraMap R (CliffordAlgebra Q)) y.2)
-- Mathlib.Algebra.Module.Equiv.Basic
Module.compHom.toLinearEquiv_apply : ∀ {R : Type u_9} {S : Type u_10} [inst : Semiring R] [inst_1 : Semiring S] (g : R ≃+* S) (a : R),
  (Module.compHom.toLinearEquiv g) a = g a
-- Mathlib.SetTheory.Descriptive.Tree
/-- A variant of `List.drop` that takes values in `subAt`  -/
Descriptive.Tree.drop : {A : Type u_1} →
  (T : ↥(Descriptive.tree A)) → (n : ℕ) → (x : ↥T) → ↥(Descriptive.Tree.subAt T ↑(Descriptive.Tree.take n x))
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getD_empty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {a : α} {fallback : β},
  ∅.getD a fallback = fallback
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.condIndepFun_self_right : ∀ {Ω : Type u_1} {β : Type u_3} {β' : Type u_4} {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {mβ : MeasurableSpace β}
  {mβ' : MeasurableSpace β'} {X : Ω → β} {Z : Ω → β'},
  Measurable X → ∀ (hZ : Measurable Z), ProbabilityTheory.CondIndepFun (MeasurableSpace.comap Z inferInstance) ⋯ X Z μ
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.PreOneHypercover.map_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (E : CategoryTheory.PreOneHypercover X),
  E.map (CategoryTheory.Functor.id C) = E
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
TopCat.Presheaf.SheafConditionEqualizerProducts.w : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] {X : TopCat}
  (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X),
  CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.SheafConditionEqualizerProducts.res F U)
      (TopCat.Presheaf.SheafConditionEqualizerProducts.leftRes F U) =
    CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.SheafConditionEqualizerProducts.res F U)
      (TopCat.Presheaf.SheafConditionEqualizerProducts.rightRes F U)
-- Init.Data.Int.DivMod.Lemmas
Int.add_one_tdiv_of_pos : ∀ {a b : ℤ}, 0 < b → (a + 1).tdiv b = a.tdiv b + if 0 < a + 1 ∧ b ∣ a + 1 ∨ a < 0 ∧ b ∣ a then 1 else 0
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
/-- If a function `f : E → H` is differentiable at `x`, sends a neighbourhood `u` of `x` to a
closed convex set `s` with nonempty interior and has surjective differential at `x`, it must send
`x` to the interior of `s`.  -/
DifferentiableAt.mem_interior_convex_of_surjective_fderiv : ∀ {E : Type u_5} {H : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup H]
  [inst_3 : NormedSpace ℝ H] {f : E → H} {x : E},
  DifferentiableAt ℝ f x →
    ∀ {u : Set E},
      u ∈ nhds x →
        ∀ {s : Set H},
          Convex ℝ s →
            IsClosed s →
              (interior s).Nonempty → Set.MapsTo f u s → Function.Surjective ⇑(fderiv ℝ f x) → f x ∈ interior s
-- Qq.Macro
Qq.Impl.stripDollars : Lean.Name → Lean.Name
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.getKeyLTD_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {k fallback : α}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getKeyLTD k fallback = t₂.getKeyLTD k fallback
-- Init.Meta.Defs
Lean.quoteNameMk : Lean.Name → Lean.Term
-- Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
SummationFilter.tprod_symmetricIcc_eq_tprod_symmetricIco : ∀ {α : Type u_1} {f : ℤ → α} [inst : CommGroup α] [inst_1 : TopologicalSpace α] [ContinuousMul α] [T2Space α],
  Multipliable f (SummationFilter.symmetricIcc ℤ) →
    Filter.Tendsto (fun N => (f ↑N)⁻¹) Filter.atTop (nhds 1) →
      ∏'[SummationFilter.symmetricIco ℤ] (b : ℤ), f b = ∏'[SummationFilter.symmetricIcc ℤ] (b : ℤ), f b
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKeyD_insert_le_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α} {v : β k} {fallback : α},
  (compare ((Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.minKeyD fallback) k).isLE = true
-- Mathlib.Topology.Order.OrderClosed
eventually_le_nhds : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIciTopology α] {a b : α},
  a < b → ∀ᶠ (x : α) in nhds a, x ≤ b
-- Mathlib.Topology.Order.LiminfLimsup
BoundedGENhdsClass.mk : ∀ {α : Type u_7} [inst : Preorder α] [inst_1 : TopologicalSpace α],
  (∀ (a : α), Filter.IsBounded (fun x1 x2 => x1 ≥ x2) (nhds a)) → BoundedGENhdsClass α
-- Mathlib.AlgebraicGeometry.Cover.Over
AlgebraicGeometry.Scheme.instOverXPullbackCoverOverProp' : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  (S : AlgebraicGeometry.Scheme) →
    [inst : P.IsStableUnderBaseChange] →
      [inst_1 : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] →
        {X W : AlgebraicGeometry.Scheme} →
          (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) →
            (f : W ⟶ X) →
              [inst_2 : W.Over S] →
                [inst_3 : X.Over S] →
                  [inst_4 : AlgebraicGeometry.Scheme.Cover.Over S 𝒰] →
                    [inst_5 : AlgebraicGeometry.Scheme.Hom.IsOver f S] →
                      {Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
                        [inst_6 : Q.HasOfPostcompProperty Q] →
                          [inst_7 : Q.IsStableUnderBaseChange] →
                            [inst_8 : Q.IsStableUnderComposition] →
                              (hX : Q (X ↘ S)) →
                                (hW : Q (W ↘ S)) →
                                  (hQ : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)) →
                                    (j : 𝒰.I₀) →
                                      ((AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp' S 𝒰 f hX hW hQ).X j).Over
                                        S
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.PartialIso.trans_iso : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X.PartialIso Y) (g : Y.PartialIso Z),
  (f.trans g).iso =
    (f.symm.restrictSource (f.target ⊓ g.source) ⋯ ⋯).iso.symm ≪≫
      Y.isoOfEq ⋯ ≪≫
        (AlgebraicGeometry.Scheme.Opens.isoOfLE ⋯).symm ≪≫
          AlgebraicGeometry.Scheme.Hom.isoImage g.iso.hom
              ((TopologicalSpace.Opens.map g.source.ι.base).obj (f.target ⊓ g.source)) ≪≫
            AlgebraicGeometry.Scheme.Hom.isoImage g.target.ι
              ((AlgebraicGeometry.Scheme.Hom.opensFunctor g.iso.hom).obj
                ((TopologicalSpace.Opens.map g.source.ι.base).obj (f.target ⊓ g.source)))
-- Mathlib.Order.BooleanAlgebra.Basic
sdiff_sdiff_sdiff_cancel_right : ∀ {α : Type u} {x y z : α} [inst : GeneralizedBooleanAlgebra α], z ≤ y → (x \ z) \ (y \ z) = x \ y
-- Mathlib.NumberTheory.Cyclotomic.Discriminant
IsPrimitiveRoot.powerBasis.congr_simp : ∀ {n n_1 : ℕ} (e_n : n = n_1) [inst : NeZero n] (K : Type u) {L : Type v} [inst_1 : Field K] [inst_2 : CommRing L]
  [inst_3 : IsDomain L] [inst_4 : Algebra K L] [inst_5 : IsCyclotomicExtension {n} K L] {ζ ζ_1 : L} (e_ζ : ζ = ζ_1)
  (hζ : IsPrimitiveRoot ζ n), IsPrimitiveRoot.powerBasis K hζ = IsPrimitiveRoot.powerBasis K ⋯
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
/-- [Stacks Tag 030H](https://stacks.math.columbia.edu/tag/030H) -/
trdeg_add_eq : ∀ (R : Type u_1) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Nontrivial R]
  {A : Type v} [inst_4 : CommRing A] [NoZeroDivisors A] [inst_6 : Algebra R A] [inst_7 : Algebra S A] [FaithfulSMul R S]
  [FaithfulSMul S A] [IsScalarTower R S A], Algebra.trdeg R S + Algebra.trdeg S A = Algebra.trdeg R A
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_filter_not_contains_iff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α}
  {hl₁ : Std.Internal.List.DistinctKeys l₁} {k : α},
  Std.Internal.List.containsKey k (List.filter (fun p => !l₂.contains p.fst) l₁) = true ↔
    Std.Internal.List.containsKey k l₁ = true ∧ ¬l₂.contains k = true
-- Lean.Elab.Task
/-- Given a monadic value in `CoreM`, creates a task that runs it in the current state,
returning a monadic value with the cached result (and subsequent state as it was after running).
 -/
Lean.Core.CoreM.asTask' : {α : Type} → Lean.CoreM α → Lean.CoreM (Task (Lean.CoreM α))
-- Std.Time.Format.Basic
/-- Parses a string into a format using the provided format type `f`.
 -/
Std.Time.Format.parse : {f : Type} →
  {typ : Type → f → Type} →
    [self : Std.Time.Format f typ] → {α : Type} → (fmt : f) → typ (Option α) fmt → String → Except String α
-- Mathlib.AlgebraicGeometry.Modules.Tilde
/-- (Implementation). The image of `tilde` under `modulesSpecToSheaf` is isomorphic to
`structurePresheafInModuleCat`. They are defeq as types but the `Smul` instance are not defeq.  -/
AlgebraicGeometry.tilde.modulesSpecToSheafIso : {R : CommRingCat} →
  (M : ModuleCat ↑R) →
    (AlgebraicGeometry.modulesSpecToSheaf.obj (AlgebraicGeometry.tilde M)).obj ≅
      AlgebraicGeometry.structurePresheafInModuleCat ↑R ↑M
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- The function `fun z ↦ (z - w) ^ n`, `n : ℤ`, is circle integrable on the circle with center `c`
and radius `|R|` if and only if `R = 0` or `0 ≤ n`, or `w` does not belong to this circle.  -/
circleIntegrable_sub_zpow_iff : ∀ {c w : ℂ} {R : ℝ} {n : ℤ}, CircleIntegrable (fun z => (z - w) ^ n) c R ↔ R = 0 ∨ 0 ≤ n ∨ w ∉ Metric.sphere c |R|
-- Mathlib.SetTheory.Ordinal.Exponential
/-- `opow b` and `log b` (almost) form a Galois connection.

See `lt_opow_iff_log_lt` for a variant assuming `x ≠ 0` rather than `c ≠ 0`. See also
`lt_opow_of_log_lt` and `lt_log_of_lt_opow`, which are both separate implications under weaker
assumptions.  -/
Ordinal.lt_opow_iff_log_lt' : ∀ {b x c : Ordinal.{u_1}}, 1 < b → c ≠ 0 → (x < b ^ c ↔ Ordinal.log b x < c)
-- Lean.Meta.AppBuilder
Lean.Meta.mkImpCongr : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.instNatCast : {R : Type u} → [inst : Semiring R] → NatCast (Polynomial R)
-- Mathlib.Logic.Equiv.Defs
Equiv.symm_bijective : ∀ {α : Sort u} {β : Sort v}, Function.Bijective Equiv.symm
-- Init.Data.String.Lemmas.Pattern.Split.Char
String.toList_split_char : ∀ {s : String} {c : Char},
  List.map String.Slice.copy (s.split c).toList = List.map String.ofList (List.splitOn c s.toList)
-- Mathlib.RepresentationTheory.Rep.Basic
_private.Mathlib.RepresentationTheory.Rep.Basic.0.Rep.mk : {k : Type u} →
  {G : Type v} →
    [inst : Semiring k] →
      [inst_1 : Monoid G] →
        (V : Type w) → [hV1 : AddCommGroup V] → [hV2 : Module k V] → Representation k G V → Rep.{w, u, v} k G