mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.BooleanAlgebra.Set
Set.sdiff_ssubset_left_iff : ∀ {α : Type u_1} {s t : Set α}, s \ t ⊂ s ↔ (s ∩ t).Nonempty
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.eq_empty_iff_forall_contains : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], m = ∅ ↔ ∀ (a : α), m.contains a = false
-- Mathlib.Algebra.Order.Ring.Abs
abs_zsmul : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] (n : ℤ) (a : α),
  |n • a| = |n| • |a|
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm_mono_ae : ∀ {α : Type u_1} {F : Type u_5} {G : Type u_6} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup F] [inst_1 : NormedAddCommGroup G] {f : α → F} {g : α → G},
  (∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g x‖) → MeasureTheory.eLpNorm f p μ ≤ MeasureTheory.eLpNorm g p μ
-- Lean.Elab.Do.Basic
Lean.Elab.Do.Context.mk : Lean.Elab.Do.MonadInfo →
  Array Lean.Elab.Do.MutVar →
    Std.HashMap Lean.Name Lean.Elab.Do.MutVar →
      Lean.Expr → Lean.Elab.Do.ContInfoRef → Lean.Elab.Do.CodeLiveness → Lean.Elab.Do.DoOpsRef → Lean.Elab.Do.Context
-- Lean.Meta.FunInfo
_private.Lean.Meta.FunInfo.0.Lean.Meta.instBEqFunInfoEnvCacheKey : BEq Lean.Meta.FunInfoEnvCacheKey✝
-- Mathlib.Analysis.Complex.OperatorNorm
Complex.imCLM_enorm : ‖Complex.imCLM‖ₑ = 1
-- Init.Data.AC
Lean.Data.AC.removeNeutrals.loop.eq_def : ∀ {α : Sort u_1} [info : Lean.Data.AC.ContextInformation α] (ctx : α) (a : List ℕ),
  Lean.Data.AC.removeNeutrals.loop ctx a =
    match a with
    | x :: xs =>
      match Lean.Data.AC.ContextInformation.isNeutral ctx x with
      | true => Lean.Data.AC.removeNeutrals.loop ctx xs
      | false => x :: Lean.Data.AC.removeNeutrals.loop ctx xs
    | [] => []
-- Mathlib.Order.BooleanAlgebra.Set
Set.inter_union_compl : ∀ {α : Type u_1} (s t : Set α), s ∩ t ∪ s ∩ tᶜ = s
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- The scalar multiplication of a `C^n` function and a constant is `C^n`.  -/
ContDiff.smul_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  {A : Type u_4} [inst_5 : NormedRing A] [inst_6 : NormedAlgebra 𝕜 A] [inst_7 : Module A F] [IsScalarTower 𝕜 A F]
  [IsBoundedSMul A F] {f : E → A}, ContDiff 𝕜 n f → ∀ (v : F), ContDiff 𝕜 n fun y => f y • v
-- Std.Do.PredTrans
/-- Adds the ability to make assertions about a state of type `σ` to a predicate transformer with
postcondition shape `ps`, resulting in postcondition shape `.arg σ ps`. This is done by
interpreting `StateT σ (PredTrans ps) α` into `PredTrans (.arg σ ps) α`.

This can be used to for all kinds of state-like effects, including reader effects or append-only
states, by interpreting them as states.
 -/
Std.Do.PredTrans.pushArg : {ps : Std.Do.PostShape} →
  {α σ : Type u} → StateT σ (Std.Do.PredTrans ps) α → Std.Do.PredTrans (Std.Do.PostShape.arg σ ps) α
-- Mathlib.Analysis.Calculus.FDeriv.Add
DifferentiableOn.const_sub : ∀ {𝕜 : 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] {f : E → F}
  {s : Set E}, DifferentiableOn 𝕜 f s → ∀ (c : F), DifferentiableOn 𝕜 (fun y => c - f y) s
