mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Ring.Subsemiring.Defs
/-- Copy of a subsemiring with a new `carrier` equal to the old one. Useful to fix definitional
equalities.  -/
Subsemiring.copy : {R : Type u} → [inst : NonAssocSemiring R] → (S : Subsemiring R) → (s : Set R) → s = ↑S → Subsemiring R
-- Mathlib.Data.SetLike.Basic
/-- **Alias** of `SetLike.setOfPred_mem_eq`. -/
SetLike.setOf_mem_eq : ∀ {A : Type u_1} {B : Type u_2} [i : SetLike A B] (a : A), {b | b ∈ a} = ↑a
-- Mathlib.NumberTheory.NumberField.Basic
/-- The ring of integers of `ℚ` as a number field is just `ℤ`.  -/
Rat.ringOfIntegersEquiv : NumberField.RingOfIntegers ℚ ≃+* ℤ
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_singleton_one : ∀ {α : Type u} [inst : Semiring α], Ideal.span {1} = ⊤
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
linearIndepOn_id_iUnion_finite : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {f : ι → Set M},
  (∀ (i : ι), LinearIndepOn R id (f i)) →
    (∀ (i : ι) (t : Set ι), t.Finite → i ∉ t → Disjoint (Submodule.span R (f i)) (⨆ i ∈ t, Submodule.span R (f i))) →
      LinearIndepOn R id (⋃ i, f i)
-- Mathlib.Logic.Function.Basic
Function.surjInv.congr_simp : ∀ {α : Sort u} {β : Sort v} {f f_1 : α → β} (e_f : f = f_1) (h : Function.Surjective f) (b b_1 : β),
  b = b_1 → Function.surjInv h b = Function.surjInv ⋯ b_1
-- Mathlib.Order.Filter.Pointwise
Filter.NeBot.of_smul_filter : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {f : Filter β} {a : α}, (a • f).NeBot → f.NeBot
-- Mathlib.Algebra.Order.Module.PositiveLinearMap
PositiveLinearMap.ext_iff : ∀ {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid E₁]
  [inst_2 : PartialOrder E₁] [inst_3 : AddCommMonoid E₂] [inst_4 : PartialOrder E₂] [inst_5 : Module R E₁]
  [inst_6 : Module R E₂] {f g : E₁ →ₚ[R] E₂}, f = g ↔ ∀ (x : E₁), f x = g x
-- Lean.DocString.Parser
/-- Parses zero or more blocks.
 -/
Lean.Doc.Parser.blocks : Lean.Doc.Parser.BlockCtxt → Lean.Parser.ParserFn
-- Mathlib.Algebra.Module.Submodule.Map
/-- A linear equivalence of two modules restricts to a linear equivalence from any submodule
`p` of the domain onto the image of that submodule.

This is the linear version of `AddEquiv.submonoidMap` and `AddEquiv.subgroupMap`.

This is `LinearEquiv.ofSubmodule'` but with `map` on the right instead of `comap` on the left.  -/
LinearEquiv.submoduleMap : {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₂] →
                {module_M : Module R M} →
                  {module_M₂ : Module R₂ M₂} →
                    {σ₁₂ : R →+* R₂} →
                      {σ₂₁ : R₂ →+* R} →
                        {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} →
                          {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} →
                            (e : M ≃ₛₗ[σ₁₂] M₂) → (p : Submodule R M) → ↥p ≃ₛₗ[σ₁₂] ↥(Submodule.map (↑e) p)
-- Mathlib.Logic.Relation
Relation.map_onFun_map_eq_map : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} (f : α → β),
  Relation.Map (Function.onFun (Relation.Map r f f) f) f f = Relation.Map r f f
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.appLE_congr : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U U' : Y.Opens} {V V' : X.Opens}
  (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (e₁ : U = U') (e₂ : V = V')
  (P : {R S : CommRingCat} → (R ⟶ S) → Prop),
  P (AlgebraicGeometry.Scheme.Hom.appLE f U V e) ↔ P (AlgebraicGeometry.Scheme.Hom.appLE f U' V' ⋯)
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C)
  [comon : CategoryTheory.ComonObj X] (X_1 : C) (comon_1 : CategoryTheory.ComonObj X_1),
  ({ X := X, comon := comon } = { X := X_1, comon := comon_1 }) = (X = X_1 ∧ comon ≍ comon_1)
