mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.Ring.Constructions
CommRingCat.equalizer_limit_isLocalRing : ∀ (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair CommRingCat)
  [IsLocalRing ↑(F.obj CategoryTheory.Limits.WalkingParallelPair.zero)], IsLocalRing ↑(CategoryTheory.Limits.limit F)
-- Mathlib.Topology.Constructions
Filter.Tendsto.apply_nhds : ∀ {Y : Type v} {ι : Type u_5} {A : ι → Type u_6} [T : (i : ι) → TopologicalSpace (A i)] {l : Filter Y}
  {f : Y → (i : ι) → A i} {x : (i : ι) → A i},
  Filter.Tendsto f l (nhds x) → ∀ (i : ι), Filter.Tendsto (fun a => f a i) l (nhds (x i))
-- Std.Time.Duration
/-- Converts a `Duration` to a `Minute.Offset`
 -/
Std.Time.Duration.toMinutes : Std.Time.Duration → Std.Time.Minute.Offset
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupNorm.instOneOfDecidableEq : {E : Type u_3} → [inst : AddGroup E] → [DecidableEq E] → One (NonarchAddGroupNorm E)
-- Mathlib.Probability.Kernel.Composition.Prod
ProbabilityTheory.Kernel.map_prod_map : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {δ : Type u_5}
  {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} {ε : Type u_6} {mε : MeasurableSpace ε}
  (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel α δ)
  [ProbabilityTheory.IsSFiniteKernel η] {f : β → γ},
  Measurable f → ∀ {g : δ → ε}, Measurable g → (κ.map f).prod (η.map g) = (κ.prod η).map (Prod.map f g)
-- Mathlib.RingTheory.Unramified.Locus
Algebra.unramifiedLocus_eq_compl_support : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  Algebra.unramifiedLocus R A = (Module.support A Ω[A⁄R])ᶜ
-- ProofWidgets.Component.HtmlDisplay
ProofWidgets.HtmlCommand.evalCommandMHtmlUnsafe : Lean.Term → Lean.Elab.TermElabM (Lean.Elab.Command.CommandElabM ProofWidgets.Html)
-- Mathlib.Algebra.Ring.Int.Parity
Int.odd_mul : ∀ {m n : ℤ}, Odd (m * n) ↔ Odd m ∧ Odd n
-- Init.Data.UInt.Lemmas
UInt8.toNat_ofNat : ∀ {n : ℕ}, (OfNat.ofNat n).toNat = n % 2 ^ 8
-- Mathlib.Logic.Equiv.List
_private.Mathlib.Logic.Equiv.List.0.Encodable.decodeList.match_3.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (v : ℕ) → motive v.succ),
  (match 0 with
    | 0 => h_1 ()
    | v.succ => h_2 v) =
    h_1 ()
-- Mathlib.ModelTheory.Algebra.Field.Basic
FirstOrder.Language.Theory.field.eq_1 : FirstOrder.Language.Theory.field = Set.range FirstOrder.Field.FieldAxiom.toSentence
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.nnnorm_eq_sup_normAtPlace : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : NumberField.mixedEmbedding.mixedSpace K),
  ‖x‖₊ = Finset.univ.sup fun w => NNReal.mk ((NumberField.mixedEmbedding.normAtPlace w) x) ⋯
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.rightHomologyMapIso'_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData),
  (CategoryTheory.ShortComplex.rightHomologyMapIso' e h₁ h₂).inv =
    CategoryTheory.ShortComplex.rightHomologyMap' e.inv h₂ h₁
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.vaddCommClass : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : DecidableEq γ] [inst_1 : VAdd α γ] [inst_2 : VAdd β γ]
  [VAddCommClass α β γ], VAddCommClass (Finset α) (Finset β) (Finset γ)
-- Std.Data.DTreeMap.Lemmas
/-- Variant of `getD_map` that holds without `LawfulEqCmp`.  -/
Std.DTreeMap.Const.getD_map' : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {f : α → β → γ} {k : α} {fallback : γ},
  Std.DTreeMap.Const.getD (Std.DTreeMap.map f t) k fallback =
    (Option.pmap (fun v h => f (t.getKey k h) v) (Std.DTreeMap.Const.get? t k) ⋯).getD fallback
