mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.CatCommSq
CategoryTheory.CatCommSq.hInv_iso_hom_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄] (T : C₁ ≌ C₂) (L : CategoryTheory.Functor C₁ C₃)
  (R : CategoryTheory.Functor C₂ C₄) (B : C₃ ≌ C₄) (x : CategoryTheory.CatCommSq T.functor L R B.functor) (X : C₂),
  (CategoryTheory.CatCommSq.iso T.inverse R L B.inverse).hom.app X =
    CategoryTheory.CategoryStruct.comp (B.unitIso.hom.app (L.obj (T.inverse.obj X)))
      (CategoryTheory.CategoryStruct.comp
        (B.inverse.map ((CategoryTheory.CatCommSq.iso T.functor L R B.functor).inv.app (T.inverse.obj X)))
        (B.inverse.map (R.map (T.counitIso.hom.app X))))
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM1to0.trAux.match_1.splitter : {Γ : Type u_1} →
  {Λ : Type u_2} →
    {σ : Type u_3} →
      (motive : Turing.TM1.Stmt Γ Λ σ → σ → Sort u_4) →
        (x : Turing.TM1.Stmt Γ Λ σ) →
          (x_1 : σ) →
            ((d : Turing.Dir) → (q : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → motive (Turing.TM1.Stmt.move d q) v) →
              ((a : Γ → σ → Γ) → (q : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → motive (Turing.TM1.Stmt.write a q) v) →
                ((a : Γ → σ → σ) → (q : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → motive (Turing.TM1.Stmt.load a q) v) →
                  ((p : Γ → σ → Bool) →
                      (q₁ q₂ : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → motive (Turing.TM1.Stmt.branch p q₁ q₂) v) →
                    ((l : Γ → σ → Λ) → (v : σ) → motive (Turing.TM1.Stmt.goto l) v) →
                      ((v : σ) → motive Turing.TM1.Stmt.halt v) → motive x x_1
-- Mathlib.Order.Std
/-- The `LE` instance of the order.  -/
Preorder.OfStdArgs.le : {α : Type u_1} → Preorder.OfStdArgs α → LE α
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.coeff_mul_X : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (n : ℕ), (p * Polynomial.X).coeff (n + 1) = p.coeff n
-- Std.Http.Data.URI.Basic
/-- A domain name (lowercase-normalized).
 -/
Std.Http.URI.Host.name : Std.Http.URI.DomainName → Std.Http.URI.Host
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.opFunctorCompSnd_hom_app : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) (X : (CategoryTheory.Comma L R)ᵒᵖ),
  (CategoryTheory.Comma.opFunctorCompSnd L R).hom.app X =
    CategoryTheory.CategoryStruct.id (Opposite.op (Opposite.unop X).left)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.inv_inv_h₀_comp_f_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreZeroHypercover S} (e : E ≅ F)
  (i : F.I₀) {Z : C} (h : S ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (e.inv.h₀ i)) (CategoryTheory.CategoryStruct.comp (F.f i) h) =
    CategoryTheory.CategoryStruct.comp (E.f (e.inv.s₀ i)) h
-- Batteries.Data.List.Basic
/-- `pop : List α → StateM (List α) (List α)` transforms the input list `old`
by taking the head of the current state and pushing it on the head of `old`.
If the state list is empty, then `old` is left unchanged.  -/
List.transpose.pop : {α : Type u_1} → List α → List α → Id (List α × List α)
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.Ring.OfSemiring.of_diseq : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] [Lean.Grind.AddRightCancel α] (ctx : Lean.Grind.CommRing.Context α)
  (lhs rhs : Lean.Grind.CommRing.Expr),
  Lean.Grind.CommRing.Expr.denoteS ctx lhs ≠ Lean.Grind.CommRing.Expr.denoteS ctx rhs →
    Lean.Grind.CommRing.Expr.denoteSAsRing ctx lhs ≠ Lean.Grind.CommRing.Expr.denoteSAsRing ctx rhs
-- Mathlib.Data.Fin.VecNotation
/-- Parses a chain of `Matrix.vecCons` calls into elements, leaving everything else in the tail.

`let ⟨xs, tailn, tail⟩ ← matchVecConsPrefix n e` decomposes `e : Fin n → _` in the form
`vecCons x₀ <| ... <| vecCons xₙ <| tail` where `tail : Fin tailn → _`.  -/
Matrix.matchVecConsPrefix : Q(ℕ) → Lean.Expr → Lean.MetaM (List Lean.Expr × Q(ℕ) × Lean.Expr)
-- Mathlib.Analysis.Complex.Circle
Real.fourierChar_apply' : ∀ (x : ℝ), Real.fourierChar x = Circle.exp (2 * Real.pi * x)
-- Mathlib.Algebra.Group.Subgroup.Pointwise
/-- For subgroups generated by a single element, see the simpler `zpow_induction_right`.  -/
Subgroup.closure_induction_right : ∀ {G : Type u_2} [inst : Group G] {s : Set G} {p : (x : G) → x ∈ Subgroup.closure s → Prop},
  p 1 ⋯ →
    (∀ (x : G) (hx : x ∈ Subgroup.closure s) (y : G) (hy : y ∈ s), p x hx → p (x * y) ⋯) →
      (∀ (x : G) (hx : x ∈ Subgroup.closure s) (y : G) (hy : y ∈ s), p x hx → p (x * y⁻¹) ⋯) →
        ∀ {x : G} (h : x ∈ Subgroup.closure s), p x h
-- Mathlib.Combinatorics.SimpleGraph.Finite
/-- In a graph, if `k` is at least the degree of every vertex, then it is at least the maximum
degree.  -/
SimpleGraph.maxDegree_le_of_forall_degree_le : ∀ {V : Type u_1} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj] (k : ℕ),
  (∀ (v : V), G.degree v ≤ k) → G.maxDegree ≤ k
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
Std.IterM.flatMapM.eq_1 : ∀ {α β α₂ γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [inst_2 : Std.Iterator α m β]
  [inst_3 : Std.Iterator α₂ m γ] (f : β → m (Std.IterM m γ)) (it : Std.IterM m β),
  Std.IterM.flatMapM f it = Std.IterM.flatMapAfterM f it none
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.mem_incidenceSet : ∀ {V : Type u} (G : SimpleGraph V) (v w : V), s(v, w) ∈ G.incidenceSet v ↔ G.Adj v w
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Diagnostics.mk.injEq : ∀ (usedThmCounter triedThmCounter : Lean.PHashMap Lean.Meta.Origin ℕ) (congrThmCounter : Lean.PHashMap Lean.Name ℕ)
  (thmsWithBadKeys : Lean.PArray Lean.Meta.SimpTheorem)
  (usedThmCounter_1 triedThmCounter_1 : Lean.PHashMap Lean.Meta.Origin ℕ)
  (congrThmCounter_1 : Lean.PHashMap Lean.Name ℕ) (thmsWithBadKeys_1 : Lean.PArray Lean.Meta.SimpTheorem),
  ({ usedThmCounter := usedThmCounter, triedThmCounter := triedThmCounter, congrThmCounter := congrThmCounter,
        thmsWithBadKeys := thmsWithBadKeys } =
      { usedThmCounter := usedThmCounter_1, triedThmCounter := triedThmCounter_1, congrThmCounter := congrThmCounter_1,
        thmsWithBadKeys := thmsWithBadKeys_1 }) =
    (usedThmCounter = usedThmCounter_1 ∧
      triedThmCounter = triedThmCounter_1 ∧ congrThmCounter = congrThmCounter_1 ∧ thmsWithBadKeys = thmsWithBadKeys_1)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
Int.reduceNegSucc : Lean.Meta.Simp.DSimproc
-- Mathlib.Topology.Algebra.Group.Basic
continuousNeg_iInf : ∀ {G : Type w} {ι' : Sort u_1} [inst : Neg G] {ts' : ι' → TopologicalSpace G},
  (∀ (i : ι'), ContinuousNeg G) → ContinuousNeg G
-- Mathlib.GroupTheory.Exponent
Monoid.pow_eq_mod_exponent : ∀ {G : Type u} [inst : Monoid G] {n : ℕ} (g : G), g ^ n = g ^ (n % Monoid.exponent G)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get!_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α}
  [inst_3 : Inhabited (β k)], (List.map Sigma.fst l).contains k = false → (t.insertMany l).get! k = t.get! k
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.InjectiveTheorem.mk : Array Lean.Name → Lean.Expr → List Lean.HeadIndex → Lean.Meta.Grind.Origin → Lean.Meta.Grind.InjectiveTheorem
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.card_sInf_range_compl_le_lift : ∀ {ι : Type u} (f : ι → Ordinal.{max u v}), (sInf (Set.range f)ᶜ).card ≤ Cardinal.lift.{v, u} (Cardinal.mk ι)
-- Init.Grind.Ordered.Field
_private.Init.Grind.Ordered.Field.0.Lean.Grind.Field.IsOrdered.lt_mul_inv_of_lt_mul : ∀ {R : Type u} [inst : Lean.Grind.Field R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsLinearOrder R] [Lean.Grind.OrderedRing R] {a b c : R}, c < 0 → a < b * c → b < a * c⁻¹
-- Mathlib.Order.Interval.Finset.SuccPred
Finset.insert_Ioc_left_eq_Ioc_pred_of_not_isMin : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : PredOrder α] {a b : α},
  a ≤ b → ¬IsMin a → insert a (Finset.Ioc a b) = Finset.Ioc (Order.pred a) b
-- Mathlib.Analysis.RCLike.Lemmas
Polynomial.ofReal_eval : ∀ {K : Type u_1} [inst : RCLike K] (p : Polynomial ℝ) (x : ℝ), ↑(Polynomial.eval x p) = (Polynomial.aeval ↑x) p
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.PolyDerivation.step.injEq : ∀ (p : Lean.Grind.CommRing.Poly) (k₁ : ℤ) (d : Lean.Meta.Grind.Arith.CommRing.PolyDerivation) (k₂ : ℤ)
  (m₂ : Lean.Grind.CommRing.Mon) (c : Lean.Meta.Grind.Arith.CommRing.EqCnstr) (p_1 : Lean.Grind.CommRing.Poly)
  (k₁_1 : ℤ) (d_1 : Lean.Meta.Grind.Arith.CommRing.PolyDerivation) (k₂_1 : ℤ) (m₂_1 : Lean.Grind.CommRing.Mon)
  (c_1 : Lean.Meta.Grind.Arith.CommRing.EqCnstr),
  (Lean.Meta.Grind.Arith.CommRing.PolyDerivation.step p k₁ d k₂ m₂ c =
      Lean.Meta.Grind.Arith.CommRing.PolyDerivation.step p_1 k₁_1 d_1 k₂_1 m₂_1 c_1) =
    (p = p_1 ∧ k₁ = k₁_1 ∧ d = d_1 ∧ k₂ = k₂_1 ∧ m₂ = m₂_1 ∧ c = c_1)
-- Mathlib.Algebra.Notation.Indicator
/-- `Set.indicator s f a` is `f a` if `a ∈ s`, `0` otherwise.  -/
Set.indicator : {α : Type u_1} → {M : Type u_3} → [Zero M] → Set α → (α → M) → α → M
-- Init.Data.Nat.Power2.Lemmas
Nat.and_sub_one_testBit_log2 : ∀ {n : ℕ}, n ≠ 0 → ¬n.isPowerOfTwo → (n &&& n - 1).testBit n.log2 = true
-- Lean.Meta.Structure
/-- Structure projection declaration for `mkProjections`.
 -/
Lean.Meta.StructProjDecl : Type
-- Mathlib.Topology.Sets.Order
/-- Reinterpret an upper clopen as an upper set.  -/
ClopenUpperSet.toUpperSet : {α : Type u_1} → [inst : TopologicalSpace α] → [inst_1 : LE α] → ClopenUpperSet α → UpperSet α
-- Mathlib.Dynamics.Flow
/-- The map `τ → α → α` underlying a flow of `τ` on `α`.  -/
Flow.toFun : {τ : Type u_1} →
  {α : Type u_2} →
    [inst : TopologicalSpace τ] → [inst_1 : TopologicalSpace α] → [inst_2 : AddZero τ] → Flow τ α → τ → α → α
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.Nat.mul_add_le_mul_of_succ_le : ∀ {a b c : ℕ}, a + 1 ≤ c → a * b + b ≤ c * b
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.IsNotG2.toIsValuedIn : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} {inst : CommRing R} {inst_1 : AddCommGroup M}
  {inst_2 : Module R M} {inst_3 : AddCommGroup N} {inst_4 : Module R N} {P : RootPairing ι R M N} [self : P.IsNotG2],
  P.IsValuedIn ℤ
-- Mathlib.Data.Vector.MapLemmas
List.Vector.mapAccumr₂_bisim : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ₁ : Type u_6} {σ₂ : Type u_7} {n : ℕ} {xs : List.Vector α n}
  {ys : List.Vector β n} {f₁ : α → β → σ₁ → σ₁ × γ} {f₂ : α → β → σ₂ → σ₂ × γ} {s₁ : σ₁} {s₂ : σ₂} (R : σ₁ → σ₂ → Prop),
  R s₁ s₂ →
    (∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).1 (f₂ a b q).1 ∧ (f₁ a b s).2 = (f₂ a b q).2) →
      R (List.Vector.mapAccumr₂ f₁ xs ys s₁).1 (List.Vector.mapAccumr₂ f₂ xs ys s₂).1 ∧
        (List.Vector.mapAccumr₂ f₁ xs ys s₁).2 = (List.Vector.mapAccumr₂ f₂ xs ys s₂).2
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
/-- A `ReflexiveCofork` is a cocone over a `WalkingReflexivePair`-shaped diagram.  -/
CategoryTheory.Limits.ReflexiveCofork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C → Type (max (max 0 u) v)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.toReal_pi_div_two : (↑(Real.pi / 2)).toReal = Real.pi / 2
-- Lean.Server.References
/-- Finds all references in `trees` and deduplicates the result.
See `dedupReferences` and `combineIdents`.
 -/
