mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.max?_eq_some_maxD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {fallback : α}, t.max? = some (t.maxD fallback)
-- Mathlib.RingTheory.AdicCompletion.Functoriality
AdicCompletion.sumInv_comp_sum : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {ι : Type u_6} (M : ι → Type u_7)
  [inst_1 : (i : ι) → AddCommGroup (M i)] [inst_2 : (i : ι) → Module R (M i)] [inst_3 : Fintype ι]
  [inst_4 : DecidableEq ι], AdicCompletion.sumInv I M ∘ₗ AdicCompletion.sum I M = LinearMap.id
-- Mathlib.Combinatorics.Additive.SubsetSum
/-- The subset-sum of a finite set `A` in a commutative monoid is the set of all sums
of subsets of `A`.  -/
Finset.subsetSum : {M : Type u_1} → [DecidableEq M] → [AddCommMonoid M] → Finset M → Finset M
-- Mathlib.Tactic.Linter.DeprecatedSyntaxLinter
/-- The option `linter.style.admit` of the deprecated syntax linter flags usages of
the `admit` tactic, which is a synonym for the much more common `sorry`.  -/
Mathlib.Linter.Style.linter.style.admit : Lean.Option Bool
-- Lean.Data.Lsp.Basic
/-- A `Location` is a `DocumentUri` and a `Range`.  -/
Lean.Lsp.Location : Type
-- Mathlib.Order.Filter.Ultrafilter.Defs
/-- If `g` is a nontrivial filter that is less than or equal to an ultrafilter, then it is greater
than or equal to the ultrafilter.  -/
Ultrafilter.le_of_le : ∀ {α : Type u_2} (self : Ultrafilter α) (g : Filter α), g.NeBot → g ≤ ↑self → ↑self ≤ g
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.norm_map : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
  [inst_5 : Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (x : E), ‖f x‖ = ‖x‖
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
LiouvilleWith.sub_rat_iff : ∀ {p x : ℝ} {r : ℚ}, LiouvilleWith p (x - ↑r) ↔ LiouvilleWith p x
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.mk : {C : Type u} →
  [inst : CategoryTheory.Groupoid C] →
    (arrows : (c d : C) → Set (c ⟶ d)) →
      (∀ {c d : C} {p : c ⟶ d}, p ∈ arrows c d → CategoryTheory.Groupoid.inv p ∈ arrows d c) →
        (∀ {c d e : C} {p : c ⟶ d},
            p ∈ arrows c d → ∀ {q : d ⟶ e}, q ∈ arrows d e → CategoryTheory.CategoryStruct.comp p q ∈ arrows c e) →
          CategoryTheory.Subgroupoid C
-- Mathlib.LinearAlgebra.Eigenspace.Basic
/-- If there exists a natural number `k` such that the kernel of `(f - μ • id) ^ k` is the
maximal generalized eigenspace, then this value is the least such `k`. If not, this value is not
meaningful.  -/
Module.End.maxGenEigenspaceIndex : {R : Type v} →
  {M : Type w} → [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Module.End R M → R → ℕ
-- Init.Data.BitVec.Lemmas
BitVec.getElem_of_getLsbD_eq_true : ∀ {w : ℕ} {x : BitVec w} {i : ℕ} (h : x.getLsbD i = true), (x[i] = true) = True
-- Mathlib.Topology.MetricSpace.IsometricSMul
dist_sub_left : ∀ {G : Type v} [inst : AddGroup G] [inst_1 : PseudoMetricSpace G] [IsIsometricVAdd G G] [IsIsometricVAdd Gᵃᵒᵖ G]
  (a b c : G), dist (a - b) (a - c) = dist b c
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instSemigroupOfMulHomClass : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [inst_4 : (i : ι) → Semigroup (G i)] →
                  [∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)] → Semigroup (DirectLimit G f)
-- Mathlib.NumberTheory.Divisors
Nat.prod_divisorsAntidiagonal' : ∀ {M : Type u_1} [inst : CommMonoid M] (f : ℕ → ℕ → M) {n : ℕ},
  ∏ i ∈ n.divisorsAntidiagonal, f i.1 i.2 = ∏ i ∈ n.divisors, f (n / i) i
-- Mathlib.Topology.Subpath
/-- The range of a subpath is the image of the original path on the relevant interval.  -/
Path.range_subpath : ∀ {X : Type u_1} [inst : TopologicalSpace X] {a b : X} (γ : Path a b) (t₀ t₁ : ↑unitInterval),
  Set.range ⇑(γ.subpath t₀ t₁) = ⇑γ '' Set.uIcc t₀ t₁
-- Lean.Parser.Term
Lean.Parser.Term.structInstDefault.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.Calculus.FDeriv.Prod
HasStrictFDerivAt.prodMk : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f₁ : E → F} {f₁' : E →L[𝕜] F} {x : E} {f₂ : E → G}
  {f₂' : E →L[𝕜] G},
  HasStrictFDerivAt f₁ f₁' x → HasStrictFDerivAt f₂ f₂' x → HasStrictFDerivAt (fun x => (f₁ x, f₂ x)) (f₁'.prod f₂') x
-- Init.Data.SInt.Lemmas
Int16.toInt_ofNat_of_lt : ∀ {n : ℕ}, n < 2 ^ 15 → (Int16.ofNat n).toInt = ↑n
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonLeanPrepareModuleHierarchyParams : Lean.FromJson Lean.Lsp.LeanPrepareModuleHierarchyParams
-- Lean.SubExpr
Lean.SubExpr.GoalsLocation.mk.inj : ∀ {mvarId : Lean.MVarId} {loc : Lean.SubExpr.GoalLocation} {mvarId_1 : Lean.MVarId} {loc_1 : Lean.SubExpr.GoalLocation},
  { mvarId := mvarId, loc := loc } = { mvarId := mvarId_1, loc := loc_1 } → mvarId = mvarId_1 ∧ loc = loc_1
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
/-- The gluing as locally ringed spaces is isomorphic to the gluing as ringed spaces.  -/
AlgebraicGeometry.LocallyRingedSpace.GlueData.isoSheafedSpace : (D : AlgebraicGeometry.LocallyRingedSpace.GlueData) → D.glued.toSheafedSpace ≅ D.toSheafedSpaceGlueData.glued
-- Mathlib.MeasureTheory.Measure.EverywherePos
IsClosed.everywherePosSubset : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α},
  IsClosed s → IsClosed (μ.everywherePosSubset s)
-- Mathlib.Order.SuccPred.LinearLocallyFinite
toZ_iterate_succ : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : SuccOrder ι] [inst_2 : IsSuccArchimedean ι] [inst_3 : PredOrder ι]
  {i0 : ι} [NoMaxOrder ι] (n : ℕ), toZ i0 (Order.succ^[n] i0) = ↑n
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
/-- Computes the absolute discriminant of the `n`-th cyclotomic field.
 -/
