mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Iterators.Combinators.Monadic.FilterMap
/-- *Note: This is a very general combinator that requires an advanced understanding of monads,
dependent types and termination proofs. The variants `filterMap` and `filterMapM` are easier to use
and sufficient for most use cases.*

If `it` is an iterator, then `it.filterMapWithPostcondition f` is another iterator that applies a
monadic function `f` to all values emitted by `it`. `f` is expected to return an `Option` inside the
monad. If `f` returns `none`, then nothing is emitted; if it returns `some x`, then `x` is emitted.

`f` is expected to return `PostconditionT n (Option _)`. The base iterator `it` being monadic in
`m`, `n` can be different from `m`, but `it.filterMapWithPostcondition f` expects a `MonadLiftT m n`
instance. The `PostconditionT` transformer allows the caller to intrinsically prove properties about
`f`'s return value in the monad `n`, enabling termination proofs depending on the specific behavior
of `f`.

**Marble diagram (without monadic effects):**

```text
it                                ---a --b--c --d-e--⊥
it.filterMapWithPostcondition     ---a'-----c'-------⊥
```

(given that `f a = pure (some a)'`, `f c = pure (some c')` and `f b = f d = d e = pure none`)

**Termination properties:**

* `Finite` instance: only if `it` is finite
* `Productive` instance: only if `it` is finite

For certain mapping functions `f`, the resulting iterator will be finite (or productive) even though
no `Finite` (or `Productive`) instance is provided. For example, if `f` never returns `none`, then
this combinator will preserve productiveness. If `f` is an `ExceptT` monad and will always fail,
then `it.filterMapWithPostcondition` will be finite even if `it` isn't. In the first case, consider
using the `map`/`mapM`/`mapWithPostcondition` combinators instead, which provide more instances out of
the box.

In such situations, the missing instances can be proved manually if the postcondition bundled in
the `PostconditionT n` monad is strong enough. If `f` always returns `some _`, a suitable
postcondition is `fun x => x.isSome`; if `f` always fails, a suitable postcondition might be
`fun _ => False`.

**Performance:**

For each value emitted by the base iterator `it`, this combinator calls `f` and matches on the
returned `Option` value.
 -/
Std.IterM.filterMapWithPostcondition : {α β γ : Type w} →
  {m : Type w → Type w'} →
    {n : Type w → Type w''} →
      [inst : MonadLiftT m n] →
        [Std.Iterator α m β] → (f : β → Std.Iterators.PostconditionT n (Option γ)) → Std.IterM m β → Std.IterM n γ
-- Lean.Structure
/-- Returns the number of fields for a non-recursive structure type.  -/
Lean.getNonRecStructureNumFields : Lean.Environment → Lean.Name → ℕ
-- Lean.Structure
Lean.StructureParentInfo.mk.inj : ∀ {structName : Lean.Name} {subobject : Bool} {projFn structName_1 : Lean.Name} {subobject_1 : Bool}
  {projFn_1 : Lean.Name},
  { structName := structName, subobject := subobject, projFn := projFn } =
      { structName := structName_1, subobject := subobject_1, projFn := projFn_1 } →
    structName = structName_1 ∧ subobject = subobject_1 ∧ projFn = projFn_1
-- Init.Data.List.Sublist
List.reverse_prefix : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.reverse <+: l₂.reverse ↔ l₁ <:+ l₂
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.smul_def : ∀ {K : Type u_2} [inst : CommRing K] {R : Type u_3} [inst_1 : SMul R (FractionRing (Polynomial K))] (x : R)
  (x_1 : RatFunc K),
  RatFunc.smul x x_1 =
    match x, x_1 with
    | r, { toFractionRing := p } => { toFractionRing := r • p }
-- Mathlib.RingTheory.Derivation.MapCoeffs
Differential.algEquiv_deriv : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : Differential A] {R : Type u_2} [inst_2 : CommRing R]
  [inst_3 : Differential R] [inst_4 : Algebra A R] [DifferentialAlgebra A R] {R' : Type u_3} [inst_6 : CommRing R']
  [inst_7 : Differential R'] [inst_8 : Algebra A R'] [DifferentialAlgebra A R'] [IsDomain R'] (f : R ≃ₐ[A] R') (x : R),
  IsSeparable A x → f x′ = (f x)′
-- Mathlib.LinearAlgebra.Dual.Defs
LinearMap.dualMap_id : ∀ {R : Type u_1} {M₁ : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R M₁],
  LinearMap.id.dualMap = LinearMap.id
-- Mathlib.Topology.MetricSpace.Contracting
ContractingWith.edist_efixedPoint_le : ∀ {α : Type u_1} [inst : EMetricSpace α] {K : NNReal} {f : α → α} [inst_1 : CompleteSpace α] (hf : ContractingWith K f)
  {x : α} (hx : edist x (f x) ≠ ⊤), edist x (ContractingWith.efixedPoint f hf x hx) ≤ edist x (f x) / (1 - ↑K)
-- Mathlib.GroupTheory.Perm.Fin
Fin.sign_cycleIcc_of_eq : ∀ {n : ℕ} {i : Fin n}, Equiv.Perm.sign (i.cycleIcc i) = 1
-- Mathlib.Tactic.Positivity.Basic
Mathlib.Meta.Positivity.int_div_self_pos : ∀ {a : ℤ}, 0 < a → 0 < a / a
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instSub.eq_1 : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} [inst : Sub M],
  Filter.Germ.instSub = { sub := Filter.Germ.map₂ fun x1 x2 => x1 - x2 }
