mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.Map
MeasureTheory.Measure.map_apply : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {f : α → β}, Measurable f → ∀ {s : Set β}, MeasurableSet s → (MeasureTheory.Measure.map f μ) s = μ (f ⁻¹' s)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPullback.isoIsPullback_inv_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : C} (X Y : C) {Z : C} {fst : P ⟶ X} {snd : P ⟶ Y}
  {f : X ⟶ Z} {g : Y ⟶ Z} {P' : C} {fst' : P' ⟶ X} {snd' : P' ⟶ Y} (h : CategoryTheory.IsPullback fst snd f g)
  (h' : CategoryTheory.IsPullback fst' snd' f g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.IsPullback.isoIsPullback X Y h h').inv snd = snd'
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.IsTerminal.instSubsingleton : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}}
  {D : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ} {e : J}, Subsingleton (D.IsTerminal e)
-- Mathlib.RingTheory.Valuation.ValuationRing
ValuationRing.mem_integer_iff : ∀ (A : Type u) [inst : CommRing A] (K : Type v) [inst_1 : Field K] [inst_2 : Algebra A K] [inst_3 : IsDomain A]
  [inst_4 : ValuationRing A] [inst_5 : IsFractionRing A K] (x : K),
  x ∈ (ValuationRing.valuation A K).integer ↔ ∃ a, (algebraMap A K) a = x
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.rootSpan_ne_bot : ∀ {ι : Type u_1} {R : Type u_2} {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] (P : RootPairing ι R M N) (S : Type u_6)
  [inst_5 : CommRing S] [inst_6 : Module S M] [Nonempty ι] [NeZero 2], P.rootSpan S ≠ ⊥
-- Mathlib.RingTheory.RingInvo
/-- The identity function of a `CommRing` is a ring involution.  -/
RingInvo.id : (R : Type u_2) → [inst : CommRing R] → RingInvo R
-- Mathlib.Algebra.Group.Pointwise.Set.Card
Cardinal.mk_inv : ∀ {G : Type u_1} [inst : InvolutiveInv G] (s : Set G), Cardinal.mk ↑s⁻¹ = Cardinal.mk ↑s
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasurableEquiv.memLp_map_measure_iff : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_7}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] {β : Type u_8} {mβ : MeasurableSpace β} {g : β → ε}
  (f : α ≃ᵐ β), MeasureTheory.MemLp g p (MeasureTheory.Measure.map (⇑f) μ) ↔ MeasureTheory.MemLp (g ∘ ⇑f) p μ
-- Mathlib.Computability.TuringMachine.Tape
Turing.BlankExtends.above_of_le : ∀ {Γ : Type u_1} [inst : Inhabited Γ] {l l₁ l₂ : List Γ},
  Turing.BlankExtends l₁ l → Turing.BlankExtends l₂ l → l₁.length ≤ l₂.length → Turing.BlankExtends l₁ l₂
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
/-- The skeleton of a monomorphism `i : X ⟶ Y` of simplicial sets.
It sends `n : ℕ` to `Subcomplex.range i ⊔ Y.skeleton n`.
See `SSet.relativeCellComplexOfMono` for the main result regarding
this definition.
(Even though `[Mono i]` is technically not required in this definition,
the intended use of this definition and the corresponding API is
when `[Mono i]` holds.)  -/
SSet.skeletonOfMono : {X Y : SSet} → (X ⟶ Y) → ℕ →o Y.Subcomplex
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.pullHom'_ofDescentData_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} (sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j))
  (sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)) (D : F.DescentData f)
  ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂)
  (hf₁ :
    autoParam (CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q)
      CategoryTheory.Pseudofunctor.DescentData'.pullHom'_ofDescentData_hom._auto_1)
  (hf₂ :
    autoParam (CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q)
      CategoryTheory.Pseudofunctor.DescentData'.pullHom'_ofDescentData_hom._auto_3),
  CategoryTheory.Pseudofunctor.DescentData'.pullHom'
      (CategoryTheory.Pseudofunctor.DescentData'.ofDescentData sq sq₃ D).hom q f₁ f₂ hf₁ hf₂ =
    D.hom q f₁ f₂ hf₁ hf₂
-- Mathlib.Analysis.Normed.Operator.NormedSpace
ContinuousLinearEquiv.nnnorm_symm_pos : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_3} {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜}
  [inst_6 : RingHomInvPair σ₁₂ σ₂₁] [inst_7 : RingHomInvPair σ₂₁ σ₁₂] [inst_8 : RingHomIsometric σ₂₁]
  [RingHomIsometric σ₁₂] [Nontrivial E] (e : E ≃SL[σ₁₂] F), 0 < ‖↑e.symm‖₊