-- Mathlib.Topology.Algebra.Valued.NormedValued
Valued.isNonarchimedean_norm : ∀ (L : Type u_1) [inst : Field L] (Γ₀ : Type u_2) [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀]
  [hv : Valued.v.RankOne], IsNonarchimedean fun x => ‖x‖
-- Lean.Data.Json.FromToJson.Basic
/-- Returns the string value or single key name, if any.  -/
Lean.Json.getTag? : Lean.Json → Option String
-- Mathlib.Algebra.Module.Equiv.Basic
/-- The `R`-linear equivalence between additive morphisms `A →+ B` and `ℤ`-linear morphisms `A →ₗ[ℤ] B`.
 -/
addMonoidHomLequivInt : {A : Type u_9} →
  {B : Type u_10} →
    (R : Type u_11) →
      [inst : Semiring R] →
        [inst_1 : AddCommGroup A] → [inst_2 : AddCommGroup B] → [inst_3 : Module R B] → (A →+ B) ≃ₗ[R] A →ₗ[ℤ] B
-- Mathlib.Combinatorics.Matroid.IndepAxioms
IndepMatroid.matroid_IsBase : ∀ {α : Type u_1} (M : IndepMatroid α) (x : Set α), M.matroid.IsBase x = Maximal M.Indep x
-- Mathlib.Dynamics.Ergodic.Conservative
/-- Restriction of a conservative system to an invariant set is a conservative system,
formulated in terms of the restriction of the measure.  -/
MeasureTheory.Conservative.measureRestrict : ∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → α} {s : Set α} {μ : MeasureTheory.Measure α},
  MeasureTheory.Conservative f μ → Set.MapsTo f s s → MeasureTheory.Conservative f (μ.restrict s)
-- Std.Http.Protocol.H1.Error
/-- Request timeout occurred.
 -/
Std.Http.Protocol.H1.Error.timeout : Std.Http.Protocol.H1.Error
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
MeasureTheory.instIsFiniteMeasureForallValNatMemFinsetInducedFamilyOfForallIic : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  (μ : (n : ℕ) → MeasureTheory.Measure ((i : ↥(Finset.Iic n)) → X ↑i)) [∀ (n : ℕ), MeasureTheory.IsFiniteMeasure (μ n)]
  (I : Finset ℕ), MeasureTheory.IsFiniteMeasure (MeasureTheory.inducedFamily μ I)
-- Mathlib.Algebra.Lie.Nilpotent
LieSubmodule.ucs.congr_simp : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M] (k k_1 : ℕ),
  k = k_1 → ∀ (a a_1 : LieSubmodule R L M), a = a_1 → LieSubmodule.ucs k a = LieSubmodule.ucs k_1 a_1
-- Init.GrindInstances.ToInt
Lean.Grind.instLTNatCiOfNatInt : Lean.Grind.ToInt.LT ℕ (Lean.Grind.IntInterval.ci 0)
-- Mathlib.LinearAlgebra.StdBasis
Pi.basis_repr_single : ∀ {R : Type u_2} {η : Type u_4} {ιs : η → Type u_5} {Ms : η → Type u_6} [inst : Semiring R]
  [inst_1 : (i : η) → AddCommMonoid (Ms i)] [inst_2 : (i : η) → Module R (Ms i)] [inst_3 : Fintype η]
  [inst_4 : DecidableEq η] (s : (j : η) → Module.Basis (ιs j) R (Ms j)) (j : η) (i : ιs j),
  (Pi.basis s).repr (Pi.single j ((s j) i)) = fun₀ | ⟨j, i⟩ => 1
