mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.LeftExact
/-- An auxiliary definition to be used in the proof of the fact that
`J.diagramFunctor D X` preserves limits.  -/
CategoryTheory.GrothendieckTopology.liftToDiagramLimitObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {D : Type w} →
        [inst_1 : CategoryTheory.Category.{t, w} D] →
          [inst_2 :
              ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X),
                CategoryTheory.Limits.HasMultiequalizer (S.index P)] →
            {X : C} →
              {K : Type s} →
                [inst_3 : CategoryTheory.SmallCategory K] →
                  [inst_4 : CategoryTheory.Limits.HasLimitsOfShape K D] →
                    {W : (J.Cover X)ᵒᵖ} →
                      (F : CategoryTheory.Functor K (CategoryTheory.Functor Cᵒᵖ D)) →
                        (E :
                            CategoryTheory.Limits.Cone
                              (F.comp
                                ((J.diagramFunctor D X).comp ((CategoryTheory.evaluation (J.Cover X)ᵒᵖ D).obj W)))) →
                          E.pt ⟶ (J.diagram (CategoryTheory.Limits.limit F) X).obj W
-- Init.Data.Array.Lemmas
List.toListRev_toArray : ∀ {α : Type u_1} {l : List α}, l.toArray.toListRev = l.reverse
-- Mathlib.Combinatorics.Quiver.Path.Vertices
Quiver.Path.vertices_comp_get_length_eq : ∀ {V : Type u_1} [inst : Quiver V] {a b c : V} (p₁ : Quiver.Path a c) (p₂ : Quiver.Path c b)
  (h : autoParam (p₁.length < (p₁.comp p₂).vertices.length) Quiver.Path.vertices_comp_get_length_eq._auto_1),
  (p₁.comp p₂).vertices.get ⟨p₁.length, h⟩ = c
-- Mathlib.Order.Interval.Set.SuccPred
Set.Icc_succ_pred_eq_Ioo : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] [inst_2 : PredOrder α] [Nontrivial α] (a b : α),
  Set.Icc (Order.succ a) (Order.pred b) = Set.Ioo a b
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.comapRingHom_apply_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {Z : Type u_6}
  [inst_2 : Semiring Z] (f : C(X, Y)) (g : LocallyConstant Y Z) (a : X),
  ((LocallyConstant.comapRingHom f) g) a = g (f a)
