mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
/-- Returns none if the given array contains complementary literals  -/
Std.Tactic.BVDecide.LRAT.Internal.Clause.ofArray : {α : outParam (Type u)} →
  {β : Type v} → [self : Std.Tactic.BVDecide.LRAT.Internal.Clause α β] → Array (Std.Sat.Literal α) → Option β
-- Lean.Parser.Basic
/-- Recover from errors in `parser` using `handler` to consume input until a known-good state has appeared.
If `handler` fails itself, then no recovery is performed.

`handler` is provided with information about the failing parser's effects , and it is run in the
state immediately after the failure.

The interactions between <|> and `recover'` are subtle, especially for syntactic
categories that admit user extension. Consider avoiding it in these cases.  -/
Lean.Parser.recover' : Lean.Parser.Parser → (Lean.Parser.RecoveryContext → Lean.Parser.Parser) → Lean.Parser.Parser
-- Mathlib.Analysis.Convex.SimplicialComplex.Basic
Geometry.SimplicialComplex.vertex_mem_convexHull_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] {K : Geometry.SimplicialComplex 𝕜 E} {s : Finset E} {x : E},
  x ∈ K.vertices → s ∈ K.faces → (x ∈ (convexHull 𝕜) ↑s ↔ x ∈ s)
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LEquiv.mk.injEq : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} (toLHom : L →ᴸ L') (invLHom : L' →ᴸ L)
  (left_inv : invLHom.comp toLHom = FirstOrder.Language.LHom.id L)
  (right_inv : toLHom.comp invLHom = FirstOrder.Language.LHom.id L') (toLHom_1 : L →ᴸ L') (invLHom_1 : L' →ᴸ L)
  (left_inv_1 : invLHom_1.comp toLHom_1 = FirstOrder.Language.LHom.id L)
  (right_inv_1 : toLHom_1.comp invLHom_1 = FirstOrder.Language.LHom.id L'),
  ({ toLHom := toLHom, invLHom := invLHom, left_inv := left_inv, right_inv := right_inv } =
      { toLHom := toLHom_1, invLHom := invLHom_1, left_inv := left_inv_1, right_inv := right_inv_1 }) =
    (toLHom = toLHom_1 ∧ invLHom = invLHom_1)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKeyD_ofList_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List (α × β)} {k k' fallback : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
      k ∈ List.map Prod.fst l → (Std.TreeMap.Raw.ofList l cmp).getKeyD k' fallback = k
-- Init.Data.Array.Lemmas
Array.getElem_eq_getElem?_get : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} (h : i < xs.size), xs[i] = xs[i]?.get ⋯
-- Mathlib.Algebra.GroupWithZero.Defs
CommGroupWithZero.mk : {G₀ : Type u_2} →
  [toCommMonoidWithZero : CommMonoidWithZero G₀] →
    [toInv : Inv G₀] →
      [toDiv : Div G₀] →
        [toZPow : ZPow G₀] →
          autoParam (∀ (a b : G₀), a / b = a * b⁻¹) DivInvMonoid.div_eq_mul_inv._autoParam →
            autoParam (∀ (a : G₀), a ^ 0 = 1) DivInvMonoid.zpow_zero'._autoParam →
              autoParam (∀ (n : ℕ) (a : G₀), a ^ ↑n.succ = a ^ ↑n * a) DivInvMonoid.zpow_succ'._autoParam →
                autoParam (∀ (n : ℕ) (a : G₀), a ^ Int.negSucc n = (a ^ ↑n.succ)⁻¹) DivInvMonoid.zpow_neg'._autoParam →
                  [toNontrivial : Nontrivial G₀] → 0⁻¹ = 0 → (∀ (a : G₀), a ≠ 0 → a * a⁻¹ = 1) → CommGroupWithZero G₀
-- Mathlib.Algebra.Polynomial.Taylor
Polynomial.coeff_taylor_natDegree : ∀ {R : Type u_1} [inst : Semiring R] (r : R) (f : Polynomial R),
  ((Polynomial.taylor r) f).coeff f.natDegree = f.leadingCoeff
-- Mathlib.Order.BooleanAlgebra.Defs
Bool.instBooleanAlgebra : BooleanAlgebra Bool
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- In a category in which every monomorphism is regular, we can express every monomorphism as
an equalizer. This is not an instance because it would create an instance loop.  -/
CategoryTheory.regularMonoOfMono : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      [CategoryTheory.IsRegularMonoCategory C] → (f : X ⟶ Y) → [CategoryTheory.Mono f] → CategoryTheory.RegularMono f
-- Mathlib.FieldTheory.IsPerfectClosure
IsPerfectClosure.equiv_comp_equiv : ∀ {K : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing K] [inst_1 : CommRing L]
  [inst_2 : CommRing M] [inst_3 : CommRing N] (i : K →+* L) (j : K →+* M) (k : K →+* N) (p : ℕ) [inst_4 : ExpChar M p]
  [inst_5 : ExpChar K p] [inst_6 : ExpChar L p] [inst_7 : PerfectRing L p] [inst_8 : IsPerfectClosure i p]
  [inst_9 : PerfectRing M p] [inst_10 : IsPerfectClosure j p] [inst_11 : ExpChar N p] [inst_12 : PerfectRing N p]
  [inst_13 : IsPerfectClosure k p],
  (IsPerfectClosure.equiv i j p).trans (IsPerfectClosure.equiv j k p) = IsPerfectClosure.equiv i k p
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.small_Ico : ∀ (a b : Ordinal.{u}), Small.{u, u + 1} ↑(Set.Ico a b)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceFunctor_obj_left : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T)
  (G : CategoryTheory.Functor D T) (c : C) (X : CategoryTheory.CostructuredArrow (CategoryTheory.Comma.fst F G) c),
  ((CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceFunctor F G c).obj X).left = CategoryTheory.Over.mk X.hom
