mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.ReflexiveCofork.π.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C}
  (G : CategoryTheory.Limits.ReflexiveCofork F), G.π = G.ι.app CategoryTheory.Limits.WalkingReflexivePair.zero
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.ext_from : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] (i j : ℤ) (hij : j + 1 = i)
  {A : C} {f g : (CochainComplex.mappingCone φ).X j ⟶ A},
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inl φ).v i j ⋯) f =
      CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inl φ).v i j ⋯) g →
    CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr φ).f j) f =
        CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr φ).f j) g →
      f = g
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.preAleph_univ : Cardinal.preAleph Ordinal.univ.{u, v} = Cardinal.univ.{u, v}
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
/-- For `z : ℂ` the function `d : ℤ ↦ ((c z + d) ^ k)⁻¹` is Summable for `2 ≤ k`.  -/
EisensteinSeries.linear_right_summable : ∀ (z : ℂ) (c : ℤ) {k : ℤ}, 2 ≤ k → Summable fun d => ((↑c * z + ↑d) ^ k)⁻¹
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.isoCocycles₁_hom_comp_i_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (x : ↑(groupCohomology.cocycles A 1)),
  (ModuleCat.Hom.hom (groupCohomology.shortComplexH1 A).g).ker.subtype
      ((CategoryTheory.ConcreteCategory.hom (groupCohomology.isoCocycles₁ A).hom) x) =
    (CategoryTheory.ConcreteCategory.hom (groupCohomology.cochainsIso₁ A).hom)
      ((CategoryTheory.ConcreteCategory.hom (groupCohomology.iCocycles A 1)) x)
-- Lean.Elab.Tactic.Basic
Lean.Elab.Tactic.mkTacticInfo : Lean.MetavarContext → List Lean.MVarId → Lean.Syntax → Lean.Elab.Tactic.TacticM Lean.Elab.Info
-- Lean.Data.FuzzyMatching
_private.Lean.Data.FuzzyMatching.0.Lean.FuzzyMatching.Score.map : Lean.FuzzyMatching.Score✝ → (Int16 → Int16) → Lean.FuzzyMatching.Score✝
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.mk_seq : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis}
  (s : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl) (f : ℝ → ℝ),
  (Tactic.ComputeAsymptotics.MultiseriesExpansion.mk s f).seq = s
-- Mathlib.LinearAlgebra.TensorProduct.Basis
/-- Given a basis `𝒞` of `N`, `x ∈ M ⊗ N` can be written as `∑ᵢ mᵢ ⊗ 𝒞 i`. The coefficient `mᵢ`
equals the `i`-th coordinate functional applied to the right tensor factor.  -/
TensorProduct.equivFinsuppOfBasisRight_apply : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} {κ : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : DecidableEq κ]
  (𝒞 : Module.Basis κ R N) (x : TensorProduct R M N) (i : κ),
  ((TensorProduct.equivFinsuppOfBasisRight 𝒞) x) i = (TensorProduct.rid R M) ((LinearMap.lTensor M (𝒞.coord i)) x)
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKeyD_eraseKey_eq_iff_beq_maxKeyD_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k fallback : α},
      (Std.Internal.List.eraseKey k l).isEmpty = false →
        (Std.Internal.List.maxKeyD (Std.Internal.List.eraseKey k l) fallback = Std.Internal.List.maxKeyD l fallback ↔
          (k == Std.Internal.List.maxKeyD l fallback) = false)
