mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Bounds.Image
MonotoneOn.mem_upperBounds_image : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s t : Set α} {a : α},
  MonotoneOn f t → s ⊆ t → a ∈ upperBounds s → a ∈ t → f a ∈ upperBounds (f '' s)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.NewFact.eq.sizeOf_spec : ∀ (lhs rhs proof : Lean.Expr) (isHEq : Bool),
  sizeOf (Lean.Meta.Grind.NewFact.eq lhs rhs proof isHEq) = 1 + sizeOf lhs + sizeOf rhs + sizeOf proof + sizeOf isHEq
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.mk.injEq : ∀ {α : Type u_4} [inst : TopologicalSpace α] (toCompacts : TopologicalSpace.Compacts α)
  (nonempty' : toCompacts.carrier.Nonempty) (toCompacts_1 : TopologicalSpace.Compacts α)
  (nonempty'_1 : toCompacts_1.carrier.Nonempty),
  ({ toCompacts := toCompacts, nonempty' := nonempty' } = { toCompacts := toCompacts_1, nonempty' := nonempty'_1 }) =
    (toCompacts = toCompacts_1)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.of_forall_getKey?_unit_eq : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {t₁ t₂ : Std.DTreeMap.Raw α (fun x => Unit) cmp},
  t₁.WF → t₂.WF → (∀ (k : α), t₁.getKey? k = t₂.getKey? k) → t₁.Equiv t₂
-- Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
CategoryTheory.Precoverage.IsStableUnderComposition.of_preZeroHypercoverFamily : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.PreZeroHypercoverFamily C},
  (∀ {X : C} (E : CategoryTheory.PreZeroHypercover X) (F : (i : E.I₀) → CategoryTheory.PreZeroHypercover (E.X i)),
      P.property E → (∀ (i : E.I₀), P.property (F i)) → P.property (E.bind F)) →
    P.precoverage.IsStableUnderComposition
-- Mathlib.Topology.MetricSpace.Algebra
AddSubmonoid.lipschitzAdd : ∀ {β : Type u_2} [inst : PseudoMetricSpace β] [inst_1 : AddMonoid β] [LipschitzAdd β] (s : AddSubmonoid β),
  LipschitzAdd ↥s
-- Mathlib.LinearAlgebra.Projection
/-- **Alias** of the reverse direction of `LinearMap.IsIdempotentElem.ext_iff`.

---

Idempotent operators are equal iff their range and kernels are.  -/
LinearMap.IsIdempotentElem.ext : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : E →ₗ[R] E},
  IsIdempotentElem p → IsIdempotentElem q → p.range = q.range ∧ p.ker = q.ker → p = q
-- Mathlib.Geometry.Manifold.BumpFunction
SmoothBumpFunction.tsupport_subset_extChartAt_source : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {c : M}
  (f : SmoothBumpFunction I c) [inst_5 : FiniteDimensional ℝ E] [T2Space M], tsupport ↑f ⊆ (extChartAt I c).source
-- Mathlib.Order.SymmDiff
bihimp_right_comm : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (a b c : α), bihimp (bihimp a b) c = bihimp (bihimp a c) b
-- Mathlib.Analysis.Complex.Exponential
Real.exp_abs_le : ∀ (x : ℝ), Real.exp |x| ≤ Real.exp x + Real.exp (-x)
-- Mathlib.ModelTheory.Definability
/-- A term is a definable function.  -/
FirstOrder.Language.Term.definableFun_realize : ∀ {M : Type u_1} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u_2} (t : L.Term α),
  Set.DefinableFun L ∅ fun v => FirstOrder.Language.Term.realize v t
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
/-- A `Functor.PullbackObjObj` structure for a functor `G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂` and
morphisms `f₁ : X₁ ⟶ Y₁` and `f₃ : X₃ ⟶ Y₃` when `X₁` is initial and both
`G.flip.obj X₃` and `G.flip.obj Y₃` preserve the terminal object.  -/
CategoryTheory.Functor.PullbackObjObj.ofIsInitial : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
            (G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)) →
              {X₁ Y₁ : C₁} →
                (f₁ : X₁ ⟶ Y₁) →
                  {X₃ Y₃ : C₃} →
                    (f₃ : X₃ ⟶ Y₃) →
                      [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})
                            (G.flip.obj X₃)] →
                        [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})
                              (G.flip.obj Y₃)] →
                          CategoryTheory.Limits.IsInitial X₁ → G.PullbackObjObj f₁ f₃
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.WalkingMulticospan.left.sizeOf_spec : ∀ {J : CategoryTheory.Limits.MulticospanShape} (a : J.L),
  sizeOf (CategoryTheory.Limits.WalkingMulticospan.left a) = 1 + sizeOf a
