mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.JacobianOneDim
MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_deriv_mul : ∀ (f : ℝ ≃ᵐ ℝ) {s : Set ℝ},
  MeasurableSet s →
    ∀ {g : ℝ → ℝ},
      (∀ᵐ (x : ℝ), x ∈ ⇑f '' s → 0 ≤ g x) →
        MeasureTheory.IntegrableOn g (⇑f '' s) MeasureTheory.volume →
          ∀ {f' : ℝ → ℝ},
            (∀ x ∈ s, HasDerivWithinAt (⇑f) (f' x) s x) →
              (MeasureTheory.Measure.map (⇑f.symm) (MeasureTheory.volume.withDensity fun x => ENNReal.ofReal (g x))) s =
                ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * g (f x))
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
_private.Mathlib.Analysis.SpecialFunctions.Gamma.Basic.0.Complex.GammaAux.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.coe_nsmul : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} {G : Type u_6} [inst : SMul M G] (f : α → G) (n : M), ↑(n • f) = n • ↑f
-- Mathlib.MeasureTheory.Function.AEEqFun
/-- Given a predicate `p` and an equivalence class `[f]`, return true if `p` holds of `f a`
for almost all `a`  -/
MeasureTheory.AEEqFun.LiftPred : {α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] →
      {μ : MeasureTheory.Measure α} → [inst_1 : TopologicalSpace β] → (β → Prop) → (α →ₘ[μ] β) → Prop
-- Lean.DocString.Parser
/-- Parses an ordered list.  -/
Lean.Doc.Parser.orderedList : Lean.Doc.Parser.BlockCtxt → Lean.Parser.ParserFn
-- Mathlib.Data.Multiset.Bind
/-- `Multiset.sigma s t` is the dependent version of `Multiset.product`. It is the sum of
`(a, b)` as `a` ranges over `s` and `b` ranges over `t a`.  -/
Multiset.sigma : {α : Type u_1} → {σ : α → Type u_4} → Multiset α → ((a : α) → Multiset (σ a)) → Multiset ((a : α) × σ a)
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.map_mkQ_eq_top : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p p' : Submodule R M),
  Submodule.map p.mkQ p' = ⊤ ↔ p ⊔ p' = ⊤
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.card_inv_le : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Inv α] {s : Finset α}, s⁻¹.card ≤ s.card
-- Mathlib.Geometry.Manifold.ChartedSpace
/-- The disjoint union of two charted spaces modelled on a non-empty space `H`
is a charted space over `H`.  -/
ChartedSpace.sumOfNonempty : {H : Type u} →
  {M : Type u_2} →
    {M' : Type u_3} →
      [inst : TopologicalSpace H] →
        [inst_1 : TopologicalSpace M] →
          [inst_2 : TopologicalSpace M'] →
            [cm : ChartedSpace H M] → [cm' : ChartedSpace H M'] → [Nonempty H] → ChartedSpace H (M ⊕ M')
-- Lean.Meta.Tactic.Grind.Intro
/-- Similar to `Grind.preprocess`, but does not simplify `e` if
`isMatchCondCandidate` (aka `Simp.isEqnThmHypothesis`) is `true`.
We added this feature because it may be coming from external sources
(e.g., manually applying an function induction principle before invoking `grind`).
 -/
Lean.Meta.Grind.preprocessHypothesis : Lean.Expr → Lean.Meta.Grind.GoalM Lean.Meta.Simp.Result
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.inv_def : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommGroup Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedAddMonoid Γ]
  [inst_3 : Field R] (x : HahnSeries Γ R),
  x⁻¹ =
    (HahnSeries.single (-x.order)) x.leadingCoeff⁻¹ *
      (HahnSeries.SummableFamily.powers (1 - (HahnSeries.single (-x.order)) x.leadingCoeff⁻¹ * x)).hsum
-- Lean.Meta.Tactic.SolveByElim
/-- Also use symmetric versions (via `@[symm]`) of local hypotheses.  -/
Lean.Meta.SolveByElim.ApplyRulesConfig.symm : Lean.Meta.SolveByElim.ApplyRulesConfig → Bool
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.support_map_subset : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (f : R →+* S₁)
  (p : MvPolynomial σ R), ((MvPolynomial.map f) p).support ⊆ p.support
-- Mathlib.Data.List.Sort
List.insertionSort_nil : ∀ {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r], List.insertionSort r [] = []
-- Init.Grind.AC
Lean.Grind.AC.Seq.sort'_k.eq_1 : ∀ (s : Lean.Grind.AC.Seq),
  s.sort'_k =
    Lean.Grind.AC.Seq.rec (motive := fun x => Lean.Grind.AC.Seq → Lean.Grind.AC.Seq)
      (fun x acc => Lean.Grind.AC.Seq.insert x acc) (fun x x_1 ih acc => ih (Lean.Grind.AC.Seq.insert x acc)) s
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.boundedOrder : {α : Type u_1} → [Fintype α] → BoundedOrder (Finset α)
-- Mathlib.GroupTheory.Index
Subgroup.index_map : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] (H : Subgroup G) (f : G →* G'),
  (Subgroup.map f H).index = (H ⊔ f.ker).index * f.range.index
-- Mathlib.Data.Bool.Set
Bool.univ_eq : Set.univ = {false, true}
-- Mathlib.AlgebraicTopology.SimplicialSet.Dimension
SSet.instHasDimensionLTToSSetRange : ∀ {X Y : SSet} (f : X ⟶ Y) (d : ℕ) [X.HasDimensionLT d], (SSet.Subcomplex.range f).toSSet.HasDimensionLT d
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
/-- Construct a strong transformation of pseudofunctors from a strong transformation of the
underlying oplax functors.  -/
CategoryTheory.Pseudofunctor.StrongTrans.mkOfOplax : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.Pseudofunctor B C} →
          CategoryTheory.Oplax.StrongTrans F.toOplax G.toOplax → F.StrongTrans G
-- Lean.Elab.BuiltinCommand
Lean.Elab.Command.elabDocsToVerso : Lean.Elab.Command.CommandElab
-- Mathlib.Analysis.Complex.UpperHalfPlane.Measure
/-- The measure on the upper half-plane is invariant under `GL(2, ℝ)`.  -/
UpperHalfPlane.instSMulInvariantMeasureGeneralLinearGroupFinOfNatNatRealVolume : MeasureTheory.SMulInvariantMeasure (GL (Fin 2) ℝ) UpperHalfPlane MeasureTheory.volume
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Trivialization.symmL_apply : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : NontriviallyNormedField R]
  [inst_1 : (x : B) → AddCommMonoid (E x)] [inst_2 : (x : B) → Module R (E x)] [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace R F] [inst_5 : TopologicalSpace B] [inst_6 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_7 : (x : B) → TopologicalSpace (E x)] [inst_8 : FiberBundle F E]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_9 : Bundle.Trivialization.IsLinear R e] {b : B},
  b ∈ e.baseSet → ∀ (y : F), (Bundle.Trivialization.symmL R e b) y = e.symm b y
