mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.VectorBundle.ContinuousAlternatingMap
Bundle.Pretrivialization.continuousAlternatingMap.isLinear : ∀ {𝕜 : Type u_1} {ι : Type u_2} [inst : NontriviallyNormedField 𝕜] {B : Type u_3} [inst_1 : TopologicalSpace B]
  {F₁ : Type u_4} [inst_2 : NormedAddCommGroup F₁] [inst_3 : NormedSpace 𝕜 F₁] {E₁ : B → Type u_5}
  [inst_4 : (x : B) → AddCommGroup (E₁ x)] [inst_5 : (x : B) → Module 𝕜 (E₁ x)]
  [inst_6 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_6} [inst_7 : NormedAddCommGroup F₂]
  [inst_8 : NormedSpace 𝕜 F₂] {E₂ : B → Type u_7} [inst_9 : (x : B) → AddCommGroup (E₂ x)]
  [inst_10 : (x : B) → Module 𝕜 (E₂ x)] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_12 : (x : B) → TopologicalSpace (E₁ x)] [inst_13 : FiberBundle F₁ E₁]
  [inst_14 : (x : B) → TopologicalSpace (E₂ x)] [inst_15 : FiberBundle F₂ E₂]
  {e₁ : Bundle.Trivialization F₁ Bundle.TotalSpace.proj} {e₂ : Bundle.Trivialization F₂ Bundle.TotalSpace.proj}
  [inst_16 : Bundle.Trivialization.IsLinear 𝕜 e₁] [inst_17 : Bundle.Trivialization.IsLinear 𝕜 e₂]
  [inst_18 : ∀ (x : B), ContinuousAdd (E₂ x)] [inst_19 : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)],
  Bundle.Pretrivialization.IsLinear 𝕜 (Bundle.Pretrivialization.continuousAlternatingMap 𝕜 ι e₁ e₂)
-- Lean.Elab.Tactic.BuiltinTactic
Lean.Elab.Tactic.evalSeq1 : Lean.Elab.Tactic.Tactic
-- Mathlib.Topology.Algebra.Module.Equiv
/-- The negation map as a continuous linear equivalence.  -/
ContinuousLinearEquiv.neg : (R : Type u_1) →
  [inst : Semiring R] →
    {M : Type u_2} →
      [inst_1 : TopologicalSpace M] → [inst_2 : AddCommGroup M] → [inst_3 : Module R M] → [ContinuousNeg M] → M ≃L[R] M
