mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.ZLattice.Basic
/-- The map that sends a vector of `E` to the element of the ℤ-lattice spanned by `b` obtained
by rounding up its coordinates on the basis `b`.  -/
ZSpan.ceil : {E : Type u_1} →
  {ι : Type u_2} →
    {K : Type u_3} →
      [inst : NormedField K] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace K E] →
            (b : Module.Basis ι K E) →
              [inst_3 : LinearOrder K] →
                [IsStrictOrderedRing K] → [FloorRing K] → [Fintype ι] → E → ↥(Submodule.span ℤ (Set.range ⇑b))
-- Mathlib.Tactic.FunProp.Mor
/-- Is `e` a coercion from some function space to functions?  -/
Mathlib.Meta.FunProp.Mor.isCoeFun : Lean.Expr → Lean.MetaM Bool
-- Mathlib.RingTheory.Extension.Generators
IsLocalization.Away.sec.congr_simp : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (x x_1 : R)
  (e_x : x = x_1) [inst_3 : IsLocalization.Away x S] (s s_1 : S),
  s = s_1 → IsLocalization.Away.sec x s = IsLocalization.Away.sec x_1 s_1
-- Mathlib.LinearAlgebra.Ray
eq_zero_of_sameRay_neg_smul_right : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {x : M} [IsDomain R] [Module.IsTorsionFree R M] {r : R},
  r < 0 → SameRay R x (r • x) → x = 0
-- Mathlib.Order.Hom.Lattice
SupHom.dual_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Max α] [inst_1 : Max β] [inst_2 : Max γ] (g : SupHom β γ)
  (f : SupHom α β), SupHom.dual (g.comp f) = (SupHom.dual g).comp (SupHom.dual f)
-- Std.Do.WP.Sound
_private.Std.Do.WP.Sound.0.Std.Do.instWPSoundExceptTExceptPureOfLawfulMonad.match_1.eq_1 : ∀ {ε α : Type u_1} (motive : Except ε α → Sort u_2) (a : α) (h_1 : (a : α) → motive (Except.ok a))
  (h_2 : (a : ε) → motive (Except.error a)),
  (match Except.ok a with
    | Except.ok a => h_1 a
    | Except.error a => h_2 a) =
    h_1 a
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.mapComp_hom_app : ∀ {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) (U : TopologicalSpace.Opens ↑Z),
  (TopologicalSpace.Opens.mapComp f g).hom.app U = CategoryTheory.eqToHom ⋯
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
/-- **Alias** of `CovariantDerivative.affineCombination`.

---

An affine combination of covariant derivatives as a covariant derivative.  -/
CovariantDerivative.affine_combination : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_3} →
            [inst_3 : TopologicalSpace H] →
              {I : ModelWithCorners 𝕜 E H} →
                {M : Type u_4} →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] →
                      {F : Type u_5} →
                        [inst_6 : NormedAddCommGroup F] →
                          [inst_7 : NormedSpace 𝕜 F] →
                            {V : M → Type u_6} →
                              [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)] →
                                [inst_9 : (x : M) → AddCommGroup (V x)] →
                                  [inst_10 : (x : M) → Module 𝕜 (V x)] →
                                    [inst_11 : (x : M) → TopologicalSpace (V x)] →
                                      [inst_12 : ∀ (x : M), IsTopologicalAddGroup (V x)] →
                                        [inst_13 : ∀ (x : M), ContinuousSMul 𝕜 (V x)] →
                                          [inst_14 : FiberBundle F V] →
                                            CovariantDerivative I F V →
                                              CovariantDerivative I F V → (M → 𝕜) → CovariantDerivative I F V
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.centerToCentroid_apply : ∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α] (z : ↥(NonUnitalSubsemiring.center α)) (a : α),
  (CentroidHom.centerToCentroid z) a = ↑z * a