-- Mathlib.Computability.NFA
NFA.evalFrom_singleton : ∀ {α : Type u} {σ : Type v} (M : NFA α σ) (S : Set σ) (a : α), M.evalFrom S [a] = M.stepSet S a
-- Mathlib.GroupTheory.Congruence.Defs
/-- A version of `AddCon.induction_on` for predicates which takes two arguments.  -/
AddCon.induction_on₂ : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {c : AddCon M} {d : AddCon N}
  {C : c.Quotient → d.Quotient → Prop} (p : c.Quotient) (q : d.Quotient), (∀ (x : M) (y : N), C ↑x ↑y) → C p q
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.size_insertMany_list_le : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {l : List (α × β)}, (↑(Std.DTreeMap.Internal.Impl.Const.insertMany t l ⋯)).size ≤ t.size + l.length
-- Mathlib.Algebra.Order.Ring.Synonym
Lex.instSemiring : {R : Type u_1} → [Semiring R] → Semiring (Lex R)
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.toList_ne_nil : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {i j : ι} (w : Monoid.CoprodI.NeWord M i j),
  w.toList ≠ []
-- Aesop.Saturate
Aesop.getSingleGoal : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadError m] →
      Aesop.RuleTacOutput → m (Aesop.GoalDiff × Lean.Meta.SavedState × Option (Array Aesop.Script.LazyStep))
-- Mathlib.Analysis.Meromorphic.Basic
MeromorphicAt.sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : 𝕜} {f g : 𝕜 → E}, MeromorphicAt f x → MeromorphicAt g x → MeromorphicAt (f - g) x
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprodComparison_inl_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{w, u₂} D]
  (F : CategoryTheory.Functor C D) {A B : C} [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct A B]
  [inst_3 : CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)] {Z : D} (h : F.obj (A ⨿ B) ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprodComparison F A B) h) =
    CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.coprod.inl) h
-- Mathlib.CategoryTheory.Filtered.Small
/-- Every functor from a small category to a filtered category factors fully faithfully through a
small filtered category. This is that category.  -/
CategoryTheory.IsFiltered.SmallFilteredIntermediate : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.IsFilteredOrEmpty C] →
      {D : Type u₁} → [inst_2 : CategoryTheory.Category.{v₁, u₁} D] → CategoryTheory.Functor D C → Type (max u₁ v)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.mem_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k k' : α} {f : β → β}, k' ∈ t.modify k f ↔ k' ∈ t
-- Mathlib.NumberTheory.Height.Basic
Height.logHeight_eq_log_mulHeight : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2} (x : ι → K),
  Height.logHeight x = Real.log (Height.mulHeight x)
-- Mathlib.Analysis.Normed.Group.Uniform
Real.isOpen_compl_range_intCast : IsOpen (Set.range Int.cast)ᶜ
-- Mathlib.CategoryTheory.GlueData
/-- A functor that preserves the pullbacks of `f i j` and `f i k` can map a family of glue data.  -/
CategoryTheory.GlueData.mapGlueData : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v, u₁} C] →
    {C' : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v, u₂} C'] →
        (D : CategoryTheory.GlueData C) →
          (F : CategoryTheory.Functor C C') →
            [∀ (i j k : D.J),
                  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F] →
              CategoryTheory.GlueData C'
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.instAddCommGroup : {α : Type u_5} → [inst : NonUnitalNonAssocRing α] → AddCommGroup (CentroidHom α)
-- Mathlib.RingTheory.Valuation.ValuationRing
PreValuationRing.iff_dvd_total : ∀ {R : Type u_1} [inst : Semigroup R], PreValuationRing R ↔ Std.Total fun x1 x2 => x1 ∣ x2
-- Mathlib.Util.Export
_private.Mathlib.Util.Export.0.Lean.Export.MethodsRef : Type
-- Mathlib.Analysis.Analytic.CPolynomialDef
HasFiniteFPowerSeriesOnBall.bound_zero_of_eq_zero : ∀ {𝕜 : 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}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal},
  (∀ y ∈ Metric.eball x r, f y = 0) → 0 < r → (∀ (n : ℕ), p n = 0) → HasFiniteFPowerSeriesOnBall f p x 0 r
