mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.δ_zero_eq_const : SSet.stdSimplex.δ 0 = SSet.const (SSet.stdSimplex.obj₀Equiv.symm 1)
-- Init.Data.Nat.ToString
/-- Auxiliary theorem for `Nat.reduceDigitCharEq` simproc.  -/
Nat.digitChar_ne : ∀ {n : ℕ} (c : Char),
  (c != '0' && c != '1' && c != '2' && c != '3' && c != '4' && c != '5' && c != '6' && c != '7' && c != '8' &&
                      c != '9' &&
                    c != 'a' &&
                  c != 'b' &&
                c != 'c' &&
              c != 'd' &&
            c != 'e' &&
          c != 'f' &&
        c != '*') =
      true →
    n.digitChar ≠ c
-- Mathlib.Algebra.Ring.Units
IsUnit.neg : ∀ {α : Type u} [inst : Monoid α] [inst_1 : HasDistribNeg α] {a : α}, IsUnit a → IsUnit (-a)
-- Mathlib.CategoryTheory.Sums.Associator
CategoryTheory.sum.inlCompInlCompAssociator_inv_app_down : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (X : C),
  ((CategoryTheory.sum.inlCompInlCompAssociator C D E).inv.app X).down =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (Sum.inl X)).down
      (CategoryTheory.CategoryStruct.id (Sum.inl X)).down
-- Mathlib.Analysis.Complex.IntegerCompl
UpperHalfPlane.int_div_mem_integerComplement : ∀ (z : UpperHalfPlane) {n : ℤ}, n ≠ 0 → ↑n / ↑z ∈ Complex.integerComplement
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
AlgebraicGeometry.Scheme.Cover.ulift_X : ∀ {X : AlgebraicGeometry.Scheme} {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) (x : ↥X), 𝒰.ulift.X x = 𝒰.X (𝒰.idx x)
-- Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
AlgebraicGeometry.instHasRingHomPropertyLocallyOfFinitePresentationFinitePresentation : AlgebraicGeometry.HasRingHomProperty @AlgebraicGeometry.LocallyOfFinitePresentation
  fun {R S} [CommRing R] [CommRing S] => RingHom.FinitePresentation
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.Const.insertListₘ.match_1.eq_2 : ∀ {α : Type u_2} {β : Type u_1} (motive : List (α × β) → Sort u_3) (hd : α × β) (tl : List (α × β))
  (h_1 : Unit → motive []) (h_2 : (hd : α × β) → (tl : List (α × β)) → motive (hd :: tl)),
  (match hd :: tl with
    | [] => h_1 ()
    | hd :: tl => h_2 hd tl) =
    h_2 hd tl
-- Mathlib.Data.Complex.Basic
Complex.instDecidableEq : DecidableEq ℂ
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
CochainComplex.mappingCone.triangleMapOfHomotopy_comm₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {K₁ L₁ K₂ L₂ : CochainComplex C ℤ} {φ₁ : K₁ ⟶ L₁}
  {φ₂ : K₂ ⟶ L₂} {a : K₁ ⟶ K₂} {b : L₁ ⟶ L₂}
  (H : Homotopy (CategoryTheory.CategoryStruct.comp φ₁ b) (CategoryTheory.CategoryStruct.comp a φ₂)),
  CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.inr φ₁) (CochainComplex.mappingCone.mapOfHomotopy H) =
    CategoryTheory.CategoryStruct.comp b (CochainComplex.mappingCone.inr φ₂)
-- Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
HomotopicalAlgebra.BifibrantObject.mk_surjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  [inst_4 : CategoryTheory.Limits.HasTerminal C] (X : HomotopicalAlgebra.BifibrantObject C),
  ∃ Y,
    ∃ (x : HomotopicalAlgebra.IsCofibrant Y) (x_1 : HomotopicalAlgebra.IsFibrant Y),
      X = HomotopicalAlgebra.BifibrantObject.mk Y
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.mem_modify : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' : α} {f : β → β}, k' ∈ Std.ExtDHashMap.Const.modify m k f ↔ k' ∈ m
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Eta-expanded form of `Differentiable.sub_iff_left` -/
Differentiable.fun_sub_iff_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F},
  Differentiable 𝕜 g → ((Differentiable 𝕜 fun i => f i - g i) ↔ Differentiable 𝕜 f)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_insertManyIfNewUnit_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α Unit} [EquivBEq α] [LawfulHashable α],
  m.WF →
    ∀ {l : List α},
      List.Pairwise (fun a b => (a == b) = false) l →
        (∀ a ∈ m, l.contains a = false) → (m.insertManyIfNewUnit l).size = m.size + l.length
-- Mathlib.RepresentationTheory.FinGroupCharZero
/-- If `G` is finite and its order is nonzero in the field `k`, then every object of
`Rep k G` is injective.
 -/
Rep.instInjective : ∀ {k : Type u} [inst : Field k] {G : Type u} [Finite G] [inst_2 : Group G] [NeZero ↑(Nat.card G)]
  (V : Rep.{w, u, u} k G), CategoryTheory.Injective V
-- Mathlib.Data.Multiset.Fintype
/-- Auxiliary definition for the `CoeSort` instance. This prevents the `CoeOut m α`
instance from inadvertently applying to other sigma types.  -/
Multiset.ToType : {α : Type u_1} → [DecidableEq α] → Multiset α → Type u_1
-- Mathlib.CategoryTheory.Localization.Triangulated
CategoryTheory.Functor.contractible_mem_essImageDistTriang : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : CategoryTheory.Limits.HasZeroObject C] [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_6 : CategoryTheory.Pretriangulated C] [inst_7 : CategoryTheory.HasShift D ℤ] [inst_8 : L.CommShift ℤ]
  [L.EssSurj] [inst_10 : CategoryTheory.Limits.HasZeroObject D] [inst_11 : CategoryTheory.Limits.HasZeroMorphisms D]
  [L.PreservesZeroMorphisms] (X : D), CategoryTheory.Pretriangulated.contractibleTriangle X ∈ L.essImageDistTriang
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.findSomeM?_toList : ∀ {α β : Type w} {γ : Type x} {m : Type x → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α Id β]
  [inst_2 : Std.IteratorLoop α Id m] [LawfulMonad m] [Std.Iterators.Finite α Id] [Std.LawfulIteratorLoop α Id m]
  {it : Std.Iter β} {f : β → m (Option γ)}, List.findSomeM? f it.toList = it.findSomeM? f
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.support.eq_1 : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (p : MvPolynomial σ R), p.support = p.coeff.support
-- Mathlib.NumberTheory.Chebyshev
_private.Mathlib.NumberTheory.Chebyshev.0.Chebyshev.b_antitone : ∀ (x : ℝ), 0 ≤ x → AntitoneOn (Chebyshev.b✝ x) (Set.Ici 1)
-- Init.Sym.Lemmas
Lean.Sym.String.le_eq_false : ∀ (a b : String), decide (a ≤ b) = false → (a ≤ b) = False
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.Equiv.instEquivLike : {N : Type u_1} →
  {E : Type u_2} →
    {G : Type u_3} →
      [inst : Group N] →
        [inst_1 : Group E] →
          [inst_2 : Group G] →
            {S : GroupExtension N E G} →
              {E' : Type u_4} → [inst_3 : Group E'] → {S' : GroupExtension N E' G} → EquivLike (S.Equiv S') E E'
-- Mathlib.CategoryTheory.Bicategory.Functor.Cat.ObjectProperty
CategoryTheory.Pseudofunctor.ObjectProperty.map₂_app_hom : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat}
  (P : F.ObjectProperty) [inst_1 : P.IsClosedUnderMapObj] {X Y : B} {f g : X ⟶ Y} (α : f ⟶ g) (X_1 : P.Obj X),
  ((P.map₂ α).app X_1).hom = (F.map₂ α).toNatTrans.app X_1.obj
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instCommMonoidOfMonoidHomClass.eq_1 : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : Nonempty ι]
  [inst_5 : (i : ι) → CommMonoid (G i)] [inst_6 : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)],
  DirectLimit.instCommMonoidOfMonoidHomClass = { toMonoid := DirectLimit.instMonoid, mul_comm := ⋯ }