-- Mathlib.GroupTheory.OrderOfElement
injective_pow_iff_not_isOfFinOrder : ∀ {G : Type u_1} [inst : LeftCancelMonoid G] {x : G}, (Function.Injective fun n => x ^ n) ↔ ¬IsOfFinOrder x
-- Mathlib.Analysis.Convex.Side
Sbtw.sOppSide_of_notMem_of_mem : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y z : P}, Sbtw R x y z → x ∉ s → y ∈ s → s.SOppSide x z
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKeyD_filter_key : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {f : α → Bool} {k fallback : α},
  m.WF → (Std.HashMap.Raw.filter (fun k x => f k) m).getKeyD k fallback = (Option.filter f (m.getKey? k)).getD fallback
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.coeIdeal_mul : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  (I J : Ideal R), ↑(I * J) = ↑I * ↑J
-- Init.Data.List.Find
List.find?_cons_of_pos : ∀ {α : Type u_1} {p : α → Bool} {a : α} {l : List α}, p a = true → List.find? p (a :: l) = some a
-- Mathlib.Geometry.Manifold.Submersion
/-- A `C^n` submersion is `C^n`  -/
Manifold.IsSubmersionOfComplement.contMDiff : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {F : Type u_5} {H : Type u_7} {G : Type u_9} {E : Type u}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace 𝕜 F] [inst_7 : TopologicalSpace H] [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [inst_9 : TopologicalSpace M]
  [inst_10 : ChartedSpace H M] [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N},
  Manifold.IsSubmersionOfComplement F I J n f → ContMDiff I J n f
-- Mathlib.SetTheory.ZFC.Cardinal
ZFSet.card_insert_le : ∀ {x y : ZFSet.{u}}, (insert x y).card ≤ y.card + 1
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.End.instMonoidId.eq_1 : ∀ {M : Type u_2} {X : Type u_4} [inst : SMul M X],
  MulActionHom.End.instMonoidId =
    { mul := fun f g => f.comp g, mul_assoc := ⋯, one := MulActionHom.id M, one_mul := ⋯, mul_one := ⋯, npow_zero := ⋯,
      npow_succ := ⋯ }
-- Mathlib.Algebra.Lie.Graded
DirectSum.bracket_apply_apply : ∀ {ι : Type u_1} {R : Type u_3} {L : Type u_4} [inst : DecidableEq ι] [inst_1 : AddCommMonoid ι] [inst_2 : CommRing R]
  [inst_3 : LieRing L] [inst_4 : LieAlgebra R L] (ℒ : ι → Submodule R L) [inst_5 : GradedLieAlgebra ℒ]
  (x y : DirectSum ι fun i => ↥(ℒ i)),
  ⁅x, y⁆ =
    (DirectSum.decomposeLinearEquiv ℒ)
      ⁅(DirectSum.decomposeLinearEquiv ℒ).symm x, (DirectSum.decomposeLinearEquiv ℒ).symm y⁆
-- Mathlib.MeasureTheory.Measure.Dirac
/-- Dirac delta measures at two points are different if and only if there is a measurable set
containing one of the points but not the other.  -/
MeasureTheory.dirac_ne_dirac_iff_exists_measurableSet : ∀ {α : Type u_1} [inst : MeasurableSpace α] {x y : α},
  MeasureTheory.Measure.dirac x ≠ MeasureTheory.Measure.dirac y ↔ ∃ A, MeasurableSet A ∧ x ∈ A ∧ y ∉ A
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Complex.measurable_sinh : Measurable Complex.sinh
-- Mathlib.MeasureTheory.Integral.Lebesgue.Add
/-- **Alias** of `MeasureTheory.lintegral_finsetSum`. -/
MeasureTheory.lintegral_finset_sum : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Finset β)
  {f : β → α → ENNReal}, (∀ b ∈ s, Measurable (f b)) → ∫⁻ (a : α), ∑ b ∈ s, f b a ∂μ = ∑ b ∈ s, ∫⁻ (a : α), f b a ∂μ
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.ZeroHypercover.isoMk_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C}
  {E F : J.ZeroHypercover S} (e : E.toPreZeroHypercover ≅ F.toPreZeroHypercover),
  (CategoryTheory.Precoverage.ZeroHypercover.isoMk e).hom = e.hom
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
/-- The short complex `T.obj₁ ⟶ T.obj₂ ⟶ T.obj₃` attached to a distinguished triangle.  -/
CategoryTheory.Pretriangulated.shortComplexOfDistTriangle : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.HasShift C ℤ] →
        [inst_3 : CategoryTheory.Preadditive C] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [hC : CategoryTheory.Pretriangulated C] →
              (T : CategoryTheory.Pretriangulated.Triangle C) →
                T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles → CategoryTheory.ShortComplex C
-- Mathlib.RingTheory.MvPowerSeries.Rename
/-- Implementation detail for `rename`. Use `MvPowerSeries.rename` instead.  -/
MvPowerSeries.renameFun : {σ : Type u_1} →
  {τ : Type u_2} →
    {R : Type u_4} → (f : σ → τ) → [Filter.TendstoCofinite f] → [Semiring R] → MvPowerSeries σ R → MvPowerSeries τ R
-- Mathlib.Topology.Category.TopCat.Basic
TopCat.hom_ext : ∀ {X Y : TopCat} {f g : X ⟶ Y}, TopCat.Hom.hom f = TopCat.Hom.hom g → f = g
-- Mathlib.RingTheory.Coalgebra.Quotient
Coalgebra.Quotient.counit_mk : ∀ {R : Type u_1} {C : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup C] [inst_2 : Module R C]
  [inst_3 : CoalgebraStruct R C] (I : Submodule R C) [inst_4 : I.IsCoideal] (x : C),
  CoalgebraStruct.counit (Submodule.Quotient.mk x) = CoalgebraStruct.counit x
