mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.homologyπ_extendHomologyIso_inv : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {j : ι} {j' : ι'}
  (hj' : e.f j = j') [inst_3 : K.HasHomology j] [inst_4 : (K.extend e).HasHomology j'],
  CategoryTheory.CategoryStruct.comp (K.homologyπ j) (K.extendHomologyIso e hj').inv =
    CategoryTheory.CategoryStruct.comp (K.extendCyclesIso e hj').inv ((K.extend e).homologyπ j')
-- Mathlib.Tactic.Algebra.Lemmas
Mathlib.Tactic.Algebra.nat_rawCast_2 : ∀ {R : Type u_1} [sR : CommSemiring R] {n : ℕ} [inst : n.AtLeastTwo], n.rawCast = OfNat.ofNat n
-- Mathlib.Combinatorics.SetFamily.Compression.Down
Finset.nonMemberSubfamily_inter : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (𝒜 ℬ : Finset (Finset α)),
  Finset.nonMemberSubfamily a (𝒜 ∩ ℬ) = Finset.nonMemberSubfamily a 𝒜 ∩ Finset.nonMemberSubfamily a ℬ
-- Mathlib.CategoryTheory.Shift.Quotient
CategoryTheory.Quotient.lift.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (r : HomRel C) {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D)
  (H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂),
  CategoryTheory.Quotient.lift r F H =
    { obj := fun a => F.obj a.as, map := fun {X Y} hf => Quot.liftOn hf (fun f => F.map f) ⋯, map_id := ⋯,
      map_comp := ⋯ }
-- Mathlib.Algebra.Homology.ExactSequence
CategoryTheory.ComposableArrows.exact₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ComposableArrows C 1), S.Exact
-- Aesop.RuleSet.Member
Aesop.BaseRuleSetMember.unsafeForwardRule : Aesop.ForwardRule → Aesop.UnsafeRule → Aesop.BaseRuleSetMember
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.op_symm_apply_apply : ∀ {α : Type u_7} {β : Type u_8} [inst : Add α] [inst_1 : Mul α] [inst_2 : Add β] [inst_3 : Mul β] (f : αᵐᵒᵖ ≃+* βᵐᵒᵖ)
  (a : α), (RingEquiv.op.symm f) a = MulOpposite.unop (f (MulOpposite.op a))
-- Mathlib.CategoryTheory.SmallObject.Construction
/-- The canonical morphism `∐ (functorObjTgtFamily f πX) ⟶ functorObj f πX`.  -/
CategoryTheory.SmallObject.ρFunctorObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {I : Type w} →
      {A B : I → C} →
        (f : (i : I) → A i ⟶ B i) →
          {S X : C} →
            (πX : X ⟶ S) →
              [inst_1 :
                  CategoryTheory.Limits.HasColimitsOfShape
                    (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] →
                [inst_2 :
                    CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX)
                      (CategoryTheory.SmallObject.functorObjLeft f πX)] →
                  ∐ CategoryTheory.SmallObject.functorObjTgtFamily f πX ⟶ CategoryTheory.SmallObject.functorObj f πX
-- Mathlib.Tactic.ProdAssoc
Lean.Expr.ProdTree.brecOn.eq : ∀ {motive : Lean.Expr.ProdTree → Sort u} (t : Lean.Expr.ProdTree)
  (F_1 : (t : Lean.Expr.ProdTree) → Lean.Expr.ProdTree.below t → motive t),
  Lean.Expr.ProdTree.brecOn t F_1 = F_1 t (Lean.Expr.ProdTree.brecOn.go t F_1).2
-- Aesop.Forward.State
/-- The pattern substitution came from the goal's target.  -/
Aesop.PatSubstSource.target : Aesop.PatSubstSource
-- Std.Tactic.BVDecide.Syntax
/-- The configuration options for `bv_decide`.
 -/
Lean.Elab.Tactic.BVDecide.BVDecideConfig : Type
-- Mathlib.Algebra.Lie.Nilpotent
LieEquiv.nilpotent_iff_equiv_nilpotent : ∀ {R : Type u} {L : Type v} {L' : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing L'] [inst_4 : LieAlgebra R L'] (e : L ≃ₗ⁅R⁆ L'), LieRing.IsNilpotent L ↔ LieRing.IsNilpotent L'
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.coe_intCast : ∀ {α : Type u} [inst : TopologicalSpace α] {R : Type u_1} [inst_1 : SeminormedRing R] (n : ℤ), ⇑↑n = ↑n
-- Lean.Data.SMap
Lean.SMap.instInhabited : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Inhabited (Lean.SMap α β)
-- Mathlib.MeasureTheory.Function.UniformIntegrable
MeasureTheory.MemLp.eLpNormEssSup_indicator_norm_ge_eq_zero : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {f : α → β},
  MeasureTheory.MemLp f ⊤ μ →
    MeasureTheory.StronglyMeasurable f → ∃ M, MeasureTheory.eLpNormEssSup ({x | M ≤ ↑‖f x‖₊}.indicator f) μ = 0
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.mk.sizeOf_spec : ∀ {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : SizeOf X] (toSetoid : Setoid X)
  (isOpen_setOfPred_rel : ∀ (x : X), IsOpen (Set.ofPred (toSetoid x))),
  sizeOf { toSetoid := toSetoid, isOpen_setOfPred_rel := isOpen_setOfPred_rel } = 1 + sizeOf toSetoid
-- Mathlib.GroupTheory.GroupAction.IterateAct
IterateAddAct.mk.inj : ∀ {α : Type u_1} {f : α → α} {val val_1 : ℕ}, { val := val } = { val := val_1 } → val = val_1
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec64_abs : ∀ (a : ISize) (h : System.Platform.numBits = 64), a.abs.toBitVec64 h = (a.toBitVec64 h).abs
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.mem_set_normalizer_iff' : ∀ {G : Type u_1} [inst : AddGroup G] {S : Set G} {g : G},
  g ∈ AddSubgroup.normalizer S ↔ ∀ (h : G), h + g ∈ S ↔ g + h ∈ S
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_maxKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t ≠ ∅ → t.getKey! t.maxKey! = t.maxKey!
-- Mathlib.Order.Hom.Basic
StrictMono.orderIsoOfRightInverse_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : Preorder β] (f : α → β) (h_mono : StrictMono f)
  (g : β → α) (hg : Function.RightInverse g f), ⇑(StrictMono.orderIsoOfRightInverse f h_mono g hg) = f
