mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.instCharZero : CharZero Ordinal.{u_4}
-- Lean.Elab.Tactic.Omega.Core
/-- Constructing the proof term for `addInequality`.  -/
Lean.Elab.Tactic.Omega.Problem.addInequality_proof : ℤ → Lean.Omega.Coeffs → Lean.Elab.Tactic.Omega.Proof → Lean.Elab.Tactic.Omega.Proof
-- Mathlib.Data.Stream.Init
Stream'.drop_const : ∀ {α : Type u} (n : ℕ) (a : α), Stream'.drop n (Stream'.const a) = Stream'.const a
-- Mathlib.Algebra.Polynomial.Laurent
/-- The support of a polynomial `f` is a finset in `ℕ`.  The lemma `toLaurent_support f`
shows that the support of `f.toLaurent` is the same finset, but viewed in `ℤ` under the natural
inclusion `ℕ ↪ ℤ`.  -/
LaurentPolynomial.support_coeff_toLaurent : ∀ {R : Type u_1} [inst : Semiring R] (f : Polynomial R),
  (Polynomial.toLaurent f).coeff.support = Finset.map Nat.castEmbedding f.support
-- Mathlib.Util.Notation3
/-- The arrays of delaborated `Term`s accumulated while matching
`foldl` and `foldr` expressions. For `foldl`, the arrays are stored in reverse order.  -/
Mathlib.Notation3.MatchState.foldState : Mathlib.Notation3.MatchState → Std.HashMap Lean.Name (Array Lean.Term)
-- Mathlib.SetTheory.ZFC.PSet
PSet.Mem.mk : ∀ {α : Type u} (A : α → PSet.{u}) (a : α), A a ∈ PSet.mk α A
-- Mathlib.Algebra.Order.Ring.WithTop
WithBot.instSemigroupWithZero : {α : Type u_1} → [DecidableEq α] → [inst : SemigroupWithZero α] → [NoZeroDivisors α] → SemigroupWithZero (WithBot α)
-- Mathlib.Topology.MetricSpace.Pseudo.Basic
/-- Given a point `x` in a discrete subset `s` of a pseudometric space, there is a closed ball
of positive radius centered at `x` and intersecting `s` only at `x`.  -/
Metric.exists_closedBall_inter_eq_singleton_of_discrete : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α},
  IsDiscrete s → ∀ {x : α}, x ∈ s → ∃ ε > 0, Metric.closedBall x ε ∩ s = {x}
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- An oriented angle is not zero and `π` if and only if the three points are not collinear.  -/
EuclideanGeometry.oangle_ne_zero_and_ne_pi_iff_not_collinear : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P},
  EuclideanGeometry.oangle p₁ p₂ p₃ ≠ 0 ∧ EuclideanGeometry.oangle p₁ p₂ p₃ ≠ ↑Real.pi ↔ ¬Collinear ℝ {p₁, p₂, p₃}
