mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsBigOTVS.symm : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {l : Filter α} {g : α → F} [ContinuousNeg E] {f₁ f₂ : α → E},
  (f₁ - f₂) =O[𝕜; l] g → (f₂ - f₁) =O[𝕜; l] g
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.setToFun_congr_smul_measure' : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C C' : ℝ} (c : NNReal) (hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
  (hT_smul : MeasureTheory.DominatedFinMeasAdditive (c • μ) T C') (f : α → E),
  MeasureTheory.setToFun μ T hT f = MeasureTheory.setToFun (c • μ) T hT_smul f
-- Mathlib.Algebra.Group.PUnit
PUnit.instZero_mathlib : Zero PUnit.{u_1 + 1}
-- Mathlib.RingTheory.RingHom.Smooth
/-- Composition of formally smooth ring homomorphisms is formally smooth.  -/
RingHom.FormallySmooth.comp : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {T : Type u_3} [inst_2 : CommRing T]
  {f : R →+* S} {g : S →+* T}, f.FormallySmooth → g.FormallySmooth → (g.comp f).FormallySmooth
-- Mathlib.AlgebraicGeometry.Cover.Open
/-- The ranges of the maps in a scheme-theoretic open cover are a topological open cover.  -/
AlgebraicGeometry.Scheme.OpenCover.isOpenCover_opensRange : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover),
  TopologicalSpace.IsOpenCover fun i => AlgebraicGeometry.Scheme.Hom.opensRange (𝒰.f i)
-- Mathlib.Analysis.Quaternion
/-- Space of quaternions over a type, denoted as `ℍ[R]`.
Implemented as a structure with four fields: `re`, `im_i`, `im_j`, and `im_k`.  -/
Quaternion.termℍ : Lean.ParserDescr
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
/-- `tan (x / 2)` takes the junk value `0` when `sin x = 0` so this always holds.  -/
Real.sin_eq_two_mul_tan_half_div_one_add_tan_half_sq : ∀ (x : ℝ), Real.sin x = 2 * Real.tan (x / 2) / (1 + Real.tan (x / 2) ^ 2)
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.Ref.mk : {α : Sort u_1} → α → Lean.Syntax → Bool → Lean.Doc.Ref✝ α
-- Mathlib.Data.Quot
/-- Recursion on two `Quotient` arguments `a` and `b`, result type depends on `⟦a⟧` and `⟦b⟧`.  -/
Quot.hrecOn₂ : {α : Sort u_1} →
  {β : Sort u_2} →
    {ra : α → α → Prop} →
      {rb : β → β → Prop} →
        {φ : Quot ra → Quot rb → Sort u_3} →
          (qa : Quot ra) →
            (qb : Quot rb) →
              (f : (a : α) → (b : β) → φ (Quot.mk ra a) (Quot.mk rb b)) →
                (∀ {b : β} {a₁ a₂ : α}, ra a₁ a₂ → f a₁ b ≍ f a₂ b) →
                  (∀ {a : α} {b₁ b₂ : β}, rb b₁ b₂ → f a b₁ ≍ f a b₂) → φ qa qb
-- Mathlib.Algebra.Group.Irreducible.Defs
not_irreducible_one : ∀ {M : Type u_1} [inst : Monoid M], ¬Irreducible 1
-- Mathlib.RingTheory.RingHom.Smooth
/-- Helper lemma for the `algebraize` tactic  -/
RingHom.Smooth.toAlgebra : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, f.Smooth → Algebra.Smooth R S
-- Mathlib.LinearAlgebra.Lagrange
Polynomial.eq_zero_of_degree_lt_of_eval_finset_eq_zero : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] {f : Polynomial R} (s : Finset R),
  f.degree < ↑s.card → (∀ x ∈ s, Polynomial.eval x f = 0) → f = 0
