mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
/-- The natural isomorphism `t.eTruncLT.obj a ⋙ t.eTruncLT.obj b ⟶ t.eTruncLT.obj b`
when `a` and `b` in `EInt` satisfy `b ≤ a`.  -/
CategoryTheory.Triangulated.TStructure.eTruncLTLTIsoLT : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              (t : CategoryTheory.Triangulated.TStructure C) →
                [CategoryTheory.IsTriangulated C] →
                  (a b : EInt) → b ≤ a → ((t.eTruncLT.obj a).comp (t.eTruncLT.obj b) ≅ t.eTruncLT.obj b)
-- Mathlib.Order.SuccPred.Limit
Order.IsSuccLimit.le_succ_iff : ∀ {α : Type u_1} {a b : α} [inst : LinearOrder α] [inst_1 : SuccOrder α],
  Order.IsSuccLimit b → (b ≤ Order.succ a ↔ b ≤ a)
-- Lean.Data.KVMap
Lean.DataValue.ofInt.inj : ∀ {v v_1 : ℤ}, Lean.DataValue.ofInt v = Lean.DataValue.ofInt v_1 → v = v_1
-- Mathlib.RingTheory.Adjoin.FG
Subalgebra.fg_of_submodule_fg : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A], ⊤.FG → ⊤.FG
-- Mathlib.Algebra.BigOperators.Finprod
finprod_mem_coe_finset : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] (f : α → M) (s : Finset α),
  ∏ᶠ (i : α) (_ : i ∈ ↑s), f i = ∏ i ∈ s, f i
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
SlashInvariantForm.coe_prod : ∀ {ι : Type} {s : Finset ι} {k : ι → ℤ} (m : ℤ) (hm : m = ∑ i ∈ s, k i) {Γ : Subgroup (GL (Fin 2) ℝ)}
  [inst : Γ.HasDetPlusMinusOne] (f : (i : ι) → SlashInvariantForm Γ (k i)),
  ⇑(SlashInvariantForm.prod m hm f) = ∏ i ∈ s, ⇑(f i)
-- Mathlib.CategoryTheory.Monad.Coequalizer
CategoryTheory.Monad.beckCofork_pt : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : T.Algebra),
  (CategoryTheory.Monad.beckCofork X).pt = X.A
-- Mathlib.Data.Finset.Lattice.Prod
/-- See also `Finset.product_biUnion`.  -/
Finset.sup_product_left : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeSup α] [inst_1 : OrderBot α] (s : Finset β)
  (t : Finset γ) (f : β × γ → α), (s ×ˢ t).sup f = s.sup fun i => t.sup fun i' => f (i, i')
-- Mathlib.CategoryTheory.Subfunctor.Sieves
/-- Given an `F`-section `s` on `U` and a subpresheaf `G`, we may define a family of elements in
`G` consisting of the restrictions of `s`  -/
CategoryTheory.Subfunctor.familyOfElementsOfSection : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor Cᵒᵖ (Type w)} →
      (G : CategoryTheory.Subfunctor F) →
        {U : Cᵒᵖ} → (s : F.obj U) → CategoryTheory.Presieve.FamilyOfElements G.toFunctor (G.sieveOfSection s).arrows
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.nonDegenerateEquiv'_iff : ∀ {n d : ℕ} (x : ↑((SSet.stdSimplex.obj { len := n }).nonDegenerate d)) (j : Fin (n + 1)),
  j ∈ ↑(SSet.stdSimplex.nonDegenerateEquiv' x) ↔ ∃ i, ↑x i = j
-- Mathlib.RepresentationTheory.FiniteIndex
/-- Let `S ≤ G` be a subgroup and `A` a `k`-linear `S`-representation. This is the `k`-linear map
`Ind_S^G(A) →ₗ[k] Coind_S^G(A)` sending `(⟦g ⊗ₜ[k] a⟧, sg) ↦ ρ(s)(a)`.  -/
Rep.indToCoind : {k : Type u} →
  {G : Type v} →
    [inst : CommRing k] →
      [inst_1 : Group G] →
        {S : Subgroup G} →
          [DecidableRel ⇑(QuotientGroup.rightRel S)] →
            (A : Rep.{w, u, v} k ↥S) → ↑(Rep.ind S.subtype A) →ₗ[k] ↑(Rep.coind.{u, v, v, w} S.subtype A)
-- Init.Data.ToString.Basic
addParenHeuristic : String → String
-- Mathlib.Analysis.Convex.Between
/-- **Alias** of the reverse direction of `sbtw_const_add_iff`. -/
Sbtw.const_add : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] {x y z : V} (v : V), Sbtw R x y z → Sbtw R (v + x) (v + y) (v + z)
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
/-- Right homotopies in a full subcategory identify to right homotopies in the
ambient category.  -/
HomotopicalAlgebra.PrepathObject.RightHomotopy.fullSubcategoryEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {P : CategoryTheory.ObjectProperty C} →
      {X Y : P.FullSubcategory} →
        {Q : HomotopicalAlgebra.PrepathObject Y} →
          {f g : X ⟶ Y} → Q.RightHomotopy f g ≃ (Q.map P.ι).RightHomotopy f.hom g.hom
