mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Descent.Precoverage
_private.Mathlib.CategoryTheory.Sites.Descent.Precoverage.0.CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.hom.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat}
  {J J_1 : CategoryTheory.GrothendieckTopology C} (e_J : J = J_1) [inst_1 : F.IsPrestack J] {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S} {α : ι' → ι}
  {p' : (j : ι') → X' j ⟶ X (α j)} (w : ∀ (j : ι'), CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) = f' j)
  (hf' : CategoryTheory.Sieve.ofArrows X' f' ∈ J S) {D₁ D₂ : F.DescentData f}
  (φ φ_1 :
    (CategoryTheory.Pseudofunctor.DescentData.pullFunctor F ⋯).obj D₁ ⟶
      (CategoryTheory.Pseudofunctor.DescentData.pullFunctor F ⋯).obj D₂),
  φ = φ_1 →
    ∀ (i : ι),
      CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.hom✝ w hf' φ i =
        CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.hom✝ w ⋯ φ_1 i
-- Lean.Parser.Extension
Lean.Parser.runParserAttributeHooks : Lean.Name → Lean.Name → Bool → Lean.AttrM Unit
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNormEssSup_zero : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε : Type u_7} [inst : TopologicalSpace ε]
  [inst_1 : ESeminormedAddMonoid ε], MeasureTheory.eLpNormEssSup 0 μ = 0
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.norm_mkPiAlgebraFin_le : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {n : ℕ} {A : Type u_1} [inst_1 : SeminormedRing A]
  [inst_2 : NormedAlgebra 𝕜 A], ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n A‖ ≤ max 1 ‖1‖
-- Mathlib.Algebra.Order.Floor.Div
Finsupp.floorDiv_apply : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : PartialOrder α]
  [inst_2 : AddCommMonoid β] [inst_3 : PartialOrder β] [inst_4 : SMulZeroClass α β] [inst_5 : FloorDiv α β] (f : ι →₀ β)
  (a : α) (i : ι), (f ⌊/⌋ a) i = f i ⌊/⌋ a
-- Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer
CategoryTheory.instInhabitedIsSplitEqualizerId : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} →
      Inhabited
        (CategoryTheory.IsSplitEqualizer (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X)
          (CategoryTheory.CategoryStruct.id X))
-- Mathlib.Analysis.Calculus.LineDeriv.Measurable
aestronglyMeasurable_lineDeriv_uncurry : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [LocallyCompactSpace 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : MeasurableSpace E] [OpensMeasurableSpace E]
  {F : Type u_3} [inst_6 : NormedAddCommGroup F] [inst_7 : NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F}
  [SecondCountableTopology E],
  Continuous f →
    ∀ (μ : MeasureTheory.Measure (E × E)), MeasureTheory.AEStronglyMeasurable (fun p => lineDeriv 𝕜 f p.1 p.2) μ
-- Mathlib.Algebra.Ring.GeomSum
geom_sum₂_mul_of_ge : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [AddLeftReflectLE R] [AddLeftMono R]
  [ExistsAddOfLE R] [inst_5 : Sub R] [OrderedSub R] {x y : R},
  y ≤ x → ∀ (n : ℕ), (∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.inter_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ m₃ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  m₁.Equiv m₂ → (m₁ ∩ m₃).Equiv (m₂ ∩ m₃)
-- Mathlib.Algebra.Order.Star.Basic
StarOrderedRing.lt_iff : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  {x y : R} [IsCancelAdd R], x < y ↔ ∃ p, p ≠ 0 ∧ p ∈ AddSubmonoid.closure (Set.range fun s => star s * s) ∧ y = x + p
-- Mathlib.Order.Interval.Set.Monotone
AntitoneOn.Ioi : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  AntitoneOn f s → MonotoneOn (fun x => Set.Ioi (f x)) s
-- Mathlib.Topology.Algebra.UniformMulAction
UniformSpace.Completion.instUniformContinuousConstSMul : ∀ (M : Type v) (X : Type x) [inst : UniformSpace X] [inst_1 : SMul M X],
  UniformContinuousConstSMul M (UniformSpace.Completion X)
-- Std.Sat.AIG.Lemmas
Std.Sat.AIG.BinaryInput.cast.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig1 aig2 : Std.Sat.AIG α} (input : aig1.BinaryInput)
  (h : aig1.decls.size ≤ aig2.decls.size), input.cast h = { lhs := input.lhs.cast h, rhs := input.rhs.cast h }