-- Init.Data.Nat.Gcd
Nat.gcd_gcd_self_right_left : ∀ (m n : ℕ), m.gcd (m.gcd n) = m.gcd n
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get_eq_of_equiv : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] (h₁ : (↑m₁).WF) (h₂ : (↑m₂).WF) (h : (↑m₁).Equiv ↑m₂) {k : α}
  (h' : m₁.contains k = true),
  Std.DHashMap.Internal.Raw₀.Const.get m₁ k h' = Std.DHashMap.Internal.Raw₀.Const.get m₂ k ⋯
-- Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
/-- An additive which preserves homology preserves finite colimits.  -/
CategoryTheory.Functor.preservesFiniteColimits_of_preservesHomology : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [inst_4 : F.Additive] [F.PreservesHomology]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasFiniteCoproducts C]
  [CategoryTheory.Limits.HasCokernels C], CategoryTheory.Limits.PreservesFiniteColimits F
-- Mathlib.Algebra.Module.Submodule.Map
LinearMap.submoduleComap_apply_coe : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  (f : M →ₛₗ[σ₁₂] M₂) (q : Submodule R₂ M₂) (c : ↥(Submodule.comap f q)), ↑((f.submoduleComap q) c) = f ↑c
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
/-- The image of `Proj π J`  -/
Profinite.NobelingProof.π : {I : Type u} → Set (I → Bool) → (J : I → Prop) → [(i : I) → Decidable (J i)] → Set (I → Bool)
-- Mathlib.AlgebraicTopology.DoldKan.FunctorN
AlgebraicTopology.DoldKan.N₁_obj_X : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (X : CategoryTheory.SimplicialObject C),
  (AlgebraicTopology.DoldKan.N₁.obj X).X = AlgebraicTopology.AlternatingFaceMapComplex.obj X
-- Mathlib.Order.Heyting.Basic
hnot_hnot_hnot : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] (a : α), ￢￢￢a = ￢a
-- Mathlib.Topology.Compactness.SigmaCompact
/-- A subset `s` is σ-compact iff `s` (with the subspace topology) is a σ-compact space.  -/
isSigmaCompact_iff_isSigmaCompact_univ : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsSigmaCompact s ↔ IsSigmaCompact Set.univ
-- Lean.Elab.Deriving.Util
/-- Removes any `[expose]` section attributes when running `cont` if `typeName` has private ctors.
 -/
Lean.Elab.Deriving.withoutExposeFromCtors : {α : Type} → Lean.Name → Lean.Elab.Command.CommandElabM α → Lean.Elab.Command.CommandElabM α
-- Mathlib.RingTheory.PowerBasis
/-- Cannot be an instance because `PowerBasis` cannot be a class.  -/
PowerBasis.finite : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] (pb : PowerBasis R S),
  Module.Finite R S
-- Mathlib.Algebra.Order.BigOperators.Group.List
List.sum_le_sum : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M] [AddRightMono M] [AddLeftMono M] {l : List ι}
  {f g : ι → M}, (∀ i ∈ l, f i ≤ g i) → (List.map f l).sum ≤ (List.map g l).sum
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.checkNoWsBefore.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Category.HopfAlgCat.Basic
_private.Mathlib.Algebra.Category.HopfAlgCat.Basic.0.HopfAlgCat.mk.sizeOf_spec : ∀ {R : Type u} [inst : CommRing R] [inst_1 : SizeOf R] (carrier : Type v) [instRing : Ring carrier]
  [instHopfAlgebra : HopfAlgebra R carrier],
  sizeOf { carrier := carrier, instRing := instRing, instHopfAlgebra := instHopfAlgebra } =
    1 + sizeOf carrier + sizeOf instRing + sizeOf instHopfAlgebra
-- Mathlib.GroupTheory.ArchimedeanDensely
exists_pow_lt₀ : ∀ {G : Type u_1} [inst : LinearOrderedCommGroupWithZero G] [MulArchimedean G] {a : G},
  a < 1 → ∀ (b : Gˣ), ∃ n, a ^ n < ↑b
-- Mathlib.Algebra.MvPolynomial.PDeriv
MvPolynomial.pderiv_C : ∀ {R : Type u} {σ : Type v} {a : R} [inst : CommSemiring R] {i : σ}, (MvPolynomial.pderiv i) (MvPolynomial.C a) = 0
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.removeAssignment.eq_1 : ∀ (b : Bool) (a : Std.Tactic.BVDecide.LRAT.Internal.Assignment),
  Std.Tactic.BVDecide.LRAT.Internal.Assignment.removeAssignment b a =
    if b = true then a.removePosAssignment else a.removeNegAssignment