-- Lean.PrettyPrinter.Delaborator.SubExpr
Lean.PrettyPrinter.Delaborator.SubExpr.withLetVarType : {α : Type} →
  [Inhabited α] →
    {m : Type → Type} → [Monad m] → [MonadReaderOf Lean.SubExpr m] → [MonadWithReaderOf Lean.SubExpr m] → m α → m α
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
/-- **Alias** of `WithSeminorms.continuous_normedSpace_dom`. -/
Seminorm.cont_normedSpace_to_withSeminorms : ∀ {𝕝 : Type u_4} {𝕝₂ : Type u_5} {F : Type u_7} {ι : Type u_9} [inst : NormedField 𝕝] [inst_1 : AddCommGroup F]
  [inst_2 : NormedField 𝕝₂] [inst_3 : Module 𝕝₂ F] {τ₁₂ : 𝕝 →+* 𝕝₂} [inst_4 : RingHomIsometric τ₁₂] (E : Type u_11)
  [inst_5 : SeminormedAddCommGroup E] [inst_6 : NormedSpace 𝕝 E] [inst_7 : TopologicalSpace F] {q : ι → Seminorm 𝕝₂ F},
  WithSeminorms q → ∀ (f : E →ₛₗ[τ₁₂] F), (∀ (i : ι), ∃ C, (q i).comp f ≤ C • normSeminorm 𝕝 E) → Continuous ⇑f
-- Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
/-- A morphism of schemes `f : X ⟶ Y` is a preimmersion if the underlying map of
topological spaces is an embedding and the induced morphisms of stalks are all surjective.  -/
AlgebraicGeometry.IsPreimmersion : {X Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → Prop
-- Mathlib.MeasureTheory.Measure.Tilted
MeasureTheory.rnDeriv_tilted_right : ∀ {α : Type u_1} {mα : MeasurableSpace α} {f : α → ℝ} (μ ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ]
  [MeasureTheory.SigmaFinite ν],
  MeasureTheory.Integrable (fun x => Real.exp (f x)) ν →
    μ.rnDeriv (ν.tilted f) =ᵐ[ν] fun x =>
      ENNReal.ofReal (Real.exp (-f x) * ∫ (x : α), Real.exp (f x) ∂ν) * μ.rnDeriv ν x
-- Mathlib.SetTheory.ZFC.Ordinal
/-- A transitive set is one where every element is a subset.

This is equivalent to being an infinite-open interval in the transitive closure of membership.  -/
ZFSet.IsTransitive : ZFSet.{u_1} → Prop
-- Mathlib.Data.ENNReal.Basic
ENNReal.coe_pow : ∀ (x : NNReal) (n : ℕ), ↑(x ^ n) = ↑x ^ n
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- The product functor can be decomposed.  -/
CategoryTheory.Limits.prod.functorLeftComp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasBinaryProducts C] →
      (X Y : C) →
        CategoryTheory.Limits.prod.functor.obj (X ⨯ Y) ≅
          (CategoryTheory.Limits.prod.functor.obj Y).comp (CategoryTheory.Limits.prod.functor.obj X)
-- Lean.Util.CollectMVars
Lean.CollectMVars.main : Lean.Expr → Lean.CollectMVars.Visitor
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.X_mul_inj : ∀ {R : Type u_1} [inst : Semiring R] {φ ψ : PowerSeries R}, PowerSeries.X * φ = PowerSeries.X * ψ ↔ φ = ψ
-- Mathlib.Dynamics.FixedPoints.Support
_private.Mathlib.Dynamics.FixedPoints.Support.0.Function.fixedSupport.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] (f : X → X), Function.fixedSupport f = closure (Function.fixedPoints f)ᶜ
-- Mathlib.Combinatorics.SetFamily.Compression.Down
Finset.memberSubfamily_image_insert : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {a : α},
  (∀ s ∈ 𝒜, a ∉ s) → Finset.memberSubfamily a (Finset.image (insert a) 𝒜) = 𝒜
