mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap_fac_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {X₁ X₂ : HomotopicalAlgebra.CofibrantObject C} (f : X₁ ⟶ X₂) {Z : HomotopicalAlgebra.CofibrantObject C}
  (h : HomotopicalAlgebra.CofibrantObject.mk X₂.bifibrantResolutionObj.obj ⟶ Z),
  CategoryTheory.CategoryStruct.comp X₁.iBifibrantResolutionObj
      (CategoryTheory.CategoryStruct.comp
        (HomotopicalAlgebra.CofibrantObject.homMk (HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap f).hom)
        h) =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp X₂.iBifibrantResolutionObj h)
-- Mathlib.LinearAlgebra.Pi
LinearMap.proj_comp_single_ne : ∀ (R : Type u) {ι : Type x} [inst : Semiring R] (φ : ι → Type i) [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)] [inst_3 : DecidableEq ι] (i j : ι),
  i ≠ j → LinearMap.proj i ∘ₗ LinearMap.single R φ j = 0
-- Mathlib.Order.Hom.Lattice
LatticeHomClass.toSupHomClass : ∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} {inst : Lattice α} {inst_1 : Lattice β} {inst_2 : FunLike F α β}
  [self : LatticeHomClass F α β], SupHomClass F α β
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
/-- The type of objects for the diagram indexing a pullback, defined as a special case of
`WidePullbackShape`.  -/
CategoryTheory.Limits.WalkingCospan : Type
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
/-- The left inclusion in the mapping cone, as a cochain of degree `-1`.  -/
CochainComplex.mappingCone.inl : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {F G : CochainComplex C ℤ} →
        (φ : F ⟶ G) →
          [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] →
            CochainComplex.HomComplex.Cochain F (CochainComplex.mappingCone φ) (-1)
-- Mathlib.AlgebraicTopology.CechNerve
/-- The Čech conerve construction, as a functor from `Arrow C`.  -/
CategoryTheory.CosimplicialObject.cechConerve : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [∀ (n : ℕ) (f : CategoryTheory.Arrow C),
          CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom] →
      CategoryTheory.Functor (CategoryTheory.Arrow C) (CategoryTheory.CosimplicialObject C)
-- Mathlib.Analysis.LocallyConvex.Basic
balanced_iUnion : ∀ {𝕜 : Type u_1} {E : Type u_3} {ι : Sort u_5} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] {f : ι → Set E},
  (∀ (i : ι), Balanced 𝕜 (f i)) → Balanced 𝕜 (⋃ i, f i)
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData_right_ι : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  [inst_3 : X.HasSpectralSequence data] (r r' : ℤ) (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq pq' pq'' : κ)
  (hpq : (c r).prev pq' = pq) (hpq' : (c r).next pq' = pq'') (i₀' i₀ i₁ i₂ i₃ i₃' : ι) (hi₀' : i₀' = data.i₀ r' pq' ⋯)
  (hi₀ : i₀ = data.i₀ r pq' ⋯) (hi₁ : i₁ = data.i₁ pq') (hi₂ : i₂ = data.i₂ pq') (hi₃ : i₃ = data.i₃ r pq' ⋯)
  (hi₃' : i₃' = data.i₃ r' pq' ⋯) (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq')
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData._auto_3),
  (X.spectralSequenceHomologyData data r r' hrr' hr pq pq' pq'' hpq hpq' i₀' i₀ i₁ i₂ i₃ i₃' hi₀' hi₀ hi₁ hi₂ hi₃ hi₃'
          n₀ n₁ n₂ hn₁' hn₁ hn₂).right.ι =
    X.mapFourδ₁Toδ₀' i₀' i₀ i₁ i₂ i₃' ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ ⋯ ⋯
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.gi.eq_1 : ∀ (M : Type u_1) [inst : Add M],
  AddCon.gi M = { choice := fun r x => addConGen r, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }
-- Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi
CategoryTheory.Idempotents.KaroubiKaroubi.idem_f : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C]
  (P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Idempotents.Karoubi C)),
  CategoryTheory.CategoryStruct.comp P.p.f P.p.f = P.p.f
-- Mathlib.Logic.Function.Basic
Function.IsPartialInv.surjective_getD : ∀ {α : Type u_4} {β : Sort u_5} {f : α → β} {g : β → Option α},
  Function.IsPartialInv f g → ∀ (x : α), Function.Surjective fun x_1 => (g x_1).getD x