-- Init.Data.Float.Float
/-- Multiplies 64-bit floating-point numbers according to IEEE 754. Typically used via the `*` operator.

This function has a logical model in terms of `Float.Model`. It is compiled to the C multiplication operator.
 -/
Float.mul : Float → Float → Float
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instAddCommMonoid : {α : Type u_1} → [AddCommMonoid α] → AddCommMonoid (Lex α)
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.swap_inj : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {x y : Monoid.Coprod M N},
  (Monoid.Coprod.swap M N) x = (Monoid.Coprod.swap M N) y ↔ x = y
-- Mathlib.NumberTheory.SumFourSquares
/-- **Euler's four-square identity**, a version for natural numbers.  -/
Nat.euler_four_squares : ∀ (a b c d x y z w : ℕ),
  (↑a * ↑x - ↑b * ↑y - ↑c * ↑z - ↑d * ↑w).natAbs ^ 2 + (↑a * ↑y + ↑b * ↑x + ↑c * ↑w - ↑d * ↑z).natAbs ^ 2 +
        (↑a * ↑z - ↑b * ↑w + ↑c * ↑x + ↑d * ↑y).natAbs ^ 2 +
      (↑a * ↑w + ↑b * ↑z - ↑c * ↑y + ↑d * ↑x).natAbs ^ 2 =
    (a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2) * (x ^ 2 + y ^ 2 + z ^ 2 + w ^ 2)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
CliffordAlgebra.foldr'.congr_simp : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticForm R M) (f f_1 : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N)
  (e_f : f = f_1)
  (hf : ∀ (m : M) (x : CliffordAlgebra Q) (fx : N), (f m) ((CliffordAlgebra.ι Q) m * x, (f m) (x, fx)) = Q m • fx)
  (n n_1 : N), n = n_1 → CliffordAlgebra.foldr' Q f hf n = CliffordAlgebra.foldr' Q f_1 ⋯ n_1
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Hom.of.sizeOf_spec : ∀ {B : Type u} [inst : Quiver B] [inst_1 : SizeOf B] {a b : B} (f : a ⟶ b),
  sizeOf (CategoryTheory.FreeBicategory.Hom.of f) = 1 + sizeOf a + sizeOf b + sizeOf f
