mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.MulAction
dist_smul₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : SeminormedRing α] [inst_1 : SeminormedAddCommGroup β] [inst_2 : Module α β]
  [NormSMulClass α β] (s : α) (x y : β), dist (s • x) (s • y) = ‖s‖ * dist x y
-- Mathlib.Data.ENNReal.Holder
ENNReal.HolderConjugate.one_le : ∀ (p q : ENNReal) [p.HolderConjugate q], 1 ≤ p
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
CategoryTheory.Limits.instFinCategoryWalkingParallelPair : CategoryTheory.FinCategory CategoryTheory.Limits.WalkingParallelPair
-- Mathlib.Logic.Relator
Relator.left_unique_of_rel_eq : ∀ {α : Sort u₁} {β : Sort u₂} {R : α → β → Prop} {eq' : β → β → Prop},
  Relator.LiftFun R (Relator.LiftFun R Iff) Eq eq' → Relator.LeftUnique R
-- Mathlib.Order.Filter.Extr
IsExtrOn.comp_mono : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β} {s : Set α} {a : α},
  IsExtrOn f s a → ∀ {g : β → γ}, Monotone g → IsExtrOn (g ∘ f) s a
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
/-- The tripartite-from-triangles graph. Two vertices are related iff there exists a triangle index
containing them both.  -/
SimpleGraph.TripartiteFromTriangles.graph : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → Finset (α × β × γ) → SimpleGraph (α ⊕ β ⊕ γ)
-- Mathlib.Data.ZMod.QuotientGroup
/-- `ℤ` modulo multiples of `a : ℤ` is `ZMod a.natAbs`.  -/
Int.quotientZMultiplesEquivZMod : (a : ℤ) → ℤ ⧸ AddSubgroup.zmultiples a ≃+ ZMod a.natAbs
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPullback.of_forall_isPullback_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F₁ F₂ F₃ F₄ : CategoryTheory.Functor C D} {f₁ : F₁ ⟶ F₂} {f₂ : F₁ ⟶ F₃} {f₃ : F₂ ⟶ F₄} {f₄ : F₃ ⟶ F₄},
  (∀ (X : C), CategoryTheory.IsPullback (f₁.app X) (f₂.app X) (f₃.app X) (f₄.app X)) →
    CategoryTheory.IsPullback f₁ f₂ f₃ f₄
-- Mathlib.Data.ENNReal.Operations
ENNReal.mul_le_mul_iff_left : ∀ {a b c : ENNReal}, c ≠ 0 → c ≠ ⊤ → (a * c ≤ b * c ↔ a ≤ b)
-- Mathlib.CategoryTheory.Triangulated.Triangulated
/-- The triangle `Z₁₂ ⟶ Z₁₃ ⟶ Z₂₃ ⟶ Z₁₂⟦1⟧` given by an `Octahedron'`.  -/
CategoryTheory.Triangulated.Octahedron'.triangle : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} →
                {u₁₂ : X₁ ⟶ X₂} →
                  {u₂₃ : X₂ ⟶ X₃} →
                    {u₁₃ : X₁ ⟶ X₃} →
                      (comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃) →
                        {v₁₂ : Z₁₂ ⟶ X₁} →
                          {w₁₂ : X₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₂} →
                            (h₁₂ :
                                CategoryTheory.Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈
                                  CategoryTheory.Pretriangulated.distinguishedTriangles) →
                              {v₂₃ : Z₂₃ ⟶ X₂} →
                                {w₂₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₂₃} →
                                  (h₂₃ :
                                      CategoryTheory.Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈
                                        CategoryTheory.Pretriangulated.distinguishedTriangles) →
                                    {v₁₃ : Z₁₃ ⟶ X₁} →
                                      {w₁₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₃} →
                                        (h₁₃ :
                                            CategoryTheory.Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈
                                              CategoryTheory.Pretriangulated.distinguishedTriangles) →
                                          CategoryTheory.Triangulated.Octahedron' comm h₁₂ h₂₃ h₁₃ →
                                            CategoryTheory.Pretriangulated.Triangle C
