mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.TightNormed
/-- In a finite-dimensional inner product space, the range of a sequence of measures
`μ : ℕ → Measure E` is tight if and only if the function
`r : ℝ ↦ limsup (fun n ↦ μ n {x | r < ‖⟪y, x⟫_𝕜‖}) atTop` tends to `0` at infinity for all `y`.  -/
MeasureTheory.isTightMeasureSet_range_iff_tendsto_limsup_inner : ∀ {E : Type u_1} {mE : MeasurableSpace E} [inst : NormedAddCommGroup E] (𝕜 : Type u_2) [inst_1 : RCLike 𝕜]
  [inst_2 : InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [BorelSpace E] {μ : ℕ → MeasureTheory.Measure E}
  [∀ (i : ℕ), MeasureTheory.IsFiniteMeasure (μ i)],
  MeasureTheory.IsTightMeasureSet (Set.range μ) ↔
    ∀ (y : E),
      Filter.Tendsto (fun r => Filter.limsup (fun n => (μ n) {x | r < ‖inner 𝕜 y x‖}) Filter.atTop) Filter.atTop
        (nhds 0)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey?_le_minKey?_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp] (h : t.WF)
  {k km kme : α} (hkme : (t.erase k).minKey? = some kme), t.minKey?.get ⋯ = km → (cmp km kme).isLE = true
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.instIsIsoH₀Inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreOneHypercover S} (e : E ≅ F)
  (i : F.I₀), CategoryTheory.IsIso (e.inv.h₀ i)
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.succ_def : ∀ (c : Cardinal.{u_1}), Order.succ c = sInf {c' | c < c'}
-- Mathlib.RingTheory.MvPowerSeries.Inverse
MvPowerSeries.mul_inv_rev : ∀ {σ : Type u_1} {k : Type u_3} [inst : Field k] (φ ψ : MvPowerSeries σ k), (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹
-- Mathlib.Order.Filter.Basic
/-- **Alias** of `Filter.sdiff_mem`. -/
Filter.diff_mem : ∀ {α : Type u} {f : Filter α} {s t : Set α}, s ∈ f → tᶜ ∈ f → s \ t ∈ f
-- Mathlib.Order.Disjoint
/-- **Alias** of the forward direction of `disjoint_self`. -/
Disjoint.eq_bot_of_self : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, Disjoint a a → a = ⊥
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If the oriented angle between three points is `-π / 2`, the unoriented angle is `π / 2`.  -/
EuclideanGeometry.angle_eq_pi_div_two_of_oangle_eq_neg_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P}, EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(-Real.pi / 2) → EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2
-- Mathlib.Algebra.Ring.Opposite
AddOpposite.instCommSemiring : {R : Type u_1} → [CommSemiring R] → CommSemiring Rᵃᵒᵖ
-- Mathlib.RingTheory.RingHomProperties
/-- A property of ring homomorphisms `Q` codescends along `Q'` if whenever
`R' →+* R' ⊗[R] S` satisfies `Q` and `R →+* R'` satisfies `Q'`, then `R →+* S` satisfies `Q`.  -/
RingHom.CodescendsAlong : ({R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) →
  ({R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) → Prop
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.toComp_toAlgHom_monomial : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_3} {T : Type u_7} [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T] (Q : Algebra.Generators S T ι') (P : Algebra.Generators R S ι) (j : ι →₀ ℕ) (a : R),
  (Q.toComp P).toAlgHom ((MvPolynomial.monomial j) a) = (MvPolynomial.monomial (Finsupp.sumElim 0 j)) a
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.ker_comp_eq_sup : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_3} {T : Type u_7} [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T] (Q : Algebra.Generators S T ι') (P : Algebra.Generators R S ι),
  (Q.comp P).ker = Ideal.map (Q.toComp P).toAlgHom P.ker ⊔ Ideal.comap (Q.ofComp P).toAlgHom Q.ker
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.integralModel_b₄_eq : ∀ (R : Type u_1) [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K] (W : WeierstrassCurve K)
  [hW : WeierstrassCurve.IsIntegral R W], (algebraMap R K) (WeierstrassCurve.integralModel R W).b₄ = W.b₄
-- Mathlib.CategoryTheory.Preadditive.CommGrp_
CategoryTheory.Preadditive.commGrpEquivalence_functor_obj_X : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.BraidedCategory C] (X : C),
  (CategoryTheory.Preadditive.commGrpEquivalence.functor.obj X).X = X
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.inducedFunctorOfEquiv : ∀ {D : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} D] {C' : Type u_1} (e : C' ≃ D),
  (CategoryTheory.inducedFunctor ⇑e).IsEquivalence
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback₃.p₁₃_p : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S}
  {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃}
  {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} (h : CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃),
  CategoryTheory.CategoryStruct.comp h.p₁₃ h₁₃.p = h.p
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
/-- Oplax left unity.  -/
CategoryTheory.OplaxFunctor.map₂_leftUnitor_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (self : CategoryTheory.OplaxFunctor B CategoryTheory.Cat)
  {a b : B} (f : a ⟶ b) (X : ↑(self.obj a)),
  (self.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom).toNatTrans.app X =
    CategoryTheory.CategoryStruct.comp ((self.mapComp (CategoryTheory.CategoryStruct.id a) f).toNatTrans.app X)
      ((self.map f).toFunctor.map ((self.mapId a).toNatTrans.app X))
