mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.Measure.FiniteAtFilter.integrableAtFilter_of_tendsto_ae : ∀ {α : Type u_1} {E : Type u_5} {mα : MeasurableSpace α} [inst : NormedAddCommGroup E] {μ : MeasureTheory.Measure α}
  {f : α → E} {l : Filter α} [l.IsMeasurablyGenerated],
  StronglyMeasurableAtFilter f l μ →
    μ.FiniteAtFilter l →
      ∀ {b : E}, Filter.Tendsto f (l ⊓ MeasureTheory.ae μ) (nhds b) → MeasureTheory.IntegrableAtFilter f l μ
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.IsIndContained.isContained : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W}, G.IsIndContained H → G.IsContained H
-- Mathlib.Topology.IsLocalHomeomorph
IsLocalHomeomorphOn.map_nhds_eq : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set X},
  IsLocalHomeomorphOn f s → ∀ {x : X}, x ∈ s → Filter.map f (nhds x) = nhds (f x)
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.uIoo_comm : ∀ {α : Type u_1} [inst : LinearOrder α] (a b : α), Set.uIoo a b = Set.uIoo b a
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey_minKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {hc : t.minKey! ∈ t}, t.getKey t.minKey! hc = t.minKey!
-- Mathlib.RingTheory.Artinian.Module
/-- For any endomorphism of an Artinian module, any sufficiently high iterate has codisjoint kernel
and range.  -/
LinearMap.eventually_codisjoint_ker_pow_range_pow : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsArtinian R M]
  (f : Module.End R M), ∀ᶠ (n : ℕ) in Filter.atTop, Codisjoint (f ^ n).ker (f ^ n).range
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.List.findSomeM?.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : (b : β) → motive (some b)) (h_2 : Unit → motive none),
  (match none with
    | some b => h_1 b
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Topology.DenseEmbedding
Dense.continuous_extend : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : Set α} {f : ↑s → β}
  [T3Space β] (hs : Dense s),
  (∀ (a : α), ∃ b, Filter.Tendsto f (Filter.comap Subtype.val (nhds a)) (nhds b)) → Continuous (hs.extend f)
-- Mathlib.Algebra.CharP.Basic
ULift.charP : ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [CharP R p], CharP (ULift.{u_2, u_1} R) p
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
max_div_min_eq_mabs' : ∀ {α : Type u_1} [inst : Group α] [inst_1 : LinearOrder α] [MulLeftMono α] [MulRightMono α] (a b : α),
  max a b / min a b = |a / b|ₘ
-- Batteries.Data.AssocList
/-- `O(n)`. Map a function `f` over the values of the list.  -/
Batteries.AssocList.mapVal : {α : Type u_1} → {β : Type u_2} → {δ : Type u_3} → (α → β → δ) → Batteries.AssocList α β → Batteries.AssocList α δ
-- Init.Grind.Module.Envelope
_private.Init.Grind.Module.Envelope.0.Lean.Grind.IntModule.OfNatModule.toQ.eq_1 : ∀ {α : Type u} [inst : Lean.Grind.NatModule α] (a : α),
  Lean.Grind.IntModule.OfNatModule.toQ a = Lean.Grind.IntModule.OfNatModule.Q.mk (a, 0)
-- Mathlib.Data.Set.Lattice.Image
Set.biInter_image2 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (s : Set α) (t : Set β) (f : α → β → γ) (g : γ → Set δ),
  ⋂ c ∈ Set.image2 f s t, g c = ⋂ a ∈ s, ⋂ b ∈ t, g (f a b)
-- Init.Data.Float.Float32
/-- Splits the given float `x` into a significand/exponent pair `(s, i)` such that `x = s * 2^i` where
`s ∈ (-1;-0.5] ∪ [0.5; 1)`. Returns an undefined value if `x` is not finite.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`frexp`.
 -/
