mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Tactic.Instances
/-- `#instances term` prints all the instances for the given class.
For example, `#instances Add _` gives all `Add` instances, and `#instances Add Nat` gives the
`Nat` instance. The `term` can be any type that can appear in `[...]` binders.

Trailing underscores can be omitted, and `#instances Add` and `#instances Add _` are equivalent;
the command adds metavariables until the argument is no longer a function.

The `#instances` command is closely related to `#synth`, but `#synth` does the full
instance synthesis algorithm and `#instances` does the first step of finding potential instances.  -/
Batteries.Tactic.Instances.«command#instances__:_» : Lean.ParserDescr
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.IsImage.inter_eq_of_inter_eq_of_eqOn : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} {e' : OpenPartialHomeomorph X Y},
  e.IsImage s t →
    e'.IsImage s t → e.source ∩ s = e'.source ∩ s → Set.EqOn (↑e) (↑e') (e.source ∩ s) → e.target ∩ t = e'.target ∩ t
-- Mathlib.Order.Max
Prod.isMax_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {x : α × β}, IsMax x ↔ IsMax x.1 ∧ IsMax x.2
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
MeasurableSet.sep_finite : ∀ {α : Type u_1} [Countable α] {S : Set (Set α)}, MeasurableSet S → MeasurableSet {s | s ∈ S ∧ s.Finite}
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.leadingCoeff_X_pow_sub_C : ∀ {R : Type u} [inst : Ring R] {n : ℕ}, 0 < n → ∀ {r : R}, (Polynomial.X ^ n - Polynomial.C r).leadingCoeff = 1
-- Mathlib.AlgebraicGeometry.Group.Affine
/-- `Spec` as a functor from `R`-algebras to schemes over `Spec R`.  -/
AlgebraicGeometry.algSpec : (R : CommRingCat) → CategoryTheory.Functor (CommAlgCat ↑R)ᵒᵖ (CategoryTheory.Over (AlgebraicGeometry.Spec R))
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.getKeyGT!_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α}, t₁.Equiv t₂ → t₁.getKeyGT! k = t₂.getKeyGT! k
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.smulCommClass : ∀ {T : Type u_1} {S : Type u_2} {R : Type u} {M : Type v} [inst : SMul T R] [inst_1 : SMul T M] [inst_2 : SMul S R]
  [inst_3 : SMul S M] [SMulCommClass T S R] [SMulCommClass T S M], SMulCommClass T S (TrivSqZeroExt R M)
-- Mathlib.Topology.ContinuousMap.Units
ContinuousMap.spectrum_eq_range : ∀ {X : Type u_1} {𝕜 : Type u_4} [inst : TopologicalSpace X] [inst_1 : NormedField 𝕜] [CompleteSpace 𝕜] (f : C(X, 𝕜)),
  spectrum 𝕜 f = Set.range ⇑f
-- Mathlib.Data.List.Rotate
List.rotate'_length : ∀ {α : Type u} (l : List α), l.rotate' l.length = l
-- Std.Internal.UV.System
Std.Internal.UV.System.PasswdInfo.homedir : Std.Internal.UV.System.PasswdInfo → Option String
-- Mathlib.Analysis.Convex.Side
AffineSubspace.SSameSide.trans_wOppSide : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y z : P}, s.SSameSide x y → s.WOppSide y z → s.WOppSide x z
-- Init.Data.Nat.Basic
Nat.lt_succ_of_lt : ∀ {a b : ℕ}, a < b → a < b.succ
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.isRadical_vanishingIdeal : ∀ {R : Type u} [inst : CommSemiring R] (s : Set (PrimeSpectrum R)), (PrimeSpectrum.vanishingIdeal s).IsRadical
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
/-- `SeparationQuotient.mk` as an `AddMonoidHom`.  -/
SeparationQuotient.mkAddMonoidHom : {M : Type u_1} →
  [inst : TopologicalSpace M] → [inst_1 : AddZeroClass M] → [inst_2 : ContinuousAdd M] → M →+ SeparationQuotient M
