mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.restrict_univ_removeLoops_eq : ∀ {α : Type u_1} {M : Matroid α}, (M.restrict Set.univ).removeLoops = M.removeLoops
-- Mathlib.Control.Monad.Writer
WriterT.run_tell : ∀ {M : Type u → Type v} {ω : Type u} [inst : Monad M] (w : ω), (tell w).run = pure (PUnit.unit, w)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.negRev_bijective : ∀ {α : Type u}, Function.Bijective FreeAddGroup.negRev
-- Mathlib.Algebra.Group.InjSurj
Function.Surjective.commMagma.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₂] [inst_1 : CommMagma M₁] (f : M₁ → M₂) (hf : Function.Surjective f)
  (mul : ∀ (x y : M₁), f (x * y) = f x * f y), Function.Surjective.commMagma f hf mul = { toMul := inst, mul_comm := ⋯ }
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxi.Iterator.Monadic.step_eq_step : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] {it : Std.IterM Id α},
  it.step = pure (Std.Shrink.deflate ⟨Std.Rxi.Iterator.Monadic.step it, ⋯⟩)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
/-- The projection from the wide pullback of `(f₁, f₂, f₃)` to `X₂`.  -/
CategoryTheory.Limits.ChosenPullback₃.p₂ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₁ X₂ X₃ S : C} →
      {f₁ : X₁ ⟶ S} →
        {f₂ : X₂ ⟶ S} →
          {f₃ : X₃ ⟶ S} →
            {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} →
              {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃} →
                {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} →
                  (h : CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃) → h.pullback ⟶ X₂
-- Mathlib.Algebra.Module.DedekindDomain
/-- A finitely generated torsion module over a Dedekind domain is an internal direct sum of its
`p i ^ e i`-torsion submodules where `p i` are factors of `(⊤ : Submodule R M).annihilator` and
`e i` are their multiplicities.  -/
Submodule.isInternal_prime_power_torsion : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {M : Type v} [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [Module.Finite R M],
  Module.IsTorsion R M →
    DirectSum.IsInternal fun p =>
      Submodule.torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (UniqueFactorizationMonoid.factors ⊤.annihilator))
-- Init.Data.Function
Function.Surjective.comp : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {g : β → γ} {f : α → β},
  Function.Surjective g → Function.Surjective f → Function.Surjective (g ∘ f)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rcc.size_toArray : ∀ {α : Type u} {r : Std.Rcc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.Rxc.HasSize α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_6 : Std.Rxc.IsAlwaysFinite α] [Std.Rxc.LawfulHasSize α], r.toArray.size = r.size
-- Mathlib.RingTheory.DedekindDomain.Different
not_dvd_differentIdeal_of_intTrace_not_mem : ∀ (A : Type u_1) {B : Type u_3} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain A]
  [inst_4 : IsDedekindDomain A] [inst_5 : IsDedekindDomain B] [inst_6 : Module.IsTorsionFree A B]
  [inst_7 : Module.Finite A B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] {p : Ideal A} (P Q : Ideal B),
  P * Q = Ideal.map (algebraMap A B) p → ∀ x ∈ Q, (Algebra.intTrace A B) x ∉ p → ¬P ∣ differentIdeal A B
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- **Alias** of `OrthonormalBasis.orthogonalProjectionOnto_eq_sum_rankOne`. -/
OrthonormalBasis.orthogonalProjection_eq_sum_rankOne : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] {U : Submodule 𝕜 E} [inst_4 : U.HasOrthogonalProjection]
  (b : OrthonormalBasis ι 𝕜 ↥U), U.orthogonalProjectionOnto = ∑ i, ((InnerProductSpace.rankOne 𝕜) (b i)) ↑(b i)
