mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.List.FinRange
List.finRange_zero : List.finRange 0 = []
-- Mathlib.Topology.LocalAtTarget
TopologicalSpace.IsOpenCover.isOpen_iff_inter : ∀ {β : Type u_2} [inst : TopologicalSpace β] {ι : Type u_3} {U : ι → TopologicalSpace.Opens β} {s : Set β},
  TopologicalSpace.IsOpenCover U → (IsOpen s ↔ ∀ (i : ι), IsOpen (s ∩ ↑(U i)))
-- Init.Data.String.Lemmas.Splits
String.Slice.Pos.Splits.cast : ∀ {s₁ s₂ : String.Slice} {p : s₁.Pos} {t₁ t₂ : String} (h : s₁.copy = s₂.copy), p.Splits t₁ t₂ → (p.cast h).Splits t₁ t₂
-- Mathlib.SetTheory.Lists
Lists.instSetoidLists : {α : Type u_1} → Setoid (Lists α)
-- Mathlib.Topology.ContinuousMap.Algebra
/-- Evaluation of a scalar-valued continuous map multiplying a vector-valued one
(as opposed to `ContinuousMap.smul_apply` which is multiplication by a constant scalar).  -/
ContinuousMap.smul_apply' : ∀ {α : Type u_1} [inst : TopologicalSpace α] {R : Type u_2} [inst_1 : Semiring R] [inst_2 : TopologicalSpace R]
  {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid M] [inst_5 : Module R M]
  [inst_6 : ContinuousSMul R M] (f : C(α, R)) (g : C(α, M)) (x : α), (f • g) x = f x • g x
-- Init.Data.Option.Attach
/-- “Attaches” a proof that an optional value, if present, is indeed this value, returning a subtype
that expresses this fact.

This function is primarily used to allow definitions by well-founded recursion that use iteration
operators (such as `Option.map`) to prove that an optional value drawn from a parameter is smaller
than the parameter. This allows the well-founded recursion mechanism to prove that the function
terminates.
 -/
Option.attach : {α : Type u_1} → (xs : Option α) → Option { x // xs = some x }
-- Mathlib.GroupTheory.GroupAction.Basic
AddAction.stabilizerEquivStabilizer_symm_apply : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {g : G} {a b : α} (hg : b = g +ᵥ a)
  (x : ↥(AddAction.stabilizer G b)), ↑((AddAction.stabilizerEquivStabilizer hg).symm x) = (AddAut.addConj (-g)) ↑x
-- Mathlib.Algebra.Module.Submodule.Range
/-- If `f : E →ₗ[R] F` has a left inverse `g`, then `range f = ker (f ∘ g - id)`.

This is the dual version of `LinearMap.ker_eq_range_of_comp_eq_id`.  -/
LinearMap.range_eq_ker_of_leftInverse : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_10} {P : Type u_11} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup P] [inst_4 : Module R P] {f : M →ₗ[R] P} {g : P →ₗ[R] M},
  Function.LeftInverse ⇑g ⇑f → f.range = (f ∘ₗ g - LinearMap.id).ker
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
SimplexCategoryGenRel.toSimplexCategory_len : ∀ {x : SimplexCategoryGenRel}, (SimplexCategoryGenRel.toSimplexCategory.obj x).len = x.len
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.natDegree_mod_lt : ∀ {k : Type y} [inst : Field k] (p : Polynomial k) {q : Polynomial k}, q.natDegree ≠ 0 → (p % q).natDegree < q.natDegree
-- Mathlib.Algebra.Group.WithOne.Defs
_private.Mathlib.Algebra.Group.WithOne.Defs.0.WithOne.unone.match_1.splitter : {α : Type u_1} →
  (motive : (x : WithOne α) → x ≠ 1 → Sort u_2) →
    (x : WithOne α) → (x_1 : x ≠ 1) → ((x : α) → (x_2 : ↑x ≠ 1) → motive (some x) x_2) → motive x x_1
-- Mathlib.Order.Bounded
Set.unbounded_inter_not : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α},
  (∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m) →
    ∀ (a : α), Set.Unbounded r (s ∩ {b | ¬r b a}) ↔ Set.Unbounded r s
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
/-- If `Irreducible (cyclotomic (p ^ n) R)` then `Irreducible (cyclotomic p R).`  -/
Polynomial.cyclotomic_irreducible_of_irreducible_pow : ∀ {p : ℕ},
  Nat.Prime p →
    ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] {n : ℕ},
      n ≠ 0 → Irreducible (Polynomial.cyclotomic (p ^ n) R) → Irreducible (Polynomial.cyclotomic p R)
