mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.Deriv.Add
HasStrictDerivAt.add : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f g : 𝕜 → F} {f' g' : F} {x : 𝕜},
  HasStrictDerivAt f f' x → HasStrictDerivAt g g' x → HasStrictDerivAt (f + g) (f' + g') x
-- Mathlib.Algebra.Group.Hom.Defs
/-- The inverse of a bijective `MonoidHom` is a `MonoidHom`.  -/
MonoidHom.inverse : {A : Type u_10} →
  {B : Type u_11} →
    [inst : Monoid A] →
      [inst_1 : Monoid B] → (f : A →* B) → (g : B → A) → Function.LeftInverse g ⇑f → Function.RightInverse g ⇑f → B →* A
-- Mathlib.RingTheory.TensorProduct.MonoidAlgebra
AddMonoidAlgebra.scalarTensorEquiv_symm_single : ∀ {R : Type u_1} {M : Type u_2} {A : Type u_5} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  [inst_3 : AddCommMonoid M] (m : M) (a : A),
  (AddMonoidAlgebra.scalarTensorEquiv R A).symm (AddMonoidAlgebra.single m a) = a ⊗ₜ[R] AddMonoidAlgebra.single m 1
-- Mathlib.Analysis.Seminorm
Seminorm.add_comp : ∀ {𝕜 : Type u_3} {𝕜₂ : Type u_4} {E : Type u_7} {E₂ : Type u_8} [inst : SeminormedRing 𝕜] [inst_1 : SeminormedRing 𝕜₂]
  {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_2 : RingHomIsometric σ₁₂] [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup E₂]
  [inst_5 : Module 𝕜 E] [inst_6 : Module 𝕜₂ E₂] (p q : Seminorm 𝕜₂ E₂) (f : E →ₛₗ[σ₁₂] E₂),
  (p + q).comp f = p.comp f + q.comp f
-- Mathlib.CategoryTheory.ConcreteCategory.Basic
CategoryTheory.id_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {X : C}
  (x : CategoryTheory.ToType X), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x
-- Mathlib.Algebra.Category.CommBialgCat
CommBialgCat.bialgEquivOfIso_apply : ∀ {R : Type u} [inst : CommRing R] {A B : CommBialgCat R} (i : A ≅ B) (a : ↑A),
  (CommBialgCat.bialgEquivOfIso i) a = (CategoryTheory.ConcreteCategory.hom i.hom) a
-- Mathlib.Combinatorics.Matroid.Loop
/-- `M.coloops` is the set of coloops of `M`.  -/
Matroid.coloops : {α : Type u_1} → Matroid α → Set α
-- Mathlib.Data.TypeVec
TypeVec.subsingleton0 : Subsingleton (TypeVec.{u_1} 0)
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pith.pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_of : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {B' : Type u₂} [inst_1 : CategoryTheory.Bicategory B']
  [inst_2 : CategoryTheory.Bicategory.IsLocallyGroupoid B'] (F : CategoryTheory.Pseudofunctor B' B) {X Y : B'}
  (f : X ⟶ Y), ((CategoryTheory.Bicategory.Pith.pseudofunctorToPith F).map f).of = F.map f
-- Mathlib.Data.Finsupp.Basic
Finsupp.zero_notMem_frange : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {f : α →₀ M}, 0 ∉ f.frange
-- Batteries.Data.String.Lemmas
/-- Induction along the valid positions in a list of characters.
(This definition is intended only for specification purposes.)
 -/
String.utf8InductionOn : {motive : List Char → String.Pos.Raw → Sort u} →
  (s : List Char) →
    (i p : String.Pos.Raw) →
      ((i : String.Pos.Raw) → motive [] i) →
        ((c : Char) → (cs : List Char) → motive (c :: cs) p) →
          ((c : Char) → (cs : List Char) → (i : String.Pos.Raw) → i ≠ p → motive cs (i + c) → motive (c :: cs) i) →
            motive s i
-- Mathlib.GroupTheory.Perm.Finite
Equiv.Perm.disjoint_support_closure_of_disjoint_support : ∀ {α : Type u} [inst : DecidableEq α] [inst_1 : Fintype α] {S T : Set (Equiv.Perm α)},
  (∀ a ∈ S, ∀ b ∈ T, Disjoint a.support b.support) →
    ∀ a ∈ Subgroup.closure S, ∀ b ∈ Subgroup.closure T, Disjoint a.support b.support
-- Mathlib.Algebra.Group.Conj
ConjClasses.carrier.eq_1 : ∀ {α : Type u} [inst : Monoid α], ConjClasses.carrier = Quotient.lift conjugatesOf ⋯
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsSpanningSubgraph.instIsPartialOrder : ∀ {α : Type u_1} {β : Type u_2}, IsPartialOrder (Graph α β) fun x1 x2 => x1 ≤s x2
-- Mathlib.CategoryTheory.Sites.LocallyInjective
/-- A morphism `φ : F₁ ⟶ F₂` of presheaves `Cᵒᵖ ⥤ D` (with `D` a concrete category)
is locally injective for a Grothendieck topology `J` on `C` if
whenever two sections of `F₁` are sent to the same section of `F₂`, then these two
sections coincide locally.  -/
CategoryTheory.Presheaf.IsLocallyInjective : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        {FD : D → D → Type u_1} →
          {CD : D → Type w} →
            [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] →
              [CategoryTheory.ConcreteCategory D FD] →
                CategoryTheory.GrothendieckTopology C → {F₁ F₂ : CategoryTheory.Functor Cᵒᵖ D} → (F₁ ⟶ F₂) → Prop
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
SemilinearIsometryClass.diam_image : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} {𝓕 : Type u_10} [inst : Semiring R]
  [inst_1 : Semiring R₂] {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂]
  [inst_4 : Module R E] [inst_5 : Module R₂ E₂] [inst_6 : FunLike 𝓕 E E₂] [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕)
  (s : Set E), Metric.diam (⇑f '' s) = Metric.diam s
