mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.DifferentialObject
/-- The functor from differential graded objects to homological complexes.
 -/
HomologicalComplex.dgoToHomologicalComplex : {β : Type u_1} →
  [inst : AddCommGroup β] →
    (b : β) →
      (V : Type u_2) →
        [inst_1 : CategoryTheory.Category.{v_1, u_2} V] →
          [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V] →
            CategoryTheory.Functor (CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V))
              (HomologicalComplex V (ComplexShape.up' b))
-- Init.Internal.Order.Basic
Lean.Order.ReverseImplicationOrder.instCompleteLattice : Lean.Order.CompleteLattice Lean.Order.ReverseImplicationOrder
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.iUnion_disjUnion : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.Prepartition I} (h : Disjoint π₁.iUnion π₂.iUnion),
  (π₁.disjUnion π₂ h).iUnion = π₁.iUnion ∪ π₂.iUnion
-- Mathlib.CategoryTheory.MorphismProperty.Descent
CategoryTheory.MorphismProperty.of_pullback_fst_of_descendsAlong : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P Q : CategoryTheory.MorphismProperty C} {X Y Z : C}
  {f : X ⟶ Z} {g : Y ⟶ Z} [P.DescendsAlong Q] [inst_2 : CategoryTheory.Limits.HasPullback f g],
  Q f → P (CategoryTheory.Limits.pullback.fst f g) → P g
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.State.mk.injEq : ∀ (stxTrav : Lean.Syntax.Traverser) (leadWord : String) (leadWordIdent isUngrouped mustBeGrouped : Bool)
  (stack : Array Std.Format) (stxTrav_1 : Lean.Syntax.Traverser) (leadWord_1 : String)
  (leadWordIdent_1 isUngrouped_1 mustBeGrouped_1 : Bool) (stack_1 : Array Std.Format),
  ({ stxTrav := stxTrav, leadWord := leadWord, leadWordIdent := leadWordIdent, isUngrouped := isUngrouped,
        mustBeGrouped := mustBeGrouped, stack := stack } =
      { stxTrav := stxTrav_1, leadWord := leadWord_1, leadWordIdent := leadWordIdent_1, isUngrouped := isUngrouped_1,
        mustBeGrouped := mustBeGrouped_1, stack := stack_1 }) =
    (stxTrav = stxTrav_1 ∧
      leadWord = leadWord_1 ∧
        leadWordIdent = leadWordIdent_1 ∧
          isUngrouped = isUngrouped_1 ∧ mustBeGrouped = mustBeGrouped_1 ∧ stack = stack_1)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
CFC.exp_log : ∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : NormedAlgebra ℝ A]
  [inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_4 : PartialOrder A] [StarOrderedRing A]
  [NonnegSpectrumClass ℝ A] (a : A),
  autoParam (IsStrictlyPositive a) CFC.exp_log._auto_1 → NormedSpace.exp (CFC.log a) = a
-- Mathlib.Computability.Primrec.Basic
Primrec.option_guard : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {p : α → β → Prop}
  [inst_2 : DecidableRel p],
  PrimrecRel p → ∀ {f : α → β}, Primrec f → Primrec fun a => Option.guard (fun b => decide (p a b)) (f a)
-- Init.Data.UInt.Lemmas
UInt16.size_dvd_usizeSize : UInt16.size ∣ USize.size
-- Mathlib.GroupTheory.Submonoid.Center
Subsemigroup.centerCongr_symm_apply_coe : ∀ {M : Type u_2} {N : Type u_1} [inst : Mul M] [inst_1 : Mul N] (e : M ≃* N) (s : ↥(Subsemigroup.center N)),
  ↑((Subsemigroup.centerCongr e).symm s) = e.symm ↑s
