mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.OpenPartialHomeomorph.Composition
Homeomorph.transOpenPartialHomeomorph_target : ∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (e : X ≃ₜ Y) (f' : OpenPartialHomeomorph Y Z),
  (e.transOpenPartialHomeomorph f').target = f'.target
-- Mathlib.CategoryTheory.Filtered.FinallySmall
CategoryTheory.FinallySmall.exists_of_isFiltered : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFiltered C]
  [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.FinallySmall C],
  ∃ D x, ∃ (_ : CategoryTheory.IsFiltered D), ∃ F, F.Final
-- Mathlib.CategoryTheory.MorphismProperty.Composition
/-- Given `app : Π X, F₁.obj X ⟶ F₂.obj X` where `F₁` and `F₂` are two functors,
this is the `MorphismProperty C` satisfied by the morphisms in `C` with respect
to which `app` is natural.  -/
CategoryTheory.MorphismProperty.naturalityProperty : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        {F₁ F₂ : CategoryTheory.Functor C D} → ((X : C) → F₁.obj X ⟶ F₂.obj X) → CategoryTheory.MorphismProperty C
-- Mathlib.Topology.ContinuousMap.Star
ContinuousMap.instStarModule : ∀ {R : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : Star R] [inst_3 : Star β] [inst_4 : SMul R β] [StarModule R β] [inst_6 : ContinuousStar β]
  [inst_7 : ContinuousConstSMul R β], StarModule R C(α, β)
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
CategoryTheory.TransportEnrichment.forgetEnrichmentEquivInverse_map : ∀ {V : Type u'} [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] {W : Type u''}
  [inst_2 : CategoryTheory.Category.{v'', u''} W] [inst_3 : CategoryTheory.MonoidalCategory W]
  (F : CategoryTheory.Functor V W) [inst_4 : F.LaxMonoidal] (D : Type u) [inst_5 : CategoryTheory.EnrichedCategory V D]
  (e :
    (v : V) →
      (CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v) ≃
        (CategoryTheory.MonoidalCategoryStruct.tensorUnit W ⟶ F.obj v))
  (h :
    ∀ (v : V) (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v),
      (e v) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (F.map f))
  {X Y : CategoryTheory.ForgetEnrichment W (CategoryTheory.TransportEnrichment F D)} (f : X ⟶ Y),
  (CategoryTheory.TransportEnrichment.forgetEnrichmentEquivInverse F D e h).map f =
    CategoryTheory.ForgetEnrichment.homOf V
      ((e (CategoryTheory.ForgetEnrichment.to W X ⟶[V] CategoryTheory.ForgetEnrichment.to W Y)).symm
        (CategoryTheory.ForgetEnrichment.homTo W f))
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintTooltip.markdown.inj : ∀ {markup markup_1 : Lean.Lsp.MarkupContent},
  Lean.Lsp.InlayHintTooltip.markdown markup = Lean.Lsp.InlayHintTooltip.markdown markup_1 → markup = markup_1
-- Mathlib.Topology.MetricSpace.HausdorffDistance
Metric.exists_real_pos_lt_infEDist_of_notMem_closure : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {E : Set α},
  x ∉ closure E → ∃ ε, 0 < ε ∧ ENNReal.ofReal ε < Metric.infEDist x E
-- Lean.Data.Json.Printer
_private.Lean.Data.Json.Printer.0.Lean.Json.CompressWorkItemKind.objectField.sizeOf_spec : sizeOf Lean.Json.CompressWorkItemKind.objectField✝ = 1
-- Mathlib.Algebra.Ring.Parity
Odd.pow : ∀ {α : Type u_2} [inst : Semiring α] {a : α} {n : ℕ}, Odd a → Odd (a ^ n)
-- Mathlib.Topology.Order.Compact
IsCompact.isGreatest_sSup : ∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [ClosedIciTopology α]
  {s : Set α}, IsCompact s → s.Nonempty → IsGreatest s (sSup s)
-- Init.Data.List.Sublist
List.IsPrefix.eq_of_length_le : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <+: l₂ → l₂.length ≤ l₁.length → l₁ = l₂
-- Mathlib.Data.EReal.Basic
EReal.coe_nnreal_eq_coe_real : ∀ (x : NNReal), ↑↑x = ↑↑x
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
/-- The integral closure of a field in a commutative domain is always a field.  -/
IsIntegralClosure.isField : ∀ {R : Type u_1} (A : Type u_2) {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R B] [inst_4 : Algebra A B] [IsIntegralClosure A R B] [inst_6 : Algebra R A] [IsScalarTower R A B]
  [IsDomain A], IsField R → IsField A
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instInhabitedEMatchDiagSource : Inhabited Lean.Meta.Grind.EMatchDiagSource
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMonObj.ofRepresentableBy_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X : C) (F : CategoryTheory.Functor Cᵒᵖ AddMonCat) (α : (F.comp (CategoryTheory.forget AddMonCat)).RepresentableBy X),
  CategoryTheory.AddMonObj.zero = α.homEquiv'.symm 0
-- Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox
MeasureTheory.LocallyIntegrable.exists_contDiff_dist_le_of_forall_mem_ball_dist_le : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [CompleteSpace F] {f : E → F} {ε : ℝ}
  [inst_6 : MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure],
  MeasureTheory.LocallyIntegrable f μ →
    0 < ε →
      ∃ g, ContDiff ℝ (↑⊤) g ∧ ∀ (a : E) (δ : ℝ), (∀ x ∈ Metric.ball a ε, dist (f x) (f a) ≤ δ) → dist (g a) (f a) ≤ δ
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
/-- Let `e : S ≃ I` be an additive isomorphism (therefore a `ℤ`-linear equiv).
Then an alternative way to compute the norm of `I` is given by taking the determinant of `e`.
See `natAbs_det_basis_change` for a more familiar formulation of this result.  -/
Ideal.natAbs_det_equiv : ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : IsDedekindDomain S] [inst_2 : Module.Free ℤ S] [Module.Finite ℤ S]
  (I : Ideal S) {E : Type u_2} [inst_4 : EquivLike E S ↥I] [inst_5 : AddEquivClass E S ↥I] (e : E),
  (LinearMap.det (↑ℤ (Submodule.subtype I) ∘ₗ (↑e).toIntLinearMap)).natAbs = Ideal.absNorm I
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
/-- The identity `CatCospanTransform`  -/
CategoryTheory.Limits.CatCospanTransform.id : {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) → CategoryTheory.Limits.CatCospanTransform F G F G
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.OplaxRightLinear.δᵣ_naturality_left : ∀ {D : Type u_1} {D' : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} D}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D'} (F : CategoryTheory.Functor D D') {C : Type u_3}
  {inst_2 : CategoryTheory.Category.{v_3, u_3} C} {inst_3 : CategoryTheory.MonoidalCategory C}
  {inst_4 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D}
  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D'} [self : F.OplaxRightLinear C] {d d' : D}
  (f : d ⟶ d') (c : C),
  CategoryTheory.CategoryStruct.comp
      (F.map (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f c))
      (CategoryTheory.Functor.OplaxRightLinear.δᵣ F d' c) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxRightLinear.δᵣ F d c)
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft (F.map f) c)
-- Mathlib.Algebra.Category.ModuleCat.Semi
linearEquivIsoModuleIsoₛ_inv : ∀ {R : Type u} [inst : Semiring R] {X Y : Type u} [inst_1 : AddCommMonoid X] [inst_2 : AddCommMonoid Y]
  [inst_3 : Module R X] [inst_4 : Module R Y], linearEquivIsoModuleIsoₛ.inv = TypeCat.ofHom fun i => i.toLinearEquivₛ
-- Mathlib.Geometry.Manifold.Immersion
Manifold.IsImmersionAtOfComplement.trans_F : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5} {F' : Type u_6}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F]
  [inst_7 : NormedAddCommGroup F'] [inst_8 : NormedSpace 𝕜 F'] {H : Type u_7} [inst_9 : TopologicalSpace H]
  {G : Type u_9} [inst_10 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G}
  {M : Type u_11} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H M] {N : Type u_13}
  [inst_13 : TopologicalSpace N] [inst_14 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M},
  Manifold.IsImmersionAtOfComplement F I J n f x → ∀ (e : F ≃L[𝕜] F'), Manifold.IsImmersionAtOfComplement F' I J n f x
-- Mathlib.Topology.MetricSpace.Defs
dist_pos : ∀ {γ : Type w} [inst : MetricSpace γ] {x y : γ}, 0 < dist x y ↔ x ≠ y
-- Mathlib.Topology.CompactOpen
ContinuousAt.compCM : ∀ {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] [LocallyCompactPair Y Z] {X' : Type u_6} [inst_4 : TopologicalSpace X'] {a : X'}
  {g : X' → C(Y, Z)} {f : X' → C(X, Y)},
  ContinuousAt g a → ContinuousAt f a → ContinuousAt (fun x => (g x).comp (f x)) a
-- Init.Data.String.Bootstrap
String.Internal.offsetOfPos : String → String.Pos.Raw → ℕ
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.isScalarTower : ∀ {R : Type u_1} {M : Type u_4} {N : Type u_5} {O : Type u_6} [inst : Semiring R] [inst_1 : SMulZeroClass N R]
  [inst_2 : SMulZeroClass O R] [inst_3 : SMul N O] [IsScalarTower N O R], IsScalarTower N O (MonoidAlgebra R M)
-- Mathlib.CategoryTheory.ObjectProperty.ContainsZero
CategoryTheory.ObjectProperty.prop_of_isZero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.ContainsZero]
  [P.IsClosedUnderIsomorphisms] {Z : C}, CategoryTheory.Limits.IsZero Z → P Z
-- Mathlib.Data.Finset.Insert
/-- Split the added element of cons off a Pi type.  -/
Finset.consPiProd : {α : Type u_1} →
  {s : Finset α} →
    {a : α} →
      (f : α → Type u_3) → (has : a ∉ s) → ((i : α) → i ∈ Finset.cons a s has → f i) → f a × ((i : α) → i ∈ s → f i)
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four
/-- Variant of the first 4-lemma for complexes of any size  -/
CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {n k : ℕ}
  (h : k + 3 ≤ n) {R₁ R₂ : CategoryTheory.ComposableArrows C n},
  R₁.Exact →
    R₂.Exact →
      ∀ (φ : R₁ ⟶ R₂) (k₀ k₁ k₂ k₃ : ℕ) (hk₀ : k₀ = k) (hk₁ : k₁ = k + 1) (hk₂ : k₂ = k + 2) (hk₃ : k₃ = k + 3),
        CategoryTheory.Epi (CategoryTheory.ComposableArrows.app' φ k₀ ⋯) →
          CategoryTheory.Mono (CategoryTheory.ComposableArrows.app' φ k₁ ⋯) →
            CategoryTheory.Mono (CategoryTheory.ComposableArrows.app' φ k₃ ⋯) →
              CategoryTheory.Mono (CategoryTheory.ComposableArrows.app' φ k₂ ⋯)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_add_const_Iic : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b : α),
  (fun x => x + a) '' Set.Iic b = Set.Iic (b + a)
-- Mathlib.Topology.MetricSpace.Infsep
Set.einfsep_triple : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {x y z : α},
  x ≠ y → y ≠ z → x ≠ z → {x, y, z}.einfsep = min (min (edist x y) (edist x z)) (edist y z)
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
/-- Restricting to a larger box does not change the set of boxes. We cannot claim equality
of prepartitions because they have different types.  -/
BoxIntegral.Prepartition.restrict_boxes_of_le : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I), I ≤ J → (π.restrict J).boxes = π.boxes
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Precoverage.instTop : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → Top (CategoryTheory.Precoverage C)
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
MvPolynomial.IsWeightedHomogeneous.weightedHomogeneousComponent_same : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] {w : σ → M} {m : M}
  {p : MvPolynomial σ R},
  MvPolynomial.IsWeightedHomogeneous w p m → (MvPolynomial.weightedHomogeneousComponent w m) p = p
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.GoodProducts.union_succ : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}},
  Profinite.NobelingProof.contained C (Order.succ o) →
    ∀ (ho : o < Ordinal.type fun x1 x2 => x1 < x2),
      Profinite.NobelingProof.GoodProducts C =
        Profinite.NobelingProof.GoodProducts
            (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o) ∪
          Profinite.NobelingProof.GoodProducts.MaxProducts C ho
-- Mathlib.NumberTheory.ModularForms.SlashActions
/-- The weight `k` action of `GL (Fin 2) ℝ` on functions `f : ℍ → ℂ`. Invoking this directly is
deprecated; it should always be used via the `SlashAction` instance.  -/
_private.Mathlib.NumberTheory.ModularForms.SlashActions.0.ModularForm.privateSlash : ℤ → GL (Fin 2) ℝ → (UpperHalfPlane → ℂ) → UpperHalfPlane → ℂ
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.Equiv.map : ∀ {α₁ α₂ β γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : LawfulMonad m] [inst_2 : Std.Iterator α₁ m β]
  [inst_3 : Std.Iterator α₂ m β] {f : β → γ} {ita : Std.IterM m β} {itb : Std.IterM m β},
  ita.Equiv itb → (Std.IterM.map f ita).Equiv (Std.IterM.map f itb)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CallHierarchyOutgoingCallsParams.mk.injEq : ∀ (item item_1 : Lean.Lsp.CallHierarchyItem), ({ item := item } = { item := item_1 }) = (item = item_1)
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- **Continuity from above**:
the measure of the intersection of an antitone family of measurable sets
indexed by a type with countably generated `atTop` filter
is equal to the infimum of the measures.  -/
Antitone.measure_iInter : ∀ {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : Preorder ι]
  [IsDirectedOrder ι] [Filter.atTop.IsCountablyGenerated] {s : ι → Set α},
  Antitone s → (∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ) → (∃ i, μ (s i) ≠ ⊤) → μ (⋂ i, s i) = ⨅ i, μ (s i)
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.coe_mul : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  [inst_3 : Algebra R A] (f g : A →A[R] A), ⇑(f * g) = ⇑f ∘ ⇑g
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
ContinuousAt.clm_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {G : Type u_4} [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {X : Type u_5}
  [inst_7 : TopologicalSpace X] {g : X → F →L[𝕜] G} {f : X → E →L[𝕜] F} {x : X},
  ContinuousAt g x → ContinuousAt f x → ContinuousAt (fun x => g x ∘SL f x) x
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.reduction.eq_1 : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra R K] [inst_5 : IsFractionRing R K] (W : WeierstrassCurve K)
  [inst_6 : WeierstrassCurve.IsMinimal R W],
  WeierstrassCurve.reduction R W = (WeierstrassCurve.integralModel R W).map (IsLocalRing.residue R)
-- Lean.Util.FoldConsts
Lean.Expr.FoldConstsImpl.State : Type
-- Mathlib.CategoryTheory.Functor.TwoSquare
/-- When composing 2-squares which form a diagram of grid, composing horizontally first yields the
same result as composing vertically first.  -/
CategoryTheory.TwoSquare.hCompVCompHComp : ∀ {C₁ : Type u₁} {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₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} {C₅ : Type u₅} {C₆ : Type u₆} {C₇ : Type u₇}
  {C₈ : Type u₈} [inst_4 : CategoryTheory.Category.{v₅, u₅} C₅] [inst_5 : CategoryTheory.Category.{v₆, u₆} C₆]
  [inst_6 : CategoryTheory.Category.{v₇, u₇} C₇] [inst_7 : CategoryTheory.Category.{v₈, u₈} C₈]
  {T' : CategoryTheory.Functor C₂ C₅} {R' : CategoryTheory.Functor C₅ C₆} {B' : CategoryTheory.Functor C₄ C₆}
  {L' : CategoryTheory.Functor C₃ C₇} {R'' : CategoryTheory.Functor C₄ C₈} {B'' : CategoryTheory.Functor C₇ C₈}
  {C₉ : Type u₉} [inst_8 : CategoryTheory.Category.{v₉, u₉} C₉] {R₃ : CategoryTheory.Functor C₆ C₉}
  {B₃ : CategoryTheory.Functor C₈ C₉} (w₁ : CategoryTheory.TwoSquare T L R B) (w₂ : CategoryTheory.TwoSquare T' R R' B')
  (w₃ : CategoryTheory.TwoSquare B L' R'' B'') (w₄ : CategoryTheory.TwoSquare B' R'' R₃ B₃),
  (w₁.hComp w₂).vComp (w₃.hComp w₄) = (w₁.vComp w₃).hComp (w₂.vComp w₄)
-- Mathlib.Data.Int.Init
Int.div_lt_div_iff_of_dvd_of_pos : ∀ {a b c d : ℤ}, 0 < b → 0 < d → b ∣ a → d ∣ c → (a / b < c / d ↔ d * a < c * b)
-- Mathlib.Control.Monad.Cont
ReaderT.callCC.eq_1 : ∀ {m : Type u → Type v} {ε : Type u} [inst : MonadCont m] {α β : Type u}
  (f : MonadCont.Label α (ReaderT ε m) β → ReaderT ε m α),
  ReaderT.callCC f = ReaderT.mk fun r => MonadCont.callCC fun f' => (f (ReaderT.mkLabel ε f')).run r
-- Mathlib.Analysis.Fourier.Notation
FourierTransform.fourierInv_neg : ∀ {E : Type u_3} {F : Type u_4} [inst : AddCommGroup E] [inst_1 : AddCommGroup F] [inst_2 : FourierTransformInv E F]
  [FourierInvAdd E F] (f : E), FourierTransformInv.fourierInv (-f) = -FourierTransformInv.fourierInv f
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Matrix.IsHyperbolic.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : Preorder R] (m : Matrix (Fin 2) (Fin 2) R),
  m.IsHyperbolic = (0 < m.discr)
-- Mathlib.Geometry.Manifold.Algebra.Monoid
contMDiff_add_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {G : Type u_4} [inst_4 : Add G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [ContMDiffAdd I n G]
  {a : G}, ContMDiff I I n fun x => a + x
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- Eta-expanded form of `ContDiff.div` -/
ContDiff.fun_div : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f g : E → 𝕜} {n : WithTop ℕ∞},
  ContDiff 𝕜 n f → ContDiff 𝕜 n g → (∀ (x : E), g x ≠ 0) → ContDiff 𝕜 n fun i => f i / g i
-- Std.Sync.Basic
/-- `AtomicT α m` is the monad that can be atomically executed inside mutual exclusion primitives like
`Mutex α` with outside monad `m`.
The action has access to the state `α` of the mutex (via `get` and `set`).
 -/
Std.AtomicT : Type → (Type → Type) → Type → Type
-- Mathlib.Data.TwoPointing
instDecidableEqTwoPointing : {α : Type u_3} → [DecidableEq α] → DecidableEq (TwoPointing α)
-- Lean.Data.Json.Elab
/-- Json false value syntax.  -/
Lean.Json.jsonFalse : Lean.ParserDescr
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.LiftActionCoreResult.closed.sizeOf_spec : sizeOf Lean.Elab.Tactic.Grind.LiftActionCoreResult.closed = 1
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddMod.instCategory : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
            {A : C} →
              [inst_4 : CategoryTheory.AddMonObj A] →
                CategoryTheory.Category.{v₂, max u₂ v₂} (CategoryTheory.AddMod D A)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.ball_mem_nhds : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x : α) {ε : ℝ}, 0 < ε → Metric.ball x ε ∈ nhds x
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeAddGroup.instNontrivialOfNonempty : ∀ {α : Type u_1} [Nonempty α], Nontrivial (FreeAddGroup α)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.zero_lt_getElem!_toArray_ric_iff : ∀ {n i : ℕ}, 0 < (*...=n).toArray[i]! ↔ i ≤ n ∧ 0 < i
-- Batteries.Tactic.Lint.Simp
/-- Returns the list of elements in the trie.  -/
_private.Batteries.Tactic.Lint.Simp.0.Lean.Meta.DiscrTree.elements.trieElements : {α : Type} → Array α → Lean.Meta.DiscrTree.Trie α → Array α
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.hasReflexiveCoequalizer_iff_hasCoequalizer : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C),
  CategoryTheory.Limits.HasColimit F ↔
    CategoryTheory.Limits.HasCoequalizer (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left)
      (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right)
