mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.instIsZeroApply : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂], IsZeroApply (M₁ →SL[σ₁₂] M₂) M₁ M₂
-- Mathlib.RingTheory.Jacobson.Artinian
Module.finite_of_isSemisimpleRing : ∀ (R : Type u_1) (A : Type u_2) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Algebra.FiniteType R A] [IsJacobsonRing R] [IsSemisimpleRing A], Module.Finite R A
-- Init.GrindInstances.ToInt
Lean.Grind.instToIntInt8SintOfNatNat : Lean.Grind.ToInt Int8 (Lean.Grind.IntInterval.sint 8)
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.DiagramOfCones.mkOfHasLimits_conePoints : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [inst_3 : CategoryTheory.Limits.HasLimitsOfShape K C],
  (CategoryTheory.Limits.DiagramOfCones.mkOfHasLimits F).conePoints = F.comp CategoryTheory.Limits.lim
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.SeparatingLeft.toMatrix' : ∀ {R₂ : Type u_3} [inst : CommRing R₂] {ι : Type u_6} [inst_1 : DecidableEq ι] [inst_2 : Fintype ι]
  {B : LinearMap.BilinForm R₂ (ι → R₂)}, LinearMap.SeparatingLeft B → (LinearMap.BilinForm.toMatrix' B).SeparatingLeft
-- Mathlib.Probability.Process.Adapted
MeasureTheory.Adapted.measurable : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : ι → Type u_3} [inst_1 : (i : ι) → MeasurableSpace (β i)] {u : (i : ι) → Ω → β i} {i : ι},
  MeasureTheory.Adapted f u → Measurable (u i)
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.toOne : {E : Type u_3} → [inst : Group E] → [DecidableEq E] → One (GroupSeminorm E)
-- Mathlib.RingTheory.Flat.Tensor
Module.Baer.eq_1 : ∀ (R : Type u) [inst : Ring R] (Q : Type v) [inst_1 : AddCommGroup Q] [inst_2 : Module R Q],
  Module.Baer R Q = ∀ (I : Ideal R) (g : ↥I →ₗ[R] Q), ∃ g', ∀ (x : R) (mem : x ∈ I), g' x = g ⟨x, mem⟩
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Iterators.HetT.ext : ∀ {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] {α : Type v} {x y : Std.Iterators.HetT m α}
  (h : x.Property = y.Property),
  (∀ (β : Type w) (f : (a : α) → x.Property a → m β), x.prun f = y.prun fun a ha => f a ⋯) → x = y
-- Mathlib.Order.ModularLattice
covBy_sup_of_inf_covBy_of_inf_covBy_right : ∀ {α : Type u_1} [inst : Lattice α] [IsWeakUpperModularLattice α] {a b : α}, a ⊓ b ⋖ a → a ⊓ b ⋖ b → b ⋖ a ⊔ b
-- Mathlib.Data.PNat.Factors
instIsOrderedCancelAddMonoidPrimeMultiset : IsOrderedCancelAddMonoid PrimeMultiset
-- Mathlib.CategoryTheory.Join.Opposites
_private.Mathlib.CategoryTheory.Join.Opposites.0.CategoryTheory.Join.opEquiv.match_5.eq_2 : ∀ (C : Type u_4) (D : Type u_3) [inst : CategoryTheory.Category.{u_2, u_4} C]
  [inst_1 : CategoryTheory.Category.{u_1, u_3} D] (motive : CategoryTheory.Join Dᵒᵖ Cᵒᵖ → Sort u_5) (a : Cᵒᵖ)
  (h_1 : (a : Dᵒᵖ) → motive (CategoryTheory.Join.left a)) (h_2 : (a : Cᵒᵖ) → motive (CategoryTheory.Join.right a)),
  (match CategoryTheory.Join.right a with
    | CategoryTheory.Join.left a => h_1 a
    | CategoryTheory.Join.right a => h_2 a) =
    h_2 a
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.Quotient.full_functor : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (r : HomRel C), (CategoryTheory.Quotient.functor r).Full
-- Mathlib.Topology.Algebra.StarSubalgebra
StarSubalgebra.topologicalClosure_toSubalgebra_comm : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : TopologicalSpace A]
  [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : StarRing A] [inst_6 : StarModule R A]
  [inst_7 : IsSemitopologicalSemiring A] [inst_8 : ContinuousStar A] (s : StarSubalgebra R A),
  s.topologicalClosure.toSubalgebra = s.topologicalClosure