-- Mathlib.Analysis.ODE.Transform
IsIntegralCurve.comp_add : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E},
  IsIntegralCurve γ v → ∀ (dt : ℝ), IsIntegralCurve (γ ∘ fun x => x + dt) (v ∘ fun x => x + dt)
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.cancel_unit_right_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) {W X X' Y : C} (f : W ⟶ X) (g : X ⟶ Y) (f' : W ⟶ X') (g' : X' ⟶ Y),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g (e.unit.app Y)) =
      CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g' (e.unit.app Y)) ↔
    CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f' g'
-- Mathlib.Logic.Equiv.Prod
Equiv.prodCongrRight_apply : ∀ {α₁ : Type u_9} {β₁ : Type u_11} {β₂ : Type u_12} (e : α₁ → β₁ ≃ β₂) (a : α₁) (b : β₁),
  (Equiv.prodCongrRight e) (a, b) = (a, (e a) b)
-- Mathlib.AlgebraicTopology.TopologicalSimplex
/-- The functor `SimplexCategory ⥤ TopCat.{0}`
associating the topological `n`-simplex to `⦋n⦌ : SimplexCategory`.  -/
SimplexCategory.toTop₀ : CategoryTheory.CosimplicialObject TopCat
-- Mathlib.Tactic.Zify
Mathlib.Tactic.Zify.Nat.cast_sub_of_add_le : ∀ {R : Type u_1} [inst : AddGroupWithOne R] {m n k : ℕ}, m + k ≤ n → ↑(n - m) = ↑n - ↑m
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.mapHomologyIso_hom_naturality : ∀ {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] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : S₁.HasHomology]
  [inst_6 : S₂.HasHomology] [inst_7 : (S₁.map F).HasHomology] [inst_8 : (S₂.map F).HasHomology]
  [inst_9 : F.PreservesLeftHomologyOf S₁] [inst_10 : F.PreservesLeftHomologyOf S₂],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap (F.mapShortComplex.map φ))
      (S₂.mapHomologyIso F).hom =
    CategoryTheory.CategoryStruct.comp (S₁.mapHomologyIso F).hom (F.map (CategoryTheory.ShortComplex.homologyMap φ))
-- Init.Data.Ord.Basic
Ordering.isGT_swap : ∀ {o : Ordering}, o.swap.isGT = o.isLT
-- Mathlib.CategoryTheory.Comma.Over.OverClass
CategoryTheory.instHomIsOverOfIsOverTower : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (S S' : C)
  [inst_1 : CategoryTheory.CanonicallyOverClass X S] [inst_2 : CategoryTheory.OverClass X S']
  [inst_3 : CategoryTheory.OverClass Y S] [inst_4 : CategoryTheory.OverClass Y S']
  [inst_5 : CategoryTheory.OverClass S S'] [CategoryTheory.IsOverTower X S S'] [CategoryTheory.IsOverTower Y S S']
  [CategoryTheory.HomIsOver f S], CategoryTheory.HomIsOver f S'
-- Std.Data.Iterators.Lemmas.Producers.Vector
Array.iterFromIdx.eq_1 : ∀ {α : Type w} (l : Array α) (pos : ℕ), l.iterFromIdx pos = (l.iterFromIdxM Id pos).toIter
-- Init.Data.List.Sublist
List.dropWhile_subset : ∀ {α : Type u_1} {l : List α} (p : α → Bool), List.dropWhile p l ⊆ l
-- Mathlib.Order.Filter.Ultrafilter.Defs
/-- A filter equals the intersection of all the ultrafilters which contain it.  -/
Filter.iSup_ultrafilter_le_eq : ∀ {α : Type u} (f : Filter α), ⨆ g, ⨆ (_ : ↑g ≤ f), ↑g = f
-- Mathlib.FieldTheory.IsAlgClosed.Classification
/-- The cardinality of an algebraically closed `R`-algebra is less than or equal to
the maximum of the cardinality of `R`, the cardinality of a transcendence basis and
`ℵ₀`

For a simpler, but less universe-polymorphic statement, see
`IsAlgClosed.cardinal_le_max_transcendence_basis'`  -/
IsAlgClosed.cardinal_le_max_transcendence_basis : ∀ {R : Type u} {K : Type v} [inst : CommRing R] [inst_1 : Field K] [inst_2 : Algebra R K] [IsAlgClosed K] {ι : Type w}
  (v : ι → K),
  IsTranscendenceBasis R v →
    Cardinal.lift.{max u w, v} (Cardinal.mk K) ≤
      max (max (Cardinal.lift.{max v w, u} (Cardinal.mk R)) (Cardinal.lift.{max u v, w} (Cardinal.mk ι)))
        Cardinal.aleph0
-- Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
AddTorsor.iConvexComb_eq_affineCombination : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_3} {I : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  (s : Convexity.StdSimplex R I) (f : I → P),
  Convexity.iConvexComb s f = (Finset.affineCombination R s.weights.support f) ⇑s.weights
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infiniteNeg_iff_infinitesimal_inv_neg : ∀ {x : ℝ*}, x.InfiniteNeg ↔ x⁻¹.Infinitesimal ∧ x⁻¹ < 0
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubring.mem_toNonUnitalSubsemiring : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {s : NonUnitalSubring R} {x : R}, x ∈ s.toNonUnitalSubsemiring ↔ x ∈ s
-- Mathlib.CategoryTheory.Adhesive.Basic
CategoryTheory.IsPushout.isVanKampen_inl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W E X Z : C} (c : CategoryTheory.Limits.BinaryCofan W E)
  [CategoryTheory.FinitaryExtensive C] [CategoryTheory.Limits.HasPullbacks C] (hc : CategoryTheory.Limits.IsColimit c)
  (f : W ⟶ X) (h : X ⟶ Z) (i : c.pt ⟶ Z) (H : CategoryTheory.IsPushout f c.inl h i), H.IsVanKampen
-- Mathlib.CategoryTheory.Endomorphism
CategoryTheory.InducedCategory.endEquiv_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} {F : D → C}
  {X : CategoryTheory.InducedCategory C F} (f : X ⟶ X), CategoryTheory.InducedCategory.endEquiv f = f.hom
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.Measure.rnDeriv_withDensity_left : ∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → ENNReal} {μ ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ]
  [MeasureTheory.SigmaFinite ν],
  AEMeasurable f ν → (∀ᵐ (x : α) ∂μ, f x ≠ ⊤) → (μ.withDensity f).rnDeriv ν =ᵐ[ν] fun x => f x * μ.rnDeriv ν x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_erase!_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF → ∀ {k : α} {fallback : β k}, (Std.DTreeMap.Internal.Impl.erase! k t).getD k fallback = fallback
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.singleton_div : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Div α] {s : Finset α} (a : α),
  {a} / s = Finset.image (fun x => a / x) s
