mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.mem_mk' : ∀ {R : Type u} [inst : NonAssocRing R] {s : Set R} {sm : Submonoid R} (hm : ↑sm = s) {sa : AddSubgroup R} (ha : ↑sa = s)
  {x : R}, x ∈ Subring.mk' s sm sa hm ha ↔ x ∈ s
-- Mathlib.Logic.Unique
/-- If the codomain of an injective function is a subsingleton, then the domain
is a subsingleton as well.  -/
Function.Injective.subsingleton : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β}, Function.Injective f → ∀ [Subsingleton β], Subsingleton α
-- Lean.Meta.Basic
Lean.Meta.State.diag : Lean.Meta.State → Lean.Meta.Diagnostics
-- Std.Time.Format.Modifier
/-- `classify` classifies the number of pattern letters into an `OffsetX` format.
 -/
Std.Time.OffsetX.classify : ℕ → Option Std.Time.OffsetX
-- Mathlib.Data.Multiset.ZeroCons
Multiset.eq_zero_of_subset_zero : ∀ {α : Type u_1} {s : Multiset α}, s ⊆ 0 → s = 0
-- Mathlib.Analysis.Convolution
MeasureTheory.AEStronglyMeasurable.convolution_integrand_snd' : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'}
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F]
  (L : E →L[𝕜] E' →L[𝕜] F) [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_8 : AddGroup G]
  [MeasurableAdd G] [MeasurableNeg G],
  MeasureTheory.AEStronglyMeasurable f μ →
    ∀ {x : G},
      MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map (fun t => x - t) μ) →
        MeasureTheory.AEStronglyMeasurable (fun t => (L (f t)) (g (x - t))) μ
-- Mathlib.RingTheory.HahnSeries.HEval
PowerSeries.heval_X : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : CommRing R] (x : HahnSeries Γ R), 0 < x.orderTop → (PowerSeries.heval x) PowerSeries.X = x
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey!_erase_le_maxKey! : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α},
      (Std.Internal.List.eraseKey k l).isEmpty = false →
        (compare (Std.Internal.List.maxKey! (Std.Internal.List.eraseKey k l)) (Std.Internal.List.maxKey! l)).isLE = true
-- Mathlib.RingTheory.WittVector.Defs
WittVector.wittNSMul_vars : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (m n : ℕ), (WittVector.wittNSMul p m n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)
-- Mathlib.Geometry.Euclidean.Angle.Sphere
_private.Mathlib.Geometry.Euclidean.Angle.Sphere.0.Affine.Triangle.termO : Lean.ParserDescr
-- Init.Data.UInt.Lemmas
USize.ofBitVec_pow : ∀ (a : BitVec System.Platform.numBits) (n : ℕ), { toBitVec := a ^ n } = { toBitVec := a } ^ n
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.drop.eq_1 : ∀ {V : Type u} {G : SimpleGraph V} {u : V} (n : ℕ), SimpleGraph.Walk.nil.drop n = SimpleGraph.Walk.nil
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.isMutableLet : Lean.Syntax → Bool
-- Mathlib.RingTheory.Ideal.Operations
Submodule.span_smul_span : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (S : Set R) (T : Set M)
  [(Ideal.span S).IsTwoSided], Ideal.span S • Submodule.span R T = Submodule.span R (S • T)