-- Std.Sat.AIG.CachedLemmas
/-- The AIG produced by `AIG.mkGateCached` agrees with the input AIG on all indices that are valid for
both.
 -/
Std.Sat.AIG.mkGateCached_decl_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig : Std.Sat.AIG α) (input : aig.BinaryInput) (idx : ℕ)
  (h1 : idx < (aig.mkGateCached input).aig.decls.size) (h2 : idx < aig.decls.size),
  (aig.mkGateCached input).aig.decls[idx] = aig.decls[idx]
-- Mathlib.Algebra.Category.Ring.Basic
CommRingCat.commRing : (self : CommRingCat) → CommRing ↑self
-- Mathlib.CategoryTheory.Simple
/-- We don't want the definition of 'simple' to include the zero object, so we check that here.  -/
CategoryTheory.zero_not_simple : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Simple 0], False
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffSection.coe_smul : ∀ {𝕜 : 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] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] [inst_11 : (x : M) → AddCommGroup (V x)]
  [inst_12 : (x : M) → Module 𝕜 (V x)] [inst_13 : VectorBundle 𝕜 F V] (r : 𝕜) (s : ContMDiffSection I F n V),
  ⇑(r • s) = r • ⇑s
-- Mathlib.Analysis.Normed.Module.Extr
/-- If `f : α → E` is a function such that `norm ∘ f` has a local maximum on a set `s` at a point
`c`, then the function `fun x => ‖f x + f c‖` has a local maximum on `s` at `c`.  -/
IsLocalMaxOn.norm_add_self : ∀ {X : Type u_2} {E : Type u_3} [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] [inst_2 : TopologicalSpace X]
  {f : X → E} {s : Set X} {c : X}, IsLocalMaxOn (norm ∘ f) s c → IsLocalMaxOn (fun x => ‖f x + f c‖) s c
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
CFC.negPart_mul_posPart : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : Module ℝ A] [inst_2 : SMulCommClass ℝ A A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : StarRing A] [inst_5 : TopologicalSpace A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A), a⁻ * a⁺ = 0
-- Mathlib.Geometry.Convex.ConvexSpace.AffineMap
Convexity.ConvexSpace.AffineMap.comp_apply : ∀ {R : Type u_1} [inst : PartialOrder R] [inst_1 : Semiring R] [inst_2 : IsStrictOrderedRing R] {X : Type u_2}
  {Y : Type u_3} {Z : Type u_4} [inst_3 : Convexity.ConvexSpace R X] [inst_4 : Convexity.ConvexSpace R Y]
  [inst_5 : Convexity.ConvexSpace R Z] (g : Convexity.ConvexSpace.AffineMap R Y Z)
  (f : Convexity.ConvexSpace.AffineMap R X Y) (a : X), (g.comp f) a = (⇑g ∘ ⇑f) a
-- Mathlib.Algebra.Algebra.Spectrum.Basic
/-- The unit `1 - r⁻¹ • a` constructed from `r • 1 - a` when the latter is a unit.  -/
IsUnit.subInvSMul : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : Ring A] →
        [inst_2 : Algebra R A] → {r : Rˣ} → {s : R} → {a : A} → IsUnit (r • (algebraMap R A) s - a) → Aˣ
-- Mathlib.RingTheory.Spectrum.Maximal.Localization
MaximalSpectrum.finite_of_toPiLocalization_surjective : ∀ {R : Type u_1} [inst : CommSemiring R],
  Function.Surjective ⇑(MaximalSpectrum.toPiLocalization R) → Finite (MaximalSpectrum R)
