mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.instOrderBot : {X : AlgebraicGeometry.Scheme} → OrderBot X.IdealSheafData
-- Mathlib.Data.Matrix.Reflection
Matrix.Exists.eq_2 : ∀ {α : Type u_1} (x n : ℕ) (x_1 : Matrix (Fin n.succ) (Fin x) α → Prop),
  Matrix.Exists x_1 = FinVec.Exists fun r => Matrix.Exists fun A => x_1 (Matrix.of (Matrix.vecCons r A))
-- Mathlib.Data.List.Permutation
List.map_permutationsAux2' : ∀ {α : Type u_1} {β : Type u_2} {α' : Type u_3} {β' : Type u_4} (g : α → α') (g' : β → β') (t : α) (ts ys : List α)
  (r : List β) (f : List α → β) (f' : List α' → β'),
  (∀ (a : List α), g' (f a) = f' (List.map g a)) →
    List.map g' (List.permutationsAux2 t ts r ys f).2 =
      (List.permutationsAux2 (g t) (List.map g ts) (List.map g' r) (List.map g ys) f').2
-- Mathlib.LinearAlgebra.Projectivization.Subspace
/-- If a set of points is a subset of another set of points, then its span will be contained in the
span of that set.  -/
Projectivization.Subspace.monotone_span : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
  Monotone Projectivization.Subspace.span
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.c₆.eq_1 : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R), W.c₆ = -W.b₂ ^ 3 + 36 * W.b₂ * W.b₄ - 216 * W.b₆
-- Init.Grind.AC
Lean.Grind.AC.simp_suffix_cert.eq_1 : ∀ (lhs rhs head s s' : Lean.Grind.AC.Seq),
  Lean.Grind.AC.simp_suffix_cert lhs rhs head s s' = (s.beq' (head.concat_k lhs)).and' (s'.beq' (head.concat_k rhs))
-- Batteries.Data.List.Scan
List.take_partialSums : ∀ {α : Type u_1} {i : ℕ} [inst : Add α] [inst_1 : Zero α] {l : List α},
  List.take (i + 1) l.partialSums = (List.take i l).partialSums
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α Unit cmp} [inst : Std.TransCmp cmp] {l : List α} {k : α},
  k ∈ t → (t.insertManyIfNewUnit l).getKey? k = t.getKey? k
-- Mathlib.Analysis.Convex.LinearIsometry
LinearIsometryEquiv.strictConvex_preimage : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedField 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : SeminormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : SeminormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] {s : Set F} (e : E ≃ₗᵢ[𝕜] F), StrictConvex 𝕜 (⇑e ⁻¹' s) ↔ StrictConvex 𝕜 s
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_fst_snd : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst f g)
          (CategoryTheory.Limits.pullback.fst f g))
        (CategoryTheory.Limits.pullback.snd f g)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd g g) g) f)
      (CategoryTheory.Limits.pullback.fst g g)
-- Mathlib.Algebra.Tropical.BigOperators
trop_sInf_image : ∀ {R : Type u_1} {S : Type u_2} [inst : ConditionallyCompleteLinearOrder R] (s : Finset S) (f : S → WithTop R),
  Tropical.trop (sInf (f '' ↑s)) = ∑ i ∈ s, Tropical.trop (f i)
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.NatTrans.whiskerRight_app_tensor_app : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {C : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.MonoidalCategory C]
  {F G F' G' : CategoryTheory.Functor J C} (α : F ⟶ F') (β : G ⟶ G') {X Y : J} (f : X ⟶ Y) (X' : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (F.map f) (G.obj X'))
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (α.app Y) (β.app X')) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (α.app X) (β.app X'))
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (F'.map f) (G'.obj X'))
-- Mathlib.RingTheory.FractionalIdeal.Norm
FractionalIdeal.coeIdeal_absNorm : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] [inst_2 : Module.Free ℤ R]
  [inst_3 : Module.Finite ℤ R] {K : Type u_2} [inst_4 : CommRing K] [inst_5 : Algebra R K] [inst_6 : IsFractionRing R K]
  (I₀ : Ideal R), FractionalIdeal.absNorm ↑I₀ = ↑(Ideal.absNorm I₀)
-- Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction
CategoryTheory.ParametrizedAdjunction.inl_arrowHomEquiv_symm_apply_left : ∀ {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₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)}
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} (adj₂ : F ⊣₂ G) {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁}
  {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} {X₃ Y₃ : C₃} {f₃ : X₃ ⟶ Y₃} (sq₁₂ : F.PushoutObjObj f₁ f₂) (sq₁₃ : G.PullbackObjObj f₁ f₃)
  (β : CategoryTheory.Arrow.mk f₂ ⟶ CategoryTheory.Arrow.mk sq₁₃.π),
  CategoryTheory.CategoryStruct.comp sq₁₂.inl (CategoryTheory.Arrow.Hom.left ((adj₂.arrowHomEquiv sq₁₂ sq₁₃).symm β)) =
    adj₂.homEquiv.symm (CategoryTheory.Arrow.Hom.left β)
-- Mathlib.Algebra.Pointwise.Stabilizer
AddAction.mem_stabilizer_set : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] {a : G} {s : Set α},
  a ∈ AddAction.stabilizer G s ↔ ∀ (b : α), a +ᵥ b ∈ s ↔ b ∈ s
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctor.comp_mapId_hom : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] {D : Type u₃}
  [inst_2 : CategoryTheory.Bicategory D] (F : CategoryTheory.StrictPseudofunctor B C)
  (G : CategoryTheory.StrictPseudofunctor C D) (a : B),
  ((F.comp G).mapId a).hom = CategoryTheory.CategoryStruct.comp (G.map₂ (F.mapId a).hom) (G.mapId (F.obj a)).hom
-- Lean.Data.JsonRpc
Lean.JsonRpc.MessageKind.request.sizeOf_spec : sizeOf Lean.JsonRpc.MessageKind.request = 1
-- Mathlib.NumberTheory.NumberField.FractionalIdeal
NumberField.basisOfFractionalIdeal.eq_1 : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ),
  NumberField.basisOfFractionalIdeal K I =
    Module.Basis.ofIsLocalizedModule ℚ (nonZeroDivisors ℤ) (↑ℤ (↑↑I).subtype) (NumberField.fractionalIdealBasis K ↑I)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.div_vle_iff : ∀ {K : Type u_2} [inst : DivisionRing K] [inst_1 : ValuativeRel K] {a b c : K}, c ≠ 0 → (a / c ≤ᵥ b ↔ a ≤ᵥ b * c)
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.getD_insertMany_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List α} {k fallback : α}, k ∉ m → l.contains k = false → (m.insertMany l).getD k fallback = fallback
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
ModelWithCorners.IsInteriorPoint.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] (x : M),
  I.IsInteriorPoint x = (↑(extChartAt I x) x ∈ interior (Set.range ↑I))
-- Mathlib.Analysis.Polynomial.MahlerMeasure
Polynomial.mapMahlerMeasure_one : ∀ {A : Type u_1} [inst : Semiring A] (v : A →+* ℂ), Polynomial.mapMahlerMeasure 1 v = 1
-- Mathlib.Topology.Separation.Connected
PreconnectedSpace.trivial_of_discrete : ∀ {X : Type u_1} [inst : TopologicalSpace X] [PreconnectedSpace X] [DiscreteTopology X], Subsingleton X
-- Mathlib.Analysis.Analytic.Constructions
/-- Eta-expanded form of `AnalyticOn.inv`

---

`(f x)⁻¹` is analytic away from `f x = 0`  -/
AnalyticOn.fun_inv : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝕝 : Type u_8} [inst_3 : NormedDivisionRing 𝕝] [inst_4 : NormedAlgebra 𝕜 𝕝] {f : E → 𝕝}
  {s : Set E}, AnalyticOn 𝕜 f s → (∀ x ∈ s, f x ≠ 0) → AnalyticOn 𝕜 (fun i => (f i)⁻¹) s
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofReal_balance : ∀ {K : Type u_1} [inst : RCLike K] {ι : Type u_3} [inst_1 : Fintype ι] (f : ι → ℝ) (i : ι),
  ↑(Fintype.balance f i) = Fintype.balance (RCLike.ofReal ∘ f) i
-- Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
HomotopicalAlgebra.FibrantBrownFactorization.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          (toMapFactorizationData :
              (HomotopicalAlgebra.trivialCofibrations C).MapFactorizationData (HomotopicalAlgebra.fibrations C) f) →
            (r : toMapFactorizationData.Z ⟶ X) →
              autoParam
                  (CategoryTheory.CategoryStruct.comp toMapFactorizationData.i r = CategoryTheory.CategoryStruct.id X)
                  HomotopicalAlgebra.FibrantBrownFactorization.i_r._autoParam →
                autoParam (HomotopicalAlgebra.Fibration r)
                    HomotopicalAlgebra.FibrantBrownFactorization.fibration_r._autoParam →
                  HomotopicalAlgebra.FibrantBrownFactorization f
-- Mathlib.Tactic.Simps.Basic
/-- TransparencyMode used to reduce the right-hand side in order to detect whether it is a
constructor. Note: was `none` in Lean 3  -/
Simps.Config.rhsMd : Simps.Config → Lean.Meta.TransparencyMode
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.det_eq_elem_of_subsingleton : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] [Subsingleton n]
  (A : Matrix n n R) (k : n), A.det = A k k
-- Mathlib.Topology.Algebra.Group.GroupTopology
/-- A version of the global `continuous_neg` suitable for dot notation.  -/
AddGroupTopology.continuous_neg' : ∀ {α : Type u} [inst : AddGroup α] (g : AddGroupTopology α), Continuous Neg.neg
-- Mathlib.Data.Setoid.Basic
/-- Equivalence closure is idempotent.  -/
Setoid.eqvGen_idem : ∀ {α : Type u_1} (r : α → α → Prop), Relation.EqvGen.setoid ⇑(Relation.EqvGen.setoid r) = Relation.EqvGen.setoid r
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.instCancelMonoid : {α : Type u_1} → CancelMonoid (FreeMonoid α)
-- Mathlib.RingTheory.PolynomialAlgebra
PolyEquivTensor.toFunLinear_mul_tmul_mul_aux_2 : ∀ (R : Type u_1) (A : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (k : ℕ) (a₁ a₂ : A)
  (p₁ p₂ : Polynomial R),
  a₁ * a₂ * (algebraMap R A) ((p₁ * p₂).coeff k) =
    ∑ x ∈ Finset.HasAntidiagonal.antidiagonal k,
      a₁ * (algebraMap R A) (p₁.coeff x.1) * (a₂ * (algebraMap R A) (p₂.coeff x.2))
-- Init.Data.String.Basic
String.Slice.replaceStartEnd! : (s : String.Slice) → s.Pos → s.Pos → String.Slice
-- Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Asymptotics.IsBigO.mul_atTop_rpow_natCast_of_isBigO_rpow : ∀ {E : Type u_2} [inst : SeminormedRing E] (a b c : ℝ) {f g : ℕ → E},
  (f =O[Filter.atTop] fun n => ↑n ^ a) →
    (g =O[Filter.atTop] fun n => ↑n ^ b) → a + b ≤ c → (f * g) =O[Filter.atTop] fun n => ↑n ^ c
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.norm_condExpInd_apply_le : ∀ {α : Type u_1} {G : Type u_4} [inst : NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {s : Set α} [inst_1 : NormedSpace ℝ G] {hm : m ≤ m0} [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)] (x : G),
  ‖(MeasureTheory.condExpInd G hm μ s) x‖ ≤ μ.real s * ‖x‖
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.entryAtIdx!.eq_def : ∀ {α : Type u} {β : Type v} [inst : Inhabited (α × β)] (x : Std.DTreeMap.Internal.Impl α fun x => β) (x_1 : ℕ),
  Std.DTreeMap.Internal.Impl.Const.entryAtIdx! x x_1 =
    match x, x_1 with
    | Std.DTreeMap.Internal.Impl.leaf, x =>
      panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Queries" "Std.DTreeMap.Internal.Impl.Const.entryAtIdx!" 870 16
        "Out-of-bounds access"
    | Std.DTreeMap.Internal.Impl.inner size k v l r, n =>
      match compare n l.size with
      | Ordering.lt => Std.DTreeMap.Internal.Impl.Const.entryAtIdx! l n
      | Ordering.eq => (k, v)
      | Ordering.gt => Std.DTreeMap.Internal.Impl.Const.entryAtIdx! r (n - l.size - 1)
-- Mathlib.Algebra.Order.Floor.Ring
Int.ceil_le_two_mul : ∀ {k : Type u_4} [inst : Field k] [inst_1 : LinearOrder k] [IsOrderedRing k] [inst_3 : FloorRing k] {a : k},
  2⁻¹ ≤ a → ↑⌈a⌉ ≤ 2 * a
-- Mathlib.CategoryTheory.Monoidal.Category
/-- Notation for the `rightUnitor`: `X ⊗ 𝟙_C ≃ X`  -/
CategoryTheory.MonoidalCategory.termρ_ : Lean.ParserDescr
-- Mathlib.Analysis.Normed.Lp.Finsupp
Finsupp.nndist_def : ∀ {ι : Type u_1} {X : Type u_2} [inst : Zero X] {p : NNReal} [inst_1 : Fact (1 ≤ p)] [inst_2 : PseudoMetricSpace X]
  (f g : WithLp (↑p) (ι →₀ X)), nndist f g = ((Finsupp.zipWith nndist ⋯ f.ofLp g.ofLp).sum fun _i r => r ^ ↑p) ^ (↑p)⁻¹
-- Mathlib.RingTheory.Congruence.Defs
RingCon.instNonUnitalCommSemiringQuotient : {R : Type u_1} → [inst : NonUnitalCommSemiring R] → (c : RingCon R) → NonUnitalCommSemiring c.Quotient
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
monoidHomOfForallMemZpowers_apply_gen : ∀ {G : Type u_2} {G' : Type u_3} [inst : Group G] [inst_1 : Group G'] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g)
  {g' : G'} (hg' : orderOf g' ∣ orderOf g), (monoidHomOfForallMemZpowers hg hg') g = g'
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
integral_sin_pow_three : ∀ {a b : ℝ}, ∫ (x : ℝ) in a..b, Real.sin x ^ 3 = Real.cos a - Real.cos b - (Real.cos a ^ 3 - Real.cos b ^ 3) / 3
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.natCast_val : ∀ {d : ℤ} (n : ℕ), ↑n = { re := ↑n, im := 0 }
-- Init.Data.Int.Order
Int.mul_neg_of_neg_of_pos : ∀ {a b : ℤ}, a < 0 → 0 < b → a * b < 0
-- Mathlib.AlgebraicTopology.SimplicialSet.Finite
SSet.finite_range : ∀ {X Y : SSet} (f : Y ⟶ X) [Y.Finite], (SSet.Subcomplex.range f).toSSet.Finite
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- The structure map of the terminal coalgebra is an isomorphism,
hence endofunctors preserve their terminal coalgebras
 -/
CategoryTheory.Endofunctor.Coalgebra.Terminal.str_isIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  {A : CategoryTheory.Endofunctor.Coalgebra F} (h : CategoryTheory.Limits.IsTerminal A), CategoryTheory.IsIso A.str
-- Init.Data.Iterators.Basic
Std.Iter.isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM : ∀ {α β : Type w} [inst : Std.Iterator α Id β] {it : Std.Iter β} {out : β},
  it.IsPlausibleIndirectOutput out ↔ it.toIterM.IsPlausibleIndirectOutput out
-- Init.Data.Fin.Lemmas
Fin.mod_def : ∀ {n : ℕ} (a m : Fin n), a % m = ⟨↑a % ↑m, ⋯⟩
-- Std.Data.DTreeMap.Raw.Basic
/-- Checks if a mapping for the given key exists and returns the key if it does, otherwise `none`.
The result in the `some` case is guaranteed to be pointer equal to the key in the map.
 -/
Std.DTreeMap.Raw.getKey? : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → α → Option α
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
CategoryTheory.FreeGroupoid.mapCompLift_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} D]
  {E : Type u₂} [inst_2 : CategoryTheory.Groupoid E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E)
  (X : CategoryTheory.FreeGroupoid C),
  (CategoryTheory.FreeGroupoid.mapCompLift F G).inv.app X =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.FreeGroupoid.lift (F.comp G)).obj X)