-- Mathlib.Data.Num.ZNum
PosNum.sub'.eq_3 : ∀ (a b : PosNum), a.bit0.sub' b.bit0 = (a.sub' b).bit0
-- Mathlib.Order.Hom.WithTopBot
/-- Adjoins a `⊤` and `⊥` to the domain of a `LatticeHom`.  -/
LatticeHom.withTopWithBot' : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Lattice α] →
      [inst_1 : Lattice β] → [inst_2 : BoundedOrder β] → LatticeHom α β → BoundedLatticeHom (WithTop (WithBot α)) β
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
/-- This is [grinberg_clifford_2016] Theorem 14  -/
CliffordAlgebra.contractRight_comm : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (d d' : Module.Dual R M) (x : CliffordAlgebra Q),
  (CliffordAlgebra.contractRight ((CliffordAlgebra.contractRight x) d)) d' =
    -(CliffordAlgebra.contractRight ((CliffordAlgebra.contractRight x) d')) d
-- Mathlib.LinearAlgebra.Matrix.Nondegenerate
/-- If `M` is nondegenerate and `w * M * v = 0` for all `v`, then `w = 0`.  -/
Matrix.Nondegenerate.eq_zero_of_ortho' : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : CommSemiring R] {M : Matrix m n R} [inst_1 : Fintype m]
  [inst_2 : Fintype n], M.Nondegenerate → ∀ {w : n → R}, (∀ (v : m → R), v ⬝ᵥ M.mulVec w = 0) → w = 0
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey?_erase_self : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → ∀ {k : α}, (m.erase k).getKey? k = none
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.prod_sum_index : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] {ι₁ : Type u₁} [inst_1 : DecidableEq ι₁]
  {β₁ : ι₁ → Type v₁} [inst_2 : (i₁ : ι₁) → Zero (β₁ i₁)] [inst_3 : (i : ι₁) → (x : β₁ i) → Decidable (x ≠ 0)]
  [inst_4 : (i : ι) → AddCommMonoid (β i)] [inst_5 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_6 : CommMonoid γ]
  {f : Π₀ (i₁ : ι₁), β₁ i₁} {g : (i₁ : ι₁) → β₁ i₁ → Π₀ (i : ι), β i} {h : (i : ι) → β i → γ},
  (∀ (i : ι), h i 0 = 1) →
    (∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ * h i b₂) → (f.sum g).prod h = f.prod fun i b => (g i b).prod h
-- Mathlib.CategoryTheory.Limits.Constructions.Filtered
CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetObj.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type w}
  [inst_1 : CategoryTheory.Limits.HasFiniteProducts C] (F F_1 : CategoryTheory.Functor (CategoryTheory.Discrete α) C),
  F = F_1 →
    CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetObj F =
      CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetObj F_1
-- Mathlib.Probability.IdentDistrib
ProbabilityTheory.IdentDistrib.neg : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → γ} {g : β → γ}
  [inst_3 : Neg γ] [MeasurableNeg γ],
  ProbabilityTheory.IdentDistrib f g μ ν → ProbabilityTheory.IdentDistrib (-f) (-g) μ ν
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
/-- Dividing out by a prime factor reduces the `padicValNat` by `1`.  -/
padicValNat.div : ∀ {p b : ℕ} [hp : Fact (Nat.Prime p)], p ∣ b → padicValNat p (b / p) = padicValNat p b - 1
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- See `AddAction.isBlock_subgroup'` for a version that works for the right action
of a group on itself.  -/
AddAction.isBlock_addSubgroup : ∀ {G : Type u_1} [inst : AddGroup G] {S : Type u_3} {H : Type u_4} [inst_1 : AddGroup H] [inst_2 : SetLike S H]
  [AddSubgroupClass S H] {s : S} [inst_4 : AddAction G H] [VAddAssocClass G H H], AddAction.IsBlock G ↑s
-- Mathlib.RepresentationTheory.Homological.TateCohomology.Basic
TateCohomology.exact₁ : ∀ {R G : Type u} [inst : CommRing R] [inst_1 : Group G] [inst_2 : Fintype G]
  {S : CategoryTheory.ShortComplex (Rep.{u, u, u} R G)} (hS : S.ShortExact) (n : ℤ),
  { X₁ := tateCohomology S.X₃ n, X₂ := tateCohomology S.X₁ (n + 1), X₃ := (tateCohomologyFunctor (n + 1)).obj S.X₂,
      f := TateCohomology.δ hS n, g := (tateCohomologyFunctor (n + 1)).map S.f, zero := ⋯ }.Exact
-- Mathlib.Geometry.Manifold.ContMDiffMFDeriv
equivTangentBundleProd_eq_tangentMap_prod_tangentMap : ∀ {𝕜 : 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'],
  ⇑(equivTangentBundleProd I M I' M') = fun p =>
    (tangentMap (I.prod I') I Prod.fst p, tangentMap (I.prod I') I' Prod.snd p)
-- Init.Data.Ord.Basic
/-- `Ord α` provides a computable total order on `α`, in terms of the
`compare : α → α → Ordering` function.

Typically instances will be transitive, reflexive, and antisymmetric,
but this is not enforced by the typeclass.

There is a derive handler, so appending `deriving Ord` to an inductive type or structure
will attempt to create an `Ord` instance.
 -/
Ord : Type u → Type u
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.instCoeTypeForall : {α : Type u} → Coe (Type v) (α → Type v)
-- Mathlib.Order.Bounds.Basic
IsGLB.prod : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α} {t : Set β} {a : α} {b : β},
  s.Nonempty → t.Nonempty → IsGLB s a → IsGLB t b → IsGLB (s ×ˢ t) (a, b)
-- Mathlib.Topology.Algebra.Monoid
/-- If multiplication on a monoid is continuous, then multiplication on the units of the monoid,
with respect to the induced topology, is continuous.

Inversion is also continuous, but we register this in a later file, `Topology.Algebra.Group`,
because the predicate `ContinuousInv` has not yet been defined.  -/
Units.instContinuousMul : ∀ {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : Monoid α] [ContinuousMul α], ContinuousMul αˣ
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Iic_sdiff_Ioc_self_of_le : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, a ≤ b → Set.Iic b \ Set.Ioc a b = Set.Iic a
-- Mathlib.Data.Part
Part.zero_def : ∀ {α : Type u_1} [inst : Zero α], 0 = Part.some 0
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.eq_prod_range_div' : ∀ {G : Type u_3} [inst : CommGroup G] (f : ℕ → G) (n : ℕ),
  f n = ∏ i ∈ Finset.range (n + 1), if i = 0 then f 0 else f i / f (i - 1)
-- Mathlib.Analysis.Distribution.Sobolev
TemperedDistribution.fourier_besselPotential_eq_smulLeftCLM_fourier_apply : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : FiniteDimensional ℝ E] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E]
  [inst_6 : InnerProductSpace ℂ F] (s : ℝ) (f : TemperedDistribution E F),
  FourierTransform.fourier ((TemperedDistribution.besselPotential E F s) f) =
    (TemperedDistribution.smulLeftCLM F fun x => ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (FourierTransform.fourier f)
-- Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
SimpleGraph.EdgeLabeling.get_comm : ∀ {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {C : G.EdgeLabeling K} (x y : V) (h : G.Adj y x),
  C.get y x h = C.get x y ⋯
-- Mathlib.Order.Concept
upperPolar_swap : ∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (t : Set β), upperPolar (Function.swap r) t = lowerPolar r t
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?_insertEntryIfNew : ∀ {α : Type u} {β : Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α} {v : β},
  Std.Internal.List.getValue? a (Std.Internal.List.insertEntryIfNew k v l) =
    if (k == a) = true ∧ Std.Internal.List.containsKey k l = false then some v else Std.Internal.List.getValue? a l
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- Restriction of an `AddSemigroup` hom to an `AddSubsemigroup` of the codomain.  -/
AddHom.codRestrict : {M : Type u_1} →
  {N : Type u_2} →
    {σ : Type u_4} →
      [inst : Add M] →
        [inst_1 : Add N] →
          [inst_2 : SetLike σ N] →
            [inst_3 : AddMemClass σ N] → (f : M →ₙ+ N) → (S : σ) → (∀ (x : M), f x ∈ S) → M →ₙ+ ↥S
-- Mathlib.Util.AtomM
/-- Run a computation in the `AtomM` monad.  -/
Mathlib.Tactic.AtomM.run : {α : Type} →
  Lean.Meta.TransparencyMode →
    Mathlib.Tactic.AtomM α →
      (optParam (Lean.Expr → Lean.MetaM Lean.Meta.Simp.Result) fun e => pure { expr := e }) → Lean.MetaM α
-- Mathlib.Order.CompleteLattice.Lemmas
/-- This is a weaker version of `sSup_inf_eq`  -/
iSup_inf_le_sSup_inf : ∀ {α : Type u_1} [inst : CompleteLattice α] {a : α} {s : Set α}, ⨆ b ∈ s, b ⊓ a ≤ sSup s ⊓ a
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.mk'_eq_of_same : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N) {a b : M} {d : ↥S}, f.mk' a d = f.mk' b d ↔ ∃ c, ↑c + a = ↑c + b
-- Mathlib.Algebra.Group.WithOne.Map
WithZero.map_coe : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (a : α), WithZero.map f ↑a = ↑(f a)
-- Mathlib.CategoryTheory.Shift.SingleFunctors
/-- The type of families of functors `A → C ⥤ D` which are compatible with
the shift by `A` on the category `D`.  -/
CategoryTheory.SingleFunctors : (C : Type u_1) →
  (D : Type u_2) →
    [CategoryTheory.Category.{v_1, u_1} C] →
      [inst : CategoryTheory.Category.{v_2, u_2} D] →
        (A : Type u_5) →
          [inst_1 : AddMonoid A] → [CategoryTheory.HasShift D A] → Type (max (max (max (max u_1 u_2) u_5) v_1) v_2)
-- Lean.Level
Lean.levelZero : Lean.Level
-- Init.Data.Int.LemmasAux
_private.Init.Data.Int.LemmasAux.0.Int.toNat.match_1.eq_2 : ∀ (motive : ℤ → Sort u_1) (a : ℕ) (h_1 : (n : ℕ) → motive (Int.ofNat n)) (h_2 : (a : ℕ) → motive (Int.negSucc a)),
  (match Int.negSucc a with
    | Int.ofNat n => h_1 n
    | Int.negSucc a => h_2 a) =
    h_2 a
-- Mathlib.LinearAlgebra.Quotient.Pi
Submodule.piQuotientLift_single : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] {Ms : ι → Type u_3} [inst_1 : (i : ι) → AddCommGroup (Ms i)]
  [inst_2 : (i : ι) → Module R (Ms i)] {N : Type u_4} [inst_3 : AddCommGroup N] [inst_4 : Module R N]
  [inst_5 : Fintype ι] [inst_6 : DecidableEq ι] (p : (i : ι) → Submodule R (Ms i)) (q : Submodule R N)
  (f : (i : ι) → Ms i →ₗ[R] N) (hf : ∀ (i : ι), p i ≤ Submodule.comap (f i) q) (i : ι) (x : Ms i ⧸ p i),
  (Submodule.piQuotientLift p q f hf) (Pi.single i x) = ((p i).mapQ q (f i) ⋯) x
-- Std.Async.IO
/-- Interface for asynchronous writing operations.
 -/
Std.Async.IO.AsyncWrite : Type → Type → Type
-- Mathlib.Tactic.Ring.Common
/-- A sum of monomials.  -/
Mathlib.Tactic.Ring.Common.ExBase.sum : {u : Lean.Level} →
  {α : Q(Type u)} →
    {BaseType : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} →
        {e : Q(«$α»)} → Mathlib.Tactic.Ring.Common.ExSum BaseType sα e → Mathlib.Tactic.Ring.Common.ExBase BaseType sα e
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKey_modify : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [Inhabited α] {k k' : α} {f : β → β} {h : k' ∈ Std.ExtDHashMap.Const.modify m k f},
  (Std.ExtDHashMap.Const.modify m k f).getKey k' h = if (k == k') = true then k else m.getKey k' ⋯