-- Mathlib.Algebra.Module.PUnit
PUnit.instSMul_mathlib.eq_1 : ∀ {R : Type u_1}, PUnit.instSMul_mathlib = { smul := fun x x_1 => x_1 }
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.instLEQOfOrderedAdd : {α : Type u} →
  [inst : Lean.Grind.Semiring α] →
    [inst_1 : LE α] → [inst_2 : Std.IsPreorder α] → [Lean.Grind.OrderedAdd α] → LE (Lean.Grind.Ring.OfSemiring.Q α)
-- Mathlib.SetTheory.Cardinal.Defs
/-- The indexed product of cardinals is the cardinality of the Pi type
(dependent product).  -/
Cardinal.prod : {ι : Type u} → (ι → Cardinal.{u_1}) → Cardinal.{max u u_1}
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- The canonical morphism from a biproduct to the biproduct over a restriction of its index
type.  -/
CategoryTheory.Limits.biproduct.toSubtype : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        (f : J → C) →
          [inst_2 : CategoryTheory.Limits.HasBiproduct f] →
            (p : J → Prop) →
              [inst_3 : CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)] → ⨁ f ⟶ ⨁ Subtype.restrict p f
-- Init.Prelude
Nat.succ_pos : ∀ (n : ℕ), 0 < n.succ
-- Mathlib.Logic.Equiv.Set
Equiv.Set.congr_apply : ∀ {α : Type u_3} {β : Type u_4} (e : α ≃ β) (s : Set α), (Equiv.Set.congr e) s = ⇑e '' s
-- Std.Time.Format.Modifier
/-- `y`: Year of era (e.g., 2004, 04, 0002, 2). Never negative: year 1 BC is formatted as `1` paired with a BC era
designator. Use `u` instead when you need the proleptic/astronomical year (which can be negative).
 -/
Std.Time.Modifier.y : Std.Time.Year → Std.Time.Modifier
-- Mathlib.Topology.NhdsSet
nhdsSet_le : ∀ {X : Type u_2} [inst : TopologicalSpace X] {f : Filter X} {s : Set X}, nhdsSet s ≤ f ↔ ∀ x ∈ s, nhds x ≤ f
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.one_toType_eq : ∀ (x : Ordinal.ToType 1), x = (Ordinal.enum fun x1 x2 => x1 < x2) ⟨0, Ordinal.uniqueToTypeOne._proof_2⟩
-- Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
AlgebraicGeometry.instFaithfulOverSchemePullbackOfSurjectiveOfFlatOfLocallyOfFinitePresentation : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.Surjective f] [AlgebraicGeometry.Flat f]
  [AlgebraicGeometry.LocallyOfFinitePresentation f], (CategoryTheory.Over.pullback f).Faithful
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- If a property holds for all points in balls of arbitrarily large radii, then it holds for all
points.  -/
Metric.forall_of_forall_mem_ball : ∀ {α : Type u} [inst : PseudoMetricSpace α] (p : α → Prop) (x : α),
  (∃ᶠ (R : ℝ) in Filter.atTop, ∀ y ∈ Metric.ball x R, p y) → ∀ (y : α), p y
-- Mathlib.Data.List.Basic
List.getLastI.eq_def : ∀ {α : Type u_1} [inst : Inhabited α] (x : List α),
  x.getLastI =
    match x with
    | [] => default
    | [a] => a
    | [head, b] => b
    | head :: head_1 :: l => l.getLastI