-- Mathlib.Topology.Algebra.Group.GroupTopology
/-- A version of the global `continuous_add` suitable for dot notation.  -/
AddGroupTopology.continuous_add' : ∀ {α : Type u} [inst : AddGroup α] (g : AddGroupTopology α), Continuous fun p => p.1 + p.2
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LEquiv.symm_toLHom : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} (e : L ≃ᴸ L'), e.symm.toLHom = e.invLHom
-- Mathlib.Algebra.SkewPolynomial.Basic
/-- Though `SkewPolynomial.support` is not definiyionally equal to `SkewMonoidAlgebra.support` we
can relate them using the following lemma.  -/
SkewPolynomial.support_eq_skewMonoidAlgebra_support : ∀ {R : Type u_1} [inst : Semiring R] (p : SkewPolynomial R),
  p.support = Finset.map Multiplicative.toAdd.toEmbedding (SkewMonoidAlgebra.support p)
-- Mathlib.Analysis.Normed.Operator.Basic
/-- The image of the unit ball under a continuous linear map is bounded.  -/
ContinuousLinearMap.unit_le_opNorm : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F)
  (x : E), ‖x‖ ≤ 1 → ‖f x‖ ≤ ‖f‖
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Walk.edgeSet_toSubgraph : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.toSubgraph.edgeSet = p.edgeSet
-- Mathlib.Algebra.Order.Ring.Unbundled.Rat
Rat.num_lt_denom_iff : ∀ {q : ℚ}, q.num < ↑q.den ↔ q < 1
-- Init.Data.String.Iterator
/-- Creates an iterator at the beginning of the string.

