mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.pointReflection_self : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P] (x : P),
  (AffineIsometryEquiv.pointReflection 𝕜 x) x = x
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.codisjoint_map : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [inst_3 : AddMonoidHomClass F M N] {f : F},
  Function.Surjective ⇑f →
    ∀ {H K : AddSubmonoid M}, Codisjoint H K → Codisjoint (AddSubmonoid.map f H) (AddSubmonoid.map f K)
-- Init.Data.Nat.Lcm
Nat.le_lcm_right : ∀ {m : ℕ} (n : ℕ), 0 < m → n ≤ m.lcm n
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.EnrichedFunctor.category_id_out : ∀ {V : Type v} [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₁}
  [inst_2 : CategoryTheory.EnrichedCategory V C] {D : Type u₂} [inst_3 : CategoryTheory.EnrichedCategory V D]
  (F : CategoryTheory.EnrichedFunctor V C D),
  (CategoryTheory.CategoryStruct.id F).out = CategoryTheory.CategoryStruct.id F.forget
-- Mathlib.Data.EReal.Operations
/-- See also `EReal.add_lt_add_of_lt_of_le'` for a version with weaker but less convenient
assumptions.  -/
EReal.add_lt_add_of_lt_of_le : ∀ {x y z t : EReal}, x < y → z ≤ t → z ≠ ⊥ → t ≠ ⊤ → x + z < y + t
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.map_dblU : ∀ {F : Type u} {K : Type v} [inst : Field F] [inst_1 : Field K] {W : WeierstrassCurve.Projective F} (f : F →+* K)
  (P : Fin 3 → F), (W.map f).dblU (⇑f ∘ P) = f (W.dblU P)
-- Mathlib.Analysis.Normed.Group.Defs
/-- Construct a normed group from a translation-invariant pseudodistance.  -/
NormedAddGroup.ofAddDist' : {E : Type u_5} →
  [inst : Norm E] →
    [inst_1 : AddGroup E] →
      [inst_2 : MetricSpace E] →
        (∀ (x : E), ‖x‖ = dist 0 x) → (∀ (x y z : E), dist (z + x) (z + y) ≤ dist x y) → NormedAddGroup E
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.constInsertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {t₁ t₂ : Std.DTreeMap.Raw α (fun x => Unit) cmp},
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ (l : List α),
          (Std.DTreeMap.Raw.Const.insertManyIfNewUnit t₁ l).Equiv (Std.DTreeMap.Raw.Const.insertManyIfNewUnit t₂ l)
-- Mathlib.Order.Hom.Basic
OrderIso.bijective : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] (e : α ≃o β), Function.Bijective ⇑e
-- Lean.Meta.Basic
/-- Local context  -/
Lean.Meta.Context.lctx : Lean.Meta.Context → Lean.LocalContext
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.MonoFactorisation.isoComp_m : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  (F : CategoryTheory.Limits.MonoFactorisation f) {X' : C} (g : X' ⟶ X), (F.isoComp g).m = F.m
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.map_normalClosure_le : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (s : Set G) (f : G →* N),
  Subgroup.map f (Subgroup.normalClosure s) ≤ Subgroup.normalClosure (⇑f '' s)
-- Lean.MetavarContext
/-- Modify the local context of a metavariable. If the metavariable is not declared,
nothing happens.

You must ensure that the modification is legal. In particular, expressions may
only be replaced with defeq expressions.
 -/