-- Batteries.Data.DList.Lemmas
Batteries.DList.ofList.eq_1 : ∀ {α : Type u} (l : List α), Batteries.DList.ofList l = { apply := fun x => l ++ x, invariant := ⋯ }
-- Mathlib.Data.Seq.Basic
Stream'.Seq.terminatedAt_map_iff : ∀ {α : Type u} {β : Type v} {f : α → β} {s : Stream'.Seq α} {n : ℕ},
  (Stream'.Seq.map f s).TerminatedAt n ↔ s.TerminatedAt n
-- Init.CbvSimproc
/-- A `cbv_simproc` declaration without automatically adding it to the cbv simproc set.
To activate, use `attribute [cbv_simproc]`.
 -/
Lean.Parser.«command_Cbv_simproc_decl_(_):=_» : Lean.ParserDescr
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Real.ball_eq_Ioo : ∀ (x r : ℝ), Metric.ball x r = Set.Ioo (x - r) (x + r)
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.map_apply : ∀ {α : Type u_1} {β : Type u_3} (f : α → β) (m : MeasureTheory.OuterMeasure α) (s : Set β),
  ((MeasureTheory.OuterMeasure.map f) m) s = m (f ⁻¹' s)
-- Init.Data.String.Termination
String.Pos.Down.mk.sizeOf_spec : ∀ {s : String} (inner : s.Pos), sizeOf { inner := inner } = 1 + sizeOf inner
-- Mathlib.Algebra.GradedMonoid
GradedMonoid.mk_mul_mk : ∀ {ι : Type u_1} (A : ι → Type u_2) [inst : Add ι] [inst_1 : GradedMonoid.GMul A] {i j : ι} (a : A i) (b : A j),
  GradedMonoid.mk i a * GradedMonoid.mk j b = GradedMonoid.mk (i + j) (GradedMonoid.GMul.mul a b)
-- Aesop.Stats.Basic
Aesop.GoalStats.mk.inj : ∀ {goalId : ℕ} {goalKind : Aesop.GoalKind} {lctxSize depth : ℕ} {forwardStateStats : Aesop.ForwardStateStats}
  {goalId_1 : ℕ} {goalKind_1 : Aesop.GoalKind} {lctxSize_1 depth_1 : ℕ} {forwardStateStats_1 : Aesop.ForwardStateStats},
  { goalId := goalId, goalKind := goalKind, lctxSize := lctxSize, depth := depth,
        forwardStateStats := forwardStateStats } =
      { goalId := goalId_1, goalKind := goalKind_1, lctxSize := lctxSize_1, depth := depth_1,
        forwardStateStats := forwardStateStats_1 } →
    goalId = goalId_1 ∧
      goalKind = goalKind_1 ∧ lctxSize = lctxSize_1 ∧ depth = depth_1 ∧ forwardStateStats = forwardStateStats_1
-- Lean.Data.Options
Lean.Options.erase : Lean.Options → Lean.Name → Lean.Options
-- Mathlib.Analysis.Normed.Ring.Basic
ULift.nonUnitalSeminormedCommRing : {α : Type u_2} → [NonUnitalSeminormedCommRing α] → NonUnitalSeminormedCommRing (ULift.{u_5, u_2} α)
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Finsupp.linearCombination_restrict : ∀ {α : Type u_1} {M : Type u_2} (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {v : α → M} (s : Set α),
  Finsupp.linearCombination R (s.domRestrict v) =
    (Submodule.span R (v '' s)).subtype ∘ₗ
      Finsupp.linearCombinationOn α M R v s ∘ₗ ↑(Finsupp.supportedEquivFinsupp s).symm
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.divCoeffs : Lean.Meta.Grind.Arith.Cutsat.LeCnstr → Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.IsPartition.existsUnique : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.Prepartition I} {x : ι → ℝ},
  π.IsPartition → x ∈ I → ∃! J, J ∈ π ∧ x ∈ J
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.instMonadStateOfHoleIteratorDelabM : MonadStateOf Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator Lean.PrettyPrinter.Delaborator.DelabM
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
AlgebraicGeometry.UniversallyOpen.instOfIsOpenImmersion : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f],
  AlgebraicGeometry.UniversallyOpen f
-- Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Algebra.IsStandardSmooth.subsingleton_h1Cotangent : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.IsStandardSmooth R S], Subsingleton (Algebra.H1Cotangent R S)
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.IndepFun.symm : ∀ {Ω : Type u_1} {β : Type u_6} {β' : Type u_7} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : Ω → β}
  {g : Ω → β'} {x : MeasurableSpace β} {x_1 : MeasurableSpace β'},
  ProbabilityTheory.IndepFun f g μ → ProbabilityTheory.IndepFun g f μ
-- Mathlib.Data.Matrix.Mul
/-- Permuting a vector on the right of a dot product can be transferred to the left.  -/
dotProduct_comp_equiv_symm : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : NonUnitalNonAssocSemiring α] (u : m → α) (x : n → α) (e : n ≃ m), u ⬝ᵥ x ∘ ⇑e.symm = u ∘ ⇑e ⬝ᵥ x
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.instIsSMulApply : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] {S₂ : Type u_9}
  [inst_8 : DistribSMul S₂ M₂] [inst_9 : SMulCommClass R₂ S₂ M₂] [inst_10 : ContinuousConstSMul S₂ M₂],
  IsSMulApply S₂ (M₁ →SL[σ₁₂] M₂) M₁ M₂
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.AdicCauchySequence.instSMulInt : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      (M : Type u_4) →
        [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → SMul ℤ (AdicCompletion.AdicCauchySequence I M)
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.HomotopyEquiv.refl_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (S : CategoryTheory.ShortComplex C),
  (CategoryTheory.ShortComplex.HomotopyEquiv.refl S).inv = CategoryTheory.CategoryStruct.id S
-- Mathlib.RingTheory.ClassGroup.Basic
PrincipalIdeals.normal : ∀ {R : Type u_1} {K : Type u_2} [inst : CommRing R] [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K], (toPrincipalIdeal R K).range.Normal
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_pair_abs : ∀ {α : Type u} [inst : Ring α] (x y : α) [inst_1 : LinearOrder α], Ideal.span {x, |y|} = Ideal.span {x, y}
-- Mathlib.Analysis.Normed.Lp.lpSpace
LipschitzOnWith.coordinate : ∀ {α : Type u_3} {ι : Type u_5} [inst : PseudoMetricSpace α] (f : α → ↥(lp (fun x => ℝ) ⊤)) (s : Set α) (K : NNReal),
  LipschitzOnWith K f s ↔ ∀ (i : ι), LipschitzOnWith K (fun a => ↑(f a) i) s
-- Mathlib.Combinatorics.SimpleGraph.LineGraph
/-- **Alias** of `SimpleGraph.map_lineGraph_le_of_le`. -/
SimpleGraph.IsSubgraph.lineGraph : ∀ {V : Type u_1} {G G' : SimpleGraph V},
  G ≤ G' →
    SimpleGraph.map (⇑(Function.Embedding.subtype fun x => x ∈ G.edgeSet)) G.lineGraph ≤
      SimpleGraph.map (⇑(Function.Embedding.subtype fun x => x ∈ G'.edgeSet)) G'.lineGraph
-- Mathlib.AlgebraicGeometry.OpenImmersion
/-- The `fg` argument is to avoid nasty stuff about dependent types.  -/
AlgebraicGeometry.IsOpenImmersion.app_eq_appIso_inv_app_of_comp_eq : ∀ {X Y U : AlgebraicGeometry.Scheme} (f : Y ⟶ U) (g : U ⟶ X) (fg : Y ⟶ X)
  (H : fg = CategoryTheory.CategoryStruct.comp f g) [h : AlgebraicGeometry.IsOpenImmersion g] (V : U.Opens),
  AlgebraicGeometry.Scheme.Hom.app f V =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appIso g V).inv
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.Scheme.Hom.app fg ((AlgebraicGeometry.Scheme.Hom.opensFunctor g).obj V))
        (Y.presheaf.map (CategoryTheory.eqToHom ⋯).op))
-- Mathlib.NumberTheory.Modular
ModularGroup.im_T_smul : ∀ (z : UpperHalfPlane), (ModularGroup.T • z).im = z.im
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_eq_getKeyD_default : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α], t.WF → ∀ {a : α}, t.getKey! a = t.getKeyD a default
-- Lean.ParserCompiler
Lean.ParserCompiler.compileEmbeddedParsers : {α : Type} → Lean.ParserCompiler.Context α → Bool → Lean.ParserDescr → Lean.MetaM Unit
-- Mathlib.MeasureTheory.Measure.Tilted
MeasureTheory.isProbabilityMeasure_tilted : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} [NeZero μ],
  MeasureTheory.Integrable (fun x => Real.exp (f x)) μ → MeasureTheory.IsProbabilityMeasure (μ.tilted f)
