mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.Const.getEntryGT.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Ord α] →
      (k : α) →
        (motive :
            (x : Std.DTreeMap.Internal.Impl α fun x => β) →
              x.Ordered → (∃ a ∈ x, compare a k = Ordering.gt) → Sort u_3) →
          (x : Std.DTreeMap.Internal.Impl α fun x => β) →
            (x_1 : x.Ordered) →
              (x_2 : ∃ a ∈ x, compare a k = Ordering.gt) →
                ((x : Std.DTreeMap.Internal.Impl.leaf.Ordered) →
                    (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.leaf, compare a k = Ordering.gt) →
                      motive Std.DTreeMap.Internal.Impl.leaf x he) →
                  ((size : ℕ) →
                      (ky : α) →
                        (y : β) →
                          (l r : Std.DTreeMap.Internal.Impl α fun x => β) →
                            (ho : (Std.DTreeMap.Internal.Impl.inner size ky y l r).Ordered) →
                              (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.inner size ky y l r, compare a k = Ordering.gt) →
                                motive (Std.DTreeMap.Internal.Impl.inner size ky y l r) ho he) →
                    motive x x_1 x_2
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurableSet_pi_of_nonempty : ∀ {δ : Type u_4} {X : δ → Type u_6} [inst : (a : δ) → MeasurableSpace (X a)] {s : Set δ} {t : (i : δ) → Set (X i)},
  s.Countable → (s.pi t).Nonempty → (MeasurableSet (s.pi t) ↔ ∀ i ∈ s, MeasurableSet (t i))
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infiniteNeg_of_tendsto_bot : ∀ {f : ℕ → ℝ}, Filter.Tendsto f Filter.atTop Filter.atBot → (Hyperreal.ofSeq f).InfiniteNeg
-- Mathlib.Algebra.Group.Units.Hom
/-- If a homomorphism `f : M →+ N` sends each element to an `IsAddUnit`, then it can be
lifted to `f : M →+ AddUnits N`. See also `AddUnits.liftRight` for a computable version.  -/
IsAddUnit.liftRight : {M : Type u_3} →
  {N : Type u_4} →
    [inst : AddMonoid M] → [inst_1 : AddMonoid N] → (f : M →+ N) → (∀ (x : M), IsAddUnit (f x)) → M →+ AddUnits N
-- Mathlib.Dynamics.OmegaLimit
/-- A set is eventually carried into any open neighbourhood of its ω-limit:
if `c` is a compact set such that `closure {ϕ t x | t ∈ v, x ∈ s} ⊆ c` for some `v ∈ f`
and `n` is an open neighbourhood of `ω f ϕ s`, then for some `u ∈ f` we have
`closure {ϕ t x | t ∈ u, x ∈ s} ⊆ n`.  -/
eventually_closure_subset_of_isCompact_absorbing_of_isOpen_of_omegaLimit_subset' : ∀ {τ : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (s : Set α)
  {c : Set β},
  IsCompact c →
    (∃ v ∈ f, closure (Set.image2 ϕ v s) ⊆ c) →
      ∀ {n : Set β}, IsOpen n → omegaLimit f ϕ s ⊆ n → ∃ u ∈ f, closure (Set.image2 ϕ u s) ⊆ n
-- Mathlib.MeasureTheory.Integral.Lebesgue.Add
MeasureTheory.measure_support_eapprox_lt_top : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  Measurable f → ∫⁻ (x : α), f x ∂μ ≠ ⊤ → ∀ (n : ℕ), μ (Function.support ⇑(MeasureTheory.SimpleFunc.eapprox f n)) < ⊤
-- Mathlib.Logic.Basic
/-- A two-argument function applied to two `dite`s is a `dite` of that two-argument function
applied to each of the branches.  -/
apply_dite₂ : ∀ {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} (f : α → β → γ) (P : Prop) [inst : Decidable P] (a : P → α) (b : ¬P → α)
  (c : P → β) (d : ¬P → β), f (dite P a b) (dite P c d) = if h : P then f (a h) (c h) else f (b h) (d h)
-- Mathlib.Geometry.Manifold.Immersion
/-- Being an immersion at `x` is a local property.  -/
Manifold.isLocalSourceTargetProperty_immersionAtProp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_7}
  [inst_7 : TopologicalSpace H] {G : Type u_9} [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_9 : TopologicalSpace M] {N : Type u_13}
  [inst_10 : TopologicalSpace N], Manifold.IsLocalSourceTargetProperty (Manifold.ImmersionAtProp F I J M N)
