mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.sup_def : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S T : Subalgebra R A),
  S ⊔ T = Algebra.adjoin R (↑S ∪ ↑T)
-- Mathlib.Topology.MetricSpace.Congruence
/-- Congruence follows from preserved distance. Backward direction of `congruent_iff_dist_eq`.  -/
Congruent.of_dist_eq : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoMetricSpace P₁]
  [inst_1 : PseudoMetricSpace P₂], (∀ (i₁ i₂ : ι), dist (v₁ i₁) (v₁ i₂) = dist (v₂ i₁) (v₂ i₂)) → Congruent v₁ v₂
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.zero_or_succ_or_isSuccLimit : ∀ (o : Ordinal.{u_4}), o = 0 ∨ o ∈ Set.range Order.succ ∨ Order.IsSuccLimit o
-- Mathlib.Analysis.Calculus.Deriv.Slope
/-- Given a set `t` such that `s ∩ t` is dense in `s`, then the range of `derivWithin f s` is
contained in the closure of the submodule spanned by the image of `t`.  -/
range_derivWithin_subset_closure_span_image : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (f : 𝕜 → F) {s t : Set 𝕜},
  s ⊆ closure (s ∩ t) → Set.range (derivWithin f s) ⊆ closure ↑(Submodule.span 𝕜 (f '' t))
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.postcompose₂_obj_map_app_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {E : Type u_7} [inst_2 : CategoryTheory.Category.{v_7, u_7} E]
  {E' : Type u_8} [inst_3 : CategoryTheory.Category.{v_8, u_8} E'] (X : CategoryTheory.Functor E E')
  {X_1 Y : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ E)} (α : X_1 ⟶ Y) (X_2 : C₁) (X_3 : C₂),
  (((CategoryTheory.Functor.postcompose₂.obj X).map α).app X_2).app X_3 = X.map ((α.app X_2).app X_3)
-- Mathlib.Topology.CWComplex.Classical.Subcomplex
Topology.RelCWComplex.Subcomplex.closedCell_subset_of_mem : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [inst : Topology.RelCWComplex C D]
  (E : Topology.RelCWComplex.Subcomplex C) {n : ℕ} {i : Topology.RelCWComplex.cell C n},
  i ∈ E.I n → Topology.RelCWComplex.closedCell n i ⊆ ↑E
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.cospanCompIso_inv_app_one : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z),
  (CategoryTheory.Limits.cospanCompIso F f g).inv.app CategoryTheory.Limits.WalkingCospan.one =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.Limits.cospan (F.map f) (F.map g)).obj CategoryTheory.Limits.WalkingCospan.one)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Cpop
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Cpop.0.Std.Tactic.BVDecide.BVExpr.bitblast.denote_blastExtractAndExtendBit : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} {assign : α → Bool} (aig : Std.Sat.AIG α)
  (xc : aig.RefVec w) (x : BitVec w) (start : ℕ),
  (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := xc.get idx hidx }⟧ = x.getLsbD idx) →
    ∀ (idx : ℕ) (hidx : idx < w),
      ⟦assign,
          { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtendBit aig { start := start, x := xc }).aig,
            ref :=
              (Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtendBit aig { start := start, x := xc }).vec.get idx
                hidx }⟧ =
        (BitVec.extractAndExtendBit start w x).getLsbD idx
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_presheafFiberCompIso_hom_app : ∀ {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] {B : Type u''}
  [inst_2 : CategoryTheory.Category.{v'', u''} B] [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A]
  [inst_4 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} B] (F : CategoryTheory.Functor A B)
  [inst_5 : CategoryTheory.LocallySmall.{w, v, u} C]
  [inst_6 : CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v'', u', u''} F] (X : C)
  (x : Φ.fiber.obj X) (P : CategoryTheory.Functor Cᵒᵖ A),
  CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x (P.comp F)) ((Φ.presheafFiberCompIso F).hom.app P) =
    F.map (Φ.toPresheafFiber X x P)
-- Mathlib.LinearAlgebra.Projection
LinearMap.IsIdempotentElem.range_eq_ker_one_sub : ∀ {S : Type u_5} [inst : Semiring S] {E : Type u_7} [inst_1 : AddCommGroup E] [inst_2 : Module S E] {p : E →ₗ[S] E},
  IsIdempotentElem p → p.range = (1 - p).ker
