mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Simprocs.mk : Lean.Meta.Simp.SimprocTree →
  Lean.Meta.Simp.SimprocTree → Lean.PHashSet Lean.Name → Lean.PHashSet Lean.Name → Lean.Meta.Simprocs
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.coe_smul : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : CommSemiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  (ρ : Representation A G V) (σ : Representation A G W) (a : A) (f : ρ.IntertwiningMap σ), ⇑(a • f) = a • ⇑f
-- Batteries.Recycling.RBTree.Basic
RBTree.RBMap.instToStreamKeysStream : {α : Type u} →
  {β : Type v} → {cmp : α → α → Ordering} → Std.ToStream (RBTree.RBMap.Keys α β cmp) (RBTree.RBMap.Keys.Stream α β)
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.map_vadd' : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2]
  [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2] (self : P1 →ᵃ[k] P2) (p : P1) (v : V1),
  self.toFun (v +ᵥ p) = self.linear v +ᵥ self.toFun p
-- Mathlib.Data.Sym.Basic
SymOptionSuccEquiv.encode_decode : ∀ {α : Type u_1} {n : ℕ} [inst : DecidableEq α] (s : Sym (Option α) n ⊕ Sym α n.succ),
  SymOptionSuccEquiv.encode (SymOptionSuccEquiv.decode s) = s
-- Init.Data.String.Basic
String.endPos_toSlice : ∀ {s : String}, s.toSlice.endPos = s.endPos.toSlice
-- Mathlib.Order.Hom.BoundedLattice
InfTopHomClass.mk : ∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} [inst : Min α] [inst_1 : Min β] [inst_2 : Top α] [inst_3 : Top β]
  [inst_4 : FunLike F α β] [toInfHomClass : InfHomClass F α β], (∀ (f : F), f ⊤ = ⊤) → InfTopHomClass F α β
-- Mathlib.Algebra.Category.Ring.Colimits
_private.Mathlib.Algebra.Category.Ring.Colimits.0.CommRingCat.Colimits.descFunLift.match_1.eq_3 : ∀ {J : Type u_1} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat)
  (motive : CommRingCat.Colimits.Prequotient F → Sort u_2)
  (h_1 : (j : J) → (x : ↑(F.obj j)) → motive (CommRingCat.Colimits.Prequotient.of j x))
  (h_2 : Unit → motive CommRingCat.Colimits.Prequotient.zero) (h_3 : Unit → motive CommRingCat.Colimits.Prequotient.one)
  (h_4 : (x : CommRingCat.Colimits.Prequotient F) → motive x.neg)
  (h_5 : (x y : CommRingCat.Colimits.Prequotient F) → motive (x.add y))
  (h_6 : (x y : CommRingCat.Colimits.Prequotient F) → motive (x.mul y)),
  (match CommRingCat.Colimits.Prequotient.one with
    | CommRingCat.Colimits.Prequotient.of j x => h_1 j x
    | CommRingCat.Colimits.Prequotient.zero => h_2 ()
    | CommRingCat.Colimits.Prequotient.one => h_3 ()
    | x.neg => h_4 x
    | x.add y => h_5 x y
    | x.mul y => h_6 x y) =
    h_3 ()
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.MonoOver.isIso_iff_subobjectMk_eq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {P Q : CategoryTheory.MonoOver X} (f : P ⟶ Q),
  CategoryTheory.IsIso f ↔ CategoryTheory.Subobject.mk P.obj.hom = CategoryTheory.Subobject.mk Q.obj.hom
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasProdLocallyUniformlyOn.exists_hasProdUniformlyOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {g : β → α} {x : β} {s : Set β}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β] [LocallyCompactSpace β],
  HasProdLocallyUniformlyOn f g s → s ∈ nhds x → ∃ t ∈ nhdsWithin x s, HasProdUniformlyOn f g t
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
zero_notMem_nonZeroDivisors : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [Nontrivial M₀], 0 ∉ nonZeroDivisors M₀
-- Mathlib.Topology.EMetricSpace.VariationOnFromTo
variationOnFromTo.add : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {f : α → E} {s : Set α},
  LocallyBoundedVariationOn f s →
    ∀ {a b c : α},
      a ∈ s → b ∈ s → c ∈ s → variationOnFromTo f s a b + variationOnFromTo f s b c = variationOnFromTo f s a c
