mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.QuotSMulTop
QuotSMulTop.map_apply_mk : ∀ {R : Type u_2} [inst : CommRing R] (r : R) {M : Type u_1} {M' : Type u_3} [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup M'] [inst_4 : Module R M'] (f : M →ₗ[R] M') (x : M),
  ((QuotSMulTop.map r) f) (Submodule.Quotient.mk x) = Submodule.Quotient.mk (f x)
-- Mathlib.RingTheory.RingHomProperties
RingHom.IsStableUnderBaseChange.and : ∀ {P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => P) →
    (RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => Q) →
      RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] f => P f ∧ Q f
-- Mathlib.Data.Set.Countable
Set.Countable.of_subsingleton : ∀ {α : Type u} [Subsingleton α] (s : Set α), s.Countable
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.mem_indepSetSet_iff : ∀ {α : Type u_1} {G : SimpleGraph α} {n : ℕ} {s : Finset α}, s ∈ G.indepSetSet n ↔ G.IsNIndepSet n s
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
HasFTaylorSeriesUpToOn.of_le : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {m n : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F},
  HasFTaylorSeriesUpToOn n f p s → m ≤ n → HasFTaylorSeriesUpToOn m f p s
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.coeIdeal_ne_zero' : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  [loc : IsLocalization S P] {I : Ideal R}, S ≤ nonZeroDivisors R → (↑I ≠ 0 ↔ I ≠ ⊥)
-- Mathlib.Logic.Basic
if_congr : ∀ {α : Sort u_1} {P Q : Prop} [inst : Decidable P] [inst_1 : Decidable Q] {x y u v : α},
  (P ↔ Q) → x = u → y = v → (if P then x else y) = if Q then u else v
-- Mathlib.Tactic.FunProp.Types
Mathlib.Meta.FunProp.GeneralTheorems.mk.injEq : ∀ (theorems theorems_1 : Lean.Meta.RefinedDiscrTree Mathlib.Meta.FunProp.GeneralTheorem),
  ({ theorems := theorems } = { theorems := theorems_1 }) = (theorems = theorems_1)
-- Std.Async.Signal
/-- Virtual alarm clock.
 -/
Std.Async.Signal.sigvtalrm : Std.Async.Signal
-- Mathlib.Algebra.Group.Ideal
SemigroupIdeal.fg_iff : ∀ {M : Type u_1} [inst : Mul M] {I : SemigroupIdeal M}, I.FG ↔ ∃ s, I = SemigroupIdeal.closure ↑s
-- Init.Grind.AC
Lean.Grind.AC.Seq.unionFuel.match_1.congr_eq_3 : ∀ (motive : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Sort u_1) (s₁ s₂ : Lean.Grind.AC.Seq)
  (h_1 : (x₁ x₂ : Lean.Grind.AC.Var) → motive (Lean.Grind.AC.Seq.var x₁) (Lean.Grind.AC.Seq.var x₂))
  (h_2 :
    (x₁ x : Lean.Grind.AC.Var) →
      (s : Lean.Grind.AC.Seq) → motive (Lean.Grind.AC.Seq.var x₁) (Lean.Grind.AC.Seq.cons x s))
  (h_3 :
    (x : Lean.Grind.AC.Var) →
      (s : Lean.Grind.AC.Seq) →
        (x₂ : Lean.Grind.AC.Var) → motive (Lean.Grind.AC.Seq.cons x s) (Lean.Grind.AC.Seq.var x₂))
  (h_4 :
    (x₁ : Lean.Grind.AC.Var) →
      (s₁ : Lean.Grind.AC.Seq) →
        (x₂ : Lean.Grind.AC.Var) →
          (s₂ : Lean.Grind.AC.Seq) → motive (Lean.Grind.AC.Seq.cons x₁ s₁) (Lean.Grind.AC.Seq.cons x₂ s₂))
  (x : Lean.Grind.AC.Var) (s : Lean.Grind.AC.Seq) (x₂ : Lean.Grind.AC.Var),
  s₁ = Lean.Grind.AC.Seq.cons x s →
    s₂ = Lean.Grind.AC.Seq.var x₂ →
      (match s₁, s₂ with
        | Lean.Grind.AC.Seq.var x₁, Lean.Grind.AC.Seq.var x₂ => h_1 x₁ x₂
        | Lean.Grind.AC.Seq.var x₁, Lean.Grind.AC.Seq.cons x s => h_2 x₁ x s
        | Lean.Grind.AC.Seq.cons x s, Lean.Grind.AC.Seq.var x₂ => h_3 x s x₂
        | Lean.Grind.AC.Seq.cons x₁ s₁, Lean.Grind.AC.Seq.cons x₂ s₂ => h_4 x₁ s₁ x₂ s₂) ≍
        h_3 x s x₂
