mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.excenterExists_compl : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) {signs : Finset (Fin (n + 1))},
  s.ExcenterExists signsᶜ ↔ s.ExcenterExists signs
-- Std.Internal.Do.Order.Basic
Lean.Order.meet_le_right : ∀ {α : Type u} [inst : Lean.Order.CompleteLattice α] (x y : α), Lean.Order.PartialOrder.rel (Lean.Order.meet x y) y
-- Init.Prelude
/-- Auxiliary function for `List.lengthTR`.  -/
List.lengthTRAux : {α : Type u_1} → List α → ℕ → ℕ
-- Mathlib.MeasureTheory.Measure.DiracProba
MeasureTheory.tendsto_diracProbaEquivSymm_iff_tendsto : ∀ {X : Type u_1} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : OpensMeasurableSpace X]
  [inst_3 : T0Space X] [CompletelyRegularSpace X] {μ : ↑(Set.range MeasureTheory.diracProba)}
  (F : Filter ↑(Set.range MeasureTheory.diracProba)),
  Filter.Tendsto (⇑MeasureTheory.diracProbaEquiv.symm) F (nhds (MeasureTheory.diracProbaEquiv.symm μ)) ↔
    Filter.Tendsto id F (nhds μ)
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.derivative_rootMultiplicity_of_root_of_mem_nonZeroDivisors : ∀ {R : Type u} [inst : CommRing R] {p : Polynomial R} {t : R},
  p.IsRoot t →
    ↑(Polynomial.rootMultiplicity t p) ∈ nonZeroDivisors R →
      Polynomial.rootMultiplicity t (Polynomial.derivative p) = Polynomial.rootMultiplicity t p - 1
-- Init.Data.Int.Linear
Int.Internal.Linear.mul_eq_kxk : ∀ (a b k₁ c k₂ k : ℤ), a = k₁ * c → b = k₂ → (k₁ * k₂ == k) = true → a * b = k * c
-- Mathlib.Data.FunLike.IsApply
IsNegApply.mk : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} [inst : FunLike F α β] [inst_1 : Neg β]
  [inst_2 : Neg F], (∀ (f : F) (x : α), (-f) x = -f x) → IsNegApply F α β
-- Mathlib.LinearAlgebra.Projection
Submodule.projection_add_projection_eq_id : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (hpq : IsCompl p q), p.projection q hpq + q.projection p ⋯ = LinearMap.id
-- Mathlib.Geometry.Manifold.Instances.Sphere
range_stereographic_symm : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {v : E} (hv : ‖v‖ = 1)
  (hv' : autoParam (v ∈ Metric.sphere 0 1) range_stereographic_symm._auto_1),
  Set.range ↑(stereographic hv).symm = {⟨v, hv'⟩}ᶜ
-- Mathlib.Order.Filter.Basic
Filter.eventually_sSup : ∀ {α : Type u} {p : α → Prop} {fs : Set (Filter α)}, (∀ᶠ (x : α) in sSup fs, p x) ↔ ∀ f ∈ fs, ∀ᶠ (x : α) in f, p x
-- Mathlib.Analysis.Convex.Jensen
ConvexOn.inf_le_of_mem_convexHull : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup β] [inst_5 : LinearOrder β] [IsOrderedAddMonoid β]
  [inst_7 : Module 𝕜 E] [inst_8 : Module 𝕜 β] [IsStrictOrderedModule 𝕜 β] {s : Set E} {f : E → β} {x : E}
  {t : Finset E}, ConcaveOn 𝕜 s f → ↑t ⊆ s → ∀ (hx : x ∈ (convexHull 𝕜) ↑t), t.inf' ⋯ f ≤ f x
-- Lean.Expr
Lean.Expr.sort.inj : ∀ {u u_1 : Lean.Level}, Lean.Expr.sort u = Lean.Expr.sort u_1 → u = u_1
-- Mathlib.AlgebraicTopology.DoldKan.Equivalence
/-- The functor `Γ` for the equivalence is the same as in the pseudoabelian case.  -/
CategoryTheory.Abelian.DoldKan.Γ : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    [inst_1 : CategoryTheory.Abelian A] → CategoryTheory.Functor (ChainComplex A ℕ) (CategoryTheory.SimplicialObject A)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.mem_map_iff_mem : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {f : M →ₙ* N},
  Function.Injective ⇑f → ∀ {S : Subsemigroup M} {x : M}, f x ∈ Subsemigroup.map f S ↔ x ∈ S
-- Init.Prelude
/-- Proves that `p` is decidable by supplying a proof of `p`  -/
Decidable.isTrue : {p : Prop} → p → Decidable p
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_const_sub_right : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ],
  MeasureTheory.Integrable Y μ →
    ∀ (c : ℝ), ProbabilityTheory.covariance X (fun ω => c - Y ω) μ = -ProbabilityTheory.covariance X Y μ
