mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.ObjectProperty.Shift
CategoryTheory.ObjectProperty.instIsStableUnderShiftByBot : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u_2} [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (a : A), ⊥.IsStableUnderShiftBy a
-- Mathlib.Tactic.ApplyFun
/-- **Alias** of the forward direction of `OrderIso.lt_iff_lt`. -/
Mathlib.Tactic.ApplyFun.lt_of_lt : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β) {x y : α}, e x < e y → x < y
-- Init.Data.SInt.Bitwise
Int32.or_zero : ∀ {a : Int32}, a ||| 0 = a
-- Mathlib.Algebra.Category.MonCat.Basic
/-- The underlying monoid homomorphism.  -/
AddMonCat.Hom.hom' : {A B : AddMonCat} → A.Hom B → ↑A →+ ↑B
-- Mathlib.Topology.Algebra.IsUniformGroup.Constructions
isUniformAddGroup_inf : ∀ {G : Type u_1} [inst : AddGroup G] {u₁ u₂ : UniformSpace G},
  IsUniformAddGroup G → IsUniformAddGroup G → IsUniformAddGroup G
-- Mathlib.Topology.Compactness.Compact
instCompactSpaceSigmaOfFinite : ∀ {ι : Type u_1} {X : ι → Type u_2} [Finite ι] [inst : (i : ι) → TopologicalSpace (X i)]
  [∀ (i : ι), CompactSpace (X i)], CompactSpace ((i : ι) × X i)
-- Mathlib.Analysis.FunctionalSpaces.SobolevInequality
MeasureTheory.eLpNormLESNormFDerivOfLeConst.congr_simp : ∀ (F : Type u_6) [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {E : Type u_7} [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace ℝ E] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E] [inst_6 : FiniteDimensional ℝ E]
  (μ μ_1 : MeasureTheory.Measure E) (e_μ : μ = μ_1) [inst_7 : μ.IsAddHaarMeasure] [inst_8 : FiniteDimensional ℝ F]
  (s s_1 : Set E),
  s = s_1 →
    ∀ (p p_1 : NNReal),
      p = p_1 →
        ∀ (q q_1 : NNReal),
          q = q_1 →
            MeasureTheory.eLpNormLESNormFDerivOfLeConst F μ s p q =
              MeasureTheory.eLpNormLESNormFDerivOfLeConst F μ_1 s_1 p_1 q_1
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.instSubsingletonOfNatNat : ∀ {R : Type u_1} [inst : CommMonoidWithZero R], Subsingleton (DirichletCharacter R 1)
-- Std.Sync.Channel
/-- Whether the channel is closed already.
 -/
_private.Std.Sync.Channel.0.Std.CloseableChannel.Unbounded.State.closed : {α : Type} → Std.CloseableChannel.Unbounded.State✝ α → Bool
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.bot_eq_initial_to : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasInitial C]
  [inst_2 : CategoryTheory.Limits.InitialMonoClass C] {B : C},
  ⊥ = CategoryTheory.Subobject.mk (CategoryTheory.Limits.initial.to B)
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.HoCat.adjCounit'_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  (X : HomotopicalAlgebra.BifibrantObject C),
  HomotopicalAlgebra.CofibrantObject.HoCat.adjCounit'.app (HomotopicalAlgebra.BifibrantObject.toHoCat.obj X) =
    HomotopicalAlgebra.BifibrantObject.toHoCat.map
      (HomotopicalAlgebra.BifibrantObject.homMk
        (HomotopicalAlgebra.CofibrantObject.mk X.obj).iBifibrantResolutionObj.hom)
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
lineDifferentiableWithinAt_smul_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {f : E → F} {s : Set E}
  {x v : E} {c : 𝕜}, c ≠ 0 → (LineDifferentiableWithinAt 𝕜 f s x (c • v) ↔ LineDifferentiableWithinAt 𝕜 f s x v)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.contains_of_contains_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {v : β k},
  (m.insert k v).contains a = true → (k == a) = false → m.contains a = true
-- Mathlib.GroupTheory.QuotientGroup.Defs
AddCon.mem_addSubgroup_iff : ∀ {G : Type u_1} [inst : AddGroup G] {c : AddCon G} {x : G}, x ∈ c.addSubgroup ↔ c x 0
-- Mathlib.Algebra.Group.Subgroup.Pointwise
inv_coe_set : ∀ {G : Type u_2} {S : Type u_4} [inst : InvolutiveInv G] [inst_1 : SetLike S G] [InvMemClass S G] {H : S}, (↑H)⁻¹ = ↑H
-- Mathlib.Analysis.Normed.Order.Lattice
norm_inf_sub_inf_le_norm : ∀ {α : Type u_1} [inst : NormedAddCommGroup α] [inst_1 : Lattice α] [HasSolidNorm α] [IsOrderedAddMonoid α] (x y z : α),
  ‖x ⊓ z - y ⊓ z‖ ≤ ‖x - y‖