-- Mathlib.RingTheory.IsTensorProduct
IsTensorProduct.map_comp : ∀ {R : Type u_1} [inst : CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} {N₁ : Type u_6} {N₂ : Type u_7} {N : Type u_8}
  [inst_7 : AddCommMonoid N₁] [inst_8 : AddCommMonoid N₂] [inst_9 : AddCommMonoid N] [inst_10 : Module R N₁]
  [inst_11 : Module R N₂] [inst_12 : Module R N] {g : N₁ →ₗ[R] N₂ →ₗ[R] N} {P₁ : Type u_9} {P₂ : Type u_10}
  {P : Type u_11} [inst_13 : AddCommMonoid P₁] [inst_14 : AddCommMonoid P₂] [inst_15 : AddCommMonoid P]
  [inst_16 : Module R P₁] [inst_17 : Module R P₂] [inst_18 : Module R P] {p : P₁ →ₗ[R] P₂ →ₗ[R] P}
  (hf : IsTensorProduct f) (hg : IsTensorProduct g) (hp : IsTensorProduct p) (i₁ : N₁ →ₗ[R] P₁) (j₁ : M₁ →ₗ[R] N₁)
  (i₂ : N₂ →ₗ[R] P₂) (j₂ : M₂ →ₗ[R] N₂), hf.map hp (i₁ ∘ₗ j₁) (i₂ ∘ₗ j₂) = hg.map hp i₁ i₂ ∘ₗ hf.map hg j₁ j₂
-- Init.Data.UInt.Lemmas
UInt16.zero_le : ∀ {a : UInt16}, 0 ≤ a
-- Mathlib.Data.ENNReal.Basic
ENNReal.coe_max : ∀ (r p : NNReal), ↑(max r p) = max ↑r ↑p
-- Lean.Elab.Tactic.Omega.Core
/-- Constructing the proof term for `addEquality`.  -/
Lean.Elab.Tactic.Omega.Problem.addEquality_proof : ℤ → Lean.Omega.Coeffs → Lean.Elab.Tactic.Omega.Proof → Lean.Elab.Tactic.Omega.Proof
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get?_inter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α}, (t₁ ∩ t₂).get? k = if k ∈ t₂ then t₁.get? k else none
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalSubgroup.instPartialOrder.eq_1 : ∀ {G : Type u} [inst : Group G] [inst_1 : TopologicalSpace G],
  OpenNormalSubgroup.instPartialOrder = PartialOrder.ofSetLike (OpenNormalSubgroup G) G
-- Lean.Meta.Basic
Lean.Meta.State.mk.inj : ∀ {mctx : Lean.MetavarContext} {cache : Lean.Meta.Cache} {zetaDeltaFVarIds : Lean.FVarIdSet}
  {postponed : Lean.PersistentArray Lean.Meta.PostponedEntry} {diag : Lean.Meta.Diagnostics}
  {mctx_1 : Lean.MetavarContext} {cache_1 : Lean.Meta.Cache} {zetaDeltaFVarIds_1 : Lean.FVarIdSet}
  {postponed_1 : Lean.PersistentArray Lean.Meta.PostponedEntry} {diag_1 : Lean.Meta.Diagnostics},
  { mctx := mctx, cache := cache, zetaDeltaFVarIds := zetaDeltaFVarIds, postponed := postponed, diag := diag } =
      { mctx := mctx_1, cache := cache_1, zetaDeltaFVarIds := zetaDeltaFVarIds_1, postponed := postponed_1,
        diag := diag_1 } →
    mctx = mctx_1 ∧ cache = cache_1 ∧ zetaDeltaFVarIds = zetaDeltaFVarIds_1 ∧ postponed = postponed_1 ∧ diag = diag_1
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofMacroExpansionInfo.sizeOf_spec : ∀ (i : Lean.Elab.MacroExpansionInfo), sizeOf (Lean.Elab.Info.ofMacroExpansionInfo i) = 1 + sizeOf i
-- Mathlib.RingTheory.LocalRing.ResidueField.Fiber
instIsLocalRingTensorProductResidueFieldOfIsLocalHomRingHomAlgebraMap : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : IsLocalRing R] [IsLocalRing S] [IsLocalHom (algebraMap R S)],
  IsLocalRing (TensorProduct R (IsLocalRing.ResidueField R) S)
-- Lean.Elab.App
/-- Auxiliary inductive datatype that represents the resolution of an `LVal`.  -/
Lean.Elab.Term.LValResolution : Type
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.add_left_addIndex_le : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] {K : Set G},
  IsCompact K →
    ∀ {V : Set G},
      (interior V).Nonempty →
        ∀ (g : G),
          MeasureTheory.Measure.haar.addIndex ((fun h => g + h) '' K) V ≤ MeasureTheory.Measure.haar.addIndex K V
