mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Order.IntermediateValue
/-- A "continuous induction principle" for a closed interval: if a set `s` meets `[a, b]`
on a closed subset, contains `a`, and for any `x ∈ [a, b)` such that `[a, x]` is included in `s`,
the set `s` includes some open neighborhood of `x` within `(x, +∞)`, then `[a, b] ⊆ s`.  -/
IsClosed.Icc_subset_of_forall_mem_nhdsGT_of_Icc_subset : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {a b : α} {s : Set α},
  IsClosed (s ∩ Set.Icc a b) →
    a ∈ s → (∀ t ∈ Set.Ico a b, Set.Icc a t ⊆ s → s ∈ nhdsWithin t (Set.Ioi t)) → Set.Icc a b ⊆ s
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsCycle.snd_ne_penultimate : ∀ {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u}, p.IsCycle → p.snd ≠ p.penultimate
-- Init.Data.AC
Lean.Data.AC.Context.evalList_mergeIdem : ∀ {α : Sort u_1} (ctx : Lean.Data.AC.Context α),
  Lean.Data.AC.ContextInformation.isIdem ctx = true →
    ∀ (e : List ℕ), Lean.Data.AC.evalList α ctx (Lean.Data.AC.mergeIdem e) = Lean.Data.AC.evalList α ctx e
-- Lean.Attributes
Lean.ParametricAttribute.mk.inj : ∀ {α : Type} {attr : Lean.AttributeImpl}
  {ext : Lean.PersistentEnvExtension (Lean.Name × α) (Lean.Name × α) (List Lean.Name × Lean.NameMap α)}
  {preserveOrder : Bool} {attr_1 : Lean.AttributeImpl}
  {ext_1 : Lean.PersistentEnvExtension (Lean.Name × α) (Lean.Name × α) (List Lean.Name × Lean.NameMap α)}
  {preserveOrder_1 : Bool},
  { attr := attr, ext := ext, preserveOrder := preserveOrder } =
      { attr := attr_1, ext := ext_1, preserveOrder := preserveOrder_1 } →
    attr = attr_1 ∧ ext = ext_1 ∧ preserveOrder = preserveOrder_1
