mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
/-- If the symmetric difference of two positive sets is a null-set, then so are the differences
between the two sets.  -/
MeasureTheory.SignedMeasure.of_sdiff_eq_zero_of_symmDiff_eq_zero_positive : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} {u v : Set α},
  MeasurableSet u →
    MeasurableSet v →
      MeasureTheory.VectorMeasure.restrict 0 u ≤ MeasureTheory.VectorMeasure.restrict s u →
        MeasureTheory.VectorMeasure.restrict 0 v ≤ MeasureTheory.VectorMeasure.restrict s v →
          s (symmDiff u v) = 0 → s (u \ v) = 0 ∧ s (v \ u) = 0
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.Arrows.Compatible.exists_familyOfElements : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {B : C}
  {I : Type u_1} {X : I → C} {π : (i : I) → X i ⟶ B} {x : (i : I) → P.obj (Opposite.op (X i))},
  CategoryTheory.Presieve.Arrows.Compatible P π x → ∃ x', ∀ (i : I), x' (π i) ⋯ = x i
-- Mathlib.Topology.Separation.Profinite
/-- Every member of an open set in a compact Hausdorff totally disconnected space
is contained in a clopen set contained in the open set.  -/
compact_exists_isClopen_in_isOpen : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X] [CompactSpace X] [TotallyDisconnectedSpace X] {x : X}
  {U : Set X}, IsOpen U → x ∈ U → ∃ V, IsClopen V ∧ x ∈ V ∧ V ⊆ U
-- Lean.MetavarContext
/-- Return free variables in `xs` that are in the local context `lctx`  -/
_private.Lean.MetavarContext.0.Lean.MetavarContext.MkBinding.getInScope : Lean.LocalContext → Array Lean.Expr → Array Lean.Expr
-- Init.Data.Int.Bitwise.Lemmas
Int.shiftLeft_mul_shiftLeft : ∀ (a b : ℤ) (m n : ℕ), a <<< m * b <<< n = (a * b) <<< (m + n)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HasHomology.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C}, Nonempty S.HomologyData → S.HasHomology
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.zero_subset : ∀ {α : Type u_2} [inst : Zero α] {s : Finset α}, 0 ⊆ s ↔ 0 ∈ s
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.insert_eq_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {p : α},
  insert p t = t.insert p
-- Mathlib.Data.Set.SMulAntidiagonal
/-- `smulAntidiagonal s t a` is the set of all pairs of an element in `s` and an element in `t`
that scalar multiply to `a`.  -/
Set.smulAntidiagonal : {G : Type u_1} → {P : Type u_2} → [SMul G P] → Set G → Set P → P → Set (G × P)
-- Mathlib.Data.Ordmap.Invariants
Ordnode.Sized.size_eq : ∀ {α : Type u_1} {s : ℕ} {l : Ordnode α} {x : α} {r : Ordnode α},
  (Ordnode.node s l x r).Sized → (Ordnode.node s l x r).size = l.size + r.size + 1
