mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Set.Operations
/-- Given a map `f` sending `s : Set α` into `t : Set β`, restrict domain of `f` to `s`
and the codomain to `t`. Same as `Subtype.map`.  -/
Set.MapsTo.restrict : {α : Type u} → {β : Type v} → (f : α → β) → (s : Set α) → (t : Set β) → Set.MapsTo f s t → ↑s → ↑t
-- Init.Data.List.Lex
List.ltIrrefl : ∀ {α : Type u_1} [inst : LT α] [Std.Irrefl fun x1 x2 => x1 < x2], Std.Irrefl fun x1 x2 => x1 < x2
-- Mathlib.Algebra.Colimit.DirectLimit
/-- `map₀` as an `AddMonoidHom`.  -/
DirectLimit.map₀AddMonoidHom : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        (f : (x x_1 : ι) → (h : x ≤ x_1) → T h) →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [inst_4 : Nonempty ι] →
                  [inst_5 : (i : ι) → AddZeroClass (G i)] →
                    [inst_6 : ∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] →
                      ((i : ι) → G i) →+ DirectLimit G f
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.CommSemiring.mk.inj : ∀ {toSemiring : Lean.Meta.Grind.Arith.CommRing.Semiring} {ringId : ℕ} {commSemiringInst : Lean.Expr}
  {addRightCancelInst? : Option (Option Lean.Expr)} {toQFn? : Option Lean.Expr}
  {toSemiring_1 : Lean.Meta.Grind.Arith.CommRing.Semiring} {ringId_1 : ℕ} {commSemiringInst_1 : Lean.Expr}
  {addRightCancelInst?_1 : Option (Option Lean.Expr)} {toQFn?_1 : Option Lean.Expr},
  { toSemiring := toSemiring, ringId := ringId, commSemiringInst := commSemiringInst,
        addRightCancelInst? := addRightCancelInst?, toQFn? := toQFn? } =
      { toSemiring := toSemiring_1, ringId := ringId_1, commSemiringInst := commSemiringInst_1,
        addRightCancelInst? := addRightCancelInst?_1, toQFn? := toQFn?_1 } →
    toSemiring = toSemiring_1 ∧
      ringId = ringId_1 ∧
        commSemiringInst = commSemiringInst_1 ∧ addRightCancelInst? = addRightCancelInst?_1 ∧ toQFn? = toQFn?_1
-- Mathlib.Tactic.ClickSuggestions.GRewrite
Mathlib.Tactic.ClickSuggestions.GrwPos.mk.sizeOf_spec : ∀ (relName : Lean.Name) (relation : Lean.Expr) (symm? : Option Bool),
  sizeOf { relName := relName, relation := relation, symm? := symm? } =
    1 + sizeOf relName + sizeOf relation + sizeOf symm?
