mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Finset.Defs
Finset.decidableExistsAndFinsetCoe : {α : Type u_1} → {s : Finset α} → {p : α → Prop} → [DecidablePred p] → Decidable (∃ a ∈ ↑s, p a)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.instBot : {R : Type u} → {M : Type v} → [inst : VAdd R M] → Bot (SubAddAction R M)
-- Mathlib.Data.Finset.Sups
Finset.infs_singleton : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeInf α] {s : Finset α} {b : α},
  s ⊼ {b} = Finset.image (fun x => x ⊓ b) s
-- Mathlib.RingTheory.Polynomial.Morse
/-- If the roots of `f` in `S` have at most one collision mod `p`, then a `MulSemiringAction` on
the roots in `S` must be the identity permutation or a transposition.

Such polynomials are called *Morse functions* in Section 4.4 of [serre-galois].  -/
Polynomial.Splits.toPermHom_apply_eq_one_or_isSwap_of_ncard_le_of_mem_inertia : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [inst_3 : IsDomain S]
  {G : Type u_3} [inst_4 : Group G] [inst_5 : MulSemiringAction G S] [inst_6 : SMulCommClass G R S] {f : Polynomial R}
  [inst_7 : DecidableEq ↑(f.rootSet S)],
  (Polynomial.map (algebraMap R S) f).Splits →
    ∀ (p : Ideal S) [inst_8 : p.IsPrime],
      (f.rootSet S).ncard ≤ (f.rootSet (S ⧸ p)).ncard + 1 →
        ∀ g ∈ Ideal.inertia G p,
          (MulAction.toPermHom G ↑(f.rootSet S)) g = 1 ∨ ((MulAction.toPermHom G ↑(f.rootSet S)) g).IsSwap
-- Mathlib.Geometry.Manifold.HasGroupoid
/-- Any charted space structure is compatible with the groupoid of all open partial
homeomorphisms.  -/
hasGroupoid_continuousGroupoid : ∀ {H : Type u} {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M],
  HasGroupoid M (continuousGroupoid H)
-- Mathlib.Order.Cover
/-- **Alias** of `exists_lt_lt_of_not_covBy`.

---

**Alias** of the forward direction of `not_covBy_iff`.

---

If `a < b`, then `b` does not cover `a` iff there's an element in between.  -/
LT.lt.exists_lt_lt : ∀ {α : Type u_1} [inst : LT α] {a b : α}, a < b → ¬a ⋖ b → ∃ c, a < c ∧ c < b
-- Lean.Data.Lsp.Basic
Lean.Lsp.MarkupContent.mk.inj : ∀ {kind : Lean.Lsp.MarkupKind} {value : String} {kind_1 : Lean.Lsp.MarkupKind} {value_1 : String},
  { kind := kind, value := value } = { kind := kind_1, value := value_1 } → kind = kind_1 ∧ value = value_1
-- Mathlib.Data.EReal.Operations
EReal.top_add_coe : ∀ (x : ℝ), ⊤ + ↑x = ⊤
-- Mathlib.Algebra.GradedMonoid
GradedMonoid.GMul.mk : {ι : Type u_1} → {A : ι → Type u_2} → [inst : Add ι] → ({i j : ι} → A i → A j → A (i + j)) → GradedMonoid.GMul A
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.content_X_mul : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : NormalizedGCDMonoid R] {p : Polynomial R},
  (Polynomial.X * p).content = p.content
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.instIsFiniteMeasureOnCompactsProdVolume : ∀ {X : Type u_4} {Y : Type u_5} [inst : TopologicalSpace X] [inst_1 : MeasureTheory.MeasureSpace X]
  [MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.volume] [inst_3 : TopologicalSpace Y]
  [inst_4 : MeasureTheory.MeasureSpace Y] [MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.volume],
  MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.volume
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
/-- **Alias** of the forward direction of `Subalgebra.finiteDimensional_toSubmodule`.