-- Mathlib.Analysis.Calculus.SmoothSeries
/-- Consider a series of smooth functions, with summable uniform bounds on the successive
derivatives. Then the iterated derivative of the sum is the sum of the iterated derivative.  -/
iteratedFDeriv_tsum_apply : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedAddCommGroup F] [CompleteSpace F]
  [inst_6 : NormedSpace 𝕜 F] {f : α → E → F} {v : ℕ → α → ℝ} {N : ℕ∞},
  (∀ (i : α), ContDiff 𝕜 (↑N) (f i)) →
    (∀ (k : ℕ), ↑k ≤ N → Summable (v k)) →
      (∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i) →
        ∀ {k : ℕ},
          ↑k ≤ N → ∀ (x : E), iteratedFDeriv 𝕜 k (fun y => ∑' (n : α), f n y) x = ∑' (n : α), iteratedFDeriv 𝕜 k (f n) x
-- Mathlib.Combinatorics.SimpleGraph.VertexCover
SimpleGraph.vertexCoverNum_lt_card : ∀ {V : Type u_1} {G : SimpleGraph V} [Nonempty V] [Finite V], G.vertexCoverNum < ENat.card V
-- Mathlib.Algebra.DirectSum.Module
DirectSum.isInternal_ne_bot_iff : ∀ {R : Type u} [inst : Ring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] {A : ι → Submodule R M}, (DirectSum.IsInternal fun i => A ↑i) ↔ DirectSum.IsInternal A
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getD_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Option γ} {k : α} {fallback : γ},
  (Std.ExtTreeMap.filterMap f t).getD k fallback = (t[k]?.pbind fun x h' => f (t.getKey k ⋯) x).getD fallback
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.rename_surjective : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] (f : σ → τ),
  Function.Surjective f → Function.Surjective ⇑(MvPolynomial.rename f)
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.disjoint_withBotCoe : ∀ {ι : Type u_1} {I J : WithBot (BoxIntegral.Box ι)}, Disjoint ↑I ↑J ↔ Disjoint I J
-- Mathlib.Analysis.Complex.UpperHalfPlane.Topology
UpperHalfPlane.isOpenMap_norm : IsOpenMap fun τ => ‖↑τ‖
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBMap.instIsStrictCutByKeyOfTransCmp : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (cmp : β → β → Ordering) [Std.TransCmp cmp] (x : β),
  RBTree.RBNode.IsStrictCut (Ordering.byKey f cmp) fun y => cmp x (f y)
-- Mathlib.Algebra.GroupWithZero.Opposite
MulOpposite.isLeftCancelMulZero_iff : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α], IsLeftCancelMulZero αᵐᵒᵖ ↔ IsRightCancelMulZero α
-- Mathlib.Topology.Constructible
Topology.IsConstructible.sInter : ∀ {X : Type u_2} [inst : TopologicalSpace X] {S : Set (Set X)},
  S.Finite → (∀ s ∈ S, Topology.IsConstructible s) → Topology.IsConstructible (⋂₀ S)
-- Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
AbsoluteValue.IsAdmissible.mk.injEq : ∀ {R : Type u_1} [inst : EuclideanDomain R] {abv : AbsoluteValue R ℤ} (toIsEuclidean : abv.IsEuclidean) (card : ℝ → ℕ)
  (exists_partition' :
    ∀ (n : ℕ) {ε : ℝ},
      0 < ε →
        ∀ {b : R},
          b ≠ 0 → ∀ (A : Fin n → R), ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑(abv (A i₁ % b - A i₀ % b)) < abv b • ε)
  (toIsEuclidean_1 : abv.IsEuclidean) (card_1 : ℝ → ℕ)
  (exists_partition'_1 :
    ∀ (n : ℕ) {ε : ℝ},
      0 < ε →
        ∀ {b : R},
          b ≠ 0 → ∀ (A : Fin n → R), ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑(abv (A i₁ % b - A i₀ % b)) < abv b • ε),
  ({ toIsEuclidean := toIsEuclidean, card := card, exists_partition' := exists_partition' } =
      { toIsEuclidean := toIsEuclidean_1, card := card_1, exists_partition' := exists_partition'_1 }) =
    (card = card_1)
