mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Sheaves.SheafCondition.Sites
/-- The restriction functor of a sheaf to an open subspace.  -/
TopologicalSpace.Opens.sheafRestrict : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : TopCat} →
      (U : TopologicalSpace.Opens ↑X) →
        CategoryTheory.Functor (CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) C)
          (CategoryTheory.Sheaf (Opens.grothendieckTopology ↥U) C)
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.smul_inter_subset : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] {s : Finset α} {t₁ t₂ : Finset β},
  s • (t₁ ∩ t₂) ⊆ s • t₁ ∩ s • t₂
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.subsingleton_iff_ker_eq_top : ∀ {R : Type u_6} {M : Type u_8} {M' : Type u_9} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (S : Submonoid R) (g : M →ₗ[R] M') [IsLocalizedModule S g],
  Subsingleton M' ↔ g.ker = ⊤
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.congr_linearEquiv_refl : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V],
  SpecialLinearGroup.congr_linearEquiv (LinearEquiv.refl R V) = MulEquiv.refl (SpecialLinearGroup R V)
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
/-- If `G.IsBipartiteWith s t` and `v ∈ s`, then the neighbor set of `v` is the set of vertices in
`t` adjacent to `v` in `G`.  -/
SimpleGraph.isBipartiteWith_neighborSet : ∀ {V : Type u_1} {v : V} {G : SimpleGraph V} {s t : Set V},
  G.IsBipartiteWith s t → v ∈ s → G.neighborSet v = {w | w ∈ t ∧ G.Adj v w}
-- Mathlib.Logic.Equiv.Prod
Equiv.uniqueSigma_apply : ∀ {α : Type u_10} {β : α → Type u_9} [inst : Unique α] (x : (a : α) × β a), (Equiv.uniqueSigma β) x = ⋯ ▸ x.snd
-- Mathlib.Data.Num.ZNum
_private.Mathlib.Data.Num.ZNum.0.Num.add.match_1.eq_2 : ∀ (motive : Num → Num → Sort u_1) (b : Num) (h_1 : (a : Num) → motive Num.zero a) (h_2 : (b : Num) → motive b Num.zero)
  (h_3 : (a b : PosNum) → motive (Num.pos a) (Num.pos b)),
  (b = Num.zero → False) →
    (match b, Num.zero with
      | Num.zero, a => h_1 a
      | b, Num.zero => h_2 b
      | Num.pos a, Num.pos b => h_3 a b) =
      h_2 b
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- Given two pairs of distinct points on the same line, such that the vectors between those
pairs of points are on the same ray (oriented in the same direction on that line), and a fifth
point, the angles at the fifth point between each of those two pairs of points have the same
sign.  -/
Collinear.oangle_sign_of_sameRay_vsub : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ p₄ : P} (p₅ : P),
  p₁ ≠ p₂ →
    p₃ ≠ p₄ →
      Collinear ℝ {p₁, p₂, p₃, p₄} →
        SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃) →
          (EuclideanGeometry.oangle p₁ p₅ p₂).sign = (EuclideanGeometry.oangle p₃ p₅ p₄).sign
-- Lean.Expr
Lean.eagerReflBoolFalse : Lean.Expr
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.balanceR_eq_balanceR! : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β} {hlb : l.Balanced}
  {hrb : r.Balanced} {hlr : Std.DTreeMap.Internal.Impl.BalanceLPrecond r.size l.size},
  Std.DTreeMap.Internal.Impl.balanceR k v l r hlb hrb hlr = Std.DTreeMap.Internal.Impl.balanceR! k v l r
