mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.ContMDiff.Atlas
contMDiffAt_of_mem_maximalAtlas : ∀ {𝕜 : 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] {n : WithTop ℕ∞} {e : OpenPartialHomeomorph M H} {x : M},
  e ∈ IsManifold.maximalAtlas I n M → x ∈ e.source → ContMDiffAt I I n (↑e) x
-- Init.Data.Int.DivMod.Lemmas
Int.mul_le_mul_left : ∀ {a b c : ℤ}, 0 < a → (a * b ≤ a * c ↔ b ≤ c)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
NumberField.ComplexEmbedding.IsConj.isReal_comp : ∀ {K : Type u_1} [inst : Field K] {k : Type u_2} [inst_1 : Field k] [inst_2 : Algebra k K] {φ : K →+* ℂ} {σ : Gal(K/k)},
  NumberField.ComplexEmbedding.IsConj φ σ → NumberField.ComplexEmbedding.IsReal (φ.comp (algebraMap k K))
-- Mathlib.Combinatorics.Enumerative.Pentagonal.Basic
pentagonal_strictMonoOn : StrictMonoOn pentagonal (Set.Ici 0)
-- Mathlib.Dynamics.Minimal
MulAction.IsMinimal.mk : ∀ {M : Type u_1} {α : Type u_2} [inst : Monoid M] [inst_1 : TopologicalSpace α] [inst_2 : MulAction M α],
  (∀ (x : α), Dense (MulAction.orbit M x)) → MulAction.IsMinimal M α
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- Make a morphism in `P.Under Q X` from a morphism in `T` with compatibilities.  -/
CategoryTheory.MorphismProperty.Under.homMk : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    {P Q : CategoryTheory.MorphismProperty T} →
      {X : T} →
        [inst_1 : Q.IsMultiplicative] →
          {A B : P.Under Q X} →
            (f : A.right ⟶ B.right) →
              autoParam (CategoryTheory.CategoryStruct.comp A.hom f = B.hom)
                  CategoryTheory.MorphismProperty.Under.homMk._auto_1 →
                autoParam (Q f) CategoryTheory.MorphismProperty.Under.homMk._auto_3 → (A ⟶ B)
-- Mathlib.Topology.Algebra.Group.Defs
ContinuousOn.sub : ∀ {G : Type u_1} {X : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace G] [inst_2 : Sub G]
  [ContinuousSub G] {f g : X → G} {s : Set X}, ContinuousOn f s → ContinuousOn g s → ContinuousOn (f - g) s
-- Mathlib.Algebra.Algebra.Tower
AlgHom.restrictScalars_extendScalarsOfSurjective : ∀ {R : Type u} {S : Type v} {A : Type w} {B : Type u₁} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R S] [inst_5 : Algebra S A] [inst_6 : Algebra S B]
  [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R S A] [inst_10 : IsScalarTower R S B]
  (h : Function.Surjective ⇑(algebraMap R S)) (f : A →ₐ[R] B),
  AlgHom.restrictScalars R ((AlgHom.extendScalarsOfSurjective h) f) = f
-- Mathlib.Data.Finset.Density
Finset.dens_map_le : ∀ {α : Type u_2} {β : Type u_3} [inst : Fintype α] {s : Finset α} [inst_1 : Fintype β] (f : α ↪ β),
  (Finset.map f s).dens ≤ s.dens
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Iterators.HetT.pure_bind : ∀ {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] {α : Type u} {β : Type v} {f : α → Std.Iterators.HetT m β}
  {a : α}, (Std.Iterators.HetT.pure a).bind f = f a
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rco.forIn'_congr : ∀ {α : Type u} [inst : LE α] [inst_1 : LT α] [inst_2 : DecidableLT α] [inst_3 : Std.PRange.UpwardEnumerable α]
  [inst_4 : Std.PRange.LawfulUpwardEnumerableLE α] [inst_5 : Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_6 : Std.Rxo.IsAlwaysFinite α] [inst_7 : Std.PRange.LawfulUpwardEnumerable α] {m : Type u → Type w}
  [inst_8 : Monad m] {γ : Type u} {init init' : γ} {r r' : Std.Rco α} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)}
  {f' : (a : α) → a ∈ r' → γ → m (ForInStep γ)} (hr : r = r'),
  init = init' → (∀ (a : α) (m_1 : a ∈ r') (b : γ), f a ⋯ b = f' a m_1 b) → forIn' r init f = forIn' r' init' f'