-- Mathlib.Order.Interval.Set.OrderIso
OrderIso.image_Ico : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β) (b a : α),
  ⇑e '' Set.Ico b a = Set.Ico (e b) (e a)
-- Init.Data.Nat.Basic
Nat.sub_lt_sub_right : ∀ {a b c : ℕ}, c ≤ a → a < b → a - c < b - c
-- Mathlib.LinearAlgebra.DFinsupp
DFinsupp.sum_mapRange_index.linearMap : ∀ {ι : Type u_1} {R : Type u_3} {N : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid N] [inst_2 : Module R N]
  {β₁ : ι → Type u_8} {β₂ : ι → Type u_9} [inst_3 : (i : ι) → AddCommMonoid (β₁ i)]
  [inst_4 : (i : ι) → AddCommMonoid (β₂ i)] [inst_5 : (i : ι) → Module R (β₁ i)] [inst_6 : (i : ι) → Module R (β₂ i)]
  [inst_7 : DecidableEq ι] {f : (i : ι) → β₁ i →ₗ[R] β₂ i} {h : (i : ι) → β₂ i →ₗ[R] N} {l : Π₀ (i : ι), β₁ i},
  ((DFinsupp.lsum ℕ) h) ((DFinsupp.mapRange.linearMap f) l) = ((DFinsupp.lsum ℕ) fun i => h i ∘ₗ f i) l
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.instPartialOrder : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : NormedAddCommGroup β] → [Lattice β] → PartialOrder (BoundedContinuousFunction α β)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKey.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (t t_1 : Std.DTreeMap.Internal.Impl α β) (e_t : t = t_1) (k k_1 : α)
  (e_k : k = k_1) (hlk : Std.DTreeMap.Internal.Impl.contains k t = true), t.getKey k hlk = t_1.getKey k_1 ⋯
-- Init.Grind.ToInt
Lean.Grind.ToInt.Sub.mk : ∀ {α : Type u} [inst : Sub α] {I : outParam Lean.Grind.IntInterval} [inst_1 : Lean.Grind.ToInt α I],
  (∀ (x y : α), ↑(x - y) = I.wrap (↑x - ↑y)) → Lean.Grind.ToInt.Sub α I
-- Mathlib.Analysis.Convex.Hull
affineSpan_convexHull : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] (s : Set E), affineSpan 𝕜 ((convexHull 𝕜) s) = affineSpan 𝕜 s
-- Mathlib.Analysis.Calculus.ContDiff.Bounds
norm_iteratedFDeriv_clm_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type uG}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F →L[𝕜] G} {g : E → F} {N : WithTop ℕ∞} {n : ℕ},
  ContDiff 𝕜 N f →
    ContDiff 𝕜 N g →
      ∀ (x : E),
        ↑n ≤ N →
          ‖iteratedFDeriv 𝕜 n (fun y => (f y) (g y)) x‖ ≤
            ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv 𝕜 i f x‖ * ‖iteratedFDeriv 𝕜 (n - i) g x‖
-- Mathlib.Order.Interval.Set.Basic
Set.Icc_inter_Icc : ∀ {α : Type u_1} [inst : Lattice α] {a₁ a₂ b₁ b₂ : α}, Set.Icc a₁ b₁ ∩ Set.Icc a₂ b₂ = Set.Icc (a₁ ⊔ a₂) (b₁ ⊓ b₂)
-- Lean.Level
Lean.Level.PP.Result.num.sizeOf_spec : ∀ (a : ℕ), sizeOf (Lean.Level.PP.Result.num a) = 1 + sizeOf a
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_pi_div_eight : Real.sin (Real.pi / 8) = √(2 - √2) / 2
-- Mathlib.Algebra.Lie.TransferInstance
/-- Transfer `LieAlgebra` across an `Equiv`  -/
Equiv.lieAlgebra : (R : Type u_1) →
  {L' : Type u_2} →
    {L : Type u_3} → [inst : CommRing R] → [inst_1 : LieRing L] → [LieAlgebra R L] → (e : L' ≃ L) → LieAlgebra R L'
-- Init.Data.Vector.Lemmas
Vector.prod_eq_foldl : ∀ {α : Type u_1} {n : ℕ} [inst : One α] [inst_1 : Mul α] [Std.Associative fun x1 x2 => x1 * x2]
  [Std.LawfulIdentity (fun x1 x2 => x1 * x2) 1] {xs : Vector α n}, xs.prod = Vector.foldl (fun x1 x2 => x1 * x2) 1 xs
-- Mathlib.AlgebraicGeometry.Stalk
AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_Spec_fromSpecStalk : ∀ {X : AlgebraicGeometry.Scheme} {R : CommRingCat} [inst : IsLocalRing ↑R] {x : ↥X} (f : X.presheaf.stalk x ⟶ R)
  [inst_1 : IsLocalHom (CommRingCat.Hom.hom f)] (U : X.Opens)
  (hU :
    (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map f) (X.fromSpecStalk x))
        (IsLocalRing.closedPoint ↑R) ∈
      U),
  CategoryTheory.CategoryStruct.comp
      (X.presheaf.germ U
        ((CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map f) (X.fromSpecStalk x))
          (IsLocalRing.closedPoint ↑R))
        hU)
      (AlgebraicGeometry.Scheme.stalkClosedPointTo
        (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map f) (X.fromSpecStalk x))) =
    CategoryTheory.CategoryStruct.comp (X.presheaf.germ U x ⋯) f