-- Batteries.Data.UnionFind.Basic
_private.Batteries.Data.UnionFind.Basic.0.Batteries.UnionFind.findAux.match_1.eq_1 : ∀ (self : Batteries.UnionFind) (motive : Batteries.UnionFind.FindAux self.size → Sort u_1)
  (arr₁ : Array Batteries.UFNode) (root : Fin self.size) (H : arr₁.size = self.size)
  (h_1 :
    (arr₁ : Array Batteries.UFNode) →
      (root : Fin self.size) → (H : arr₁.size = self.size) → motive { s := arr₁, root := root, size_eq := H }),
  (match { s := arr₁, root := root, size_eq := H } with
    | { s := arr₁, root := root, size_eq := H } => h_1 arr₁ root H) =
    h_1 arr₁ root H
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- The "opcycles" of a short complex, given by the `Q` field of a chosen right homology data.
This is the dual notion to cycles.  -/
CategoryTheory.ShortComplex.opcycles : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → (S : CategoryTheory.ShortComplex C) → [S.HasRightHomology] → C
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Submodule
PresheafOfModules.Submodule.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M : PresheafOfModules R} (obj : (X : Cᵒᵖ) → Submodule ↑(R.obj X) ↑(M.obj X))
  (map : ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), obj X ≤ Submodule.comap (M.restrictₛₗ f) (obj Y))
  (obj_1 : (X : Cᵒᵖ) → Submodule ↑(R.obj X) ↑(M.obj X))
  (map_1 : ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), obj_1 X ≤ Submodule.comap (M.restrictₛₗ f) (obj_1 Y)),
  ({ obj := obj, map := map } = { obj := obj_1, map := map_1 }) = (obj = obj_1)
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.biInf_mem : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} [inst : CompleteLattice β]
  {f : Set α → β}, l.HasBasis p s → Monotone f → ⨅ t ∈ l, f t = ⨅ i, ⨅ (_ : p i), f (s i)
-- Mathlib.Analysis.RCLike.Lemmas
RCLike.rank_le_two : ∀ (K : Type u_1) [inst : RCLike K], Module.rank ℝ K ≤ 2
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
linearIndependent_of_subsingleton : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [Subsingleton R], LinearIndependent R v
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.mk : (ω₁ ω₂ : ℂ) → LinearIndependent ℝ ![ω₁, ω₂] → PeriodPair
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
Ideal.absNorm_ne_zero_of_nonZeroDivisors : ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : IsDedekindDomain S] [inst_2 : Module.Free ℤ S] [Module.Finite ℤ S]
  (I : ↥(nonZeroDivisors (Ideal S))), Ideal.absNorm ↑I ≠ 0
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.measure_toMeasurable_add_inter_right : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {s t : Set α},
  MeasurableSet s → (μ + ν) t ≠ ⊤ → ν (MeasureTheory.toMeasurable (μ + ν) t ∩ s) = ν (t ∩ s)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKeyD_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {fallback : α}, t.minKeyD fallback ∈ t
-- Mathlib.Data.Sum.Order
Sum.instPreorderSum : {α : Type u_1} → {β : Type u_2} → [Preorder α] → [Preorder β] → Preorder (α ⊕ β)
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.coe_rpow_of_ne_zero : ∀ {x : NNReal}, x ≠ 0 → ∀ (y : ℝ), ↑(x ^ y) = ↑x ^ y
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
/-- One direction of `Real.log_le_iff_le_exp` without positivity assumption.  -/
Real.le_exp_of_log_le : ∀ {x y : ℝ}, Real.log x ≤ y → x ≤ Real.exp y
-- Batteries.Data.Array.Basic
_private.Batteries.Data.Array.Basic.0.Array.scanlM_eq_scanlMFast : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [inst : Monad m] {f : β → α → m β} {init : β} {as : Array α}
  {h_size : Array.SizeFitsUSize✝ as} {start stop : ℕ},
  Array.scanlM f init as start stop = Array.scanlMFast✝ f init as start stop
-- Init.Data.Array.Basic
/-- Appends the contents of array of arrays into a single array. The resulting array contains the same
elements as the nested arrays in the same order.

Examples:
 * `#[#[5], #[4], #[3, 2]].flatten = #[5, 4, 3, 2]`
 * `#[#[0, 1], #[], #[2], #[1, 0, 1]].flatten = #[0, 1, 2, 1, 0, 1]`
 * `(#[] : Array Nat).flatten = #[]`
 -/
Array.flatten : {α : Type u} → Array (Array α) → Array α
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.Truncated.tensor_map_apply_fst : ∀ {n : ℕ} {X Y : SSet.Truncated n} {d e : (SimplexCategory.Truncated n)ᵒᵖ} (f : d ⟶ e)
  (x : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).obj d),
  ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.tensorHom (X.map f) (Y.map f))) x).1 =
    (CategoryTheory.ConcreteCategory.hom (X.map f)) x.1