-- Mathlib.CategoryTheory.FiberedCategory.HasFibers
HasFibers.inducedMap.eq_1 : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  {p : CategoryTheory.Functor 𝒳 𝒮} [inst_2 : HasFibers p] {R S : 𝒮} {a : 𝒳} {b b' : HasFibers.Fib p R} (f : R ⟶ S)
  (ψ : (HasFibers.ι R).obj b' ⟶ a) [inst_3 : p.IsCartesian f ψ] (φ : (HasFibers.ι R).obj b ⟶ a)
  [inst_4 : p.IsHomLift f φ],
  HasFibers.inducedMap f ψ φ = HasFibers.Fib.homMk (CategoryTheory.Functor.IsCartesian.map p f ψ φ)
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.homOfLE_faceSingletonComplIso_inv_eq_facePairComplIso_inv_δ_castPred_assoc : ∀ {n : ℕ} (i j : Fin (n + 3)) (h : i < j) {Z : SSet} (h_1 : SSet.stdSimplex.obj { len := n + 1 } ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SSet.Subcomplex.homOfLE ⋯)
      (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.faceSingletonComplIso j).inv h_1) =
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.facePairComplIso i j h).inv
      (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ (i.castPred ⋯)) h_1)
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
AddSubgroup.unop_sup : ∀ {G : Type u_2} [inst : AddGroup G] (S₁ S₂ : AddSubgroup Gᵃᵒᵖ), (S₁ ⊔ S₂).unop = S₁.unop ⊔ S₂.unop
-- Mathlib.CategoryTheory.Limits.Preserves.Filtered
/-- `ReflectsCofilteredLimitsOfSize_shrink.{w, w'} F` tries to obtain
`ReflectsCofilteredLimitsOfSize.{w, w'} F` from some other `ReflectsCofilteredLimitsOfSize F`.
 -/
CategoryTheory.Limits.reflectsCofilteredLimitsOfSize_shrink : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.ReflectsCofilteredLimitsOfSize.{max w w₂, max w' w₂', v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.ReflectsCofilteredLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.Poly.denoteN_add : ∀ {α : Type u_1} [inst : Lean.Grind.NatModule α] (ctx : Lean.Grind.Linarith.Context α) (k : ℤ)
  (x : Lean.Grind.Linarith.Var) (p : Lean.Grind.Linarith.Poly),
  k ≥ 0 →
    Lean.Grind.Linarith.Poly.denoteN ctx (Lean.Grind.Linarith.Poly.add k x p) =
      k.toNat • Lean.Grind.Linarith.Var.denote ctx x + Lean.Grind.Linarith.Poly.denoteN ctx p
-- Mathlib.GroupTheory.FiniteAbelian.Duality
_private.Mathlib.GroupTheory.FiniteAbelian.Duality.0.CommGroup.exists_apply_ne_one_aux : ∀ (G : Type u_1) (M : Type u_2) [inst : CommGroup G] [Finite G] [inst_2 : CommMonoid M],
  (∀ (n : ℕ), n ∣ Monoid.exponent G → ∀ (a : ZMod n), a ≠ 0 → ∃ φ, φ (Multiplicative.ofAdd a) ≠ 1) →
    ∀ {a : G}, a ≠ 1 → ∃ φ, φ a ≠ 1
-- Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
/-- A version of `Finset.one_le_prod'` for `PosMulMono` in place of `MulLeftMono`.  -/
Finset.one_le_prod : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommMonoidWithZero R] [inst_1 : Preorder R] [ZeroLEOneClass R] [PosMulMono R]
  {f : ι → R} {s : Finset ι}, (∀ i ∈ s, 1 ≤ f i) → 1 ≤ ∏ i ∈ s, f i
-- Mathlib.Algebra.Central.Basic
Algebra.IsCentral.self : ∀ (K : Type u) [inst : CommSemiring K], Algebra.IsCentral K K
-- Mathlib.Topology.Compactification.OnePoint.Basic
Homeomorph.onePointCongr_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y) (a : OnePoint X),
  h.onePointCongr a = OnePoint.map (⇑h) a
-- Mathlib.Topology.Connected.PathConnected
isPathConnected_iff_pathConnectedSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] {F : Set X}, IsPathConnected F ↔ PathConnectedSpace ↑F
-- Mathlib.Order.Notation
/-- Set / lattice complement  -/
HasCompl.compl : {α : Type u_1} → [self : HasCompl α] → α → α
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
/-- The universal property of a free group: A function from the generators of `G` to another
group extends in a unique way to a homomorphism from `G`.

