mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.minKeyD.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : Std.DTreeMap.Internal.Impl α β → α → Sort u_3) →
      (x : Std.DTreeMap.Internal.Impl α β) →
        (x_1 : α) →
          ((fallback : α) → motive Std.DTreeMap.Internal.Impl.leaf fallback) →
            ((size : ℕ) →
                (k : α) →
                  (v : β k) →
                    (r : Std.DTreeMap.Internal.Impl α β) →
                      (x : α) →
                        motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x) →
              ((size : ℕ) →
                  (k : α) →
                    (v : β k) →
                      (size_1 : ℕ) →
                        (k_1 : α) →
                          (v_1 : β k_1) →
                            (l r r_1 : Std.DTreeMap.Internal.Impl α β) →
                              (fallback : α) →
                                motive
                                  (Std.DTreeMap.Internal.Impl.inner size k v
                                    (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1)
                                  fallback) →
                motive x x_1
-- Mathlib.Data.Rel.Separated
SetRel.IsSeparated.insert : ∀ {X : Type u_1} {R : SetRel X X} {s : Set X} {x : X} [R.IsSymm],
  R.IsSeparated s → (∀ y ∈ s, (x, y) ∈ R → x = y) → R.IsSeparated (insert x s)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
SimpleGraph.IsEdgeReachable.symm : ∀ {V : Type u_1} {G : SimpleGraph V} {k : ℕ} {u v : V}, G.IsEdgeReachable k u v → G.IsEdgeReachable k v u
-- Mathlib.Analysis.SpecialFunctions.Log.Deriv
HasFDerivAt.log : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {f' : StrongDual ℝ E},
  HasFDerivAt f f' x → f x ≠ 0 → HasFDerivAt (fun x => Real.log (f x)) ((f x)⁻¹ • f') x
-- Std.Internal.Do.PredTrans
/-- `MonadExceptOf` instance for the outermost exception layer:
`throw` invokes the head exception postcondition, `tryCatch` intercepts it.  -/
Std.Internal.Do.instMonadExceptOfPredTransConsForall : {ε : Type u} →
  {Pred : Type v} → {EPred : Type w} → MonadExceptOf ε (Std.Internal.Do.PredTrans Pred (EPost.Cons✝ (ε → Pred) EPred))
-- Lean.Parser.Attr
Lean.Parser.Attr.externEntry.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Order.Monoid.Defs
IsOrderedAddMonoid.mk : ∀ {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : Preorder α],
  (∀ (a b : α), a ≤ b → ∀ (c : α), a + c ≤ b + c) →
    (∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b) → IsOrderedAddMonoid α
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.Partial.extend.congr_simp : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] {seed : HahnEmbedding.Seed K M R}
  (f f_1 : HahnEmbedding.Partial seed) (e_f : f = f_1) [inst_12 : IsOrderedAddMonoid R] [inst_13 : Archimedean R]
  {x x_1 : M} (e_x : x = x_1) (hx : x ∉ (↑f).domain), f.extend hx = f_1.extend ⋯
-- Std.Time.Internal.Bounded
/-- Adjust the bounds of a `Bounded` by adding a constant value to the lower bounds.
 -/
Std.Time.Internal.Bounded.LE.subBottom : {n m : ℤ} → Std.Time.Internal.Bounded.LE n m → (num : ℤ) → num ≥ 0 → Std.Time.Internal.Bounded.LE (n - num) m
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.contains_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → γ} {k : α}, (Std.ExtHashMap.map f m).contains k = m.contains k
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.unique : {ι : Type u} →
  {β : ι → Type v} → [inst : (i : ι) → Zero (β i)] → [∀ (i : ι), Subsingleton (β i)] → Unique (Π₀ (i : ι), β i)
-- Batteries.Data.Vector.Lemmas
Vector.getElem?_scanl : ∀ {β : Type u_1} {α : Type u_2} {n : ℕ} {init : β} {i : ℕ} {f : β → α → β} {as : Vector α n},
  (Vector.scanl f init as)[i]? = if i ≤ n then some (Vector.foldl f init (as.take i)) else none
