mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Interval.Set.Basic
Set.Ici_injective : ∀ {α : Type u_1} [inst : PartialOrder α], Function.Injective Set.Ici
-- Batteries.Util.Cache
/-- The cached data.  -/
Batteries.Tactic.DeclCache.cache : {α : Type} → Batteries.Tactic.DeclCache α → Batteries.Tactic.Cache α
-- Mathlib.Data.DFinsupp.Defs
/-- `DFinsupp.mapRange.addMonoidHom` as an `AddEquiv`.  -/
DFinsupp.mapRange.addEquiv : {ι : Type u} →
  {β₁ : ι → Type v₁} →
    {β₂ : ι → Type v₂} →
      [inst : (i : ι) → AddZeroClass (β₁ i)] →
        [inst_1 : (i : ι) → AddZeroClass (β₂ i)] → ((i : ι) → β₁ i ≃+ β₂ i) → (Π₀ (i : ι), β₁ i) ≃+ Π₀ (i : ι), β₂ i
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.NatIso.naturality_2_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} {X Y : C} (α : F ≅ G) (f : X ⟶ Y) {Z : D} (h : F.obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (α.hom.app X)
      (CategoryTheory.CategoryStruct.comp (G.map f) (CategoryTheory.CategoryStruct.comp (α.inv.app Y) h)) =
    CategoryTheory.CategoryStruct.comp (F.map f) h
-- Mathlib.CategoryTheory.Sites.Subcanonical
CategoryTheory.GrothendieckTopology.subcanonical_of_full_of_faithful : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v', u_1} D]
  (F : CategoryTheory.Functor C D) (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) [F.Full] [F.Faithful] [F.IsContinuous J K] [K.Subcanonical],
  J.Subcanonical
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
/-- A dependent version of `Subalgebra.iSup_induction`.  -/
Algebra.iSup_induction' : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {ι : Sort u_1}
  (S : ι → Subalgebra R A) {motive : (x : A) → x ∈ ⨆ i, S i → Prop} {x : A} (mem : x ∈ ⨆ i, S i),
  (∀ (i : ι) (x : A) (hx : x ∈ S i), motive x ⋯) →
    (∀ (x y : A) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), motive x hx → motive y hy → motive (x + y) ⋯) →
      (∀ (x y : A) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), motive x hx → motive y hy → motive (x * y) ⋯) →
        (∀ (r : R), motive ((algebraMap R A) r) ⋯) → motive x mem
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isLittleO_zero_right_iff : ∀ {α : Type u_1} {F' : Type u_7} {E'' : Type u_9} [inst : SeminormedAddCommGroup F'] [inst_1 : NormedAddCommGroup E'']
  {f'' : α → E''} {l : Filter α}, (f'' =o[l] fun _x => 0) ↔ f'' =ᶠ[l] 0
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.singleton_vadd : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] {t : Finset β} (a : α), {a} +ᵥ t = a +ᵥ t
-- ProofWidgets.Component.Basic
ProofWidgets.InteractiveExprProps.mk.injEq : ∀ (expr expr_1 : Lean.Server.WithRpcRef ProofWidgets.ExprWithCtx),
  ({ expr := expr } = { expr := expr_1 }) = (expr = expr_1)
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.mapTriangleIdIso_inv_app_hom₁ : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  (X : CategoryTheory.Pretriangulated.Triangle C),
  ((CategoryTheory.Functor.mapTriangleIdIso C).inv.app X).hom₁ = CategoryTheory.CategoryStruct.id X.obj₁
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.coeff_domCongr : ∀ {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 : AddMonoid M] [inst_4 : AddMonoid N] (e : M ≃+ N) (f : AddMonoidAlgebra A M) (n : N),
  ((AddMonoidAlgebra.domCongr R A e) f).coeff n = f.coeff (e.symm n)
-- Mathlib.Algebra.Torsor.Defs
/-- Adding the result of subtracting from another point produces that
point.  -/
vsub_vadd : ∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] (p₁ p₂ : P), (p₁ -ᵥ p₂) +ᵥ p₂ = p₁
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.domCongr_support : ∀ {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 : AddMonoid M] [inst_4 : AddMonoid N] (e : M ≃+ N) (x : AddMonoidAlgebra A M),
  ((AddMonoidAlgebra.domCongr R A e) x).coeff.support = Finset.map (↑e).toEmbedding x.coeff.support