-- Init.Grind.Interactive
/-- `(grindSeq)` runs the `grindSeq` in sequence on the current list of targets.
This is pure grouping with no added effects.  -/
Lean.Parser.Tactic.Grind.paren : Lean.ParserDescr
-- Mathlib.MeasureTheory.MeasurableSpace.PreorderRestrict
Preorder.measurable_frestrictLe : ∀ {α : Type u_1} [inst : Preorder α] {X : α → Type u_2} [inst_1 : (a : α) → MeasurableSpace (X a)]
  [inst_2 : LocallyFiniteOrderBot α] (a : α), Measurable (Preorder.frestrictLe a)
-- Mathlib.Data.Multiset.Basic
Multiset.strongDownwardInductionOn_eq : ∀ {α : Type u_1} {p : Multiset α → Sort u_3} (s : Multiset α) {n : ℕ}
  (H : (t₁ : Multiset α) → ({t₂ : Multiset α} → t₂.card ≤ n → t₁ < t₂ → p t₂) → t₁.card ≤ n → p t₁),
  (fun a => s.strongDownwardInductionOn H a) = H s fun {t} ht _h => t.strongDownwardInductionOn H ht
-- Init.Data.Cast
instCoeHTCTNatOfNatCast : {R : Type u_1} → [NatCast R] → CoeHTCT ℕ R
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
/-- Construct an iso in `TopModuleCat` from a continuous linear equiv.  -/
TopModuleCat.ofIso : {R : Type u} →
  [inst : Ring R] →
    [inst_1 : TopologicalSpace R] → {X Y : TopModuleCat R} → (↑X.toModuleCat ≃L[R] ↑Y.toModuleCat) → (X ≅ Y)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getD_modify_self : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} {k : α}
  {fallback : β} {f : β → β},
  Std.DTreeMap.Const.getD (Std.DTreeMap.Const.modify t k f) k fallback =
    (Option.map f (Std.DTreeMap.Const.get? t k)).getD fallback
-- Lean.Meta.Sym.Pattern
/-- Checks whether `e` satisfies the Miller pattern condition on its arguments.

Returns `true` if `e` is not an application, or `e` is an n-ary application `f a₁ ... aₙ`
where all arguments are pairwise distinct free variables that were introduced during the
current `isDefEqS` invocation (i.e., their declaration index is ≥ `lctxInitialNextIndex`).

This condition is essential for higher-order unification: when assigning a metavariable
`?m a₁ ... aₙ := rhs`, the Miller pattern restriction ensures there is a unique solution
`?m := fun x₁ ... xₙ => rhs[aᵢ/xᵢ]`. The index check ensures we only consider variables
bound by the binders being compared, not pre-existing free variables from the context.

Examples:
- `f x y z` where `x`, `y`, `z` are distinct, newly-introduced free variables → `true`
- `f x c z` where `c` is a constant → `false` (non-variable argument)
- `f x y x` → `false` (repeated variable)
- `f x y z` where `x` existed before `isDefEqS` was called → `false` (pre-existing variable)
- `f` (nullary) → `true`
 -/
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.isMillerPatternArgs : Lean.Expr → Lean.Meta.Sym.DefEqM✝ Bool
-- Mathlib.Algebra.Group.Hom.Defs
/-- Composition of monoid homomorphisms is associative.  -/
OneHom.comp_assoc : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_10} [inst : One M] [inst_1 : One N] [inst_2 : One P]
  [inst_3 : One Q] (f : OneHom M N) (g : OneHom N P) (h : OneHom P Q), (h.comp g).comp f = h.comp (g.comp f)
