mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonLeanImportMetaKind.fromJson : Lean.Json → Except String Lean.Lsp.LeanImportMetaKind
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Sphere.isDiameter_comm : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p₁ p₂ : P}, s.IsDiameter p₁ p₂ ↔ s.IsDiameter p₂ p₁
-- Mathlib.GroupTheory.Perm.Cycle.Basic
/-- Unlike `support_congr`, which assumes that `∀ (x ∈ g.support), f x = g x)`, here
we have the weaker assumption that `∀ (x ∈ f.support), f x = g x`.  -/
Equiv.Perm.IsCycle.support_congr : ∀ {α : Type u_2} {f g : Equiv.Perm α} [inst : DecidableEq α] [inst_1 : Fintype α],
  f.IsCycle → g.IsCycle → f.support ⊆ g.support → (∀ x ∈ f.support, f x = g x) → f = g
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.vanishingIdeal_univ : ∀ {R : Type u} [inst : CommSemiring R], PrimeSpectrum.vanishingIdeal Set.univ = nilradical R
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.instDecidableMem : {α : Type u} →
  {β : α → Type v} → [inst : BEq α] → [inst_1 : Hashable α] → {m : Std.DHashMap.Raw α β} → {a : α} → Decidable (a ∈ m)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKeyD_minKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → t.isEmpty = false → ∀ {fallback : α}, t.getKeyD t.minKey! fallback = t.minKey!
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
/-- Equivalence between a subgraph with deleted vertices and its corresponding simple graph.  -/
SimpleGraph.Subgraph.coeDeleteVertsIso : {V : Type u} →
  {G : SimpleGraph V} →
    {G' : G.Subgraph} → (s : Set V) → (G'.deleteVerts s).coe ≃g SimpleGraph.induce {v | ↑v ∉ s} G'.coe
-- Std.Tactic.BVDecide.LRAT.Internal.CompactLRATChecker
Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker : {n : ℕ} →
  Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n →
    Array Std.Tactic.BVDecide.LRAT.IntAction → Std.Tactic.BVDecide.LRAT.Internal.Result
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.mkPrecomp_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {Y : C} {S : CategoryTheory.Functor C D} (f : S.obj Y ⟶ T),
  CategoryTheory.CostructuredArrow.mkPrecomp f (CategoryTheory.CategoryStruct.id Y) = CategoryTheory.eqToHom ⋯
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.RightLift.whiskering_obj : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a} {x : B} (h : x ⟶ c)
  (t : CategoryTheory.Bicategory.RightLift f g), (CategoryTheory.Bicategory.RightLift.whiskering h).obj t = t.whisker h
-- Mathlib.Algebra.GroupWithZero.Associated
Associated.irreducible_iff : ∀ {M : Type u_1} [inst : Monoid M] {p q : M}, Associated p q → (Irreducible p ↔ Irreducible q)
-- Batteries.Data.Float.Lemmas
Float.Model.UnpackedFloat.isNaN.eq_2 : ∀ (x : Float.Model.UnpackedFloat), (x = Float.Model.UnpackedFloat.notANumber → False) → x.isNaN = false
-- Mathlib.Topology.Homotopy.LocallyContractible
/-- Open embeddings preserve strong local contractibility: if `X` is strongly locally contractible
and `e : Y → X` is an open embedding, then `Y` is strongly locally contractible.  -/
Topology.IsOpenEmbedding.stronglyLocallyContractibleSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [StronglyLocallyContractibleSpace X] {e : Y → X}, Topology.IsOpenEmbedding e → StronglyLocallyContractibleSpace Y
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.monotone_isoClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], Monotone CategoryTheory.MorphismProperty.isoClosure
-- Mathlib.Algebra.Ring.Parity
Even.neg_pow : ∀ {α : Type u_2} [inst : Monoid α] [inst_1 : HasDistribNeg α] {n : ℕ}, Even n → ∀ (a : α), (-a) ^ n = a ^ n
-- Mathlib.Order.Interval.Finset.Floor
Nat.cast_mem_Ioc_iff : ∀ {α : Type u_1} [inst : Semiring α] [inst_1 : LinearOrder α] [inst_2 : FloorSemiring α] {a b : α} {n : ℕ},
  0 ≤ a → 0 ≤ b → (↑n ∈ Set.Ioc a b ↔ n ∈ Finset.Ioc ⌊a⌋₊ ⌊b⌋₊)
