mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sums.Basic
/-- An induction principle for morphisms in a sum of categories: a morphism is either of the form
`(inl_ _ _).map _` or of the form `(inr_ _ _).map _`.  -/
CategoryTheory.Sum.homInduction : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {P : {x y : C ⊕ D} → (x ⟶ y) → Sort u_1} →
          ((x y : C) → (f : x ⟶ y) → P ((CategoryTheory.Sum.inl_ C D).map f)) →
            ((x y : D) → (f : x ⟶ y) → P ((CategoryTheory.Sum.inr_ C D).map f)) → {x y : C ⊕ D} → (f : x ⟶ y) → P f
-- Mathlib.Topology.EMetricSpace.Paracompact
/-- **Alias** of `Metric.t4Space`. -/
EMetric.t4Space : ∀ {α : Type u_1} [inst : EMetricSpace α], T4Space α
-- Init.Data.Option.Basic
/-- Checks whether an optional value either satisfies a Boolean predicate or is `none`.

Examples:
* `(some 33).all (· % 2 == 0) = false
* `(some 22).all (· % 2 == 0) = true
* `none.all (fun x : Nat => x % 2 == 0) = true
 -/
Option.all : {α : Type u_1} → (α → Bool) → Option α → Bool
-- Mathlib.Algebra.Order.Ring.Canonical
/-- The `tsub` version of `mul_self_sub_mul_self`. Notably, this holds for `Nat` and `NNReal`.  -/
mul_self_tsub_mul_self : ∀ {R : Type u} [inst : CommSemiring R] [inst_1 : PartialOrder R] [CanonicallyOrderedAdd R] [inst_3 : Sub R]
  [OrderedSub R] [Std.Total fun x1 x2 => x1 ≤ x2] [AddLeftReflectLE R] (a b : R), a * a - b * b = (a + b) * (a - b)
-- Mathlib.Topology.MetricSpace.CoveringNumbers
/-- The covering number (or internal covering number) of a set `A` for radius `ε` is
the minimal cardinality (in `ℕ∞`) of an `ε`-cover contained in `A`.  -/
Metric.coveringNumber : {X : Type u_1} → [PseudoEMetricSpace X] → NNReal → Set X → ℕ∞
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- The counit isomorphism of the equivalence
`widePushoutShapeOpEquiv : (WidePushoutShape J)ᵒᵖ ≌ WidePullbackShape J`  -/
CategoryTheory.Limits.widePullbackShapeUnopOp : (J : Type w) →
  (CategoryTheory.Limits.widePullbackShapeOp J).comp (CategoryTheory.Limits.widePushoutShapeUnop J) ≅
    CategoryTheory.Functor.id (CategoryTheory.Limits.WidePullbackShape J)
-- Mathlib.Data.List.AList
AList.lookup_union_right : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {s₁ s₂ : AList β},
  a ∉ s₁ → AList.lookup a (s₁ ∪ s₂) = AList.lookup a s₂
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.map_one : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommMonoidWithZero R'] (χ : MulChar R R'), χ 1 = 1
-- Mathlib.RingTheory.Valuation.ExtendToLocalization
Valuation.extendToLocalization_mk' : ∀ {A : Type u_1} [inst : CommRing A] {Γ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ] (v : Valuation A Γ)
  {S : Submonoid A} (hS : S ≤ v.supp.primeCompl) (B : Type u_3) [inst_2 : CommRing B] [inst_3 : Algebra A B]
  [inst_4 : IsLocalization S B] (x : A) (y : ↥S),
  (v.extendToLocalization hS B) (IsLocalization.mk' B x y) = v x * (v ↑y)⁻¹
-- Mathlib.Algebra.Module.LocalizedModule.Basic
/-- If `(M', f : M ⟶ M')` satisfies universal property of localized module, then `M'` is isomorphic to
`LocalizedModule S M` as an `R`-module.
 -/