-- Mathlib.CategoryTheory.Limits.Chosen.End
/-- The data of chosen coends in `C`.  -/
CategoryTheory.Limits.ChosenCoends : (C : Type u_1) →
  [CategoryTheory.Category.{v_1, u_1} C] → Type (max (max (max (max (max (max (u + 1) (v + 1)) u) u_1) v_1) u) v)
-- Mathlib.Topology.Algebra.Monoid
AddMonoidHom.isClosed_range_coe : ∀ (M₁ : Type u_6) (M₂ : Type u_7) [inst : TopologicalSpace M₂] [T2Space M₂] [inst_2 : AddZeroClass M₁]
  [inst_3 : AddZeroClass M₂] [ContinuousAdd M₂], IsClosed (Set.range DFunLike.coe)
-- Lean.Data.Lsp.Client
Lean.Lsp.instToJsonRegistration : Lean.ToJson Lean.Lsp.Registration
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.sSup_def : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E]
  (S : Set (IntermediateField F E)), sSup S = IntermediateField.adjoin F (⋃₀ (SetLike.coe '' S))
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddLocalization.induction_on : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {p : AddLocalization S → Prop} (x : AddLocalization S),
  (∀ (y : M × ↥S), p (AddLocalization.mk y.1 y.2)) → p x
-- Mathlib.RingTheory.Nilpotent.Basic
IsNilpotent.isUnit_add_left_of_commute : ∀ {R : Type u_1} [inst : Ring R] {r u : R}, IsNilpotent r → IsUnit u → Commute r u → IsUnit (u + r)
-- Mathlib.CategoryTheory.Yoneda
/-- The co-Yoneda embedding, as a functor from `Cᵒᵖ` into co-presheaves on `C`.
 -/
CategoryTheory.coyoneda : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Functor Cᵒᵖ (CategoryTheory.Functor C (Type v₁))
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.size_roc : ∀ {a b : ℕ}, (a<...=b).size = b - a
-- Lean.Elab.Tactic.Omega.Core
/-- `tidy`, implemented on `Fact`.  -/
Lean.Elab.Tactic.Omega.Fact.tidy : Lean.Elab.Tactic.Omega.Fact → Lean.Elab.Tactic.Omega.Fact
-- Std.Http.Protocol.H1.Event
Std.Http.Protocol.H1.Event.endHeaders.inj : ∀ {dir : Std.Http.Protocol.H1.Direction} {head head_1 : Std.Http.Protocol.H1.Message.Head dir},
  Std.Http.Protocol.H1.Event.endHeaders head = Std.Http.Protocol.H1.Event.endHeaders head_1 → head = head_1
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
/-- The `trajContent` is sigma-subadditive.  -/
ProbabilityTheory.Kernel.isSigmaSubadditive_trajContent : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  (κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1)))
  [inst_1 : ∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] {a : ℕ} (x₀ : (i : ↥(Finset.Iic a)) → X ↑i),
  (ProbabilityTheory.Kernel.trajContent κ x₀).IsSigmaSubadditive
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.right_homologyIso_eq_left_homologyIso_trans_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.HomologyData) [inst_2 : S.HasHomology],
  h.right.homologyIso = h.left.homologyIso ≪≫ h.iso
