mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
_private.Mathlib.Algebra.BigOperators.Group.Finset.Defs.0.BigOperators.FinsetResult.Ici.injEq : ∀ (n n_1 : Lean.Term), (BigOperators.FinsetResult.Ici✝ n = BigOperators.FinsetResult.Ici✝ n_1) = (n = n_1)
-- Mathlib.Data.Fintype.Defs
List.instDecidableInjOnCoeFinsetOfDecidableEq : {α : Type u_1} → {β : Type u_2} → {f : α → β} → {s : Finset α} → [DecidableEq β] → Decidable (Set.InjOn f ↑s)
-- Mathlib.AlgebraicTopology.DoldKan.Degeneracies
AlgebraicTopology.DoldKan.degeneracy_comp_PInfty_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (X : CategoryTheory.SimplicialObject C) (n : ℕ) {Δ' : SimplexCategory} (θ : { len := n } ⟶ Δ'),
  ¬CategoryTheory.Mono θ →
    ∀ {Z : C} (h : X.obj (Opposite.op { len := n }) ⟶ Z),
      CategoryTheory.CategoryStruct.comp (X.map θ.op)
          (CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f n) h) =
        CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
/-- If `f,g` is a kernel pair for some morphism `q`, then it is reflexive.  -/
CategoryTheory.IsKernelPair.isReflexivePair : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B R : C} {f g : R ⟶ A} {q : A ⟶ B},
  CategoryTheory.IsKernelPair q f g → CategoryTheory.IsReflexivePair f g
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
/-- `coprod F G` is a binary coproduct for `F` and `G`.  -/
CategoryTheory.FunctorToTypes.binaryCoproductColimitCocone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F G : CategoryTheory.Functor C (Type w)) → CategoryTheory.Limits.ColimitCocone (CategoryTheory.Limits.pair F G)
-- Mathlib.Analysis.SpecialFunctions.Pochhammer
/-- `descPochhammer 𝕜 n` is continuous.  -/
continuous_descPochhammer_eval : ∀ {n : ℕ} {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜], Continuous fun x => Polynomial.eval x (descPochhammer 𝕜 n)
-- Mathlib.CategoryTheory.FiberedCategory.Fibered
CategoryTheory.Functor.IsPreFibered.pullbackObj_proj : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  {p : CategoryTheory.Functor 𝒳 𝒮} [inst_2 : p.IsPreFibered] {R S : 𝒮} {a : 𝒳} (ha : p.obj a = S) (f : R ⟶ S),
  p.obj (CategoryTheory.Functor.IsPreFibered.pullbackObj ha f) = R
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.bounded : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [IsAbsoluteValue abv] (f : CauSeq β abv), ∃ r, ∀ (i : ℕ), abv (↑f i) < r
-- Mathlib.Tactic.Tauto
Mathlib.Tactic.Tauto.Config.mk : Mathlib.Tactic.Tauto.Config
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.JordanDecomposition.real_smul_posPart_neg : ∀ {α : Type u_1} [inst : MeasurableSpace α] (j : MeasureTheory.JordanDecomposition α),
  ∀ r < 0, (r • j).posPart = (-r).toNNReal • j.negPart
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.IsSheafFor.amalgamate.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {R : CategoryTheory.Presieve X} (t : CategoryTheory.Presieve.IsSheafFor P R)
  (x x_1 : CategoryTheory.Presieve.FamilyOfElements P R) (e_x : x = x_1) (hx : x.Compatible),
  t.amalgamate x hx = t.amalgamate x_1 ⋯
