mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.Widget.StringDiagram
/-- The vertical position of the node in the string diagram.  -/
Mathlib.Tactic.Widget.StringDiagram.IdNode.vPos : Mathlib.Tactic.Widget.StringDiagram.IdNode → ℕ
-- Mathlib.RingTheory.Length
Module.length_pi : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_5},
  Module.length R (ι → M) = ENat.card ι * Module.length R M
-- Std.Http.Data.Status
Std.Http.Status.misdirectedRequest.sizeOf_spec : sizeOf Std.Http.Status.misdirectedRequest = 1
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteArchimedeanClass.eq_1 : ∀ (M : Type u_1) [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M],
  FiniteArchimedeanClass M = { A // A ≠ ⊤ }
-- Mathlib.RepresentationTheory.Continuous.TopRep
/-- The unit isomorphism of the equivalence `TopRepIsoActionTop`.  -/
TopRep.toActionFromAction : {k : Type u} →
  {G : Type v} →
    [inst : TopologicalSpace k] →
      [inst_1 : Ring k] →
        [inst_2 : Monoid G] → (X : TopRep k G) → TopRep.fromActionTopModFunc.obj (TopRep.toActionTopModFunc.obj X) ≅ X
-- Mathlib.Algebra.Group.End
Equiv.zsmul_addRight : ∀ {α : Type u_4} [inst : AddGroup α] (a : α) (n : ℤ), Equiv.addRight a ^ n = Equiv.addRight (n • a)
-- Mathlib.Order.CompleteLattice.Basic
iSup_eq_if : ∀ {α : Type u_1} [inst : CompleteLattice α] {p : Prop} [inst_1 : Decidable p] (a : α), ⨆ (_ : p), a = if p then a else ⊥
-- Mathlib.Data.ENat.Basic
/-- **Alias** of `ENat.toNat_le_of_le_natCast`. -/
ENat.toNat_le_of_le_coe : ∀ {m : ℕ∞} {n : ℕ}, m ≤ ↑n → m.toNat ≤ n
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.isUnit_iff_norm_isUnit : ∀ {d : ℤ} (z : ℤ√d), IsUnit z ↔ IsUnit z.norm
-- Init.Data.UInt.Bitwise
UInt64.ofNat_or : ∀ (a b : ℕ), UInt64.ofNat (a ||| b) = UInt64.ofNat a ||| UInt64.ofNat b
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
/-- Given a graph homomorphism, map walks to walks.  -/
SimpleGraph.Walk.map : {V : Type u} →
  {V' : Type v} →
    {G : SimpleGraph V} → {G' : SimpleGraph V'} → (f : G →g G') → {u v : V} → G.Walk u v → G'.Walk (f u) (f v)
-- Mathlib.Probability.Distributions.Geometric
ProbabilityTheory.hasSum_integral_geometricMeasure : ∀ {p : ↑unitInterval} {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℕ → E} [inst_1 : NormedSpace ℝ E]
  [CompleteSpace E],
  p ≠ 0 →
    MeasureTheory.Integrable f (ProbabilityTheory.geometricMeasure p) →
      HasSum (fun n => ((1 - ↑p) ^ n * ↑p) • f n) (∫ (n : ℕ), f n ∂ProbabilityTheory.geometricMeasure p)
-- Mathlib.Algebra.Group.Prod
MulHom.coe_snd : ∀ {M : Type u_3} {N : Type u_4} [inst : Mul M] [inst_1 : Mul N], ⇑(MulHom.snd M N) = Prod.snd
-- Mathlib.Algebra.Order.Ring.StandardPart
/-- The valuation subring of elements in non-negative Archimedean classes, i.e. elements bounded by
some natural number.  -/
ArchimedeanClass.FiniteElement : (K : Type u_1) → [inst : LinearOrder K] → [inst_1 : Field K] → [IsOrderedRing K] → Type u_1
-- Mathlib.Analysis.Normed.Ring.Basic
/-- A non-unital ring homomorphism from a `NonUnitalCommRing` to a `NonUnitalSeminormedCommRing`
induces a `NonUnitalSeminormedCommRing` structure on the domain.

See note [reducible non-instances]  -/
NonUnitalSeminormedCommRing.induced : {F : Type u_5} →
  (R : Type u_6) →
    (S : Type u_7) →
      [inst : FunLike F R S] →
        [inst_1 : NonUnitalCommRing R] →
          [inst_2 : NonUnitalSeminormedCommRing S] → [NonUnitalRingHomClass F R S] → F → NonUnitalSeminormedCommRing R
-- Mathlib.MeasureTheory.Function.Jacobian
MeasureTheory.addHaar_image_le_lintegral_abs_det_fderiv_aux2 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E}
  {f : E → E} {f' : E → E →L[ℝ] E} [inst_3 : MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E)
  [μ.IsAddHaarMeasure],
  MeasurableSet s →
    μ s ≠ ⊤ → (∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) → μ (f '' s) ≤ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ
-- Mathlib.Tactic.Simps.Basic
Simps.ProjectionRule.prefix.inj : ∀ {a : Lean.Name} {a_1 : Lean.Syntax} {a_2 : Lean.Name} {a_3 : Lean.Syntax},
  Simps.ProjectionRule.prefix a a_1 = Simps.ProjectionRule.prefix a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.Algebra.Module.Equiv.Basic
LinearMap.piApply_apply_apply : ∀ {R : Type u_1} {M : Type u_5} {V : M → Type u_9} [inst : CommSemiring R] [inst_1 : (x : M) → AddCommMonoid (V x)]
  [inst_2 : (x : M) → Module R (V x)] (e : (x : M) → V x →ₗ[R] R) (s : (x : M) → V x) (x : M),
  (LinearMap.piApply e) s x = (e x) (s x)
-- Init.Data.List.Sort.Lemmas
_private.Init.Data.List.Sort.Lemmas.0.List.merge.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (xs : List α) (h_1 : (ys : List α) → motive [] ys)
  (h_2 : (xs : List α) → motive xs [])
  (h_3 : (x : α) → (xs : List α) → (y : α) → (ys : List α) → motive (x :: xs) (y :: ys)),
  (xs = [] → False) →
    (match xs, [] with
      | [], ys => h_1 ys
      | xs, [] => h_2 xs
      | x :: xs, y :: ys => h_3 x xs y ys) =
      h_2 xs
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
CategoryTheory.CatEnrichedOrdinary.Hom.base_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat C] {X Y : CategoryTheory.CatEnrichedOrdinary C}
  (f : X ⟶ Y),
  CategoryTheory.CatEnrichedOrdinary.Hom.base (CategoryTheory.CategoryStruct.id f) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.CatEnrichedOrdinary.homEquiv f)
-- Lean.PrettyPrinter.Delaborator.Metavariable
_private.Lean.PrettyPrinter.Delaborator.Metavariable.0.Lean.PrettyPrinter.Delaborator.delabMVarAuxAux : {α : Type} →
  Lean.MVarId → Lean.MetaM α → (Lean.Name → Lean.MetaM α) → (Lean.Name → Lean.MetaM α) → Bool → Bool → Lean.MetaM α
-- Mathlib.RingTheory.DividedPowers.DPMorphism
DividedPowers.DPMorphism.mk.inj : ∀ {A : Type u_3} {B : Type u_4} {inst : CommSemiring A} {inst_1 : CommSemiring B} {I : Ideal A} {J : Ideal B}
  {hI : DividedPowers I} {hJ : DividedPowers J} {toRingHom : A →+* B} {ideal_comp : Ideal.map toRingHom I ≤ J}
  {dpow_comp : ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (toRingHom a) = toRingHom (hI.dpow n a)} {toRingHom_1 : A →+* B}
  {ideal_comp_1 : Ideal.map toRingHom_1 I ≤ J}
  {dpow_comp_1 : ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (toRingHom_1 a) = toRingHom_1 (hI.dpow n a)},
  { toRingHom := toRingHom, ideal_comp := ideal_comp, dpow_comp := dpow_comp } =
      { toRingHom := toRingHom_1, ideal_comp := ideal_comp_1, dpow_comp := dpow_comp_1 } →
    toRingHom = toRingHom_1
-- Mathlib.Data.Set.Basic
Set.union_empty : ∀ {α : Type u} (a : Set α), a ∪ ∅ = a
-- Mathlib.Tactic.Positivity.Basic
/-- Extension for `Int.lcm`.  -/
Mathlib.Meta.Positivity.evalIntLCM : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.CategoryTheory.Abelian.Injective.Dimension
CategoryTheory.hasInjectiveDimensionLT_zero_iff_isZero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] (X : C),
  CategoryTheory.HasInjectiveDimensionLT X 0 ↔ CategoryTheory.Limits.IsZero X
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
/-- Do not use this. Use `le_of_mul_le_mul_right'` instead.  -/
MulRightReflectLE.le_of_mul_le_mul_right' : ∀ {M : Type u_1} {inst : Mul M} {inst_1 : LE M} [self : MulRightReflectLE M] {b a₁ a₂ : M}, a₁ * b ≤ a₂ * b → a₁ ≤ a₂
-- Mathlib.Order.Interval.Finset.Defs
instLocallyFiniteOrderBotSubtypeLeOfDecidableLEOfLocallyFiniteOrder.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] {y : α} [inst_1 : DecidableLE α] [inst_2 : LocallyFiniteOrder α],
  instLocallyFiniteOrderBotSubtypeLeOfDecidableLEOfLocallyFiniteOrder =
    { finsetIio := fun a => Finset.Ico ⟨y, ⋯⟩ a, finsetIic := fun a => Finset.Icc ⟨y, ⋯⟩ a, finset_mem_Iic := ⋯,
      finset_mem_Iio := ⋯ }