-- Init.Grind.Order
Lean.Grind.Order.lt_eq_false_k : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [inst_3 : Std.IsPreorder α]
  [inst_4 : Lean.Grind.Ring α] [Lean.Grind.OrderedRing α] {a : α} {k : ℤ}, k.ble' 0 = true → (a < a + ↑k) = False
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.structureMapLM_eq_of_scalars : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} {i : ℕ} (𝕜' : Type u_5)
  [inst_7 : NontriviallyNormedField 𝕜'] [inst_8 : NormedSpace 𝕜' F] [inst_9 : SMulCommClass ℝ 𝕜' F],
  ⇑(ContDiffMapSupportedIn.structureMapLM 𝕜 n i) = ⇑(ContDiffMapSupportedIn.structureMapLM 𝕜' n i)
-- Std.Http.Data.Status
/-- 205 Reset Content
 -/
Std.Http.Status.resetContent : Std.Http.Status
-- Mathlib.CategoryTheory.Sites.Sieves
/-- the underlying presieve  -/
CategoryTheory.Sieve.arrows : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → {X : C} → CategoryTheory.Sieve X → CategoryTheory.Presieve X
-- Init.Data.SInt.Lemmas
Int32.toNatClampNeg_toISize : ∀ (x : Int32), x.toISize.toNatClampNeg = x.toNatClampNeg
-- Mathlib.Data.Setoid.Basic
Setoid.comap_rel : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (r : Setoid β) (x y : α), (Setoid.comap f r) x y ↔ r (f x) (f y)
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
/-- **Alias** of `MeasureTheory.integral_finsetSum_measure`. -/
MeasureTheory.integral_finset_sum_measure : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {ι : Type u_6}
  {m : MeasurableSpace α} {f : α → G} {μ : ι → MeasureTheory.Measure α} {s : Finset ι},
  (∀ i ∈ s, MeasureTheory.Integrable f (μ i)) → ∫ (a : α), f a ∂∑ i ∈ s, μ i = ∑ i ∈ s, ∫ (a : α), f a ∂μ i
-- Mathlib.GroupTheory.CommutingProbability
commProb_le_one : ∀ (M : Type u_1) [inst : Mul M] [Finite M], commProb M ≤ 1
-- Lean.Elab.Tactic.Try
Lean.Elab.Tactic.Try.TrySuggestionEntry.mk.injEq : ∀ (name : Lean.Name) (prio : ℕ) (name_1 : Lean.Name) (prio_1 : ℕ),
  ({ name := name, prio := prio } = { name := name_1, prio := prio_1 }) = (name = name_1 ∧ prio = prio_1)
-- Mathlib.Order.Interval.Set.OrdConnectedLinear
Set.Nonempty.ordConnected_iff_of_bdd : ∀ {α : Type u_1} {I : Set α} [inst : ConditionallyCompleteLinearOrder α] [LocallyFiniteOrder α],
  I.Nonempty → BddBelow I → BddAbove I → (I.OrdConnected ↔ I = Set.Icc (sInf I) (sSup I))
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.FactorSetMem.eq_1 : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] (s : Associates.FactorSet α) (p : Associates α),
  Associates.FactorSetMem s p = if hp : Irreducible p then Associates.BfactorSetMem ⟨p, hp⟩ s else False
-- Mathlib.FieldTheory.Finite.Basic
/-- If `f` and `g` are quadratic polynomials, then the `f.eval a + g.eval b = 0` has a solution.  -/
FiniteField.exists_root_sum_quadratic : ∀ {R : Type u_2} [inst : CommRing R] [IsDomain R] [inst_2 : Fintype R] {f g : Polynomial R},
  f.degree = 2 → g.degree = 2 → Fintype.card R % 2 = 1 → ∃ a b, Polynomial.eval a f + Polynomial.eval b g = 0
-- Lean.SubExpr
Lean.SubExpr.Pos.pushNaryArg : ℕ → ℕ → Lean.SubExpr.Pos → Lean.SubExpr.Pos
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.instHashableBVBinOp : Hashable Std.Tactic.BVDecide.BVBinOp
-- Mathlib.Order.Filter.Partial
Filter.ptendsto_def : ∀ {α : Type u} {β : Type v} (f : α →. β) (l₁ : Filter α) (l₂ : Filter β),
  Filter.PTendsto f l₁ l₂ ↔ ∀ s ∈ l₂, f.core s ∈ l₁
-- Mathlib.Computability.PartrecCode
_private.Mathlib.Computability.PartrecCode.0.Nat.Partrec.Code.encodeCode.match_1.eq_8 : ∀ (motive : Nat.Partrec.Code → Sort u_1) (cf : Nat.Partrec.Code) (h_1 : Unit → motive Nat.Partrec.Code.zero)
  (h_2 : Unit → motive Nat.Partrec.Code.succ) (h_3 : Unit → motive Nat.Partrec.Code.left)
  (h_4 : Unit → motive Nat.Partrec.Code.right) (h_5 : (cf cg : Nat.Partrec.Code) → motive (cf.pair cg))
  (h_6 : (cf cg : Nat.Partrec.Code) → motive (cf.comp cg)) (h_7 : (cf cg : Nat.Partrec.Code) → motive (cf.prec cg))
  (h_8 : (cf : Nat.Partrec.Code) → motive cf.rfind'),
  (match cf.rfind' with
    | Nat.Partrec.Code.zero => h_1 ()
    | Nat.Partrec.Code.succ => h_2 ()
    | Nat.Partrec.Code.left => h_3 ()
    | Nat.Partrec.Code.right => h_4 ()
    | cf.pair cg => h_5 cf cg
    | cf.comp cg => h_6 cf cg
    | cf.prec cg => h_7 cf cg
    | cf.rfind' => h_8 cf) =
    h_8 cf
-- Mathlib.Analysis.Calculus.Taylor
/-- If `f` is `n` times continuous differentiable on a set `s`, then the Taylor polynomial
`taylorWithinEval f n s x₀ x` is continuous in `x₀`.  -/
continuousOn_taylorWithinEval : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {x : ℝ} {n : ℕ} {s : Set ℝ},
  UniqueDiffOn ℝ s → ContDiffOn ℝ (↑n) f s → ContinuousOn (fun t => taylorWithinEval f n s t x) s
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.eval₂_pUnitAlgEquiv_symm : ∀ {R : Type u_2} {S : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring S] {f : Polynomial R} {φ : R →+* S}
  {a : Unit → S}, MvPolynomial.eval₂ φ a ((MvPolynomial.pUnitAlgEquiv R).symm f) = Polynomial.eval₂ φ (a ()) f
-- Std.Data.DTreeMap.Internal.Operations
/-- A tree map obtained by inserting elements into `t`, bundled with an inductive principle.  -/
Std.DTreeMap.Internal.Impl.Const.IteratedUnitInsertionInto : {α : Type u} → [Ord α] → (Std.DTreeMap.Internal.Impl α fun x => Unit) → Type (max 0 u)
-- Mathlib.RingTheory.AdicCompletion.LocalRing
AdicCompletion.maximalIdeal_eq_map : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsNoetherianRing R] [inst_2 : IsLocalRing R],
  IsLocalRing.maximalIdeal (AdicCompletion (IsLocalRing.maximalIdeal R) R) =
    Ideal.map (algebraMap R (AdicCompletion (IsLocalRing.maximalIdeal R) R)) (IsLocalRing.maximalIdeal R)
-- Mathlib.Probability.Kernel.CondDistrib
/-- `condDistrib` is a.e. uniquely defined as the kernel satisfying the defining property of
`condKernel`.  -/
ProbabilityTheory.condDistrib_ae_eq_of_measure_eq_compProd : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_3 : MeasureTheory.IsFiniteMeasure μ] {Y : α → Ω} {mβ : MeasurableSpace β} (X : α → β),
  AEMeasurable Y μ →
    ∀ {κ : ProbabilityTheory.Kernel β Ω} [ProbabilityTheory.IsFiniteKernel κ],
      MeasureTheory.Measure.map (fun x => (X x, Y x)) μ = (MeasureTheory.Measure.map X μ).compProd κ →
        ⇑(ProbabilityTheory.condDistrib Y X μ) =ᵐ[MeasureTheory.Measure.map X μ] ⇑κ
-- Mathlib.Algebra.CharP.Frobenius
iterateFrobenius_zero : ∀ (R : Type u_1) [inst : CommSemiring R] (p : ℕ) [inst_1 : ExpChar R p], iterateFrobenius R p 0 = RingHom.id R
-- Mathlib.Data.Matrix.Basic
AddMonoidHom.mapMatrix_apply : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_11} {β : Type u_12} [inst : AddZeroClass α] [inst_1 : AddZeroClass β]
  (f : α →+ β) (M : Matrix m n α), f.mapMatrix M = M.map ⇑f
-- Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Real.self_sub_one_le_mul_log : ∀ {x : ℝ}, 0 ≤ x → x - 1 ≤ x * Real.log x
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
/-- Given a group homomorphism `f : G →* H`, this is a natural transformation between the functors
sending `A : Rep k H` to `Hⁿ(H, A)` and to `Hⁿ(G, Res(f)(A))`.  -/
groupCohomology.resNatTrans : (k : Type u) →
  {G H : Type u} →
    [inst : CommRing k] →
      [inst_1 : Group G] →
        [inst_2 : Group H] →
          (f : G →* H) →
            (n : ℕ) → groupCohomology.functor k H n ⟶ (Rep.resFunctor f).comp (groupCohomology.functor k G n)
-- Lean.Language.Lean.Types
Lean.Language.Lean.HeaderProcessedSnapshot.mk : Lean.Language.Snapshot →
  Lean.Language.SnapshotTask Lean.Language.SnapshotLeaf →
    Option Lean.Language.Lean.HeaderProcessedState → Lean.Language.Lean.HeaderProcessedSnapshot
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- A finite, mutually orthogonal family of subspaces of `E`, which span `E`, induce an isometry
from `E` to `PiLp 2` of the subspaces equipped with the `L2` inner product.  -/
DirectSum.IsInternal.isometryL2OfOrthogonalFamily : {ι : Type u_1} →
  {𝕜 : Type u_3} →
    [inst : RCLike 𝕜] →
      {E : Type u_4} →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : InnerProductSpace 𝕜 E] →
            [inst_3 : Fintype ι] →
              [inst_4 : DecidableEq ι] →
                {V : ι → Submodule 𝕜 E} →
                  DirectSum.IsInternal V →
                    (OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ) → E ≃ₗᵢ[𝕜] PiLp 2 fun i => ↥(V i)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get!_eq_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [inst_2 : Inhabited α] {k : α}, k ∈ t → t.get! k = k
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.measurableSet_succ_memPartition : ∀ {α : Type u_1} (t : ℕ → Set α) (n : ℕ) {s : Set α}, s ∈ memPartition t n → MeasurableSet s
-- Mathlib.ModelTheory.Order
FirstOrder.Language.instIsUniversalPartialOrderTheory : ∀ (L : FirstOrder.Language) [inst : L.IsOrdered], L.partialOrderTheory.IsUniversal
-- Aesop.Script.Step
Aesop.Script.LazyStep.BuildInput.mk : {α : Type} →
  Lean.MetaM α → (α → Array Lean.MVarId) → (α → Aesop.Script.TacticBuilder) → Aesop.Script.LazyStep.BuildInput α
