mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- If G and H are naturally isomorphic functors, establish an equivalence of hom-sets.  -/
CategoryTheory.Adjunction.equivHomsetRightOfNatIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F F' : CategoryTheory.Functor C D} → (F ≅ F') → {X : C} → {Y : D} → (Y ⟶ F.obj X) ≃ (Y ⟶ F'.obj X)
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.coe_smul : ∀ {α : Type u_1} [inst : TopologicalSpace α] {R : Type u_3} {M : Type u_5} [inst_1 : TopologicalSpace M]
  [inst_2 : SMul R M] [inst_3 : ContinuousConstSMul R M] (c : R) (f : C(α, M)), ⇑(c • f) = c • ⇑f
-- Mathlib.RingTheory.Polynomial.GaussNorm
Polynomial.gaussNorm_C : ∀ {R : Type u_1} {F : Type u_2} [inst : Semiring R] [inst_1 : FunLike F R ℝ] (v : F) (c : ℝ) [ZeroHomClass F R ℝ]
  (r : R), Polynomial.gaussNorm v c (Polynomial.C r) = v r
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.instEpiPOpcycles : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasRightHomology], CategoryTheory.Epi S.pOpcycles
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.Stream.foldr.match_1.eq_2 : ∀ {α : Type u_1} {σ : Sort u_3} (motive : RBTree.RBNode.Stream α → σ → Sort u_2) (v : α) (r : RBTree.RBNode α)
  (tail : RBTree.RBNode.Stream α) (b : σ) (h_1 : (b : σ) → motive RBTree.RBNode.Stream.nil b)
  (h_2 :
    (v : α) →
      (r : RBTree.RBNode α) →
        (tail : RBTree.RBNode.Stream α) → (b : σ) → motive (RBTree.RBNode.Stream.cons v r tail) b),
  (match RBTree.RBNode.Stream.cons v r tail, b with
    | RBTree.RBNode.Stream.nil, b => h_1 b
    | RBTree.RBNode.Stream.cons v r tail, b => h_2 v r tail b) =
    h_2 v r tail b
-- Std.Time.Zoned.Database.TzIf
/-- The transition time of the leap second event.
 -/
Std.Time.TimeZone.TZif.LeapSecond.transitionTime : Std.Time.TimeZone.TZif.LeapSecond → ℤ
-- Mathlib.Order.Filter.Pointwise
Filter.eventually_zero : ∀ {α : Type u_2} [inst : Zero α] {p : α → Prop}, (∀ᶠ (x : α) in 0, p x) ↔ p 0
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.StructuredArrow.ofCommaSndEquivalence_unitIso : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T)
  (G : CategoryTheory.Functor D T) (c : C),
  (CategoryTheory.StructuredArrow.ofCommaSndEquivalence F G c).unitIso =
    CategoryTheory.NatIso.ofComponents
      (fun x =>
        CategoryTheory.Iso.refl
          ((CategoryTheory.Functor.id (CategoryTheory.StructuredArrow c (CategoryTheory.Comma.fst F G))).obj x))
      ⋯
-- Init.Data.Range.Polymorphic.Internal.SignedBitVec
_private.Init.Data.Range.Polymorphic.Internal.SignedBitVec.0.BitVec.Signed.intMaxSealed : (n : ℕ) → BitVec n
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.ideal_mul : ∀ {X : AlgebraicGeometry.Scheme} (I J : X.IdealSheafData), (I * J).ideal = I.ideal * J.ideal
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.AffineScheme.forgetToScheme_obj : ∀ (self : AlgebraicGeometry.Scheme.Spec.essImage.FullSubcategory),
  AlgebraicGeometry.AffineScheme.forgetToScheme.obj self = self.obj
