mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.TensorProduct.MvPolynomial
MvPolynomial.instIsPushout : ∀ {R : Type u} [inst : CommSemiring R] {σ : Type u_1} {S : Type u_3} [inst_1 : CommSemiring S] [inst_2 : Algebra R S],
  Algebra.IsPushout R S (MvPolynomial σ R) (MvPolynomial σ S)
-- Mathlib.Geometry.Convex.Cone.Face.Basic
PointedCone.IsFaceOf.mem_of_smul_add_smul_mem_left : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {C F : PointedCone R M} {x y : M} {a b : R},
  F.IsFaceOf C → x ∈ C → y ∈ C → 0 < a → 0 < b → a • x + b • y ∈ F → x ∈ F
-- Aesop.Rule
Aesop.UnsafeRuleInfo.mk.injEq : ∀ (successProbability successProbability_1 : Aesop.Percent),
  ({ successProbability := successProbability } = { successProbability := successProbability_1 }) =
    (successProbability = successProbability_1)
-- Mathlib.Data.Complex.Basic
Complex.ofReal_mul' : ∀ (r : ℝ) (z : ℂ), ↑r * z = { re := r * z.re, im := r * z.im }
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.mk_eq_add_smul_omega : ∀ {R : Type u_2} {a b : R} [inst : CommSemiring R] (x y : R),
  { re := x, im := y } = (algebraMap R (QuadraticAlgebra R a b)) x + y • QuadraticAlgebra.omega
