mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Point.Map
CategoryTheory.GrothendieckTopology.Point.presheafFiberMapIso_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D)
  (K : CategoryTheory.GrothendieckTopology D) [inst_2 : F.IsCocontinuous J K]
  [inst_3 : CategoryTheory.LocallySmall.{w, v', u'} D] (A : Type u'') [inst_4 : CategoryTheory.Category.{v'', u''} A]
  [inst_5 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] (X : CategoryTheory.Functor Dᵒᵖ A),
  (Φ.presheafFiberMapIso F K A).hom.app X = (Φ.presheafFiberMapObjIso F K X).hom
-- Mathlib.Topology.Algebra.Group.Basic
/-- Eta-expanded form of `ContinuousOn.zpow` -/
ContinuousOn.fun_zpow : ∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G]
  [inst_3 : TopologicalSpace α] {f : α → G} {s : Set α}, ContinuousOn f s → ∀ (z : ℤ), ContinuousOn (fun i => f i ^ z) s
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.map_eq_eval₂Hom_C_comp : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (f : R →+* S₁),
  MvPolynomial.map f = MvPolynomial.eval₂Hom (MvPolynomial.C.comp f) MvPolynomial.X
-- Mathlib.RepresentationTheory.Basic
Representation.asAlgebraHom_def : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommSemiring k] [inst_1 : Monoid G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module k V] (ρ : Representation k G V), ρ.asAlgebraHom = (MonoidAlgebra.lift k (V →ₗ[k] V) G) ρ
-- Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
le_iff_forall_pos_le_add : ∀ {α : Type u} [inst : LinearOrder α] [DenselyOrdered α] [inst_2 : AddMonoid α] [ExistsAddOfLE α] [AddLeftReflectLT α]
  {a b : α} [AddLeftStrictMono α], a ≤ b ↔ ∀ (ε : α), 0 < ε → a ≤ b + ε
-- Mathlib.Topology.FiberBundle.Basic
/-- If `E` is a fiber bundle over a conditionally complete linear order,
then it is trivial over any closed interval.  -/
FiberBundle.exists_trivialization_Icc_subset : ∀ {B : Type u_2} (F : Type u_3) [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] (E : B → Type u_5)
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_3 : (b : B) → TopologicalSpace (E b)]
  [inst_4 : ConditionallyCompleteLinearOrder B] [OrderTopology B] [FiberBundle F E] (a b : B),
  ∃ e, Set.Icc a b ⊆ e.baseSet
-- Mathlib.Geometry.Euclidean.SignedDist
signedDist_vadd_left_swap : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (v w : V) (p q : P), ((signedDist v) (w +ᵥ p)) q = ((signedDist v) p) (-w +ᵥ q)
-- Lean.Elab.InfoTree.Types
Lean.Elab.CommandInfo.mk.inj : ∀ {toElabInfo toElabInfo_1 : Lean.Elab.ElabInfo},
  { toElabInfo := toElabInfo } = { toElabInfo := toElabInfo_1 } → toElabInfo = toElabInfo_1
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.continuous_invFun : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_4} {V₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁]
  [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂]
  (self : P₁ ≃ᴬ[k] P₂), Continuous (↑self).invFun
-- Init.Data.List.Monadic
/-- Applies the monadic action `f` to the corresponding elements of two lists, left-to-right, stopping
at the end of the shorter list. `zipWithM' f as bs` is equivalent to `mapM id (zipWith f as bs)`
for lawful `Monad` instances.
 -/
List.zipWithM' : {m : Type u → Type v} →
  [Monad m] → {α : Type w} → {β : Type x} → {γ : Type u} → (α → β → m γ) → List α → List β → m (List γ)
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.withDensity_sum : ∀ {α : Type u_1} {ι : Type u_2} {m : MeasurableSpace α} (μ : ι → MeasureTheory.Measure α) (f : α → ENNReal),
  (MeasureTheory.Measure.sum μ).withDensity f = MeasureTheory.Measure.sum fun n => (μ n).withDensity f
