mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.FullyFaithful.grpObj.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {F : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] (hF : F.FullyFaithful) (X : C)
  [inst_5 : CategoryTheory.GrpObj (F.obj X)],
  hF.grpObj X = { toMonObj := hF.monObj X, inv := hF.preimage CategoryTheory.GrpObj.inv, left_inv := ⋯, right_inv := ⋯ }
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.FunDecl.binderName : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.FunDecl pu → Lean.Name
-- Init.Grind.Ring.Field
Lean.Grind.Field.div_add : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] {x y z : α}, y ≠ 0 → x / y + z = (x + y * z) / y
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
AddLECancellable.add_tsub_tsub_cancel : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α}, AddLECancellable (a - c) → c ≤ a → a + b - (a - c) = b + c
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.toListModel_alterₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  {m : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α} {f : Option (β a) → Option (β a)},
      (Std.DHashMap.Internal.toListModel (↑(m.alterₘ a f)).buckets).Perm
        (Std.Internal.List.alterKey a f (Std.DHashMap.Internal.toListModel (↑m).buckets))
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.image2_div : ∀ {α : Type u_2} [inst : Div α] {s t : Set α}, Set.image2 (fun x1 x2 => x1 / x2) s t = s / t
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
/-- Decomposition of an affine map in the special case when the point space and vector space
are the same.  -/
AffineMap.decomp' : ∀ {k : Type u_1} {V1 : Type u_2} {V2 : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
  [inst_3 : AddCommGroup V2] [inst_4 : Module k V2] (f : V1 →ᵃ[k] V2), ⇑f.linear = ⇑f - fun x => f 0
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.instDecidableEq : {R : Type u_2} →
  {M : Type u_3} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → [DecidableEq M] → DecidableEq (PolynomialModule R M)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- Given a point `p₁` in an affine subspace `s`, and a point `p₂`, a point `p` is in the span of
`s` with `p₂` added if and only if it is a multiple of `p₂ -ᵥ p₁` added to a point in `s`.  -/
AffineSubspace.mem_affineSpan_insert_iff : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : AffineSubspace k P} {p₁ : P},
  p₁ ∈ s → ∀ (p₂ p : P), p ∈ affineSpan k (insert p₂ ↑s) ↔ ∃ r, ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁) +ᵥ p0
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.subst.injEq : ∀ (x : Int.Internal.Linear.Var) (c₁ : Lean.Meta.Grind.Arith.Cutsat.EqCnstr) (c₂ : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr)
  (x_1 : Int.Internal.Linear.Var) (c₁_1 : Lean.Meta.Grind.Arith.Cutsat.EqCnstr)
  (c₂_1 : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr),
  (Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.subst x c₁ c₂ =
      Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.subst x_1 c₁_1 c₂_1) =
    (x = x_1 ∧ c₁ = c₁_1 ∧ c₂ = c₂_1)
-- Mathlib.Analysis.Complex.OpenMapping
/-- Corollary to the open mapping theorem: A holomorphic function whose real part is constant is itself
constant.
 -/
AnalyticOnNhd.eq_const_of_re_eq_const : ∀ {f : ℂ → ℂ} {U : Set ℂ} {c₀ : ℝ},
  AnalyticOnNhd ℂ f U → (∀ x ∈ U, (f x).re = c₀) → IsOpen U → IsConnected U → ∃ c, ∀ x ∈ U, f x = c
-- Mathlib.Analysis.Subadditive
Subadditive.apply_mul_add_le : ∀ {u : ℕ → ℝ}, Subadditive u → ∀ (k n r : ℕ), u (k * n + r) ≤ ↑k * u n + u r
-- Mathlib.CategoryTheory.Galois.Topology
CategoryTheory.PreGaloisCategory.autEmbedding_injective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat),
  Function.Injective ⇑(CategoryTheory.PreGaloisCategory.autEmbedding F)
