mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.BaseChange
_private.Mathlib.Algebra.Lie.BaseChange.0.LieAlgebra.ExtendScalars.bracket_leibniz_lie : ∀ (R : Type u_1) (A : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A] [inst_3 : LieRing L] [inst_4 : LieAlgebra R L] [inst_5 : AddCommGroup M] [inst_6 : Module R M]
  [inst_7 : LieRingModule L M] [inst_8 : LieModule R L M] (x y : TensorProduct R A L) (z : TensorProduct R A M),
  ⁅x, ⁅y, z⁆⁆ = ⁅⁅x, y⁆, z⁆ + ⁅y, ⁅x, z⁆⁆
-- Mathlib.Analysis.MellinInversion
_private.Mathlib.Analysis.MellinInversion.0.rexp_cexp_aux : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (x : ℝ) (s : ℂ) (f : E),
  Real.exp (-x) • Complex.exp (-↑x) ^ (s - 1) • f = Complex.exp (-s * ↑x) • f
-- Mathlib.Order.Interval.Set.Basic
Set.nonempty_Ici : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, (Set.Ici a).Nonempty
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.Measure.restrict_toMeasurable_of_sFinite : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] (s : Set α),
  μ.restrict (MeasureTheory.toMeasurable μ s) = μ.restrict s
-- Init.Data.UInt.Lemmas
UInt8.pos_iff_ne_zero : ∀ {a : UInt8}, 0 < a ↔ a ≠ 0
-- Mathlib.Tactic.NormNum.RealSqrt
Mathlib.Meta.NormNum.isNNRat_realSqrt_of_isNNRat : ∀ {x : ℝ} {n sn d sd : ℕ},
  sn * sn = n → sd * sd = d → Mathlib.Meta.NormNum.IsNNRat x n d → Mathlib.Meta.NormNum.IsNNRat (√x) sn sd
