mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Localization.Module
Module.Basis.ofIsLocalizedModule.congr_simp : ∀ {R : Type u_1} (Rₛ : Type u_2) [inst : CommSemiring R] (S S_1 : Submonoid R) (e_S : S = S_1)
  [inst_1 : CommSemiring Rₛ] [inst_2 : Algebra R Rₛ] [inst_3 : IsLocalization S Rₛ] {M : Type u_3} {Mₛ : Type u_4}
  [inst_4 : AddCommMonoid M] [inst_5 : Module R M] [inst_6 : AddCommMonoid Mₛ] [inst_7 : Module R Mₛ]
  [inst_8 : Module Rₛ Mₛ] [inst_9 : IsScalarTower R Rₛ Mₛ] (f f_1 : M →ₗ[R] Mₛ) (e_f : f = f_1)
  [inst_10 : IsLocalizedModule S f] {ι : Type u_5} (b b_1 : Module.Basis ι R M),
  b = b_1 → Module.Basis.ofIsLocalizedModule Rₛ S f b = Module.Basis.ofIsLocalizedModule Rₛ S_1 f_1 b_1
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Carry
Std.Tactic.BVDecide.BVExpr.bitblast.OverflowInput.w : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] → {aig : Std.Sat.AIG α} → Std.Tactic.BVDecide.BVExpr.bitblast.OverflowInput aig → ℕ
-- Aesop.Builder.Tactic
Aesop.matchByTactic? : Lean.Term → Option (Lean.TSyntax `Lean.Parser.Tactic.tacticSeq)
-- Mathlib.Data.Nat.Factorial.NatCast
Nat.castChoose_eq : ∀ {A : Type u_1} [inst : CommSemiring A] {m : ℕ} {k : ℕ × ℕ},
  IsUnit ↑m.factorial →
    k ∈ Finset.HasAntidiagonal.antidiagonal m →
      ↑(m.choose k.1) = ↑m.factorial * Ring.inverse ↑k.1.factorial * Ring.inverse ↑k.2.factorial
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degreeOf_def : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : DecidableEq σ] (n : σ) (p : MvPolynomial σ R),
  MvPolynomial.degreeOf n p = Multiset.count n p.degrees
-- Mathlib.SetTheory.Ordinal.Notation
ONote.nf_opowAux : ∀ (e a0 a : ONote) [e.NF] [a0.NF] [a.NF] (k m : ℕ), (e.opowAux a0 a k m).NF
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.isUnit_iff_norm_isUnit : ∀ {R : Type u_2} {a b : R} [inst : CommRing R] {x : QuadraticAlgebra R a b}, IsUnit x ↔ IsUnit (QuadraticAlgebra.norm x)
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
CategoryTheory.Limits.initial.hom_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasInitial C] {P : C}
  (f g : ⊥_ C ⟶ P), f = g
-- Lean.Meta.Sym.Offset
/-- Represents a natural number expression as a base plus a constant offset.
- `.num k` represents the literal `k`
- `.add e k` represents `e + k`

Used for pattern matching and unification.
 -/
Lean.Meta.Sym.Offset : Type
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- Uses `right` co(ntra)variant.  -/
Right.neg_pos_iff : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddRightStrictMono α] {a : α}, 0 < -a ↔ a < 0
-- Mathlib.Algebra.Exact.Basic
Function.Exact.linearEquivOfSurjective.congr_simp : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {P : Type u_6} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R P]
  {f : M →ₗ[R] N} {g g_1 : N →ₗ[R] P} (e_g : g = g_1) (h : Function.Exact ⇑f ⇑g) (hg : Function.Surjective ⇑g),
  h.linearEquivOfSurjective hg = ⋯.linearEquivOfSurjective ⋯
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv.0.Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go.eq_def : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (curr : ℕ) (n d : aig.RefVec w)
  (wn wr : ℕ) (q r : aig.RefVec w),
  Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go aig curr n d wn wr q r =
    match curr with
    | 0 => { aig := aig, q := q, r := r, hle := ⋯ }
    | curr.succ =>
      let res := Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig n d wn wr q r;
      let aig_1 := res.aig;
      let wn_1 := res.wn;
      let wr_1 := res.wr;
      let q_1 := res.q;
      let r_1 := res.r;
      have this := ⋯;
      let n_1 := n.cast this;
      let d_1 := d.cast this;
      let res := Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go aig_1 curr n_1 d_1 wn_1 wr_1 q_1 r_1;
      let aig_2 := res.aig;
      have q_2 := res.q;
      have r_2 := res.r;
      have this := ⋯;
      { aig := aig_2, q := q_2, r := r_2, hle := this }
-- Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM
ContinuousLinearEquiv.compactConvergenceCLMCongr_symm_apply : ∀ {𝕜 : Type u_7} {E : Type u_8} {F : Type u_9} {G : Type u_10} {H : Type u_11} [inst : AddCommGroup E]
  [inst_1 : AddCommGroup F] [inst_2 : AddCommGroup G] [inst_3 : AddCommGroup H] [inst_4 : NormedField 𝕜]
  [inst_5 : Module 𝕜 E] [inst_6 : Module 𝕜 F] [inst_7 : Module 𝕜 G] [inst_8 : Module 𝕜 H] [inst_9 : TopologicalSpace E]
  [inst_10 : TopologicalSpace F] [inst_11 : TopologicalSpace G] [inst_12 : TopologicalSpace H]
  [inst_13 : IsTopologicalAddGroup G] [inst_14 : IsTopologicalAddGroup H] [inst_15 : ContinuousConstSMul 𝕜 G]
  [inst_16 : ContinuousConstSMul 𝕜 H] (e₁ : E ≃L[𝕜] F) (e₂ : H ≃L[𝕜] G) (φ : CompactConvergenceCLM (RingHom.id 𝕜) F G)
  (e : E), ((e₁.compactConvergenceCLMCongr e₂).symm φ) e = e₂.symm (φ (e₁ e))
-- Mathlib.Algebra.Order.GroupWithZero.Basic
StrictMono.mul_monotone : ∀ {α : Type u_1} {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : PartialOrder M₀] [inst_2 : Preorder α]
  {f g : α → M₀} [PosMulMono M₀] [MulPosStrictMono M₀],
  StrictMono f → Monotone g → (∀ (x : α), 0 ≤ f x) → (∀ (x : α), 0 < g x) → StrictMono (f * g)
-- Init.Data.Vector.Find
Vector.exists_of_findSome?_eq_some : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {b : β} {f : α → Option β} {xs : Vector α n},
  Vector.findSome? f xs = some b → ∃ a ∈ xs, f a = some b
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.destruct_map : ∀ {α : Type u} {β : Type v} (f : α → β) (s : Stream'.WSeq α),
  (Stream'.WSeq.map f s).destruct = Computation.map (Option.map (Prod.map f (Stream'.WSeq.map f))) s.destruct
-- Mathlib.GroupTheory.Congruence.Basic
AddCon.quotientKerEquivRange.eq_1 : ∀ {M : Type u_1} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass P] (f : M →+ P),
  AddCon.quotientKerEquivRange f =
    {
      toEquiv :=
        Equiv.ofBijective ⇑((AddEquiv.addSubmonoidCongr ⋯).toAddMonoidHom.comp (AddCon.kerLift f).mrangeRestrict) ⋯,
      map_add' := ⋯ }
-- Mathlib.CategoryTheory.Adjunction.Triple
CategoryTheory.Adjunction.Triple.leftToRight_app_map_adj₁_unit_app : ∀ {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] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  {H : CategoryTheory.Functor C D} (t : CategoryTheory.Adjunction.Triple F G H) [inst_2 : F.Full] [inst_3 : F.Faithful]
  (X : C),
  CategoryTheory.CategoryStruct.comp (t.leftToRight.app X) (H.map (t.adj₁.unit.app X)) = t.adj₂.unit.app (F.obj X)
-- Mathlib.Topology.Order.Monotone
sSup_mem_closure : ∀ {α : Type u_1} [inst : CompleteLinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α] {s : Set α},
  s.Nonempty → sSup s ∈ closure s
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.mkOfDiscrete_apply : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : DiscreteTopology α]
  (f : α → β) (C : ℝ) (h : ∀ (x y : α), dist (f x) (f y) ≤ C) (a : α),
  (BoundedContinuousFunction.mkOfDiscrete f C h) a = f a
-- Mathlib.CategoryTheory.ObjectProperty.Local
CategoryTheory.MorphismProperty.isColocal_iSup : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Sort u_1} (W : ι → CategoryTheory.MorphismProperty C),
  (⨆ i, W i).isColocal = ⨅ i, (W i).isColocal
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
DiscreteConvolution.addFiber.eq_1 : ∀ {M : Type u_1} [inst : AddMonoid M] (x : M), DiscreteConvolution.addFiber x = Set.univ.antidiagonal Set.univ x
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for rotate right on `BitVec`.  -/
BitVec.reduceRotateRight : Lean.Meta.Simp.DSimproc
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Goal.getGeneration : Lean.Meta.Grind.Goal → Lean.Expr → ℕ
-- Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
lift_rank_lt_rank_dual' : ∀ {K : Type u} [inst : DivisionRing K] {V : Type v} [inst_1 : AddCommGroup V] [inst_2 : Module K V],
  Cardinal.aleph0 ≤ Module.rank K V → Cardinal.lift.{u, v} (Module.rank K V) < Module.rank Kᵐᵒᵖ (V →ₗ[K] K)
-- Mathlib.ModelTheory.Order
/-- A structure is ordered if its language has a `≤` symbol whose interpretation is `≤`.  -/
FirstOrder.Language.OrderedStructure : (L : FirstOrder.Language) → (M : Type w') → [L.IsOrdered] → [LE M] → [L.Structure M] → Prop
-- Mathlib.Topology.MetricSpace.Holder
HolderOnWith.ediam_image_le : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {C r : NNReal} {f : X → Y}
  {s : Set X}, HolderOnWith C r f s → Metric.ediam (f '' s) ≤ ↑C * Metric.ediam s ^ ↑r
-- Init.Data.List.Sublist
List.sublist_flatten_of_mem : ∀ {α : Type u_1} {L : List (List α)} {l : List α}, l ∈ L → l.Sublist L.flatten
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.LeftHomologyData.map_H : ∀ {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] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : h.IsPreservedBy F],
  (h.map F).H = F.obj h.H
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_disjSum : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : CommMonoid M] (s : Finset ι) (t : Finset κ) (f : ι ⊕ κ → M),
  ∏ x ∈ s.disjSum t, f x = (∏ x ∈ s, f (Sum.inl x)) * ∏ x ∈ t, f (Sum.inr x)
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.join_mono_right : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P Q Q' : l},
  Lean.Order.PartialOrder.rel Q Q' → Lean.Order.PartialOrder.rel (Lean.Order.join P Q) (Lean.Order.join P Q')
-- Init.Grind.Interactive
/-- The `sorry` tactic is a temporary placeholder for an incomplete tactic proof.  -/
Lean.Parser.Tactic.Grind.sorry : Lean.ParserDescr
-- Mathlib.Analysis.InnerProductSpace.Basic
re_inner_self_nonpos : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {x : E}, RCLike.re (inner 𝕜 x x) ≤ 0 ↔ x = 0
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.Nondegenerate.toMatrix₂' : ∀ {R : Type u_1} {n : Type u_11} {m : Type u_12} [inst : CommRing R] [inst_1 : DecidableEq m] [inst_2 : Fintype m]
  [inst_3 : DecidableEq n] [inst_4 : Fintype n] {B : (m → R) →ₗ[R] (n → R) →ₗ[R] R},
  B.Nondegenerate → ((LinearMap.toMatrix₂' R) B).Nondegenerate
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.Raw₀.interSmallerFn.match_1.splitter : {α : Type u_2} →
  {β : α → Type u_1} →
    (motive : Option ((a : α) × β a) → Sort u_3) →
      (x : Option ((a : α) × β a)) → ((kv' : (a : α) × β a) → motive (some kv')) → (Unit → motive none) → motive x
-- Mathlib.Algebra.Ring.CentroidHom
/-- `CentroidHomClass F α` states that `F` is a type of centroid homomorphisms.

You should extend this class when you extend `CentroidHom`.  -/
CentroidHomClass : (F : Type u_6) → (α : outParam (Type u_7)) → [NonUnitalNonAssocSemiring α] → [FunLike F α α] → Prop
-- Mathlib.Analysis.Normed.Group.Basic
abs_norm_sub_norm_le_norm_neg_add : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (a b : E), |‖a‖ - ‖b‖| ≤ ‖-a + b‖
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.pOpcyclesIso_hom_inv_id_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) (hi : c.prev j = i) (h : K.d i j = 0)
  [inst_2 : K.HasHomology j] {Z : C} (h_1 : K.X j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.pOpcycles j)
      (CategoryTheory.CategoryStruct.comp (K.pOpcyclesIso i j hi h).inv h_1) =
    h_1
-- Mathlib.Data.Setoid.Basic
/-- The image of `f` lifted to the quotient by its kernel is equal to the image of `f` itself.  -/
Setoid.range_kerLift_eq_range : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), Set.range (Setoid.kerLift f) = Set.range f
-- Init.Data.Array.Erase
_private.Init.Data.Array.Erase.0.List.eraseP_filterMap.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (y : β) (h_1 : (y : β) → motive (some y)) (h_2 : Unit → motive none),
  (match some y with
    | some y => h_1 y
    | none => h_2 ()) =
    h_1 y
-- Mathlib.Order.Filter.Map
Set.LeftInvOn.filter_map_Iic : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {g : β → α},
  Set.LeftInvOn g f s → Set.LeftInvOn (Filter.map g) (Filter.map f) (Set.Iic (Filter.principal s))
-- Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
MeasureTheory.isSetRing_measurableCylinders : ∀ {ι : Type u_1} {α : ι → Type u_2} {mα : (i : ι) → MeasurableSpace (α i)},
  MeasureTheory.IsSetRing (MeasureTheory.measurableCylinders α)
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
abs_eq_zero : ∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : LinearOrder α] [AddLeftMono α] {a : α} [AddRightMono α], |a| = 0 ↔ a = 0
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.pow_eq_one_iff : ∀ {a : Ordinal.{u_1}} {n : ℕ}, a ^ n = 1 ↔ a = 1 ∨ n = 0
-- Mathlib.NumberTheory.LegendreSymbol.Basic
/-- The square of the symbol is 1 if `p ∤ a`.  -/
legendreSym.sq_one : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] {a : ℤ}, ↑a ≠ 0 → legendreSym p a ^ 2 = 1
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.contains_eq_isSome_get? : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α}, t.contains a = (Std.DTreeMap.Raw.Const.get? t a).isSome
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.Measure.setLIntegral_rnDeriv' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [μ.HaveLebesgueDecomposition ν],
  μ.AbsolutelyContinuous ν → ∀ {s : Set α}, MeasurableSet s → ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν = μ s
-- Init.Data.String.Substring
/-- Checks whether a substring contains the specified character.
 -/
Substring.Raw.contains : Substring.Raw → Char → Bool
-- Mathlib.Order.RelIso.Basic
RelIso.ext : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} ⦃f g : r ≃r s⦄, (∀ (x : α), f x = g x) → f = g
-- Init.Grind.Module.Basic
Lean.Grind.NatModule.mk : {M : Type u} →
  [toAddCommMonoid : Lean.Grind.AddCommMonoid M] →
    [nsmul : SMul ℕ M] → (∀ (a : M), 0 • a = 0) → (∀ (n : ℕ) (a : M), (n + 1) • a = n • a + a) → Lean.Grind.NatModule M
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.FamilyOfElements.singletonEquiv_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor Cᵒᵖ (Type w)) {X Y : C}
  (f : X ⟶ Y) (x : CategoryTheory.Presieve.FamilyOfElements P (CategoryTheory.Presieve.singleton f)),
  (CategoryTheory.Presieve.FamilyOfElements.singletonEquiv P f) x = x f ⋯
-- Mathlib.Tactic.Linter.TextBased
/-- How to format style errors  -/
Mathlib.Linter.TextBased.ErrorFormat : Type
-- Std.Async.Select
/-- The core data structure for racing on winning a `Selectable.one` if multiple event sources are ready
at the same time. A `Task` can try to finish the waiter by calling `Waiter.race`.
 -/
Std.Async.Waiter : Type → Type
-- Mathlib.CategoryTheory.Core
CategoryTheory.Equivalence.core_functor_obj_of : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : C ≌ D) (X : CategoryTheory.Core C), (E.core.functor.obj X).of = E.functor.obj X.of
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- **Alias** of `CategoryTheory.Limits.ι_coproductUniqueIso_hom`. -/
CategoryTheory.Limits.coproductUniqueIso_hom : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : Unique β] (f : β → C) (b : β),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f b)
      (CategoryTheory.Limits.coproductUniqueIso f).hom =
    CategoryTheory.eqToHom ⋯
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.Context.optionsPerPos : Lean.PrettyPrinter.Delaborator.Context → Lean.PrettyPrinter.Delaborator.OptionsPerPos
-- Mathlib.Order.CompleteLattice.Defs
iSup_eq_top : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLinearOrder α] {f : ι → α}, iSup f = ⊤ ↔ ∀ b < ⊤, ∃ i, b < f i
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
CategoryTheory.Lax.OplaxTrans.homCategory.ext : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} {η θ : F ⟶ G} {Γ Δ : η ⟶ θ}, (∀ (a : B), Γ.as.app a = Δ.as.app a) → Γ = Δ
-- Mathlib.Algebra.Order.Floor.Defs
FloorRing.toFloorSemiring : {α : Type u_2} → [inst : Ring α] → [inst_1 : LinearOrder α] → [FloorRing α] → FloorSemiring α
-- Mathlib.Data.DFinsupp.Defs
/-- Create an element of `Π₀ i, β i` from a finset `s` and a function `x`
defined on this `Finset`.  -/
DFinsupp.mk : {ι : Type u} →
  {β : ι → Type v} →
    [inst : (i : ι) → Zero (β i)] → [DecidableEq ι] → (s : Finset ι) → ((i : ↑↑s) → β ↑i) → Π₀ (i : ι), β i
-- Mathlib.Order.Hom.Basic
OrderIsoClass.mk : ∀ {F : Type u_6} {α : outParam (Type u_7)} {β : outParam (Type u_8)} [inst : LE α] [inst_1 : LE β]
  [inst_2 : EquivLike F α β], (∀ (f : F) {a b : α}, f a ≤ f b ↔ a ≤ b) → OrderIsoClass F α β
-- Mathlib.Data.Matrix.DMatrix
DMatrix.instSub : {m : Type u_1} → {n : Type u_2} → {α : m → n → Type v} → [(i : m) → (j : n) → Sub (α i j)] → Sub (DMatrix m n α)
-- Mathlib.CategoryTheory.IsConnected
CategoryTheory.Zigzag.of_inv : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {j₁ j₂ : J} (f : j₂ ⟶ j₁), CategoryTheory.Zigzag j₁ j₂
-- Std.Async.ContextAsync
/-- Returns a selector that completes when the current context is cancelled.
This is useful for selecting on cancellation alongside other asynchronous operations.
 -/
Std.Async.Selector.cancelled : Std.Async.ContextAsync (Std.Async.Selector Unit)
-- Mathlib.Algebra.Group.Subgroup.Pointwise
AddSubgroup.normalizer_le_normalizer_sup_of_normalizer_le_right : ∀ {G : Type u_2} [inst : AddGroup G] {H K : AddSubgroup G},
  AddSubgroup.normalizer ↑H ≤ AddSubgroup.normalizer ↑K → AddSubgroup.normalizer ↑H ≤ AddSubgroup.normalizer ↑(K ⊔ H)
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- A finite-dimensional inner product space admits an orthonormal basis.  -/
exists_orthonormalBasis : ∀ (𝕜 : Type u_3) [inst : RCLike 𝕜] (E : Type u_4) [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [FiniteDimensional 𝕜 E], ∃ w b, ⇑b = Subtype.val
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PrepathObject.map_p₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (P : HomotopicalAlgebra.PrepathObject X) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] (F : CategoryTheory.Functor C D), (P.map F).p₀ = F.map P.p₀
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Equivalence.leftOp_counitIso_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ Dᵒᵖ) (X : D), e.leftOp.counitIso.hom.app X = (e.counitIso.inv.app (Opposite.op X)).unop
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.stalkSpecializes_stalkMap : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (x x' : ↥X) (h : x ⤳ x'),
  CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes ⋯) (AlgebraicGeometry.Scheme.Hom.stalkMap f x) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.stalkMap f x') (X.presheaf.stalkSpecializes h)
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
AddEquiv.withTopCongr.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Add α] [inst_1 : Add β] (e : α ≃+ β),
  e.withTopCongr = { toEquiv := e.withTopCongr, map_add' := ⋯ }
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
CategoryTheory.ForgetEnrichment.equiv_unitIso : ∀ (V : Type u') [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] {D : Type u''}
  [inst_2 : CategoryTheory.Category.{v'', u''} D] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V D],
  (CategoryTheory.ForgetEnrichment.equiv V).unitIso =
    CategoryTheory.NatIso.ofComponents
      (fun X => CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.ForgetEnrichment V D)).obj X)) ⋯
-- Std.Net.Addr
Std.Net.IPv6Addr.mk : Vector UInt16 8 → Std.Net.IPv6Addr
-- Mathlib.Topology.DerivedSet
isClosed_derivedSet : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] (A : Set X), IsClosed (derivedSet A)
-- Mathlib.Algebra.Order.GroupWithZero.Defs
/-- Local notation for the nonnegative elements of a type `α`.  -/
_private.Mathlib.Algebra.Order.GroupWithZero.Defs.0.«termα≥0» : Lean.ParserDescr
-- Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Polynomial.isMonicOfDegree_iff' : ∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R) (n : ℕ), p.IsMonicOfDegree n ↔ p.natDegree = n ∧ p.Monic
-- Mathlib.Algebra.Group.Action.TypeTags
ofAdd_smul : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] (a : α) (b : β), Multiplicative.ofAdd a • b = a +ᵥ b
-- Mathlib.Algebra.GroupWithZero.Units.Basic
Ring.inverse_one : ∀ (M₀ : Type u_2) [inst : MonoidWithZero M₀], Ring.inverse 1 = 1
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.unone.eq_1 : ∀ {α : Type u} (x_2 : α) (x_3 : ↑x_2 ≠ 1), WithOne.unone x_3 = x_2
-- Init.Data.String.Lemmas.FindPos
_private.Init.Data.String.Lemmas.FindPos.0.String.posGT.eq_1 : ∀ (s : String) (offset : String.Pos.Raw) (h : offset < s.rawEndPos),
  s.posGT offset h = String.Pos.ofToSlice (s.toSlice.posGT offset ⋯)
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.instFstScheme : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f],
  AlgebraicGeometry.IsOpenImmersion (CategoryTheory.Limits.pullback.fst g f)
-- Mathlib.Order.Monotone.Basic
/-- A bounded monotone function `ℕ → ℕ` converges.  -/
converges_of_monotone_of_bounded : ∀ {f : ℕ → ℕ}, Monotone f → ∀ {c : ℕ}, (∀ (n : ℕ), f n ≤ c) → ∃ b N, ∀ n ≥ N, f n = b
-- Lean.Meta.Tactic.Grind.AC.Util
Lean.Meta.Grind.AC.instMonadGetStructACM : Lean.Meta.Grind.AC.MonadGetStruct Lean.Meta.Grind.AC.ACM
-- Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
/-- Integration by parts of Schwartz functions for the 1-dimensional derivative.

Version for a Schwartz function with values in continuous linear maps.  -/
SchwartzMap.integral_clm_comp_deriv_right_eq_neg_left : ∀ {𝕜 : Type u_2} {V : Type u_7} {F : Type u_8} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F]
  [inst_2 : NormedAddCommGroup V] [inst_3 : NormedSpace ℝ V] [inst_4 : RCLike 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : NormedSpace 𝕜 V] (f : SchwartzMap ℝ (F →L[𝕜] V)) (g : SchwartzMap ℝ F),
  ∫ (x : ℝ), (f x) (deriv (⇑g) x) = -∫ (x : ℝ), (deriv (⇑f) x) (g x)
-- Mathlib.Order.Bounds.Basic
/-- If the range of a function `g` is bounded below, then `g ∘ f` is bounded below for all
functions `f`.  -/
BddBelow.range_comp_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] (f : γ → β) {g : β → α},
  BddBelow (Set.range g) → BddBelow (Set.range (g ∘ f))
-- Mathlib.Algebra.Category.Grp.EpiMono
_private.Mathlib.Algebra.Category.Grp.EpiMono.0.GrpCat.SurjectiveOfEpiAuxs.termX' : Lean.ParserDescr
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.balanceRErase_eq_balance : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β} {hlb : l.Balanced}
  {hrb : r.Balanced} {hlr : Std.DTreeMap.Internal.Impl.BalanceLErasePrecond r.size l.size},
  Std.DTreeMap.Internal.Impl.balanceRErase k v l r hlb hrb hlr = Std.DTreeMap.Internal.Impl.balance k v l r hlb hrb ⋯
-- Mathlib.Algebra.Order.GroupWithZero.Action.Synonym
OrderDual.instMulActionWithZero : {G₀ : Type u_1} →
  {M₀ : Type u_2} →
    [inst : MonoidWithZero G₀] → [inst_1 : AddMonoid M₀] → [MulActionWithZero G₀ M₀] → MulActionWithZero G₀ᵒᵈ M₀