-- Mathlib.Algebra.Module.LinearMap.Basic
/-- The map `Sum.elim` specialised with zero in the second argument, as a linear map.  -/
Sum.elimZeroRight : {ι : Type u_6} → {κ : Type u_7} → {R : Type u_8} → [inst : Semiring R] → (ι → R) →ₗ[R] ι ⊕ κ → R
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.unreach.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {type type_1 : Lean.Expr},
  Lean.Compiler.LCNF.Code.unreach type = Lean.Compiler.LCNF.Code.unreach type_1 → type = type_1
-- Mathlib.AlgebraicTopology.DoldKan.PInfty
AlgebraicTopology.DoldKan.QInfty_f_0 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C}, AlgebraicTopology.DoldKan.QInfty.f 0 = 0
-- Mathlib.Analysis.Complex.SqrtDeriv
Complex.differentiableOn_sqrt : DifferentiableOn ℂ Complex.sqrt Complex.slitPlane
-- Lean.Data.SMap
Lean.SMap.fromHashMap : {α : Type u} →
  {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Std.HashMap α β → optParam Bool true → Lean.SMap α β
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKeyD_erase!_eq_iff_not_compare_minKeyD_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k fallback : α},
      (Std.DTreeMap.Internal.Impl.erase! k t).isEmpty = false →
        ((Std.DTreeMap.Internal.Impl.erase! k t).minKeyD fallback = t.minKeyD fallback ↔
          ¬compare k (t.minKeyD fallback) = Ordering.eq)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getD_inter_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k : α} {fallback : β}, k ∉ m₁ → Std.DHashMap.Raw.Const.getD (m₁ ∩ m₂) k fallback = fallback
-- Mathlib.GroupTheory.Finiteness
AddSubmonoid.FG.eq_1 : ∀ {M : Type u_1} [inst : AddMonoid M] (P : AddSubmonoid M), P.FG = ∃ S, AddSubmonoid.closure ↑S = P
-- Std.Sat.AIG.Basic
Std.Sat.AIG.RefVec.hrefs : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {w : ℕ} (self : aig.RefVec w) {i : ℕ}
  (h : i < w), self.refs[i].gate < aig.decls.size
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.isBridge_iff_forall_walk_mem_edges : ∀ {V : Type u} {G : SimpleGraph V} {v w : V}, G.IsBridge s(v, w) ↔ ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
-- Aesop.RulePattern
/-- A partial map from the index set `{0, ..., n-1}` into `{0, ..., k-1}`. If
`argMap[i] = j`, this indicates that when matching against the rule type, the
instantiation `tⱼ` of `yⱼ` should be substituted for `xᵢ`.
 -/
Aesop.RulePattern.argMap : Aesop.RulePattern → Array (Option ℕ)
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.coe_toSubMulAction : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (p : Submodule R M),
  ↑p.toSubMulAction = ↑p
-- Mathlib.Analysis.InnerProductSpace.Calculus
ContDiff.inner : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : NormedSpace ℝ E] {G : Type u_4} [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G] {f g : G → E}
  {n : WithTop ℕ∞}, ContDiff ℝ n f → ContDiff ℝ n g → ContDiff ℝ n fun x => inner 𝕜 (f x) (g x)
-- Lean.Widget.InteractiveDiagnostic
_private.Lean.Widget.InteractiveDiagnostic.0.Lean.Widget.MsgFmtM : Type → Type
-- Mathlib.Data.Nat.BinaryRec
Nat.bit_false_apply : ∀ (n : ℕ), Nat.bit false n = 2 * n
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.shortComplexH1_f : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{max u u_1, u, u} k G),
  (groupCohomology.shortComplexH1 A).f = groupCohomology.d₀₁ A
-- Init.Data.UInt.Bitwise
USize.ofNat_shiftLeft : ∀ (a b : ℕ), b < System.Platform.numBits → USize.ofNat (a <<< b) = USize.ofNat a <<< USize.ofNat b
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.Augmented.toArrow_map_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.SimplicialObject.Augmented C}
  (η : X ⟶ Y),
  (CategoryTheory.SimplicialObject.Augmented.toArrow.map η).left =
    (CategoryTheory.SimplicialObject.Augmented.drop.map η).app (Opposite.op { len := 0 })
