mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Localization.Submodule
IsLocalization.mem_coeSubmodule : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (I : Ideal R)
  {x : S}, x ∈ IsLocalization.coeSubmodule S I ↔ ∃ y ∈ I, (algebraMap R S) y = x
-- Mathlib.Order.Booleanisation
Booleanisation.not_comp_lt_lift : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] {a b : α}, ¬Booleanisation.comp a < Booleanisation.lift b
-- Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
SSet.Subcomplex.degenerate_eq_top_iff : ∀ {X : SSet} (A : X.Subcomplex) (n : ℕ),
  A.toSSet.degenerate n = ⊤ ↔ X.degenerate n ⊓ A.obj (Opposite.op { len := n }) = A.obj (Opposite.op { len := n })
-- Mathlib.Order.Lattice
instIdempotentOpMax_mathlib : ∀ {α : Type u} [inst : SemilatticeSup α], Std.IdempotentOp fun x1 x2 => x1 ⊔ x2
-- Mathlib.CategoryTheory.Limits.Preserves.Filtered
/-- A functor is said to reflect cofiltered limits, if it reflects all limits of shape `J`, where
`J` is a cofiltered category which is small relative to the universe in which morphisms of the
source live.
 -/
CategoryTheory.Limits.ReflectsCofilteredLimits : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → Prop
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.HasModel.decode : {α : Type u} →
  {inst : LE α} →
    {inst_1 : LT α} →
      {β : outParam (Type v)} →
        {inst_2 : LE β} →
          {inst_3 : LT β} →
            {inst_4 : Std.PRange.UpwardEnumerable β} →
              {inst_5 : Std.PRange.LawfulUpwardEnumerable β} →
                {inst_6 : Std.PRange.LawfulUpwardEnumerableLE β} →
                  {inst_7 : Std.PRange.LawfulUpwardEnumerableLT β} → [self : HasModel✝ α β] → β → α
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.withLocalDecls.loop : {n : Type → Type u_1} →
  [MonadControlT Lean.MetaM n] →
    [Monad n] →
      {α : Type} →
        Array (Lean.Name × Lean.BinderInfo × (Array Lean.Expr → n Lean.Expr)) →
          (Array Lean.Expr → n α) → Lean.LocalDeclKind → [Inhabited α] → Array Lean.Expr → n α
-- Mathlib.CategoryTheory.Category.Pointed
Pointed.mk.sizeOf_spec : ∀ (X : Type u) (point : X), sizeOf { X := X, point := point } = 1 + sizeOf X + sizeOf point
-- Mathlib.Order.Antisymmetrization
acc_antisymmetrization_iff : ∀ {α : Type u_1} {a : α} [inst : Preorder α],
  Acc (fun x1 x2 => x1 < x2) (toAntisymmetrization (fun x1 x2 => x1 ≤ x2) a) ↔ Acc (fun x1 x2 => x1 < x2) a
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.map_le_iff_le_comap : ∀ {F : Type w} {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S]
  [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] {f : F} {s : NonUnitalSubring R}
  {t : NonUnitalSubring S}, NonUnitalSubring.map f s ≤ t ↔ s ≤ NonUnitalSubring.comap f t
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.DHashMap.Internal.AssocList.foldl_apply : ∀ {α : Type u} {β : α → Type v} {δ : Type w} {l : Std.DHashMap.Internal.AssocList α β} {acc : List δ}
  (f : (a : α) → β a → δ),
  Std.DHashMap.Internal.AssocList.foldl (fun acc k v => f k v :: acc) acc l =
    (List.map (fun p => f p.fst p.snd) l.toList).reverse ++ acc
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.insertIdxTR.go.eq_3 : ∀ {α : Type u_1} (a : α) (a_1 : Array α) (n : ℕ) (a_1_1 : α) (l : List α),
  List.insertIdxTR.go✝ a n.succ (a_1_1 :: l) a_1 = List.insertIdxTR.go✝ a n l (a_1.push a_1_1)
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imI_swapEquiv_apply : ∀ {R : Type u_3} (c₁ c₃ : R) [inst : CommRing R] (t : QuaternionAlgebra R c₁ 0 c₃),
  ((QuaternionAlgebra.swapEquiv c₁ c₃) t).imI = t.imJ