IsCyclotomicExtension.Rat.discr : ∀ (n : ℕ) (K : Type u) [inst : Field K] [inst_1 : CharZero K] [hn : NeZero n] [hK : IsCyclotomicExtension {n} ℚ K],
  NumberField.discr K = (-1) ^ (n.totient / 2) * (↑n ^ n.totient / ↑(∏ p ∈ n.primeFactors, p ^ (n.totient / (p - 1))))
-- Mathlib.Computability.Primrec.List
Primrec.vector_toList_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {n : ℕ} {f : α → List.Vector β n},
  (Primrec fun a => (f a).toList) ↔ Primrec f
-- Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup
AddGrpCat.toGrp_map : ∀ {x x_1 : AddGrpCat} (f : x ⟶ x_1),
  AddGrpCat.toGrp.map f = GrpCat.ofHom (AddMonoidHom.toMultiplicative (AddGrpCat.Hom.hom f))
-- Mathlib.Order.Lattice
inf_left_idem : ∀ {α : Type u} [inst : SemilatticeInf α] (a b : α), a ⊓ (a ⊓ b) = a ⊓ b
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.small_Icc : ∀ (a b : Cardinal.{u}), Small.{u, u + 1} ↑(Set.Icc a b)
-- Mathlib.Topology.ContinuousOn
continuousWithinAt_congr_of_insert : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : α → β} {s : Set α}
  {x : α}, (∀ y ∈ insert x s, g y = f y) → (ContinuousWithinAt g s x ↔ ContinuousWithinAt f s x)
