mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
/-- Auxiliary lemma for `rnDeriv_withDensity_right`.  -/
MeasureTheory.Measure.rnDeriv_withDensity_withDensity_rnDeriv_right : ∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → ENNReal} (μ ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ]
  [MeasureTheory.SigmaFinite ν],
  AEMeasurable f ν →
    (∀ᵐ (x : α) ∂ν, f x ≠ 0) →
      (∀ᵐ (x : α) ∂ν, f x ≠ ⊤) →
        (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᵐ[ν] μ.rnDeriv (ν.withDensity f)
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_control_apply_eq : ∀ {n : Type u_1 → Type u_2} {m : Type u_1 → Type u_3} {Pred : Type u_4} {EPred : Type u_5} {α : Type u_1}
  {post : α → Pred} {epost : EPred} [inst : Bind n] [Monad m] [Monad n] [inst_3 : Std.Internal.Do.Assertion Pred]
  [inst_4 : Std.Internal.Do.Assertion EPred] [inst_5 : (α : Type u_1) → Std.Internal.Do.WP (n α) α Pred EPred]
  [inst_6 : MonadControlT m n] (f : ({β : Type u_1} → n β → m (stM m n β)) → m (stM m n α)),
  Std.Internal.Do.wp (control f) post epost = Std.Internal.Do.wp (liftWith f >>= restoreM) post epost
-- Mathlib.Topology.FiberBundle.Basic
FiberBundleCore.mem_localTriv_target : ∀ {ι : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  (Z : FiberBundleCore ι B F) (i : ι) (p : B × F), p ∈ (Z.localTriv i).target ↔ p.1 ∈ (Z.localTriv i).baseSet
-- Mathlib.RingTheory.Spectrum.Prime.Basic
/-- The prime spectrum of `R × S` is in bijection with the disjoint unions of the prime spectrum of
`R` and the prime spectrum of `S`.  -/
PrimeSpectrum.primeSpectrumProd : (R : Type u) →
  (S : Type v) →
    [inst : CommSemiring R] → [inst_1 : CommSemiring S] → PrimeSpectrum (R × S) ≃ PrimeSpectrum R ⊕ PrimeSpectrum S
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval₂_C : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (f : R →+* S₁)
  (g : σ → S₁) (a : R), MvPolynomial.eval₂ f g (MvPolynomial.C a) = f a
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.coe_div : ∀ {α : Type u_1} [inst : Div α] (a b : α), ↑(a / b) = ↑a / ↑b
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.instIsBoundedSMul : ∀ (p : ENNReal) (𝕜 : Type u_1) {ι : Type u_2} (β : ι → Type u_4) [hp : Fact (1 ≤ p)] [inst : Fintype ι]
  [inst_1 : SeminormedRing 𝕜] [inst_2 : (i : ι) → SeminormedAddCommGroup (β i)] [inst_3 : (i : ι) → Module 𝕜 (β i)]
  [∀ (i : ι), IsBoundedSMul 𝕜 (β i)], IsBoundedSMul 𝕜 (PiLp p β)
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.const_add_beq_const : ∀ {w b : ℕ} {a : BitVec w} {c : ℕ},
  (BitVec.ofNat w b + a == BitVec.ofNat w c) = (a == BitVec.ofNat w c - BitVec.ofNat w b)
-- Mathlib.Order.Interval.Set.Monotone
Monotone.Ioo : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f g : α → β},
  Monotone f → Antitone g → Antitone fun x => Set.Ioo (f x) (g x)
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.smulCommClass : ∀ {R : Type u_1} {M : Type u_4} {N : Type u_5} {O : Type u_6} [inst : Semiring R] [inst_1 : SMulZeroClass N R]
  [inst_2 : SMulZeroClass O R] [SMulCommClass N O R], SMulCommClass N O (AddMonoidAlgebra R M)
-- Mathlib.Algebra.Star.Unitary
/-- In a star monoid, the product `a⁻¹ * b` of units is unitary if `a * star a = b * star b`.  -/
Units.inv_mul_mem_unitary : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] (a b : Rˣ), ↑a⁻¹ * ↑b ∈ unitary R ↔ a * star a = b * star b
-- Mathlib.Order.BoundedOrder.Basic
ULift.instOrderBot : {α : Type u} → [inst : LE α] → [OrderBot α] → OrderBot (ULift.{v, u} α)
-- Mathlib.RingTheory.Valuation.Integers
Valuation.Integers.bijective_algebraMap_of_subsingleton_units_mrange : ∀ {F : Type u} {Γ₀ : Type v} [inst : Field F] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {v : Valuation F Γ₀}
  {O : Type w} [inst_2 : CommRing O] [inst_3 : Algebra O F],
  v.Integers O → ∀ [Subsingleton (↥(MonoidHom.mrange v))ˣ], Function.Bijective ⇑(algebraMap O F)