-- Mathlib.Tactic.Explode.Datatypes
/-- Allows us to compare `Expr`s fast.  -/
Mathlib.Explode.Entries.s : Mathlib.Explode.Entries → Lean.ExprMap Mathlib.Explode.Entry
-- Init.Data.Vector.Find
Vector.find?_eq_findSome?_guard : ∀ {α : Type} {n : ℕ} {p : α → Bool} {xs : Vector α n}, Vector.find? p xs = Vector.findSome? (Option.guard p) xs
-- Mathlib.Data.Int.Log
Int.clog.eq_1 : ∀ {R : Type u_1} [inst : Semifield R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] (b : ℕ) (r : R),
  Int.clog b r = if 1 ≤ r then ↑(Nat.clog b ⌈r⌉₊) else -↑(Nat.log b ⌊r⁻¹⌋₊)
-- Mathlib.Data.Set.Restrict
Set.restrictPreimage_mk : ∀ {α : Type u_1} {β : Type u_2} (t : Set β) {f : α → β} {a : α} (h : a ∈ f ⁻¹' t),
  t.restrictPreimage f ⟨a, h⟩ = ⟨f a, h⟩
-- Lean.Elab.BuiltinTerm
_private.Lean.Elab.BuiltinTerm.0.Lean.Elab.Term.getMVarFromUserName : Lean.Syntax → Lean.MetaM Lean.Expr
-- Lean.Parser.Types
Lean.Parser.ParserState : Type
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryFan.IsLimit.lift_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y W : C} {s : CategoryTheory.Limits.BinaryFan X Y}
  (h : CategoryTheory.Limits.IsLimit s) (f : W ⟶ X) (g : W ⟶ Y) {Z : C}
  (h_1 : (CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left } ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.IsLimit.lift h f g)
      (CategoryTheory.CategoryStruct.comp s.fst h_1) =
    CategoryTheory.CategoryStruct.comp f h_1
-- Mathlib.Analysis.SpecialFunctions.FrullaniIntegral
Frullani.intervalIntegrable_inv_smul_comp_mul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b c : ℝ},
  MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume →
    0 < a → 0 < b → 0 < c → IntervalIntegrable (fun x => x⁻¹ • f (c * x)) MeasureTheory.volume a b
-- Mathlib.Order.Bounds.Basic
bbdAbove_range_sup : ∀ {ι : Sort u_4} {α : Type u_5} [inst : SemilatticeSup α] {f g : ι → α},
  BddAbove (Set.range f) → BddAbove (Set.range g) → BddAbove (Set.range fun x => f x ⊔ g x)
-- Mathlib.Data.Nat.BinaryRec
Nat.binaryRec'.eq_1 : ∀ {motive : ℕ → Sort u} (zero : motive 0)
  (bit : (b : Bool) → (n : ℕ) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)) (n : ℕ),
  Nat.binaryRec' zero bit n =
    Nat.binaryRec zero
      (fun b n ih =>
        if h : n = 0 → b = true then bit b n h ih
        else
          have this := ⋯;
          ⋯ ▸ zero)
      n
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.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
-- Mathlib.Algebra.Order.Group.Cone
/-- Construct a partially ordered abelian group by designating a cone in an abelian group.  -/
IsOrderedAddMonoid.mkOfCone : ∀ {S : Type u_1} {G : Type u_2} [inst : AddCommGroup G] [inst_1 : SetLike S G] (C : S) [inst_2 : AddGroupConeClass S G],
  have x := PartialOrder.mkOfAddGroupCone C;
  IsOrderedAddMonoid G
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_mul_const_Ioo₀ : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [MulPosReflectLT G₀] {c : G₀} (a b : G₀),
  0 < c → (fun x => x * c) ⁻¹' Set.Ioo a b = Set.Ioo (a / c) (b / c)
-- Mathlib.RingTheory.Polynomial.GaussNorm
Polynomial.gaussNorm_zero : ∀ {R : Type u_1} {F : Type u_2} [inst : Semiring R] [inst_1 : FunLike F R ℝ] (v : F) (c : ℝ),
  Polynomial.gaussNorm v c 0 = 0
