mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk_eq_iff_leftFractionRel : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C}
  [inst_1 : W.HasLeftCalculusOfFractions] {X Y : C} (z₁ z₂ : W.LeftFraction X Y),
  CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk z₁ =
      CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk z₂ ↔
    CategoryTheory.MorphismProperty.LeftFractionRel z₁ z₂
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
/-- The morphism `Z ⟶ succ W Z`.  -/
CategoryTheory.OrthogonalReflection.toSucc : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (W : CategoryTheory.MorphismProperty C) →
      (Z : C) →
        [inst_1 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁] →
          [inst_2 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂] →
            [inst_3 : CategoryTheory.Limits.HasPushouts C] →
              [inst_4 :
                  CategoryTheory.Limits.HasMulticoequalizer
                    (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)] →
                Z ⟶ CategoryTheory.OrthogonalReflection.succ W Z
-- Mathlib.Topology.MetricSpace.HolderNorm
MemHolder.holderWith : ∀ {X : Type u_1} {Y : Type u_2} [inst : MetricSpace X] [inst_1 : EMetricSpace Y] {r : NNReal} {f : X → Y},
  MemHolder r f → HolderWith (nnHolderNorm r f) r f
-- Init.Data.Iterators.ToIterator
/-- Creates a monadic `ToIterator` instance.  -/
Std.ToIterator.ofM : {γ : Type u_1} → {m : Type w → Type u_2} → {β : Type w} → (α : Type w) → (γ → Std.IterM m β) → Std.ToIterator γ m α β
-- Mathlib.Algebra.Divisibility.Units
/-- In a commutative monoid, an element `a` divides an element `b` iff all
left associates of `a` divide `b`.  -/
Units.mul_left_dvd : ∀ {α : Type u_1} [inst : CommMonoid α] {a b : α} {u : αˣ}, ↑u * a ∣ b ↔ a ∣ b
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
CategoryTheory.Limits.PreservesLimitPair.iso_inv_fst_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) (X Y : C) [inst_2 : CategoryTheory.Limits.HasBinaryProduct X Y]
  [inst_3 : CategoryTheory.Limits.HasBinaryProduct (G.obj X) (G.obj Y)]
  [inst_4 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair X Y) G] {Z : D} (h : G.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesLimitPair.iso G X Y).inv
      (CategoryTheory.CategoryStruct.comp (G.map CategoryTheory.Limits.prod.fst) h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h
-- Lean.Meta.Sym.Arith.MonadCanon
Lean.Meta.Sym.Arith.MonadCanon : (Type → Type) → Type
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
cpow_eq_nhds : ∀ {a b : ℂ}, a ≠ 0 → (fun x => x ^ b) =ᶠ[nhds a] fun x => Complex.exp (Complex.log x * b)
-- Mathlib.Topology.Algebra.Group.Matrix
_private.Mathlib.Topology.Algebra.Group.Matrix.0.Matrix.SpecialLinearGroup.termSL : Lean.ParserDescr
-- Init.Data.Option.Lemmas
Option.some_lt_some : ∀ {α : Type u_1} [inst : LT α] {a b : α}, some a < some b ↔ a < b
-- Lean.Meta.Tactic.Grind.Types
/-- Returns the root enode in the equivalence class of `e` if it is in an equivalence class.  -/
Lean.Meta.Grind.getRootENode? : Lean.Expr → Lean.Meta.Grind.GoalM (Option Lean.Meta.Grind.ENode)
-- Mathlib.Topology.Algebra.Module.FiniteDimension
/-- **Alias** of `ContinuousLinearMap.exists_rightInverse_of_surjective`. -/
ContinuousLinearMap.exists_right_inverse_of_surjective : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
  [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [IsTopologicalAddGroup E] [inst_5 : Module 𝕜 E]
  [ContinuousSMul 𝕜 E] [inst_7 : AddCommGroup F] [inst_8 : TopologicalSpace F] [IsTopologicalAddGroup F]
  [inst_10 : Module 𝕜 F] [ContinuousSMul 𝕜 F] [T2Space F] [FiniteDimensional 𝕜 F] (f : E →L[𝕜] F),
  (↑f).range = ⊤ → ∃ g, f ∘SL g = ContinuousLinearMap.id 𝕜 F
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
/-- Given `X : C`, this is a cofibrant object `X'` equipped with a
trivial fibration `X' ⟶ X` (see `HoCat.pResolutionObj`).  -/
HomotopicalAlgebra.CofibrantObject.HoCat.resolutionObj : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → [HomotopicalAlgebra.ModelCategory C] → C → C
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.Completion.coe_toCompletion : ∀ {K : Type u_1} [inst : Field K] (v : NumberField.InfinitePlace K) (x : WithAbs ↑v),
  { toCompletion := ↑x }.toCompletion = ↑x
-- Mathlib.Data.Nat.Digits.Div
/-- **Divisibility by 3 Rule**  -/
Nat.three_dvd_iff : ∀ (n : ℕ), 3 ∣ n ↔ 3 ∣ (Nat.digits 10 n).sum
-- Mathlib.Algebra.GroupWithZero.Divisibility
/-- **Alias** of `dvd_antisymm'`. -/
Dvd.dvd.antisymm' : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [IsCancelMulZero α] {a b : α} [Subsingleton αˣ], a ∣ b → b ∣ a → b = a
-- Mathlib.Logic.Function.Basic
Function.update_eq_iff : ∀ {α : Sort u} {β : α → Sort v} [inst : DecidableEq α] {a : α} {b : β a} {f g : (a : α) → β a},
  Function.update f a b = g ↔ b = g a ∧ ∀ (x : α), x ≠ a → f x = g x
-- Mathlib.Topology.Homeomorph.Defs
/-- Inverse of a homeomorphism.  -/
Homeomorph.symm : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → X ≃ₜ Y → Y ≃ₜ X
-- Mathlib.Analysis.CStarAlgebra.Basic
CStarRing.nnnorm_star_mul_self : ∀ {E : Type u_2} [inst : NonUnitalNormedRing E] [inst_1 : StarRing E] [CStarRing E] {x : E}, ‖star x * x‖₊ = ‖x‖₊ * ‖x‖₊
-- Init.Data.Option.Lemmas
Option.isSome_filter : ∀ {α : Type u_1} {p : α → Bool} {o : Option α}, (Option.filter p o).isSome = Option.any p o
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
/-- The singleton operation as a `ZeroHom`.  -/
Set.singletonZeroHom : {α : Type u_2} → [inst : Zero α] → ZeroHom α (Set α)
-- Mathlib.RingTheory.Localization.FractionRing
/-- A `CommRing` `K` which is the localization of an integral domain `R` at `R - {0}` is a field.
See note [reducible non-instances].  -/
IsFractionRing.toField : (A : Type u_4) →
  [inst : CommRing A] →
    {K : Type u_5} → [inst_1 : CommRing K] → [inst_2 : Algebra A K] → [IsFractionRing A K] → [IsDomain A] → Field K
-- Mathlib.CategoryTheory.Adjunction.Parametrized
CategoryTheory.ParametrizedAdjunction.homEquiv_symm_naturality_one_assoc : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)}
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} (adj₂ : F ⊣₂ G) {X₁ Y₁ : C₁} {X₂ : C₂} {X₃ : C₃}
  (f₁ : X₁ ⟶ Y₁) (g : X₂ ⟶ (G.obj (Opposite.op Y₁)).obj X₃) {Z : C₃} (h : X₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (adj₂.homEquiv.symm (CategoryTheory.CategoryStruct.comp g ((G.map f₁.op).app X₃)))
      h =
    CategoryTheory.CategoryStruct.comp ((F.map f₁).app X₂) (CategoryTheory.CategoryStruct.comp (adj₂.homEquiv.symm g) h)
-- Mathlib.Algebra.Module.LinearMap.Basic
LinearMap.mulLeft_mul : ∀ (R : Type u_6) (A : Type u_7) [inst : Semiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A] (a b : A), LinearMap.mulLeft R (a * b) = LinearMap.mulLeft R a ∘ₗ LinearMap.mulLeft R b
-- Mathlib.Algebra.Group.Pointwise.Set.BigOperators
/-- **Alias** of `Set.finsetSum_subset_finsetSum`.

---

An n-ary version of `Set.add_subset_add`.  -/
Set.finset_sum_subset_finset_sum : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] (t : Finset ι) (f₁ f₂ : ι → Set α),
  (∀ i ∈ t, f₁ i ⊆ f₂ i) → ∑ i ∈ t, f₁ i ⊆ ∑ i ∈ t, f₂ i
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.minD.congr_simp : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtTreeSet α cmp),
  t = t_1 → ∀ (fallback fallback_1 : α), fallback = fallback_1 → t.minD fallback = t_1.minD fallback_1
