mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.SmallObject.Construction
/-- The canonical morphism `∐ (functorObjSrcFamily f πX) ⟶ ∐ (functorObjSrcFamily f πY)`
induced by a morphism `Arrow.mk πX ⟶ Arrow.mk πY`.  -/
CategoryTheory.SmallObject.functorMapSrc : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {I : Type w} →
      {A B : I → C} →
        (f : (i : I) → A i ⟶ B i) →
          {S T X Y : C} →
            {πX : X ⟶ S} →
              {πY : Y ⟶ T} →
                (CategoryTheory.Arrow.mk πX ⟶ CategoryTheory.Arrow.mk πY) →
                  [inst_1 :
                      CategoryTheory.Limits.HasColimitsOfShape
                        (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] →
                    [inst_2 :
                        CategoryTheory.Limits.HasColimitsOfShape
                          (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πY)) C] →
                      ∐ CategoryTheory.SmallObject.functorObjSrcFamily f πX ⟶
                        ∐ CategoryTheory.SmallObject.functorObjSrcFamily f πY
-- Mathlib.Topology.Constructions.SumProd
continuous_inl : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y], Continuous Sum.inl
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
/-- Negative part of a function in `L^p`.  -/
MeasureTheory.Lp.negPart : {α : Type u_1} →
  {m : MeasurableSpace α} →
    {p : ENNReal} → {μ : MeasureTheory.Measure α} → ↥(MeasureTheory.Lp ℝ p μ) → ↥(MeasureTheory.Lp ℝ p μ)
-- Mathlib.Order.Filter.Bases.Basic
/-- If `{s i | p i}` is a basis of a filter `l` and `V ∈ l`, then `{s i | p i ∧ s i ⊆ V}`
is a basis of `l`.  -/
Filter.HasBasis.restrict_subset : ∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
  l.HasBasis p s → ∀ {V : Set α}, V ∈ l → l.HasBasis (fun i => p i ∧ s i ⊆ V) s
-- Mathlib.Algebra.Group.Basic
zpow_natCast_sub_one : ∀ {G : Type u_3} [inst : Group G] (a : G) (n : ℕ), a ^ (↑n - 1) = a ^ n / a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_union : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [inst : Inhabited α]
  [Std.TransOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α}, (m₁.union m₂ ⋯ ⋯).getKey! k = m₂.getKeyD k (m₁.getKey! k)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
MulLECancellable.mul_le_mul_iff_left : ∀ {α : Type u_1} [inst : LE α] [inst_1 : Mul α] [MulLeftMono α] {a b c : α},
  MulLECancellable a → (a * b ≤ a * c ↔ b ≤ c)
-- Mathlib.Data.PNat.Basic
PNat.coeAddHom_apply : ∀ (a : ℕ+), PNat.coeAddHom a = ↑a
-- Std.Data.ExtDHashMap.Basic
/-- Returns `true` if there is a mapping for the given key. There is also a `Prop`-valued version
of this: `a ∈ m` is equivalent to `m.contains a = true`.

Observe that this is different behavior than for lists: for lists, `∈` uses `=` and `contains` uses
`==` for comparisons, while for hash maps, both use `==`.
 -/
Std.ExtDHashMap.contains : {α : Type u} →
  {β : α → Type v} →
    {x : BEq α} → {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → Std.ExtDHashMap α β → α → Bool
-- Mathlib.MeasureTheory.Group.ModularCharacter
MeasureTheory.Measure.addModularCharacterFun_map_add : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : LocallyCompactSpace G] (g h : G),
  MeasureTheory.Measure.addModularCharacterFun (g + h) =
    MeasureTheory.Measure.addModularCharacterFun g * MeasureTheory.Measure.addModularCharacterFun h