-- Mathlib.CategoryTheory.Limits.ExactFunctor
CategoryTheory.instIsClosedUnderIsomorphismsFunctorExactFunctor : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D],
  (CategoryTheory.exactFunctor C D).IsClosedUnderIsomorphisms
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
/-- An odd function is interval integrable (with respect to the volume measure) on every interval
iff it is interval integrable (with respect to the volume measure) on every interval of the form
`0..x`, for positive `x`.  -/
intervalIntegrable_of_odd : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] {f : ℝ → E},
  (∀ (x : ℝ), -f x = f (-x)) →
    (∀ (x : ℝ), 0 < x → IntervalIntegrable f MeasureTheory.volume 0 x) →
      ∀ {a b : ℝ},
        autoParam (‖f (min 0 a)‖ₑ ≠ ⊤) intervalIntegrable_of_odd._auto_1 →
          autoParam (‖f (min 0 b)‖ₑ ≠ ⊤) intervalIntegrable_of_odd._auto_3 →
            IntervalIntegrable f MeasureTheory.volume a b
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- An oriented angle is `π` if and only if the angle with the order of the points reversed is
`π`.  -/
EuclideanGeometry.oangle_eq_pi_iff_oangle_rev_eq_pi : ∀ {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}, EuclideanGeometry.oangle p₁ p₂ p₃ = ↑Real.pi ↔ EuclideanGeometry.oangle p₃ p₂ p₁ = ↑Real.pi
-- Batteries.Data.List.Lemmas
_private.Batteries.Data.List.Lemmas.0.List.isPrefixOf.match_1.splitter : {α : Type u_1} →
  (motive : List α → List α → Sort u_2) →
    (x x_1 : List α) →
      ((x : List α) → motive [] x) →
        ((x : List α) → (x = [] → False) → motive x []) →
          ((a : α) → (as : List α) → (b : α) → (bs : List α) → motive (a :: as) (b :: bs)) → motive x x_1
