mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Finset.Card
Finset.card_subtype : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (s : Finset α),
  (Finset.subtype p s).card = (Finset.filter p s).card
-- Mathlib.Tactic.Sat.FromLRAT
Sat.Literal.neg : ℕ → Sat.Literal
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.FunctorToTypes.shrinkCompUliftFunctorIso_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w'))
  [inst_1 : CategoryTheory.FunctorToTypes.Small.{w, w', v, u} F]
  [inst_2 : CategoryTheory.FunctorToTypes.Small.{max w w'', w', v, u} F] (X : C),
  (CategoryTheory.FunctorToTypes.shrinkCompUliftFunctorIso F).hom.app X =
    ((Equiv.ulift.trans (equivShrink (F.obj X)).symm).trans (equivShrink (F.obj X))).toIso.hom
-- Mathlib.Algebra.Order.Antidiag.Prod
/-- The class of additive monoids with an antidiagonal.  -/
Finset.HasAntidiagonal : (A : Type u_1) → [AddMonoid A] → Type u_1
-- Mathlib.Algebra.Module.Projective
Module.Projective.of_equiv : ∀ {R : Type u_8} {S : Type u_9} [inst : Semiring R] [inst_1 : Semiring S] {M : Type u_10} {N : Type u_11}
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : Module R M] [inst_5 : Module S N] {σ : R →+* S}
  {σ' : S →+* R} [inst_6 : RingHomInvPair σ σ'] [inst_7 : RingHomInvPair σ' σ] (e₂ : M ≃ₛₗ[σ] N)
  [Module.Projective R M], Module.Projective S N
-- Mathlib.RingTheory.PowerSeries.Evaluation
PowerSeries.eval₂_X : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] (φ : R →+* S) (a : S)
  [inst_2 : UniformSpace R] [inst_3 : UniformSpace S], PowerSeries.eval₂ φ a PowerSeries.X = a
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
/-- A right homology data `h` of a short complex `S` is preserved by a functor `F` is
`F` preserves the cokernel of `S.f : S.X₁ ⟶ S.X₂` and the kernel of `h.g' : h.Q ⟶ S.X₃`.  -/
CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            {S : CategoryTheory.ShortComplex C} →
              S.RightHomologyData → (F : CategoryTheory.Functor C D) → [F.PreservesZeroMorphisms] → Prop
-- Mathlib.Data.ENNReal.Basic
ENNReal.ofNat_ne_top : ∀ {n : ℕ} [inst : n.AtLeastTwo], OfNat.ofNat n ≠ ⊤
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskeringRightObjIdIso_inv_app_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {E : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} E]
  (X : CategoryTheory.Functor E C) (X_1 : E),
  (CategoryTheory.Functor.whiskeringRightObjIdIso.inv.app X).app X_1 = CategoryTheory.CategoryStruct.id (X.obj X_1)
-- Aesop.Tree.AddRapp
Aesop.AddRapp.successProbability : Aesop.AddRapp → Aesop.Percent
-- Mathlib.Algebra.GradedMonoid
/-- A version of `GradedMonoid.GOne` for internally graded objects.  -/
SetLike.GradedOne : {ι : Type u_1} → {R : Type u_2} → {S : Type u_3} → [SetLike S R] → [One R] → [Zero ι] → (ι → S) → Prop
-- Mathlib.Order.BooleanAlgebra.Set
Set.subset_ite : ∀ {α : Type u_1} {t s s' u : Set α}, u ⊆ t.ite s s' ↔ u ∩ t ⊆ s ∧ u \ t ⊆ s'
-- Mathlib.LinearAlgebra.Matrix.Swap
Matrix.GeneralLinearGroup.val_swap : ∀ (R : Type u_1) {n : Type u_2} [inst : CommRing R] [inst_1 : DecidableEq n] [inst_2 : Fintype n] (i j : n),
  ↑(Matrix.GeneralLinearGroup.swap R i j) = Matrix.swap R i j
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.mem_range_veblen : ∀ {o a : Ordinal.{u}}, o ≠ 0 → (a ∈ Set.range (Ordinal.veblen o) ↔ ∀ b < o, Ordinal.veblen b a = a)
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.edist_apply_le : ∀ {p : ENNReal} {ι : Type u_2} {β : ι → Type u_4} [hp : Fact (1 ≤ p)] [inst : Fintype ι]
  [inst_1 : (i : ι) → PseudoEMetricSpace (β i)] (x y : PiLp p β) (i : ι), edist (x.ofLp i) (y.ofLp i) ≤ edist x y
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.ext_iff : ∀ {E : Type u_3} [inst : AddGroup E] {p q : AddGroupSeminorm E}, p = q ↔ ∀ (x : E), p x = q x
-- Mathlib.Analysis.InnerProductSpace.LinearMap
InnerProductSpace.rankOne_one_left_eq_innerSL : ∀ {𝕜 : Type u_4} {F : Type u_6} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  (x : F), ((InnerProductSpace.rankOne 𝕜) 1) x = (innerSL 𝕜) x
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.Localization.exists_leftFraction : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : L.IsLocalization W] [W.HasLeftCalculusOfFractions] {X Y : C}
  (f : L.obj X ⟶ L.obj Y), ∃ φ, f = φ.map L ⋯
-- Mathlib.Algebra.DirectSum.Basic
/-- An alternative induction, where the addition assumption is restricted to singles.  -/
DirectSum.induction_on' : ∀ {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] [inst_1 : DecidableEq ι]
  {motive : (DirectSum ι fun i => β i) → Prop} (f : DirectSum ι fun i => β i),
  motive 0 →
    (∀ (i : ι) (b : β i) (f : DirectSum ι fun i => β i),
        f i = 0 → b ≠ 0 → motive f → motive ((DirectSum.of β i) b + f)) →
      motive f
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddSubsemigroup.coe_inf : ∀ {M : Type u_1} [inst : Add M] (p p' : AddSubsemigroup M), ↑(p ⊓ p') = ↑p ∩ ↑p'
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- Convert a `Bicone` over a function on `WalkingPair` to a BinaryBicone.  -/
CategoryTheory.Limits.Bicone.toBinaryBiconeFunctor : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        CategoryTheory.Functor (CategoryTheory.Limits.Bicone (CategoryTheory.Limits.pairFunction X Y))
          (CategoryTheory.Limits.BinaryBicone X Y)
-- Mathlib.Probability.Kernel.Proper
/-- **Alias** of the reverse direction of `ProbabilityTheory.Kernel.isProper_iff_inter_eq_indicator_mul`. -/
ProbabilityTheory.Kernel.IsProper.of_inter_eq_indicator_mul : ∀ {X : Type u_1} {𝓑 𝓧 : MeasurableSpace X} {π : ProbabilityTheory.Kernel X X},
  𝓑 ≤ 𝓧 →
    (∀ ⦃A : Set X⦄,
        MeasurableSet A → ∀ ⦃B : Set X⦄, MeasurableSet B → ∀ (x : X), (π x) (A ∩ B) = B.indicator 1 x * (π x) A) →
      π.IsProper
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Real.contDiffAt_arcsin : ∀ {x : ℝ}, x ≠ -1 → x ≠ 1 → ∀ {n : WithTop ℕ∞}, ContDiffAt ℝ n Real.arcsin x
-- Init.Data.String.Lemmas.Iterate
_private.Init.Data.String.Lemmas.Iterate.0.String.Slice.revPositionsFrom.eq_1 : ∀ (s : String.Slice) (p : s.Pos), s.revPositionsFrom p = { internalState := { currPos := p } }
-- Mathlib.LinearAlgebra.AffineSpace.Slope
StrictMonoOn.slope_pos : ∀ {k : Type u_1} {E : Type u_2} [inst : Field k] [inst_1 : AddCommGroup E] [inst_2 : Module k E]
  [inst_3 : LinearOrder k] [IsStrictOrderedRing k] [inst_5 : PartialOrder E] [IsOrderedAddMonoid E] [PosSMulMono k E]
  {f : k → E} {x y : k} {s : Set k}, StrictMonoOn f s → x ∈ s → y ∈ s → x ≠ y → 0 < slope f x y
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.PartialIso.trans'_source : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X.PartialIso Y) (g : Y.PartialIso Z) (e : f.target = g.source),
  (f.trans' g e).source = f.source
-- Init.Data.Array.Monadic
Array.mapM_eq_foldlM_push : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {f : α → m β} {xs : Array α},
  Array.mapM f xs =
    Array.foldlM
      (fun acc a => do
        let __do_lift ← f a
        pure (acc.push __do_lift))
      #[] xs
-- Mathlib.Data.Part
Part.some_add_some : ∀ {α : Type u_1} [inst : Add α] (a b : α), Part.some a + Part.some b = Part.some (a + b)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
/-- **Alias** of the reverse direction of `SimpleGraph.Walk.length_eq_zero_iff`. -/
SimpleGraph.Walk.Nil.length_eq_zero : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v}, p.Nil → p.length = 0
-- Init.Data.Dyadic.Basic
/-- Multiply two dyadic numbers.  -/
Dyadic.pow : Dyadic → ℕ → Dyadic
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.instDecidableCmpLTOfTransCmp : {α : Type u_1} → {x y : α} → (cmp : α → α → Ordering) → [Std.TransCmp cmp] → Decidable (RBTree.RBNode.cmpLT cmp x y)
-- Std.Time.DateTime.PlainDateTime
/-- Creates a new `PlainDateTime` by adjusting the `nano` component of its `time` to the given value.
 -/
Std.Time.PlainDateTime.withNanoseconds : Std.Time.PlainDateTime → Std.Time.Nanosecond.Ordinal → Std.Time.PlainDateTime
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.isRegularEpi_of_regularEpi : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} (h : CategoryTheory.RegularEpi f),
  CategoryTheory.IsRegularEpi f
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
CategoryTheory.CardinalDirectedPoset.isCardinalPresentable_of_hasCardinalLT_of_le : ∀ {κ : Cardinal.{u}} [inst : Fact κ.IsRegular] (J : CategoryTheory.CardinalDirectedPoset κ) {κ' : Cardinal.{u}}
  [inst_1 : Fact κ'.IsRegular], HasCardinalLT (↑J.obj) κ' → κ ≤ κ' → CategoryTheory.IsCardinalPresentable J κ'
-- Mathlib.Topology.Algebra.InfiniteSum.Order
Summable.tsum_le_tsum : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : AddCommMonoid α] [inst_1 : Preorder α]
  [IsOrderedAddMonoid α] [inst_3 : TopologicalSpace α] [OrderClosedTopology α] {f g : ι → α} [L.NeBot],
  (∀ (i : ι), f i ≤ g i) → Summable f L → Summable g L → ∑'[L] (i : ι), f i ≤ ∑'[L] (i : ι), g i
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
CategoryTheory.IsPullback.of_hasBinaryBiproduct : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [inst_3 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  CategoryTheory.IsPullback 0 0 CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.biprod.inr
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.getKeyD_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] {k fallback : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getD k fallback = t₂.getD k fallback
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.RightFractionRel.unop : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty Cᵒᵖ} {X Y : Cᵒᵖ}
  {z₁ z₂ : W.RightFraction X Y},
  CategoryTheory.MorphismProperty.RightFractionRel z₁ z₂ →
    CategoryTheory.MorphismProperty.LeftFractionRel z₁.unop z₂.unop
-- Mathlib.FieldTheory.SeparableDegree
/-- The `Field.finSepDegree F E` is equal to the cardinality of `E →ₐ[F] K` as a natural number,
when `E / F` is algebraic and `K / F` is algebraically closed.  -/
Field.finSepDegree_eq_of_isAlgClosed : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type w) [inst_3 : Field K]
  [inst_4 : Algebra F K] [Algebra.IsAlgebraic F E] [IsAlgClosed K], Field.finSepDegree F E = Nat.card (E →ₐ[F] K)
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.hasLimit_cospan_forget_of_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Z)
  (g : Y ⟶ Z) [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f],
  CategoryTheory.Limits.HasLimit
    ((CategoryTheory.Limits.cospan g f).comp AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace)
