mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Instances.AddCircle.Defs
/-- **Alias** of `continuousWithinAt_toIocMod_Iic`.

---

`toIocMod` is continuous on the right at every point.  -/
continuous_left_toIocMod : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  [inst_3 : Archimedean 𝕜] [inst_4 : TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a x : 𝕜),
  ContinuousWithinAt (toIocMod hp a) (Set.Iic x) x
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.stmts₁_trans : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} {q₁ q₂ : Turing.TM2.Stmt Γ Λ σ},
  q₁ ∈ Turing.TM2.stmts₁ q₂ → Turing.TM2.stmts₁ q₁ ⊆ Turing.TM2.stmts₁ q₂
-- Mathlib.RingTheory.Bialgebra.Hom
/-- The counit of a bialgebra as a `BialgHom`.  -/
Bialgebra.counitBialgHom : (R : Type u_1) →
  (A : Type u_2) → [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Bialgebra R A] → A →ₐc[R] R
-- Init.Data.List.Erase
List.Nodup.erase : ∀ {α : Type u_1} [inst : BEq α] {l : List α} [LawfulBEq α] (a : α), l.Nodup → (l.erase a).Nodup
-- Mathlib.Data.Finmap
Finmap.toFinmap_cons : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) (b : β a) (xs : List (Sigma β)),
  (⟨a, b⟩ :: xs).toFinmap = Finmap.insert a b xs.toFinmap
-- Mathlib.Data.Fin.Rev
Fin.rev_surjective : ∀ {n : ℕ}, Function.Surjective Fin.rev
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.rank_le_height : ∀ {R : Type uR} [inst : CommSemiring R] [StrongRankCondition R] {m n : ℕ} (A : Matrix (Fin m) (Fin n) R), A.rank ≤ m
-- Std.Time.Date.Basic
Std.Time.instHSubOffsetOffset_19 : HSub Std.Time.Minute.Offset Std.Time.Millisecond.Offset Std.Time.Millisecond.Offset
-- Mathlib.Algebra.Polynomial.Homogenize
Polynomial.homogenize_dvd : ∀ {R : Type u_1} [inst : CommSemiring R] [NoZeroDivisors R] {p q : Polynomial R},
  p ∣ q → p.homogenize p.natDegree ∣ q.homogenize q.natDegree
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
spinGroup.units_involute_act_eq_conjAct : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {x : (CliffordAlgebra Q)ˣ},
  ↑x ∈ spinGroup Q →
    ∀ (y : M),
      CliffordAlgebra.involute ↑x * (CliffordAlgebra.ι Q) y * ↑x⁻¹ = ConjAct.toConjAct x • (CliffordAlgebra.ι Q) y
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.verify₄_eq_isSome_assemble₄ : ∀ {w x y z : UInt8}, ByteArray.utf8DecodeChar?.verify₄ w x y z = (ByteArray.utf8DecodeChar?.assemble₄ w x y z).isSome
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.inhabited : {R : Type u_2} →
  {A : Type u_3} →
    [inst : CommSemiring R] →
      [inst_1 : StarRing R] →
        [inst_2 : Semiring A] →
          [inst_3 : Algebra R A] → [inst_4 : StarRing A] → [inst_5 : StarModule R A] → Inhabited (StarSubalgebra R A)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.size_alter_le_size : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k : α} {f : Option (β k) → Option (β k)}, m.WF → (m.alter k f).size ≤ m.size + 1
-- Mathlib.Order.Interval.Basic
Interval.setLike : {α : Type u_1} → [inst : PartialOrder α] → SetLike (Interval α) α
-- Mathlib.Algebra.Order.Group.Indicator
Set.le_indicator : ∀ {α : Type u_2} {M : Type u_3} [inst : LE M] [inst_1 : Zero M] {s : Set α} {f g : α → M},
  (∀ a ∈ s, f a ≤ g a) → (∀ a ∉ s, f a ≤ 0) → f ≤ s.indicator g
-- Mathlib.Data.SetLike.Basic
SetLike.mem_mk_set : ∀ {X : Type u_3} {p : Set X → Prop} {U : Set X} {h : p U} {x : X}, x ∈ ⟨U, h⟩ ↔ x ∈ U
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
le_tsub_iff_left : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α], a ≤ c → (b ≤ c - a ↔ a + b ≤ c)
-- Mathlib.Combinatorics.Matroid.Rank.Finite
Matroid.Indep.subset_finite_isBasis'_of_subset_of_isRkFinite : ∀ {α : Type u_1} {M : Matroid α} {X I : Set α},
  M.Indep I → I ⊆ X → M.IsRkFinite X → ∃ J, M.IsBasis' J X ∧ I ⊆ J ∧ J.Finite