IsLocalizedModule.iso : {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] → LocalizedModule S M ≃ₗ[R] M'
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem!_union_of_not_mem_right : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} [inst_2 : Inhabited β], k ∉ m₂ → (m₁ ∪ m₂)[k]! = m₁[k]!
-- Mathlib.Order.Filter.Prod
Filter.tendsto_prod_iff' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Filter β} {g' : Filter γ} {s : α → β × γ},
  Filter.Tendsto s f (g ×ˢ g') ↔ Filter.Tendsto (fun n => (s n).1) f g ∧ Filter.Tendsto (fun n => (s n).2) f g'
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.normalizeObj_congr : ∀ {C : Type u} (n : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C)
  {X Y : CategoryTheory.FreeMonoidalCategory C} (f : X ⟶ Y), X.normalizeObj n = Y.normalizeObj n
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.whisker_exchange_assoc : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈}
  {C'' : Type u₉} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  [inst_6 : CategoryTheory.Category.{v₇, u₇} A''] [inst_7 : CategoryTheory.Category.{v₈, u₈} B'']
  [inst_8 : CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''}
  {G'' : CategoryTheory.Functor C'' B''} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (η : ψ ⟶ ψ')
  {φ φ' : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''} (θ : φ ⟶ φ')
  {Z : CategoryTheory.Limits.CatCospanTransform F G F'' G''} (h : ψ'.comp φ' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft ψ θ)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight η φ') h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight η φ)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft ψ' θ) h)
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.UniversallyEffectiveEquivalenceRelation.toEffectiveEquivalenceRelation : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {R A : C} →
      {p₁ p₂ : R ⟶ A} →
        CategoryTheory.UniversallyEffectiveEquivalenceRelation p₁ p₂ → CategoryTheory.EffectiveEquivalenceRelation p₁ p₂
-- Mathlib.MeasureTheory.Measure.Hausdorff
/-- Mapping a set of reals along a line segment scales the measure by the length of a segment.

This is an auxiliary result used to prove `hausdorffMeasure_affineSegment`.  -/
MeasureTheory.hausdorffMeasure_lineMap_image : ∀ {E : Type u_5} {P : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace P]
  [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor E P] [inst_5 : BorelSpace P] (x y : P) (s : Set ℝ),
  (MeasureTheory.Measure.hausdorffMeasure 1) (⇑(AffineMap.lineMap x y) '' s) =
    nndist x y • (MeasureTheory.Measure.hausdorffMeasure 1) s
-- Mathlib.CategoryTheory.Linear.LinearFunctor
CategoryTheory.Equivalence.inverseLinear : ∀ (R : Type u_1) [inst : Semiring R] {C : Type u_2} {D : Type u_3} [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Category.{v_2, u_3} D] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : CategoryTheory.Preadditive D] [inst_5 : CategoryTheory.Linear R C] [inst_6 : CategoryTheory.Linear R D]
  (e : C ≌ D) [CategoryTheory.Functor.Linear R e.functor], CategoryTheory.Functor.Linear R e.inverse
-- Mathlib.Analysis.SpecialFunctions.Arsinh
/-- `Real.sinh` as an `OrderIso`.  -/
Real.sinhOrderIso : ℝ ≃o ℝ
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.σ_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X' X : CategoryTheory.SimplicialObject C} (f : X ⟶ X') {n : ℕ}
  (i : Fin (n + 1)),
  CategoryTheory.CategoryStruct.comp (X.σ i) (f.app (Opposite.op { len := n + 1 })) =
    CategoryTheory.CategoryStruct.comp (f.app (Opposite.op { len := n })) (X'.σ i)
-- Mathlib.Analysis.Calculus.ContDiff.Operations
iteratedFDerivWithin_const_smul_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {x : E} {R : Type u_3} [inst_5 : DistribSMul R F] [inst_6 : SMulCommClass 𝕜 R F]
  [inst_7 : ContinuousConstSMul R F] {i : ℕ} {a : R},
  ContDiffWithinAt 𝕜 (↑i) f s x →
    UniqueDiffOn 𝕜 s → x ∈ s → iteratedFDerivWithin 𝕜 i (a • f) s x = a • iteratedFDerivWithin 𝕜 i f s x
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.homologyMap_comp_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {K L M : HomologicalComplex C c} (φ : K ⟶ L) (ψ : L ⟶ M) (i : ι)
  [inst_2 : K.HasHomology i] [inst_3 : L.HasHomology i] [inst_4 : M.HasHomology i] {Z : C} (h : M.homology i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (CategoryTheory.CategoryStruct.comp φ ψ) i) h =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap φ i)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap ψ i) h)