-- Mathlib.Order.Max
not_isMax_of_lt : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a < b → ¬IsMax a
-- Mathlib.LinearAlgebra.Pi
LinearMap.iSup_range_single_eq_iInf_ker_proj : ∀ (R : Type u) {ι : Type x} [inst : Semiring R] (φ : ι → Type i) [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)] [inst_3 : DecidableEq ι] {I J : Set ι},
  IsCompl I J → I.Finite → ⨆ i ∈ I, (LinearMap.single R φ i).range = ⨅ i ∈ J, (LinearMap.proj i).ker
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.toList_filter : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} {f : α → β → Bool}
  (h : t.WF),
  Std.DTreeMap.Internal.Impl.Const.toList (Std.DTreeMap.Internal.Impl.filter f t ⋯).impl =
    List.filter (fun p => f p.1 p.2) (Std.DTreeMap.Internal.Impl.Const.toList t)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
deriv_ccos : ∀ {f : ℂ → ℂ} {x : ℂ}, DifferentiableAt ℂ f x → deriv (fun x => Complex.cos (f x)) x = -Complex.sin (f x) * deriv f x
-- Lean.Data.Lsp.CodeActions
/-- The code action kind values the client supports. When this
property exists the client also guarantees that it will
handle values outside its set gracefully and falls back
to a default value when unknown.
 -/
Lean.Lsp.CodeActionLiteralSupportValueSet.valueSet : Lean.Lsp.CodeActionLiteralSupportValueSet → Array Lean.Lsp.CodeActionKind
-- Mathlib.Algebra.Polynomial.Eval.Coeff
Polynomial.mapRingHom_id : ∀ {R : Type u} [inst : Semiring R], Polynomial.mapRingHom (RingHom.id R) = RingHom.id (Polynomial R)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.natIsoSc'_inv_app_τ₁ : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} (c : ComplexShape ι) (i j k : ι) (hi : c.prev j = i) (hk : c.next j = k) (X : HomologicalComplex C c),
  ((HomologicalComplex.natIsoSc' C c i j k hi hk).inv.app X).τ₁ = (X.XIsoOfEq hi).inv
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.algebraMap_fst : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A] (k : 𝕜),
  ((algebraMap 𝕜 (DoubleCentralizer 𝕜 A)) k).toProd.1 = (algebraMap 𝕜 (A →L[𝕜] A)) k
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- Continuity from below:
the measure of the union of a directed sequence of (not necessarily measurable) sets
is the supremum of the measures.  -/
Directed.measure_iUnion : ∀ {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable ι] {s : ι → Set α},
  Directed (fun x1 x2 => x1 ⊆ x2) s → μ (⋃ i, s i) = ⨆ i, μ (s i)
-- Mathlib.Tactic.Order.Graph.Basic
/-- Proof of `atoms[src] ≤ atoms[dst]`.  -/
Mathlib.Tactic.Order.Edge.proof : Mathlib.Tactic.Order.Edge → Lean.Expr
-- Mathlib.Tactic.FBinop
_private.Mathlib.Tactic.FBinop.0.FBinopElab.Tree.term.sizeOf_spec : ∀ (ref : Lean.Syntax) (infoTrees : Lean.PersistentArray Lean.Elab.InfoTree) (val : Lean.Expr),
  sizeOf (FBinopElab.Tree.term✝ ref infoTrees val) = 1 + sizeOf ref + sizeOf infoTrees + sizeOf val
-- Mathlib.ModelTheory.Basic
/-- A first-order embedding is also a first-order homomorphism.  -/
FirstOrder.Language.Embedding.toHom : {L : FirstOrder.Language} →
  {M : Type w} → {N : Type w'} → [inst : L.Structure M] → [inst_1 : L.Structure N] → L.Embedding M N → L.Hom M N
-- Mathlib.Data.Nat.Choose.Basic
Nat.choose_le_add : ∀ (a b c : ℕ), a.choose c ≤ (a + b).choose c
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.nonsing_inv_mul_cancel_left : ∀ {m : Type u} {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α]
  (A : Matrix n n α) (B : Matrix n m α), IsUnit A.det → A⁻¹ * (A * B) = B
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.sc₂_X₁ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n₀ : ℤ),
  (X.sc₂ f g fg h n₀).X₁ = (X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ f)
-- Mathlib.Tactic.Translate.Reorder
/-- The reordering of arguments.  -/
Mathlib.Tactic.Translate.Reorder.reorder : Mathlib.Tactic.Translate.Reorder → Mathlib.Tactic.Translate.ArgReorder
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.toStarAlgHom_refl : ∀ {R : Type u_1} {A₁ : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Algebra R A₁]
  [inst_3 : Star A₁], (StarAlgEquiv.refl R A₁).toStarAlgHom = StarAlgHom.id R A₁
-- Mathlib.RingTheory.UniqueFactorizationDomain.Defs
UniqueFactorizationMonoid.induction_on_prime : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [UniqueFactorizationMonoid α] {P : α → Prop} (a : α),
  P 0 → (∀ (x : α), IsUnit x → P x) → (∀ (a p : α), a ≠ 0 → Prime p → P a → P (p * a)) → P a
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.insertMany_list_eq_foldl : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List α}, m.insertMany l = List.foldl (fun acc a => acc.insert a) m l
-- Mathlib.Analysis.Normed.Unbundled.InvariantExtension
/-- The algebra norm `invariantExtension` is nonarchimedean.  -/
IsUltrametricDist.isNonarchimedean_invariantExtension : ∀ (K : Type u_1) [inst : NormedField K] (L : Type u_2) [inst_1 : Field L] [inst_2 : Algebra K L]
  [h_fin : FiniteDimensional K L] [hu : IsUltrametricDist K],
  IsNonarchimedean ⇑(IsUltrametricDist.invariantExtension K L)