-- Mathlib.Tactic.FieldSimp.Lemmas
/-- Augment a `FieldSimp.NF M` object `l`, i.e. a list of pairs in `ℤ × M`, by prepending another
pair `p : ℤ × M`.  -/
Mathlib.Tactic.FieldSimp.NF.«term_::ᵣ_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Module.Equiv.Basic
DistribMulAction.toModuleAut_apply : ∀ (R : Type u_1) {S : Type u_4} (M : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Group S] [inst_4 : DistribMulAction S M] [inst_5 : SMulCommClass S R M] (s : S),
  (DistribMulAction.toModuleAut R M) s = DistribMulAction.toLinearEquiv R M s
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- Transfer preservation of limits along a natural isomorphism in the diagram.  -/
CategoryTheory.Limits.preservesLimit_of_iso_diagram : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {K₁ K₂ : CategoryTheory.Functor J C}
  (F : CategoryTheory.Functor C D) (h : K₁ ≅ K₂) [CategoryTheory.Limits.PreservesLimit K₁ F],
  CategoryTheory.Limits.PreservesLimit K₂ F
-- Mathlib.NumberTheory.Bernoulli
bernoulli'_eq_bernoulli : ∀ (n : ℕ), bernoulli' n = (-1) ^ n * bernoulli n
-- Init.Data.BitVec.Lemmas
_private.Init.Data.BitVec.Lemmas.0.BitVec.toInt_signExtend_of_le.toInt_signExtend_of_lt : ∀ {w v : ℕ}, w ≤ v → ∀ {x : BitVec w}, w < v → (BitVec.signExtend v x).toInt = x.toInt
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.re_C : ∀ {R : Type u_1} {a b : R} (r : R) [inst : Zero R], (QuadraticAlgebra.C r).re = r
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.of_zero : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Zero α], Matrix.of 0 = 0
-- Init.Tactics
/-- Similar to `refine_lift`, but using `refine'`  -/
Lean.Parser.Tactic.tacticRefine_lift'_ : Lean.ParserDescr
-- Mathlib.Analysis.InnerProductSpace.Positive
ContinuousLinearMap.isPositive_natCast : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {n : ℕ}, (↑n).IsPositive
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
IsLUB.mul : ∀ {G : Type u_2} [inst : Group G] [inst_1 : Preorder G] [MulLeftMono G] [MulRightMono G] {s t : Set G} {a b : G},
  IsLUB s a → IsLUB t b → IsLUB (s * t) (a * b)
-- Init.Data.SInt.Bitwise
Int32.xor_comm : ∀ (a b : Int32), a ^^^ b = b ^^^ a
-- Init.Grind.ToIntLemmas
Lean.Grind.ToInt.mul_congr.ww : ∀ {α : Type u_1} {i : Lean.Grind.IntInterval} [inst : Lean.Grind.ToInt α i] [inst_1 : Mul α] [Lean.Grind.ToInt.Mul α i],
  i.isFinite = true → ∀ {a b : α} {a' b' : ℤ}, ↑a = i.wrap a' → ↑b = i.wrap b' → ↑(a * b) = i.wrap (a' * b')
-- Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Polynomial.IsMonicOfDegree.add_left : ∀ {R : Type u_1} [inst : Semiring R] {p q : Polynomial R} {n : ℕ},
  p.natDegree < n → q.IsMonicOfDegree n → (p + q).IsMonicOfDegree n
-- Mathlib.Topology.NhdsWithin
tendsto_nhds_of_tendsto_nhdsWithin : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : β → α} {a : α} {s : Set α} {l : Filter β},
  Filter.Tendsto f l (nhdsWithin a s) → Filter.Tendsto f l (nhds a)
-- Mathlib.Analysis.InnerProductSpace.Affine
inner_vsub_left_eq_zero_symm : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] {a b : P} {v : V},
  inner 𝕜 (a -ᵥ b) v = 0 ↔ inner 𝕜 (b -ᵥ a) v = 0
-- Mathlib.Analysis.Calculus.ContDiff.Defs
/-- A function is `C^(n + 1)` at a point iff locally, it has a derivative which is `C^n`.  -/
contDiffAt_succ_iff_hasFDerivAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} {n : ℕ},
  ContDiffAt 𝕜 (↑n + 1) f x ↔ ∃ f', (∃ u ∈ nhds x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt 𝕜 (↑n) f' x
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.map_id : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α}, Filter.Germ.map id = id
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
MeasureTheory.condExpIndSMul_ae_eq_smul : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {s : Set α} [inst_1 : NormedSpace ℝ G] (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : G),
  ↑↑(MeasureTheory.condExpIndSMul hm hs hμs x) =ᵐ[μ] fun a =>
    ↑↑↑((MeasureTheory.condExpL2 ℝ ℝ hm) (MeasureTheory.indicatorConstLp 2 hs hμs 1)) a • x
-- Mathlib.CategoryTheory.ComposableArrows.Basic
_private.Mathlib.CategoryTheory.ComposableArrows.Basic.0.CategoryTheory.ComposableArrows.Mk₁.map.match_1.eq_3 : ∀ (motive : (x x_1 : Fin 2) → x ≤ x_1 → Sort u_1) (isLt isLt_1 : 1 < 2) (x : ⟨1, isLt⟩ ≤ ⟨1, isLt_1⟩)
  (h_1 : (isLt isLt_2 : 0 < 2) → (x : ⟨0, isLt⟩ ≤ ⟨0, isLt_2⟩) → motive ⟨0, isLt⟩ ⟨0, isLt_2⟩ x)
  (h_2 : (isLt : 0 < 2) → (isLt_2 : 1 < 2) → (x : ⟨0, isLt⟩ ≤ ⟨1, isLt_2⟩) → motive ⟨0, isLt⟩ ⟨1, isLt_2⟩ x)
  (h_3 : (isLt isLt_2 : 1 < 2) → (x : ⟨1, isLt⟩ ≤ ⟨1, isLt_2⟩) → motive ⟨1, isLt⟩ ⟨1, isLt_2⟩ x),
  (match ⟨1, isLt⟩, ⟨1, isLt_1⟩, x with
    | ⟨0, isLt⟩, ⟨0, isLt_2⟩, x => h_1 isLt isLt_2 x
    | ⟨0, isLt⟩, ⟨1, isLt_2⟩, x => h_2 isLt isLt_2 x
    | ⟨1, isLt⟩, ⟨1, isLt_2⟩, x => h_3 isLt isLt_2 x) =
    h_3 isLt isLt_1 x
