mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.ODE.PicardLindelof
/-- `FunSpace t₀ x₀ r L` contains the constant map at `x₀`.  -/
ODE.FunSpace.instInhabited : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    {tmin tmax : ℝ} → {t₀ : ↑(Set.Icc tmin tmax)} → {x₀ : E} → {r L : NNReal} → Inhabited (ODE.FunSpace t₀ x₀ r L)
-- Batteries.Data.List.Basic
List.swap_eq_swapTR : @List.swap = @List.swapTR
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.AppImplicitArg.named.inj : ∀ {s s_1 : Lean.TSyntax `Lean.Parser.Term.namedArgument},
  Lean.PrettyPrinter.Delaborator.AppImplicitArg.named s = Lean.PrettyPrinter.Delaborator.AppImplicitArg.named s_1 →
    s = s_1
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.piCongrLeft_refl : ∀ {ι : Type u_7} {X : ι → Type u_8} [inst : (i : ι) → TopologicalSpace (X i)],
  Homeomorph.piCongrLeft (Equiv.refl ι) = Homeomorph.refl ((i : ι) → X i)
-- Init.Data.Iterators.Basic
Std.IterStep.successor.eq_1 : ∀ {α : Type u} {β : Type w} (it : α) (out : β), (Std.IterStep.yield it out).successor = some it
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.coe_ofSupportedInCLM : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F] {n : ℕ∞} [inst_6 : SMulCommClass ℝ 𝕜 F]
  {K : TopologicalSpace.Compacts E} (K_sub_Ω : ↑K ⊆ ↑Ω),
  ⇑(TestFunction.ofSupportedInCLM 𝕜 K_sub_Ω) = TestFunction.ofSupportedIn K_sub_Ω
-- Lean.Syntax
Lean.Syntax.Traverser.cur : Lean.Syntax.Traverser → Lean.Syntax
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_X : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {X : C}
  (S : J.Cover X) (f : S.Arrow), S.preOneHypercover.X f = f.Y
-- Init.Coe
/-- Coerces a value of type `α` to type `β`. Accessible by the notation `↑x`,
or by double type ascription `((x : α) : β)`.  -/
CoeHead.coe : {α : Sort u} → {β : semiOutParam (Sort v)} → [self : CoeHead α β] → α → β
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.coe_nsmul : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) (x : ↥H) (n : ℕ), ↑(n • x) = n • ↑x
-- Init.Core
/-- The loop should terminate early.

`ForInStep.done` is produced by uses of `break` or `return` in the loop body.
 -/
ForInStep.done : {α : Type u} → α → ForInStep α
-- Std.Net.Addr
Std.Net.instDecidableEqSocketAddress.decEq : (x x_1 : Std.Net.SocketAddress) → Decidable (x = x_1)
-- Lean.Expr
Lean.Expr.mkData : UInt64 →
  optParam ℕ 0 →
    optParam UInt32 0 →
      optParam Bool false → optParam Bool false → optParam Bool false → optParam Bool false → Lean.Expr.Data
-- Init.Data.List.Lemmas
List.insert_replicate_ne : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {n : ℕ} {a b : α},
  (!b == a) = true → List.insert b (List.replicate n a) = b :: List.replicate n a
-- Mathlib.GroupTheory.GroupAction.Quotient
/-- A bijection between the quotient of the action of a subgroup `H` on an orbit, and a
corresponding quotient expressed in terms of `Setoid.comap Subtype.val`.  -/
MulAction.equivSubgroupOrbitsSetoidComap : {G : Type u} →
  {X : Type v} →
    [inst : Group G] →
      [inst_1 : MulAction G X] →
        (H : Subgroup G) →
          (ω : Quotient (MulAction.orbitRel G X)) →
            MulAction.orbitRel.Quotient ↥H ↑(MulAction.orbitRel.Quotient.orbit ω) ≃
              Quotient (Setoid.comap Subtype.val (MulAction.orbitRel (↥H) X))
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.LawfulBackwardPattern.endsWith_eq : ∀ {ρ : Type} {pat : ρ} {inst : String.Slice.Pattern.BackwardPattern pat}
  [self : String.Slice.Pattern.LawfulBackwardPattern pat] (s : String.Slice),
  String.Slice.Pattern.BackwardPattern.endsWith pat s = (String.Slice.Pattern.BackwardPattern.skipSuffix? pat s).isSome
-- Mathlib.Data.Int.GCD
/-- **Bézout's lemma**: given `x y : ℕ`, `gcd x y = x * a + y * b`, where `a = gcd_a x y` and
`b = gcd_b x y` are computed by the extended Euclidean algorithm.
 -/
Nat.gcd_eq_gcd_ab : ∀ (x y : ℕ), ↑(x.gcd y) = ↑x * x.gcdA y + ↑y * x.gcdB y
-- Mathlib.RingTheory.Polynomial.Basic
Polynomial.eval₂_restriction : ∀ {R : Type u} {S : Type u_1} [inst : Ring R] [inst_1 : Semiring S] {f : R →+* S} {x : S} {p : Polynomial R},
  Polynomial.eval₂ f x p = Polynomial.eval₂ (f.comp (Subring.closure ↑p.coeffs).subtype) x p.restriction
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.IsSingular.isSuccLimit_of_aleph : ∀ {o : Ordinal.{u_1}}, (Cardinal.aleph o).IsSingular → Order.IsSuccLimit o
-- Mathlib.NumberTheory.LSeries.DirichletContinuation
/-- Relation between the completed L-function and the usual one. We state it this way around so
it holds at the poles of the gamma factor as well.
 -/
DirichletCharacter.LFunction_eq_completed_div_gammaFactor : ∀ {N : ℕ} [inst : NeZero N] (χ : DirichletCharacter ℂ N) (s : ℂ),
  s ≠ 0 ∨ N ≠ 1 → DirichletCharacter.LFunction χ s = DirichletCharacter.completedLFunction χ s / χ.gammaFactor s
-- Mathlib.Topology.Connected.PathConnected
JoinedIn.trans : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y z : X} {F : Set X}, JoinedIn F x y → JoinedIn F y z → JoinedIn F x z
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Λ'.push.inj : ∀ {k : Turing.PartrecToTM2.K'} {s : Option Turing.PartrecToTM2.Γ' → Option Turing.PartrecToTM2.Γ'}
  {q : Turing.PartrecToTM2.Λ'} {k_1 : Turing.PartrecToTM2.K'}
  {s_1 : Option Turing.PartrecToTM2.Γ' → Option Turing.PartrecToTM2.Γ'} {q_1 : Turing.PartrecToTM2.Λ'},
  Turing.PartrecToTM2.Λ'.push k s q = Turing.PartrecToTM2.Λ'.push k_1 s_1 q_1 → k = k_1 ∧ s = s_1 ∧ q = q_1
-- Mathlib.Algebra.Order.Interval.Set.Group
Set.sub_mem_Ioc_zero_iff_right : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {a b : α},
  b - a ∈ Set.Ioc 0 b ↔ a ∈ Set.Ico 0 b
-- Mathlib.AlgebraicGeometry.Geometrically.Reduced
AlgebraicGeometry.instIsStableUnderBaseChangeSchemeGeometricallyReduced : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.GeometricallyReduced
-- Mathlib.Data.Finset.Fin
Finset.attachFin.congr_simp : ∀ (s s_1 : Finset ℕ) (e_s : s = s_1) {n : ℕ} (h : ∀ m ∈ s, m < n), s.attachFin h = s_1.attachFin ⋯
-- Mathlib.Analysis.CStarAlgebra.Basic
IsStarProjection.norm_le : ∀ {E : Type u_2} [inst : NonUnitalNormedRing E] [inst_1 : StarRing E] [CStarRing E] (e : E),
  IsStarProjection e → ‖e‖ ≤ 1
-- Batteries.Data.Float.Lemmas
/-- This theorem is true for all types but most other types have `LawfulBEq` where
`bne_self_eq_false` or `bne_iff_ne` apply.
 -/
Float32.bne_eq : ∀ {f : Float32}, (f != f) = !f == f
-- Mathlib.Algebra.Group.Defs
mul_ne_mul_right : ∀ {G : Type u_1} [inst : Mul G] [IsLeftCancelMul G] (a : G) {b c : G}, a * b ≠ a * c ↔ b ≠ c
-- Init.Data.Iterators.Consumers.Monadic.Partial
Std.IterM.Partial.mk.inj : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} {it it_1 : Std.IterM m β}, { it := it } = { it := it_1 } → it = it_1
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.zeroLocus_anti_mono : ∀ {R : Type u} [inst : CommSemiring R] {s t : Set R}, s ⊆ t → PrimeSpectrum.zeroLocus t ⊆ PrimeSpectrum.zeroLocus s
-- Mathlib.Algebra.Homology.Factorizations.CM5b
CochainComplex.cm5b.instMonoFIntI : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.EnoughInjectives C] {K L : CochainComplex C ℤ} (f : K ⟶ L) (n : ℤ),
  CategoryTheory.Mono ((CochainComplex.cm5b.i f).f n)
-- Lean.Message
Lean.TraceResult.error.sizeOf_spec : sizeOf Lean.TraceResult.error = 1
-- Init.Data.String.Lemmas.Pattern.Split.Basic
_private.Init.Data.String.Lemmas.Pattern.Split.Basic.0.String.Slice.Pattern.Model.splitFromSteps.eq_1 : ∀ {s : String.Slice} (currPos : s.Pos), String.Slice.Pattern.Model.splitFromSteps✝ currPos [] = [s.subsliceFrom currPos]
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
SimpleGraph.Walk.getElem_edges : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} {i : ℕ} (h : i < p.edges.length),
  p.edges[i] = s(p.getVert i, p.getVert (i + 1))
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.AffineTargetMorphismProperty.ext : ∀ {P Q : AlgebraicGeometry.AffineTargetMorphismProperty},
  (∀ ⦃X Y : AlgebraicGeometry.Scheme⦄ (f : X ⟶ Y) [inst : AlgebraicGeometry.IsAffine Y], P f ↔ Q f) → P = Q
-- Mathlib.Topology.OpenPartialHomeomorph.Continuity
OpenPartialHomeomorph.eventually_nhds : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {x : X} (p : Y → Prop),
  x ∈ e.source → ((∀ᶠ (y : Y) in nhds (↑e x), p y) ↔ ∀ᶠ (x : X) in nhds x, p (↑e x))
-- Mathlib.Topology.NhdsSet
/-- **Alias** of the forward direction of `nhdsSet_neBot_iff`. -/
Set.Nonempty.nhdsSet_neBot : ∀ {α : Type u_4} [inst : TopologicalSpace α] {s : Set α}, (nhdsSet s).NeBot → s.Nonempty
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey!_le_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α}, t.contains k = true → (cmp t.minKey! k).isLE = true
-- Mathlib.Topology.UnitInterval
unitInterval.one_minus_le_one : ∀ (x : ↑unitInterval), 1 - ↑x ≤ 1
-- Mathlib.Algebra.BigOperators.Finprod
map_finsetSum : ∀ {M : Type u_5} {N : Type u_6} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] {α : Type u_7} {F : Type u_8}
  [inst_2 : Fintype α] [inst_3 : EquivLike F M N] [AddEquivClass F M N] (f : F) (g : α → M), f (∑ i, g i) = ∑ i, f (g i)
-- Mathlib.CategoryTheory.Monad.Products
CategoryTheory.coprodMonad_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C]
  {x x_1 : C} (g : x ⟶ x_1),
  (CategoryTheory.coprodMonad X).map g = CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id X) g
-- Mathlib.CategoryTheory.Bicategory.Span.Basic
CategoryTheory.Span.Hom.hom_l : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {Wₗ Wᵣ : CategoryTheory.MorphismProperty C} {c c' : C}
  {S₁ S₂ : CategoryTheory.Span Wₗ Wᵣ c c'} (self : S₁.Hom S₂), CategoryTheory.CategoryStruct.comp self.hom S₂.l = S₁.l
-- Mathlib.Data.Int.Cast.Lemmas
/-- Monoid homomorphisms from `Multiplicative ℤ` are defined by the image
of `Multiplicative.ofAdd 1`.  -/
zpowersHom : (α : Type u_3) → [inst : Group α] → α ≃ (Multiplicative ℤ →* α)
-- Mathlib.Data.Set.Image
Set.range_quotient_mk : ∀ {α : Type u_1} {s : Setoid α}, Set.range (Quotient.mk s) = Set.univ
-- Init.Data.Option.Attach
_private.Init.Data.Option.Attach.0.OptionT.instMonadAttach.match_1.eq_1 : ∀ {m : Type u_1 → Type u_2} [inst : MonadAttach m] {α : Type u_1} (x : OptionT m α)
  (motive : Subtype (MonadAttach.CanReturn x.run) → Sort u_3) (a : α) (h : MonadAttach.CanReturn x.run (some a))
  (h_1 : (a : α) → (h : MonadAttach.CanReturn x.run (some a)) → motive ⟨some a, h⟩)
  (h_2 : (property : MonadAttach.CanReturn x.run none) → motive ⟨none, property⟩),
  (match ⟨some a, h⟩ with
    | ⟨some a, h⟩ => h_1 a h
    | ⟨none, property⟩ => h_2 property) =
    h_1 a h
-- Mathlib.Algebra.Order.Ring.Synonym
Lex.instDistrib : {R : Type u_1} → [Distrib R] → Distrib (Lex R)
-- Mathlib.Topology.Algebra.WithZeroTopology
/-- The topology on a linearly ordered group with zero element adjoined makes it a topological
monoid.  -/
WithZeroTopology.instContinuousMul : ∀ {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀], ContinuousMul Γ₀
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.tendsto_finsetProd_of_ne_top : ∀ {α : Type u_1} {ι : Type u_4} {f : ι → α → ENNReal} {x : Filter α} {a : ι → ENNReal} (s : Finset ι),
  (∀ i ∈ s, Filter.Tendsto (f i) x (nhds (a i))) →
    (∀ i ∈ s, a i ≠ ⊤) → Filter.Tendsto (fun b => ∏ c ∈ s, f c b) x (nhds (∏ c ∈ s, a c))
-- Mathlib.Analysis.Meromorphic.Basic
/-- Finite sums of meromorphic functions are meromorphic.  -/
MeromorphicAt.fun_sum : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {ι : Type u_5} {s : Finset ι} {G : ι → 𝕜 → E} {x : 𝕜},
  (∀ σ ∈ s, MeromorphicAt (G σ) x) → MeromorphicAt (fun z => ∑ n ∈ s, G n z) x
-- Mathlib.Algebra.Lie.Subalgebra
/-- The set of Lie subalgebras of a Lie algebra form a complete lattice.

We provide explicit values for the fields `bot`, `top`, `inf` to get more convenient definitions
than we would otherwise obtain from `completeLatticeOfInf`.  -/
LieSubalgebra.completeLattice : {R : Type u} →
  {L : Type v} →
    [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → CompleteLattice (LieSubalgebra R L)
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Roo.toList_iter_eq_toList : ∀ {α : Type u_1} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [inst_4 : Std.Rxo.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Roo α}, r.iter.toList = r.toList
-- Mathlib.Analysis.Calculus.TangentCone.Basic
/-- Intersecting with a neighborhood of the point does not change the tangent cone.  -/
tangentConeAt_inter_nhds : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : AddCommGroup E] [inst_1 : SMul 𝕜 E] [inst_2 : TopologicalSpace E] {s t : Set E}
  {x : E} [ContinuousAdd E], t ∈ nhds x → tangentConeAt 𝕜 (s ∩ t) x = tangentConeAt 𝕜 s x
-- Mathlib.Data.Nat.Squarefree
Nat.minSqFacAux_has_prop : ∀ {n : ℕ} (k : ℕ),
  0 < n → ∀ (i : ℕ), k = 2 * i + 3 → (∀ (m : ℕ), Nat.Prime m → m ∣ n → k ≤ m) → n.MinSqFacProp (n.minSqFacAux k)
-- Mathlib.Algebra.Group.Hom.Defs
instInhabitedZeroHom : {M : Type u_4} → {N : Type u_5} → [inst : Zero M] → [inst_1 : Zero N] → Inhabited (ZeroHom M N)
-- Std.Data.ExtHashMap.Lemmas
_private.Std.Data.ExtHashMap.Lemmas.0.GetElem?.match_1.eq_1 : ∀ (elem : outParam (Type u_1)) (motive : Option elem → Sort u_2) (e : elem) (h_1 : (e : elem) → motive (some e))
  (h_2 : Unit → motive none),
  (match some e with
    | some e => h_1 e
    | none => h_2 ()) =
    h_1 e
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey?_inter_of_not_mem_right : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∉ m₂ → (m₁ ∩ m₂).getKey? k = none
-- Mathlib.Topology.EMetricSpace.Defs
/-- Given `f : β → ℝ≥0∞`, if `f` sends `{i | p i}` to a set of positive numbers
accumulating to zero, then `f i`-neighborhoods of the diagonal form a basis of `𝓤 α`.

For specific bases see `uniformity_basis_edist`, `uniformity_basis_edist'`,
`uniformity_basis_edist_nnreal`, and `uniformity_basis_edist_inv_nat`.  -/
EMetric.mk_uniformity_basis : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {β : Type u_2} {p : β → Prop} {f : β → ENNReal},
  (∀ (x : β), p x → 0 < f x) →
    (∀ (ε : ENNReal), 0 < ε → ∃ x, p x ∧ f x ≤ ε) → (uniformity α).HasBasis p fun x => {p | edist p.1 p.2 < f x}
-- Mathlib.Algebra.Order.Group.Synonym
toLex_zero : ∀ {α : Type u_1} [inst : Zero α], toLex 0 = 0
-- Lean.CoreM
/-- Returns `true` if the given message kind has not been reported in the message log,
and then mark it as logged. Otherwise, returns `false`.
We use this API to ensure we don't log the same kind of warning multiple times.
 -/
Lean.logMessageKind : Lean.Name → Lean.CoreM Bool
-- Mathlib.RingTheory.TensorProduct.MonoidAlgebra
AddMonoidAlgebra.rTensorEquivAlgEquiv.invFun_tmul : ∀ (R : Type u_1) {M : Type u_2} {S : Type u_4} (A : Type u_5) (B : Type u_6) [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : CommSemiring A] [inst_3 : CommSemiring B] [inst_4 : Algebra R S]
  [inst_5 : Algebra R A] [inst_6 : Algebra R B] [inst_7 : Algebra S A] [inst_8 : IsScalarTower R S A]
  [inst_9 : AddCommMonoid M] (a : A) (m : M) (b : B),
  AddMonoidAlgebra.rTensorEquivAlgEquiv.invFun (AddMonoidAlgebra.single m (a ⊗ₜ[R] b)) =
    a ⊗ₜ[R] AddMonoidAlgebra.single m b
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.denom_one : ∀ (z : UpperHalfPlane), UpperHalfPlane.denom 1 ↑z = 1
-- Mathlib.Order.OmegaCompletePartialOrder
Prod.ωScottContinuous.prodMk : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : OmegaCompletePartialOrder α]
  [inst_1 : OmegaCompletePartialOrder β] [inst_2 : OmegaCompletePartialOrder γ] {f : α → β},
  OmegaCompletePartialOrder.ωScottContinuous f →
    ∀ {g : α → γ},
      OmegaCompletePartialOrder.ωScottContinuous g → OmegaCompletePartialOrder.ωScottContinuous fun x => (f x, g x)