-- Mathlib.Order.PartialSups
disjoint_partialSups_left : ∀ {α : Type u_1} {ι : Type u_3} [inst : Preorder ι] [inst_1 : LocallyFiniteOrderBot ι] [inst_2 : DistribLattice α]
  [inst_3 : OrderBot α] {f : ι → α} {i : ι} {x : α}, Disjoint ((partialSups f) i) x ↔ ∀ j ≤ i, Disjoint (f j) x
-- Std.Http.Data.Status
/-- Checks if the status code is a success status, meaning that the request was successfully received,
understood, and accepted.

Reference: https://httpwg.org/specs/rfc9110.html#status.codes
 -/
Std.Http.Status.isSuccess : Std.Http.Status → Bool
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
AlgHom.bijective : ∀ {K : Type u_1} {S : Type u_2} [inst : Field K] [inst_1 : Ring S] [IsSimpleRing S] [inst_3 : Algebra K S]
  [FiniteDimensional K S] (f : S →ₐ[K] S), Function.Bijective ⇑f
-- Mathlib.Order.Filter.AtTopBot.Tendsto
/-- A function `f` goes to `-∞` independent of an order-preserving embedding `e`.  -/
Filter.tendsto_atBot_embedding : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β} {e : β → γ}
  {l : Filter α},
  (∀ (b₂ b₁ : β), e b₂ ≤ e b₁ ↔ b₂ ≤ b₁) →
    (∀ (c : γ), ∃ b, e b ≤ c) → (Filter.Tendsto (e ∘ f) l Filter.atBot ↔ Filter.Tendsto f l Filter.atBot)
