mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.Arrow.mapAugmentedCechConerve_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C}
  [inst_1 : ∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom]
  [inst_2 : ∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout g.left (fun x => g.right) fun x => g.hom] (F : f ⟶ g),
  (CategoryTheory.Arrow.mapAugmentedCechConerve F).left = CategoryTheory.Arrow.Hom.left F
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblenWith_zero_strictMono : ∀ {f : Ordinal.{u} → Ordinal.{u}}, Order.IsNormal f → 0 < f 0 → StrictMono fun x => Ordinal.veblenWith f x 0
-- Mathlib.Computability.TuringMachine.Tape
/-- Given two `BlankRel` lists, there exists (constructively) a common join.  -/
Turing.BlankRel.above : {Γ : Type u_1} →
  [inst : Inhabited Γ] →
    {l₁ l₂ : List Γ} → Turing.BlankRel l₁ l₂ → { l // Turing.BlankExtends l₁ l ∧ Turing.BlankExtends l₂ l }
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instRightCancelSemigroupOfMulOpposite.eq_1 : ∀ {M : Type u_1} [inst : RightCancelSemigroup Mᵐᵒᵖ], DomMulAct.instRightCancelSemigroupOfMulOpposite = inst
-- Mathlib.LinearAlgebra.ExteriorPower.Pairing
exteriorPower.toTensorPower_apply_ιMulti : ∀ (R : Type u_1) {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {n : ℕ}
  (v : Fin n → M),
  (exteriorPower.toTensorPower R M n) ((exteriorPower.ιMulti R n) v) =
    ∑ σ, Equiv.Perm.sign σ • (PiTensorProduct.tprod R) fun i => v (σ i)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_diff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α}, (t₁ \ t₂).getKey! k = if k ∈ t₂ then default else t₁.getKey! k
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
PresheafOfModules.evaluation_preservesColimitsOfSize : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat)
  [CategoryTheory.Limits.HasColimitsOfSize.{v₂, u₂, v, v + 1} AddCommGrpCat] (X : Cᵒᵖ),
  CategoryTheory.Limits.PreservesColimitsOfSize.{v₂, u₂, max u₁ v, v, max (max (max u u₁) (v + 1)) v₁, max u (v + 1)}
    (PresheafOfModules.evaluation R X)
-- Mathlib.Data.Seq.Defs
/-- If `s.get? n = some aₙ` for some value `aₙ`, then there is also some value `aₘ` such
that `s.get? = some aₘ` for `m ≤ n`.
 -/
Stream'.Seq.ge_stable : ∀ {α : Type u} (s : Stream'.Seq α) {aₙ : α} {n m : ℕ}, m ≤ n → s.get? n = some aₙ → ∃ aₘ, s.get? m = some aₘ
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.map_id_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct W X] [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct W Y]
  [inst_3 : CategoryTheory.Limits.HasBinaryCoproduct W Z],
  CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id W) (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id W) f)
      (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id W) g)
-- Mathlib.GroupTheory.IndexNormal
/-- A subgroup of index 2 is normal (does not require finiteness of G)  -/
Subgroup.normal_of_index_eq_two : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.index = 2 → H.Normal
-- Mathlib.Topology.MetricSpace.HausdorffDistance
Metric.infEDist_prod : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (x : α × β) (s : Set α)
  (t : Set β), Metric.infEDist x (s ×ˢ t) = max (Metric.infEDist x.1 s) (Metric.infEDist x.2 t)
-- Mathlib.Data.Finmap
Finmap.mem_lookup_union : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {b : β a} {s₁ s₂ : Finmap β},
  b ∈ Finmap.lookup a (s₁ ∪ s₂) ↔ b ∈ Finmap.lookup a s₁ ∨ a ∉ s₁ ∧ b ∈ Finmap.lookup a s₂
