mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.TensorProduct.DirectLimit
/-- `M ⊗ (limᵢ Gᵢ)` and `limᵢ (M ⊗ Gᵢ)` are isomorphic as modules
 -/
TensorProduct.directLimitRight : {R : Type u_1} →
  [inst : CommSemiring R] →
    {ι : Type u_2} →
      [inst_1 : DecidableEq ι] →
        [inst_2 : Preorder ι] →
          {G : ι → Type u_3} →
            [inst_3 : (i : ι) → AddCommMonoid (G i)] →
              [inst_4 : (i : ι) → Module R (G i)] →
                (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) →
                  (M : Type u_4) →
                    [inst_5 : AddCommMonoid M] →
                      [inst_6 : Module R M] →
                        TensorProduct R M (Module.DirectLimit G f) ≃ₗ[R]
                          Module.DirectLimit (fun x => TensorProduct R M (G x)) fun i j h =>
                            LinearMap.lTensor M (f i j h)
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.iIndepSets.eq_1 : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} (π : ι → Set (Set Ω))
  (κ : ProbabilityTheory.Kernel α Ω) (μ : MeasureTheory.Measure α),
  ProbabilityTheory.Kernel.iIndepSets π κ μ =
    ∀ (s : Finset ι) {f : ι → Set Ω}, (∀ i ∈ s, f i ∈ π i) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ s, f i) = ∏ i ∈ s, (κ a) (f i)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
AlgebraicGeometry.Proj.mapAffineOpenCover_I₀ : ∀ {A B σ τ : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] [inst_3 : CommRing B]
  [inst_4 : SetLike τ B] [inst_5 : AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [inst_6 : GradedRing 𝒜]
  [inst_7 : GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ)
  (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜)),
  (AlgebraicGeometry.Proj.mapAffineOpenCover f hf).I₀ = (AlgebraicGeometry.Proj.affineOpenCover 𝒜).I₀
-- Mathlib.LinearAlgebra.AffineSpace.Basis
AffineBasis.basisOf_smul : ∀ {ι : Type u_1} {G : Type u_3} {k : Type u_5} {V : Type u_6} [inst : AddCommGroup V] [inst_1 : Ring k]
  [inst_2 : Module k V] [inst_3 : Group G] [inst_4 : DistribMulAction G V] [inst_5 : SMulCommClass G k V] (a : G)
  (b : AffineBasis ι k V) (i : ι), (a • b).basisOf i = a • b.basisOf i
-- Mathlib.Analysis.Complex.Circle
Circle.instIsScalarTower : ∀ {α : Type u_1} {β : Type u_2} [inst : SMul ℂ α] [inst_1 : SMul ℂ β] [inst_2 : SMul α β] [IsScalarTower ℂ α β],
  IsScalarTower Circle α β
