mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.UniformSpace.UniformEmbedding
Filter.HasBasis.isUniformInducing_iff : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {ι : Sort u_1} {ι' : Sort u_2}
  {p : ι → Prop} {p' : ι' → Prop} {s : ι → Set (α × α)} {s' : ι' → Set (β × β)},
  (uniformity α).HasBasis p s →
    (uniformity β).HasBasis p' s' →
      ∀ {f : α → β},
        IsUniformInducing f ↔
          (∀ (i : ι'), p' i → ∃ j, p j ∧ ∀ (x y : α), (x, y) ∈ s j → (f x, f y) ∈ s' i) ∧
            ∀ (j : ι), p j → ∃ i, p' i ∧ ∀ (x y : α), (f x, f y) ∈ s' i → (x, y) ∈ s j
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.constantCoeff_comp_C : ∀ (R : Type u) (σ : Type u_1) [inst : CommSemiring R], MvPolynomial.constantCoeff.comp MvPolynomial.C = RingHom.id R
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.instDistribMulAction : {R : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Monoid G] →
          [inst_1 : Ring R] →
            [inst_2 : AddCommGroup V] →
              [inst_3 : TopologicalSpace V] →
                [inst_4 : IsTopologicalAddGroup V] →
                  [inst_5 : Module R V] →
                    [inst_6 : AddCommGroup W] →
                      [inst_7 : TopologicalSpace W] →
                        [inst_8 : IsTopologicalAddGroup W] →
                          [inst_9 : Module R W] →
                            {π₁ : ContRepresentation R G V} →
                              {π₂ : ContRepresentation R G W} →
                                {S : Type u_6} →
                                  [inst_10 : Monoid S] →
                                    [inst_11 : DistribMulAction S W] →
                                      [SMulCommClass R S W] →
                                        [ContinuousConstSMul S W] →
                                          [LinearMap.CompatibleSMul W W S R] →
                                            DistribMulAction S (ContIntertwiningMap π₁ π₂)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.isLE_iff_isZero_truncGT_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (X : C),
  t.IsLE X n ↔ CategoryTheory.Limits.IsZero ((t.truncGT n).obj X)
-- Lean.Environment
_private.Lean.Environment.0.Lean.ImportState.moduleNames : Lean.ImportState → Array Lean.Name
-- Mathlib.Algebra.Ring.Parity
Odd.neg_one_pow : ∀ {α : Type u_2} [inst : Monoid α] [inst_1 : HasDistribNeg α] {n : ℕ}, Odd n → (-1) ^ n = -1
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.WF.insertMany! : ∀ {α : Type u} {β : α → Type v} {x : Ord α} [Std.TransOrd α] {ρ : Type u_1} [inst : ForIn Id ρ ((a : α) × β a)] {l : ρ}
  {t : Std.DTreeMap.Internal.Impl α β}, t.WF → (↑(t.insertMany! l)).WF
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- Expand the square  -/
norm_sub_sq : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x y : E), ‖x - y‖ ^ 2 = ‖x‖ ^ 2 - 2 * RCLike.re (inner 𝕜 x y) + ‖y‖ ^ 2
-- Mathlib.Logic.Basic
congr_fun_congr_arg : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β → γ) {a a' : α} (p : a = a') (b : β), ⋯ = ⋯
-- Init.Data.List.Scan.Lemmas
List.head?_scanl : ∀ {β : Type u_1} {α : Type u_2} {b : β} {l : List α} {f : β → α → β}, (List.scanl f b l).head? = some b
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.grevlex : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Ordering
-- Mathlib.Analysis.Normed.Group.Defs
ESeminormedCommMonoid.toESeminormedMonoid : {E : Type u_8} → {inst : TopologicalSpace E} → [self : ESeminormedCommMonoid E] → ESeminormedMonoid E
-- Batteries.Recycling.MonadSatisfying.Array
Array.SatisfiesM_anyM : ∀ {m : Type → Type u_1} {α : Type u_2} {start stop : ℕ} [inst : Monad m] [LawfulMonad m] {p : α → m Bool}
  {as : Array α},
  start ≤ min stop as.size →
    ∀ (tru : Prop) (fal : ℕ → Prop),
      fal start →
        (∀ (i : Fin as.size), ↑i < stop → fal ↑i → SatisfiesM (fun x => bif x then tru else fal (↑i + 1)) (p as[i])) →
          SatisfiesM (fun res => bif res then tru else fal (min stop as.size)) (Array.anyM p as start stop)
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ D` reflects limits, then `F.op : Cᵒᵖ ⥤ Dᵒᵖ` reflects colimits.  -/
CategoryTheory.Limits.reflectsColimitsOfSize_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.ReflectsColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.op
-- Lean.Expr
Lean.mkDecIsTrue : Lean.Expr → Lean.Expr → Lean.Expr
-- Batteries.Data.AssocList
Batteries.AssocList.brecOn.go : {α : Type u} →
  {β : Type v} →
    {motive : Batteries.AssocList α β → Sort u_1} →
      (t : Batteries.AssocList α β) →
        ((t : Batteries.AssocList α β) → Batteries.AssocList.below t → motive t) →
          motive t ×' Batteries.AssocList.below t
-- Mathlib.MeasureTheory.Order.Lattice
MeasurableSup.measurable_const_sup : ∀ {M : Type u_1} {inst : MeasurableSpace M} {inst_1 : Max M} [self : MeasurableSup M] (c : M), Measurable fun x => c ⊔ x
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.reflectsLimitsOfShape_of_reflectsLimits : ∀ {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] (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.ReflectsLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.ReflectsLimitsOfShape J F
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKey!.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) [inst_1 : Inhabited α] (size : ℕ) (k' : α) (v : β k')
  (l r : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.inner size k' v l r).getKey! k =
    match compare k k' with
    | Ordering.lt => l.getKey! k
    | Ordering.gt => r.getKey! k
    | Ordering.eq => k'
-- Lean.Elab.DocString
/-- Builds a hint for an "Unknown role/directive/..." error when the name might be shadowed.
 -/
_private.Lean.Elab.DocString.0.Lean.Doc.shadowedHint : {α : Type} → Lean.NameMap (Array Lean.Name) → Lean.NameMap α → Lean.Ident → String → Lean.Doc.DocM Lean.MessageData
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.ImageFactorisation.ofArrowIso_isImage : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C}
  (F : CategoryTheory.Limits.ImageFactorisation f.hom) (sq : f ⟶ g) [inst_1 : CategoryTheory.IsIso sq],
  (F.ofArrowIso sq).isImage = F.isImage.ofArrowIso sq
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.swapLeft_prodMkLeft : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β)
  (γ : Type u_5) {x : MeasurableSpace γ},
  (ProbabilityTheory.Kernel.prodMkLeft γ κ).swapLeft = ProbabilityTheory.Kernel.prodMkRight γ κ
-- Mathlib.GroupTheory.Congruence.Defs
/-- The map sending a binary relation to the smallest additive
congruence relation in which it is contained is idempotent.  -/
AddCon.addConGen_idem : ∀ {M : Type u_1} [inst : Add M] (r : M → M → Prop), addConGen ⇑(addConGen r) = addConGen r
-- Mathlib.RingTheory.PolynomialAlgebra
polyEquivTensor_symm_apply_tmul_eq_smul : ∀ (R : Type u_1) (A : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (a : A)
  (p : Polynomial R), (polyEquivTensor R A).symm (a ⊗ₜ[R] p) = a • Polynomial.map (algebraMap R A) p
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.upperCrossingTime.eq_1 : ∀ {Ω : Type u_1} {ι : Type u_2} [inst : Preorder ι] [inst_1 : OrderBot ι] [inst_2 : InfSet ι] (a b : ℝ) (f : ι → Ω → ℝ)
  (N : ι), MeasureTheory.upperCrossingTime a b f N 0 = ⊥
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instBEqMon.beq_spec : ∀ (x x_1 : Lean.Grind.CommRing.Mon),
  (x == x_1) =
    match x, x_1 with
    | Lean.Grind.CommRing.Mon.unit, Lean.Grind.CommRing.Mon.unit => true
    | Lean.Grind.CommRing.Mon.mult a a_1, Lean.Grind.CommRing.Mon.mult b b_1 => a == b && a_1 == b_1
    | x, x_2 => false
-- Mathlib.LinearAlgebra.Alternating.Curry
AlternatingMap.curryLeft_smul : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] {n : ℕ} (r : R) (f : M [⋀^Fin n.succ]→ₗ[R] N),
  (r • f).curryLeft = r • f.curryLeft
-- Mathlib.Analysis.Analytic.CPolynomialDef
HasFiniteFPowerSeriesAt.cpolynomialAt : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {n : ℕ}, HasFiniteFPowerSeriesAt f p x n → CPolynomialAt 𝕜 f x
-- Mathlib.Data.Multiset.Dedup
Multiset.dedup_eq_self : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Multiset α}, s.dedup = s ↔ s.Nodup
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosDef.inv : ∀ {n : Type u_2} [inst : Fintype n] {K : Type u_5} [inst_1 : Field K] [inst_2 : PartialOrder K] [inst_3 : StarRing K]
  [inst_4 : DecidableEq n] {M : Matrix n n K}, M.PosDef → M⁻¹.PosDef
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.mk.injEq : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  (toPartialEquiv : PartialEquiv Z (B × F)) (open_target : IsOpen toPartialEquiv.target) (baseSet : Set B)
  (open_baseSet : IsOpen baseSet) (source_eq : toPartialEquiv.source = proj ⁻¹' baseSet)
  (target_eq : toPartialEquiv.target = baseSet ×ˢ Set.univ)
  (proj_toFun : ∀ p ∈ toPartialEquiv.source, (↑toPartialEquiv p).1 = proj p) (toPartialEquiv_1 : PartialEquiv Z (B × F))
  (open_target_1 : IsOpen toPartialEquiv_1.target) (baseSet_1 : Set B) (open_baseSet_1 : IsOpen baseSet_1)
  (source_eq_1 : toPartialEquiv_1.source = proj ⁻¹' baseSet_1)
  (target_eq_1 : toPartialEquiv_1.target = baseSet_1 ×ˢ Set.univ)
  (proj_toFun_1 : ∀ p ∈ toPartialEquiv_1.source, (↑toPartialEquiv_1 p).1 = proj p),
  ({ toPartialEquiv := toPartialEquiv, open_target := open_target, baseSet := baseSet, open_baseSet := open_baseSet,
        source_eq := source_eq, target_eq := target_eq, proj_toFun := proj_toFun } =
      { toPartialEquiv := toPartialEquiv_1, open_target := open_target_1, baseSet := baseSet_1,
        open_baseSet := open_baseSet_1, source_eq := source_eq_1, target_eq := target_eq_1,
        proj_toFun := proj_toFun_1 }) =
    (toPartialEquiv = toPartialEquiv_1 ∧ baseSet = baseSet_1)
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
/-- `DayFunctor C V` is a type synonym for `C ⥤ V`, implemented as a one-field
structure.  -/
CategoryTheory.MonoidalCategory.DayFunctor : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (V : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [CategoryTheory.MonoidalCategory C] → [CategoryTheory.MonoidalCategory V] → Type (max (max (max u₁ u₂) v₁) v₂)
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.commonNeighbors_top_eq : ∀ {V : Type u} {v w : V}, ⊤.commonNeighbors v w = Set.univ \ {v, w}
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minKey.congr_simp : ∀ {α : Type u} {β : α → Type v} (t t_1 : Std.DTreeMap.Internal.Impl α β) (e_t : t = t_1) (h : t.isEmpty = false),
  t.minKey h = t_1.minKey ⋯
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward
PresheafOfModules.pushforward_obj_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ RingCat} {S : CategoryTheory.Functor Cᵒᵖ RingCat}
  (φ : S ⟶ F.op.comp R) (X : PresheafOfModules R) (X_1 : Cᵒᵖ),
  ((PresheafOfModules.pushforward φ).obj X).obj X_1 =
    (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.app X_1))).obj ((PresheafOfModules.pushforward₀Obj F R X).obj X_1)
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
/-- Whether a graph can be colored by at most `n` colors.  -/
SimpleGraph.Colorable : {V : Type u} → SimpleGraph V → ℕ → Prop
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.copyBase_eq : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) (g : ↥X → ↥Y) (h : ⇑f = g), f.copyBase g h = f
-- Mathlib.Algebra.Order.CauSeq.BigOperators
IsCauSeq.congr_simp : ∀ {α : Type u_3} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_4}
  [inst_3 : Ring β] (abv abv_1 : β → α), abv = abv_1 → ∀ (f f_1 : ℕ → β), f = f_1 → IsCauSeq abv f = IsCauSeq abv_1 f_1
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getD_filterMap_of_getKey?_eq_some : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w}
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [EquivBEq α] [LawfulHashable α] {f : α → β → Option γ} {k k' : α}
  {fallback : γ},
  (↑m).WF →
    m.getKey? k = some k' →
      Std.DHashMap.Internal.Raw₀.Const.getD (Std.DHashMap.Internal.Raw₀.filterMap f m) k fallback =
        ((Std.DHashMap.Internal.Raw₀.Const.get? m k).bind fun x => f k' x).getD fallback
-- Mathlib.Topology.Covering.Basic
IsEvenlyCovered.of_trivialization : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {I : Type u_3}
  [inst_2 : TopologicalSpace I] [DiscreteTopology I] {x : X} {t : Bundle.Trivialization I f},
  x ∈ t.baseSet → IsEvenlyCovered f x I
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.mkTacticInfo : Lean.MetavarContext → List Lean.MVarId → Lean.Syntax → Lean.Elab.Tactic.Grind.GrindTacticM Lean.Elab.Info
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
/-- The topology induced by a family of seminorms is exactly the infimum of the ones induced by
each seminorm individually. We express this as a characterization of `WithSeminorms p`.  -/
SeminormFamily.withSeminorms_iff_topologicalSpace_eq_iInf : ∀ {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [t : TopologicalSpace E] [IsTopologicalAddGroup E] (p : SeminormFamily 𝕜 E ι),
  WithSeminorms p ↔ t = ⨅ i, PseudoMetricSpace.toUniformSpace.toTopologicalSpace
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.subtype_apply : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (L : BooleanSubalgebra α) (a : ↥L), L.subtype a = ↑a
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
_private.Mathlib.Algebra.BigOperators.Group.Finset.Defs.0.BigOperators.FinsetResult.Iio.sizeOf_spec : ∀ (n : Lean.Term), sizeOf (BigOperators.FinsetResult.Iio✝ n) = 1 + sizeOf n
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.interior_restrict : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [inst_4 : PartialOrder k] {n : ℕ} (s : Affine.Simplex k P n) {S : AffineSubspace k P}
  (hS : affineSpan k (Set.range s.points) ≤ S), (s.restrict S hS).interior = ⇑S.subtype ⁻¹' s.interior
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.kernelSequenceCyclesE_g : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.kernelSequenceCyclesE._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.kernelSequenceCyclesE._auto_3),
  (X.kernelSequenceCyclesE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).g =
    CategoryTheory.CategoryStruct.comp (X.iCycles f₁ f₂₃ n₁)
      ((X.H n₁).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f₂ f₃ f₂₃ h₂₃))
-- Init.Data.Vector.Lemmas
Vector.forall_mem_empty : ∀ {α : Type u_1} (p : α → Prop), ∀ x ∈ #v[], p x
-- Init.Omega.Coeffs
/-- Shim for `IntList.leading`.  -/
Lean.Omega.Coeffs.leading : Lean.Omega.Coeffs → ℤ
-- Mathlib.MeasureTheory.Measure.Stieltjes
isOpen_Iotop : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] [OrderTopology R] (a b : R), IsOpen (Iotop a b)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- Every equalizer of `(f, f)` is an isomorphism.  -/
CategoryTheory.Limits.isIso_limit_cone_parallelPair_of_self : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f : X ⟶ Y} {c : CategoryTheory.Limits.Fork f f}
  (h : CategoryTheory.Limits.IsLimit c), CategoryTheory.IsIso c.ι
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.equiv_iff_toArray_perm : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp},
  t₁.Equiv t₂ ↔ (Std.DTreeMap.Const.toArray t₁).Perm (Std.DTreeMap.Const.toArray t₂)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- Every kernel of the zero morphism is an isomorphism  -/
CategoryTheory.Limits.kernel.ι_zero_isIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C},
  CategoryTheory.IsIso (CategoryTheory.Limits.kernel.ι 0)
-- Mathlib.Order.BooleanAlgebra.Set
Set.inter_sdiff_right_comm : ∀ {α : Type u_1} {s t u : Set α}, (s ∩ t) \ u = s \ u ∩ t
-- Mathlib.Algebra.Group.Subgroup.Lattice
/-- `closure` forms a Galois insertion with the coercion to set.  -/
Subgroup.gi : (G : Type u_1) → [inst : Group G] → GaloisInsertion Subgroup.closure SetLike.coe
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.forgetToPresheafModuleCatObj_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (X : Cᵒᵖ)
  (hX : CategoryTheory.Limits.IsInitial X) (M : PresheafOfModules R) {X_1 Y : Cᵒᵖ} (f : X_1 ⟶ Y),
  (PresheafOfModules.forgetToPresheafModuleCatObj X hX M).map f =
    PresheafOfModules.forgetToPresheafModuleCatObjMap X hX M f
-- Init.Data.List.Lemmas
List.eraseDups_nil : ∀ {α : Type u_1} [inst : BEq α], [].eraseDups = []
-- Mathlib.Algebra.Group.Submonoid.Membership
/-- Exponentiation map from natural numbers to powers.  -/
Submonoid.pow : {M : Type u_1} → [inst : Monoid M] → (n : M) → ℕ → ↥(Submonoid.powers n)
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.restrictScalarsComp'App_inv_naturality_assoc : ∀ {R₁ : Type u₁} {R₂ : Type u₂} {R₃ : Type u₃} [inst : Ring R₁] [inst_1 : Ring R₂] [inst_2 : Ring R₃] (f : R₁ →+* R₂)
  (g : R₂ →+* R₃) (gf : R₁ →+* R₃) (hgf : gf = g.comp f) {M N : ModuleCat R₃} (φ : M ⟶ N) {Z : ModuleCat R₁}
  (h : (ModuleCat.restrictScalars gf).obj N ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((ModuleCat.restrictScalars f).map ((ModuleCat.restrictScalars g).map φ))
      (CategoryTheory.CategoryStruct.comp (ModuleCat.restrictScalarsComp'App f g gf hgf N).inv h) =
    CategoryTheory.CategoryStruct.comp (ModuleCat.restrictScalarsComp'App f g gf hgf M).inv
      (CategoryTheory.CategoryStruct.comp ((ModuleCat.restrictScalars gf).map φ) h)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.toList_eq_nil_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t.toList = [] ↔ t = ∅
-- Mathlib.Topology.Instances.Matrix
Continuous.matrix_map : ∀ {X : Type u_1} {m : Type u_4} {n : Type u_5} {S : Type u_7} {R : Type u_8} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace R] [inst_2 : TopologicalSpace S] {A : X → Matrix m n S} {f : S → R},
  Continuous A → Continuous f → Continuous fun x => (A x).map f
-- Mathlib.Algebra.Polynomial.Lifts
Polynomial.monic_of_monic_mapAlg : ∀ {R : Type u} [inst : CommSemiring R] {S : Type v} [inst_1 : Semiring S] [inst_2 : Algebra R S] [FaithfulSMul R S]
  {p : Polynomial R}, ((Polynomial.mapAlg R S) p).Monic → p.Monic
-- Mathlib.Data.Finset.Dedup
Multiset.toFinset_eq : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} (n : s.Nodup), { val := s, nodup := n } = s.toFinset
-- Mathlib.RingTheory.Ideal.GoingUp
Ideal.exists_ideal_over_prime_of_isIntegral : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.IsIntegral R S] (P : Ideal R) [P.IsPrime] (I : Ideal S),
  Ideal.comap (algebraMap R S) I ≤ P → ∃ Q ≥ I, Q.IsPrime ∧ Ideal.comap (algebraMap R S) Q = P
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.dirichletInverseFun_apply_ne : ∀ {R : Type u_1} [inst : Ring R] (f : ℕ → R) (hf : Invertible (f 1)) {n : ℕ},
  n ≠ 0 →
    n ≠ 1 →
      ArithmeticFunction.dirichletInverseFun f hf n =
        -⅟(f 1) * ∑ d ∈ n.properDivisors, f (n / d) * ArithmeticFunction.dirichletInverseFun f hf d
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.support_add : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p q : MvPolynomial σ R} [inst_1 : DecidableEq σ],
  (p + q).support ⊆ p.support ∪ q.support
-- Mathlib.Algebra.Category.MonCat.Limits
AddMonCat.HasLimits.limitCone.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddMonCat)
  [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddMonCat)).sections],
  AddMonCat.HasLimits.limitCone F =
    { pt := AddMonCat.of (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget AddMonCat))).pt,
      π := { app := fun j => AddMonCat.ofHom (AddMonCat.limitπAddMonoidHom F j), naturality := ⋯ } }
-- Mathlib.Data.Seq.Computation
Computation.think_bind : ∀ {α : Type u} {β : Type v} (c : Computation α) (f : α → Computation β), c.think.bind f = (c.bind f).think
-- Init.Data.SInt.Lemmas
Int8.toInt_mul : ∀ (a b : Int8), (a * b).toInt = (a.toInt * b.toInt).bmod (2 ^ 8)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.not_vlt : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x y : R}, ¬x <ᵥ y ↔ y ≤ᵥ x
-- Mathlib.CategoryTheory.Sites.Subsheaf
CategoryTheory.Subfunctor.le_sheafify : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  {F : CategoryTheory.Functor Cᵒᵖ (Type w)} (G : CategoryTheory.Subfunctor F),
  G ≤ CategoryTheory.Subfunctor.sheafify J G
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.kroneckerTMul_assoc' : ∀ (R : Type u_1) {α : Type u_3} {β : Type u_5} {γ : Type u_7} {l : Type u_9} {m : Type u_10} {n : Type u_11}
  {p : Type u_12} {q : Type u_13} {r : Type u_14} [inst : CommSemiring R] [inst_1 : AddCommMonoid α]
  [inst_2 : AddCommMonoid β] [inst_3 : AddCommMonoid γ] [inst_4 : Module R α] [inst_5 : Module R β]
  [inst_6 : Module R γ] (A : Matrix l m α) (B : Matrix n p β) (C : Matrix q r γ),
  ((Matrix.kroneckerMap (TensorProduct.tmul R) (Matrix.kroneckerMap (TensorProduct.tmul R) A B) C).map
          ⇑(TensorProduct.assoc R α β γ)).submatrix
      ⇑(Equiv.prodAssoc l n q).symm ⇑(Equiv.prodAssoc m p r).symm =
    Matrix.kroneckerMap (TensorProduct.tmul R) A (Matrix.kroneckerMap (TensorProduct.tmul R) B C)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
/-- Given a graded ring hom `f : 𝒜 →+*ᵍ ℬ` satisfying the hypothesis `ℬ₊ ≤ 𝒜₊.map f`, we obtain
an affine open cover of `Proj ℬ` consisting of `D(f(s))` for `s ∈ A` positive degree.  -/
AlgebraicGeometry.Proj.mapAffineOpenCover : {A B σ τ : Type u} →
  [inst : CommRing A] →
    [inst_1 : SetLike σ A] →
      [inst_2 : AddSubgroupClass σ A] →
        [inst_3 : CommRing B] →
          [inst_4 : SetLike τ B] →
            [inst_5 : AddSubgroupClass τ B] →
              {𝒜 : ℕ → σ} →
                {ℬ : ℕ → τ} →
                  [inst_6 : GradedRing 𝒜] →
                    [inst_7 : GradedRing ℬ] →
                      (f : 𝒜 →+*ᵍ ℬ) →
                        HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜) →
                          (AlgebraicGeometry.Proj ℬ).AffineOpenCover