mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Coset.Basic
Subgroup.quotientiInfEmbedding_apply : ∀ {α : Type u_1} [inst : Group α] {ι : Type u_2} (f : ι → Subgroup α) (q : α ⧸ ⨅ i, f i) (i : ι),
  (Subgroup.quotientiInfEmbedding f) q i = Subgroup.quotientMapOfLE ⋯ q
-- Init.Data.UInt.Lemmas
UInt64.toUInt16_le : ∀ {a b : UInt64}, a.toUInt16 ≤ b.toUInt16 ↔ a % 65536 ≤ b % 65536
-- Mathlib.Analysis.Normed.Module.WeakDual
/-- The image under `↑ : StrongDual 𝕜 E → (E → 𝕜)` of a polar `polar 𝕜 s` of a
neighborhood `s` of the origin is a closed set.  -/
NormedSpace.Dual.isClosed_image_polar_of_mem_nhds : ∀ (𝕜 : Type u_1) {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E}, s ∈ nhds 0 → IsClosed (DFunLike.coe '' StrongDual.polar 𝕜 s)
-- Mathlib.Data.Finset.Empty
Finset.Nonempty.ne_empty : ∀ {α : Type u_1} {s : Finset α}, s.Nonempty → s ≠ ∅
-- Mathlib.Order.Filter.AtTopBot.Finite
Filter.Eventually.atTop_of_arithmetic : ∀ {p : ℕ → Prop} {n : ℕ}, n ≠ 0 → (∀ k < n, ∀ᶠ (a : ℕ) in Filter.atTop, p (n * a + k)) → ∀ᶠ (a : ℕ) in Filter.atTop, p a
-- Mathlib.Combinatorics.SetFamily.KruskalKatona
/-- These are the compressions which we will apply to decrease the "measure" of a family of sets.  -/
_private.Mathlib.Combinatorics.SetFamily.KruskalKatona.0.Finset.UV.UsefulCompression : {α : Type u_1} → [LinearOrder α] → Finset α → Finset α → Prop
-- Lean.MetavarContext
Lean.MetavarKind.natural.sizeOf_spec : sizeOf Lean.MetavarKind.natural = 1
-- Lean.MetavarContext
Lean.MetavarDecl.kind : Lean.MetavarDecl → Lean.MetavarKind
-- Mathlib.Analysis.Complex.Trigonometric
Complex.cosh_neg : ∀ (x : ℂ), Complex.cosh (-x) = Complex.cosh x
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.MVarErrorInfo.mk.inj : ∀ {mvarId : Lean.MVarId} {ref : Lean.Syntax} {kind : Lean.Elab.Term.MVarErrorKind} {mvarId_1 : Lean.MVarId}
  {ref_1 : Lean.Syntax} {kind_1 : Lean.Elab.Term.MVarErrorKind},
  { mvarId := mvarId, ref := ref, kind := kind } = { mvarId := mvarId_1, ref := ref_1, kind := kind_1 } →
    mvarId = mvarId_1 ∧ ref = ref_1 ∧ kind = kind_1
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.sign_two_zsmul_eq_neg_sign_iff : ∀ {θ : Real.Angle}, (2 • θ).sign = -θ.sign ↔ θ = 0 ∨ Real.pi / 2 < |θ.toReal|
-- Mathlib.AlgebraicGeometry.Morphisms.FlatRank
/-- A finite flat locally finitely presented morphism is surjective if and only if its rank
function is at least `1` everywhere.  -/
AlgebraicGeometry.Scheme.Hom.one_le_finrank_iff_surjective : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.Flat f] [AlgebraicGeometry.IsFinite f],
  1 ≤ AlgebraicGeometry.Scheme.Hom.finrank f ↔ AlgebraicGeometry.Surjective f
