mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prodComparison_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{w, u₂} D]
  (F : CategoryTheory.Functor C D) (A B : C) [inst_2 : CategoryTheory.Limits.HasBinaryProduct A B]
  [inst_3 : CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)] {Z : D} (h : F.obj A ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prodComparison F A B)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h) =
    CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.prod.fst) h
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.colimitIsoOfIsLeftKanExtension.congr_simp : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α α_1 : F ⟶ L.comp F') (e_α : α = α_1) [inst_3 : F'.IsLeftKanExtension α]
  [inst_4 : CategoryTheory.Limits.HasColimit F] [inst_5 : CategoryTheory.Limits.HasColimit F'],
  F'.colimitIsoOfIsLeftKanExtension α = F'.colimitIsoOfIsLeftKanExtension α_1
-- Mathlib.Order.Filter.CountableInter
Filter.countableInter_ofCountableInter : ∀ {α : Type u_2} (l : Set (Set α)) (hl : ∀ (S : Set (Set α)), S.Countable → S ⊆ l → ⋂₀ S ∈ l)
  (h_mono : ∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l), CountableInterFilter (Filter.ofCountableInter l hl h_mono)
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  (X : CategoryTheory.Functor (CategoryTheory.WithInitial SimplexCategory)ᵒᵖ C) (x : SimplexCategoryᵒᵖ),
  (AugmentedSimplexCategory.equivAugmentedSimplicialObject.functor.obj X).hom.app x =
    X.map
      (match CategoryTheory.WithTerminal.incl.obj x, CategoryTheory.WithTerminal.star,
        CategoryTheory.WithTerminal.starTerminal.from (CategoryTheory.WithTerminal.of x) with
      | CategoryTheory.WithTerminal.of (Opposite.op x), CategoryTheory.WithTerminal.of (Opposite.op y), f =>
        CategoryTheory.WithInitial.down f
      | CategoryTheory.WithTerminal.of (Opposite.op unop), CategoryTheory.WithTerminal.star, x =>
        Opposite.op (CategoryTheory.WithInitial.starInitial.to (CategoryTheory.WithInitial.of unop))
      | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x =>
        CategoryTheory.CategoryStruct.id (Opposite.op CategoryTheory.WithInitial.star))
-- Mathlib.Analysis.Normed.Group.Hom
/-- A `NormedAddGroupHom` is additive.  -/
NormedAddGroupHom.map_add' : ∀ {V : Type u_1} {W : Type u_2} [inst : SeminormedAddCommGroup V] [inst_1 : SeminormedAddCommGroup W]
  (self : NormedAddGroupHom V W) (v₁ v₂ : V), self.toFun (v₁ + v₂) = self.toFun v₁ + self.toFun v₂
-- Mathlib.Algebra.Group.Hom.Basic
MonoidHom.instDiv.eq_1 : ∀ {M : Type u_2} {G : Type u_5} [inst : MulOneClass M] [inst_1 : CommGroup G],
  MonoidHom.instDiv = { div := fun f g => MonoidHom.mk' (fun x => f x / g x) ⋯ }
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.braiding_tensorUnit_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : C),
  (β_ (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.mem_closure_insert : ∀ {α : Type u_2} {M : Matroid α} {X : Set α} {e f : α},
  e ∉ M.closure X → e ∈ M.closure (insert f X) → f ∈ M.closure (insert e X)
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.closure_closure_coe_preimage : ∀ {G : Type u_1} [inst : AddGroup G] {k : Set G}, AddSubgroup.closure (Subtype.val ⁻¹' k) = ⊤
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
/-- The linear equivalence between bilinear forms on `n → R` and `n × n` matrices  -/
LinearMap.BilinForm.toMatrix' : {R₁ : Type u_1} →
  [inst : CommSemiring R₁] →
    {n : Type u_5} → [Fintype n] → [DecidableEq n] → LinearMap.BilinForm R₁ (n → R₁) ≃ₗ[R₁] Matrix n n R₁
-- Mathlib.Topology.Order
nhds_induced : ∀ {α : Type u} {β : Type v} [T : TopologicalSpace α] (f : β → α) (a : β), nhds a = Filter.comap f (nhds (f a))
-- Mathlib.MeasureTheory.Integral.CircleAverage
/-- Analogue of `intervalIntegral.abs_integral_le_integral_abs`: The absolute value of a circle average
is less than or equal to the circle average of the absolute value of the function.
 -/
Real.abs_circleAverage_le_circleAverage_abs : ∀ {c : ℂ} {R : ℝ} {f : ℂ → ℝ}, |Real.circleAverage f c R| ≤ Real.circleAverage |f| c R
-- Init.Omega.IntList
Lean.Omega.IntList.sub_eq_add_neg : ∀ (xs ys : Lean.Omega.IntList), xs - ys = xs + -ys
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
/-- The unit as a natural transformation.  -/
AlgebraicGeometry.identityToΓSpec : CategoryTheory.Functor.id AlgebraicGeometry.LocallyRingedSpace ⟶
  AlgebraicGeometry.LocallyRingedSpace.Γ.rightOp.comp AlgebraicGeometry.Spec.toLocallyRingedSpace
-- Mathlib.Order.DirSupClosed
/-- **Alias** of the reverse direction of `dirSupInacc_compl`. -/
DirSupClosed.compl : ∀ {α : Type u_1} {s : Set α} [inst : Preorder α], DirSupClosed s → DirSupInacc sᶜ
-- Mathlib.Topology.Separation.Regular
instRegularSpaceSubtype : ∀ {X : Type u_1} [inst : TopologicalSpace X] [RegularSpace X] {p : X → Prop}, RegularSpace (Subtype p)
-- Mathlib.Topology.Algebra.Monoid
/-- Construct a bundled additive monoid homomorphism from a pointwise limit of additive
monoid homomorphisms  -/
addMonoidHomOfTendsto : {α : Type u_2} →
  {M₁ : Type u_6} →
    {M₂ : Type u_7} →
      [inst : TopologicalSpace M₂] →
        [T2Space M₂] →
          [inst_2 : AddZeroClass M₁] →
            [inst_3 : AddZeroClass M₂] →
              [ContinuousAdd M₂] →
                {F : Type u_8} →
                  [inst_5 : FunLike F M₁ M₂] →
                    [AddMonoidHomClass F M₁ M₂] →
                      {l : Filter α} →
                        (f : M₁ → M₂) →
                          (g : α → F) → [l.NeBot] → Filter.Tendsto (fun a x => (g a) x) l (nhds f) → M₁ →+ M₂
-- Init.Tactics
/-- A target for the `induction` or `cases` tactic, of the form `e` or `h : e`.

The `h : e` syntax introduces a hypotheses of the form `h : e = _` in each goal,
with `_` replaced by the corresponding value of the target.
It is useful when `e` is not a free variable.
 -/
Lean.Parser.Tactic.elimTarget : Lean.ParserDescr
-- Mathlib.Combinatorics.Enumerative.Catalan.Tree
BinaryTree.treesOfNumNodesEq_succ : ∀ (n : ℕ),
  BinaryTree.treesOfNumNodesEq (n + 1) =
    (Finset.HasAntidiagonal.antidiagonal n).biUnion fun ij =>
      BinaryTree.pairwiseNode (BinaryTree.treesOfNumNodesEq ij.1) (BinaryTree.treesOfNumNodesEq ij.2)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.functorPushforward_mem_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor C D) {X : C} {S : CategoryTheory.Sieve X}
  [CategoryTheory.Functor.IsDenseSubsite J K G], CategoryTheory.Sieve.functorPushforward G S ∈ K (G.obj X) ↔ S ∈ J X
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Multiset.aestronglyMeasurable_fun_prod : ∀ {α : Type u_1} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {M : Type u_5} [inst : CommMonoid M]
  [inst_1 : TopologicalSpace M] [ContinuousMul M] (s : Multiset (α → M)),
  (∀ f ∈ s, MeasureTheory.AEStronglyMeasurable f μ) →
    MeasureTheory.AEStronglyMeasurable (fun x => (Multiset.map (fun f => f x) s).prod) μ
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.piecewise_apply_right : ∀ {X : Type u_1} {Z : Type u_3} [inst : TopologicalSpace X] {C₁ C₂ : Set X} (h₁ : IsClosed C₁) (h₂ : IsClosed C₂)
  (h : C₁ ∪ C₂ = Set.univ) (f : LocallyConstant (↑C₁) Z) (g : LocallyConstant (↑C₂) Z)
  (hfg : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f ⟨x, ⋯⟩ = g ⟨x, ⋯⟩) [inst_1 : DecidablePred fun x => x ∈ C₁] (x : X)
  (hx : x ∈ C₂), (LocallyConstant.piecewise h₁ h₂ h f g hfg) x = g ⟨x, hx⟩
-- Mathlib.Algebra.NoZeroSMulDivisors.Basic
/-- This instance applies to `DivisionSemiring`s, in particular `NNReal` and `NNRat`.  -/
GroupWithZero.toNoZeroSMulDivisors : ∀ {R : Type u_1} {M : Type u_2} [inst : GroupWithZero R] [inst_1 : AddMonoid M] [inst_2 : DistribMulAction R M],
  NoZeroSMulDivisors R M
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsAtomic.realize_comp : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {M : Type u_1} [inst : L.Structure M] {N : Type u_2}
  [inst_1 : L.Structure N] {F : Type u_3} [inst_2 : FunLike F M N] {φ : L.BoundedFormula α n},
  φ.IsAtomic →
    ∀ [EmbeddingLike F M N] [L.HomClass F M N] (f : F) {v : α → M} {xs : Fin n → M},
      φ.Realize v xs → φ.Realize (⇑f ∘ v) (⇑f ∘ xs)
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
const_smul_mfderiv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {z : M} {f : M → E'}, MDiffAt f z → ∀ (s : 𝕜), mfderiv% (s • f) z = s • mfderiv% f z
-- Mathlib.Analysis.Convex.PathConnected
/-- A subspace in a topological vector space over `ℝ` is path connected.  -/
Submodule.isPathConnected : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [ContinuousAdd E]
  [ContinuousSMul ℝ E] (s : Submodule ℝ E), IsPathConnected ↑s
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.Integrable.lintegral_lt_top : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  MeasureTheory.Integrable f μ → ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ < ⊤
-- Mathlib.Algebra.Group.Subgroup.Map
/-- If `H ≤ K`, then `H` as a subgroup of `K` is isomorphic to `H`.  -/
Subgroup.subgroupOfEquivOfLe : {G : Type u_7} → [inst : Group G] → {H K : Subgroup G} → H ≤ K → ↥(H.subgroupOf K) ≃* ↥H
-- Mathlib.Analysis.SpecificLimits.Normed
Units.val_oneSub : ∀ {R : Type u_4} [inst : NormedRing R] [inst_1 : HasSummableGeomSeries R] (t : R) (h : ‖t‖ < 1),
  ↑(Units.oneSub t h) = 1 - t
-- Mathlib.Analysis.ODE.Transform
IsIntegralCurveAt.comp_sub : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {t₀ : ℝ},
  IsIntegralCurveAt γ v t₀ → ∀ (dt : ℝ), IsIntegralCurveAt (γ ∘ fun x => x - dt) (v ∘ fun x => x - dt) (t₀ + dt)
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.nsmul_mem : ∀ {G : Type u_1} [inst : AddGroup G] (K : AddSubgroup G) {x : G}, x ∈ K → ∀ (n : ℕ), n • x ∈ K
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.coe_toAddSubgroup_apply : ∀ {G : Type u_1} [inst : Group G] (S : Subgroup G), ↑(Subgroup.toAddSubgroup S) = ⇑Additive.toMul ⁻¹' ↑S
-- Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit
CategoryTheory.Functor.weightedLimObjObjMap_π : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {W W' : CategoryTheory.Functor J (Type w)} (g : W ⟶ W') (F : CategoryTheory.Functor J C)
  [inst_2 : CategoryTheory.Limits.HasWeightedLimit W F] [inst_3 : CategoryTheory.Limits.HasWeightedLimit W' F] ⦃j : J⦄
  (x : W.obj j),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.weightedLimFlipObjMap g F) (W.weightedLimObjObjπ F x) =
    W'.weightedLimObjObjπ F ((CategoryTheory.ConcreteCategory.hom (g.app j)) x)
-- Init.Data.List.Attach
List.attach_map_val : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : α → β}, List.map (fun i => f ↑i) l.attach = List.map f l
-- Mathlib.NumberTheory.Dioph
/-- Diophantine sets are closed under union.  -/
Dioph.union : ∀ {α : Type u} {S S' : Set (α → ℕ)}, Dioph S → Dioph S' → Dioph (S ∪ S')
-- Mathlib.Algebra.Module.ZLattice.Basic
/-- Return an arbitrary `ℤ`-basis of a lattice `L` of `ι → ℝ` indexed by `ι`.
 -/
IsZLattice.basis : {ι : Type u_1} →
  [inst : Fintype ι] →
    (L : Submodule ℤ (ι → ℝ)) → [inst_1 : DiscreteTopology ↥L] → [IsZLattice ℝ L] → Module.Basis ι ℤ ↥L
-- Mathlib.Analysis.Complex.HasPrimitives
_private.Mathlib.Analysis.Complex.HasPrimitives.0.Complex.re_add_im_mul_mem_ball : ∀ {c z : ℂ} {r : ℝ}, z ∈ Metric.ball c r → ↑z.re + ↑c.im * Complex.I ∈ Metric.ball c r
-- Mathlib.Algebra.Group.Submonoid.Pointwise
Submonoid.closure_pow_anti : ∀ {M : Type u_3} [inst : Monoid M] {s : Set M} {m n : ℕ}, m ∣ n → Submonoid.closure (s ^ n) ≤ Submonoid.closure (s ^ m)
-- Mathlib.GroupTheory.EckmannHilton
EckmannHilton.IsUnital.toLawfulIdentity : ∀ {X : Type u} {m : X → X → X} {e : X}, EckmannHilton.IsUnital m e → Std.LawfulIdentity m e
-- Mathlib.RingTheory.PrincipalIdealDomain
/-- Any Bézout domain is a GCD domain. This is not an instance since `GCDMonoid` contains data,
and this might not be how we would like to construct it.  -/
IsBezout.toGCDDomain : (R : Type u) → [inst : CommRing R] → [IsBezout R] → [IsCancelMulZero R] → [DecidableEq R] → GCDMonoid R
-- Mathlib.Data.Finset.NAry
Set.Finite.toFinset_image2 : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {s : Set α} {t : Set β} (f : α → β → γ)
  (hs : s.Finite) (ht : t.Finite) (hf : optParam (Set.image2 f s t).Finite ⋯),
  hf.toFinset = Finset.image₂ f hs.toFinset ht.toFinset
-- Init.Data.UInt.BasicAux
/-- Adds two word-sized unsigned integers, wrapping around on overflow.  Usually accessed via the `+`
operator.

This function is overridden at runtime with an efficient implementation.
 -/
USize.add : USize → USize → USize
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.Comonad.map_counit_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Comonad C) (X : C)
  [CategoryTheory.IsIso T.δ], T.map (T.ε.app X) = T.ε.app (T.obj X)
-- Std.Tactic.BVDecide.LRAT.Internal.CompactLRATCheckerSound
_private.Std.Tactic.BVDecide.LRAT.Internal.CompactLRATCheckerSound.0.Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker.go.match_3.eq_3 : ∀ {n : ℕ} (motive : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClauseAction n) → Sort u_1) (id : ℕ)
  (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (rupHints : Array ℕ) (h_1 : Unit → motive none)
  (h_2 : (id : ℕ) → (rupHints : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints)))
  (h_3 :
    (id : ℕ) →
      (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) →
        (rupHints : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints)))
  (h_4 :
    (id : ℕ) →
      (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) →
        (pivot : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) →
          (rupHints : Array ℕ) →
            (ratHints : Array (ℕ × Array ℕ)) →
              motive (some (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints)))
  (h_5 : (ids : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.del ids))),
  (match some (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints) with
    | none => h_1 ()
    | some (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints) => h_2 id rupHints
    | some (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints) => h_3 id c rupHints
    | some (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints) => h_4 id c pivot rupHints ratHints
    | some (Std.Tactic.BVDecide.LRAT.Action.del ids) => h_5 ids) =
    h_3 id c rupHints
-- Mathlib.Order.Antisymmetrization
ofAntisymmetrization_le_ofAntisymmetrization_iff : ∀ {α : Type u_1} [inst : Preorder α] {a b : Antisymmetrization α fun x1 x2 => x1 ≤ x2},
  ofAntisymmetrization (fun x1 x2 => x1 ≤ x2) a ≤ ofAntisymmetrization (fun x1 x2 => x1 ≤ x2) b ↔ a ≤ b
-- Mathlib.GroupTheory.Index
Subgroup.relIndex_map_map : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] (f : G →* G') (H K : Subgroup G),
  (Subgroup.map f H).relIndex (Subgroup.map f K) = (H ⊔ f.ker).relIndex (K ⊔ f.ker)
-- Mathlib.Topology.Order.Category.AlexDisc
AlexDisc.instCoeSortType : CoeSort AlexDisc (Type u_1)
-- Mathlib.Algebra.Homology.HomologicalComplex
ChainComplex.mkHom_f_1 : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (P Q : ChainComplex V ℕ) (zero : P.X 0 ⟶ Q.X 0) (one : P.X 1 ⟶ Q.X 1)
  (one_zero_comm : CategoryTheory.CategoryStruct.comp one (Q.d 1 0) = CategoryTheory.CategoryStruct.comp (P.d 1 0) zero)
  (succ :
    (n : ℕ) →
      (p :
          (f : P.X n ⟶ Q.X n) ×'
            (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×'
              CategoryTheory.CategoryStruct.comp f' (Q.d (n + 1) n) =
                CategoryTheory.CategoryStruct.comp (P.d (n + 1) n) f) →
        (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×'
          CategoryTheory.CategoryStruct.comp f'' (Q.d (n + 2) (n + 1)) =
            CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 1)) p.snd.fst),
  (P.mkHom Q zero one one_zero_comm succ).f 1 = one
-- Mathlib.GroupTheory.OrderOfElement
LeftCancelMonoid.groupOfFinite.eq_1 : ∀ {G : Type u_1} [inst : LeftCancelMonoid G] [inst_1 : Finite G],
  LeftCancelMonoid.groupOfFinite =
    { toMonoid := inst.toMonoid, inv := fun x => x ^ (orderOf x - 1), div := DivInvMonoid.div', zpow := zpowRec,
      div_eq_mul_inv := ⋯, zpow_zero' := ⋯, zpow_succ' := ⋯, zpow_neg' := ⋯, inv_mul_cancel := ⋯ }
-- Init.Data.Ord.Basic
Ordering.then_eq_lt : ∀ {o₁ o₂ : Ordering}, o₁.then o₂ = Ordering.lt ↔ o₁ = Ordering.lt ∨ o₁ = Ordering.eq ∧ o₂ = Ordering.lt
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
NumberField.Units.dirichletUnitTheorem.logEmbedding_component_le : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {r : ℝ} {x : (NumberField.RingOfIntegers K)ˣ},
  0 ≤ r →
    ‖(NumberField.Units.logEmbedding K) x‖ ≤ r →
      ∀ (w : { w // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ }),
        |(NumberField.Units.logEmbedding K) (Additive.ofMul x) w| ≤ r
-- Mathlib.LinearAlgebra.Trace
/-- An idempotent endomorphism of a module over a characteristic-zero commutative ring
with vanishing trace is the zero map, provided its range and kernel are finite and free.

The `Module.Free` and `Module.Finite` instance arguments on `range e` and `ker e` are
automatic over a field, and more generally over any principal ideal domain `R` for which
`M` itself is finite and free (submodules of finite free modules over a PID are finite
and free).  -/
LinearMap.IsIdempotentElem.trace_eq_zero_iff : ∀ {R : Type u_6} [inst : CommRing R] [CharZero R] {M : Type u_7} [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  {e : M →ₗ[R] M},
  IsIdempotentElem e →
    ∀ [Module.Free R ↥e.range] [Module.Finite R ↥e.range] [Module.Free R ↥e.ker] [Module.Finite R ↥e.ker],
      (LinearMap.trace R M) e = 0 ↔ e = 0
-- Mathlib.Topology.ContinuousOn
ContinuousWithinAt.snd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] {f : α → β × γ} {s : Set α} {a : α},
  ContinuousWithinAt f s a → ContinuousWithinAt (fun x => (f x).2) s a
-- Mathlib.Order.Filter.Prod
/-- If a function tends to a product `g ×ˢ h` of filters, then its first component tends to
`g`. See also `Filter.Tendsto.fst_nhds` for the special case of converging to a point in a
product of two topological spaces.  -/
Filter.Tendsto.fst : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Filter β} {h : Filter γ} {m : α → β × γ},
  Filter.Tendsto m f (g ×ˢ h) → Filter.Tendsto (fun a => (m a).1) f g
-- Init.Data.List.Nat.Range
List.find?_range_eq_some : ∀ {n i : ℕ} {p : ℕ → Bool},
  List.find? p (List.range n) = some i ↔ p i = true ∧ i ∈ List.range n ∧ ∀ j < i, (!p j) = true
-- Mathlib.CategoryTheory.Idempotents.FunctorCategories
CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.obj_obj_p : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] (P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Functor J C))
  (j : J), ((CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.obj P).obj j).p = P.p.app j
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.basis.eq_1 : ∀ (L : PeriodPair), L.basis = basisOfLinearIndependentOfCardEqFinrank ⋯ PeriodPair.basis._proof_1
-- Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi
CategoryTheory.Idempotents.KaroubiKaroubi.equivalence_inverse : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C],
  (CategoryTheory.Idempotents.KaroubiKaroubi.equivalence C).inverse =
    CategoryTheory.Idempotents.KaroubiKaroubi.inverse C
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get?_insertIfNew : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF →
    ∀ {k a : α} {v : β},
      Std.DHashMap.Internal.Raw₀.Const.get? (m.insertIfNew k v) a =
        if (k == a) = true ∧ m.contains k = false then some v else Std.DHashMap.Internal.Raw₀.Const.get? m a
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getD_union_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {k : α} {fallback : β},
  k ∉ t₁ → Std.ExtDTreeMap.Const.getD (t₁.union t₂) k fallback = Std.ExtDTreeMap.Const.getD t₂ k fallback
