mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to1.trNormal.eq_4 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} {n : ℕ} (dec : List.Vector Bool n → Γ) (a : Γ → σ → Bool)
  (q₁ q₂ : Turing.TM1.Stmt Γ Λ σ),
  Turing.TM1to1.trNormal dec (Turing.TM1.Stmt.branch a q₁ q₂) =
    Turing.TM1to1.read dec fun a_1 =>
      Turing.TM1.Stmt.branch (fun x s => a a_1 s) (Turing.TM1to1.trNormal dec q₁) (Turing.TM1to1.trNormal dec q₂)
-- Mathlib.GroupTheory.EckmannHilton
EckmannHilton.commGroup.eq_1 : ∀ {X : Type u} {m₁ : X → X → X} {e₁ : X} (h₁ : EckmannHilton.IsUnital m₁ e₁) [G : Group X]
  (distrib : ∀ (a b c d : X), m₁ (a * b) (c * d) = m₁ a c * m₁ b d),
  EckmannHilton.commGroup h₁ distrib = { toGroup := G, mul_comm := ⋯ }
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
/-- Weighted sum of `P (x)` where `x` goes over `cos ((2 * i + 1) / (2 * n) * π)` for
`0 ≤ i < n`.  -/
Polynomial.Chebyshev.sumZeroes : ℕ → Polynomial ℝ → ℝ
-- Mathlib.Algebra.Algebra.Opposite
AlgHom.toOpposite_apply : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₐ[R] B) (hf : ∀ (x y : A), Commute (f x) (f y)),
  ⇑(f.toOpposite hf) = MulOpposite.op ∘ ⇑f
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKeyD_erase : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {k a fallback : α}, (m.erase k).getKeyD a fallback = if (k == a) = true then fallback else m.getKeyD a fallback
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.instLocallyConvexSpace : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F], LocallyConvexSpace ℝ (SchwartzMap E F)
-- Init.Core
iff_false_right : ∀ {a b : Prop}, ¬a → ((b ↔ a) ↔ ¬b)
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.map_one : ∀ {Γ : Type u_1} {R : Type u_3} {S : Type u_4} [inst : Zero Γ] [inst_1 : PartialOrder Γ] [inst_2 : MonoidWithZero R]
  [inst_3 : MonoidWithZero S] (f : R →*₀ S), HahnSeries.map 1 f = 1