-- Lean.Compiler.Specialize
Lean.Compiler.SpecializeAttributeKind.nospecialize.sizeOf_spec : sizeOf Lean.Compiler.SpecializeAttributeKind.nospecialize = 1
-- Init.Data.AC
Lean.Data.AC.Expr.var.sizeOf_spec : ∀ (x : ℕ), sizeOf (Lean.Data.AC.Expr.var x) = 1 + sizeOf x
-- Mathlib.LinearAlgebra.PiTensorProduct.Dual
/-- An inverse to `PiTensorProduct.dualDistrib` given bases.  -/
PiTensorProduct.dualDistribInvOfBasis : {ι : Type u_1} →
  {R : Type u_2} →
    {κ : ι → Type u_3} →
      {M : ι → Type u_4} →
        [inst : CommRing R] →
          [inst_1 : (i : ι) → AddCommGroup (M i)] →
            [inst_2 : (i : ι) → Module R (M i)] →
              [Finite ι] →
                [∀ (i : ι), Finite (κ i)] →
                  ((i : ι) → Module.Basis (κ i) R (M i)) →
                    Module.Dual R (PiTensorProduct R fun i => M i) →ₗ[R] PiTensorProduct R fun i => Module.Dual R (M i)
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_obj_d_f : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (α : Type u_3)
  [inst_2 : AddRightCancelSemigroup α] [inst_3 : One α]
  (P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C (ComplexShape.down α))) (i j : α),
  (((CategoryTheory.Idempotents.karoubiChainComplexEquivalence C α).functor.obj P).d i j).f =
    CategoryTheory.CategoryStruct.comp (P.X.d i j) (P.p.f j)
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.DateBuilder.w : Std.Time.GenericFormat.DateBuilder✝ → Option Std.Time.Week.OfYear.Ordinal
-- Mathlib.LinearAlgebra.Finsupp.LSum
Submodule.mulLeftMap.congr_simp : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_4} [inst_1 : Semiring S] [inst_2 : Module R S]
  [inst_3 : SMulCommClass R R S] [inst_4 : SMulCommClass R S S] {M : Submodule R S} (N : Submodule R S) {ι : Type u_5}
  (m m_1 : ι → ↥M), m = m_1 → Submodule.mulLeftMap N m = Submodule.mulLeftMap N m_1
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- 7.6(a) from [axler2024].
See `ContinuousLinearMap.orthogonal_range` for the infinite-dimensional version.  -/
LinearMap.orthogonal_range : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : FiniteDimensional 𝕜 E] [inst_6 : FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F),
  A.rangeᗮ = (LinearMap.adjoint A).ker
-- Mathlib.Topology.Algebra.Algebra
/-- Composition of continuous algebra homomorphisms.  -/
ContinuousAlgHom.comp : {R : Type u_1} →
  [inst : CommSemiring R] →
    {A : Type u_2} →
      [inst_1 : Semiring A] →
        [inst_2 : TopologicalSpace A] →
          {B : Type u_3} →
            [inst_3 : Semiring B] →
              [inst_4 : TopologicalSpace B] →
                [inst_5 : Algebra R A] →
                  [inst_6 : Algebra R B] →
                    {C : Type u_4} →
                      [inst_7 : Semiring C] →
                        [inst_8 : Algebra R C] → [inst_9 : TopologicalSpace C] → (B →A[R] C) → (A →A[R] B) → A →A[R] C
-- Mathlib.Data.Nat.ModEq
Nat.modEq_add_modulus_iff : ∀ {n a b : ℕ}, a ≡ b + n [MOD n] ↔ a ≡ b [MOD n]
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
/-- A family of friendly operations on multiseries indexed by a type `γ`.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperationClass : {basis_hd : ℝ → ℝ} →
  {basis_tl : Tactic.ComputeAsymptotics.Basis} →
    {γ : Type u_1} →
      (γ →
          Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl →
            Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl) →
        Prop
-- Mathlib.Order.CompleteLattice.Basic
iInf_image2 : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {γ : Type u_8} {δ : Type u_9} (f : β → γ → δ) (s : Set β)
  (t : Set γ) (g : δ → α), ⨅ d ∈ Set.image2 f s t, g d = ⨅ b ∈ s, ⨅ c ∈ t, g (f b c)
-- Lean.SubExpr
/-- Creates a subexpression `Pos` from an array of 'coordinates'.
Each coordinate is a number {0,1,2} expressing which child subexpression should be explored.
The first coordinate in the array corresponds to the root of the expression tree.   -/
Lean.SubExpr.Pos.ofArray : Array ℕ → Lean.SubExpr.Pos
-- Init.Data.String.Lemmas.StringOrder
String.not_le : ∀ {a b : String}, ¬a ≤ b ↔ b < a
-- Mathlib.Algebra.Module.Torsion.Basic
/-- **Alias** of `isAddTorsion_iff_isTorsion_nat`. -/
AddMonoid.isTorsion_iff_isTorsion_nat : ∀ {M : Type u_2} [inst : AddCommMonoid M], IsAddTorsion M ↔ Module.IsTorsion ℕ M
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.maxKey?_alter_eq_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α}
  {f : Option β → Option β},
  (Std.DTreeMap.Const.alter t k f).maxKey? = some k ↔
    (f (Std.DTreeMap.Const.get? t k)).isSome = true ∧ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.maxView_kv_eq_maxView! : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β} {hl : l.Balanced}
  {hr : r.Balanced} {hlr : Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size r.size},
  ⟨(Std.DTreeMap.Internal.Impl.maxView k v l r hl hr hlr).k, (Std.DTreeMap.Internal.Impl.maxView k v l r hl hr hlr).v⟩ =
    ⟨(Std.DTreeMap.Internal.Impl.maxView! k v l r).k, (Std.DTreeMap.Internal.Impl.maxView! k v l r).v⟩
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryCofan.mk_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y P : C} (ι₁ : X ⟶ P) (ι₂ : Y ⟶ P),
  (CategoryTheory.Limits.BinaryCofan.mk ι₁ ι₂).pt = P