-- Mathlib.Probability.Moments.IntegrableExpMul
/-- If `ω ↦ exp (t * X ω)` is integrable at `t` and `-t`, then `ω ↦ exp (t * |X ω|)` is
integrable.  -/
ProbabilityTheory.integrable_exp_mul_abs : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ},
  MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ →
    MeasureTheory.Integrable (fun ω => Real.exp (-t * X ω)) μ →
      MeasureTheory.Integrable (fun ω => Real.exp (t * |X ω|)) μ
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.le_comap_pow_of_le_comap : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (p : Submodule R M)
  {f : M →ₗ[R] M}, p ≤ Submodule.comap f p → ∀ (k : ℕ), p ≤ Submodule.comap (f ^ k) p
-- Mathlib.Probability.Process.HittingTime
MeasureTheory.hittingBtwn_le : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder ι] {u : ι → Ω → β} {s : Set β}
  {n m : ι} (ω : Ω), MeasureTheory.hittingBtwn u s n m ω ≤ m
-- Mathlib.Data.List.Sublists
List.sublistsLen_sublist_of_sublist : ∀ {α : Type u} (n : ℕ) {l₁ l₂ : List α}, l₁.Sublist l₂ → (List.sublistsLen n l₁).Sublist (List.sublistsLen n l₂)
-- Mathlib.Topology.MetricSpace.Congruence
Congruent.comp_right : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {P₃ : Type u_5} {v₁ : ι → P₁} {v₂ : ι → P₂}
  [inst : PseudoEMetricSpace P₁] [inst_1 : PseudoEMetricSpace P₂] [inst_2 : PseudoEMetricSpace P₃] {f : P₂ → P₃},
  Isometry f → Congruent v₁ v₂ → Congruent v₁ (f ∘ v₂)
-- Mathlib.Algebra.Polynomial.BigOperators
Polynomial.prod_X_sub_C_nextCoeff : ∀ {R : Type u} {ι : Type w} [inst : CommRing R] {s : Finset ι} (f : ι → R),
  (∏ i ∈ s, (Polynomial.X - Polynomial.C (f i))).nextCoeff = -∑ i ∈ s, f i
-- Std.Time.Format.Modifier
Std.Time.Modifier.G.sizeOf_spec : ∀ (presentation : Std.Time.Text), sizeOf (Std.Time.Modifier.G presentation) = 1 + sizeOf presentation
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.mapDomainNonUnitalAlgHom_apply : ∀ (R : Type u_1) (A : Type u_4) {M : Type u_7} {N : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Add M] [inst_4 : Add N] (f : M →ₙ+ N) (a : AddMonoidAlgebra A M),
  (AddMonoidAlgebra.mapDomainNonUnitalAlgHom R A f) a = (AddMonoidAlgebra.mapDomainNonUnitalRingHom A f).toFun a