-- Init.Data.BitVec.Lemmas
BitVec.shiftRight_add : ∀ {w : ℕ} (x : BitVec w) (n m : ℕ), x >>> (n + m) = x >>> n >>> m
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.beq'.eq_1 : ∀ (m₁ : Lean.Grind.CommRing.Mon),
  m₁.beq' =
    Lean.Grind.CommRing.Mon.rec (motive := fun x => Lean.Grind.CommRing.Mon → Bool)
      (fun m₂ => Lean.Grind.CommRing.Mon.rec true (fun x x_1 x_2 => false) m₂)
      (fun pw₁ x ih m₂ => Lean.Grind.CommRing.Mon.rec false (fun pw₂ m₂ x => (pw₁.beq' pw₂).and' (ih m₂)) m₂) m₁
-- Mathlib.Algebra.Divisibility.Units
IsRelPrime.dvd_of_dvd_mul_right : ∀ {α : Type u_1} [inst : CommMonoid α] {x y z : α} [DecompositionMonoid α], IsRelPrime x z → x ∣ y * z → x ∣ y
-- Mathlib.Topology.VectorBundle.Basic
/-- A randomly chosen coordinate change on a `VectorPrebundle`, given by
the field `exists_coordChange`.  -/
VectorPrebundle.coordChange : {R : Type u_1} →
  {B : Type u_2} →
    {F : Type u_3} →
      {E : B → Type u_4} →
        [inst : NontriviallyNormedField R] →
          [inst_1 : (x : B) → AddCommMonoid (E x)] →
            [inst_2 : (x : B) → Module R (E x)] →
              [inst_3 : NormedAddCommGroup F] →
                [inst_4 : NormedSpace R F] →
                  [inst_5 : TopologicalSpace B] →
                    [inst_6 : (x : B) → TopologicalSpace (E x)] →
                      (a : VectorPrebundle R F E) →
                        {e e' : Bundle.Pretrivialization F Bundle.TotalSpace.proj} →
                          e ∈ a.pretrivializationAtlas → e' ∈ a.pretrivializationAtlas → B → F →L[R] F
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.coe_inj : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {f g : LocallyConstant X Y}, ⇑f = ⇑g ↔ f = g
-- Mathlib.RepresentationTheory.Irreducible
Representation.IsIrreducible.finrank_eq_one_of_isMulCommutative : ∀ {G : Type u_1} {k : Type u_2} {V : Type u_3} [inst : Monoid G] [inst_1 : Field k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] (ρ : Representation k G V) [ρ.IsIrreducible] [FiniteDimensional k V] [IsAlgClosed k]
  [IsMulCommutative G], Module.finrank k V = 1
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.coe_toEquiv : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁]
  [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂]
  (e : P₁ ≃ᴬ[k] P₂), ⇑(↑e).toEquiv = ⇑e
-- Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
MvPowerSeries.order_mul : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] [NoZeroDivisors R] (f g : MvPowerSeries σ R),
  (f * g).order = f.order + g.order
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.widePushoutShapeOp_obj : ∀ (J : Type w) (X : CategoryTheory.Limits.WidePushoutShape J),
  (CategoryTheory.Limits.widePushoutShapeOp J).obj X = Opposite.op X
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.instIsScalarTowerRing_1 : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (P : Algebra.Extension R S)
  {R₀ : Type u_1} [inst_3 : CommRing R₀] [inst_4 : Algebra R₀ R] [inst_5 : Algebra R₀ S] [inst_6 : IsScalarTower R₀ R S]
  {R₁ : Type u_2} [inst_7 : CommRing R₁] [inst_8 : Algebra R₁ R] [inst_9 : Algebra R₁ S]
  [inst_10 : IsScalarTower R₁ R S] [inst_11 : Algebra R₀ R₁] [IsScalarTower R₀ R₁ R], IsScalarTower R₀ R₁ P.Ring