-- Lean.Elab.SyntheticMVars
_private.Lean.Elab.SyntheticMVars.0.Lean.Elab.Term.synthesizeUsingDefaultPrio.synthesizeUsingDefaultInstance : Lean.MVarId → Lean.Name → Lean.Elab.TermElabM Bool
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
CategoryTheory.MorphismProperty.LeftFraction₃.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} →
      {X Y Y' : C} → (X ⟶ Y') → (X ⟶ Y') → (X ⟶ Y') → (s : Y ⟶ Y') → W s → W.LeftFraction₃ X Y
-- Mathlib.LinearAlgebra.Matrix.Hermitian
Matrix.isHermitian_comp_iff_forall : ∀ {α : Type u_1} {m : Type u_3} {n : Type u_4} [inst : Star α] {A : Matrix m m (Matrix n n α)},
  ((Matrix.comp m m n n α) A).IsHermitian ↔ ∀ (i j : m) (i' j' : n), star (A j i j' i') = A i j i' j'
-- Mathlib.Lean.Meta.RefinedDiscrTree
/-- Returns candidates from this module that match the expression.  -/
Lean.Meta.RefinedDiscrTree.findModuleMatches : {α : Type} →
  Lean.Meta.RefinedDiscrTree.ModuleDiscrTreeRef α → Lean.Expr → Lean.MetaM (Lean.Meta.RefinedDiscrTree.MatchResult α)
-- Aesop.Rule.Name
Aesop.BuilderName.simp.sizeOf_spec : sizeOf Aesop.BuilderName.simp = 1
-- Mathlib.Topology.Category.CompHausLike.Limits
CompHausLike.pullback.cone_π : ∀ {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [inst : CompHausLike.HasExplicitPullback f g],
  (CompHausLike.pullback.cone f g).π =
    {
      app := fun j =>
        Option.rec (CategoryTheory.CategoryStruct.comp (CompHausLike.pullback.fst f g) f)
          (fun val =>
            CategoryTheory.Limits.WalkingPair.rec (CompHausLike.pullback.fst f g) (CompHausLike.pullback.snd f g) val)
          j,
      naturality := ⋯ }
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
CategoryTheory.Limits.weakLimit.π_comp_eqToHom_assoc : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {C : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_3, u_3} C] (F : CategoryTheory.Functor J C)
  [inst_2 : CategoryTheory.Limits.HasWeakLimit F] {j j' : J} (hj : j = j') {Z : C} (h : F.obj j' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.weakLimit.π F j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.weakLimit.π F j') h
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof.notCore.injEq : ∀ (e : Lean.Expr) (lhs rhs : Lean.Grind.CommRing.Expr) (e_1 : Lean.Expr) (lhs_1 rhs_1 : Lean.Grind.CommRing.Expr),
  (Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof.notCore e lhs rhs =
      Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof.notCore e_1 lhs_1 rhs_1) =
    (e = e_1 ∧ lhs = lhs_1 ∧ rhs = rhs_1)
-- Mathlib.Order.SuccPred.Basic
Order.pred_lt_iff_of_not_isMin' : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {a b : α}, ¬IsMin b → (Order.pred a < b ↔ a ≤ b)
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
nonpos_of_mul_nonneg_right : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] {a b : R} [MulPosStrictMono R], 0 ≤ a * b → a < 0 → b ≤ 0
-- Init.Data.List.Lex
List.map_lt : ∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LT β] {l₁ l₂ : List α} {f : α → β},
  (∀ (x y : α), x < y → f x < f y) → l₁ < l₂ → List.map f l₁ < List.map f l₂
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.instInhabited : {M : Type u_1} → [inst : AddZeroClass M] → Inhabited (AddSubmonoid M)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- The image of a binary fan by a functor.  -/
CategoryTheory.Limits.BinaryFan.map : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        (F : CategoryTheory.Functor C D) →
          {X Y : C} → CategoryTheory.Limits.BinaryFan X Y → CategoryTheory.Limits.BinaryFan (F.obj X) (F.obj Y)