Lean.Server.findModuleRefs : Lean.FileMap → Array Lean.Elab.InfoTree → optParam Bool true → optParam Bool false → Lean.Server.ModuleRefs
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.ringCon_le_iff : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] {I J : TwoSidedIdeal R}, I ≤ J ↔ I.ringCon ≤ J.ringCon
-- Mathlib.Dynamics.Minimal
AddAction.IsMinimal.dense_orbit : ∀ {M : Type u_1} {α : Type u_2} {inst : AddMonoid M} {inst_1 : TopologicalSpace α} {inst_2 : AddAction M α}
  [self : AddAction.IsMinimal M α] (x : α), Dense (AddAction.orbit M x)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.GetLsbD
Std.Tactic.BVDecide.BVPred.GetLsbDTarget.mk : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} → {w : ℕ} → aig.RefVec w → ℕ → Std.Tactic.BVDecide.BVPred.GetLsbDTarget aig
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
_private.Mathlib.Combinatorics.SimpleGraph.Regularity.Bound.0.termA : Lean.ParserDescr
-- Mathlib.Data.Quot
/-- `Trunc α` is the quotient of `α` by the always-true relation. This
is related to the propositional truncation in HoTT, and is similar
in effect to `Nonempty α`, but unlike `Nonempty α`, `Trunc α` is data,
so the VM representation is the same as `α`, and so this can be used to
maintain computability.  -/
Trunc : Sort u → Sort u
-- Init.Data.String.Iterate
String.Slice.PosIterator : String.Slice → Type
-- Mathlib.Order.Hom.CompleteLattice
FrameHom.mk : {α : Type u_8} →
  {β : Type u_9} →
    [inst : CompleteLattice α] →
      [inst_1 : CompleteLattice β] →
        (toInfTopHom : InfTopHom α β) →
          (∀ (s : Set α), toInfTopHom.toFun (sSup s) = sSup (toInfTopHom.toFun '' s)) → FrameHom α β