-- Mathlib.AlgebraicGeometry.Geometrically.Connected
AlgebraicGeometry.instGeometricallyConnectedSndScheme : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [AlgebraicGeometry.GeometricallyConnected f],
  AlgebraicGeometry.GeometricallyConnected (CategoryTheory.Limits.pullback.snd f g)
-- Init.Data.String.Basic
String.ofList_comp_toList : String.ofList ∘ String.toList = id
-- Mathlib.Algebra.Module.PID
Module.exists_ker_toSpanSingleton_eq_annihilator : ∀ (R : Type u) [inst : CommRing R] [IsPrincipalIdealRing R] (M : Type v) [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [IsDomain R] [Module.Finite R M], ∃ x, (LinearMap.toSpanSingleton R M x).ker = Module.annihilator R M
-- Mathlib.GroupTheory.Coset.Card
/-- **Lagrange's Theorem**: The order of a subgroup divides the order of its ambient group. 

[Wikidata Q505798](https://www.wikidata.org/wiki/Q505798) -/
Subgroup.card_subgroup_dvd_card : ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α), Nat.card ↥s ∣ Nat.card α
-- Lean.Meta.SizeOf
Lean.Meta.mkSizeOfInstances : Lean.Name → Lean.MetaM Unit
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepSet.indep_generateFrom_lt : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : Preorder ι]
  {s : ι → Set Ω},
  (∀ (n : ι), MeasurableSet (s n)) →
    ProbabilityTheory.iIndepSet s μ →
      ∀ (i : ι),
        ProbabilityTheory.Indep (MeasurableSpace.generateFrom {s i})
          (MeasurableSpace.generateFrom {t | ∃ j < i, s j = t}) μ
-- Mathlib.Topology.Semicontinuity.Basic
ContinuousAt.comp_lowerSemicontinuousAt_antitone : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {γ : Type u_4} [inst_1 : LinearOrder γ]
  [inst_2 : TopologicalSpace γ] [OrderTopology γ] {δ : Type u_5} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ]
  [OrderTopology δ] {g : γ → δ} {f : α → γ},
  ContinuousAt g (f x) → LowerSemicontinuousAt f x → Antitone g → UpperSemicontinuousAt (g ∘ f) x
-- Mathlib.Order.SymmDiff
IsCompl.symmDiff_eq_top : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] {a b : α}, IsCompl a b → symmDiff a b = ⊤
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.ringHom_ext : ∀ {R : Type u_1} {T : Type u_3} [inst : CommRing R] [inst_1 : Semiring T] {p : Polynomial R} {f g : AdjoinRoot p →+* T},
  f.comp (AdjoinRoot.of p) = g.comp (AdjoinRoot.of p) → f (AdjoinRoot.root p) = g (AdjoinRoot.root p) → f = g
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
ContinuousMultilinearMap.instTopologicalSpace.eq_1 : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [inst : NormedField 𝕜]
  [inst_1 : (i : ι) → TopologicalSpace (E i)] [inst_2 : (i : ι) → AddCommGroup (E i)]
  [inst_3 : (i : ι) → Module 𝕜 (E i)] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F] [inst_6 : TopologicalSpace F]
  [inst_7 : IsTopologicalAddGroup F],
  ContinuousMultilinearMap.instTopologicalSpace =
    TopologicalSpace.induced ContinuousMultilinearMap.toUniformOnFun
      (UniformOnFun.topologicalSpace ((i : ι) → E i) F {s | Bornology.IsVonNBounded 𝕜 s})
-- Mathlib.MeasureTheory.Group.Prod
MeasureTheory.absolutelyContinuous_map_sub_left : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G)
  [MeasureTheory.SFinite μ] [MeasurableNeg G] [μ.IsAddLeftInvariant] (g : G),
  μ.AbsolutelyContinuous (MeasureTheory.Measure.map (fun h => g - h) μ)