-- Mathlib.MeasureTheory.Measure.Regular
/-- If `μ` is a regular measure, then any open set can be approximated by a compact subset.  -/
IsOpen.exists_lt_isCompact : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α] [μ.Regular]
  ⦃U : Set α⦄, IsOpen U → ∀ {r : ENNReal}, r < μ U → ∃ K ⊆ U, IsCompact K ∧ r < μ K
-- Mathlib.Data.Set.Lattice.Image
Set.image2_eq_seq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (s : Set α) (t : Set β),
  Set.image2 f s t = (f '' s).seq t
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.fullyFaithfulForget₂Mon.eq_1 : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.Grp.fullyFaithfulForget₂Mon C = CategoryTheory.fullyFaithfulInducedFunctor CategoryTheory.Grp.toMon
-- Mathlib.Analysis.CStarAlgebra.Multiplier
/-- The canonical map `DoubleCentralizer.toProdMulOpposite` as a ring homomorphism.  -/
DoubleCentralizer.toProdMulOppositeHom : {𝕜 : Type u_1} →
  {A : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NonUnitalNormedRing A] →
        [inst_2 : NormedSpace 𝕜 A] →
          [inst_3 : SMulCommClass 𝕜 A A] →
            [inst_4 : IsScalarTower 𝕜 A A] → DoubleCentralizer 𝕜 A →+* (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ
-- Lean.Meta.SynthInstance
_private.Lean.Meta.SynthInstance.0.Lean.Meta.PreprocessResult.mk.inj : ∀ {type cacheKeyType : Lean.Expr} {kind : Lean.Meta.PreprocessKind✝} {type_1 cacheKeyType_1 : Lean.Expr}
  {kind_1 : Lean.Meta.PreprocessKind✝},
  { type := type, cacheKeyType := cacheKeyType, kind := kind } =
      { type := type_1, cacheKeyType := cacheKeyType_1, kind := kind_1 } →
    type = type_1 ∧ cacheKeyType = cacheKeyType_1 ∧ kind = kind_1
-- Init.Data.SInt.Lemmas
Int32.ofInt_sub : ∀ (a b : ℤ), Int32.ofInt (a - b) = Int32.ofInt a - Int32.ofInt b
-- Mathlib.Algebra.Order.Field.Basic
half_le_self_iff : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a : α} [IsStrictOrderedRing α],
  a / 2 ≤ a ↔ 0 ≤ a
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
ContinuousLinearEquiv.continuousAlternatingMapCongrRight_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_4} {G : Type u_5} {ι : Type u_6} [inst : NormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F]
  [inst_5 : Module 𝕜 F] [inst_6 : TopologicalSpace F] [inst_7 : IsTopologicalAddGroup F]
  [inst_8 : ContinuousConstSMul 𝕜 F] [inst_9 : AddCommGroup G] [inst_10 : Module 𝕜 G] [inst_11 : TopologicalSpace G]
  [inst_12 : IsTopologicalAddGroup G] [inst_13 : ContinuousConstSMul 𝕜 G] (g : F ≃L[𝕜] G) (a : E [⋀^ι]→L[𝕜] F),
  g.continuousAlternatingMapCongrRight a = (↑g).compContinuousAlternatingMap a