-- Mathlib.Data.Set.Enumerate
Set.enumerate.eq_def : ∀ {α : Type u_1} (sel : Set α → Option α) (x : Set α) (x_1 : ℕ),
  Set.enumerate sel x x_1 =
    match x, x_1 with
    | s, 0 => sel s
    | s, n.succ => do
      let a ← sel s
      Set.enumerate sel (s \ {a}) n
-- Mathlib.Topology.UniformSpace.UniformConvergence
tendstoUniformlyOn_iff_seq_tendstoUniformlyOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α}
  {l : Filter ι} [l.IsCountablyGenerated],
  TendstoUniformlyOn F f l s ↔
    ∀ (u : ℕ → ι), Filter.Tendsto u Filter.atTop l → TendstoUniformlyOn (fun n => F (u n)) f Filter.atTop s
-- Mathlib.Order.ConditionallyCompleteLattice.Finset
Finset.ciSup_union : ∀ {ι : Type u_1} {α : Type u_2} [inst : ConditionallyCompleteLinearOrderBot α] [inst_1 : DecidableEq ι] {f : ι → α}
  {s t : Finset ι}, ⨆ x ∈ s ∪ t, f x = max (⨆ x ∈ s, f x) (⨆ x ∈ t, f x)
-- Mathlib.Data.DList.Instances
Batteries.instTraversableDList : Traversable Batteries.DList
-- Mathlib.Tactic.ComputeDegree
Mathlib.Tactic.ComputeDegree.natDegree_smul_le_of_le : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_2} [inst_1 : SMulZeroClass S R] {n : ℕ} {a : S} {f : Polynomial R},
  f.natDegree ≤ n → (a • f).natDegree ≤ n
-- Mathlib.Data.List.Cycle
Cycle.lists.eq_1 : ∀ {α : Type u_1} (s : Cycle α), s.lists = Quotient.liftOn' s (fun l => ↑l.cyclicPermutations) ⋯
-- Mathlib.CategoryTheory.Comma.Over.OverClass
/-- See Note [custom simps projection]  -/
CategoryTheory.OverClass.Simps.over : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → (X S : C) → [CategoryTheory.OverClass X S] → X ⟶ S
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTranspose_eq_intCast : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Ring α] [inst_2 : StarRing α] {M : Matrix n n α} {d : ℤ},
  M.conjTranspose = ↑d ↔ M = ↑d