-- Std.Net.Addr
Std.Net.instInhabitedIPv4Addr : Inhabited Std.Net.IPv4Addr
-- Mathlib.Algebra.Torsor.Defs
AddGroup.instAddTorsor.eq_1 : ∀ (G : Type u_1) [inst : AddGroup G],
  AddGroup.instAddTorsor G =
    { toAddAction := AddMonoid.toAddAction G, vsub := Sub.sub, nonempty := ⋯, vsub_vadd' := ⋯, vadd_vsub' := ⋯ }
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
instIsDomainSubtypeMemSubalgebraIntegralClosure : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [IsDomain S] [inst_3 : Algebra R S],
  IsDomain ↥(integralClosure R S)
-- Mathlib.Topology.UniformSpace.Defs
UniformSpace.hasBasis_nhds : ∀ {α : Type ua} [inst : UniformSpace α] (x : α),
  (nhds x).HasBasis (fun s => s ∈ uniformity α ∧ s.IsSymm) fun s => UniformSpace.ball x s
-- Mathlib.Algebra.Order.Quantale
mul_sSup_distrib : ∀ {α : Type u_1} {x : α} {s : Set α} [inst : Semigroup α] [inst_1 : CompleteLattice α] [IsQuantale α],
  x * sSup s = ⨆ y ∈ s, x * y
-- Mathlib.Data.Seq.Basic
Stream'.Seq.map_cons : ∀ {α : Type u} {β : Type v} (f : α → β) (a : α) (s : Stream'.Seq α),
  Stream'.Seq.map f (Stream'.Seq.cons a s) = Stream'.Seq.cons (f a) (Stream'.Seq.map f s)
-- Mathlib.CategoryTheory.Subobject.Lattice
/-- `map f` sends `⊤ : MonoOver X` to `⟨X, f⟩ : MonoOver Y`.  -/
CategoryTheory.MonoOver.mapTop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      (f : X ⟶ Y) →
        [inst_1 : CategoryTheory.Mono f] → (CategoryTheory.MonoOver.map f).obj ⊤ ≅ CategoryTheory.MonoOver.mk f
-- Mathlib.Data.Ordmap.Ordnode
/-- O(log n). Modify an element in the set with the given function,
doing nothing if the key is not found.
Note that the element returned by `f` must be equivalent to `x`.

```
adjustWith f 0 {1, 2, 3} = {1, 2, 3}
adjustWith f 1 {1, 2, 3} = {f 1, 2, 3}
```

Using a preorder on `ℕ × ℕ` that only compares the first coordinate:

```
adjustWith f (1, 1) {(0, 1), (1, 2)} = {(0, 1), f (1, 2)}
adjustWith f (3, 1) {(0, 1), (1, 2)} = {(0, 1), (1, 2)}
```  -/
Ordnode.adjustWith : {α : Type u_1} → [inst : LE α] → [DecidableLE α] → (α → α) → α → Ordnode α → Ordnode α
-- Mathlib.Data.Int.GCD
/-- Use the extended GCD algorithm to generate the `a` and `b` values
satisfying `gcd x y = x * a + y * b`.  -/
Nat.xgcd : ℕ → ℕ → ℤ × ℤ
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.range_snd : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S], (RingHom.snd R S).rangeS = ⊤
-- Lean.Setup
Lean.ModuleArtifacts.mk.injEq : ∀
  (lean? olean? oleanServer? oleanPrivate? ilean? irSig? ir? c? bc? lean?_1 olean?_1 oleanServer?_1 oleanPrivate?_1
    ilean?_1 irSig?_1 ir?_1 c?_1 bc?_1 : Option System.FilePath),
  ({ lean? := lean?, olean? := olean?, oleanServer? := oleanServer?, oleanPrivate? := oleanPrivate?, ilean? := ilean?,
        irSig? := irSig?, ir? := ir?, c? := c?, bc? := bc? } =
      { lean? := lean?_1, olean? := olean?_1, oleanServer? := oleanServer?_1, oleanPrivate? := oleanPrivate?_1,
        ilean? := ilean?_1, irSig? := irSig?_1, ir? := ir?_1, c? := c?_1, bc? := bc?_1 }) =
    (lean? = lean?_1 ∧
      olean? = olean?_1 ∧
        oleanServer? = oleanServer?_1 ∧
          oleanPrivate? = oleanPrivate?_1 ∧
            ilean? = ilean?_1 ∧ irSig? = irSig?_1 ∧ ir? = ir?_1 ∧ c? = c?_1 ∧ bc? = bc?_1)
-- Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureFibrant
HomotopicalAlgebra.FibrantObject.instIsRightDerivabilityStructureWeakEquivalencesLocalizerMorphism : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C],
  (HomotopicalAlgebra.FibrantObject.localizerMorphism C).IsRightDerivabilityStructure
-- Mathlib.Tactic.Simps.Basic
Simps.instToMessageDataParsedProjectionData : Lean.ToMessageData Simps.ParsedProjectionData
-- Mathlib.Topology.Semicontinuity.Basic
ContinuousOn.lowerSemicontinuousOn : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {γ : Type u_4} [inst_1 : LinearOrder γ]
  [inst_2 : TopologicalSpace γ] [OrderTopology γ] {f : α → γ}, ContinuousOn f s → LowerSemicontinuousOn f s
-- Mathlib.Order.BooleanAlgebra.Set
Set.insert_sdiff_of_mem : ∀ {α : Type u_1} {t : Set α} {a : α} (s : Set α), a ∈ t → insert a s \ t = s \ t
-- Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
/-- The `i`th entry of `invAccumulate n m s` is `s i - s (i+1)`, where `s j = 0` if `j ≥ m`.  -/
Fin.invAccumulate : (n m : ℕ) → (Fin m → ℕ) → Fin n → ℕ
-- Mathlib.RingTheory.Finiteness.Cardinality
/-- The kernel (as a congruence relation) of a random surjective linear map
from a finite free module to a given finite module.  -/
Module.Finite.kerReprₛ : (R : Type u) →
  (M : Type u_1) →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → [inst_3 : Module.Finite R M] → ModuleCon R (Fin ⋯.choose → R)
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.TrailingMonic.def : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.TrailingMonic ↔ p.trailingCoeff = 1
-- Lean.Data.SMap
Lean.SMap.instForMProdOfMonad : {α : Type u} →
  {β : Type v} →
    [inst : BEq α] → [inst_1 : Hashable α] → {m : Type u_1 → Type u_2} → [Monad m] → ForM m (Lean.SMap α β) (α × β)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.compare_minKey?_modify_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {f : β → β} {km kmm : α} (hkm : t.minKey? = some km),
  (Std.DTreeMap.Internal.Impl.Const.modify k f t).minKey?.get ⋯ = kmm → compare kmm km = Ordering.eq
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.contains.match_1.eq_3 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.gt)
  (h_3 : Unit → motive Ordering.eq),
  (match Ordering.eq with
    | Ordering.lt => h_1 ()
    | Ordering.gt => h_2 ()
    | Ordering.eq => h_3 ()) =
    h_3 ()
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Differentiable.cos : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ},
  Differentiable ℝ f → Differentiable ℝ fun x => Real.cos (f x)
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pith.inclusion_toPrelaxFunctor_toPrelaxFunctorStruct_map₂ : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Pith B} {f g : a ⟶ b} (η : f ⟶ g),
  (CategoryTheory.Bicategory.Pith.inclusion B).map₂ η = η.iso.hom
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
CategoryTheory.Limits.pullbackLeftPullbackSndIso_inv_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (g' : W ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPullback f g]
  [inst_2 : CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.snd f g) g'],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackLeftPullbackSndIso f g g').inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd f g) g')
        (CategoryTheory.Limits.pullback.fst f g)) =
    CategoryTheory.Limits.pullback.fst f (CategoryTheory.CategoryStruct.comp g' g)
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.subsemiringClass : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A], SubsemiringClass (StarSubalgebra R A) A
-- Init.Data.BitVec.Bootstrap
BitVec.ofNatLT_eq_ofNat : ∀ {w n : ℕ} (hn : n < 2 ^ w), n#'hn = BitVec.ofNat w n
-- Mathlib.Algebra.Group.Hom.Instances
instIsLeftCancelAddZeroHom : ∀ {M : Type uM} {N : Type uN} [inst : Zero M] [inst_1 : AddZeroClass N] [IsLeftCancelAdd N],
  IsLeftCancelAdd (ZeroHom M N)