-- Mathlib.Analysis.Normed.Module.Basic
/-- A normed space over a normed field is a vector space endowed with a norm which satisfies the
equality `‖c • x‖ = ‖c‖ ‖x‖`. We require only `‖c • x‖ ≤ ‖c‖ ‖x‖` in the definition, then prove
`‖c • x‖ = ‖c‖ ‖x‖` in `norm_smul`.

Note that since this requires `SeminormedAddCommGroup` and not `NormedAddCommGroup`, this
typeclass can be used for "seminormed spaces" too, just as `Module` can be used for
"semimodules".  -/
NormedSpace : (𝕜 : Type u_6) → (E : Type u_7) → [NormedField 𝕜] → [SeminormedAddCommGroup E] → Type (max u_6 u_7)
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the reverse direction of `Asymptotics.isBigOWith_iff`.

---

Definition of `IsBigOWith`. We record it in a lemma as `IsBigOWith` is irreducible.  -/
Asymptotics.IsBigOWith.of_bound : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {c : ℝ} {f : α → E} {g : α → F}
  {l : Filter α}, (∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖) → Asymptotics.IsBigOWith c l f g
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
/-- The 2-morphism underlying the oplax functoriality constraint.  -/
CategoryTheory.OplaxFunctor.mapComp : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        (self : CategoryTheory.OplaxFunctor B C) →
          {a b c : B} →
            (f : a ⟶ b) →
              (g : b ⟶ c) →
                self.map (CategoryTheory.CategoryStruct.comp f g) ⟶
                  CategoryTheory.CategoryStruct.comp (self.map f) (self.map g)
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.precomposingCat_obj : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (a b c : B) (f : a ⟶ b),
  (CategoryTheory.Bicategory.precomposingCat a b c).obj f = (CategoryTheory.Bicategory.precomp c f).toCatHom
-- Aesop.RulePattern.Cache
Aesop.RulePatternCache.mk.injEq : ∀ (map map_1 : Std.HashMap Lean.Expr Aesop.RulePatternCache.Entry), ({ map := map } = { map := map_1 }) = (map = map_1)
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
csSup_Ico : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {a b : α} [DenselyOrdered α], a < b → sSup (Set.Ico a b) = b
-- Mathlib.CategoryTheory.Distributive.Monoidal
/-- The composite of `(X ◁ coprod.inr) : X ⊗ Z ⟶ X ⊗ (Y ⨿ Z)` and
`(∂L X Y Z).inv :  X ⊗ (Y ⨿ Z) ⟶ (X ⊗ Y) ⨿ (X ⊗ Z)`
is equal to the right coprojection `coprod.inr : X ⊗ Z ⟶ (X ⊗ Y) ⨿ (X ⊗ Z)`.  -/
CategoryTheory.whiskerLeft_coprod_inr_leftDistrib_inv_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] [inst_3 : CategoryTheory.IsMonoidalLeftDistrib C]
  {X Y Z Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⨿ CategoryTheory.MonoidalCategoryStruct.tensorObj X Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.Limits.coprod.inr)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.leftDistrib X Y Z).inv h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr h
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getD_erase_self : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α} {fallback : β}, (m.erase k).getD k fallback = fallback
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.insertMany_cons : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List (α × β)} {k : α} {v : β},
  m.insertMany ((k, v) :: l) = (m.insert k v).insertMany l
-- Aesop.Rule.Name
Aesop.ScopeName.local : Aesop.ScopeName
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.lintegral_mono : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α →ₘ[μ] ENNReal},
  f ≤ g → f.lintegral ≤ g.lintegral