Lean.MVarId.modifyLCtx : {m : Type → Type} → [Lean.MonadMCtx m] → Lean.MVarId → (Lean.LocalContext → Lean.LocalContext) → m Unit
-- Mathlib.Order.RelClasses
/-- **Alias** of `LT.lt.false`. -/
HasSSubset.SSubset.false : ∀ {α : Type u_2} [inst : Preorder α] {a : α}, a < a → False
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
/-- A zero object is in particular terminal.  -/
CategoryTheory.Limits.HasZeroObject.zeroIsTerminal : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] → CategoryTheory.Limits.IsTerminal 0
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- The symbol `J(a | b)` takes the value `1` or `-1` if `a` and `b` are coprime.  -/
jacobiSym.eq_one_or_neg_one : ∀ {a : ℤ} {b : ℕ}, a.gcd ↑b = 1 → jacobiSym a b = 1 ∨ jacobiSym a b = -1
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.StrongTrans.naturality_comp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} (self : CategoryTheory.Oplax.StrongTrans F G) {a b c : B} (f : a ⟶ b)
  (g : b ⟶ c),
  CategoryTheory.CategoryStruct.comp (self.naturality (CategoryTheory.CategoryStruct.comp f g)).hom
      (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.mapComp f g)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (self.app c))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (self.app c)).hom
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (self.naturality g).hom)
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Bicategory.associator (F.map f) (self.app b) (G.map g)).inv
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Bicategory.whiskerRight (self.naturality f).hom (G.map g))
              (CategoryTheory.Bicategory.associator (self.app a) (G.map f) (G.map g)).hom))))
-- Mathlib.NumberTheory.Rayleigh
/-- Generalization of Rayleigh's theorem on Beatty sequences. Let `r` be a real number greater
than 1, and `1/r + 1/s = 1`. Then `B⁺_r` and `B⁺'_s` partition the positive integers.  -/
beattySeq_symmDiff_beattySeq'_pos : ∀ {r s : ℝ},
  r.HolderConjugate s → symmDiff {x | ∃ k > 0, beattySeq r k = x} {x | ∃ k > 0, beattySeq' s k = x} = {n | 0 < n}
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Roo.toArray_iter : ∀ {α : Type u_1} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [inst_4 : Std.Rxo.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Roo α}, r.iter.toArray = r.toArray
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.pushforward_eq_bot_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : Y ⟶ X} {S : CategoryTheory.Sieve Y},
  CategoryTheory.Sieve.pushforward f S = ⊥ ↔ S = ⊥
-- Mathlib.Data.ENNReal.BigOperators
ENNReal.sum_lt_sum_of_nonempty : ∀ {α : Type u_1} {s : Finset α}, s.Nonempty → ∀ {f g : α → ENNReal}, (∀ i ∈ s, f i < g i) → ∑ i ∈ s, f i < ∑ i ∈ s, g i
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
OpenPartialHomeomorph.extend_target_subset_range : ∀ {𝕜 : 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}, (f.extend I).target ⊆ Set.range ↑I
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.addMap_of_Z_eq_zero_left : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F}
  {Q : WeierstrassCurve.Projective.PointClass F}, W.Nonsingular P → W.NonsingularLift Q → P 2 = 0 → W.addMap ⟦P⟧ Q = Q
-- Mathlib.Analysis.Polynomial.Factorization
/-- If `f : ℝ[X]` is monic of positive degree, then `f = f₁ * f₂` with `f₁` monic
of degree `1` or `2`.