-- Mathlib.Order.InitialSeg
PrincipalSeg.mem_range_iff_rel : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : PrincipalSeg r s) {b : β},
  b ∈ Set.range ⇑f.toRelEmbedding ↔ s b f.top
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instSemiringOfAddOpposite : {M : Type u_1} → [Semiring Mᵃᵒᵖ] → Semiring Mᵈᵃᵃ
-- Mathlib.Algebra.Ring.Pi
Pi.nonUnitalRing : {I : Type u} → {f : I → Type v} → [(i : I) → NonUnitalRing (f i)] → NonUnitalRing ((i : I) → f i)
-- Mathlib.Algebra.Group.Subgroup.Pointwise
AddSubgroup.add_subset : ∀ {G : Type u_2} [inst : AddGroup G] {s t : Set G} {H : AddSubgroup G}, s ⊆ ↑H → t ⊆ ↑H → s + t ⊆ ↑H
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- The cokernel of the kernel of a monomorphism is an isomorphism  -/
CategoryTheory.Limits.cokernel.of_kernel_of_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Limits.HasKernel f]
  [inst_4 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)] [CategoryTheory.Mono f],
  CategoryTheory.IsIso (CategoryTheory.Limits.cokernel.π (CategoryTheory.Limits.kernel.ι f))
-- Mathlib.Data.Fin.Tuple.Basic
Fin.snoc_inj : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u_1} {x y : (i : Fin n) → α i.castSucc} {xₙ yₙ : α (Fin.last n)},
  Fin.snoc x xₙ = Fin.snoc y yₙ ↔ x = y ∧ xₙ = yₙ
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.monad : {R : Type u_3} → [inst : CommSemiring R] → Monad fun σ => MvPolynomial σ R
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.coeFn_sub : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] (f g : ↥(MeasureTheory.Lp E p μ)), ↑↑(f - g) =ᵐ[μ] ↑↑f - ↑↑g
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.maxD_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] {fallback : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.maxD fallback = t₂.maxD fallback
-- Mathlib.Combinatorics.SimpleGraph.Operations
SimpleGraph.disjoint_edge : ∀ {V : Type u_1} (G : SimpleGraph V) {u v : V}, Disjoint G (SimpleGraph.edge u v) ↔ ¬G.Adj u v
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- The action by an intermediate field is the action by the underlying field.  -/
IntermediateField.instMulSemiringActionSubtypeMem : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] →
          {X : Type u_4} →
            [inst_3 : Semiring X] → [MulSemiringAction L X] → (F : IntermediateField K L) → MulSemiringAction (↥F) X
-- Mathlib.CategoryTheory.Sites.MayerVietorisSquare
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.instMonoSheafAddCommGrpCatFShortComplex : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] [inst_2 : CategoryTheory.HasSheafify J AddCommGrpCat]
  (S : J.MayerVietorisSquare), CategoryTheory.Mono S.shortComplex.f
-- Mathlib.Tactic.Tauto
/-- State of the `distribNotAt` function. We need to carry around the list of
remaining hypothesis as fvars so that we can incrementally apply the
`AssertAfterResult.subst` from each step to each of them. Otherwise,
they could end up referring to old hypotheses.
 -/
Mathlib.Tactic.Tauto.DistribNotState : Type
-- Init.Prelude
Nat.lt_succ_of_le : ∀ {n m : ℕ}, n ≤ m → n < m.succ
-- Mathlib.Topology.ContinuousOn
ContinuousOn.isOpen_preimage : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
  {t : Set β}, ContinuousOn f s → IsOpen s → f ⁻¹' t ⊆ s → IsOpen t → IsOpen (f ⁻¹' t)
-- Init.Data.UInt.Lemmas
UInt16.ofNatLT.congr_simp : ∀ (n n_1 : ℕ) (e_n : n = n_1) (h : n < UInt16.size), UInt16.ofNatLT n h = UInt16.ofNatLT n_1 ⋯
-- Mathlib.CategoryTheory.Sites.SheafHom
/-- Equational lemma for the presheaf structure on `presheafHom`.
It is advisable to use this lemma rather than `dsimp [presheafHom]` which may result
in the need to prove equalities of objects in an `Over` category.  -/
CategoryTheory.presheafHom_map_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  {F G : CategoryTheory.Functor Cᵒᵖ A} {X Y Z : C} (f : Z ⟶ Y) (g : Y ⟶ X) (h : Z ⟶ X),
  CategoryTheory.CategoryStruct.comp f g = h →
    ∀ (α : (CategoryTheory.presheafHom F G).obj (Opposite.op X)),
      ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.presheafHom F G).map g.op)) α).app
          (Opposite.op (CategoryTheory.Over.mk f)) =
        α.app (Opposite.op (CategoryTheory.Over.mk h))