-- Mathlib.Tactic.NormNum.Basic
/-- Helper function to synthesize a typed `DivisionRing α` expression.  -/
Mathlib.Meta.NormNum.inferDivisionRing : {u : Lean.Level} → (α : Q(Type u)) → Lean.MetaM Q(DivisionRing «$α»)
-- Lean.Util.LeanOptions
Lean.LeanOptions.mk.inj : ∀ {values values_1 : Lean.NameMap Lean.LeanOptionValue},
  { values := values } = { values := values_1 } → values = values_1
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.opNNNorm_le_iff : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : Fintype ι] {f : E [⋀^ι]→L[𝕜] F} {C : NNReal},
  ‖f‖₊ ≤ C ↔ ∀ (m : ι → E), ‖f m‖₊ ≤ C * ∏ i, ‖m i‖₊
-- Batteries.Data.Random.MersenneTwister
/-- Default initialization seed value.  -/
Batteries.Random.MersenneTwister.Config.initSeed : (self : Batteries.Random.MersenneTwister.Config) → BitVec self.wordSize
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
/-- If `f` is continuous alternating, then `f (Σ_{j₁ ∈ A₁} g₁ j₁, ..., Σ_{jₙ ∈ Aₙ} gₙ jₙ)` is the
sum of `f (g₁ (r 1), ..., gₙ (r n))` where `r` ranges over all functions with `r 1 ∈ A₁`, ...,
`r n ∈ Aₙ`. This follows from multilinearity by expanding successively with respect to each
coordinate.  -/
ContinuousAlternatingMap.map_sum_finset : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N] (f : M [⋀^ι]→L[R] N) {α : ι → Type u_7} [inst_7 : Fintype ι] [inst_8 : DecidableEq ι]
  (g' : (i : ι) → α i → M) (A : (i : ι) → Finset (α i)),
  (f fun i => ∑ j ∈ A i, g' i j) = ∑ r ∈ Fintype.piFinset A, f fun i => g' i (r i)
-- Init.Data.Int.DivMod.Lemmas
Int.fmod_fmod_of_dvd : ∀ (n : ℤ) {m k : ℤ}, m ∣ k → (n.fmod k).fmod m = n.fmod m
-- Mathlib.Algebra.WithConv
WithConv.instAddGroup : {A : Type u_2} → [AddGroup A] → AddGroup (WithConv A)
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.integral_eq_zero_of_ae : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {f : X → E} {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G},
  f =ᵐ[μ.variation] 0 → ∫ᵛ (x : X), f x ∂[B; μ] = 0
-- Init.Data.Float.Float32
instDecidableEqFloat32 : DecidableEq Float32
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
/-- The map `S → T` when `S` is a subalgebra contained in the subalgebra `T`.

This is the subalgebra version of `Submodule.inclusion`, or `Subring.inclusion`  -/
Subalgebra.inclusion : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] → [inst_2 : Algebra R A] → {S T : Subalgebra R A} → S ≤ T → ↥S →ₐ[R] ↥T
-- Lean.Elab.Open
Lean.Elab.OpenDecl.State.currNamespace : Lean.Elab.OpenDecl.State → Lean.Name
-- Mathlib.Data.Finsupp.Basic
Finsupp.sumElim_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Zero γ] (f : α →₀ γ) (g : β →₀ γ) (x : α ⊕ β),
  (f.sumElim g) x = Sum.elim (⇑f) (⇑g) x
-- Init.Data.List.Attach
_private.Init.Data.List.Attach.0.List.filterMap.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (x : Option β) → (Unit → motive none) → ((b : β) → motive (some b)) → motive x
-- Mathlib.Data.Int.Bitwise
/-- Compare with `Int.zero_shiftLeft`, which has `n : ℕ`.  -/
Int.zero_shiftLeft' : ∀ (n : ℤ), 0 <<< n = 0
-- Mathlib.Logic.Relation
/-- **Alias** of `Std.Refl.map`. -/
Relation.map_reflexive : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} [Std.Refl r] {f : α → β},
  Function.Surjective f → Std.Refl (Relation.Map r f f)