-- Aesop.Frontend.Saturate
Aesop.Frontend.tacticForward?____ : Lean.ParserDescr
-- Mathlib.Combinatorics.SimpleGraph.Dart
SimpleGraph.dartOfNeighborSet_injective : ∀ {V : Type u_1} (G : SimpleGraph V) (v : V), Function.Injective (G.dartOfNeighborSet v)
-- Mathlib.Algebra.Order.GroupWithZero.WithZero
OrderIso.withZeroUnits_symm_apply : ∀ {α : Type u_1} [inst : LinearOrderedCommGroupWithZero α] (a : α),
  (RelIso.symm OrderIso.withZeroUnits) a = if h : a = 0 then 0 else ↑(Units.mk0 a h)
-- Init.Data.Int.Linear
Int.Internal.Linear.dvd_norm : ∀ (ctx : Int.Internal.Linear.Context) (d : ℤ) (p₁ p₂ : Int.Internal.Linear.Poly),
  p₁.norm.beq' p₂ = true → d ∣ Int.Internal.Linear.Poly.denote' ctx p₁ → d ∣ Int.Internal.Linear.Poly.denote' ctx p₂
-- Mathlib.Algebra.Opposites
AddOpposite.op_add : ∀ {α : Type u_1} [inst : Add α] (x y : α), AddOpposite.op (x + y) = AddOpposite.op y + AddOpposite.op x
-- Mathlib.CategoryTheory.Sites.Monoidal
CategoryTheory.presheafHom.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  (F G : CategoryTheory.Functor Cᵒᵖ A),
  CategoryTheory.presheafHom F G =
    {
      obj := fun X =>
        (CategoryTheory.Over.forget (Opposite.unop X)).op.comp F ⟶
          (CategoryTheory.Over.forget (Opposite.unop X)).op.comp G,
      map := fun {X Y} f => TypeCat.ofHom (CategoryTheory.Over.map f.unop).op.whiskerLeft, map_id := ⋯, map_comp := ⋯ }
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toList_rcc_eq_add : ∀ {m n i : ℕ}, i < n + 1 - m → (m...=n).toList[i]! = m + i
-- Mathlib.Analysis.CStarAlgebra.Basic
coe_starₗᵢ : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : CommSemiring 𝕜] [inst_1 : StarRing 𝕜] [inst_2 : SeminormedAddCommGroup E]
  [inst_3 : StarAddMonoid E] [inst_4 : NormedStarGroup E] [inst_5 : Module 𝕜 E] [inst_6 : StarModule 𝕜 E],
  ⇑(starₗᵢ 𝕜) = star
-- Mathlib.Data.Finset.Lattice.Fold
/-- Infimum of a finite set: `inf {a, b, c} f = f a ⊓ f b ⊓ f c`  -/
Finset.inf : {α : Type u_2} → {β : Type u_3} → [inst : SemilatticeInf α] → [OrderTop α] → Finset β → (β → α) → α
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
/-- Associator for the vertical composition of lax natural transformations.  -/
CategoryTheory.Lax.LaxTrans.associator : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G H I : CategoryTheory.LaxFunctor B C} →
          (η : F ⟶ G) →
            (θ : G ⟶ H) →
              (ι : H ⟶ I) →
                CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp η θ) ι ≅
                  CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.comp θ ι)
-- Mathlib.Algebra.Ring.Hom.Defs
RingHom.ext : ∀ {α : Type u_2} {β : Type u_3} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} ⦃f g : α →+* β⦄,
  (∀ (x_2 : α), f x_2 = g x_2) → f = g
-- Mathlib.Topology.Path
/-- `γ.truncateOfLE t₀ t₁ h`, where `h : t₀ ≤ t₁` is `γ.truncate t₀ t₁`
casted as a path from `γ.extend t₀` to `γ.extend t₁`.  -/
Path.truncateOfLE : {X : Type u_4} →
  [inst : TopologicalSpace X] → {a b : X} → (γ : Path a b) → {t₀ t₁ : ℝ} → t₀ ≤ t₁ → Path (γ.extend t₀) (γ.extend t₁)
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) (U : TopologicalSpace.Opens ↑Y.toTopCat) (x : ↑X.toTopCat)
  (hx : (CategoryTheory.ConcreteCategory.hom f.base) x ∈ U),
  CategoryTheory.CategoryStruct.comp (Y.presheaf.germ U ((CategoryTheory.ConcreteCategory.hom f.base) x) hx)
      (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x) =
    CategoryTheory.CategoryStruct.comp (f.c.app (Opposite.op U))
      (X.presheaf.germ ((TopologicalSpace.Opens.map f.base).obj U) x hx)