-- Mathlib.MeasureTheory.Function.Jacobian
/-- A version of **Sard's lemma** in fixed dimension: given a differentiable function from `E`
to `E` and a set where the differential is not invertible, then the image of this set has
zero measure. Here, we give an auxiliary statement towards this result.  -/
MeasureTheory.addHaar_image_eq_zero_of_det_fderivWithin_eq_zero_aux : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E}
  {f : E → E} {f' : E → E →L[ℝ] E} [inst_3 : MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E)
  [μ.IsAddHaarMeasure],
  (∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) →
    ∀ (R : ℝ),
      s ⊆ Metric.closedBall 0 R →
        ∀ (ε : NNReal), 0 < ε → (∀ x ∈ s, (f' x).det = 0) → μ (f '' s) ≤ ↑ε * μ (Metric.closedBall 0 R)
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
/-- Evidence that `lanLeftExtension f g` is a Kan extension.  -/
CategoryTheory.Bicategory.lanIsKan : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      (f : a ⟶ b) →
        (g : a ⟶ c) →
          [inst_1 : CategoryTheory.Bicategory.HasLeftKanExtension f g] →
            (CategoryTheory.Bicategory.lanLeftExtension f g).IsKan
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.Prod.sectL_mapId_hom : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] (c : C)
  (x : B),
  ((CategoryTheory.Bicategory.Prod.sectL B c).mapId x).hom =
    CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id x))
      (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id c))
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.coe_subtype : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] (S : L.Substructure M), ⇑S.subtype = Subtype.val
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Take
Std.IterM.step_toTake : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Monad m] [inst_1 : Std.Iterator α m β]
  [inst_2 : Std.Iterators.Finite α m] {it : Std.IterM m β},
  it.toTake.step = do
    let __do_lift ← it.step
    match __do_lift.inflate with
      | ⟨Std.IterStep.yield it' out, h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.yield it'.toTake out ⋯))
      | ⟨Std.IterStep.skip it', h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip it'.toTake ⋯))
      | ⟨Std.IterStep.done, h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.done ⋯))
-- Lean.Data.Lsp.Basic
Lean.Lsp.instOrdLocation : Ord Lean.Lsp.Location
-- Mathlib.Data.Multiset.Bind
Multiset.cons_sigma : ∀ {α : Type u_1} {σ : α → Type u_4} (a : α) (s : Multiset α) (t : (a : α) → Multiset (σ a)),
  (a ::ₘ s).sigma t = Multiset.map (Sigma.mk a) (t a) + s.sigma t
-- Mathlib.Algebra.Group.Finsupp
AddEquiv.finsuppUnique_symm : ∀ {M : Type u_8} [inst : AddZeroClass M] (d : M), AddEquiv.finsuppUnique.symm d = fun₀ | () => d
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.Quotient.mk_comp_algebraMap : ∀ (R₁ : Type u_1) {A : Type u_3} [inst : CommSemiring R₁] [inst_1 : Ring A] [inst_2 : Algebra R₁ A] (I : Ideal A)
  [inst_3 : I.IsTwoSided], (Ideal.Quotient.mk I).comp (algebraMap R₁ A) = algebraMap R₁ (A ⧸ I)
-- Mathlib.CategoryTheory.Localization.Bousfield
CategoryTheory.ObjectProperty.isLocalization_isLocal : ∀ {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] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : G ⊣ F) [F.Full] [F.Faithful],
  G.IsLocalization (CategoryTheory.ObjectProperty.isLocal fun x => x ∈ Set.range F.obj)
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.LocallyRingedSpace.Hom.mk.congr_simp : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (toHom toHom_1 : X.Hom Y.toPresheafedSpace) (e_toHom : toHom = toHom_1)
  (prop : ∀ (x : ↑↑X.toPresheafedSpace), IsLocalHom (CommRingCat.Hom.hom (toHom.stalkMap x))),
  { toHom := toHom, prop := prop } = { toHom := toHom_1, prop := ⋯ }
-- Mathlib.Algebra.Module.Equiv.Basic
/-- If `M` and `M₂` are both `R`-semimodules and `S`-semimodules and `R`-semimodule structures
are defined by an action of `R` on `S` (formally, we have two scalar towers), then any `S`-linear
equivalence from `M` to `M₂` is also an `R`-linear equivalence.