-- Std.Net.Addr
/-- Obtain the `IPAddr` contained in a `SocketAddress`.
 -/
Std.Net.SocketAddress.ipAddr : Std.Net.SocketAddress → Std.Net.IPAddr
-- Std.Data.HashSet.Raw
Std.HashSet.Raw.WF.ofList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {l : List α}, (Std.HashSet.Raw.ofList l).WF
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.DefaultConsumers.forIn'.congr_simp : ∀ {m : Type w → Type w'} {α β : Type w} [inst : Std.Iterator α m β] {n : Type x → Type x'} [inst_1 : Monad n]
  (lift lift_1 : (γ : Type w) → (δ : Type x) → (γ → n δ) → m γ → n δ),
  lift = lift_1 →
    ∀ (γ : Type x) (PlausibleForInStep : β → γ → ForInStep γ → Prop) (it it_1 : Std.IterM m β) (e_it : it = it_1)
      (init init_1 : γ),
      init = init_1 →
        ∀ (P : β → Prop) (hP : ∀ (b : β), it.IsPlausibleIndirectOutput b → P b)
          (f f_1 : (b : β) → P b → (c : γ) → n (Subtype (PlausibleForInStep b c))),
          f = f_1 →
            Std.IterM.DefaultConsumers.forIn' lift γ PlausibleForInStep it init P hP f =
              Std.IterM.DefaultConsumers.forIn' lift_1 γ PlausibleForInStep it_1 init_1 P ⋯ f_1
-- Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
/-- If `C` has pullbacks, the category of `1`-hypercovers up to homotopy is cofiltered.  -/
CategoryTheory.GrothendieckTopology.HOneHypercover.isCofiltered_of_hasPullbacks : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {S : C}
  [CategoryTheory.Limits.HasPullbacks C], CategoryTheory.IsCofiltered (J.HOneHypercover S)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Localization.mkHom_apply : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} (x : M × ↥S), Localization.mkHom x = Localization.mk x.1 x.2
-- Mathlib.Algebra.Group.Action.Hom
MulAction.compHom.eq_1 : ∀ {M : Type u_1} {N : Type u_2} (α : Type u_3) [inst : Monoid M] [inst_1 : MulAction M α] [inst_2 : Monoid N]
  (g : N →* M), MulAction.compHom α g = { smul := SMul.comp.smul ⇑g, mul_smul := ⋯, one_smul := ⋯ }
-- Mathlib.Data.Prod.Lex
Prod.Lex.toLex_covBy_toLex_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {a₁ a₂ : α} {b₁ b₂ : β},
  toLex (a₁, b₁) ⋖ toLex (a₂, b₂) ↔ a₁ = a₂ ∧ b₁ ⋖ b₂ ∨ a₁ ⋖ a₂ ∧ IsMax b₁ ∧ IsMin b₂
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
SSet.Truncated.HomotopyCategory.BinaryProduct.right_unitality : ∀ (X Y : SSet.Truncated 2)
  [inst : Unique (Y.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 }))]
  [inst_1 :
    Subsingleton
      (Y.obj (Opposite.op { obj := { len := 1 }, property := SSet.Truncated.HomotopyCategory.isoTerminal._proof_1 }))],
  CategoryTheory.Prod.fst X.HomotopyCategory ↑CategoryTheory.Cat.chosenTerminal =
    ((CategoryTheory.Functor.id X.HomotopyCategory).prod
          (SSet.Truncated.HomotopyCategory.isoTerminal Y).inv.toFunctor).comp
      ((SSet.Truncated.HomotopyCategory.BinaryProduct.inverse X Y).comp
        (SSet.Truncated.mapHomotopyCategory (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y)))
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- The identity costructured arrow is terminal.  -/
CategoryTheory.CostructuredArrow.mkIdTerminal : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {Y : C} →
          {S : CategoryTheory.Functor C D} →
            [S.Full] →
              [S.Faithful] →
                CategoryTheory.Limits.IsTerminal
                  (CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.id (S.obj Y)))