-- Lean.Parser.Types
Lean.Parser.ParserState.mk.sizeOf_spec : ∀ (stxStack : Lean.Parser.SyntaxStack) (lhsPrec : ℕ) (pos : String.Pos.Raw) (cache : Lean.Parser.ParserCache)
  (errorMsg : Option Lean.Parser.Error)
  (recoveredErrors : Array (String.Pos.Raw × Lean.Parser.SyntaxStack × Lean.Parser.Error)),
  sizeOf
      { stxStack := stxStack, lhsPrec := lhsPrec, pos := pos, cache := cache, errorMsg := errorMsg,
        recoveredErrors := recoveredErrors } =
    1 + sizeOf stxStack + sizeOf lhsPrec + sizeOf pos + sizeOf cache + sizeOf errorMsg + sizeOf recoveredErrors
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.map_pure : ∀ {α β : Type u} (f : α → β) (x : α), f <$> pure x = pure (f x)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.of_forall_contains_unit_eq : ∀ {α : Type u} {instOrd : Ord α} [Std.TransOrd α] [Std.LawfulEqOrd α]
  {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => Unit},
  t₁.WF →
    t₂.WF →
      (∀ (k : α), Std.DTreeMap.Internal.Impl.contains k t₁ = Std.DTreeMap.Internal.Impl.contains k t₂) → t₁.Equiv t₂
-- Mathlib.Data.FinEnum
FinEnum.instSigma : {α : Type u} → (β : α → Type v) → [FinEnum α] → [(a : α) → FinEnum (β a)] → FinEnum (Sigma β)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.univ_mul_univ : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Monoid α] [inst_2 : Fintype α],
  Finset.univ * Finset.univ = Finset.univ
-- Mathlib.Algebra.Category.BialgCat.Basic
/-- A type alias for `BialgHom` to avoid confusion between the categorical and
algebraic spellings of composition.  -/
BialgCat.Hom : {R : Type u} → [inst : CommRing R] → BialgCat R → BialgCat R → Type v
-- Mathlib.Algebra.Order.Interval.Set.Monoid
Set.Ico_add_bij : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [IsOrderedCancelAddMonoid M] [ExistsAddOfLE M]
  (a b d : M), Set.BijOn (fun x => x + d) (Set.Ico a b) (Set.Ico (a + d) (b + d))
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.Nonnegg.eq_2 : ∀ (c d a b : ℕ), Zsqrtd.Nonnegg c d (Int.ofNat a) (Int.negSucc b) = Zsqrtd.SqLe (b + 1) c a d
-- Mathlib.Algebra.BigOperators.WithTop
/-- A sum is infinite iff one term is infinite.  -/
WithTop.sum_eq_top : ∀ {ι : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] {s : Finset ι} {f : ι → WithTop M},
  ∑ i ∈ s, f i = ⊤ ↔ ∃ i ∈ s, f i = ⊤
