mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.TransferInstance
Equiv.commSemigroup.eq_1 : ∀ {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : CommSemigroup β],
  e.commSemigroup = Function.Injective.commSemigroup ⇑e ⋯ ⋯
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.Equation.baseChange : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} {S : Type s} [inst_1 : CommRing S] {A : Type u}
  [inst_2 : CommRing A] {B : Type v} [inst_3 : CommRing B] [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  (f : A →ₐ[S] B) {P : Fin 3 → A}, (W'.baseChange A).Equation P → (W'.baseChange B).Equation (⇑f ∘ P)
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
QuadraticMap.tmul.congr_simp : ∀ {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} {N₁ : Type uN₁} {N₂ : Type uN₂} [inst : CommRing R]
  [inst_1 : CommRing A] [inst_2 : AddCommGroup M₁] [inst_3 : AddCommGroup M₂] [inst_4 : AddCommGroup N₁]
  [inst_5 : AddCommGroup N₂] [inst_6 : Algebra R A] [inst_7 : Module R M₁] [inst_8 : Module A M₁] [inst_9 : Module R N₁]
  [inst_10 : Module A N₁] [inst_11 : SMulCommClass R A M₁] [inst_12 : IsScalarTower R A M₁]
  [inst_13 : IsScalarTower R A N₁] [inst_14 : Module R M₂] [inst_15 : Module R N₂] [inst_16 : Invertible 2]
  (Q₁ Q₁_1 : QuadraticMap A M₁ N₁),
  Q₁ = Q₁_1 → ∀ (Q₂ Q₂_1 : QuadraticMap R M₂ N₂), Q₂ = Q₂_1 → Q₁.tmul Q₂ = Q₁_1.tmul Q₂_1
-- Mathlib.SetTheory.Cardinal.Continuum
Cardinal.continuum_mul_aleph0 : Cardinal.continuum * Cardinal.aleph0 = Cardinal.continuum
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestRevMatch.ne_endPos : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatch pat pos → pos ≠ s.endPos
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tsum_eq_sum' : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  {L : SummationFilter β} [L.LeAtTop] {s : Finset β}, Function.support f ⊆ ↑s → ∑'[L] (b : β), f b = ∑ b ∈ s, f b
-- Mathlib.Analysis.Normed.Group.Ultra
/-- Nonarchimedean norm of a product is less than or equal the norm of any term in the product.
This version is phrased using `Finset.sup'` and `Finset.Nonempty` due to `Finset.sup`
operating over an `OrderBot`, which `ℝ` is not.  -/
Finset.Nonempty.norm_prod_le_sup'_norm : ∀ {M : Type u_1} {ι : Type u_2} [inst : SeminormedCommGroup M] [IsUltrametricDist M] {s : Finset ι} (hs : s.Nonempty)
  (f : ι → M), ‖∏ i ∈ s, f i‖ ≤ s.sup' hs fun x => ‖f x‖
-- Mathlib.Combinatorics.Quiver.Covering
Prefunctor.IsCovering.comp : ∀ {U : Type u_1} [inst : Quiver U] {V : Type u_2} [inst_1 : Quiver V] (φ : U ⥤q V) {W : Type u_3} [inst_2 : Quiver W]
  (ψ : V ⥤q W), φ.IsCovering → ψ.IsCovering → (φ ⋙q ψ).IsCovering
-- Init.PropLemmas
Decidable.imp_iff_left_iff : ∀ {a b : Prop} [Decidable a], (b ↔ a → b) ↔ a ∨ b
-- Mathlib.Data.Int.ModEq
Int.existsUnique_equiv : ∀ (a : ℤ) {b : ℤ}, 0 < b → ∃ z, 0 ≤ z ∧ z < b ∧ z ≡ a [ZMOD b]
-- Mathlib.Algebra.DirectSum.Algebra
DirectSum.instAlgebra : {ι : Type uι} →
  (R : Type uR) →
    (A : ι → Type uA) →
      [inst : CommSemiring R] →
        [inst_1 : (i : ι) → AddCommMonoid (A i)] →
          [inst_2 : (i : ι) → Module R (A i)] →
            [inst_3 : AddMonoid ι] →
              [inst_4 : DirectSum.GSemiring A] →
                [DirectSum.GAlgebra R A] → [inst_6 : DecidableEq ι] → Algebra R (DirectSum ι fun i => A i)
-- Init.Data.List.Range
List.head?_range' : ∀ {s n : ℕ}, (List.range' s n).head? = if n = 0 then none else some s
-- Mathlib.Analysis.RCLike.Basic
RCLike.nnnorm_nsmul : ∀ (K : Type u_1) {E : Type u_2} [inst : RCLike K] [inst_1 : NormedAddCommGroup E] [NormedSpace K E] (n : ℕ) (x : E),
  ‖n • x‖₊ = n • ‖x‖₊
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₁₂.ι_D₂_assoc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_3} C₁₂] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₁₂] [inst_9 : CategoryTheory.Preadditive C₄]
  (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
  (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [inst_10 : F₁₂.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [inst_12 : G.Additive]
  [inst_13 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9}
  {ι₁₂ : Type u_10} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃)
  (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [inst_18 : DecidableEq ι₁₂]
  [inst_19 : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j j' : ι₄)
  (h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j) [inst_20 : HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄]
  {Z : C₄} (h_1 : (⋯.mapBifunctor K₃ G c₄).X j' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h)
      (CategoryTheory.CategoryStruct.comp ⋯ h_1) =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.d₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j') h_1
-- Mathlib.Algebra.LieRinehartAlgebra.Defs
/-- This is `LieRinehartAlgebra.Hom.apply_lie'` restated using the coercion to function rather
than `LieRinehartAlgebra.Hom.toLieHom`.  -/
LieRinehartAlgebra.Hom.apply_lie : ∀ {R : Type u_1} {A₁ : Type u_2} {L₁ : Type u_3} {A₂ : Type u_4} {L₂ : Type u_5} [inst : CommRing R]
  [inst_1 : CommRing A₁] [inst_2 : LieRing L₁] [inst_3 : Module A₁ L₁] [inst_4 : LieRingModule L₁ A₁]
  [inst_5 : CommRing A₂] [inst_6 : LieRing L₂] [inst_7 : Module A₂ L₂] [inst_8 : LieRingModule L₂ A₂]
  [inst_9 : Algebra R A₁] [inst_10 : LieAlgebra R L₁] [inst_11 : Algebra R A₂] [inst_12 : LieAlgebra R L₂]
  {σ₁₂ : A₁ →ₐ[R] A₂} (f : LieRinehartAlgebra.Hom σ₁₂ L₁ L₂) (a : A₁) (x : L₁), σ₁₂ ⁅x, a⁆ = ⁅f.toLieHom x, σ₁₂ a⁆
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.discreteTopology_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α],
  DiscreteTopology (TopologicalSpace.NonemptyCompacts α) ↔ DiscreteTopology α
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.FindAux.mk.congr_simp : ∀ {n : ℕ} (s s_1 : Array Batteries.UFNode) (e_s : s = s_1) (root root_1 : Fin n),
  root = root_1 →
    ∀ (size_eq : s.size = n), { s := s, root := root, size_eq := size_eq } = { s := s_1, root := root_1, size_eq := ⋯ }
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
UniformOnFun.hasBasis_uniformity_of_basis_aux₁ : ∀ (α : Type u_1) (β : Type u_2) {ι : Type u_4} [inst : UniformSpace β] (𝔖 : Set (Set α)) {p : ι → Prop}
  {s : ι → Set (β × β)},
  (uniformity β).HasBasis p s →
    ∀ (S : Set α), (uniformity (UniformOnFun α β 𝔖)).HasBasis p fun i => UniformOnFun.gen 𝔖 S (s i)
-- Mathlib.Algebra.Group.Subgroup.Map
MonoidHom.subgroupMap_surjective : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] (f : G →* G') (H : Subgroup G),
  Function.Surjective ⇑(f.subgroupMap H)
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.not_isLongestMatch_startPos : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] {s : String.Slice},
  ¬String.Slice.Pattern.Model.IsLongestMatch pat s.startPos
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
tendsto_measure_Icc_nhdsWithin_right' : ∀ (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasureOnCompacts μ] (b : ℝ),
  Filter.Tendsto (fun δ => μ (Set.Icc (b - δ) (b + δ))) (nhdsWithin 0 (Set.Ioi 0)) (nhds (μ {b}))
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Raw.fold.eq_1 : ∀ {α : Type u} {β : α → Type v} {δ : Type w} (f : δ → (a : α) → β a → δ) (init : δ) (b : Std.DHashMap.Raw α β),
  Std.DHashMap.Raw.fold f init b = (Std.DHashMap.Raw.foldM (fun x1 x2 x3 => pure (f x1 x2 x3)) init b).run
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.isUnsatDiseq_k : Int.Internal.Linear.Poly → Bool
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
/-- In the presence of 0-morphisms we can define a projection morphism from any coproduct.  -/
CategoryTheory.Limits.Sigma.π : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasZeroMorphisms C] →
      {β : Type w} →
        [DecidableEq β] → (f : β → C) → [inst_3 : CategoryTheory.Limits.HasCoproduct f] → (b : β) → ∐ f ⟶ f b
-- Mathlib.Order.UpperLower.Closure
LowerSet.Iic_sup_erase : ∀ {α : Type u_1} [inst : Preorder α] {s : LowerSet α} {a : α},
  a ∈ s → (∀ b ∈ s, a ≤ b → b = a) → LowerSet.Iic a ⊔ s.erase a = s
-- Mathlib.Order.RelClasses
instIsTransOfIsWellOrder : ∀ {α : Type u} (r : α → α → Prop) [IsWellOrder α r], IsTrans α r
-- Mathlib.Data.Nat.MaxPowDiv
Nat.pow_padicValNat_mul_divMaxPow : ∀ (p n : ℕ), p ^ padicValNat p n * n.divMaxPow p = n
-- Mathlib.CategoryTheory.Sites.Descent.IsPrestack
CategoryTheory.Pseudofunctor.presheafHom_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {S : C}
  (M N : ↑(F.obj { as := Opposite.op S })) (T : (CategoryTheory.Over S)ᵒᵖ),
  (F.presheafHom M N).obj T =
    ((F.map (Opposite.unop T).hom.op.toLoc).toFunctor.obj M ⟶ (F.map (Opposite.unop T).hom.op.toLoc).toFunctor.obj N)
-- Mathlib.Topology.Path
Path.add_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : Add X] [inst_2 : ContinuousAdd X] {a₁ b₁ a₂ b₂ : X}
  (γ₁ : Path a₁ b₁) (γ₂ : Path a₂ b₂) (a : ↑unitInterval), (γ₁.add γ₂) a = γ₁ a + γ₂ a
-- Init.Data.SInt.Basic
instLTInt8 : LT Int8
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.instMul : {R : Type u_1} → {a b : R} → [Mul R] → [Add R] → Mul (QuadraticAlgebra R a b)
-- Lean.Meta.Tactic.Grind.EMatch
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.getLHS : Array Lean.Expr → ℕ → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.coeMonad : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → Coe (CategoryTheory.Monad C) (CategoryTheory.Functor C C)
-- Mathlib.MeasureTheory.Function.UniformIntegrable
/-- The averaging of a uniformly integrable sequence is also uniformly integrable.  -/
MeasureTheory.uniformIntegrable_average : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : ENNReal} {E : Type u_4}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E],
  1 ≤ p →
    ∀ {f : ℕ → α → E},
      MeasureTheory.UniformIntegrable f p μ →
        MeasureTheory.UniformIntegrable (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, f i) p μ
