mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
_private.Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic.0.CategoryTheory.WithInitial.id.match_1.eq_2 : ∀ {C : Type u_1} (motive : CategoryTheory.WithInitial C → Sort u_2)
  (h_1 : (a : C) → motive (CategoryTheory.WithInitial.of a)) (h_2 : Unit → motive CategoryTheory.WithInitial.star),
  (match CategoryTheory.WithInitial.star with
    | CategoryTheory.WithInitial.of a => h_1 a
    | CategoryTheory.WithInitial.star => h_2 ()) =
    h_2 ()
-- Mathlib.Topology.Order.MonotoneContinuity
OrderIso.instHomeomorphClass : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : TopologicalSpace α]
  [inst_3 : TopologicalSpace β] [OrderTopology α] [OrderTopology β], HomeomorphClass (α ≃o β) α β
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.foldlM_toList : ∀ {α β : Type w} {γ : Type x} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] {m : Type x → Type x'}
  [inst_2 : Monad m] [LawfulMonad m] [inst_4 : Std.IteratorLoop α Id m] [Std.LawfulIteratorLoop α Id m]
  {f : γ → β → m γ} {init : γ} {it : Std.Iter β}, List.foldlM f init it.toList = Std.Iter.foldM f init it
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion
SemiNormedGrp.completion.lift_unique : ∀ {V W : SemiNormedGrp} [inst : CompleteSpace W.carrier] [inst_1 : T0Space W.carrier] (f : V ⟶ W)
  (g : SemiNormedGrp.completion.obj V ⟶ W),
  CategoryTheory.CategoryStruct.comp SemiNormedGrp.completion.incl g = f → g = SemiNormedGrp.completion.lift f
-- Mathlib.AlgebraicTopology.SimplicialSet.Simplices
SSet.S.equivElements_symm_apply_simplex : ∀ {X : SSet} (a : CategoryTheory.Functor.Elements X), (SSet.S.equivElements.symm a).simplex = a.snd
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
LinearMap.ker_localizedMap_eq_localized'_ker : ∀ {R : Type u_1} (S : Type u_2) {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Algebra R S] [inst_7 : Module S N] [inst_8 : IsScalarTower R S N] (p : Submonoid R)
  [inst_9 : IsLocalization p S] (f : M →ₗ[R] N) [inst_10 : IsLocalizedModule p f] {P : Type u_5}
  [inst_11 : AddCommMonoid P] [inst_12 : Module R P] {Q : Type u_6} [inst_13 : AddCommMonoid Q] [inst_14 : Module R Q]
  [inst_15 : Module S Q] [IsScalarTower R S Q] (f' : P →ₗ[R] Q) [inst_17 : IsLocalizedModule p f'] (g : M →ₗ[R] P),
  ((IsLocalizedModule.map p f f') g).ker = Submodule.restrictScalars R (Submodule.localized' S p f g.ker)
-- Mathlib.Analysis.SpecialFunctions.Complex.Arctan
/-- `cos z` is nonzero when the bounds in `arctan_tan` are met (`z` lies in the vertical strip
`-π / 2 < z.re < π / 2` and `z ≠ π / 2`).  -/
Complex.cos_ne_zero_of_arctan_bounds : ∀ {z : ℂ}, z ≠ ↑Real.pi / 2 → -(Real.pi / 2) < z.re → z.re ≤ Real.pi / 2 → Complex.cos z ≠ 0
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey_minKey : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {he : t.isEmpty = false} {hc : t.minKey he ∈ t}, t.getKey (t.minKey he) hc = t.minKey he
-- Mathlib.Topology.UniformSpace.DiscreteUniformity
/-- A product of spaces with discrete uniformity has a discrete uniformity.  -/
DiscreteUniformity.instProd : ∀ {X : Type u_1} [u : UniformSpace X] [DiscreteUniformity X] {Y : Type u_2} [inst : UniformSpace Y]
  [DiscreteUniformity Y], DiscreteUniformity (X × Y)
-- Lean.Elab.Tactic.Omega.Core
/-- The result of `tidy` on another `Justification`.  -/
Lean.Elab.Tactic.Omega.Justification.tidy : {s : Lean.Omega.Constraint} →
  {c : Lean.Omega.Coeffs} →
    Lean.Elab.Tactic.Omega.Justification s c →
      Lean.Elab.Tactic.Omega.Justification (Lean.Omega.tidyConstraint s c) (Lean.Omega.tidyCoeffs s c)
-- Init.Data.Bool
Bool.instDecidableExistsOfDecidablePred : (p : Bool → Prop) → [inst : DecidablePred p] → Decidable (∃ x, p x)
-- Mathlib.MeasureTheory.Covering.Besicovitch
Besicovitch.TauPackage.iUnionUpTo.congr_simp : ∀ {α : Type u_1} [inst : MetricSpace α] {β : Type u} [inst_1 : Nonempty β] (p p_1 : Besicovitch.TauPackage β α),
  p = p_1 → ∀ (i i_1 : Ordinal.{u}), i = i_1 → ∀ (a a_1 : α), a = a_1 → p.iUnionUpTo i a = p_1.iUnionUpTo i_1 a_1
-- Std.Http.Protocol.H1.Parser
/-- Parses an HTTP token (RFC 9110 §5.6.2): one or more token characters, up to `limit` bytes.
Fails if the input starts with a non-token character or is empty.
 -/
_private.Std.Http.Protocol.H1.Parser.0.Std.Http.Protocol.H1.parseToken : ℕ → Std.Internal.Parsec.ByteArray.Parser ByteSlice
-- Lean.Meta.Tactic.Grind.Proof
_private.Lean.Meta.Tactic.Grind.Proof.0.Lean.Meta.Grind.mkCongrProofFunCC : Lean.Expr → Lean.Expr → Bool → Lean.Meta.Grind.GoalM Lean.Expr
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.instSetLike : {α : Type u_1} → [inst : TopologicalSpace α] → SetLike (TopologicalSpace.NonemptyCompacts α) α
-- Mathlib.Order.Filter.Cocardinal
Filter.eventually_cocardinal_notMem_of_card_lt : ∀ {α : Type u} {c : Cardinal.{u}} {hreg : c.IsRegular} {s : Set α},
  Cardinal.mk ↑s < c → ∀ᶠ (x : α) in Filter.cocardinal α hreg, x ∉ s
-- Mathlib.Analysis.SpecialFunctions.Complex.Analytic
AnalyticOn.re_ofReal : ∀ {f : ℂ → ℂ} {s : Set ℝ}, AnalyticOn ℂ f (Complex.ofReal '' s) → AnalyticOn ℝ (fun x => (f ↑x).re) s
-- Mathlib.Combinatorics.Configuration
Configuration.ProjectivePlane.pointCount_eq_pointCount : ∀ (P : Type u_1) {L : Type u_2} [inst : Membership P L] [Configuration.ProjectivePlane P L] [Finite P] [Finite L]
  (l m : L), Configuration.pointCount P l = Configuration.pointCount P m
-- Mathlib.MeasureTheory.Group.Arithmetic
AEMeasurable.fun_vadd : ∀ {M : Type u_2} {X : Type u_3} {α : Type u_4} [inst : MeasurableSpace X] [inst_1 : VAdd M X] {m : MeasurableSpace α}
  {f : α → M} {g : α → X} [inst_2 : MeasurableSpace M] [MeasurableVAdd₂ M X] {μ : MeasureTheory.Measure α},
  AEMeasurable f μ → AEMeasurable g μ → AEMeasurable (fun i => f i +ᵥ g i) μ
-- Mathlib.GroupTheory.Finiteness
AddSubmonoid.map.congr_simp : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] (f f_1 : F),
  f = f_1 → ∀ (S S_1 : AddSubmonoid M), S = S_1 → AddSubmonoid.map f S = AddSubmonoid.map f_1 S_1
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.mono_of_kernel_iso_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X Y : C} {f : X ⟶ Y}
  [inst_3 : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair f 0)]
  (w : CategoryTheory.Limits.kernel f ≅ 0), CategoryTheory.Mono f
