mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.FDeriv.Prod
differentiableWithinAt_pi'' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {s : Set E} {ι : Type u_6} {F' : ι → Type u_7}
  [inst_3 : (i : ι) → NormedAddCommGroup (F' i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i},
  (∀ (i : ι), DifferentiableWithinAt 𝕜 (fun x => Φ x i) s x) → DifferentiableWithinAt 𝕜 Φ s x
-- Init.Data.String.Basic
String.Pos.ofReplaceStart : {s : String} → {p₀ : s.Pos} → (s.sliceFrom p₀).Pos → s.Pos
-- Mathlib.Analysis.Calculus.Deriv.Linear
LinearMap.hasDerivWithinAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {x : 𝕜} {s : Set 𝕜} (e : 𝕜 →ₗ[𝕜] F), HasDerivWithinAt (⇑e) (e 1) s x
-- Mathlib.Analysis.Normed.Group.AddTorsor
dist_vsub_cancel_right : ∀ {V : Type u_2} {P : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] (x y z : P), dist (x -ᵥ z) (y -ᵥ z) = dist x y
-- Mathlib.Combinatorics.SimpleGraph.Hasse
SimpleGraph.hasseDualIso_symm_apply : ∀ {α : Type u_1} [inst : Preorder α] (a : α), SimpleGraph.hasseDualIso.symm a = OrderDual.toDual a
-- Mathlib.Analysis.SpecialFunctions.FrullaniIntegral
Frullani.tendsto_integral_inv_smul_of_tendsto_uniform : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} [CompleteSpace E],
  MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume →
    0 < a →
      0 < b →
        ∀ {F : Filter ℝ},
          (∀ᶠ (t : ℝ) in F, 0 < t) →
            ∀ {V : E},
              (∀ δ > 0, ∀ᶠ (t : ℝ) in F, ∀ x ∈ Set.uIoc (a * t) (b * t), ‖f x - V‖ ≤ δ) →
                Filter.Tendsto (fun t => ∫ (x : ℝ) in a * t..b * t, x⁻¹ • f x) F (nhds (Real.log (b / a) • V))
-- Mathlib.Analysis.Convex.Continuous
ConvexOn.continuousOn_interior : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {C : Set E} {f : E → ℝ}
  [FiniteDimensional ℝ E], ConvexOn ℝ C f → ContinuousOn f (interior C)
-- Mathlib.Order.SymmDiff
symmDiff.eq_1 : ∀ {α : Type u_2} [inst : Max α] [inst_1 : SDiff α] (a b : α), symmDiff a b = a \ b ⊔ b \ a
-- Init.Data.Slice.Notation
/-- Slices `carrier` from `range.lower` to `range.upper`, both exclusive.
   -/
Std.Roo.Sliceable.mkSlice : {α : Type u} → {β : outParam (Type v)} → {γ : outParam (Type w)} → [self : Std.Roo.Sliceable α β γ] → α → Std.Roo β → γ
-- Mathlib.Data.Multiset.Dedup
Multiset.mem_dedup : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α}, a ∈ s.dedup ↔ a ∈ s
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.opNorm_eq_of_bounds : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
  (f : NormedAddGroupHom V₁ V₂) {M : ℝ},
  0 ≤ M → (∀ (x : V₁), ‖f x‖ ≤ M * ‖x‖) → (∀ N ≥ 0, (∀ (x : V₁), ‖f x‖ ≤ N * ‖x‖) → M ≤ N) → ‖f‖ = M
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
intervalIntegral.FTCFilter.nhdsWithinSingleton : ∀ (a : ℝ), intervalIntegral.FTCFilter a (nhdsWithin a {a}) ⊥
-- Mathlib.Order.Filter.Basic
Filter.EventuallyLE.le_sup_of_le_left : ∀ {α : Type u} {β : Type v} [inst : SemilatticeSup β] {l : Filter α} {f g h : α → β}, h ≤ᶠ[l] f → h ≤ᶠ[l] f ⊔ g
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.withAlts.loop : {α : Type} →
  Lean.Expr →
    Array Lean.Expr →
      Array Lean.Meta.Match.DiscrInfo →
        Option Lean.Meta.Match.Overlaps →
          (List Lean.Meta.Match.Alt → Array Lean.Expr → Array Lean.Meta.Match.AltParamInfo → Lean.MetaM α) →
            List Lean.Meta.Match.AltLHS →
              List Lean.Meta.Match.Alt →
                Array Lean.Expr → Array Lean.Meta.Match.AltParamInfo → Array Lean.Expr → Lean.MetaM α
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.OuterMeasure.le_mkMetric : ∀ {X : Type u_2} [inst : EMetricSpace X] (m : ENNReal → ENNReal) (μ : MeasureTheory.OuterMeasure X) (r : ENNReal),
  0 < r → (∀ (s : Set X), Metric.ediam s ≤ r → μ s ≤ m (Metric.ediam s)) → μ ≤ MeasureTheory.OuterMeasure.mkMetric m
-- Mathlib.Data.Fin.VecNotation
Matrix.vecAppend_eq_ite : ∀ {m n : ℕ} {α : Type u_1} {o : ℕ} (ho : o = m + n) (u : Fin m → α) (v : Fin n → α),
  Matrix.vecAppend ho u v = fun i => if h : ↑i < m then u ⟨↑i, h⟩ else v ⟨↑i - m, ⋯⟩
-- Mathlib.Algebra.Lie.Weights.Linear
LieModule.LinearWeights.map_smul : ∀ {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} [self : LieModule.LinearWeights R L M] (χ : L → R),
  LieModule.genWeightSpace M χ ≠ ⊥ → ∀ (t : R) (x : L), χ (t • x) = t • χ x
-- Mathlib.Order.KrullDimension
/-- The elements of finite coheight `n` are the maximal elements among those of coheight `≥ n`.  -/
Order.coheight_eq_coe_iff_maximal_le_coheight : ∀ {α : Type u_1} [inst : Preorder α] {a : α} {n : ℕ}, Order.coheight a = ↑n ↔ Maximal (fun y => ↑n ≤ Order.coheight y) a
-- Lean.Meta.Tactic.Grind.Types
/-- If `funCC := true`, then the expression associated with this entry is an application, and
function congruence closure is enabled for it.
See `Grind.Config.funCC` for additional details.
 -/
Lean.Meta.Grind.ENode.funCC : Lean.Meta.Grind.ENode → Bool
-- Mathlib.Order.Atoms
isLUB_atoms_le : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderBot α] [IsAtomistic α] (b : α), IsLUB {a | IsAtom a ∧ a ≤ b} b
-- Mathlib.Order.CompleteLattice.Lemmas
inf_eq_iInf : ∀ {α : Type u_1} [inst : CompleteLattice α] (x y : α), x ⊓ y = ⨅ b, bif b then x else y
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Additive.linearOrder : {α : Type u_1} → [LinearOrder α] → LinearOrder (Additive α)
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.continuous : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
  (f : BoundedContinuousFunction α β), Continuous ⇑f