-- Mathlib.MeasureTheory.Measure.Restrict
indicator_ae_eq_restrict : ∀ {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {f : α → β}
  [inst_1 : Zero β], MeasurableSet s → s.indicator f =ᵐ[μ.restrict s] f
-- Init.Data.List.Find
_private.Init.Data.List.Find.0.List.findIdx?_go_eq : ∀ {α : Type u_1} {p : α → Bool} {xs : List α} {i : ℕ},
  List.findIdx?.go p xs (i + 1) = Option.map (fun k => k + (i + 1)) (List.findIdx?.go p xs 0)
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.t_fac : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (self : CategoryTheory.GlueData C) (i j k : self.J),
  CategoryTheory.CategoryStruct.comp (self.t' i j k) (CategoryTheory.Limits.pullback.snd (self.f j k) (self.f j i)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (self.f i j) (self.f i k)) (self.t i j)
-- Mathlib.Topology.MetricSpace.UniformConvergence
UniformFun.instMetricSpaceOfBoundedSpace : {α : Type u_1} → {β : Type u_4} → [inst : MetricSpace β] → [BoundedSpace β] → MetricSpace (UniformFun α β)
-- Mathlib.Combinatorics.Additive.CovBySMul
/-- Predicate for a set `A` to be covered by at most `K` cosets of another set `B` under the action
by the monoid `M`.  -/
CovBySMul : (M : Type u_1) → {X : Type u_3} → [inst : Monoid M] → [MulAction M X] → ℝ → Set X → Set X → Prop
-- Mathlib.Topology.Compactness.LocallyCompact
instWeaklyLocallyCompactSpaceForallOfFinite : ∀ {ι : Type u_4} [Finite ι] {X : ι → Type u_5} [inst : (i : ι) → TopologicalSpace (X i)]
  [∀ (i : ι), WeaklyLocallyCompactSpace (X i)], WeaklyLocallyCompactSpace ((i : ι) → X i)
-- Init.Data.Int.Order
Int.neg_le_of_neg_le : ∀ {a b : ℤ}, -a ≤ b → -b ≤ a
-- Mathlib.Analysis.Meromorphic.Order
/-- Variant of `codiscrete_setOfPred_meromorphicOrderAt_eq_zero_or_top`: The set where a meromorphic
function has zero or infinite order is codiscrete within its domain of meromorphicity.
 -/
MeromorphicOn.codiscreteWithin_setOfPred_meromorphicOrderAt_eq_zero_or_top : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜},
  MeromorphicOn f U →
    (∀ u ∈ U, meromorphicOrderAt f u ≠ ⊤) →
      {u | u ∈ U ∧ (meromorphicOrderAt f u = 0 ∨ meromorphicOrderAt f u = ⊤)} ∈ Filter.codiscreteWithin U
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.pointReflection_midpoint_left : ∀ {V : Type u_2} {P : Type u_10} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] [inst_3 : NormedSpace ℝ V] (x y : P),
  (AffineIsometryEquiv.pointReflection ℝ (midpoint ℝ x y)) x = y