-- Mathlib.Algebra.Category.ModuleCat.Basic
/-- The scalar multiplication on `ModuleCat R` considered as a morphism of rings
to the endomorphisms of the forgetful functor to `AddCommGrpCat)`.  -/
ModuleCat.smulNatTrans : (R : Type u) → [inst : Ring R] → R →+* CategoryTheory.End (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat)
-- Mathlib.Order.Filter.ENNReal
ENNReal.liminf_const_mul_of_ne_top : ∀ {α : Type u_1} {f : Filter α} [f.NeBot] {u : α → ENNReal} {a : ENNReal},
  a ≠ ⊤ → Filter.liminf (fun x => a * u x) f = a * Filter.liminf u f
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Internal.Small.map : ∀ {α : Type v} {β : Type w} (P : α → Prop) (f : (a : α) → P a → β) [Std.Internal.Small { a // P a }],
  Std.Internal.Small { b // ∃ a, ∃ (h : P a), f a h = b }
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Real.qaryEntropy_nonneg : ∀ {q : ℕ} {p : ℝ}, 0 ≤ p → p ≤ 1 → 0 ≤ Real.qaryEntropy q p
-- Mathlib.RingTheory.Ideal.Maximal
Ideal.irreducible_of_isMaximal_span_singleton : ∀ {α : Type u} [inst : CommSemiring α] [IsDomain α] {a : α}, a ≠ 0 → (Ideal.span {a}).IsMaximal → Irreducible a
-- Init.Data.Option.Lemmas
Option.isSome_guard : ∀ {α : Type u_1} {p : α → Bool} {a : α}, (Option.guard p a).isSome = p a
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.comp_symm : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂), (↑e).comp ↑e.symm = AlgHom.id R A₂
-- Mathlib.CategoryTheory.Limits.MorphismProperty
CategoryTheory.MorphismProperty.Over.hasFiniteLimits : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) (X : T)
  [CategoryTheory.Limits.HasPullbacks T] [P.IsMultiplicative] [P.IsStableUnderBaseChange] [P.HasOfPostcompProperty P],
  CategoryTheory.Limits.HasFiniteLimits (P.Over ⊤ X)
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
/-- A set of vectors `v` is orthogonal with respect to some bilinear map `B` if and only
if for all `i ≠ j`, `B (v i) (v j) = 0`.  -/
LinearMap.IsOrthoᵢ : {R : Type u_1} →
  {R₁ : Type u_2} →
    {M : Type u_5} →
      {M₁ : Type u_6} →
        {n : Type u_19} →
          [inst : CommSemiring R] →
            [inst_1 : CommSemiring R₁] →
              [inst_2 : AddCommMonoid M₁] →
                [inst_3 : Module R₁ M₁] →
                  [inst_4 : AddCommMonoid M] →
                    [inst_5 : Module R M] → {I₁ I₁' : R₁ →+* R} → (M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] M) → (n → M₁) → Prop
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey!_filter_key : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {f : α → Bool} {k : α},
  (Std.HashMap.filter (fun k x => f k) m).getKey! k = (Option.filter f (m.getKey? k)).get!
-- Mathlib.Algebra.Colimit.Module
DirectLimit.Module.lift.congr_simp : ∀ (R : Type u_1) (ι : Type u_2) [inst : Preorder ι] (G : ι → Type u_3) {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  (f : (x x_1 : ι) → (h : x ≤ x_1) → T h) [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : Semiring R]
  [inst_5 : (i : ι) → AddCommMonoid (G i)] [inst_6 : (i : ι) → Module R (G i)]
  [inst_7 : ∀ (i j : ι) (h : i ≤ j), LinearMapClass (T h) R (G i) (G j)] [inst_8 : Nonempty ι] {P : Type u_7}
  [inst_9 : AddCommMonoid P] [inst_10 : Module R P] (g g_1 : (i : ι) → G i →ₗ[R] P) (e_g : g = g_1)
  (Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x),
  DirectLimit.Module.lift R ι G f g Hg = DirectLimit.Module.lift R ι G f g_1 ⋯
-- Mathlib.Algebra.Homology.Embedding.Basic
ComplexShape.instIsRelIffNatIntEmbeddingUpNat : ComplexShape.embeddingUpNat.IsRelIff
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
/-- The basis after applying a basis extension.  -/
Tactic.ComputeAsymptotics.BasisExtension.getBasis : {basis : Tactic.ComputeAsymptotics.Basis} →
  Tactic.ComputeAsymptotics.BasisExtension basis → Tactic.ComputeAsymptotics.Basis
-- Mathlib.Algebra.Group.WithOne.Basic
WithOne.lift_coe : ∀ {α : Type u} {β : Type v} [inst : Mul α] [inst_1 : MulOneClass β] (f : α →ₙ* β) (x : α), (WithOne.lift f) ↑x = f x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPullback.isoPullback.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst fst_1 : P ⟶ X} (e_fst : fst = fst_1)
  {snd snd_1 : P ⟶ Y} (e_snd : snd = snd_1) {f : X ⟶ Z} {g : Y ⟶ Z} (h : CategoryTheory.IsPullback fst snd f g)
  [inst_1 : CategoryTheory.Limits.HasPullback f g], h.isoPullback = ⋯.isoPullback
-- Mathlib.Data.Int.Cast.Lemmas
Commute.intCast_mul_self : ∀ {α : Type u_3} [inst : Ring α] (a : α) (n : ℤ), Commute (↑n * a) a
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.Hom.comm_from_assoc : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c}
  (f : C₁.Hom C₂) (i : ι) {Z : V} (h : C₂.xNext i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (f.f i) (CategoryTheory.CategoryStruct.comp (C₂.dFrom i) h) =
    CategoryTheory.CategoryStruct.comp (C₁.dFrom i) (CategoryTheory.CategoryStruct.comp (f.next i) h)
-- Mathlib.Order.Filter.Ker
Filter.ker_top : ∀ {α : Type u_2}, ⊤.ker = Set.univ
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
_private.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.0.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyzeAppStagedCore.checkOutParams : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeAppM Unit
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.comp_f₂_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex.SnakeInput C} (f : S₁ ⟶ S₂) (g : S₂ ⟶ S₃) {Z : CategoryTheory.ShortComplex C}
  (h : S₃.L₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).f₂ h =
    CategoryTheory.CategoryStruct.comp f.f₂ (CategoryTheory.CategoryStruct.comp g.f₂ h)
-- Mathlib.LinearAlgebra.TensorProduct.Map
TensorProduct.congr_symm_tmul : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7}
  {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N]
  [inst_4 : AddCommMonoid M₂] [inst_5 : AddCommMonoid N₂] [inst_6 : Module R M] [inst_7 : Module R N]
  [inst_8 : Module R₂ M₂] [inst_9 : Module R₂ N₂] {σ₂₁ : R₂ →+* R} [inst_10 : RingHomInvPair σ₁₂ σ₂₁]
  [inst_11 : RingHomInvPair σ₂₁ σ₁₂] (f : M ≃ₛₗ[σ₁₂] M₂) (g : N ≃ₛₗ[σ₁₂] N₂) (p : M₂) (q : N₂),
  (TensorProduct.congr f g).symm (p ⊗ₜ[R₂] q) = f.symm p ⊗ₜ[R] g.symm q
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
ContDiffOn.exp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {n : WithTop ℕ∞},
  ContDiffOn ℝ n f s → ContDiffOn ℝ n (fun x => Real.exp (f x)) s
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.inst : {M : Type u_1} → {N : Type u_2} → [inst : Monoid M] → [inst_1 : Monoid N] → Monoid (Monoid.Coprod M N)
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
/-- The boundary of `M × N` is `∂M × N ∪ (M × ∂N)`.  -/
ModelWithCorners.boundary_prod : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {N : Type u_7}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H' N] {J : ModelWithCorners 𝕜 E' H'},
  ModelWithCorners.boundary (M × N) =
    Set.univ.prod (ModelWithCorners.boundary N) ∪ (ModelWithCorners.boundary M).prod Set.univ
