mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Multilinear.DirectSum
MultilinearMap.directSum_ext_iff : ∀ {R : Type u_1} {ι : Type u_2} {M' : Type u_3} {κ : ι → Type u_4} {M : (i : ι) → κ i → Type u_5}
  [inst : CommSemiring R] [inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)]
  [inst_2 : (i : ι) → (j : κ i) → Module R (M i j)] [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] [Finite ι]
  [inst_6 : (i : ι) → DecidableEq (κ i)] {f g : MultilinearMap R (fun i => DirectSum (κ i) fun j => M i j) M'},
  f = g ↔
    ∀ (p : (i : ι) → κ i),
      (f.compLinearMap fun i => DirectSum.lof R (κ i) (M i) (p i)) =
        g.compLinearMap fun i => DirectSum.lof R (κ i) (M i) (p i)
-- Mathlib.LinearAlgebra.Determinant
LinearMap.detAux_def'' : ∀ {M : Type u_2} [inst : AddCommGroup M] {ι : Type u_4} [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] {A : Type u_5}
  [inst_3 : CommRing A] [inst_4 : Module A M] {ι' : Type u_7} [inst_5 : Fintype ι'] [inst_6 : DecidableEq ι']
  (tb : Trunc (Module.Basis ι A M)) (b' : Module.Basis ι' A M) (f : M →ₗ[A] M),
  (LinearMap.detAux tb) f = ((LinearMap.toMatrix b' b') f).det
-- Mathlib.CategoryTheory.ExtremalEpi
CategoryTheory.ExtremalEpi.toEpi : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X Y : C} {f : X ⟶ Y} [self : CategoryTheory.ExtremalEpi f],
  CategoryTheory.Epi f
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.WalkingReflexivePair.Hom.id : (X : CategoryTheory.Limits.WalkingReflexivePair) → X.Hom X
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.ofCoeff.injEq : ∀ {R : Type u_8} {M : Type u_9} [inst : Semiring R] (coeff coeff_1 : M →₀ R),
  (MonoidAlgebra.ofCoeff coeff = MonoidAlgebra.ofCoeff coeff_1) = (coeff = coeff_1)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
CategoryTheory.Functor.instPreservesZeroMorphismsObjFlip : ∀ {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 C]
  [inst_4 : CategoryTheory.Limits.HasZeroMorphisms E] (F : CategoryTheory.Functor C (CategoryTheory.Functor D E))
  [F.PreservesZeroMorphisms] (Y : D), (F.flip.obj Y).PreservesZeroMorphisms
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instSMulWithZeroOfMulActionHomClassOfZeroHomClass : {R : Type u_1} →
  {ι : 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 : Zero R] →
                      [inst_6 : (i : ι) → Zero (G i)] →
                        [inst_7 : (i : ι) → SMulWithZero R (G i)] →
                          [∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)] →
                            [∀ (i j : ι) (h : i ≤ j), ZeroHomClass (T h) (G i) (G j)] → SMulWithZero R (DirectLimit G f)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVPred.getLsbD.sizeOf_spec : ∀ {w : ℕ} (expr : Std.Tactic.BVDecide.BVExpr w) (idx : ℕ),
  sizeOf (Std.Tactic.BVDecide.BVPred.getLsbD expr idx) = 1 + sizeOf w + sizeOf expr + sizeOf idx
-- Std.Time.Duration
/-- Creates a new `Duration` out of `Nanosecond.Offset`.
 -/
Std.Time.Duration.ofNanoseconds : Std.Time.Nanosecond.Offset → Std.Time.Duration
-- Mathlib.Analysis.Normed.Lp.LpEquiv
coe_lpBCFₗᵢ_symm : ∀ {α : Type u_1} {E : Type u_2} {𝕜 : Type u_5} [inst : TopologicalSpace α] [inst_1 : DiscreteTopology α]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E]
  (f : BoundedContinuousFunction α E), ↑((lpBCFₗᵢ E 𝕜).symm f) = ⇑f
