mathlib-initiative/mathlib-types huggingface dataset:
-- Aesop.Script.TacticState
Aesop.Script.TacticState.mk.injEq : ∀ (visibleGoals : Array Aesop.GoalWithMVars) (invisibleGoals : Std.HashSet Lean.MVarId)
  (visibleGoals_1 : Array Aesop.GoalWithMVars) (invisibleGoals_1 : Std.HashSet Lean.MVarId),
  ({ visibleGoals := visibleGoals, invisibleGoals := invisibleGoals } =
      { visibleGoals := visibleGoals_1, invisibleGoals := invisibleGoals_1 }) =
    (visibleGoals = visibleGoals_1 ∧ invisibleGoals = invisibleGoals_1)
-- Batteries.Tactic.Congr
Batteries.Tactic.Congr.Config.mk.sizeOf_spec : ∀ (closePre closePost : Bool),
  sizeOf { closePre := closePre, closePost := closePost } = 1 + sizeOf closePre + sizeOf closePost
-- Mathlib.Order.Filter.IsBounded
Filter.isBoundedUnder_le_add : ∀ {α : Type u_5} {f : Filter α} {R : Type u_6} [inst : Preorder R] [inst_1 : Add R] [AddLeftMono R] [AddRightMono R]
  {u v : α → R},
  Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u →
    Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v → Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f (u + v)
-- Lean.MetavarContext
Lean.MetavarContext.MkBindingM.Context.lctx : Lean.MetavarContext.MkBindingM.Context → Lean.LocalContext
-- Mathlib.RingTheory.RegularLocalRing.Defs
IsRegularLocalRing.of_ringEquiv : ∀ {R : Type u_1} [inst : CommRing R] [IsRegularLocalRing R] {R' : Type u_2} [inst_2 : CommRing R'] (e : R ≃+* R'),
  IsRegularLocalRing R'
-- Mathlib.Algebra.Group.Submonoid.Pointwise
AddSubmonoid.neg_inf : ∀ {G : Type u_2} [inst : AddGroup G] (S T : AddSubmonoid G), -(S ⊓ T) = -S ⊓ -T
-- Mathlib.Algebra.Category.Ring.Adjunctions
CommRingCat.instIsRightAdjointForgetRingHomCarrier : (CategoryTheory.forget CommRingCat).IsRightAdjoint
-- Mathlib.Tactic.FieldSimp
/-- Given `e₁` and `e₂`, cancel nonzero factors to construct a new equality which is logically
equivalent to `e₁ = e₂`.  -/
Mathlib.Tactic.FieldSimp.reduceEqQ : {v : Lean.Level} →
  {M : Q(Type v)} →
    ({u : Lean.Level} → (type : Q(Sort u)) → Lean.MetaM Q(«$type»)) →
      Q(CommGroupWithZero «$M») →
        (e₁ e₂ : Q(«$M»)) →
          Mathlib.Tactic.AtomM ((f₁ : Q(«$M»)) × (f₂ : Q(«$M»)) × Q((«$e₁» = «$e₂») = («$f₁» = «$f₂»)))
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.isZero_of_isGE : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : CochainComplex C ℤ) (n i : ℤ),
  autoParam (i < n) CochainComplex.isZero_of_isGE._auto_1 →
    ∀ [K.IsGE n] [inst_3 : HomologicalComplex.HasHomology K i],
      CategoryTheory.Limits.IsZero (HomologicalComplex.homology K i)
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.instIsOverHomOfVectorOverSchemeInferInstanceOverClass : ∀ {n : Type u} (S : AlgebraicGeometry.Scheme) {X : AlgebraicGeometry.Scheme} [inst : X.Over S]
  (v : n → ↑(X.presheaf.obj (Opposite.op ⊤))),
  AlgebraicGeometry.Scheme.Hom.IsOver (AlgebraicGeometry.AffineSpace.homOfVector (X ↘ S) v) S
-- Mathlib.NumberTheory.Height.Basic
Height.zero_le_logHeight₁ : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] (x : K), 0 ≤ Height.logHeight₁ x
-- Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
/-- `f : X ⟶ S` is formally unramified if `X ⟶ X ×ₛ X` is an open immersion.
In particular, monomorphisms (e.g. immersions) are formally unramified.
The converse is true if `f` is locally of finite type.  -/
AlgebraicGeometry.FormallyUnramified.instOfIsOpenImmersionDiagonalScheme : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y)
  [AlgebraicGeometry.IsOpenImmersion (CategoryTheory.Limits.pullback.diagonal f)],
  AlgebraicGeometry.FormallyUnramified f
