mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Products
CategoryTheory.Limits.ι_comp_sigmaObjIso_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} D]
  {α : Type w} [inst_2 : CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete α) C]
  (f : α → CategoryTheory.Functor D C) (d : D) (s : α) {Z : C} (h : (∐ fun s => (f s).obj d) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.Sigma.ι f s).app d)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.sigmaObjIso f d).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun s => (f s).obj d) s) h
-- Init.Prelude
Fin.decLe : {n : ℕ} → (a b : Fin n) → Decidable (a ≤ b)
-- Mathlib.Geometry.Diffeology.Basic
/-- Technical condition saying that the topology on a type agrees with the D-topology.
Necessary because the D-topologies on for example products and subspaces don't agree with
the product and subspace topologies.  -/
Diffeology.IsDTopologyCompatible : (X : Type u_1) → [t : TopologicalSpace X] → [DiffeologicalSpace X] → Prop
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.contSupp.match_1.eq_2 : ∀ (motive : Turing.PartrecToTM2.Cont' → Sort u_1) (k : Turing.PartrecToTM2.Cont')
  (h_1 : (fs : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Cont'.cons₁ fs k))
  (h_2 : (k : Turing.PartrecToTM2.Cont') → motive k.cons₂)
  (h_3 : (f : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Cont'.comp f k))
  (h_4 : (f : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Cont'.fix f k))
  (h_5 : Unit → motive Turing.PartrecToTM2.Cont'.halt),
  (match k.cons₂ with
    | Turing.PartrecToTM2.Cont'.cons₁ fs k => h_1 fs k
    | k.cons₂ => h_2 k
    | Turing.PartrecToTM2.Cont'.comp f k => h_3 f k
    | Turing.PartrecToTM2.Cont'.fix f k => h_4 f k
    | Turing.PartrecToTM2.Cont'.halt => h_5 ()) =
    h_2 k
-- Batteries.Data.BitVec.Lemmas
BitVec.ofFnLEAux.eq_1 : ∀ {n : ℕ} (m : ℕ) (f : Fin n → Bool), BitVec.ofFnLEAux m f = Fin.foldr n (fun i v => v.shiftConcat (f i)) 0
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.subset_toFinset : ∀ {α : Type u} {t : Set α} {ht : t.Finite} {s : Finset α}, s ⊆ ht.toFinset ↔ ↑s ⊆ t
-- Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative
/-- The **Fredholm alternative** for compact operators: if `T` is a compact operator and `μ ≠ 0`,
then either `μ` is an eigenvalue of `T`, or `μ` is in the resolvent set of `T`.
See also `hasEigenvalue_iff_mem_spectrum`, which says that the nonzero eigenvalues of a compact
operator are exactly the nonzero points in the spectrum of the operator.
 -/
IsCompactOperator.hasEigenvalue_or_mem_resolventSet : ∀ {𝕜 : Type u_1} {X : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] {T : X →L[𝕜] X} {μ : 𝕜} [CompleteSpace X],
  IsCompactOperator ⇑T → μ ≠ 0 → Module.End.HasEigenvalue (↑T) μ ∨ μ ∈ resolventSet 𝕜 T
-- Mathlib.Data.ZMod.QuotientGroup
Int.index_zmultiples : ∀ (a : ℤ), (AddSubgroup.zmultiples a).index = a.natAbs
-- Lean.Parser.Extension
/-- Sets the option named by `nameStx` to the value parsed from `valStx` in the parser context.  -/
_private.Lean.Parser.Extension.0.Lean.Parser.withSetOptionValueFnCore : Lean.Syntax → Lean.Syntax → Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Mathlib.LinearAlgebra.Matrix.Defs
/-- The matrix constructed from the row-major array of `A`'s entries is `A`.  -/
Matrix.ofArray_ofFn : ∀ {R : Type u_7} {m n : ℕ} (A : Matrix (Fin m) (Fin n) R),
  Matrix.ofArray (Array.ofFn fun k => A k.divNat k.modNat) ⋯ = A
-- Lean.LocalContext
/-- Returns the value of the `ldecl` if it has a visible value.

If `allowNondep` is true, then allows nondependent `ldecl`s, whose values are normally hidden.
 -/
Lean.LocalDecl.value : Lean.LocalDecl → optParam Bool false → Lean.Expr
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.measure_ball_ne_top : ∀ {α : Type u_1} {m0 : MeasurableSpace α} [inst : PseudoMetricSpace α] [ProperSpace α] {μ : MeasureTheory.Measure α}
  [MeasureTheory.IsFiniteMeasureOnCompacts μ] {x : α} {r : ℝ}, μ (Metric.ball x r) ≠ ⊤
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getD_toList_roc_eq_fallback : ∀ {m n fallback : ℤ} {i : ℕ}, (n - m).toNat ≤ i → (m<...=n).toList.getD i fallback = fallback
-- Mathlib.RingTheory.PrincipalIdealDomain
Submodule.IsPrincipal.dvd_generator_span_iff : ∀ {R : Type u} [inst : CommSemiring R] {r : R} {s : Set R} [inst_1 : Submodule.IsPrincipal (Ideal.span s)],
  r ∣ Submodule.IsPrincipal.generator (Ideal.span s) ↔ ∀ x ∈ s, r ∣ x
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.card_sum : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language},
  (L.sum L').card = Cardinal.lift.{max u' v', max u v} L.card + Cardinal.lift.{max u v, max u' v'} L'.card
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.toAffineEquiv_injective : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂], Function.Injective AffineIsometryEquiv.toAffineEquiv
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.drop_drop : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (n m : ℕ), (p.drop n).drop m = (p.drop (n + m)).copy ⋯ ⋯
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RooSlice : (α : Type u_1) → Type u_2 → [Ord α] → Type (max u_2 u_1)
-- Mathlib.GroupTheory.Congruence.Basic
/-- Coercion from a congruence relation `c` on an `AddMonoid` `M`
to the `AddSubmonoid` of `M × M` whose elements are `(x, y)` such that `x`
is related to `y` by `c`.  -/
AddCon.toAddSubmonoid : {M : Type u_1} → [inst : AddZeroClass M] → Coe (AddCon M) (AddSubmonoid (M × M))
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.size_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  (t.insert k).size = if t.contains k = true then t.size else t.size + 1
-- Mathlib.Order.TypeTags
WithTop.inhabited : {α : Type u_1} → Inhabited (WithTop α)
-- Mathlib.AlgebraicTopology.SimplicialSet.Homotopy
SSet.Homotopy.h₁_assoc : ∀ {X Y : SSet} {f g : X ⟶ Y} (H : SSet.Homotopy f g) {Z : SSet} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp SSet.ι₁ (CategoryTheory.CategoryStruct.comp H.h h) =
    CategoryTheory.CategoryStruct.comp g h
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
SSet.Edge.ext_iff : ∀ {X : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 0 })} {e e' : SSet.Edge x₀ x₁}, e = e' ↔ e.edge = e'.edge
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the reverse direction of `le_inv_mul_iff_mul_le`. -/
le_inv_mul_of_mul_le : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [MulLeftMono α] {a b c : α}, a * b ≤ c → b ≤ a⁻¹ * c
-- Mathlib.Combinatorics.Quiver.ConnectedComponent
/-- The type of weakly connected components of a directed graph. Two vertices are
in the same weakly connected component if there is a zigzag of arrows from one
to the other.  -/
Quiver.WeaklyConnectedComponent : (V : Type u_1) → [Quiver V] → Type u_1
-- Mathlib.Algebra.Lie.Submodule
LieModuleHom.ker_toSubmodule : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : LieRingModule L M] [inst_5 : AddCommGroup N]
  [inst_6 : Module R N] [inst_7 : LieRingModule L N] (f : M →ₗ⁅R,L⁆ N), ↑f.ker = (↑f).ker
-- Mathlib.Order.Filter.Ker
Filter.ker_comap : ∀ {α : Type u_2} {β : Type u_3} (m : α → β) (f : Filter β), (Filter.comap m f).ker = m ⁻¹' f.ker
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.instIsIsoAppLanUnit_1 : ∀ {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] (L : CategoryTheory.Functor C D) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H] [L.Full] [L.Faithful] (F : CategoryTheory.Functor C H)
  [L.HasPointwiseLeftKanExtension F] [inst_6 : ∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension F],
  CategoryTheory.IsIso (L.lanUnit.app F)
-- Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
CategoryTheory.Limits.inl_pushoutZeroZeroIso_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [inst_3 : CategoryTheory.Limits.HasBinaryCoproduct X Y],
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl
      (CategoryTheory.Limits.pushoutZeroZeroIso X Y).inv =
    CategoryTheory.Limits.pushout.inl 0 0
-- Mathlib.Algebra.Homology.ComplexShapeSigns
TotalComplexShapeSymmetry.mk : {I₁ : Type u_1} →
  {I₂ : Type u_2} →
    {I₁₂ : Type u_4} →
      {c₁ : ComplexShape I₁} →
        {c₂ : ComplexShape I₂} →
          {c₁₂ : ComplexShape I₁₂} →
            [inst : TotalComplexShape c₁ c₂ c₁₂] →
              [inst_1 : TotalComplexShape c₂ c₁ c₁₂] →
                (∀ (i₁ : I₁) (i₂ : I₂), c₂.π c₁ c₁₂ (i₂, i₁) = c₁.π c₂ c₁₂ (i₁, i₂)) →
                  (σ : I₁ → I₂ → ℤˣ) →
                    (∀ {i₁ i₁' : I₁},
                        c₁.Rel i₁ i₁' →
                          ∀ (i₂ : I₂), σ i₁ i₂ * c₁.ε₁ c₂ c₁₂ (i₁, i₂) = c₂.ε₂ c₁ c₁₂ (i₂, i₁) * σ i₁' i₂) →
                      (∀ (i₁ : I₁) {i₂ i₂' : I₂},
                          c₂.Rel i₂ i₂' → σ i₁ i₂ * c₁.ε₂ c₂ c₁₂ (i₁, i₂) = c₂.ε₁ c₁ c₁₂ (i₂, i₁) * σ i₁ i₂') →
                        TotalComplexShapeSymmetry c₁ c₂ c₁₂
-- Init.Data.Char.Ordinal
Char.map_ordinal_succ? : ∀ {c : Char}, Option.map Char.ordinal c.succ? = c.ordinal.addNat? 1
-- Mathlib.Logic.Function.CompTypeclasses
CompTriple.comp_inv : ∀ {M : Type u_1} {N : Type u_2} {φ : M → N} {ψ : N → M},
  Function.RightInverse φ ψ → ∀ {χ : M → M} [CompTriple.IsId χ], CompTriple φ ψ χ
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.associatorNatIso_inv_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C × C × C),
  (CategoryTheory.MonoidalCategory.associatorNatIso C).inv.app X =
    (CategoryTheory.MonoidalCategoryStruct.associator X.1 X.2.1 X.2.2).inv
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.skipPrefix?_prop_eq_some_iff : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String} {pos : s.Pos},
  s.skipPrefix? P = some pos ↔ ∃ (h : s.startPos ≠ s.endPos), pos = s.startPos.next h ∧ P (s.startPos.get h)
-- Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
ContinuousAlternatingMap.alternatizeUncurryFinCLM_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ}
  (f : E →L[𝕜] E [⋀^Fin n]→L[𝕜] F),
  (ContinuousAlternatingMap.alternatizeUncurryFinCLM 𝕜 E F) f = ContinuousAlternatingMap.alternatizeUncurryFin f
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
Real.iSup_const_zero : ∀ {ι : Sort u_1}, ⨆ x, 0 = 0
-- Mathlib.Order.Filter.Ultrafilter.Basic
Ultrafilter.finite_sUnion_mem_iff : ∀ {α : Type u} {f : Ultrafilter α} {s : Set (Set α)}, s.Finite → (⋃₀ s ∈ f ↔ ∃ t ∈ s, t ∈ f)
-- Mathlib.Algebra.Pointwise.Stabilizer
AddAction.stabilizer_finset_empty : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : DecidableEq α],
  AddAction.stabilizer G ∅ = ⊤
-- Mathlib.LinearAlgebra.Prod
LinearMap.ker_coprod_of_disjoint_range : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {M₂ : Type u_3}
  [inst_3 : AddCommGroup M₂] [inst_4 : Module R M₂] {M₃ : Type u_4} [inst_5 : AddCommGroup M₃] [inst_6 : Module R M₃]
  (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃), Disjoint f.range g.range → (f.coprod g).ker = f.ker.prod g.ker
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
Real.deriv_fourierChar : ∀ (x : ℝ), deriv (fun x => ↑(Real.fourierChar x)) x = 2 * ↑Real.pi * Complex.I * ↑(Real.fourierChar x)
-- Std.Time.Zoned.RecurringRule
/-- `Jn` form: Julian day 1–365 (Feb 29 never counted, even in leap years).
 -/
Std.Time.TimeZone.TransitionSpec.julian : Std.Time.Internal.Bounded.LE 1 365 → Std.Time.TimeZone.TransitionSpec
-- Std.Data.DHashMap.Raw
/-- If there is no mapping for the given key, inserts the given mapping into the map. Otherwise,
returns the map unaltered.
 -/
Std.DHashMap.Raw.insertIfNew : {α : Type u} → {β : α → Type v} → [BEq α] → [Hashable α] → Std.DHashMap.Raw α β → (a : α) → β a → Std.DHashMap.Raw α β
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- **Alias** of `AddMonoidHom.domRestrictHom`.

---

A version of `AddMonoidHom.domRestrict` as a homomorphism.  -/
AddMonoidHom.restrictHom : {M : Type u_1} →
  [inst : AddZeroClass M] →
    {S : Type u_5} →
      [inst_1 : SetLike S M] →
        [inst_2 : AddSubmonoidClass S M] → (M' : S) → (A : Type u_6) → [inst_3 : AddCommMonoid A] → (M →+ A) →+ ↥M' →+ A
-- Mathlib.Order.Heyting.Basic
le_compl_iff_disjoint_right : ∀ {α : Type u_2} [inst : HeytingAlgebra α] {a b : α}, a ≤ bᶜ ↔ Disjoint a b
-- Lean.Server.References
/-- Finds all references in `trees`.  -/
Lean.Server.findReferences : Lean.FileMap → Array Lean.Elab.InfoTree → Array Lean.Server.Reference
-- Mathlib.RingTheory.Trace.Basic
/-- The dual basis of a powerbasis `{1, x, x²...}` under the trace form is `aᵢ / f'(x)`,
with `f` being the minimal polynomial of `x` and `f / (X - x) = ∑ aᵢxⁱ`.
 -/
Module.Basis.traceDual_powerBasis_eq : ∀ {K : Type u_4} {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : FiniteDimensional K L] [inst_4 : Algebra.IsSeparable K L] (pb : PowerBasis K L) (i : Fin pb.dim),
  pb.basis.traceDual i =
    (minpolyDiv K pb.gen).coeff ↑i / (Polynomial.aeval pb.gen) (Polynomial.derivative (minpoly K pb.gen))
-- Mathlib.GroupTheory.Perm.Centralizer
Equiv.Perm.Basis.sameCycle : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {g : Equiv.Perm α} (a : g.Basis) {x : α}
  (hx : g.cycleOf x ∈ g.cycleFactorsFinset), g.SameCycle (a ⟨g.cycleOf x, hx⟩) x
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.pointEquivSubtype_symm_some : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} [inst_1 : Nontrivial R]
  [inst_2 : WeierstrassCurve.IsElliptic W'] {x y : R} {h : W'.Equation x y} {p : W'.Point → Prop}
  (p0 : p WeierstrassCurve.Affine.Point.zero) (ph : p (WeierstrassCurve.Affine.Point.mk h)),
  (WeierstrassCurve.Affine.pointEquivSubtype p0).symm (some ⟨(x, y), ⋯⟩) = ⟨WeierstrassCurve.Affine.Point.mk h, ph⟩
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- An angle in a right-angled triangle expressed using `arctan`, version subtracting vectors.  -/
InnerProductGeometry.angle_sub_eq_arctan_of_inner_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  inner ℝ x y = 0 → x ≠ 0 → InnerProductGeometry.angle x (x - y) = Real.arctan (‖y‖ / ‖x‖)
-- Mathlib.RingTheory.Ideal.GoingUp
Ideal.nonempty_primesOver : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.IsIntegral R S] [FaithfulSMul R S] (P : Ideal R) [P.IsPrime], Nonempty ↑(P.primesOver S)
-- Mathlib.Order.Basic
Prod.mk_lt_mk_iff_left : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {a₁ a₂ : α} {b : β},
  (a₁, b) < (a₂, b) ↔ a₁ < a₂
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.mulPow_nc.eq_def : ∀ (pw : Lean.Grind.CommRing.Power) (m : Lean.Grind.CommRing.Mon),
  Lean.Grind.CommRing.Mon.mulPow_nc pw m =
    match m with
    | Lean.Grind.CommRing.Mon.unit => Lean.Grind.CommRing.Mon.mult pw Lean.Grind.CommRing.Mon.unit
    | Lean.Grind.CommRing.Mon.mult pw' m =>
      bif pw.x == pw'.x then Lean.Grind.CommRing.Mon.mult { x := pw.x, k := pw.k + pw'.k } m
      else Lean.Grind.CommRing.Mon.mult pw (Lean.Grind.CommRing.Mon.mult pw' m)
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.evalEval.eq_1 : ∀ {R : Type u_1} [inst : Semiring R] (x y : R) (p : Polynomial (Polynomial R)),
  Polynomial.evalEval x y p = Polynomial.eval x (Polynomial.eval (Polynomial.C y) p)
-- Mathlib.Algebra.Module.Torsion.Basic
Ideal.quotTorsionOfEquivSpanSingleton_apply_mk : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (x : M) (a : R),
  (Ideal.quotTorsionOfEquivSpanSingleton R M x) (Submodule.Quotient.mk a) = a • ⟨x, ⋯⟩
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey_congr : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp] (h : t.WF)
  {k₁ k₂ : α} (h' : cmp k₁ k₂ = Ordering.eq) (h₁ : k₁ ∈ t), t.getKey k₁ h₁ = t.getKey k₂ ⋯
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.beq_iff_equiv : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [LawfulBEq α]
  [inst_3 : BEq β] [LawfulBEq β], m₁.WF → m₂.WF → ((m₁ == m₂) = true ↔ m₁.Equiv m₂)
-- Mathlib.Order.Hom.Bounded
TopHom.instPreorder.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Top α] [inst_1 : Preorder β] [inst_2 : Top β],
  TopHom.instPreorder = Preorder.lift DFunLike.coe
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
/-- The underlying set.  -/
Delone.DeloneSet.carrier : {X : Type u_3} → [inst : MetricSpace X] → Delone.DeloneSet X → Set X
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKey!_insertManyIfNewUnit_emptyWithCapacity_list_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited α] {l : List α}
  {k : α},
  l.contains k = false →
    (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)).getKey! k =
      default
-- Mathlib.Analysis.Real.Pi.Chudnovsky
/-- The numerator of the nth term in Chudnovsky's series  -/
chudnovskyNum : ℕ → ℤ
-- Mathlib.Data.Matrix.Mul
Matrix.sub_mulVec : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalNonAssocRing α] [inst_1 : Fintype n] (A B : Matrix m n α)
  (x : n → α), (A - B).mulVec x = A.mulVec x - B.mulVec x
-- Init.Data.Range.Polymorphic.Iterators
Std.Rcc.Internal.iter.eq_1 : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] (r : Std.Rcc α),
  Std.Rcc.Internal.iter r = { internalState := { next := some r.lower, upperBound := r.upper } }