-- Mathlib.Tactic.Simps.Basic
/-- A variant of `String.splitOn` that does not split `toFoo_1` into `toFoo` and `1`.  -/
_private.Mathlib.Tactic.Simps.Basic.0.Simps.splitOnNotNumber : String → String → List String
-- Mathlib.Geometry.Euclidean.Triangle
/-- The **sum of the angles of a triangle** (possibly degenerate, where the triangle is a line),
oriented angles at point.  -/
EuclideanGeometry.oangle_add_oangle_add_oangle_eq_pi : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [inst_4 : Module.Oriented ℝ V (Fin 2)] [inst_5 : Fact (Module.finrank ℝ V = 2)]
  {p₁ p₂ p₃ : P},
  p₂ ≠ p₁ →
    p₃ ≠ p₂ →
      p₁ ≠ p₃ →
        EuclideanGeometry.oangle p₁ p₂ p₃ + EuclideanGeometry.oangle p₂ p₃ p₁ + EuclideanGeometry.oangle p₃ p₁ p₂ =
          ↑Real.pi
-- Mathlib.Data.Complex.Basic
Complex.I_pow_three : Complex.I ^ 3 = -Complex.I
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- Given two functors which have equivalent categories of cones, we can transport a limiting cone
across the equivalence.
 -/
CategoryTheory.Limits.IsLimit.ofConeEquiv : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {K : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} K] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor J C} →
              {D : Type u₄} →
                [inst_3 : CategoryTheory.Category.{v₄, u₄} D] →
                  {G : CategoryTheory.Functor K D} →
                    (h : CategoryTheory.Limits.Cone G ≌ CategoryTheory.Limits.Cone F) →
                      {c : CategoryTheory.Limits.Cone G} →
                        CategoryTheory.Limits.IsLimit (h.functor.obj c) ≃ CategoryTheory.Limits.IsLimit c