-- Lean.Message
Lean.instToMessageDataList : {α : Type} → [Lean.ToMessageData α] → Lean.ToMessageData (List α)
-- Mathlib.Order.Bounds.Image
mem_upperBounds_image2_of_mem_upperBounds_of_mem_upperBounds : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {f : α → β → γ}
  {s : Set α} {t : Set β} {a : α} {b : β},
  (∀ (b : β), Antitone (Function.swap f b)) →
    (∀ (a : α), Monotone (f a)) → a ∈ lowerBounds s → b ∈ upperBounds t → f a b ∈ upperBounds (Set.image2 f s t)
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.setIntegral_condExpInd : ∀ {α : Type u_1} {G' : Type u_5} [inst : NormedAddCommGroup G'] [inst_1 : NormedSpace ℝ G'] [CompleteSpace G']
  {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α} {hm : m ≤ m0}
  [inst_3 : MeasureTheory.SigmaFinite (μ.trim hm)],
  MeasurableSet s →
    MeasurableSet t →
      μ s ≠ ⊤ →
        μ t ≠ ⊤ → ∀ (x : G'), ∫ (a : α) in s, ↑↑((MeasureTheory.condExpInd G' hm μ t) x) a ∂μ = μ.real (t ∩ s) • x
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.euclidean.stdOrthonormalBasis_map_eq : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  (NumberField.mixedEmbedding.euclidean.stdOrthonormalBasis K).toBasis.map
      ↑(NumberField.mixedEmbedding.euclidean.toMixed K) =
    NumberField.mixedEmbedding.stdBasis K
