mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.Embedding.Extend
/-- The extension of a single complex is a single complex.  -/
HomologicalComplex.extendSingleIso : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
              [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
                [inst_3 : DecidableEq ι] →
                  (e : c.Embedding c') →
                    (X : C) →
                      [inst_4 : DecidableEq ι'] →
                        (i : ι) →
                          (i' : ι') →
                            e.f i = i' →
                              (((HomologicalComplex.single C c i).obj X).extend e ≅
                                (HomologicalComplex.single C c' i').obj X)
-- Mathlib.SetTheory.Cardinal.Basic
Set.countable_infinite_iff_nonempty_denumerable : ∀ {α : Type u_1} {s : Set α}, s.Countable ∧ s.Infinite ↔ Nonempty (Denumerable ↑s)
-- Mathlib.GroupTheory.Torsion
AddCommGroup.freeRank_eq_zero_iff : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : AddGroup.FG G], AddCommGroup.freeRank G = 0 ↔ IsAddTorsion G
-- Mathlib.MeasureTheory.Measure.NullMeasurable
Set.Finite.nullMeasurableSet_sInter : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set (Set α)},
  s.Finite → (∀ t ∈ s, MeasureTheory.NullMeasurableSet t μ) → MeasureTheory.NullMeasurableSet (⋂₀ s) μ
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.succ.match_1.eq_1 : ∀ {n : ℕ} (motive : Fin n → Sort u_1) (i : ℕ) (h : i < n) (h_1 : (i : ℕ) → (h : i < n) → motive ⟨i, h⟩),
  (match ⟨i, h⟩ with
    | ⟨i, h⟩ => h_1 i h) =
    h_1 i h
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.getKey?.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a : α) (x : List ((a : α) × β a)),
  Std.Internal.List.getKey? a x =
    match x with
    | [] => none
    | ⟨k, snd⟩ :: l => bif k == a then some k else Std.Internal.List.getKey? a l
-- Mathlib.Data.DFinsupp.Ext
DFinsupp.add_closure_iUnion_range_single : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddZeroClass (β i)],
  AddSubmonoid.closure (⋃ i, Set.range (DFinsupp.single i)) = ⊤
-- Mathlib.Topology.MetricSpace.IsometricSMul
dist_vadd : ∀ {M : Type u} {X : Type w} [inst : PseudoMetricSpace X] [inst_1 : VAdd M X] [IsIsometricVAdd M X] (c : M) (x y : X),
  dist (c +ᵥ x) (c +ᵥ y) = dist x y
-- Mathlib.GroupTheory.CosetCover
Subgroup.exists_finiteIndex_of_leftCoset_cover_aux : ∀ {G : Type u_1} [inst : Group G] {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι},
  ⋃ i ∈ s, g i • ↑(H i) = Set.univ →
    ∀ [inst_1 : DecidableEq (Subgroup G)],
      ∀ j ∈ s, ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ → ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
-- Mathlib.Algebra.AffineMonoid.UniqueSums
AffineAddMonoid.to_twoUniqueSums : ∀ {M : Type u_1} [inst : AddCancelCommMonoid M] [AddMonoid.FG M] [IsAddTorsionFree M], TwoUniqueSums M
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_unsat : ∀ (ctx : Int.Internal.Linear.Context) (p₁ p₂ p₃ : Int.Internal.Linear.Poly) (d α β : ℤ),
  Int.Internal.Linear.cooper_unsat_cert p₁ p₂ p₃ d α β = true →
    Int.Internal.Linear.Poly.denote' ctx p₁ ≤ 0 →
      Int.Internal.Linear.Poly.denote' ctx p₂ ≤ 0 → d ∣ Int.Internal.Linear.Poly.denote' ctx p₃ → False
