mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.comp_assoc : ∀ {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [inst : SeminormedAddCommGroup V₁]
  [inst_1 : SeminormedAddCommGroup V₂] [inst_2 : SeminormedAddCommGroup V₃] {V₄ : Type u_5}
  [inst_3 : SeminormedAddCommGroup V₄] (h : NormedAddGroupHom V₃ V₄) (g : NormedAddGroupHom V₂ V₃)
  (f : NormedAddGroupHom V₁ V₂), (h.comp g).comp f = h.comp (g.comp f)
-- Mathlib.Order.Heyting.Basic
GeneralizedCoheytingAlgebra.toSDiff : {α : Type u_4} → [self : GeneralizedCoheytingAlgebra α] → SDiff α
-- Lean.Environment
Lean.PersistentEnvExtensionDescr.mk.injEq : ∀ {α β σ : Type} (toPersistentEnvExtensionDescrCore : Lean.PersistentEnvExtensionDescrCore α β σ)
  (exportEntriesFn : σ → Array α) (toPersistentEnvExtensionDescrCore_1 : Lean.PersistentEnvExtensionDescrCore α β σ)
  (exportEntriesFn_1 : σ → Array α),
  ({ toPersistentEnvExtensionDescrCore := toPersistentEnvExtensionDescrCore, exportEntriesFn := exportEntriesFn } =
      { toPersistentEnvExtensionDescrCore := toPersistentEnvExtensionDescrCore_1,
        exportEntriesFn := exportEntriesFn_1 }) =
    (toPersistentEnvExtensionDescrCore = toPersistentEnvExtensionDescrCore_1 ∧ exportEntriesFn = exportEntriesFn_1)
-- Mathlib.Topology.Bornology.Absorbs
Set.Finite.absorbs_biUnion : ∀ {M : Type u_1} {α : Type u_2} [inst : Bornology M] [inst_1 : SMul M α] {s : Set α} {ι : Type u_3} {t : ι → Set α}
  {I : Set ι}, I.Finite → (Absorbs M s (⋃ i ∈ I, t i) ↔ ∀ i ∈ I, Absorbs M s (t i))
-- Mathlib.Analysis.Normed.Module.Bases
/-- The projection norms are bounded above in a complete space.  -/
SchauderBasis.bddAbove_range_nnnorm_proj : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {X : Type u_2} [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] (b : SchauderBasis 𝕜 X) [CompleteSpace X], BddAbove (Set.range fun n => ‖b.proj n‖₊)
-- Mathlib.Tactic.Simps.Basic
Simps.ProjectionRule.prefix.sizeOf_spec : ∀ (a : Lean.Name) (a_1 : Lean.Syntax), sizeOf (Simps.ProjectionRule.prefix a a_1) = 1 + sizeOf a + sizeOf a_1
-- Mathlib.Topology.Algebra.Nonarchimedean.Completion
/-- The completion of a nonarchimedean additive group is a nonarchimedean additive group.  -/
instNonarchimedeanAddGroupCompletion : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : UniformSpace G] [inst_2 : IsUniformAddGroup G]
  [NonarchimedeanAddGroup G], NonarchimedeanAddGroup (UniformSpace.Completion G)