-- Init.Data.List.Nat.Modify
List.getElem_modifyHead_succ : ∀ {α : Type u_1} {l : List α} {f : α → α} {n : ℕ} (h : n + 1 < (List.modifyHead f l).length),
  (List.modifyHead f l)[n + 1] = l[n + 1]
-- Init.Data.Ord.Basic
Ordering.isGE_of_eq_gt : ∀ {o : Ordering}, o = Ordering.gt → o.isGE = true
-- Mathlib.CategoryTheory.Bicategory.Opposites
Bicategory.Opposite.op2_whiskerRight : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f f' : a ⟶ b} {g : b ⟶ c} (η : f ⟶ f'),
  Bicategory.Opposite.op2 (CategoryTheory.Bicategory.whiskerRight η g) =
    CategoryTheory.Bicategory.whiskerLeft g.op (Bicategory.Opposite.op2 η)
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.restrict_eqOn : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : Zero Y] {V : Set X}
  (D : Function.locallyFinsuppWithin U Y) (h : V ⊆ U), Set.EqOn (⇑(D.restrict h)) (⇑D) V
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule
HomogeneousSubmodule.toSubmodule_injective : ∀ {ιA : Type u_1} {ιM : Type u_2} {σA : Type u_3} {σM : Type u_4} {A : Type u_5} {M : Type u_6} [inst : Semiring A]
  [inst_1 : AddCommMonoid M] [inst_2 : Module A M] (𝒜 : ιA → σA) (ℳ : ιM → σM) [inst_3 : DecidableEq ιA]
  [inst_4 : AddMonoid ιA] [inst_5 : SetLike σA A] [inst_6 : AddSubmonoidClass σA A] [inst_7 : GradedRing 𝒜]
  [inst_8 : DecidableEq ιM] [inst_9 : SetLike σM M] [inst_10 : AddSubmonoidClass σM M]
  [inst_11 : DirectSum.Decomposition ℳ] [inst_12 : VAdd ιA ιM] [inst_13 : SetLike.GradedSMul 𝒜 ℳ],
  Function.Injective HomogeneousSubmodule.toSubmodule
-- Mathlib.Analysis.Meromorphic.TrailingCoefficient
/-- If `f₁` and `f₂` have equal order at `x` and if their trailing coefficients do not cancel, then the
trailing coefficient of `f₁ - f₂` at `x` is the sum of the trailing coefficients.
 -/
MeromorphicAt.meromorphicTrailingCoeffAt_fun_sub_eq_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : 𝕜} {f₁ f₂ : 𝕜 → E},
  MeromorphicAt f₁ x →
    MeromorphicAt f₂ x →
      meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x →
        meromorphicTrailingCoeffAt f₁ x - meromorphicTrailingCoeffAt f₂ x ≠ 0 →
          meromorphicTrailingCoeffAt (fun z => f₁ z - f₂ z) x =
            meromorphicTrailingCoeffAt f₁ x - meromorphicTrailingCoeffAt f₂ x
-- Mathlib.Data.Finset.Max
Finset.max'.eq_1 : ∀ {α : Type u_2} [inst : LinearOrder α] (s : Finset α) (H : s.Nonempty), s.max' H = s.sup' H id
-- Mathlib.Combinatorics.Pigeonhole
/-- The strong pigeonhole principle for finitely many pigeons and pigeonholes. There is a pigeonhole
with at least as many pigeons as the ceiling of the average number of pigeons across all
pigeonholes.  -/
Fintype.exists_lt_card_fiber_of_nsmul_lt_card : ∀ {α : Type u} {β : Type v} {M : Type w} [inst : DecidableEq β] [inst_1 : Fintype α] [inst_2 : Fintype β] (f : α → β)
  {b : M} [inst_3 : CommSemiring M] [inst_4 : LinearOrder M] [IsStrictOrderedRing M],
  Fintype.card β • b < ↑(Fintype.card α) → ∃ y, b < ↑{x | f x = y}.card
