mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Complex.Periodic
_private.Mathlib.Analysis.Complex.Periodic.0.«termI∞» : Lean.ParserDescr
-- Mathlib.Order.Types.Arithmetic
OrderType.instHMul : HMul OrderType.{u} OrderType.{v} OrderType.{max u v}
-- Std.Time.Duration
Std.Time.Duration.instHAddOffset_1 : HAdd Std.Time.Duration Std.Time.Week.Offset Std.Time.Duration
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.instMul.eq_1 : ∀ {ι : Type u_1} {M : ι → Type u_5} [inst : (i : ι) → Mul (M i)], Pi.instMul = { mul := fun f g i => f i * g i }
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
QuadraticMap.posDef_prod_iff : ∀ {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid P] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R P] [inst_7 : PartialOrder P] [AddLeftMono P] {Q₁ : QuadraticMap R M₁ P} {Q₂ : QuadraticMap R M₂ P},
  (Q₁.prod Q₂).PosDef ↔ Q₁.PosDef ∧ Q₂.PosDef
-- Mathlib.LinearAlgebra.Span.TensorProduct
Submodule.coe_tensorSpanEquivSpan_apply_tmul : ∀ {R : Type u_1} (A : Type u_2) {M : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M] [inst_6 : IsScalarTower R A M]
  [inst_7 : Algebra.IsEpi R A] [inst_8 : Module.Flat R A] {s : Set M} (a : A) (x : ↥(Submodule.span R s)),
  ↑((Submodule.tensorSpanEquivSpan R A s) (a ⊗ₜ[R] x)) = a • ↑x
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.toAlgHom_ofBijective : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (f : A₁ →ₐ[R] A₂) (hf : Function.Bijective ⇑f),
  ↑(AlgEquiv.ofBijective f hf) = f
-- Std.Time.Zoned.ZoneRules
/-- Finds the `LocalTimeType` corresponding to a given `Timestamp` in `ZoneRules`.
If the timestamp falls between two transitions, it returns the most recent transition before the timestamp.
When the timestamp is beyond all stored transitions and a POSIX TZ footer rule is present, the rule is
consulted. Falls back to `initialLocalTimeType` if no transition or rule applies.
 -/
Std.Time.TimeZone.ZoneRules.findLocalTimeTypeForTimestamp : Std.Time.TimeZone.ZoneRules → Std.Time.Timestamp → Std.Time.TimeZone.LocalTimeType
-- Mathlib.Algebra.Group.Hom.Defs
ZeroHom.coe_coe : ∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : Zero M] [inst_1 : Zero N] [inst_2 : FunLike F M N]
  [inst_3 : ZeroHomClass F M N] (f : F), ⇑↑f = ⇑f
-- Mathlib.AlgebraicGeometry.Scheme
TopCat.Presheaf.stalk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  (ℱ ℱ_1 : TopCat.Presheaf C X), ℱ = ℱ_1 → ∀ (x x_1 : ↑X), x = x_1 → ℱ.stalk x = ℱ_1.stalk x_1
-- Mathlib.Topology.Homotopy.Basic
/-- If each `f₀ i : C(X, Y i)` is homotopic to `f₁ i : C(X, Y i)`, then `ContinuousMap.pi f₀` is
homotopic to `ContinuousMap.pi f₁`.  -/
ContinuousMap.Homotopic.pi : ∀ {X : Type u} {ι : Type u_2} [inst : TopologicalSpace X] {Y : ι → Type u_3} [inst_1 : (i : ι) → TopologicalSpace (Y i)]
  {f₀ f₁ : (i : ι) → C(X, Y i)},
  (∀ (i : ι), (f₀ i).Homotopic (f₁ i)) → (ContinuousMap.pi f₀).Homotopic (ContinuousMap.pi f₁)
-- Mathlib.Data.Nat.Bits
Nat.div2_bit : ∀ (b : Bool) (n : ℕ), (Nat.bit b n).div2 = n
-- Std.Sat.AIG.Basic
/-- A circuit node. These are not recursive but instead contain indices into an `AIG`, with inputs indexed by `α`.
 -/
Std.Sat.AIG.Decl : Type → Type
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.over : (n : Type u) → (S : AlgebraicGeometry.Scheme) → (AlgebraicGeometry.AffineSpace n S).CanonicallyOver S
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.commutes : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (r : R),
  e ((algebraMap R A₁) r) = (algebraMap R A₂) r
