mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.inv_hom_id_tensor' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {V W X Y Z : C}
  (f : V ⟶ W) [inst_2 : CategoryTheory.IsIso f] (g : X ⟶ Y) (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.inv f) g)
      (CategoryTheory.MonoidalCategoryStruct.tensorHom f h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id W) g)
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id W) h)
-- Mathlib.Algebra.Category.AlgCat.Basic
_private.Mathlib.Algebra.Category.AlgCat.Basic.0.AlgCat.Hom.mk : {R : Type u} → [inst : CommRing R] → {A B : AlgCat R} → (↑A →ₐ[R] ↑B) → A.Hom B
-- Mathlib.GroupTheory.Congruence.Basic
Con.pi.eq_1 : ∀ {ι : Type u_4} {f : ι → Type u_5} [inst : (i : ι) → Mul (f i)] (C : (i : ι) → Con (f i)),
  Con.pi C = { toSetoid := piSetoid, mul' := ⋯ }
-- Mathlib.Order.NonemptyFiniteChains
PartialOrder.NonemptyFiniteChains.mk : {X : Type u} →
  [inst : PartialOrder X] →
    (finset : Finset X) →
      autoParam finset.Nonempty PartialOrder.NonemptyFiniteChains.nonempty._autoParam →
        (∀ (a b : ↥finset), a ≤ b ∨ b ≤ a) → PartialOrder.NonemptyFiniteChains X
-- Mathlib.MeasureTheory.OuterMeasure.OfAddContent
/-- For `m : AddContent C` sigma-sub-additive, finite on `C`, the `OuterMeasure` given by `m`
coincides with `m` on `C`.  -/
MeasureTheory.AddContent.ofFunction_eq : ∀ {α : Type u_1} {C : Set (Set α)} {s : Set α},
  MeasureTheory.IsSetSemiring C →
    ∀ (m : MeasureTheory.AddContent ENNReal C),
      m.IsSigmaSubadditive → (∀ s ∉ C, m s = ⊤) → s ∈ C → (MeasureTheory.OuterMeasure.ofFunction ⇑m ⋯) s = m s
-- Init.Data.List.Sublist
List.Sublist.filter : ∀ {α : Type u_1} (p : α → Bool) {l₁ l₂ : List α}, l₁.Sublist l₂ → (List.filter p l₁).Sublist (List.filter p l₂)
-- Mathlib.SetTheory.Cardinal.NatCard
ENat.card_eq_coe_natCard : ∀ (α : Type u_4) [Finite α], ENat.card α = ↑(Nat.card α)
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.lift_includeLeft_includeRight : ∀ {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A]
  [inst_6 : IsScalarTower R S A] [inst_7 : Semiring B] [inst_8 : Algebra R B],
  Algebra.TensorProduct.lift Algebra.TensorProduct.includeLeft Algebra.TensorProduct.includeRight ⋯ =
    AlgHom.id S (TensorProduct R A B)
-- Mathlib.Analysis.Convex.Cone.InnerDual
/-- Geometric interpretation of **Farkas' lemma**. Also stronger version of the
**Hahn-Banach separation theorem** for proper cones.  -/
ProperCone.hyperplane_separation' : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [CompleteSpace E] {x₀ : E}
  (C : ProperCone ℝ E), x₀ ∉ C → ∃ y, (∀ x ∈ C, 0 ≤ inner ℝ x y) ∧ inner ℝ x₀ y < 0
-- Mathlib.RingTheory.LocalRing.Module
/-- Given a linear map `l : M → N` over a local ring `(R, 𝔪, k)`
with `M` finite and `N` finite free,
`l` is a split injection if and only if `k ⊗ l` is a (split) injection.
 -/
IsLocalRing.split_injective_iff_lTensor_residueField_injective : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] [inst_5 : IsLocalRing R] [Module.Finite R M] [Module.Finite R N]
  [Module.Free R N] (l : M →ₗ[R] N),
  (∃ l', l' ∘ₗ l = LinearMap.id) ↔ Function.Injective ⇑(LinearMap.lTensor (IsLocalRing.ResidueField R) l)