-- Aesop.Index
Aesop.Index.foldM : {α : Type} → {m : Type u_1 → Type u_2} → {σ : Type u_1} → [Monad m] → Aesop.Index α → (σ → Aesop.Rule α → m σ) → σ → m σ
-- Init.Data.String.Lemmas.Pattern.Memcmp
_private.Init.Data.String.Lemmas.Pattern.Memcmp.0.String.Slice.Pattern.Internal.memcmpSlice.eq_1 : ∀ (lhs rhs : String.Slice) (lstart rstart len : String.Pos.Raw) (h1 : len.offsetBy lstart ≤ lhs.rawEndPos)
  (h2 : len.offsetBy rstart ≤ rhs.rawEndPos),
  String.Slice.Pattern.Internal.memcmpSlice lhs rhs lstart rstart len h1 h2 =
    String.Slice.Pattern.Internal.memcmpStr lhs.str rhs.str (lstart.offsetBy lhs.startInclusive.offset)
      (rstart.offsetBy rhs.startInclusive.offset) len ⋯ ⋯
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : BEq α] [inst_2 : Std.LawfulBEqOrd α] [inst_3 : Std.LawfulEqOrd α] (h : t.WF) {l : List ((a : α) × β a)}
  {k : α} (contains : (List.map Sigma.fst l).contains k = false) {h' : k ∈ ↑(t.insertMany l ⋯)},
  (↑(t.insertMany l ⋯)).get k h' = t.get k ⋯
-- Mathlib.Data.QPF.Multivariate.Constructions.Cofix
MvQPF.Cofix.repr.eq_1 : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n},
  MvQPF.Cofix.repr = MvPFunctor.M.corec (MvQPF.P F) (MvQPF.repr ∘ MvQPF.Cofix.dest)
-- Mathlib.Algebra.Homology.ImageToKernel
/-- `imageToKernel` for `A --f--> B --0--> C`, where `g` is an epi is itself an epi
(i.e. the sequence is exact at `B`).
 -/
imageToKernel_epi_of_epi_of_zero : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V}
  (f : A ⟶ B) [inst_2 : CategoryTheory.Limits.HasImages V] [CategoryTheory.Epi f],
  CategoryTheory.Epi (imageToKernel f 0 ⋯)
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.forget_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : CategoryTheory.CommMon C),
  (CategoryTheory.CommMon.forget C).obj X = X.X
-- Mathlib.Order.Disjoint
Disjoint.of_disjoint_inf_of_le' : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {a b c : α}, Disjoint (a ⊓ b) c → b ≤ c → Disjoint a b
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_eq_some_getKey!_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {a : α}, t.contains a = true → t.getKey? a = some (t.getKey! a)
-- Aesop.RuleTac.Apply
Aesop.RuleTac.applyConst : Lean.Name → Lean.Meta.TransparencyMode → Aesop.RuleTac
-- Mathlib.Topology.Order.MonotoneConvergence
/-- proof that a monotone function tends to `𝓝 a` as `x → -∞`  -/
InfConvergenceClass.tendsto_coe_atBot_isGLB : ∀ {α : Type u_3} {inst : Preorder α} {inst_1 : TopologicalSpace α} [self : InfConvergenceClass α] (a : α) (s : Set α),
  IsGLB s a → Filter.Tendsto Subtype.val Filter.atBot (nhds a)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