-- Mathlib.Combinatorics.Additive.Convolution
Finset.addConvolution_le_card_left : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] {A B : Finset G} {x : G}, A.addConvolution B x ≤ A.card
-- Mathlib.CategoryTheory.Limits.Cones
/-- If `F` and `G` are naturally isomorphic functors, then they have equivalent categories of
cones.
 -/
CategoryTheory.Limits.Cone.postcomposeEquivalence : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F G : CategoryTheory.Functor J C} → (F ≅ G) → (CategoryTheory.Limits.Cone F ≌ CategoryTheory.Limits.Cone G)
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.Discrete.mk.injEq : ∀ {α : Type u₁} (as as_1 : α), ({ as := as } = { as := as_1 }) = (as = as_1)
-- Mathlib.GroupTheory.GroupAction.Defs
/-- When you take a set `U` in `α`, push it down to the quotient, and pull back, you get the union
of the orbit of `U` under `G`.  -/
MulAction.quotient_preimage_image_eq_union_mul : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] (U : Set α),
  Quotient.mk' ⁻¹' Quotient.mk' '' U = ⋃ g, (fun x => g • x) '' U
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.ofRingEquiv_apply : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] {f : A₁ ≃+* A₂}
  (hf : ∀ (x : R), f ((algebraMap R A₁) x) = (algebraMap R A₂) x) (a : A₁), (AlgEquiv.ofRingEquiv hf) a = f a
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.copy.eq_1 : ∀ {M : Type u_1} [inst : MulOneClass M] (S : Submonoid M) (s : Set M) (hs : s = ↑S),
  S.copy s hs = { carrier := s, mul_mem' := ⋯, one_mem' := ⋯ }