-- Mathlib.Analysis.Fourier.AddCircleMulti
/-- The family of monomials `mFourier n`, parametrized by `n : ℤᵈ` and considered as
elements of the `Lp` space of functions `UnitAddTorus d → ℂ`.  -/
UnitAddTorus.mFourierLp : {d : Type u_1} →
  [inst : Fintype d] → (p : ENNReal) → [Fact (1 ≤ p)] → (d → ℤ) → ↥(MeasureTheory.Lp ℂ p MeasureTheory.volume)
-- Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
CategoryTheory.ObjectProperty.IsVerdierLeftLocalizing.fac : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {A B : CategoryTheory.ObjectProperty C}
  [self : A.IsVerdierLeftLocalizing B] {X Y : C} (f : X ⟶ Y),
  A X → B Y → ∃ Z a b, A Z ∧ B Z ∧ CategoryTheory.CategoryStruct.comp a b = f
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Extension.toKaehler_surjective : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {P : Algebra.Extension R S}, Function.Surjective ⇑P.toKaehler
-- Init.Data.BitVec.Bitblast
BitVec.getLsbD_srem : ∀ {w i : ℕ} {x y : BitVec w},
  (x.srem y).getLsbD i =
    match x.msb, y.msb with
    | false, false => (x % y).getLsbD i
    | false, true => (x % -y).getLsbD i
    | true, false => (-(-x % y)).getLsbD i
    | true, true => (-(-x % -y)).getLsbD i
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.tmul_one_eq_one_tmul : ∀ {R : Type uR} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (r : R), (algebraMap R A) r ⊗ₜ[R] 1 = 1 ⊗ₜ[R] (algebraMap R B) r
-- Mathlib.Order.Partition.Basic
/-- Partitions on `s` are ordered by refinement: `P ≤ Q` if every part of `P` is contained in a part
of `Q`.  -/
Partition.instPartialOrder : {α : Type u_1} → {s : α} → [inst : CompleteLattice α] → PartialOrder (Partition s)
-- Mathlib.MeasureTheory.Function.Holder
ContinuousLinearMap.norm_holder_apply_apply_le : ∀ {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {p q r : ENNReal} [hpqr : p.HolderTriple q r] [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedAddCommGroup G]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 F] [inst_6 : NormedSpace 𝕜 G] (B : E →L[𝕜] F →L[𝕜] G)
  (f : ↥(MeasureTheory.Lp E p μ)) (g : ↥(MeasureTheory.Lp F q μ)),
  ‖ContinuousLinearMap.holder r B f g‖ ≤ ‖B‖ * ‖f‖ * ‖g‖
-- Mathlib.Data.Finset.Sigma
Set.biUnion_finsetSigma' : ∀ {ι : Type u_1} {α : ι → Type u_2} {β : Type u_3} (s : Finset ι) (t : (i : ι) → Finset (α i))
  (f : (i : ι) → α i → Set β), ⋃ i ∈ s, ⋃ j ∈ t i, f i j = ⋃ ij ∈ s.sigma t, f ij.fst ij.snd
-- Mathlib.Analysis.InnerProductSpace.Laplacian
/-- Expression of `bilinearIteratedFDerivTwo` in terms of `iteratedFDeriv`.
 -/