-- Mathlib.Data.Set.Semiring
Set.up_empty : ∀ {α : Type u_1}, Set.up ∅ = 0
-- Mathlib.Tactic.SetNotationForOrder
/-- This relation is an implementation detail of the `⊆` elaborator.  -/
Mathlib.Meta.SetNotationForOrder.SubsetElabAux : {α : Type u} → α → α → Prop
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurableSet_lt_le : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
  {τ : Ω → WithTop ι} [inst_1 : TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι],
  MeasureTheory.IsStoppingTime f τ → ∀ {i j : ι}, i ≤ j → MeasurableSet {ω | τ ω < ↑i}
-- Mathlib.Algebra.Group.Graph
MonoidHom.graph_eq_range_prod : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] (f : G →* H),
  f.graph = ((MonoidHom.id G).prod f).range
-- Std.Time.Internal.Bounded
Std.Time.Internal.Bounded.LE.truncateTop.eq_1 : ∀ {n m j : ℤ} (bounded : Std.Time.Internal.Bounded.LE n m) (h : ↑bounded ≤ j), bounded.truncateTop h = ⟨↑bounded, ⋯⟩
-- Mathlib.Order.Filter.AtTopBot.Archimedean
Filter.map_sub_atTop_eq : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] [IsDirectedOrder α] (k : α),
  Filter.map (fun a => a - k) Filter.atTop = Filter.atTop
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem!_map_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited γ] {f : α → β → γ} {k k' : α},
  m.WF → m.getKey? k = some k' → (Std.HashMap.Raw.map f m)[k]! = (Option.map (f k') m[k]?).get!
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Char
String.endsWith_char_eq_getLast? : ∀ {c : Char} {s : String}, s.endsWith c = (s.toList.getLast? == some c)
-- Mathlib.Data.Matrix.Basic
/-- `Matrix.transpose` as a `LinearMap`  -/
Matrix.transposeLinearEquiv : (m : Type u_2) →
  (n : Type u_3) →
    (R : Type u_7) →
      (α : Type u_11) →
        [inst : Semiring R] → [inst_1 : AddCommMonoid α] → [inst_2 : Module R α] → Matrix m n α ≃ₗ[R] Matrix n m α
-- Mathlib.Analysis.Normed.Lp.PiLp
/-- This definition allows to endow `Π i, α i` with a normed space structure corresponding to
the Lp norm. It is useful for type synonyms of `Π i, α i`.  -/
PiLp.normedSpaceSeminormedAddCommGroupToPi : (p : ENNReal) →
  {ι : Type u_2} →
    (α : ι → Type u_3) →
      [inst : Fact (1 ≤ p)] →
        [inst_1 : Fintype ι] →
          [inst_2 : (i : ι) → SeminormedAddCommGroup (α i)] →
            {R : Type u_5} → [inst_3 : NormedField R] → [(i : ι) → NormedSpace R (α i)] → NormedSpace R ((i : ι) → α i)
