mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubAddAction.ofFixingAddSubgroup_insert_map_apply : ∀ {M : Type u_1} {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] {a : α}
  {s : Set ↥(SubAddAction.ofStabilizer M a)} {x : α}
  (hx : x ∈ SubAddAction.ofFixingAddSubgroup M (insert a (Subtype.val '' s))),
  ↑↑((SubAddAction.ofFixingAddSubgroup_insert_map a s) ⟨x, hx⟩) = x
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.add_measure : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [TopologicalSpace.PseudoMetrizableSpace β] {ν : MeasureTheory.Measure α} {f : α → β},
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable f ν → MeasureTheory.AEStronglyMeasurable f (μ + ν)
-- Mathlib.RingTheory.Ideal.Cotangent
Ideal.Cotangent.lift_toCotangent : ∀ {R : Type u} [inst : CommRing R] {S : Type u_3} [inst_1 : CommRing S] [inst_2 : Algebra R S] {I : Ideal S}
  {M : Type u_4} [inst_3 : AddCommGroup M] [inst_4 : Module R M] (f : ↥I →ₗ[R] M) (hf : ∀ (x y : ↥I), f (x * y) = 0)
  (x : ↥I), (Ideal.Cotangent.lift f hf) (I.toCotangent x) = f x
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.mem_insertIfNew : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k a : α} {v : β k}, a ∈ m.insertIfNew k v ↔ (k == a) = true ∨ a ∈ m
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.le_floor_iff' : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] {a : R} {n : ℕ}
  [IsStrictOrderedRing R], n ≠ 0 → (n ≤ ⌊a⌋₊ ↔ ↑n ≤ a)
-- Mathlib.Topology.Covering.Quotient
IsQuotientCoveringMap.disjoint : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {G : Type u_3}
  [inst_2 : Group G] [inst_3 : MulAction G E],
  IsQuotientCoveringMap f G → ∀ (e : E), ∃ U ∈ nhds e, ∀ (g : G), ((fun x => g • x) '' U ∩ U).Nonempty → g = 1
-- Mathlib.RingTheory.Localization.Integral
/-- Given a particular witness to an element being algebraic over an algebra `R → S`,
We can localize to a submonoid containing the leading coefficient to make it integral.
Explicitly, the map between the localizations will be an integral ring morphism  -/
is_integral_localization_at_leadingCoeff : ∀ {R : Type u_1} [inst : CommRing R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {Rₘ : Type u_3} {Sₘ : Type u_4} [inst_3 : CommRing Rₘ] [inst_4 : CommRing Sₘ] [inst_5 : Algebra R Rₘ]
  [inst_6 : IsLocalization M Rₘ] [inst_7 : Algebra S Sₘ] [inst_8 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ]
  {x : S} (p : Polynomial R),
  (Polynomial.aeval x) p = 0 →
    p.leadingCoeff ∈ M → (IsLocalization.map Sₘ (algebraMap R S) ⋯).IsIntegralElem ((algebraMap S Sₘ) x)
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Iso.comap_apply : ∀ {V : Type u_1} {W : Type u_2} (f : V ≃ W) (G : SimpleGraph W) (v : V), (SimpleGraph.Iso.comap f G) v = f v
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get?_insertManyIfNewUnit_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtDHashMap α fun x => Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List α} {k : α},
  Std.ExtDHashMap.Const.get? (Std.ExtDHashMap.Const.insertManyIfNewUnit m l) k =
    if k ∈ m ∨ l.contains k = true then some () else none
-- Mathlib.CategoryTheory.Monoidal.Limits.Basic
CategoryTheory.Limits.instLaxMonoidalFunctorLim : {J : Type w} →
  [inst : CategoryTheory.SmallCategory J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.Limits.HasLimitsOfShape J C] →
          [inst_3 : CategoryTheory.MonoidalCategory C] → CategoryTheory.Limits.lim.LaxMonoidal
