mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.TietzeExtension
/-- **Tietze extension theorem** for real-valued bounded continuous maps, a version for a closed
embedding. Let `e` be a closed embedding of a nonempty topological space `X` into a normal
topological space `Y`. Let `f` be a bounded continuous real-valued function on `X`. Let `t` be
a nonempty convex set of real numbers (we use `OrdConnected` instead of `Convex` to automatically
deduce this argument by typeclass search) such that `f x ∈ t` for all `x`. Then there exists
a bounded continuous real-valued function `g : Y →ᵇ ℝ` such that `g y ∈ t` for all `y` and
`g ∘ e = f`.  -/
BoundedContinuousFunction.exists_extension_forall_mem_of_isClosedEmbedding : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [NormalSpace Y]
  (f : BoundedContinuousFunction X ℝ) {t : Set ℝ} {e : X → Y} [hs : t.OrdConnected],
  (∀ (x : X), f x ∈ t) → t.Nonempty → Topology.IsClosedEmbedding e → ∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
/-- This is the isomorphism of simplicial sets corresponding to
an equality of subcomplexes.  -/
SSet.Subcomplex.eqToIso : {X : SSet} → {S₁ S₂ : X.Subcomplex} → S₁ = S₂ → (S₁.toSSet ≅ S₂.toSSet)
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.mul.eq_1 : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n m : ℕ} (χ₁ : DirichletCharacter R n) (χ₂ : DirichletCharacter R m),
  χ₁.mul χ₂ = (DirichletCharacter.changeLevel ⋯) χ₁ * (DirichletCharacter.changeLevel ⋯) χ₂
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.touchpointWeights_eq_zero : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] {s : Affine.Simplex ℝ P n} {signs : Finset (Fin (n + 1))}
  (i : Fin (n + 1)), s.touchpointWeights signs i i = 0
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RioSlice : (α : Type u_1) → [Ord α] → Type u_1
-- Mathlib.Combinatorics.Additive.Convolution
Finset.convolution_le_card_left : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {A B : Finset G} {x : G}, A.convolution B x ≤ A.card
-- Mathlib.Logic.Equiv.List
_private.Mathlib.Logic.Equiv.List.0.Encodable.decodeList.match_3.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((v : ℕ) → motive v.succ) → motive x
-- Mathlib.Order.Filter.Map
Filter.map_inf' : ∀ {α : Type u_1} {β : Type u_2} {f g : Filter α} {m : α → β} {t : Set α},
  t ∈ f → t ∈ g → Set.InjOn m t → Filter.map m (f ⊓ g) = Filter.map m f ⊓ Filter.map m g
-- Mathlib.NumberTheory.RamificationInertia.Ramification
Ideal.ramificationIdx'_ne_one_iff : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal R}
  {P : Ideal S}, Ideal.map (algebraMap R S) p ≤ P → (p.ramificationIdx' P ≠ 1 ↔ Ideal.map (algebraMap R S) p ≤ P ^ 2)
-- Mathlib.Probability.Distributions.Cauchy
ProbabilityTheory.cauchyPDFReal_scale_zero : ∀ (x₀ : ℝ), ProbabilityTheory.cauchyPDFReal x₀ 0 = 0
-- Mathlib.Topology.EMetricSpace.Defs
edist_ofMul : ∀ {X : Type u_1} [inst : EDist X] (a b : X), edist (Additive.ofMul a) (Additive.ofMul b) = edist a b
-- Mathlib.Analysis.Convex.Cone.Dual
ProperCone.congr_simp : ∀ (R : Type u_2) (E : Type u_3) [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : TopologicalSpace E] [inst_5 : Module R E], ProperCone R E = ProperCone R E
-- Mathlib.Algebra.Lie.Abelian
LieSubmodule.lie_abelian_iff_lie_self_eq_bot : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L),
  IsLieAbelian ↥I ↔ ⁅I, I⁆ = ⊥