-- Mathlib.Data.QPF.Multivariate.Constructions.Fix
MvQPF.WEquiv.below.ind : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n}
  {motive : (a a_1 : (MvQPF.P F).W α) → MvQPF.WEquiv a a_1 → Prop} (a : (MvQPF.P F).A)
  (f' : ((MvQPF.P F).drop.B a).Arrow α) (f₀ f₁ : (MvQPF.P F).last.B a → (MvQPF.P F).W α)
  (a_1 : ∀ (x : (MvQPF.P F).last.B a), MvQPF.WEquiv (f₀ x) (f₁ x)),
  (∀ (x : (MvQPF.P F).last.B a), MvQPF.WEquiv.below ⋯) →
    (∀ (x : (MvQPF.P F).last.B a), motive (f₀ x) (f₁ x) ⋯) → MvQPF.WEquiv.below ⋯
-- Mathlib.Analysis.SpecificLimits.Basic
tsum_geometric_two' : ∀ (a : ℝ), ∑' (n : ℕ), a / 2 / 2 ^ n = a
-- Mathlib.SetTheory.Ordinal.Basic
Cardinal.ord_zero : Cardinal.ord 0 = 0
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.instMonoidalCategoryStruct.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.Grp.instMonoidalCategoryStruct =
    {
      tensorObj := fun G H =>
        { X := CategoryTheory.MonoidalCategoryStruct.tensorObj G.X H.X,
          grp := CategoryTheory.GrpObj.tensorObj.instTensorObj },
      whiskerLeft := fun G x x_1 f =>
        CategoryTheory.Grp.homMk' (CategoryTheory.MonoidalCategoryStruct.whiskerLeft G.toMon f.hom),
      whiskerRight := fun {X₁ X₂} f G =>
        CategoryTheory.Grp.homMk' (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom G.toMon),
      tensorHom := fun {X₁ Y₁ X₂ Y₂} f g =>
        CategoryTheory.Grp.homMk' (CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom g.hom),
      tensorUnit :=
        { X := CategoryTheory.MonoidalCategoryStruct.tensorUnit C, grp := CategoryTheory.GrpObj.instTensorUnit },
      associator := fun X Y Z =>
        (CategoryTheory.Grp.fullyFaithfulForget₂Mon C).preimageIso
          (CategoryTheory.MonoidalCategoryStruct.associator X.toMon Y.toMon Z.toMon),
      leftUnitor := fun G =>
        (CategoryTheory.Grp.fullyFaithfulForget₂Mon C).preimageIso
          (CategoryTheory.MonoidalCategoryStruct.leftUnitor G.toMon),
      rightUnitor := fun G =>
        (CategoryTheory.Grp.fullyFaithfulForget₂Mon C).preimageIso
          (CategoryTheory.MonoidalCategoryStruct.rightUnitor G.toMon) }
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonVersionedTextDocumentIdentifier.fromJson : Lean.Json → Except String Lean.Lsp.VersionedTextDocumentIdentifier
-- Lean.Declaration
Lean.instReprDefinitionSafety : Repr Lean.DefinitionSafety
-- Mathlib.Topology.Algebra.GroupWithZero
nhds_translation_mul_inv₀ : ∀ {G₀ : Type u_3} [inst : TopologicalSpace G₀] [inst_1 : GroupWithZero G₀] [SeparatelyContinuousMul G₀] {a : G₀},
  a ≠ 0 → Filter.comap (fun x => x * a⁻¹) (nhds 1) = nhds a
-- Lean.DocString.Extension
Lean.VersoModuleDocs.isEmpty : Lean.VersoModuleDocs → Bool
-- Mathlib.Data.Set.Card.Arithmetic
Set.Finite.encard_biUnion_le : ∀ {α : Type u_1} {ι : Type u_2} {t : Set ι},
  t.Finite → ∀ (s : ι → Set α), (⋃ i ∈ t, s i).encard ≤ ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard
-- Mathlib.RingTheory.Coalgebra.Basic
Pi.counit_single : ∀ {R : Type u_1} {n : Type u_2} [inst : CommSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {A : n → Type u_3}
  [inst_3 : (i : n) → AddCommMonoid (A i)] [inst_4 : (i : n) → Module R (A i)]
  [inst_5 : (i : n) → CoalgebraStruct R (A i)] (i : n) (a : A i),
  CoalgebraStruct.counit (Pi.single i a) = CoalgebraStruct.counit a
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.prod_add_prod_comm : ∀ {α : Type u_2} {β : Type u_3} [inst : Add α] [inst_1 : Add β] (s₁ s₂ : Set α) (t₁ t₂ : Set β),
  s₁ ×ˢ t₁ + s₂ ×ˢ t₂ = (s₁ + s₂) ×ˢ (t₁ + t₂)
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.instIsLeftAdjointModuleCatForget₂ContinuousLinearMapIdCarrierLinearMap : ∀ (R : Type u) [inst : Ring R] [inst_1 : TopologicalSpace R],
  (CategoryTheory.forget₂ (TopModuleCat R) (ModuleCat R)).IsLeftAdjoint
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
SpectrumRestricts.compactSpace : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} [inst : Semifield R] [inst_1 : Semifield S] [inst_2 : Ring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A]
  [inst_7 : TopologicalSpace R] [inst_8 : TopologicalSpace S] {a : A} (f : C(S, R)),
  SpectrumRestricts a ⇑f → ∀ [h_cpct : CompactSpace ↑(spectrum S a)], CompactSpace ↑(spectrum R a)
-- Mathlib.Order.Filter.Extr
IsMinFilter.min : ∀ {α : Type u} {β : Type v} [inst : LinearOrder β] {f g : α → β} {a : α} {l : Filter α},
  IsMinFilter f l a → IsMinFilter g l a → IsMinFilter (fun x => min (f x) (g x)) l a
-- Mathlib.Topology.LocallyFinite
Equiv.locallyFinite_comp_iff : ∀ {ι : Type u_1} {ι' : Type u_2} {X : Type u_4} [inst : TopologicalSpace X] {f : ι → Set X} (e : ι' ≃ ι),
  LocallyFinite (f ∘ ⇑e) ↔ LocallyFinite f
-- Lean.Parser.Term
Lean.Parser.Term.num.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.GroupTheory.Commutator.Basic
AddSubgroup.addCommutator_eq_bot_iff_le_centralizer : ∀ {G : Type u_1} [inst : AddGroup G] {H₁ H₂ : AddSubgroup G}, ⁅H₁, H₂⁆ = ⊥ ↔ H₁ ≤ AddSubgroup.centralizer ↑H₂
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.left_comp_retraction : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : C} (f g : A ⟶ B)
  [inst_1 : CategoryTheory.IsCoreflexivePair f g],
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.commonRetraction f g) = CategoryTheory.CategoryStruct.id A
-- Mathlib.CategoryTheory.Localization.HomEquiv
CategoryTheory.LocalizerMorphism.homMap_comp : ∀ {C₁ : Type u_2} {C₂ : Type u_3} {D₁ : Type u_5} {D₂ : Type u_6} [inst : CategoryTheory.Category.{v_2, u_2} C₁]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} C₂] [inst_2 : CategoryTheory.Category.{v_5, u_5} D₁]
  [inst_3 : CategoryTheory.Category.{v_6, u_6} D₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
  (L₁ : CategoryTheory.Functor C₁ D₁) [inst_4 : L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂)
  [inst_5 : L₂.IsLocalization W₂] {X Y Z : C₁} (f : L₁.obj X ⟶ L₁.obj Y) (g : L₁.obj Y ⟶ L₁.obj Z),
  Φ.homMap L₁ L₂ (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (Φ.homMap L₁ L₂ f) (Φ.homMap L₁ L₂ g)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.ofHom_v : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) (p : ℤ), (CochainComplex.HomComplex.Cochain.ofHom φ).v p p ⋯ = φ.f p
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.EmbeddedG2.mem_span_of_mem_allRoots : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N)
  [inst_5 : P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R] {x : M},
  x ∈ RootPairing.EmbeddedG2.allRoots P →
    x ∈ Submodule.span ℤ {RootPairing.EmbeddedG2.longRoot P, RootPairing.EmbeddedG2.shortRoot P}