-- Mathlib.Geometry.RingedSpace.SheafedSpace
AlgebraicGeometry.SheafedSpace.instCreatesColimitsOfShapePresheafedSpaceForgetToPresheafedSpaceOfSmallOfHasLimitsOfShapeOpposite : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : Type w) →
      [inst_1 : CategoryTheory.Category.{w', w} J] →
        [Small.{v, w} J] →
          [CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ C] →
            CategoryTheory.CreatesColimitsOfShape J AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.K'.elim_update_main : ∀ {a b c d a' : List Turing.PartrecToTM2.Γ'},
  Function.update (Turing.PartrecToTM2.K'.elim a b c d) Turing.PartrecToTM2.K'.main a' =
    Turing.PartrecToTM2.K'.elim a' b c d
-- Mathlib.RingTheory.Artinian.Algebra
/-- In an `R`-algebra over an Artinian ring `R`, if an element is integral and
is not a zero divisor, then it is a unit.  -/
IsArtinianRing.isUnit_of_nonZeroDivisor_of_isIntegral' : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [IsArtinianRing R] [inst_2 : Ring A] [inst_3 : Algebra R A]
  [Algebra.IsIntegral R A] {a : A}, a ∈ nonZeroDivisors A → IsUnit a
-- Mathlib.Algebra.Group.Shrink
Shrink.instIsCancelAdd : ∀ {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : Add α] [IsCancelAdd α], IsCancelAdd (Shrink.{v, u_2} α)
-- Mathlib.Algebra.Order.Interval.Basic
Interval.length_sum_le : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedAddMonoid α]
  (f : ι → Interval α) (s : Finset ι), (∑ i ∈ s, f i).length ≤ ∑ i ∈ s, (f i).length
-- Mathlib.Data.Int.AbsoluteValue
AbsoluteValue.map_units_int_smul : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : CommRing S] [inst_2 : LinearOrder S] [IsStrictOrderedRing S]
  (abv : AbsoluteValue R S) (x : ℤˣ) (y : R), abv (x • y) = abv y
-- Mathlib.RingTheory.Filtration
Ideal.Filtration.stable_iff_exists_pow_smul_eq_of_ge : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I : Ideal R}
  {F : I.Filtration M}, F.Stable ↔ ∃ n₀, ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀
-- LeanSearchClient.Syntax
LeanSearchClient.leanSearchCommandImpl : Lean.Elab.Command.CommandElab
-- Mathlib.Algebra.Ring.Defs
/-- Negation is left distributive over multiplication  -/
HasDistribNeg.neg_mul : ∀ {α : Type u_1} {inst : Mul α} [self : HasDistribNeg α] (x y : α), -x * y = -(x * y)
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
CategoryTheory.MorphismProperty.isRightAdjoint_ι_isLocal : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [CategoryTheory.MorphismProperty.IsSmall.{w, v, u} W]
  [CategoryTheory.LocallySmall.{w, v, u} C],
  (∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → CategoryTheory.IsCardinalPresentable X κ ∧ CategoryTheory.IsCardinalPresentable Y κ) →
    ∀ [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v, u} C], W.isLocal.ι.IsRightAdjoint