-- Mathlib.CategoryTheory.Sigma.Basic
CategoryTheory.Sigma.mapId_inv_app : ∀ (I : Type w₁) (C : I → Type u₁) [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  (x : (i : I) × (fun i => C (id i)) i),
  (CategoryTheory.Sigma.mapId I C).inv.app x = CategoryTheory.CategoryStruct.id ⟨x.fst, x.snd⟩
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKey!_unitOfList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α] {l : List α} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l →
      k ∈ l → (Std.ExtDTreeMap.Const.unitOfList l cmp).getKey! k' = k
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
/-- The obvious map from a type to its 1-combinations, as an equivariant map.  -/
Set.powersetCard.addActionHom_singleton : (G : Type u_1) →
  [inst : AddGroup G] →
    (α : Type u_2) → [inst_1 : AddAction G α] → [inst_2 : DecidableEq α] → α →ₑ[id] ↑(Set.powersetCard α 1)
-- Mathlib.Algebra.Group.PNatPowAssoc
Prod.instPNatPowAssoc : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Pow M ℕ+] [PNatPowAssoc M] [inst_3 : Mul N] [inst_4 : Pow N ℕ+]
  [PNatPowAssoc N], PNatPowAssoc (M × N)
-- Init.Control.Except
instMonadAttachExceptTOfMonad : {m : Type (max u_1 u_2) → Type u_3} → {ε : Type (max u_1 u_2)} → [Monad m] → [MonadAttach m] → MonadAttach (ExceptT ε m)
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.instCategory : (R : Type u) →
  [inst : Ring R] → [inst_1 : TopologicalSpace R] → CategoryTheory.Category.{u_1, max u (u_1 + 1)} (TopModuleCat R)
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.hom_nsmul : ∀ {R : Type u} [inst : Ring R] {M N : ModuleCat R} (n : ℕ) (f : M ⟶ N),
  ModuleCat.Hom.hom (n • f) = n • ModuleCat.Hom.hom f
-- Lean.Data.FuzzyMatching
Lean.FuzzyMatching.CharRole.head : Lean.FuzzyMatching.CharRole
-- Mathlib.Order.Basic
le_of_forall_lt_imp_le_of_dense : ∀ {α : Type u_2} [inst : LinearOrder α] [DenselyOrdered α] {a₁ a₂ : α}, (∀ a < a₂, a ≤ a₁) → a₂ ≤ a₁
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.lt_veblen_iff_invVeblen₁_le : ∀ {o a : Ordinal.{u}}, a < Ordinal.veblen o a ↔ a.invVeblen₁ ≤ o
-- Mathlib.Algebra.Group.Equiv.TypeTags
/-- Reinterpret `Multiplicative G ≃* H` as `G ≃+ Additive H` as.  -/
MulEquiv.toAdditiveRight : {G : Type u_2} →
  {H : Type u_3} → [inst : AddZeroClass G] → [inst_1 : MulOneClass H] → Multiplicative G ≃* H ≃ (G ≃+ Additive H)
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
/-- This is a trivial fibration `resolutionObj X ⟶ X` where
`resolutionObj X` is a choice of a cofibrant resolution of `X`.  -/
HomotopicalAlgebra.CofibrantObject.HoCat.pResolutionObj : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      (X : C) → HomotopicalAlgebra.CofibrantObject.HoCat.resolutionObj X ⟶ X
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- `p.mulOccursInAt x g` means that the finite pattern
`p` appears in the configuration `x`
at position `g`.