-- Batteries.Data.MLList.Basic
/-- Given a lazy list in a state monad, run it on some initial state.  -/
MLList.runState' : {m : Type u → Type u} → {σ α : Type u} → [Monad m] → MLList (StateT σ m) α → σ → MLList m α
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.mem_ofList : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k : α}, k ∈ Std.HashMap.Raw.ofList l ↔ (List.map Prod.fst l).contains k = true
-- Mathlib.Topology.LocallyClosed
IsLocallyClosed.preimage : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set Y},
  IsLocallyClosed s → ∀ {f : X → Y}, Continuous f → IsLocallyClosed (f ⁻¹' s)
-- Lean.Parser.Term
Lean.Parser.Term.leading_parser.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.RingTheory.TensorProduct.MonoidAlgebra
AddMonoidAlgebra.scalarTensorEquiv.eq_1 : ∀ (R : Type u_1) {M : Type u_2} (A : Type u_5) [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  [inst_3 : AddCommMonoid M],
  AddMonoidAlgebra.scalarTensorEquiv R A =
    (AddMonoidAlgebra.rTensorEquivAlgEquiv R A A R).trans
      (AddMonoidAlgebra.mapAlgEquiv A M (Algebra.TensorProduct.rid R A A))
-- Mathlib.Algebra.Order.Interval.Basic
Interval.addZeroClass : {α : Type u_2} → [inst : AddCommMonoid α] → [inst_1 : Preorder α] → [IsOrderedAddMonoid α] → AddZeroClass (Interval α)
-- Mathlib.RingTheory.Support
Module.exists_localizedMap_away_surjective_of_localizedMap_atPrime_surjective : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [Module.Finite R M] (p : Ideal R) [inst_6 : p.IsPrime]
  (φ : N →ₗ[R] M),
  Function.Surjective ⇑((LocalizedModule.map p.primeCompl) φ) →
    ∃ a ∉ p, Function.Surjective ⇑((LocalizedModule.map (Submonoid.powers a)) φ)
-- Lean.Meta.Closure
Lean.Meta.Closure.collectExpr : Lean.Expr → Lean.Meta.Closure.ClosureM Lean.Expr
-- Mathlib.Analysis.Normed.Ring.Basic
NonUnitalNormedRing.toNonUnitalRing : {α : Type u_5} → [self : NonUnitalNormedRing α] → NonUnitalRing α
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
/-- The inverse of `c.emb` for `c : OrderedFinpartition`. It maps `j : Fin n` to the point in
`Fin (c.partSize (c.index j))` which is mapped back to `j` by `c.emb (c.index j)`.  -/
OrderedFinpartition.invEmbedding : {n : ℕ} → (c : OrderedFinpartition n) → (j : Fin n) → Fin (c.partSize (c.index j))
-- Mathlib.Order.Antichain
IsMaxAntichain.nonempty_iff : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α}, IsMaxAntichain r s → (Nonempty α ↔ s.Nonempty)
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MonotoneOn.integrableOn_of_measure_ne_top : ∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} {s : Set X} [BorelSpace X] [inst_4 : ConditionallyCompleteLinearOrder X]
  [inst_5 : ConditionallyCompleteLinearOrder E] [OrderTopology X] [OrderTopology E] [SecondCountableTopology E]
  {f : X → E},
  MonotoneOn f s →
    ∀ {a b : X}, IsLeast s a → IsGreatest s b → μ s ≠ ⊤ → MeasurableSet s → MeasureTheory.IntegrableOn f s μ
-- Std.Data.DTreeMap.Internal.Operations
/-- A tree map obtained by inserting elements into `t`, bundled with an inductive principle.  -/
Std.DTreeMap.Internal.Impl.IteratedInsertionInto : {α : Type u} → {β : α → Type v} → [Ord α] → Std.DTreeMap.Internal.Impl α β → Type (max 0 u v)
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.smul : {S : Type u_2} → {R : Type u} → {M : Type v} → [SMul S R] → [SMul S M] → SMul S (TrivSqZeroExt R M)
-- Mathlib.Analysis.Normed.Group.AddTorsor
uniformContinuous_vsub : ∀ {V : Type u_2} {P : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P], UniformContinuous fun x => x.1 -ᵥ x.2
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.IterM.fold_mapWithPostcondition : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {Pred EPred : Type w} [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_2 : Monad m] [LawfulMonad m] [inst_4 : Monad n]
  [inst_5 : Std.Internal.Do.Assertion Pred] [inst_6 : Std.Internal.Do.Assertion EPred]
  [inst_7 : Std.Internal.Do.WPMonad n Pred EPred] [inst_8 : Std.IteratorLoop α m n] [Std.LawfulIteratorLoop α m n]
  [inst_10 : MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → Std.Iterators.PostconditionT n γ} {g : δ → γ → δ}
  {init : δ} {it : Std.IterM m β} {P : Pred} {Q : δ → Pred} {eQ : EPred},
  ⦃ P ⦄
      Std.IterM.foldM
        (fun d b => do
          let c ← (f b).run
          pure (g d c))
        init it ⦃
      Q; eQ ⦄ →
    ⦃ P ⦄ Std.IterM.fold g init (Std.IterM.mapWithPostcondition f it) ⦃ Q; eQ ⦄