-- Mathlib.RepresentationTheory.Irreducible
Representation.IsIrreducible.injective_or_eq_zero : ∀ {G : Type u_1} {k : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Field k]
  [inst_2 : AddCommGroup V] [inst_3 : Module k V] [inst_4 : AddCommGroup W] [inst_5 : Module k W]
  {ρ : Representation k G V} {σ : Representation k G W} (f : ρ.IntertwiningMap σ) [ρ.IsIrreducible],
  Function.Injective ⇑f ∨ f = 0
-- Lean.Meta.Tactic.Grind.MatchCond
_private.Lean.Meta.Tactic.Grind.MatchCond.0.Lean.Meta.Grind.collectMatchCondLhssAndAbstract.go : Lean.Expr →
  Array (Lean.Expr × Option Lean.Expr) →
    ℕ →
      Array Lean.Expr →
        Array (Option Lean.Expr) →
          Array Lean.Expr → Array Lean.Expr → Lean.Meta.Grind.GoalM (Array Lean.Expr × Lean.Expr)
-- Mathlib.RingTheory.Polynomial.Pochhammer
ascPochhammer_nat_eq_natCast_descFactorial : ∀ (S : Type u_1) [inst : Semiring S] (a b : ℕ),
  Polynomial.eval (↑a) (ascPochhammer S b) = ↑((a + b - 1).descFactorial b)
-- Mathlib.SetTheory.Ordinal.FundamentalSequence
Ordinal.IsFundamentalSequence.blsub_eq : ∀ {a o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{u}}, a.IsFundamentalSequence o f → o.blsub f = a
-- Mathlib.ModelTheory.Order
FirstOrder.Language.orderLHom_onFunction : ∀ (L : FirstOrder.Language) [inst : L.IsOrdered] {n : ℕ} (a : FirstOrder.Language.order.Functions n),
  L.orderLHom.onFunction a = isEmptyElim a
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
/-- The identity prelax functor.  -/
CategoryTheory.PrelaxFunctor.id : (B : Type u₁) → [inst : CategoryTheory.Bicategory B] → CategoryTheory.PrelaxFunctor B B
-- Mathlib.Order.Filter.Map
Function.Commute.filter_comap : ∀ {α : Type u_1} {f g : α → α}, Function.Commute f g → Function.Commute (Filter.comap f) (Filter.comap g)
-- Mathlib.RingTheory.PowerSeries.Order
PowerSeries.le_order_map : ∀ {R : Type u_1} [inst : Semiring R] {φ : PowerSeries R} {S : Type u_2} [inst_1 : Semiring S] (f : R →+* S),
  φ.order ≤ ((PowerSeries.map f) φ).order
-- Mathlib.Algebra.Module.Presentation.Cokernel
Module.Presentation.ofExact_R : ∀ {A : Type u} [inst : Ring A] {M₁ : Type v₁} {M₂ : Type v₂} {M₃ : Type v₃} [inst_1 : AddCommGroup M₁]
  [inst_2 : Module A M₁] [inst_3 : AddCommGroup M₂] [inst_4 : Module A M₂] [inst_5 : AddCommGroup M₃]
  [inst_6 : Module A M₃] {f : M₁ →ₗ[A] M₂} {g : M₂ →ₗ[A] M₃} (pres₂ : Module.Presentation A M₂) {ι : Type w₁}
  {g₁ : ι → M₁} (data : pres₂.CokernelData f g₁) (hfg : Function.Exact ⇑f ⇑g) (hg : Function.Surjective ⇑g)
  (hg₁ : Submodule.span A (Set.range g₁) = ⊤), (pres₂.ofExact data hfg hg hg₁).R = (pres₂.R ⊕ ι)
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_sub_natCast_mul' : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℕ), toIocMod hp (a - ↑m * p) b = toIocMod hp a b - ↑m * p
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.exists_eq_zero : ∀ {ι : 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 : ι) → Zero (G i)] [∀ (i j : ι) (h : i ≤ j), ZeroHomClass (T h) (G i) (G j)] (x : (i : ι) × G i),
  ⟦x⟧ = 0 ↔ ∃ i, ∃ (h : x.fst ≤ i), (f x.fst i h) x.snd = 0