-- Mathlib.Topology.EMetricSpace.Lipschitz
/-- `f` is Lipschitz iff it is Lipschitz on the entire space.  -/
lipschitzOnWith_univ : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β},
  LipschitzOnWith K f Set.univ ↔ LipschitzWith K f
-- Mathlib.Analysis.Normed.Group.Basic
norm_sub_pos_iff : ∀ {E : Type u_5} [inst : NormedAddGroup E] {a b : E}, 0 < ‖a - b‖ ↔ a ≠ b
-- Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders
MeasureTheory.mem_measurableCylinders_of_mem_closedCompactCylinders : ∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (X i)] {t : Set ((i : ι) → X i)}
  [inst_1 : (i : ι) → MeasurableSpace (X i)] [∀ (i : ι), SecondCountableTopology (X i)]
  [∀ (i : ι), OpensMeasurableSpace (X i)],
  t ∈ MeasureTheory.closedCompactCylinders X → t ∈ MeasureTheory.measurableCylinders X
-- Mathlib.Data.Real.ConjExponents
Real.HolderTriple.right_pos : ∀ {p q r : ℝ}, p.HolderTriple q r → 0 < q
-- Init.Data.BitVec.Lemmas
BitVec.toNat_xor : ∀ {v : ℕ} (x y : BitVec v), (x ^^^ y).toNat = x.toNat ^^^ y.toNat
-- Init.Data.String.Lemmas.Pattern.Pred
_private.Init.Data.String.Lemmas.Pattern.Pred.0.String.Slice.all.eq_1 : ∀ {ρ : Type} (s : String.Slice) (pat : ρ) [inst : String.Slice.Pattern.ForwardPattern pat],
  s.all pat = (s.skipPrefixWhile pat == s.endPos)
-- Init.Data.Array.Attach
Array.map_attachWith : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {P : α → Prop} {H : ∀ a ∈ xs, P a} {f : { x // P x } → β},
  Array.map f (xs.attachWith P H) =
    Array.map
      (fun x =>
        match x with
        | ⟨x, h⟩ => f ⟨x, ⋯⟩)
      xs.attach
-- Std.Time.DateTime.Timestamp
/-- Converts a `Timestamp` to a `Second.Offset`.
 -/
Std.Time.Timestamp.toSecondsSinceUnixEpoch : Std.Time.Timestamp → Std.Time.Second.Offset
-- Mathlib.Topology.UniformSpace.UniformConvergence
/-- An analogue of `Filter.HasBasis.tendsto_right_iff` for `TendstoUniformly`.  -/
Filter.HasBasis.tendstoUniformly_iff_of_uniformity : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace β] {X : Type u_5} {ιβ : Type u_8} {F : X → α → β} {f : α → β}
  {l : Filter X} {pβ : ιβ → Prop} {sβ : ιβ → Set (β × β)},
  (uniformity β).HasBasis pβ sβ →
    (TendstoUniformly F f l ↔ ∀ (i : ιβ), pβ i → ∀ᶠ (n : X) in l, ∀ (x : α), (f x, F n x) ∈ sβ i)
-- Lean.DocString.Parser
/-- Formatter for `ifVerso`—formats according to the underlying formatters.
 -/
Lean.Doc.Parser.ifVerso.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Mathlib.LinearAlgebra.Matrix.Nondegenerate
Matrix.SeparatingLeft.eq_zero_of_vecMul_eq_zero : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : CommSemiring R] {M : Matrix m n R} [inst_1 : Fintype m]
  [inst_2 : Finite n], M.SeparatingLeft → ∀ {v : m → R}, Matrix.vecMul v M = 0 → v = 0
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.constVAddHom_apply : ∀ (k : Type u_1) (P₁ : Type u_2) {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] (v : Multiplicative V₁),
  (AffineEquiv.constVAddHom k P₁) v = AffineEquiv.constVAdd k P₁ (Multiplicative.toAdd v)
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.isWeierstrassDivisionAt_iff : ∀ {A : Type u_1} [inst : CommRing A] (f g q : PowerSeries A) (r : Polynomial A) (I : Ideal A),
  f.IsWeierstrassDivisionAt g q r I ↔
    r.degree < ↑((PowerSeries.map (Ideal.Quotient.mk I)) g).order.toNat ∧ f = g * q + ↑r
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.defn.injEq : ∀ (e : Lean.Expr) (p : Int.Internal.Linear.Poly) (e_1 : Lean.Expr) (p_1 : Int.Internal.Linear.Poly),
  (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.defn e p = Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.defn e_1 p_1) =
    (e = e_1 ∧ p = p_1)
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
/-- The set `A f L r ε` is the set of points `x` around which the function `f` is well approximated
at scale `r` by the linear map `h ↦ h • L`, up to an error `ε`. We tweak the definition to
make sure that this is open on the right.  -/
RightDerivMeasurableAux.A : {F : Type u_1} → [inst : NormedAddCommGroup F] → [NormedSpace ℝ F] → (ℝ → F) → F → ℝ → ℝ → Set ℝ
-- Mathlib.CategoryTheory.Comma.Over.OverClass
CategoryTheory.instIsOverTower : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (S : C) [inst_1 : CategoryTheory.OverClass X S],
  CategoryTheory.IsOverTower X X S
