mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.BumpFunction
SmoothBumpFunction.mk.injEq : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {c : M}
  (toContDiffBump : ContDiffBump (↑(extChartAt I c) c))
  (closedBall_subset :
    Metric.closedBall (↑(extChartAt I c) c) toContDiffBump.rOut ∩ Set.range ↑I ⊆ (extChartAt I c).target)
  (toContDiffBump_1 : ContDiffBump (↑(extChartAt I c) c))
  (closedBall_subset_1 :
    Metric.closedBall (↑(extChartAt I c) c) toContDiffBump_1.rOut ∩ Set.range ↑I ⊆ (extChartAt I c).target),
  ({ toContDiffBump := toContDiffBump, closedBall_subset := closedBall_subset } =
      { toContDiffBump := toContDiffBump_1, closedBall_subset := closedBall_subset_1 }) =
    (toContDiffBump = toContDiffBump_1)
-- Mathlib.Data.Ordmap.Ordset
_private.Mathlib.Data.Ordmap.Ordset.0.Ordnode.mem.match_1.splitter : (motive : Ordering → Sort u_1) →
  (x : Ordering) → (Unit → motive Ordering.lt) → (Unit → motive Ordering.eq) → (Unit → motive Ordering.gt) → motive x
-- Aesop.RuleTac.Basic
Aesop.instInhabitedCasesTarget : Inhabited Aesop.CasesTarget
-- Init.Data.String.Pattern.Basic
/-- The end position of a `SearchStep`.  -/
String.Slice.Pattern.SearchStep.endPos : {s : String.Slice} → String.Slice.Pattern.SearchStep s → s.Pos
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.coe_units_iff : ∀ {M : Type u_1} [inst : CommMonoid M] {k : ℕ} {ζ : Mˣ}, IsPrimitiveRoot (↑ζ) k ↔ IsPrimitiveRoot ζ k
-- Mathlib.RingTheory.Algebraic.Basic
Algebra.injective_of_transcendental : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A]
  [h : Algebra.Transcendental R A], Function.Injective ⇑(algebraMap R A)
-- Mathlib.Topology.Algebra.Valued.LocallyCompact
Valued.integer.isPrincipalIdealRing_of_compactSpace : ∀ {K : Type u_1} {Γ₀ : Type u_2} [inst : Field K] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [inst_2 : Valued K Γ₀]
  [hc : CompactSpace ↥(Valued.integer K)], IsPrincipalIdealRing ↥(Valued.integer K)
-- Mathlib.Algebra.Group.End
MulAutMultiplicative_symm_apply_apply : ∀ (G : Type u_3) [inst : AddGroup G] (a : G ≃+ G) (a_1 : Multiplicative G),
  ((MulAutMultiplicative G).symm a) a_1 = Multiplicative.ofAdd (a (Multiplicative.toAdd a_1))
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
/-- To give an object of `Over A`, we will in particular need a presheaf `Cᵒᵖ ⥤ Type v`. This is
the definition of that presheaf on objects.

We would prefer to think of this sigma type to be indexed by natural transformations
`yoneda.obj X ⟶ A` instead of `A.obj (op X)`. These are equivalent by the Yoneda lemma, but
we cannot use the former because that type lives in the wrong universe. Hence, we will provide
a lot of API that will enable us to pretend that we are really indexing over
`yoneda.obj X ⟶ A`.  -/
CategoryTheory.OverPresheafAux.YonedaCollection : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : CategoryTheory.Functor Cᵒᵖ (Type v)} →
      CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v) → C → Type v
-- Init.Data.SInt.Lemmas
Int8.sub_le : ∀ {a b : Int8}, 0 ≤ b → b ≤ a → a - b ≤ a
-- Mathlib.MeasureTheory.Measure.Haar.Unique
/-- An invariant measure is absolutely continuous with respect to an additive Haar measure.  -/
MeasureTheory.Measure.absolutelyContinuous_isAddHaarMeasure : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [BorelSpace G] [LocallyCompactSpace G] [SecondCountableTopology G]
  (μ ν : MeasureTheory.Measure G) [MeasureTheory.SigmaFinite μ] [μ.IsAddLeftInvariant] [ν.IsAddHaarMeasure],
  μ.AbsolutelyContinuous ν