-- Init.Data.List.Nat.Erase
List.set_eraseIdx : ∀ {α : Type u_1} {xs : List α} {i j : ℕ} {a : α},
  (xs.eraseIdx i).set j a = if i ≤ j then (xs.set (j + 1) a).eraseIdx i else (xs.set j a).eraseIdx i
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.Hexagon.functor₂₃₁'_obj_obj_obj : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] (G H K : C),
  (((CategoryTheory.BraidedCategory.Hexagon.functor₂₃₁' C).obj G).obj H).obj K =
    CategoryTheory.MonoidalCategoryStruct.tensorObj H (CategoryTheory.MonoidalCategoryStruct.tensorObj K G)
-- Mathlib.Algebra.Order.Group.Synonym
ofLex_mul : ∀ {α : Type u_1} [inst : Mul α] (a b : Lex α), ofLex (a * b) = ofLex a * ofLex b
-- Mathlib.Data.ENat.Basic
ENat.succ_natCast : ∀ (n : ℕ), SuccOrder.succ ↑n = ↑(n + 1)
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
CategoryTheory.GrothendieckTopology.Plus.toPlus_eq_mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t}
  [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [instCC : CategoryTheory.ConcreteCategory D FD]
  [inst_3 :
    ∀ {X : C} (S : J.Cover X),
      CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape)
        (CategoryTheory.forget D)]
  [inst_4 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [inst_5 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  {X : C} {P : CategoryTheory.Functor Cᵒᵖ D} (x : CategoryTheory.ToType (P.obj (Opposite.op X))),
  (CategoryTheory.ConcreteCategory.hom ((J.toPlus P).app (Opposite.op X))) x =
    CategoryTheory.GrothendieckTopology.Plus.mk (CategoryTheory.Meq.mk ⊤ x)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.ofList_cons : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {k : α} {v : β k}
  {tl : List ((a : α) × β a)}, Std.ExtDTreeMap.ofList (⟨k, v⟩ :: tl) cmp = (∅.insert k v).insertMany tl
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
/-- The functor `HomologicalComplex (Karoubi C) c ⥤ Karoubi (HomologicalComplex C c)`.  -/
CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.inverse : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          CategoryTheory.Functor (HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) c)
            (CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c))
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SetLike.instSMulCommClassSubtypeMem_2 : ∀ {S : Type u'} {M : Type v} {N : Type u_1} {α : Type u_2} [inst : SetLike S α] [inst_1 : SMul M N] [inst_2 : SMul M α]
  [inst_3 : Monoid N] [inst_4 : MulAction N α] [inst_5 : SMulMemClass S N α] [inst_6 : IsScalarTower M N α] (s : S)
  [SMulCommClass N M α], SMulCommClass N M ↥s
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKeyD_le : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {k fallback : α}, (cmp (t.maxKeyD fallback) k).isLE = true ↔ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Init.Data.BitVec.Lemmas
BitVec.abs_intMin : ∀ {w : ℕ}, (BitVec.intMin w).abs = BitVec.intMin w
-- Mathlib.Data.Finset.Insert
Finset.ssubset_singleton_iff : ∀ {α : Type u_1} {s : Finset α} {a : α}, s ⊂ {a} ↔ s = ∅
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits
CategoryTheory.NatTrans.instIsClosedUnderLimitsOfShapeOverFunctorEquifiberedHomOfHasCoproductsOfShapeHom : ∀ {J : Type u_1} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} C] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F : CategoryTheory.Functor C D) [∀ (a b : C), CategoryTheory.Limits.HasCoproductsOfShape (a ⟶ b) D],
  CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape (fun f => CategoryTheory.NatTrans.Equifibered f.hom) J
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
AlgebraicGeometry.Scheme.jointlySurjectivePrecoverage.eq_1 : AlgebraicGeometry.Scheme.jointlySurjectivePrecoverage =
  CategoryTheory.Precoverage.comap AlgebraicGeometry.Scheme.forget CategoryTheory.Types.jointlySurjectivePrecoverage
-- Mathlib.Topology.Specialization
Specialization.map_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] (g : C(β, γ)) (f : C(α, β)),
  Specialization.map (g.comp f) = (Specialization.map g).comp (Specialization.map f)
-- Init.Data.Array.Basic
/-- Removes the first element that satisfies the predicate `p`. If no element satisfies `p`, the array
is returned unmodified.

This function takes worst-case `O(n)` time because it back-shifts all later elements.

Examples:
* `#["red", "green", "", "blue"].eraseP (·.isEmpty) = #["red", "green", "blue"]`
* `#["red", "green", "", "blue", ""].eraseP (·.isEmpty) = #["red", "green", "blue", ""]`
* `#["red", "green", "blue"].eraseP (·.length % 2 == 0) = #["red", "green"]`
* `#["red", "green", "blue"].eraseP (fun _ => true) = #["green", "blue"]`
* `(#[] : Array String).eraseP (fun _ => true) = #[]`
 -/
Array.eraseP : {α : Type u} → Array α → (α → Bool) → Array α
-- Std.Http.Data.Body.Stream
/-- A waiter for `Stream.interestSelector`.
 -/
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Channel.State.interestWaiter : Std.Http.Body.Channel.State✝ → Option (Std.Async.Waiter Bool)
-- Lean.Meta.Basic
Lean.Meta.instHashableSynthInstanceCacheKey.hash : Lean.Meta.SynthInstanceCacheKey → UInt64
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.instSMulCommClass : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  {S : NonUnitalSubalgebra R A} [SMulCommClass R A A], SMulCommClass R ↥S ↥S
-- Mathlib.Data.Prod.Basic
Prod.eq_iff_fst_eq_snd_eq : ∀ {α : Type u_1} {β : Type u_2} {p q : α × β}, p = q ↔ p.1 = q.1 ∧ p.2 = q.2
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.eq_empty_iff_forall_contains : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α],
  m = ∅ ↔ ∀ (a : α), m.contains a = false
