mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Matrix.Basis
Matrix.single_mem_matrix : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_7} [inst : DecidableEq m] [inst_1 : DecidableEq n] [inst_2 : Zero α]
  {S : Set α}, 0 ∈ S → ∀ {i : m} {j : n} {a : α}, Matrix.single i j a ∈ S.matrix ↔ a ∈ S
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.fst_map_swap : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {ρ : MeasureTheory.Measure (α × β)}, (MeasureTheory.Measure.map Prod.swap ρ).fst = ρ.snd
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.support_sub_subset : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : AddGroup R] (x y : HahnSeries Γ R),
  (x - y).support ⊆ x.support ∪ y.support
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.balance2_All : ∀ {α : Type u_1} {p : α → Prop} {l : RBTree.RBNode α} {v : α} {r : RBTree.RBNode α},
  RBTree.RBNode.All p (l.balance2 v r) ↔ p v ∧ RBTree.RBNode.All p l ∧ RBTree.RBNode.All p r
-- Lean.Meta.Sym.AlphaShareBuilder
Lean.Meta.Sym.Internal.mkConstS : {m : Type → Type} →
  [Lean.Meta.Sym.Internal.MonadShareCommon m] → Lean.Name → optParam (List Lean.Level) [] → m Lean.Expr
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.mk.sizeOf_spec : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : SizeOf X] (val : X), sizeOf { val := val } = 1 + sizeOf val
-- Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
_private.Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity.0.MeasureTheory.le_mul_iff_eq_zero_of_nonneg_of_neg_of_nonneg : ∀ {α : Type u_7} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a b c : α},
  0 ≤ a → b < 0 → 0 ≤ c → (a ≤ b * c ↔ a = 0 ∧ c = 0)
-- Mathlib.RingTheory.RingHom.Etale
/-- A ring hom `R →+* S` is étale, if `S` is an étale `R`-algebra.  -/
RingHom.Etale : {R : Type u_3} → {S : Type u_4} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
-- Mathlib.Tactic.Widget.StringDiagram
/-- The start point of the strand in the string diagram.  -/
Mathlib.Tactic.Widget.StringDiagram.Strand.startPoint : Mathlib.Tactic.Widget.StringDiagram.Strand → Mathlib.Tactic.Widget.StringDiagram.Node
-- Mathlib.LinearAlgebra.Orientation
Orientation.reindex_apply : ∀ (R : Type u_1) [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] (M : Type u_2)
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {ι : Type u_4} {ι' : Type u_5} (e : ι ≃ ι') (v : M [⋀^ι]→ₗ[R] R)
  (hv : v ≠ 0), (Orientation.reindex R M e) (rayOfNeZero R v hv) = rayOfNeZero R (AlternatingMap.domDomCongr e v) ⋯