-- Mathlib.CategoryTheory.Localization.LocallySmall
/-- If a class of morphisms `W : MorphismProperty C` satisfies `HasLocalization.{w} W`,
then any localized category for `W` (i.e. any target of a localization functor
`L : C ⥤ D` for `W`) is locally `w`-small.  -/
CategoryTheory.MorphismProperty.locallySmall_of_hasLocalization : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) [L.IsLocalization W]
  [W.HasLocalization], CategoryTheory.LocallySmall.{w, v₂, u₂} D
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.Collector.Context.mk : Lean.Expr → Array Lean.Expr → Lean.Meta.Grind.Collector.Context✝
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteMulArchimedeanClass.liftOrderHom.eq_1 : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {α : Type u_2}
  [inst_3 : PartialOrder α] (f : { a // a ≠ 1 } → α)
  (h : ∀ (a b : { a // a ≠ 1 }), FiniteMulArchimedeanClass.mk ↑a ⋯ ≤ FiniteMulArchimedeanClass.mk ↑b ⋯ → f a ≤ f b),
  FiniteMulArchimedeanClass.liftOrderHom f h = { toFun := FiniteMulArchimedeanClass.lift f ⋯, monotone' := ⋯ }
-- Mathlib.Order.Filter.AtTopBot.Archimedean
tendsto_intCast_atTop_atTop : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : PartialOrder R] [IsStrictOrderedRing R] [Archimedean R],
  Filter.Tendsto Int.cast Filter.atTop Filter.atTop
-- Mathlib.Data.Complex.BigOperators
Complex.re_sum : ∀ {α : Type u_1} (s : Finset α) (f : α → ℂ), (∑ i ∈ s, f i).re = ∑ i ∈ s, (f i).re
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.instLE : {ι : Type u_1} → LE (BoxIntegral.Box ι)
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.mapAlongRingHom_apply : ∀ {ι₁ : Type u_3} {ι₂ : Type u_4} (R₁ : ι₁ → Type u_5) (R₂ : ι₂ → Type u_6) {𝓕₁ : Filter ι₁} {𝓕₂ : Filter ι₂}
  {S₁ : ι₁ → Type u_7} {S₂ : ι₂ → Type u_8} [inst : (i : ι₁) → SetLike (S₁ i) (R₁ i)]
  [inst_1 : (j : ι₂) → SetLike (S₂ j) (R₂ j)] {B₁ : (i : ι₁) → S₁ i} {B₂ : (j : ι₂) → S₂ j} (f : ι₂ → ι₁)
  (hf : Filter.Tendsto f 𝓕₂ 𝓕₁) [inst_2 : (i : ι₁) → Ring (R₁ i)] [inst_3 : (i : ι₂) → Ring (R₂ i)]
  [inst_4 : ∀ (i : ι₁), SubringClass (S₁ i) (R₁ i)] [inst_5 : ∀ (i : ι₂), SubringClass (S₂ i) (R₂ i)]
  (φ : (j : ι₂) → R₁ (f j) →+* R₂ j) (hφ : ∀ᶠ (j : ι₂) in 𝓕₂, Set.MapsTo ⇑(φ j) ↑(B₁ (f j)) ↑(B₂ j))
  (x : RestrictedProduct (fun i => R₁ i) (fun i => ↑(B₁ i)) 𝓕₁) (j : ι₂),
  ((RestrictedProduct.mapAlongRingHom R₁ R₂ f hf φ hφ) x) j = (φ j) (x (f j))
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.num.injEq : ∀ (k k_1 : ℤ), (Int.Internal.Linear.Poly.num k = Int.Internal.Linear.Poly.num k_1) = (k = k_1)
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.topIso_inv_ι : ∀ (X : SSet),
  CategoryTheory.CategoryStruct.comp (SSet.Subcomplex.topIso X).inv (CategoryTheory.Subfunctor.ι ⊤) =
    CategoryTheory.CategoryStruct.id X
-- Mathlib.Topology.Sheaves.Stalks
/-- The stalk of a presheaf `F` at a point `x` is calculated as the colimit of the functor
nbhds x ⥤ opens F.X ⥤ C
 -/
TopCat.Presheaf.stalk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasColimits C] → {X : TopCat} → TopCat.Presheaf C X → ↑X → C
-- Batteries.Tactic.Lint.Basic
/-- A linting test for the `#lint` command.  -/
Batteries.Tactic.Lint.Linter : Type
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.reflective' : ∀ {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]
  [inst_5 : ∀ (F : CategoryTheory.Functor C H), L.HasPointwiseRightKanExtension F],
  CategoryTheory.IsIso (L.ranAdjunction H).counit
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosSemidef.submatrix : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
  {M : Matrix n n R}, M.PosSemidef → ∀ (e : m → n), (M.submatrix e e).PosSemidef
-- Mathlib.Geometry.Manifold.Algebra.Monoid
/-- **Alias** of `contMDiffAt_finsetProd'`. -/
contMDiffAt_finset_prod' : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : CommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffMul I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {x : M} {t : Finset ι} {f : ι → M → G},
  (∀ i ∈ t, ContMDiffAt I' I n (f i) x) → ContMDiffAt I' I n (∏ i ∈ t, f i) x
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- Given three points in weak order on the same line, with the first not equal to the second,
and a fourth point, the angles at the fourth point between the first and second or first and
third points have the same sign.  -/
Wbtw.oangle_sign_eq_of_ne_left : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P} (p₄ : P),
  Wbtw ℝ p₁ p₂ p₃ → p₁ ≠ p₂ → (EuclideanGeometry.oangle p₁ p₄ p₂).sign = (EuclideanGeometry.oangle p₁ p₄ p₃).sign
-- Mathlib.Computability.AkraBazzi.GrowsPolynomially
AkraBazziRecurrence.GrowsPolynomially.of_isEquivalent : ∀ {f g : ℝ → ℝ},
  AkraBazziRecurrence.GrowsPolynomially g →
    Asymptotics.IsEquivalent Filter.atTop f g → AkraBazziRecurrence.GrowsPolynomially f
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesAt.continuousAt : ∀ {𝕜 : 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] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E}, HasFPowerSeriesAt f p x → ContinuousAt f x
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
/-- The value of the quadratic character on `a` is zero iff `a = 0`.  -/
quadraticChar_eq_zero_iff : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F] {a : F}, (quadraticChar F) a = 0 ↔ a = 0
-- Mathlib.Combinatorics.Matroid.Rank.Finite
Matroid.isRkFinite_singleton : ∀ {α : Type u_1} {M : Matroid α} {e : α}, M.IsRkFinite {e}
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.inv_hom_apply : ∀ {X Y : AlgebraicGeometry.Scheme} (e : X ≅ Y) (y : ↥Y), e.hom (e.inv y) = y
-- Mathlib.Algebra.Category.Semigrp.Basic
AddEquiv.toAddSemigrpIso.eq_1 : ∀ {X Y : Type u} [inst : AddSemigroup X] [inst_1 : AddSemigroup Y] (e : X ≃+ Y),
  e.toAddSemigrpIso =
    { hom := AddSemigrp.ofHom e.toAddHom, inv := AddSemigrp.ofHom e.symm.toAddHom, hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.inv_hom_id_right_assoc : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (e : f ≅ g) {Z : T}
  (h : g.right ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right e.inv)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right e.hom) h) =
    h
-- Init.Data.BitVec.Bitblast
BitVec.cpop_eq_cpopRec : ∀ {w : ℕ} {x : BitVec w}, x.cpop = x.cpopRec
-- Mathlib.Topology.Category.TopCat.Limits.Pullbacks
TopCat.isInducing_pullback_to_prod : ∀ {X Y Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z),
  Topology.IsInducing
    ⇑(CategoryTheory.ConcreteCategory.hom
        (CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.pullback.fst f g)
          (CategoryTheory.Limits.pullback.snd f g)))
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.Int64.toBitVec_ite : ∀ {c : Prop} {t e : Int64} [inst : Decidable c], (if c then t else e).toBitVec = if c then t.toBitVec else e.toBitVec
-- Mathlib.LinearAlgebra.Matrix.Module
LinearMap.mapMatrixModule_id : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Ring R] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M], LinearMap.mapMatrixModule ι LinearMap.id = LinearMap.id
-- Mathlib.NumberTheory.ArithmeticFunction.Carmichael
/-- Note that `2 ^ (n - 1) = 1` when `n = 0`.  -/
ArithmeticFunction.carmichael_two_pow_of_le_two : ∀ {n : ℕ}, n ≤ 2 → ArithmeticFunction.carmichael (2 ^ n) = 2 ^ (n - 1)
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremKind.eqBwd.sizeOf_spec : sizeOf Lean.Meta.Grind.EMatchTheoremKind.eqBwd = 1
-- Mathlib.Data.Set.Lattice
Set.iUnion_sigma : ∀ {α : Type u_1} {β : Type u_2} {γ : α → Type u_12} (s : Sigma γ → Set β), ⋃ ia, s ia = ⋃ i, ⋃ a, s ⟨i, a⟩
-- Lean.Compiler.ExternAttr
Lean.ExternEntry : Type
-- Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
ExistsContDiffBumpBase.w.congr_simp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] (D D_1 : ℝ),
  D = D_1 → ∀ (x x_1 : E), x = x_1 → ExistsContDiffBumpBase.w D x = ExistsContDiffBumpBase.w D_1 x_1
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.neighborFinset_eq_empty : ∀ {V : Type u_1} (G : SimpleGraph V) (v : V) [inst : Fintype ↑(G.neighborSet v)],
  G.neighborFinset v = ∅ ↔ G.IsIsolated v
