mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Matrix.toLinearEquiv'_symm_apply : ∀ {n : Type u_1} [inst : Fintype n] {R : Type u_2} [inst_1 : CommRing R] [inst_2 : DecidableEq n] (P : Matrix n n R)
  (h : Invertible P), ↑(P.toLinearEquiv' h).symm = Matrix.toLin' ⅟P
-- Mathlib.Computability.Primrec.Basic
Primrec.ofNat : ∀ (α : Type u_4) [inst : Denumerable α], Primrec (Denumerable.ofNat α)
-- Lean.Meta.Sym.Apply
/-- The theorem used to create the rule. It is often of the form `Expr.const declName`.  -/
Lean.Meta.Sym.BackwardRule.expr : Lean.Meta.Sym.BackwardRule → Lean.Expr
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.toPullback_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) {i₁ i₂ : E.I₀}
  [inst_1 : CategoryTheory.Limits.HasPullback (E.f i₁) (E.f i₂)] (k : E.I₁ i₁ i₂),
  CategoryTheory.CategoryStruct.comp (E.toPullback k) (CategoryTheory.Limits.pullback.fst (E.f i₁) (E.f i₂)) = E.p₁ k
-- Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
rpow_mul_exp_neg_mul_rpow_isLittleO_exp_neg : ∀ (s : ℝ) {b p : ℝ},
  1 < p → 0 < b → (fun x => x ^ s * Real.exp (-b * x ^ p)) =o[Filter.atTop] fun x => Real.exp (-(1 / 2) * x)
-- Mathlib.Data.Seq.Computation
Computation.LiftRel.symm : ∀ {α : Type u} (R : α → α → Prop) [Std.Symm R], Std.Symm (Computation.LiftRel R)
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.nullMeasurable_comp_snd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν]
  [NeZero μ] {f : β → γ}, MeasureTheory.NullMeasurable (f ∘ Prod.snd) (μ.prod ν) ↔ MeasureTheory.NullMeasurable f ν
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.inter_mul_union_subset_union : ∀ {α : Type u_2} [inst : Mul α] {s₁ s₂ t₁ t₂ : Set α}, s₁ ∩ s₂ * (t₁ ∪ t₂) ⊆ s₁ * t₁ ∪ s₂ * t₂
-- Mathlib.CategoryTheory.Shift.CommShift
/-- If `τ : F₁ ⟶ F₂` is a natural transformation between two functors
which commute with a shift by an additive monoid `A`, this typeclass
asserts a compatibility of `τ` with these shifts.  -/
CategoryTheory.NatTrans.CommShift : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {F₁ F₂ : CategoryTheory.Functor C D} →
          (F₁ ⟶ F₂) →
            (A : Type u_5) →
              [inst_2 : AddMonoid A] →
                [inst_3 : CategoryTheory.HasShift C A] →
                  [inst_4 : CategoryTheory.HasShift D A] → [F₁.CommShift A] → [F₂.CommShift A] → Prop
-- Init.Data.UInt.Lemmas
UInt64.toUSize_ofFin : ∀ (n : Fin UInt64.size), (UInt64.ofFin n).toUSize = USize.ofNat ↑n
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.map'_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MulOneClass α] [inst_1 : MulOneClass β] [inst_2 : MulOneClass γ]
  (f : α →* β) (g : β →* γ), WithZero.map' (g.comp f) = (WithZero.map' g).comp (WithZero.map' f)
-- Mathlib.Order.Filter.Prod
Filter.disjoint_prod : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} {f' : Filter α} {g' : Filter β},
  Disjoint (f ×ˢ g) (f' ×ˢ g') ↔ Disjoint f f' ∨ Disjoint g g'
-- Mathlib.Order.GaloisConnection.Defs
GaloisConnection.u_eq_top : ∀ {α : Type u} {β : Type v} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : OrderTop α] {l : α → β} {u : β → α},
  GaloisConnection l u → ∀ {x : β}, u x = ⊤ ↔ l ⊤ ≤ x