-- Mathlib.LinearAlgebra.Matrix.WithConv
instStarWithConvMatrix : {m : Type u_1} → {n : Type u_2} → {α : Type u_3} → [Star α] → Star (WithConv (Matrix m n α))
-- Mathlib.Order.Filter.Pointwise
Filter.divisionMonoid.eq_1 : ∀ {α : Type u_2} [inst : DivisionMonoid α],
  Filter.divisionMonoid =
    { toMonoid := Filter.monoid, toInv := Filter.instInvolutiveInv.toInv, toDiv := Filter.instDiv, toZPow := ZPow.ofPow,
      div_eq_mul_inv := ⋯, zpow_zero' := ⋯, zpow_succ' := ⋯, zpow_neg' := ⋯, inv_inv := ⋯, mul_inv_rev := ⋯,
      inv_eq_of_mul := ⋯ }
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj_d_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} (P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)) (i j : ι),
  ((CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj P).d i j).f =
    CategoryTheory.CategoryStruct.comp (P.p.f i) (P.X.d i j)
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
WithTop.sSup_of_not_bddAbove : ∀ {α : Type u_1} [inst : LE α] [inst_1 : SupSet α] {s : Set (WithTop α)}, ¬BddAbove (WithTop.some ⁻¹' s) → sSup s = ⊤
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.size_ofList_le : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List (α × β)},
  (Std.TreeMap.ofList l cmp).size ≤ l.length
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.FullyFaithful.comp_preimage : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} E] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful)
  {G : CategoryTheory.Functor D E} (hG : G.FullyFaithful) {X Y : C} (f : (F.comp G).obj X ⟶ (F.comp G).obj Y),
  (hF.comp hG).preimage f = hF.preimage (hG.preimage f)
-- Mathlib.Order.SuccPred.Limit
Order.not_isSuccPrelimit_iff_succ_eq : ∀ {α : Type u_1} {a : α} [inst : PartialOrder α] [inst_1 : SuccOrder α],
  ¬Order.IsSuccPrelimit a ↔ ∃ b, ¬IsMax b ∧ Order.succ b = a
-- Mathlib.Tactic.NormNum.Ordinal
Mathlib.Meta.NormNum.isNat_ordinalDiv : ∀ {a b : Ordinal.{u}} {an bn rn : ℕ},
  Mathlib.Meta.NormNum.IsNat a an →
    Mathlib.Meta.NormNum.IsNat b bn → an / bn = rn → Mathlib.Meta.NormNum.IsNat (a / b) rn
-- Mathlib.Topology.Category.CompHausLike.Basic
CompHausLike.homeoOfIso_symm_apply : ∀ {P : TopCat → Prop} {X Y : CompHausLike P} (f : X ≅ Y) (a : ↑Y.toTop),
  (CompHausLike.homeoOfIso f).symm a = (CategoryTheory.ConcreteCategory.hom f.inv.hom) a
-- Mathlib.LinearAlgebra.Ray
/-- If two nonzero vectors are equivalent, so are their negations.  -/
RayVector.equiv_neg_iff : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {v₁ v₂ : RayVector R M}, -v₁ ≈ -v₂ ↔ v₁ ≈ v₂
-- Mathlib.SetTheory.Ordinal.Notation
ONote.oadd_lt_oadd_1 : ∀ {e₁ : ONote} {n₁ : ℕ+} {o₁ e₂ : ONote} {n₂ : ℕ+} {o₂ : ONote},
  (e₁.oadd n₁ o₁).NF → e₁ < e₂ → e₁.oadd n₁ o₁ < e₂.oadd n₂ o₂
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
/-- The square with `0 : 0 ⟶ 0` on the top and `𝟙 X` on the bottom is a pullback square.  -/
CategoryTheory.IsPullback.zero_top : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X : C),
  CategoryTheory.IsPullback 0 0 0 (CategoryTheory.CategoryStruct.id X)
-- Mathlib.RingTheory.Valuation.Basic
Valuation.IsEquiv.eq_iff : ∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀]
  [inst_2 : LinearOrderedCommMonoidWithZero Γ'₀] {v₁ : Valuation R Γ₀} {v₂ : Valuation R Γ'₀},
  v₁.IsEquiv v₂ → ∀ {r s : R}, v₁ r = v₁ s ↔ v₂ r = v₂ s