-- Mathlib.Algebra.Group.Basic
inv_pow : ∀ {α : Type u_1} [inst : DivisionMonoid α] (a : α) (n : ℕ), a⁻¹ ^ n = (a ^ n)⁻¹
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.mapAddMonoidHom_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {Z : Type u_6} [inst_1 : AddZeroClass Y]
  [inst_2 : AddZeroClass Z] (f : Y →+ Z) (g : LocallyConstant X Y),
  (LocallyConstant.mapAddMonoidHom f) g = LocallyConstant.map (⇑f) g
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
/-- A characterization of weak convergence in terms of integrals of bounded continuous
real-valued functions.  -/
MeasureTheory.FiniteMeasure.tendsto_iff_forall_integral_tendsto : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
  {γ : Type u_2} {F : Filter γ} {μs : γ → MeasureTheory.FiniteMeasure Ω} {μ : MeasureTheory.FiniteMeasure Ω},
  Filter.Tendsto μs F (nhds μ) ↔
    ∀ (f : BoundedContinuousFunction Ω ℝ),
      Filter.Tendsto (fun i => ∫ (x : Ω), f x ∂↑(μs i)) F (nhds (∫ (x : Ω), f x ∂↑μ))
-- Mathlib.Algebra.Order.Ring.Nat
Nat.instLinearOrderedCommMonoidWithZero : LinearOrderedCommMonoidWithZero ℕ
-- Lean.Server.Rpc.Basic
Lean.Server.ReferencedObject.mk : Dynamic → USize → ℕ → Lean.Server.ReferencedObject
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- The oriented angle between two vectors is `π` if and only if the angle with the vectors
swapped is `π`.  -/
Orientation.oangle_eq_pi_iff_oangle_rev_eq_pi : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑Real.pi ↔ o.oangle y x = ↑Real.pi
-- Mathlib.Data.PNat.Basic
/-- If `n : ℕ+` is different from `1`, then it is the successor of some `k : ℕ+`.  -/
PNat.exists_eq_succ_of_ne_one : ∀ {n : ℕ+}, n ≠ 1 → ∃ k, n = k + 1
-- Lean.Language.Lean.Types
/-- State after successfully parsing the module header.  -/
Lean.Language.Lean.HeaderParsedState : Type
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.ofList_singleton : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {k : α} {v : β k},
  Std.ExtDTreeMap.ofList [⟨k, v⟩] cmp = ∅.insert k v
-- Mathlib.Algebra.Algebra.Tower
IsScalarTower.algebraMap_apply : ∀ (R : Type u) (S : Type v) (A : Type w) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra S A] [inst_5 : Algebra R A] [IsScalarTower R S A] (x : R),
  (algebraMap R A) x = (algebraMap S A) ((algebraMap R S) x)
-- Mathlib.CategoryTheory.FiberedCategory.Grothendieck
CategoryTheory.Pseudofunctor.CoGrothendieck.ι_map_fiber : ∀ {𝒮 : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} 𝒮]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat) (S : 𝒮)
  {a b : ↑(F.obj { as := Opposite.op S })} (φ : a ⟶ b),
  ((CategoryTheory.Pseudofunctor.CoGrothendieck.ι F S).map φ).fiber =
    CategoryTheory.CategoryStruct.comp φ ((F.mapId { as := Opposite.op S }).inv.toNatTrans.app b)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.isEmpty_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp}, t.toArray.isEmpty = t.isEmpty
-- Mathlib.Algebra.CharP.Lemmas
sub_pow_char : ∀ {R : Type u_1} [inst : CommRing R] (x y : R) {p : ℕ} [hp : Fact (Nat.Prime p)] [CharP R p],
  (x - y) ^ p = x ^ p - y ^ p
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rio_succ_eq_push : ∀ {n : ℕ}, (*...n + 1).toArray = (*...n).toArray.push n
-- Batteries.Data.List.Basic
/-- Auxiliary for `dropSliceTR`: `dropSliceTR.go l m xs n acc = acc.toList ++ dropSlice n m xs`
unless `n ≥ length xs`, in which case it is `l`.  -/
List.dropSliceTR.go : {α : Type u_1} → List α → ℕ → List α → ℕ → Array α → List α
-- Std.Data.HashMap.Lemmas
Std.HashMap.mem_diff_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, k ∈ m₁ \ m₂ ↔ k ∈ m₁ ∧ k ∉ m₂
-- Mathlib.Data.Sum.Interval
/-- Lifts maps `α₁ → β₁ → Finset γ₁` and `α₂ → β₂ → Finset γ₂` to a map
`α₁ ⊕ α₂ → β₁ ⊕ β₂ → Finset (γ₁ ⊕ γ₂)`. Could be generalized to `Alternative` functors if we can
make sure to keep computability and universe polymorphism.  -/
Finset.sumLift₂ : {α₁ : Type u_1} →
  {α₂ : Type u_2} →
    {β₁ : Type u_3} →
      {β₂ : Type u_4} →
        {γ₁ : Type u_5} →
          {γ₂ : Type u_6} → (α₁ → β₁ → Finset γ₁) → (α₂ → β₂ → Finset γ₂) → α₁ ⊕ α₂ → β₁ ⊕ β₂ → Finset (γ₁ ⊕ γ₂)