-- Lean.Meta.Tactic.SolveByElim
Lean.Meta.SolveByElim.SolveByElimConfig.toApplyRulesConfig : Lean.Meta.SolveByElim.SolveByElimConfig → Lean.Meta.SolveByElim.ApplyRulesConfig
-- Mathlib.Topology.UniformSpace.UniformConvergence
/-- **Alias** of the reverse direction of `tendstoUniformlyOn_iff_tendstoUniformlyOnFilter`. -/
TendstoUniformlyOnFilter.tendstoUniformlyOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α}
  {p : Filter ι}, TendstoUniformlyOnFilter F f p (Filter.principal s) → TendstoUniformlyOn F f p s
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.isLittleO_const_log_atTop : ∀ {c : ℝ}, (fun x => c) =o[Filter.atTop] Real.log
-- Mathlib.Probability.Moments.SubGaussian
/-- Chernoff bound on the right tail of a sub-Gaussian random variable.  -/
ProbabilityTheory.Kernel.HasSubgaussianMGF.measure_ge_le : ∀ {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'}
  {κ : ProbabilityTheory.Kernel Ω' Ω} {X : Ω → ℝ} {c : NNReal},
  ProbabilityTheory.Kernel.HasSubgaussianMGF X c κ ν →
    ∀ {ε : ℝ}, 0 ≤ ε → ∀ᵐ (ω' : Ω') ∂ν, (κ ω').real {ω | ε ≤ X ω} ≤ Real.exp (-ε ^ 2 / (2 * ↑c))
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.opcyclesMap_threeδ₂Toδ₁_opcyclesToE_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₁₂ : i₀ ⟶ i₂) (f₂₃ : i₁ ⟶ i₃) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.opcyclesMap_threeδ₂Toδ₁_opcyclesToE._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.opcyclesMap_threeδ₂Toδ₁_opcyclesToE._auto_3)
  {Z : C} (h : X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (X.opcyclesMap f₁ f₂₃ f₁₂ f₃ (CategoryTheory.ComposableArrows.threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃) n₁)
      (CategoryTheory.CategoryStruct.comp (X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Analysis.Convex.BetweenList
List.wbtw_triple : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] {p₁ p₂ p₃ : P}, List.Wbtw R [p₁, p₂, p₃] ↔ Wbtw R p₁ p₂ p₃
-- Mathlib.Analysis.Calculus.FDeriv.Mul
Differentiable.const_mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝔸 : Type u_5} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸] {a : E → 𝔸},
  Differentiable 𝕜 a → ∀ (b : 𝔸), Differentiable 𝕜 fun y => b * a y
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.Extension.addGrindEqAttr : Lean.Meta.Grind.Extension →
  Lean.Name →
    Lean.AttributeKind → Lean.Meta.Grind.EMatchTheoremKind → optParam Bool true → optParam Bool false → Lean.MetaM Unit
-- Mathlib.MeasureTheory.Measure.Regular
/-- In a `σ`-compact space, any closed set can be approximated by a compact subset.  -/
MeasureTheory.Measure.InnerRegularWRT.isCompact_isClosed : ∀ {X : Type u_3} [inst : TopologicalSpace X] [SigmaCompactSpace X] [inst_2 : MeasurableSpace X]
  (μ : MeasureTheory.Measure X), μ.InnerRegularWRT IsCompact IsClosed
-- Std.Sat.AIG.Lemmas
Std.Sat.AIG.mkGate.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig : Std.Sat.AIG α) (input : aig.BinaryInput),
  aig.mkGate input =
    {
      aig :=
        {
          decls :=
            aig.decls.push
              (Std.Sat.AIG.Decl.gate (Std.Sat.AIG.Fanin.mk input.lhs.gate input.lhs.invert)
                (Std.Sat.AIG.Fanin.mk input.rhs.gate input.rhs.invert)),
          cache := aig.cache.noUpdate, hdag := ⋯, hzero := ⋯, hconst := ⋯ },
      ref := { gate := aig.decls.size, invert := false, hgate := ⋯ } }
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgHom.instFunLike : {R : Type u_2} →
  {A : Type u_3} →
    {B : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : Star A] →
              [inst_4 : Semiring B] → [inst_5 : Algebra R B] → [inst_6 : Star B] → FunLike (A →⋆ₐ[R] B) A B
-- Mathlib.GroupTheory.Coxeter.Length
CoxeterSystem.isRightDescent_iff : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {w : W} {i : B},
  cs.IsRightDescent w i ↔ cs.length (w * cs.simple i) + 1 = cs.length w
-- Std.Data.HashMap.Basic
/-- Inserts the given mapping into the map. If there is already a mapping for the given key, then both
key and value will be replaced.

Note: this replacement behavior is true for `HashMap`, `DHashMap`, `HashMap.Raw` and `DHashMap.Raw`.
The `insert` function on `HashSet` and `HashSet.Raw` behaves differently: it will return the set
unchanged if a matching key is already present.
 -/