-- Mathlib.Analysis.Calculus.Deriv.Inverse
/-- If `f (g y) = y` for `y` in some neighborhood of `a`, `g` is continuous at `a`, and `f` has an
invertible derivative `f'` at `g a`, then `g` has the derivative `f'⁻¹` at `a`.

This is one of the easy parts of the inverse function theorem: it assumes that we already have
an inverse function.  -/
HasDerivAt.of_local_left_inverse : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {f g : 𝕜 → 𝕜} {f' a : 𝕜},
  ContinuousAt g a → HasDerivAt f f' (g a) → f' ≠ 0 → (∀ᶠ (y : 𝕜) in nhds a, f (g y) = y) → HasDerivAt g f'⁻¹ a
-- Mathlib.Order.CompleteLattice.Lemmas
ULift.supSet : {α : Type u_1} → [SupSet α] → SupSet (ULift.{v, u_1} α)
-- Mathlib.Data.Tree.Basic
BinaryTree.height.eq_1 : ∀ {α : Type u}, BinaryTree.nil.height = 0
-- Mathlib.Algebra.Lie.Weights.Chain
LieModule.chainTopCoeff.eq_1 : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {M : Type u_3}
  [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] [inst_8 : IsAddTorsionFree R] [inst_9 : IsDomain R]
  [inst_10 : Module.IsTorsionFree R M] [inst_11 : IsNoetherian R M] (α : L → R) (β : LieModule.Weight R L M),
  LieModule.chainTopCoeff α β = if hα : α = 0 then 0 else (Nat.find ⋯).pred
-- Mathlib.RingTheory.Derivation.DifferentialRing
/-- A differential algebra is an `Algebra` where the derivation commutes with `algebraMap`.
 -/
DifferentialAlgebra : (A : Type u_1) →
  (B : Type u_2) →
    [inst : CommRing A] → [inst_1 : CommRing B] → [Algebra A B] → [Differential A] → [Differential B] → Prop
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.insertManyIfNewUnit.congr_simp : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {ρ : Type u_1} [inst_1 : ForIn Id ρ α]
  (t t_1 : Std.ExtDTreeMap α (fun x => Unit) cmp),
  t = t_1 →
    ∀ (l l_1 : ρ),
      l = l_1 → Std.ExtDTreeMap.Const.insertManyIfNewUnit t l = Std.ExtDTreeMap.Const.insertManyIfNewUnit t_1 l_1
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- **Alias** of `MeasureTheory.measure_add_sdiff`. -/
MeasureTheory.measure_add_diff : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasureTheory.NullMeasurableSet s μ → ∀ (t : Set α), μ s + μ (t \ s) = μ (s ∪ t)
-- Mathlib.RingTheory.Henselian
/-- A local ring `R` is *Henselian* if the following condition holds:
for every polynomial `f` over `R`, with a *simple* root `a₀` over the residue field,
there exists a lift `a : R` of `a₀` that is a root of `f`.
(Recall that a root `b` of a polynomial `g` is *simple* if it is not a double root, so if
`g.derivative.eval b ≠ 0`.)

In other words, `R` is local Henselian if it is Henselian at the ideal `I`,
in the sense of `HenselianRing`.  -/
HenselianLocalRing : (R : Type u_1) → [CommRing R] → Prop
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasurableEquiv.symm_smul : ∀ {G : Type u_1} {α : Type u_3} [inst : MeasurableSpace α] [inst_1 : Group G] [inst_2 : MulAction G α]
  [inst_3 : MeasurableConstSMul G α] (c : G), (MeasurableEquiv.smul c).symm = MeasurableEquiv.smul c⁻¹
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.coe_ofAddEquiv : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Add α], ⇑Matrix.ofAddEquiv = ⇑Matrix.of
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
IsAbsoluteValue.abv_add : ∀ {S : Type u_5} [inst : Semiring S] [inst_1 : PartialOrder S] {R : Type u_6} [inst_2 : Semiring R] (abv : R → S)
  [IsAbsoluteValue abv] (x y : R), abv (x + y) ≤ abv x + abv y
