mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_17.splitter : (motive : (w : ℕ) → Std.Tactic.BVDecide.BVExpr w → Sort u_1) →
  (w : ℕ) →
    (expr : Std.Tactic.BVDecide.BVExpr w) →
      ((w a : ℕ) → motive w (Std.Tactic.BVDecide.BVExpr.var a)) →
        ((w : ℕ) → (val : BitVec w) → motive w (Std.Tactic.BVDecide.BVExpr.const val)) →
          ((w : ℕ) →
              (lhsExpr : Std.Tactic.BVDecide.BVExpr w) →
                (op : Std.Tactic.BVDecide.BVBinOp) →
                  (rhsExpr : Std.Tactic.BVDecide.BVExpr w) → motive w (lhsExpr.bin op rhsExpr)) →
            ((w : ℕ) →
                (op : Std.Tactic.BVDecide.BVUnOp) →
                  (expr : Std.Tactic.BVDecide.BVExpr w) → motive w (Std.Tactic.BVDecide.BVExpr.un op expr)) →
              ((w l r : ℕ) →
                  (lhs : Std.Tactic.BVDecide.BVExpr l) →
                    (rhs : Std.Tactic.BVDecide.BVExpr r) → (h : w = l + r) → motive w (lhs.append rhs h)) →
                ((w w_1 n : ℕ) →
                    (expr : Std.Tactic.BVDecide.BVExpr w_1) →
                      (h : w = w_1 * n) → motive w (Std.Tactic.BVDecide.BVExpr.replicate n expr h)) →
                  ((len w start : ℕ) →
                      (expr : Std.Tactic.BVDecide.BVExpr w) →
                        motive len (Std.Tactic.BVDecide.BVExpr.extract start len expr)) →
                    ((w n : ℕ) →
                        (lhs : Std.Tactic.BVDecide.BVExpr w) →
                          (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftLeft rhs)) →
                      ((w n : ℕ) →
                          (lhs : Std.Tactic.BVDecide.BVExpr w) →
                            (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftRight rhs)) →
                        ((w n : ℕ) →
                            (lhs : Std.Tactic.BVDecide.BVExpr w) →
                              (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.arithShiftRight rhs)) →
                          motive w expr
-- Lean.Message
/-- Write the given list of messages as a list, separating each item with `,\n` and surrounding with square brackets.  -/
Lean.MessageData.ofList : List Lean.MessageData → Lean.MessageData
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.C_add_one : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ),
  Polynomial.Chebyshev.C R (n + 1) = Polynomial.X * Polynomial.Chebyshev.C R n - Polynomial.Chebyshev.C R (n - 1)