-- Lean.DocString.Parser
/-- Parses a metadata block, which contains the contents of a Lean structure initialization but is
surrounded by `%%%` on each side.
 -/
Lean.Doc.Parser.metadataBlock : optParam Lean.Doc.Parser.BlockCtxt { } → Lean.Parser.ParserFn
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instDiv : {α : Type u_1} → {β : Type u_2} → [inst : MeasurableSpace α] → [Div β] → Div (MeasureTheory.SimpleFunc α β)
-- Mathlib.Topology.MetricSpace.Holder
/-- If a function is `(C₁, r)`-Hölder and `(C₂, s)`-Hölder, then it is
`(C₁ ^ t₁ * C₂ ^ t₂, r * t₁ + s * t₂)`-Hölder for all `t₁ t₂ : ℝ≥0` such that
`t₁ + t₂ = 1`.  -/
HolderOnWith.interpolate : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {r : NNReal} {f : X → Y}
  {C₁ C₂ s t₁ t₂ : NNReal} {A : Set X},
  HolderOnWith C₁ r f A → HolderOnWith C₂ s f A → t₁ + t₂ = 1 → HolderOnWith (C₁ ^ ↑t₁ * C₂ ^ ↑t₂) (r * t₁ + s * t₂) f A
-- Mathlib.Topology.Algebra.Group.Basic
IsOpen.rightCoset : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [SeparatelyContinuousMul G] {U : Set G},
  IsOpen U → ∀ (x : G), IsOpen (MulOpposite.op x • U)
-- Mathlib.LinearAlgebra.FreeModule.Basic
Module.End.mem_center_iff : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M]
  {f : Module.End R M}, f ∈ Set.center (Module.End R M) ↔ ∃ α, ∃ (hα : α ∈ Set.center R), f = Module.End.smulLeft α hα
-- Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
/-- A version of `Polynomial.isMonicOfDegree_two_iff` with negated middle coefficient.  -/
Polynomial.isMonicOfDegree_two_iff' : ∀ {R : Type u_1} [inst : Ring R] [Nontrivial R] {f : Polynomial R},
  f.IsMonicOfDegree 2 ↔ ∃ a b, f = Polynomial.X ^ 2 - Polynomial.C a * Polynomial.X + Polynomial.C b
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Internal.USquashOrUnit : Type v → Type u
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.coe_coe : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] (e : A ≃A[R] B), ⇑↑e = ⇑e
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.evalFunInduction : Lean.Elab.Tactic.Tactic
-- Mathlib.Probability.ProbabilityMassFunction.Monad
PMF.mem_support_bindOnSupport_iff : ∀ {α : Type u_1} {β : Type u_2} {p : PMF α} (f : (a : α) → a ∈ p.support → PMF β) (b : β),
  b ∈ (p.bindOnSupport f).support ↔ ∃ a, ∃ (h : a ∈ p.support), b ∈ (f a h).support
-- Init.Data.SInt.Basic
instDecidableEqInt32 : DecidableEq Int32
-- Std.Data.ExtDTreeMap.Basic
/-- Given a proof that such a mapping exists, retrieves the key-value pair with the smallest key that is
greater than the given key.
 -/