-- Mathlib.NumberTheory.Divisors
Nat.Prime.sum_properDivisors : ∀ {α : Type u_1} [inst : AddCommMonoid α] {p : ℕ} {f : ℕ → α}, Nat.Prime p → ∑ x ∈ p.properDivisors, f x = f 1
-- Mathlib.Data.Set.SymmDiff
Set.mem_symmDiff : ∀ {α : Type u} {a : α} {s t : Set α}, a ∈ symmDiff s t ↔ a ∈ s ∧ a ∉ t ∨ a ∈ t ∧ a ∉ s
-- Init.Tactics
/-- `(opt := val)` sets the `opt` configuration option to `val`.

As a special case, `(config := ...)` sets the entire configuration.
 -/
Lean.Parser.Tactic.valConfigItem : Lean.ParserDescr
-- Batteries.Data.HashMap.Basic
Batteries.HashMap.mk : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Std.HashMap α β → Batteries.HashMap α β
-- Mathlib.Data.Nat.Bits
Nat.bits.eq_1 : ∀ (n : ℕ), n.bits = Nat.binaryRec [] (fun b x IH => b :: IH) n
-- Mathlib.Order.Filter.Pi
Filter.pi_le_pi : ∀ {ι : Type u_1} {α : ι → Type u_2} {f₁ f₂ : (i : ι) → Filter (α i)} [∀ (i : ι), (f₁ i).NeBot],
  Filter.pi f₁ ≤ Filter.pi f₂ ↔ ∀ (i : ι), f₁ i ≤ f₂ i
-- Std.Data.HashMap.Basic
Std.HashMap.instLawfulSingletonProd : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α}, LawfulSingleton (α × β) (Std.HashMap α β)
-- Mathlib.Algebra.Quaternion
Quaternion.star_coe : ∀ {R : Type u_3} [inst : CommRing R] (x : R), star ↑x = ↑x
-- Lean.Elab.Tactic.Omega.Core
/-- Which variable is being eliminated.  -/
Lean.Elab.Tactic.Omega.Problem.FourierMotzkinData.var : Lean.Elab.Tactic.Omega.Problem.FourierMotzkinData → ℕ
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.instAddGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousAddMonoidHomToProfiniteContinuousMap.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J ProfiniteAddGrp.{max v u}),
  ProfiniteAddGrp.instAddGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousAddMonoidHomToProfiniteContinuousMap
      F =
    {
      add :=
        ProfiniteAddGrp.instAddGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousAddMonoidHomToProfiniteContinuousMap._aux_1
          F,
      add_assoc := ⋯,
      zero :=
        ProfiniteAddGrp.instAddGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousAddMonoidHomToProfiniteContinuousMap._aux_4
          F,
      zero_add := ⋯, add_zero := ⋯,
      nsmul :=
        ProfiniteAddGrp.instAddGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousAddMonoidHomToProfiniteContinuousMap._aux_8
          F,
      nsmul_zero := ⋯, nsmul_succ := ⋯,
      neg :=
        ProfiniteAddGrp.instAddGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousAddMonoidHomToProfiniteContinuousMap._aux_12
          F,
      sub :=
        ProfiniteAddGrp.instAddGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousAddMonoidHomToProfiniteContinuousMap._aux_14
          F,
      zsmul :=
        ProfiniteAddGrp.instAddGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousAddMonoidHomToProfiniteContinuousMap._aux_16
          F,
      sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯, neg_add_cancel := ⋯ }
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.comm_toLinearEquiv : ∀ (R : Type uR) (A : Type uA) (B : Type uB) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B], ↑(Algebra.TensorProduct.comm R A B) = TensorProduct.comm R A B
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Pos.Raw.extract.match_1.splitter : (motive : String → String.Pos.Raw → String.Pos.Raw → Sort u_1) →
  (x : String) → (x_1 x_2 : String.Pos.Raw) → ((s : String) → (b e : String.Pos.Raw) → motive s b e) → motive x x_1 x_2