-- Mathlib.Analysis.Normed.Lp.PiLp
/-- A copy of a Pi type, on which we will put the `L^p` distance. Since the Pi type itself is
already endowed with the `L^∞` distance, we need the type synonym to avoid confusing typeclass
resolution. Also, we let it depend on `p`, to get a whole family of type on which we can put
different distances.  -/
PiLp : ENNReal → {ι : Type u_1} → (ι → Type u_2) → Type (max u_1 u_2)
-- Init.Data.Array.Lemmas
Array.all_eq_false : ∀ {α : Type u_1} {p : α → Bool} {as : Array α}, as.all p = false ↔ ∃ i, ∃ (x : i < as.size), ¬p as[i] = true
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
CauchySeq.const_add : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Type u_3}
  [inst_3 : Preorder ι] {u : ι → α} {x : α}, CauchySeq u → CauchySeq fun n => x + u n
-- Std.Data.DHashMap.Internal.AssocList.Basic
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.AssocList.getKey? : {α : Type u} → {β : α → Type v} → [BEq α] → α → Std.DHashMap.Internal.AssocList α β → Option α
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey!_eq_default : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.isEmpty = true → t.maxKey! = default
-- Mathlib.RingTheory.Localization.Cardinality
IsLocalization.lift_cardinalMk_le : ∀ {R : Type u} [inst : CommSemiring R] {L : Type v} [inst_1 : CommSemiring L] [inst_2 : Algebra R L] (S : Submonoid R)
  [IsLocalization S L], Cardinal.lift.{u, v} (Cardinal.mk L) ≤ Cardinal.lift.{v, u} (Cardinal.mk R)