-- Mathlib.Data.Sigma.Basic
PSigma.subtype_ext_iff : ∀ {α : Sort u_1} {β : Sort u_3} {p : α → β → Prop} {x₀ x₁ : (a : α) ×' Subtype (p a)},
  x₀ = x₁ ↔ x₀.fst = x₁.fst ∧ ↑x₀.snd = ↑x₁.snd
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.Const.modify.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (buckets : Array (Std.DHashMap.Internal.AssocList α fun x => β))
  (motive : { u // u.toNat < buckets.size } → Sort u_3) (i : USize) (hi : i.toNat < buckets.size)
  (h_1 : (i : USize) → (hi : i.toNat < buckets.size) → motive ⟨i, hi⟩),
  (match ⟨i, hi⟩ with
    | ⟨i, hi⟩ => h_1 i hi) =
    h_1 i hi
-- Mathlib.Algebra.MvPolynomial.Counit
MvPolynomial.counitNat_surjective : ∀ (A : Type u_1) [inst : CommSemiring A], Function.Surjective ⇑(MvPolynomial.counitNat A)
-- Mathlib.Algebra.Group.Units.Defs
Units.copy.eq_1 : ∀ {α : Type u} [inst : Monoid α] (u : αˣ) (val : α) (hv : val = ↑u) (inv : α) (hi : inv = ↑u⁻¹),
  u.copy val hv inv hi = { val := val, inv := inv, val_inv := ⋯, inv_val := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
/-- The oplax lineator morphism.  -/
CategoryTheory.Functor.OplaxRightLinear.δᵣ : {D : Type u_1} →
  {D' : Type u_2} →
    {inst : CategoryTheory.Category.{v_1, u_1} D} →
      {inst_1 : CategoryTheory.Category.{v_2, u_2} D'} →
        (F : CategoryTheory.Functor D D') →
          {C : Type u_3} →
            {inst_2 : CategoryTheory.Category.{v_3, u_3} C} →
              {inst_3 : CategoryTheory.MonoidalCategory C} →
                {inst_4 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D} →
                  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D'} →
                    [self : F.OplaxRightLinear C] →
                      (d : D) →
                        (c : C) →
                          F.obj (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c) ⟶
                            CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj (F.obj d) c
-- Mathlib.Analysis.Calculus.FDeriv.Const
hasFDerivWithinAt_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] (c : F) (x : E) (s : Set E), HasFDerivWithinAt (fun x => c) 0 s x
-- Mathlib.Probability.Kernel.Defs
/-- Sum of an indexed family of kernels.  -/
ProbabilityTheory.Kernel.sum : {α : Type u_1} →
  {β : Type u_2} →
    {ι : Type u_3} →
      {mα : MeasurableSpace α} →
        {mβ : MeasurableSpace β} → [Countable ι] → (ι → ProbabilityTheory.Kernel α β) → ProbabilityTheory.Kernel α β
-- Mathlib.RingTheory.Jacobson.Artinian
/-- If `A` is a finite type algebra over an Artinian ring `R`,
then `A` is finite over `R` if and only if `dim A = 0`.  -/
Module.finite_iff_krullDimLE_zero : ∀ (R : Type u_1) (A : Type u_2) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Algebra.FiniteType R A] [IsArtinianRing R], Module.Finite R A ↔ Ring.KrullDimLE 0 A
-- Lean.Level
Lean.Level.PP.Context.mk.injEq : ∀ (mvars : Bool) (lIndex? : Lean.LMVarId → Option ℕ) (mvars_1 : Bool) (lIndex?_1 : Lean.LMVarId → Option ℕ),
  ({ mvars := mvars, lIndex? := lIndex? } = { mvars := mvars_1, lIndex? := lIndex?_1 }) =
    (mvars = mvars_1 ∧ lIndex? = lIndex?_1)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.propagateDown : Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Order.Filter.Extr
/-- If `f` is antitone on `Icc a b` and monotone on `Icc b c`, then the minimum of `f` on
`Icc a c` is attained at `b`.  -/
isMinOn_Icc_of_anti_mono : ∀ {α : Type u} {β : Type u_1} [inst : LinearOrder α] [inst_1 : Preorder β] {a b c : α} {f : α → β},
  AntitoneOn f (Set.Icc a b) → MonotoneOn f (Set.Icc b c) → IsMinOn f (Set.Icc a c) b
-- Mathlib.Data.Nat.Factorization.Basic
Nat.ordCompl_le : ∀ (n p : ℕ), n / p ^ n.factorization p ≤ n
-- Mathlib.Data.Set.Function
Set.EqOn.image_eq : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ : α → β}, Set.EqOn f₁ f₂ s → f₁ '' s = f₂ '' s
-- Mathlib.LinearAlgebra.Matrix.Reindex
Matrix.toAddEquiv_reindexAlgEquiv : ∀ {m : Type u_2} {n : Type u_3} (R : Type u_11) (A : Type u_12) [inst : CommSemiring R] [inst_1 : Fintype n]
  [inst_2 : Fintype m] [inst_3 : DecidableEq m] [inst_4 : DecidableEq n] [inst_5 : Semiring A] [inst_6 : Algebra R A]
  (e : m ≃ n), ↑(Matrix.reindexAlgEquiv R A e) = Matrix.reindexAddEquiv A e e
-- Mathlib.NumberTheory.PythagoreanTriples
/-- **Formula for Pythagorean Triples**  -/
PythagoreanTriple.classification : ∀ {x y z : ℤ},
  PythagoreanTriple x y z ↔
    ∃ k m n,
      (x = k * (m ^ 2 - n ^ 2) ∧ y = k * (2 * m * n) ∨ x = k * (2 * m * n) ∧ y = k * (m ^ 2 - n ^ 2)) ∧
        (z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2))
-- Std.Sat.AIG.Basic
/-- An input node to the circuit.
 -/
Std.Sat.AIG.Decl.atom : {α : Type} → α → Std.Sat.AIG.Decl α
-- Mathlib.Topology.Constructions
IsClosed.isClosedEmbedding_subtypeVal : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsClosed s → Topology.IsClosedEmbedding Subtype.val
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.triangleLEGE_obj_mor₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b) (j : C),
  ((t.triangleLEGE a b h).obj j).mor₁ = (t.truncLEι a).app j
-- Mathlib.Order.Sublattice
Sublattice.map_top : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] (f : LatticeHom α β),
  Function.Surjective ⇑f → Sublattice.map f ⊤ = ⊤
-- Mathlib.Analysis.SpecificLimits.Normed
tendsto_pow_atTop_nhds_zero_of_abs_lt_one : ∀ {r : ℝ}, |r| < 1 → Filter.Tendsto (fun n => r ^ n) Filter.atTop (nhds 0)
-- Mathlib.Order.Antisymmetrization
instTransSymmGenLeAntisymmRel : {α : Type u_1} →
  [inst : Preorder α] →
    Trans (Relation.SymmGen fun x1 x2 => x1 ≤ x2) (AntisymmRel fun x1 x2 => x1 ≤ x2)
      (Relation.SymmGen fun x1 x2 => x1 ≤ x2)
-- Init.Data.Function
Function.uncurry_apply_pair : ∀ {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : α → β → γ) (x : α) (y : β), Function.uncurry f (x, y) = f x y
-- Mathlib.Topology.Compactness.Lindelof
lindelofSpace_of_countable_subfamily_closed : ∀ {X : Type u} [inst : TopologicalSpace X],
  (∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed (t i)) → ⋂ i, t i = ∅ → ∃ u, u.Countable ∧ ⋂ i ∈ u, t i = ∅) →
    LindelofSpace X
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Hom.mapEdgeSet.injective : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G'),
  Function.Injective ⇑f → Function.Injective f.mapEdgeSet