-- Mathlib.Order.Partition.Basic
Partition.coe_parts : ∀ {α : Type u_1} {s : α} [inst : CompleteLattice α] {P : Partition s}, P.parts = ↑P
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Equivalence.instMonoidalFunctorRefl : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → CategoryTheory.Equivalence.refl.functor.Monoidal
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?_append : ∀ {α : Type u} {β : Type v} [inst : BEq α] {l l' : List ((_ : α) × β)} {a : α},
  Std.Internal.List.getValue? a (l ++ l') = (Std.Internal.List.getValue? a l).or (Std.Internal.List.getValue? a l')
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
/-- The unique two-coloring of a forest that colors the given vertices with zero  -/
SimpleGraph.IsAcyclic.coloringTwoOfVerts : {V : Type u_1} →
  {G : SimpleGraph V} →
    G.IsAcyclic → (verts : G.ConnectedComponent → V) → (∀ (C : G.ConnectedComponent), verts C ∈ C) → G.Coloring (Fin 2)
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.conductor_ne_zero : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) [NeZero n], χ.conductor ≠ 0
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.div_subset_div : ∀ {α : Type u_2} [inst : Div α] {s₁ s₂ t₁ t₂ : Set α}, s₁ ⊆ t₁ → s₂ ⊆ t₂ → s₁ / s₂ ⊆ t₁ / t₂
-- Lean.Meta.Sym.DSimp.DSimpM
Lean.Meta.Sym.DSimp.State.mk.inj : ∀ {numSteps : ℕ} {cache : Lean.Meta.Sym.DSimp.Cache} {numSteps_1 : ℕ} {cache_1 : Lean.Meta.Sym.DSimp.Cache},
  { numSteps := numSteps, cache := cache } = { numSteps := numSteps_1, cache := cache_1 } →
    numSteps = numSteps_1 ∧ cache = cache_1
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {f : Equiv.Perm α} {x : α},
  f.cycleOf x ∈ f.cycleFactorsFinset ↔ x ∈ f.support
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.instMul.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_4}
  [inst_5 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_6} [inst_7 : TopologicalSpace N] [inst_8 : ChartedSpace H N]
  {n : WithTop ℕ∞} {G : Type u_10} [inst_9 : Mul G] [inst_10 : TopologicalSpace G] [inst_11 : ChartedSpace H' G]
  [inst_12 : ContMDiffMul I' n G], ContMDiffMap.instMul = { mul := fun f g => ⟨⇑f * ⇑g, ⋯⟩ }
-- Init.System.IO
instMonadFinallyEIO : {ε : Type} → MonadFinally (EIO ε)
-- Mathlib.Data.PFun
PFun.comp_assoc : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : γ →. δ) (g : β →. γ) (h : α →. β),
  (f.comp g).comp h = f.comp (g.comp h)
-- Mathlib.Topology.Category.TopPair
/-- The inclusion functor from topological spaces to topological pairs that sends a space X to
(X, ∅).  -/
TopPair.incl : CategoryTheory.Functor TopCat TopPair
-- Mathlib.Topology.Compactness.Lindelof
/-- Sets of subtype are Lindelöf iff the image under a coercion is.  -/
Subtype.isLindelof_iff : ∀ {X : Type u} [inst : TopologicalSpace X] {p : X → Prop} {s : Set { x // p x }},
  IsLindelof s ↔ IsLindelof (Subtype.val '' s)
-- Std.Data.Iterators.Producers.Range
/-- Returns an iterator over the given range. This iterator will emit the elements of the range
in increasing order.
 -/
Std.Rio.iter : {α : Type u_1} → [Std.PRange.Least? α] → Std.Rio α → Std.Iter α
-- Mathlib.Topology.Semicontinuity.Defs
lowerSemicontinuousWithinAt_iff_frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f : α → β} {x : α} {s : Set α},
  LowerSemicontinuousWithinAt f s x ↔ ∀ (y : β), (∃ᶠ (x' : α) in nhdsWithin x s, f x' ≤ y) → f x ≤ y
-- Init.Data.SInt.Bitwise
Int64.toInt8_xor : ∀ (a b : Int64), (a ^^^ b).toInt8 = a.toInt8 ^^^ b.toInt8
-- Lean.Compiler.IR.Basic
Lean.IR.Expr.lit.inj : ∀ {v v_1 : Lean.IR.LitVal}, Lean.IR.Expr.lit v = Lean.IR.Expr.lit v_1 → v = v_1
-- Mathlib.Data.Int.ModEq
Int.mod_mul_right_mod : ∀ (a b c : ℤ), a % (b * c) % b = a % b
-- Mathlib.CategoryTheory.Bicategory.Coherence
/-- Auxiliary definition for `normalizeEquiv`.  -/
CategoryTheory.FreeBicategory.normalizeUnitIso : {B : Type u} →
  [inst : Quiver B] →
    (a b : CategoryTheory.FreeBicategory B) →
      CategoryTheory.Functor.id (a ⟶ b) ≅
        ((CategoryTheory.FreeBicategory.normalize B).mapFunctor a b).comp
          (CategoryTheory.FreeBicategory.inclusionPath a b)
-- Mathlib.Algebra.Ring.Parity
Odd.sub_even : ∀ {α : Type u_2} [inst : Ring α] {a b : α}, Odd a → Even b → Odd (a - b)
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- The duality equivalence `(WidePushoutShape J)ᵒᵖ ≌ WidePullbackShape J`  -/
CategoryTheory.Limits.widePushoutShapeOpEquiv : (J : Type w) → (CategoryTheory.Limits.WidePushoutShape J)ᵒᵖ ≌ CategoryTheory.Limits.WidePullbackShape J
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
ProfiniteAddGrp.ProfiniteCompletion.preimage.eq_1 : ∀ {G : AddGrpCat} {P : ProfiniteAddGrp.{u}} (f : G ⟶ AddGrpCat.of ↑P.toProfinite.toTop)
  (H : OpenNormalAddSubgroup ↑P.toProfinite.toTop),
  ProfiniteAddGrp.ProfiniteCompletion.preimage f H =
    FiniteIndexNormalAddSubgroup.comap (AddGrpCat.Hom.hom f) H.toFiniteIndexNormalAddSubgroup
-- Mathlib.Tactic.Widget.LibraryRewrite
Mathlib.Tactic.LibraryRewrite.RewriteInterface.mk.injEq : ∀ (symm : Bool) (tactic : String) (replacement : Lean.Expr) (replacementString : String)
  (extraGoals : Array Lean.Widget.CodeWithInfos) (prettyLemma : Lean.Widget.CodeWithInfos) (lemmaType : Lean.Expr)
  (makesNewMVars symm_1 : Bool) (tactic_1 : String) (replacement_1 : Lean.Expr) (replacementString_1 : String)
  (extraGoals_1 : Array Lean.Widget.CodeWithInfos) (prettyLemma_1 : Lean.Widget.CodeWithInfos) (lemmaType_1 : Lean.Expr)
  (makesNewMVars_1 : Bool),
  ({ symm := symm, tactic := tactic, replacement := replacement, replacementString := replacementString,
        extraGoals := extraGoals, prettyLemma := prettyLemma, lemmaType := lemmaType, makesNewMVars := makesNewMVars } =
      { symm := symm_1, tactic := tactic_1, replacement := replacement_1, replacementString := replacementString_1,
        extraGoals := extraGoals_1, prettyLemma := prettyLemma_1, lemmaType := lemmaType_1,
        makesNewMVars := makesNewMVars_1 }) =
    (symm = symm_1 ∧
      tactic = tactic_1 ∧
        replacement = replacement_1 ∧
          replacementString = replacementString_1 ∧
            extraGoals = extraGoals_1 ∧
              prettyLemma = prettyLemma_1 ∧ lemmaType = lemmaType_1 ∧ makesNewMVars = makesNewMVars_1)
-- Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
_private.Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas.0.Nat.nthRoot.match_1.eq_1 : ∀ (motive : ℕ → ℕ → Sort u_1) (guess : ℕ) (h_1 : (guess : ℕ) → motive 0 guess)
  (h_2 : (fuel guess : ℕ) → motive fuel.succ guess),
  (match 0, guess with
    | 0, guess => h_1 guess
    | fuel.succ, guess => h_2 fuel guess) =
    h_1 guess
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
DerivedCategory.instEssSurjArrowHomotopyCategoryIntUpMapArrowQh : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C], DerivedCategory.Qh.mapArrow.EssSurj
-- Lean.Elab.Command
_private.Lean.Elab.Command.0.Lean.liftCommandElabMCore : {α : Type} → Lean.Elab.Command.CommandElabM α → Bool → Lean.CoreM α
-- Mathlib.Algebra.Module.Submodule.Invariant
Module.End.invtSubmodule.inf_mem : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {f : Module.End R M} {p q : Submodule R M}, p ∈ f.invtSubmodule → q ∈ f.invtSubmodule → p ⊓ q ∈ f.invtSubmodule
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Polynomial.Chebyshev.sumNodes.eq_1 : ∀ (n : ℕ) (c : ℕ → ℝ) (P : Polynomial ℝ),
  Polynomial.Chebyshev.sumNodes n c P = ∑ i ≤ n, Polynomial.eval (Polynomial.Chebyshev.node n i) P * c i
-- Init.Data.SInt.Lemmas
Int64.cast_toNatClampNeg : ∀ (x : Int64), 0 ≤ x → ↑x.toNatClampNeg = x.toInt
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.lieSpan_eq : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N : LieSubmodule R L M), LieSubmodule.lieSpan R L ↑N = N
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument_aleph0 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C)
  [I.IsCardinalForSmallObjectArgument Cardinal.aleph0],
  I.rlp.llp =
    ((CategoryTheory.MorphismProperty.coproducts.{w, v, u} I).pushouts.transfiniteCompositionsOfShape ℕ).retracts
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
integral_inv_of_pos : ∀ {a b : ℝ}, 0 < a → 0 < b → ∫ (x : ℝ) in a..b, x⁻¹ = Real.log (b / a)
-- Aesop.Rule
Aesop.NormSimpRule.mk : Aesop.RuleName → Array Lean.Meta.SimpEntry → Aesop.NormSimpRule
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.uniqueBaseOn_indep_iff' : ∀ {α : Type u_1} {E I J : Set α}, (Matroid.uniqueBaseOn I E).Indep J ↔ J ⊆ I ∩ E
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.limitRecOn_limit : ∀ {motive : Ordinal.{u_4} → Sort u_5} (o : Ordinal.{u_4}) (H₁ : motive 0)
  (H₂ : (o : Ordinal.{u_4}) → motive o → motive (o + 1))
  (H₃ : (o : Ordinal.{u_4}) → Order.IsSuccLimit o → ((o' : Ordinal.{u_4}) → o' < o → motive o') → motive o)
  (h : Order.IsSuccLimit o), Ordinal.limitRecOn o H₁ H₂ H₃ = H₃ o h fun x _h => Ordinal.limitRecOn x H₁ H₂ H₃
-- Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
CategoryTheory.SmallObject.SuccStruct.ofCocone_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {J : Type u} [inst_1 : LinearOrder J] {j : J}
  {F : CategoryTheory.Functor (↑(Set.Iio j)) C} (c : CategoryTheory.Limits.Cocone F) (i₁ i₂ : J) (hi : i₁ ≤ i₂)
  (hi₂ : i₂ < j),
  (CategoryTheory.SmallObject.SuccStruct.ofCocone c).map (CategoryTheory.homOfLE hi) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.SuccStruct.ofCoconeObjIso c i₁ ⋯).hom
      (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.homOfLE hi))
        (CategoryTheory.SmallObject.SuccStruct.ofCoconeObjIso c i₂ hi₂).inv)