-- Init.Data.Slice.Array.Lemmas
_private.Init.Data.Slice.Array.Lemmas.0.Subarray.take.eq_1 : ∀ {α : Type u_1} (arr : Subarray α) (i : ℕ),
  arr.take i =
    {
      internalRepresentation :=
        { array := arr.array, start := arr.start, stop := min (arr.start + i) arr.stop, start_le_stop := ⋯,
          stop_le_array_size := ⋯ } }
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
_private.Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion.0.termℍₒ : Lean.ParserDescr
-- Lean.Environment
Lean.OLeanEntries.server : {α : Type} → Lean.OLeanEntries α → α
-- Mathlib.Analysis.Complex.UpperHalfPlane.Topology
UpperHalfPlane.verticalStrip_mono : ∀ {A B A' B' : ℝ}, A ≤ A' → B' ≤ B → UpperHalfPlane.verticalStrip A B ⊆ UpperHalfPlane.verticalStrip A' B'
-- Mathlib.Topology.Algebra.IsUniformGroup.Constructions
Prod.instIsUniformAddGroup : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] [inst_2 : UniformSpace G]
  [hG : IsUniformAddGroup G] [inst_3 : UniformSpace H] [hH : IsUniformAddGroup H], IsUniformAddGroup (G × H)
-- Init.Data.Vector.Find
Vector.map_findSome? : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} {f : α → Option β} {g : β → γ} {xs : Vector α n},
  Option.map g (Vector.findSome? f xs) = Vector.findSome? (Option.map g ∘ f) xs
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.coe_symm_toHomeomorph : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂), ⇑e.toHomeomorph.symm = ⇑e.symm
-- Mathlib.Algebra.Order.Module.Defs
smul_pos' : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulWithZero α β]
  [inst_3 : Preorder α] [inst_4 : Preorder β] [SMulPosStrictMono α β], 0 < a → 0 < b → 0 < a • b
-- Mathlib.Algebra.Group.Basic
dite_vadd : ∀ {α : Type u_1} {β : Type u_2} [inst : VAdd β α] (p : Prop) [inst_1 : Decidable p] (a : α) (b : p → β) (c : ¬p → β),
  (if h : p then b h else c h) +ᵥ a = if h : p then b h +ᵥ a else c h +ᵥ a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.constEntryAtIdx?_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {i : ℕ}, Std.DTreeMap.Internal.Impl.Const.entryAtIdx? t₁ i = Std.DTreeMap.Internal.Impl.Const.entryAtIdx? t₂ i