Std.HashMap.insert : {α : Type u} → {β : Type v} → {x : BEq α} → {x_1 : Hashable α} → Std.HashMap α β → α → β → Std.HashMap α β
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Normal
CategoryTheory.IsMonHom.Normal.of_isPullback_η : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G H : C} [inst_2 : CategoryTheory.GrpObj G] [inst_3 : CategoryTheory.GrpObj H] {φ : H ⟶ G}
  [CategoryTheory.IsMonHom φ] {P : C} (p : G ⟶ P) [inst_5 : CategoryTheory.GrpObj P] [CategoryTheory.IsMonHom p],
  CategoryTheory.IsPullback φ (CategoryTheory.SemiCartesianMonoidalCategory.toUnit H) p CategoryTheory.MonObj.one →
    CategoryTheory.IsMonHom.Normal φ
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.sumInr_isExpansionOn : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} (M : Type u_1) [inst : L.Structure M] [inst_1 : L'.Structure M],
  FirstOrder.Language.LHom.sumInr.IsExpansionOn M
-- Mathlib.Topology.MetricSpace.Congruence
/-- Families with at most a single point are always congruent.  -/
Congruent.of_subsingleton_index : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoEMetricSpace P₁]
  [inst_1 : PseudoEMetricSpace P₂] [Subsingleton ι], Congruent v₁ v₂
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- Define a continuous semilinear map from Schwartz space to a normed space.  -/
SchwartzMap.mkCLMtoNormedSpace : {𝕜 : Type u_2} →
  {𝕜' : Type u_3} →
    {D : Type u_4} →
      {E : Type u_5} →
        {G : Type u_7} →
          [inst : NormedAddCommGroup E] →
            [inst_1 : NormedSpace ℝ E] →
              [inst_2 : NormedField 𝕜] →
                [inst_3 : NormedField 𝕜'] →
                  [inst_4 : NormedAddCommGroup D] →
                    [inst_5 : NormedSpace ℝ D] →
                      [inst_6 : NormedSpace 𝕜 E] →
                        [inst_7 : SMulCommClass ℝ 𝕜 E] →
                          [inst_8 : NormedAddCommGroup G] →
                            [inst_9 : NormedSpace 𝕜' G] →
                              {σ : 𝕜 →+* 𝕜'} →
                                [RingHomIsometric σ] →
                                  (A : SchwartzMap D E → G) →
                                    (∀ (f g : SchwartzMap D E), A (f + g) = A f + A g) →
                                      (∀ (a : 𝕜) (f : SchwartzMap D E), A (a • f) = σ a • A f) →
                                        (∃ s C,
                                            0 ≤ C ∧
                                              ∀ (f : SchwartzMap D E),
                                                ‖A f‖ ≤ C * (s.sup (schwartzSeminormFamily 𝕜 D E)) f) →
                                          SchwartzMap D E →SL[σ] G
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
ModuleCat.Derivation.d.eq_1 : ∀ {A B : CommRingCat} {M : ModuleCat ↑B} {f : A ⟶ B} (D : M.Derivation f) (b : ↑B), D.d b = ↑D b
-- Mathlib.RingTheory.Localization.Integral
/-- If the field `L` is a finite extension of the fraction field of the integral domain `A`,
the integral closure of `A` in `L` has fraction field `L`.  -/
integralClosure.isFractionRing_of_finite_extension : ∀ {A : Type u_3} (K : Type u_4) [inst : CommRing A] (L : Type u_5) [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra A K] [IsFractionRing A K] [IsDomain A] [inst_6 : Algebra A L] [inst_7 : Algebra K L]
  [IsScalarTower A K L] [FiniteDimensional K L], IsFractionRing (↥(integralClosure A L)) L
-- Lean.Meta.Tactic.SplitIf
Lean.Meta.SplitKind.match : Lean.Meta.SplitKind
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.swap.eq_1 : ∀ (α : Type u_4) (β : Type u_5) [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β],
  ProbabilityTheory.Kernel.swap α β = ProbabilityTheory.Kernel.deterministic Prod.swap ⋯
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.injective_iff_isRegular : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f],
  Function.Injective ⇑f ↔ ∀ (c : ↥S), IsSMulRegular M c
-- Mathlib.CategoryTheory.Comma.Over.Pullback
CategoryTheory.Over.instIsRightAdjointPullback : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPullbacksAlong f], (CategoryTheory.Over.pullback f).IsRightAdjoint
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.compMeasurePreserving_comp : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {β : Type u_7} [inst_1 : MeasurableSpace β] {μb : MeasureTheory.Measure β}
  {γ : Type u_8} {mγ : MeasurableSpace γ} {μc : MeasureTheory.Measure γ} {f : β → γ}
  (hf : MeasureTheory.MeasurePreserving f μb μc) {f' : α → β} (hf' : MeasureTheory.MeasurePreserving f' μ μb),
  MeasureTheory.Lp.compMeasurePreserving (f ∘ f') ⋯ =
    (MeasureTheory.Lp.compMeasurePreserving f' hf').comp (MeasureTheory.Lp.compMeasurePreserving f hf)
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trNormal_respects : ∀ (c : Turing.ToPartrec.Code) (k : Turing.ToPartrec.Cont) (v : List ℕ) (s : Option Turing.PartrecToTM2.Γ'),
  ∃ b₂,
    Turing.PartrecToTM2.TrCfg (Turing.ToPartrec.stepNormal c k v) b₂ ∧
      StateTransition.Reaches₁ (Turing.TM2.step Turing.PartrecToTM2.tr)
        { l := some (Turing.PartrecToTM2.trNormal c (Turing.PartrecToTM2.trCont k)), var := s,
          stk := Turing.PartrecToTM2.K'.elim (Turing.PartrecToTM2.trList v) [] [] (Turing.PartrecToTM2.trContStack k) }
        b₂
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.ofHasCokernelOfHasKernel_p : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : CategoryTheory.Limits.HasCokernel S.f]
  [inst_3 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.desc S.f S.g ⋯)],
  (CategoryTheory.ShortComplex.RightHomologyData.ofHasCokernelOfHasKernel S).p = CategoryTheory.Limits.cokernel.π S.f
-- Mathlib.ModelTheory.PartialEquiv
/-- A partial `L`-equivalence, implemented as an equivalence between substructures.  -/
FirstOrder.«term_≃ₚ[_]_» : Lean.TrailingParserDescr
-- Aesop.Forward.PremiseIndex
Aesop.PremiseIndex.mk.sizeOf_spec : ∀ (toNat : ℕ), sizeOf { toNat := toNat } = 1 + sizeOf toNat
-- Mathlib.Topology.Spectral.Hom
/-- The type of spectral maps from `α` to `β`.  -/
SpectralMap : (α : Type u_6) → (β : Type u_7) → [TopologicalSpace α] → [TopologicalSpace β] → Type (max u_6 u_7)
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.bound_eq_one : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [Nonempty α]
  (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel κ], κ.bound = 1
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cochain.toSingleMk_surjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {q n : ℤ}
  (α : CochainComplex.HomComplex.Cochain K ((CochainComplex.singleFunctor C q).obj X) n) (p : ℤ) (h : p + n = q),
  ∃ f, CochainComplex.HomComplex.Cochain.toSingleMk f h = α
-- Mathlib.Topology.MetricSpace.Bounded
Metric.disjoint_nhds_cobounded : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x : α), Disjoint (nhds x) (Bornology.cobounded α)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
AffineSubspace.mk'_le_mk'_iff : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] (p : P) {d₁ d₂ : Submodule k V}, AffineSubspace.mk' p d₁ ≤ AffineSubspace.mk' p d₂ ↔ d₁ ≤ d₂
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
CliffordAlgebra.involute_eq_of_mem_odd : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {x : CliffordAlgebra Q}, x ∈ CliffordAlgebra.evenOdd Q 1 → CliffordAlgebra.involute x = -x
-- Mathlib.Order.Antichain
IsAntichain.diff : ∀ {α : Type u_1} {r : α → α → Prop} {s t : Set α}, IsAntichain r s → IsAntichain r (s \ t)
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.add_comp : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_8} {M₂ : Type u_10} {M₃ : Type u_11} [inst : Semiring R₁]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] [inst_6 : Module R₁ M] [inst_7 : Module R₂ M₂] [inst_8 : Module R₃ M₃] {σ₁₂ : R₁ →+* R₂}
  {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂)
  (g h : M₂ →ₛₗ[σ₂₃] M₃), (h + g) ∘ₛₗ f = h ∘ₛₗ f + g ∘ₛₗ f
