mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Kernel.Disintegration.Basic
ProbabilityTheory.Kernel.disintegrate : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mΩ : MeasurableSpace Ω} (κ : ProbabilityTheory.Kernel α (β × Ω)) (κCond : ProbabilityTheory.Kernel (α × β) Ω)
  [κ.IsCondKernel κCond], κ.fst.compProd κCond = κ
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
ContinuousLinearMap.commIsometry_comp_lTensor_comp_commIsometry_eq : ∀ {𝕜 : 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] (g : E →L[𝕜] F),
  ↑↑(TensorProduct.commIsometry 𝕜 F G) ∘SL ContinuousLinearMap.rTensor G g ∘SL ↑↑(TensorProduct.commIsometry 𝕜 G E) =
    ContinuousLinearMap.lTensor G g
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryLaxFunctor.mk'_mapComp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (S : CategoryTheory.StrictlyUnitaryLaxFunctorCore B C) {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  (CategoryTheory.StrictlyUnitaryLaxFunctor.mk' S).mapComp f g = S.mapComp f g
-- Mathlib.Control.Fix
Part.Fix.approx.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) → (a : α) → Part (β a)) (i : ℕ),
  Part.Fix.approx f i.succ = f (Part.Fix.approx f i)
-- Mathlib.Order.CompleteSublattice
CompleteSublattice.instCompleteLattice : {α : Type u_1} → [inst : CompleteLattice α] → {L : CompleteSublattice α} → CompleteLattice ↥L
-- Mathlib.Analysis.Complex.ReImTopology
Complex.interior_reProdIm : ∀ (s t : Set ℝ), interior (s ×ℂ t) = interior s ×ℂ interior t
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.tensorHom_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {X₁ X₂ Y₁ Y₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)
      (CategoryTheory.SemiCartesianMonoidalCategory.snd X₂ Y₂) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd X₁ Y₁) g
-- Init.System.IO
/-- Runs `act` in a separate `Task`, with priority `prio`. Because `EIO ε` actions may throw an exception
of type `ε`, the result of the task is an `Except ε α`.

Running the resulting `IO` action causes the task to be started eagerly. Pure accesses to the `Task`
do not influence the impure `act`.

Unlike pure tasks created by `Task.spawn`, tasks created by this function will run even if the last
reference to the task is dropped. The `act` should explicitly check for cancellation via
`IO.checkCanceled` if it should be terminated or otherwise react to the last reference being
dropped.
 -/
EIO.asTask : {ε α : Type} → EIO ε α → optParam Task.Priority Task.Priority.default → BaseIO (Task (Except ε α))
-- Init.Data.Float.Model.Float32
/-- Compute the product of two `Float32.Model`.
 -/
Float32.Model.mul : Float32.Model → Float32.Model → Float32.Model
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
map_sum : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] {G : Type u_7}
  [inst_2 : FunLike G M N] [AddMonoidHomClass G M N] (g : G) (f : ι → M) (s : Finset ι),
  g (∑ x ∈ s, f x) = ∑ x ∈ s, g (f x)