-- Mathlib.Analysis.Real.OfDigits
Real.digits.eq_1 : ∀ (x : ℝ) (b : ℕ) [inst : NeZero b] (i : ℕ), x.digits b i = Fin.ofNat b ⌊x * ↑b ^ (i + 1)⌋₊
-- Mathlib.AlgebraicTopology.DoldKan.Equivalence
CategoryTheory.Abelian.DoldKan.comparisonN_hom_app_f : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] [inst_1 : CategoryTheory.Abelian A]
  (X : CategoryTheory.SimplicialObject A) (i : ℕ),
  (CategoryTheory.Abelian.DoldKan.comparisonN.hom.app X).f i =
    CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.Idempotents.toKaroubiEquivalence (ChainComplex A ℕ)).unitIso.hom.app
            (CategoryTheory.Abelian.DoldKan.N.obj X)).f
        i)
      (((CategoryTheory.Idempotents.toKaroubiEquivalence (ChainComplex A ℕ)).inverse.map
            ((AlgebraicTopology.DoldKan.N₁_iso_normalizedMooreComplex_comp_toKaroubi A).inv.app X)).f
        i)
-- Std.Sat.AIG.CNF
/-- The second cache is true at the new index.
 -/
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.Cache.IsExtensionBy.trueAt : ∀ {aig : Std.Sat.AIG ℕ} {cnf1 cnf2 : Std.Sat.CNF ℕ} {cache1 : Std.Sat.AIG.toCNF.Cache✝ aig cnf1}
  {cache2 : Std.Sat.AIG.toCNF.Cache✝ aig cnf2} {new : ℕ} {hnew : new < aig.decls.size},
  Std.Sat.AIG.toCNF.Cache.IsExtensionBy✝ cache1 cache2 new hnew → (Std.Sat.AIG.toCNF.Cache.marks✝ cache2)[new] = true
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.functorPushforward_bot : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (X : C), CategoryTheory.Sieve.functorPushforward F ⊥ = ⊥
-- Mathlib.Analysis.ODE.ExistUnique
/-- There exists only one solution of an ODE $\dot x=v(t, x)$ in a set `s ⊆ ℝ × E` with
a given initial value provided that the RHS is Lipschitz continuous in `x` within `s`,
and we consider only solutions included in `s`.