-- Mathlib.Order.Filter.NAry
Filter.map₂_right_comm : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {δ' : Type u_8} {ε : Type u_9} {f : Filter α}
  {g : Filter β} {h : Filter γ} {m : δ → γ → ε} {n : α → β → δ} {m' : α → γ → δ'} {n' : δ' → β → ε},
  (∀ (a : α) (b : β) (c : γ), m (n a b) c = n' (m' a c) b) →
    Filter.map₂ m (Filter.map₂ n f g) h = Filter.map₂ n' (Filter.map₂ m' f h) g
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.le_of_mul_le_mul_left : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] (a b c : Associates M), a ≠ 0 → a * b ≤ a * c → b ≤ c
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.cospanExt_app_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z X' Y' Z' : C} (iX : X ≅ X') (iY : Y ≅ Y') (iZ : Z ≅ Z')
  {f : X ⟶ Z} {g : Y ⟶ Z} {f' : X' ⟶ Z'} {g' : Y' ⟶ Z'}
  (wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iZ.hom)
  (wg : CategoryTheory.CategoryStruct.comp iY.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom),
  (CategoryTheory.Limits.cospanExt iX iY iZ wf wg).app CategoryTheory.Limits.WalkingCospan.right = iY
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.coe_prod : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : StarRing A]
  [inst_3 : Module R A] [inst_4 : NonUnitalSemiring B] [inst_5 : StarRing B] [inst_6 : Module R B]
  (S : NonUnitalStarSubalgebra R A) (S₁ : NonUnitalStarSubalgebra R B), ↑(S.prod S₁) = ↑S ×ˢ ↑S₁
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.isTriangulated_iff_comp_right : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : CategoryTheory.HasShift D ℤ] [inst_5 : CategoryTheory.HasShift E ℤ]
  [inst_6 : CategoryTheory.Limits.HasZeroObject C] [inst_7 : CategoryTheory.Limits.HasZeroObject D]
  [inst_8 : CategoryTheory.Limits.HasZeroObject E] [inst_9 : CategoryTheory.Preadditive C]
  [inst_10 : CategoryTheory.Preadditive D] [inst_11 : CategoryTheory.Preadditive E]
  [inst_12 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_13 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive]
  [inst_14 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor E n).Additive] [inst_15 : CategoryTheory.Pretriangulated C]
  [inst_16 : CategoryTheory.Pretriangulated D] [inst_17 : CategoryTheory.Pretriangulated E]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} {H : CategoryTheory.Functor C E} (e : F.comp G ≅ H)
  [inst_18 : F.CommShift ℤ] [inst_19 : G.CommShift ℤ] [inst_20 : H.CommShift ℤ]
  [CategoryTheory.NatTrans.CommShift e.hom ℤ] [G.IsTriangulated] [G.Full] [G.Faithful],
  F.IsTriangulated ↔ H.IsTriangulated
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_natAdd_Ico_natAdd : ∀ {n : ℕ} (m : ℕ) (i j : Fin n), Fin.natAdd m ⁻¹' Set.Ico (Fin.natAdd m i) (Fin.natAdd m j) = Set.Ico i j
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.domExtend_baseSet : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  {s : Set B} (e : Bundle.Pretrivialization F fun z => proj ↑z) [inst_2 : Nonempty (Z → F)],
  e.domExtend.baseSet = e.baseSet
-- Mathlib.Algebra.Order.Nonneg.Lattice
Nonneg.noMaxOrder : ∀ {α : Type u_1} [inst : PartialOrder α] [NoMaxOrder α] {a : α}, NoMaxOrder { x // a ≤ x }
-- Mathlib.Algebra.Group.Submonoid.Pointwise
/-- The additive submonoid with every element negated.  -/
AddSubmonoid.neg : {G : Type u_2} → [inst : AddGroup G] → Neg (AddSubmonoid G)
-- Mathlib.Topology.Order
generateFrom_insert_univ : ∀ {α : Type u_1} {s : Set (Set α)}, TopologicalSpace.generateFrom (insert Set.univ s) = TopologicalSpace.generateFrom s
-- Mathlib.Data.LawfulXor.Basic
instLawfulXorBitVec : ∀ {w : ℕ}, LawfulXor (BitVec w)
-- Mathlib.Algebra.Quandle
/-- The type of homomorphisms between shelves.
This is also the notion of rack and quandle homomorphisms.
 -/
ShelfHom : (S₁ : Type u_1) → (S₂ : Type u_2) → [Shelf S₁] → [Shelf S₂] → Type (max u_1 u_2)
-- Mathlib.Data.Finset.Sort
Finset.length_sort : ∀ {α : Type u_1} {s : Finset α} (r : α → α → Prop) [inst : DecidableRel r] [inst_1 : IsTrans α r]
  [inst_2 : Std.Antisymm r] [inst_3 : Std.Total r], (s.sort r).length = s.card
-- Mathlib.Computability.StateTransition
StateTransition.FRespects.eq_2 : ∀ {σ₁ : Type u_1} {σ₂ : Type u_2} (f₂ : σ₂ → Option σ₂) (tr : σ₁ → σ₂) (a₂ : σ₂),
  StateTransition.FRespects f₂ tr a₂ none = (f₂ a₂ = none)
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.isUniformEmbedding_equivBoundedOfCompact : ∀ (α : Type u_1) (β : Type u_2) [inst : TopologicalSpace α] [inst_1 : CompactSpace α] [inst_2 : PseudoMetricSpace β],
  IsUniformEmbedding ⇑(ContinuousMap.equivBoundedOfCompact α β)
-- Init.Data.String.Extra
_private.Init.Data.String.Extra.0.String.findLeadingSpacesSize : String → ℕ
-- Mathlib.Topology.Semicontinuity.Basic
Continuous.comp_lowerSemicontinuous : ∀ {α : Type u_1} [inst : TopologicalSpace α] {γ : Type u_4} [inst_1 : LinearOrder γ] [inst_2 : TopologicalSpace γ]
  [OrderTopology γ] {δ : Type u_5} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderTopology δ] {g : γ → δ}
  {f : α → γ}, Continuous g → LowerSemicontinuous f → Monotone g → LowerSemicontinuous (g ∘ f)