-- Mathlib.Algebra.Group.Defs
AddZeroClass.ext_iff : ∀ {M : Type u} {m₁ m₂ : AddZeroClass M}, m₁ = m₂ ↔ Add.add = Add.add
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four
CategoryTheory.Abelian.epi_of_epi_of_epi_of_epi : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {R₁ R₂ : CategoryTheory.ComposableArrows C 2} (φ : R₁ ⟶ R₂),
  R₂.Exact →
    CategoryTheory.Epi
        (R₁.map' 1 2 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_6
          CategoryTheory.Abelian.mono_of_epi_of_epi_mono'._proof_1) →
      CategoryTheory.Epi
          (CategoryTheory.ComposableArrows.app' φ 0 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_2) →
        CategoryTheory.Epi
            (CategoryTheory.ComposableArrows.app' φ 2 CategoryTheory.Abelian.mono_of_epi_of_epi_mono'._proof_1) →
          CategoryTheory.Epi
            (CategoryTheory.ComposableArrows.app' φ 1 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_6)
-- Mathlib.CategoryTheory.EssentiallySmall
CategoryTheory.essentiallySmall_of_fully_faithful : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (F : CategoryTheory.Functor C D) [F.Full] [F.Faithful] [CategoryTheory.EssentiallySmall.{w, v', u'} D],
  CategoryTheory.EssentiallySmall.{w, v, u} C
-- Mathlib.Topology.Connected.Basic
IsConnected.iUnion_of_reflTransGen : ∀ {α : Type u} [inst : TopologicalSpace α] {ι : Type u_3} [Nonempty ι] {s : ι → Set α},
  (∀ (i : ι), IsConnected (s i)) →
    (∀ (i j : ι), Relation.ReflTransGen (fun i j => (s i ∩ s j).Nonempty) i j) → IsConnected (⋃ n, s n)
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.ext_to_X : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (i j : ι) (hij : c.Rel i j) {A : C}
  {f g : A ⟶ HomologicalComplex.homotopyCofiber.X φ i},
  CategoryTheory.CategoryStruct.comp f (HomologicalComplex.homotopyCofiber.fstX φ i j hij) =
      CategoryTheory.CategoryStruct.comp g (HomologicalComplex.homotopyCofiber.fstX φ i j hij) →
    CategoryTheory.CategoryStruct.comp f (HomologicalComplex.homotopyCofiber.sndX φ i) =
        CategoryTheory.CategoryStruct.comp g (HomologicalComplex.homotopyCofiber.sndX φ i) →
      f = g
-- Std.Data.HashSet.Raw
Std.HashSet.Raw.WF.insertMany : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {ρ : Type v} [inst_2 : ForIn Id ρ α] {m : Std.HashSet.Raw α}
  {l : ρ}, m.WF → (m.insertMany l).WF
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
/-- The pushforward of `traj κ a` along the the point at time `a + 1` is the kernel `κ a`.  -/
ProbabilityTheory.Kernel.map_traj_succ_self : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))}
  [inst_1 : ∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] {a : ℕ},
  ((ProbabilityTheory.Kernel.traj κ a).map fun x => x (a + 1)) = κ a
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.tryCatch_OptionT_lift : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {ε α : Type u} {x : OptionT m α} {h : ε → OptionT m α}
  [inst : Std.Do.WP m ps] [inst_1 : MonadExceptOf ε m]
  (Q : Std.Do.PostCond α (Std.Do.PostShape.except PUnit.{u + 1} ps)),
  ⦃(Std.Do.wp (MonadExceptOf.tryCatch x h)).apply (fun o => Option.casesOn o (Q.2.1 PUnit.unit) Q.1, Q.2.2)⦄
    MonadExceptOf.tryCatch x h ⦃Q⦄
-- Mathlib.Data.List.Perm.Basic
List.count_eq_count_filter_add : ∀ {α : Type u_1} [inst : DecidableEq α] (P : α → Prop) [inst_1 : DecidablePred P] (l : List α) (a : α),
  List.count a l =
    List.count a (List.filter (fun b => decide (P b)) l) + List.count a (List.filter (fun x => decide ¬P x) l)