-- Mathlib.Algebra.Module.LocalizedModule.IsLocalization
instIsLocalizedModuleToLinearMapToAlgHomOfIsLocalizationAlgebraMapSubmonoid : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {A : Type u_2} {Aₛ : Type u_3} [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] [inst_3 : CommSemiring Aₛ] [inst_4 : Algebra A Aₛ] [inst_5 : Algebra R Aₛ]
  [inst_6 : IsScalarTower R A Aₛ] [IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ],
  IsLocalizedModule S (IsScalarTower.toAlgHom R A Aₛ).toLinearMap
-- Mathlib.Topology.Neighborhoods
TopologicalSpace.ext_iff_nhds : ∀ {X : Type u_2} {t t' : TopologicalSpace X}, t = t' ↔ ∀ (x : X), nhds x = nhds x
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.containsThenInsert_fst : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α],
  m.WF → ∀ {k : α}, (m.containsThenInsert k).1 = m.contains k
-- Mathlib.Algebra.Algebra.Spectrum.Basic
/-- **Alias** of the reverse direction of `spectrum.zero_notMem_iff`. -/
spectrum.zero_notMem : ∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] {a : A},
  IsUnit a → 0 ∉ spectrum R a
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.AttributeEntry.mk.sizeOf_spec : ∀ {γ : Type} [inst : SizeOf γ] (toOLeanEntry : Lean.KeyedDeclsAttribute.OLeanEntry) (isBuiltin : Bool) (value : γ),
  sizeOf { toOLeanEntry := toOLeanEntry, isBuiltin := isBuiltin, value := value } =
    1 + sizeOf toOLeanEntry + sizeOf isBuiltin + sizeOf value