-- Mathlib.SetTheory.Ordinal.Basic
Set.embeddingOfSubset.congr_simp : ∀ {α : Type u_1} (s t : Set α) (h : s ⊆ t), s.embeddingOfSubset t h = s.embeddingOfSubset t h
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.rnDeriv_eq_rnDeriv_measure : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} {κ η : ProbabilityTheory.Kernel α γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] [ProbabilityTheory.IsFiniteKernel η]
  [ProbabilityTheory.IsFiniteKernel κ] {a : α}, κ.rnDeriv η a =ᵐ[η a] (κ a).rnDeriv (η a)
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_add_nsmul' : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α) (m : ℕ), toIocMod hp (a + m • p) b = toIocMod hp a b + m • p
-- Mathlib.Topology.Algebra.LinearMapCompletion
/-- Lift a continuous semilinear map to a continuous semilinear map between the
`UniformSpace.Completion`s of the spaces. This is `UniformSpace.Completion.map` bundled as a
continuous linear map when the input is itself a continuous linear map.
 -/
ContinuousLinearMap.completion : {α : Type u_1} →
  {β : Type u_2} →
    {R₁ : Type u_3} →
      {R₂ : Type u_4} →
        [inst : UniformSpace α] →
          [inst_1 : AddCommGroup α] →
            [inst_2 : IsUniformAddGroup α] →
              [inst_3 : Semiring R₁] →
                [inst_4 : Module R₁ α] →
                  [inst_5 : UniformContinuousConstSMul R₁ α] →
                    [inst_6 : Semiring R₂] →
                      [inst_7 : UniformSpace β] →
                        [inst_8 : AddCommGroup β] →
                          [inst_9 : IsUniformAddGroup β] →
                            [inst_10 : Module R₂ β] →
                              [inst_11 : UniformContinuousConstSMul R₂ β] →
                                {σ : R₁ →+* R₂} →
                                  (α →SL[σ] β) → UniformSpace.Completion α →SL[σ] UniformSpace.Completion β
-- Mathlib.Order.Basic
max_def_lt' : ∀ {α : Type u_2} [inst : LinearOrder α] (a b : α), max a b = if b < a then a else b
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.lim_neg : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_2}
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] [inst_5 : CauSeq.IsComplete β abv] (f : CauSeq β abv),
  (-f).lim = -f.lim
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.IsBasis.transfer : ∀ {α : Type u_1} {M : Matroid α} {I X Y J : Set α},
  M.IsBasis I X → M.IsBasis J X → X ⊆ Y → M.IsBasis J Y → M.IsBasis I Y
-- Mathlib.Algebra.Group.Basic
leftInverse_sub_add_left : ∀ {G : Type u_3} [inst : AddGroup G] (c : G), Function.LeftInverse (fun x => x - c) fun x => x + c
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
measurableSet_Iio : ∀ {α : Type u_1} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [inst_2 : LinearOrder α]
  {a : α} [ClosedIciTopology α], MeasurableSet (Set.Iio a)
-- Mathlib.Order.Hom.CompleteLattice
FrameHom.comp_apply : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  [inst_2 : CompleteLattice γ] (f : FrameHom β γ) (g : FrameHom α β) (a : α), (f.comp g) a = f (g a)
-- Mathlib.Data.Matrix.Mul
Matrix.mul_add : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype n]
  (L : Matrix m n α) (M N : Matrix n o α), L * (M + N) = L * M + L * N
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Poly.append.eq_2 : ∀ (p₂ : Lean.Grind.Linarith.Poly) (k : ℤ) (v : Lean.Grind.Linarith.Var) (p_1 : Lean.Grind.Linarith.Poly),
  (Lean.Grind.Linarith.Poly.add k v p_1).append p₂ = Lean.Grind.Linarith.Poly.add k v (p_1.append p₂)
-- Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
/-- `E` and `F` are homotopy equivalent, then the multifork associated
to `E` is exact if and only if the multifork associated to `F` is exact.  -/
CategoryTheory.PreOneHypercover.Homotopy.isLimitMultiforkEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      {E : CategoryTheory.PreOneHypercover S} →
        {F : CategoryTheory.PreOneHypercover S} →
          {A : Type u_1} →
            [inst_1 : CategoryTheory.Category.{v_1, u_1} A] →
              (f : E.Hom F) →
                (g : F.Hom E) →
                  CategoryTheory.PreOneHypercover.Homotopy (f.comp g) (CategoryTheory.PreOneHypercover.Hom.id E) →
                    CategoryTheory.PreOneHypercover.Homotopy (g.comp f) (CategoryTheory.PreOneHypercover.Hom.id F) →
                      {G : CategoryTheory.Functor Cᵒᵖ A} →
                        CategoryTheory.Limits.IsLimit (E.multifork G) ≃ CategoryTheory.Limits.IsLimit (F.multifork G)
-- Init.Data.Range.Polymorphic.UInt
USize.succ?_ofBitVec : ∀ {x : BitVec System.Platform.numBits}, Std.PRange.succ? { toBitVec := x } = USize.ofBitVec <$> Std.PRange.succ? x
-- Mathlib.Algebra.Polynomial.Homogenize
Polynomial.toTupleMvPolynomial_zero_eq : ∀ {R : Type u_1} [inst : CommSemiring R] (p : Polynomial R), p.toTupleMvPolynomial 0 = p.homogenize p.natDegree
-- Mathlib.NumberTheory.ModularForms.Cusps
cosetToCuspOrbit.congr_simp : ∀ (𝒢 : Subgroup (GL (Fin 2) ℝ)) [inst : 𝒢.IsArithmetic]
  (a a_1 : Matrix.SpecialLinearGroup (Fin 2) ℤ ⧸ Subgroup.comap (Matrix.SpecialLinearGroup.mapGL ℝ) 𝒢),
  a = a_1 → cosetToCuspOrbit 𝒢 a = cosetToCuspOrbit 𝒢 a_1
-- Init.Data.Vector.MapIdx
Vector.mapFinIdx_eq_mapFinIdx_iff : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {f g : (i : ℕ) → α → i < n → β},
  xs.mapFinIdx f = xs.mapFinIdx g ↔ ∀ (i : ℕ) (h : i < n), f i xs[i] h = g i xs[i] h
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.mk_lt_mk : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {a b : M},
  MulArchimedeanClass.mk a < MulArchimedeanClass.mk b ↔ ∀ (n : ℕ), |b|ₘ ^ n < |a|ₘ
-- Mathlib.Order.LatticeIntervals
Set.Ici.coe_inf : ∀ {α : Type u_1} [inst : SemilatticeInf α] {a : α} {x y : ↑(Set.Ici a)}, ↑(x ⊓ y) = ↑x ⊓ ↑y
-- Mathlib.Order.Monotone.Basic
strictAnti_comp_ofDual_iff : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  StrictAnti (f ∘ ⇑OrderDual.ofDual) ↔ StrictMono f
-- Init.Data.SInt.Lemmas
ISize.toInt_ofIntTruncate : ∀ {x : ℤ}, ISize.minValue.toInt ≤ x → x ≤ ISize.maxValue.toInt → (ISize.ofIntClamp x).toInt = x
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.HasOrthogonalProjection.map_linearIsometryEquiv' : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] {E' : Type u_4} [inst_4 : NormedAddCommGroup E']
  [inst_5 : InnerProductSpace 𝕜 E'] (f : E ≃ₗᵢ[𝕜] E'), (Submodule.map (↑f.toLinearIsometry) K).HasOrthogonalProjection
-- Mathlib.RingTheory.MatrixAlgebra
MatrixEquivTensor.left_inv : ∀ (n : Type u_3) (R : Type u_5) (A : Type u_7) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : DecidableEq n] [inst_4 : Fintype n] (M : TensorProduct R A (Matrix n n R)),
  MatrixEquivTensor.invFun n R A ((MatrixEquivTensor.toFunAlgHom n R A) M) = M