-- Mathlib.Analysis.Normed.Group.Uniform
LocallyLipschitzOn.sub : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedAddCommGroup E] [inst_1 : PseudoEMetricSpace α] {f g : α → E}
  {s : Set α}, LocallyLipschitzOn s f → LocallyLipschitzOn s g → LocallyLipschitzOn s fun x => f x - g x
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.below.add_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  {motive : (a a_1 : CommRingCat.Colimits.Prequotient F) → CommRingCat.Colimits.Relation F a a_1 → Prop}
  (x x' y : CommRingCat.Colimits.Prequotient F) (x_1 : CommRingCat.Colimits.Relation F x x'),
  CommRingCat.Colimits.Relation.below x_1 → motive x x' x_1 → CommRingCat.Colimits.Relation.below ⋯
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.recoverUnindent : ℕ → Lean.Parser.ParserFn → optParam Lean.Parser.ParserFn Lean.Doc.Parser.skipFn → Lean.Parser.ParserFn
-- Mathlib.Topology.Closure
interior_univ : ∀ {X : Type u} [inst : TopologicalSpace X], interior Set.univ = Set.univ
-- Mathlib.Order.Interval.Finset.Defs
/-- The finset $[a, b]$ of elements `x` such that `a ≤ x` and `x ≤ b`. Basically `Set.Icc a b` as a
finset.  -/
Finset.Icc : {α : Type u_1} → [inst : Preorder α] → [LocallyFiniteOrder α] → α → α → Finset α
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instAddMonoidCoeOfAddSubmonoidClass : {ι : Type u_1} →
  (R : ι → Type u_2) →
    {𝓕 : Filter ι} →
      {S : ι → Type u_3} →
        [inst : (i : ι) → SetLike (S i) (R i)] →
          {B : (i : ι) → S i} →
            [inst_1 : (i : ι) → AddMonoid (R i)] →
              [∀ (i : ι), AddSubmonoidClass (S i) (R i)] →
                AddMonoid (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕)
-- Mathlib.Combinatorics.Quiver.Path
Quiver.Path.comp_nil : ∀ {V : Type u} [inst : Quiver V] {a b : V} (p : Quiver.Path a b), p.comp Quiver.Path.nil = p
-- Mathlib.Algebra.Algebra.Defs
Algebra.linearMap_self : ∀ (R : Type u) [inst : CommSemiring R], Algebra.linearMap R R = LinearMap.id
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprodComparisonNatIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{w, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C]
  [inst_3 : CategoryTheory.Limits.HasBinaryCoproducts D] (A : C)
  [inst_4 : ∀ (B : C), CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison F A B)],
  (CategoryTheory.Limits.coprodComparisonNatIso F A).inv =
    (CategoryTheory.asIso { app := fun B => CategoryTheory.Limits.coprodComparison F A B, naturality := ⋯ }).inv