-- Init.Data.UInt.Lemmas
UInt64.toUInt32_ofNatClamp_of_lt : ∀ {n : ℕ}, n < UInt64.size → (UInt64.ofNatClamp n).toUInt32 = UInt32.ofNat n
-- Aesop.Tree.Data.ForwardRuleMatches
/-- Get the unsafe rules corresponding to the unsafe rule matches.  -/
Aesop.ForwardRuleMatches.unsafeRules : Aesop.ForwardRuleMatches → Array Aesop.UnsafeRule
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
aemeasurable_const : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {b : β}, AEMeasurable (fun _a => b) μ
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
/-- Two algebra morphisms are equal on `Algebra.span s` iff they are equal on `s`.  -/
AlgHom.eqOn_adjoin_iff : ∀ {R : Type uR} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] {φ ψ : A →ₐ[R] B} {s : Set A},
  Set.EqOn ⇑φ ⇑ψ ↑(Algebra.adjoin R s) ↔ Set.EqOn (⇑φ) (⇑ψ) s
-- Init.Data.BitVec.Basic
/-- Flatten a list of bitvectors into one bitvector.

This is `noncomputable` so that the only compiled implementation is the
divide-and-conquer `BitVec.flattenListFast`, installed via `@[csimp]`; see there
for the cost analysis.
 -/
BitVec.flattenList : {n : ℕ} → (xs : List (BitVec n)) → BitVec (n * xs.length)
-- Init.Data.List.Nat.Range
List.zipIdx_eq_append_iff : ∀ {α : Type u_1} {l₁ l₂ : List (α × ℕ)} {l : List α} {k : ℕ},
  l.zipIdx k = l₁ ++ l₂ ↔ ∃ l₁' l₂', l = l₁' ++ l₂' ∧ l₁ = l₁'.zipIdx k ∧ l₂ = l₂'.zipIdx (k + l₁'.length)
-- Mathlib.Combinatorics.Pigeonhole
/-- The strong pigeonhole principle for finitely many pigeons and pigeonholes.  Given a function `f`
between finite types `α` and `β` and a number `n` such that `card β * n ≤ card α`, there exists an
element `y : β` such that its preimage has at least `n` elements. See also
`Fintype.exists_lt_card_fiber_of_mul_lt_card` for a stronger statement.  -/
Fintype.exists_le_card_fiber_of_mul_le_card : ∀ {α : Type u} {β : Type v} [inst : DecidableEq β] [inst_1 : Fintype α] [inst_2 : Fintype β] (f : α → β) {n : ℕ}
  [Nonempty β], Fintype.card β * n ≤ Fintype.card α → ∃ y, n ≤ {x | f x = y}.card
-- Mathlib.Data.Nat.Cast.SetInterval
Nat.image_cast_int_Ici : ∀ (a : ℕ), Nat.cast '' Set.Ici a = Set.Ici ↑a
-- Mathlib.Algebra.Star.Unitary
Unitary.coe_div : ∀ {R : Type u_1} [inst : GroupWithZero R] [inst_1 : StarMul R] (U₁ U₂ : ↥(unitary R)), ↑(U₁ / U₂) = ↑U₁ / ↑U₂
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Expr.toPolyS.match_1.congr_eq_1 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (a : Lean.Grind.CommRing.Expr)
  (h_1 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.num n))
  (h_2 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_3 : (x : Lean.Grind.CommRing.Expr) → motive x) (n : ℤ),
  a = Lean.Grind.CommRing.Expr.num n →
    (match a with
      | Lean.Grind.CommRing.Expr.num n => h_1 n
      | Lean.Grind.CommRing.Expr.var x => h_2 x
      | x => h_3 x) ≍
      h_1 n
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
/-- The inclusion `Δ[1] ⟶ Λ[2, 1]` which avoids `2`.  -/
SSet.horn₂₁.ι₀₁ : SSet.stdSimplex.obj { len := 1 } ⟶ (SSet.horn 2 1).toSSet
-- Mathlib.Topology.Order.Monotone
AntitoneOn.tendsto_nhdsWithin_Ioo_left : ∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : ConditionallyCompleteLinearOrder β] [inst_4 : TopologicalSpace β] [OrderTopology β] {f : α → β} {x y : α},
  (Set.Ioo y x).Nonempty →
    AntitoneOn f (Set.Ioo y x) →
      BddBelow (f '' Set.Ioo y x) → Filter.Tendsto f (nhdsWithin x (Set.Iio x)) (nhds (sInf (f '' Set.Ioo y x)))
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.IsPresentation.of_linearEquiv : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] {solution : relations.Solution M},
  solution.IsPresentation →
    ∀ {N : Type v'} [inst_3 : AddCommGroup N] [inst_4 : Module A N] (e : M ≃ₗ[A] N),
      (solution.postcomp ↑e).IsPresentation
-- Mathlib.Order.Partition.Basic
/-- The function maps related elements to the same representative.  -/
Partition.IsRepFun.apply_eq_apply : ∀ {α : Type u_1} {u : Set α} {P : Partition u} {f : α → α}, P.IsRepFun f → ∀ ⦃a b : α⦄, P.Rel a b → f a = f b
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.IsHomogeneous.degree_eq_sum_deg_support : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] {φ : MvPolynomial σ R} {n : ℕ},
  φ.IsHomogeneous n → ∀ {s : σ →₀ ℕ}, s ∈ φ.support → n = ∑ i ∈ s.support, s i
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.instIsScalarTower : ∀ (R' : Type u) (M : Type v) [inst : CommSemiring R'] [inst_1 : AddCommMonoid M] [inst_2 : Module R' M]
  [inst_3 : Module R'ᵐᵒᵖ M] [inst_4 : IsCentralScalar R' M], IsScalarTower R' (TrivSqZeroExt R' M) R'
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.instEpiNegHom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {P Q : C} {f : P ⟶ Q}
  [CategoryTheory.Epi f], CategoryTheory.Epi (-f)