-- Mathlib.RingTheory.GradedAlgebra.Basic
DirectSum.decompose_mul_add_right : ∀ {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [inst : DecidableEq ι] [inst_1 : Semiring A] [inst_2 : SetLike σ A]
  [inst_3 : AddSubmonoidClass σ A] (𝒜 : ι → σ) {i j : ι} [inst_4 : AddRightCancelMonoid ι] [inst_5 : GradedRing 𝒜]
  {a : A} (b : ↥(𝒜 j)),
  ((DirectSum.decompose 𝒜) (a * ↑b)) (i + j) = GradedMonoid.GMul.mul (((DirectSum.decompose 𝒜) a) i) b
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.Subcomplex.mk.inj : ∀ {X : Type u_1} {t : TopologicalSpace X} {C D : Set X} {inst : Topology.RelCWComplex C D} {carrier : Set X}
  {I : (n : ℕ) → Set (Topology.RelCWComplex.cell C n)} {closed' : IsClosed carrier}
  {union' : D ∪ ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j = carrier} {carrier_1 : Set X}
  {I_1 : (n : ℕ) → Set (Topology.RelCWComplex.cell C n)} {closed'_1 : IsClosed carrier_1}
  {union'_1 : D ∪ ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j = carrier_1},
  { carrier := carrier, I := I, closed' := closed', union' := union' } =
      { carrier := carrier_1, I := I_1, closed' := closed'_1, union' := union'_1 } →
    carrier = carrier_1 ∧ I = I_1
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
MeasureTheory.preVariation.eq_1 : ∀ {X : Type u_1} [inst : MeasurableSpace X] (f : Set X → ENNReal) (hf : MeasureTheory.IsSigmaSubadditiveSetFun f)
  (hf' : f ∅ = 0), MeasureTheory.preVariation f hf hf' = (MeasureTheory.ennrealPreVariation f hf hf').ennrealToMeasure
-- Init.Data.Bool
Bool.forall_bool' : ∀ {p : Bool → Prop} (b : Bool), (∀ (x : Bool), p x) ↔ p b ∧ p !b
-- Mathlib.SetTheory.Lists
Finsets.instDecidableEq : {α : Type u_1} → [DecidableEq α] → DecidableEq (Finsets α)
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.snd.eq_1 : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T)
  (L : CategoryTheory.Functor A T),
  CategoryTheory.Comma.snd R L = { obj := fun X => X.right, map := fun {Y X} f => f.right, map_id := ⋯, map_comp := ⋯ }
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.top_injective_iff : ∀ {M : Type u_1} {N : Type u_2} [inst : CommMonoid M] [inst_1 : CommMonoid N] (f : ⊤.LocalizationMap N),
  Function.Injective ⇑f ↔ IsCancelMul M
-- Mathlib.Data.Set.Card
Set.ncard_image_of_injective : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} (s : Set α), Function.Injective f → (f '' s).ncard = s.ncard
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
/-- The natural isomorphism `t.eTruncGE.obj b ≅ t.eTruncGE.obj a ⋙ t.eTruncGE.obj b`
when `a` and `b` in `EInt` satisfy `a ≤ b`.  -/
CategoryTheory.Triangulated.TStructure.eTruncGEIsoGEGE : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              (t : CategoryTheory.Triangulated.TStructure C) →
                [CategoryTheory.IsTriangulated C] →
                  (a b : EInt) → a ≤ b → (t.eTruncGE.obj b ≅ (t.eTruncGE.obj a).comp (t.eTruncGE.obj b))
-- Mathlib.RingTheory.DedekindDomain.Factorization
FractionalIdeal.divMod_zero_right : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDedekindDomain R] {I J : FractionalIdeal (nonZeroDivisors R) K},
  I.divMod J 0 = 0
-- Mathlib.Order.Monotone.Basic
strictAntiOn_toDual_comp_iff : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  StrictAntiOn (⇑OrderDual.toDual ∘ f) s ↔ StrictMonoOn f s
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Broadcast.mk : {α : Type} → Std.Bounded✝ α → Std.Broadcast α
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.getEntry : {α : Type u} →
  {β : α → Type v} →
    [inst : BEq α] →
      [inst_1 : Hashable α] → (m : Std.DHashMap.Internal.Raw₀ α β) → (a : α) → m.contains a = true → (a : α) × β a
-- Mathlib.Order.UpperLower.Basic
IsLowerSet.bot_notMem : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} [inst_1 : OrderBot α], IsLowerSet s → (⊥ ∉ s ↔ s = ∅)
-- Std.Http.Data.URI.Basic
Std.Http.URI.instInhabitedHost.default : Std.Http.URI.Host
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.volume_real_Ioc_of_le : ∀ {a b : ℝ}, a ≤ b → MeasureTheory.volume.real (Set.Ioc a b) = b - a
-- Mathlib.RingTheory.DedekindDomain.Ideal.Basic
FractionalIdeal.instPosMulReflectLENonZeroDivisors : ∀ {A : Type u_2} (K : Type u_3) [inst : CommRing A] [inst_1 : Field K] [IsDedekindDomain A] [inst_3 : Algebra A K]
  [IsFractionRing A K], PosMulReflectLE (FractionalIdeal (nonZeroDivisors A) K)
-- Mathlib.CategoryTheory.Galois.Full
/-- The by a fiber functor `F : C ⥤ FintypeCat` induced functor `functorToAction F` to
finite `Aut F`-sets is full.  -/
CategoryTheory.PreGaloisCategory.functorToAction_full : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F],
  (CategoryTheory.PreGaloisCategory.functorToAction F).Full
-- Mathlib.Topology.EMetricSpace.PairReduction
PairReduction.pairSetSeq.eq_1 : ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] [inst_1 : DecidableEq T] (J : Finset T) (a c : ENNReal) (n : ℕ),
  PairReduction.pairSetSeq J a c n =
    if hJ : J.Nonempty then
      {(PairReduction.logSizeBallSeq J hJ a c n).point}.product ((PairReduction.logSizeBallSeq J hJ a c n).ball c)
    else ∅
-- Mathlib.Algebra.Homology.AlternatingConst
ChainComplex.alternatingConst_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (X : C), ChainComplex.alternatingConst.obj X = HomologicalComplex.alternatingConst X ⋯ ⋯ ⋯
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- If `t.unop : Cocone F` is a colimit cocone, then `t : Cone F.op` is a limit cone.  -/
CategoryTheory.Limits.isLimitOfUnop : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor J C} →
          {t : CategoryTheory.Limits.Cone F.op} →
            CategoryTheory.Limits.IsColimit t.unop → CategoryTheory.Limits.IsLimit t