This relies on the fact that irreducible polynomials over `ℝ` have degree at most `2`.  -/
Polynomial.IsMonicOfDegree.eq_isMonicOfDegree_one_or_two_mul : ∀ {f : Polynomial ℝ} {n : ℕ},
  f.IsMonicOfDegree (n + 1) → ∃ f₁ f₂, (f₁.IsMonicOfDegree 1 ∨ f₁.IsMonicOfDegree 2) ∧ f = f₁ * f₂
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.equiv_symm_smul : ∀ {R : Type u_1} {A : Type u_3} {E : Type u_4} [inst : SMul R E] (c : R) (x' : E),
  (WithCStarModule.equiv A E).symm (c • x') = c • (WithCStarModule.equiv A E).symm x'
-- Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
CategoryTheory.SmallObject.SuccStruct.ofCocone.objIso.hcongr_9 : ∀ (C C' : Type u_1),
  C = C' →
    ∀ (inst : CategoryTheory.Category.{v_1, u_1} C) (inst' : CategoryTheory.Category.{v_1, u_1} C'),
      inst ≍ inst' →
        ∀ (J J' : Type u),
          J = J' →
            ∀ (inst_1 : LinearOrder J) (inst'_1 : LinearOrder J'),
              inst_1 ≍ inst'_1 →
                ∀ (j : J) (j' : J'),
                  j ≍ j' →
                    ∀ (F : CategoryTheory.Functor (↑(Set.Iio j)) C) (F' : CategoryTheory.Functor (↑(Set.Iio j')) C'),
                      F ≍ F' →
                        ∀ (c : CategoryTheory.Limits.Cocone F) (c' : CategoryTheory.Limits.Cocone F'),
                          c ≍ c' →
                            ∀ (i : J) (i' : J'),
                              i ≍ i' →
                                ∀ (hi : i < j) (hi' : i' < j'),
                                  hi ≍ hi' →
                                    CategoryTheory.SmallObject.SuccStruct.ofCocone.objIso c i hi ≍
                                      CategoryTheory.SmallObject.SuccStruct.ofCocone.objIso c' i' hi'
-- Aesop.Index.Forward
/-- Constant forward rules, i.e. forward rules that have no premises and no
rule pattern.  -/
Aesop.ForwardIndex.constRules : Aesop.ForwardIndex → Lean.PHashSet Aesop.ForwardRule
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.ext_indep : ∀ {α : Type u_1} {M₁ M₂ : Matroid α}, M₁.E = M₂.E → (∀ ⦃I : Set α⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I)) → M₁ = M₂
-- Mathlib.Topology.Order.DenselyOrdered
nonempty_nhds_inter_Iio : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α] {x : α}
  {u : Set α}, u ∈ nhds x → ¬IsMin x → (u ∩ Set.Iio x).Nonempty
-- Mathlib.Order.Category.FinBoolAlg
/-- Construct a bundled `FinBoolAlg` from `BooleanAlgebra` + `Fintype`.  -/
FinBoolAlg.of : (α : Type u_1) → [BooleanAlgebra α] → [Fintype α] → FinBoolAlg
-- Mathlib.Topology.MetricSpace.Basic
Subtype.metricSpace : {α : Type u_2} → {p : α → Prop} → [MetricSpace α] → MetricSpace (Subtype p)
-- Mathlib.Combinatorics.SetFamily.Compression.Down
Finset.card_memberSubfamily_add_card_nonMemberSubfamily : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (𝒜 : Finset (Finset α)),
  (Finset.memberSubfamily a 𝒜).card + (Finset.nonMemberSubfamily a 𝒜).card = 𝒜.card
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
/-- The continuous linear isomorphism between elements of a normed space, and continuous multilinear
maps in `0` variables with values in this normed space.

The direct and inverse maps are `uncurry0` and `curry0`. Use these unless you need the full
framework of linear isometric equivs.  -/
continuousMultilinearCurryFin0 : (𝕜 : Type u) →
  (G : Type wG) →
    (G' : Type wG') →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup G] →
          [inst_2 : NormedSpace 𝕜 G] →
            [inst_3 : NormedAddCommGroup G'] → [inst_4 : NormedSpace 𝕜 G'] → (G [×0]→L[𝕜] G') ≃ₗᵢ[𝕜] G'
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKeyD_unitOfList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α} {k k' fallback : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l →
      k ∈ l → (Std.TreeMap.Raw.unitOfList l cmp).getKeyD k' fallback = k
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.coe_prodMap' : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  {B : Type u_3} [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  {C : Type u_4} [inst_7 : Semiring C] [inst_8 : Algebra R C] [inst_9 : TopologicalSpace C] {D : Type u_5}
  [inst_10 : Semiring D] [inst_11 : TopologicalSpace D] [inst_12 : Algebra R D] (f₁ : A →A[R] B) (f₂ : C →A[R] D),
  ⇑(f₁.prodMap f₂) = Prod.map ⇑f₁ ⇑f₂
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₁₂.ι_D₁ : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_3} C₁₂] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₁₂] [inst_9 : CategoryTheory.Preadditive C₄]
  (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
  (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [inst_10 : F₁₂.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [inst_12 : G.Additive]
  [inst_13 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9}
  {ι₁₂ : Type u_10} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃)
  (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [inst_18 : DecidableEq ι₁₂]
  [inst_19 : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j j' : ι₄)
  (h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j) [inst_20 : HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄],
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h)
      (HomologicalComplex.mapBifunctor₁₂.D₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j') =
    HomologicalComplex.mapBifunctor₁₂.d₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j'
-- Mathlib.Algebra.Group.Equiv.Defs
/-- **Alias** of `EmbeddingLike.map_ne_one_iff`. -/
MulEquivClass.map_ne_one_iff : ∀ {F : Type u_1} {M : Type u_4} {N : Type u_5} [inst : One M] [inst_1 : One N] [inst_2 : FunLike F M N]
  [EmbeddingLike F M N] [OneHomClass F M N] {f : F} {x : M}, f x ≠ 1 ↔ x ≠ 1
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.mkOfBound_coe : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] {f : C(α, β)} {C : ℝ}
  {h : ∀ (x y : α), dist (f x) (f y) ≤ C}, ⇑(BoundedContinuousFunction.mkOfBound f C h) = ⇑f
-- Lean.Elab.ConfigEval.Basic
/-- Gets the current name of the option after any shifting.
For example, if an option is named `a.b.c.d` and there is a handler
for `a.b.*`, then the handler receives a `ConfigItem` whose current option
name is `c.d`.
 -/
Lean.Elab.ConfigEval.ConfigItem.getCurrOptionName : Lean.Elab.ConfigEval.ConfigItem → Lean.Name
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
/-- Any enriched category has an underlying category structure defined by `ForgetEnrichment`.
This is equivalent but not definitionally equal to the category structure constructed here, which is
more canonically associated to the data of an `EnrichedCategory Cat` structure.  -/
CategoryTheory.CatEnriched.instCategoryStruct : {C : Type u_1} →
  [CategoryTheory.EnrichedCategory CategoryTheory.Cat C] →
    CategoryTheory.CategoryStruct.{u_2, u_1} (CategoryTheory.CatEnriched C)
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
/-- The underlying family of 2-morphisms.  -/
CategoryTheory.Lax.LaxTrans.Modification.app : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.LaxFunctor B C} →
          {η θ : F ⟶ G} → CategoryTheory.Lax.LaxTrans.Modification η θ → (a : B) → η.app a ⟶ θ.app a
-- Mathlib.Tactic.NormNum.LegendreSymbol
Mathlib.Meta.NormNum.jacobiSymNat.even_odd₃ : ∀ (a b c : ℕ) (r : ℤ),
  a % 2 = 0 →
    b % 8 = 3 → a / 2 = c → Mathlib.Meta.NormNum.jacobiSymNat c b = r → Mathlib.Meta.NormNum.jacobiSymNat a b = -r
-- Init.Data.Vector.Lemmas
Vector.mk_beq_mk : ∀ {α : Type u_1} {n : ℕ} [inst : BEq α] {xs ys : Array α} {h : xs.size = n} {h' : ys.size = n},
  (Vector.mk xs h == Vector.mk ys h') = (xs == ys)
-- Mathlib.Data.Fin.Tuple.Basic
Fin.consCases_cons : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u} {motive : ((i : Fin n.succ) → α i) → Sort v}
  (cons : (x₀ : α 0) → (x : (i : Fin n) → α i.succ) → motive (Fin.cons x₀ x)) (x₀ : α 0) (x : (i : Fin n) → α i.succ),
  Fin.consCases cons (Fin.cons x₀ x) = cons x₀ x
-- Mathlib.Geometry.Manifold.StructureGroupoid
/-- The trivial groupoid, containing only the identity (and maps with empty source, as this is
necessary from the definition).  -/
idGroupoid : (H : Type u_2) → [inst : TopologicalSpace H] → StructureGroupoid H
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Reachable.nonempty_neighborSet_right : ∀ {V : Type u} {G : SimpleGraph V} {u v : V}, u ≠ v → G.Reachable u v → (G.neighborSet v).Nonempty
-- Mathlib.Order.Filter.AtTopBot.Group
Filter.tendsto_neg_atTop_atBot : ∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : PartialOrder G] [IsOrderedAddMonoid G],
  Filter.Tendsto Neg.neg Filter.atTop Filter.atBot
-- Mathlib.Algebra.GCDMonoid.Multiset
Multiset.gcd_ndinsert : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] [inst_2 : DecidableEq α] (a : α)
  (s : Multiset α), (Multiset.ndinsert a s).gcd = gcd a s.gcd
-- Init.Data.String.Basic
String.Pos.cast_inj : ∀ {s t : String} {hst : s = t} {p q : s.Pos}, p.cast hst = q.cast hst ↔ p = q
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- A free group over one generator is an instance of a cyclic group.  -/
FreeGroup.instIsCyclicOfUnique : ∀ {α : Type u} [Unique α], IsCyclic (FreeGroup α)
-- Mathlib.Combinatorics.Quiver.Cast
Quiver.Path.cast_cast : ∀ {U : Type u_1} [inst : Quiver U] {u v u' v' u'' v'' : U} (p : Quiver.Path u v) (hu : u = u') (hv : v = v')
  (hu' : u' = u'') (hv' : v' = v''), Quiver.Path.cast hu' hv' (Quiver.Path.cast hu hv p) = Quiver.Path.cast ⋯ ⋯ p
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.StdSimplex.ext_iff : ∀ {R : Type u} [inst : PartialOrder R] [inst_1 : Semiring R] {M : Type u_9} {f g : Convexity.StdSimplex R M},
  f = g ↔ f.weights = g.weights
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.lift_natCast : ∀ (n : ℕ), Cardinal.lift.{u, v} ↑n = ↑n
-- Mathlib.Geometry.Manifold.BumpFunction
SmoothBumpFunction.mk.sizeOf_spec : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {c : M}
  [inst_5 : SizeOf E] [inst_6 : SizeOf H] [inst_7 : SizeOf M] (toContDiffBump : ContDiffBump (↑(extChartAt I c) c))
  (closedBall_subset :
    Metric.closedBall (↑(extChartAt I c) c) toContDiffBump.rOut ∩ Set.range ↑I ⊆ (extChartAt I c).target),
  sizeOf { toContDiffBump := toContDiffBump, closedBall_subset := closedBall_subset } = 1 + sizeOf toContDiffBump
-- Mathlib.GroupTheory.Subgroup.Simple
IsSimpleGroup.isSimpleGroup_of_surjective : ∀ {G : Type u_1} [inst : Group G] {H : Type u_3} [inst_1 : Group H] [IsSimpleGroup G] [Nontrivial H] (f : G →* H),
  Function.Surjective ⇑f → IsSimpleGroup H
-- Init.Data.UInt.Lemmas
UInt8.add_assoc : ∀ (a b c : UInt8), a + b + c = a + (b + c)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.unop.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F.op),
  c.unop = { pt := Opposite.unop c.pt, π := CategoryTheory.NatTrans.removeOp c.ι }
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.gc_map_comap : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : AddCommGroup V₂]
  [inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂),
  GaloisConnection (AffineSubspace.map f) (AffineSubspace.comap f)