-- Lean.Elab.InfoTree.Types
Lean.Elab.instInhabitedPartialTermInfo.default : Lean.Elab.PartialTermInfo
-- Mathlib.Topology.Connected.TotallyDisconnected
/-- A set `s` is called totally separated if any two points of this set can be separated
by two disjoint open sets covering `s`.  -/
IsTotallySeparated : {α : Type u} → [TopologicalSpace α] → Set α → Prop
-- Mathlib.Analysis.SpecialFunctions.Log.Deriv
Real.differentiableAt_log_iff : ∀ {x : ℝ}, DifferentiableAt ℝ Real.log x ↔ x ≠ 0
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.map_snd_darts : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), List.map (fun x => x.toProd.2) p.darts = p.support.tail
-- Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
/-- **Alias** of `MeasureTheory.Measure.AbsolutelyContinuous.refl`. -/
MeasureTheory.Measure.absolutelyContinuous_refl : ∀ {α : Type u_1} {_m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α), μ.AbsolutelyContinuous μ
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.mkIncorrectNumberOfPatternsMsg : {α : Type} → [Lean.ToMessageData α] → String → ℕ → ℕ → List α → Lean.MessageData
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- The orthogonal projection is self-adjoint.  -/
Submodule.inner_starProjection_left_eq_right : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection] (u v : E),
  inner 𝕜 (K.starProjection u) v = inner 𝕜 u (K.starProjection v)
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.continuousAt_logb : ∀ {b x : ℝ}, x ≠ 0 → ContinuousAt (Real.logb b) x
-- Mathlib.CategoryTheory.Equivalence
/-- Sanity check: `isoFunctorOfIsoInverse (isoInverseOfIsoFunctor i)` is just `i`.  -/
CategoryTheory.Iso.isoFunctorOfIsoInverse_isoInverseOfIsoFunctor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {G G' : C ≌ D} (i : G.functor ≅ G'.functor), i.isoInverseOfIsoFunctor.isoFunctorOfIsoInverse = i
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.gaussianReal_add_gaussianReal_of_indepFun : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {m₁ m₂ : ℝ} {v₁ v₂ : NNReal} {X Y : Ω → ℝ},
  ProbabilityTheory.IndepFun X Y P →
    MeasureTheory.Measure.map X P = ProbabilityTheory.gaussianReal m₁ v₁ →
      MeasureTheory.Measure.map Y P = ProbabilityTheory.gaussianReal m₂ v₂ →
        MeasureTheory.Measure.map (X + Y) P = ProbabilityTheory.gaussianReal (m₁ + m₂) (v₁ + v₂)
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.mapDomainAlgHom_apply : ∀ (R : Type u_1) (A : Type u_4) {M : Type u_7} {N : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddMonoid M] [inst_4 : AddMonoid N] (f : M →+ N) (x : AddMonoidAlgebra A M),
  (AddMonoidAlgebra.mapDomainAlgHom R A f) x = AddMonoidAlgebra.mapDomain (⇑f) x
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.TriangleMorphism.comp_hom₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {T₁ T₂ T₃ : CategoryTheory.Pretriangulated.Triangle C} (f : CategoryTheory.Pretriangulated.TriangleMorphism T₁ T₂)
  (g : CategoryTheory.Pretriangulated.TriangleMorphism T₂ T₃),
  (f.comp g).hom₂ = CategoryTheory.CategoryStruct.comp f.hom₂ g.hom₂
-- Mathlib.Data.Set.Disjoint
Set.empty_disjoint : ∀ {α : Type u} (s : Set α), Disjoint ∅ s
-- Mathlib.Order.Interval.Finset.Defs
Finset.Icc_product_Icc : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] [inst_4 : DecidableLE (α × β)] (a₁ a₂ : α) (b₁ b₂ : β),
  Finset.Icc a₁ a₂ ×ˢ Finset.Icc b₁ b₂ = Finset.Icc (a₁, b₁) (a₂, b₂)