-- Init.Data.Queue
/-- The enqueue list, which stores elements that have just been pushed
(with the most recently enqueued elements at the head).  -/
Std.Queue.eList : {α : Type u} → Std.Queue α → List α
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
IsTranscendenceBasis.sumElim_comp : ∀ {ι : Type u} {ι' : Type u'} {R : Type u_1} {S : Type v} {A : Type w} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : CommRing A] [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A]
  [NoZeroDivisors A] {x : ι → S} {y : ι' → A},
  IsTranscendenceBasis R x → IsTranscendenceBasis S y → IsTranscendenceBasis R (Sum.elim y (⇑(algebraMap S A) ∘ x))
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_pair_sub_right' : ∀ {α : Type u} [inst : Ring α] (x y : α), Ideal.span {x, x - y} = Ideal.span {x, y}
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.opcyclesOpIso_hom_toCycles_op : ∀ {ι : Type u_1} {V : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} V] {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] (K : HomologicalComplex V c) (i : ι) [inst_2 : K.HasHomology i]
  (j : ι), CategoryTheory.CategoryStruct.comp (K.opcyclesOpIso i).hom (K.toCycles j i).op = K.op.fromOpcycles i j
-- Mathlib.Algebra.Group.Hom.Basic
OneHom.mul_apply : ∀ {M : Type u_8} {N : Type u_9} [inst : One M] [inst_1 : MulOneClass N] (f g : OneHom M N) (x : M),
  (f * g) x = f x * g x
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryPseudofunctor.mk'_map₂ : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (S : CategoryTheory.StrictlyUnitaryPseudofunctorCore B C) {a b : B} {f g : a ⟶ b} (a_1 : f ⟶ g),
  (CategoryTheory.StrictlyUnitaryPseudofunctor.mk' S).map₂ a_1 = S.map₂ a_1
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey_eq_getLast_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {he : t ≠ ∅}, t.maxKey he = t.keys.getLast ⋯
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.le_ofAdd_of_toAdd_unzero_le : ∀ {α : Type u_1} [inst : Preorder α] {a : WithZero (Multiplicative α)} {b : α} (ha : a ≠ 0),
  Multiplicative.toAdd (WithZero.unzero ha) ≤ b → a ≤ ↑(Multiplicative.ofAdd b)
-- Mathlib.Data.Matrix.Block
/-- `Matrix.blockDiagonal` as a `RingHom`.  -/
Matrix.blockDiagonalRingHom : (m : Type u_2) →
  (o : Type u_4) →
    (α : Type u_12) →
      [inst : DecidableEq o] →
        [inst_1 : DecidableEq m] →
          [inst_2 : Fintype o] →
            [inst_3 : Fintype m] → [inst_4 : NonAssocSemiring α] → (o → Matrix m m α) →+* Matrix (m × o) (m × o) α
-- Mathlib.Analysis.Meromorphic.Basic
/-- Eta-expanded form of `MeromorphicAt.sub` -/
MeromorphicAt.fun_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : 𝕜} {f g : 𝕜 → E},
  MeromorphicAt f x → MeromorphicAt g x → MeromorphicAt (fun i => f i - g i) x
