mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.Hom.id_comp : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {R' : Type u_1} {S' : Type u_2} [inst_3 : CommRing R'] [inst_4 : CommRing S'] [inst_5 : Algebra R' S']
  {P' : Algebra.Extension R' S'} [inst_6 : Algebra R R'] [inst_7 : Algebra S S'] (f : P.Hom P'),
  (Algebra.Extension.Hom.id P').comp f = f
-- Mathlib.Data.Nat.Factorial.SuperFactorial
_private.Mathlib.Data.Nat.Factorial.SuperFactorial.0.Nat.factorial.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.functorPullback_pullback : ∀ {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} (f : X ⟶ Y) (S : CategoryTheory.Sieve (F.obj Y)),
  CategoryTheory.Sieve.functorPullback F (CategoryTheory.Sieve.pullback (F.map f) S) =
    CategoryTheory.Sieve.pullback f (CategoryTheory.Sieve.functorPullback F S)
-- Init.Data.Array.Bootstrap
Array.foldrM.fold.congr_simp : ∀ {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (f f_1 : α → β → m β),
  f = f_1 →
    ∀ (as as_1 : Array α) (e_as : as = as_1) (stop stop_1 : ℕ),
      stop = stop_1 →
        ∀ (i i_1 : ℕ) (e_i : i = i_1) (h : i ≤ as.size) (b b_1 : β),
          b = b_1 → Array.foldrM.fold f as stop i h b = Array.foldrM.fold f_1 as_1 stop_1 i_1 ⋯ b_1
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- `b.reindex (e : ι ≃ ι')` is an `OrthonormalBasis` indexed by `ι'`  -/
OrthonormalBasis.reindex : {ι : Type u_1} →
  {ι' : Type u_2} →
    {𝕜 : Type u_3} →
      [inst : RCLike 𝕜] →
        {E : Type u_4} →
          [inst_1 : NormedAddCommGroup E] →
            [inst_2 : InnerProductSpace 𝕜 E] →
              [inst_3 : Fintype ι] → [inst_4 : Fintype ι'] → OrthonormalBasis ι 𝕜 E → ι ≃ ι' → OrthonormalBasis ι' 𝕜 E
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
fixingAddSubgroup.eq_1 : ∀ (M : Type u_1) {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] (s : Set α),
  fixingAddSubgroup M s = { toAddSubmonoid := fixingAddSubmonoid M s, neg_mem' := ⋯ }
-- Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty
UpperHalfPlane.atImInfty_basis : UpperHalfPlane.atImInfty.HasBasis (fun x => True) fun i => UpperHalfPlane.im ⁻¹' Set.Ici i
-- Mathlib.Order.CompleteBooleanAlgebra
_private.Mathlib.Order.CompleteBooleanAlgebra.0.Order.Frame.MinimalAxioms.sSup_inf_eq : ∀ {α : Type u} (s : Set α) (b : α) [inst : CompleteLattice α], Order.Frame.MinimalAxioms α → sSup s ⊓ b = ⨆ a ∈ s, a ⊓ b
-- Mathlib.CategoryTheory.Category.Quiv
CategoryTheory.Quiv.instInhabited : Inhabited CategoryTheory.Quiv
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
/-- Constructs an instance of `CartesianMonoidalCategory C` given the existence of finite products
in `C`.  -/
CategoryTheory.CartesianMonoidalCategory.ofHasFiniteProducts : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasFiniteProducts C] → CategoryTheory.CartesianMonoidalCategory C
-- Mathlib.Algebra.Category.CommBialgCat
/-- Bialgebra equivalences between `Bialgebra`s are the same as isomorphisms in `CommBialgCat`.  -/
CommBialgCat.isoEquivBialgEquiv : {R : Type u} →
  [inst : CommRing R] →
    {X Y : Type v} →
      [inst_1 : CommRing X] →
        [inst_2 : Bialgebra R X] →
          [inst_3 : CommRing Y] → [inst_4 : Bialgebra R Y] → (CommBialgCat.of R X ≅ CommBialgCat.of R Y) ≃ X ≃ₐc[R] Y
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey!_maxKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t ≠ ∅ → t.getKey! t.maxKey! = t.maxKey!
-- Mathlib.CategoryTheory.ObjectProperty.Basic
/-- The typeclass associated to `P : ObjectProperty C`.  -/
CategoryTheory.ObjectProperty.Is : {C : Type u} → [inst : CategoryTheory.CategoryStruct.{v, u} C] → CategoryTheory.ObjectProperty C → C → Prop
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)}
  {sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)}
  (obj : (i : ι) → ↑(F.obj { as := Opposite.op (X i) }))
  (hom :
    (i j : ι) → (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj j))
  (pullHom'_hom_self :
    ∀ (i : ι),
      CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom (f i) (CategoryTheory.CategoryStruct.id (X i))
          (CategoryTheory.CategoryStruct.id (X i)) ⋯ ⋯ =
        CategoryTheory.CategoryStruct.id
          ((F.map (CategoryTheory.CategoryStruct.id (X i)).op.toLoc).toFunctor.obj (obj i)))
  (pullHom'_hom_comp :
    ∀ (i₁ i₂ i₃ : ι),
      CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯
            ⋯)
          (CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ ⋯
            ⋯) =
        CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯)
  (obj_1 : (i : ι) → ↑(F.obj { as := Opposite.op (X i) }))
  (hom_1 :
    (i j : ι) →
      (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj_1 i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj_1 j))
  (pullHom'_hom_self_1 :
    ∀ (i : ι),
      CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom_1 (f i) (CategoryTheory.CategoryStruct.id (X i))
          (CategoryTheory.CategoryStruct.id (X i)) ⋯ ⋯ =
        CategoryTheory.CategoryStruct.id
          ((F.map (CategoryTheory.CategoryStruct.id (X i)).op.toLoc).toFunctor.obj (obj_1 i)))
  (pullHom'_hom_comp_1 :
    ∀ (i₁ i₂ i₃ : ι),
      CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom_1 (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂
            ⋯ ⋯)
          (CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom_1 (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃
            ⋯ ⋯) =
        CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom_1 (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯
          ⋯),
  ({ obj := obj, hom := hom, pullHom'_hom_self := pullHom'_hom_self, pullHom'_hom_comp := pullHom'_hom_comp } =
      { obj := obj_1, hom := hom_1, pullHom'_hom_self := pullHom'_hom_self_1,
        pullHom'_hom_comp := pullHom'_hom_comp_1 }) =
    (obj = obj_1 ∧ hom ≍ hom_1)
-- Mathlib.RingTheory.MvPowerSeries.Trunc
MvPowerSeries.constantCoeff_truncTotal_eq_ite : ∀ {σ : Type u_1} {R : Type u_2} {n : ℕ} [inst : Finite σ] [inst_1 : CommSemiring R] (p : MvPowerSeries σ R),
  MvPolynomial.constantCoeff ((MvPowerSeries.truncTotal n) p) = if 0 < n then MvPowerSeries.constantCoeff p else 0
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.List.forIn'_cons.match_1.splitter : {β : Type u_1} →
  (motive : ForInStep β → Sort u_2) →
    (x : ForInStep β) → ((b : β) → motive (ForInStep.done b)) → ((b : β) → motive (ForInStep.yield b)) → motive x
-- Mathlib.Probability.Martingale.Convergence
/-- An L¹-bounded submartingale converges almost everywhere.  -/
MeasureTheory.Submartingale.exists_ae_tendsto_of_bdd : ∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0}
  {f : ℕ → Ω → ℝ} {R : NNReal} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.Submartingale f ℱ μ →
    (∀ (n : ℕ), MeasureTheory.eLpNorm (f n) 1 μ ≤ ↑R) →
      ∀ᵐ (ω : Ω) ∂μ, ∃ c, Filter.Tendsto (fun n => f n ω) Filter.atTop (nhds c)
-- Mathlib.Data.Finset.Card
/-- Given an injective map `f : α → β` for finite sets `s ⊂ α` and `t ⊂ β` such that `t` has
cardinality one more than `s`, there exists a unique element of `t` not in `f(s)`.  -/
Finset.existsUnique_notMem_image_of_injOn_of_card_eq_add_one : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α → β} {t : Finset β} [inst : DecidableEq β],
  Set.InjOn f ↑s → Set.MapsTo f ↑s ↑t → t.card = s.card + 1 → ∃! x, x ∈ t ∧ x ∉ Finset.image f s
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arccos_nonneg : ∀ (x : ℝ), 0 ≤ Real.arccos x
-- Mathlib.MeasureTheory.Group.LIntegral
/-- For nonzero regular left invariant measures, the integral of a continuous nonnegative function
`f` is 0 iff `f` is 0.  -/
MeasureTheory.lintegral_eq_zero_of_isMulLeftInvariant : ∀ {G : Type u_1} [inst : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_1 : TopologicalSpace G]
  [inst_2 : Group G] [IsTopologicalGroup G] [BorelSpace G] [μ.IsMulLeftInvariant] [μ.Regular] [NeZero μ]
  {f : G → ENNReal}, Continuous f → (∫⁻ (x : G), f x ∂μ = 0 ↔ f = 0)
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.homMk_hom₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  (A B : CategoryTheory.Pretriangulated.Triangle C) (hom₁ : A.obj₁ ⟶ B.obj₁) (hom₂ : A.obj₂ ⟶ B.obj₂)
  (hom₃ : A.obj₃ ⟶ B.obj₃)
  (comm₁ :
    autoParam (CategoryTheory.CategoryStruct.comp A.mor₁ hom₂ = CategoryTheory.CategoryStruct.comp hom₁ B.mor₁)
      CategoryTheory.Pretriangulated.Triangle.homMk._auto_1)
  (comm₂ :
    autoParam (CategoryTheory.CategoryStruct.comp A.mor₂ hom₃ = CategoryTheory.CategoryStruct.comp hom₂ B.mor₂)
      CategoryTheory.Pretriangulated.Triangle.homMk._auto_3)
  (comm₃ :
    autoParam
      (CategoryTheory.CategoryStruct.comp A.mor₃ ((CategoryTheory.shiftFunctor C 1).map hom₁) =
        CategoryTheory.CategoryStruct.comp hom₃ B.mor₃)
      CategoryTheory.Pretriangulated.Triangle.homMk._auto_5),
  (A.homMk B hom₁ hom₂ hom₃ comm₁ comm₂ comm₃).hom₁ = hom₁
