mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- Decomposition of a `R`-algebra homomorphism from `R[M]` by
its values on `F (single a 1)`.  -/
AddMonoidAlgebra.lift_unique : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} [inst : CommSemiring R] [inst_1 : AddMonoid M] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] (F : AddMonoidAlgebra R M →ₐ[R] A) (f : AddMonoidAlgebra R M),
  F f = f.coeff.sum fun m r => r • F (AddMonoidAlgebra.single m 1)
-- Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
CochainComplex.shiftShortComplexFunctor'_hom_app_τ₁ : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (n i j k i' j' k' : ℤ) (hi : n + i = i') (hj : n + j = j') (hk : n + k = k') (X : CochainComplex C ℤ),
  ((CochainComplex.shiftShortComplexFunctor' C n i j k i' j' k' hi hj hk).hom.app X).τ₁ =
    n.negOnePow • (HomologicalComplex.XIsoOfEq X ⋯).hom
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem!_modify_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α}
  [inst : Inhabited β] {f : β → β}, (m.modify k f)[k]! = (Option.map f m[k]?).get!
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
HasDerivWithinAt.const_rpow : ∀ {f : ℝ → ℝ} {f' x : ℝ} {s : Set ℝ} {a : ℝ},
  0 < a → HasDerivWithinAt f f' s x → HasDerivWithinAt (fun x => a ^ f x) (Real.log a * f' * a ^ f x) s x
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.orthogonalProjectionOnto_eq_zero_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} [inst_3 : K.HasOrthogonalProjection] {v : E}, K.orthogonalProjectionOnto v = 0 ↔ v ∈ Kᗮ
-- Mathlib.Order.SupClosed
SupClosed.finsetSup'_mem : ∀ {α : Type u_3} [inst : SemilatticeSup α] {ι : Type u_5} {f : ι → α} {s : Set α} {t : Finset ι},
  SupClosed s → ∀ (ht : t.Nonempty), (∀ i ∈ t, f i ∈ s) → t.sup' ht f ∈ s
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_filter_key_iff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] {f : α → Bool}
  (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filter (fun a x => f a) t ⋯).impl.isEmpty = true ↔
    ∀ (k : α) (h : Std.DTreeMap.Internal.Impl.contains k t = true), f (t.getKey k h) = false
-- Mathlib.Order.Basic
Prod.mk_le_swap : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] {x : α × β} {a : α} {b : β}, (b, a) ≤ x.swap ↔ (a, b) ≤ x
-- Mathlib.Data.Finset.Card
Finset.one_lt_card_iff_nontrivial : ∀ {α : Type u_1} {s : Finset α}, 1 < s.card ↔ s.Nontrivial
-- Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits
_private.Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits.0.SimpleGraph.ErdosStone.le_card_edgeFinset_between_verts : ∀ {n : ℕ} {G : SimpleGraph (Fin n)} [inst : DecidableRel G.Adj] {r t' : ℕ} (K : G.CompleteEquipartiteSubgraph r t'),
  ↑K.verts.card * (↑G.minDegree - ↑K.verts.card) ≤ ↑(SimpleGraph.between (↑K.verts) (↑K.verts)ᶜ G).edgeFinset.card
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
/-- The counit for the equivalence `Mon (C ⥤ D) ≌ C ⥤ Mon D`.
 -/
CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.counitIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.MonoidalCategory D] →
          CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverse✝.comp
              CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functor ≅
            CategoryTheory.Functor.id (CategoryTheory.Functor C (CategoryTheory.Comon D))
-- Init.SizeOf
Except.ok.sizeOf_spec : ∀ {ε : Type u} {α : Type v} [inst : SizeOf ε] [inst_1 : SizeOf α] (a : α), sizeOf (Except.ok a) = 1 + sizeOf a
-- Lean.Meta.Closure
Lean.Meta.Closure.State.mk : Lean.LevelMap Lean.Level →
  Lean.ExprStructMap Lean.Expr →
    Array Lean.Name →
      ℕ →
        Array Lean.Level →
          Array Lean.LocalDecl →
            Array Lean.LocalDecl →
              Array Lean.LocalDecl →
                ℕ →
                  Array Lean.Expr → Array Lean.Expr → Array Lean.Meta.Closure.ToProcessElement → Lean.Meta.Closure.State
