mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.SInt.Lemmas
Int64.toNatClampNeg_ofIntTruncate_of_lt : ∀ {n : ℤ}, n < 2 ^ 63 → (Int64.ofIntClamp n).toNatClampNeg = n.toNat
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.refl_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C),
  (CategoryTheory.Iso.refl X).inv = CategoryTheory.CategoryStruct.id X
-- Mathlib.Data.Num.Lemmas
_private.Mathlib.Data.Num.Lemmas.0.PosNum.pred'.match_1.splitter : (motive : PosNum → Sort u_1) →
  (x : PosNum) → (Unit → motive PosNum.one) → ((n : PosNum) → motive n.bit0) → ((n : PosNum) → motive n.bit1) → motive x
-- Mathlib.NumberTheory.LSeries.HurwitzZeta
/-- The Hurwitz zeta function is differentiable away from `s = 1`.  -/
HurwitzZeta.differentiableAt_hurwitzZeta : ∀ (a : UnitAddCircle) {s : ℂ}, s ≠ 1 → DifferentiableAt ℂ (HurwitzZeta.hurwitzZeta a) s
-- Mathlib.RingTheory.HahnSeries.Cardinal
HahnSeries.coe_cardSuppLTAddSubmonoid : ∀ (Γ : Type u_1) (R : Type u_2) (κ : Cardinal.{u_1}) [inst : PartialOrder Γ] [inst_1 : AddMonoid R]
  [hκ : Fact (Cardinal.aleph0 ≤ κ)], ↑(HahnSeries.cardSuppLTAddSubmonoid Γ R κ) = {x | x.cardSupp < κ}
-- Mathlib.CategoryTheory.Galois.Full
CategoryTheory.Limits.PreservesCoproduct.iso.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) [inst_2 : CategoryTheory.Limits.HasCoproduct f]
  [inst_3 : CategoryTheory.Limits.HasCoproduct fun j => G.obj (f j)]
  [inst_4 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Discrete.functor f) G],
  CategoryTheory.Limits.PreservesCoproduct.iso G f = CategoryTheory.Limits.PreservesCoproduct.iso G f
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- A multiple of the difference between two points (reversed) lies in their `vectorSpan`.  -/
smul_vsub_rev_mem_vectorSpan_pair : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (r : k) (p₁ p₂ : P), r • (p₂ -ᵥ p₁) ∈ vectorSpan k {p₁, p₂}
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
Int.reduceDvd : Lean.Meta.Simp.Simproc
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
/-- If `μ` has finite spanning sets in `C` and `C ∩ {s | μ s < ∞} ⊆ D` then `μ` has finite spanning
sets in `D`.  -/
MeasureTheory.Measure.FiniteSpanningSetsIn.mono' : {α : Type u_1} →
  {m0 : MeasurableSpace α} →
    {μ : MeasureTheory.Measure α} →
      {C D : Set (Set α)} → μ.FiniteSpanningSetsIn C → C ∩ {s | μ s < ⊤} ⊆ D → μ.FiniteSpanningSetsIn D
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Splitting.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} (r : S.X₂ ⟶ S.X₁) (s : S.X₃ ⟶ S.X₂)
  (f_r :
    autoParam (CategoryTheory.CategoryStruct.comp S.f r = CategoryTheory.CategoryStruct.id S.X₁)
      CategoryTheory.ShortComplex.Splitting.f_r._autoParam)
  (s_g :
    autoParam (CategoryTheory.CategoryStruct.comp s S.g = CategoryTheory.CategoryStruct.id S.X₃)
      CategoryTheory.ShortComplex.Splitting.s_g._autoParam)
  (id :
    autoParam
      (CategoryTheory.CategoryStruct.comp r S.f + CategoryTheory.CategoryStruct.comp S.g s =
        CategoryTheory.CategoryStruct.id S.X₂)
      CategoryTheory.ShortComplex.Splitting.id._autoParam)
  (r_1 : S.X₂ ⟶ S.X₁) (s_1 : S.X₃ ⟶ S.X₂)
  (f_r_1 :
    autoParam (CategoryTheory.CategoryStruct.comp S.f r_1 = CategoryTheory.CategoryStruct.id S.X₁)
      CategoryTheory.ShortComplex.Splitting.f_r._autoParam)
  (s_g_1 :
    autoParam (CategoryTheory.CategoryStruct.comp s_1 S.g = CategoryTheory.CategoryStruct.id S.X₃)
      CategoryTheory.ShortComplex.Splitting.s_g._autoParam)
  (id_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp r_1 S.f + CategoryTheory.CategoryStruct.comp S.g s_1 =
        CategoryTheory.CategoryStruct.id S.X₂)
      CategoryTheory.ShortComplex.Splitting.id._autoParam),
  ({ r := r, s := s, f_r := f_r, s_g := s_g, id := id } =
      { r := r_1, s := s_1, f_r := f_r_1, s_g := s_g_1, id := id_1 }) =
    (r = r_1 ∧ s = s_1)