-- Mathlib.Algebra.Group.End
/-- `extendDomain` as a group homomorphism  -/
Equiv.Perm.extendDomainHom : {α : Type u_4} → {β : Type u_5} → {p : β → Prop} → [DecidablePred p] → α ≃ Subtype p → Equiv.Perm α →* Equiv.Perm β
-- Mathlib.Algebra.Ring.Submonoid.Pointwise
AddSubmonoid.smul_subset_smul : ∀ {R : Type u_2} {A : Type u_3} [inst : AddMonoid R] [inst_1 : AddMonoid A] [inst_2 : DistribSMul R A]
  {M : AddSubmonoid R} {N : AddSubmonoid A}, ↑M • ↑N ⊆ ↑(M • N)
-- Mathlib.Combinatorics.Quiver.Basic
Quiver.empty_arrow : ∀ {V : Type u} (a b : Quiver.Empty V), (a ⟶ b) = PEmpty.{u + 1}
-- Mathlib.Data.Sym.Basic
Sym.coe_attach : ∀ {α : Type u_1} {n : ℕ} (s : Sym α n), ↑s.attach = (↑s).attach
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- The inf of two submonoids is their intersection.  -/
Submonoid.instMin : {M : Type u_1} → [inst : MulOneClass M] → Min (Submonoid M)
-- Mathlib.Order.Filter.AtTopBot.Monoid
Filter.Tendsto.atBot_add_eventuallyLE_zero : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : Preorder M] [IsOrderedAddMonoid M] {l : Filter α}
  {f g : α → M}, Filter.Tendsto f l Filter.atBot → g ≤ᶠ[l] 0 → Filter.Tendsto (fun x => f x + g x) l Filter.atBot
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Finsupp.linearCombination_zero_apply : ∀ {α : Type u_1} {M : Type u_2} (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (x : α →₀ R), (Finsupp.linearCombination R 0) x = 0
-- Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
CategoryTheory.SmallObject.SuccStruct.restrictionLTOfCoconeIso_inv_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {J : Type u} [inst_1 : LinearOrder J] {j : J}
  {F : CategoryTheory.Functor (↑(Set.Iio j)) C} (c : CategoryTheory.Limits.Cocone F) (X : ↑(Set.Iio j)),
  (CategoryTheory.SmallObject.SuccStruct.restrictionLTOfCoconeIso c).inv.app X =
    (CategoryTheory.SmallObject.SuccStruct.ofCoconeObjIso c ↑X ⋯).inv
-- Mathlib.Analysis.Real.OfDigits
Real.continuous_ofDigits : ∀ {b : ℕ}, Continuous Real.ofDigits
-- Mathlib.Algebra.Category.Ring.Limits
/-- The forgetful functor from commutative rings to commutative semirings preserves all limits.
(That is, the underlying commutative semirings could have been computed instead as limits
in the category of commutative semirings.)
 -/
CommRingCat.forget₂CommSemiRing_preservesLimitsOfSize : ∀ [UnivLE.{v, u}],
  CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1}
    (CategoryTheory.forget₂ CommRingCat CommSemiRingCat)