-- Std.Sync.CancellationContext
Std.CancellationContext.state : Std.CancellationContext → Std.Mutex Std.CancellationContext.State
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
WeierstrassCurve.Affine.addY.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Affine R) (x₁ x₂ y₁ ℓ : R),
  W'.addY x₁ x₂ y₁ ℓ = W'.negY (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ)
-- Mathlib.MeasureTheory.Integral.Prod
/-- A binary function is integrable if the function `x ↦ f (x, y)` is integrable for almost every
`y` and the function `y ↦ ∫ ‖f (x, y)‖ dx` is integrable.  -/
MeasureTheory.integrable_prod_iff' : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E] [MeasureTheory.SFinite ν]
  [MeasureTheory.SFinite μ] ⦃f : α × β → E⦄,
  MeasureTheory.AEStronglyMeasurable f (μ.prod ν) →
    (MeasureTheory.Integrable f (μ.prod ν) ↔
      (∀ᵐ (y : β) ∂ν, MeasureTheory.Integrable (fun x => f (x, y)) μ) ∧
        MeasureTheory.Integrable (fun y => ∫ (x : α), ‖f (x, y)‖ ∂μ) ν)
-- Mathlib.Data.Nat.Prime.Basic
Nat.Prime.eq_two_or_odd : ∀ {p : ℕ}, Nat.Prime p → p = 2 ∨ p % 2 = 1
-- Mathlib.Algebra.Group.Subgroup.Order
MulEquiv.strictMono_symm : ∀ {G : Type u_1} {G' : Type u_2} [inst : CommMonoid G] [inst_1 : LinearOrder G] [inst_2 : CommMonoid G']
  [inst_3 : Preorder G'] {e : G ≃* G'}, StrictMono ⇑e → StrictMono ⇑e.symm
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
padicValNat_prime_prime_pow : ∀ {p q : ℕ} [hp : Fact (Nat.Prime p)] [hq : Fact (Nat.Prime q)] (n : ℕ), p ≠ q → padicValNat p (q ^ n) = 0
-- Mathlib.Data.Fin.Tuple.Take
Fin.take_take : ∀ {n : ℕ} {α : Fin n → Sort u_1} {m n' : ℕ} (h : m ≤ n') (h' : n' ≤ n) (v : (i : Fin n) → α i),
  Fin.take m h (Fin.take n' h' v) = Fin.take m ⋯ v
-- Init.Data.List.Lemmas
List.eq_getElem_of_length_eq_four : ∀ {α : Type u_1} (l : List α) (hl : l.length = 4), l = [l[0], l[1], l[2], l[3]]
-- Mathlib.LinearAlgebra.SpecialLinearGroup
LinearEquiv.dualMap.eq_1 : ∀ {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : Module R M₁] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M₂] (f : M₁ ≃ₗ[R] M₂),
  f.dualMap = { toLinearMap := (↑f).dualMap, invFun := ⇑(↑f.symm).dualMap, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Tactic.Linarith.Preprocessing
/-- `preprocess pps l` takes a list `l` of proofs of propositions.
It maps each preprocessor `pp ∈ pps` over this list.
The preprocessors are run sequentially: each receives the output of the previous one.
Note that a preprocessor may produce multiple or no expressions from each input expression,
so the size of the list may change.
 -/
Mathlib.Tactic.Linarith.preprocess : List Mathlib.Tactic.Linarith.GlobalBranchingPreprocessor →
  Lean.MVarId → List Lean.Expr → Lean.MetaM (List Mathlib.Tactic.Linarith.Branch)
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanImportMetaKind : Type
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.term.congr_simp : ∀ (I : Type u) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o o_1 : Ordinal.{u}} (e_o : o = o_1)
  (ho : o < Ordinal.type fun x1 x2 => x1 < x2), Profinite.NobelingProof.term I ho = Profinite.NobelingProof.term I ⋯
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExProd.const.sizeOf_spec : ∀ {u : Lean.Level} {α : Q(Type u)} {BaseType : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)}
  [inst : (a : Q(«$α»)) → SizeOf (BaseType a)] {e : Q(«$α»)} (value : BaseType e),
  sizeOf (Mathlib.Tactic.Ring.Common.ExProd.const value) = 1 + sizeOf e + sizeOf value
