mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Util.LeanOptions
Lean.LeanOptionValue.ofString.inj : ∀ {s s_1 : String}, Lean.LeanOptionValue.ofString s = Lean.LeanOptionValue.ofString s_1 → s = s_1
-- Mathlib.Topology.MetricSpace.MetricSeparated
Metric.AreSeparated.union_left : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {s t s' : Set X},
  Metric.AreSeparated s t → Metric.AreSeparated s' t → Metric.AreSeparated (s ∪ s') t
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.instOplaxMonoidalActionTypeLinearization : (k : Type u) → (G : Type v) → [inst : CommRing k] → [inst_1 : Monoid G] → (Rep.linearization k G).OplaxMonoidal
-- Mathlib.Algebra.Ring.ULift
ULift.nonUnitalSemiring : {R : Type u} → [NonUnitalSemiring R] → NonUnitalSemiring (ULift.{u_1, u} R)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Tactic.ComputeAsymptotics.WellFormedBasis.push : ∀ {basis : Tactic.ComputeAsymptotics.Basis} {f : ℝ → ℝ},
  Tactic.ComputeAsymptotics.WellFormedBasis basis →
    Filter.Tendsto f Filter.atTop Filter.atTop →
      (∀ (g : ℝ → ℝ), List.getLast? basis = some g → (Real.log ∘ f) =o[Filter.atTop] (Real.log ∘ g)) →
        Tactic.ComputeAsymptotics.WellFormedBasis (basis ++ [f])
-- Mathlib.Algebra.Group.Conj
AddConjClasses.mk_bijective : ∀ {α : Type u} [inst : AddCommMonoid α], Function.Bijective AddConjClasses.mk
-- Mathlib.Algebra.Star.StarRingHom
/-- The identity map as a star ring isomorphism.  -/
StarRingEquiv.refl : {A : Type u_1} → [inst : Add A] → [inst_1 : Mul A] → [inst_2 : Star A] → A ≃⋆+* A
-- Batteries.Recycling.RBTree.Basic
RBTree.RBColor.red.sizeOf_spec : sizeOf RBTree.RBColor.red = 1
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.of_ringEquiv_left : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_4} [inst_1 : CommSemiring S] {K : Type u_5}
  [inst_2 : CommSemiring K] [inst_3 : Algebra R K] (e : R ≃+* S) [inst_4 : Algebra S K] {M₁ : Submonoid S}
  {M₂ : Submonoid R},
  Submonoid.map e M₂ = M₁ →
    (∀ (x : R), (algebraMap R K) x = (algebraMap S K) (e x)) → ∀ [IsLocalization M₁ K], IsLocalization M₂ K
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.contains_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k a : α} {v : β}, (t.insertIfNew k v).contains a = (cmp k a == Ordering.eq || t.contains a)
-- Mathlib.Analysis.CStarAlgebra.Matrix
Matrix.l2_opNorm_def : ∀ {𝕜 : Type u_1} {m : Type u_2} {n : Type u_3} [inst : RCLike 𝕜] [inst_1 : Fintype m] [inst_2 : Fintype n]
  [inst_3 : DecidableEq n] (A : Matrix m n 𝕜), ‖A‖ = ‖(Matrix.toEuclideanLin ≪≫ₗ LinearMap.toContinuousLinearMap) A‖
-- Mathlib.Topology.Semicontinuity.Basic
/-- **Alias** of the reverse direction of `lowerSemicontinuousWithinAt_neg_iff`. -/
UpperSemicontinuousWithinAt.neg : ∀ {α : Type u_4} [inst : TopologicalSpace α] {β : Type u_5} {f : α → β} {s : Set α} {a : α} [inst_1 : PartialOrder β]
  [inst_2 : AddCommGroup β] [IsOrderedAddMonoid β],
  UpperSemicontinuousWithinAt f s a → LowerSemicontinuousWithinAt (-f) s a
