mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.FieldTheory.PurelyInseparable.Basic
isSeparable_iff_finInsepDegree_eq_one : ∀ (F : Type u) [inst : Field F] (K : Type w) [inst_1 : Field K] [inst_2 : Algebra F K],
  Algebra.IsSeparable F K ↔ Field.finInsepDegree F K = 1
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
continuousAt_jacobiTheta : ∀ {τ : ℂ}, 0 < τ.im → ContinuousAt jacobiTheta τ
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_filter_not_contains : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.getKey? k (List.filter (fun p => !l₂.contains p.fst) l₁) =
      if l₂.contains k = true then none else Std.Internal.List.getKey? k l₁
-- Mathlib.Algebra.Homology.Augment
_private.Mathlib.Algebra.Homology.Augment.0.ChainComplex.augment.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (i : ℕ) (h_1 : Unit → motive 0) (h_2 : (i : ℕ) → motive i.succ),
  (match i.succ with
    | 0 => h_1 ()
    | i.succ => h_2 i) =
    h_2 i
-- Lean.Parser.Types
Lean.Parser.ParserCacheEntry : Type
-- Mathlib.Data.Part
Part.some_sub_some : ∀ {α : Type u_1} [inst : Sub α] (a b : α), Part.some a - Part.some b = Part.some (a - b)
-- Mathlib.ModelTheory.Order
/-- Any countable nonempty model of the theory of dense linear orders is a Fraïssé limit of the
class of finite models of the theory of linear orders.  -/
FirstOrder.Language.isFraisseLimit_of_countable_nonempty_dlo : ∀ (M : Type w) [inst : FirstOrder.Language.order.Structure M] [inst_1 : Countable M] [Nonempty M]
  [M ⊨ FirstOrder.Language.order.dlo],
  FirstOrder.Language.IsFraisseLimit {M | Finite ↑M ∧ ↑M ⊨ FirstOrder.Language.order.linearOrderTheory} M
-- Init.Data.Array.Lemmas
/-- Variant of `any_push` with a side condition on `stop`.  -/
Array.any_push' : ∀ {α : Type u_1} {stop : ℕ} {xs : Array α} {a : α} {p : α → Bool},
  stop = xs.size + 1 → (xs.push a).any p 0 stop = (xs.any p || p a)
-- Mathlib.Tactic.CancelDenoms.Core
Mathlib.Tactic.CancelDenoms.CancelResult.mk.inj : ∀ {u : Lean.Level} {α : Q(Type u)} {mα : Q(Mul «$α»)} {e v cancelled : Q(«$α»)} {pf : Q(«$v» * «$e» = «$cancelled»)}
  {cancelled_1 : Q(«$α»)} {pf_1 : Q(«$v» * «$e» = «$cancelled_1»)},
  { cancelled := cancelled, pf := pf } = { cancelled := cancelled_1, pf := pf_1 } → cancelled = cancelled_1 ∧ pf = pf_1
-- Batteries.Data.List.Basic
/-- `rotate l n` rotates the elements of `l` to the left by `n`
```
rotate [0, 1, 2, 3, 4, 5] 2 = [2, 3, 4, 5, 0, 1]
```
 -/
List.rotate : {α : Type u_1} → List α → ℕ → List α
-- Mathlib.Topology.Algebra.UniformConvergence
instNSMulUniformFun : {α : Type u_1} → {β : Type u_2} → {M : Type u_5} → [SMul M β] → SMul M (UniformFun α β)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- The sum of two strictly antitone functions is strictly antitone.  -/
StrictAntiOn.add : ∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α} {s : Set β}
  [AddLeftStrictMono α] [AddRightStrictMono α],
  StrictAntiOn f s → StrictAntiOn g s → StrictAntiOn (fun x => f x + g x) s
-- Mathlib.Order.Filter.Pi
Filter.coprodᵢ_bot : ∀ {ι : Type u_1} {α : ι → Type u_2}, (Filter.coprodᵢ fun x => ⊥) = ⊥
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.mem_map_equiv : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S] {f : R ≃+* S}
  {K : NonUnitalSubring R} {x : S}, x ∈ NonUnitalSubring.map (↑f) K ↔ f.symm x ∈ K
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
zmodAddEquivOfGenerator.congr_simp : ∀ {G : Type u_2} [inst : AddGroup G] {g g_1 : G} (e_g : g = g_1) (hg : ∀ (x : G), x ∈ AddSubgroup.zmultiples g) {n : ℕ}
  (hn : Nat.card G = n), zmodAddEquivOfGenerator hg hn = zmodAddEquivOfGenerator ⋯ hn