-- Mathlib.RingTheory.Etale.Basic
/-- Étale is stable under composition.  -/
Algebra.Etale.comp : ∀ (R : Type u) (A : Type v) (B : Type u_1) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [inst_5 : Algebra A B] [IsScalarTower R A B] [Algebra.Etale R A]
  [Algebra.Etale A B], Algebra.Etale R B
-- Mathlib.Geometry.Euclidean.Basic
/-- Distances `r₁` `r₂` of `p` from two different points `c₁` `c₂` determine at
most two points `p₁` `p₂` in two-dimensional space (two circles intersect in at
most two points).  -/
EuclideanGeometry.eq_of_dist_eq_of_dist_eq_of_finrank_eq_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [NormedAddTorsor V P] [FiniteDimensional ℝ V],
  Module.finrank ℝ V = 2 →
    ∀ {c₁ c₂ p₁ p₂ p : P} {r₁ r₂ : ℝ},
      c₁ ≠ c₂ →
        p₁ ≠ p₂ →
          dist p₁ c₁ = r₁ →
            dist p₂ c₁ = r₁ → dist p c₁ = r₁ → dist p₁ c₂ = r₂ → dist p₂ c₂ = r₂ → dist p c₂ = r₂ → p = p₁ ∨ p = p₂
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.smul_eq_C_mul : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} (a : R), a • p = Polynomial.C a * p
-- Init.Data.List.Nat.Range
List.fst_mem_of_mem_zipIdx : ∀ {α : Type u_1} {x : α × ℕ} {l : List α} {k : ℕ}, x ∈ l.zipIdx k → x.1 ∈ l
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.liftIoc_zero_continuous : ∀ {𝕜 : Type u_1} {B : Type u_2} [inst : AddCommGroup 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜] {p : 𝕜}
  [hp : Fact (0 < p)] [inst_3 : Archimedean 𝕜] [inst_4 : TopologicalSpace 𝕜] [OrderTopology 𝕜]
  [inst_6 : TopologicalSpace B] {f : 𝕜 → B},
  f 0 = f p → ContinuousOn f (Set.Icc 0 p) → Continuous (AddCircle.liftIoc p 0 f)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- `closure` forms a Galois insertion with the coercion to set.  -/
Subsemiring.gi : (R : Type u) → [inst : NonAssocSemiring R] → GaloisInsertion Subsemiring.closure SetLike.coe
-- Init.Data.List.Attach
List.mem_attach : ∀ {α : Type u_1} (l : List α) (x : { x // x ∈ l }), x ∈ l.attach
-- Mathlib.Analysis.Convex.Side
AffineSubspace.sOppSide_iff_exists_left : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y p₁ : P},
  p₁ ∈ s → (s.SOppSide x y ↔ x ∉ s ∧ y ∉ s ∧ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y))
-- Mathlib.Analysis.ODE.PicardLindelof
ODE.FunSpace.mk.congr_simp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {r L : NNReal}
  (toFun toFun_1 : ↑(Set.Icc tmin tmax) → E) (e_toFun : toFun = toFun_1) (lipschitzWith : LipschitzWith L toFun)
  (mem_closedBall₀ : toFun t₀ ∈ Metric.closedBall x₀ ↑r),
  { toFun := toFun, lipschitzWith := lipschitzWith, mem_closedBall₀ := mem_closedBall₀ } =
    { toFun := toFun_1, lipschitzWith := ⋯, mem_closedBall₀ := ⋯ }