-- Mathlib.ModelTheory.DirectLimit
/-- The structure on the `Σ`-type which becomes the structure on the direct limit after quotienting.
 -/
FirstOrder.Language.DirectLimit.sigmaStructure : {L : FirstOrder.Language} →
  {ι : Type v} →
    [inst : Preorder ι] →
      (G : ι → Type w) →
        [inst_1 : (i : ι) → L.Structure (G i)] →
          (f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)) →
            [IsDirectedOrder ι] → [Nonempty ι] → L.Structure (FirstOrder.Language.Structure.Sigma f)
-- Mathlib.Data.List.MinMax
List.Perm.maximum_eq : ∀ {α : Type u_1} [inst : LinearOrder α] {l l' : List α}, l.Perm l' → l.maximum = l'.maximum
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.ConsumerNode.mctx : Lean.Meta.SynthInstance.ConsumerNode → Lean.MetavarContext
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.pow_nc : Lean.Grind.CommRing.Poly → ℕ → Lean.Grind.CommRing.Poly
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.Hom.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {M N : CategoryTheory.AddMon C} {hom : M.X ⟶ N.X} {isAddMonHom_hom : CategoryTheory.IsAddMonHom hom}
  {hom_1 : M.X ⟶ N.X} {isAddMonHom_hom_1 : CategoryTheory.IsAddMonHom hom_1},
  { hom := hom, isAddMonHom_hom := isAddMonHom_hom } = { hom := hom_1, isAddMonHom_hom := isAddMonHom_hom_1 } →
    hom = hom_1
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
/-- In the tangent bundle to the model space, the second projection is `C^n`.  -/
contMDiff_snd_tangentBundle_modelSpace : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (H : Type u_4) [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H),
  ContMDiff I.tangent (modelWithCornersSelf 𝕜 E) n fun p => p.snd
-- Lean.Meta.Tactic.Simp.Simproc
/-- Implements attributes `builtin_simproc` and `builtin_sevalproc`.
 -/
Lean.Meta.Simp.addSimprocBuiltinAttrCore : IO.Ref Lean.Meta.Simprocs → Lean.Name → Bool → Lean.Meta.Simp.Simproc ⊕ Lean.Meta.Simp.DSimproc → IO Unit
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
multipliable_prod : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α]
  {L : SummationFilter β} [ContinuousMul α] {f : γ → β → α} {s : Finset γ},
  (∀ i ∈ s, Multipliable (f i) L) → Multipliable (fun b => ∏ i ∈ s, f i b) L