-- Init.Data.Int.Order
Int.natAbs.eq_2 : ∀ (n_1 : ℕ), (Int.negSucc n_1).natAbs = n_1.succ
-- Mathlib.Analysis.Normed.Lp.WithLp
LinearEquiv.withLpCongr_refl : ∀ (p : ENNReal) {K : Type u_1} {V : Type u_4} [inst : Semiring K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
  LinearEquiv.withLpCongr p (LinearEquiv.refl K V) = LinearEquiv.refl K (WithLp p V)
-- Init.Data.Nat.Lemmas
Nat.mul_left_inj : ∀ {a b c : ℕ}, a ≠ 0 → (b * a = c * a ↔ b = c)
-- Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
MeasureTheory.integral_sum_dirac : ∀ {ι : Type u_1} {X : Type u_2} {E : Type u_3} [Countable ι] {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  {f : X → E} [inst_1 : NormedSpace ℝ E] [MeasurableSingletonClass X] {x : ι → X} {c : ι → ENNReal}
  [FiniteDimensional ℝ E],
  (∀ (i : ι), c i ≠ ⊤) →
    (∫ (x : X), f x ∂MeasureTheory.Measure.sum fun i => c i • MeasureTheory.Measure.dirac (x i)) =
      ∑' (i : ι), (c i).toReal • f (x i)
-- Mathlib.Analysis.Normed.Operator.Banach
ContinuousLinearEquiv.ofBijective_apply_symm_apply : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'}
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {F : Type u_4}
  [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜' F] {σ' : 𝕜' →+* 𝕜} [inst_6 : RingHomInvPair σ σ']
  [inst_7 : RingHomIsometric σ] [inst_8 : RingHomIsometric σ'] [inst_9 : CompleteSpace F] [inst_10 : CompleteSpace E]
  [inst_11 : RingHomInvPair σ' σ] (f : E →SL[σ] F) (hinj : (↑f).ker = ⊥) (hsurj : (↑f).range = ⊤) (y : F),
  f ((ContinuousLinearEquiv.ofBijective f hinj hsurj).symm y) = y
-- Mathlib.RingTheory.Etale.StandardEtale
Algebra.instIsStandardEtaleTensorProduct : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [Algebra.IsStandardEtale R S],
  Algebra.IsStandardEtale T (TensorProduct R T S)
-- Mathlib.RingTheory.Ideal.MinimalPrime.Basic
IsMinimalPrime.isPrime : ∀ {R : Type u_1} [inst : CommSemiring R] {p : Ideal R}, IsMinimalPrime p → p.IsPrime
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
/-- For a `WeierstrassCurve` defined over a ring of characteristic = 2,
there is an explicit change of variables of it to `Y² + a₃Y = X³ + a₄X + a₆`
(`WeierstrassCurve.IsCharTwoJEqZeroNF`) if its j = 0.  -/
WeierstrassCurve.toCharTwoJEqZeroNF : {R : Type u_1} → [inst : CommRing R] → WeierstrassCurve R → WeierstrassCurve.VariableChange R
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.MemBaseSet.exists_common_compl : ∀ {ι : Type u_1} [inst : Fintype ι] {I : BoxIntegral.Box ι} {c₁ c₂ : NNReal} {l : BoxIntegral.IntegrationParams}
  {r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)} {π₁ π₂ : BoxIntegral.TaggedPrepartition I},
  l.MemBaseSet I c₁ r₁ π₁ →
    l.MemBaseSet I c₂ r₂ π₂ →
      π₁.iUnion = π₂.iUnion →
        ∃ π,
          π.iUnion = ↑I \ π₁.iUnion ∧
            (l.bDistortion = true → π.distortion ≤ c₁) ∧ (l.bDistortion = true → π.distortion ≤ c₂)
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
AlgebraicGeometry.flat_iff : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.Flat f ↔
    ∀ {U : Y.Opens},
      AlgebraicGeometry.IsAffineOpen U →
        ∀ {V : X.Opens},
          AlgebraicGeometry.IsAffineOpen V →
            ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
              (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)).Flat
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
/-- The value of the Infimum of a nonempty family of outer measures on a set is not simply
the minimum value of a measure on that set: it is the infimum sum of measures of countable set of
sets that covers that set, where a different measure can be used for each set in the cover.  -/
MeasureTheory.OuterMeasure.biInf_apply' : ∀ {α : Type u_1} {ι : Type u_2} (I : Set ι) (m : ι → MeasureTheory.OuterMeasure α) {s : Set α},
  s.Nonempty → (⨅ i ∈ I, m i) s = ⨅ t, ⨅ (_ : s ⊆ Set.iUnion t), ∑' (n : ℕ), ⨅ i ∈ I, (m i) (t n)
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.pruneSolvedGoals : Lean.Elab.Tactic.Grind.GrindTacticM Unit
-- Mathlib.Algebra.Module.Equiv.Basic
/-- The equivalence between R-linear maps from `R` to `M`, and points of `M` itself.
This says that the forgetful functor from `R`-modules to types is representable, by `R`.

This is an `S`-linear equivalence, under the assumption that `S` acts on `M` commuting with `R`.
When `R` is commutative, we can take this to be the usual action with `S = R`.
Otherwise, `S = ℕ` shows that the equivalence is additive.
See note [bundled maps over different rings].
 -/
LinearMap.ringLmapEquivSelf : (R : Type u_1) →
  (S : Type u_4) →
    (M : Type u_5) →
      [inst : Semiring R] →
        [inst_1 : Semiring S] →
          [inst_2 : AddCommMonoid M] →
            [inst_3 : Module R M] → [inst_4 : Module S M] → [inst_5 : SMulCommClass R S M] → (R →ₗ[R] M) ≃ₗ[S] M
-- Mathlib.Algebra.Group.Commute.Basic
/-- **Alias** of the reverse direction of `Commute.inv_right_iff`. -/
Commute.inv_right : ∀ {G : Type u_1} [inst : Group G] {a b : G}, Commute a b → Commute a b⁻¹
-- Lean.Elab.Do.InferControlInfo
/-- The `do` block syntactically contains an early `return`.  -/
Lean.Elab.Do.ControlInfo.returnsEarly : Lean.Elab.Do.ControlInfo → Bool
-- Batteries.Data.List.Lemmas
List.nodup_idxsOf : ∀ {α : Type u_1} {xs : List α} {x : α} {s : ℕ} [inst : BEq α], (List.idxsOf x xs s).Nodup
-- Mathlib.Data.Setoid.Partition
/-- A finpartition gives rise to a setoid partition  -/
Finpartition.isPartition_parts : ∀ {α : Type u_1} (f : Finpartition Set.univ), Setoid.IsPartition ↑f.parts
-- Init.Data.List.Pairwise
List.Pairwise.forall_of_forall_of_flip : ∀ {α : Type u_1} {l : List α} {R : α → α → Prop},
  (∀ x ∈ l, R x x) → List.Pairwise R l → List.Pairwise (flip R) l → ∀ ⦃x : α⦄, x ∈ l → ∀ ⦃y : α⦄, y ∈ l → R x y
-- Mathlib.Topology.Algebra.Monoid
Prod.separatelyContinuousMul : ∀ {M : Type u_6} {N : Type u_7} [inst : TopologicalSpace M] [inst_1 : Mul M] [SeparatelyContinuousMul M]
  [inst_3 : TopologicalSpace N] [inst_4 : Mul N] [SeparatelyContinuousMul N], SeparatelyContinuousMul (M × N)
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.ext : ∀ {R : Type u_1} [inst : Zero R] ⦃f g : ArithmeticFunction R⦄, (∀ (x : ℕ), f x = g x) → f = g
-- Mathlib.Data.FinEnum
/-- enumerate all functions whose domain and range are finitely enumerable  -/
List.Pi.enum : {α : Type u_1} → [FinEnum α] → (β : α → Type u_3) → [(a : α) → FinEnum (β a)] → List ((a : α) → β a)
-- Mathlib.Analysis.Normed.Operator.Banach
ContinuousLinearMap.NonlinearRightInverse.right_inv' : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'}
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {F : Type u_4}
  [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜' F] {f : E →SL[σ] F} (self : f.NonlinearRightInverse) (y : F),
  f (self.toFun y) = y
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.forgetToPresheafModuleCatObjObj_coe : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (X : Cᵒᵖ)
  (hX : CategoryTheory.Limits.IsInitial X) (M : PresheafOfModules R) (Y : Cᵒᵖ),
  ↑(PresheafOfModules.forgetToPresheafModuleCatObjObj X hX M Y) = ↑(M.obj Y)
-- Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
/-- A locally discrete bicategory is strict.  -/
CategoryTheory.locallyDiscreteBicategory.strict : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.Bicategory.Strict (CategoryTheory.LocallyDiscrete C)
-- Batteries.Tactic.SeqFocus
/-- `tac <;> tac'` runs `tac` on the main goal and `tac'` on each produced goal,
concatenating all goals produced by `tac'`.


Extensions:

 * `t <;> [t1; t2; ...; tn]` focuses on the first goal and applies `t`, which should result in `n`
   subgoals. It then applies each `ti` to the corresponding goal and collects the resulting
   subgoals. It raises an error if the number of subgoals does not match. -/
Batteries.Tactic.seq_focus : Lean.TrailingParserDescr
-- Mathlib.Topology.Algebra.Valued.ValuationTopology
Valuation.map_eq_one_of_forall_lt : ∀ {K : Type u} [inst : DivisionRing K] {Γ₀ : Type v} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [MulArchimedean Γ₀]
  {v : Valuation K Γ₀} {r : Γ₀}, r ≠ 0 → (∀ (x : K), v x ≠ 0 → r < v x) → ∀ (x : K), v x ≠ 0 → v x = 1
-- Init.Grind.AC
Lean.Grind.AC.superpose_head_idempotent_cert.eq_1 : ∀ (x : Lean.Grind.AC.Var) (lhs₁ rhs₁ rhs : Lean.Grind.AC.Seq),
  Lean.Grind.AC.superpose_head_idempotent_cert x lhs₁ rhs₁ rhs =
    (lhs₁.startsWithVar_k x).and' (rhs.beq' ((Lean.Grind.AC.Seq.var x).concat rhs₁))
-- Std.Do.WP.SimpLemmas
Option.orElse.eq_1 : ∀ {α : Type u_1} (x : Unit → Option α) (a : α), (some a).orElse x = some a
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.maxGenEigenspace_eq_genEigenspace_finrank : ∀ {K : Type v} {V : Type w} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] [FiniteDimensional K V]
  (f : Module.End K V) (μ : K), f.maxGenEigenspace μ = (f.genEigenspace μ) ↑(Module.finrank K V)