-- Mathlib.Topology.Closure
closure_interior_idem : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, closure (interior (closure (interior s))) = closure (interior s)
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
/-- `padicValRat p q` is symmetric in `q`.  -/
padicValRat.neg : ∀ {p : ℕ} (q : ℚ), padicValRat p (-q) = padicValRat p q
-- Mathlib.Data.Fin.Basic
Fin.coe_int_add_eq_ite : ∀ {n : ℕ} (u v : Fin n), ↑↑(u + v) = if ↑u + ↑v < n then ↑↑u + ↑↑v else ↑↑u + ↑↑v - ↑n
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.zero_hom₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C} [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive],
  CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ 0 = 0
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- An auxiliary tactic closing goals `UniqueDiffWithinAt ℝ s a` where
`s ∈ {Iic a, Ici a, univ}`.  -/
intervalIntegral.tacticUniqueDiffWithinAt_Ici_Iic_univ : Lean.ParserDescr
-- Lean.Elab.MutualDef
Lean.Elab.Term.MutualClosure.pushMain : Array Lean.Elab.PreDefinition →
  Array Lean.Expr →
    Array Lean.Elab.DefViewElabHeader → Array Lean.Expr → Lean.Elab.TermElabM (Array Lean.Elab.PreDefinition)
-- Mathlib.Algebra.Group.AddChar
AddChar.injective_iff : ∀ {A : Type u_1} {M : Type u_2} [inst : AddCommGroup A] [inst_1 : DivisionCommMonoid M] {ψ : AddChar A M},
  Function.Injective ⇑ψ ↔ ∀ ⦃x : A⦄, ψ x = 1 → x = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanShape.ofLinearOrder_L : ∀ (ι : Type w) [inst : LinearOrder ι], (CategoryTheory.Limits.MultispanShape.ofLinearOrder ι).L = ↑{x | x.1 < x.2}
-- Mathlib.GroupTheory.Perm.Centralizer
/-- Computes the range of `Equiv.Perm.toPermHom g`  -/
Equiv.Perm.OnCycleFactors.range_toPermHom_eq_range_toPermHom' : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {g : Equiv.Perm α},
  (Equiv.Perm.OnCycleFactors.toPermHom g).range = Equiv.Perm.OnCycleFactors.range_toPermHom' g
-- Mathlib.Topology.Spectral.Hom
/-- `id` as a `SpectralMap`.  -/
SpectralMap.id : (α : Type u_2) → [inst : TopologicalSpace α] → SpectralMap α α
-- Lean.Parser.Do
Lean.Parser.Term.doRepeatUntil.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.Pos.revSkip?_bool_eq_none_iff : ∀ {p : Char → Bool} {s : String.Slice} {pos : s.Pos},
  pos.revSkip? p = none ↔ ∀ (h : pos ≠ s.startPos), p ((pos.prev h).get ⋯) = false
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
surjective_of_linearIndependent_of_span : ∀ {ι : Type u'} {ι' : Type u_1} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [Nontrivial R],
  LinearIndependent R v →
    ∀ (f : ι' ↪ ι), Set.range v ⊆ ↑(Submodule.span R (Set.range (v ∘ ⇑f))) → Function.Surjective ⇑f
-- Mathlib.Geometry.Manifold.GroupLieAlgebra
addInvariantVectorField.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : AddGroup G] (v : AddGroupLieAlgebra I G) (g : G),
  addInvariantVectorField v g = ((mfderiv% fun x => g + x) 0) v