-- Mathlib.Order.UpperLower.Basic
OrderEmbedding.image_Iio : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ↪o β),
  IsLowerSet (Set.range ⇑e) → ∀ (a : α), ⇑e '' Set.Iio a = Set.Iio (e a)
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.ι_colimitIsoColimitGrothendieck_inv : ∀ {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) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H] (G : CategoryTheory.Functor C H)
  [inst_3 : L.HasPointwiseLeftKanExtension G] [inst_4 : CategoryTheory.Limits.HasColimitsOfShape D H]
  [inst_5 : CategoryTheory.Limits.HasColimitsOfShape C H]
  (X : CategoryTheory.Grothendieck (CategoryTheory.CostructuredArrow.functor L)),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι ((CategoryTheory.CostructuredArrow.grothendieckProj L).comp G) X)
      (L.colimitIsoColimitGrothendieck G).inv =
    CategoryTheory.Limits.colimit.ι G ((CategoryTheory.CostructuredArrow.proj L X.base).obj X.fiber)
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.coe_inv : ∀ {R : Type u_1} {E : Type u_5} [inst : Semiring R] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module R E]
  (e : E ≃ₗᵢ[R] E), ⇑e⁻¹ = ⇑e.symm
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.isOpenEmbedding : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f], Topology.IsOpenEmbedding ⇑f
-- Mathlib.Algebra.Group.Equiv.Opposite
/-- `AddOpposite.op` on a commutative additive monoid is an isomorphism.  -/
AddOpposite.opAddEquiv : {M : Type u_1} → [inst : AddCommMonoid M] → M ≃+ Mᵃᵒᵖ
-- Mathlib.Data.Real.Basic
/-- The type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.  -/
Real : Type
-- Mathlib.RepresentationTheory.Basic
Representation.instFiniteAsModule : ∀ {k : Type u_4} {G : Type u_5} {V : Type u_6} [inst : Semiring k] [inst_1 : Monoid G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module k V] [Module.Finite k V] (ρ : Representation k G V), Module.Finite k ρ.asModule
-- Mathlib.Order.Interval.Set.SuccPred
Set.insert_Ico_left_eq_Ico_pred_of_not_isMin : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {a b : α},
  a ≤ b → ¬IsMin a → insert (Order.pred a) (Set.Ico a b) = Set.Ico (Order.pred a) b
-- Mathlib.SetTheory.Cardinal.Free
nonempty_ring_iff : ∀ (α : Type u), Nonempty (Ring α) ↔ Nonempty α
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.LeftHomologyData.canonical_H : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology],
  (CategoryTheory.ShortComplex.LeftHomologyData.canonical S).H = S.homology
-- Mathlib.Analysis.Analytic.IteratedFDeriv
/-- The `n`-th iterated derivative of an analytic function on a set is symmetric.  -/
AnalyticOn.iteratedFDerivWithin_comp_perm : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {s : Set E} {x : E},
  AnalyticOn 𝕜 f s →
    UniqueDiffOn 𝕜 s →
      x ∈ s →
        ∀ {n : ℕ} (v : Fin n → E) (σ : Equiv.Perm (Fin n)),
          (iteratedFDerivWithin 𝕜 n f s x) (v ∘ ⇑σ) = (iteratedFDerivWithin 𝕜 n f s x) v
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.aemeasurable_exp_mul : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} (t : ℝ),
  AEMeasurable X μ → MeasureTheory.AEStronglyMeasurable (fun ω => Real.exp (t * X ω)) μ