-- Lean.Attributes
Lean.TagAttribute.mk : Lean.AttributeImpl → Lean.PersistentEnvExtension Lean.Name Lean.Name Lean.NameSet → Lean.TagAttribute
-- Mathlib.GroupTheory.Commutator.Basic
instNormalCommutator : ∀ (G : Type u_1) [inst : Group G], (commutator G).Normal
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.toSubsemigroup_injective : ∀ {M : Type u_1} [inst : AddZeroClass M], Function.Injective AddSubmonoid.toAddSubsemigroup
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.PreSubmersivePresentation.reindex.eq_1 : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.PreSubmersivePresentation R S ι σ) {ι' : Type u_1} {σ' : Type u_2} (e : ι' ≃ ι) (f : σ' ≃ σ),
  P.reindex e f = { toPresentation := P.reindex e f, map := ⇑e.symm ∘ P.map ∘ ⇑f, map_inj := ⋯ }
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.DiseqCnstrProof.simp_suffix.inj : ∀ {lhs : Bool} {s : Lean.Grind.AC.Seq} {c₁ : Lean.Meta.Grind.AC.EqCnstr} {c₂ : Lean.Meta.Grind.AC.DiseqCnstr}
  {lhs_1 : Bool} {s_1 : Lean.Grind.AC.Seq} {c₁_1 : Lean.Meta.Grind.AC.EqCnstr} {c₂_1 : Lean.Meta.Grind.AC.DiseqCnstr},
  Lean.Meta.Grind.AC.DiseqCnstrProof.simp_suffix lhs s c₁ c₂ =
      Lean.Meta.Grind.AC.DiseqCnstrProof.simp_suffix lhs_1 s_1 c₁_1 c₂_1 →
    lhs = lhs_1 ∧ s = s_1 ∧ c₁ = c₁_1 ∧ c₂ = c₂_1
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
/-- the second morphism in the factorizations  -/
CategoryTheory.MorphismProperty.FunctorialFactorizationData.p : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W₁ W₂ : CategoryTheory.MorphismProperty C} →
      (self : W₁.FunctorialFactorizationData W₂) → self.Z ⟶ CategoryTheory.Arrow.rightFunc
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.neg_eq_self_iff_neg_subset : ∀ {α : Type u_2} [inst : InvolutiveNeg α] {s : Set α}, -s = s ↔ -s ⊆ s
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosSemidef.of_dotProduct_mulVec_nonneg : ∀ {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [inst_3 : Fintype n]
  {M : Matrix n n R}, M.IsHermitian → (∀ (x : n → R), 0 ≤ star x ⬝ᵥ M.mulVec x) → M.PosSemidef
-- Mathlib.Order.DirSupClosed
DirSupInaccOn.iUnion : ∀ {α : Type u_1} {D : Set (Set α)} [inst : Preorder α] {ι : Sort u_2} {f : ι → Set α},
  (∀ (i : ι), DirSupInaccOn D (f i)) → DirSupInaccOn D (⋃ i, f i)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
_private.Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangle_obj₃_isGE : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} 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]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (X : C),
  t.IsGE (CategoryTheory.Triangulated.TStructure.TruncAux.triangle✝ t n X).obj₃ n
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instMonoid : {α : Type u_1} → {β : Type u_2} → [inst : MeasurableSpace α] → [Monoid β] → Monoid (MeasureTheory.SimpleFunc α β)
-- Mathlib.Analysis.Distribution.DerivNotation
LineDerivAdd.lineDerivOp_add : ∀ {V : Type u} {E : Type v} {F : outParam (Type w)} {inst : AddCommGroup V} {inst_1 : AddCommGroup E}
  {inst_2 : AddCommGroup F} {inst_3 : LineDeriv V E F} [self : LineDerivAdd V E F] (v : V) (x y : E),
  LineDeriv.lineDerivOp v (x + y) = LineDeriv.lineDerivOp v x + LineDeriv.lineDerivOp v y
-- Mathlib.Dynamics.Flow
Flow.IsSemiconjugacy.mk : ∀ {τ : Type u_1} {α : Type u_2} [inst : TopologicalSpace τ] [inst_1 : TopologicalSpace α] [inst_2 : AddMonoid τ]
  {β : Type u_3} [inst_3 : TopologicalSpace β] {π : α → β} {ϕ : Flow τ α} {ψ : Flow τ β},
  Continuous π →
    Function.Surjective π → (∀ (t : τ), Function.Semiconj π (ϕ.toFun t) (ψ.toFun t)) → Flow.IsSemiconjugacy π ϕ ψ
