mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.LawfulBackwardPatternModel.mk : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat]
  [inst_1 : String.Slice.Pattern.Model.PatternModel pat]
  [toLawfulBackwardPattern : String.Slice.Pattern.LawfulBackwardPattern pat],
  (∀ {s : String.Slice} (pos : s.Pos),
      String.Slice.Pattern.BackwardPattern.skipSuffix? pat s = some pos ↔
        String.Slice.Pattern.Model.IsLongestRevMatch pat pos) →
    String.Slice.Pattern.Model.LawfulBackwardPatternModel pat
-- Mathlib.Algebra.Lie.Cochain
LieModule.Cohomology.twoCochain_skew : ∀ {R : Type u_1} [inst : CommRing R] {L : Type u_2} [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {M : Type u_3}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (a : ↥(LieModule.Cohomology.twoCochain R L M)) (x y : L),
  -(a x) y = (a y) x
-- ProofWidgets.Data.Html
ProofWidgets.Html.brecOn_2.go : {motive_1 : ProofWidgets.Html → Sort u} →
  {motive_2 : Array ProofWidgets.Html → Sort u} →
    {motive_3 : List ProofWidgets.Html → Sort u} →
      (t : List ProofWidgets.Html) →
        ((t : ProofWidgets.Html) → t.below → motive_1 t) →
          ((t : Array ProofWidgets.Html) → ProofWidgets.Html.below_1 t → motive_2 t) →
            ((t : List ProofWidgets.Html) → ProofWidgets.Html.below_2 t → motive_3 t) →
              motive_3 t ×' ProofWidgets.Html.below_2 t
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toArray_rco_eq_zero : ∀ {m n i : ℕ}, n ≤ i + m → (m...n).toArray[i]! = 0
-- Mathlib.Data.Ordmap.Ordnode
/-- O(log n). Get an initial segment of the set that satisfies the predicate `p`.
`p` is required to be antitone, that is, `x < y → p y → p x`.

```
takeWhile (fun x ↦ x < 4) {1, 2, 3, 4, 5} = {1, 2, 3}
takeWhile (fun x ↦ x > 4) {1, 2, 3, 4, 5} = precondition violation
```  -/
Ordnode.takeWhile : {α : Type u_1} → (p : α → Prop) → [DecidablePred p] → Ordnode α → Ordnode α
-- Mathlib.Data.Rat.Lemmas
Rat.mul_den : ∀ (q₁ q₂ : ℚ), (q₁ * q₂).den = q₁.den * q₂.den / (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)
-- Lean.EnvExtension
/-- Modify the state of the given extension in the given environment by applying the given function. This change is *not* persisted across files.  -/
Lean.SimplePersistentEnvExtension.modifyState : {α σ : Type} → Lean.SimplePersistentEnvExtension α σ → Lean.Environment → (σ → σ) → Lean.Environment
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.size_le_size_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  t.size ≤ (t.insert k).size
-- Mathlib.Control.Applicative
Functor.Comp.instLawfulApplicativeComp : ∀ {F : Type u → Type w} {G : Type v → Type u} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative F]
  [LawfulApplicative G], LawfulApplicative (Functor.Comp F G)
-- Mathlib.Order.Hom.CompleteLattice
CompleteLatticeHom.setPreimage_id : ∀ {α : Type u_2}, CompleteLatticeHom.setPreimage id = CompleteLatticeHom.id (Set α)
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.uncurry_pre_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {A B : C} (X : C)
  {Y : C} [inst_2 : CategoryTheory.Closed A] [inst_3 : CategoryTheory.Closed B] (f : Y ⟶ A ⟹ X) (g : B ⟶ A),
  CategoryTheory.MonoidalClosed.uncurry
      (CategoryTheory.CategoryStruct.comp f ((CategoryTheory.MonoidalClosed.pre g).app X)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight g Y)
      (CategoryTheory.MonoidalClosed.uncurry f)
-- Mathlib.Topology.Connected.PathConnected
/-- The product of two path-connected sets is path-connected.  -/
IsPathConnected.prod : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {t : Set Y},
  IsPathConnected s → IsPathConnected t → IsPathConnected (s ×ˢ t)