-- Lean.Server.GoTo
/-- Checks whether `ti1` is an instance projection info that subsumes `ti2`.  -/
Lean.Server.isInstanceProjectionInfoFor : Lean.Server.GoToKind → Lean.Elab.TermInfo → Lean.Elab.TermInfo → Lean.MetaM Bool
-- Mathlib.RingTheory.RamificationInertia.Inertia
Ideal.inertiaDeg_eq_of_isMaximal : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  (q : Ideal S) [inst_3 : q.LiesOver p] [p.IsMaximal] [q.IsMaximal], q.inertiaDeg R = Module.finrank (R ⧸ p) (S ⧸ q)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_filter!_key_eq_size_iff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] {f : α → Bool},
  t.WF →
    ((Std.DTreeMap.Internal.Impl.filter! (fun k x => f k) t).size = t.size ↔
      ∀ (k : α) (h : Std.DTreeMap.Internal.Impl.contains k t = true), f (t.getKey k h) = true)
-- Init.Prelude
/-- A reader monad that additionally allows the value to be locally overridden.

In this class, `ρ` is a `semiOutParam`, which means that it can influence the choice of instance.
`MonadWithReader ρ` provides the same operations, but requires that `ρ` be inferable from `m`.
 -/
MonadWithReaderOf : semiOutParam (Type u) → (Type u → Type v) → Type (max (u + 1) v)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.walkingParallelPairOpEquiv_inverse : CategoryTheory.Limits.walkingParallelPairOpEquiv.inverse = CategoryTheory.Limits.walkingParallelPairOp.leftOp
-- Mathlib.Analysis.Convex.Between
/-- The point `y` is weakly between `x` and `z`.  -/
Wbtw : (R : Type u_1) →
  {V : Type u_2} →
    {P : Type u_4} →
      [inst : Ring R] → [PartialOrder R] → [inst_2 : AddCommGroup V] → [Module R V] → [AddTorsor V P] → P → P → P → Prop
-- Lean.Elab.Match
Lean.Elab.Term.GeneralizeResult.matchType : Lean.Elab.Term.GeneralizeResult → Lean.Expr
-- Init.Prelude
MonadExcept.instOrElse : {ε : Type u} → {m : Type v → Type w} → [MonadExcept ε m] → {α : Type v} → OrElse (m α)
-- Mathlib.Analysis.MellinInversion
_private.Mathlib.Analysis.MellinInversion.0.rexp_neg_deriv_aux : ∀ x ∈ Set.univ, HasDerivWithinAt (Real.exp ∘ Neg.neg) (-Real.exp (-x)) Set.univ x
-- Lean.Meta.Tactic.Grind.Theorems
Lean.Meta.Grind.TheoremsArray.retrieve? : {α : Type} → Lean.Meta.Grind.TheoremsArray α → Lean.Name → Option (List α × Lean.Meta.Grind.TheoremsArray α)
-- Mathlib.Topology.Category.Stonean.Basic
Stonean.instExtremallyDisconnectedCarrierToTop : ∀ (X : Stonean), ExtremallyDisconnected ↑X.toTop
-- Mathlib.Topology.NhdsSet
mem_nhdsSet_interior : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s : Set X}, s ∈ nhdsSet (interior s)
-- Mathlib.Algebra.BigOperators.ModEq
Nat.ModEq.listProd_map : ∀ {α : Type u_1} {n : ℕ} {l : List α} {f g : α → ℕ},
  (∀ x ∈ l, f x ≡ g x [MOD n]) → (List.map f l).prod ≡ (List.map g l).prod [MOD n]