Formally: for every position `h` in the support of `p`, the value of the configuration
at `g * h` coincides with the value of `p.config` at `h`.

Intuitively, if you shift the configuration `x` by `g` (using `mulShift g`),
then on the support of `p` you exactly recover the pattern `p`. This is the basic
notion of "pattern occurrence" used to define subshifts via forbidden patterns.  -/
SymbolicDynamics.FullShift.Pattern.mulOccursInAt : {A : Type u_1} →
  {G : Type u_2} → [inst : Inhabited A] → [Monoid G] → SymbolicDynamics.FullShift.Pattern A G → (G → A) → G → Prop
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.mem_smul_iff_of_ne : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] [inst_1 : DecidableEq ι]
  [inst_2 : (i : ι) → DecidableEq (M i)] {i j : ι},
  i ≠ j →
    ∀ {m₁ : M i} {m₂ : M j} {w : Monoid.CoprodI.Word M},
      ⟨i, m₁⟩ ∈ (Monoid.CoprodI.of m₂ • w).toList ↔ ⟨i, m₁⟩ ∈ w.toList
-- Mathlib.MeasureTheory.Function.Jacobian
/-- Assume that a function `f` has a derivative at every point of a set `s`. Then one may
partition `s` into countably many disjoint relatively measurable sets (i.e., intersections
of `s` with measurable sets `t n`) on which `f` is well approximated by linear maps `A n`.  -/
exists_partition_approximatesLinearOn_of_hasFDerivWithinAt : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : MeasurableSpace E] [BorelSpace E]
  [SecondCountableTopology F] (f : E → F) (s : Set E) (f' : E → E →L[ℝ] F),
  (∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) →
    ∀ (r : (E →L[ℝ] F) → NNReal),
      (∀ (A : E →L[ℝ] F), r A ≠ 0) →
        ∃ t A,
          Pairwise (Function.onFun Disjoint t) ∧
            (∀ (n : ℕ), MeasurableSet (t n)) ∧
              s ⊆ ⋃ n, t n ∧
                (∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))) ∧
                  (s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y)
-- Mathlib.Topology.UniformSpace.Equicontinuity
Filter.HasBasis.equicontinuousWithinAt_iff_left : ∀ {ι : Type u_1} {κ : Type u_2} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α]
  {p : κ → Prop} {s : κ → Set X} {F : ι → X → α} {S : Set X} {x₀ : X},
  (nhdsWithin x₀ S).HasBasis p s →
    (EquicontinuousWithinAt F S x₀ ↔ ∀ U ∈ uniformity α, ∃ k, p k ∧ ∀ x ∈ s k, ∀ (i : ι), (F i x₀, F i x) ∈ U)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.DeclValue.isCodeAndM : {m : Type → Type u_1} →
  {pu : Lean.Compiler.LCNF.Purity} →
    [Monad m] → Lean.Compiler.LCNF.DeclValue pu → (Lean.Compiler.LCNF.Code pu → m Bool) → m Bool
-- Mathlib.Combinatorics.Additive.CovBySMul
covByVAdd_zero : ∀ {M : Type u_1} {X : Type u_3} [inst : AddMonoid M] [inst_1 : AddAction M X] {A B : Set X}, CovByVAdd M 0 A B ↔ A = ∅
-- Lean.Meta.Tactic.Simp.Arith.Int.Basic
Lean.Meta.Simp.Arith.Int.ToLinear.State.mk.sizeOf_spec : ∀ (varMap : Lean.Meta.KExprMap ℕ) (vars : Array Lean.Expr),
  sizeOf { varMap := varMap, vars := vars } = 1 + sizeOf varMap + sizeOf vars
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyMapData.comm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData}
  (h : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂),
  CategoryTheory.CategoryStruct.comp h.left.φH h₂.iso.hom = CategoryTheory.CategoryStruct.comp h₁.iso.hom h.right.φH