-- Mathlib.AlgebraicGeometry.AlgClosed.Basic
/-- If `X` is a locally of finite type `k`-scheme and `k` is algebraically closed, then
the residue field of any closed point of `x` is isomorphic to `k`.  -/
AlgebraicGeometry.residueFieldIsoBase : {X : AlgebraicGeometry.Scheme} →
  {K : Type u} →
    [inst : Field K] →
      [IsAlgClosed K] →
        (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) →
          [AlgebraicGeometry.LocallyOfFiniteType f] → (x : ↥X) → IsClosed {x} → (X.residueField x ≅ CommRingCat.of K)
-- Mathlib.RingTheory.AdicCompletion.RingHom
IsAdicComplete.liftRingHom.congr_simp : ∀ {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst_1 : CommRing S] (I : Ideal S)
  [inst_2 : IsAdicComplete I S] (f f_1 : (n : ℕ) → R →+* S ⧸ I ^ n) (e_f : f = f_1)
  (hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f n) = f m),
  IsAdicComplete.liftRingHom I f hf = IsAdicComplete.liftRingHom I f_1 ⋯
-- Mathlib.Topology.Category.TopCat.Basic
/-- Any isomorphism in `Top` induces a homeomorphism.  -/
TopCat.homeoOfIso : {X Y : TopCat} → (X ≅ Y) → ↑X ≃ₜ ↑Y
-- Mathlib.RingTheory.Congruence.Hom
RingCon.congr.congr_simp : ∀ {M : Type u_1} {N : Type u_2} [inst : NonAssocSemiring M] [inst_1 : NonAssocSemiring N] {c : RingCon M}
  {d : RingCon N} (e e_1 : M ≃+* N) (e_e : e = e_1) (h : c = d.comap e), RingCon.congr e h = RingCon.congr e_1 ⋯
-- Mathlib.RingTheory.TwoSidedIdeal.Lattice
TwoSidedIdeal.instInfSet : (R : Type u_1) → [inst : NonUnitalNonAssocRing R] → InfSet (TwoSidedIdeal R)
-- Mathlib.Geometry.Manifold.Bordism
/-- If `M` is a closed `C^k` manifold, it is a singular manifold over itself.  -/
SingularManifold.refl : {k : WithTop ℕ∞} →
  {E : Type u_4} →
    {H : Type u_5} →
      (M : Type u_6) →
        [inst : NormedAddCommGroup E] →
          [inst_1 : NormedSpace ℝ E] →
            [inst_2 : FiniteDimensional ℝ E] →
              [inst_3 : TopologicalSpace H] →
                (I : ModelWithCorners ℝ E H) →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] →
                      [IsManifold I k M] → [CompactSpace M] → [BoundarylessManifold I M] → SingularManifold M k I
-- Mathlib.Analysis.CStarAlgebra.Classes
CommCStarAlgebra.mk : {A : Type u_1} →
  [toNormedCommRing : NormedCommRing A] →
    [toStarRing : StarRing A] →
      [toCompleteSpace : CompleteSpace A] →
        [toCStarRing : CStarRing A] →
          [toNormedAlgebra : NormedAlgebra ℂ A] → [toStarModule : StarModule ℂ A] → CommCStarAlgebra A
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingEqCnstr.mk.inj : ∀ {p : Lean.Grind.CommRing.Poly} {h : Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof} {p_1 : Lean.Grind.CommRing.Poly}
  {h_1 : Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof}, { p := p, h := h } = { p := p_1, h := h_1 } → p = p_1 ∧ h = h_1
-- Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
HomotopicalAlgebra.Precylinder.LeftHomotopy.trans_h : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {P : HomotopicalAlgebra.Precylinder X} {Y : C}
  {f₀ f₁ f₂ : X ⟶ Y} (h : P.LeftHomotopy f₀ f₁) {P' : HomotopicalAlgebra.Precylinder X} (h' : P'.LeftHomotopy f₁ f₂)
  [inst_1 : CategoryTheory.Limits.HasPushout P.i₁ P'.i₀], (h.trans h').h = CategoryTheory.Limits.pushout.desc h.h h'.h ⋯
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
/-- basic open sets in `Proj`  -/
_private.Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme.0.AlgebraicGeometry.termPbo_ : Lean.ParserDescr
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.getKeyD.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a fallback : α) (x : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.getKeyD a fallback x =
    match x with
    | Std.DHashMap.Internal.AssocList.nil => fallback
    | Std.DHashMap.Internal.AssocList.cons k value es =>
      if (k == a) = true then k else Std.DHashMap.Internal.AssocList.getKeyD a fallback es
-- Mathlib.RingTheory.GradedAlgebra.Basic
DirectSum.coe_decompose_mul_of_right_mem_of_not_le : ∀ {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddCommMonoid ι]
  [inst_3 : PartialOrder ι] [CanonicallyOrderedAdd ι] [inst_5 : SetLike σ A] [inst_6 : AddSubmonoidClass σ A]
  (𝒜 : ι → σ) [inst_7 : GradedRing 𝒜] {a b : A} {n i : ι}, b ∈ 𝒜 i → ¬i ≤ n → ↑(((DirectSum.decompose 𝒜) (a * b)) n) = 0
-- Init.Data.SInt.Lemmas
ISize.add_sub_cancel : ∀ (a b : ISize), a + b - b = a
-- Init.Data.BitVec.Bitblast
/-- The result of `udiv` agrees with the result of the division recurrence.  -/
BitVec.udiv_eq_divRec : ∀ {w : ℕ} {d n : BitVec w},
  0#w < d →
    have out := BitVec.divRec w { n := n, d := d } (BitVec.DivModState.init w);
    n / d = out.q
-- Init.Data.Array.Lemmas
Array.any_map : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α} {p : β → Bool}, (Array.map f xs).any p = xs.any (p ∘ f)
-- Mathlib.Analysis.Calculus.Deriv.ZPow
iter_deriv_inv_linear_sub : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (k : ℕ) (c d : 𝕜),
  (deriv^[k] fun x => (c * x - d)⁻¹) = fun x => (-1) ^ k * ↑k.factorial * c ^ k * (c * x - d) ^ (-1 - ↑k)
-- Mathlib.CategoryTheory.Comma.Over.Pullback
CategoryTheory.Under.costar_obj_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C]
  (X_1 : C), ((CategoryTheory.Under.costar X).obj X_1).left = { as := PUnit.unit }
-- Lean.Meta.Constructions.NoConfusion
_private.Lean.Meta.Constructions.NoConfusion.0.Lean.mkIfNatEq : Lean.Expr →
  Lean.Expr → Lean.Expr → (Lean.Expr → Lean.MetaM Lean.Expr) → (Lean.Expr → Lean.MetaM Lean.Expr) → Lean.MetaM Lean.Expr
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
Std.IterM.step_flatMap : ∀ {α β α₂ γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : LawfulMonad m] [inst_2 : Std.Iterator α m β]
  [inst_3 : Std.Iterator α₂ m γ] {f : β → Std.IterM m γ} {it₁ : Std.IterM m β},
  (Std.IterM.flatMap f it₁).step = do
    let __do_lift ← it₁.step
    match __do_lift.inflate with
      | ⟨Std.IterStep.yield it₁' b, h⟩ =>
        pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.flatMapAfter f it₁' (some (f b))) ⋯))
      | ⟨Std.IterStep.skip it₁', h⟩ =>
        pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.flatMapAfter f it₁' none) ⋯))
      | ⟨Std.IterStep.done, h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.done ⋯))
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.ofLE_mk_le_mk_of_comm : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A₁ A₂ : C} {f₁ : A₁ ⟶ B} {f₂ : A₂ ⟶ B}
  [inst_1 : CategoryTheory.Mono f₁] [inst_2 : CategoryTheory.Mono f₂] (g : A₁ ⟶ A₂)
  (w : CategoryTheory.CategoryStruct.comp g f₂ = f₁),
  (CategoryTheory.Subobject.mk f₁).ofLE (CategoryTheory.Subobject.mk f₂) ⋯ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.underlyingIso f₁).hom
      (CategoryTheory.CategoryStruct.comp g (CategoryTheory.Subobject.underlyingIso f₂).inv)