-- Mathlib.Algebra.Ring.GeomSum
mul_geom_sum₂_Ico : ∀ {R : Type u_1} [inst : CommRing R] (x y : R) {m n : ℕ},
  m ≤ n → (x - y) * ∑ i ∈ Finset.Ico m n, x ^ i * y ^ (n - 1 - i) = x ^ n - x ^ m * y ^ (n - m)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.gradedHomologyFunctor_obj : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} (c : ComplexShape ι) [inst_2 : CategoryTheory.CategoryWithHomology C] (K : HomologicalComplex C c)
  (i : ι), (HomologicalComplex.gradedHomologyFunctor C c).obj K i = K.homology i
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.two_zsmul_coe_div_two : ∀ (θ : ℝ), 2 • ↑(θ / 2) = ↑θ
-- Aesop.Tree.Data
Aesop.GoalId.one : Aesop.GoalId
-- Mathlib.Topology.Separation.SeparatedNhds
SeparatedNhds.preimage : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s t : Set Y},
  SeparatedNhds s t → Continuous f → SeparatedNhds (f ⁻¹' s) (f ⁻¹' t)
-- Aesop.BaseM
Aesop.BaseM.State.mk.sizeOf_spec : ∀ (rulePatternCache : Aesop.RulePatternCache) (stats : Aesop.Stats),
  sizeOf { rulePatternCache := rulePatternCache, stats := stats } = 1 + sizeOf rulePatternCache + sizeOf stats
-- Mathlib.Topology.Homeomorph.Defs
/-- `HomeomorphClass F A B` states that `F` is a type of homeomorphisms.  -/
HomeomorphClass : (F : Type u_5) →
  (A : outParam (Type u_6)) →
    (B : outParam (Type u_7)) → [TopologicalSpace A] → [TopologicalSpace B] → [h : EquivLike F A B] → Prop
-- Init.Grind.Lemmas
Lean.Grind.Nat.and_congr : ∀ {a b k₁ k₂ k : ℕ}, a = k₁ → b = k₂ → (k == k₁ &&& k₂) = true → a &&& b = k
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.instTopologicalSpace : (E : Type u_5) →
  (F : Type u_6) →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        [inst_2 : NormedAddCommGroup F] → [inst_3 : NormedSpace ℝ F] → TopologicalSpace (SchwartzMap E F)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
CategoryTheory.NatTrans.Coequifibered.whiskerLeft : ∀ {J : Type u_1} {K : Type u_2} {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} C] [inst_2 : CategoryTheory.Category.{v_3, u_2} K]
  {F G : CategoryTheory.Functor J C} {α : F ⟶ G},
  CategoryTheory.NatTrans.Coequifibered α →
    ∀ (H : CategoryTheory.Functor K J), CategoryTheory.NatTrans.Coequifibered (H.whiskerLeft α)
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.ediam_image : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) (s : Set P),
  Metric.ediam (⇑e '' s) = Metric.ediam s
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.instMembership : {α : Type u_1} → Membership α (FreeMonoid α)
-- Mathlib.Data.Finsupp.Order
Finsupp.disjoint_iff : ∀ {ι : Type u_1} {α : Type u_3} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [inst_2 : IsBotZeroClass α]
  {f g : ι →₀ α}, Disjoint f g ↔ Disjoint f.support g.support
-- Mathlib.Topology.Order.Lattice
continuous_inf : ∀ {L : Type u_1} [inst : TopologicalSpace L] [inst_1 : Min L] [ContinuousInf L], Continuous fun p => p.1 ⊓ p.2
-- Mathlib.CategoryTheory.Limits.IsConnected
/-- The domain of a final functor is connected if and only if its codomain is connected.  -/
CategoryTheory.Functor.isConnected_iff_of_final : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.Final], CategoryTheory.IsConnected C ↔ CategoryTheory.IsConnected D
-- Mathlib.GroupTheory.Commutator.Basic
AddSubgroup.addCommutator_le_right : ∀ {G : Type u_1} [inst : AddGroup G] (H₁ H₂ : AddSubgroup G) [h : H₂.Normal], ⁅H₁, H₂⁆ ≤ H₂
-- Mathlib.CategoryTheory.Filtered.Final
/-- In this situation, `C` is also cofiltered, see
`IsCofilteredOrEmpty.of_exists_of_isCofiltered_of_fullyFaithful`.  -/
CategoryTheory.Functor.initial_of_exists_of_isCofiltered_of_fullyFaithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.IsCofilteredOrEmpty D] [F.Full] [F.Faithful],
  (∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)) → F.Initial