-- Mathlib.Algebra.Notation.Defs
HVAdd.mk : {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → (α → β → γ) → HVAdd α β γ
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Flavors.bounded.injEq : ∀ {α : Type} (ch ch_1 : Std.CloseableChannel.Bounded✝ α),
  (Std.CloseableChannel.Flavors.bounded✝ ch = Std.CloseableChannel.Flavors.bounded✝ ch_1) = (ch = ch_1)
-- Mathlib.Topology.Semicontinuity.Defs
LowerSemicontinuous.lowerSemicontinuousAt : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β},
  LowerSemicontinuous f → ∀ (x : α), LowerSemicontinuousAt f x
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.inverse'_apply : ∀ {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [inst : SMul M X] {Y : Type u_6} [inst_1 : SMul N Y]
  {φ' : N → M} (f : X →ₑ[φ] Y) (g : Y → X) (k : Function.RightInverse φ' φ) (h₁ : Function.LeftInverse g ⇑f)
  (h₂ : Function.RightInverse g ⇑f) (a : Y), (f.inverse' g k h₁ h₂) a = g a
-- Mathlib.CategoryTheory.Abelian.Preradical.Colon
/-- There is a morphism `Φ ⟶ (Φ.colon Ψ)` induced by the universal property for the pullback
via `Φ.ι : Φ.r X ⟶ 𝟭 C` and the zero morphism `Φ.r ⟶  Φ.quotient ⋙ Ψ.r`.  -/
CategoryTheory.Abelian.Preradical.toColon : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] → (Φ Ψ : CategoryTheory.Abelian.Preradical C) → Φ ⟶ Φ.colon Ψ
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.id_apply : ∀ (X : PartOrdEmb) (x : ↑X), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x
-- Mathlib.Algebra.Group.AddChar
AddChar.mk.sizeOf_spec : ∀ {A : Type u_1} [inst : AddMonoid A] {M : Type u_2} [inst_1 : Monoid M] [inst_2 : SizeOf A] [inst_3 : SizeOf M]
  (toFun : A → M) (map_zero_eq_one' : toFun 0 = 1) (map_add_eq_mul' : ∀ (a b : A), toFun (a + b) = toFun a * toFun b),
  sizeOf { toFun := toFun, map_zero_eq_one' := map_zero_eq_one', map_add_eq_mul' := map_add_eq_mul' } =
    1 + sizeOf map_zero_eq_one'
-- Init.Data.UInt.Lemmas
USize.ne_of_lt : ∀ {a b : USize}, a < b → a ≠ b
-- Mathlib.RingTheory.RootsOfUnity.Minpoly
/-- Let `P` be the minimal polynomial of a root of unity `μ` and `Q` be the minimal polynomial of
`μ ^ p`, where `p` is a natural number that does not divide `n`. Then `P` divides `expand ℤ p Q`.  -/
IsPrimitiveRoot.minpoly_dvd_expand : ∀ {n : ℕ} {K : Type u_1} [inst : CommRing K] {μ : K},
  IsPrimitiveRoot μ n →
    ∀ [IsDomain K] [CharZero K] {p : ℕ}, ¬p ∣ n → minpoly ℤ μ ∣ (Polynomial.expand ℤ p) (minpoly ℤ (μ ^ p))
-- Mathlib.Algebra.MvPolynomial.Division
MvPolynomial.X_prime : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {i : σ} [IsCancelMulZero R] [Nontrivial R], Prime (MvPolynomial.X i)
-- Mathlib.Order.Heyting.Basic
le_hnot_inf_hnot : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] {a b : α}, ￢(a ⊔ b) ≤ ￢a ⊓ ￢b
-- Mathlib.Tactic.TFAE
/-- See `haveDecl`. Any of `tfaeHaveIdDecl`, `tfaeHavePatDecl`, or `tfaeHaveEqnsDecl`.  -/
Mathlib.Tactic.TFAE.Parser.tfaeHaveDecl : Lean.Parser.Parser
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.instIsRegularMonoOppositeOpOfIsRegularEpi : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.IsRegularEpi f],
  CategoryTheory.IsRegularMono f.op