-- Mathlib.GroupTheory.GroupAction.Support
/-- A set `s` supports `b` if `g +ᵥ b = b` whenever `g +ᵥ a = a` for all `a ∈ s`.  -/
AddAction.Supports : (G : Type u_1) → {α : Type u_3} → {β : Type u_4} → [VAdd G α] → [VAdd G β] → Set α → β → Prop
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.isoLimitCone_hom_π : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F] (t : CategoryTheory.Limits.LimitCone F)
  (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.isoLimitCone t).hom (t.cone.π.app j) =
    CategoryTheory.Limits.limit.π F j
-- Init.Data.String.Extra
_private.Init.Data.String.Extra.0.String.removeNumLeadingSpaces.consumeSpaces : ℕ → ℕ → {s : String} → s.Pos → String → String
-- Mathlib.Analysis.Matrix.Normed
/-- Seminormed group instance (using sup norm of L1 norm) for matrices over a seminormed group. Not
declared as an instance because there are several natural choices for defining the norm of a
matrix.  -/
Matrix.linftyOpSeminormedAddCommGroup : {m : Type u_3} →
  {n : Type u_4} →
    {α : Type u_5} → [Fintype m] → [Fintype n] → [SeminormedAddCommGroup α] → SeminormedAddCommGroup (Matrix m n α)
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.refl_toBialgHom : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : CoalgebraStruct R A], ↑(BialgEquiv.refl R A) = BialgHom.id R A
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.Functor.map_shiftFunctorCompIsoId_inv_app_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) {A : Type u_4} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A] [inst_5 : F.CommShift A] (X : C)
  (a b : A) (h : a + b = 0) {Z : D}
  (h_1 : F.obj ((CategoryTheory.shiftFunctor C b).obj ((CategoryTheory.shiftFunctor C a).obj X)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctorCompIsoId C a b h).inv.app X)) h_1 =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId D a b h).inv.app (F.obj X))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor D b).map ((CategoryTheory.Functor.commShiftIso F a).inv.app X))
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.Functor.commShiftIso F b).inv.app ((CategoryTheory.shiftFunctor C a).obj X)) h_1))
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.lift_fac_assoc : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f]
  (H' : Set.range ⇑g ⊆ Set.range ⇑f) {Z_1 : AlgebraicGeometry.Scheme} (h : Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.IsOpenImmersion.lift f g H')
      (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp g h
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCastD_filter_not_contains_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α} {k : α}
  {fallback : β k},
  Std.Internal.List.DistinctKeys l₁ →
    l₂.contains k = false →
      Std.Internal.List.getValueCastD k (List.filter (fun p => !l₂.contains p.fst) l₁) fallback =
        Std.Internal.List.getValueCastD k l₁ fallback
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_insert!_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α], t.WF → ∀ {k : α} {v : β k}, (Std.DTreeMap.Internal.Impl.insert! k v t).get? k = some v
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.toSubmodule_toSubalgebra : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (S : Subalgebra R A), (Subalgebra.toSubmodule S).toSubalgebra ⋯ ⋯ = S
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
le_one_of_mul_le_right : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : LE α] [MulLeftReflectLE α] {a b : α}, a * b ≤ a → b ≤ 1
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
Multipliable.sigma_factor : ∀ {α : Type u_1} {β : Type u_2} [inst : CommGroup α] [inst_1 : UniformSpace α] [IsUniformGroup α] [CompleteSpace α]
  {γ : β → Type u_4} {f : (b : β) × γ b → α}, Multipliable f → ∀ (b : β), Multipliable fun c => f ⟨b, c⟩
-- Mathlib.Geometry.Euclidean.MongePoint
/-- The orthocenter of a triangle is the intersection of its
altitudes.  It is defined here as the 2-dimensional case of the
Monge point.  -/
Affine.Triangle.orthocenter : {V : Type u_1} →
  {P : Type u_2} →
    [inst : NormedAddCommGroup V] →
      [inst_1 : InnerProductSpace ℝ V] →
        [inst_2 : MetricSpace P] → [inst_3 : NormedAddTorsor V P] → Affine.Triangle ℝ P → P