-- Mathlib.Topology.Constructions
IsClosedMap.subtype_map : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsClosedMap f → ∀ {s : Set X} {t : Set Y}, IsClosed s → ∀ (hst : ∀ x ∈ s, f x ∈ t), IsClosedMap (Subtype.map f hst)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.core.sizeOf_spec : ∀ (e : Lean.Expr), sizeOf (Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.core e) = 1 + sizeOf e
-- Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
/-- Characterize the inverse direction of the isomorphism
`PreservesLimit₂.isoLimitUncurryWhiskeringLeft₂` w.r.t. the canonical maps to the limit.  -/
CategoryTheory.Limits.PreservesLimit₂.isoLimitUncurryWhiskeringLeft₂_inv_comp_π : ∀ {J₁ : Type u_1} {J₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} J₂] {C₁ : Type u_3} {C₂ : Type u_4} {C : Type u_5}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₁] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₂]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C] (K₁ : CategoryTheory.Functor J₁ C₁)
  (K₂ : CategoryTheory.Functor J₂ C₂) (G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C))
  [inst_5 : CategoryTheory.Limits.PreservesLimit₂ K₁ K₂ G] [inst_6 : CategoryTheory.Limits.HasLimit K₁]
  [inst_7 : CategoryTheory.Limits.HasLimit K₂] (j : J₁ × J₂),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesLimit₂.isoLimitUncurryWhiskeringLeft₂ K₁ K₂ G).inv
      (CategoryTheory.Limits.limit.π
        (CategoryTheory.Functor.uncurry.obj ((((CategoryTheory.Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G)) j) =
    CategoryTheory.CategoryStruct.comp
      ((G.map (CategoryTheory.Limits.limit.π K₁ j.1)).app (CategoryTheory.Limits.limit K₂))
      ((G.obj (K₁.obj j.1)).map (CategoryTheory.Limits.limit.π K₂ j.2))
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKeyD_unitOfList_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List α}
  {k fallback : α}, l.contains k = false → (Std.ExtDTreeMap.Const.unitOfList l cmp).getKeyD k fallback = fallback
-- Std.Data.HashMap.RawLemmas
/-- Simpler variant of `getD_filterMap` when `LawfulBEq` is available.  -/
Std.HashMap.Raw.getD_filterMap' : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [LawfulBEq α]
  {f : α → β → Option γ} {k : α} {fallback : γ},
  m.WF → (Std.HashMap.Raw.filterMap f m).getD k fallback = (m[k]?.bind (f k)).getD fallback
-- Mathlib.Topology.UniformSpace.Cauchy
Filter.TotallyBounded.mono : ∀ {α : Type u} [uniformSpace : UniformSpace α] {f g : Filter α}, f ≤ g → g.TotallyBounded → f.TotallyBounded
-- Mathlib.Analysis.Analytic.Inverse
FormalMultilinearSeries.rightInv.eq_3 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) (n : ℕ),
  p.rightInv i x n.succ.succ =
    -(↑i.symm).compContinuousMultilinearMap (p.comp (fun k => if k < n + 2 then p.rightInv i x k else 0) (n + 2))
-- Init.Data.List.OfFn
List.map_ofFn : ∀ {n : ℕ} {α : Type u_1} {β : Type u_2} {f : Fin n → α} {g : α → β}, List.map g (List.ofFn f) = List.ofFn (g ∘ f)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.find?_some : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x y : α} [Std.TransCmp cmp] {t : RBTree.RBSet α cmp},
  t.find? x = some y ↔ y ∈ t.toList ∧ cmp x y = Ordering.eq
-- Mathlib.RingTheory.WittVector.Basic
_private.Mathlib.RingTheory.WittVector.Basic.0.Int.castDef.match_1.eq_1 : ∀ (motive : ℤ → Sort u_1) (n : ℕ) (h_1 : (n : ℕ) → motive (Int.ofNat n)) (h_2 : (n : ℕ) → motive (Int.negSucc n)),
  (match Int.ofNat n with
    | Int.ofNat n => h_1 n
    | Int.negSucc n => h_2 n) =
    h_1 n