-- Mathlib.Data.Fin.Tuple.Basic
Fin.insertNth_update : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u_1} (p : Fin (n + 1)) (x : α p) (i : Fin n) (y : α (p.succAbove i))
  (f : (j : Fin n) → α (p.succAbove j)),
  p.insertNth x (Function.update f i y) = Function.update (p.insertNth x f) (p.succAbove i) y
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.HoverParams : Type
-- Mathlib.Algebra.Lie.Quotient
/-- Given a Lie module `M` over a Lie algebra `L`, together with a Lie submodule `N ⊆ M`, there
is a natural Lie algebra morphism from `L` to the linear endomorphism of the quotient `M/N`.  -/
LieSubmodule.Quotient.actionAsEndoMap : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : AddCommGroup M] →
            [inst_3 : Module R M] →
              [inst_4 : LieRingModule L M] →
                (N : LieSubmodule R L M) → [inst_5 : LieAlgebra R L] → [LieModule R L M] → L →ₗ⁅R⁆ Module.End R (M ⧸ N)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instHashableCongrTheoremCacheKey : Hashable Lean.Meta.Grind.CongrTheoremCacheKey
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKeyD_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {v : β k} {fallback : α},
      (t.insert k v).minKeyD fallback = t.minKey?.elim k fun k' => if (cmp k k').isLE = true then k else k'
-- Lean.Elab.Tactic.Basic
/-- If `true`, enable "error recovery" in some tactics. For example, `cases` tactic
admits unsolved alternatives when `recover == true`. The combinator `withoutRecover <tac>` disables
"error recovery" while executing `<tac>`. This is useful for tactics such as `first | ... | ...`.
 -/
Lean.Elab.Tactic.Context.recover : Lean.Elab.Tactic.Context → Bool
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.nextCoeffUp_zero : ∀ {R : Type u} [inst : Semiring R], Polynomial.nextCoeffUp 0 = 0
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.instReprCustomEliminator.repr : Lean.Meta.CustomEliminator → ℕ → Std.Format
-- Mathlib.Probability.Martingale.OptionalSampling
/-- The value of a martingale `f` at a stopping time `τ` bounded by `n` is the conditional
expectation of `f n` with respect to the σ-algebra generated by `τ`.  -/
MeasureTheory.Martingale.stoppedValue_ae_eq_condExp_of_le_const : ∀ {Ω : Type u_1} {E : Type u_2} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : TopologicalSpace ι]
  [OrderTopology ι] {ℱ : MeasureTheory.Filtration ι m} [MeasureTheory.SigmaFiniteFiltration μ ℱ] {τ : Ω → WithTop ι}
  {f : ι → Ω → E} {n : ι} [inst_7 : Nonempty ι] [Countable ι],
  MeasureTheory.Martingale f ℱ μ →
    ∀ (hτ : MeasureTheory.IsStoppingTime ℱ τ) (hτ_le : ∀ (x : Ω), τ x ≤ ↑n) [MeasureTheory.SigmaFinite (μ.trim ⋯)],
      MeasureTheory.stoppedValue f τ =ᵐ[μ] μ[f n | hτ.measurableSpace]
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.OuterMeasure.sInfGen.eq_1 : ∀ {α : Type u_1} (m : Set (MeasureTheory.OuterMeasure α)) (s : Set α),
  MeasureTheory.OuterMeasure.sInfGen m s = ⨅ μ ∈ m, μ s
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
/-- See also `Complex.cpow_int_mul'`.  -/
Complex.cpow_int_mul : ∀ (x : ℂ) (n : ℤ) (y : ℂ), x ^ (↑n * y) = (x ^ y) ^ n
-- Mathlib.Topology.Category.TopCat.Limits.Products
TopCat.sigmaIsoSigma.eq_1 : ∀ {ι : Type v} (α : ι → TopCat),
  TopCat.sigmaIsoSigma α =
    (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Discrete.functor α)).coconePointUniqueUpToIso
      (TopCat.sigmaCofanIsColimit α)
