mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.linearDeriv_apply : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂]
  (f : ContinuousMultilinearMap R M₁ M₂) [inst_7 : ContinuousAdd M₂] [inst_8 : DecidableEq ι] [inst_9 : Fintype ι]
  (x y : (i : ι) → M₁ i), (f.linearDeriv x) y = ∑ i, f (Function.update x i (y i))
-- Lean.Elab.PreDefinition.FixedParams
Lean.Elab.FixedParamPerms.mk.inj : ∀ {numFixed : ℕ} {perms : Array Lean.Elab.FixedParamPerm} {revDeps : Array (Array (Array ℕ))} {numFixed_1 : ℕ}
  {perms_1 : Array Lean.Elab.FixedParamPerm} {revDeps_1 : Array (Array (Array ℕ))},
  { numFixed := numFixed, perms := perms, revDeps := revDeps } =
      { numFixed := numFixed_1, perms := perms_1, revDeps := revDeps_1 } →
    numFixed = numFixed_1 ∧ perms = perms_1 ∧ revDeps = revDeps_1
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getD_inter_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  {fallback : β k}, k ∉ m₂ → (m₁ ∩ m₂).getD k fallback = fallback
-- Mathlib.RingTheory.RamificationInertia.Ramification
/-- **Alias** of `Ideal.ramificationIdx_def`. -/
Ideal.ramificationIdx'_def : ∀ {S : Type u_1} [inst : CommRing S] (q : Ideal S) (R : Type u_2) [inst_1 : CommRing R] [inst_2 : Algebra R S]
  [inst_3 : q.IsPrime],
  q.ramificationIdx R =
    (Module.length (Localization.AtPrime q)
        (Localization.AtPrime q ⧸ Ideal.map (algebraMap R (Localization.AtPrime q)) (Ideal.under R q))).toNat
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.sumArrowIsometryEquivProdArrow_toHomeomorph : ∀ {γ : Type w} [inst : PseudoEMetricSpace γ] {α : Type u_3} {β : Type u_4} [inst_1 : Fintype α] [inst_2 : Fintype β],
  IsometryEquiv.sumArrowIsometryEquivProdArrow.toHomeomorph = Homeomorph.sumArrowHomeomorphProdArrow
-- Std.Time.Zoned.TimeZone
Std.Time.TimeZone.mk.injEq : ∀ (offset : Std.Time.TimeZone.Offset) (name abbreviation : String) (isDST : Bool) (offset_1 : Std.Time.TimeZone.Offset)
  (name_1 abbreviation_1 : String) (isDST_1 : Bool),
  ({ offset := offset, name := name, abbreviation := abbreviation, isDST := isDST } =
      { offset := offset_1, name := name_1, abbreviation := abbreviation_1, isDST := isDST_1 }) =
    (offset = offset_1 ∧ name = name_1 ∧ abbreviation = abbreviation_1 ∧ isDST = isDST_1)
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `antivaryOn_neg`. -/
AntivaryOn.of_neg : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] {s : Set ι} {f : ι → α} {g : ι → β},
  AntivaryOn (-f) (-g) s → AntivaryOn f g s
-- Mathlib.Algebra.Order.Ring.Archimedean
ArchimedeanClass.mk_le_mk_iff_denselyOrdered : ∀ {R : Type u_1} {S : Type u_2} [inst : LinearOrder R] [inst_1 : LinearOrder S] [inst_2 : CommRing R]
  [IsStrictOrderedRing R] [inst_4 : Ring S] [inst_5 : IsStrictOrderedRing S] [DenselyOrdered R] [Archimedean R]
  {x y : S} (f : R →+* S),
  StrictMono ⇑f → (ArchimedeanClass.mk x ≤ ArchimedeanClass.mk y ↔ ∃ q, 0 < f q ∧ f q * |y| ≤ |x|)