-- Init.Notation
/-- The default priority `default = 1000`, which is used when no priority is set.  -/
prioDefault : Lean.ParserDescr
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.natCast_def : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddZeroClass M] (n : ℕ), ↑n = AddMonoidAlgebra.single 0 ↑n
-- Std.Time.Format.Modifier
/-- `A`: Millisecond of day (e.g., 1234).
 -/
Std.Time.Modifier.A : Std.Time.Number → Std.Time.Modifier
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_of_containsKey_insertEntry : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k},
  Std.Internal.List.containsKey a (Std.Internal.List.insertEntry k v l) = true →
    (k == a) = false → Std.Internal.List.containsKey a l = true
-- Mathlib.NumberTheory.LSeries.Convergence
/-- If `f` is `O(1)`, then the abscissa of absolute convergence of `f` is bounded above by `1`.  -/
LSeries.abscissaOfAbsConv_le_one_of_isBigO_one : ∀ {f : ℕ → ℂ}, (f =O[Filter.atTop] fun x => 1) → LSeries.abscissaOfAbsConv f ≤ 1
-- Mathlib.Algebra.DirectSum.Internal
DirectSum.coe_mul_of_apply_of_mem_zero : ∀ {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [inst : DecidableEq ι] [inst_1 : Semiring R] [inst_2 : SetLike σ R]
  [inst_3 : AddSubmonoidClass σ R] (A : ι → σ) [inst_4 : AddMonoid ι] [inst_5 : SetLike.GradedMonoid A]
  (r : DirectSum ι fun i => ↥(A i)) (r' : ↥(A 0)) (j : ι),
  ↑((r * (DirectSum.of (fun i => ↥(A i)) 0) r') j) = ↑(r j) * ↑r'
-- Mathlib.Algebra.Category.Grp.ForgetCorepresentable
/-- The forget functor `GrpCat.{u} ⥤ Type u` is corepresentable.  -/
GrpCat.coyonedaObjIsoForget : CategoryTheory.coyoneda.obj (Opposite.op (GrpCat.of (ULift.{u, 0} (Multiplicative ℤ)))) ≅ CategoryTheory.forget GrpCat
-- Mathlib.CategoryTheory.Limits.IndYoneda
/-- Ind-Yoneda lemma: morphisms from colimit of yoneda of diagram `D` to `F` is limit of `F`
evaluated at `D`. This version is for covariant diagrams, see `colimitYonedaHomIsoLimit'` for a
contravariant version.  -/
CategoryTheory.Limits.colimitYonedaHomIsoLimitOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    {I : Type v₁} →
      [inst_1 : CategoryTheory.Category.{v₂, v₁} I] →
        (D : CategoryTheory.Functor I C) →
          (F : CategoryTheory.Functor Cᵒᵖ (Type u₂)) →
            [inst_2 : CategoryTheory.Limits.HasColimit (D.comp CategoryTheory.yoneda)] →
              [inst_3 : CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))] →
                (CategoryTheory.Limits.colimit (D.comp CategoryTheory.yoneda) ⟶ F) ≅
                  CategoryTheory.Limits.limit (D.op.comp (F.comp CategoryTheory.uliftFunctor.{u₁, u₂}))
-- Mathlib.Algebra.Algebra.Operations
/-- `Submonoid.map` as a `RingHom`, when applied to an `AlgHom`.  -/
Submodule.mapHom : {R : Type u} →
  [inst : CommSemiring R] →
    {A : Type v} →
      [inst_1 : Semiring A] →
        [inst_2 : Algebra R A] →
          {A' : Type u_1} →
            [inst_3 : Semiring A'] → [inst_4 : Algebra R A'] → (A →ₐ[R] A') → Submodule R A →+* Submodule R A'