mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
/-- The forward image of a measurable space under a function. `map f m` contains the sets
`s : Set β` whose preimage under `f` is measurable.  -/
MeasurableSpace.map : {α : Type u_1} → {β : Type u_2} → (α → β) → MeasurableSpace α → MeasurableSpace β
-- Init.Data.BitVec.Lemmas
_private.Init.Data.BitVec.Lemmas.0.BitVec.sdiv_eq.match_1.eq_3 : ∀ (motive : Bool → Bool → Sort u_1) (h_1 : Unit → motive false false) (h_2 : Unit → motive false true)
  (h_3 : Unit → motive true false) (h_4 : Unit → motive true true),
  (match true, false with
    | false, false => h_1 ()
    | false, true => h_2 ()
    | true, false => h_3 ()
    | true, true => h_4 ()) =
    h_3 ()
-- Mathlib.CategoryTheory.EssentiallySmall
CategoryTheory.ShrinkHoms.from_to : ∀ {C' : Type u_1} (X : CategoryTheory.ShrinkHoms.{u_1} C'), CategoryTheory.ShrinkHoms.toShrinkHoms X.fromShrinkHoms = X
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.image.map_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C}
  [inst_1 : CategoryTheory.Limits.HasImage f.hom] [inst_2 : CategoryTheory.Limits.HasImage g.hom] (sq : f ⟶ g)
  [inst_3 : CategoryTheory.Limits.HasImageMap sq] {h : CategoryTheory.Arrow C}
  [inst_4 : CategoryTheory.Limits.HasImage h.hom] (sq' : g ⟶ h) [inst_5 : CategoryTheory.Limits.HasImageMap sq']
  [inst_6 : CategoryTheory.Limits.HasImageMap (CategoryTheory.CategoryStruct.comp sq sq')],
  CategoryTheory.Limits.image.map (CategoryTheory.CategoryStruct.comp sq sq') =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.map sq) (CategoryTheory.Limits.image.map sq')
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.card_support_eq_two : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {f : Equiv.Perm α}, f.support.card = 2 ↔ f.IsSwap
-- Mathlib.Algebra.Group.Pi.Lemmas
AddHom.piMap_apply : ∀ {ι : Type u_1} {M : ι → Type u_3} {N : ι → Type u_4} [inst : (i : ι) → Add (M i)] [inst_1 : (i : ι) → Add (N i)]
  (g : (i : ι) → M i →ₙ+ N i) (x : (i : ι) → M i) (i : ι), (AddHom.piMap g) x i = (g i) (x i)
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.aeval_eq_bind₁ : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [inst : CommSemiring R] (f : σ → MvPolynomial τ R),
  MvPolynomial.aeval f = MvPolynomial.bind₁ f
-- Init.Data.Range.Polymorphic.Lemmas
Std.Ric.pairwise_toList_upwardEnumerableLt : ∀ {α : Type u} {r : Std.Ric α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_7 : Std.Rxc.IsAlwaysFinite α], List.Pairwise (fun a b => Std.PRange.UpwardEnumerable.LT a b) r.toList
-- Mathlib.Order.Shrink
instOrderTopShrink.eq_1 : ∀ {α : Type u_1} [inst : Small.{u, u_1} α] [inst_1 : Preorder α] [inst_2 : OrderTop α],
  instOrderTopShrink = { toTop := instTopShrink, le_top := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.CommGrp.forget₂Grp_comp_forget : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  (CategoryTheory.CommGrp.forget₂Grp C).comp (CategoryTheory.Grp.forget C) = CategoryTheory.CommGrp.forget C
-- Batteries.Data.AssocList
_private.Batteries.Data.AssocList.0.List.filter.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match false with
    | true => h_1 ()
    | false => h_2 ()) =
    h_2 ()
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
/-- The image of `seminormFromConst_seq c f x` is bounded below by zero.  -/
seminormFromConst_bddBelow : ∀ {R : Type u_1} [inst : CommRing R] (c : R) (f : RingSeminorm R) (x : R),
  BddBelow (Set.range (seminormFromConst_seq c f x))
-- Mathlib.RingTheory.ClassGroup.Basic
ClassGroup.mk.congr_simp : ∀ {R : Type u_1} (K : Type u_2) [inst : CommRing R] [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDomain R], ClassGroup.mk K = ClassGroup.mk K
-- Mathlib.Data.ENNReal.Basic
/-- Coercion `ℝ≥0 → ℝ≥0∞` as a `RingHom`.  -/
ENNReal.ofNNRealHom : NNReal →+* ENNReal
-- Mathlib.NumberTheory.NumberField.CMField
NumberField.IsCMField.regulator_div_regulator_eq_two_pow_mul_indexRealUnits_inv : ∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [NumberField.IsCMField K] [inst_3 : NumberField K],
  NumberField.Units.regulator K / NumberField.Units.regulator ↥(NumberField.maximalRealSubfield K) =
    2 ^ NumberField.Units.rank K * (↑(NumberField.IsCMField.indexRealUnits K))⁻¹
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- Eta-expanded form of `MeasureTheory.StronglyMeasurable.inv` -/
MeasureTheory.StronglyMeasurable.fun_inv : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {mα : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : Inv β]
  [ContinuousInv β], MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable fun i => (f i)⁻¹
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurableAtom_subset : ∀ {β : Type u_2} [inst : MeasurableSpace β] {s : Set β} {x : β}, MeasurableSet s → x ∈ s → measurableAtom x ⊆ s
-- Mathlib.Data.Finset.Lattice.Basic
Finset.inter_congr_right : ∀ {α : Type u_1} [inst : DecidableEq α] {s t u : Finset α}, t ∩ u ⊆ s → s ∩ u ⊆ t → s ∩ u = t ∩ u
-- Lean.Parser
Lean.PrettyPrinter.Parenthesizer.numLit.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Topology.Instances.AddCircle.Defs
/-- The rescaling equivalence between additive circles with different periods.  -/
AddCircle.equivAddCircle : {𝕜 : Type u_1} → [inst : Field 𝕜] → (p q : 𝕜) → p ≠ 0 → q ≠ 0 → AddCircle p ≃+ AddCircle q
-- Mathlib.Algebra.Homology.ImageToKernel
imageToKernel_zero_left : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V}
  (g : B ⟶ C) [inst_2 : CategoryTheory.Limits.HasKernels V] [inst_3 : CategoryTheory.Limits.HasZeroObject V]
  {w : CategoryTheory.CategoryStruct.comp 0 g = 0}, imageToKernel 0 g w = 0
-- Std.Time.Date.Unit.Day
Std.Time.Day.instNegOffset : Neg Std.Time.Day.Offset
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.Monomial.mk.inj : ∀ {coef : ℝ} {unit : Tactic.ComputeAsymptotics.UnitMonomial} {coef_1 : ℝ}
  {unit_1 : Tactic.ComputeAsymptotics.UnitMonomial},
  { coef := coef, unit := unit } = { coef := coef_1, unit := unit_1 } → coef = coef_1 ∧ unit = unit_1
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- A meromorphic function has normal form at `x` iff it is either analytic
there, or if it has a pole at `x` and takes the default value `0`.  -/
meromorphicNFAt_iff_analyticAt_or : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜},
  MeromorphicNFAt f x ↔ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0