-- Aesop.Stats.Basic
Aesop.instInhabitedForwardInstantiationStats.default : Aesop.ForwardInstantiationStats
-- Std.Time.Zoned.Database.TzIf
_private.Std.Time.Zoned.Database.TzIf.0.Std.Time.TimeZone.TZif.manyN : {α : Type} → ℕ → Std.Internal.Parsec.ByteArray.Parser α → Std.Internal.Parsec.ByteArray.Parser (Array α)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.contains_diff : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, (m₁ \ m₂).contains k = (m₁.contains k && !m₂.contains k)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonCallHierarchyIncomingCallsParams.fromJson : Lean.Json → Except String Lean.Lsp.CallHierarchyIncomingCallsParams
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.insertManyIfNewUnit_ind : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {ρ : Type w} [inst : ForIn Id ρ α] [inst_1 : EquivBEq α]
  [inst_2 : LawfulHashable α] {motive : Std.ExtHashMap α Unit → Prop} (m : Std.ExtHashMap α Unit) (l : ρ),
  motive m →
    (∀ (m : Std.ExtHashMap α Unit) (a : α), motive m → motive (m.insertIfNew a ())) → motive (m.insertManyIfNewUnit l)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.zpow_le_iff_le_log : ∀ {x y : ℝ} {n : ℤ}, 0 < x → 0 < y → (x ^ n ≤ y ↔ ↑n * Real.log x ≤ Real.log y)
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
/-- The external product of edges of `2`-truncated simplicial sets.  -/
SSet.Truncated.Edge.tensor : {X Y : SSet.Truncated 2} →
  {x x' : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })} →
    SSet.Truncated.Edge x x' →
      {y y' : Y.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })} →
        SSet.Truncated.Edge y y' → SSet.Truncated.Edge (x, y) (x', y')
-- Mathlib.Algebra.Group.Ext
Monoid.ext_iff : ∀ {M : Type u} {m₁ m₂ : Monoid M}, m₁ = m₂ ↔ HMul.hMul = HMul.hMul
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.id_mapComp : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  (CategoryTheory.Pseudofunctor.id B).mapComp f g = CategoryTheory.Iso.refl (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Analysis.InnerProductSpace.Laplacian
/-- The Laplacian commutes with scalar multiplication.  -/
InnerProductSpace.laplacian_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAlgebra ℝ 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : InnerProductSpace ℝ E] [inst_4 : FiniteDimensional ℝ E] {F : Type u_3}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace ℝ F] [inst_7 : NormedSpace 𝕜 F] [IsScalarTower ℝ 𝕜 F]
  {f : E → F} {x : E} (v : 𝕜), ContDiffAt ℝ 2 f x → Laplacian.laplacian (v • f) x = v • Laplacian.laplacian f x
-- Mathlib.MeasureTheory.Integral.CircleAverage
/-- The circle average of a constant function equals the constant.
 -/
Real.circleAverage_const : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] (a : E) (c : ℂ) (R : ℝ),
  Real.circleAverage (fun x => a) c R = a
-- Mathlib.Algebra.Group.Action.Basic
smul_left_cancel : ∀ {α : Type u_5} {β : Type u_6} [inst : Group α] [inst_1 : MulAction α β] (g : α) {x y : β}, g • x = g • y → x = y
-- Mathlib.Topology.GDelta.Basic
/-- A subset of a nowhere dense set is nowhere dense.  -/
IsNowhereDense.mono : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X}, t ⊆ s → IsNowhereDense s → IsNowhereDense t
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.mul_add : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (φ₁ φ₂ φ₃ : MvPowerSeries σ R), φ₁ * (φ₂ + φ₃) = φ₁ * φ₂ + φ₁ * φ₃
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
/-- Extend a function `f : α → ℚ → ℝ` with property `IsMeasurableRatCDF` from `ℚ` to `ℝ`,
to a function `α → StieltjesFunction ℝ`.  -/
ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunction : {α : Type u_1} →
  {f : α → ℚ → ℝ} → [inst : MeasurableSpace α] → ProbabilityTheory.IsMeasurableRatCDF f → α → StieltjesFunction ℝ
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.rnDeriv_lt_top : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ η : ProbabilityTheory.Kernel α γ)
  [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] {a : α},
  ∀ᵐ (x : γ) ∂η a, κ.rnDeriv η a x < ⊤
-- Init.PropLemmas
Decidable.or_congr_right' : ∀ {a b c : Prop} [Decidable a], (¬a → (b ↔ c)) → (a ∨ b ↔ a ∨ c)
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.instExpChar : ∀ {K : Type u} [inst : Field K] {p : ℕ} [ExpChar K p], ExpChar (RatFunc K) p
-- Mathlib.Topology.Order.LocalExtr
/-- `IsLocalExtrOn f s a` means `IsLocalMinOn f s a ∨ IsLocalMaxOn f s a`.  -/
IsLocalExtrOn : {α : Type u} → {β : Type v} → [TopologicalSpace α] → [Preorder β] → (α → β) → Set α → α → Prop
-- Mathlib.Computability.TuringMachine.Computable
/-- A forgetful map, forgetting the time bound on the number of steps.  -/
Turing.TM2ComputableInTime.toTM2Computable : {α β αΓ βΓ : Type} →
  {ea : α → List αΓ} →
    {eb : β → List βΓ} → {f : α → β} → Turing.TM2ComputableInTime ea eb f → Turing.TM2Computable ea eb f