-- Mathlib.Algebra.Homology.ExactSequence
CategoryTheory.ShortComplex.isComplex_toComposableArrows : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C), S.toComposableArrows.IsComplex
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
ContinuousLinearMap.smul_compLpL : ∀ {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] {𝕜 : Type u_6} {𝕜' : Type u_7}
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜'] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedSpace 𝕜' F] {σ : 𝕜 →+* 𝕜'} [inst_6 : RingHomIsometric σ] [inst_7 : Fact (1 ≤ p)] {𝕜'' : Type u_8}
  [inst_8 : NormedRing 𝕜''] [inst_9 : Module 𝕜'' F] [inst_10 : IsBoundedSMul 𝕜'' F] [inst_11 : SMulCommClass 𝕜' 𝕜'' F]
  (c : 𝕜'') (L : E →SL[σ] F), ContinuousLinearMap.compLpL p μ (c • L) = c • ContinuousLinearMap.compLpL p μ L
-- Mathlib.LinearAlgebra.Prod
/-- Split equality of linear maps from a product into linear maps over each component, to allow `ext`
to apply lemmas specific to `M →ₗ M₃` and `M₂ →ₗ M₃`.

See note [partially-applied ext lemmas].  -/
LinearMap.prod_ext : ∀ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module R M₂]
  [inst_6 : Module R M₃] {f g : M × M₂ →ₗ[R] M₃},
  f ∘ₗ LinearMap.inl R M M₂ = g ∘ₗ LinearMap.inl R M M₂ → f ∘ₗ LinearMap.inr R M M₂ = g ∘ₗ LinearMap.inr R M M₂ → f = g
-- Mathlib.Order.Nucleus
Nucleus.instHImp : {X : Type u_1} → [inst : Order.Frame X] → HImp (Nucleus X)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.ValueGroupWithZero.mk_self : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] (x : ↥(ValuativeRel.posSubmonoid R)),
  ValuativeRel.ValueGroupWithZero.mk (↑x) x = 1
-- Init.Prelude
/-- The second element of a pair.  -/
PProd.snd : {α : Sort u} → {β : Sort v} → α ×' β → β
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
/-- Conditional Jensen's inequality for hereditarily Lindelof Spaces.  -/
_private.Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen.0.ConvexOn.map_condExp_le_of_hereditarilyLindelofSpace : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {α : Type u_2} {f : α → E}
  {φ : E → ℝ} {m mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set E} [MeasureTheory.IsFiniteMeasure μ]
  [HereditarilyLindelofSpace E],
  m ≤ mα →
    ConvexOn ℝ s φ →
      LowerSemicontinuousOn φ s →
        (∀ᵐ (a : α) ∂μ, f a ∈ s) →
          IsClosed s →
            MeasureTheory.Integrable f μ →
              MeasureTheory.Integrable (φ ∘ f) μ → ∀ᵐ (a : α) ∂μ, φ (μ[f | m] a) ≤ μ[φ ∘ f | m] a
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.equiv_of_forall_getKey?_unit_eq : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => Unit},
  (↑m₁).WF → (↑m₂).WF → (∀ (k : α), m₁.getKey? k = m₂.getKey? k) → (↑m₁).Equiv ↑m₂
-- Mathlib.Analysis.RCLike.Inner
/-- Weighted inner product giving rise to the L2 norm, denoted as `⟪g, f⟫_[𝕜, w]`.  -/
RCLike.«term⟪_,_⟫_[_,_]» : Lean.ParserDescr
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe.congr_simp : ∀ {X : Type u_1} [inst : TopologicalSpace X] (s : TopologicalSpace.Opens X) (hs : Nonempty ↥s),
  s.openPartialHomeomorphSubtypeCoe hs = s.openPartialHomeomorphSubtypeCoe hs
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
CategoryTheory.Limits.IsIndObject.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
  (P : CategoryTheory.Limits.IndObjectPresentation A), CategoryTheory.Limits.IsIndObject A