-- Mathlib.GroupTheory.GroupAction.Quotient
AddAction.selfEquivOrbitsQuotientProd'.eq_1 : ∀ {G : Type u} {X : Type v} [inst : AddGroup G] [inst_1 : AddAction G X] {φ : Quotient (AddAction.orbitRel G X) → X}
  (hφ : Function.LeftInverse Quotient.mk'' φ) (h : ∀ (b : X), AddAction.stabilizer G b = ⊥),
  AddAction.selfEquivOrbitsQuotientProd' hφ h =
    (AddAction.selfEquivSigmaOrbitsQuotientStabilizer' G X hφ).trans
      ((Equiv.sigmaCongrRight fun x =>
            (AddSubgroup.quotientEquivOfEq ⋯).trans (QuotientAddGroup.quotientEquivSelf G)).trans
        (Equiv.sigmaEquivProd (Quotient (AddAction.orbitRel G X)) G))
-- Lean.Meta.TryThis
/-- Holds a `suggestion` for replacement, along with `preInfo` and `postInfo` strings to be printed
immediately before and after that suggestion, respectively. It also includes an optional
`MessageData` to represent the suggestion in logs; by default, this is `none`, and `suggestion` is
used.  -/
Lean.Meta.Tactic.TryThis.Suggestion : Type
-- Mathlib.Tactic.Linter.FlexibleLinter
/-- By default, if a `SyntaxNodeKind` is not special-cased here, then the linter assumes that
the tactic will use the goal as well: this heuristic works well with `exact`, `refine`, `apply`.
For tactics such as `cases` this is not true: for these tactics, `usesGoal?` yields `false`.  -/
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.usesGoal? : Lean.SyntaxNodeKind → Bool
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_17.eq_3 : ∀ (motive : (w : ℕ) → Std.Tactic.BVDecide.BVExpr w → Sort u_1) (w : ℕ) (lhsExpr : Std.Tactic.BVDecide.BVExpr w)
  (op : Std.Tactic.BVDecide.BVBinOp) (rhsExpr : Std.Tactic.BVDecide.BVExpr w)
  (h_1 : (w a : ℕ) → motive w (Std.Tactic.BVDecide.BVExpr.var a))
  (h_2 : (w : ℕ) → (val : BitVec w) → motive w (Std.Tactic.BVDecide.BVExpr.const val))
  (h_3 :
    (w : ℕ) →
      (lhsExpr : Std.Tactic.BVDecide.BVExpr w) →
        (op : Std.Tactic.BVDecide.BVBinOp) →
          (rhsExpr : Std.Tactic.BVDecide.BVExpr w) → motive w (lhsExpr.bin op rhsExpr))
  (h_4 :
    (w : ℕ) →
      (op : Std.Tactic.BVDecide.BVUnOp) →
        (expr : Std.Tactic.BVDecide.BVExpr w) → motive w (Std.Tactic.BVDecide.BVExpr.un op expr))
  (h_5 :
    (w l r : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr l) →
        (rhs : Std.Tactic.BVDecide.BVExpr r) → (h : w = l + r) → motive w (lhs.append rhs h))
  (h_6 :
    (w w_1 n : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w_1) →
        (h : w = w_1 * n) → motive w (Std.Tactic.BVDecide.BVExpr.replicate n expr h))
  (h_7 :
    (len w start : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w) → motive len (Std.Tactic.BVDecide.BVExpr.extract start len expr))
  (h_8 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftLeft rhs))
  (h_9 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftRight rhs))
  (h_10 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.arithShiftRight rhs)),
  (match w, lhsExpr.bin op rhsExpr with
    | w, Std.Tactic.BVDecide.BVExpr.var a => h_1 w a
    | w, Std.Tactic.BVDecide.BVExpr.const val => h_2 w val
    | w, lhsExpr.bin op rhsExpr => h_3 w lhsExpr op rhsExpr
    | w, Std.Tactic.BVDecide.BVExpr.un op expr => h_4 w op expr
    | w, lhs.append rhs h => h_5 w l r lhs rhs h
    | w, Std.Tactic.BVDecide.BVExpr.replicate n expr h => h_6 w w_1 n expr h
    | len, Std.Tactic.BVDecide.BVExpr.extract start .(len) expr => h_7 len w start expr
    | w, lhs.shiftLeft rhs => h_8 w n lhs rhs
    | w, lhs.shiftRight rhs => h_9 w n lhs rhs
    | w, lhs.arithShiftRight rhs => h_10 w n lhs rhs) =
    h_3 w lhsExpr op rhsExpr
-- Mathlib.Analysis.MeanInequalitiesPow
/-- Weighted generalized mean inequality, version sums over finite sets, with `ℝ≥0`-valued
functions and natural exponent.  -/
NNReal.pow_arith_mean_le_arith_mean_pow : ∀ {ι : Type u} (s : Finset ι) (w z : ι → NNReal),
  ∑ i ∈ s, w i = 1 → ∀ (n : ℕ), (∑ i ∈ s, w i * z i) ^ n ≤ ∑ i ∈ s, w i * z i ^ n
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.lintegral_one : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}, ∫⁻ (x : α), 1 ∂μ = μ Set.univ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_inter_of_contains_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h₁ : m₁.WF),
  m₂.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k m₂ = true → (m₁.inter m₂ ⋯).get? k = m₁.get? k
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
/-- A unique factorization domain with at least one irreducible element
in which all irreducible elements are associated
is a discrete valuation ring.
 -/
IsDiscreteValuationRing.of_ufd_of_unique_irreducible : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] [UniqueFactorizationMonoid R],
  (∃ p, Irreducible p) → (∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q) → IsDiscreteValuationRing R
