mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.instNormSMulClass : ∀ (p : ENNReal) (𝕜 : Type u_1) {ι : Type u_2} (β : ι → Type u_4) [hp : Fact (1 ≤ p)] [inst : Fintype ι]
  [inst_1 : SeminormedRing 𝕜] [inst_2 : (i : ι) → SeminormedAddCommGroup (β i)] [inst_3 : (i : ι) → Module 𝕜 (β i)]
  [∀ (i : ι), NormSMulClass 𝕜 (β i)], NormSMulClass 𝕜 (PiLp p β)
-- Aesop.Options.Public
/-- Enable the builtin `unfold` normalisation rule.
 -/
Aesop.Options.enableUnfold : Aesop.Options → Bool
-- Mathlib.Topology.ContinuousMap.StarOrdered
ContinuousMapZero.instStarOrderedRing : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : Zero α] {R : Type u_2} [inst_2 : TopologicalSpace R]
  [inst_3 : CommSemiring R] [inst_4 : PartialOrder R] [NoZeroDivisors R] [inst_6 : StarRing R] [StarOrderedRing R]
  [inst_8 : IsTopologicalSemiring R] [inst_9 : ContinuousStar R] [StarOrderedRing C(α, R)],
  StarOrderedRing (ContinuousMapZero α R)
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.reverseAux.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (r : List α) (h_1 : (r : List α) → motive [] r)
  (h_2 : (a : α) → (l r : List α) → motive (a :: l) r),
  (match [], r with
    | [], r => h_1 r
    | a :: l, r => h_2 a l r) =
    h_1 r
-- Std.Data.Iterators.Combinators.Monadic.Zip
Std.Iterators.Types.Zip.rel₃_of_left : ∀ {m : Type w → Type w'} {α₁ β₁ : Type w} [inst : Std.Iterator α₁ m β₁] {α₂ β₂ : Type w} [inst_1 : Std.Iterator α₂ m β₂]
  [inst_2 : Std.Iterators.Productive α₁ m] [inst_3 : Std.Iterators.Productive α₂ m] {left' left : Std.IterM m β₁}
  {b : Option { out // ∃ it, it.IsPlausibleOutput out }} {right' right : Std.IterM m β₂},
  left'.finitelyManySkips.Rel left.finitelyManySkips →
    Std.Iterators.Types.Zip.Rel₃ m { internalState := { left := left', memoizedLeft := b, right := right' } }
      { internalState := { left := left, memoizedLeft := b, right := right } }
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.extFunctor.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] (n n_1 : ℕ),
  n = n_1 → CategoryTheory.Abelian.extFunctor n = CategoryTheory.Abelian.extFunctor n_1
-- Mathlib.Combinatorics.Additive.Dissociation
Finset.mem_mulSpan : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : DecidableEq α] [inst_2 : Fintype α] {s : Finset α} {a : α},
  a ∈ s.mulSpan ↔ ∃ ε, (∀ (a : α), ε a = -1 ∨ ε a = 0 ∨ ε a = 1) ∧ ∏ a ∈ s, a ^ ε a = a
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
CategoryTheory.Limits.pullback_snd_iso_of_left_factors_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Z : C} (f : X ⟶ Z) (i : Z ⟶ W)
  [inst_1 : CategoryTheory.Mono i],
  CategoryTheory.IsIso (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp f i) i)
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassFactorizationAt.natDegree_eq_toNat_order_map_of_ne_top : ∀ {A : Type u_1} [inst : CommRing A] {g : PowerSeries A} {f : Polynomial A} {h : PowerSeries A} {I : Ideal A},
  g.IsWeierstrassFactorizationAt f h I → I ≠ ⊤ → f.natDegree = ((PowerSeries.map (Ideal.Quotient.mk I)) g).order.toNat
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.ofList_eq_insertMany! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {l : List ((a : α) × β a)},
  Std.DTreeMap.Internal.Impl.ofList l = ↑(Std.DTreeMap.Internal.Impl.empty.insertMany! l)