-- Mathlib.Algebra.Ring.Int.Parity
Int.not_odd_iff_even : ∀ {n : ℤ}, ¬Odd n ↔ Even n
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey_union_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} (mem : k ∈ t₂), (t₁ ∪ t₂).getKey k ⋯ = t₂.getKey k mem
-- Mathlib.Data.Finset.Basic
Finset.erase_empty : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α), ∅.erase a = ∅
-- Mathlib.RingTheory.Localization.Basic
Localization.coe_algEquiv_symm : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S],
  ↑(Localization.algEquiv M S).symm = IsLocalization.map (Localization M) (RingHom.id R) ⋯
-- Mathlib.GroupTheory.Congruence.Hom
/-- The diagram describing the universal property for quotients of monoids commutes.  -/
Con.lift_mk' : ∀ {M : Type u_1} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass P] {c : Con M} {f : M →* P}
  (H : c ≤ Con.ker f) (x : M), (c.lift f H) (c.mk' x) = f x
-- Mathlib.RingTheory.Etale.Basic
Algebra.FormallyEtale.instLocalization : ∀ {R : Type u_2} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.FormallyEtale R S] (M : Submonoid S), Algebra.FormallyEtale R (Localization M)
-- Mathlib.Analysis.Calculus.FDeriv.Mul
HasFDerivWithinAt.mul' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {s : Set E} {𝔸 : Type u_5} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸]
  {a b : E → 𝔸} {a' b' : E →L[𝕜] 𝔸},
  HasFDerivWithinAt a a' s x →
    HasFDerivWithinAt b b' s x → HasFDerivWithinAt (a * b) (a x • b' + MulOpposite.op (b x) • a') s x
-- Init.Data.String.Lemmas.Basic
String.Pos.startPos_le : ∀ {s : String} (p : s.Pos), s.startPos ≤ p
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.exactAt_of_isGE : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : CochainComplex C ℤ) (n i : ℤ),
  autoParam (i < n) CochainComplex.exactAt_of_isGE._auto_1 → ∀ [K.IsGE n], HomologicalComplex.ExactAt K i
-- Mathlib.Data.List.AList
AList.lookup_isSome : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {s : AList β}, (AList.lookup a s).isSome = true ↔ a ∈ s
-- Mathlib.Data.Nat.Factorization.Basic
/-- A product over `n.primeFactors` can be written as a product over `n.factorization`;  -/
Nat.prod_primeFactors_prod_factorization : ∀ {n : ℕ} {β : Type u_1} [inst : CommMonoid β] (f : ℕ → β),
  ∏ p ∈ n.primeFactors, f p = n.factorization.prod fun p x => f p
-- Init.Data.Option.Basic
Option.isNone_some : ∀ {α : Type u_1} {a : α}, (some a).isNone = false
-- Init.Data.Option.Lemmas
Option.map_id_apply' : ∀ {α : Type u} {x : Option α}, Option.map (fun a => a) x = x
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.Cell.ι_t_assoc : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] {f : P.RankFunction ι}
  [inst_1 : P.IsProper] {j : ι} (c : f.Cell j) {Z : SSet} (h : (f.filtration j).toSSet ⟶ Z),
  CategoryTheory.CategoryStruct.comp c.ιSigmaHorn (CategoryTheory.CategoryStruct.comp (f.t j) h) =
    CategoryTheory.CategoryStruct.comp (SSet.Subcomplex.Pairing.RankFunction.Cell.mapHorn f c) h
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.mkPrecomp_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {Y Y' : C} {S : CategoryTheory.Functor C D} (f : S.obj Y ⟶ T) (g : Y' ⟶ Y),
  (CategoryTheory.CostructuredArrow.mkPrecomp f g).right =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.comp (S.map g) f)).right
-- Mathlib.Topology.Algebra.Monoid
tendsto_add : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Add M] [ContinuousAdd M] {a b : M},
  Filter.Tendsto (fun p => p.1 + p.2) (nhds (a, b)) (nhds (a + b))
-- Mathlib.Topology.EMetricSpace.Basic
/-- An emetric space is separated  -/
EMetricSpace.instT0Space : ∀ {γ : Type w} [inst : EMetricSpace γ], T0Space γ
-- Mathlib.MeasureTheory.Group.Arithmetic
AEMeasurable.smul_const : ∀ {M : Type u_2} {X : Type u_3} {α : Type u_4} [inst : MeasurableSpace X] [inst_1 : SMul M X] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {f : α → M} [inst_2 : MeasurableSpace M] [MeasurableSMul M X],
  AEMeasurable f μ → ∀ (y : X), AEMeasurable (fun x => f x • y) μ