-- Mathlib.Algebra.Order.Interval.Basic
Interval.bot_ne_zero : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : Zero α], ⊥ ≠ 0
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Module.Basis.card_le_card_of_linearIndependent : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  {ι : Type u_2} [inst_4 : Fintype ι] (b : Module.Basis ι R M) {ι' : Type u_3} [inst_5 : Fintype ι'] {v : ι' → M},
  LinearIndependent R v → Fintype.card ι' ≤ Fintype.card ι
-- Mathlib.Algebra.Quaternion
/-- Third imaginary part (k) of a quaternion.  -/
QuaternionAlgebra.imK : {R : Type u_1} → {a b c : R} → QuaternionAlgebra R a b c → R
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageXIso.congr_simp : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, 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₀)
  (r : ℤ) (hr : r₀ ≤ r) (pq : κ) (i₀ i₁ i₂ i₃ : ι) (h₀ : i₀ = data.i₀ r pq ⋯) (h₁ : i₁ = data.i₁ pq)
  (h₂ : i₂ = data.i₂ pq) (h₃ : i₃ = data.i₃ r pq ⋯) (n₀ n₁ n₂ : ℤ) (h : n₁ = data.deg pq) (hn₁ : n₀ + 1 = n₁)
  (hn₂ : n₁ + 1 = n₂),
  CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageXIso X data r hr pq i₀ i₁ i₂ i₃ h₀ h₁ h₂ h₃ n₀ n₁ n₂ h hn₁
      hn₂ =
    CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageXIso X data r hr pq i₀ i₁ i₂ i₃ h₀ h₁ h₂ h₃ n₀ n₁ n₂ h
      hn₁ hn₂
-- Mathlib.Computability.Partrec
Computable.cond : ∀ {α : Type u_1} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable σ] {c : α → Bool} {f g : α → σ},
  Computable c → Computable f → Computable g → Computable fun a => bif c a then f a else g a
-- Mathlib.Analysis.Convex.Between
wbtw_add_const_iff : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] {x y z : V} (v : V), Wbtw R (x + v) (y + v) (z + v) ↔ Wbtw R x y z
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.cycleOf_pow_apply_self : ∀ {α : Type u_2} (f : Equiv.Perm α) [inst : DecidableRel f.SameCycle] (x : α) (n : ℕ), (f.cycleOf x ^ n) x = (f ^ n) x
-- Mathlib.CategoryTheory.MorphismProperty.Retract
/-- A class of morphisms is stable under retracts if a retract of such a morphism still
lies in the class.  -/
CategoryTheory.MorphismProperty.IsStableUnderRetracts : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → Prop
-- Mathlib.LinearAlgebra.Matrix.Defs
/-- The right `n × r` part of an `n × (l+r)` matrix.  -/
Matrix.subRight : {α : Type v} → {m l r : ℕ} → Matrix (Fin m) (Fin (l + r)) α → Matrix (Fin m) (Fin r) α
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPoly.match_1.congr_eq_4 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (a : Lean.Grind.CommRing.Expr)
  (h_1 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.num n))
  (h_2 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast n))
  (h_3 : (n : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast n))
  (h_4 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_5 : (x : Lean.Grind.CommRing.Expr) → motive x) (x : Lean.Grind.CommRing.Var),
  a = Lean.Grind.CommRing.Expr.var x →
    (match a with
      | Lean.Grind.CommRing.Expr.num n => h_1 n
      | Lean.Grind.CommRing.Expr.intCast n => h_2 n
      | Lean.Grind.CommRing.Expr.natCast n => h_3 n
      | Lean.Grind.CommRing.Expr.var x => h_4 x
      | x => h_5 x) ≍
      h_4 x
-- Mathlib.LinearAlgebra.Matrix.SchurComplement
Matrix.invOf_fromBlocks₁₁_eq : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_4} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
  [inst_3 : DecidableEq n] [inst_4 : CommRing α] (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α)
  (D : Matrix n n α) [inst_5 : Invertible A] [inst_6 : Invertible (D - C * ⅟A * B)]
  [inst_7 : Invertible (Matrix.fromBlocks A B C D)],
  ⅟(Matrix.fromBlocks A B C D) =
    Matrix.fromBlocks (⅟A + ⅟A * B * ⅟(D - C * ⅟A * B) * C * ⅟A) (-(⅟A * B * ⅟(D - C * ⅟A * B)))
      (-(⅟(D - C * ⅟A * B) * C * ⅟A)) ⅟(D - C * ⅟A * B)