-- Lean.Parser.Basic
Lean.Parser.numberFnAux : optParam Bool true → Lean.Parser.ParserFn
-- Lean.Meta.Tactic.Simp.Types
/-- Result type for a simplification procedure. We have `pre` and `post` simplification procedures.
 -/
Lean.Meta.Simp.Step : Type
-- Mathlib.Order.ModularLattice
instIsWeakLowerModularLatticeOrderDual : ∀ {α : Type u_1} [inst : Lattice α] [IsWeakUpperModularLattice α], IsWeakLowerModularLattice αᵒᵈ
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearEquiv.isQuasiInverse : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [inst : CommRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] (e : V ≃ₗ[K] V₂), (↑e.symm).IsQuasiInverse ↑e
-- Mathlib.Algebra.Order.GroupWithZero.Action.Synonym
OrderDual.instDistribSMul : {G₀ : Type u_1} → {M₀ : Type u_2} → [inst : AddZeroClass M₀] → [DistribSMul G₀ M₀] → DistribSMul G₀ᵒᵈ M₀
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
_private.Mathlib.NumberTheory.EllipticDivisibilitySequence.0.preNormEDS'.match_1.eq_4 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : Unit → motive 2)
  (h_4 : Unit → motive 3) (h_5 : Unit → motive 4) (h_6 : (n : ℕ) → motive n.succ.succ.succ.succ.succ),
  (match 3 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | 2 => h_3 ()
    | 3 => h_4 ()
    | 4 => h_5 ()
    | n.succ.succ.succ.succ.succ => h_6 n) =
    h_4 ()
-- Init.Data.Iterators.Consumers.Loop
/-- Returns the first non-`none` result of applying `f` to each output of the iterator, in order.
Returns `none` if `f` returns `none` for all outputs.

`O(|it|)`. Short-circuits when `f` returns `some _`.The outputs of `it` are examined in order of
iteration.

This function is deprecated. Instead of `it.allowNontermination.findSome?`, use `it.findSome?`.