-- Batteries.CodeAction.Misc
/-- Constructs a hole with a kind matching the provided hole elaborator.   -/
Batteries.CodeAction.holeKindToHoleString : Lean.Name → String → String
-- Mathlib.RingTheory.WittVector.FrobeniusFractionField
/-- Recursively defines the sequence of coefficients for `WittVector.frobeniusRotation`.  -/
WittVector.frobeniusRotationCoeff : (p : ℕ) →
  [hp : Fact (Nat.Prime p)] →
    {k : Type u_1} →
      [inst : Field k] →
        [CharP k p] → [IsAlgClosed k] → {a₁ a₂ : WittVector p k} → a₁.coeff 0 ≠ 0 → a₂.coeff 0 ≠ 0 → ℕ → k
-- Mathlib.Data.PNat.Basic
instDistribPNat : Distrib ℕ+
-- Mathlib.RepresentationTheory.Invariants
Representation.mem_invariants_iff_of_forall_mem_zpowers : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommRing k] [inst_1 : Group G] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] (ρ : Representation k G V) (g : G),
  (∀ (x : G), x ∈ Subgroup.zpowers g) → ∀ (x : V), x ∈ ρ.invariants ↔ (ρ g) x = x
-- Lean.Parser.Command
Lean.Parser.Command.structFields.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic
/-- A localizer morphism `Φ : LocalizerMorphism W₁ W₂` is a left derivability
structure if it has left resolutions and the 2-square where the top and bottom functors
are localization functors for `W₁` and `W₂` is Guitart exact.  -/
CategoryTheory.LocalizerMorphism.IsLeftDerivabilityStructure : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
        {W₁ : CategoryTheory.MorphismProperty C₁} →
          {W₂ : CategoryTheory.MorphismProperty C₂} → CategoryTheory.LocalizerMorphism W₁ W₂ → Prop
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.combine.go.eq_def : ∀ (fuel : ℕ) (p₁ p₂ : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.combine.go fuel p₁ p₂ =
    match fuel with
    | 0 => p₁.concat p₂
    | fuel.succ =>
      match p₁, p₂ with
      | Lean.Grind.CommRing.Poly.num k₁, Lean.Grind.CommRing.Poly.num k₂ => Lean.Grind.CommRing.Poly.num (k₁ + k₂)
      | Lean.Grind.CommRing.Poly.num k₁, Lean.Grind.CommRing.Poly.add k₂ m₂ p₂ =>
        (Lean.Grind.CommRing.Poly.add k₂ m₂ p₂).addConst k₁
      | Lean.Grind.CommRing.Poly.add k₁ m₁ p₁, Lean.Grind.CommRing.Poly.num k₂ =>
        (Lean.Grind.CommRing.Poly.add k₁ m₁ p₁).addConst k₂
      | Lean.Grind.CommRing.Poly.add k₁ m₁ p₁, Lean.Grind.CommRing.Poly.add k₂ m₂ p₂ =>
        match m₁.grevlex m₂ with
        | Ordering.eq =>
          have k := k₁ + k₂;
          bif k == 0 then Lean.Grind.CommRing.Poly.combine.go fuel p₁ p₂
          else Lean.Grind.CommRing.Poly.add k m₁ (Lean.Grind.CommRing.Poly.combine.go fuel p₁ p₂)
        | Ordering.gt =>
          Lean.Grind.CommRing.Poly.add k₁ m₁
            (Lean.Grind.CommRing.Poly.combine.go fuel p₁ (Lean.Grind.CommRing.Poly.add k₂ m₂ p₂))
        | Ordering.lt =>
          Lean.Grind.CommRing.Poly.add k₂ m₂
            (Lean.Grind.CommRing.Poly.combine.go fuel (Lean.Grind.CommRing.Poly.add k₁ m₁ p₁) p₂)
-- Mathlib.Tactic.IntervalCases
/-- Given `(z1, e1, p1)` a lower bound on `e` and `(z2, e2, p2)` an upper bound on `e`, such that the
distance between the bounds matches the number of `cases` in the subarray (which must be positive),
proves the goal `g` using the metavariables in the array by recursive bisection.
This is the core of the tactic, producing a case tree of if statements which bottoms out
at the `cases`.
 -/
Mathlib.Tactic.IntervalCases.Methods.bisect : Mathlib.Tactic.IntervalCases.Methods →
  Lean.MVarId →
    Subarray Mathlib.Tactic.IntervalCases.IntervalCasesSubgoal →
      Mathlib.Tactic.IntervalCases.Bound →
        Mathlib.Tactic.IntervalCases.Bound → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.MetaM Unit
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.real_toNNReal : ∀ {α : Type u_1} {x : MeasurableSpace α} {f : α → ℝ},
  MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable fun x => (f x).toNNReal
-- Mathlib.CategoryTheory.FinCategory.Basic
/-- The opposite of a finite category is finite.
 -/
CategoryTheory.finCategoryOpposite : {J : Type v} → [inst : CategoryTheory.SmallCategory J] → [CategoryTheory.FinCategory J] → CategoryTheory.FinCategory Jᵒᵖ
-- Mathlib.Tactic.Relation.Rfl
/-- This tactic applies to a goal whose target has the form `x ~ x`, where `~` is a reflexive
relation, that is, a relation which has a reflexive lemma tagged with the attribute `@[refl]`.
 -/
Mathlib.Tactic.rflTac : Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Topology.Order.Compact
IsCompact.lt_sInf_iff_of_continuous : ∀ {α : Type u_2} {β : Type u_3} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
  [inst_2 : TopologicalSpace β] [ClosedIicTopology α] {f : β → α} {K : Set β},
  IsCompact K → K.Nonempty → ContinuousOn f K → ∀ (y : α), y < sInf (f '' K) ↔ ∀ x ∈ K, y < f x
-- Mathlib.Topology.Hom.Open
ContinuousOpenMap.coe_id : ∀ (α : Type u_2) [inst : TopologicalSpace α], ⇑(ContinuousOpenMap.id α) = id
-- Mathlib.Order.InitialSeg
PrincipalSeg.image_Iio : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder β] [inst_1 : PartialOrder α] (f : α <i β) (a : α),
  ⇑f.toRelEmbedding '' Set.Iio a = Set.Iio (f.toRelEmbedding a)