-- Mathlib.Algebra.Homology.AlternatingConst
HomologicalComplex.alternatingConst_iCycles_even_comp_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (A : C) {φ ψ : A ⟶ A} (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0)
  (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) {c : ComplexShape ℕ} [inst_2 : DecidableRel c.Rel]
  (hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)) [inst_3 : CategoryTheory.CategoryWithHomology C] {j : ℕ},
  c.Rel (c.prev j) j →
    c.Rel j (c.next j) →
      Even j →
        ∀ {F : C → C → Type uF} {carrier : C → Type w}
          {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)}
          [inst_4 : CategoryTheory.ConcreteCategory C F]
          (x : carrier ((HomologicalComplex.alternatingConst A hOdd hEven hc).cycles j)),
          (CategoryTheory.ConcreteCategory.hom φ)
              ((CategoryTheory.ConcreteCategory.hom ((HomologicalComplex.alternatingConst A hOdd hEven hc).iCycles j))
                x) =
            (CategoryTheory.ConcreteCategory.hom 0) x
-- Init.Data.String.Lemmas.Pattern.Find.Pred
String.Slice.Pos.find?_bool_eq_none_iff : ∀ {p : Char → Bool} {s : String.Slice} {pos : s.Pos},
  pos.find? p = none ↔ ∀ (pos' : s.Pos), pos ≤ pos' → ∀ (h : pos' ≠ s.endPos), p (pos'.get h) = false
-- Mathlib.Data.List.Defs
_private.Mathlib.Data.List.Defs.0.List.headI.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (a : α) (tail : List α) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (tail : List α) → motive (a :: tail)),
  (match a :: tail with
    | [] => h_1 ()
    | a :: tail => h_2 a tail) =
    h_2 a tail
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.add_lt_top : ∀ {α : Type u} [inst : Add α] {x y : WithTop α} [inst_1 : LT α], x + y < ⊤ ↔ x < ⊤ ∧ y < ⊤
-- Mathlib.Data.NNRat.Defs
Mathlib.Tactic.Qify.nnratCast_ne : ∀ (a b : ℚ≥0), a ≠ b ↔ ↑a ≠ ↑b
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitInfo.default.inj : ∀ {e : Lean.Expr} {source : Lean.Meta.Grind.SplitSource} {e_1 : Lean.Expr} {source_1 : Lean.Meta.Grind.SplitSource},
  Lean.Meta.Grind.SplitInfo.default e source = Lean.Meta.Grind.SplitInfo.default e_1 source_1 →
    e = e_1 ∧ source = source_1
-- Init.Data.String.Basic
String.Pos.Raw.utf8GetAux : List Char → String.Pos.Raw → String.Pos.Raw → Char
-- Init.Data.Option.Attach
Option.unattach.eq_1 : ∀ {α : Type u_1} {p : α → Prop} (o : Option { x // p x }), o.unattach = Option.map (fun x => ↑x) o
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.UInt32.toBitVec_ite : ∀ {c : Prop} {t e : UInt32} [inst : Decidable c], (if c then t else e).toBitVec = if c then t.toBitVec else e.toBitVec
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
/-- If a function vanishes on `t \ s` with `s ⊆ t`, then its integrals on `s`
and `t` coincide.  -/
MeasureTheory.VectorMeasure.setIntegral_eq_of_subset_of_forall_sdiff_eq_zero : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F} {f : X → E}
  {s t : Set X} [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G]
  {B : E →L[ℝ] F →L[ℝ] G},
  MeasurableSet s →
    MeasurableSet t → s ⊆ t → (∀ x ∈ t \ s, f x = 0) → ∫ᵛ (x : X) in t, f x ∂[B; μ] = ∫ᵛ (x : X) in s, f x ∂[B; μ]
-- Mathlib.Order.Basic
PUnit.not_lt : ∀ (a b : PUnit.{u_5 + 1}), ¬a < b
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Set.measurable_restrict₂_apply : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace γ] {s t : Set α} (hst : s ⊆ t)
  {f : ↑t → γ}, Measurable f → Measurable (Set.domRestrict₂ hst f)
-- Mathlib.Computability.Reduce
Computable.eqv : ∀ (α : Type u_1) [inst : Denumerable α], (Denumerable.eqv α).Computable
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.iInf_mul_le_lintegral : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → ENNReal),
  (⨅ x, f x) * μ Set.univ ≤ ∫⁻ (x : α), f x ∂μ