-- Mathlib.Testing.Plausible.Sampleable
Plausible.PNat.shrinkable : Plausible.Shrinkable ℕ+
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.coe_finsetSum : ∀ {α : Type u_1} {ι : Type u_2} {N : Type u_10} [inst : AddCommMonoid N] (S : Finset ι) (f : ι → α →₀ N),
  ⇑(∑ i ∈ S, f i) = ∑ i ∈ S, ⇑(f i)
-- Mathlib.RingTheory.Length
Module.length_submodule : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Submodule R M},
  Module.length R ↥N = Order.height N
-- Mathlib.Algebra.Group.Defs
InvolutiveInv.inv_inv : ∀ {G : Type u_2} [self : InvolutiveInv G] (x : G), x⁻¹⁻¹ = x
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.bddAbove_range_comp : ∀ {ι : Type u} {f : ι → Cardinal.{v}},
  BddAbove (Set.range f) → ∀ (g : Cardinal.{v} → Cardinal.{max v w}), BddAbove (Set.range (g ∘ f))
-- Mathlib.Data.Set.Semiring
SetSemiring.instAddCommMonoid : {α : Type u_1} → AddCommMonoid (SetSemiring α)
-- Mathlib.Data.Int.CardIntervalMod
Nat.Ico_filter_modEq_cast : ∀ (a b : ℕ) {r v : ℕ},
  Finset.map Nat.castEmbedding ({x ∈ Finset.Ico a b | x ≡ v [MOD r]}) = {x ∈ Finset.Ico ↑a ↑b | x ≡ ↑v [ZMOD ↑r]}
-- Mathlib.Tactic.Basic
_private.Mathlib.Tactic.Basic.0.Mathlib.Tactic.evalIntrov.introsDep : Lean.Elab.Tactic.TacticM Unit
-- Mathlib.RingTheory.Ideal.IsPrincipal
/-- The `MulEquiv` version of `Ideal.associatesNonZeroDivisorsEquivIsPrincipal`.  -/
Ideal.associatesNonZeroDivisorsMulEquivIsPrincipal : (R : Type u_1) →
  [inst : CommRing R] → [IsDomain R] → Associates ↥(nonZeroDivisors R) ≃* ↥(Ideal.isPrincipalNonZeroDivisorsSubmonoid R)
-- Mathlib.Data.Set.Lattice.Image
Set.seq_def : ∀ {α : Type u_1} {β : Type u_2} {s : Set (α → β)} {t : Set α}, s.seq t = ⋃ f ∈ s, f '' t
-- Mathlib.Topology.Algebra.Group.Basic
continuousWithinAt_neg : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Neg G] [ContinuousNeg G] {s : Set G} {x : G},
  ContinuousWithinAt Neg.neg s x