-- Mathlib.CategoryTheory.Triangulated.Orthogonal
CategoryTheory.ObjectProperty.leftOrthogonal.map_bijective_of_isTriangulated : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {P : CategoryTheory.ObjectProperty C} [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  [P.IsTriangulated] [CategoryTheory.IsTriangulated C] {X : C},
  P.leftOrthogonal X → ∀ (L : CategoryTheory.Functor C D) [L.IsLocalization P.trW] (Y : C), Function.Bijective L.map
-- Mathlib.Algebra.Order.Nonneg.Basic
Nonneg.coe_nsmul : ∀ {α : Type u_1} [inst : AddMonoid α] [inst_1 : Preorder α] [inst_2 : AddLeftMono α] (n : ℕ) (a : { x // 0 ≤ x }),
  ↑(n • a) = n • ↑a
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint.match_3.eq_1 : ∀ {n : ℕ} (motive : Option (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)) → Sort u_1)
  (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)
  (h_1 : (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → motive (some (some c)))
  (h_2 : Unit → motive (some none)) (h_3 : Unit → motive none),
  (match some (some c) with
    | some (some c) => h_1 c
    | some none => h_2 ()
    | none => h_3 ()) =
    h_1 c
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.extend_π : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) {X : C} (f : X ⟶ c.pt),
  (c.extend f).π = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.const J).map f) c.π
-- Mathlib.Data.EReal.Basic
EReal.coe_ne_coe_iff : ∀ {x y : ℝ}, ↑x ≠ ↑y ↔ x ≠ y
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
Std.IterM.reverse_toListRev_ensureTermination : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α m β]
  [inst_3 : Std.Iterators.Finite α m] {it : Std.IterM m β}, List.reverse <$> it.ensureTermination.toListRev = it.toList
-- Mathlib.Algebra.Order.Interval.Set.SuccPred
Set.insert_Ico_right_eq_Ico_add_one : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : Add α] [SuccAddOrder α] {a b : α} [NoMaxOrder α],
  a ≤ b → insert b (Set.Ico a b) = Set.Ico a (b + 1)
-- Aesop.Stats.Report
Aesop.StatsReport.instToStringNanos : ToString Aesop.Nanos
-- Batteries.Data.Array.Match
/-- Validity condition to help with termination proofs  -/
Array.PrefixTable.valid : ∀ {α : Type u_1} (self : Array.PrefixTable α) {i : ℕ} (h : i < self.size), self.toArray[i].2 ≤ i
-- Init.Data.BitVec.Lemmas
BitVec.allOnes_xor : ∀ {w : ℕ} {x : BitVec w}, BitVec.allOnes w ^^^ x = ~~~x
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
_private.Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks.0.CategoryTheory.Limits.cospanOp.match_1.eq_3 : ∀ (motive : CategoryTheory.Limits.WalkingCospan → Sort u_1) (h_1 : Unit → motive none)
  (h_2 : Unit → motive (some CategoryTheory.Limits.WalkingPair.left))
  (h_3 : Unit → motive (some CategoryTheory.Limits.WalkingPair.right)),
  (match some CategoryTheory.Limits.WalkingPair.right with
    | none => h_1 ()
    | some CategoryTheory.Limits.WalkingPair.left => h_2 ()
    | some CategoryTheory.Limits.WalkingPair.right => h_3 ()) =
    h_3 ()
-- Mathlib.Algebra.Group.Prod
AddEquiv.prodUnique_apply : ∀ {M : Type u_3} {N : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] [inst_2 : Unique N] (a : M × N),
  AddEquiv.prodUnique a = a.1
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.pullback_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : Y ⟶ X) (R : CategoryTheory.Presieve Z)
  (g : X ⟶ Z),
  CategoryTheory.Presieve.pullback (CategoryTheory.CategoryStruct.comp f g) R =
    CategoryTheory.Presieve.pullback f (CategoryTheory.Presieve.pullback g R)
-- Mathlib.Analysis.RCLike.Basic
RCLike.abs_im_div_norm_le_one : ∀ {K : Type u_1} [inst : RCLike K] (z : K), |RCLike.im z / ‖z‖| ≤ 1
-- Lean.Environment
_private.Lean.Environment.0.Lean.AsyncConsts.mk.sizeOf_spec : ∀ (size : ℕ) (revList : List Lean.AsyncConst✝) (map : Lean.NameMap Lean.AsyncConst✝)
  (normalizedTrie : Lean.NameTrie Lean.AsyncConst✝),
  sizeOf { size := size, revList := revList, map := map, normalizedTrie := normalizedTrie } =
    1 + sizeOf size + sizeOf revList + sizeOf map + sizeOf normalizedTrie