-- Mathlib.Data.Set.Countable
Set.Countable.insert : ∀ {α : Type u} {s : Set α} (a : α), s.Countable → (insert a s).Countable
-- Mathlib.Topology.Sequences
/-- The sum (disjoint union) of two sequential spaces is a sequential space.  -/
Sum.instSequentialSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [SequentialSpace X]
  [SequentialSpace Y], SequentialSpace (X ⊕ Y)
-- Init.Data.UInt.Lemmas
USize.le_rfl : ∀ {a : USize}, a ≤ a
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.uliftYonedaEquiv_uliftYoneda_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.uliftYonedaEquiv (CategoryTheory.uliftYoneda.{w, v₁, u₁}.map f) = { down := f }
-- Init.Data.BitVec.Lemmas
BitVec.cons_append_append : ∀ {w₁ w₂ w₃ : ℕ} (x : BitVec w₁) (y : BitVec w₂) (z : BitVec w₃) (a : Bool),
  BitVec.cons a x ++ y ++ z = BitVec.cast ⋯ (BitVec.cons a (x ++ y ++ z))
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.map_codiag_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct X X] [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct Y Y]
  {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map f f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.codiag Y) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.codiag X) (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback.LiftStruct.w : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S}
  {h : CategoryTheory.Limits.ChosenPullback f₁ f₂} {Y : C} {g₁ : Y ⟶ X₁} {g₂ : Y ⟶ X₂} {b : Y ⟶ S}
  (l : h.LiftStruct g₁ g₂ b), CategoryTheory.CategoryStruct.comp g₁ f₁ = CategoryTheory.CategoryStruct.comp g₂ f₂
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.WithLowerSet.ofLowerSet_symm : ∀ {α : Type u_1}, Topology.WithLowerSet.ofLowerSet.symm = Topology.WithLowerSet.toLowerSet
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
/-- We can always derive `HasFiniteColimits C` by providing colimits at an
arbitrary universe.  -/
CategoryTheory.Limits.hasFiniteColimits_of_hasFiniteColimits_of_size : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  (∀ (J : Type w) {𝒥 : CategoryTheory.SmallCategory J} (x : CategoryTheory.FinCategory J),
      CategoryTheory.Limits.HasColimitsOfShape J C) →
    CategoryTheory.Limits.HasFiniteColimits C
-- Batteries.Data.String.Lemmas
String.utf8GetAux_addChar_right_cancel : ∀ (s : List Char) (i p : String.Pos.Raw) (c : Char),
  String.Pos.Raw.utf8GetAux s (i + c) (p + c) = String.Pos.Raw.utf8GetAux s i p
-- Lean.Environment
_private.Lean.Environment.0.Lean.ImportedModule.mk.inj : ∀ {toEffectiveImport : Lean.EffectiveImport} {parts irParts : Array (Lean.ModuleData × Lean.CompactedRegion)}
  {needsIRTrans : Bool} {toEffectiveImport_1 : Lean.EffectiveImport}
  {parts_1 irParts_1 : Array (Lean.ModuleData × Lean.CompactedRegion)} {needsIRTrans_1 : Bool},
  { toEffectiveImport := toEffectiveImport, parts := parts, irParts := irParts, needsIRTrans := needsIRTrans } =
      { toEffectiveImport := toEffectiveImport_1, parts := parts_1, irParts := irParts_1,
        needsIRTrans := needsIRTrans_1 } →
    toEffectiveImport = toEffectiveImport_1 ∧ parts = parts_1 ∧ irParts = irParts_1 ∧ needsIRTrans = needsIRTrans_1
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.instNeg : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.Preadditive C] → {P Q : CategoryTheory.Idempotents.Karoubi C} → Neg (P ⟶ Q)
-- Mathlib.Data.EReal.Basic
EReal.toENNReal_zero : EReal.toENNReal 0 = 0
-- Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp
/-- This returns the multiset of irreducible factors as a `Finsupp`.  -/
factorization : {α : Type u_1} →
  [inst : CommMonoidWithZero α] → [UniqueFactorizationMonoid α] → [NormalizationMonoid α] → [DecidableEq α] → α → α →₀ ℕ
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.ofReal_integral_eq_lintegral_ofReal : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  MeasureTheory.Integrable f μ → 0 ≤ᵐ[μ] f → ENNReal.ofReal (∫ (x : α), f x ∂μ) = ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ
-- Mathlib.CategoryTheory.Functor.CurryingThree
CategoryTheory.Functor.curry₃_map_app_app_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_4} C₃]
  [inst_3 : CategoryTheory.Category.{v_9, u_9} E] {F G : CategoryTheory.Functor (C₁ × C₂ × C₃) E} (f : F ⟶ G) (X₁ : C₁)
  (X₂ : C₂) (X₃ : C₃), (((CategoryTheory.Functor.curry₃.map f).app X₁).app X₂).app X₃ = f.app (X₁, X₂, X₃)