-- Mathlib.GroupTheory.GroupExtension.Defs
/-- `Section` is a right inverse to `S.rightHom`  -/
AddGroupExtension.Section.rightInverse_rightHom : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : AddGroup N] [inst_1 : AddGroup E] [inst_2 : AddGroup G]
  {S : AddGroupExtension N E G} (self : S.Section), Function.RightInverse self.toFun ⇑S.rightHom
-- Init.Data.Array.GetLit
Array.getLit.congr_simp : ∀ {α : Type u} {n n_1 : ℕ} (e_n : n = n_1) (xs xs_1 : Array α) (e_xs : xs = xs_1) (i i_1 : ℕ) (e_i : i = i_1)
  (h₁ : xs.size = n) (h₂ : i < n), xs.getLit i h₁ h₂ = xs_1.getLit i_1 ⋯ ⋯
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.monadToFunctor_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : CategoryTheory.Monad C} (f : X ⟶ Y),
  (CategoryTheory.monadToFunctor C).map f = f.toNatTrans
-- Mathlib.Algebra.MonoidAlgebra.Module
/-- A copy of `Finsupp.lsingle` for `AddMonoidAlgebra`.  -/
AddMonoidAlgebra.lsingle : {R : Type u_1} →
  {S : Type u_2} →
    {M : Type u_3} →
      [inst : Semiring S] → [inst_1 : Semiring R] → [inst_2 : Module R S] → M → S →ₗ[R] AddMonoidAlgebra S M
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.comap_mono : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : C(X, Y))
  {A B : DiscreteQuotient Y}, A ≤ B → DiscreteQuotient.comap f A ≤ DiscreteQuotient.comap f B