-- Batteries.Data.Vector.Basic
_private.Batteries.Data.Vector.Basic.0.Vector.scanrMFast.loop : {m : Type u_1 → Type u_2} →
  {α : Type u_3} →
    {β : Type u_1} →
      {n : ℕ} →
        [Monad m] →
          (α → β → m β) →
            Vector α n →
              β → (i n_usize : USize) → n_usize.toNat = n → i.toNat ≤ n → Vector β (n + 1) → m (Vector β (n + 1))
-- Mathlib.Order.Category.FinPartOrd
FinPartOrd.dualEquiv_counitIso : FinPartOrd.dualEquiv.counitIso =
  CategoryTheory.NatIso.ofComponents (fun X => FinPartOrd.Iso.mk (OrderIso.dualDual ↑X.toPartOrd))
    @FinPartOrd.dualEquiv._proof_2
-- Mathlib.Analysis.Convex.Function
/-- If a function is convex on `s`, it remains convex when precomposed by an affine map.  -/
ConvexOn.comp_affineMap : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {β : Type u_5} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜]
  [inst_2 : AddCommGroup E] [inst_3 : AddCommGroup F] [inst_4 : AddCommMonoid β] [inst_5 : PartialOrder β]
  [inst_6 : Module 𝕜 E] [inst_7 : Module 𝕜 F] [inst_8 : SMul 𝕜 β] {f : F → β} (g : E →ᵃ[𝕜] F) {s : Set F},
  ConvexOn 𝕜 s f → ConvexOn 𝕜 (⇑g ⁻¹' s) (f ∘ ⇑g)
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
WithBot.coe_sSup' : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SupSet α] {s : Set α},
  s.Nonempty → BddAbove s → ↑(sSup s) = sSup ((fun a => ↑a) '' s)
-- Batteries.Data.HashMap.Basic
/-- The number of buckets in the hash map.  -/
Batteries.HashMap.numBuckets : {α : Type u_1} → {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → Batteries.HashMap α β → ℕ
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.mapRingHom_single : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddMonoid M]
  (f : R →+* S) (a : M) (b : R),
  (AddMonoidAlgebra.mapRingHom M f) (AddMonoidAlgebra.single a b) = AddMonoidAlgebra.single a (f b)
-- Mathlib.AlgebraicGeometry.Sites.Representability
AlgebraicGeometry.Scheme.LocalRepresentability.glueData_t : ∀ {F : CategoryTheory.Sheaf AlgebraicGeometry.Scheme.zariskiTopology (Type u)} {ι : Type u}
  {X : ι → AlgebraicGeometry.Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.obj}
  (hf : ∀ (i : ι), AlgebraicGeometry.IsOpenImmersion.presheaf (f i)) (i j : ι),
  (AlgebraicGeometry.Scheme.LocalRepresentability.glueData hf).t i j = ⋯.symmetry ⋯
-- Mathlib.Order.Hom.Lattice
InfHom.mk : {α : Type u_6} →
  {β : Type u_7} →
    [inst : Min α] → [inst_1 : Min β] → (toFun : α → β) → (∀ (a b : α), toFun (a ⊓ b) = toFun a ⊓ toFun b) → InfHom α β
-- Mathlib.LinearAlgebra.Dual.Lemmas
Submodule.quotDualCoannihilatorToDual_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (W : Submodule R (Module.Dual R M)) (m : M) (w : ↥W),
  (W.quotDualCoannihilatorToDual (Submodule.Quotient.mk m)) w = ↑w m
-- Mathlib.Algebra.Polynomial.Lifts
/-- A polynomial lifts if and only if it can be lifted to a polynomial of the same degree.  -/
Polynomial.exists_degree_eq_of_mem_lifts : ∀ {R : Type u} [inst : Semiring R] {S : Type v} [inst_1 : Semiring S] {f : R →+* S} {p : Polynomial S},
  p ∈ Polynomial.lifts f → ∃ q, Polynomial.map f q = p ∧ q.degree = p.degree
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
AEMeasurable.iSup : ∀ {α : Type u_1} {δ : Type u_4} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α]
  {mδ : MeasurableSpace δ} [inst_2 : ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α]
  {ι : Sort u_5} {μ : MeasureTheory.Measure δ} [Countable ι] {f : ι → δ → α},
  (∀ (i : ι), AEMeasurable (f i) μ) → AEMeasurable (fun b => ⨆ i, f i b) μ