-- Mathlib.Geometry.Manifold.Instances.Real
frontier_halfSpace : ∀ {n : ℕ} (p : ENNReal) (a : ℝ) (i : Fin n), frontier {y | a ≤ y.ofLp i} = {y | a = y.ofLp i}
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.var.sizeOf_spec : ∀ {w : ℕ} (idx : ℕ), sizeOf (Std.Tactic.BVDecide.BVExpr.var idx) = 1 + sizeOf w + sizeOf idx
-- Mathlib.CategoryTheory.Monad.Monadicity
CategoryTheory.Monad.instPreservesColimitWalkingParallelPairParallelPairOfIsSplitPairOfPreservesColimitOfIsSplitPair : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {G : CategoryTheory.Functor D C} {A B : D} (f g : A ⟶ B) [G.IsSplitPair f g]
  [CategoryTheory.Monad.PreservesColimitOfIsSplitPair G],
  CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G
-- Mathlib.Analysis.Complex.Norm
Complex.normSq_ofReal_add_I_mul_sqrt_one_sub : ∀ {x : ℝ}, ‖x‖ ≤ 1 → Complex.normSq (↑x + Complex.I * ↑√(1 - x ^ 2)) = 1
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron.triangle_mor₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂}
  {w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
  {h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃), h.triangle.mor₂ = h.m₃
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
BoundedContinuousFunction.mk.congr_simp : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
  (toContinuousMap toContinuousMap_1 : C(α, β)) (e_toContinuousMap : toContinuousMap = toContinuousMap_1)
  (map_bounded' : ∃ C, ∀ (x y : α), dist (toContinuousMap.toFun x) (toContinuousMap.toFun y) ≤ C),
  { toContinuousMap := toContinuousMap, map_bounded' := map_bounded' } =
    { toContinuousMap := toContinuousMap_1, map_bounded' := ⋯ }
-- Mathlib.Data.Fin.Tuple.Take
/-- Alternative version of `take_eq_take_list_ofFn` with `l : List α` instead of `v : Fin n → α`.  -/
Fin.ofFn_take_get : ∀ {α : Type u_2} {m : ℕ} (l : List α) (h : m ≤ l.length), List.ofFn (Fin.take m h l.get) = List.take m l
-- Mathlib.Analysis.Normed.Group.Defs
ContinuousENorm.continuous_enorm : ∀ {E : Type u_8} {inst : TopologicalSpace E} [self : ContinuousENorm E], Continuous enorm
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get?_empty : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : LawfulBEq α] {a : α}, ∅.get? a = none
-- Init.Data.Vector.MapIdx
Vector.mk_mem_zipIdx_iff_le_and_getElem?_sub : ∀ {α : Type u_1} {n : ℕ} {x : α} {i : ℕ} {xs : Vector α n} {k : ℕ}, (x, i) ∈ xs.zipIdx k ↔ k ≤ i ∧ xs[i - k]? = some x
-- Mathlib.Topology.Order.IsLUB
IsLUB.mem_of_isClosed : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {a : α} {s : Set α},
  IsLUB s a → s.Nonempty → IsClosed s → a ∈ s
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multifork.app_right_eq_ι_comp_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  {I : CategoryTheory.Limits.MulticospanIndex J C} (K : CategoryTheory.Limits.Multifork I) (b : J.R) {Z : C}
  (h : I.multicospan.obj (CategoryTheory.Limits.WalkingMulticospan.right b) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.π.app (CategoryTheory.Limits.WalkingMulticospan.right b)) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (K.ι (J.snd b)) (I.snd b)) h
-- Mathlib.Order.Monotone.Basic
Nat.rel_of_forall_rel_succ_of_lt : ∀ {β : Type v} (r : β → β → Prop) [IsTrans β r] {f : ℕ → β},
  (∀ (n : ℕ), r (f n) (f (n + 1))) → ∀ ⦃a b : ℕ⦄, a < b → r (f a) (f b)
-- Mathlib.Order.CompletePartialOrder
DirectedOn.isLUB_sSup : ∀ {α : Type u_2} [inst : CompletePartialOrder α] {d : Set α}, DirectedOn (fun x1 x2 => x1 ≤ x2) d → IsLUB d (sSup d)
-- Mathlib.Algebra.Group.Prod
AddUnits.mk.congr_simp : ∀ {α : Type u} [inst : AddMonoid α] (val val_1 : α) (e_val : val = val_1) (neg neg_1 : α) (e_neg : neg = neg_1)
  (val_neg : val + neg = 0) (neg_val : neg + val = 0),
  { val := val, neg := neg, val_neg := val_neg, neg_val := neg_val } =
    { val := val_1, neg := neg_1, val_neg := ⋯, neg_val := ⋯ }
-- Lean.Parser.Basic
_private.Lean.Parser.Basic.0.Lean.Parser.isHexDigit : Char → Bool
-- Mathlib.CategoryTheory.Sites.Point.Monoidal
CategoryTheory.GrothendieckTopology.Point.instOplaxMonoidalFunctorOppositePresheafFiber : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      (Φ : J.Point) →
        {A : Type u'} →
          [inst_1 : CategoryTheory.Category.{v', u'} A] →
            [inst_2 : CategoryTheory.MonoidalCategory A] →
              [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] → Φ.presheafFiber.OplaxMonoidal
-- Init.Data.List.Sublist
List.IsPrefix.getElem : ∀ {α : Type u_1} {xs ys : List α} (h : xs <+: ys) {i : ℕ} (hi : i < xs.length), xs[i] = ys[i]
-- Mathlib.CategoryTheory.Monoidal.Hopf_
CategoryTheory.Hopf.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : C) [hopf : CategoryTheory.HopfObj X] (X_1 : C)
  (hopf_1 : CategoryTheory.HopfObj X_1),
  ({ X := X, hopf := hopf } = { X := X_1, hopf := hopf_1 }) = (X = X_1 ∧ hopf ≍ hopf_1)
-- Mathlib.Order.ConditionallyCompletePartialOrder.Basic
csInf_Ico : ∀ {α : Type u_5} [inst : ConditionallyCompletePartialOrderInf α] {a b : α}, a < b → sInf (Set.Ico a b) = a
-- Mathlib.Data.Nat.GCD.Basic
Nat.coprime_add_self_right : ∀ {m n : ℕ}, m.Coprime (n + m) ↔ m.Coprime n
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.mem_congr : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a b : α}, (a == b) = true → (a ∈ m ↔ b ∈ m)
-- Init.Data.Float.Model.Float
/-- Converts a `Nat` to a `Float.Model`, returning positive zero on zero.  -/
Float.Model.ofNat : ℕ → Float.Model
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.size_alter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β),
  (↑m).WF →
    ∀ {k : α} {f : Option β → Option β},
      (↑(Std.DHashMap.Internal.Raw₀.Const.alter m k f)).size =
        if m.contains k = true ∧ (f (Std.DHashMap.Internal.Raw₀.Const.get? m k)).isNone = true then (↑m).size - 1
        else
          if ¬m.contains k = true ∧ (f (Std.DHashMap.Internal.Raw₀.Const.get? m k)).isSome = true then (↑m).size + 1
          else (↑m).size