-- Mathlib.Algebra.SkewMonoidAlgebra.Support
SkewMonoidAlgebra.support_one : ∀ {k : Type u_1} {G : Type u_2} [inst : One G] [inst_1 : AddCommMonoidWithOne k] [NeZero 1],
  SkewMonoidAlgebra.support 1 = 1
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- If `s` and `s'` are local frames which are equal at `x`,
a section `t` has equal frame coefficients in them.  -/
IsLocalFrameOn.coeff_eq_of_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] {ι : Type u_7} {s s' : ι → (x : M) → V x}
  {u : Set M} {n : WithTop ℕ∞} {x : M} (hs : IsLocalFrameOn I F n s u) (hs' : IsLocalFrameOn I F n s' u),
  (∀ (i : ι), s i x = s' i x) → ∀ {t : (x : M) → V x} (i : ι), (hs.coeff i x) (t x) = (hs'.coeff i x) (t x)
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.isPrefixOf.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (x : List α) (h_1 : (x : List α) → motive [] x)
  (h_2 : (x : List α) → motive x [])
  (h_3 : (a : α) → (as : List α) → (b : α) → (bs : List α) → motive (a :: as) (b :: bs)),
  (x = [] → False) →
    (match x, [] with
      | [], x => h_1 x
      | x, [] => h_2 x
      | a :: as, b :: bs => h_3 a as b bs) =
      h_2 x
-- Mathlib.LinearAlgebra.Span.Basic
/-- Given a nonzero element `x` of a torsion-free module `M` over a ring `R`, the natural
isomorphism from `R` to the span of `x` given by $r \mapsto r \cdot x$.  -/
LinearEquiv.toSpanNonzeroSingleton : (R : Type u_1) →
  (M : Type u_4) →
    [inst : Ring R] →
      [IsDomain R] →
        [inst_2 : AddCommGroup M] →
          [inst_3 : Module R M] → [Module.IsTorsionFree R M] → (x : M) → x ≠ 0 → R ≃ₗ[R] ↥(R ∙ x)
-- Mathlib.Algebra.Group.Pi.Lemmas
MonoidHom.coeFn_apply : ∀ (α : Type u_5) (β : Type u_6) [inst : MulOneClass α] [inst_1 : CommMonoid β] (g : α →* β) (a : α),
  (MonoidHom.coeFn α β) g a = g a
-- Mathlib.Order.Interval.Set.ProjIcc
Set.range_projIcc : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α} (h : a ≤ b), Set.range (Set.projIcc a b h) = Set.univ
-- Mathlib.Analysis.Analytic.ChangeOrigin
AnalyticAt.exists_mem_nhds_analyticOnNhd : ∀ {𝕜 : 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] [CompleteSpace F] {f : E → F}
  {x : E}, AnalyticAt 𝕜 f x → ∃ s ∈ nhds x, AnalyticOnNhd 𝕜 f s
-- Init.Data.Int.Gcd
Int.one_gcd : ∀ {a : ℤ}, Int.gcd 1 a = 1
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.one.eq_1 : ∀ {α : Type u} [inst : One α], WithTop.one = { one := ↑1 }
-- Mathlib.RingTheory.RingHom.OpenImmersion
RingHom.IsStandardOpenImmersion.isStableUnderBaseChange : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => RingHom.IsStandardOpenImmersion
-- Mathlib.LinearAlgebra.Matrix.Trace
Matrix.trace_transpose_mul : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_6} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : AddCommMonoid R]
  [inst_3 : Mul R] (A : Matrix m n R) (B : Matrix n m R), (A.transpose * B.transpose).trace = (A * B).trace
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.evalₐ.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (n : ℕ),
  AdicCompletion.evalₐ I n =
    (↑(Ideal.quotientEquivAlgOfEq R ⋯)).comp (AlgHom.ofLinearMap (AdicCompletion.eval I R n) ⋯ ⋯)
-- Mathlib.Topology.Bornology.BoundedOperation
isBounded_pow : ∀ {R : Type u_2} [inst : Bornology R] [inst_1 : Monoid R] [BoundedMul R] {s : Set R},
  Bornology.IsBounded s → ∀ (n : ℕ), Bornology.IsBounded ((fun x => x ^ n) '' s)
-- Mathlib.Analysis.Fourier.FourierTransform
Real.Lp.fourierTransformInvCLM.eq_1 : ∀ (V : Type u_1) (E : Type u_3) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : MeasurableSpace V] [inst_5 : BorelSpace V]
  [inst_6 : FiniteDimensional ℝ V],
  Real.Lp.fourierTransformInvCLM V E =
    BoundedContinuousFunction.compContinuousCLM E ℂ (-ContinuousMap.id V) ∘SL Real.Lp.fourierTransformCLM V E