mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtTreeSet.Basic
/-- Given a proof that such an element exists, retrieves the smallest element that is
greater than the given element.
 -/
Std.ExtTreeSet.getGT : {α : Type u} →
  {cmp : α → α → Ordering} →
    [inst : Std.TransCmp cmp] → (t : Std.ExtTreeSet α cmp) → (k : α) → (∃ a ∈ t, cmp a k = Ordering.gt) → α
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.IsCycles.exists_cycle_toSubgraph_verts_eq_connectedComponentSupp : ∀ {V : Type u_1} {G : SimpleGraph V} {v : V} [Finite V] {c : G.ConnectedComponent},
  G.IsCycles → v ∈ c.supp → (G.neighborSet v).Nonempty → ∃ p, p.IsCycle ∧ p.toSubgraph.verts = c.supp
-- Mathlib.Algebra.BigOperators.Finprod
finprod_emb_domain' : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : CommMonoid M] {f : α → β},
  Function.Injective f →
    ∀ [inst_1 : DecidablePred fun x => x ∈ Set.range f] (g : α → M),
      (∏ᶠ (b : β), if h : b ∈ Set.range f then g (Classical.choose h) else 1) = ∏ᶠ (a : α), g a
-- Mathlib.RingTheory.AdicCompletion.Functoriality
AdicCompletion.exists_smodEq_pow_smul_top_and_mkQ_eq : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u_3} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {f : M →ₗ[R] N},
  Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f) →
    ∀ {x : M} {n : ℕ} {y : N ⧸ I ^ n • ⊤} {y' : N ⧸ I ^ (n + 1) • ⊤},
      (Submodule.factor ⋯) y' = y →
        (I ^ n • ⊤).mkQ (f x) = y → ∃ x', x ≡ x' [SMOD I ^ n • ⊤] ∧ (I ^ (n + 1) • ⊤).mkQ (f x') = y'
-- Mathlib.Algebra.BigOperators.Finprod
/-- If `s : Set α` and `t : Set β` are finite sets, then summing over `s` commutes with
summing over `t`.  -/
finsum_mem_comm : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] {s : Set α} {t : Set β} (f : α → β → M),
  s.Finite →
    t.Finite → ∑ᶠ (i : α) (_ : i ∈ s) (j : β) (_ : j ∈ t), f i j = ∑ᶠ (j : β) (_ : j ∈ t) (i : α) (_ : i ∈ s), f i j
-- Mathlib.Algebra.Lie.Weights.Chain
LieModule.genWeightSpaceChain_def : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (M : Type u_3)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] (χ₁ χ₂ : L → R) (p q : ℤ),
  LieModule.genWeightSpaceChain M χ₁ χ₂ p q = ⨆ k ∈ Set.Ioo p q, LieModule.genWeightSpace M (k • χ₁ + χ₂)
-- Lean.Linter.UnusedVariables
/-- An `IgnoreFunction` receives:

* a `Syntax.ident` for the unused variable
* a `Syntax.Stack` with the location of this piece of syntax in the command
* The `LinterOptions` set locally to this syntax

and should return `true` to indicate that the lint should be suppressed,
or `false` to proceed with linting as usual (other `IgnoreFunction`s may still
say it is ignored). A variable is only linted if it is unused and no
`IgnoreFunction` returns `true` on this syntax.
 -/