-- Mathlib.Probability.Distributions.Pareto
ProbabilityTheory.cdf_paretoMeasure_eq_lintegral : ∀ {t r : ℝ},
  0 < t →
    0 < r →
      ∀ (x : ℝ),
        ↑(ProbabilityTheory.cdf (ProbabilityTheory.paretoMeasure t r)) x =
          (∫⁻ (x : ℝ) in Set.Iic x, ProbabilityTheory.paretoPDF t r x).toReal
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
SSet.Subcomplex.Pairing.isUniquelyCodimOneFace : ∀ {X : SSet} {A : X.Subcomplex} (P : A.Pairing) [P.IsProper] (x : ↑P.II), (↑x).IsUniquelyCodimOneFace (↑(P.p x)).toS
-- Mathlib.CategoryTheory.Galois.GaloisObjects
/-- If `X` is Galois, the quotient `X / Aut X` is terminal.  -/
CategoryTheory.PreGaloisCategory.isTerminalQuotientOfIsGalois : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    [inst_1 : CategoryTheory.GaloisCategory C] →
      (X : C) →
        [inst_2 : CategoryTheory.PreGaloisCategory.IsGalois X] →
          CategoryTheory.Limits.IsTerminal
            (CategoryTheory.Limits.colimit (CategoryTheory.SingleObj.functor (CategoryTheory.Aut.toEnd X)))
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.contains_ofList : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [inst : Std.TransCmp cmp] [inst_1 : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List (α × β)} {k : α}, (Std.ExtDTreeMap.Const.ofList l cmp).contains k = (List.map Prod.fst l).contains k
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.mul_apply : ∀ {R : Type u_1} [inst : Semiring R] {f g : ArithmeticFunction R} {n : ℕ},
  (f * g) n = ∑ x ∈ n.divisorsAntidiagonal, f x.1 * g x.2
-- Init.Data.Array.Lemmas
Array.getElem_replicate : ∀ {α : Type u_1} {n : ℕ} {v : α} {i : ℕ} (h : i < (Array.replicate n v).size), (Array.replicate n v)[i] = v
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey!_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k a : α} {v : β k},
  (t.insertIfNew k v).getKey! a = if cmp k a = Ordering.eq ∧ k ∉ t then k else t.getKey! a
-- Mathlib.Data.DFinsupp.Order
DFinsupp.single_nonpos : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] [inst_1 : (i : ι) → Preorder (α i)] {i : ι} {a : α i}
  [inst_2 : DecidableEq ι], (fun₀ | i => a) ≤ 0 ↔ a ≤ 0
-- Mathlib.NumberTheory.Cyclotomic.Gal
/-- `IsCyclotomicExtension.autEquivPow` repackaged in terms of `Gal`.
Asserts that the Galois group of `X ^ n - 1` is equivalent to `(ZMod n)ˣ`
if `cyclotomic n K` is irreducible in the base field.  -/
galXPowEquivUnitsZMod : {n : ℕ} →
  [NeZero n] →
    {K : Type u_1} →
      [inst : Field K] →
        {L : Type u_2} →
          [inst_1 : Field L] →
            [inst_2 : Algebra K L] →
              [IsCyclotomicExtension {n} K L] →
                Irreducible (Polynomial.cyclotomic n K) → (Polynomial.X ^ n - 1).Gal ≃* (ZMod n)ˣ
-- Init.Data.Vector.Int
Vector.prod_replicate_int : ∀ {n : ℕ} {a : ℤ}, (Vector.replicate n a).prod = a ^ n
-- Aesop.Stats.Basic
Aesop.GoalStats.goalId : Aesop.GoalStats → ℕ
-- Mathlib.Analysis.SpecificLimits.Normed
summable_norm_mul_geometric_of_norm_lt_one : ∀ {R : Type u_4} [inst : NormedRing R] {k : ℕ} {r : R},
  ‖r‖ < 1 → ∀ {u : ℕ → ℕ}, ((fun n => ↑(u n)) =O[Filter.atTop] fun n => ↑(n ^ k)) → Summable fun n => ‖↑(u n) * r ^ n‖
-- Mathlib.Tactic.Algebra.Lemmas
Mathlib.Tactic.Algebra.smul_one_eq_smul_one' : ∀ {R : Type u_1} {A : Type u_2} [sR : CommSemiring R] [sA : CommSemiring A] [sAlg : Algebra R A] {r s : R},
  r = s → r • 1 = s • 1
-- Mathlib.Topology.Algebra.Nonarchimedean.Bases
/-- Condition for `B` to be a filter basis on `M`.  -/
RingFilterBasis.SubmodulesBasis.inter : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {BR : RingFilterBasis R} {B : ι → Submodule R M}, BR.SubmodulesBasis B → ∀ (i j : ι), ∃ k, B k ≤ B i ⊓ B j
-- Mathlib.LinearAlgebra.TensorProduct.Submodule
Submodule.mulMap_one_left_eq : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] (N : Submodule R S),
  (Subalgebra.toSubmodule ⊥).mulMap N = N.subtype ∘ₗ ↑N.lTensorOne
