mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Invariant.Profinite
/-- The stabilizer subgroup of `Q` surjects onto `Aut((B/Q)/(A/P))`.  -/
Ideal.Quotient.stabilizerHom_surjective_of_profinite : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] {G : Type u}
  [inst_3 : Group G] [inst_4 : MulSemiringAction G B] [inst_5 : SMulCommClass G A B] [inst_6 : TopologicalSpace G]
  [CompactSpace G] [TotallyDisconnectedSpace G] [IsTopologicalGroup G] [inst_10 : TopologicalSpace B]
  [DiscreteTopology B] [ContinuousSMul G B] (P : Ideal A) (Q : Ideal B) [Q.IsPrime] [inst_14 : Q.LiesOver P]
  [Algebra.IsInvariant A B G], Function.Surjective ⇑(Ideal.Quotient.stabilizerHom Q P G)
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.eq_one_iff : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommMonoidWithZero R'] {χ : MulChar R R'},
  χ = 1 ↔ ∀ (a : Rˣ), χ ↑a = 1
-- Mathlib.RingTheory.PowerSeries.Basic
Polynomial.coeToPowerSeries.algHom_apply : ∀ {R : Type u_1} [inst : CommSemiring R] (φ : Polynomial R) (A : Type u_2) [inst_1 : Semiring A] [inst_2 : Algebra R A],
  (Polynomial.coeToPowerSeries.algHom A) φ = (PowerSeries.map (algebraMap R A)) ↑φ
-- Mathlib.Condensed.Light.TopCatAdjunction
/-- Auxiliary definition to define the topology on `X(*)` for a light condensed set `X`.  -/
_private.Mathlib.Condensed.Light.TopCatAdjunction.0.LightCondSet.coinducingCoprod : (X : LightCondSet) →
  (i : (S : LightProfinite) × X.obj.obj (Opposite.op S)) × ↑i.fst.toTop →
    X.obj.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))
-- Mathlib.NumberTheory.ModularForms.BoundedAtCusp
OnePoint.IsBoundedAt.add : ∀ {c : OnePoint ℝ} {f : UpperHalfPlane → ℂ} {k : ℤ} {f' : UpperHalfPlane → ℂ},
  c.IsBoundedAt f k → c.IsBoundedAt f' k → c.IsBoundedAt (f + f') k