-- Mathlib.NumberTheory.LSeries.Basic
LSeries.mul_delta_eq_smul_delta : ∀ {f : ℕ → ℂ}, f * LSeries.delta = f 1 • LSeries.delta
-- Mathlib.Order.SuccPred.Basic
Order.Ioi_pred_eq_insert_of_not_isMin : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {a : α},
  ¬IsMin a → Set.Ioi (Order.pred a) = insert a (Set.Ioi a)
-- Mathlib.CategoryTheory.Functor.CurryingThree
CategoryTheory.Functor.flip₁₃_map_app_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_4} C₃]
  [inst_3 : CategoryTheory.Category.{v_9, u_9} E]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))) {X Y : C₃} (h : X ⟶ Y)
  (X_1 : C₂) (Y_1 : C₁), ((F.flip₁₃.map h).app X_1).app Y_1 = ((F.obj Y_1).obj X_1).map h
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.map_comap_eq_of_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {f : M →ₙ* N},
  Function.Surjective ⇑f → ∀ (S : Subsemigroup N), Subsemigroup.map f (Subsemigroup.comap f S) = S
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.UnitMonomial.toFun_tendsto_top_of_head_pos : ∀ {exps_hd : ℝ} {exps_tl : Tactic.ComputeAsymptotics.UnitMonomial} {basis_hd : ℝ → ℝ}
  {basis_tl : Tactic.ComputeAsymptotics.Basis},
  Tactic.ComputeAsymptotics.WellFormedBasis (basis_hd :: basis_tl) →
    0 < exps_hd →
      Filter.Tendsto (Tactic.ComputeAsymptotics.UnitMonomial.toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl))
        Filter.atTop Filter.atTop