-- Mathlib.NumberTheory.PrimeCounting
Nat.primesLE_zero : Nat.primesLE 0 = ∅
-- Mathlib.Algebra.Algebra.Pi
/-- If `ι` has a unique element, then `ι → S` is isomorphic to `S` as an `R`-algebra.  -/
AlgEquiv.funUnique : (R : Type u_3) →
  (ι : Type u_4) →
    [inst : CommSemiring R] →
      (S : Type u_8) → [inst_1 : Semiring S] → [inst_2 : Algebra R S] → [Unique ι] → (ι → S) ≃ₐ[R] S
-- Lean.Meta.Tactic.Grind.Action
Lean.Meta.Grind.Action.notApplicable.eq_1 : ∀ (goal : Lean.Meta.Grind.Goal) (kna x : Lean.Meta.Grind.ActionCont),
  Lean.Meta.Grind.Action.notApplicable goal kna x = kna goal
-- Mathlib.Tactic.Order.CollectFacts
/-- A structure for storing facts about variables.  -/
Mathlib.Tactic.Order.AtomicFact : Type
-- Mathlib.Topology.Sequences
/-- An alternative construction for `FrechetUrysohnSpace`: if sequential convergence implies
convergence, then the space is a Fréchet-Urysohn space.  -/
FrechetUrysohnSpace.of_seq_tendsto_imp_tendsto : ∀ {X : Type u_1} [inst : TopologicalSpace X],
  (∀ (f : X → Prop) (a : X),
      (∀ (u : ℕ → X), Filter.Tendsto u Filter.atTop (nhds a) → Filter.Tendsto (f ∘ u) Filter.atTop (nhds (f a))) →
        ContinuousAt f a) →
    FrechetUrysohnSpace X