-- Lean.Elab.MutualInductive
/-- Executes `k` using the `Syntax` reference associated with constructor `ctorName`.
 -/
Lean.Elab.Command.withCtorRef : {m : Type → Type} →
  {α : Type} → [Monad m] → [Lean.MonadRef m] → Array Lean.Elab.Command.InductiveView → Lean.Name → m α → m α
-- Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
DomMulAct.smul_Lp_val : ∀ {M : Type u_1} {α : Type u_3} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure α} {p : ENNReal} [inst_2 : SMul M α] [inst_3 : MeasureTheory.SMulInvariantMeasure M α μ]
  [inst_4 : MeasurableConstSMul M α] (c : Mᵈᵐᵃ) (f : ↥(MeasureTheory.Lp E p μ)), ↑(c • f) = c • ↑f
-- Lean.DocString.Syntax
/-- A footnote use site.

Footnotes must be defined elsewhere using the `[^NAME]: TEXT` syntax.
 -/
Lean.Doc.Syntax.footnote : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- The isomorphism between points of limit cokernel coforks induced by an isomorphism
in the category of arrows.  -/
CategoryTheory.Limits.CokernelCofork.mapIsoOfIsColimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          {X' Y' : C} →
            {f' : X' ⟶ Y'} →
              {cc : CategoryTheory.Limits.CokernelCofork f} →
                {cc' : CategoryTheory.Limits.CokernelCofork f'} →
                  CategoryTheory.Limits.IsColimit cc →
                    CategoryTheory.Limits.IsColimit cc' →
                      (CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f') → (cc.pt ≅ cc'.pt)
-- Mathlib.RingTheory.Polynomial.DegreeLT
Polynomial.degreeLT.basisProd_natAdd : ∀ {R : Type u_1} [inst : Semiring R] (m n : ℕ) (i : Fin n),
  (Polynomial.degreeLT.basisProd R m n) (Fin.natAdd m i) = (0, (Polynomial.degreeLT.basis R n) i)
-- Mathlib.MeasureTheory.OuterMeasure.OfAddContent
/-- Construct a measure from a sigma-subadditive content on a semiring. This
measure is defined on the associated Carathéodory sigma-algebra.  -/
MeasureTheory.AddContent.measureCaratheodory : {α : Type u_1} →
  {C : Set (Set α)} →
    (m : MeasureTheory.AddContent ENNReal C) →
      (hC : MeasureTheory.IsSetSemiring C) → m.IsSigmaSubadditive → MeasureTheory.Measure α
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.View.mk.injEq : ∀ {α : Type u} {β : α → Type v} {size : ℕ} (k : α) (v : β k) (tree : Std.DTreeMap.Internal.Impl.Tree α β size) (k_1 : α)
  (v_1 : β k_1) (tree_1 : Std.DTreeMap.Internal.Impl.Tree α β size),
  ({ k := k, v := v, tree := tree } = { k := k_1, v := v_1, tree := tree_1 }) = (k = k_1 ∧ v ≍ v_1 ∧ tree = tree_1)
-- Init.Data.SInt.Lemmas
Int8.sub_eq_add_neg : ∀ (a b : Int8), a - b = a + -b
-- Lean.MonadEnv
Lean.evalConst : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadEnv m] → [Lean.MonadError m] → [Lean.MonadOptions m] → (α : Type) → Lean.Name → optParam Bool true → m α
-- Mathlib.Data.List.Rotate
List.isRotated_comm : ∀ {α : Type u} {l l' : List α}, l ~r l' ↔ l' ~r l
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.Functor.instAdditiveId : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C],
  (CategoryTheory.Functor.id C).Additive
-- Mathlib.Data.List.Cycle
_private.Mathlib.Data.List.Cycle.0.List.nextOr.match_1.splitter : {α : Type u_1} →
  (motive : List α → α → α → Sort u_2) →
    (x : List α) →
      (x_1 x_2 : α) →
        ((x default : α) → motive [] x default) →
          ((head x default : α) → motive [head] x default) →
            ((y z : α) → (xs : List α) → (x default : α) → motive (y :: z :: xs) x default) → motive x x_1 x_2