-- Lean.MetavarContext
Lean.LevelMetavarDecl.mk.inj : ∀ {depth index depth_1 index_1 : ℕ},
  { depth := depth, index := index } = { depth := depth_1, index := index_1 } → depth = depth_1 ∧ index = index_1
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
add_abs_nonneg : ∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : LinearOrder α] [AddLeftMono α] (a : α), 0 ≤ a + |a|
-- Mathlib.Probability.Decision.BayesEstimator
/-- If the estimation problem admits an argmin estimator, then the Bayesian risk
attains the risk lower bound `∫⁻ x, ⨅ y, ∫⁻ θ, ℓ θ y ∂((P†π) x) ∂(P ∘ₘ π)`.  -/
ProbabilityTheory.HasArgminEstimator.bayesRisk_eq : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} {P : ProbabilityTheory.Kernel Θ 𝓧} {π : MeasureTheory.Measure Θ}
  [inst : StandardBorelSpace Θ] [inst_1 : Nonempty Θ] [inst_2 : ProbabilityTheory.IsFiniteKernel P]
  [inst_3 : MeasureTheory.IsFiniteMeasure π],
  Measurable (Function.uncurry ℓ) →
    ProbabilityTheory.HasArgminEstimator ℓ P π →
      ProbabilityTheory.bayesRisk ℓ P π =
        ∫⁻ (x : 𝓧), ⨅ y, ∫⁻ (θ : Θ), ℓ θ y ∂(ProbabilityTheory.posterior P π) x ∂π.bind ⇑P
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.C_ne_zero : ∀ {R : Type u} {σ : Type u_1} {a : R} [inst : CommSemiring R], MvPolynomial.C a ≠ 0 ↔ a ≠ 0
-- Init.Data.Ord.Basic
Ordering.swap_then : ∀ (o₁ o₂ : Ordering), (o₁.then o₂).swap = o₁.swap.then o₂.swap
-- Mathlib.Algebra.Group.End
Equiv.addLeft_add : ∀ {α : Type u_4} [inst : AddGroup α] (a b : α), Equiv.addLeft (a + b) = Equiv.addLeft a * Equiv.addLeft b
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBiproductData.mk.sizeOf_spec : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} [inst_2 : SizeOf C] (bicone : CategoryTheory.Limits.BinaryBicone P Q) (isBilimit : bicone.IsBilimit),
  sizeOf { bicone := bicone, isBilimit := isBilimit } = 1 + sizeOf bicone + sizeOf isBilimit
-- Mathlib.RingTheory.LocalProperties.InjectiveDimension
ModuleCat.hasInjectiveDimensionLE_iff_forall_maximalSpectrum : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Small.{v, u} R] [IsNoetherianRing R] (n : ℕ) (M : ModuleCat R),
  CategoryTheory.HasInjectiveDimensionLE M n ↔
    ∀ (m : MaximalSpectrum R), CategoryTheory.HasInjectiveDimensionLE (M.localizedModule m.asIdeal.primeCompl) n