-- Mathlib.Analysis.InnerProductSpace.Adjoint
LinearMap.id_mem_unitary : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E], LinearMap.id ∈ unitary (E →ₗ[𝕜] E)
-- Lean.Meta.Coe
Lean.Meta.autoLift : Lean.Option Bool
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.liftRel_nil : ∀ {α : Type u} {β : Type v} (R : α → β → Prop), Stream'.WSeq.LiftRel R Stream'.WSeq.nil Stream'.WSeq.nil
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.balanceₘ.match_3.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (r : Std.DTreeMap.Internal.Impl α β)
  (motive :
    (l : Std.DTreeMap.Internal.Impl α β) →
      ¬r.size > Std.DTreeMap.Internal.delta * l.size → l.size > Std.DTreeMap.Internal.delta * r.size → Sort u_3)
  (h : ¬r.size > Std.DTreeMap.Internal.delta * Std.DTreeMap.Internal.Impl.leaf.size)
  (h_1 : Std.DTreeMap.Internal.Impl.leaf.size > Std.DTreeMap.Internal.delta * r.size)
  (h_1_1 :
    (h : ¬r.size > Std.DTreeMap.Internal.delta * Std.DTreeMap.Internal.Impl.leaf.size) →
      (h_2 : Std.DTreeMap.Internal.Impl.leaf.size > Std.DTreeMap.Internal.delta * r.size) →
        motive Std.DTreeMap.Internal.Impl.leaf h h_2)
  (h_2 :
    (size : ℕ) →
      (lk : α) →
        (lv : β lk) →
          (ll lr : Std.DTreeMap.Internal.Impl α β) →
            (h : ¬r.size > Std.DTreeMap.Internal.delta * (Std.DTreeMap.Internal.Impl.inner size lk lv ll lr).size) →
              (h_2 : (Std.DTreeMap.Internal.Impl.inner size lk lv ll lr).size > Std.DTreeMap.Internal.delta * r.size) →
                motive (Std.DTreeMap.Internal.Impl.inner size lk lv ll lr) h h_2),
  (match Std.DTreeMap.Internal.Impl.leaf, h, h_1 with
    | Std.DTreeMap.Internal.Impl.leaf, h, h_3 => h_1_1 h h_3
    | Std.DTreeMap.Internal.Impl.inner size lk lv ll lr, h, h_3 => h_2 size lk lv ll lr h h_3) =
    h_1_1 h h_1
-- Mathlib.FieldTheory.LinearDisjoint
/-- If `A ⊗[F] L` is a field, then `A` and `L` are linearly disjoint over `F`.  -/
IntermediateField.LinearDisjoint.of_isField : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A : IntermediateField F E}
  {L : Type w} [inst_3 : Field L] [inst_4 : Algebra F L] [inst_5 : Algebra L E] [inst_6 : IsScalarTower F L E],
  IsField (TensorProduct F (↥A) L) → A.LinearDisjoint L
-- Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy
_private.Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy.0.CategoryTheory.SimplicialObject.Homotopy.ToChainHomotopy.comm_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {X Y : CategoryTheory.SimplicialObject C} {f g : X ⟶ Y} (H : CategoryTheory.SimplicialObject.Homotopy f g),
  f.app (Opposite.op { len := 0 }) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.Homotopy.ToChainHomotopy.hom H 0 1)
        (((AlgebraicTopology.alternatingFaceMapComplex C).obj Y).d 1 0) +
      g.app (Opposite.op { len := 0 })
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.ProjRestricts.congr_simp : ∀ {I : Type u} (C : Set (I → Bool)) {J K : I → Prop} [inst : (i : I) → Decidable (J i)]
  [inst_1 : (i : I) → Decidable (K i)] (h : ∀ (i : I), J i → K i) (a a_1 : ↑(Profinite.NobelingProof.π C K)),
  a = a_1 → Profinite.NobelingProof.ProjRestricts C h a = Profinite.NobelingProof.ProjRestricts C h a_1
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get?_insertMany_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    ∀ {v : β},
      List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
        (k, v) ∈ l → Std.DTreeMap.Const.get? (Std.DTreeMap.Const.insertMany t l) k' = some v