-- Std.Time.Internal.Bounded
_private.Std.Time.Internal.Bounded.0.Int.tdiv.match_1.eq_2 : ∀ (motive : ℤ → ℤ → Sort u_1) (m n : ℕ) (h_1 : (m n : ℕ) → motive (Int.ofNat m) (Int.ofNat n))
  (h_2 : (m n : ℕ) → motive (Int.ofNat m) (Int.negSucc n)) (h_3 : (m n : ℕ) → motive (Int.negSucc m) (Int.ofNat n))
  (h_4 : (m n : ℕ) → motive (Int.negSucc m) (Int.negSucc n)),
  (match Int.ofNat m, Int.negSucc n with
    | Int.ofNat m, Int.ofNat n => h_1 m n
    | Int.ofNat m, Int.negSucc n => h_2 m n
    | Int.negSucc m, Int.ofNat n => h_3 m n
    | Int.negSucc m, Int.negSucc n => h_4 m n) =
    h_2 m n
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- If a set of functions is equicontinuous at some `x₀`, the same is true for its closure in *any*
topology for which evaluation at any point is continuous. Since this will be applied to
`DFunLike` types, we state it for any topological space with a map to `X → α` satisfying the right
continuity conditions. See also `Set.EquicontinuousAt.closure` for a more familiar statement.  -/
EquicontinuousAt.closure' : ∀ {X : Type u_3} {Y : Type u_5} {α : Type u_6} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] [uα : UniformSpace α]
  {A : Set Y} {u : Y → X → α} {x₀ : X},
  EquicontinuousAt (u ∘ Subtype.val) x₀ → Continuous u → EquicontinuousAt (u ∘ Subtype.val) x₀
-- Mathlib.SetTheory.ZFC.Basic
/-- The union operator, the collection of elements of elements of a ZFC set. Uses `⋃₀` notation,
scoped under the `ZFSet` namespace.
 -/
ZFSet.«term⋃₀_» : Lean.ParserDescr
-- Mathlib.Tactic.ClickSuggestions.Util
Mathlib.Tactic.ClickSuggestions.Premise.fvar.inj : ∀ {fvarId fvarId_1 : Lean.FVarId},
  Mathlib.Tactic.ClickSuggestions.Premise.fvar fvarId = Mathlib.Tactic.ClickSuggestions.Premise.fvar fvarId_1 →
    fvarId = fvarId_1
-- Mathlib.Algebra.SkewMonoidAlgebra.Single
SkewMonoidAlgebra.induction : ∀ {M : Type u_4} {α : Type u_5} [inst : AddCommMonoid M] {p : SkewMonoidAlgebra M α → Prop} (f : SkewMonoidAlgebra M α),
  p 0 →
    (∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α),
        a ∉ f.support → b ≠ 0 → p f → p (SkewMonoidAlgebra.single a b + f)) →
      p f
-- Mathlib.Topology.Order.DenselyOrdered
frontier_Iio' : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α},
  (Set.Iio a).Nonempty → frontier (Set.Iio a) = {a}
-- Mathlib.Tactic.Simps.Basic
/-- Configuration items for `@[simps]` attribute.  -/
Lean.Parser.Attr.simpsConfigItem : Lean.ParserDescr
-- Mathlib.Data.Finmap
Finmap.liftOn₂.congr_simp : ∀ {α : Type u} {β : α → Type v} {γ : Type u_1} (s₁ s₁_1 : Finmap β),
  s₁ = s₁_1 →
    ∀ (s₂ s₂_1 : Finmap β),
      s₂ = s₂_1 →
        ∀ (f f_1 : AList β → AList β → γ) (e_f : f = f_1)
          (H : ∀ (a₁ b₁ a₂ b₂ : AList β), a₁.entries.Perm a₂.entries → b₁.entries.Perm b₂.entries → f a₁ b₁ = f a₂ b₂),
          s₁.liftOn₂ s₂ f H = s₁_1.liftOn₂ s₂_1 f_1 ⋯
