mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.mk : {R : Type u_2} →
  {M : Type u_4} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] →
        [inst_2 : AddCommMonoid M] →
          [inst_3 : SMul R M] →
            (carrier : Set M) →
              (∀ ⦃c : R⦄, 0 < c → ∀ ⦃x : M⦄, x ∈ carrier → c • x ∈ carrier) →
                (∀ ⦃x : M⦄, x ∈ carrier → ∀ ⦃y : M⦄, y ∈ carrier → x + y ∈ carrier) → ConvexCone R M
-- Mathlib.Algebra.Order.Monovary
MonovaryOn.div_right₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : Semifield β] [inst_2 : LinearOrder β]
  [IsStrictOrderedRing β] {s : Set ι} {f : ι → α} {g₁ g₂ : ι → β},
  (∀ i ∈ s, 0 ≤ g₁ i) → (∀ i ∈ s, 0 < g₂ i) → MonovaryOn f g₁ s → AntivaryOn f g₂ s → MonovaryOn f (g₁ / g₂) s
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKey?_insertManyIfNewUnit_list_of_contains : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) [EquivBEq α]
  [LawfulHashable α],
  (↑m).WF →
    ∀ {l : List α} {k : α},
      m.contains k = true → (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l)).getKey? k = m.getKey? k
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If the sign of the angle between three points is negative, the first two points are not
equal.  -/
EuclideanGeometry.left_ne_of_oangle_sign_eq_neg_one : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P}, (EuclideanGeometry.oangle p₁ p₂ p₃).sign = -1 → p₁ ≠ p₂
-- Init.Data.List.Sublist
List.subset_nil : ∀ {α : Type u_1} {l : List α}, l ⊆ [] ↔ l = []
-- Std.Http.Internal.String
/-- Checks whether a string is a valid non-empty HTTP token.
 -/
Std.Http.Internal.isToken : String → Bool
-- Mathlib.Condensed.Discrete.LocallyConstant
LightCondSet.LocallyConstant.instFaithfulLightCondensedTypeDiscrete : (LightCondensed.discrete (Type u)).Faithful
-- Lean.Server.Requests
Lean.Server.LspResponse.isComplete : {α : Type} → Lean.Server.LspResponse α → Bool
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
/-- Harder inclusion: at a point in `D f K`, the function `f` has a derivative, in `K`.  -/
FDerivMeasurableAux.D_subset_differentiable_set : ∀ {𝕜 : 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}
  {K : Set (E →L[𝕜] F)}, IsComplete K → FDerivMeasurableAux.D f K ⊆ {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K}
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get_map : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  {γ : α → Type w} [inst_2 : LawfulBEq α] {f : (a : α) → β a → γ a} {k : α} (h : (↑m).WF)
  {h' : (Std.DHashMap.Internal.Raw₀.map f m).contains k = true},
  (Std.DHashMap.Internal.Raw₀.map f m).get k h' = f k (m.get k ⋯)
-- Mathlib.Analysis.InnerProductSpace.PiL2
EuclideanSpace.single_apply : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] [inst_1 : DecidableEq ι] (i : ι) (a : 𝕜) (j : ι),
  (EuclideanSpace.single i a).ofLp j = if j = i then a else 0
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.isTheta_sup : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [inst : SeminormedAddCommGroup E'] [inst_1 : SeminormedAddCommGroup F']
  {f' : α → E'} {g' : α → F'} {l l' : Filter α}, f' =Θ[l ⊔ l'] g' ↔ f' =Θ[l] g' ∧ f' =Θ[l'] g'
-- Mathlib.MeasureTheory.Constructions.HaarToSphere
MeasureTheory.integrable_fun_norm_addHaar : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] {F : Type u_2}
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [Nontrivial E] (μ : MeasureTheory.Measure E)
  [FiniteDimensional ℝ E] [BorelSpace E] [μ.IsAddHaarMeasure] {f : ℝ → F},
  MeasureTheory.Integrable (fun x => f ‖x‖) μ ↔
    MeasureTheory.IntegrableOn (fun y => y ^ (Module.finrank ℝ E - 1) • f y) (Set.Ioi 0) MeasureTheory.volume
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.containsThenInsertIfNew_fst : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α],
  m.WF → ∀ {k : α} {v : β}, (m.containsThenInsertIfNew k v).1 = m.contains k