-- Mathlib.Data.Finset.Pi
Finset.domRestrict_preimage : ∀ {ι : Type u_2} {π : ι → Type u_3} [inst : DecidableEq ι] {I : Set ι} [inst_1 : DecidablePred fun x => x ∈ I]
  (s : Finset ↑I) (u : (i : ↑I) → Set (π ↑i)),
  I.domRestrict ⁻¹' (↑s).pi u = (↑(Finset.image Subtype.val s)).pi fun i => if h : i ∈ I then u ⟨i, h⟩ else Set.univ
-- Mathlib.MeasureTheory.Measure.Haar.Unique
/-- **Uniqueness of left-invariant measures**:
Given two left-invariant measures which are finite on compacts, they coincide in the following
sense: they give the same value to sets with compact closure, up to the multiplicative
constant `haarScalarFactor μ' μ`.  -/
MeasureTheory.Measure.measure_isMulInvariant_eq_smul_of_isCompact_closure : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [LocallyCompactSpace G] (μ' μ : MeasureTheory.Measure G)
  [inst_6 : μ.IsHaarMeasure] [inst_7 : MeasureTheory.IsFiniteMeasureOnCompacts μ'] [inst_8 : μ'.IsMulLeftInvariant]
  {s : Set G}, IsCompact (closure s) → μ' s = μ'.haarScalarFactor μ • μ s
-- Mathlib.Data.Finsupp.Basic
Finsupp.subtypeDomain_sum : ∀ {α : Type u_1} {ι : Type u_4} {M : Type u_5} [inst : AddCommMonoid M] {p : α → Prop} {s : Finset ι} {h : ι → α →₀ M},
  Finsupp.subtypeDomain p (∑ c ∈ s, h c) = ∑ c ∈ s, Finsupp.subtypeDomain p (h c)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_left_le_size_union : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → m₁.size ≤ (m₁ ∪ m₂).size
-- Mathlib.Testing.Plausible.Functions
Plausible.TotalFunction.zeroDefaultSupp.congr_simp : ∀ {α : Type u} {β : Type v} [inst : DecidableEq α] [inst_1 : Zero β] {inst_2 : DecidableEq β} [inst_3 : DecidableEq β]
  (a a_1 : Plausible.TotalFunction α β), a = a_1 → a.zeroDefaultSupp = a_1.zeroDefaultSupp
-- Init.Data.List.Find
List.findIdx_lt_length : ∀ {α : Type u_1} {p : α → Bool} {xs : List α}, List.findIdx p xs < xs.length ↔ ∃ x ∈ xs, p x = true
-- Mathlib.Algebra.Category.CommAlgCat.Basic
/-- The object in the category of R-algebras associated to a type equipped with the appropriate
typeclasses. This is the preferred way to construct a term of `CommAlgCat R`.  -/
CommAlgCat.of : (R : Type u) → [inst : CommRing R] → (X : Type v) → [inst_1 : CommRing X] → [Algebra R X] → CommAlgCat R
-- Init.Grind.Norm
Lean.Grind.imp_eq : ∀ (p q : Prop), (p → q) = (¬p ∨ q)
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
Std.Iter.toArray_flatMapAfter : ∀ {α α₂ β γ : Type w} [inst : Std.Iterator α Id β] [inst_1 : Std.Iterator α₂ Id γ] [Std.Iterators.Finite α Id]
  [Std.Iterators.Finite α₂ Id] {f : β → Std.Iter γ} {it₁ : Std.Iter β} {it₂ : Option (Std.Iter γ)},
  (Std.Iter.flatMapAfter f it₁ it₂).toArray =
    match it₂ with
    | none => (Std.Iter.map (fun b => (f b).toArray) it₁).toArray.flatten
    | some it₂ => it₂.toArray ++ (Std.Iter.map (fun b => (f b).toArray) it₁).toArray.flatten
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.OplaxMonoidal.left_unitality_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.OplaxMonoidal] (X : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OplaxMonoidal.δ F (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.OplaxMonoidal.η F) (F.obj X))
        (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj X)).hom) =
    F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.instIsCorepresentableObjOppositeTypeCoyoneda : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ}, (CategoryTheory.coyoneda.obj X).IsCorepresentable
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite
/-- Transfer creation of finite products along a natural isomorphism in the functor.  -/
CategoryTheory.Limits.createsFiniteProductsOfNatIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F G : CategoryTheory.Functor C D} →
          {h : F ≅ G} → [CategoryTheory.Limits.CreatesFiniteProducts F] → CategoryTheory.Limits.CreatesFiniteProducts G