-- Mathlib.Analysis.InnerProductSpace.PiL2
LinearIsometry.comp.congr_simp : ∀ {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {E : Type u_5} {E₂ : Type u_6} {E₃ : Type u_7} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] {σ₁₂ : R →+* R₂} {σ₁₃ : R →+* R₃} {σ₂₃ : R₂ →+* R₃}
  [inst_3 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂]
  [inst_6 : SeminormedAddCommGroup E₃] [inst_7 : Module R E] [inst_8 : Module R₂ E₂] [inst_9 : Module R₃ E₃]
  (g g_1 : E₂ →ₛₗᵢ[σ₂₃] E₃), g = g_1 → ∀ (f f_1 : E →ₛₗᵢ[σ₁₂] E₂), f = f_1 → g.comp f = g_1.comp f_1
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Equivalence.op_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D), e.op.functor = e.functor.op
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.instHasPullbacksOfArrowsOfHasPullback : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) {ι : Type u_1} (Z : ι → C)
  (g : (i : ι) → Z i ⟶ X) [∀ (i : ι), CategoryTheory.Limits.HasPullback (g i) f],
  (CategoryTheory.Presieve.ofArrows Z g).HasPullbacks f
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Broadcast.Receiver.inner : {α : Type} → Std.Broadcast.Receiver α → Std.Bounded.Receiver✝ α
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
List.pairwise_sameCycle_formPerm : ∀ {α : Type u_1} [inst : DecidableEq α] {l : List α}, l.Nodup → 2 ≤ l.length → List.Pairwise l.formPerm.SameCycle l
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
AlgebraicGeometry.HasRingHomProperty.ext : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
  [AlgebraicGeometry.HasRingHomProperty P Q] {P' : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  {Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
  [AlgebraicGeometry.HasRingHomProperty P' fun {R S} [CommRing R] [CommRing S] => Q'],
  (∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S), Q f ↔ Q' f) → P = P'
-- Mathlib.Algebra.Order.Field.Pointwise
LinearOrderedField.smul_Ioo : ∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] {a b r : K},
  0 < r → r • Set.Ioo a b = Set.Ioo (r * a) (r * b)