-- Std.Data.ExtHashMap.Basic
Std.ExtHashMap.instBEqOfEquivBEqOfLawfulHashable : {α : Type u} →
  {β : Type v} →
    {x : BEq α} → {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → [BEq β] → BEq (Std.ExtHashMap α β)
-- Init.Data.UInt.Lemmas
UInt32.ofNat_mod : ∀ {a b : ℕ}, a < 2 ^ 32 → b < 2 ^ 32 → UInt32.ofNat (a % b) = UInt32.ofNat a % UInt32.ofNat b
-- Mathlib.CategoryTheory.Limits.Constructions.Equalizers
/-- Define the equalizing morphism  -/
CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.pushoutInl : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C] →
      [inst_2 : CategoryTheory.Limits.HasPushouts C] →
        (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C) →
          F.obj CategoryTheory.Limits.WalkingParallelPair.one ⟶
            CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.constructCoequalizer F
-- Mathlib.Algebra.Order.Group.PosPart
one_lt_oneLePart_iff : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : Group α] {a : α}, 1 < a⁺ᵐ ↔ 1 < a
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.mopEquiv_functor : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C],
  (CategoryTheory.MonoidalOpposite.mopEquiv C).functor = CategoryTheory.mopFunctor C
-- Aesop.RuleTac.Forward
Aesop.RuleTac.forwardMatch : Aesop.ForwardRuleMatch → Aesop.RuleTac
-- Init.Data.Nat.Lcm
Nat.lcm_eq_iff : ∀ {n m l : ℕ}, n.lcm m = l ↔ n ∣ l ∧ m ∣ l ∧ ∀ (c : ℕ), n ∣ c → m ∣ c → l ∣ c
-- Mathlib.CategoryTheory.Limits.Cones
/-- A cone morphism between two cones for the same diagram is a morphism of the cone points which
commutes with the cone legs.  -/
CategoryTheory.Limits.ConeMorphism : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} → CategoryTheory.Limits.Cone F → CategoryTheory.Limits.Cone F → Type v₃
-- Init.Data.Array.Count
Array.countP_push_of_pos : ∀ {α : Type u_1} {p : α → Bool} {a : α} {xs : Array α}, p a = true → Array.countP p (xs.push a) = Array.countP p xs + 1
-- Mathlib.Geometry.Manifold.HasGroupoid
StructureGroupoid.compatible_of_mem_maximalAtlas_left : ∀ {H : Type u} {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  {G : StructureGroupoid H} {e' : OpenPartialHomeomorph M H} {x : M},
  e' ∈ StructureGroupoid.maximalAtlas M G → e'.symm.trans (chartAt H x) ∈ G
-- Mathlib.Analysis.SpecialFunctions.JapaneseBracket
integrable_rpow_neg_one_add_norm_sq : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {r : ℝ},
  ↑(Module.finrank ℝ E) < r → MeasureTheory.Integrable (fun x => (1 + ‖x‖ ^ 2) ^ (-r / 2)) μ
-- Mathlib.Data.Set.Countable
Set.countable_iUnion_iff : ∀ {α : Type u} {ι : Sort x} [Countable ι] {t : ι → Set α}, (⋃ i, t i).Countable ↔ ∀ (i : ι), (t i).Countable
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.LambdaTheorem.mk : Lean.Name → Lean.Name → Mathlib.Meta.FunProp.LambdaTheoremArgs → Mathlib.Meta.FunProp.LambdaTheorem
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
/-- **Alias** of `MeasureTheory.locallyIntegrable_finsetSum`. -/
MeasureTheory.locallyIntegrable_finset_sum : ∀ {X : Type u_1} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] {μ : MeasureTheory.Measure X}
  {ε''' : Type u_9} [inst_2 : TopologicalSpace ε'''] [inst_3 : ESeminormedAddCommMonoid ε'''] [ContinuousAdd ε''']
  {ι : Type u_10} (s : Finset ι) {f : ι → X → ε'''},
  (∀ i ∈ s, MeasureTheory.LocallyIntegrable (f i) μ) → MeasureTheory.LocallyIntegrable (fun a => ∑ i ∈ s, f i a) μ
-- Mathlib.Algebra.Category.CommHopfAlgCat
CommHopfAlgCat.ofHom_hom : ∀ {R : Type u} [inst : CommRing R] {A B : CommHopfAlgCat R} (f : A ⟶ B),
  CommHopfAlgCat.ofHom (CommHopfAlgCat.Hom.hom f) = f
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
PiTensorProduct.liftIsometry_comp_mapL : ∀ {ι : Type u_1} [inst : Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] {F : Type u_4}
  [inst_4 : SeminormedAddCommGroup F] [inst_5 : NormedSpace 𝕜 F] {E' : ι → Type u_5}
  [inst_6 : (i : ι) → SeminormedAddCommGroup (E' i)] [inst_7 : (i : ι) → NormedSpace 𝕜 (E' i)]
  (f : (i : ι) → E i →L[𝕜] E' i) (h : ContinuousMultilinearMap 𝕜 E' F),
  (PiTensorProduct.liftIsometry 𝕜 E' F) h ∘SL PiTensorProduct.mapL f =
    (PiTensorProduct.liftIsometry 𝕜 E F) (h.compContinuousLinearMap f)
-- Mathlib.Data.List.Lattice
/-- **Alias** of `List.cons_bagInter`. -/
List.cons_bagInteger : ∀ {α : Type u_1} {l₁ l₂ : List α} {a : α} [inst : DecidableEq α],
  (a :: l₁).bagInter l₂ = if a ∈ l₂ then a :: l₁.bagInter (l₂.erase a) else l₁.bagInter l₂
-- Mathlib.LinearAlgebra.Trace
Matrix.trace_map' : ∀ {K : Type u_6} {m : Type u_7} {F : Type u_8} [inst : Field K] [inst_1 : Fintype m] [inst_2 : DecidableEq m]
  [inst_3 : FunLike F (Matrix m m K) (Matrix m m K)] [AlgHomClass F K (Matrix m m K) (Matrix m m K)] (f : F)
  (x : Matrix m m K), (f x).trace = x.trace
-- Mathlib.Analysis.Complex.Polynomial.Basic
Polynomial.Gal.galActionHom.congr_simp : ∀ {F : Type u_1} [inst : Field F] (p : Polynomial F) (E : Type u_2) [inst_1 : Field E] [inst_2 : Algebra F E]
  [inst_3 : Fact (Polynomial.map (algebraMap F E) p).Splits],
  Polynomial.Gal.galActionHom p E = Polynomial.Gal.galActionHom p E
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.Hom.id_h₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) (x : E.I₀),
  (CategoryTheory.PreZeroHypercover.Hom.id E).h₀ x = CategoryTheory.CategoryStruct.id (E.X x)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
one_lt_mul_of_lt_of_le : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : Preorder M₀] {a b : M₀} [ZeroLEOneClass M₀] [PosMulMono M₀],
  1 < a → 1 ≤ b → 1 < a * b
-- Mathlib.Analysis.Calculus.ParametricIntegral
/-- Derivative under integral of `x ↦ ∫ F x a` at a given point `x₀ : 𝕜`, `𝕜 = ℝ` or `𝕜 = ℂ`,
assuming `F x₀` is integrable, `x ↦ F x a` is locally Lipschitz on a neighborhood of `x₀` for ae `a`
(with a neighborhood independent of `a`) with integrable Lipschitz bound, and `F x` is
ae-measurable for `x` in a possibly smaller neighborhood of `x₀`.  -/
hasDerivAt_integral_of_dominated_loc_of_lip : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {𝕜 : Type u_2} [inst_1 : RCLike 𝕜]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace 𝕜 E] {bound : α → ℝ}
  {F : 𝕜 → α → E} {x₀ : 𝕜} {s : Set 𝕜} {F' : α → E},
  s ∈ nhds x₀ →
    (∀ᶠ (x : 𝕜) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) μ) →
      MeasureTheory.Integrable (F x₀) μ →
        MeasureTheory.AEStronglyMeasurable F' μ →
          (∀ᵐ (a : α) ∂μ, LipschitzOnWith (Real.nnabs (bound a)) (fun x => F x a) s) →
            MeasureTheory.Integrable bound μ →
              (∀ᵐ (a : α) ∂μ, HasDerivAt (fun x => F x a) (F' a) x₀) →
                MeasureTheory.Integrable F' μ ∧ HasDerivAt (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Matrix.BlockTriangular.eq_1 : ∀ {α : Type u_1} {m : Type u_3} {R : Type v} [inst : LT α] [inst_1 : Zero R] (M : Matrix m m R) (b : m → α),
  M.BlockTriangular b = ∀ ⦃i j : m⦄, b j < b i → M i j = 0
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.add_apply : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} (f f' : M [⋀^ι]→ₗ[R] N) (v : ι → M),
  (f + f') v = f v + f' v
-- Mathlib.Topology.Separation.Hausdorff
eqOn_closure₂' : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {Z : Type u_3} [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] [T2Space Z] {s : Set X} {t : Set Y} {f g : X → Y → Z},
  (∀ x ∈ s, ∀ y ∈ t, f x y = g x y) →
    (∀ (x : X), Continuous (f x)) →
      (∀ (y : Y), Continuous fun x => f x y) →
        (∀ (x : X), Continuous (g x)) →
          (∀ (y : Y), Continuous fun x => g x y) → ∀ x ∈ closure s, ∀ y ∈ closure t, f x y = g x y
-- Mathlib.Data.PNat.Xgcd
/-- Another `mk` using ℕ and ℕ+  -/
PNat.XgcdType.mk' : ℕ+ → ℕ → ℕ → ℕ+ → ℕ+ → ℕ+ → PNat.XgcdType
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- `AddMonoid.SMul` is measurable.  -/
AddMonoid.measurableSMul_nat₂ : ∀ (M : Type u_6) [inst : AddMonoid M] [inst_1 : MeasurableSpace M] [MeasurableAdd₂ M], MeasurableSMul₂ ℕ M
-- Mathlib.MeasureTheory.Group.Convolution
/-- Convolution of a measure μ with the zero measure returns the zero measure.  -/
MeasureTheory.Measure.mconv_zero : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : MeasurableSpace M] (μ : MeasureTheory.Measure M), μ.mconv 0 = 0
-- Mathlib.Topology.MetricSpace.Pseudo.Pi
nndist_pi_le_iff : ∀ {β : Type u_2} {X : β → Type u_3} [inst : Fintype β] [inst_1 : (b : β) → PseudoMetricSpace (X b)]
  {f g : (b : β) → X b} {r : NNReal}, nndist f g ≤ r ↔ ∀ (b : β), nndist (f b) (g b) ≤ r
-- Mathlib.Topology.Algebra.Monoid
IsCompact.mul : ∀ {N : Type u_4} [inst : TopologicalSpace N] [inst_1 : Mul N] [ContinuousMul N] {s t : Set N},
  IsCompact s → IsCompact t → IsCompact (s * t)