-- Mathlib.Analysis.Analytic.Basic
/-- Taylor formula for an analytic function, `IsBigO` version.  -/
HasFPowerSeriesAt.isBigO_sub_partialSum_pow : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E},
  HasFPowerSeriesAt f p x → ∀ (n : ℕ), (fun y => f (x + y) - p.partialSum n y) =O[nhds 0] fun y => ‖y‖ ^ n
-- Mathlib.Probability.Process.Stopping
MeasureTheory.integrable_stoppedProcess_of_mem_finset : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Nonempty ι] {μ : MeasureTheory.Measure Ω}
  {τ : Ω → WithTop ι} {E : Type u_4} {u : ι → Ω → E} [inst_1 : LinearOrder ι] [inst_2 : TopologicalSpace ι]
  [OrderTopology ι] [FirstCountableTopology ι] {ℱ : MeasureTheory.Filtration ι m} [inst_5 : NormedAddCommGroup E],
  MeasureTheory.IsStoppingTime ℱ τ →
    (∀ (n : ι), MeasureTheory.Integrable (u n) μ) →
      ∀ (n : ι) {s : Finset ι},
        (∀ (ω : Ω), τ ω < ↑n → τ ω ∈ WithTop.some '' ↑s) →
          MeasureTheory.Integrable (MeasureTheory.stoppedProcess u τ n) μ