-- Mathlib.CategoryTheory.Adjunction.Triple
/-- For an adjoint triple `F ⊣ G ⊣ H` where `G` is fully faithful, the natural transformation
`F.op ⟶ H.op` obtained from the dual adjoint triple `H.op ⊣ G.op ⊣ F.op` is dual to the natural
transformation `H ⟶ F`.  -/
CategoryTheory.Adjunction.Triple.op_rightToLeft : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  {H : CategoryTheory.Functor C D} (t : CategoryTheory.Adjunction.Triple F G H) [inst_2 : G.Full] [inst_3 : G.Faithful],
  t.op.rightToLeft = CategoryTheory.NatTrans.op t.rightToLeft
-- Mathlib.MeasureTheory.Integral.Prod
MeasureTheory.Integrable.op_fst_snd : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E] {F : Type u_4}
  {G : Type u_5} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedAddCommGroup G] {op : E → F → G},
  Continuous (Function.uncurry op) →
    (∃ C, ∀ (x : E) (y : F), ‖op x y‖ ≤ C * ‖x‖ * ‖y‖) →
      ∀ {f : α → E} {g : β → F},
        MeasureTheory.Integrable f μ →
          MeasureTheory.Integrable g ν → MeasureTheory.Integrable (fun z => op (f z.1) (g z.2)) (μ.prod ν)
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- The bilinear pairing of Schwartz functions.

The continuity in the left argument is provided in `SchwartzMap.pairing_continuous_left`.  -/
SchwartzMap.pairing : {𝕜 : Type u_2} →
  {D : Type u_4} →
    {E : Type u_5} →
      {F : Type u_6} →
        {G : Type u_7} →
          [inst : NormedAddCommGroup E] →
            [inst_1 : NormedSpace ℝ E] →
              [inst_2 : NormedAddCommGroup F] →
                [inst_3 : NormedSpace ℝ F] →
                  [inst_4 : NontriviallyNormedField 𝕜] →
                    [inst_5 : NormedAlgebra ℝ 𝕜] →
                      [inst_6 : NormedAddCommGroup D] →
                        [inst_7 : NormedSpace ℝ D] →
                          [inst_8 : NormedAddCommGroup G] →
                            [inst_9 : NormedSpace ℝ G] →
                              [inst_10 : NormedSpace 𝕜 F] →
                                [inst_11 : NormedSpace 𝕜 E] →
                                  [inst_12 : NormedSpace 𝕜 G] →
                                    (E →L[𝕜] F →L[𝕜] G) → SchwartzMap D E →ₗ[𝕜] SchwartzMap D F →L[𝕜] SchwartzMap D G
-- Init.PropLemmas
ite_iff_left_iff : ∀ {p : Prop} [inst : Decidable p] {x y : Prop}, ((if p then x else y) ↔ x) ↔ ¬p → y = x
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.NonUnitalRing.lift_apply : ∀ {ι : Type u_2} [inst : Preorder ι] (G : ι → Type u_3) {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  (f : (x x_1 : ι) → (h : x ≤ x_1) → T h) [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι]
  [inst_4 : (i : ι) → NonUnitalNonAssocSemiring (G i)]
  [inst_5 : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] [inst_6 : Nonempty ι] (P : Type u_7)
  [inst_7 : NonUnitalNonAssocSemiring P] (g : (i : ι) → G i →ₙ+* P)
  (Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x) (z : DirectLimit G f),
  (DirectLimit.NonUnitalRing.lift G f P g Hg) z = DirectLimit.lift f (fun x1 x2 => (g x1) x2) ⋯ z
-- Mathlib.Algebra.BigOperators.Finprod
finprod_mem_inter_mulSupport_eq : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] (f : α → M) (s t : Set α),
  s ∩ Function.mulSupport f = t ∩ Function.mulSupport f → ∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ᶠ (i : α) (_ : i ∈ t), f i