-- Mathlib.Order.Compare
Ordering.swap_eq_iff_eq_swap : ∀ {o o' : Ordering}, o.swap = o' ↔ o = o'.swap
-- Mathlib.Order.Filter.EventuallyConst
Filter.eventuallyConst_pred' : ∀ {α : Type u_1} {l : Filter α} {p : α → Prop},
  Filter.EventuallyConst p l ↔ (p =ᶠ[l] fun x => False) ∨ p =ᶠ[l] fun x => True
-- Mathlib.Tactic.Nontriviality.Core
/-- Tries to generate a `Nontrivial α` instance using `nontrivial_of_ne` or `nontrivial_of_lt`
and local hypotheses.
 -/
Mathlib.Tactic.Nontriviality.nontrivialityByAssumption : Lean.MVarId → Lean.MetaM Unit
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.galoisConnection_map_comap : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {D : Type u_1} [inst_1 : CategoryTheory.Groupoid D]
  (φ : CategoryTheory.Functor C D) (hφ : Function.Injective φ.obj),
  GaloisConnection (CategoryTheory.Subgroupoid.map φ hφ) (CategoryTheory.Subgroupoid.comap φ)
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.Equiv.refl_apply : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : AddGroup N] [inst_1 : AddGroup E] [inst_2 : AddGroup G]
  (S : AddGroupExtension N E G) (a : E), (AddGroupExtension.Equiv.refl S) a = a
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.mk₀_surjective : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (F : CategoryTheory.ComposableArrows C 0),
  ∃ X, F = CategoryTheory.ComposableArrows.mk₀ X
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
CategoryTheory.Meq.instCoeFunForallToTypeObjOppositeOpY : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {D : Type w} →
        [inst_1 : CategoryTheory.Category.{w', w} D] →
          {FD : D → D → Type u_1} →
            {CD : D → Type t} →
              [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] →
                [inst_3 : CategoryTheory.ConcreteCategory D FD] →
                  {X : C} →
                    (P : CategoryTheory.Functor Cᵒᵖ D) →
                      (S : J.Cover X) →
                        CoeFun (CategoryTheory.Meq P S) fun x =>
                          (I : S.Arrow) → CategoryTheory.ToType (P.obj (Opposite.op I.Y))
-- Mathlib.Order.RelSeries
RelSeries.singleton.eq_1 : ∀ {α : Type u_1} (r : SetRel α α) (a : α), RelSeries.singleton r a = { length := 0, toFun := fun x => a, step := ⋯ }
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.isStrongPrelimit_preBeth : ∀ {o : Ordinal.{u_1}}, (Cardinal.preBeth o).IsStrongPrelimit ↔ Order.IsSuccPrelimit o
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.sum_take_add_sum_drop : ∀ {M : Type u_4} [inst : AddMonoid M] (L : List M) (i : ℕ), (List.take i L).sum + (List.drop i L).sum = L.sum
-- Mathlib.GroupTheory.QuotientGroup.Defs
/-- `QuotientGroup.congr` lifts the isomorphism `e : G ≃ H` to `G ⧸ G' ≃ H ⧸ H'`,
given that `e` maps `G` to `H`.  -/
QuotientGroup.congr : {G : Type u_1} →
  {H : Type u_2} →
    [inst : Group G] →
      [inst_1 : Group H] →
        (G' : Subgroup G) →
          (H' : Subgroup H) →
            [inst_2 : G'.Normal] → [inst_3 : H'.Normal] → (e : G ≃* H) → Subgroup.map (↑e) G' = H' → G ⧸ G' ≃* H ⧸ H'
-- Mathlib.RingTheory.Ideal.Operations
Ideal.dvd_bot : ∀ {R : Type u} [inst : CommSemiring R] {I : Ideal R}, I ∣ ⊥
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.shrinkCoyonedaCorepresentableBy_homEquiv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] (X : Cᵒᵖ)
  {Y : C}, (CategoryTheory.shrinkCoyonedaCorepresentableBy X).homEquiv = CategoryTheory.shrinkCoyonedaObjObjEquiv.symm
-- Mathlib.RingTheory.Ideal.MinimalPrime.Localization
IsLocalization.AtPrime.radical_map_of_mem_minimalPrimes : ∀ {R : Type u_1} [inst : CommSemiring R] (A : Type u_2) [inst_1 : CommSemiring A] [inst_2 : Algebra R A] (q : Ideal R)
  [hqp : q.IsPrime] [IsLocalization.AtPrime A q] (I : Ideal R),
  q ∈ I.minimalPrimes → (Ideal.map (algebraMap R A) I).radical = Ideal.map (algebraMap R A) q
-- Mathlib.Algebra.Group.Indicator
Set.mulIndicator_union_mul_inter_apply : ∀ {α : Type u_1} {M : Type u_4} [inst : MulOneClass M] (f : α → M) (s t : Set α) (a : α),
  (s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a
-- Mathlib.Order.Filter.Pointwise
Filter.Tendsto.neg_neg : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : SubtractionMonoid β]
  [inst_2 : FunLike F α β] [AddMonoidHomClass F α β] (m : F) {f₁ : Filter α} {f₂ : Filter β},
  Filter.Tendsto (⇑m) f₁ f₂ → Filter.Tendsto (⇑m) (-f₁) (-f₂)
-- Mathlib.MeasureTheory.Group.LIntegral
MeasurableEquiv.inv.congr_simp : ∀ (G : Type u_4) [inst : MeasurableSpace G] [inst_1 : InvolutiveInv G] [inst_2 : MeasurableInv G],
  MeasurableEquiv.inv G = MeasurableEquiv.inv G
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.CoreMonoidal.toOplaxMonoidal_δ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} (h : F.CoreMonoidal) (X Y : C),
  CategoryTheory.Functor.OplaxMonoidal.δ F X Y = (h.μIso X Y).inv
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Subgraph.instCoeFunConnectedForallForallReachableElemVertsCoe : {V : Type u} →
  {G : SimpleGraph V} → {H : G.Subgraph} → CoeFun H.Connected fun x => ∀ (u v : ↑H.verts), H.coe.Reachable u v
-- Init.Data.UInt.Basic
/-- Converts `true` to `1` and `false` to `0`.
 -/
Bool.toUInt64 : Bool → UInt64
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- If `f : M →+ N` and `k : M →+ R` are Localization maps for an AddSubmonoid `S`, we get an
isomorphism of `N` and `R`.  -/
AddSubmonoid.LocalizationMap.addEquivOfLocalizations : {M : Type u_1} →
  [inst : AddCommMonoid M] →
    {S : AddSubmonoid M} →
      {N : Type u_2} →
        [inst_1 : AddCommMonoid N] →
          {P : Type u_3} → [inst_2 : AddCommMonoid P] → S.LocalizationMap N → S.LocalizationMap P → N ≃+ P
-- Init.Data.Range.Polymorphic.Iterators
/-- Returns the elements of the given left-open right-unbounded range as an array in ascending order.
 -/
Std.Roi.toArray : {α : Type u} →
  [inst : Std.PRange.UpwardEnumerable α] →
    [Std.PRange.LawfulUpwardEnumerable α] → [Std.Rxi.IsAlwaysFinite α] → Std.Roi α → Array α
-- Mathlib.Data.Set.Disjoint
Set.mem_union_of_disjoint : ∀ {α : Type u_1} {s t : Set α}, Disjoint s t → ∀ {x : α}, x ∈ s ∪ t ↔ Xor (x ∈ s) (x ∈ t)
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.coe_copy : ∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α] (f : CentroidHom α) (f' : α → α) (h : f' = ⇑f),
  ⇑(f.copy f' h) = f'
-- Mathlib.Combinatorics.SimpleGraph.Circulant
SimpleGraph.circulantGraph_adj_translate : ∀ {G : Type u_1} [inst : AddGroup G] {s : Set G} {u v d : G},
  (SimpleGraph.circulantGraph s).Adj (u + d) (v + d) ↔ (SimpleGraph.circulantGraph s).Adj u v
-- Mathlib.Algebra.Group.Defs
AddCommSemigroup.ext : ∀ {G : Type u} {x y : AddCommSemigroup G}, Add.add = Add.add → x = y
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.log_le_self : ∀ (b x : Ordinal.{u_1}), Ordinal.log b x ≤ x
-- Mathlib.Topology.Metrizable.CompletelyMetrizable
TopologicalSpace.IsCompletelyPseudoMetrizableSpace.complete : ∀ {X : Type u_3} {t : TopologicalSpace X} [self : TopologicalSpace.IsCompletelyPseudoMetrizableSpace X],
  ∃ m, PseudoMetricSpace.toUniformSpace.toTopologicalSpace = t ∧ CompleteSpace X
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
/-- The canonical morphism from a presheaf of modules to its associated sheaf.  -/
PresheafOfModules.toSheafify : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} →
        {R : CategoryTheory.Sheaf J RingCat} →
          (α : R₀ ⟶ R.obj) →
            [inst_1 : CategoryTheory.Presheaf.IsLocallyInjective J α] →
              [inst_2 : CategoryTheory.Presheaf.IsLocallySurjective J α] →
                {M₀ : PresheafOfModules R₀} →
                  {A : CategoryTheory.Sheaf J AddCommGrpCat} →
                    (φ : M₀.presheaf ⟶ A.obj) →
                      [inst_3 : CategoryTheory.Presheaf.IsLocallyInjective J φ] →
                        [inst_4 : CategoryTheory.Presheaf.IsLocallySurjective J φ] →
                          M₀ ⟶ (PresheafOfModules.restrictScalars α).obj (PresheafOfModules.sheafify α φ).val
-- Init.Data.UInt.Bitwise
USize.ofNat_or : ∀ (a b : ℕ), USize.ofNat (a ||| b) = USize.ofNat a ||| USize.ofNat b
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.mem_map : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : AddCommGroup V₂]
  [inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] {f : P₁ →ᵃ[k] P₂} {x : P₂} {s : AffineSubspace k P₁},
  x ∈ AffineSubspace.map f s ↔ ∃ y ∈ s, f y = x