-- Mathlib.CategoryTheory.Localization.Bifunctor
CategoryTheory.Localization.instLifting₂Lift₂ : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D₁ : Type u_3} →
      {D₂ : Type u_4} →
        {E : Type u_5} →
          [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
            [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁] →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] →
                  [inst_4 : CategoryTheory.Category.{v_5, u_5} E] →
                    (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ E)) →
                      {W₁ : CategoryTheory.MorphismProperty C₁} →
                        {W₂ : CategoryTheory.MorphismProperty C₂} →
                          (hF : W₁.IsInvertedBy₂ W₂ F) →
                            (L₁ : CategoryTheory.Functor C₁ D₁) →
                              (L₂ : CategoryTheory.Functor C₂ D₂) →
                                [inst_5 : L₁.IsLocalization W₁] →
                                  [inst_6 : L₂.IsLocalization W₂] →
                                    [inst_7 : W₁.ContainsIdentities] →
                                      [inst_8 : W₂.ContainsIdentities] →
                                        CategoryTheory.Localization.Lifting₂ L₁ L₂ W₁ W₂ F
                                          (CategoryTheory.Localization.lift₂ F hF L₁ L₂)
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
VectorField.mlieBracketWithin_congr : ∀ {𝕜 : 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} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {x : M}
  {V W V₁ W₁ : (x : M) → TangentSpace I x},
  Set.EqOn V₁ V s →
    V₁ x = V x →
      Set.EqOn W₁ W s → W₁ x = W x → VectorField.mlieBracketWithin I V₁ W₁ s x = VectorField.mlieBracketWithin I V W s x
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatTrans.removeOp_id : ∀ {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.NatTrans.removeOp (CategoryTheory.CategoryStruct.id F.op) = CategoryTheory.CategoryStruct.id F
-- Std.Http.Data.URI.Parser
_private.Std.Http.Data.URI.Parser.0.Std.Http.URI.Parser.parseHost : Std.Http.URI.Config → Std.Internal.Parsec.ByteArray.Parser Std.Http.URI.Host
-- Mathlib.Order.DirSupClosed
dirSupClosed_iff_of_linearOrder : ∀ {α : Type u_1} {s : Set α} [inst : LinearOrder α],
  DirSupClosed s ↔ ∀ ⦃d : Set α⦄, d ⊆ s → d.Nonempty → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s
-- Mathlib.Data.Option.Basic
Option.orElse_eq_some : ∀ {α : Type u_1} (o o' : Option α) (x : α), (o <|> o') = some x ↔ o = some x ∨ o = none ∧ o' = some x
-- Mathlib.Data.Setoid.Basic
/-- The elements related to x ∈ α by the kernel of f are those in the preimage of f(x) under f.  -/
Setoid.ker_iff_mem_preimage : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {x y : α}, (Setoid.ker f) x y ↔ x ∈ f ⁻¹' {f y}
-- Mathlib.Algebra.Order.GroupWithZero.Basic
div_le_div_of_nonneg_left : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] [MulPosReflectLT G₀]
  {a b c : G₀}, 0 ≤ a → 0 < c → c ≤ b → a / b ≤ a / c
-- Mathlib.Order.Filter.Ker
Filter.ker_sup : ∀ {α : Type u_2} (f g : Filter α), (f ⊔ g).ker = f.ker ∪ g.ker
-- Mathlib.Algebra.Order.Group.End
RelHom.mul_def : ∀ {α : Type u_1} {r : α → α → Prop} (f g : r →r r), f * g = f.comp g
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxi.Iterator.Monadic.step.eq_1 : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] (it : Std.IterM Id α),
  Std.Rxi.Iterator.Monadic.step it =
    match it.internalState.next with
    | none => Std.IterStep.done
    | some next => Std.IterStep.yield { internalState := { next := Std.PRange.succ? next } } next
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.instInhabitedDBuilderName : Inhabited Aesop.Frontend.DBuilderName
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.replicateCol_vecMul : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {ι : Type u_6} [inst : Fintype m] [inst_1 : NonUnitalNonAssocSemiring α]
  (M : Matrix m n α) (v : m → α), Matrix.replicateCol ι (Matrix.vecMul v M) = (Matrix.replicateRow ι v * M).transpose
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.multicospanShape_R : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S),
  E.multicospanShape.R = E.I₁'
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.linearMap_eq_iff_of_span_eq_top : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_8}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (f g : M →ₗ[R] N) {S : Set M},
  Submodule.span R S = ⊤ → (f = g ↔ ∀ (s : ↑S), f ↑s = g ↑s)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.pow.match_1.congr_eq_2 : ∀ (motive : ℕ → Sort u_1) (k : ℕ) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (k : ℕ) → motive k.succ),
  k = 1 →
    (match k with
      | 0 => h_1 ()
      | 1 => h_2 ()
      | k.succ => h_3 k) ≍
      h_2 ()
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.instAsymmLTOfLawfulUpwardEnumerable : ∀ {α : Type u_1} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α],
  Std.Asymm Std.PRange.UpwardEnumerable.LT
-- Mathlib.CategoryTheory.Subterminal
/-- If `A` is subterminal, the unique morphism from it to the terminal object is a monomorphism.
The converse of `isSubterminal_of_mono_terminal_from`.
 -/