---

A `Subalgebra` is `FiniteDimensional` iff it is `FiniteDimensional` as a submodule.  -/
FiniteDimensional.of_subalgebra_toSubmodule : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Ring E] [inst_2 : Algebra F E] {S : Subalgebra F E},
  FiniteDimensional F ↥(Subalgebra.toSubmodule S) → FiniteDimensional F ↥S
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.rootSet_finite : ∀ {T : Type w} [inst : CommRing T] (p : Polynomial T) (S : Type u_1) [inst_1 : CommRing S] [inst_2 : IsDomain S]
  [inst_3 : Algebra T S], (p.rootSet S).Finite
-- Std.Time.Date.Unit.Month
Eq.mp.congr_simp : ∀ {α β : Sort u} (h : α = β) (a a_1 : α), a = a_1 → h.mp a = h.mp a_1
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.T.eq_1 : ∀ (R : Type u_1) [inst : CommRing R], Polynomial.Chebyshev.T R 0 = 1
-- Mathlib.Tactic.Abel
_private.Mathlib.Tactic.Abel.0.Mathlib.Tactic.Abel.instEvalTermAbelMode.evalTerm : Lean.Term → Lean.Elab.TermElabM (Mathlib.Tactic.Abel.AbelMode × Lean.Expr)
-- Mathlib.Probability.Kernel.IonescuTulcea.Maps
measurable_IicProdIoc : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : LocallyFiniteOrder ι] [inst_2 : DecidableLE ι] {X : ι → Type u_2}
  [inst_3 : LocallyFiniteOrderBot ι] [inst_4 : (i : ι) → MeasurableSpace (X i)] {m n : ι}, Measurable (IicProdIoc m n)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Walk.mapToSubgraph.eq_1 : ∀ {V : Type u} {G : SimpleGraph V} {u : V}, SimpleGraph.Walk.nil.mapToSubgraph = SimpleGraph.Walk.nil
-- Init.Control.Lawful.Basic
bind_congr : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Bind m] {x : m α} {f g : α → m β},
  (∀ (a : α), f a = g a) → x >>= f = x >>= g
-- Aesop.Script.UScriptToSScript
Aesop.Script.StepTree.brecOn_1.eq : ∀ {motive_1 : Aesop.Script.StepTree → Sort u} {motive_2 : Array Aesop.Script.StepTree → Sort u}
  {motive_3 : List Aesop.Script.StepTree → Sort u} (t : Array Aesop.Script.StepTree)
  (F_1 : (t : Aesop.Script.StepTree) → t.below → motive_1 t)
  (F_2 : (t : Array Aesop.Script.StepTree) → Aesop.Script.StepTree.below_1 t → motive_2 t)
  (F_3 : (t : List Aesop.Script.StepTree) → Aesop.Script.StepTree.below_2 t → motive_3 t),
  Aesop.Script.StepTree.brecOn_1 t F_1 F_2 F_3 = F_2 t (Aesop.Script.StepTree.brecOn_1.go t F_1 F_2 F_3).2