-- Mathlib.Probability.Kernel.Deterministic
ProbabilityTheory.IsDeterministic.mk : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β},
  (κ.parallelComp κ).comp (ProbabilityTheory.Kernel.copy α) = (ProbabilityTheory.Kernel.copy β).comp κ →
    ProbabilityTheory.IsDeterministic κ
-- Aesop.Options.Public
/-- If `true`, Aesop succeeds only if it proves the goal. If `false`, Aesop always
succeeds and reports the goals remaining after safe rules were applied.
 -/
Aesop.Options.terminal : Aesop.Options → Bool
-- Mathlib.Probability.StrongLaw
ProbabilityTheory.abs_truncation_le_abs_self : ∀ {α : Type u_1} (f : α → ℝ) (A : ℝ) (x : α), |ProbabilityTheory.truncation f A x| ≤ |f x|
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- **Alias** of `FunLike.coe_smul`. -/
AddGroupSeminorm.coe_smul : ∀ {M : Type u_1} {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : SMul M F]
  [inst_2 : SMul M β] [IsSMulApply M F α β] (n : M) (f : F), ⇑(n • f) = n • ⇑f
-- Mathlib.Algebra.Module.Torsion.Basic
/-- The additive `n`-torsion subgroup for an integer `n`, denoted as `A[n]`.  -/
AddSubgroup.torsionByStx : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.hom_ext₃_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 3}
  {φ φ' : f ⟶ g},
  φ = φ' ↔
    CategoryTheory.ComposableArrows.app' φ 0 _proof_297✝ = CategoryTheory.ComposableArrows.app' φ' 0 _proof_297✝ ∧
      CategoryTheory.ComposableArrows.app' φ 1 _proof_298✝ = CategoryTheory.ComposableArrows.app' φ' 1 _proof_298✝ ∧
        CategoryTheory.ComposableArrows.app' φ 2 _proof_299✝ = CategoryTheory.ComposableArrows.app' φ' 2 _proof_299✝ ∧
          CategoryTheory.ComposableArrows.app' φ 3 _proof_300✝ = CategoryTheory.ComposableArrows.app' φ' 3 _proof_300✝
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roo.pairwise_toList_ne : ∀ {α : Type u} {r : Std.Roo α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.Rxo.IsAlwaysFinite α], List.Pairwise (fun a b => a ≠ b) r.toList
-- Mathlib.NumberTheory.PrimeCounting
Nat.primeCounting_zero : Nat.primeCounting 0 = 0
-- Std.Data.HashSet.Raw
Std.HashSet.Raw.instLawfulSingleton : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α], LawfulSingleton α (Std.HashSet.Raw α)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.coreOfNat.inj : ∀ {e thm : Lean.Expr} {d : ℕ} {a : Int.Internal.Linear.Expr} {e_1 thm_1 : Lean.Expr} {d_1 : ℕ}
  {a_1 : Int.Internal.Linear.Expr},
  Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.coreOfNat e thm d a =
      Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.coreOfNat e_1 thm_1 d_1 a_1 →
    e = e_1 ∧ thm = thm_1 ∧ d = d_1 ∧ a = a_1
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
SimplexCategoryGenRel.σ_comp_σ_assoc : ∀ {n : ℕ} {i j : Fin (n + 1)},
  i ≤ j →
    ∀ {Z : SimplexCategoryGenRel} (h : SimplexCategoryGenRel.mk n ⟶ Z),
      CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.σ i.castSucc)
          (CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.σ j) h) =
        CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.σ j.succ)
          (CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.σ i) h)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- **Alias** of `ValuativeRel.vle_trans`. -/
ValuativeRel.vle.trans : ∀ {R : Type u_1} {inst : Semiring R} [self : ValuativeRel R] {z y x : R}, x ≤ᵥ y → y ≤ᵥ z → x ≤ᵥ z
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
/-- The function `update f a : X a → Π a, X a` is always measurable.
This doesn't require `f` to be measurable.
This should not be confused with the statement that `update f a x` is measurable.  -/
measurable_update : ∀ {δ : Type u_4} {X : δ → Type u_6} [inst : (a : δ) → MeasurableSpace (X a)] (f : (a : δ) → X a) {a : δ}
  [inst_1 : DecidableEq δ], Measurable (Function.update f a)