Lean.Linter.IgnoreFunction : Type
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get?_filter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {f : α → Bool} {k : α}, (Std.ExtHashSet.filter f m).get? k = Option.filter f (m.get? k)
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
/-- **Alias** of `OpenPartialHomeomorph.coe_mk`. -/
OpenPartialHomeomorph.mk_coe : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialEquiv X Y)
  (h₁ : ContinuousOn (↑e) e.source) (h₂ : ContinuousOn e.invFun e.target)
  (h₃ : IsOpen { toPartialEquiv := e, continuousOn_toFun := h₁, continuousOn_invFun := h₂ }.source)
  (h₄ : IsOpen { toPartialEquiv := e, continuousOn_toFun := h₁, continuousOn_invFun := h₂ }.target),
  ↑{ toPartialEquiv := e, continuousOn_toFun := h₁, continuousOn_invFun := h₂, open_source := h₃, open_target := h₄ } =
    ↑e
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.instSMulCommClassSpecialLinearGroupForall : ∀ {F : Type u_1} [inst : CommRing F] {ι : Type u_2} [inst_1 : DecidableEq ι] [inst_2 : Fintype ι],
  SMulCommClass (Matrix.SpecialLinearGroup ι F) F (ι → F)
-- Mathlib.Order.InitialSeg
/-- The identity function shows that `≼i` is reflexive  -/
InitialSeg.refl : {α : Type u_1} → (r : α → α → Prop) → InitialSeg r r
-- Mathlib.Order.Heyting.Hom
map_compl : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : HeytingAlgebra α]
  [inst_2 : HeytingAlgebra β] [HeytingHomClass F α β] (f : F) (a : α), f aᶜ = (f a)ᶜ
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getThenInsertIfNew?_snd : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k : α}
  {v : β k}, (m.getThenInsertIfNew? k v).2 = m.insertIfNew k v
-- Mathlib.RingTheory.WittVector.Complete
/-- If `k` is a perfect ring of characteristic `p`, a Witt vector `x : 𝕎 k` falls in ideal generated by
`p` if and only if its zeroth coefficient is `0`.
 -/
WittVector.mem_span_p_iff_coeff_zero_eq_zero : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : CommRing k] [CharP k p] [PerfectRing k p]
  (x : WittVector p k), x ∈ Ideal.span {↑p} ↔ x.coeff 0 = 0
