mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.denote_blast : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (lhs rhs : BitVec w)
  (assign : α → Bool) (input : aig.BinaryRefVec w),
  (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx) →
    (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx) →
      ∀ (idx : ℕ) (hidx : idx < w),
        ⟦assign,
            { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.blast aig input).aig,
              ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.blast aig input).vec.get idx hidx }⟧ =
          (lhs + rhs).getLsbD idx
-- Mathlib.Topology.Algebra.Ring.Basic
/-- A semitopological ring is a ring `R` where addition is jointly continuous and
multiplication is continuous in each variable separately, and negation is continuous as well.
We allow for non-unital and non-associative rings as well.

If `R` is a (unital) ring, then continuity of negation can be derived from continuity of
multiplication as it is multiplication with `-1`. (See `IsTopologicalSemiring.continuousNeg_of_mul`
and `IsSemitopologicalSemiring.toIsSemitopologicalRing`)  -/
IsSemitopologicalRing : (R : Type u_2) → [TopologicalSpace R] → [NonUnitalNonAssocRing R] → Prop
-- Mathlib.Topology.Homotopy.Lifting
IsAddQuotientCoveringMap.ker_monodromyPerm : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X} {G : Type u_4}
  [inst_2 : AddGroup G] [inst_3 : AddAction G E] (hp : IsAddQuotientCoveringMap p G) {x : X} (e : ↑(p ⁻¹' {x})),
  (⋯.monodromyPerm x).ker = (FundamentalGroup.mapOfEq { toFun := p, continuous_toFun := ⋯ } ⋯).range
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.Partial.extend.eq_1 : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] {seed : HahnEmbedding.Seed K M R} (f : HahnEmbedding.Partial seed)
  [inst_12 : IsOrderedAddMonoid R] [inst_13 : Archimedean R] {x : M} (hx : x ∉ (↑f).domain),
  f.extend hx = ⟨f.extendFun hx, ⋯⟩
-- Mathlib.Topology.JacobsonSpace
isClosed_singleton_of_isLocallyClosed_singleton : ∀ {X : Type u_1} [inst : TopologicalSpace X] [JacobsonSpace X] {x : X}, IsLocallyClosed {x} → IsClosed {x}
-- Mathlib.Order.Filter.Defs
/-- Specialize `lift` to functions `Set α → Set β`. This can be viewed as a generalization of `map`.
This is essentially a push-forward along a function mapping each set to a set.  -/
Filter.lift' : {α : Type u_1} → {β : Type u_2} → Filter α → (Set α → Set β) → Filter β
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.commAlgEquiv_single_single : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Monoid M] [inst_4 : Monoid N] (m : M) (n : N) (a : A),
  (MonoidAlgebra.commAlgEquiv R) (MonoidAlgebra.single m (MonoidAlgebra.single n a)) =
    MonoidAlgebra.single n (MonoidAlgebra.single m a)
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
CategoryTheory.Limits.IsColimit.pushoutCoconeEquivBinaryCofanFunctor_desc_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
  {c : CategoryTheory.Limits.PushoutCocone f g} (hc : CategoryTheory.Limits.IsColimit c)
  (s : CategoryTheory.Limits.BinaryCofan (CategoryTheory.Under.mk f) (CategoryTheory.Under.mk g)),
  (hc.pushoutCoconeEquivBinaryCofanFunctor.desc s).right =
    hc.desc
      (CategoryTheory.Limits.PushoutCocone.mk (CategoryTheory.Under.Hom.right s.inl)
        (CategoryTheory.Under.Hom.right s.inr) ⋯)
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.coeff_subst : ∀ {R : Type u_2} [inst : CommRing R] {τ : Type u_3} {S : Type u_4} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {a : MvPowerSeries τ S},
  PowerSeries.HasSubst a →
    ∀ (f : PowerSeries R) (e : τ →₀ ℕ),
      (MvPowerSeries.coeff e) (PowerSeries.subst a f) =
        ∑ᶠ (d : ℕ), (PowerSeries.coeff d) f • (MvPowerSeries.coeff e) (a ^ d)