-- Mathlib.Tactic.Simps.Basic
/-- A variant of `String.isPrefixOf` that does not consider `toFoo` to be a prefix to `toFoo_1`.  -/
_private.Mathlib.Tactic.Simps.Basic.0.Simps.isPrefixOfAndNotNumber : String → String → Bool
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
/-- An arbitrary choice of initial object, if one exists.
You can use the notation `⊥_ C`.
This object is characterized by having a unique morphism to any object.
 -/
CategoryTheory.Limits.initial : (C : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} C] → [CategoryTheory.Limits.HasInitial C] → C
-- Lean.ResolveName
/-- Retrieve aliases for `a`. If `skipProtected` is `true`, then the resulting list only includes
declarations that are not marked as `protected`.
 -/
Lean.getAliases : Lean.Environment → Lean.Name → Bool → List Lean.Name
-- Init.Data.SInt.Lemmas
Int8.toInt16_toInt32 : ∀ (n : Int8), n.toInt32.toInt16 = n.toInt16
-- Mathlib.Order.WithBot
WithTop.lt_untopA_iff : ∀ {α : Type u_1} {a : α} [inst : LT α] {x : WithTop α} [inst_1 : Nonempty α], x ≠ ⊤ → (a < x.untopA ↔ ↑a < x)
-- Mathlib.Data.ZMod.ValMinAbs
ZMod.valMinAbs_mem_Ioc : ∀ {n : ℕ} [NeZero n] (x : ZMod n), x.valMinAbs * 2 ∈ Set.Ioc (-↑n) ↑n
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalSubgroup.instPartialOrderOpenNormalSubgroup : {G : Type u} → [inst : Group G] → [inst_1 : TopologicalSpace G] → PartialOrder (OpenNormalSubgroup G)
-- Mathlib.Analysis.Convex.Function
ConvexOn.le_right_of_left_le : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : LinearOrder β] [IsOrderedCancelAddMonoid β] [inst_6 : SMul 𝕜 E]
  [inst_7 : Module 𝕜 β] [PosSMulStrictMono 𝕜 β] {s : Set E} {f : E → β},
  ConvexOn 𝕜 s f → ∀ {x y z : E}, x ∈ s → y ∈ s → z ∈ openSegment 𝕜 x y → f x ≤ f z → f z ≤ f y
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubAddAction.addConjMap_ofFixingAddSubgroup.eq_1 : ∀ {M : Type u_1} {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] {s t : Set α} {g : M} (hg : g +ᵥ t = s),
  SubAddAction.addConjMap_ofFixingAddSubgroup hg =
    {
      toFun := fun x =>
        match x with
        | ⟨x, hx⟩ => ⟨g +ᵥ x, ⋯⟩,
      map_vadd' := ⋯ }
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.Section.rightHom_comp_section : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : AddGroup N] [inst_1 : AddGroup E] [inst_2 : AddGroup G]
  {S : AddGroupExtension N E G} (σ : S.Section), ⇑S.rightHom ∘ ⇑σ = id