-- Init.Data.UInt.Bitwise
UInt16.zero_shiftRight : ∀ {a : UInt16}, 0 >>> a = 0
-- Mathlib.Order.WellFounded
WellFounded.notMem_of_lt_min : ∀ {α : Type u_1} {r : α → α → Prop} {wf : WellFounded r} {s : Set α} {hs : s.Nonempty} {x : α},
  r x (wf.min s hs) → x ∉ s
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- A wide equalizer morphism is a monomorphism  -/
CategoryTheory.Limits.wideEqualizer.ι_mono : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)}
  [inst_1 : CategoryTheory.Limits.HasWideEqualizer f] [Nonempty J],
  CategoryTheory.Mono (CategoryTheory.Limits.wideEqualizer.ι f)
-- Batteries.Data.Vector.Lemmas
Vector.uget_mk : ∀ {α : Type u_1} {n : ℕ} (a : Array α) (h : a.size = n) (i : USize) (hi : i.toNat < n),
  (Vector.mk a h).uget i hi = a.uget i ⋯
-- Mathlib.Data.PFunctor.Multivariate.W
MvPFunctor.wInd_wMk : ∀ {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} {C : P.W α → Sort v}
  (ih :
    (a : P.A) →
      (f' : (P.drop.B a).Arrow α) → (f : P.last.B a → P.W α) → ((i : P.last.B a) → C (f i)) → C (P.wMk a f' f))
  {a : P.drop.A} {f' : (P.drop.B a).Arrow α} {f : P.last.B a → P.W α},
  P.wInd ih (P.wMk a f' f) = ih a f' f fun i => P.wInd ih (f i)
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
Bundle.Trivialization.localFrame_apply_of_mem_baseSet : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {M : Type u_4} [inst_1 : TopologicalSpace M] {F : Type u_5}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 F] {V : M → Type u_6}
  [inst_4 : TopologicalSpace (Bundle.TotalSpace F V)] [inst_5 : (x : M) → AddCommGroup (V x)]
  [inst_6 : (x : M) → Module 𝕜 (V x)] [inst_7 : (x : M) → TopologicalSpace (V x)] [inst_8 : FiberBundle F V]
  [inst_9 : VectorBundle 𝕜 F V] {ι : Type u_7} {x : M} (e : Bundle.Trivialization F Bundle.TotalSpace.proj)
  [inst_10 : MemTrivializationAtlas e] (b : Module.Basis ι 𝕜 F) {i : ι} (hx : x ∈ e.baseSet),
  e.localFrame b i x = (e.basisAt b hx) i
-- Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer
CategoryTheory.IsSplitEqualizer.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {W : C} {ι : W ⟶ X}
  (leftRetraction : X ⟶ W) (rightRetraction : Y ⟶ X)
  (condition :
    autoParam (CategoryTheory.CategoryStruct.comp ι f = CategoryTheory.CategoryStruct.comp ι g)
      CategoryTheory.IsSplitEqualizer.condition._autoParam)
  (ι_leftRetraction :
    autoParam (CategoryTheory.CategoryStruct.comp ι leftRetraction = CategoryTheory.CategoryStruct.id W)
      CategoryTheory.IsSplitEqualizer.ι_leftRetraction._autoParam)
  (bottom_rightRetraction :
    autoParam (CategoryTheory.CategoryStruct.comp g rightRetraction = CategoryTheory.CategoryStruct.id X)
      CategoryTheory.IsSplitEqualizer.bottom_rightRetraction._autoParam)
  (top_rightRetraction :
    autoParam
      (CategoryTheory.CategoryStruct.comp f rightRetraction = CategoryTheory.CategoryStruct.comp leftRetraction ι)
      CategoryTheory.IsSplitEqualizer.top_rightRetraction._autoParam)
  (leftRetraction_1 : X ⟶ W) (rightRetraction_1 : Y ⟶ X)
  (condition_1 :
    autoParam (CategoryTheory.CategoryStruct.comp ι f = CategoryTheory.CategoryStruct.comp ι g)
      CategoryTheory.IsSplitEqualizer.condition._autoParam)
  (ι_leftRetraction_1 :
    autoParam (CategoryTheory.CategoryStruct.comp ι leftRetraction_1 = CategoryTheory.CategoryStruct.id W)
      CategoryTheory.IsSplitEqualizer.ι_leftRetraction._autoParam)
  (bottom_rightRetraction_1 :
    autoParam (CategoryTheory.CategoryStruct.comp g rightRetraction_1 = CategoryTheory.CategoryStruct.id X)
      CategoryTheory.IsSplitEqualizer.bottom_rightRetraction._autoParam)
  (top_rightRetraction_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp f rightRetraction_1 = CategoryTheory.CategoryStruct.comp leftRetraction_1 ι)
      CategoryTheory.IsSplitEqualizer.top_rightRetraction._autoParam),
  ({ leftRetraction := leftRetraction, rightRetraction := rightRetraction, condition := condition,
        ι_leftRetraction := ι_leftRetraction, bottom_rightRetraction := bottom_rightRetraction,
        top_rightRetraction := top_rightRetraction } =
      { leftRetraction := leftRetraction_1, rightRetraction := rightRetraction_1, condition := condition_1,
        ι_leftRetraction := ι_leftRetraction_1, bottom_rightRetraction := bottom_rightRetraction_1,
        top_rightRetraction := top_rightRetraction_1 }) =
    (leftRetraction = leftRetraction_1 ∧ rightRetraction = rightRetraction_1)
