mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
_private.Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes.0.CategoryTheory.Limits.WalkingPair.swap.match_1.splitter : (motive : CategoryTheory.Limits.WalkingPair → Sort u_1) →
  (x : CategoryTheory.Limits.WalkingPair) →
    (Unit → motive CategoryTheory.Limits.WalkingPair.left) →
      (Unit → motive CategoryTheory.Limits.WalkingPair.right) → motive x
-- Mathlib.Lean.Expr.Basic
/-- Gets the indices `i` (in ascending order) of the binders of a nested `.forallE`,
`(x₀ : A₀) → (x₁ : A₁) → ⋯ → X`, such that
- the binder `[xᵢ : Aᵢ]` has `instImplicit` `binderInfo`
-  `p Aᵢ` is `true`
- The rest of the type `(xᵢ₊₁ : Aᵢ₊₁) → ⋯ → X` does not depend on `xᵢ`. (It's in this sense that
  `xᵢ : Aᵢ` is "unused".)

Note that the argument to `p` may have loose bvars. This is a performance optimization.

This function runs `cleanupAnnotations` on each expression before examining it.

We see through `let`s, and do not increment the index when doing so. This behavior is compatible
with `forallBoundedTelescope`.
 -/
Lean.Expr.getUnusedForallInstanceBinderIdxsWhere : (Lean.Expr → Bool) → Lean.Expr → Array ℕ
-- Mathlib.Analysis.Calculus.FDeriv.Const
fderiv_of_notMem_tsupport : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E}, x ∉ tsupport f → fderiv 𝕜 f x = 0
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.beq : Lean.IR.FnBody → Lean.IR.FnBody → Bool
-- Mathlib.MeasureTheory.Group.Convolution
MeasureTheory.Measure.conv.eq_1 : ∀ {M : Type u_1} [inst : AddMonoid M] [inst_1 : MeasurableSpace M] (μ ν : MeasureTheory.Measure M),
  μ.conv ν = MeasureTheory.Measure.map (fun x => x.1 + x.2) (μ.prod ν)
-- Mathlib.Order.Filter.Partial
Filter.ptendsto'_def : ∀ {α : Type u} {β : Type v} (f : α →. β) (l₁ : Filter α) (l₂ : Filter β),
  Filter.PTendsto' f l₁ l₂ ↔ ∀ s ∈ l₂, f.preimage s ∈ l₁
-- Mathlib.GroupTheory.Perm.Centralizer
/-- Cardinality of the `Finset` of `Equiv.Perm α` of given `cycleType`  -/
Equiv.Perm.card_of_cycleType : ∀ (α : Type u_1) [inst : DecidableEq α] [inst_1 : Fintype α] (m : Multiset ℕ),
  {g | g.cycleType = m}.card =
    if m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then
      (Fintype.card α).factorial /
        ((Fintype.card α - m.sum).factorial * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m).factorial)
    else 0