-- Std.Http.Protocol.H1
/-- Parses trailers after a zero-size chunk and finalizes chunked body processing.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.parseLastChunkBodyState : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Machine dir →
    Array (Std.Http.Chunk.ExtensionName × Option Std.Http.Chunk.ExtensionValue) →
      Std.Http.Protocol.H1.Machine dir × Option Std.Http.Protocol.H1.PulledChunk × Bool
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommGroupWithTop.toSubtractionMonoid : {α : Type u_2} → [LinearOrderedAddCommGroupWithTop α] → SubtractionMonoid α
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.lowerBound?_eq_find? : ∀ {α : Type u_1} {x : α} {t : RBTree.RBNode α} {cut : α → Ordering} (lb : Option α),
  RBTree.RBNode.find? cut t = some x → RBTree.RBNode.lowerBound? cut t lb = some x
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.mk.inj : ∀ {R : Type u_3} {inst : CommSemiring R} {A : Type u_4} {inst_1 : Semiring A} {inst_2 : TopologicalSpace A}
  {B : Type u_5} {inst_3 : Semiring B} {inst_4 : TopologicalSpace B} {inst_5 : Algebra R A} {inst_6 : Algebra R B}
  {toAlgHom : A →ₐ[R] B} {cont : autoParam (Continuous (↑↑toAlgHom.toRingHom).toFun) ContinuousAlgHom.cont._autoParam}
  {toAlgHom_1 : A →ₐ[R] B}
  {cont_1 : autoParam (Continuous (↑↑toAlgHom_1.toRingHom).toFun) ContinuousAlgHom.cont._autoParam},
  { toAlgHom := toAlgHom, cont := cont } = { toAlgHom := toAlgHom_1, cont := cont_1 } → toAlgHom = toAlgHom_1
-- Std.Http.Protocol.H1
/-- Returns `true` when body chunks should be drained internally rather than surfaced to the caller.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.drainBodyInternally : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → Bool
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.zero_apply : ∀ {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] (i : ι), 0 i = 0
-- Mathlib.Order.Category.FinBddDistLat
FinBddDistLat.coe_comp : ∀ {X Y Z : FinBddDistLat} {f : X ⟶ Y} {g : Y ⟶ Z},
  ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) =
    ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Lean.Log
/-- Log a new warning message using the given message data. The position is provided by `getRef`.  -/
Lean.logWarning : {m : Type → Type} →
  [Monad m] → [Lean.MonadLog m] → [Lean.AddMessageContext m] → [Lean.MonadOptions m] → Lean.MessageData → m Unit
-- Init.Data.Order.Factories
/-- This instance is only publicly defined in `Init.Data.Order.Lemmas`.
 -/
_private.Init.Data.Order.Factories.0.Std.instReflOfTotal : ∀ {α : Sort u_1} {r : α → α → Prop} [Std.Total r], Std.Refl r
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.zero_vlt_one : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R], 0 <ᵥ 1
-- Lean.Parser.Term.Basic
Lean.Parser.Tactic.tacticSeq.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Lean.Parser.Command
Lean.Parser.Command.check.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
_private.Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense.0.CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.fac : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A]
  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] {data : (X : C) → F.OneHypercoverDenseData J₀ J X}
  {G : CategoryTheory.Functor Cᵒᵖ A} (hG₀ : CategoryTheory.Presheaf.IsSheaf J₀ (F.op.comp G))
  (hG : (X : C) → CategoryTheory.Limits.IsLimit ((data X).toOneHypercover.multifork G)) {X : C} {S : J.Cover X}
  (s : CategoryTheory.Limits.Multifork (S.index G)) (a : S.Arrow),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.lift✝ hG₀ hG s)
      (G.map a.f.op) =
    s.ι a
-- Mathlib.Topology.NhdsSet
Filter.Eventually.eventually_nhdsSet : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s : Set X} {p : X → Prop},
  (∀ᶠ (y : X) in nhdsSet s, p y) → ∀ᶠ (y : X) in nhdsSet s, ∀ᶠ (x : X) in nhds y, p x