This is a no-longer-supported legacy API that will be removed in a future release. You should use
`String.Pos` instead, which is similar, but safer. To iterate over a string `s`, start with
`p : s.startPos`, advance it using `p.next`, access the current character using `p.get` and
check if the position is at the end using `p = s.endPos` or `p.IsAtEnd`.
 -/
String.Legacy.iter : String → String.Legacy.Iterator
-- Mathlib.Order.Filter.CardinalInter
Filter.eventually_cardinal_forall : ∀ {ι α : Type u} {c : Cardinal.{u}} {l : Filter α} [CardinalInterFilter l c] {p : α → ι → Prop},
  Cardinal.mk ι < c → ((∀ᶠ (x : α) in l, ∀ (i : ι), p x i) ↔ ∀ (i : ι), ∀ᶠ (x : α) in l, p x i)
-- Mathlib.Algebra.Homology.Embedding.TruncGE
HomologicalComplex.truncGE'XIso.eq_1 : ∀ {ι : 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') [inst_2 : e.IsTruncGE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  {i : ι} {i' : ι'} (hi' : e.f i = i') (hi : ¬e.BoundaryGE i),
  K.truncGE'XIso e hi' hi = HomologicalComplex.truncGE'.XIso K e hi ≪≫ CategoryTheory.eqToIso ⋯
-- Mathlib.Order.Hom.Basic
OrderIso.dual_symm_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] (f : α ≃o β) (x : βᵒᵈ),
  f.dual.symm x = OrderDual.toDual (f.symm (OrderDual.ofDual x))
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
mvfderiv.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_8} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] (g : M → F) (x : M), d% g x = ↑(NormedSpace.fromTangentSpace (g x)) ∘SL mfderiv% g x
-- Std.Data.DHashMap.Internal.RawLemmas
/-- Internal implementation detail  -/
Std.DHashMap.Internal.Raw₀.decidableEquiv : {α : Type u} →
  {β : α → Type v} →
    [inst : BEq α] →
      [LawfulBEq α] →
        [inst_2 : Hashable α] →
          [inst_3 : (k : α) → BEq (β k)] →
            [∀ (k : α), LawfulBEq (β k)] →
              (m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β) → (↑m₁).WF → (↑m₂).WF → Decidable ((↑m₁).Equiv ↑m₂)
-- Mathlib.Topology.Algebra.Module.Basic
instCompleteSpaceSubtypeMemSubmoduleOfIsClosedCoe : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : UniformSpace M]
  [inst_3 : Module R M] [CompleteSpace M] (K : Submodule R M) [c : IsClosed ↑K], CompleteSpace ↥K