-- Mathlib.Data.Finset.Union
Finset.filter_biUnion : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (s : Finset α) (f : α → Finset β) (p : β → Prop)
  [inst_1 : DecidablePred p], Finset.filter p (s.biUnion f) = s.biUnion fun a => Finset.filter p (f a)
-- Init.Data.List.MinMaxOn
List.min_map : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [inst_2 : Min β] [Std.IsLinearPreorder β]
  [Std.LawfulOrderLeftLeaningMin β] {xs : List α} {f : α → β} (h : xs ≠ []),
  (List.map f xs).min ⋯ = f (List.minOn f xs h)
-- Mathlib.Analysis.Analytic.CPolynomialDef
FormalMultilinearSeries.changeOrigin.eq_1 : ∀ {𝕜 : 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]
  (p : FormalMultilinearSeries 𝕜 E F) (x : E) (k : ℕ), p.changeOrigin x k = (p.changeOriginSeries k).sum x
-- Mathlib.Topology.Sober
IsGenericPoint.mem_closed_set_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {S Z : Set α}, IsGenericPoint x S → IsClosed Z → (x ∈ Z ↔ S ⊆ Z)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.max'_one : ∀ {α : Type u_2} [inst : One α] [inst_1 : LinearOrder α], Finset.max' 1 ⋯ = 1
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.opEquiv_inverse : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C],
  (CategoryTheory.ShortComplex.opEquiv C).inverse = CategoryTheory.ShortComplex.unopFunctor C
-- Mathlib.CategoryTheory.Abelian.Subcategory
CategoryTheory.ObjectProperty.instIsNormalEpiCategoryFullSubcategoryOfContainsZeroOfIsClosedUnderKernelsOfIsClosedUnderCokernels : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C)
  [inst_1 : CategoryTheory.Abelian C] [P.ContainsZero] [P.IsClosedUnderKernels] [P.IsClosedUnderCokernels],
  CategoryTheory.IsNormalEpiCategory P.FullSubcategory
-- Mathlib.Topology.EMetricSpace.PairReduction
PairReduction.logSizeBallStruct.smallBall.eq_1 : ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] (struct : PairReduction.logSizeBallStruct T) (c : ENNReal),
  struct.smallBall c = {x ∈ struct.finset | edist struct.point x ≤ (↑struct.radius - 1) * c}
-- Mathlib.NumberTheory.LSeries.ZMod
/-- Functional equation for completed L-functions (even case), valid at all points of differentiability.
 -/
ZMod.completedLFunction_one_sub_even : ∀ {N : ℕ} [inst : NeZero N] {Φ : ZMod N → ℂ},
  Function.Even Φ →
    ∀ (s : ℂ),
      s ≠ 0 ∨ ∑ j, Φ j = 0 →
        s ≠ 1 ∨ Φ 0 = 0 → ZMod.completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * ZMod.completedLFunction (ZMod.dft Φ) s
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_roc_eq_toList_rcc : ∀ {m n : ℤ}, (m<...=n).toList = ((m + 1)...=n).toList
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.le_maxKeyD_of_contains : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α},
      Std.DTreeMap.Internal.Impl.contains k t = true → ∀ {fallback : α}, (compare k (t.maxKeyD fallback)).isLE = true
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.DifferentialObject.mk.sizeOf_spec : ∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] [inst_4 : SizeOf S]
  [inst_5 : SizeOf C] (obj : C) (d : obj ⟶ (CategoryTheory.shiftFunctor C 1).obj obj)
  (d_squared :
    autoParam (CategoryTheory.CategoryStruct.comp d ((CategoryTheory.shiftFunctor C 1).map d) = 0)
      CategoryTheory.DifferentialObject.d_squared._autoParam),
  sizeOf { obj := obj, d := d, d_squared := d_squared } = 1 + sizeOf obj + sizeOf d + sizeOf d_squared