-- Init.Data.BitVec.Bitblast
/-- A lawful DivModState implies `w > 0`.  -/
BitVec.DivModState.Lawful.hw : ∀ {w : ℕ} {args : BitVec.DivModArgs w} {qr : BitVec.DivModState w} {h : BitVec.DivModState.Lawful args qr}, 0 < w
-- Mathlib.Algebra.Group.Action.Opposite
VAddAssocClass.opposite_mid : ∀ {M : Type u_5} {N : Type u_6} [inst : Add N] [inst_1 : VAdd M N] [VAddCommClass M N N], VAddAssocClass M Nᵃᵒᵖ N
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.intEquivalence_inverse_obj : ∀ (A : RingCat), AlgCat.intEquivalence.inverse.obj A = AlgCat.of ℤ ↑A
-- Mathlib.Data.Num.Basic
znumCoe : {α : Type u_1} → [Zero α] → [One α] → [Add α] → [Neg α] → CoeHTCT ZNum α
-- Init.Data.Vector.Lemmas
Vector.countP_toList : ∀ {α : Type u_1} {n : ℕ} {p : α → Bool} {xs : Vector α n}, List.countP p xs.toList = Vector.countP p xs
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.add_mul : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_5} {l : Type u_7} [inst : Fintype m] [inst_1 : NonUnitalNonAssocSemiring A]
  (L M : CStarMatrix l m A) (N : CStarMatrix m n A), (L + M) * N = L * N + M * N
-- Mathlib.LinearAlgebra.Finsupp.VectorSpace
MonoidAlgebra.instFree : ∀ {M : Type u_1} {R : Type u_2} {S : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Module R S]
  [Module.Free R S], Module.Free R (MonoidAlgebra S M)