-- Mathlib.Order.Atoms
IsSimpleOrder.bot_ne_top : ∀ {α : Type u_2} [inst : LE α] [inst_1 : BoundedOrder α] [IsSimpleOrder α], ⊥ ≠ ⊤
-- Mathlib.CategoryTheory.Limits.ExactFunctor
CategoryTheory.ExactFunctor.whiskeringLeft_obj_obj_obj : ∀ (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 : C ⥤ₑ D) (X : D ⥤ₑ E),
  (((CategoryTheory.ExactFunctor.whiskeringLeft C D E).obj F).obj X).obj = F.obj.comp X.obj
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
SimpleGraph.TripartiteFromTriangles.Graph.in₀₁_iff' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {a : α} {b : β},
  (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₀ a) (Sum3.in₁ b) ↔ ∃ x ∈ t, x.1 = a ∧ x.2.1 = b
-- Mathlib.LinearAlgebra.Prod
/-- **Goursat's lemma** for module isomorphisms.

Let `G ≤ H × I` be a submodule of a product of modules. Assume that the natural maps from `G` to
both factors are bijective. Then `G` is the graph of some module isomorphism `f : H ≃ I`.  -/
Submodule.exists_equiv_eq_graph : ∀ {S : Type u_4} {H : Type u_6} {I : Type u_7} [inst : Semiring S] [inst_1 : AddCommMonoid H] [inst_2 : Module S H]
  [inst_3 : AddCommMonoid I] [inst_4 : Module S I] {G : Submodule S (H × I)},
  Function.Bijective (Prod.fst ∘ ⇑G.subtype) → Function.Bijective (Prod.snd ∘ ⇑G.subtype) → ∃ e, G = (↑e).graph
-- Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
/-- (Implementation) Given the appropriate coproduct and coequalizer cocones,
build the cocone for `F` which is colimiting if the given cocones are also.
 -/
CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildColimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.SmallCategory J] →
        {F : CategoryTheory.Functor J C} →
          {c₁ : CategoryTheory.Limits.Cofan fun f => F.obj f.fst.1} →
            {c₂ : CategoryTheory.Limits.Cofan F.obj} →
              (s t : c₁.pt ⟶ c₂.pt) →
                (∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
                    CategoryTheory.CategoryStruct.comp (c₁.ι.app { as := f }) s =
                      CategoryTheory.CategoryStruct.comp (F.map f.snd) (c₂.ι.app { as := f.fst.2 })) →
                  (∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
                      CategoryTheory.CategoryStruct.comp (c₁.ι.app { as := f }) t = c₂.ι.app { as := f.fst.1 }) →
                    CategoryTheory.Limits.Cofork s t → CategoryTheory.Limits.Cocone F
-- Mathlib.Topology.MetricSpace.BundledFun
PseudoMetric.IsUltra.isTrans_ball : ∀ {X : Type u_1} {R : Type u_2} [inst : Add R] [inst_1 : Zero R] [inst_2 : LinearOrder R] (d : PseudoMetric X R)
  [d.IsUltra] {ε : R}, SetRel.IsTrans {xy | d xy.1 xy.2 < ε}
-- Mathlib.Order.Category.BddLat
BddLat.comp_apply : ∀ {X Y Z : Lat} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↑X),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)
-- Mathlib.Data.Nat.Hyperoperation
hyperoperation.eq_def : ∀ (x x_1 x_2 : ℕ),
  hyperoperation x x_1 x_2 =
    match x, x_1, x_2 with
    | 0, x, k => k + 1
    | 1, m, 0 => m
    | 2, x, 0 => 0
    | n.succ.succ.succ, x, 0 => 1
    | n.succ, m, k.succ => hyperoperation n m (hyperoperation (n + 1) m k)