bilinearIteratedFDerivTwo_eq_iteratedFDeriv : ∀ {𝕜 : 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)
  (e e₁ e₂ : E), ((bilinearIteratedFDerivTwo 𝕜 f e) e₁) e₂ = (iteratedFDeriv 𝕜 2 f e) ![e₁, e₂]
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.norm_integral_le_of_le_const : ∀ {ι : Type u} {E : Type v} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {I : BoxIntegral.Box ι}
  [inst_2 : Fintype ι] {l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {c : ℝ},
  (∀ x ∈ BoxIntegral.Box.Icc I, ‖f x‖ ≤ c) →
    ∀ (μ : MeasureTheory.Measure (ι → ℝ)) [inst_3 : MeasureTheory.IsLocallyFiniteMeasure μ],
      ‖BoxIntegral.integral I l f μ.toBoxAdditive.toSMul‖ ≤ μ.real ↑I * c
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
MulAlgebraNormClass.toSeminormClass : ∀ {F : Type u_1} {R : outParam (Type u_2)} [inst : SeminormedCommRing R] {S : outParam (Type u_3)} [inst_1 : Ring S]
  [inst_2 : Algebra R S] [inst_3 : FunLike F S ℝ] [self : MulAlgebraNormClass F R S], SeminormClass F R S
-- Mathlib.Topology.Algebra.UniformRing
UniformSpace.Completion.one : (α : Type u_1) → [Ring α] → [inst : UniformSpace α] → One (UniformSpace.Completion α)
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- Symmetric bilinear maps can be lifted to quadratic maps  -/
QuadraticMap.canLift' : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : Invertible 2],
  CanLift (LinearMap.BilinMap R M N) (QuadraticMap R M N) ⇑(QuadraticMap.associatedHom ℕ) fun B => LinearMap.flip B = B
-- Mathlib.Combinatorics.Additive.CovBySMul
CovBySMul.rfl : ∀ {M : Type u_1} {X : Type u_3} [inst : Monoid M] [inst_1 : MulAction M X] {A : Set X}, CovBySMul M 1 A A
-- Mathlib.Algebra.Ring.Divisibility.Basic
map_dvd_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Semigroup α] [inst_1 : Semigroup β] {F : Type u_3} [inst_2 : EquivLike F α β]
  [MulEquivClass F α β] (f : F) {a b : α}, f a ∣ f b ↔ a ∣ b
-- Mathlib.Order.Concept
Concept.extent_max : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c d : Concept α β r),
  (c ⊔ d).extent = lowerPolar r (c.intent ∩ d.intent)