-- Mathlib.SetTheory.Cardinal.Cofinality.Basic
Order.le_lift_cof_iff : ∀ {α : Type u} [inst : Preorder α] {c : Cardinal.{max u v}},
  c ≤ Cardinal.lift.{v, u} (Order.cof α) ↔ ∀ (s : Set α), IsCofinal s → c ≤ Cardinal.lift.{v, u} (Cardinal.mk ↑s)
-- Mathlib.Algebra.Group.Defs
LeftCancelSemigroup.mk : {G : Type u} → [toSemigroup : Semigroup G] → [toIsLeftCancelMul : IsLeftCancelMul G] → LeftCancelSemigroup G
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.get?_diff_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∉ t₂ → (t₁ \ t₂).get? k = t₁.get? k
-- Lean.Meta.Structure
/-- Eta reduces all structures satisfying `p` in the whole expression.

See `etaStruct?` for reducing single expressions.
 -/
Lean.Meta.etaStructReduce : Lean.Expr → (Lean.Name → Bool) → Lean.MetaM Lean.Expr
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
BoundarylessManifold.isInteriorPoint' : ∀ {𝕜 : Type u_5} {inst : NontriviallyNormedField 𝕜} {E : Type u_6} {inst_1 : NormedAddCommGroup E}
  {inst_2 : NormedSpace 𝕜 E} {H : Type u_7} {inst_3 : TopologicalSpace H} {I : ModelWithCorners 𝕜 E H} {M : Type u_8}
  {inst_4 : TopologicalSpace M} {inst_5 : ChartedSpace H M} [self : BoundarylessManifold I M] (x : M),
  I.IsInteriorPoint x
-- Mathlib.Data.EReal.Basic
EReal.toReal_nonpos : ∀ {x : EReal}, x ≤ 0 → x.toReal ≤ 0
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
/-- The dilation of set `x • s` is defined as `{x • y | y ∈ s}` in scope `Pointwise`.  -/
Set.smulSet : {α : Type u_2} → {β : Type u_3} → [SMul α β] → SMul α (Set β)
-- Mathlib.LinearAlgebra.Projection
/-- Restriction of the codomain of a projection of onto a subspace `p` to `p` instead of the whole
space.
 -/
LinearMap.IsProj.codRestrict : {S : Type u_5} →
  [inst : Semiring S] →
    {M : Type u_6} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module S M] → {m : Submodule S M} → {f : M →ₗ[S] M} → LinearMap.IsProj m f → M →ₗ[S] ↥m
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- Algebras of an endofunctor `F` form a category  -/
CategoryTheory.Endofunctor.Algebra.instCategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor C C) → CategoryTheory.Category.{v, max u v} (CategoryTheory.Endofunctor.Algebra F)
-- Mathlib.Algebra.Order.Ring.Canonical
CanonicallyOrderedAdd.mul_lt_mul_of_lt_of_lt : ∀ {R : Type u} [inst : CommSemiring R] [inst_1 : PartialOrder R] [CanonicallyOrderedAdd R] [PosMulStrictMono R]
  {a b c d : R}, a < b → c < d → a * c < b * d