-- Mathlib.NumberTheory.Ostrowski
Rat.AbsoluteValue.padic_eq_padicNorm : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] (r : ℚ), (Rat.AbsoluteValue.padic p) r = ↑(padicNorm p r)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- The pointwise subtraction of finsets `s - t` is defined as `{x - y | x ∈ s, y ∈ t}`
in scope `Pointwise`.  -/
Finset.sub : {α : Type u_2} → [DecidableEq α] → [Sub α] → Sub (Finset α)
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instOne : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] → [Nonempty ι] → [(i : ι) → One (G i)] → One (DirectLimit G f)
-- Mathlib.Logic.IsEmpty.Basic
Relator.LeftTotal.eq_1 : ∀ {α : Sort u₁} {β : Sort u₂} (R : α → β → Prop), Relator.LeftTotal R = ∀ (a : α), ∃ b, R a b
-- Mathlib.Order.Heyting.Hom
/-- The proposition that a co-Heyting homomorphism preserves the difference operation.  -/
CoheytingHomClass.map_sdiff : ∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} {inst : CoheytingAlgebra α} {inst_1 : CoheytingAlgebra β}
  {inst_2 : FunLike F α β} [self : CoheytingHomClass F α β] (f : F) (a b : α), f (a \ b) = f a \ f b
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Fintype.prod_subset : ∀ {M : Type u_4} {ι : Type u_7} [inst : Fintype ι] [inst_1 : CommMonoid M] {s : Finset ι} {f : ι → M},
  (∀ (i : ι), f i ≠ 1 → i ∈ s) → ∏ i ∈ s, f i = ∏ i, f i