-- Mathlib.Tactic.Widget.LibraryRewrite
Mathlib.Tactic.LibraryRewrite.instBEqRewriteLemma : BEq Mathlib.Tactic.LibraryRewrite.RewriteLemma
-- Mathlib.Analysis.Analytic.Constructions
FormalMultilinearSeries.radius_pi_le : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {ι : Type u_9} [inst_3 : Fintype ι] {Fm : ι → Type u_10}
  [inst_4 : (i : ι) → NormedAddCommGroup (Fm i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (Fm i)]
  (p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)) (i : ι), (FormalMultilinearSeries.pi p).radius ≤ (p i).radius
-- Lean.Declaration
Lean.InductiveVal.toConstantVal : Lean.InductiveVal → Lean.ConstantVal
-- Lean.Data.Lsp.Diagnostics
/-- Whether the client should append this set of diagnostics to the previous set
rather than replacing the previous set by this one (the default LSP behavior).
`false` means the client should replace.
`none` is equivalent to `false`.
This is a Lean-specific extension (see `LeanClientCapabilities`).
 -/
Lean.Lsp.PublishDiagnosticsParams.isIncremental? : Lean.Lsp.PublishDiagnosticsParams → Option Bool
-- Mathlib.Analysis.Real.Sqrt
Real.sqrt_eq_iff_mul_self_eq : ∀ {x y : ℝ}, 0 ≤ x → 0 ≤ y → (√x = y ↔ x = y * y)
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.getEntryGT?ₘ'.match_1.eq_3 : ∀ {α : Type u_2} {β : α → Type u_1} [inst : Ord α] (k : α)
  (motive :
    Option ((a : α) × β a) →
      (Std.DTreeMap.Internal.Impl.ExplorationStep α β fun k' => (compare k k').then Ordering.gt) → Sort u_3)
  (base : Option ((a : α) × β a)) (a : List ((a : α) × β a)) (a_1 : α)
  (a_2 : (compare k a_1).then Ordering.gt = Ordering.gt) (a_3 : β a_1)
  (h_1 :
    (x : Option ((a : α) × β a)) →
      (k' : α) →
        (a : (compare k k').then Ordering.gt = Ordering.lt) →
          (v : β k') →
            (a_4 : List ((a : α) × β a)) → motive x (Std.DTreeMap.Internal.Impl.ExplorationStep.lt k' a v a_4))
  (h_2 :
    (base : Option ((a : α) × β a)) →
      (a : List ((a : α) × β a)) →
        (a_4 : Std.DTreeMap.Internal.Cell α β fun k' => (compare k k').then Ordering.gt) →
          (r : List ((a : α) × β a)) → motive base (Std.DTreeMap.Internal.Impl.ExplorationStep.eq a a_4 r))
  (h_3 :
    (base : Option ((a : α) × β a)) →
      (a : List ((a : α) × β a)) →
        (a_4 : α) →
          (a_5 : (compare k a_4).then Ordering.gt = Ordering.gt) →
            (a_6 : β a_4) → motive base (Std.DTreeMap.Internal.Impl.ExplorationStep.gt a a_4 a_5 a_6)),
  (match base, Std.DTreeMap.Internal.Impl.ExplorationStep.gt a a_1 a_2 a_3 with
    | x, Std.DTreeMap.Internal.Impl.ExplorationStep.lt k' a v a_4 => h_1 x k' a v a_4
    | base, Std.DTreeMap.Internal.Impl.ExplorationStep.eq a a_4 r => h_2 base a a_4 r
    | base, Std.DTreeMap.Internal.Impl.ExplorationStep.gt a a_4 a_5 a_6 => h_3 base a a_4 a_5 a_6) =
    h_3 base a a_1 a_2 a_3
-- Mathlib.Order.Basic
/-- **Alias** of `strongLT_of_strongLT_of_le`. -/
StrongLT.trans_le : ∀ {ι : Type u_1} {π : ι → Type u_4} [inst : (i : ι) → Preorder (π i)] {a b c : (i : ι) → π i},
  StrongLT a b → b ≤ c → StrongLT a c
-- Mathlib.RingTheory.LocalRing.ResidueField.Instances
IsLocalRing.ResidueField.isScalarTowerOfIsIntegral : ∀ {R : Type u_4} {k : Type u_5} [inst : CommRing R] [inst_1 : IsLocalRing R] [inst_2 : Field k] [inst_3 : Algebra R k]
  [inst_4 : Algebra.IsIntegral R k], IsScalarTower R (IsLocalRing.ResidueField R) k
-- Std.Data.Internal.List.Associative
Std.Internal.List.insertEntry_of_containsKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k},
  Std.Internal.List.containsKey k l = true → Std.Internal.List.insertEntry k v l = Std.Internal.List.replaceEntry k v l
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.toFinset_symmDiff : ∀ {α : Type u} {s t : Set α} [inst : DecidableEq α] (hs : s.Finite) (ht : t.Finite) (h : (symmDiff s t).Finite),
  h.toFinset = symmDiff hs.toFinset ht.toFinset
-- Mathlib.Data.List.Induction
List.twoStepInduction.eq_3 : ∀ {α : Type u_1} {motive : List α → Sort u_2} (nil : motive []) (singleton : (x : α) → motive [x])
  (cons_cons : (x y : α) → (xs : List α) → motive xs → ((y : α) → motive (y :: xs)) → motive (x :: y :: xs)) (a b : α)
  (l_1 : List α),
  List.twoStepInduction nil singleton cons_cons (a :: b :: l_1) =
    cons_cons a b l_1 (List.twoStepInduction nil singleton cons_cons l_1) fun y =>
      List.twoStepInduction nil singleton cons_cons (y :: l_1)
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval₂_sum : ∀ {R : Type u} {S : Type v} {T : Type w} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) [inst_2 : Semiring T]
  (p : Polynomial T) (g : ℕ → T → Polynomial R) (x : S),
  Polynomial.eval₂ f x (p.sum g) = p.sum fun n a => Polynomial.eval₂ f x (g n a)
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
CategoryTheory.Limits.terminal.congr_simp : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasTerminal C],
  (⊤_ C) = ⊤_ C
-- Mathlib.Algebra.Opposites
/-- Multiplicative opposite of a type. This type inherits all additive structures on `α` and
reverses left and right in multiplication.  -/
MulOpposite : Type u_3 → Type u_3
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
/-- Join operation for standard simplices (monadic join).
Given a distribution over distributions, flattens it to a single distribution.

Use `ConvexSpace.sConvexComb` instead.
 -/
Convexity.StdSimplex.join : {R : Type u} →
  [inst : PartialOrder R] →
    [inst_1 : Semiring R] →
      {M : Type u_9} →
        [IsStrictOrderedRing R] → Convexity.StdSimplex R (Convexity.StdSimplex R M) → Convexity.StdSimplex R M
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.one_mem_div_iff : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Group α] {s t : Finset α}, 1 ∈ s / t ↔ ¬Disjoint s t
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.invVeblen₂_veblen : ∀ {o a : Ordinal.{u}}, o ≠ 0 → a < Ordinal.veblen o a → (Ordinal.veblen o a).invVeblen₂ = a
-- Batteries.Data.Fin.Fold
Fin.dfoldr_eq_foldr : ∀ {n : ℕ} {α : Type u_1} (f : Fin n → α → α) (x : α), Fin.dfoldr n (fun x => α) f x = Fin.foldr n f x
-- Lean.Parser.Do
/-- `unless e do s` is a nicer way to write `if !e do s`.  -/
Lean.Parser.Term.termUnless : Lean.Parser.Parser
-- Mathlib.Topology.MetricSpace.Algebra
dist_smul_pair : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : Zero α]
  [inst_3 : Zero β] [inst_4 : SMul α β] [IsBoundedSMul α β] (x : α) (y₁ y₂ : β),
  dist (x • y₁) (x • y₂) ≤ dist x 0 * dist y₁ y₂