-- Mathlib.Data.Nat.Squarefree
/-- `Squarefree` is multiplicative. Note that the → direction does not require `hmn`
and generalizes to arbitrary commutative monoids. See `Squarefree.of_mul_left` and
`Squarefree.of_mul_right` above for auxiliary lemmas.  -/
Nat.squarefree_mul : ∀ {m n : ℕ}, m.Coprime n → (Squarefree (m * n) ↔ Squarefree m ∧ Squarefree n)
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.submatrix_updateRow_equiv : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [inst : DecidableEq l]
  [inst_1 : DecidableEq m] (A : Matrix m n α) (i : m) (r : n → α) (e : l ≃ m) (f : o ≃ n),
  (A.updateRow i r).submatrix ⇑e ⇑f = (A.submatrix ⇑e ⇑f).updateRow (e.symm i) fun i => r (f i)
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
AddLECancellable.tsub_lt_tsub_iff_left_of_le_of_le : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLT α],
  AddLECancellable b → AddLECancellable (a - b) → b ≤ a → c ≤ a → (a - b < a - c ↔ c < b)
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instAddCommSemigroupOfAddOpposite.eq_1 : ∀ {M : Type u_1} [inst : AddCommSemigroup Mᵃᵒᵖ], DomAddAct.instAddCommSemigroupOfAddOpposite = inst
-- Aesop.Script.StructureDynamic
Aesop.Script.DynStructureM.State.mk.inj : ∀ {perfect perfect_1 : Bool}, { perfect := perfect } = { perfect := perfect_1 } → perfect = perfect_1
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
_private.Mathlib.Analysis.Calculus.FDeriv.Analytic.0.HasFPowerSeriesOnBall.factorial_smul' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {r : ENNReal} (y : E) {n : ℕ} {F : Type (max u v)} [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [CompleteSpace F] {p : FormalMultilinearSeries 𝕜 E F} {f : E → F},
  HasFPowerSeriesOnBall f p x r → (n.factorial • (p n) fun x => y) = (iteratedFDeriv 𝕜 n f x) fun x => y
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.mem_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.LawfulEqCmp cmp]
  [Std.TransCmp cmp], t.WF → ∀ {k : α}, k ∈ t.keys ↔ k ∈ t
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
AddEquiv.withBotCongr_apply : ∀ {α : Type u} {β : Type v} [inst : Add α] [inst_1 : Add β] (e : α ≃+ β) (a : WithBot α),
  e.withBotCongr a = WithBot.map (⇑e) a
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.smul_empty : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {s : Set α}, s • ∅ = ∅
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.mk_one : ∀ {G : Type u_1} [inst : Group G] (N : Subgroup G) [nN : N.Normal], ↑1 = 1
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.alterₘ.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.OrientedOrd α] [inst_2 : Std.LawfulEqOrd α] (k : α)
  (f f_1 : Option (β k) → Option (β k)),
  f = f_1 →
    ∀ (t t_1 : Std.DTreeMap.Internal.Impl α β) (e_t : t = t_1) (h : t.Balanced),
      Std.DTreeMap.Internal.Impl.alterₘ k f t h = Std.DTreeMap.Internal.Impl.alterₘ k f_1 t_1 ⋯
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.mk_le_mk : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace β]
  [inst_2 : Preorder β] {f g : α → β} (hf : MeasureTheory.AEStronglyMeasurable f μ)
  (hg : MeasureTheory.AEStronglyMeasurable g μ),
  MeasureTheory.AEEqFun.mk f hf ≤ MeasureTheory.AEEqFun.mk g hg ↔ f ≤ᵐ[μ] g
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.lift_comp_conePointUniqueUpToIso_inv_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {r s t : CategoryTheory.Limits.Cone F} (P : CategoryTheory.Limits.IsLimit s)
  (Q : CategoryTheory.Limits.IsLimit t) {Z : C} (h : s.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp (Q.lift r)
      (CategoryTheory.CategoryStruct.comp (P.conePointUniqueUpToIso Q).inv h) =
    CategoryTheory.CategoryStruct.comp (P.lift r) h
-- Init.Data.Vector.Find
Vector.find?_eq_some_iff_append : ∀ {α : Type} {n : ℕ} {p : α → Bool} {b : α} {xs : Vector α n},
  Vector.find? p xs = some b ↔
    p b = true ∧
      ∃ k₁ k₂, ∃ (w : n = k₁ + 1 + k₂), ∃ as bs, xs = Vector.cast ⋯ (as.push b ++ bs) ∧ ∀ a ∈ as, (!p a) = true
-- Lean.Parser.Tactic.Doc
_private.Lean.Parser.Tactic.Doc.0.Lean.Parser.Tactic.Doc.getTacticExtensionString.indentLine : String.Slice → String
-- Mathlib.RingTheory.Ideal.Operations
Ideal.mem_span_singleton_mul : ∀ {R : Type u} [inst : CommSemiring R] {x y : R} {I : Ideal R}, x ∈ Ideal.span {y} * I ↔ ∃ z ∈ I, y * z = x
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalSubgroup.instLattice.eq_1 : ∀ {G : Type u_1} [inst : Group G],
  FiniteIndexNormalSubgroup.instLattice =
    { toSemilatticeSup := FiniteIndexNormalSubgroup.instSemilatticeSupFiniteIndexNormalSubgroup,
      inf := SemilatticeInf.inf, inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯ }
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.withAntiquotSuffixSplice.formatter : Lean.SyntaxNodeKind → Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Init.Data.List.Nat.TakeDrop
List.length_take_le : ∀ {α : Type u_1} (i : ℕ) (l : List α), (List.take i l).length ≤ i
-- Mathlib.CategoryTheory.HomCongr
CategoryTheory.Iso.homCongr_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z X₁ Y₁ Z₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) (γ : Z ≅ Z₁)
  (f : X ⟶ Y) (g : Y ⟶ Z),
  (α.homCongr γ) (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp ((α.homCongr β) f) ((β.homCongr γ) g)
-- Mathlib.Data.EReal.Operations
/-- If `a ≤ -b` then `b ≤ -a` on `EReal`.  -/
EReal.le_neg_of_le_neg : ∀ {a b : EReal}, a ≤ -b → b ≤ -a
-- Mathlib.AlgebraicTopology.SimplicialSet.Nerve
/-- Bijection between edges in the nerve of category and morphisms in the category.  -/
CategoryTheory.nerve.homEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {x y : CategoryTheory.ComposableArrows C 0} →
      SSet.Edge x y ≃ (CategoryTheory.nerveEquiv x ⟶ CategoryTheory.nerveEquiv y)
-- Mathlib.Algebra.Squarefree.Basic
Finset.squarefree_prod_of_pairwise_isCoprime : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] [IsCancelMulZero R] [DecompositionMonoid R] {ι : Type u_2} {s : Finset ι}
  {f : ι → R}, (↑s).Pairwise (Function.onFun IsRelPrime f) → (∀ i ∈ s, Squarefree (f i)) → Squarefree (∏ i ∈ s, f i)
