mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Filter.instIsCountablyGeneratedAtTopProd : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [Filter.atTop.IsCountablyGenerated] [inst_2 : Preorder β]
  [Filter.atTop.IsCountablyGenerated], Filter.atTop.IsCountablyGenerated
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.ΓSpec.adjunction_counit_app' : ∀ {R : CommRingCatᵒᵖ},
  AlgebraicGeometry.ΓSpec.adjunction.counit.app R = AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction.counit.app R
-- Mathlib.Topology.Homeomorph.Lemmas
/-- `Equiv.piCongrLeft` as a homeomorphism: this is the natural homeomorphism
`Π i, Y (e i) ≃ₜ Π j, Y j` obtained from a bijection `ι ≃ ι'`.  -/
Homeomorph.piCongrLeft : {ι : Type u_7} →
  {ι' : Type u_8} →
    {Y : ι' → Type u_9} →
      [inst : (j : ι') → TopologicalSpace (Y j)] → (e : ι ≃ ι') → ((i : ι) → Y (e i)) ≃ₜ ((j : ι') → Y j)
-- Mathlib.GroupTheory.Congruence.Basic
Con.quotientKerEquivOfRightInverse_apply : ∀ {M : Type u_1} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass P] (f : M →* P) (g : P → M)
  (hf : Function.RightInverse g ⇑f) (a : (Con.ker f).Quotient),
  (Con.quotientKerEquivOfRightInverse f g hf) a = (Con.kerLift f) a
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
/-- **Alias** of the reverse direction of `SimpleGraph.Walk.eq_nil_iff_nil`.

---

A walk with its endpoints defeq is `Nil` if and only if it is equal to `nil`.  -/
SimpleGraph.Walk.Nil.eq_nil : ∀ {V : Type u} {G : SimpleGraph V} {v : V} {p : G.Walk v v}, p.Nil → p = SimpleGraph.Walk.nil
-- Mathlib.AlgebraicGeometry.Modules.Tilde
/-- `M ↦ M^~` is an equivalence of categories from `ModuleCat R` to the full subcategory
of quasi-coherent `𝒪_{Spec R}`-modules.  -/
AlgebraicGeometry.tildeEquiv : {R : CommRingCat} →
  ModuleCat ↑R ≌ (SheafOfModules.isQuasicoherent (AlgebraicGeometry.Spec R).ringCatSheaf).FullSubcategory
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.Quotient.functor_homRel_eq_compClosure_eqvGen : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (r : HomRel C) {X Y : C} (f g : X ⟶ Y),
  (CategoryTheory.Quotient.functor r).homRel f g ↔ Relation.EqvGen (CategoryTheory.HomRel.CompClosure r) f g
-- Mathlib.MeasureTheory.MeasurableSpace.Instances
Bool.instMeasurableSingletonClass : MeasurableSingletonClass Bool
-- Mathlib.Tactic.Sat.FromLRAT
Mathlib.Tactic.Sat.Clause.mk.inj : ∀ {lits : Array ℤ} {expr proof : Lean.Expr} {lits_1 : Array ℤ} {expr_1 proof_1 : Lean.Expr},
  { lits := lits, expr := expr, proof := proof } = { lits := lits_1, expr := expr_1, proof := proof_1 } →
    lits = lits_1 ∧ expr = expr_1 ∧ proof = proof_1
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
/-- Given a functor `F : Set.Iic j ⥤ C` and `i : J` such that `i < j`,
this is the arrow `F.obj ⟨i, _⟩ ⟶ F.obj ⟨Order.succ i, _⟩`.  -/
CategoryTheory.SmallObject.SuccStruct.arrowSucc : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : LinearOrder J] →
        [SuccOrder J] → {j : J} → CategoryTheory.Functor (↑(Set.Iic j)) C → (i : J) → i < j → CategoryTheory.Arrow C
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.rightHomologyFunctorOpNatIso_hom_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasKernels C] [inst_3 : CategoryTheory.Limits.HasCokernels C]
  [inst_4 : CategoryTheory.Limits.HasKernels Cᵒᵖ] [inst_5 : CategoryTheory.Limits.HasCokernels Cᵒᵖ]
  (X : (CategoryTheory.ShortComplex C)ᵒᵖ),
  (CategoryTheory.ShortComplex.rightHomologyFunctorOpNatIso C).hom.app X = (Opposite.unop X).leftHomologyOpIso.inv
-- Lean.Meta.Basic
Lean.Meta.Context.keyedConfig : Lean.Meta.Context → Lean.Meta.ConfigWithKey
-- Mathlib.Algebra.Order.Floor.Defs
Nat.floor_int : Nat.floor = Int.toNat
-- Mathlib.Data.Set.Card
Set.encard_univ : ∀ (α : Type u_3), Set.univ.encard = ENat.card α
-- Mathlib.AlgebraicTopology.RelativeCellComplex.Basic
HomotopicalAlgebra.RelativeCellComplex.Cells.ι.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w'} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J] {α : J → Type t} {A B : (j : J) → α j → C}
  {basicCell : (j : J) → (i : α j) → A j i ⟶ B j i} {X Y : C} {f : X ⟶ Y}
  {c : HomotopicalAlgebra.RelativeCellComplex basicCell f} (γ : c.Cells),
  γ.ι = CategoryTheory.CategoryStruct.comp ((c.attachCells γ.j ⋯).cell γ.k) (c.incl.app (Order.succ γ.j))
-- Init.Data.ByteArray.Basic
ByteArray.instGetElemUSizeUInt8LtNatValToFinSize : GetElem ByteArray USize UInt8 fun xs i => ↑i.toFin < xs.size
-- Mathlib.Analysis.Convex.Approximation
/-- The real version of `univ_sSup_of_nat_affine_eq`.  -/
ConvexOn.real_univ_sSup_of_nat_affine_eq : ∀ {E : Type u_2} {φ : E → ℝ} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E]
  [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] [HereditarilyLindelofSpace E],
  LowerSemicontinuous φ →
    ConvexOn ℝ Set.univ φ →
      ∃ l c, (∀ (i : ℕ), ⇑(l i) + Function.const E (c i) ≤ φ) ∧ ⨆ i, ⇑(l i) + Function.const E (c i) = φ
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey!_eq_default_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α], m.WF → ∀ {a : α}, m.contains a = false → m.getKey! a = default
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.IsCondKernelCDF.toKernel_apply : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {x : MeasurableSpace β} {f : α × β → StieltjesFunction ℝ}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β}
  {hf : ProbabilityTheory.IsCondKernelCDF f κ ν} (p : α × β),
  (ProbabilityTheory.IsCondKernelCDF.toKernel f hf) p = (f p).measure