-- Init.Prelude
instLTUInt8 : LT UInt8
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.instPartialOrder : {α : Type u_1} → [inst : LE α] → PartialOrder (LowerSet α)
-- Mathlib.CategoryTheory.Category.Basic
/-- Identity morphisms are left identities for composition.  -/
CategoryTheory.Category.id_comp : ∀ {obj : Type u} [self : CategoryTheory.Category.{v, u} obj] {X Y : obj} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id X) f = f
-- Mathlib.Tactic.Order.ToInt
/-- The main theorem asserting the existence of a translation.
We use `Classical.choose` to turn this into a value for use in the `order` tactic,
see `toInt`.
 -/
Mathlib.Tactic.Order.ToInt.exists_translation : ∀ {α : Type u_1} [inst : LinearOrder α] {n : ℕ} (val : Fin n → α), ∃ tr, ∀ (i j : Fin n), val i ≤ val j ↔ tr i ≤ tr j
-- Mathlib.Data.Set.Finite.Basic
/-- **Alias** of the forward direction of `Set.finite_univ_iff`. -/
Finite.of_finite_univ : ∀ {α : Type u}, Set.univ.Finite → Finite α
-- Lean.Elab.Binders
Lean.Elab.Term.LetIdDeclView.id : Lean.Elab.Term.LetIdDeclView → Lean.Syntax
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.canonical_right_p : ∀ {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.HomologyData.canonical S).right.p = S.pOpcycles
-- Std.Sat.AIG.Basic
Std.Sat.AIG.Decl.gate.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (l r : Std.Sat.AIG.Fanin), sizeOf (Std.Sat.AIG.Decl.gate l r) = 1 + sizeOf l + sizeOf r
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
AddMonCat.FilteredColimits.colimitAddAux.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCat)
  [inst_1 : CategoryTheory.IsFiltered J] (x y : (j : J) × ↑(F.obj j)),
  AddMonCat.FilteredColimits.colimitAddAux F x y =
    AddMonCat.FilteredColimits.M.mk F
      ⟨CategoryTheory.IsFiltered.max x.fst y.fst,
        (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.IsFiltered.leftToMax x.fst y.fst))) x.snd +
          (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.IsFiltered.rightToMax x.fst y.fst))) y.snd⟩