-- Mathlib.Algebra.DualNumber
/-- When applied to `inl`, `DualNumber.lift` applies the map `f : A →ₐ[R] B`.  -/
DualNumber.lift_apply_inl : ∀ {R : Type u_1} {B : Type u_3} {A : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (fe : { _fe // _fe.2 * _fe.2 = 0 ∧ ∀ (a : A), Commute _fe.2 (_fe.1 a) })
  (a : A), (DualNumber.lift fe) (TrivSqZeroExt.inl a) = (↑fe).1 a
-- Mathlib.Analysis.ConstantSpeed
HasUnitSpeedOn.Icc_Icc : ∀ {E : Type u_2} [inst : PseudoEMetricSpace E] {f : ℝ → E} {x y z : ℝ},
  HasUnitSpeedOn f (Set.Icc x y) → HasUnitSpeedOn f (Set.Icc y z) → HasUnitSpeedOn f (Set.Icc x z)
-- Mathlib.Topology.Sets.Compacts
/-- See Note [custom simps projection].  -/
TopologicalSpace.Compacts.Simps.coe : {α : Type u_1} → [inst : TopologicalSpace α] → TopologicalSpace.Compacts α → Set α
-- Init.Internal.Order.Lemmas
_private.Init.Internal.Order.Lemmas.0.Array.forIn'.loop.match_3.splitter : {α : Type u_1} →
  (as : Array α) →
    (motive : (i : ℕ) → i ≤ as.size → Sort u_2) →
      (i : ℕ) →
        (h : i ≤ as.size) →
          ((x : 0 ≤ as.size) → motive 0 x) → ((i : ℕ) → (h : i + 1 ≤ as.size) → motive i.succ h) → motive i h
-- Init.Data.Nat.Bitwise.Lemmas
Nat.instLawfulCommIdentityHOrOfNat : Std.LawfulCommIdentity (fun x1 x2 => x1 ||| x2) 0