-- Mathlib.Tactic.GCongr.Core
/-- Patterns to use when doing intro.  -/
Mathlib.Tactic.GCongr.State.patterns : Mathlib.Tactic.GCongr.State → List (Lean.TSyntax `rintroPat)
-- Lean.Meta.Injective
_private.Lean.Meta.Injective.0.Lean.Meta.mkInjectiveEqTheoremType? : Lean.ConstructorVal → Lean.MetaM (Option Lean.Expr)
-- Mathlib.Analysis.Distribution.DerivNotation
LineDeriv.iteratedLineDerivOp_succ_left : ∀ {V : Type u_11} {E : Type u_12} [inst : LineDeriv V E E] {n : ℕ} (m : Fin (n + 1) → V) (f : E),
  LineDeriv.iteratedLineDerivOp m f = LineDeriv.lineDerivOp (m 0) (LineDeriv.iteratedLineDerivOp (Fin.tail m) f)
-- Mathlib.Analysis.SpecialFunctions.Complex.Analytic
AnalyticWithinAt.log : ∀ {f : ℝ → ℝ} {s : Set ℝ} {x : ℝ}, AnalyticWithinAt ℝ f s x → 0 < f x → AnalyticWithinAt ℝ (fun z => Real.log (f z)) s x
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
/-- The Zariski topology on the prime spectrum of a commutative ring is defined via the closed sets
of the topology: they are exactly those sets that are the zero locus of a subset of the ring.  -/
ProjectiveSpectrum.zariskiTopology : {A : Type u_1} →
  {σ : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubmonoidClass σ A] →
          (𝒜 : ℕ → σ) → [inst_3 : GradedRing 𝒜] → TopologicalSpace (ProjectiveSpectrum 𝒜)
-- Lean.Parser.Basic
Lean.Parser.tokenFn : optParam (List String) [] → Lean.Parser.ParserFn
-- Mathlib.MeasureTheory.Measure.Haar.Extension
TopologicalGroup.IsSES.integrate_mono : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : Group A] [inst_1 : Group B] [inst_2 : Group C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] {φ : A →* B} {ψ : B →* C}
  (H : TopologicalGroup.IsSES φ ψ) [inst_6 : IsTopologicalGroup A] [inst_7 : IsTopologicalGroup B]
  [inst_8 : MeasurableSpace A] [inst_9 : BorelSpace A] (μA : MeasureTheory.Measure A) [hμA : μA.IsHaarMeasure]
  [inst_10 : IsTopologicalGroup C] [inst_11 : LocallyCompactSpace B] [inst_12 : MeasurableSpace C]
  [inst_13 : BorelSpace C] (μC : MeasureTheory.Measure C) [hμC : μC.IsHaarMeasure]
  {f g : CompactlySupportedContinuousMap B ℝ}, f ≤ g → (H.integrate μA μC) f ≤ (H.integrate μA μC) g
-- Mathlib.Topology.Connected.Basic
IsConnected.preimage_of_isClosedMap : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : Set β},
  IsConnected s → ∀ {f : α → β}, Function.Injective f → IsClosedMap f → s ⊆ Set.range f → IsConnected (f ⁻¹' s)
-- Mathlib.Analysis.Distribution.TestFunction
ContDiffMapSupportedIn.integralAgainstBilinCLM.congr_simp : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {n : ℕ∞} {K : TopologicalSpace.Compacts E} {m : MeasurableSpace E}
  [inst_3 : OpensMeasurableSpace E] {F₁ : Type u_5} {F₂ : Type u_6} {F₃ : Type u_7} [inst_4 : NormedAddCommGroup F₁]
  [inst_5 : NormedSpace 𝕜 F₁] [inst_6 : NormedSpace ℝ F₁] [inst_7 : NormedAddCommGroup F₂] [inst_8 : NormedSpace 𝕜 F₂]
  [inst_9 : NormedAddCommGroup F₃] [inst_10 : NormedSpace 𝕜 F₃] [inst_11 : SMulCommClass ℝ 𝕜 F₁]
  [inst_12 : NormedSpace ℝ F₃] [inst_13 : SMulCommClass ℝ 𝕜 F₃] (B B_1 : F₁ →L[𝕜] F₂ →L[𝕜] F₃),
  B = B_1 →
    ∀ (μ μ_1 : MeasureTheory.Measure E),
      μ = μ_1 →
        ∀ (φ φ_1 : E → F₂),
          φ = φ_1 →
            ContDiffMapSupportedIn.integralAgainstBilinCLM B μ φ =
              ContDiffMapSupportedIn.integralAgainstBilinCLM B_1 μ_1 φ_1
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.alter!.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Ord α] (k : α) (f : Option β → Option β),
  Std.DTreeMap.Internal.Impl.Const.alter! k f Std.DTreeMap.Internal.Impl.leaf =
    match f none with
    | none => Std.DTreeMap.Internal.Impl.leaf
    | some v => Std.DTreeMap.Internal.Impl.inner 1 k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf
-- Mathlib.FieldTheory.Separable
IsSeparable.eq_1 : ∀ (F : Type u_1) {K : Type u_3} [inst : CommRing F] [inst_1 : Ring K] [inst_2 : Algebra F K] (x : K),
  IsSeparable F x = (minpoly F x).Separable
-- Mathlib.Algebra.EuclideanDomain.Defs
EuclideanDomain.GCD.induction : ∀ {R : Type u} [inst : EuclideanDomain R] {P : R → R → Prop} (a b : R),
  (∀ (x : R), P 0 x) → (∀ (a b : R), a ≠ 0 → P (b % a) a → P a b) → P a b
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.mapDomain_apply : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {G' : Type u_3} (f : G → G') (v : SkewMonoidAlgebra k G),
  (SkewMonoidAlgebra.mapDomain f) v = v.sum fun a => SkewMonoidAlgebra.single (f a)
-- Mathlib.GroupTheory.SemidirectProduct
instDecidableEqSemidirectProduct : {N : Type u_4} →
  {G : Type u_5} →
    {inst : Group N} →
      {inst_1 : Group G} → {φ : G →* MulAut N} → [DecidableEq N] → [DecidableEq G] → DecidableEq (N ⋊[φ] G)
-- Lean.Elab.Tactic.Induction
/-- The code path shared between `cases` and `fun_cases`; when we already have an `elimInfo`
and the `targets` contains the implicit targets
 -/
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.evalCasesCore : Lean.Syntax →
  Lean.Meta.ElimInfo → Array Lean.Expr → optParam (Array (Lean.Ident × Lean.FVarId)) #[] → Lean.Elab.Tactic.TacticM Unit
-- Std.Time.Time.PlainTime
/-- Adds minutes to a `PlainTime`.
 -/
Std.Time.PlainTime.addMinutes : Std.Time.PlainTime → Std.Time.Minute.Offset → Std.Time.PlainTime
-- Mathlib.Data.Fin.SuccPredOrder
Fin.orderSucc_last : ∀ (n : ℕ), Order.succ (Fin.last n) = Fin.last n
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.compare_minKey_modify_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {f : β → β} {he : Std.ExtDTreeMap.Const.modify t k f ≠ ∅},
  cmp ((Std.ExtDTreeMap.Const.modify t k f).minKey he) (t.minKey ⋯) = Ordering.eq
-- Mathlib.Data.Multiset.Bind
Multiset.bind_add : ∀ {α : Type u_1} {β : Type v} (s : Multiset α) (f g : α → Multiset β), (s.bind fun a => f a + g a) = s.bind f + s.bind g