-- Mathlib.CategoryTheory.Limits.IndYoneda
CategoryTheory.Limits.colimitCoyonedaHomIsoLimitUnop_π_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [inst_1 : CategoryTheory.Category.{v₂, v₁} I]
  (D : CategoryTheory.Functor Iᵒᵖ Cᵒᵖ) (F : CategoryTheory.Functor C (Type u₂))
  [inst_2 : CategoryTheory.Limits.HasColimit (D.comp CategoryTheory.coyoneda)]
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape I (Type (max u₁ u₂))]
  (f : CategoryTheory.Limits.colimit (D.comp CategoryTheory.coyoneda) ⟶ F) (i : I),
  (CategoryTheory.ConcreteCategory.hom
        (CategoryTheory.Limits.limit.π (D.unop.comp (F.comp CategoryTheory.uliftFunctor.{u₁, u₂})) i))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimitCoyonedaHomIsoLimitUnop D F).hom) f) =
    {
      down :=
        (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.unop (D.obj (Opposite.op i)))))
          ((CategoryTheory.ConcreteCategory.hom
              ((CategoryTheory.Limits.colimit.ι (D.comp CategoryTheory.coyoneda) (Opposite.op i)).app
                (Opposite.unop (D.obj (Opposite.op i)))))
            (CategoryTheory.CategoryStruct.id (Opposite.unop (D.obj (Opposite.op i))))) }
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.curryingEquiv_apply_obj : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (X : C × D),
  (CategoryTheory.Functor.curryingEquiv F).obj X = (F.obj X.1).obj X.2
-- Mathlib.Order.Filter.AtTopBot.Group
Filter.tendsto_neg_atBot_iff : ∀ {α : Type u_1} {G : Type u_2} [inst : AddCommGroup G] [inst_1 : PartialOrder G] [IsOrderedAddMonoid G] {l : Filter α}
  {f : α → G}, Filter.Tendsto (fun x => -f x) l Filter.atBot ↔ Filter.Tendsto f l Filter.atTop
-- Mathlib.Combinatorics.Schnirelmann
/-- The Schnirelmann density of a set not containing `1` is `0`.  -/
schnirelmannDensity_eq_zero_of_one_notMem : ∀ {A : Set ℕ} [inst : DecidablePred fun x => x ∈ A], 1 ∉ A → schnirelmannDensity A = 0
-- Mathlib.Order.SuccPred.WithBot
/-- Not to be confused with `WithBot.orderSucc_coe`, which is about `Order.succ`.  -/
WithBot.succ_coe : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderBot α] [inst_2 : SuccOrder α] (a : α), (↑a).succ = Order.succ a
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
SheafOfModules.hom_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} {X Y : SheafOfModules R} {f g : X ⟶ Y}, f.val = g.val → f = g
-- Mathlib.Order.Lattice
inf_lt_iff : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, min b c < a ↔ b < a ∨ c < a
-- Lean.Meta.RecursorInfo
Lean.Meta.RecursorInfo.majorPos : Lean.Meta.RecursorInfo → ℕ
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.rightUnitor_hom_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X : C}
  (Y : CategoryTheory.Over X),
  CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).hom =
    CategoryTheory.Limits.pullback.fst Y.hom (CategoryTheory.CategoryStruct.id X)
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.distribBaseChange_symm_tmul : ∀ (R : Type uR) (A : Type uA) {N : Type uN} {Q : Type uQ} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : AddCommMonoid Q]
  [inst_6 : Module R Q] (n : N) (q : Q) (a b : A),
  (TensorProduct.AlgebraTensorModule.distribBaseChange R A N Q).symm (a ⊗ₜ[R] n ⊗ₜ[A] (b ⊗ₜ[R] q)) =
    (a * b) ⊗ₜ[R] (n ⊗ₜ[R] q)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- The right unitor isomorphism for binary products with the terminal object.  -/