-- Mathlib.Order.CompleteLattice.Basic
Function.Surjective.iInf_congr : ∀ {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [inst : InfSet α] {f : ι → α} {g : ι' → α} (h : ι → ι'),
  Function.Surjective h → (∀ (x : ι), g (h x) = f x) → ⨅ x, f x = ⨅ y, g y
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
/-- If the set where you want `f` to be smooth lies entirely in a single chart, and `f` maps it
into a single chart, the smoothness of `f` on that set can be expressed by purely looking in
these charts.
Note: this lemma uses `extChartAt I x '' s` instead of `(extChartAt I x).symm ⁻¹' s` to ensure
that this set lies in `(extChartAt I x).target`.  -/
mdifferentiableOn_iff_of_subset_source' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M}
  [IsManifold I 1 M] [IsManifold I' 1 M'] {x : M} {y : M'},
  s ⊆ (extChartAt I x).source →
    Set.MapsTo f s (extChartAt I' y).source →
      (MDiff[s] f ↔ DifferentiableOn 𝕜 (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) '' s))
-- Mathlib.Algebra.Order.Floor.Extended
ENat.toENNReal_iSup : ∀ {ι : Sort u_1} (f : ι → ℕ∞), ↑(⨆ i, f i) = ⨆ i, ↑(f i)
-- Mathlib.Data.Finset.Image
Finset.image_subset_image_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} {s t : Finset α},
  Function.Injective f → (Finset.image f s ⊆ Finset.image f t ↔ s ⊆ t)
-- Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
BoundedContinuousFunction.char_neg : ∀ {V : Type u_1} {W : Type u_2} [inst : AddCommGroup V] [inst_1 : Module ℝ V] [inst_2 : TopologicalSpace V]
  [inst_3 : AddCommGroup W] [inst_4 : Module ℝ W] [inst_5 : TopologicalSpace W] {e : AddChar ℝ Circle}
  {L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ} {he : Continuous ⇑e} {hL : Continuous fun p => (L p.1) p.2} (w : W),
  BoundedContinuousFunction.char he hL (-w) = star (BoundedContinuousFunction.char he hL w)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey!_alter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] [inst_2 : Inhabited α] {k k' : α} {f : Option (β k) → Option (β k)},
  (t.alter k f).getKey! k' =
    if cmp k k' = Ordering.eq then if (f (t.get? k)).isSome = true then k else default else t.getKey! k'
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.iterate_injOn_Iio_minimalPeriod : ∀ {α : Type u_1} {f : α → α} {x : α}, Set.InjOn (fun x_1 => f^[x_1] x) (Set.Iio (Function.minimalPeriod f x))
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.argPartialEquiv_symm_apply : ↑Circle.argPartialEquiv.symm = ⇑Circle.exp
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  (m m_1 : Std.DHashMap.Raw α β) (e_m : m = m_1) (a : α) (h : a ∈ m), m.get a h = m_1.get a ⋯
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.whiskerRight_id_bimod : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C]
  [inst_3 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorLeft X)]
  [inst_4 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorRight X)]
  {X Y : CategoryTheory.Mon C} {M N : Bimod X Y} (f : M ⟶ N),
  Bimod.whiskerRight f (Bimod.regular Y) =
    CategoryTheory.CategoryStruct.comp M.rightUnitorBimod.hom
      (CategoryTheory.CategoryStruct.comp f N.rightUnitorBimod.inv)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_eq_some_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k k' : α}, t.getKey? k = some k' ↔ ∃ (h : k ∈ t), t.getKey k h = k'
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- Restrict a graph to the vertices in the set `s`, deleting all edges incident to vertices
outside the set. This is a wrapper around `SimpleGraph.comap`.  -/
SimpleGraph.induce : {V : Type u_1} → (s : Set V) → SimpleGraph V → SimpleGraph ↑s
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- The reflection of the circumcenter of a simplex in an edge, in
terms of `pointsWithCircumcenter`.  -/
Affine.Simplex.reflection_circumcenter_eq_affineCombination_of_pointsWithCircumcenter : ∀ {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 : ℕ} (s : Affine.Simplex ℝ P n) {i₁ i₂ : Fin (n + 1)},
  i₁ ≠ i₂ →
    (EuclideanGeometry.reflection (affineSpan ℝ (s.points '' {i₁, i₂}))) s.circumcenter =
      (Finset.affineCombination ℝ Finset.univ s.pointsWithCircumcenter)
        (Affine.Simplex.reflectionCircumcenterWeightsWithCircumcenter i₁ i₂)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.eventually_nhds_iff_ball : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {p : α → Prop},
  (∀ᶠ (y : α) in nhds x, p y) ↔ ∃ ε > 0, ∀ y ∈ Metric.ball x ε, p y
-- Init.Data.Array.Find
Array.find?_replicate_of_size_pos : ∀ {n : ℕ} {α : Type u_1} {p : α → Bool} {a : α},
  0 < n → Array.find? p (Array.replicate n a) = if p a = true then some a else none
-- Mathlib.Analysis.Normed.Group.CocompactMap
Filter.tendsto_cocompact_cocompact_of_norm : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] [ProperSpace E]
  {f : E → F},
  (∀ (ε : ℝ), ∃ r, ∀ (x : E), r < ‖x‖ → ε < ‖f x‖) → Filter.Tendsto f (Filter.cocompact E) (Filter.cocompact F)