-- Mathlib.Analysis.SpecialFunctions.CompareExp
Complex.IsExpCmpFilter.tendsto_abs_re : ∀ {l : Filter ℂ}, Complex.IsExpCmpFilter l → Filter.Tendsto (fun z => |z.re|) l Filter.atTop
-- Lean.Parser.Basic
Lean.Parser.hexNumberFn : String.Pos.Raw → optParam Bool true → optParam Lean.SyntaxNodeKind Lean.numLitKind → Lean.Parser.ParserFn
-- Mathlib.Dynamics.Ergodic.Conservative
MeasureTheory.Conservative.inter_frequently_image_mem_ae_eq : ∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → α} {s : Set α} {μ : MeasureTheory.Measure α},
  MeasureTheory.Conservative f μ →
    MeasureTheory.NullMeasurableSet s μ → s ∩ {x | ∃ᶠ (n : ℕ) in Filter.atTop, f^[n] x ∈ s} =ᵐ[μ] s
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.indep_iff_not_dep : ∀ {α : Type u_1} {M : Matroid α} {I : Set α}, M.Indep I ↔ ¬M.Dep I ∧ I ⊆ M.E
-- Mathlib.Order.Disjoint
Codisjoint.mono_left : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderTop α] {a b c : α}, b ≤ a → Codisjoint b c → Codisjoint a c
-- Lean.Elab.Tactic.Doc
Lean.Elab.Tactic.Doc.TacticDoc.mk : Lean.Name → String → Lean.NameSet → Option String → Array String → Lean.Elab.Tactic.Doc.TacticDoc
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.ext_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : Add β]
  {f g : α ≃+o β}, f = g ↔ ∀ (a : α), f a = g a
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.instIsEquivalenceLeftExtensionCompPrecomp : ∀ {C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C'] [inst_2 : CategoryTheory.Category.{v_3, u_3} H]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H)
  (G : CategoryTheory.Functor C' C) [G.IsEquivalence],
  (CategoryTheory.Functor.LeftExtension.precomp L F G).IsEquivalence
-- Mathlib.Order.Minimal
image_monotone_setOfPred_maximal : ∀ {α : Type u_2} {β : Type u_3} {P : α → Prop} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  (∀ ⦃y x : α⦄, P y → P x → (f y ≤ f x ↔ y ≤ x)) →
    f '' {x | Maximal P x} = {x | Maximal (fun x => ∃ x₀, P x₀ ∧ f x₀ = x) x}
-- Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
/-- This has to come after `WeakDual.CharacterSpace.instFunLike`, otherwise the right-hand side
gets coerced via `Subtype.val` instead of directly via `DFunLike`.  -/
WeakDual.CharacterSpace.coe_coe : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : ContinuousAdd 𝕜]
  [inst_3 : ContinuousConstSMul 𝕜 𝕜] [inst_4 : NonUnitalNonAssocSemiring A] [inst_5 : TopologicalSpace A]
  [inst_6 : Module 𝕜 A] (φ : ↑(WeakDual.characterSpace 𝕜 A)), ⇑↑φ = ⇑φ
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
StarOrderedRing.isStrictlyPositive_iff_spectrum_pos : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [ContinuousSqrt R]
  [StarOrderedRing R] [inst_8 : TopologicalSpace A] [inst_9 : Ring A] [inst_10 : StarRing A] [inst_11 : PartialOrder A]
  [StarOrderedRing A] [inst_13 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] [NonnegSpectrumClass R A]
  (a : A),
  autoParam (p a) StarOrderedRing.isStrictlyPositive_iff_spectrum_pos._auto_1 →
    (IsStrictlyPositive a ↔ ∀ x ∈ spectrum R a, 0 < x)
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.basis_apply : ∀ {ι : Type u_3} {s : Set (ι → ℕ)} (hs : IsProperLinearSet s) [inst : Finite ι] (i : ↑(IsProperLinearSet.basisSet✝ hs)),
  (IsProperLinearSet.basis✝ hs) i = toRatVec✝ ↑i
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.exp_log : ∀ {x : ℝ}, 0 < x → Real.exp (Real.log x) = x
-- Mathlib.Algebra.Order.Sub.Defs
le_tsub_add_add : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b c : α}
  [AddLeftMono α], a + b ≤ a - c + (b + c)
