mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey!_modify : ∀ {α : Type u} {instOrd : Ord α} [Std.TransOrd α] {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β},
  t.WF →
    ∀ [inst : Inhabited α] {k k' : α} {f : β → β},
      (Std.DTreeMap.Internal.Impl.Const.modify k f t).getKey! k' =
        if compare k k' = Ordering.eq then if k ∈ t then k else default else t.getKey! k'
-- Init.Data.Nat.Div.Basic
Nat.mul_div_left : ∀ (m : ℕ) {n : ℕ}, 0 < n → m * n / n = m
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
/-- Half of **Jordan's inequality** for negative values.  -/
Real.sin_le_mul : ∀ {x : ℝ}, -(Real.pi / 2) ≤ x → x ≤ 0 → Real.sin x ≤ 2 / Real.pi * x
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ico_filter_lt_of_right_le : ∀ {α : Type u_2} {a b c : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α]
  [inst_2 : DecidablePred fun x => x < c], b ≤ c → {x ∈ Finset.Ico a b | x < c} = Finset.Ico a b
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.SimpleFunc.integral.eq_1 : ∀ {α : Type u_1} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {x : MeasurableSpace α}
  (μ : MeasureTheory.Measure α) (f : MeasureTheory.SimpleFunc α F),
  MeasureTheory.SimpleFunc.integral μ f = MeasureTheory.SimpleFunc.setToSimpleFunc (MeasureTheory.weightedSMul μ) f
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getD_eq_fallback_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {a : α} {fallback : β a}, t.contains a = false → t.getD a fallback = fallback
-- Mathlib.Order.Filter.CountablyGenerated
/-- There exists a countable set that generates the filter.  -/
Filter.IsCountablyGenerated.out : ∀ {α : Type u_1} {f : Filter α} [self : f.IsCountablyGenerated], ∃ s, s.Countable ∧ f = Filter.generate s
-- Mathlib.Algebra.Group.End
Equiv.nsmul_addRight : ∀ {α : Type u_4} [inst : AddGroup α] (a : α) (n : ℕ), Equiv.addRight a ^ n = Equiv.addRight (n • a)
-- Mathlib.CategoryTheory.Sites.Preserves
/-- If `F` is a presheaf which `IsSheafFor` a presieve of arrows and the empty presieve, then it
preserves the product corresponding to the presieve of arrows.
 -/
CategoryTheory.Presieve.preservesProduct_of_isSheafFor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : C} (F : CategoryTheory.Functor Cᵒᵖ (Type w)),
  CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows Empty.elim fun a => Empty.instIsEmpty.elim a) →
    ∀ (hI : CategoryTheory.Limits.IsInitial I) {α : Type u_1} [Small.{w, u_1} α] {X : α → C}
      (c : CategoryTheory.Limits.Cofan X) (hc : CategoryTheory.Limits.IsColimit c)
      [(CategoryTheory.Presieve.ofArrows X c.inj).HasPairwisePullbacks] [inst_3 : CategoryTheory.Limits.HasInitial C]
      [∀ (i : α), CategoryTheory.Mono (c.inj i)],
      (Pairwise fun i j =>
          CategoryTheory.IsPullback (CategoryTheory.Limits.initial.to (X i)) (CategoryTheory.Limits.initial.to (X j))
            (c.inj i) (c.inj j)) →
        CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows X c.inj) →
          CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor fun x => Opposite.op (X x)) F
-- Std.Tactic.Do.Syntax
/-- `mspecialize` is like `specialize`, but operating on a stateful `Std.Do.SPred` goal.
It specializes a hypothesis from the stateful context with hypotheses from either the pure
or stateful context or pure terms.
```lean
example (P Q : SPred σs) : P ⊢ₛ (P → Q) → Q := by
  mintro HP HPQ
  mspecialize HPQ HP
  mexact HPQ

example (y : Nat) (P Q : SPred σs) (Ψ : Nat → SPred σs) (hP : ⊢ₛ P) : ⊢ₛ Q → (∀ x, P → Q → Ψ x) → Ψ (y + 1) := by
  mintro HQ HΨ
  mspecialize HΨ (y + 1) hP HQ
  mexact HΨ
```
 -/