-- Mathlib.Algebra.Algebra.Equiv
/-- **Alias** of `AlgEquiv.coe_ringEquiv`. -/
AlgEquiv.coe_ringEquiv' : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂), ⇑e.toRingEquiv = ⇑e
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.forM_eq_forM_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m]
  {f : α → m PUnit.{w + 1}}, forM t f = Array.forM f t.toArray
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey_eraseKey_eq_of_beq_maxKey_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] [inst_2 : BEq α] [inst_3 : Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {k : α}
  {he : (Std.Internal.List.eraseKey k l).isEmpty = false},
  (k == Std.Internal.List.maxKey l ⋯) = false →
    Std.Internal.List.maxKey (Std.Internal.List.eraseKey k l) he = Std.Internal.List.maxKey l ⋯
-- Mathlib.Topology.NhdsWithin
nhdsWithin_univ : ∀ {α : Type u_1} [inst : TopologicalSpace α] (a : α), nhdsWithin a Set.univ = nhds a
-- Mathlib.FieldTheory.Finite.Polynomial
/-- Evaluation in the `MvPolynomial.R` subtype.  -/
MvPolynomial.evalᵢ : (σ K : Type u) → [inst : Fintype K] → [inst_1 : CommRing K] → MvPolynomial.R σ K →ₗ[K] (σ → K) → K
-- Lean.Meta.Injective
_private.Lean.Meta.Injective.0.Lean.Meta.MkHInjTypeResult.numIndices : Lean.Meta.MkHInjTypeResult✝ → ℕ
-- Mathlib.Topology.UniformSpace.Defs
UniformSpace.ball_inter_left : ∀ {β : Type ub} (x : β) (V W : Set (β × β)), UniformSpace.ball x (V ∩ W) ⊆ UniformSpace.ball x V
-- Mathlib.CategoryTheory.Functor.Derived.Adjunction
/-- The unit of the derived adjunction, see `Adjunction.derived`.  -/
CategoryTheory.Adjunction.derivedη : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D₁ : Type u_3} →
      {D₂ : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] →
                {G : CategoryTheory.Functor C₁ C₂} →
                  {F : CategoryTheory.Functor C₂ C₁} →
                    (G ⊣ F) →
                      {L₁ : CategoryTheory.Functor C₁ D₁} →
                        {L₂ : CategoryTheory.Functor C₂ D₂} →
                          (W₁ : CategoryTheory.MorphismProperty C₁) →
                            [inst_4 : L₁.IsLocalization W₁] →
                              {G' : CategoryTheory.Functor D₁ D₂} →
                                {F' : CategoryTheory.Functor D₂ D₁} →
                                  (α : L₁.comp G' ⟶ G.comp L₂) →
                                    (F.comp L₁ ⟶ L₂.comp F') →
                                      [(G'.comp F').IsLeftDerivedFunctor
                                            (CategoryTheory.CategoryStruct.comp (L₁.associator G' F').inv
                                              (CategoryTheory.Functor.whiskerRight α F'))
                                            W₁] →
                                        CategoryTheory.Functor.id D₁ ⟶ G'.comp F'
-- Mathlib.Data.Finset.Sups
Finset.disjSups_inter_subset_right : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] [inst_2 : OrderBot α]
  [inst_3 : DecidableRel Disjoint] {s t₁ t₂ : Finset α}, s.disjSups (t₁ ∩ t₂) ⊆ s.disjSups t₁ ∩ s.disjSups t₂
-- Mathlib.LinearAlgebra.Pi
LinearEquiv.finTwoArrow_symm_apply : ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  ⇑(LinearEquiv.finTwoArrow R M).symm = fun x => ![x.1, x.2]
-- Mathlib.Analysis.Normed.Affine.Isometry
LinearIsometry.toAffineIsometry_linearIsometry : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : SeminormedAddCommGroup V₂] [inst_4 : NormedSpace 𝕜 V₂] (f : V →ₗᵢ[𝕜] V₂),
  f.toAffineIsometry.linearIsometry = f
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.instDecidableEq_1 : {ι : Type u_1} →
  {M : ι → Type u_2} →
    [inst : (i : ι) → Monoid (M i)] → [DecidableEq ι] → [(i : ι) → DecidableEq (M i)] → DecidableEq (Monoid.CoprodI M)
-- Init.Data.Range.Polymorphic.BitVec
BitVec.instLawfulUpwardEnumerableLT : ∀ {n : ℕ}, Std.PRange.LawfulUpwardEnumerableLT (BitVec n)
-- Plausible.Testable
Plausible.Testable.instInhabitedOptionTOfPure : {α : Type u} → {m : Type u → Type u_1} → [Pure m] → Inhabited (OptionT m α)
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.exists_walk_of_edist_eq_coe : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V} {k : ℕ}, G.edist u v = ↑k → ∃ p, p.length = k
-- Mathlib.CategoryTheory.NatIso
/-- Constructor for a functor that is isomorphic to a given functor `F : C ⥤ D`,
while being definitionally equal on objects to a given map `obj : C → D`
such that for all `X : C`, we have an isomorphism `F.obj X ≅ obj X`.  -/
CategoryTheory.Functor.copyObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) → (obj : C → D) → ((X : C) → F.obj X ≅ obj X) → CategoryTheory.Functor C D
-- Mathlib.Topology.Instances.Real.Lemmas
Real.uniformContinuous_abs : UniformContinuous abs
-- Mathlib.Topology.Algebra.ProperAction.Basic
/-- The action `Gᵃᵒᵖ ↷ G` by right translations is proper.  -/
instProperVAddAddOppositeOfIsTopologicalAddGroup : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G], ProperVAdd Gᵃᵒᵖ G
-- Mathlib.Order.Category.BddOrd
/-- The underlying object in the category of partial orders.  -/
BddOrd.toPartOrd : BddOrd → PartOrd
-- Mathlib.Order.Category.PartOrdEmb
/-- The category of partial orders.  -/
PartOrdEmb : Type (u_1 + 1)
-- Mathlib.Order.Heyting.Boundary
Coheyting.boundary.eq_1 : ∀ {α : Type u_1} [inst : CoheytingAlgebra α] (a : α), Coheyting.boundary a = a ⊓ ￢a
-- Mathlib.Data.NNRat.Defs
NNRat.forall : ∀ {p : ℚ≥0 → Prop}, (∀ (q : ℚ≥0), p q) ↔ ∀ (q : ℚ) (hq : 0 ≤ q), p ⟨q, hq⟩
-- Init.Data.String.Decode
ByteArray.lt_size_of_isSome_utf8DecodeChar? : ∀ {b : ByteArray} {i : ℕ}, (b.utf8DecodeChar? i).isSome = true → i < b.size
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
IsSelfAdjoint.exp_nonneg : ∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : NormedAlgebra ℝ A]
  [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_4 : PartialOrder A] [StarOrderedRing A] {a : A},
  IsSelfAdjoint a → 0 ≤ NormedSpace.exp a