-- Mathlib.Algebra.Group.Prod
Prod.addCommMagma.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : AddCommMagma M] [inst_1 : AddCommMagma N],
  Prod.addCommMagma = { toAdd := Prod.instAdd, add_comm := ⋯ }
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.getEntryLE!_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited ((a : α) × β a)] {k : α}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getEntryLE! k = t₂.getEntryLE! k
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.projectMapAux.eq_4 : ∀ {C : Type u} {D : Type u'} [inst : CategoryTheory.Category.{v', u'} D] [inst_1 : CategoryTheory.MonoidalCategory D]
  (f : C → D) (x : CategoryTheory.FreeMonoidalCategory C),
  CategoryTheory.FreeMonoidalCategory.projectMapAux f (CategoryTheory.FreeMonoidalCategory.Hom.l_hom x) =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.FreeMonoidalCategory.projectObj f x)).hom
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.separatingRight_toMatrix₂'_iff : ∀ {R : Type u_1} {n : Type u_11} {m : Type u_12} [inst : CommRing R] [inst_1 : DecidableEq m] [inst_2 : Fintype m]
  [inst_3 : DecidableEq n] [inst_4 : Fintype n] {B : (m → R) →ₗ[R] (n → R) →ₗ[R] R},
  ((LinearMap.toMatrix₂' R) B).SeparatingRight ↔ B.SeparatingRight
-- Std.Internal.Do.Order.PreservesSup
/-- The upper adjoint of `f`: the join of all `x` with `f x ⊑ b`. For `f = (a ⊓ ·)` this is Heyting
implication `a ⇨ ·`.  -/
Lean.Order.PreservesSup.upperAdjoint : {α : Type u} → [Lean.Order.CompleteLattice α] → (α → α) → α → α
-- Mathlib.Algebra.Order.Module.Defs
instSMulPosStrictMonoIntOfIsOrderedAddMonoid : ∀ {G : Type u_3} [inst : PartialOrder G] [inst_1 : AddCommGroup G] [IsOrderedAddMonoid G], SMulPosStrictMono ℤ G
-- Mathlib.MeasureTheory.Integral.DominatedConvergence
MeasureTheory.IntegrableOn.continuousOn_Ici_primitive_Ici : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {μ : MeasureTheory.Measure ℝ} {f : ℝ → E}
  [MeasureTheory.NullSingletonClass μ] {a₀ : ℝ},
  MeasureTheory.IntegrableOn f (Set.Ici a₀) μ → ContinuousOn (fun b => ∫ (x : ℝ) in Set.Ici b, f x ∂μ) (Set.Ici a₀)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get_inter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {k : α} {h_mem : k ∈ t₁ ∩ t₂},
  Std.ExtDTreeMap.Const.get (t₁ ∩ t₂) k h_mem = Std.ExtDTreeMap.Const.get t₁ k ⋯
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.coe_prodAssoc_symm : ∀ (R : Type u_1) (E : Type u_5) (E₂ : Type u_6) (E₃ : Type u_7) [inst : Semiring R] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : SeminormedAddCommGroup E₂] [inst_3 : SeminormedAddCommGroup E₃] [inst_4 : Module R E] [inst_5 : Module R E₂]
  [inst_6 : Module R E₃], ⇑(LinearIsometryEquiv.prodAssoc R E E₂ E₃).symm = ⇑(Equiv.prodAssoc E E₂ E₃).symm
-- Mathlib.Algebra.Homology.FullSubcategory
/-- Given `P : ObjectProperty V` and `K : HomologicalComplex V c`,
this is a lift of `K` in `HomologicalComplex P.FullSubcategory c`
when `K.X n` satisfies `P` for all `n`.  -/
HomologicalComplex.liftObjectProperty : {ι : Type u_1} →
  {c : ComplexShape ι} →
    {V : Type u_2} →
      [inst : CategoryTheory.Category.{v_1, u_2} V] →
        [inst_1 : CategoryTheory.Preadditive V] →
          (P : CategoryTheory.ObjectProperty V) →
            (K : HomologicalComplex V c) → (∀ (n : ι), P (K.X n)) → HomologicalComplex P.FullSubcategory c
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (f : Polynomial R), AdjoinRoot f = (Polynomial R ⧸ Ideal.span {f})
-- Mathlib.Topology.MetricSpace.Antilipschitz
/-- **Alias** of the forward direction of `antilipschitzWith_iff_le_mul_nndist`. -/
AntilipschitzWith.le_mul_nndist : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {K : NNReal} {f : α → β},
  AntilipschitzWith K f → ∀ (x y : α), nndist x y ≤ K * nndist (f x) (f y)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get!_inter_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : LawfulBEq α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α} [inst_3 : Inhabited (β k)], m₂.contains k = false → (m₁.inter m₂).get! k = default
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size_inter_le_size_left : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], (m₁ ∩ m₂).size ≤ m₁.size
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
/-- Given a subgraph `G'` and a set of vertex pairs, remove all of the corresponding edges
from its edge set, if present.