-- Init.Try
/-- If `harder` is `true`, more expensive tactics and operations are tried.  -/
Lean.Try.Config.harder : Lean.Try.Config → Bool
-- Batteries.Data.List.Basic
/-- `revzip l` returns a list of pairs of the elements of `l` paired
with the elements of `l` in reverse order.
```
revzip [1, 2, 3, 4, 5] = [(1, 5), (2, 4), (3, 3), (4, 2), (5, 1)]
```
 -/
List.revzip : {α : Type u_1} → List α → List (α × α)
-- Mathlib.Data.Finset.Union
Finset.mem_disjiUnion : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : α → Finset β} {b : β} {h : (↑s).PairwiseDisjoint t},
  b ∈ s.disjiUnion t h ↔ ∃ a ∈ s, b ∈ t a
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.map_bot : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N), Subsemigroup.map f ⊥ = ⊥
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.Integrable.convergenceR.eq_1 : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
  {l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤}
  (h : BoxIntegral.Integrable I l f vol) (ε : ℝ),
  h.convergenceR ε = if hε : 0 < ε then ⋯.choose else fun x x_1 => ⟨1, BoxIntegral.Integrable.convergenceR._proof_2⟩
-- Mathlib.Algebra.Group.Submonoid.Defs
nsmul_mem : ∀ {M : Type u_3} {A : Type u_4} [inst : AddMonoid M] [inst_1 : SetLike A M] [AddSubmonoidClass A M] {S : A} {x : M},
  x ∈ S → ∀ (n : ℕ), n • x ∈ S
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey!_insertIfNew_of_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {k : α} {v : β}, t.isEmpty = true → (t.insertIfNew k v).minKey! = k
-- Mathlib.RingTheory.WittVector.StructurePolynomial
constantCoeff_wittStructureInt_zero : ∀ (p : ℕ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ℤ),
  MvPolynomial.constantCoeff (wittStructureInt p Φ 0) = MvPolynomial.constantCoeff Φ
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.le_rpow_inv_iff : ∀ {x y : ENNReal} {z : ℝ}, 0 < z → (x ≤ y ^ z⁻¹ ↔ x ^ z ≤ y)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.one_mul_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.MonObj M] {Z : C} (f : Z ⟶ M),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.one f)
      CategoryTheory.MonObj.mul =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor Z).hom f
-- Mathlib.Data.Set.Prod
Set.eval_image_univ_pi : ∀ {ι : Type u_1} {α : ι → Type u_2} {t : (i : ι) → Set (α i)} {i : ι},
  (Set.univ.pi t).Nonempty → (fun f => f i) '' Set.univ.pi t = t i
-- Mathlib.Order.RelClasses
/-- Set notation form of `le_antisymm_iff` -/
subset_antisymm_iff : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : PartialOrder α] {a b : α}, a = b ↔ a ⊆ b ∧ b ⊆ a
-- Mathlib.Algebra.Category.Grp.FilteredColimits
AddCommGrpCat.FilteredColimits.colimitAddCommGroup.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J AddCommGrpCat),
  AddCommGrpCat.FilteredColimits.colimitAddCommGroup F =
    { toAddGroup := (AddCommGrpCat.FilteredColimits.G F).str, add_comm := ⋯ }
-- Init.Data.List.Nat.InsertIdx
List.insertIdx_zero : ∀ {α : Type u} {xs : List α} {x : α}, xs.insertIdx 0 x = x :: xs
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.comp_left_assoc : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} (a b c : CategoryTheory.Over X) (f : a ⟶ b)
  (g : b ⟶ c) {Z : T} (h : c.left ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (CategoryTheory.CategoryStruct.comp f g)) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left g) h)
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
DifferentiableOn.cexp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAlgebra 𝕜 ℂ] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {f : E → ℂ} {s : Set E},
  DifferentiableOn 𝕜 f s → DifferentiableOn 𝕜 (fun x => Complex.exp (f x)) s