-- Mathlib.Data.Nat.Nth
Nat.nth_injOn : ∀ {p : ℕ → Prop} (hf : (Set.ofPred p).Finite), Set.InjOn (Nat.nth p) (Set.Iio hf.toFinset.card)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- **Alias** of `MulHom.domRestrict_apply`. -/
MulHom.restrict_apply : ∀ {M : Type u_1} {σ : Type u_4} [inst : Mul M] {N : Type u_5} [inst_1 : Mul N] [inst_2 : SetLike σ M]
  [inst_3 : MulMemClass σ M] (f : M →ₙ* N) {S : σ} (x : ↥S), (f.domRestrict S) x = f ↑x
-- Mathlib.Algebra.Polynomial.Roots
/-- A polynomial `p` that has as many roots as its degree
can be written `p = p.leadingCoeff * ∏(X - a)`, for `a` in `p.roots`.  -/
Polynomial.C_leadingCoeff_mul_prod_multiset_X_sub_C : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] {p : Polynomial R},
  p.roots.card = p.natDegree →
    Polynomial.C p.leadingCoeff * (Multiset.map (fun a => Polynomial.X - Polynomial.C a) p.roots).prod = p
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- The diagram
```
      U ---------m----------> X
      |                       |
    χ₀ U                     χ m
      |                       |
      v                       v
      Ω₀ ------truth--------> Ω
```
commutes.
 -/
CategoryTheory.HasSubobjectClassifier.comm_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasSubobjectClassifier C] {U X : C}
  (m : U ⟶ X) [inst_2 : CategoryTheory.Mono m] {Z : C} (h : CategoryTheory.HasSubobjectClassifier.Ω C ⟶ Z),
  CategoryTheory.CategoryStruct.comp m
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.HasSubobjectClassifier.χ m) h) =
    CategoryTheory.CategoryStruct.comp (⋯.some.χ₀ U)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.HasSubobjectClassifier.truth C) h)
-- Mathlib.Order.Monotone.Monovary
MonovaryOn.comp_monotone_on_left : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : Preorder α] [inst_1 : Preorder β]
  [inst_2 : Preorder γ] {f : ι → α} {f' : α → γ} {g : ι → β} {s : Set ι},
  MonovaryOn f g s → Monotone f' → MonovaryOn (f' ∘ f) g s
-- Init.Data.List.Lemmas
/-- Variant of `getElem_append_left` useful for rewriting from the small list to the big list.  -/
List.getElem_append_left' : ∀ {α : Type u_1} {l₁ : List α} {i : ℕ} (hi : i < l₁.length) (l₂ : List α), l₁[i] = (l₁ ++ l₂)[i]
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- The intersection of the translates of a *finite* subset which contain a given point
is a block (Wielandt, th. 7.3).  -/
AddAction.IsBlock.of_subset : ∀ {G : Type u_1} [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] [AddAction.IsPretransitive G X] {B : Set X}
  (a : X), B.Finite → AddAction.IsBlock G (⋂ k, ⋂ (_ : a ∈ k +ᵥ B), k +ᵥ B)
-- Mathlib.Order.Hom.BoundedLattice
SupBotHomClass.toSupHomClass : ∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} {inst : Max α} {inst_1 : Max β} {inst_2 : Bot α} {inst_3 : Bot β}
  {inst_4 : FunLike F α β} [self : SupBotHomClass F α β], SupHomClass F α β
-- Init.System.IO
/-- Replaces the standard input stream of the current thread and returns its previous value.

Use `IO.getStdin` to get the current standard input stream.
 -/