-- Mathlib.Topology.Algebra.MetricSpace.Lipschitz
/-- If `f` is locally Lipschitz on a compact set `s`, it is Lipschitz on `s`.  -/
LocallyLipschitzOn.exists_lipschitzOnWith_of_compact : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β} {s : Set α},
  IsCompact s → LocallyLipschitzOn s f → ∃ K, LipschitzOnWith K f s
-- Mathlib.Data.Nat.Choose.Multinomial
/-- The multinomial coefficient. Gives the number of strings consisting of symbols
from `s`, where `c ∈ s` appears with multiplicity `f c`.

Defined as `(∑ i ∈ s, f i)! / ∏ i ∈ s, (f i)!`.
 -/
Nat.multinomial : {α : Type u_1} → Finset α → (α → ℕ) → ℕ
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.equivIoc_coe_of_mem : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] {p : 𝕜} [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  [hp : Fact (0 < p)] {a : 𝕜} [inst_3 : Archimedean 𝕜] {y : 𝕜},
  y ∈ Set.Ioc a (a + p) → ↑((AddCircle.equivIoc p a) ↑y) = y
-- Mathlib.LinearAlgebra.Alternating.DomCoprod
/-- Swapping elements in `σ` with equal values in `v` result in zero if the swap has no effect
on the quotient.  -/
AlternatingMap.domCoprod.summand_eq_zero_of_smul_invariant : ∀ {ιa : Type u_1} {ιb : Type u_2} [inst : Fintype ιa] [inst_1 : Fintype ιb] {R' : Type u_3} {Mᵢ : Type u_4}
  {N₁ : Type u_5} {N₂ : Type u_6} [inst_2 : CommSemiring R'] [inst_3 : AddCommGroup N₁] [inst_4 : Module R' N₁]
  [inst_5 : AddCommGroup N₂] [inst_6 : Module R' N₂] [inst_7 : AddCommMonoid Mᵢ] [inst_8 : Module R' Mᵢ]
  [inst_9 : DecidableEq ιa] [inst_10 : DecidableEq ιb] (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂)
  (σ : Equiv.Perm.ModSumCongr ιa ιb) {v : ιa ⊕ ιb → Mᵢ} {i j : ιa ⊕ ιb},
  v i = v j → i ≠ j → Equiv.swap i j • σ = σ → (AlternatingMap.domCoprod.summand a b σ) v = 0
-- Mathlib.GroupTheory.Index
/-- If `J` has finite index in `K`, then the same holds for their comaps under any group hom.  -/
Subgroup.relIndex_comap_ne_zero : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] (f : G →* G') {J K : Subgroup G'},
  J.relIndex K ≠ 0 → (Subgroup.comap f J).relIndex (Subgroup.comap f K) ≠ 0
-- Mathlib.CategoryTheory.Monoidal.Opposite.Mon
MonObj.mopEquivCompForgetIso_hom_app_unmop : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X : CategoryTheory.Mon C), (MonObj.mopEquivCompForgetIso.hom.app X).unmop = CategoryTheory.CategoryStruct.id X.X
-- Std.Async.TCP
/-- Binds the server socket to the specified address. Address reuse is enabled to allow rebinding the
same address.
 -/
Std.Async.TCP.Socket.Server.bind : Std.Async.TCP.Socket.Server → Std.Net.SocketAddress → IO Unit
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.obj.σ_def_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} [inst_4 : F.LaxMonoidal] (X : C) [inst_5 : CategoryTheory.AddMonObj X] {Z : D}
  (h : F.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F X X)
      (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.AddMonObj.add) h)
-- Lean.Meta.NatInstTesters
Lean.Meta.DefEq.isInstAddNat : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Analysis.Analytic.Basic
/-- Given a function `f : E → F` and a formal multilinear series `p`, we say that `f` has `p` as
a power series on the ball of radius `r > 0` around `x` if `f (x + y) = ∑' pₙ yⁿ` for all `‖y‖ < r`.
 -/