-- Mathlib.Algebra.Homology.ShortComplex.Basic
/-- The isomorphism of short complexes `S.map F ≅ S.map G` induced by
a natural isomorphism `F ≅ G`.  -/
CategoryTheory.ShortComplex.mapNatIso : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            (S : CategoryTheory.ShortComplex C) →
              {F G : CategoryTheory.Functor C D} →
                [inst_4 : F.PreservesZeroMorphisms] →
                  [inst_5 : G.PreservesZeroMorphisms] → (F ≅ G) → (S.map F ≅ S.map G)
-- Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
GenContFract.squashGCF.eq_2 : ∀ {K : Type u_1} [inst : DivisionRing K] (g : GenContFract K) (n : ℕ),
  g.squashGCF n.succ = { h := g.h, s := GenContFract.squashSeq g.s n }
-- Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
/-- If `f` is harmonic at `x`, then it is harmonic at all points in a neighborhood of `x`.
 -/
InnerProductSpace.HarmonicAt.eventually : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f : E → F} {x : E},
  InnerProductSpace.HarmonicAt f x → ∀ᶠ (y : E) in nhds x, InnerProductSpace.HarmonicAt f y
-- Mathlib.NumberTheory.Pell
/-- The `n`th power of a fundamental solution is trivial if and only if `n = 0`.  -/
Pell.IsFundamental.zpow_eq_one_iff : ∀ {d : ℤ} {a : Pell.Solution₁ d}, Pell.IsFundamental a → ∀ (n : ℤ), a ^ n = 1 ↔ n = 0
-- Mathlib.Data.ENNReal.Real
ENNReal.toReal_top_mul : ∀ (a : ENNReal), (⊤ * a).toReal = 0
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.univ_pi_Ioo_ae_eq_Icc : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  {μ : (i : ι) → MeasureTheory.Measure (α i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)]
  [inst_3 : (i : ι) → PartialOrder (α i)] [∀ (i : ι), MeasureTheory.NullSingletonClass (μ i)] {f g : (i : ι) → α i},
  (Set.univ.pi fun i => Set.Ioo (f i) (g i)) =ᵐ[MeasureTheory.Measure.pi μ] Set.Icc f g
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
NNReal.tsum_eq_add_tsum_ite : ∀ {α : Type u_1} {f : α → NNReal}, Summable f → ∀ (i : α), ∑' (x : α), f x = f i + ∑' (x : α), if x = i then 0 else f x
-- Mathlib.NumberTheory.Primorial
primorial_add_dvd : ∀ {m n : ℕ}, n ≤ m → primorial (m + n) ∣ primorial m * (m + n).choose m
-- Mathlib.Algebra.Polynomial.Eval.Subring
Polynomial.notMem_map_rangeS : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) {p : Polynomial S},
  p ∉ (Polynomial.mapRingHom f).rangeS ↔ ∃ n, p.coeff n ∉ f.rangeS
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Expr.var.injEq : ∀ (i i_1 : Nat.Internal.Linear.Var), (Nat.Internal.Linear.Expr.var i = Nat.Internal.Linear.Expr.var i_1) = (i = i_1)
-- Mathlib.Analysis.Calculus.Deriv.Comp
HasDerivWithinAt.comp_hasFDerivWithinAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type w} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝕜' : Type u_1} [inst_3 : NontriviallyNormedField 𝕜'] [inst_4 : NormedAlgebra 𝕜 𝕜']
  {h₂ : 𝕜' → 𝕜'} {h₂' : 𝕜'} {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} {s : Set E} {t : Set 𝕜'} (x : E),
  HasDerivWithinAt h₂ h₂' t (f x) →
    HasFDerivWithinAt f f' s x → Set.MapsTo f s t → HasFDerivWithinAt (h₂ ∘ f) (h₂' • f') s x
-- Mathlib.Algebra.Module.Hom
/-- Scalar multiplication on the left as an additive monoid homomorphism.

See also the linear map version of this `Module.End.smulLeft`.  -/
AddMonoidHom.smulLeft : {M : Type u_3} → {A : Type u_4} → [inst : AddMonoid A] → [DistribSMul M A] → M → A →+ A
-- Mathlib.Analysis.Convex.GaugeRescale
image_gaugeRescaleHomeomorph_interior : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E]
  [inst_3 : IsTopologicalAddGroup E] [inst_4 : ContinuousSMul ℝ E] [inst_5 : T1Space E] {s t : Set E} (hsc : Convex ℝ s)
  (hs₀ : s ∈ nhds 0) (hsb : Bornology.IsVonNBounded ℝ s) (htc : Convex ℝ t) (ht₀ : t ∈ nhds 0)
  (htb : Bornology.IsVonNBounded ℝ t), ⇑(gaugeRescaleHomeomorph s t hsc hs₀ hsb htc ht₀ htb) '' interior s = interior t
-- Mathlib.RingTheory.Artinian.Module
isArtinian_of_linearEquiv : ∀ {R : Type u_1} {M : Type u_2} {P : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid P]
  [inst_3 : Module R M] [inst_4 : Module R P] (f : M ≃ₗ[R] P) [IsArtinian R M], IsArtinian R P
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Algebra.forget_reflects_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C},
  (CategoryTheory.Endofunctor.Algebra.forget F).ReflectsIsomorphisms
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.lintegral_mono_set : ∀ {α : Type u_1} {x : MeasurableSpace α} ⦃μ : MeasureTheory.Measure α⦄ {s t : Set α} {f : α → ENNReal},
  s ⊆ t → ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in t, f x ∂μ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKeyD_le_maxKeyD_insert : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF),
  t.isEmpty = false →
    ∀ {k : α} {v : β k} {fallback : α},
      (compare (t.maxKeyD fallback) ((Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.maxKeyD fallback)).isLE = true
-- Mathlib.NumberTheory.RamificationInertia.HilbertTheory
IsDecompositionField.algebraMap_ringEquiv_apply : ∀ (K : Type u_2) (L : Type u_3) {B : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : CommRing B] (P : Ideal B) (D : Type u_5) [inst_4 : Field D] [inst_5 : Algebra D L]
  [inst_6 : MulSemiringAction Gal(L/K) B] (D' : Type u_8) [inst_7 : Field D'] [inst_8 : Algebra D' L]
  [inst_9 : IsDecompositionField K L P D] [inst_10 : IsDecompositionField K L P D'] (x : D),
  (algebraMap D' L) ((IsDecompositionField.ringEquiv K L P D D') x) = (algebraMap D L) x
-- Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
Complex.hasDerivAt_log : ∀ {z : ℂ}, z ∈ Complex.slitPlane → HasDerivAt Complex.log z⁻¹ z
-- Mathlib.Data.Finsupp.Basic
Finsupp.graph_inj : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {f g : α →₀ M}, f.graph = g.graph ↔ f = g
-- Mathlib.Data.PEquiv
/-- Turns an `Equiv` into a `PEquiv` of the whole type.  -/
Equiv.toPEquiv : {α : Type u_1} → {β : Type u_2} → α ≃ β → α ≃. β
-- Mathlib.Algebra.Module.Presentation.DirectSum
Module.Relations.Solution.directSumEquiv_apply_var : ∀ {A : Type u} [inst : Ring A] {ι : Type w} {relations : ι → Module.Relations A} {N : Type v} [inst_1 : AddCommGroup N]
  [inst_2 : Module A N] (s : (Module.Relations.directSum relations).Solution N) (i : ι) (g : (relations i).G),
  (Module.Relations.Solution.directSumEquiv s i).var g = s.var ⟨i, g⟩
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.ofList_eq_foldl : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {l : List α},
  Std.ExtHashSet.ofList l = List.foldl (fun acc a => acc.insert a) ∅ l
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.productUniqueIso_inv_π_assoc : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : Unique β] (f : β → C) (b : β) {Z : C}
  (h : f b ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.productUniqueIso f).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f b) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h