-- Mathlib.Logic.Equiv.Defs
Equiv.permCongr_symm_apply : ∀ {α' : Type u_1} {β' : Type u_2} (e : α' ≃ β') (p : Equiv.Perm β') (x : α'), (e.permCongr.symm p) x = e.symm (p (e x))
-- Std.Time.Time.Unit.Hour
Std.Time.Hour.instLTOrdinal : LT Std.Time.Hour.Ordinal
-- Mathlib.CategoryTheory.Localization.FiniteProducts
/-- The adjunction between the constant functor `D ⥤ (Discrete J ⥤ D)`
and `limitFunctor L W J`.  -/
CategoryTheory.Localization.HasProductsOfShapeAux.adj : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (L : CategoryTheory.Functor C D) →
          (W : CategoryTheory.MorphismProperty C) →
            [inst_2 : L.IsLocalization W] →
              (J : Type) →
                [inst_3 : CategoryTheory.Limits.HasProductsOfShape J C] →
                  [inst_4 : W.IsStableUnderProductsOfShape J] →
                    [inst_5 : W.ContainsIdentities] →
                      [inst_6 : Finite J] →
                        CategoryTheory.Functor.const (CategoryTheory.Discrete J) ⊣
                          CategoryTheory.Localization.HasProductsOfShapeAux.limitFunctor L W J
-- Lean.Linter.UnusedVariables
/-- Collect information from the `infoTrees` into `References`.
See `References` for more information about the return value.  -/
Lean.Linter.UnusedVariables.collectReferences : Array Lean.Elab.InfoTree →
  Lean.Syntax.Range → Lean.Linter.LinterSets → StateRefT' IO.RealWorld Lean.Linter.UnusedVariables.References IO Unit
-- Init.Data.UInt.Lemmas
UInt16.toUSize_toUInt32 : ∀ (n : UInt16), n.toUInt32.toUSize = n.toUSize
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry?_of_perm : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} {a : α},
  Std.Internal.List.DistinctKeys l → l.Perm l' → Std.Internal.List.getEntry? a l = Std.Internal.List.getEntry? a l'
-- Lean.Data.LBool
Lean.LBool.toString : Lean.LBool → String
-- Init.Data.Rat.Lemmas
Rat.neg_num : ∀ (a : ℚ), (-a).num = -a.num
-- Mathlib.LinearAlgebra.TensorProduct.Basic
TensorProduct.comm_comm : ∀ (R : Type u_1) [inst : CommSemiring R] (M : Type u_7) (N : Type u_8) [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (x : TensorProduct R N M),
  (TensorProduct.comm R M N) ((TensorProduct.comm R N M) x) = x
-- Mathlib.Algebra.DualNumber
DualNumber.inr_eq_smul_eps : ∀ {R : Type u_1} [inst : MulZeroOneClass R] (r : R), TrivSqZeroExt.inr r = r • DualNumber.eps
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.self_trans_symm : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_8} {M₂ : Type u_9} [inst : Semiring R₁] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M₁] [inst_3 : AddCommMonoid M₂] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂}
  {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂}
  (f : M₁ ≃ₛₗ[σ₁₂] M₂), f.trans f.symm = LinearEquiv.refl R₁ M₁