-- Mathlib.Topology.Order
instTopologicalSpacePUnit : TopologicalSpace PUnit.{u_1 + 1}
-- Std.Data.HashMap.Lemmas
Std.HashMap.contains_insertIfNew : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k a : α} {v : β}, (m.insertIfNew k v).contains a = (k == a || m.contains a)
-- Mathlib.LinearAlgebra.TensorProduct.Map
/-- The tensor product of a pair of semilinear maps between modules, bilinear in both maps.  -/
TensorProduct.mapBilinear : {R : Type u_1} →
  {R₂ : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring R₂] →
        (σ₁₂ : R →+* R₂) →
          (M : Type u_7) →
            (N : Type u_8) →
              (M₂ : Type u_12) →
                (N₂ : Type u_14) →
                  [inst_2 : AddCommMonoid M] →
                    [inst_3 : AddCommMonoid N] →
                      [inst_4 : AddCommMonoid M₂] →
                        [inst_5 : AddCommMonoid N₂] →
                          [inst_6 : Module R M] →
                            [inst_7 : Module R N] →
                              [inst_8 : Module R₂ M₂] →
                                [inst_9 : Module R₂ N₂] →
                                  (M →ₛₗ[σ₁₂] M₂) →ₗ[R₂]
                                    (N →ₛₗ[σ₁₂] N₂) →ₗ[R₂] TensorProduct R M N →ₛₗ[σ₁₂] TensorProduct R₂ M₂ N₂
-- Mathlib.Order.Interval.Set.Basic
Set.Ioi_ssubset_Ici_self : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, Set.Ioi a ⊂ Set.Ici a
-- Mathlib.Tactic.NormNum.Basic
/-- The `norm_num` extension which identifies `False`.  -/
Mathlib.Meta.NormNum.evalFalse : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.mapDomainAlgHom_apply : ∀ (R : Type u_1) (A : Type u_4) {M : Type u_7} {N : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Monoid M] [inst_4 : Monoid N] (f : M →* N) (x : MonoidAlgebra A M),
  (MonoidAlgebra.mapDomainAlgHom R A f) x = MonoidAlgebra.mapDomain (⇑f) x
-- Init.Data.SInt.Lemmas
Int8.neg_add_mul_eq_mul_not : ∀ {a b : Int8}, -(a + a * b) = a * ~~~b
-- Mathlib.Topology.Order.AtTopBotIxx
/-- A family of half-open intervals bounded by diverging limits is locally finite.  -/
locallyFinite_Ico_of_tendsto : ∀ {X : Type u_1} [inst : LinearOrder X] [inst_1 : TopologicalSpace X] [OrderTopology X] {α : Type u_2}
  [inst_3 : LinearOrder α] [LocallyFiniteOrder α] [NoMaxOrder X] [NoMinOrder X] {l u : α → X},
  Filter.Tendsto l Filter.atTop Filter.atTop →
    Filter.Tendsto u Filter.atBot Filter.atBot → LocallyFinite fun n => Set.Ico (l n) (u n)