-- Mathlib.Data.Option.Defs
Option.elim'_some : ∀ {α : Type u_1} {β : Type u_2} {a : α} (b : β) (f : α → β), Option.elim' b f (some a) = f a
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.monomial_left_inj : ∀ {R : Type u_5} [inst : Semiring R] {a : R},
  a ≠ 0 → ∀ {i j : ℕ}, (SkewPolynomial.monomial i) a = (SkewPolynomial.monomial j) a ↔ i = j
-- Mathlib.Analysis.Calculus.LineDeriv.Measurable
measurableSet_lineDifferentiableAt_uncurry : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [LocallyCompactSpace 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : MeasurableSpace E] [OpensMeasurableSpace E]
  {F : Type u_3} [inst_6 : NormedAddCommGroup F] [inst_7 : NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F}
  [SecondCountableTopology E], Continuous f → MeasurableSet {p | LineDifferentiableAt 𝕜 f p.1 p.2}
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDeriv_const_add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {f : 𝕜 → F},
  0 < n → ∀ (c : F), iteratedDeriv n (fun z => c + f z) x = iteratedDeriv n f x
-- Mathlib.Analysis.Normed.Group.Real
Real.enorm_of_nonneg : ∀ {r : ℝ}, 0 ≤ r → ‖r‖ₑ = ENNReal.ofReal r
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.add_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (x : α)
  [inst_2 : AddZeroClass β] [inst_3 : ContinuousAdd β] (f g : CompactlySupportedContinuousMap α β),
  (f + g) x = f x + g x
-- Mathlib.CategoryTheory.Elements
CategoryTheory.Functor.Elements.precomp_obj_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{u_2, u_1} D]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D (Type w)) (x : (F.comp G).Elements),
  ((CategoryTheory.Functor.Elements.precomp F G).obj x).snd = x.snd
-- Mathlib.Computability.StateTransition
StateTransition.tr_eval' : ∀ {σ₁ σ₂ : Type u_1} (f₁ : σ₁ → Option σ₁) (f₂ : σ₂ → Option σ₂) (tr : σ₁ → σ₂),
  (StateTransition.Respects f₁ f₂ fun a b => tr a = b) →
    ∀ (a₁ : σ₁), StateTransition.eval f₂ (tr a₁) = tr <$> StateTransition.eval f₁ a₁
-- Mathlib.CategoryTheory.Category.Cat.Op
/-- The natural isomorphism between the double application of `Cat.opFunctor` and the
identity functor on `Cat`.  -/
CategoryTheory.Cat.opFunctorInvolutive : CategoryTheory.Cat.opFunctor.comp CategoryTheory.Cat.opFunctor ≅ CategoryTheory.Functor.id CategoryTheory.Cat
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.face_singleton_compl : ∀ {n : ℕ} (i : Fin (n + 2)),
  SSet.stdSimplex.face {i}ᶜ = SSet.Subcomplex.ofSimplex (SSet.stdSimplex.objEquiv.symm (SimplexCategory.δ i))
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.mulLeft.congr_simp : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : SeparatelyContinuousMul G] (a a_1 : G),
  a = a_1 → Homeomorph.mulLeft a = Homeomorph.mulLeft a_1