-- Mathlib.CategoryTheory.Bicategory.Span.Basic
/-- A (Wₗ, Wᵣ)-span from c to c' is the data of an
object `a : C`, together with a morphism `a ⟶ c` in Wₗ,
and a morphism `a ⟶ c'` in Wᵣ.  -/
CategoryTheory.Span : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.MorphismProperty C → CategoryTheory.MorphismProperty C → C → C → Type (max u_1 v_1)
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
MDifferentiableWithinAt.change_section_trivialization : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB)
  {EM : Type u_10} [inst_8 : NormedAddCommGroup EM] [inst_9 : NormedSpace 𝕜 EM] {HM : Type u_11}
  [inst_10 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [inst_11 : TopologicalSpace M]
  [inst_12 : ChartedSpace HM M] [inst_13 : TopologicalSpace B] [inst_14 : ChartedSpace HB B] [inst_15 : FiberBundle F E]
  [inst_16 : (x : B) → AddCommMonoid (E x)] [inst_17 : (x : B) → Module 𝕜 (E x)] [inst_18 : VectorBundle 𝕜 F E]
  [ContMDiffVectorBundle 1 F E IB] {e : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e]
  {e' : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e'] {f : M → Bundle.TotalSpace F E}
  {s : Set M} {x₀ : M},
  MDiffAt[s] (Bundle.TotalSpace.proj ∘ f) x₀ →
    (MDiffAt[s] fun x => (↑e (f x)).2) x₀ → f x₀ ∈ e.source → f x₀ ∈ e'.source → (MDiffAt[s] fun x => (↑e' (f x)).2) x₀
-- Mathlib.NumberTheory.MulChar.Duality
MulChar.finite : ∀ {M : Type u_1} {R : Type u_2} [inst : CommMonoid M] [inst_1 : CommRing R] [Finite Mˣ] [IsDomain R],
  Finite (MulChar M R)
-- Aesop.Rule
Aesop.UnsafeRuleInfo.mk.inj : ∀ {successProbability successProbability_1 : Aesop.Percent},
  { successProbability := successProbability } = { successProbability := successProbability_1 } →
    successProbability = successProbability_1
-- Mathlib.CategoryTheory.Sites.MayerVietorisSquare
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] [inst_2 : SizeOf C] (toSquare : CategoryTheory.Square C)
  (mono_f₁₃ :
    autoParam (CategoryTheory.Mono toSquare.f₁₃)
      CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mono_f₁₃._autoParam)
  (isPushout : (toSquare.map (CategoryTheory.yoneda.comp (CategoryTheory.presheafToSheaf J (Type v)))).IsPushout),
  sizeOf { toSquare := toSquare, mono_f₁₃ := mono_f₁₃, isPushout := isPushout } =
    1 + sizeOf toSquare + sizeOf mono_f₁₃ + sizeOf isPushout
-- Std.Http.Protocol.H1.Writer
/-- Extracts all accumulated output data and returns it with a cleared output buffer.
 -/
Std.Http.Protocol.H1.Writer.takeOutput : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Writer dir → Option (Std.Http.Protocol.H1.Writer dir × ByteArray)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.isSome_minKey?_iff_ne_empty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t.minKey?.isSome = true ↔ t ≠ ∅
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
FormalMultilinearSeries.order_eq_find : ∀ {𝕜 : Type u} {E : Type v} {F : Type w} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [inst_4 : ContinuousAdd E] [inst_5 : ContinuousConstSMul 𝕜 E] [inst_6 : AddCommMonoid F]
  [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [inst_9 : ContinuousAdd F] [inst_10 : ContinuousConstSMul 𝕜 F]
  {p : FormalMultilinearSeries 𝕜 E F} [inst_11 : DecidablePred fun n => p n ≠ 0] (hp : ∃ n, p n ≠ 0),
  p.order = Nat.find hp
-- Init.Data.Vector.Lex
Vector.mk_le_mk : ∀ {α : Type u_1} {n : ℕ} {data₁ : Array α} {size₁ : data₁.size = n} {data₂ : Array α} {size₂ : data₂.size = n}
  [inst : LT α], Vector.mk data₁ size₁ ≤ Vector.mk data₂ size₂ ↔ data₁ ≤ data₂
-- Mathlib.Analysis.Normed.Lp.LpEquiv
coe_addEquiv_lpPiLp_symm : ∀ {α : Type u_1} {E : α → Type u_2} [inst : (i : α) → NormedAddCommGroup (E i)] {p : ENNReal} [inst_1 : Finite α]
  (f : PiLp p E), ↑(AddEquiv.lpPiLp.symm f) = f.ofLp
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Module.Basis.mk_range_eq_rank : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type w}
  [StrongRankCondition R] (v : Module.Basis ι R M), Cardinal.mk ↑(Set.range ⇑v) = Module.rank R M
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey?_ofList_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α]
  {l : List ((a : α) × β a)} {k : α},
  (List.map Sigma.fst l).contains k = false → (Std.DHashMap.ofList l).getKey? k = none