-- Mathlib.Algebra.Group.Shrink
Shrink.instGroup.eq_1 : ∀ {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : Group α], Shrink.instGroup = (equivShrink α).symm.group
-- Mathlib.Data.Finsupp.SMul
/-- See note [partially-applied ext lemmas].  -/
Finsupp.distribMulActionHom_ext' : ∀ {α : Type u_1} {M : Type u_3} {N : Type u_4} {R : Type u_6} [inst : Monoid R] [inst_1 : AddMonoid M]
  [inst_2 : AddMonoid N] [inst_3 : DistribMulAction R M] [inst_4 : DistribMulAction R N] {f g : (α →₀ M) →+[R] N},
  (∀ (a : α), f.comp (Finsupp.DistribMulActionHom.single a) = g.comp (Finsupp.DistribMulActionHom.single a)) → f = g
-- Lean.ToExpr
_private.Lean.ToExpr.0.Lean.Name.toExprAux.mkStr : Lean.Name → ℕ → Array Lean.Expr → Lean.Expr
-- Mathlib.Order.Defs.LinearOrder
min_comm : ∀ {α : Type u_1} [inst : LinearOrder α] (a b : α), min a b = min b a
-- Mathlib.Data.List.Sort
OrderIso.sortedLT_listMap : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β) {l : List α},
  (List.map (⇑e) l).SortedLT ↔ l.SortedLT