-- Mathlib.CategoryTheory.Functor.Derived.LeftDerived
CategoryTheory.Functor.IsLeftDerivedFunctor.isRightKanExtension : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_3} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Category.{v_3, u_2} D} {inst_2 : CategoryTheory.Category.{v_5, u_3} H}
  (LF : CategoryTheory.Functor D H) {F : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  (α : L.comp LF ⟶ F) (W : CategoryTheory.MorphismProperty C) {inst_3 : L.IsLocalization W}
  [self : LF.IsLeftDerivedFunctor α W], LF.IsRightKanExtension α
-- Mathlib.Order.Hom.Bounded
BotHom.comp.eq_1 : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Bot α] [inst_1 : Bot β] [inst_2 : Bot γ] (f : BotHom β γ)
  (g : BotHom α β), f.comp g = { toFun := ⇑f ∘ ⇑g, map_bot' := ⋯ }
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.unitAuxAuxAux_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A F : CategoryTheory.Functor Cᵒᵖ (Type v)} (η : F ⟶ A)
  (X : C),
  (CategoryTheory.OverPresheafAux.unitAuxAuxAux η X).hom =
    TypeCat.ofHom (CategoryTheory.OverPresheafAux.unitForward η X)
-- Lean.Util.ParamMinimizer
Lean.Util.ParamMinimizer.Result.mk : Lean.Util.ParamMinimizer.Status → Array Bool → ℕ → Lean.Util.ParamMinimizer.Result
-- Mathlib.Analysis.Normed.Operator.ContinuousLinearMap
LinearMap.toContinuousLinearMap₁_coe : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : IsBoundedSMul 𝕜 E] (f : 𝕜 →ₗ[𝕜] E), ↑f.toContinuousLinearMap₁ = f
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.mkL_apply_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] (x : E) (y : F),
  ((TensorProduct.mkL 𝕜 E F) x) y = x ⊗ₜ[𝕜] y
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.LevelMVarErrorInfo.mk.inj : ∀ {lctx : Lean.LocalContext} {expr : Lean.Expr} {ref : Lean.Syntax} {msgData? : Option Lean.MessageData}
  {lctx_1 : Lean.LocalContext} {expr_1 : Lean.Expr} {ref_1 : Lean.Syntax} {msgData?_1 : Option Lean.MessageData},
  { lctx := lctx, expr := expr, ref := ref, msgData? := msgData? } =
      { lctx := lctx_1, expr := expr_1, ref := ref_1, msgData? := msgData?_1 } →
    lctx = lctx_1 ∧ expr = expr_1 ∧ ref = ref_1 ∧ msgData? = msgData?_1