-- Mathlib.Algebra.Ring.Hom.Defs
/-- `f : α →+* β` has a trivial codomain iff it has a trivial range.  -/
RingHom.codomain_trivial_iff_range_trivial : ∀ {α : Type u_2} {β : Type u_3} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β),
  0 = 1 ↔ ∀ (x_2 : α), f x_2 = 0
-- Mathlib.Algebra.MvPolynomial.Expand
MvPolynomial.rename_expand : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [inst : CommSemiring R] (p : ℕ) (f : σ → τ) (φ : MvPolynomial σ R),
  (MvPolynomial.rename f) ((MvPolynomial.expand p) φ) = (MvPolynomial.expand p) ((MvPolynomial.rename f) φ)
-- Mathlib.Order.Monotone.Monovary
MonovaryOn.subset : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
  {s t : Set ι}, s ⊆ t → MonovaryOn f g t → MonovaryOn f g s
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.vietoris.isPreconnected_biUnion : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : Set α} {f : α → Set β},
  IsPreconnected s → ContinuousOn f s → (∃ x ∈ s, IsPreconnected (f x)) → IsPreconnected (⋃ x ∈ s, f x)
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasProdUniformly.hasProdLocallyUniformly : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {g : β → α}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β], HasProdUniformly f g → HasProdLocallyUniformly f g
-- Mathlib.Analysis.Convex.GaugeRescale
gauge_gaugeRescale_le : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] (s t : Set E) (x : E),
  gauge t (gaugeRescale s t x) ≤ gauge s x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
/-- the coherence condition for the left square  -/
CategoryTheory.Limits.CatCospanTransformMorphism.left_coherence_assoc : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'}
  (self : CategoryTheory.Limits.CatCospanTransformMorphism ψ ψ') {Z : CategoryTheory.Functor A B'}
  (h : ψ'.left.comp F' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso F ψ.left ψ.base F').hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight self.left F') h) =
    CategoryTheory.CategoryStruct.comp (F.whiskerLeft self.base)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso F ψ'.left ψ'.base F').hom h)
-- Mathlib.Lean.FoldEnvironment
/-- An `IO.Ref` that keeps track of any errors that could have been thrown by `act`
when folding over the constants in the environment.  -/
Lean.Meta.FoldDeclErrorRef : Type
-- Lean.Meta.Tactic.Grind.Action
_private.Lean.Meta.Tactic.Grind.Action.0.Lean.Meta.Grind.Action.orElse.eq_1 : ∀ (x y : Lean.Meta.Grind.Action) (goal : Lean.Meta.Grind.Goal) (kna kp : Lean.Meta.Grind.ActionCont),
  x.orElse y goal kna kp = x goal (fun goal => y goal kna kp) kp
-- Mathlib.Topology.Category.FinTopCat
/-- Construct a bundled `FinTopCat` from the underlying type and the appropriate typeclasses.  -/
FinTopCat.of : (X : Type u) → [Fintype X] → [TopologicalSpace X] → FinTopCat
-- Init.Data.Nat.Basic
Nat.instCommutativeHAdd : Std.Commutative fun x1 x2 => x1 + x2
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.le_arcsin_iff_sin_le : ∀ {x y : ℝ}, x ∈ Set.Icc (-(Real.pi / 2)) (Real.pi / 2) → y ∈ Set.Icc (-1) 1 → (x ≤ Real.arcsin y ↔ Real.sin x ≤ y)
-- Mathlib.CategoryTheory.Square
/-- A morphism between two commutative squares consists of 4 morphisms
which extend these two squares into a commuting cube.  -/
CategoryTheory.Square.Hom : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Square C → CategoryTheory.Square C → Type v
-- Mathlib.Dynamics.Ergodic.Action.OfMinimal
/-- **Alias** of `aeconst_of_dense_setOfPred_preimage_vadd_ae`.

---