-- Mathlib.Algebra.MvPolynomial.Nilpotent
MvPolynomial.isUnit_iff : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R] {P : MvPolynomial σ R},
  IsUnit P ↔ IsUnit (MvPolynomial.coeff 0 P) ∧ ∀ (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (MvPolynomial.coeff i P)
-- Mathlib.Analysis.Complex.Order
Complex.nonpos_iff : ∀ {z : ℂ}, z ≤ 0 ↔ z.re ≤ 0 ∧ z.im = 0
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubring.mk : {R : Type u} →
  [inst : NonUnitalNonAssocRing R] →
    (toNonUnitalSubsemiring : NonUnitalSubsemiring R) →
      (∀ {x : R}, x ∈ toNonUnitalSubsemiring.carrier → -x ∈ toNonUnitalSubsemiring.carrier) → NonUnitalSubring R
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
/-- Copy of a `MeasurableSpace` with a new `MeasurableSet` equal to the old one. Useful to fix
definitional equalities.  -/
MeasurableSpace.copy : {α : Type u_1} →
  (m : MeasurableSpace α) → (p : Set α → Prop) → (∀ (s : Set α), p s ↔ MeasurableSet s) → MeasurableSpace α
-- Mathlib.Tactic.FunProp.Types
/-- Maximum number of steps `fun_prop` can take.  -/
Mathlib.Meta.FunProp.Config.maxSteps : Mathlib.Meta.FunProp.Config → ℕ
-- Mathlib.Algebra.Algebra.RestrictScalars
instRingRestrictScalars : (R : Type u_1) → (S : Type u_2) → (A : Type u_4) → [I : Ring A] → Ring (RestrictScalars R S A)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.inv_int_eqC : ∀ {α : Type u_1} {c : ℕ} [inst : Lean.Grind.Field α] [Lean.Grind.IsCharP α c] (b : ℤ),
  (b % ↑c != 0) = true → Lean.Grind.CommRing.denoteInt b * (Lean.Grind.CommRing.denoteInt b)⁻¹ = 1
-- Init.Data.Array.Lemmas
Array.eq_or_ne_mem_of_mem : ∀ {α : Type u_1} {a b : α} {xs : Array α}, a ∈ xs.push b → a = b ∨ a ≠ b ∧ a ∈ xs
-- Mathlib.Order.Heyting.Basic
top_sdiff' : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] (a : α), ⊤ \ a = ￢a
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Complex.measurable_im : Measurable Complex.im
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.IndepSet.eq_1 : ∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} (s t : Set Ω)
  (κ : ProbabilityTheory.Kernel α Ω) (μ : MeasureTheory.Measure α),
  ProbabilityTheory.Kernel.IndepSet s t κ μ =
    ProbabilityTheory.Kernel.Indep (MeasurableSpace.generateFrom {s}) (MeasurableSpace.generateFrom {t}) κ μ
-- Init.Data.Range.Polymorphic.IntLemmas
Std.PRange.Int.succMany?_eq : ∀ {n : ℕ} {m : ℤ}, Std.PRange.succMany? n m = some (m + ↑n)
-- Lean.Elab.PreDefinition.WF.Eqns
Lean.Elab.WF.registerEqnsInfo : Array Lean.Elab.PreDefinition → Lean.Name → Lean.Elab.FixedParamPerms → Lean.Meta.ArgsPacker → Lean.MetaM Unit
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.not_isLongestRevMatchAt_self : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] {s : String.Slice} {endPos : s.Pos},
  ¬String.Slice.Pattern.Model.IsLongestRevMatchAt pat endPos endPos
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.recoverEol : Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Mathlib.RingTheory.Multiplicity
emultiplicity_le_emultiplicity_of_dvd_left : ∀ {α : Type u_1} [inst : CommMonoid α] {a b c : α}, a ∣ b → emultiplicity b c ≤ emultiplicity a c
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.forIn_eq_forIn_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {δ : Type w}
  {m : Type w → Type w'} [inst : Std.TransCmp cmp] [inst_1 : Monad m] [inst_2 : LawfulMonad m]
  {f : α → δ → m (ForInStep δ)} {init : δ}, (forIn t init fun a d => f a.fst d) = forIn t.keys init f
-- Mathlib.RingTheory.MvPowerSeries.Basic
/-- The coercion from multivariate polynomials to multivariate power series
as a ring homomorphism.
 -/
MvPolynomial.coeToMvPowerSeries.ringHom : {σ : Type u_1} → {R : Type u_2} → [inst : CommSemiring R] → MvPolynomial σ R →+* MvPowerSeries σ R
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.isIso_eTruncLTLTIsoLT : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C] (a b : EInt),
  b ≤ a → CategoryTheory.IsIso (t.eTruncLTLTToLT a b)
-- Std.Data.DHashMap.Internal.RawLemmas
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.tacticEmpty : Lean.ParserDescr
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.isEmpty_toList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α], (↑m).WF → (Std.DHashMap.Raw.Const.toList ↑m).isEmpty = (↑m).isEmpty
-- Mathlib.Algebra.Group.Action.Equidecomp
/-- Note that `Equidecomp X G` is not `FunLike`.  -/
Equidecomp.instCoeFunForall : {X : Type u_1} → {G : Type u_2} → [inst : SMul G X] → CoeFun (Equidecomp X G) fun x => X → X
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
/-- The logarithmic counting function of a singleton indicator is asymptotically equal to
`log · - log ‖e‖`.
 -/