-- Init.Core
true_ne_false : ¬True = False
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.SmallObject.functorialFactorizationData_i_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [inst_3 : I.IsCardinalForSmallObjectArgument κ]
  (f : CategoryTheory.Arrow C),
  (CategoryTheory.SmallObject.functorialFactorizationData I κ).i.app f = CategoryTheory.SmallObject.ιObj I κ f.hom
-- Mathlib.Algebra.Star.Basic
/-- the maps preserve star  -/
StarHomClass.map_star : ∀ {F : Type u_1} {R : outParam (Type u_2)} {S : outParam (Type u_3)} {inst : Star R} {inst_1 : Star S}
  {inst_2 : FunLike F R S} [self : StarHomClass F R S] (f : F) (r : R), f (star r) = star (f r)
-- Mathlib.Topology.Algebra.InfiniteSum.Ring
/-- The family `(k, l) : ℕ × ℕ ↦ f k * g l` is summable if and only if the family
`(n, k, l) : Σ (n : ℕ), antidiagonal n ↦ f k * g l` is summable.  -/
summable_mul_prod_iff_summable_mul_sigma_antidiagonal : ∀ {α : Type u_3} {A : Type u_4} [inst : AddCommMonoid A] [inst_1 : Finset.HasAntidiagonal A]
  [inst_2 : TopologicalSpace α] [inst_3 : NonUnitalNonAssocSemiring α] {f g : A → α},
  (Summable fun x => f x.1 * g x.2) ↔ Summable fun x => f (↑x.snd).1 * g (↑x.snd).2
-- Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
/-- If `S` is a finite `R`-algebra, finitely presented as a module and as an algebra
is equivalent.  -/
Module.FinitePresentation.iff_finitePresentation_of_finite : ∀ (R : Type u) (S : Type u_1) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Module.Finite R S],
  Module.FinitePresentation R S ↔ Algebra.FinitePresentation R S
-- Init.Data.Int.OfNat
Nat.ToInt.finVal : ∀ {n : ℕ} {a : Fin n} {a' : ℤ}, ↑a = a' → ↑↑a = a'
-- Mathlib.RingTheory.GradedAlgebra.Basic
DirectSum.coe_decompose_mul_of_right_mem : ∀ {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddCommMonoid ι]
  [inst_3 : PartialOrder ι] [CanonicallyOrderedAdd ι] [inst_5 : SetLike σ A] [inst_6 : AddSubmonoidClass σ A]
  (𝒜 : ι → σ) [inst_7 : GradedRing 𝒜] {a b : A} {i : ι} [inst_8 : Sub ι] [OrderedSub ι] [AddLeftReflectLE ι] (n : ι)
  [inst_11 : Decidable (i ≤ n)],
  b ∈ 𝒜 i → ↑(((DirectSum.decompose 𝒜) (a * b)) n) = if i ≤ n then ↑(((DirectSum.decompose 𝒜) a) (n - i)) * b else 0
-- Mathlib.Algebra.Order.Group.CompleteLattice
ciSup_sub : ∀ {ι : Type u_1} {G : Type u_2} [inst : AddGroup G] [inst_1 : ConditionallyCompleteLattice G] [Nonempty ι] {f : ι → G}
  [AddRightMono G], BddAbove (Set.range f) → ∀ (a : G), (⨆ i, f i) - a = ⨆ i, f i - a
-- Mathlib.Topology.Semicontinuity.Basic
lowerSemicontinuousOn_neg_iff : ∀ {α : Type u_4} [inst : TopologicalSpace α] {β : Type u_5} {f : α → β} {s : Set α} [inst_1 : PartialOrder β]
  [inst_2 : AddCommGroup β] [IsOrderedAddMonoid β], LowerSemicontinuousOn (-f) s ↔ UpperSemicontinuousOn f s
-- Mathlib.Order.DirSupClosed
DirSupInaccOn.union : ∀ {α : Type u_1} {s t : Set α} {D : Set (Set α)} [inst : Preorder α],
  DirSupInaccOn D s → DirSupInaccOn D t → DirSupInaccOn D (s ∪ t)
-- Mathlib.Algebra.Group.Defs
Monoid.mk : {M : Type u} →
  [toSemigroup : Semigroup M] →
    [toOne : One M] →
      (∀ (a : M), 1 * a = a) →
        (∀ (a : M), a * 1 = a) →
          [toNPow : NPow M] →
            autoParam (∀ (x : M), x ^ 0 = 1) Monoid.npow_zero._autoParam →
              autoParam (∀ (n : ℕ) (x : M), x ^ (n + 1) = x ^ n * x) Monoid.npow_succ._autoParam → Monoid M
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.addSemigroup.eq_1 : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddSemigroup α],
  Finset.addSemigroup = Function.Injective.addSemigroup SetLike.coe ⋯ ⋯