Examples:
 * `[7, 6, 5, 8, 1, 2, 6].iter.allowNontermination.findSome? (fun x => if x < 5 then some (10 * x) else none) = some 10`
 * `[7, 6, 5, 8, 1, 2, 6].iter.allowNontermination.findSome? (fun x => if x < 1 then some (10 * x) else none) = none`
 -/
Std.Iter.Partial.findSome? : {α β : Type w} →
  {γ : Type x} →
    [inst : Std.Iterator α Id β] → [Std.IteratorLoop α Id Id] → Std.Iter.Partial β → (β → Option γ) → Option γ
-- Std.Sat.AIG.Relabel
Std.Sat.AIG.Entrypoint.Unsat.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (entry : Std.Sat.AIG.Entrypoint α),
  entry.Unsat = entry.aig.UnsatAt entry.ref.gate entry.ref.invert ⋯
-- Mathlib.Topology.Algebra.Constructions
AddOpposite.opHomeomorph_symm_apply : ∀ {M : Type u_1} [inst : TopologicalSpace M] (a : Mᵃᵒᵖ), AddOpposite.opHomeomorph.symm a = AddOpposite.unop a
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.iSup_mrange_of : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)], ⨆ i, MonoidHom.mrange Monoid.CoprodI.of = ⊤
-- Lean.Data.KVMap
Lean.DataValue.ofInt.sizeOf_spec : ∀ (v : ℤ), sizeOf (Lean.DataValue.ofInt v) = 1 + sizeOf v
-- Init.Data.Function
Function.Injective.leftInverse : ∀ {α : Sort u_1} {β : Sort u_2} (f : α → β), Function.Injective f → ∀ [hα : Nonempty α], ∃ g, Function.LeftInverse g f
-- Mathlib.MeasureTheory.Measure.Haar.Extension
TopologicalAddGroup.IsSES.pushforward_apply_apply : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {E : Type u_4} [inst : AddGroup A] [inst_1 : AddGroup B]
  [inst_2 : AddGroup C] [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C]
  {φ : A →+ B} {ψ : B →+ C} (H : TopologicalAddGroup.IsSES φ ψ) [inst_6 : IsTopologicalAddGroup A]
  [inst_7 : IsTopologicalAddGroup B] [inst_8 : NormedAddCommGroup E] [inst_9 : MeasurableSpace A]
  [inst_10 : BorelSpace A] (μA : MeasureTheory.Measure A) [hμA : μA.IsAddHaarMeasure] [inst_11 : NormedSpace ℝ E]
  [inst_12 : IsTopologicalAddGroup C] [inst_13 : LocallyCompactSpace B] (f : CompactlySupportedContinuousMap B E)
  (b : B), ((H.pushforward μA) f) (ψ b) = ∫ (a : A), (H.pullback f b) a ∂μA
-- Mathlib.Data.Real.Basic
Real.ofCauchy_inf : ∀ (a b : CauSeq ℚ abs), { cauchy := ⟦a ⊓ b⟧ } = min { cauchy := ⟦a⟧ } { cauchy := ⟦b⟧ }
-- Std.Data.TreeSet.Iterator
/-- Returns a finite iterator over the entries of a tree set.
The iterator yields the elements of the set in order and then terminates.

**Termination properties:**

* `Finite` instance: always
* `Productive` instance: always
 -/