-- Lean.LocalContext
Lean.instReprLocalDeclKind.repr : Lean.LocalDeclKind → ℕ → Std.Format
-- Mathlib.Analysis.Calculus.FDeriv.Mul
HasFDerivWithinAt.finsetProd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {ι : Type u_5} {𝔸' : Type u_7} [inst_3 : NormedCommRing 𝔸']
  [inst_4 : NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {g : ι → E → 𝔸'} {g' : ι → E →L[𝕜] 𝔸'} [inst_5 : DecidableEq ι] {x : E},
  (∀ i ∈ u, HasFDerivWithinAt (g i) (g' i) s x) →
    HasFDerivWithinAt (fun x => ∏ i ∈ u, g i x) (∑ i ∈ u, (∏ j ∈ u.erase i, g j x) • g' i) s x
-- Mathlib.Topology.Maps.Basic
Topology.IsOpenEmbedding.continuousAt_iff : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace Y] [inst_2 : TopologicalSpace Z],
  Topology.IsOpenEmbedding f → ∀ {x : X}, ContinuousAt (g ∘ f) x ↔ ContinuousAt g (f x)
-- Mathlib.Order.Partition.Finpartition
Finpartition.biUnion_parts : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} (P : Finpartition s), P.parts.biUnion id = s
-- Mathlib.Analysis.Complex.Norm
Complex.one_le_normSq_iff : ∀ {x : ℂ}, 1 ≤ Complex.normSq x ↔ 1 ≤ ‖x‖
-- Mathlib.Algebra.Homology.Embedding.TruncGE
/-- The canonical truncation of a homological complex relative to an embedding
of complex shapes `e` which satisfies `e.IsTruncGE`.  -/
HomologicalComplex.truncGE : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
              (K : HomologicalComplex C c') →
                (e : c.Embedding c') →
                  [e.IsTruncGE] →
                    [∀ (i' : ι'), K.HasHomology i'] → [CategoryTheory.Limits.HasZeroObject C] → HomologicalComplex C c'
-- Mathlib.Algebra.BigOperators.Finprod
Multiset.prod_map_eq_finprod : ∀ {α : Type u_1} {M : Type u_2} [inst : DecidableEq α] [inst_1 : CommMonoid M] (s : Multiset α) (f : α → M),
  (Multiset.map f s).prod = ∏ᶠ (a : α), f a ^ Multiset.count a s
-- Mathlib.Topology.Order.OrderClosed
/-- **Alias** of `le_of_tendsto_of_tendsto`. -/
tendsto_le_of_eventuallyLE : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder α] [t : OrderClosedTopology α] {f g : β → α}
  {b : Filter β} {a₁ a₂ : α} [hb : b.NeBot],
  Filter.Tendsto f b (nhds a₁) → Filter.Tendsto g b (nhds a₂) → f ≤ᶠ[b] g → a₁ ≤ a₂
-- Mathlib.Algebra.GroupWithZero.Semiconj
Commute.self_zpow₀ : ∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] (a : G₀) (n : ℤ), Commute a (a ^ n)
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
/-- The canonical pullback cone is a limit cone.
Note: this limit cone is computable as lifts are constructed from the data contained in the
`ChosenPullbackAlong` instance, contrary to `IsPullback.isLimit`, which constructs lifting data from
`CategoryTheory.Square.IsPullback` (a `Prop`).  -/
CategoryTheory.ChosenPullbacksAlong.isLimitPullbackCone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {Y Z X : C} →
      (f : Y ⟶ X) →
        (g : Z ⟶ X) →
          [inst_1 : CategoryTheory.ChosenPullbacksAlong g] →
            CategoryTheory.Limits.IsLimit (CategoryTheory.ChosenPullbacksAlong.pullbackCone f g)
-- Std.Data.HashMap.Lemmas
Std.HashMap.mem_iff_isSome_getElem? : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {a : α}, a ∈ m ↔ m[a]?.isSome = true
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
CategoryTheory.Limits.pushoutCoconeOfLeftIso_ι_app_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
  [inst_1 : CategoryTheory.IsIso f],
  (CategoryTheory.Limits.pushoutCoconeOfLeftIso f g).ι.app CategoryTheory.Limits.WalkingSpan.right =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.Limits.span f g).obj CategoryTheory.Limits.WalkingSpan.right)
-- Init.Internal.Order.Basic
Lean.Order.monotone_compose : ∀ {α : Sort u} [inst : Lean.Order.PartialOrder α] {β : Sort v} [inst_1 : Lean.Order.PartialOrder β] {γ : Sort w}
  [inst_2 : Lean.Order.PartialOrder γ] {f : α → β} {g : β → γ},
  Lean.Order.monotone f → Lean.Order.monotone g → Lean.Order.monotone fun x => g (f x)
-- Mathlib.Analysis.Fourier.AddCircleMulti
/-- The equivalence `measurableEquivPiIoc` is measure preserving.  -/
UnitAddTorus.measurePreserving_equivPiIoc : ∀ {d : Type u_1} [inst : Fintype d] (a : d → ℝ),
  MeasureTheory.MeasurePreserving (⇑(UnitAddTorus.measurableEquivPiIoc a)) MeasureTheory.volume
    (MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.opcyclesMap_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) [inst_2 : K.HasHomology i],
  HomologicalComplex.opcyclesMap (CategoryTheory.CategoryStruct.id K) i =
    CategoryTheory.CategoryStruct.id (K.opcycles i)
-- Mathlib.GroupTheory.GroupAction.ConjAct
ConjAct.toConjAct_inv_smul : ∀ {G : Type u_3} [inst : Group G] (g h : G), ConjAct.toConjAct g⁻¹ • h = g⁻¹ * h * g
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.Nonempty.eq_univ : ∀ {α : Type u_1} {s : Finset α} [inst : Fintype α] [Subsingleton α], s.Nonempty → s = Finset.univ
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.iCondIndepFun.congr_simp : ∀ {Ω : Type u_1} {ι : Type u_2} (m' m'_1 : MeasurableSpace Ω) (e_m' : m' = m'_1) {mΩ : MeasurableSpace Ω}
  [inst : StandardBorelSpace Ω] (hm' : m' ≤ mΩ) {β : ι → Type u_3} [m : (x : ι) → MeasurableSpace (β x)]
  (f f_1 : (x : ι) → Ω → β x),
  f = f_1 →
    ∀ (μ μ_1 : MeasureTheory.Measure Ω) (e_μ : μ = μ_1) [inst_1 : MeasureTheory.IsFiniteMeasure μ],
      ProbabilityTheory.iCondIndepFun m' hm' f μ = ProbabilityTheory.iCondIndepFun m'_1 ⋯ f_1 μ_1
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
/-- A walk between two vertices separated by an edge must go through that edge.  -/
SimpleGraph.Walk.mem_edges_of_not_reachable_deleteEdges : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (w : G.Walk u v) {e : Sym2 V},
  ¬(G.deleteEdges {e}).Reachable u v → e ∈ w.edges
-- Lean.Meta.Structure
Lean.Meta.StructProjDecl.mk : Lean.Syntax → Lean.Name → List (Option Lean.BinderInfo) → Lean.Meta.StructProjDecl
-- Mathlib.Analysis.Matrix.Normed
Matrix.frobenius_norm_map_eq : ∀ {m : Type u_3} {n : Type u_4} {α : Type u_5} {β : Type u_6} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : SeminormedAddCommGroup α] [inst_3 : SeminormedAddCommGroup β] (A : Matrix m n α) (f : α → β),
  (∀ (a : α), ‖f a‖ = ‖a‖) → ‖A.map f‖ = ‖A‖
-- Mathlib.Order.Hom.WithTopBot
LatticeHom.coe_withBotWithTop : ∀ {α : Type u_1} {β : Type u_2} [inst : Lattice α] [inst_1 : Lattice β] (f : LatticeHom α β),
  ⇑f.withBotWithTop = WithBot.map (WithTop.map ⇑f)
-- Mathlib.Data.Vector.MapLemmas
List.Vector.mapAccumr_bisim_tail : ∀ {α : Type u_1} {β : Type u_2} {σ₁ : Type u_6} {σ₂ : Type u_7} {n : ℕ} {xs : List.Vector α n} {f₁ : α → σ₁ → σ₁ × β}
  {f₂ : α → σ₂ → σ₂ × β} {s₁ : σ₁} {s₂ : σ₂},
  (∃ R, R s₁ s₂ ∧ ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).1 (f₂ a q).1 ∧ (f₁ a s).2 = (f₂ a q).2) →
    (List.Vector.mapAccumr f₁ xs s₁).2 = (List.Vector.mapAccumr f₂ xs s₂).2
-- Mathlib.Algebra.Group.Commute.Units
Units.commute_iff_inv_mul_cancel : ∀ {M : Type u_1} [inst : Monoid M] {u : Mˣ} {a : M}, Commute (↑u) a ↔ ↑u⁻¹ * a * ↑u = a
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Sections
/-- The uncurrying operation `Hom A (section X) → Hom ((toOver I).obj A) X`.  -/
CategoryTheory.Over.sectionsUncurry : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {I : C} →
        [inst_2 : CategoryTheory.Closed I] →
          [inst_3 : CategoryTheory.ChosenPullbacksAlong (CategoryTheory.curryRightUnitorHom I)] →
            [CategoryTheory.BraidedCategory C] →
              {X : CategoryTheory.Over I} →
                {A : C} → (A ⟶ (CategoryTheory.Over.sections I).obj X) → ((CategoryTheory.toOver I).obj A ⟶ X)
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Algebra.Hom.ext_iff : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {F : CategoryTheory.Functor C C}
  {A₀ A₁ : CategoryTheory.Endofunctor.Algebra F} {x y : A₀.Hom A₁}, x = y ↔ x.f = y.f
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instAddCommGroupWithOne : {n : Type u_2} → {A : Type u_5} → [DecidableEq n] → [AddCommGroupWithOne A] → AddCommGroupWithOne (CStarMatrix n n A)
-- Mathlib.Algebra.Polynomial.Degree.Support
Polynomial.as_sum_range_C_mul_X_pow : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R),
  p = ∑ i ∈ Finset.range (p.natDegree + 1), Polynomial.C (p.coeff i) * Polynomial.X ^ i
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.symm_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D), e.symm.functor = e.inverse
-- ProofWidgets.Data.Html
ProofWidgets.Html.element.inj : ∀ {a : String} {a_1 : Array (String × Lean.Json)} {a_2 : Array ProofWidgets.Html} {a_3 : String}
  {a_4 : Array (String × Lean.Json)} {a_5 : Array ProofWidgets.Html},
  ProofWidgets.Html.element a a_1 a_2 = ProofWidgets.Html.element a_3 a_4 a_5 → a = a_3 ∧ a_1 = a_4 ∧ a_2 = a_5