CategoryTheory.Limits.prod.rightUnitor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasTerminal C] →
      (P : C) → [inst_2 : CategoryTheory.Limits.HasBinaryProduct P (⊤_ C)] → P ⨯ ⊤_ C ≅ P
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.grothendieckTypeToCat_inverse_obj_fiber_as : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) (X : G.Elements),
  ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).inverse.obj X).fiber.as = X.snd
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.iCondIndepFun.indepFun_mul_mul : ∀ {Ω : Type u_1} {ι : Type u_2} {β : Type u_3} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {m : MeasurableSpace β} [inst_2 : Mul β]
  [MeasurableMul₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iCondIndepFun m' hm' f μ →
    (∀ (i : ι), Measurable (f i)) →
      ∀ (i j k l : ι), i ≠ k → i ≠ l → j ≠ k → j ≠ l → ProbabilityTheory.CondIndepFun m' hm' (f i * f j) (f k * f l) μ
-- Mathlib.Logic.Function.Basic
/-- **Alias** of `Std.Symm.forall_existsUnique_iff'`.

---

A symmetric relation `r : α → α → Prop` is "function-like"
(for each `a` there exists a unique `b` such that `r a b`)
if and only if it is `(f · = ·)` for some involutive function `f`.  -/
Symmetric.forall_existsUnique_iff' : ∀ {α : Sort u_1} {r : α → α → Prop} [Std.Symm r],
  (∀ (a : α), ∃! b, r a b) ↔ ∃ f, Function.Involutive f ∧ r = fun x1 x2 => f x1 = x2
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctor.map_comp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.StrictPseudofunctor B C) {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  self.map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (self.map f) (self.map g)
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.coe_subtype : ∀ {M : Type u_4} [inst : MulOneClass M] (S : Submonoid M), ⇑S.subtype = Subtype.val
-- Mathlib.Data.Finset.SDiff
Finset.sdiff_union_of_subset : ∀ {α : Type u_1} [inst : DecidableEq α] {s₁ s₂ : Finset α}, s₁ ⊆ s₂ → s₂ \ s₁ ∪ s₁ = s₂
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.WalkingMulticospan.Hom.id : {J : CategoryTheory.Limits.MulticospanShape} → (A : CategoryTheory.Limits.WalkingMulticospan J) → A.Hom A
-- Mathlib.CategoryTheory.Join.Final
CategoryTheory.Join.instFinalInclRightOfIsConnected : ∀ (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] [CategoryTheory.IsConnected D],
  (CategoryTheory.Join.inclRight C D).Final
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExProd.brecOn.go : {u : Lean.Level} →
  {α : Q(Type u)} →
    {BaseType : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} →
        {motive_1 : (e : Q(«$α»)) → Mathlib.Tactic.Ring.Common.ExBase BaseType sα e → Sort u} →
          {motive_2 : (e : Q(«$α»)) → Mathlib.Tactic.Ring.Common.ExProd BaseType sα e → Sort u} →
            {motive_3 : (e : Q(«$α»)) → Mathlib.Tactic.Ring.Common.ExSum BaseType sα e → Sort u} →
              {e : Q(«$α»)} →
                (t : Mathlib.Tactic.Ring.Common.ExProd BaseType sα e) →
                  ((e : Q(«$α»)) → (t : Mathlib.Tactic.Ring.Common.ExBase BaseType sα e) → t.below → motive_1 e t) →
                    ((e : Q(«$α»)) → (t : Mathlib.Tactic.Ring.Common.ExProd BaseType sα e) → t.below → motive_2 e t) →
                      ((e : Q(«$α»)) → (t : Mathlib.Tactic.Ring.Common.ExSum BaseType sα e) → t.below → motive_3 e t) →
                        motive_2 e t ×' t.below
-- Mathlib.Algebra.BigOperators.Intervals
Finset.prod_Ico_eq_mul_inv : ∀ {δ : Type u_4} [inst : CommGroup δ] (f : ℕ → δ) {m n : ℕ},
  m ≤ n → ∏ k ∈ Finset.Ico m n, f k = (∏ k ∈ Finset.range n, f k) * (∏ k ∈ Finset.range m, f k)⁻¹
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
/-- Eta-expanded form of `MeasureTheory.Integrable.add` -/
MeasureTheory.Integrable.fun_add : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε' : Type u_8} [inst : TopologicalSpace ε']
  [inst_1 : ESeminormedAddMonoid ε'] [ContinuousAdd ε'] {f g : α → ε'},
  MeasureTheory.Integrable f μ → MeasureTheory.Integrable g μ → MeasureTheory.Integrable (fun i => f i + g i) μ
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Γ_map_op : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.Scheme.Γ.map f.op = AlgebraicGeometry.Scheme.Hom.appTop f
-- Lean.Meta.DiscrTree.Types
Lean.Meta.DiscrTree.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (root : Lean.PersistentHashMap Lean.Meta.DiscrTree.Key (Lean.Meta.DiscrTree.Trie α)),
  sizeOf { root := root } = 1 + sizeOf root
-- Init.Data.BitVec.Lemmas
BitVec.smtSDiv_eq : ∀ {w : ℕ} (x y : BitVec w),
  x.smtSDiv y =
    match x.msb, y.msb with
    | false, false => x.smtUDiv y
    | false, true => -x.smtUDiv (-y)
    | true, false => -(-x).smtUDiv y
    | true, true => (-x).smtUDiv (-y)
-- Mathlib.Analysis.BoxIntegral.Partition.Split
BoxIntegral.Box.splitLower_ne_splitUpper : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι) (i : ι) (x : ℝ), I.splitLower i x ≠ I.splitUpper i x
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mk_embedding_eq_zero_iff_lift_lt : ∀ {α : Type u} {β' : Type v},
  Cardinal.mk (α ↪ β') = 0 ↔ Cardinal.lift.{u, v} (Cardinal.mk β') < Cardinal.lift.{v, u} (Cardinal.mk α)
-- Mathlib.Topology.Order.ScottTopology
Topology.scott.eq_1 : ∀ (α : Type u_3) (D : Set (Set α)) [inst : Preorder α],
  Topology.scott α D = Topology.upperSet α ⊔ Topology.scottHausdorff α D
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.symm_trans_self : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_8} {M₂ : Type u_9} [inst : Semiring R₁] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M₁] [inst_3 : AddCommMonoid M₂] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂}
  {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂}
  (f : M₁ ≃ₛₗ[σ₁₂] M₂), f.symm.trans f = LinearEquiv.refl R₂ M₂