-- Mathlib.Algebra.Group.UniqueProds.Basic
Additive.instTwoUniqueSumsOfTwoUniqueProds : ∀ {M : Type u_1} [inst : Mul M] [TwoUniqueProds M], TwoUniqueSums (Additive M)
-- Mathlib.GroupTheory.Perm.Cycle.Type
/-- The cycle type of a permutation  -/
Equiv.Perm.cycleType : {α : Type u_1} → [Fintype α] → [DecidableEq α] → Equiv.Perm α → Multiset ℕ
-- Mathlib.Data.Sign.Defs
sign_eq_one_iff : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : Preorder α] [inst_2 : DecidableLT α] {a : α}, SignType.sign a = 1 ↔ 0 < a
-- Mathlib.RingTheory.PowerSeries.Inverse
PowerSeries.coeff_inv_aux : ∀ {R : Type u_1} [inst : Ring R] (n : ℕ) (a : R) (φ : PowerSeries R),
  (PowerSeries.coeff n) (PowerSeries.inv.aux a φ) =
    if n = 0 then a
    else
      -a *
        ∑ x ∈ Finset.HasAntidiagonal.antidiagonal n,
          if x.2 < n then (PowerSeries.coeff x.1) φ * (PowerSeries.coeff x.2) (PowerSeries.inv.aux a φ) else 0
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
_private.Mathlib.Tactic.CategoryTheory.Coherence.Normalize.0.Mathlib.Tactic.BicategoryLike.evalWhiskerLeft.match_1.splitter : (motive : Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.NormalExpr → Sort u_1) →
  (x : Mathlib.Tactic.BicategoryLike.Mor₁) →
    (x_1 : Mathlib.Tactic.BicategoryLike.NormalExpr) →
      ((f : Mathlib.Tactic.BicategoryLike.Mor₁) →
          (e : Mathlib.Tactic.BicategoryLike.Mor₂) →
            (α : Mathlib.Tactic.BicategoryLike.Structural) →
              motive f (Mathlib.Tactic.BicategoryLike.NormalExpr.nil e α)) →
        ((f : Mathlib.Tactic.BicategoryLike.Atom₁) →
            (e : Mathlib.Tactic.BicategoryLike.Mor₂) →
              (α : Mathlib.Tactic.BicategoryLike.Structural) →
                (η : Mathlib.Tactic.BicategoryLike.WhiskerLeft) →
                  (ηs : Mathlib.Tactic.BicategoryLike.NormalExpr) →
                    motive (Mathlib.Tactic.BicategoryLike.Mor₁.of f)
                      (Mathlib.Tactic.BicategoryLike.NormalExpr.cons e α η ηs)) →
          ((e : Lean.Expr) →
              (f g : Mathlib.Tactic.BicategoryLike.Mor₁) →
                (η : Mathlib.Tactic.BicategoryLike.NormalExpr) →
                  (∀ (e : Mathlib.Tactic.BicategoryLike.Mor₂) (α : Mathlib.Tactic.BicategoryLike.Structural),
                      η = Mathlib.Tactic.BicategoryLike.NormalExpr.nil e α → False) →
                    motive (Mathlib.Tactic.BicategoryLike.Mor₁.comp e f g) η) →
            ((e : Lean.Expr) →
                (a : Mathlib.Tactic.BicategoryLike.Obj) →
                  (η : Mathlib.Tactic.BicategoryLike.NormalExpr) →
                    (∀ (e : Mathlib.Tactic.BicategoryLike.Mor₂) (α : Mathlib.Tactic.BicategoryLike.Structural),
                        η = Mathlib.Tactic.BicategoryLike.NormalExpr.nil e α → False) →
                      motive (Mathlib.Tactic.BicategoryLike.Mor₁.id e a) η) →
              motive x x_1
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
/-- One can reformulate being `Cⁿ` within a set at a point as being `Cⁿ` in the source space when
composing with the extended chart.  -/
contMDiffWithinAt_iff_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} {x : M}
  {n : WithTop ℕ∞},
  ContMDiffWithinAt I I' n f s x ↔
    ContMDiffWithinAt (modelWithCornersSelf 𝕜 E) I' n (f ∘ ↑(extChartAt I x).symm)
      (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I) (↑(extChartAt I x) x)