-- Mathlib.AlgebraicTopology.DoldKan.NCompGamma
AlgebraicTopology.DoldKan.Γ₂N₁_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C],
  AlgebraicTopology.DoldKan.Γ₂N₁.inv = AlgebraicTopology.DoldKan.Γ₂N₁.natTrans
-- Mathlib.Analysis.Complex.MeanValue
/-- **Alias** of `DiffContOnCl.circleAverage`.

---

The **Mean Value Property** of complex differentiable functions: If `f : ℂ → E` is complex
differentiable at all points of a closed disc of radius `R` and center `c`, then the circle average
`circleAverage f c R` equals `f c`.
 -/
circleAverage_of_differentiable_on : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {R : ℝ} {c : ℂ},
  DiffContOnCl ℂ f (Metric.ball c |R|) → Real.circleAverage f c R = f c
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
/-- *Ionescu-Tulcea Theorem* : Given a family of kernels `κ n` taking variables in `Iic n` with
value in `X (n + 1)`, the kernel `traj κ a` takes a variable `x` depending on the
variables `i ≤ a` and associates to it a kernel on trajectories depending on all variables,
where the entries with index `≤ a` are those of `x`, and then one follows iteratively the
kernels `κ a`, then `κ (a + 1)`, and so on.

The fact that such a kernel exists on infinite trajectories is not obvious, and is the content of
the Ionescu-Tulcea theorem.  -/
ProbabilityTheory.Kernel.traj : {X : ℕ → Type u_1} →
  [inst : (n : ℕ) → MeasurableSpace (X n)] →
    (κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))) →
      [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] →
        (a : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic a)) → X ↑i) ((n : ℕ) → X n)