-- Init.Data.Int.Order
Int.neg_lt_neg : ∀ {a b : ℤ}, a < b → -b < -a
-- Mathlib.Data.Set.Countable
/-- **Alias** of the forward direction of `Set.countable_iff_exists_surjective`.

---

A non-empty set is countable iff there exists a surjection from the
natural numbers onto the subtype induced by the set.
 -/
Set.Countable.exists_surjective : ∀ {α : Type u} {s : Set α}, s.Nonempty → s.Countable → ∃ f, Function.Surjective f
-- Mathlib.CategoryTheory.Subobject.NoetherianObject
CategoryTheory.isNoetherianObject_of_isZero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C},
  CategoryTheory.Limits.IsZero X → CategoryTheory.IsNoetherianObject X
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddSound
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.sat_of_confirmRupHint_of_insertRat_fold : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n),
  f.ratUnits = #[] ∧ f.AssignmentsInvariant →
    ∀ (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (rupHints : Array ℕ)
      (p : Std.Tactic.BVDecide.LRAT.Internal.PosFin n → Bool),
      Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p f →
        have fc := f.insertRatUnits c.negate;
        have confirmRupHint_fold_res :=
          Array.foldl (Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint fc.1.clauses)
            (fc.1.assignments, [], false, false) rupHints;
        confirmRupHint_fold_res.2.2.1 = true → Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p c
-- Mathlib.SetTheory.Cardinal.Divisibility
Cardinal.le_of_dvd : ∀ {a b : Cardinal.{u_1}}, b ≠ 0 → a ∣ b → a ≤ b
-- Mathlib.Topology.QuasiSeparated
quasiSeparatedSpace_iff : ∀ (α : Type u_3) [inst : TopologicalSpace α],
  QuasiSeparatedSpace α ↔ ∀ (U V : Set α), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)
-- Mathlib.Data.Part
Part.mem_right_unique : ∀ {α : Type u_1} {a : α} {o p : Part α}, a ∈ o → a ∈ p → o = p
-- Mathlib.Order.SuccPred.Limit
Order.IsPredPrelimit.pred_ne : ∀ {α : Type u_1} {a : α} [inst : Preorder α] [inst_1 : PredOrder α] [NoMinOrder α],
  Order.IsPredPrelimit a → ∀ (b : α), Order.pred b ≠ a
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
/-- The objectwise map in the isomorphism `spanFunctor ≅ Profinite.indexFunctor`.  -/
Profinite.NobelingProof.iso_map : {I : Type u} →
  (C : Set (I → Bool)) →
    (J : I → Prop) →
      [inst : (i : I) → Decidable (J i)] → C(↑(Profinite.NobelingProof.π C J), ↑(Profinite.IndexFunctor.obj C J))
-- Init.Data.UInt.Lemmas
UInt8.neg_mul_neg : ∀ (a b : UInt8), -a * -b = a * b
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
/-- the pullback  -/
CategoryTheory.Limits.ChosenPullback.pullback : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₁ X₂ S : C} → {f₁ : X₁ ⟶ S} → {f₂ : X₂ ⟶ S} → CategoryTheory.Limits.ChosenPullback f₁ f₂ → C
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval₂_multiset_sum : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (s : Multiset (Polynomial R))
  (x : S), Polynomial.eval₂ f x s.sum = (Multiset.map (Polynomial.eval₂ f x) s).sum