-- Mathlib.CategoryTheory.Limits.Shapes.KernelPair
CategoryTheory.IsKernelPair.mono_of_eq_fst_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {R X Y : C} {f : X ⟶ Y} {a b : R ⟶ X},
  CategoryTheory.IsKernelPair f a b → a = b → CategoryTheory.Mono f
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
/-- `ContinuousMultilinearMap.prod` as an `Equiv`.  -/
ContinuousMultilinearMap.prodEquiv : {R : Type u} →
  {ι : Type v} →
    {M₁ : ι → Type w₁} →
      {M₂ : Type w₂} →
        {M₃ : Type w₃} →
          [inst : Semiring R] →
            [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
              [inst_2 : AddCommMonoid M₂] →
                [inst_3 : AddCommMonoid M₃] →
                  [inst_4 : (i : ι) → Module R (M₁ i)] →
                    [inst_5 : Module R M₂] →
                      [inst_6 : Module R M₃] →
                        [inst_7 : (i : ι) → TopologicalSpace (M₁ i)] →
                          [inst_8 : TopologicalSpace M₂] →
                            [inst_9 : TopologicalSpace M₃] →
                              ContinuousMultilinearMap R M₁ M₂ × ContinuousMultilinearMap R M₁ M₃ ≃
                                ContinuousMultilinearMap R M₁ (M₂ × M₃)
-- Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Matrix.nondegenerate_iff_separatingRight : ∀ {n : Type u_1} {A : Type u_4} [inst : CommRing A] [IsDomain A] {M : Matrix n n A} [inst_2 : Finite n],
  M.Nondegenerate ↔ M.SeparatingRight
-- Mathlib.Tactic.Abel
/-- Extract the expression from a normal form.  -/
Mathlib.Tactic.Abel.NormalExpr.e : Mathlib.Tactic.Abel.NormalExpr → Lean.Expr
-- Init.Data.UInt.Basic
instPowUSizeNat : Pow USize ℕ
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- A continuous function with compact support on a product space is strongly measurable for the
product sigma-algebra. The subtlety is that we do not assume that the spaces are separable, so the
product of the Borel sigma algebras might not contain all open sets, but still it contains enough
of them to approximate compactly supported continuous functions.  -/
HasCompactSupport.stronglyMeasurable_of_prod : ∀ {α : Type u_1} {X : Type u_5} {Y : Type u_6} [inst : Zero α] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace Y] [inst_3 : MeasurableSpace X] [inst_4 : MeasurableSpace Y] [OpensMeasurableSpace X]
  [OpensMeasurableSpace Y] [inst_7 : TopologicalSpace α] [TopologicalSpace.PseudoMetrizableSpace α] {f : X × Y → α},
  Continuous f → HasCompactSupport f → MeasureTheory.StronglyMeasurable f
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.subset_hull : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : SMul R M] {s : Set M}, s ⊆ ↑(ConvexCone.hull R s)
-- Mathlib.Topology.Category.Stonean.Basic
/-- The functor from Stonean spaces to profinite spaces.  -/
Stonean.toProfinite : CategoryTheory.Functor Stonean Profinite
-- Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
cyclotomicCharacter.toFun_apply : ∀ {L : Type u} [inst : CommRing L] [inst_1 : IsDomain L] (p : ℕ) [inst_2 : Fact (Nat.Prime p)] (g : L ≃+* L)
  [inst_3 : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)],
  cyclotomicCharacter.toFun p g = PadicInt.ofIntSeq (fun n => modularCyclotomicCharacter.aux g (p ^ n)) ⋯
