mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toArray_map_eq_toArray_filterMapM : ∀ {α β γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [WeaklyLawfulMonadAttach m] [inst_4 : Std.Iterator α m β] [Std.Iterators.Finite α m] {f : β → γ} {it : Std.IterM m β},
  (Std.IterM.map f it).toArray = (Std.IterM.filterMapM (fun b => pure (some (f b))) it).toArray
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
IsGaloisGroup.restrictHom.eq_1 : ∀ (G : Type u_1) (G' : Type u_2) [inst : Group G] [inst_1 : Group G'] (A : Type u_5) (B : Type u_6) (C : Type u_7)
  [inst_2 : CommRing A] [inst_3 : CommRing B] [inst_4 : CommRing C] [inst_5 : IsDomain C] [inst_6 : Algebra A B]
  [inst_7 : Algebra A C] [inst_8 : Algebra B C] [inst_9 : FaithfulSMul A B] [inst_10 : FaithfulSMul B C]
  [inst_11 : IsScalarTower A B C] [inst_12 : Finite G] [inst_13 : Finite G'] [inst_14 : MulSemiringAction G C]
  [inst_15 : IsGaloisGroup G A C] [inst_16 : MulSemiringAction G' B] [inst_17 : IsGaloisGroup G' A B],
  IsGaloisGroup.restrictHom G G' A B C =
    (IsGaloisGroup.quotientMulEquiv G G' (FractionRing A) (FractionRing B) (FractionRing C)
            (fixingSubgroup G (Set.range ⇑(algebraMap (FractionRing B) (FractionRing C))))).toMonoidHom.comp
      (QuotientGroup.mk' (fixingSubgroup G (Set.range ⇑(algebraMap (FractionRing B) (FractionRing C)))))
-- Mathlib.Analysis.Normed.Group.Uniform
dist_self_mul_right : ∀ {E : Type u_2} [inst : SeminormedGroup E] (a b : E), dist b (b * a) = ‖a‖
-- Std.Http.Data.Body.Empty
Std.Http.Body.Empty.mk : Std.Http.Body.Empty
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
PartialHomeomorph.ofContinuousOpenRestrict.congr_simp : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e e_1 : PartialEquiv X Y)
  (e_e : e = e_1) (hc : ContinuousOn (↑e) e.source) (ho : IsOpenMap (e.source.domRestrict ↑e)),
  PartialHomeomorph.ofContinuousOpenRestrict e hc ho = PartialHomeomorph.ofContinuousOpenRestrict e_1 ⋯ ⋯
-- Mathlib.Data.Vector.Mem
List.Vector.mem_succ_iff : ∀ {α : Type u_1} {n : ℕ} (a : α) (v : List.Vector α (n + 1)), a ∈ v.toList ↔ a = v.head ∨ a ∈ v.tail.toList
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.equation_zero : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R}, W'.Equation ![0, 1, 0]
-- Mathlib.Geometry.Euclidean.MongePoint
/-- Four points form an orthocentric system if they consist of the
vertices of a triangle and its orthocenter.  -/
EuclideanGeometry.OrthocentricSystem : {V : Type u_1} →
  {P : Type u_2} →
    [inst : NormedAddCommGroup V] →
      [InnerProductSpace ℝ V] → [inst_2 : MetricSpace P] → [NormedAddTorsor V P] → Set P → Prop
-- Std.Data.HashMap.Raw
/-- Inserts the given mapping into the map. If there is already a mapping for the given key, then both
key and value will be replaced.

Note: this replacement behavior is true for `HashMap`, `DHashMap`, `HashMap.Raw` and `DHashMap.Raw`.
The `insert` function on `HashSet` and `HashSet.Raw` behaves differently: it will return the set
unchanged if a matching key is already present.
 -/
Std.HashMap.Raw.insert : {α : Type u} → {β : Type v} → [beq : BEq α] → [Hashable α] → Std.HashMap.Raw α β → α → β → Std.HashMap.Raw α β
-- Mathlib.Algebra.Order.Group.Abs
/-- For an element `a` of a multiplicative linear ordered group,
either `|a|ₘ = a` and `1 ≤ a`, or `|a|ₘ = a⁻¹` and `a < 1`.  -/
mabs_cases : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] (a : G),
  |a|ₘ = a ∧ 1 ≤ a ∨ |a|ₘ = a⁻¹ ∧ a < 1