IO.setStdin : IO.FS.Stream → BaseIO IO.FS.Stream
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
SSet.Truncated.HomotopyCategory.BinaryProduct.associativity'Iso_hom_app : ∀ {X Y Z : SSet.Truncated 2} (xyz : X.HomotopyCategory × Y.HomotopyCategory × Z.HomotopyCategory),
  (SSet.Truncated.HomotopyCategory.BinaryProduct.associativity'Iso X Y Z).hom.app xyz =
    CategoryTheory.CategoryStruct.id
      (((CategoryTheory.prod.associativity X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory).inverse.comp
            (((SSet.Truncated.HomotopyCategory.BinaryProduct.inverse X Y).prod
                  (CategoryTheory.Functor.id Z.HomotopyCategory)).comp
              ((SSet.Truncated.HomotopyCategory.BinaryProduct.inverse
                    (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).comp
                (SSet.Truncated.mapHomotopyCategory (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)))).obj
        xyz)
-- Mathlib.Order.CompleteLattice.Defs
sInf_le_sInf : ∀ {α : Type u_1} [inst : CompleteSemilatticeInf α] {s t : Set α}, s ⊆ t → sInf t ≤ sInf s
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Path.zoom_insert : ∀ {α : Type u_1} {c : RBTree.RBColor} {n : ℕ} {cmp : α → α → Ordering} {t' : RBTree.RBNode α} {v : α}
  {path : RBTree.RBNode.Path α} {t : RBTree.RBNode α},
  t.Balanced c n →
    RBTree.RBNode.zoom (cmp v) t = (t', path) → (path.insert t' v).setBlack = (RBTree.RBNode.insert cmp t v).setBlack
-- Mathlib.Topology.Compactness.Compact
Filter.hasBasis_coclosedCompact : ∀ {X : Type u} [inst : TopologicalSpace X],
  (Filter.coclosedCompact X).HasBasis (fun s => IsClosed s ∧ IsCompact s) compl
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- **Alias** of `Fintype.prod_bijective`.

---

`Fintype.prod_bijective` is a variant of `Finset.prod_bij` that accepts `Function.Bijective`.

See `Function.Bijective.prod_comp` for a version without `h`.  -/
Function.Bijective.finsetProd : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [inst : Fintype ι] [inst_1 : Fintype κ] [inst_2 : CommMonoid M]
  (e : ι → κ), Function.Bijective e → ∀ (f : ι → M) (g : κ → M), (∀ (x : ι), f x = g (e x)) → ∏ x, f x = ∏ x, g x
-- Mathlib.NumberTheory.Padics.Complex
/-- `PadicAlgCl p` is a normed algebra over `ℚ_[p]`.  -/
PadicAlgCl.normedAlgebra : (p : ℕ) → [hp : Fact (Nat.Prime p)] → NormedAlgebra ℚ_[p] (PadicAlgCl p)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_insertMany_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {l : List (α × β)} {k k' : α},
  (k == k') = true →
    ∀ {v : β},
      List.Pairwise (fun a b => (a.1 == b.1) = false) l →
        (k, v) ∈ l → Std.DHashMap.Const.get? (Std.DHashMap.Const.insertMany m l) k' = some v
-- Lean.AuxRecursor
Lean.NoConfusionInfo.regular.inj : ∀ {arity lhs rhs arity_1 lhs_1 rhs_1 : ℕ},
  Lean.NoConfusionInfo.regular arity lhs rhs = Lean.NoConfusionInfo.regular arity_1 lhs_1 rhs_1 →
    arity = arity_1 ∧ lhs = lhs_1 ∧ rhs = rhs_1
-- Init.Data.Iterators.Basic
/-- A well-founded relation such that if `it'` is obtained from `it` by skipping, then `Rel it' it`.
 -/
Std.Iterators.ProductivenessRelation.Rel : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      [inst : Std.Iterator α m β] → Std.Iterators.ProductivenessRelation α m → Std.IterM m β → Std.IterM m β → Prop
-- Lean.Elab.BuiltinTerm
Lean.Elab.Term.elabScientificLit : Lean.Elab.Term.TermElab
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.algebraPolynomial' : {R : Type u_1} →
  [inst : CommSemiring R] →
    {A : Type u_3} → [inst_1 : CommSemiring A] → [Algebra R (Polynomial A)] → Algebra R (PowerSeries A)
-- Mathlib.Data.Multiset.NatAntidiagonal
/-- A pair (i, j) is contained in the antidiagonal of `n` if and only if `i + j = n`.  -/
Multiset.Nat.mem_antidiagonal : ∀ {n : ℕ} {x : ℕ × ℕ}, x ∈ Multiset.Nat.antidiagonal n ↔ x.1 + x.2 = n
-- Batteries.Data.List.Interleave
_private.Batteries.Data.List.Interleave.0.List.interleave.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (a : α) (l₁ l₂ : List α) (h_1 : (l₂ : List α) → motive [] l₂)
  (h_2 : (a : α) → (l₁ l₂ : List α) → motive (a :: l₁) l₂),
  (match a :: l₁, l₂ with
    | [], l₂ => h_1 l₂
    | a :: l₁, l₂ => h_2 a l₁ l₂) =
    h_2 a l₁ l₂
-- Mathlib.Geometry.Manifold.DerivationBundle
/-- With the `evalAlgebra` algebra structure evaluation is actually an algebra morphism.  -/
PointedContMDiffMap.eval : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_3} →
            [inst_3 : TopologicalSpace H] →
              {I : ModelWithCorners 𝕜 E H} →
                {M : Type u_4} →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] →
                      (x : M) → ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 ↑⊤ →ₐ[PointedContMDiffMap 𝕜 I M (↑⊤) x] 𝕜
-- Init.Data.Array.Subarray
Subarray.stop.eq_1 : ∀ {α : Type u_1} (xs : Subarray α), xs.stop = xs.internalRepresentation.stop
-- Mathlib.CategoryTheory.Filtered.FinallySmall
CategoryTheory.InitiallySmall.instIsCofilteredCofilteredInitialModel : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsCofiltered C]
  [inst_2 : CategoryTheory.LocallySmall.{w, v, u} C] [inst_3 : CategoryTheory.InitiallySmall C],
  CategoryTheory.IsCofiltered (CategoryTheory.InitiallySmall.CofilteredInitialModel C)
-- Mathlib.Algebra.Homology.SpectralObject.Differentials
CategoryTheory.Abelian.SpectralObject.Ψ.congr_simp : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ : ℤ)
  (hn₁ : n₀ + 1 = n₁), X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ = X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁
-- Init.Data.String.Defs
String.Pos.Raw.IsValidForSlice.mk : ∀ {s : String.Slice} {p : String.Pos.Raw},
  p ≤ s.rawEndPos →
    String.Pos.Raw.IsValid s.str (p.offsetBy s.startInclusive.offset) → String.Pos.Raw.IsValidForSlice s p
-- Mathlib.Analysis.Normed.Module.ContinuousInverse
/-- An invertible continuous linear map has a continuous left inverse.  -/
ContinuousLinearMap.HasLeftInverse.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.HasLeftInverse
-- Mathlib.RingTheory.Extension.Cotangent.Basis
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.tensorCotangentHom_tmul : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type u_4}
  {P : Algebra.Generators R S ι} {σ : Type u_5} {b : Module.Basis σ S P.toExtension.Cotangent}
  (D : Algebra.Generators.PresentationOfFreeCotangent.Aux✝ P b)
  (x : ↥(Algebra.Generators.PresentationOfFreeCotangent.Aux.presLeft✝ D).toExtension.ker),
  (Algebra.Generators.PresentationOfFreeCotangent.Aux.tensorCotangentHom✝ D)
      (1 ⊗ₜ[Algebra.Generators.PresentationOfFreeCotangent.Aux.T✝ D] Algebra.Extension.Cotangent.mk x) =
    Algebra.Extension.Cotangent.mk ⟨↑x, ⋯⟩
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- the morphisms in the covering of `S`  -/
CategoryTheory.PreZeroHypercover.f : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} → (self : CategoryTheory.PreZeroHypercover S) → (i : self.I₀) → self.X i ⟶ S
-- Mathlib.Logic.Equiv.Embedding
/-- Embeddings from a single-member type are equivalent to members of the target type.  -/
Equiv.uniqueEmbeddingEquivResult : {α : Type u_1} → {β : Type u_2} → [Unique α] → (α ↪ β) ≃ β
-- Mathlib.Tactic.DeriveEncodable
_private.Mathlib.Tactic.DeriveEncodable.0.Mathlib.Deriving.Encodable.S.decode : ℕ → Mathlib.Deriving.Encodable.S✝
-- Mathlib.Algebra.Ring.TransferInstance
/-- Transfer `NonUnitalNonAssocSemiring` across an `Equiv`  -/
Equiv.nonUnitalNonAssocSemiring : {α : Type u_1} → {β : Type u_2} → α ≃ β → [NonUnitalNonAssocSemiring β] → NonUnitalNonAssocSemiring α
-- Mathlib.Data.Finset.Empty
Finset.notMem_empty : ∀ {α : Type u_1} (a : α), a ∉ ∅
-- Mathlib.Tactic.FunProp.FunctionData
/-- Result of `getFunctionData?`. It returns function data if the function is in the form
`fun x ↦ f y₁ ... yₙ`. Two other cases are `fun x ↦ let y := ...` or `fun x y ↦ ...`  -/
Mathlib.Meta.FunProp.MaybeFunctionData : Type
-- Lean.Linter.MissingDocs
Lean.Linter.MissingDocs.builtinHandlersRef : IO.Ref (Lean.NameMap Lean.Linter.MissingDocs.Handler)
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
/-- Canonical ring homomorphism from the stalk of `smoothSheafCommRing IM I M R` at `x` to `R`,
given by evaluating sections at `x`, considered as a morphism in the category of commutative rings.
 -/