-- Mathlib.Topology.Algebra.ProperAction.Basic
/-- If `H` is a closed subgroup of `G` and `G` acts properly on `X`, then so does `H`.  -/
instProperSMulSubtypeMemSubgroupOfIsClosedCoe : ∀ {G : Type u_1} {X : Type u_2} [inst : Group G] [inst_1 : MulAction G X] [inst_2 : TopologicalSpace G]
  [inst_3 : TopologicalSpace X] {H : Subgroup G} [ProperSMul G X] [H_closed : IsClosed ↑H], ProperSMul (↥H) X
-- Mathlib.Algebra.GradedMonoid
/-- When `A` is a `SetLike.GradedMonoid A`, then the homogeneous elements forms a submonoid.  -/
SetLike.homogeneousSubmonoid : {ι : Type u_1} →
  {R : Type u_2} →
    {S : Type u_3} →
      [inst : SetLike S R] →
        [inst_1 : AddMonoid ι] → [inst_2 : Monoid R] → (A : ι → S) → [SetLike.GradedMonoid A] → Submonoid R
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.norm_assoc : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] (x : TensorProduct 𝕜 (TensorProduct 𝕜 E F) G),
  ‖(TensorProduct.assoc 𝕜 E F G) x‖ = ‖x‖
-- Lean.Server.Rpc.Basic
/-- The *RPC wire format* specifies how user data is encoded in RPC requests.  -/
Lean.Lsp.RpcWireFormat : Type
-- Init.Data.SInt.Lemmas
Int32.ofNat_mod : ∀ {a b : ℕ}, a < 2 ^ 31 → b < 2 ^ 31 → Int32.ofNat (a % b) = Int32.ofNat a % Int32.ofNat b
-- Init.Data.Iterators.Consumers.Partial
/-- The wrapped iterator, which was wrapped by `Iter.allowNontermination`.
 -/
Std.Iter.Partial.it : {α β : Type w} → Std.Iter.Partial β → Std.Iter β
-- Mathlib.Data.Finset.NoncommProd
Finset.noncommProd_congr : ∀ {α : Type u_3} {β : Type u_4} [inst : Monoid β] {s₁ s₂ : Finset α} {f g : α → β} (h₁ : s₁ = s₂)
  (h₂ : ∀ x ∈ s₂, f x = g x) (comm : (↑s₁).Pairwise (Function.onFun Commute f)),
  s₁.noncommProd f comm = s₂.noncommProd g ⋯