-- Mathlib.Algebra.CubicDiscriminant
Cubic.leadingCoeff_of_c_ne_zero : ∀ {R : Type u_1} {P : Cubic R} [inst : Semiring R], P.a = 0 → P.b = 0 → P.c ≠ 0 → P.toPoly.leadingCoeff = P.c
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.associator_inv_τl : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : CategoryTheory.Bicategory.Adj B} (α : a ⟶ b) (β : b ⟶ c)
  (γ : c ⟶ d),
  (CategoryTheory.Bicategory.associator α β γ).inv.τl = (CategoryTheory.Bicategory.associator α.l β.l γ.l).inv
-- Init.Data.Order.LemmasExtra
Std.instLawfulEqOrdOfLawfulOrderOrdOfAntisymmLe : ∀ {α : Type u} [inst : Ord α] [inst_1 : LE α] [Std.LawfulOrderOrd α] [Std.Antisymm fun x1 x2 => x1 ≤ x2],
  Std.LawfulEqOrd α
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.d₁₂_hom_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u_1, u, u} k G) (f : G → ↑A) (g : G × G),
  (ModuleCat.Hom.hom (groupCohomology.d₁₂ A)) f g = (A.ρ g.1) (f g.2) - f (g.1 * g.2) + f g.1
-- Init.Data.String.Substring
/-- Checks whether the substring can be interpreted as the decimal representation of a natural number,
returning the number if it can.