/-- If `w : InfinitePlace L` lies above `v : InfinitePlace K` and `w` is real, then so is `v`.  -/
NumberField.InfinitePlace.LiesOver.isReal_of_isReal_over : ∀ {K : Type u_4} {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (w : NumberField.InfinitePlace L) {v : NumberField.InfinitePlace K} [w.LiesOver v], w.IsReal → v.IsReal
-- Mathlib.Order.Antisymmetrization
AntisymmRel.antisymmRel_congr : ∀ {α : Type u_1} {a b c d : α} [inst : Preorder α],
  AntisymmRel (fun x1 x2 => x1 ≤ x2) a b →
    AntisymmRel (fun x1 x2 => x1 ≤ x2) c d →
      (AntisymmRel (fun x1 x2 => x1 ≤ x2) a c ↔ AntisymmRel (fun x1 x2 => x1 ≤ x2) b d)
-- Init.Data.String.Lemmas.Order
String.Pos.le_ofSlice_iff : ∀ {s : String} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos},
  q ≤ String.Pos.ofSlice p ↔ ∃ (h₁ : q ≤ p₁), ∀ (h₀ : p₀ ≤ q), q.slice p₀ p₁ h₀ h₁ ≤ p
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.map_iSup : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S] {F : Type u_1}
  [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] {ι : Sort u_2} (f : F)
  (s : ι → NonUnitalSubsemiring R), NonUnitalSubsemiring.map f (iSup s) = ⨆ i, NonUnitalSubsemiring.map f (s i)
-- Mathlib.Topology.AlexandrovDiscrete
Pi.instAlexandrovDiscreteOfFinite : ∀ {ι : Type u_5} [Finite ι] {X : ι → Type u_6} [inst : (i : ι) → TopologicalSpace (X i)]
  [∀ (i : ι), AlexandrovDiscrete (X i)], AlexandrovDiscrete ((i : ι) → X i)
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
/-- The derivative of `det (1 + M X)` at `0` is the trace of `M`.  -/
Matrix.derivative_det_one_add_X_smul : ∀ {R : Type u} [inst : CommRing R] {n : Type v} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n R),
  Polynomial.eval 0 (Polynomial.derivative (1 + Polynomial.X • M.map ⇑Polynomial.C).det) = M.trace
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.counitIso_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι},
  CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.counitIso.inv = CategoryTheory.eqToHom ⋯
-- Mathlib.Topology.JacobsonSpace
nonempty_inter_closedPoints : ∀ {X : Type u_1} [inst : TopologicalSpace X] [JacobsonSpace X] {Z : Set X},
  Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty
-- Mathlib.Algebra.Module.LinearMap.End
Module.End.instMonoid : {R : Type u_1} →
  {M : Type u_4} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Monoid (Module.End R M)
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Λ'.read : (Option Turing.PartrecToTM2.Γ' → Turing.PartrecToTM2.Λ') → Turing.PartrecToTM2.Λ'
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- The oriented angle between two vectors is zero if and only if the angle with the vectors
swapped is zero.  -/
Orientation.oangle_eq_zero_iff_oangle_rev_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = 0 ↔ o.oangle y x = 0
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Three
/-- We have that `x ^ 3 - 1 = (x - 1) * (x - η) * (x - η ^ 2)`.  -/
IsCyclotomicExtension.Rat.Three.cube_sub_one_eq_mul : ∀ {K : Type u_1} [inst : Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ 3) (x : NumberField.RingOfIntegers K),
  x ^ 3 - 1 = (x - 1) * (x - ↑⋯.unit) * (x - ↑⋯.unit ^ 2)
-- Mathlib.Analysis.Normed.Operator.Basic
closedBall_subset_range_iff_surjective : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} {𝓕 : Type u_8} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : FunLike 𝓕 E F]
  [SemilinearMapClass 𝓕 σ₁₂ E F] [RingHomSurjective σ₁₂] {f : 𝓕} (x : F) {r : ℝ},
  0 < r → (Metric.closedBall x r ⊆ Set.range ⇑f ↔ Function.Surjective ⇑f)
-- Mathlib.Topology.ContinuousMap.StoneWeierstrass
ContinuousMap.adjoin_id_eq_span_one_add : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] (s : Set 𝕜),
  ↑(StarAlgebra.adjoin 𝕜 {ContinuousMap.restrict s (ContinuousMap.id 𝕜)}) =
    ↑(𝕜 ∙ 1) + ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMap.restrict s (ContinuousMap.id 𝕜)})