-- Mathlib.AlgebraicTopology.SimplicialNerve
CategoryTheory.SimplicialThickening.functor_obj_as : ∀ {J K : Type u} [inst : LinearOrder J] [inst_1 : LinearOrder K] (f : J →o K)
  (x : CategoryTheory.SimplicialThickening J), ((CategoryTheory.SimplicialThickening.functor f).obj x).as = f x.as
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
/-- `∑' i, f i` is the unconditional sum of `f` if it exists, or 0 otherwise.

More generally, if `L` is a `SummationFilter`, `∑'[L] i, f i` is the sum of `f` with respect to
`L` if it exists, and `0` otherwise.

(Note that even if the unconditional sum exists, it might not be unique if the topology is not
separated. When the support of `f` is finite, we make the most reasonable choice, to use the sum
over the support. Otherwise, we choose arbitrarily an `a` satisfying `HasSum f a`. Similar remarks
apply to more general summation filters.)
 -/
«term∑'_,_» : Lean.ParserDescr
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rio.mem_toArray_iff_mem : ∀ {α : Type u} {r : Std.Rio α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_7 : Std.Rxo.IsAlwaysFinite α] {a : α}, a ∈ r.toArray ↔ a ∈ r
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKeyD_le_maxKeyD_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = false →
    ∀ {k : α} {v : β} {fallback : α}, (cmp (t.maxKeyD fallback) ((t.insertIfNew k v).maxKeyD fallback)).isLE = true
-- Mathlib.Data.Holor
/-- A slice is a subholor consisting of all entries with initial index i.  -/
Holor.slice : {α : Type} → {d : ℕ} → {ds : List ℕ} → Holor α (d :: ds) → (i : ℕ) → i < d → Holor α ds
-- Mathlib.Order.Basic
max_rec : ∀ {α : Type u_2} [inst : LinearOrder α] {a b : α} {p : α → Prop}, (b ≤ a → p a) → (a ≤ b → p b) → p (max a b)
-- Std.Data.TreeMap.Raw.Slice
Std.TreeMap.Raw.toList_roc : ∀ {α : Type u} {β : Type v} (cmp : autoParam (α → α → Ordering) Std.TreeMap.Raw.toList_roc._auto_1) [Std.TransCmp cmp]
  {t : Std.TreeMap.Raw α β cmp},
  t.WF →
    ∀ {lowerBound upperBound : α},
      Std.Slice.toList (Std.Roc.Sliceable.mkSlice t lowerBound<...=upperBound) =
        List.filter (fun e => decide ((cmp e.1 lowerBound).isGT = true ∧ (cmp e.1 upperBound).isLE = true)) t.toList
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.BifibrantObject.instIsStableUnderPrecompHomRel : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C],
  CategoryTheory.HomRel.IsStableUnderPrecomp (HomotopicalAlgebra.BifibrantObject.homRel C)
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
/-- The map `f ↦ (x ↦ B (f x) (g x))` as a continuous `𝕜`-linear map on 𝓓^{n}_{K}(E, F₁),
where `B` is a continuous `𝕜`-linear map and `g` is a C^n function.