-- Mathlib.Logic.OpClass
instRightCommutativeOfLeftCommutative : ∀ {α : Sort u} {β : Sort v} {f : α → β → β} [h : LeftCommutative f], RightCommutative fun x y => f y x
-- Mathlib.Topology.Category.TopCat.Limits.Pullbacks
TopCat.pullbackIsoProdSubtype_hom_snd : ∀ {X Y Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (TopCat.pullbackIsoProdSubtype f g).hom (TopCat.pullbackSnd f g) =
    CategoryTheory.Limits.pullback.snd f g
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
AlgebraicGeometry.instQuasiSeparatedFstScheme : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [AlgebraicGeometry.QuasiSeparated g],
  AlgebraicGeometry.QuasiSeparated (CategoryTheory.Limits.pullback.fst f g)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.lintegral_add_measure : ∀ {α : Type u_1} {m : MeasurableSpace α} (f : α → ENNReal) (μ ν : MeasureTheory.Measure α),
  ∫⁻ (a : α), f a ∂(μ + ν) = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), f a ∂ν
-- Mathlib.RingTheory.Adjoin.Singleton
/-- **Alias** of `Algebra.RingHom.adjoinAlgebraMap_apply`. -/
Algebra.RingHom.adjoin_algebraMap_apply : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : CommSemiring A] [inst_1 : CommSemiring B]
  [inst_2 : CommSemiring C] [inst_3 : Algebra A B] [inst_4 : Algebra B C] [inst_5 : Algebra A C]
  [inst_6 : IsScalarTower A B C] (b : B) (x : ↥A[b]), ↑((Algebra.RingHom.adjoinAlgebraMap b) x) = (algebraMap B C) ↑x