-- Mathlib.Probability.Kernel.Category.SFinKer
SFinKer.tensorUnit_str : (CategoryTheory.MonoidalCategoryStruct.tensorUnit SFinKer).str = PUnit.instMeasurableSpace
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.zero_comp : ∀ {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃]
  {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {M₁ : Type u_4} [inst_3 : TopologicalSpace M₁]
  [inst_4 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_5 : TopologicalSpace M₂] [inst_6 : AddCommMonoid M₂] {M₃ : Type u_7}
  [inst_7 : TopologicalSpace M₃] [inst_8 : AddCommMonoid M₃] [inst_9 : Module R₁ M₁] [inst_10 : Module R₂ M₂]
  [inst_11 : Module R₃ M₃] [inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M₁ →SL[σ₁₂] M₂), 0 ∘SL f = 0
-- Mathlib.CategoryTheory.Elements
CategoryTheory.CategoryOfElements.map_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} {p q : F.Elements}
  (f : p ⟶ q), (CategoryTheory.ConcreteCategory.hom (F.map ↑f)) p.snd = q.snd
-- Mathlib.Algebra.Ring.TransferInstance
/-- Transfer `IsDomain` across an `Equiv`  -/
Equiv.isDomain : ∀ {α : Type u_1} {β : Type u_2} [inst : Semiring β] [IsDomain β] (e : α ≃ β), IsDomain α
-- Init.Omega.IntList
Lean.Omega.IntList.sum_nil : Lean.Omega.IntList.sum [] = 0
-- Mathlib.Topology.Hom.ContinuousEval
ContinuousAt.eval : ∀ {F : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [inst : FunLike F X Y] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace X] [inst_3 : TopologicalSpace Y] [ContinuousEval F X Y] [inst_5 : TopologicalSpace Z]
  {f : Z → F} {g : Z → X} {z : Z}, ContinuousAt f z → ContinuousAt g z → ContinuousAt (fun z => (f z) (g z)) z
-- Aesop.Tree.ExtractProof
_private.Aesop.Tree.ExtractProof.0.Aesop.extractProofGoal : Lean.Environment → Aesop.Goal → Lean.MetaM Unit
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
/-- The cone of topological modules associated to a cone over the underlying modules, where
the cone point is given the induced topology. This is limiting when the given cone is.  -/
TopModuleCat.ofCone : {R : Type u} →
  [inst : Ring R] →
    [inst_1 : TopologicalSpace R] →
      {J : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_1, u_2} J] →
          {F : CategoryTheory.Functor J (TopModuleCat R)} →
            CategoryTheory.Limits.Cone (F.comp (CategoryTheory.forget₂ (TopModuleCat R) (ModuleCat R))) →
              CategoryTheory.Limits.Cone F