-- Mathlib.Data.Nat.Fib.Zeckendorf
Nat.lt_fib_greatestFib_add_one : ∀ (n : ℕ), n < Nat.fib (n.greatestFib + 1)
-- Mathlib.Order.RelIso.Basic
RelEmbedding.coe_toRelHom : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {f : r ↪r s}, ⇑f.toRelHom = ⇑f
-- Std.Data.Internal.List.Associative
/-- Internal implementation detail of the hash map  -/
Std.Internal.List.getValue? : {α : Type u} → {β : Type v} → [BEq α] → α → List ((_ : α) × β) → Option β
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
/-- If `0 < n`, then `DihedralGroup n` is a finite group.
 -/
DihedralGroup.instFintypeOfNeZeroNat : {n : ℕ} → [NeZero n] → Fintype (DihedralGroup n)
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instRightCancelSemigroup : {α : Type u_1} → [RightCancelSemigroup α] → RightCancelSemigroup (Colex α)
-- Mathlib.Algebra.Polynomial.Expand
Polynomial.map_frobenius_expand : ∀ {R : Type u} [inst : CommSemiring R] (p : ℕ) [inst_1 : ExpChar R p] (f : Polynomial R),
  Polynomial.map (frobenius R p) ((Polynomial.expand R p) f) = f ^ p
-- Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
/-- **Vitali-Carathéodory Theorem**: given an integrable real function `f`, there exists an
integrable function `g < f` which is upper semicontinuous, with integral arbitrarily close to that
of `f`. This function has to be `EReal`-valued in general.  -/
MeasureTheory.exists_upperSemicontinuous_lt_integral_gt : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [BorelSpace α] {μ : MeasureTheory.Measure α}
  [μ.WeaklyRegular] [MeasureTheory.SigmaFinite μ] (f : α → ℝ),
  MeasureTheory.Integrable f μ →
    ∀ {ε : ℝ},
      0 < ε →
        ∃ g,
          (∀ (x : α), g x < ↑(f x)) ∧
            UpperSemicontinuous g ∧
              MeasureTheory.Integrable (fun x => (g x).toReal) μ ∧
                (∀ᵐ (x : α) ∂μ, ⊥ < g x) ∧ ∫ (x : α), f x ∂μ < ∫ (x : α), (g x).toReal ∂μ + ε
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulMon_nc.go : ℤ → Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly
-- Mathlib.Tactic.Ring.Common
/-- Adds two polynomials `va, vb` together to get a normalized result polynomial.

* `0 + b = b`
* `a + 0 = a`
* `a * x + a * y = a * (x + y)` (for `x`, `y` coefficients; uses `evalAddOverlap`)
* `(a₁ + a₂) + (b₁ + b₂) = a₁ + (a₂ + (b₁ + b₂))` (if `a₁.lt b₁`)
* `(a₁ + a₂) + (b₁ + b₂) = b₁ + ((a₁ + a₂) + b₂)` (if not `a₁.lt b₁`)
 -/