Lean.Parser.Tactic.mspecializePureError : Lean.ParserDescr
-- Mathlib.RingTheory.Ideal.Pointwise
Ideal.IsPrime.smul : ∀ {M : Type u_1} {R : Type u_3} [inst : Group M] [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R] {I : Ideal R}
  [H : I.IsPrime] (g : M), (g • I).IsPrime
-- Mathlib.Data.List.Intervals
List.Ico.filter_le_of_top_le : ∀ {n m l : ℕ}, m ≤ l → List.filter (fun x => decide (l ≤ x)) (List.Ico n m) = []
-- Mathlib.Geometry.Manifold.Immersion
Manifold.IsImmersionAtOfComplement.domChart_mem_maximalAtlas : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_7}
  [inst_7 : TopologicalSpace H] {G : Type u_9} [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H M]
  {N : Type u_13} [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  (h : Manifold.IsImmersionAtOfComplement F I J n f x), h.domChart ∈ IsManifold.maximalAtlas I n M
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.vanishingIdeal_empty : ∀ {R : Type u} [inst : CommSemiring R], PrimeSpectrum.vanishingIdeal ∅ = ⊤
-- Mathlib.Algebra.Order.Ring.Abs
pow_abs : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [IsOrderedRing α] (a : α) (n : ℕ), |a| ^ n = |a ^ n|
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
/-- The non-unital star algebra homomorphism underlying an instance of the continuous functional
calculus for non-unital algebras; a version for continuous functions on the quasispectrum.

In this case, the user must supply the fact that `a` satisfies the predicate `p`.

While `NonUnitalContinuousFunctionalCalculus` is stated in terms of these homomorphisms, in practice
the user should instead prefer `cfcₙ` over `cfcₙHom`.
 -/
cfcₙHom : {R : Type u_1} →
  {A : Type u_2} →
    {p : A → Prop} →
      [inst : CommSemiring R] →
        [inst_1 : Nontrivial R] →
          [inst_2 : StarRing R] →
            [inst_3 : MetricSpace R] →
              [inst_4 : IsTopologicalSemiring R] →
                [inst_5 : ContinuousStar R] →
                  [inst_6 : NonUnitalRing A] →
                    [inst_7 : StarRing A] →
                      [inst_8 : TopologicalSpace A] →
                        [inst_9 : Module R A] →
                          [inst_10 : IsScalarTower R A A] →
                            [inst_11 : SMulCommClass R A A] →
                              [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] →
                                {a : A} → p a → ContinuousMapZero (↑(quasispectrum R a)) R →⋆ₙₐ[R] A
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.mem_inter_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∈ t₁ ∩ t₂ ↔ k ∈ t₁ ∧ k ∈ t₂
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- **Fundamental theorem of calculus-2**: If `f : ℝ → E` is continuous on `[a, b]` (where `a ≤ b`)
and has a right derivative at `f' x` for all `x` in `(a, b)`, and `f'` is integrable on `[a, b]`,
then `∫ y in a..b, f' y` equals `f b - f a`.  -/
intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} [CompleteSpace E] {f f' : ℝ → E},
  a ≤ b →
    ContinuousOn f (Set.Icc a b) →
      (∀ x ∈ Set.Ioo a b, HasDerivWithinAt f (f' x) (Set.Ioi x) x) →
        IntervalIntegrable f' MeasureTheory.volume a b → ∫ (y : ℝ) in a..b, f' y = f b - f a
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.Hom.toAlgHom_comp_apply : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Generators R S ι) {R' : Type u_1} {S' : Type u_2} {ι' : Type u_3} [inst_3 : CommRing R']
  [inst_4 : CommRing S'] [inst_5 : Algebra R' S'] (P' : Algebra.Generators R' S' ι') {R'' : Type u_4} {S'' : Type u_5}
  {ι'' : Type u_6} [inst_6 : CommRing R''] [inst_7 : CommRing S''] [inst_8 : Algebra R'' S'']
  (P'' : Algebra.Generators R'' S'' ι'') [inst_9 : Algebra R R'] [inst_10 : Algebra R' R''] [inst_11 : Algebra R' S'']
  [inst_12 : Algebra S S'] [inst_13 : Algebra S' S''] [inst_14 : Algebra S S''] [inst_15 : Algebra R R'']
  [IsScalarTower R R' R''] [inst_17 : IsScalarTower R' R'' S''] [inst_18 : IsScalarTower R' S' S'']
  [inst_19 : IsScalarTower S S' S''] (f : P.Hom P') (g : P'.Hom P'') (x : P.Ring),
  (g.comp f).toAlgHom x = g.toAlgHom (f.toAlgHom x)
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.instDecidableEq.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : DecidableEq R] [inst_2 : DecidableEq M],
  MonoidAlgebra.instDecidableEq = MonoidAlgebra.coeffEquiv.decidableEq
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.Stmt.goto : {Γ : Type u_1} → {Λ : Type u_2} → {σ : Type u_3} → (Γ → σ → Λ) → Turing.TM1.Stmt Γ Λ σ
-- Init.Data.Vector.Attach
Vector.attachWith.congr_simp : ∀ {α : Type u_1} {n : ℕ} (xs xs_1 : Vector α n) (e_xs : xs = xs_1) (P : α → Prop) (H : ∀ x ∈ xs, P x),
  xs.attachWith P H = xs_1.attachWith P ⋯
-- Mathlib.Algebra.Order.GroupWithZero.Basic
mul_eq_mul_iff_eq_and_eq_of_pos' : ∀ {α : Type u_1} [inst : MulZeroClass α] {a b c d : α} [inst_1 : PartialOrder α] [PosMulStrictMono α]
  [MulPosStrictMono α], a ≤ b → c ≤ d → 0 < b → 0 < c → (a * c = b * d ↔ a = b ∧ c = d)
-- Mathlib.Algebra.Group.Defs
InvOneClass.inv_one : ∀ {G : Type u_2} [self : InvOneClass G], 1⁻¹ = 1
-- Mathlib.Algebra.DualQuaternion
Quaternion.fst_imK_dualNumberEquiv_symm : ∀ {R : Type u_1} [inst : CommRing R] (d : DualNumber (Quaternion R)),
  TrivSqZeroExt.fst (Quaternion.dualNumberEquiv.symm d).imK = (TrivSqZeroExt.fst d).imK
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.IsInitial.card_le_card : ∀ {a b : Ordinal.{u_1}}, a.IsInitial → (a.card ≤ b.card ↔ a ≤ b)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
AEMeasurable.edist : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α]
  [inst_3 : MeasurableSpace β] [SecondCountableTopology α] {f g : β → α} {μ : MeasureTheory.Measure β},
  AEMeasurable f μ → AEMeasurable g μ → AEMeasurable (fun a => edist (f a) (g a)) μ
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.coe_symm_toContinuousLinearEquiv : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂), ⇑(↑e).symm = ⇑e.symm
-- Mathlib.Order.Extension.Well
/-- An arbitrary well order on `α` that extends `r`.

The construction maps `r` into two well-orders: the first map is `IsWellFounded.rank`, which is not
necessarily injective but respects the order `r`; the other map is the identity (with an arbitrarily
chosen well-order on `α`), which is injective but doesn't respect `r`.

By taking the lexicographic product of the two, we get both properties, so we can pull it back and
get a well-order that extend our original order `r`. Another way to view this is that we choose an
arbitrary well-order to serve as a tiebreak between two elements of same rank.
 -/
IsWellFounded.wellOrderExtension : {α : Type u} → (r : α → α → Prop) → [IsWellFounded α r] → LinearOrder α
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.instAdd : {F : Type u} → [inst : Field F] → {W : WeierstrassCurve.Affine F} → [DecidableEq F] → Add W.Point
-- Mathlib.Analysis.Normed.Group.Basic
normAddGroupSeminorm.eq_1 : ∀ (E : Type u_5) [inst : SeminormedAddGroup E],
  normAddGroupSeminorm E = { toFun := norm, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯ }
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.traceSimpCall : Lean.Syntax → Lean.Meta.Simp.UsedSimps → Lean.MetaM Unit
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Free
PresheafOfModules.freeHomEquiv.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {F : CategoryTheory.Functor Cᵒᵖ (Type u)} {G : PresheafOfModules R},
  PresheafOfModules.freeHomEquiv =
    {
      toFun := fun ψ =>
        CategoryTheory.CategoryStruct.comp (PresheafOfModules.freeAdjunctionUnit R F)
          (CategoryTheory.Functor.whiskerRight ((PresheafOfModules.toPresheaf R).map ψ) (CategoryTheory.forget Ab)),
      invFun := fun φ => PresheafOfModules.freeObjDesc φ, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Topology.FiberBundle.Basic
FiberBundleCore.localTrivAsPartialEquiv_apply : ∀ {ι : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  (Z : FiberBundleCore ι B F) (i : ι) (p : Z.TotalSpace),
  ↑(Z.localTrivAsPartialEquiv i) p = (p.proj, Z.coordChange (Z.indexAt p.proj) i p.proj p.snd)
-- Mathlib.Algebra.Free
Magma.AssocQuotient.lift_symm_apply : ∀ {α : Type u} [inst : Mul α] {β : Type v} [inst_1 : Semigroup β] (f : Magma.AssocQuotient α →ₙ* β),
  Magma.AssocQuotient.lift.symm f = f.comp Magma.AssocQuotient.of
-- Mathlib.CategoryTheory.Sites.Over
/-- The Grothendieck topology on the category `Over X` for any `X : C` that is
induced by a Grothendieck topology on `C`.  -/
CategoryTheory.GrothendieckTopology.over : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.GrothendieckTopology C → (X : C) → CategoryTheory.GrothendieckTopology (CategoryTheory.Over X)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicone.binary_fan_snd_toCone : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} (c : CategoryTheory.Limits.BinaryBicone P Q), CategoryTheory.Limits.BinaryFan.snd c.toCone = c.snd
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.bot_ne_zero : ∀ {α : Type u} [inst : Zero α], ⊥ ≠ 0
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPMData : Lean.Options → Bool
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Projection
EuclideanGeometry.two_zsmul_oangle_orthogonalProjection_self : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)] (p : P)
  {p' : P} {s : AffineSubspace ℝ P} [inst_5 : s.direction.HasOrthogonalProjection],
  p ∉ s →
    ∀ (h : p' ∈ s),
      p' ≠ ↑((EuclideanGeometry.orthogonalProjection s) p) →
        2 • EuclideanGeometry.oangle p' (↑((EuclideanGeometry.orthogonalProjection s) p)) p = ↑Real.pi
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
/-- A functor is said to reflect finite limits, if it reflects all limits of shape `J`,
where `J : Type` is a finite category.
 -/
CategoryTheory.Limits.ReflectsFiniteLimits : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → Prop
-- Mathlib.NumberTheory.ADEInequality
ADEInequality.admissible_E'3 : ADEInequality.Admissible (ADEInequality.E' 3)
-- Lean.Data.PersistentHashSet
Lean.PersistentHashSet.find? : {α : Type u_1} → {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashSet α → α → Option α
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit_inverse_obj_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (A : CategoryTheory.AddMon C) {X Y : CategoryTheory.Discrete PUnit.{w + 1}} (x : X ⟶ Y),
  (CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit.inverse.obj A).map x = CategoryTheory.CategoryStruct.id A.X
-- Mathlib.RingTheory.Smooth.Kaehler
Algebra.Extension.H1Cotangent.map_toInfinitesimal_bijective : ∀ {R : Type u_1} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Extension R S), Function.Bijective ⇑(Algebra.Extension.H1Cotangent.map P.toInfinitesimal)
-- Mathlib.RingTheory.Spectrum.Prime.RingHom
/-- The pullback of an element of `PrimeSpectrum S` along a ring homomorphism `f : R →+* S`.
The bundled continuous version is `PrimeSpectrum.comap`.  -/
PrimeSpectrum.comap : {R : Type u_1} →
  {S : Type u_2} → [inst : CommSemiring R] → [inst_1 : CommSemiring S] → (R →+* S) → PrimeSpectrum S → PrimeSpectrum R
-- Mathlib.Topology.Algebra.Group.Torsor
ContinuousAt.vsub : ∀ {V : Type u_1} {P : Type u_2} {α : Type u_3} [inst : AddGroup V] [inst_1 : TopologicalSpace V]
  [inst_2 : AddTorsor V P] [inst_3 : TopologicalSpace P] [IsTopologicalAddTorsor P] [inst_5 : TopologicalSpace α]
  {f g : α → P} {x : α}, ContinuousAt f x → ContinuousAt g x → ContinuousAt (fun x => f x -ᵥ g x) x
-- Mathlib.RingTheory.Ideal.Quotient.Nilpotent
Ideal.Quotient.isUnit_mk_pow_iff_notMem : ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S) [I.IsMaximal] {n : ℕ},
  n ≠ 0 → ∀ {x : S}, IsUnit ((Ideal.Quotient.mk (I ^ n)) x) ↔ x ∉ I
-- Batteries.Recycling.RBTree.Basic
/-- `O(log n)`. Find an element in the tree, or return a default value `v₀`.  -/
RBTree.RBSet.findPD : {α : Type u_1} → {cmp : α → α → Ordering} → RBTree.RBSet α cmp → (α → Ordering) → α → α
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVBinPred.eq.sizeOf_spec : sizeOf Std.Tactic.BVDecide.BVBinPred.eq = 1
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.SubgoalsResult.instVal : Lean.Meta.SynthInstance.SubgoalsResult → Lean.Expr
-- Mathlib.InformationTheory.KullbackLeibler.Basic
InformationTheory.klDiv_zero_left : ∀ {α : Type u_1} {mα : MeasurableSpace α} {ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure ν],
  InformationTheory.klDiv 0 ν = ν Set.univ
-- Mathlib.AlgebraicGeometry.Pullbacks
/-- The composition of the inverse of the isomorphism `pullbackSpecIso R S T` (from the pullback of
`Spec S ⟶ Spec R` and `Spec T ⟶ Spec R` to `Spec (S ⊗[R] T)`) with the second projection is
the morphism `Spec (S ⊗[R] T) ⟶ Spec T` obtained by applying `Spec.map` to the ring morphism
`t ↦ 1 ⊗ₜ[R] t`.
 -/
AlgebraicGeometry.pullbackSpecIso_inv_snd_assoc : ∀ (R S T : Type u) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
  [inst_4 : Algebra R T] {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (CommRingCat.of T) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackSpecIso R S T).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)))
          (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R T))))
        h) =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑Algebra.TensorProduct.includeRight)) h