-- Mathlib.LinearAlgebra.Dimension.Constructions
Submodule.finrank_mono : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  {s t : Submodule R M} [Module.Finite R ↥t], s ≤ t → Module.finrank R ↥s ≤ Module.finrank R ↥t
-- Mathlib.Data.Rat.Cast.Order
NNRat.preimage_cast_uIoc : ∀ {K : Type u_5} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] (p q : ℚ≥0),
  NNRat.cast ⁻¹' Set.uIoc ↑p ↑q = Set.uIoc p q
-- Mathlib.Algebra.Field.TransferInstance
/-- Transfer `DivisionRing` across an `Equiv`  -/
Equiv.divisionRing : {α : Type u_1} → {β : Type u_2} → α ≃ β → [DivisionRing β] → DivisionRing α
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.inr.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ],
  CochainComplex.mappingCocone.inr φ =
    (CochainComplex.HomComplex.Cocycle.ofHom (CochainComplex.mappingCone.inr φ)).rightShift (-1) 1
      CochainComplex.mappingCocone.inr._proof_2
-- Mathlib.Tactic.GRewrite.Elab
_private.Mathlib.Tactic.GRewrite.Elab.0.Mathlib.Tactic.GRewrite.instEvalExprConfig : Lean.Elab.ConfigEval.EvalExpr Mathlib.Tactic.GRewrite.Config
-- Lean.Elab.MutualDef
/-- Snapshot for incremental processing of definition body.

Invariant: if the bundle's `old?` is set, then elaboration of the body is guaranteed to result in
the same elaboration result and state, i.e. reuse is possible.
 -/
Lean.Elab.DefViewElabHeader.bodySnap? : Lean.Elab.DefViewElabHeader → Option (Lean.Language.SnapshotBundle (Option Lean.Elab.BodyProcessedSnapshot))
-- Mathlib.RingTheory.Ideal.Cotangent
IsLocalRing.finrank_cotangentSpace_eq_zero : ∀ (R : Type u_2) [inst : Field R], Module.finrank (IsLocalRing.ResidueField R) (IsLocalRing.CotangentSpace R) = 0
-- Std.Data.HashMap.Lemmas
Std.HashMap.toList_keysArray : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β}, m.keysArray.toList = m.keys
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
FiniteDimensional.basisSingleton.congr_simp : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] (ι : Type u_1)
  [inst_3 : Unique ι] (h : Module.finrank K V = 1) (v v_1 : V) (e_v : v = v_1) (hv : v ≠ 0),
  FiniteDimensional.basisSingleton ι h v hv = FiniteDimensional.basisSingleton ι h v_1 ⋯
-- Mathlib.Data.Fin.Tuple.Basic
Fin.succAbove_cases_eq_insertNth : @Fin.succAboveCases = @Fin.insertNth
-- Mathlib.Analysis.Normed.Lp.PiLp
LinearIsometryEquiv.piLpCongrRight_symm : ∀ {p : ENNReal} {𝕜 : Type u_1} {ι : Type u_2} {α : ι → Type u_3} {β : ι → Type u_4} [hp : Fact (1 ≤ p)]
  [inst : Fintype ι] [inst_1 : Semiring 𝕜] [inst_2 : (i : ι) → SeminormedAddCommGroup (α i)]
  [inst_3 : (i : ι) → SeminormedAddCommGroup (β i)] [inst_4 : (i : ι) → Module 𝕜 (α i)]
  [inst_5 : (i : ι) → Module 𝕜 (β i)] (e : (i : ι) → α i ≃ₗᵢ[𝕜] β i),
  (LinearIsometryEquiv.piLpCongrRight p e).symm = LinearIsometryEquiv.piLpCongrRight p fun i => (e i).symm