-- Lean.Compiler.IR.Basic
/-- Given `x : [t]object`, obtain the scalar value.  -/
Lean.IR.Expr.unbox : Lean.IR.VarId → Lean.IR.Expr
-- Mathlib.Computability.RegularExpressions
_private.Mathlib.Computability.RegularExpressions.0.RegularExpression.deriv.match_1.splitter : {α : Type u_1} →
  (motive : RegularExpression α → α → Sort u_2) →
    (x : RegularExpression α) →
      (x_1 : α) →
        ((x : α) → motive RegularExpression.zero x) →
          ((x : α) → motive RegularExpression.epsilon x) →
            ((a₁ a₂ : α) → motive (RegularExpression.char a₁) a₂) →
              ((P Q : RegularExpression α) → (a : α) → motive (P.plus Q) a) →
                ((P Q : RegularExpression α) → (a : α) → motive (P.comp Q) a) →
                  ((P : RegularExpression α) → (a : α) → motive P.star a) → motive x x_1
-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.SplitIterator.finitenessRelation : {ρ : Type} →
  {σ : String.Slice → Type} →
    [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] →
      {pat : ρ} →
        [inst_1 : String.Slice.Pattern.ToForwardSearcher pat σ] →
          {s : String.Slice} →
            [Std.Iterators.Finite (σ s) Id] → Std.Iterators.FinitenessRelation (String.Slice.SplitIterator pat s) Id
-- Mathlib.Algebra.ContinuedFractions.Basic
/-- Returns the next numerator `Aₙ = bₙ₋₁ * Aₙ₋₁ + aₙ₋₁ * Aₙ₋₂`, where `predA` is `Aₙ₋₁`,
`ppredA` is `Aₙ₋₂`, `a` is `aₙ₋₁`, and `b` is `bₙ₋₁`.
 -/
GenContFract.nextNum : {K : Type u_2} → [DivisionRing K] → K → K → K → K → K
-- Mathlib.Data.Set.Countable
Set.countable_empty : ∀ {α : Type u}, ∅.Countable
-- Lean.Server.ServerTask
Lean.Server.ServerTask.bindCheap : {α : Type u_1} → {β : Type u_2} → Lean.Server.ServerTask α → (α → Lean.Server.ServerTask β) → Lean.Server.ServerTask β
-- Mathlib.CategoryTheory.Sums.Basic
CategoryTheory.Functor.inrCompSum'_inv_app : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A C)
  (G : CategoryTheory.Functor B C) (X : B),
  (F.inrCompSum' G).inv.app X = CategoryTheory.CategoryStruct.id ((F.sum' G).obj (Sum.inr X))