-- Mathlib.FieldTheory.Relrank
Subfield.relfinrank_comap : ∀ {E : Type v} [inst : Field E] {L : Type w} [inst_1 : Field L] (A : Subfield E) (f : L →+* E) (B : Subfield L),
  (Subfield.comap f A).relfinrank B = A.relfinrank (Subfield.map f B)
-- Lean.Elab.Do.Legacy
/-- Generate `CodeBlock` for `doFor; doElems`
`doFor` is of the form
```
def doForDecl := leading_parser termParser >> " in " >> withForbidden "do" termParser
def doFor := leading_parser "for " >> sepBy1 doForDecl ", " >> "do " >> doSeq
```
 -/
Lean.Elab.Term.Do.ToCodeBlock.doForToCode : Lean.Syntax → List Lean.Syntax → Lean.Elab.Term.Do.ToCodeBlock.M Lean.Elab.Term.Do.CodeBlock
-- Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
differentiableAt_iff_restrictScalars : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedSpace 𝕜' E] [inst_6 : IsScalarTower 𝕜 𝕜' E] {F : Type u_4} [inst_7 : NormedAddCommGroup F]
  [inst_8 : NormedSpace 𝕜 F] [inst_9 : NormedSpace 𝕜' F] [inst_10 : IsScalarTower 𝕜 𝕜' F] {f : E → F} {x : E},
  DifferentiableAt 𝕜 f x → (DifferentiableAt 𝕜' f x ↔ ∃ g', ContinuousLinearMap.restrictScalars 𝕜 g' = fderiv 𝕜 f x)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
/-- Let `x` be a nondegenerate simplex of `Δ[m + 1] ⊗ Δ[n]` which
does not belong to `Λ[m + 1, k.castSucc].unionProd ∂Δ[n]`. This is
the property that `x` is a type (II) simplex for the pairing
`prodStdSimplex.pairingCore` that is constructed below.  -/
SSet.prodStdSimplex.pairingCore.IsType₂ : {m : ℕ} → {k : Fin (m + 1)} → {n : ℕ} → ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N → Prop
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.carrier_eq_coe : ∀ {α : Type u_1} [inst : TopologicalSpace α] (s : TopologicalSpace.Compacts α), s.carrier = ↑s
-- Lean.Data.Lsp.Basic
Lean.Lsp.WorkDoneProgressParams.mk.injEq : ∀ (workDoneToken? workDoneToken?_1 : Option Lean.Lsp.ProgressToken),
  ({ workDoneToken? := workDoneToken? } = { workDoneToken? := workDoneToken?_1 }) = (workDoneToken? = workDoneToken?_1)
-- Mathlib.RingTheory.Polynomial.Pochhammer
descPochhammer_eq_ascPochhammer : ∀ (n : ℕ), descPochhammer ℤ n = (ascPochhammer ℤ n).comp (Polynomial.X - ↑n + 1)
-- Mathlib.Algebra.Homology.ModelCategory.Injective
CochainComplex.Plus.modelCategoryQuillen.isFibrant_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (X : CochainComplex.Plus C), HomotopicalAlgebra.IsFibrant X ↔ ∀ (n : ℤ), CategoryTheory.Injective (X.obj.X n)
-- Mathlib.Topology.Category.TopPair
TopPair.Homotopy.mk.sizeOf_spec : ∀ {X Y : TopPair} {f g : X ⟶ Y} (fst : TopCat.Homotopy (TopPair.Hom.fst f) (TopPair.Hom.fst g))
  (snd : TopCat.Homotopy (TopPair.Hom.snd f) (TopPair.Hom.snd g))
  (w :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight TopPair.map TopCat.I)
          fst.h =
        CategoryTheory.CategoryStruct.comp snd.h TopPair.map)
      TopPair.Homotopy.w._autoParam),
  sizeOf { fst := fst, snd := snd, w := w } = 1 + sizeOf fst + sizeOf snd + sizeOf w
