mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Filter.ENNReal
ENNReal.limsup_liminf_le_liminf_limsup : ∀ {α : Type u_1} {β : Type u_2} [Countable β] {f : Filter α} [CountableInterFilter f] {g : Filter β}
  (u : α → β → ENNReal),
  Filter.limsup (fun a => Filter.liminf (fun b => u a b) g) f ≤
    Filter.liminf (fun b => Filter.limsup (fun a => u a b) f) g
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
MonCat.FilteredColimits.colimit.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCat)
  [inst_1 : CategoryTheory.IsFiltered J], MonCat.FilteredColimits.colimit F = MonCat.of (MonCat.FilteredColimits.M F)
-- Mathlib.Analysis.InnerProductSpace.Basic
real_inner_self_nonneg : ∀ {F : Type u_3} [inst : SeminormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {x : F}, 0 ≤ inner ℝ x x
-- Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup
CommGrpCat.toAddCommGrp_map : ∀ {x x_1 : CommGrpCat} (f : x ⟶ x_1),
  CommGrpCat.toAddCommGrp.map f = AddCommGrpCat.ofHom (MonoidHom.toAdditive (CommGrpCat.Hom.hom f))
-- Mathlib.Data.UInt
UInt32.toBitVec_zsmul : ∀ (z : ℤ) (a : UInt32), (z • a).toBitVec = z • a.toBitVec
-- Mathlib.AlgebraicGeometry.AffineScheme
/-- In an affine open set `U`, a family of basic open covers `U` iff the sections span `Γ(X, U)`.
See `iSup_basicOpen_of_span_eq_top` for the inverse direction without the affine-ness assumption.
 -/
AlgebraicGeometry.IsAffineOpen.iSup_basicOpen_eq_self_iff : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens},
  AlgebraicGeometry.IsAffineOpen U →
    ∀ {s : Set ↑(X.presheaf.obj (Opposite.op U))}, ⨆ f, X.basicOpen ↑f = U ↔ Ideal.span s = ⊤
-- Lean.Parser.Term
Lean.Parser.Term.macroLastArg.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
/-- `𝓞 K ⧸ Ideal.span {ζ - 1}` is finite.  -/
IsPrimitiveRoot.finite_quotient_toInteger_sub_one : ∀ {K : Type u} [inst : Field K] {ζ : K} [NumberField K] {k : ℕ} (hk : 1 < k) (hζ : IsPrimitiveRoot ζ k),
  Finite (NumberField.RingOfIntegers K ⧸ Ideal.span {hζ.toInteger - 1})
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.IsCircuit.not_ssubset : ∀ {α : Type u_1} {M : Matroid α} {C C' : Set α}, M.IsCircuit C → M.IsCircuit C' → ¬C' ⊂ C
-- Mathlib.CategoryTheory.Join.Pseudofunctor
CategoryTheory.Join.mapCompLeft.eq_1 : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} (D : Type u_4) [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor B C),
  CategoryTheory.Join.mapCompLeft D F G =
    CategoryTheory.Join.mapIsoWhiskerLeft (F.comp G) (CategoryTheory.Functor.id D).leftUnitor.symm ≪≫
      CategoryTheory.Join.mapPairComp F (CategoryTheory.Functor.id D) G (CategoryTheory.Functor.id D)
-- Std.Data.ExtTreeSet.Basic
Std.ExtTreeSet.instInterOfTransCmp : {α : Type u} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Inter (Std.ExtTreeSet α cmp)
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g}
  {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf)
  (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt}
  (fac :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) =
      CategoryTheory.CategoryStruct.comp π ι)
  [inst_2 : CategoryTheory.Epi π] [inst_3 : CategoryTheory.Mono ι],
  (CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation S hkf hcc fac).left =
    CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.leftHomologyData S hkf hcc fac