-- Mathlib.RingTheory.AdicCompletion.Exactness
_private.Mathlib.RingTheory.AdicCompletion.Exactness.0.AdicCompletion.mapPreimageDelta.congr_simp : ∀ {R : Type u} [inst : CommRing R] {I : Ideal R} {M : Type v} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type w} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {f : M →ₗ[R] N} (hf : Function.Surjective ⇑f)
  (x x_1 : AdicCompletion.AdicCauchySequence I N) (e_x : x = x_1) {n : ℕ} {y yₙ : M} (hy : f y = ↑x (n + 1))
  (hyₙ : f yₙ = ↑x n), AdicCompletion.mapPreimageDelta✝ hf x hy hyₙ = AdicCompletion.mapPreimageDelta✝ hf x_1 ⋯ ⋯
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.smul_single' : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (r' : R) (m : M) (r : R),
  r' • MonoidAlgebra.single m r = MonoidAlgebra.single m (r' * r)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.intervalIntegral_conj : ∀ {𝕜 : Type u_8} [inst : RCLike 𝕜] {f : ℝ → 𝕜} {a b : ℝ} {μ : MeasureTheory.Measure ℝ},
  ∫ (x : ℝ) in a..b, (starRingEnd 𝕜) (f x) ∂μ = (starRingEnd 𝕜) (∫ (x : ℝ) in a..b, f x ∂μ)
-- Plausible.Testable
Plausible.instInhabitedTestResult.default : {p : Prop} → Plausible.TestResult p
-- Init.Data.String.Basic
/-- Advances a valid position on a string to the next valid position, given a proof that the
position is not the past-the-end position, which guarantees that such a position exists.  -/
String.Pos.next : {s : String} → (pos : s.Pos) → pos ≠ s.endPos → s.Pos
-- Mathlib.Data.Finset.NoncommProd
Multiset.noncommFold_eq_fold : ∀ {α : Type u_3} (op : α → α → α) [assoc : Std.Associative op] (s : Multiset α) [inst : Std.Commutative op] (a : α),
  Multiset.noncommFold op s ⋯ a = Multiset.fold op a s
-- Lean.Meta.Tactic.Grind.Theorems
Lean.Meta.Grind.Origin.pp : Lean.Meta.Grind.Origin → Lean.MessageData
-- Mathlib.Geometry.Manifold.ContMDiffMFDeriv
/-- The canonical equivalence between the product of tangent bundles and the tangent bundle of a
product is smooth.  -/
contMDiff_equivTangentBundleProd_symm : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] [inst_11 : IsManifold I 1 M]
  [inst_12 : IsManifold I' 1 M'],
  ContMDiff (I.tangent.prod I'.tangent) (I.prod I').tangent n ⇑(equivTangentBundleProd I M I' M').symm
-- Mathlib.Algebra.Homology.ModelCategory.Injective
CochainComplex.Plus.modelCategoryQuillen.instHasFactorizationTrivialCofibrationsFibrations : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [CategoryTheory.EnoughInjectives C],
  (HomotopicalAlgebra.trivialCofibrations (CochainComplex.Plus C)).HasFactorization
    (HomotopicalAlgebra.fibrations (CochainComplex.Plus C))
-- Mathlib.RingTheory.Polynomial.ContentIdeal
Polynomial.contentIdeal_mul_le_mul_contentIdeal : ∀ {R : Type u_1} [inst : Semiring R] (p q : Polynomial R), (p * q).contentIdeal ≤ p.contentIdeal * q.contentIdeal
-- Lean.Elab.Util
Lean.Elab.mkMacroAttributeUnsafe : Lean.Name → IO (Lean.KeyedDeclsAttribute Lean.Macro)
-- Mathlib.Order.Interval.Finset.Basic
Finset.Icc_map_sectR : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] [inst_4 : DecidableLE (α × β)] (c : α) (a b : β),
  Finset.map (Function.Embedding.sectR c β) (Finset.Icc a b) = Finset.Icc (c, a) (c, b)