Function.locallyFinsuppWithin.logCounting_single_eq_log_sub_const : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : DecidableEq E] [inst_2 : ProperSpace E] {e : E} {r : ℝ}
  {n : ℤ},
  ‖e‖ ≤ r →
    Function.locallyFinsuppWithin.logCounting (Function.locallyFinsuppWithin.single e n) r =
      ↑n * (Real.log r - Real.log ‖e‖)
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.newton_seq_aux.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((k : ℕ) → motive k.succ) → motive x
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardStringSearcher.isLongestMatchAtChain_startPos_endPos_iff : ∀ {pat : String} {s : String.Slice},
  String.Slice.Pattern.Model.IsLongestMatchAtChain pat s.startPos s.endPos ↔
    ∃ n, s.copy = String.join (List.replicate n pat)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.sqrt.congr_simp : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalRing A] [inst_2 : TopologicalSpace A] [inst_3 : StarRing A]
  [inst_4 : Module ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : StarOrderedRing A]
  [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A] (a a_1 : A),
  a = a_1 → CFC.sqrt a = CFC.sqrt a_1
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.updateProj! : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.LetValue pu → Lean.FVarId → Lean.Compiler.LCNF.LetValue pu
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.insertMany_list_eq_empty_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {l : List ((a : α) × β a)}, t.insertMany l = ∅ ↔ t = ∅ ∧ l = []
-- Mathlib.GroupTheory.GroupAction.Basic
MulAction.instDecidablePredMemSetFixedByOfDecidableEq : {M : Type u} →
  [inst : Monoid M] →
    {β : Type u_1} →
      [inst_1 : MulAction M β] → (m : M) → [DecidableEq β] → DecidablePred fun b => b ∈ MulAction.fixedBy β m
-- Lean.Meta.Tactic.Grind.MarkNestedSubsingletons
Lean.Meta.Grind.isMarkedSubsingletonConst : Lean.Expr → Bool
-- Mathlib.Topology.Order.OrderClosed
/-- **Alias** of the reverse direction of `bddBelow_closure`. -/
BddBelow.closure : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Preorder α] [ClosedIciTopology α] {s : Set α},
  BddBelow s → BddBelow (closure s)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
SSet.Subcomplex.Pairing.mk : {X : SSet} → {A : X.Subcomplex} → (I II : Set A.N) → I ∩ II = ∅ → I ∪ II = Set.univ → ↑II ≃ ↑I → A.Pairing
-- Lean.Hygiene
Lean.pp.sanitizeNames : Lean.Option Bool
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.Context.mk.injEq : ∀ (maxResultSize maxHeartbeats maxResultSize_1 maxHeartbeats_1 : ℕ),
  ({ maxResultSize := maxResultSize, maxHeartbeats := maxHeartbeats } =
      { maxResultSize := maxResultSize_1, maxHeartbeats := maxHeartbeats_1 }) =
    (maxResultSize = maxResultSize_1 ∧ maxHeartbeats = maxHeartbeats_1)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} [inst_2 : SizeOf C] (Q H : C) (p : S.X₂ ⟶ Q) (ι : H ⟶ Q)
  (wp : CategoryTheory.CategoryStruct.comp S.f p = 0)
  (hp : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ p wp))
  (wι : CategoryTheory.CategoryStruct.comp ι (hp.desc (CategoryTheory.Limits.CokernelCofork.ofπ S.g ⋯)) = 0)
  (hι : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι ι wι)),
  sizeOf { Q := Q, H := H, p := p, ι := ι, wp := wp, hp := hp, wι := wι, hι := hι } =
    1 + sizeOf Q + sizeOf H + sizeOf p + sizeOf ι + sizeOf wp + sizeOf hp + sizeOf wι + sizeOf hι
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to1.trNormal.eq_1 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} {n : ℕ} (dec : List.Vector Bool n → Γ) (a : Turing.Dir)
  (q : Turing.TM1.Stmt Γ Λ σ),
  Turing.TM1to1.trNormal dec (Turing.TM1.Stmt.move a q) = Turing.TM1to1.move n a (Turing.TM1to1.trNormal dec q)
-- Mathlib.Tactic.FunProp.Decl
/-- function transformation name  -/
Mathlib.Meta.FunProp.FunPropDecl.funPropName : Mathlib.Meta.FunProp.FunPropDecl → Lean.Name
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.card_roots' : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] (p : Polynomial R), p.roots.card ≤ p.natDegree
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.truncLEIsoTruncLT_hom_ι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b),
  CategoryTheory.CategoryStruct.comp (t.truncLEIsoTruncLT a b h).hom (t.truncLTι b) = t.truncLEι a