-- Mathlib.Algebra.Homology.SpectralObject.Page
/-- Constructor for morphisms to `E^{n₁}(f₁, f₂, f₃)`.  -/
CategoryTheory.Abelian.SpectralObject.liftE : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          (X : CategoryTheory.Abelian.SpectralObject C ι) →
            {i j k l : ι} →
              (f₁ : i ⟶ j) →
                (f₂ : j ⟶ k) →
                  (f₃ : k ⟶ l) →
                    (f₂₃ : j ⟶ l) →
                      (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) →
                        (n₀ n₁ n₂ : ℤ) →
                          {A : C} →
                            (x : A ⟶ (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f₂₃)) →
                              CategoryTheory.CategoryStruct.comp x
                                    ((X.H n₁).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃)) =
                                  0 →
                                (hn₂ : n₁ + 1 = n₂) →
                                  CategoryTheory.CategoryStruct.comp x (X.δ f₁ f₂₃ n₁ n₂ hn₂) = 0 →
                                    (hn₁ :
                                        autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.liftE._auto_1) →
                                      A ⟶ X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.mk'_eq_iff_mk'_eq : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) (g : S.LocalizationMap P) {x₁ x₂ : M} {y₁ y₂ : ↥S},
  f.mk' x₁ y₁ = f.mk' x₂ y₂ ↔ g.mk' x₁ y₁ = g.mk' x₂ y₂
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- **Alias** of `NumberField.FinitePlace.equivHeightOneSpectrum_symm_apply`. -/
NumberField.FinitePlace.IsDedekindDomain.HeightOneSpectrum.equivHeightOneSpectrum_symm_apply : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (x : K),
  (NumberField.FinitePlace.equivHeightOneSpectrum.symm v) x = ‖(NumberField.FinitePlace.embedding v) x‖
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.π₁Toπ₂_comp_π₂Toπ₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C],
  CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex.π₁Toπ₂ CategoryTheory.ShortComplex.π₂Toπ₃ = 0
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.IsRoot.def : ∀ {R : Type u} {a : R} [inst : Semiring R] {p : Polynomial R}, p.IsRoot a ↔ Polynomial.eval a p = 0
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- `g : R →+* S` is `R`-linear when the module structure on `S` is `Module.compHom S g` .  -/
Module.compHom.toLinearMap : {R : Type u_14} → {S : Type u_15} → [inst : Semiring R] → [inst_1 : Semiring S] → (g : R →+* S) → R →ₗ[R] S
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
ContinuousAlternatingMap.instUniformContinuousConstSMul : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : UniformSpace F] [inst_7 : IsUniformAddGroup F] {M : Type u_5} [inst_8 : Monoid M]
  [inst_9 : DistribMulAction M F] [inst_10 : SMulCommClass 𝕜 M F] [inst_11 : ContinuousConstSMul M F],
  UniformContinuousConstSMul M (E [⋀^ι]→L[𝕜] F)
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.throwUnexpectedType : {α : Type} → Lean.Name → Lean.Name → ExceptT String Id α
-- Batteries.Data.Fin.Coding
/-- Decode `Char` from `Fin Char.count`.  -/
Fin.decodeChar : Fin Char.count → Char
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.sin_arcsin' : ∀ {x : ℝ}, x ∈ Set.Icc (-1) 1 → Real.sin (Real.arcsin x) = x
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.imageSubobject_arrow'_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasImage f] {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectIso f).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject f).arrow h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f) h
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.values_emptyWithCapacity : ∀ {α : Type u} {c : ℕ} {β : Type v}, (↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity c)).values = []
-- Mathlib.Analysis.Calculus.Deriv.Comp
HasStrictDerivAt.comp : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (x : 𝕜) {𝕜' : Type u_1} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {h : 𝕜 → 𝕜'} {h₂ : 𝕜' → 𝕜'} {h' h₂' : 𝕜'},
  HasStrictDerivAt h₂ h₂' (h x) → HasStrictDerivAt h h' x → HasStrictDerivAt (h₂ ∘ h) (h₂' * h') x
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.instLaxMonoidalDiscretePUnitMonToLaxMonoidalObj.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (A : CategoryTheory.AddMon C),
  CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.instLaxMonoidalDiscretePUnitMonToLaxMonoidalObj A =
    { ε := CategoryTheory.AddMonObj.zero, μ := fun x x_1 => CategoryTheory.AddMonObj.add, μ_natural_left := ⋯,
      μ_natural_right := ⋯, associativity := ⋯, left_unitality := ⋯, right_unitality := ⋯ }
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.Δ_of_char_three : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [CharP R 3], W.Δ = -W.b₂ ^ 2 * W.b₈ - 8 * W.b₄ ^ 3
-- Std.Data.DHashMap.Internal.Index
/-- `sz` is an explicit parameter because having it inferred from `h` can lead to suboptimal IR,
cf. https://github.com/leanprover/lean4/issues/4157
 -/
Std.DHashMap.Internal.mkIdx : (sz : ℕ) → 0 < sz → UInt64 → { u // u.toNat < sz }
-- Lean.MonadEnv
Lean.isDefn? : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Lean.Name → m (Option Lean.DefinitionVal)
-- Mathlib.Order.Closure
LowerAdjoint.mk.injEq : ∀ {α : Type u_1} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {u : β → α} (toFun : α → β)
  (gc' : GaloisConnection toFun u) (toFun_1 : α → β) (gc'_1 : GaloisConnection toFun_1 u),
  ({ toFun := toFun, gc' := gc' } = { toFun := toFun_1, gc' := gc'_1 }) = (toFun = toFun_1)
-- Mathlib.RingTheory.TotallySplit
Algebra.IsFiniteSplit.of_algEquiv : ∀ {R : Type u_2} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {S' : Type u_4}
  [inst_3 : CommRing S'] [inst_4 : Algebra R S'] (e : S ≃ₐ[R] S') [Algebra.IsFiniteSplit R S],
  Algebra.IsFiniteSplit R S'
-- Mathlib.Topology.Algebra.Valued.ValuationTopology
Valued.mem_nhds : ∀ {R : Type u} [inst : Ring R] {Γ₀ : Type v} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀] {s : Set R}
  {x : R}, s ∈ nhds x ↔ ∃ γ, {y | Valued.v.restrict (y - x) < ↑γ} ⊆ s
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.factors_self : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] [Nontrivial α] {p : Associates α}
  (hp : Irreducible p), p.factors = ↑{⟨p, hp⟩}
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.neg_comp : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_8} {M₂ : Type u_10} {N₃ : Type u_13} [inst : Semiring R₁]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommGroup N₃] [inst_6 : Module R₁ M] [inst_7 : Module R₂ M₂] [inst_8 : Module R₃ N₃] {σ₁₂ : R₁ →+* R₂}
  {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] N₃),
  (-g) ∘ₛₗ f = -g ∘ₛₗ f
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toArray_rio_eq_zero : ∀ {n i : ℕ}, n ≤ i → (*...n).toArray[i]! = 0
-- Mathlib.Analysis.Asymptotics.LinearGrowth
/-- Lower linear growth as an `InfTopHom`.  -/
LinearGrowth.linearGrowthInfTopHom : InfTopHom (ℕ → EReal) EReal
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePushoutShape.instDecidableEqHom.decEq : {J : Type u_1} →
  {a a_1 : CategoryTheory.Limits.WidePushoutShape J} → [DecidableEq J] → (x x_1 : a.Hom a_1) → Decidable (x = x_1)