-- Mathlib.Order.Defs.Unbundled
Std.Antisymm.decide : ∀ {α : Sort u_1} {r : α → α → Prop} [inst : DecidableRel r] [Std.Antisymm r],
  Std.Antisymm fun a b => decide (r a b) = true
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey?_alter!_eq_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {k : α} {f : Option (β k) → Option (β k)},
      (Std.DTreeMap.Internal.Impl.alter! k f t).maxKey? = some k ↔
        (f (t.get? k)).isSome = true ∧ ∀ k' ∈ t, (compare k' k).isLE = true
-- Mathlib.CategoryTheory.Retract
CategoryTheory.Retract.retract_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (self : CategoryTheory.Retract X Y) {Z : C}
  (h : X ⟶ Z), CategoryTheory.CategoryStruct.comp self.i (CategoryTheory.CategoryStruct.comp self.r h) = h
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.hom_right_inv_right : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Under X} (e : f ≅ g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Under.Hom.right e.hom) (CategoryTheory.Under.Hom.right e.inv) =
    CategoryTheory.CategoryStruct.id f.right
-- Mathlib.RingTheory.UniqueFactorizationDomain.Finite
/-- If `y` is a nonzero element of a unique factorization monoid with finitely
many units (e.g. `ℤ`, `Ideal (ring_of_integers K)`), it has finitely many divisors.  -/
UniqueFactorizationMonoid.fintypeSubtypeDvd : {M : Type u_2} →
  [inst : CommMonoidWithZero M] →
    [UniqueFactorizationMonoid M] → [Fintype Mˣ] → (y : M) → y ≠ 0 → Fintype { x // x ∣ y }
-- Std.Http.Protocol.H1
/-- Turns off keep-alive for the current connection; once disabled it remains
disabled for this machine instance.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.disableKeepAlive : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → Std.Http.Protocol.H1.Machine dir
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.le_minKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  (∀ (k' : α), t.minKey? = some k' → (cmp k k').isLE = true) ↔ ∀ k' ∈ t, (cmp k k').isLE = true
-- Mathlib.NumberTheory.Padics.RingHoms
/-- `limNthHom f_compat r` is the limit of a sequence `f` of compatible ring homs `R →+* ZMod (p^k)`.
This is itself a ring hom: see `PadicInt.lift`.
 -/
PadicInt.limNthHom : {R : Type u_1} →
  [inst : NonAssocSemiring R] →
    {p : ℕ} →
      {f : (k : ℕ) → R →+* ZMod (p ^ k)} →
        [hp_prime : Fact (Nat.Prime p)] →
          (∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1) → R → ℤ_[p]
-- Mathlib.Topology.EMetricSpace.Defs
/-- Auxiliary function to replace the uniformity on a pseudoemetric space with
a uniformity which is equal to the original one, but maybe not defeq.
This is useful if one wants to construct a pseudoemetric space with a
specified uniformity. See Note [forgetful inheritance] explaining why having definitionally
the right uniformity is often important.
See note [reducible non-instances].
 -/
PseudoEMetricSpace.replaceUniformity : {α : Type u_2} → [U : UniformSpace α] → (m : PseudoEMetricSpace α) → uniformity α = uniformity α → PseudoEMetricSpace α
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.Heap.brecOn.eq : ∀ {α : Type u} {motive : Batteries.BinomialHeap.Imp.Heap α → Sort u_1} (t : Batteries.BinomialHeap.Imp.Heap α)
  (F_1 : (t : Batteries.BinomialHeap.Imp.Heap α) → Batteries.BinomialHeap.Imp.Heap.below t → motive t),
  Batteries.BinomialHeap.Imp.Heap.brecOn t F_1 = F_1 t (Batteries.BinomialHeap.Imp.Heap.brecOn.go t F_1).2
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.List.filter.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match true with
    | true => h_1 ()
    | false => h_2 ()) =
    h_1 ()
-- Mathlib.Data.Int.CardIntervalMod
/-- There are `⌈(b - v) / r⌉ - ⌈(a - v) / r⌉` numbers congruent to `v` mod `r` in `[a, b)`,
if `a ≤ b`.  -/
Int.Ico_filter_modEq_card : ∀ (a b : ℤ) {r : ℤ},
  0 < r → ∀ (v : ℤ), ↑{x ∈ Finset.Ico a b | x ≡ v [ZMOD r]}.card = max (⌈(↑b - ↑v) / ↑r⌉ - ⌈(↑a - ↑v) / ↑r⌉) 0
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
/-- Given natural transformations `F₁ ⟶ F` and `F₂ ⟶ F`, construct
a natural transformation `coprod F₁ F₂ ⟶ F`.  -/
CategoryTheory.FunctorToTypes.coprod.desc : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F F₁ F₂ : CategoryTheory.Functor C (Type w)} →
      (F₁ ⟶ F) → (F₂ ⟶ F) → (CategoryTheory.FunctorToTypes.coprod F₁ F₂ ⟶ F)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.uniqueHomFromTrivial : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      (A : CategoryTheory.AddGrp C) → Unique (CategoryTheory.AddGrp.trivial C ⟶ A)
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.fromNormalization_app_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f] {U : Y.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) {Z : CommRingCat}
  (h :
    (AlgebraicGeometry.Scheme.Hom.normalization f).presheaf.obj
        (Opposite.op ((TopologicalSpace.Opens.map (AlgebraicGeometry.Scheme.Hom.fromNormalization f).base).obj U)) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.Hom.app (AlgebraicGeometry.Scheme.Hom.fromNormalization f) U) h =
    CategoryTheory.CategoryStruct.comp
      (CommRingCat.ofHom
        (algebraMap ↑(Y.presheaf.1 (Opposite.op U))
          ↥(integralClosure ↑(Y.presheaf.obj (Opposite.op U))
              ↑(X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.base).obj U))))))
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.normalizationObjIso f hU).inv h)
-- Mathlib.LinearAlgebra.Dual.Lemmas
/-- Consider a reflexive module and a set `s` of linear forms. If for any `z ≠ 0` there exists
`f ∈ s` such that `f z ≠ 0`, then `s` spans the whole dual space.  -/
Submodule.span_eq_top_of_ne_zero : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [Module.IsReflexive R M] {s : Set (M →ₗ[R] R)} [Module.Projective R ((M →ₗ[R] R) ⧸ Submodule.span R s)],
  (∀ (z : M), z ≠ 0 → ∃ f ∈ s, f z ≠ 0) → Submodule.span R s = ⊤