-- Mathlib.Analysis.Real.Sqrt
Real.sqrt_eq_zero : ∀ {x : ℝ}, 0 ≤ x → (√x = 0 ↔ x = 0)
-- Mathlib.Algebra.Ring.Equiv
/-- Gives a `RingEquiv` from an element of a `MulEquivClass` preserving addition.  -/
MulEquiv.toRingEquiv : {R : Type u_7} →
  {S : Type u_8} →
    {F : Type u_9} →
      [inst : Add R] →
        [inst_1 : Add S] →
          [inst_2 : Mul R] →
            [inst_3 : Mul S] →
              [inst_4 : EquivLike F R S] →
                [MulEquivClass F R S] → (f : F) → (∀ (x y : R), f (x + y) = f x + f y) → R ≃+* S
-- Mathlib.Algebra.Colimit.Module
/-- The universal property of the direct limit: maps from the components to another module
that respect the directed system structure (i.e. make some diagram commute) give rise
to a unique map out of the direct limit.  -/
Module.DirectLimit.lift : (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)] →
              (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) →
                [inst_4 : DecidableEq ι] →
                  {P : Type u_4} →
                    [inst_5 : AddCommMonoid P] →
                      [inst_6 : Module R P] →
                        (g : (i : ι) → G i →ₗ[R] P) →
                          (∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x) →
                            Module.DirectLimit G f →ₗ[R] P
-- Mathlib.RingTheory.Ideal.Cotangent
Ideal.mem_toCotangent_ker : ∀ {R : Type u} [inst : CommRing R] (I : Ideal R) {x : ↥I}, x ∈ I.toCotangent.ker ↔ ↑x ∈ I ^ 2
-- Mathlib.Data.Quot
Trunc.out_eq : ∀ {α : Sort u_1} (q : Trunc α), Trunc.mk q.out = q
-- Mathlib.LinearAlgebra.BilinearForm.Orthogonal
LinearMap.BilinForm.eq_top_of_restrict_nondegenerate_of_orthogonal_eq_bot : ∀ {V : Type u_5} {K : Type u_6} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] [FiniteDimensional K V]
  {B : LinearMap.BilinForm K V} {W : Submodule K V},
  B.IsRefl → (B.restrict W).Nondegenerate → B.orthogonal W = ⊥ → W = ⊤
-- Mathlib.Algebra.Order.ToIntervalMod
QuotientAddGroup.equivIocMod_zero : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a : α), (QuotientAddGroup.equivIocMod hp a) 0 = ⟨toIocMod hp a 0, ⋯⟩
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.to_average : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε : Type u_8} [inst : TopologicalSpace ε]
  [inst_1 : ESeminormedAddMonoid ε] {f : α → ε},
  MeasureTheory.Integrable f μ → MeasureTheory.Integrable f ((μ Set.univ)⁻¹ • μ)
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.BoolExpr.literal.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (a : α), sizeOf (Std.Tactic.BVDecide.BoolExpr.literal a) = 1 + sizeOf a
-- Mathlib.CategoryTheory.Triangulated.TStructure.Induced
/-- Constructor for `HasInducedTStructure`.  -/
CategoryTheory.ObjectProperty.HasInducedTStructure.mk' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {P : CategoryTheory.ObjectProperty C} [inst_6 : P.IsTriangulated] {t : CategoryTheory.Triangulated.TStructure C},
  (∀ (X : C), P X → ∀ (n : ℤ), P ((t.truncLE n).obj X) ∧ P ((t.truncGE n).obj X)) → P.HasInducedTStructure t
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
continuousAt_extChartAt : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} [inst_5 : ChartedSpace H M] (x : M), ContinuousAt (↑(extChartAt I x)) x
-- Mathlib.AlgebraicTopology.SimplicialObject.Op
SimplicialObject.opFunctorCompOpFunctorIso_inv_app_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] (X : CategoryTheory.SimplicialObject C)
  (n : SimplexCategoryᵒᵖ),
  (SimplicialObject.opFunctorCompOpFunctorIso.inv.app X).app n =
    CategoryTheory.CategoryStruct.comp SimplicialObject.opObjIso.inv SimplicialObject.opObjIso.inv