-- Mathlib.Geometry.Euclidean.SignedDist
AffineSubspace.signedInfDist_apply_self : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (s : AffineSubspace ℝ P) [inst_4 : Nonempty ↥s]
  [inst_5 : s.direction.HasOrthogonalProjection] (p : P),
  (s.signedInfDist p) p = ‖p -ᵥ ↑((EuclideanGeometry.orthogonalProjection s) p)‖
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.toContinuousAddMonoidHom_inj : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] {f g : M₁ →SL[σ₁₂] M₂}, ↑f = ↑g ↔ f = g
-- Init.Data.SInt.Basic
Int64.toBitVec.inj : ∀ {x y : Int64}, x.toBitVec = y.toBitVec → x = y
-- Mathlib.Algebra.Group.Defs
IsAddTorsionFree.mk : ∀ {M : Type u_2} [inst : AddMonoid M], (∀ ⦃n : ℕ⦄, n ≠ 0 → Function.Injective fun a => n • a) → IsAddTorsionFree M
-- Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
CliffordAlgebraComplex.equiv_apply : ∀ (a : CliffordAlgebra CliffordAlgebraComplex.Q), CliffordAlgebraComplex.equiv a = CliffordAlgebraComplex.toComplex a
-- Mathlib.NumberTheory.Dioph
_private.Mathlib.NumberTheory.Dioph.0.Poly.sumsq.match_1.splitter : {α : Type u_1} →
  (motive : List (Poly α) → Sort u_2) →
    (x : List (Poly α)) → (Unit → motive []) → ((p : Poly α) → (ps : List (Poly α)) → motive (p :: ps)) → motive x
-- Mathlib.MeasureTheory.Measure.AEMeasurable
AEMeasurable.indicator : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β}
  {μ : MeasureTheory.Measure α} [inst_1 : Zero β],
  AEMeasurable f μ → ∀ {s : Set α}, MeasurableSet s → AEMeasurable (s.indicator f) μ