-- Mathlib.Data.Finset.SDiff
Finset.sdiff_subset_sdiff_iff_subset : ∀ {α : Type u_1} [inst : DecidableEq α] {s t r : Finset α}, s ⊆ r → t ⊆ r → (r \ s ⊆ r \ t ↔ t ⊆ s)
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.instMulAction : (p : ENNReal) → (K : Type u_1) → (V : Type u_4) → [inst : Monoid K] → [MulAction K V] → MulAction K (WithLp p V)
-- Mathlib.Data.List.Rotate
List.head?_rotate : ∀ {α : Type u} {l : List α} {n : ℕ}, n < l.length → (l.rotate n).head? = l[n]?
-- Mathlib.Analysis.Calculus.ContDiff.Defs
/-- On a set with unique differentiability, an analytic function is automatically `C^ω`, as its
successive derivatives are also analytic. This does not require completeness of the space. See
also `AnalyticOnNhd.contDiffOn_of_completeSpace`.  -/
AnalyticOnNhd.contDiffOn : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {n : WithTop ℕ∞}, AnalyticOnNhd 𝕜 f s → UniqueDiffOn 𝕜 s → ContDiffOn 𝕜 n f s
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- the second component of `f : Hom x y` is a morphism `x.snd ⟶ y.snd`  -/
CategoryTheory.Limits.CategoricalPullback.Hom.snd : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor A B} →
              {G : CategoryTheory.Functor C B} →
                {x y : CategoryTheory.Limits.CategoricalPullback F G} → x.Hom y → (x.snd ⟶ y.snd)