-- Mathlib.Algebra.Homology.Embedding.TruncGE
/-- The isomorphism `(K.truncGE e).X i' ≅ K.opcycles i'` when `e.f i = i'`
and `e.BoundaryGE i` holds.  -/
HomologicalComplex.truncGEXIsoOpcycles : {ι : 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] →
              (K : HomologicalComplex C c') →
                (e : c.Embedding c') →
                  [inst_2 : e.IsTruncGE] →
                    [inst_3 : ∀ (i' : ι'), K.HasHomology i'] →
                      [inst_4 : CategoryTheory.Limits.HasZeroObject C] →
                        {i : ι} → {i' : ι'} → e.f i = i' → e.BoundaryGE i → ((K.truncGE e).X i' ≅ K.opcycles i')
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_minKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t ≠ ∅ → t.getKey? t.minKey! = some t.minKey!
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.strictMono_iff_injective : ∀ (f : CircleDeg1Lift), StrictMono ⇑f ↔ Function.Injective ⇑f
-- Mathlib.Algebra.Module.Equiv.Basic
AddEquiv.toIntLinearEquiv_refl : ∀ {M : Type u_5} [inst : AddCommGroup M] {modM : Module ℤ M}, (AddEquiv.refl M).toIntLinearEquiv = LinearEquiv.refl ℤ M
-- Mathlib.GroupTheory.Subgroup.Simple
AddEquiv.isSimpleAddGroup : ∀ {G : Type u_1} [inst : AddGroup G] {H : Type u_3} [inst_1 : AddGroup H] [IsSimpleAddGroup H] (e : G ≃+ H),
  IsSimpleAddGroup G
-- Mathlib.Data.Sum.Order
WithTop.orderIsoSumLexPUnit_toLex : ∀ {α : Type u_1} [inst : LE α] (a : α), WithTop.orderIsoSumLexPUnit ↑a = toLex (Sum.inl a)
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.mk : {k : Type u_1} →
  {P₁ : Type u_2} →
    {P₂ : Type u_3} →
      {V₁ : Type u_4} →
        {V₂ : Type u_5} →
          [inst : Ring k] →
            [inst_1 : AddCommGroup V₁] →
              [inst_2 : AddCommGroup V₂] →
                [inst_3 : Module k V₁] →
                  [inst_4 : Module k V₂] →
                    [inst_5 : AddTorsor V₁ P₁] →
                      [inst_6 : AddTorsor V₂ P₂] →
                        (toEquiv : P₁ ≃ P₂) →
                          (linear : V₁ ≃ₗ[k] V₂) →
                            (∀ (p : P₁) (v : V₁), toEquiv (v +ᵥ p) = linear v +ᵥ toEquiv p) → P₁ ≃ᵃ[k] P₂
-- Mathlib.Order.Circular
Btw.btw.antisymm : ∀ {α : Type u_1} [inst : CircularPartialOrder α] {a b c : α}, btw a b c → btw c b a → a = b ∨ b = c ∨ c = a
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
/-- **Alias** of `IsEllipticDvdSequence.id`.

---

The identity sequence is an EDS.  -/
isEllDivSequence_id : IsEllipticDvdSequence id
-- Mathlib.Order.Concept
Concept.intent_swap : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c : Concept α β r), c.swap.intent = c.extent
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.Const.insertListₘ.match_1.eq_1 : ∀ {α : Type u_2} {β : Type u_1} (motive : List (α × β) → Sort u_3) (h_1 : Unit → motive [])
  (h_2 : (hd : α × β) → (tl : List (α × β)) → motive (hd :: tl)),
  (match [] with
    | [] => h_1 ()
    | hd :: tl => h_2 hd tl) =
    h_1 ()
-- Init.Data.BitVec.Basic
/-- Rotates the bits in a bitvector to the right.

All the bits of `x` are shifted to lower positions, with the bottom `n` bits wrapping around to fill
the vacated high bits.

SMT-LIB name: `rotate_right`, except this operator uses a `Nat` shift amount.

Example:
 * `rotateRight 0b01001#5 1 = 0b10100`
 -/
BitVec.rotateRight : {w : ℕ} → BitVec w → ℕ → BitVec w
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Ioo_ae_eq_Ioc' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : PartialOrder α] {a b : α},
  μ {b} = 0 → Set.Ioo a b =ᵐ[μ] Set.Ioc a b
-- Mathlib.Topology.Defs.Filter
/-- The filter of neighborhoods of a set in a topological space.  -/
nhdsSet : {X : Type u_1} → [TopologicalSpace X] → Set X → Filter X
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.cooper₂.injEq : ∀ (c c_1 : Lean.Meta.Grind.Arith.Cutsat.CooperSplit),
  (Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.cooper₂ c = Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.cooper₂ c_1) =
    (c = c_1)
-- Lean.Meta.KExprMap
/-- Insert `e ↦ v` into `m`  -/
Lean.Meta.KExprMap.insert : {α : Type} → Lean.Meta.KExprMap α → Lean.Expr → α → Lean.MetaM (Lean.Meta.KExprMap α)
-- Mathlib.Algebra.CharP.Two
CharTwo.sum_sq : ∀ {R : Type u_1} {ι : Type u_2} [inst : CommSemiring R] [CharP R 2] (s : Finset ι) (f : ι → R),
  (∑ i ∈ s, f i) ^ 2 = ∑ i ∈ s, f i ^ 2
-- Mathlib.NumberTheory.LSeries.PrimesInAP
/-- We can express `ArithmeticFunction.vonMangoldt.residueClass` as a linear combination
of twists of the von Mangoldt function by Dirichlet characters.  -/
ArithmeticFunction.vonMangoldt.residueClass_apply : ∀ {q : ℕ} {a : ZMod q} [NeZero q],
  IsUnit a →
    ∀ (n : ℕ),
      ↑(ArithmeticFunction.vonMangoldt.residueClass a n) =
        (↑q.totient)⁻¹ * ∑ χ, χ a⁻¹ * χ ↑n * ↑(ArithmeticFunction.vonMangoldt n)
-- Lean.CoreM
/-- Creates a name from `n` that is guaranteed to be unique.
This is intended to be used for creating inaccessible user names for free variables and constants.

It works by adding a fresh macro scope to `n`.
Applying `Lean.Name.eraseMacroScopes` to the resulting name yields `n`.

See also `Lean.LocalContext.getUnusedName` (for creating a new accessible user name that is
unused in the local context) and `Lean.Meta.mkFreshBinderNameForTactic` (for creating names
that are conditionally inaccessible, depending on the current value of the `tactic.hygiene` option).
 -/
Lean.Core.mkFreshUserName : Lean.Name → Lean.CoreM Lean.Name
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.CompactOpens.coe_inf : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : QuasiSeparatedSpace α] (s t : TopologicalSpace.CompactOpens α),
  ↑(s ⊓ t) = ↑s ∩ ↑t
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.inv_inv_h₀_comp_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreZeroHypercover S} (e : E ≅ F)
  (i : F.I₀), CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (e.inv.h₀ i)) (F.f i) = E.f (e.inv.s₀ i)
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.aut_inv : ∀ {R : Type uR} {A₁ : Type uA₁} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Algebra R A₁]
  (ϕ : A₁ ≃ₐ[R] A₁), ϕ⁻¹ = ϕ.symm