-- Mathlib.RingTheory.Algebraic.Basic
transcendental_algebraMap_iff : ∀ {R : Type u} {S : Type u_1} {A : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Ring A]
  [inst_3 : Algebra R A] [inst_4 : Algebra R S] [inst_5 : Algebra S A] [IsScalarTower R S A] {a : S},
  Function.Injective ⇑(algebraMap S A) → (Transcendental R ((algebraMap S A) a) ↔ Transcendental R a)
-- Mathlib.RingTheory.DedekindDomain.Factorization
/-- `val_v(I)` does not depend on the choice of `a` and `J` used to represent `I`.  -/
FractionalIdeal.count_well_defined : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
  {I : FractionalIdeal (nonZeroDivisors R) K},
  I ≠ 0 →
    ∀ {a : R} {J : Ideal R},
      I = FractionalIdeal.spanSingleton (nonZeroDivisors R) ((algebraMap R K) a)⁻¹ * ↑J →
        FractionalIdeal.count K v I =
          ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
            ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)
-- Init.Data.List.Basic
List.intersperse_eq_intersperseTR : @List.intersperse = @List.intersperseTR
-- Init.Data.Nat.Lemmas
Nat.succ_mod_succ_eq_zero_iff : ∀ {a b : ℕ}, (a + 1) % (b + 1) = 0 ↔ a % (b + 1) = b
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.isPrefixOfAux.eq_def : ∀ {α : Type u} [inst : BEq α] (as bs : Array α) (hle : as.size ≤ bs.size) (i : ℕ),
  as.isPrefixOfAux bs hle i =
    if h : i < as.size then
      have a := as[i];
      have this := ⋯;
      have b := bs[i];
      if (a == b) = true then as.isPrefixOfAux bs hle (i + 1) else false
    else true
-- Mathlib.Data.Finset.Filter
Finset.filter_eq_self : ∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {s : Finset α}, Finset.filter p s = s ↔ ∀ x ∈ s, p x
-- Mathlib.Data.Seq.Defs
/-- member definition for `Seq`  -/
Stream'.Seq.Mem : {α : Type u} → Stream'.Seq α → α → Prop
-- Std.Data.HashMap.RawDecidableEquiv
Std.HashMap.Raw.instDecidableEquiv : {α : Type u} →
  {β : Type v} →
    [inst : BEq α] →
      [LawfulBEq α] →
        [inst_2 : Hashable α] →
          [inst_3 : BEq β] → [LawfulBEq β] → {m₁ m₂ : Std.HashMap.Raw α β} → m₁.WF → m₂.WF → Decidable (m₁.Equiv m₂)
-- Mathlib.Algebra.Homology.HomologySequenceLemmas
CategoryTheory.ShortComplex.ShortExact.acyclic_X₁ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)},
  S.ShortExact → QuasiIso S.g → S.X₁.Acyclic
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- If `(F', α)` is a right Kan extension of `F` along `L`, then this
is the induced bijection `(G ⟶ F') ≃ (L ⋙ G ⟶ F)` for all `G`.  -/
CategoryTheory.Functor.homEquivOfIsRightKanExtension : {C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} H] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} D] →
            (F' : CategoryTheory.Functor D H) →
              {L : CategoryTheory.Functor C D} →
                {F : CategoryTheory.Functor C H} →
                  (α : L.comp F' ⟶ F) →
                    [F'.IsRightKanExtension α] → (G : CategoryTheory.Functor D H) → (G ⟶ F') ≃ (L.comp G ⟶ F)
-- Lean.MetavarContext
/-- Similar to `Expr.abstractRange`, but handles metavariables correctly.
It uses `elimMVarDeps` to ensure `e` and the type of the free variables `xs` do not
contain a metavariable `?m` s.t. local context of `?m` contains a free variable in `xs`.
 -/
Lean.MetavarContext.MkBinding.abstractRange : Array Lean.Expr → ℕ → Lean.Expr → Lean.MetavarContext.MkBinding.M Lean.Expr
-- Mathlib.RingTheory.MvPowerSeries.LexOrder
MvPowerSeries.coeff_eq_zero_of_lt_lexOrder : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : LinearOrder σ] [inst_2 : WellFoundedGT σ]
  {φ : MvPowerSeries σ R} {d : σ →₀ ℕ}, ↑(toLex d) < φ.lexOrder → (MvPowerSeries.coeff d) φ = 0
-- Batteries.Data.Float.Lemmas
Float.nan_beq_eq_false : ∀ (f : Float), (Float.nan == f) = false
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.coe_centralizer : ∀ (R : Type u_2) {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] (s : Set A),
  ↑(StarSubalgebra.centralizer R s) = (s ∪ star s).centralizer
-- Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
/-- If `f` is a symmetric continuous bilinear map
taking values in the space of continuous alternating maps,
then the twice uncurried `f` is zero.  -/
ContinuousAlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinCLM_comp_of_symmetric : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ}
  {f : E →L[𝕜] E →L[𝕜] E [⋀^Fin n]→L[𝕜] F},
  (∀ (x y : E), (f x) y = (f y) x) →
    ContinuousAlternatingMap.alternatizeUncurryFin (ContinuousAlternatingMap.alternatizeUncurryFinCLM 𝕜 E F ∘SL f) = 0