-- Mathlib.Analysis.Normed.Ring.Lemmas
tendsto_pow_cobounded_cobounded : ∀ {α : Type u_1} [inst : SeminormedRing α] [NormOneClass α] [NormMulClass α] {m : ℕ},
  m ≠ 0 → Filter.Tendsto (fun x => x ^ m) (Bornology.cobounded α) (Bornology.cobounded α)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.foldrM_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} {δ : Type w} {m : Type w → Type w'}
  [Std.TransCmp cmp] [inst : Monad m] [LawfulMonad m] {f : α → β → δ → m δ} {init : δ},
  t₁.Equiv t₂ → Std.TreeMap.foldrM f init t₁ = Std.TreeMap.foldrM f init t₂
-- Mathlib.Logic.Equiv.Finset
/-- An encodable `Fintype` is equivalent to the same size `Fin`.  -/
Encodable.fintypeEquivFin : {α : Type u_1} → [inst : Fintype α] → [Encodable α] → α ≃ Fin (Fintype.card α)
-- Mathlib.Analysis.SumOverResidueClass
/-- If `f` is a summable function on `ℕ`, and `0 < N`, then we may compute `∑' n : ℕ, f n` by
summing each residue class mod `N` separately.  -/
Nat.sumByResidueClasses : ∀ {R : Type u_1} [inst : AddCommGroup R] [inst_1 : UniformSpace R] [IsUniformAddGroup R] [CompleteSpace R] [T0Space R]
  {f : ℕ → R}, Summable f → ∀ (N : ℕ) [inst_5 : NeZero N], ∑' (n : ℕ), f n = ∑ j, ∑' (m : ℕ), f (j.val + N * m)
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.entryAtIdx.match_3.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2}
  (motive : (x : Std.DTreeMap.Internal.Impl α β) → x.Balanced → (x_2 : ℕ) → x_2 < x.size → Sort u_3) (size : ℕ) (k : α)
  (v : β k) (l' r' : Std.DTreeMap.Internal.Impl α β) (hl : (Std.DTreeMap.Internal.Impl.inner size k v l' r').Balanced)
  (n : ℕ) (h : n < (Std.DTreeMap.Internal.Impl.inner size k v l' r').size)
  (h_1 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l' r' : Std.DTreeMap.Internal.Impl α β) →
            (hl : (Std.DTreeMap.Internal.Impl.inner size k v l' r').Balanced) →
              (n : ℕ) →
                (h : n < (Std.DTreeMap.Internal.Impl.inner size k v l' r').size) →
                  motive (Std.DTreeMap.Internal.Impl.inner size k v l' r') hl n h),
  (match Std.DTreeMap.Internal.Impl.inner size k v l' r', hl, n, h with
    | Std.DTreeMap.Internal.Impl.inner size k v l' r', hl, n, h => h_1 size k v l' r' hl n h) =
    h_1 size k v l' r' hl n h
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.Scheme.Modules.instIsScalarTowerCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecPresheafOpOpensCarrierAbPresheaf : ∀ {R : CommRingCat} {M : (AlgebraicGeometry.Spec R).Modules} {U : (AlgebraicGeometry.Spec R).Opens},
  IsScalarTower ↑R ↑((AlgebraicGeometry.Spec R).presheaf.obj (Opposite.op U)) ↑(M.presheaf.obj (Opposite.op U))
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.instIsLeftAdjointModuleCatCarrierModulesSpecOfFunctor : ∀ {R : CommRingCat}, (AlgebraicGeometry.tilde.functor R).IsLeftAdjoint
-- Std.Sync.Channel
Std.CloseableChannel.instNonemptyFlavors : ∀ {α : Type}, Nonempty (Std.CloseableChannel.Flavors α)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.leftUnitor_neg_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (G : CategoryTheory.AddGrp C),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor G).inv.hom.hom =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor G.X).inv
-- Mathlib.Data.Int.Fib.Basic
_private.Mathlib.Data.Int.Fib.Basic.0.Int.fib_natCast_dvd : ∀ {m : ℕ} {n : ℤ}, ↑m ∣ n → Int.fib ↑m ∣ Int.fib n
-- Mathlib.Analysis.Normed.Group.Uniform
/-- **Alias** of the reverse direction of `lipschitzWith_neg_iff`. -/
LipschitzWith.neg : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedAddCommGroup E] [inst_1 : PseudoEMetricSpace α] {K : NNReal}
  {f : α → E}, LipschitzWith K f → LipschitzWith K (-f)
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_univ_getElem : ∀ {M : Type u_2} [inst : AddCommMonoid M] (l : List M), ∑ i, l[↑i] = l.sum
-- Lean.Server.FileWorker.Utils
Lean.Server.FileWorker.RpcSession.mk.sizeOf_spec : ∀ (objects : Lean.Server.RpcObjectStore) (expireTime : ℕ),
  sizeOf { objects := objects, expireTime := expireTime } = 1 + sizeOf objects + sizeOf expireTime