-- Mathlib.Topology.NoetherianSpace
/-- [Stacks Tag 0052](https://stacks.math.columbia.edu/tag/0052) ((1)) -/
TopologicalSpace.NoetherianSpace.set : ∀ {α : Type u_1} [inst : TopologicalSpace α] [TopologicalSpace.NoetherianSpace α] (s : Set α),
  TopologicalSpace.NoetherianSpace ↑s
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigOWith.congr_right : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {c : ℝ} {f : α → E} {l : Filter α}
  {g₁ g₂ : α → F}, Asymptotics.IsBigOWith c l f g₁ → (∀ (x : α), g₁ x = g₂ x) → Asymptotics.IsBigOWith c l f g₂
-- Mathlib.Analysis.Real.Hyperreal
/-- **Alias** of `Hyperreal.epsilon_lt_of_pos`. -/
Hyperreal.epsilon_lt_pos : ∀ {r : ℝ}, 0 < r → Hyperreal.epsilon < ↑r
-- Mathlib.Order.Category.Frm
FrameHom.mk.congr_simp : ∀ {α : Type u_8} {β : Type u_9} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  (toInfTopHom toInfTopHom_1 : InfTopHom α β) (e_toInfTopHom : toInfTopHom = toInfTopHom_1)
  (map_sSup' : ∀ (s : Set α), toInfTopHom.toFun (sSup s) = sSup (toInfTopHom.toFun '' s)),
  { toInfTopHom := toInfTopHom, map_sSup' := map_sSup' } = { toInfTopHom := toInfTopHom_1, map_sSup' := ⋯ }
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
CategoryTheory.Free.lift_obj : ∀ (R : Type u_1) [inst : CommRing R] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] {D : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} D] [inst_3 : CategoryTheory.Preadditive D]
  [inst_4 : CategoryTheory.Linear R D] (F : CategoryTheory.Functor C D) (X : CategoryTheory.Free R C),
  (CategoryTheory.Free.lift R F).obj X = F.obj X
-- Init.Data.List.MinMax
_private.Init.Data.List.MinMax.0.List.getLast?.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (as : List α) → motive (a :: as)),
  (match [] with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_1 ()
-- Mathlib.Algebra.Group.Hom.Defs
AddHom.comp_id : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (f : M →ₙ+ N), f.comp (AddHom.id M) = f
-- Mathlib.GroupTheory.Commensurable
/-- Two subgroups `H K` of `G` are commensurable if `H ⊓ K` has finite index in both
`H` and `K`.  -/
AddSubgroup.Commensurable : {G : Type u_1} → [inst : AddGroup G] → AddSubgroup G → AddSubgroup G → Prop
-- Mathlib.Algebra.Squarefree.Basic
squarefree_iff_emultiplicity_le_one : ∀ {R : Type u_1} [inst : CommMonoid R] (r : R), Squarefree r ↔ ∀ (x : R), emultiplicity x r ≤ 1 ∨ IsUnit x
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPolynomial.coe_pow : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {φ : MvPolynomial σ R} (n : ℕ), ↑(φ ^ n) = ↑φ ^ n
-- Mathlib.RingTheory.GradedAlgebra.RingHom
/-- A graded ring homomorphism descends to a ring homomorphism on the zeroth component.  -/
GradedRingHom.gradedZeroRingHom : {ι : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      {σ : Type u_6} →
        {τ : Type u_7} →
          [inst : Semiring A] →
            [inst_1 : Semiring B] →
              [inst_2 : SetLike σ A] →
                [inst_3 : SetLike τ B] →
                  {𝒜 : ι → σ} →
                    {ℬ : ι → τ} →
                      [inst_4 : AddSubmonoidClass σ A] →
                        [inst_5 : AddSubmonoidClass τ B] →
                          [inst_6 : AddMonoid ι] →
                            [inst_7 : SetLike.GradedMonoid 𝒜] →
                              [inst_8 : SetLike.GradedMonoid ℬ] → (𝒜 →+*ᵍ ℬ) → ↥(𝒜 0) →+* ↥(ℬ 0)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorExtractAndExtendBitTargetBlastExtractAndExtendBit : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulVecOperator α Std.Tactic.BVDecide.BVExpr.bitblast.ExtractAndExtendBitTarget fun {len} =>
    Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtendBit
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
mul_mem_nonZeroDivisors_of_mem_nonZeroDivisors : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] {x y : M₀},
  x ∈ nonZeroDivisors M₀ → y ∈ nonZeroDivisors M₀ → x * y ∈ nonZeroDivisors M₀
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey?_modify : ∀ {α : Type u} {instOrd : Ord α} [Std.TransOrd α] {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β},
  t.WF →
    ∀ {k k' : α} {f : β → β},
      (Std.DTreeMap.Internal.Impl.Const.modify k f t).getKey? k' =
        if compare k k' = Ordering.eq then if k ∈ t then some k else none else t.getKey? k'
-- Mathlib.Order.GaloisConnection.Defs
GaloisConnection.l_bot : ∀ {α : Type u} {β : Type v} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : OrderBot α] [inst_3 : OrderBot β]
  {u : α → β} {l : β → α}, GaloisConnection l u → l ⊥ = ⊥
-- Lean.Meta.DiscrTree.Main
_private.Lean.Meta.DiscrTree.Main.0.Lean.Meta.DiscrTree.reduceUntilBadKey.step : Lean.Expr → Lean.MetaM Lean.Expr
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKey?_filterMap : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : α → β → Option γ} {k : α} (h : m.WF),
  (Std.DHashMap.Raw.filterMap f m).getKey? k =
    (m.getKey? k).pfilter fun x h' => (f x (Std.DHashMap.Raw.Const.get m x ⋯)).isSome