-- Batteries.Recycling.MonadSatisfying.Array
_private.Batteries.Recycling.MonadSatisfying.Array.0.cond.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match false with
    | true => h_1 ()
    | false => h_2 ()) =
    h_2 ()
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forgetToPresheafedSpace_reflectsPullback_of_right : ∀ {X Y Z : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z)
  [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f],
  CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Limits.cospan g f)
    (AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace.comp
      AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace)
-- Mathlib.CategoryTheory.Yoneda
/-- Transport `RepresentableBy` along an isomorphism of the object.  -/
CategoryTheory.Functor.CorepresentableBy.ofIsoObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {F : CategoryTheory.Functor C (Type w)} → {X Y : C} → F.CorepresentableBy X → (Y ≅ X) → F.CorepresentableBy Y
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.mker_inr : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N], MonoidHom.mker (MonoidHom.inr M N) = ⊥
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne
SSet.stdSimplex.objMk₁_apply_eq_one_iff : ∀ {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)), (SSet.stdSimplex.objMk₁ i) j = 1 ↔ i ≤ j.castSucc
-- Mathlib.Data.Sym.Basic
SymOptionSuccEquiv.decode_inl : ∀ {α : Type u_1} {n : ℕ} (s : Sym (Option α) n), SymOptionSuccEquiv.decode (Sum.inl s) = none ::ₛ s
-- Mathlib.Data.PFunctor.Univariate.M
/-- Given an infinite series of approximations `approx`,
`AllAgree approx` states that they are all consistent with each other.
 -/
