mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalAlgEquivClass.toRingEquivClass : ∀ {F : Type u_1} {R : outParam (Type u_2)} {A : outParam (Type u_3)} {B : outParam (Type u_4)} {inst : Add A}
  {inst_1 : Mul A} {inst_2 : SMul R A} {inst_3 : Add B} {inst_4 : Mul B} {inst_5 : SMul R B} {inst_6 : EquivLike F A B}
  [self : NonUnitalAlgEquivClass F R A B], RingEquivClass F A B
-- Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
/-- If `g` is a non-scalar orientation preserving matrix with a fixed point in `ℍ`,
then it's an elliptic matrix.  -/
UpperHalfPlane.isElliptic_of_exists_smul_eq_self : ∀ {g : GL (Fin 2) ℝ}, 0 < (↑g).det → g ∉ Subgroup.center (GL (Fin 2) ℝ) → (∃ z, g • z = z) → g.IsElliptic
-- Mathlib.Data.List.Basic
List.get_attach : ∀ {α : Type u} (l : List α) (i : Fin l.attach.length), ↑(l.attach.get i) = l.get ⟨↑i, ⋯⟩
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
/-- The action by a subalgebra is the action by the underlying algebra.  -/
Subalgebra.instSMulWithZeroSubtypeMem : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] →
        [inst_2 : Algebra R A] →
          {α : Type u_1} → [inst_3 : Zero α] → [SMulWithZero A α] → (S : Subalgebra R A) → SMulWithZero (↥S) α
-- Mathlib.NumberTheory.Pell
/-- The set of solutions with `x` and `y` positive is closed under multiplication.  -/
Pell.Solution₁.y_mul_pos : ∀ {d : ℤ} {a b : Pell.Solution₁ d}, 0 < a.x → 0 < a.y → 0 < b.x → 0 < b.y → 0 < (a * b).y
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.setRed.eq_1 : ∀ {α : Type u_1} (c : RBTree.RBColor) (a : RBTree.RBNode α) (v : α) (b : RBTree.RBNode α),
  (RBTree.RBNode.node c a v b).setRed = RBTree.RBNode.node RBTree.RBColor.red a v b
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
ModuleCat.free_η_freeMk : ∀ (R : Type u) [inst : CommRing R] (x : PUnit.{u + 1}),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Functor.OplaxMonoidal.η (ModuleCat.free R)))
      (ModuleCat.freeMk x) =
    1
-- Std.Data.HashSet.IteratorLemmas
Std.HashSet.Raw.toArray_iter : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → m.iter.toArray = m.toArray
-- Mathlib.Order.OrderDual
/-- Transfer `HNot` across an `Equiv`.  -/
Equiv.hnot : {α : Type u_1} → {β : Type u_2} → α ≃ β → [HNot β] → HNot α
-- Mathlib.Topology.Instances.Nat
Nat.preimage_ball : ∀ (x : ℕ) (r : ℝ), Nat.cast ⁻¹' Metric.ball (↑x) r = Metric.ball x r
-- Mathlib.Order.CompleteLattice.Finset
Finset.iSup_union : ∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice β] [inst_1 : DecidableEq α] {f : α → β} {s t : Finset α},
  ⨆ x ∈ s ∪ t, f x = (⨆ x ∈ s, f x) ⊔ ⨆ x ∈ t, f x
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
/-- The cone for `StructuredArrow.proj Y L ⋙ F` attached to `E : RightExtension L F`.
The point of this cone is `E.left.obj Y`  -/
CategoryTheory.Functor.RightExtension.coneAt : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} H] →
            {L : CategoryTheory.Functor C D} →
              {F : CategoryTheory.Functor C H} →
                L.RightExtension F →
                  (Y : D) → CategoryTheory.Limits.Cone ((CategoryTheory.StructuredArrow.proj Y L).comp F)