-- Mathlib.Order.Basic
/-- Given a relation `R` on `β` and a function `f : α → β`, the preimage relation on `α` is defined
by `x ≤ y ↔ f x ≤ f y`. It is the unique relation on `α` making `f` a `RelEmbedding` (assuming `f`
is injective).  -/
«term_⁻¹'o_» : Lean.TrailingParserDescr
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.δ_comp_σ_succ' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ}
  {j : Fin (n + 2)} {i : Fin (n + 1)},
  j = i.succ →
    CategoryTheory.CategoryStruct.comp (X.δ j) (X.σ i) = CategoryTheory.CategoryStruct.id (X.obj { len := n })
-- Mathlib.Analysis.Fourier.LpSpace
MeasureTheory.Lp.instFourierPair : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [inst_2 : BorelSpace E]
  [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace ℂ F] [inst_5 : CompleteSpace F]
  [inst_6 : InnerProductSpace ℝ E] [inst_7 : FiniteDimensional ℝ E],
  FourierPair ↥(MeasureTheory.Lp F 2 MeasureTheory.volume) ↥(MeasureTheory.Lp F 2 MeasureTheory.volume)
-- Mathlib.Analysis.Calculus.Implicit
ImplicitFunctionData.map_pt_mem_toOpenPartialHomeomorph_target : ∀ {𝕜 : 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),
  (φ.leftFun φ.pt, φ.rightFun φ.pt) ∈ φ.toOpenPartialHomeomorph.target
-- Mathlib.Tactic.Linter.EmptyLine
/-- The `SyntaxNodeKind`s where the `EmptyLine` linter is not active  -/
Mathlib.Linter.EmptyLine.AllowEmptyLines : Std.HashSet Lean.SyntaxNodeKind
-- Init.Data.Order.MinMaxOn
_private.Init.Data.Order.MinMaxOn.0.minOn.eq_1 : ∀ {β : Type u_1} {α : Sort u_2} [inst : LE β] [inst_1 : DecidableLE β] (f : α → β) (x y : α),
  minOn f x y = if f x ≤ f y then x else y
-- Mathlib.Order.Disjoint
IsCompl.le_right_iff : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : BoundedOrder α] {x y z : α}, IsCompl x y → (z ≤ y ↔ Disjoint z x)
-- Mathlib.MeasureTheory.Measure.Hausdorff
/-- **Carathéodory's theorem**. If `m` is a metric outer measure, then every Borel measurable set
`t` is Carathéodory measurable: for any (not necessarily measurable) set `s` we have
`μ (s ∩ t) + μ (s \ t) = μ s`.  -/
MeasureTheory.OuterMeasure.IsMetric.borel_le_caratheodory : ∀ {X : Type u_2} [inst : EMetricSpace X] {μ : MeasureTheory.OuterMeasure X}, μ.IsMetric → borel X ≤ μ.caratheodory
-- Std.Data.Iterators.Lemmas.Combinators.DropWhile
Std.Iter.Intermediate.dropWhile_eq_dropWhile_toIterM : ∀ {α β : Type u_1} [Std.Iterator α Id β] {P : β → Bool} {it : Std.Iter β} {dropping : Bool},
  Std.Iter.Intermediate.dropWhile P dropping it = (Std.IterM.Intermediate.dropWhile P dropping it.toIterM).toIter