TODO: Introduce a type of bundled C^k functions.  -/
ContDiffMapSupportedIn.bilinLeftCLM : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace ℝ E] →
          {n : ℕ∞} →
            {K : TopologicalSpace.Compacts E} →
              {F₁ : Type u_5} →
                {F₂ : Type u_6} →
                  {F₃ : Type u_7} →
                    [inst_3 : NormedAlgebra ℝ 𝕜] →
                      [inst_4 : NormedAddCommGroup F₁] →
                        [inst_5 : NormedSpace 𝕜 F₁] →
                          [inst_6 : NormedSpace ℝ F₁] →
                            [inst_7 : NormedAddCommGroup F₂] →
                              [inst_8 : NormedSpace 𝕜 F₂] →
                                [inst_9 : NormedSpace ℝ F₂] →
                                  [inst_10 : NormedAddCommGroup F₃] →
                                    [inst_11 : NormedSpace 𝕜 F₃] →
                                      [inst_12 : NormedSpace ℝ F₃] →
                                        (F₁ →L[𝕜] F₂ →L[𝕜] F₃) →
                                          {g : E → F₂} →
                                            ContDiff ℝ (↑n) g →
                                              ContDiffMapSupportedIn E F₁ n K →L[𝕜] ContDiffMapSupportedIn E F₃ n K
-- Std.Internal.UV.System
Std.Internal.UV.System.CPUTimes.sys : Std.Internal.UV.System.CPUTimes → UInt64
-- Init.Data.SInt.Lemmas
Int32.toBitVec_toISize : ∀ (x : Int32), x.toISize.toBitVec = BitVec.signExtend System.Platform.numBits x.toBitVec
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.ext : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  {f g : S.LocalizationMap N}, (∀ (x : M), f x = g x) → f = g
-- Std.Http.Data.URI.Parser
_private.Std.Http.Data.URI.Parser.0.Std.Http.URI.Parser.parseHierPart : Std.Http.URI.Config → Std.Internal.Parsec.ByteArray.Parser (Option Std.Http.URI.Authority × Std.Http.URI.Path)
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.Seed.mk.injEq : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] (toArchimedeanStrata : HahnEmbedding.ArchimedeanStrata K M)
  (coeff : (c : FiniteArchimedeanClass M) → ↥(toArchimedeanStrata.stratum c) →ₗ[K] R)
  (strictMono_coeff : ∀ (c : FiniteArchimedeanClass M), StrictMono ⇑(coeff c))
  (toArchimedeanStrata_1 : HahnEmbedding.ArchimedeanStrata K M)
  (coeff_1 : (c : FiniteArchimedeanClass M) → ↥(toArchimedeanStrata_1.stratum c) →ₗ[K] R)
  (strictMono_coeff_1 : ∀ (c : FiniteArchimedeanClass M), StrictMono ⇑(coeff_1 c)),
  ({ toArchimedeanStrata := toArchimedeanStrata, coeff := coeff, strictMono_coeff := strictMono_coeff } =
      { toArchimedeanStrata := toArchimedeanStrata_1, coeff := coeff_1, strictMono_coeff := strictMono_coeff_1 }) =
    (toArchimedeanStrata = toArchimedeanStrata_1 ∧ coeff ≍ coeff_1)
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.coe_addHom : ∀ {α : Type u} [inst : AddMonoid α], ⇑WithBot.addHom = WithBot.some
-- Mathlib.LinearAlgebra.Alternating.DomCoprod
AlternatingMap.domCoprod_coe : ∀ {ιa : Type u_1} {ιb : Type u_2} [inst : Fintype ιa] [inst_1 : Fintype ιb] {R' : Type u_3} {Mᵢ : Type u_4}
  {N₁ : Type u_5} {N₂ : Type u_6} [inst_2 : CommSemiring R'] [inst_3 : AddCommGroup N₁] [inst_4 : Module R' N₁]
  [inst_5 : AddCommGroup N₂] [inst_6 : Module R' N₂] [inst_7 : AddCommMonoid Mᵢ] [inst_8 : Module R' Mᵢ]
  [inst_9 : DecidableEq ιa] [inst_10 : DecidableEq ιb] (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂),
  ↑(a.domCoprod b) = ∑ σ, AlternatingMap.domCoprod.summand a b σ
-- Init.Prelude
/-- A UTF-8 byte position that points at the end of a string, just after the last character.

* `"abc".rawEndPos = ⟨3⟩`
* `"L∃∀N".rawEndPos = ⟨8⟩`
 -/
String.rawEndPos : String → String.Pos.Raw
-- Mathlib.Algebra.Ring.Hom.Defs
/-- Any type satisfying `NonUnitalRingHomClass` can be cast into `NonUnitalRingHom` via
`NonUnitalRingHomClass.toNonUnitalRingHom`.  -/
instCoeTCNonUnitalRingHom : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : NonUnitalNonAssocSemiring α] →
        [inst_1 : NonUnitalNonAssocSemiring β] →
          [inst_2 : FunLike F α β] → [NonUnitalRingHomClass F α β] → CoeTC F (α →ₙ+* β)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- A fixed choice of positive orientation of Euclidean space `ℝ²`  -/