-- Mathlib.Algebra.Group.Action.Faithful
/-- `Mul.toSMulMulOpposite` is faithful when there is a (left) identity.  -/
instFaithfulSMulMulOpposite : ∀ (R : Type u_4) [inst : MulOneClass R], FaithfulSMul Rᵐᵒᵖ R
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
/-- The angle between the negation of a vector and another vector.  -/
InnerProductGeometry.angle_neg_left : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V),
  InnerProductGeometry.angle (-x) y = Real.pi - InnerProductGeometry.angle x y
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.destruct_append.aux.eq_1 : ∀ {α : Type u} (t : Stream'.WSeq α), Stream'.WSeq.destruct_append.aux t none = t.destruct
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.ExtensionState.mk.sizeOf_spec : ∀ {γ : Type} [inst : SizeOf γ] (newEntries : List Lean.KeyedDeclsAttribute.OLeanEntry)
  (table : Lean.KeyedDeclsAttribute.Table γ) (declNames erased : Lean.PHashSet Lean.Name),
  sizeOf { newEntries := newEntries, table := table, declNames := declNames, erased := erased } =
    1 + sizeOf newEntries + sizeOf table + sizeOf declNames + sizeOf erased
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Iso.reachable_iff : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {φ : G ≃g G'} {u v : V},
  G'.Reachable (φ u) (φ v) ↔ G.Reachable u v
-- Init.Data.SInt.Basic
instAddInt16 : Add Int16
-- Mathlib.Topology.NoetherianSpace
TopologicalSpace.noetherianSpace_iff_isCompact : ∀ {α : Type u_1} [inst : TopologicalSpace α], TopologicalSpace.NoetherianSpace α ↔ ∀ (s : Set α), IsCompact s
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.isClique_pair : ∀ {α : Type u_1} {G : SimpleGraph α} {a b : α}, G.IsClique {a, b} ↔ a ≠ b → G.Adj a b
-- Lean.Meta.Hint
_private.Lean.Meta.Hint.0.Lean.Meta.Hint.readableDiff.splitWordsAux : String → String.Pos.Raw → String.Pos.Raw → Array String → Array String → Array String × Array String
-- Lean.Elab.InfoTree.Types
Lean.Elab.PartialTermInfo.lctx : Lean.Elab.PartialTermInfo → Lean.LocalContext
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mdifferentiableOn_const : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {s : Set M} {c : M'},
  MDiff[s] fun x => c
-- Mathlib.RingTheory.MvPowerSeries.Equiv
MvPowerSeries.mk_truncTotal_toAdicCompletionInv : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : Finite σ] {n : ℕ}
  {f : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)},
  (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n • ⊤))
      ((MvPowerSeries.truncTotal n) (MvPowerSeries.toAdicCompletionInv σ R f)) =
    ↑f n
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.maxView.eq_2 : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β) (hl : l.Balanced) (size : ℕ)
  (k' : α) (v' : β k') (l' r' : Std.DTreeMap.Internal.Impl α β)
  (hr_2 : (Std.DTreeMap.Internal.Impl.inner size k' v' l' r').Balanced)
  (hlr_2 : Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size (Std.DTreeMap.Internal.Impl.inner size k' v' l' r').size),
  Std.DTreeMap.Internal.Impl.maxView k v l (Std.DTreeMap.Internal.Impl.inner size k' v' l' r') hl hr_2 hlr_2 =
    match Std.DTreeMap.Internal.Impl.maxView k' v' l' r' ⋯ ⋯ ⋯ with
    | { k := dk, v := dv, tree := { impl := dt, balanced_impl := hdt, size_impl := hdt' } } =>
      { k := dk, v := dv,
        tree :=
          { impl := Std.DTreeMap.Internal.Impl.balanceLErase k v l dt ⋯ ⋯ ⋯, balanced_impl := ⋯, size_impl := ⋯ } }
-- Mathlib.Logic.Relation
Relation.comp_eq : ∀ {α : Type u_1} {β : Type u_2} {r : α → β → Prop}, (Relation.Comp r fun x1 x2 => x1 = x2) = r
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.coe_center : ∀ (R : Type u) (A : Type v) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  ↑(Subalgebra.center R A) = (NonUnitalSubsemiring.center A).carrier
-- Mathlib.Data.Matrix.Mul
dotProduct_diagonal : ∀ {m : Type u_2} {α : Type v} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : NonUnitalNonAssocSemiring α]
  (v w : m → α) (i : m), v ⬝ᵥ Matrix.diagonal w i = v i * w i
-- Mathlib.GroupTheory.FreeGroup.GeneratorEquiv
/-- Isomorphic free abelian groups (as additive groups) have equivalent bases.  -/
Equiv.ofFreeAbelianGroupEquiv : {α : Type u_1} → {β : Type u_2} → FreeAbelianGroup α ≃+ FreeAbelianGroup β → α ≃ β
-- Mathlib.Topology.Algebra.Ring.Basic
/-- If a subsemiring of a topological semiring is commutative, then so is its
topological closure.

See note [reducible non-instances].  -/
Subsemiring.commSemiringTopologicalClosure : {R : Type u_1} →
  [inst : TopologicalSpace R] →
    [inst_1 : Semiring R] →
      [inst_2 : IsSemitopologicalSemiring R] →
        [T2Space R] → (s : Subsemiring R) → (∀ (x y : ↥s), x * y = y * x) → CommSemiring ↥s.topologicalClosure
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
IsLinearSet.isProperSemilinearSet : ∀ {M : Type u_1} [inst : AddCommMonoid M] {s : Set M} [IsCancelAdd M], IsLinearSet s → IsProperSemilinearSet s
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.instIsEquivalenceActionModuleCatRepToAction : ∀ (k : Type u) (G : Type v) [inst : Ring k] [inst_1 : Monoid G], (Rep.RepToAction k G).IsEquivalence
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
TendstoLocallyUniformlyOn.mul : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Type u_3} {X : Type u_4}
  [inst_3 : TopologicalSpace X] {F G : ι → X → α} {f g : X → α} {s : Set X} {l : Filter ι},
  TendstoLocallyUniformlyOn F f l s → TendstoLocallyUniformlyOn G g l s → TendstoLocallyUniformlyOn (F * G) (f * g) l s
-- Mathlib.Algebra.Order.Ring.Synonym
Lex.instNonUnitalCommRing : {R : Type u_1} → [NonUnitalCommRing R] → NonUnitalCommRing (Lex R)
-- Init.Data.Option.Lemmas
Option.right_le_of_merge_le : ∀ {α : Type u_1} [inst : LE α] {f : α → α → α},
  (∀ (a b c : α), f a b ≤ c → b ≤ c) → ∀ {o₁ o₂ o₃ : Option α}, Option.merge f o₁ o₂ ≤ o₃ → o₂ ≤ o₃
-- Mathlib.Data.Ineq
/-- `Ineq` is ordered `eq < le < lt`.  -/
Mathlib.Ineq.cmp : Mathlib.Ineq → Mathlib.Ineq → Ordering
-- Mathlib.MeasureTheory.Integral.CircleIntegral
circleIntegrable_id : ∀ (c : ℂ) (R : ℝ), CircleIntegrable (fun z => z) c R
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
WeierstrassCurve.Affine.nonsingular_zero : ∀ {R : Type r} [inst : CommRing R] {W : WeierstrassCurve.Affine R}, W.Nonsingular 0 0 ↔ W.a₆ = 0 ∧ (W.a₃ ≠ 0 ∨ W.a₄ ≠ 0)
-- Mathlib.Analysis.Convex.DoublyStochasticMatrix
/-- A matrix is `s` times a doubly stochastic matrix iff all entries are nonnegative, and all row and
column sums are equal to `s`.

This lemma is useful for the proof of Birkhoff's theorem - in particular because it allows scaling
by nonnegative factors rather than positive ones only.
 -/
exists_mem_doublyStochastic_eq_smul_iff : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semifield R]
  [inst_3 : LinearOrder R] [inst_4 : IsStrictOrderedRing R] {M : Matrix n n R} {s : R},
  0 ≤ s →
    ((∃ M' ∈ doublyStochastic R n, M = s • M') ↔
      (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j, M i j = s) ∧ ∀ (j : n), ∑ i, M i j = s)