-- Mathlib.Topology.Algebra.MetricSpace.Lipschitz
/-- If a function is locally Lipschitz around a point, then it is continuous at this point.  -/
continuousAt_of_locally_lipschitz : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β} {x : α} {r : ℝ},
  0 < r → ∀ (K : ℝ), (∀ (y : α), dist y x < r → dist (f y) (f x) ≤ K * dist y x) → ContinuousAt f x
-- Mathlib.Order.WithBot
WithBot.semilatticeInf : {α : Type u_1} → [SemilatticeInf α] → SemilatticeInf (WithBot α)
-- Mathlib.Data.Set.Card
Set.eq_of_subset_of_ncard_le : ∀ {α : Type u_1} {s t : Set α},
  s ⊆ t → t.ncard ≤ s.ncard → autoParam t.Finite Set.eq_of_subset_of_ncard_le._auto_1 → s = t
-- Lean.Meta.MethodSpecs
Lean.MethodSpecsAttrData.mk.inj : ∀ {clsName : Lean.Name} {privateSpecs : Bool} {clsName_1 : Lean.Name} {privateSpecs_1 : Bool},
  { clsName := clsName, privateSpecs := privateSpecs } = { clsName := clsName_1, privateSpecs := privateSpecs_1 } →
    clsName = clsName_1 ∧ privateSpecs = privateSpecs_1
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.trInit.eq_1 : ∀ {K : Type u_1} {Γ : K → Type u_2} [inst : DecidableEq K] (k : K) (L : List (Γ k)),
  Turing.TM2to1.trInit k L =
    (true, (List.map (fun a => (false, Function.update (fun x => none) k (some a))) L.reverse).headI.2) ::
      (List.map (fun a => (false, Function.update (fun x => none) k (some a))) L.reverse).tail
-- Mathlib.Tactic.FunProp.Theorems
/-- form of the theorem, see documentation of TheoremForm  -/
Mathlib.Meta.FunProp.FunctionTheorem.form : Mathlib.Meta.FunProp.FunctionTheorem → Mathlib.Meta.FunProp.TheoremForm
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.nnnorm_snd_le : ∀ {p : ENNReal} (α : Type u_2) {β : Type u_3} [hp : Fact (1 ≤ p)] [inst : SeminormedAddCommGroup α]
  [inst_1 : SeminormedAddCommGroup β] (x : WithLp p (α × β)), ‖x.snd‖₊ ≤ ‖x‖₊
-- Std.Data.Internal.List.Associative
Std.Internal.List.insertEntry_of_perm : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l l' : List ((a : α) × β a)} {k : α} {v : β k},
  Std.Internal.List.DistinctKeys l →
    l.Perm l' → (Std.Internal.List.insertEntry k v l).Perm (Std.Internal.List.insertEntry k v l')
-- Std.Data.HashMap.Raw
Std.HashMap.Raw.instDecidableMem : {α : Type u} →
  {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → {m : Std.HashMap.Raw α β} → {a : α} → Decidable (a ∈ m)
-- Mathlib.Data.Set.Insert
Set.subset_insert : ∀ {α : Type u_1} (x : α) (s : Set α), s ⊆ insert x s
-- Init.Data.SInt.Lemmas
Int16.toInt_bmod_18446744073709551616 : ∀ (x : Int16), x.toInt.bmod 18446744073709551616 = x.toInt
-- Init.Data.SInt.Lemmas
Int16.ne_iff_ofBitVec_ne : ∀ {a b : BitVec 16}, a ≠ b ↔ Int16.ofBitVec a ≠ Int16.ofBitVec b
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.IsRatCondKernelCDFAux.bddBelow_range : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β} {f : α × β → ℚ → ℝ},
  ProbabilityTheory.IsRatCondKernelCDFAux f κ ν →
    ∀ (a : α), ∀ᵐ (t : β) ∂ν a, ∀ (q : ℚ), BddBelow (Set.range fun r => f (a, t) ↑r)