-- Mathlib.Analysis.SpecialFunctions.Arsinh
Real.arsinh_pos_iff : ∀ {x : ℝ}, 0 < Real.arsinh x ↔ 0 < x
-- Mathlib.Combinatorics.Enumerative.Stirling
_private.Mathlib.Combinatorics.Enumerative.Stirling.0.Nat.stirlingFirst.match_1.eq_2 : ∀ (motive : ℕ → ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0 0) (h_2 : (n : ℕ) → motive 0 n.succ)
  (h_3 : (n : ℕ) → motive n.succ 0) (h_4 : (n k : ℕ) → motive n.succ k.succ),
  (match 0, n.succ with
    | 0, 0 => h_1 ()
    | 0, n.succ => h_2 n
    | n.succ, 0 => h_3 n
    | n.succ, k.succ => h_4 n k) =
    h_2 n
-- Mathlib.Algebra.Lie.Submodule
/-- The `lieSpan` of a set `s ⊆ M` is the smallest Lie submodule of `M` that contains `s`.  -/
LieSubmodule.lieSpan : (R : Type u) →
  (L : Type v) →
    {M : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : AddCommGroup M] → [inst_3 : Module R M] → [inst_4 : LieRingModule L M] → Set M → LieSubmodule R L M
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get?_eq_some_get! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {a : α} [inst_1 : Inhabited (β a)], a ∈ t → t.get? a = some (t.get! a)
-- Mathlib.Order.Filter.SmallSets
/-- **Alias** of the reverse direction of `Filter.tendsto_image_smallSets`. -/
Filter.Tendsto.image_smallSets : ∀ {α : Type u_1} {β : Type u_2} {la : Filter α} {lb : Filter β} {f : α → β},
  Filter.Tendsto f la lb → Filter.Tendsto (fun x => f '' x) la.smallSets lb.smallSets
-- Mathlib.Data.Finset.Image
Disjoint.of_image_finset : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {s t : Finset α} {f : α → β},
  Disjoint (Finset.image f s) (Finset.image f t) → Disjoint s t
-- Mathlib.Data.ENNReal.Inv
ENNReal.iSup_mul : ∀ {ι : Sort u_1} (f : ι → ENNReal) (a : ENNReal), (⨆ i, f i) * a = ⨆ i, f i * a
-- Mathlib.ModelTheory.Syntax
/-- Maps a formula's symbols along a language equivalence.  -/
FirstOrder.Language.LEquiv.onFormula : {L : FirstOrder.Language} → {L' : FirstOrder.Language} → {α : Type u'} → (L ≃ᴸ L') → L.Formula α ≃ L'.Formula α
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
ENNReal.continuous_exp : Continuous EReal.exp
-- Mathlib.Topology.VectorBundle.Basic
/-- Topological structure on the total space of a vector bundle created from core, designed so
that all the local trivialization are continuous.  -/
VectorBundleCore.toTopologicalSpace : {R : Type u_1} →
  {B : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField R] →
        [inst_1 : NormedAddCommGroup F] →
          [inst_2 : NormedSpace R F] →
            [inst_3 : TopologicalSpace B] →
              {ι : Type u_5} → (Z : VectorBundleCore R B F ι) → TopologicalSpace Z.TotalSpace
-- Mathlib.GroupTheory.Coset.Card
QuotientAddGroup.card_quotient_rightRel : ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) [inst_1 : Fintype (α ⧸ s)],
  Fintype.card (Quotient (QuotientAddGroup.rightRel s)) = Fintype.card (α ⧸ s)
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Algebra.IsIntegral.nontrivial_heightOneSpectrum : ∀ (R : Type u_1) (A : Type u_2) [inst : CommRing R] [inst_1 : CommRing A] [IsDomain A] [inst_3 : Algebra R A]
  [FaithfulSMul R A] [Algebra.IsIntegral R A] [Nontrivial (IsDedekindDomain.HeightOneSpectrum R)],
  Nontrivial (IsDedekindDomain.HeightOneSpectrum A)