-- Mathlib.Algebra.Group.UniqueProds.Basic
UniqueAdd.mono : ∀ {G : Type u_1} [inst : Add G] {A B : Finset G} {a0 b0 : G} {A' B' : Finset G},
  A ⊆ A' → B ⊆ B' → UniqueAdd A' B' a0 b0 → UniqueAdd A B a0 b0
-- Std.Http.Protocol.H1.Writer
/-- Running total of bytes across all `userData` chunks, maintained incrementally
to avoid an O(n) fold on every fixed-length write step.
 -/
Std.Http.Protocol.H1.Writer.userDataBytes : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Writer dir → ℕ
-- Mathlib.Data.Fintype.Card
Finset.card_eq_iff_eq_univ : ∀ {α : Type u_1} [inst : Fintype α] (s : Finset α), s.card = Fintype.card α ↔ s = Finset.univ
-- Mathlib.Algebra.Group.Submonoid.DistribMulAction
/-- The action by a submonoid is the action by the underlying monoid.  -/
Submonoid.mulDistribMulAction : {M : Type u_1} →
  {α : Type u_2} →
    [inst : Monoid M] → [inst_1 : Monoid α] → [MulDistribMulAction M α] → (S : Submonoid M) → MulDistribMulAction (↥S) α
-- Mathlib.Topology.MetricSpace.CoveringNumbers
/-- A finite `ε`-separated subset of a set `A` with maximal cardinality.
It is defined as the empty set if no such finite subset exists.  -/
Metric.maximalSeparatedSet : {X : Type u_1} → [PseudoEMetricSpace X] → NNReal → Set X → Set X
-- Mathlib.Order.Monotone.Defs
monotoneOn_const : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {c : β} {s : Set α}, MonotoneOn (fun x => c) s
-- Mathlib.Algebra.Quaternion
Quaternion.coe_natCast : ∀ {R : Type u_3} [inst : CommRing R] (n : ℕ), ↑↑n = ↑n
-- Lean.Compiler.IR.Basic
Lean.IR.IRType.isVoid : Lean.IR.IRType → Bool
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Mon.instCartesianMonoidalCategory : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] → CategoryTheory.CartesianMonoidalCategory (CategoryTheory.Mon C)
-- Mathlib.Algebra.Group.Submonoid.BigOperators
/-- Product of a multiset of elements in a submonoid of a `CommMonoid` is in the submonoid.  -/
Submonoid.multiset_prod_mem : ∀ {M : Type u_4} [inst : CommMonoid M] (S : Submonoid M) (m : Multiset M), (∀ a ∈ m, a ∈ S) → m.prod ∈ S
-- Init.Data.String.Lemmas.Basic
String.Slice.Pos.nextn_endPos : ∀ {n : ℕ} {s : String.Slice}, s.endPos.nextn n = s.endPos
-- Mathlib.Algebra.Group.End
Equiv.Perm.default_eq : ∀ {α : Type u_4}, default = 1
-- Mathlib.Analysis.Convex.StrictConvexSpace
sameRay_iff_norm_sub : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [StrictConvexSpace ℝ E] {x y : E},
  SameRay ℝ x y ↔ ‖x - y‖ = |‖x‖ - ‖y‖|