-- Mathlib.Topology.Sheaves.Skyscraper
skyscraperPresheaf_map : ∀ {X : TopCat} (p₀ : ↑X) [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v}
  [inst_1 : CategoryTheory.Category.{w, v} C] [inst_2 : CategoryTheory.Limits.HasTerminal C] (A : C)
  {U V : (TopologicalSpace.Opens ↑X)ᵒᵖ} (i : U ⟶ V),
  (skyscraperPresheaf p₀ A).map i =
    if h : p₀ ∈ Opposite.unop V then CategoryTheory.eqToHom ⋯
    else (⋯ ▸ CategoryTheory.Limits.terminalIsTerminal).from (if p₀ ∈ Opposite.unop U then A else ⊤_ C)
-- Mathlib.Order.Interval.Set.Image
Set.image_subtype_val_Ioc_Iic : ∀ {α : Type u_1} [inst : Preorder α] {a b : α} (c : ↑(Set.Ioc a b)), Subtype.val '' Set.Iic c = Set.Ioc a ↑c
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
ciSup_unique : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompletePartialOrderSup α] [inst_1 : Unique ι] {s : ι → α},
  ⨆ i, s i = s default
-- Lean.Server.Requests
Lean.Server.SerializedLspResponse.mk : Option Lean.Json → String → Bool → Lean.Server.SerializedLspResponse
-- ProofWidgets.Data.Html
ProofWidgets.Jsx.proofWidgetsJsxChild__1 : Lean.ParserDescr
-- Mathlib.FieldTheory.FinTrdeg
exists_finset_isTranscendenceBasis : ∀ (K : Type u_1) (L : Type u_2) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [FinTrdeg K L],
  ∃ s, IsTranscendenceBasis K Subtype.val
-- Init.Data.AC
Lean.Data.AC.EvalInformation : Sort u → Sort v → Sort (max (max 1 u) v)
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.GrindCnstr.guard.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Probability.Independence.Kernel.Indep
/-- The measurable space structures generated by independent pi-systems are independent.  -/
ProbabilityTheory.Kernel.IndepSets.indep : ∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {m1 m2 m : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} [ProbabilityTheory.IsZeroOrMarkovKernel κ]
  {p1 p2 : Set (Set Ω)},
  m1 ≤ m →
    m2 ≤ m →
      IsPiSystem p1 →
        IsPiSystem p2 →
          m1 = MeasurableSpace.generateFrom p1 →
            m2 = MeasurableSpace.generateFrom p2 →
              ProbabilityTheory.Kernel.IndepSets p1 p2 κ μ → ProbabilityTheory.Kernel.Indep m1 m2 κ μ
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.isEmpty_diff_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t₁.isEmpty = true → (t₁ \ t₂).isEmpty = true
-- Mathlib.Data.Multiset.Filter
Multiset.card_filter_le_iff : ∀ {α : Type u_1} (s : Multiset α) (P : α → Prop) [inst : DecidablePred P] (n : ℕ),
  (Multiset.filter P s).card ≤ n ↔ ∀ s' ≤ s, n < s'.card → ∃ a ∈ s', ¬P a
-- Std.Http.Data.Status
Std.Http.Status.permanentRedirect.sizeOf_spec : sizeOf Std.Http.Status.permanentRedirect = 1
-- Mathlib.Order.Category.DistLat
DistLat.instConcreteCategoryLatticeHomCarrier : CategoryTheory.ConcreteCategory DistLat fun x1 x2 => LatticeHom ↑x1 ↑x2
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.getKeyD_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → ∀ {k fallback : α}, t₁.getKeyD k fallback = t₂.getKeyD k fallback
-- Mathlib.FieldTheory.IsPerfectClosure
IsPerfectClosure.equiv_comp : ∀ {K : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing K] [inst_1 : CommRing L] [inst_2 : CommRing M]
  (i : K →+* L) (j : K →+* M) (p : ℕ) [inst_3 : ExpChar M p] [inst_4 : ExpChar K p] [inst_5 : ExpChar L p]
  [inst_6 : PerfectRing L p] [inst_7 : IsPerfectClosure i p] [inst_8 : PerfectRing M p] [inst_9 : IsPerfectClosure j p],
  (↑(IsPerfectClosure.equiv i j p)).comp i = j