-- Mathlib.GroupTheory.Submonoid.Inverses
/-- The additive submonoid of pointwise additive inverse of `S`
is `AddEquiv` to `S`.  -/
AddSubmonoid.leftNegEquiv : {M : Type u_1} → [inst : AddCommMonoid M] → (S : AddSubmonoid M) → S ≤ IsAddUnit.addSubmonoid M → ↥S.leftNeg ≃+ ↥S
-- Mathlib.Topology.Compactness.Compact
/-- **Tychonoff's theorem** formulated in terms of filters: `Filter.cocompact` on an indexed product
type `Π d, X d` the `Filter.coprodᵢ` of filters `Filter.cocompact` on `X d`.  -/
Filter.coprodᵢ_cocompact : ∀ {ι : Type u_1} {X : ι → Type u_3} [inst : (d : ι) → TopologicalSpace (X d)],
  (Filter.coprodᵢ fun d => Filter.cocompact (X d)) = Filter.cocompact ((d : ι) → X d)
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Set.measurable_restrict_apply : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace γ] (s : Set α) {f : α → γ},
  Measurable f → Measurable (s.domRestrict f)
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
/-- The region between two measurable functions on a measurable set is measurable.  -/
measurableSet_regionBetween : ∀ {α : Type u_1} [inst : MeasurableSpace α] {f g : α → ℝ} {s : Set α},
  Measurable f → Measurable g → MeasurableSet s → MeasurableSet (regionBetween f g s)