-- Mathlib.Topology.Algebra.MulAction
Filter.Tendsto.vadd_const : ∀ {M : Type u_1} {X : Type u_2} {α : Type u_4} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X]
  [inst_2 : VAdd M X] [ContinuousVAdd M X] {f : α → M} {l : Filter α} {c : M},
  Filter.Tendsto f l (nhds c) → ∀ (a : X), Filter.Tendsto (fun x => f x +ᵥ a) l (nhds (c +ᵥ a))
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.of_apply : ∀ {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] [inst_1 : DecidableEq ι] {i : ι} (j : ι)
  (x : β i), ((DirectSum.of β i) x) j = if h : i = j then Eq.recOn h x else 0
-- Lean.Elab.DocString
Lean.Doc.State.mk.inj : ∀ {scopes : List Lean.Elab.Command.Scope} {openDecls : List Lean.OpenDecl} {lctx : Lean.LocalContext}
  {localInstances : Lean.LocalInstances} {options : Lean.Options} {scopes_1 : List Lean.Elab.Command.Scope}
  {openDecls_1 : List Lean.OpenDecl} {lctx_1 : Lean.LocalContext} {localInstances_1 : Lean.LocalInstances}
  {options_1 : Lean.Options},
  { scopes := scopes, openDecls := openDecls, lctx := lctx, localInstances := localInstances, options := options } =
      { scopes := scopes_1, openDecls := openDecls_1, lctx := lctx_1, localInstances := localInstances_1,
        options := options_1 } →
    scopes = scopes_1 ∧
      openDecls = openDecls_1 ∧ lctx = lctx_1 ∧ localInstances = localInstances_1 ∧ options = options_1
-- Std.Do.WP.Sound
/-- Soundness lemma for `Option`: `Id`-specialization of `OptionT.of_wp_run`.  -/
Std.Do.Option.of_wp_eq : ∀ {α : Type} {x prog : Option α},
  prog = x →
    ∀ (P : Option α → Prop), (⊢ₛ (Std.Do.wp prog).apply (fun a => ⌜P (some a)⌝, fun x => ⌜P none⌝, PUnit.unit)) → P x
-- Mathlib.Data.Set.Function
Set.InjOn.cancel_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {f₁ f₂ : α → β} {g : β → γ},
  Set.InjOn g t → Set.MapsTo f₁ s t → Set.MapsTo f₂ s t → (Set.EqOn (g ∘ f₁) (g ∘ f₂) s ↔ Set.EqOn f₁ f₂ s)
-- Mathlib.Algebra.Homology.HomologicalBicomplex
/-- The graded object indexed by `I₁ × I₂` induced by a bicomplex.  -/
HomologicalComplex₂.toGradedObject : {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₂} → HomologicalComplex₂ C c₁ c₂ → CategoryTheory.GradedObject (I₁ × I₂) C
-- Mathlib.Topology.Homotopy.Path
Path.Homotopy.map_apply : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x₀ x₁ : X} {p q : Path x₀ x₁}
  (F : p.Homotopy q) (f : C(X, Y)) (a : ↑unitInterval × ↑unitInterval), (F.map f) a = (⇑f ∘ ⇑F) a
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.dropWhile_eq_self_iff_or : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s : String.Slice},
  s.dropWhile pat = s ↔
    ¬String.Slice.Pattern.Model.MatchesAt pat s.startPos ∨ String.Slice.Pattern.Model.IsLongestMatch pat s.startPos
-- Mathlib.CategoryTheory.Subterminal
/-- If the diagonal morphism of `A` is an isomorphism, then it is subterminal.
The converse of `isSubterminal.isIso_diag`.
 -/
CategoryTheory.isSubterminal_of_isIso_diag : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct A A] [CategoryTheory.IsIso (CategoryTheory.Limits.diag A)],
  CategoryTheory.IsSubterminal A
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsLink.mono : ∀ {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G H : Graph α β}, H ≤ G → H.IsLink e x y → G.IsLink e x y
-- Mathlib.Analysis.Convex.MetricSpace
Convexity.dist_convexCombPair_right : ∀ {X : Type u_2} [inst : Convexity.ConvexSpace ℝ X] [inst_1 : MetricSpace X] [Convexity.IsConvexDist X] {s t : ℝ}
  (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : X), dist (Convexity.convexCombPair s t hs ht h x y) y = s * dist x y