-- Init.Data.RArray
_private.Init.Data.RArray.0.Lean.RArray.get_eq_def : ∀ {α : Type u} (a : Lean.RArray α) (n : ℕ),
  a.get n =
    match a with
    | Lean.RArray.leaf x => x
    | Lean.RArray.branch p l r => Bool.rec (l.get n) (r.get n) (p.ble n)
-- Mathlib.LinearAlgebra.Multilinear.Curry
/-- Given a family of modules `N : (ι ⊕ ι') → Type*`, a multilinear map on
`(fun (i : ι) ↦ N (.inl i))` taking values in the space of
linear maps on `(fun (i : ι') ↦ N (.inr i))` induces a multilinear map
on `(fun _ : ι ⊕ ι' => M')` induces.  -/
MultilinearMap.uncurrySum : {R : Type uR} →
  {ι : Type uι} →
    {ι' : Type uι'} →
      {M₂ : Type v₂} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M₂] →
            [inst_2 : Module R M₂] →
              {N : ι ⊕ ι' → Type u_1} →
                [inst_3 : (i : ι ⊕ ι') → AddCommMonoid (N i)] →
                  [inst_4 : (i : ι ⊕ ι') → Module R (N i)] →
                    MultilinearMap R (fun i => N (Sum.inl i)) (MultilinearMap R (fun i => N (Sum.inr i)) M₂) →
                      MultilinearMap R N M₂
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.closedBall_subset_ball : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε₁ ε₂ : ℝ}, ε₁ < ε₂ → Metric.closedBall x ε₁ ⊆ Metric.ball x ε₂
-- Mathlib.CategoryTheory.Presentable.Type
/-- The cocone for `Set.functor X κ : HasCardinalLT.Set X κ ⥤ Type u` with point `X`.  -/
HasCardinalLT.Set.cocone : (X : Type u) → (κ : Cardinal.{u}) → CategoryTheory.Limits.Cocone (HasCardinalLT.Set.functor X κ)
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  (X : HomotopicalAlgebra.BifibrantObject C),
  HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject.obj (HomotopicalAlgebra.BifibrantObject.toHoCat.obj X) =
    HomotopicalAlgebra.CofibrantObject.toHoCat.obj (HomotopicalAlgebra.BifibrantObject.ιCofibrantObject.obj X)
-- Std.Data.DTreeMap.Internal.Operations
/-- A tree map obtained by erasing elements from `t`, bundled with an inductive principle.  -/
Std.DTreeMap.Internal.Impl.IteratedSlowErasureFrom : {α : Type u} → {β : α → Type v} → [Ord α] → Std.DTreeMap.Internal.Impl α β → Type (max 0 u v)
-- Mathlib.Data.Finset.Functor
Finset.lawfulFunctor : ∀ [inst : (P : Prop) → Decidable P], LawfulFunctor Finset
-- Lean.Linter.AmbiguousOpen
/-- Warns if the namespace identifier `nsStx` of an `open` declaration can also be interpreted as an
existing namespace that the `open` declaration silently does not open. `resolved` must be the
interpretations the `open` declaration actually uses, as returned by `resolveNamespace`.
Shadowed interpretations whose declarations are accessible anyway — because the namespace is
already opened without exceptions or encloses the current scope — are not reported.
 -/
Lean.Linter.checkAmbiguousOpen : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadEnv m] →
      [Lean.MonadOptions m] →
        [Lean.MonadLog m] →
          [Lean.AddMessageContext m] → [Lean.MonadResolveName m] → Lean.Ident → List Lean.Name → m Unit
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.add.injEq : ∀ (k : ℤ) (v : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly) (k_1 : ℤ) (v_1 : Lean.Grind.CommRing.Mon)
  (p_1 : Lean.Grind.CommRing.Poly),
  (Lean.Grind.CommRing.Poly.add k v p = Lean.Grind.CommRing.Poly.add k_1 v_1 p_1) = (k = k_1 ∧ v = v_1 ∧ p = p_1)
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.sumAlgEquiv_comp_rename_inr : ∀ (R : Type u) (S₁ : Type v) (S₂ : Type w) [inst : CommSemiring R],
  (↑(MvPolynomial.sumAlgEquiv R S₁ S₂)).comp (MvPolynomial.rename Sum.inr) =
    IsScalarTower.toAlgHom R (MvPolynomial S₂ R) (MvPolynomial S₁ (MvPolynomial S₂ R))
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Group.isNilpotent_prod`.

---

Products of nilpotent groups are nilpotent.  -/
isNilpotent_prod : ∀ {G₁ : Type u_2} {G₂ : Type u_3} [inst : Group G₁] [inst_1 : Group G₂] [Group.IsNilpotent G₁] [Group.IsNilpotent G₂],
  Group.IsNilpotent (G₁ × G₂)
-- Mathlib.MeasureTheory.Measure.Regular
/-- Given a σ-finite measure, any measurable set can be approximated from inside by a measurable
set of finite measure.  -/
MeasureTheory.Measure.InnerRegularWRT.of_sigmaFinite : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ],
  μ.InnerRegularWRT (fun s => MeasurableSet s ∧ μ s ≠ ⊤) fun s => MeasurableSet s
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.mul_def : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] (f g : α →ᵈ α), f * g = f.comp g
-- Lean.Expr
Lean.Expr.forallBody : (a : Lean.Expr) → a.isForall = true → Lean.Expr
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem!_erase : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β],
  m.WF → ∀ {k a : α}, (m.erase k)[a]! = if (k == a) = true then default else m[a]!
-- Mathlib.Algebra.Star.Conjneg
conjneg_apply : ∀ {G : Type u_2} {R : Type u_3} [inst : AddGroup G] [inst_1 : CommSemiring R] [inst_2 : StarRing R] (f : G → R) (x : G),
  conjneg f x = (starRingEnd R) (f (-x))
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
/-- A scheme morphism as a rational map.  -/
AlgebraicGeometry.Scheme.Hom.toRationalMap : {X Y : AlgebraicGeometry.Scheme} → X.Hom Y → X.RationalMap Y
-- Batteries.Data.Array.Match
Array.Matcher.Iterator.mk.injEq : ∀ {σ : Type u_1} {n : Type u_1 → Type u_2} {α : Type u_1} [inst : BEq α] {m : Array.Matcher α}
  [inst_1 : Std.Iterator σ n α] (inner : Std.IterM n α) (state : Fin (m.table.size + 1)) (inner_1 : Std.IterM n α)
  (state_1 : Fin (m.table.size + 1)),
  ({ inner := inner, state := state } = { inner := inner_1, state := state_1 }) = (inner = inner_1 ∧ state = state_1)
-- Batteries.Util.ProofWanted
_private.Batteries.Util.ProofWanted.0.WantedRefKind.noConfusionType : Sort v✝ → WantedRefKind✝ → WantedRefKind✝ → Sort v✝
-- Mathlib.Topology.UniformSpace.Defs
/-- For every set `u ∈ uniformity`, there exists `v ∈ uniformity` such that `v ○ v ⊆ u`.  -/
UniformSpace.Core.comp : ∀ {α : Type u} (self : UniformSpace.Core α), (self.uniformity.lift' fun s => SetRel.comp s s) ≤ self.uniformity
-- Mathlib.Algebra.GroupWithZero.Action.Basic
div_smul_div_comm : ∀ {G : Type u_1} {G₀ : Type u_2} [inst : Group G] [inst_1 : GroupWithZero G₀] [inst_2 : MulAction G G₀]
  [IsScalarTower G G₀ G₀] [SMulCommClass G G₀ G₀] (g h : G) (a b : G₀), (g / h) • (a / b) = g • a / h • b
-- Init.Data.List.TakeDrop
List.take_drop : ∀ {α : Type u_1} {i j : ℕ} {l : List α}, List.take i (List.drop j l) = List.drop j (List.take (j + i) l)
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.equivProd_apply : ∀ {R : Type u_1} (c₁ c₂ c₃ : R) (a : QuaternionAlgebra R c₁ c₂ c₃),
  (QuaternionAlgebra.equivProd c₁ c₂ c₃) a = (a.re, a.imI, a.imJ, a.imK)
-- Mathlib.RingTheory.Norm.Transitivity
Algebra.Norm.Transitivity.auxMat_toSquareBlock_eq : ∀ {S : Type u_2} {m : Type u_5} [inst : CommRing S] (M : Matrix m m S) [inst_1 : DecidableEq m] (k : m),
  (Algebra.Norm.Transitivity.auxMat M k).toSquareBlock (fun x => x ≠ k) False = 1
-- Mathlib.Topology.EMetricSpace.BoundedVariation
BoundedVariationOn.eVariationOn_Ici_eq_Ioi_add_edist : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] [CompleteSpace E]
  [DenselyOrdered α] {f : α → E} {a : α},
  BoundedVariationOn f Set.univ →
    eVariationOn f (Set.Ici a) = eVariationOn f (Set.Ioi a) + edist (f a) (Function.rightLim f a)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.List.forIn'_cons.match_1.eq_2 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.done b))
  (h_2 : (b : β) → motive (ForInStep.yield b)),
  (match ForInStep.yield b with
    | ForInStep.done b => h_1 b
    | ForInStep.yield b => h_2 b) =
    h_2 b
-- Init.Data.String.Lemmas.Basic
String.Slice.slice_endPos : ∀ {s : String.Slice} {p : s.Pos}, s.slice p s.endPos ⋯ = s.sliceFrom p
-- Mathlib.NumberTheory.Dioph
IsPoly.below.proj : ∀ {α : Type u_1} {motive : (a : (α → ℕ) → ℤ) → IsPoly a → Prop} (i : α), IsPoly.below ⋯
-- Mathlib.CategoryTheory.Yoneda
/-- If `F ≅ F'`, and `F` is corepresentable, then `F'` is corepresentable.  -/
CategoryTheory.Functor.CorepresentableBy.ofIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {F F' : CategoryTheory.Functor C (Type v)} → {X : C} → F.CorepresentableBy X → (F ≅ F') → F'.CorepresentableBy X
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.self_comp_symm : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (e : M ≃* N), ⇑e ∘ ⇑e.symm = id
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
ENNReal.log_eq_top_iff : ∀ {x : ENNReal}, x.log = ⊤ ↔ x = ⊤
-- Std.Tactic.BVDecide.LRAT.Internal.LRATCheckerSound
Std.Tactic.BVDecide.LRAT.Internal.Equisat.eq_1 : ∀ (α : Type u) {σ1 : Type v} {σ2 : Type w} [inst : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ1]
  [inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ2] (f1 : σ1) (f2 : σ2),
  Std.Tactic.BVDecide.LRAT.Internal.Equisat α f1 f2 =
    (Std.Tactic.BVDecide.LRAT.Internal.Unsatisfiable α f1 ↔ Std.Tactic.BVDecide.LRAT.Internal.Unsatisfiable α f2)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
/-- The version one probably wants to use more.  -/
Complex.cot_pi_eq_exp_ratio : ∀ (z : ℂ),
  (↑Real.pi * z).cot =
    (Complex.exp (2 * ↑Real.pi * Complex.I * z) + 1) / (Complex.I * (1 - Complex.exp (2 * ↑Real.pi * Complex.I * z)))
-- Mathlib.Analysis.Complex.Liouville
/-- A corollary of Liouville's theorem where the function tends to a finite value at infinity
(i.e., along `Filter.cocompact`, which in proper spaces coincides with `Bornology.cobounded`).  -/
Differentiable.eq_const_of_tendsto_cocompact : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type v} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] [Nontrivial E] {f : E → F},
  Differentiable ℂ f → ∀ {c : F}, Filter.Tendsto f (Filter.cocompact E) (nhds c) → f = Function.const E c
-- Mathlib.Algebra.CharP.Lemmas
add_pow_expChar_pow : ∀ {R : Type u_1} [inst : CommSemiring R] (x y : R) (p n : ℕ) [hR : ExpChar R p], (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n
-- Lean.Message
Lean.MessageLog.empty : Lean.MessageLog
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork_Q : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f)
  (hc : CategoryTheory.Limits.IsColimit c),
  (CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork S hg c hc).Q = c.pt
-- Mathlib.RingTheory.GradedAlgebra.Basic
DirectSum.coe_decompose_mul_of_left_mem_of_not_le : ∀ {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddCommMonoid ι]
  [inst_3 : PartialOrder ι] [CanonicallyOrderedAdd ι] [inst_5 : SetLike σ A] [inst_6 : AddSubmonoidClass σ A]
  (𝒜 : ι → σ) [inst_7 : GradedRing 𝒜] {a b : A} {n i : ι}, a ∈ 𝒜 i → ¬i ≤ n → ↑(((DirectSum.decompose 𝒜) (a * b)) n) = 0
-- Mathlib.CategoryTheory.Skeletal
/-- `IsSkeletonOf C D F` says that `F : D ⥤ C` exhibits `D` as a skeletal full subcategory of `C`,
in particular `F` is a (strong) equivalence and `D` is skeletal.
 -/
CategoryTheory.IsSkeletonOf : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor D C → Prop
-- Mathlib.Topology.Neighborhoods
nhdsWithin_neBot : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {s : Set X},
  (nhdsWithin x s).NeBot ↔ ∀ ⦃t : Set X⦄, t ∈ nhds x → (t ∩ s).Nonempty
-- Mathlib.Combinatorics.Matroid.IndepAxioms
Matroid.ofIsBaseOfFinite_isBase : ∀ {α : Type u_1} {E : Set α} (hE : E.Finite) (IsBase : Set α → Prop) (exists_isBase : ∃ B, IsBase B)
  (isBase_exchange : Matroid.ExchangeProperty IsBase) (subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E),
  (Matroid.ofIsBaseOfFinite hE IsBase exists_isBase isBase_exchange subset_ground).IsBase = IsBase
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- A monad equipped with the ability to construct `Mor₁` terms.  -/
Mathlib.Tactic.BicategoryLike.MkMor₁ : (Type → Type) → Type
-- Mathlib.AlgebraicGeometry.Geometrically.Basic
AlgebraicGeometry.instIsZariskiLocalAtTargetGeometricallyOfIsClosedUnderIsomorphismsScheme : ∀ (P : CategoryTheory.ObjectProperty AlgebraicGeometry.Scheme) [P.IsClosedUnderIsomorphisms],
  AlgebraicGeometry.IsZariskiLocalAtTarget (AlgebraicGeometry.geometrically P)
-- Mathlib.Data.Set.Insert
Set.insert_subset_insert_iff : ∀ {α : Type u_1} {s t : Set α} {a : α}, a ∉ s → (insert a s ⊆ insert a t ↔ s ⊆ t)
-- Mathlib.Algebra.Order.Monovary
monovary_iff_forall_mul_nonneg : ∀ {ι : Type u_1} {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {f g : ι → α},
  Monovary f g ↔ ∀ (i j : ι), 0 ≤ (f j - f i) * (g j - g i)
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.preimage_eval_singleton : ∀ {R : Type u} {a : R} [inst : CommRing R] [inst_1 : IsDomain R] {p : Polynomial R},
  p ≠ Polynomial.C a → (fun x => Polynomial.eval x p) ⁻¹' {a} = (p - Polynomial.C a).rootSet R
-- Mathlib.Data.Fin.SuccPred
Fin.castPred_succAbove : ∀ {n : ℕ} (x : Fin n) (y : Fin (n + 1)) (h : x.castSucc < y) (h' : optParam (y.succAbove x ≠ Fin.last n) ⋯),
  (y.succAbove x).castPred h' = x
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.equivalenceOfReindexing.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C}
  {G : CategoryTheory.Functor K C} (e : K ≌ J) (α : e.functor.comp F ≅ G),
  CategoryTheory.Limits.Cone.equivalenceOfReindexing e α =
    (CategoryTheory.Limits.Cone.whiskeringEquivalence e).trans (CategoryTheory.Limits.Cone.postcomposeEquivalence α)
-- Aesop.Forward.RuleInfo
/-- Discrimination tree keys for the type of this slot. If the slot is for the
rule pattern, it is not associated with a premise, so doesn't have
discrimination tree keys.  -/
Aesop.Slot.typeDiscrTreeKeys? : Aesop.Slot → Option (Array Lean.Meta.DiscrTree.Key)
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get?_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k a : α}, (m.insert k).get? a = if (k == a) = true ∧ k ∉ m then some k else m.get? a
-- Mathlib.Analysis.Convex.Basic
Convex.segment_subset : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {s : Set E}, Convex 𝕜 s → ∀ {x y : E}, x ∈ s → y ∈ s → segment 𝕜 x y ⊆ s
-- Mathlib.Topology.Separation.CompletelyRegular
T35Space.instT3space : ∀ {X : Type u} [inst : TopologicalSpace X] [T35Space X], T3Space X
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.genWeightSpace.congr_simp : ∀ {R : Type u_2} {L : Type u_3} (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] (χ χ_1 : L → R),
  χ = χ_1 → LieModule.genWeightSpace M χ = LieModule.genWeightSpace M χ_1
-- Mathlib.Data.List.Defs
List.iterate.eq_1 : ∀ {α : Type u_1} (f : α → α) (a : α), List.iterate f a 0 = []
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.iso_pullback_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y X : C} (f : Y ≅ X) {Y_1 Z : CategoryTheory.Over X}
  (g : Y_1 ⟶ Z),
  (CategoryTheory.ChosenPullbacksAlong.pullback f.hom).map g =
    CategoryTheory.Over.homMk (CategoryTheory.Over.Hom.left g) ⋯
-- Init.Data.BitVec.Lemmas
BitVec.toNat_intCast : ∀ {w : ℕ} (x : ℤ), (↑x).toNat = (x % 2 ^ w).toNat
-- Mathlib.Order.Interval.Set.Basic
/-- **Alias** of `Set.Iic_sdiff_Iio_same`. -/
Set.Iic_diff_Iio_same : ∀ {α : Type u_1} [inst : PartialOrder α] {a : α}, Set.Iic a \ Set.Iio a = {a}
-- Mathlib.Topology.Homotopy.Basic
/-- the intermediate maps of the homotopy satisfy the property  -/
ContinuousMap.HomotopyWith.prop' : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
  {P : C(X, Y) → Prop} (self : f₀.HomotopyWith f₁ P) (t : ↑unitInterval),
  P { toFun := fun x => self.toFun (t, x), continuous_toFun := ⋯ }
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.Comma.costructuredArrowSndInclusion_obj_hom : ∀ {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] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) (b : B) (X : CategoryTheory.CostructuredArrow L (R.obj b)),
  ((CategoryTheory.Comma.costructuredArrowSndInclusion L R b).obj X).hom = CategoryTheory.CategoryStruct.id b
-- Mathlib.CategoryTheory.Monoidal.Category
/-- curried tensor product of objects  -/
CategoryTheory.MonoidalCategoryStruct.tensorObj : {C : Type u} → {𝒞 : CategoryTheory.Category.{v, u} C} → [self : CategoryTheory.MonoidalCategoryStruct C] → C → C → C
-- Mathlib.Lean.Expr.Basic
/-- `Lean.Expr.le? e` takes `e : Expr` as input.
If `e` represents `a ≤ b`, then it returns `some (t, a, b)`, where `t` is the Type of `a`,
otherwise, it returns `none`.  -/
Lean.Expr.le? : Lean.Expr → Option (Lean.Expr × Lean.Expr × Lean.Expr)
-- Mathlib.NumberTheory.Divisors
Nat.divisor_le : ∀ {n m : ℕ}, n ∈ m.divisors → n ≤ m
-- Mathlib.Analysis.Complex.Periodic
Function.Periodic.tendsto_nhds_zero : ∀ {h : ℝ} {f : ℂ → ℂ},
  ContinuousAt (Function.Periodic.cuspFunction h f) 0 →
    Filter.Tendsto (fun x => f (Function.Periodic.invQParam h x)) (nhdsWithin 0 {0}ᶜ)
      (nhds (Function.Periodic.cuspFunction h f 0))
-- Mathlib.Logic.Function.Basic
/-- A binary injective function is injective when only the left argument varies.  -/
Function.Injective2.left : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β → γ},
  Function.Injective2 f → ∀ (b : β), Function.Injective fun a => f a b
-- Mathlib.SetTheory.ZFC.Basic
/-- A simpler constructor for `ZFSet.Definable₁`.  -/
ZFSet.Definable₁.mk : {f : ZFSet.{u} → ZFSet.{u}} → (out : PSet.{u} → PSet.{u}) → (∀ (x : PSet.{u}), ⟦out x⟧ = f ⟦x⟧) → ZFSet.Definable₁ f
-- Mathlib.Algebra.Order.Field.Basic
/-- For the single implications with fewer assumptions, see `one_div_le_one_div_of_le` and
`le_of_one_div_le_one_div`  -/
one_div_le_one_div : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a b : α} [IsStrictOrderedRing α],
  0 < a → 0 < b → (1 / a ≤ 1 / b ↔ b ≤ a)
-- Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Mathlib.Tactic.Monoidal.evalHorizontalCompAux_of : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {f g h i : C}
  (η : f ⟶ g) (θ : h ⟶ i),
  CategoryTheory.MonoidalCategoryStruct.tensorHom η θ =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Iso.refl (CategoryTheory.MonoidalCategoryStruct.tensorObj f h)).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom η θ)
        (CategoryTheory.Iso.refl (CategoryTheory.MonoidalCategoryStruct.tensorObj g i)).hom)
-- Mathlib.NumberTheory.FLT.MasonStothers
/-- **Polynomial ABC theorem.**  -/
Polynomial.abc : ∀ {k : Type u_1} [inst : Field k] [inst_1 : DecidableEq k] {a b c : Polynomial k},
  a ≠ 0 →
    b ≠ 0 →
      c ≠ 0 →
        IsCoprime a b →
          a + b + c = 0 →
            a.natDegree + 1 ≤ (UniqueFactorizationMonoid.radical (a * b * c)).natDegree ∧
                b.natDegree + 1 ≤ (UniqueFactorizationMonoid.radical (a * b * c)).natDegree ∧
                  c.natDegree + 1 ≤ (UniqueFactorizationMonoid.radical (a * b * c)).natDegree ∨
              Polynomial.derivative a = 0 ∧ Polynomial.derivative b = 0 ∧ Polynomial.derivative c = 0
-- Mathlib.Topology.Order.LeftRight
nhdsLE_sup_nhdsGT : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] (a : α),
  nhdsWithin a (Set.Iic a) ⊔ nhdsWithin a (Set.Ioi a) = nhds a
-- Init.Data.SInt.Lemmas
Int8.neg_ofNat : ∀ {n : ℕ}, -Int8.ofNat n = Int8.ofInt (-↑n)
-- Mathlib.NumberTheory.LegendreSymbol.ZModChar
/-- An explicit description of `χ₈` on integers / naturals  -/
ZMod.χ₈_int_eq_if_mod_eight : ∀ (n : ℤ), ZMod.χ₈ ↑n = if n % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 7 then 1 else -1
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.get' : Lean.Meta.Grind.GoalM Lean.Meta.Grind.Arith.CommRing.State