-- Mathlib.Algebra.Category.HopfAlgCat.Basic
HopfAlgCat.category : {R : Type u} → [inst : CommRing R] → CategoryTheory.Category.{v, max (v + 1) u} (HopfAlgCat R)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RoiSlice.instToIterator : {α : Type u_1} →
  [inst : Ord α] →
    Std.ToIterator (Std.Slice (Std.DTreeMap.Internal.Unit.RoiSliceData α)) Id
      (Std.Iterators.Types.Map (Std.DTreeMap.Internal.Zipper α fun x => Unit) Id Id (fun ⦃x⦄ => monadLift) fun b =>
        pure b.fst)
      α
-- Mathlib.Algebra.Group.TypeTags.Basic
Additive.exists : ∀ {α : Type u} {p : Additive α → Prop}, (∃ a, p a) ↔ ∃ a, p (Additive.ofMul a)
-- Mathlib.LinearAlgebra.RootSystem.WeylGroup
RootPairing.reflection_mem_weylGroup : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (i : ι),
  RootPairing.Equiv.reflection P i ∈ P.weylGroup
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
FundamentalGroupoid.instSubsingleton : ∀ (X : Type u_3) [Subsingleton X], Subsingleton (FundamentalGroupoid X)
-- Std.Sat.AIG.CNF
/-- Add a `Decl.gate` to a cache.
 -/
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.Cache.addGate : {aig : Std.Sat.AIG ℕ} →
  {cnf : Std.Sat.CNF ℕ} →
    {lhs rhs : Std.Sat.AIG.Fanin} →
      (cache : Std.Sat.AIG.toCNF.Cache✝ aig cnf) →
        {hlb : lhs.gate < (Std.Sat.AIG.toCNF.Cache.marks✝ cache).size} →
          {hrb : rhs.gate < (Std.Sat.AIG.toCNF.Cache.marks✝ cache).size} →
            (idx : ℕ) →
              (h : idx < aig.decls.size) →
                aig.decls[idx] = Std.Sat.AIG.Decl.gate lhs rhs →
                  (Std.Sat.AIG.toCNF.Cache.marks✝ cache)[lhs.gate] = true →
                    (Std.Sat.AIG.toCNF.Cache.marks✝ cache)[rhs.gate] = true →
                      { out // Std.Sat.AIG.toCNF.Cache.IsExtensionBy✝ cache out idx h }
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.height_add : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (b : P.Base)
  [inst_5 : CharZero R] {i j k : ι}, P.root k = P.root i + P.root j → b.height k = b.height i + b.height j
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.dep_iff : ∀ {α : Type u_1} {M : Matroid α} {D : Set α}, M.Dep D ↔ ¬M.Indep D ∧ D ⊆ M.E
-- Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
CategoryTheory.ObjectProperty.instIsStableUnderCobaseChangeMonoModSerre : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsSerreClass], P.monoModSerre.IsStableUnderCobaseChange
-- Mathlib.Data.Matrix.Basic
LinearMap.mapMatrix_add : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} {α : Type u_11} {β : Type u_12} [inst : Semiring R]
  [inst_1 : Semiring S] {σᵣₛ : R →+* S} [inst_2 : AddCommMonoid α] [inst_3 : AddCommMonoid β] [inst_4 : Module R α]
  [inst_5 : Module S β] (f g : α →ₛₗ[σᵣₛ] β), (f + g).mapMatrix = f.mapMatrix + g.mapMatrix