-- Mathlib.Data.Multiset.AddSub
Multiset.le_add_right : ∀ {α : Type u_1} (s t : Multiset α), s ≤ s + t
-- Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Algebra.adjoin.powerBasis'_gen : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsDomain R] [inst_3 : Algebra R S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsDomain S] [inst_6 : Module.IsTorsionFree R S] {x : S}
  (hx : IsIntegral R x), (Algebra.adjoin.powerBasis' hx).gen = ⟨x, ⋯⟩
-- Std.Time.Time.PlainTime
Std.Time.PlainTime.mk.sizeOf_spec : ∀ (hour : Std.Time.Hour.Ordinal) (minute : Std.Time.Minute.Ordinal) (second : Std.Time.Second.Ordinal true)
  (nanosecond : Std.Time.Nanosecond.Ordinal),
  sizeOf { hour := hour, minute := minute, second := second, nanosecond := nanosecond } =
    1 + sizeOf hour + sizeOf minute + sizeOf second + sizeOf nanosecond
-- Mathlib.Data.Real.Basic
Real.instNNRatCast : NNRatCast ℝ
-- Mathlib.Algebra.Group.Hom.Defs
/-- The proposition that the function preserves multiplication  -/
MonoidHom.map_mul' : ∀ {M : Type u_10} {N : Type u_11} [inst : MulOne M] [inst_1 : MulOne N] (self : M →* N) (x y : M),
  (↑self).toFun (x * y) = (↑self).toFun x * (↑self).toFun y
-- Mathlib.Data.Set.Prod
Set.instMembership.hcongr_1 : ∀ (α α' : Type u), α = α' → Set.instMembership ≍ Set.instMembership
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.instSubsingleton : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [Subsingleton R], Subsingleton (QuaternionAlgebra R c₁ c₂ c₃)
-- Mathlib.Order.Concept
Concept.ofObjects_le_iff : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {s : Set α} {c : Concept α β r},
  Concept.ofObjects r s ≤ c ↔ s ⊆ c.extent
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.mk.inj : ∀ {M : Type u_1} {inst : AddCommMonoid M} {S : AddSubmonoid M} {N : Type u_2} {inst_1 : AddCommMonoid N}
  {toAddHom : M →ₙ+ N} {isLocalizationMap : S.IsLocalizationMap toAddHom.toFun} {toAddHom_1 : M →ₙ+ N}
  {isLocalizationMap_1 : S.IsLocalizationMap toAddHom_1.toFun},
  { toAddHom := toAddHom, isLocalizationMap := isLocalizationMap } =
      { toAddHom := toAddHom_1, isLocalizationMap := isLocalizationMap_1 } →
    toAddHom = toAddHom_1
-- Lean.Parser.Module.Syntax
Lean.Parser.Module.header : Lean.Parser.Parser
-- Mathlib.Algebra.GroupWithZero.Regular
/-- The element `0` is left-regular if and only if `R` is trivial.  -/
IsLeftRegular.subsingleton : ∀ {R : Type u_1} [inst : MulZeroClass R], IsLeftRegular 0 → Subsingleton R
-- Mathlib.Util.AtomM.Recurse
/-- A cleanup routine, which simplifies evaluation results to a more human-friendly format.  -/
Mathlib.Tactic.AtomM.Recurse.Context.simp : Mathlib.Tactic.AtomM.Recurse.Context → Lean.Meta.Simp.Result → Lean.MetaM Lean.Meta.Simp.Result
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
LinearIndependent.linearCombination_comp_repr : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (hv : LinearIndependent R v),
  Finsupp.linearCombination R v ∘ₗ hv.repr = (Submodule.span R (Set.range v)).subtype
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.mk_eq_zero : ∀ {R : Type u_1} [inst : CommRing R] {f g : Polynomial R}, (AdjoinRoot.mk f) g = 0 ↔ f ∣ g
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.biUnion_smul_finset : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] (s : Finset α) (t : Finset β),
  (s.biUnion fun x => x • t) = s • t
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.delabFVar : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.codRestrict_apply_coe : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂]
  (f : ContinuousMultilinearMap R M₁ M₂) (p : Submodule R M₂) (h : ∀ (v : (i : ι) → M₁ i), f v ∈ p)
  (v : (i : ι) → M₁ i), ↑((f.codRestrict p h) v) = f v