-- Mathlib.FieldTheory.LinearDisjoint
IntermediateField.LinearDisjoint.bot_right : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (A : IntermediateField F E),
  A.LinearDisjoint ↥⊥
-- Mathlib.Algebra.GCDMonoid.IntegrallyClosed
GCDMonoid.toIsIntegrallyClosed : ∀ {R : Type u_1} [inst : CommRing R] [h : IsGCDMonoid R], IsIntegrallyClosed R
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- The bijection between the sets of normalized factors of I and J induced by a ring
isomorphism `f : R/I ≅ A/J`.  -/
IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing A] →
        [inst_2 : IsDedekindDomain A] →
          {I : Ideal R} →
            {J : Ideal A} →
              [inst_3 : IsDedekindDomain R] →
                R ⧸ I ≃+* A ⧸ J →
                  I ≠ ⊥ →
                    J ≠ ⊥ →
                      ↑{L | L ∈ UniqueFactorizationMonoid.normalizedFactors I} ≃
                        ↑{M | M ∈ UniqueFactorizationMonoid.normalizedFactors J}
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.any.eq_1 : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (t : Std.DTreeMap.Raw α β cmp) (p : (a : α) → β a → Bool),
  t.any p = t.inner.any p
-- Mathlib.Algebra.Polynomial.Sequence
/-- No polynomial in the sequence is zero.  -/
Polynomial.Sequence.ne_zero : ∀ {R : Type u_1} [inst : Semiring R] (S : Polynomial.Sequence R) (i : ℕ), ↑S i ≠ 0
-- Batteries.Data.UInt
UInt32.lt_iff_toNat_lt_toNat : ∀ {x y : UInt32}, x < y ↔ x.toNat < y.toNat
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
_private.Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt.0.Lean.Meta.Grind.Arith.Cutsat.toInt'.processNeg : Lean.Expr → Lean.Expr → Lean.Meta.Grind.Arith.Cutsat.ToIntM (Lean.Expr × Lean.Expr)
-- Mathlib.Combinatorics.Additive.FreimanHom
IsMulFreimanIso.comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : CommMonoid α] [inst_1 : CommMonoid β] [inst_2 : CommMonoid γ]
  {A : Set α} {B : Set β} {C : Set γ} {f : α → β} {g : β → γ} {n : ℕ},
  IsMulFreimanIso n B C g → IsMulFreimanIso n A B f → IsMulFreimanIso n A C (g ∘ f)
-- Mathlib.FieldTheory.PrimitiveElement
Field.finite_intermediateField_of_exists_primitive_element : ∀ (F : Type u_1) (E : Type u_2) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [Algebra.IsAlgebraic F E],
  (∃ α, F⟮α⟯ = ⊤) → Finite (IntermediateField F E)
-- Mathlib.Topology.Homotopy.Basic
/-- value of the homotopy at 1  -/
ContinuousMap.Homotopy.map_one_left : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
  (self : f₀.Homotopy f₁) (x : X), self.toFun (1, x) = f₁ x
-- Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
ContinuousAffineMap.toConstProdContinuousLinearMap_snd : ∀ (𝕜 : Type u_1) (V : Type u_3) (W : Type u_4) [inst : SeminormedAddCommGroup V] [inst_1 : SeminormedAddCommGroup W]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedSpace 𝕜 V] [inst_4 : NormedSpace 𝕜 W] (f : V →ᴬ[𝕜] W),
  ((ContinuousAffineMap.toConstProdContinuousLinearMap 𝕜 V W) f).2 = f.contLinear
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyGT.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k : α)
  (x_3 : Std.DTreeMap.Internal.Impl.leaf.Ordered)
  (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.leaf, compare a k = Ordering.gt),
  Std.DTreeMap.Internal.Impl.getKeyGT k Std.DTreeMap.Internal.Impl.leaf x_3 he = ⋯.elim
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.LHom.realize_onTerm : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'}
  [inst_1 : L'.Structure M] (φ : L →ᴸ L') [φ.IsExpansionOn M] (t : L.Term α) (v : α → M),
  FirstOrder.Language.Term.realize v (φ.onTerm t) = FirstOrder.Language.Term.realize v t
-- Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems
/-- A consequence of the special adjoint functor theorem: if `C` is complete, well-powered and
has a small coseparating set, then it is cocomplete.  -/
CategoryTheory.Limits.hasColimits_of_hasLimits_of_isCoseparating : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C]
  [CategoryTheory.WellPowered.{v, v, u} C] {P : CategoryTheory.ObjectProperty C}
  [CategoryTheory.ObjectProperty.Small.{v, v, u} P], P.IsCoseparating → CategoryTheory.Limits.HasColimits C
-- Mathlib.Data.Ordmap.Invariants
Ordnode.findMax'.eq_def : ∀ {α : Type u_1} (x : α) (x_1 : Ordnode α),
  Ordnode.findMax' x x_1 =
    match x, x_1 with
    | x, Ordnode.nil => x
    | x, Ordnode.node size l x_2 r => Ordnode.findMax' x_2 r
-- Init.Data.UInt.Lemmas
USize.toUInt32_ofNatLT : ∀ {n : ℕ} (hn : n < USize.size), (USize.ofNatLT n hn).toUInt32 = UInt32.ofNat n
-- Init.Data.List.Count
List.count_eq_length : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {l : List α}, List.count a l = l.length ↔ ∀ b ∈ l, a = b
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
circleMap_eq_center_iff : ∀ {c : ℂ} {R θ : ℝ}, circleMap c R θ = c ↔ R = 0
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.induction_reflect : ∀ {ι : 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} {b : P.Base}
  [CharZero R] [Finite ι] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] (i : ι) {p : ι → Prop},
  (∀ (i : ι), p i → p ((P.reflectionPerm i) i)) →
    (∀ i ∈ b.support, p i) → (∀ (i j : ι), p i → j ∈ b.support → p ((P.reflectionPerm j) i)) → p i
-- Mathlib.RingTheory.Ideal.Norm.RelNorm
/-- `Ideal.spanNorm R (I : Ideal S)` is the ideal generated by mapping `Algebra.intNorm R S`
over `I`.

See also `Ideal.relNorm`.
 -/
Ideal.spanNorm : (R : Type u_1) →
  [inst : CommRing R] →
    [IsDomain R] →
      {S : Type u_3} →
        [inst_2 : CommRing S] →
          [IsDomain S] →
            [IsIntegrallyClosed R] →
              [IsIntegrallyClosed S] →
                [inst_6 : Algebra R S] → [Module.Finite R S] → [Module.IsTorsionFree R S] → Ideal S → Ideal R
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
IsometricContinuousFunctionalCalculus.nnnorm_spectrum_le : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [inst : RCLike 𝕜] [inst_1 : NormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedAlgebra 𝕜 A] [IsometricContinuousFunctionalCalculus 𝕜 A p] (a : A) ⦃x : 𝕜⦄,
  x ∈ spectrum 𝕜 a → autoParam (p a) IsometricContinuousFunctionalCalculus.nnnorm_spectrum_le._auto_1 → ‖x‖₊ ≤ ‖a‖₊
-- Mathlib.Topology.EMetricSpace.Defs
WeakPseudoEMetricSpace.toEDist : {α : Type u} → {τ : TopologicalSpace α} → [self : WeakPseudoEMetricSpace α] → EDist α
-- Mathlib.Order.Interval.Basic
instOrderBotInterval : (α : Type u_1) → [inst : LE α] → OrderBot (Interval α)
-- Mathlib.Tactic.CategoryTheory.Coherence
Mathlib.Tactic.Coherence.LiftObj.of : {C : Type u} → (X : C) → Mathlib.Tactic.Coherence.LiftObj X
-- Std.Data.Iterators.Combinators.Monadic.TakeWhile
/-- *Note: This is a very general combinator that requires an advanced understanding of monads,
dependent types and termination proofs. The variants `takeWhile` and `takeWhileM` are easier to use
and sufficient for most use cases.*