-- Aesop.Forward.LevelIndex
Aesop.LevelIndex.toNat : Aesop.LevelIndex → ℕ
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork_π : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} (hS : S.Exact) [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  (kf : CategoryTheory.Limits.KernelFork S.g) (hkf : CategoryTheory.Limits.IsLimit kf),
  (hS.leftHomologyDataOfIsLimitKernelFork kf hkf).π = 0
-- Mathlib.FieldTheory.Extension
IntermediateField.Lifts.nonempty_algHom_of_exist_lifts_finset : ∀ {F : Type u_1} {E : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
  [inst_3 : Algebra F E] [inst_4 : Algebra F K] [alg : Algebra.IsAlgebraic F E],
  (∀ (S : Finset E), ∃ σ, ↑S ⊆ ↑σ.carrier) → Nonempty (E →ₐ[F] K)
-- Batteries.Tactic.GeneralizeProofs
/-- The prop/proof triples to add to the local context.
The proofs must not refer to fvars in `fvars`.  -/
Batteries.Tactic.GeneralizeProofs.AState.generalizations : Batteries.Tactic.GeneralizeProofs.AState → Array (Lean.Expr × Lean.Expr)
-- Mathlib.Computability.NFA
/-- Regular languages are closed under reversal.  -/
Language.isRegular_reverse_iff : ∀ {α : Type u} {L : Language α}, L.reverse.IsRegular ↔ L.IsRegular
-- Std.Http.Protocol.H1.Reader
Std.Http.Protocol.H1.Reader.State.needHeader.inj : ∀ {dir : Std.Http.Protocol.H1.Direction} {a a_1 : ℕ},
  Std.Http.Protocol.H1.Reader.State.needHeader a = Std.Http.Protocol.H1.Reader.State.needHeader a_1 → a = a_1
-- Mathlib.CategoryTheory.Galois.IsFundamentalgroup
CategoryTheory.PreGaloisCategory.IsNaturalSMul.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {F : CategoryTheory.Functor C FintypeCat} {G : Type u_1}
  [inst_1 : Group G] [inst_2 : (X : C) → MulAction G (F.obj X).obj],
  (∀ (g : G) {X Y : C} (f : X ⟶ Y) (x : (F.obj X).obj),
      (CategoryTheory.ConcreteCategory.hom (F.map f)) (g • x) = g • (CategoryTheory.ConcreteCategory.hom (F.map f)) x) →
    CategoryTheory.PreGaloisCategory.IsNaturalSMul F G
-- Mathlib.Analysis.Convex.Function
ConcaveOn.right_le_of_le_left'' : ∀ {𝕜 : Type u_1} {β : Type u_5} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommMonoid β] [inst_4 : LinearOrder β] [IsOrderedCancelAddMonoid β] [inst_6 : Module 𝕜 β]
  [PosSMulStrictMono 𝕜 β] {x y z : 𝕜} {s : Set 𝕜} {f : 𝕜 → β},
  ConcaveOn 𝕜 s f → x ∈ s → z ∈ s → x < y → y ≤ z → f y ≤ f x → f z ≤ f y
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback₃.p₂₃_eq_lift : ∀ {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₃} (h : CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃),
  h.p₂₃ = ⋯.lift h.p₂ h.p₃ ⋯
-- Lean.Meta.DiscrTree.Types
Lean.Meta.DiscrTree.Trie.node.injEq : ∀ {α : Type} (vs : Array α) (children : Array (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α)) (vs_1 : Array α)
  (children_1 : Array (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α)),
  (Lean.Meta.DiscrTree.Trie.node vs children = Lean.Meta.DiscrTree.Trie.node vs_1 children_1) =
    (vs = vs_1 ∧ children = children_1)
-- Init.Data.Order.Opposite
Std.OppositeOrderInstances.instLawfulOrderLeftLeaningMaxOpposite : ∀ {α : Type u_1} {il : LE α} {im : Max α} [Std.LawfulOrderLeftLeaningMax α], Std.LawfulOrderLeftLeaningMin α
-- Mathlib.Geometry.Manifold.ChartedSpace
modelPiInhabited : {ι : Type u_5} → {Hi : ι → Type u_6} → [(i : ι) → Inhabited (Hi i)] → Inhabited (ModelPi Hi)
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeRule.mk.inj : ∀ {T : Type u_1} {N : Type u_2} {input : N} {output : List (Symbol T N)} {input_1 : N} {output_1 : List (Symbol T N)},
  { input := input, output := output } = { input := input_1, output := output_1 } → input = input_1 ∧ output = output_1
-- Mathlib.Topology.Algebra.Group.CompactOpen
ContinuousMonoidHom.locallyCompactSpace_of_hasBasis : ∀ {X : Type u_7} {Y : Type u_8} [inst : TopologicalSpace X] [inst_1 : Group X] [IsTopologicalGroup X]
  [inst_3 : UniformSpace Y] [inst_4 : CommGroup Y] [IsUniformGroup Y] [T0Space Y] [CompactSpace Y]
  [LocallyCompactSpace X] (V : ℕ → Set Y),
  (∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)) →
    (nhds 1).HasBasis (fun x => True) V → LocallyCompactSpace (X →ₜ* Y)
-- Mathlib.CategoryTheory.Sites.Equivalence
CategoryTheory.Equivalence.eq_inducedTopology_of_isDenseSubsite : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D)
  [CategoryTheory.Functor.IsDenseSubsite K J e.inverse], K = e.inverse.inducedTopology J