-- Mathlib.CategoryTheory.Filtered.Small
CategoryTheory.IsCofiltered.eq.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsCofilteredOrEmpty C] {j j' : C}
  (f f_1 : j ⟶ j'),
  f = f_1 →
    ∀ (f' f'_1 : j ⟶ j'), f' = f'_1 → CategoryTheory.IsCofiltered.eq f f' = CategoryTheory.IsCofiltered.eq f_1 f'_1
-- Mathlib.CategoryTheory.Monoidal.CommMon_
/-- Commutative monoid objects in `C` are "just" braided lax monoidal functors from the trivial
braided monoidal category to `C`.
 -/
CategoryTheory.CommMon.equivLaxBraidedFunctorPUnit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        CategoryTheory.LaxBraidedFunctor (CategoryTheory.Discrete PUnit.{u + 1}) C ≌ CategoryTheory.CommMon C
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imI_add : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : Add R] (a b : QuaternionAlgebra R c₁ c₂ c₃), (a + b).imI = a.imI + b.imI
-- Mathlib.Combinatorics.Additive.Energy
Finset.mulEnergy.congr_simp : ∀ {α : Type u_1} {inst : DecidableEq α} [inst_1 : DecidableEq α] [inst_2 : Mul α] (s s_1 : Finset α),
  s = s_1 → ∀ (t t_1 : Finset α), t = t_1 → s.mulEnergy t = s_1.mulEnergy t_1
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.matrixEquiv_symm_apply : ∀ {J : Type} [inst : Finite J] {K : Type} [inst_1 : Finite K] {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {f : J → C}
  {g : K → C} (m : (j : J) → (k : K) → f j ⟶ g k),
  CategoryTheory.Limits.biproduct.matrixEquiv.symm m = CategoryTheory.Limits.biproduct.matrix m
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.preservesTerminalIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) F],
  (CategoryTheory.CartesianMonoidalCategory.preservesTerminalIso F).hom =
    CategoryTheory.CartesianMonoidalCategory.terminalComparison F
-- Mathlib.Analysis.Analytic.Basic
/-- If `f` has formal power series `∑ n, pₙ` at `x`, then
`f y - f z - p 1 (fun _ ↦ y - z) = O(‖(y, z) - (x, x)‖ * ‖y - z‖)` as `(y, z) → (x, x)`.
In particular, `f` is strictly differentiable at `x`.  -/
HasFPowerSeriesAt.isBigO_image_sub_norm_mul_norm_sub : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E},
  HasFPowerSeriesAt f p x →
    (fun y => f y.1 - f y.2 - (p 1) fun x => y.1 - y.2) =O[nhds (x, x)] fun y => ‖y - (x, x)‖ * ‖y.1 - y.2‖
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
BddBelow.range_add : ∀ {ι : Type u_1} {M : Type u_3} [inst : Add M] [inst_1 : Preorder M] [AddLeftMono M] [AddRightMono M] {f g : ι → M},
  BddBelow (Set.range f) → BddBelow (Set.range g) → BddBelow (Set.range fun i => f i + g i)
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.instInhabitedLambdaTheorems.default : Mathlib.Meta.FunProp.LambdaTheorems
-- Mathlib.RingTheory.Etale.Finite
/-- If `Ω` is separably closed, the fiber `S →ₐ[R] Ω`
is isomorphic to the prime spectrum of the base change `Ω ⊗[R] S`.  -/
CommAlgCat.FiniteEtale.fiberIsoComp : (R : Type u) →
  [inst : CommRing R] →
    (Ω : Type w) →
      [inst_1 : Field Ω] →
        [inst_2 : Algebra R Ω] →
          [IsSepClosed Ω] →
            CommAlgCat.FiniteEtale.fiber R Ω ≅
              (CommAlgCat.FiniteEtale.baseChange R Ω).op.comp (CommAlgCat.FiniteEtale.finiteSpec Ω)
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
CategoryTheory.Grpd.freeForgetAdjunction_counit_app : ∀ {D : Type u} [inst : CategoryTheory.Groupoid D],
  CategoryTheory.Grpd.freeForgetAdjunction.counit.app (CategoryTheory.Grpd.of D) =
    CategoryTheory.FreeGroupoid.lift (CategoryTheory.Functor.id D)
-- Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd
Measure.ext_of_integral_prod_mul_boundedContinuousFunction' : ∀ {ι : Type u_1} {T : Type u_4} {X : ι → Type u_5} {mX : (i : ι) → MeasurableSpace (X i)}
  [inst : (i : ι) → TopologicalSpace (X i)] [∀ (i : ι), BorelSpace (X i)] [∀ (i : ι), HasOuterApproxClosed (X i)]
  {mT : MeasurableSpace T} [inst_3 : TopologicalSpace T] [BorelSpace T] [HasOuterApproxClosed T] [Finite ι]
  {μ ν : MeasureTheory.Measure (((i : ι) → X i) × T)} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν],
  (∀ (f : BoundedContinuousFunction ((i : ι) → X i) ℝ) (g : BoundedContinuousFunction T ℝ),
      ∫ (p : ((i : ι) → X i) × T), f p.1 * g p.2 ∂μ = ∫ (p : ((i : ι) → X i) × T), f p.1 * g p.2 ∂ν) →
    μ = ν
-- Mathlib.Algebra.Regular.Basic
IsAddRightRegular.nsmul_iff : ∀ {R : Type u_1} [inst : AddMonoid R] {a : R} {n : ℕ}, 0 < n → (IsAddRightRegular (n • a) ↔ IsAddRightRegular a)
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.prod_contLinear : ∀ {k : Type u_10} {P₁ : Type u_11} {P₂ : Type u_12} {P₃ : Type u_13} {V₁ : Type u_15} {V₂ : Type u_16} {V₃ : Type u_17}
  [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁]
  [inst_4 : TopologicalSpace P₁] [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂]
  [inst_8 : TopologicalSpace P₂] [inst_9 : AddCommGroup V₃] [inst_10 : Module k V₃] [inst_11 : AddTorsor V₃ P₃]
  [inst_12 : TopologicalSpace P₃] [inst_13 : TopologicalSpace V₁] [inst_14 : IsTopologicalAddTorsor P₁]
  [inst_15 : TopologicalSpace V₂] [inst_16 : IsTopologicalAddTorsor P₂] [inst_17 : TopologicalSpace V₃]
  [inst_18 : IsTopologicalAddTorsor P₃] (f : P₁ →ᴬ[k] P₂) (g : P₁ →ᴬ[k] P₃),
  (f.prod g).contLinear = f.contLinear.prod g.contLinear
-- Lean.Meta.Tactic.Grind.Arith.Linear.Reify
_private.Lean.Meta.Tactic.Grind.Arith.Linear.Reify.0.Lean.Meta.Grind.Arith.Linear.reify?.asTopVar : Bool → ℕ → Lean.Expr → Lean.Meta.Grind.Arith.Linear.LinearM (Option Lean.Meta.Grind.Arith.Linear.LinExpr)
-- Mathlib.Algebra.Lie.Basic
LieModuleHom.congr_fun : ∀ {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 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] {f g : M →ₗ⁅R,L⁆ N}, f = g → ∀ (x : M), f x = g x
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubgroup.mem_ofAddUnits_iff_exists_isAddUnit : ∀ {M : Type u_1} [inst : AddMonoid M] (S : AddSubgroup (AddUnits M)) (x : M),
  x ∈ S.ofAddUnits ↔ ∃ (h : IsAddUnit x), h.addUnit ∈ S