-- Mathlib.Order.Comparable
AntisymmRel.incompRel_congr_left : ∀ {α : Type u_1} {a b c : α} [inst : Preorder α],
  AntisymmRel (fun x1 x2 => x1 ≤ x2) a b → (IncompRel (fun x1 x2 => x1 ≤ x2) a c ↔ IncompRel (fun x1 x2 => x1 ≤ x2) b c)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.WalkingMultispan.inclusionOfLinearOrder_obj : ∀ (ι : Type w) [inst : LinearOrder ι]
  (x : CategoryTheory.Limits.WalkingMultispan (CategoryTheory.Limits.MultispanShape.ofLinearOrder ι)),
  (CategoryTheory.Limits.WalkingMultispan.inclusionOfLinearOrder ι).obj x =
    match x with
    | CategoryTheory.Limits.WalkingMultispan.left a => CategoryTheory.Limits.WalkingMultispan.left ↑a
    | CategoryTheory.Limits.WalkingMultispan.right b => CategoryTheory.Limits.WalkingMultispan.right b
-- Mathlib.Data.Ordmap.Ordnode
/-- An `Ordnode α` is a finite set of values, represented as a tree.
The operations on this type maintain that the tree is balanced
and correctly stores subtree sizes at each level.

This is a copy of `BinaryTree` with a cached `size` field for `BinaryTree.numNodes`.  -/
Ordnode : Type u → Type u
-- Mathlib.Algebra.Homology.Embedding.Extend
HomologicalComplex.extend.d_none_eq_zero : ∀ {ι : Type u_1} {c : ComplexShape ι} {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_3} C]
  [inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c) (i j : Option ι), i = none → HomologicalComplex.extend.d K i j = 0
-- Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Mathlib.Tactic.Monoidal.evalWhiskerLeft_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {f g : C}
  {η : f ⟶ g}
  {η₁ : f ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) g}
  {η₂ :
    CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) f ⟶
      CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) g},
  CategoryTheory.CategoryStruct.comp η (CategoryTheory.MonoidalCategoryStruct.leftUnitor g).inv = η₁ →
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor f).hom η₁ = η₂ →
      CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) η = η₂
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.lt_iterate_pos_iff : ∀ (f : CircleDeg1Lift) {x : ℝ} {m : ℤ} {n : ℕ}, 0 < n → (x + ↑n * ↑m < (⇑f)^[n] x ↔ x + ↑m < f x)
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.erase_eq_eraseₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α),
  m.erase a = m.eraseₘ a
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.prod_const_one : ∀ {ι : Type u_1} {M : Type u_3} {s : Finset ι} [inst : CommMonoid M], ∏ _x ∈ s, 1 = 1
-- Mathlib.Data.List.Sort
/-- **Alias** of the forward direction of `List.sortedGT_iff_strictAnti_get`. -/
List.SortedGT.strictAnti_get : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], l.SortedGT → StrictAnti l.get
-- Mathlib.CategoryTheory.Category.ULift
CategoryTheory.AsSmall.up_obj_down : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C), (CategoryTheory.AsSmall.up.obj X).down = X
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
lineDerivWithin_zero_of_not_lineDifferentiableWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {f : E → F} {s : Set E}
  {x v : E}, ¬LineDifferentiableWithinAt 𝕜 f s x v → lineDerivWithin 𝕜 f s x v = 0
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getD_filter : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α]
  {f : (a : α) → β a → Bool} {k : α} {fallback : β k},
  (Std.DHashMap.filter f m).getD k fallback = (Option.filter (f k) (m.get? k)).getD fallback
-- Mathlib.GroupTheory.GroupAction.Hom
/-- Equivariant ring homomorphisms.  -/
MulSemiringActionHom : {M : Type u_1} →
  [inst : Monoid M] →
    {N : Type u_2} →
      [inst_1 : Monoid N] →
        (M →* N) →
          (R : Type u_10) →
            [inst_2 : Semiring R] →
              [MulSemiringAction M R] →
                (S : Type u_12) → [inst : Semiring S] → [MulSemiringAction N S] → Type (max u_10 u_12)
-- Mathlib.Algebra.Lie.OfAssociative
/-- A representation of an associative algebra `A` is also a representation of `A`, regarded as a
Lie algebra via the ring commutator.