-- Mathlib.RepresentationTheory.Homological.ContCohomology.Basic
/-- The `n`-th term in the resolution of a topological representation induced by `TopRep.coind₁`.  -/
TopRep.resolutionX : {k : Type u_1} →
  {G : Type u_2} →
    [inst : Ring k] →
      [inst_1 : Group G] →
        [inst_2 : TopologicalSpace k] →
          [inst_3 : TopologicalSpace G] → [IsTopologicalGroup G] → TopRep k G → ℕ → TopRep k G
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.charLitNoAntiquot.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Order.Interval.Finset.SuccPred
Finset.Ioc_pred_pred_eq_Ico_of_not_isMin : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : PredOrder α] {a : α},
  ¬IsMin a → ∀ (b : α), Finset.Ioc (Order.pred a) (Order.pred b) = Finset.Ico a b
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.one_comul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M : C) [inst_3 : CategoryTheory.BimonObj M],
  CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one CategoryTheory.ComonObj.comul =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.one CategoryTheory.MonObj.one)
-- Init.Data.UInt.Bitwise
UInt16.neg_eq_not_add : ∀ (a : UInt16), -a = ~~~a + 1
-- Mathlib.Order.RelIso.Basic
/-- The map `DFunLike.coe : (r ≃r s) → (α → β)` is injective.  -/
RelIso.coe_fn_injective : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop}, Function.Injective fun f => ⇑f
-- Mathlib.Topology.Order.Basic
IsLowerSet.isClosed : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [WellFoundedGT α] {s : Set α},
  IsLowerSet s → IsClosed s
-- Mathlib.Data.Ordmap.Ordset
Ordnode.valid_nil : ∀ {α : Type u_1} [inst : Preorder α], Ordnode.nil.Valid
-- Batteries.Lean.NameMapAttribute
/-- Add the given k,v pair to the NameMapExtension.  -/
Lean.NameMapExtension.add : {M : Type → Type} →
  {α : Type} → [Monad M] → [Lean.MonadEnv M] → [Lean.MonadError M] → Lean.NameMapExtension α → Lean.Name → α → M Unit
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getD_modify_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k : α}
  {fallback : β k} {f : β k → β k}, (m.modify k f).getD k fallback = (Option.map f (m.get? k)).getD fallback
-- Mathlib.Analysis.Normed.Field.UnitBall
Metric.unitClosedBall.coe_one : ∀ {𝕜 : Type u_1} [inst : SeminormedRing 𝕜] [inst_1 : NormOneClass 𝕜], ↑1 = 1
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
measure_Ioo_lt_top : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [CompactIccSpace α] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure μ] {a b : α}, μ (Set.Ioo a b) < ⊤
-- Mathlib.Data.Int.Basic
Int.gcd_emod : ∀ (m n : ℤ), (m % n).gcd n = m.gcd n
-- Mathlib.Topology.Order.IntermediateValue
IsPreconnected.intermediate_value₂_eventually₂ : ∀ {X : Type u} {α : Type v} [inst : TopologicalSpace X] [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α]
  [OrderClosedTopology α] {s : Set X},
  IsPreconnected s →
    ∀ {l₁ l₂ : Filter X} [l₁.NeBot] [l₂.NeBot],
      l₁ ≤ Filter.principal s →
        l₂ ≤ Filter.principal s →
          ∀ {f g : X → α}, ContinuousOn f s → ContinuousOn g s → f ≤ᶠ[l₁] g → g ≤ᶠ[l₂] f → ∃ x ∈ s, f x = g x
-- Mathlib.GroupTheory.Sylow
/-- The fixed points of the action of `H` on its cosets correspond to `normalizer H / H`.  -/
Sylow.fixedPointsMulLeftCosetsEquivQuotient : {G : Type u} →
  [inst : Group G] →
    (H : Subgroup G) →
      [Finite ↑↑H] →
        ↑(MulAction.fixedPoints (↥H) (G ⧸ H)) ≃
          ↥(Subgroup.normalizer ↑H) ⧸ Subgroup.comap (Subgroup.normalizer ↑H).subtype H
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
/-- `curry'` and `uncurry'` are inverse bijections.  -/
CategoryTheory.MonoidalClosed.curry'_uncurry' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  [inst_2 : CategoryTheory.Closed X] (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ X ⟹ Y),
  CategoryTheory.MonoidalClosed.curry' (CategoryTheory.MonoidalClosed.uncurry' g) = g
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CallHierarchyIncomingCallsParams.mk : Lean.Lsp.CallHierarchyItem → Lean.Lsp.CallHierarchyIncomingCallsParams
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.vaddSet.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β], Set.vaddSet = { vadd := fun a => Set.image fun x => a +ᵥ x }
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.Units.regulator.congr_simp : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.Units.regulator K = NumberField.Units.regulator K
-- Mathlib.Order.Interval.Set.Fin
Fin.range_natAdd : ∀ (m n : ℕ), Set.range (Fin.natAdd m) = {i | m ≤ ↑i}
-- Mathlib.Algebra.Polynomial.Basic
/-- **Alias** of `Polynomial.support_monomial_subset`. -/
Polynomial.support_monomial' : ∀ {R : Type u} [inst : Semiring R] (n : ℕ) (a : R), ((Polynomial.monomial n) a).support ⊆ {n}
-- Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
LinearIsometryEquiv.toSpanUnitSingleton.congr_simp : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedDivisionRing 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : NormSMulClass 𝕜 E] (x : E) (hx : ‖x‖ = 1),
  LinearIsometryEquiv.toSpanUnitSingleton x hx = LinearIsometryEquiv.toSpanUnitSingleton x hx