-- Lean.Data.DeclarationRange
Lean.instDecidableEqDeclarationRange : DecidableEq Lean.DeclarationRange
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_17.eq_1 : ∀ (motive : (w : ℕ) → Std.Tactic.BVDecide.BVExpr w → Sort u_1) (w a : ℕ)
  (h_1 : (w a : ℕ) → motive w (Std.Tactic.BVDecide.BVExpr.var a))
  (h_2 : (w : ℕ) → (val : BitVec w) → motive w (Std.Tactic.BVDecide.BVExpr.const val))
  (h_3 :
    (w : ℕ) →
      (lhsExpr : Std.Tactic.BVDecide.BVExpr w) →
        (op : Std.Tactic.BVDecide.BVBinOp) →
          (rhsExpr : Std.Tactic.BVDecide.BVExpr w) → motive w (lhsExpr.bin op rhsExpr))
  (h_4 :
    (w : ℕ) →
      (op : Std.Tactic.BVDecide.BVUnOp) →
        (expr : Std.Tactic.BVDecide.BVExpr w) → motive w (Std.Tactic.BVDecide.BVExpr.un op expr))
  (h_5 :
    (w l r : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr l) →
        (rhs : Std.Tactic.BVDecide.BVExpr r) → (h : w = l + r) → motive w (lhs.append rhs h))
  (h_6 :
    (w w_1 n : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w_1) →
        (h : w = w_1 * n) → motive w (Std.Tactic.BVDecide.BVExpr.replicate n expr h))
  (h_7 :
    (len w start : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w) → motive len (Std.Tactic.BVDecide.BVExpr.extract start len expr))
  (h_8 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftLeft rhs))
  (h_9 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftRight rhs))
  (h_10 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.arithShiftRight rhs)),
  (match w, Std.Tactic.BVDecide.BVExpr.var a with
    | w, Std.Tactic.BVDecide.BVExpr.var a => h_1 w a
    | w, Std.Tactic.BVDecide.BVExpr.const val => h_2 w val
    | w, lhsExpr.bin op rhsExpr => h_3 w lhsExpr op rhsExpr
    | w, Std.Tactic.BVDecide.BVExpr.un op expr => h_4 w op expr
    | w, lhs.append rhs h => h_5 w l r lhs rhs h
    | w, Std.Tactic.BVDecide.BVExpr.replicate n expr h => h_6 w w_1 n expr h
    | len, Std.Tactic.BVDecide.BVExpr.extract start .(len) expr => h_7 len w start expr
    | w, lhs.shiftLeft rhs => h_8 w n lhs rhs
    | w, lhs.shiftRight rhs => h_9 w n lhs rhs
    | w, lhs.arithShiftRight rhs => h_10 w n lhs rhs) =
    h_1 w a
-- Init.Data.SInt.Lemmas
Int64.sub_neg : ∀ {a b : Int64}, a - -b = a + b
-- Init.Data.SInt.Lemmas
Int64.toInt32_ofNat : ∀ {n : ℕ}, (OfNat.ofNat n).toInt32 = OfNat.ofNat n
-- Mathlib.Algebra.Order.GroupWithZero.Basic
one_lt_zpow₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀]
  {n : ℤ}, 1 < a → 0 < n → 1 < a ^ n
-- Std.Do.WP.Sound
/-- Soundness lemma for `Except`: `Id`-specialization of `ExceptT.of_wp_run`.  -/
Std.Do.Except.of_wp_eq : ∀ {ε α : Type} {x prog : Except ε α},
  prog = x →
    ∀ (P : Except ε α → Prop),
      (⊢ₛ (Std.Do.wp prog).apply (fun a => ⌜P (Except.ok a)⌝, fun e => ⌜P (Except.error e)⌝, PUnit.unit)) → P x