-- Mathlib.RingTheory.FractionalIdeal.Extended
/-- **Alias** of `FractionalIdeal.extendedHom_injective`. -/
FractionalIdeal.extendedHomₐ_injective : ∀ (A : Type u_1) (K : Type u_2) (L : Type u_3) (B : Type u_4) [inst : CommRing A] [inst_1 : IsDomain A]
  [inst_2 : CommRing B] [inst_3 : IsDomain B] [inst_4 : Algebra A B] [inst_5 : Module.IsTorsionFree A B]
  [inst_6 : Field K] [inst_7 : Field L] [inst_8 : Algebra A K] [inst_9 : Algebra B L] [inst_10 : IsFractionRing A K]
  [inst_11 : IsFractionRing B L] [inst_12 : Algebra K L] [inst_13 : Algebra A L] [IsScalarTower A B L]
  [IsScalarTower A K L] [Algebra.IsIntegral A B] [IsDedekindDomain A] [IsDedekindDomain B],
  Function.Injective fun I => (FractionalIdeal.extendedHom L B) I
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
/-- A functor to the category of comonoid objects can be translated as a comonoid object
in the functor category.  -/
CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverseObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.MonoidalCategory D] →
          CategoryTheory.Functor C (CategoryTheory.Comon D) → CategoryTheory.Comon (CategoryTheory.Functor C D)
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.ιTensorObj₄.congr_simp : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (X₁ X₂ X₃ X₄ : CategoryTheory.GradedObject I C)
  [inst_3 : X₃.HasTensor X₄] [inst_4 : X₂.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)]
  [inst_5 :
    X₁.HasTensor
      (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄))]
  (i₁ i₂ i₃ i₄ j : I) (h : i₁ + i₂ + i₃ + i₄ = j),
  CategoryTheory.GradedObject.Monoidal.ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h =
    CategoryTheory.GradedObject.Monoidal.ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h
-- Lean.Elab.Term.TermElabM
/-- Syntax tree of the tactic, stored and compared for incremental reuse.  -/
Lean.Elab.Tactic.TacticParsedSnapshotInner.stx : {α : Type} → Lean.Elab.Tactic.TacticParsedSnapshotInner α → Lean.Syntax
-- Mathlib.Order.Category.FinPartOrd
FinPartOrd.instCoeSortType : CoeSort FinPartOrd (Type u_1)
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.vaddInvariantMeasure_map_vadd : ∀ {M : Type uM} {N : Type uN} {α : Type uα} [inst : MeasurableSpace α] [inst_1 : VAdd M α] [inst_2 : VAdd N α]
  [VAddCommClass N M α] [MeasurableConstVAdd M α] [MeasurableConstVAdd N α] (μ : MeasureTheory.Measure α)
  [MeasureTheory.VAddInvariantMeasure M α μ] (n : N),
  MeasureTheory.VAddInvariantMeasure M α (MeasureTheory.Measure.map (fun x => n +ᵥ x) μ)
-- Mathlib.Data.Nat.Digits.Lemmas
List.fixedLengthDigits.congr_simp : ∀ {b b_1 : ℕ} (e_b : b = b_1) (hb : 1 < b) (l l_1 : ℕ),
  l = l_1 → List.fixedLengthDigits hb l = List.fixedLengthDigits ⋯ l_1
-- Mathlib.CategoryTheory.Limits.Types.Limits
/-- Given a section of a functor F into `Type*`,
construct a cone over F with `PUnit` as the cone point.  -/
CategoryTheory.Limits.Types.coneOfSection : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    {F : CategoryTheory.Functor J (Type u)} → {s : (j : J) → F.obj j} → s ∈ F.sections → CategoryTheory.Limits.Cone F
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
CategoryTheory.Iso.toIsometryEquiv_toFun : ∀ {R : Type u} [inst : CommRing R] {X Y : QuadraticModuleCat R} (i : X ≅ Y) (a : ↑X.toModuleCat),
  i.toIsometryEquiv a = (QuadraticModuleCat.Hom.toIsometry i.hom) a
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.add_apply : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (f g : StieltjesFunction R) (x : R),
  ↑(f + g) x = ↑f x + ↑g x