-- Mathlib.RingTheory.TensorProduct.MvPolynomial
MvPolynomial.tensorEquivSum.eq_1 : ∀ (R : Type u) [inst : CommSemiring R] (σ : Type u_1) (ι : Type u_2) (S : Type u_3) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S],
  MvPolynomial.tensorEquivSum R σ ι S =
    (AlgEquiv.restrictScalars S (MvPolynomial.algebraTensorAlgEquiv R (MvPolynomial σ S))).trans
      ((MvPolynomial.sumAlgEquiv S ι σ).symm.trans (MvPolynomial.renameEquiv S (Equiv.sumComm ι σ)))
-- Mathlib.CategoryTheory.Monoidal.Comon_
/-- The property that a morphism between comonoid objects is a comonoid morphism.  -/
CategoryTheory.IsComonHom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {M N : C} → [CategoryTheory.ComonObj M] → [CategoryTheory.ComonObj N] → (M ⟶ N) → Prop
-- Init.Data.SInt.Bitwise
UInt8.toInt8_xor : ∀ (a b : UInt8), (a ^^^ b).toInt8 = a.toInt8 ^^^ b.toInt8
-- Mathlib.Order.LiminfLimsup
Filter.liminf_const : ∀ {β : Type u_2} {α : Type u_6} [inst : ConditionallyCompleteLattice β] {f : Filter α} [f.NeBot] (b : β),
  Filter.liminf (fun x => b) f = b
-- Mathlib.Order.SuccPred.Limit
Order.IsSuccPrelimit.le_iff_forall_le : ∀ {α : Type u_1} {a b : α} [inst : LinearOrder α], Order.IsSuccPrelimit a → (a ≤ b ↔ ∀ c < a, c ≤ b)
-- Mathlib.Order.Filter.AtTopBot.Archimedean
/-- See also `Filter.Tendsto.atBot_mul_const_of_neg` for a version of this lemma for
linearly ordered fields which does not require the `Archimedean` assumption.  -/
Filter.Tendsto.atBot_mul_const_of_neg' : ∀ {α : Type u_1} {R : Type u_2} {l : Filter α} {f : α → R} {r : R} [inst : Ring R] [inst_1 : LinearOrder R]
  [IsStrictOrderedRing R] [Archimedean R],
  r < 0 → Filter.Tendsto f l Filter.atBot → Filter.Tendsto (fun x => f x * r) l Filter.atTop
-- Mathlib.Logic.Small.Set
small_univ : ∀ {α : Type u1} [h : Small.{u, u1} α], Small.{u, u1} ↑Set.univ
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.Internal.List.insertListIfNewUnit.match_1.splitter : {α : Type u_1} →
  (motive : List α → Sort u_2) →
    (toInsert : List α) → (Unit → motive []) → ((hd : α) → (tl : List α) → motive (hd :: tl)) → motive toInsert
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- The norm of a maximal ideal is `> 1`  -/
NumberField.HeightOneSpectrum.one_lt_absNorm : ∀ {R : Type u_2} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
  [Module.Finite ℤ R] [inst_3 : Module.Free ℤ R], 1 < Ideal.absNorm v.asIdeal
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithTerminal.widePullbackShapeEquivObj.match_1.splitter : {J : Type u_1} →
  (motive : CategoryTheory.Limits.WidePullbackShape J → Sort u_2) →
    (x : CategoryTheory.Limits.WidePullbackShape J) → ((x : J) → motive (some x)) → (Unit → motive none) → motive x
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.symm_comp_ofMulEquivOfLocalizations_apply : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {k : N ≃* P} (x : M),
  k.symm ((f.ofMulEquivOfLocalizations k) x) = f x