-- Mathlib.Topology.Instances.NNReal.Lemmas
/-- `x ↦ x ^ n` as an order isomorphism of `ℝ≥0∞`.

See also `ENNReal.orderIsoRpow`.  -/
ENNReal.powOrderIso : (n : ℕ) → n ≠ 0 → ENNReal ≃o ENNReal
-- Mathlib.Algebra.Group.Irreducible.Lemmas
/-- Irreducibility is preserved by multiplicative equivalences.

Note that surjective + local hom is not enough. Consider the additive monoids `M = ℕ ⊕ ℕ`, `N = ℕ`,
with x surjective local (additive) hom `f : M →+ N` sending `(m, n)` to `2m + n`.
It is local because the only add unit in `N` is `0`, with preimage `{(0, 0)}` also an add unit.
Then `x = (1, 0)` is irreducible in `M`, but `f x = 2 = 1 + 1` is not irreducible in `N`.  -/
Irreducible.map : ∀ {F : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Monoid M] [inst_1 : Monoid N] {x : M} [inst_2 : EquivLike F M N]
  [MulEquivClass F M N] (f : F), Irreducible x → Irreducible (f x)
-- Mathlib.LinearAlgebra.Matrix.Swap
Matrix.conjTranspose_swap : ∀ {n : Type u_2} [inst : DecidableEq n] {R : Type u_3} [inst_1 : NonAssocSemiring R] [inst_2 : StarRing R] (i j : n),
  (Matrix.swap R i j).conjTranspose = Matrix.swap R i j
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
not_linearIndependent_iff_finsupp : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {v : ι → M}, ¬LinearIndependent R v ↔ ∃ f, (f.sum fun x r => r • v x) = 0 ∧ f ≠ 0
-- Mathlib.Order.WellFoundedSet
Set.WellFoundedOn.mono' : ∀ {α : Type u_2} {r r' : α → α → Prop} {s : Set α},
  (∀ a ∈ s, ∀ b ∈ s, r' a b → r a b) → s.WellFoundedOn r → s.WellFoundedOn r'
-- Std.Data.TreeSet.Raw.Basic
/-- Tries to retrieve the smallest element of the tree set, panicking if the set is empty.
 -/
Std.TreeSet.Raw.min! : {α : Type u} → {cmp : α → α → Ordering} → [Inhabited α] → Std.TreeSet.Raw α cmp → α
-- Mathlib.Topology.Algebra.Module.Basic
Submodule.smul_closure_subset : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [ContinuousConstSMul R M] (s : Submodule R M) (c : R), c • closure ↑s ⊆ closure ↑s
-- Mathlib.Topology.Constructions.SumProd
frontier_prod_univ_eq : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (s : Set X),
  frontier (s ×ˢ Set.univ) = frontier s ×ˢ Set.univ
-- Batteries.Data.List.Lemmas
List.swap_cons_zero_right : ∀ {α : Type u_1} {a : α} {xs : List α} {i : ℕ}, (a :: xs).swap (i + 1) 0 = xs[i]?.getD a :: xs.set i a
-- Mathlib.Order.GaloisConnection.Defs
/-- If there exists an `b` such that `a = l b`, then `b = u a` is one such element.  -/
GaloisConnection.exists_eq_l : ∀ {α : Type u} {β : Type v} [inst : PartialOrder α] [inst_1 : Preorder β] {u : α → β} {l : β → α},
  GaloisConnection l u → ∀ (a : α), (∃ b, a = l b) ↔ a = l (u a)
-- Std.Tactic.BVDecide.Normalize.Canonicalize
Std.Tactic.BVDecide.Normalize.BitVec.ne_to_beq : ∀ {w : ℕ} (a b : BitVec w), (a ≠ b) = ((!a == b) = true)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
SimpleGraph.Walk.IsSubwalk.cons : ∀ {V : Type u_1} {G : SimpleGraph V} {u v u' v' w : V} {p : G.Walk u v} {q : G.Walk u' v'},
  p.IsSubwalk q → ∀ (h : G.Adj w u'), p.IsSubwalk (SimpleGraph.Walk.cons h q)
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.rnDeriv_ne_top : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ η : ProbabilityTheory.Kernel α γ)
  [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] {a : α},
  ∀ᵐ (x : γ) ∂η a, κ.rnDeriv η a x ≠ ⊤
-- Mathlib.Order.DirectedInverseSystem
DirectLimit.mk_apply : ∀ {ι : Type u_1} [inst : Preorder ι] {F : ι → Type u_4} {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8}
  {f : (i j : ι) → (h : i ≤ j) → T h} [inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)]
  [inst_2 : DirectedSystem F fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] (i j : ι) (x : F i)
  (h : i ≤ j), ⟦⟨j, (f i j h) x⟩⟧ = ⟦⟨i, x⟩⟧
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Over.changeProp_obj_left : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T} {X : T}
  [inst_1 : Q.IsMultiplicative] {P' Q' : CategoryTheory.MorphismProperty T} [inst_2 : Q'.IsMultiplicative]
  (hPP' : P ≤ P') (hQQ' : Q ≤ Q') (Y : P.Over Q X),
  ((CategoryTheory.MorphismProperty.Over.changeProp X hPP' hQQ').obj Y).left = Y.left
-- Init.Grind.Offset
Lean.Grind.Nat.ro_eq_false_of_lo : ∀ (u v k₁ k₂ : ℕ), Lean.Grind.isLt k₂ k₁ = true → u + k₁ ≤ v → (v ≤ u + k₂) = False
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.zip.eq_1 : ∀ {α : Type u} {β : Type u_1} (as : Array α) (bs : Array β), as.zip bs = Array.zipWith Prod.mk as bs
-- Mathlib.Algebra.Star.Pointwise
Set.star_inv' : ∀ {α : Type u_1} [inst : GroupWithZero α] [inst_1 : StarMul α] (s : Set α), star s⁻¹ = (star s)⁻¹
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.toVal_ratCast : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : DivisionRing R]
  (v : Valuation R Γ₀) (q : ℚ), WithVal.toVal v ↑q = ↑q