-- Std.Tactic.BVDecide.LRAT.Internal.LRATCheckerSound
_private.Std.Tactic.BVDecide.LRAT.Internal.LRATCheckerSound.0.Std.Tactic.BVDecide.LRAT.Internal.lratChecker.match_3.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : List (Std.Tactic.BVDecide.LRAT.Action β α) → Sort u_3) →
      (prf : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
        (Unit → motive []) →
          ((id : ℕ) →
              (rupHints : Array ℕ) →
                (tail : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
                  motive (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints :: tail)) →
            ((id : ℕ) →
                (c : β) →
                  (rupHints : Array ℕ) →
                    (restPrf : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
                      motive (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints :: restPrf)) →
              ((id : ℕ) →
                  (c : β) →
                    (pivot : Std.Sat.Literal α) →
                      (rupHints : Array ℕ) →
                        (ratHints : Array (ℕ × Array ℕ)) →
                          (restPrf : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
                            motive (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints :: restPrf)) →
                ((ids : Array ℕ) →
                    (restPrf : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
                      motive (Std.Tactic.BVDecide.LRAT.Action.del ids :: restPrf)) →
                  motive prf
-- Mathlib.Topology.UniformSpace.Basic
instUniformSpaceProd : {α : Type ua} → {β : Type ub} → [u₁ : UniformSpace α] → [u₂ : UniformSpace β] → UniformSpace (α × β)
-- Mathlib.Data.Nat.Fib.Zeckendorf
/-- The Zeckendorf representation of a natural number.

Note: For unfolding, you should use the equational lemmas `Nat.zeckendorf_zero` and
`Nat.zeckendorf_of_pos` instead of the autogenerated one.  -/
Nat.zeckendorf : ℕ → List ℕ
-- Mathlib.CategoryTheory.Shift.Adjunction
/-- If `E : C ≌ D` is an equivalence and we have a `CommShift` structure on `E.inverse`,
this constructs the unique compatible `CommShift` structure on `E.functor`.
 -/
CategoryTheory.Equivalence.commShiftFunctor : {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] →
        (E : C ≌ D) →
          (A : Type u_3) →
            [inst_2 : AddGroup A] →
              [inst_3 : CategoryTheory.HasShift C A] →
                [inst_4 : CategoryTheory.HasShift D A] → [E.inverse.CommShift A] → E.functor.CommShift A
-- Mathlib.GroupTheory.Solvable
Group.IsSolvable.mk : ∀ {G : Type u_1} [inst : Group G], (∃ n, derivedSeries G n = ⊥) → Group.IsSolvable G
-- Std.Sat.AIG.Relabel
Std.Sat.AIG.relabel_size_eq_size : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {β : Type} [inst_2 : Hashable β] [inst_3 : DecidableEq β]
  {aig : Std.Sat.AIG α} {r : α → β}, (Std.Sat.AIG.relabel r aig).decls.size = aig.decls.size
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_sum_eq_prod_toLeft_mul_prod_toRight : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : CommMonoid M] (s : Finset (ι ⊕ κ)) (f : ι ⊕ κ → M),
  ∏ x ∈ s, f x = (∏ x ∈ s.toLeft, f (Sum.inl x)) * ∏ x ∈ s.toRight, f (Sum.inr x)
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.diagramIsoParallelFamily_hom_app : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor (CategoryTheory.Limits.WalkingParallelFamily J) C)
  (X : CategoryTheory.Limits.WalkingParallelFamily J),
  (CategoryTheory.Limits.diagramIsoParallelFamily F).hom.app X = CategoryTheory.eqToHom ⋯
-- Mathlib.CategoryTheory.Elements
_private.Mathlib.CategoryTheory.Elements.0.CategoryTheory.NatTrans.mapElements.match_1.splitter : {C : Type u_3} →
  [inst : CategoryTheory.Category.{u_2, u_3} C] →
    {F : CategoryTheory.Functor C (Type u_1)} →
      (motive : F.Elements → Sort u_4) → (x : F.Elements) → ((X : C) → (x : F.obj X) → motive ⟨X, x⟩) → motive x
-- Mathlib.Topology.EMetricSpace.PairReduction
PairReduction.card_le_logSizeRadius_le_pow_logSizeRadius : ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ENNReal} {V : Finset T} {t : T},
  1 < a →
    ↑{x ∈ V | edist t x ≤ ↑(PairReduction.logSizeRadius t V a c) * c}.card ≤ a ^ PairReduction.logSizeRadius t V a c
-- Mathlib.SetTheory.ZFC.PSet
PSet.instCoeSet : Coe PSet.{u_1} (Set PSet.{u_1})
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
/-- The norm, relative to `ℤ`, of `ζ ^ p ^ s - 1` in a `p ^ (k + 1)`-th cyclotomic extension of `ℚ`
is `p ^ p ^ s` if `s ≤ k` and `p ≠ 2`.  -/
IsPrimitiveRoot.norm_toInteger_pow_sub_one_of_prime_ne_two : ∀ {p k : ℕ} {K : Type u} [inst : Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [inst_1 : CharZero K]
  [IsCyclotomicExtension {p ^ (k + 1)} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) {s : ℕ},
  s ≤ k → p ≠ 2 → (Algebra.norm ℤ) (hζ.toInteger ^ p ^ s - 1) = ↑p ^ p ^ s
-- Mathlib.Order.Concept
Concept.instBoundedOrderConcept : {α : Type u_2} → {β : Type u_3} → {r : α → β → Prop} → BoundedOrder (Concept α β r)
-- Mathlib.Probability.Martingale.BorelCantelli
MeasureTheory.BorelCantelli.martingalePart_process_ae_eq : ∀ {Ω : Type u_2} {m0 : MeasurableSpace Ω} (ℱ : MeasureTheory.Filtration ℕ m0) (μ : MeasureTheory.Measure Ω)
  (s : ℕ → Set Ω) (n : ℕ),
  MeasureTheory.martingalePart (MeasureTheory.BorelCantelli.process s) ℱ μ n =
    ∑ k ∈ Finset.range n, ((s (k + 1)).indicator 1 - μ[(s (k + 1)).indicator 1 | ↑ℱ k])
-- Init.Data.Int.DivMod.Basic
_private.Init.Data.Int.DivMod.Basic.0.Int.fdiv.match_1.eq_4 : ∀ (motive : ℤ → ℤ → Sort u_1) (a : ℕ) (h_1 : (x : ℤ) → motive 0 x)
  (h_2 : (m n : ℕ) → motive (Int.ofNat m) (Int.ofNat n)) (h_3 : (m n : ℕ) → motive (Int.ofNat m.succ) (Int.negSucc n))
  (h_4 : (a : ℕ) → motive (Int.negSucc a) 0) (h_5 : (m n : ℕ) → motive (Int.negSucc m) (Int.ofNat n.succ))
  (h_6 : (m n : ℕ) → motive (Int.negSucc m) (Int.negSucc n)),
  (match Int.negSucc a, 0 with
    | 0, x => h_1 x
    | Int.ofNat m, Int.ofNat n => h_2 m n
    | Int.ofNat m.succ, Int.negSucc n => h_3 m n
    | Int.negSucc a, 0 => h_4 a
    | Int.negSucc m, Int.ofNat n.succ => h_5 m n
    | Int.negSucc m, Int.negSucc n => h_6 m n) =
    h_4 a
-- Mathlib.CategoryTheory.Enriched.HomCongr
/-- Given isomorphisms `α : X ≅ X₁` and `β : Y ≅ Y₁` in `C`, we can construct
an isomorphism between `V` objects `X ⟶[V] Y` and `X₁ ⟶[V] Y₁`.  -/
CategoryTheory.Iso.eHomCongr : (V : Type u') →
  [inst : CategoryTheory.Category.{v', u'} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u} →
        [inst_2 : CategoryTheory.Category.{v, u} C] →
          [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V C] →
            {X Y X₁ Y₁ : C} → (X ≅ X₁) → (Y ≅ Y₁) → ((X ⟶[V] Y) ≅ X₁ ⟶[V] Y₁)
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.indepFun_prodMk : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : ι → Type u_10}
  {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ω → β i},
  ProbabilityTheory.iIndepFun f μ →
    (∀ (i : ι), Measurable (f i)) →
      ∀ (i j k : ι), i ≠ k → j ≠ k → ProbabilityTheory.IndepFun (fun a => (f i a, f j a)) (f k) μ
-- Batteries.Data.ByteArray
ByteArray.size_ofFn : ∀ {n : ℕ} (f : Fin n → UInt8), (ByteArray.ofFn f).size = n
-- Mathlib.Data.Sym.Basic
Sym.attach_mk : ∀ {α : Type u_1} {n : ℕ} {m : Multiset α} {hc : m.card = n}, (Sym.mk m hc).attach = Sym.mk m.attach ⋯
-- Init.Data.Sum.Basic
Sum.getRight_inr : ∀ {α : Type u_1} {β : Type u_2} {x : β} (h : (Sum.inr x).isRight = true), (Sum.inr x).getRight h = x
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
CategoryTheory.Over.prodLeftIsoPullback_hom_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (Y Z : CategoryTheory.Over X)
  [inst_1 : CategoryTheory.Limits.HasPullback Y.hom Z.hom] [inst_2 : CategoryTheory.Limits.HasBinaryProduct Y Z]
  {Z_1 : C} (h : Z.left ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (Y.prodLeftIsoPullback Z).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd Y.hom Z.hom) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left CategoryTheory.Limits.prod.snd) h
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Submodule
PresheafOfModules.Submodule.ι_app_hom_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M : PresheafOfModules R} (N : M.Submodule) (X : Cᵒᵖ) (a : ↑(N.toPresheafOfModules.presheaf.obj X)),
  (ModuleCat.Hom.hom (N.ι.app X)) a =
    (CategoryTheory.ConcreteCategory.hom (AddCommGrpCat.ofHom (N.obj X).subtype.toAddMonoidHom)) a
-- Mathlib.Topology.Category.UniformSpace
/-- The completion functor is left adjoint to the forgetful functor.  -/
UniformSpaceCat.adj : UniformSpaceCat.completionFunctor ⊣ CategoryTheory.forget₂ CpltSepUniformSpace UniformSpaceCat
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.Hom.whiskerLeft.injEq : ∀ {C : Type u} (X : CategoryTheory.FreeMonoidalCategory C) {Y₁ Y₂ : CategoryTheory.FreeMonoidalCategory C}
  (f f_1 : Y₁.Hom Y₂),
  (CategoryTheory.FreeMonoidalCategory.Hom.whiskerLeft X f =
      CategoryTheory.FreeMonoidalCategory.Hom.whiskerLeft X f_1) =
    (f = f_1)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.ExplorationStep.gt.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {k : α → Ordering} (a a_1 : List ((a : α) × β a)),
  a = a_1 →
    ∀ (a_2 : α) (a_3 : k a_2 = Ordering.gt) (a_4 a_5 : β a_2),
      a_4 = a_5 →
        Std.DTreeMap.Internal.Impl.ExplorationStep.gt a a_2 a_3 a_4 =
          Std.DTreeMap.Internal.Impl.ExplorationStep.gt a_1 a_2 a_3 a_5
-- Mathlib.Data.Part
Part.left_dom_of_sub_dom : ∀ {α : Type u_1} [inst : Sub α] {a b : Part α}, (a - b).Dom → a.Dom
-- Mathlib.Order.SuccPred.Tree
IsPredArchimedean.findAtom_le : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] [inst_2 : IsPredArchimedean α] [inst_3 : OrderBot α]
  [inst_4 : DecidableEq α] (r : α), IsPredArchimedean.findAtom r ≤ r