-- Mathlib.Algebra.Module.ULift
ULift.addAction : {R : Type u} → {M : Type v} → [inst : AddMonoid R] → [AddAction R M] → AddAction (ULift.{u_1, u} R) M
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.AppImplicitArg.optional.injEq : ∀ (name : Lean.Name) (s : Lean.Term) (name_1 : Lean.Name) (s_1 : Lean.Term),
  (Lean.PrettyPrinter.Delaborator.AppImplicitArg.optional name s =
      Lean.PrettyPrinter.Delaborator.AppImplicitArg.optional name_1 s_1) =
    (name = name_1 ∧ s = s_1)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
/-- The inclusion of a SubAddAction into the ambient set, as an equivariant map.  -/
SubAddAction.inclusion : {M : Type u_1} → {α : Type u_2} → [inst : AddMonoid M] → [inst_1 : AddAction M α] → (s : SubAddAction M α) → ↥s →ₑ[id] α
-- Mathlib.Algebra.CharP.Defs
/-- Noncomputable function that outputs the unique exponential characteristic of a semiring.  -/
ringExpChar : (R : Type u_1) → [NonAssocSemiring R] → ℕ
-- Mathlib.RingTheory.LocalRing.ResidueField.Polynomial
Polynomial.fiberEquivQuotient.eq_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (f : Polynomial R →ₐ[R] S) (hf : Function.Surjective ⇑f) (p : Ideal R) [inst_3 : p.IsPrime],
  Polynomial.fiberEquivQuotient f hf p =
    AlgEquiv.ofAlgHom
      (Algebra.TensorProduct.lift
        (Algebra.ofId p.ResidueField
          (Polynomial p.ResidueField ⧸
            Ideal.map (Polynomial.mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f)))
        (f.liftOfSurjective hf
          ((Ideal.Quotient.mkₐ R
                (Ideal.map (Polynomial.mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f))).comp
            (Polynomial.mapAlgHom (Algebra.ofId R p.ResidueField)))
          ⋯)
        ⋯)
      (Ideal.Quotient.liftₐ (Ideal.map (Polynomial.mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f))
        (Polynomial.aeval (1 ⊗ₜ[R] f Polynomial.X)) ⋯)
      ⋯ ⋯
-- Mathlib.Tactic.Linter.Header
/-- `getImports s` takes as input `s : Syntax`.
It returns the array of all `import` statement syntax nodes in `s`.  -/
_private.Mathlib.Tactic.Linter.Header.0.Mathlib.Linter.getImports : Lean.Syntax → Array Lean.Syntax