-- Mathlib.LinearAlgebra.Eigenspace.Basic
/-- If there exists a natural number `k` such that the kernel of `(f - μ • id) ^ k` is the
maximal generalized eigenspace, then this value is the least such `k`. If not, this value is not
meaningful.  -/
Module.End.maxUnifEigenspaceIndex : {R : Type v} →
  {M : Type w} → [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Module.End R M → R → ℕ
-- Mathlib.Algebra.Homology.HasNoLoop
ComplexShape.HasNoLoop.mk : ∀ {ι : Type u_1} {c : ComplexShape ι}, (∀ (i : ι), ¬c.Rel i i) → c.HasNoLoop
-- Mathlib.FieldTheory.Normal.Basic
/-- A quadratic extension is normal.
 -/
Algebra.IsQuadraticExtension.normal : ∀ (F : Type u_6) (K : Type u_7) [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K]
  [Algebra.IsQuadraticExtension F K], Normal F K
-- Mathlib.Topology.Bornology.Basic
/-- A space with a `Bornology` is a **bounded space** if `Set.univ : Set α` is bounded.  -/
BoundedSpace : (α : Type u_4) → [Bornology α] → Prop
-- Mathlib.Algebra.Order.Hom.Monoid
/-- `e.symm` is a left inverse of `e`, written as `e.symm (e y) = y`.  -/
OrderAddMonoidIso.symm_apply_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : Add β]
  (e : α ≃+o β) (x : α), e.symm (e x) = x
-- Mathlib.CategoryTheory.Sites.JointlySurjective
CategoryTheory.Types.mem_jointlySurjectivePrecoverage_iff : ∀ {X : Type u} {R : CategoryTheory.Presieve X},
  R ∈ CategoryTheory.Types.jointlySurjectivePrecoverage.coverings X ↔
    ∀ (x : X), ∃ Y g, R g ∧ x ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom g)
-- Mathlib.Geometry.Convex.ConvexSpace.AffineMap
Convexity.ConvexSpace.AffineMap.id_apply : ∀ {R : Type u_1} [inst : PartialOrder R] [inst_1 : Semiring R] [inst_2 : IsStrictOrderedRing R] (X : Type u_2)
  [inst_3 : Convexity.ConvexSpace R X] (a : X), (Convexity.ConvexSpace.AffineMap.id X) a = id a
-- Mathlib.Analysis.Analytic.Order
eventuallyConst_iff_analyticOrderAt_sub_eq_top : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜},
  Filter.EventuallyConst f (nhds z₀) ↔ analyticOrderAt (fun x => f x - f z₀) z₀ = ⊤
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_throwThe_apply_eq : ∀ {Pred : Type u_2} {EPred : Type u_3} {m : Type u → Type v} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {ε : Type u_1} {α : Type u}
  {post : α → Pred} {epost : EPred} [inst_4 : MonadExceptOf ε m] (err : ε),
  Std.Internal.Do.wp (throwThe ε err) post epost = Std.Internal.Do.wp (MonadExceptOf.throw err) post epost
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.le_of_transpose_le : ∀ {μ ν : YoungDiagram}, μ.transpose ≤ ν → μ ≤ ν.transpose
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.zero_apply : ∀ {A : Type u_2} {ι : Type u_3} {E : ι → Type u_4} (i : ι) [inst : (i : ι) → AddCommGroup (E i)], 0 i = 0
-- Mathlib.MeasureTheory.VectorMeasure.Integral
/-- `f : X → E` is said to be integrable with respect to `μ` and `B` if it is integrable with
respect to `(μ.transpose B).variation`.  -/
MeasureTheory.VectorMeasure.Integrable : {X : Type u_2} →
  {E : Type u_4} →
    {F : Type u_5} →
      {mX : MeasurableSpace X} →
        [NormedAddCommGroup E] → [inst : NormedAddCommGroup F] → MeasureTheory.VectorMeasure X F → (X → E) → Prop
-- Mathlib.GroupTheory.Coset.Basic
QuotientAddGroup.quotientEquivSelf.eq_1 : ∀ (α : Type u_1) [inst : AddGroup α],
  QuotientAddGroup.quotientEquivSelf α =
    { toFun := Quotient.lift id ⋯, invFun := QuotientAddGroup.mk, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Order.Hom.Basic
/-- A preorder which embeds into a preorder in which `(· > ·)` is well-founded
also has `(· > ·)` well-founded.  -/
OrderEmbedding.wellFoundedGT : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [WellFoundedGT β] (f : α ↪o β),
  WellFoundedGT α