-- Mathlib.Order.Disjoint
Disjoint.eq_iff : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] {a b : α}, Disjoint a b → (a = b ↔ a = ⊥ ∧ b = ⊥)
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.linkTarget : Lean.Parser.ParserFn
-- Mathlib.Data.Num.Bitwise
PosNum.land_eq_and : ∀ (p q : PosNum), p.land q = p &&& q
-- Mathlib.RingTheory.GradedAlgebra.Basic
GradedRing.projZeroRingHom'_apply_coe : ∀ {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddCommMonoid ι]
  [inst_3 : PartialOrder ι] [inst_4 : CanonicallyOrderedAdd ι] [inst_5 : SetLike σ A] [inst_6 : AddSubmonoidClass σ A]
  (𝒜 : ι → σ) [inst_7 : GradedRing 𝒜] (a : ↥(𝒜 0)), (GradedRing.projZeroRingHom' 𝒜) ↑a = a
-- Batteries.Data.BinomialHeap.Basic
/-- Computes `s.toHeap ++ res` tail-recursively, assuming `n = s.rank`.  -/
Batteries.BinomialHeap.Imp.HeapNode.toHeap.go : {α : Type u_1} →
  Batteries.BinomialHeap.Imp.HeapNode α → ℕ → Batteries.BinomialHeap.Imp.Heap α → Batteries.BinomialHeap.Imp.Heap α
-- Mathlib.Topology.UniformSpace.Basic
UniformSpace.isClosed_ball : ∀ {α : Type ua} [inst : UniformSpace α] (x : α) {V : SetRel α α}, IsClosed V → IsClosed (UniformSpace.ball x V)
-- Mathlib.NumberTheory.FLT.Three
/-- We say that `S : Solution` is minimal if for all `S₁ : Solution`, the multiplicity of `λ` in
`S.c` is less or equal than the multiplicity in `S₁.c`.  -/
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.isMinimal : {K : Type u_1} →
  [inst : Field K] → {ζ : K} → {hζ : IsPrimitiveRoot ζ 3} → FermatLastTheoremForThreeGen.Solution✝ hζ → Prop
-- Mathlib.Order.BooleanAlgebra.Basic
sdiff_eq_self_iff_disjoint : ∀ {α : Type u} {x y : α} [inst : GeneralizedBooleanAlgebra α], x \ y = x ↔ Disjoint y x
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.addMonoid : {R : Type u} → {M : Type v} → [AddMonoid R] → [AddMonoid M] → AddMonoid (TrivSqZeroExt R M)
-- Mathlib.AlgebraicGeometry.Geometrically.Basic
/-- This holds in particular if `Y = Spec K`.  -/
AlgebraicGeometry.self_of_isIntegral_of_geometrically : ∀ {P : CategoryTheory.ObjectProperty AlgebraicGeometry.Scheme} {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y}
  [AlgebraicGeometry.IsIntegral Y] [Subsingleton ↥Y], AlgebraicGeometry.geometrically P f → P X
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.size_le_size_insertIfNew : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α} {v : β k}, m.size ≤ (m.insertIfNew k v).size
-- Mathlib.GroupTheory.IsSubnormal
/-- A normal subgroup is subnormal.  -/
Subgroup.Normal.isSubnormal : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.Normal → H.IsSubnormal
-- Std.Sat.CNF.RelabelFin
Std.Sat.CNF.Clause.of_maxLiteral_eq_none : ∀ (c : Std.Sat.CNF.Clause ℕ), c.maxLiteral = none → ∀ (lit : ℕ), ¬Std.Sat.CNF.Clause.Mem lit c
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
integral_sin_pow_pos : ∀ (n : ℕ), 0 < ∫ (x : ℝ) in 0..Real.pi, Real.sin x ^ n
-- Lean.Meta.WHNF
Lean.Meta.ReduceMatcherResult.reduced.injEq : ∀ (val val_1 : Lean.Expr),
  (Lean.Meta.ReduceMatcherResult.reduced val = Lean.Meta.ReduceMatcherResult.reduced val_1) = (val = val_1)
-- Mathlib.LinearAlgebra.BilinearForm.TensorProduct
LinearMap.BilinMap.baseChange_isSymm : ∀ {R : Type uR} {A : Type uA} {M₂ : Type uM₂} {N₂ : Type uN₂} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid N₂] [inst_4 : Algebra R A] [inst_5 : Module R M₂]
  [inst_6 : Module R N₂] {B₂ : LinearMap.BilinMap R M₂ N₂},
  (∀ (x y : M₂), (B₂ x) y = (B₂ y) x) →
    ∀ (x y : TensorProduct R A M₂),
      ((LinearMap.BilinMap.baseChange A B₂) x) y = ((LinearMap.BilinMap.baseChange A B₂) y) x