-- Mathlib.RingTheory.RingHom.FaithfullyFlat
RingHom.FaithfullyFlat.of_bijective : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S},
  Function.Bijective ⇑f → f.FaithfullyFlat
-- Init.Data.Float.Model.Unpacked.Basic
Float.Model.UnpackedFloat.infinity.inj : ∀ {sign sign_1 : Float.Model.UnpackedFloat.Sign},
  Float.Model.UnpackedFloat.infinity sign = Float.Model.UnpackedFloat.infinity sign_1 → sign = sign_1
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
SSet.S.IsUniquelyCodimOneFace.op : ∀ {X : SSet} {x y : X.S},
  x.IsUniquelyCodimOneFace y → (SSet.S.opEquiv.symm x).IsUniquelyCodimOneFace (SSet.S.opEquiv.symm y)
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.of.congr_simp : ∀ {α : Type u} (f f_1 : Filter α) (e_f : f = f_1) [inst : f.NeBot], Ultrafilter.of f = Ultrafilter.of f_1
-- Mathlib.CategoryTheory.Monoidal.Closed.Ideal
/-- Given a reflective subcategory `D` of a category with chosen finite products `C`, `D` admits
finite chosen products.  -/
CategoryTheory.CartesianMonoidalCategory.ofReflective : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] →
        (i : CategoryTheory.Functor D C) →
          [CategoryTheory.CartesianMonoidalCategory C] →
            [CategoryTheory.Reflective i] → CategoryTheory.CartesianMonoidalCategory D
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Context.simpMethods : Lean.Meta.Grind.Context → Lean.Meta.Simp.Methods
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
/-- The submodule generated by a finite supremum of finite-dimensional submodules is
finite-dimensional.

Note that strictly this only needs `∀ i ∈ s, FiniteDimensional K (S i)`, but that doesn't
work well with typeclass search.  -/
Submodule.finiteDimensional_finset_sup : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {ι : Type u_1}
  (s : Finset ι) (S : ι → Submodule K V) [∀ (i : ι), FiniteDimensional K ↥(S i)], FiniteDimensional K ↥(s.sup S)
-- Mathlib.RingTheory.WittVector.WittPolynomial
xInTermsOfW_aux : ∀ (p : ℕ) (R : Type u_1) [inst : CommRing R] [inst_1 : Invertible ↑p] (n : ℕ),
  xInTermsOfW p R n * MvPolynomial.C (↑p ^ n) =
    MvPolynomial.X n - ∑ i ∈ Finset.range n, MvPolynomial.C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i)
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.triangle_bimod : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C]
  [inst_3 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorLeft X)]
  [inst_4 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorRight X)]
  {X Y Z : CategoryTheory.Mon C} (M : Bimod X Y) (N : Bimod Y Z),
  CategoryTheory.CategoryStruct.comp (M.associatorBimod (Bimod.regular Y) N).hom (M.whiskerLeft N.leftUnitorBimod.hom) =
    Bimod.whiskerRight M.rightUnitorBimod.hom N
