mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Functor.Category
CategoryTheory.NatTrans.app_naturality_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
  {F G : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (T : F ⟶ G) (X : C) {Y Z : D} (f : Y ⟶ Z) {Z_1 : E}
  (h : (G.obj X).obj Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp ((F.obj X).map f) (CategoryTheory.CategoryStruct.comp ((T.app X).app Z) h) =
    CategoryTheory.CategoryStruct.comp ((T.app X).app Y) (CategoryTheory.CategoryStruct.comp ((G.obj X).map f) h)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.size_inter_le_size_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  (t₁ ∩ t₂).size ≤ t₁.size
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToTerm.Context.kind : Lean.Elab.Term.Do.ToTerm.Context → Lean.Elab.Term.Do.ToTerm.Kind
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.IsBigO.eq_zero_of_norm_pow : ∀ {E'' : Type u_9} {F'' : Type u_10} [inst : NormedAddCommGroup E''] [inst_1 : NormedAddCommGroup F''] {f : E'' → F''}
  {x₀ : E''} {n : ℕ}, (f =O[nhds x₀] fun x => ‖x - x₀‖ ^ n) → n ≠ 0 → f x₀ = 0
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
MeasureTheory.OuterMeasure.sInf_eq_boundedBy_sInfGen : ∀ {α : Type u_1} (m : Set (MeasureTheory.OuterMeasure α)),
  sInf m = MeasureTheory.OuterMeasure.boundedBy (MeasureTheory.OuterMeasure.sInfGen m)
-- Mathlib.Order.Heyting.Basic
/-- `(· \ a)` is left adjoint to `(· ⊔ a)`  -/
GeneralizedCoheytingAlgebra.sdiff_le_iff : ∀ {α : Type u_4} [self : GeneralizedCoheytingAlgebra α] (a b c : α), a \ b ≤ c ↔ a ≤ b ⊔ c
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp_id_left_hom_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b : B}
  (f : a ⟶ b) (X : ↑(F.obj a)),
  (F.mapComp (CategoryTheory.CategoryStruct.id a) f).hom.toNatTrans.app X =
    CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom).toNatTrans.app X)
      ((F.map f).toFunctor.map ((F.mapId a).inv.toNatTrans.app X))
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.contains_erase : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k a : α}, (m.erase k).contains a = (!k == a && m.contains a)
-- Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Real.negMulLog_zero : Real.negMulLog 0 = 0
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
AddSubgroup.coe_zmultiples : ∀ {G : Type u_1} [inst : AddGroup G] (g : G), ↑(AddSubgroup.zmultiples g) = Set.range fun x => x • g
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Hom.preimageIso_inv_ι : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : CategoryTheory.IsIso f] (U : Y.Opens),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.preimageIso f U).inv
      (CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map f.base).obj U).ι f) =
    U.ι
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
UniformConvergenceCLM.instTopologicalSpace.congr_simp : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3}
  (F : Type u_4) [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : TopologicalSpace E]
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜₂ F] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F]
  (𝔖 : Set (Set E)), UniformConvergenceCLM.instTopologicalSpace σ F 𝔖 = UniformConvergenceCLM.instTopologicalSpace σ F 𝔖
-- Mathlib.RingTheory.QuasiFinite.Basic
/-- [Stacks Tag 00PP](https://stacks.math.columbia.edu/tag/00PP) ((3)) -/
Algebra.QuasiFinite.baseChange : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.QuasiFinite R S] {A : Type u_4} [inst_4 : CommRing A] [inst_5 : Algebra R A],
  Algebra.QuasiFinite A (TensorProduct R A S)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono_K : ∀ {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) [inst_2 : CategoryTheory.Epi φ.τ₁]
  [inst_3 : CategoryTheory.IsIso φ.τ₂] [inst_4 : CategoryTheory.Mono φ.τ₃],
  (CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono φ h).K = h.K