-- Mathlib.Order.LiminfLimsup
Filter.limsInf_le_limsSup : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {f : Filter α} [f.NeBot],
  autoParam (Filter.IsBounded (fun x1 x2 => x1 ≤ x2) f) Filter.limsInf_le_limsSup._auto_1 →
    autoParam (Filter.IsBounded (fun x1 x2 => x1 ≥ x2) f) Filter.limsInf_le_limsSup._auto_3 → f.limsInf ≤ f.limsSup
-- Lean.Data.PersistentHashSet
Lean.PersistentHashSet.empty : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → Lean.PersistentHashSet α
-- Init.Grind.ToInt
Lean.Grind.IntInterval.isFinite.eq_3 : ∀ (hi : ℤ), (Lean.Grind.IntInterval.io hi).isFinite = false
-- Mathlib.Geometry.RingedSpace.Stalks
/-- An isomorphism between presheafed spaces induces an isomorphism of stalks.
 -/
AlgebraicGeometry.PresheafedSpace.stalkMap.stalkIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasColimits C] →
      {X Y : AlgebraicGeometry.PresheafedSpace C} →
        (α : X ≅ Y) →
          (x : ↑↑X) → Y.presheaf.stalk ((CategoryTheory.ConcreteCategory.hom α.hom.base) x) ≅ X.presheaf.stalk x
-- Mathlib.Algebra.Group.Subgroup.Even
Subgroup.mem_square : ∀ {G : Type u_1} [inst : CommGroup G] {a : G}, a ∈ Subgroup.square G ↔ IsSquare a
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.Functor.isContinuous_of_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F₁ F₂ : CategoryTheory.Functor C D} (e : F₁ ≅ F₂) (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) [F₁.IsContinuous J K], F₂.IsContinuous J K
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
/-- The middle right map in the oplax associativity hexagon.
 -/
CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.secondMap₂ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F : CategoryTheory.Functor C D} →
              (CategoryTheory.MonoidalCategory.curriedTensorPost F ⟶
                  CategoryTheory.MonoidalCategory.curriedTensorPre F) →
                (CategoryTheory.MonoidalCategory.curriedTensorPostPost' F ⟶
                  CategoryTheory.MonoidalCategory.curriedTensorPrePost F)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.congr_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Std.TreeMap α β cmp},
  t₁.Equiv t₂ → (t₃.Equiv t₁ ↔ t₃.Equiv t₂)
-- Lean.MetavarContext
/-- Set the `BinderInfo` of an fvar. If the given metavariable is not declared or
the given fvar doesn't exist in its context, the `MetavarContext` is returned
unchanged.
 -/
Lean.MetavarContext.setFVarBinderInfo : Lean.MetavarContext → Lean.MVarId → Lean.FVarId → Lean.BinderInfo → Lean.MetavarContext
-- Mathlib.Algebra.GroupWithZero.Units.Basic
IsUnit.mk0 : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] (x : G₀), x ≠ 0 → IsUnit x
-- Mathlib.Algebra.Module.Submodule.Ker
/-- **Alias** of `LinearMap.injective_restrict_iff`. -/
LinearMap.injective_restrict_iff_disjoint : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [inst : Ring R] [inst_1 : Ring R₂]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  {p : Submodule R M} {q : Submodule R₂ M₂} {f : M →ₛₗ[τ₁₂] M₂} (hf : ∀ x ∈ p, f x ∈ q),
  Function.Injective ⇑(f.restrict hf) ↔ Disjoint p f.ker
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.natGeneratingSequence.eq_1 : ∀ (α : Type u_3) [inst : MeasurableSpace α] [inst_1 : MeasurableSpace.CountablyGenerated α],
  MeasurableSpace.natGeneratingSequence α = Set.enumerateCountable ⋯ ∅
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.coe_mul_eq_smul : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} (r : R) (a : QuaternionAlgebra R c₁ c₂ c₃) [inst : CommRing R], ↑r * a = r • a
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
covariant_flip_iff : ∀ (N : Type u_2) (r : N → N → Prop) (mu : N → N → N) [h : Std.Commutative mu],
  Covariant N N (flip mu) r ↔ Covariant N N mu r
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
/-- The objects of the free simplex quiver are the natural numbers.  -/
FreeSimplexQuiver : Type
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.HasRightHomology.of_zeros : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (X Y Z : C), { X₁ := X, X₂ := Y, X₃ := Z, f := 0, g := 0, zero := ⋯ }.HasRightHomology
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
add_neg_nonpos_iff : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddRightMono α] {a b : α}, b + -a ≤ 0 ↔ b ≤ a
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.integral_eq_setIntegral : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {s : Set X} {μ : MeasureTheory.Measure X},
  (∀ᵐ (x : X) ∂μ, x ∈ s) → ∀ (f : X → E), ∫ (x : X), f x ∂μ = ∫ (x : X) in s, f x ∂μ
