mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Fourier.Notation
ContinuousFourierInv.mk : ∀ {E : Type u_5} {F : outParam (Type u_6)} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace F]
  [inst_2 : FourierTransformInv E F], Continuous FourierTransformInv.fourierInv → ContinuousFourierInv E F
-- Lean.Meta.Match.Basic
Lean.Meta.Match.instantiateAltLHSMVars : Lean.Meta.Match.AltLHS → Lean.MetaM Lean.Meta.Match.AltLHS
-- Std.Sat.AIG.CNF
/-- The CNF within the state is sat.
 -/
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.State.Sat : {aig : Std.Sat.AIG ℕ} → (ℕ → Bool) → Std.Sat.AIG.toCNF.State✝ aig → Prop
-- Mathlib.Analysis.Complex.ReImTopology
/-- **Alias** of `Complex.frontier_setOfPred_le_re_and_le_im`. -/
Complex.frontier_setOf_le_re_and_le_im : ∀ (a b : ℝ), frontier {z | a ≤ z.re ∧ b ≤ z.im} = {z | a ≤ z.re ∧ z.im = b ∨ z.re = a ∧ b ≤ z.im}
-- Mathlib.Topology.Constructible
/-- [Stacks Tag 0069](https://stacks.math.columbia.edu/tag/0069) (Iff form of (2). Note that Stacks doesn't define quasi-separated spaces.) -/
QuasiSeparatedSpace.isRetrocompact_iff_isCompact : ∀ {X : Type u_2} [inst : TopologicalSpace X] {U : Set X} [CompactSpace X] [QuasiSeparatedSpace X],
  IsOpen U → (IsRetrocompact U ↔ IsCompact U)
-- Init.Data.Array.Find
_private.Init.Data.Array.Find.0.Option.pmap_or.match_1.eq_1 : ∀ {α : Type u_1} {p : α → Prop} {o' : Option α}
  (motive : (o : Option α) → {h : ∀ (a : α), o.or o' = some a → p a} → Sort u_2)
  (h : ∀ (a : α), none.or o' = some a → p a) (h_1 : (h : ∀ (a : α), none.or o' = some a → p a) → motive none)
  (h_2 : (a : α) → (h : ∀ (a_1 : α), (some a).or o' = some a_1 → p a_1) → motive (some a)),
  (match none, h with
    | none, h => h_1 h
    | some a, h => h_2 a h) =
    h_1 h
-- Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass
MeasureTheory.Measure.restrict.instNullSingletonClass : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NullSingletonClass μ]
  (s : Set α), MeasureTheory.NullSingletonClass (μ.restrict s)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry?_insertEntryIfNew : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k},
  Std.Internal.List.getEntry? a (Std.Internal.List.insertEntryIfNew k v l) =
    if (k == a && !Std.Internal.List.containsKey k l) = true then some ⟨k, v⟩ else Std.Internal.List.getEntry? a l
-- Mathlib.Analysis.Normed.Group.Real
Real.enorm_eq_ofReal_abs : ∀ (r : ℝ), ‖r‖ₑ = ENNReal.ofReal |r|
-- Mathlib.Topology.UniformSpace.Basic
uniformity_additive : ∀ {α : Type ua} [inst : UniformSpace α],
  uniformity (Additive α) = Filter.map (Prod.map ⇑Additive.ofMul ⇑Additive.ofMul) (uniformity α)
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
linearIndepOn_iff_linearCombinationOn : ∀ {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] {v : ι → M}, LinearIndepOn R v s ↔ (Finsupp.linearCombinationOn ι M R v s).ker = ⊥
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- If `s` is a measurable set in a measurable space, that space is equivalent
to the sum of `s` and `sᶜ`.  -/
MeasurableEquiv.sumCompl : {α : Type u_1} →
  [inst : MeasurableSpace α] → {s : Set α} → [DecidablePred fun x => x ∈ s] → MeasurableSet s → ↑s ⊕ ↑sᶜ ≃ᵐ α
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.Expr.denoteN.match_1.congr_eq_2 : ∀ (motive : Lean.Grind.Linarith.Expr → Sort u_1) (x : Lean.Grind.Linarith.Expr)
  (h_1 : (a b : Lean.Grind.Linarith.Expr) → motive (a.sub b)) (h_2 : (a : Lean.Grind.Linarith.Expr) → motive a.neg)
  (h_3 : (k : ℤ) → (a : Lean.Grind.Linarith.Expr) → motive (Lean.Grind.Linarith.Expr.intMul k a))
  (h_4 : Unit → motive Lean.Grind.Linarith.Expr.zero)
  (h_5 : (v : Lean.Grind.Linarith.Var) → motive (Lean.Grind.Linarith.Expr.var v))
  (h_6 : (a b : Lean.Grind.Linarith.Expr) → motive (a.add b))
  (h_7 : (k : ℕ) → (a : Lean.Grind.Linarith.Expr) → motive (Lean.Grind.Linarith.Expr.natMul k a))
  (a : Lean.Grind.Linarith.Expr),
  x = a.neg →
    (match x with
      | a.sub b => h_1 a b
      | a.neg => h_2 a
      | Lean.Grind.Linarith.Expr.intMul k a => h_3 k a
      | Lean.Grind.Linarith.Expr.zero => h_4 ()
      | Lean.Grind.Linarith.Expr.var v => h_5 v
      | a.add b => h_6 a b
      | Lean.Grind.Linarith.Expr.natMul k a => h_7 k a) ≍
      h_2 a
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.opLaxMonoidalPi : {I : Type w₁} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] →
        {D : I → Type u₂} →
          [inst_2 : (i : I) → CategoryTheory.Category.{v₂, u₂} (D i)] →
            [inst_3 : (i : I) → CategoryTheory.MonoidalCategory (D i)] →
              (F : (i : I) → CategoryTheory.Functor (D i) (C i)) →
                [(i : I) → (F i).OplaxMonoidal] → (CategoryTheory.Functor.pi F).OplaxMonoidal
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.HomologyData.exact_iff' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.HomologyData), S.Exact ↔ CategoryTheory.Limits.IsZero h.right.H
-- Mathlib.Algebra.Ring.Opposite
AddOpposite.instRing : {R : Type u_1} → [Ring R] → Ring Rᵃᵒᵖ
-- Mathlib.Data.Num.Basic
PosNum.brecOn.eq : ∀ {motive : PosNum → Sort u} (t : PosNum) (F_1 : (t : PosNum) → PosNum.below t → motive t),
  PosNum.brecOn t F_1 = F_1 t (PosNum.brecOn.go t F_1).2
-- Mathlib.Data.List.Forall2
List.sublistForall₂_iff : ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {l₁ : List α} {l₂ : List β},
  List.SublistForall₂ R l₁ l₂ ↔ ∃ l, List.Forall₂ R l₁ l ∧ l.Sublist l₂
-- Lean.Elab.Term.TermElabM
/-- State of the `TacticM` monad.
 -/
Lean.Elab.Tactic.State : Type
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- The `v`-adic absolute value is nonarchimedean  -/
IsDedekindDomain.HeightOneSpectrum.isNonarchimedean_intAdicAbv : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
  {b : NNReal} (hb : 1 < b), IsNonarchimedean ⇑(v.intAdicAbv hb)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.insertManyIfNewUnit_list_eq_foldl : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α Unit cmp} [inst : Std.TransCmp cmp] {l : List α},
  t.insertManyIfNewUnit l = List.foldl (fun acc a => acc.insertIfNew a ()) t l
-- Lean.Parser.Command
Lean.Parser.Command.derivingClasses.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonSymbolTag : Lean.FromJson Lean.Lsp.SymbolTag
-- Mathlib.Order.Filter.IsBounded
Antitone.isBoundedUnder_ge_comp_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Nonempty β] [inst : LinearOrder β] [inst_1 : Preorder γ] [NoMinOrder γ]
  {g : β → γ} {f : α → β} {l : Filter α},
  Antitone g →
    Filter.Tendsto g Filter.atTop Filter.atBot →
      (Filter.IsBoundedUnder (fun x1 x2 => x2 ≤ x1) l (g ∘ f) ↔ Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l f)