-- Init.Data.List.Lemmas
List.filter_bne_eq_self_of_not_mem : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {l : List α}, a ∉ l → List.filter (fun x => x != a) l = l
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
Complex.div_cpow_ofReal_nonneg : ∀ {a b : ℝ}, 0 ≤ a → 0 ≤ b → ∀ (r : ℂ), (↑a / ↑b) ^ r = ↑a ^ r / ↑b ^ r
-- Mathlib.Algebra.Order.Group.Finset
Finset.sup'_mul : ∀ {ι : Type u_1} {G : Type u_4} [inst : Group G] [inst_1 : LinearOrder G] [MulRightMono G] (s : Finset ι) (f : ι → G)
  (a : G) (hs : s.Nonempty), s.sup' hs f * a = s.sup' hs fun i => f i * a
-- Mathlib.Probability.Process.Adapted
MeasureTheory.Adapted.stronglyAdapted : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : ι → Type u_3} [inst_1 : (i : ι) → TopologicalSpace (β i)] {u : (i : ι) → Ω → β i}
  [mΒ : (i : ι) → MeasurableSpace (β i)] [∀ (i : ι), OpensMeasurableSpace (β i)]
  [∀ (i : ι), TopologicalSpace.PseudoMetrizableSpace (β i)] [∀ (i : ι), SecondCountableTopology (β i)],
  MeasureTheory.Adapted f u → MeasureTheory.StronglyAdapted f u
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.universalMulHom_commutes : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {T : Type u_2}
  [inst_2 : Monoid T] (f : R →* T) (fS : ↥S →* Tˣ) (hf : ∀ (s : ↥S), f ↑s = ↑(fS s)) {r : R},
  (OreLocalization.universalMulHom f fS hf) (OreLocalization.numeratorHom r) = f r
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- If there is an additive fundamental domain `s`, then `HasAddFundamentalDomain`
holds.  -/
MeasureTheory.IsAddFundamentalDomain.hasAddFundamentalDomain : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α]
  (ν : MeasureTheory.Measure α) {s : Set α},
  MeasureTheory.IsAddFundamentalDomain G s ν → MeasureTheory.HasAddFundamentalDomain G α ν
-- Mathlib.FieldTheory.Minpoly.IsConjRoot
IsConjRoot.decidable : {K : Type u_2} →
  {L : Type u_3} →
    [inst : Field K] →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] →
          [Normal K L] → [DecidableEq L] → [Fintype Gal(L/K)] → (x y : L) → Decidable (IsConjRoot K x y)
-- Lean.Linter.Init
Lean.Linter.LinterOptions.mk.inj : ∀ {toOptions : Lean.Options} {linterSets : Lean.Linter.LinterSets} {toOptions_1 : Lean.Options}
  {linterSets_1 : Lean.Linter.LinterSets},
  { toOptions := toOptions, linterSets := linterSets } = { toOptions := toOptions_1, linterSets := linterSets_1 } →
    toOptions = toOptions_1 ∧ linterSets = linterSets_1
-- Mathlib.Order.Filter.Map
Filter.map_generate_le_generate_preimage_preimage : ∀ {α : Type u_1} {β : Type u_2} (U : Set (Set β)) (f : β → α),
  Filter.map f (Filter.generate U) ≤ Filter.generate ((fun x => f ⁻¹' x) ⁻¹' U)
-- Mathlib.Data.Int.Init
Int.sign_mul_self_eq_natAbs : ∀ (a : ℤ), a.sign * a = ↑a.natAbs
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
/-- Functoriality of `restrictedYonedaObj η` in `η`.  -/
CategoryTheory.OverPresheafAux.restrictedYonedaObjMap₁ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A F G : CategoryTheory.Functor Cᵒᵖ (Type v)} →
      {η : F ⟶ A} →
        {μ : G ⟶ A} →
          (ε : F ⟶ G) →
            CategoryTheory.CategoryStruct.comp ε μ = η →
              (CategoryTheory.OverPresheafAux.restrictedYonedaObj η ⟶
                CategoryTheory.OverPresheafAux.restrictedYonedaObj μ)
-- Mathlib.Algebra.Order.Quantale
Quantale.iSup_mul_distrib : ∀ {α : Type u_1} {ι : Type u_2} {x : α} {f : ι → α} [inst : Semigroup α] [inst_1 : CompleteLattice α] [IsQuantale α],
  (⨆ i, f i) * x = ⨆ i, f i * x
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.SignedMeasure.totalVariation_zero : ∀ {α : Type u_1} [inst : MeasurableSpace α], MeasureTheory.SignedMeasure.totalVariation 0 = 0
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.toList_filterMap : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w}
  {f : (a : α) → β a → Option (γ a)} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filterMap f t ⋯).impl.toList =
    List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) t.toList