-- Lean.Data.KVMap
Lean.instInhabitedDataValue.default : Lean.DataValue
-- Mathlib.Algebra.Category.ModuleCat.AB
instAB4StarModuleCat : ∀ (R : Type u) [inst : Ring R], CategoryTheory.AB4Star (ModuleCat R)
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.valueGroupEquiv_apply : ∀ {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] {R : Type u_3} [inst_1 : Ring R] (v : Valuation R Γ₀)
  (a : { a // (fun x => x ∈ ↑(MonoidWithZeroHom.ofClass Valued.v).valueGroup) a }),
  (WithVal.valueGroupEquiv v) a = ⟨↑a, ⋯⟩
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.lineMap_apply_one : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
  [inst_3 : AddTorsor V1 P1] (p₀ p₁ : P1), (AffineMap.lineMap p₀ p₁) 1 = p₁
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {f : β k → β k} {he : (t.modify k f).isEmpty = false},
  (t.modify k f).maxKey he = t.maxKey ⋯
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.startsWith_copy : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat]
  [inst_1 : String.Slice.Pattern.Model.PatternModel pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s : String.Slice}, s.copy.startsWith pat = s.startsWith pat
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
le_csSup_of_le : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a b : α}, BddAbove s → b ∈ s → a ≤ b → a ≤ sSup s
-- Init.System.IOError
IO.Error.unsatisfiedConstraints.injEq : ∀ (osCode : UInt32) (details : String) (osCode_1 : UInt32) (details_1 : String),
  (IO.Error.unsatisfiedConstraints osCode details = IO.Error.unsatisfiedConstraints osCode_1 details_1) =
    (osCode = osCode_1 ∧ details = details_1)
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
FormalMultilinearSeries.order_zero : ∀ {𝕜 : Type u} {E : Type v} {F : Type w} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [inst_4 : ContinuousAdd E] [inst_5 : ContinuousConstSMul 𝕜 E] [inst_6 : AddCommMonoid F]
  [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [inst_9 : ContinuousAdd F] [inst_10 : ContinuousConstSMul 𝕜 F],
  FormalMultilinearSeries.order 0 = 0
-- Mathlib.FieldTheory.IsRealClosed.Basic
IsRealClosed.nonneg_iff_isSquare : ∀ {R : Type u} [inst : Field R] [IsRealClosed R] [inst_2 : LinearOrder R] [IsStrictOrderedRing R] {x : R},
  0 ≤ x ↔ IsSquare x
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RiiSlice.instToIterator : {α : Type u} →
  {β : Type v} →
    Std.ToIterator (Std.Slice (Std.DTreeMap.Internal.Const.RiiSliceData α β)) Id
      (Std.Iterators.Types.Map (Std.DTreeMap.Internal.Zipper α fun x => β) Id Id (fun ⦃x⦄ => monadLift) fun b =>
        pure (b.fst, b.snd))
      (α × β)
-- Mathlib.CategoryTheory.Monad.Comonadicity
/-- If `f, g` is an `F`-cosplit pair, then they have an equalizer.  -/
CategoryTheory.Comonad.HasEqualizerOfIsCosplitPair.out : ∀ {C : Type u₁} {D : Type u₂} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.Category.{v₁, u₂} D}
  (F : CategoryTheory.Functor C D) [self : CategoryTheory.Comonad.HasEqualizerOfIsCosplitPair F] {A B : C} (f g : A ⟶ B)
  [F.IsCosplitPair f g], CategoryTheory.Limits.HasEqualizer f g
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.rootSet_zero : ∀ {T : Type w} [inst : CommRing T] (S : Type u_1) [inst_1 : CommRing S] [inst_2 : IsDomain S] [inst_3 : Algebra T S],
  Polynomial.rootSet 0 S = ∅
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.link2.eq_def : ∀ {α : Type u} {β : α → Type v} (l r : Std.DTreeMap.Internal.Impl α β) (hl : l.Balanced) (hr : r.Balanced),
  l.link2 r hl hr =
    match hr' : l, hl with
    | Std.DTreeMap.Internal.Impl.leaf, hl => { impl := r, balanced_impl := ⋯, size_impl := ⋯ }
    | Std.DTreeMap.Internal.Impl.inner szl k' v' l' r', hl =>
      match hr'_1 : r, hr with
      | Std.DTreeMap.Internal.Impl.leaf, hr => { impl := l, balanced_impl := ⋯, size_impl := ⋯ }
      | Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'', hr =>
        if h₁ : Std.DTreeMap.Internal.delta * szl < szr then
          match l.link2 l'' ⋯ ⋯ with
          | { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ } =>
            { impl := Std.DTreeMap.Internal.Impl.balanceLErase k'' v'' ℓ r'' ⋯ ⋯ ⋯, balanced_impl := ⋯, size_impl := ⋯ }
        else
          if h₂ : Std.DTreeMap.Internal.delta * szr < szl then
            match r'.link2 r ⋯ ⋯ with
            | { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ } =>
              { impl := Std.DTreeMap.Internal.Impl.balanceRErase k' v' l' ℓ ⋯ ⋯ ⋯, balanced_impl := ⋯, size_impl := ⋯ }
          else { impl := l.glue r ⋯ ⋯ ⋯, balanced_impl := ⋯, size_impl := ⋯ }
-- Mathlib.LinearAlgebra.Dual.Lemmas
/-- `Submodule.dualAnnihilator` and `Submodule.dualCoannihilator` form a Galois coinsertion.  -/
Subspace.dualAnnihilatorGci : (K : Type u_3) →
  (V : Type u_4) →
    [inst : Field K] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module K V] →
          GaloisCoinsertion (⇑OrderDual.toDual ∘ Submodule.dualAnnihilator)
            (Submodule.dualCoannihilator ∘ ⇑OrderDual.ofDual)