-- Init.Prelude
/-- Is this syntax `.missing`?  -/
Lean.Syntax.isMissing : Lean.Syntax → Bool
-- Mathlib.CategoryTheory.Limits.Indization.ParallelPair
CategoryTheory.IndParallelPairPresentation.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} {f g : A ⟶ B}
  (I : Type v₁) [ℐ : CategoryTheory.SmallCategory I] [hI : CategoryTheory.IsFiltered I]
  (F₁ F₂ : CategoryTheory.Functor I C) (ι₁ : F₁.comp CategoryTheory.yoneda ⟶ (CategoryTheory.Functor.const I).obj A)
  (isColimit₁ : CategoryTheory.Limits.IsColimit { pt := A, ι := ι₁ })
  (ι₂ : F₂.comp CategoryTheory.yoneda ⟶ (CategoryTheory.Functor.const I).obj B)
  (isColimit₂ : CategoryTheory.Limits.IsColimit { pt := B, ι := ι₂ }) (φ ψ : F₁ ⟶ F₂)
  (hf : f = isColimit₁.map { pt := B, ι := ι₂ } (CategoryTheory.Functor.whiskerRight φ CategoryTheory.yoneda))
  (hg : g = isColimit₁.map { pt := B, ι := ι₂ } (CategoryTheory.Functor.whiskerRight ψ CategoryTheory.yoneda))
  (I_1 : Type v₁) (ℐ_1 : CategoryTheory.SmallCategory I_1) (hI_1 : CategoryTheory.IsFiltered I_1)
  (F₁_1 F₂_1 : CategoryTheory.Functor I_1 C)
  (ι₁_1 : F₁_1.comp CategoryTheory.yoneda ⟶ (CategoryTheory.Functor.const I_1).obj A)
  (isColimit₁_1 : CategoryTheory.Limits.IsColimit { pt := A, ι := ι₁_1 })
  (ι₂_1 : F₂_1.comp CategoryTheory.yoneda ⟶ (CategoryTheory.Functor.const I_1).obj B)
  (isColimit₂_1 : CategoryTheory.Limits.IsColimit { pt := B, ι := ι₂_1 }) (φ_1 ψ_1 : F₁_1 ⟶ F₂_1)
  (hf_1 : f = isColimit₁_1.map { pt := B, ι := ι₂_1 } (CategoryTheory.Functor.whiskerRight φ_1 CategoryTheory.yoneda))
  (hg_1 : g = isColimit₁_1.map { pt := B, ι := ι₂_1 } (CategoryTheory.Functor.whiskerRight ψ_1 CategoryTheory.yoneda)),
  ({ I := I, ℐ := ℐ, hI := hI, F₁ := F₁, F₂ := F₂, ι₁ := ι₁, isColimit₁ := isColimit₁, ι₂ := ι₂,
        isColimit₂ := isColimit₂, φ := φ, ψ := ψ, hf := hf, hg := hg } =
      { I := I_1, ℐ := ℐ_1, hI := hI_1, F₁ := F₁_1, F₂ := F₂_1, ι₁ := ι₁_1, isColimit₁ := isColimit₁_1, ι₂ := ι₂_1,
        isColimit₂ := isColimit₂_1, φ := φ_1, ψ := ψ_1, hf := hf_1, hg := hg_1 }) =
    (I = I_1 ∧
      ℐ ≍ ℐ_1 ∧
        F₁ ≍ F₁_1 ∧
          F₂ ≍ F₂_1 ∧ ι₁ ≍ ι₁_1 ∧ isColimit₁ ≍ isColimit₁_1 ∧ ι₂ ≍ ι₂_1 ∧ isColimit₂ ≍ isColimit₂_1 ∧ φ ≍ φ_1 ∧ ψ ≍ ψ_1)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.b₄.eq_1 : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R), W.b₄ = 2 * W.a₄ + W.a₁ * W.a₃
-- Std.Do.PredTrans
Std.Do.PredTrans.mk.inj : ∀ {ps : Std.Do.PostShape} {α : Type u} {trans : Std.Do.PostCond α ps → Std.Do.Assertion ps}
  {conjunctiveRaw : Std.Do.PredTrans.Conjunctive trans} {trans_1 : Std.Do.PostCond α ps → Std.Do.Assertion ps}
  {conjunctiveRaw_1 : Std.Do.PredTrans.Conjunctive trans_1},
  { trans := trans, conjunctiveRaw := conjunctiveRaw } = { trans := trans_1, conjunctiveRaw := conjunctiveRaw_1 } →
    trans = trans_1
-- Mathlib.Combinatorics.SimpleGraph.Ends.Defs
SimpleGraph.ComponentCompl.hom_mk : ∀ {V : Type u} {G : SimpleGraph V} {K L : Set V} {v : V} (vnL : v ∉ L) (h : K ⊆ L),
  SimpleGraph.ComponentCompl.hom h (G.componentComplMk vnL) = G.componentComplMk ⋯
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.add_smul_of_equiv : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} {P Q : Fin 3 → R},
  P ≈ Q → ∀ {u v : R}, IsUnit u → IsUnit v → W'.add (u • P) (v • Q) = u ^ 4 • W'.add P Q