-- Mathlib.Probability.Moments.Tilted
/-- The variance of `X` under the tilted measure `μ.tilted (t * X ·)` is the second derivative of
the cumulant-generating function of `X` at `t`.  -/
ProbabilityTheory.variance_tilted_mul : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {t : ℝ},
  t ∈ interior (ProbabilityTheory.integrableExpSet X μ) →
    ProbabilityTheory.variance X (μ.tilted fun x => t * X x) = iteratedDeriv 2 (ProbabilityTheory.cgf X μ) t
-- Mathlib.Algebra.Homology.Monoidal
/-- The associator isomorphism for the tensor product of homological complexes.  -/
HomologicalComplex.associator : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.Preadditive C] →
        [inst_3 : (CategoryTheory.MonoidalCategory.curriedTensor C).Additive] →
          [inst_4 : ∀ (X₁ : C), ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁).Additive] →
            {I : Type u_2} →
              [inst_5 : AddMonoid I] →
                {c : ComplexShape I} →
                  [inst_6 : c.TensorSigns] →
                    [inst_7 : DecidableEq I] →
                      (K₁ K₂ K₃ : HomologicalComplex C c) →
                        [inst_8 : K₁.HasTensor K₂] →
                          [inst_9 : K₂.HasTensor K₃] →
                            [inst_10 : (K₁.tensorObj K₂).HasTensor K₃] →
                              [inst_11 : K₁.HasTensor (K₂.tensorObj K₃)] →
                                [K₁.HasGoodTensor₁₂ K₂ K₃] →
                                  [K₁.HasGoodTensor₂₃ K₂ K₃] →
                                    (K₁.tensorObj K₂).tensorObj K₃ ≅ K₁.tensorObj (K₂.tensorObj K₃)