-- Mathlib.Geometry.Manifold.HasGroupoid
hasGroupoid_inf_iff : ∀ {H : Type u} {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  {G₁ G₂ : StructureGroupoid H}, HasGroupoid M (G₁ ⊓ G₂) ↔ HasGroupoid M G₁ ∧ HasGroupoid M G₂
-- Mathlib.LinearAlgebra.TensorProduct.Graded.External
TensorProduct.gradedComm_tmul_of_zero : ∀ (R : Type u_1) {ι : Type u_2} [inst : CommSemiring ι] [inst_1 : Module ι (Additive ℤˣ)] [inst_2 : DecidableEq ι]
  (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [inst_3 : CommRing R] [inst_4 : (i : ι) → AddCommGroup (𝒜 i)]
  [inst_5 : (i : ι) → AddCommGroup (ℬ i)] [inst_6 : (i : ι) → Module R (𝒜 i)] [inst_7 : (i : ι) → Module R (ℬ i)]
  (a : DirectSum ι fun i => 𝒜 i) (b : ℬ 0),
  (TensorProduct.gradedComm R 𝒜 ℬ) (a ⊗ₜ[R] (DirectSum.lof R ι ℬ 0) b) = (DirectSum.lof R ι ℬ 0) b ⊗ₜ[R] a
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.moduleCatLeftHomologyData_K : ∀ {R : Type u} [inst : Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)),
  S.moduleCatLeftHomologyData.K = ModuleCat.of R ↥(ModuleCat.Hom.hom S.g).ker
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonLeanDidOpenTextDocumentParams : Lean.ToJson Lean.Lsp.LeanDidOpenTextDocumentParams
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Matrix.GeneralLinearGroup.IsParabolic.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (g : GL (Fin 2) R), g.IsParabolic = (↑g).IsParabolic
-- Init.Grind.Module.Basic
Lean.Grind.AddCommGroup.mk : {M : Type u} →
  [toAddCommMonoid : Lean.Grind.AddCommMonoid M] →
    [toNeg : Neg M] →
      [toSub : Sub M] → (∀ (a : M), -a + a = 0) → (∀ (a b : M), a - b = a + -b) → Lean.Grind.AddCommGroup M
-- Mathlib.CategoryTheory.Limits.Types.Equalizers
CategoryTheory.Limits.Types.type_equalizer_iff_unique : ∀ {X Y Z : Type u} (f : X ⟶ Y) {g h : Y ⟶ Z}
  (w : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f h),
  Nonempty (CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι f w)) ↔
    ∀ (y : Y),
      (CategoryTheory.ConcreteCategory.hom g) y = (CategoryTheory.ConcreteCategory.hom h) y →
        ∃! x, (CategoryTheory.ConcreteCategory.hom f) x = y
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
/-- A variant of `iteratedDeriv_fun_const_smul` without differentiability assumption when
the scalar multiplication is by division ring elements.  -/
iteratedDeriv_fun_const_smul_field : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {x : 𝕜} {𝕝 : Type u_4} [inst_3 : DivisionSemiring 𝕝] [inst_4 : Module 𝕝 F]
  [SMulCommClass 𝕜 𝕝 F] [ContinuousConstSMul 𝕝 F] {n : ℕ} (c : 𝕝) (f : 𝕜 → F),
  iteratedDeriv n (fun x => c • f x) x = c • iteratedDeriv n f x
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.decidableMemIncidenceSet : {V : Type u} →
  (G : SimpleGraph V) → [DecidableEq V] → [DecidableRel G.Adj] → (v : V) → DecidablePred fun x => x ∈ G.incidenceSet v