This version shows uniqueness in a closed interval `Icc a b`, where `a` is the initial time.  -/
ODE_solution_unique_of_mem_Icc_right : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {v : ℝ → E → E} {s : ℝ → Set E} {K : NNReal}
  {f g : ℝ → E} {a b : ℝ},
  (∀ t ∈ Set.Ico a b, LipschitzOnWith K (v t) (s t)) →
    ContinuousOn f (Set.Icc a b) →
      (∀ t ∈ Set.Ico a b, HasDerivWithinAt f (v t (f t)) (Set.Ici t) t) →
        (∀ t ∈ Set.Ico a b, f t ∈ s t) →
          ContinuousOn g (Set.Icc a b) →
            (∀ t ∈ Set.Ico a b, HasDerivWithinAt g (v t (g t)) (Set.Ici t) t) →
              (∀ t ∈ Set.Ico a b, g t ∈ s t) → f a = g a → Set.EqOn f g (Set.Icc a b)
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.hab : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (self : FermatLastTheoremForThreeGen.Solution✝ hζ),
  (hζ.toInteger - 1) ^ 2 ∣
    FermatLastTheoremForThreeGen.Solution'.a✝ (FermatLastTheoremForThreeGen.Solution.toSolution'✝ self) +
      FermatLastTheoremForThreeGen.Solution'.b✝ (FermatLastTheoremForThreeGen.Solution.toSolution'✝ self)