-- Mathlib.NumberTheory.Real.Irrational
Irrational.of_mul_intCast : ∀ {x : ℝ} (m : ℤ), Irrational (x * ↑m) → Irrational x
-- Mathlib.Data.Fin.SuccPred
/-- `succAbove` is injective at the pivot  -/
Fin.succAbove_left_injective : ∀ {n : ℕ}, Function.Injective Fin.succAbove
-- Mathlib.Data.Set.Card
Set.encard_ne_zero : ∀ {α : Type u_1} {s : Set α}, s.encard ≠ 0 ↔ s.Nonempty
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.isSymm_zero : ∀ {R : Type u_1} {M : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {I : R →+* R},
  LinearMap.IsSymm 0
-- Mathlib.Algebra.Group.Submonoid.Saturation
Submonoid.MulSaturated.eq_1 : ∀ {M : Type u_1} [inst : MulOneClass M] (s : Submonoid M), s.MulSaturated = ∀ ⦃x y : M⦄, x * y ∈ s → x ∈ s ∧ y ∈ s
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PrepathObject.unop_I : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Cᵒᵖ} (P : HomotopicalAlgebra.PrepathObject A),
  P.unop.I = Opposite.unop P.P
-- Mathlib.Analysis.Analytic.Basic
analyticOn_congr : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F} {s : Set E},
  Set.EqOn f g s → (AnalyticOn 𝕜 f s ↔ AnalyticOn 𝕜 g s)
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
Pi.abs_def : ∀ {ι : Type u_2} {α : ι → Type u_3} [inst : (i : ι) → AddGroup (α i)] (f : (i : ι) → α i)
  [inst_1 : (i : ι) → Lattice (α i)], |f| = fun i => |f i|
-- Std.Http.Protocol.H1.Writer
/-- Writing a fixed-length body; `n` is the number of bytes still to be sent.
 -/