-- Mathlib.Algebra.Group.Hom.Defs
map_comp_sub : ∀ {ι : Type u_1} {G : Type u_7} {H : Type u_8} {F : Type u_9} [inst : FunLike F G H] [inst_1 : AddGroup G]
  [inst_2 : SubtractionMonoid H] [AddMonoidHomClass F G H] (f : F) (g h : ι → G), ⇑f ∘ (g - h) = ⇑f ∘ g - ⇑f ∘ h
-- Init.Data.Iterators.Basic
/-- This theorem is used by a `decreasing_trivial` extension. It powers automatic termination proofs
with `IterM.finitelyManySkips`.
 -/
Std.IterM.TerminationMeasures.Productive.rel_of_skip : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] {it it' : Std.IterM m β},
  it.IsPlausibleStep (Std.IterStep.skip it') → { it := it' }.Rel { it := it }
-- Mathlib.Order.SuccPred.Basic
Order.Ico_succ_right : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] [NoMaxOrder α] (a b : α),
  Set.Ico a (Order.succ b) = Set.Icc a b
-- Mathlib.Algebra.Category.ModuleCat.Kernels
/-- The category of R-modules has kernels, given by the inclusion of the kernel submodule.  -/
ModuleCat.hasKernels_moduleCat : ∀ {R : Type u} [inst : Ring R], CategoryTheory.Limits.HasKernels (ModuleCat R)
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxo.Iterator.instProductivenessRelation : {α : Type u} →
  [inst : Std.PRange.UpwardEnumerable α] →
    [inst_1 : LT α] →
      [inst_2 : DecidableLT α] →
        [Std.PRange.LawfulUpwardEnumerable α] → Std.Iterators.ProductivenessRelation (Std.Rxo.Iterator α) Id
-- Mathlib.LinearAlgebra.Determinant
/-- Conjugating a linear equiv by a linear equiv does not change its determinant.  -/
LinearEquiv.det_conj : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {M' : Type u_3}
  [inst_3 : AddCommGroup M'] [inst_4 : Module R M'] (f : M ≃ₗ[R] M) (e : M ≃ₗ[R] M'),
  LinearEquiv.det (e.symm ≪≫ₗ f ≪≫ₗ e) = LinearEquiv.det f
-- Mathlib.Order.Hom.CompleteLattice
CompleteLatticeHom.setPreimage_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} (g : β → γ) (f : α → β),
  CompleteLatticeHom.setPreimage (g ∘ f) = (CompleteLatticeHom.setPreimage f).comp (CompleteLatticeHom.setPreimage g)
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.oreDiv_smul_oreDiv : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_2}
  [inst_2 : MulAction R X] {r₁ : R} {r₂ : X} {s₁ s₂ : ↥S},
  (r₁ /ₒ s₁) • (r₂ /ₒ s₂) = OreLocalization.oreNum r₁ s₂ • r₂ /ₒ (OreLocalization.oreDenom r₁ s₂ * s₁)
-- Mathlib.Order.Hom.Basic
/-- The trivial embedding from an empty preorder to another preorder  -/
OrderEmbedding.ofIsEmpty : {α : Type u_2} → {β : Type u_3} → [inst : Preorder α] → [inst_1 : Preorder β] → [IsEmpty α] → α ↪o β
-- Lean.Elab.ConfigEval.Types
/-- A view of a `Lean.Parser.Term.configItem`.
 -/