-- Mathlib.Data.Stream.Defs
/-- Get the `n`-th element of a stream.  -/
Stream'.get : {α : Type u} → Stream' α → ℕ → α
-- Mathlib.MeasureTheory.Measure.Hausdorff
/-- To bound the Hausdorff measure (or, more generally, for a measure defined using
`MeasureTheory.Measure.mkMetric`) of a set, one may use coverings with maximum diameter tending to
`0`, indexed by any sequence of finite types.  -/
MeasureTheory.Measure.mkMetric_le_liminf_sum : ∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] {β : Type u_4}
  {ι : β → Type u_5} [hι : (n : β) → Fintype (ι n)] (s : Set X) {l : Filter β} (r : β → ENNReal),
  Filter.Tendsto r l (nhds 0) →
    ∀ (t : (n : β) → ι n → Set X),
      (∀ᶠ (n : β) in l, ∀ (i : ι n), Metric.ediam (t n i) ≤ r n) →
        (∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i) →
          ∀ (m : ENNReal → ENNReal),
            (MeasureTheory.Measure.mkMetric m) s ≤ Filter.liminf (fun n => ∑ i, m (Metric.ediam (t n i))) l
-- Mathlib.LinearAlgebra.DFinsupp
AddMonoidHom.mker.congr_simp : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] (f f_1 : F),
  f = f_1 → AddMonoidHom.mker f = AddMonoidHom.mker f_1
-- Batteries.Data.Float.Lemmas
Float.Model.UnpackedFloat.packComponents_unpackSign_unpackExponent_unpackMantissa : ∀ {spec : Float.Model.Format} (b : BitVec spec.numBits),
  Float.Model.UnpackedFloat.packComponents spec
      (Float.Model.UnpackedFloat.Sign.ofBitVec (Float.Model.UnpackedFloat.unpackSign b))
      (Float.Model.UnpackedFloat.unpackExponent b) (Float.Model.UnpackedFloat.unpackMantissa b) =
    b
-- Mathlib.Algebra.Homology.HomologySequence
HomologicalComplex.pOpcycles_opcyclesToCycles_iCycles_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι)
  [inst_2 : K.HasHomology i] [inst_3 : K.HasHomology j] {Z : C} (h : K.X j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.pOpcycles i)
      (CategoryTheory.CategoryStruct.comp (K.opcyclesToCycles i j)
        (CategoryTheory.CategoryStruct.comp (K.iCycles j) h)) =
    CategoryTheory.CategoryStruct.comp (K.d i j) h
-- Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
ProbabilityTheory.IsGaussianProcess.hasGaussianLaw_add : ∀ {T : Type u_2} {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : T → Ω → E}
  [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [BorelSpace E] [inst_3 : NormedSpace ℝ E]
  [SecondCountableTopology E],
  ProbabilityTheory.IsGaussianProcess X P → ∀ {s t : T}, ProbabilityTheory.HasGaussianLaw (X s + X t) P
-- Init.Data.Dyadic.Basic
Dyadic.instLE : LE Dyadic
-- Mathlib.Geometry.Manifold.Riemannian.PathELength
Manifold.pathELength_eq_lintegral_mfderiv_Ioo : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : (x : M) → ENorm (TangentSpace I x)] {a b : ℝ} {γ : ℝ → M},
  Manifold.pathELength I γ a b = ∫⁻ (t : ℝ) in Set.Ioo a b, ‖(mfderiv% γ t) 1‖ₑ
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.swapLeft_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel (α × β) γ) (a : β × α), κ.swapLeft a = κ a.swap
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.mapTriangleCommShiftIso_inv_app_hom₃ : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ]
  [inst_5 : CategoryTheory.Preadditive C] [inst_6 : CategoryTheory.Preadditive D] [inst_7 : F.Additive] (n : ℤ)
  (X : CategoryTheory.Pretriangulated.Triangle C),
  ((F.mapTriangleCommShiftIso n).inv.app X).hom₃ = (CategoryTheory.Functor.commShiftIso F n).inv.app X.obj₃