-- Mathlib.Data.Set.Function
Function.invFunOn.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Nonempty α] (f : α → β) (s : Set α) (b : β),
  Function.invFunOn f s b = if h : ∃ a ∈ s, f a = b then Classical.choose h else Classical.choice inst
-- Mathlib.Data.Set.Prod
Set.Nonempty.snd : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β}, (s ×ˢ t).Nonempty → t.Nonempty
-- Mathlib.CategoryTheory.Category.PartialFun
partialFunToPointed_map : ∀ {X Y : PartialFun} (f : X ⟶ Y),
  partialFunToPointed.map f = { toFun := Option.elim' none fun a => (f a).toOption, map_point := ⋯ }
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.equivLike : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : TopologicalSpace A] →
            [inst_3 : Semiring B] →
              [inst_4 : TopologicalSpace B] →
                [inst_5 : Algebra R A] → [inst_6 : Algebra R B] → EquivLike (A ≃A[R] B) A B
-- Mathlib.Analysis.Convex.Segment
Nonneg.segment_eq_Icc : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsStrictOrderedRing 𝕜] {x y : { t // 0 ≤ t }},
  x ≤ y → segment { t // 0 ≤ t } x y = Set.Icc x y
-- Lean.Declaration
Lean.instInhabitedInductiveType.default : Lean.InductiveType
-- Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
/-- A number `τ > 1`, but chosen close enough to `1` so that the construction in the Besicovitch
covering theorem using this parameter `τ` will give the smallest possible number of covering
families.  -/
Besicovitch.goodτ : (E : Type u_1) → [inst : NormedAddCommGroup E] → [inst_1 : NormedSpace ℝ E] → [FiniteDimensional ℝ E] → ℝ
-- Mathlib.ModelTheory.Basic
/-- The cardinality of a language is the cardinality of its type of symbols.  -/
FirstOrder.Language.card : FirstOrder.Language → Cardinal.{max u v}
-- Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM
ContinuousLinearMap.postcompCompactConvergenceCLM_apply : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂]
  [inst_2 : NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [inst_3 : RingHomCompTriple σ τ ρ]
  (E : Type u_4) {F : Type u_5} {G : Type u_6} [inst_4 : AddCommGroup E] [inst_5 : Module 𝕜₁ E]
  [inst_6 : AddCommGroup F] [inst_7 : Module 𝕜₂ F] [inst_8 : AddCommGroup G] [inst_9 : Module 𝕜₃ G]
  [inst_10 : TopologicalSpace E] [inst_11 : TopologicalSpace F] [inst_12 : TopologicalSpace G]
  [inst_13 : IsTopologicalAddGroup F] [inst_14 : IsTopologicalAddGroup G] [inst_15 : ContinuousConstSMul 𝕜₃ G]
  [inst_16 : ContinuousConstSMul 𝕜₂ F] (L : F →SL[τ] G) (f : UniformConvergenceCLM σ F {S | IsCompact S}),
  (ContinuousLinearMap.postcompCompactConvergenceCLM E L) f = L ∘SL f
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_hom_inv' : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (x : D) {y z : C} (f : y ⟶ z)
  [inst_4 : CategoryTheory.IsIso f],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight x f)
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight x (CategoryTheory.inv f)) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj x y)
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.balance.congr_simp : ∀ {α : Type u} {β : α → Type v} (k : α) (v v_1 : β k),
  v = v_1 →
    ∀ (l l_1 : Std.DTreeMap.Internal.Impl α β) (e_l : l = l_1) (r r_1 : Std.DTreeMap.Internal.Impl α β) (e_r : r = r_1)
      (hl : l.Balanced) (hr : r.Balanced)
      (h :
        Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l.size r.size ∨
          Std.DTreeMap.Internal.Impl.BalanceLErasePrecond r.size l.size),
      Std.DTreeMap.Internal.Impl.balance k v l r hl hr h = Std.DTreeMap.Internal.Impl.balance k v_1 l_1 r_1 ⋯ ⋯ ⋯