-- Mathlib.Algebra.Group.Commute.Defs
/-- If `a` commutes with both `b` and `c`, then it commutes with their sum.  -/
AddCommute.add_right : ∀ {S : Type u_3} [inst : AddSemigroup S] {a b c : S}, AddCommute a b → AddCommute a c → AddCommute a (b + c)
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.eq_mk_support : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] (f : Π₀ (i : ι), β i), f = DFinsupp.mk f.support fun i => f ↑i
-- Mathlib.CategoryTheory.Limits.Indization.ParallelPair
/-- Structure containing data exhibiting two parallel natural transformations `f` and `g` between
presheaves `A` and `B` as induced by a natural transformation in a functor category exhibiting
`A` and `B` as ind-objects.  -/
CategoryTheory.IndParallelPairPresentation : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} → (A ⟶ B) → (A ⟶ B) → Type (max u₁ (v₁ + 1))
-- Lean.Elab.PreDefinition.WF.Eqns
Lean.Elab.WF.EqnInfo.mk : Lean.Name →
  List Lean.Name →
    Lean.Expr →
      Lean.Expr → Array Lean.Name → Lean.Name → Lean.Meta.ArgsPacker → Lean.Elab.FixedParamPerms → Lean.Elab.WF.EqnInfo
-- Lean.Widget.Diff
/-- Map from subexpr positions in `e₀` to diff points. -/
_private.Lean.Widget.Diff.0.Lean.Widget.ExprDiff.changesBefore : Lean.Widget.ExprDiff✝ → Lean.SubExpr.PosMap Lean.Widget.ExprDiffTag✝
-- Mathlib.Topology.Compactness.Compact
Filter.cocompact_neBot_iff : ∀ {X : Type u} [inst : TopologicalSpace X], (Filter.cocompact X).NeBot ↔ NoncompactSpace X
-- Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
/-- When `j` is a limit element, and `x` is a compatible family of elements
in `F.obj (op i)` for all `i < j`, this is a lifting to `F.obj (op j)`.  -/
CategoryTheory.Functor.WellOrderInductionData.lift : {J : Type u} →
  [inst : LinearOrder J] →
    [inst_1 : SuccOrder J] →
      {F : CategoryTheory.Functor Jᵒᵖ (Type v)} →
        F.WellOrderInductionData →
          (j : J) → Order.IsSuccLimit j → ↑(⋯.functor.op.comp F).sections → F.obj (Opposite.op j)
