mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplexCategory.Truncated
SimplexCategory.Truncated.δ₂_two_comp_σ₂_one : CategoryTheory.CategoryStruct.comp
    (SimplexCategory.Truncated.δ₂ 2 SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_1
      SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_2)
    (SimplexCategory.Truncated.σ₂ 1 SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_2
      SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_1) =
  CategoryTheory.CategoryStruct.id
    { obj := { len := 1 }, property := SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one._proof_1 }
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.Measure.real.eq_1 : ∀ {α : Type u_6} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (s : Set α), μ.real s = (μ s).toReal
-- Mathlib.Order.Bounds.Basic
Nat.instDecidableIsLeast : (p : ℕ → Prop) → (n : ℕ) → [DecidablePred p] → Decidable (IsLeast {n | p n} n)
-- Init.MetaTypes
Lean.Meta.DSimp.Config.mk : Bool →
  Bool →
    Bool →
      Lean.Meta.EtaStructMode →
        Bool → Bool → Bool → Bool → Bool → Bool → Bool → Bool → Bool → Bool → Bool → Bool → Lean.Meta.DSimp.Config
-- Lean.CoreM
/-- Name generator for producing unique `FVarId`s, `MVarId`s, and `LMVarId`s  -/
Lean.Core.State.ngen : Lean.Core.State → Lean.NameGenerator
-- Std.Data.ExtTreeMap.Basic
/-- Given a proof that the tree map is not empty, retrieves the key-value pair with the smallest key.
 -/
Std.ExtTreeMap.minEntry : {α : Type u} →
  {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → (t : Std.ExtTreeMap α β cmp) → t ≠ ∅ → α × β
-- Mathlib.Order.WithBot
WithBot.map_le_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {x y : WithBot α} (f : α → β),
  (∀ {a b : α}, f a ≤ f b ↔ a ≤ b) → (WithBot.map f x ≤ WithBot.map f y ↔ x ≤ y)
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.prod_homCategory_id_fst : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C] (X Y : B × C)
  (X_1 : (X.1 ⟶ Y.1) × (X.2 ⟶ Y.2)), (CategoryTheory.CategoryStruct.id X_1).1 = CategoryTheory.CategoryStruct.id X_1.1
-- Init.Data.Iterators.Consumers.Loop
/-- A `ForIn'` instance for iterators. Its generic membership relation is not easy to use,
so this is not marked as `instance`. This way, more convenient instances can be built on top of it
or future library improvements will make it more comfortable.
 -/
Std.Iter.instForIn' : {α β : Type w} →
  {n : Type x → Type x'} →
    [Monad n] →
      [inst : Std.Iterator α Id β] →
        [Std.IteratorLoop α Id n] → ForIn' n (Std.Iter β) β { mem := fun it out => it.IsPlausibleIndirectOutput out }
-- Mathlib.RingTheory.SimpleModule.Basic
IsSemisimpleModule.sSup_simples_eq_top : ∀ (R : Type u_2) [inst : Ring R] (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [IsSemisimpleModule R M], sSup {m | IsSimpleModule R ↥m} = ⊤
-- Mathlib.Algebra.Group.Submonoid.Units
/-- The equivalence between the subgroup of units of `S` and the submonoid of unit
elements of `S`.  -/
Submonoid.unitsEquivIsUnitSubmonoid : {M : Type u_1} → [inst : Monoid M] → (S : Submonoid M) → ↥S.units ≃* ↥(IsUnit.submonoid ↥S)
-- Std.Data.DTreeMap.Basic
/-- Erases multiple mappings from the tree map by iterating over the given collection and calling
`erase`.
 -/
Std.DTreeMap.eraseMany : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → {ρ : Type u_1} → [ForIn Id ρ α] → Std.DTreeMap α β cmp → ρ → Std.DTreeMap α β cmp
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.Hom.sqFrom_comp : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ C₃ : HomologicalComplex V c}
  (f : C₁ ⟶ C₂) (g : C₂ ⟶ C₃) (i : ι),
  HomologicalComplex.Hom.sqFrom (CategoryTheory.CategoryStruct.comp f g) i =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.sqFrom f i) (HomologicalComplex.Hom.sqFrom g i)