-- Mathlib.MeasureTheory.Function.L2Space
MeasureTheory.MemLp.const_inner : ∀ {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {E : Type u_2} {𝕜 : Type u_3}
  [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (c : E) {f : α → E},
  MeasureTheory.MemLp f p μ → MeasureTheory.MemLp (fun a => inner 𝕜 c (f a)) p μ
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.coreflection_apply_self : ∀ {ι : 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) (i : ι),
  (P.coreflection i) (P.coroot i) = -P.coroot i
-- Mathlib.RingTheory.AdicCompletion.Basic
/-- To show a statement about an element of `adicCompletion I M`, it suffices to check it
on Cauchy sequences.  -/
AdicCompletion.induction_on : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {p : AdicCompletion I M → Prop} (x : AdicCompletion I M),
  (∀ (f : AdicCompletion.AdicCauchySequence I M), p ((AdicCompletion.mk I M) f)) → p x
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonDocumentColorOptions : Lean.FromJson Lean.Lsp.DocumentColorOptions
-- Mathlib.Analysis.Real.Sqrt
/-- Note: if you want to conclude `x ≤ √y`, then use `Real.le_sqrt_of_sq_le`.
If you have `x > 0`, consider using `Real.le_sqrt'`  -/
Real.le_sqrt : ∀ {x y : ℝ}, 0 ≤ x → 0 ≤ y → (x ≤ √y ↔ x ^ 2 ≤ y)
-- Mathlib.Data.Fin.Tuple.Finset
Fin.mem_piFinset_iff_pivot_removeNth : ∀ {n : ℕ} {α : Fin (n + 1) → Type u_1} {f : (i : Fin (n + 1)) → α i} {s : (i : Fin (n + 1)) → Finset (α i)}
  (p : Fin (n + 1)), f ∈ Fintype.piFinset s ↔ f p ∈ s p ∧ p.removeNth f ∈ Fintype.piFinset (p.removeNth s)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
logDeriv_sin_div_eq_cot : ∀ {x : ℂ},
  x ∈ Complex.integerComplement →
    logDeriv (fun t => Complex.sin (↑Real.pi * t) / (↑Real.pi * t)) x = ↑Real.pi * (↑Real.pi * x).cot - 1 / x
-- Lean.Widget.TaggedText
/-- Invariants:
- non-empty
- no adjacent `text` elements (they should be collapsed)
- no directly nested `append`s (but `append #[tag _ (append ..)]` is okay)  -/
Lean.Widget.TaggedText.append : {α : Type u} → Array (Lean.Widget.TaggedText α) → Lean.Widget.TaggedText α
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.IsBasis.contract_isBasis_of_indep : ∀ {α : Type u_1} {M : Matroid α} {I J X : Set α},
  M.IsBasis I X → M.Indep (I ∪ J) → (M.contract J).IsBasis (I \ J) (X \ J)
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.toEquiv : {α : Type u_6} → {β : Type u_7} → [inst : MeasurableSpace α] → [inst_1 : MeasurableSpace β] → α ≃ᵐ β → α ≃ β
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepSets.of_subsingleton : ∀ {Ω : Type u_1} {ι : Type u_2} {x : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [Subsingleton ι]
  {m : ι → Set (Set Ω)} [MeasureTheory.IsProbabilityMeasure μ], ProbabilityTheory.iIndepSets m μ
-- Mathlib.RingTheory.HopfAlgebra.Quotient
/-- Post-composition by an algebra homomorphism preserves the convolution unit.  -/
LinearMap.algHom_comp_convOne : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : HopfAlgebra R A] [inst_4 : HopfAlgebraStruct R B] (g : A →ₐ[R] B),
  g.toLinearMap ∘ₗ WithConv.ofConv 1 = WithConv.ofConv 1
-- Lean.Data.Lsp.Workspace
Lean.Lsp.DidChangeWatchedFilesRegistrationOptions.mk.injEq : ∀ (watchers watchers_1 : Array Lean.Lsp.FileSystemWatcher),
  ({ watchers := watchers } = { watchers := watchers_1 }) = (watchers = watchers_1)
-- Mathlib.Algebra.Polynomial.Degree.SmallDegree
Polynomial.degree_cubic_lt : ∀ {R : Type u} {a b c d : R} [inst : Semiring R],
  (Polynomial.C a * Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X +
        Polynomial.C d).degree <
    4
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.average_union : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {μ : MeasureTheory.Measure α} {f : α → E} {s t : Set α},
  MeasureTheory.AEDisjoint μ s t →
    MeasureTheory.NullMeasurableSet t μ →
      μ s ≠ ⊤ →
        μ t ≠ ⊤ →
          MeasureTheory.IntegrableOn f s μ →
            MeasureTheory.IntegrableOn f t μ →
              ⨍ (x : α) in s ∪ t, f x ∂μ =
                (μ.real s / (μ.real s + μ.real t)) • ⨍ (x : α) in s, f x ∂μ +
                  (μ.real t / (μ.real s + μ.real t)) • ⨍ (x : α) in t, f x ∂μ
-- Batteries.Lean.Meta.UnusedNames
/-- Obtain `n` distinct names such that each name is unused in the given local
context and `suggestion` is a prefix of each name.
 -/
Lean.LocalContext.getUnusedUserNames : Lean.LocalContext → ℕ → Lean.Name → Array Lean.Name
-- Lean.Parser.Types
Lean.Parser.ParserContextCore.mk.inj : ∀ {toInputContext : Lean.Parser.InputContext} {toParserModuleContext : Lean.Parser.ParserModuleContext}
  {toCacheableParserContext : Lean.Parser.CacheableParserContext} {tokens : Lean.Parser.TokenTable}
  {toInputContext_1 : Lean.Parser.InputContext} {toParserModuleContext_1 : Lean.Parser.ParserModuleContext}
  {toCacheableParserContext_1 : Lean.Parser.CacheableParserContext} {tokens_1 : Lean.Parser.TokenTable},
  { toInputContext := toInputContext, toParserModuleContext := toParserModuleContext,
        toCacheableParserContext := toCacheableParserContext, tokens := tokens } =
      { toInputContext := toInputContext_1, toParserModuleContext := toParserModuleContext_1,
        toCacheableParserContext := toCacheableParserContext_1, tokens := tokens_1 } →
    toInputContext = toInputContext_1 ∧
      toParserModuleContext = toParserModuleContext_1 ∧
        toCacheableParserContext = toCacheableParserContext_1 ∧ tokens = tokens_1
-- Mathlib.Analysis.Complex.Hadamard
Complex.HadamardThreeLines.interpStrip.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] (f : ℂ → E) (z : ℂ),
  Complex.HadamardThreeLines.interpStrip f z =
    if Complex.HadamardThreeLines.sSupNormIm f 0 = 0 ∨ Complex.HadamardThreeLines.sSupNormIm f 1 = 0 then 0
    else ↑(Complex.HadamardThreeLines.sSupNormIm f 0) ^ (1 - z) * ↑(Complex.HadamardThreeLines.sSupNormIm f 1) ^ z
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem!_toArray_roc_eq_zero : ∀ {m n : ℤ} {i : ℕ}, (n - m).toNat ≤ i → (m<...=n).toArray[i]! = 0
-- Init.Grind.Util
/-- Gadget for annotating conditions of `match` equational lemmas.
We use this annotation for two different reasons:
- We don't want to normalize them.
- We have a propagator for them.
 -/
Lean.Grind.MatchCond : Prop → Prop
-- Mathlib.CategoryTheory.RegularCategory.Basic
/-- Regular categories satisfy Frobenius reciprocity. That is, in the internal language of regular
categories, we have `∃ x, (P(x) ⊓ Q)` iff `(∃ x, P(x)) ⊓ Q`, for a proposition `Q` not depending on
`x`.
 -/
CategoryTheory.Regular.exists_inf_pullback_eq_exists_inf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Regular C] {A B : C} (f : A ⟶ B)
  (A' : CategoryTheory.Subobject A) (B' : CategoryTheory.Subobject B),
  (CategoryTheory.Subobject.exists f).obj (A' ⊓ (CategoryTheory.Subobject.pullback f).obj B') =
    (CategoryTheory.Subobject.exists f).obj A' ⊓ B'