Lean.Elab.ConfigEval.ConfigItem : Type
-- Init.Data.Slice.Array.Lemmas
Array.array_mkSlice_roc : ∀ {α : Type u_1} {xs : Array α} {lo hi : ℕ}, (Std.Roc.Sliceable.mkSlice xs lo<...=hi).array = xs
-- Mathlib.LinearAlgebra.AffineSpace.Combination
Finset.affineCombinationSingleWeights.eq_1 : ∀ (k : Type u_1) [inst : Ring k] {ι : Type u_4} [inst_1 : DecidableEq ι] (i : ι),
  Finset.affineCombinationSingleWeights k i = Pi.single i 1
-- Mathlib.Algebra.GradedMonoid
/-- `GradedMonoid.mk 0` is a `MonoidHom`, using the `GradedMonoid.GradeZero.monoid` structure.
 -/
GradedMonoid.mkZeroMonoidHom : {ι : Type u_1} → (A : ι → Type u_2) → [inst : AddMonoid ι] → [inst_1 : GradedMonoid.GMonoid A] → A 0 →* GradedMonoid A
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
Submodule.symmetric_isOrtho : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E],
  Std.Symm Submodule.IsOrtho
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapLeftIso_inverse_obj_left : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T)
  {L₁ L₂ : CategoryTheory.Functor A T} (i : L₁ ≅ L₂) (X : CategoryTheory.Comma L₂ R),
  ((CategoryTheory.Comma.mapLeftIso R i).inverse.obj X).left = X.left
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.tmulEquivDep_symm_apply : ∀ {ι : Type u_1} {ι₂ : Type u_2} (R : Type u_4) [inst : CommSemiring R] (N : ι ⊕ ι₂ → Type u_12)
  [inst_1 : (i : ι ⊕ ι₂) → AddCommMonoid (N i)] [inst_2 : (i : ι ⊕ ι₂) → Module R (N i)] (f : (i : ι ⊕ ι₂) → N i),
  (PiTensorProduct.tmulEquivDep R N).symm (⨂ₜ[R] (i : ι ⊕ ι₂), f i) =
    ((PiTensorProduct.tprod R) fun i₁ => f (Sum.inl i₁)) ⊗ₜ[R] (PiTensorProduct.tprod R) fun i₂ => f (Sum.inr i₂)