-- Mathlib.CategoryTheory.GradedObject.Unitor
CategoryTheory.GradedObject.singleObjApplyIsoOfEq.congr_simp : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Limits.HasInitial C] [inst_2 : DecidableEq J] (j : J) (X : C) (i : J) (h : i = j),
  CategoryTheory.GradedObject.singleObjApplyIsoOfEq j X i h = CategoryTheory.GradedObject.singleObjApplyIsoOfEq j X i h
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.stdPart_sub_eq_right : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] {x y : K},
  0 < ArchimedeanClass.mk x → ArchimedeanClass.stdPart (x - y) = -ArchimedeanClass.stdPart y
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.equivTreesOfNumNodesEq_symm_apply_coe : ∀ (n : ℕ) (b : ↥(BinaryTree.treesOfNumNodesEq n)), ↑((DyckWord.equivTreesOfNumNodesEq n).symm b) = DyckWord.ofTree ↑b
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.evaln.eq_5 : ∀ (k : ℕ),
  Nat.Partrec.Code.evaln k.succ Nat.Partrec.Code.right = fun n => do
    guard (n ≤ k)
    pure (Nat.unpair n).2
-- Mathlib.Data.Finset.Piecewise
Finset.update_piecewise_of_notMem : ∀ {ι : Type u_1} {π : ι → Sort u_2} (s : Finset ι) (f g : (i : ι) → π i) [inst : (j : ι) → Decidable (j ∈ s)]
  [inst_1 : DecidableEq ι] {i : ι},
  i ∉ s → ∀ (v : π i), Function.update (s.piecewise f g) i v = s.piecewise f (Function.update g i v)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.μ_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (G H : CategoryTheory.AddGrp C),
  CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.AddGrp.forget₂Mon C) G H =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.AddGrp.forget₂Mon C).obj G)
        ((CategoryTheory.AddGrp.forget₂Mon C).obj H))
-- Std.Data.HashMap.Lemmas
Std.HashMap.contains_of_mem_keysArray : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, k ∈ m.keysArray → m.contains k = true
-- Mathlib.Util.PrintSorries
Mathlib.PrintSorries.State.mk : Lean.NameSet → Std.HashSet Lean.Expr → Array Lean.MessageData → Mathlib.PrintSorries.State
-- Mathlib.Geometry.Euclidean.Sphere.Basic
/-- Given a point on a sphere and a point not outside it, the inner product between the
difference of those points and the radius vector is nonnegative.  -/
EuclideanGeometry.inner_nonneg_of_dist_le_radius : ∀ {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₁ p₂ : P},
  p₁ ∈ s → dist p₂ s.center ≤ s.radius → 0 ≤ inner ℝ (p₁ -ᵥ p₂) (p₁ -ᵥ s.center)
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.image_smul_comm : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SMul α β] [inst_1 : SMul α γ] (f : β → γ) (a : α) (s : Set β),
  (∀ (b : β), f (a • b) = a • f b) → f '' (a • s) = a • f '' s
-- Mathlib.LinearAlgebra.Matrix.Hermitian
/-- Note this is more general than `IsSelfAdjoint.mul_star_self` as `B` can be rectangular.  -/
Matrix.isHermitian_mul_conjTranspose_self : ∀ {α : Type u_1} {m : Type u_3} {n : Type u_4} [inst : NonUnitalSemiring α] [inst_1 : StarRing α] [inst_2 : Fintype n]
  (A : Matrix m n α), (A * A.conjTranspose).IsHermitian
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.ServerInfo.mk : String → Option String → Lean.Lsp.ServerInfo
-- Mathlib.Topology.Algebra.Valued.ValuationTopology
/-- A sphere centred at the origin in a valued ring is open.  -/
Valued.isOpen_sphere : ∀ (R : Type u) [inst : Ring R] {Γ₀ : Type v} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀]
  {r : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀}, r ≠ 0 → IsOpen {x | Valued.v.restrict x = r}
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
/-- Given an action of `GL n R` such that the scalar matrices act trivially,
define an action of `PGL n R`.  -/
Matrix.ProjGenLinGroup.mulActionOfGL : {n : Type u_1} →
  {R : Type u_2} →
    [inst : Fintype n] →
      [inst_1 : DecidableEq n] →
        [inst_2 : CommRing R] →
          {α : Type u_4} →
            [inst_3 : MulAction (GL n R) α] →
              (∀ (u : Rˣ) (a : α), (Matrix.GeneralLinearGroup.scalar n) u • a = a) →
                MulAction (Matrix.ProjGenLinGroup n R) α