Let `M` act continuously on an R₁ topological space `X`.
Let `μ` be a finite inner regular measure on `X` which is ergodic with respect to this action.
If a null measurable set `s` is a.e. equal
to its preimages under the action of a dense set of elements of `M`,
then it is either null or conull.  -/
aeconst_of_dense_setOf_preimage_vadd_ae : ∀ {M : Type u_1} [inst : TopologicalSpace M] {X : Type u_2} [inst_1 : TopologicalSpace X] [R1Space X]
  [inst_3 : MeasurableSpace X] [BorelSpace X] [inst_5 : VAdd M X] [ContinuousVAdd M X] {μ : MeasureTheory.Measure X}
  [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [ErgodicVAdd M X μ] {s : Set X},
  MeasureTheory.NullMeasurableSet s μ →
    Dense {g | (fun x => g +ᵥ x) ⁻¹' s =ᵐ[μ] s} → Filter.EventuallyConst s (MeasureTheory.ae μ)
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
Nat.Partition.mk : {n : ℕ} → (parts : Multiset ℕ) → (∀ {i : ℕ}, i ∈ parts → 0 < i) → parts.sum = n → n.Partition
-- Lean.Meta.Tactic.Grind.AC.Util
Lean.Meta.Grind.AC.ACM.Context.mk.inj : ∀ {opId opId_1 : ℕ}, { opId := opId } = { opId := opId_1 } → opId = opId_1
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey_maxKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {hc : t.maxKey! ∈ t}, t.getKey t.maxKey! hc = t.maxKey!
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.eval₂_root : ∀ {R : Type u_1} [inst : CommRing R] (f : Polynomial R), Polynomial.eval₂ (AdjoinRoot.of f) (AdjoinRoot.root f) f = 0
-- Mathlib.Algebra.Algebra.Spectrum.Basic
/-- **Alias** of the reverse direction of `spectrum.inv₀_mem_iff`. -/
spectrum.inv₀_mem : ∀ {R : Type u} {A : Type v} [inst : Semifield R] [inst_1 : Ring A] [inst_2 : Algebra R A] {r : R} {a : Aˣ},
  r ∈ spectrum R ↑a⁻¹ → r⁻¹ ∈ spectrum R ↑a
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- The (nonzero) prime elements of the monoid with zero `Ideal R` correspond
to an element of type `HeightOneSpectrum R`.

See `IsDedekindDomain.HeightOneSpectrum.prime` for the inverse direction.  -/
IsDedekindDomain.HeightOneSpectrum.ofPrime : {R : Type u_1} →
  [inst : CommRing R] → [IsDedekindDomain R] → {p : Ideal R} → Prime p → IsDedekindDomain.HeightOneSpectrum R
-- Init.Data.Int.Compare
Int.instLawfulOrderOrd : Std.LawfulOrderOrd ℤ
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_mono_on : ∀ {f g : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ},
  a ≤ b →
    IntervalIntegrable f μ a b →
      IntervalIntegrable g μ a b →
        (∀ x ∈ Set.Icc a b, f x ≤ g x) → ∫ (u : ℝ) in a..b, f u ∂μ ≤ ∫ (u : ℝ) in a..b, g u ∂μ
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.isPath_mapLe : ∀ {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u v : V} {p : G.Walk u v},
  (SimpleGraph.Walk.mapLe h p).IsPath ↔ p.IsPath
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
/-- If we preserve colimits of some arbitrary size, then we preserve all finite colimits.  -/
CategoryTheory.Limits.PreservesColimitsOfSize.preservesFiniteColimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.PreservesFiniteColimits F
-- Mathlib.Order.Filter.Cofinite
Filter.comap_cofinite_le : ∀ {α : Type u_2} {β : Type u_3} (f : α → β), Filter.comap f Filter.cofinite ≤ Filter.cofinite
-- Init.Data.Vector.Lemmas
Vector.find?.eq_1 : ∀ {n : ℕ} {α : Type} (f : α → Bool) (as : Vector α n), Vector.find? f as = Array.find? f as.toArray
-- Mathlib.Order.LiminfLimsup
Filter.sup_limsup : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteDistribLattice α] {f : Filter β} {u : β → α} [f.NeBot] (a : α),
  a ⊔ Filter.limsup u f = Filter.limsup (fun x => a ⊔ u x) f
-- Mathlib.Analysis.Convex.SimplicialComplex.Basic
Geometry.SimplicialComplex.faces_bot : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E], ⊥.faces = ∅
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.instInfSet : {R : Type u} → [inst : NonAssocRing R] → InfSet (Subring R)
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
/-- The type of homotopy classes of relative morphisms.  -/
SSet.RelativeMorphism.HomotopyClass : {X Y : SSet} → (A : X.Subcomplex) → (B : Y.Subcomplex) → (A.toSSet ⟶ B.toSSet) → Type u
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
/-- the index of the intermediate object  -/
CategoryTheory.Functor.OneHypercoverDenseData.SieveStruct.i₀ : {C₀ : Type u₀} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v₀, u₀} C₀] →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor C₀ C} →
          {J₀ : CategoryTheory.GrothendieckTopology C₀} →
            {J : CategoryTheory.GrothendieckTopology C} →
              {X : C} →
                {data : F.OneHypercoverDenseData J₀ J X} →
                  {X₀ : C₀} → {f : F.obj X₀ ⟶ X} → {Y₀ : C₀} → {g : Y₀ ⟶ X₀} → data.SieveStruct f g → data.I₀