-- Batteries.Data.UnionFind.Basic
/-- Array of union-find nodes  -/
Batteries.UnionFind.arr : Batteries.UnionFind → Array Batteries.UFNode
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.neg_seq : ∀ {α β : Type u} (f : FreeAbelianGroup (α → β)) (x : FreeAbelianGroup α), -f <*> x = -(f <*> x)
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.closure_def : ∀ {α : Type u_2} (M : Matroid α) (X : Set α), M.closure X = ⋂₀ {F | M.IsFlat F ∧ X ∩ M.E ⊆ F}
-- Mathlib.NumberTheory.SelbergSieve
BoundingSieve.siftedSum_le_mainSum_errSum_of_upperMoebius : ∀ {s : BoundingSieve} (muPlus : ℕ → ℝ),
  BoundingSieve.IsUpperMoebius muPlus →
    BoundingSieve.siftedSum ≤ s.totalMass * BoundingSieve.mainSum muPlus + BoundingSieve.errSum muPlus
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_eq_measureReal_of_between_null_sdiff : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ s₃ : Set α},
  s₁ ⊆ s₂ →
    s₂ ⊆ s₃ →
      μ.real (s₃ \ s₁) = 0 →
        autoParam (μ (s₃ \ s₁) ≠ ⊤) MeasureTheory.measureReal_eq_measureReal_of_between_null_sdiff._auto_1 →
          μ.real s₁ = μ.real s₂ ∧ μ.real s₂ = μ.real s₃
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
/-- Given `K ∈ ℝ` and a finite `S ⊆ G`, an atom of `G` with respect to `K` and `S` is a (finite
and nonempty) fragment `A` of minimal cardinality.  -/
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.IsAtom : {G : Type u_1} → [Group G] → [DecidableEq G] → ℝ → Finset G → Finset G → Prop
-- Mathlib.Topology.Order.Category.AlexDisc
alexDiscEquivPreord_inverse_obj_carrier : ∀ (X : Preord), ↑(alexDiscEquivPreord.inverse.obj X).toTopCat = Topology.WithUpperSet ↑X
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
ciInf_of_not_bddBelow : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrder α] {f : ι → α},
  ¬BddBelow (Set.range f) → ⨅ i, f i = sInf ∅
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
toENat_rank_span_set : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type w}
  [StrongRankCondition R] {v : ι → M} {s : Set ι},
  LinearIndepOn R v s → Cardinal.toENat (Module.rank R ↥(Submodule.span R (v '' s))) = s.encard
-- Mathlib.GroupTheory.Commutator.Basic
Subgroup.Normal.of_commutator_le : ∀ (G : Type u_1) [inst : Group G] {H : Subgroup G}, commutator G ≤ H → H.Normal
-- Lean.Exception
/-- Throw an error exception using the given message data and reference syntax.  -/
Lean.throwErrorAt : {m : Type → Type} → {α : Type} → [Monad m] → [Lean.MonadError m] → Lean.Syntax → Lean.MessageData → m α
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulC_nc.go.eq_def : ∀ (p₂ : Lean.Grind.CommRing.Poly) (c : ℕ) (p₁ acc : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.mulC_nc.go p₂ c p₁ acc =
    match p₁ with
    | Lean.Grind.CommRing.Poly.num k => acc.combineC (Lean.Grind.CommRing.Poly.mulConstC k p₂ c) c
    | Lean.Grind.CommRing.Poly.add k m p₁ =>
      Lean.Grind.CommRing.Poly.mulC_nc.go p₂ c p₁ (acc.combineC (Lean.Grind.CommRing.Poly.mulMonC_nc k m p₂ c) c)
-- Mathlib.Order.Partition.Basic
/-- The bottom element is not a part.  -/
Partition.bot_notMem' : ∀ {α : Type u_1} [inst : CompleteLattice α] {s : α} (self : Partition s), ⊥ ∉ self.parts
-- Std.Async.Signal
Std.Async.instReprSignal : Repr Std.Async.Signal
-- Mathlib.Topology.Compactification.OnePoint.Basic
/-- For any topological space `X`, its one point compactification is a compact space.  -/
OnePoint.instCompactSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X], CompactSpace (OnePoint X)
-- Mathlib.Analysis.Convex.Gauge
Convex.setOfPred_gauge_le : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E},
  Convex ℝ s → 0 ∈ s → Absorbent ℝ s → ∀ (a : ℝ), Convex ℝ {x | gauge s x ≤ a}