-- Lean.Meta.Tactic.Grind.Arith.Util
/-- Returns `true` if `e` is a numeral supported by cutsat.  -/
Lean.Meta.Grind.Arith.isNum : Lean.Expr → Bool
-- Mathlib.Topology.Separation.Basic
exists_isOpen_xor_mem : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T0Space X] {x y : X}, x ≠ y → ∃ U, IsOpen U ∧ Xor (x ∈ U) (y ∈ U)
-- Lean.Compiler.IR.Basic
Lean.IR.IRType.tagged.sizeOf_spec : sizeOf Lean.IR.IRType.tagged = 1
-- Mathlib.Data.Fin.SuccPred
/-- `pred` commutes with `succAbove`.  -/
Fin.pred_succAbove_pred : ∀ {n : ℕ} {a : Fin (n + 2)} {b : Fin (n + 1)} (ha : a ≠ 0) (hb : b ≠ 0) (hk : optParam (a.succAbove b ≠ 0) ⋯),
  (a.pred ha).succAbove (b.pred hb) = (a.succAbove b).pred hk
-- Mathlib.Topology.Algebra.Polynomial
Polynomial.continuousAt_aeval : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : TopologicalSpace A] [IsTopologicalSemiring A] (p : Polynomial R) {a : A},
  ContinuousAt (fun x => (Polynomial.aeval x) p) a
-- Mathlib.GroupTheory.Exponent
Monoid.ExponentExists.of_finite : ∀ {G : Type u} [inst : LeftCancelMonoid G] [Finite G], Monoid.ExponentExists G
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
ProbabilityTheory.HasGaussianLaw.fun_add : ∀ {Ω : Type u_1} {E : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : MeasurableSpace E] [BorelSpace E] {X : Ω → E} [inst_3 : NormedSpace ℝ E] [SecondCountableTopology E]
  {Y : Ω → E},
  ProbabilityTheory.HasGaussianLaw (fun ω => (X ω, Y ω)) P → ProbabilityTheory.HasGaussianLaw (fun ω => X ω + Y ω) P
-- Mathlib.NumberTheory.Divisors
Int.divisorsAntidiag_zero : Int.divisorsAntidiag 0 = ∅
-- Mathlib.Algebra.Category.Ring.Basic
CategoryTheory.Iso.ringCatIsoToRingEquiv_toRingHom : ∀ {R S : RingCat} (e : R ≅ S), ↑e.ringCatIsoToRingEquiv = RingCat.Hom.hom e.hom
-- Mathlib.Algebra.Exact.Basic
Function.Exact.linearMap_ker_eq : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {P : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P}, Function.Exact ⇑f ⇑g → g.ker = f.range
-- Lean.Elab.Do.Basic
Lean.Elab.Do.MonadInfo : Type
-- Init.Data.List.Lemmas
List.foldr_cons_eq_append : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : α → β} {l' : List β},
  List.foldr (fun x ys => f x :: ys) l' l = List.map f l ++ l'
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.step_filterMapWithPostcondition.match_3.eq_3 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (h : it.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (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.done, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_3 h
-- Mathlib.AlgebraicGeometry.Cover.Open
AlgebraicGeometry.Scheme.AffineOpenCover.openCover_X : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.AffineOpenCover) (j : 𝒰.I₀), 𝒰.openCover.X j = AlgebraicGeometry.Spec (𝒰.X j)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.homologyOpIso_hom_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap (CategoryTheory.ShortComplex.opMap φ))
      S₁.homologyOpIso.hom =
    CategoryTheory.CategoryStruct.comp S₂.homologyOpIso.hom (CategoryTheory.ShortComplex.homologyMap φ).op
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinOrder.finite_powers : ∀ {G : Type u_1} [inst : Monoid G] {a : G}, IsOfFinOrder a → (↑(Submonoid.powers a)).Finite