-- Mathlib.Order.Heyting.Hom
BiheytingHom.instPartialOrder : {α : Type u_2} →
  {β : Type u_3} → [inst : BiheytingAlgebra α] → [inst_1 : BiheytingAlgebra β] → PartialOrder (BiheytingHom α β)
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.comp_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {A B : CategoryTheory.Mon C} {M N O : Bimod A B} (f : M.Hom N) (g : N.Hom O),
  (Bimod.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
-- Mathlib.Topology.Homotopy.Path
Path.Homotopy.symm_trans : ∀ {X : Type u} [inst : TopologicalSpace X] {x₀ x₁ : X} {p₀ p₁ p₂ : Path x₀ x₁} (F : p₀.Homotopy p₁)
  (G : p₁.Homotopy p₂), (F.trans G).symm = G.symm.trans F.symm
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeAddGroup.instDecidableEq : {α : Type u_1} → [DecidableEq α] → DecidableEq (FreeAddGroup α)
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.InitEntry.mk.inj : ∀ {α : Type} {key : Lean.Meta.LazyDiscrTree.Key} {entry : Lean.Meta.LazyDiscrTree.LazyEntry α}
  {key_1 : Lean.Meta.LazyDiscrTree.Key} {entry_1 : Lean.Meta.LazyDiscrTree.LazyEntry α},
  { key := key, entry := entry } = { key := key_1, entry := entry_1 } → key = key_1 ∧ entry = entry_1
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Sigma.map_id : ∀ {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f : α → C}
  [inst_1 : CategoryTheory.Limits.HasCoproduct f],
  (CategoryTheory.Limits.Sigma.map fun a => CategoryTheory.CategoryStruct.id (f a)) =
    CategoryTheory.CategoryStruct.id (∐ f)
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.stdPart_monotoneOn : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K],
  MonotoneOn ArchimedeanClass.stdPart {x | 0 ≤ ArchimedeanClass.mk x}
-- Mathlib.Data.Finset.MulAntidiagonal
Finset.mem_mulAntidiagonal : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelMonoid α] {s t : Set α}
  {hs : s.IsPWO} {ht : t.IsPWO} {a : α} {x : α × α},
  x ∈ Finset.mulAntidiagonal hs ht a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 * x.2 = a
-- Init.Data.Slice.Array.Basic
instSliceableArrayNatSubarray_8 : {α : Type u} → Std.Rii.Sliceable (Array α) ℕ (Subarray α)
-- Mathlib.AlgebraicTopology.ModelCategory.Opposite
HomotopicalAlgebra.instHasFactorizationOppositeCofibrationsTrivialFibrationsOfTrivialCofibrationsFibrations : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  [(HomotopicalAlgebra.trivialCofibrations C).HasFactorization (HomotopicalAlgebra.fibrations C)],
  (HomotopicalAlgebra.cofibrations Cᵒᵖ).HasFactorization (HomotopicalAlgebra.trivialFibrations Cᵒᵖ)
-- Mathlib.Topology.Inseparable
SeparationQuotient.continuousAt_lift : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x : X} {f : X → Y}
  {hf : ∀ (x y : X), Inseparable x y → f x = f y},
  ContinuousAt (SeparationQuotient.lift f hf) (SeparationQuotient.mk x) ↔ ContinuousAt f x
-- Mathlib.LinearAlgebra.Span.Basic
LinearMap.toSpanSingleton_apply_one : ∀ (R : Type u_1) (M : Type u_4) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x : M),
  (LinearMap.toSpanSingleton R M x) 1 = x
-- Init.Data.String.Defs
/-- Accesses the indicated byte in the UTF-8 encoding of the string slice, or panics if the position
is out-of-bounds.
 -/
String.Slice.getUTF8Byte! : String.Slice → String.Pos.Raw → UInt8
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_le_size_erase : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, m.size ≤ (m.erase k).size + 1
-- Lean.Parser.Attr
Lean.Parser.Attr.class.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Dynamics.Flow
/-- Restriction of a flow onto an invariant set.  -/
Flow.restrict : {τ : Type u_1} →
  {α : Type u_2} →
    [inst : TopologicalSpace τ] →
      [inst_1 : TopologicalSpace α] →
        [inst_2 : AddZero τ] → (ϕ : Flow τ α) → {s : Set α} → IsInvariant ϕ.toFun s → Flow τ ↑s
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
/-- A type synonym for endowing a given type with a `CStarModule` structure. This has the scoped
notation `C⋆ᵐᵒᵈ`.  -/
WithCStarModule.«termC⋆ᵐᵒᵈ(_,_)» : Lean.ParserDescr
-- Mathlib.Algebra.Category.HopfAlgCat.Basic
/-- The underlying type.  -/
HopfAlgCat.carrier : {R : Type u} → [inst : CommRing R] → HopfAlgCat R → Type v
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.nonempty_left : ∀ {G : Type u_1} [inst : Group G] {S T : Set G}, Subgroup.IsComplement S T → S.Nonempty
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.maxD_erase_eq_of_not_compare_maxD_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k fallback : α},
      (t.erase k).isEmpty = false → ¬cmp k (t.maxD fallback) = Ordering.eq → (t.erase k).maxD fallback = t.maxD fallback
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- **Alias** of `Left.mul_lt_one`.