-- Mathlib.Data.Set.Basic
Set.union_eq_self_of_subset_left : ∀ {α : Type u} {s t : Set α}, s ⊆ t → s ∪ t = t
-- Init.Data.BitVec.Bitblast
/-- The output of `divRec` is a lawful state  -/
BitVec.lawful_divRec : ∀ {w : ℕ} {args : BitVec.DivModArgs w} {qr : BitVec.DivModState w},
  BitVec.DivModState.Lawful args qr → BitVec.DivModState.Lawful args (BitVec.divRec qr.wn args qr)
-- Init.Omega.Constraint
Lean.Omega.instReprConstraint.repr : Lean.Omega.Constraint → ℕ → Std.Format
-- Mathlib.Algebra.MvPolynomial.Eval
/-- If `f` is a right-inverse of `g` then `map f` is a right-inverse of `map g`.  -/
MvPolynomial.map_rightInverse : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] {f : R →+* S₁}
  {g : S₁ →+* R}, Function.RightInverse ⇑f ⇑g → Function.RightInverse ⇑(MvPolynomial.map f) ⇑(MvPolynomial.map g)
-- Mathlib.Topology.Basic
/-- If a filter `f` is majorated by some `𝓝 x`, then it is majorated by `𝓝 (Filter.lim f)`. We
formulate this lemma with a `[Nonempty X]` argument of `lim` derived from `h` to make it useful for
types without a `[Nonempty X]` instance. Because of the built-in proof irrelevance, Lean will unify
this instance with any other instance.  -/
le_nhds_lim : ∀ {X : Type u} [inst : TopologicalSpace X] {f : Filter X} (h : ∃ x, f ≤ nhds x), f ≤ nhds f.lim
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Unbounded.tryRecv' : {m : Type → Type} →
  {α : Type} →
    [Monad m] → [MonadLiftT (ST IO.RealWorld) m] → Std.AtomicT (Std.CloseableChannel.Unbounded.State✝ α) m (Option α)
-- Mathlib.CategoryTheory.Filtered.Small
_private.Mathlib.CategoryTheory.Filtered.Small.0.CategoryTheory.IsCofiltered.CofilteredClosureSmall.inductiveStepRealization.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsCofilteredOrEmpty C] (n : ℕ)
  (X : (k : ℕ) → k < n → (t : Type (max v w)) × (t → C))
  (a a_1 : CategoryTheory.IsCofiltered.CofilteredClosureSmall.InductiveStep✝ n X),
  a = a_1 →
    CategoryTheory.IsCofiltered.CofilteredClosureSmall.inductiveStepRealization✝ n X a =
      CategoryTheory.IsCofiltered.CofilteredClosureSmall.inductiveStepRealization✝ n X a_1
-- Std.Do.WP.SimpLemmas
_private.Std.Do.WP.SimpLemmas.0.Std.Do.EStateM.instWP.match_1.eq_2 : ∀ {ε σ α : Type u_1} (motive : EStateM.Result ε σ α → Sort u_2) (e : ε) (s' : σ)
  (h_1 : (a : α) → (s' : σ) → motive (EStateM.Result.ok a s'))
  (h_2 : (e : ε) → (s' : σ) → motive (EStateM.Result.error e s')),
  (match EStateM.Result.error e s' with
    | EStateM.Result.ok a s' => h_1 a s'
    | EStateM.Result.error e s' => h_2 e s') =
    h_2 e s'
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.target_subset_range : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β), e.target ⊆ Set.range ↑e
-- Mathlib.MeasureTheory.Constructions.UnitInterval
unitInterval.volume_apply : ∀ {s : Set ↑unitInterval}, MeasureTheory.volume s = MeasureTheory.volume (Subtype.val '' s)
-- Mathlib.AlgebraicTopology.SingularSet
/-- The geometric realization of a simplicial set.  -/
Simplicial.«term|_|» : Lean.ParserDescr
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.WithUpperSet.toUpperSet_ofUpperSet : ∀ {α : Type u_1} (a : Topology.WithUpperSet α),
  Topology.WithUpperSet.toUpperSet (Topology.WithUpperSet.ofUpperSet a) = a
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.limitLeftOpIsoUnopColimit_inv_comp_π_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor J Cᵒᵖ) [inst_2 : CategoryTheory.Limits.HasColimit F] (j : Jᵒᵖ) {Z : C}
  (h : F.leftOp.obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitLeftOpIsoUnopColimit F).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F.leftOp j) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F (Opposite.unop j)).unop h
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
QuadraticForm.associated_baseChange : ∀ {R : Type uR} {A : Type uA} {M₂ : Type uM₂} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : AddCommGroup M₂]
  [inst_3 : Algebra R A] [inst_4 : Module R M₂] [inst_5 : Invertible 2] [inst_6 : Invertible 2]
  (Q : QuadraticForm R M₂),
  QuadraticMap.associated (QuadraticForm.baseChange A Q) = LinearMap.BilinForm.baseChange A (QuadraticMap.associated Q)