-- Mathlib.Order.Bounds.Basic
upperBounds_Ico : ∀ {γ : Type u_3} [inst : SemilatticeInf γ] [DenselyOrdered γ] {a b : γ}, b < a → upperBounds (Set.Ico b a) = Set.Ici a
-- Mathlib.Logic.Equiv.Defs
Equiv.trans_def : ∀ {a : Sort u_2} {b : Sort u_1} {c : Sort u_3} (e₁ : a ≃ b) (e₂ : b ≃ c), Trans.trans e₁ e₂ = e₁.trans e₂
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey_maxKey!_eq_maxKey : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {hc : t.maxKey! ∈ t}, t.getKey t.maxKey! hc = t.maxKey ⋯
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
/-- `localized₀` as a `FrameHom`.  -/
Submodule.localized₀FrameHom : {R : Type u_1} →
  {M : Type u_3} →
    {N : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid N] →
            [inst_3 : Module R M] →
              [inst_4 : Module R N] →
                (p : Submonoid R) → (f : M →ₗ[R] N) → [IsLocalizedModule p f] → FrameHom (Submodule R M) (Submodule R N)
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
unitInterval.continuous_sigmoid : Continuous unitInterval.sigmoid
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.algEquivAevalNegX_apply : ∀ {R : Type u_3} [inst : CommRing R] (a : Polynomial R),
  Polynomial.algEquivAevalNegX a = (Polynomial.aeval (-Polynomial.X)) a
-- Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Metric.biUnion_lt_ball : ∀ {α : Type u_2} [inst : PseudoMetricSpace α] (x : α) (r : ℝ), ⋃ r', ⋃ (_ : r' < r), Metric.ball x r' = Metric.ball x r
-- Mathlib.RingTheory.Flat.Basic
/-- Tensor product of linearly independent families is linearly
independent under some flatness conditions.

The flatness condition could be removed over domains.
See `LinearIndependent.tmul_of_isDomain`.  -/
LinearIndependent.tmul_of_flat_right : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} {N : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] {ι : Type u_6} {κ : Type u_7} {v : ι → M}
  {w : κ → N} [Module.Flat R N],
  LinearIndependent R v → LinearIndependent R w → LinearIndependent R fun i => v i.1 ⊗ₜ[R] w i.2
-- Init.Data.Nat.Lemmas
Nat.one_le_two_pow : ∀ {n : ℕ}, 1 ≤ 2 ^ n
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Zipper.cons.injEq : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (tree : Std.DTreeMap.Internal.Impl α β)
  (next : Std.DTreeMap.Internal.Zipper α β) (k_1 : α) (v_1 : β k_1) (tree_1 : Std.DTreeMap.Internal.Impl α β)
  (next_1 : Std.DTreeMap.Internal.Zipper α β),
  (Std.DTreeMap.Internal.Zipper.cons k v tree next = Std.DTreeMap.Internal.Zipper.cons k_1 v_1 tree_1 next_1) =
    (k = k_1 ∧ v ≍ v_1 ∧ tree = tree_1 ∧ next = next_1)
-- Mathlib.Order.Preorder.Chain
Flag.top_mem : ∀ {α : Type u_1} [inst : LE α] [inst_1 : OrderTop α] (s : Flag α), ⊤ ∈ s
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.instInhabitedMRefinePat : Inhabited Lean.Parser.Tactic.MRefinePat
-- Init.Data.Rat.Lemmas
Rat.lt_iff : ∀ (a b : ℚ), a < b ↔ a.num * ↑b.den < b.num * ↑a.den
-- Mathlib.Order.Circular
/-- Syntax typeclass for a betweenness relation.  -/
Btw : Type u_1 → Type u_1
-- Init.Data.SInt.Lemmas
Int64.sub_le : ∀ {a b : Int64}, 0 ≤ b → b ≤ a → a - b ≤ a
-- Mathlib.Algebra.CubicDiscriminant
Cubic.leadingCoeff_of_b_ne_zero' : ∀ {R : Type u_1} {b c d : R} [inst : Semiring R], b ≠ 0 → { a := 0, b := b, c := c, d := d }.toPoly.leadingCoeff = b
-- Mathlib.Probability.Kernel.Composition.Prod
ProbabilityTheory.Kernel.prodComm_prod : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ]
  {η : ProbabilityTheory.Kernel α γ} [ProbabilityTheory.IsSFiniteKernel η],
  (κ.prod η).map ⇑MeasurableEquiv.prodComm = η.prod κ