-- Mathlib.CategoryTheory.Products.Basic
/-- The product `F.prod' G` followed by projection on the first component is isomorphic to `F`  -/
CategoryTheory.Functor.prod'CompFst : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            (F : CategoryTheory.Functor A B) →
              (G : CategoryTheory.Functor A C) → (F.prod' G).comp (CategoryTheory.Prod.fst B C) ≅ F
-- Mathlib.Topology.Sober
genericPoints.ofComponent_component : ∀ {α : Type u_1} [inst : TopologicalSpace α] [T0Space α] [inst_2 : QuasiSober α] (x : ↑(genericPoints α)),
  genericPoints.ofComponent (genericPoints.component x) = x
-- Mathlib.FieldTheory.RatFunc.Luroth
RatFunc.Luroth.adjoin_generator_le : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)}, K⟮RatFunc.Luroth.generator E⟯ ≤ E
-- Mathlib.Order.ScottContinuity
ScottContinuous.scottContinuousOn : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {D : Set (Set α)},
  ScottContinuous f → ScottContinuousOn D f
-- Mathlib.Topology.UniformSpace.UniformConvergence
/-- Uniform convergence on a set `s` to a constant function is equivalent to convergence in
`p ×ˢ 𝓟 s`.  -/
tendsto_prod_principal_iff : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {s : Set α} {p : Filter ι}
  {c : β}, Filter.Tendsto (↿F) (p ×ˢ Filter.principal s) (nhds c) ↔ TendstoUniformlyOn F (fun x => c) p s
-- Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Polynomial.Monic.isEisensteinAt_of_mem_of_notMem : ∀ {R : Type u} [inst : CommSemiring R] {𝓟 : Ideal R} {f : Polynomial R},
  f.Monic → 𝓟 ≠ ⊤ → (∀ {n : ℕ}, n < f.natDegree → f.coeff n ∈ 𝓟) → f.coeff 0 ∉ 𝓟 ^ 2 → f.IsEisensteinAt 𝓟
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.mk'_add_cancel_right : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N) (x : M) (y : ↥S), f.mk' (x + ↑y) y = f x
-- Init.Data.Nat.Basic
Nat.zero_add : ∀ (n : ℕ), 0 + n = n
-- Mathlib.MeasureTheory.Measure.Trim
MeasureTheory.trim_eq_self : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}, μ.trim ⋯ = μ
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.RxoIterator.step.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} [inst : Ord α] (motive : Std.DTreeMap.Internal.RxoIterator α β → Sort u_3)
  (upper : α) (h_1 : (upper : α) → motive { iter := Std.DTreeMap.Internal.Zipper.done, upper := upper })
  (h_2 :
    (k : α) →
      (v : β k) →
        (t : Std.DTreeMap.Internal.Impl α β) →
          (it : Std.DTreeMap.Internal.Zipper α β) →
            (upper : α) → motive { iter := Std.DTreeMap.Internal.Zipper.cons k v t it, upper := upper }),
  (match { iter := Std.DTreeMap.Internal.Zipper.done, upper := upper } with
    | { iter := Std.DTreeMap.Internal.Zipper.done, upper := upper } => h_1 upper
    | { iter := Std.DTreeMap.Internal.Zipper.cons k v t it, upper := upper } => h_2 k v t it upper) =
    h_1 upper