-- Mathlib.Data.Multiset.Pi
Multiset.Pi.cons_eta : ∀ {α : Type u_1} [inst : DecidableEq α] {δ : α → Sort u_2} {m : Multiset α} {a : α}
  (f : (a' : α) → a' ∈ a ::ₘ m → δ a'), (Multiset.Pi.cons m a (f a ⋯) fun a' ha' => f a' ⋯) = f
-- Init.Data.Array.Lemmas
Array.getElem?_reverse : ∀ {α : Type u_1} {xs : Array α} {i : ℕ}, i < xs.size → xs.reverse[i]? = xs[xs.size - 1 - i]?
-- Mathlib.Algebra.Group.Subsemigroup.Basic
/-- An induction principle for additive closure membership for
predicates with two arguments.  -/
AddSubsemigroup.closure_induction₂ : ∀ {M : Type u_1} [inst : Add M] {s : Set M}
  {p : (x y : M) → x ∈ AddSubsemigroup.closure s → y ∈ AddSubsemigroup.closure s → Prop},
  (∀ (x y : M) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯) →
    (∀ (x y z : M) (hx : x ∈ AddSubsemigroup.closure s) (hy : y ∈ AddSubsemigroup.closure s)
        (hz : z ∈ AddSubsemigroup.closure s), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz) →
      (∀ (x y z : M) (hx : x ∈ AddSubsemigroup.closure s) (hy : y ∈ AddSubsemigroup.closure s)
          (hz : z ∈ AddSubsemigroup.closure s), p z x hz hx → p z y hz hy → p z (x + y) hz ⋯) →
        ∀ {x y : M} (hx : x ∈ AddSubsemigroup.closure s) (hy : y ∈ AddSubsemigroup.closure s), p x y hx hy
-- Mathlib.Analysis.Convex.Basic
MonotoneOn.convex_gt : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LinearOrder E] [IsOrderedAddMonoid E] [inst_5 : PartialOrder β] [inst_6 : Module 𝕜 E] [PosSMulMono 𝕜 E]
  {s : Set E} {f : E → β}, MonotoneOn f s → Convex 𝕜 s → ∀ (r : β), Convex 𝕜 {x | x ∈ s ∧ r < f x}
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Iso.apply_mem_neighborSet_iff : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') {v w : V},
  f w ∈ G'.neighborSet (f v) ↔ w ∈ G.neighborSet v