-- Lean.Meta.MatchUtil
Lean.Meta.testHelper : Lean.Expr → (Lean.Expr → Lean.MetaM Bool) → Lean.MetaM Bool
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- A side of a right-angled triangle divided by the tangent of the opposite angle equals the
adjacent side.  -/
InnerProductGeometry.norm_div_tan_angle_add_of_inner_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  inner ℝ x y = 0 → x = 0 ∨ y ≠ 0 → ‖y‖ / Real.tan (InnerProductGeometry.angle x (x + y)) = ‖x‖
-- Mathlib.RingTheory.Trace.Quotient
IsLocalization.AtPrime.equivQuotientMapMaximalIdeal.eq_1 : ∀ (S : Type u_6) {R : Type u_7} [inst : CommRing R] (p : Ideal R) [inst_1 : p.IsMaximal] (Rₚ : Type u_8)
  [inst_2 : CommRing Rₚ] [inst_3 : Algebra R Rₚ] [inst_4 : IsLocalization.AtPrime Rₚ p] [inst_5 : IsLocalRing Rₚ]
  (Sₚ : Type u_9) [inst_6 : CommRing S] [inst_7 : Algebra R S] [inst_8 : CommRing Sₚ] [inst_9 : Algebra S Sₚ]
  [inst_10 : Algebra R Sₚ] [inst_11 : Algebra Rₚ Sₚ]
  [inst_12 : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ] [inst_13 : IsScalarTower R S Sₚ]
  [inst_14 : IsScalarTower R Rₚ Sₚ],
  IsLocalization.AtPrime.equivQuotientMapMaximalIdeal S p Rₚ Sₚ =
    (Ideal.quotEquivOfEq ⋯).trans (RingHom.quotientKerEquivOfSurjective ⋯)
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.coord.eq_1 : ∀ {n : Type u} (S : AlgebraicGeometry.Scheme) (i : n),
  AlgebraicGeometry.AffineSpace.coord S i =
    (AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv n) (AlgebraicGeometry.AffineSpace.toSpecMvPoly n S) i
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.Const.minEntry.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : (x : Std.DTreeMap.Internal.Impl α fun x => β) → x.isEmpty = false → Sort u_3)
  (size : ℕ) (k : α) (v : β) (r : Std.DTreeMap.Internal.Impl α fun x => β)
  (x : (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r).isEmpty = false)
  (h_1 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (r : Std.DTreeMap.Internal.Impl α fun x => β) →
            (x : (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r).isEmpty = false) →
              motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l : Std.DTreeMap.Internal.Impl α fun x => β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α fun x => β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r →
                      (r_1 : Std.DTreeMap.Internal.Impl α fun x => β) →
                        (h :
                            (Std.DTreeMap.Internal.Impl.inner size k v
                                  (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) r_1).isEmpty =
                              false) →
                          motive
                            (Std.DTreeMap.Internal.Impl.inner size k v
                              (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) r_1)
                            h),
  (match Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x with
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x => h_1 size k v r x
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) r_1,
      h_3 => h_2 size k v l size_1 k_1 v_1 l_1 r h r_1 h_3) =
    h_1 size k v r x
-- Lean.Data.Lsp.Basic
Lean.Lsp.TextDocumentIdentifier.mk.inj : ∀ {uri uri_1 : Lean.Lsp.DocumentUri}, { uri := uri } = { uri := uri_1 } → uri = uri_1
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
AddOpposite.instPseudoMetricSpace : {α : Type u_1} → [PseudoMetricSpace α] → PseudoMetricSpace αᵃᵒᵖ
-- Init.Tactics
Lean.Parser.Tactic.LibrarySearchConfig.mk : Bool → Bool → Bool → Bool → Lean.Parser.Tactic.LibrarySearchConfig
-- Lean.Parser.Term
/-- A shorthand for `panic! "unreachable code has been reached"`.  -/
Lean.Parser.Term.unreachable : Lean.Parser.Parser