-- Mathlib.Topology.MetricSpace.Thickening
/-- The (open) `δ`-thickening `Metric.thickening δ E` of a subset `E` in a metric space equals the
union of balls of radius `δ` centered at points of `E`.  -/
Metric.thickening_eq_biUnion_ball : ∀ {X : Type u} [inst : PseudoMetricSpace X] {δ : ℝ} {E : Set X}, Metric.thickening δ E = ⋃ x ∈ E, Metric.ball x δ
-- Mathlib.Order.SupClosed
InfClosed.finsetInf'_mem : ∀ {α : Type u_3} [inst : SemilatticeInf α] {ι : Type u_5} {f : ι → α} {s : Set α} {t : Finset ι},
  InfClosed s → ∀ (ht : t.Nonempty), (∀ i ∈ t, f i ∈ s) → t.inf' ht f ∈ s
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
CategoryTheory.OplaxFunctor.PseudoCore.mk : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F : CategoryTheory.OplaxFunctor B C} →
          (mapIdIso :
              (a : B) → F.map (CategoryTheory.CategoryStruct.id a) ≅ CategoryTheory.CategoryStruct.id (F.obj a)) →
            (mapCompIso :
                {a b c : B} →
                  (f : a ⟶ b) →
                    (g : b ⟶ c) →
                      F.map (CategoryTheory.CategoryStruct.comp f g) ≅
                        CategoryTheory.CategoryStruct.comp (F.map f) (F.map g)) →
              autoParam (∀ {a : B}, (mapIdIso a).hom = F.mapId a)
                  CategoryTheory.OplaxFunctor.PseudoCore.mapIdIso_hom._autoParam →
                autoParam (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), (mapCompIso f g).hom = F.mapComp f g)
                    CategoryTheory.OplaxFunctor.PseudoCore.mapCompIso_hom._autoParam →
                  F.PseudoCore
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_maxKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → t.isEmpty = false → t.getKey? t.maxKey! = some t.maxKey!
-- Mathlib.Analysis.Seminorm
Seminorm.smul_inf : ∀ {R : Type u_1} {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : SMul R ℝ] [inst_4 : SMul R NNReal] [inst_5 : IsScalarTower R NNReal ℝ] (r : R) (p q : Seminorm 𝕜 E),
  r • (p ⊓ q) = r • p ⊓ r • q
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToTerm.declToTerm : Lean.Syntax → Lean.Syntax → Lean.Elab.Term.Do.ToTerm.M Lean.Syntax
-- Mathlib.Topology.Compactness.DeltaGeneratedSpace
/-- The topology coinduced by all maps from ℝⁿ into a space.  -/
TopologicalSpace.deltaGenerated : (X : Type u_1) → [TopologicalSpace X] → TopologicalSpace X
-- Mathlib.Data.ENat.Lattice
/-- **Alias** of `ENat.iSup_natCast_ne_top`. -/
ENat.iSup_coe_ne_top : ∀ {ι : Sort u_1} {f : ι → ℕ}, ⨆ i, ↑(f i) ≠ ⊤ ↔ BddAbove (Set.range f)
-- Mathlib.Topology.Order.Category.FrameAdjunction
Locale.localePointOfSpacePoint_toFun : ∀ (X : Type u_1) [inst : TopologicalSpace X] (x : X) (x_1 : TopologicalSpace.Opens X),
  (Locale.localePointOfSpacePoint X x) x_1 = (x ∈ x_1)
-- Mathlib.NumberTheory.RamificationInertia.Inertia
Ideal.inertiaDeg'_comap_eq : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  {S₁ : Type u_1} [inst_3 : CommRing S₁] [inst_4 : Algebra R S₁] (e : S ≃ₐ[R] S₁) (P : Ideal S₁),
  p.inertiaDeg' (Ideal.comap e P) = p.inertiaDeg' P
-- Mathlib.Algebra.Lie.Solvable
LieIdeal.derivedSeries_map_le : ∀ {R : Type u} {L : Type v} {L' : Type w₁} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing L'] [inst_4 : LieAlgebra R L'] {f : L' →ₗ⁅R⁆ L} (k : ℕ),
  LieIdeal.map f (LieAlgebra.derivedSeries R L' k) ≤ LieAlgebra.derivedSeries R L k
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintLabel.name.inj : ∀ {n n_1 : String}, Lean.Lsp.InlayHintLabel.name n = Lean.Lsp.InlayHintLabel.name n_1 → n = n_1
-- Mathlib.Algebra.Lie.BaseChange
LieSubmodule.baseChange_top : ∀ (R : Type u_1) (A : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : LieAlgebra R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M]
  [inst_6 : LieModule R L M] [inst_7 : CommRing A] [inst_8 : Algebra R A], LieSubmodule.baseChange A ⊤ = ⊤
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprodComparison_inl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{w, u₂} D]
  (F : CategoryTheory.Functor C D) {A B : C} [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct A B]
  [inst_3 : CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)],
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.Limits.coprodComparison F A B) =
    F.map CategoryTheory.Limits.coprod.inl
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
CategoryTheory.Bicategory.InducedBicategory.categoryStruct_id_hom : ∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory C] {F : B → C}
  (X : CategoryTheory.Bicategory.InducedBicategory C F),
  (CategoryTheory.CategoryStruct.id X).hom = CategoryTheory.CategoryStruct.id (F X)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point.0.WeierstrassCurve.Jacobian.nonsingular_neg_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F},
  W.Nonsingular P → P 2 ≠ 0 → W.Nonsingular ![P 0 / P 2 ^ 2, W.toAffine.negY (P 0 / P 2 ^ 2) (P 1 / P 2 ^ 3), 1]
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- The cycles in the opposite category of the opposite of a short complex identifies
to the opcycles of this short complex.  -/
CategoryTheory.ShortComplex.cyclesOpIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) → [inst_2 : S.HasRightHomology] → S.op.cycles ≅ Opposite.op S.opcycles
-- Mathlib.Data.Set.Card.Arithmetic
Set.Finite.encard_biUnion : ∀ {α : Type u_1} {ι : Type u_2} {t : Set ι},
  t.Finite → ∀ {s : ι → Set α}, t.PairwiseDisjoint s → (⋃ i ∈ t, s i).encard = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard
-- Mathlib.Tactic.Peel
Mathlib.Tactic.Peel.and_imp_left_of_imp_imp : ∀ {p q r : Prop}, (r → p → q) → r ∧ p → r ∧ q
-- Lean.Data.Name
/-- Check that a string begins with the given prefix, and then is only digits/'_'.  -/
_private.Lean.Data.Name.0.Lean.Name.isInternalDetail.matchPrefix : String → String → Bool
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Mul
Std.Tactic.BVDecide.BVExpr.bitblast.denote_blastMul : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (lhs rhs : BitVec w)
  (assign : α → Bool) (input : aig.BinaryRefVec w),
  (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx) →
    (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx) →
      ∀ (idx : ℕ) (hidx : idx < w),
        ⟦assign,
            { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastMul aig input).aig,
              ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastMul aig input).vec.get idx hidx }⟧ =
          (lhs * rhs).getLsbD idx
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
/-- The restriction of `Proj π J` to a subset, mapping to its image.  -/
Profinite.NobelingProof.ProjRestrict : {I : Type u} →
  (C : Set (I → Bool)) → (J : I → Prop) → [inst : (i : I) → Decidable (J i)] → ↑C → ↑(Profinite.NobelingProof.π C J)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey?_modify : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α],
  (↑m).WF →
    ∀ {k k' : α} {f : β k → β k},
      (m.modify k f).getKey? k' =
        if (k == k') = true then if m.contains k = true then some k else none else m.getKey? k'
-- Mathlib.Data.Matrix.Basic
/-- Extracting entries from a matrix as a linear map. Note this cannot be upgraded to an algebra
homomorphism, as it does not respect multiplication.
 -/
Matrix.entryLinearMap : {m : Type u_2} →
  {n : Type u_3} →
    (R : Type u_7) →
      (α : Type u_11) →
        [inst : Semiring R] → [inst_1 : AddCommMonoid α] → [inst_2 : Module R α] → m → n → Matrix m n α →ₗ[R] α
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.liftRel_flatten : ∀ {α : Type u} {β : Type v} {R : α → β → Prop} {c1 : Computation (Stream'.WSeq α)} {c2 : Computation (Stream'.WSeq β)},
  Computation.LiftRel (Stream'.WSeq.LiftRel R) c1 c2 →
    Stream'.WSeq.LiftRel R (Stream'.WSeq.flatten c1) (Stream'.WSeq.flatten c2)
-- Lean.Meta.SynthInstance
/-- Create a new answer after `cNode` resolved all subgoals.
That is, `cNode.subgoals == []`.
And then, store it in the tabled entries map, and wakeup waiters.  -/
Lean.Meta.SynthInstance.addAnswer : Lean.Meta.SynthInstance.ConsumerNode → Lean.Meta.SynthInstance.SynthM Unit
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.node.inj : ∀ {α : Type u} {c : RBTree.RBColor} {l : RBTree.RBNode α} {v : α} {r : RBTree.RBNode α} {c_1 : RBTree.RBColor}
  {l_1 : RBTree.RBNode α} {v_1 : α} {r_1 : RBTree.RBNode α},
  RBTree.RBNode.node c l v r = RBTree.RBNode.node c_1 l_1 v_1 r_1 → c = c_1 ∧ l = l_1 ∧ v = v_1 ∧ r = r_1
-- Mathlib.Data.FunLike.Module
/-- A `FunLike` type with scalar multiplication that satisfies `(m • f) x = m • f x` and
`0 x = 0`, `(f + g) x = f x + g x` is a `DistribSMul` if `β` is a `DistribSMul`.  -/
FunLike.distribSMul : {M : Type u_1} →
  {F : Type u_3} →
    {α : Type u_4} →
      {β : Type u_5} →
        [i : FunLike F α β] →
          [inst : AddZeroClass β] →
            [inst_1 : AddZeroClass F] →
              [inst_2 : DistribSMul M β] →
                [inst_3 : SMul M F] → [IsZeroApply F α β] → [IsAddApply F α β] → [IsSMulApply M F α β] → DistribSMul M F
-- Lean.Parser.Types
Lean.Parser.ParserCache.mk : Lean.Parser.TokenCacheEntry →
  Std.HashMap Lean.Parser.ParserCacheKey Lean.Parser.ParserCacheEntry → Lean.Parser.ParserCache
-- Mathlib.CategoryTheory.Abelian.LeftDerived
CategoryTheory.Functor.leftDerivedZeroIsoSelf_hom_inv_id_app : ∀ {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 : CategoryTheory.Functor C D) [inst_5 : F.Additive]
  [inst_6 : CategoryTheory.Limits.PreservesFiniteColimits F] (X : C),
  CategoryTheory.CategoryStruct.comp (F.fromLeftDerivedZero.app X) (F.leftDerivedZeroIsoSelf.inv.app X) =
    CategoryTheory.CategoryStruct.id ((F.leftDerived 0).obj X)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- Every multicofork is isomorphic to one of the form `Multicofork.ofπ`.  -/
CategoryTheory.Limits.Multicofork.isoOfπ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MultispanShape} →
      {I : CategoryTheory.Limits.MultispanIndex J C} →
        (t : CategoryTheory.Limits.Multicofork I) → t ≅ CategoryTheory.Limits.Multicofork.ofπ I t.pt t.π ⋯
-- Mathlib.Order.BourbakiWitt
/-- If a chain is a subset of an admissible set, its `cSup` is a member of the admissible set  -/
ChainCompletePartialOrder.IsAdmissible.cSup_mem : ∀ {α : Type u_1} [inst : ChainCompletePartialOrder α] {x : α} {f : α → α} {s : Set α},
  ChainCompletePartialOrder.IsAdmissible x f s → ∀ (c : NonemptyChain α), ↑c ⊆ s → ChainCompletePartialOrder.cSup c ∈ s
-- Mathlib.Order.Interval.Set.OrdConnectedComponent
Set.ordSeparatingSet.eq_1 : ∀ {α : Type u_1} [inst : LinearOrder α] (s t : Set α),
  s.ordSeparatingSet t = (⋃ x ∈ s, tᶜ.ordConnectedComponent x) ∩ ⋃ x ∈ t, sᶜ.ordConnectedComponent x
-- Mathlib.Analysis.Normed.Group.Defs
/-- Construct a seminormed group from a seminorm, i.e., registering the pseudodistance
and the pseudometric space structure from the seminorm properties. Note that in most cases this
instance creates bad definitional equalities (e.g., it does not take into account a possibly
existing `UniformSpace` instance on `E`).  -/
AddGroupSeminorm.toSeminormedAddGroup : {E : Type u_5} → [inst : AddGroup E] → AddGroupSeminorm E → SeminormedAddGroup E
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Final.colimitIso.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : F.Final] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  (G : CategoryTheory.Functor D E) [inst_4 : CategoryTheory.Limits.HasColimit G],
  CategoryTheory.Functor.Final.colimitIso F G = CategoryTheory.asIso (CategoryTheory.Limits.colimit.pre G F)
-- Init.Data.Nat.Basic
Nat.add_one_lt_add_one_iff : ∀ {a b : ℕ}, a + 1 < b + 1 ↔ a < b
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
LinearIsometryEquiv.symm_lTensor : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] (f : F ≃ₗᵢ[𝕜] G),
  (LinearIsometryEquiv.lTensor E f).symm = LinearIsometryEquiv.lTensor E f.symm