-- Mathlib.CategoryTheory.Sites.Descent.Precoverage
CategoryTheory.Precoverage.toPretopology.congr_simp : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  (J J_1 : CategoryTheory.Precoverage C) (e_J : J = J_1) [inst_2 : J.HasIsos] [inst_3 : J.IsStableUnderBaseChange]
  [inst_4 : J.IsStableUnderComposition],
  CategoryTheory.Precoverage.toPretopology C J = CategoryTheory.Precoverage.toPretopology C J_1
-- Mathlib.RingTheory.HahnSeries.Addition
/-- `ofFinsupp` as a linear map.  -/
HahnSeries.ofFinsuppLinearMap : {Γ : Type u_1} →
  (R : Type u_3) →
    {V : Type u_6} →
      [inst : PartialOrder Γ] →
        [inst_1 : Semiring R] → [inst_2 : AddCommMonoid V] → [inst_3 : Module R V] → (Γ →₀ V) →ₗ[R] HahnSeries Γ V
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.denoteAsIntModule : {α : Type u_1} → [Lean.Grind.CommRing α] → Lean.Grind.CommRing.Context α → Lean.Grind.CommRing.Mon → α
-- Mathlib.RingTheory.Frobenius
IsArithFrobAt.arithFrobAt : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (G : Type u_3)
  [inst_3 : Group G] [inst_4 : MulSemiringAction G S] [inst_5 : SMulCommClass G R S] (Q : Ideal S) [inst_6 : Finite G]
  [inst_7 : Algebra.IsInvariant R S G] [inst_8 : Q.IsPrime] [inst_9 : Finite (S ⧸ Q)],
  IsArithFrobAt R (arithFrobAt R G Q) Q
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.top_prod_top : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S], ⊤.prod ⊤ = ⊤
-- Mathlib.MeasureTheory.Function.LpSpace.Complete
_private.Mathlib.MeasureTheory.Function.LpSpace.Complete.0.MeasureTheory.Lp.tsum_enorm_sub_ae_lt_top : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_3} [inst : NormedAddCommGroup E]
  {f : ℕ → α → E},
  (∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ) →
    ∀ {p : ℝ},
      1 ≤ p →
        ∀ {B : ℕ → ENNReal},
          ∑' (i : ℕ), B i ≠ ⊤ →
            (∫⁻ (a : α), (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i →
              ∀ᵐ (x : α) ∂μ, ∑' (i : ℕ), ‖f (i + 1) x - f i x‖ₑ < ⊤
-- Mathlib.Topology.Algebra.InfiniteSum.Ring
summable_mul_left_iff : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : DivisionSemiring α] [inst_1 : TopologicalSpace α]
  [IsTopologicalSemiring α] {f : ι → α} {a : α}, a ≠ 0 → (Summable (fun i => a * f i) L ↔ Summable f L)
-- Batteries.Recycling.RBTree.Basic
/-- `O(1)` amortized, `O(log n)` worst case: Get the next element from the stream.  -/
RBTree.RBMap.Keys.Stream.next? : {α : Type u} → {β : Type v} → RBTree.RBMap.Keys.Stream α β → Option (α × RBTree.RBMap.Keys.Stream α β)
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop.0.List.forIn'_eq_foldlM.match_1.eq_2 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.yield b))
  (h_2 : (b : β) → motive (ForInStep.done b)),
  (match ForInStep.done b with
    | ForInStep.yield b => h_1 b
    | ForInStep.done b => h_2 b) =
    h_2 b
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
SSet.Edge.CompStruct.idComp_simplex : ∀ {X : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 0 })} (e : SSet.Edge x₀ x₁),
  (SSet.Edge.CompStruct.idComp e).simplex =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ X 0)) e.edge