-- Init.Data.Order.Ord
/-- The corresponding lemma for `LawfulEqCmp` is `LawfulEqCmp.compare_beq_iff_eq`  -/
Std.LawfulEqOrd.compare_beq_iff_eq : ∀ {α : Type u} [inst : Ord α] [Std.LawfulEqOrd α] {a b : α}, (compare a b == Ordering.eq) = true ↔ a = b
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
/-- If `M / R` and `M' / R'` are modules, `i : R' → R` is a map, `j : M →+ M'` is a monoid map,
such that they send non-zero elements to non-zero elements, and compatible with the scalar
multiplications on `M` and `M'`, then `j` sends linearly independent families of vectors to
linearly independent families of vectors. As a special case, taking `R = R'`
it is `LinearIndependent.map'`.  -/
LinearIndependent.map_of_injective_injective : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] {R' : Type u_6} {M' : Type u_7} [inst_3 : Ring R'] [inst_4 : AddCommGroup M']
  [inst_5 : Module R' M'],
  LinearIndependent R v →
    ∀ (i : R' → R) (j : M →+ M'),
      (∀ (r : R'), i r = 0 → r = 0) →
        (∀ (m : M), j m = 0 → m = 0) → (∀ (r : R') (m : M), j (i r • m) = r • j m) → LinearIndependent R' (⇑j ∘ v)
-- Init.Util
mkPanicMessage : String → ℕ → ℕ → String → String
-- Std.Do.SPred.SVal
Std.Do.SVal.uncurry_curry : ∀ {α : Type u} {σs : List (Type u)} {f : Std.Do.SVal.StateTuple σs → α}, (Std.Do.SVal.curry f).uncurry = f
-- Mathlib.Analysis.Analytic.Constructions
/-- The geometric series as an `ofScalars` series.  -/
formalMultilinearSeries_geometric_eq_ofScalars : ∀ (𝕜 : Type u_2) [inst : NontriviallyNormedField 𝕜] (A : Type u_7) [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A],
  formalMultilinearSeries_geometric 𝕜 A = FormalMultilinearSeries.ofScalars A fun x => 1
-- Mathlib.Algebra.Star.StarRingHom
NonUnitalStarRingHom.coe_zero : ∀ {A : Type u_1} {B : Type u_2} [inst : NonUnitalNonAssocSemiring A] [inst_1 : StarAddMonoid A]
  [inst_2 : NonUnitalNonAssocSemiring B] [inst_3 : StarAddMonoid B], ⇑0 = 0
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
/-- A universe-heterogeneous version of `Bind.bind`.
 -/
Std.Iterators.HetT.bind : {m : Type w → Type w'} →
  [Monad m] →
    {α : Type u} → {β : Type v} → Std.Iterators.HetT m α → (α → Std.Iterators.HetT m β) → Std.Iterators.HetT m β
-- Mathlib.Analysis.LocallyConvex.Polar
StrongDual.polar_nonempty : ∀ (𝕜 : Type u_4) [inst : NontriviallyNormedField 𝕜] {E : Type u_5} [inst_1 : AddCommMonoid E]
  [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] (s : Set E), (StrongDual.polar 𝕜 s).Nonempty
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
Real.iSup_of_not_bddAbove : ∀ {ι : Sort u_1} {f : ι → ℝ}, ¬BddAbove (Set.range f) → ⨆ i, f i = 0
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- A localization map between additive monoids automatically preserves 0 and
therefore is an additive monoid homomorphism.  -/
AddSubmonoid.LocalizationMap.toAddMonoidHom : {M : Type u_1} →
  [inst : AddCommMonoid M] →
    {S : AddSubmonoid M} → {N : Type u_2} → [inst_1 : AddCommMonoid N] → S.LocalizationMap N → M →+ N
-- Mathlib.Order.Interval.Set.Disjoint
Set.iUnion_Iic : ∀ {α : Type v} [inst : Preorder α], ⋃ a, Set.Iic a = Set.univ
-- Mathlib.Data.Set.Monotone
StrictMono.codRestrict : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  StrictMono f → ∀ {s : Set β} (hs : ∀ (x : α), f x ∈ s), StrictMono (Set.codRestrict f s hs)
-- Init.Data.Array.Lemmas
Array.getElem?_set_self : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} (h : i < xs.size) {v : α}, (xs.set i v h)[i]? = some v
-- Mathlib.Algebra.Exact.Basic
/-- The linear equivalence `(N ⧸ LinearMap.range f) ≃ₗ[A] P` associated to
an exact sequence `M → N → P → 0` of `R`-modules.  -/
Function.Exact.linearEquivOfSurjective : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_4} →
      {P : Type u_6} →
        [inst : Ring R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : AddCommGroup N] →
              [inst_3 : AddCommGroup 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 → Function.Surjective ⇑g → (N ⧸ f.range) ≃ₗ[R] P
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
ZMod.toCircle_intCast : ∀ {N : ℕ} [inst : NeZero N] (j : ℤ), ↑(ZMod.toCircle ↑j) = Complex.exp (2 * ↑Real.pi * Complex.I * ↑j / ↑N)
-- Lean.Meta.Sym.LitValues
Lean.Meta.Sym.BitVecValue.mk : (n : ℕ) → BitVec n → Lean.Meta.Sym.BitVecValue
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- If `M` and `N` are linearly disjoint, if `M` is flat, then any two commutative
elements of `↥(M ⊓ N)` are not `R`-linearly independent (namely, their span is not `R ^ 2`).  -/
Submodule.LinearDisjoint.not_linearIndependent_pair_of_commute_of_flat_left : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {M N : Submodule R S},
  M.LinearDisjoint N →
    ∀ [Nontrivial R] [Module.Flat R ↥M] (a b : ↥(M ⊓ N)), Commute ↑a ↑b → ¬LinearIndependent R ![a, b]
-- Mathlib.Algebra.ContinuedFractions.Computation.Basic
/-- Coerce a pair by coercing the fractional component.  -/
GenContFract.IntFractPair.coe : {K : Type u_1} → {β : Type u_2} → [Coe K β] → Coe (GenContFract.IntFractPair K) (GenContFract.IntFractPair β)
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.instSubsingleton : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Subsingleton M]
  (S : Submonoid R), Subsingleton (LocalizedModule S M)
-- Mathlib.Data.Finsupp.Pointwise
/-- Pointwise scalar multiplication given by `(f • g) x = f x • g x`.  -/
Finsupp.pointwiseScalar : {α : Type u₁} → {β : Type u₂} → {γ : Type u₃} → [inst : Zero γ] → [SMulZeroClass β γ] → SMul (α → β) (α →₀ γ)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey_minKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {hc : t.minKey! ∈ t}, t.getKey t.minKey! hc = t.minKey!
-- Mathlib.Data.ENNReal.Operations
ENNReal.pow_pos : ∀ {a : ENNReal}, 0 < a → ∀ (n : ℕ), 0 < a ^ n
-- Mathlib.Algebra.GroupWithZero.Pointwise.Finset
Finset.mul_zero_subset : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] (s : Finset α), s * 0 ⊆ 0
-- Mathlib.Data.Sum.Interval
Sum.Lex.Iio_inr : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Fintype α]
  [inst_3 : LocallyFiniteOrderBot α] [inst_4 : LocallyFiniteOrderBot β] (b : β),
  Finset.Iio (Sum.inrₗ b) = Finset.map toLex.toEmbedding (Finset.univ.disjSum (Finset.Iio b))
-- Mathlib.CategoryTheory.SmallRepresentatives
CategoryTheory.SmallCategoryOfSet.id_comp : ∀ {Ω : Type w} (self : CategoryTheory.SmallCategoryOfSet Ω) {X Y : ↑self.obj} (f : ↑(self.hom X Y)),
  self.comp (self.id X) f = f
-- Init.Grind.Module.Envelope
_private.Init.Grind.Module.Envelope.0.Lean.Grind.IntModule.OfNatModule.nsmul.eq_1 : ∀ {α : Type u} [inst : Lean.Grind.NatModule α] (n : ℕ) (q : Lean.Grind.IntModule.OfNatModule.Q α),
  Lean.Grind.IntModule.OfNatModule.nsmul n q =
    Quot.liftOn q
      (fun x =>
        match x with
        | (a, b) => Lean.Grind.IntModule.OfNatModule.Q.mk (n • a, n • b))
      ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_snd_fst : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst f g)
          (CategoryTheory.Limits.pullback.fst f g))
        (CategoryTheory.Limits.pullback.fst f g)) =
    CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd g g) g) f