-- Mathlib.Order.Disjoint
isComplemented_bot : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : BoundedOrder α], IsComplemented ⊥
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.baseChange_addY : ∀ {R : Type r} {S : Type s} {A : Type u} {B : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing A]
  [inst_3 : CommRing B] {W' : WeierstrassCurve.Jacobian R} [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  (f : A →ₐ[S] B) (P Q : Fin 3 → A), (W'.baseChange B).addY (⇑f ∘ P) (⇑f ∘ Q) = f ((W'.baseChange A).addY P Q)
-- Init.Data.Slice.List.Iterator
List.instReprListSlice : {α : Type u} → [Repr α] → Repr (ListSlice α)
-- Mathlib.RingTheory.WittVector.Basic
WittVector.map_injective : ∀ {p : ℕ} {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Fact (Nat.Prime p)]
  (f : R →+* S), Function.Injective ⇑f → Function.Injective ⇑(WittVector.map f)
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
SSet.horn₃₂.desc.multicofork_π_zero : ∀ {X : SSet} (f₀ f₁ f₃ : SSet.stdSimplex.obj { len := 2 } ⟶ X)
  (h₀₂ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₁ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 1) f₃)
  (h₁₂ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₃)
  (h₂₃ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₁),
  (SSet.horn₃₂.desc.multicofork f₀ f₁ f₃ h₀₂ h₁₂ h₂₃).π ⟨0, SSet.horn₃₂.desc.multicofork_π_zero._proof_1⟩ =
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.faceSingletonComplIso 0).inv f₀
-- Mathlib.Tactic.DefEqTransformations
_private.Mathlib.Tactic.DefEqTransformations.0.Mathlib.Tactic.etaExpandAll.expandSubterms : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.RingTheory.SimpleModule.Basic
instIsSemisimpleModuleFinsupp : ∀ {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] (ι : Type u_6)
  [IsSemisimpleModule R M], IsSemisimpleModule R (ι →₀ M)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
one_div_nonneg : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀}, 0 ≤ 1 / a ↔ 0 ≤ a
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
/-- Absolute values from a nontrivial `R` to a linear ordered ring preserve `*`, `0` and `1`.  -/
AbsoluteValue.toMonoidWithZeroHom : {R : Type u_5} →
  {S : Type u_6} →
    [inst : Semiring R] →
      [inst_1 : Semiring S] → [inst_2 : PartialOrder S] → AbsoluteValue R S → [IsDomain S] → [Nontrivial R] → R →*₀ S
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
/-- Given a left homology map data for morphism `φ`, this is the induced left homology
map data for `-φ`.  -/
CategoryTheory.ShortComplex.LeftHomologyMapData.neg : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        {φ : S₁ ⟶ S₂} →
          {h₁ : S₁.LeftHomologyData} →
            {h₂ : S₂.LeftHomologyData} →
              CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂ →
                CategoryTheory.ShortComplex.LeftHomologyMapData (-φ) h₁ h₂
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.IsRatCondKernelCDFAux.mono : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β} {f : α × β → ℚ → ℝ},
  ProbabilityTheory.IsRatCondKernelCDFAux f κ ν → ∀ (a : α), ∀ᵐ (c : β) ∂ν a, Monotone (f (a, c))
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.takeWhile.go.eq_def : ∀ {α : Type u} (p : α → Bool) (as : Array α) (i : ℕ) (acc : Array α),
  Array.takeWhile.go✝ p as i acc =
    if h : i < as.size then
      have a := as[i];
      if p a = true then Array.takeWhile.go✝ p as (i + 1) (acc.push a) else acc
    else acc
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim
/-- Assume that `φ : X₁ ⟶ X₂` is a natural transformation in `J ⥤ C` which
consists of epimorphisms, then if `f : c₁.pt ⟶ c₂.pt` is a morphism
between the points of cocones `c₁` and `c₂` for `X₁` and `X₂`, in such
a way that `c₂` is colimit and `f` is compatible with `φ`, then `f` is an epimorphism.  -/
CategoryTheory.Limits.colim.map_epi' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} J]
  {X₁ X₂ : CategoryTheory.Functor J C} (φ : X₁ ⟶ X₂) [∀ (j : J), CategoryTheory.Epi (φ.app j)]
  (c₁ : CategoryTheory.Limits.Cocone X₁) {c₂ : CategoryTheory.Limits.Cocone X₂}
  (hc₂ : CategoryTheory.Limits.IsColimit c₂) (f : c₁.pt ⟶ c₂.pt),
  (∀ (j : J),
      CategoryTheory.CategoryStruct.comp (c₁.ι.app j) f = CategoryTheory.CategoryStruct.comp (φ.app j) (c₂.ι.app j)) →
    CategoryTheory.Epi f