-- Init.Prelude
/-- Modifies a reader monad's local value with `f`. The resulting computation applies `f` to the
incoming local value and passes the result to the inner computation.
 -/
ReaderT.adapt : {ρ : Type u} → {m : Type u → Type v} → {ρ' α : Type u} → (ρ' → ρ) → ReaderT ρ m α → ReaderT ρ' m α
-- Mathlib.AlgebraicGeometry.Artinian
AlgebraicGeometry.instIsLocallyArtinianXScheme : ∀ {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyArtinian X] {U : X.OpenCover} (i : U.I₀),
  AlgebraicGeometry.IsLocallyArtinian (U.X i)
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
Submodule.isOrtho_orthogonal_left : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (U : Submodule 𝕜 E), Uᗮ ⟂ U
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- Given a compatible local trivialisation `e` of `V` and a basis `b` of the model fiber `F`,
return the corresponding basis of `V x`.  -/
Bundle.Trivialization.basisAt : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {M : Type u_4} →
      [inst_1 : TopologicalSpace M] →
        {F : Type u_5} →
          [inst_2 : NormedAddCommGroup F] →
            [inst_3 : NormedSpace 𝕜 F] →
              {V : M → Type u_6} →
                [inst_4 : TopologicalSpace (Bundle.TotalSpace F V)] →
                  [inst_5 : (x : M) → AddCommGroup (V x)] →
                    [inst_6 : (x : M) → Module 𝕜 (V x)] →
                      [inst_7 : (x : M) → TopologicalSpace (V x)] →
                        [inst_8 : FiberBundle F V] →
                          [VectorBundle 𝕜 F V] →
                            {ι : Type u_7} →
                              {x : M} →
                                (e : Bundle.Trivialization F Bundle.TotalSpace.proj) →
                                  [MemTrivializationAtlas e] →
                                    Module.Basis ι 𝕜 F → x ∈ e.baseSet → Module.Basis ι 𝕜 (V x)