-- Init.Data.SInt.Lemmas
Int8.ofIntLE_le_iff_le : ∀ {a b : ℤ} (ha₁ : Int8.minValue.toInt ≤ a) (ha₂ : a ≤ Int8.maxValue.toInt) (hb₁ : Int8.minValue.toInt ≤ b)
  (hb₂ : b ≤ Int8.maxValue.toInt), Int8.ofIntLE a ha₁ ha₂ ≤ Int8.ofIntLE b hb₁ hb₂ ↔ a ≤ b
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The Hausdorff distance is nonnegative.  -/
Metric.hausdorffDist_nonneg : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s t : Set α}, 0 ≤ Metric.hausdorffDist s t
-- Mathlib.GroupTheory.GroupAction.Period
AddAction.period_dvd_exponent : ∀ {α : Type v} {M : Type u} [inst : AddMonoid M] [inst_1 : AddAction M α] (m : M) (a : α),
  AddAction.period m a ∣ AddMonoid.exponent M
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.eq_top_iff : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K), A = ⊤ ↔ ¬A.valuation.IsNontrivial
-- Mathlib.MeasureTheory.Measure.Haar.Basic
TopologicalSpace.Compacts.mk.congr_simp : ∀ {α : Type u_4} [inst : TopologicalSpace α] (carrier carrier_1 : Set α) (e_carrier : carrier = carrier_1)
  (isCompact' : IsCompact carrier),
  { carrier := carrier, isCompact' := isCompact' } = { carrier := carrier_1, isCompact' := ⋯ }
-- Mathlib.Topology.Constructible
Topology.IsConstructible.isLocallyConstructible : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s : Set X}, Topology.IsConstructible s → Topology.IsLocallyConstructible s
-- Mathlib.Topology.ContinuousMap.Ideals
ContinuousMap.idealOf_compl_singleton_isMaximal : ∀ {X : Type u_1} (𝕜 : Type u_2) [inst : RCLike 𝕜] [inst_1 : TopologicalSpace X] [CompactSpace X] [T2Space X] (x : X),
  (ContinuousMap.idealOfSet 𝕜 {x}ᶜ).IsMaximal
-- Mathlib.Order.Bounds.Basic
IsCofinalFor.of_subset : ∀ {α : Type u_1} [inst : Preorder α] {s t : Set α}, s ⊆ t → IsCofinalFor s t
-- Batteries.Data.List.Count
List.injective_sigmaCountToIdx : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {xs : List α}, Function.Injective xs.sigmaCountToIdx
-- Mathlib.Data.Vector.Defs
List.Vector.append_def : ∀ {α : Type u_1} {n m : ℕ},
  HAppend.hAppend = fun x x_1 =>
    match x, x_1 with
    | ⟨l₁, h₁⟩, ⟨l₂, h₂⟩ => ⟨l₁ ++ l₂, ⋯⟩
-- Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
/-- If `μ x = 0`, then `smoothingFun μ x` is the limit of `smoothingSeminormSeq μ x`.  -/
tendsto_smoothingFun_of_eq_zero : ∀ {R : Type u_1} [inst : CommRing R] (μ : RingSeminorm R) {x : R},
  μ x = 0 → Filter.Tendsto (smoothingSeminormSeq μ x) Filter.atTop (nhds (smoothingFun μ x))
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.ones.eq_1 : ∀ (n : ℕ), Composition.ones n = { blocks := List.replicate n 1, blocks_pos := ⋯, blocks_sum := ⋯ }
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.core.injEq : ∀ (a b : Lean.Expr) (p₁ p₂ : Int.Internal.Linear.Poly) (a_1 b_1 : Lean.Expr) (p₁_1 p₂_1 : Int.Internal.Linear.Poly),
  (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.core a b p₁ p₂ =
      Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.core a_1 b_1 p₁_1 p₂_1) =
    (a = a_1 ∧ b = b_1 ∧ p₁ = p₁_1 ∧ p₂ = p₂_1)
-- Mathlib.CategoryTheory.Abelian.ShortExact
CategoryTheory.ShortExact.reflects_shortExact_of_faithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.PreservesZeroMorphisms] [F.Faithful] {S : CategoryTheory.ShortComplex C},
  (S.map F).ShortExact → S.ShortExact
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.lift.congr_simp : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h h_1 : IsAdjoinRoot S f),
  h = h_1 →
    ∀ {T : Type u_1} [inst_3 : CommRing T] (i i_1 : R →+* T) (e_i : i = i_1) (x x_1 : T) (e_x : x = x_1)
      (hx : Polynomial.eval₂ i x f = 0), h.lift i x hx = h_1.lift i_1 x_1 ⋯