-- Mathlib.Algebra.Field.Defs
/-- Scalar multiplication by a nonnegative rational number.

Unless there is a risk of a `Module ℚ≥0 _` instance diamond, write `nnqsmul := _`. This will set
`nnqsmul` to `(NNRat.cast · * ·)` thanks to unification in the default proof of `nnqsmul_def`.

Do not use directly. Instead use the `•` notation.  -/
Semifield.nnqsmul : {K : Type u_2} → [self : Semifield K] → ℚ≥0 → K → K
-- Mathlib.RingTheory.Bialgebra.Hom
/-- See Note [custom simps projection]  -/
BialgHom.Simps.apply : {R : Type u_6} →
  {α : Type u_7} →
    {β : Type u_8} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring α] →
          [inst_2 : Algebra R α] →
            [inst_3 : Semiring β] →
              [inst_4 : Algebra R β] →
                [inst_5 : CoalgebraStruct R α] → [inst_6 : CoalgebraStruct R β] → (α →ₐc[R] β) → α → β
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroupClass.coe_inclusion : ∀ {G : Type u_1} [inst : AddGroup G] {S : Type u_4} [inst_1 : SetLike S G] [inst_2 : AddSubgroupClass S G]
  [inst_3 : LE S] [inst_4 : IsConcreteLE S G] {H K : S} (h : H ≤ K) (a : ↥H), ↑((AddSubgroupClass.inclusion h) a) = ↑a
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
IsCyclotomicExtension.Rat.card_subgroupGalEquivSubgroupChar : ∀ (n : ℕ) [inst : NeZero n] (K : Type u_1) [inst_1 : Field K] [inst_2 : NumberField K]
  [hK : IsCyclotomicExtension {n} ℚ K] (R : Type u_2) [inst_3 : CommRing R]
  [inst_4 : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)] [IsMulCommutative Gal(K/ℚ)] (H : Subgroup Gal(K/ℚ)),
  Nat.card ↥(OrderDual.ofDual ((IsCyclotomicExtension.Rat.subgroupGalEquivSubgroupChar n K R) H)) =
    Nat.card (Gal(K/ℚ) ⧸ H)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.mem_insertManyIfNewUnit_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtDHashMap α fun x => Unit} {ρ : Type w} [inst : ForIn Id ρ α]
  [inst_1 : EquivBEq α] [inst_2 : LawfulHashable α] {l : ρ} {k : α},
  k ∈ m → k ∈ Std.ExtDHashMap.Const.insertManyIfNewUnit m l
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getD_ofList_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : LawfulBEq α] {l : List ((a : α) × β a)} {k : α}
  {fallback : β k}, (List.map Sigma.fst l).contains k = false → (Std.DHashMap.ofList l).getD k fallback = fallback
-- Mathlib.Algebra.Group.Action.Defs
VAddAssocClass.of_vadd_zero_add : ∀ {M : Type u_9} {N : Type u_10} [inst : AddMonoid N] [inst_1 : VAdd M N],
  (∀ (x : M) (y : N), (x +ᵥ 0) + y = x +ᵥ y) → VAddAssocClass M N N
-- Mathlib.Algebra.Category.Semigrp.Basic
MagmaCat.mk.sizeOf_spec : ∀ (carrier : Type u) [str : Mul carrier], sizeOf { carrier := carrier, str := str } = 1 + sizeOf carrier + sizeOf str
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.coeff_toAdditive_apply : ∀ (R : Type u_3) (M : Type u_6) [inst : Semiring R] [inst_1 : Mul M] (x : MonoidAlgebra R M),
  ((MonoidAlgebra.toAdditive R M) x).coeff = Finsupp.mapDomain (⇑Additive.ofMul) x.coeff
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.coe_copy : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S : Subalgebra R A)
  (s : Set A) (hs : s = ↑S), ↑(S.copy s hs) = s