-- Mathlib.Topology.Algebra.Module.FiniteDimension
LinearEquiv.coe_toContinuousLinearEquiv_symm' : ∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E]
  [inst_2 : TopologicalSpace E] [inst_3 : IsTopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] {F : Type w}
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜 F] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F]
  [inst_9 : ContinuousSMul 𝕜 F] [inst_10 : CompleteSpace 𝕜] [inst_11 : T2Space E] [inst_12 : T2Space F]
  [inst_13 : FiniteDimensional 𝕜 E] (e : E ≃ₗ[𝕜] F), ⇑e.toContinuousLinearEquiv.symm = ⇑e.symm
-- Lean.Parser.Types
Lean.Parser.ParserState.mkEOIError : Lean.Parser.ParserState → optParam (List String) [] → Lean.Parser.ParserState
-- Mathlib.Analysis.Complex.Trigonometric
Complex.cos_sq : ∀ (x : ℂ), Complex.cos x ^ 2 = 1 / 2 + Complex.cos (2 * x) / 2
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.iCondIndepSet.condIndep_generateFrom_lt : ∀ {Ω : Type u_1} {ι : Type u_2} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] [inst_2 : Preorder ι] {s : ι → Set Ω},
  (∀ (n : ι), MeasurableSet (s n)) →
    ProbabilityTheory.iCondIndepSet m' hm' s μ →
      ∀ (i : ι),
        ProbabilityTheory.CondIndep m' (MeasurableSpace.generateFrom {s i})
          (MeasurableSpace.generateFrom {t | ∃ j < i, s j = t}) hm' μ
-- Mathlib.RingTheory.Valuation.Basic
/-- An alternate constructor of `AddValuation`, that doesn't reference `Multiplicative Γ₀ᵒᵈ`  -/
AddValuation.of : {R : Type u_3} →
  {Γ₀ : Type u_4} →
    [inst : Ring R] →
      [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀] →
        (f : R → Γ₀) →
          f 0 = ⊤ →
            f 1 = 0 →
              (∀ (x y : R), min (f x) (f y) ≤ f (x + y)) → (∀ (x y : R), f (x * y) = f x + f y) → AddValuation R Γ₀
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_roc_eq_singleton_iff : ∀ {k m n : ℕ}, (m<...=n).toArray = #[k] ↔ n = m + 1 ∧ m + 1 = k
-- Mathlib.Algebra.Star.Rat
NNRat.instStarRing : StarRing ℚ≥0
-- Mathlib.Data.List.Lattice
List.forall_mem_union : ∀ {α : Type u_1} {l₁ l₂ : List α} {p : α → Prop} [inst : DecidableEq α],
  (∀ x ∈ l₁ ∪ l₂, p x) ↔ (∀ x ∈ l₁, p x) ∧ ∀ x ∈ l₂, p x