-- Mathlib.Topology.Algebra.Module.ModuleTopology
ModuleTopology.eq_coinduced_of_surjectiveₛₗ : ∀ {R : Type u_1} {S : Type u_2} [τR : TopologicalSpace R] [τS : TopologicalSpace S] [inst : Ring R] [inst_1 : Ring S]
  {A : Type u_3} [inst_2 : AddCommGroup A] [inst_3 : Module R A] [inst_4 : TopologicalSpace A] [IsModuleTopology R A]
  {B' : Type u_5} [inst_6 : AddCommGroup B'] [inst_7 : Module S B'] {σ : R →+* S},
  IsOpenQuotientMap ⇑σ →
    ∀ (φ : A →ₛₗ[σ] B'), Function.Surjective ⇑φ → moduleTopology S B' = TopologicalSpace.coinduced (⇑φ) inferInstance
-- Init.Data.Dyadic.Basic
instDecidableEqDyadic : DecidableEq Dyadic
-- Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap
CompletelyPositiveMap.map_cstarMatrix_nonneg : ∀ {A₁ : Type u_1} {A₂ : Type u_2} [inst : NonUnitalCStarAlgebra A₁] [inst_1 : NonUnitalCStarAlgebra A₂]
  [inst_2 : PartialOrder A₁] [inst_3 : PartialOrder A₂] [inst_4 : StarOrderedRing A₁] [inst_5 : StarOrderedRing A₂]
  {n : Type u_3} [inst_6 : Fintype n] (φ : CompletelyPositiveMap A₁ A₂) (M : CStarMatrix n n A₁), 0 ≤ M → 0 ≤ M.map ⇑φ
-- Mathlib.Tactic.Abel
/-- Function elaborating `AbelNF.Config`.  -/
Mathlib.Tactic.Abel.elabAbelNFConfig : Lean.Syntax →
  optParam Mathlib.Tactic.Abel.AbelNF.Config { } →
    optParam Bool true → Lean.Elab.Tactic.TacticM Mathlib.Tactic.Abel.AbelNF.Config
-- Mathlib.CategoryTheory.Monad.Equalizer
/-- The bottom map in the equalizer diagram we will construct.  -/
CategoryTheory.Comonad.CofreeEqualizer.bottomMap : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T : CategoryTheory.Comonad C} → (X : T.Coalgebra) → T.cofree.obj X.A ⟶ T.cofree.obj (T.obj X.A)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Real.isPiSystem_Iio_rat : IsPiSystem (⋃ a, {Set.Iio ↑a})
-- Mathlib.RingTheory.Ideal.Maximal
/-- **Krull's theorem**: if `I` is an ideal that is not the whole ring, then it is included in some
maximal ideal.  -/
Ideal.exists_le_maximal : ∀ {α : Type u} [inst : Semiring α] (I : Ideal α), I ≠ ⊤ → ∃ M, M.IsMaximal ∧ I ≤ M
-- Mathlib.AlgebraicGeometry.QuasiAffine
AlgebraicGeometry.Scheme.openCoverBasicOpenTop_f : ∀ (X : AlgebraicGeometry.Scheme) [inst : X.IsQuasiAffine] (i : { r // AlgebraicGeometry.IsAffineOpen (X.basicOpen r) }),
  X.openCoverBasicOpenTop.f i = (X.basicOpen ↑i).ι
-- Mathlib.Algebra.FreeMonoid.FreeSemigroup
FreeSemigroup.eq_one_or_toFreeMonoid : ∀ {α : Type u_1} (x : FreeMonoid α), x = 1 ∨ ∃ y, FreeSemigroup.toFreeMonoid y = x
-- Mathlib.Order.RelIso.Basic
/-- A relation isomorphism is an equivalence that is also a relation embedding.  -/
«term_≃r_» : Lean.TrailingParserDescr
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution'.a : {K : Type u_1} →
  [inst : Field K] →
    {ζ : K} → {hζ : IsPrimitiveRoot ζ 3} → FermatLastTheoremForThreeGen.Solution'✝ hζ → NumberField.RingOfIntegers K
-- Mathlib.RingTheory.GradedAlgebra.Basic
GradedRing.mk : {ι : Type u_1} →
  {A : Type u_3} →
    {σ : Type u_4} →
      [inst : DecidableEq ι] →
        [inst_1 : AddMonoid ι] →
          [inst_2 : Semiring A] →
            [inst_3 : SetLike σ A] →
              [inst_4 : AddSubmonoidClass σ A] →
                {𝒜 : ι → σ} →
                  [toGradedMonoid : SetLike.GradedMonoid 𝒜] →
                    [toDecomposition : DirectSum.Decomposition 𝒜] → GradedRing 𝒜
-- Init.Data.Int.Order
Int.lt_iff_le_and_not_ge : ∀ {a b : ℤ}, a < b ↔ a ≤ b ∧ ¬b ≤ a
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.eventually_mul_left_iff : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul G] (μ : MeasureTheory.Measure G)
  [μ.IsMulLeftInvariant] (t : G) {p : G → Prop}, (∀ᵐ (x : G) ∂μ, p (t * x)) ↔ ∀ᵐ (x : G) ∂μ, p x
-- Mathlib.CategoryTheory.Discrete.SumsProducts
_private.Mathlib.CategoryTheory.Discrete.SumsProducts.0.CategoryTheory.Discrete.sumEquiv.match_1.eq_2 : ∀ {J : Type u_1} {K : Type u_2} (motive : J ⊕ K → Sort u_3) (k : K) (h_1 : (j : J) → motive (Sum.inl j))
  (h_2 : (k : K) → motive (Sum.inr k)),
  (match Sum.inr k with
    | Sum.inl j => h_1 j
    | Sum.inr k => h_2 k) =
    h_2 k
-- Mathlib.Algebra.Lie.IdealOperations
LieIdeal.map_comap_bracket_eq : ∀ {R : Type u} {L : Type v} {L' : Type w₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing L'] [inst_4 : LieAlgebra R L'] {f : L →ₗ⁅R⁆ L'} {J₁ J₂ : LieIdeal R L'},
  f.IsIdealMorphism → LieIdeal.map f ⁅LieIdeal.comap f J₁, LieIdeal.comap f J₂⁆ = ⁅f.idealRange ⊓ J₁, f.idealRange ⊓ J₂⁆
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.Karoubi.coe_p : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : C),
  { X := X, p := CategoryTheory.CategoryStruct.id X, idem := ⋯ }.p = CategoryTheory.CategoryStruct.id X
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.Indep.closure_inter_eq_self_of_subset : ∀ {α : Type u_2} {M : Matroid α} {I J : Set α}, M.Indep I → J ⊆ I → M.closure J ∩ I = J
-- Mathlib.Topology.MetricSpace.HolderNorm
MemHolder.comp : ∀ {X : Type u_1} {Y : Type u_2} [inst : MetricSpace X] [inst_1 : EMetricSpace Y] {r s : NNReal} {Z : Type u_3}
  [inst_2 : MetricSpace Z] {f : Z → X} {g : X → Y}, MemHolder r f → MemHolder s g → MemHolder (s * r) (g ∘ f)
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
/-- Construct an element of `OverArrows η s` with `F = yoneda.obj Y` from a suitable morphism
`f : X ⟶ Y`.  -/
CategoryTheory.OverPresheafAux.OverArrows.yonedaArrow : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : CategoryTheory.Functor Cᵒᵖ (Type v)} →
      {Y : C} →
        {η : CategoryTheory.yoneda.obj Y ⟶ A} →
          {X : C} →
            {s : CategoryTheory.yoneda.obj X ⟶ A} →
              (f : X ⟶ Y) →
                CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map f) η = s →
                  CategoryTheory.OverPresheafAux.OverArrows η s