-- Mathlib.Data.Rel
SetRel.inv_empty : ∀ {α : Type u_1} {β : Type u_2}, ∅.inv = ∅
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.limitProcess.eq_1 : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {E : Type u_4} [inst_1 : Zero E]
  [inst_2 : TopologicalSpace E] (f : ι → Ω → E) (ℱ : MeasureTheory.Filtration ι m) (μ : MeasureTheory.Measure Ω),
  MeasureTheory.Filtration.limitProcess f ℱ μ =
    if h :
        ∃ g,
          MeasureTheory.StronglyMeasurable g ∧
            ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun n => f n ω) Filter.atTop (nhds (g ω)) then
      Classical.choose h
    else 0
-- Mathlib.Logic.Function.Basic
Function.sometimes_eq : ∀ {p : Prop} {α : Sort u_1} [inst : Nonempty α] (f : p → α) (a : p), Function.sometimes f = f a
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.tendsto_densityProcess_atTop_of_antitone : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] (κ : ProbabilityTheory.Kernel α (γ × β))
  (ν : ProbabilityTheory.Kernel α γ) [ProbabilityTheory.IsFiniteKernel κ] (n : ℕ) (a : α) (x : γ) (seq : ℕ → Set β),
  Antitone seq →
    ⋂ i, seq i = ∅ →
      (∀ (m : ℕ), MeasurableSet (seq m)) →
        Filter.Tendsto (fun m => κ.densityProcess ν n a x (seq m)) Filter.atTop (nhds 0)
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroupClass.inclusion_mk : ∀ {G : Type u_1} [inst : AddGroup G] {S : Type u_4} {H K : S} [inst_1 : SetLike S G] [inst_2 : AddSubgroupClass S G]
  [inst_3 : LE S] [inst_4 : IsConcreteLE S G] {h : H ≤ K} (x : G) (hx : x ∈ H),
  (AddSubgroupClass.inclusion h) ⟨x, hx⟩ = ⟨x, ⋯⟩
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.orderOf : ∀ {M : Type u_1} [inst : CommMonoid M] (ζ : M), IsPrimitiveRoot ζ (orderOf ζ)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.instLawfulMonad : LawfulMonad FreeGroup
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
CFC.spectrum_zero_eq : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] [Nontrivial A],
  spectrum R 0 = {0}