-- Mathlib.Topology.Compactness.Lindelof
Quot.lindelofSpace : ∀ {X : Type u} [inst : TopologicalSpace X] {r : X → X → Prop} [LindelofSpace X], LindelofSpace (Quot r)
-- Mathlib.Data.Set.Image
Set.range_quotient_lift : ∀ {α : Type u_1} {ι : Sort u_4} {f : ι → α} [s : Setoid ι] (hf : ∀ (a b : ι), a ≈ b → f a = f b),
  Set.range (Quotient.lift f hf) = Set.range f
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
/-- Reindex a free group basis through a bijection of the indexing sets.  -/
FreeGroupBasis.reindex : {ι : Type u_1} → {ι' : Type u_2} → {G : Type u_3} → [inst : Group G] → FreeGroupBasis ι G → ι ≃ ι' → FreeGroupBasis ι' G
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.op_epi_of_mono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A B : C} (f : A ⟶ B) [CategoryTheory.Mono f],
  CategoryTheory.Epi f.op
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
add_lt_add_right : ∀ {α : Type u_1} [inst : Add α] [inst_1 : LT α] [AddLeftStrictMono α] {b c : α}, b < c → ∀ (a : α), a + b < a + c
-- Mathlib.Combinatorics.SimpleGraph.Operations
SimpleGraph.sup_edge_self : ∀ {V : Type u_1} (G : SimpleGraph V) (s : V), G ⊔ SimpleGraph.edge s s = G
-- Mathlib.CategoryTheory.Limits.Types.Pushouts
CategoryTheory.Limits.Types.Pushout.Rel'.symm : ∀ {S X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} {x y : X₁ ⊕ X₂},
  CategoryTheory.Limits.Types.Pushout.Rel' f g x y → CategoryTheory.Limits.Types.Pushout.Rel' f g y x
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.mk.inj : ∀ {α : Type u_5} {β : Type u_6} {inst : TopologicalSpace α} {inst_1 : Zero β} {inst_2 : TopologicalSpace β}
  {toContinuousMap : C(α, β)} {hasCompactSupport' : HasCompactSupport toContinuousMap.toFun}
  {toContinuousMap_1 : C(α, β)} {hasCompactSupport'_1 : HasCompactSupport toContinuousMap_1.toFun},
  { toContinuousMap := toContinuousMap, hasCompactSupport' := hasCompactSupport' } =
      { toContinuousMap := toContinuousMap_1, hasCompactSupport' := hasCompactSupport'_1 } →
    toContinuousMap = toContinuousMap_1
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.mul_def : ∀ (α β : Type u), Cardinal.mk α * Cardinal.mk β = Cardinal.mk (α × β)
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.instInhabited : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : Zero β] → Inhabited (ZeroAtInftyContinuousMap α β)
-- Mathlib.Geometry.RingedSpace.Basic
/-- The zero locus of a set of sections `s` over an open set `U` is the closed set consisting of
the complement of `U` and of all points of `U`, where all elements of `f` vanish.
 -/
AlgebraicGeometry.RingedSpace.zeroLocus : (X : AlgebraicGeometry.RingedSpace) →
  {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} → Set ↑(X.presheaf.obj (Opposite.op U)) → Set ↑↑X.toPresheafedSpace
-- Mathlib.Data.List.ProdSigma
List.mem_sigma : ∀ {α : Type u_1} {σ : α → Type u_3} {l₁ : List α} {l₂ : (a : α) → List (σ a)} {a : α} {b : σ a},
  ⟨a, b⟩ ∈ l₁.sigma l₂ ↔ a ∈ l₁ ∧ b ∈ l₂ a
-- Mathlib.Topology.FiberBundle.Constructions
Bundle.Trivialization.Prod.continuous_to_fun : ∀ {B : Type u_1} [inst : TopologicalSpace B] {F₁ : Type u_2} [inst_1 : TopologicalSpace F₁] {E₁ : B → Type u_3}
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_4} [inst_3 : TopologicalSpace F₂]
  {E₂ : B → Type u_5} [inst_4 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  {e₁ : Bundle.Trivialization F₁ Bundle.TotalSpace.proj} {e₂ : Bundle.Trivialization F₂ Bundle.TotalSpace.proj},
  ContinuousOn (Bundle.Trivialization.Prod.toFun' e₁ e₂) (Bundle.TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet))
-- Mathlib.LinearAlgebra.Dual.Defs
Module.dualPairing_apply : ∀ (R : Type u_1) (M : Type u_3) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (v : Module.Dual R M) (x : M), ((Module.dualPairing R M) v) x = v x
-- Mathlib.CategoryTheory.Monad.Monadicity
CategoryTheory.Monad.instPreservesColimitWalkingParallelPairParallelPairOfIsReflexivePairOfPreservesColimitOfIsReflexivePair : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {G : CategoryTheory.Functor D C} {A B : D} (f g : A ⟶ B) [CategoryTheory.IsReflexivePair f g]
  [CategoryTheory.Monad.PreservesColimitOfIsReflexivePair G],
  CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.type_set_le : ∀ {α : Type u} [inst : LinearOrder α] [inst_1 : WellFoundedLT α] (s : Set α),
  (Ordinal.type fun x1 x2 => x1 < x2) ≤ Ordinal.type fun x1 x2 => x1 < x2
-- Mathlib.Dynamics.Ergodic.MeasurePreserving
MeasureTheory.MeasurePreserving.map_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : α → β}
  {μa : autoParam (MeasureTheory.Measure α) MeasureTheory.MeasurePreserving._auto_1}
  {μb : autoParam (MeasureTheory.Measure β) MeasureTheory.MeasurePreserving._auto_3},
  MeasureTheory.MeasurePreserving f μa μb → MeasureTheory.Measure.map f μa = μb
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.inverse_obj_hom : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor T D) (Y : D) (X : T)
  (Y_1 : CategoryTheory.CostructuredArrow ((CategoryTheory.Over.forget X).comp F) Y),
  ((CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.inverse F Y X).obj Y_1).hom = Y_1.left.hom
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.balLeft.match_1.congr_eq_1 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (r : RBTree.RBNode α)
  (h_1 :
    (a : RBTree.RBNode α) → (y : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.black a y b))
  (h_2 :
    (a : RBTree.RBNode α) →
      (y : α) →
        (b : RBTree.RBNode α) →
          (z : α) →
            (c : RBTree.RBNode α) →
              motive (RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.black a y b) z c))
  (h_3 : (r : RBTree.RBNode α) → motive r) (a : RBTree.RBNode α) (y : α) (b : RBTree.RBNode α),
  r = RBTree.RBNode.node RBTree.RBColor.black a y b →
    (match r with
      | RBTree.RBNode.node RBTree.RBColor.black a y b => h_1 a y b
      | RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.black a y b) z c => h_2 a y b z c
      | r => h_3 r) ≍
      h_1 a y b
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
Delone.DeloneSet.mapIsometry_apply_packingRadius : ∀ {X : Type u_1} {Y : Type u_2} [inst : MetricSpace X] [inst_1 : MetricSpace Y] (f : X ≃ᵢ Y) (D : Delone.DeloneSet X),
  ((Delone.DeloneSet.mapIsometry f) D).packingRadius = D.packingRadius