-- Mathlib.Probability.HasLaw
ProbabilityTheory.indepFun_iff_hasLaw_prodMk_prod : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {X : Ω → 𝓧}
  {μ : MeasureTheory.Measure 𝓧} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {𝓨 : Type u_3}
  {m𝓨 : MeasurableSpace 𝓨} {ν : MeasureTheory.Measure 𝓨} {Y : Ω → 𝓨},
  ProbabilityTheory.HasLaw X μ P →
    ProbabilityTheory.HasLaw Y ν P →
      (ProbabilityTheory.IndepFun X Y P ↔ ProbabilityTheory.HasLaw (fun ω => (X ω, Y ω)) (μ.prod ν) P)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey!_modify_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF → ∀ [inst_1 : Inhabited α] {k : α} {f : β k → β k}, (t.modify k f).getKey! k = if k ∈ t then k else default
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.leftUnitor_inv_whiskerRight_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C) {Z : C}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj
        (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X) Y ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv Y)
      h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X Y).inv
        h)
-- Mathlib.Order.Hom.Basic
OrderEmbedding.id_toEmbedding : ∀ {α : Type u_2} [inst : LE α], (OrderEmbedding.id α).toEmbedding = Function.Embedding.refl α
-- Mathlib.NumberTheory.ModularForms.QExpansion
/-- **Alias** of `ModularForm.cuspFunction_sub`. -/
ModularFormClass.cuspFunction_sub : ∀ {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} {G : Type u_2}
  [inst_1 : FunLike G UpperHalfPlane ℂ],
  0 < h →
    h ∈ Γ.strictPeriods →
      ∀ {a b : ℤ} (f : F) [ModularFormClass F Γ a] (g : G) [ModularFormClass G Γ b],
        UpperHalfPlane.cuspFunction h (⇑f - ⇑g) = UpperHalfPlane.cuspFunction h ⇑f - UpperHalfPlane.cuspFunction h ⇑g
-- Mathlib.Analysis.Normed.Lp.LpEquiv
coe_addEquiv_lpBCF_symm : ∀ {α : Type u_1} {E : Type u_2} [inst : TopologicalSpace α] [inst_1 : DiscreteTopology α]
  [inst_2 : NormedAddCommGroup E] (f : BoundedContinuousFunction α E), ↑(AddEquiv.lpBCF.symm f) = ⇑f
-- Mathlib.Algebra.GCDMonoid.Multiset
Multiset.gcd_union : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] [inst_2 : DecidableEq α]
  (s₁ s₂ : Multiset α), (s₁ ∪ s₂).gcd = gcd s₁.gcd s₂.gcd
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getD_alter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k k' : α} {fallback : β} {f : Option β → Option β},
      Std.DTreeMap.Raw.Const.getD (Std.DTreeMap.Raw.Const.alter t k f) k' fallback =
        if cmp k k' = Ordering.eq then (f (Std.DTreeMap.Raw.Const.get? t k)).getD fallback
        else Std.DTreeMap.Raw.Const.getD t k' fallback
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_inv_fac : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [inst : AlgebraicGeometry.IsOpenImmersion f]
  [inst_1 : AlgebraicGeometry.IsOpenImmersion g] (e : Set.range ⇑f = Set.range ⇑g),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq f g e).inv f = g
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
/-- **Alias** of the forward direction of `AddSubgroup.normal_op`. -/
AddSubgroup.Normal.of_op : ∀ {G : Type u_2} [inst : AddGroup G] {H : AddSubgroup G}, H.op.Normal → H.Normal
-- Mathlib.Tactic.Sat.FromLRAT
/-- A formula is a list of clauses, thought of as a conjunction like `(a ∨ b) ∧ c ∧ (¬c ∨ ¬d)`.  -/
Sat.Fmla : Type
-- Mathlib.Topology.Algebra.Group.Pointwise
subset_interior_div_left : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] {s t : Set G},
  interior s / t ⊆ interior (s / t)
-- Mathlib.Algebra.ContinuedFractions.Determinant
/-- The determinant formula `Aₙ * Bₙ₊₁ - Bₙ * Aₙ₊₁ = (-1) ^ (n + 1)` for `SimpContFract`.  -/
SimpContFract.determinant : ∀ {K : Type u_1} [inst : Field K] {s : SimpContFract K} {n : ℕ},
  ¬(↑s).TerminatedAt n → (↑s).nums n * (↑s).dens (n + 1) - (↑s).dens n * (↑s).nums (n + 1) = (-1) ^ (n + 1)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.piPiIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} (f : ι → Type u_2) (g : (i : ι) → f i → C)
  [inst_1 : ∀ (i : ι), CategoryTheory.Limits.HasProduct (g i)]
  [inst_2 : CategoryTheory.Limits.HasProduct fun i => ∏ᶜ g i],
  (CategoryTheory.Limits.piPiIso f g).hom =
    CategoryTheory.Limits.Pi.lift fun x =>
      match x with
      | ⟨i, x⟩ =>
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun i => ∏ᶜ g i) i)
          (CategoryTheory.Limits.Pi.π (g i) x)