-- Mathlib.Util.Export
Lean.Export.biStr : Lean.BinderInfo → String
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.symm_mk : ∀ {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] (e : R ≃ S)
  (h₁ : ∀ (x y : R), e.toFun (x * y) = e.toFun x * e.toFun y)
  (h₂ : ∀ (x y : R), e.toFun (x + y) = e.toFun x + e.toFun y),
  { toEquiv := e, map_mul' := h₁, map_add' := h₂ }.symm = { toEquiv := e.symm, map_mul' := ⋯, map_add' := ⋯ }
-- Mathlib.Topology.Order.SuccPred
PredOrder.nhds_of_isMax : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α] [PredOrder α] [NoMinOrder α]
  {a : α}, IsMax a → nhds a = pure a
-- Init.Data.UInt.Lemmas
UInt8.neg_inj : ∀ {a b : UInt8}, -a = -b ↔ a = b
-- Aesop.RuleTac.Descr
Aesop.RuleTacDescr.apply.injEq : ∀ (term : Aesop.RuleTerm) (md : Lean.Meta.TransparencyMode) (term_1 : Aesop.RuleTerm)
  (md_1 : Lean.Meta.TransparencyMode),
  (Aesop.RuleTacDescr.apply term md = Aesop.RuleTacDescr.apply term_1 md_1) = (term = term_1 ∧ md = md_1)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.maxView!.eq_2 : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β) (size : ℕ) (k' : α) (v' : β k')
  (l' r' : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.maxView! k v l (Std.DTreeMap.Internal.Impl.inner size k' v' l' r') =
    { k := (Std.DTreeMap.Internal.Impl.maxView! k' v' l' r').k,
      v := (Std.DTreeMap.Internal.Impl.maxView! k' v' l' r').v,
      tree := Std.DTreeMap.Internal.Impl.balanceL! k v l (Std.DTreeMap.Internal.Impl.maxView! k' v' l' r').tree }
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y}
  [inst_2 : CategoryTheory.IsSplitMono f] {c : CategoryTheory.Limits.CokernelCofork f}
  (i : CategoryTheory.Limits.IsColimit c),
  (CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel i).fst = CategoryTheory.retraction f
-- Mathlib.Analysis.Convex.SpecificFunctions.Pow
Real.strictConcaveOn_sqrt : StrictConcaveOn ℝ (Set.Ici 0) fun x => √x
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.max?_of_isEmpty : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp], t.isEmpty = true → t.max? = none
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get!_alter_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} [inst_1 : Inhabited β] {f : Option β → Option β},
  Std.ExtDTreeMap.Const.get! (Std.ExtDTreeMap.Const.alter t k f) k = (f (Std.ExtDTreeMap.Const.get? t k)).get!
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.Const.minEntryD.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → α × β → Sort u_3) (size : ℕ)
  (k : α) (v : β) (r : Std.DTreeMap.Internal.Impl α fun x => β) (x : α × β)
  (h_1 : (fallback : α × β) → motive Std.DTreeMap.Internal.Impl.leaf fallback)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (r : Std.DTreeMap.Internal.Impl α fun x => β) →
            (x : α × β) → motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x)
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l : Std.DTreeMap.Internal.Impl α fun x => β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α fun x => β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r →
                      (r_1 : Std.DTreeMap.Internal.Impl α fun x => β) →
                        (fallback : α × β) →
                          motive
                            (Std.DTreeMap.Internal.Impl.inner size k v
                              (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) r_1)
                            fallback),
  (match Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x with
    | Std.DTreeMap.Internal.Impl.leaf, fallback => h_1 fallback
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x => h_2 size k v r x
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) r_1,
      fallback => h_3 size k v l size_1 k_1 v_1 l_1 r h r_1 fallback) =
    h_2 size k v r x
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
ContMDiffOn.coordChange : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6}
  [inst : NontriviallyNormedField 𝕜] {EB : Type u_7} [inst_1 : NormedAddCommGroup EB] [inst_2 : NormedSpace 𝕜 EB]
  {HB : Type u_8} [inst_3 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [inst_4 : TopologicalSpace B]
  [inst_5 : ChartedSpace HB B] {EM : Type u_9} [inst_6 : NormedAddCommGroup EM] [inst_7 : NormedSpace 𝕜 EM]
  {HM : Type u_10} [inst_8 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [inst_9 : TopologicalSpace M]
  [inst_10 : ChartedSpace HM M] [inst_11 : (x : B) → AddCommMonoid (E x)] [inst_12 : (x : B) → Module 𝕜 (E x)]
  [inst_13 : NormedAddCommGroup F] [inst_14 : NormedSpace 𝕜 F] [inst_15 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_16 : (x : B) → TopologicalSpace (E x)] [inst_17 : FiberBundle F E] [inst_18 : VectorBundle 𝕜 F E]
  [ContMDiffVectorBundle n F E IB] {e e' : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e]
  [MemTrivializationAtlas e'] {s : Set M} {f : M → B} {g : M → F},
  ContMDiffOn IM IB n f s →
    ContMDiffOn IM (modelWithCornersSelf 𝕜 F) n g s →
      Set.MapsTo f s e.baseSet →
        Set.MapsTo f s e'.baseSet →
          ContMDiffOn IM (modelWithCornersSelf 𝕜 F) n (fun y => e.coordChange e' (f y) (g y)) s
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.Hom.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y : AlgebraicGeometry.PresheafedSpace C} →
      (base : ↑X ⟶ ↑Y) → (Y.presheaf ⟶ (TopCat.Presheaf.pushforward C base).obj X.presheaf) → X.Hom Y
-- Lean.Elab.Tactic.Try
Lean.Elab.Tactic.Try.evalSuggestExact : Lean.Elab.Tactic.TacticM (Lean.TSyntax `tactic)
-- Mathlib.Algebra.GroupWithZero.Nat
Nat.instMulZeroOneClass : MulZeroOneClass ℕ
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
contDiffWithinAtProp_mono_of_mem_nhdsWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {E' : Type u_5}
  [inst_4 : NormedAddCommGroup E'] [inst_5 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_6 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} (n : WithTop ℕ∞) ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄,
  s ∈ nhdsWithin x t → ContDiffWithinAtProp I I' n f s x → ContDiffWithinAtProp I I' n f t x
-- Mathlib.Order.Hom.Bounded
map_eq_top_iff : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : EquivLike F α β] [inst_1 : LE α] [inst_2 : OrderTop α]
  [inst_3 : PartialOrder β] [inst_4 : OrderTop β] [OrderIsoClass F α β] (f : F) {a : α}, f a = ⊤ ↔ a = ⊤
-- Mathlib.NumberTheory.Modular
/-- Linear map sending the matrix [a, b; c, d] to the matrix [ac₀ + bd₀, - ad₀ + bc₀; c, d], for
some fixed `(c₀, d₀)`.  -/
ModularGroup.lcRow0Extend : {cd : Fin 2 → ℤ} → IsCoprime (cd 0) (cd 1) → Matrix (Fin 2) (Fin 2) ℝ ≃ₗ[ℝ] Matrix (Fin 2) (Fin 2) ℝ
-- Mathlib.CategoryTheory.Adjunction.Evaluation
CategoryTheory.evaluationRightAdjoint_obj_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : ∀ (a b : C), CategoryTheory.Limits.HasProductsOfShape (a ⟶ b) D] (c : C) (d : D) (t : C),
  ((CategoryTheory.evaluationRightAdjoint D c).obj d).obj t = ∏ᶜ fun x => d
-- Mathlib.RingTheory.Algebraic.Basic
/-- **Alias** of `isAlgebraic_intCast`. -/
isAlgebraic_int : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] [Nontrivial R] (n : ℤ),
  IsAlgebraic R ↑n
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.instHasOrthogonalProjectionOfCompleteSpace : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : ClosedSubmodule 𝕜 E) [CompleteSpace E], (↑K).HasOrthogonalProjection
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.continuousVAdd : ∀ {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i}
  [inst_1 : (i : ι) → TopologicalSpace (R i)] [hBopen : Fact (∀ (i : ι), IsOpen ↑(B i))] {G : Type u_4}
  [inst_2 : TopologicalSpace G] [inst_3 : (i : ι) → VAdd G (R i)] [inst_4 : ∀ (i : ι), VAddMemClass (S i) G (R i)]
  [∀ (i : ι), ContinuousVAdd G (R i)],
  ContinuousVAdd G (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) Filter.cofinite)
-- Mathlib.RingTheory.Localization.BaseChange
Localization.tensorLeftAlgEquiv_apply_tmul_one : ∀ {R : Type u_10} [inst : CommRing R] (M : Submonoid R) {S : Type u_12} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (x : S),
  (Localization.tensorLeftAlgEquiv M S) (x ⊗ₜ[R] 1) = (algebraMap S (Localization (Algebra.algebraMapSubmonoid S M))) x
-- Mathlib.Algebra.Group.Submonoid.Operations
MulEquiv.submonoidMap_symm_apply : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (e : M ≃* N) (S : Submonoid M)
  (g : ↥(Submonoid.map (↑e) S)), (e.submonoidMap S).symm g = ⟨e.symm ↑g, ⋯⟩
-- Mathlib.Topology.Algebra.Valued.NormedValued
Valued.instIsUltrametricDist : ∀ (L : Type u_1) [inst : Field L] (Γ₀ : Type u_2) [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀]
  [hv : Valued.v.RankOne], IsUltrametricDist L
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basis
ExteriorAlgebra.basis_apply : ∀ {R : Type u_1} {M : Type u_2} {I : Type u_3} [inst : LinearOrder I] [inst_1 : CommRing R] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] (b : Module.Basis I R M) (s : Finset I),
  b.ExteriorAlgebra s = ExteriorAlgebra.ιMulti_family R s.card (⇑b) (Set.powersetCard.prodEquiv.symm s).snd
-- Mathlib.FieldTheory.Normal.Closure
IntermediateField.normalClosure.eq_1 : ∀ (F : Type u_1) (K : Type u_2) (L : Type u_3) [inst : Field F] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra F K] [inst_4 : Algebra F L], IntermediateField.normalClosure F K L = ⨆ f, f.fieldRange
-- Init.Data.Array.MinMax
List.min_toArray : ∀ {α : Type u_1} [inst : Min α] {l : List α} {h : l.toArray ≠ #[]}, l.toArray.min h = l.min ⋯
-- Lean.Meta.TryThis
_private.Lean.Meta.TryThis.0.Lean.Meta.Tactic.TryThis.getIndentAndColumn.findLineStart : {s : String} → s.Pos → s.Pos
-- Mathlib.Data.List.SplitBy
_private.Mathlib.Data.List.SplitBy.0.List.nil_notMem_splitByLoop : ∀ {α : Type u_1} {r : α → α → Bool} {l : List α} {a : α} {g : List α}, [] ∉ List.splitBy.loop r l a g []
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
MeasureTheory.charFun.eq_1 : ∀ {E : Type u_2} {mE : MeasurableSpace E} [inst : Inner ℝ E] (μ : MeasureTheory.Measure E) (t : E),
  MeasureTheory.charFun μ t = ∫ (x : E), Complex.exp (↑(inner ℝ x t) * Complex.I) ∂μ
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
mul_nonpos_iff_neg_imp_nonneg : ∀ {R : Type u} [inst : Ring R] [inst_1 : LinearOrder R] {a b : R} [PosMulStrictMono R] [MulPosStrictMono R]
  [AddLeftMono R] [AddLeftReflectLE R], a * b ≤ 0 ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_roc_eq_toArray_roo : ∀ {m n : ℕ}, (m<...=n).toArray = (m<...n + 1).toArray
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.upperCrossingTime_eq_of_upcrossingsBefore_lt : ∀ {Ω : Type u_1} {a b : ℝ} {f : ℕ → Ω → ℝ} {N n : ℕ} {ω : Ω},
  a < b → MeasureTheory.upcrossingsBefore a b f N ω < n → MeasureTheory.upperCrossingTime a b f N n ω = N
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
unitInterval.sigmoid_le_iff : ∀ {a b : ℝ}, unitInterval.sigmoid a ≤ unitInterval.sigmoid b ↔ a ≤ b
-- Mathlib.Analysis.Matrix.LDL
/-- The entries of the diagonal matrix `D` of the LDL decomposition.  -/
LDL.diagEntries : {𝕜 : Type u_1} →
  [inst : RCLike 𝕜] →
    {n : Type u_2} →
      [inst_1 : LinearOrder n] →
        [WellFoundedLT n] → [LocallyFiniteOrderBot n] → {S : Matrix n n 𝕜} → [Fintype n] → S.PosDef → n → 𝕜
-- Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
/-- If a set in a manifold has the unique derivative property, then its pullback by any extended
chart, in the vector space, also has the unique derivative property.  -/
UniqueMDiffOn.uniqueDiffOn_target_inter : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} [IsManifold I 1 M],
  UniqueMDiff[s] → ∀ (x : M), UniqueDiffOn 𝕜 ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s)
-- Init.Data.Nat.Lemmas
Nat.mul_eq_right : ∀ {b a : ℕ}, b ≠ 0 → (a * b = b ↔ a = 1)
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.pow_eq : ∀ {κ μ : Cardinal.{u}}, Cardinal.aleph0 ≤ κ → 1 ≤ μ → μ < Cardinal.aleph0 → κ ^ μ = κ
-- Mathlib.Topology.Algebra.Module.ModuleTopology
IsModuleTopology.continuousNeg : ∀ (R : Type u_1) [τR : TopologicalSpace R] [inst : Semiring R] (C : Type u_6) [inst_1 : AddCommGroup C]
  [inst_2 : Module R C] [inst_3 : TopologicalSpace C] [IsModuleTopology R C], ContinuousNeg C
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.commute_sub_int : ∀ (f : CircleDeg1Lift) (n : ℤ), Function.Commute ⇑f fun x => x - ↑n
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
TensorAlgebra.toClifford_ι : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (m : M), TensorAlgebra.toClifford ((TensorAlgebra.ι R) m) = (CliffordAlgebra.ι Q) m
-- Mathlib.Order.Filter.Finite
Filter.eventually_all : ∀ {α : Type u} {ι : Sort u_2} [Finite ι] {l : Filter α} {p : ι → α → Prop},
  (∀ᶠ (x : α) in l, ∀ (i : ι), p i x) ↔ ∀ (i : ι), ∀ᶠ (x : α) in l, p i x
-- Mathlib.Algebra.Polynomial.Eval.Defs
/-- **Alias** of `Polynomial.eval_finsetSum`. -/
Polynomial.eval_finset_sum : ∀ {R : Type u} {ι : Type y} [inst : Semiring R] (s : Finset ι) (g : ι → Polynomial R) (x : R),
  Polynomial.eval x (∑ i ∈ s, g i) = ∑ i ∈ s, Polynomial.eval x (g i)
-- Mathlib.Geometry.Manifold.ChartedSpace
chart_source_mem_nhds : ∀ (H : Type u) {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  (x : M), (chartAt H x).source ∈ nhds x
-- Mathlib.Order.Interval.Set.Basic
Set.Ioc_ofDual : ∀ {α : Type u_1} [inst : Preorder α] {x y : αᵒᵈ},
  Set.Ioc (OrderDual.ofDual x) (OrderDual.ofDual y) = ⇑OrderDual.toDual ⁻¹' Set.Ico y x
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.skip.formatter : Lean.PrettyPrinter.Formatter
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryLE.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k : α)
  (x_3 : Std.DTreeMap.Internal.Impl.leaf.Ordered)
  (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.leaf, (compare a k).isLE = true),
  Std.DTreeMap.Internal.Impl.getEntryLE k Std.DTreeMap.Internal.Impl.leaf x_3 he = ⋯.elim
-- Lean.DocString.Markdown
Lean.Doc.ToMarkdown.mk : {α : Type u} → (α → Lean.Doc.MarkdownM (Array String)) → Lean.Doc.ToMarkdown α
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.set_support_apply_mem : ∀ {α : Type u_1} {p : Equiv.Perm α} {a : α}, p a ∈ {x | p x ≠ x} ↔ a ∈ {x | p x ≠ x}
-- Mathlib.Algebra.DualNumber
/-- For two `R`-algebra morphisms out of `R[ε]` to agree, it suffices for them to agree on `ε`.  -/
DualNumber.algHom_ext : ∀ {R : Type u_1} {A : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  ⦃f g : DualNumber R →ₐ[R] A⦄, f DualNumber.eps = g DualNumber.eps → f = g
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey?_eq_none : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {a : α}, a ∉ m → m.getKey? a = none
-- Mathlib.Topology.Bornology.Absorbs
Filter.mem_absorbing : ∀ {G₀ : Type u_1} {α : Type u_2} [inst : GroupWithZero G₀] [inst_1 : Bornology G₀] [inst_2 : MulAction G₀ α]
  {s u : Set α}, s ∈ Filter.absorbing G₀ u ↔ Absorbs G₀ s u
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀ : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) {f : α → ENNReal} {s : Set α},
  AEMeasurable f (μ.restrict s) →
    ∀ (g : α → ENNReal),
      MeasurableSet s →
        (∀ᵐ (x : α) ∂μ.restrict s, f x < ⊤) → ∫⁻ (a : α) in s, g a ∂μ.withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ
-- Mathlib.GroupTheory.OrderOfElement
/-- A multiplicative equivalence preserves orders of elements.  -/
MulEquiv.orderOf_eq : ∀ {G : Type u_1} [inst : Monoid G] {H : Type u_6} [inst_1 : Monoid H] (e : G ≃* H) (x : G), orderOf (e x) = orderOf x
-- Mathlib.Analysis.Convex.Star
starConvex_empty : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] (x : E), StarConvex 𝕜 x ∅
-- Mathlib.Order.Ideal
/-- An ideal on an order `P` is a subset of `P` that is
- nonempty
- upward directed (any pair of elements in the ideal has an upper bound in the ideal)
- downward closed (any element less than an element of the ideal is in the ideal).  -/
Order.Ideal : (P : Type u_2) → [LE P] → Type u_2
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MCasesPat.one.sizeOf_spec : ∀ (name : Lean.TSyntax `Lean.binderIdent), sizeOf (Lean.Parser.Tactic.MCasesPat.one name) = 1 + sizeOf name
-- Mathlib.Data.ZMod.Basic
ZMod.ringEquivCongr_symm : ∀ {a b : ℕ} (hab : a = b), (ZMod.ringEquivCongr hab).symm = ZMod.ringEquivCongr ⋯
-- Mathlib.Topology.Algebra.Module.ModuleTopology
/-- A class asserting that the topology on a module over a topological ring `R` is
the module topology. See `moduleTopology` for more discussion of the module topology.  -/
IsModuleTopology : (R : Type u_1) → [TopologicalSpace R] → (A : Type u_2) → [Add A] → [SMul R A] → [τA : TopologicalSpace A] → Prop
-- Init.Grind.AC
_private.Init.Grind.AC.0.Lean.Grind.AC.Seq.unionFuel.match_3.splitter : (motive : ℕ → Sort u_1) → (fuel : ℕ) → (Unit → motive 0) → ((fuel : ℕ) → motive fuel.succ) → motive fuel
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.map_id : ∀ {R : Type u_1} [inst : Semiring R], ⇑(PowerSeries.map (RingHom.id R)) = id
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.FamilyOfElements.Compatible.pullback : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X Y : C}
  {S : CategoryTheory.Sieve X} (f : Y ⟶ X) {x : CategoryTheory.Presieve.FamilyOfElements P S.arrows},
  x.Compatible → (CategoryTheory.Presieve.FamilyOfElements.pullback f x).Compatible
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
Int.reduceEq : Lean.Meta.Simp.Simproc
-- Mathlib.GroupTheory.GroupExtension.Basic
AddGroupExtension.IsAddConj.setoid.eq_1 : ∀ {N : Type u_1} {G : Type u_2} [inst : AddGroup N] [inst_1 : AddGroup G] {E : Type u_3} [inst_2 : AddGroup E]
  (S : AddGroupExtension N E G), AddGroupExtension.IsAddConj.setoid S = { r := S.IsAddConj, iseqv := ⋯ }
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.restrictScalarsEquivalenceOfRingEquiv_counitIso : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] (e : R ≃+* S),
  (ModuleCat.restrictScalarsEquivalenceOfRingEquiv e).counitIso =
    (ModuleCat.restrictScalarsComp' e.toRingHom e.symm.toRingHom (RingHom.id R) ⋯).symm ≪≫ ModuleCat.restrictScalarsId R
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.closure_closure_coe_preimage : ∀ {M : Type u_1} [inst : Mul M] {s : Set M}, Subsemigroup.closure (Subtype.val ⁻¹' s) = ⊤
-- Mathlib.SetTheory.ZFC.PSet
/-- The underlying type of a pre-set  -/
PSet.Type : PSet.{u} → Type u
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.coe_compRingHom : ∀ {R : Type u} [inst : CommSemiring R] (q : Polynomial R), ⇑q.compRingHom = fun p => p.comp q