See the comment at `LieRingModule.ofAssociativeModule` for why the possibility `M = A` means
this cannot be a global instance.  -/
LieModule.ofAssociativeModule : ∀ {A : Type v} [inst : Ring A] {R : Type u} [inst_1 : CommRing R] [inst_2 : Algebra R A] {M : Type w}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module A M] [IsScalarTower R A M], LieModule R A M
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
MulOpposite.unop_finsuppSum : ∀ {ι : Type u_16} {M : Type u_17} {N : Type u_18} [inst : AddCommMonoid M] [inst_1 : Zero N] (f : ι →₀ N)
  (g : ι → N → Mᵐᵒᵖ), MulOpposite.unop (f.sum g) = f.sum fun i n => MulOpposite.unop (g i n)
-- Mathlib.Topology.Basic
IsOpen.sdiff : ∀ {X : Type u} {s t : Set X} [inst : TopologicalSpace X], IsOpen s → IsClosed t → IsOpen (s \ t)
-- Mathlib.Probability.HasLaw
ProbabilityTheory.HasLaw.covariance_fun_comp : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {X : Ω → 𝓧}
  {μ : MeasureTheory.Measure 𝓧} {P : MeasureTheory.Measure Ω},
  ProbabilityTheory.HasLaw X μ P →
    ∀ {f g : 𝓧 → ℝ},
      AEMeasurable f μ →
        AEMeasurable g μ →
          ProbabilityTheory.covariance (fun ω => f (X ω)) (fun ω => g (X ω)) P = ProbabilityTheory.covariance f g μ
-- Init.Data.UInt.Bitwise
UInt32.and_le_left : ∀ {a b : UInt32}, a &&& b ≤ a
-- Mathlib.Algebra.Lie.Submodule
/-- The kernel of a morphism of Lie algebras, as an ideal in the domain.  -/
LieModuleHom.ker : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      {N : Type w₁} →
        [inst : CommRing R] →
          [inst_1 : LieRing L] →
            [inst_2 : AddCommGroup M] →
              [inst_3 : Module R M] →
                [inst_4 : LieRingModule L M] →
                  [inst_5 : AddCommGroup N] →
                    [inst_6 : Module R N] → [inst_7 : LieRingModule L N] → (M →ₗ⁅R,L⁆ N) → LieSubmodule R L M
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.pi_liftQ_eq_liftQ_pi : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_5}
  {N : ι → Type u_6} [inst_3 : (i : ι) → AddCommGroup (N i)] [inst_4 : (i : ι) → Module R (N i)]
  (f : (i : ι) → M →ₗ[R] N i) {p : Submodule R M} (h : ∀ (i : ι), p ≤ (f i).ker),
  (LinearMap.pi fun i => p.liftQ (f i) ⋯) = p.liftQ (LinearMap.pi f) ⋯
-- Lean.Meta.Tactic.Grind.Arith.Linear.StructId
_private.Lean.Meta.Tactic.Grind.Arith.Linear.StructId.0.Lean.Meta.Grind.Arith.Linear.getStructId?.go? : Lean.Expr → Lean.Meta.Grind.GoalM (Option ℕ)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DeclarationParams.mk.sizeOf_spec : ∀ (toTextDocumentPositionParams : Lean.Lsp.TextDocumentPositionParams),
  sizeOf { toTextDocumentPositionParams := toTextDocumentPositionParams } = 1 + sizeOf toTextDocumentPositionParams
-- Mathlib.Combinatorics.SimpleGraph.Sum
SimpleGraph.Colorable.of_sum_right : ∀ {V : Type u_3} {W : Type u_5} {G : SimpleGraph V} {H : SimpleGraph W} {n : ℕ}, (G ⊕g H).Colorable n → H.Colorable n
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.C_neg_two : ∀ (R : Type u_1) [inst : CommRing R], Polynomial.Chebyshev.C R (-2) = Polynomial.X ^ 2 - 2
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.get!_inter_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  [inst_1 : Inhabited β], k ∉ t₂ → (t₁ ∩ t₂).get! k = default
-- Lean.MetavarContext
Lean.MetavarContext.MkBindingM.Context.mk.injEq : ∀ (quotContext : Lean.Name) (lctx : Lean.LocalContext) (quotContext_1 : Lean.Name) (lctx_1 : Lean.LocalContext),
  ({ quotContext := quotContext, lctx := lctx } = { quotContext := quotContext_1, lctx := lctx_1 }) =
    (quotContext = quotContext_1 ∧ lctx = lctx_1)