Std.ExtDTreeMap.Const.getEntryGT : {α : Type u} →
  {cmp : α → α → Ordering} →
    {β : Type v} →
      [inst : Std.TransCmp cmp] →
        (t : Std.ExtDTreeMap α (fun x => β) cmp) → (k : α) → (∃ a ∈ t, cmp a k = Ordering.gt) → α × β
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙHom_id : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] {a : A} (ha : p a),
  (cfcₙHom ha) (ContinuousMapZero.id (quasispectrum R a)) = a
-- Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf
CategoryTheory.Precoverage.SubsheafClosure.below : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {K : CategoryTheory.Precoverage C} →
      {F : CategoryTheory.Functor Cᵒᵖ (Type w)} →
        {𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))} →
          {motive : (Z : C) → (a : F.obj (Opposite.op Z)) → K.SubsheafClosure 𝒮 Z a → Prop} →
            {Z : C} → {a : F.obj (Opposite.op Z)} → K.SubsheafClosure 𝒮 Z a → Prop
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
linearIndependent_le_span_aux' : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  {ι : Type u_2} [inst_4 : Fintype ι] (v : ι → M),
  LinearIndependent R v →
    ∀ (w : Set M) [inst_5 : Fintype ↑w], Set.range v ⊆ ↑(Submodule.span R w) → Fintype.card ι ≤ Fintype.card ↑w
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.minD_le_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  t.contains k = true → ∀ {fallback : α}, (cmp (t.minD fallback) k).isLE = true
-- Mathlib.Topology.Constructions
IsDiscrete.mk : ∀ {X : Type u_5} [inst : TopologicalSpace X] {s : Set X}, DiscreteTopology ↑s → IsDiscrete s
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get_max? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {km : α}
  {hc : t.contains km = true}, t.max?.get ⋯ = km → t.get km hc = km
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.mapTrifunctorMapFunctorObj_obj_obj : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))) {I₁ : Type u_7}
  {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} (p : I₁ × I₂ × I₃ → J) (X₁ : CategoryTheory.GradedObject I₁ C₁)
  [inst_4 :
    ∀ (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃),
      ((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p]
  (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃),
  ((CategoryTheory.GradedObject.mapTrifunctorMapFunctorObj F p X₁).obj X₂).obj X₃ =
    CategoryTheory.GradedObject.mapTrifunctorMapObj F p X₁ X₂ X₃
-- Mathlib.LinearAlgebra.Dimension.Finite
LinearIndependent.finrank_eq_zero_of_infinite : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Nontrivial R]
  {ι : Type u_1} [Infinite ι] {v : ι → M}, LinearIndependent R v → Module.finrank R M = 0
-- Lean.Compiler.IR.Basic
Lean.IR.Arg.erased.sizeOf_spec : sizeOf Lean.IR.Arg.erased = 1
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rio.isSome_succMany?_of_lt_size_toArray : ∀ {α : Type u} {r : Std.Rio α} [inst : Std.PRange.Least? α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [inst_6 : Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_7 : Std.Rxo.IsAlwaysFinite α] {i : ℕ},
  i < r.toArray.size → (Std.PRange.succMany? i Std.PRange.UpwardEnumerable.least).isSome = true
-- Mathlib.NumberTheory.Real.Irrational
Irrational.ne_rational : ∀ {x : ℝ}, Irrational x → ∀ (a b : ℤ), x ≠ ↑a / ↑b
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.degree_comp : ∀ {R : Type u} [inst : Semiring R] [NoZeroDivisors R] {p q : Polynomial R},
  0 < q.degree → (p.comp q).degree = p.degree * q.degree
-- Mathlib.CategoryTheory.Preadditive.LeftExact
/-- A cokernel-preserving functor between preadditive categories preserves binary coproducts.  -/
CategoryTheory.Functor.preservesBinaryCoproducts_of_preservesCokernels : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D)
  [F.PreservesZeroMorphisms]
  [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F],
  CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F
-- Init.Data.Array.MinMax
Array.min?_eq_some_iff : ∀ {α : Type u_1} {a : α} [inst : Min α] [inst_1 : LE α] {xs : Array α} [Std.IsLinearOrder α] [Std.LawfulOrderMin α],
  xs.min? = some a ↔ a ∈ xs ∧ ∀ b ∈ xs, a ≤ b
-- Mathlib.Topology.Order.LiminfLimsup
exists_seq_tendsto_limsup : ∀ {α : Type u_2} {β : Type u_3} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
  [OrderTopology α] [FirstCountableTopology α] {f : Filter β} [f.NeBot] [f.IsCountablyGenerated] {u : β → α},
  autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) exists_seq_tendsto_limsup._auto_1 →
    autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) exists_seq_tendsto_limsup._auto_3 →
      ∃ x, Filter.Tendsto (u ∘ x) Filter.atTop (nhds (Filter.limsup u f)) ∧ Filter.Tendsto x Filter.atTop f
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imI_zero : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : Zero R], QuaternionAlgebra.imI 0 = 0
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.instZeroSubtypeMem : {R : Type u_1} → [inst : NonUnitalNonAssocRing R] → (I : TwoSidedIdeal R) → Zero ↥I
-- Mathlib.Data.QPF.Multivariate.Constructions.Sigma
MvQPF.Pi.inst : {n : ℕ} → {A : Type u} → (F : A → TypeVec.{u} n → Type u) → [(α : A) → MvQPF (F α)] → MvQPF (MvQPF.Pi F)
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.mk : {V : Type u_1} →
  {W : Type u_2} →
    [inst : SeminormedAddCommGroup V] →
      [inst_1 : SeminormedAddCommGroup W] →
        (toFun : V → W) →
          (∀ (v₁ v₂ : V), toFun (v₁ + v₂) = toFun v₁ + toFun v₂) →
            (∃ C, ∀ (v : V), ‖toFun v‖ ≤ C * ‖v‖) → NormedAddGroupHom V W