-- Init.Data.String.Lemmas.Slice
String.Slice.beq_eq_false_iff : ∀ {s t : String.Slice}, (s == t) = false ↔ s.copy ≠ t.copy
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.Products.eval_πs' : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I]
  {l : Profinite.NobelingProof.Products I} {o₁ o₂ : Ordinal.{u}} (h : o₁ ≤ o₂),
  (∀ i ∈ ↑l, Profinite.NobelingProof.ord I i < o₁) →
    (Profinite.NobelingProof.πs' C h)
        (Profinite.NobelingProof.Products.eval
          (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o₁) l) =
      Profinite.NobelingProof.Products.eval (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o₂)
        l
-- Mathlib.Tactic.NormNum.Result
/-- The result is `proof : IsRat x n d`,
where `n` is `.negOfNat lit` with `lit` a raw nat literal,
`d` is a raw nat literal (not 0 or 1),
`n` and `d` are coprime, and `q` is the value of `n / d`.  -/
Mathlib.Meta.NormNum.Result.isNegNNRat : {u : Lean.Level} →
  {α : Q(Type u)} →
    {x : Q(«$α»)} →
      (inst : autoParam Q(DivisionRing «$α») Mathlib.Meta.NormNum.Result.isNegNNRat._auto_1) →
        ℚ → (n d : Q(ℕ)) → Q(Mathlib.Meta.NormNum.IsRat «$x» (Int.negOfNat «$n») «$d») → Mathlib.Meta.NormNum.Result x
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip
Std.IterM.step_intermediateZip : ∀ {α₁ α₂ β₁ β₂ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α₁ m β₁]
  [inst_2 : Std.Iterator α₂ m β₂] {it₁ : Std.IterM m β₁} {memo : Option { out // ∃ it, it.IsPlausibleOutput out }}
  {it₂ : Std.IterM m β₂},
  (Std.IterM.Intermediate.zip it₁ memo it₂).step =
    match memo with
    | none => do
      let __do_lift ← it₁.step
      match __do_lift.inflate with
        | ⟨Std.IterStep.yield it₁' out, hp⟩ =>
          pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.Intermediate.zip it₁' (some ⟨out, ⋯⟩) it₂) ⋯))
        | ⟨Std.IterStep.skip it₁', hp⟩ =>
          pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.Intermediate.zip it₁' none it₂) ⋯))
        | ⟨Std.IterStep.done, hp⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.done ⋯))
    | some out₁ => do
      let __do_lift ← it₂.step
      match __do_lift.inflate with
        | ⟨Std.IterStep.yield it₂' out₂, hp⟩ =>
          pure
            (Std.Shrink.deflate
              (Std.PlausibleIterStep.yield (Std.IterM.Intermediate.zip it₁ none it₂') (↑out₁, out₂) ⋯))
        | ⟨Std.IterStep.skip it₂', hp⟩ =>
          pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.Intermediate.zip it₁ (some out₁) it₂') ⋯))
        | ⟨Std.IterStep.done, hp⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.done ⋯))
-- Mathlib.FieldTheory.SeparableClosure
IntermediateField.finInsepDegree_bot' : ∀ {F : Type u} (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type w) [inst_3 : Field K]
  [inst_4 : Algebra F K] [inst_5 : Algebra E K] [inst_6 : IsScalarTower F E K],
  Field.finInsepDegree F ↥⊥ = Field.finInsepDegree F E
-- Std.Http.Data.Headers
/-- Creates headers from a list of key-value pairs.
 -/
Std.Http.Headers.ofList : List (Std.Http.Header.Name × Std.Http.Header.Value) → Std.Http.Headers
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.ThinSkeleton.map_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : CategoryTheory.ThinSkeleton C} (a : X ⟶ Y),
  (CategoryTheory.ThinSkeleton.map F).map a =
    Quotient.recOnSubsingleton₂ (motive := fun x x_1 => (x ⟶ x_1) → (Quotient.map F.obj ⋯ x ⟶ Quotient.map F.obj ⋯ x_1))
      X Y (fun x x_1 k => CategoryTheory.homOfLE ⋯) a
-- Mathlib.Algebra.GroupWithZero.Defs
CancelMonoidWithZero.mk.sizeOf_spec : ∀ {M₀ : Type u_2} [inst : SizeOf M₀] (toMonoidWithZero : MonoidWithZero M₀) (toIsCancelMulZero : IsCancelMulZero M₀),
  sizeOf { toMonoidWithZero := toMonoidWithZero, toIsCancelMulZero := toIsCancelMulZero } =
    1 + sizeOf toMonoidWithZero + sizeOf toIsCancelMulZero
-- Mathlib.Analysis.RCLike.Basic
RCLike.nonpos_iff_exists_ofReal : ∀ {K : Type u_1} [inst : RCLike K] {z : K}, z ≤ 0 ↔ ∃ x ≤ 0, ↑x = z
-- Init.Data.Int.OfNat
Nat.ToInt.of_not_le : ∀ {a b : ℕ} {a' b' : ℤ}, ↑a = a' → ↑b = b' → ¬a ≤ b → b' + 1 ≤ a'
-- Mathlib.NumberTheory.BernoulliPolynomials
Polynomial.sum_bernoulli : ∀ (n : ℕ), ∑ k ∈ Finset.range (n + 1), ↑((n + 1).choose k) • Polynomial.bernoulli k = (Polynomial.monomial n) (↑n + 1)
-- Mathlib.Order.Filter.Pointwise
Filter.inv_eq_bot_iff : ∀ {α : Type u_2} [inst : Inv α] {f : Filter α}, f⁻¹ = ⊥ ↔ f = ⊥
-- Mathlib.Probability.Independence.Kernel.IndepFun
/-- If `f` is a family of mutually independent random variables (`iIndepFun m f μ`) and `S, T` are
two disjoint finite index sets, then the tuple formed by `f i` for `i ∈ S` is independent of the
tuple `(f i)_i` for `i ∈ T`.  -/
ProbabilityTheory.Kernel.iIndepFun.indepFun_finset : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : ι → Type u_8}
  {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ω → β i} (S T : Finset ι),
  Disjoint S T →
    ProbabilityTheory.Kernel.iIndepFun f κ μ →
      (∀ (i : ι), Measurable (f i)) → ProbabilityTheory.Kernel.IndepFun (fun a i => f (↑i) a) (fun a i => f (↑i) a) κ μ