-- Init.Data.Array.Lemmas
Array.foldl_hom : ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} (f : α₁ → α₂) {g₁ : α₁ → β → α₁} {g₂ : α₂ → β → α₂} {xs : Array β}
  {init : α₁}, (∀ (x : α₁) (y : β), g₂ (f x) y = f (g₁ x y)) → Array.foldl g₂ (f init) xs = f (Array.foldl g₁ init xs)
-- Mathlib.Algebra.Group.Hom.Defs
OneHom.comp_id : ∀ {M : Type u_4} {N : Type u_5} [inst : One M] [inst_1 : One N] (f : OneHom M N), f.comp (OneHom.id M) = f
-- Mathlib.Data.EReal.Inv
EReal.add_div_of_nonneg_right : ∀ {a b c : EReal}, 0 ≤ c → (a + b) / c = a / c + b / c
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
ExteriorAlgebra.ι_mul_prod_list : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {n : ℕ}
  (f : Fin n → M) (i : Fin n), (ExteriorAlgebra.ι R) (f i) * (List.ofFn fun i => (ExteriorAlgebra.ι R) (f i)).prod = 0
-- Mathlib.Probability.Density
ProbabilityTheory.IndepFun.pdf_mul_eq_mlconvolution_pdf : ∀ {Ω : Type u_1} {G : Type u_2} {mΩ : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} [inst : Group G]
  {mG : MeasurableSpace G} [MeasurableMul₂ G] [MeasurableInv G] {μ : MeasureTheory.Measure G} [μ.IsMulLeftInvariant]
  {X Y : Ω → G} [MeasureTheory.SFinite μ] [MeasureTheory.HasPDF X ℙ μ] [MeasureTheory.HasPDF Y ℙ μ]
  [MeasureTheory.IsFiniteMeasure ℙ],
  ProbabilityTheory.IndepFun X Y ℙ →
    MeasureTheory.pdf (X * Y) ℙ μ =ᵐ[μ]
      MeasureTheory.mlconvolution (MeasureTheory.pdf X ℙ μ) (MeasureTheory.pdf Y ℙ μ) μ
-- Mathlib.Probability.Process.Predictable
_private.Mathlib.Probability.Process.Predictable.0.MeasureTheory.IsStronglyPredictable.of_measurable_add_one.match_1_1.congr_eq_2 : ∀ (motive : ℕ → Sort u_1) (x : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ) (n : ℕ),
  x = n.succ →
    (match x with
      | 0 => h_1 ()
      | n.succ => h_2 n) ≍
      h_2 n
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_filter! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] {f : (a : α) → β a → Bool} {k : α} {fallback : β k},
  t.WF → (Std.DTreeMap.Internal.Impl.filter! f t).getD k fallback = (Option.filter (f k) (t.get? k)).getD fallback