-- Mathlib.InformationTheory.Hamming
/-- Corresponds to `eq_of_dist_eq_zero`.  -/
eq_of_hammingDist_eq_zero : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)] {x y : (i : ι) → β i},
  hammingDist x y = 0 → x = y
-- Mathlib.Algebra.GroupWithZero.Basic
/-- **Alias** of `eq_zero_of_pow_eq_zero`. -/
IsReduced.pow_eq_zero : ∀ {R : Type u_3} {x : R} [inst : Zero R] [inst_1 : Pow R ℕ] [IsReduced R] {n : ℕ}, x ^ n = 0 → x = 0
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.size_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {v : β k}, (t.insertIfNew k v).size = if k ∈ t then t.size else t.size + 1
-- Aesop.Tree.Free
_private.Aesop.Tree.Free.0.Aesop.freeRappRef : Aesop.GoalRef → Aesop.MVarClusterRef → Aesop.RappRef → BaseIO Unit
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
UniformContinuous.neg : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α]
  [inst_3 : UniformSpace β] {f : β → α}, UniformContinuous f → UniformContinuous fun x => -f x
-- Mathlib.Analysis.InnerProductSpace.Calculus
DifferentiableWithinAt.dist : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
  [inst : NormedSpace ℝ E] {G : Type u_4} [inst_2 : NormedAddCommGroup G] [inst_3 : NormedSpace ℝ G] {f g : G → E}
  {s : Set G} {x : G},
  DifferentiableWithinAt ℝ f s x →
    DifferentiableWithinAt ℝ g s x → f x ≠ g x → DifferentiableWithinAt ℝ (fun y => dist (f y) (g y)) s x
-- Init.Data.UInt.Lemmas
USize.toUInt8_le : ∀ {a b : USize}, a.toUInt8 ≤ b.toUInt8 ↔ a % 256 ≤ b % 256
-- Mathlib.Topology.Category.TopCat.Basic
TopCat.ofHom_id : ∀ {X : Type u} [inst : TopologicalSpace X],
  TopCat.ofHom (ContinuousMap.id X) = CategoryTheory.CategoryStruct.id (TopCat.of X)
-- Mathlib.RingTheory.RingHom.Unramified
RingHom.FormallyUnramified.ofLocalizationSpanTarget : RingHom.OfLocalizationSpanTarget fun {R S} [CommRing R] [CommRing S] => RingHom.FormallyUnramified
-- Mathlib.Data.Finsupp.Lex
Finsupp.Lex.single_le_iff : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, ((toLex fun₀ | b => 1) ≤ toLex fun₀ | a => 1) ↔ a ≤ b
-- Mathlib.RingTheory.AdicCompletion.Exactness
_private.Mathlib.RingTheory.AdicCompletion.Exactness.0.AdicCompletion.mapExactAuxDelta.congr_simp : ∀ {R : Type u} [inst : CommRing R] {I : Ideal R} {M : Type u} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {f : M →ₗ[R] N} (hf : Function.Injective ⇑f) {k : ℕ}
  (hkn : ∀ n ≥ k, I ^ n • ⊤ ⊓ f.range = I ^ (n - k) • (I ^ k • ⊤ ⊓ f.range)) (x : AdicCompletion.AdicCauchySequence I N)
  {n : ℕ} {d d_1 : N} (e_d : d = d_1) (hdmem : d ∈ I ^ (k + n + 1) • ⊤) {y y_1 : M} (e_y : y = y_1) {yₙ : M}
  (hd : f y = ↑x (k + n + 1) - d) (hyₙ : f yₙ - ↑x (k + n) ∈ I ^ (k + n) • ⊤),
  AdicCompletion.mapExactAuxDelta✝ hf hkn x hdmem hd hyₙ = AdicCompletion.mapExactAuxDelta✝ hf hkn x ⋯ ⋯ hyₙ