-- Mathlib.Geometry.Euclidean.Sphere.OrthRadius
EuclideanGeometry.Sphere.orthRadius_eq_orthRadius_iff : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p q : P}, s.orthRadius p = s.orthRadius q ↔ p = q
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.Measure.FiniteAtFilter.filter_mono_ae : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : Filter α},
  f ⊓ MeasureTheory.ae μ ≤ g → μ.FiniteAtFilter g → μ.FiniteAtFilter f
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
/-- **Alias** of the reverse direction of `Subgroup.normal_op`. -/
Subgroup.Normal.op : ∀ {G : Type u_2} [inst : Group G] {H : Subgroup G}, H.Normal → H.op.Normal
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Functor.obj.ε_def : ∀ {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 : CategoryTheory.Functor C D) [inst_4 : F.OplaxMonoidal] (X : C) [inst_5 : CategoryTheory.ComonObj X],
  CategoryTheory.ComonObj.counit =
    CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.ComonObj.counit) (CategoryTheory.Functor.OplaxMonoidal.η F)
-- Mathlib.Algebra.Order.Interval.Set.SuccPred
Set.Icc_add_one_sub_one_eq_Ioo : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : Add α] [inst_3 : Sub α] [SuccAddOrder α]
  [PredSubOrder α] [Nontrivial α] (a b : α), Set.Icc (a + 1) (b - 1) = Set.Ioo a b
-- Mathlib.Data.Fin.SuccPred
Fin.predAbove_succ_of_le : ∀ {n : ℕ} (p i : Fin n), p ≤ i → p.predAbove i.succ = i
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
/-- The square with `0 : 0 ⟶ 0` on the bottom and `𝟙 X` on the top is a pullback square.  -/
CategoryTheory.IsPullback.zero_bot : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X : C),
  CategoryTheory.IsPullback (CategoryTheory.CategoryStruct.id X) 0 0 0
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
Topology.IsClosedEmbedding.continuousOn_comap_finiteMeasure : ∀ {Ω : Type u_1} {Ω' : Type u_2} [inst : MeasurableSpace Ω] [inst_1 : MeasurableSpace Ω'] [inst_2 : TopologicalSpace Ω]
  [inst_3 : TopologicalSpace Ω'] [inst_4 : BorelSpace Ω] [inst_5 : BorelSpace Ω'] [NormalSpace Ω'] {f : Ω → Ω'},
  Topology.IsClosedEmbedding f →
    ContinuousOn (fun μ => MeasureTheory.FiniteMeasure.comap f μ) {μ | μ (Set.range f)ᶜ = 0}
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.unit_smul_eq_iff_mul_eq : ∀ {K : Type u_1} [inst : Field K] [NumberField K] {x y : NumberField.RingOfIntegers K}
  {u : (NumberField.RingOfIntegers K)ˣ},
  u • (NumberField.mixedEmbedding K) ↑x = (NumberField.mixedEmbedding K) ↑y ↔ ↑u * x = y
-- Aesop.RuleSet.Member
Aesop.instInhabitedGlobalRuleSetMember : Inhabited Aesop.GlobalRuleSetMember
-- Std.Data.DTreeMap.Raw.WF
Std.DTreeMap.Raw.WF.constOfList : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] {l : List (α × β)},
  (Std.DTreeMap.Raw.Const.ofList l cmp).WF
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rcc_add_succ_right_eq_push' : ∀ {m n : ℕ}, (m...=m + (n + 1)).toArray = (m...=m + n).toArray.push (m + n + 1)
-- Mathlib.Data.List.Sublists
List.mem_sublistsLen_self : ∀ {α : Type u} {l l' : List α}, l'.Sublist l → l' ∈ List.sublistsLen l'.length l
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.basicOpen_zero : ∀ (X : AlgebraicGeometry.Scheme) (U : X.Opens), X.basicOpen 0 = ⊥
-- Mathlib.Data.Int.SuccPred
Int.natCast_covBy : ∀ {a b : ℕ}, ↑a ⋖ ↑b ↔ a ⋖ b
-- Mathlib.Order.Partition.Finpartition
/-- A `Finpartition` constructor from a bigger existing finpartition.  -/
Finpartition.ofSubset : {α : Type u_1} →
  [inst : Lattice α] →
    [inst_1 : OrderBot α] →
      {a b : α} → (P : Finpartition a) → {parts : Finset α} → parts ⊆ P.parts → parts.sup id = b → Finpartition b