-- Mathlib.Order.Interval.Set.Fin
Fin.image_castLE_uIoc : ∀ {m n : ℕ} (i j : Fin m) (h : m ≤ n), Fin.castLE h '' Set.uIoc i j = Set.uIoc (Fin.castLE h i) (Fin.castLE h j)
-- Mathlib.Order.Antisymmetrization
AntisymmRel.ge : ∀ {α : Type u_1} {a b : α} [inst : LE α], AntisymmRel (fun x1 x2 => x1 ≤ x2) a b → b ≤ a
-- Mathlib.Data.List.Sym
_private.Mathlib.Data.List.Sym.0.List.sym.match_1.eq_1 : ∀ {α : Type u_1} (motive : ℕ → List α → Sort u_2) (x : List α) (h_1 : (x : List α) → motive 0 x)
  (h_2 : (x : ℕ) → motive x []) (h_3 : (n : ℕ) → (x : α) → (xs : List α) → motive n.succ (x :: xs)),
  (match 0, x with
    | 0, x => h_1 x
    | x, [] => h_2 x
    | n.succ, x :: xs => h_3 n x xs) =
    h_1 x
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.unmopEquiv_counitIso_inv_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C),
  (CategoryTheory.MonoidalOpposite.unmopEquiv C).counitIso.inv.app X = CategoryTheory.CategoryStruct.id X
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem?_eq_some_iff_exists_beq_and_mem_toList : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α}
  {v : β}, m[k]? = some v ↔ ∃ k', (k == k') = true ∧ (k', v) ∈ m.toList
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKey!_insertMany_list_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α],
  m.WF →
    ∀ {l : List (α × β)} {k k' : α},
      (k == k') = true →
        List.Pairwise (fun a b => (a.1 == b.1) = false) l →
          k ∈ List.map Prod.fst l → (Std.DHashMap.Raw.Const.insertMany m l).getKey! k' = k
-- Mathlib.Algebra.Order.ZeroLEOne
/-- `zero_le_one` with the type argument explicit.  -/
zero_le_one' : ∀ (α : Type u_2) [inst : Zero α] [inst_1 : One α] [inst_2 : LE α] [ZeroLEOneClass α], 0 ≤ 1
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
ContMDiff.congr : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f f₁ : M → M'} {n : WithTop ℕ∞},
  ContMDiff I I' n f → (∀ (y : M), f₁ y = f y) → ContMDiff I I' n f₁
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.instMembershipOfOrd : {α : Type u} → {β : α → Type v} → [Ord α] → Membership α (Std.DTreeMap.Internal.Impl α β)
-- Mathlib.Topology.Algebra.Nonarchimedean.Bases
SubmodulesBasis.nonarchimedean : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : TopologicalSpace R] [inst_4 : Nonempty ι] {B : ι → Submodule R M} (hB : SubmodulesBasis B),
  NonarchimedeanAddGroup M
-- Aesop.RuleSet.Filter
Aesop.RuleSetNameFilter.ns : Aesop.RuleSetNameFilter → Array Aesop.RuleSetName
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.basicOpenSectionsToAffine_isIso : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U)
  (f : ↑(X.presheaf.obj (Opposite.op U))), CategoryTheory.IsIso (hU.basicOpenSectionsToAffine f)
-- Lean.Data.Lsp.BasicAux
Lean.Lsp.instFromJsonRange : Lean.FromJson Lean.Lsp.Range
-- Mathlib.Tactic.Linarith.NNRealPreprocessor
/-- **Alias** of `Mathlib.Tactic.Linarith.getNNRealToRealArg?`.

---

If `e` is of the form `((x : ℝ≥0) : ℝ)`, `NNReal.toReal e` returns `x`.  -/
Mathlib.Tactic.Linarith.isNNRealtoReal : Lean.Expr → Option Lean.Expr
-- Mathlib.Analysis.ODE.Basic
IsIntegralCurveOn.continuousWithinAt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {s : Set ℝ}
  {t₀ : ℝ}, IsIntegralCurveOn γ v s → t₀ ∈ s → ContinuousWithinAt γ s t₀
-- Lean.Elab.Tactic.Basic
/-- Discard the first goal and replace it by the given list of goals,
keeping the other goals. This is used in conjunction with `getMainGoal`.

Contract: between `getMainGoal` and `replaceMainGoal`, nothing manipulates the goal list.

See also `Lean.Elab.Tactic.popMainGoal` and `Lean.Elab.Tactic.pushGoal`/`Lean.Elab.Tactic.pushGoal` for another interface.
 -/