Note that since `IsFreeGroup.lift` is expressed as a bijection, it already
expresses the universal property.  -/
IsFreeGroup.unique_lift : ∀ {G : Type u_1} [inst : Group G] [inst_1 : IsFreeGroup G] {H : Type u_2} [inst_2 : Group H]
  (f : IsFreeGroup.Generators G → H), ∃! F, ∀ (a : IsFreeGroup.Generators G), F (IsFreeGroup.of a) = f a
-- Mathlib.RingTheory.Localization.FractionRing
/-- Given a commutative ring `A` with field of fractions `K`,
and an injective ring hom `g : A →+* L` where `L` is a field,
the field hom induced from `K` to `L` maps `x` to `g x` for all
`x : A`.  -/
IsFractionRing.lift_algebraMap : ∀ {A : Type u_4} [inst : CommRing A] {K : Type u_5} [inst_1 : Field K] {L : Type u_7} [inst_2 : Field L]
  [inst_3 : Algebra A K] [inst_4 : IsFractionRing A K] {g : A →+* L} (hg : Function.Injective ⇑g) (x : A),
  (IsFractionRing.lift hg) ((algebraMap A K) x) = g x
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKeyD_insertIfNew : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k a fallback : α} {v : β},
  (m.insertIfNew k v).getKeyD a fallback = if (k == a) = true ∧ k ∉ m then k else m.getKeyD a fallback
-- Std.Http.Protocol.H1.Writer
Std.Http.Protocol.H1.Writer.instBEqState.beq : Std.Http.Protocol.H1.Writer.State → Std.Http.Protocol.H1.Writer.State → Bool
-- Mathlib.Probability.Kernel.Composition.KernelLemmas
ProbabilityTheory.Kernel.parallelComp_comm : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {T : Type u_4} {mX : MeasurableSpace X} {mY : MeasurableSpace Y}
  {mZ : MeasurableSpace Z} {mT : MeasurableSpace T} {κ : ProbabilityTheory.Kernel X Y}
  {η : ProbabilityTheory.Kernel Z T},
  (ProbabilityTheory.Kernel.id.parallelComp κ).comp (η.parallelComp ProbabilityTheory.Kernel.id) =
    (η.parallelComp ProbabilityTheory.Kernel.id).comp (ProbabilityTheory.Kernel.id.parallelComp κ)