-- Mathlib.Order.Minimal
minimalFor_iff_forall_lt : ∀ {ι : Type u_1} {α : Type u_2} [inst : Preorder α] {Q : ι → Prop} {f : ι → α} {i : ι},
  MinimalFor Q f i ↔ Q i ∧ ∀ ⦃j : ι⦄, f j < f i → ¬Q j
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
GaloisConnection.l_csSup : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] [inst_1 : ConditionallyCompleteLattice β]
  {l : α → β} {u : β → α}, GaloisConnection l u → ∀ {s : Set α}, s.Nonempty → BddAbove s → l (sSup s) = ⨆ x, l ↑x
-- Mathlib.Order.Interval.Set.ProjIcc
Set.IicExtend_of_le : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] {b x : α} (f : ↑(Set.Iic b) → β),
  b ≤ x → Set.IicExtend f x = f ⟨b, ⋯⟩
-- Mathlib.Data.Num.Bitwise
Num.instHShiftRightNat : HShiftRight Num ℕ Num
-- Mathlib.RepresentationTheory.Continuous.Basic
/-- The underlying module of the coinduced continuous representation.  -/
ContRepresentation.coindV : {R : Type u_1} →
  {V : Type u_3} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : TopologicalSpace V] →
          [inst_3 : IsTopologicalAddGroup V] →
            [inst_4 : Module R V] →
              {G : Type u_7} →
                {H : Type u_8} →
                  [inst_5 : Group G] →
                    [inst_6 : TopologicalSpace G] →
                      [inst_7 : TopologicalSpace R] →
                        [inst_8 : ContinuousSMul R V] →
                          [inst_9 : Group H] →
                            [inst_10 : TopologicalSpace H] → (G →ₜ* H) → ContRepresentation R G V → Submodule R C(H, V)