EuclideanGeometry.o : {R : Type u_3} →
  {inst : CommSemiring R} →
    {inst_1 : PartialOrder R} →
      {inst_2 : IsStrictOrderedRing R} →
        {M : Type u_4} →
          {inst_3 : AddCommMonoid M} →
            {inst_4 : Module R M} → {ι : Type u_5} → [self : Module.Oriented R M ι] → Orientation R M ι
-- Mathlib.RingTheory.Derivation.DifferentialRing
Differential.ContainConstants.mk : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [inst_3 : Differential B], (∀ {x : B}, x′ = 0 → x ∈ (algebraMap A B).range) → Differential.ContainConstants A B
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.Iter.foldM_filterMapM : ∀ {α β γ δ : Type w} {n : Type w → Type w'} {o : Type w → Type w''} {Pred EPred : Type w} [inst : Std.Iterator α Id β]
  [Std.Iterators.Finite α Id] [inst_2 : Monad n] [inst_3 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
  [inst_6 : Monad o] [inst_7 : Std.Internal.Do.Assertion Pred] [inst_8 : Std.Internal.Do.Assertion EPred]
  [inst_9 : Std.Internal.Do.WPMonad o Pred EPred] [inst_10 : Std.IteratorLoop α Id n]
  [inst_11 : Std.IteratorLoop α Id o] [Std.LawfulIteratorLoop α Id n] [Std.LawfulIteratorLoop α Id o]
  [inst_14 : MonadLiftT n o] [LawfulMonadLiftT n o] {f : β → n (Option γ)} {g : δ → γ → o δ} {init : δ}
  {it : Std.Iter β} {P : Pred} {Q : δ → Pred} {eQ : EPred},
  ⦃ P ⦄
      Std.Iter.foldM
        (fun d b => do
          let __x ← liftM (f b)
          match __x with
            | some c => g d c
            | x => pure d)
        init it ⦃
      Q; eQ ⦄ →
    ⦃ P ⦄ Std.IterM.foldM g init (Std.Iter.filterMapM f it) ⦃ Q; eQ ⦄
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_erase_lt : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p ≠ 0 → (Polynomial.erase p.natDegree p).degree < p.degree
-- Init.Data.Nat.Basic
Nat.pred_le_iff_le_succ : ∀ {n : ℕ} {m : ℕ}, n.pred ≤ m ↔ n ≤ m.succ
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Matrix.IsElliptic.b_ne_zero : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [IsOrderedRing R] {m : Matrix (Fin 2) (Fin 2) R},
  m.IsElliptic → m 0 1 ≠ 0
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.coe_zero : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  (ρ : Representation A G V) (σ : Representation A G W), ⇑0 = 0
-- Mathlib.Tactic.Ring.Compare
Mathlib.Tactic.Ring.ExceptType.notComparable : Mathlib.Tactic.Ring.ExceptType