-- Mathlib.CategoryTheory.Types.Basic
_private.Mathlib.CategoryTheory.Types.Basic.0.TypeCat.Hom.mk.sizeOf_spec : ∀ {X Y : Type u} [inst : SizeOf X] [inst_1 : SizeOf Y] (hom' : TypeCat.Fun X Y),
  sizeOf { hom' := hom' } = 1 + sizeOf hom'
-- Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
AlgebraicClosure.instSMulOfIsScalarTower : (k : Type u) →
  [inst : Field k] → {S : Type u_1} → [inst_1 : DistribSMul S k] → [IsScalarTower S k k] → SMul S (AlgebraicClosure k)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.BlastUdivOutput.mk : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {old : Std.Sat.AIG α} →
        {w : ℕ} →
          (aig : Std.Sat.AIG α) →
            aig.RefVec w →
              aig.RefVec w →
                old.decls.size ≤ aig.decls.size → Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.BlastUdivOutput old w
-- Mathlib.NumberTheory.NumberField.House
/-- `supOfBasis K` calculates the supremum of the absolute values of
the elements in `newBasis K`.  -/
_private.Mathlib.NumberTheory.NumberField.House.0.NumberField.house.supOfBasis : (K : Type u_1) → [inst : Field K] → [NumberField K] → ℝ
-- Init.Data.String.Slice
/-- Removes leading and trailing whitespace from a slice.

“Whitespace” is defined as characters for which `Char.isWhitespace` returns `true`.

Examples:

* `"abc".toSlice.trimAscii == "abc".toSlice`

* `"   abc".toSlice.trimAscii == "abc".toSlice`

* `"abc \t  ".toSlice.trimAscii == "abc".toSlice`

* `"  abc   ".toSlice.trimAscii == "abc".toSlice`

* `"abc\ndef\n".toSlice.trimAscii == "abc\ndef".toSlice`
 -/
String.Slice.trimAscii : String.Slice → String.Slice
-- Mathlib.Topology.Semicontinuity.Basic
lowerSemicontinuousWithinAt_sum : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {x : α} {ι : Type u_4} {γ : Type u_5}
  [inst_1 : AddCommMonoid γ] [inst_2 : LinearOrder γ] [IsOrderedAddMonoid γ] [inst_4 : TopologicalSpace γ]
  [OrderTopology γ] [ContinuousAdd γ] {f : ι → α → γ} {a : Finset ι},
  (∀ i ∈ a, LowerSemicontinuousWithinAt (f i) s x) → LowerSemicontinuousWithinAt (fun z => ∑ i ∈ a, f i z) s x
-- Mathlib.Algebra.Group.Subgroup.Defs
exists_neg_mem_iff_exists_mem : ∀ {G : Type u_1} [inst : AddGroup G] {S : Type u_4} {H : S} [inst_1 : SetLike S G] [AddSubgroupClass S G]
  {P : G → Prop}, (∃ x ∈ H, P (-x)) ↔ ∃ x ∈ H, P x
-- Init.Meta.Defs
Lean.Syntax.instReprPreresolved : Repr Lean.Syntax.Preresolved
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
ModularGroup.coe_S : ↑ModularGroup.S = !![0, -1; 1, 0]
-- Mathlib.CategoryTheory.GradedObject.Unitor
CategoryTheory.GradedObject.TriangleIndexData.h₃ : ∀ {I₁ : Type u_1} {I₂ : Type u_2} {I₃ : Type u_3} {J : Type u_4} [inst : Zero I₂] {r : I₁ × I₂ × I₃ → J}
  {π : I₁ × I₃ → J} (self : CategoryTheory.GradedObject.TriangleIndexData r π) (i₃ : I₃), self.p₂₃ (0, i₃) = i₃
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
IsDiscreteValuationRing.remainder.eq_1 : ∀ {R : Type u_2} [inst : CommRing R] (x y : R), IsDiscreteValuationRing.remainder x y = if y ∣ x then 0 else x
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Ring
CategoryTheory.yonedaCommRing_map_app_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {R₁ R₂ : CategoryTheory.CommRingObjCat C} (f : R₁ ⟶ R₂) {X : C}
  (x : X ⟶ R₁.X),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.yonedaCommRing.map f).app (Opposite.op X))) x =
    CategoryTheory.CategoryStruct.comp x f.hom