-- Lean.Meta.ForEachExpr
/-- Given a sequence of let binders `let (x₁ : α₁ := v₁) ... in b`, runs `f` on each `αᵢ`, `vᵢ` and `b`.  -/
Lean.Meta.visitLet : {m : Type → Type u_1} → [Monad m] → [MonadControlT Lean.MetaM m] → (Lean.Expr → m Unit) → Lean.Expr → m Unit
-- Mathlib.RingTheory.Derivation.Basic
Derivation.liftOfRightInverse_apply : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : CommRing A] [inst_2 : CommRing M]
  [inst_3 : Algebra R A] [inst_4 : Algebra R M] {F : Type u_4} [inst_5 : FunLike F A M] [inst_6 : AlgHomClass F R A M]
  {f : F} {f_inv : M → A} (hf : Function.RightInverse f_inv ⇑f) {d : Derivation R A A}
  (hd : ∀ (x : A), f x = 0 → f (d x) = 0) (x : A), (Derivation.liftOfRightInverse hf hd) (f x) = f (d x)
-- Init.Data.UInt.Lemmas
USize.toUInt64_ofNat' : ∀ {n : ℕ}, n < USize.size → (USize.ofNat n).toUInt64 = UInt64.ofNat n
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- A copy gives rise to a homomorphism.  -/
SimpleGraph.Copy.toHom : {α : Type u_4} → {β : Type u_5} → {A : SimpleGraph α} → {B : SimpleGraph β} → A.Copy B → A →g B
-- Mathlib.Analysis.Normed.Lp.lpSpace
/-- `lp.single` as a continuous morphism of additive monoids.  -/
lp.singleContinuousAddMonoidHom : {α : Type u_3} →
  (E : α → Type u_4) →
    (p : ENNReal) →
      [inst : (i : α) → NormedAddCommGroup (E i)] →
        [DecidableEq α] → [inst_2 : Fact (1 ≤ p)] → (i : α) → E i →ₜ+ ↥(lp E p)