-- Lean.Meta.Tactic.Simp.Rewrite
_private.Lean.Meta.Tactic.Simp.Rewrite.0.Lean.Meta.Simp.dischargeEqnThmHypothesis?.go? : Lean.MVarId → Lean.MetaM (Option Lean.MVarId)
-- Mathlib.Algebra.Group.Action.Units
Units.instSMul : {M : Type u_3} → {α : Type u_5} → [inst : Monoid M] → [SMul M α] → SMul Mˣ α
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
/-- The short complex `H¹(G ⧸ S, A^S) ⟶ H¹(G, A) ⟶ H¹(S, A)`.  -/
groupCohomology.H1InfRes : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] → Rep.{u, u, u} k G → (S : Subgroup G) → [S.Normal] → CategoryTheory.ShortComplex (ModuleCat k)
-- Init.Data.UInt.Bitwise
USize.toUInt64_or : ∀ (a b : USize), (a ||| b).toUInt64 = a.toUInt64 ||| b.toUInt64
-- Mathlib.CategoryTheory.Triangulated.Basic
/-- the second commutative square of a triangle morphism  -/
CategoryTheory.Pretriangulated.TriangleMorphism.comm₂_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C} (self : CategoryTheory.Pretriangulated.TriangleMorphism T₁ T₂)
  {Z : C} (h : T₂.obj₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp T₁.mor₂ (CategoryTheory.CategoryStruct.comp self.hom₃ h) =
    CategoryTheory.CategoryStruct.comp self.hom₂ (CategoryTheory.CategoryStruct.comp T₂.mor₂ h)
-- Init.Data.Array.Lemmas
Array.findM?_toList : ∀ {m : Type → Type u_1} {α : Type} [inst : Monad m] [LawfulMonad m] {p : α → m Bool} {xs : Array α},
  List.findM? p xs.toList = Array.findM? p xs
-- Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
SSet.opObjEquiv_mem_degenerate_iff : ∀ (X : SSet) {n : ℕ} (x : X.op.obj (Opposite.op { len := n })),
  SSet.opObjEquiv x ∈ X.degenerate n ↔ x ∈ X.op.degenerate n
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.Connected.exists_path_of_dist : ∀ {V : Type u_1} {G : SimpleGraph V}, G.Connected → ∀ (u v : V), ∃ p, p.IsPath ∧ p.length = G.dist u v
-- Mathlib.Topology.PartialHomeomorph.Defs
/-- Coercion of a `PartialHomeomorph` to function.
Note that a `PartialHomeomorph` is not `DFunLike`.  -/
PartialHomeomorph.instCoeFunForall : {X : Type u_1} →
  {Y : Type u_3} →
    [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → CoeFun (PartialHomeomorph X Y) fun x => X → Y
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.completeLattice : {R : Type u_1} →
  {M : Type u_3} →
    [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → CompleteLattice (Submodule R M)
-- Lean.Meta.CongrTheorems
/-- For congr-simp theorems only.  Indicates a decidable instance argument.
The lemma contains two arguments [a_i : Decidable ...] [b_i : Decidable ...]  -/
Lean.Meta.CongrArgKind.subsingletonInst : Lean.Meta.CongrArgKind
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
/-- For a based functor `F : 𝒳 ⟶ 𝒴`, and an arrow `φ` in `𝒳`, then `φ` lifts an arrow `f` in `𝒮`
if `F(φ)` does.  -/
CategoryTheory.BasedFunctor.isHomLift_map : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] {𝒳 : CategoryTheory.BasedCategory 𝒮}
  {𝒴 : CategoryTheory.BasedCategory 𝒮} (F : CategoryTheory.BasedFunctor 𝒳 𝒴) {R S : 𝒮} {a b : 𝒳.obj} (f : R ⟶ S)
  (φ : a ⟶ b) [𝒴.p.IsHomLift f (F.map φ)], 𝒳.p.IsHomLift f φ
-- Mathlib.Data.EReal.Operations
EReal.coe_sub_bot : ∀ (x : ℝ), ↑x - ⊥ = ⊤
-- Mathlib.Algebra.GCDMonoid.Basic
CommGroupWithZero.normalize_eq_one : ∀ (G₀ : Type u_2) [inst : CommGroupWithZero G₀] [inst_1 : DecidableEq G₀] {a : G₀}, a ≠ 0 → normalize a = 1
-- Mathlib.Data.ENNReal.BigOperators
ENNReal.ofNNReal_finsuppSum : ∀ {ι : Type u_1} {M : Type u_2} [inst : Zero M] (f : ι →₀ M) (g : ι → M → NNReal),
  ↑(f.sum g) = f.sum fun i m => ↑(g i m)
-- Init.Data.AC
_private.Init.Data.AC.0.Lean.Data.AC.mergeIdem.loop.match_1.eq_2 : ∀ (motive : ℕ → List ℕ → Sort u_1) (curr : ℕ) (h_1 : (curr next : ℕ) → (rest : List ℕ) → motive curr (next :: rest))
  (h_2 : (curr : ℕ) → motive curr []),
  (match curr, [] with
    | curr, next :: rest => h_1 curr next rest
    | curr, [] => h_2 curr) =
    h_2 curr
-- Mathlib.Topology.EMetricSpace.BoundedVariation
/-- The map `(eVariationOn · s)` is lower semicontinuous for uniform convergence on `s`.  -/
eVariationOn.lowerSemicontinuous_uniformOn : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] (s : Set α),
  LowerSemicontinuous fun f => eVariationOn f s
-- Mathlib.Topology.Filter
Filter.nhds_top : ∀ {α : Type u_2}, nhds ⊤ = ⊤
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
CategoryTheory.NatTrans.pi.eq_1 : ∀ {I : Type w₀} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : I → Type u₂}
  [inst_1 : (i : I) → CategoryTheory.Category.{v₂, u₂} (D i)] {F G : (i : I) → CategoryTheory.Functor (C i) (D i)}
  (α : (i : I) → F i ⟶ G i), CategoryTheory.NatTrans.pi α = { app := fun f i => (α i).app (f i), naturality := ⋯ }