-- Init.Data.List.Sublist
List.IsInfix.eq_of_length : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+: l₂ → l₁.length = l₂.length → l₁ = l₂
-- Mathlib.MeasureTheory.Function.AEMeasurableSequence
aeSeq.aeSeq_eq_mk_of_mem_aeSeqSet : ∀ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : ι → α → β}
  {μ : MeasureTheory.Measure α} {p : α → (ι → β) → Prop} (hf : ∀ (i : ι), AEMeasurable (f i) μ) {x : α},
  x ∈ aeSeqSet hf p → ∀ (i : ι), aeSeq hf p i x = AEMeasurable.mk (f i) ⋯ x
-- Mathlib.CategoryTheory.Dialectica.Basic
CategoryTheory.Dial.id_F : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X : CategoryTheory.Dial C),
  (CategoryTheory.CategoryStruct.id X).F = CategoryTheory.Limits.prod.snd
-- Init.Data.List.MinMaxOn
/-- `List.minOn?` returns `none` when applied to an empty list.  -/
List.minOn?_nil : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β}, List.minOn? f [] = none
-- Mathlib.GroupTheory.SpecificGroups.Quaternion
QuaternionGroup.a_mul_xa : ∀ {n : ℕ} (i j : ZMod (2 * n)), QuaternionGroup.a i * QuaternionGroup.xa j = QuaternionGroup.xa (j - i)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.mem_iff : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {k : α}, m₁.WF → m₂.WF → m₁.Equiv m₂ → (k ∈ m₁ ↔ k ∈ m₂)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_le_algebraMap : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [ContinuousSqrt R]
  [StarOrderedRing R] [inst_8 : TopologicalSpace A] [inst_9 : Ring A] [inst_10 : StarRing A] [inst_11 : PartialOrder A]
  [StarOrderedRing A] [inst_13 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (f : R → R) (r : R)
  (a : A),
  (∀ x ∈ spectrum R a, f x ≤ r) →
    autoParam (ContinuousOn f (spectrum R a)) cfc_le_algebraMap._auto_1 →
      autoParam (p a) cfc_le_algebraMap._auto_3 → cfc f a ≤ (algebraMap R A) r
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- The functor `Fin (l + 1) ⥤ Fin (n + 1)` which sends `i` to `k + i`  -/
Fin.natAddLEFunctor : {n k l : ℕ} → k + l ≤ n → CategoryTheory.Functor (Fin (l + 1)) (Fin (n + 1))
-- Mathlib.Algebra.Group.Subgroup.Ker
/-- The canonical surjective `AddGroup` homomorphism `G →+ f(G)` induced by a group
homomorphism `G →+ N`.  -/
AddMonoidHom.rangeRestrict : {G : Type u_1} → [inst : AddGroup G] → {N : Type u_5} → [inst_1 : AddGroup N] → (f : G →+ N) → G →+ ↥f.range
-- Init.Data.SInt.Lemmas
Int8.ofBitVec_sdiv : ∀ (a b : BitVec 8), Int8.ofBitVec (a.sdiv b) = Int8.ofBitVec a / Int8.ofBitVec b
-- Mathlib.Analysis.Convex.Star
StarConvex.is_linear_preimage : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid F] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜 F] {x : E} {s : Set F} {f : E → F},
  StarConvex 𝕜 (f x) s → IsLinearMap 𝕜 f → StarConvex 𝕜 x (f ⁻¹' s)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
HasFDerivAt.arctan : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {x : E},
  HasFDerivAt f f' x → HasFDerivAt (fun x => Real.arctan (f x)) ((1 / (1 + f x ^ 2)) • f') x
-- Mathlib.Algebra.Group.Basic
DivisionMonoid.toDivInvOneMonoid.eq_1 : ∀ {α : Type u_1} [inst : DivisionMonoid α],
  DivisionMonoid.toDivInvOneMonoid = { toDivInvMonoid := inst.toDivInvMonoid, inv_one := ⋯ }