-- Mathlib.Order.Category.BoolAlg
BoolAlg.id_apply : ∀ (X : BoolAlg) (x : ↑X), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x
-- Lean.DocString.Markdown
Lean.Doc.MdRendererState.mk.injEq : ∀ (imported current imported_1 current_1 : Lean.NameMap Lean.Name),
  ({ imported := imported, current := current } = { imported := imported_1, current := current_1 }) =
    (imported = imported_1 ∧ current = current_1)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.get_eq : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  (hk : k ∈ m₁) (h : m₁.Equiv m₂), m₁.get k hk = m₂.get k ⋯
-- Mathlib.Tactic.ApplyFun
/-- **Alias** of the forward direction of `OrderIso.le_iff_le`. -/
Mathlib.Tactic.ApplyFun.le_of_le : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] (e : α ≃o β) {x y : α}, e x ≤ e y → x ≤ y
-- Init.Prelude
ne_true_of_eq_false : ∀ {b : Bool}, b = false → ¬b = true
-- Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
/-- The canonical embedding (as an ordered monoid hom) from a linearly ordered cancellative
group into `ℤ`. This is either surjective or zero.  -/
LocallyFiniteOrder.orderAddMonoidHom : (G : Type u_2) →
  [inst : AddCommGroup G] → [inst_1 : LinearOrder G] → [IsOrderedAddMonoid G] → [LocallyFiniteOrder G] → G →+o ℤ