-- Std.Http.Data.Method
Std.Http.Method.versionControl.sizeOf_spec : sizeOf Std.Http.Method.versionControl = 1
-- Lean.Elab.Tactic.BuiltinTactic
Lean.Elab.Tactic.evalTacticSeq1Indented : Lean.Elab.Tactic.Tactic
-- Mathlib.RingTheory.Valuation.Basic
AddValuation.map_add_eq_of_lt_right : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀)
  {x y : R}, v y < v x → v (x + y) = v y
-- Mathlib.Algebra.Homology.ShortComplex.QuasiIso
/-- A morphism `φ : S₁ ⟶ S₂` of short complexes that have homology is a quasi-isomorphism if
the induced map `homologyMap φ : S₁.homology ⟶ S₂.homology` is an isomorphism.  -/
CategoryTheory.ShortComplex.QuasiIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} → [S₁.HasHomology] → [S₂.HasHomology] → (S₁ ⟶ S₂) → Prop
-- Mathlib.Algebra.Order.Ring.Synonym
ofLex_natCast : ∀ {R : Type u_1} [inst : NatCast R] (n : ℕ), ofLex ↑n = ↑n
-- Mathlib.CategoryTheory.Subobject.ArtinianObject
CategoryTheory.isArtinianObject_iff_isEventuallyConstant : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C),
  CategoryTheory.IsArtinianObject X ↔
    ∀ (F : CategoryTheory.Functor ℕ (CategoryTheory.MonoOver X)ᵒᵖ), CategoryTheory.IsFiltered.IsEventuallyConstant F
-- Mathlib.Algebra.Algebra.Bilinear
LinearMap.mul'_comm : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocCommSemiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A] (x : TensorProduct R A A),
  (LinearMap.mul' R A) ((TensorProduct.comm R A A) x) = (LinearMap.mul' R A) x
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.coe_iInf : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : SMul R M] {ι : Sort u_7} (f : ι → ConvexCone R M), ↑(iInf f) = ⋂ i, ↑(f i)
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- **Alias** of `FunLike.coe_zero`. -/
GroupSeminorm.coe_zero : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Zero F] [inst_2 : Zero β]
  [IsZeroApply F α β], ⇑0 = 0
-- Mathlib.Data.Finset.Density
Finset.dens_sdiff_add_dens_eq_dens : ∀ {α : Type u_2} [inst : Fintype α] {s t : Finset α} [inst_1 : DecidableEq α], s ⊆ t → (t \ s).dens + s.dens = t.dens