-- Mathlib.Topology.MetricSpace.IsometricSMul
Metric.preimage_add_left_closedBall : ∀ {G : Type v} [inst : AddGroup G] [inst_1 : PseudoMetricSpace G] [IsIsometricVAdd G G] (a b : G) (r : ℝ),
  (fun x => a + x) ⁻¹' Metric.closedBall b r = Metric.closedBall (-a + b) r
-- Mathlib.Order.Monotone.Basic
StrictAntiOn.lt_iff_gt : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  StrictAntiOn f s → ∀ {a b : α}, a ∈ s → b ∈ s → (f a < f b ↔ b < a)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RccSliceData.mk.inj : ∀ {α : Type u} {β : Type v} {inst : Ord α} {treeMap : Std.DTreeMap.Internal.Impl α fun x => β} {range : Std.Rcc α}
  {treeMap_1 : Std.DTreeMap.Internal.Impl α fun x => β} {range_1 : Std.Rcc α},
  { treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 } →
    treeMap = treeMap_1 ∧ range = range_1
-- Mathlib.Tactic.DeriveTraversable
/-- Make the new deriving handler depends on other deriving handlers.  -/
Mathlib.Deriving.Traversable.higherOrderDeriveHandler : Lean.Name →
  (Lean.MVarId → Lean.Elab.TermElabM Unit) →
    optParam (List Lean.Elab.DerivingHandler) [] →
      (optParam (Lean.Name → Lean.Expr → Lean.Elab.TermElabM Lean.Expr) fun n arg =>
          liftM (Lean.Meta.mkAppM n #[arg])) →
        Lean.Elab.DerivingHandler
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
/-- The canonical image of the `TensorAlgebra` in the `ExteriorAlgebra`, which maps
`TensorAlgebra.ι R x` to `ExteriorAlgebra.ι R x`.  -/
TensorAlgebra.toExterior : {R : Type u1} →
  [inst : CommRing R] →
    {M : Type u2} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → TensorAlgebra R M →ₐ[R] ExteriorAlgebra R M
-- Mathlib.Data.List.Cycle
Cycle.prev_reverse_eq_next : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Cycle α) (hs : s.Nodup) (x : α) (hx : x ∈ s),
  s.reverse.prev ⋯ x ⋯ = s.next hs x hx
-- Mathlib.Algebra.Group.Defs
zero_zsmul : ∀ {G : Type u_1} [inst : SubNegMonoid G] (a : G), 0 • a = 0
-- Lean.Parser.Syntax
Lean.Parser.Command.macro.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Homology.TotalComplexShift
HomologicalComplex₂.shiftFunctor₁XXIso.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (a x a' : ℤ) (h : a' = a + x) (b : ℤ),
  K.shiftFunctor₁XXIso a x a' h b = K.shiftFunctor₁XXIso a x a' h b
-- Mathlib.Analysis.SpecialFunctions.Complex.Analytic
AnalyticWithinAt.re_ofReal : ∀ {f : ℂ → ℂ} {s : Set ℝ} {x : ℝ},
  AnalyticWithinAt ℂ f (Complex.ofReal '' s) ↑x → AnalyticWithinAt ℝ (fun x => (f ↑x).re) s x
-- Mathlib.Probability.Distributions.Binomial
ProbabilityTheory.binomial_eq_sum_dirac : ∀ (n : ℕ) (p : ↑unitInterval),
  ProbabilityTheory.binomial n p =
    ∑ k ≤ n, ENNReal.ofReal (↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k)) • MeasureTheory.Measure.dirac k
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.joinpoint.injEq : ∀ (name : Lean.Name) (params : Array (Lean.Elab.Term.Do.Var × Bool)) (body k : Lean.Elab.Term.Do.Code)
  (name_1 : Lean.Name) (params_1 : Array (Lean.Elab.Term.Do.Var × Bool)) (body_1 k_1 : Lean.Elab.Term.Do.Code),
  (Lean.Elab.Term.Do.Code.joinpoint name params body k = Lean.Elab.Term.Do.Code.joinpoint name_1 params_1 body_1 k_1) =
    (name = name_1 ∧ params = params_1 ∧ body = body_1 ∧ k = k_1)