Float32.frExp : Float32 → Float32 × ℤ
-- Mathlib.NumberTheory.Dioph
/-- The `i`th projection function, `x_i`.  -/
Poly.proj : {α : Type u_1} → α → Poly α
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePushoutShape.mkCocone_pt : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor (CategoryTheory.Limits.WidePushoutShape J) C} {X : C} (f : F.obj none ⟶ X)
  (ι : (j : J) → F.obj (some j) ⟶ X)
  (w :
    ∀ (j : J),
      CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.WidePushoutShape.Hom.init j)) (ι j) = f),
  (CategoryTheory.Limits.WidePushoutShape.mkCocone f ι w).pt = X
-- Mathlib.CategoryTheory.Limits.Types.Equalizers
CategoryTheory.Limits.Types.equalizerIso_inv_comp_ι : ∀ {Y Z : Type u} (g h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.equalizerIso g h).inv
      (CategoryTheory.Limits.equalizer.ι g h) =
    TypeCat.ofHom Subtype.val
-- Mathlib.RingTheory.TensorProduct.Quotient
_private.Mathlib.RingTheory.TensorProduct.Quotient.0.Algebra.TensorProduct.quotIdealMapEquivTensorQuotAux_mk : ∀ {A : Type u_1} (B : Type u_2) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (I : Ideal A) (b : B),
  (Algebra.TensorProduct.quotIdealMapEquivTensorQuotAux B I) ((Ideal.Quotient.mk (Ideal.map (algebraMap A B) I)) b) =
    b ⊗ₜ[A] 1
-- Mathlib.NumberTheory.Harmonic.EulerMascheroni
Real.eulerMascheroniSeq'.eq_1 : ∀ (n : ℕ), Real.eulerMascheroniSeq' n = if n = 0 then 2 else ↑(harmonic n) - Real.log ↑n
-- Mathlib.Data.Set.Basic
Set.ofPred_subset : ∀ {α : Type u} {p : α → Prop} {s : Set α}, Set.ofPred p ⊆ s ↔ ∀ (x : α), p x → x ∈ s
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.recover'.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.RingTheory.Ideal.Prod
Ideal.prod_mono : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {I₁ I₂ : Ideal R} {J₁ J₂ : Ideal S},
  I₁ ≤ I₂ → J₁ ≤ J₂ → I₁.prod J₁ ≤ I₂.prod J₂
-- Mathlib.MeasureTheory.Measure.GiryMonad
MeasureTheory.Measure.measurable_measure : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : α → MeasureTheory.Measure β},
  Measurable μ ↔ ∀ (s : Set β), MeasurableSet s → Measurable fun b => (μ b) s
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.prod.unique : ∀ {α : Type u} [inst : Group α] (g : FreeGroup α →* α),
  (∀ (x : α), g (FreeGroup.of x) = x) → ∀ {x : FreeGroup α}, g x = FreeGroup.prod x
-- Mathlib.CategoryTheory.Sites.SheafOfTypes
/-- If `P` is separated and every compatible family of elements of `P` for a covering
sieve has an amalgamation, `P` is a sheaf.  -/
CategoryTheory.Presieve.IsSeparated.isSheaf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {P : CategoryTheory.Functor Cᵒᵖ (Type w)},
  CategoryTheory.Presieve.IsSeparated J P →
    (∀ (X : C),
        ∀ S ∈ J X,
          ∀ (x : CategoryTheory.Presieve.FamilyOfElements P S.arrows), x.Compatible → ∃ t, x.IsAmalgamation t) →
      CategoryTheory.Presieve.IsSheaf J P
-- Mathlib.Algebra.Category.MonCat.Adjunctions
MonCat.instIsRightAdjointForgetMonoidHomCarrier : (CategoryTheory.forget MonCat).IsRightAdjoint
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get?_diff_of_contains_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, m₂.contains k = true → Std.DHashMap.Internal.Raw₀.Const.get? (m₁.diff m₂) k = none
-- Mathlib.MeasureTheory.Function.Jacobian
/-- If a function is differentiable and injective on a measurable set `s`, then its restriction
to `s` is a measurable embedding.  -/
MeasureTheory.measurableEmbedding_of_fderivWithin : ∀ {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],
  MeasurableSet s → (∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) → Set.InjOn f s → MeasurableEmbedding (s.domRestrict f)