PFunctor.Approx.AllAgree : {F : PFunctor.{uA, uB}} → ((n : ℕ) → PFunctor.Approx.CofixA F n) → Prop
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.length.eq_1 : ∀ {α : Type u} {β : α → Type v} (l : Std.DHashMap.Internal.AssocList α β),
  l.length = Std.DHashMap.Internal.AssocList.foldl (fun n x x_1 => n + 1) 0 l
-- Init.Data.List.Basic
List.eraseIdx_cons_zero : ∀ {α : Type u_1} {a : α} {as : List α}, (a :: as).eraseIdx 0 = as
-- Mathlib.Algebra.Homology.ComplexShape
/-- If `c : ComplexShape α` is such that `c.Rel` is decidable, it is also the
case of `c.symm.Rel`.  -/
ComplexShape.decidableRelSymm : {α : Type u_2} → (c : ComplexShape α) → [DecidableRel c.Rel] → DecidableRel c.symm.Rel
-- Lean.Elab.Do.InferControlInfo
Lean.Elab.Do.ControlInfo.mk.inj : ∀ {breaks continues returnsEarly : Bool} {numRegularExits : ℕ} {noFallthrough : Bool} {reassigns : Lean.NameSet}
  {breaks_1 continues_1 returnsEarly_1 : Bool} {numRegularExits_1 : ℕ} {noFallthrough_1 : Bool}
  {reassigns_1 : Lean.NameSet},
  { breaks := breaks, continues := continues, returnsEarly := returnsEarly, numRegularExits := numRegularExits,
        noFallthrough := noFallthrough, reassigns := reassigns } =
      { breaks := breaks_1, continues := continues_1, returnsEarly := returnsEarly_1,
        numRegularExits := numRegularExits_1, noFallthrough := noFallthrough_1, reassigns := reassigns_1 } →
    breaks = breaks_1 ∧
      continues = continues_1 ∧
        returnsEarly = returnsEarly_1 ∧
          numRegularExits = numRegularExits_1 ∧ noFallthrough = noFallthrough_1 ∧ reassigns = reassigns_1