-- Init.Data.List.Lex
List.le_total_of_asymm : ∀ {α : Type u_1} [inst : LT α] [i : Std.Asymm fun x1 x2 => x1 < x2] (l₁ l₂ : List α), l₁ ≤ l₂ ∨ l₂ ≤ l₁
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.step_filterMapWithPostcondition : ∀ {α β γ : Type w} [inst : Std.Iterator α Id β] {it : Std.Iter β} {m : Type w → Type w'} {n : Type w → Type w''}
  {f : β → Std.Iterators.PostconditionT n (Option γ)} [inst_1 : Monad n] [LawfulMonad n] [MonadLiftT m n],
  (Std.Iter.filterMapWithPostcondition f it).step =
    match it.step with
    | ⟨Std.IterStep.yield it' out, h⟩ => do
      let __do_lift ← (f out).operation
      match __do_lift with
        | ⟨none, h'⟩ =>
          pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.Iter.filterMapWithPostcondition f it') ⋯))
        | ⟨some out', h'⟩ =>
          pure (Std.Shrink.deflate (Std.PlausibleIterStep.yield (Std.Iter.filterMapWithPostcondition f it') out' ⋯))
    | ⟨Std.IterStep.skip it', h⟩ =>
      pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.Iter.filterMapWithPostcondition f it') ⋯))
    | ⟨Std.IterStep.done, h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.done ⋯))
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
add_pos_iff : ∀ {α : Type u} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [CanonicallyOrderedAdd α] {a b : α},
  0 < a + b ↔ 0 < a ∨ 0 < b
-- Mathlib.Topology.EMetricSpace.Diam
/-- **Alias** of `Metric.ediam_eq_sSup`. -/
EMetric.diam_eq_sSup : ∀ {X : Type u_2} [inst : PseudoEMetricSpace X] (s : Set X), Metric.ediam s = sSup (Set.image2 edist s s)
-- Std.Http.Test.Helpers
/-- Always respond 200 "ok" without reading the request body.
 -/
Std.Http.Internal.Test.okHandler : Std.Http.Internal.Test.TestHandler
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.im_zero : ∀ {d : ℤ}, Zsqrtd.im 0 = 0
-- Mathlib.Topology.VectorBundle.Riemannian
/-- `Core` structure associated to a family of inner products on the fibers of a fiber bundle. This
is an auxiliary construction to endow the fibers with an inner product space structure without
creating diamonds.