-- Mathlib.RingTheory.Polynomial.Opposites
Polynomial.isDomain_iff : ∀ {R : Type u_1} [inst : Semiring R], IsDomain (Polynomial R) ↔ IsDomain R ∧ IsCancelAdd R
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.size_ofList_le : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List ((a : α) × β a)}, (Std.ExtDHashMap.ofList l).size ≤ l.length
-- Std.Tactic.BVDecide.Reflect
_private.Std.Tactic.BVDecide.Reflect.0.Std.Tactic.BVDecide.Reflect.verifyCert.match_1.eq_2 : ∀ (motive : Except String (Array Std.Tactic.BVDecide.LRAT.IntAction) → Sort u_1) (a : String)
  (h_1 : (lratProof : Array Std.Tactic.BVDecide.LRAT.IntAction) → motive (Except.ok lratProof))
  (h_2 : (a : String) → motive (Except.error a)),
  (match Except.error a with
    | Except.ok lratProof => h_1 lratProof
    | Except.error a => h_2 a) =
    h_2 a
-- Lean.Meta.Instances
Lean.Meta.InstanceTree : Type
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instContinuousDiv : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Div G] [inst_2 : ContinuousDiv G],
  ContinuousDiv (SeparationQuotient G)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.mono_fun_enorm : ∀ {ε : Type u_3} {ε' : Type u_4} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε]
  [inst_2 : TopologicalSpace ε'] [inst_3 : ENormedAddMonoid ε'] {f : ℝ → ε} {a b : ℝ} {μ : MeasureTheory.Measure ℝ}
  [TopologicalSpace.PseudoMetrizableSpace ε] [TopologicalSpace.PseudoMetrizableSpace ε'] {g : ℝ → ε'},
  IntervalIntegrable f μ a b →
    MeasureTheory.AEStronglyMeasurable g (μ.restrict (Set.uIoc a b)) →
      ((fun x => ‖g x‖ₑ) ≤ᵐ[μ.restrict (Set.uIoc a b)] fun x => ‖f x‖ₑ) → IntervalIntegrable g μ a b
-- Mathlib.Topology.Order.LeftRightLim
mapClusterPt_leftLim : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace α]
  [OrderTopology α] (f : α → β) (a : α), MapClusterPt (Function.leftLim f a) (nhdsWithin a (Set.Iic a)) f
-- Mathlib.RingTheory.Ideal.IsPrincipal
/-- A version of `Ideal.associatesEquivIsPrincipal` for non-zero-divisors generators.  -/
Ideal.associatesNonZeroDivisorsEquivIsPrincipal : (R : Type u_1) →
  [inst : CommRing R] → [IsDomain R] → Associates ↥(nonZeroDivisors R) ≃ { I // Submodule.IsPrincipal ↑I }
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.ae_smul_measure_le : ∀ {α : Type u_1} {R : Type u_6} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : SMul R ENNReal]
  [inst_1 : IsScalarTower R ENNReal ENNReal] (c : R), MeasureTheory.ae (c • μ) ≤ MeasureTheory.ae μ