-- Mathlib.Algebra.Module.PID
Module.p_pow_smul_lift : ∀ {R : Type u} [inst : CommRing R] [IsPrincipalIdealRing R] {M : Type v} [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [IsDomain R] {p : R},
  Irreducible p →
    ∀ (hM : Module.IsTorsion' M ↥(Submonoid.powers p)) [dec : (x : M) → Decidable (x = 0)] {x y : M} {k : ℕ},
      Module.IsTorsionBy R M (p ^ Submodule.pOrder hM y) → p ^ k • x ∈ R ∙ y → ∃ a, p ^ k • x = p ^ k • a • y
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
/-- Monomial degree of product  -/
MonomialOrder.degree_mul_of_isRegular_left : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f g : MvPolynomial σ R},
  IsRegular (m.leadingCoeff f) → g ≠ 0 → m.degree (f * g) = m.degree f + m.degree g
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.comap_strictMono_of_surjective : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [RingHomSurjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂}, Function.Surjective ⇑f → StrictMono (Submodule.comap f)
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_const_add_left : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ],
  MeasureTheory.Integrable X μ →
    ∀ (c : ℝ), ProbabilityTheory.covariance (fun ω => c + X ω) Y μ = ProbabilityTheory.covariance X Y μ
-- Mathlib.GroupTheory.Focal
AddSubgroup.focalAddSubgroup_def : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G),
  H.focalAddSubgroup = AddSubgroup.closure {g | g ∈ H ∧ ∃ x ∈ H, ∃ u, g = ⁅x, u⁆}