-- Mathlib.Algebra.Homology.SpectralObject.Differentials
CategoryTheory.Abelian.SpectralObject.toCycles_πE_d_assoc : ∀ {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₀ i₁ i₂ i₃ i₄ i₅ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) (f₃₄ : i₂ ⟶ i₄)
  (h₃₄ : CategoryTheory.CategoryStruct.comp f₃ f₄ = f₃₄) (n₀ n₁ n₂ n₃ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.toCycles_πE_d._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.toCycles_πE_d._auto_3)
  (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.toCycles_πE_d._auto_5) {Z : C}
  (h : X.E f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.toCycles f₃ f₄ f₃₄ h₃₄ n₁)
      (CategoryTheory.CategoryStruct.comp (X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂)
        (CategoryTheory.CategoryStruct.comp (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃) h)) =
    CategoryTheory.CategoryStruct.comp (X.δ f₁₂ f₃₄ n₁ n₂ hn₂)
      (CategoryTheory.CategoryStruct.comp (X.toCycles f₁ f₂ f₁₂ h₁₂ n₂)
        (CategoryTheory.CategoryStruct.comp (X.πE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃) h))
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.union_eq : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], m₁.union m₂ = m₁ ∪ m₂
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- commutation with `π`  -/
CategoryTheory.ShortComplex.LeftHomologyMapData.commπ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData}
  (self : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂),
  CategoryTheory.CategoryStruct.comp h₁.π self.φH = CategoryTheory.CategoryStruct.comp self.φK h₂.π
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.MemLp.integrable_mul : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_8} [inst : NormedRing 𝕜]
  {p q : ENNReal} {f g : α → 𝕜},
  MeasureTheory.MemLp f p μ → MeasureTheory.MemLp g q μ → ∀ [p.HolderTriple q 1], MeasureTheory.Integrable (f * g) μ
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- Part of 7.64(d) in [axler2024].  -/
LinearMap.finrank_range_adjoint : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : FiniteDimensional 𝕜 E] [inst_6 : FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F),
  Module.finrank 𝕜 ↥(LinearMap.adjoint A).range = Module.finrank 𝕜 ↥A.range
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKeyD_diff_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k fallback : α}, k ∉ m₂ → (m₁ \ m₂).getKeyD k fallback = m₁.getKeyD k fallback
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Expr.toPolyC.go.match_4.eq_3 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (k : ℤ) (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k))
  (h_2 : (k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k))
  (h_3 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k))
  (h_4 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_5 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_6 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b)) (h_7 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_8 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b))
  (h_9 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k)),
  (match Lean.Grind.CommRing.Expr.intCast k with
    | Lean.Grind.CommRing.Expr.num k => h_1 k
    | Lean.Grind.CommRing.Expr.natCast k => h_2 k
    | Lean.Grind.CommRing.Expr.intCast k => h_3 k
    | Lean.Grind.CommRing.Expr.var x => h_4 x
    | a.add b => h_5 a b
    | a.mul b => h_6 a b
    | a.neg => h_7 a
    | a.sub b => h_8 a b
    | a.pow k => h_9 a k) =
    h_3 k
-- Mathlib.Geometry.Manifold.Notation
/-- Delaborator for `mfderivWithin` using the custom elaborator, and special-casing
arguments that can use the `T%` elaborator.  -/
Manifold.delabMFDerivWithin : Lean.PrettyPrinter.Delaborator.Delab
-- Lean.Data.Trie
_private.Lean.Data.Trie.0.Lean.Data.Trie.upsert.loop : {α : Type} → String → (Option α → α) → ℕ → Lean.Data.Trie α → Lean.Data.Trie α
-- Lean.Elab.DefView
/-- Full name for this declaration. This is the name that will be added to the `Environment`.  -/
Lean.Elab.DefViewElabHeaderData.declName : Lean.Elab.DefViewElabHeaderData → Lean.Name
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.memL1_smul_of_L1_withDensity : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_8} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {f : α → NNReal},
  Measurable f →
    ∀ (u : ↥(MeasureTheory.Lp E 1 (μ.withDensity fun x => ↑(f x)))), MeasureTheory.MemLp (fun x => f x • ↑↑u x) 1 μ
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.XXIsoOfEq.congr_simp : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (K : HomologicalComplex₂ C c₁ c₂)
  {x₁ y₁ : I₁} (h₁ : x₁ = y₁) {x₂ y₂ : I₂} (h₂ : x₂ = y₂),
  HomologicalComplex₂.XXIsoOfEq C c₁ c₂ K h₁ h₂ = HomologicalComplex₂.XXIsoOfEq C c₁ c₂ K h₁ h₂