-- Lean.Meta.DiscrTree.Types
Lean.Meta.DiscrTree.Key.hash : Lean.Meta.DiscrTree.Key → UInt64
-- Mathlib.Topology.Order
continuous_coinduced_rng : ∀ {α : Type u} {β : Type v} {f : α → β} {t : TopologicalSpace α}, Continuous f
-- Mathlib.Algebra.Ring.Hom.Defs
RingHom.instInhabited : {α : Type u_2} → {x : NonAssocSemiring α} → Inhabited (α →+* α)
-- Mathlib.CategoryTheory.Triangulated.Opposite.Functor
CategoryTheory.Pretriangulated.Opposite.commShift_adjunction_op_int : ∀ {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] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] {F : CategoryTheory.Functor C D} [inst_4 : F.CommShift ℤ]
  {G : CategoryTheory.Functor D C} [inst_5 : G.CommShift ℤ] (adj : F ⊣ G) [adj.CommShift ℤ], adj.op.CommShift ℤ
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.rfl : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp}, t.Equiv t
-- Mathlib.Topology.Order.LawsonTopology
Topology.lawson_le_scott : ∀ {α : Type u_1} [inst : Preorder α], Topology.lawson α ≤ Topology.scott α Set.univ
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- A fixed block is a block.  -/
AddAction.IsFixedBlock.isBlock : ∀ {G : Type u_1} {X : Type u_2} [inst : VAdd G X] {B : Set X}, AddAction.IsFixedBlock G B → AddAction.IsBlock G B
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.instTransVeqVlt : {R : Type u_1} →
  [inst : Semiring R] → [inst_1 : ValuativeRel R] → Trans ValuativeRel.veq ValuativeRel.vlt ValuativeRel.vlt
-- Mathlib.CategoryTheory.Limits.Types.Limits
CategoryTheory.Limits.Types.hasLimit_iff_small_sections : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)),
  CategoryTheory.Limits.HasLimit F ↔ Small.{u, max u v} ↑F.sections
-- Mathlib.Algebra.DirectSum.Basic
/-- The canonical embedding from `⨁ i, A i` to `M` where `A` is a collection of `AddSubmonoid M`
indexed by `ι`.

When `S = Submodule _ M`, this is available as a `LinearMap`, `DirectSum.coe_linearMap`.  -/
DirectSum.coeAddMonoidHom : {ι : Type v} →
  {M : Type u_1} →
    {S : Type u_2} →
      [DecidableEq ι] →
        [inst : AddCommMonoid M] →
          [inst_1 : SetLike S M] → [inst_2 : AddSubmonoidClass S M] → (A : ι → S) → (DirectSum ι fun i => ↥(A i)) →+ M
-- Init.Omega.IntList
/-- A linear combination of two `IntList`s.  -/
Lean.Omega.IntList.combo : ℤ → Lean.Omega.IntList → ℤ → Lean.Omega.IntList → Lean.Omega.IntList
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.forM_eq_forM_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} {m : Type w → Type w'} [inst : Monad m]
  [LawfulMonad m] {f : α → m PUnit.{w + 1}}, forM t f = Array.forM f t.toArray