-- Mathlib.Algebra.Group.Pi.Basic
Pi.rightCancelSemigroup.eq_1 : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → RightCancelSemigroup (f i)],
  Pi.rightCancelSemigroup = { toSemigroup := Pi.semigroup, toIsRightCancelMul := ⋯ }
-- Mathlib.Order.Ideal
Order.Ideal.coe_inf : ∀ {P : Type u_1} [inst : SemilatticeSup P] [inst_1 : IsCodirectedOrder P] {s t : Order.Ideal P}, ↑(s ⊓ t) = ↑s ∩ ↑t
-- Mathlib.CategoryTheory.Abelian.SerreClass.Localization
CategoryTheory.ObjectProperty.SerreClassLocalization.inverseImage_epimorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C)
  [inst_3 : P.IsSerreClass] [L.IsLocalization P.isoModSerre] [inst_5 : CategoryTheory.Preadditive D] [L.Additive],
  (CategoryTheory.MorphismProperty.epimorphisms D).inverseImage L = P.epiModSerre
-- Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Mathlib.Tactic.Monoidal.evalComp_nil_nil : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g h : C} (α : f ≅ g) (β : g ≅ h),
  (α ≪≫ β).hom = (α ≪≫ β).hom
-- Lean.PrettyPrinter.Delaborator.Basic
/-- `@[app_delab c]` registers a delaborator for applications with head constant `c`.
Such delaborators also apply to the constant `c` itself (known as a "nullary application").

This attribute should be applied to definitions of type `Lean.PrettyPrinter.Delaborator.Delab`.

When defining delaborators for constant applications, one should prefer this attribute over `@[delab app.c]`,
as `@[app_delab c]` first performs name resolution on `c` in the current scope.
 -/
Lean.PrettyPrinter.Delaborator.attrApp_delab_ : Lean.ParserDescr
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
/-- Return `.done` for positive Int values. We don't want to unfold in the symbolic evaluator.  -/
Int.isPosValue : Lean.Meta.Simp.DSimproc
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.iSup_iff : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] {ι : Sort u_1}
  (W : ι → CategoryTheory.MorphismProperty C) {X Y : C} (f : X ⟶ Y), iSup W f ↔ ∃ i, W i f
-- Mathlib.Analysis.LConvolution
/-- Scoped notation for the additive convolution of functions with respect to a measure `μ`.  -/
MeasureTheory.«term_⋆ₗ[_]_» : Lean.TrailingParserDescr
-- Mathlib.Analysis.InnerProductSpace.Projection.Submodule
/-- In a Hilbert space, the orthogonal complement of the orthogonal complement of a subspace `K`
is the topological closure of `K`.