-- Mathlib.LinearAlgebra.Alternating.Basic
/-- Combine a family of alternating maps with the same domain and codomains `N i` into an
alternating map taking values in the space of functions `Π i, N i`.  -/
AlternatingMap.pi : {R : Type u_1} →
  [inst : Semiring R] →
    {M : Type u_2} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {ι : Type u_7} →
            {ι' : Type u_10} →
              {N : ι' → Type u_11} →
                [inst_3 : (i : ι') → AddCommMonoid (N i)] →
                  [inst_4 : (i : ι') → Module R (N i)] → ((i : ι') → M [⋀^ι]→ₗ[R] N i) → M [⋀^ι]→ₗ[R] ((i : ι') → N i)
-- Lean.Elab.Command.Scope
/-- True if (applicable) declarations should automatically be marked as `meta`. No surface syntax
currently.
 -/
Lean.Elab.Command.Scope.isMeta : Lean.Elab.Command.Scope → Bool
-- Mathlib.Algebra.Order.UpperLower
LowerSet.coe_div : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : Preorder α] [inst_2 : IsOrderedMonoid α] (s t : LowerSet α),
  ↑(s / t) = ↑s / ↑t
-- Init.Data.SInt.Bitwise
Int64.zero_or : ∀ {a : Int64}, 0 ||| a = a
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- For a functor `F : C ⥤ D` and an object `d : D`, we obtain a contravariant functor from the
category of structured arrows `op d ⟶ F.op.obj c` to the category of costructured arrows
`F.obj c ⟶ d`.
 -/
CategoryTheory.StructuredArrow.toCostructuredArrow' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          (d : D) →
            CategoryTheory.Functor (CategoryTheory.StructuredArrow (Opposite.op d) F.op)ᵒᵖ
              (CategoryTheory.CostructuredArrow F d)
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
/-- Suppose we have a monoidal equivalence `F : C ≌ D`, with `D` monoidal closed. We can pull the
monoidal closed instance back along the equivalence. For `X, Y, Z : C`, this lemma describes the
resulting currying map `Hom(X ⊗ Y, Z) → Hom(Y, (X ⟶[C] Z))`. (`X ⟶[C] Z` is defined to be
`F⁻¹(F(X) ⟶[D] F(Z))`, so currying in `C` is given by essentially conjugating currying in
`D` by `F.`)  -/
CategoryTheory.MonoidalClosed.ofEquiv_curry_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [inst_4 : F.Monoidal]
  [inst_5 : F.IsEquivalence] [inst_6 : CategoryTheory.MonoidalClosed D] {X Y Z : C}
  (f : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Z),
  CategoryTheory.MonoidalClosed.curry f =
    (adj.homEquiv Y (F.obj X ⟹ F.obj Z))
      (CategoryTheory.MonoidalClosed.curry
        ((adj.toEquivalence.symm.toAdjunction.homEquiv
            (CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)) Z)
          (CategoryTheory.CategoryStruct.comp
            ((CategoryTheory.Functor.Monoidal.commTensorLeft F X).compInverseIso.hom.app Y) f)))
-- Init.Data.SInt.Bitwise
Int64.or_zero : ∀ {a : Int64}, a ||| 0 = a
-- Mathlib.Order.BoundedOrder.Basic
Pi.top_comp : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : Top γ] (x : α → β), ⊤ ∘ x = ⊤
-- Init.Data.SInt.Basic
/-- Constructs an `Int64` from an `Int` that is known to be in bounds.  -/
Int64.ofIntLE : (i : ℤ) → Int64.minValue.toInt ≤ i → i ≤ Int64.maxValue.toInt → Int64
-- Mathlib.MeasureTheory.OuterMeasure.Induced
MeasureTheory.inducedOuterMeasure.congr_simp : ∀ {α : Type u_1} {P : Set α → Prop} (m m_1 : (s : Set α) → P s → ENNReal) (e_m : m = m_1) (P0 : P ∅) (m0 : m ∅ P0 = 0),
  MeasureTheory.inducedOuterMeasure m P0 m0 = MeasureTheory.inducedOuterMeasure m_1 P0 ⋯
-- Mathlib.Algebra.Ring.Subring.MulOpposite
Subring.unop_closure : ∀ {R : Type u_2} [inst : NonAssocRing R] (s : Set Rᵐᵒᵖ),
  (Subring.closure s).unop = Subring.closure (MulOpposite.op ⁻¹' s)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Carry
Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit.go : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {w : ℕ} → (aig : Std.Sat.AIG α) → aig.RefVec w → aig.RefVec w → ℕ → aig.Ref → Std.Sat.AIG.Entrypoint α
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Split.Hom.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {S₁ S₂ : CategoryTheory.SimplicialObject.Split C}
  [inst_1 : SizeOf C] (F : S₁.X ⟶ S₂.X) (f : (n : ℕ) → S₁.s.N n ⟶ S₂.s.N n)
  (comm :
    autoParam
      (∀ (n : ℕ),
        CategoryTheory.CategoryStruct.comp (S₁.s.ι n) (F.app (Opposite.op { len := n })) =
          CategoryTheory.CategoryStruct.comp (f n) (S₂.s.ι n))
      CategoryTheory.SimplicialObject.Split.Hom.comm._autoParam),
  sizeOf { F := F, f := f, comm := comm } = 1 + sizeOf F
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
AEMeasurable.measurable_mk : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β}
  {μ : MeasureTheory.Measure α} (h : AEMeasurable f μ), Measurable (AEMeasurable.mk f h)
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.restoreM_ReaderT : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {α ρ : Type u}
  {epost : EPred} (x : m α) (post : α → ρ → Pred),
  ⦃ fun r => Std.Internal.Do.wp x (fun a => post a r) epost ⦄ MonadControl.restoreM x ⦃ post; epost ⦄
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.fundamentalCone.instMulActionSubtypeUnitsRingOfIntegersMemSubgroupTorsionElemMixedSpaceIntegerSet : {K : Type u_1} →
  [inst : Field K] →
    [inst_1 : NumberField K] →
      MulAction ↥(NumberField.Units.torsion K) ↑(NumberField.mixedEmbedding.fundamentalCone.integerSet K)
-- Mathlib.Order.Filter.Map
Filter.compl_mem_comap : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l : Filter β} {s : Set α}, sᶜ ∈ Filter.comap f l ↔ (f '' s)ᶜ ∈ l
-- Mathlib.Order.Bounds.OrderIso
OrderIso.isGLB_preimage : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β) {s : Set β} {x : α},
  IsGLB (⇑f ⁻¹' s) x ↔ IsGLB s (f x)
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestRevMatchAtChain.brecOn : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {a : s.Pos}
  {motive : (a_1 : s.Pos) → String.Slice.Pattern.Model.IsLongestRevMatchAtChain pat a a_1 → Prop} {a_1 : s.Pos}
  (t : String.Slice.Pattern.Model.IsLongestRevMatchAtChain pat a a_1),
  (∀ (a_2 : s.Pos) (t : String.Slice.Pattern.Model.IsLongestRevMatchAtChain pat a a_2),
      String.Slice.Pattern.Model.IsLongestRevMatchAtChain.below t → motive a_2 t) →
    motive a_1 t
-- Init.Data.String.PosRaw
String.Pos.Raw.byteIdx_add_char : ∀ {p : String.Pos.Raw} {c : Char}, (p + c).byteIdx = p.byteIdx + c.utf8Size
-- Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
TopCat.Presheaf.SheafCondition.instNonemptyStructuredArrowPairwiseOpensLeCoverPairwiseToOpensLeCover : ∀ {X : TopCat} {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X) (V : TopCat.Presheaf.SheafCondition.OpensLeCover U),
  Nonempty (CategoryTheory.StructuredArrow V (TopCat.Presheaf.SheafCondition.pairwiseToOpensLeCover U))
-- Mathlib.Order.SuccPred.Archimedean
/-- **Alias** of `Order.succ_max`. -/
succ_max : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] (a b : α),
  Order.succ (max a b) = max (Order.succ a) (Order.succ b)
-- Mathlib.MeasureTheory.OuterMeasure.Caratheodory
MeasureTheory.OuterMeasure.isCaratheodory_iff_le : ∀ {α : Type u} (m : MeasureTheory.OuterMeasure α) {s : Set α},
  MeasurableSet s ↔ ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Module.FaithfullyFlat.nontrivial_tensorProduct_iff_left : ∀ (R : Type u) (M : Type v) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_1}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [Module.FaithfullyFlat R N],
  Nontrivial (TensorProduct R M N) ↔ Nontrivial M