-- Init.Data.Int.Linear
Int.Internal.Linear.instReflBEqPoly : ReflBEq Int.Internal.Linear.Poly
-- Init.Data.Array.MapIdx
_private.Init.Data.Array.MapIdx.0.List.mapFinIdx.go.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (as : List α)
  (motive : (x : List α) → (x_1 : Array β) → x.length + x_1.size = as.length → Sort u_3) (acc : Array β)
  (h : [].length + acc.size = as.length)
  (h_1 : (acc : Array β) → (h : [].length + acc.size = as.length) → motive [] acc h)
  (h_2 :
    (a : α) →
      (as_1 : List α) → (acc : Array β) → (h : (a :: as_1).length + acc.size = as.length) → motive (a :: as_1) acc h),
  (match [], acc, h with
    | [], acc, h => h_1 acc h
    | a :: as_1, acc, h => h_2 a as_1 acc h) =
    h_1 acc h
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.mem_basicOpen : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (f : A) (x : ↥(AlgebraicGeometry.Proj 𝒜)),
  x ∈ AlgebraicGeometry.Proj.basicOpen 𝒜 f ↔ f ∉ x.asHomogeneousIdeal
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetSemiring.pairwiseDisjoint_disjointOfUnion_of_mem : ∀ {α : Type u_1} {C : Set (Set α)} {j : Set α} {J : Finset (Set α)} (hC : MeasureTheory.IsSetSemiring C) (hJ : ↑J ⊆ C),
  j ∈ J → (↑(hC.disjointOfUnion hJ j)).PairwiseDisjoint id
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_fiberwise_of_maps_to : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : AddCommMonoid M] {s : Finset ι} {t : Finset κ}
  [inst_1 : DecidableEq κ] {g : ι → κ},
  (∀ i ∈ s, g i ∈ t) → ∀ (f : ι → M), ∑ j ∈ t, ∑ i ∈ s with g i = j, f i = ∑ i ∈ s, f i