-- Mathlib.Logic.Basic
exists_mem_or_left : ∀ {α : Sort u_1} {r p q : α → Prop}, (∃ x, ∃ (_ : p x ∨ q x), r x) ↔ (∃ x, ∃ (_ : p x), r x) ∨ ∃ x, ∃ (_ : q x), r x
-- Lean.Server.Completion.CompletionCollectors
_private.Lean.Server.Completion.CompletionCollectors.0.Lean.Server.Completion.State.mk.injEq : ∀ (items items_1 : Array Lean.Lsp.ResolvableCompletionItem),
  ({ items := items } = { items := items_1 }) = (items = items_1)
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
/-- The underlying set of points of a Delone set.  -/
Delone.DeloneSet.toSet : {X : Type u_1} → [inst : MetricSpace X] → Delone.DeloneSet X → Set X
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.isSuccPrelimit_mul_right : ∀ {a b : Ordinal.{u_4}}, Order.IsSuccLimit b → Order.IsSuccPrelimit (a * b)
-- Mathlib.Algebra.Homology.Embedding.TruncLEHomology
HomologicalComplex.shortComplexTruncLE_X₁ : ∀ {ι : 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.Abelian C] (K : HomologicalComplex C c')
  (e : c.Embedding c') [inst_2 : e.IsTruncLE], (K.shortComplexTruncLE e).X₁ = K.truncLE e
-- Mathlib.Topology.Bornology.Basic
Filter.HasBasis.disjoint_cobounded_iff : ∀ {α : Type u_2} [inst : Bornology α] {ι : Sort u_4} {p : ι → Prop} {s : ι → Set α} {l : Filter α},
  l.HasBasis p s → (Disjoint l (Bornology.cobounded α) ↔ ∃ i, p i ∧ Bornology.IsBounded (s i))
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.hcomp_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {G H : CategoryTheory.Functor C D} (α : G ⟶ H)
  (F : CategoryTheory.Functor D E), α ◫ CategoryTheory.CategoryStruct.id F = CategoryTheory.Functor.whiskerRight α F
-- Mathlib.Computability.NFA
/-- An NFA is a set of states (`σ`), a transition function from state to state labelled by the
alphabet (`step`), a set of starting states (`start`) and a set of acceptance states (`accept`).
Note the transition function sends a state to a `Set` of states. These are the states that it
may be sent to.  -/
NFA : Type u → Type v → Type (max u v)
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
/-- This shows `G2` can be defined as a certain absolutely convergent double sum.  -/
_private.Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform.0.EisensteinSeries.G2_eq_tsum_G2Term : ∀ (z : UpperHalfPlane), EisensteinSeries.G2 z = ∑' (m : ℤ) (n : ℤ), EisensteinSeries.G2Term✝ z ![m, n]
-- Mathlib.NumberTheory.Cyclotomic.Basic
instIsTorsionFreeCyclotomicFieldOfIsDomainOfIsFractionRing : ∀ (n : ℕ) (A : Type u) (K : Type w) [inst : CommRing A] [inst_1 : Field K] [inst_2 : Algebra A K] [IsDomain A]
  [IsFractionRing A K], Module.IsTorsionFree A (CyclotomicField n K)
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
NonUnitalSubsemiring.mk.sizeOf_spec : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] [inst_1 : SizeOf R] (toAddSubmonoid : AddSubmonoid R)
  (mul_mem' : ∀ {a b : R}, a ∈ toAddSubmonoid.carrier → b ∈ toAddSubmonoid.carrier → a * b ∈ toAddSubmonoid.carrier),
  sizeOf { toAddSubmonoid := toAddSubmonoid, mul_mem' := mul_mem' } = 1 + sizeOf toAddSubmonoid