-- Mathlib.Data.Setoid.Partition
Setoid.classes_ker_subset_fiber_set : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), (Setoid.ker f).classes ⊆ Set.range fun y => {x | f x = y}
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.single_le_sum : ∀ {ι : Type u_1} {N : Type u_5} [inst : AddCommMonoid N] [inst_1 : Preorder N] {f : ι → N} {s : Finset ι}
  [AddLeftMono N], (∀ i ∈ s, 0 ≤ f i) → ∀ {a : ι}, a ∈ s → f a ≤ ∑ x ∈ s, f x
-- Init.Data.String.Substring
Substring.Raw.prev_zero : ∀ (s : Substring.Raw), s.prev 0 = 0
-- Mathlib.AlgebraicGeometry.Cover.Over
AlgebraicGeometry.Scheme.instOverPullbackCoverOver' : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  (S : AlgebraicGeometry.Scheme) →
    [inst : P.IsStableUnderBaseChange] →
      [inst_1 : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] →
        {X W : AlgebraicGeometry.Scheme} →
          (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) →
            (f : W ⟶ X) →
              [inst_2 : W.Over S] →
                [inst_3 : X.Over S] →
                  [inst_4 : AlgebraicGeometry.Scheme.Cover.Over S 𝒰] →
                    [inst_5 : AlgebraicGeometry.Scheme.Hom.IsOver f S] →
                      AlgebraicGeometry.Scheme.Cover.Over S (AlgebraicGeometry.Scheme.Cover.pullbackCoverOver' S 𝒰 f)
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.of.inj : ∀ {carrier : Type u} {str : SeminormedAddCommGroup carrier} {carrier_1 : Type u}
  {str_1 : SeminormedAddCommGroup carrier_1},
  { carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 } → carrier = carrier_1 ∧ str ≍ str_1
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
/-- The pullback of sheaves of modules by the identity morphism identifies
to the identity functor.  -/
AlgebraicGeometry.Scheme.Modules.pullbackId : (X : AlgebraicGeometry.Scheme) →
  AlgebraicGeometry.Scheme.Modules.pullback (CategoryTheory.CategoryStruct.id X) ≅ CategoryTheory.Functor.id X.Modules
-- Init.Data.Nat.Power2.Lemmas
Nat.and_sub_one_eq_zero_iff_isPowerOfTwo : ∀ {n : ℕ}, n ≠ 0 → (n &&& n - 1 = 0 ↔ n.isPowerOfTwo)
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_σ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject.Augmented C}
  (self : X.ExtraDegeneracy) (n : ℕ) (i : Fin (n + 1)),
  CategoryTheory.CategoryStruct.comp (self.s n) (X.left.σ i.succ) =
    CategoryTheory.CategoryStruct.comp (X.left.σ i) (self.s (n + 1))
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PushoutObjObj.ofIsInitialLeft_inr : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₂ Y₂ : C₂} (f₂ : X₂ ⟶ Y₂)
  [inst_3 : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (F.flip.obj X₂)]
  [inst_4 : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (F.flip.obj Y₂)]
  (h : CategoryTheory.Limits.IsInitial X₁),
  (CategoryTheory.Functor.PushoutObjObj.ofIsInitialLeft F f₁ f₂ h).inr =
    (CategoryTheory.Limits.IsInitial.isInitialObj (F.flip.obj Y₂) X₁ h).to ((F.obj Y₁).obj X₂)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.neg_pi_div_two_lt_arcsin : ∀ {x : ℝ}, -(Real.pi / 2) < Real.arcsin x ↔ -1 < x