Lean.Elab.Tactic.replaceMainGoal : List Lean.MVarId → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Data.Set.Card
Set.ncard_eq_toFinset_card : ∀ {α : Type u_1} (s : Set α) (hs : autoParam s.Finite Set.ncard_eq_toFinset_card._auto_1), s.ncard = hs.toFinset.card
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.Pi.ι_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {β : Type w} [inst_2 : DecidableEq β] (f : β → C) [inst_3 : CategoryTheory.Limits.HasProduct f] (b c : β),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.ι f b) (CategoryTheory.Limits.Pi.π f c) =
    if h : b = c then CategoryTheory.eqToHom ⋯ else 0
-- Mathlib.Analysis.Calculus.ContDiff.RCLike
/-- If a function is `C^n` with `1 ≤ n`, then the derivative of `f` is also a strict derivative.  -/
ContDiff.hasStrictDerivAt : ∀ {n : WithTop ℕ∞} {𝕂 : Type u_1} [inst : RCLike 𝕂] {F' : Type u_3} [inst_1 : NormedAddCommGroup F']
  [inst_2 : NormedSpace 𝕂 F'] {f : 𝕂 → F'} {x : 𝕂}, ContDiff 𝕂 n f → n ≠ 0 → HasStrictDerivAt f (deriv f x) x
-- Mathlib.CategoryTheory.EffectiveEpi.Preserves
CategoryTheory.Functor.instReflectsEffectiveEpisOfReflectsFiniteEffectiveEpiFamilies : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D)
  [F.ReflectsFiniteEffectiveEpiFamilies], F.ReflectsEffectiveEpis
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.beq_congr : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [inst : BEq β] [EquivBEq α]
  [LawfulHashable α] {m₃ m₄ : Std.HashMap α β}, m₁.Equiv m₃ → m₂.Equiv m₄ → (m₁ == m₂) = (m₃ == m₄)
-- Mathlib.Geometry.Convex.ConvexSpace.Module
/-- Any semimodule over an ordered semiring is a convex space.

This is not an instance because it creates a diamond with structural instances such as
`ConvexSpace R X → ConvexSpace R Y → ConvexSpace R (X × Y)` because
`(∑ i, f i).fst = ∑ i, (f i).fst` isn't defeq, ultimately because `Finset.sum` isn't a field of
`AddCommMonoid` but derived from them through recursion.  -/
Convexity.ConvexSpace.ofModule : {R : Type u_2} →
  {M : Type u_3} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] →
        [inst_2 : IsStrictOrderedRing R] → [inst_3 : AddCommMonoid M] → [Module R M] → Convexity.ConvexSpace R M
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Bicones.functoriality_faithful : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {D : Type uD} [inst_2 : CategoryTheory.Category.{uD', uD} D]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {F : J → C} (G : CategoryTheory.Functor C D)
  [inst_4 : G.PreservesZeroMorphisms] [G.Faithful], (CategoryTheory.Limits.Bicones.functoriality F G).Faithful
-- Lean.Exception
Lean.MonadError.toMonadRef : {m : Type → Type} → [self : Lean.MonadError m] → Lean.MonadRef m
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_eq_isSome_getValueCast? : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)} {a : α},
  Std.Internal.List.containsKey a l = (Std.Internal.List.getValueCast? a l).isSome
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.IsInvInvariant.mk : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Inv G] {μ : MeasureTheory.Measure G}, μ.inv = μ → μ.IsInvInvariant
-- Batteries.Data.Random.MersenneTwister
/-- Coefficients of the twist matrix (`a`).  -/
Batteries.Random.MersenneTwister.Config.xorMask : (self : Batteries.Random.MersenneTwister.Config) → BitVec self.wordSize
-- Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
/-- For finite values `a₀`, the proximity function `proximity f a₀` equals the proximity function for
the value zero of the shifted function `f - a₀`.
 -/
ValueDistribution.proximity_coe_eq_proximity_sub_const_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℂ → E} {a₀ : E},
  ValueDistribution.proximity f ↑a₀ = ValueDistribution.proximity (f - fun x => a₀) 0
-- Mathlib.GroupTheory.Commutator.Basic
Subgroup.commutator_le_left : ∀ {G : Type u_1} [inst : Group G] (H₁ H₂ : Subgroup G) [H₁.Normal], ⁅H₁, H₂⁆ ≤ H₁