-- Mathlib.RingTheory.Nakayama
/-- **Nakayama's Lemma** - A slightly more general version of (2) in
[Stacks 00DV](https://stacks.math.columbia.edu/tag/00DV).
See also `eq_bot_of_le_smul_of_le_jacobson_bot` for the special case when `J = ⊥`.  -/
Submodule.eq_smul_of_le_smul_of_le_jacobson : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I J : Ideal R}
  {N : Submodule R M}, N.FG → N ≤ I • N → I ≤ J.jacobson → N = J • N
-- Lean.Elab.InfoTree.Types
Lean.Elab.DocInfo.toElabInfo : Lean.Elab.DocInfo → Lean.Elab.ElabInfo
-- Init.Data.Order.Classes
Std.LawfulOrderBEq.beq_iff_le_and_ge : ∀ {α : Type u} {inst : BEq α} {inst_1 : LE α} [self : Std.LawfulOrderBEq α] (a b : α), (a == b) = true ↔ a ≤ b ∧ b ≤ a
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.ae_restrict_biUnion_eq : ∀ {α : Type u_2} {ι : Type u_6} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : ι → Set α) {t : Set ι},
  t.Countable → MeasureTheory.ae (μ.restrict (⋃ i ∈ t, s i)) = ⨆ i ∈ t, MeasureTheory.ae (μ.restrict (s i))
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_map_f_f : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (α : Type u_3)
  [inst_2 : AddRightCancelSemigroup α] [inst_3 : One α]
  {X Y : HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) (ComplexShape.down α)} (f : X ⟶ Y) (n : α),
  ((CategoryTheory.Idempotents.karoubiChainComplexEquivalence C α).inverse.map f).f.f n = (f.f n).f
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.Code.instantiateValueLevelParams.instParams : List Lean.Name →
  List Lean.Level →
    Array (Lean.Compiler.LCNF.Param Lean.Compiler.LCNF.Purity.pure) →
      Array (Lean.Compiler.LCNF.Param Lean.Compiler.LCNF.Purity.pure)
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalCategory.tensor_ε : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.MonoidalCategory.tensor C) =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
-- Mathlib.Data.QPF.Multivariate.Constructions.Fix
MvQPF.WEquiv.below : {n : ℕ} →
  {F : TypeVec.{u} (n + 1) → Type u} →
    [q : MvQPF F] →
      {α : TypeVec.{u} n} →
        {motive : (a a_1 : (MvQPF.P F).W α) → MvQPF.WEquiv a a_1 → Prop} →
          {a a_1 : (MvQPF.P F).W α} → MvQPF.WEquiv a a_1 → Prop