-- Mathlib.Analysis.Calculus.FDeriv.Basic
fderiv_id : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {x : E} [ContinuousAdd E] [ContinuousSMul 𝕜 E] [T2Space E],
  fderiv 𝕜 id x = ContinuousLinearMap.id 𝕜 E
-- Mathlib.Algebra.Category.BialgCat.Monoidal
BialgCat.MonoidalCategory.inducingFunctorData_εIso : ∀ (R : Type u) [inst : CommRing R],
  (BialgCat.MonoidalCategory.inducingFunctorData R).εIso =
    CategoryTheory.Iso.refl (CategoryTheory.MonoidalCategoryStruct.tensorUnit (AlgCat R))
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.ofRepr.injEq : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (repr repr_1 : M ≃ₗ[R] ι →₀ R), ({ repr := repr } = { repr := repr_1 }) = (repr = repr_1)
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.map_iInf : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] {ι : Sort u_1} [Nonempty ι] (f : A →ₐ[R] B),
  Function.Injective ⇑f → ∀ (s : ι → Subalgebra R A), Subalgebra.map f (iInf s) = ⨅ i, Subalgebra.map f (s i)
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.clearUnit.eq_1 : ∀ {n : ℕ} (x : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin n)
  (b : Bool),
  Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.clearUnit x (l, b) =
    x.modify (↑l) (Std.Tactic.BVDecide.LRAT.Internal.Assignment.removeAssignment b)
-- Mathlib.GroupTheory.QuotientGroup.Basic
/-- **Alias** of `MonoidHom.domRestrictHomKerEquiv_apply_coe`. -/
MonoidHom.restrictHomKerEquiv_apply_coe : ∀ {G : Type u} [inst : Group G] (A : Type u_1) [inst_1 : CommGroup A] (H : Subgroup G) [inst_2 : H.Normal]
  (f : ↥(MonoidHom.domRestrictHom H A).ker) (g : G), ((MonoidHom.domRestrictHomKerEquiv A H) f) ↑g = ↑f g
-- Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer
/-- Composition of `ι` with `f` and with `g` agree  -/
CategoryTheory.IsSplitEqualizer.condition : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {W : C} {ι : W ⟶ X}
  (self : CategoryTheory.IsSplitEqualizer f g ι),
  CategoryTheory.CategoryStruct.comp ι f = CategoryTheory.CategoryStruct.comp ι g
-- Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian
/-- The Dold-Kan equivalence for pseudoabelian categories given
by the functors `N` and `Γ`. It is obtained by applying the results in
`Compatibility.lean` to the equivalence `Preadditive.DoldKan.Equivalence`.  -/
CategoryTheory.Idempotents.DoldKan.equivalence : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [CategoryTheory.IsIdempotentComplete C] →
        [CategoryTheory.Limits.HasFiniteCoproducts C] → CategoryTheory.SimplicialObject C ≌ ChainComplex C ℕ
-- Mathlib.Computability.TuringMachine.PostTuringMachine
cond.match_1.congr_eq_2 : ∀ (motive : Bool → Sort u_1) (c : Bool) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  c = false →
    (match c with
      | true => h_1 ()
      | false => h_2 ()) ≍
      h_2 ()
-- Init.Internal.Order.Basic
Lean.Order.chain_empty : ∀ (α : Sort u) [inst : Lean.Order.PartialOrder α], Lean.Order.chain (Lean.Order.empty_chain α)
-- Mathlib.CategoryTheory.Functor.Trifunctor
CategoryTheory.bifunctorComp₁₂FunctorMap_app_app_app_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5}
  [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₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C₁₂]
  {F₁₂ F₁₂' : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} (φ : F₁₂ ⟶ F₁₂')
  (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) (X₁ : C₁) (X₂ : C₂) (X₃ : C₃),
  ((((CategoryTheory.bifunctorComp₁₂FunctorMap φ).app G).app X₁).app X₂).app X₃ = (G.map ((φ.app X₁).app X₂)).app X₃