-- Mathlib.Data.Finset.Sum
Finset.gc_map_inl_toLeft : ∀ {α : Type u_1} {β : Type u_2}, GaloisConnection (fun x => Finset.map Function.Embedding.inl x) Finset.toLeft
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey_ofList_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
      k ∈ List.map Prod.fst l →
        ∀ {h' : k' ∈ Std.ExtTreeMap.ofList l cmp}, (Std.ExtTreeMap.ofList l cmp).getKey k' h' = k
-- Mathlib.Algebra.Group.Submonoid.Saturation
Submonoid.saturation_le_iff_le : ∀ {M : Type u_1} [inst : MulOneClass M] {a : Submonoid M} {b : SaturatedSubmonoid M},
  a.saturation ≤ b ↔ a ≤ b.toSubmonoid
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.support.eq_def : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (x : G.Walk u v),
  x.support =
    match v, x with
    | .(u), SimpleGraph.Walk.nil => [u]
    | v, SimpleGraph.Walk.cons h p => u :: p.support
-- Mathlib.Data.Matrix.Block
Matrix.toBlock_mul_eq_add : ∀ {R : Type u_10} [inst : CommRing R] {m : Type u_14} {n : Type u_15} {k : Type u_16} [inst_1 : Fintype n]
  (p : m → Prop) (q : n → Prop) [inst_2 : DecidablePred q] (r : k → Prop) (A : Matrix m n R) (B : Matrix n k R),
  (A * B).toBlock p r = A.toBlock p q * B.toBlock q r + (A.toBlock p fun i => ¬q i) * B.toBlock (fun i => ¬q i) r
-- Mathlib.RingTheory.Ideal.IdempotentFG
Ideal.isIdempotentElem_iff_eq_bot_or_top : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] (I : Ideal R), I.FG → (IsIdempotentElem I ↔ I = ⊥ ∨ I = ⊤)
-- Init.Data.Option.Lemmas
Option.get_eq_getD : ∀ {α : Type u_1} {fallback : α} (o : Option α) {h : o.isSome = true}, o.get h = o.getD fallback
-- Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
LinearMap.exists_monic_and_aeval_eq_zero : ∀ {M : Type u_2} [inst : AddCommGroup M] (R : Type u_3) [inst_1 : CommRing R] [inst_2 : Module R M] [Module.Finite R M]
  (f : Module.End R M), ∃ p, p.Monic ∧ (Polynomial.aeval f) p = 0
-- Mathlib.Geometry.Manifold.Notation
/-- Delaborator for `Bundle.TotalSpace.mk'` using anonymous constructor notation.  -/
Manifold.delabTotalSpaceMkPrime : Lean.PrettyPrinter.Delaborator.Delab
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get?_eq_none_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t.WF → ∀ {a : α}, t.contains a = false → t.get? a = none
-- Mathlib.AlgebraicGeometry.RelativeGluing
AlgebraicGeometry.Scheme.Cover.RelativeGluingData.cover_I₀ : ∀ {S : AlgebraicGeometry.Scheme} {𝒰 : S.OpenCover} [inst : CategoryTheory.Category.{u_2, u_1} 𝒰.I₀]
  [inst_1 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] (d : AlgebraicGeometry.Scheme.Cover.RelativeGluingData 𝒰)
  [inst_2 : Small.{u, u_1} 𝒰.I₀] [inst_3 : Quiver.IsThin 𝒰.I₀], d.cover.I₀ = 𝒰.I₀
-- Mathlib.Topology.UniformSpace.Basic
tendsto_prod_uniformity_snd : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β],
  Filter.Tendsto (fun p => (p.1.2, p.2.2)) (uniformity (α × β)) (uniformity β)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