-- Mathlib.GroupTheory.OrderOfElement
addOrderOf_eq_zero_iff' : ∀ {G : Type u_1} [inst : AddMonoid G] {x : G}, addOrderOf x = 0 ↔ ∀ (n : ℕ), 0 < n → n • x ≠ 0
-- Mathlib.Order.Interval.Set.Disjoint
Set.iUnion_Ici : ∀ {α : Type v} [inst : Preorder α], ⋃ a, Set.Ici a = Set.univ
-- Mathlib.Analysis.RCLike.Basic
RCLike.I_mul_I_ax : ∀ {K : semiOutParam (Type u_1)} [self : RCLike K], RCLike.I = 0 ∨ RCLike.I * RCLike.I = -1
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.mkInductiveAux₁.eq_3 : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {P Q : ChainComplex V ℕ} (e : P ⟶ Q) (zero : P.X 0 ⟶ Q.X 1) (one : P.X 1 ⟶ Q.X 2)
  (comm_one :
    e.f 1 = CategoryTheory.CategoryStruct.comp (P.d 1 0) zero + CategoryTheory.CategoryStruct.comp one (Q.d 2 1))
  (succ :
    (n : ℕ) →
      (p :
          (f : P.X n ⟶ Q.X (n + 1)) ×'
            (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×'
              e.f (n + 1) =
                CategoryTheory.CategoryStruct.comp (P.d (n + 1) n) f +
                  CategoryTheory.CategoryStruct.comp f' (Q.d (n + 2) (n + 1))) →
        (f'' : P.X (n + 2) ⟶ Q.X (n + 3)) ×'
          e.f (n + 2) =
            CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 1)) p.snd.fst +
              CategoryTheory.CategoryStruct.comp f'' (Q.d (n + 3) (n + 2)))
  (n : ℕ),
  Homotopy.mkInductiveAux₁ e zero one comm_one succ n.succ.succ =
    ⟨(Homotopy.mkInductiveAux₁ e zero one comm_one succ (n + 1)).snd.fst,
      ⟨(succ (n + 1) (Homotopy.mkInductiveAux₁ e zero one comm_one succ (n + 1))).fst, ⋯⟩⟩
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKeyD_insertMany_emptyWithCapacity_list_of_mem : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {l : List ((a : α) × β a)} {k k' fallback : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
      k ∈ List.map Sigma.fst l → (↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertMany l)).getKeyD k' fallback = k
-- Mathlib.Data.List.Cycle
List.prev_cons_cons_of_ne : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α) (x y : α) (h : x ∈ y :: x :: l), x ≠ y → (y :: x :: l).prev x h = y
-- Std.Data.Iterators.Lemmas.Producers.Repeat
Std.Iter.repeat.eq_1 : ∀ {α : Type w} (f : α → α) (init : α), Std.Iter.repeat f init = { internalState := { next := init } }
-- Mathlib.Algebra.BigOperators.Finprod
finprod_zero_le_one : ∀ {M : Type u_7} {α : Type u_8} [inst : CommMonoidWithZero M] [inst_1 : PartialOrder M] [ZeroLEOneClass M]
  [PosMulMono M], ∏ᶠ (x : α), 0 ≤ 1
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.modifyArithState : (Lean.Meta.Sym.Arith.State → Lean.Meta.Sym.Arith.State) → Lean.Meta.Sym.SymM Unit
-- Init.Data.String.Lemmas.Iterate
String.Slice.Pos.Splits.mem_toList_left_iff : ∀ {s : String.Slice} {pos : s.Pos} {t u : String} {c : Char},
  pos.Splits t u → (c ∈ t.toList ↔ ∃ pos', ∃ (h : pos' < pos), pos'.get ⋯ = c)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.tan_eq_sin_div_cos : ∀ (θ : Real.Angle), θ.tan = θ.sin / θ.cos
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.not_bot_adj : ∀ {V : Type u} {G : SimpleGraph V} {a b : V}, ¬⊥.Adj a b
-- Mathlib.CategoryTheory.Bicategory.Span.Basic
CategoryTheory.Span.Hom.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {Wₗ Wᵣ : CategoryTheory.MorphismProperty C} {c c' : C}
  {S₁ S₂ : CategoryTheory.Span Wₗ Wᵣ c c'} [inst_1 : SizeOf C] [inst_2 : ⦃X Y : C⦄ → (x : X ⟶ Y) → SizeOf (Wₗ x)]
  [inst_3 : ⦃X Y : C⦄ → (x : X ⟶ Y) → SizeOf (Wᵣ x)] (hom : S₁.apex ⟶ S₂.apex)
  (hom_l : autoParam (CategoryTheory.CategoryStruct.comp hom S₂.l = S₁.l) CategoryTheory.Span.Hom.hom_l._autoParam)
  (hom_r : autoParam (CategoryTheory.CategoryStruct.comp hom S₂.r = S₁.r) CategoryTheory.Span.Hom.hom_r._autoParam),
  sizeOf { hom := hom, hom_l := hom_l, hom_r := hom_r } = 1 + sizeOf hom + sizeOf hom_l + sizeOf hom_r
-- Mathlib.RingTheory.Coprime.Basic
isCoprime_mul_unit_left : ∀ {R : Type u_1} [inst : CommSemiring R] {x : R}, IsUnit x → ∀ (y z : R), IsCoprime (x * y) (x * z) ↔ IsCoprime y z
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.size_filterMap_eq_size_iff : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  {γ : α → Type w} [inst_2 : LawfulBEq α] {f : (a : α) → β a → Option (γ a)},
  (↑m).WF →
    ((↑(Std.DHashMap.Internal.Raw₀.filterMap f m)).size = (↑m).size ↔
      ∀ (a : α) (h : m.contains a = true), (f a (m.get a h)).isSome = true)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
Lean.Meta.Grind.Arith.CommRing.getNext? : Lean.Meta.Grind.Arith.CommRing.RingM (Option Lean.Meta.Grind.Arith.CommRing.EqCnstr)
-- Init.Data.Bool
Bool.bne_left_inj : ∀ {x y z : Bool}, (x != z) = (y != z) ↔ x = y
-- Mathlib.RingTheory.Conductor
conductor_subset_adjoin : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {x : S},
  ↑(conductor R x) ⊆ ↑R[x]
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Functor.reflectsEpimorphisms_of_preserves_of_reflects : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [G.PreservesEpimorphisms] [(F.comp G).ReflectsEpimorphisms], F.ReflectsEpimorphisms
-- Mathlib.Geometry.Manifold.DerivationBundle
/-- `ContMDiffMap.evalRingHom` gives rise to an algebra structure of `C^∞⟮I, M; 𝕜⟯` on `𝕜`.  -/
PointedContMDiffMap.evalAlgebra : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_3} →
            [inst_3 : TopologicalSpace H] →
              {I : ModelWithCorners 𝕜 E H} →
                {M : Type u_4} →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] → {x : M} → Algebra (PointedContMDiffMap 𝕜 I M (↑⊤) x) 𝕜