-- Mathlib.Analysis.SpecialFunctions.Arsinh
Real.arsinh_eq_zero_iff : ∀ {x : ℝ}, Real.arsinh x = 0 ↔ x = 0
-- Mathlib.CategoryTheory.Core
CategoryTheory.Equivalence.core_inverse_map_iso_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : C ≌ D) {X Y : CategoryTheory.Core D} (f : X ⟶ Y), (E.core.inverse.map f).iso.inv = E.inverse.map f.iso.inv
-- Mathlib.Order.PrimeIdeal
Order.Ideal.PrimePair.I : {P : Type u_2} → [inst : Preorder P] → Order.Ideal.PrimePair P → Order.Ideal P
-- Std.Internal.Do.WP.Conjunctive
/-- `Id` is conjunctive: its `wp` is evaluation at the result.  -/
Std.Internal.Do.Id.instWPConjunctive : ∀ {α : Type u}, Std.Internal.Do.WPConjunctive (Id α) α Prop EPost⟨⟩
-- Lean.Elab.Tactic.BuiltinTactic
/-- Evaluates an `intro` argument.
 -/
_private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalIntro.evalArg : Lean.Term → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Combinatorics.Optimization.ValuedCSP
/-- Function `f` has Max-Cut property at labels `a` and `b` when `argmin f` is exactly
`{ ![a, b], ![b, a] }`.  -/
Function.HasMaxCutPropertyAt : {D : Type u_1} → {C : Type u_2} → [PartialOrder C] → ((Fin 2 → D) → C) → D → D → Prop
-- Mathlib.Order.BourbakiWitt
ChainCompletePartialOrder.instOfCompleteLattice : {α : Type u_1} → [CompleteLattice α] → ChainCompletePartialOrder α
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.beth_zero : Cardinal.beth 0 = Cardinal.aleph0
-- Mathlib.CategoryTheory.Localization.SmallHom
CategoryTheory.LocalizerMorphism.smallHomMap_comp : ∀ {C₁ : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C₁] {W₁ : CategoryTheory.MorphismProperty C₁} {C₂ : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₂ : CategoryTheory.MorphismProperty C₂}
  (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) {X Y Z : C₁}
  [inst_2 : CategoryTheory.Localization.HasSmallLocalizedHom W₁ X Y]
  [inst_3 : CategoryTheory.Localization.HasSmallLocalizedHom W₁ Y Z]
  [inst_4 : CategoryTheory.Localization.HasSmallLocalizedHom W₁ X Z]
  [inst_5 : CategoryTheory.Localization.HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)]
  [inst_6 : CategoryTheory.Localization.HasSmallLocalizedHom W₂ (Φ.functor.obj Y) (Φ.functor.obj Z)]
  [inst_7 : CategoryTheory.Localization.HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Z)]
  (f : CategoryTheory.Localization.SmallHom W₁ X Y) (g : CategoryTheory.Localization.SmallHom W₁ Y Z),
  Φ.smallHomMap (f.comp g) = (Φ.smallHomMap f).comp (Φ.smallHomMap g)
-- Lean.MetavarContext
Lean.MetavarContext.MkBinding.Context.preserveOrder : Lean.MetavarContext.MkBinding.Context → Bool
-- Mathlib.Geometry.RingedSpace.OpenImmersion
/-- Two open immersions with equal range is isomorphic.  -/
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoOfRangeEq : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : AlgebraicGeometry.PresheafedSpace C} →
      (f : X ⟶ Z) →
        [hf : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] →
          (g : Y ⟶ Z) →
            [AlgebraicGeometry.PresheafedSpace.IsOpenImmersion g] →
              Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base) =
                  Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base) →
                (X ≅ Y)