-- Mathlib.Topology.MetricSpace.IsometricSMul
Metric.smul_closedBall : ∀ {G : Type v} {X : Type w} [inst : PseudoMetricSpace X] [inst_1 : Group G] [inst_2 : MulAction G X]
  [IsIsometricSMul G X] (c : G) (x : X) (r : ℝ), c • Metric.closedBall x r = Metric.closedBall (c • x) r
-- Std.Data.TreeSet.Raw.Basic
Std.TreeSet.Raw.instInsert : {α : Type u} → {cmp : α → α → Ordering} → Insert α (Std.TreeSet.Raw α cmp)
-- Mathlib.Topology.Filter
Filter.isInducing_nhds : ∀ {X : Type u_4} [inst : TopologicalSpace X], Topology.IsInducing nhds
-- Init.Data.SInt.Lemmas
Int64.ofNat_mod : ∀ {a b : ℕ}, a < 2 ^ 63 → b < 2 ^ 63 → Int64.ofNat (a % b) = Int64.ofNat a % Int64.ofNat b
-- Mathlib.Data.Nat.Choose.Factorization
/-- Primes greater than about `2 * n / 3` and less than `n` do not appear in the factorization of
`centralBinom n`.  -/
Nat.factorization_centralBinom_of_two_mul_self_lt_three_mul : ∀ {p n : ℕ}, 2 < n → p ≤ n → 2 * n < 3 * p → n.centralBinom.factorization p = 0
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
/-- The image of a set `s` under a continuous linear map `f` has measure
equal to `μ s` times the absolute value of the determinant of `f`.  -/
MeasureTheory.Measure.addHaar_image_continuousLinearMap : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (f : E →L[ℝ] E) (s : Set E),
  μ (⇑f '' s) = ENNReal.ofReal |LinearMap.det ↑f| * μ s
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.inftyStarRing : {I : Type u_5} →
  {B : I → Type u_6} →
    [inst : (i : I) → NonUnitalNormedRing (B i)] →
      [inst_1 : (i : I) → StarRing (B i)] → [∀ (i : I), NormedStarGroup (B i)] → StarRing ↥(lp B ⊤)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙ_predicate : ∀ {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] (f : R → R) (a : A),
  p (cfcₙ f a)