-- Mathlib.Analysis.Normed.Ring.Basic
/-- The norm is submultiplicative.  -/
NonUnitalSeminormedRing.norm_mul_le : ∀ {α : Type u_5} [self : NonUnitalSeminormedRing α] (a b : α), ‖a * b‖ ≤ ‖a‖ * ‖b‖
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
CategoryTheory.Bicategory.rightAdjointSquare.vcomp.eq_1 : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d e f : B} {g₁ : a ⟶ c} {g₂ : c ⟶ e} {h₁ : b ⟶ d}
  {h₂ : d ⟶ f} {r₁ : b ⟶ a} {r₂ : d ⟶ c} {r₃ : f ⟶ e}
  (α : CategoryTheory.CategoryStruct.comp r₁ g₁ ⟶ CategoryTheory.CategoryStruct.comp h₁ r₂)
  (β : CategoryTheory.CategoryStruct.comp r₂ g₂ ⟶ CategoryTheory.CategoryStruct.comp h₂ r₃),
  CategoryTheory.Bicategory.rightAdjointSquare.vcomp α β =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator r₁ g₁ g₂).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight α g₂)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator h₁ r₂ g₂).hom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft h₁ β)
            (CategoryTheory.Bicategory.associator h₁ h₂ r₃).inv)))