-- Mathlib.CategoryTheory.Join.Basic
_private.Mathlib.CategoryTheory.Join.Basic.0.CategoryTheory.Join.comp.match_1.splitter : {C : Type u_3} →
  [inst : CategoryTheory.Category.{u_1, u_3} C] →
    {D : Type u_4} →
      [inst_1 : CategoryTheory.Category.{u_2, u_4} D] →
        (motive : (x x_1 x_2 : CategoryTheory.Join C D) → x.Hom x_1 → x_1.Hom x_2 → Sort u_5) →
          (x x_1 x_2 : CategoryTheory.Join C D) →
            (x_3 : x.Hom x_1) →
              (x_4 : x_1.Hom x_2) →
                ((_x _y _z : C) →
                    (f : (CategoryTheory.Join.left _x).Hom (CategoryTheory.Join.left _y)) →
                      (g : (CategoryTheory.Join.left _y).Hom (CategoryTheory.Join.left _z)) →
                        motive (CategoryTheory.Join.left _x) (CategoryTheory.Join.left _y) (CategoryTheory.Join.left _z)
                          f g) →
                  ((_x _y : C) →
                      (_z : D) →
                        (x : (CategoryTheory.Join.left _x).Hom (CategoryTheory.Join.left _y)) →
                          (x_5 : (CategoryTheory.Join.left _y).Hom (CategoryTheory.Join.right _z)) →
                            motive (CategoryTheory.Join.left _x) (CategoryTheory.Join.left _y)
                              (CategoryTheory.Join.right _z) x x_5) →
                    ((_x : C) →
                        (_y _z : D) →
                          (x : (CategoryTheory.Join.left _x).Hom (CategoryTheory.Join.right _y)) →
                            (x_5 : (CategoryTheory.Join.right _y).Hom (CategoryTheory.Join.right _z)) →
                              motive (CategoryTheory.Join.left _x) (CategoryTheory.Join.right _y)
                                (CategoryTheory.Join.right _z) x x_5) →
                      ((_x _y _z : D) →
                          (f : (CategoryTheory.Join.right _x).Hom (CategoryTheory.Join.right _y)) →
                            (g : (CategoryTheory.Join.right _y).Hom (CategoryTheory.Join.right _z)) →
                              motive (CategoryTheory.Join.right _x) (CategoryTheory.Join.right _y)
                                (CategoryTheory.Join.right _z) f g) →
                        motive x x_1 x_2 x_3 x_4
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.WalkingMulticospan.instSmallCategory : {J : CategoryTheory.Limits.MulticospanShape} → CategoryTheory.SmallCategory (CategoryTheory.Limits.WalkingMulticospan J)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.self_le_maxKey?_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α} {v : β}
  {kmi : α}, (t.insert k v).maxKey?.get ⋯ = kmi → (cmp k kmi).isLE = true