-- Init.Data.UInt.Bitwise
instCommutativeUSizeHOr : Std.Commutative fun x1 x2 => x1 ||| x2
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
/-- If `R` is of characteristic `p` and `¬p ∣ m`, then
`cyclotomic (p ^ k * m) R = (cyclotomic m R) ^ (p ^ k - p ^ (k - 1))`.  -/
Polynomial.cyclotomic_mul_prime_pow_eq : ∀ (R : Type u_1) {p m : ℕ} [Fact (Nat.Prime p)] [inst : Ring R] [CharP R p],
  ¬p ∣ m → ∀ {k : ℕ}, 0 < k → Polynomial.cyclotomic (p ^ k * m) R = Polynomial.cyclotomic m R ^ (p ^ k - p ^ (k - 1))
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.FullyFaithful.faithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful), F.Faithful
-- Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
MeasureTheory.mul_meas_ge_le_pow_eLpNorm : ∀ {α : Type u_1} {ε' : Type u_3} {m0 : MeasurableSpace α} [inst : TopologicalSpace ε'] [inst_1 : ContinuousENorm ε']
  {p : ENNReal} (μ : MeasureTheory.Measure α),
  p ≠ 0 →
    p ≠ ⊤ →
      ∀ {f : α → ε'},
        MeasureTheory.AEStronglyMeasurable f μ →
          ∀ (ε : ENNReal), ε * μ {x | ε ≤ ‖f x‖ₑ ^ p.toReal} ≤ MeasureTheory.eLpNorm f p μ ^ p.toReal
-- Mathlib.Analysis.SpecialFunctions.Integrability.Basic
intervalIntegral.intervalIntegrable_zpow : ∀ {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] {n : ℤ},
  0 ≤ n ∨ 0 ∉ Set.uIcc a b → IntervalIntegrable (fun x => x ^ n) μ a b
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithInitial.Hom.match_1.eq_3 : ∀ {C : Type u_1} (motive : CategoryTheory.WithInitial C → CategoryTheory.WithInitial C → Sort u_2)
  (x : CategoryTheory.WithInitial C)
  (h_1 : (X Y : C) → motive (CategoryTheory.WithInitial.of X) (CategoryTheory.WithInitial.of Y))
  (h_2 : (a : C) → (x : CategoryTheory.WithInitial C) → motive (CategoryTheory.WithInitial.of a) x)
  (h_3 : (x : CategoryTheory.WithInitial C) → motive CategoryTheory.WithInitial.star x),
  (match CategoryTheory.WithInitial.star, x with
    | CategoryTheory.WithInitial.of X, CategoryTheory.WithInitial.of Y => h_1 X Y
    | CategoryTheory.WithInitial.of a, x => h_2 a x
    | CategoryTheory.WithInitial.star, x => h_3 x) =
    h_3 x
-- Lean.Data.Options
Lean.MonadWithOptions : (Type → Type) → Type 1
-- Batteries.Data.String.Lemmas
String.join_eq : ∀ (ss : List String), String.join ss = String.ofList (List.map String.toList ss).flatten
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.coe_finsum : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {ι : Type u_3} {F : ι → Function.locallyFinsuppWithin U ℤ},
  ⇑(∑ᶠ (i : ι), F i) = ∑ᶠ (i : ι), ⇑(F i)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem?_union : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, (m₁ ∪ m₂)[k]? = m₂[k]?.or m₁[k]?
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.isBase_iff_minimal_spanning : ∀ {α : Type u_2} {M : Matroid α} {B : Set α}, M.IsBase B ↔ Minimal M.Spanning B
-- Mathlib.RingTheory.Polynomial.Basic
MvPolynomial.aeval_natDegree_le : ∀ {σ : Type v} {R : Type u_2} [inst : CommSemiring R] {m n : ℕ} (F : MvPolynomial σ R),
  F.totalDegree ≤ m →
    ∀ (f : σ → Polynomial R), (∀ (i : σ), (f i).natDegree ≤ n) → ((MvPolynomial.aeval f) F).natDegree ≤ m * n
-- Mathlib.FieldTheory.Minpoly.Field
minpoly.eq_iff_aeval_eq_zero : ∀ {A : Type u_1} {B : Type u_2} [inst : Field A] [inst_1 : Ring B] [inst_2 : Algebra A B] {x : B} [Nontrivial B]
  {p : Polynomial A}, Irreducible p → p.Monic → (p = minpoly A x ↔ (Polynomial.aeval x) p = 0)
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.restrict_isRestriction : ∀ {α : Type u_1} (M : Matroid α) (R : Set α),
  autoParam (R ⊆ M.E) Matroid.restrict_isRestriction._auto_1 → (M.restrict R).IsRestriction M
-- Mathlib.Tactic.Translate.UnfoldBoundary
/-- Modify `e` so that it is well typed if the constants in `b` cannot be unfolded.

Note: it may be that `e` contains some constant whose type is not well typed in this setting.
We don't make an effort to replace such constants.
It seems that this approximation works well enough.  -/
Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaries.insertBoundaries : Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaries → Lean.Expr → Lean.Name → Lean.MetaM Lean.Expr
-- Std.Data.HashMap.Basic
/-- The notation `m[a]!` is preferred over calling this function directly.

Tries to retrieve the mapping for the given key, panicking if no such mapping is present.
 -/
Std.HashMap.get! : {α : Type u} → {β : Type v} → {x : BEq α} → {x_1 : Hashable α} → [Inhabited β] → Std.HashMap α β → α → β
-- Lean.Language.Basic
Lean.Language.instInhabitedTransformedSnap : {α : Type} → [Inhabited α] → Inhabited (Lean.Language.TransformedSnap α)
-- Mathlib.Data.List.Destutter
List.destutter_sublist : ∀ {α : Type u_1} (R : α → α → Prop) [inst : DecidableRel R] (l : List α), (List.destutter R l).Sublist l
-- Mathlib.Tactic.Linarith.Datatypes
/-- `c.vars` returns the list of variables that appear in the linear expression contained in `c`.  -/
Mathlib.Tactic.Linarith.Comp.vars : Mathlib.Tactic.Linarith.Comp → List ℕ
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassDivision.isWeierstrassFactorization : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A] {g q : PowerSeries A} {r : Polynomial A}
  (hg : (PowerSeries.map (IsLocalRing.residue A)) g ≠ 0)
  (H : (PowerSeries.X ^ ((PowerSeries.map (IsLocalRing.residue A)) g).order.toNat).IsWeierstrassDivision g q r),
  g.IsWeierstrassFactorization (Polynomial.X ^ ((PowerSeries.map (IsLocalRing.residue A)) g).order.toNat - r) ↑⋯.unit⁻¹
-- Mathlib.Algebra.Category.ModuleCat.Basic
/-- The categorical equivalence between `ModuleCat` and `SemimoduleCat`.

In the inverse direction, data (such as the negation operation) is created which may lead to
diamonds when applied to semi-modules that already have an existing additive group structure.  -/
ModuleCat.equivalenceSemimoduleCat : {R : Type u} → [inst : Ring R] → ModuleCat R ≌ SemimoduleCat R
-- Mathlib.AlgebraicGeometry.Morphisms.Finite
AlgebraicGeometry.IsFinite.instIsStableUnderCompositionScheme : CategoryTheory.MorphismProperty.IsStableUnderComposition @AlgebraicGeometry.IsFinite
-- Mathlib.Data.Finsupp.Single
Finsupp.erase_idem : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (f : α →₀ M) (a : α),
  Finsupp.erase a (Finsupp.erase a f) = Finsupp.erase a f
-- Lean.Elab.Level
Lean.Elab.Level.Context.mk.inj : ∀ {options : Lean.Options} {ref : Lean.Syntax} {autoBoundImplicit : Bool} {options_1 : Lean.Options}
  {ref_1 : Lean.Syntax} {autoBoundImplicit_1 : Bool},
  { options := options, ref := ref, autoBoundImplicit := autoBoundImplicit } =
      { options := options_1, ref := ref_1, autoBoundImplicit := autoBoundImplicit_1 } →
    options = options_1 ∧ ref = ref_1 ∧ autoBoundImplicit = autoBoundImplicit_1
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToCodeBlock.checkNotShadowingMutable : Array Lean.Elab.Term.Do.Var → Lean.Elab.Term.Do.ToCodeBlock.M Unit
-- Init.Data.Nat.Bitwise.Lemmas
Nat.instAssociativeHOr : Std.Associative fun x1 x2 => x1 ||| x2
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_modify_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {k : α} {f : β → β}, (t.modify k f).getKey! k = if k ∈ t then k else default
-- Lean.ExtraModUses
/-- Records this module to be preserved as an import by `shake`.  -/
Lean.recordExtraRevUseOfCurrentModule : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadEnv m] →
      [Lean.MonadTrace m] → [Lean.MonadOptions m] → [Lean.MonadRef m] → [Lean.AddMessageContext m] → m Unit
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
range_cfcHom : ∀ (𝕜 : Type u_1) {A : Type u_2} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : Ring A] [inst_2 : StarRing A]
  [inst_3 : Algebra 𝕜 A] [inst_4 : TopologicalSpace A] [inst_5 : StarModule 𝕜 A]
  [inst_6 : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 A p] [inst_7 : IsTopologicalRing A]
  [inst_8 : ContinuousStar A] {a : A} (ha : p a), (cfcHom ha).range = StarAlgebra.elemental 𝕜 a