-- Lean.Environment
Lean.PersistentEnvExtensionDescr.mk.sizeOf_spec : ∀ {α β σ : Type} [inst : SizeOf α] [inst_1 : SizeOf β] [inst_2 : SizeOf σ]
  (toPersistentEnvExtensionDescrCore : Lean.PersistentEnvExtensionDescrCore α β σ) (exportEntriesFn : σ → Array α),
  sizeOf
      { toPersistentEnvExtensionDescrCore := toPersistentEnvExtensionDescrCore, exportEntriesFn := exportEntriesFn } =
    1 + sizeOf toPersistentEnvExtensionDescrCore
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.extend_apply' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  (f₁ : MeasureTheory.SimpleFunc α γ) {g : α → β} (hg : MeasurableEmbedding g) (f₂ : MeasureTheory.SimpleFunc β γ)
  {y : β}, (¬∃ x, g x = y) → (f₁.extend g hg f₂) y = f₂ y
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.preservesLimits_forget : ∀ (k : Type u) (G : Type v) [inst : Ring k] [inst_1 : Monoid G],
  CategoryTheory.Limits.PreservesLimitsOfSize.{w, w, w, w, max (max u v) (w + 1), max u (w + 1)}
    (CategoryTheory.forget₂ (Rep.{w, u, v} k G) (ModuleCat k))
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.IsStableUnderFiniteProducts.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C},
  (∀ (J : Type) [Finite J], W.IsStableUnderProductsOfShape J) → W.IsStableUnderFiniteProducts
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.foldl_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} {δ : Type w}
  [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {f : δ → (a : α) → β a → δ} {init : δ},
          Std.DTreeMap.Internal.Impl.foldl f init t₁ = Std.DTreeMap.Internal.Impl.foldl f init t₂
-- Mathlib.RingTheory.Localization.Integral
IsLocalization.integerNormalization_aeval_eq_zero : ∀ {R : Type u_1} [inst : CommRing R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : IsLocalization M S] {R' : Type u_3} [inst_4 : CommRing R'] [inst_5 : Algebra R R'] [inst_6 : Algebra S R']
  [IsScalarTower R S R'] (p : Polynomial S) {x : R'},
  (Polynomial.aeval x) p = 0 → (Polynomial.aeval x) (IsLocalization.integerNormalization M p) = 0
-- Lean.Elab.MatchAltView
Lean.Elab.Term.MatchAltView.mk.injEq : ∀ {k : Lean.SyntaxNodeKinds} (ref : Lean.Syntax) (patterns : Array Lean.Syntax) (lhs : Lean.Syntax)
  (rhs : Lean.TSyntax k) (ref_1 : Lean.Syntax) (patterns_1 : Array Lean.Syntax) (lhs_1 : Lean.Syntax)
  (rhs_1 : Lean.TSyntax k),
  ({ ref := ref, patterns := patterns, lhs := lhs, rhs := rhs } =
      { ref := ref_1, patterns := patterns_1, lhs := lhs_1, rhs := rhs_1 }) =
    (ref = ref_1 ∧ patterns = patterns_1 ∧ lhs = lhs_1 ∧ rhs = rhs_1)
-- Mathlib.MeasureTheory.Measure.AddContent
/-- Extend a content over `C` to the finite unions of elements of `C` by additivity.
Use instead `AddContent.supClosure` which is the same function bundled as an `AddContent`.  -/
_private.Mathlib.MeasureTheory.Measure.AddContent.0.MeasureTheory.AddContent.supClosureFun : {α : Type u_1} →
  {C : Set (Set α)} → {G : Type u_2} → [inst : AddCommMonoid G] → MeasureTheory.AddContent G C → Set α → G
-- Mathlib.NumberTheory.PythagoreanTriples
_private.Mathlib.NumberTheory.PythagoreanTriples.0.coprime_sq_sub_mul_of_odd_even : ∀ {m n : ℤ}, m.gcd n = 1 → m % 2 = 1 → n % 2 = 0 → (m ^ 2 - n ^ 2).gcd (2 * m * n) = 1
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
/-- Pullback a `LinearOrderedCommMonoidWithZero` under an injective map.
See note [reducible non-instances].  -/
Function.Injective.linearOrderedCommMonoidWithZero : {α : Type u_1} →
  [inst : LinearOrderedCommMonoidWithZero α] →
    {β : Type u_3} →
      [inst_1 : Zero β] →
        [inst_2 : Bot β] →
          [inst_3 : One β] →
            [inst_4 : Mul β] →
              [inst_5 : Pow β ℕ] →
                [inst_6 : LE β] →
                  [inst_7 : LT β] →
                    [inst_8 : Max β] →
                      [inst_9 : Min β] →
                        [inst_10 : Ord β] →
                          [DecidableEq β] →
                            [DecidableLE β] →
                              [DecidableLT β] →
                                (f : β → α) →
                                  Function.Injective f →
                                    f 0 = 0 →
                                      f 1 = 1 →
                                        (∀ (x y : β), f (x * y) = f x * f y) →
                                          (∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n) →
                                            (∀ {x y : β}, f x ≤ f y ↔ x ≤ y) →
                                              (∀ {x y : β}, f x < f y ↔ x < y) →
                                                (∀ (x y : β), f (x ⊔ y) = max (f x) (f y)) →
                                                  (∀ (x y : β), f (x ⊓ y) = min (f x) (f y)) →
                                                    f ⊥ = ⊥ →
                                                      (∀ (x y : β), compare (f x) (f y) = compare x y) →
                                                        LinearOrderedCommMonoidWithZero β
-- Mathlib.Topology.Sheaves.Over
TopologicalSpace.Opens.overEquivalence_counitIso_hom_app : ∀ {X : Type u} [inst : TopologicalSpace X] (U : TopologicalSpace.Opens X) (X_1 : TopologicalSpace.Opens ↥U),
  U.overEquivalence.counitIso.hom.app X_1 = CategoryTheory.eqToHom ⋯
-- Mathlib.Algebra.Ring.Defs
/-- The canonical homomorphism `ℤ → R` for negative values is just the negation of the values
of the canonical homomorphism `ℕ → R`.  -/
NonAssocRing.intCast_negSucc : ∀ {α : Type u_1} [self : NonAssocRing α] (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKey?_alter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k k' : α} {f : Option β → Option β},
  (Std.DHashMap.Const.alter m k f).getKey? k' =
    if (k == k') = true then if (f (Std.DHashMap.Const.get? m k)).isSome = true then some k else none else m.getKey? k'
-- Init.Data.Rat.Lemmas
Rat.divInt_num_den : ∀ {d n n' : ℤ} {d' : ℕ} {z' : d' ≠ 0} {c : n'.natAbs.Coprime d'},
  d ≠ 0 → Rat.divInt n d = { num := n', den := d', den_nz := z', reduced := c } → ∃ m, m ≠ 0 ∧ n = n' * m ∧ d = ↑d' * m
-- Mathlib.RingTheory.FinitePresentation
/-- An algebra is finitely presented if and only if it is a quotient of a polynomial ring whose
variables are indexed by a fintype by a finitely generated ideal.  -/
Algebra.FinitePresentation.iff_quotient_mvPolynomial' : ∀ {R : Type w₁} {A : Type w₂} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  Algebra.FinitePresentation R A ↔ ∃ ι x f, Function.Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat.id_def : ∀ (R : Type u) [inst : Semiring R] (M : CategoryTheory.Mat R),
  CategoryTheory.CategoryStruct.id M = fun i j => if i = j then 1 else 0
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.instHasRightCalculusOfFractionsTrWOfIsTriangulatedOfIsTriangulated : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) [CategoryTheory.IsTriangulated C] [P.IsTriangulated],
  P.trW.HasRightCalculusOfFractions
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.eq_restrictScalarsRange₂_iff : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} {M' : Type u_6} {N' : Type u_7}
  {P' : Type u_8} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : SMul S R] [inst_3 : AddCommMonoid M]
  [inst_4 : Module R M] [inst_5 : AddCommMonoid N] [inst_6 : Module R N] [inst_7 : AddCommMonoid P]
  [inst_8 : Module R P] [inst_9 : Module S M] [inst_10 : Module S N] [inst_11 : Module S P]
  [inst_12 : IsScalarTower S R M] [inst_13 : IsScalarTower S R N] [inst_14 : IsScalarTower S R P]
  [inst_15 : AddCommMonoid M'] [inst_16 : Module S M'] [inst_17 : AddCommMonoid N'] [inst_18 : Module S N']
  [inst_19 : AddCommMonoid P'] [inst_20 : Module S P'] [inst_21 : SMulCommClass R S P] (i : M' →ₗ[S] M) (j : N' →ₗ[S] N)
  (k : P' →ₗ[S] P) (hk : Function.Injective ⇑k) (B : M →ₗ[R] N →ₗ[R] P)
  (hB : ∀ (m : M') (n : N'), (B (i m)) (j n) ∈ k.range) (m : M') (n : N') (p : P'),
  p = ((i.restrictScalarsRange₂ j k hk B hB) m) n ↔ k p = (B (i m)) (j n)
-- Init.Data.UInt.Bitwise
UInt64.toFin_and : ∀ (a b : UInt64), (a &&& b).toFin = a.toFin &&& b.toFin
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.Option.dmap_none : ∀ {α : Type u} {β : Type v} (f : (a : α) → none = some a → β), Std.Internal.List.Option.dmap✝ none f = none
-- Mathlib.RepresentationTheory.Continuous.TopRep
TopRep.comp_apply : ∀ {k : Type u} {G : Type v} [inst : TopologicalSpace k] [inst_1 : Ring k] [inst_2 : Monoid G] {A B C : TopRep k G}
  (f : A ⟶ B) (g : B ⟶ C) (a : ↑A),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) a =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) a)
-- Mathlib.Data.NNReal.Defs
NNReal.mul_eq_mul_left : ∀ {a b c : NNReal}, a ≠ 0 → (a * b = a * c ↔ b = c)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_insert!_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} {fallback v : β},
      Std.DTreeMap.Internal.Impl.Const.getD (Std.DTreeMap.Internal.Impl.insert! k v t) k fallback = v
-- Mathlib.Order.JordanHolder
JordanHolderLattice.second_iso_of_eq : ∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] {x y a b : X},
  JordanHolderLattice.IsMaximal x a → x ⊔ y = a → x ⊓ y = b → JordanHolderLattice.Iso (x, a) (b, y)
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile.0.Std.Iterators.Types.TakeWhile.instIterator.match_1.eq_1 : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {P : β → Std.Iterators.PostconditionT m (ULift.{u_1, 0} Bool)} (out : β)
  (motive : Subtype (P out).Property → Sort u_3) (h' : (P out).Property { down := true })
  (h_1 : (h' : (P out).Property { down := true }) → motive ⟨{ down := true }, h'⟩)
  (h_2 : (h' : (P out).Property { down := false }) → motive ⟨{ down := false }, h'⟩),
  (match ⟨{ down := true }, h'⟩ with
    | ⟨{ down := true }, h'⟩ => h_1 h'
    | ⟨{ down := false }, h'⟩ => h_2 h') =
    h_1 h'
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Path.insert.eq_2 : ∀ {α : Type u_1} (path : RBTree.RBNode.Path α) (v : α) (c : RBTree.RBColor) (l : RBTree.RBNode α) (v_1 : α)
  (r : RBTree.RBNode α), path.insert (RBTree.RBNode.node c l v_1 r) v = path.fill (RBTree.RBNode.node c l v r)
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_natCast_mul_add' : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℕ), toIcoMod hp (↑m * p + a) b = ↑m * p + toIcoMod hp a b
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.DelayedTheoremInstance.proof : Lean.Meta.Grind.DelayedTheoremInstance → Lean.Expr
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Option γ} {k : α} {h' : k ∈ Std.HashMap.filterMap f m},
  (Std.HashMap.filterMap f m).getKey k h' = m.getKey k ⋯
-- Mathlib.CategoryTheory.Iso
CategoryTheory.IsIso.mono_of_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : Y ⟶ X) [CategoryTheory.IsIso f],
  CategoryTheory.Mono f
-- Mathlib.Algebra.MonoidAlgebra.Defs
_private.Mathlib.Algebra.MonoidAlgebra.Defs.0.MonoidAlgebra.instSMulUnits : {M : Type u_4} → {α : Type u_9} → [inst : Monoid M] → [SMul M α] → SMul Mˣ α
-- Std.Internal.Do.ExceptPost
/-- Extract a head ordering from an `EPost.Cons` ordering.  -/
Std.Internal.Do.EPost.Cons.le_head : ∀ {eh : Type u_1} {et : Type u_2} [inst : Lean.Order.PartialOrder eh] [inst_1 : Lean.Order.PartialOrder et]
  {p q : EPost.Cons✝ eh et}, Lean.Order.PartialOrder.rel p q → Lean.Order.PartialOrder.rel p.head q.head
-- Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
/-- A bicategory is locally discrete if the categories of 1-morphisms are discrete.  -/
CategoryTheory.Bicategory.IsLocallyDiscrete : (B : Type u_1) → [CategoryTheory.Bicategory B] → Prop
-- Init.Data.BitVec.Lemmas
BitVec.ofBoolListBE.eq_def : ∀ (x : List Bool),
  BitVec.ofBoolListBE x =
    match x with
    | [] => 0#0
    | b :: bs => BitVec.cons b (BitVec.ofBoolListBE bs)
-- Mathlib.Data.Seq.Basic
Stream'.Seq.getElem?_toList : ∀ {α : Type u} (s : Stream'.Seq α) (h : s.Terminates) (n : ℕ), (s.toList h)[n]? = s.get? n
-- Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
DomAddAct.instVAddSubtypeAEEqFunMemAddAddSubgroupLp.eq_1 : ∀ {M : Type u_1} {α : Type u_3} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure α} {p : ENNReal} [inst_2 : VAdd M α] [inst_3 : MeasureTheory.VAddInvariantMeasure M α μ]
  [inst_4 : MeasurableConstVAdd M α],
  DomAddAct.instVAddSubtypeAEEqFunMemAddAddSubgroupLp =
    { vadd := fun c f => (MeasureTheory.Lp.compMeasurePreserving (fun x => DomAddAct.mk.symm c +ᵥ x) ⋯) f }
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.normalCore_eq_self : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) [H.Normal], H.normalCore = H
-- Mathlib.Topology.Sheaves.LocalPredicate
TopCat.PrelocalPredicate.mk.injEq : ∀ {X : TopCat} {T : ↑X → Type u_1} (pred : {U : TopologicalSpace.Opens ↑X} → ((x : ↥U) → T ↑x) → Prop)
  (res : ∀ {U V : TopologicalSpace.Opens ↑X} (i : U ⟶ V) (f : (x : ↥V) → T ↑x), pred f → pred fun x => f (i x))
  (pred_1 : {U : TopologicalSpace.Opens ↑X} → ((x : ↥U) → T ↑x) → Prop)
  (res_1 : ∀ {U V : TopologicalSpace.Opens ↑X} (i : U ⟶ V) (f : (x : ↥V) → T ↑x), pred_1 f → pred_1 fun x => f (i x)),
  ({ pred := pred, res := res } = { pred := pred_1, res := res_1 }) = (pred = pred_1)