-- Mathlib.RingTheory.FiniteType
/-- If a set `S` generates an additive monoid `M`, then the image of `M` generates, as algebra,
`R[M]`.  -/
MonoidAlgebra.freeAlgebra_lift_of_surjective_of_closure : ∀ {R : Type u_1} {M : Type u_2} [inst : Monoid M] [inst_1 : CommSemiring R] {S : Set M},
  Submonoid.closure S = ⊤ → Function.Surjective ⇑((FreeAlgebra.lift R) fun s => (MonoidAlgebra.of R M) ↑s)
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.getCastD.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] (a : α) (fallback : β a) (a_1 : α) (b : β a_1)
  (es : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.getCastD a fallback (Std.DHashMap.Internal.AssocList.cons a_1 b es) =
    if h : (a_1 == a) = true then cast ⋯ b else Std.DHashMap.Internal.AssocList.getCastD a fallback es
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.indepFun_add_left₀ : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10}
  {m : MeasurableSpace β} [inst : Add β] [MeasurableAdd₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iIndepFun f μ →
    (∀ (i : ι), AEMeasurable (f i) μ) → ∀ (i j k : ι), i ≠ k → j ≠ k → ProbabilityTheory.IndepFun (f i + f j) (f k) μ
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
/-- Naturality of the lax functoriality constraint, on the left.  -/
CategoryTheory.LaxFunctor.mapComp_naturality_left_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (self : CategoryTheory.LaxFunctor B CategoryTheory.Cat)
  {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (X : ↑(self.obj a)) {Z : ↑(self.obj c)}
  (h : (self.map (CategoryTheory.CategoryStruct.comp f' g)).toFunctor.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((self.mapComp f g).toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((self.map₂ (CategoryTheory.Bicategory.whiskerRight η g)).toNatTrans.app X)
        h) =
    CategoryTheory.CategoryStruct.comp ((self.map g).toFunctor.map ((self.map₂ η).toNatTrans.app X))
      (CategoryTheory.CategoryStruct.comp ((self.mapComp f' g).toNatTrans.app X) h)
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.nullHomotopicMap'_f : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} {k₂ k₁ k₀ : ι} (r₂₁ : c.Rel k₂ k₁) (r₁₀ : c.Rel k₁ k₀)
  (h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)),
  (Homotopy.nullHomotopicMap' h).f k₁ =
    CategoryTheory.CategoryStruct.comp (C.d k₁ k₀) (h k₀ k₁ r₁₀) +
      CategoryTheory.CategoryStruct.comp (h k₁ k₂ r₂₁) (D.d k₂ k₁)
-- Mathlib.Order.Heyting.Regular
Heyting.Regular.instBooleanAlgebra : {α : Type u_1} → [inst : HeytingAlgebra α] → BooleanAlgebra (Heyting.Regular α)
-- Mathlib.CategoryTheory.Sites.Sieves
/-- A variant of `Sieve.sieveOfSubfunctor` with universe lifting.  -/
CategoryTheory.Sieve.sieveOfUliftSubfunctor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} →
      {R : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁))} →
        (R ⟶ CategoryTheory.uliftYoneda.{w, v₁, u₁}.obj X) → CategoryTheory.Sieve X
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Adjunction.instIsMonoidal : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [inst_4 : F.OplaxMonoidal],
  adj.IsMonoidal
-- Mathlib.RingTheory.Congruence.Defs
RingConGen.Rel.below.refl : ∀ {R : Type u_1} [inst : Add R] [inst_1 : Mul R] {r : R → R → Prop}
  {motive : (a a_1 : R) → RingConGen.Rel r a a_1 → Prop} (x : R), RingConGen.Rel.below ⋯
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.mem_coe_basicOpen : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (f : A) (x : ProjectiveSpectrum 𝒜),
  x ∈ ↑(ProjectiveSpectrum.basicOpen 𝒜 f) ↔ f ∉ x.asHomogeneousIdeal
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.insert_eq_insert : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] {p : α × β},
  insert p m = m.insert p.1 p.2
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.foldl_eq_foldl_toList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {δ : Type w} {f : δ → α → β → δ}
  {init : δ}, Std.TreeMap.foldl f init t = List.foldl (fun a b => f a b.1 b.2) init t.toList
-- Mathlib.GroupTheory.Coxeter.Length
CoxeterSystem.isReduced_reverse_iff : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B),
  cs.IsReduced ω.reverse ↔ cs.IsReduced ω
-- Mathlib.Topology.Algebra.Ring.Basic
/-- The (topological-space) closure of a subring of a topological ring is
itself a subring.  -/
Subring.topologicalClosure : {R : Type u_1} → [inst : TopologicalSpace R] → [inst_1 : Ring R] → [IsSemitopologicalRing R] → Subring R → Subring R
-- Mathlib.NumberTheory.Modular
/-- This was previously an auxiliary result en route to
`ModularGroup.eq_smul_self_of_mem_fdo_mem_fdo`. It is now deprecated, since the proof has been
refactored so this step is no longer needed.  -/
ModularGroup.c_eq_zero : ∀ {g : Matrix.SpecialLinearGroup (Fin 2) ℤ} {z : UpperHalfPlane},
  z ∈ ModularGroup.fdo → g • z ∈ ModularGroup.fdo → ↑g 1 0 = 0
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Matrix.charpoly_monic : ∀ {R : Type u} [inst : CommRing R] {n : Type v} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n R),
  M.charpoly.Monic
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.opcyclesIso_hom_δFromOpcycles : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.opcyclesIso_hom_δFromOpcycles._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.opcyclesIso_hom_δFromOpcycles._auto_3),
  CategoryTheory.CategoryStruct.comp (X.opcyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).hom
      (X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ hn₂) =
    (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).fromOpcycles
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
LinearMap.BilinForm.tensorDistrib.congr_simp : ∀ (R : Type uR) (A : Type uA) {M₁ : Type uM₁} {M₂ : Type uM₂} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M₁] [inst_3 : AddCommMonoid M₂] [inst_4 : Algebra R A] [inst_5 : Module R M₁]
  [inst_6 : Module A M₁] [inst_7 : SMulCommClass R A M₁] [inst_8 : IsScalarTower R A M₁] [inst_9 : Module R M₂],
  LinearMap.BilinForm.tensorDistrib R A = LinearMap.BilinForm.tensorDistrib R A