-- Mathlib.Topology.Compactness.Compact
IsCompact.prod_nhdsSet_eq_biSup : ∀ {Y : Type v} [inst : TopologicalSpace Y] {K : Set Y},
  IsCompact K → ∀ {X : Type u_2} (l : Filter X), l ×ˢ nhdsSet K = ⨆ y ∈ K, l ×ˢ nhds y
-- Mathlib.Topology.Order.Lattice
Filter.Tendsto.finset_sup'_nhds : ∀ {L : Type u_1} [inst : TopologicalSpace L] {ι : Type u_3} {α : Type u_4} {s : Finset ι} {f : ι → α → L} {l : Filter α}
  {g : ι → L} [inst_1 : SemilatticeSup L] [ContinuousSup L] (hne : s.Nonempty),
  (∀ i ∈ s, Filter.Tendsto (f i) l (nhds (g i))) → Filter.Tendsto (s.sup' hne f) l (nhds (s.sup' hne g))
-- Mathlib.Algebra.Lie.CartanCriterion
/-- A convenience variation of `LieAlgebra.isSolvable_of_forall_derived_killingForm_eq_zero` for
working with ideals.

Over a principal ideal domain by `LieIdeal.killingForm_eq` this is just a specialisation of
`LieAlgebra.isSolvable_of_killingForm_apply_lie_eq_zero` but since it does not require the PID
assumption, it is a slightly stronger result.  -/
LieIdeal.isSolvable_of_killingForm_apply_lie_eq_zero : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [CharZero R] [IsDomain R] [inst_3 : LieRing L]
  [inst_4 : LieAlgebra R L] [IsNoetherian R L] [Module.Free R L] (I : LieIdeal R L),
  (∀ x ∈ I, ∀ y ∈ ⁅I, I⁆, ((killingForm R L) x) y = 0) → LieAlgebra.IsSolvable ↥I