-- Mathlib.Topology.Neighborhoods
/-- A filter lies below the neighborhood filter at `x` iff it contains every open set around `x`.  -/
le_nhds_iff : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {f : Filter X}, f ≤ nhds x ↔ ∀ (s : Set X), x ∈ s → IsOpen s → s ∈ f
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
SimpleGraph.TripartiteFromTriangles.Rel.in₀₁ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄,
  (a, b, c) ∈ t → SimpleGraph.TripartiteFromTriangles.Rel t (Sum3.in₀ a) (Sum3.in₁ b)
-- Mathlib.Algebra.Module.SpanRank
Submodule.FG.spanRank_eq_spanFinrank : ∀ {R : Type u_1} {M : Type u} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {p : Submodule R M},
  p.FG → p.spanRank = ↑p.spanFinrank
-- Mathlib.Algebra.Module.ZLattice.Basic
Module.Basis.ofZLatticeComap.eq_1 : ∀ (K : Type u_1) [inst : NormedField K] {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace K E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace K F] (L : Submodule ℤ E)
  (e : F ≃ₗ[K] E) {ι : Type u_4} (b : Module.Basis ι ℤ ↥L),
  Module.Basis.ofZLatticeComap K L e b = b.map (ZLattice.comap_equiv K L e)
-- Mathlib.Tactic.ClickSuggestions.Rewrite
/-- Whether the two suggestions are duplicates of each other.  -/
Mathlib.Tactic.ClickSuggestions.RwKey.isDuplicate : Mathlib.Tactic.ClickSuggestions.RwKey → Mathlib.Tactic.ClickSuggestions.RwKey → Lean.MetaM Bool
-- Lean.Meta.Tactic.Grind.Anchor
Lean.Meta.Grind.mkAnchorSyntax : ℕ → UInt64 → Lean.CoreM (Lean.TSyntax `Lean.Parser.Tactic.anchor)
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.simpExtensionMapRef : IO.Ref Lean.Meta.SimpExtensionMap
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.opcyclesToE_ιE_assoc : ∀ {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.opcyclesToE_ιE._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.opcyclesToE_ιE._auto_3) {Z : C}
  (h : X.opcycles f₂ f₃ n₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂)
      (CategoryTheory.CategoryStruct.comp (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) h) =
    CategoryTheory.CategoryStruct.comp
      (X.opcyclesMap f₁₂ f₃ f₂ f₃ (CategoryTheory.ComposableArrows.threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₁) h
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKey!_insert_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {k : α} {v : β k}, t.isEmpty = true → (t.insert k v).minKey! = k
-- Mathlib.Data.Fin.Fin2
Fin2.rev.eq_1 : ∀ (n_1 : ℕ), Fin2.fz.rev = Fin2.last
-- Std.Http.Data.URI.Basic
/-- Whether the path is absolute (begins with '/') or relative.
 -/
Std.Http.URI.Path.absolute : Std.Http.URI.Path → Bool
-- Mathlib.Analysis.Calculus.ImplicitContDiff
/-- **Alias** of `ContDiffAt.contDiffAt_implicitFunction`.

---

If the implicit equation `f` is $C^n$ at `(u₁, u₂)`, then its implicit function `ψ` around `u₁`
is also $C^n$ at `u₁`.  -/
IsContDiffImplicitAt.contDiffAt_implicitFunction : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E₁ : Type u_2} [inst_1 : NormedAddCommGroup E₁] [inst_2 : NormedSpace 𝕜 E₁]
  [inst_3 : CompleteSpace E₁] {E₂ : Type u_3} [inst_4 : NormedAddCommGroup E₂] [inst_5 : NormedSpace 𝕜 E₂]
  [inst_6 : CompleteSpace E₂] {F : Type u_4} [inst_7 : NormedAddCommGroup F] [inst_8 : NormedSpace 𝕜 F]
  [inst_9 : CompleteSpace F] {u : E₁ × E₂} {f : E₁ × E₂ → F} {n : WithTop ℕ∞} (cdf : ContDiffAt 𝕜 n f u) (pn : n ≠ 0)
  (if₂ : (fderiv 𝕜 f u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible),
  ContDiffAt 𝕜 n (cdf.implicitFunction pn if₂) u.1
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.filter : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} (f : (a : α) → β a → Bool),
  m₁.Equiv m₂ → (Std.DHashMap.filter f m₁).Equiv (Std.DHashMap.filter f m₂)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKey!_erase_eq_of_not_compare_maxKey!_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF → ∀ {k : α}, (t.erase k).isEmpty = false → ¬cmp k t.maxKey! = Ordering.eq → (t.erase k).maxKey! = t.maxKey!
-- Std.Internal.Do.WP.Basic
/-- Soundness of `bind`: composing weakest preconditions is at least as strong as the weakest
precondition of `>>=`.  -/
Std.Internal.Do.WPMonad.bind_le_wp_bind : ∀ {m : Type u → Type v} {Pred : outParam (Type w)} {EPred : outParam (Type w')} {inst : Monad m}
  {inst_1 : Std.Internal.Do.Assertion Pred} {inst_2 : Std.Internal.Do.Assertion EPred}
  [self : Std.Internal.Do.WPMonad m Pred EPred] {α β : Type u} (x : m α) (f : α → m β) (post : β → Pred)
  (epost : EPred),
  Lean.Order.PartialOrder.rel (Std.Internal.Do.wp x (fun a => Std.Internal.Do.wp (f a) post epost) epost)
    (Std.Internal.Do.wp (x >>= f) post epost)
-- Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
/-- The extension of `inductiveSystem iter` to a functor `Set.Iic j ⥤ C` which
sends the top element to the colimit of `inductiveSystem iter`.  -/
CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.functor : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {Φ : CategoryTheory.SmallObject.SuccStruct C} →
      {J : Type u} →
        [inst_1 : LinearOrder J] →
          [inst_2 : OrderBot J] →
            [inst_3 : SuccOrder J] →
              [inst_4 : WellFoundedLT J] →
                [inst_5 : CategoryTheory.Limits.HasIterationOfShape J C] →
                  {j : J} →
                    Order.IsSuccLimit j → ((i : J) → i < j → Φ.Iteration i) → CategoryTheory.Functor (↑(Set.Iic j)) C
-- Mathlib.RingTheory.Jacobson.Radical
Ring.jacobson_lt_top : ∀ (R : Type u_1) [inst : Ring R] [Nontrivial R], Ring.jacobson R < ⊤
-- Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
CategoryTheory.whiskeringRightPreservesColimits : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  (F : CategoryTheory.Functor D E) [CategoryTheory.Limits.HasColimitsOfSize.{w, w', v_2, u_2} D]
  [CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v_2, v_3, u_2, u_3} F],
  CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', max u_1 v_2, max u_1 v_3, max (max (max u_1 u_2) v_1) v_2,
      max (max (max u_1 u_3) v_1) v_3}
    ((CategoryTheory.Functor.whiskeringRight C D E).obj F)
-- Lean.Elab.Tactic.Induction
/-- Given `inductionAlts` of the form
```
syntax inductionAlts := "with " (tactic)? withPosition( (colGe inductionAlt)*)
```
runs `cont (some alts)` where `alts` is an array containing all `inductionAlt`s while disabling incremental
reuse if any other syntax changed. If there's no `with` clause, then runs `cont none`.
 -/
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.withAltsOfOptInductionAlts : {α : Type} → Lean.Syntax → (Option (Array Lean.Syntax) → Lean.Elab.Tactic.TacticM α) → Lean.Elab.Tactic.TacticM α
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.isSome_get?_iff_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {a : α}, (m.get? a).isSome = true ↔ a ∈ m
-- Mathlib.Topology.Spectral.Prespectral
instTotallySeparatedSpaceOfT2SpaceOfPrespectralSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X] [PrespectralSpace X], TotallySeparatedSpace X
-- Lean.Parser.Basic
Lean.Parser.skip : Lean.Parser.Parser
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.constantCoeff_toSubring : ∀ {σ : Type u_1} {R : Type u_2} [inst : Ring R] (p : MvPowerSeries σ R) (T : Subring R)
  (hp : ∀ (n : σ →₀ ℕ), (MvPowerSeries.coeff n) p ∈ T),
  ↑(MvPowerSeries.constantCoeff (p.toSubring T hp)) = MvPowerSeries.constantCoeff p
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey?_erase_le_maxKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k km kme : α} (hkme : (t.erase k).maxKey? = some kme), t.maxKey?.get ⋯ = km → (cmp kme km).isLE = true
-- Mathlib.Data.Fintype.Card
Fintype.card_subtype_mono : ∀ {α : Type u_1} (p q : α → Prop),
  p ≤ q →
    ∀ [inst : Fintype { x // p x }] [inst_1 : Fintype { x // q x }],
      Fintype.card { x // p x } ≤ Fintype.card { x // q x }
-- Mathlib.Algebra.Lie.SerreConstruction
CartanMatrix.Generators.H.inj : ∀ {B : Type v} {a a_1 : B}, CartanMatrix.Generators.H a = CartanMatrix.Generators.H a_1 → a = a_1
-- Init.Data.SInt.Float32
/-- Truncates a floating-point number to the nearest 64-bit signed integer, rounding towards zero.

If the `Float` is larger than the maximum value for `Int64` (including `Inf`), returns the maximum
value of `Int64` (i.e. `Int64.maxValue`). If it is smaller than the minimum value for `Int64`
(including `-Inf`), returns the minimum value of `Int64` (i.e. `Int64.minValue`). If it is `NaN`,
returns `0`.

This function does not reduce in the kernel.
 -/
Float32.toInt64 : Float32 → Int64
-- Mathlib.Analysis.Analytic.IsolatedZeros
AnalyticOnNhd.eqOn_zero_of_preconnected_of_mem_closure : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜} {U : Set 𝕜},
  AnalyticOnNhd 𝕜 f U → IsPreconnected U → z₀ ∈ U → z₀ ∈ closure ({z | f z = 0} \ {z₀}) → Set.EqOn f 0 U
-- Mathlib.Algebra.Quaternion
/-- The equivalence between the quaternions over `R` and `R × R × R × R`.  -/
Quaternion.equivProd : (R : Type u_1) → [inst : Zero R] → [inst_1 : One R] → [inst_2 : Neg R] → Quaternion R ≃ R × R × R × R
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.le_sup_iff : ∀ {α : Type u} {u : Ultrafilter α} {f g : Filter α}, ↑u ≤ f ⊔ g ↔ ↑u ≤ f ∨ ↑u ≤ g
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.coe_add : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N : LieSubmodule R L M) (m m' : ↥N), ↑(m + m') = ↑m + ↑m'
-- Mathlib.Geometry.Manifold.Algebra.SMul
ContMDiffSMul.mk : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {H' : Type u_4}
  [inst_4 : TopologicalSpace H'] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'} {n : WithTop ℕ∞} {G : Type u_6} [inst_7 : TopologicalSpace G]
  [inst_8 : ChartedSpace H G] {M : Type u_7} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H' M]
  [inst_11 : SMul G M], (ContMDiff (I.prod I') I' n fun p => p.1 • p.2) → ContMDiffSMul I I' n G M
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.mem_sup_iff : ∀ {α : Type u_1} [inst : LE α] {s t : UpperSet α} {a : α}, a ∈ s ⊔ t ↔ a ∈ s ∧ a ∈ t
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- Adding a `weightedVSub` to an `affineCombination`.  -/
Finset.weightedVSub_vadd_affineCombination : ∀ {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] {ι : Type u_4} (s : Finset ι) (w₁ w₂ : ι → k) (p : ι → P),
  (s.weightedVSub p) w₁ +ᵥ (Finset.affineCombination k s p) w₂ = (Finset.affineCombination k s p) (w₁ + w₂)
-- Init.Data.BitVec.Bitblast
BitVec.msb_umod_of_le_of_ne_zero_of_le : ∀ {w : ℕ} {x y : BitVec w}, x ≤ BitVec.intMin w → y ≠ 0#w → y ≤ BitVec.intMin w → (x % y).msb = false
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.symm_coe_proj : ∀ {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] {x : B} {y : F}
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj), x ∈ e.baseSet → (↑e.symm (x, y)).proj = x
-- Mathlib.Analysis.CStarAlgebra.Unitization
/-- The norm on `Unitization 𝕜 E` satisfies the C⋆-property  -/
Unitization.instCStarRing : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : DenselyNormedField 𝕜] [inst_1 : NonUnitalNormedRing E] [inst_2 : StarRing E]
  [inst_3 : CStarRing E] [inst_4 : NormedSpace 𝕜 E] [inst_5 : IsScalarTower 𝕜 E E] [inst_6 : SMulCommClass 𝕜 E E]
  [inst_7 : StarRing 𝕜] [inst_8 : StarModule 𝕜 E] [CStarRing 𝕜], CStarRing (Unitization 𝕜 E)
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_spec_assoc : ∀ (X : AlgebraicGeometry.LocallyRingedSpace) (r : ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X)))
  {Z : CommRingCat}
  (h :
    ((TopCat.Presheaf.pushforward CommRingCat X.toΓSpecSheafedSpace.hom.base).obj X.presheaf).obj
        (Opposite.op (PrimeSpectrum.basicOpen r)) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CommRingCat.ofHom
        (algebraMap (↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X)))
          ((AlgebraicGeometry.structureSheafInType ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))
                  ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))).obj.obj
            (Opposite.op (PrimeSpectrum.basicOpen r)))))
      (CategoryTheory.CategoryStruct.comp (X.toΓSpecSheafedSpace.hom.c.app (Opposite.op (PrimeSpectrum.basicOpen r)))
        h) =
    CategoryTheory.CategoryStruct.comp (X.toToΓSpecMapBasicOpen r) h
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.norm_apply_le : ∀ {p : ENNReal} {ι : Type u_2} {β : ι → Type u_4} [hp : Fact (1 ≤ p)] [inst : Fintype ι]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (β i)] (x : PiLp p β) (i : ι), ‖x.ofLp i‖ ≤ ‖x‖
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.instDecidableEq.eq_1 : ∀ {α : Type u} [inst : AddMonoid α] [inst_1 : DecidableEq α] (x x_1 : AddUnits α),
  x.instDecidableEq x_1 = decidable_of_iff' (↑x = ↑x_1) ⋯
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.prod_monomial : ∀ {R : Type u_2} [inst : CommSemiring R] {ι : Type u_3} (f : ι → ℕ) (g : ι → R) (s : Finset ι),
  ∏ i ∈ s, (PowerSeries.monomial (f i)) (g i) = (PowerSeries.monomial (∑ i ∈ s, f i)) (∏ i ∈ s, g i)
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
IsEllipticNet.atom_neg_right : ∀ {R : Type u_1} [inst : CommRing R] (W : ℤ → R) (a b : ℤ), IsEllipticNet.atom W a (-b) = IsEllipticNet.atom W a b
-- Mathlib.Algebra.Group.Indicator
/-- **Alias** of `Set.mulIndicator_sdiff'`. -/
Set.mulIndicator_diff' : ∀ {α : Type u_1} {G : Type u_6} [inst : Group G] {s t : Set α},
  s ⊆ t → ∀ (f : α → G), (t \ s).mulIndicator f = t.mulIndicator f / s.mulIndicator f
-- Mathlib.RingTheory.Spectrum.Prime.Topology
/-- `nhds` as an order embedding.  -/
PrimeSpectrum.nhdsOrderEmbedding : {R : Type u} → [inst : CommSemiring R] → PrimeSpectrum R ↪o Filter (PrimeSpectrum R)
-- Mathlib.AlgebraicGeometry.Cover.QuasiCompact
/-- [Stacks Tag 022D](https://stacks.math.columbia.edu/tag/022D) ((1)) -/
AlgebraicGeometry.QuasiCompactCover.instCoverOfIsIso : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.ContainsIdentities] [inst_1 : P.RespectsIso]
  {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [inst_2 : CategoryTheory.IsIso f],
  AlgebraicGeometry.QuasiCompactCover (AlgebraicGeometry.Scheme.coverOfIsIso f).toPreZeroHypercover
-- Mathlib.Topology.CompactOpen
ContinuousMap.instT1Space : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T1Space Y], T1Space C(X, Y)
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.instDecidableRelDvd : {M : Type u_1} → [inst : CommMonoidWithZero M] → [DecidableRel fun x1 x2 => x1 ∣ x2] → DecidableRel fun x1 x2 => x1 ∣ x2
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.isFiniteMeasure : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (f : StieltjesFunction R)
  [inst_2 : OrderTopology R] [inst_3 : CompactIccSpace R] [inst_4 : MeasurableSpace R] [inst_5 : BorelSpace R]
  [inst_6 : SecondCountableTopology R] [inst_7 : DenselyOrdered R] {l u : ℝ},
  Filter.Tendsto (↑f) Filter.atBot (nhds l) →
    Filter.Tendsto (↑f) Filter.atTop (nhds u) → MeasureTheory.IsFiniteMeasure f.measure
-- Mathlib.Data.Set.Subsingleton
Set.nontrivial_of_nontrivial : ∀ {α : Type u} {s : Set α}, s.Nontrivial → Nontrivial α
-- Mathlib.RingTheory.Valuation.Quotient
Valuation.supp_quot_supp : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : CommRing R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀),
  (v.onQuot ⋯).supp = 0
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.IsElliptic.mk : ∀ {R : Type u} [inst : CommRing R] {W : WeierstrassCurve R}, IsUnit W.Δ → W.IsElliptic
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.obj.ι_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {F : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] {G : C} [inst_5 : CategoryTheory.GrpObj G],
  CategoryTheory.GrpObj.inv = F.map CategoryTheory.GrpObj.inv