-- Mathlib.CategoryTheory.EqToHom
/-- See the note on `eqToHom_map` regarding using this as a `simp` lemma.
 -/
CategoryTheory.eqToIso_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : C} (p : X = Y), F.mapIso (CategoryTheory.eqToIso p) = CategoryTheory.eqToIso ⋯
-- Mathlib.Topology.Separation.Basic
instR1SpaceForall : ∀ {ι : Type u_3} {X : ι → Type u_4} [inst : (i : ι) → TopologicalSpace (X i)] [∀ (i : ι), R1Space (X i)],
  R1Space ((i : ι) → X i)
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.Waiter.isRoot : Lean.Meta.SynthInstance.Waiter → Bool
-- Init.Data.String.PosRaw
/-- Advances `p` by `n` bytes. This is not an `HAdd` instance because it should be a relatively
rare operation, so we use a name to make accidental use less likely. To add the size of a
character `c` or string `s` to a raw position `p`, you can use `p + c` resp. `p + s`.

This should be seen as an "advance" or "skip".

See also `Pos.Raw.offsetBy`, which turns relative positions into absolute positions.
 -/
String.Pos.Raw.increaseBy : String.Pos.Raw → ℕ → String.Pos.Raw
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpEntry.thm.injEq : ∀ (a a_1 : Lean.Meta.SimpTheorem), (Lean.Meta.SimpEntry.thm a = Lean.Meta.SimpEntry.thm a_1) = (a = a_1)
-- Mathlib.LinearAlgebra.Prod
Submodule.fst_inf_snd : ∀ (R : Type u) (M : Type v) (M₂ : Type w) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂], Submodule.fst R M M₂ ⊓ Submodule.snd R M M₂ = ⊥
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.toBasis_singleton : ∀ {ι : Type u_7} {𝕜 : Type u_8} [inst : Unique ι] [inst_1 : RCLike 𝕜],
  (OrthonormalBasis.singleton ι 𝕜).toBasis = Module.Basis.singleton ι 𝕜
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- Equivalence between linear maps `M₂ →ₗ[R] M₃` and one-multilinear maps.  -/
MultilinearMap.ofSubsingleton : (R : Type uR) →
  {ι : Type uι} →
    (M₂ : Type v₂) →
      (M₃ : Type v₃) →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M₂] →
            [inst_2 : AddCommMonoid M₃] →
              [inst_3 : Module R M₂] →
                [inst_4 : Module R M₃] → [Subsingleton ι] → ι → (M₂ →ₗ[R] M₃) ≃ MultilinearMap R (fun x => M₂) M₃