-- Mathlib.Order.SupClosed
inf_mem_infClosure : ∀ {α : Type u_3} [inst : SemilatticeInf α] {s : Set α} {a b : α}, a ∈ s → b ∈ s → a ⊓ b ∈ infClosure s
-- Mathlib.Data.EReal.Inv
EReal.sign_eq_and_abs_eq_iff_eq : ∀ {x y : EReal}, x.abs = y.abs ∧ SignType.sign x = SignType.sign y ↔ x = y
-- Mathlib.Geometry.Manifold.Instances.Icc
Homeomorph.pointReflection.eq_1 : ∀ {V : Type u_4} {P : Type u_5} [inst : AddGroup V] [inst_1 : TopologicalSpace V] [inst_2 : AddTorsor V P]
  [inst_3 : TopologicalSpace P] [inst_4 : IsTopologicalAddTorsor P] (p : P),
  Homeomorph.pointReflection p = (Homeomorph.constVSub p).trans (Homeomorph.vaddConst p)
-- Init.Data.List.SplitOn.Basic
_private.Init.Data.List.SplitOn.Basic.0.List.splitOnPTR.go.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Array α → Array (List α) → Sort u_2) (acc : Array α) (r : Array (List α))
  (h_1 : (acc : Array α) → (r : Array (List α)) → motive [] acc r)
  (h_2 : (a : α) → (t : List α) → (acc : Array α) → (r : Array (List α)) → motive (a :: t) acc r),
  (match [], acc, r with
    | [], acc, r => h_1 acc r
    | a :: t, acc, r => h_2 a t acc r) =
    h_1 acc r
-- Init.Data.BitVec.Lemmas
BitVec.smulOverflow.eq_1 : ∀ {w : ℕ} (x y : BitVec w),
  x.smulOverflow y = (decide (x.toInt * y.toInt ≥ 2 ^ (w - 1)) || decide (x.toInt * y.toInt < -2 ^ (w - 1)))