-- Aesop.Search.SearchM
Aesop.SearchM.State.mk : {Q : Type} → [inst : Aesop.Queue Q] → Aesop.Iteration → Q → Bool → Aesop.SearchM.State Q
-- Mathlib.RingTheory.OrderOfVanishing.Noetherian
Ring.ordFrac_irreducible : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra R K] [inst_5 : IsFractionRing R K] {ϖ : R},
  Irreducible ϖ → (Ring.ordFrac R) ((algebraMap R K) ϖ) = WithZero.exp 1
-- Mathlib.Algebra.CubicDiscriminant
Cubic.degree_of_d_eq_zero' : ∀ {R : Type u_1} [inst : Semiring R], { a := 0, b := 0, c := 0, d := 0 }.toPoly.degree = ⊥
-- Mathlib.Algebra.Ring.Int.Parity
Int.even_mul_succ_self : ∀ (n : ℤ), Even (n * (n + 1))
-- Init.Data.UInt.Lemmas
UInt32.eq_of_toFin_eq : ∀ {a b : UInt32}, a.toFin = b.toFin → a = b
-- Mathlib.Order.Atoms
isAtom_top : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : BoundedOrder α] [IsSimpleOrder α], IsAtom ⊤
-- Mathlib.Analysis.Calculus.ContDiff.CPolynomial
/-- A polynomial function is infinitely differentiable.  -/
CPolynomialOn.contDiffOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {s : Set E}, CPolynomialOn 𝕜 f s → ∀ {n : WithTop ℕ∞}, ContDiffOn 𝕜 n f s
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.variance_id_map : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ},
  AEMeasurable X μ → ProbabilityTheory.variance id (MeasureTheory.Measure.map X μ) = ProbabilityTheory.variance X μ
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Normal
/-- A morphism `φ : H ⟶ G` of group objects is a normal monoid homomorphism if it is a
monoid homomorphism that is mono and such that the conjugation map `(g, h) ↦ g * h * g⁻¹`
factors through `φ`.  -/
CategoryTheory.IsMonHom.Normal : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {G H : C} → [CategoryTheory.GrpObj G] → [CategoryTheory.GrpObj H] → (H ⟶ G) → Prop
-- Mathlib.Data.EReal.Operations
EReal.ge_of_forall_gt_iff_ge : ∀ {x y : EReal}, (∀ (z : ℝ), ↑z < y → ↑z ≤ x) ↔ y ≤ x
-- Mathlib.Data.Multiset.Defs
Multiset.pairwise_coe_iff : ∀ {α : Type u_1} {r : α → α → Prop} {l : List α}, Multiset.Pairwise r ↑l ↔ ∃ l', l.Perm l' ∧ List.Pairwise r l'
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
CategoryTheory.Limits.BinaryFan.ext.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : C} {c c' : CategoryTheory.Limits.BinaryFan A B}
  (e : c.pt ≅ c'.pt) (h₁ : c.fst = CategoryTheory.CategoryStruct.comp e.hom c'.fst)
  (h₂ : c.snd = CategoryTheory.CategoryStruct.comp e.hom c'.snd),
  CategoryTheory.Limits.BinaryFan.ext e h₁ h₂ = CategoryTheory.Limits.Cone.ext e ⋯
-- Mathlib.Probability.Kernel.Composition.ParallelComp
ProbabilityTheory.Kernel.parallelComp_zero_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} (η : ProbabilityTheory.Kernel γ δ),
  ProbabilityTheory.Kernel.parallelComp 0 η = 0
-- Mathlib.GroupTheory.Coset.Basic
AddMonoidHom.fiberEquiv.eq_1 : ∀ {α : Type u_1} [inst : AddGroup α] {H : Type u_2} [inst_1 : AddGroup H] (f : α →+ H) (a b : α),
  f.fiberEquiv a b = (f.fiberEquivKer a).trans (f.fiberEquivKer b).symm
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SolverExtension.newEq : {σ : Type} → Lean.Meta.Grind.SolverExtension σ → Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.one_ne_bot : ∀ {α : Type u} [inst : One α], 1 ≠ ⊥
-- Mathlib.Order.Interval.Set.ProjIcc
Set.projIcc.eq_1 : ∀ {α : Type u_1} [inst : LinearOrder α] (a b : α) (h : a ≤ b) (x : α), Set.projIcc a b h x = ⟨max a (min b x), ⋯⟩
-- Lean.Meta.Basic
/-- `withTrackingZetaDeltaSet s x` executes `x` in a context where `zetaDeltaFVarIds` has been temporarily cleared.
- If `s` is nonempty, zeta-delta tracking is enabled and `zetaDeltaSet := s`.
  Furthermore, the cache is temporarily reset so that zeta-delta tracking is accurate.
- If `s` is empty, then zeta-delta tracking is disabled. The `zetaDeltaSet` is *not* modified, and the cache is not cleared.

Any zeta-delta reductions recorded while executing `x` will *not* persist when leaving `withTrackingZetaDeltaSet`.

See also `withZetaDeltaSet`, which does not interact with zeta-delta tracking.
 -/
Lean.Meta.withTrackingZetaDeltaSet : {n : Type → Type u_1} → [MonadControlT Lean.MetaM n] → [Monad n] → {α : Type} → Lean.FVarIdSet → n α → n α
-- Init.Data.SInt.Lemmas
ISize.le_of_lt : ∀ {a b : ISize}, a < b → a ≤ b
-- Mathlib.RingTheory.Localization.Integer
/-- A choice of a common multiple of the denominators of a finite set of fractions.  -/
IsLocalization.commonDenomOfFinset : {R : Type u_1} →
  [inst : CommSemiring R] →
    (M : Submonoid R) →
      {S : Type u_2} → [inst_1 : CommSemiring S] → [inst_2 : Algebra R S] → [IsLocalization M S] → Finset S → ↥M
-- Mathlib.CategoryTheory.Sites.SheafOfTypes
/-- For a topology generated by a basis, it suffices to check the sheaf condition on the basis
presieves only.
 -/
CategoryTheory.Presieve.isSheaf_pretopology : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)}
  [inst_1 : CategoryTheory.Limits.HasPullbacks C] (K : CategoryTheory.Pretopology C),
  CategoryTheory.Presieve.IsSheaf K.toGrothendieck P ↔
    ∀ {X : C}, ∀ R ∈ K.coverings X, CategoryTheory.Presieve.IsSheafFor P R