Warning: Do not use this `Core` structure if the space you are interested in already has a norm
instance defined on it, otherwise this will create a second non-defeq norm instance!  -/
Bundle.RiemannianMetric.toCore : {B : Type u_4} →
  {E : B → Type u_6} →
    [inst : (b : B) → TopologicalSpace (E b)] →
      [inst_1 : (b : B) → AddCommGroup (E b)] →
        [inst_2 : (b : B) → Module ℝ (E b)] → Bundle.RiemannianMetric E → (b : B) → InnerProductSpace.Core ℝ (E b)
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
/-- **Alias** of `ciSup_subtype_fun`. -/
ciSup_subtype'' : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {ι : Type u_5} {s : Set ι} {f : ι → α},
  BddAbove (Set.range fun i => f ↑i) → sSup ∅ ≤ ⨆ i, f ↑i → ⨆ i, f ↑i = ⨆ t ∈ s, f t
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKeyD_eq_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    l.isEmpty = false →
      ∀ {km fallback : α},
        Std.Internal.List.maxKeyD l fallback = km ↔
          Std.Internal.List.getKey? km l = some km ∧
            ∀ (k : α), Std.Internal.List.containsKey k l = true → (compare k km).isLE = true
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.apply_faithfulSMul : ∀ {R : Type uR} {A₁ : Type uA₁} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Algebra R A₁],
  FaithfulSMul (A₁ ≃ₐ[R] A₁) A₁
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.NormalizePattern.getPatternFn? : Lean.Expr →
  Bool → Bool → Lean.Meta.Grind.NormalizePattern.PatternArgKind → Lean.Meta.Grind.NormalizePattern.M✝ (Option Lean.Expr)
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
Equiv.toLinearEquiv.congr_simp : ∀ {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M₂] (e e_1 : M ≃ M₂) (e_e : e = e_1) (h : IsLinearMap R ⇑e),
  e.toLinearEquiv h = e_1.toLinearEquiv ⋯
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.toContinuousLinearMap_id : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} [inst : Monoid G] [inst_1 : Ring R] [inst_2 : AddCommGroup V]
  [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  {π₁ : ContRepresentation R G V}, ContIntertwiningMap.id.toContinuousLinearMap = ContinuousLinearMap.id R V
-- Mathlib.FieldTheory.Finite.GaloisField
GaloisField.instIsGaloisOfFinite : ∀ {K : Type u_2} {K' : Type u_3} [inst : Field K] [inst_1 : Field K'] [Finite K'] [inst_3 : Algebra K K'], IsGalois K K'
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- A functor between preadditive categories that preserves (zero morphisms and) finite biproducts
preserves finite products.  -/
CategoryTheory.Limits.preservesProductsOfShape_of_preservesBiproductsOfShape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.PreservesZeroMorphisms] {J : Type u_1} [Finite J] [CategoryTheory.Limits.PreservesBiproductsOfShape J F],
  CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete J) F
-- Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
/-- `Q c₁ c₂` is a quadratic form over `R × R` such that `CliffordAlgebra (Q c₁ c₂)` is isomorphic
as an `R`-algebra to `ℍ[R,c₁,c₂]`.  -/
CliffordAlgebraQuaternion.Q : {R : Type u_1} → [inst : CommRing R] → R → R → QuadraticForm R (R × R)
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
hasProd_fintype_support : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] [inst_2 : Fintype β] (f : β → α)
  (L : SummationFilter β) [L.HasSupport] [inst_4 : DecidablePred fun x => x ∈ L.support],
  HasProd f (∏ b ∈ L.support.toFinset, f b) L
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.isInitial_ord : ∀ (c : Cardinal.{u_1}), c.ord.IsInitial
-- Mathlib.Analysis.Normed.Module.Bases
/-- The vector `e_n` is non-zero.  -/
SchauderBasis.RankOneDecomposition.e_ne_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {X : Type u_2} [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] (self : SchauderBasis.RankOneDecomposition 𝕜 X) (n : ℕ), self.e n ≠ 0
-- Mathlib.Data.Finsupp.MonomialOrder
MonomialOrder.toWithBotSyn_apply_bot : ∀ {σ : Type u_1} (m : MonomialOrder σ), m.toWithBotSyn ⊥ = ⊥
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.degree_finSuccEquiv : ∀ {R : Type u} [inst : CommSemiring R] {n : ℕ} {f : MvPolynomial (Fin (n + 1)) R},
  f ≠ 0 → ((MvPolynomial.finSuccEquiv R n) f).degree = ↑(MvPolynomial.degreeOf 0 f)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.mem_of_mem_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k a : α} {v : β k}, a ∈ t.insert k v → cmp k a ≠ Ordering.eq → a ∈ t
-- Lean.Meta.Tactic.Backtrack
/-- `discharge g` is called on goals for which there were no alternatives.
If `none` we return `g` as a new subgoal.
If `some l`, we replace `g` by `l` in the list of active goals, and recurse.
If failure, we backtrack. (defaults to failure)  -/
Lean.Meta.Tactic.Backtrack.BacktrackConfig.discharge : Lean.Meta.Tactic.Backtrack.BacktrackConfig → Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))
-- Mathlib.GroupTheory.Coset.Basic
AddSubgroup.quotientiInfAddSubgroupOfEmbedding_apply_mk : ∀ {α : Type u_1} [inst : AddGroup α] {ι : Type u_2} (f : ι → AddSubgroup α) (H : AddSubgroup α) (g : ↥H) (i : ι),
  (AddSubgroup.quotientiInfAddSubgroupOfEmbedding f H) (↑g) i = ↑g