-- Mathlib.RingTheory.Finiteness.Basic
/-- If a ring `R` is finite over a subring `S` then the `R`-span of an FG `S`-submodule is FG.  -/
Submodule.FG.span : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_3}
  [inst_3 : Semiring A] [inst_4 : Module R A] [inst_5 : Module A M] [IsScalarTower R A M] {S : Submodule R M},
  S.FG → (Submodule.span A ↑S).FG
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.mem_iff_isSome_getKey? : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {a : α}, a ∈ m ↔ (m.getKey? a).isSome = true
-- Init.Data.Vector.Algebra
Vector.instAddRightCancel : ∀ {α : Type u_1} {n : ℕ} [inst : Add α] [Lean.Grind.AddRightCancel α], Lean.Grind.AddRightCancel (Vector α n)
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction
ModuleCat.extendScalars_η : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
  CategoryTheory.Functor.OplaxMonoidal.η (ModuleCat.extendScalars f) =
    ModuleCat.ofHom ↑(TensorProduct.AlgebraTensorModule.rid R S S)
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.tmul_pow : ∀ {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] (a : A) (b : B) (k : ℕ), a ⊗ₜ[R] b ^ k = (a ^ k) ⊗ₜ[R] (b ^ k)
-- Mathlib.AlgebraicGeometry.Gluing
_private.Mathlib.AlgebraicGeometry.Gluing.0.AlgebraicGeometry.Scheme.GlueData.«term𝖣» : Lean.ParserDescr
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.erase.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k k_1 : α),
  k = k_1 →
    ∀ (t : Std.DTreeMap.Internal.Impl α β) (h : t.Balanced),
      Std.DTreeMap.Internal.Impl.erase k t h = Std.DTreeMap.Internal.Impl.erase k_1 t h
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
CategoryTheory.Limits.IsIndObject.iff_of_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : CategoryTheory.Functor Cᵒᵖ (Type v)} (η : A ⟶ B)
  [CategoryTheory.IsIso η], CategoryTheory.Limits.IsIndObject A ↔ CategoryTheory.Limits.IsIndObject B
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.Cover.gluedCoverT'_snd_snd_assoc : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.I₀) {Z : AlgebraicGeometry.Scheme} (h : 𝒰.X x ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.gluedCoverT' 𝒰 x y z)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (𝒰.f y) (𝒰.f z))
          (CategoryTheory.Limits.pullback.fst (𝒰.f y) (𝒰.f x)))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (𝒰.f y) (𝒰.f x)) h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y))
        (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f z)))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y)) h)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.associator_hom : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] (P Q R : C),
  (CategoryTheory.Limits.biprod.associator P Q R).hom =
    CategoryTheory.Limits.biprod.lift
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.fst)
      (CategoryTheory.Limits.biprod.lift
        (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.snd)
        CategoryTheory.Limits.biprod.snd)
-- Lean.Parser.Basic
Lean.Parser.instBEqOrElseOnAntiquotBehavior : BEq Lean.Parser.OrElseOnAntiquotBehavior
-- Aesop.Tracing
Aesop.TraceOption.forwardDebug : Aesop.TraceOption
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
UniqueFactorizationMonoid.exists_mem_normalizedFactors : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizationMonoid α] [inst_2 : UniqueFactorizationMonoid α]
  {x : α}, x ≠ 0 → ¬IsUnit x → ∃ p, p ∈ UniqueFactorizationMonoid.normalizedFactors x