-- Mathlib.Probability.Kernel.Category.Stoch
/-- Morphism property selecting Markov kernels in `SFinKer`.  -/
StochHom : CategoryTheory.MorphismProperty SFinKer
-- Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
_private.Mathlib.MeasureTheory.VectorMeasure.BoundedVariation.0.BoundedVariationOn.measureAux.congr_simp : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : DenselyOrdered α] [inst_2 : TopologicalSpace α]
  [inst_3 : OrderTopology α] [inst_4 : SecondCountableTopology α] [inst_5 : CompactIccSpace α] [hα : MeasurableSpace α]
  [inst_6 : BorelSpace α] {E : Type u_2} [inst_7 : NormedAddCommGroup E] [inst_8 : CompleteSpace E] {f f_1 : α → E}
  (e_f : f = f_1) (hf : BoundedVariationOn f Set.univ),
  BoundedVariationOn.measureAux✝ hf = BoundedVariationOn.measureAux✝ ⋯
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ContinuousHom.ext_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β]
  {f g : α →𝒄 β}, f = g ↔ ∀ (x : α), f x = g x
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.contract_finitary : ∀ {α : Type u_1} {M : Matroid α} {C : Set α} [M.Finitary], (M.contract C).Finitary
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.insert.induct_unfolding : ∀ (k : ℤ) (v : Int.Internal.Linear.Var) (motive : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Prop),
  (∀ (k_1 : ℤ),
      motive (Int.Internal.Linear.Poly.num k_1) (Int.Internal.Linear.Poly.add k v (Int.Internal.Linear.Poly.num k_1))) →
    (∀ (k_1 : ℤ) (v_1 : Int.Internal.Linear.Var) (p : Int.Internal.Linear.Poly),
        Nat.blt v_1 v = true →
          motive (Int.Internal.Linear.Poly.add k_1 v_1 p)
            (Int.Internal.Linear.Poly.add k v (Int.Internal.Linear.Poly.add k_1 v_1 p))) →
      (∀ (k_1 : ℤ) (v_1 : Int.Internal.Linear.Var) (p : Int.Internal.Linear.Poly),
          Nat.blt v_1 v = false →
            Nat.beq v v_1 = true → (k.add k_1 == 0) = true → motive (Int.Internal.Linear.Poly.add k_1 v_1 p) p) →
        (∀ (k_1 : ℤ) (v_1 : Int.Internal.Linear.Var) (p : Int.Internal.Linear.Poly),
            Nat.blt v_1 v = false →
              Nat.beq v v_1 = true →
                ¬(k.add k_1 == 0) = true →
                  motive (Int.Internal.Linear.Poly.add k_1 v_1 p) (Int.Internal.Linear.Poly.add (k.add k_1) v_1 p)) →
          (∀ (k_1 : ℤ) (v_1 : Int.Internal.Linear.Var) (p : Int.Internal.Linear.Poly),
              Nat.blt v_1 v = false →
                Nat.beq v v_1 = false →
                  motive p (Int.Internal.Linear.Poly.insert k v p) →
                    motive (Int.Internal.Linear.Poly.add k_1 v_1 p)
                      (Int.Internal.Linear.Poly.add k_1 v_1 (Int.Internal.Linear.Poly.insert k v p))) →
            ∀ (p : Int.Internal.Linear.Poly), motive p (Int.Internal.Linear.Poly.insert k v p)
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.infEDist_singleton`.

---

The edist to a singleton is the edistance to the single point of this singleton  -/
EMetric.infEdist_singleton : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x y : α}, Metric.infEDist x {y} = edist x y
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.snd_opProdIsoCoprod_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A B : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct A B],
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd.op (CategoryTheory.Limits.opProdIsoCoprod A B).hom =
    CategoryTheory.Limits.coprod.inr
-- Mathlib.MeasureTheory.Function.LpSpace.Indicator
MeasureTheory.Lp.norm_const : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α)
  [inst : NormedAddCommGroup E] [inst_1 : MeasureTheory.IsFiniteMeasure μ] (c : E) [NeZero μ],
  p ≠ 0 → ‖(MeasureTheory.Lp.const p μ) c‖ = ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.monomial_sub : ∀ {R : Type u} {a b : R} [inst : Ring R] (n : ℕ),
  (Polynomial.monomial n) (a - b) = (Polynomial.monomial n) a - (Polynomial.monomial n) b
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsPath.ne_of_mem_support_of_append : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk u v} {q : G.Walk v w},
  (p.append q).IsPath → ∀ {x y : V}, y ≠ v → x ∈ p.support → y ∈ q.support → x ≠ y
-- Mathlib.Algebra.Order.Ring.Synonym
Lex.instNonUnitalCommSemiring : {R : Type u_1} → [NonUnitalCommSemiring R] → NonUnitalCommSemiring (Lex R)
-- Mathlib.Algebra.CharP.CharAndCard
/-- A prime that divides the cardinality of a finite commutative ring `R`
isn't a unit in `R`.  -/
not_isUnit_prime_of_dvd_card : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : Fintype R] {p : ℕ} [Fact (Nat.Prime p)], p ∣ Fintype.card R → ¬IsUnit ↑p
-- Mathlib.Data.Seq.Basic
Stream'.Seq.cons.eq_1 : ∀ {α : Type u} (a : α) (s : Stream'.Seq α), Stream'.Seq.cons a s = ⟨Stream'.cons (some a) ↑s, ⋯⟩
-- Mathlib.Topology.Algebra.Module.TransferInstance
/-- An equivalence `e : α ≃ β` gives a continuous linear equivalence `α ≃L[R] β`
where the continuous `R`-module structure on `α` is the one obtained by transporting an
`R`-module structure on `β` back along `e`.

This is `e.linearEquiv` as a continuous linear equivalence.  -/
Equiv.continuousLinearEquiv : (R : Type u_1) →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : TopologicalSpace β] →
        [inst_1 : AddCommMonoid β] → [inst_2 : Semiring R] → [inst_3 : Module R β] → (e : α ≃ β) → α ≃L[R] β
-- Mathlib.Data.List.ReduceOption
List.reduceOption_eq_append_iff : ∀ {α : Type u_1} (l : List (Option α)) (l'₁ l'₂ : List α),
  l.reduceOption = l'₁ ++ l'₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁.reduceOption = l'₁ ∧ l₂.reduceOption = l'₂
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
CategoryTheory.Limits.inr_pushoutRightPushoutInlIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (f' : Y ⟶ W)
  [inst_1 : CategoryTheory.Limits.HasPushout f g]
  [inst_2 : CategoryTheory.Limits.HasPushout f' (CategoryTheory.Limits.pushout.inl f g)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr (CategoryTheory.CategoryStruct.comp f f') g)
      (CategoryTheory.Limits.pushoutRightPushoutInlIso f g f').inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f g)
      (CategoryTheory.Limits.pushout.inr f' (CategoryTheory.Limits.pushout.inl f g))
-- Mathlib.CategoryTheory.Limits.Opposites
/-- Turn a colimit for `F.unop : J ⥤ C` into a limit for `F : Jᵒᵖ ⥤ Cᵒᵖ`.  -/
CategoryTheory.Limits.isLimitOfCoconeUnopOfCone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} J] →
        (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) →
          {c : CategoryTheory.Limits.Cone F} →
            CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeUnopOfCone c) → CategoryTheory.Limits.IsLimit c
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
preNormEDS'_odd : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R) (m : ℕ),
  preNormEDS' b c d (2 * (m + 2) + 1) =
    (preNormEDS' b c d (m + 4) * preNormEDS' b c d (m + 2) ^ 3 * if Even m then b else 1) -
      preNormEDS' b c d (m + 1) * preNormEDS' b c d (m + 3) ^ 3 * if Even m then 1 else b
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.range_fst : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S], (RingHom.fst R S).rangeS = ⊤
-- Mathlib.CategoryTheory.Limits.Final
/-- Given a limit cone over `F ⋙ G` we can construct a limit cone over `G`.  -/
CategoryTheory.Functor.Initial.limitConeOfComp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [F.Initial] →
            {E : Type u₃} →
              [inst_3 : CategoryTheory.Category.{v₃, u₃} E] →
                {G : CategoryTheory.Functor D E} →
                  CategoryTheory.Limits.LimitCone (F.comp G) → CategoryTheory.Limits.LimitCone G
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
/-- The characteristic function of a product of measures is a product of
characteristic functions. This is `charFunDual_prod` for `WithLp`.
See `charFun_prod` for the Hilbert space version.  -/
MeasureTheory.charFunDual_prod' : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {mE : MeasurableSpace E}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {mF : MeasurableSpace F} {μ : MeasureTheory.Measure E}
  {ν : MeasureTheory.Measure F} (p : ENNReal) [inst_4 : Fact (1 ≤ p)] [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν] (L : StrongDual ℝ (WithLp p (E × F))),
  MeasureTheory.charFunDual (MeasureTheory.Measure.map (WithLp.toLp p) (μ.prod ν)) L =
    MeasureTheory.charFunDual μ
        (L ∘SL ↑(WithLp.prodContinuousLinearEquiv p ℝ E F).symm ∘SL ContinuousLinearMap.inl ℝ E F) *
      MeasureTheory.charFunDual ν
        (L ∘SL ↑(WithLp.prodContinuousLinearEquiv p ℝ E F).symm ∘SL ContinuousLinearMap.inr ℝ E F)
-- Mathlib.RingTheory.Nilpotent.Exp
IsNilpotent.exp_mul_exp_neg_self : ∀ {A : Type u_1} [inst : Ring A] [inst_1 : Module ℚ A] {a : A},
  IsNilpotent a → IsNilpotent.exp a * IsNilpotent.exp (-a) = 1
-- Lean.Parser.Types
Lean.Parser.ParserState.errorMsg : Lean.Parser.ParserState → Option Lean.Parser.Error
-- Mathlib.Algebra.Group.Units.Basic
AddUnits.neg_eq_of_add_eq_zero_right : ∀ {α : Type u} [inst : AddMonoid α] {u : AddUnits α} {a : α}, ↑u + a = 0 → ↑(-u) = a
-- Mathlib.Algebra.Module.Injective
/-- The linear map `M ⊔ ⟨y⟩ ⟶ Q` by `x + r • y ↦ f x + φ r` is an extension of `f`  -/
Module.Baer.extensionOfMaxAdjoin : {R : Type u} →
  [inst : Ring R] →
    {Q : Type v} →
      [inst_1 : AddCommGroup Q] →
        [inst_2 : Module R Q] →
          {M : Type u_1} →
            {N : Type u_2} →
              [inst_3 : AddCommGroup M] →
                [inst_4 : AddCommGroup N] →
                  [inst_5 : Module R M] →
                    [inst_6 : Module R N] →
                      (i : M →ₗ[R] N) →
                        (f : M →ₗ[R] Q) →
                          [Fact (Function.Injective ⇑i)] → Module.Baer R Q → N → Module.Baer.ExtensionOf i f
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
/-- **Alias** of `MeasureTheory.integrable_finsetSum_measure`. -/
MeasureTheory.integrable_finset_sum_measure : ∀ {α : Type u_1} {ε : Type u_5} [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε]
  [TopologicalSpace.PseudoMetrizableSpace ε] {ι : Type u_8} {m : MeasurableSpace α} {f : α → ε}
  {μ : ι → MeasureTheory.Measure α} {s : Finset ι},
  MeasureTheory.Integrable f (∑ i ∈ s, μ i) ↔ ∀ i ∈ s, MeasureTheory.Integrable f (μ i)
-- Mathlib.NumberTheory.ADEInequality
ADEInequality.lt_six : ∀ {r : ℕ+}, 1 < ADEInequality.sumInv {2, 3, r} → r < 6
-- Mathlib.MeasureTheory.SpecificCodomains.WithLp
/-- **Alias** of the reverse direction of `MeasureTheory.integrable_prodLp_iff`. -/
MeasureTheory.Integrable.of_fst_of_snd_prodLp : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {q : ENNReal} [inst : Fact (1 ≤ q)]
  {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedAddCommGroup F]
  {f : X → WithLp q (E × F)},
  MeasureTheory.Integrable (fun x => (f x).fst) μ ∧ MeasureTheory.Integrable (fun x => (f x).snd) μ →
    MeasureTheory.Integrable f μ
-- Mathlib.Topology.Algebra.Monoid
Prod.continuousAdd : ∀ {M : Type u_3} {N : Type u_4} [inst : TopologicalSpace M] [inst_1 : Add M] [ContinuousAdd M]
  [inst_3 : TopologicalSpace N] [inst_4 : Add N] [ContinuousAdd N], ContinuousAdd (M × N)
-- Init.Data.Array.Range
Array.range'_one : ∀ {s step : ℕ}, Array.range' s 1 step = #[s]
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.equivFun_apply : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Finite ι] (b : Module.Basis ι R M) (u : M), b.equivFun u = ⇑(b.repr u)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.toHomeomorph_eq_coe : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Mul M]
  [inst_3 : Mul N] (f : M ≃ₜ* N), f.toHomeomorph = ↑f
-- Mathlib.Data.Fintype.Sum
Finset.univ_disjSum_univ : ∀ {α : Type u_3} {β : Type u_4} [inst : Fintype α] [inst_1 : Fintype β], Finset.univ.disjSum Finset.univ = Finset.univ
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.norm_zero : ∀ {R : Type u_2} {a b : R} [inst : CommRing R], QuadraticAlgebra.norm 0 = 0
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey?_filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {k : α} (h : m.WF),
  (Std.DHashMap.Raw.filterMap f m).getKey? k = (m.getKey? k).pfilter fun x h' => (f x (m.get x ⋯)).isSome
-- Mathlib.Data.List.Cycle
_private.Mathlib.Data.List.Cycle.0.List.prev.match_1.eq_1 : ∀ {α : Type u_1} (motive : (x : List α) → (x_1 : α) → x_1 ∈ x → Sort u_2) (x : α) (h : x ∈ [])
  (h_1 : (x : α) → (h : x ∈ []) → motive [] x h) (h_2 : (y x : α) → (x_1 : x ∈ [y]) → motive [y] x x_1)
  (h_3 : (y z : α) → (xs : List α) → (x : α) → (h : x ∈ y :: z :: xs) → motive (y :: z :: xs) x h),
  (match [], x, h with
    | [], x, h => h_1 x h
    | [y], x, x_1 => h_2 y x x_1
    | y :: z :: xs, x, h => h_3 y z xs x h) =
    h_1 x h
-- Mathlib.Topology.Algebra.Monoid.Defs
ContinuousOn.add_const : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Add M] [SeparatelyContinuousAdd M] {X : Type u_2}
  [inst_3 : TopologicalSpace X] {f : X → M} {s : Set X}, ContinuousOn f s → ∀ (b : M), ContinuousOn (fun x => f x + b) s
-- Mathlib.RingTheory.Finiteness.Small
Submodule.instInhabitedSubtypeSmallMem : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Inhabited { P // Small.{u, u_2} ↥P }
-- Mathlib.Order.Filter.AtTopBot.Archimedean
atTop_isCountablyGenerated_of_archimedean : ∀ {R : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [IsOrderedRing R] [Archimedean R],
  Filter.atTop.IsCountablyGenerated
-- Mathlib.NumberTheory.LegendreSymbol.Basic
legendreSym.at_one : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], legendreSym p 1 = 1
-- Std.Data.HashMap.Lemmas
Std.HashMap.not_mem_emptyWithCapacity : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {a : α} {c : ℕ}, a ∉ Std.HashMap.emptyWithCapacity c
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
_private.Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctor_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) {X Y : C} (φ : X ⟶ Y),
  (CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctor✝ t n).map φ =
    CategoryTheory.Triangulated.TStructure.TruncAux.triangleMap✝ t n φ
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.coe_πs : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] (o : Ordinal.{u})
  (f : LocallyConstant ↑(Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o) ℤ),
  ⇑((Profinite.NobelingProof.πs C o) f) =
    ⇑f ∘ Profinite.NobelingProof.ProjRestrict C fun x => Profinite.NobelingProof.ord I x < o
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.Const.modify.eq_1 : ∀ {α : Type u} [inst : BEq α] {β : Type v} [inst_1 : Hashable α] (a : α) (f : β → β) (size : ℕ)
  (buckets : Array (Std.DHashMap.Internal.AssocList α fun x => β))
  (hm : 0 < { size := size, buckets := buckets }.buckets.size),
  Std.DHashMap.Internal.Raw₀.Const.modify ⟨{ size := size, buckets := buckets }, hm⟩ a f =
    match Std.DHashMap.Internal.mkIdx buckets.size hm (hash a) with
    | ⟨i, hi⟩ =>
      let bucket := buckets[i];
      if Std.DHashMap.Internal.AssocList.contains a bucket = true then
        let buckets_1 := buckets.uset i Std.DHashMap.Internal.AssocList.nil hi;
        let bucket := Std.DHashMap.Internal.AssocList.Const.modify a f bucket;
        ⟨{ size := size, buckets := buckets_1.uset i bucket ⋯ }, ⋯⟩
      else ⟨{ size := size, buckets := buckets }, hm⟩
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasProdLocallyUniformlyOn.multipliableLocallyUniformlyOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β],
  HasProdLocallyUniformlyOn f g s → MultipliableLocallyUniformlyOn f s
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.rightIso_inv : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {R₁ : CategoryTheory.Functor B T}
  {L₁ : CategoryTheory.Functor A T} {X Y : CategoryTheory.Comma L₁ R₁} (α : X ≅ Y),
  (CategoryTheory.Comma.rightIso α).inv = α.inv.right
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.mk.inj : ∀ {R : Type u} {inst : NonAssocSemiring R} {toSubmonoid : Submonoid R}
  {add_mem' : ∀ {a b : R}, a ∈ toSubmonoid.carrier → b ∈ toSubmonoid.carrier → a + b ∈ toSubmonoid.carrier}
  {zero_mem' : 0 ∈ toSubmonoid.carrier} {toSubmonoid_1 : Submonoid R}
  {add_mem'_1 : ∀ {a b : R}, a ∈ toSubmonoid_1.carrier → b ∈ toSubmonoid_1.carrier → a + b ∈ toSubmonoid_1.carrier}
  {zero_mem'_1 : 0 ∈ toSubmonoid_1.carrier},
  { toSubmonoid := toSubmonoid, add_mem' := add_mem', zero_mem' := zero_mem' } =
      { toSubmonoid := toSubmonoid_1, add_mem' := add_mem'_1, zero_mem' := zero_mem'_1 } →
    toSubmonoid = toSubmonoid_1
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.degree_add_div : ∀ {R : Type u} [inst : Field R] {p q : Polynomial R}, q ≠ 0 → q.degree ≤ p.degree → q.degree + (p / q).degree = p.degree
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.GrindCnstr.notDefEq.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.comp_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G H : CategoryTheory.Pseudofunctor B C} (η : F ⟶ G) (θ : G ⟶ H) (a : B),
  (CategoryTheory.CategoryStruct.comp η θ).app a = CategoryTheory.CategoryStruct.comp (η.app a) (θ.app a)
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.equivalence_unitIso : AddCommMonCat.equivalence.unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id AddCommMonCat)