-- Std.Async.Signal
Std.Async.instBEqSignal.beq : Std.Async.Signal → Std.Async.Signal → Bool
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey?_eq_some_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {km : α},
  t.maxKey? = some km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
IsBoundedBilinearMap.symm : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : Semiring 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : Module 𝕜 F] [inst_5 : SeminormedAddCommGroup G]
  [inst_6 : Module 𝕜 G] {f : E × F → G}, IsBoundedBilinearMap 𝕜 f → IsBoundedBilinearMap 𝕜 fun p => f (p.2, p.1)
-- Mathlib.Analysis.Fourier.FourierTransform
Fourier.fourierIntegral_def : ∀ {𝕜 : Type u_1} [inst : CommRing 𝕜] [inst_1 : MeasurableSpace 𝕜] {E : Type u_2} [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace ℂ E] (e : AddChar 𝕜 Circle) (μ : MeasureTheory.Measure 𝕜) (f : 𝕜 → E) (w : 𝕜),
  Fourier.fourierIntegral e μ f w = ∫ (v : 𝕜), e (-(v * w)) • f v ∂μ
-- Mathlib.Topology.Instances.Matrix
isClosed_setOfPred_blockTriangular : ∀ {m : Type u_4} {R : Type u_8} [inst : TopologicalSpace R] {α : Type u_11} {b : m → α} [inst_1 : LinearOrder α]
  [inst_2 : Zero R] [T2Space R], IsClosed {M | M.BlockTriangular b}
-- Init.Data.Range.Polymorphic.PRange
/-- Every element of the intersection is an element of both original ranges.
   -/