-- Mathlib.Algebra.Algebra.Equiv
MulSemiringAction.toAlgEquiv_injective : ∀ {G : Type u_2} (R : Type u_3) (A : Type u_4) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Group G] [inst_4 : MulSemiringAction G A] [inst_5 : SMulCommClass G R A] [FaithfulSMul G A],
  Function.Injective (MulSemiringAction.toAlgEquiv R A)
-- Mathlib.Analysis.Meromorphic.Order
/-- The meromorphic order of the derivative is one less than the order of the original function.
This however is not true if the characteristic of the domain field divides the original order,
where the order of the derivative can rise to a larger integer.  -/
meromorphicOrderAt_deriv_eq_sub_one : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [CompleteSpace E] {f : 𝕜 → E} {x : 𝕜} {n : ℤ},
  ↑n ≠ 0 → meromorphicOrderAt f x = ↑n → meromorphicOrderAt (deriv f) x = ↑(n - 1)
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.ofHom_sum : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] {ι : Type u'} {M N : Type v'}
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module k M] [inst_5 : Module k N]
  {σ : Representation k G M} {ρ : Representation k G N} (f : ι → σ.IntertwiningMap ρ) (s : Finset ι),
  Rep.ofHom (∑ i ∈ s, f i) = ∑ i ∈ s, Rep.ofHom (f i)