Mathlib.Tactic.Ring.Common.evalAdd : {u : Lean.Level} →
  {α : Q(Type u)} →
    {bt : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} →
        Mathlib.Tactic.Ring.Common.RingCompute bt sα →
          Mathlib.Tactic.Ring.Common.RingCompute Mathlib.Tactic.Ring.Common.btℕ Mathlib.Tactic.Ring.Common.sℕ →
            {a b : Q(«$α»)} →
              Mathlib.Tactic.Ring.Common.ExSum bt sα a →
                Mathlib.Tactic.Ring.Common.ExSum bt sα b →
                  Lean.MetaM (Mathlib.Tactic.Ring.Common.Result (Mathlib.Tactic.Ring.Common.ExSum bt sα) q(«$a» + «$b»))
-- Mathlib.Topology.Algebra.Module.Equiv
/-- The product of topological modules is four-way commutative up to continuous linear isomorphism.
This is `LinearEquiv.prodProdProdComm` prodAssoc as a continuous linear equivalence.  -/
ContinuousLinearEquiv.prodProdProdComm : (R : Type u_8) →
  (M₁ : Type u_9) →
    (M₂ : Type u_10) →
      (M₃ : Type u_11) →
        (M₄ : Type u_12) →
          [inst : Semiring R] →
            [inst_1 : AddCommMonoid M₁] →
              [inst_2 : AddCommMonoid M₂] →
                [inst_3 : AddCommMonoid M₃] →
                  [inst_4 : AddCommMonoid M₄] →
                    [inst_5 : Module R M₁] →
                      [inst_6 : Module R M₂] →
                        [inst_7 : Module R M₃] →
                          [inst_8 : Module R M₄] →
                            [inst_9 : TopologicalSpace M₁] →
                              [inst_10 : TopologicalSpace M₂] →
                                [inst_11 : TopologicalSpace M₃] →
                                  [inst_12 : TopologicalSpace M₄] → ((M₁ × M₂) × M₃ × M₄) ≃L[R] (M₁ × M₃) × M₂ × M₄
-- Mathlib.Analysis.Normed.Group.Pointwise
sphere_sub_singleton : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (δ : ℝ) (x y : E), Metric.sphere x δ - {y} = Metric.sphere (x - y) δ
-- Mathlib.Order.Filter.NAry
Filter.NeBot.map₂ : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {f : Filter α} {g : Filter β},
  f.NeBot → g.NeBot → (Filter.map₂ m f g).NeBot
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.endofunctorMonoidalCategory_associator_inv_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (F G H : CategoryTheory.Functor C C) (X : C),
  (CategoryTheory.MonoidalCategoryStruct.associator F G H).inv.app X =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.MonoidalCategoryStruct.tensorObj F (CategoryTheory.MonoidalCategoryStruct.tensorObj G H)).obj X)
-- Lean.Elab.Tactic.Omega.OmegaM
/-- The internal state for the `OmegaM` monad, recording previously encountered atoms.  -/
Lean.Elab.Tactic.Omega.State : Type