MeasurableSet.induction_on_open : ∀ {γ : Type u_3} [inst : TopologicalSpace γ] [inst_1 : MeasurableSpace γ] [inst_2 : BorelSpace γ]
  {C : (s : Set γ) → MeasurableSet s → Prop},
  (∀ (U : Set γ) (hU : IsOpen U), C U ⋯) →
    (∀ (t : Set γ) (ht : MeasurableSet t), C t ht → C tᶜ ⋯) →
      (∀ (f : ℕ → Set γ),
          Pairwise (Function.onFun Disjoint f) →
            ∀ (hf : ∀ (i : ℕ), MeasurableSet (f i)), (∀ (i : ℕ), C (f i) ⋯) → C (⋃ i, f i) ⋯) →
        ∀ (t : Set γ) (ht : MeasurableSet t), C t ht
-- Mathlib.Topology.UnitInterval
unitInterval.one_minus_nonneg : ∀ (x : ↑unitInterval), 0 ≤ 1 - ↑x
-- Init.Data.Option.Attach
Option.getD_attach : ∀ {α : Type u_1} {o : Option α} {fallback : { x // o = some x }}, o.attach.getD fallback = fallback
-- Init.GrindInstances.ToInt
Lean.Grind.instZeroUInt64UintOfNatNat : Lean.Grind.ToInt.Zero UInt64 (Lean.Grind.IntInterval.uint 64)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.map_iSup : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] {ι : Sort u_1} (f : R →+* S)
  (s : ι → Subsemiring R), Subsemiring.map f (iSup s) = ⨆ i, Subsemiring.map f (s i)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey?_union : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, (m₁ ∪ m₂).getKey? k = (m₂.getKey? k).or (m₁.getKey? k)
-- Std.Data.HashSet.Lemmas
Std.HashSet.size_le_size_insertMany : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} {ρ : Type v} [inst : ForIn Id ρ α] [EquivBEq α]
  [LawfulHashable α] {l : ρ}, m.size ≤ (m.insertMany l).size
-- Mathlib.RingTheory.Ideal.Maps
Ideal.exists_ideal_comap_le_prime : ∀ {R : Type u} {F : Type u_1} [inst : Semiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : FunLike F R S]
  [inst_3 : RingHomClass F R S] {f : F} (P : Ideal R) [P.IsPrime] (I : Ideal S),
  Ideal.comap f I ≤ P → ∃ Q ≥ I, Q.IsPrime ∧ Ideal.comap f Q ≤ P
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem!_filter_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited β] {f : α → β → Bool} {k k' : α},
  t.getKey? k = some k' → (Std.ExtTreeMap.filter f t)[k]! = (Option.filter (f k') t[k]?).get!
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit_empty_list_singleton : ∀ {α : Type u} {instOrd : Ord α} {k : α},
  ↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit Std.DTreeMap.Internal.Impl.empty [k] ⋯) =
    (Std.DTreeMap.Internal.Impl.insertIfNew k () Std.DTreeMap.Internal.Impl.empty ⋯).impl