-- Std.Time.Format.Modifier
/-- `Text` represents different text formatting styles.
 -/
Std.Time.Text : Type
-- Mathlib.RingTheory.PicardGroup
/-- The Picard group of a commutative semiring R consists of the invertible R-modules,
up to isomorphism.  -/
CommRing.Pic : (R : Type u) → [CommSemiring R] → Type u
-- Mathlib.CategoryTheory.Localization.OfQuotient
CategoryTheory.Functor.isLocalization_of_essSurj_of_full_of_exists_cylinders : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) [L.EssSurj] [L.Full]
  (W : CategoryTheory.MorphismProperty C),
  W.IsInvertedBy L → (∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), L.map f₀ = L.map f₁ → ∃ P x, W P.π) → L.IsLocalization W
-- Lean.Meta.NatInstTesters
Lean.Meta.Structural.isInstHModNat : Lean.Expr → Lean.MetaM Bool
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
/-- Auxiliary definition for `StrictSegal.ofCore`.  -/
SSet.StrictSegalCore.spineToSimplex : {X : SSet} → ((n : ℕ) → X.StrictSegalCore n) → {n : ℕ} → X.Path n → X.obj (Opposite.op { len := n })
-- Init.Grind.ToInt
Lean.Grind.ToInt.Add.mk : ∀ {α : Type u} [inst : Add α] {I : outParam Lean.Grind.IntInterval} [inst_1 : Lean.Grind.ToInt α I],
  (∀ (x y : α), ↑(x + y) = I.wrap (↑x + ↑y)) → Lean.Grind.ToInt.Add α I
-- Mathlib.Computability.TuringMachine.Computable
_private.Mathlib.Computability.TuringMachine.Computable.0.Turing.TM2ComputableInPolyTime.comp : {α β γ αΓ βΓ γΓ : Type} →
  {eα : α → List αΓ} →
    {eβ : β → List βΓ} →
      {eγ : γ → List γΓ} →
        {f : α → β} →
          {g : β → γ} →
            Turing.TM2ComputableInPolyTime eα eβ f →
              Turing.TM2ComputableInPolyTime eβ eγ g →
                ProofWanted (Nonempty (Turing.TM2ComputableInPolyTime eα eγ (g ∘ f)))
-- Mathlib.RingTheory.WittVector.Truncated
TruncatedWittVector.instNatCast : (p n : ℕ) → (R : Type u_1) → [CommRing R] → [Fact (Nat.Prime p)] → NatCast (TruncatedWittVector p n R)
-- Mathlib.MeasureTheory.Measure.Haar.Unique
/-- If an invariant measure is inner regular, then it gives less mass to sets with compact closure
than any other invariant measure, up to the scalar `haarScalarFactor μ' μ`.

Auxiliary lemma in the proof of the more general
`measure_isMulInvariant_eq_smul_of_isCompact_closure`, which gives equality for any
set with compact closure.  -/
MeasureTheory.Measure.smul_measure_isMulInvariant_le_of_isCompact_closure : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [LocallyCompactSpace G] (μ' μ : MeasureTheory.Measure G)
  [inst_6 : μ.IsHaarMeasure] [inst_7 : MeasureTheory.IsFiniteMeasureOnCompacts μ'] [inst_8 : μ'.IsMulLeftInvariant]
  [μ.InnerRegularCompactLTTop] {s : Set G}, MeasurableSet s → IsCompact (closure s) → μ'.haarScalarFactor μ • μ s ≤ μ' s
-- Init.Data.Int.DivMod.Lemmas
Int.tdiv_eq_of_eq_mul_left : ∀ {a b c : ℤ}, b ≠ 0 → a = c * b → a.tdiv b = c
-- Mathlib.Data.Seq.Parallel
/-- Induction principle for parallel computations.
The reason this isn't trivial from `exists_of_mem_parallel` is because it eliminates to `Sort`.  -/
Computation.parallelRec : {α : Type u} →
  {S : Stream'.WSeq (Computation α)} →
    (C : α → Sort v) →
      ((s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a) → {a : α} → a ∈ Computation.parallel S → C a