-- Mathlib.Algebra.Homology.Embedding.TruncGE
HomologicalComplex.truncGE'XIsoOpcycles.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'XIsoOpcycles e hi' hi = HomologicalComplex.truncGE'.XIsoOpcycles K e hi ≪≫ CategoryTheory.eqToIso ⋯
-- Mathlib.InformationTheory.KullbackLeibler.Basic
InformationTheory.klDiv_smul_same : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν] (c : NNReal),
  InformationTheory.klDiv (c • μ) (c • ν) = ↑c * InformationTheory.klDiv μ ν
-- Mathlib.AlgebraicGeometry.Spec
AlgebraicGeometry.Spec.sheafedSpaceMap_comp : ∀ {R S T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T),
  AlgebraicGeometry.Spec.sheafedSpaceMap (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.sheafedSpaceMap g)
      (AlgebraicGeometry.Spec.sheafedSpaceMap f)
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.mem_rec_on : ∀ {α : Type u} {C : Stream'.WSeq α → Prop} {a : α} {s : Stream'.WSeq α},
  a ∈ s →
    (∀ (b : α) (s' : Stream'.WSeq α), a = b ∨ C s' → C (Stream'.WSeq.cons b s')) →
      (∀ (s : Stream'.WSeq α), C s → C s.think) → C s
-- Aesop.RuleSet
Aesop.GlobalRuleSet.onBase : {α : Type u_1} → (Aesop.BaseRuleSet → Aesop.BaseRuleSet × α) → Aesop.GlobalRuleSet → Aesop.GlobalRuleSet × α
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Cases : Lean.Compiler.LCNF.Purity → Type
-- Mathlib.CategoryTheory.Filtered.Small
CategoryTheory.IsFiltered.SmallFilteredIntermediate.instIsFilteredOrEmpty : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFilteredOrEmpty C] {D : Type u₁}
  [inst_2 : CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor D C),
  CategoryTheory.IsFilteredOrEmpty (CategoryTheory.IsFiltered.SmallFilteredIntermediate F)
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Zero.tryRecv' : {m : Type → Type} →
  {α : Type} →
    [Monad m] →
      [MonadLiftT (ST IO.RealWorld) m] →
        [MonadLiftT BaseIO m] → Std.AtomicT (Std.CloseableChannel.Zero.State✝ α) m (Option α)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.right_cancel_posSubmonoid : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] (x y : R) (u : ↥(ValuativeRel.posSubmonoid R)),
  x * ↑u ≤ᵥ y * ↑u ↔ x ≤ᵥ y
-- Mathlib.Order.ModularLattice
Set.Iic.isCompl_inf_inf_of_isCompl_of_le : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : BoundedOrder α] [IsModularLattice α] {a b c : α},
  IsCompl b c → b ≤ a → IsCompl ⟨a ⊓ b, ⋯⟩ ⟨a ⊓ c, ⋯⟩
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
CategoryTheory.MonoidalCategory.Arrow.PullbackHom.isInitialIso_hom_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.MonoidalClosed C]
  [inst_4 : CategoryTheory.BraidedCategory C] (X : CategoryTheory.Arrow C) {I : C}
  (i : CategoryTheory.Limits.IsInitial I) {W : C},
  (CategoryTheory.MonoidalCategory.Arrow.PullbackHom.isInitialIso X i).hom.right = ⋯.isoPullback.inv
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.isLocalization_iff_of_base_ringEquiv : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] (h : R ≃+* P),
  IsLocalization M S ↔ IsLocalization (Submonoid.map h M) S