-- Lean.Elab.BuiltinCommand
Lean.Elab.Command.elabEoi : Lean.Elab.Command.CommandElab
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.IsBasis.contract_isBasis : ∀ {α : Type u_1} {M : Matroid α} {I J X C : Set α},
  M.IsBasis I X → M.IsBasis J C → M.Indep (I \ C ∪ J) → (M.contract C).IsBasis (I \ C) (X \ C)
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.Prepartition.distortion_biUnionTagged : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} [inst : Fintype ι] (π : BoxIntegral.Prepartition I)
  (πi : (J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J),
  (π.biUnionTagged πi).distortion = π.boxes.sup fun J => (πi J).distortion
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Cont.cons₁.injEq : ∀ (a : Turing.ToPartrec.Code) (a_1 : List ℕ) (a_2 : Turing.ToPartrec.Cont) (a_3 : Turing.ToPartrec.Code) (a_4 : List ℕ)
  (a_5 : Turing.ToPartrec.Cont),
  (Turing.ToPartrec.Cont.cons₁ a a_1 a_2 = Turing.ToPartrec.Cont.cons₁ a_3 a_4 a_5) = (a = a_3 ∧ a_1 = a_4 ∧ a_2 = a_5)
-- Mathlib.Algebra.Group.Hom.Basic
/-- Define a morphism of additive groups given a map which respects difference.  -/
AddMonoidHom.ofMapSub : {G : Type u_5} →
  [inst : AddGroup G] →
    {H : Type u_8} → [inst_1 : AddGroup H] → (f : G → H) → (∀ (x y : G), f (x - y) = f x - f y) → G →+ H
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- The canonical morphism `S.homology ⟶ S.opcycles` for a short complex `S` that has homology.  -/
CategoryTheory.ShortComplex.homologyι : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) → [inst_2 : S.HasHomology] → S.homology ⟶ S.opcycles
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.bind₂_C_right : ∀ {σ : Type u_1} {R : Type u_3} {S : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  (f : R →+* MvPolynomial σ S) (r : R), (MvPolynomial.bind₂ f) (MvPolynomial.C r) = f r
-- Lean.Elab.Arg
Lean.Elab.Term.NamedArg.val : Lean.Elab.Term.NamedArg → Lean.Elab.Term.Arg
-- Mathlib.CategoryTheory.Shift.Localization
CategoryTheory.Functor.commShiftOfLocalization_iso_inv_app : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W] {A : Type w} [inst_4 : AddMonoid A]
  [inst_5 : CategoryTheory.HasShift C A] (F : CategoryTheory.Functor C E) (F' : CategoryTheory.Functor D E)
  [inst_6 : CategoryTheory.Localization.Lifting L W F F'] [inst_7 : CategoryTheory.HasShift D A]
  [inst_8 : CategoryTheory.HasShift E A] [inst_9 : L.CommShift A] [inst_10 : F.CommShift A] (a : A) (X : C),
  (CategoryTheory.Functor.commShiftIso F' a).inv.app (L.obj X) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.shiftFunctor E a).map ((CategoryTheory.Localization.Lifting.iso L W F F').hom.app X))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F a).inv.app X)
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.Localization.Lifting.iso L W F F').inv.app ((CategoryTheory.shiftFunctor C a).obj X))
          (F'.map ((CategoryTheory.Functor.commShiftIso L a).hom.app X))))
-- Mathlib.AlgebraicGeometry.Sites.Etale
AlgebraicGeometry.Scheme.instEtaleF : ∀ {S : AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage @AlgebraicGeometry.Etale) S) (i : 𝒰.I₀),
  AlgebraicGeometry.Etale (𝒰.f i)
-- Mathlib.LinearAlgebra.Dimension.Basic
LinearMap.lift_rank_le_of_injective : ∀ {R : Type u} {M : Type v} {M' : Type v'} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (f : M →ₗ[R] M'),
  Function.Injective ⇑f → Cardinal.lift.{v', v} (Module.rank R M) ≤ Cardinal.lift.{v, v'} (Module.rank R M')
-- Mathlib.Analysis.InnerProductSpace.l2Space
HilbertBasis.summable_inner_mul_inner : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] (b : HilbertBasis ι 𝕜 E) (x y : E),
  Summable fun i => inner 𝕜 x (b i) * inner 𝕜 (b i) y
-- Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
/-- For natural numbers `n`, the characteristic function for the poles of `f ^ n` equals `n` times the
characteristic function for the poles of `f`.
 -/
ValueDistribution.characteristic_pow_top : ∀ {f : ℂ → ℂ} {n : ℕ},
  Meromorphic f → ValueDistribution.characteristic (f ^ n) ⊤ = n • ValueDistribution.characteristic f ⊤
-- Init.Data.List.Lemmas
/-- Variant of `replicate_succ` that concatenates `a` to the end of the list.  -/
List.replicate_succ' : ∀ {n : ℕ} {α : Type u_1} {a : α}, List.replicate (n + 1) a = List.replicate n a ++ [a]
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.eraseLead.eq_1 : ∀ {R : Type u_1} [inst : Semiring R] (f : Polynomial R), f.eraseLead = Polynomial.erase f.natDegree f
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
extChartAt_source : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  (I : ModelWithCorners 𝕜 E H) [inst_5 : ChartedSpace H M] (x : M), (extChartAt I x).source = (chartAt H x).source
-- Mathlib.CategoryTheory.Adjunction.Mates
CategoryTheory.conjugateEquiv_symm_comp_assoc : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L₁ L₂ L₃ : CategoryTheory.Functor C D} {R₁ R₂ R₃ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂)
  (adj₃ : L₃ ⊣ R₃) (α : R₁ ⟶ R₂) (β : R₂ ⟶ R₃) {Z : CategoryTheory.Functor C D} (h : L₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.conjugateEquiv adj₂ adj₃).symm β)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.conjugateEquiv adj₁ adj₂).symm α) h) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.conjugateEquiv adj₁ adj₃).symm (CategoryTheory.CategoryStruct.comp α β)) h
-- Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
/-- Any category with pullbacks and terminal object has binary products.  -/
hasBinaryProducts_of_hasTerminal_and_pullbacks : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C]
  [CategoryTheory.Limits.HasPullbacks C], CategoryTheory.Limits.HasBinaryProducts C
-- Mathlib.Algebra.Homology.FullSubcategory
HomologicalComplex.liftFunctorObjectProperty_obj : ∀ {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} D] {ι : Type u_2} {c : ComplexShape ι} {V : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_2, u_3} V] [inst_2 : CategoryTheory.Preadditive V]
  (P : CategoryTheory.ObjectProperty V) (F : CategoryTheory.Functor D (HomologicalComplex V c))
  (hF : ∀ (X : D) (n : ι), P ((F.obj X).X n)) (X : D),
  (HomologicalComplex.liftFunctorObjectProperty P F hF).obj X = HomologicalComplex.liftObjectProperty P (F.obj X) ⋯
-- Mathlib.Algebra.Group.Submonoid.Units
Subgroup.unit_of_mem_ofUnits.eq_1 : ∀ {M : Type u_1} [inst : Monoid M] (S : Subgroup Mˣ) {x : M} (h : x ∈ S.ofUnits),
  S.unit_of_mem_ofUnits h = (Classical.choose h).copy x ⋯ ↑(Classical.choose h)⁻¹ ⋯
-- Mathlib.Analysis.Normed.Group.Ultra
IsUltrametricDist.nnnorm_tsum_le_of_forall_le : ∀ {M : Type u_1} {ι : Type u_2} [inst : SeminormedAddCommGroup M] [IsUltrametricDist M] {f : ι → M} {C : NNReal},
  (∀ (i : ι), ‖f i‖₊ ≤ C) → ‖∑' (i : ι), f i‖₊ ≤ C
-- Mathlib.Topology.Category.CompHausLike.Basic
CompHausLike.toCompHausLike_map : ∀ {P P' : TopCat → Prop} (h : ∀ (X : CompHausLike P), P X.toTop → P' X.toTop) {X Y : CompHausLike P} (f : X ⟶ Y),
  (CompHausLike.toCompHausLike h).map f = CategoryTheory.ConcreteCategory.ofHom (TopCat.Hom.hom f.hom)
-- Mathlib.Algebra.Group.Subsemigroup.Membership
AddSubsemigroup.coe_sSup_of_directed_on : ∀ {M : Type u_2} [inst : Add M] {S : Set (AddSubsemigroup M)},
  DirectedOn (fun x1 x2 => x1 ≤ x2) S → ↑(sSup S) = ⋃ s ∈ S, ↑s
-- Mathlib.Dynamics.Ergodic.MeasurePreserving
MeasureTheory.MeasurePreserving.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μa : MeasureTheory.Measure α} {μb : MeasureTheory.Measure β}
  {μc : MeasureTheory.Measure γ} {g : β → γ} {f : α → β},
  MeasureTheory.MeasurePreserving g μb μc →
    MeasureTheory.MeasurePreserving f μa μb → MeasureTheory.MeasurePreserving (g ∘ f) μa μc