-- Mathlib.Data.PFunctor.Multivariate.M
/-- Using corecursion, construct the contents of an M-type  -/
MvPFunctor.M.corecContents : {n : ℕ} →
  (P : MvPFunctor.{u} (n + 1)) →
    {α : TypeVec.{u} n} →
      {β : Type v} →
        (g₀ : β → P.A) →
          ((b : β) → (P.drop.B (g₀ b)).Arrow α) →
            (g₂ : (b : β) → P.last.B (g₀ b) → β) →
              (x : P.last.M) → (b : β) → x = MvPFunctor.M.corecShape P g₀ g₂ b → TypeVec.Arrow (MvPFunctor.M.Path P x) α
-- Lean.Data.Lsp.Internal
Lean.Lsp.instToJsonDecls : Lean.ToJson Lean.Lsp.Decls
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.IsAddModHom.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  {M' N' : D} {A : C} [inst_4 : CategoryTheory.AddMonObj A] [inst_5 : CategoryTheory.AddModObj A M']
  [inst_6 : CategoryTheory.AddModObj A N'] {f : M' ⟶ N'},
  autoParam
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddModObj.vadd f =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f)
          CategoryTheory.AddModObj.vadd)
      CategoryTheory.IsAddModHom.vadd_hom._autoParam →
    CategoryTheory.IsAddModHom A f
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroup.mul : {R : Type u} → Rack.PreEnvelGroup R → Rack.PreEnvelGroup R → Rack.PreEnvelGroup R
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.compl₁₂_comp_right : ∀ {R₁ : Type u_3} {R₂ : Type u_4} [inst : Semiring R₁] [inst_1 : Semiring R₂] {Mₗ : Type u_6} {N : Type u_7}
  {Pₗ : Type u_9} {Qₗ : Type u_10} {Qₗ' : Type u_11} [inst_2 : AddCommMonoid Mₗ] [inst_3 : AddCommMonoid N]
  [inst_4 : AddCommMonoid Pₗ] [inst_5 : AddCommMonoid Qₗ] [inst_6 : AddCommMonoid Qₗ'] [inst_7 : Module R₁ Mₗ]
  [inst_8 : Module R₂ N] [inst_9 : Module R₂ Pₗ] [inst_10 : Module R₁ Pₗ] [inst_11 : Module R₁ Qₗ]
  [inst_12 : Module R₂ Qₗ'] {Tₗ' : Type u_13} [inst_13 : AddCommMonoid Tₗ'] [inst_14 : Module R₂ Tₗ']
  [inst_15 : SMulCommClass R₂ R₁ Pₗ] (f : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ) (g : Qₗ →ₗ[R₁] Mₗ) (g' : Qₗ' →ₗ[R₂] N)
  (h' : Tₗ' →ₗ[R₂] Qₗ'), f.compl₁₂ g (g' ∘ₗ h') = (f.compl₁₂ g g').compl₂ h'
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.coeFn_mk : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (hμ : MeasureTheory.IsProbabilityMeasure μ),
  ⇑⟨μ, hμ⟩ = fun s => (μ s).toNNReal
-- Mathlib.Algebra.Homology.SpectralObject.FirstPage
CategoryTheory.Abelian.SpectralObject.spectralSequenceFirstPageXIso_hom_assoc : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{u_4, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  [inst_3 : data.HasFirstPageComputation] [inst_4 : X.HasSpectralSequence data] (pq : κ) (i₁ i₂ : ι)
  (hi₁ : i₁ = data.i₁ pq) (hi₂ : i₂ = data.i₂ pq) (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.spectralSequenceFirstPageXIso_hom._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.spectralSequenceFirstPageXIso_hom._auto_3)
  {Z : C} (h : (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE ⋯)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.spectralSequenceFirstPageXIso data pq i₁ i₂ hi₁ hi₂ n₁ hn₁').hom h =
    CategoryTheory.CategoryStruct.comp
      (X.spectralSequencePageXIso data r₀ ⋯ pq i₁ i₁ i₂ i₂ ⋯ hi₁ hi₂ ⋯ n₀ n₁ n₂ hn₁' ⋯ ⋯).hom
      (CategoryTheory.CategoryStruct.comp (X.EIsoH (CategoryTheory.homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂).hom h)
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.measure_Ioi : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (f : StieltjesFunction R)
  [inst_2 : OrderTopology R] [inst_3 : CompactIccSpace R] [inst_4 : MeasurableSpace R] [inst_5 : BorelSpace R]
  [inst_6 : SecondCountableTopology R] [inst_7 : DenselyOrdered R] {l : ℝ},
  Filter.Tendsto (↑f) Filter.atTop (nhds l) → ∀ (x : R), f.measure (Set.Ioi x) = ENNReal.ofReal (l - ↑f x)
-- Mathlib.Data.Nat.Choose.Sum
Nat.sum_range_multichoose : ∀ (n k : ℕ), ∑ i ∈ Finset.range (n + 1), k.multichoose i = (n + k).choose k
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.norm_eq_zpow_neg_valuation : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {x : ℤ_[p]}, x ≠ 0 → ‖x‖ = ↑p ^ (-↑x.valuation)
-- Mathlib.Topology.Sheaves.Module
/-- `sheafOfModulesEquivOver` takes `R.over U` to `R |_ U`.  -/
TopologicalSpace.Opens.sheafOfModulesEquivOverUnit : {X : TopCat} →
  (U : TopologicalSpace.Opens ↑X) →
    (R : TopCat.Sheaf RingCat X) →
      (U.sheafOfModulesEquivOver R).functor.obj (SheafOfModules.unit (CategoryTheory.Sheaf.over R U)) ≅
        SheafOfModules.unit (U.sheafRestrict.obj R)
-- Lean.Server.GoTo
Lean.Server.locationLinksFromDelabTermInfo : Lean.Elab.DelabTermInfo → Lean.Server.GoToM (Array Lean.Lsp.LeanLocationLink)
-- Init.Data.Int.Order
Int.add_le_add : ∀ {a b c d : ℤ}, a ≤ b → c ≤ d → a + c ≤ b + d
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.reflexivePair.compRightIso_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {A B : C} (f g : A ⟶ B) (s : B ⟶ A) (sl : CategoryTheory.CategoryStruct.comp s f = CategoryTheory.CategoryStruct.id B)
  (sr : CategoryTheory.CategoryStruct.comp s g = CategoryTheory.CategoryStruct.id B) (F : CategoryTheory.Functor C D)
  (x : CategoryTheory.Limits.WalkingReflexivePair),
  (CategoryTheory.Limits.reflexivePair.compRightIso f g s sl sr F).hom.app x =
    match x with
    | CategoryTheory.Limits.WalkingReflexivePair.zero => CategoryTheory.CategoryStruct.id (F.obj B)
    | CategoryTheory.Limits.WalkingReflexivePair.one => CategoryTheory.CategoryStruct.id (F.obj A)