-- Mathlib.Topology.MetricSpace.Algebra
LipschitzAdd.mk : ∀ {β : Type u_2} [inst : PseudoMetricSpace β] [inst_1 : AddMonoid β],
  (∃ C, LipschitzWith C fun p => p.1 + p.2) → LipschitzAdd β
-- Lean.Meta.Tactic.Grind.Main
_private.Lean.Meta.Tactic.Grind.Main.0.Lean.Meta.Grind.splitDiagInfoToMessageData : Array Lean.Meta.Grind.SplitDiagInfo → Lean.MetaM Lean.MessageData
-- Mathlib.Topology.MetricSpace.PiNat
Metric.PiNatEmbed.isHomeomorph_toPiNat : ∀ {ι : Type u_2} {X : Type u_3} {Y : ι → Type u_4} {f : (i : ι) → X → Y i} [inst : Encodable ι]
  [inst_1 : (i : ι) → MetricSpace (Y i)] [inst_2 : TopologicalSpace X] [CompactSpace X],
  (∀ (i : ι), Continuous (f i)) → (Pairwise fun x y => ∃ i, f i x ≠ f i y) → IsHomeomorph Metric.PiNatEmbed.toPiNat
-- Mathlib.Topology.Ultrafilter
continuousAt_iff_ultrafilter : ∀ {X : Type u} {Y : Type v} {x : X} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  ContinuousAt f x ↔ ∀ (g : Ultrafilter X), ↑g ≤ nhds x → Filter.Tendsto f (↑g) (nhds (f x))
-- Mathlib.Topology.Spectral.Hom
/-- [Stacks Tag 005B](https://stacks.math.columbia.edu/tag/005B) -/
IsSpectralMap.comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] {f : β → γ} {g : α → β}, IsSpectralMap f → IsSpectralMap g → IsSpectralMap (f ∘ g)
-- Mathlib.FieldTheory.Minpoly.Basic
minpoly.algHom_eq : ∀ {A : Type u_1} {B : Type u_2} {B' : Type u_3} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : Ring B']
  [inst_3 : Algebra A B] [inst_4 : Algebra A B'] (f : B →ₐ[A] B'),
  Function.Injective ⇑f → ∀ (x : B), minpoly A (f x) = minpoly A x
-- Init.ShareCommon
ShareCommonT.withShareCommon : {m : Type u_1 → Type u_2} → {α : Type u_1} → {σ : ShareCommon.StateFactory} → [Monad m] → α → ShareCommonT σ m α
-- Mathlib.GroupTheory.Congruence.Defs
AddConGen.Rel.add : ∀ {M : Type u_1} [inst : Add M] {r : M → M → Prop} {w x y z : M},
  AddConGen.Rel r w x → AddConGen.Rel r y z → AddConGen.Rel r (w + y) (x + z)
-- Init.Data.Vector.Lemmas
Vector.and_any_distrib_right : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {p : α → Bool} {q : Bool}, (xs.any p && q) = xs.any fun a => p a && q
-- Mathlib.Algebra.DirectSum.Ring
DirectSum.mulHom.eq_1 : ∀ {ι : Type u_1} [inst : DecidableEq ι] (A : ι → Type u_2) [inst_1 : Add ι] [inst_2 : (i : ι) → AddCommMonoid (A i)]
  [inst_3 : DirectSum.GNonUnitalNonAssocSemiring A],
  DirectSum.mulHom A =
    DirectSum.toAddMonoid fun x =>
      (DirectSum.toAddMonoid fun x_1 =>
          ((AddMonoidHom.compHom (DirectSum.of A (x + x_1))).comp (DirectSum.gMulHom A)).flip).flip