-- Init.Data.List.ToArray
Array.flatMap_empty : ∀ {α : Type u_1} {β : Type u_2} (f : α → Array β), Array.flatMap f #[] = #[]
-- Lean.Elab.Binders
/-- Auxiliary function for expanding `fun` notation binders. Recall that `fun` parser is defined as
```
def funBinder : Parser := implicitBinder <|> instBinder <|> termParser maxPrec
leading_parser unicodeSymbol "λ" "fun" >> many1 funBinder >> "=>" >> termParser
```
to allow notation such as `fun (a, b) => a + b`, where `(a, b)` should be treated as a pattern.
The result is a pair `(explicitBinders, newBody)`, where `explicitBinders` is syntax of the form
```
`(` ident `:` term `)`
```
which can be elaborated using `elabBinders`, and `newBody` is the updated `body` syntax.
We update the `body` syntax when expanding the pattern notation.
Example: `fun (a, b) => a + b` expands into `fun _a_1 => match _a_1 with | (a, b) => a + b`.
See local function `processAsPattern` at `expandFunBindersAux`.

The resulting `Bool` is true if a pattern was found. We use it "mark" a macro expansion.  -/
Lean.Elab.Term.expandFunBinders : Array Lean.Syntax → Lean.Syntax → Lean.MacroM (Array Lean.Syntax × Lean.Syntax × Bool)
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.repr_fract_apply : ∀ {E : Type u_1} {ι : Type u_2} {K : Type u_3} [inst : NormedField K] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace K E] (b : Module.Basis ι K E) [inst_3 : LinearOrder K] [inst_4 : IsStrictOrderedRing K]
  [inst_5 : FloorRing K] [inst_6 : Fintype ι] (m : E) (i : ι), (b.repr (ZSpan.fract b m)) i = Int.fract ((b.repr m) i)
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- Reflecting limits at any universe implies reflecting limits at universe `0`.  -/
CategoryTheory.Limits.reflectsSmallestLimits_of_reflectsLimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsLimitsOfSize.{v₃, u₃, v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.ReflectsLimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F
-- Mathlib.CategoryTheory.Sites.CoverLifting
CategoryTheory.Functor.pushforwardContinuousSheafificationCompatibility_hom_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] (G : CategoryTheory.Functor C D) (A : Type w)
  [inst_2 : CategoryTheory.Category.{w', w} A] (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) [inst_3 : G.IsCocontinuous J K]
  [inst_4 : ∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] [inst_5 : G.IsContinuous J K]
  [inst_6 : CategoryTheory.HasWeakSheafify J A] [inst_7 : CategoryTheory.HasWeakSheafify K A]
  (F : CategoryTheory.Functor Dᵒᵖ A),
  ((G.pushforwardContinuousSheafificationCompatibility A J K).hom.app F).hom =
    CategoryTheory.sheafifyLift J (G.op.whiskerLeft (CategoryTheory.toSheafify K F)) ⋯
-- Mathlib.Topology.Order.MonotoneConvergence
Monotone.le_of_tendsto : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder α] [OrderClosedTopology α]
  [inst_3 : Preorder β] [IsCodirectedOrder β] {f : β → α} {a : α},
  Monotone f → Filter.Tendsto f Filter.atBot (nhds a) → ∀ (b : β), a ≤ f b
-- Mathlib.Topology.ClopenBox
TopologicalSpace.Clopens.surjective_finset_sup_prod : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [CompactSpace Y]
  [CompactSpace X], Function.Surjective fun I => I.sup fun i => i.1 ×ˢ i.2
-- Lean.Meta.Sym.DSimp.DSimpM
Lean.Meta.Sym.DSimp.Config.mk.sizeOf_spec : ∀ (maxSteps : ℕ), sizeOf { maxSteps := maxSteps } = 1 + sizeOf maxSteps
-- Mathlib.Analysis.Normed.Ring.WithAbs
/-- **Alias** of `WithAbs.instAlgebra`. -/
WithAbs.instAlgebra_right : {S : Type u_2} →
  [inst : Semiring S] →
    [inst_1 : PartialOrder S] →
      {R : Type u_3} →
        {T : Type u_4} →
          [inst_2 : CommSemiring R] →
            [inst_3 : Semiring T] → [Algebra R T] → (v : AbsoluteValue T S) → Algebra R (WithAbs v)
-- Mathlib.Analysis.SpecialFunctions.Bernstein
bernsteinApproximation.apply : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E] [inst_2 : IsTopologicalAddGroup E]
  [inst_3 : Module ℝ E] [inst_4 : ContinuousSMul ℝ E] (n : ℕ) (f : C(↑unitInterval, E)) (x : ↑unitInterval),
  (bernsteinApproximation n f) x = ∑ k, (bernstein n ↑k) x • f (bernstein.z k)