-- Mathlib.Topology.Algebra.UniformConvergence
instNegUniformFun : {α : Type u_1} → {β : Type u_2} → [Neg β] → Neg (UniformFun α β)
-- Mathlib.Algebra.Order.Group.Indicator
Function.support_iInf : ∀ {ι : Sort u_1} {α : Type u_2} {M : Type u_3} [inst : Zero M] [inst_1 : ConditionallyCompleteLattice M] [Nonempty ι]
  (f : ι → α → M), (Function.support fun x => ⨅ i, f i x) ⊆ ⋃ i, Function.support (f i)
-- Batteries.Data.List.Basic
List.zipWithLeft'TR.go.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β → γ) (a : List β) (a_1 : Array γ),
  List.zipWithLeft'TR.go f [] a a_1 = (a_1.toList, a)
-- Mathlib.Topology.Algebra.Group.Basic
AddSubgroup.topologicalClosure_mono : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G]
  {s t : AddSubgroup G}, s ≤ t → s.topologicalClosure ≤ t.topologicalClosure
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.add_apply : ∀ {ι : Type u_1} {M : ι → Type u_5} [inst : (i : ι) → Add (M i)] (f g : (i : ι) → M i) (i : ι), (f + g) i = f i + g i
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.step_filterMapWithPostcondition.match_1.eq_2 : ∀ {β β' : Type u_1} {n : Type u_1 → Type u_2} {f : β → Std.Iterators.PostconditionT n (Option β')} (out : β)
  (motive : Subtype (f out).Property → Sort u_3) (out' : β') (h' : (f out).Property (some out'))
  (h_1 : (h' : (f out).Property none) → motive ⟨none, h'⟩)
  (h_2 : (out' : β') → (h' : (f out).Property (some out')) → motive ⟨some out', h'⟩),
  (match ⟨some out', h'⟩ with
    | ⟨none, h'⟩ => h_1 h'
    | ⟨some out', h'⟩ => h_2 out' h') =
    h_2 out' h'
-- Mathlib.Topology.UnitInterval
/-- Unit interval central symmetry.  -/
unitInterval.termσ : Lean.ParserDescr
-- Mathlib.Analysis.Convex.SpecificFunctions.Deriv
strictConcaveOn_sin_Icc : StrictConcaveOn ℝ (Set.Icc 0 Real.pi) Real.sin
-- Mathlib.Algebra.Algebra.Operations
Submodule.pow_eq_bot : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [IsReduced A] {M : Submodule R A} {n : ℕ}, n ≠ 0 → (M ^ n = ⊥ ↔ M = ⊥)
-- Mathlib.Data.Multiset.Find
Multiset.find?_eq_none_iff : ∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {s : Multiset α} (hp : {x | x ∈ s ∧ p x}.Subsingleton),
  Multiset.find? p s hp = none ↔ ∀ a ∈ s, ¬p a