---

Assumes left covariance.
The lemma assuming right covariance is `Right.mul_lt_one`.  -/
mul_lt_one : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulLeftStrictMono α] {a b : α}, a < 1 → b < 1 → a * b < 1
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.preimage_of_isIso : ∀ {X Y : AlgebraicGeometry.Scheme} {U : Y.Opens},
  AlgebraicGeometry.IsAffineOpen U →
    ∀ (f : X ⟶ Y) [CategoryTheory.IsIso f], AlgebraicGeometry.IsAffineOpen ((TopologicalSpace.Opens.map f.base).obj U)
-- Mathlib.Data.Real.ConjExponents
NNReal.HolderTriple.inv_ne_zero : ∀ {p q r : NNReal}, p.HolderTriple q r → p⁻¹ ≠ 0
-- Mathlib.Probability.Process.HittingTime
/-- **Alias** of `MeasureTheory.Adapted.isStoppingTime_hittingAfter`. -/
MeasureTheory.hittingAfter_isStoppingTime : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : ConditionallyCompleteLinearOrder ι]
  [WellFoundedLT ι] [Countable ι] {x : MeasurableSpace β} {f : MeasureTheory.Filtration ι m} {u : ι → Ω → β} {s : Set β}
  {n : ι},
  MeasureTheory.Adapted f u → MeasurableSet s → MeasureTheory.IsStoppingTime f (MeasureTheory.hittingAfter u s n)
-- Mathlib.Combinatorics.Matroid.Circuit
/-- The fundamental cocircuit for `B` and `e`:
that is, the unique cocircuit `K` of `M` for which `K ∩ B = {e}`.
Should be used when `B` is a base and `e ∈ B`.
Has the junk value `{e}` if `e ∉ B` or `e ∉ M.E`.  -/
Matroid.fundCocircuit : {α : Type u_1} → Matroid α → α → Set α → Set α
-- Mathlib.FieldTheory.NormalizedTrace
Algebra.normalizedTrace_eq_of_finiteDimensional : ∀ (F : Type u_1) (K : Type u_2) [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K] [inst_3 : CharZero F]
  [inst_4 : Algebra.IsIntegral F K] [FiniteDimensional F K],
  Algebra.normalizedTrace F K = (↑(Module.finrank F K))⁻¹ • Algebra.trace F K
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
/-- An `OrderMonoidWithZeroHom` is a monotone function.  -/
OrderMonoidWithZeroHom.monotone' : ∀ {α : Type u_6} {β : Type u_7} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulZeroOneClass α]
  [inst_3 : MulZeroOneClass β] (self : α →*₀o β), Monotone (↑self.toMonoidWithZeroHom).toFun
-- Mathlib.Topology.Order.SuccPred
PredOrder.isOpen_singleton_iff : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α] {a : α} [PredOrder α]
  [NoMinOrder α], IsOpen {a} ↔ ¬Order.IsPredLimit a
-- Mathlib.RingTheory.Ideal.Oka
Ideal.IsOka.mk : ∀ {R : Type u_1} [inst : CommSemiring R] {P : Ideal R → Prop},
  P ⊤ →
    (∀ {I : Ideal R} {a : R}, P (I ⊔ Ideal.span {a}) → P (Submodule.colon I ↑(Ideal.span {a})) → P I) → Ideal.IsOka P
-- Mathlib.Data.ENNReal.Basic
ENNReal.one_eq_coe : ∀ {r : NNReal}, 1 = ↑r ↔ 1 = r
-- Lean.Meta.Tactic.Grind.EMatch
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.withInitApp : {α : Type} → Lean.Expr → Lean.Meta.Grind.EMatch.M α → Lean.Meta.Grind.EMatch.M α
-- Mathlib.Analysis.Real.Pi.Wallis
Real.Wallis.tendsto_W_nhds_pi_div_two : Filter.Tendsto Real.Wallis.W Filter.atTop (nhds (Real.pi / 2))