HasFPowerSeriesOnBall : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] → (E → F) → FormalMultilinearSeries 𝕜 E F → E → ENNReal → Prop
-- Mathlib.Algebra.Homology.Embedding.Connect
CochainComplex.ConnectData.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (d₀ : K.X 0 ⟶ L.X 0)
  (comp_d₀ : CategoryTheory.CategoryStruct.comp (K.d 1 0) d₀ = 0)
  (d₀_comp : CategoryTheory.CategoryStruct.comp d₀ (L.d 0 1) = 0) (d₀_1 : K.X 0 ⟶ L.X 0)
  (comp_d₀_1 : CategoryTheory.CategoryStruct.comp (K.d 1 0) d₀_1 = 0)
  (d₀_comp_1 : CategoryTheory.CategoryStruct.comp d₀_1 (L.d 0 1) = 0),
  ({ d₀ := d₀, comp_d₀ := comp_d₀, d₀_comp := d₀_comp } = { d₀ := d₀_1, comp_d₀ := comp_d₀_1, d₀_comp := d₀_comp_1 }) =
    (d₀ = d₀_1)
-- Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight
/-- If `IsEffective R S` is true, then the equalizer of `s ↦ s ⊗ₜ 1 : S →+* S ⊗[R] S` and
`s ↦ 1 ⊗ₜ s : S →+* S ⊗[R] S` is the image of `algebraMap R S : R →+* S`.  -/
Algebra.IsEffective.eqLocus_includeLeft_includeRight : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : Ring S] [inst_2 : Algebra R S],
  Algebra.IsEffective R S →
    ↑(Algebra.TensorProduct.includeLeftRingHom.eqLocus Algebra.TensorProduct.includeRight.toRingHom) =
      Set.range ⇑(algebraMap R S)
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinOrder.val_unit : ∀ {M : Type u_6} [inst : Monoid M] {x : M} (hx : IsOfFinOrder x), ↑hx.unit = x
-- Init.Data.UInt.Lemmas
UInt16.toUSize_sub : ∀ (a b : UInt16), (a - b).toUSize = (a.toUSize - b.toUSize) % 65536
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsAddFundamentalDomain.integrableOn_iff : ∀ {G : Type u_1} {α : Type u_3} {E : Type u_5} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α]
  [inst_3 : NormedAddCommGroup E] {s t : Set α} {μ : MeasureTheory.Measure α} [MeasurableConstVAdd G α]
  [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G],
  MeasureTheory.IsAddFundamentalDomain G s μ →
    MeasureTheory.IsAddFundamentalDomain G t μ →
      ∀ {f : α → E},
        (∀ (g : G) (x : α), f (g +ᵥ x) = f x) → (MeasureTheory.IntegrableOn f s μ ↔ MeasureTheory.IntegrableOn f t μ)
-- Mathlib.Topology.Algebra.SeparationQuotient.Hom
SeparationQuotient.liftContinuousCommMonoidHom_mk : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : CommMonoid M]
  [inst_3 : ContinuousMul M] [inst_4 : CommMonoid N] (f : M →ₜ* N) (hf : ∀ (x y : M), Inseparable x y → f x = f y)
  (x : M), (SeparationQuotient.liftContinuousMonoidHom f hf) (SeparationQuotient.mk x) = f x