See also: `SimpleGraph.deleteEdges`.  -/
SimpleGraph.Subgraph.deleteEdges : {V : Type u} → {G : SimpleGraph V} → G.Subgraph → Set (Sym2 V) → G.Subgraph
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.map_single : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (R' : Type u_6)
  {M' : Type u_7} [inst_3 : CommRing R'] [inst_4 : AddCommGroup M'] [inst_5 : Module R' M'] [inst_6 : Module R M']
  (f : M →ₗ[R] M') (i : ℕ) (m : M),
  (PolynomialModule.map R' f) (PolynomialModule.single R i m) = PolynomialModule.single R' i (f m)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CStarAlgebra.isStrictlyPositive_iff_exists_isUnit_and_isSelfAdjoint_and_eq_mul_self : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [StarOrderedRing A] [inst_5 : Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A]
  [IsSemitopologicalRing A] [T2Space A] {a : A}, IsStrictlyPositive a ↔ ∃ b, IsUnit b ∧ IsSelfAdjoint b ∧ a = b * b
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback₃.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S}
  {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃}
  {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} [inst_1 : SizeOf C]
  (chosenPullback : CategoryTheory.Limits.ChosenPullback h₁₂.p₂ h₂₃.p₁) (p : chosenPullback.pullback ⟶ S)
  (p₁ : chosenPullback.pullback ⟶ X₁) (p₃ : chosenPullback.pullback ⟶ X₃) (l : h₁₃.LiftStruct p₁ p₃ p)
  (hp₁ :
    autoParam (CategoryTheory.CategoryStruct.comp chosenPullback.p₁ h₁₂.p₁ = p₁)
      CategoryTheory.Limits.ChosenPullback₃.hp₁._autoParam)
  (hp₃ :
    autoParam (CategoryTheory.CategoryStruct.comp chosenPullback.p₂ h₂₃.p₂ = p₃)
      CategoryTheory.Limits.ChosenPullback₃.hp₃._autoParam),
  sizeOf { chosenPullback := chosenPullback, p := p, p₁ := p₁, p₃ := p₃, l := l, hp₁ := hp₁, hp₃ := hp₃ } =
    1 + sizeOf chosenPullback + sizeOf p + sizeOf p₁ + sizeOf p₃ + sizeOf l + sizeOf hp₁ + sizeOf hp₃
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
/-- A modification `Γ` between strong natural transformations `η` and `θ` (between oplax functors)
consists of a family of 2-morphisms `Γ.app a : η.app a ⟶ θ.app a`, which satisfies the equation
`(F.map f ◁ app b) ≫ (θ.naturality f).hom = (η.naturality f).hom ≫ (app a ▷ G.map f)`
for each 1-morphism `f : a ⟶ b`.
 -/
CategoryTheory.Oplax.StrongTrans.Modification : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} → (F ⟶ G) → (F ⟶ G) → Type (max u₁ w₂)
-- Mathlib.Algebra.Category.Ring.Constructions
/-- `ℤ` is the initial object of `CommRingCat`.  -/
CommRingCat.zIsInitial : CategoryTheory.Limits.IsInitial (CommRingCat.of ℤ)
-- Lean.Meta.Tactic.Grind.Arith.FieldNormNum
_private.Lean.Meta.Tactic.Grind.Arith.FieldNormNum.0.Lean.Meta.Grind.Arith.FieldNormNum.Context.mk.injEq : ∀ (u : Lean.Level) (type fieldInst isChar0Inst ringInst semiringInst : Lean.Expr) (u_1 : Lean.Level)
  (type_1 fieldInst_1 isChar0Inst_1 ringInst_1 semiringInst_1 : Lean.Expr),
  ({ u := u, type := type, fieldInst := fieldInst, isChar0Inst := isChar0Inst, ringInst := ringInst,
        semiringInst := semiringInst } =
      { u := u_1, type := type_1, fieldInst := fieldInst_1, isChar0Inst := isChar0Inst_1, ringInst := ringInst_1,
        semiringInst := semiringInst_1 }) =
    (u = u_1 ∧
      type = type_1 ∧
        fieldInst = fieldInst_1 ∧ isChar0Inst = isChar0Inst_1 ∧ ringInst = ringInst_1 ∧ semiringInst = semiringInst_1)
-- Mathlib.MeasureTheory.Measure.AddContent
MeasureTheory.addContent_union_le : ∀ {α : Type u_1} {C : Set (Set α)} {s t : Set α} {G : Type u_2} [inst : AddCommMonoid G]
  {m : MeasureTheory.AddContent G C} [inst_1 : PartialOrder G] [CanonicallyOrderedAdd G],
  MeasureTheory.IsSetRing C → s ∈ C → t ∈ C → m (s ∪ t) ≤ m s + m t
-- Mathlib.RingTheory.Etale.Finite
/-- If `Ω` is separably closed, the fiber functor for finite étale `Ω`-algebras
is naturally isomorphic to the (finite) `Spec` functor.  -/
CommAlgCat.FiniteEtale.fiberIsoFiniteSpec : (Ω : Type w) →
  [inst : Field Ω] → [IsSepClosed Ω] → CommAlgCat.FiniteEtale.fiber Ω Ω ≅ CommAlgCat.FiniteEtale.finiteSpec Ω
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.isBridge_deleteEdges_singleton : ∀ {V : Type u} {G : SimpleGraph V} {e : Sym2 V}, (G.deleteEdges {e}).IsBridge e ↔ G.IsBridge e
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.instRingHomInvPairToRingHomRingEquivSymm : ∀ {A : Type u_8} {B : Type u_9} [inst : CommRing A] [inst_1 : CommRing B] (f : A ≃+* B), RingHomInvPair ↑f ↑f.symm