-- Mathlib.Data.Set.Piecewise
Set.EqOn.piecewise_ite' : ∀ {α : Type u_1} {β : Type u_2} (s : Set α) [inst : (j : α) → Decidable (j ∈ s)] {f f' g : α → β} {t t' : Set α},
  Set.EqOn f g (t ∩ s) → Set.EqOn f' g (t' ∩ sᶜ) → Set.EqOn (s.piecewise f f') g (s.ite t t')
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
HasDerivAt.ccos : ∀ {f : ℂ → ℂ} {f' x : ℂ}, HasDerivAt f f' x → HasDerivAt (fun x => Complex.cos (f x)) (-Complex.sin (f x) * f') x
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKey?_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {v : β k},
      (t.insertIfNew k v).minKey? = some (t.minKey?.elim k fun k' => if cmp k k' = Ordering.lt then k else k')
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyMapData.ofIsLimitKernelFork_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (hf₁ : S₁.f = 0) (c₁ : CategoryTheory.Limits.KernelFork S₁.g)
  (hc₁ : CategoryTheory.Limits.IsLimit c₁) (hf₂ : S₂.f = 0) (c₂ : CategoryTheory.Limits.KernelFork S₂.g)
  (hc₂ : CategoryTheory.Limits.IsLimit c₂) (f : c₁.pt ⟶ c₂.pt)
  (comm :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι c₁) φ.τ₂ =
      CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.Fork.ι c₂)),
  (CategoryTheory.ShortComplex.HomologyMapData.ofIsLimitKernelFork φ hf₁ c₁ hc₁ hf₂ c₂ hc₂ f comm).right =
    CategoryTheory.ShortComplex.RightHomologyMapData.ofIsLimitKernelFork φ hf₁ c₁ hc₁ hf₂ c₂ hc₂ f comm
-- Lean.Elab.Tactic.Grind.Main
Lean.Elab.Tactic.evalGrindTraceCore : Lean.Syntax →
  optParam Bool true → optParam Bool true → optParam Bool true → Lean.Elab.Tactic.TacticM (Array (Lean.TSyntax `tactic))
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.derivWeierstrassP_zero : ∀ (L : PeriodPair), L.derivWeierstrassP 0 = 0
-- Lean.Elab.DocString
/-- A value paired with the syntax it is derived from.

This can be used to provide hints and code actions.
 -/
Lean.Doc.WithSyntax : Type u → Type u
-- Mathlib.Algebra.Group.Pointwise.Finset.BigOperators
Finset.coe_prod : ∀ {α : Type u_1} {ι : Type u_2} [inst : CommMonoid α] [inst_1 : DecidableEq α] (s : Finset ι) (f : ι → Finset α),
  ↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.kernelComparison.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (G : CategoryTheory.Functor C D)
  [inst_4 : G.PreservesZeroMorphisms] [inst_5 : CategoryTheory.Limits.HasKernel f]
  [inst_6 : CategoryTheory.Limits.HasKernel (G.map f)],
  CategoryTheory.Limits.kernelComparison f G = CategoryTheory.Limits.kernelComparison f G
-- Mathlib.Analysis.Calculus.VectorField
/-- The Lie bracket `[V, W] (x)` of two vector fields within a set at a point, defined as
`DW(x) (V x) - DV(x) (W x)` where the derivatives are taken inside `s`.  -/
VectorField.lieBracketWithin : (𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} → [inst_1 : NormedAddCommGroup E] → [NormedSpace 𝕜 E] → (E → E) → (E → E) → Set E → E → E
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.step_mapM : ∀ {α β γ : Type w} [inst : Std.Iterator α Id β] {it : Std.Iter β} {n : Type w → Type w''} {f : β → n γ}
  [inst_1 : Monad n] [inst_2 : MonadAttach n] [LawfulMonad n],
  (Std.Iter.mapM f it).step =
    match it.step with
    | ⟨Std.IterStep.yield it' out, h⟩ => do
      let out' ← MonadAttach.attach (f out)
      pure (Std.Shrink.deflate (Std.PlausibleIterStep.yield (Std.Iter.mapM f it') ↑out' ⋯))
    | ⟨Std.IterStep.skip it', h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.Iter.mapM f it') ⋯))
    | ⟨Std.IterStep.done, h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.done ⋯))
-- Mathlib.Analysis.InnerProductSpace.Defs
/-- Normed space core structure constructed from an `InnerProductSpace.Core` structure  -/
InnerProductSpace.Core.toNormedSpaceCore : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  (cd : InnerProductSpace.Core 𝕜 F), NormedSpace.Core 𝕜 F
-- Mathlib.ModelTheory.Order
FirstOrder.Language.realize_noBotOrder : ∀ (L : FirstOrder.Language) (M : Type w') [inst : L.IsOrdered] [inst_1 : L.Structure M] [inst_2 : LE M]
  [L.OrderedStructure M] [h : NoBotOrder M], M ⊨ L.noBotOrderSentence
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.darts_eq_nil : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w}, p.darts = [] ↔ p.Nil
-- Mathlib.Analysis.Calculus.BumpFunction.Normed
ContDiffBump.integrable_normed : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E]
  [inst_3 : MeasurableSpace E] {c : E} (f : ContDiffBump c) {μ : MeasureTheory.Measure E} [BorelSpace E]
  [FiniteDimensional ℝ E] [MeasureTheory.IsLocallyFiniteMeasure μ], MeasureTheory.Integrable (f.normed μ) μ
-- Mathlib.Analysis.Normed.Group.Bounded
tendsto_norm_comp_cofinite_atTop_of_isClosedEmbedding : ∀ {E : Type u_2} [inst : SeminormedAddGroup E] {X : Type u_5} [inst_1 : TopologicalSpace X] [DiscreteTopology X]
  [ProperSpace E] {e : X → E}, Topology.IsClosedEmbedding e → Filter.Tendsto (norm ∘ e) Filter.cofinite Filter.atTop
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.EmbeddedG2.pairingIn_shortAddLong_right : ∀ {ι : 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)
  [inst_5 : P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R] (i : ι),
  P.pairingIn ℤ i (RootPairing.EmbeddedG2.shortAddLong P) =
    P.pairingIn ℤ i (RootPairing.EmbeddedG2.short P) + 3 * P.pairingIn ℤ i (RootPairing.EmbeddedG2.long P)