-- Lean.MetavarContext
Lean.MVarId.isDelayedAssigned : {m : Type → Type} → [Monad m] → [Lean.MonadMCtx m] → Lean.MVarId → m Bool
-- Mathlib.Order.UpperLower.Closure
UpperSet.upperClosure : ∀ {α : Type u_1} [inst : Preorder α] (s : UpperSet α), upperClosure ↑s = s
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
PresheafOfModules.Derivation.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} →
          {F : CategoryTheory.Functor C D} →
            {R : CategoryTheory.Functor Dᵒᵖ CommRingCat} →
              {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} →
                {φ : S ⟶ F.op.comp R} →
                  (d : {X : Dᵒᵖ} → ↑(R.obj X) →+ ↑(M.obj X)) →
                    autoParam (∀ {X : Dᵒᵖ} (a b : ↑(R.obj X)), d (a * b) = a • d b + b • d a)
                        PresheafOfModules.Derivation.d_mul._autoParam →
                      autoParam
                          (∀ {X Y : Dᵒᵖ} (f : X ⟶ Y) (x : ↑(R.obj X)),
                            d ((CategoryTheory.ConcreteCategory.hom (R.map f)) x) =
                              (CategoryTheory.ConcreteCategory.hom (M.map f)) (d x))
                          PresheafOfModules.Derivation.d_map._autoParam →
                        autoParam
                            (∀ {X : Cᵒᵖ} (a : ↑(S.obj X)), d ((CategoryTheory.ConcreteCategory.hom (φ.app X)) a) = 0)
                            PresheafOfModules.Derivation.d_app._autoParam →
                          M.Derivation φ
-- Lean.Meta.DiscrTree.Basic
_private.Lean.Meta.DiscrTree.Basic.0.Lean.Meta.DiscrTree.insertAux : {α : Type} → [BEq α] → Array Lean.Meta.DiscrTree.Key → α → ℕ → Lean.Meta.DiscrTree.Trie α → Lean.Meta.DiscrTree.Trie α
-- Mathlib.RingTheory.Polynomial.Nilpotent
Polynomial.isNilpotent_reflect_iff : ∀ {R : Type u_1} [inst : CommRing R] {P : Polynomial R} {N : ℕ},
  P.natDegree ≤ N → (IsNilpotent (Polynomial.reflect N P) ↔ IsNilpotent P)
-- Mathlib.Data.Set.Card
Set.encard_eq_two : ∀ {α : Type u_1} {s : Set α}, s.encard = 2 ↔ ∃ x y, x ≠ y ∧ s = {x, y}
-- Init.Sym.Lemmas
Lean.Sym.UInt64.eq_eq_true : ∀ (a b : UInt64), decide (a = b) = true → (a = b) = True
-- Mathlib.Analysis.Analytic.Basic
/-- Analytic everywhere implies continuous  -/
AnalyticOnNhd.continuous : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F},
  AnalyticOnNhd 𝕜 f Set.univ → Continuous f
-- Mathlib.Control.Monad.Basic
map_eq_bind_pure_comp : ∀ {α β : Type u} (m : Type u → Type v) [inst : Monad m] [LawfulMonad m] (f : α → β) (x : m α), f <$> x = x >>= pure ∘ f
-- Mathlib.Probability.Distributions.Poisson.Basic
/-- **Alias** of `ProbabilityTheory.hasSum_one_poissonMeasure`. -/
ProbabilityTheory.poissonPMFRealSum : ∀ (r : NNReal), HasSum (fun n => Real.exp (-↑r) * ↑r ^ n / ↑n.factorial) 1
-- Mathlib.Algebra.BigOperators.GroupWithZero.Action
Finset.prod_smul : ∀ {M : Type u_1} {N : Type u_2} {ι : Type u_4} [inst : CommMonoid N] [inst_1 : CommMonoid M] [inst_2 : MulAction M N]
  [IsScalarTower M N N] [SMulCommClass M N N] (s : Finset ι) (b : ι → M) (f : ι → N),
  ∏ i ∈ s, b i • f i = (∏ i ∈ s, b i) • ∏ i ∈ s, f i