-- Mathlib.LinearAlgebra.Projection
/-- **Alias** of `LinearMap.ofIsCompl_apply_right`. -/
LinearMap.ofIsCompl_right_apply : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_3}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] {p q : Submodule R E} (h : IsCompl p q) {φ : ↥p →ₗ[R] F}
  {ψ : ↥q →ₗ[R] F} (v : ↥q), (LinearMap.ofIsCompl h φ ψ) ↑v = ψ v
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
CliffordAlgebra.contractRight_eq : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (d : Module.Dual R M) (x : CliffordAlgebra Q),
  (CliffordAlgebra.contractRight x) d =
    CliffordAlgebra.reverse ((CliffordAlgebra.contractLeft d) (CliffordAlgebra.reverse x))
-- Batteries.Data.List.Basic
/-- `fillNones xs ys` replaces the `none`s in `xs` with elements of `ys`. If there
are not enough `ys` to replace all the `none`s, the remaining `none`s are
dropped from `xs`.
```
fillNones [none, some 1, none, none] [2, 3] = [2, 1, 3]
```
 -/
List.fillNones : {α : Type u_1} → List (Option α) → List α → List α
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.ReflectsColimitsOfShape.reflectsColimit : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {J : Type w} {inst_2 : CategoryTheory.Category.{w', w} J} {F : CategoryTheory.Functor C D}
  [self : CategoryTheory.Limits.ReflectsColimitsOfShape J F] {K : CategoryTheory.Functor J C},
  CategoryTheory.Limits.ReflectsColimit K F
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.mul_inv_cancel_right_of_invertible : ∀ {m : Type u} {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α]
  (A : Matrix n n α) (B : Matrix m n α) [Invertible A], B * A * A⁻¹ = B
-- Mathlib.MeasureTheory.Measure.Restrict
/-- If two measures agree on all measurable subsets of `s` and `t`, then they agree on all
measurable subsets of `s ∪ t`.  -/
MeasureTheory.Measure.restrict_union_congr : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {s t : Set α},
  μ.restrict (s ∪ t) = ν.restrict (s ∪ t) ↔ μ.restrict s = ν.restrict s ∧ μ.restrict t = ν.restrict t
-- Init.Data.BitVec.Lemmas
BitVec.ofInt.eq_1 : ∀ (n : ℕ) (i : ℤ), BitVec.ofInt n i = (i % Int.ofNat (2 ^ n)).toNat#'⋯
-- Mathlib.Data.Matrix.ColumnRowPartitioned
/-- Multiplication of a matrix by its inverse is commutative.
This is the column and row partitioned matrix form of `Matrix.mul_eq_one_comm`.

The condition `e : n ≃ n₁ ⊕ n₂` states that `fromCols A₁ A₂` and `fromRows B₁ B₂` are "square".
 -/
Matrix.fromCols_mul_fromRows_eq_one_comm : ∀ {R : Type u_1} {n : Type u_5} {n₁ : Type u_6} {n₂ : Type u_7} [inst : CommRing R] [inst_1 : Fintype n₁]
  [inst_2 : Fintype n₂] [inst_3 : Fintype n] [inst_4 : DecidableEq n] [inst_5 : DecidableEq n₁]
  [inst_6 : DecidableEq n₂] (e : n ≃ n₁ ⊕ n₂) (A₁ : Matrix n n₁ R) (A₂ : Matrix n n₂ R) (B₁ : Matrix n₁ n R)
  (B₂ : Matrix n₂ n R), A₁.fromCols A₂ * B₁.fromRows B₂ = 1 ↔ B₁.fromRows B₂ * A₁.fromCols A₂ = 1
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.dArrowIso₀₁_inv_right : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  (groupCohomology.dArrowIso₀₁ A).inv.right = (groupCohomology.cochainsIso₁ A).inv
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.memLp : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] (f : ↥(MeasureTheory.Lp E p μ)), MeasureTheory.MemLp (↑↑f) p μ
-- Mathlib.Analysis.Calculus.Deriv.Add
differentiableAt_comp_add_const : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {a b : 𝕜},
  DifferentiableAt 𝕜 (fun x => f (x + b)) a ↔ DifferentiableAt 𝕜 f (a + b)