-- Init.Data.Iterators.Consumers.Monadic.Loop
Std.IterM.DefaultConsumers.forIn'.wf.eq_def : ∀ {m : Type w → Type w'} {α β : Type w} [inst : Std.Iterator α m β] {n : Type x → Type x'} [inst_1 : Monad n]
  (lift : (γ : Type w) → (δ : Type x) → (γ → n δ) → m γ → n δ) (γ : Type x)
  (PlausibleForInStep : β → γ → ForInStep γ → Prop) (wf : Std.IteratorLoop.WellFounded α m PlausibleForInStep)
  (it : Std.IterM m β) (init : γ) (P : β → Prop) (hP : ∀ (b : β), it.IsPlausibleIndirectOutput b → P b)
  (f : (b : β) → P b → (c : γ) → n (Subtype (PlausibleForInStep b c))),
  Std.IterM.DefaultConsumers.forIn'.wf lift γ PlausibleForInStep wf it init P hP f =
    (fun x => lift (Std.Shrink it.Step) γ x it.step) fun s =>
      match s.inflate with
      | ⟨Std.IterStep.yield it' out, h⟩ => do
        let __do_lift ← f out ⋯ init
        match __do_lift with
          | ⟨ForInStep.yield c, property⟩ =>
            Std.IterM.DefaultConsumers.forIn'.wf lift γ PlausibleForInStep wf it' c P ⋯ f
          | ⟨ForInStep.done c, property⟩ => pure c
      | ⟨Std.IterStep.skip it', h⟩ => Std.IterM.DefaultConsumers.forIn'.wf lift γ PlausibleForInStep wf it' init P ⋯ f
      | ⟨Std.IterStep.done, property⟩ => pure init
-- Mathlib.NumberTheory.Bernoulli
sum_bernoulli : ∀ (n : ℕ), ∑ k ∈ Finset.range n, ↑(n.choose k) * bernoulli k = if n = 1 then 1 else 0
-- Std.Sync.Broadcast
/-- Peeks at the element at the front of the buffer without removing it.
Returns none if the buffer is empty.
 -/
_private.Std.Sync.Broadcast.0.Std.Bounded.getSlot : {m : Type → Type} →
  {α : Type} →
    [Monad m] → [MonadLiftT (ST IO.RealWorld) m] → ℕ → Std.AtomicT (Std.Bounded.State✝ α) m (IO.Ref (Std.Slot✝ α))
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getD_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool} {k : α} {fallback : β},
  Std.ExtDTreeMap.Const.getD (Std.ExtDTreeMap.filter f t) k fallback =
    ((Std.ExtDTreeMap.Const.get? t k).pfilter fun x h' => f (t.getKey k ⋯) x).getD fallback
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.instMulAction : {R : Type u_1} → {S : Type u_2} → {a b : R} → [inst : Monoid S] → [MulAction S R] → MulAction S (QuadraticAlgebra R a b)
-- Mathlib.Analysis.Normed.Module.Convex
/-- The segment from `x` to `y` is contained in the closed ball centered at `x` with radius
`dist x y`.  -/
segment_subset_closedBall_left : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (x y : E),
  segment ℝ x y ⊆ Metric.closedBall x (dist x y)
-- Mathlib.Algebra.Ring.Hom.Defs
NonUnitalRingHom.coe_comp_addMonoidHom : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : NonUnitalNonAssocSemiring α]
  [inst_1 : NonUnitalNonAssocSemiring β] [inst_2 : NonUnitalNonAssocSemiring γ] (g : β →ₙ+* γ) (f : α →ₙ+* β),
  { toFun := ⇑g ∘ ⇑f, map_zero' := ⋯, map_add' := ⋯ } = (↑g).comp ↑f
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
/-- A continuous equivalence `f` between modules `M` and `N` on `R` induces an equivalence between
closed submodules in `M` and those in `N` through `map f`.
The definition does not use `ClosedSubmodule.map` because that has additional `ContinuousAdd` and
`ContinuousConstSMul` type-class assumptions.  -/
ClosedSubmodule.mapEquiv : {R : Type u_2} →
  {M : Type u_3} →
    {N : Type u_4} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : TopologicalSpace M] →
            [inst_3 : Module R M] →
              [inst_4 : AddCommMonoid N] →
                [inst_5 : TopologicalSpace N] →
                  [inst_6 : Module R N] → (M ≃L[R] N) → ClosedSubmodule R M ≃ ClosedSubmodule R N
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
LineDifferentiableAt.smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {f : E → F} {x v : E},
  LineDifferentiableAt 𝕜 f x v → ∀ (c : 𝕜), LineDifferentiableAt 𝕜 f x (c • v)
-- Init.Data.Range.Polymorphic.Map
/-- Compatibility class for `Map` and `≤`.  -/
Std.PRange.UpwardEnumerable.Map.PreservesLE : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Std.PRange.UpwardEnumerable α] →
      [inst_1 : Std.PRange.UpwardEnumerable β] → [LE α] → [LE β] → Std.PRange.UpwardEnumerable.Map α β → Prop
-- Mathlib.Algebra.Category.MonCat.Limits
/-- If `J` is `u`-small, the forgetful functor from `CommMonCat.{u}` preserves limits of
shape `J`.  -/
CommMonCat.forget_preservesLimitsOfShape : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] [Small.{u, v} J],
  CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget CommMonCat)