-- Batteries.Control.LawfulMonadState
/-- Discarding the result of `get` is the same as never getting the state.  -/
LawfulMonadStateOf.get_bind_const : ∀ {σ : semiOutParam (Type u_1)} {m : Type u_1 → Type u_2} {inst : Monad m} {inst_1 : MonadStateOf σ m}
  [self : LawfulMonadStateOf σ m] {α : Type u_1} (mx : m α),
  (do
      let _ ← get
      mx) =
    mx
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.reorder : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr → Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cocycle.instCoeCochain : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {F G : CochainComplex C ℤ} →
        {n : ℤ} → Coe (CochainComplex.HomComplex.Cocycle F G n) (CochainComplex.HomComplex.Cochain F G n)
-- Init.Data.String.Defs
String.Slice.Pos.lt_iff : ∀ {s : String.Slice} {l r : s.Pos}, l < r ↔ l.offset < r.offset
-- Mathlib.MeasureTheory.Function.ConvergenceInMeasure
MeasureTheory.TendstoInMeasure.congr_right : ∀ {α : Type u_1} {ι : Type u_2} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : EDist E]
  {l : Filter ι} {f : ι → α → E} {g g' : α → E},
  g =ᵐ[μ] g' → MeasureTheory.TendstoInMeasure μ f l g → MeasureTheory.TendstoInMeasure μ f l g'
-- Mathlib.Algebra.Order.Group.Unbundled.Int
Int.le_self_sq : ∀ (b : ℤ), b ≤ b ^ 2
-- Mathlib.Data.Fin.Tuple.Take
Fin.take.eq_1 : ∀ {n : ℕ} {α : Fin n → Sort u_1} (m : ℕ) (h : m ≤ n) (v : (i : Fin n) → α i) (i : Fin m),
  Fin.take m h v i = v (Fin.castLE h i)
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.take.congr_simp : ∀ (p p_1 : DyckWord) (e_p : p = p_1) (i i_1 : ℕ) (e_i : i = i_1)
  (hi : List.count DyckStep.U (List.take i ↑p) = List.count DyckStep.D (List.take i ↑p)), p.take i hi = p_1.take i_1 ⋯
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.set_eq_setTR.go : ∀ (α : Type u_1) (l : List α) (a : α) (acc : Array α) (xs : List α) (i : ℕ),
  l = acc.toList ++ xs → List.setTR.go✝ l a xs i acc = acc.toList ++ xs.set i a
-- Mathlib.CategoryTheory.Galois.IsFundamentalgroup
CategoryTheory.PreGaloisCategory.toAutMulEquiv_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.GaloisCategory C] {G : Type u_1} [inst_2 : Group G]
  [inst_3 : (X : C) → MulAction G (F.obj X).obj] [inst_4 : CategoryTheory.PreGaloisCategory.FiberFunctor F]
  [inst_5 : TopologicalSpace G] [inst_6 : IsTopologicalGroup G] [inst_7 : CompactSpace G]
  [inst_8 : CategoryTheory.PreGaloisCategory.IsFundamentalGroup F G] (g : G),
  (CategoryTheory.PreGaloisCategory.toAutMulEquiv F G) g = (CategoryTheory.PreGaloisCategory.toAut F G) g
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.trStmts₁.eq_5 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (a : σ → Bool) (q₁ q₂ : Turing.TM2.Stmt Γ Λ σ),
  Turing.TM2to1.trStmts₁ (Turing.TM2.Stmt.branch a q₁ q₂) = Turing.TM2to1.trStmts₁ q₁ ∪ Turing.TM2to1.trStmts₁ q₂