-- Mathlib.Data.List.Chain
List.IsChain.imp_of_mem_tail_imp : ∀ {α : Type u_1} {R S : α → α → Prop} {l : List α},
  (∀ (a b : α), a ∈ l → b ∈ l.tail → R a b → S a b) → List.IsChain R l → List.IsChain S l
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHom.coe_coe : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction R B] [inst_6 : Star B] {F : Type u_6} [inst_7 : FunLike F A B]
  [inst_8 : NonUnitalAlgHomClass F R A B] [inst_9 : StarHomClass F A B] (f : F), ⇑↑f = ⇑f
-- Mathlib.Order.MinMax
Monotone.map_max : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β} {a b : α},
  Monotone f → f (max a b) = max (f a) (f b)
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- The norm of the image after the embedding associated to `v` is equal to the norm of `v` raised
to the power of the `v`-adic valuation for integers.  -/
NumberField.FinitePlace.norm_embedding_int : ∀ (K : Type u_1) [inst : Field K] {R : Type u_2} [inst_1 : CommRing R] [inst_2 : Algebra R K]
  [inst_3 : IsDedekindDomain R] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  [inst_5 : Module.Finite ℤ R] [inst_6 : Module.Free ℤ R] (x : R),
  ‖(NumberField.FinitePlace.embedding v) ((algebraMap R K) x)‖ = ↑((WithZeroMulInt.toNNReal ⋯) (v.intValuation x))
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
/-- Technical lemma used in the proof of `hasFTaylorSeriesUpTo_iteratedFDeriv`, to compare sums
over embedding of `Fin k` and `Fin (k + 1)`.  -/
_private.Mathlib.Analysis.Calculus.FDeriv.Analytic.0.Equiv.succ_embeddingFinSucc_fst_symm_apply : ∀ {ι : Type u_4} [inst : DecidableEq ι] {n : ℕ} (e : Fin (n + 1) ↪ ι) {k : ι}
  (h'k : k ∈ Set.range ⇑((Equiv.embeddingFinSucc n ι) e).fst) (hk : k ∈ Set.range ⇑e),
  (((Equiv.embeddingFinSucc n ι) e).fst.toEquivRange.symm ⟨k, h'k⟩).succ = e.toEquivRange.symm ⟨k, hk⟩
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.instAddCommMonoidWithOne : {R : Type u_1} → {a b : R} → [AddCommMonoidWithOne R] → AddCommMonoidWithOne (QuadraticAlgebra R a b)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get!_union_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} [inst_1 : Inhabited (β k)], k ∉ t₁ → (t₁ ∪ t₂).get! k = t₂.get! k
-- Init.Data.Rat.Lemmas
Rat.sub_eq_add_neg : ∀ (a b : ℚ), a - b = a + -b
-- Mathlib.Data.Finset.Fold
/-- A stronger version of `Finset.fold_ite`, but relies on
an explicit proof of idempotency on the seed element, rather
than relying on typeclass idempotency over the whole type.  -/
Finset.fold_ite' : ∀ {α : Type u_1} {β : Type u_2} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op] {f : α → β} {b : β}
  {s : Finset α} {g : α → β},
  op b b = b →
    ∀ (p : α → Prop) [inst : DecidablePred p],
      Finset.fold op b (fun i => if p i then f i else g i) s =
        op (Finset.fold op b f (Finset.filter p s)) (Finset.fold op b g ({i ∈ s | ¬p i}))
-- Mathlib.Data.List.Palindrome
List.Palindrome.reverse_eq : ∀ {α : Type u_1} {l : List α}, l.Palindrome → l.reverse = l
-- Mathlib.CategoryTheory.CopyDiscardCategory.Widesubcategory
/-- A braided-stable morphism property stable under comonoid counit and comultiplication.  -/
CategoryTheory.MorphismProperty.IsStableUnderComonoid : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      CategoryTheory.MorphismProperty C → (c : C) → [CategoryTheory.ComonObj c] → Prop
-- Mathlib.AlgebraicGeometry.Morphisms.Finite
AlgebraicGeometry.IsFinite.SpecMap_iff : ∀ {R S : CommRingCat} (f : R ⟶ S),
  AlgebraicGeometry.IsFinite (AlgebraicGeometry.Spec.map f) ↔ (CommRingCat.Hom.hom f).Finite
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.coe_opensRestrict_symm_apply : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens) (a : { V // V ≤ U }),
  ↑((AlgebraicGeometry.opensRestrict U).symm a) = ⇑U.ι ⁻¹' ↑↑((Equiv.subtypeEquivProp ⋯).symm a)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.IsBridge.eq_1 : ∀ {V : Type u} (G : SimpleGraph V) (e : Sym2 V),
  G.IsBridge e = Sym2.lift ⟨fun v w => ¬(G.deleteEdges {e}).Reachable v w, ⋯⟩ e
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullback.lift_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  [inst_1 : CategoryTheory.Limits.HasPullback f g] (h : W ⟶ X) (k : W ⟶ Y)
  (w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.lift h k w)
      (CategoryTheory.Limits.pullback.snd f g) =
    k
-- Mathlib.Order.Hom.Lattice
InfHom.coe_id : ∀ (α : Type u_2) [inst : Min α], ⇑(InfHom.id α) = id
-- Mathlib.NumberTheory.Niven
/-- `2 sin(q * π)` for `q : ℚ` is integral over `ℤ`, using the real `sin` function.  -/
Real.isIntegral_two_mul_sin_rat_mul_pi : ∀ (q : ℚ), IsIntegral ℤ (2 * Real.sin (↑q * Real.pi))
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.ofCoeff_neg : ∀ {k : Type u_1} {G : Type u_2} [inst : AddGroup k] {a : G →₀ k}, { coeff := -a } = -{ coeff := a }
-- Init.Data.SInt.Lemmas
Int8.ofInt_add : ∀ (a b : ℤ), Int8.ofInt (a + b) = Int8.ofInt a + Int8.ofInt b
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
/-- `CohomologyClass K L m` identifies to the cohomology of the complex `HomComplex K L`
in degree `m`.  -/
CochainComplex.HomComplex.leftHomologyData : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (K L : CochainComplex C ℤ) → (n : ℤ) → (HomologicalComplex.sc (K.HomComplex L) n).LeftHomologyData
-- Init.Data.BitVec.Lemmas
BitVec.toNat_sub_of_not_usubOverflow : ∀ {w : ℕ} {x y : BitVec w}, ¬x.usubOverflow y = true → (x - y).toNat = x.toNat - y.toNat
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- If `α` and `β` are arbitrary types and there is a surjection between them,
then the induced map on their free groups is also surjective.  -/
FreeGroup.map_surjective : ∀ {α : Type u} {β : Type v} {f : α → β}, Function.Surjective f → Function.Surjective ⇑(FreeGroup.map f)
-- Mathlib.Data.Matrix.Diagonal
Matrix.instAddMonoidWithOne : {n : Type u_3} → {α : Type v} → [DecidableEq n] → [AddMonoidWithOne α] → AddMonoidWithOne (Matrix n n α)
-- Lean.Elab.Tactic.Rewrite
_private.Lean.Elab.Tactic.Rewrite.0.Lean.Elab.Tactic.instEvalExprConfig : Lean.Elab.ConfigEval.EvalExpr Lean.Meta.Rewrite.Config
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instCommMonoid : {α : Type u_1} → [CommMonoid α] → CommMonoid (Lex α)
-- Mathlib.Analysis.Normed.Group.Pointwise
neg_thickening : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (δ : ℝ) (s : Set E),
  -Metric.thickening δ s = Metric.thickening δ (-s)
-- Mathlib.Order.Filter.Pointwise
/-- The inverse of a filter is the pointwise preimage under `⁻¹` of its sets.  -/
Filter.instInv : {α : Type u_2} → [Inv α] → Inv (Filter α)
-- Mathlib.FieldTheory.RatFunc.Basic
/-- The zero rational function.  -/
RatFunc.zero : {K : Type u_1} → [inst : CommRing K] → RatFunc K
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.removeLoops_restrict_eq_restrict : ∀ {α : Type u_1} {M : Matroid α} {X : Set α}, X ⊆ {e | M.IsNonloop e} → M.removeLoops.restrict X = M.restrict X
-- Lean.Elab.InfoTree.Types
Lean.Elab.CompletionInfo.dot.sizeOf_spec : ∀ (termInfo : Lean.Elab.TermInfo) (expectedType? : Option Lean.Expr),
  sizeOf (Lean.Elab.CompletionInfo.dot termInfo expectedType?) = 1 + sizeOf termInfo + sizeOf expectedType?
-- Mathlib.Analysis.Calculus.FDeriv.CompCLM
HasStrictFDerivAt.clm_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {x : E} {H : Type u_5} [inst_7 : NormedAddCommGroup H]
  [inst_8 : NormedSpace 𝕜 H] {c : E → G →L[𝕜] H} {c' : E →L[𝕜] G →L[𝕜] H} {d : E → F →L[𝕜] G} {d' : E →L[𝕜] F →L[𝕜] G},
  HasStrictFDerivAt c c' x →
    HasStrictFDerivAt d d' x →
      HasStrictFDerivAt (fun y => c y ∘SL d y)
        ((ContinuousLinearMap.compL 𝕜 F G H) (c x) ∘SL d' + (ContinuousLinearMap.compL 𝕜 F G H).flip (d x) ∘SL c') x
-- Mathlib.Analysis.InnerProductSpace.Projection.Minimal
/-- Characterization of minimizers in the projection on a subspace.
Let `u` be a point in an inner product space, and let `K` be a nonempty subspace.
Then point `v` minimizes the distance `‖u - v‖` over points in `K` if and only if
for all `w ∈ K`, `⟪u - v, w⟫ = 0` (i.e., `u - v` is orthogonal to the subspace `K`)
 -/
Submodule.norm_eq_iInf_iff_inner_eq_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) {u v : E}, v ∈ K → (‖u - v‖ = ⨅ w, ‖u - ↑w‖ ↔ ∀ w ∈ K, inner 𝕜 (u - v) w = 0)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Real.hasStrictDerivAt_tan : ∀ {x : ℝ}, Real.cos x ≠ 0 → HasStrictDerivAt Real.tan (1 / Real.cos x ^ 2) x
-- Lean.Meta.Tactic.Grind.Attr
/-- Return theorem kind for `stx` of the form `(Attr.grindMod)?`  -/
Lean.Meta.Grind.getAttrKindFromOpt : Lean.Syntax → Lean.CoreM Lean.Meta.Grind.AttrKind
-- Mathlib.LinearAlgebra.TensorProduct.RightExactness
/-- For a surjective `f : N →ₗ[R] P`,
the natural equivalence between `Q ⊗ N ⧸ (image of ker f)` to `Q ⊗ P`
(computably, given a right inverse)  -/
lTensor.linearEquiv_of_rightInverse : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      {P : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : AddCommGroup N] →
              [inst_3 : AddCommGroup P] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : Module R P] →
                      {f : M →ₗ[R] N} →
                        {g : N →ₗ[R] P} →
                          (Q : Type u_5) →
                            [inst_7 : AddCommGroup Q] →
                              [inst_8 : Module R Q] →
                                Function.Exact ⇑f ⇑g →
                                  {h : P → N} →
                                    Function.RightInverse h ⇑g →
                                      (TensorProduct R Q N ⧸ (LinearMap.lTensor Q f).range) ≃ₗ[R] TensorProduct R Q P
-- Init.Data.Nat.Lemmas
Nat.dvd_sub_mod : ∀ {n : ℕ} (k : ℕ), n ∣ k - k % n