-- Mathlib.CategoryTheory.Functor.TwoSquare
/-- The natural transformation associated to a 2-square.  -/
CategoryTheory.TwoSquare.natTrans : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      {C₄ : Type u₄} →
        [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
          [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
            [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] →
                {T : CategoryTheory.Functor C₁ C₂} →
                  {L : CategoryTheory.Functor C₁ C₃} →
                    {R : CategoryTheory.Functor C₂ C₄} →
                      {B : CategoryTheory.Functor C₃ C₄} → CategoryTheory.TwoSquare T L R B → (T.comp R ⟶ L.comp B)
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
/-- The isomorphism from `ZMod n` to any additive group of `Nat.card` equal to `n`
generated by a single element `g` which sends `1` to `g`.
See `zmodAddCyclicAddEquiv` for a version which doesn't take an explicit generator,
and instead picks one out with the axiom of choice.  -/
zmodAddEquivOfGenerator : {G : Type u_2} →
  [inst : AddGroup G] → {g : G} → (∀ (x : G), x ∈ AddSubgroup.zmultiples g) → {n : ℕ} → Nat.card G = n → ZMod n ≃+ G
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.instIsAddMonHomHom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {M N : CategoryTheory.AddMon C} (f : M ⟶ N), CategoryTheory.IsAddMonHom f.hom
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.inter!_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ m₃ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF → m₂.WF → m₃.WF → m₁.Equiv m₂ → (m₁.inter! m₃).Equiv (m₂.inter! m₃)
-- Init.Data.SInt.Bitwise
Int64.toInt_not : ∀ (a : Int64), (~~~a).toInt = (-a.toInt - 1).bmod (2 ^ 64)
-- Mathlib.Data.Set.Basic
/-- **Alias** of `Set.ofPred_injective`. -/
Set.setOf_injective : ∀ {α : Type u}, Function.Injective Set.ofPred
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey?_modify_eq_minKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {k : α} {f : β → β}, (t.modify k f).minKey? = t.minKey?
-- Lean.Data.Lsp.Basic
/-- Signals the end of progress reporting.  -/
Lean.Lsp.WorkDoneProgressEnd : Type
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.vanishingIdeal_union : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (t t' : Set (ProjectiveSpectrum 𝒜)),
  ProjectiveSpectrum.vanishingIdeal (t ∪ t') =
    ProjectiveSpectrum.vanishingIdeal t ⊓ ProjectiveSpectrum.vanishingIdeal t'
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
/-- Transfer preservation of finite limits along a natural isomorphism in the functor.  -/
CategoryTheory.Limits.preservesFiniteLimits_of_natIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (h : F ≅ G) [CategoryTheory.Limits.PreservesFiniteLimits F],
  CategoryTheory.Limits.PreservesFiniteLimits G
-- Mathlib.CategoryTheory.Types.Basic
CategoryTheory.ofTypeFunctor_map : ∀ (m : Type u → Type v) [inst : Functor m] [inst_1 : LawfulFunctor m] {X Y : Type u} (f : X ⟶ Y),
  (CategoryTheory.ofTypeFunctor m).map f = TypeCat.ofHom (Functor.map ⇑(TypeCat.Hom.hom f))
-- Mathlib.RingTheory.Flat.Tensor
/-- `CharacterModule M` is an injective module iff `M` is flat.
See [Lambek_1964] for a self-contained proof.  -/
Module.Flat.iff_characterModule_injective : ∀ {R : Type u} {M : Type v} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Small.{v, u} R],
  Module.Flat R M ↔ Module.Injective R (CharacterModule M)
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.prod.leftUnitorEquivalence.eq_1 : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.prod.leftUnitorEquivalence C =
    { functor := CategoryTheory.prod.leftUnitor C, inverse := CategoryTheory.prod.leftInverseUnitor C,
      unitIso := CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.Discrete PUnit.{w + 1} × C)),
      counitIso :=
        CategoryTheory.Iso.refl ((CategoryTheory.prod.leftInverseUnitor C).comp (CategoryTheory.prod.leftUnitor C)),
      functor_unitIso_comp := ⋯ }
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.CWComplex.Subcomplex.mk'_I : ∀ {X : Type u_1} [t : TopologicalSpace X] [inst : T2Space X] (C : Set X) [inst_1 : Topology.CWComplex C] (E : Set X)
  (I : (n : ℕ) → Set (Topology.RelCWComplex.cell C n))
  (closedCell_subset : ∀ (n : ℕ) (i : ↑(I n)), Topology.RelCWComplex.closedCell n ↑i ⊆ E)
  (union : ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j = E) (n : ℕ),
  (Topology.CWComplex.Subcomplex.mk' C E I closedCell_subset union).I n = I n
-- Mathlib.Topology.MetricSpace.UniformConvergence
/-- The natural `EMetric` structure on `α →ᵤ[𝔖] β` when `𝔖` is finite given by
`edist f g = ⨆ x ∈ ⋃₀ 𝔖, edist (f x) (g x)`.  -/
UniformOnFun.instPseudoEMetricSpace : {α : Type u_1} →
  {β : Type u_2} → {𝔖 : Set (Set α)} → [PseudoEMetricSpace β] → [Finite ↑𝔖] → PseudoEMetricSpace (UniformOnFun α β 𝔖)
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.OplaxRightLinear.δᵣ_associativity_inv : ∀ {D : Type u_1} {D' : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} D]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D'] (F : CategoryTheory.Functor D D') {C : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C] [inst_3 : CategoryTheory.MonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D]
  [inst_5 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D'] [inst_6 : F.OplaxRightLinear C] (d : D)
  (c c' : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OplaxRightLinear.δᵣ F
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c) c')
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft
          (CategoryTheory.Functor.OplaxRightLinear.δᵣ F d c) c')
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso (F.obj d) c c').inv) =
    CategoryTheory.CategoryStruct.comp
      (F.map (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c c').inv)
      (CategoryTheory.Functor.OplaxRightLinear.δᵣ F d (CategoryTheory.MonoidalCategoryStruct.tensorObj c c'))
-- Mathlib.NumberTheory.NumberField.House
_private.Mathlib.NumberTheory.NumberField.House.0.NumberField.house.asiegel_remark : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] {α : Type u_2} {β : Type u_3}
  (a : Matrix α β (NumberField.RingOfIntegers K)) [inst_2 : Fintype β] {A : ℝ},
  (∀ (k : α) (l : β), NumberField.house ((algebraMap (NumberField.RingOfIntegers K) K) (a k l)) ≤ A) →
    ∀ [inst_3 : DecidableEq (K →+* ℂ)] [inst_4 : Fintype α],
      0 ≤ A → ‖NumberField.house.asiegel✝ K a‖ ≤ NumberField.house.c₂✝ K * A
-- Mathlib.Analysis.Convex.Exposed
exposedPoints_empty : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : TopologicalSpace 𝕜] [inst_1 : Ring 𝕜] [inst_2 : PartialOrder 𝕜]
  [inst_3 : AddCommMonoid E] [inst_4 : TopologicalSpace E] [inst_5 : Module 𝕜 E], Set.exposedPoints 𝕜 ∅ = ∅
-- Mathlib.Combinatorics.SimpleGraph.Density
SimpleGraph.card_interedges_div_card : ∀ {α : Type u_4} (G : SimpleGraph α) [inst : DecidableRel G.Adj] (s t : Finset α),
  ↑(G.interedges s t).card / (↑s.card * ↑t.card) = G.edgeDensity s t
-- Mathlib.Algebra.Group.Action.Pi
Function.hasVAdd.eq_1 : ∀ {ι : Type u_1} {M : Type u_2} {α : Type u_7} [inst : VAdd M α], Function.hasVAdd = Pi.instVAdd
-- Mathlib.Topology.Constructions
IsClosedMap.subtype_coind : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {p : X → Prop} {f : Y → X},
  IsClosedMap f → ∀ (hp : ∀ (x : Y), p (f x)), IsClosedMap (Subtype.coind f hp)
-- Mathlib.Analysis.Normed.Group.Basic
enorm_add₄_le : ∀ {E : Type u_8} [inst : TopologicalSpace E] [inst_1 : ESeminormedAddMonoid E] {a b c d : E},
  ‖a + b + c + d‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ + ‖c‖ₑ + ‖d‖ₑ
-- Init.PropLemmas
forall_eq_or_imp : ∀ {α : Sort u_1} {a' : α} {P Q : α → Prop}, (∀ (a : α), a = a' ∨ Q a → P a) ↔ P a' ∧ ∀ (a : α), Q a → P a
-- Mathlib.CategoryTheory.IsConnected
/-- For objects `X Y : C`, any natural transformation `α : const X ⟶ const Y` from a connected
category must be constant.
This is the key property of connected categories which we use to establish properties about limits.
 -/
CategoryTheory.nat_trans_from_is_connected : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type w₂} [inst_1 : CategoryTheory.Category.{w₁, w₂} C]
  [CategoryTheory.IsPreconnected J] {X Y : C}
  (α : (CategoryTheory.Functor.const J).obj X ⟶ (CategoryTheory.Functor.const J).obj Y) (j j' : J), α.app j = α.app j'
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Summable.tsum_finsetSum : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α]
  {L : SummationFilter β} [T2Space α] [ContinuousAdd α] [L.NeBot] {f : γ → β → α} {s : Finset γ},
  (∀ i ∈ s, Summable (f i) L) → ∑'[L] (b : β), ∑ i ∈ s, f i b = ∑ i ∈ s, ∑'[L] (b : β), f i b