-- Mathlib.Order.CompleteBooleanAlgebra
/-- **Alias** of `sdiff_iInf_eq`. -/
sdiff_iSup_eq : ∀ {α : Type u} {ι : Sort w} [inst : Order.Coframe α] {a : α} {f : ι → α}, a \ ⨅ x, f x = ⨆ x, a \ f x
-- Mathlib.Algebra.Order.Star.Conjneg
conjneg_neg' : ∀ {G : Type u_1} {R : Type u_2} [inst : AddGroup G] [inst_1 : CommRing R] [inst_2 : PartialOrder R]
  [inst_3 : StarRing R] [StarOrderedRing R] {f : G → R}, conjneg f < 0 ↔ f < 0
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
/-- An `AlgHom` between two rings restricts to an `AlgHom` from any subalgebra of the
domain onto the image of that subalgebra.  -/
AlgHom.subalgebraMap : {R : Type u} →
  {A : Type v} →
    {B : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : Semiring B] →
              [inst_4 : Algebra R B] → (S : Subalgebra R A) → (f : A →ₐ[R] B) → ↥S →ₐ[R] ↥(Subalgebra.map f S)
-- Mathlib.Analysis.Distribution.Support
Distribution.TemperedDistribution.dsupport_delta : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] (x : E),
  Distribution.dsupport ⇑(TemperedDistribution.delta x) = {x}
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.join_comm : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P Q : l}, Lean.Order.join P Q = Lean.Order.join Q P
-- Mathlib.Topology.Category.LightProfinite.Basic
LightDiagram.mk.inj : ∀ {diagram : CategoryTheory.Functor ℕᵒᵖ FintypeCat}
  {cone : CategoryTheory.Limits.Cone (diagram.comp FintypeCat.toProfinite)}
  {isLimit : CategoryTheory.Limits.IsLimit cone} {diagram_1 : CategoryTheory.Functor ℕᵒᵖ FintypeCat}
  {cone_1 : CategoryTheory.Limits.Cone (diagram_1.comp FintypeCat.toProfinite)}
  {isLimit_1 : CategoryTheory.Limits.IsLimit cone_1},
  { diagram := diagram, cone := cone, isLimit := isLimit } =
      { diagram := diagram_1, cone := cone_1, isLimit := isLimit_1 } →
    diagram = diagram_1 ∧ cone ≍ cone_1 ∧ isLimit ≍ isLimit_1
-- Mathlib.SetTheory.ZFC.PSet
PSet.Subset.congr_left : ∀ {x y z : PSet.{u_1}}, x.Equiv y → (x ⊆ z ↔ y ⊆ z)
-- Mathlib.Data.List.Basic
/-- If the first element of two lists are different, then a sublist relation can be reduced.  -/
List.Sublist.of_cons_of_ne : ∀ {α : Type u} {l₁ l₂ : List α} {a b : α}, a ≠ b → (a :: l₁).Sublist (b :: l₂) → (a :: l₁).Sublist l₂
-- Mathlib.Algebra.Group.Submonoid.MulAction
/-- The additive action by an `AddSubmonoid` is the action by the underlying `AddMonoid`.  -/
AddSubmonoid.addAction : {M' : Type u_1} → {α : Type u_2} → [inst : AddMonoid M'] → [AddAction M' α] → (S : AddSubmonoid M') → AddAction (↥S) α
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
HomotopicalAlgebra.RightHomotopyRel.precomp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] {f g : X ⟶ Y},
  HomotopicalAlgebra.RightHomotopyRel f g →
    ∀ {Z : C} (i : Z ⟶ X),
      HomotopicalAlgebra.RightHomotopyRel (CategoryTheory.CategoryStruct.comp i f)
        (CategoryTheory.CategoryStruct.comp i g)
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletion.equiv_apply : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  (self : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v),
  (IsDedekindDomain.HeightOneSpectrum.adicCompletion.equiv K v) self = self.toCompletion
-- Mathlib.RingTheory.Ideal.KrullsHeightTheorem
ringKrullDim_le_ringKrullDim_quotient_add_spanFinrank : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R],
  ∀ I ≤ Ring.jacobson R, ringKrullDim R ≤ ringKrullDim (R ⧸ I) + ↑(Submodule.spanFinrank I)