-- Mathlib.Data.List.AList
/-- `AList β` is a key-value map stored as a `List` (i.e. a linked list).
It is a wrapper around certain `List` functions with the added constraint
that the list have unique keys.  -/
AList : {α : Type u} → (α → Type v) → Type (max u v)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
Lean.Meta.Grind.Arith.CommRing.RingM.Context.ringId : Lean.Meta.Grind.Arith.CommRing.RingM.Context → ℕ
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakKernels
/-- Any morphism `k : W ⟶ X` satisfying `k ≫ f = 0` induces a morphism `l : W ⟶ weakKernel f`
such that `l ≫ weakKernel.ι f = k`.  -/
CategoryTheory.Limits.weakKernel.lift' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        (f : X ⟶ Y) →
          [inst_2 : CategoryTheory.Limits.HasWeakKernel f] →
            {W : C} →
              (k : W ⟶ X) →
                CategoryTheory.CategoryStruct.comp k f = 0 →
                  { l // CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.weakKernel.ι f) = k }
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_rcc_ne_empty_iff : ∀ {m n : ℤ}, (m...=n).toArray ≠ #[] ↔ m ≤ n
-- Mathlib.Logic.Equiv.Basic
Equiv.piCongr.eq_1 : ∀ {α : Sort u_1} {β : Sort u_4} {W : α → Sort w} {Z : β → Sort z} (h₁ : α ≃ β) (h₂ : (a : α) → W a ≃ Z (h₁ a)),
  h₁.piCongr h₂ = (Equiv.piCongrRight h₂).trans (Equiv.piCongrLeft Z h₁)
-- Mathlib.Logic.Encodable.Basic
/-- Explicit encoding function for a decidable subtype of an encodable type  -/
Encodable.encodeSubtype : {α : Type u_1} → {P : α → Prop} → [encA : Encodable α] → { a // P a } → ℕ
-- Init.Data.Float.Model.Float
Float.instDecidableEqModel : DecidableEq Float.Model
-- Mathlib.Order.SuccPred.Limit
Order.IsPredLimit.mk : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, ¬IsMax a → Order.IsPredPrelimit a → Order.IsPredLimit a
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.contains'.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α → Ordering),
  Std.DTreeMap.Internal.Impl.contains' k Std.DTreeMap.Internal.Impl.leaf = false
-- Mathlib.Topology.Sets.OpenCover
TopologicalSpace.IsOpenCover.mk : ∀ {ι : Type u_1} {X : Type u_3} [inst : TopologicalSpace X] {u : ι → TopologicalSpace.Opens X},
  iSup u = ⊤ → TopologicalSpace.IsOpenCover u
-- Init.System.IOError
IO.Error.mkResourceBusy : UInt32 → String → IO.Error
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.WithLower.toLower_lt_toLower : ∀ {α : Type u_1} [inst : Preorder α] {x y : α}, Topology.WithLower.toLower x < Topology.WithLower.toLower y ↔ x < y
-- Mathlib.Data.ENNReal.Action
ENNReal.smul_toNNReal : ∀ (a : NNReal) (b : ENNReal), (a • b).toNNReal = a * b.toNNReal
-- Mathlib.Data.Int.Bitwise
Int.ldiff.eq_3 : ∀ (m n : ℕ), (Int.negSucc m).ldiff (Int.ofNat n) = Int.negSucc (m ||| n)
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.ext : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {X : CategoryTheory.SimplicialObject.Augmented C}
  {x y : X.ExtraDegeneracy}, x.s' = y.s' → x.s = y.s → x = y
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
CochainComplex.XIsoOfEq_shift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : CochainComplex C ℤ) (n : ℤ) {p q : ℤ} (hpq : p = q),
  HomologicalComplex.XIsoOfEq ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K) hpq =
    HomologicalComplex.XIsoOfEq K ⋯