-- Mathlib.LinearAlgebra.Ray
/-- If `x` and `y` are nonzero vectors on the same ray, then there exist positive numbers `r₁ r₂`
such that `r₁ • x = r₂ • y`.  -/
SameRay.exists_pos : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {x y : M},
  SameRay R x y → x ≠ 0 → y ≠ 0 → ∃ r₁ r₂, 0 < r₁ ∧ 0 < r₂ ∧ r₁ • x = r₂ • y
-- Mathlib.CategoryTheory.Monoidal.Action.End
CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_η_unmop_app : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (X : D),
  (CategoryTheory.Functor.OplaxMonoidal.η
            (CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMop C D)).unmop.app
      X =
    (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso X).hom
-- Mathlib.MeasureTheory.Function.LpSpace.Complete
MeasureTheory.Lp.ae_tendsto_of_cauchy_eLpNorm : ∀ {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {E : Type u_3}
  [inst : NormedAddCommGroup E] [CompleteSpace E] {f : ℕ → α → E},
  (∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ) →
    1 ≤ p →
      ∀ {B : ℕ → ENNReal},
        ∑' (i : ℕ), B i ≠ ⊤ →
          (∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → MeasureTheory.eLpNorm (f n - f m_1) p μ < B N) →
            ∀ᵐ (x : α) ∂μ, ∃ l, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds l)
-- Mathlib.Analysis.Complex.Trigonometric
Complex.norm_cos_add_sin_mul_I : ∀ (x : ℝ), ‖Complex.cos ↑x + Complex.sin ↑x * Complex.I‖ = 1
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.union_left : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ m₃ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α], m₁.Equiv m₂ → (m₁ ∪ m₃).Equiv (m₂ ∪ m₃)
-- Lean.Parser.Types
Lean.Parser.FirstTokens.optTokens.inj : ∀ {a a_1 : List Lean.Parser.Token},
  Lean.Parser.FirstTokens.optTokens a = Lean.Parser.FirstTokens.optTokens a_1 → a = a_1
-- Mathlib.Data.Nat.Fib.Zeckendorf
Nat.greatestFib_mono : Monotone Nat.greatestFib
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Subgraph.Connected.nonempty : ∀ {V : Type u} {G : SimpleGraph V} {H : G.Subgraph}, H.Connected → H.verts.Nonempty
-- Init.Data.Float.Float
/-- Obtains the `Float` whose value is the same as the given `UInt8`.  -/
UInt8.toFloat : UInt8 → Float
-- Mathlib.Probability.Martingale.Centering
MeasureTheory.predictablePart_zero : ∀ {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {f : ℕ → Ω → E} {ℱ : MeasureTheory.Filtration ℕ m0},
  MeasureTheory.predictablePart f ℱ μ 0 = 0
-- Init.Guard
/-- Syntactic matching for `guard_hyp` values  -/
Lean.Parser.colonEqS : Lean.ParserDescr
-- Mathlib.Analysis.InnerProductSpace.Calculus
HasDerivAt.inner : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : NormedSpace ℝ E] {f g : ℝ → E} {f' g' : E} {x : ℝ},
  HasDerivAt f f' x →
    HasDerivAt g g' x → HasDerivAt (fun t => inner 𝕜 (f t) (g t)) (inner 𝕜 (f x) g' + inner 𝕜 f' (g x)) x