CategoryTheory.IsSubterminal.mono_terminal_from : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : C} [inst_1 : CategoryTheory.Limits.HasTerminal C],
  CategoryTheory.IsSubterminal A → CategoryTheory.Mono (CategoryTheory.Limits.terminal.from A)
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.coe_toEquiv : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (h : α ≃ᵢ β), ⇑h.toEquiv = ⇑h
-- Mathlib.Analysis.Normed.Module.ContinuousInverse
ContinuousLinearMap.HasLeftInverse.isClosed_complement : ∀ {R : Type u_7} {E : Type u_8} {F : Type u_10} [inst : Ring R] [inst_1 : TopologicalSpace E] [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] [inst_4 : TopologicalSpace F] [inst_5 : AddCommGroup F] [inst_6 : Module R F] {f : E →L[R] F}
  [T1Space F] (h : f.HasLeftInverse), IsClosed ↑h.complement
-- Mathlib.Order.Closure
LowerAdjoint.closure_sup_closure : ∀ {α : Type u_1} {β : Type u_4} [inst : SemilatticeSup α] [inst_1 : Preorder β] {u : β → α} (l : LowerAdjoint u)
  (x y : α), u (l.toFun (u (l.toFun x) ⊔ u (l.toFun y))) = u (l.toFun (x ⊔ y))
-- Mathlib.Algebra.CharP.Defs
CharP.existsUnique : ∀ (R : Type u_1) [inst : NonAssocSemiring R], ∃! p, CharP R p
-- Mathlib.RingTheory.Ideal.Operations
Ideal.IsPrime.pow_le_iff : ∀ {R : Type u} [inst : CommSemiring R] {I P : Ideal R} [hP : P.IsPrime] {n : ℕ}, n ≠ 0 → (I ^ n ≤ P ↔ I ≤ P)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.isNone_getElem?_toList_roo_eq : ∀ {m n i : ℕ}, ((m<...n).toList[i]?.isNone = true) = (n ≤ i + (m + 1))
-- Mathlib.Data.QPF.Multivariate.Constructions.Sigma
MvQPF.Sigma.inhabited : {n : ℕ} →
  {A : Type u} →
    (F : A → TypeVec.{u} n → Type u) →
      {α : TypeVec.{u} n} → [inst : Inhabited A] → [Inhabited (F default α)] → Inhabited (MvQPF.Sigma F α)
-- Lean.Message
/-- Whether trace node defaults to collapsed in the infoview.  -/
Lean.TraceData.collapsed : Lean.TraceData → Bool
-- Mathlib.Algebra.Group.TypeTags.Basic
Additive.addMonoid : {α : Type u} → [h : Monoid α] → AddMonoid (Additive α)
-- Mathlib.CategoryTheory.Adjunction.Mates
CategoryTheory.conjugateIsoEquiv_symm_apply_hom : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L₁ L₂ : CategoryTheory.Functor C D} {R₁ R₂ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂)
  (β : R₁ ≅ R₂),
  ((CategoryTheory.conjugateIsoEquiv adj₁ adj₂).symm β).hom = (CategoryTheory.conjugateEquiv adj₁ adj₂).symm β.hom
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.vertexSet_ssubset_or_edgeSet_ssubset_of_lt : ∀ {α : Type u_1} {β : Type u_2} {G H : Graph α β}, G < H → G.vertexSet ⊂ H.vertexSet ∨ G.edgeSet ⊂ H.edgeSet
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.sectL_zero : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (b : β), ProbabilityTheory.Kernel.sectL 0 b = 0
-- Std.Data.HashSet.Lemmas
Std.HashSet.Equiv.filter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} (f : α → Bool),
  m₁.Equiv m₂ → (Std.HashSet.filter f m₁).Equiv (Std.HashSet.filter f m₂)
-- Mathlib.Data.Set.Card.Arithmetic
Finset.exists_disjoint_union_of_even_card : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α}, Even s.card → ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ t.card = u.card
-- Mathlib.Algebra.Module.Submodule.Lattice
LE.le.eq_1 : ∀ (α : Type u) [self : LE α], LE.le = self.1
-- Mathlib.Algebra.Order.Archimedean.Basic
/-- An archimedean decidable linearly ordered `AddCommGroup` has a version of the
floor: for `a > 0`, any `g` in the group lies between some two consecutive multiples of `a`.  -/
existsUnique_zsmul_near_of_pos : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] {a : G},
  0 < a → ∀ (g : G), ∃! k, k • a ≤ g ∧ g < (k + 1) • a
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.instInhabitedPartialMatch : Inhabited Lean.Meta.LazyDiscrTree.PartialMatch
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsEquivalent.pow : ∀ {α : Type u_1} {β : Type u_3} [inst : NormedField β] {t u : α → β} {l : Filter α},
  Asymptotics.IsEquivalent l t u → ∀ (n : ℕ), Asymptotics.IsEquivalent l (t ^ n) (u ^ n)