-- Mathlib.CategoryTheory.Sites.CartesianMonoidal
/-- **Alias** of `CategoryTheory.Sheaf.cartesianMonoidalCategorySnd_hom`. -/
CategoryTheory.Sheaf.cartesianMonoidalCategorySnd_val : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  (J : CategoryTheory.GrothendieckTopology C) [inst_2 : CategoryTheory.CartesianMonoidalCategory A]
  (X Y : CategoryTheory.Sheaf J A),
  (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y).hom =
    CategoryTheory.SemiCartesianMonoidalCategory.snd X.obj Y.obj
-- Mathlib.Analysis.Complex.Order
Complex.not_lt_zero_iff : ∀ {z : ℂ}, ¬z < 0 ↔ 0 ≤ z.re ∨ z.im ≠ 0
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
div_lt_comm : ∀ {α : Type u} [inst : CommGroup α] [inst_1 : LT α] [MulLeftStrictMono α] {a b c : α}, a / b < c ↔ a / c < b
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.instInhabitedCfg : Inhabited Turing.ToPartrec.Cfg
-- Mathlib.Probability.Independence.Integration
/-- **Alias** of `ProbabilityTheory.IndepFun.integrable_left_of_integrable_op`.

---

If `X` and `Y` are two independent random variables, `B X Y` is integrable, `Y` is not
almost-surely `0` and `c * ‖x‖ₑ * ‖y‖ₑ ≤ ‖B x y‖ₑ`, then `X` is integrable.

This is useful for the case where `B` is scalar multiplication, as it will allow to drop
integrability hypotheses.  -/
ProbabilityTheory.IndepFun.integrable_left_of_integrable_mul : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {E : Type u_5} {F : Type u_6} {G : Type u_7}
  [inst : TopologicalSpace E] [inst_1 : ContinuousENorm E] [inst_2 : MeasurableSpace E] [OpensMeasurableSpace E]
  [inst_4 : NormedAddGroup F] [inst_5 : MeasurableSpace F] [OpensMeasurableSpace F] [inst_7 : TopologicalSpace G]
  [inst_8 : ContinuousENorm G] {X : Ω → E} {Y : Ω → F},
  ProbabilityTheory.IndepFun X Y μ →
    ∀ (B : E → F → G) (c : NNReal),
      c ≠ 0 →
        (∀ (x : E) (y : F), ↑c * ‖x‖ₑ * ‖y‖ₑ ≤ ‖B x y‖ₑ) →
          MeasureTheory.Integrable (fun ω => B (X ω) (Y ω)) μ →
            MeasureTheory.AEStronglyMeasurable X μ →
              MeasureTheory.AEStronglyMeasurable Y μ → ¬Y =ᵐ[μ] 0 → MeasureTheory.Integrable X μ
-- Lean.Meta.Sym.Pattern
/-- Creates a `Pattern` from the type of a theorem.

The pattern is constructed by stripping leading universal quantifiers from the theorem's type.
Each quantified variable becomes a pattern variable, with its type recorded in `varTypes` and
whether it is a type class instance recorded in `isInstance`. The remaining type after
stripping quantifiers becomes the `pattern` expression.

Universe level parameters are replaced with fresh unification variables (prefixed with `_uvar`).

If `num?` is `some n`, at most `n` leading quantifiers are stripped.
If `num?` is `none`, all leading quantifiers are stripped.
 -/
Lean.Meta.Sym.mkPatternFromDecl : Lean.Name → optParam (Option ℕ) none → Lean.MetaM Lean.Meta.Sym.Pattern
-- Batteries.Data.List.Perm
List.Perm.subperm_left : ∀ {α : Type u_1} {l l₁ l₂ : List α}, l₁.Perm l₂ → (l.Subperm l₁ ↔ l.Subperm l₂)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get?_modify_self : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α], (↑m).WF → ∀ {k : α} {f : β k → β k}, (m.modify k f).get? k = Option.map f (m.get? k)
-- Mathlib.RingTheory.MvPowerSeries.Expand
MvPowerSeries.expand_monomial : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] (p : ℕ) (hp : p ≠ 0) (d : σ →₀ ℕ) (r : R),
  (MvPowerSeries.expand p hp) ((MvPowerSeries.monomial d) r) = (MvPowerSeries.monomial (p • d)) r