Std.Http.Protocol.H1.Writer.State.writingBodyFixed : ℕ → Std.Http.Protocol.H1.Writer.State
-- Init.Grind.AC
Lean.Grind.AC.Seq.erase0.match_1.congr_eq_2 : ∀ (motive : Lean.Grind.AC.Seq → Sort u_1) (s : Lean.Grind.AC.Seq)
  (h_1 : (x : Lean.Grind.AC.Var) → motive (Lean.Grind.AC.Seq.var x))
  (h_2 : (x : Lean.Grind.AC.Var) → (s : Lean.Grind.AC.Seq) → motive (Lean.Grind.AC.Seq.cons x s))
  (x : Lean.Grind.AC.Var) (s_1 : Lean.Grind.AC.Seq),
  s = Lean.Grind.AC.Seq.cons x s_1 →
    (match s with
      | Lean.Grind.AC.Seq.var x => h_1 x
      | Lean.Grind.AC.Seq.cons x s => h_2 x s) ≍
      h_2 x s_1
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
/-- Coercion from `MeasureTheory.FiniteMeasure Ω` to `MeasureTheory.Measure Ω`.  -/
MeasureTheory.FiniteMeasure.toMeasure : {Ω : Type u_1} → [inst : MeasurableSpace Ω] → MeasureTheory.FiniteMeasure Ω → MeasureTheory.Measure Ω
-- Mathlib.Data.Nat.Digits.Defs
/-- The String representation produced by toDigitsCore has the proper length relative to
the number of digits in `n < e` for some base `b`. Since this works with any base,
it can be used for binary, decimal, and hex.  -/
Nat.toDigitsCore_length : ∀ (b f n e : ℕ), 0 < e → n < b ^ e → (b.toDigitsCore f n []).length ≤ e
-- Mathlib.Lean.CoreM
CoreM.withImportModules.unsafe_4 : {α : Type} → Array Lean.Name → Lean.CoreM α → Option Lean.SearchPath → Lean.Options → UInt32 → String → IO α
-- Mathlib.Algebra.Homology.Additive
HomologicalComplex.instAdditiveSingle : ∀ {ι : Type u_1} {c : ComplexShape ι} (W : Type u_5) [inst : CategoryTheory.Category.{v_4, u_5} W]
  [inst_1 : CategoryTheory.Preadditive W] [inst_2 : CategoryTheory.Limits.HasZeroObject W] [inst_3 : DecidableEq ι]
  (j : ι), (HomologicalComplex.single W c j).Additive
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.typein_inj : ∀ {α : Type u} (r : α → α → Prop) [inst : IsWellOrder α r] {a b : α},
  (Ordinal.typein r).toRelEmbedding a = (Ordinal.typein r).toRelEmbedding b ↔ a = b
-- Mathlib.Analysis.Complex.Basic
Complex.zero_notMem_slitPlane : 0 ∉ Complex.slitPlane
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey_union_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} (mem : k ∈ m₂), (m₁ ∪ m₂).getKey k ⋯ = m₂.getKey k mem
-- Mathlib.FieldTheory.IsAlgClosed.Basic
IsAlgClosed.card_aroots_eq_natDegree_of_isUnit_leadingCoeff : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : Field B] [IsAlgClosed B] [inst_3 : Algebra A B]
  {p : Polynomial A}, IsUnit p.leadingCoeff → (p.aroots B).card = p.natDegree
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
padicValNat_mul_pow_right : ∀ {p q : ℕ} [hp : Fact (Nat.Prime p)] [hq : Fact (Nat.Prime q)] (n m : ℕ), q ≠ p → padicValNat q (p ^ n * q ^ m) = m
-- Mathlib.CategoryTheory.Sites.JointlySurjective
CategoryTheory.Presieve.mem_comap_jointlySurjectivePrecoverage_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (F : CategoryTheory.Functor C (Type u)) {X : C}
  {R : CategoryTheory.Presieve X},
  R ∈ (CategoryTheory.Precoverage.comap F CategoryTheory.Types.jointlySurjectivePrecoverage).coverings X ↔
    ∀ (x : F.obj X), ∃ Y f, R f ∧ x ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (F.map f))
-- Mathlib.Topology.Algebra.UniformMulAction
UniformSpace.Completion.instVAdd : (M : Type v) → (X : Type x) → [inst : UniformSpace X] → [VAdd M X] → VAdd M (UniformSpace.Completion X)
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.InitializeResult.mk.sizeOf_spec : ∀ (capabilities : Lean.Lsp.ServerCapabilities) (serverInfo? : Option Lean.Lsp.ServerInfo),
  sizeOf { capabilities := capabilities, serverInfo? := serverInfo? } = 1 + sizeOf capabilities + sizeOf serverInfo?