-- Lean.Meta.Tactic.Grind.Attr
Lean.Meta.Grind.AttrKind.ematch.inj : ∀ {k k_1 : Lean.Meta.Grind.EMatchTheoremKind},
  Lean.Meta.Grind.AttrKind.ematch k = Lean.Meta.Grind.AttrKind.ematch k_1 → k = k_1
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey_union_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : α → Type v} {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (not_mem : k ∉ m₁)
  {h' : k ∈ m₁ ∪ m₂}, (m₁ ∪ m₂).getKey k h' = m₂.getKey k ⋯
-- Mathlib.Data.Set.Sigma
biInf_sigma' : ∀ {ι : Type u_1} {α : ι → Type u_3} {β : Type u_4} [inst : CompleteLattice β] (s : Set ι) (t : (i : ι) → Set (α i))
  (f : (i : ι) → α i → β), ⨅ i ∈ s, ⨅ j ∈ t i, f i j = ⨅ ij ∈ s.sigma t, f ij.fst ij.snd
-- Mathlib.LinearAlgebra.Projectivization.Cardinality
/-- The non-zero elements of `V` are equivalent to the product of `ℙ k V` with the units of `k`.  -/
Projectivization.nonZeroEquivProjectivizationProdUnits : (k : Type u_1) →
  (V : Type u_2) →
    [inst : DivisionRing k] →
      [inst_1 : AddCommGroup V] → [inst_2 : Module k V] → { v // v ≠ 0 } ≃ Projectivization k V × kˣ
-- Mathlib.Topology.Sober
isGenericPoint_def : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {S : Set α}, IsGenericPoint x S ↔ closure {x} = S
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioc_subset_Ioo_right : ∀ {α : Type u_2} {a b₁ b₂ : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α],
  b₁ < b₂ → Finset.Ioc a b₁ ⊆ Finset.Ioo a b₂
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.bijective_coweightMap : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7}
  [inst_5 : AddCommGroup M₂] [inst_6 : Module R M₂] [inst_7 : AddCommGroup N₂] [inst_8 : Module R N₂]
  {P : RootPairing ι R M N} {Q : RootPairing ι₂ R M₂ N₂} (self : P.Equiv Q), Function.Bijective ⇑(↑self).coweightMap
-- Mathlib.CategoryTheory.ShrinkYoneda
/-- `shrinkCoyoneda` at the morphism universe level is `coyoneda`.  -/
CategoryTheory.shrinkCoyonedaIsoCoyoneda : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.shrinkCoyoneda.{v, v, u} ≅ CategoryTheory.coyoneda
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
/-- In a σ-finite space, any measurable set of measure `> r` contains a measurable subset of
finite measure `> r`.  -/
MeasureTheory.Measure.exists_subset_measure_lt_top : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.SigmaFinite μ]
  {r : ENNReal}, MeasurableSet s → r < μ s → ∃ t, MeasurableSet t ∧ t ⊆ s ∧ r < μ t ∧ μ t < ⊤
-- Mathlib.MeasureTheory.Covering.Besicovitch
Besicovitch.SatelliteConfig.h : ∀ {α : Type u_1} [inst : MetricSpace α] {N : ℕ} {τ : ℝ} (self : Besicovitch.SatelliteConfig α N τ),
  Pairwise fun i j =>
    self.r i ≤ dist (self.c i) (self.c j) ∧ self.r j ≤ τ * self.r i ∨
      self.r j ≤ dist (self.c j) (self.c i) ∧ self.r i ≤ τ * self.r j
-- Mathlib.Data.Stream.Defs
/-- Given a stream of functions and a stream of values, apply `n`-th function to `n`-th value.  -/
Stream'.«term_⊛_» : Lean.TrailingParserDescr
-- Mathlib.Combinatorics.SimpleGraph.Sum
SimpleGraph.Iso.sumAssoc_comp_sumCongr : ∀ {U : Type u_1} {U' : Type u_2} {V : Type u_3} {V' : Type u_4} {W : Type u_5} {W' : Type u_6} {G : SimpleGraph V}
  {H : SimpleGraph W} {I : SimpleGraph U} {G' : SimpleGraph V'} {H' : SimpleGraph W'} {I' : SimpleGraph U'}
  (f : G ≃g G') (g : H ≃g H') (h : I ≃g I'),
  SimpleGraph.Iso.sumAssoc.comp ((f.sumCongr g).sumCongr h) = (f.sumCongr (g.sumCongr h)).comp SimpleGraph.Iso.sumAssoc
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.congr_simp : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] (σ σ_1 : R →+* S) (e_σ : σ = σ_1)
  {σ' σ'_1 : S →+* R} (e_σ' : σ' = σ'_1) [inst_2 : RingHomInvPair σ σ'] [inst_3 : RingHomInvPair σ' σ] (M : Type u_3)
  [inst_4 : TopologicalSpace M] [inst_5 : AddCommMonoid M] (M₂ : Type u_4) [inst_6 : TopologicalSpace M₂]
  [inst_7 : AddCommMonoid M₂] [inst_8 : Module R M] [inst_9 : Module S M₂], (M ≃SL[σ] M₂) = (M ≃SL[σ_1] M₂)
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.isBigOTVS_neg_right : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {l : Filter α} {f : α → E} {g : α → F} [ContinuousNeg F],
  f =O[𝕜; l] (-g) ↔ f =O[𝕜; l] g
-- Lean.Util.Trace
_private.Lean.Util.Trace.0.Lean.addTraceNode : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadTrace m] →
      [Lean.MonadRef m] →
        [Lean.AddMessageContext m] →
          Lean.PersistentArray Lean.TraceElem → Lean.TraceData → Lean.Syntax → Lean.MessageData → m Unit
-- Mathlib.Algebra.BigOperators.Finprod
/-- If the additive supports of `f` and `g` are finite, then the sum of `f i - g i`
equals the sum of `f i` minus the sum of `g i`.  -/
finsum_sub_distrib : ∀ {α : Type u_1} {G : Type u_4} [inst : SubtractionCommMonoid G] {f g : α → G},
  Function.HasFiniteSupport f →
    Function.HasFiniteSupport g → ∑ᶠ (i : α), (f i - g i) = ∑ᶠ (i : α), f i - ∑ᶠ (i : α), g i
-- Mathlib.FieldTheory.Normal.Basic
AlgEquiv.liftNormal_commutes : ∀ {F : Type u_1} [inst : Field F] {K₁ : Type u_3} {K₂ : Type u_4} [inst_1 : Field K₁] [inst_2 : Field K₂]
  [inst_3 : Algebra F K₁] [inst_4 : Algebra F K₂] (χ : K₁ ≃ₐ[F] K₂) (E : Type u_6) [inst_5 : Field E]
  [inst_6 : Algebra F E] [inst_7 : Algebra K₁ E] [inst_8 : Algebra K₂ E] [inst_9 : IsScalarTower F K₁ E]
  [inst_10 : IsScalarTower F K₂ E] [inst_11 : Normal F E] (x : K₁),
  (χ.liftNormal E) ((algebraMap K₁ E) x) = (algebraMap K₂ E) (χ x)
-- Std.Sat.CNF.Basic
Std.Sat.CNF.VarMem_of : ∀ {α : Type u_1} {f : Std.Sat.CNF α} {c : Std.Sat.CNF.Clause α} {v : α},
  c ∈ f → Std.Sat.CNF.Clause.Mem v c → Std.Sat.CNF.VarMem v f
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonRpcConnectParams : Lean.FromJson Lean.Lsp.RpcConnectParams
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.map_obj_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T T' : D} {S : CategoryTheory.Functor C D} (f : T ⟶ T')
  (X : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)),
  ((CategoryTheory.CostructuredArrow.map f).obj X).hom = CategoryTheory.CategoryStruct.comp X.hom f