-- Lean.Meta.Instances
Lean.Meta.DefaultInstances.mk : Lean.NameMap (List (Lean.Name × ℕ)) → Lean.Meta.PrioritySet → Lean.Meta.DefaultInstances
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Covariant.flip : ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop}, Covariant M N μ r → Covariant M N μ (flip r)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.mk_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {Y : C} {S : CategoryTheory.Functor C D} (f : S.obj Y ⟶ T), (CategoryTheory.CostructuredArrow.mk f).left = Y
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
CategoryTheory.LaxFunctor.map₂_rightUnitor_hom_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.LaxFunctor B CategoryTheory.Cat) {a b : B}
  (f : a ⟶ b) (X : ↑(F.obj a)) {Z : ↑(F.obj b)}
  (h : (CategoryTheory.CategoryStruct.id (F.obj b)).toFunctor.obj ((F.map f).toFunctor.obj X) ⟶ Z),
  h =
    CategoryTheory.CategoryStruct.comp ((F.mapId b).toNatTrans.app ((F.map f).toFunctor.obj X))
      (CategoryTheory.CategoryStruct.comp ((F.mapComp f (CategoryTheory.CategoryStruct.id b)).toNatTrans.app X)
        (CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom).toNatTrans.app X)
          h))
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.names : Array String
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.w₀₂_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (self : CategoryTheory.ShortComplex.SnakeInput C) {Z : CategoryTheory.ShortComplex C} (h : self.L₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.v₀₁ (CategoryTheory.CategoryStruct.comp self.v₁₂ h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
/-- The power series expansion of `℘'[L - l₀]` at `x`.
See `PeriodPair.hasFPowerSeriesOnBall_derivWeierstrassPExcept`.  -/
PeriodPair.derivWeierstrassPExceptSeries : PeriodPair → ℂ → ℂ → FormalMultilinearSeries ℂ ℂ ℂ
-- Mathlib.Tactic.CategoryTheory.Coherence
Mathlib.Tactic.Coherence.LiftHom.rightUnitorInv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (X : C) →
        [inst_2 : Mathlib.Tactic.Coherence.LiftObj X] →
          Mathlib.Tactic.Coherence.LiftHom (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv
-- Mathlib.GroupTheory.Coxeter.Basic
CoxeterSystem.simple_mul_simple_pow : ∀ {B : Type u_1} {W : Type u_3} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i i' : B),
  (cs.simple i * cs.simple i') ^ M.M i i' = 1
-- Aesop.Script.SpecificTactics
Aesop.Script.TacticBuilder.casesOrObtain : Lean.MVarId → Lean.Expr → Array Aesop.CtorNames → Aesop.Script.TacticBuilder
-- Mathlib.LinearAlgebra.Finsupp.LSum
Finsupp.lcongr_symm_single : ∀ {M : Type u_2} {N : Type u_3} {R : Type u_5} {R₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : AddCommMonoid N] [inst_5 : Module R₂ N] {σ : R →+* R₂}
  {σ_inv : R₂ →+* R} [inst_6 : RingHomInvPair σ σ_inv] [inst_7 : RingHomInvPair σ_inv σ] {ι : Type u_9} {κ : Type u_10}
  (e₁ : ι ≃ κ) (e₂ : M ≃ₛₗ[σ] N) (k : κ) (n : N),
  ((Finsupp.lcongr e₁ e₂).symm fun₀ | k => n) = fun₀ | e₁.symm k => e₂.symm n
-- Mathlib.CategoryTheory.Generator.Basic
/-- We say that `G` is a detector if the functor `C(G, -)` reflects isomorphisms.  -/
CategoryTheory.IsDetector : {C : Type u₁} → [CategoryTheory.Category.{v₁, u₁} C] → C → Prop
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.mapsTo_insertNth_face_Icc : ∀ {n : ℕ} (I : BoxIntegral.Box (Fin (n + 1))) {i : Fin (n + 1)} {x : ℝ},
  x ∈ Set.Icc (I.lower i) (I.upper i) →
    Set.MapsTo (i.insertNth x) (BoxIntegral.Box.Icc (I.face i)) (BoxIntegral.Box.Icc I)
-- Mathlib.Analysis.Meromorphic.FactorizedRational
/-- Helper Lemma: If the support of `d` is finite, then evaluation of functions commutes with finprod,
and the function `∏ᶠ u, (· - u) ^ d u` equals `fun x ↦ ∏ᶠ u, (x - u) ^ d u`.
 -/
Function.FactorizedRational.finprod_eq_fun : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {d : 𝕜 → ℤ},
  Function.HasFiniteSupport d → ∏ᶠ (u : 𝕜), (fun x => x - u) ^ d u = fun x => ∏ᶠ (u : 𝕜), (x - u) ^ d u
-- Mathlib.Geometry.Convex.Cone.Basic
/-- A blunt cone (one not containing `0`) is always salient.  -/
ConvexCone.Blunt.salient : ∀ {R : Type u_2} {G : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup G]
  [inst_3 : SMul R G] {C : ConvexCone R G}, C.Blunt → C.Salient
-- Mathlib.Analysis.Normed.Group.Basic
/-- A group homomorphism from an `AddGroup` to a
`SeminormedAddGroup` induces a `SeminormedAddGroup` structure on the domain.  -/
SeminormedAddGroup.induced : {𝓕 : Type u_1} →
  (E : Type u_5) →
    (F : Type u_6) →
      [inst : FunLike 𝓕 E F] →
        [inst_1 : AddGroup E] → [inst_2 : SeminormedAddGroup F] → [AddMonoidHomClass 𝓕 E F] → 𝓕 → SeminormedAddGroup E
-- Mathlib.Algebra.MonoidAlgebra.Module
MonoidAlgebra.coeffLinearEquiv_symm_apply : ∀ (R : Type u_1) {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Module R S]
  (a : M →₀ S), (MonoidAlgebra.coeffLinearEquiv R).symm a = MonoidAlgebra.ofCoeff a
-- Mathlib.Algebra.Group.Hom.Defs
AddHom.id_apply : ∀ (M : Type u_10) [inst : Add M] (x : M), (AddHom.id M) x = x
-- Mathlib.RingTheory.FiniteType
RingHom.FiniteType.of_finite : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] {f : A →+* B}, f.Finite → f.FiniteType
-- Aesop.Rule.Name
Aesop.DisplayRuleName.ruleName.injEq : ∀ (n n_1 : Aesop.RuleName), (Aesop.DisplayRuleName.ruleName n = Aesop.DisplayRuleName.ruleName n_1) = (n = n_1)
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.expansion.congr_simp : ∀ {G : Type u_1} [inst : Group G] {inst_1 : DecidableEq G} [inst_2 : DecidableEq G] (K K_1 : ℝ),
  K = K_1 →
    ∀ (S S_1 : Finset G),
      S = S_1 → ∀ (A A_1 : Finset G), A = A_1 → Finset.expansion✝ K S A = Finset.expansion✝ K_1 S_1 A_1
-- Mathlib.Analysis.Complex.HasPrimitives
/-- **Morera's theorem for a disk** On a disk, a holomorphic function has primitives.  -/
DifferentiableOn.isExactOn_ball : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {c : ℂ} {r : ℝ} {f : ℂ → E} [CompleteSpace E],
  DifferentiableOn ℂ f (Metric.ball c r) → Complex.IsExactOn f (Metric.ball c r)
-- Mathlib.Combinatorics.Graph.Basic
/-- `G.Adj x y` means that `G` has an edge whose ends are the vertices `x` and `y`.  -/
Graph.Adj : {α : Type u_1} → {β : Type u_2} → Graph α β → α → α → Prop
-- Mathlib.Order.SuccPred.Archimedean
strictMono_of_lt_succ : ∀ {α : Type u_3} {β : Type u_4} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : SuccOrder α]
  [IsSuccArchimedean α] {f : α → β}, (∀ (a : α), ¬IsMax a → f a < f (Order.succ a)) → StrictMono f
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rci.toArray.congr_simp : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_2 : Std.Rxi.IsAlwaysFinite α] (r r_1 : Std.Rci α), r = r_1 → r.toArray = r_1.toArray
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.GrothendieckTopology.Point.presheafFiberCompIso.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] {B : Type u''}
  [inst_2 : CategoryTheory.Category.{v'', u''} B] [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A]
  [inst_4 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} B] (F : CategoryTheory.Functor A B)
  [inst_5 : CategoryTheory.LocallySmall.{w, v, u} C]
  [inst_6 : CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v'', u', u''} F],
  Φ.presheafFiberCompIso F =
    ((CategoryTheory.Functor.whiskeringLeft Φ.fiber.Elementsᵒᵖ Cᵒᵖ A).obj
          (CategoryTheory.CategoryOfElements.π Φ.fiber).op).isoWhiskerLeft
      (CategoryTheory.preservesColimitNatIso F).symm
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.degree_add_eq_right_of_degree_lt : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, p.degree < q.degree → (p + q).degree = q.degree
-- Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
CategoryTheory.SimplicialObject.Homotopy.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : CategoryTheory.SimplicialObject C} →
      {f g : X ⟶ Y} →
        (h : {n : ℕ} → Fin (n + 1) → (X.obj (Opposite.op { len := n }) ⟶ Y.obj (Opposite.op { len := n + 1 }))) →
          (∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (h 0) (Y.δ 0) = g.app (Opposite.op { len := n })) →
            (∀ (n : ℕ),
                CategoryTheory.CategoryStruct.comp (h (Fin.last n)) (Y.δ (Fin.last (n + 1))) =
                  f.app (Opposite.op { len := n })) →
              (∀ {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)),
                  i ≤ j.castSucc →
                    CategoryTheory.CategoryStruct.comp (h j.succ) (Y.δ i.castSucc) =
                      CategoryTheory.CategoryStruct.comp (X.δ i) (h j)) →
                (∀ {n : ℕ} (j : Fin (n + 1)),
                    CategoryTheory.CategoryStruct.comp (h j.succ) (Y.δ j.castSucc.succ) =
                      CategoryTheory.CategoryStruct.comp (h j.castSucc) (Y.δ j.castSucc.succ)) →
                  (∀ {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)),
                      j.castSucc < i →
                        CategoryTheory.CategoryStruct.comp (h j.castSucc) (Y.δ i.succ) =
                          CategoryTheory.CategoryStruct.comp (X.δ i) (h j)) →
                    (∀ {n : ℕ} (i j : Fin (n + 1)),
                        i ≤ j →
                          CategoryTheory.CategoryStruct.comp (h j) (Y.σ i.castSucc) =
                            CategoryTheory.CategoryStruct.comp (X.σ i) (h j.succ)) →
                      (∀ {n : ℕ} (i j : Fin (n + 1)),
                          j ≤ i →
                            CategoryTheory.CategoryStruct.comp (h j) (Y.σ i.succ) =
                              CategoryTheory.CategoryStruct.comp (X.σ i) (h j.castSucc)) →
                        CategoryTheory.SimplicialObject.Homotopy f g
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey?_emptyc : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}, ∅.maxKey? = none
-- Mathlib.Topology.Algebra.Group.Basic
/-- Conjugation is jointly continuous on `G × G` when both `mul` and `inv` are continuous.  -/
IsTopologicalGroup.continuous_conj_prod : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Inv G] [inst_2 : Mul G] [ContinuousMul G] [ContinuousInv G],
  Continuous fun g => g.1 * g.2 * g.1⁻¹
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
opensMeasurableSpace_iff_forall_measurableSet : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α],
  OpensMeasurableSpace α ↔ ∀ (s : Set α), IsOpen s → MeasurableSet s
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.fst_apply : ∀ (M : Type u_1) (α : Type u_2) (β : Type u_3) [inst : SMul M α] [inst_1 : SMul M β],
  ⇑(MulActionHom.fst M α β) = Prod.fst
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
/-- The function `Real.sin` is real analytic.  -/
Real.analyticOnNhd_sin : ∀ {s : Set ℝ}, AnalyticOnNhd ℝ Real.sin s
-- Mathlib.Data.Holor
Holor.cprankMax_mul : ∀ {α : Type} {d : ℕ} {ds : List ℕ} [inst : NonUnitalNonAssocSemiring α] (n : ℕ) (x : Holor α [d]) (y : Holor α ds),
  Holor.CPRankMax n y → Holor.CPRankMax n (x.mul y)
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.find_parent_or : ∀ (self : Batteries.UnionFind) (x : Fin self.size) (i : ℕ),
  (self.find x).fst.parent i = self.rootD i ∧ self.rootD i = self.rootD ↑x ∨ (self.find x).fst.parent i = self.parent i