-- Mathlib.LinearAlgebra.TensorProduct.Tower
LinearEquiv.baseChange_inv : ∀ (R : Type u_1) (A : Type u_2) (M : Type u_4) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (e : M ≃ₗ[R] M),
  LinearEquiv.baseChange R A M M e⁻¹ = (LinearEquiv.baseChange R A M M e)⁻¹
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
_private.Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree.0.WeierstrassCurve.expCoeff : ℕ → ℤ
-- Mathlib.Data.Rat.Defs
Rat.divInt_ne_zero : ∀ {a b : ℤ}, b ≠ 0 → (Rat.divInt a b ≠ 0 ↔ a ≠ 0)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
CategoryTheory.Functor.whiskerRight_zero : ∀ {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] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  [inst_4 : CategoryTheory.Limits.HasZeroMorphisms E] {F G : CategoryTheory.Functor C D}
  (H : CategoryTheory.Functor D E) [H.PreservesZeroMorphisms], CategoryTheory.Functor.whiskerRight 0 H = 0
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?_insertEntry_of_beq : ∀ {α : Type u} {β : Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α} {v : β},
  (k == a) = true → Std.Internal.List.getValue? a (Std.Internal.List.insertEntry k v l) = some v
-- Init.Data.Int.Basic
/-- Converts an integer into a natural number. Returns `none` for negative numbers.

Examples:
* `(7 : Int).toNat? = some 7`
* `(0 : Int).toNat? = some 0`
* `(-7 : Int).toNat? = none`
 -/
Int.toNat? : ℤ → Option ℕ
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
/-- `sigma_eq_one_iff` is to be preferred.  -/
_private.Mathlib.NumberTheory.ArithmeticFunction.Misc.0.ArithmeticFunction.sigma_zero_eq_one_iff : ∀ (n : ℕ), (ArithmeticFunction.sigma 0) n = 1 ↔ n = 1
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.congr_toOrderHom_apply : ∀ {a b : SimplexCategory} {f g : a ⟶ b},
  f = g → ∀ (x : Fin (a.len + 1)), (SimplexCategory.Hom.toOrderHom f) x = (SimplexCategory.Hom.toOrderHom g) x
-- Mathlib.SetTheory.Ordinal.Veblen
/-- `veblen o₁ a ≤ veblen o₂ b` iff one of the following holds:
* `o₁ = o₂` and `a ≤ b`
* `o₁ < o₂` and `a ≤ veblen o₂ b`
* `o₁ > o₂` and `veblen o₁ a ≤ b`  -/
Ordinal.veblen_le_veblen_iff : ∀ {o₁ o₂ a b : Ordinal.{u}},
  Ordinal.veblen o₁ a ≤ Ordinal.veblen o₂ b ↔
    o₁ = o₂ ∧ a ≤ b ∨ o₁ < o₂ ∧ a ≤ Ordinal.veblen o₂ b ∨ o₂ < o₁ ∧ Ordinal.veblen o₁ a ≤ b