Given an iterator `it` and a monadic predicate `P`, `it.takeWhileWithPostcondition P` is an iterator
that emits the values emitted by `it` until one of those values is rejected by `P`.
If some emitted value is rejected by `P`, the value is dropped and the iterator terminates.

`P` is expected to return `PostconditionT m (ULift Bool)`. The `PostconditionT` transformer allows
the caller to intrinsically prove properties about `P`'s return value in the monad `m`, enabling
termination proofs depending on the specific behavior of `P`.

**Marble diagram (ignoring monadic effects):**

Assuming that the predicate `P` accepts `a` and `b` but rejects `c`:

```text
it                                ---a----b---c--d-e--⊥
it.takeWhileWithPostcondition P   ---a----b---⊥

it                                ---a----⊥
it.takeWhileWithPostcondition P   ---a----⊥
```

**Termination properties:**

* `Finite` instance: only if `it` is finite
* `Productive` instance: only if `it` is productive

Depending on `P`, it is possible that `it.takeWhileWithPostcondition P` is finite (or productive)
although `it` is not. In this case, the `Finite` (or `Productive`) instance needs to be proved
manually.

**Performance:**

This combinator calls `P` on each output of `it` until the predicate evaluates to false. Then
it terminates.
 -/
Std.IterM.takeWhileWithPostcondition : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} → (P : β → Std.Iterators.PostconditionT m (ULift.{w, 0} Bool)) → Std.IterM m β → Std.IterM m β
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremConstraint.genLt.sizeOf_spec : ∀ (n : ℕ), sizeOf (Lean.Meta.Grind.EMatchTheoremConstraint.genLt n) = 1 + sizeOf n
-- Init.Data.SInt.Basic
/-- Converts a 32-bit signed integer to a natural number, mapping all negative numbers to `0`.

Use `Int32.toBitVec` to obtain the two's complement representation.
 -/
Int32.toNatClampNeg : Int32 → ℕ
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.Decidable.isLongestMatchAt_of_get : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice} {pos : s.Pos} {h : pos ≠ s.endPos},
  p (pos.get h) → String.Slice.Pattern.Model.IsLongestMatchAt p pos (pos.next h)
-- Lean.Language.Basic
Lean.Language.SnapshotTree.brecOn_4.go : {motive_1 : Lean.Language.SnapshotTree → Sort u} →
  {motive_2 : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree) → Sort u} →
    {motive_3 : List (Lean.Language.SnapshotTask Lean.Language.SnapshotTree) → Sort u} →
      {motive_4 : Lean.Language.SnapshotTask Lean.Language.SnapshotTree → Sort u} →
        {motive_5 : Task Lean.Language.SnapshotTree → Sort u} →
          (t : Task Lean.Language.SnapshotTree) →
            ((t : Lean.Language.SnapshotTree) → t.below → motive_1 t) →
              ((t : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)) →
                  Lean.Language.SnapshotTree.below_1 t → motive_2 t) →
                ((t : List (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)) →
                    Lean.Language.SnapshotTree.below_2 t → motive_3 t) →
                  ((t : Lean.Language.SnapshotTask Lean.Language.SnapshotTree) →
                      Lean.Language.SnapshotTree.below_3 t → motive_4 t) →
                    ((t : Task Lean.Language.SnapshotTree) → Lean.Language.SnapshotTree.below_4 t → motive_5 t) →
                      motive_5 t ×' Lean.Language.SnapshotTree.below_4 t
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace : AlgebraicGeometry.LocallyRingedSpace → AlgebraicGeometry.SheafedSpace CommRingCat
-- Mathlib.Algebra.Polynomial.Eval.Degree
Polynomial.mapEquiv_symm_apply : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (e : R ≃+* S) (a : Polynomial S),
  (Polynomial.mapEquiv e).symm a = Polynomial.map (↑e.symm) a