-- Mathlib.CategoryTheory.GradedObject.Monoidal
/-- Given four graded objects, this is the condition
`HasLeftTensor₃ObjExt (X₁ i₁) X₂ X₃ X₄ i₂₃₄` for all indices `i₁` and `i₂₃₄`,
see the lemma `tensorObj₄_ext`.  -/
CategoryTheory.GradedObject.HasTensor₄ObjExt : {I : Type u} →
  [AddMonoid I] →
    {C : Type u_1} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [CategoryTheory.MonoidalCategory C] →
          CategoryTheory.GradedObject I C →
            CategoryTheory.GradedObject I C → CategoryTheory.GradedObject I C → CategoryTheory.GradedObject I C → Prop
-- Mathlib.GroupTheory.Subsemigroup.Centralizer
/-- If all the elements of a set `s` commute, then `closure s` is commutative.  -/
AddSubsemigroup.isAddCommutative_closure : ∀ (M : Type u_1) [inst : AddSemigroup M] {s : Set M},
  (∀ a ∈ s, ∀ b ∈ s, a + b = b + a) → IsAddCommutative ↥(AddSubsemigroup.closure s)
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.single_mono : ∀ {I : Type u} {f : I → Type v} (i : I) [inst : DecidableEq I] [inst_1 : (i : I) → Preorder (f i)]
  [inst_2 : (i : I) → Zero (f i)], Monotone (Pi.single i)
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.cons_eq_smul : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] [inst_1 : DecidableEq ι]
  [inst_2 : (i : ι) → DecidableEq (M i)] {i : ι} {m : M i} {ls : Monoid.CoprodI.Word M} {h1 : ls.fstIdx ≠ some i}
  {h2 : m ≠ 1}, Monoid.CoprodI.Word.cons m ls h1 h2 = Monoid.CoprodI.of m • ls
-- Mathlib.Analysis.Calculus.DiffContOnCl
Differentiable.diffContOnCl : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E},
  Differentiable 𝕜 f → DiffContOnCl 𝕜 f s
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
AffineSubspace.coe_eq_univ_iff : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] (Q : AffineSubspace k P), ↑Q = Set.univ ↔ Q = ⊤
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.BlastDivSubtractShiftOutput.aig : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {old : Std.Sat.AIG α} →
        {w : ℕ} → Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.BlastDivSubtractShiftOutput old w → Std.Sat.AIG α
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Polynomial.instAlgebraUniversalFactorizationRing : {R : Type u_1} →
  [inst : CommRing R] →
    {n : ℕ} →
      (m k : ℕ) →
        (hn : n = m + k) →
          (p : Polynomial.MonicDegreeEq R n) → Algebra R (Polynomial.UniversalFactorizationRing m k hn p)
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_updateFinset_left : ∀ {δ : Type u_4} {X : δ → Type u_6} [inst : (a : δ) → MeasurableSpace (X a)] [inst_1 : DecidableEq δ] {s : Finset δ}
  {x : (i : ↥s) → X ↑i}, Measurable fun x_1 => Function.updateFinset x_1 s x