-- Std.Data.DTreeMap.Raw.Basic
/-- Retrieves the key-value pair, whose key matches `a`. Ensures that such a mapping exists by requiring a proof of `a ∈ m`. The key in the returned pair will be `BEq` to the input `a`.
 -/
Std.DTreeMap.Raw.getEntry : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → [Std.LawfulEqCmp cmp] → (t : Std.DTreeMap.Raw α β cmp) → (a : α) → a ∈ t → (a : α) × β a
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.contains_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [inst : BEq α] [Std.LawfulBEqCmp cmp]
  [Std.TransCmp cmp], t.WF → ∀ {k : α}, t.toArray.contains k = t.contains k
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.empty_smul : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {t : Set β}, ∅ • t = ∅
-- Mathlib.Algebra.Module.LinearMap.End
Module.End.commute_pow_left_of_commute : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Semiring R₂] [inst_4 : AddCommMonoid M₂] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  {f : M →ₛₗ[σ₁₂] M₂} {g : Module.End R M} {g₂ : Module.End R₂ M₂},
  g₂ ∘ₛₗ f = f ∘ₛₗ g → ∀ (k : ℕ), (g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g ^ k)
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.conductor_one_dvd : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] (n : ℕ), DirichletCharacter.conductor 1 ∣ n
-- Mathlib.Analysis.InnerProductSpace.PiL2
unitary.eq_1 : ∀ (R : Type u_1) [inst : Monoid R] [inst_1 : StarMul R],
  unitary R = { carrier := {U | star U * U = 1 ∧ U * star U = 1}, mul_mem' := ⋯, one_mem' := ⋯ }
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.normal_iInf_normal : ∀ {G : Type u_1} [inst : AddGroup G] {ι : Sort u_6} {a : ι → AddSubgroup G}, (∀ (i : ι), (a i).Normal) → (iInf a).Normal
-- Mathlib.Topology.MetricSpace.Contracting
ContractingWith.efixedPoint_isFixedPt : ∀ {α : Type u_1} [inst : EMetricSpace α] {K : NNReal} {f : α → α} [inst_1 : CompleteSpace α] (hf : ContractingWith K f)
  {x : α} (hx : edist x (f x) ≠ ⊤), Function.IsFixedPt f (ContractingWith.efixedPoint f hf x hx)