-- Mathlib.Geometry.Convex.Cone.Dual
PointedCone.positive.congr_simp : ∀ (R : Type u_1) (E : Type u_2) [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : PartialOrder E] [inst_5 : IsOrderedAddMonoid E] [inst_6 : Module R E]
  [inst_7 : PosSMulMono R E], PointedCone.positive R E = PointedCone.positive R E
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.snd_comp_prod : ∀ {R : Type u_1} [inst : Semiring R] {M₁ : Type u_2} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R M₁] {M₂ : Type u_3} [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂] {M₃ : Type u_4} [inst_7 : TopologicalSpace M₃] [inst_8 : AddCommMonoid M₃]
  [inst_9 : Module R M₃] (f : M₁ →L[R] M₂) (g : M₁ →L[R] M₃), ContinuousLinearMap.snd R M₂ M₃ ∘SL f.prod g = g
-- Mathlib.Algebra.Order.Antidiag.Pi
Finset.nsmul_piAntidiag : ∀ {ι : Type u_1} [inst : DecidableEq ι] [inst_1 : DecidableEq (ι → ℕ)] (s : Finset ι) (m : ℕ) {n : ℕ},
  n ≠ 0 → n • s.piAntidiag m = {f ∈ s.piAntidiag (n * m) | ∀ i ∈ s, n ∣ f i}
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.SymmetricCategory.braiding_swap_eq_inv_braiding : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.SymmetricCategory C] (X Y : C), (β_ Y X).hom = (β_ X Y).inv
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.mem_toArray_iff_getKey?_eq_some_and_get?_eq_some : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {k : α} {v : β},
      (k, v) ∈ Std.DHashMap.Raw.Const.toArray m ↔ m.getKey? k = some k ∧ Std.DHashMap.Raw.Const.get? m k = some v
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.isNone_getElem?_toArray_roc_eq : ∀ {m n i : ℕ}, ((m<...=n).toArray[i]?.isNone = true) = (n ≤ i + m)
-- Lean.Structure
Lean.StructureResolutionOrderConflict.mk.injEq : ∀ (isDirectParent : Bool) (badParent : Lean.Name) (conflicts : Array (Bool × Lean.Name)) (isDirectParent_1 : Bool)
  (badParent_1 : Lean.Name) (conflicts_1 : Array (Bool × Lean.Name)),
  ({ isDirectParent := isDirectParent, badParent := badParent, conflicts := conflicts } =
      { isDirectParent := isDirectParent_1, badParent := badParent_1, conflicts := conflicts_1 }) =
    (isDirectParent = isDirectParent_1 ∧ badParent = badParent_1 ∧ conflicts = conflicts_1)
-- Mathlib.Algebra.Homology.HasNoLoop
ComplexShape.instHasNoLoopNatUp : (ComplexShape.up ℕ).HasNoLoop
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey!_insert_le_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α} {v : β}, (cmp (t.insert k v).minKey! k).isLE = true