-- Mathlib.Algebra.Order.Floor.Div
Nat.instFloorDiv : FloorDiv ℕ ℕ
-- Mathlib.AlgebraicGeometry.Morphisms.Affine
AlgebraicGeometry.IsAffineOpen.iInf : ∀ {X : AlgebraicGeometry.Scheme}
  [AlgebraicGeometry.IsAffineHom (CategoryTheory.Limits.pullback.diagonal (CategoryTheory.Limits.terminal.from X))]
  {ι : Sort u_1} [Finite ι] [Nonempty ι] {U : ι → X.Opens},
  (∀ (i : ι), AlgebraicGeometry.IsAffineOpen (U i)) → AlgebraicGeometry.IsAffineOpen (⨅ i, U i)
-- Mathlib.Data.Set.Lattice.Image
Set.image2_iUnion_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_5} (f : α → β → γ) (s : Set α) (t : ι → Set β),
  Set.image2 f s (⋃ i, t i) = ⋃ i, Set.image2 f s (t i)
-- Mathlib.Logic.Equiv.Basic
Equiv.sigmaSigmaSubtypeEq_apply : ∀ {α : Type u_9} {β : Type u_10} {γ : α → β → Type u_11} {a : α} {b : β} (s : { s // s.fst = a ∧ s.snd.fst = b }),
  (Equiv.sigmaSigmaSubtypeEq a b) s = cast ⋯ (↑s).snd.snd
-- Mathlib.Algebra.Module.StablyFree.Basic
Module.instProjectiveOfIsStablyFree : ∀ (R : Type u) [inst : Ring R] (M : Type v) [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.IsStablyFree R M],
  Module.Projective R M
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
CStarAlgebra.mem_Icc_iff_norm_le_one : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {x : A},
  x ∈ Set.Icc 0 1 ↔ 0 ≤ x ∧ ‖x‖ ≤ 1
-- Mathlib.Analysis.Complex.Hadamard
Complex.HadamardThreeLines.interpStrip'.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] (f : ℂ → E) (l u : ℝ) (z : ℂ),
  Complex.HadamardThreeLines.interpStrip' f l u z =
    if Complex.HadamardThreeLines.sSupNormIm f l = 0 ∨ Complex.HadamardThreeLines.sSupNormIm f u = 0 then 0
    else
      ↑(Complex.HadamardThreeLines.sSupNormIm f l) ^ (1 - (z - ↑l) / (↑u - ↑l)) *
        ↑(Complex.HadamardThreeLines.sSupNormIm f u) ^ ((z - ↑l) / (↑u - ↑l))
-- Mathlib.Tactic.Recover
/-- `recover tacs` applies the tactic (sequence) `tacs` and then re-adds goals that were
incorrectly marked as closed. This helps to debug issues where a tactic closes goals without
solving them (i.e. goals were removed from the MetaM state without the metavariable
being assigned), resulting in the error "(kernel) declaration has metavariables".  -/
Mathlib.Tactic.tacticRecover_ : Lean.ParserDescr
-- Mathlib.Logic.Embedding.Basic
/-- A subtype `{x // p x}` can be injectively sent to into a subtype `{x // q x}`,
if `p x → q x` for all `x : α`.  -/
Subtype.impEmbedding : {α : Type u_1} → (p q : α → Prop) → (∀ (x : α), p x → q x) → { x // p x } ↪ { x // q x }
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Splitting.homologyData_right : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} [inst_2 : CategoryTheory.Limits.HasZeroObject C] (s : S.Splitting),
  s.homologyData.right = s.rightHomologyData
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.Point.toAffine_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F} (hP : W.Nonsingular P)
  (hPz : P 2 ≠ 0),
  WeierstrassCurve.Projective.Point.toAffine W P = WeierstrassCurve.Affine.Point.some (P 0 / P 2) (P 1 / P 2) ⋯
-- Mathlib.Algebra.Algebra.Opposite
AlgEquiv.opComm_symm_apply_symm_apply : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (a : Aᵐᵒᵖ ≃ₐ[R] B) (a_1 : Bᵐᵒᵖ),
  (AlgEquiv.opComm.symm a).symm a_1 = MulOpposite.unop (a.symm (MulOpposite.unop a_1))