-- Lean.DocString.Types
Lean.Doc.instInhabitedInline : {a : Type u_1} → Inhabited (Lean.Doc.Inline a)
-- Mathlib.RingTheory.WittVector.Defs
/-- The polynomials used for defining repeated addition of the ring of Witt vectors.  -/
WittVector.wittPow : (p : ℕ) → [hp : Fact (Nat.Prime p)] → ℕ → ℕ → MvPolynomial (Fin 1 × ℕ) ℤ
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
AlgebraicIndependent.isTranscendenceBasis_of_lift_trdeg_le_of_finite : ∀ {ι : Type u} {R : Type u_1} {A : Type w} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Nontrivial R] [NoZeroDivisors A] [Finite ι],
  AlgebraicIndependent R x →
    Cardinal.lift.{u, w} (Algebra.trdeg R A) ≤ Cardinal.lift.{w, u} (Cardinal.mk ι) → IsTranscendenceBasis R x
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxc.Iterator.isSome_next_of_isPlausibleIndirectOutput : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LE α] [inst_2 : DecidableLE α] {it : Std.Iter α}
  {out : α}, it.IsPlausibleIndirectOutput out → it.internalState.next.isSome = true
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
/-- The closed interior is the union of the open interior and the surface.  -/
Affine.Simplex.closedInterior_eq_interior_union : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [inst_4 : LinearOrder k] [IsOrderedAddMonoid k] [ZeroLEOneClass k] {n : ℕ}
  [inst_7 : NeZero n] (s : Affine.Simplex k P n), s.closedInterior = s.interior ∪ ⋃ i, (s.faceOpposite i).closedInterior
-- Mathlib.CategoryTheory.Topos.Sheaf
/-- Sheaf categories on essentially small sites have a subobject classifier.  -/
CategoryTheory.Sheaf.instHasSubobjectClassifierTypeOfEssentiallySmall : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [CategoryTheory.EssentiallySmall.{w, v, u} C], CategoryTheory.HasSubobjectClassifier (CategoryTheory.Sheaf J (Type w))
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
/-- Constructor for isomorphisms in `DescentDataAsCoalgebra`.  -/
CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.isoMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F :
        CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
          (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)} →
      {ι : Type t} →
        {S : C} →
          {X : ι → C} →
            {f : (i : ι) → X i ⟶ S} →
              {D₁ D₂ : F.DescentDataAsCoalgebra f} →
                (e : (i : ι) → D₁.obj i ≅ D₂.obj i) →
                  autoParam
                      (∀ (i₁ i₂ : ι),
                        CategoryTheory.CategoryStruct.comp (D₁.hom i₁ i₂)
                            ((F.map (f i₁).op.toLoc).l.toFunctor.map
                              ((F.map (f i₂).op.toLoc).r.toFunctor.map (e i₂).hom)) =
                          CategoryTheory.CategoryStruct.comp (e i₁).hom (D₂.hom i₁ i₂))
                      CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.isoMk._auto_1 →
                    (D₁ ≅ D₂)
-- Mathlib.RingTheory.Spectrum.Prime.Topology
/-- [Stacks Tag 00EE](https://stacks.math.columbia.edu/tag/00EE) -/
PrimeSpectrum.existsUnique_idempotent_basicOpen_eq_of_isClopen : ∀ {R : Type u} [inst : CommSemiring R] {s : Set (PrimeSpectrum R)},
  IsClopen s → ∃! e, IsIdempotentElem e ∧ s = ↑(PrimeSpectrum.basicOpen e)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
/-- The map of an empty cone is a limit iff the mapped object is terminal.
 -/
CategoryTheory.Limits.isLimitMapConeEmptyConeEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          (X : C) →
            CategoryTheory.Limits.IsLimit (G.mapCone (CategoryTheory.Limits.asEmptyCone X)) ≃
              CategoryTheory.Limits.IsTerminal (G.obj X)
-- Mathlib.SetTheory.Cardinal.Arithmetic
/-- If `α` is an infinite type, then the cardinality of `α ⊕ β` is the maximum
of the cardinalities of `α` and `β`.  -/
Cardinal.add_eq_max : ∀ {a b : Cardinal.{u_1}}, Cardinal.aleph0 ≤ a → a + b = max a b
-- Lean.Elab.Quotation
Lean.Elab.Term.Quotation.HeadCheck.other.sizeOf_spec : ∀ (pat : Lean.Syntax), sizeOf (Lean.Elab.Term.Quotation.HeadCheck.other pat) = 1 + sizeOf pat
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearEquiv.congr_trans_lTensor : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} {S : Type u_11}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : AddCommMonoid S] [inst_6 : Module R M] [inst_7 : Module R N] [inst_8 : Module R S] [inst_9 : Module R P]
  [inst_10 : Module R Q] (g' : Q ≃ₗ[R] S) (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q),
  TensorProduct.congr f g ≪≫ₗ LinearEquiv.lTensor P g' = TensorProduct.congr f (g ≪≫ₗ g')