See also `LinearMap.restrictScalars`.  -/
LinearEquiv.restrictScalars : (R : Type u_1) →
  {S : Type u_4} →
    {M : Type u_5} →
      {M₂ : Type u_7} →
        [inst : Semiring R] →
          [inst_1 : Semiring S] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₂] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R M₂] →
                    [inst_6 : Module S M] →
                      [inst_7 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ R S] → (M ≃ₗ[S] M₂) → M ≃ₗ[R] M₂
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.Compacts.instT0SpaceOfT1Space : ∀ {α : Type u_1} [inst : TopologicalSpace α] [T1Space α], T0Space (TopologicalSpace.Compacts α)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get_erase : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] (h : (↑m).WF) {k a : α} {h' : (m.erase k).contains a = true},
  Std.DHashMap.Internal.Raw₀.Const.get (m.erase k) a h' = Std.DHashMap.Internal.Raw₀.Const.get m a ⋯
-- Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Profinite.NobelingProof.Products.limitOrdinal : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}},
  Order.IsSuccLimit o →
    ∀ (l : Profinite.NobelingProof.Products I),
      Profinite.NobelingProof.Products.isGood (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o)
          l ↔
        ∃ o' < o,
          Profinite.NobelingProof.Products.isGood
            (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o') l
-- Init.Internal.Order.Basic
Lean.Order.PProd.chain.chain_snd : ∀ {α : Sort u} {β : Sort v} [inst : Lean.Order.CCPO α] [inst_1 : Lean.Order.CCPO β] {c : α ×' β → Prop},
  Lean.Order.chain c → Lean.Order.chain (Lean.Order.PProd.chain.snd c)
-- Mathlib.Algebra.GroupWithZero.Basic
pow_ne_zero_iff : ∀ {M₀ : Type u_1} [inst : MonoidWithZero M₀] {a : M₀} {n : ℕ} [IsReduced M₀], n ≠ 0 → (a ^ n ≠ 0 ↔ a ≠ 0)
-- Mathlib.Combinatorics.Enumerative.Bell
_private.Mathlib.Combinatorics.Enumerative.Bell.0.Nat.sigmaPartitionWithPartEquiv.eq_1 : ∀ (n : ℕ),
  Nat.sigmaPartitionWithPartEquiv✝ n =
    { toFun := fun x => ⟨↑x.snd, ⟨↑x.fst + 1, ⋯⟩⟩, invFun := fun x => ⟨⟨↑x.snd - 1, ⋯⟩, ⟨x.fst, ⋯⟩⟩, left_inv := ⋯,
      right_inv := ⋯ }
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_mul_right_Ioo : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [MulPosReflectLT G₀] {c : G₀} (a b : G₀),
  0 < c → (fun x => x * c) '' Set.Ioo a b = Set.Ioo (a * c) (b * c)
-- Mathlib.Algebra.Ring.Defs
/-- Multiplication is commutative in a commutative multiplicative magma.  -/
NonUnitalCommSemiring.mul_comm : ∀ {α : Type u} [self : NonUnitalCommSemiring α] (a b : α), a * b = b * a
-- Mathlib.Topology.Maps.Basic
Topology.IsInducing.nhdsSet_eq_comap : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace Y] [inst_1 : TopologicalSpace X],
  Topology.IsInducing f → ∀ (s : Set X), nhdsSet s = Filter.comap f (nhdsSet (f '' s))
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four
CategoryTheory.ShortComplex.epi_of_epi_of_epi_of_epi : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {R₁ R₂ : CategoryTheory.ShortComplex C} (φ : R₁ ⟶ R₂),
  R₂.Exact → CategoryTheory.Epi R₁.g → CategoryTheory.Epi φ.τ₁ → CategoryTheory.Epi φ.τ₃ → CategoryTheory.Epi φ.τ₂
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
/-- A Lie-Rinehart subalgebra of a Lie-Rinehart ring forms a new Lie-Rinehart ring.  -/
LieRinehartSubalgebra.instLieRinehartRingSubtypeMem : ∀ {A : Type u_1} {L : Type u_2} [inst : CommRing A] [inst_1 : LieRing L] [inst_2 : Module A L]
  (L' : LieRinehartSubalgebra A L) [inst_3 : LieRingModule L A] [LieRinehartRing A L], LieRinehartRing A ↥L'
-- Mathlib.Analysis.Calculus.FDeriv.Mul
HasFDerivAt.mul_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {𝔸' : Type u_6} [inst_3 : NormedCommRing 𝔸'] [inst_4 : NormedAlgebra 𝕜 𝔸']
  {c : E → 𝔸'} {c' : E →L[𝕜] 𝔸'}, HasFDerivAt c c' x → ∀ (d : 𝔸'), HasFDerivAt (fun y => c y * d) (d • c') x
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
/-- A finite group of order dividing a prime is cyclic.  -/
isAddCyclic_of_card_dvd_prime : ∀ {α : Type u_1} [inst : AddGroup α] {p : ℕ} [hp : Fact (Nat.Prime p)], Nat.card α ∣ p → IsAddCyclic α
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.instReprTZifV2.repr : Std.Time.TimeZone.TZif.TZifV2 → ℕ → Std.Format
-- Init.Data.Float.Model.Unpacked.Round
/-- The mantissa.  -/
Float.Model.UnpackedFloat.ExtendedMantissa.mantissa : Float.Model.UnpackedFloat.ExtendedMantissa → ℕ
-- Mathlib.LinearAlgebra.CliffordAlgebra.Even
/-- The even submodule `CliffordAlgebra.evenOdd Q 0` is also a subalgebra.  -/
CliffordAlgebra.even : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (Q : QuadraticForm R M) → Subalgebra R (CliffordAlgebra Q)
-- Mathlib.Order.UpperLower.Principal
UpperSet.mem_Ioi_iff : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, b ∈ UpperSet.Ioi a ↔ a < b
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.map_zero_mem_closedCell`. -/
Topology.CWComplex.map_zero_mem_closedCell : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D] (n : ℕ)
  (i : Topology.RelCWComplex.cell C n), ↑(Topology.RelCWComplex.map n i) 0 ∈ Topology.RelCWComplex.closedCell n i
-- Mathlib.NumberTheory.LSeries.HurwitzZeta
HurwitzZeta.differentiableAt_expZeta : ∀ (a : UnitAddCircle) (s : ℂ), s ≠ 1 ∨ a ≠ 0 → DifferentiableAt ℂ (HurwitzZeta.expZeta a) s
-- Mathlib.NumberTheory.NumberField.House
/-- The house of an algebraic number as the norm of its image by the canonical embedding.  -/
NumberField.house : {K : Type u_1} → [inst : Field K] → [NumberField K] → K → ℝ
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKeyD_alter_eq_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {f : Option (β k) → Option (β k)},
  (t.alter k f).isEmpty = false →
    ∀ {fallback : α},
      (t.alter k f).maxKeyD fallback = k ↔ (f (t.get? k)).isSome = true ∧ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.divLeft.eq_1 : ∀ {G : Type v} [inst : Group G] [inst_1 : PseudoEMetricSpace G] [inst_2 : IsIsometricSMul G G]
  [inst_3 : IsIsometricSMul Gᵐᵒᵖ G] (c : G),
  IsometryEquiv.divLeft c = { toEquiv := Equiv.divLeft c, isometry_toFun := ⋯ }
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.reduct_withConstants : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {S : L.Substructure M} {A : Set M} (h : A ⊆ ↑S),
  (L.lhomWithConstants ↑A).substructureReduct (S.withConstants h) = S
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
SimpleGraph.dotProduct_mulVec_adjMatrix : ∀ {α : Type u_1} {V : Type u_2} {G : SimpleGraph V} [inst : DecidableRel G.Adj] [inst_1 : Fintype V]
  [inst_2 : NonAssocSemiring α] (x y : V → α),
  x ⬝ᵥ (SimpleGraph.adjMatrix α G).mulVec y = ∑ i, ∑ j, if G.Adj i j then x i * y j else 0
-- Mathlib.FieldTheory.PurelyInseparable.Basic
/-- If `K / E / F` is a field extension tower, such that `E / F` is algebraic and `K / E`
is separable, then `E` adjoin `separableClosure F K` is equal to `K`. It is a special case of
`separableClosure.adjoin_eq_of_isAlgebraic`, and is an intermediate result used to prove it.  -/
separableClosure.adjoin_eq_of_isAlgebraic_of_isSeparable : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type w) [inst_3 : Field K]
  [inst_4 : Algebra F K] [inst_5 : Algebra E K] [IsScalarTower F E K] [Algebra.IsAlgebraic F E]
  [Algebra.IsSeparable E K], IntermediateField.adjoin E ↑(separableClosure F K) = ⊤
-- Mathlib.Topology.LocallyConstant.Algebra
/-- `LocallyConstant.map` as a linear map.  -/
LocallyConstant.mapₗ : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      {Z : Type u_6} →
        (R : Type u_7) →
          [inst_1 : Semiring R] →
            [inst_2 : AddCommMonoid Y] →
              [inst_3 : Module R Y] →
                [inst_4 : AddCommMonoid Z] →
                  [inst_5 : Module R Z] → (Y →ₗ[R] Z) → LocallyConstant X Y →ₗ[R] LocallyConstant X Z
-- Mathlib.Util.AtomM.Recurse
/-- The recursive context.  -/
_private.Mathlib.Util.AtomM.Recurse.0.Mathlib.Tactic.AtomM.RecurseM.run.rctx : IO.Ref Mathlib.Tactic.AtomM.State →
  Mathlib.Tactic.AtomM.Recurse.Config →
    Bool →
      (Lean.Expr → Mathlib.Tactic.AtomM Lean.Meta.Simp.Result) →
        Mathlib.Tactic.AtomM.Recurse.Context → Mathlib.Tactic.AtomM.Context
-- Std.Data.HashMap.Lemmas
Std.HashMap.mem_iff_contains : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {a : α}, a ∈ m ↔ m.contains a = true
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_comp_add_left : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} (f : ℝ → E) (d : ℝ),
  ∫ (x : ℝ) in a..b, f (d + x) = ∫ (x : ℝ) in d + a..d + b, f x
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
HasSum.star : ∀ {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α]
  [inst_2 : StarAddMonoid α] [ContinuousStar α] {f : β → α} {a : α},
  HasSum f a L → HasSum (fun b => star (f b)) (star a) L
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.Quotient.group : {G : Type u_1} → [inst : Group G] → (N : Subgroup G) → [nN : N.Normal] → Group (G ⧸ N)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- Fundamental theorem of calculus: if `f : ℝ → E` is integrable on `a..b` and `f` has a finite
limit `c` almost surely at `b`, then the derivative of `u ↦ ∫ x in a..u, f x` at `b` equals `c`.  -/
intervalIntegral.deriv_integral_of_tendsto_ae_right : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {c : E}
  {a b : ℝ},
  IntervalIntegrable f MeasureTheory.volume a b →
    StronglyMeasurableAtFilter f (nhds b) MeasureTheory.volume →
      Filter.Tendsto f (nhds b ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds c) →
        deriv (fun u => ∫ (x : ℝ) in a..u, f x) b = c
-- Mathlib.Data.Fin.Tuple.Reflection
FinVec.Forall.eq_def : ∀ {α : Type u_1} (x : ℕ) (x_1 : (Fin x → α) → Prop),
  FinVec.Forall x_1 =
    match x, x_1 with
    | 0, P => P ![]
    | n.succ, P => ∀ (x : α), FinVec.Forall fun v => P (Matrix.vecCons x v)
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiffWithinAt_insert_self : ∀ {𝕜 : 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} {x : E} {n : WithTop ℕ∞}, ContDiffWithinAt 𝕜 n f (insert x s) x ↔ ContDiffWithinAt 𝕜 n f s x
-- Mathlib.Algebra.GroupWithZero.NeZero
/-- In a nontrivial monoid with zero, zero and one are different.  -/
NeZero.one : ∀ {M₀ : Type u_1} [inst : MulZeroOneClass M₀] [Nontrivial M₀], NeZero 1
-- Mathlib.Combinatorics.Quiver.Path.Vertices
Quiver.Path.vertices_cons : ∀ {V : Type u_1} [inst : Quiver V] {a b c : V} (p : Quiver.Path a b) (e : b ⟶ c),
  (p.cons e).vertices = p.vertices.concat c
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toArray_rio_eq_none_iff : ∀ {n i : ℕ}, (*...n).toArray[i]? = none ↔ n ≤ i
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four
_private.Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four.0.CategoryTheory.ComposableArrows.Precomp.map.match_1.eq_1 : ∀ {n : ℕ} (motive : (x x_1 : Fin (n + 1 + 1)) → x ≤ x_1 → Sort u_1) (isLt isLt_1 : 0 < n + 1 + 1)
  (x : ⟨0, isLt⟩ ≤ ⟨0, isLt_1⟩)
  (h_1 : (isLt isLt_2 : 0 < n + 1 + 1) → (x : ⟨0, isLt⟩ ≤ ⟨0, isLt_2⟩) → motive ⟨0, isLt⟩ ⟨0, isLt_2⟩ x)
  (h_2 :
    (isLt : 0 < n + 1 + 1) → (isLt_2 : 1 < n + 1 + 1) → (x : ⟨0, isLt⟩ ≤ ⟨1, isLt_2⟩) → motive ⟨0, isLt⟩ ⟨1, isLt_2⟩ x)
  (h_3 :
    (isLt : 0 < n + 1 + 1) →
      (j : ℕ) → (hj : j + 2 < n + 1 + 1) → (x : ⟨0, isLt⟩ ≤ ⟨j + 2, hj⟩) → motive ⟨0, isLt⟩ ⟨j.succ.succ, hj⟩ x)
  (h_4 :
    (i : ℕ) →
      (hi : i + 1 < n + 1 + 1) →
        (j : ℕ) → (hj : j + 1 < n + 1 + 1) → (hij : ⟨i + 1, hi⟩ ≤ ⟨j + 1, hj⟩) → motive ⟨i.succ, hi⟩ ⟨j.succ, hj⟩ hij),
  (match ⟨0, isLt⟩, ⟨0, isLt_1⟩, x with
    | ⟨0, isLt⟩, ⟨0, isLt_2⟩, x => h_1 isLt isLt_2 x
    | ⟨0, isLt⟩, ⟨1, isLt_2⟩, x => h_2 isLt isLt_2 x
    | ⟨0, isLt⟩, ⟨j.succ.succ, hj⟩, x => h_3 isLt j hj x
    | ⟨i.succ, hi⟩, ⟨j.succ, hj⟩, hij => h_4 i hi j hj hij) =
    h_1 isLt isLt_1 x
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.AdicCauchySequence.ext : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {x y : AdicCompletion.AdicCauchySequence I M}, (∀ (n : ℕ), ↑x n = ↑y n) → x = y
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.grp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] → (self : CategoryTheory.Grp C) → CategoryTheory.GrpObj self.X
-- Mathlib.Combinatorics.Additive.PluenneckeRuzsa
/-- **Ruzsa's triangle inequality**. Division version.  -/
Finset.ruzsa_triangle_inequality_div_div_div : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : Group G] (A B C : Finset G),
  (A / C).card * B.card ≤ (A / B).card * (C / B).card
-- Init.Data.String.TakeDrop
/-- Checks whether a string only consists of matches of the pattern `pat`.

Short-circuits at the first pattern mis-match.

This function is generic over all currently supported patterns.

Examples:

* `"brown".all Char.isLower = true`

* `"brown and orange".all Char.isLower = false`

* `"aaaaaa".all 'a' = true`

* `"aaaaaa".all "aa" = true`

* `"aaaaaaa".all "aa" = false`
 -/
String.all : {ρ : Type} → String → (pat : ρ) → [String.Slice.Pattern.ForwardPattern pat] → Bool
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Multipliable.tsum_congr_cofinite₀ : ∀ {α : Type u_1} {K : Type u_4} [inst : CommGroupWithZero K] [inst_1 : TopologicalSpace K] {f g : α → K}
  [SeparatelyContinuousMul K] [T2Space K],
  Multipliable f →
    ∀ {s : Finset α},
      (∀ a ∈ s, f a ≠ 0) → (∀ a ∉ s, f a = g a) → ∏' (i : α), g i = (∏' (i : α), f i) * ((∏ i ∈ s, g i) / ∏ i ∈ s, f i)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
measurable_iInf_of_upperSemicontinuous : ∀ {β : Type u_2} {δ : Type u_4} [inst : TopologicalSpace β] {mβ : MeasurableSpace β} [BorelSpace β]
  {mδ : MeasurableSpace δ} [inst_2 : CompleteLinearOrder β] [OrderTopology β] [SecondCountableTopology β] {ι : Type u_5}
  [inst : TopologicalSpace ι] [TopologicalSpace.SeparableSpace ι] {f : ι → δ → β},
  (∀ (t : ι), Measurable (f t)) → (∀ (x : δ), UpperSemicontinuous fun x_1 => f x_1 x) → Measurable (⨅ i, f i)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonPrepareRenameParams.toJson : Lean.Lsp.PrepareRenameParams → Lean.Json
-- Mathlib.RingTheory.Adjoin.Polynomial.Basic
Algebra.adjoin_eq_exists_aeval : ∀ (R : Type u) {A : Type z} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (x : A) (a : ↥R[x]),
  ∃ p, (Polynomial.aeval x) p = ↑a
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.leftHomologyFunctorOpNatIso_hom_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasKernels C] [inst_3 : CategoryTheory.Limits.HasCokernels C]
  [inst_4 : CategoryTheory.Limits.HasKernels Cᵒᵖ] [inst_5 : CategoryTheory.Limits.HasCokernels Cᵒᵖ]
  (X : (CategoryTheory.ShortComplex C)ᵒᵖ),
  (CategoryTheory.ShortComplex.leftHomologyFunctorOpNatIso C).hom.app X = (Opposite.unop X).rightHomologyOpIso.inv