-- Mathlib.Control.LawfulFix
/-- `Sigma.curry` as a monotone function.  -/
Pi.monotoneCurry : (α : Type u_1) →
  (β : α → Type u_2) →
    (γ : (a : α) → β a → Type u_3) →
      [inst : (x : α) → (y : β x) → Preorder (γ x y)] →
        ((x : (a : α) × β a) → γ x.fst x.snd) →o (a : α) → (b : β a) → γ a b
-- Init.Data.Array.Basic
Array.instLE : {α : Type u} → [LT α] → LE (Array α)
-- Mathlib.Data.Nat.Cast.Commute
Commute.natCast_mul_self : ∀ {α : Type u_1} [inst : Semiring α] (a : α) (n : ℕ), Commute (↑n * a) a
-- Mathlib.MeasureTheory.Measure.Haar.Basic
/-- To show that an invariant σ-finite measure is regular it is sufficient to show that it is
finite on some compact set with non-empty interior.  -/
MeasureTheory.Measure.regular_of_isAddLeftInvariant : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [BorelSpace G] [SecondCountableTopology G] {μ : MeasureTheory.Measure G}
  [MeasureTheory.SigmaFinite μ] [μ.IsAddLeftInvariant] {K : Set G},
  IsCompact K → (interior K).Nonempty → μ K ≠ ⊤ → μ.Regular
-- Mathlib.Algebra.Group.ULift
ULift.inv.eq_1 : ∀ {α : Type u} [inst : Inv α], ULift.inv = { inv := fun f => { down := f.down⁻¹ } }
-- Mathlib.Data.Nat.Factorization.Basic
Nat.not_dvd_ordCompl : ∀ {n p : ℕ}, Nat.Prime p → n ≠ 0 → ¬p ∣ n / p ^ n.factorization p
-- Mathlib.Algebra.FreeAlgebra
/-- Zero in `Pre R X` defined as the image of `0` from `R`. Note: Used for notation only.  -/
FreeAlgebra.Pre.hasZero : (R : Type u_1) → (X : Type u_2) → [CommSemiring R] → Zero (FreeAlgebra.Pre R X)
-- Mathlib.Algebra.Order.Sub.Defs
add_le_add_add_tsub : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b c : α}
  [AddLeftMono α], a + b ≤ a + c + (b - c)
-- Init.Core
Std.LawfulRightIdentity.mk : ∀ {α : Sort u} {β : Sort u_1} {op : α → β → α} {o : outParam β} [toRightIdentity : Std.RightIdentity op o],
  (∀ (a : α), op a o = a) → Std.LawfulRightIdentity op o