-- Lean.Parser.Command
Lean.Parser.Command.computedFields.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Homology.DerivedCategory.KInjective
CochainComplex.IsKInjective.quasiIso_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {K L : CochainComplex C ℤ}
  [K.IsKInjective] [L.IsKInjective] (f : K ⟶ L),
  QuasiIso f ↔ HomologicalComplex.homotopyEquivalences C (ComplexShape.up ℤ) f
-- Lean.Server.CodeActions.Basic
/-- Name of CodeActionProvider that produced this request.  -/
Lean.Server.CodeActionResolveData.providerName : Lean.Server.CodeActionResolveData → Lean.Name
-- Init.Data.BitVec.Lemmas
BitVec.instIdempotentOpHAnd : ∀ {n : ℕ}, Std.IdempotentOp fun x1 x2 => x1 &&& x2
-- Init.Data.SInt.Lemmas
ISize.neg_ofNat : ∀ {n : ℕ}, -ISize.ofNat n = ISize.ofInt (-↑n)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.combine.go.eq_2 : ∀ (fuel_2 : ℕ) (k₁ k₂ : ℤ),
  Lean.Grind.CommRing.Poly.combine.go fuel_2.succ (Lean.Grind.CommRing.Poly.num k₁) (Lean.Grind.CommRing.Poly.num k₂) =
    Lean.Grind.CommRing.Poly.num (k₁ + k₂)
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
_private.Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree.0.WeierstrassCurve.expDegree : ℕ → ℕ
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
CategoryTheory.Functor.CoconeTypes.ι_naturality : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w₀)} (self : F.CoconeTypes)
  {j j' : J} (f : j ⟶ j'), self.ι j' ∘ ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) = self.ι j
-- Mathlib.Data.Finset.Basic
Finset.erase_ssubset_insert : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α) (a : α), s.erase a ⊂ insert a s
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.map_map : ∀ {R : Type u_2} {M : Type u_4} {N : Type u_5} {O : Type u_6} [inst : Semiring R] [inst_1 : PartialOrder R]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : AddCommMonoid O] [inst_5 : Module R M]
  [inst_6 : Module R N] [inst_7 : Module R O] (g : N →ₗ[R] O) (f : M →ₗ[R] N) (C : ConvexCone R M),
  ConvexCone.map g (ConvexCone.map f C) = ConvexCone.map (g ∘ₗ f) C
-- Lean.Elab.Do.Basic
/-- Given a continuation `dec`, returns a continuation derived from `dec` with result type `PUnit`.
If `dec` already has result type `PUnit`, simply returns `dec`. Otherwise, an error is logged and a
new continuation is returned that calls `dec` with `sorry` as a result.
 -/
Lean.Elab.Do.DoElemCont.ensureUnit : Lean.Elab.Do.DoElemCont → Lean.Elab.Do.DoElabM Lean.Elab.Do.DoElemCont
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Functor.map_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : C} (f : X ⟶ Y) [inst_2 : CategoryTheory.IsIso f],
  F.map (CategoryTheory.inv f) = CategoryTheory.inv (F.map f)
-- Init.Dynamic
_private.Init.Dynamic.0.Dynamic.mkImpl : {α : Type u_1} → [TypeName α] → α → Dynamic
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.Clause.not_tautology : ∀ {α : outParam (Type u)} {β : Type v} [self : Std.Tactic.BVDecide.LRAT.Internal.Clause α β] (c : β)
  (l : Std.Sat.Literal α),
  l ∉ Std.Tactic.BVDecide.LRAT.Internal.Clause.toList c ∨ l.negate ∉ Std.Tactic.BVDecide.LRAT.Internal.Clause.toList c
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.foldlM.match_1.eq_1 : ∀ {α : Type u_2} {β : α → Type u_1} {δ : Type u_4} (motive : δ → Std.DHashMap.Internal.AssocList α β → Sort u_3) (d : δ)
  (h_1 : (d : δ) → motive d Std.DHashMap.Internal.AssocList.nil)
  (h_2 :
    (d : δ) →
      (a : α) →
        (b : β a) →
          (es : Std.DHashMap.Internal.AssocList α β) → motive d (Std.DHashMap.Internal.AssocList.cons a b es)),
  (match d, Std.DHashMap.Internal.AssocList.nil with
    | d, Std.DHashMap.Internal.AssocList.nil => h_1 d
    | d, Std.DHashMap.Internal.AssocList.cons a b es => h_2 d a b es) =
    h_1 d