-- Mathlib.Topology.Constructions
isClosed_preimage_val : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsClosed (Subtype.val ⁻¹' t) ↔ s ∩ closure (s ∩ t) ⊆ t
-- Std.Http.Protocol.H1.Writer
/-- Writes the final chunk terminator (0\r\n\r\n) and transitions to complete state.
 -/
Std.Http.Protocol.H1.Writer.writeFinalChunk : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Writer dir → Std.Http.Protocol.H1.Writer dir
-- Mathlib.Algebra.AddConstMap.Equiv
AddConstEquiv.refl_toEquiv : ∀ {G : Type u_1} [inst : Add G] (a : G), (AddConstEquiv.refl a).toEquiv = Equiv.refl G
-- Lean.Elab.DocString
/-- The local instances.

The `MonadLift TermElabM DocM` instance runs the lifted action with these instances, so elaboration
commands that mutate this state cause it to take effect in subsequent commands.
 -/
Lean.Doc.State.localInstances : Lean.Doc.State → Lean.LocalInstances
-- Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
/-- If a set `s` is a neighborhood of `x`, then there exists a smooth function `f` taking
values in `[0, 1]`, supported in `s` and with `f x = 1`.  -/
exists_contDiff_tsupport_subset : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {x : E}
  {n : ℕ∞},
  s ∈ nhds x → ∃ f, tsupport f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ (↑n) f ∧ Set.range f ⊆ Set.Icc 0 1 ∧ f x = 1
-- Mathlib.RingTheory.Polynomial.Hermite.Basic
Polynomial.hermite.eq_1 : Polynomial.hermite 0 = 1
-- Std.Time.Duration
Std.Time.Duration.mk : (second : Std.Time.Second.Offset) →
  (nano : Std.Time.Nanosecond.Span) → second.val ≥ 0 ∧ ↑nano ≥ 0 ∨ second.val ≤ 0 ∧ ↑nano ≤ 0 → Std.Time.Duration
-- Init.Prelude
Pi.instInhabited : {α : Sort u} → {β : α → Sort v} → [(a : α) → Inhabited (β a)] → Inhabited ((a : α) → β a)
-- Mathlib.FieldTheory.Finiteness
IsNoetherian.range_finsetBasis : ∀ (K : Type u) (V : Type v) [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : IsNoetherian K V], Set.range ⇑(IsNoetherian.finsetBasis K V) = Module.Basis.ofVectorSpaceIndex K V
-- Mathlib.Analysis.Convex.SimplicialComplex.Basic
Geometry.SimplicialComplex.mem_facets : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] {K : Geometry.SimplicialComplex 𝕜 E} {s : Finset E},
  s ∈ K.facets ↔ s ∈ K.faces ∧ ∀ t ∈ K.faces, s ⊆ t → s = t
-- Lean.Meta.Tactic.Grind.Types
/-- Forall-propagator.  -/
Lean.Meta.Grind.SplitSource.forallProp : Lean.Expr → Lean.Meta.Grind.SplitSource
-- Lean.Meta.Basic
/-- `withLCtx lctx localInsts k` replaces the local context and local instances, and then executes `k`.
The local context and instances are restored after executing `k`.
This method assumes that the local instances in `localInsts` are in the local context `lctx`.
 -/
Lean.Meta.withLCtx : {n : Type → Type u_1} →
  [MonadControlT Lean.MetaM n] → [Monad n] → {α : Type} → Lean.LocalContext → Lean.LocalInstances → n α → n α
-- Mathlib.Algebra.GroupWithZero.Equiv
MulEquiv.toMonoidWithZeroHom_bijective : ∀ {G : Type u_1} {H : Type u_2} [inst : MulZeroOneClass G] [inst_1 : MulZeroOneClass H] (f : G ≃* H),
  Function.Bijective ⇑f.toMonoidWithZeroHom
-- Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes
Mathlib.Tactic.Bicategory.structuralIsoOfExpr_whiskerLeft : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h) (η' : g ≅ h),
  η'.hom = η → (CategoryTheory.Bicategory.whiskerLeftIso f η').hom = CategoryTheory.Bicategory.whiskerLeft f η