-- Mathlib.AlgebraicGeometry.Cover.Open
AlgebraicGeometry.Scheme.affineOpenCover_I₀ : ∀ (X : AlgebraicGeometry.Scheme), X.affineOpenCover.I₀ = X.affineCover.I₀
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsLoop.isLoop_isRestriction : ∀ {α : Type u_1} {M N : Matroid α} {e : α}, M.IsLoop e → N.IsRestriction M → e ∈ N.E → N.IsLoop e
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.lift_single : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Monoid M] (F : M →* A) (a : M) (b : R), ((MonoidAlgebra.lift R A M) F) (MonoidAlgebra.single a b) = b • F a
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.exists_ne_zero_of_nontrivial : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) [Nontrivial ↥H], ∃ x ∈ H, x ≠ 0
-- Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
integral_withDensity_eq_integral_toReal_smul₀ : ∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {f : X → ENNReal},
  AEMeasurable f μ →
    (∀ᵐ (x : X) ∂μ, f x < ⊤) → ∀ (g : X → E), ∫ (x : X), g x ∂μ.withDensity f = ∫ (x : X), (f x).toReal • g x ∂μ
-- Init.Data.Array.Range
Array.map_sub_range' : ∀ {step a s : ℕ}, a ≤ s → ∀ (n : ℕ), Array.map (fun x => x - a) (Array.range' s n step) = Array.range' (s - a) n step
-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.SplitInclusiveIterator.toOption : {ρ : Type} →
  {σ : String.Slice → Type} →
    {pat : ρ} →
      [inst : String.Slice.Pattern.ToForwardSearcher pat σ] →
        {s : String.Slice} →
          String.Slice.SplitInclusiveIterator pat s → Option (Std.Iter (String.Slice.Pattern.SearchStep s))
-- Mathlib.Analysis.Normed.Operator.Compact.Basic
isCompactOperator_iff_image_ball_subset_compact : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NontriviallyNormedField 𝕜₁] [inst_1 : SeminormedRing 𝕜₂] {σ₁₂ : 𝕜₁ →+* 𝕜₂}
  {M₁ : Type u_3} {M₂ : Type u_4} [inst_2 : SeminormedAddCommGroup M₁] [inst_3 : TopologicalSpace M₂]
  [inst_4 : AddCommMonoid M₂] [inst_5 : NormedSpace 𝕜₁ M₁] [inst_6 : Module 𝕜₂ M₂] [ContinuousConstSMul 𝕜₂ M₂]
  (f : M₁ →ₛₗ[σ₁₂] M₂) {r : ℝ}, 0 < r → (IsCompactOperator ⇑f ↔ ∃ K, IsCompact K ∧ ⇑f '' Metric.ball 0 r ⊆ K)
-- Mathlib.Data.Finset.Card
Finset.eq_of_superset_of_card_ge : ∀ {α : Type u_1} {s t : Finset α}, s ⊆ t → t.card ≤ s.card → t = s
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal.ext_iff : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}}
  {D₁ D₂ : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal J κ},
  D₁ = D₂ ↔ D₁.W = D₂.W ∧ D₁.P = D₂.P