-- Mathlib.Combinatorics.Additive.FreimanHom
IsMulFreimanIso.subset : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] {A₁ A₂ : Set α} {B₁ B₂ : Set β}
  {f : α → β} {n : ℕ}, A₁ ⊆ A₂ → IsMulFreimanIso n A₂ B₂ f → Set.BijOn f A₁ B₁ → IsMulFreimanIso n A₁ B₁ f
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
CategoryTheory.LocalizerMorphism.inverts : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {D₂ : Type u₅} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₅, u₅} D₂]
  {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂}
  (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (L₂ : CategoryTheory.Functor C₂ D₂) [L₂.IsLocalization W₂],
  W₁.IsInvertedBy (Φ.functor.comp L₂)
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.instIsEquivalenceOppositeOp : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [F.IsEquivalence], F.op.IsEquivalence
-- Std.Sat.AIG.Relabel
Std.Sat.AIG.relabel : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {β : Type} → [inst_2 : Hashable β] → [inst_3 : DecidableEq β] → (α → β) → Std.Sat.AIG α → Std.Sat.AIG β
-- Mathlib.Topology.Defs.Basic
/-- Delaborator for `closure[_]`.  -/
Topology.delabClosure : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.monomial_zero_one : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R], (MvPowerSeries.monomial 0) 1 = 1
-- Mathlib.CategoryTheory.Sites.LocalSite
/-- See `IsLocalSite.full_constantSheaf` for a version for `w`-locally small sites.  -/
CategoryTheory.GrothendieckTopology.IsLocalSite.instFullSheafConstantSheafOfHasColimitsOfSizeOfHasProducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.IsLocalSite]
  (A : Type u') [inst_2 : CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasColimitsOfSize.{v, v, v', u'} A]
  [CategoryTheory.Limits.HasProducts A] [inst_5 : CategoryTheory.HasWeakSheafify J A],
  (CategoryTheory.constantSheaf J A).Full
-- Mathlib.Data.ENat.Lattice
instCompleteLinearOrderWithBotENat : CompleteLinearOrder (WithBot ℕ∞)
-- Mathlib.Topology.Homeomorph.Lemmas
/-- If two sets are equal, then they are homeomorphic.  -/
Homeomorph.setCongr : {X : Type u_1} → [inst : TopologicalSpace X] → {s t : Set X} → s = t → ↑s ≃ₜ ↑t
-- Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
MeasureTheory.llr_smul_same : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  [μ.HaveLebesgueDecomposition ν],
  μ.AbsolutelyContinuous ν →
    ∀ (c : ENNReal), c ≠ 0 → c ≠ ⊤ → MeasureTheory.llr (c • μ) (c • ν) =ᵐ[μ] MeasureTheory.llr μ ν
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.fibrations_eq_unop : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithFibrations C],
  HomotopicalAlgebra.fibrations C = (HomotopicalAlgebra.cofibrations Cᵒᵖ).unop
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
Real.sigmoid_neg : ∀ (x : ℝ), (-x).sigmoid = 1 - x.sigmoid
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.ext : ∀ {ι : Type u_1} {V : Type u} {inst : CategoryTheory.Category.{v, u} V} {inst_1 : CategoryTheory.Preadditive V}
  {c : ComplexShape ι} {C D : HomologicalComplex V c} {f g : C ⟶ D} {x y : Homotopy f g}, x.hom = y.hom → x = y