-- Aesop.Tree.Data
Aesop.Goal.preNormGoal : Aesop.Goal → Lean.MVarId
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.integral_toReal_rnDeriv_mul : ∀ {α : Type u_3} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [μ.HaveLebesgueDecomposition ν]
  [MeasureTheory.SigmaFinite μ],
  μ.AbsolutelyContinuous ν → ∀ {f : α → ℝ}, ∫ (x : α), (μ.rnDeriv ν x).toReal * f x ∂ν = ∫ (x : α), f x ∂μ
-- Init.Data.SInt.Basic
/-- Converts an arbitrary-precision integer to a 32-bit integer, wrapping on overflow or underflow.

Examples:
* `Int.toInt32 48 = 48`
* `Int.toInt32 (-129) = -129`
* `Int.toInt32 70000 = 70000`
* `Int.toInt32 (-40000) = -40000`
* `Int.toInt32 2147483648 = -2147483648`
* `Int.toInt32 (-2147483649) = 2147483647`
 -/
Int.toInt32 : ℤ → Int32
-- Mathlib.Util.Notation3
/-- Used when processing different kinds of variables when building the
final delaborator.  -/
Mathlib.Notation3.BoundValueType : Type
-- Mathlib.Logic.Relator
Relator.rel_imp : Relator.LiftFun Iff (Relator.LiftFun Iff Iff) (fun x1 x2 => x1 → x2) fun x1 x2 => x1 → x2
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalSubgroup.instFiniteIndex : ∀ {G : Type u_1} [inst : Group G] (H : FiniteIndexNormalSubgroup G), H.FiniteIndex
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
/-- If a path `p` is Hamiltonian then the graph has finitely many vertices.  -/
SimpleGraph.Walk.IsHamiltonian.finite : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {a b : α} {p : G.Walk a b}, p.IsHamiltonian → Finite α
-- Mathlib.Data.QPF.Univariate.Basic
QPF.Cofix.corec.eq_1 : ∀ {F : Type u → Type u} [q : QPF F] {α : Type u} (g : α → F α) (x : α),
  QPF.Cofix.corec g x = Quot.mk QPF.Mcongr (QPF.corecF g x)