-- Lean.Data.SMap
Lean.List.toSMap : {α : Type u_1} → {β : Type u_2} → [inst : BEq α] → [inst_1 : Hashable α] → List (α × β) → Lean.SMap α β
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidWithZeroHom.mk.inj : ∀ {α : Type u_6} {β : Type u_7} {inst : Preorder α} {inst_1 : Preorder β} {inst_2 : MulZeroOneClass α}
  {inst_3 : MulZeroOneClass β} {toMonoidWithZeroHom : α →*₀ β} {monotone' : Monotone (↑toMonoidWithZeroHom).toFun}
  {toMonoidWithZeroHom_1 : α →*₀ β} {monotone'_1 : Monotone (↑toMonoidWithZeroHom_1).toFun},
  { toMonoidWithZeroHom := toMonoidWithZeroHom, monotone' := monotone' } =
      { toMonoidWithZeroHom := toMonoidWithZeroHom_1, monotone' := monotone'_1 } →
    toMonoidWithZeroHom = toMonoidWithZeroHom_1
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.span.eq_1 : ∀ {ι' : Type u_2} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : DecidableEq E] {v' : ι' → E} (h : Orthonormal 𝕜 v') (s : Finset ι'),
  OrthonormalBasis.span h s =
    (OrthonormalBasis.mk ⋯ ⋯).map
      (LinearIsometryEquiv.ofEq (Submodule.span 𝕜 ↑(Finset.image v' s))
          (Submodule.span 𝕜 (Set.range (v' ∘ Subtype.val))) ⋯).symm
-- Mathlib.CategoryTheory.Filtered.Final
/-- The functor `CostructuredArrow.proj : CostructuredArrow Y T ⥤ C` is initial if `T : C ⥤ D` is
initial and `C` is cofiltered.  -/
CategoryTheory.CostructuredArrow.initial_proj_of_isCofiltered : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.IsCofilteredOrEmpty C] (T : CategoryTheory.Functor C D) [T.Initial] (Y : D),
  (CategoryTheory.CostructuredArrow.proj T Y).Initial
-- Mathlib.Analysis.Normed.Ring.Basic
/-- In a seminormed ring, the right-multiplication `AddMonoidHom` is bounded.  -/
mulRight_bound : ∀ {α : Type u_2} [inst : NonUnitalSeminormedRing α] (x y : α), ‖(AddMonoidHom.mulRight x) y‖ ≤ ‖x‖ * ‖y‖
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.isRightQuasiInverse_congr : ∀ {K : Type u_1} {V₂ : Type u_4} {V₃ : Type u_6} [inst : CommRing K] [inst_1 : AddCommGroup V₂] [inst_2 : Module K V₂]
  [inst_3 : AddCommGroup V₃] [inst_4 : Module K V₃] {u u' : V₃ →ₗ[K] V₂} {v v' : V₂ →ₗ[K] V₃},
  u' ≈ u → v' ≈ v → (u.IsRightQuasiInverse v ↔ u'.IsRightQuasiInverse v')
-- Mathlib.CategoryTheory.Limits.Preorder
/-- If the point of cone is a glb, the cone is a limit.  -/
Preorder.isLimitOfIsGLB : {C : Type u} →
  [inst : Preorder C] →
    {J : Type u'} →
      [inst_1 : CategoryTheory.Category.{v, u'} J] →
        (F : CategoryTheory.Functor J C) →
          (c : CategoryTheory.Limits.Cone F) → IsGLB (Set.range F.obj) c.pt → CategoryTheory.Limits.IsLimit c
-- Mathlib.RingTheory.Flat.Localization
IsLocalization.flat : ∀ {R : Type u_1} (S : Type u_2) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  (p : Submonoid R) [IsLocalization p S], Module.Flat R S
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
/-- The postcomposition of a derivation by a morphism of presheaves of modules.  -/
PresheafOfModules.Derivation.postcomp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} →
          {F : CategoryTheory.Functor C D} →
            {R : CategoryTheory.Functor Dᵒᵖ CommRingCat} →
              {M N : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} →
                {φ : S ⟶ F.op.comp R} → M.Derivation φ → (M ⟶ N) → N.Derivation φ
-- Lean.Elab.Syntax
_private.Lean.Elab.Syntax.0.Lean.Elab.Term.toParserDescr.processAlias : Lean.Syntax → Array Lean.Syntax → Lean.Elab.Term.ToParserDescrM (Lean.Term × ℕ)
-- Mathlib.Probability.Martingale.Basic
/-- The converse of this lemma is `MeasureTheory.submartingale_of_setIntegral_le`.  -/
MeasureTheory.Submartingale.setIntegral_le : ∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  {ℱ : MeasureTheory.Filtration ι m0} [CompleteSpace E] [inst_4 : PartialOrder E] [IsOrderedAddMonoid E]
  [IsOrderedModule ℝ E] [ClosedIciTopology E] [MeasureTheory.SigmaFiniteFiltration μ ℱ] {f : ι → Ω → E},
  MeasureTheory.Submartingale f ℱ μ →
    ∀ {i j : ι}, i ≤ j → ∀ {s : Set Ω}, MeasurableSet s → ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f j ω ∂μ
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.continuousOn_cos : ∀ {s : Set ℂ}, ContinuousOn Complex.cos s
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.tendsto_density_fst_atTop_ae_of_monotone : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] {κ : ProbabilityTheory.Kernel α (γ × β)}
  [ProbabilityTheory.IsFiniteKernel κ] (a : α) (seq : ℕ → Set β),
  Monotone seq →
    ⋃ i, seq i = Set.univ →
      (∀ (m : ℕ), MeasurableSet (seq m)) →
        ∀ᵐ (x : γ) ∂κ.fst a, Filter.Tendsto (fun m => κ.density κ.fst a x (seq m)) Filter.atTop (nhds 1)
-- Mathlib.Control.Basic
/-- Takes a value `β` and `List α` and accumulates pairs according to a monadic function `f`.
Accumulation occurs from the left (i.e., starting from the head of the list).  -/
List.mapAccumLM : {α : Type u} →
  {β' γ' : Type v} → {m' : Type v → Type w} → [Monad m'] → (β' → α → m' (β' × γ')) → β' → List α → m' (β' × List γ')
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.Const.entryAtIdx?.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → ℕ → Sort u_3) (x : ℕ)
  (h_1 : (x : ℕ) → motive Std.DTreeMap.Internal.Impl.leaf x)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l r : Std.DTreeMap.Internal.Impl α fun x => β) →
            (n : ℕ) → motive (Std.DTreeMap.Internal.Impl.inner size k v l r) n),
  (match Std.DTreeMap.Internal.Impl.leaf, x with
    | Std.DTreeMap.Internal.Impl.leaf, x => h_1 x
    | Std.DTreeMap.Internal.Impl.inner size k v l r, n => h_2 size k v l r n) =
    h_1 x
-- Mathlib.Probability.Independence.Basic
/-- **Alias** of the reverse direction of `ProbabilityTheory.iIndep_comap_mem_iff`. -/
ProbabilityTheory.iIndepSet.iIndep_comap_mem : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : ι → Set Ω},
  ProbabilityTheory.iIndepSet f μ → ProbabilityTheory.iIndep (fun i => MeasurableSpace.comap (fun x => x ∈ f i) ⊤) μ
-- Mathlib.Algebra.Group.Subsemigroup.Basic
AddSubsemigroup.gi.eq_1 : ∀ (M : Type u_1) [inst : Add M], AddSubsemigroup.gi M = GaloisConnection.toGaloisInsertion ⋯ ⋯
-- Lean.Environment
/-- "Forward declaration" for retrieving the number of builtin attributes.  -/
Lean.getNumBuiltinAttributes : IO ℕ
-- Lean.Compiler.IR.Basic
Lean.IR.IRType.tagged : Lean.IR.IRType
-- Mathlib.Data.Finset.Sigma
Set.biInter_finsetSigma : ∀ {ι : Type u_1} {α : ι → Type u_2} {β : Type u_3} (s : Finset ι) (t : (i : ι) → Finset (α i)) (f : Sigma α → Set β),
  ⋂ ij ∈ s.sigma t, f ij = ⋂ i ∈ s, ⋂ j ∈ t i, f ⟨i, j⟩
-- Mathlib.Topology.Connected.LocallyPathConnected
/-- A topological space is locally path connected if, at every point, path connected
neighborhoods form a neighborhood basis.  -/
LocallyPathConnectedSpace : (X : Type u_4) → [TopologicalSpace X] → Prop
-- Mathlib.Data.Stream.Init
Stream'.take_take : ∀ {α : Type u} {s : Stream' α} {m n : ℕ}, List.take m (Stream'.take n s) = Stream'.take (min n m) s
-- Batteries.Data.Fin.Lemmas
Fin.exists_eq_true_iff_exists_maximal_eq_true : ∀ {n : ℕ} (p : Fin n → Bool), (∃ i, p i = true) ↔ ∃ i, p i = true ∧ ∀ (j : Fin n), i < j → p j = false
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.NullMeasurableSet.diff : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasureTheory.NullMeasurableSet s μ → MeasureTheory.NullMeasurableSet t μ → MeasureTheory.NullMeasurableSet (s \ t) μ