Std.TreeSet.iter : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet α cmp → Std.Iter α
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticForm.discr_comp : ∀ {R : Type u_3} {N : Type u_5} {P : Type u_6} {n : Type w} [inst : Fintype n] [inst_1 : DecidableEq n]
  [inst_2 : CommRing R] [inst_3 : Invertible 2] [inst_4 : AddCommGroup N] [inst_5 : Module R N] {b : Module.Basis n R N}
  [inst_6 : AddCommGroup P] [inst_7 : Module R P] (b' : Module.Basis n R P) (Q : QuadraticForm R P) (f : N →ₗ[R] P),
  QuadraticForm.discr b (QuadraticMap.comp Q f) =
    ((LinearMap.toMatrix b b') f).det * ((LinearMap.toMatrix b b') f).det * QuadraticForm.discr b' Q
-- Init.Data.Iterators.Consumers.Collect
/-- Traverses the given iterator and stores the emitted values in reverse order in a list. Because
lists are prepend-only, this `toListRev` is usually more efficient that `toList`.

If the iterator is not finite, this function might run forever. The variant
`it.ensureTermination.toListRev` always terminates after finitely many steps.
 -/
Std.Iter.toListRev : {α β : Type w} → [Std.Iterator α Id β] → Std.Iter β → List β
-- Mathlib.AlgebraicTopology.DoldKan.Compatibility
/-- The counit isomorphism of `equivalence`.  -/
AlgebraicTopology.DoldKan.Compatibility.equivalenceCounitIso : {A : Type u_1} →
  {B : Type u_3} →
    {B' : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} A] →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} B] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} B'] →
            {eB : B ≌ B'} →
              {F : CategoryTheory.Functor A B'} →
                {G : CategoryTheory.Functor B A} →
                  (G.comp F ≅ eB.functor) → (G.comp (F.comp eB.inverse) ≅ CategoryTheory.Functor.id B)
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.mulSingle_strictMono : ∀ {I : Type u} {f : I → Type v} (i : I) [inst : DecidableEq I] [inst_1 : (i : I) → Preorder (f i)]
  [inst_2 : (i : I) → One (f i)], StrictMono (Pi.mulSingle i)
-- Mathlib.Data.FunLike.Group
FunLike.addRightCancelMonoid.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Add F] [inst_2 : Zero F]
  [inst_3 : SMul ℕ F] [inst_4 : AddRightCancelMonoid β] [inst_5 : IsZeroApply F α β] [inst_6 : IsAddApply F α β]
  [inst_7 : IsSMulApply ℕ F α β],
  FunLike.addRightCancelMonoid = Function.Injective.addRightCancelMonoid (fun f => ⇑f) ⋯ ⋯ ⋯ ⋯
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.intCoe_apply : ∀ {R : Type u_1} [inst : AddGroupWithOne R] {f : ArithmeticFunction ℤ} {x : ℕ}, ↑f x = ↑(f x)
-- Mathlib.Data.Ordmap.Invariants
Ordnode.not_le_delta : ∀ {s : ℕ}, 1 ≤ s → ¬s ≤ Ordnode.delta * 0
-- Mathlib.NumberTheory.RamificationInertia.HilbertTheory
/-- Let `L/K` be a Galois extension of fields and let `P` be a prime ideal of `B`. The predicate that
says that `D` is the decomposition field of `P` in `L/K`, that is the subfield fixed by the
decomposition subgroup of `P`, that is the stabilizer of `P` in `Gal(L/K)`.
 -/
IsDecompositionField : (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] →
              Ideal B → (D : Type u_5) → [inst_4 : Field D] → [Algebra D L] → [MulSemiringAction Gal(L/K) B] → Prop
-- Mathlib.Analysis.Normed.Ring.Basic
/-- A ring homomorphism from a `Ring R` to a `SeminormedRing S` which induces the norm structure
`SeminormedRing.induced` makes `R` satisfy `‖(1 : R)‖ = 1` whenever `‖(1 : S)‖ = 1`.  -/
NormOneClass.induced : ∀ {F : Type u_8} (R : Type u_9) (S : Type u_10) [inst : Ring R] [inst_1 : SeminormedRing S] [NormOneClass S]
  [inst_3 : FunLike F R S] [inst_4 : RingHomClass F R S] (f : F), NormOneClass R
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey?_eq_getElem?_keysArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t.minKey? = t.keysArray[0]?
-- Mathlib.Data.Finset.Sups
Finset.biUnion_image_sdiff_right : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : GeneralizedBooleanAlgebra α] (s t : Finset α),
  (t.biUnion fun b => Finset.image (fun x => x \ b) s) = s.diffs t
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.range_lift_eq_closure : ∀ {α : Type u} {β : Type v} [inst : Group β] {f : α → β}, (FreeGroup.lift f).range = Subgroup.closure (Set.range f)
-- Mathlib.Topology.Compactness.NhdsKer
/-- **Alias** of the reverse direction of `IsCompact.nhdsKer_iff`. -/
IsCompact.nhdsKer : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsCompact s → IsCompact (nhdsKer s)
-- Lean.Meta.Sym.AlphaShareBuilder
Lean.Meta.Sym.Internal.mkProjS : {m : Type → Type} → [Lean.Meta.Sym.Internal.MonadShareCommon m] → [Monad m] → Lean.Name → ℕ → Lean.Expr → m Lean.Expr
-- Batteries.Data.Random.MersenneTwister
/-- Update the state by a number of generation steps (default 1).  -/
Batteries.Random.MersenneTwister.State.update : {cfg : Batteries.Random.MersenneTwister.Config} →
  Batteries.Random.MersenneTwister.State cfg → optParam ℕ 1 → Batteries.Random.MersenneTwister.State cfg
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Generators.cotangentSpaceBasis_repr_tmul : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type w}
  (P : Algebra.Generators R S ι) (r : S) (x : P.Ring) (i : ι),
  (P.cotangentSpaceBasis.repr (r ⊗ₜ[P.Ring] (KaehlerDifferential.D R P.Ring) x)) i =
    r * (MvPolynomial.aeval P.val) ((MvPolynomial.pderiv i) x)
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.sumCoords_self_apply : ∀ {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M) (i : ι), b.sumCoords (b i) = 1
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.Hom.ext_iff : ∀ {A B : AddMonCat} {x y : A.Hom B}, x = y ↔ x.hom' = y.hom'
-- Mathlib.Topology.WithTopology
WithTopology.image_toTopology : ∀ {X : Type u_1} (t : TopologicalSpace X) (s : Set X), WithTopology.toTopology t '' s = WithTopology.ofTopology ⁻¹' s
-- Mathlib.Topology.Bornology.Hom
/-- Copy of a `LocallyBoundedMap` with a new `toFun` equal to the old one. Useful to fix
definitional equalities.  -/
LocallyBoundedMap.copy : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Bornology α] →
      [inst_1 : Bornology β] → (f : LocallyBoundedMap α β) → (f' : α → β) → f' = ⇑f → LocallyBoundedMap α β
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.Disjoint.mul_right : ∀ {α : Type u_1} {f g h : Equiv.Perm α}, f.Disjoint g → f.Disjoint h → f.Disjoint (g * h)
-- Init.Data.Nat.Bitwise.Lemmas
/-- `testBit 1 i` is true iff the index `i` equals 0.  -/
Nat.testBit_one_eq_true_iff_self_eq_zero : ∀ {i : ℕ}, Nat.testBit 1 i = true ↔ i = 0
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Bicategory.Adjunction.instInhabitedId : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {a : B} →
      Inhabited
        (CategoryTheory.Bicategory.Adjunction (CategoryTheory.CategoryStruct.id a) (CategoryTheory.CategoryStruct.id a))
-- Mathlib.Algebra.Algebra.Operations
Submodule.mul_eq_span_mul_set : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] (s t : Submodule R A),
  s * t = Submodule.span R (↑s * ↑t)