-- Mathlib.Order.Bounds.Basic
bddBelow_preimage_toDual : ∀ {α : Type u_1} [inst : Preorder α] {s : Set αᵒᵈ}, BddBelow (⇑OrderDual.toDual ⁻¹' s) ↔ BddAbove s
-- Mathlib.Order.Interval.Set.ProjIcc
Monotone.IicExtend : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Preorder β] {b : α} {f : ↑(Set.Iic b) → β},
  Monotone f → Monotone (Set.IicExtend f)
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
/-- **Alias** of the reverse direction of `upperHemicontinuousAt_iff_forall_isOpen`. -/
UpperHemicontinuousAt.of_forall_isOpen : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → Set β} {x : α} [inst_1 : TopologicalSpace β],
  (∀ (u : Set β), IsOpen u → f x ⊆ u → ∀ᶠ (x' : α) in nhds x, f x' ⊆ u) → UpperHemicontinuousAt f x
-- Mathlib.Analysis.Complex.Exponential
Real.exp_eq_exp : ∀ {x y : ℝ}, Real.exp x = Real.exp y ↔ x = y
-- Mathlib.NumberTheory.FLT.MasonStothers
_private.Mathlib.NumberTheory.FLT.MasonStothers.0.abc_subcall : ∀ {k : Type u_1} [inst : Field k] [inst_1 : DecidableEq k] {a b c w : Polynomial k} {hw : w ≠ 0},
  w = a.wronskian b →
    a ≠ 0 →
      b ≠ 0 →
        c ≠ 0 →
          EuclideanDomain.divRadical (a * b * c) ∣ w →
            c.natDegree + 1 ≤ (UniqueFactorizationMonoid.radical (a * b * c)).natDegree
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
SimpleGraph.Walk.map_id : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), SimpleGraph.Walk.map SimpleGraph.Hom.id p = p
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.IsComplete.isNonempty : ∀ {α : Type u_1} {H : Hypergraph α}, H.IsComplete → H.IsNonempty
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Finite
/-- **Alias** of the reverse direction of `Set.infinite_vadd_set`. -/
Set.Infinite.vadd_set : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {a : G} {s : Set α},
  s.Infinite → (a +ᵥ s).Infinite
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.exists_edist_eq_radius_of_finite : ∀ {α : Type u_1} {G : SimpleGraph α} [Nonempty α] [Finite α], ∃ u v, G.edist u v = G.radius
-- Mathlib.CategoryTheory.Discrete.Basic
/-- A variant of `eqToHom` that lifts terms to the discrete category.  -/
CategoryTheory.Discrete.eqToHom' : {α : Type u₁} → {a b : α} → a = b → ({ as := a } ⟶ { as := b })
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- If `α` has a unique term, then the type of function `α → β` is measurably equivalent to `β`.  -/
MeasurableEquiv.funUnique : (α : Type u_8) → (β : Type u_9) → [Unique α] → [inst : MeasurableSpace β] → (α → β) ≃ᵐ β
-- Init.Data.Vector.Attach
Vector.attach_push : ∀ {α : Type u_1} {n : ℕ} {a : α} {xs : Vector α n},
  (xs.push a).attach =
    (Vector.map
          (fun x =>
            match x with
            | ⟨x, h⟩ => ⟨x, ⋯⟩)
          xs.attach).push
      ⟨a, ⋯⟩
-- Mathlib.MeasureTheory.OuterMeasure.Caratheodory
MeasureTheory.OuterMeasure.isCaratheodory_sdiff : ∀ {α : Type u} (m : MeasureTheory.OuterMeasure α) {s₁ s₂ : Set α},
  m.IsCaratheodory s₁ → m.IsCaratheodory s₂ → m.IsCaratheodory (s₁ \ s₂)
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
Quotient.borelSpace : ∀ {X : Type u_3} [inst : TopologicalSpace X] [PolishSpace X] [inst_2 : MeasurableSpace X] [BorelSpace X] {s : Setoid X}
  [T0Space (Quotient s)] [SecondCountableTopology (Quotient s)], BorelSpace (Quotient s)
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.IsBase.fundCircuit_isCircuit : ∀ {α : Type u_1} {M : Matroid α} {x : α} {B : Set α}, M.IsBase B → x ∈ M.E → x ∉ B → M.IsCircuit (M.fundCircuit x B)
-- Mathlib.AlgebraicGeometry.Morphisms.LocalClosure
AlgebraicGeometry.sourceLocalClosure.instIsZariskiLocalAtSourceIsOpenImmersionOfRespectsIsoOfRespectsLeftScheme : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.RespectsIso]
  [P.RespectsLeft AlgebraicGeometry.IsOpenImmersion],
  AlgebraicGeometry.IsZariskiLocalAtSource (AlgebraicGeometry.sourceLocalClosure AlgebraicGeometry.IsOpenImmersion P)