-- Mathlib.CategoryTheory.GuitartExact.VerticalComposition
/-- Given `w : TwoSquare T L R B`, one may obtain a 2-square `TwoSquare T L' R' B` if we
provide natural transformations `α : L ⟶ L'` and `β : R' ⟶ R`.  -/
CategoryTheory.TwoSquare.whiskerVertical : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D₁ : Type u_4} →
      {D₂ : Type u_5} →
        [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
            [inst_2 : CategoryTheory.Category.{v_4, u_4} D₁] →
              [inst_3 : CategoryTheory.Category.{v_5, u_5} D₂] →
                {T : CategoryTheory.Functor C₁ D₁} →
                  {L : CategoryTheory.Functor C₁ C₂} →
                    {R : CategoryTheory.Functor D₁ D₂} →
                      {B : CategoryTheory.Functor C₂ D₂} →
                        CategoryTheory.TwoSquare T L R B →
                          {L' : CategoryTheory.Functor C₁ C₂} →
                            {R' : CategoryTheory.Functor D₁ D₂} →
                              (L ⟶ L') → (R' ⟶ R) → CategoryTheory.TwoSquare T L' R' B
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxo.Iterator.instIteratorLoop.loop.wf.eq_def : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLT α] {n : Type u → Type w}
  [inst_5 : Monad n] (γ : Type u) (Pl : α → γ → ForInStep γ → Prop)
  (wf : Std.IteratorLoop.WellFounded (Std.Rxo.Iterator α) Id Pl) (LargeEnough : α → Prop)
  (hl : ∀ (a b : α), Std.PRange.UpwardEnumerable.LE a b → LargeEnough a → LargeEnough b) (upperBound : α) (acc : γ)
  (next : α) (h : LargeEnough next)
  (f : (out : α) → LargeEnough out → out < upperBound → (c : γ) → n { s // Pl out c s }),
  Std.Rxo.Iterator.instIteratorLoop.loop.wf✝ γ Pl wf LargeEnough hl upperBound acc next h f =
    if hu : next < upperBound then do
      let __do_lift ← f next h hu acc
      match __do_lift with
        | ⟨ForInStep.yield acc', property⟩ =>
          match hs : Std.PRange.succ? next with
          | some next' => Std.Rxo.Iterator.instIteratorLoop.loop.wf✝ γ Pl wf LargeEnough hl upperBound acc' next' ⋯ f
          | none => pure acc'
        | ⟨ForInStep.done acc', property⟩ => pure acc'
    else pure acc
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.mk.injEq : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (toEquiv : A ≃ B)
  (map_mul' : ∀ (x y : A), toEquiv.toFun (x * y) = toEquiv.toFun x * toEquiv.toFun y)
  (map_add' : ∀ (x y : A), toEquiv.toFun (x + y) = toEquiv.toFun x + toEquiv.toFun y)
  (commutes' : ∀ (r : R), toEquiv.toFun ((algebraMap R A) r) = (algebraMap R B) r) (toEquiv_1 : A ≃ B)
  (map_mul'_1 : ∀ (x y : A), toEquiv_1.toFun (x * y) = toEquiv_1.toFun x * toEquiv_1.toFun y)
  (map_add'_1 : ∀ (x y : A), toEquiv_1.toFun (x + y) = toEquiv_1.toFun x + toEquiv_1.toFun y)
  (commutes'_1 : ∀ (r : R), toEquiv_1.toFun ((algebraMap R A) r) = (algebraMap R B) r),
  ({ toEquiv := toEquiv, map_mul' := map_mul', map_add' := map_add', commutes' := commutes' } =
      { toEquiv := toEquiv_1, map_mul' := map_mul'_1, map_add' := map_add'_1, commutes' := commutes'_1 }) =
    (toEquiv = toEquiv_1)
-- Init.Data.SInt.Lemmas
UInt64.toInt64_sub : ∀ (a b : UInt64), (a - b).toInt64 = a.toInt64 - b.toInt64
-- Mathlib.Logic.Equiv.Prod
Equiv.pprodProd_apply : ∀ {α₁ : Sort u_2} {β₁ : Sort u_5} {α₂ : Type u_9} {β₂ : Type u_10} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) (a : α₁ ×' β₁),
  (ea.pprodProd eb) a = (ea a.fst, eb a.snd)
-- Mathlib.Data.Set.Operations
Set.rangeFactorization_eq_rangeFactorization_iff : ∀ {ι : Sort u_2} {α : Type u_3} {f : ι → α} (a b : ι),
  Set.rangeFactorization f a = Set.rangeFactorization f b ↔ f a = f b
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.coeFn_compMeasurable : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace γ] [inst_3 : MeasurableSpace β]
  [inst_4 : TopologicalSpace.PseudoMetrizableSpace β] [inst_5 : BorelSpace β] [inst_6 : MeasurableSpace γ]
  [inst_7 : TopologicalSpace.PseudoMetrizableSpace γ] [inst_8 : OpensMeasurableSpace γ]
  [inst_9 : SecondCountableTopology γ] (g : β → γ) (hg : Measurable g) (f : α →ₘ[μ] β),
  ↑(MeasureTheory.AEEqFun.compMeasurable g hg f) =ᵐ[μ] g ∘ ↑f
-- Mathlib.Algebra.Group.Submonoid.Units
ofUnits_units_gc : ∀ {M : Type u_1} [inst : Monoid M], GaloisConnection Subgroup.ofUnits Submonoid.units
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
stronglyMeasurable_deriv_with_param : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_3} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {α : Type u_4} [inst_3 : TopologicalSpace α] [inst_4 : MeasurableSpace α]
  [OpensMeasurableSpace α] [CompleteSpace F] [LocallyCompactSpace 𝕜] [inst_8 : MeasurableSpace 𝕜]
  [OpensMeasurableSpace 𝕜] [h : SecondCountableTopologyEither α F] {f : α → 𝕜 → F},
  Continuous (Function.uncurry f) → MeasureTheory.StronglyMeasurable fun p => deriv (f p.1) p.2
-- Batteries.Tactic.Lint.Basic
/-- Defines the `@[env_linter]` attribute for adding a linter to the default set.
The form `@[env_linter disabled]` will not add the linter to the default set,
but it will be shown by `#list_linters` and can be selected by the `#lint` command.

Linters are named using their declaration names, without the namespace. These must be distinct.
 -/
Batteries.Tactic.Lint.env_linter : Lean.ParserDescr
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.prodEquiv.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (s : AddSubsemigroup M) (t : AddSubsemigroup N),
  s.prodEquiv t = { toEquiv := Equiv.Set.prod ↑s ↑t, map_add' := ⋯ }
-- Mathlib.Topology.Order.ScottTopology
/-- `ofScott` is the identity function from the `WithScott` of a type.  -/
Topology.WithScott.ofScott : {α : Type u_1} → Topology.WithScott α ≃ α
-- Std.Sat.AIG.CNF
/-- Combining two CNFs for which `State.Inv` holds preserves `State.Inv`.
 -/
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.State.Inv_append : ∀ {aig : Std.Sat.AIG ℕ} {cnf1 cnf2 : Std.Sat.CNF ℕ},
  Std.Sat.AIG.toCNF.State.Inv✝ aig cnf1 →
    Std.Sat.AIG.toCNF.State.Inv✝ aig cnf2 → Std.Sat.AIG.toCNF.State.Inv✝ aig (cnf1 ++ cnf2)
-- Mathlib.Algebra.Colimit.Module
Module.DirectLimit.lift_injective : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_2} [inst_1 : Preorder ι] {G : ι → Type u_3}
  [inst_2 : (i : ι) → AddCommMonoid (G i)] [inst_3 : (i : ι) → Module R (G i)] {f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
  [inst_4 : DecidableEq ι] {P : Type u_4} [inst_5 : AddCommMonoid P] [inst_6 : Module R P] (g : (i : ι) → G i →ₗ[R] P)
  (Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x) [IsDirectedOrder ι],
  (∀ (i : ι), Function.Injective ⇑(g i)) → Function.Injective ⇑(Module.DirectLimit.lift R ι G f g Hg)
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHom.prod_fst_snd : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction R B] [inst_6 : Star B],
  (NonUnitalStarAlgHom.fst R A B).prod (NonUnitalStarAlgHom.snd R A B) = 1
-- Mathlib.Topology.UniformSpace.Closeds
UniformSpace.hausdorff.instCompactSpaceSet : ∀ {α : Type u_1} [inst : UniformSpace α] [CompactSpace α], CompactSpace (Set α)
-- Mathlib.Analysis.Convex.Between
sbtw_const_sub_iff : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] {x y z : V} (v : V), Sbtw R (v - x) (v - y) (v - z) ↔ Sbtw R x y z
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
/-- **Alias** of `CategoryTheory.CardinalDirectedPoset.PropSet`.

---

Given `J : CardinalDirectedPoset κ`, this is the predicate
on `Set J.obj` that is satisfied by subsets that are of
cardinality `< κ` and have a terminal object.  -/
CategoryTheory.CardinalFilteredPoset.PropSet : {κ : Cardinal.{u}} → [inst : Fact κ.IsRegular] → (J : CategoryTheory.CardinalDirectedPoset κ) → Set ↑J.obj → Prop
-- Mathlib.GroupTheory.GroupAction.Blocks
AddAction.IsTrivialBlock.vadd_iff : ∀ {M : Type u_3} {α : Type u_4} [inst : AddGroup M] [inst_1 : AddAction M α] {B : Set α} (g : M),
  AddAction.IsTrivialBlock (g +ᵥ B) ↔ AddAction.IsTrivialBlock B