-- Mathlib.Data.Set.Insert
Set.forall_mem_insert : ∀ {α : Type u_1} {P : α → Prop} {a : α} {s : Set α}, (∀ x ∈ insert a s, P x) ↔ P a ∧ ∀ x ∈ s, P x
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
nonpos_of_mul_nonpos_right : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] {a b : R} [PosMulStrictMono R], a * b ≤ 0 → 0 < a → b ≤ 0
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenModifier.deprecated : Lean.Lsp.SemanticTokenModifier
-- Init.MetaTypes
/-- Do reductions of types and propositions. Default: `false`.  -/
Lean.Meta.Command.ReduceConfig.types : Lean.Meta.Command.ReduceConfig → Bool
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
HomogeneousIdeal.instAdd : {ι : Type u_1} →
  {σ : Type u_2} →
    {A : Type u_3} →
      [inst : Semiring A] →
        [inst_1 : DecidableEq ι] →
          [inst_2 : AddMonoid ι] →
            [inst_3 : SetLike σ A] →
              [inst_4 : AddSubmonoidClass σ A] → {𝒜 : ι → σ} → [inst_5 : GradedRing 𝒜] → Add (HomogeneousIdeal 𝒜)
-- Mathlib.Topology.Ultrafilter
/-- `x` belongs to the closure of `s` if and only if some ultrafilter
supported on `s` converges to `x`.  -/
mem_closure_iff_ultrafilter : ∀ {X : Type u} {x : X} {s : Set X} [inst : TopologicalSpace X], x ∈ closure s ↔ ∃ u, s ∈ u ∧ ↑u ≤ nhds x
-- Mathlib.Analysis.Analytic.Order
/-- The set where an analytic function has zero or infinite order is discrete within its domain of
analyticity.  -/
AnalyticOnNhd.codiscrete_setOfPred_analyticOrderAt_eq_zero_or_top : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {U : Set 𝕜} {f : 𝕜 → E},
  AnalyticOnNhd 𝕜 f U → {u | analyticOrderAt f ↑u = 0 ∨ analyticOrderAt f ↑u = ⊤} ∈ Filter.codiscrete ↑U