-- Mathlib.Analysis.LocallyConvex.BalancedCoreHull
subset_balancedHull : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [NormOneClass 𝕜] {s : Set E}, s ⊆ balancedHull 𝕜 s
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.size_insertIfNew_le : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β k}, (m.insertIfNew k v).size ≤ m.size + 1
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- **Alias** of `neg_apply`. -/
SchwartzMap.neg_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Neg β}
  {inst_2 : Neg F} [self : IsNegApply F α β] (f : F) (x : α), (-f) x = -f x
-- Mathlib.Computability.TuringMachine.Tape
Turing.Tape.mk'_left_right₀ : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (T : Turing.Tape Γ), Turing.Tape.mk' T.left T.right₀ = T
-- Init.Try
Lean.Parser.Tactic.tryTrace : Lean.ParserDescr
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.instInhabited.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.Mon.instInhabited = { default := CategoryTheory.Mon.trivial C }
-- Mathlib.LinearAlgebra.Semisimple
Module.End.IsFinitelySemisimple.restrict : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {p : Submodule R M} (hp : p ∈ f.invtSubmodule),
  f.IsFinitelySemisimple → Module.End.IsFinitelySemisimple (LinearMap.restrict f hp)
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffSection.coe_zero : ∀ {𝕜 : 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] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] [inst_11 : (x : M) → AddCommGroup (V x)]
  [inst_12 : (x : M) → Module 𝕜 (V x)] [inst_13 : VectorBundle 𝕜 F V], ⇑0 = 0
-- Mathlib.MeasureTheory.Measure.MeasuredSets
/-- Given a semiring of sets `C` covering the space modulo `0` and generating the measurable space
structure, finite unions of elements of `C` are dense among measurable sets.  -/
MeasureTheory.dense_of_generateFrom_isSetSemiring : ∀ {α : Type u_1} [mα : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst : MeasureTheory.IsFiniteMeasure μ]
  {C : Set (Set α)},
  MeasureTheory.IsSetSemiring C →
    (∃ D, D.Countable ∧ D ⊆ C ∧ μ (⋃₀ D)ᶜ = 0) →
      mα = MeasurableSpace.generateFrom C → Dense (SetLike.coe ⁻¹' supClosure C)
-- Mathlib.Topology.Algebra.Group.Units
Units.symm_mapContinuousMulEquiv : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Monoid M]
  [inst_3 : Monoid N] (f : M ≃ₜ* N), (Units.mapContinuousMulEquiv f).symm = Units.mapContinuousMulEquiv f.symm
-- Mathlib.Algebra.Order.Group.Synonym
ofColex_vadd' : ∀ {β : Type u_2} {α : Type u_1} [inst : VAdd β α] (b : Colex β) (a : α), ofColex b +ᵥ a = b +ᵥ a
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.d_toCycles : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j k : ι) [inst_2 : K.HasHomology k],
  CategoryTheory.CategoryStruct.comp (K.d i j) (K.toCycles j k) = 0