-- Mathlib.Combinatorics.SetFamily.Intersecting
/-- An `L`-intersecting family is also `L'`-intersecting whenever `L ⊆ L'`.
 -/
Set.IsIntersectingOf.mono : ∀ {L L' : Set ℕ} {α : Type u_1} [inst : DecidableEq α] {𝒜 : Set (Finset α)},
  L ⊆ L' → L.IsIntersectingOf 𝒜 → L'.IsIntersectingOf 𝒜
-- ProofWidgets.Component.RefreshComponent
/-- Displays a HTML tree, refreshing the display when the tree is updated.

Use `mkRefreshComponentM` to conveniently spawn a dedicated thread
from which you can update the display.

The component resets its state when rendered with a new `props.state`.
Conversely, reusing `props.state` preserves the client-side state.   -/
ProofWidgets.RefreshComponent : ProofWidgets.Component ProofWidgets.RefreshComponent.Props
-- Lean.Data.Lsp.Internal
/-- End line of selection range.  -/
Lean.Lsp.DeclInfo.selectionRangeEndPosLine : Lean.Lsp.DeclInfo → ℕ
-- Mathlib.CategoryTheory.DifferentialObject
/-- The morphism between underlying objects of the two differentiable objects.  -/
CategoryTheory.DifferentialObject.Hom.f : {S : Type u_1} →
  [inst : AddMonoidWithOne S] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.HasShift C S] →
            {X Y : CategoryTheory.DifferentialObject S C} → X.Hom Y → (X.obj ⟶ Y.obj)
-- Init.Data.Ord.Basic
compareOfLessAndEq_eq_lt : ∀ {α : Type u} [inst : LT α] [LE α] [inst_2 : DecidableLT α] [inst_3 : DecidableEq α] {x y : α},
  compareOfLessAndEq x y = Ordering.lt ↔ x < y
-- Batteries.Data.String.Lemmas
String.Pos.Raw.utf8GetAux?.eq_def : ∀ (x : List Char) (x_1 x_2 : String.Pos.Raw),
  String.Pos.Raw.utf8GetAux? x x_1 x_2 =
    match x, x_1, x_2 with
    | [], x, x_3 => none
    | c :: cs, i, p => if i = p then some c else String.Pos.Raw.utf8GetAux? cs (i + c) p
-- Mathlib.Analysis.Complex.Trigonometric
Complex.sinh.eq_1 : ∀ (z : ℂ), Complex.sinh z = (Complex.exp z - Complex.exp (-z)) / 2
-- Mathlib.RingTheory.Norm.Transitivity
Algebra.norm_eq_prod_roots : ∀ {L : Type u_6} {K : Type u_7} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (F : Type u_8)
  [inst_3 : Field F] [inst_4 : Algebra K F] {x : L},
  (Polynomial.map (algebraMap K F) (minpoly K x)).Splits →
    (algebraMap K F) ((Algebra.norm K) x) = ((minpoly K x).aroots F).prod ^ Module.finrank (↥K⟮x⟯) L
-- Mathlib.Algebra.AddConstMap.Equiv
AddConstEquiv.ext : ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H} {e₁ e₂ : AddConstEquiv G H a b},
  (∀ (x : G), e₁ x = e₂ x) → e₁ = e₂
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
CategoryTheory.Limits.equalizerPullbackMapIso_inv_ι_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasEqualizers C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] {X Y S T : C} {f g : X ⟶ Y} {s : X ⟶ S} {t : Y ⟶ S}
  (hf : CategoryTheory.CategoryStruct.comp f t = s) (hg : CategoryTheory.CategoryStruct.comp g t = s) (v : T ⟶ S)
  {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizerPullbackMapIso hf hg v).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.equalizer.ι
          (CategoryTheory.Limits.pullback.map s v t v f (CategoryTheory.CategoryStruct.id T)
            (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)
          (CategoryTheory.Limits.pullback.map s v t v g (CategoryTheory.CategoryStruct.id T)
            (CategoryTheory.CategoryStruct.id S) ⋯ ⋯))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst s v) h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.equalizer.ι f g)
        (CategoryTheory.Limits.pullback.fst s v))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizer.ι f g) h)