-- Mathlib.Topology.Compactness.Paracompact
/-- A compact space is paracompact.  -/
paracompact_of_compact : ∀ {X : Type v} [inst : TopologicalSpace X] [CompactSpace X], ParacompactSpace X
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.instAddMonoidHomClass : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : AddZeroClass α]
  [inst_3 : AddZeroClass β], AddMonoidHomClass (α →+o β) α β
-- Mathlib.Computability.TuringMachine.Config
_private.Mathlib.Computability.TuringMachine.Config.0.Turing.ToPartrec.Code.eval.match_1.eq_3 : ∀ (motive : Turing.ToPartrec.Code → Sort u_1) (h_1 : Unit → motive Turing.ToPartrec.Code.zero')
  (h_2 : Unit → motive Turing.ToPartrec.Code.succ) (h_3 : Unit → motive Turing.ToPartrec.Code.tail)
  (h_4 : (f fs : Turing.ToPartrec.Code) → motive (f.cons fs)) (h_5 : (f g : Turing.ToPartrec.Code) → motive (f.comp g))
  (h_6 : (f g : Turing.ToPartrec.Code) → motive (f.case g)) (h_7 : (f : Turing.ToPartrec.Code) → motive f.fix),
  (match Turing.ToPartrec.Code.tail with
    | Turing.ToPartrec.Code.zero' => h_1 ()
    | Turing.ToPartrec.Code.succ => h_2 ()
    | Turing.ToPartrec.Code.tail => h_3 ()
    | f.cons fs => h_4 f fs
    | f.comp g => h_5 f g
    | f.case g => h_6 f g
    | f.fix => h_7 f) =
    h_3 ()
-- Mathlib.Algebra.Homology.Embedding.Restriction
/-- Given `e : ComplexShape.Embedding c c'`, this is the restriction
functor `HomologicalComplex C c' ⥤ HomologicalComplex C c`.  -/
ComplexShape.Embedding.restrictionFunctor : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        (e : c.Embedding c') →
          (C : Type u_3) →
            [inst : CategoryTheory.Category.{v_1, u_3} C] →
              [e.IsRelIff] →
                [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
                  CategoryTheory.Functor (HomologicalComplex C c') (HomologicalComplex C c)
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
CategoryTheory.IsHomLift.comp_eqToHom_lift_iff : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a' a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) (h : a' = a),
  p.IsHomLift f (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h) φ) ↔ p.IsHomLift f φ
-- Mathlib.Topology.MetricSpace.Ultra.Basic
IsUltrametricDist.isClopen_sphere : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] [IsUltrametricDist X] (x : X) {r : ℝ},
  r ≠ 0 → IsClopen (Metric.sphere x r)
-- Init.Data.Iterators.Lemmas.Consumers.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Loop.0.Std.Iter.forIn'_eq_match_step.match_1.eq_2 : ∀ {γ : Type u_1} (motive : ForInStep γ → Sort u_2) (c : γ) (h_1 : (c : γ) → motive (ForInStep.yield c))
  (h_2 : (c : γ) → motive (ForInStep.done c)),
  (match ForInStep.done c with
    | ForInStep.yield c => h_1 c
    | ForInStep.done c => h_2 c) =
    h_2 c
-- Mathlib.Data.Matrix.Mul
one_dotProduct : ∀ {n : Type u_3} {α : Type v} [inst : Fintype n] [inst_1 : MulOneClass α] [inst_2 : AddCommMonoid α] (v : n → α),
  1 ⬝ᵥ v = ∑ i, v i
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalAddSubgroup.ext : ∀ {G : Type u} {inst : AddGroup G} {inst_1 : TopologicalSpace G} {x y : OpenNormalAddSubgroup G},
  (↑x.toOpenAddSubgroup).carrier = (↑y.toOpenAddSubgroup).carrier → x = y
-- Mathlib.Algebra.BigOperators.Finprod
MulEquivClass.map_finprod : ∀ {M : Type u_2} {N : Type u_3} {α : Sort u_4} [inst : CommMonoid M] [inst_1 : CommMonoid N] {F : Type u_7}
  [inst_2 : EquivLike F M N] [MulEquivClass F M N] (g : F) (f : α → M), g (∏ᶠ (i : α), f i) = ∏ᶠ (i : α), g (f i)
-- Mathlib.Topology.Path
Path.instFunLike : {X : Type u_1} → [inst : TopologicalSpace X] → {x y : X} → FunLike (Path x y) (↑unitInterval) X
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.supports_union : ∀ {K₁ K₂ S : Finset Turing.PartrecToTM2.Λ'},
  Turing.PartrecToTM2.Supports (K₁ ∪ K₂) S ↔ Turing.PartrecToTM2.Supports K₁ S ∧ Turing.PartrecToTM2.Supports K₂ S
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
/-- Consider a function `f : E → F` continuous on a segment `[a, b]`
and line differentiable in the direction `b - a` at all points of the open segment `(a, b)`.

If `‖∂_{b - a} f‖ ≤ C` at a.e. all points of the open segment,
then `‖f b - f a‖ ≤ C * volume s`, where `s` is the set of points `t ∈ Ioo 0 1`
such that `f` has nonzero line derivative in the direction `b - a` at `lineMap a b t`.  -/
norm_sub_le_mul_volume_of_norm_lineDeriv_le : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {f : E → F} {a b : E} {C : ℝ},
  ContinuousOn f (segment ℝ a b) →
    (∀ t ∈ Set.Ioo 0 1, LineDifferentiableAt ℝ f ((AffineMap.lineMap a b) t) (b - a)) →
      (∀ᵐ (t : ℝ), t ∈ Set.Ioo 0 1 → ‖lineDeriv ℝ f ((AffineMap.lineMap a b) t) (b - a)‖ ≤ C) →
        ‖f b - f a‖ ≤
          C * MeasureTheory.volume.real {t | t ∈ Set.Ioo 0 1 ∧ lineDeriv ℝ f ((AffineMap.lineMap a b) t) (b - a) ≠ 0}
-- Init.Data.Nat.Lcm
Nat.lcm_mul_right : ∀ (m n k : ℕ), (m * n).lcm (k * n) = m.lcm k * n
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Verify that `grind? +suggestions` suggestions actually work.  -/
verifyGrindSuggestions : Mathlib.TacticAnalysis.Config
-- Mathlib.Algebra.Lie.Free
FreeLieAlgebra.instLieAlgebra : (R : Type u) → (X : Type v) → [inst : CommRing R] → LieAlgebra R (FreeLieAlgebra R X)
-- Init.Data.Repr
/-- Turns `a` into a `Format` using its `Repr` instance. The precedence level is initially set to 0.
 -/
repr : {α : Type u_1} → [Repr α] → α → Std.Format
-- Aesop.Script.Step
Aesop.Script.LazyStep.BuildInput.mk.inj : ∀ {α : Type} {tac : Lean.MetaM α} {postGoals : α → Array Lean.MVarId} {tacticBuilder : α → Aesop.Script.TacticBuilder}
  {tac_1 : Lean.MetaM α} {postGoals_1 : α → Array Lean.MVarId} {tacticBuilder_1 : α → Aesop.Script.TacticBuilder},
  { tac := tac, postGoals := postGoals, tacticBuilder := tacticBuilder } =
      { tac := tac_1, postGoals := postGoals_1, tacticBuilder := tacticBuilder_1 } →
    tac = tac_1 ∧ postGoals = postGoals_1 ∧ tacticBuilder = tacticBuilder_1
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.Substring.Raw.Legacy.foldl.eq_1 : ∀ {α : Type u} (f : α → Char → α) (init : α) (s_2 : String) (b e : String.Pos.Raw),
  Substring.Raw.Legacy.foldl f init { str := s_2, startPos := b, stopPos := e } = String.Legacy.foldlAux f s_2 e b init
-- Mathlib.Algebra.DirectSum.Ring
/-- The multiplication from the `Mul` instance, as a bundled homomorphism.  -/
DirectSum.mulHom : {ι : Type u_1} →
  [DecidableEq ι] →
    (A : ι → Type u_2) →
      [inst : Add ι] →
        [inst_1 : (i : ι) → AddCommMonoid (A i)] →
          [DirectSum.GNonUnitalNonAssocSemiring A] →
            (DirectSum ι fun i => A i) →+ (DirectSum ι fun i => A i) →+ DirectSum ι fun i => A i
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.contains_filter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {f : (a : α) → β a → Bool} {k : α}, (Std.ExtDHashMap.filter f m).contains k = Option.any (f k) (m.get? k)
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Implementation
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.mk : {numVarsSucc : ℕ} →
  Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause numVarsSucc)) →
    Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin numVarsSucc)) →
      Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin numVarsSucc)) →
        Array Std.Tactic.BVDecide.LRAT.Internal.Assignment →
          Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula numVarsSucc