-- Mathlib.NumberTheory.NumberField.ExistsRamified
/-- If `K` is a number field with positive rank such that `K/ℚ` is galois, then there exists
some rational prime `p : ℕ` such that every prime of `K` over `p` is ramified.  -/
NumberField.exists_not_isUnramifiedAt_int_of_isGalois : ∀ {K : Type u_1} {𝒪 : Type u_2} [inst : Field K] [inst_1 : NumberField K] [inst_2 : CommRing 𝒪] [inst_3 : Algebra 𝒪 K]
  [IsIntegralClosure 𝒪 ℤ K] [IsGalois ℚ K],
  1 < Module.finrank ℚ K → ∃ p, Nat.Prime p ∧ ∀ (P : Ideal 𝒪) (x : P.IsPrime), ↑p ∈ P → ¬Algebra.IsUnramifiedAt ℤ P
-- Mathlib.RingTheory.Localization.Defs
IsLocalization'.toIsLocalizationMap : ∀ {R : Type u_1} {inst : CommSemiring R} {M : Submonoid R} {S : Type u_2} {inst_1 : CommSemiring S}
  {inst_2 : Algebra R S} [self : IsLocalization' M S], M.IsLocalizationMap ⇑(algebraMap R S)
-- Mathlib.CategoryTheory.Subterminal
/-- If `A` is subterminal, its diagonal morphism is an isomorphism.
The converse of `isSubterminal_of_isIso_diag`.
 -/
CategoryTheory.IsSubterminal.isIso_diag : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : C},
  CategoryTheory.IsSubterminal A →
    ∀ [inst_1 : CategoryTheory.Limits.HasBinaryProduct A A], CategoryTheory.IsIso (CategoryTheory.Limits.diag A)
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.homEquiv_symm_unit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (X : C),
  (adj.homEquiv X (F.obj X)).symm (adj.unit.app X) = CategoryTheory.CategoryStruct.id (F.obj X)
-- Std.Async.TCP
Std.Async.TCP.Socket.Client.native : Std.Async.TCP.Socket.Client → Std.Internal.UV.TCP.Socket
-- Mathlib.Data.Set.Image
Set.Nonempty.of_image : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α}, (f '' s).Nonempty → s.Nonempty
-- Mathlib.Algebra.BigOperators.Fin
finFunctionFinEquiv_symm_apply_val : ∀ {m n : ℕ} (a : Fin (m ^ n)) (b : Fin n), ↑(finFunctionFinEquiv.symm a b) = ↑a / m ^ ↑b % m
-- Mathlib.Analysis.Normed.Group.Constructions
Pi.normedGroup.eq_1 : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → NormedGroup (G i)],
  Pi.normedGroup =
    { toNorm := Pi.seminormedGroup.toNorm, toGroup := Pi.seminormedGroup.toGroup,
      toPseudoMetricSpace := Pi.seminormedGroup.toPseudoMetricSpace, eq_of_dist_eq_zero := ⋯, dist_eq := ⋯ }
-- Mathlib.Data.Rat.Cast.Order
Rat.cast_lt : ∀ {p q : ℚ} {K : Type u_5} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K], ↑p < ↑q ↔ p < q
-- Lean.Meta.Tactic.Grind.Types
/-- Returns maximum term generation that is considered during ematching.  -/
Lean.Meta.Grind.getMaxGeneration : Lean.Meta.Grind.GrindM ℕ
-- Init.Data.Slice.Operations
/-- This type class states that the slice's iterator emits exactly `Slice.size` elements before
terminating.
 -/
Std.Slice.LawfulSliceSize : {α β : Type u_1} →
  (γ : Type u) → [Std.Slice.SliceSize γ] → [Std.ToIterator (Std.Slice γ) Id α β] → [Std.Iterator α Id β] → Prop
-- Mathlib.Data.Finset.Functor
Finset.applicative : [(P : Prop) → Decidable P] → Applicative Finset
-- Mathlib.Analysis.Normed.Module.Ball.Action
instSMulElemClosedBallOfNatRealBall : {𝕜 : Type u_1} →
  {E : Type u_3} →
    [inst : NormedField 𝕜] →
      [inst_1 : SeminormedAddCommGroup E] →
        [NormedSpace 𝕜 E] → {r : ℝ} → SMul ↑(Metric.closedBall 0 1) ↑(Metric.ball 0 r)