-- Mathlib.Algebra.DirectSum.Internal
DirectSum.coe_of_mul_apply_add : ∀ {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [inst : DecidableEq ι] [inst_1 : Semiring R] [inst_2 : SetLike σ R]
  [inst_3 : AddSubmonoidClass σ R] (A : ι → σ) [inst_4 : AddLeftCancelMonoid ι] [inst_5 : SetLike.GradedMonoid A]
  {i : ι} (r : ↥(A i)) (r' : DirectSum ι fun i => ↥(A i)) (j : ι),
  ↑(((DirectSum.of (fun i => ↥(A i)) i) r * r') (i + j)) = ↑r * ↑(r' j)
-- Mathlib.Order.Birkhoff
Fintype.toOrderBot.congr_simp : ∀ (α : Type u_2) [inst : Fintype α] [inst_1 : Nonempty α] [inst_2 : SemilatticeInf α],
  Fintype.toOrderBot α = Fintype.toOrderBot α
-- Mathlib.Algebra.BigOperators.Group.Finset.Gaps
Finset.sum_intervalGapsWithin_eq_sub_sub_sum : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : AddCommGroup β] (F : Finset (α × α)) {k : ℕ}
  (h : F.card = k) {a b : α} (g : α → β),
  ∑ i ∈ Finset.range (k + 1), (g (F.intervalGapsWithin h a b ↑i).2 - g (F.intervalGapsWithin h a b ↑i).1) =
    g b - g a - ∑ z ∈ F, (g z.2 - g z.1)
-- Mathlib.Topology.Category.CompHausLike.Limits
CompHausLike.HasExplicitPullbacksOfInclusions.hasProp : ∀ {P : TopCat → Prop} {inst : CompHausLike.HasExplicitFiniteCoproducts P}
  [self : CompHausLike.HasExplicitPullbacksOfInclusions P] {X Y Z : CompHausLike P} (f : Z ⟶ X ⨿ Y),
  CompHausLike.HasExplicitPullback CategoryTheory.Limits.coprod.inl f
-- Mathlib.Algebra.Category.Semigrp.Basic
AddMagmaCat.hom_ext_iff : ∀ {M N : AddMagmaCat} {f g : M ⟶ N}, f = g ↔ AddMagmaCat.Hom.hom f = AddMagmaCat.Hom.hom g
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
LinearIndependent.repr_ker : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (hv : LinearIndependent R v), hv.repr.ker = ⊥
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.measurableSet_countableGeneratingSet : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace.CountablyGenerated α] {s : Set α},
  s ∈ MeasurableSpace.countableGeneratingSet α → MeasurableSet s
-- Mathlib.Data.Set.Function
Set.EqOn.surjOn_iff : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f₁ f₂ : α → β},
  Set.EqOn f₁ f₂ s → (Set.SurjOn f₁ s t ↔ Set.SurjOn f₂ s t)
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
MvPolynomial.IsWeightedHomogeneous.pow : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] {φ : MvPolynomial σ R}
  {m : M} {w : σ → M},
  MvPolynomial.IsWeightedHomogeneous w φ m → ∀ (n : ℕ), MvPolynomial.IsWeightedHomogeneous w (φ ^ n) (n • m)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- When the right derivative of a function is nonnegative, then it is automatically integrable.  -/