-- Mathlib.NumberTheory.SelbergSieve
/-- The main sum we get from Λ² coefficients is a quadratic form. Used to prove the Selberg sieve
identity by choosing weights that maximize this sum.  -/
BoundingSieve.mainSum_lambdaSquared_eq_sum_sum_mul : ∀ {s : BoundingSieve} (w : ℕ → ℝ),
  BoundingSieve.mainSum (BoundingSieve.lambdaSquared w) =
    ∑ d1 ∈ s.prodPrimes.divisors, ∑ d2 ∈ s.prodPrimes.divisors, s.nu d1 * w d1 * s.nu d2 * w d2 * (s.nu (d1.gcd d2))⁻¹
-- Init.Prelude
Mod.mk : {α : Type u} → (α → α → α) → Mod α
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.norm_num_ext.isNat_not_lucasLehmerTest : ∀ {p np : ℕ}, Mathlib.Meta.NormNum.IsNat p np → ¬LucasLehmerTest np → ¬LucasLehmerTest p
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.neighborSet_fst_subgraphOfAdj : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} (hvw : G.Adj v w), (G.subgraphOfAdj hvw).neighborSet v = {w}
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.FinStronglyMeasurable.fin_support_approx : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → β} [inst : Zero β]
  [inst_1 : TopologicalSpace β] (hf : MeasureTheory.FinStronglyMeasurable f μ) (n : ℕ),
  μ (Function.support ⇑(hf.approx n)) < ⊤
-- Mathlib.SetTheory.Cardinal.Finite
Nat.card_pos_iff : ∀ {α : Type u_1}, 0 < Nat.card α ↔ Nonempty α ∧ Finite α
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.XIsoOfEq_inv_comp_XIsoOfEq_hom_assoc : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (K : HomologicalComplex V c) {p₁ p₂ p₃ : ι}
  (h₂₁ : p₂ = p₁) (h₂₃ : p₂ = p₃) {Z : V} (h : K.X p₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h₂₁).inv (CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h₂₃).hom h) =
    CategoryTheory.CategoryStruct.comp (K.XIsoOfEq ⋯).hom h
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get!_diff_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {k : α} [inst_1 : Inhabited (β k)], k ∉ m₁ → (m₁ \ m₂).get! k = default
-- Lean.Message
Lean.MessageData.instAppend : Append Lean.MessageData
-- Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
/-- The pushout over the zero object is the coproduct.  -/
CategoryTheory.Limits.pushoutZeroZeroIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
        (X Y : C) → [inst_3 : CategoryTheory.Limits.HasBinaryCoproduct X Y] → CategoryTheory.Limits.pushout 0 0 ≅ X ⨿ Y
-- Mathlib.CategoryTheory.Types.Basic
CategoryTheory.Functor.map_comp_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (self : CategoryTheory.Functor C D) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) {F : D → D → Type uF} {carrier : D → Type w}
  {instFunLike : (X Y : D) → FunLike (F X Y) (carrier X) (carrier Y)} [inst_2 : CategoryTheory.ConcreteCategory D F]
  (x : carrier (self.obj X)),
  (CategoryTheory.ConcreteCategory.hom (self.map (CategoryTheory.CategoryStruct.comp f g))) x =
    (CategoryTheory.ConcreteCategory.hom (self.map g)) ((CategoryTheory.ConcreteCategory.hom (self.map f)) x)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMon.instHasZeroObject : ∀ {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} D]
  [inst_1 : CategoryTheory.SemiCartesianMonoidalCategory D],
  CategoryTheory.Limits.HasZeroObject (CategoryTheory.AddMon D)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.getD_erase : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {k a fallback : α}, (m.erase k).getD a fallback = if (k == a) = true then fallback else m.getD a fallback