-- Init.Data.Format.Basic
/-- The default width of the targeted output, which is 120 columns.  -/
Std.Format.defWidth : ℕ
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_swap_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : MeasurableSpace γ}
  {f : α × β → γ}, Measurable (f ∘ Prod.swap) ↔ Measurable f
-- Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
CategoryTheory.MorphismProperty.antitone_llp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], Antitone CategoryTheory.MorphismProperty.llp
-- Mathlib.LinearAlgebra.AffineSpace.MidpointZero
lineMap_inv_two : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing R] [inst_1 : CharZero R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] (a b : P), (AffineMap.lineMap a b) 2⁻¹ = midpoint R a b
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.ringEquivOfRingEquiv_apply_val : ∀ {R : Type u_5} {S : Type u_6} (K : Type u_7) (L : Type u_8) [inst : CommRing R] [inst_1 : IsDomain R]
  [inst_2 : CommRing S] [inst_3 : IsDomain S] [inst_4 : CommRing K] [inst_5 : CommRing L] [inst_6 : Algebra R K]
  [inst_7 : Algebra S L] [inst_8 : IsFractionRing R K] [inst_9 : IsFractionRing S L] (f : R ≃+* S)
  (I : FractionalIdeal (nonZeroDivisors R) K),
  ↑((FractionalIdeal.ringEquivOfRingEquiv K L f) I) =
    Submodule.map ↑(IsFractionRing.semilinearEquivOfRingEquiv K L f) ↑I
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_map_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] [inst_3 : CategoryTheory.BraidedCategory D]
  (A : CategoryTheory.CommMon (CategoryTheory.Functor C D)) {X Y : C} (f : X ⟶ Y),
  ((CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor.obj A).map f).hom.hom = A.X.map f
-- Mathlib.MeasureTheory.Integral.IntegrableOn
/-- If a function is continuous on a measurable set `s`, then it is measurable at the filter
`𝓝[s] x` for all `x`.  -/
ContinuousOn.stronglyMeasurableAtFilter_nhdsWithin : ∀ {α : Type u_7} {β : Type u_8} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [OpensMeasurableSpace α]
  [inst_3 : TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [SecondCountableTopologyEither α β]
  {f : α → β} {s : Set α} {μ : MeasureTheory.Measure α},
  ContinuousOn f s → MeasurableSet s → ∀ (x : α), StronglyMeasurableAtFilter f (nhdsWithin x s) μ