-- Mathlib.Tactic.Sat.FromLRAT
Mathlib.Tactic.Sat.Clause.mk : Array ℤ → Lean.Expr → Lean.Expr → Mathlib.Tactic.Sat.Clause
-- Mathlib.SetTheory.Cardinal.Aleph
/-- **Alias** of the reverse direction of `Ordinal.mem_range_preOmega_iff`. -/
Ordinal.IsInitial.mem_range_preOmega : ∀ {x : Ordinal.{u_1}}, x.IsInitial → x ∈ Set.range ⇑Ordinal.preOmega
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.entryAtIdx.induct_unfolding : ∀ {α : Type u} {β : α → Type v}
  (motive : (t : Std.DTreeMap.Internal.Impl α β) → t.Balanced → (n : ℕ) → n < t.size → (a : α) × β a → Prop),
  (∀ (size : ℕ) (k : α) (v : β k) (l' r' : Std.DTreeMap.Internal.Impl α β)
      (hl : (Std.DTreeMap.Internal.Impl.inner size k v l' r').Balanced) (n : ℕ)
      (h : n < (Std.DTreeMap.Internal.Impl.inner size k v l' r').size) (h_1 : compare n l'.size = Ordering.lt),
      motive l' ⋯ n ⋯ (l'.entryAtIdx ⋯ n ⋯) →
        motive (Std.DTreeMap.Internal.Impl.inner size k v l' r') hl n h (l'.entryAtIdx ⋯ n ⋯)) →
    (∀ (size : ℕ) (k : α) (v : β k) (l' r' : Std.DTreeMap.Internal.Impl α β)
        (hl : (Std.DTreeMap.Internal.Impl.inner size k v l' r').Balanced) (n : ℕ)
        (h : n < (Std.DTreeMap.Internal.Impl.inner size k v l' r').size),
        compare n l'.size = Ordering.eq → motive (Std.DTreeMap.Internal.Impl.inner size k v l' r') hl n h ⟨k, v⟩) →
      (∀ (size : ℕ) (k : α) (v : β k) (l' r' : Std.DTreeMap.Internal.Impl α β)
          (hl : (Std.DTreeMap.Internal.Impl.inner size k v l' r').Balanced) (n : ℕ)
          (h : n < (Std.DTreeMap.Internal.Impl.inner size k v l' r').size) (h_1 : compare n l'.size = Ordering.gt),
          motive r' ⋯ (n - l'.size - 1) ⋯ (r'.entryAtIdx ⋯ (n - l'.size - 1) ⋯) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v l' r') hl n h (r'.entryAtIdx ⋯ (n - l'.size - 1) ⋯)) →
        ∀ (t : Std.DTreeMap.Internal.Impl α β) (hl : t.Balanced) (n : ℕ) (h : n < t.size),
          motive t hl n h (t.entryAtIdx hl n h)
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblen_add_one : ∀ (o : Ordinal.{u_1}), Ordinal.veblen (o + 1) = Ordinal.deriv (Ordinal.veblen o)
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
/-- A category `HasFiniteWidePullbacks` if it has all limits of shape `WidePullbackShape J` for
finite `J`, i.e. if it has a wide pullback for every finite collection of morphisms with the same
codomain.  -/
CategoryTheory.Limits.HasFiniteWidePullbacks : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Mathlib.ModelTheory.Equivalence
FirstOrder.Language.Theory.Imp.instIsTransBoundedFormula : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ}, IsTrans (L.BoundedFormula α n) T.Imp
-- Lean.Parser.Term
Lean.Parser.Term.matchAlt.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.smulCommClass_left : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {X : Type u_5} {Y : Type u_4}
  [inst_3 : SMul L Y] [inst_4 : SMul X Y] [SMulCommClass L X Y] (F : IntermediateField K L), SMulCommClass (↥F) X Y
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
selfAdjointMatricesSubmodule.eq_1 : ∀ {R : Type u_1} {n : Type u_11} [inst : CommRing R] [inst_1 : Fintype n] (J : Matrix n n R) [inst_2 : DecidableEq n],
  selfAdjointMatricesSubmodule J = pairSelfAdjointMatricesSubmodule J J
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.coe_sup : ∀ {α : Type u_1} [inst : TopologicalSpace α] (s t : TopologicalSpace.Compacts α), ↑(s ⊔ t) = ↑s ∪ ↑t
-- Mathlib.RepresentationTheory.Rep.Basic
/-- the underlying representation of an object in `Rep k G`  -/
Rep.ρ : {k : Type u} →
  {G : Type v} → [inst : Semiring k] → [inst_1 : Monoid G] → (self : Rep.{w, u, v} k G) → Representation k G ↑self
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.Substring.Raw.take.eq_1 : ∀ (x : ℕ) (s : String) (b e : String.Pos.Raw),
  { str := s, startPos := b, stopPos := e }.take x =
    { str := s, startPos := b, stopPos := ({ str := s, startPos := b, stopPos := e }.nextn x 0).offsetBy b }