-- Mathlib.Algebra.Homology.SpectralObject.Homology
CategoryTheory.Abelian.SpectralObject.dShortComplex_g : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {i₀ i₁ i₂ i₃ i₄ i₅ i₆ i₇ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅)
  (f₆ : i₅ ⟶ i₆) (f₇ : i₆ ⟶ i₇) (n₀ n₁ n₂ n₃ n₄ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.dShortComplex._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.dShortComplex._auto_3)
  (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.dShortComplex._auto_5)
  (hn₄ : autoParam (n₃ + 1 = n₄) CategoryTheory.Abelian.SpectralObject.dShortComplex._auto_7),
  (X.dShortComplex f₁ f₂ f₃ f₄ f₅ f₆ f₇ n₀ n₁ n₂ n₃ n₄ hn₁ hn₂ hn₃ hn₄).g = X.d f₁ f₂ f₃ f₄ f₅ n₁ n₂ n₃ n₄ ⋯ ⋯ ⋯
-- Mathlib.Algebra.Category.BialgCat.Basic
BialgCat.mk.injEq : ∀ {R : Type u} [inst : CommRing R] (carrier : Type v) [instRing : Ring carrier] [instBialgebra : Bialgebra R carrier]
  (carrier_1 : Type v) (instRing_1 : Ring carrier_1) (instBialgebra_1 : Bialgebra R carrier_1),
  ({ carrier := carrier, instRing := instRing, instBialgebra := instBialgebra } =
      { carrier := carrier_1, instRing := instRing_1, instBialgebra := instBialgebra_1 }) =
    (carrier = carrier_1 ∧ instRing ≍ instRing_1 ∧ instBialgebra ≍ instBialgebra_1)
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.domCongr_refl : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : AddMonoid M], AddMonoidAlgebra.domCongr R A (AddEquiv.refl M) = AlgEquiv.refl
-- Init.Data.UInt.Lemmas
USize.ofNatLT_uInt16ToNat : ∀ (n : UInt16), USize.ofNatLT n.toNat ⋯ = n.toUSize
-- Mathlib.Order.Cover
Pi.covBy_iff : ∀ {ι : Type u_3} {α : ι → Type u_4} [inst : (i : ι) → PartialOrder (α i)] {a b : (i : ι) → α i},
  a ⋖ b ↔ ∃ i, a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → a j = b j