-- Lean.Meta.Tactic.Grind.Intro
_private.Lean.Meta.Tactic.Grind.Intro.0.Lean.Meta.Grind.instInhabitedIntroResult : Inhabited Lean.Meta.Grind.IntroResult✝
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile.0.Std.IterM.step_intermediateDropWhile.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : true = true → motive true) (h_2 : true = false → motive false),
  (match hP : true with
    | true => h_1 hP
    | false => h_2 hP) =
    h_1 ⋯
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.UInt64.toBitVec_cond : ∀ {c : Bool} {t e : UInt64}, (bif c then t else e).toBitVec = bif c then t.toBitVec else e.toBitVec
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- A fan over `f : β → C` consists of a collection of maps from an object `P` to every `f b`.  -/
CategoryTheory.Limits.Fan.mk : {β : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f : β → C} → (P : C) → ((b : β) → P ⟶ f b) → CategoryTheory.Limits.Fan f
-- Init.Data.SInt.Bitwise
Int32.or_eq_zero_iff : ∀ {a b : Int32}, a ||| b = 0 ↔ a = 0 ∧ b = 0
-- Mathlib.LinearAlgebra.Matrix.ZPow
Matrix.Commute.zpow_self : ∀ {n' : Type u_1} [inst : DecidableEq n'] [inst_1 : Fintype n'] {R : Type u_2} [inst_2 : CommRing R]
  (A : Matrix n' n' R) (n : ℤ), Commute (A ^ n) A
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
/-- The second left fraction.  -/
CategoryTheory.MorphismProperty.LeftFraction₃.snd : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} → {X Y : C} → W.LeftFraction₃ X Y → W.LeftFraction X Y
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.ascending_central_series_le_upper`.

---

Any ascending central series for a group is bounded above by the upper central series.  -/
ascending_central_series_le_upper : ∀ {G : Type u_1} [inst : Group G] (H : ℕ → Subgroup G),
  Subgroup.IsAscendingCentralSeries H → ∀ (n : ℕ), H n ≤ Subgroup.upperCentralSeries G n
-- Init.Data.SInt.Lemmas
Int16.eq_sub_iff_add_eq : ∀ {a b c : Int16}, a = c - b ↔ a + b = c
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
/-- The morphism between base objects.  -/
CategoryTheory.Pseudofunctor.CoGrothendieck.Hom.base : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} →
      {X Y : F.CoGrothendieck} → X.Hom Y → (X.base ⟶ Y.base)
-- Mathlib.LinearAlgebra.Finsupp.VectorSpace
FreeAbelianGroup.instFreeInt : ∀ {σ : Type u_1}, Module.Free ℤ (FreeAbelianGroup σ)
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- Equivalence of homomorphisms induced by isomorphisms of graphs.  -/
SimpleGraph.Iso.homCongr : {V : Type u_1} →
  {W : Type u_2} →
    {X : Type u_3} →
      {Y : Type u_4} →
        {G : SimpleGraph V} →
          {G' : SimpleGraph W} →
            G ≃g G' → {G'' : SimpleGraph X} → {G''' : SimpleGraph Y} → G'' ≃g G''' → G →g G'' ≃ G' →g G'''
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalOpposite.unmopFunctor_δ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y : Cᴹᵒᵖ),
  CategoryTheory.Functor.OplaxMonoidal.δ (CategoryTheory.unmopFunctor C) X Y = (β_ X.unmop Y.unmop).inv
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Functor.isEquivalence_iff_of_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (e : F ≅ G), F.IsEquivalence ↔ G.IsEquivalence
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.Relation.mul : ∀ {J : Type v} [inst : CategoryTheory.Category.{u, v} J] {F : CategoryTheory.Functor J MonCat} (j : J)
  (x y : ↑(F.obj j)),
  MonCat.Colimits.Relation F (MonCat.Colimits.Prequotient.of j (x * y))
    ((MonCat.Colimits.Prequotient.of j x).mul (MonCat.Colimits.Prequotient.of j y))
-- Mathlib.Order.Category.BddDistLat
/-- The equivalence between `BddDistLat` and itself induced by `OrderDual` both ways.  -/
BddDistLat.dualEquiv : BddDistLat ≌ BddDistLat
-- Mathlib.Order.Filter.Tendsto
Filter.tendsto_bot : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l : Filter β}, Filter.Tendsto f ⊥ l
-- Mathlib.Algebra.Group.Action.Basic
arrowAction.eq_1 : ∀ {G : Type u_7} {A : Type u_8} {B : Type u_9} [inst : DivisionMonoid G] [inst_1 : MulAction G A],
  arrowAction = { smul := fun g F a => F (g⁻¹ • a), mul_smul := ⋯, one_smul := ⋯ }
-- Mathlib.Analysis.Convex.StdSimplex
stdSimplexEquivIcc_one : ∀ (𝕜 : Type u_1) [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : IsOrderedRing 𝕜],
  (stdSimplexEquivIcc 𝕜) ⟨Pi.single 1 1, ⋯⟩ = 1
-- Mathlib.Order.Interval.Set.ProjIcc
Set.strictMonoOn_projIci : ∀ {α : Type u_1} [inst : LinearOrder α] {a : α}, StrictMonoOn (Set.projIci a) (Set.Ici a)
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.partialOrder : PartialOrder Cardinal.{u}
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
/-- The map `inCoordinates` for the tangent bundle is trivial on the model spaces  -/
inCoordinates_tangent_bundle_core_model_space : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_4}
  [inst_5 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} (x₀ x : H) (y₀ y : H') (ϕ : E →L[𝕜] E'),
  ContinuousLinearMap.inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x y₀ y ϕ = ϕ
-- Init.Data.Sum.Basic
Sum.instBEq.beq : {α : Type u_1} → {β : Type u_2} → [BEq α] → [BEq β] → α ⊕ β → α ⊕ β → Bool
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : BEq α] [inst_2 : Std.LawfulBEqOrd α] (h : t.WF) {l : List ((a : α) × β a)} {k : α}
  (h₁ : (List.map Sigma.fst l).contains k = false)
  {h' : Std.DTreeMap.Internal.Impl.contains k ↑(t.insertMany l ⋯) = true},
  (↑(t.insertMany l ⋯)).getKey k h' = t.getKey k ⋯
-- Std.Do.SPred.DerivedLaws
/-- A proof that `φ` and `P` are logically equivalent.  -/
Std.Do.SPred.Tactic.PropAsSPredTautology.iff : ∀ {φ : Prop} {σs : outParam (List (Type u))} {P : outParam (Std.Do.SPred σs)}
  [self : Std.Do.SPred.Tactic.PropAsSPredTautology φ P], φ ↔ ⊢ₛ P
-- Mathlib.Geometry.Manifold.MFDeriv.FDeriv
/-- **Alias** of the reverse direction of `mdifferentiable_iff_differentiable`.

---

For maps between vector spaces, `MDifferentiable` and `Differentiable` coincide  -/
Differentiable.mdifferentiable : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {f : E → E'},
  Differentiable 𝕜 f → MDiff f
-- Mathlib.Algebra.GCDMonoid.Basic
gcd_zero_left : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (a : α), gcd 0 a = normalize a
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Bicone.IsBilimit.mk.injEq : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} {B : CategoryTheory.Limits.Bicone F}
  (isLimit : CategoryTheory.Limits.IsLimit B.toCone) (isColimit : CategoryTheory.Limits.IsColimit B.toCocone)
  (isLimit_1 : CategoryTheory.Limits.IsLimit B.toCone) (isColimit_1 : CategoryTheory.Limits.IsColimit B.toCocone),
  ({ isLimit := isLimit, isColimit := isColimit } = { isLimit := isLimit_1, isColimit := isColimit_1 }) =
    (isLimit = isLimit_1 ∧ isColimit = isColimit_1)
-- Mathlib.Topology.Category.TopCat.Limits.Basic
/-- The unique map ∅ ⟶ X is inducing.  -/
TopCat.IsInducing.empty : ∀ (X : TopCat), Topology.IsInducing ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.isInitialPEmpty.to X))
-- Mathlib.Order.SupClosed
/-- A set `s` is *inf-closed* if `a ⊓ b ∈ s` for all `a ∈ s`, `b ∈ s`.  -/
InfClosed : {α : Type u_3} → [SemilatticeInf α] → Set α → Prop
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
CategoryTheory.IsHomLift.lift_comp_id : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsHomLift f φ],
  p.IsHomLift (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id S)) φ
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.degree.eq_1 : ∀ {V : Type u_1} (G : SimpleGraph V) (v : V) [inst : Fintype ↑(G.neighborSet v)], G.degree v = (G.neighborFinset v).card
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
IsPrimitiveRoot.finite_quotient_span_sub_one : ∀ {p k : ℕ} {K : Type u} [inst : Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [inst_1 : CharZero K]
  [hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))),
  Finite (NumberField.RingOfIntegers K ⧸ Ideal.span {hζ.toInteger - 1})
-- Lean.Elab.Tactic.Grind.Config
_private.Lean.Elab.Tactic.Grind.Config.0.Lean.Elab.Tactic.instEvalExprGrobnerConfig.evalExpr : Lean.Expr → Lean.MetaM Lean.Grind.GrobnerConfig
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.XXIsoOfEq_hom_ιTotal : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂] [inst_4 : K.HasTotal c₁₂]
  {x₁ y₁ : I₁} (h₁ : x₁ = y₁) {x₂ y₂ : I₂} (h₂ : x₂ = y₂) (i₁₂ : I₁₂) (h : c₁.π c₂ c₁₂ (y₁, y₂) = i₁₂),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.XXIsoOfEq C c₁ c₂ K h₁ h₂).hom (K.ιTotal c₁₂ y₁ y₂ i₁₂ h) =
    K.ιTotal c₁₂ x₁ x₂ i₁₂ ⋯
-- Mathlib.Analysis.Normed.Group.Uniform
NormedAddGroup.to_isIsometricVAdd_right : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E], IsIsometricVAdd Eᵃᵒᵖ E
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKeyD_congr : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k k' fallback : α}, cmp k k' = Ordering.eq → t.getKeyD k fallback = t.getKeyD k' fallback
-- Lean.Meta.Tactic.Grind.Split
Lean.Meta.Grind.instBEqSplitStatus : BEq Lean.Meta.Grind.SplitStatus
-- Mathlib.Topology.Category.TopPair
TopPair.incl_obj : ∀ (X : TopCat), TopPair.incl.obj X = TopPair.ofTopCat X
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.atBot_neBot : ∀ {α : Type u_3} [inst : Preorder α] [IsCodirectedOrder α] [Nonempty α], Filter.atBot.NeBot
-- Mathlib.Logic.Relation
Relation.EqvGen.symm : ∀ {α : Type u_1} {r : α → α → Prop} (x y : α), Relation.EqvGen r x y → Relation.EqvGen r y x
-- Init.Data.Array.Lemmas
Array.size_empty : ∀ {α : Type u_1}, #[].size = 0
-- Mathlib.Geometry.Manifold.ContMDiffMFDeriv
inTangentCoordinates.congr_simp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_4}
  [inst_5 : TopologicalSpace H] (I I_1 : ModelWithCorners 𝕜 E H) (e_I : I = I_1) {H' : Type u_5}
  [inst_6 : TopologicalSpace H'] (I' I'_1 : ModelWithCorners 𝕜 E' H') (e_I' : I' = I'_1) {M : Type u_6}
  [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M] {M' : Type u_7} [inst_9 : TopologicalSpace M']
  [inst_10 : ChartedSpace H' M'] [inst_11 : IsManifold I 1 M] [inst_12 : IsManifold I' 1 M'] {N : Type u_9}
  (f f_1 : N → M),
  f = f_1 →
    ∀ (g g_1 : N → M'),
      g = g_1 →
        ∀ (ϕ ϕ_1 : N → E →L[𝕜] E'),
          ϕ = ϕ_1 →
            ∀ (a a_1 : N),
              a = a_1 →
                ∀ (a_2 a_3 : N),
                  a_2 = a_3 → inTangentCoordinates I I' f g ϕ a a_2 = inTangentCoordinates I_1 I'_1 f_1 g_1 ϕ_1 a_1 a_3
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- The diagram of the multifork attached to a presheaf
`F : Cᵒᵖ ⥤ A`, `S : C` and `E : PreOneHypercover S`.  -/
CategoryTheory.PreOneHypercover.multicospanIndex : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} A] →
        {S : C} →
          (E : CategoryTheory.PreOneHypercover S) →
            CategoryTheory.Functor Cᵒᵖ A → CategoryTheory.Limits.MulticospanIndex E.multicospanShape A
-- Mathlib.MeasureTheory.Measure.DiracProba
/-- The Dirac delta mass at a point `x : X` as a `ProbabilityMeasure`.  -/
MeasureTheory.diracProba : {X : Type u_1} → [inst : MeasurableSpace X] → X → MeasureTheory.ProbabilityMeasure X
-- Mathlib.RingTheory.LocalProperties.ProjectiveDimension
ModuleCat.projectiveDimension_eq_iSup_localizedModule_maximal : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Small.{v, u} R] [IsNoetherianRing R] (M : ModuleCat R)
  [Module.Finite R ↑M],
  CategoryTheory.projectiveDimension M =
    ⨆ p, CategoryTheory.projectiveDimension (M.localizedModule p.asIdeal.primeCompl)
-- Lean.Meta.Tactic.Grind.AC.Seq
Lean.Grind.AC.Seq.noAdjacentDuplicates : Lean.Grind.AC.Seq → Bool
-- Std.Data.ExtTreeMap.Basic
/-- Given a proof that such a mapping exists, retrieves the key-value pair with the largest key that is
less than or equal to the given key.
 -/
Std.ExtTreeMap.getEntryLE : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      [inst : Std.TransCmp cmp] → (t : Std.ExtTreeMap α β cmp) → (k : α) → (∃ a ∈ t, (cmp a k).isLE = true) → α × β
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKey?_eq_back?_keysArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.maxKey? = t.keysArray.back?
-- Aesop.RuleSet
Aesop.LocalRuleSet.applicableUnsafeRules : Aesop.LocalRuleSet →
  Aesop.ForwardRuleMatches → Lean.MVarId → Aesop.BaseM (Array (Aesop.IndexMatchResult Aesop.UnsafeRule))
-- Mathlib.Topology.LocallyClosed
/-- The coborder of any set is dense  -/
dense_coborder : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, Dense (coborder s)
-- Mathlib.Combinatorics.Matroid.Map
Matroid.Indep.mapEmbedding : ∀ {α : Type u_1} {β : Type u_2} {I : Set α} {M : Matroid α},
  M.Indep I → ∀ (f : α ↪ β), (M.mapEmbedding f).Indep (⇑f '' I)
-- Lean.Data.Lsp.Extra
Lean.Lsp.RpcConnected.mk.injEq : ∀ (sessionId sessionId_1 : UInt64),
  ({ sessionId := sessionId } = { sessionId := sessionId_1 }) = (sessionId = sessionId_1)
-- Aesop.ElabM
Aesop.shouldParsePriorities : Aesop.ElabM Bool
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_fiberwise_eq_prod_filter' : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : CommMonoid M] [inst_1 : DecidableEq κ] (s : Finset ι)
  (t : Finset κ) (g : ι → κ) (f : κ → M), ∏ j ∈ t, ∏ i ∈ s with g i = j, f j = ∏ i ∈ s with g i ∈ t, f (g i)
-- Mathlib.NumberTheory.Bernoulli
/-- The exponential generating function for the Bernoulli numbers `bernoulli' n`.  -/
bernoulli'PowerSeries : (A : Type u_1) → [inst : CommRing A] → [Algebra ℚ A] → PowerSeries A
-- Mathlib.Data.Int.Cast.Defs
AddCommGroupWithOne.mk : {R : Type u} →
  [toAddCommGroup : AddCommGroup R] →
    [toIntCast : IntCast R] →
      [toNatCast : NatCast R] →
        [toOne : One R] →
          autoParam (↑0 = 0) AddMonoidWithOne.natCast_zero._autoParam →
            autoParam (∀ (n : ℕ), ↑(n + 1) = ↑n + 1) AddMonoidWithOne.natCast_succ._autoParam →
              autoParam (∀ (n : ℕ), IntCast.intCast ↑n = ↑n) AddGroupWithOne.intCast_ofNat._autoParam →
                autoParam (∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1))
                    AddGroupWithOne.intCast_negSucc._autoParam →
                  AddCommGroupWithOne R
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.apply_le_nfp : ∀ {f : Ordinal.{u} → Ordinal.{u}}, Order.IsNormal f → ∀ {a b : Ordinal.{u}}, f b ≤ Ordinal.nfp f a ↔ b ≤ Ordinal.nfp f a
-- Mathlib.Algebra.Order.GroupWithZero.Defs
MulPosReflectLT.to_contravariantClass_pos_mul_lt : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [MulPosReflectLT α],
  ContravariantClass { x // 0 < x } α (fun x y => y * ↑x) fun x1 x2 => x1 < x2
-- Mathlib.CategoryTheory.Localization.Equivalence
/-- If `L₁ : C₁ ⥤ D₁` is a localization functor for `W₁ : MorphismProperty C₁`, then if we
transport this functor `L₁` via equivalences `C₁ ≌ C₂` and `D₁ ≌ D₂` to get a functor
`L₂ : C₂ ⥤ D₂`, then `L₂` is also a localization functor for
a suitable `W₂ : MorphismProperty C₂`.  -/
CategoryTheory.Functor.IsLocalization.of_equivalences : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D₂] (L₁ : CategoryTheory.Functor C₁ D₁)
  (W₁ : CategoryTheory.MorphismProperty C₁) [L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂)
  (W₂ : CategoryTheory.MorphismProperty C₂) (E : C₁ ≌ C₂) (E' : D₁ ≌ D₂)
  [CategoryTheory.CatCommSq E.functor L₁ L₂ E'.functor],
  W₁ ≤ W₂.isoClosure.inverseImage E.functor → W₂.IsInvertedBy L₂ → L₂.IsLocalization W₂
-- Mathlib.Combinatorics.SimpleGraph.LapMatrix
Matrix.IsAdjMatrix.isHermitian : ∀ {α : Type u_1} {V : Type u_2} [inst : NonAssocSemiring α] [inst_1 : StarRing α] {A : Matrix V V α},
  A.IsAdjMatrix → A.IsHermitian
-- Mathlib.Data.Real.ConjExponents
NNReal.HolderTriple.of_pos : ∀ {p q : NNReal}, 0 < p → 0 < q → p.HolderTriple q (p⁻¹ + q⁻¹)⁻¹
-- Mathlib.Algebra.Order.Ring.WithTop
WithBot.instPosMulReflectLE : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] [inst_2 : Preorder α] [PosMulReflectLE α],
  PosMulReflectLE (WithBot α)
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.filterWithPostcondition.eq_1 : ∀ {α β : Type w} [inst : Std.Iterator α Id β] {m : Type w → Type w'} [inst_1 : Monad m]
  (f : β → Std.Iterators.PostconditionT m (ULift.{w, 0} Bool)) (it : Std.Iter β),
  Std.Iter.filterWithPostcondition f it = Std.IterM.filterWithPostcondition f it.toIterM
-- Lean.Meta.Basic
/-- Given `e` of the form `forall ..xs, A`, this combinator will create a new
metavariable for each `x` in `xs` and instantiate `A` with these.
Returns a product containing
- the new metavariables
- the binder info for the `xs`
- the instantiated `A`
 -/
Lean.Meta.forallMetaTelescope : Lean.Expr →
  optParam Lean.MetavarKind Lean.MetavarKind.natural → Lean.MetaM (Array Lean.Expr × Array Lean.BinderInfo × Lean.Expr)