-- Init.Data.BitVec.Bitblast
BitVec.srem_zero_of_dvd : ∀ {w : ℕ} {x y : BitVec w}, y.toInt ∣ x.toInt → x.srem y = 0#w
-- Mathlib.RingTheory.ClassGroup.ExtendedHom
ClassGroup.extendedIdeal_extendedIdeal : ∀ (A : Type u_1) (B : Type u_2) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [inst_3 : Module.IsTorsionFree A B] [inst_4 : IsDomain A] [inst_5 : IsDomain B] (C : Type u_3) [inst_6 : CommRing C]
  [inst_7 : IsDomain C] [inst_8 : Algebra B C] [inst_9 : Algebra A C] [IsScalarTower A B C]
  [inst_11 : Module.IsTorsionFree B C] [inst_12 : Module.IsTorsionFree A C] (I : ↥(nonZeroDivisors (Ideal A))),
  ClassGroup.extendedIdeal B C (ClassGroup.extendedIdeal A B I) = ClassGroup.extendedIdeal A C I
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- Variant of `homMk'` where both objects are applications of `mk`.  -/
CategoryTheory.CostructuredArrow.mkPrecomp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {T : D} →
          {Y Y' : C} →
            {S : CategoryTheory.Functor C D} →
              (f : S.obj Y ⟶ T) →
                (g : Y' ⟶ Y) →
                  CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.comp (S.map g) f) ⟶
                    CategoryTheory.CostructuredArrow.mk f
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] [inst : BEq α]
  [Std.LawfulBEqOrd α] (h : t.WF) {l : List ((a : α) × β a)} {k : α},
  (List.map Sigma.fst l).contains k = false → (↑(t.insertMany l ⋯)).getKey? k = t.getKey? k
-- Init.Data.UInt.Lemmas
USize.le_refl : ∀ (a : USize), a ≤ a
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Functor.instIsSplitMonoApp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (f : G ⟶ F) [CategoryTheory.IsSplitMono f] (X : C),
  CategoryTheory.IsSplitMono (f.app X)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentHighlight.mk.inj : ∀ {range : Lean.Lsp.Range} {kind? : Option Lean.Lsp.DocumentHighlightKind} {range_1 : Lean.Lsp.Range}
  {kind?_1 : Option Lean.Lsp.DocumentHighlightKind},
  { range := range, kind? := kind? } = { range := range_1, kind? := kind?_1 } → range = range_1 ∧ kind? = kind?_1
-- Init.Data.String.Modify
/-- Applies the function `f` to every character in a string, returning a string that contains the
resulting characters.

Examples:
 * `"abc123".map Char.toUpper = "ABC123"`
 * `"".map Char.toUpper = ""`
 -/
String.map : (Char → Char) → String → String
-- Mathlib.Data.PFunctor.Multivariate.W
MvPFunctor.WPath.child.sizeOf_spec : ∀ {n : ℕ} {P : MvPFunctor.{u} (n + 1)} (a : P.A) (f : P.last.B a → P.last.W) (i : Fin2 n) (j : P.last.B a)
  (c : P.WPath (f j) i), sizeOf (MvPFunctor.WPath.child a f i j c) = 1 + sizeOf a + sizeOf i + sizeOf j + sizeOf c
-- Mathlib.AlgebraicTopology.TopologicalSimplex
SimplexCategory.toTop₀_obj : ∀ (n : SimplexCategory), SimplexCategory.toTop₀.obj n = TopCat.of ↑(stdSimplex ℝ (Fin (n.len + 1)))
-- Mathlib.Algebra.MvPolynomial.Expand
MvPolynomial.expand_one_apply : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] (f : MvPolynomial σ R), (MvPolynomial.expand 1) f = f
-- Mathlib.MeasureTheory.Function.UniformIntegrable
/-- Suppose `f` is a sequence of functions that converges a.e. to `g`. If `f` is
`UniformIntegrable`, then `g` is integrable.  -/
MeasureTheory.UniformIntegrable.integrable_of_ae_tendsto : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {κ : Type u_4} {u : Filter κ} [u.NeBot] [u.IsCountablyGenerated] {f : κ → α → β} {g : α → β},
  MeasureTheory.UniformIntegrable f 1 μ →
    (∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) u (nhds (g x))) → MeasureTheory.Integrable g μ
-- Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
Finset.sum_eq_sum_Ico_succ_bot : ∀ {M : Type u_2} [inst : AddCommMonoid M] {a b : ℕ},
  a < b → ∀ (f : ℕ → M), ∑ k ∈ Finset.Ico a b, f k = f a + ∑ k ∈ Finset.Ico (a + 1) b, f k
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.instCompleteSpaceOfT1SpaceOfContinuousMap : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero X] [inst_1 : TopologicalSpace X] [inst_2 : Zero R]
  [inst_3 : UniformSpace R] [T1Space R] [CompleteSpace C(X, R)], CompleteSpace (ContinuousMapZero X R)
-- Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
/-- The coercion `(fun x y => B x y) : E → (F → 𝕜)` is continuous.  -/
WeakBilin.coeFn_continuous : ∀ {𝕜 : Type u_2} {E : Type u_4} {F : Type u_5} [inst : TopologicalSpace 𝕜] [inst_1 : CommSemiring 𝕜]
  [inst_2 : AddCommMonoid E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommMonoid F] [inst_5 : Module 𝕜 F]
  (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜), Continuous fun x y => (B x) y
-- Aesop.Script.SpecificTactics
Aesop.Script.TacticBuilder.applyStx : Lean.Term → Lean.Meta.TransparencyMode → Aesop.Script.TacticBuilder
-- Init.Data.SInt.Lemmas
Int32.toInt8_ofNat : ∀ {n : ℕ}, (OfNat.ofNat n).toInt8 = OfNat.ofNat n
-- Init.Prelude
Lean.Macro.instInhabitedMethodsRef : Inhabited Lean.Macro.MethodsRef
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderOutput.mk.injEq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {old : Std.Sat.AIG α} (aig : Std.Sat.AIG α)
  (out cout : aig.Ref) (hle : old.decls.size ≤ aig.decls.size) (aig_1 : Std.Sat.AIG α) (out_1 cout_1 : aig_1.Ref)
  (hle_1 : old.decls.size ≤ aig_1.decls.size),
  ({ aig := aig, out := out, cout := cout, hle := hle } =
      { aig := aig_1, out := out_1, cout := cout_1, hle := hle_1 }) =
    (aig = aig_1 ∧ out ≍ out_1 ∧ cout ≍ cout_1)
-- Mathlib.Algebra.Group.Units.Defs
IsAddUnit.eq_zero : ∀ {M : Type u_1} [inst : AddMonoid M] {a : M} [Subsingleton (AddUnits M)], IsAddUnit a → a = 0
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.instIsLEObjTruncGELE : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C] (X : C) (a b : ℤ),
  t.IsLE ((t.truncGELE a b).obj X) b
-- Mathlib.Analysis.RCLike.Sqrt
RCLike.sqrt_one : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜], RCLike.sqrt 1 = 1
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.comp_mapAddMon_zero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] {E : Type u₃}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.MonoidalCategory E]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [inst_6 : F.LaxMonoidal] [inst_7 : G.LaxMonoidal]
  (X : CategoryTheory.AddMon C),
  CategoryTheory.AddMonObj.zero =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε (F.comp G))
      ((F.comp G).map CategoryTheory.AddMonObj.zero)
-- Mathlib.CategoryTheory.Sites.Sheaf
/-- Given presieve `R` and presheaf `P : Cᵒᵖ ⥤ A`, the natural cone associated to `P` and
the sieve `Sieve.generate R` generated by `R` is a limit cone iff `Hom (E, P -)` is a
sheaf of types for the presieve `R` and all `E : A`.  -/
CategoryTheory.Presheaf.isLimit_iff_isSheafFor_presieve : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  (P : CategoryTheory.Functor Cᵒᵖ A) {X : C} (R : CategoryTheory.Presieve X),
  Nonempty (CategoryTheory.Limits.IsLimit (P.mapCone (CategoryTheory.Sieve.generate R).arrows.cocone.op)) ↔
    ∀ (E : Aᵒᵖ), CategoryTheory.Presieve.IsSheafFor (P.comp (CategoryTheory.coyoneda.obj E)) R
-- Mathlib.RingTheory.Localization.FractionRing
/-- An algebra automorphism of a ring induces an algebra automorphism of its fraction field.