-- Std.Data.HashSet.Lemmas
Std.HashSet.ofList_nil : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α}, Std.HashSet.ofList [] = ∅
-- Mathlib.Tactic.DuplicateDecls
/-- Return the object by which to sort the module that `name` is from.
That is, the `libraryNumber` followed by the module as a string.  -/
_private.Mathlib.Tactic.DuplicateDecls.0.Mathlib.Tactic.DuplicateDecls.mkModuleKey! : Lean.Name → Lean.Environment → Mathlib.Tactic.DuplicateDecls.ModuleKey✝
-- Mathlib.Order.CompleteBooleanAlgebra
/-- `(a ⇨ ·)` is right adjoint to `(a ⊓ ·)`  -/
Order.Frame.le_himp_iff : ∀ {α : Type u_1} [self : Order.Frame α] (a b c : α), a ≤ b ⇨ c ↔ a ⊓ b ≤ c
-- Mathlib.SetTheory.Ordinal.Enum
Ordinal.enumOrd_inj : ∀ {s : Set Ordinal.{u}}, ¬BddAbove s → ∀ {a b : Ordinal.{u}}, Ordinal.enumOrd s a = Ordinal.enumOrd s b ↔ a = b
-- Lean.Parser.Extra
Lean.Parser.withOpenDecl.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Geometry.Manifold.PartitionOfUnity
/-- **Alias** of the reverse direction of `SmoothPartitionOfUnity.isSubordinate_toPartitionOfUnity`. -/
SmoothPartitionOfUnity.IsSubordinate.toPartitionOfUnity : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] {s : Set M} {f : SmoothPartitionOfUnity ι I M s} {U : ι → Set M},
  f.IsSubordinate U → f.toPartitionOfUnity.IsSubordinate U
-- Mathlib.CategoryTheory.Localization.Bousfield
CategoryTheory.ObjectProperty.isoClosure_isLocal : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C),
  P.isoClosure.isLocal = P.isLocal
-- Mathlib.CategoryTheory.Sites.Sieves
/-- the morphism which appear in the factorisation  -/
CategoryTheory.Presieve.FunctorPushforwardStructure.lift : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {X : C} →
            {S : CategoryTheory.Presieve X} →
              {Y : D} →
                {f : Y ⟶ F.obj X} →
                  (self : CategoryTheory.Presieve.FunctorPushforwardStructure F S f) → Y ⟶ F.obj self.preobj