-- Mathlib.Algebra.Group.TransferInstance
Equiv.addCommSemigroup.eq_1 : ∀ {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : AddCommSemigroup β],
  e.addCommSemigroup = Function.Injective.addCommSemigroup ⇑e ⋯ ⋯
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.BasedNatTrans.instReflectsIsomorphismsBasedFunctorFunctorObjForgetful : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] {𝒳 : CategoryTheory.BasedCategory 𝒮}
  {𝒴 : CategoryTheory.BasedCategory 𝒮}, (CategoryTheory.BasedNatTrans.forgetful 𝒳 𝒴).ReflectsIsomorphisms
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.residueFieldMap_id : ∀ {X : AlgebraicGeometry.Scheme} (x : ↥X),
  AlgebraicGeometry.Scheme.Hom.residueFieldMap (CategoryTheory.CategoryStruct.id X) x =
    CategoryTheory.CategoryStruct.id (X.residueField x)
-- Mathlib.Order.Interval.Set.Limit
Set.Ici.isSuccLimit_coe : ∀ {J : Type u} [inst : LinearOrder J] {j : J} (m : ↑(Set.Ici j)), Order.IsSuccLimit m → Order.IsSuccLimit ↑m
-- Mathlib.Analysis.Calculus.FDeriv.Defs
/-- **Alias** of the forward direction of `hasFDerivAt_iff_isLittleOTVS`. -/
HasFDerivAt.isLittleOTVS : ∀ {𝕜 : 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} {f' : E →L[𝕜] F} {x : E},
  HasFDerivAt f f' x → (fun x' => f x' - f x - f' (x' - x)) =o[𝕜; nhds x] fun x' => x' - x
-- ProofWidgets.Component.FilterDetails
/-- Whether to start in the filtered state.  -/
ProofWidgets.FilterDetailsProps.initiallyFiltered : ProofWidgets.FilterDetailsProps → Bool
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.Hom.mk : {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] →
        {A : Type u_5} →
          [inst_2 : AddMonoid A] →
            [inst_3 : CategoryTheory.HasShift D A] →
              {F G : CategoryTheory.SingleFunctors C D A} →
                (hom : (a : A) → F.functor a ⟶ G.functor a) →
                  autoParam
                      (∀ (n a a' : A) (ha' : n + a = a'),
                        CategoryTheory.CategoryStruct.comp (F.shiftIso n a a' ha').hom (hom a) =
                          CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.Functor.whiskerRight (hom a') (CategoryTheory.shiftFunctor D n))
                            (G.shiftIso n a a' ha').hom)
                      CategoryTheory.SingleFunctors.Hom.comm._autoParam →
                    F.Hom G
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.ite_sum_zero : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] (p : Prop) [inst_1 : Decidable p] (s : Finset ι) (f : ι → M),
  (if p then ∑ x ∈ s, f x else 0) = ∑ x ∈ s, if p then f x else 0
-- Mathlib.Topology.Compactness.CompactSystem
/-- Any subset of a compact system is a compact system.  -/
IsCompactSystem.mono : ∀ {α : Type u_1} {S T : Set (Set α)}, IsCompactSystem T → S ⊆ T → IsCompactSystem S
-- Mathlib.Order.RelIso.Set
RelHomClass.directed : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {F : Type u_3} [inst : FunLike F α β]
  [RelHomClass F r s] {ι : Sort u_4} {a : ι → α} {f : F}, Directed r a → Directed s (⇑f ∘ a)
-- Lean.Meta.MkIffOfInductiveProp
/-- `mkOrList [x1, x2, ...]` is defined as `x1 ∨ (x2 ∨ ...)`, or `False` if the list is empty.  -/
_private.Lean.Meta.MkIffOfInductiveProp.0.Lean.Meta.mkOrList : List Lean.Expr → Lean.Expr
-- Mathlib.RingTheory.Ideal.Over
Ideal.instLiesOverBotOfIsPrime : ∀ {K : Type u_2} {A : Type u_3} [inst : Field K] [inst_1 : Semiring A] [inst_2 : Algebra K A] (P : Ideal A) [P.IsPrime],
  P.LiesOver ⊥
-- Mathlib.Computability.Language
Language.mem_iSup : ∀ {α : Type u_1} {ι : Sort v} {l : ι → Language α} {x : List α}, x ∈ ⨆ i, l i ↔ ∃ i, x ∈ l i
-- Aesop.Search.ExpandSafePrefix
Aesop.SafeExpansionM : (Q : Type) → [Aesop.Queue Q] → Type → Type
-- Init.Data.Array.Lex.Lemmas
_private.Init.Data.Array.Lex.Lemmas.0.Array.cons_lex_cons : ∀ {α : Type u_1} [inst : BEq α] {lt : α → α → Bool} {a b : α} {xs ys : Array α},
  (#[a] ++ xs).lex (#[b] ++ ys) lt = (lt a b || a == b && xs.lex ys lt)
-- Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
UpperHalfPlane.mdifferentiableAt_iff : ∀ {f : UpperHalfPlane → ℂ} {τ : UpperHalfPlane}, MDiffAt f τ ↔ DifferentiableAt ℂ (f ∘ ↑UpperHalfPlane.ofComplex) ↑τ
-- Mathlib.Algebra.Order.Ring.GeomSum
geom_sum_alternating_of_lt_neg_one : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : PartialOrder R] [IsStrictOrderedRing R] {n : ℕ} {x : R},
  x + 1 < 0 → 1 < n → if Even n then ∑ i ∈ Finset.range n, x ^ i < 0 else 1 < ∑ i ∈ Finset.range n, x ^ i
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.veq_trans : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x y z : R}, x =ᵥ y → y =ᵥ z → x =ᵥ z
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.zpow_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Group β]
  [inst_3 : IsTopologicalGroup β] (f : C(α, β)) (z : ℤ) (x : α), (f ^ z) x = f x ^ z