-- Mathlib.Data.Nat.Cast.Order.Ring
Nat.cast_min : ∀ {α : Type u_3} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (m n : ℕ), ↑(min m n) = min ↑m ↑n
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get_diff : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [inst : Std.TransCmp cmp] (h₁ : t₁.WF)
  (h₂ : t₂.WF) {k : α} {h_mem : k ∈ t₁ \ t₂}, (t₁ \ t₂).get k h_mem = t₁.get k ⋯
-- Mathlib.CategoryTheory.Shift.ShiftSequence
CategoryTheory.Functor.shiftIso_add_inv_app : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A) {M : Type u_4} [inst_2 : AddMonoid M]
  [inst_3 : CategoryTheory.HasShift C M] [inst_4 : F.ShiftSequence M] (n m a a' a'' : M) (ha' : n + a = a')
  (ha'' : m + a' = a'') (X : C),
  (F.shiftIso (m + n) a a'' ⋯).inv.app X =
    CategoryTheory.CategoryStruct.comp ((F.shiftIso m a' a'' ha'').inv.app X)
      (CategoryTheory.CategoryStruct.comp ((F.shiftIso n a a' ha').inv.app ((CategoryTheory.shiftFunctor C m).obj X))
        ((F.shift a).map ((CategoryTheory.shiftFunctorAdd C m n).inv.app X)))
-- Mathlib.RingTheory.Valuation.ValuationRing
ValuationRing.iff_isInteger_or_isInteger : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] (K : Type u_2) [inst_2 : Field K] [inst_3 : Algebra R K]
  [IsFractionRing R K], ValuationRing R ↔ ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
-- Std.Time.Zoned.Database.TzIf
/-- The array of local time type structures.
 -/
Std.Time.TimeZone.TZif.TZifV1.localTimeTypes : Std.Time.TimeZone.TZif.TZifV1 → Array Std.Time.TimeZone.TZif.LocalTimeType
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.whiskering_obj_obj_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (D : Type u_1) [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (H : CategoryTheory.Functor C D) (F : CategoryTheory.Functor SimplexCategory C) (X : SimplexCategory),
  (((CategoryTheory.CosimplicialObject.whiskering C D).obj H).obj F).obj X = H.obj (F.obj X)
-- Mathlib.Data.Nat.Digits.Defs
_private.Mathlib.Data.Nat.Digits.Defs.0.Nat.digits.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (b : ℕ) → motive b.succ.succ),
  (match 1 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | b.succ.succ => h_3 b) =
    h_2 ()
-- Mathlib.Algebra.Group.Basic
zero_sub_add_zero_sub : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (a b : α), 0 - a + (0 - b) = 0 - (a + b)
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticForm.toMatrix'.eq_1 : ∀ {R : Type u_3} {n : Type w} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R] [inst_3 : Invertible 2]
  (Q : QuadraticForm R (n → R)), Q.toMatrix' = (LinearMap.toMatrix₂' R) (QuadraticMap.associated Q)
-- Mathlib.Order.CompleteLattice.Basic
iInf₂_mono' : ∀ {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {κ : ι → Sort u_6} {κ' : ι' → Sort u_7} [inst : CompleteLattice α]
  {f : (i : ι) → κ i → α} {g : (i' : ι') → κ' i' → α},
  (∀ (i : ι) (j : κ i), ∃ i' j', g i' j' ≤ f i j) → ⨅ i, ⨅ j, g i j ≤ ⨅ i, ⨅ j, f i j
-- Mathlib.CategoryTheory.Category.Pairwise
CategoryTheory.Pairwise.Hom.left : {ι : Type v} → (i j : ι) → (CategoryTheory.Pairwise.pair i j).Hom (CategoryTheory.Pairwise.single i)
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.empty_vadd : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] (t : Finset β), ∅ +ᵥ t = ∅
-- Mathlib.Tactic.DuplicateDecls
Mathlib.Tactic.DuplicateDecls.Target.theorems.sizeOf_spec : sizeOf Mathlib.Tactic.DuplicateDecls.Target.theorems = 1
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile
Std.IterM.takeWhileM.eq_1 : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Monad m] [inst_1 : MonadAttach m]
  (P : β → m (ULift.{w, 0} Bool)) (it : Std.IterM m β),
  Std.IterM.takeWhileM P it = Std.IterM.takeWhileWithPostcondition (Std.Iterators.PostconditionT.attachLift ∘ P) it