-- Lean.Parser.Term
Lean.Parser.Term.typeAscription.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Left.one_lt_mul_of_left : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [IsBotOneClass α] [MulLeftMono α] {a : α},
  1 < a → ∀ (b : α), 1 < a * b
-- Mathlib.Order.Preorder.Chain
IsChain.not_le : ∀ {α : Type u_1} {s : Set α} [inst : Preorder α],
  IsChain (fun x1 x2 => x1 ≤ x2) s → ∀ {x y : α}, x ∈ s → y ∈ s → (¬x ≤ y ↔ y < x)
-- Init.Data.Nat.Lemmas
Nat.lt_iff_lt_of_mul_eq_mul : ∀ {a b d c e : ℕ}, a ≠ 0 → a = b * d → a = c * e → (c < b ↔ d < e)
-- Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
Mathlib.Tactic.Bicategory.eval_bicategoricalComp : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} {f g h i : a ⟶ b} {η η' : f ⟶ g} {α : g ≅ h}
  {θ θ' : h ⟶ i} {αθ : g ⟶ i} {ηαθ : f ⟶ i},
  η = η' →
    θ = θ' →
      CategoryTheory.CategoryStruct.comp α.hom θ' = αθ →
        CategoryTheory.CategoryStruct.comp η' αθ = ηαθ →
          CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.comp α.hom θ) = ηαθ
-- Mathlib.Order.Filter.Tendsto
Filter.tendsto_congr : ∀ {α : Type u_1} {β : Type u_2} {f₁ f₂ : α → β} {l₁ : Filter α} {l₂ : Filter β},
  (∀ (x : α), f₁ x = f₂ x) → (Filter.Tendsto f₁ l₁ l₂ ↔ Filter.Tendsto f₂ l₁ l₂)
-- Mathlib.Algebra.Order.GroupWithZero.Synonym
OrderDual.instCommGroupWithZero : {α : Type u_1} → [CommGroupWithZero α] → CommGroupWithZero αᵒᵈ
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.Const.alterKey.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : Unit → motive none) (h_2 : (v : β) → motive (some v)),
  (match none with
    | none => h_1 ()
    | some v => h_2 v) =
    h_1 ()
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If the angle between three points is nonzero, the last two points are not equal.  -/
EuclideanGeometry.right_ne_of_oangle_ne_zero : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P}, EuclideanGeometry.oangle p₁ p₂ p₃ ≠ 0 → p₃ ≠ p₂