-- Init.Data.UInt.Bitwise
UInt64.toUInt8_and : ∀ (a b : UInt64), (a &&& b).toUInt8 = a.toUInt8 &&& b.toUInt8
-- Mathlib.MeasureTheory.Function.EssSup
essSup_ennreal_smul_measure : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : ConditionallyCompleteLattice β] {c : ENNReal}, c ≠ 0 → ∀ (f : α → β), essSup f (c • μ) = essSup f μ
-- Mathlib.Algebra.GradedMonoid
SetLike.IsHomogeneousElem.mul : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : SetLike S R] [inst_1 : Add ι] [inst_2 : Mul R] {A : ι → S}
  [SetLike.GradedMul A] {a b : R},
  SetLike.IsHomogeneousElem A a → SetLike.IsHomogeneousElem A b → SetLike.IsHomogeneousElem A (a * b)
-- Mathlib.Topology.CompactOpen
/-- The compact-open topology on `C(X, Y)`
is equal to the infimum of the compact-open topologies on `C(s, Y)` for `s` a compact subset of `X`.
The key point of the proof is that for every compact set `K`,
the universal set `Set.univ : Set K` is a compact set as well.  -/
ContinuousMap.compactOpen_eq_iInf_induced : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  ContinuousMap.compactOpen =
    ⨅ K, ⨅ (_ : IsCompact K), TopologicalSpace.induced (ContinuousMap.restrict K) ContinuousMap.compactOpen
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.addCancelCommMonoid.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : AddCancelCommMonoid M] {S : AddSubmonoid M} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N), f.addCancelCommMonoid = { toAddCommMonoid := inst_1, toIsLeftCancelAdd := ⋯ }
-- Mathlib.GroupTheory.Torsion
AddCommGroup.freeRank_def : ∀ (G : Type u_1) [inst : AddCommGroup G] [inst_1 : AddGroup.FG G],
  AddCommGroup.freeRank G = AddGroup.rank (G ⧸ AddCommGroup.torsion G)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.filter_equiv_self_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {f : α → β → Bool},
  (Std.DTreeMap.filter f t).Equiv t ↔ ∀ (k : α) (h : k ∈ t), f (t.getKey k h) (Std.DTreeMap.Const.get t k h) = true