-- Std.Internal.UV.TCP
/-- Starts listening for incoming connections on a TCP socket.
 -/
Std.Internal.UV.TCP.Socket.listen : Std.Internal.UV.TCP.Socket → UInt32 → IO Unit
-- Mathlib.Analysis.Analytic.Order
/-- If `g` is analytic at `x`, and `g' x ≠ 0`, then the analytic order of
`f ∘ g` at `x` is the analytic order of `f` at `g x` (even if `f` is not analytic).  -/
analyticOrderAt_comp_of_deriv_ne_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {g : 𝕜 → 𝕜} {z₀ : 𝕜},
  AnalyticAt 𝕜 g z₀ →
    deriv g z₀ ≠ 0 → ∀ [CompleteSpace 𝕜] [CharZero 𝕜], analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀)
-- Mathlib.NumberTheory.LSeries.HurwitzZeta
/-- Reformulation of `hasSum_expZeta_of_one_lt_re` using `LSeriesHasSum`.  -/
HurwitzZeta.LSeriesHasSum_exp : ∀ (a : ℝ) {s : ℂ},
  1 < s.re → LSeriesHasSum (fun x => Complex.exp (2 * ↑Real.pi * Complex.I * ↑a * ↑x)) s (HurwitzZeta.expZeta (↑a) s)
-- Std.Internal.Do.WP.Conjunctive
/-- A meet of postconditions maps below the `wp` of their meet.  -/
Std.Internal.Do.WPConjunctive.wp_meet_wp_le : ∀ {Prog : Type u} {Value : outParam (Type v)} {Pred : outParam (Type w)} {EPred : outParam (Type z)}
  {inst : Std.Internal.Do.Assertion Pred} {inst_1 : Std.Internal.Do.Assertion EPred}
  {inst_2 : Std.Internal.Do.WP Prog Value Pred EPred} [self : Std.Internal.Do.WPConjunctive Prog Value Pred EPred]
  (x : Prog) (Q₁ Q₂ : Value → Pred) (E : EPred),
  Lean.Order.PartialOrder.rel (Lean.Order.meet (Std.Internal.Do.wp x Q₁ E) (Std.Internal.Do.wp x Q₂ E))
    (Std.Internal.Do.wp x (Lean.Order.meet Q₁ Q₂) E)
-- Mathlib.Order.Interval.Basic
NonemptyInterval.le : {α : Type u_1} → [inst : LE α] → LE (NonemptyInterval α)
-- Mathlib.Analysis.Calculus.TangentCone.Seq
/-- In a normed space over a nontrivially normed field,
a point `y` belongs to the tangent cone of a set `s` at `x`
iff there exists a sequence of scalars `c n` and a sequence of points `d n` such that

- `‖c n‖ → ∞` as `n → ∞`;
- `x + d n ∈ s` for sufficiently large `n`;
- `c n • d n` tends to `y`.

Before https://github.com/leanprover-community/mathlib4/pull/34127,
the right-hand side of this equivalence was the definition of the tangent cone.

In most cases, `exists_fun_of_mem_tangentConeAt` and/or `mem_tangentConeAt_of_seq`
can be used to generalize a proof using this lemma to topological vector spaces.
 -/
mem_tangentConeAt_iff_exists_seq_norm_tendsto_atTop : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {x y : E},
  y ∈ tangentConeAt 𝕜 s x ↔
    ∃ c d,
      Filter.Tendsto (fun x => ‖c x‖) Filter.atTop Filter.atTop ∧
        (∀ᶠ (n : ℕ) in Filter.atTop, x + d n ∈ s) ∧ Filter.Tendsto (fun n => c n • d n) Filter.atTop (nhds y)
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.Faithful.id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C], (CategoryTheory.Functor.id C).Faithful
-- Mathlib.Analysis.InnerProductSpace.ProdL2
Submodule.fstL_comp_coe_orthogonalDecomposition : ∀ {𝕜 : Type u_1} {E : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection],
  WithLp.fstL 2 𝕜 ↥K ↥Kᗮ ∘SL ↑↑K.orthogonalDecomposition = K.orthogonalProjectionOnto