-- Mathlib.NumberTheory.LSeries.Convergence
/-- If `F` is a binary operation on `ℕ → ℂ` with the property that the `LSeries` of `F f g`
converges whenever the `LSeries` of `f` and `g` do, then the abscissa of absolute convergence
of `F f g` is at most the maximum of the abscissa of absolute convergence of `f`
and that of `g`.  -/
LSeries.abscissaOfAbsConv_binop_le : ∀ {F : (ℕ → ℂ) → (ℕ → ℂ) → ℕ → ℂ},
  (∀ {f g : ℕ → ℂ} {s : ℂ}, LSeriesSummable f s → LSeriesSummable g s → LSeriesSummable (F f g) s) →
    ∀ (f g : ℕ → ℂ), LSeries.abscissaOfAbsConv (F f g) ≤ max (LSeries.abscissaOfAbsConv f) (LSeries.abscissaOfAbsConv g)
-- Mathlib.Order.Category.Preord
Preord.hom_ext : ∀ {X Y : Preord} {f g : X ⟶ Y}, Preord.Hom.hom f = Preord.Hom.hom g → f = g
-- Init.Data.Iterators.Lemmas.Combinators.Take
_private.Init.Data.Iterators.Lemmas.Combinators.Take.0.Std.Iter.step_take.match_1.eq_2 : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {it : Std.Iter β} (motive : it.Step → Sort u_2) (it' : Std.Iter β)
  (h : it.IsPlausibleStep (Std.IterStep.skip it'))
  (h_1 :
    (it' : Std.Iter β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.Iter β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.skip it', h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_2 it' h
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.curry_natural_right_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {A X Y Y' : C}
  [inst_2 : CategoryTheory.Closed A] (f : CategoryTheory.MonoidalCategoryStruct.tensorObj A X ⟶ Y) (g : Y ⟶ Y') {Z : C}
  (h : A ⟹ Y' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.curry (CategoryTheory.CategoryStruct.comp f g)) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.curry f)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom A).map g) h)
-- Mathlib.CategoryTheory.Action.Continuous
ContAction.resComp_hom : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] {FV : V → V → Type u_2} {CV : V → Type u_3}
  [inst_1 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] [inst_2 : CategoryTheory.ConcreteCategory V FV]
  [inst_3 : CategoryTheory.HasForget₂ V TopCat] {G : Type u_4} [inst_4 : Monoid G] [inst_5 : TopologicalSpace G]
  {H : Type u_5} [inst_6 : Monoid H] [inst_7 : TopologicalSpace H] {K : Type u_6} [inst_8 : Monoid K]
  [inst_9 : TopologicalSpace K] (f : G →ₜ* H) (h : H →ₜ* K),
  (ContAction.resComp V f h).hom =
    { app := fun X => CategoryTheory.CategoryStruct.id ((ContAction.res V (h.comp f)).obj X), naturality := ⋯ }
-- Mathlib.NumberTheory.NumberField.InfiniteAdeleRing
/-- The infinite adele ring of a number field.  -/
NumberField.InfiniteAdeleRing : (K : Type u_1) → [Field K] → Type u_1
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.dblX_of_Y_eq : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} [NoZeroDivisors R] {P Q : Fin 3 → R},
  W'.Equation P →
    P 2 ≠ 0 → Q 2 ≠ 0 → P 0 * Q 2 = Q 0 * P 2 → P 1 * Q 2 = Q 1 * P 2 → P 1 * Q 2 = W'.negY Q * P 2 → W'.dblX P = 0
-- Mathlib.Combinatorics.SetFamily.Compression.Down
/-- Induction principle for finset families. To prove a statement for every finset family,
it suffices to prove it for
* the empty finset family.
* the finset family which only contains the empty finset.
* `{s ∪ {a} | s ∈ 𝒜}` assuming the property for `𝒜` a family of finsets not containing `a`.
* `ℬ ∪ 𝒞` assuming the property for `ℬ` and `𝒞`, where `a` is an element of the ground type and
  `ℬ` is a family of finsets not containing `a` and `𝒞` a family of finsets containing `a`.
  Note that instead of giving `ℬ` and `𝒞`, the `subfamily` case gives you `𝒜 = ℬ ∪ 𝒞`, so that
  `ℬ = {s ∈ 𝒜 | a ∉ s}` and `𝒞 = {s ∈ 𝒜 | a ∈ s}`.

This is a way of formalising induction on `n` where `𝒜` is a finset family on `n` elements.

See also `Finset.memberFamily_induction_on.`  -/
Finset.family_induction_on : ∀ {α : Type u_1} [inst : DecidableEq α] {p : Finset (Finset α) → Prop} (𝒜 : Finset (Finset α)),
  p ∅ →
    p {∅} →
      (∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, (∀ s ∈ 𝒜, a ∉ s) → p 𝒜 → p (Finset.image (insert a) 𝒜)) →
        (∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p ({s ∈ 𝒜 | a ∉ s}) → p ({s ∈ 𝒜 | a ∈ s}) → p 𝒜) → p 𝒜
-- Mathlib.Topology.Sets.Compacts
/-- In an inhabited space, the type of nonempty compact subsets is also inhabited, with
default element the singleton set containing the default element.  -/
TopologicalSpace.NonemptyCompacts.instInhabited : {α : Type u_1} → [inst : TopologicalSpace α] → [Inhabited α] → Inhabited (TopologicalSpace.NonemptyCompacts α)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.trans : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Std.DTreeMap α β cmp},
  t₁.Equiv t₂ → t₂.Equiv t₃ → t₁.Equiv t₃
-- Aesop.Stats.Basic
Aesop.instInhabitedScriptGenerated.default : Aesop.ScriptGenerated
-- Mathlib.Topology.Category.TopCat.Limits.Basic
TopCat.isClosed_iff_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) (X : Set ↑c.pt),
  IsClosed X ↔ ∀ (j : J), IsClosed (⇑(CategoryTheory.ConcreteCategory.hom (c.ι.app j)) ⁻¹' X)
-- Init.Data.Vector.Monadic
_private.Init.Data.Vector.Monadic.0.Vector.forIn'_eq_foldlM.match_1.eq_1 : ∀ {β : 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.yield b with
    | ForInStep.yield b => h_1 b
    | ForInStep.done b => h_2 b) =
    h_1 b
-- Mathlib.Order.Defs.LinearOrder
min_assoc : ∀ {α : Type u_1} [inst : LinearOrder α] (a b c : α), min (min a b) c = min a (min b c)
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
ContinuousLinearMap.rTensor_sub : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} (G : Type u_4) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] (f₁ f₂ : E →L[𝕜] F),
  ContinuousLinearMap.rTensor G (f₁ - f₂) = ContinuousLinearMap.rTensor G f₁ - ContinuousLinearMap.rTensor G f₂
-- Mathlib.Tactic.ReduceModChar
Tactic.ReduceModChar.TypeToCharPResult.intLike.sizeOf_spec : ∀ {u : Lean.Level} {α : Q(Type u)} (n : Q(ℕ)) (instRing : Q(Ring «$α»)) (instCharP : Q(CharP «$α» «$n»)),
  sizeOf (Tactic.ReduceModChar.TypeToCharPResult.intLike n instRing instCharP) =
    1 + sizeOf n + sizeOf instRing + sizeOf instCharP
-- Init.Data.Range.Polymorphic.IntLemmas
Int.map_add_toArray_roo' : ∀ {m n k : ℤ}, Array.map (fun x => k + x) (m<...n).toArray = ((k + m)<...k + n).toArray
-- Mathlib.MeasureTheory.Measure.Dirac
MeasureTheory.Measure.dirac.instIsFiniteMeasure : ∀ {α : Type u_1} [inst : MeasurableSpace α] {a : α}, MeasureTheory.IsFiniteMeasure (MeasureTheory.Measure.dirac a)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.minKeyD_modify : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {f : β → β},
      (Std.DTreeMap.Raw.Const.modify t k f).isEmpty = false →
        ∀ {fallback : α},
          (Std.DTreeMap.Raw.Const.modify t k f).minKeyD fallback =
            if cmp (t.minKeyD fallback) k = Ordering.eq then k else t.minKeyD fallback
-- Init.Data.String.Iterator
/-- Extracts the substring between the positions of two iterators. The first iterator's position is the
start of the substring, and the second iterator's position is the end.

Returns the empty string if the iterators are for different strings, or if the position of the first
iterator is past the position of the second iterator.
 -/
String.Legacy.Iterator.extract : String.Legacy.Iterator → String.Legacy.Iterator → String
-- Init.Data.List.MinMaxOn
List.minOn?_cons : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {x : α}
  {xs : List α}, List.minOn? f (x :: xs) = some ((List.minOn? f xs).elim x (minOn f x))