-- Mathlib.CategoryTheory.Profunctor.Basic
CategoryTheory.Profunctor.ulift_obj_obj : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (P : CategoryTheory.Profunctor.{w, v₁, v₂, u₁, u₂} C D) (X : C) (X_1 : Dᵒᵖ),
  ((CategoryTheory.Profunctor.ulift.{w', w, v₁, v₂, u₁, u₂} P).obj X).obj X_1 = ULift.{w', w} ((P.obj X).obj X_1)
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
/-- **Alias** of the forward direction of `hasSumUniformlyOn_iff_tendstoUniformlyOn`. -/
HasSumUniformlyOn.tendstoUniformlyOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β}
  [inst_1 : UniformSpace α],
  HasSumUniformlyOn f g s → TendstoUniformlyOn (fun x1 x2 => ∑ i ∈ x1, f i x2) g Filter.atTop s
-- Mathlib.CategoryTheory.Limits.Types.Images
/-- the image of a morphism in Type is just `Set.range f`  -/
CategoryTheory.Limits.Types.Image : {α β : Type u} → (α ⟶ β) → Type u
-- Mathlib.CategoryTheory.Presentable.Directed
/-- the morphisms which belong to the diagram  -/
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.W : {J : Type w} →
  [inst : CategoryTheory.SmallCategory J] →
    {κ : Cardinal.{w}} →
      CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ → CategoryTheory.MorphismProperty J
-- Mathlib.LinearAlgebra.Finsupp.Supported
/-- An equivalence of sets induces a linear equivalence of `Finsupp`s supported on those sets.  -/
Finsupp.congr : {α : Type u_1} →
  {M : Type u_2} →
    {R : Type u_5} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            {α' : Type u_7} →
              (s : Set α) → (t : Set α') → ↑s ≃ ↑t → ↥(Finsupp.supported M R s) ≃ₗ[R] ↥(Finsupp.supported M R t)
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
MeasureTheory.VectorMeasure.variation_restrict : ∀ {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [inst : TopologicalSpace V] [inst_1 : ENormedAddCommMonoid V]
  [inst_2 : T2Space V] {μ : MeasureTheory.VectorMeasure X V} {s : Set X},
  MeasurableSet s → (μ.restrict s).variation = μ.variation.restrict s
-- Mathlib.Order.Filter.Germ.Basic
Filter.Tendsto.congr_germ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f g : β → γ} {l : Filter α} {l' : Filter β},
  f =ᶠ[l'] g → ∀ {φ : α → β}, Filter.Tendsto φ l l' → ↑(f ∘ φ) = ↑(g ∘ φ)
-- Lean.Meta.Sym.Canon
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.ShouldCanonResult.visit : Lean.Meta.Sym.Canon.ShouldCanonResult✝
-- Mathlib.Analysis.Normed.Operator.NormedSpace
LinearIsometry.nnnorm_toContinuousLinearMap : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_3} {E : Type u_5} {F : Type u_6} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [NontrivialTopology E]
  [inst_7 : RingHomIsometric σ₁₂] (f : E →ₛₗᵢ[σ₁₂] F), ‖f.toContinuousLinearMap‖₊ = 1
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.maxKeyD_modify : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {f : β → β},
      (Std.DTreeMap.Raw.Const.modify t k f).isEmpty = false →
        ∀ {fallback : α},
          (Std.DTreeMap.Raw.Const.modify t k f).maxKeyD fallback =
            if cmp (t.maxKeyD fallback) k = Ordering.eq then k else t.maxKeyD fallback
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.nsmul_eq_empty : ∀ {α : Type u_2} [inst : AddMonoid α] {s : Set α} {n : ℕ}, n • s = ∅ ↔ s = ∅ ∧ n ≠ 0
-- Mathlib.Topology.Bornology.Absorbs
/-- A set is *absorbent* if it absorbs every singleton.  -/
Absorbent : (M : Type u_1) → {α : Type u_2} → [Bornology M] → [SMul M α] → Set α → Prop
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp₁.mkIso_inv : ∀ {M N : SemiNormedGrp} (f : M ≅ N) (i : (SemiNormedGrp.Hom.hom f.hom).NormNoninc)
  (i' : (SemiNormedGrp.Hom.hom f.inv).NormNoninc),
  (SemiNormedGrp₁.mkIso f i i').inv = SemiNormedGrp₁.mkHom (SemiNormedGrp.Hom.hom f.inv) i'
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
/-- Arithmetic subgroups of `GL(2, ℝ)` are discrete.  -/
Subgroup.IsArithmetic.discreteTopology : ∀ {𝒢 : Subgroup (GL (Fin 2) ℝ)} [𝒢.IsArithmetic], DiscreteTopology ↥𝒢
-- Lean.Meta.Basic
/-- Takes an array `xs` of free variables and metavariables and a
body term `e` and creates `fun ..xs => e`, suitably
abstracting `e` and the types in `xs`.  -/
Lean.Meta.mkLambdaFVars : Array Lean.Expr →
  Lean.Expr →
    optParam Bool false →
      optParam Bool true →
        optParam Bool false →
          optParam Bool true → optParam Lean.BinderInfo Lean.BinderInfo.implicit → Lean.MetaM Lean.Expr