smoothSheafCommRing.evalHom : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {EM : Type u_2} →
      [inst_1 : NormedAddCommGroup EM] →
        [inst_2 : NormedSpace 𝕜 EM] →
          {HM : Type u_3} →
            [inst_3 : TopologicalSpace HM] →
              (IM : ModelWithCorners 𝕜 EM HM) →
                {E : Type u_4} →
                  [inst_4 : NormedAddCommGroup E] →
                    [inst_5 : NormedSpace 𝕜 E] →
                      {H : Type u_5} →
                        [inst_6 : TopologicalSpace H] →
                          (I : ModelWithCorners 𝕜 E H) →
                            (M : Type u) →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace HM M] →
                                  (R : Type u) →
                                    [inst_9 : TopologicalSpace R] →
                                      [inst_10 : ChartedSpace H R] →
                                        [inst_11 : CommRing R] →
                                          [inst_12 : ContMDiffRing I (↑⊤) R] →
                                            (x : ↑(TopCat.of M)) →
                                              (smoothSheafCommRing IM I M R).presheaf.stalk x ⟶ CommRingCat.of R
-- Init.Data.Float.Model.Unpacked.Basic
Float.Model.UnpackedFloat.infinity.injEq : ∀ (sign sign_1 : Float.Model.UnpackedFloat.Sign),
  (Float.Model.UnpackedFloat.infinity sign = Float.Model.UnpackedFloat.infinity sign_1) = (sign = sign_1)