-- Mathlib.Topology.Covering.Quotient
IsQuotientCoveringMap.toPermFiber_apply_apply_coe : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {G : Type u_3}
  [inst_2 : Group G] [inst_3 : MulAction G E] (hf : IsQuotientCoveringMap f G) (x : X) (a : G) (x_1 : ↑(f ⁻¹' {x})),
  ↑(((hf.toPermFiber x) a) x_1) = a • ↑x_1
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instAddCommGroup : {α : Type u_1} → [AddCommGroup α] → AddCommGroup (Colex α)
-- Mathlib.RingTheory.Localization.Finiteness
/-- If there exists a finite set `{ r }` of `R` that generates the unit ideal and such that `Mᵣ` is
`Rᵣ`-finite for each `r`, then `M` is a finite `R`-module.

General version for any modules `Mᵣ` and rings `Rᵣ` satisfying the correct universal properties.
See `Module.Finite.of_localizationSpan_finite` for the specialized version.

See `of_localizationSpan'` for a version without the finite set assumption.
 -/
Module.Finite.of_localizationSpan_finite' : ∀ {R : Type u} [inst : CommSemiring R] {M : Type w} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (t : Finset R),
  Ideal.span ↑t = ⊤ →
    ∀ {Mₚ : ↥t → Type u_1} [inst_3 : (g : ↥t) → AddCommMonoid (Mₚ g)] [inst_4 : (g : ↥t) → Module R (Mₚ g)]
      {Rₚ : ↥t → Type u_2} [inst_5 : (g : ↥t) → CommSemiring (Rₚ g)] [inst_6 : (g : ↥t) → Algebra R (Rₚ g)]
      [∀ (g : ↥t), IsLocalization.Away (↑g) (Rₚ g)] [inst_8 : (g : ↥t) → Module (Rₚ g) (Mₚ g)]
      [∀ (g : ↥t), IsScalarTower R (Rₚ g) (Mₚ g)] (f : (g : ↥t) → M →ₗ[R] Mₚ g)
      [∀ (g : ↥t), IsLocalizedModule.Away (↑g) (f g)], (∀ (g : ↥t), Module.Finite (Rₚ g) (Mₚ g)) → Module.Finite R M
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.delabSeqLeft : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Analysis.Calculus.TangentCone.Real
uniqueDiffOn_Ioo : ∀ (a b : ℝ), UniqueDiffOn ℝ (Set.Ioo a b)
-- Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.Modification.vcomp_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} {η θ ι : F ⟶ G}
  (Γ : CategoryTheory.Pseudofunctor.StrongTrans.Modification η θ)
  (Δ : CategoryTheory.Pseudofunctor.StrongTrans.Modification θ ι) (a : B),
  (Γ.vcomp Δ).app a = CategoryTheory.CategoryStruct.comp (Γ.app a) (Δ.app a)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Subtracting the second vector passed to `oangle` from a multiple of the first vector negates
the sign of the angle.  -/
Orientation.oangle_sign_smul_sub_right : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x y : V) (r : ℝ), (o.oangle x (r • x - y)).sign = -(o.oangle x y).sign
-- Mathlib.Topology.Connected.PathConnected
mem_pathComponentIn_self : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x : X} {F : Set X}, x ∈ F → x ∈ pathComponentIn F x