A substring can be interpreted as a decimal natural number if it is not empty and all the characters
in it are digits. Underscores ({lit}`_`) are allowed as digit separators and are ignored during parsing.

Use `Substring.isNat` to check whether the substring is such a substring.
 -/
Substring.Raw.toNat? : Substring.Raw → Option ℕ
-- Init.Data.Vector.Lemmas
/-- Variant of `getElem_pop` that will sometimes fire when `getElem_pop` gets stuck because of
defeq issues in the implicit size argument.
 -/
Vector.getElem_pop' : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α (n + 1)} {i : ℕ} (h : i < n + 1 - 1), xs.pop[i] = xs[i]
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
Monotone.csSup_image_le_map_csSup : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice β] [inst_1 : ConditionallyCompleteLattice α]
  {f : α → β} {s : Set α},
  s.Nonempty →
    Monotone f → autoParam (BddAbove s) Monotone.csSup_image_le_map_csSup._auto_1 → sSup (f '' s) ≤ f (sSup s)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.lowerBound?_mem : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x y : α} [Std.OrientedCmp cmp] {t : RBTree.RBSet α cmp},
  t.lowerBound? x = some y → y ∈ t
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
cmp_mul_neg_right : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] [ExistsAddOfLE R] [MulPosStrictMono R] [AddRightReflectLT R]
  [AddRightStrictMono R] {a : R}, a < 0 → ∀ (b c : R), cmp (b * a) (c * a) = cmp c b
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_dvd_right_split_dvd2_cert : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → ℤ → ℕ → ℤ → Int.Internal.Linear.Poly → Bool
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.maxEntryD.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → (a : α) × β a → Sort u_3)
  (fallback : (a : α) × β a) (h_1 : (fallback : (a : α) × β a) → motive Std.DTreeMap.Internal.Impl.leaf fallback)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (x : (a : α) × β a) →
              motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x)
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β k_1) →
                  (l_1 r_1 : Std.DTreeMap.Internal.Impl α β) →
                    r = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1 →
                      (fallback : (a : α) × β a) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v l
                            (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1))
                          fallback),
  (match Std.DTreeMap.Internal.Impl.leaf, fallback with
    | Std.DTreeMap.Internal.Impl.leaf, fallback => h_1 fallback
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x => h_2 size k v l x
    | Std.DTreeMap.Internal.Impl.inner size k v l r@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1),
      fallback => h_3 size k v l r size_1 k_1 v_1 l_1 r_1 h fallback) =
    h_1 fallback