-- Mathlib.Order.IsNormal
Order.IsNormal.mk : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β},
  StrictMono f → (∀ {a : α}, Order.IsSuccLimit a → f a ∈ lowerBounds (upperBounds (f '' Set.Iio a))) → Order.IsNormal f
-- Std.Net.Addr
Std.Net.IPv6Addr.mk.sizeOf_spec : ∀ (segments : Vector UInt16 8), sizeOf { segments := segments } = 1 + sizeOf segments
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RicSliceData.range : {α : Type u} → {β : α → Type v} → [inst : Ord α] → Std.DTreeMap.Internal.RicSliceData α β → Std.Ric α
-- Lean.Data.AssocList
Lean.AssocList.nil : {α : Type u} → {β : Type v} → Lean.AssocList α β
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.isoMk_hom_τ₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (e₁ : S₁.X₁ ≅ S₂.X₁) (e₂ : S₁.X₂ ≅ S₂.X₂) (e₃ : S₁.X₃ ≅ S₂.X₃)
  (comm₁₂ :
    autoParam (CategoryTheory.CategoryStruct.comp e₁.hom S₂.f = CategoryTheory.CategoryStruct.comp S₁.f e₂.hom)
      CategoryTheory.ShortComplex.isoMk._auto_1)
  (comm₂₃ :
    autoParam (CategoryTheory.CategoryStruct.comp e₂.hom S₂.g = CategoryTheory.CategoryStruct.comp S₁.g e₃.hom)
      CategoryTheory.ShortComplex.isoMk._auto_3),
  (CategoryTheory.ShortComplex.isoMk e₁ e₂ e₃ comm₁₂ comm₂₃).hom.τ₃ = e₃.hom