-- Mathlib.Algebra.Group.End
/-- See `Equiv.Perm.inv_subtypePerm`.  -/
Equiv.Perm.subtypePerm_inv : ∀ {α : Type u_4} {p : α → Prop} (f : Equiv.Perm α) (hf : ∀ (x : α), p (f⁻¹ x) ↔ p x),
  f⁻¹.subtypePerm hf = (f.subtypePerm ⋯)⁻¹
-- Mathlib.Analysis.Normed.Algebra.Spectrum
SpectrumRestricts.nnreal_iff_spectralRadius_le : ∀ {A : Type u_3} [inst : Ring A] [inst_1 : Algebra ℝ A] {a : A} {t : NNReal},
  spectralRadius ℝ a ≤ ↑t →
    (SpectrumRestricts a ⇑ContinuousMap.realToNNReal ↔ spectralRadius ℝ ((algebraMap ℝ A) ↑t - a) ≤ ↑t)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Units
/-- **Alias** of the reverse direction of `Units.one_le_inv_mul`. -/
Units.one_le_inv_mul_of_le : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : LE M] [MulLeftMono M] (u : Mˣ) {a : M}, ↑u ≤ a → 1 ≤ ↑u⁻¹ * a
-- Lean.Environment
/-- Participating in the module system?  -/
Lean.ModuleData.isModule : Lean.ModuleData → Bool
-- Init.Data.SInt.Bitwise
Int32.and_self : ∀ {a : Int32}, a &&& a = a
-- Mathlib.Topology.Semicontinuity.Basic
ContinuousAt.comp_upperSemicontinuousAt_antitone : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {γ : Type u_4} [inst_1 : LinearOrder γ]
  [inst_2 : TopologicalSpace γ] [OrderTopology γ] {δ : Type u_5} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ]
  [OrderTopology δ] {g : γ → δ} {f : α → γ},
  ContinuousAt g (f x) → UpperSemicontinuousAt f x → Antitone g → LowerSemicontinuousAt (g ∘ f) x
-- Mathlib.Analysis.Normed.Lp.lpSpace
PreLp.instSMulOfModule : {𝕜 : Type u_1} →
  {α : Type u_2} →
    {E : α → Type u_3} →
      [inst : (i : α) → NormedAddCommGroup (E i)] →
        [inst_1 : NormedRing 𝕜] → [(i : α) → Module 𝕜 (E i)] → SMul 𝕜 (PreLp E)
-- Mathlib.Algebra.Category.Ring.Basic
SemiRingCat.semiring : (self : SemiRingCat) → Semiring ↑self
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.instMonoid : {α : Type u_1} → [inst : PseudoEMetricSpace α] → Monoid (α →ᵈ α)
-- Lean.Elab.Tactic.Omega.MinNatAbs
Lean.Elab.Tactic.Omega.List.nonzeroMinimum_eq_of_nonzero : ∀ {xs : List ℕ},
  Lean.Elab.Tactic.Omega.List.nonzeroMinimum xs ≠ 0 → ∃ x ∈ xs, Lean.Elab.Tactic.Omega.List.nonzeroMinimum xs = x
-- Mathlib.Data.Fin.VecNotation
Matrix.vecAppend_empty : ∀ {α : Type u} {n : ℕ} (v : Fin n → α), Matrix.vecAppend ⋯ v ![] = v
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNormEssSup_lt_top_of_ae_nnnorm_bound : ∀ {α : Type u_1} {F : Type u_5} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup F]
  {f : α → F} {C : NNReal}, (∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C) → MeasureTheory.eLpNormEssSup f μ < ⊤
-- Mathlib.Algebra.Field.Rat
NNRat.coe_zpow : ∀ (p : ℚ≥0) (n : ℤ), ↑(p ^ n) = ↑p ^ n
-- Init.Data.Int.Order
Int.toNat_add : ∀ {a b : ℤ}, 0 ≤ a → 0 ≤ b → (a + b).toNat = a.toNat + b.toNat
-- Init.Data.Array.BasicAux
_private.Init.Data.Array.BasicAux.0.List.toArrayAux.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Array α → Sort u_2) (a : α) (as : List α) (xs : Array α)
  (h_1 : (xs : Array α) → motive [] xs) (h_2 : (a : α) → (as : List α) → (xs : Array α) → motive (a :: as) xs),
  (match a :: as, xs with
    | [], xs => h_1 xs
    | a :: as, xs => h_2 a as xs) =
    h_2 a as xs