-- Mathlib.Algebra.Ring.InjSurj
/-- Pushforward a `NonAssocSemiring` instance along a surjective function.  -/
Function.Surjective.nonAssocSemiring : {R : Type u_1} →
  {S : Type u_2} →
    (f : R → S) →
      Function.Surjective f →
        [inst : Add S] →
          [inst_1 : Mul S] →
            [inst_2 : Zero S] →
              [inst_3 : One S] →
                [inst_4 : SMul ℕ S] →
                  [inst_5 : NatCast S] →
                    [inst_6 : NonAssocSemiring R] →
                      f 0 = 0 →
                        f 1 = 1 →
                          (∀ (x y : R), f (x + y) = f x + f y) →
                            (∀ (x y : R), f (x * y) = f x * f y) →
                              (∀ (n : ℕ) (x : R), f (n • x) = n • f x) → (∀ (n : ℕ), f ↑n = ↑n) → NonAssocSemiring S
-- Batteries.Recycling.RBTree.Basic
/-- The result of `toStream` on a `Keys`.  -/
RBTree.RBMap.Keys.Stream : Type u_1 → Type u_2 → Type (max u_2 u_1)
-- Mathlib.Order.Nucleus
Nucleus.mem_range : ∀ {X : Type u_1} [inst : Order.Frame X] {n : Nucleus X} {x : X}, x ∈ Set.range ⇑n ↔ n x = x
-- Mathlib.NumberTheory.Padics.PadicNumbers
_private.Mathlib.NumberTheory.Padics.PadicNumbers.0.PadicSeq.norm_nonarchimedean_aux : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {f g : PadicSeq p}, ¬f + g ≈ 0 → ¬f ≈ 0 → ¬g ≈ 0 → (f + g).norm ≤ max f.norm g.norm
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.Hexagon.functor₁₂₃_map_app_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X₁ Y₁ : C}
  (φ : X₁ ⟶ Y₁) (X₂ X₃ : C),
  (((CategoryTheory.BraidedCategory.Hexagon.functor₁₂₃ C).map φ).app X₂).app X₃ =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight φ X₂) X₃
-- Mathlib.Algebra.ContinuedFractions.Computation.Translations
_private.Mathlib.Algebra.ContinuedFractions.Computation.Translations.0.Option.getD.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (opt : Option α) → ((x : α) → motive (some x)) → (Unit → motive none) → motive opt
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.star_eq_conjTranspose : ∀ {m : Type u_2} {α : Type v} [inst : Star α] (M : Matrix m m α), star M = M.conjTranspose
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.equiv_toEmbedding_trans_symm_toEmbedding : ∀ {α : Sort u_1} {β : Sort u_2} (e : α ≃ β), e.toEmbedding.trans e.symm.toEmbedding = Function.Embedding.refl α
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
/-- Auxiliary definition for `sheafifyAdjunctionOfIsEquivalence`.  -/
CategoryTheory.Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (J : CategoryTheory.GrothendieckTopology C) →
          (K : CategoryTheory.GrothendieckTopology D) →
            (G : CategoryTheory.Functor C D) →
              {A : Type u_4} →
                [inst_2 : CategoryTheory.Category.{v_4, u_4} A] →
                  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J K G] →
                    [inst_4 : (G.sheafPushforwardContinuous A J K).IsEquivalence] →
                      [inst_5 : CategoryTheory.HasWeakSheafify J A] →
                        {P : CategoryTheory.Functor Dᵒᵖ A} →
                          {Q : CategoryTheory.Sheaf K A} →
                            ((CategoryTheory.Functor.IsDenseSubsite.sheafifyOfIsEquivalence J K G A).obj P ⟶ Q) ≃
                              (P ⟶ Q.obj)
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- `I ^ n ⧸ I ^ (n + 1)` can be viewed as a quotient module and as ideal of `R ⧸ I ^ (n + 1)`.
This definition gives the `R`-linear equivalence between the two.  -/
Ideal.powQuotPowSuccLinearEquivMapMkPowSuccPow : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) → (n : ℕ) → (↥(I ^ n) ⧸ I • ⊤) ≃ₗ[R] ↥(Ideal.map (Ideal.Quotient.mk (I ^ (n + 1))) (I ^ n))
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.maxD_eq_iff_mem_and_forall : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [Std.LawfulEqCmp cmp],
  t ≠ ∅ → ∀ {km fallback : α}, t.maxD fallback = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.Algebra.Notation.Prod