-- Mathlib.Order.WithBot
WithBot.toDual_le_toDual_iff : ∀ {α : Type u_1} [inst : LE α] {x y : WithBot α}, WithBot.toDual x ≤ WithBot.toDual y ↔ y ≤ x
-- Mathlib.Analysis.Normed.Group.Ultra
IsUltrametricDist.nnnorm_zsmul_le : ∀ {S : Type u_1} [inst : SeminormedAddGroup S] [IsUltrametricDist S] (x : S) (z : ℤ), ‖z • x‖₊ ≤ ‖x‖₊
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.rTensor_comp_lTensor : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : CommSemiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : AddCommMonoid U] [inst_5 : Module A V]
  [inst_6 : Module A W] [inst_7 : Module A U] {ρ : Representation A G V} {σ : Representation A G W}
  {τ : Representation A G U} {Q : Type u_7} [inst_8 : AddCommMonoid Q] [inst_9 : Module A Q] {υ : Representation A G Q}
  (f : ρ.IntertwiningMap τ) (g : σ.IntertwiningMap υ),
  (Representation.IntertwiningMap.rTensor υ f).comp (Representation.IntertwiningMap.lTensor ρ g) = f.tensor g
-- Std.Internal.Do.Order.PreservesSup
/-- Landing below the frame closure reduces to landing below the base transformer together with
framing: if `pre ⊑ k Q` and `k` frames every `op r` (`op r (k Q') ⊑ k (fun a => op r (Q' a))`), then
`pre ⊑ frameClosure op k Q`.  -/
Lean.Order.PreservesSup.le_frameClosure : ∀ {α : Type u} [inst : Lean.Order.CompleteLattice α] {R : Type v} {β : Type w} (op : R → α → α)
  [∀ (r : R), Lean.Order.PreservesSup (op r)] (k : (β → α) → α) {Q : β → α} {pre : α},
  (∀ (r : R) (Q' : β → α), Lean.Order.PartialOrder.rel (op r (k Q')) (k fun a => op r (Q' a))) →
    Lean.Order.PartialOrder.rel pre (k Q) →
      Lean.Order.PartialOrder.rel pre (Lean.Order.PreservesSup.frameClosure op k Q)
-- Mathlib.RingTheory.PicardGroup
Module.Flat.toAlgebra_injective : ∀ {R : Type u} {M : Type v} {A : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Semiring A] [inst_4 : Algebra R A] (e : TensorProduct R A M ≃ₗ[A] A) [Module.Flat R M] [FaithfulSMul R A],
  Function.Injective ⇑(Module.Flat.toAlgebra e)
-- Init.Data.Ord.SInt
ISize.instOrd : Ord ISize
-- Lean.Environment
_private.Lean.Environment.0.Lean.Kernel.Environment.irBaseExts : Lean.Kernel.Environment → Array Lean.EnvExtensionState
-- Mathlib.Data.Set.Lattice
Set.iUnion_const : ∀ {β : Type u_2} {ι : Sort u_5} [Nonempty ι] (s : Set β), ⋃ x, s = s
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- The Law of Quadratic Reciprocity for the Jacobi symbol: if `a` and `b` are natural numbers
with `a` odd and `b % 4 = 1`, then `J(a | b) = J(b | a)`.  -/
jacobiSym.quadratic_reciprocity_one_mod_four' : ∀ {a b : ℕ}, Odd a → b % 4 = 1 → jacobiSym (↑a) b = jacobiSym (↑b) a
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.Iso.hom_inv_id_app_app : ∀ {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]
  {F G : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (e : F ≅ G) (X₁ : C) (X₂ : D),
  CategoryTheory.CategoryStruct.comp ((e.hom.app X₁).app X₂) ((e.inv.app X₁).app X₂) =
    CategoryTheory.CategoryStruct.id ((F.obj X₁).obj X₂)
-- Mathlib.Algebra.Order.Group.End
OrderHom.instMul : {α : Type u_1} → [inst : Preorder α] → Mul (α →o α)
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
HomotopicalAlgebra.RightHomotopyRel.postcomp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {f g : X ⟶ Y} [HomotopicalAlgebra.IsCofibrant X],
  HomotopicalAlgebra.RightHomotopyRel f g →
    ∀ {Z : C} (p : Y ⟶ Z),
      HomotopicalAlgebra.RightHomotopyRel (CategoryTheory.CategoryStruct.comp f p)
        (CategoryTheory.CategoryStruct.comp g p)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Complex.tan_int_mul_pi_div_two : ∀ (n : ℤ), Complex.tan (↑n * ↑Real.pi / 2) = 0
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.Subgraph.IsMatching.toEdge.eq_1 : ∀ {V : Type u_1} {G : SimpleGraph V} {M : G.Subgraph} (h : M.IsMatching) (v : ↑M.verts),
  h.toEdge v = ⟨s(↑v, Exists.choose ⋯), ⋯⟩
-- Init.Data.Iterators.Combinators.Monadic.Take
Std.Iterators.Types.Take.mk.congr_simp : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] (countdown countdown_1 : ℕ)
  (e_countdown : countdown = countdown_1) (inner inner_1 : Std.IterM m β),
  inner = inner_1 →
    ∀ (finite : countdown > 0 ∨ Std.Iterators.Finite α m),
      { countdown := countdown, inner := inner, finite := finite } =
        { countdown := countdown_1, inner := inner_1, finite := ⋯ }
-- Init.Data.UInt.Lemmas
USize.ofBitVec_uInt32ToBitVec : ∀ (n : UInt32), { toBitVec := BitVec.setWidth System.Platform.numBits n.toBitVec } = n.toUSize
-- Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
le_or_le_of_add_le_add : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : Add α] [AddLeftStrictMono α] [AddRightStrictMono α] {a₁ a₂ b₁ b₂ : α},
  a₁ + b₁ ≤ a₂ + b₂ → a₁ ≤ a₂ ∨ b₁ ≤ b₂
-- Mathlib.Algebra.Polynomial.Div
/-- The multiplicity of `p + q` is at least the minimum of the multiplicities.  -/
Polynomial.rootMultiplicity_add : ∀ {R : Type u} [inst : CommRing R] {p q : Polynomial R} (a : R),
  p + q ≠ 0 →
    min (Polynomial.rootMultiplicity a p) (Polynomial.rootMultiplicity a q) ≤ Polynomial.rootMultiplicity a (p + q)
-- Mathlib.MeasureTheory.Measure.FiniteMeasureProd
MeasureTheory.FiniteMeasure.toMeasure_prod : ∀ {α : Type u_1} [inst : MeasurableSpace α] {β : Type u_2} [inst_1 : MeasurableSpace β]
  (μ : MeasureTheory.FiniteMeasure α) (ν : MeasureTheory.FiniteMeasure β), ↑(μ.prod ν) = (↑μ).prod ↑ν
-- Mathlib.Algebra.Group.ULift
ULift.sub : {α : Type u} → [Sub α] → Sub (ULift.{u_1, u} α)
-- Mathlib.Topology.MetricSpace.HausdorffDimension
/-- If `f` is a Lipschitz continuous map, then the Hausdorff dimension of its range is at most the
Hausdorff dimension of its domain.  -/
LipschitzWith.dimH_range_le : ∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] {K : NNReal} {f : X → Y},
  LipschitzWith K f → dimH (Set.range f) ≤ dimH Set.univ
-- Mathlib.RingTheory.HopkinsLevitzki
IsArtinianRing.tfae : ∀ (R : Type u_2) (M : Type u) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsArtinianRing R],
  [Module.Finite R M, IsNoetherian R M, IsArtinian R M, IsFiniteLength R M].TFAE
-- Init.Data.Range.Polymorphic.IntLemmas
Int.size_roo : ∀ {a b : ℤ}, (a<...b).size = (b - a - 1).toNat
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.Measure.hausdorffMeasure_le_one_of_subsingleton : ∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] {s : Set X},
  s.Subsingleton → ∀ {d : ℝ}, 0 ≤ d → (MeasureTheory.Measure.hausdorffMeasure d) s ≤ 1
-- Lean.Elab.PreDefinition.WF.Fix
Lean.Elab.WF.debug.definition.wf.replaceRecApps : Lean.Option Bool
-- Mathlib.Data.Set.Functor
Set.orElse_def : ∀ {α : Type u} (s t : Set α), (s <|> t) = s ∪ t