-- Std.Do.Triple.SpecLemmas
Std.Do.Iter.foldM_filterMapM : ∀ {ps : Std.Do.PostShape} {α β γ δ : Type w} {n : Type w → Type w''} {o : Type w → Type w'''}
  [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Monad n] [inst_3 : MonadAttach n] [LawfulMonad n]
  [WeaklyLawfulMonadAttach n] [inst_6 : Monad o] [LawfulMonad o] [inst_8 : Std.Do.WPMonad o ps]
  [inst_9 : Std.IteratorLoop α Id n] [inst_10 : Std.IteratorLoop α Id o] [Std.LawfulIteratorLoop α Id n]
  [Std.LawfulIteratorLoop α Id o] [inst_13 : MonadLiftT n o] [LawfulMonadLiftT n o] {f : β → n (Option γ)}
  {g : δ → γ → o δ} {init : δ} {it : Std.Iter β} {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond δ ps},
  ⦃P⦄
      Std.Iter.foldM
        (fun d b => do
          let __x ← liftM (f b)
          match __x with
            | some c => g d c
            | x => pure d)
        init it ⦃Q⦄ →
    ⦃P⦄ Std.IterM.foldM g init (Std.Iter.filterMapM f it) ⦃Q⦄
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : α → β → Option γ} {k : α} (h : m.WF),
  (Std.HashMap.Raw.filterMap f m).getKey? k = (m.getKey? k).pfilter fun x h' => (f x m[x]).isSome
-- Mathlib.Data.List.Sort
/-- The list obtained from a strictly monotone tuple is sorted.  -/
StrictMono.sortedLT_ofFn : ∀ {α : Type u_1} [inst : Preorder α] {n : ℕ} {f : Fin n → α}, StrictMono f → (List.ofFn f).SortedLT
-- Mathlib.RepresentationTheory.Coinvariants
Representation.finsuppToCoinvariants.eq_1 : ∀ {k : Type u_6} {G : Type u_7} {V : Type u_8} [inst : CommRing k] [inst_1 : Group G] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] (ρ : Representation k G V) (α : Type u_9),
  ρ.finsuppToCoinvariants α =
    (Finsupp.lsum k) fun a =>
      Representation.Coinvariants.lift ρ (Representation.Coinvariants.mk (ρ.finsupp α) ∘ₗ Finsupp.lsingle a) ⋯
-- Std.Do.Triple.SpecLemmas
List.Cursor.suffix_at : ∀ {α : Type u_1} {n : ℕ} (l : List α), (List.Cursor.at l n).suffix = List.drop n l
-- Mathlib.CategoryTheory.FiberedCategory.Cocartesian
CategoryTheory.Functor.IsStronglyCocartesian.mk : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  {p : CategoryTheory.Functor 𝒳 𝒮} {R S : 𝒮} {a b : 𝒳} {f : R ⟶ S} {φ : a ⟶ b} [toIsHomLift : p.IsHomLift f φ],
  (∀ {b' : 𝒳} (g : S ⟶ p.obj b') (φ' : a ⟶ b') [p.IsHomLift (CategoryTheory.CategoryStruct.comp f g) φ'],
      ∃! χ, p.IsHomLift g χ ∧ CategoryTheory.CategoryStruct.comp φ χ = φ') →
    p.IsStronglyCocartesian f φ
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.mk_proj_snd : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e : Bundle.Trivialization F proj) {x : Z}, x ∈ e.source → (proj x, (↑e x).2) = ↑e x
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
/-- Each tagged point belongs to `I`  -/
BoxIntegral.TaggedPrepartition.tag_mem_Icc : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (self : BoxIntegral.TaggedPrepartition I) (J : BoxIntegral.Box ι),
  self.tag J ∈ BoxIntegral.Box.Icc I
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.exfalso'.injEq : ∀ (p p_1 : Mathlib.Tactic.ITauto.Proof), (p.exfalso' = p_1.exfalso') = (p = p_1)
-- Init.Prelude
/-- Translates an action from monad `m` into monad `n`.  -/
MonadLiftT.monadLift : {m : Type u → Type v} → {n : Type u → Type w} → [self : MonadLiftT m n] → {α : Type u} → m α → n α
-- Mathlib.Algebra.MonoidAlgebra.Module
MonoidAlgebra.mapDomainLinearMap.eq_1 : ∀ (R : Type u_1) (S : Type u_2) {M : Type u_3} {N : Type u_4} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : Module R S] (f : M → N),
  MonoidAlgebra.mapDomainLinearMap R S f =
    ↑(MonoidAlgebra.coeffLinearEquiv R).symm ∘ₗ Finsupp.lmapDomain S R f ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv R)
-- Mathlib.Analysis.Normed.Module.FiniteDimension
/-- **Alias** of `isOpen_setOfPred_affineIndependent`. -/
isOpen_setOf_affineIndependent : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [CompleteSpace 𝕜] {ι : Type u_1} [Finite ι], IsOpen {p | AffineIndependent 𝕜 p}
-- Init.Data.UInt.Bitwise
UInt32.toUInt8_or : ∀ (a b : UInt32), (a ||| b).toUInt8 = a.toUInt8 ||| b.toUInt8
-- Mathlib.Order.Category.Lat
Lat.hom_ofHom : ∀ {X Y : Type u} [inst : Lattice X] [inst_1 : Lattice Y] (f : LatticeHom X Y), Lat.Hom.hom (Lat.ofHom f) = f