-- Aesop.Tree.Traversal
Aesop.TreeRef.rapp.sizeOf_spec : ∀ (rref : Aesop.RappRef), sizeOf (Aesop.TreeRef.rapp rref) = 1 + sizeOf rref
-- Mathlib.Order.Closure
LowerAdjoint.monotone : ∀ {α : Type u_1} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {u : β → α} (l : LowerAdjoint u),
  Monotone (u ∘ l.toFun)
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinOrder.powers_eq_image_range_orderOf : ∀ {G : Type u_1} [inst : Monoid G] {x : G} [inst_1 : DecidableEq G],
  IsOfFinOrder x → ↑(Submonoid.powers x) = ↑(Finset.image (fun x_1 => x ^ x_1) (Finset.range (orderOf x)))
-- Lean.PrettyPrinter.Delaborator.Basic
/-- Set the given option at the current position and execute `x` in this context.  -/
Lean.PrettyPrinter.Delaborator.withOptionAtCurrPos : {α : Type} →
  Lean.Name → Lean.DataValue → Lean.PrettyPrinter.Delaborator.DelabM α → Lean.PrettyPrinter.Delaborator.DelabM α
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.equiv_iff_eq_of_Z_eq' : ∀ {R : Type r} [inst : CommRing R] {P Q : Fin 3 → R}, P 2 = Q 2 → Q 2 ∈ nonZeroDivisors R → (P ≈ Q ↔ P = Q)
-- Mathlib.NumberTheory.Zsqrtd.GaussianInt
GaussianInt.im_toComplex : ∀ (x y : ℤ), (GaussianInt.toComplex { re := x, im := y }).im = ↑y
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.comap_injective_of_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {f : M →ₙ* N},
  Function.Surjective ⇑f → Function.Injective (Subsemigroup.comap f)