-- Std.Sync.SharedMutex
/-- Locks a `BaseSharedMutex` for shared read access. This function blocks until there are no more
writers which hold the lock. There may be other readers currently inside the lock when this method
returns.

The current thread must not have already locked the mutex.
Reentrant locking is undefined behavior (inherited from the C++ implementation).
 -/
Std.BaseSharedMutex.read : Std.BaseSharedMutex → BaseIO Unit
-- Aesop.Percent
Aesop.Percent.toHumanString : Aesop.Percent → String
-- Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
TendstoUniformlyOn.comp_cexp : ∀ {α : Type u_1} {ι : Type u_2} {K : Set α} {f : ι → α → ℂ} {p : Filter ι} {g : α → ℂ},
  TendstoUniformlyOn f g p K →
    BddAbove ((fun x => (g x).re) '' K) → TendstoUniformlyOn (fun x => Complex.exp ∘ f x) (Complex.exp ∘ g) p K
-- Mathlib.Data.List.Sort
OrderEmbedding.sortedLE_listMap : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ↪o β) {l : List α},
  (List.map (⇑e) l).SortedLE ↔ l.SortedLE
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.lowerBound?.eq_2 : ∀ {α : Type u_1} (cut : α → Ordering) (x : Option α) (c : RBTree.RBColor) (a : RBTree.RBNode α) (y : α)
  (b : RBTree.RBNode α),
  RBTree.RBNode.lowerBound? cut (RBTree.RBNode.node c a y b) x =
    match cut y with
    | Ordering.lt => RBTree.RBNode.lowerBound? cut a x
    | Ordering.gt => RBTree.RBNode.lowerBound? cut b (some y)
    | Ordering.eq => some y
-- Mathlib.LinearAlgebra.TensorProduct.Basis
Module.Basis.tensorProduct_repr_tmul_apply : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [inst : CommSemiring R]
  [inst_1 : Semiring S] [inst_2 : Algebra R S] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module S M]
  [inst_6 : IsScalarTower R S M] [inst_7 : AddCommMonoid N] [inst_8 : Module R N] (b : Module.Basis ι S M)
  (c : Module.Basis κ R N) (m : M) (n : N) (i : ι) (j : κ),
  ((b.tensorProduct c).repr (m ⊗ₜ[R] n)) (i, j) = (c.repr n) j • (b.repr m) i
-- Mathlib.GroupTheory.SemidirectProduct
/-- Two maps out of the semidirect product are equal if they're equal after composition
with both `inl` and `inr`  -/
SemidirectProduct.hom_ext : ∀ {N : Type u_1} {G : Type u_2} {H : Type u_3} [inst : Group N] [inst_1 : Group G] [inst_2 : Group H]
  {φ : G →* MulAut N} {f g : N ⋊[φ] G →* H},
  f.comp SemidirectProduct.inl = g.comp SemidirectProduct.inl →
    f.comp SemidirectProduct.inr = g.comp SemidirectProduct.inr → f = g
-- Mathlib.Tactic.FunProp.Core
/-- Prove function property of using *morphism theorems*.  -/
Mathlib.Meta.FunProp.applyMorRules : Mathlib.Meta.FunProp.FunPropDecl →
  Lean.Expr →
    Mathlib.Meta.FunProp.FunctionData →
      (Lean.Expr → Mathlib.Meta.FunProp.FunPropM (Option Mathlib.Meta.FunProp.Result)) →
        Mathlib.Meta.FunProp.FunPropM (Option Mathlib.Meta.FunProp.Result)
-- Mathlib.Data.List.Cycle
List.prev.eq_def : ∀ {α : Type u_1} [inst : DecidableEq α] (x : List α) (x_1 : α) (x_2 : x_1 ∈ x),
  x.prev x_1 x_2 =
    match x, x_1, x_2 with
    | [], x, h => ⋯.elim
    | [y], x, x_3 => y
    | y :: z :: xs, x, h => if hx : x = y then (z :: xs).getLast ⋯ else if x = z then y else (z :: xs).prev x ⋯