This is a bundled version of `fieldEquivOfAlgEquiv`.  -/
IsFractionRing.fieldEquivOfAlgEquivHom : {A : Type u_8} →
  {B : Type u_9} →
    [inst : CommRing A] →
      [inst_1 : CommRing B] →
        [inst_2 : Algebra A B] →
          (K : Type u_10) →
            (L : Type u_11) →
              [inst_3 : Field K] →
                [inst_4 : Field L] →
                  [inst_5 : Algebra A K] →
                    [inst_6 : Algebra B L] →
                      [IsFractionRing A K] →
                        [IsFractionRing B L] →
                          [inst_9 : Algebra A L] →
                            [IsScalarTower A B L] →
                              [inst_11 : Algebra K L] → [IsScalarTower A K L] → (B ≃ₐ[A] B) →* Gal(L/K)
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided
/-- The braiding isomorphism for Day convolution.  -/
CategoryTheory.MonoidalCategory.DayConvolution.braiding : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {V : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [CategoryTheory.BraidedCategory C] →
            [inst_4 : CategoryTheory.MonoidalCategory V] →
              [CategoryTheory.BraidedCategory V] →
                (F G : CategoryTheory.Functor C V) →
                  [inst_6 : CategoryTheory.MonoidalCategory.DayConvolution F G] →
                    [inst_7 : CategoryTheory.MonoidalCategory.DayConvolution G F] →
                      CategoryTheory.MonoidalCategory.DayConvolution.convolution F G ≅
                        CategoryTheory.MonoidalCategory.DayConvolution.convolution G F
-- Lean.Elab.MutualInductive
Lean.Elab.Command.InductiveView.derivingClasses : Lean.Elab.Command.InductiveView → Array Lean.Elab.DerivingClassView
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.List.filter.match_1.splitter : (motive : Bool → Sort u_1) → (x : Bool) → (Unit → motive true) → (Unit → motive false) → motive x
-- Init.Data.Vector.Lemmas
/-- In an equality between two casts, push the casts to the right hand side.  -/
Vector.cast_eq_cast : ∀ {α : Type u_1} {n m k : ℕ} {as : Vector α n} {bs : Vector α m} {wa : n = k} {wb : m = k},
  Vector.cast wa as = Vector.cast wb bs ↔ as = Vector.cast ⋯ bs
-- Mathlib.Geometry.Euclidean.SignedDist
signedDist_congr : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (v w : V), (∃ r > 0, r • v = w) → signedDist v = signedDist w
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.instHasDimensionLETensorUnitOfNatNat : (CategoryTheory.MonoidalCategoryStruct.tensorUnit SSet).HasDimensionLE 0
-- Std.Do.PostCond
Std.Do.ExceptConds.const.eq_def : ∀ {ps : Std.Do.PostShape} (p : Prop),
  Std.Do.ExceptConds.const p =
    match ps with
    | Std.Do.PostShape.pure => PUnit.unit
    | Std.Do.PostShape.arg σ ps => Std.Do.ExceptConds.const p
    | Std.Do.PostShape.except ε ps => (fun _ε => ⌜p⌝, Std.Do.ExceptConds.const p)
-- Mathlib.LinearAlgebra.Prod
LinearMap.range_prodMap : ∀ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : AddCommMonoid M₄] [inst_5 : Module R M]
  [inst_6 : Module R M₂] [inst_7 : Module R M₃] [inst_8 : Module R M₄] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₄),
  (f.prodMap g).range = f.range.prod g.range
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
/-- Given measures `μ` and `ν`, if `s` is a measure mutually singular to `ν` and `f` is a
measurable function such that `μ = s + fν`, then `s = μ.singularPart μ`.

This theorem provides the uniqueness of the `singularPart` in the Lebesgue decomposition theorem,
while `MeasureTheory.Measure.eq_rnDeriv` provides the uniqueness of the
`rnDeriv`.  -/
MeasureTheory.Measure.eq_singularPart : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν s : MeasureTheory.Measure α} {f : α → ENNReal},
  Measurable f → s.MutuallySingular ν → μ = s + ν.withDensity f → s = μ.singularPart ν