-- Mathlib.Tactic.Tauto
/-- The list of hypothesis left to work on, renamed to be up-to-date with
the current goal.  -/
Mathlib.Tactic.Tauto.DistribNotState.fvars : Mathlib.Tactic.Tauto.DistribNotState → List Lean.Expr
-- Mathlib.CategoryTheory.Monoidal.Tor
/-- The higher `Tor'` groups for `X` and `Y` are zero if `X` is projective.  -/
CategoryTheory.isZero_Tor'_succ_of_projective : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.MonoidalPreadditive C]
  [inst_4 : CategoryTheory.HasProjectiveResolutions C] (X Y : C) [CategoryTheory.Projective X] (n : ℕ),
  CategoryTheory.Limits.IsZero (((CategoryTheory.Tor' C (n + 1)).obj X).obj Y)
-- Mathlib.Algebra.Group.Subgroup.Map
/-- An isomorphism of groups gives an order isomorphism between the lattices of subgroups,
defined by sending subgroups to their forward images.

See also `AddEquiv.comapAddSubgroup` which maps subgroups to their inverse images.  -/
AddEquiv.mapAddSubgroup : {G : Type u_1} → [inst : AddGroup G] → {H : Type u_6} → [inst_1 : AddGroup H] → G ≃+ H → AddSubgroup G ≃o AddSubgroup H
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
/-- The bivariate `n`-division polynomials `ψₙ`.  -/
WeierstrassCurve.ψ : {R : Type r} → [inst : CommRing R] → WeierstrassCurve R → ℤ → Polynomial (Polynomial R)
-- Mathlib.Algebra.Field.Basic
/-- Constructs a `Field` structure on a `CommRing` consisting only of units and 0.  -/
Field.ofIsUnitOrEqZero : {R : Type u_3} → [Nontrivial R] → [inst : CommRing R] → (∀ (a : R), IsUnit a ∨ a = 0) → Field R
-- Mathlib.Topology.MetricSpace.ThickenedIndicator
thickenedIndicatorAux_lt_top : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {δ : ℝ} {E : Set α} {x : α}, thickenedIndicatorAux δ E x < ⊤
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.str : (self : AddGrpCat) → AddGroup ↑self
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Subsemiring.op_sInf : ∀ {R : Type u_2} [inst : NonAssocSemiring R] (S : Set (Subsemiring R)), (sInf S).op = sInf (Subsemiring.unop ⁻¹' S)
-- Mathlib.CategoryTheory.Monoidal.NaturalTransformation
CategoryTheory.NatTrans.IsMonoidal.tensor_assoc : ∀ {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₁ F₂ : CategoryTheory.Functor C D} {τ : F₁ ⟶ F₂} {inst_4 : F₁.LaxMonoidal} {inst_5 : F₂.LaxMonoidal}
  [self : CategoryTheory.NatTrans.IsMonoidal τ] (X Y : C) {Z : D}
  (h : F₂.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F₁ X Y)
      (CategoryTheory.CategoryStruct.comp (τ.app (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (τ.app X) (τ.app Y))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F₂ X Y) h)
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.associator_hom_τl : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : CategoryTheory.Bicategory.Adj B} (α : a ⟶ b) (β : b ⟶ c)
  (γ : c ⟶ d),
  (CategoryTheory.Bicategory.associator α β γ).hom.τl = (CategoryTheory.Bicategory.associator α.l β.l γ.l).hom
-- Std.Data.HashMap.RawLemmas
/-- Simpler variant of `getD_filter` when `LawfulBEq` is available.  -/
Std.HashMap.Raw.getD_filter' : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [LawfulBEq α]
  {f : α → β → Bool} {k : α} {fallback : β},
  m.WF → (Std.HashMap.Raw.filter f m).getD k fallback = (Option.filter (f k) m[k]?).getD fallback
-- Mathlib.Analysis.Analytic.IsolatedZeros
/-- The *principle of isolated zeros* for an analytic function, local version: if a function is
analytic at `z₀`, then either it is identically zero in a neighborhood of `z₀`, or it does not
vanish in a punctured neighborhood of `z₀`.  -/
AnalyticAt.eventually_eq_zero_or_eventually_ne_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜},
  AnalyticAt 𝕜 f z₀ → (∀ᶠ (z : 𝕜) in nhds z₀, f z = 0) ∨ ∀ᶠ (z : 𝕜) in nhdsWithin z₀ {z₀}ᶜ, f z ≠ 0
-- Mathlib.Algebra.Order.Group.End
RelHom.coe_one : ∀ {α : Type u_1} {r : α → α → Prop}, ⇑1 = id
-- Init.Data.List.MinMaxOn
_private.Init.Data.List.MinMaxOn.0.List.foldl.match_1.eq_1 : ∀ {α : Type u_3} {β : Type u_1} (motive : α → List β → Sort u_2) (a : α) (h_1 : (a : α) → motive a [])
  (h_2 : (a : α) → (b : β) → (l : List β) → motive a (b :: l)),
  (match a, [] with
    | a, [] => h_1 a
    | a, b :: l => h_2 a b l) =
    h_1 a
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.isIso₂_truncGT_map_of_isLE : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    ∀ (n₀ : ℤ), t.IsLE T.obj₁ n₀ → CategoryTheory.IsIso ((t.truncGT n₀).map T.mor₂)
-- Mathlib.CategoryTheory.Limits.Shapes.KernelPair
/-- If `(a,b)` is a kernel pair for `f₁` and `f₂` is mono, then `(a,b)` is a kernel pair for `f₁ ≫ f₂`.
The converse of `cancel_right_of_mono`.
 -/
CategoryTheory.IsKernelPair.comp_of_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {R X Y Z : C} {a b : R ⟶ X} {f₁ : X ⟶ Y} {f₂ : Y ⟶ Z}
  [CategoryTheory.Mono f₂],
  CategoryTheory.IsKernelPair f₁ a b → CategoryTheory.IsKernelPair (CategoryTheory.CategoryStruct.comp f₁ f₂) a b
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.all_eq_not_any_not : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] {p : α → Bool},
  m.WF → m.all p = !m.any fun a => !p a