intervalIntegral.integrableOn_deriv_right_of_nonneg : ∀ {g' g : ℝ → ℝ} {a b : ℝ},
  ContinuousOn g (Set.Icc a b) →
    (∀ x ∈ Set.Ioo a b, HasDerivWithinAt g (g' x) (Set.Ioi x) x) →
      (∀ x ∈ Set.Ioo a b, 0 ≤ g' x) → MeasureTheory.IntegrableOn g' (Set.Ioc a b) MeasureTheory.volume
-- Lean.Meta.Tactic.Simp.Main
Lean.Meta.simpTargetStar : Lean.MVarId →
  Lean.Meta.Simp.Context →
    optParam Lean.Meta.Simp.SimprocsArray #[] →
      optParam (Option Lean.Meta.Simp.Discharge) none →
        optParam Lean.Meta.Simp.Stats { } → Lean.MetaM (Lean.Meta.TacticResultCNM × Lean.Meta.Simp.Stats)
-- Mathlib.Data.Sym.Sym2
/-- Addition as a function from `Sym2`.  -/
Sym2.add : {M : Type u_4} → [AddCommMagma M] → Sym2 M → M
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubMulAction.not_mem_of_mem_ofFixingSubgroup : ∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {s : Set α}
  (x : ↥(SubMulAction.ofFixingSubgroup M s)), ↑x ∉ s
-- Mathlib.Analysis.Complex.Basic
/-- A subset of the circle centered at the origin in `ℂ` of radius `r` is a subset of
the `slitPlane` if it does not contain `-r`.  -/
Complex.subset_slitPlane_iff_of_subset_sphere : ∀ {r : ℝ} {s : Set ℂ}, s ⊆ Metric.sphere 0 r → (s ⊆ Complex.slitPlane ↔ -↑r ∉ s)
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_X_sub_C : ∀ {R : Type u_2} [inst : CommRing R] [Nontrivial R] {ι : Type u_3} (m : MonomialOrder ι) (i : ι) (r : R),
  m.degree (MvPolynomial.X i - MvPolynomial.C r) = fun₀ | i => 1
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
ChartedSpace.LiftPropWithinAt.prop : ∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
  [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
  [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M'] {P : (H → H') → Set H → H → Prop} {f : M → M'}
  {s : Set M} {x : M},
  ChartedSpace.LiftPropWithinAt P f s x →
    P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x)
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
/-- A space is simply connected iff it is path connected, and there is at most one path
up to homotopy between any two points.  -/
simply_connected_iff_paths_homotopic : ∀ {Y : Type u_2} [inst : TopologicalSpace Y],
  SimplyConnectedSpace Y ↔ PathConnectedSpace Y ∧ ∀ (x y : Y), Subsingleton (Path.Homotopic.Quotient x y)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.mk.sizeOf_spec : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {X : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] [inst_4 : SizeOf A] [inst_5 : SizeOf B] [inst_6 : SizeOf C]
  [inst_7 : SizeOf X] (fst : CategoryTheory.Functor X A) (snd : CategoryTheory.Functor X C)
  (iso : fst.comp F ≅ snd.comp G),
  sizeOf { fst := fst, snd := snd, iso := iso } = 1 + sizeOf fst + sizeOf snd + sizeOf iso
-- Aesop.Tree.AddRapp
Aesop.findPathForAssignedMVars : Aesop.UnorderedArraySet Lean.MVarId → Aesop.GoalRef → Aesop.TreeM (Array Aesop.RappRef × Std.HashSet Aesop.GoalId)
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.setAverage_const : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {μ : MeasureTheory.Measure α} [CompleteSpace E] {s : Set α}, μ s ≠ 0 → μ s ≠ ⊤ → ∀ (c : E), ⨍ (x : α) in s, c ∂μ = c
-- Std.Data.ByteSlice
instSliceableByteArrayNatByteSlice_7 : Std.Rio.Sliceable ByteArray ℕ ByteSlice
-- Std.Internal.Parsec.Basic
/-- Peeks at the next element, errors on EOF, does not consume input.
 -/
Std.Internal.Parsec.peek! : {ι elem idx : Type} →
  [inst : DecidableEq idx] →
    [inst_1 : DecidableEq elem] → [Std.Internal.Parsec.Input ι elem idx] → Std.Internal.Parsec ι elem
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.MIntl.mk.inj : ∀ {F : PFunctor.{uA, uB}} {approx : (n : ℕ) → PFunctor.Approx.CofixA F n} {consistent : PFunctor.Approx.AllAgree approx}
  {approx_1 : (n : ℕ) → PFunctor.Approx.CofixA F n} {consistent_1 : PFunctor.Approx.AllAgree approx_1},
  { approx := approx, consistent := consistent } = { approx := approx_1, consistent := consistent_1 } →
    approx = approx_1
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.withBotDegree_monomial : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] (d : σ →₀ ℕ) (c : R)
  [inst_1 : Decidable (c = 0)], m.withBotDegree ((MvPolynomial.monomial d) c) = if c = 0 then ⊥ else ↑d
-- Std.Time.DateTime
/-- Getter for the `TimeZone.Offset` inside of a `DateTime`
 -/
Std.Time.DateTime.offset : Std.Time.DateTime → Std.Time.TimeZone.Offset
-- Mathlib.LinearAlgebra.RootSystem.BaseChange
/-- Restriction of scalars to `ℚ` for a crystallographic root pairing in characteristic zero.  -/
RootPairing.restrictScalarsRat : {ι : Type u_1} →
  {L : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : Field L] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : AddCommGroup N] →
              [inst_3 : Module L M] →
                [inst_4 : Module L N] →
                  (P : RootPairing ι L M N) →
                    [P.IsBalanced] →
                      [inst_6 : CharZero L] →
                        [P.IsCrystallographic] →
                          RootPairing ι ℚ ↥(Submodule.span ℚ (Set.range ⇑P.root))
                            ↥(Submodule.span ℚ (Set.range ⇑P.coroot))
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyGT?.go.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (best : Option α) (a : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.getKeyGT?.go k best a =
    match a with
    | Std.DTreeMap.Internal.Impl.leaf => best
    | Std.DTreeMap.Internal.Impl.inner size ky v l r =>
      match compare k ky with
      | Ordering.lt => Std.DTreeMap.Internal.Impl.getKeyGT?.go k (some ky) l
      | x => Std.DTreeMap.Internal.Impl.getKeyGT?.go k best r
-- Mathlib.Topology.Algebra.Nonarchimedean.Bases
RingSubgroupsBasis.hasBasis_nhds_zero : ∀ {A : Type u_1} {ι : Type u_2} [inst : Ring A] [inst_1 : Nonempty ι] {B : ι → AddSubgroup A}
  (hB : RingSubgroupsBasis B), (nhds 0).HasBasis (fun x => True) fun i => ↑(B i)
-- Mathlib.Data.Rat.Lemmas
Rat.mkRat_add_mkRat_of_den : ∀ (n₁ n₂ : ℤ) {d : ℕ}, d ≠ 0 → mkRat n₁ d + mkRat n₂ d = mkRat (n₁ + n₂) d
-- Mathlib.Data.Seq.Computation
Computation.ret_mem : ∀ {α : Type u} (a : α), a ∈ Computation.pure a
-- Mathlib.Probability.Kernel.Condexp
MeasureTheory.Integrable.integral_norm_condExpKernel : ∀ {Ω : Type u_1} {F : Type u_2} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [inst : StandardBorelSpace Ω]
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] [inst_2 : NormedAddCommGroup F] {f : Ω → F},
  MeasureTheory.Integrable f μ →
    MeasureTheory.Integrable (fun ω => ∫ (y : Ω), ‖f y‖ ∂(ProbabilityTheory.condExpKernel μ m) ω) μ
-- Mathlib.Data.Set.Restrict
Set.surjective_codRestrict : ∀ {α : Type u_1} {ι : Sort u_5} {f : ι → α} {s : Set α} (h : ∀ (x : ι), f x ∈ s),
  Function.Surjective (Set.codRestrict f s h) ↔ Set.range f = s
-- Init.Data.Nat.Lemmas
Nat.div_le_div_of_mul_le_mul : ∀ {d c a b : ℕ}, d ≠ 0 → d ∣ c → a * d ≤ c * b → a / b ≤ c / d
-- Mathlib.RingTheory.Ideal.Maps
Ideal.instIsTwoSidedMapRingHomOfRingHomSurjective : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) [RingHomSurjective f] (I : Ideal R)
  [I.IsTwoSided], (Ideal.map f I).IsTwoSided
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.isKernelCompMono.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f : X ⟶ Y} {c : CategoryTheory.Limits.KernelFork f} (i i_1 : CategoryTheory.Limits.IsLimit c),
  i = i_1 →
    ∀ {Z : C} (g : Y ⟶ Z) [hg : CategoryTheory.Mono g] {h : X ⟶ Z} (hh : h = CategoryTheory.CategoryStruct.comp f g),
      CategoryTheory.Limits.isKernelCompMono i g hh = CategoryTheory.Limits.isKernelCompMono i_1 g hh
-- Init.Data.Array.Lemmas
Array.replicate_one : ∀ {α : Type u_1} {a : α}, Array.replicate 1 a = #[a]
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPFullNames : Lean.Options → Bool
-- Mathlib.Analysis.Complex.OperatorNorm
Complex.imCLM_nnnorm : ‖Complex.imCLM‖₊ = 1