-- Mathlib.Order.CompleteBooleanAlgebra
Order.Frame.toDistribLattice.eq_1 : ∀ {α : Type u} [inst : Order.Frame α], Order.Frame.toDistribLattice = DistribLattice.ofInfSupLe ⋯
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.opEquiv_functor_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (x : (CategoryTheory.WithTerminal C)ᵒᵖ),
  (CategoryTheory.WithTerminal.opEquiv C).functor.obj x =
    match Opposite.unop x with
    | CategoryTheory.WithTerminal.of x => CategoryTheory.WithInitial.of (Opposite.op x)
    | CategoryTheory.WithTerminal.star => CategoryTheory.WithInitial.star
-- Mathlib.RingTheory.LocalRing.ResidueField.Ideal
/-- If `I = f⁻¹(J)`, then there is a canonical embedding `κ(I) ↪ κ(J)`.  -/
Ideal.ResidueField.map : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        (I : Ideal R) →
          [inst_2 : I.IsPrime] →
            (J : Ideal S) →
              [inst_3 : J.IsPrime] → (f : R →+* S) → I = Ideal.comap f J → I.ResidueField →+* J.ResidueField
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.intervalIntegral_tendsto_integral_Iic : ∀ {ι : Type u_1} {E : Type u_2} {μ : MeasureTheory.Measure ℝ} {l : Filter ι} [l.IsCountablyGenerated]
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a : ι → ℝ} {f : ℝ → E} (b : ℝ),
  MeasureTheory.IntegrableOn f (Set.Iic b) μ →
    Filter.Tendsto a l Filter.atBot →
      Filter.Tendsto (fun i => ∫ (x : ℝ) in a i..b, f x ∂μ) l (nhds (∫ (x : ℝ) in Set.Iic b, f x ∂μ))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey_insertIfNew_le_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {v : β k}, (compare ((Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl.minKey ⋯) k).isLE = true
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ContinuousHom.monotone : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β]
  (f : α →𝒄 β), Monotone ⇑f
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.PublishDiagnosticsParams.version? : Lean.Lsp.PublishDiagnosticsParams → Option ℤ
-- Mathlib.Topology.Sets.Compacts
/-- The product of two `TopologicalSpace.PositiveCompacts`, as a `TopologicalSpace.PositiveCompacts`
in the product space.  -/
TopologicalSpace.PositiveCompacts.instSProdProd : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        SProd (TopologicalSpace.PositiveCompacts α) (TopologicalSpace.PositiveCompacts β)
          (TopologicalSpace.PositiveCompacts (α × β))
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- The normal closure of `s` is the smallest normal additive subgroup containing`s`.
 -/
AddSubgroup.normalClosure_le_normal : ∀ {G : Type u_1} [inst : AddGroup G] {s : Set G} {N : AddSubgroup G} [N.Normal],
  s ⊆ ↑N → AddSubgroup.normalClosure s ≤ N
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.coe_type_toSubfield : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L),
  ↥S.toSubfield = ↥S
-- Mathlib.Order.Filter.Map
Filter.join_pure : ∀ {α : Type u_1} (f : Filter α), (pure f).join = f
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Zipper.brecOn.go : {α : Type u} →
  {β : α → Type v} →
    {motive : Std.DTreeMap.Internal.Zipper α β → Sort u_1} →
      (t : Std.DTreeMap.Internal.Zipper α β) →
        ((t : Std.DTreeMap.Internal.Zipper α β) → Std.DTreeMap.Internal.Zipper.below t → motive t) →
          motive t ×' Std.DTreeMap.Internal.Zipper.below t
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.presieve₀_pushforward : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (E : CategoryTheory.PreZeroHypercover X),
  (CategoryTheory.PreZeroHypercover.pushforward f E).presieve₀ = CategoryTheory.Presieve.pushforward f E.presieve₀