-- Mathlib.Data.Finite.Prod
Set.Finite.of_prod_right : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β}, (s ×ˢ t).Finite → s.Nonempty → t.Finite
-- Mathlib.Algebra.Notation.Pi.Basic
Pi.mulSingle_op₂ : ∀ {ι : Type u_1} {M : ι → Type u_6} {N : ι → Type u_7} {O : ι → Type u_8} [inst : (i : ι) → One (M i)]
  [inst_1 : (i : ι) → One (N i)] [inst_2 : (i : ι) → One (O i)] [inst_3 : DecidableEq ι]
  (op : (i : ι) → M i → N i → O i),
  (∀ (i : ι), op i 1 1 = 1) →
    ∀ (i : ι) (x : M i) (y : N i), Pi.mulSingle i (op i x y) = fun j => op j (Pi.mulSingle i x j) (Pi.mulSingle i y j)
-- Mathlib.Order.Hom.Basic
OrderIso.symm_injective : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β], Function.Injective OrderIso.symm
-- Mathlib.Data.NNReal.Defs
NNReal.coe_eq_zero : ∀ {r : NNReal}, ↑r = 0 ↔ r = 0
-- Init.Data.Option.Lemmas
Option.pbind_some : ∀ {α : Type u_1} {a : α} {α_1 : Type u_2} {f : (a_1 : α) → some a = some a_1 → Option α_1}, (some a).pbind f = f a ⋯
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.stRun.eq_3 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} {k : K} (f : σ → Option (Γ k) → σ),
  Turing.TM2to1.stRun (Turing.TM2to1.StAct.pop f) = Turing.TM2.Stmt.pop k f
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.contains_of_contains_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k a : α},
  (t.erase k).contains a = true → t.contains a = true
-- Mathlib.Data.ENNReal.Basic
ENNReal.iSup_ne_top : ∀ {α : Type u_1} [inst : CompleteLattice α] (f : ENNReal → α), ⨆ x, ⨆ (_ : x ≠ ⊤), f x = ⨆ x, f ↑x
-- Mathlib.Algebra.Order.GroupWithZero.Basic
pow_left_monotoneOn : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : Preorder M₀] {n : ℕ} [PosMulMono M₀] [MulPosMono M₀],
  MonotoneOn (fun a => a ^ n) {x | 0 ≤ x}
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Complex.differentiableAt_cosh : ∀ {x : ℂ}, DifferentiableAt ℂ Complex.cosh x
-- Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
MeasureTheory.eLpNorm_smul_le_eLpNorm_mul_eLpNorm_top : ∀ {𝕜 : Type u_1} {α : Type u_2} {E : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedRing 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : MulActionWithZero 𝕜 E] [IsBoundedSMul 𝕜 E]
  (p : ENNReal) (f : α → E) {φ : α → 𝕜},
  MeasureTheory.AEStronglyMeasurable φ μ →
    MeasureTheory.eLpNorm (φ • f) p μ ≤ MeasureTheory.eLpNorm φ p μ * MeasureTheory.eLpNorm f ⊤ μ
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instAddCommSemigroupOfAddOpposite : {M : Type u_1} → [AddCommSemigroup Mᵃᵒᵖ] → AddCommSemigroup Mᵈᵃᵃ
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurableDiv.toMeasurableInv : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : Group α] [MeasurableDiv α], MeasurableInv α
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Impl.toListModel.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3) →
      (x : Std.DTreeMap.Internal.Impl α β) →
        (Unit → motive Std.DTreeMap.Internal.Impl.leaf) →
          ((size : ℕ) →
              (k : α) →
                (v : β k) →
                  (l r : Std.DTreeMap.Internal.Impl α β) → motive (Std.DTreeMap.Internal.Impl.inner size k v l r)) →
            motive x
-- Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
/-- Any linearly ordered abelian group that is locally finite embeds into `Multiplicative ℤ`.  -/
LocallyFiniteOrder.orderMonoidHom : (G : Type u_3) →
  [inst : CommGroup G] →
    [inst_1 : LinearOrder G] → [IsOrderedMonoid G] → [LocallyFiniteOrder G] → G →*o Multiplicative ℤ
-- Mathlib.Data.Set.Card
Set.ncard_pos : ∀ {α : Type u_1} {s : Set α}, autoParam s.Finite Set.ncard_pos._auto_1 → (0 < s.ncard ↔ s.Nonempty)
-- Mathlib.Algebra.GroupWithZero.Opposite
MulOpposite.instGroupWithZero : {α : Type u_1} → [GroupWithZero α] → GroupWithZero αᵐᵒᵖ
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- State for all `IntModule` types detected by `grind`.  -/
Lean.Meta.Grind.Arith.Linear.State : Type