-- Mathlib.Data.Fintype.Sets
Set.ssubset_toFinset : ∀ {α : Type u_1} {t : Set α} {s : Finset α} [inst : Fintype ↑t], s ⊂ t.toFinset ↔ ↑s ⊂ t
-- Mathlib.MeasureTheory.Group.FoelnerFilter
IsFoelner.mean_univ_eq_one : ∀ {G : Type u_1} {X : Type u_2} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : Group G]
  [inst_2 : MulAction G X] {ι : Type u_3} {u : Ultrafilter ι} {F : ι → Set X},
  IsFoelner G μ (↑u) F → IsFoelner.mean μ u F Set.univ = 1
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.prop_of_isColimit : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) {J : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} J] [P.IsClosedUnderColimitsOfShape J] {F : CategoryTheory.Functor J C}
  {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c), (∀ (j : J), P (F.obj j)) → P c.pt
-- Mathlib.Topology.ContinuousOn
continuousOn_singleton : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (a : α),
  ContinuousOn f {a}
-- Mathlib.Topology.MetricSpace.Algebra
LipschitzAdd.continuousAdd : ∀ {β : Type u_2} [inst : PseudoMetricSpace β] [inst_1 : AddMonoid β] [LipschitzAdd β], ContinuousAdd β
-- Mathlib.Algebra.GroupWithZero.Range
MonoidWithZeroHom.valueGroup.eq_1 : ∀ {A : Type u_1} {B : Type u_2} [inst : MonoidWithZero A] [inst_1 : MonoidWithZero B] (f : A →*₀ B),
  f.valueGroup = Subgroup.closure ↑f.valueMonoid
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.reflexiveCoforkEquivCofork.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C),
  CategoryTheory.Limits.reflexiveCoforkEquivCofork F =
    (CategoryTheory.Functor.Final.coconesEquiv CategoryTheory.Limits.WalkingParallelPair.inclusionWalkingReflexivePair
            F).symm.trans
      (CategoryTheory.Limits.Cocone.precomposeEquivalence
        (CategoryTheory.Limits.diagramIsoParallelPair
          (CategoryTheory.Limits.WalkingParallelPair.inclusionWalkingReflexivePair.comp F)))
-- Init.Data.UInt.Bitwise
Bool.toUInt16.eq_1 : ∀ (b : Bool), b.toUInt16 = if b = true then 1 else 0
-- Lean.Data.NameMap.Basic
Lean.NameSet : Type
-- Mathlib.RingTheory.IsAdjoinRoot
/-- `IsAdjoinRoot S f` states that the ring `S` can be constructed by adjoining a specified root
of the polynomial `f : R[X]` to `R`.

Compare `PowerBasis R S`, which does not explicitly specify which polynomial we adjoin a root of
(in particular `f` does not need to be the minimal polynomial of the root we adjoin),
and `AdjoinRoot` which constructs a new type.

This is not a typeclass because the choice of root given `S` and `f` is not unique.
 -/
IsAdjoinRoot : {R : Type u} →
  (S : Type v) → [inst : CommSemiring R] → [inst_1 : Semiring S] → [Algebra R S] → Polynomial R → Type (max u v)
-- Mathlib.MeasureTheory.Function.L2Space
_private.Mathlib.MeasureTheory.Function.L2Space.0.MeasureTheory.L2.«term⟪_,_⟫» : Lean.ParserDescr
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_diff!_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF → m₂.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k m₁ = false → (m₁.diff! m₂).getKey? k = none
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
ContinuousMultilinearMap.curryRight.eq_1 : ∀ {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)] [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)]
  [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 Ei G),
  f.curryRight =
    { toFun := fun m => (f.curryRight m).mkContinuous (‖f‖ * ∏ i, ‖m i‖) ⋯, map_update_add' := ⋯,
          map_update_smul' := ⋯ }.mkContinuous
      ‖f‖ ⋯
-- Mathlib.CategoryTheory.FintypeCat
FintypeCat.hom_inv_id_apply : ∀ {X Y : FintypeCat} (f : X ≅ Y) (x : X.obj),
  (CategoryTheory.ConcreteCategory.hom f.inv) ((CategoryTheory.ConcreteCategory.hom f.hom) x) = x
-- Lean.Meta.MonadSimp
Lean.Meta.MonadSimp : (Type → Type) → Type 1
-- Mathlib.Analysis.Normed.Group.Real
instENormedAddCommMonoidENNReal : ENormedAddCommMonoid ENNReal
-- Mathlib.Data.Vector.MapLemmas
List.Vector.mapAccumr₂_mapAccumr₂_right_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ₁ : Type u_6} {σ₂ : Type u_7} {φ : Type u_8} {n : ℕ} {s₁ : σ₁}
  {s₂ : σ₂} (xs : List.Vector α n) (ys : List.Vector β n) (f₁ : α → γ → σ₁ → σ₁ × φ) (f₂ : α → β → σ₂ → σ₂ × γ),
  List.Vector.mapAccumr₂ f₁ xs (List.Vector.mapAccumr₂ f₂ xs ys s₂).2 s₁ =
    have m :=
      List.Vector.mapAccumr₂
        (fun x y x_1 =>
          match x_1 with
          | (s₁, s₂) =>
            have r₂ := f₂ x y s₂;
            have r₁ := f₁ x r₂.2 s₁;
            ((r₁.1, r₂.1), r₁.2))
        xs ys (s₁, s₂);
    (m.1.1, m.2)