-- Mathlib.Order.Interval.Set.Basic
Set.Ico_toDual : ∀ {α : Type u_1} [inst : Preorder α] {a b : α},
  Set.Ico (OrderDual.toDual a) (OrderDual.toDual b) = ⇑OrderDual.ofDual ⁻¹' Set.Ioc b a
-- Mathlib.Tactic.Sat.FromLRAT
/-- A conjunction of formulas.  -/
Sat.Fmla.and : Sat.Fmla → Sat.Fmla → Sat.Fmla
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_unique_nonempty : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Unique ι] (s : Finset ι) (f : ι → M),
  s.Nonempty → ∑ x ∈ s, f x = f default
-- Init.Data.String.Defs
String.Slice.Pos.le_refl : ∀ {s : String.Slice} (p : s.Pos), p ≤ p
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.compl_mem_iff_notMem : ∀ {α : Type u} {f : Ultrafilter α} {s : Set α}, sᶜ ∈ f ↔ s ∉ f
-- Mathlib.FieldTheory.Finite.GaloisField
/-- Uniqueness of finite fields:
Any two finite fields of the same cardinality are (possibly noncanonically) isomorphic  -/
FiniteField.ringEquivOfCardEq : {K : Type u_1} →
  {K' : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field K'] → [inst_2 : Fintype K] → [inst_3 : Fintype K'] → Fintype.card K = Fintype.card K' → K ≃+* K'
-- Init.Data.Nat.Bitwise.Basic
/-- Bitwise and. Usually accessed via the `&&&` operator.

Each bit of the resulting value is set if the corresponding bit is set in both of the inputs.
 -/
Nat.land : ℕ → ℕ → ℕ
-- Mathlib.Order.ConditionallyCompletePartialOrder.Defs
ConditionallyCompletePartialOrderSup.toPartialOrder : {α : Type u_3} → [self : ConditionallyCompletePartialOrderSup α] → PartialOrder α
-- Init.Data.SInt.Lemmas
Int16.ofInt_eq_iff_bmod_eq_toInt : ∀ (a : ℤ) (b : Int16), Int16.ofInt a = b ↔ a.bmod (2 ^ 16) = b.toInt
-- Mathlib.Combinatorics.Additive.DoublingConst
/-- The difference constant `δₘ[A, B]` of two finsets `A` and `B` in a group is `|A / B| / |A|`.

The notation `δₘ[A, B]` is available in scope `Combinatorics.Additive`.  -/
Finset.divConst : {G : Type u_1} → [Group G] → [DecidableEq G] → Finset G → Finset G → ℚ≥0
-- Mathlib.CategoryTheory.EqToHom
/-- If we (perhaps unintentionally) perform equational rewriting on
the target object of a morphism,
we can replace the resulting `_.mpr f` term by a composition with an `eqToHom`.

It may be advisable to introduce any necessary `eqToHom` morphisms manually,
rather than relying on this lemma firing.
 -/
CategoryTheory.congrArg_mpr_hom_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (p : X ⟶ Y) (q : Z = Y),
  ⋯.mpr p = CategoryTheory.CategoryStruct.comp p (CategoryTheory.eqToHom ⋯)
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.withDensity_rnDeriv_eq_zero_iff_apply_eq_zero : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ η : ProbabilityTheory.Kernel α γ)
  [ProbabilityTheory.IsFiniteKernel κ] [inst : ProbabilityTheory.IsFiniteKernel η] (a : α),
  (η.withDensity (κ.rnDeriv η)) a = 0 ↔ ((η.withDensity (κ.rnDeriv η)) a) (κ.mutuallySingularSetSlice η a)ᶜ = 0