-- Aesop.EMap
Aesop.EMap.singleton : {m : Type → Type u_1} → [Monad m] → [MonadLiftT Lean.MetaM m] → {α : Type} → Lean.Expr → α → m (Aesop.EMap α)
-- Mathlib.SetTheory.Ordinal.FundamentalSequence
Ordinal.IsFundamentalSequence.cof_eq : ∀ {a o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{u}}, a.IsFundamentalSequence o f → a.cof.ord = o
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryPseudofunctor.mk'_obj : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (S : CategoryTheory.StrictlyUnitaryPseudofunctorCore B C) (a : B),
  (CategoryTheory.StrictlyUnitaryPseudofunctor.mk' S).obj a = S.obj a
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.IsCut.congr : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {x y : α} [RBTree.RBNode.IsCut cmp cut]
  [Std.TransCmp cmp], cmp x y = Ordering.eq → cut x = cut y
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.toQ.eq_1 : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (a : α), ↑a = Lean.Grind.Ring.OfSemiring.Q.mk (a, 0)
-- Mathlib.Analysis.Analytic.IsolatedZeros
HasFPowerSeriesAt.eq_pow_order_mul_iterate_dslope : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {p : FormalMultilinearSeries 𝕜 𝕜 E} {f : 𝕜 → E} {z₀ : 𝕜},
  HasFPowerSeriesAt f p z₀ → ∀ (z : 𝕜), f z = (z - z₀) ^ p.order • (Function.swap dslope z₀)^[p.order] f z
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- The span of a union of sets is the sup of their spans.  -/
AffineSubspace.span_union : ∀ (k : Type u_1) (V : Type u_2) {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] (s t : Set P), affineSpan k (s ∪ t) = affineSpan k s ⊔ affineSpan k t
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.mem_of_mem_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∈ t.keys → k ∈ t
-- Mathlib.Logic.OpClass
instLeftCommutativeOfCommutativeOfAssociative : ∀ {α : Sort u} {f : α → α → α} [hc : Std.Commutative f] [ha : Std.Associative f], LeftCommutative f
-- Mathlib.Logic.Equiv.Finset
/-- Outputs the list of partial sums plus one of the input list, that is
`raise [a₁, a₂, a₃, ...] n = [n + a₁, n + a₁ + a₂ + 1, n + a₁ + a₂ + a₃ + 2, ...]`. Adding one each
time ensures the elements are distinct.  -/
Denumerable.raise' : List ℕ → ℕ → List ℕ
-- Mathlib.Analysis.Analytic.Constructions
HasFPowerSeriesWithinAt.compContinuousLinearMap : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} {G : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {u : E →L[𝕜] F} {f : F → G}
  {pf : FormalMultilinearSeries 𝕜 F G} {s : Set F} {x : E},
  HasFPowerSeriesWithinAt f pf s (u x) → HasFPowerSeriesWithinAt (f ∘ ⇑u) (pf.compContinuousLinearMap u) (⇑u ⁻¹' s) x
-- Mathlib.CategoryTheory.GuitartExact.KanExtension
CategoryTheory.TwoSquare.hasPointwiseLeftKanExtensionAt_iff : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} {D : Type u₅} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] [inst_4 : CategoryTheory.Category.{v₅, u₅} D]
  {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃} {R : CategoryTheory.Functor C₂ C₄}
  {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B) (F : CategoryTheory.Functor C₂ D) (X₃ : C₃)
  [(w.costructuredArrowRightwards X₃).Final],
  L.HasPointwiseLeftKanExtensionAt (T.comp F) X₃ ↔ R.HasPointwiseLeftKanExtensionAt F (B.obj X₃)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Bicones.ext_inv_hom : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} {c c' : CategoryTheory.Limits.Bicone F}
  (φ : c.pt ≅ c'.pt)
  (wι :
    autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp (c.ι j) φ.hom = c'.ι j)
      CategoryTheory.Limits.Bicones.ext._auto_1)
  (wπ :
    autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp φ.hom (c'.π j) = c.π j)
      CategoryTheory.Limits.Bicones.ext._auto_3),
  (CategoryTheory.Limits.Bicones.ext φ wι wπ).inv.hom = φ.inv
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.addSubgroupOf.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] (H K : AddSubgroup G), H.addSubgroupOf K = AddSubgroup.comap K.subtype H
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.addHaar_singleton : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [inst_2 : TopologicalSpace G]
  (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [ContinuousAdd G] [BorelSpace G] (g : G), μ {g} = μ {0}
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey_maxKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {fallback : α} {hc : t.maxKeyD fallback ∈ t}, t.getKey (t.maxKeyD fallback) hc = t.maxKeyD fallback
-- Mathlib.CategoryTheory.Distributive.Monoidal
CategoryTheory.coprod_inr_rightDistrib_hom_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] [inst_3 : CategoryTheory.IsMonoidalRightDistrib C]
  {X Y Z Z_1 : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (Y ⨿ Z) X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr
      (CategoryTheory.CategoryStruct.comp (∂R X Y Z).hom h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.coprod.inr X) h
-- Lean.MetavarContext
/-- Return `true` iff expression contains assigned (level/expr) metavariables or delayed assigned mvars  -/
Lean.hasAssignedMVar : {m : Type → Type} → [Monad m] → [Lean.MonadMCtx m] → Lean.Expr → m Bool
-- Lean.Elab.Do.Switch
Lean.Elab.Term.elabTermNestedAction : Lean.Elab.Term.TermElab
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.IsLocallyDirected.t.eq_1 : ∀ {J : Type w} [inst : CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J AlgebraicGeometry.Scheme)
  [inst_1 : ∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f)]
  [inst_2 : (F.comp AlgebraicGeometry.Scheme.forget).IsLocallyDirected] [inst_3 : Quiver.IsThin J] (i j : J),
  AlgebraicGeometry.Scheme.IsLocallyDirected.t F i j =
    AlgebraicGeometry.IsOpenImmersion.lift (AlgebraicGeometry.Scheme.IsLocallyDirected.V F j i).ι
      (AlgebraicGeometry.Scheme.IsLocallyDirected.tAux F i j) ⋯
-- Mathlib.Topology.NhdsWithin
nhdsSetWithin_mono_left : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s s' t : Set α}, s ⊆ s' → nhdsSetWithin s t ≤ nhdsSetWithin s' t
-- Init.Data.Nat.ToString
Nat.digitChar_eq_five : ∀ {n : ℕ}, n.digitChar = '5' ↔ n = 5
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.Const.alterKey_cons_perm.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (x : Option β) → (Unit → motive none) → ((v : β) → motive (some v)) → motive x
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.FlatMap.0.Std.Iter.step_flatMapAfterM.match_1.eq_1 : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {it₁ : Std.Iter β} (motive : it₁.Step → Sort u_2) (it₁' : Std.Iter β)
  (b : β) (h : it₁.IsPlausibleStep (Std.IterStep.yield it₁' b))
  (h_1 :
    (it₁' : Std.Iter β) →
      (b : β) → (h : it₁.IsPlausibleStep (Std.IterStep.yield it₁' b)) → motive ⟨Std.IterStep.yield it₁' b, 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.yield it₁' b, h⟩ with
    | ⟨Std.IterStep.yield it₁' b, h⟩ => h_1 it₁' b h
    | ⟨Std.IterStep.skip it₁', h⟩ => h_2 it₁' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_1 it₁' b h
-- Lean.Data.Lsp.Internal
Lean.Lsp.LeanIdentifier.mk.sizeOf_spec : ∀ (module decl : Lean.Name) (isExactMatch : Bool),
  sizeOf { module := module, decl := decl, isExactMatch := isExactMatch } =
    1 + sizeOf module + sizeOf decl + sizeOf isExactMatch
-- Mathlib.Topology.UniformSpace.Separation
SeparationQuotient.map_id : ∀ {α : Type u} [inst : UniformSpace α], SeparationQuotient.map id = id
-- Mathlib.Algebra.Group.Subgroup.Ker
/-- Additive subgroups of the subgroup `H` are considered as
additive subgroups that are less than or equal to `H`.  -/
AddSubgroup.MapSubtype.orderIso : {G : Type u_1} → [inst : AddGroup G] → (H : AddSubgroup G) → AddSubgroup ↥H ≃o { H' // H' ≤ H }
-- Mathlib.Order.PiLex
Pi.instPartialOrderLexForallOfLinearOrder : {ι : Type u_1} →
  {β : ι → Type u_2} → [LinearOrder ι] → [(a : ι) → PartialOrder (β a)] → PartialOrder (Lex ((i : ι) → β i))
-- Mathlib.Order.Interval.Finset.Basic
Set.Infinite.exists_gt : ∀ {α : Type u_2} [inst : LinearOrder α] [LocallyFiniteOrderBot α] {s : Set α}, s.Infinite → ∀ (a : α), ∃ b ∈ s, a < b
-- Mathlib.Tactic.DeriveTraversable
/-- The deriving handler for `LawfulFunctor`.  -/
Mathlib.Deriving.Traversable.lawfulFunctorDeriveHandler : Lean.Elab.DerivingHandler
-- Mathlib.Algebra.Group.Basic
neg_add_eq_zero : ∀ {G : Type u_3} [inst : AddGroup G] {a b : G}, -a + b = 0 ↔ a = b
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.coe_mk : ∀ {𝕜 : Type u_2} {α : Type u_5} [inst : Zero 𝕜] [inst_1 : LE α] (f : α → α → 𝕜) (h : ∀ ⦃a b : α⦄, ¬a ≤ b → f a b = 0),
  ⇑{ toFun := f, eq_zero_of_not_le' := h } = f
-- Init.System.IOError
/-- Exceptions that may be thrown in the `IO` monad.

Many of the constructors of `IO.Error` correspond to POSIX error numbers. In these cases, the
documentation string lists POSIX standard error macros that correspond to the error. This list is
not necessarily exhaustive, and these constructor includes a field for the underlying error number.
 -/
IO.Error : Type
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.utf8DecodeChar?_eq_assemble₄ : ∀ {b : ByteArray} (hb : 4 ≤ b.size),
  ByteArray.utf8DecodeChar?.parseFirstByte b[0] = ByteArray.utf8DecodeChar?.FirstByte.threeMore →
    b.utf8DecodeChar? 0 = ByteArray.utf8DecodeChar?.assemble₄ b[0] b[1] b[2] b[3]
-- Mathlib.Algebra.NonAssoc.PreLie.Basic
LeftPreLieAlgebra.toSMulCommClass : ∀ {R : Type u_1} {inst : CommRing R} {L : Type u_2} {inst_1 : LeftPreLieRing L} [self : LeftPreLieAlgebra R L],
  SMulCommClass R L L
-- Mathlib.Data.Rel
SetRel.preimage_eq_biUnion : ∀ {α : Type u_1} {β : Type u_2} {R : SetRel α β} {t : Set β}, R.preimage t = ⋃ y ∈ t, {x | (x, y) ∈ R}
-- Init.Data.BitVec.Lemmas
BitVec.srem.eq_1 : ∀ {n : ℕ} (x y : BitVec n),
  x.srem y =
    match x.msb, y.msb with
    | false, false => x.umod y
    | false, true => x.umod y.neg
    | true, false => (x.neg.umod y).neg
    | true, true => (x.neg.umod y.neg).neg
-- Mathlib.MeasureTheory.Integral.IntegrableOn
ContinuousOn.aemeasurable₀ : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [inst : TopologicalSpace α] [OpensMeasurableSpace α]
  [inst_2 : MeasurableSpace β] [inst_3 : TopologicalSpace β] [BorelSpace β] {f : α → β} {s : Set α}
  {μ : MeasureTheory.Measure α}, ContinuousOn f s → MeasureTheory.NullMeasurableSet s μ → AEMeasurable f (μ.restrict s)
-- Mathlib.Data.ENNReal.Basic
ENNReal.iInf_ennreal : ∀ {α : Type u_2} [inst : CompleteLattice α] {f : ENNReal → α}, ⨅ n, f n = (⨅ n, f ↑n) ⊓ f ⊤
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- `toAdjunction'` is the dual of `ToAdjunction`, which we need for `to_dual`.
Please avoid using this directly.  -/
CategoryTheory.Equivalence.toAdjunction' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → (e : C ≌ D) → e.inverse ⊣ e.functor
-- Mathlib.NumberTheory.RamificationInertia.Unramified
/-- Let `R` be a domain of characteristic 0, finite rank over `ℤ`, `S` be a Dedekind domain
that is a finite `R`-algebra. Let `p` be a prime of `S`, then `p` is unramified iff `e(p) = 1`.  -/
Algebra.isUnramifiedAt_iff_of_isDedekindDomain : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal S}
  [inst_3 : p.IsPrime] [Algebra.EssFiniteType R S] [IsDomain R] [Module.Finite ℤ R] [CharZero R]
  [Algebra.IsIntegral R S], Algebra.IsUnramifiedAt R p ↔ p.ramificationIdx R = 1
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_roo_zero_right_eq_nil : ∀ {m : ℕ}, (m<...0).toList = []
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.Presentation.finite_coeffs : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {P : Algebra.Presentation R S ι σ} [Finite σ], P.coeffs.Finite
-- Mathlib.CategoryTheory.Idempotents.Biproducts
/-- `P.complement` is the formal direct factor of `P.X` given by the idempotent
endomorphism `𝟙 P.X - P.p`  -/
CategoryTheory.Idempotents.Karoubi.complement : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [CategoryTheory.Preadditive C] → CategoryTheory.Idempotents.Karoubi C → CategoryTheory.Idempotents.Karoubi C
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Matrix.charmatrix_reindex : ∀ {R : Type u_1} [inst : CommRing R] {m : Type u_3} {n : Type u_4} [inst_1 : DecidableEq m] [inst_2 : DecidableEq n]
  [inst_3 : Fintype m] [inst_4 : Fintype n] (M : Matrix n n R) (e : n ≃ m),
  ((Matrix.reindex e e) M).charmatrix = (Matrix.reindex e e) M.charmatrix
-- Mathlib.Algebra.Quaternion
Quaternion.re_coe : ∀ {R : Type u_3} [inst : CommRing R] (x : R), (↑x).re = x
-- Aesop.Frontend.Tactic
Aesop.Frontend.TacticConfig.simpConfigSyntax? : Aesop.Frontend.TacticConfig → Option Lean.Term
-- Mathlib.Order.Concept
Concept.swap_le_swap_iff : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c d : Concept α β r}, c.swap ≤ d.swap ↔ d ≤ c