-- Mathlib.Order.Category.FinBddDistLat
FinBddDistLat.forget_map : ∀ {X Y : FinBddDistLat} (f : X ⟶ Y),
  ⇑(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget FinBddDistLat).map f)) =
    ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
/-- Given a cocone `c` for a functor `F : J ⥤ C` from a well-ordered type,
and maps `p : X ⟶ Y`, `f : F.obj ⊥ ⟶ X`, `g : c.pt ⟶ Y`, this structure
contains the data of a map `F.obj j ⟶ X` such that `F.map (homOfLE bot_le) ≫ f' = f`
and `f' ≫ p = c.ι.app j ≫ g`. (This implies that the outer square below
commutes, see `SqStruct.w`.)

```
         f
F.obj ⊥ --> X
   |      Λ |
   |   f'╱  |
   v    ╱   |
F.obj j     | p
   |        |
   |        |
   v    g   v
  c.pt ---> Y
```
 -/
CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : LinearOrder J] →
        [inst_2 : OrderBot J] →
          {F : CategoryTheory.Functor J C} →
            (c : CategoryTheory.Limits.Cocone F) → {X Y : C} → (X ⟶ Y) → (F.obj ⊥ ⟶ X) → (c.pt ⟶ Y) → J → Type v
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.zero_apply : ∀ {ι : Type u_1} {M : ι → Type u_5} [inst : (i : ι) → Zero (M i)] (i : ι), 0 i = 0
-- Init.Data.Iterators.Lemmas.Producers.List
List.toList_iter : ∀ {β : Type w} {l : List β}, l.iter.toList = l
-- Init.Data.String.Basic
String.Pos.toSlice_lt_toSlice_iff : ∀ {s : String} {p q : s.Pos}, p.toSlice < q.toSlice ↔ p < q
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- The semantics of boolean problems involving BitVec predicates as atoms.
 -/