-- Mathlib.Algebra.Lie.AdjointAction.Derivation
/-- If the center of a Lie algebra is trivial, then the adjoint action is injective.  -/
LieDerivation.injective_ad_of_center_eq_bot : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  LieAlgebra.center R L = ⊥ → Function.Injective ⇑(LieDerivation.ad R L)
-- Mathlib.Topology.Algebra.Valued.WithVal
/-- The completion of a field with respect to a valuation.  -/
Valuation.Completion : {Γ₀ : Type u_2} →
  [inst : LinearOrderedCommGroupWithZero Γ₀] → {R : Type u_3} → [inst_1 : Ring R] → Valuation R Γ₀ → Type u_3
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.WalkingPair.ofNat_ctorIdx : ∀ (x : CategoryTheory.Limits.WalkingPair), CategoryTheory.Limits.WalkingPair.ofNat x.ctorIdx = x
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.mk_inv : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Inv G] [inst_2 : ContinuousInv G] (x : G),
  SeparationQuotient.mk x⁻¹ = (SeparationQuotient.mk x)⁻¹
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.instNonemptyRingCompute : ∀ (u : Lean.Level) (α : Q(Type u)) (BaseType : Q(«$α») → Type) [∀ (e : Q(«$α»)), Nonempty (BaseType e)]
  (sα : Q(CommSemiring «$α»)), Nonempty (Mathlib.Tactic.Ring.Common.RingCompute BaseType sα)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_int_mul_pi : ∀ (n : ℤ), Real.sin (↑n * Real.pi) = 0