-- Mathlib.Order.ModularLattice
eq_of_le_of_sup_le_of_le_inf : ∀ {α : Type u_1} [inst : Lattice α] [IsModularLattice α] {x y z : α}, y ≤ x → x ≤ y ⊔ z → x ⊓ z ≤ y → x = y
-- Mathlib.GroupTheory.Index
AddSubgroup.exists_nsmul_mem_of_index_ne_zero : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, H.index ≠ 0 → ∀ (a : G), ∃ n, 0 < n ∧ n ≤ H.index ∧ n • a ∈ H
-- Mathlib.CategoryTheory.GradedObject.Unitor
/-- Given `F : C ⥤ D ⥤ D`, `X : C`, `e : F.obj X ≅ 𝟭 D`, `Y : GradedObject J D` and
`p : I × J → J` such that `p ⟨0, j⟩ = j` for all `j`,
this is the (colimit) cofan which shall be used to construct the isomorphism
`mapBifunctorMapObj F p ((single₀ I).obj X) Y ≅ Y`, see `mapBifunctorLeftUnitor`.  -/
CategoryTheory.GradedObject.mapBifunctorLeftUnitorCofan : {C : Type u_1} →
  {D : Type u_2} →
    {I : Type u_3} →
      {J : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} C] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
            [inst_2 : Zero I] →
              [inst_3 : DecidableEq I] →
                [inst_4 : CategoryTheory.Limits.HasInitial C] →
                  (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) →
                    (X : C) →
                      (F.obj X ≅ CategoryTheory.Functor.id D) →
                        [∀ (Y : D),
                              CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)] →
                          (p : I × J → J) →
                            (∀ (j : J), p (0, j) = j) →
                              (Y : CategoryTheory.GradedObject J D) →
                                (j : J) →
                                  (((CategoryTheory.GradedObject.mapBifunctor F I J).obj
                                            ((CategoryTheory.GradedObject.single₀ I).obj X)).obj
                                        Y).CofanMapObjFun
                                    p j
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokensParams : Type
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.instInfSet : {R : Type u} → [inst : NonUnitalNonAssocSemiring R] → InfSet (NonUnitalSubsemiring R)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
MonoidHom.toLocalizationMap.eq_1 : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] (f : M →* N)
  (H1 : ∀ (y : ↥S), IsUnit (f ↑y)) (H2 : ∀ (z : N), ∃ x, z * f ↑x.2 = f x.1)
  (H3 : ∀ (x y : M), f x = f y → ∃ c, ↑c * x = ↑c * y),
  f.toLocalizationMap H1 H2 H3 = { toFun := (↑f).toFun, map_mul' := ⋯, isLocalizationMap := ⋯ }
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurableSet_setOfPred : ∀ {α : Type u_1} [inst : MeasurableSpace α] {p : α → Prop}, MeasurableSet {a | p a} ↔ Measurable p
-- Mathlib.Algebra.Homology.ShortComplex.Linear
CategoryTheory.ShortComplex.instModuleHom : {R : Type u_1} →
  {C : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : CategoryTheory.Category.{v_1, u_2} C] →
        [inst_2 : CategoryTheory.Preadditive C] →
          [CategoryTheory.Linear R C] → {S₁ S₂ : CategoryTheory.ShortComplex C} → Module R (S₁ ⟶ S₂)
-- Mathlib.Data.Fintype.Card
Finset.card_fin : ∀ (n : ℕ), Finset.univ.card = n
-- Mathlib.Algebra.LieRinehartAlgebra.Defs
/-- The identity morphism of a Lie-Rinehart algebra over the identity algebra homomorphism of the
underlying algebra.  -/
LieRinehartAlgebra.Hom.id : {R : Type u_1} →
  {A₁ : Type u_2} →
    {L₁ : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : CommRing A₁] →
          [inst_2 : LieRing L₁] →
            [inst_3 : Module A₁ L₁] →
              [inst_4 : LieRingModule L₁ A₁] →
                [inst_5 : Algebra R A₁] → [inst_6 : LieAlgebra R L₁] → LieRinehartAlgebra.Hom (AlgHom.id R A₁) L₁ L₁
-- Mathlib.GroupTheory.Congruence.Hom
/-- The diagram describing the universal property for quotients of
`AddMonoid`s commutes.  -/
AddCon.lift_comp_mk' : ∀ {M : Type u_1} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass P] {c : AddCon M} {f : M →+ P}
  (H : c ≤ AddCon.ker f), (c.lift f H).comp c.mk' = f
-- Mathlib.Algebra.Group.Action.Units
AddUnits.instFaithfulVAdd : ∀ {M : Type u_3} {α : Type u_5} [inst : AddMonoid M] [inst_1 : VAdd M α] [FaithfulVAdd M α], FaithfulVAdd (AddUnits M) α
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnModule.support_smul_subset_vadd_support' : ∀ {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_5} [inst : PartialOrder Γ] [inst_1 : PartialOrder Γ']
  [inst_2 : VAdd Γ Γ'] [inst_3 : IsOrderedCancelVAdd Γ Γ'] [inst_4 : AddCommMonoid V] [inst_5 : MulZeroClass R]
  [inst_6 : SMulWithZero R V] {x : HahnSeries Γ R} {y : HahnModule Γ' R V},
  ((HahnModule.of R).symm (x • y)).support ⊆ x.support +ᵥ ((HahnModule.of R).symm y).support
-- Mathlib.LinearAlgebra.Matrix.Integer
Matrix.map_mul_natCast : ∀ {n : Type u_2} [inst : Fintype n] {α : Type u_3} [inst_1 : NonAssocSemiring α] (A B : Matrix n n ℕ),
  (A * B).map Nat.cast = A.map Nat.cast * B.map Nat.cast
-- Init.Data.String.Lemmas.Pattern.Pred
_private.Init.Data.String.Lemmas.Pattern.Pred.0.String.Slice.Pos.skipWhile.eq_1 : ∀ {ρ : Type} {s : String.Slice} (pos : s.Pos) (pat : ρ) [inst : String.Slice.Pattern.ForwardPattern pat],
  pos.skipWhile pat =
    match pos.skip? pat with
    | some nextCurr => if pos < nextCurr then nextCurr.skipWhile pat else pos
    | none => pos
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.FullyFaithful.compUliftCoyonedaCompWhiskeringLeft_hom_app_app_hom_apply_down : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (X : Cᵒᵖ) (X_1 : C)
  (x : (F.comp (CategoryTheory.uliftCoyoneda.{v₁, v₂, u₂}.obj (Opposite.op (F.obj (Opposite.unop X))))).obj X_1),
  ((CategoryTheory.ConcreteCategory.hom ((hF.compUliftCoyonedaCompWhiskeringLeft.hom.app X).app X_1)) x).down =
    hF.preimage x.down
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, (t.insertIfNew k v).maxKey ⋯ = t.maxKey?.elim k fun k' => if cmp k' k = Ordering.lt then k else k'
-- Mathlib.Algebra.Group.Commute.Units
Commute.mul_inv_eq_mul_inv_iff_of_isUnit : ∀ {M : Type u_1} [inst : DivisionMonoid M] {a b c d : M},
  Commute b d → IsUnit b → IsUnit d → (a * b⁻¹ = c * d⁻¹ ↔ a * d = c * b)
-- Mathlib.GroupTheory.FinitelyPresentedGroup
AddGroup.IsFinitelyPresented.instOfFinite : ∀ (G : Type u_1) [inst : AddGroup G] [Finite G], AddGroup.IsFinitelyPresented G
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.lcm.eq_1 : ∀ {R : Type u} [inst : EuclideanDomain R] [inst_1 : DecidableEq R] (x y : R),
  EuclideanDomain.lcm x y = x * y / EuclideanDomain.gcd x y
-- Mathlib.Data.List.Sort
_private.Mathlib.Data.List.Sort.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.RingTheory.Localization.Submodule
IsLocalization.coeSubmodule_strictMono : ∀ {R : Type u_3} [inst : CommRing R] {M : Submonoid R} {S : Type u_4} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [IsLocalization M S], M ≤ nonZeroDivisors R → StrictMono (IsLocalization.coeSubmodule S)
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.mem_domain_of_mem_graph : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_4} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_5}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] {f : E →ₗ.[R] F} {x : E} {y : F}, (x, y) ∈ f.graph → x ∈ f.domain
-- Mathlib.RingTheory.TensorProduct.IsBaseChangeFree
/-- The basis of a module deduced by base change from a free module with a basis.  -/
IsBaseChange.basis : {R : Type u_1} →
  [inst : CommSemiring R] →
    {S : Type u_2} →
      [inst_1 : CommSemiring S] →
        [inst_2 : Algebra R S] →
          {V : Type u_3} →
            [inst_3 : AddCommMonoid V] →
              [inst_4 : Module R V] →
                {W : Type u_4} →
                  [inst_5 : AddCommMonoid W] →
                    [inst_6 : Module R W] →
                      [inst_7 : Module S W] →
                        [inst_8 : IsScalarTower R S W] →
                          {ι : Type u_5} → {ε : V →ₗ[R] W} → Module.Basis ι R V → IsBaseChange S ε → Module.Basis ι S W