-- Mathlib.Order.Disjoint
Disjoint.dual : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] {a b : α},
  Disjoint a b → Codisjoint (OrderDual.toDual a) (OrderDual.toDual b)
-- Mathlib.Topology.DiscreteSubset
/-- The union of two discrete closed subsets is discrete.  -/
IsDiscrete.union : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X},
  IsDiscrete s → IsDiscrete t → IsClosed s → IsClosed t → IsDiscrete (s ∪ t)
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.trans_symm_cancel_right : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_8} {M₂ : Type u_9} {M₃ : Type u_10} [inst : Semiring R₁]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃}
  {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₁₃ : R₁ →+* R₃} {σ₃₁ : R₃ →+* R₁} [inst_6 : RingHomInvPair σ₁₃ σ₃₁]
  [inst_7 : RingHomInvPair σ₃₁ σ₁₃] {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
  {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {re₂₃ : RingHomInvPair σ₂₃ σ₃₂} {re₃₂ : RingHomInvPair σ₃₂ σ₂₃}
  [inst_8 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_9 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁]
  [inst_10 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃] [inst_11 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂] (e : M₁ ≃ₛₗ[σ₁₂] M₂)
  (f : M₃ ≃ₛₗ[σ₃₁] M₁), (f.trans e).trans e.symm = f
-- Mathlib.Tactic.ProdAssoc
Lean.Expr.ProdTree.type.injEq : ∀ (tp : Lean.Expr) (l : Lean.Level) (tp_1 : Lean.Expr) (l_1 : Lean.Level),
  (Lean.Expr.ProdTree.type tp l = Lean.Expr.ProdTree.type tp_1 l_1) = (tp = tp_1 ∧ l = l_1)
-- Mathlib.RingTheory.Congruence.Basic
/-- The infimum of a set of congruence relations is the same as the infimum of the set's image
under the map to the underlying binary relation.  -/
RingCon.coe_sInf : ∀ {R : Type u_3} [inst : Add R] [inst_1 : Mul R] (S : Set (RingCon R)), ⇑(sInf S) = sInf (DFunLike.coe '' S)
-- Mathlib.Tactic.Ring.Common
/-- A typed expression of type `CommSemiring ℕ` used when we are working on
ring subexpressions of type `ℕ`.
 -/
Mathlib.Tactic.Ring.Common.sℕ : Q(CommSemiring ℕ)
-- Mathlib.CategoryTheory.Sites.ConstantSheaf
CategoryTheory.Sheaf.isConstant_of_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C)
  {D : Type u_2} [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  {F : CategoryTheory.Sheaf J D} {X : D} (i : F ≅ (CategoryTheory.constantSheaf J D).obj X),
  CategoryTheory.Sheaf.IsConstant J F
-- Mathlib.RingTheory.WittVector.Basic
WittVector.constantCoeff_apply : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] (x : WittVector p R),
  WittVector.constantCoeff x = x.coeff 0
-- Mathlib.Topology.MetricSpace.Bounded
Metric.comap_dist_right_atTop : ∀ {α : Type u} [inst : PseudoMetricSpace α] (c : α),
  Filter.comap (fun x => dist x c) Filter.atTop = Bornology.cobounded α