-- Mathlib.Probability.Distributions.Gamma
ProbabilityTheory.gammaPDF_of_neg : ∀ {a r x : ℝ}, x < 0 → ProbabilityTheory.gammaPDF a r x = 0
-- Mathlib.ModelTheory.Algebra.Ring.Basic
FirstOrder.Ring.instMulTermRing : (α : Type u_2) → Mul (FirstOrder.Language.ring.Term α)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.size_alter_le_size : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  {f : Option (β k) → Option (β k)}, (m.alter k f).size ≤ m.size + 1
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMap.instInhabited : {G : Type u_1} → [inst : Add G] → {a : G} → Inhabited (AddConstMap G G a a)
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.δlastFunctor_map_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} {X Y : CategoryTheory.ComposableArrows C (n + 1)}
  (f : X ⟶ Y) (X_1 : Fin (n + 1)), (CategoryTheory.ComposableArrows.δlastFunctor.map f).app X_1 = f.app X_1.castSucc
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolInformation.tags : Lean.Lsp.SymbolInformation → Array Lean.Lsp.SymbolTag
-- Batteries.Data.String.Legacy
/-- Auxuliary definition for `String.Legacy.foldr`.

This is an old implementation, preserved here for users of the lemmas in
`Batteries.Data.String.Lemmas`.
 -/
String.Legacy.foldrAux : {α : Type u} → (Char → α → α) → α → String → String.Pos.Raw → String.Pos.Raw → α
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Ideal.mul_iInf : ∀ {A : Type u_2} [inst : CommRing A] [IsDedekindDomain A] (I : Ideal A) {ι : Type u_4} [Nonempty ι] (J : ι → Ideal A),
  I * ⨅ i, J i = ⨅ i, I * J i
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.coe_comap : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] {N : Type u_2} [inst_2 : Group N]
  [inst_3 : TopologicalSpace N] (H : OpenSubgroup N) (f : G →* N) (hf : Continuous ⇑f),
  ↑(OpenSubgroup.comap f hf H) = ⇑f ⁻¹' ↑H
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.addLeftMono : AddLeftMono Cardinal.{u_1}
-- Mathlib.Topology.MetricSpace.Contracting
/-- If a globally contracting map `f` has two complete forward-invariant sets `s`, `t`,
and `x ∈ s` is at a finite distance from `y ∈ t`, then the `efixedPoint'` constructed by `x`
is the same as the `efixedPoint'` constructed by `y`.

This lemma takes additional arguments stating that `f` contracts on `s` and `t` because this way
it can be used to prove the desired equality with non-trivial proofs of these facts.  -/
ContractingWith.efixedPoint_eq_of_edist_lt_top' : ∀ {α : Type u_1} [inst : EMetricSpace α] {K : NNReal} {f : α → α},
  ContractingWith K f →
    ∀ {s : Set α} (hsc : IsComplete s) (hsf : Set.MapsTo f s s)
      (hfs : ContractingWith K (Set.MapsTo.restrict f s s hsf)) {x : α} (hxs : x ∈ s) (hx : edist x (f x) ≠ ⊤)
      {t : Set α} (htc : IsComplete t) (htf : Set.MapsTo f t t)
      (hft : ContractingWith K (Set.MapsTo.restrict f t t htf)) {y : α} (hyt : y ∈ t) (hy : edist y (f y) ≠ ⊤),
      edist x y ≠ ⊤ →
        ContractingWith.efixedPoint' f hsc hsf hfs x hxs hx = ContractingWith.efixedPoint' f htc htf hft y hyt hy
-- Mathlib.Topology.MetricSpace.Holder
HolderOnWith.mono_const : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {r : NNReal} {f : X → Y}
  {C₁ C₂ : NNReal} {A : Set X}, HolderOnWith C₁ r f A → C₁ ≤ C₂ → HolderOnWith C₂ r f A