-- Init.Data.Vector.Basic
Vector.instHAppendHAddNat : {α : Type u_1} → {n m : ℕ} → HAppend (Vector α n) (Vector α m) (Vector α (n + m))
-- Std.Data.Internal.List.Associative
Std.Internal.List.eraseList_perm_filter_not_contains : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] (l toErase : List ((a : α) × β a)),
  Std.Internal.List.DistinctKeys l →
    (Std.Internal.List.eraseList l (List.map Sigma.fst toErase)).Perm
      (List.filter (fun p => !(List.map Sigma.fst toErase).contains p.fst) l)
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.refl_trans : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂),
  (AffineIsometryEquiv.refl 𝕜 P).trans e = e
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.Answer.mk.inj : ∀ {result : Lean.Meta.AbstractMVarsResult} {resultType : Lean.Expr} {size : ℕ}
  {result_1 : Lean.Meta.AbstractMVarsResult} {resultType_1 : Lean.Expr} {size_1 : ℕ},
  { result := result, resultType := resultType, size := size } =
      { result := result_1, resultType := resultType_1, size := size_1 } →
    result = result_1 ∧ resultType = resultType_1 ∧ size = size_1
-- Mathlib.Data.Nat.Factorization.Basic
/-- **Alias** of `Nat.prod_primeFactors_coe_pow_factorization`. -/
Nat.prod_pow_primeFactors_factorization : ∀ {n : ℕ}, n ≠ 0 → n = ∏ p, ↑p ^ n.factorization ↑p
-- Mathlib.Algebra.Group.Submonoid.Pointwise
Submonoid.instCovariantClassHSMulLe : ∀ {α : Type u_1} {M : Type u_3} [inst : Monoid M] [inst_1 : Monoid α] [inst_2 : MulDistribMulAction α M],
  CovariantClass α (Submonoid M) HSMul.hSMul LE.le