-- Mathlib.Analysis.Polynomial.Fourier
Polynomial.instTwoPiPos : Fact (0 < 2 * Real.pi)
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
/-- `homothety` as an affine map.  -/
AffineMap.homothetyAffine : {k : Type u_2} →
  {V1 : Type u_3} →
    {P1 : Type u_4} →
      [inst : CommRing k] →
        [inst_1 : AddCommGroup V1] → [inst_2 : AddTorsor V1 P1] → [inst_3 : Module k V1] → P1 → k →ᵃ[k] P1 →ᵃ[k] P1
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `antivaryOn_inv₀`. -/
AntivaryOn.of_inv₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : Semifield β] [inst_4 : LinearOrder β] [IsStrictOrderedRing β] {s : Set ι} {f : ι → α} {g : ι → β},
  (∀ i ∈ s, 0 < f i) → (∀ i ∈ s, 0 < g i) → AntivaryOn f⁻¹ g⁻¹ s → AntivaryOn f g s
-- Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
/-- A compositum of two purely inseparable extensions is purely inseparable.  -/
IntermediateField.isPurelyInseparable_sup : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (L1 L2 : IntermediateField F E)
  [h1 : IsPurelyInseparable F ↥L1] [h2 : IsPurelyInseparable F ↥L2], IsPurelyInseparable F ↥(L1 ⊔ L2)
-- Mathlib.CategoryTheory.Sites.Sheaf
CategoryTheory.sheafSectionsNatIsoEvaluation_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₂)
  [inst_1 : CategoryTheory.Category.{v₂, u₂} A] {X : C} (X_1 : CategoryTheory.Sheaf J A),
  (CategoryTheory.sheafSectionsNatIsoEvaluation J A).inv.app X_1 =
    CategoryTheory.CategoryStruct.id (X_1.obj.obj (Opposite.op X))
-- Mathlib.Analysis.InnerProductSpace.Defs
InnerProductSpace.Core.mk.injEq : ∀ {𝕜 : Type u_4} {F : Type u_5} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  (toCore : PreInnerProductSpace.Core 𝕜 F) (definite : ∀ (x : F), inner 𝕜 x x = 0 → x = 0)
  (toCore_1 : PreInnerProductSpace.Core 𝕜 F) (definite_1 : ∀ (x : F), inner 𝕜 x x = 0 → x = 0),
  ({ toCore := toCore, definite := definite } = { toCore := toCore_1, definite := definite_1 }) = (toCore = toCore_1)
-- Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
CategoryTheory.ObjectProperty.instIsStableUnderRetractsEpiModSerre : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsSerreClass], P.epiModSerre.IsStableUnderRetracts
-- Mathlib.RingTheory.WittVector.Defs
WittVector.wittMul.eq_1 : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], WittVector.wittMul p = wittStructureInt p (MvPolynomial.X 0 * MvPolynomial.X 1)
-- Mathlib.GroupTheory.GroupAction.Quotient
MulAction.right_quotientAction' : ∀ {G : Type u} [inst : Group G] (H : Subgroup G) [hH : H.Normal], MulAction.QuotientAction Gᵐᵒᵖ H
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.ofEq_symm : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E] {R' : Type u_12} [inst_1 : Ring R'] [inst_2 : Module R' E]
  {p q : Submodule R' E} (h : p = q), (LinearIsometryEquiv.ofEq p q h).symm = LinearIsometryEquiv.ofEq q p ⋯
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.isHenstock_biUnionTagged : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.Prepartition I}
  {πi : (J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J},
  (π.biUnionTagged πi).IsHenstock ↔ ∀ J ∈ π, (πi J).IsHenstock
-- Mathlib.Order.Quotient
Quotient.lt_of_mk_lt_mk : ∀ {α : Type u_1} {s : Setoid α} [inst : LinearOrder α] [H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected]
  {x y : α}, ⟦x⟧ < ⟦y⟧ → x < y
-- Aesop.ElabM
Aesop.instMonadElabM : Monad Aesop.ElabM
-- Mathlib.Order.BoundedOrder.Basic
OrderDual.toDual_bot : ∀ (α : Type u) [inst : Bot α], OrderDual.toDual ⊥ = ⊤
-- Mathlib.Data.PFun
PFun.pure_defined : ∀ {α : Type u_1} {β : Type u_2} (p : Set α) (x : β), p ⊆ (PFun.pure x).Dom
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasDerivWithinAt_Iio_iff_Iic : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} [inst_3 : PartialOrder 𝕜],
  HasDerivWithinAt f f' (Set.Iio x) x ↔ HasDerivWithinAt f f' (Set.Iic x) x
-- Mathlib.Topology.Category.LightProfinite.Basic
instFaithfulFintypeCatLightProfiniteToLightProfinite : FintypeCat.toLightProfinite.Faithful
-- Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
CategoryTheory.Limits.Concrete.widePullback_ext' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type (max v w)}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {B : C}
  {ι : Type w} [Nonempty ι] {X : ι → C} (f : (j : ι) → X j ⟶ B) [inst_4 : CategoryTheory.Limits.HasWidePullback B X f]
  [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.WidePullbackShape.wideCospan B X f)
      (CategoryTheory.forget C)]
  (x y : CategoryTheory.ToType (CategoryTheory.Limits.widePullback B X f)),
  (∀ (j : ι),
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.WidePullback.π f j)) x =
        (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.WidePullback.π f j)) y) →
    x = y