-- Mathlib.Analysis.InnerProductSpace.Orientation
/-- `OrthonormalBasis.adjustToOrientation`, applied to an orthonormal basis, preserves the
property of orthonormality.  -/
OrthonormalBasis.orthonormal_adjustToOrientation : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {ι : Type u_2} [inst_2 : Fintype ι]
  [inst_3 : DecidableEq ι] (e : OrthonormalBasis ι ℝ E) (x : Orientation ℝ E ι) [inst_4 : Nonempty ι],
  Orthonormal ℝ ⇑(e.toBasis.adjustToOrientation x)
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.Decidable.isLongestMatchAt_iff_isLongestMatchAt_decide : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice} {pos pos' : s.Pos},
  String.Slice.Pattern.Model.IsLongestMatchAt p pos pos' ↔
    String.Slice.Pattern.Model.IsLongestMatchAt (fun x => decide (p x)) pos pos'
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv
/-- A function that is inverse to `f` near `a`.  -/
HasStrictDerivAt.localInverse : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    [CompleteSpace 𝕜] → (f : 𝕜 → 𝕜) → (f' a : 𝕜) → HasStrictDerivAt f f' a → f' ≠ 0 → 𝕜 → 𝕜
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.symm : ∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] {f : ℝ → ε} {a b : ℝ}
  {μ : MeasureTheory.Measure ℝ}, IntervalIntegrable f μ a b → IntervalIntegrable f μ b a
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.insertManyIfNewUnit_ind : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {ρ : Type w} [inst_2 : ForIn Id ρ α]
  {motive : (Std.DHashMap.Raw α fun x => Unit) → Prop} (m : Std.DHashMap.Raw α fun x => Unit) (l : ρ),
  motive m →
    (∀ (m : Std.DHashMap.Raw α fun x => Unit) (a : α), motive m → motive (m.insertIfNew a ())) →
      motive (Std.DHashMap.Raw.Const.insertManyIfNewUnit m l)
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.FirstByte.noConfusionType : Sort v✝ → ByteArray.utf8DecodeChar?.FirstByte → ByteArray.utf8DecodeChar?.FirstByte → Sort v✝
-- Mathlib.Data.Multiset.Fintype
/-- Constructor for terms of the coercion of `m` to a type.
This helps Lean pick up the correct instances.  -/
Multiset.mkToType : {α : Type u_1} → [inst : DecidableEq α] → (m : Multiset α) → (x : α) → Fin (Multiset.count x m) → m.ToType
-- Mathlib.Probability.Kernel.IonescuTulcea.Maps
IocProdIoc_preimage : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : LocallyFiniteOrder ι] [inst_2 : DecidableLE ι] {X : ι → Type u_2}
  {a b c : ι} (hab : a ≤ b) (hbc : b ≤ c) (s : (i : ↥(Finset.Ioc a c)) → Set (X ↑i)),
  IocProdIoc a b c ⁻¹' Set.univ.pi s = Set.univ.pi (Finset.restrict₂ ⋯ s) ×ˢ Set.univ.pi (Finset.restrict₂ ⋯ s)
-- Mathlib.Topology.AlexandrovDiscrete
Sigma.instAlexandrovDiscrete : ∀ {ι : Type u_5} {X : ι → Type u_6} [inst : (i : ι) → TopologicalSpace (X i)] [∀ (i : ι), AlexandrovDiscrete (X i)],
  AlexandrovDiscrete ((i : ι) × X i)
-- Init.Grind.Ordered.Ring
Lean.Grind.OrderedRing.natCast_le_natCast_of_le : ∀ {R : Type u} [inst : Lean.Grind.Ring R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsPreorder R] [Lean.Grind.OrderedRing R] (a b : ℕ), a ≤ b → ↑a ≤ ↑b
-- Mathlib.Logic.Function.Basic
Function.injective_iff_hasLeftInverse : ∀ {α : Sort u_1} {β : Sort u_2} [Nonempty α] {f : α → β}, Function.Injective f ↔ Function.HasLeftInverse f
-- Mathlib.Algebra.Star.LinearMap
TensorProduct.star_map_apply_eq_map_intrinsicStar : ∀ {R : Type u_5} {E : Type u_6} {F : Type u_7} {G : Type u_8} {H : Type u_9} [inst : CommSemiring R]
  [inst_1 : StarRing R] [inst_2 : AddCommMonoid E] [inst_3 : StarAddMonoid E] [inst_4 : Module R E]
  [inst_5 : StarModule R E] [inst_6 : AddCommMonoid F] [inst_7 : StarAddMonoid F] [inst_8 : Module R F]
  [inst_9 : StarModule R F] [inst_10 : AddCommMonoid G] [inst_11 : StarAddMonoid G] [inst_12 : Module R G]
  [inst_13 : StarModule R G] [inst_14 : AddCommMonoid H] [inst_15 : StarAddMonoid H] [inst_16 : Module R H]
  [inst_17 : StarModule R H] (f : WithConv (E →ₗ[R] F)) (g : WithConv (G →ₗ[R] H)) (x : TensorProduct R E G),
  star ((TensorProduct.map f.ofConv g.ofConv) x) = (TensorProduct.map (star f).ofConv (star g).ofConv) (star x)
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.le_measureReal_sdiff : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ : Set α},
  autoParam (μ s₂ ≠ ⊤) MeasureTheory.le_measureReal_sdiff._auto_1 → μ.real s₁ - μ.real s₂ ≤ μ.real (s₁ \ s₂)