-- Mathlib.CategoryTheory.Action.Basic
CategoryTheory.Functor.mapAction_obj_V : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {W : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} W] (F : CategoryTheory.Functor V W) (G : Type u_3) [inst_2 : Monoid G]
  (M : Action V G), ((F.mapAction G).obj M).V = F.obj M.V
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.Iter.length_eq_match_step.match_1.eq_2 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2) (it' : Std.Iter β)
  (h_1 : (it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.Iter β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.skip it' with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_2 it'
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.setENode : Lean.Expr → Lean.Meta.Grind.ENode → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Topology.Algebra.Group.Basic
/-- **Alias** of the forward direction of `continuous_inv_iff`. -/
Continuous.of_inv : ∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : InvolutiveInv G] [ContinuousInv G]
  [inst_3 : TopologicalSpace α] {f : α → G}, Continuous f⁻¹ → Continuous f
-- Mathlib.Analysis.Analytic.Constructions
FormalMultilinearSeries.prod.eq_1 : ∀ {𝕜 : Type u} {E : Type v} {F : Type w} {G : Type x} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : ContinuousAdd E] [inst_5 : ContinuousConstSMul 𝕜 E]
  [inst_6 : AddCommMonoid F] [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [inst_9 : ContinuousAdd F]
  [inst_10 : ContinuousConstSMul 𝕜 F] [inst_11 : AddCommMonoid G] [inst_12 : Module 𝕜 G] [inst_13 : TopologicalSpace G]
  [inst_14 : ContinuousAdd G] [inst_15 : ContinuousConstSMul 𝕜 G] (p : FormalMultilinearSeries 𝕜 E F)
  (q : FormalMultilinearSeries 𝕜 E G) (x : ℕ), p.prod q x = (p x).prod (q x)
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Multipliable.div : ∀ {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [inst : CommGroup α] [inst_1 : TopologicalSpace α]
  [IsTopologicalGroup α] {f g : β → α}, Multipliable f L → Multipliable g L → Multipliable (fun b => f b / g b) L
-- Mathlib.Data.List.Lemmas
List.foldr_range_eq_of_range_eq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : β → α → α} {g : γ → α → α},
  Set.range f = Set.range g → ∀ (a : α), Set.range (List.foldr f a) = Set.range (List.foldr g a)
-- Mathlib.Data.ENat.Lattice
/-- A version of `mul_iInf` with a slightly more general hypothesis.  -/
ENat.mul_iInf' : ∀ {ι : Sort u_2} {f : ι → ℕ∞} {a : ℕ∞}, (a = 0 → Nonempty ι) → a * ⨅ i, f i = ⨅ i, a * f i
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.HasFiniteRange.of_isNoetherian_rng : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [inst : Semiring K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [inst_3 : AddCommMonoid V₂] [inst_4 : Module K V₂] [IsNoetherian K V₂] {f : V →ₗ[K] V₂}, f.HasFiniteRange
-- Mathlib.RepresentationTheory.Continuous.TopRep
_private.Mathlib.RepresentationTheory.Continuous.TopRep.0.TopRep.mk.inj : ∀ {k : Type u} {G : Type v} {inst : Ring k} {inst_1 : TopologicalSpace k} {inst_2 : Monoid G} {V : Type w}
  {hV1 : AddCommGroup V} {hV2 : Module k V} {hV3 : TopologicalSpace V} {hV4 : IsTopologicalAddGroup V}
  {hV5 : ContinuousSMul k V} {ρ : ContRepresentation k G V} {V_1 : Type w} {hV1_1 : AddCommGroup V_1}
  {hV2_1 : Module k V_1} {hV3_1 : TopologicalSpace V_1} {hV4_1 : IsTopologicalAddGroup V_1}
  {hV5_1 : ContinuousSMul k V_1} {ρ_1 : ContRepresentation k G V_1},
  { V := V, hV1 := hV1, hV2 := hV2, hV3 := hV3, hV4 := hV4, hV5 := hV5, ρ := ρ } =
      { V := V_1, hV1 := hV1_1, hV2 := hV2_1, hV3 := hV3_1, hV4 := hV4_1, hV5 := hV5_1, ρ := ρ_1 } →
    V = V_1 ∧ hV1 ≍ hV1_1 ∧ hV2 ≍ hV2_1 ∧ hV3 ≍ hV3_1 ∧ ρ ≍ ρ_1
-- Mathlib.LinearAlgebra.Pi
LinearEquiv.sumArrowLequivProdArrow_apply_fst : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {α : Type u_5}
  {β : Type u_6} (f : α ⊕ β → M) (a : α), ((LinearEquiv.sumArrowLequivProdArrow α β R M) f).1 a = f (Sum.inl a)
-- Mathlib.RingTheory.UniqueFactorizationDomain.Defs
/-- Unique factorization monoids are defined as cancellative `CommMonoidWithZero`s with well-founded
strict divisibility relations, but this is equivalent to more familiar definitions:

Each element (except zero) is uniquely represented as a multiset of irreducible factors.
Uniqueness is only up to associated elements.

Each element (except zero) is non-uniquely represented as a multiset
of prime factors.

To define a UFD using the definition in terms of multisets
of irreducible factors, use the definition `of_existsUnique_irreducible_factors`

To define a UFD using the definition in terms of multisets
of prime factors, use the definition `of_exists_prime_factors`
 -/
UniqueFactorizationMonoid : (α : Type u_2) → [CommMonoidWithZero α] → Prop
-- Batteries.Data.Fin.Coding
/-- Decode `Empty` from `Fin 0`.  -/
Fin.decodeEmpty : Fin 0 → Empty
-- Mathlib.RingTheory.Filtration
Ideal.Filtration.smul_le : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (self : I.Filtration M) (i : ℕ), I • self.N i ≤ self.N (i + 1)
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.inr_injective : ∀ {R : Type u} {M : Type v} [inst : Zero R], Function.Injective TrivSqZeroExt.inr
-- Lean.Meta.Eqns
_private.Lean.Meta.Eqns.0.Lean.Meta.getEqnsFnsRef : IO.Ref (List Lean.Meta.GetEqnsFn)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.kernelCompMono_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y Z : C}
  (f : X ⟶ Y) (g : Y ⟶ Z) [inst_2 : CategoryTheory.Limits.HasKernel f] [inst_3 : CategoryTheory.Mono g],
  (CategoryTheory.Limits.kernelCompMono f g).hom =
    CategoryTheory.Limits.kernel.lift f (CategoryTheory.Limits.kernel.ι (CategoryTheory.CategoryStruct.comp f g)) ⋯
-- Mathlib.Analysis.InnerProductSpace.Projection.Submodule
ClosedSubmodule.orthogonal_orthogonal_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : ClosedSubmodule 𝕜 E) [(↑K).HasOrthogonalProjection], Kᗮᗮ = K
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.skeletonOfMono_obj_eq_top : ∀ {X Y : SSet} (i : X ⟶ Y) {d n : ℕ}, d < n → ((SSet.skeletonOfMono i) n).obj (Opposite.op { len := d }) = ⊤
-- Init.Conv
/-- The `*` occurrence list means to apply to all occurrences of the pattern.  -/
Lean.Parser.Tactic.Conv.occsWildcard : Lean.ParserDescr
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
IsUniformAddGroup.to_topologicalAddGroup : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α], IsTopologicalAddGroup α
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
Birkhoff_inequalities : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddCommGroup α] [AddLeftMono α] (a b c : α),
  |a ⊔ c - b ⊔ c| ⊔ |a ⊓ c - b ⊓ c| ≤ |a - b|