-- Mathlib.Algebra.Category.MonCat.Limits
/-- The flat sections of a functor into `MonCat` form a submonoid of all sections.  -/
MonCat.sectionsSubmonoid : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] → (F : CategoryTheory.Functor J MonCat) → Submonoid ((j : J) → ↑(F.obj j))
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonLocation.fromJson : Lean.Json → Except String Lean.Lsp.Location
-- Aesop.Forward.Match
/-- Fold over the hypotheses contained in a match.  -/
Aesop.ForwardRuleMatch.foldHypsM : {M : Type u_1 → Type u_2} → {σ : Type u_1} → [Monad M] → (σ → Lean.FVarId → M σ) → σ → Aesop.ForwardRuleMatch → M σ
-- Mathlib.Data.Finite.Prod
Set.fintypeProd : {α : Type u_1} → {β : Type u_2} → (s : Set α) → (t : Set β) → [Fintype ↑s] → [Fintype ↑t] → Fintype ↑(s ×ˢ t)
-- Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM
/-- **Alias** of `ContinuousLinearMap.postcompCompactConvergenceCLM_apply`. -/
postcomp_compactConvergenceCLM_apply : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂]
  [inst_2 : NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [inst_3 : RingHomCompTriple σ τ ρ]
  (E : Type u_4) {F : Type u_5} {G : Type u_6} [inst_4 : AddCommGroup E] [inst_5 : Module 𝕜₁ E]
  [inst_6 : AddCommGroup F] [inst_7 : Module 𝕜₂ F] [inst_8 : AddCommGroup G] [inst_9 : Module 𝕜₃ G]
  [inst_10 : TopologicalSpace E] [inst_11 : TopologicalSpace F] [inst_12 : TopologicalSpace G]
  [inst_13 : IsTopologicalAddGroup F] [inst_14 : IsTopologicalAddGroup G] [inst_15 : ContinuousConstSMul 𝕜₃ G]
  [inst_16 : ContinuousConstSMul 𝕜₂ F] (L : F →SL[τ] G) (f : UniformConvergenceCLM σ F {S | IsCompact S}),
  (ContinuousLinearMap.postcompCompactConvergenceCLM E L) f = L ∘SL f
-- Mathlib.NumberTheory.PrimeCounting
/-- The cardinality of the finset `primesLE n` equals the counting function
`primeCounting` at `n`.  -/
Nat.primesLE_card_eq_primeCounting : ∀ (n : ℕ), n.primesLE.card = n.primeCounting
-- Mathlib.Analysis.Distribution.FourierMultiplier
TemperedDistribution.fourierMultiplierCLM_toTemperedDistributionCLM_eq : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : NormedSpace ℂ F] [inst_4 : FiniteDimensional ℝ E]
  [inst_5 : MeasurableSpace E] [inst_6 : BorelSpace E] [CompleteSpace F] {g : E → ℂ},
  Function.HasTemperateGrowth g →
    ∀ (f : SchwartzMap E F),
      (TemperedDistribution.fourierMultiplierCLM F g)
          ((SchwartzMap.toTemperedDistributionCLM E F MeasureTheory.volume) f) =
        (SchwartzMap.toTemperedDistributionCLM E F MeasureTheory.volume) ((SchwartzMap.fourierMultiplierCLM F g) f)