-- Mathlib.Analysis.MeanInequalities
/-- **Alias** of `Real.geom_mean_eq_arith_mean_weighted_iff_of_nonneg'`.

---

**AM-GM inequality - equality condition**: This theorem provides the equality condition for the
weighted version of the AM-GM inequality for real-valued nonnegative functions.

The condition is that all elements of `z` with a nonzero weight are equal to their center of mass
`∑ i ∈ s, w i * z i`; see `geom_mean_eq_arith_mean_weighted_iff_of_nonneg` for a version that
compares the elements to each other instead.  -/
Real.geom_mean_eq_arith_mean_weighted_iff : ∀ {ι : Type u} (s : Finset ι) (w z : ι → ℝ),
  (∀ i ∈ s, 0 ≤ w i) →
    ∑ i ∈ s, w i = 1 →
      (∀ i ∈ s, 0 ≤ z i) → (∏ i ∈ s, z i ^ w i = ∑ i ∈ s, w i * z i ↔ ∀ j ∈ s, w j ≠ 0 → z j = ∑ i ∈ s, w i * z i)
-- Mathlib.Geometry.Manifold.MFDeriv.Defs
/-- Predicate ensuring that, at a point and within a set, a function can have at most one
derivative. This is expressed using the preferred chart at the considered point.  -/
UniqueMDiffWithinAt : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_3} →
            [inst_3 : TopologicalSpace H] →
              ModelWithCorners 𝕜 E H →
                {M : Type u_4} → [inst : TopologicalSpace M] → [ChartedSpace H M] → Set M → M → Prop