-- Mathlib.Combinatorics.SimpleGraph.DeleteEdges
SimpleGraph.deleteIncidenceSet_le : ∀ {V : Type u_1} (G : SimpleGraph V) (x : V), G.deleteIncidenceSet x ≤ G
-- Mathlib.ModelTheory.Basic
/-- A structure induced by a bijection.  -/
Equiv.inducedStructure : {L : FirstOrder.Language} → {M : Type u_1} → {N : Type u_2} → [L.Structure M] → M ≃ N → L.Structure N
-- Init.Sym.Lemmas
Lean.Sym.Int64.eq_eq_false : ∀ (a b : Int64), decide (a = b) = false → (a = b) = False
-- Mathlib.Analysis.InnerProductSpace.Defs
InnerProductSpace.toNormedSpace : {𝕜 : Type u_4} →
  {E : Type u_5} →
    {inst : RCLike 𝕜} → {inst_1 : SeminormedAddCommGroup E} → [self : InnerProductSpace 𝕜 E] → NormedSpace 𝕜 E
-- Init.Prelude
Lean.Syntax.brecOn_1.eq : ∀ {motive_1 : Lean.Syntax → Sort u} {motive_2 : Array Lean.Syntax → Sort u} {motive_3 : List Lean.Syntax → Sort u}
  (t : Array Lean.Syntax) (F_1 : (t : Lean.Syntax) → t.below → motive_1 t)
  (F_2 : (t : Array Lean.Syntax) → Lean.Syntax.below_1 t → motive_2 t)
  (F_3 : (t : List Lean.Syntax) → Lean.Syntax.below_2 t → motive_3 t),
  Lean.Syntax.brecOn_1 t F_1 F_2 F_3 = F_2 t (Lean.Syntax.brecOn_1.go t F_1 F_2 F_3).2
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.codeSuggestions : Lean.Elab.TermElabM (Array (Lean.StrLit → Lean.Doc.DocM (Array Lean.Doc.CodeSuggestion)))
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKeyD_inter_of_mem_right : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] {k fallback : α}, k ∈ m₂ → (m₁ ∩ m₂).getKeyD k fallback = m₁.getKeyD k fallback
-- Mathlib.RingTheory.Grassmannian
Module.Grassmannian.mk.injEq : ∀ {R : Type u} [inst : CommRing R] {M : Type v} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {k : ℕ}
  (toSubmodule : Submodule R M) (finite_quotient : Module.Finite R (M ⧸ toSubmodule))
  (projective_quotient : Module.Projective R (M ⧸ toSubmodule))
  (rankAtStalk_eq : ∀ (p : PrimeSpectrum R), Module.rankAtStalk (M ⧸ toSubmodule) p = k) (toSubmodule_1 : Submodule R M)
  (finite_quotient_1 : Module.Finite R (M ⧸ toSubmodule_1))
  (projective_quotient_1 : Module.Projective R (M ⧸ toSubmodule_1))
  (rankAtStalk_eq_1 : ∀ (p : PrimeSpectrum R), Module.rankAtStalk (M ⧸ toSubmodule_1) p = k),
  ({ toSubmodule := toSubmodule, finite_quotient := finite_quotient, projective_quotient := projective_quotient,
        rankAtStalk_eq := rankAtStalk_eq } =
      { toSubmodule := toSubmodule_1, finite_quotient := finite_quotient_1,
        projective_quotient := projective_quotient_1, rankAtStalk_eq := rankAtStalk_eq_1 }) =
    (toSubmodule = toSubmodule_1)
-- Mathlib.Order.Filter.Extr
/-- **Alias** of the forward direction of `isMinFilter_dual_iff`. -/
IsMinFilter.undual : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
  IsMinFilter (⇑OrderDual.toDual ∘ f) l a → IsMaxFilter f l a
-- Mathlib.Data.Finsupp.MonomialOrder.DegLex
/-- `Finsupp.DegLex r s` is the homogeneous lexicographic order on `α →₀ M`,
where `α` is ordered by `r` and `M` is ordered by `s`.
The type synonym `DegLex (α →₀ M)` has an order given by `Finsupp.DegLex (· < ·) (· < ·)`.  -/
Finsupp.DegLex : {α : Type u_1} → (α → α → Prop) → (ℕ → ℕ → Prop) → (α →₀ ℕ) → (α →₀ ℕ) → Prop
-- Mathlib.Analysis.Normed.Module.Bases
/-- The enorm of any projection is bounded by the basis constant.  -/
SchauderBasis.enorm_proj_le_enormProjBound : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {X : Type u_2} [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] (b : SchauderBasis 𝕜 X) (n : ℕ), ‖b.proj n‖ₑ ≤ b.enormProjBound
-- Mathlib.Analysis.SpecialFunctions.SmoothTransition
Real.smoothTransition.monotone : Monotone Real.smoothTransition