-- Mathlib.Analysis.AbsoluteValue.Equivalence
AbsoluteValue.instSetoid : {R : Type u_1} →
  [inst : Semiring R] → {S : Type u_2} → [inst_1 : Semiring S] → [inst_2 : PartialOrder S] → Setoid (AbsoluteValue R S)
-- Mathlib.Analysis.Analytic.ConvergenceRadius
FormalMultilinearSeries.le_radius_of_summable_norm : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {r : NNReal}
  (p : FormalMultilinearSeries 𝕜 E F), (Summable fun n => ‖p n‖ * ↑r ^ n) → ↑r ≤ p.radius
-- Std.Sat.AIG.RefVec
Std.Sat.AIG.BinaryRefVec.rhs_get_cast : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len : ℕ} {aig1 aig2 : Std.Sat.AIG α}
  (s : aig1.BinaryRefVec len) (idx : ℕ) (hidx : idx < len) (hcast : aig1.decls.size ≤ aig2.decls.size),
  (s.cast hcast).rhs.get idx hidx = (s.rhs.get idx hidx).cast hcast
-- Mathlib.MeasureTheory.Function.Jacobian
MeasureTheory.lintegral_abs_det_fderiv_le_addHaar_image : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E}
  {f : E → E} {f' : E → E →L[ℝ] E} [inst_3 : MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E)
  [μ.IsAddHaarMeasure],
  MeasurableSet s →
    (∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) →
      Set.InjOn f s → ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ ≤ μ (f '' s)
-- Mathlib.FieldTheory.AbelRuffini
gal_zero_isSolvable : ∀ {F : Type u_1} [inst : Field F], Group.IsSolvable (Polynomial.Gal 0)
-- Mathlib.Analysis.Calculus.Deriv.Add
HasDerivWithinAt.neg : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s : Set 𝕜},
  HasDerivWithinAt f f' s x → HasDerivWithinAt (-f) (-f') s x
-- Mathlib.Analysis.CStarAlgebra.Classes
CStarAlgebra.toCompleteSpace : ∀ {A : Type u_1} [self : CStarAlgebra A], CompleteSpace A
-- Mathlib.Order.Heyting.Basic
hnot_le_iff_codisjoint_right : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] {a b : α}, ￢b ≤ a ↔ Codisjoint b a
-- Mathlib.GroupTheory.GroupExtension.Basic
GroupExtension.Section.exists_mul_eq_inl_mul_mul : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {E : Type u_3} [inst_2 : Group E]
  {S : GroupExtension N E G} (σ : S.Section) (g₁ g₂ : G), ∃ n, σ (g₁ * g₂) = S.inl n * σ g₁ * σ g₂