-- Mathlib.Topology.Algebra.UniformConvergence
instZeroUniformOnFun.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [inst : Zero β],
  instZeroUniformOnFun = { zero := instZeroUniformOnFun._aux_1 }
-- Mathlib.Order.Interval.Finset.Basic
Finset.right_mem_Icc : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α], b ∈ Finset.Icc a b ↔ a ≤ b
-- Lean.Meta.IndPredBelow
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.mkBelowInductive.go.match_1.eq_1 : ∀ (motive : Option ℕ → Sort u_1) (val : ℕ) (h_1 : (val : ℕ) → motive (some val)) (h_2 : (x : Option ℕ) → motive x),
  (match some val with
    | some val => h_1 val
    | x => h_2 x) =
    h_1 val
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
/-- Uniqueness property of `BoxIntegral.Prepartition.biUnionIndex`.  -/
BoxIntegral.Prepartition.biUnionIndex_of_mem : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I)
  {πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J},
  J ∈ π → ∀ {J' : BoxIntegral.Box ι}, J' ∈ πi J → π.biUnionIndex πi J' = J
-- Mathlib.Algebra.Notation.Indicator
Set.indicator_support : ∀ {α : Type u_1} {M : Type u_3} [inst : Zero M] {f : α → M}, (Function.support f).indicator f = f
-- Mathlib.NumberTheory.Dioph
Dioph.diophFn_iff_pFun : ∀ {α : Type u} (f : (α → ℕ) → ℕ), Dioph.DiophFn f = Dioph.DiophPFun ↑f
-- Mathlib.Topology.Algebra.Monoid.Defs
ContinuousAt.const_mul : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Mul M] [SeparatelyContinuousMul M] {X : Type u_2}
  [inst_3 : TopologicalSpace X] {f : X → M} {x : X}, ContinuousAt f x → ∀ (b : M), ContinuousAt (fun x => b * f x) x