-- Mathlib.RingTheory.GradedAlgebra.RingHom
GradedRingHom.ofClass.congr_simp : ∀ {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [inst : Semiring A] [inst_1 : Semiring B]
  [inst_2 : SetLike σ A] [inst_3 : SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} {F : Type u_10} [inst_4 : FunLike F A B]
  [inst_5 : GradedFunLike F 𝒜 ℬ] [inst_6 : RingHomClass F A B] (f f_1 : F), f = f_1 → ↑f = ↑f_1
-- Mathlib.Data.FunLike.IsApply
/-- **Alias** of `IsVAddApply.vadd_apply`. -/
vadd_apply : ∀ {M : Type u_1} {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} {inst : FunLike F α β}
  {inst_1 : VAdd M β} {inst_2 : VAdd M F} [self : IsVAddApply M F α β] (f : F) (r : M) (x : α), (r +ᵥ f) x = r +ᵥ f x
-- Mathlib.MeasureTheory.Constructions.Cylinders
MeasureTheory.union_cylinder : ∀ {ι : Type u_1} {α : ι → Type u_2} (s₁ s₂ : Finset ι) (S₁ : Set ((i : ↥s₁) → α ↑i)) (S₂ : Set ((i : ↥s₂) → α ↑i))
  [inst : DecidableEq ι],
  MeasureTheory.cylinder s₁ S₁ ∪ MeasureTheory.cylinder s₂ S₂ =
    MeasureTheory.cylinder (s₁ ∪ s₂) (Finset.restrict₂ ⋯ ⁻¹' S₁ ∪ Finset.restrict₂ ⋯ ⁻¹' S₂)
-- Mathlib.Tactic.Order.Graph.Basic
Mathlib.Tactic.Order.Edge.mk : ℕ → ℕ → Lean.Expr → Mathlib.Tactic.Order.Edge
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.lift_umax_eq : ∀ {a : Cardinal.{u}} {b : Cardinal.{v}},
  Cardinal.lift.{max v w, u} a = Cardinal.lift.{max u w, v} b ↔ Cardinal.lift.{v, u} a = Cardinal.lift.{u, v} b
-- Mathlib.Data.Set.Card
/-- **Alias** of `Set.ncard_sdiff_singleton_le`. -/
Set.ncard_diff_singleton_le : ∀ {α : Type u_1} (s : Set α) (a : α), (s \ {a}).ncard ≤ s.ncard
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_eq_of_eq_mul_right : ∀ {a b c : ℤ}, b ≠ 0 → a = b * c → a / b = c
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.Measure.withDensity_rnDeriv_eq : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [μ.HaveLebesgueDecomposition ν],
  μ.AbsolutelyContinuous ν → ν.withDensity (μ.rnDeriv ν) = μ
-- Init.MetaTypes
Lean.NameGenerator.mk.inj : ∀ {namePrefix : Lean.Name} {idx : ℕ} {namePrefix_1 : Lean.Name} {idx_1 : ℕ},
  { namePrefix := namePrefix, idx := idx } = { namePrefix := namePrefix_1, idx := idx_1 } →
    namePrefix = namePrefix_1 ∧ idx = idx_1
-- Init.SizeOfLemmas
Subtype.sizeOf : ∀ {α : Sort u_1} {p : α → Prop} (s : Subtype p), sizeOf s = sizeOf ↑s + 1
-- Lean.Parser.Term
Lean.Parser.Term.ensureExpectedType.formatter : Lean.PrettyPrinter.Formatter
-- Init.Prelude
/-- The typeclass behind the notation `a &&& b : γ` where `a : α`, `b : β`.  -/
HAnd : Type u → Type v → outParam (Type w) → Type (max (max u v) w)
-- Mathlib.Analysis.Calculus.FDeriv.Basic
HasStrictFDerivAt.isBigO_sub : ∀ {𝕜 : 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}
  {f' : E →L[𝕜] F} {x : E}, HasStrictFDerivAt f f' x → (fun p => f p.1 - f p.2) =O[nhds (x, x)] fun p => p.1 - p.2
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
/-- **Alias** of `AlgebraicGeometry.UniversallyClosed.universally_isClosedMap`. -/
AlgebraicGeometry.UniversallyClosed.out : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : AlgebraicGeometry.UniversallyClosed f],
  (AlgebraicGeometry.topologically @IsClosedMap).universally f
-- Mathlib.Topology.Algebra.Module.Equiv
/-- A continuous linear equivalence of two modules restricts to a continuous linear equivalence
from the preimage of any submodule to that submodule.
This is `ContinuousLinearEquiv.ofSubmodule` but with `comap` on the left
instead of `map` on the right.  -/
ContinuousLinearEquiv.ofSubmodule' : {R : Type u_1} →
  {R₂ : Type u_2} →
    {M : Type u_3} →
      {M₂ : Type u_4} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : TopologicalSpace M] →
                [inst_4 : AddCommMonoid M₂] →
                  [inst_5 : TopologicalSpace M₂] →
                    {module_M : Module R M} →
                      {module_M₂ : Module R₂ M₂} →
                        {σ₁₂ : R →+* R₂} →
                          {σ₂₁ : R₂ →+* R} →
                            {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} →
                              {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} →
                                (f : M ≃SL[σ₁₂] M₂) → (U : Submodule R₂ M₂) → ↥(Submodule.comap (↑↑f) U) ≃SL[σ₁₂] ↥U
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {γ : α → Type w}
  [inst : Std.TransCmp cmp] {f : (a : α) → β a → γ a} {k : α}, (Std.ExtDTreeMap.map f t).getKey? k = t.getKey? k
-- Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
ComplexShape.Embedding.instFaithfulHomotopyCategoryExtendHomotopyFunctor : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [inst : e.IsRelIff]
  (C : Type u_3) [inst_1 : CategoryTheory.Category.{v_1, u_3} C] [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.Preadditive C], (e.extendHomotopyFunctor C).Faithful
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.trans_source : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (e' : PartialEquiv β γ),
  (e.trans e').source = e.source ∩ ↑e ⁻¹' e'.source
-- Mathlib.CategoryTheory.Localization.HomEquiv
/-- Bijection between types of morphisms in two localized categories
for the same class of morphisms `W`.  -/
CategoryTheory.Localization.homEquiv : {C : Type u_1} →
  {D₁ : Type u_5} →
    {D₂ : Type u_6} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_5, u_5} D₁] →
          [inst_2 : CategoryTheory.Category.{v_6, u_6} D₂] →
            (W : CategoryTheory.MorphismProperty C) →
              (L₁ : CategoryTheory.Functor C D₁) →
                [L₁.IsLocalization W] →
                  (L₂ : CategoryTheory.Functor C D₂) →
                    [L₂.IsLocalization W] → {X Y : C} → (L₁.obj X ⟶ L₁.obj Y) ≃ (L₂.obj X ⟶ L₂.obj Y)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.coe_adj_sub : ∀ {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (u v : ↑G'.verts), G'.coe.Adj u v → G.Adj ↑u ↑v
-- Mathlib.CategoryTheory.Sites.Sheafification
CategoryTheory.isoSheafify_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  {P : CategoryTheory.Functor Cᵒᵖ D} (hP : CategoryTheory.Presheaf.IsSheaf J P),
  (CategoryTheory.isoSheafify J hP).inv = CategoryTheory.sheafifyLift J (CategoryTheory.CategoryStruct.id P) hP
-- Std.Http.Data.Body.Basic
/-- Typeclass for types that can be converted to a `ByteArray`.
 -/
Std.Http.Body.ToByteArray : Type → Type
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
/-- The homotopy between morphisms in `ShortComplex C` that is induced by a homotopy
between morphisms in `ShortComplex Cᵒᵖ`.  -/
CategoryTheory.ShortComplex.Homotopy.unop : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S₁ S₂ : CategoryTheory.ShortComplex Cᵒᵖ} →
        {φ₁ φ₂ : S₁ ⟶ S₂} →
          CategoryTheory.ShortComplex.Homotopy φ₁ φ₂ →
            CategoryTheory.ShortComplex.Homotopy (CategoryTheory.ShortComplex.unopMap φ₁)
              (CategoryTheory.ShortComplex.unopMap φ₂)