-- Mathlib.Order.Filter.Pointwise
Filter.map_vadd : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {f : Filter β} {a : α}, Filter.map (fun b => a +ᵥ b) f = a +ᵥ f
-- Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
RootPairing.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed' : ∀ {ι : 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) [Finite ι]
  [CharZero R] [inst_7 : P.IsCrystallographic] (i j : ι) [IsDomain R] [P.IsReduced],
  P.root i ≠ P.root j →
    P.root i ≠ -P.root j →
      (P.pairingIn ℤ i j, P.pairingIn ℤ j i) ∈
        {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.SavedState.term : Lean.Elab.Tactic.Grind.SavedState → Lean.Elab.Term.SavedState
-- Lean.Meta.Sym.Simp.SimpM
/-- Saves and restores the transient cache and funext, leaving
the persistent cache untouched. Used when entering binders.  -/
Lean.Meta.Sym.Simp.withFreshTransientCache : {α : Type} → Lean.Meta.Sym.Simp.SimpM α → Lean.Meta.Sym.Simp.SimpM α
-- Mathlib.Order.Hom.Basic
OrderHom.toFun_eq_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : α →o β), f.toFun = ⇑f
-- Mathlib.GroupTheory.GroupAction.Hom
Pi.evalAddActionHom_apply : ∀ {ι : Type u_1} {M : Type u_2} {X : ι → Type u_3} [inst : (i : ι) → VAdd M (X i)] (i : ι) (f : (x : ι) → X x),
  (Pi.evalAddActionHom i) f = Function.eval i f
-- Mathlib.Topology.SmallInductiveDimension
smallInductiveDimension_lt : ∀ (X : Type u_1) [inst : TopologicalSpace X] (n : ℕ) [H : HasSmallInductiveDimensionLT X n],
  smallInductiveDimension X < ↑n
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.mapCoconeInvMapCocone.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J D}
  (H : CategoryTheory.Functor D C) [inst_3 : H.IsEquivalence] (c : CategoryTheory.Limits.Cocone F),
  CategoryTheory.Functor.mapCoconeInvMapCocone H c =
    (CategoryTheory.Limits.Cocone.functorialityEquivalence F H.asEquivalence).unitIso.symm.app c
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.MsgEmbed.trace.inj : ∀ {indent : ℕ} {cls : Lean.Name} {msg : Lean.Widget.TaggedText Lean.Widget.MsgEmbed} {collapsed : Bool}
  {children :
    Lean.Widget.StrictOrLazy (Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed))
      (Lean.Server.WithRpcRef Lean.Widget.LazyTraceChildren)}
  {indent_1 : ℕ} {cls_1 : Lean.Name} {msg_1 : Lean.Widget.TaggedText Lean.Widget.MsgEmbed} {collapsed_1 : Bool}
  {children_1 :
    Lean.Widget.StrictOrLazy (Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed))
      (Lean.Server.WithRpcRef Lean.Widget.LazyTraceChildren)},
  Lean.Widget.MsgEmbed.trace indent cls msg collapsed children =
      Lean.Widget.MsgEmbed.trace indent_1 cls_1 msg_1 collapsed_1 children_1 →
    indent = indent_1 ∧ cls = cls_1 ∧ msg = msg_1 ∧ collapsed = collapsed_1 ∧ children = children_1
-- Mathlib.Analysis.Analytic.Order
/-- If an analytic function `f` is not constantly zero on `𝕜`, then its set of zeros is codiscrete.

See `AnalyticOnNhd.preimage_mem_codiscreteWithin` for a more general statement in preimages of
codiscrete sets.
 -/
AnalyticOnNhd.preimage_zero_mem_codiscrete : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} [ConnectedSpace 𝕜] {x : 𝕜},
  AnalyticOnNhd 𝕜 f Set.univ → f x ≠ 0 → f ⁻¹' {0}ᶜ ∈ Filter.codiscrete 𝕜
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_comm : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (X Y : Ω → ℝ) {μ : MeasureTheory.Measure Ω},
  ProbabilityTheory.covariance X Y μ = ProbabilityTheory.covariance Y X μ
-- Mathlib.Analysis.BoxIntegral.Basic
/-- If `f` is integrable on a box `I` along `l`, then for any fixed subset `s` of `I` that can be
represented as a finite union of boxes, the integral sums of `f` over tagged prepartitions that
cover exactly `s` form a Cauchy “sequence” along `l`.  -/
BoxIntegral.Integrable.cauchy_map_integralSum_toFilteriUnion : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
  {l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤},
  BoxIntegral.Integrable I l f vol →
    ∀ (π₀ : BoxIntegral.Prepartition I),
      Cauchy (Filter.map (BoxIntegral.integralSum f vol) (BoxIntegral.IntegrationParams.toFilteriUnion I π₀))