-- Mathlib.Order.Max
noMinOrder_of_right : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [NoMinOrder β], NoMinOrder (α × β)
-- Mathlib.Data.NNReal.Defs
NNReal.instNNRatCast : NNRatCast NNReal
-- Init.Coe
instCoeOTCOfCoeTC : {α : Sort u_1} → {β : Sort u_2} → [CoeTC α β] → CoeOTC α β
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
/-- The colimit of `F ⋙ forget AddMon` in the category of types.
In the following, we will construct an additive monoid structure on `M`.  -/
AddMonCat.FilteredColimits.M : {J : Type v} → [inst : CategoryTheory.SmallCategory J] → CategoryTheory.Functor J AddMonCat → Type (max u v)
-- Mathlib.Algebra.Algebra.Hom
AlgHom.congr_fun : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] {φ₁ φ₂ : A →ₐ[R] B}, φ₁ = φ₂ → ∀ (x : A), φ₁ x = φ₂ x
-- Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
PositiveLinearMap.gnsStarAlgHom_apply : ∀ {A : Type u_2} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : StarOrderedRing A] (f : A →ₚ[ℂ] ℂ) (a : A),
  f.gnsStarAlgHom a = f.gnsNonUnitalStarAlgHom.toFun a
-- Lean.LocalContext
/-- Returns the value of the `ldecl` if it has a visible value.

If `allowNondep` is true, then allows nondependent `ldecl`s, whose values are normally hidden.
 -/
Lean.LocalDecl.value? : Lean.LocalDecl → optParam Bool false → Option Lean.Expr
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.findSomeM?_eq_match_step : ∀ {α β γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α m β]
  [inst_2 : Std.IteratorLoop α m m] [LawfulMonad m] [Std.Iterators.Finite α m] [Std.LawfulIteratorLoop α m m]
  {it : Std.IterM m β} {f : β → m (Option γ)},
  it.findSomeM? f = do
    let __do_lift ← it.step
    match ↑__do_lift.inflate with
      | Std.IterStep.yield it' out => do
        let __do_lift ← f out
        match __do_lift with
          | none => it'.findSomeM? f
          | some fx => pure (some fx)
      | Std.IterStep.skip it' => it'.findSomeM? f
      | Std.IterStep.done => pure none
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.filterMapWithPostcondition.eq_1 : ∀ {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : MonadLiftT m n] [inst_1 : Std.Iterator α m β]
  (f : β → Std.Iterators.PostconditionT n (Option γ)) (it : Std.IterM m β),
  Std.IterM.filterMapWithPostcondition f it = Std.IterM.InternalCombinators.filterMap (fun ⦃x⦄ => monadLift) f it
-- Init.GrindInstances.ToInt
Lean.Grind.instPowNatCiOfNatInt : Lean.Grind.ToInt.Pow ℕ (Lean.Grind.IntInterval.ci 0)
-- Mathlib.Condensed.Explicit
/-- The condensed object associated to a presheaf on `Profinite` whose postcomposition with the
forgetful functor preserves finite products and satisfies the equalizer condition.
 -/
Condensed.ofSheafForgetProfinite : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    [∀ (X : CompHausᵒᵖ),
          CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X profiniteToCompHaus.op) A] →
      {FA : A → A → Type u_2} →
        {CA : A → Type u_3} →
          [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] →
            [inst_3 : CategoryTheory.ConcreteCategory A FA] →
              [CategoryTheory.Limits.ReflectsFiniteLimits (CategoryTheory.forget A)] →
                (F : CategoryTheory.Functor Profiniteᵒᵖ A) →
                  [CategoryTheory.Limits.PreservesFiniteProducts (F.comp (CategoryTheory.forget A))] →
                    CategoryTheory.regularTopology.EqualizerCondition (F.comp (CategoryTheory.forget A)) → Condensed A
-- Mathlib.CategoryTheory.Monad.Monadicity
/-- Typeclass expressing that for all `G`-split pairs `f,g`, `G` creates colimits of
`parallelPair f g`.  -/
CategoryTheory.Monad.CreatesColimitOfIsSplitPair : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] → CategoryTheory.Functor D C → Type (max (max u₁ u₂) v₁)
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
/-- Definition of the `n`th exterior power of an `R`-module `M`. We introduce the notation
`⋀[R]^n M` for `exteriorPower R n M`.  -/
ExteriorAlgebra.«term⋀[_]^_» : Lean.ParserDescr