-- Mathlib.Analysis.InnerProductSpace.Spectrum
LinearMap.IsSymmetric.charpoly_eq : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E} [inst_3 : FiniteDimensional 𝕜 E] {n : ℕ} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n),
  T.charpoly = ∏ i, (Polynomial.X - Polynomial.C ↑(hT.eigenvalues hn i))
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Any_def : ∀ {α : Type u_1} {p : α → Prop} {t : RBTree.RBNode α}, RBTree.RBNode.Any p t ↔ ∃ x ∈ t, p x
-- Std.Http.Internal.ChunkedBuffer
/-- Writes a `Char` to the `ChunkedBuffer`. Only the low byte is written (`Char.toUInt8`),
so this is only correct for ASCII characters.
 -/
Std.Http.Internal.ChunkedBuffer.writeChar : Std.Http.Internal.ChunkedBuffer → Char → Std.Http.Internal.ChunkedBuffer
-- Mathlib.Algebra.Ring.Nat
Nat.instNonUnitalSemiring : NonUnitalSemiring ℕ
-- Mathlib.LinearAlgebra.Dual.Lemmas
Module.dualProdDualEquivDual_apply : ∀ (R : Type u_1) (M : Type u_3) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (M' : Type u_4)
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (φ : Module.Dual R M) (ψ : Module.Dual R M'),
  (Module.dualProdDualEquivDual R M M') (φ, ψ) = LinearMap.coprod φ ψ
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.FullyFaithful.preimage_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) {X Y Z : C} (f : F.obj X ⟶ F.obj Y) (g : F.obj Y ⟶ F.obj Z),
  hF.preimage (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (hF.preimage f) (hF.preimage g)
-- Mathlib.MeasureTheory.Measure.Haar.Basic
/-- The Haar measure on the locally compact group `G`, scaled so that `haarMeasure K₀ K₀ = 1`.  -/
MeasureTheory.Measure.haarMeasure : {G : Type u_1} →
  [inst : Group G] →
    [inst_1 : TopologicalSpace G] →
      [IsTopologicalGroup G] →
        [inst : MeasurableSpace G] → [BorelSpace G] → TopologicalSpace.PositiveCompacts G → MeasureTheory.Measure G
-- Mathlib.CategoryTheory.Monad.EquivMon
CategoryTheory.Monad.monadMonEquiv_functor : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  (CategoryTheory.Monad.monadMonEquiv C).functor = CategoryTheory.Monad.monadToMon C
-- Mathlib.Topology.Category.TopCat.Limits.Basic
TopCat.coinduced_of_isColimit : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J TopCat}
  (c : CategoryTheory.Limits.Cocone F) (hc : CategoryTheory.Limits.IsColimit c),
  c.pt.str = ⨆ j, TopologicalSpace.coinduced (⇑(CategoryTheory.ConcreteCategory.hom (c.ι.app j))) (F.obj j).str
-- Mathlib.Analysis.CStarAlgebra.Unitary.Maps
Unitary.mulLeft_apply : ∀ (R : Type u_1) {A : Type u_2} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : CStarRing A] [inst_3 : Ring R]
  [inst_4 : Module R A] [inst_5 : SMulCommClass R A A] (u : ↥(unitary A)) (x : A), ((Unitary.mulLeft R A) u) x = ↑u * x
-- Mathlib.Analysis.Complex.Trigonometric
Complex.ofReal_tanh : ∀ (x : ℝ), ↑(Real.tanh x) = Complex.tanh ↑x
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minView!.eq_1 : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (r : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.minView! k v Std.DTreeMap.Internal.Impl.leaf r = { k := k, v := v, tree := r }
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_eq_getElem?_getD : ∀ {w : ℕ} {x : BitVec w} {i : ℕ}, x.getLsbD i = x[i]?.getD false
-- Init.Data.Nat.Gcd
Nat.gcd_mul_left_add_left : ∀ (m n k : ℕ), (m * k + n).gcd m = n.gcd m