-- Mathlib.Algebra.MonoidAlgebra.Module
/-- A copy of `Finsupp.lhom_ext'` for `MonoidAlgebra`.  -/
MonoidAlgebra.lhom_ext' : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring S] {N : Type u_7} [inst_1 : Semiring R]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R N] [inst_4 : Module R S] ⦃f g : MonoidAlgebra S M →ₗ[R] N⦄,
  (∀ (x : M), f ∘ₗ MonoidAlgebra.lsingle x = g ∘ₗ MonoidAlgebra.lsingle x) → f = g
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.of_keys_unit_perm : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α (fun x => Unit) cmp},
  t₁.keys.Perm t₂.keys → t₁.Equiv t₂
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.AdjoinPair.algebraMap_gen₁ : ∀ (K : Type u_1) {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (x y : L),
  (algebraMap (↥K⟮x, y⟯) L) (IntermediateField.AdjoinPair.gen₁ K x y) = x
-- Mathlib.Algebra.Order.CompleteField
ConditionallyCompleteLinearOrderedField.toIsOrderedCancelAddMonoid : ∀ {α : Type u_5} (self : ConditionallyCompleteLinearOrderedField α), IsOrderedCancelAddMonoid α
-- Mathlib.Control.Bitraversable.Instances
Const.bitraverse.eq_1 : ∀ {F : Type u → Type u} [inst : Applicative F] {α : Type u_1} {α' : Type u} {β : Type u_2} {β' : Type u} (f : α → F α')
  (f' : β → F β'), Const.bitraverse f f' = f
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.AbelNF.Config.mk.inj : ∀ {toConfig : Mathlib.Tactic.AtomM.Recurse.Config} {mode : Mathlib.Tactic.Abel.AbelMode}
  {toConfig_1 : Mathlib.Tactic.AtomM.Recurse.Config} {mode_1 : Mathlib.Tactic.Abel.AbelMode},
  { toConfig := toConfig, mode := mode } = { toConfig := toConfig_1, mode := mode_1 } →
    toConfig = toConfig_1 ∧ mode = mode_1
-- Mathlib.Data.Fin.VecNotation
Matrix.vecHead_vecAlt0 : ∀ {α : Type u} {m n : ℕ} (hm : m + 2 = n + 1 + (n + 1)) (v : Fin (m + 2) → α),
  Matrix.vecHead (Matrix.vecAlt0 hm v) = v 0
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.mem_of_mem_insertMany_list : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α},
  k ∈ t.insertMany l → (List.map Sigma.fst l).contains k = false → k ∈ t
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- Given a set `s`, `conjugatesOfSet s` is the set of all conjugates of
the elements of `s`.  -/
Group.conjugatesOfSet : {G : Type u_1} → [Group G] → Set G → Set G
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
MonoidAlgebra.coeff_domCongrBialgEquiv_apply : ∀ (R : Type u_1) (A : Type u_3) {M : Type u_8} {N : Type u_9} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Bialgebra R A] [inst_3 : Monoid M] [inst_4 : Monoid N] (e : M ≃* N) (a : MonoidAlgebra A M),
  ((MonoidAlgebra.domCongrBialgEquiv R A e) a).coeff = Finsupp.mapDomain (⇑e) a.coeff
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Functor.mapIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : C} (i : X ≅ Y), (F.mapIso i).inv = F.map i.inv
-- Mathlib.Algebra.Group.Subgroup.Finite
AddSubgroup.eq_bot_of_card_eq : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), Nat.card ↥H = 1 → H = ⊥
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.IsUpperSet.topology_eq : ∀ (α : Type u_1) [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsUpperSet α], inst_1 = Topology.upperSet α
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- Auxiliary definition for `costructuredArrowToOverEquivalence`.  -/
CategoryTheory.CostructuredArrow.costructuredArrowToOverEquivalence.functor : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor D T) →
          {X : T} →
            (Y : CategoryTheory.Over X) →
              CategoryTheory.Functor (CategoryTheory.CostructuredArrow (CategoryTheory.CostructuredArrow.toOver F X) Y)
                (CategoryTheory.CostructuredArrow F Y.left)
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
CategoryTheory.preservesFiniteColimits_liftToFinset : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {α : Type w}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_2 : CategoryTheory.Limits.HasFiniteBiproducts C]
  [CategoryTheory.Limits.HasFiniteColimits C],
  CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset C α)
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
CategoryTheory.Arrow.RightHomotopy.mk : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    [inst_1 : CategoryTheory.Preadditive V] →
      {u v : CategoryTheory.Arrow V} →
        {f g : u ⟶ v} →
          (hom : u.right ⟶ v.left) →
            autoParam
                (CategoryTheory.Arrow.Hom.right f - CategoryTheory.Arrow.Hom.right g =
                  CategoryTheory.CategoryStruct.comp hom v.hom)
                CategoryTheory.Arrow.RightHomotopy.comm._autoParam →
              CategoryTheory.Arrow.RightHomotopy f g
-- Lean.Meta.Constructions.BRecOn
/-- Constructs the `.below` definition for a inductive predicate.