Note that the completeness assumption is necessary. Let `E` be the space `ℕ →₀ ℝ` with inner space
structure inherited from `PiLp 2 (fun _ : ℕ ↦ ℝ)`. Let `K` be the subspace of sequences with the sum
of all elements equal to zero. Then `Kᗮ = ⊥`, `Kᗮᗮ = ⊤`.  -/
Submodule.orthogonal_orthogonal_eq_closure : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [CompleteSpace E], Kᗮᗮ = K.topologicalClosure
-- Std.Time.Format.Modifier
Std.Time.Text.twoLetterShort.sizeOf_spec : sizeOf Std.Time.Text.twoLetterShort = 1
-- Init.Data.Iterators.Combinators.Monadic.FlatMap
Std.Iterators.Types.Flatten.IsPlausibleStep.innerSkip : ∀ {α α₂ β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m (Std.IterM m β)] [inst_1 : Std.Iterator α₂ m β]
  {it₁ : Std.IterM m (Std.IterM m β)} {it₂ it₂' : Std.IterM m β},
  it₂.IsPlausibleStep (Std.IterStep.skip it₂') →
    Std.Iterators.Types.Flatten.IsPlausibleStep { internalState := { it₁ := it₁, it₂ := some it₂ } }
      (Std.IterStep.skip { internalState := { it₁ := it₁, it₂ := some it₂' } })
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CochainComplex.singleFunctors.congr_simp : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C], CochainComplex.singleFunctors C = CochainComplex.singleFunctors C
-- Mathlib.Algebra.Homology.HomologicalBicomplex
HomologicalComplex₂.comm_f_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L : HomologicalComplex₂ C c₁ c₂}
  (f : K ⟶ L) (i₁ i₁' : I₁) (i₂ : I₂) {Z : C} (h : (L.X i₁').X i₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((f.f i₁).f i₂) (CategoryTheory.CategoryStruct.comp ((L.d i₁ i₁').f i₂) h) =
    CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂) (CategoryTheory.CategoryStruct.comp ((f.f i₁').f i₂) h)
-- Std.Time.Zoned.ZoneRules
Std.Time.TimeZone.instInhabitedLocalTimeType.default : Std.Time.TimeZone.LocalTimeType
-- Mathlib.Data.Real.Pointwise
Real.smul_iSup_of_nonpos : ∀ {ι : Sort u_1} {α : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : Module α ℝ]
  [IsOrderedModule α ℝ] {a : α}, a ≤ 0 → ∀ (f : ι → ℝ), a • ⨆ i, f i = ⨅ i, a • f i
-- Mathlib.Analysis.Complex.Trigonometric
Real.exp_sub_cosh : ∀ (x : ℝ), Real.exp x - Real.cosh x = Real.sinh x
-- Lean.Meta.Tactic.Rename
/-- Rename the user-face naming for the free variable `fvarId` at `mvarId`.
 -/
Lean.MVarId.rename : Lean.MVarId → Lean.FVarId → Lean.Name → Lean.MetaM Lean.MVarId
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.mapDomainNonUnitalRingHom_apply : ∀ (R : Type u_3) {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : Add M] [inst_2 : Add N] (f : M →ₙ+ N)
  (x : AddMonoidAlgebra R M), (AddMonoidAlgebra.mapDomainNonUnitalRingHom R f) x = AddMonoidAlgebra.mapDomain (⇑f) x
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.toLinearEquiv_injective : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂], Function.Injective AlgEquiv.toLinearEquiv
-- Mathlib.Order.Disjoint
Codisjoint.top_le : ∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderTop α] {a b : α}, Codisjoint a b → ⊤ ≤ a ⊔ b
-- Mathlib.RingTheory.Ideal.Height
RingEquiv.height_map : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] (e : R ≃+* S) (I : Ideal R),
  (Ideal.map e I).height = I.height
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char
Char.reduceIsAlpha : Lean.Meta.Simp.DSimproc
-- Mathlib.Data.Finsupp.Basic
Finsupp.frange.eq_1 : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (f : α →₀ M), f.frange = Finset.image (⇑f) f.support
-- Mathlib.NumberTheory.ModularForms.Bounds
/-- If `f` is a cusp form and `f'` a modular form, then `petersson k f f'` is bounded.  -/
CuspFormClass.petersson_bounded_left : ∀ (k : ℤ) (Γ : Subgroup (GL (Fin 2) ℝ)) [Γ.IsArithmetic] {F : Type u_2} {F' : Type u_3} (f : F) (f' : F')
  [inst : FunLike F UpperHalfPlane ℂ] [inst_1 : FunLike F' UpperHalfPlane ℂ] [CuspFormClass F Γ k]
  [ModularFormClass F' Γ k], ∃ C, ∀ (τ : UpperHalfPlane), ‖UpperHalfPlane.petersson k (⇑f) (⇑f') τ‖ ≤ C
-- Mathlib.Algebra.Order.Module.Defs
IsStrictOrderedModule.toIsOrderedModule : ∀ {α : Type u_1} {β : Type u_2} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulWithZero α β] [inst_3 : PartialOrder α]
  [inst_4 : PartialOrder β] [IsStrictOrderedModule α β], IsOrderedModule α β
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax
CategoryTheory.Oplax.OplaxTrans.leftUnitor_inv_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} (η : F ⟶ G) (a : B),
  (CategoryTheory.Oplax.OplaxTrans.leftUnitor η).inv.as.app a = (CategoryTheory.Bicategory.leftUnitor (η.app a)).inv
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.ExcenterExists.excenter_map : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {V₂ : Type u_3} {P₂ : Type u_4} [inst_4 : NormedAddCommGroup V₂]
  [inst_5 : InnerProductSpace ℝ V₂] [inst_6 : MetricSpace P₂] [inst_7 : NormedAddTorsor V₂ P₂] {n : ℕ}
  [inst_8 : NeZero n] {s : Affine.Simplex ℝ P n} {signs : Finset (Fin (n + 1))},
  s.ExcenterExists signs → ∀ (f : P →ᵃⁱ[ℝ] P₂), (s.map f.toAffineMap ⋯).excenter signs = f (s.excenter signs)
-- Batteries.Data.List.Interleave
List.interleave_eq_nil : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.interleave l₂ = [] ↔ l₁ = [] ∧ l₂ = []
-- Batteries.Data.Array.Basic
_private.Batteries.Data.Array.Basic.0.Array.scanlMFast.loop.eq_def : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [inst : Monad m] (f : β → α → m β) (init : β) (as : Array α)
  (start stop : USize) (h_stop : stop.toNat ≤ as.size) (acc : Array β),
  Array.scanlMFast.loop✝ f init as start stop h_stop acc =
    if h_lt : start < stop then do
      let next ← f init (as.uget start ⋯)
      Array.scanlMFast.loop✝ f next as (start + 1) stop h_stop (acc.push init)
    else pure (acc.push init)
-- Init.Data.Array.Lemmas
Array.getElem_setIfInBounds_ne : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} {a : α} {j : ℕ} (hj : j < xs.size), i ≠ j → (xs.setIfInBounds i a)[j] = xs[j]
-- Mathlib.Order.BoundedOrder.Basic
ite_ne_top : ∀ {α : Type u} [inst : Top α] {p : Prop} [inst_1 : Decidable p] {a b : α},
  (p → a ≠ ⊤) → (¬p → b ≠ ⊤) → (if p then a else b) ≠ ⊤
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.log_ne_zero_of_pos_of_ne_one : ∀ {x : ℝ}, 0 < x → x ≠ 1 → Real.log x ≠ 0
-- Init.Data.List.Perm
List.exists_perm_sublist : ∀ {α : Type u_1} {l₁ l₂ l₂' : List α}, l₁.Sublist l₂ → l₂.Perm l₂' → ∃ l₁', l₁'.Perm l₁ ∧ l₁'.Sublist l₂'
-- Mathlib.Data.Sign.Defs
SignType.coe_neg : ∀ {α : Type u_2} [inst : One α] [inst_1 : SubtractionMonoid α] (s : SignType), ↑(-s) = -↑s
-- Lean.Meta.SizeOf
_private.Lean.Meta.SizeOf.0.Lean.Meta.SizeOfSpecNested.main.loop : Lean.Expr → Lean.Expr → Lean.Meta.SizeOfSpecNested.M Lean.Expr
-- Mathlib.Analysis.RCLike.Sqrt
Complex.sqrt_neg_of_nonneg : ∀ {a : ℂ}, 0 ≤ a → (-a).sqrt = Complex.I * a.sqrt
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- Functor composition induces a functor on augmented simplicial objects.  -/
CategoryTheory.SimplicialObject.Augmented.whiskering : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    (D : Type u') →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        CategoryTheory.Functor (CategoryTheory.Functor C D)
          (CategoryTheory.Functor (CategoryTheory.SimplicialObject.Augmented C)
            (CategoryTheory.SimplicialObject.Augmented D))