-- Aesop.Forward.State
/-- Add a hypothesis to the forward state. If `fs` represents a local context
`lctx`, then `fs.addHyp h ms` represents `lctx` with `h` added. `ms` must
overapproximate the rules for which `h` may unify with a maximal premise.  -/
Aesop.ForwardState.enqueueHyp : Lean.FVarId → Array (Aesop.ForwardRule × Aesop.PremiseIndex) → Aesop.ForwardState → Aesop.ForwardState
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem_alter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp] (h : t.WF)
  {k k' : α} {f : Option β → Option β} {hc : k' ∈ t.alter k f},
  (t.alter k f)[k'] = if heq : cmp k k' = Ordering.eq then (f t[k]?).get ⋯ else t[k']
-- Init.Prelude
/-- The `restore` implementation for `Backtrackable PUnit σ`.  -/
EStateM.dummyRestore : {σ : Type u} → σ → PUnit.{u_1} → σ
-- Mathlib.Geometry.Manifold.VectorField.Pullback
instIsManifoldOfNatWithTopENatOfMinSmoothness : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {n : ℕ} [inst_6 : n.AtLeastTwo]
  [IsManifold I (minSmoothness 𝕜 (OfNat.ofNat n)) M], IsManifold I (OfNat.ofNat n) M
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonInlayHintTooltip : Lean.FromJson Lean.Lsp.InlayHintTooltip
-- Mathlib.Algebra.Category.Grp.Ulift
AddGrpCat.uliftFunctorFullyFaithful.eq_1 : AddGrpCat.uliftFunctorFullyFaithful =
  {
    preimage := fun {X Y} f =>
      AddGrpCat.ofHom
        (AddEquiv.ulift.toAddMonoidHom.comp ((AddGrpCat.Hom.hom f).comp AddEquiv.ulift.symm.toAddMonoidHom)),
    map_preimage := @AddGrpCat.uliftFunctorFullyFaithful._proof_1,
    preimage_map := @AddGrpCat.uliftFunctorFullyFaithful._proof_2 }
-- Mathlib.Data.Rel
SetRel.self_subset_preimage : ∀ {α : Type u_1} {R : SetRel α α} [R.IsRefl] (s : Set α), s ⊆ R.preimage s
-- Init.Data.BitVec.Bitblast
BitVec.shiftLeftRec.eq_def : ∀ {w₁ w₂ : ℕ} (x : BitVec w₁) (y : BitVec w₂) (n : ℕ),
  x.shiftLeftRec y n =
    have shiftAmt := y &&& BitVec.twoPow w₂ n;
    match n with
    | 0 => x <<< shiftAmt
    | n.succ => x.shiftLeftRec y n <<< shiftAmt
-- Std.Http.Protocol.H1.Reader
/-- The input is malformed.
 -/
Std.Http.Protocol.H1.Reader.State.failed : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Error → Std.Http.Protocol.H1.Reader.State dir
-- Mathlib.CategoryTheory.Adjunction.Reflective
/-- If `A` is essentially in the image of a reflective functor `i`, then `η_A` is an isomorphism.
This gives that the "witness" for `A` being in the essential image can instead be given as the
reflection of `A`, with the isomorphism as `η_A`.

(For any `B` in the reflective subcategory, we automatically have that `ε_B` is an iso.)
 -/
CategoryTheory.Functor.essImage.unit_isIso : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {i : CategoryTheory.Functor D C} [inst_2 : CategoryTheory.Reflective i] {A : C},
  i.essImage A → CategoryTheory.IsIso ((CategoryTheory.reflectorAdjunction i).unit.app A)
-- Lean.Meta.Sym.AlphaShareCommon
_private.Lean.Meta.Sym.AlphaShareCommon.0.Lean.Meta.Sym.State.set : Lean.Meta.Sym.State✝ → Lean.PHashSet Lean.Meta.Sym.AlphaKey
-- Mathlib.Analysis.Normed.Group.Uniform
CauchySeq.norm_bddAbove : ∀ {G : Type u_4} [inst : SeminormedAddGroup G] {u : ℕ → G}, CauchySeq u → BddAbove (Set.range fun n => ‖u n‖)
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.coeff_mk : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ) (f : ℕ → R), (PowerSeries.coeff n) (PowerSeries.mk f) = f n
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleConfig.getPhaseSpec : {m : Type → Type} → [Monad m] → [Lean.MonadError m] → Aesop.Frontend.RuleConfig → m Aesop.PhaseSpec
-- Init.Data.List.Basic
List.intersperse.eq_1 : ∀ {α : Type u} (sep : α), List.intersperse sep [] = []
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.mk.congr_simp : ∀ (z z_1 : ℂ) (e_z : z = z_1) (hz : ‖z‖ ≤ 1), Complex.UnitClosedDisc.mk z hz = Complex.UnitClosedDisc.mk z_1 ⋯
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.IsSFiniteKernel.swapLeft : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsSFiniteKernel κ],
  ProbabilityTheory.IsSFiniteKernel κ.swapLeft
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Replicate
Std.Tactic.BVDecide.BVExpr.bitblast.blastReplicate.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {newWidth : ℕ} (aig : Std.Sat.AIG α) (w n : ℕ)
  (inner : aig.RefVec w) (h : newWidth = w * n),
  Std.Tactic.BVDecide.BVExpr.bitblast.blastReplicate aig { w := w, n := n, inner := inner, h := h } =
    { aig := aig,
      vec :=
        ⋯ ▸
          Std.Tactic.BVDecide.BVExpr.bitblast.blastReplicate.go n inner 0 ⋯
            (Std.Sat.AIG.RefVec.emptyWithCapacity newWidth) }
-- Mathlib.Probability.Distributions.Poisson.Basic
/-- If a function is integrable with respect to `poissonMeasure r`, then its integral
against this measure is given by its sum weighted by `exp (-r) * r ^ n / n!`.

See `integral_poissonMeasure` for a version where the codomain is finite-dimensional
and does not require the integrability hypothesis.  -/
ProbabilityTheory.integral_poissonMeasure' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {r : NNReal} {f : ℕ → E},
  MeasureTheory.Integrable f (ProbabilityTheory.poissonMeasure r) →
    ∫ (n : ℕ), f n ∂ProbabilityTheory.poissonMeasure r = ∑' (n : ℕ), (Real.exp (-↑r) * ↑r ^ n / ↑n.factorial) • f n
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
mem_powers_of_prime_card : ∀ {G : Type u_2} [inst : Group G] {p : ℕ} [hp : Fact (Nat.Prime p)],
  Nat.card G = p → ∀ {g g' : G}, g ≠ 1 → g' ∈ Submonoid.powers g
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
ZMod.toCircle_natCast : ∀ {N : ℕ} [inst : NeZero N] (j : ℕ), ↑(ZMod.toCircle ↑j) = Complex.exp (2 * ↑Real.pi * Complex.I * ↑j / ↑N)
-- Mathlib.Tactic.Linarith.Datatypes
/-- Replace a hypothesis by a list of hypotheses. These expressions are the proof terms.  -/
Mathlib.Tactic.Linarith.Preprocessor.transform : Mathlib.Tactic.Linarith.Preprocessor → Lean.Expr → Lean.MetaM (List Lean.Expr)