-- Mathlib.Data.PFun
/-- Core of a set `s : Set β` with respect to a partial function `f : α →. β`. Set of all `a : α`
such that `f a ∈ s`, if `f a` is defined.  -/
PFun.core : {α : Type u_1} → {β : Type u_2} → (α →. β) → Set β → Set α
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
SemiNormedGrp₁.instHasCokernels : CategoryTheory.Limits.HasCokernels SemiNormedGrp₁
-- Lean.Elab.ComputedFields
Lean.Elab.ComputedFields.Context.compFieldVars : Lean.Elab.ComputedFields.Context → Array Lean.Expr
-- Mathlib.Algebra.Order.Sub.WithTop
WithTop.instOrderedSub : ∀ {α : Type u_1} [inst : Add α] [inst_1 : LE α] [inst_2 : OrderBot α] [inst_3 : Sub α] [OrderedSub α],
  OrderedSub (WithTop α)
-- Mathlib.Algebra.Group.Ideal
/-- In an additive monoid, the semigroup ideal generated by `s` is `Set.univ + s`.  -/
AddSemigroupIdeal.coe_closure' : ∀ {M : Type u_1} [inst : AddMonoid M] {s : Set M}, ↑(AddSemigroupIdeal.closure s) = Set.univ + s
-- Mathlib.Algebra.Group.Defs
zpow_natCast : ∀ {G : Type u_1} [inst : DivInvMonoid G] (a : G) (n : ℕ), a ^ ↑n = a ^ n
-- Mathlib.Topology.MetricSpace.HausdorffDistance
Metric.infEDist_closure_pos_iff_notMem_closure : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {E : Set α}, 0 < Metric.infEDist x (closure E) ↔ x ∉ closure E
-- Mathlib.AlgebraicTopology.SimplicialSet.Nerve
CategoryTheory.nerve.δ₂_two : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (x : CategoryTheory.ComposableArrows C 2),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (CategoryTheory.nerve C) 2)) x =
    CategoryTheory.ComposableArrows.mk₁
      (x.map' 0 1 CategoryTheory.nerve.δ₂_two._proof_1 CategoryTheory.nerve.δ₂_two._proof_3)
-- Init.Data.Array.Lemmas
Array.getElem?_map : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α} {i : ℕ}, (Array.map f xs)[i]? = Option.map f xs[i]?
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_mono_on_of_le_Ioo : ∀ {f g : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ},
  a ≤ b →
    IntervalIntegrable f μ a b →
      IntervalIntegrable g μ a b →
        ∀ [MeasureTheory.NullSingletonClass μ],
          (∀ x ∈ Set.Ioo a b, f x ≤ g x) → ∫ (u : ℝ) in a..b, f u ∂μ ≤ ∫ (u : ℝ) in a..b, g u ∂μ