-- Lean.Data.Json.Basic
Lean.JsonNumber.ltProp : LT Lean.JsonNumber
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxc.Iterator.Monadic.isPlausibleSuccessorOf_iff : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LE α] [inst_2 : DecidableLE α]
  {it' it : Std.IterM Id α},
  it'.IsPlausibleSuccessorOf it ↔
    ∃ a,
      it.internalState.next = some a ∧
        a ≤ it.internalState.upperBound ∧
          Std.PRange.succ? a = it'.internalState.next ∧ it'.internalState.upperBound = it.internalState.upperBound
-- Mathlib.Algebra.Category.Ring.Under.Basic
CommRingCat.toAlgHom_id : ∀ {R : CommRingCat} (A : CategoryTheory.Under R),
  CommRingCat.toAlgHom (CategoryTheory.CategoryStruct.id A) = AlgHom.id ↑R ↑A.right
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.instSMulNat : {R : Type u_1} →
  [inst : CommRing R] →
    {S : Submonoid R} → {P : Type u_2} → [inst_1 : CommRing P] → [inst_2 : Algebra R P] → SMul ℕ (FractionalIdeal S P)
-- Mathlib.Data.NNRat.Defs
NNRat.coe_zero : ↑0 = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.kernel.condition : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι f) f = 0
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- An additive semigroup with a partial order and satisfying `AddLeftCancelSemigroup`
(i.e. `c + a < c + b → a < b`) is a `AddLeftCancelSemigroup`.  -/
Contravariant.toAddLeftCancelSemigroup : {α : Type u_1} → [inst : AddSemigroup α] → [inst_1 : PartialOrder α] → [AddLeftReflectLE α] → AddLeftCancelSemigroup α
-- Mathlib.RingTheory.LocalProperties.Projective
Module.free_of_isLocalizedModule : ∀ {R : Type u_1} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {Rₛ : Type u_4}
  {Mₛ : Type u_5} [inst_3 : AddCommGroup Mₛ] [inst_4 : Module R Mₛ] [inst_5 : CommRing Rₛ] [inst_6 : Algebra R Rₛ]
  [inst_7 : Module Rₛ Mₛ] [IsScalarTower R Rₛ Mₛ] (S : Submonoid R) (f : M →ₗ[R] Mₛ) [IsLocalization S Rₛ]
  [IsLocalizedModule S f] [Module.Free R M], Module.Free Rₛ Mₛ
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
SubAddAction.notMem_val_image : ∀ (G : Type u_1) [inst : AddGroup G] {α : Type u_2} [inst_1 : AddAction G α] {a : α}
  (t : Set ↥(SubAddAction.ofStabilizer G a)), a ∉ Subtype.val '' t
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.equivPair_eq_of_fstIdx_ne : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] [inst_1 : DecidableEq ι]
  [inst_2 : (i : ι) → DecidableEq (M i)] {i : ι} {w : Monoid.CoprodI.Word M} (h : w.fstIdx ≠ some i),
  (Monoid.CoprodI.Word.equivPair i) w = { head := 1, tail := w, fstIdx_ne := h }
-- Mathlib.RingTheory.Length
Module.length_pos_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  0 < Module.length R M ↔ Nontrivial M
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.mk.inj : ∀ {R : Type u_2} {M : Type u_3} {inst : Semiring R} {inst_1 : AddCommMonoid M} {inst_2 : TopologicalSpace M}
  {inst_3 : Module R M} {toSubmodule : Submodule R M} {isClosed' : IsClosed toSubmodule.carrier}
  {toSubmodule_1 : Submodule R M} {isClosed'_1 : IsClosed toSubmodule_1.carrier},
  { toSubmodule := toSubmodule, isClosed' := isClosed' } = { toSubmodule := toSubmodule_1, isClosed' := isClosed'_1 } →
    toSubmodule = toSubmodule_1
-- Init.Data.RArray
Lean.RArray.branch.injEq : ∀ {α : Type u} (a : ℕ) (a_1 a_2 : Lean.RArray α) (a_3 : ℕ) (a_4 a_5 : Lean.RArray α),
  (Lean.RArray.branch a a_1 a_2 = Lean.RArray.branch a_3 a_4 a_5) = (a = a_3 ∧ a_1 = a_4 ∧ a_2 = a_5)
-- Init.Data.Nat.Basic
Nat.succ_add : ∀ (n m : ℕ), n.succ + m = (n + m).succ
-- Init.Data.Format.Basic
/-- The empty format.  -/
Std.Format.nil : Std.Format
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.eq_diseq_subst_cert : ℤ → ℤ → Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Poly → Bool
-- Init.Data.Int.DivMod.Lemmas
Int.emod_eq_of_lt : ∀ {a b : ℤ}, 0 ≤ a → a < b → a % b = a
-- Std.Internal.Do.Order.Heyting
Lean.Order.propSup.eq_1 : ∀ (c : Prop → Prop), Lean.Order.propSup c = ∃ p, c p ∧ p
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Tactic.ComputeAsymptotics.Seq.dist_le_one : ∀ {α : Type u_1} (s t : Stream'.Seq α), dist s t ≤ 1
-- Mathlib.Algebra.Category.Grp.Limits
AddCommGrpCat.forget₂AddGroup_preservesLimit : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommGrpCat),
  CategoryTheory.Limits.PreservesLimit F (CategoryTheory.forget₂ AddCommGrpCat AddGrpCat)
-- Mathlib.Algebra.Lie.Engel
Function.Surjective.isEngelian : ∀ {R : Type u₁} {L : Type u₂} {L₂ : Type u₃} [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₂},
  Function.Surjective ⇑f → LieAlgebra.IsEngelian R L → LieAlgebra.IsEngelian R L₂
-- Mathlib.Data.Set.NAry
Set.image2_subset_right : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s s' : Set α} {t : Set β},
  s ⊆ s' → Set.image2 f s t ⊆ Set.image2 f s' t