-- Mathlib.GroupTheory.MonoidLocalization.Away
Submonoid.LocalizationMap.AwayMap.lift_comp : ∀ {M : Type u_1} [inst : CommMonoid M] {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3} [inst_2 : CommMonoid P]
  {g : M →* P} (x : M) (F : Submonoid.LocalizationMap.AwayMap x N) (hg : IsUnit (g x)),
  (Submonoid.LocalizationMap.AwayMap.lift x F hg).comp ↑F = g
-- Mathlib.Order.Defs.Prop
Pi.hasLe : {ι : Type u_1} → {π : ι → Type u_2} → [(i : ι) → LE (π i)] → LE ((i : ι) → π i)
-- Lean.Elab.PreDefinition.Structural.Eqns
Lean.Elab.Structural.instInhabitedEqnInfo : Inhabited Lean.Elab.Structural.EqnInfo
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.Color.blue : Lean.Lsp.Color → Float
-- Mathlib.Algebra.Regular.SMul
Equiv.isSMulRegular_congr : ∀ {R : Type u_4} {S : Type u_5} {M : Type u_6} {M' : Type u_7} [inst : SMul R M] [inst_1 : SMul S M'] {e : M ≃ M'}
  {r : R} {s : S}, (∀ (x : M), e (r • x) = s • e x) → (IsSMulRegular M r ↔ IsSMulRegular M' s)
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.num.sizeOf_spec : ∀ (k : ℤ), sizeOf (Int.Internal.Linear.Poly.num k) = 1 + sizeOf k
-- Aesop.Script.Tactic
Aesop.Script.Tactic.mk.sizeOf_spec : ∀ (uTactic : Aesop.Script.UTactic) (sTactic? : Option Aesop.Script.STactic),
  sizeOf { uTactic := uTactic, sTactic? := sTactic? } = 1 + sizeOf uTactic + sizeOf sTactic?
-- Mathlib.Algebra.Homology.Factorizations.CM5b
/-- A lift of a morphism `f : K ⟶ L` between bounded below cochain complexes
as a monomorphism `K ⟶ mappingCone (𝟙 (I K)) ⊞ L`.  -/
CochainComplex.cm5b.i : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : CategoryTheory.EnoughInjectives C] →
        {K L : CochainComplex C ℤ} →
          (K ⟶ L) → (K ⟶ CochainComplex.mappingCone (CategoryTheory.CategoryStruct.id (CochainComplex.cm5b.I K)) ⊞ L)
-- Mathlib.GroupTheory.GroupAction.Hom
/-- Any type satisfying `MulDistribMulActionSemiHomClass` can be cast into `MulDistribMulActionHom`
via `MulDistribMulActionSemiHomClass.toMulDistribMulActionHom`.  -/
MulDistribMulActionHom.instCoeTCOfMulDistribMulActionSemiHomClassCoeMonoidHom : {M : Type u_1} →
  [inst : Monoid M] →
    {N : Type u_2} →
      [inst_1 : Monoid N] →
        {φ : M →* N} →
          {A : Type u_4} →
            [inst_2 : Monoid A] →
              [inst_3 : MulDistribMulAction M A] →
                {B : Type u_5} →
                  [inst_4 : Monoid B] →
                    [inst_5 : MulDistribMulAction N B] →
                      {F : Type u_10} →
                        [inst_6 : FunLike F A B] → [MulDistribMulActionSemiHomClass F (⇑φ) A B] → CoeTC F (A →ₑ*[φ] B)
-- Mathlib.AlgebraicGeometry.Stalk
AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem_ι : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens) (x : ↥X) (hxU : x ∈ U),
  CategoryTheory.CategoryStruct.comp (U.fromSpecStalkOfMem x hxU) U.ι = X.fromSpecStalk x
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.algEquivAevalXAddC_symm : ∀ {R : Type u_3} [inst : CommRing R] (t : R),
  (Polynomial.algEquivAevalXAddC t).symm = Polynomial.algEquivAevalXAddC (-t)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.forall_mem_range : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {f : MeasureTheory.SimpleFunc α β} {p : β → Prop},
  (∀ y ∈ f.range, p y) ↔ ∀ (x : α), p (f x)
-- Aesop.Rule
Aesop.instToStringNormRule : ToString Aesop.NormRule