-- Mathlib.Topology.Order.IntermediateValue
IsPreconnected.intermediate_value_Iio : ∀ {X : Type u} {α : Type v} [inst : TopologicalSpace X] [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α]
  [OrderClosedTopology α] {s : Set X},
  IsPreconnected s →
    ∀ {l₁ l₂ : Filter X} [l₁.NeBot] [l₂.NeBot],
      l₁ ≤ Filter.principal s →
        l₂ ≤ Filter.principal s →
          ∀ {f : X → α},
            ContinuousOn f s →
              ∀ {v : α}, Filter.Tendsto f l₁ Filter.atBot → Filter.Tendsto f l₂ (nhds v) → Set.Iio v ⊆ f '' s
-- Mathlib.Probability.Kernel.Integral
ProbabilityTheory.Kernel.integral_indicator₂ : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (f : α → β → E) (s : Set α) (a : α),
  ∫ (y : β), s.indicator (fun x => f x y) a ∂κ a = s.indicator (fun x => ∫ (y : β), f x y ∂κ x) a
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- The `Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat_left`
for commutative rings.  -/
Submodule.LinearDisjoint.rank_inf_le_one_of_flat_left : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {M N : Submodule R S},
  M.LinearDisjoint N → ∀ [Module.Flat R ↥M], Module.rank R ↥(M ⊓ N) ≤ 1
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.mapEquiv_apply : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  {P' : Type u_3} [inst_3 : CommRing P'] [inst_4 : Algebra R P'] (g : P ≃ₐ[R] P') (I : FractionalIdeal S P),
  (FractionalIdeal.mapEquiv g) I = FractionalIdeal.map (↑g) I
-- Mathlib.Topology.UniformSpace.UniformConvergence
/-- A sequence of functions `Fₙ` converges uniformly on a set `s` to a limiting function `f` with
respect to the filter `p` if, for any entourage of the diagonal `u`, one has `p`-eventually
`(f x, Fₙ x) ∈ u` for all `x ∈ s`.  -/
TendstoUniformlyOn : {α : Type u_1} → {β : Type u_2} → {ι : Type u_4} → [UniformSpace β] → (ι → α → β) → (α → β) → Filter ι → Set α → Prop
-- Mathlib.RingTheory.RootsOfUnity.Basic
MulEquiv.restrictRootsOfUnity_symm : ∀ {R : Type u_4} {S : Type u_5} {k : ℕ} [inst : CommMonoid R] [inst_1 : CommMonoid S] (σ : R ≃* S),
  (σ.restrictRootsOfUnity k).symm = σ.symm.restrictRootsOfUnity k
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.ones_blocksFun : ∀ (n : ℕ) (i : Fin (Composition.ones n).length), (Composition.ones n).blocksFun i = 1
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.actRight_one_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {A B : CategoryTheory.Mon C} (self : Bimod A B) {Z : C} (h : self.X ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft self.X CategoryTheory.MonObj.one)
      (CategoryTheory.CategoryStruct.comp self.actRight h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor self.X).hom h
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.get_inter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {h_mem : k ∈ m₁ ∩ m₂}, (m₁ ∩ m₂).get k h_mem = m₁.get k ⋯