-- Mathlib.Order.DirSupClosed
/-- **Alias** of the forward direction of `dirSupClosed_compl`. -/
DirSupInacc.of_compl : ∀ {α : Type u_1} {s : Set α} [inst : Preorder α], DirSupClosed sᶜ → DirSupInacc s
-- Mathlib.Algebra.Field.Periodic
Function.Antiperiodic.add_nat_mul_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [inst : NonAssocSemiring α] [inst_1 : Ring β],
  Function.Antiperiodic f c → ∀ (n : ℕ), f (x + ↑n * c) = (-1) ^ n * f x
-- Mathlib.Algebra.Group.Hom.Basic
AddMonoidHom.coe_of_map_add_neg : ∀ {G : Type u_5} [inst : AddGroup G] {H : Type u_8} [inst_1 : AddGroup H] (f : G → H)
  (map_sub : ∀ (a b : G), f (a + -b) = f a + -f b), ⇑(AddMonoidHom.ofMapAddNeg f map_sub) = f
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
/-- Typeclass for strict reverse monotonicity of multiplication on the right,
namely `a₁ * b < a₂ * b → a₁ < a₂`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`IsOrderedMonoid`.  -/
MulRightReflectLT : (M : Type u_1) → [Mul M] → [LT M] → Prop
-- Mathlib.LinearAlgebra.Dimension.LinearMap
LinearMap.rank.eq_1 : ∀ {K : Type u} {V : Type v} {V' : Type v'} [inst : Semiring K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [inst_3 : AddCommMonoid V'] [inst_4 : Module K V'] (f : V →ₗ[K] V'), f.rank = Module.rank K ↥f.range
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.nil.sizeOf_spec : ∀ {V : Type u} {G : SimpleGraph V} [inst : SizeOf V] {u : V}, sizeOf SimpleGraph.Walk.nil = 1 + sizeOf u
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.re_star : ∀ (z : Complex.UnitDisc), (star z).re = z.re
-- Mathlib.Data.EReal.Basic
EReal.preimage_coe_Iio_top : Real.toEReal ⁻¹' Set.Iio ⊤ = Set.univ
-- Mathlib.Topology.OpenPartialHomeomorph.Continuity
OpenPartialHomeomorph.map_nhdsWithin_preimage_eq : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {x : X},
  x ∈ e.source → ∀ (s : Set Y), Filter.map (↑e) (nhdsWithin x (↑e ⁻¹' s)) = nhdsWithin (↑e x) s
-- Init.Data.ByteArray.Lemmas
ByteArray.data_set : ∀ {as : ByteArray} {i : ℕ} {h : i < as.size} {a : UInt8}, (as.set i a h).data = as.data.set i a ⋯
-- Init.Data.BitVec.Folds
BitVec.iunfoldr_getLsbD : ∀ {w : ℕ} {α : Type u_1} {f : Fin w → α → α × Bool} (state : ℕ → α) (i : Fin w),
  (∀ (i : Fin w), (f i (state ↑i)).1 = state (↑i + 1)) → (BitVec.iunfoldr f (state 0)).2.getLsbD ↑i = (f i (state ↑i)).2
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- **Alias** of `MeasureTheory.VectorMeasure.of_add_of_sdiff`. -/
MeasureTheory.VectorMeasure.of_add_of_diff : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  {v : MeasureTheory.VectorMeasure α M} [T2Space M] {A B : Set α},
  MeasurableSet A → MeasurableSet B → A ⊆ B → v A + v (B \ A) = v B
-- Mathlib.Logic.IsEmpty.Basic
Relator.RightTotal.eq_1 : ∀ {α : Sort u₁} {β : Sort u₂} (R : α → β → Prop), Relator.RightTotal R = ∀ (b : β), ∃ a, R a b
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Legacy.mapAux.eq_def : ∀ (f : Char → Char) (i : String.Pos.Raw) (s : String),
  String.Legacy.mapAux f i s =
    if h : String.Pos.Raw.atEnd s i = true then s
    else
      have c := f (String.Pos.Raw.get s i);
      have this := ⋯;
      have s := String.Pos.Raw.set s i c;
      String.Legacy.mapAux f (String.Pos.Raw.next s i) s
-- Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
SSet.modelCategoryQuillen.cofibration_of_mono : ∀ {X Y : SSet} (f : X ⟶ Y) [CategoryTheory.Mono f], HomotopicalAlgebra.Cofibration f
-- Mathlib.GroupTheory.Sylow
Sylow.coe_ofCard : ∀ {G : Type u_1} [inst : Group G] [inst_1 : Finite G] {p : ℕ} [inst_2 : Fact (Nat.Prime p)] (H : Subgroup G)
  (card_eq : Nat.card ↥H = p ^ (Nat.card G).factorization p), ↑(Sylow.ofCard H card_eq) = H
-- Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
/-- Integration by parts of Schwartz functions for the 1-dimensional derivative.

Version for multiplication of scalar-valued Schwartz functions.  -/
SchwartzMap.integral_mul_deriv_eq_neg_deriv_mul : ∀ {𝕜 : Type u_2} [inst : NormedRing 𝕜] [inst_1 : NormedSpace ℝ 𝕜] [IsScalarTower ℝ 𝕜 𝕜] [SMulCommClass ℝ 𝕜 𝕜]
  (f g : SchwartzMap ℝ 𝕜), ∫ (x : ℝ), f x * deriv (⇑g) x = -∫ (x : ℝ), deriv (⇑f) x * g x
-- Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
/-- The two-sided ideal of compactly supported functions.  -/
BoundedContinuousFunction.«termC_cb(_,_)» : Lean.ParserDescr
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙ_sub : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommRing R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalRing R] [inst_5 : ContinuousStar R] [inst_6 : TopologicalSpace A]
  [inst_7 : NonUnitalRing A] [inst_8 : StarRing A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [inst_12 : NonUnitalContinuousFunctionalCalculus R A p] (f g : R → R) (a : A),
  autoParam (ContinuousOn f (quasispectrum R a)) _auto_660✝ →
    autoParam (f 0 = 0) _auto_662✝ →
      autoParam (ContinuousOn g (quasispectrum R a)) _auto_664✝ →
        autoParam (g 0 = 0) _auto_666✝ → cfcₙ (fun x => f x - g x) a = cfcₙ f a - cfcₙ g a
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.mem_of_mem_insertMany_list : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {l : List α} {k : α}, l.contains k = false → k ∈ m.insertMany l → k ∈ m
-- Mathlib.Tactic.NormNum.BigOperators
Mathlib.Meta.Multiset.ProveZeroOrConsResult.zero.sizeOf_spec : ∀ {u : Lean.Level} {α : Q(Type u)} {s : Q(Multiset «$α»)} (pf : Q(«$s» = 0)),
  sizeOf (Mathlib.Meta.Multiset.ProveZeroOrConsResult.zero pf) = 1 + sizeOf pf
-- Mathlib.LinearAlgebra.Projectivization.Basic
Projectivization.submodule_injective : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
  Function.Injective Projectivization.submodule
-- Mathlib.Analysis.Seminorm
coe_normSeminorm : ∀ (𝕜 : Type u_3) (E : Type u_7) [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E],
  ⇑(normSeminorm 𝕜 E) = norm
-- Mathlib.Algebra.Algebra.Unitization
StarAlgHom.mk.congr_simp : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Star A] [inst_4 : Semiring B] [inst_5 : Algebra R B] [inst_6 : Star B] (toAlgHom toAlgHom_1 : A →ₐ[R] B)
  (e_toAlgHom : toAlgHom = toAlgHom_1)
  (map_star' : ∀ (x : A), (↑↑toAlgHom.toRingHom).toFun (star x) = star ((↑↑toAlgHom.toRingHom).toFun x)),
  { toAlgHom := toAlgHom, map_star' := map_star' } = { toAlgHom := toAlgHom_1, map_star' := ⋯ }
-- Mathlib.Analysis.Normed.Ring.Ultra
IsUltrametricDist.norm_add_one_le_max_norm_one : ∀ {R : Type u_1} [inst : SeminormedRing R] [NormOneClass R] [IsUltrametricDist R] (x : R), ‖x + 1‖ ≤ max ‖x‖ 1
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.Hom.toImage_imageι : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.toImage f) (AlgebraicGeometry.Scheme.Hom.imageι f) =
    f
-- Mathlib.Topology.Separation.Regular
T4Space.t3Space : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T4Space X], T3Space X
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.hasKernel_iso_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y Z : C}
  (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.IsIso f] [CategoryTheory.Limits.HasKernel g],
  CategoryTheory.Limits.HasKernel (CategoryTheory.CategoryStruct.comp f g)