-- Init.Data.Option.Lemmas
Option.orElse_apply : ∀ {α : Type u_1} {o : Option α} {o' : Unit → Option α}, (o <|> o' ()) = o.orElse o'
-- Mathlib.Data.Multiset.MapFold
Multiset.coe_foldr : ∀ {α : Type u_1} {β : Type v} (f : α → β → β) [inst : LeftCommutative f] (b : β) (l : List α),
  Multiset.foldr f b ↑l = List.foldr f b l
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.hom_ext₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {F G : CategoryTheory.ComposableArrows C 0}
  {φ φ' : F ⟶ G},
  CategoryTheory.ComposableArrows.app' φ 0 CategoryTheory.ComposableArrows.homMk₀._proof_1 =
      CategoryTheory.ComposableArrows.app' φ' 0 CategoryTheory.ComposableArrows.homMk₀._proof_1 →
    φ = φ'
-- Mathlib.RingTheory.HahnSeries.Lex
HahnSeries.finiteArchimedeanClassOrderIso_apply : ∀ {Γ : Type u_1} {R : Type u_2} [inst : LinearOrder Γ] [inst_1 : LinearOrder R] [inst_2 : AddCommGroup R]
  [inst_3 : IsOrderedAddMonoid R] [inst_4 : Archimedean R] [inst_5 : Nontrivial R] {x : Lex (HahnSeries Γ R)}
  (h : x ≠ 0), ↑((HahnSeries.finiteArchimedeanClassOrderIso Γ R) (FiniteArchimedeanClass.mk x h)) = (ofLex x).orderTop
-- Mathlib.LinearAlgebra.PerfectPairing.Basic
Submodule.map_dualCoannihilator_linearEquiv_flip : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [Module.IsReflexive R M] (e : N ≃ₗ[R] Module.Dual R M)
  (p : Submodule R (Module.Dual R M)),
  Submodule.map (↑e).flip p.dualCoannihilator = (Submodule.map (↑e.symm) p).dualAnnihilator
-- Mathlib.Data.Nat.Init
Nat.decreasingInduction_trans : ∀ {m n k : ℕ} {motive : (m : ℕ) → m ≤ k → Sort u_1} (hmn : m ≤ n) (hnk : n ≤ k)
  (of_succ : (k_1 : ℕ) → (h : k_1 < k) → motive (k_1 + 1) h → motive k_1 ⋯) (self : motive k ⋯),
  Nat.decreasingInduction of_succ self ⋯ =
    Nat.decreasingInduction (fun x x_1 => of_succ x ⋯) (Nat.decreasingInduction of_succ self hnk) hmn
-- Mathlib.Data.Ordmap.Ordset
Ordnode.erase.eq_1 : ∀ {α : Type u_1} [inst : LE α] [inst_1 : DecidableLE α] (x : α), Ordnode.erase x Ordnode.nil = Ordnode.nil
-- Mathlib.Algebra.Group.Ext
RightCancelMonoid.ext : ∀ {M : Type u} ⦃m₁ m₂ : RightCancelMonoid M⦄, HMul.hMul = HMul.hMul → m₁ = m₂
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey!_eq_minKeyD_default : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.minKey! = t.minKeyD default
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.type_toType : ∀ (o : Ordinal.{u_1}), (Ordinal.type fun x1 x2 => x1 < x2) = o
-- Mathlib.Algebra.Polynomial.Mirror
Polynomial.natTrailingDegree_mul_mirror : ∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R) [NoZeroDivisors R],
  (p * p.mirror).natTrailingDegree = 2 * p.natTrailingDegree
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKeyD_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool} {k fallback : α},
  (Std.DTreeMap.filter f t).getKeyD k fallback =
    ((t.getKey? k).pfilter fun x h' => f x (Std.DTreeMap.Const.get t x ⋯)).getD fallback
-- Mathlib.Combinatorics.Matroid.Sum
Matroid.sum'_isBasis_iff : ∀ {α : Type u_1} {ι : Type u_2} {M : ι → Matroid α} {I X : Set (ι × α)},
  (Matroid.sum' M).IsBasis I X ↔ ∀ (i : ι), (M i).IsBasis (Prod.mk i ⁻¹' I) (Prod.mk i ⁻¹' X)
-- Mathlib.CategoryTheory.Pi.Basic
/-- Assemble an `I`-indexed family of natural transformations into a single natural transformation.
 -/
CategoryTheory.NatTrans.pi : {I : Type w₀} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      {D : I → Type u₂} →
        [inst_1 : (i : I) → CategoryTheory.Category.{v₂, u₂} (D i)] →
          {F G : (i : I) → CategoryTheory.Functor (C i) (D i)} →
            ((i : I) → F i ⟶ G i) → (CategoryTheory.Functor.pi F ⟶ CategoryTheory.Functor.pi G)
-- Mathlib.Algebra.RingQuot
/-- The universal ring homomorphism from `B ⧸ Ideal.ofRel r` to `RingQuot r`.  -/
RingQuot.idealQuotientToRingQuot : {B : Type uR} → [inst : CommRing B] → (r : B → B → Prop) → B ⧸ Ideal.ofRel r →+* RingQuot r
-- Mathlib.Order.Bounds.Basic
/-- A set `s` is not bounded above if and only if for each `x` there exists `y ∈ s` that is greater
than `x`. A version for preorders is called `not_bddAbove_iff'`.  -/
not_bddAbove_iff : ∀ {α : Type u_4} [inst : LinearOrder α] {s : Set α}, ¬BddAbove s ↔ ∀ (x : α), ∃ y ∈ s, x < y
-- Mathlib.RingTheory.RegularLocalRing.Defs
IsRegularLocalRing.iff_finrank_cotangentSpace : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsLocalRing R] [IsNoetherianRing R],
  IsRegularLocalRing R ↔ ↑(Module.finrank (IsLocalRing.ResidueField R) (IsLocalRing.CotangentSpace R)) = ringKrullDim R
-- Mathlib.MeasureTheory.Measure.FiniteMeasureProd
MeasureTheory.FiniteMeasure.map_fst_prod : ∀ {α : Type u_1} [inst : MeasurableSpace α] {β : Type u_2} [inst_1 : MeasurableSpace β]
  (μ : MeasureTheory.FiniteMeasure α) (ν : MeasureTheory.FiniteMeasure β), (μ.prod ν).map Prod.fst = ν Set.univ • μ