-- Mathlib.Data.Nat.Choose.Basic
Nat.choose_eq_one_iff : ∀ {n k : ℕ}, n.choose k = 1 ↔ k = 0 ∨ n = k
-- Mathlib.Data.Finmap
Finmap.mem_keys : ∀ {α : Type u} {β : α → Type v} {a : α} {s : Finmap β}, a ∈ s.keys ↔ a ∈ s
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftFunctorAdd_assoc : ∀ (C : Type u) {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (a₁ a₂ a₃ : A),
  CategoryTheory.shiftFunctorAdd C (a₁ + a₂) a₃ ≪≫
      CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.shiftFunctorAdd C a₁ a₂)
          (CategoryTheory.shiftFunctor C a₃) ≪≫
        (CategoryTheory.shiftFunctor C a₁).associator (CategoryTheory.shiftFunctor C a₂)
          (CategoryTheory.shiftFunctor C a₃) =
    CategoryTheory.shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯ ≪≫
      (CategoryTheory.shiftFunctor C a₁).isoWhiskerLeft (CategoryTheory.shiftFunctorAdd C a₂ a₃)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Substructure
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Substructure.0.Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go.match_5.eq_4 : ∀ (motive : Std.Tactic.BVDecide.BVLogicalExpr → Sort u_1)
  (discr lhs rhs : Std.Tactic.BVDecide.BoolExpr Std.Tactic.BVDecide.BVPred)
  (h_1 : (var : Std.Tactic.BVDecide.BVPred) → motive (Std.Tactic.BVDecide.BoolExpr.literal var))
  (h_2 : (val : Bool) → motive (Std.Tactic.BVDecide.BoolExpr.const val))
  (h_3 : (expr : Std.Tactic.BVDecide.BoolExpr Std.Tactic.BVDecide.BVPred) → motive expr.not)
  (h_4 : (discr lhs rhs : Std.Tactic.BVDecide.BoolExpr Std.Tactic.BVDecide.BVPred) → motive (discr.ite lhs rhs))
  (h_5 :
    (g : Std.Tactic.BVDecide.Gate) →
      (lhs rhs : Std.Tactic.BVDecide.BoolExpr Std.Tactic.BVDecide.BVPred) →
        motive (Std.Tactic.BVDecide.BoolExpr.gate g lhs rhs)),
  (match discr.ite lhs rhs with
    | Std.Tactic.BVDecide.BoolExpr.literal var => h_1 var
    | Std.Tactic.BVDecide.BoolExpr.const val => h_2 val
    | expr.not => h_3 expr
    | discr.ite lhs rhs => h_4 discr lhs rhs
    | Std.Tactic.BVDecide.BoolExpr.gate g lhs rhs => h_5 g lhs rhs) =
    h_4 discr lhs rhs
-- Std.Data.TreeSet.Raw.Basic
/-- Creates a new empty tree set. It is also possible and recommended to
use the empty collection notations `∅` and `{}` to create an empty tree set. `simp` replaces
`empty` with `∅`.
 -/
Std.TreeSet.Raw.foldlM : {α : Type u} →
  {cmp : α → α → Ordering} →
    {δ : Type w} → {m : Type w → Type w₂} → [Monad m] → (δ → α → m δ) → δ → Std.TreeSet.Raw α cmp → m δ
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.Const.alterKey.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (v : β) (h_1 : Unit → motive none) (h_2 : (v : β) → motive (some v)),
  (match some v with
    | none => h_1 ()
    | some v => h_2 v) =
    h_2 v
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape
CategoryTheory.Limits.instHasIterationOfShapeOfHasColimitsOfSize : ∀ (J : Type w) [inst : LinearOrder J] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v, u} C], CategoryTheory.Limits.HasIterationOfShape J C
-- Mathlib.Algebra.Module.LinearMap.End
Module.End.apply_isScalarTower : ∀ {R : Type u_1} {S : Type u_3} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Monoid S] [inst_4 : DistribMulAction S M] [inst_5 : SMulCommClass R S M], IsScalarTower S (Module.End R M) M