-- Mathlib.Topology.LocallyConstant.Algebra
/-- `DFunLike.coe` as a linear map.  -/
LocallyConstant.coeFnₗ : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      (R : Type u_6) →
        [inst_1 : Semiring R] → [inst_2 : AddCommMonoid Y] → [inst_3 : Module R Y] → LocallyConstant X Y →ₗ[R] X → Y
-- Init.Prelude
/-- A `Nat` denotes a valid Unicode code point if it is less than `0x110000` and it is also not a
surrogate code point (the range `0xd800` to `0xdfff` inclusive).
 -/
Nat.isValidChar : ℕ → Prop
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.le_of_ceil_le : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] {a : R} {n : ℕ}
  [IsStrictOrderedRing R], ⌈a⌉₊ ≤ n → a ≤ ↑n
-- Init.Data.BitVec.Basic
/-- Checks whether addition of `x` and `y` results in *signed* overflow, treating `x` and `y` as 2's
complement signed bitvectors.

SMT-LIB name: `bvsaddo`.
 -/
BitVec.saddOverflow : {w : ℕ} → BitVec w → BitVec w → Bool
-- Lean.Language.Basic
Lean.Language.SnapshotTree.brecOn_1.eq : ∀ {motive_1 : Lean.Language.SnapshotTree → Sort u}
  {motive_2 : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree) → Sort u}
  {motive_3 : List (Lean.Language.SnapshotTask Lean.Language.SnapshotTree) → Sort u}
  {motive_4 : Lean.Language.SnapshotTask Lean.Language.SnapshotTree → Sort u}
  {motive_5 : Task Lean.Language.SnapshotTree → Sort u}
  (t : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree))
  (F_1 : (t : Lean.Language.SnapshotTree) → t.below → motive_1 t)
  (F_2 :
    (t : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)) →
      Lean.Language.SnapshotTree.below_1 t → motive_2 t)
  (F_3 :
    (t : List (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)) →
      Lean.Language.SnapshotTree.below_2 t → motive_3 t)
  (F_4 :
    (t : Lean.Language.SnapshotTask Lean.Language.SnapshotTree) → Lean.Language.SnapshotTree.below_3 t → motive_4 t)
  (F_5 : (t : Task Lean.Language.SnapshotTree) → Lean.Language.SnapshotTree.below_4 t → motive_5 t),
  Lean.Language.SnapshotTree.brecOn_1 t F_1 F_2 F_3 F_4 F_5 =
    F_2 t (Lean.Language.SnapshotTree.brecOn_1.go t F_1 F_2 F_3 F_4 F_5).2