-- Std.Data.DHashMap.RawLemmas
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw.tacticSimp_to_rawUsing_ : Lean.ParserDescr
-- Mathlib.Probability.Kernel.Disintegration.Integral
ProbabilityTheory.setLIntegral_condKernel_eq_measure_prod : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω] [inst_2 : Nonempty Ω]
  [inst_3 : MeasurableSpace.CountableOrCountablyGenerated α β] {κ : ProbabilityTheory.Kernel α (β × Ω)}
  [inst_4 : ProbabilityTheory.IsFiniteKernel κ] (a : α) {s : Set β},
  MeasurableSet s → ∀ {t : Set Ω}, MeasurableSet t → ∫⁻ (b : β) in s, (κ.condKernel (a, b)) t ∂κ.fst a = (κ a) (s ×ˢ t)
-- Init.Data.List.Lemmas
List.append_eq_filterMap_iff : ∀ {α : Type u_1} {β : Type u_2} {L₁ L₂ : List β} {l : List α} {f : α → Option β},
  L₁ ++ L₂ = List.filterMap f l ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ List.filterMap f l₁ = L₁ ∧ List.filterMap f l₂ = L₂
-- Init.Data.BitVec.Lemmas
BitVec.toInt_twoPow : ∀ {w i : ℕ}, (BitVec.twoPow w i).toInt = if w ≤ i then 0 else if i + 1 = w then -↑(2 ^ i) else 2 ^ i
-- Mathlib.CategoryTheory.Limits.Types.Pullbacks
CategoryTheory.Limits.Types.pullbackIsoPullback_inv_fst_apply : ∀ {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) (x : CategoryTheory.Limits.Types.PullbackObj f g),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.fst f g))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Types.pullbackIsoPullback f g).inv) x) =
    (↑x).1
-- Mathlib.Order.Heyting.Basic
IsCompl.compl_eq : ∀ {α : Type u_2} [inst : HeytingAlgebra α] {a b : α}, IsCompl a b → aᶜ = b
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.notCore.injEq : ∀ (e : Lean.Expr) (lhs rhs : Lean.Meta.Grind.Arith.Linear.LinExpr) (e_1 : Lean.Expr)
  (lhs_1 rhs_1 : Lean.Meta.Grind.Arith.Linear.LinExpr),
  (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.notCore e lhs rhs =
      Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.notCore e_1 lhs_1 rhs_1) =
    (e = e_1 ∧ lhs = lhs_1 ∧ rhs = rhs_1)