For example for the `List` type, it constructs,
```
@[reducible] protected def List.below.{u} : {a : Type} → {motive : List a → Sort u} → List a → Sort (max 1 u) :=
fun {a} {motive} t => List.rec PUnit (fun a_1 a a_ih => motive a ×' a_ih) t
```
 -/
_private.Lean.Meta.Constructions.BRecOn.0.Lean.mkBelowFromRec : Lean.Name → ℕ → Lean.Name → Lean.MetaM Unit
-- Mathlib.Combinatorics.Quiver.Path
Quiver.Path.cons_ne_nil : ∀ {V : Type u} [inst : Quiver V] {a b : V} (p : Quiver.Path a b) (e : b ⟶ a), p.cons e ≠ Quiver.Path.nil
-- Mathlib.Data.ENNReal.Basic
ENNReal.bot_eq_zero : ⊥ = 0
-- Mathlib.Topology.UniformSpace.Defs
refl_mem_uniformity : ∀ {α : Type ua} [inst : UniformSpace α] {x : α} {s : SetRel α α}, s ∈ uniformity α → (x, x) ∈ s
-- Mathlib.MeasureTheory.Measure.Dirac
MeasureTheory.Measure.dirac_apply_ne_one_iff_eq_zero : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : Set α} {a : α},
  (MeasureTheory.Measure.dirac a) s ≠ 1 ↔ (MeasureTheory.Measure.dirac a) s = 0
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
Delone.DeloneSet.mapBilipschitz_coveringRadius : ∀ {X : Type u_1} {Y : Type u_2} [inst : MetricSpace X] [inst_1 : MetricSpace Y] (f : X ≃ Y) (K₁ K₂ : NNReal)
  (hK₁ : 0 < K₁) (hK₂ : 0 < K₂) (hf₁ : AntilipschitzWith K₁ ⇑f) (hf₂ : LipschitzWith K₂ ⇑f) (D : Delone.DeloneSet X),
  (Delone.DeloneSet.mapBilipschitz f K₁ K₂ hK₁ hK₂ hf₁ hf₂ D).coveringRadius = K₂ * D.coveringRadius
-- Mathlib.Algebra.GroupWithZero.Units.Basic
Ring.inverse_inverse_inverse : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] {a : M₀}, Ring.inverse (Ring.inverse (Ring.inverse a)) = Ring.inverse a
-- Mathlib.Algebra.Order.UpperLower
UpperSet.instMul : {α : Type u_1} → [inst : CommGroup α] → [inst_1 : Preorder α] → [IsOrderedMonoid α] → Mul (UpperSet α)
-- Batteries.Data.List.Basic
List.zipWithLeft'.eq_def : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β → γ) (x : List α) (x_1 : List β),
  List.zipWithLeft' f x x_1 =
    match x, x_1 with
    | [], bs => ([], bs)
    | a :: as, [] => (List.map (fun a => f a none) (a :: as), [])
    | a :: as, b :: bs =>
      have r := List.zipWithLeft' f as bs;
      (f a (some b) :: r.1, r.2)
-- Mathlib.Analysis.Calculus.FDeriv.Symmetric
isSymmSndFDerivAt_iff_iteratedFDeriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E},
  IsSymmSndFDerivAt 𝕜 f x ↔
    ContinuousMultilinearMap.domDomCongr Fin.revPerm (iteratedFDeriv 𝕜 2 f x) = iteratedFDeriv 𝕜 2 f x
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
SSet.Subcomplex.Pairing.union : ∀ {X : SSet} {A : X.Subcomplex} (self : A.Pairing), self.I ∪ self.II = Set.univ
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.weightedOrder.eq_1 : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (w : σ → ℕ) (f : MvPowerSeries σ R),
  MvPowerSeries.weightedOrder w f = if x : f = 0 then ⊤ else ↑(Nat.find ⋯)
-- Mathlib.Algebra.Order.Group.Action.Synonym
Lex.instVAddAssocClass : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : VAdd M N] [inst_1 : VAdd M α] [inst_2 : VAdd N α]
  [VAddAssocClass M N α], VAddAssocClass (Lex M) N α
-- Mathlib.Order.InitialSeg
PrincipalSeg.relIsoTrans_top : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (f : r ≃r s)
  (g : PrincipalSeg s t), (PrincipalSeg.relIsoTrans f g).top = g.top
-- Mathlib.CategoryTheory.Comma.Over.OverClass
CategoryTheory.instIsOverTower_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (S : C) [inst_1 : CategoryTheory.OverClass X S],
  CategoryTheory.IsOverTower X S S