-- Mathlib.Analysis.BoxIntegral.Partition.Additive
/-- A function on `Box ι` is called box additive if for every box `J` and a partition `π` of `J`
we have `f J = ∑ Ji ∈ π.boxes, f Ji`. A function is called box additive on subboxes of `I : Box ι`
if the same property holds for `J ≤ I`. We formalize these two notions in the same definition
using `I : WithBot (Box ι)`: the value `I = ⊤` corresponds to functions box additive on the whole
space.  -/
BoxIntegral.«term_→ᵇᵃ[_]_» : Lean.TrailingParserDescr
-- Mathlib.Data.Num.Prime
PosNum.minFac.eq_1 : PosNum.one.minFac = 1
-- Mathlib.Tactic.FunProp.Decl
Mathlib.Meta.FunProp.FunPropDecl.mk.sizeOf_spec : ∀ (funPropName : Lean.Name) (path : Array Lean.Meta.DiscrTree.Key) (funArgId : ℕ),
  sizeOf { funPropName := funPropName, path := path, funArgId := funArgId } =
    1 + sizeOf funPropName + sizeOf path + sizeOf funArgId
-- Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence
AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_homotopyInvHomId : ∀ {A : Type u_2} [inst : CategoryTheory.Category.{v_2, u_2} A] [inst_1 : CategoryTheory.Abelian A]
  {Y : CategoryTheory.SimplicialObject A},
  AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex.homotopyInvHomId =
    (Homotopy.ofEq ⋯).trans (AlgebraicTopology.DoldKan.homotopyPInftyToId Y)
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.singleOneRingHom.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : MulOneClass M],
  MonoidAlgebra.singleOneRingHom =
    { toFun := (↑(MonoidAlgebra.singleAddHom 1)).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Analysis.Convex.FunctionTopology
/-- The set of concave functions on a set `s` is closed.  -/
isClosed_setOfPred_concaveOn : ∀ {𝕜 : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : PartialOrder β]
  [inst_3 : TopologicalSpace β] [OrderClosedTopology β] [inst_5 : AddCommMonoid α] [inst_6 : AddCommMonoid β]
  [inst_7 : SMul 𝕜 α] [inst_8 : SMul 𝕜 β] [ContinuousConstSMul 𝕜 β] [ContinuousAdd β] {s : Set α},
  IsClosed {f | ConcaveOn 𝕜 s f}
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.instHasColimitCompOfPreservesColimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C}
  [CategoryTheory.Limits.HasColimit K] {F : CategoryTheory.Functor C D} [CategoryTheory.Limits.PreservesColimit K F],
  CategoryTheory.Limits.HasColimit (K.comp F)
-- Batteries.Data.List.Basic
List.swap.eq_3 : ∀ {α : Type u_1} (a : α) (xs : List α) (i : ℕ), (a :: xs).swap 0 i.succ = xs[i]?.getD a :: xs.set i a
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddMemClass.add.eq_1 : ∀ {M : Type u_1} {A : Type u_3} [inst : Add M] [inst_1 : SetLike A M] [hA : AddMemClass A M] (S' : A),
  AddMemClass.add S' = { add := fun a b => ⟨↑a + ↑b, ⋯⟩ }
-- Mathlib.Order.Interval.Set.Basic
Set.Ioi_inter_Iic : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ioi a ∩ Set.Iic b = Set.Ioc a b
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.mapShortComplexH2_zero : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H), groupHomology.mapShortComplexH2 f 0 = 0
-- Lean.Elab.Tactic.BuiltinTactic
Lean.Elab.Tactic.evalRunTac : Lean.Elab.Tactic.Tactic
-- Init.Data.Vector.Lemmas
Vector.flatMap_def : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {m : ℕ} {xs : Vector α n} {f : α → Vector β m},
  xs.flatMap f = (Vector.map f xs).flatten
-- Mathlib.Data.Fin.SuccPred
Fin.sub_castPred_eq_castPred_sub_of_le : ∀ {n : ℕ} {a b : Fin (n + 1)} (ha : a ≠ Fin.last n) (h : b ≤ a), a.castPred ha - b.castPred ⋯ = (a - b).castPred ⋯
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.NullMeasurableSet.measurable_of_complete : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasureTheory.NullMeasurableSet s μ → ∀ [μ.IsComplete], MeasurableSet s
-- Mathlib.CategoryTheory.Subobject.Limits
/-- The image of `h ≫ f` is always a smaller subobject than the image of `f`.  -/
CategoryTheory.Limits.imageSubobject_comp_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y X' : C} (h : X' ⟶ X) (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasImage f]
  [inst_2 : CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp h f)],
  CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp h f) ≤ CategoryTheory.Limits.imageSubobject f
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.darts_append : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (p' : G.Walk v w),
  (p.append p').darts = p.darts ++ p'.darts