-- Mathlib.RepresentationTheory.Irreducible
Representation.IsIrreducible.bijective_or_eq_zero : ∀ {G : Type u_1} {k : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Field k]
  [inst_2 : AddCommGroup V] [inst_3 : Module k V] [inst_4 : AddCommGroup W] [inst_5 : Module k W]
  {ρ : Representation k G V} {σ : Representation k G W} (f : ρ.IntertwiningMap σ) [ρ.IsIrreducible] [σ.IsIrreducible],
  Function.Bijective ⇑f ∨ f = 0
-- Mathlib.Topology.NhdsWithin
sdiff_mem_nhdsWithin_compl : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {s : Set α}, s ∈ nhds x → ∀ (t : Set α), s \ t ∈ nhdsWithin x tᶜ
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- The bijection between the (normalized) prime factors of `r` and the (normalized) prime factors
of `span {r}`  -/
Ideal.normalizedFactorsEquivSpanNormalizedFactors : {R : Type u_1} →
  [inst : CommRing R] →
    [inst_1 : IsDomain R] →
      [inst_2 : IsPrincipalIdealRing R] →
        [inst_3 : NormalizationMonoid R] →
          {r : R} →
            r ≠ 0 →
              ↑{d | d ∈ UniqueFactorizationMonoid.normalizedFactors r} ≃
                ↑{I | I ∈ UniqueFactorizationMonoid.normalizedFactors (Ideal.span {r})}