-- Mathlib.Data.ENNReal.Basic
/-- `toNNReal x` returns `x` if it is real, otherwise 0.  -/
ENNReal.toNNReal : ENNReal → NNReal
-- Init.Control.Lawful.Instances
ExceptT.run_lift : ∀ {m : Type u → Type v} {α ε : Type u} [inst : Monad m] (x : m α), (ExceptT.lift x).run = Except.ok <$> x
-- Init.Data.List.Sublist
List.infix_cons : ∀ {α : Type u_1} {l₁ l₂ : List α} {a : α}, l₁ <:+: l₂ → l₁ <:+: a :: l₂
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- Occurrence sets are closed.  -/
SymbolicDynamics.FullShift.isClosed_occursInAt : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : Inhabited A] {G : Type u_2} [inst_2 : AddMonoid G]
  [IsLeftCancelAdd G] [T1Space A] (p : SymbolicDynamics.FullShift.Pattern A G) (g : G), IsClosed {x | p.occursInAt x g}
-- Mathlib.CategoryTheory.Category.Pairwise
CategoryTheory.Pairwise.single : {ι : Type v} → ι → CategoryTheory.Pairwise ι
-- Mathlib.Data.Finsupp.Notation
/-- Implementation detail for `fun₀`, used by both `Finsupp` and `DFinsupp`  -/
Finsupp.Internal.stxUpdate₀ : Lean.ParserDescr
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.eq_1 : ∀ (M : Type u_1) (N : Type u_2) [inst : MulOneClass M] [inst_1 : MulOneClass N],
  Monoid.Coprod M N = (Monoid.coprodCon M N).Quotient
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.cast_subConst_mul_card : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] {𝕜 : Type u_3} [inst_2 : Semifield 𝕜] [CharZero 𝕜]
  (A B : Finset G), ↑(A.subConst B) * ↑A.card = ↑(A - B).card
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.cyclesIsoSc'.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j k : ι) (hi : c.prev j = i) (hk : c.next j = k)
  [inst_2 : K.HasHomology j] [inst_3 : (K.sc' i j k).HasHomology],
  K.cyclesIsoSc' i j k hi hk = CategoryTheory.ShortComplex.cyclesMapIso (K.isoSc' i j k hi hk)
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
Complex.log_inv : ∀ (x : ℂ), x.arg ≠ Real.pi → Complex.log x⁻¹ = -Complex.log x
-- Mathlib.Topology.Order.Hom.Esakia
EsakiaHom.coe_id_pseudoEpimorphism : ∀ (α : Type u_2) [inst : TopologicalSpace α] [inst_1 : Preorder α],
  { toOrderHom := ↑(EsakiaHom.id α), exists_map_eq_of_map_le' := ⋯ } = PseudoEpimorphism.id α
-- Mathlib.Topology.Algebra.Polynomial
Polynomial.tendsto_abv_aeval_atTop : ∀ {R : Type u_1} {A : Type u_2} {k : Type u_3} {α : Type u_4} [inst : CommSemiring R] [inst_1 : Ring A]
  [inst_2 : Algebra R A] [inst_3 : Field k] [inst_4 : LinearOrder k] [IsStrictOrderedRing k] (abv : A → k)
  [IsAbsoluteValue abv] (p : Polynomial R),
  0 < p.degree →
    (algebraMap R A) p.leadingCoeff ≠ 0 →
      ∀ {l : Filter α} {z : α → A},
        Filter.Tendsto (abv ∘ z) l Filter.atTop →
          Filter.Tendsto (fun x => abv ((Polynomial.aeval (z x)) p)) l Filter.atTop
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.GrothendieckTopology.Point.jointly_surjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (self : J.Point)
  {X : C},
  ∀ R ∈ J X,
    ∀ (x : self.fiber.obj X),
      ∃ Y f, ∃ (_ : R.arrows f), ∃ y, (CategoryTheory.ConcreteCategory.hom (self.fiber.map f)) y = x