-- Init.Data.String.PosRaw
String.Pos.Raw.byteIdx_sub_char : ∀ {p : String.Pos.Raw} {c : Char}, (p - c).byteIdx = p.byteIdx - c.utf8Size
-- Aesop.Script.SpecificTactics
_private.Aesop.Script.SpecificTactics.0.Aesop.clearS.tacticBuilder : Lean.MVarId → Lean.FVarId → Lean.MVarId → Aesop.Script.TacticBuilder
-- Lean.Elab.Do.Control
_private.Lean.Elab.Do.Control.0.Lean.Elab.Do.ControlStack.optionT.stM : Lean.Elab.Do.MonadInfo → Lean.Expr → Lean.Expr
-- Mathlib.Algebra.Tropical.Basic
Tropical.untrop_lt_iff : ∀ {R : Type u} [inst : LT R] {x y : Tropical R}, Tropical.untrop x < Tropical.untrop y ↔ x < y
-- Mathlib.Algebra.Group.PUnit
PUnit.instMul_mathlib.eq_1 : PUnit.instMul_mathlib = { mul := fun x x_1 => PUnit.unit }
-- Std.Do.Triple.SpecLemmas
Std.Do.Iter.foldM_filterMapWithPostcondition : ∀ {ps : Std.Do.PostShape} {α β γ δ : Type w} {n : Type w → Type w''} {o : Type w → Type w'''}
  [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Monad n] [inst_3 : Monad o] [LawfulMonad n]
  [LawfulMonad o] [inst_6 : Std.Do.WPMonad o ps] [inst_7 : Std.IteratorLoop α Id n] [inst_8 : Std.IteratorLoop α Id o]
  [Std.LawfulIteratorLoop α Id n] [Std.LawfulIteratorLoop α Id o] [inst_11 : MonadLiftT n o] [LawfulMonadLiftT n o]
  {f : β → Std.Iterators.PostconditionT n (Option γ)} {g : δ → γ → o δ} {init : δ} {it : Std.Iter β}
  {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond δ ps},
  ⦃P⦄
      Std.Iter.foldM
        (fun d b => do
          let __x ← liftM (f b).run
          match __x with
            | some c => g d c
            | x => pure d)
        init it ⦃Q⦄ →
    ⦃P⦄ Std.IterM.foldM g init (Std.Iter.filterMapWithPostcondition f it) ⦃Q⦄
-- Mathlib.CategoryTheory.Monad.Comonadicity
/-- If `F` is comonadic, it creates limits of `F`-cosplit pairs. This is the "boring" direction of
Beck's comonadicity theorem, the converse is given in `comonadicOfCreatesFSplitEqualizers`.
 -/
CategoryTheory.Comonad.createsFSplitEqualizersOfComonadic : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          [CategoryTheory.ComonadicLeftAdjoint F] →
            ⦃A B : C⦄ →
              (f g : A ⟶ B) →
                [F.IsCosplitPair f g] → CategoryTheory.CreatesLimit (CategoryTheory.Limits.parallelPair f g) F
-- Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes
/-- Check that `e` is definitionally equal to `𝟙 a`.  -/
Mathlib.Tactic.Bicategory.id₁? : Lean.Expr → Mathlib.Tactic.Bicategory.BicategoryM (Option Mathlib.Tactic.BicategoryLike.Obj)
-- Std.Data.String.ToInt
String.Slice.toInt?_comp_copy : String.toInt? ∘ String.Slice.copy = String.Slice.toInt?
-- Lean.Environment
Lean.EnvExtension.AsyncMode.local.sizeOf_spec : sizeOf Lean.EnvExtension.AsyncMode.local = 1
-- Mathlib.NumberTheory.Dioph
/-- Diophantine functions are closed under multiplication.  -/
Dioph.mul_dioph : ∀ {α : Type} {f g : (α → ℕ) → ℕ}, Dioph.DiophFn f → Dioph.DiophFn g → Dioph.DiophFn fun v => f v * g v
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.Triplet.mk.inj : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} {x : ↥X} {y : ↥Y} {s : ↥S} {hx : f x = s} {hy : g y = s}
  {x_1 : ↥X} {y_1 : ↥Y} {s_1 : ↥S} {hx_1 : f x_1 = s_1} {hy_1 : g y_1 = s_1},
  { x := x, y := y, s := s, hx := hx, hy := hy } = { x := x_1, y := y_1, s := s_1, hx := hx_1, hy := hy_1 } →
    x = x_1 ∧ y = y_1 ∧ s = s_1
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakEqualizers
CategoryTheory.Limits.weakEqualizer.condition_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f g : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasWeakEqualizer f g] {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.weakEqualizer.ι f g)
      (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.weakEqualizer.ι f g)
      (CategoryTheory.CategoryStruct.comp g h)
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.uniqueBaseOn_self : ∀ {α : Type u_1} (I : Set α), Matroid.uniqueBaseOn I I = Matroid.freeOn I
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingIso.coe_ringEquiv_refl : ∀ (α : Type u_2) [inst : Mul α] [inst_1 : Add α] [inst_2 : LE α], (OrderRingIso.refl α).toRingEquiv = RingEquiv.refl α
-- Std.Tactic.BVDecide.LRAT.Actions
Std.Tactic.BVDecide.LRAT.Action.addRup.inj : ∀ {β : Type u} {α : Type v} {id : ℕ} {c : β} {rupHints : Array ℕ} {id_1 : ℕ} {c_1 : β} {rupHints_1 : Array ℕ},
  Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints = Std.Tactic.BVDecide.LRAT.Action.addRup id_1 c_1 rupHints_1 →
    id = id_1 ∧ c = c_1 ∧ rupHints = rupHints_1
-- Mathlib.Tactic.NormNum.Basic
Mathlib.Meta.NormNum.ne_of_true_of_false : ∀ {a b : Prop}, a → ¬b → a ≠ b
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.isPrimitive_one_level_zero : ∀ {R : Type u_1} [inst : CommMonoidWithZero R], DirichletCharacter.IsPrimitive 1
-- Mathlib.RepresentationTheory.Continuous.TopRep
TopRep.hom_add : ∀ {k : Type u} {G : Type v} [inst : TopologicalSpace k] [inst_1 : Ring k] [inst_2 : Monoid G] (A B : TopRep k G)
  (f g : A ⟶ B), TopRep.Hom.hom (f + g) = TopRep.Hom.hom f + TopRep.Hom.hom g
-- Mathlib.Topology.Algebra.Algebra
instContinuousMulElemIccOfNat : ∀ (A : Type u) [inst : Semiring A] [inst_1 : TopologicalSpace A] [inst_2 : PartialOrder A] [inst_3 : IsOrderedRing A]
  [ContinuousMul A], ContinuousMul ↑(Set.Icc 0 1)
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.canLift : ∀ {X : Type u_1}, CanLift (OnePoint X) X OnePoint.some fun x => x ≠ OnePoint.infty
-- Init.Data.Ord.Basic
List.compareLex_nil_cons : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x : α} {xs : List α}, List.compareLex cmp [] (x :: xs) = Ordering.lt
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- The type family of morphisms for the diagram indexing a wide (co)equalizer.  -/
CategoryTheory.Limits.WalkingParallelFamily.Hom : (J : Type w) → CategoryTheory.Limits.WalkingParallelFamily J → CategoryTheory.Limits.WalkingParallelFamily J → Type w
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.IsStableUnderTransfiniteComposition.shrink : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C)
  [W.IsStableUnderTransfiniteComposition] [UnivLE.{w, w'}], W.IsStableUnderTransfiniteComposition
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get?_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k a : α},
  (t.insert k).get? a = if cmp k a = Ordering.eq ∧ k ∉ t then some k else t.get? a
-- Mathlib.Analysis.Normed.Group.Constructions
MulOpposite.instNormedAddGroup : {E : Type u_2} → [NormedAddGroup E] → NormedAddGroup Eᵐᵒᵖ
-- Mathlib.GroupTheory.DoubleCoset
DoubleCoset.mk_out_eq_mul : ∀ {G : Type u_1} [inst : Group G] (H K : Subgroup G) (g : G),
  ∃ h k, h ∈ H ∧ k ∈ K ∧ Quotient.out (DoubleCoset.mk H K g) = h * g * k
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.event.sizeOf_spec : sizeOf Lean.Lsp.CompletionItemKind.event = 1
-- Mathlib.RingTheory.PowerSeries.Expand
PowerSeries.map_expand : ∀ {R : Type u_2} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] (p : ℕ) (hp : p ≠ 0) (f : R →+* S)
  (φ : PowerSeries R),
  (PowerSeries.map f) ((PowerSeries.expand p hp) φ) = (PowerSeries.expand p hp) ((PowerSeries.map f) φ)
-- Mathlib.Algebra.Group.Irreducible.Indecomposable
isMulIndecomposable_id_univ : ∀ {M : Type u_2} [inst : Monoid M] [Subsingleton Mˣ] {x : M},
  x ≠ 1 → (IsMulIndecomposable id Set.univ x ↔ Irreducible x)
-- Mathlib.GroupTheory.Rank
Group.rank.eq_1 : ∀ (G : Type u_1) [inst : Group G] [h : Group.FG G], Group.rank G = Nat.find ⋯
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.prodOpEquiv_unitIso_inv_app : ∀ (C : Type u₃) [inst : CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [inst_1 : CategoryTheory.Category.{v₄, u₄} D]
  (X : (C × D)ᵒᵖ), (CategoryTheory.prodOpEquiv C).unitIso.inv.app X = CategoryTheory.CategoryStruct.id X
-- Lean.Parser.Syntax
Lean.Parser.precedence : Lean.Parser.Parser
-- Init.SizeOf
EStateM.Result.error.sizeOf_spec : ∀ {ε σ α : Type u} [inst : SizeOf ε] [inst_1 : SizeOf σ] [inst_2 : SizeOf α] (a : ε) (a_1 : σ),
  sizeOf (EStateM.Result.error a a_1) = 1 + sizeOf a + sizeOf a_1
-- Mathlib.Tactic.Widget.StringDiagram
Mathlib.Tactic.Widget.StringDiagram.Node.atom.injEq : ∀ (a a_1 : Mathlib.Tactic.Widget.StringDiagram.AtomNode),
  (Mathlib.Tactic.Widget.StringDiagram.Node.atom a = Mathlib.Tactic.Widget.StringDiagram.Node.atom a_1) = (a = a_1)
-- Mathlib.RingTheory.PicardGroup
/-- If M is invertible, `rTensorHom M` admits an inverse.  -/
Module.Invertible.rTensorInv : {R : Type u} →
  {M : Type v} →
    {N : Type u_1} →
      (P : Type u_2) →
        (Q : Type u_3) →
          [inst : CommSemiring R] →
            [inst_1 : AddCommMonoid M] →
              [inst_2 : AddCommMonoid N] →
                [inst_3 : AddCommMonoid P] →
                  [inst_4 : AddCommMonoid Q] →
                    [inst_5 : Module R M] →
                      [inst_6 : Module R N] →
                        [inst_7 : Module R P] →
                          [inst_8 : Module R Q] →
                            (TensorProduct R M N ≃ₗ[R] R) →
                              (TensorProduct R P M →ₗ[R] TensorProduct R Q M) →ₗ[R] P →ₗ[R] Q
-- Std.Http.Data.Headers.Basic
/-- Checks whether a specific token is present in the `Connection` header value.
 -/
Std.Http.Header.Connection.containsToken : Std.Http.Header.Connection → String → Bool
-- Mathlib.Data.Vector.Basic
List.Vector.mk_toList : ∀ {α : Type u_1} {n : ℕ} (v : List.Vector α n) (h : v.toList.length = n), ⟨v.toList, h⟩ = v
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubMulAction.map_ofFixingSubgroupUnion_def : ∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {s t : Set α}
  (x : ↥(SubMulAction.ofFixingSubgroup M (s ∪ t))), ↑↑((SubMulAction.map_ofFixingSubgroupUnion M s t) x) = ↑x
-- Lean.Environment
_private.Lean.Environment.0.Lean.PersistentEnvExtension.getModuleIREntries.unsafe_impl_2 : {α β σ : Type} → [Inhabited σ] → Lean.PersistentEnvExtension α β σ → Lean.Environment → Lean.ModuleIdx → Array α
-- Lean.Data.JsonRpc
Lean.JsonRpc.Batch : Type
-- Mathlib.Probability.Kernel.CondDistrib
ProbabilityTheory.condDistrib_const : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_3 : MeasureTheory.IsFiniteMeasure μ] {mβ : MeasurableSpace β} (X : α → β) (c : Ω),
  ⇑(ProbabilityTheory.condDistrib (fun x => c) X μ) =ᵐ[MeasureTheory.Measure.map X μ]
    ⇑(ProbabilityTheory.Kernel.deterministic (fun x => c) ⋯)
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.Iter.foldM_filterWithPostcondition : ∀ {α β δ : Type w} {n : Type w → Type w'} {o : Type w → Type w''} {Pred EPred : Type w} [inst : Std.Iterator α Id β]
  [Std.Iterators.Finite α Id] [inst_2 : Monad n] [inst_3 : Monad o] [LawfulMonad n]
  [inst_5 : Std.Internal.Do.Assertion Pred] [inst_6 : Std.Internal.Do.Assertion EPred]
  [inst_7 : Std.Internal.Do.WPMonad o Pred EPred] [inst_8 : Std.IteratorLoop α Id n] [inst_9 : Std.IteratorLoop α Id o]
  [Std.LawfulIteratorLoop α Id n] [Std.LawfulIteratorLoop α Id o] [inst_12 : MonadLiftT n o] [LawfulMonadLiftT n o]
  {f : β → Std.Iterators.PostconditionT n (ULift.{w, 0} Bool)} {g : δ → β → o δ} {init : δ} {it : Std.Iter β} {P : Pred}
  {Q : δ → Pred} {eQ : EPred},
  ⦃ P ⦄
      Std.Iter.foldM
        (fun d b => do
          let __do_lift ← liftM (f b).run
          if __do_lift.down = true then g d b else pure d)
        init it ⦃
      Q; eQ ⦄ →
    ⦃ P ⦄ Std.IterM.foldM g init (Std.Iter.filterWithPostcondition f it) ⦃ Q; eQ ⦄
-- Lean.Elab.Binders
/-- Similar to `expandMatchAltsIntoMatch`, but supports an optional `where` clause.

Expand `matchAltsWhereDecls` into `let rec` + `match`-expression.
Example
```
| 0, true => ... f 0 ...
| i, _    => ... f i + g i ...
where
  f x := g x + 1

  g : Nat → Nat
    | 0   => 1
    | x+1 => f x
```
expands into
```
fun x_1 x_2 =>
  let rec
    f x := g x + 1,
    g : Nat → Nat
      | 0   => 1
      | x+1 => f x
  match x_1, x_2 with
  | 0, true => ... f 0 ...
  | i, _    => ... f i + g i ...
```
 -/
Lean.Elab.Term.expandMatchAltsWhereDecls : Lean.Syntax → Lean.Expr → Lean.Elab.TermElabM Lean.Syntax
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.universalMulHom.congr_simp : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {T : Type u_2}
  [inst_2 : Monoid T] (f f_1 : R →* T) (e_f : f = f_1) (fS fS_1 : ↥S →* Tˣ) (e_fS : fS = fS_1)
  (hf : ∀ (s : ↥S), f ↑s = ↑(fS s)),
  OreLocalization.universalMulHom f fS hf = OreLocalization.universalMulHom f_1 fS_1 ⋯
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.map_iSup : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type u_3}
  [inst_3 : Field K] [inst_4 : Algebra F K] {ι : Sort u_4} (f : E →ₐ[F] K) (s : ι → IntermediateField F E),
  IntermediateField.map f (iSup s) = ⨆ i, IntermediateField.map f (s i)
-- Mathlib.Analysis.Normed.Module.Alternating.Curry
/-- `ContinuousAlternatingMap.curryLeft` as a `LinearIsometry`.  -/
ContinuousAlternatingMap.curryLeftLI : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] → {n : ℕ} → E [⋀^Fin (n + 1)]→L[𝕜] F →ₗᵢ[𝕜] E →L[𝕜] E [⋀^Fin n]→L[𝕜] F
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.isUnit_primPart_C : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : NormalizedGCDMonoid R] (r : R), IsUnit (Polynomial.C r).primPart
-- Mathlib.Topology.Order.Hom.Esakia
instCoeTCPseudoEpimorphismOfPseudoEpimorphismClass : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : Preorder α] → [inst_2 : Preorder β] → [PseudoEpimorphismClass F α β] → CoeTC F (PseudoEpimorphism α β)
-- Mathlib.Algebra.FreeMonoid.Count
/-- `List.countP` lifted to free monoids  -/
FreeMonoid.countP' : {α : Type u_1} → (p : α → Prop) → [DecidablePred p] → FreeMonoid α → ℕ
-- Mathlib.CategoryTheory.Adjunction.Reflective
CategoryTheory.Functor.fullyFaithfulCancelRight.congr_simp : ∀ {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 G : CategoryTheory.Functor C D}
  (H : CategoryTheory.Functor D E) [inst_3 : H.Full] [inst_4 : H.Faithful] (comp_iso comp_iso_1 : F.comp H ≅ G.comp H),
  comp_iso = comp_iso_1 →
    CategoryTheory.Functor.fullyFaithfulCancelRight H comp_iso =
      CategoryTheory.Functor.fullyFaithfulCancelRight H comp_iso_1
-- Mathlib.Algebra.Group.Pi.Lemmas
SemiconjBy.pi : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → Mul (f i)] {x y z : (i : I) → f i},
  (∀ (i : I), SemiconjBy (x i) (y i) (z i)) → SemiconjBy x y z
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
/-- If `f : R → ℝ` is a nonnegative, multiplicatively bounded function, then
`seminormFromBounded' f x = 0` if and only if `f x = 0`.  -/
seminormFromBounded_eq_zero_iff : ∀ {R : Type u_1} [inst : CommRing R] {f : R → ℝ} {c : ℝ},
  0 ≤ f → (∀ (x y : R), f (x * y) ≤ c * f x * f y) → ∀ (x : R), seminormFromBounded' f x = 0 ↔ f x = 0
-- Mathlib.Order.RelClasses
instAntisymmLt : ∀ {α : Type u} [inst : Preorder α], Std.Antisymm fun x1 x2 => x1 < x2
-- Init.Data.String.Lemmas.Splits
String.splits_endPos_iff : ∀ {t₁ t₂ s : String}, s.endPos.Splits t₁ t₂ ↔ t₁ = s ∧ t₂ = ""
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.isTopCompl_comm : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} [ContinuousSub M], Submodule.IsTopCompl p q ↔ Submodule.IsTopCompl q p
-- Mathlib.Algebra.Ring.Divisibility.Basic
dvd_sub : ∀ {α : Type u_1} [inst : NonUnitalRing α] {a b c : α}, a ∣ b → a ∣ c → a ∣ b - c