-- Mathlib.Algebra.GroupWithZero.Action.Pi
Pi.mulActionWithZero' : {I : Type u} →
  {f : I → Type v} →
    {g : I → Type u_1} →
      [inst : (i : I) → MonoidWithZero (g i)] →
        [inst_1 : (i : I) → Zero (f i)] →
          [(i : I) → MulActionWithZero (g i) (f i)] → MulActionWithZero ((i : I) → g i) ((i : I) → f i)
-- Mathlib.Algebra.Notation.Support
Function.mulSupport_curry : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [inst : One M] (f : ι × κ → M),
  Function.mulSupport (Function.curry f) = Prod.fst '' Function.mulSupport f
-- Lean.Elab.PatternVar
Lean.Elab.Term.CollectPatternVars.instInhabitedContext.default : Lean.Elab.Term.CollectPatternVars.Context
-- Mathlib.CategoryTheory.Yoneda
/-- The "Coyoneda pairing" functor, which sends `X : C` and `F : C ⥤ Type`
to `coyoneda.rightOp.obj X ⟶ F`, functorially in both `X` and `F`.
 -/
CategoryTheory.coyonedaPairing : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    CategoryTheory.Functor (C × CategoryTheory.Functor C (Type v₁)) (Type (max u₁ v₁))
-- Mathlib.Order.Interval.Set.SuccPred
Set.insert_Ioc_succ_left_eq_Ioc : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] {a b : α},
  a < b → insert (Order.succ a) (Set.Ioc (Order.succ a) b) = Set.Ioc a b
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
OpenPartialHomeomorph.subtypeRestr_coe : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {s : TopologicalSpace.Opens X} (hs : Nonempty ↥s),
  ↑(e.subtypeRestr hs) = (↑s).domRestrict ↑e
-- Mathlib.MeasureTheory.Group.Prod
MeasureTheory.lintegral_lintegral_add_neg : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd₂ G] (μ ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableNeg G] [μ.IsAddLeftInvariant] [ν.IsAddLeftInvariant]
  (f : G → G → ENNReal),
  AEMeasurable (Function.uncurry f) (μ.prod ν) →
    ∫⁻ (x : G), ∫⁻ (y : G), f (y + x) (-x) ∂ν ∂μ = ∫⁻ (x : G), ∫⁻ (y : G), f x y ∂ν ∂μ
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.adjoin_mono : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] {s t : Set A},
  s ⊆ t → NonUnitalAlgebra.adjoin R s ≤ NonUnitalAlgebra.adjoin R t
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKeyD_erase_eq_of_not_compare_minKeyD_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k fallback : α},
  t.erase k ≠ ∅ → ¬cmp k (t.minKeyD fallback) = Ordering.eq → (t.erase k).minKeyD fallback = t.minKeyD fallback
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.eq_natCast_of_le_natCast : ∀ {a : Ordinal.{u_4}} {b : ℕ}, a ≤ ↑b → ∃ c, a = ↑c