-- Batteries.Recycling.RBTree.Basic
/-- `O(n * log n)`. Map a function on every value in the set.
If the function is monotone, consider using the more efficient `RBSet.mapMonotone` instead.
 -/
RBTree.RBSet.map : {α : Type u_1} →
  {cmpα : α → α → Ordering} →
    {β : Type u_2} → {cmpβ : β → β → Ordering} → RBTree.RBSet α cmpα → (α → β) → RBTree.RBSet β cmpβ
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PushoutObjObj.flip_inl : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂}
  (sq : F.PushoutObjObj f₁ f₂), sq.flip.inl = sq.inr
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
LinearIndependent.pair_add_left_iff : ∀ {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {x y : M},
  LinearIndependent R ![x + y, y] ↔ LinearIndependent R ![x, y]
-- Mathlib.CategoryTheory.Limits.FunctorCategory.BinaryBiproducts
/-- If `C` has binary biproducts, then the functor category `D ⥤ C` does too.  -/
CategoryTheory.Limits.functorCategoryHasBinaryBiproducts : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u_2} [inst_3 : CategoryTheory.Category.{v_2, u_2} D],
  CategoryTheory.Limits.HasBinaryBiproducts (CategoryTheory.Functor D C)
-- Mathlib.Computability.Primrec.Basic
Primrec.map_decode_iff : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable σ]
  {f : α → β → σ}, (Primrec₂ fun a n => Option.map (f a) (Encodable.decode n)) ↔ Primrec₂ f
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKey?_modify_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α} {f : β → β}, (Std.DHashMap.Const.modify m k f).getKey? k = if k ∈ m then some k else none
-- Mathlib.Algebra.Homology.SpectralObject.Homology
CategoryTheory.Abelian.SpectralObject.dCokernelSequence.congr_simp : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] (X X_1 : CategoryTheory.Abelian.SpectralObject C ι),
  X = X_1 →
    ∀ {i₀ i₁ i₂ i₃ i₄ i₅ : ι} (f₁ f₁_1 : i₀ ⟶ i₁),
      f₁ = f₁_1 →
        ∀ (f₂ f₂_1 : i₁ ⟶ i₂),
          f₂ = f₂_1 →
            ∀ (f₃ f₃_1 : i₂ ⟶ i₃) (e_f₃ : f₃ = f₃_1) (f₄ f₄_1 : i₃ ⟶ i₄) (e_f₄ : f₄ = f₄_1) (f₅ f₅_1 : i₄ ⟶ i₅),
              f₅ = f₅_1 →
                ∀ (f₃₄ f₃₄_1 : i₂ ⟶ i₄) (e_f₃₄ : f₃₄ = f₃₄_1) (h₃₄ : CategoryTheory.CategoryStruct.comp f₃ f₄ = f₃₄)
                  (n₀ n₀_1 : ℤ) (e_n₀ : n₀ = n₀_1) (n₁ n₁_1 : ℤ) (e_n₁ : n₁ = n₁_1) (n₂ n₂_1 : ℤ) (e_n₂ : n₂ = n₂_1)
                  (n₃ n₃_1 : ℤ) (e_n₃ : n₃ = n₃_1) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) (hn₃ : n₂ + 1 = n₃),
                  X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ =
                    X_1.dCokernelSequence f₁_1 f₂_1 f₃_1 f₄_1 f₅_1 f₃₄_1 ⋯ n₀_1 n₁_1 n₂_1 n₃_1 ⋯ ⋯ ⋯