-- Lean.Elab.DeclModifiers
Lean.Elab.instReprComputeKind.repr : Lean.Elab.ComputeKind → ℕ → Std.Format
-- Mathlib.Data.Matrix.ColumnRowPartitioned
Matrix.fromRows_zero : ∀ {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} [inst : Semiring R], Matrix.fromRows 0 0 = 0
-- Mathlib.Data.Finsupp.Option
Finsupp.optionElim_ne_zero_of_right : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] (y : M) (f : α →₀ M), f ≠ 0 → Finsupp.optionElim y f ≠ 0
-- Mathlib.LinearAlgebra.Dimension.Finrank
finrank_top : ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Module.finrank R ↥⊤ = Module.finrank R M
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tsum_empty : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  {L : SummationFilter β} [IsEmpty β], ∑'[L] (b : β), f b = 0
-- Mathlib.Algebra.Group.ULift
ULift.inv_down : ∀ {α : Type u} {x : ULift.{w, u} α} [inst : Inv α], x⁻¹.down = x.down⁻¹
-- Lean.Expr
/-- Return `true` if the given expression is an application.  -/
Lean.Expr.isApp : Lean.Expr → Bool
-- Mathlib.LinearAlgebra.Matrix.Adjugate
/-- A weaker version of `Matrix.adjugate_adjugate` that uses `Nontrivial`.  -/
Matrix.adjugate_adjugate' : ∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] (A : Matrix n n α)
  [Nontrivial n], A.adjugate.adjugate = A.det ^ (Fintype.card n - 2) • A
-- Mathlib.Analysis.Analytic.Constructions
/-- Eta-expanded form of `AnalyticAt.zpow`

---

ZPowers of analytic functions (into a normed field over `𝕜`) are analytic away from the zeros.
 -/
AnalyticAt.fun_zpow : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝕝 : Type u_8} [inst_3 : NormedDivisionRing 𝕝] [inst_4 : NormedAlgebra 𝕜 𝕝] {f : E → 𝕝}
  {z : E} {n : ℤ}, AnalyticAt 𝕜 f z → f z ≠ 0 → AnalyticAt 𝕜 (fun i => f i ^ n) z
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.ext : ∀ {α : Type u_1} [inst : LE α] {s t : UpperSet α}, ↑s = ↑t → s = t
-- Mathlib.Algebra.Order.Group.Multiset
Multiset.nsmul_cons : ∀ {α : Type u_1} {s : Multiset α} (n : ℕ) (a : α), n • (a ::ₘ s) = n • {a} + n • s