-- Mathlib.Analysis.Calculus.ContDiff.Operations
OpenPartialHomeomorph.restrContDiff_target : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (f : OpenPartialHomeomorph E F) (n : WithTop ℕ∞) (hn : n ≠ ↑⊤),
  (OpenPartialHomeomorph.restrContDiff 𝕜 f n hn).target =
    f.target ∩ {y | ContDiffAt 𝕜 n (↑f.symm) y ∧ ContDiffAt 𝕜 n (↑f) (↑f.symm y)}
-- Batteries.Data.List.Basic
/-- `Disjoint l₁ l₂` means that `l₁` and `l₂` have no elements in common.  -/
List.Disjoint : {α : Type u_1} → List α → List α → Prop
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.DiseqCnstrProof.simp_ac : Bool →
  Lean.Grind.AC.Seq → Lean.Meta.Grind.AC.EqCnstr → Lean.Meta.Grind.AC.DiseqCnstr → Lean.Meta.Grind.AC.DiseqCnstrProof
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.findFinIdx?.loop.eq_def : ∀ {α : Type u} (p : α → Bool) (as : Array α) (j : ℕ),
  Array.findFinIdx?.loop✝ p as j =
    if h : j < as.size then if p as[j] = true then some ⟨j, h⟩ else Array.findFinIdx?.loop✝ p as (j + 1) else none
-- Init.Data.Array.Attach
Array.back?_pmap : ∀ {α : Type u_1} {β : Type u_2} {P : α → Prop} {f : (a : α) → P a → β} {xs : Array α} (H : ∀ a ∈ xs, P a),
  (Array.pmap f xs H).back? =
    Option.map
      (fun x =>
        match x with
        | ⟨a, m⟩ => f a ⋯)
      xs.attach.back?
-- Mathlib.NumberTheory.ModularForms.QExpansion
/-- Version of `exp_decay_atImInfty` stating a less precise result but easier to apply in practice
(not specifying the growth rate precisely). Note that the `Fact` hypothesis is automatically
synthesized for arithmetic subgroups.  -/
ModularFormClass.exp_decay_atImInfty' : ∀ {k : ℤ} {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} (f : F)
  [ModularFormClass F Γ k] [Γ.HasDetPlusMinusOne] [DiscreteTopology ↥Γ] [Fact (IsCusp OnePoint.infty Γ)],
  UpperHalfPlane.IsZeroAtImInfty ⇑f → ∃ c > 0, ⇑f =O[UpperHalfPlane.atImInfty] fun τ => Real.exp (-c * τ.im)
-- Mathlib.Analysis.Analytic.Constructions
/-- Eta-expanded form of `AnalyticAt.neg` -/
AnalyticAt.fun_neg : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E},
  AnalyticAt 𝕜 f x → AnalyticAt 𝕜 (fun i => -f i) x
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
Summable.prod : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommGroup α] [inst_1 : UniformSpace α] [IsUniformAddGroup α]
  [CompleteSpace α] {f : β × γ → α}, Summable f → Summable fun b => ∑' (c : γ), f (b, c)
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.all_filterMap : ∀ {α β β' : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Std.IteratorLoop α Id Id]
  [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β} {f : β → Option β'} {p : β' → Bool},
  Std.Iter.all p (Std.Iter.filterMap f it) =
    Std.Iter.all
      (fun x =>
        match f x with
        | some fx => p fx
        | none => true)
      it