Std.Tactic.BVDecide.BVLogicalExpr.eval : Std.Tactic.BVDecide.BVExpr.Assignment → Std.Tactic.BVDecide.BVLogicalExpr → Bool
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.instToFormatLazyEntry : Std.ToFormat Lean.Meta.RefinedDiscrTree.LazyEntry
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.prodCongr_symm : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {F : Type u_4}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_5} [inst_7 : TopologicalSpace H]
  {H' : Type u_6} [inst_8 : TopologicalSpace H'] {G : Type u_7} [inst_9 : TopologicalSpace G] {G' : Type u_8}
  [inst_10 : TopologicalSpace G'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'}
  {J : ModelWithCorners 𝕜 F G} {J' : ModelWithCorners 𝕜 F G'} {M : Type u_9} [inst_11 : TopologicalSpace M]
  [inst_12 : ChartedSpace H M] {M' : Type u_10} [inst_13 : TopologicalSpace M'] [inst_14 : ChartedSpace H' M']
  {N : Type u_11} [inst_15 : TopologicalSpace N] [inst_16 : ChartedSpace G N] {N' : Type u_12}
  [inst_17 : TopologicalSpace N'] [inst_18 : ChartedSpace G' N'] {n : WithTop ℕ∞} (h₁ : Diffeomorph I I' M M' n)
  (h₂ : Diffeomorph J J' N N' n), (h₁.prodCongr h₂).symm = h₁.symm.prodCongr h₂.symm
-- Mathlib.Probability.Kernel.Disintegration.CondCDF
ProbabilityTheory.integrable_condCDF : ∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) [MeasureTheory.IsFiniteMeasure ρ] (x : ℝ),
  MeasureTheory.Integrable (fun a => ↑(ProbabilityTheory.condCDF ρ a) x) ρ.fst
-- Init.Grind.Module.Basic
/-- A module over the integers, i.e. a type with zero, addition, negation, subtraction, and scalar multiplication by integers,
satisfying appropriate compatibilities.

Equivalently, an additive commutative group.
 -/
Lean.Grind.IntModule : Type u → Type u
-- Mathlib.CategoryTheory.Category.Basic
/-- The composition of epimorphisms is again an epimorphism. This version takes `Epi f` and `Epi g`
as explicit arguments. For a version taking them as typeclass arguments, see `epi_comp`.  -/
CategoryTheory.epi_comp' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z},
  CategoryTheory.Epi f → CategoryTheory.Epi g → CategoryTheory.Epi (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Data.List.Chain
List.isChain_split : ∀ {α : Type u_1} {R : α → α → Prop} {c : α} {l₁ l₂ : List α},
  List.IsChain R (l₁ ++ c :: l₂) ↔ List.IsChain R (l₁ ++ [c]) ∧ List.IsChain R (c :: l₂)
-- Mathlib.Order.Interval.Set.Defs
Set.mem_Icc : ∀ {α : Type u_1} [inst : Preorder α] {a b x : α}, x ∈ Set.Icc a b ↔ a ≤ x ∧ x ≤ b
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.stronglyMeasurable_zero : ∀ {α : Type u_1} {β : Type u_2} {x : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : Zero β],
  MeasureTheory.StronglyMeasurable 0
-- Mathlib.Order.Ideal
Order.Ideal.instInhabited : {P : Type u_1} → [inst : Preorder P] → [Inhabited P] → Inhabited (Order.Ideal P)
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.single_eq_zero : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] {a : Γ}, (HahnSeries.single a) 0 = 0
-- Mathlib.Data.Sym.Sym2
/-- **Alias** of `Sym2.eq_swap`. -/
Sym2.mk_prod_swap_eq : ∀ {α : Type u_1} {a b : α}, s(a, b) = s(b, a)
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoid.End.ext : ∀ (M : Type u_4) [inst : AddZero M] {f g : AddMonoid.End M}, (∀ (x : M), f x = g x) → f = g
-- Mathlib.Algebra.LieRinehartAlgebra.Defs
LieRinehartAlgebra.mk : ∀ {R : Type u_1} {A : Type u_2} {L : Type u_3} [inst : CommRing A] [inst_1 : LieRing L] [inst_2 : Module A L]
  [inst_3 : LieRingModule L A] [inst_4 : LieRinehartRing A L] [inst_5 : CommRing R] [inst_6 : Algebra R A]
  [inst_7 : LieAlgebra R L] [toIsScalarTower : IsScalarTower R A L] [toLieModule : LieModule R L A],
  LieRinehartAlgebra R A L
-- Std.Do.PostCond
Std.Do.PostCond.entails.trans : ∀ {α : Type u_1} {ps : Std.Do.PostShape} {P Q R : Std.Do.PostCond α ps}, P.entails Q → Q.entails R → P.entails R
-- Mathlib.Algebra.GroupWithZero.Regular
IsLeftRegular.mul_left_eq_zero_iff : ∀ {R : Type u_1} [inst : MulZeroClass R] {a b : R}, IsLeftRegular b → (b * a = 0 ↔ a = 0)
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
uniformity_eq_comap_mul_inv_nhds_one : ∀ (Gᵣ : Type u_3) [inst : UniformSpace Gᵣ] [inst_1 : Group Gᵣ] [IsRightUniformGroup Gᵣ],
  uniformity Gᵣ = Filter.comap (fun x => x.2 * x.1⁻¹) (nhds 1)
-- Mathlib.Data.Sym.Sym2
Sym2.coe_lift₂_symm_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (F : Sym2 α → Sym2 β → γ) (a₁ a₂ : α) (b₁ b₂ : β),
  ↑(Sym2.lift₂.symm F) a₁ a₂ b₁ b₂ = F s(a₁, a₂) s(b₁, b₂)
-- Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders
MeasureTheory.closedCompactCylinders.eq_1 : ∀ {ι : Type u_1} (X : ι → Type u_2) [inst : (i : ι) → TopologicalSpace (X i)],
  MeasureTheory.closedCompactCylinders X =
    ⋃ s, ⋃ S, ⋃ (_ : IsClosed S), ⋃ (_ : IsCompact S), {MeasureTheory.cylinder s S}
-- Mathlib.Data.Complex.Basic
Complex.instNNRatCast : NNRatCast ℂ
-- Mathlib.Order.Booleanisation
Booleanisation.instSemilatticeSup : {α : Type u_1} → [GeneralizedBooleanAlgebra α] → SemilatticeSup (Booleanisation α)
-- Aesop.Index.RulePattern
/-- Get rule pattern substitutions for the patterns that match `e`.  -/
Aesop.RulePatternIndex.getSingle : Lean.Expr → Aesop.RulePatternIndex → Aesop.BaseM (Array (Aesop.RuleName × Aesop.Substitution))
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
/-- **Alias** of `FunLike.coe_zero`. -/
UniformConvergenceCLM.coe_zero : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Zero F] [inst_2 : Zero β]
  [IsZeroApply F α β], ⇑0 = 0
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.image_toSnowflaking_closedEBall : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : PseudoEMetricSpace X] (x : X) (r : ENNReal),
  ⇑Metric.Snowflaking.toSnowflaking '' Metric.closedEBall x r =
    Metric.closedEBall (Metric.Snowflaking.toSnowflaking x) (r ^ α)
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
/-- The choice of `d` in `Ideal.exists_mul_add_mem_pow_succ` is unique, up to `P`.
Inspired by [Neukirch], proposition 6.1  -/
Ideal.mul_add_mem_pow_succ_unique : ∀ {S : Type u_1} [inst : CommRing S] {P : Ideal S} [P_prime : P.IsPrime] [IsDedekindDomain S],
  P ≠ ⊥ →
    ∀ {i : ℕ} (a d d' e e' : S),
      a ∉ P ^ (i + 1) → e ∈ P ^ (i + 1) → e' ∈ P ^ (i + 1) → a * d + e - (a * d' + e') ∈ P ^ (i + 1) → d - d' ∈ P
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size_alter_eq_add_one : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {f : Option β → Option β},
  k ∉ m → (f m[k]?).isSome = true → (m.alter k f).size = m.size + 1
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Bounded.send : {α : Type} → Std.CloseableChannel.Bounded✝ α → α → BaseIO (Task (Except Std.CloseableChannel.Error Unit))
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.evalEval_multiset_prod : ∀ {R : Type u_1} [inst : CommSemiring R] (x y : R) (l : Multiset (Polynomial (Polynomial R))),
  Polynomial.evalEval x y l.prod = (Multiset.map (Polynomial.evalEval x y) l).prod