-- Mathlib.CategoryTheory.Abelian.Opposite
CategoryTheory.imageUnopOp_inv_comp_op_factorThruImage : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {A B : Cᵒᵖ}
  (g : A ⟶ B),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.imageUnopOp g).inv
      (CategoryTheory.Limits.factorThruImage g.unop).op =
    CategoryTheory.Limits.image.ι g
-- Mathlib.Analysis.Normed.Module.Basic
NontriviallyNormedField.infinite : ∀ (𝕜 : Type u_1) [NontriviallyNormedField 𝕜], Infinite 𝕜
-- Mathlib.Order.Interval.Set.Monotone
Monotone.Iic : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Monotone f → Monotone fun x => Set.Iic (f x)
-- Mathlib.RingTheory.Etale.Basic
Algebra.FormallyEtale.comp_bijective : ∀ (R : Type u) (A : Type v) {B : Type u_1} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [Algebra.FormallyEtale R A] (I : Ideal B),
  I ^ 2 = ⊥ → Function.Bijective (Ideal.Quotient.mkₐ R I).comp
-- Mathlib.CategoryTheory.Limits.Final
/-- If `F` is initial,
the category of cones on `F ⋙ G` is equivalent to the category of cones on `G`,
for any `G : D ⥤ E`.
 -/
CategoryTheory.Functor.Initial.conesEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [F.Initial] →
            {E : Type u₃} →
              [inst_3 : CategoryTheory.Category.{v₃, u₃} E] →
                (G : CategoryTheory.Functor D E) → CategoryTheory.Limits.Cone (F.comp G) ≌ CategoryTheory.Limits.Cone G
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.measure_le_bound : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β)
  (a : α) (s : Set β), (κ a) s ≤ κ.bound
-- Mathlib.Data.Multiset.ZeroCons
Multiset.pmap_cons : ∀ {α : Type u_1} {β : Type v} {p : α → Prop} (f : (a : α) → p a → β) (a : α) (m : Multiset α) (h : ∀ b ∈ a ::ₘ m, p b),
  Multiset.pmap f (a ::ₘ m) h = f a ⋯ ::ₘ Multiset.pmap f m ⋯
-- Mathlib.Algebra.CharP.Defs
/-- The generator of the kernel of the unique homomorphism ℕ → R for a semiring R.

*Warning*: for a semiring `R`, `CharP R 0` and `CharZero R` need not coincide.
* `CharP R 0` asks that only `0 : ℕ` maps to `0 : R` under the map `ℕ → R`;
* `CharZero R` requires an injection `ℕ ↪ R`.

For instance, endowing `{0, 1}` with addition given by `max` (i.e. `1` is absorbing), shows that
`CharZero {0, 1}` does not hold and yet `CharP {0, 1} 0` does.
This example is formalized in `Counterexamples/CharPZeroNeCharZero.lean`.
 -/
CharP : (R : Type u_2) → [AddMonoidWithOne R] → outParam ℕ → Prop
-- Mathlib.Algebra.Order.Antidiag.Prod
Finset.HasMulAntidiagonal.sigmaMulAntidiagonalEquivProd_symm_apply_fst : ∀ {A : Type u_1} [inst : Monoid A] [inst_1 : Finset.HasMulAntidiagonal A] (x : A × A),
  (Finset.HasMulAntidiagonal.sigmaMulAntidiagonalEquivProd.symm x).fst = x.1 * x.2
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
/-- If `F` preserves a biproduct, we get a definitionally nice isomorphism
`F.obj (⨁ f) ≅ ⨁ (F.obj ∘ f)`.  -/
CategoryTheory.Functor.mapBiproduct : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            {J : Type w₁} →
              (F : CategoryTheory.Functor C D) →
                (f : J → C) →
                  [inst_4 : CategoryTheory.Limits.HasBiproduct f] →
                    [inst_5 : F.PreservesZeroMorphisms] →
                      [inst_6 : CategoryTheory.Limits.PreservesBiproduct f F] → F.obj (⨁ f) ≅ ⨁ F.obj ∘ f
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.vadd_finset_insert : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] (a : α) (b : β) (s : Finset β),
  a +ᵥ insert b s = insert (a +ᵥ b) (a +ᵥ s)
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
QuotientAddGroup.measurable_coe : ∀ {G : Type u_6} [inst : AddGroup G] [inst_1 : MeasurableSpace G] {S : AddSubgroup G}, Measurable QuotientAddGroup.mk