-- Mathlib.Algebra.Module.FinitePresentation
Module.FinitePresentation.pi : ∀ {R : Type u_3} [inst : Ring R] {ι : Type u_1} (M : ι → Type u_2) [inst_1 : (i : ι) → AddCommGroup (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [∀ (i : ι), Module.FinitePresentation R (M i)] [Finite ι],
  Module.FinitePresentation R ((i : ι) → M i)
-- Mathlib.Data.Ordmap.Invariants
Ordnode.balancedSz_up : ∀ {l r₁ r₂ : ℕ}, r₁ ≤ r₂ → l + r₂ ≤ 1 ∨ r₂ ≤ Ordnode.delta * l → Ordnode.BalancedSz l r₁ → Ordnode.BalancedSz l r₂
-- Mathlib.Analysis.Normed.Module.ContinuousInverse
/-- An invertible continuous linear map has a continuous right inverse.  -/
ContinuousLinearMap.HasRightInverse.of_isInvertible : ∀ {R : Type u_1} [inst : Semiring R] {E : Type u_2} {F : Type u_4} [inst_1 : TopologicalSpace E]
  [inst_2 : AddCommMonoid E] [inst_3 : Module R E] [inst_4 : TopologicalSpace F] [inst_5 : AddCommMonoid F]
  [inst_6 : Module R F] {f : E →L[R] F}, f.IsInvertible → f.HasRightInverse
-- Mathlib.LinearAlgebra.Projectivization.Basic
Projectivization.instNonemptyOfNontrivial : ∀ (K : Type u_1) {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] [Nontrivial V],
  Nonempty (Projectivization K V)
-- Mathlib.NumberTheory.NumberField.Completion.Ramification
/-- If `w` is an unramified place over `v` then `w.Completion` has `v.Completion` dimension one.  -/
NumberField.InfinitePlace.IsUnramified.finrank_eq_one : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (v : NumberField.InfinitePlace K) {w : NumberField.InfinitePlace L} [inst_3 : w.LiesOver v],
  NumberField.InfinitePlace.IsUnramified K w → Module.finrank v.Completion w.Completion = 1
-- Mathlib.Topology.Order.OrderClosed
continuousWithinAt_Ioo_iff_Iio : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIicTopology α]
  [inst_3 : TopologicalSpace β] {a b : α} {f : α → β},
  a < b → (ContinuousWithinAt f (Set.Ioo a b) b ↔ ContinuousWithinAt f (Set.Iio b) b)
-- Mathlib.Algebra.Lie.Quotient
LieSubmodule.Quotient.toEnd_comp_mk' : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N : LieSubmodule R L M) [inst_5 : LieAlgebra R L]
  [inst_6 : LieModule R L M] (x : L),
  (LieModule.toEnd R L (M ⧸ N)) x ∘ₗ ↑(LieSubmodule.Quotient.mk' N) =
    ↑(LieSubmodule.Quotient.mk' N) ∘ₗ (LieModule.toEnd R L M) x
-- Mathlib.Geometry.Manifold.ChartedSpace
ModelProd.ext : ∀ {H : Type u} {H' : Type u_1} {x y : ModelProd H H'}, x.1 = y.1 → x.2 = y.2 → x = y
-- Mathlib.GroupTheory.GroupAction.Iwasawa
MulAction.IwasawaStructure.mk : {M : Type u_1} →
  [inst : Group M] →
    {α : Type u_2} →
      [inst_1 : MulAction M α] →
        (T : α → Subgroup M) →
          (∀ (x : α), IsMulCommutative ↥(T x)) →
            (∀ (g : M) (x : α), T (g • x) = MulAut.conj g • T x) → iSup T = ⊤ → MulAction.IwasawaStructure M α
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.IsBigO.multisetProd : ∀ {α : Type u_1} {l : Filter α} {ι : Type u_17} {R : Type u_18} {𝕜 : Type u_19} [inst : SeminormedCommRing R]
  [inst_1 : NormedField 𝕜] {s : Multiset ι} {f : ι → α → R} {g : ι → α → 𝕜},
  (∀ i ∈ s, f i =O[l] g i) →
    (fun x => (Multiset.map (fun x_1 => f x_1 x) s).prod) =O[l] fun x => (Multiset.map (fun x_1 => g x_1 x) s).prod
-- Mathlib.Data.Multiset.UnionInter
Multiset.disjoint_union_left : ∀ {α : Type u_1} [inst : DecidableEq α] {s t u : Multiset α}, Disjoint (s ∪ t) u ↔ Disjoint s u ∧ Disjoint t u
-- Mathlib.Analysis.Normed.Group.Continuity
continuous_nnnorm' : ∀ {E : Type u_4} [inst : SeminormedGroup E], Continuous fun a => ‖a‖₊
-- Mathlib.Algebra.Lie.Prod
LieHom.range_inr : ∀ (R : Type u_1) (L₁ : Type u_2) (L₂ : Type u_3) [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁]
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂],
  (LieHom.inr R L₁ L₂).range = LieIdeal.toLieSubalgebra R (L₁ × L₂) (LieHom.fst R L₁ L₂).ker