-- Mathlib.Order.DirectedInverseSystem
/-- To define a function from the direct limit, it suffices to provide one function from each
component subject to a compatibility condition.  -/
DirectLimit.map₂ : {ι : Type u_1} →
  [inst : Preorder ι] →
    {F₁ : ι → Type u_2} →
      {F₂ : ι → Type u_3} →
        {F : ι → Type u_4} →
          {T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6} →
            (f₁ : (i j : ι) → (h : i ≤ j) → T₁ h) →
              [inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₁ h) (F₁ i) (F₁ j)] →
                [inst_2 : DirectedSystem F₁ fun x1 x2 x3 => ⇑(f₁ x1 x2 x3)] →
                  {T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7} →
                    (f₂ : (i j : ι) → (h : i ≤ j) → T₂ h) →
                      [inst_3 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₂ h) (F₂ i) (F₂ j)] →
                        [inst_4 : DirectedSystem F₂ fun x1 x2 x3 => ⇑(f₂ x1 x2 x3)] →
                          {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8} →
                            (f : (i j : ι) → (h : i ≤ j) → T h) →
                              [inst_5 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)] →
                                [inst_6 : DirectedSystem F fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
                                  [inst_7 : IsDirectedOrder ι] →
                                    (ih : (i : ι) → F₁ i → F₂ i → F i) →
                                      (∀ (i j : ι) (h : i ≤ j) (x : F₁ i) (y : F₂ i),
                                          (f i j h) (ih i x y) = ih j ((f₁ i j h) x) ((f₂ i j h) y)) →
                                        DirectLimit F₁ f₁ → DirectLimit F₂ f₂ → DirectLimit F f
-- Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
CongruenceSubgroup.Gamma0_is_congruence : ∀ (N : ℕ) [NeZero N], CongruenceSubgroup.IsCongruenceSubgroup (CongruenceSubgroup.Gamma0 N)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- Product of a multiset of elements in a `Subsemiring` of a `CommSemiring`
is in the `Subsemiring`.  -/
Subsemiring.multiset_prod_mem : ∀ {R : Type u_1} [inst : CommSemiring R] (s : Subsemiring R) (m : Multiset R), (∀ a ∈ m, a ∈ s) → m.prod ∈ s