-- Mathlib.Algebra.Notation.Support
Function.mulSupport.eq_1 : ∀ {ι : Type u_1} {M : Type u_3} [inst : One M] (f : ι → M), Function.mulSupport f = {x | f x ≠ 1}
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
/-- The right homotopy that is deduced from a left homotopy in the opposite category.  -/
HomotopicalAlgebra.Precylinder.LeftHomotopy.unop : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : Cᵒᵖ} →
      {P : HomotopicalAlgebra.Precylinder X} → {f g : X ⟶ Y} → P.LeftHomotopy f g → P.unop.RightHomotopy f.unop g.unop
-- Mathlib.Topology.NhdsWithin
nhdsWithin_inter_of_mem : ∀ {α : Type u_1} [inst : TopologicalSpace α] {a : α} {s t : Set α},
  s ∈ nhdsWithin a t → nhdsWithin a (s ∩ t) = nhdsWithin a t
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
RootPairing.RootPositiveForm.mk.injEq : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing S]
  [inst_1 : LinearOrder S] [inst_2 : CommRing R] [inst_3 : Algebra S R] [inst_4 : AddCommGroup M] [inst_5 : Module R M]
  [inst_6 : AddCommGroup N] [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsValuedIn S]
  (form : LinearMap.BilinForm R M) (symm : LinearMap.IsSymm form)
  (isOrthogonal_reflection : ∀ (i : ι), LinearMap.IsOrthogonal form ⇑(P.reflection i))
  (exists_eq : ∀ (i j : ι), ∃ s, (algebraMap S R) s = (form (P.root i)) (P.root j))
  (exists_pos_eq : ∀ (i : ι), ∃ s > 0, (algebraMap S R) s = (form (P.root i)) (P.root i))
  (form_1 : LinearMap.BilinForm R M) (symm_1 : LinearMap.IsSymm form_1)
  (isOrthogonal_reflection_1 : ∀ (i : ι), LinearMap.IsOrthogonal form_1 ⇑(P.reflection i))
  (exists_eq_1 : ∀ (i j : ι), ∃ s, (algebraMap S R) s = (form_1 (P.root i)) (P.root j))
  (exists_pos_eq_1 : ∀ (i : ι), ∃ s > 0, (algebraMap S R) s = (form_1 (P.root i)) (P.root i)),
  ({ form := form, symm := symm, isOrthogonal_reflection := isOrthogonal_reflection, exists_eq := exists_eq,
        exists_pos_eq := exists_pos_eq } =
      { form := form_1, symm := symm_1, isOrthogonal_reflection := isOrthogonal_reflection_1, exists_eq := exists_eq_1,
        exists_pos_eq := exists_pos_eq_1 }) =
    (form = form_1)
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.mk.injEq : ∀ (bRiemann bHenstock bDistortion bRiemann_1 bHenstock_1 bDistortion_1 : Bool),
  ({ bRiemann := bRiemann, bHenstock := bHenstock, bDistortion := bDistortion } =
      { bRiemann := bRiemann_1, bHenstock := bHenstock_1, bDistortion := bDistortion_1 }) =
    (bRiemann = bRiemann_1 ∧ bHenstock = bHenstock_1 ∧ bDistortion = bDistortion_1)
-- Init.Data.Int.Lemmas
Int.natCast_succ : ∀ (n : ℕ), ↑n.succ = ↑n + 1
-- Mathlib.Analysis.Normed.Group.InfiniteSum
Summable.of_nnnorm : ∀ {ι : Type u_1} {E : Type u_3} [inst : SeminormedAddCommGroup E] [CompleteSpace E] {f : ι → E},
  (Summable fun a => ‖f a‖₊) → Summable f
-- Init.Data.UInt.Lemmas
UInt8.zero_sub : ∀ (a : UInt8), 0 - a = -a