-- Mathlib.Topology.Algebra.Group.Basic
nhds_translation_inv_mul : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] (x : G),
  Filter.comap (fun x_1 => x⁻¹ * x_1) (nhds 1) = nhds x
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
/-- A finite affine combination of covariant derivatives as a covariant derivative.  -/
CovariantDerivative.finiteAffineCombination : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_3} →
            [inst_3 : TopologicalSpace H] →
              {I : ModelWithCorners 𝕜 E H} →
                {M : Type u_4} →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] →
                      {F : Type u_5} →
                        [inst_6 : NormedAddCommGroup F] →
                          [inst_7 : NormedSpace 𝕜 F] →
                            {V : M → Type u_6} →
                              [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)] →
                                [inst_9 : (x : M) → AddCommGroup (V x)] →
                                  [inst_10 : (x : M) → Module 𝕜 (V x)] →
                                    [inst_11 : (x : M) → TopologicalSpace (V x)] →
                                      [inst_12 : ∀ (x : M), IsTopologicalAddGroup (V x)] →
                                        [inst_13 : ∀ (x : M), ContinuousSMul 𝕜 (V x)] →
                                          [inst_14 : FiberBundle F V] →
                                            {ι : Type u_7} →
                                              {s : Finset ι} →
                                                (ι → CovariantDerivative I F V) →
                                                  {f : ι → M → 𝕜} → ∑ i ∈ s, f i = 1 → CovariantDerivative I F V
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.HasFiniteIntegral.of_mem_Icc_of_ne_top : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  {a b : ENNReal},
  a ≠ ⊤ → b ≠ ⊤ → ∀ {X : α → ENNReal}, (∀ᵐ (ω : α) ∂μ, X ω ∈ Set.Icc a b) → MeasureTheory.HasFiniteIntegral X μ