-- Mathlib.CategoryTheory.MorphismProperty.Ind
CategoryTheory.MorphismProperty.ind_underObj_pushout : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {X Y : C} (g : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPushouts C] [P.IsStableUnderCobaseChange] {f : CategoryTheory.Under X},
  P.underObj.ind f → P.underObj.ind ((CategoryTheory.Under.pushout g).obj f)
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.FlatMap.0.Std.Iter.step_flatMapAfterM.match_1.splitter : {α β : Type u_1} →
  [inst : Std.Iterator α Id β] →
    {it₁ : Std.Iter β} →
      (motive : it₁.Step → Sort u_2) →
        (x : it₁.Step) →
          ((it₁' : Std.Iter β) →
              (b : β) → (h : it₁.IsPlausibleStep (Std.IterStep.yield it₁' b)) → motive ⟨Std.IterStep.yield it₁' b, h⟩) →
            ((it₁' : Std.Iter β) →
                (h : it₁.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', h⟩) →
              ((h : it₁.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩) → motive x
-- Mathlib.Topology.Homeomorph.Defs
HomeomorphClass.instHomeomorph : ∀ {α : Type u_6} {β : Type u_7} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β], HomeomorphClass (α ≃ₜ β) α β
-- Mathlib.LinearAlgebra.Dimension.Finite
/-- If a finset has cardinality larger than the rank of a module,
then there is a nontrivial linear relation amongst its elements.  -/
Module.exists_nontrivial_relation_of_finrank_lt_card : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Finite R M]
  [StrongRankCondition R] {t : Finset M}, Module.finrank R M < t.card → ∃ f, ∑ e ∈ t, f e • e = 0 ∧ ∃ x ∈ t, f x ≠ 0
-- Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass
MeasureTheory.restrict_Ioo_eq_restrict_Icc : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NullSingletonClass μ]
  [inst : PartialOrder α] {a b : α}, μ.restrict (Set.Ioo a b) = μ.restrict (Set.Icc a b)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.mem_union_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  k ∈ t₁ ∪ t₂ ↔ k ∈ t₁ ∨ k ∈ t₂
-- Init.Omega.IntList
Lean.Omega.IntList.gcd_cons_div_right : ∀ {x : ℤ} {xs : List ℤ}, Lean.Omega.IntList.gcd (x :: xs) ∣ Lean.Omega.IntList.gcd xs
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.nhds_top' : nhds ⊤ = ⨅ r, Filter.principal (Set.Ioi ↑r)
-- Mathlib.Algebra.Ring.CompTypeclasses
instRingHomIdId : ∀ {R : Type u_4} [inst : Semiring R], RingHomId (RingHom.id R)
-- Mathlib.Data.Fintype.BigOperators
Fintype.card_piFinset : ∀ {ι : Type u_4} {α : ι → Type u_6} [inst : DecidableEq ι] [inst_1 : Fintype ι] (s : (i : ι) → Finset (α i)),
  (Fintype.piFinset s).card = ∏ i, (s i).card
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey!_eq_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    l.isEmpty = false →
      ∀ {km : α},
        Std.Internal.List.maxKey! l = km ↔
          Std.Internal.List.getKey? km l = some km ∧
            ∀ (k : α), Std.Internal.List.containsKey k l = true → (compare k km).isLE = true
-- Mathlib.Tactic.Determinant.Bird.Meta
Mathlib.Tactic.Determinant.ReifiedBirdDet.mk.injEq : ∀ {u : Lean.Level} {α : Q(Type u)} (rα : Q(CommRing «$α»)) (ctx : Mathlib.Tactic.Determinant.Ctx rα) (u_1 : Lean.Level)
  (α_1 : Q(Type u_1)) (rα_1 : Q(CommRing «$α_1»)) (ctx_1 : Mathlib.Tactic.Determinant.Ctx rα_1),
  ({ u := u, α := α, rα := rα, ctx := ctx } = { u := u_1, α := α_1, rα := rα_1, ctx := ctx_1 }) =
    (u = u_1 ∧ α = α_1 ∧ rα = rα_1 ∧ ctx ≍ ctx_1)
-- Mathlib.Algebra.DirectSum.LinearMap
/-- The trace of an endomorphism of a direct sum is the sum of the traces on each component.

Note that it is important the statement gives the user definitional control over `p` since the
_type_ of the term `trace R p (f.restrict hp')` depends on `p`.  -/
LinearMap.trace_eq_sum_trace_restrict_of_eq_biSup : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : ι → Submodule R M} [∀ (i : ι), Module.Finite R ↥(N i)] [∀ (i : ι), Module.Free R ↥(N i)] (s : Finset ι),
  (iSupIndep fun i => N ↑i) →
    ∀ {f : Module.End R M} (hf : ∀ (i : ι), Set.MapsTo ⇑f ↑(N i) ↑(N i)) (p : Submodule R M) (hp : p = ⨆ i ∈ s, N i)
      (hp' : optParam (Set.MapsTo ⇑f ↑p ↑p) ⋯),
      (LinearMap.trace R ↥p) (LinearMap.restrict f hp') = ∑ i ∈ s, (LinearMap.trace R ↥(N i)) (LinearMap.restrict f ⋯)
-- Mathlib.Tactic.CasesM
/-- Core tactic for `constructorm`. Calls `constructor` on all subgoals for which
`matcher ldecl.type` returns true.
* `recursive`: if true, it calls itself repeatedly on the resulting subgoals
* `throwOnNoMatch`: if true, throws an error if no match is found
 -/
Mathlib.Tactic.constructorMatching : Lean.MVarId → (Lean.Expr → Lean.MetaM Bool) → optParam Bool false → optParam Bool true → Lean.MetaM (List Lean.MVarId)
-- Mathlib.LinearAlgebra.Finsupp.Supported
Finsupp.supported_empty : ∀ {α : Type u_1} {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Finsupp.supported M R ∅ = ⊥
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.contains_insert_self : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → ∀ {k : α} {v : β k}, (m.insert k v).contains k = true
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.any.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → (α → Bool) → Sort u_2) (x : α → Bool) (h_1 : (x : α → Bool) → motive [] x)
  (h_2 : (h : α) → (t : List α) → (p : α → Bool) → motive (h :: t) p),
  (match [], x with
    | [], x => h_1 x
    | h :: t, p => h_2 h t p) =
    h_1 x
-- Mathlib.Topology.EMetricSpace.Defs
Metric.closedEBall_subset_closedEBall : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {ε₁ ε₂ : ENNReal},
  ε₁ ≤ ε₂ → Metric.closedEBall x ε₁ ⊆ Metric.closedEBall x ε₂
-- Mathlib.Analysis.Normed.Operator.Bilinear
/-- Create a bilinear map (represented as a map `E →L[𝕜] F →L[𝕜] G`) from the corresponding linear
map and existence of a bound on the norm of the image. The linear map can be constructed using
`LinearMap.mk₂`.

If you have an explicit bound, use `LinearMap.mkContinuous₂` instead, as a norm estimate will
follow automatically in `LinearMap.mkContinuous₂_norm_le`.  -/
LinearMap.mkContinuousOfExistsBound₂ : {𝕜 : Type u_1} →
  {𝕜₂ : Type u_2} →
    {𝕜₃ : Type u_3} →
      {E : Type u_4} →
        {F : Type u_6} →
          {G : Type u_8} →
            [inst : SeminormedAddCommGroup E] →
              [inst_1 : SeminormedAddCommGroup F] →
                [inst_2 : SeminormedAddCommGroup G] →
                  [inst_3 : NontriviallyNormedField 𝕜] →
                    [inst_4 : NontriviallyNormedField 𝕜₂] →
                      [inst_5 : NontriviallyNormedField 𝕜₃] →
                        [inst_6 : NormedSpace 𝕜 E] →
                          [inst_7 : NormedSpace 𝕜₂ F] →
                            [inst_8 : NormedSpace 𝕜₃ G] →
                              {σ₂₃ : 𝕜₂ →+* 𝕜₃} →
                                {σ₁₃ : 𝕜 →+* 𝕜₃} →
                                  [RingHomIsometric σ₂₃] →
                                    (f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G) →
                                      (∃ C, ∀ (x : E) (y : F), ‖(f x) y‖ ≤ C * ‖x‖ * ‖y‖) → E →SL[σ₁₃] F →SL[σ₂₃] G
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
AlgebraicGeometry.instLocallyQuasiFiniteResLE : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : X.Opens) (V : Y.Opens)
  (e : U ≤ (TopologicalSpace.Opens.map f.base).obj V) [AlgebraicGeometry.LocallyQuasiFinite f],
  AlgebraicGeometry.LocallyQuasiFinite (AlgebraicGeometry.Scheme.Hom.resLE f V U e)
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.CostructuredArrow.overEquivPresheafCostructuredArrow_inverse_map_toOverCompCoyoneda : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
  {T : CategoryTheory.Over A} {X : CategoryTheory.CostructuredArrow CategoryTheory.yoneda A}
  (f : (CategoryTheory.CostructuredArrow.toOver CategoryTheory.yoneda A).obj X ⟶ T),
  (CategoryTheory.overEquivPresheafCostructuredArrow A).inverse.map
      ((CategoryTheory.ConcreteCategory.hom
          (((CategoryTheory.CostructuredArrow.toOverCompCoyoneda A).hom.app (Opposite.op X)).app T))
        f) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.CostructuredArrow.toOverCompOverEquivPresheafCostructuredArrow A).isoCompInverse.inv.app X)
      (CategoryTheory.CategoryStruct.comp f ((CategoryTheory.overEquivPresheafCostructuredArrow A).unit.app T))
-- Mathlib.Algebra.Star.StarRingHom
/-- The identity as a non-unital ⋆-ring homomorphism.  -/
NonUnitalStarRingHom.id : (A : Type u_1) → [inst : NonUnitalNonAssocSemiring A] → [inst_1 : Star A] → A →⋆ₙ+* A
-- Mathlib.CategoryTheory.Category.RelCat
CategoryTheory.instInhabitedRelCat : Inhabited CategoryTheory.RelCat
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.coe_equivIco : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] {p : 𝕜} [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  [hp : Fact (0 < p)] {a : 𝕜} [inst_3 : Archimedean 𝕜] {y : AddCircle p}, ↑↑((AddCircle.equivIco p a) y) = y
-- Mathlib.MeasureTheory.VectorMeasure.WithDensity
MeasureTheory.withDensityᵥ_sub' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {f g : α → E},
  MeasureTheory.Integrable f μ →
    MeasureTheory.Integrable g μ → (μ.withDensityᵥ fun x => f x - g x) = μ.withDensityᵥ f - μ.withDensityᵥ g
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
ContMDiffWithinAt.inv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {G : Type u_4} [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Group G] {E' : Type u_5}
  [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_9 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [inst_10 : TopologicalSpace M] [inst_11 : ChartedSpace H' M]
  [LieGroup I n G] {f : M → G} {s : Set M} {x₀ : M},
  ContMDiffWithinAt I' I n f s x₀ → ContMDiffWithinAt I' I n (fun x => (f x)⁻¹) s x₀
-- Mathlib.LinearAlgebra.Pi
Submodule.mem_pi : ∀ {R : Type u} {ι : Type x} [inst : Semiring R] {φ : ι → Type u_1} [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)] {I : Set ι} {p : (i : ι) → Submodule R (φ i)} {x : (i : ι) → φ i},
  x ∈ Submodule.pi I p ↔ ∀ i ∈ I, x i ∈ p i
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.map_iInf_comap_of_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] {ι : Type u_5} {f : F},
  Function.Surjective ⇑f → ∀ (S : ι → AddSubmonoid N), AddSubmonoid.map f (⨅ i, AddSubmonoid.comap f (S i)) = iInf S
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.pentagon_inv_hom_hom_hom_inv : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d e : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h i).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h).hom i)
        (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h) i).hom) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h i)).hom
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h i).inv)
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.gc_map_comap : ∀ {F : Type w} {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S]
  [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] (f : F),
  GaloisConnection (NonUnitalSubring.map f) (NonUnitalSubring.comap f)
-- Mathlib.Algebra.Category.Grp.Limits
AddCommGrpCat.forget_createsLimitsOfShape : (J : Type v) →
  [inst : CategoryTheory.Category.{w, v} J] →
    CategoryTheory.CreatesLimitsOfShape J (CategoryTheory.forget AddCommGrpCat)
-- Batteries.Data.String.Lemmas
String.foldr_eq : ∀ {α : Type u_1} (f : Char → α → α) (s : String) (a : α), String.Legacy.foldr f a s = List.foldr f a s.toList