-- Mathlib.Topology.MetricSpace.Gluing
/-- The type giving the inductive limit in a metric space context.  -/
Metric.InductiveLimit : {X : ℕ → Type u} →
  [inst : (n : ℕ) → MetricSpace (X n)] → {f : (n : ℕ) → X n → X (n + 1)} → (∀ (n : ℕ), Isometry (f n)) → Type u
-- Mathlib.RingTheory.Congruence.Basic
RingCon.ringConGen_iSup : ∀ {R : Type u_3} [inst : Add R] [inst_1 : Mul R] {ι : Sort u_5} (r : ι → R → R → Prop),
  ringConGen (iSup r) = ⨆ i, ringConGen (r i)
-- Mathlib.Combinatorics.Matroid.Dual
Matroid.dualIndepMatroid_E : ∀ {α : Type u_1} (M : Matroid α), M.dualIndepMatroid.E = M.E
-- Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
/-- This proves map_smul' of gnsNonUnitalStarAlgHom so that map_zero' can be proven as a direct
consequence.
 -/
_private.Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal.0.PositiveLinearMap.completion_leftMulMapPreGNS_map_smul : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] (f : A →ₚ[ℂ] ℂ) [inst_2 : StarOrderedRing A]
  (m : ℂ) (x : A), (f.leftMulMapPreGNS (m • x)).completion = m • (f.leftMulMapPreGNS x).completion
-- Mathlib.Probability.Kernel.Disintegration.CondCDF
ProbabilityTheory.setIntegral_condCDF : ∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) [MeasureTheory.IsFiniteMeasure ρ] (x : ℝ)
  {s : Set α}, MeasurableSet s → ∫ (a : α) in s, ↑(ProbabilityTheory.condCDF ρ a) x ∂ρ.fst = ρ.real (s ×ˢ Set.Iic x)
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.InnerRegularWRT.mono : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p q p' q' : Set α → Prop},
  μ.InnerRegularWRT p q → (∀ (s : Set α), q' s → q s) → (∀ (s : Set α), p s → p' s) → μ.InnerRegularWRT p' q'
-- Mathlib.CategoryTheory.Comma.Presheaf.Colimit
/-- Naturally in `X`, we have `Hom(YX, colim_i Fi) ≅ colim_i Hom(YX, Fi)`, where `Y` is the
"Yoneda embedding" `CostructuredArrow.toOver yoneda A`. This is a relative version of
`yonedaYonedaColimit`.  -/
CategoryTheory.CostructuredArrow.toOverCompYonedaColimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type v} →
      [inst_1 : CategoryTheory.SmallCategory J] →
        {A : CategoryTheory.Functor Cᵒᵖ (Type v)} →
          (F : CategoryTheory.Functor J (CategoryTheory.Over A)) →
            (CategoryTheory.CostructuredArrow.toOver CategoryTheory.yoneda A).op.comp
                (CategoryTheory.yoneda.obj (CategoryTheory.Limits.colimit F)) ≅
              (CategoryTheory.CostructuredArrow.toOver CategoryTheory.yoneda A).op.comp
                (CategoryTheory.Limits.colimit (F.comp CategoryTheory.yoneda))
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.germ_restrictStalkNatIso_hom_app : ∀ {X Y : AlgebraicGeometry.Scheme} {U : X.Opens} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] (x : ↥X)
  (M : Y.Modules) (hxU : x ∈ U),
  CategoryTheory.CategoryStruct.comp
      (((AlgebraicGeometry.Scheme.Modules.restrictFunctor f).obj M).presheaf.germ U x hxU)
      ((AlgebraicGeometry.Scheme.Modules.restrictStalkNatIso f x).hom.app M) =
    M.presheaf.germ ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj (Opposite.unop (Opposite.op U))) (f x) ⋯
-- Std.Time.Date.Unit.Month
Std.Time.Month.instLTQuarter : LT Std.Time.Month.Quarter
-- Mathlib.Order.Filter.Basic
Filter.inter_mem_inf : ∀ {α : Type u} {f g : Filter α} {s t : Set α}, s ∈ f → t ∈ g → s ∩ t ∈ f ⊓ g
-- Mathlib.Order.Filter.Germ.OrderedMonoid
Filter.Germ.instIsOrderedCancelMonoid : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} [inst : CommMonoid β] [inst_1 : Preorder β] [IsOrderedCancelMonoid β],
  IsOrderedCancelMonoid (l.Germ β)