-- Mathlib.Data.ENNReal.Inv
ENNReal.sSup_div : ∀ (s : Set ENNReal) (a : ENNReal), sSup s / a = ⨆ b ∈ s, b / a
-- Std.Http.Data.URI.Parser
_private.Std.Http.Data.URI.Parser.0.Std.Http.URI.Parser.parseFragment : Std.Http.URI.Config → Std.Internal.Parsec.ByteArray.Parser Std.Http.URI.EncodedFragment
-- Mathlib.Analysis.Normed.Group.InfiniteSum
/-- The direct comparison test for series:  if the norm of `f` is bounded by a real function `g`
which is summable, then `f` is summable.  -/
Summable.of_norm_bounded : ∀ {ι : Type u_1} {E : Type u_3} [inst : SeminormedAddCommGroup E] [CompleteSpace E] {f : ι → E} {g : ι → ℝ},
  Summable g → (∀ (i : ι), ‖f i‖ ≤ g i) → Summable f
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
euler_sineTerm_tprod : ∀ {x : ℂ}, x ∈ Complex.integerComplement → ∏' (i : ℕ), (1 + sineTerm x i) = Complex.sin (↑Real.pi * x) / (↑Real.pi * x)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Pos.skip?_prop_eq_none_iff : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String} {pos : s.Pos},
  pos.skip? P = none ↔ ∀ (h : pos ≠ s.endPos), ¬P (pos.get h)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.beq_iff_equiv : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.DTreeMap α (fun x => β) cmp} [inst : BEq β]
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [LawfulBEq β], Std.DTreeMap.Const.beq m₁ m₂ = true ↔ m₁.Equiv m₂