-- Mathlib.Probability.HasLaw
ProbabilityTheory.IndepFun.hasLaw_fun_add : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {M : Type u_3} [inst : AddMonoid M]
  {mM : MeasurableSpace M} [MeasurableAdd₂ M] {μ ν : MeasureTheory.Measure M} [MeasureTheory.SigmaFinite μ]
  [MeasureTheory.SigmaFinite ν] {X Y : Ω → M},
  ProbabilityTheory.HasLaw X μ P →
    ProbabilityTheory.HasLaw Y ν P →
      ProbabilityTheory.IndepFun X Y P → ProbabilityTheory.HasLaw (fun ω => X ω + Y ω) (μ.conv ν) P
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.image_eq_preimage_symm : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_4} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {G : Type u_7} [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M] {N : Type u_11}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} (h : Diffeomorph I J M N n) (s : Set M),
  ⇑h '' s = ⇑h.symm ⁻¹' s
-- Mathlib.Analysis.Calculus.Deriv.Pow
HasDerivAt.fun_pow' : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕜 𝔸]
  {f : 𝕜 → 𝔸} {f' : 𝔸} {x : 𝕜},
  HasDerivAt f f' x →
    ∀ (n : ℕ), HasDerivAt (fun x => f x ^ n) (∑ i ∈ Finset.range n, f x ^ (n.pred - i) * f' * f x ^ i) x
-- Mathlib.Algebra.Colimit.Module
/-- The congruence relation to quotient the direct sum by to obtain the direct limit.  -/
Module.DirectLimit.moduleCon : {R : Type u_1} →
  [inst : Semiring R] →
    {ι : Type u_2} →
      [inst_1 : Preorder ι] →
        {G : ι → Type u_3} →
          [inst_2 : (i : ι) → AddCommMonoid (G i)] →
            [inst_3 : (i : ι) → Module R (G i)] →
              ((i j : ι) → i ≤ j → G i →ₗ[R] G j) → [DecidableEq ι] → ModuleCon R (DirectSum ι G)
-- Mathlib.CategoryTheory.Adjunction.FullyFaithful
CategoryTheory.Adjunction.whiskerRight_counit_iso_of_L_fully_faithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) [L.Full] [L.Faithful],
  CategoryTheory.IsIso (CategoryTheory.Functor.whiskerRight h.counit R)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.toList_toArray : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α],
  m.WF → m.toArray.toList = m.toList
-- Mathlib.Analysis.Normed.Field.Basic
nnnorm_div : ∀ {α : Type u_2} [inst : NormedDivisionRing α] (a b : α), ‖a / b‖₊ = ‖a‖₊ / ‖b‖₊
-- Mathlib.CategoryTheory.Localization.Construction
CategoryTheory.Localization.Construction.instQuiverLocQuiver : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    (W : CategoryTheory.MorphismProperty C) → Quiver (CategoryTheory.Localization.Construction.LocQuiver W)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
CliffordAlgebra.changeForm.associated_neg_proof : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} [inst_3 : Invertible 2], (QuadraticMap.associated (-Q)).toQuadraticMap = 0 - Q
-- Init.Data.Char.Ordinal
_private.Init.Data.Char.Ordinal.0.Char.ordinal.eq_1 : ∀ (c : Char), c.ordinal = if h : c.val < 55296 then ⟨c.val.toNat, ⋯⟩ else ⟨c.val.toNat - Char.numSurrogates, ⋯⟩
-- Mathlib.CategoryTheory.Limits.Cones
/-- Forget the cocone structure and obtain just the cocone point.  -/
CategoryTheory.Limits.Cocone.forget : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        (F : CategoryTheory.Functor J C) → CategoryTheory.Functor (CategoryTheory.Limits.Cocone F) C