-- Mathlib.Topology.Connected.PathConnected
/-- If for each `i`, `x i` is joined to `y i`, then `x` is joined to `y` in the product space.  -/
Joined.pi : ∀ {ι : Type u_3} {Z : ι → Type u_4} [inst : (i : ι) → TopologicalSpace (Z i)] {x y : (i : ι) → Z i},
  (∀ (i : ι), Joined (x i) (y i)) → Joined x y
-- Init.Notation
/-- `a ++ b` is the result of concatenation of `a` and `b`, usually read "append".
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `++` in identifiers is `append`. -/
«term_++_» : Lean.TrailingParserDescr
-- Mathlib.MeasureTheory.Measure.Hausdorff
/-- Hausdorff measure `μH[d] s` is monotone in `d`.  -/
MeasureTheory.Measure.hausdorffMeasure_mono : ∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] {d₁ d₂ : ℝ},
  d₁ ≤ d₂ → ∀ (s : Set X), (MeasureTheory.Measure.hausdorffMeasure d₂) s ≤ (MeasureTheory.Measure.hausdorffMeasure d₁) s
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.nonempty : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2]
  [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2], Nonempty (P1 →ᵃ[k] P2)
-- Mathlib.Data.Finmap
Finmap.mk.injEq : ∀ {α : Type u} {β : α → Type v} (entries : Multiset (Sigma β)) (nodupKeys : entries.NodupKeys)
  (entries_1 : Multiset (Sigma β)) (nodupKeys_1 : entries_1.NodupKeys),
  ({ entries := entries, nodupKeys := nodupKeys } = { entries := entries_1, nodupKeys := nodupKeys_1 }) =
    (entries = entries_1)
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.span_prod_le : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {M' : Type u_8}
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (s : Set M) (t : Set M'),
  Submodule.span R (s ×ˢ t) ≤ (Submodule.span R s).prod (Submodule.span R t)
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
SimpleGraph.completeEquipartiteGraph_adj : ∀ {r t : ℕ} {v w : Fin r × Fin t}, (SimpleGraph.completeEquipartiteGraph r t).Adj v w ↔ v.1 ≠ w.1
-- Mathlib.Data.EReal.Basic
EReal.zero_mul : ∀ (x : EReal), 0 * x = 0
-- Mathlib.Algebra.Field.Subfield.Basic
/-- The action by a subfield is the action by the underlying field.  -/
Subfield.instSMulWithZeroSubtypeMem : {K : Type u} →
  [inst : DivisionRing K] →
    {X : Type u_1} → [inst_1 : Zero X] → [SMulWithZero K X] → (F : Subfield K) → SMulWithZero (↥F) X
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
SimpleGraph.TripartiteFromTriangles.cliqueFinset_eq_image : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (t : Finset (α × β × γ)) [inst : DecidableEq α] [inst_1 : DecidableEq β]
  [inst_2 : DecidableEq γ] [inst_3 : Fintype α] [inst_4 : Fintype β] [inst_5 : Fintype γ]
  [SimpleGraph.TripartiteFromTriangles.NoAccidental t],
  (SimpleGraph.TripartiteFromTriangles.graph t).cliqueFinset 3 =
    Finset.image (⇑SimpleGraph.TripartiteFromTriangles.toTriangle) t
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.Hom.mk : {R : Type u} → [inst : Semiring R] → {M N : SemimoduleCat R} → (↑M →ₗ[R] ↑N) → M.Hom N
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.isLeftAdjoint_pushout : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) {X Y : T}
  [P.IsStableUnderComposition] (f : X ⟶ Y) [inst_2 : P.HasPushoutsAlong f]
  [inst_3 : P.IsStableUnderCobaseChangeAlong f],
  P f → (CategoryTheory.MorphismProperty.Under.pushout P ⊤ f).IsLeftAdjoint
-- Mathlib.Topology.FiberBundle.Constructions
Pullback.continuous_proj : ∀ {B : Type u} (F : Type v) (E : B → Type w₁) {B' : Type w₂} [inst : TopologicalSpace B']
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] (f : B' → B), Continuous Bundle.TotalSpace.proj