-- Lean.Meta.Tactic.Grind.EMatch
/-- Partial assignment so far. Recall that pattern variables are encoded as de-Bruijn variables.  -/
Lean.Meta.Grind.EMatch.Choice.assignment : Lean.Meta.Grind.EMatch.Choice → Array Lean.Expr
-- Mathlib.Topology.Defs.Filter
/-- In a locally compact space,
every neighbourhood of every point contains a compact neighbourhood of that same point.  -/
LocallyCompactSpace.local_compact_nhds : ∀ {X : Type u_3} {inst : TopologicalSpace X} [self : LocallyCompactSpace X] (x : X),
  ∀ n ∈ nhds x, ∃ s ∈ nhds x, s ⊆ n ∧ IsCompact s
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Bicategory.rightZigzagIso_hom : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {a b : B} {f : a ⟶ b} {g : b ⟶ a}
  (η : CategoryTheory.CategoryStruct.id a ≅ CategoryTheory.CategoryStruct.comp f g)
  (ε : CategoryTheory.CategoryStruct.comp g f ≅ CategoryTheory.CategoryStruct.id b),
  (CategoryTheory.Bicategory.rightZigzagIso η ε).hom = CategoryTheory.Bicategory.rightZigzag η.hom ε.hom
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.norm_condExpIndL1_le : ∀ {α : Type u_1} {G : Type u_4} [inst : NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {s : Set α} [inst_1 : NormedSpace ℝ G] {hm : m ≤ m0} [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)] (x : G),
  ‖MeasureTheory.condExpIndL1 hm μ s x‖ ≤ μ.real s * ‖x‖
-- Mathlib.Analysis.Calculus.Deriv.MeanValue
/-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
of the real line. If `f` is differentiable on the interior of `D` and `f'` is strictly positive,
then `f` is a strictly monotone function on `D`.  -/
strictMonoOn_of_hasDerivWithinAt_pos : ∀ {D : Set ℝ},
  Convex ℝ D →
    ∀ {f f' : ℝ → ℝ},
      ContinuousOn f D →
        (∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x) → (∀ x ∈ interior D, 0 < f' x) → StrictMonoOn f D
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
CochainComplex.isSplitEpi_to_singleFunctor_obj_of_projective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P : C}
  [CategoryTheory.Projective P] {K : CochainComplex C ℤ} {i : ℤ} (π : K ⟶ (CochainComplex.singleFunctor C i).obj P)
  [K.IsStrictlyLE i] [QuasiIsoAt π i], CategoryTheory.IsSplitEpi π
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.rightKanExtensionUniqueOfIso_hom : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : L.comp F' ⟶ F) [inst_3 : F'.IsRightKanExtension α] {G : CategoryTheory.Functor C H} (i : F ≅ G)
  (G' : CategoryTheory.Functor D H) (β : L.comp G' ⟶ G) [inst_4 : G'.IsRightKanExtension β],
  (F'.rightKanExtensionUniqueOfIso α i G' β).hom =
    G'.liftOfIsRightKanExtension β F' (CategoryTheory.CategoryStruct.comp α i.hom)
-- Mathlib.Topology.MetricSpace.CantorScheme
/-- A scheme with vanishing diameter along each branch induces a continuous map.  -/
CantorScheme.VanishingDiam.map_continuous : ∀ {β : Type u_1} {α : Type u_2} {A : List β → Set α} [inst : PseudoMetricSpace α] [inst_1 : TopologicalSpace β]
  [DiscreteTopology β], CantorScheme.VanishingDiam A → Continuous (CantorScheme.inducedMap A).snd
-- Mathlib.Algebra.Torsor.Defs
AddTorsor.mk : {G : outParam (Type u_1)} →
  {P : Type u_2} →
    [inst : AddGroup G] →
      [toAddAction : AddAction G P] →
        [toVSub : VSub G P] →
          [nonempty : Nonempty P] →
            (∀ (p₁ p₂ : P), (p₁ -ᵥ p₂) +ᵥ p₂ = p₁) → (∀ (g : G) (p : P), (g +ᵥ p) -ᵥ p = g) → AddTorsor G P