-- Init.MetaTypes
/-- Unfolds only constants tagged with the `@[reducible]` attribute. Used for speculative
`isDefEq` in proof automation (`simp`, `rw`, type class resolution) where most checks fail
and we must not try too hard.  -/
Lean.Meta.TransparencyMode.reducible : Lean.Meta.TransparencyMode
-- Aesop.RulePattern
Aesop.instInhabitedRulePattern : Inhabited Aesop.RulePattern
-- Lean.Meta.CoeAttr
/-- Lookup the coercion information for a given function  -/
Lean.Meta.getCoeFnInfo? : Lean.Name → Lean.CoreM (Option Lean.Meta.CoeFnInfo)
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.pentagon : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (X₁ X₂ X₃ X₄ : CategoryTheory.GradedObject I C)
  [inst_3 : X₁.HasTensor X₂] [inst_4 : X₂.HasTensor X₃] [inst_5 : X₃.HasTensor X₄]
  [inst_6 : (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃]
  [inst_7 : X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)]
  [inst_8 : (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃).HasTensor X₄]
  [inst_9 : X₂.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)]
  [inst_10 :
    (CategoryTheory.GradedObject.Monoidal.tensorObj (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂) X₃).HasTensor
      X₄]
  [inst_11 :
    (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)).HasTensor
      X₄]
  [inst_12 :
    X₁.HasTensor
      (CategoryTheory.GradedObject.Monoidal.tensorObj (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃) X₄)]
  [inst_13 :
    X₁.HasTensor
      (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄))]
  [inst_14 :
    (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor
      (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)]
  [inst_15 : X₁.HasGoodTensor₁₂Tensor X₂ X₃] [inst_16 : X₁.HasGoodTensorTensor₂₃ X₂ X₃]
  [inst_17 : X₁.HasGoodTensor₁₂Tensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃) X₄]
  [inst_18 : X₁.HasGoodTensorTensor₂₃ (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃) X₄]
  [inst_19 : X₂.HasGoodTensor₁₂Tensor X₃ X₄] [inst_20 : X₂.HasGoodTensorTensor₂₃ X₃ X₄]
  [inst_21 : (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasGoodTensor₁₂Tensor X₃ X₄]
  [inst_22 : (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasGoodTensorTensor₂₃ X₃ X₄]
  [inst_23 : X₁.HasGoodTensor₁₂Tensor X₂ (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)]
  [inst_24 : X₁.HasGoodTensorTensor₂₃ X₂ (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)]
  [X₁.HasTensor₄ObjExt X₂ X₃ X₄],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.Monoidal.tensorHom (CategoryTheory.GradedObject.Monoidal.associator X₁ X₂ X₃).hom
        (CategoryTheory.CategoryStruct.id X₄))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.GradedObject.Monoidal.associator X₁ (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)
            X₄).hom
        (CategoryTheory.GradedObject.Monoidal.tensorHom (CategoryTheory.CategoryStruct.id X₁)
          (CategoryTheory.GradedObject.Monoidal.associator X₂ X₃ X₄).hom)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.Monoidal.associator (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂) X₃ X₄).hom
      (CategoryTheory.GradedObject.Monoidal.associator X₁ X₂ (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)).hom
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.symm_map_add : ∀ {M : Type u_9} {N : Type u_10} [inst : Add M] [inst_1 : Add N] (h : M ≃+ N) (x y : N),
  h.symm (x + y) = h.symm x + h.symm y