-- Lean.Parser.Do
Lean.Parser.Term.doSeqBracketed : Lean.Parser.Parser
-- Mathlib.GroupTheory.Torsion
IsMulTorsion.torsionMulEquiv_apply : ∀ {G : Type u_1} [inst : CommMonoid G] (tG : IsMulTorsion G) (a : ↥(CommMonoid.torsion G)),
  tG.torsionMulEquiv a = ↑((MulEquiv.submonoidCongr ⋯) a)
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.StronglyAdapted.measurable_upcrossingsBefore : ∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {a b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {ℱ : MeasureTheory.Filtration ℕ m0},
  MeasureTheory.StronglyAdapted ℱ f → a < b → Measurable (MeasureTheory.upcrossingsBefore a b f N)
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.isUniformEmbedding : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {E₁ : Type u_8} {E₂ : Type u_9}
  [inst_4 : UniformSpace E₁] [inst_5 : UniformSpace E₂] [inst_6 : AddCommGroup E₁] [inst_7 : AddCommGroup E₂]
  [inst_8 : Module R₁ E₁] [inst_9 : Module R₂ E₂] [IsUniformAddGroup E₁] [IsUniformAddGroup E₂] (e : E₁ ≃SL[σ₁₂] E₂),
  IsUniformEmbedding ⇑e
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instAddGroup : {α : Type u_1} → [AddGroup α] → AddGroup (Lex α)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LitValue.uint64.inj : ∀ {val val_1 : UInt64}, Lean.Compiler.LCNF.LitValue.uint64 val = Lean.Compiler.LCNF.LitValue.uint64 val_1 → val = val_1
-- Mathlib.Algebra.Category.MonCat.Adjunctions
AddMonCat.adjoinZeroAdj.eq_1 : AddMonCat.adjoinZeroAdj =
  CategoryTheory.Adjunction.mkOfHomEquiv
    {
      homEquiv := fun X Y =>
        CategoryTheory.ConcreteCategory.homEquiv.trans
          (WithZero.lift.symm.trans CategoryTheory.ConcreteCategory.homEquiv.symm),
      homEquiv_naturality_left_symm := @AddMonCat.adjoinZeroAdj._proof_1,
      homEquiv_naturality_right := @AddMonCat.adjoinZeroAdj._proof_2 }
-- Mathlib.Analysis.Convex.Basic
convex_iff_segment_subset : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {s : Set E}, Convex 𝕜 s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → segment 𝕜 x y ⊆ s
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.instInhabited.eq_1 : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G], OpenSubgroup.instInhabited = { default := ⊤ }
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
AddSubgroup.isAddCyclic_iff_exists_zmultiples_eq_top : ∀ {α : Type u_1} [inst : AddGroup α] (H : AddSubgroup α), IsAddCyclic ↥H ↔ ∃ g, AddSubgroup.zmultiples g = H
-- Std.Data.HashSet.Lemmas
Std.HashSet.get?_filter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {f : α → Bool}
  {k : α}, (Std.HashSet.filter f m).get? k = Option.filter f (m.get? k)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.UnsatProof.le.injEq : ∀ (c c_1 : Lean.Meta.Grind.Arith.Cutsat.LeCnstr),
  (Lean.Meta.Grind.Arith.Cutsat.UnsatProof.le c = Lean.Meta.Grind.Arith.Cutsat.UnsatProof.le c_1) = (c = c_1)
-- Mathlib.NumberTheory.Modular
/-- The standard open fundamental domain of the action of `SL(2,ℤ)` on `ℍ`.  -/
ModularGroup.fdo : Set UpperHalfPlane
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.ι_inj : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R] [Nontrivial R] (x y : X),
  FreeAlgebra.ι R x = FreeAlgebra.ι R y ↔ x = y
-- Mathlib.Analysis.CStarAlgebra.Module.Constructions
WithCStarModule.inner_single_left : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] {ι : Type u_2} {E : ι → Type u_3}
  [inst_2 : Fintype ι] [inst_3 : (i : ι) → NormedAddCommGroup (E i)] [inst_4 : (i : ι) → Module ℂ (E i)]
  [inst_5 : (i : ι) → SMul A (E i)] [inst_6 : (i : ι) → CStarModule A (E i)] [inst_7 : StarOrderedRing A]
  [inst_8 : DecidableEq ι] (x : WithCStarModule A ((i : ι) → E i)) {i : ι} (y : E i),
  inner A ((WithCStarModule.equiv A ((j : ι) → E j)).symm (Pi.single i y)) x = inner A y (x i)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Equiv.diff_congr : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ m₃ m₄ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → (↑m₃).WF → (↑m₄).WF → (↑m₁).Equiv ↑m₃ → (↑m₂).Equiv ↑m₄ → (↑(m₁.diff m₂)).Equiv ↑(m₃.diff m₄)
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.instZero : Zero Cardinal.{u}
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.getGED_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {k fallback : α},
  t₁.Equiv t₂ → t₁.getGED k fallback = t₂.getGED k fallback
-- Mathlib.CategoryTheory.Presentable.ColimitPresentation
CategoryTheory.Limits.ColimitPresentation.instLocallySmallTotal : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u_1} {I : J → Type u_2}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] [inst_2 : (j : J) → CategoryTheory.Category.{u_3, u_2} (I j)]
  {D : CategoryTheory.Functor J C} {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)}
  [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.LocallySmall.{w, v_1, u_1} J],
  CategoryTheory.LocallySmall.{w, max v v_1, max u_2 u_1} (CategoryTheory.Limits.ColimitPresentation.Total P)