-- Lean.Meta.Tactic.Grind.Proof
/-- Constructs a congruence proof for `lhs` and `rhs`.  -/
_private.Lean.Meta.Tactic.Grind.Proof.0.Lean.Meta.Grind.mkCongrProof : Lean.Expr → Lean.Expr → Bool → Lean.Meta.Grind.GoalM Lean.Expr
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
/-- For a signed measure, the variation is realized by the norm of the measure of a single set, up
to a factor of `2` and an arbitrarily small error.  -/
MeasureTheory.SignedMeasure.exists_subset_lt_enorm_apply_of_lt_variation : ∀ {X : Type u_1} {mX : MeasurableSpace X} (μ : MeasureTheory.SignedMeasure X) {s : Set X},
  MeasurableSet s →
    ∀ {a : ENNReal}, a < (MeasureTheory.VectorMeasure.variation μ) s → ∃ t ⊆ s, MeasurableSet t ∧ a < 2 * ‖μ t‖ₑ
-- Mathlib.Data.Matrix.Mul
dotProduct_neg : ∀ {m : Type u_2} {α : Type v} [inst : Fintype m] [inst_1 : NonUnitalNonAssocRing α] (v w : m → α), v ⬝ᵥ -w = -(v ⬝ᵥ w)
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
ContinuousLinearMap.uncurryMid_apply : ∀ {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)] [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)]
  [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] (p : Fin (n + 1))
  (f : Ei p →L[𝕜] Ei (p.succAbove i) [×n]→L[𝕜] G) (m : (i : Fin n.succ) → Ei i),
  (ContinuousLinearMap.uncurryMid p f) m = (f (m p)) (p.removeNth m)
-- Mathlib.Order.RelClasses
instAsymmGt : ∀ {α : Type u} [inst : Preorder α], Std.Asymm fun x1 x2 => x2 < x1
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.Equiv.trans_symm : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} (φ : ρ.Equiv σ),
  φ.trans φ.symm = ContRepresentation.Equiv.refl ρ
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get?_inter_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {k : α}, k ∉ t₁ → Std.DTreeMap.Const.get? (t₁ ∩ t₂) k = none