-- Init.Data.Int.DivMod.Lemmas
Int.emod_sub_cancel_right : ∀ {m n k : ℤ} (i : ℤ), (m - i) % n = (k - i) % n ↔ m % n = k % n
-- Mathlib.LinearAlgebra.Matrix.Vec
Matrix.vec_transpose : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} (A : Matrix m n R), A.transpose.vec = A.vec ∘ Prod.swap
-- Init.System.FilePath
/-- The list of all path separator characters supported on the current platform.

On platforms that support multiple separators, `System.FilePath.pathSeparator` is the “ideal” one
expected by users on the platform.
 -/
System.FilePath.pathSeparators : List Char
-- Init.Data.List.ToArray
List.swap_toArray : ∀ {α : Type u_1} (l : List α) (i j : ℕ) {hi : i < l.toArray.size} {hj : j < l.toArray.size},
  l.toArray.swap i j hi hj = ((l.set i l[j]).set j l[i]).toArray
-- Mathlib.Order.Category.FinPartOrd
FinPartOrd.largeCategory : CategoryTheory.LargeCategory FinPartOrd
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKey?.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (size : ℕ) (k' : α) (v : β k')
  (l r : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.inner size k' v l r).getKey? k =
    match compare k k' with
    | Ordering.lt => l.getKey? k
    | Ordering.gt => r.getKey? k
    | Ordering.eq => some k'
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.equalizerComparison_comp_π_assoc : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] (f g : X ⟶ Y) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D)
  [inst_2 : CategoryTheory.Limits.HasEqualizer f g] [inst_3 : CategoryTheory.Limits.HasEqualizer (G.map f) (G.map g)]
  {Z : D} (h : G.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizerComparison f g G)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizer.ι (G.map f) (G.map g)) h) =
    CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.equalizer.ι f g)) h
-- Mathlib.Algebra.Quandle
Quandle.fix_inv : ∀ {Q : Type u_1} [inst : Quandle Q] {x : Q}, Rack.invAct x x = x
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roo.isSome_succMany?_of_lt_length_toList : ∀ {α : Type u} {r : Std.Roo α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.Rxo.IsAlwaysFinite α] {i : ℕ},
  i < r.toList.length → (Std.PRange.succMany? (i + 1) r.lower).isSome = true
-- Init.Data.List.MapIdx
/-- Applies a function to each element of the list along with the index at which that element is found,
returning the list of results. In addition to the index, the function is also provided with a proof
that the index is valid.

`List.mapIdx` is a variant that does not provide the function with evidence that the index is valid.
 -/
List.mapFinIdx : {α : Type u_1} → {β : Type u_2} → (as : List α) → ((i : ℕ) → α → i < as.length → β) → List β