-- Mathlib.RingTheory.Multiplicity
emultiplicity_eq_emultiplicity_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Monoid α] [inst_1 : Monoid β] {a b : α} {c d : β},
  emultiplicity a b = emultiplicity c d ↔ ∀ (n : ℕ), a ^ n ∣ b ↔ c ^ n ∣ d
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.addSubgroupOf_isAddCommutative : ∀ {G : Type u_1} [inst : AddGroup G] (K H : AddSubgroup G) [IsAddCommutative ↥H], IsAddCommutative ↥(H.addSubgroupOf K)
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.instPartialOrder : {α : Type u_2} → [inst : TopologicalSpace α] → PartialOrder (TopologicalSpace.Opens α)
-- Lean.ExtraModUses
Lean.instBEqIndirectModUse : BEq Lean.IndirectModUse
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.NSMul.eq_1 : ∀ {α : Type u_2} [inst : Zero α] [inst_1 : Add α], Set.NSMul = { smul := fun n s => nsmulRec n s }
-- Init.Data.Vector.Lemmas
Vector.getElem?_eq_none_iff : ∀ {α : Type u_1} {n i : ℕ} {xs : Vector α n}, xs[i]? = none ↔ n ≤ i
-- Init.Data.UInt.Lemmas
UInt8.mod_zero : ∀ {a : UInt8}, a % 0 = a
-- Mathlib.Analysis.BoxIntegral.Partition.Additive
/-- If `g : M → N` is an additive map and `f` is a box additive map, then `g ∘ f` is a box additive
map.  -/
BoxIntegral.BoxAdditiveMap.map : {ι : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      [inst : AddCommMonoid M] →
        [inst_1 : AddCommMonoid N] →
          {I₀ : WithTop (BoxIntegral.Box ι)} →
            BoxIntegral.BoxAdditiveMap ι M I₀ → (M →+ N) → BoxIntegral.BoxAdditiveMap ι N I₀