-- Mathlib.RingTheory.Ideal.KrullsHeightTheorem
/-- If `p` is a prime ideal containing `s`, the height of `p` is bounded
by the sum of the height of the image of `p` in `R ⧸ (s)` and the cardinality of `s`.  -/
Ideal.height_le_height_add_encard_of_subset : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (s : Set R) {p : Ideal R} [p.IsPrime],
  s ⊆ ↑p → p.height ≤ (Ideal.map (Ideal.Quotient.mk (Ideal.span s)) p).height + s.encard
-- Mathlib.CategoryTheory.Sites.CoverLifting
CategoryTheory.instIsContinuousRightAdjointOfIsCocontinuous : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) {F : CategoryTheory.Functor C D} [F.IsCocontinuous J K]
  [inst_3 : F.IsLeftAdjoint], F.rightAdjoint.IsContinuous K J
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming
Tactic.ComputeAsymptotics.MultiseriesExpansion.Trimmed.brecOn : ∀
  {motive :
    {basis : Tactic.ComputeAsymptotics.Basis} →
      (a : Tactic.ComputeAsymptotics.MultiseriesExpansion basis) → a.Trimmed → Prop}
  {basis : Tactic.ComputeAsymptotics.Basis} {a : Tactic.ComputeAsymptotics.MultiseriesExpansion basis} (t : a.Trimmed),
  (∀ {basis : Tactic.ComputeAsymptotics.Basis} (a : Tactic.ComputeAsymptotics.MultiseriesExpansion basis)
      (t : a.Trimmed), Tactic.ComputeAsymptotics.MultiseriesExpansion.Trimmed.below t → motive a t) →
    motive a t
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.CompactOpens.map_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] (f : β → γ) (g : α → β) (hf : Continuous f) (hg : Continuous g) (hf' : IsOpenMap f)
  (hg' : IsOpenMap g) (K : TopologicalSpace.CompactOpens α),
  TopologicalSpace.CompactOpens.map (f ∘ g) ⋯ ⋯ K =
    TopologicalSpace.CompactOpens.map f hf hf' (TopologicalSpace.CompactOpens.map g hg hg' K)
-- Mathlib.Analysis.Calculus.Darboux
/-- **Darboux's theorem**: the image of a convex set under `f'` is a convex set,
`derivWithin` version.  -/
Convex.image_derivWithin : ∀ {f : ℝ → ℝ} {s : Set ℝ}, Convex ℝ s → DifferentiableOn ℝ f s → Convex ℝ (derivWithin f s '' s)
-- Mathlib.Topology.Separation.Regular
/-- A weakly locally compact R₁ space is regular.  -/
instRegularSpaceOfWeaklyLocallyCompactSpaceOfR1Space : ∀ {X : Type u_1} [inst : TopologicalSpace X] [WeaklyLocallyCompactSpace X] [R1Space X], RegularSpace X
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.instSupSet.eq_1 : ∀ {α : Type u_1} [inst : LE α], LowerSet.instSupSet = { sSup := fun S => { carrier := ⋃ s ∈ S, ↑s, lower' := ⋯ } }
-- Mathlib.RingTheory.Bialgebra.Equiv
/-- The equivalence of types underlying a bialgebra equivalence.  -/
BialgEquiv.toEquiv : {R : Type u} →
  {A : Type v} →
    {B : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra R B] →
                [inst_5 : CoalgebraStruct R A] → [inst_6 : CoalgebraStruct R B] → (A ≃ₐc[R] B) → A ≃ B
-- Mathlib.Order.Notation
/-- Typeclass for the `⊥` (`\bot`) notation  -/
Bot : Type u_1 → Type u_1
-- Lean.Meta.Tactic.Grind.Action
_private.Lean.Meta.Tactic.Grind.Action.0.Lean.Meta.Grind.Action.andThen.eq_1 : ∀ (x y : Lean.Meta.Grind.Action) (goal : Lean.Meta.Grind.Goal) (kna kp : Lean.Meta.Grind.ActionCont),
  x.andThen y goal kna kp = x goal kna fun goal' => y goal' kp kp
-- Mathlib.Computability.Primrec.Basic
Primcodable.prod : {α : Type u_1} → {β : Type u_2} → [Primcodable α] → [Primcodable β] → Primcodable (α × β)
-- Mathlib.Analysis.Convex.Deriv
StrictConvexOn.slope_lt_leftDeriv : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y : ℝ},
  StrictConvexOn ℝ S f →
    x ∈ S → y ∈ S → x < y → DifferentiableWithinAt ℝ f (Set.Iio y) y → slope f x y < derivWithin f (Set.Iio y) y
-- Mathlib.Algebra.Homology.Factorizations.CM5a
/-- The first morphism `ι f n₀ : K ⟶ mid f n₀` of the factorization lemma `cm5a_cof`.  -/
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.ι : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {K L : CochainComplex C ℤ} →
        (f : K ⟶ L) →
          [inst_2 : CategoryTheory.EnoughInjectives C] →
            [inst_3 : CategoryTheory.Mono f] →
              (n₀ : ℤ) →
                [inst_4 : K.IsStrictlyGE (n₀ + 1)] →
                  [inst_5 : L.IsStrictlyGE (n₀ + 1)] → K ⟶ CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.mid✝ f n₀
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.homIso_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor J C) [inst_2 : CategoryTheory.Limits.HasLimit F] {W : C},
  (CategoryTheory.Limits.limit.homIso F W).hom =
    TypeCat.ofHom fun f =>
      CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.const J).map f.down)
        (CategoryTheory.Limits.limit.cone F).π
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- Given a commutative diagram
```
    X --f--> Y --g--> Z
    |        |        |
    |        |        |
    v        v        v
    X' -f'-> Y' -g'-> Z'
```
with horizontal arrows composing to zero,
then we obtain a commutative square
```
   X ---> kernel g
   |         |
   |         | kernel.map
   |         |
   v         v
   X' --> kernel g'
```
 -/
CategoryTheory.Limits.kernel.lift_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y Z X' Y' Z' : C} (f : X ⟶ Y) (g : Y ⟶ Z) [inst_2 : CategoryTheory.Limits.HasKernel g]
  (w : CategoryTheory.CategoryStruct.comp f g = 0) (f' : X' ⟶ Y') (g' : Y' ⟶ Z')
  [inst_3 : CategoryTheory.Limits.HasKernel g'] (w' : CategoryTheory.CategoryStruct.comp f' g' = 0) (p : X ⟶ X')
  (q : Y ⟶ Y') (r : Z ⟶ Z'),
  CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p f' →
    ∀ (h₂ : CategoryTheory.CategoryStruct.comp g r = CategoryTheory.CategoryStruct.comp q g'),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.lift g f w)
          (CategoryTheory.Limits.kernel.map g g' q r h₂) =
        CategoryTheory.CategoryStruct.comp p (CategoryTheory.Limits.kernel.lift g' f' w')
-- Mathlib.Order.Hom.CompleteLattice
/-- The proposition that frame homomorphisms commute with arbitrary suprema/joins.  -/
FrameHom.map_sSup' : ∀ {α : Type u_8} {β : Type u_9} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (self : FrameHom α β)
  (s : Set α), self.toFun (sSup s) = sSup (self.toFun '' s)
-- Mathlib.Analysis.Matrix.Order
/-- A positive definite matrix `M` induces a norm on `Matrix n n 𝕜`:
`‖x‖ = sqrt (x * M * xᴴ).trace`.  -/
Matrix.toMatrixNormedAddCommGroup : {𝕜 : Type u_1} →
  {n : Type u_2} → [inst : RCLike 𝕜] → [Fintype n] → (M : Matrix n n 𝕜) → M.PosDef → NormedAddCommGroup (Matrix n n 𝕜)
-- Mathlib.CategoryTheory.Sites.Point.Skyscraper
CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.Limits.HasProducts A]
  {P : CategoryTheory.Functor Cᵒᵖ A} {M : A} [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A]
  (g : P ⟶ Φ.skyscraperPresheaf M),
  Φ.skyscraperPresheafHomEquiv.symm g =
    Φ.presheafFiberDesc
      (fun X x =>
        CategoryTheory.CategoryStruct.comp (g.app (Opposite.op X)) (CategoryTheory.Limits.Pi.π (fun t => M) x))
      ⋯
-- Mathlib.Analysis.Calculus.Implicit
ImplicitFunctionData.rightFun_implicitFunction_eq_rightFun : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {G : Type u_4} [inst_7 : NormedAddCommGroup G]
  [inst_8 : NormedSpace 𝕜 G] [inst_9 : CompleteSpace G] (φ : ImplicitFunctionData 𝕜 E F G),
  ∀ᶠ (x : E) in nhds φ.pt, φ.rightFun (φ.implicitFunction (φ.leftFun φ.pt) (φ.rightFun x)) = φ.rightFun x
-- Mathlib.CategoryTheory.Monoidal.Tor
CategoryTheory.Functor.leftDerived.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasProjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] (F F_1 : CategoryTheory.Functor C D) (e_F : F = F_1) [inst_5 : F.Additive]
  (n n_1 : ℕ), n = n_1 → F.leftDerived n = F_1.leftDerived n_1
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.comap_injective : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] [inst_6 : Semiring B] [inst_7 : StarRing B]
  [inst_8 : Algebra R B] [inst_9 : StarModule R B] {f : A →⋆ₐ[R] B},
  Function.Surjective ⇑f → Function.Injective (StarSubalgebra.comap f)
-- Mathlib.Algebra.Field.Defs
DivisionRing.toRatCast : {K : Type u_2} → [self : DivisionRing K] → RatCast K
-- Mathlib.Topology.MetricSpace.Gluing
Metric.glueDist.eq_3 : ∀ {X : Type u} {Y : Type v} {Z : Type w} [inst : MetricSpace X] [inst_1 : MetricSpace Y] (Φ : Z → X) (Ψ : Z → Y) (ε : ℝ)
  (x_2 : X) (y : Y), Metric.glueDist Φ Ψ ε (Sum.inl x_2) (Sum.inr y) = (⨅ p, dist x_2 (Φ p) + dist y (Ψ p)) + ε
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakKernels
CategoryTheory.Limits.weakEqualizer_as_weakKernel : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasWeakKernel f],
  CategoryTheory.Limits.weakEqualizer.ι f 0 = CategoryTheory.Limits.weakKernel.ι f
-- Init.Data.String.TakeDrop
String.Slice.stripPrefix : String.Slice → String.Slice → String.Slice
-- Aesop.Tree.Data
Aesop.GoalId.mk.sizeOf_spec : ∀ (toNat : ℕ), sizeOf { toNat := toNat } = 1 + sizeOf toNat
-- Mathlib.LinearAlgebra.RootSystem.WeylGroup
RootPairing.range_weylGroup_coweightHom : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N),
  ((RootPairing.Equiv.coweightHom P).domRestrict P.weylGroup).range =
    Subgroup.closure (Set.range (MulOpposite.op ∘ P.coreflection))
-- Mathlib.CategoryTheory.Monad.Limits
/-- If `D ⋙ forget T` has a colimit, then `D` has a colimit.  -/
CategoryTheory.Comonad.hasColimit_of_comp_forget_hasColimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  {T : CategoryTheory.Comonad C} (D : CategoryTheory.Functor J T.Coalgebra)
  [CategoryTheory.Limits.HasColimit (D.comp T.forget)], CategoryTheory.Limits.HasColimit D
-- Std.Sync.Channel
/-- Send a value through the channel, returning a task that will resolve once the transmission could be
completed. Note that the task may resolve to `Except.error` if the channel was closed before it
could be completed.
 -/
Std.CloseableChannel.send : {α : Type} → Std.CloseableChannel α → α → BaseIO (Task (Except Std.CloseableChannel.Error Unit))