-- Mathlib.Algebra.Order.Group.PosPart
posPart_neg : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : SubNegMonoid α] (a : α), (-a)⁺ = a⁻
-- Mathlib.Geometry.Convex.ConvexSpace.Module
/-- Eta-expanded form of `Convexity.IsAffineMap.neg` -/
Convexity.IsAffineMap.fun_neg : ∀ {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : AddCommGroup N]
  [inst_6 : Module R N] [inst_7 : Convexity.ConvexSpace R M] [Convexity.IsModuleConvexSpace R M]
  [inst_9 : Convexity.ConvexSpace R N] [Convexity.IsModuleConvexSpace R N] {f : M → N},
  Convexity.IsAffineMap R f → Convexity.IsAffineMap R fun i => -f i
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Class
Std.Tactic.BVDecide.LRAT.Internal.Formula.ratAdd_result : ∀ {α : outParam (Type u)} {β : outParam (Type v)} {inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β} {σ : Type w}
  {inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ} [self : Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ]
  (f : σ) (c : β) (p : Std.Sat.Literal α) (rupHints : Array ℕ) (ratHints : Array (ℕ × Array ℕ)) (f' : σ),
  Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRatAdd f →
    p ∈ Std.Tactic.BVDecide.LRAT.Internal.Clause.toList c →
      Std.Tactic.BVDecide.LRAT.Internal.Formula.performRatAdd f c p rupHints ratHints = (f', true) →
        f' = Std.Tactic.BVDecide.LRAT.Internal.Formula.insert f c
-- Mathlib.Algebra.Category.Ring.Adjunctions
CommRingCat.coyoneda_obj_map : ∀ (n : Type vᵒᵖ) {R S : CommRingCat} (φ : R ⟶ S),
  (CommRingCat.coyoneda.obj n).map φ =
    CommRingCat.ofHom (RingHom.pi fun x => (CommRingCat.Hom.hom φ).comp (Pi.evalRingHom (fun a => ↑R) x))
-- Mathlib.Algebra.Category.Grp.CartesianMonoidal
/-- We choose `AddGrpCat.of (G × H)` as the product of `G` and `H` and `AddGrpCat.of PUnit` as
the terminal object.  -/
AddGrpCat.cartesianMonoidalCategoryAddGrp : CategoryTheory.CartesianMonoidalCategory AddGrpCat
-- Mathlib.Algebra.Order.Monoid.Unbundled.Units
/-- **Alias** of the forward direction of `Units.inv_mul_le_iff`. -/
Units.le_mul_of_inv_mul_le : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : LE M] [MulLeftMono M] (u : Mˣ) {a b : M}, ↑u⁻¹ * a ≤ b → a ≤ ↑u * b
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubmonoid.addUnitsEquivAddUnitsType.eq_1 : ∀ {M : Type u_1} [inst : AddMonoid M] (S : AddSubmonoid M),
  S.addUnitsEquivAddUnitsType =
    {
      toFun := fun x =>
        match x with
        | ⟨val, h⟩ =>
          { val := ⟨(AddUnits.coeHom M) val, ⋯⟩, neg := ⟨(AddUnits.coeHom M) (-val), ⋯⟩, val_neg := ⋯, neg_val := ⋯ },
      invFun := fun x => ⟨{ val := ↑↑x, neg := ↑↑(-x), val_neg := ⋯, neg_val := ⋯ }, ⋯⟩, left_inv := ⋯, right_inv := ⋯,
      map_add' := ⋯ }
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Path.mk'_mem_edges_singleton : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (h : G.Adj u v), s(u, v) ∈ (↑(SimpleGraph.Path.singleton h)).edges
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Module.End.exists_ker_pow_eq_ker_pow_succ : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [FiniteDimensional K V] (f : Module.End K V),
  ∃ k ≤ Module.finrank K V, LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
-- Mathlib.Analysis.InnerProductSpace.NormPow
hasDerivAt_norm_rpow : ∀ (x : ℝ) {p : ℝ}, 1 < p → HasDerivAt (fun x => ‖x‖ ^ p) (p * ‖x‖ ^ (p - 2) * x) x
-- Mathlib.Data.Int.Interval
Finset.Ioc_succ_succ : ∀ (m n : ℕ), Finset.Ioc (-(↑m + 1)) (↑n + 1) = Finset.Ioc (-↑m) ↑n ∪ {-↑m, ↑n + 1}
-- Mathlib.Combinatorics.Graph.Simple
/-- The isomorphism between `toSimpleGraph (ofSimpleGraph G)` and `G`.  -/
Graph.toSimpleGraphOfSimpleGraphIso : {α : Type u_1} → (G : SimpleGraph α) → (Graph.ofSimpleGraph G).toSimpleGraph ≃g G
-- Mathlib.Tactic.Linter.TacticDocumentation
/-- Check that all tactics available in Mathlib have a docstring.  -/
tacticDocs : Batteries.Tactic.Lint.Linter
-- Mathlib.Data.UInt
/-- Is this an uppercase ASCII letter?  -/
UInt8.isASCIIUpper : UInt8 → Bool
-- Init.Data.UInt.Lemmas
UInt32.toNat.inj : ∀ {a b : UInt32}, a.toNat = b.toNat → a = b
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Embedding.subtype_substructureEquivMap : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f : L.Embedding M N) (s : L.Substructure M),
  (FirstOrder.Language.Substructure.map f.toHom s).subtype.comp (f.substructureEquivMap s).toEmbedding =
    f.comp s.subtype
-- Mathlib.Algebra.Homology.BifunctorShift
/-- Auxiliary definition for `mapBifunctorShift₂Iso`.  -/
CochainComplex.mapBifunctorHomologicalComplexShift₂Iso : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} D] →
            [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] →
              [inst_4 : CategoryTheory.Preadditive C₂] →
                [inst_5 : CategoryTheory.Preadditive D] →
                  (K₁ : CochainComplex C₁ ℤ) →
                    (K₂ : CochainComplex C₂ ℤ) →
                      (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) →
                        [inst_6 : F.PreservesZeroMorphisms] →
                          [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive] →
                            (y : ℤ) →
                              ((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj
                                  ((CategoryTheory.shiftFunctor (HomologicalComplex C₂ (ComplexShape.up ℤ)) y).obj K₂) ≅
                                (HomologicalComplex₂.shiftFunctor₂ D y).obj
                                  (((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj
                                        K₁).obj
                                    K₂)
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.restrict_map : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [inst : MeasurableSpace β] {M : Type u_3}
  [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M] (v : MeasureTheory.VectorMeasure α M) {f : α → β},
  Measurable f → ∀ {s : Set β}, MeasurableSet s → (v.map f).restrict s = (v.restrict (f ⁻¹' s)).map f
-- Mathlib.Analysis.Normed.Group.Basic
norm_zpow_abs : ∀ {E : Type u_5} [inst : SeminormedGroup E] (a : E) (n : ℤ), ‖a ^ |n|‖ = ‖a ^ n‖
-- Mathlib.Order.Hom.Basic
/-- Composition of two order isomorphisms is an order isomorphism.  -/
OrderIso.trans : {α : Type u_2} →
  {β : Type u_3} → {γ : Type u_4} → [inst : LE α] → [inst_1 : LE β] → [inst_2 : LE γ] → α ≃o β → β ≃o γ → α ≃o γ
-- Mathlib.Analysis.Calculus.FDeriv.Prod
HasFDerivAt.prodMk : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f₁ : E → F} {f₁' : E →L[𝕜] F} {x : E} {f₂ : E → G}
  {f₂' : E →L[𝕜] G}, HasFDerivAt f₁ f₁' x → HasFDerivAt f₂ f₂' x → HasFDerivAt (fun x => (f₁ x, f₂ x)) (f₁'.prod f₂') x
-- Batteries.Data.Fin.Coding
/-- Decode `Option (Fin n)` from `Fin (n+1)`.  -/
Fin.decodeOption : {n : ℕ} → Fin (n + 1) → Option (Fin n)
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
_private.Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass.0.PeriodPair.relation_eq_zero : ∀ (L : PeriodPair), PeriodPair.relation✝ L = 0
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
ContMDiffOn.continuousOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M}
  {n : WithTop ℕ∞}, ContMDiffOn I I' n f s → ContinuousOn f s
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cocone.toOver_ι_app : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) (j : J),
  c.toOver.ι.app j = CategoryTheory.Over.homMk (c.ι.app j) ⋯
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrix'_id : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_5} [inst_1 : DecidableEq n] [inst_2 : Fintype n],
  LinearMap.toMatrix' LinearMap.id = 1
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.exp_neg : ∀ {G : Type u_5} [inst : AddGroup G] (a : G), WithZero.exp (-a) = (WithZero.exp a)⁻¹
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- Given any other limit cone for `F`, the chosen `limit F` is isomorphic to the cone point.  -/
CategoryTheory.Limits.limit.isoLimitCone : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor J C} →
          [inst_2 : CategoryTheory.Limits.HasLimit F] →
            (t : CategoryTheory.Limits.LimitCone F) → CategoryTheory.Limits.limit F ≅ t.cone.pt
-- Init.Data.List.SplitOn.Lemmas
/-- If no element satisfies `p` in the list `xs`, then `xs.splitOnP p = [xs]`  -/
List.splitOn_eq_singleton_of_beq_eq_false : ∀ {α : Type u_1} {xs : List α} [inst : BEq α] {a : α}, (∀ x ∈ xs, (x == a) = false) → List.splitOn a xs = [xs]
-- Mathlib.Data.List.Cycle
Cycle.nodup_reverse_iff : ∀ {α : Type u_1} {s : Cycle α}, s.reverse.Nodup ↔ s.Nodup
-- Mathlib.MeasureTheory.OuterMeasure.Induced
MeasureTheory.extend_iUnion_le_tsum_nat : ∀ {α : Type u_1} [inst : MeasurableSpace α] {m : (s : Set α) → MeasurableSet s → ENNReal},
  m ∅ ⋯ = 0 →
    (∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
        Pairwise (Function.onFun Disjoint f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯) →
      ∀ (s : ℕ → Set α), MeasureTheory.extend m (⋃ i, s i) ≤ ∑' (i : ℕ), MeasureTheory.extend m (s i)
-- Mathlib.Order.Bounds.Defs
/-- `a` is a least element of a set `s`; for a partial order, it is unique if exists.  -/
IsLeast : {α : Type u_1} → [LE α] → Set α → α → Prop
-- Mathlib.Analysis.Normed.Group.Basic
enorm_inv' : ∀ {E : Type u_5} [inst : SeminormedGroup E] (a : E), ‖a⁻¹‖ₑ = ‖a‖ₑ
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
Ideal.absNorm_mem : ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : IsDedekindDomain S] [inst_2 : Module.Free ℤ S] (I : Ideal S),
  ↑(Ideal.absNorm I) ∈ I
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.forget_ε : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.Comon.forget C) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.contains_congr : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k k' : α},
  cmp k k' = Ordering.eq → t.contains k = t.contains k'
-- Mathlib.Data.Fin.FlagRange
/-- Let `f : Fin (n + 1) → α` be an `(n + 1)`-tuple `(f₀, …, fₙ)` such that
- `f₀ = ⊥` and `fₙ = ⊤`;
- `fₖ₊₁` weakly covers `fₖ` for all `0 ≤ k < n`;
  this means that `fₖ ≤ fₖ₊₁` and there is no `c` such that `fₖ<c<fₖ₊₁`.

Then the range of `f` is a `Flag α`.  -/
Flag.rangeFin : {α : Type u_1} →
  [inst : PartialOrder α] →
    [inst_1 : BoundedOrder α] →
      {n : ℕ} → (f : Fin (n + 1) → α) → f 0 = ⊥ → f (Fin.last n) = ⊤ → (∀ (k : Fin n), f k.castSucc ⩿ f k.succ) → Flag α
-- Mathlib.Data.Seq.Basic
/-- The `return` operator for the `Seq1` monad,
which produces a singleton sequence.  -/
Stream'.Seq1.ret : {α : Type u} → α → Stream'.Seq1 α
-- Mathlib.Analysis.Calculus.Deriv.Prod
hasStrictDerivAt_finCons : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {n : ℕ} {F' : Fin n.succ → Type u_1}
  [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (F' i)] [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
  {φ : 𝕜 → F' 0} {φs : 𝕜 → (i : Fin n) → F' i.succ} {φ' : (i : Fin n.succ) → F' i},
  HasStrictDerivAt (fun x => Fin.cons (φ x) (φs x)) φ' x ↔
    HasStrictDerivAt φ (φ' 0) x ∧ HasStrictDerivAt φs (fun i => φ' i.succ) x
-- Mathlib.Data.Fintype.Quotient
Quotient.liftOn.congr_simp : ∀ {α : Sort u} {β : Sort v} {s : Setoid α} (q q_1 : Quotient s),
  q = q_1 → ∀ (f f_1 : α → β) (e_f : f = f_1) (c : ∀ (a b : α), a ≈ b → f a = f b), q.liftOn f c = q_1.liftOn f_1 ⋯
-- Mathlib.RingTheory.Jacobson.Radical
Ring.jacobson_le_of_eq_bot : ∀ {R : Type u_1} [inst : Ring R] {I : Ideal R} [inst_1 : I.IsTwoSided], Ring.jacobson (R ⧸ I) = ⊥ → Ring.jacobson R ≤ I
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
/-- A morphism of locally ringed spaces `f : X ⟶ Y` induces
a local ring homomorphism from `Y.stalk (f x)` to `X.stalk x` for any `x : X`.
 -/
AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap : {X Y : AlgebraicGeometry.LocallyRingedSpace} →
  (f : X ⟶ Y) →
    (x : ↑X.toTopCat) → Y.presheaf.stalk ((CategoryTheory.ConcreteCategory.hom f.base) x) ⟶ X.presheaf.stalk x
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.proj_continuous : ∀ {X : Type u_2} [inst : TopologicalSpace X] (S : DiscreteQuotient X), Continuous S.proj
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RciSlice.instToIterator : {α : Type u_1} →
  [inst : Ord α] →
    Std.ToIterator (Std.Slice (Std.DTreeMap.Internal.Unit.RciSliceData α)) Id
      (Std.Iterators.Types.Map (Std.DTreeMap.Internal.Zipper α fun x => Unit) Id Id (fun ⦃x⦄ => monadLift) fun b =>
        pure b.fst)
      α
-- Mathlib.Data.Sum.Interval
Sum.Lex.instLocallyFiniteOrderBot : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        [Fintype α] → [LocallyFiniteOrderBot α] → [LocallyFiniteOrderBot β] → LocallyFiniteOrderBot (α ⊕ₗ β)
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.shouldGeneralizeTarget : Lean.Expr → Lean.MetaM Bool
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.getThenInsertIfNew?.match_1.eq_1 : ∀ {α : Type u_3} {β : α → Type u_1} (k : α) (motive : Option (β k) → Sort u_2) (h_1 : Unit → motive none)
  (h_2 : (b : β k) → motive (some b)),
  (match none with
    | none => h_1 ()
    | some b => h_2 b) =
    h_1 ()
-- Mathlib.RingTheory.Polynomial.Vieta
Finset.prod_X_add_C_coeff : ∀ {R : Type u_1} [inst : CommSemiring R] {σ : Type u_2} (s : Finset σ) (r : σ → R) {k : ℕ},
  k ≤ s.card →
    (∏ i ∈ s, (Polynomial.X + Polynomial.C (r i))).coeff k = ∑ t ∈ Finset.powersetCard (s.card - k) s, ∏ i ∈ t, r i
-- Lean.Expr
/-- If `f` is a lambda expression, than "beta-reduce" it using `revArgs`.
This function is often used with `getAppRev` or `withAppRev`.
Examples:
- `betaRev (fun x y => t x y) #[]` ==> `fun x y => t x y`
- `betaRev (fun x y => t x y) #[a]` ==> `fun y => t a y`
- `betaRev (fun x y => t x y) #[a, b]` ==> `t b a`
- `betaRev (fun x y => t x y) #[a, b, c, d]` ==> `t d c b a`
Suppose `t` is `(fun x y => t x y) a b c d`, then
`args := t.getAppRev` is `#[d, c, b, a]`,
and `betaRev (fun x y => t x y) #[d, c, b, a]` is `t a b c d`.

If `useZeta` is true, the function also performs zeta-reduction (reduction of let binders) to create further
opportunities for beta reduction.
 -/
Lean.Expr.betaRev : Lean.Expr → Array Lean.Expr → optParam Bool false → optParam Bool false → Lean.Expr
-- Mathlib.RingTheory.Radical.NatInt
Nat.radical_pos : ∀ (n : ℕ), 0 < UniqueFactorizationMonoid.radical n
-- Mathlib.RepresentationTheory.Rep.Res
/-- Given a normal subgroup `S ≤ G`, a `G`-representation `ρ` which is trivial on `S` factors
through `G ⧸ S`.  -/
Rep.ofQuotient : {k : Type u} →
  [inst : Semiring k] →
    {G : Type v} →
      [inst_1 : Group G] →
        (A : Rep.{u_1, u, v} k G) →
          (S : Subgroup G) →
            [inst_2 : S.Normal] → [Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)] → Rep.{u_1, u, v} k (G ⧸ S)
-- Mathlib.Algebra.Symmetrized
SymAlg.instOne : {α : Type u_1} → [One α] → One αˢʸᵐ
-- Mathlib.Geometry.Manifold.PartitionOfUnity
/-- All the bump functions in the covering are centered at points in `s`.  -/
SmoothBumpCovering.c_mem' : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] [inst_5 : FiniteDimensional ℝ E] {s : optParam (Set M) Set.univ}
  (self : SmoothBumpCovering ι I M s) (i : ι), self.c i ∈ s
-- Mathlib.Order.Defs.PartialOrder
lt_of_le_of_ne : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a ≤ b → a ≠ b → a < b
-- Mathlib.Algebra.Group.Equiv.Basic
AddMonoidHomClass.toAddMonoidHom.congr_simp : ∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : AddZero M] [inst_1 : AddZero N] [inst_2 : FunLike F M N]
  [inst_3 : AddMonoidHomClass F M N] (f f_1 : F), f = f_1 → ↑f = ↑f_1
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getD_filterMap : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} {γ : α → Type w}
  [inst : LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {k : α} {fallback : γ k},
  (Std.ExtDHashMap.filterMap f m).getD k fallback = ((m.get? k).bind (f k)).getD fallback
-- Mathlib.Geometry.Convex.Cone.Dual
PointedCone.dual_univ : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {N : Type u_3} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  {p : M →ₗ[R] N →ₗ[R] R}, Function.Injective ⇑p.flip → PointedCone.dual p Set.univ = 0
-- Mathlib.Data.DFinsupp.Ext
/-- If two additive homomorphisms from `Π₀ i, β i` are equal on each `single a b`, then
they are equal.  -/
DFinsupp.addHom_ext : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddZeroClass (β i)] {γ : Type w}
  [inst_2 : AddZeroClass γ] ⦃f g : (Π₀ (i : ι), β i) →+ γ⦄,
  (∀ (i : ι) (y : β i), (f fun₀ | i => y) = g fun₀ | i => y) → f = g
-- Mathlib.Algebra.Tropical.BigOperators
Multiset.untrop_prod : ∀ {R : Type u_1} [inst : AddCommMonoid R] (s : Multiset (Tropical R)),
  Tropical.untrop s.prod = (Multiset.map Tropical.untrop s).sum