-- Mathlib.Data.Nat.Totient
Nat.totient_two_mul_of_odd : ∀ {n : ℕ}, Odd n → (2 * n).totient = n.totient
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.contains_filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Bool} {k : α},
  (Std.DTreeMap.filter f t).contains k = Option.any (f k) (t.get? k)
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedAddSubmonoid.instTop : {M : Type u_1} → [inst : AddZeroClass M] → Top (SaturatedAddSubmonoid M)
-- Std.Http.Data.Headers.Basic
/-- Proof that all tokens satisfy `isToken`.
 -/
Std.Http.Header.Connection.valid : ∀ (self : Std.Http.Header.Connection), self.tokens.all Std.Http.Internal.isToken = true
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.skipPrefix?_eq_forwardPatternSkipPrefix? : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat] {s : String.Slice},
  s.skipPrefix? pat = String.Slice.Pattern.ForwardPattern.skipPrefix? pat s
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Multipliable.countable_mulSupport : ∀ {α : Type u_1} {G : Type u_4} [inst : TopologicalSpace G] [inst_1 : CommGroup G] [IsTopologicalGroup G] {f : α → G}
  [FirstCountableTopology G] [T1Space G], Multipliable f → (Function.mulSupport f).Countable
-- Mathlib.Logic.Function.Basic
Function.instSymmSwapProp : ∀ {α : Sort u_1} (r : α → α → Prop) [Std.Symm r], Std.Symm (Function.swap r)
-- Mathlib.Algebra.Star.MonoidHom
StarMulEquiv.rightInverse_symm : ∀ {A : Type u_2} {B : Type u_3} [inst : Mul A] [inst_1 : Mul B] [inst_2 : Star A] [inst_3 : Star B] (e : A ≃⋆* B),
  Function.RightInverse ⇑e.symm ⇑e
-- Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy
TopCat.zerothHomotopyEquiv_symm_mk : ∀ {X : TopCat} (x : (TopCat.toSSet.obj X).obj (Opposite.op { len := 0 })),
  TopCat.zerothHomotopyEquiv.symm (SSet.π₀.mk x) = ZerothHomotopy.mk (TopCat.toSSetObj₀Equiv x)
-- Mathlib.Order.TypeTags
WithBot.coe.eq_1 : ∀ {α : Type u_1}, WithBot.coe = { coe := WithBot.some }