-- Lean.Meta.Sym.AlphaShareCommon
_private.Lean.Meta.Sym.AlphaShareCommon.0.Lean.Meta.Sym.visit : Lean.Expr → Lean.Meta.Sym.M✝ Lean.Expr → Lean.Meta.Sym.M✝ Lean.Expr
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get_modify_self : ∀ {α : Type u} {instOrd : Ord α} [inst : Std.TransOrd α] {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  (h : t.WF) {k : α} {f : β → β} {hc : k ∈ Std.DTreeMap.Internal.Impl.Const.modify k f t},
  Std.DTreeMap.Internal.Impl.Const.get (Std.DTreeMap.Internal.Impl.Const.modify k f t) k hc =
    f (Std.DTreeMap.Internal.Impl.Const.get t k ⋯)
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
measurableSet_preimage : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {t : Set β},
  Measurable f → MeasurableSet t → MeasurableSet (f ⁻¹' t)
-- Init.Data.UInt.Lemmas
UInt8.toBitVec_ofNatTruncate_of_lt : ∀ {n : ℕ} (hn : n < UInt8.size), (UInt8.ofNatClamp n).toBitVec = n#'hn
-- Mathlib.RingTheory.IsTensorProduct
Algebra.IsPushout.cancelBaseChangeAlg_tmul : ∀ (R : Type u_1) (S : Type v₃) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (A : Type u_8)
  (B : Type u_9) [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  [inst_7 : Algebra A B] [inst_8 : Algebra S B] [inst_9 : IsScalarTower R A B] [inst_10 : IsScalarTower R S B]
  [inst_11 : Algebra.IsPushout R S A B] (C : Type u_11) [inst_12 : CommRing C] [inst_13 : Algebra R C]
  [inst_14 : Algebra A C] [inst_15 : IsScalarTower R A C] (c : C),
  (Algebra.IsPushout.cancelBaseChangeAlg R S A B C) (1 ⊗ₜ[A] c) = 1 ⊗ₜ[R] c
-- Init.Data.Dyadic.Basic
Dyadic.toRat_ofOdd_eq_mul_two_pow : ∀ {n k : ℤ} {hn : n % 2 = 1}, (Dyadic.ofOdd n k hn).toRat = ↑n * 2 ^ (-k)
-- Init.Meta.Defs
Lean.TSyntax.instCoeIdentLevel : Coe Lean.Ident Lean.Syntax.Level
-- Batteries.Data.List.Lemmas
List.dropPrefix?.eq_1 : ∀ {α : Type u_1} [inst : BEq α] (x : List α), x.dropPrefix? [] = some x
-- Mathlib.Algebra.Quandle
/-- Relations for the enveloping group. This is a type-valued relation because
`toEnvelGroup.mapAux.well_def` inducts on it to show `toEnvelGroup.map`
is well-defined.  The relation `PreEnvelGroupRel` is the `Prop`-valued version,
which is used to define `EnvelGroup` itself.
 -/
Rack.PreEnvelGroupRel' : (R : Type u) → [Rack R] → Rack.PreEnvelGroup R → Rack.PreEnvelGroup R → Type u
-- Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Nat.nthRoot_pow : ∀ {n : ℕ}, n ≠ 0 → ∀ (a : ℕ), n.nthRoot (a ^ n) = a
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.ringHom_ext : ∀ {R : Type uR} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] {C : Type u_3} [inst_5 : Semiring C] {f g : TensorProduct R A B →+* C},
  f.comp Algebra.TensorProduct.includeLeftRingHom = g.comp Algebra.TensorProduct.includeLeftRingHom →
    f.comp Algebra.TensorProduct.includeRight.toRingHom = g.comp Algebra.TensorProduct.includeRight.toRingHom → f = g
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.restrictScalars_injective : ∀ (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [inst : Monoid R] [inst_1 : Monoid S]
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : MulAction R S]
  [inst_5 : DistribMulAction S A] [inst_6 : DistribMulAction S B] [inst_7 : DistribMulAction R A]
  [inst_8 : DistribMulAction R B] [inst_9 : IsScalarTower R S A] [inst_10 : IsScalarTower R S B],
  Function.Injective (NonUnitalAlgHom.restrictScalars R)