-- Mathlib.Algebra.Pointwise.Stabilizer
AddAction.stabilizer_univ : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α], AddAction.stabilizer G Set.univ = ⊤
-- Mathlib.RingTheory.PowerSeries.Basic
Polynomial.coe_X : ∀ {R : Type u_1} [inst : Semiring R], ↑Polynomial.X = PowerSeries.X
-- Mathlib.SetTheory.Cardinal.NatCard
Set.ecard_le_ecard : ∀ {α : Type u_1} {s t : Set α}, s ⊆ t → ENat.card ↑s ≤ ENat.card ↑t
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.SyntheticMVarDecl.mk.injEq : ∀ (stx : Lean.Syntax) (kind : Lean.Elab.Term.SyntheticMVarKind) (stx_1 : Lean.Syntax)
  (kind_1 : Lean.Elab.Term.SyntheticMVarKind),
  ({ stx := stx, kind := kind } = { stx := stx_1, kind := kind_1 }) = (stx = stx_1 ∧ kind = kind_1)
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.lintegral_restrict : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set β}
  (κ : ProbabilityTheory.Kernel α β) (hs : MeasurableSet s) (a : α) (f : β → ENNReal),
  ∫⁻ (b : β), f b ∂(κ.restrict hs) a = ∫⁻ (b : β) in s, f b ∂κ a
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.instInhabitedSimpKind : Inhabited Lean.Elab.Tactic.SimpKind
-- Init.Data.SInt.Bitwise
Int16.toInt32_or : ∀ (a b : Int16), (a ||| b).toInt32 = a.toInt32 ||| b.toInt32
-- Mathlib.Analysis.Normed.Module.Basic
/-- A non-unital algebra homomorphism from an `Algebra` to a `NormedAlgebra` induces a
`NormedAlgebra` structure on the domain, using the `SeminormedRing.induced` norm.

See note [reducible non-instances]  -/
NormedAlgebra.induced : {F : Type u_6} →
  (𝕜 : Type u_7) →
    (R : Type u_8) →
      (S : Type u_9) →
        [inst : NormedField 𝕜] →
          [inst_1 : Ring R] →
            [inst_2 : Algebra 𝕜 R] →
              [inst_3 : SeminormedRing S] →
                [inst_4 : NormedAlgebra 𝕜 S] →
                  [inst_5 : FunLike F R S] → [inst_6 : NonUnitalAlgHomClass F 𝕜 R S] → (f : F) → NormedAlgebra 𝕜 R
-- Lean.Elab.BuiltinNotation
Lean.Elab.Term.expandTuple : Lean.Macro
-- Mathlib.Topology.Separation.Basic
t1Space_of_injective_of_continuous : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Function.Injective f → Continuous f → ∀ [T1Space Y], T1Space X
-- Mathlib.Algebra.Module.Presentation.Basic
/-- The type of solutions in a module `M` of the equations given by `relations : Relations A`.  -/
Module.Relations.Solution : {A : Type u} →
  [inst : Ring A] → Module.Relations A → (M : Type v) → [inst_1 : AddCommGroup M] → [Module A M] → Type (max v w₀)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.simp_cert.eq_1 : ∀ (k₁ : ℤ) (p₁ : Lean.Grind.CommRing.Poly) (k₂ : ℤ) (m₂ : Lean.Grind.CommRing.Mon) (p₂ p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Stepwise.simp_cert k₁ p₁ k₂ m₂ p₂ p =
    ((Lean.Grind.CommRing.Poly.mulConst_k k₁ p₁).combine_k (Lean.Grind.CommRing.Poly.mulMon_k k₂ m₂ p₂)).beq' p
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.coe_pow : ∀ (z : Complex.UnitDisc) (n : ℕ+), ↑(z ^ n) = ↑z ^ ↑n
-- Batteries.Data.Float.Lemmas
Float.Model.UnpackedFloat.Sign.ofBitVec_toBitVec : ∀ (s : Float.Model.UnpackedFloat.Sign), Float.Model.UnpackedFloat.Sign.ofBitVec s.toBitVec = s
-- Mathlib.CategoryTheory.Limits.Sifted
/-- Being sifted is preserved by equivalences of categories  -/
CategoryTheory.IsSifted.isSifted_of_equiv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsSifted C] {D : Type u₁}
  [inst_2 : CategoryTheory.Category.{v₁, u₁} D] (e : D ≌ C), CategoryTheory.IsSifted D