-- Mathlib.CategoryTheory.Idempotents.Karoubi
/-- The category structure on the karoubi envelope of a category.  -/
CategoryTheory.Idempotents.Karoubi.instCategory : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.Category.{v_1, max u_1 v_1} (CategoryTheory.Idempotents.Karoubi C)
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
OpenPartialHomeomorph.continuousOn_extend : ∀ {𝕜 : 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]
  (f : OpenPartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H}, ContinuousOn (↑(f.extend I)) (f.extend I).source
-- Mathlib.CategoryTheory.Abelian.Pseudoelements
/-- A morphism that is surjective on pseudoelements is an epimorphism.  -/
CategoryTheory.Abelian.Pseudoelement.epi_of_pseudo_surjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q),
  Function.Surjective (CategoryTheory.Abelian.Pseudoelement.pseudoApply f) → CategoryTheory.Epi f
-- Mathlib.Topology.Continuous
ContinuousAt.tendsto : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {x : X},
  ContinuousAt f x → Filter.Tendsto f (nhds x) (nhds (f x))
-- Mathlib.Data.Num.ZNum
ZNum.cast_succ : ∀ {α : Type u_1} [inst : AddGroupWithOne α] (n : ZNum), ↑n.succ = ↑n + 1
-- Mathlib.LinearAlgebra.Projection
LinearMap.IsIdempotentElem.isCompl : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {f : E →ₗ[R] E},
  IsIdempotentElem f → IsCompl f.range f.ker
-- Mathlib.Data.Num.Basic
posNumCoe : {α : Type u_1} → [One α] → [Add α] → CoeHTCT PosNum α
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.instHasWidePushoutsOppositeOfHasWidePullbacks : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasWidePullbacks C],
  CategoryTheory.Limits.HasWidePushouts Cᵒᵖ
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : α → β → Option γ} {k : α}
  {g : k ∈ Std.HashMap.Raw.filterMap f m} (h : m.WF), (Std.HashMap.Raw.filterMap f m)[k] = (f (m.getKey k ⋯) m[k]).get ⋯
-- Mathlib.Topology.TietzeExtension
/-- This theorem is not intended to be used directly because it is rare for a set alone to
satisfy `[TietzeExtension t]`. For example, `Metric.ball` in `ℝ` only satisfies it when
the radius is strictly positive, so finding this as an instance will fail.

Instead, it is intended to be used as a constructor for theorems about sets which *do* satisfy
`[TietzeExtension t]` under some hypotheses.  -/
ContinuousMap.exists_extension_forall_mem : ∀ {X₁ : Type u₁} [inst : TopologicalSpace X₁] {X : Type u} [inst_1 : TopologicalSpace X] [NormalSpace X] {e : X₁ → X}
  (he : Topology.IsClosedEmbedding e) {Y : Type v} [inst_3 : TopologicalSpace Y] (f : C(X₁, Y)) {t : Set Y},
  (∀ (x : X₁), f x ∈ t) →
    ∀ [ht : TietzeExtension ↑t], ∃ g, (∀ (x : X), g x ∈ t) ∧ g.comp { toFun := e, continuous_toFun := ⋯ } = f
-- Mathlib.Analysis.Normed.Group.Quotient
QuotientAddGroup.instNormedAddCommGroup.eq_1 : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] (S : AddSubgroup M) [hS : IsClosed ↑S],
  QuotientAddGroup.instNormedAddCommGroup S =
    { toNorm := QuotientAddGroup.instNorm, toAddCommGroup := QuotientAddGroup.Quotient.addCommGroup S,
      toMetricSpace := MetricSpace.ofT0PseudoMetricSpace (M ⧸ S), dist_eq := ⋯ }
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.Subgraph.IsMatching.iSup : ∀ {V : Type u_1} {G : SimpleGraph V} {ι : Type u_3} {f : ι → G.Subgraph},
  (∀ (i : ι), (f i).IsMatching) → (Pairwise fun i j => Disjoint (f i).support (f j).support) → (⨆ i, f i).IsMatching
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.self_iff_surjective : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_5) [inst_1 : CommRing K] [inst_2 : Algebra R K] [IsFractionRing R K],
  IsFractionRing R R ↔ Function.Surjective ⇑(algebraMap R K)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.instStarMemClass : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : Star A], StarMemClass (NonUnitalStarSubalgebra R A) A