-- Mathlib.Topology.Category.Profinite.Product
/-- The limit cone on `indexFunctor`  -/
Profinite.indexCone : {ι : Type u} →
  {X : ι → Type} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      {C : Set ((i : ι) → X i)} →
        [inst_1 : ∀ (i : ι), T2Space (X i)] →
          [inst_2 : ∀ (i : ι), TotallyDisconnectedSpace (X i)] →
            (hC : IsCompact C) → CategoryTheory.Limits.Cone (Profinite.indexFunctor hC)
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
AlgebraicTopology.DoldKan.Γ₀.Obj.map_epi_on_summand_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : ChainComplex C ℕ) [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] {Δ Δ' : SimplexCategory} (e : Δ' ⟶ Δ)
  [inst_3 : CategoryTheory.Epi e],
  CategoryTheory.CategoryStruct.comp
      (((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan (Opposite.op Δ)).inj
        (CategoryTheory.SimplicialObject.Splitting.IndexSet.id (Opposite.op Δ)))
      ((AlgebraicTopology.DoldKan.Γ₀.obj K).map e.op) =
    ((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan (Opposite.op Δ')).inj
      (CategoryTheory.SimplicialObject.Splitting.IndexSet.mk e)
-- Init.Data.Array.Extract
Array.ne_empty_of_extract_ne_empty : ∀ {α : Type u_1} {as : Array α} {i j : ℕ}, as.extract i j ≠ #[] → as ≠ #[]
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.mem_keysArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.LawfulEqCmp cmp] [Std.TransCmp cmp]
  {k : α}, k ∈ t.keysArray ↔ k ∈ t
-- Mathlib.RingTheory.Localization.Defs
Localization.neg_mk : ∀ {R : Type u_1} [inst : CommRing R] {M : Submonoid R} (a : R) (b : ↥M), -Localization.mk a b = Localization.mk (-a) b
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.StdSimplex.weights_ne_zero : ∀ {R : Type u} [inst : PartialOrder R] [inst_1 : Semiring R] {M : Type u_9} [Nontrivial R]
  (w : Convexity.StdSimplex R M), w.weights ≠ 0
-- Mathlib.Data.Tree.Basic
/-- A node with `Unit` data  -/
BinaryTree.«term_△_» : Lean.TrailingParserDescr
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.AbsolutelyContinuous.neg_right : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  {N : Type u_6} [inst_2 : AddCommGroup N] [inst_3 : TopologicalSpace N] [inst_4 : IsTopologicalAddGroup N]
  {v : MeasureTheory.VectorMeasure α M} {w : MeasureTheory.VectorMeasure α N},
  v.AbsolutelyContinuous w → v.AbsolutelyContinuous (-w)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get?_insertIfNew : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF →
    ∀ {k a : α} {v : β k},
      (m.insertIfNew k v).get? a = if h : (k == a) = true ∧ k ∉ m then some (cast ⋯ v) else m.get? a
-- Mathlib.RingTheory.DedekindDomain.Factorization
/-- `val_v(v^n) = n` for every `n ∈ ℤ`.  -/
FractionalIdeal.count_zpow_self : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (n : ℤ),
  FractionalIdeal.count K v (↑v.asIdeal ^ n) = n
-- Mathlib.Order.RelIso.Basic
/-- `Sum.inl` as a relation embedding into `Sum.LiftRel r s`.  -/
RelEmbedding.sumLiftRelInl : {α : Type u_1} → {β : Type u_2} → (r : α → α → Prop) → (s : β → β → Prop) → r ↪r Sum.LiftRel r s
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
IsLocalFrameOn.linearIndependent : ∀ {𝕜 : 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 : FiberBundle F V] {ι : Type u_7} {n : WithTop ℕ∞}
  {s : ι → (x : M) → V x} {u : Set M},
  IsLocalFrameOn I F n s u → ∀ {x : M}, x ∈ u → LinearIndependent 𝕜 fun x_1 => s x_1 x
-- Mathlib.SetTheory.ZFC.PSet
PSet.Equiv.comm : ∀ {x : PSet.{u_1}} {y : PSet.{u_2}}, x.Equiv y ↔ y.Equiv x
-- Init.Data.UInt.Lemmas
UInt8.ofFin_lt_iff_lt : ∀ {a b : Fin UInt8.size}, UInt8.ofFin a < UInt8.ofFin b ↔ a < b
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval₂_ofNat : ∀ {R : Type u} [inst : Semiring R] {S : Type u_1} [inst_1 : Semiring S] (n : ℕ) [inst_2 : n.AtLeastTwo] (f : R →+* S)
  (a : S), Polynomial.eval₂ f a (OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.Algebra.Lie.UniversalEnveloping
_private.Mathlib.Algebra.Lie.UniversalEnveloping.0.UniversalEnvelopingAlgebra.ringCon.eq_1 : ∀ (R : Type u₁) (L : Type u₂) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  UniversalEnvelopingAlgebra.ringCon R L = ringConGen (UniversalEnvelopingAlgebra.Rel R L)
-- Lean.Compiler.InlineAttrs
Lean.Compiler.setInlineAttribute : Lean.Environment → Lean.Name → Lean.Compiler.InlineAttributeKind → Except String Lean.Environment
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
neg_lt_iff_pos_add : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddRightStrictMono α] {a b : α}, -a < b ↔ 0 < b + a
-- Mathlib.Algebra.Module.Submodule.LinearMap
/-- The action by a submodule is the action by the underlying module.  -/
Submodule.instAddActionSubtypeMem : {R : Type u} →
  {M : Type v} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        {module_M : Module R M} → (p : Submodule R M) → {α : Type u_1} → [AddAction M α] → AddAction (↥p) α
-- Mathlib.Algebra.GradedMonoid
GradedMonoid.GCommMonoid.mk : {ι : Type u_1} →
  {A : ι → Type u_2} →
    [inst : AddCommMonoid ι] →
      [toGMonoid : GradedMonoid.GMonoid A] → (∀ (a b : GradedMonoid A), a * b = b * a) → GradedMonoid.GCommMonoid A
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isEmpty_iff_forall_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → (t.isEmpty = true ↔ ∀ (a : α), t.contains a = false)
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Set.instNoZeroDivisors : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : Mul α] [NoZeroDivisors α], NoZeroDivisors (Set α)
-- Init.Data.String.Search
String.Internal.frontImpl : String → Char
-- Mathlib.Algebra.Ring.PUnit
PUnit.commRing : CommRing PUnit.{u_1 + 1}
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxc.Iterator.instIteratorLoop.loop.wf.eq_1 : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LE α] [inst_2 : DecidableLE α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLE α] {n : Type u → Type w}
  [inst_5 : Monad n] (γ : Type u) (Pl : α → γ → ForInStep γ → Prop)
  (wf : Std.IteratorLoop.WellFounded (Std.Rxc.Iterator α) Id Pl) (LargeEnough : α → Prop)
  (hl : ∀ (a b : α), a ≤ b → LargeEnough a → LargeEnough b) (upperBound : α) (acc : γ) (next : α) (h : LargeEnough next)
  (f : (out : α) → LargeEnough out → out ≤ upperBound → (c : γ) → n { s // Pl out c s }),
  Std.Rxc.Iterator.instIteratorLoop.loop.wf✝ γ Pl wf LargeEnough hl upperBound acc next h f =
    if hu : next ≤ upperBound then do
      let __do_lift ← f next h hu acc
      match __do_lift with
        | ⟨ForInStep.yield acc', property⟩ =>
          match hs : Std.PRange.succ? next with
          | some next' => Std.Rxc.Iterator.instIteratorLoop.loop.wf✝ γ Pl wf LargeEnough hl upperBound acc' next' ⋯ f
          | none => pure acc'
        | ⟨ForInStep.done acc', property⟩ => pure acc'
    else pure acc
-- Mathlib.Order.Category.Semilat
SemilatInfCat.dual_obj_isSemilatticeSup : ∀ (X : SemilatInfCat), (SemilatInfCat.dual.obj X).isSemilatticeSup = OrderDual.instSemilatticeSup X.X
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
/-- The inclusion functor forgetting the common section  -/
CategoryTheory.Limits.WalkingParallelPair.inclusionWalkingReflexivePair : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.WalkingReflexivePair
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
/-- The equivalence to matrices, bundled as a linear equivalence.  -/
CStarMatrix.ofMatrixₗ : {m : Type u_1} →
  {n : Type u_2} →
    {R : Type u_3} →
      {A : Type u_5} →
        [inst : AddCommMonoid A] → [inst_1 : Semiring R] → [inst_2 : Module R A] → Matrix m n A ≃ₗ[R] CStarMatrix m n A
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toList_rco_eq_none_iff : ∀ {m n i : ℕ}, (m...n).toList[i]? = none ↔ n ≤ i + m
-- Mathlib.Data.Nat.Factorization.Divisors
Nat.Iio_factorization_prod_pow_injective : ∀ (n : ℕ), Function.Injective fun x => (↑x).prod fun x1 x2 => x1 ^ x2
-- Init.Data.List.Nat.InsertIdx
List.insertIdx_of_length_lt : ∀ {α : Type u} {l : List α} {x : α} {i : ℕ}, l.length < i → l.insertIdx i x = l
-- Mathlib.Algebra.Group.Subgroup.Ker
Subgroup.map_eq_range_iff : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {f : G →* N} {H : Subgroup G},
  Subgroup.map f H = f.range ↔ Codisjoint H f.ker
-- Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing
/-- The modular discriminant equals `(E₄³ - E₆²) / 1728` in the graded ring
`⨁ k, ModularForm 𝒮ℒ k`.  -/
ModularForm.discriminant_eq_E₄_cube_sub_E₆_sq_graded : (DirectSum.of (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range) 12)
    (ModularFormClass.modularForm CuspForm.discriminant) =
  (1 / 1728) •
    ((DirectSum.of (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range) 4) ModularForm.E₄ ^ 3 -
      (DirectSum.of (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range) 6) ModularForm.E₆ ^ 2)
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.ObjectProperty.isGroupoid_of_isCodetecting_bot : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C], ⊥.IsCodetecting → CategoryTheory.IsGroupoid C
-- Lean.Meta.Sym.DSimp.DSimpM
Lean.Meta.Sym.DSimp.Result.step.injEq : ∀ (e' : Lean.Expr) (done : Bool) (e'_1 : Lean.Expr) (done_1 : Bool),
  (Lean.Meta.Sym.DSimp.Result.step e' done = Lean.Meta.Sym.DSimp.Result.step e'_1 done_1) = (e' = e'_1 ∧ done = done_1)
-- Mathlib.Computability.ContextFreeGrammar
/-- Context-free grammar that generates words over the alphabet `T` (a type of terminals).  -/
ContextFreeGrammar : Type u_1 → Type (max 1 u_1)
-- Mathlib.Algebra.Star.Conjneg
conjneg_neg : ∀ {G : Type u_2} {R : Type u_3} [inst : AddGroup G] [inst_1 : CommRing R] [inst_2 : StarRing R] (f : G → R),
  conjneg (-f) = -conjneg f
-- Lean.Data.Lsp.Utf16
_private.Lean.Data.Lsp.Utf16.0.Lean.String.codepointPosToUtf16PosFromAux : String → ℕ → String.Pos.Raw → ℕ → ℕ