Std.Rcc.LawfulRcoIntersection.mem_intersection_iff : ∀ {α : Type w} {inst : LT α} {inst_1 : LE α} {inst_2 : Std.Rcc.HasRcoIntersection α}
  [self : Std.Rcc.LawfulRcoIntersection α] {a : α} {r : Std.Rcc α} {s : Std.Rco α},
  a ∈ Std.Rcc.HasRcoIntersection.intersection r s ↔ a ∈ r ∧ a ∈ s
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.Internal.optionPelim' : {α : Type u_1} → (t : Option α) → {β : Sort u_2} → (t = none → β) → ((val : α) → t = some val → β) → β
-- Mathlib.Algebra.Star.SelfAdjoint
/-- An element of a star monoid is normal if it commutes with its adjoint.  -/
IsStarNormal : {R : Type u_1} → [Mul R] → [Star R] → R → Prop
-- Mathlib.Logic.Encodable.Basic
/-- Constructive choice function for a decidable subtype of an encodable type.  -/
Encodable.chooseX : {α : Type u_1} → {p : α → Prop} → [Encodable α] → [DecidablePred p] → (∃ x, p x) → { a // p a }
-- Mathlib.RingTheory.WittVector.TeichmullerSeries
WittVector.sum_coeff_eq_coeff_sum : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {R : Type u_1} [inst : CommRing R] {α : Type u_2} {S : Finset α}
  (x : α → WittVector p R),
  (∀ (n : ℕ), Subsingleton ↑{r | r ∈ S ∧ (x r).coeff n ≠ 0}) →
    ∀ (n : ℕ), (∑ s ∈ S, x s).coeff n = ∑ s ∈ S, (x s).coeff n
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.getEntryLE?_eq_findRev? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] {t : Std.DTreeMap.Internal.Impl α β},
  t.Ordered →
    ∀ {k : α},
      Std.DTreeMap.Internal.Impl.getEntryLE? k t = List.findRev? (fun e => (compare e.fst k).isLE) t.toListModel
-- Mathlib.Topology.UniformSpace.Cauchy
totallyBounded_singleton : ∀ {α : Type u} [uniformSpace : UniformSpace α] (a : α), TotallyBounded {a}
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.t'_fst_fst_snd : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g]
  (i j k : 𝒰.I₀),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j k)
          (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j i))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pullback.fst
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f j) f) g) (𝒰.f j))
            (𝒰.f k))
          (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (𝒰.f j) f) g))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j)
        (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i k))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) (𝒰.f i))
          (𝒰.f j))
        (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g))
-- Std.Time.Time.HourMarker
Std.Time.instDecidableEqHourMarker : DecidableEq Std.Time.HourMarker
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get?_eq_some_get! : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  [inst_2 : Inhabited α] {a : α}, a ∈ m → m.get? a = some (m.get! a)
-- Mathlib.Topology.Algebra.Group.Quotient
QuotientGroup.instContinuousConstSMul : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [SeparatelyContinuousMul G] {N : Subgroup G},
  ContinuousConstSMul G (G ⧸ N)
-- Mathlib.Order.Interval.Set.Basic
Set.Ioc_subset_Ioc : ∀ {α : Type u_1} [inst : Preorder α] {a₁ a₂ b₁ b₂ : α}, b₂ ≤ b₁ → a₁ ≤ a₂ → Set.Ioc b₁ a₁ ⊆ Set.Ioc b₂ a₂
-- Lean.Parser.Tactic
/-- `match` performs case analysis on one or more expressions.
See [Induction and Recursion][tpil4].
The syntax for the `match` tactic is the same as term-mode `match`, except that
the match arms are tactics instead of expressions.
```
example (n : Nat) : n = n := by
  match n with
  | 0 => rfl
  | i+1 => simp
```

[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html
 -/
Lean.Parser.Tactic.match : Lean.Parser.Parser
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.emptyWithCapacity : {α : Type u} → {β : α → Type v} → optParam ℕ 8 → Std.DHashMap.Internal.Raw₀ α β
-- Init.Data.UInt.Lemmas
UInt16.ofNatLT_sub : ∀ {a b : ℕ} (ha : a < 2 ^ 16) (hab : b ≤ a), UInt16.ofNatLT (a - b) ⋯ = UInt16.ofNatLT a ha - UInt16.ofNatLT b ⋯
-- Mathlib.Combinatorics.Enumerative.Stirling
Nat.stirlingFirst.eq_1 : Nat.stirlingFirst 0 0 = 1
-- Mathlib.RingTheory.Adjoin.Basic
/-- If `A` is spanned over `R` by `s`, then the algebra spanned over `A` by `t` is the equal to the
algebra spanned over `R` by `s ∪ t`.
 -/
Algebra.adjoin_eq_adjoin_union : ∀ (R : Type uR) {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  [inst_3 : CommSemiring B] [inst_4 : Algebra R B] [inst_5 : Algebra A B] [inst_6 : IsScalarTower R A B] (s : Set A)
  (t : Set B),
  Algebra.adjoin R s = ⊤ →
    Subalgebra.restrictScalars R (Algebra.adjoin A t) = Algebra.adjoin R (⇑(algebraMap A B) '' s ∪ t)