Prod.mk_eq_one : ∀ {M : Type u_3} {N : Type u_4} [inst : One M] [inst_1 : One N] {x : M} {y : N}, (x, y) = 1 ↔ x = 1 ∧ y = 1
-- Mathlib.Order.Interval.Basic
NonemptyInterval.instSemilatticeSup : {α : Type u_1} → [inst : Lattice α] → SemilatticeSup (NonemptyInterval α)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.eq_le_subst : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α] [inst_1 : LE α] [inst_2 : Std.IsPreorder α] [Lean.Grind.OrderedAdd α]
  (ctx : Lean.Grind.Linarith.Context α) (x : Lean.Grind.Linarith.Var) (p₁ p₂ p₃ : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.eq_le_subst_cert x p₁ p₂ p₃ = true →
    Lean.Grind.Linarith.Poly.denote' ctx p₁ = 0 →
      Lean.Grind.Linarith.Poly.denote' ctx p₂ ≤ 0 → Lean.Grind.Linarith.Poly.denote' ctx p₃ ≤ 0
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.List.takeWhile_go_toArray : ∀ {α : Type u_1} {r : Array α} (p : α → Bool) (l : List α) (i : ℕ),
  Array.takeWhile.go✝ p l.toArray i r = r ++ (List.takeWhile p (List.drop i l)).toArray
-- Lean.Elab.DefView
Lean.Elab.BodyProcessedSnapshot.mk : Lean.Language.Snapshot →
  Lean.Elab.Term.SavedState →
    Lean.Expr → Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree) → Lean.Elab.BodyProcessedSnapshot
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.flipEquiv_symm_apply : ∀ (ι : Type u_1) (R : Type u_2) (M : Type u_3) (N : Type u_4) [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N),
  (RootPairing.flipEquiv ι R M N).symm P = P.flip
-- Mathlib.Topology.Neighborhoods
tendsto_nhds_of_eventually_eq : ∀ {X : Type u} [inst : TopologicalSpace X] {α : Type u_1} {x : X} {l : Filter α} {f : α → X},
  (∀ᶠ (x' : α) in l, f x' = x) → Filter.Tendsto f l (nhds x)
-- Mathlib.NumberTheory.RamificationInertia.Ramification
Ideal.IsDedekindDomain.ramificationIdx'_eq_one_iff : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsDedekindDomain S]
  {p : Ideal R} {P : Ideal S} [inst_4 : P.IsPrime],
  P ≠ ⊥ →
    Ideal.map (algebraMap R S) p ≤ P →
      (p.ramificationIdx' P = 1 ↔
        Ideal.map (algebraMap R (Localization.AtPrime P)) p = IsLocalRing.maximalIdeal (Localization.AtPrime P))
-- Mathlib.Analysis.SpecialFunctions.Sqrt
ContDiffAt.sqrt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {n : WithTop ℕ∞} {x : E},
  ContDiffAt ℝ n f x → f x ≠ 0 → ContDiffAt ℝ n (fun y => √(f y)) x
-- Mathlib.Algebra.Free
FreeAddSemigroup.length_add : ∀ {α : Type u} (x y : FreeAddSemigroup α), (x + y).length = x.length + y.length
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalNat_i₁ : ∀ (pq : ℕ × ℕ), CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalNat.i₁ pq = WithBotTop.coe ↑pq.2
-- Batteries.Data.Array.Match
Array.instInhabitedPrefixTable : {α : Type u_1} → Inhabited (Array.PrefixTable α)