-- Mathlib.Data.Rat.Defs
Rat.add_divInt : ∀ (a b c : ℤ), Rat.divInt (a + b) c = Rat.divInt a c + Rat.divInt b c
-- Mathlib.Algebra.Order.Group.Indicator
Set.abs_indicator_symmDiff : ∀ {α : Type u_2} {M : Type u_3} [inst : AddCommGroup M] [inst_1 : Lattice M] (s t : Set α) (f : α → M) (x : α),
  |(symmDiff s t).indicator f x| = |s.indicator f x - t.indicator f x|
-- Mathlib.Analysis.CStarAlgebra.GelfandDuality
Ideal.toCharacterSpace_apply_eq_zero_of_mem : ∀ {A : Type u_1} [inst : NormedCommRing A] [inst_1 : NormedAlgebra ℂ A] [inst_2 : CompleteSpace A] (I : Ideal A)
  [inst_3 : I.IsMaximal] {a : A}, a ∈ I → I.toCharacterSpace a = 0
-- Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence
CategoryTheory.ShortComplex.FunctorEquivalence.counitIso_hom_app_app_τ₁ : ∀ (J : Type u_1) (C : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  (X : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) (X_1 : J),
  (((CategoryTheory.ShortComplex.FunctorEquivalence.counitIso J C).hom.app X).app X_1).τ₁ =
    CategoryTheory.CategoryStruct.id (X.obj X_1).X₁
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
Multipliable.sum : ∀ {α : Type u_4} {β : Type u_5} {M : Type u_6} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] [ContinuousMul M]
  (f : α ⊕ β → M), Multipliable (f ∘ Sum.inl) → Multipliable (f ∘ Sum.inr) → Multipliable f
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.coeff_toSubring : ∀ {σ : Type u_1} {R : Type u_2} [inst : Ring R] (p : MvPowerSeries σ R) (T : Subring R)
  (hp : ∀ (n : σ →₀ ℕ), (MvPowerSeries.coeff n) p ∈ T) {n : σ →₀ ℕ},
  ↑((MvPowerSeries.coeff n) (p.toSubring T hp)) = (MvPowerSeries.coeff n) p
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
/-- The prefunctor on refl quivers `OneTruncation₂` induced by a morphism
of `2`-truncated simplicial sets.  -/
SSet.OneTruncation₂.map : {S T : SSet.Truncated 2} → (S ⟶ T) → SSet.OneTruncation₂ S ⥤rq SSet.OneTruncation₂ T
-- Mathlib.Geometry.RingedSpace.Stalks
AlgebraicGeometry.PresheafedSpace.stalkMap.isIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C]
  {X Y : AlgebraicGeometry.PresheafedSpace C} (α : X ⟶ Y) [CategoryTheory.IsIso α] (x : ↑↑X),
  CategoryTheory.IsIso (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap α x)
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
hasSum_fintype : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] [inst_2 : Fintype β] (f : β → α)
  (L : optParam (SummationFilter β) (SummationFilter.unconditional β)) [L.LeAtTop], HasSum f (∑ b, f b) L
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.coeff_single_mul_apply : ∀ {R : Type u_1} {G : Type u_3} [inst : Semiring R] [inst_1 : Group G] (x : MonoidAlgebra R G) (r : R) (g h : G),
  (MonoidAlgebra.single g r * x).coeff h = r * x.coeff (g⁻¹ * h)
-- Batteries.Data.List.Scan
List.getElem_flatten_aux₁ : ∀ {α : Type u_1} (L : List (List α)),
  ∀ i < L.flatten.length, List.findIdx (fun x => decide (x > i)) (List.map List.length L).partialSums - 1 < L.length