-- Mathlib.Data.Rat.Cast.Defs
Rat.cast_ofNat : ∀ {α : Type u_3} [inst : DivisionRing α] (n : ℕ) [inst_1 : n.AtLeastTwo], ↑(OfNat.ofNat n) = OfNat.ofNat n
-- Init.Data.List.Lemmas
List.idRun_foldrM : ∀ {α : Type u_1} {β : Type u_2} {f : α → β → Id β} {b : β} {l : List α},
  (List.foldrM f b l).run = List.foldr (fun x1 x2 => (f x1 x2).run) b l
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.preBeth_zero : Cardinal.preBeth 0 = 0
-- Mathlib.Topology.EMetricSpace.PairReduction
PairReduction.radius_logSizeBallSeq_le : ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ENNReal} {n : ℕ} {J : Finset T} [inst_1 : DecidableEq T]
  (hJ : J.Nonempty), 1 < a → 1 ≤ n → ↑J.card ≤ a ^ n → ∀ (i : ℕ), (PairReduction.logSizeBallSeq J hJ a c i).radius ≤ n
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.Functor.additive_iff_of_iso : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D] {F G : CategoryTheory.Functor C D} (e : F ≅ G), F.Additive ↔ G.Additive
-- Mathlib.Data.Matrix.Basis
Matrix.sum_sum_single : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_7} [inst : DecidableEq m] [inst_1 : DecidableEq n]
  [inst_2 : AddCommMonoid α] [inst_3 : Fintype m] [inst_4 : Fintype n] (x : m → n → α),
  ∑ i, ∑ j, Matrix.single i j (x i j) = Matrix.of x
-- Mathlib.Topology.Algebra.Ring.Basic
/-- The order embedding from ring topologies on `a` to additive group topologies on `a`.  -/
RingTopology.toAddGroupTopology.orderEmbedding : {R : Type u_1} → [inst : Ring R] → RingTopology R ↪o AddGroupTopology R
-- Lean.Data.JsonRpc
/-- Generic version of `Message.response`.

A Response Message sent as a result of a request. If a request doesn’t provide a
result value the receiver of a request still needs to return a response message
to conform to the JSON-RPC specification. The result property of the ResponseMessage
should be set to null in this case to signal a successful request.

References:
- [JSON-RPC](https://www.jsonrpc.org/specification#response_object)
- [LSP](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#responseMessage)
 -/
Lean.JsonRpc.Response : Type u → Type u
-- Mathlib.RingTheory.Smooth.Basic
Algebra.FormallySmooth.subsingleton_h1Cotangent : ∀ {R : Type u} {A : Type v} {inst : CommRing R} {inst_1 : CommRing A} {inst_2 : Algebra R A}
  [self : Algebra.FormallySmooth R A], Subsingleton (Algebra.H1Cotangent R A)
-- Mathlib.Probability.Kernel.Disintegration.CondCDF
MeasureTheory.Measure.IicSnd_apply : ∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (r : ℝ) {s : Set α},
  MeasurableSet s → (ρ.IicSnd r) s = ρ (s ×ˢ Set.Iic r)
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Iic_union_Ioi : ∀ {α : Type u_1} [inst : LinearOrder α] {a : α}, Set.Iic a ∪ Set.Ioi a = Set.univ
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.natCast_fin_three : ∀ {α : Type u} [inst : AddMonoidWithOne α] (n : ℕ), ↑n = !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n]
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Step.done.injEq : ∀ (r r_1 : Lean.Meta.Simp.Result), (Lean.Meta.Simp.Step.done r = Lean.Meta.Simp.Step.done r_1) = (r = r_1)
-- Mathlib.Analysis.RCLike.Basic
RCLike.mul_im_ax : ∀ {K : semiOutParam (Type u_1)} [self : RCLike K] (z w : K),
  RCLike.im (z * w) = RCLike.re z * RCLike.im w + RCLike.im z * RCLike.re w
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
CategoryTheory.GrothendieckTopology.sheafifyMap_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q R : CategoryTheory.Functor Cᵒᵖ D}
  (η : P ⟶ Q) (γ : Q ⟶ R),
  J.sheafifyMap (CategoryTheory.CategoryStruct.comp η γ) =
    CategoryTheory.CategoryStruct.comp (J.sheafifyMap η) (J.sheafifyMap γ)
-- Mathlib.Order.RelSeries
/-- If a series `a₀ -r→ a₁ -r→ ...` has positive length, then `a₁ -r→ ...` is another series
 -/
RelSeries.tail : {α : Type u_1} → {r : SetRel α α} → (p : RelSeries r) → p.length ≠ 0 → RelSeries r
-- Mathlib.Analysis.Calculus.ContDiff.Operations
ContDiffAt.div : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {f g : E → 𝕜} {n : WithTop ℕ∞},
  ContDiffAt 𝕜 n f x → ContDiffAt 𝕜 n g x → g x ≠ 0 → ContDiffAt 𝕜 n (f / g) x