-- Lean.Parser.Term.Basic
Lean.Parser.Term.optEllipsis : Lean.Parser.Parser
-- Std.Sat.AIG.Relabel
Std.Sat.AIG.Decl.relabel_id_map : ∀ {α : Type} (decl : Std.Sat.AIG.Decl α), Std.Sat.AIG.Decl.relabel id decl = decl
-- Mathlib.RepresentationTheory.Tannaka
TannakaDuality.FiniteGroup.ofRightFDRep_hom : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Finite G] [inst_3 : Fintype G] (X : FDRep k G)
  (v : ↑X.V),
  (TannakaDuality.FiniteGroup.ofRightFDRep X v).hom =
    CategoryTheory.InducedCategory.homMk (ModuleCat.ofHom (TannakaDuality.FiniteGroup.sumSMulInv v))
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.rotate'.match_1.eq_3 : ∀ {α : Type u_1} (motive : List α → ℕ → Sort u_2) (a : α) (l : List α) (n : ℕ) (h_1 : (x : ℕ) → motive [] x)
  (h_2 : (l : List α) → motive l 0) (h_3 : (a : α) → (l : List α) → (n : ℕ) → motive (a :: l) n.succ),
  (match a :: l, n.succ with
    | [], x => h_1 x
    | l, 0 => h_2 l
    | a :: l, n.succ => h_3 a l n) =
    h_3 a l n
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_I₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {X : C}
  (S : J.Cover X) (f₁ f₂ : S.Arrow), S.preOneHypercover.I₁ f₁ f₂ = f₁.Relation f₂
-- Mathlib.Analysis.Normed.Module.Dual
NormedSpace.sInter_polar_eq_closedBall : ∀ {𝕜 : Type u_3} {E : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {r : ℝ},
  0 < r → ⋂₀ (StrongDual.polar 𝕜 '' {F | F.Finite ∧ F ⊆ Metric.closedBall 0 r⁻¹}) = Metric.closedBall 0 r
-- Mathlib.RingTheory.HahnSeries.HEval
PowerSeries.heval_C : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : CommRing R] (x : HahnSeries Γ R) (r : R), (PowerSeries.heval x) (PowerSeries.C r) = r • 1
-- Mathlib.Topology.Constructions
Topology.IsOpenEmbedding.inclusion : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X} (hst : s ⊆ t),
  IsOpen (Subtype.val ⁻¹' s) → Topology.IsOpenEmbedding (Set.inclusion hst)
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
CauchySeq.mul_const : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Type u_3} [inst_3 : Preorder ι]
  {u : ι → α} {x : α}, CauchySeq u → CauchySeq fun n => u n * x
-- Mathlib.CategoryTheory.Types.Basic
TypeCat.homEquiv_apply : ∀ {X Y : Type u} (f : X ⟶ Y), TypeCat.homEquiv f = ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.X_mem_nonzeroDivisors : ∀ {R : Type u} [inst : CommSemiring R], Polynomial.X ∈ nonZeroDivisors (Polynomial R)
-- Mathlib.Order.Defs.Unbundled
IsTrans.trans : ∀ {α : Sort u_1} {r : α → α → Prop} [self : IsTrans α r] (a b c : α), r a b → r b c → r a c
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.isPrefixOf.match_1.splitter : {α : Type u_1} →
  (motive : List α → List α → Sort u_2) →
    (x x_1 : List α) →
      ((x : List α) → motive [] x) →
        ((x : List α) → (x = [] → False) → motive x []) →
          ((a : α) → (as : List α) → (b : α) → (bs : List α) → motive (a :: as) (b :: bs)) → motive x x_1
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.mapIso_inverse_map_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T T' : D} {S : CategoryTheory.Functor C D} (i : T ≅ T')
  {Y X : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T')} (f : Y ⟶ X),
  ((CategoryTheory.CostructuredArrow.mapIso i).inverse.map f).left = f.left