-- Mathlib.Algebra.Order.Antidiag.Prod
/-- A pair belongs to `antidiagonal n` iff the sum of its components is equal to `n`.  -/
Finset.HasAntidiagonal.mem_antidiagonal : ∀ {A : Type u_1} {inst : AddMonoid A} [self : Finset.HasAntidiagonal A] {n : A} {a : A × A},
  a ∈ Finset.HasAntidiagonal.antidiagonal n ↔ a.1 + a.2 = n
-- Mathlib.Order.SuccPred.Limit
Order.IsPredPrelimit.isMax : ∀ {α : Type u_1} {a : α} [inst : PartialOrder α] [inst_1 : PredOrder α] [IsPredArchimedean α],
  Order.IsPredPrelimit a → IsMax a
-- Mathlib.Algebra.Algebra.Hom
/-- `AlgHom.toLinearMap` as a `MonoidHom`.  -/
AlgHom.toEnd : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → (A →ₐ[R] A) →* Module.End R A
-- Mathlib.Probability.Independence.Basic
/-- **Alias** of `ProbabilityTheory.iIndepFun.indepFun_finsetSum_of_notMem₀`. -/
ProbabilityTheory.iIndepFun.indepFun_finset_sum_of_notMem₀ : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10}
  {m : MeasurableSpace β} [inst : AddCommMonoid β] [MeasurableAdd₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iIndepFun f μ →
    (∀ (i : ι), AEMeasurable (f i) μ) →
      ∀ {s : Finset ι} {i : ι}, i ∉ s → ProbabilityTheory.IndepFun (∑ j ∈ s, f j) (f i) μ
-- Lean.Declaration
Lean.instInhabitedConstructor : Inhabited Lean.Constructor
-- Lean.Compiler.IR.Basic
Lean.IR.LocalContext.addLocal : Lean.IR.LocalContext → Lean.IR.VarId → Lean.IR.IRType → Lean.IR.Expr → Lean.IR.LocalContext
-- Mathlib.Data.Finsupp.Basic
Finsupp.comapDomain_sumElim_comapDomain : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Zero γ] (c : α ⊕ β →₀ γ),
  (Finsupp.comapDomain Sum.inl c ⋯).sumElim (Finsupp.comapDomain Sum.inr c ⋯) = c
-- Lean.Language.Basic
/-- Inherit range from outer task if any, or else the entire file.  -/
Lean.Language.SnapshotTask.ReportingRange.inherit : Lean.Language.SnapshotTask.ReportingRange
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquivClass.toAddEquiv.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : EquivLike F α β] [inst_1 : Add α] [inst_2 : Add β]
  [inst_3 : AddEquivClass F α β] (f : F), ↑f = { toEquiv := ↑f, map_add' := ⋯ }
-- Mathlib.Data.Set.Functor
Set.mem_of_mem_image_val : ∀ {α : Type u} {β : Set α} {γ : Set ↑β} {a : α} (ha : a ∈ Subtype.val '' γ), ⟨a, ⋯⟩ ∈ γ
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.not_iff : ∀ {M : Type u_1} [inst : CommMonoid M] {k : ℕ} {ζ : M}, ¬IsPrimitiveRoot ζ k ↔ orderOf ζ ≠ k
-- Init.Data.Nat.Lemmas
Nat.div_two_le_of_sub_le_div_two : ∀ {a b : ℕ}, a - b ≤ a / 2 → a / 2 ≤ b
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.eq_gcd_cert.eq_4 : ∀ (a b g g_1 g_2 : ℤ),
  Lean.Grind.CommRing.eq_gcd_cert a b (Lean.Grind.CommRing.Poly.num g) (Lean.Grind.CommRing.Poly.num g_1)
      (Lean.Grind.CommRing.Poly.num g_2) =
    (g_2 == a * g + b * g_1)