-- Mathlib.RingTheory.Coalgebra.Basic
/-- The comultiplication of the coalgebra  -/
RingTheory.LinearMap.termδ : Lean.ParserDescr
-- Init.Data.String.Lemmas.Pattern.Split.Basic
_private.Init.Data.String.Lemmas.Pattern.Split.Basic.0.String.Slice.SplitIterator.instIteratorIdSubslice.match_3.eq_1 : ∀ {σ : String.Slice → Type} [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)]
  {s : String.Slice} (searcher : Std.Iter (String.Slice.Pattern.SearchStep s)) (motive : searcher.Step → Sort u_1)
  (searcher' : Std.Iter (String.Slice.Pattern.SearchStep s)) (startPos endPos : s.Pos)
  (hps :
    searcher.IsPlausibleStep (Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.matched startPos endPos)))
  (h_1 :
    (searcher'_1 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
      (startPos_1 endPos_1 : s.Pos) →
        (hps_1 :
            searcher.IsPlausibleStep
              (Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.matched startPos_1 endPos_1))) →
          ⟨Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.matched startPos endPos), hps⟩ =
              ⟨Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.matched startPos_1 endPos_1), hps_1⟩ →
            motive
              ⟨Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.matched startPos_1 endPos_1), hps_1⟩)
  (h_2 :
    (searcher'_1 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
      (startPos_1 endPos_1 : s.Pos) →
        (hps_1 :
            searcher.IsPlausibleStep
              (Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.rejected startPos_1 endPos_1))) →
          ⟨Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.matched startPos endPos), hps⟩ =
              ⟨Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.rejected startPos_1 endPos_1), hps_1⟩ →
            motive
              ⟨Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.rejected startPos_1 endPos_1), hps_1⟩)
  (h_3 :
    (searcher'_1 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
      (hps_1 : searcher.IsPlausibleStep (Std.IterStep.skip searcher'_1)) →
        ⟨Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.matched startPos endPos), hps⟩ =
            ⟨Std.IterStep.skip searcher'_1, hps_1⟩ →
          motive ⟨Std.IterStep.skip searcher'_1, hps_1⟩)
  (h_4 :
    (property : searcher.IsPlausibleStep Std.IterStep.done) →
      ⟨Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.matched startPos endPos), hps⟩ =
          ⟨Std.IterStep.done, property⟩ →
        motive ⟨Std.IterStep.done, property⟩),
  (match h : ⟨Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.matched startPos endPos), hps⟩ with
    | ⟨Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.matched startPos_1 endPos_1), hps_1⟩ =>
      h_1 searcher'_1 startPos_1 endPos_1 hps_1 h
    | ⟨Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.rejected startPos_1 endPos_1), hps_1⟩ =>
      h_2 searcher'_1 startPos_1 endPos_1 hps_1 h
    | ⟨Std.IterStep.skip searcher'_1, hps_1⟩ => h_3 searcher'_1 hps_1 h
    | ⟨Std.IterStep.done, property⟩ => h_4 property h) =
    h_1 searcher' startPos endPos hps ⋯
-- Lean.Elab.Tactic.RCases
Lean.Elab.Tactic.RCases.RCasesPatt.clear.inj : ∀ {ref ref_1 : Lean.Syntax},
  Lean.Elab.Tactic.RCases.RCasesPatt.clear ref = Lean.Elab.Tactic.RCases.RCasesPatt.clear ref_1 → ref = ref_1
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.mem_toArray_iff_getKey?_eq_some_and_get?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {v : β},
      (k, v) ∈ Std.DTreeMap.Raw.Const.toArray t ↔ t.getKey? k = some k ∧ Std.DTreeMap.Raw.Const.get? t k = some v
-- Mathlib.Algebra.Polynomial.Derivative
/-- **Alias** of the forward direction of `Polynomial.derivative_eq_zero`. -/
Polynomial.natDegree_eq_zero_of_derivative_eq_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} [IsAddTorsionFree R],
  Polynomial.derivative p = 0 → p.natDegree = 0
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
/-- A Lie-Rinehart subalgebra of a Lie-Rinehart algebra `(R A L)` is an `A`-submodule of `L`, which
is stable under the Lie bracket. (This can be defined independently of `R` and most
Lie-Rinehart algebra axioms).  -/
LieRinehartSubalgebra : (A : Type u_1) → (L : Type u_2) → [inst : CommRing A] → [inst_1 : LieRing L] → [Module A L] → Type u_2
-- Mathlib.RingTheory.PowerSeries.Binomial
/-- The power series for `(1 + X) ^ r`.  -/
PowerSeries.binomialSeries : {R : Type u_1} → [inst : CommRing R] → [BinomialRing R] → (A : Type u_3) → [One A] → [SMul R A] → R → PowerSeries A
-- Lean.EnvExtension
Lean.TagDeclarationExtension.isTagged : (ext : Lean.TagDeclarationExtension) →
  Lean.Environment → Lean.Name → optParam Lean.EnvExtension.AsyncMode ext.toEnvExtension.asyncMode → Bool