-- Mathlib.FieldTheory.Galois.GaloisClosure
FiniteGaloisIntermediateField.finiteDimensional : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K]
  (self : FiniteGaloisIntermediateField k K), FiniteDimensional k ↥self.toIntermediateField
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.unit.eq_1 : ∀ {n : ℕ} (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
  Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.unit l = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
-- Mathlib.RingTheory.NormalClosure
Ring.instIsScalarTowerSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsDomain R] [inst_3 : IsDomain S]
  [inst_4 : Algebra R S] [inst_5 : Module.IsTorsionFree R S],
  IsScalarTower R S
    ↥(IntermediateField.normalClosure (FractionRing R) (FractionRing S) (AlgebraicClosure (FractionRing S)))
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extend.homologyData_iso : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {i j k : ι}
  {i' j' k' : ι'} (hj' : e.f j = j') (hi : c.prev j = i) (hi' : c'.prev j' = i') (hk : c.next j = k)
  (hk' : c'.next j' = k') (h : (K.sc' i j k).HomologyData),
  (HomologicalComplex.extend.homologyData K e hj' hi hi' hk hk' h).iso = h.iso
-- Mathlib.RingTheory.Ideal.Pointwise
Ideal.smul_mem_pointwise_smul : ∀ {M : Type u_1} {R : Type u_3} [inst : Monoid M] [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R] (m : M) (r : R)
  (S : Ideal R), r ∈ S → m • r ∈ m • S
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.ofRestrict_c_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {U : TopCat} (X : AlgebraicGeometry.PresheafedSpace C)
  {f : U ⟶ ↑X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f))
  (V : (TopologicalSpace.Opens ↑↑X)ᵒᵖ),
  (X.ofRestrict h).c.app V = X.presheaf.map (⋯.adjunction.counit.app (Opposite.unop V)).op
-- Mathlib.Order.Category.FinBddDistLat
finBddDistLat_dual_comp_forget_to_bddDistLat : FinBddDistLat.dual.comp (CategoryTheory.forget₂ FinBddDistLat BddDistLat) =
  (CategoryTheory.forget₂ FinBddDistLat BddDistLat).comp BddDistLat.dual
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.image_mem_functorPushforward : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X : C} (R : CategoryTheory.Sieve X) {V : C} {f : V ⟶ X},
  R.arrows f → (CategoryTheory.Sieve.functorPushforward F R).arrows (F.map f)
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived
CategoryTheory.LocalizerMorphism.rightDerivedFunctorComparison.congr_simp : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {H : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} H] {D₁ : Type u₄}
  {D₂ : Type u₅} [inst_3 : CategoryTheory.Category.{v₄, u₄} D₁] [inst_4 : CategoryTheory.Category.{v₅, u₅} D₂]
  {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂}
  (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (L₁ : CategoryTheory.Functor C₁ D₁) (L₂ : CategoryTheory.Functor C₂ D₂)
  [inst_5 : L₁.IsLocalization W₁] [inst_6 : L₂.IsLocalization W₂] (F : CategoryTheory.Functor C₂ H)
  (F₁ : CategoryTheory.Functor D₁ H) (α₁ α₁_1 : Φ.functor.comp F ⟶ L₁.comp F₁) (e_α₁ : α₁ = α₁_1)
  (F₂ : CategoryTheory.Functor D₂ H) (α₂ α₂_1 : F ⟶ L₂.comp F₂),
  α₂ = α₂_1 →
    ∀ [inst_7 : F₁.IsRightDerivedFunctor α₁ W₁],
      Φ.rightDerivedFunctorComparison L₁ L₂ F F₁ α₁ F₂ α₂ = Φ.rightDerivedFunctorComparison L₁ L₂ F F₁ α₁_1 F₂ α₂_1
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Multiset.stronglyMeasurable_fun_sum : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] [ContinuousAdd M]
  {m : MeasurableSpace α} (s : Multiset (α → M)),
  (∀ f ∈ s, MeasureTheory.StronglyMeasurable f) →
    MeasureTheory.StronglyMeasurable fun x => (Multiset.map (fun f => f x) s).sum
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
/-- A class for the non-unital continuous functional calculus which requires the homomorphisms
`C(quasispectrum R a, R)₀ → A` to be closed embeddings, as opposed to only continuous and injective.
The primary advantage of this is that one can conclude the range of this map is the non-unital
closed star subalgebra generated by `a`. However, unless the topology on `A` is induced by a
C⋆-norm, this is unlikely to occur.  -/
NonUnitalClosedEmbeddingContinuousFunctionalCalculus : (R : Type u_1) →
  (A : Type u_2) →
    outParam (A → Prop) →
      [inst : CommSemiring R] →
        [Nontrivial R] →
          [inst_2 : StarRing R] →
            [inst_3 : MetricSpace R] →
              [IsTopologicalSemiring R] →
                [ContinuousStar R] →
                  [inst_6 : NonUnitalRing A] →
                    [StarRing A] →
                      [TopologicalSpace A] →
                        [inst_9 : Module R A] → [IsScalarTower R A A] → [SMulCommClass R A A] → Prop
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.Const.minEntry.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : (x : Std.DTreeMap.Internal.Impl α fun x => β) → x.isEmpty = false → Sort u_3) →
      (x : Std.DTreeMap.Internal.Impl α fun x => β) →
        (x_1 : x.isEmpty = false) →
          ((size : ℕ) →
              (k : α) →
                (v : β) →
                  (r : Std.DTreeMap.Internal.Impl α fun x => β) →
                    (x :
                        (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r).isEmpty = false) →
                      motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x) →
            ((size : ℕ) →
                (k : α) →
                  (v : β) →
                    (size_1 : ℕ) →
                      (k_1 : α) →
                        (v_1 : β) →
                          (l r r_1 : Std.DTreeMap.Internal.Impl α fun x => β) →
                            (h :
                                (Std.DTreeMap.Internal.Impl.inner size k v
                                      (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1).isEmpty =
                                  false) →
                              motive
                                (Std.DTreeMap.Internal.Impl.inner size k v
                                  (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1)
                                h) →
              motive x x_1
-- Mathlib.LinearAlgebra.Matrix.ToLin
Algebra.toMatrix_lmul' : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {m : Type u_3}
  [inst_3 : Fintype m] [inst_4 : DecidableEq m] (b : Module.Basis m R S) (x : S) (i j : m),
  (LinearMap.toMatrix b b) ((Algebra.lmul R S) x) i j = (b.repr (x * b j)) i
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.instPrespectralSpace : ∀ {R : Type u} [inst : CommSemiring R], PrespectralSpace (PrimeSpectrum R)
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite
CategoryTheory.Limits.createsColimitsOfShapeOfCreatesFiniteColimits : {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.Limits.CreatesFiniteColimits F] →
            (J : Type w) →
              [inst_3 : CategoryTheory.SmallCategory J] →
                [CategoryTheory.FinCategory J] → CategoryTheory.CreatesColimitsOfShape J F
-- Mathlib.Analysis.Calculus.DerivativeTest
/-- The First-Derivative Test from calculus, maxima version.
Suppose `a < b < c`, `f : ℝ → ℝ` is continuous at `b`, the derivative `f'` is nonnegative on
`Ioo a b` and nonpositive on `Ioo b c`. Then `f` has a local maximum at `b`.  -/
isLocalMax_of_deriv_Ioo : ∀ {f : ℝ → ℝ} {a b c : ℝ},
  a < b →
    b < c →
      ContinuousAt f b →
        DifferentiableOn ℝ f (Set.Ioo a b) →
          DifferentiableOn ℝ f (Set.Ioo b c) →
            (∀ x ∈ Set.Ioo a b, 0 ≤ deriv f x) → (∀ x ∈ Set.Ioo b c, deriv f x ≤ 0) → IsLocalMax f b
-- Mathlib.Algebra.BigOperators.Finprod
finsum_set_coe_eq_finsum_mem : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} (s : Set α),
  ∑ᶠ (j : ↑s), f ↑j = ∑ᶠ (i : α) (_ : i ∈ s), f i
-- Mathlib.Order.Max
isBot_ofDual_iff : ∀ {α : Type u_1} [inst : LE α] {a : αᵒᵈ}, IsBot (OrderDual.ofDual a) ↔ IsTop a
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.DateBuilder.Q : Std.Time.GenericFormat.DateBuilder✝ → Option Std.Time.Month.Quarter
-- Mathlib.RingTheory.Localization.NormTrace
/-- Let `S` be an extension of `R` and `Rₘ Sₘ` be localizations at `M` of `R S` respectively.
Then the trace of `a : Sₘ` over `Rₘ` is the trace of `a : S` over `R` if `S` is free as `R`-module.
 -/
Algebra.trace_localization : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {Rₘ : Type u_3}
  {Sₘ : Type u_4} [inst_3 : CommRing Rₘ] [inst_4 : Algebra R Rₘ] [inst_5 : CommRing Sₘ] [inst_6 : Algebra S Sₘ]
  (M : Submonoid R) [IsLocalization M Rₘ] [IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ] [inst_9 : Algebra Rₘ Sₘ]
  [inst_10 : Algebra R Sₘ] [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ] [Module.Free R S] [Module.Finite R S] (a : S),
  (Algebra.trace Rₘ Sₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) ((Algebra.trace R S) a)
-- Mathlib.LinearAlgebra.AffineSpace.Centroid
/-- In the characteristic zero case, the weights in the centroid sum
to 1 if the number of points is not zero.  -/
Finset.sum_centroidWeights_eq_one_of_card_ne_zero : ∀ (k : Type u_1) [inst : DivisionRing k] {ι : Type u_4} (s : Finset ι) [CharZero k],
  s.card ≠ 0 → ∑ i ∈ s, Finset.centroidWeights k s i = 1