mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iUnion₂_add : ∀ {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [inst : Add α] (s : (i : ι) → κ i → Set α) (t : Set α),
  (⋃ i, ⋃ j, s i j) + t = ⋃ i, ⋃ j, s i j + t
-- Mathlib.CategoryTheory.IsConnected
/-- `J` is connected if: given any function `F : J → α` which is constant for any
`j₁, j₂` for which there is a morphism `j₁ ⟶ j₂`, then `F` is constant.
This can be thought of as a local-to-global property.

The converse of `constant_of_preserves_morphisms`.
 -/
CategoryTheory.IsPreconnected.of_constant_of_preserves_morphisms : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J],
  (∀ {α : Type u₁} (F : J → α), (∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂) → ∀ (j j' : J), F j = F j') →
    CategoryTheory.IsPreconnected J
-- Mathlib.Tactic.Translate.Core
/-- Translate the declaration `src` and recursively all declarations `rootSrc._proof_i`
occurring in `src` using the `translations` dictionary.

- `rootSrc` is the declaration that got the translation attribute and `rootTgt` is its target.
- `src` is assumed to have a value available in the environment.
- `reorder` and `rename` are only used for the translation of `src`.
 -/
Mathlib.Tactic.Translate.transformDeclRec : Mathlib.Tactic.Translate.TranslateData →
  Mathlib.Tactic.Translate.Config →
    Lean.Name →
      Lean.Name →
        Lean.Name →
          optParam Mathlib.Tactic.Translate.ArgReorder { } → optParam (Lean.NameMap Lean.Name) ∅ → Lean.CoreM Unit
-- Mathlib.Algebra.Category.FGModuleCat.EssentiallySmall
FGModuleRepr.instSmallCategory : (R : Type u) → [inst : Ring R] → CategoryTheory.SmallCategory (FGModuleRepr R)
-- Mathlib.Topology.Separation.Basic
continuousOn_update_iff : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [T1Space X] [inst_2 : DecidableEq X]
  [inst_3 : TopologicalSpace Y] {f : X → Y} {s : Set X} {x : X} {y : Y},
  ContinuousOn (Function.update f x y) s ↔
    ContinuousOn f (s \ {x}) ∧ (x ∈ s → Filter.Tendsto f (nhdsWithin x (s \ {x})) (nhds y))
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.mem_insertMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : BEq α] [Std.LawfulBEqCmp cmp] {l : List (α × β)} {k : α},
  k ∈ Std.DTreeMap.Const.insertMany t l ↔ k ∈ t ∨ (List.map Prod.fst l).contains k = true
-- Init.Data.Order.Factories
/-- If an `LT α` instance is asymmetric and its negation is transitive, then `LE.ofLT α` represents a
linear preorder.
 -/
Std.IsLinearPreorder.of_lt : ∀ {α : Type u} [inst : LT α],
  autoParam (Std.Asymm fun x1 x2 => x1 < x2) Std.IsLinearPreorder.of_lt._auto_1 →
    ∀
      (not_lt_trans :
        autoParam (Trans (fun x1 x2 => ¬x1 < x2) (fun x1 x2 => ¬x1 < x2) fun x1 x2 => ¬x1 < x2)
          Std.IsLinearPreorder.of_lt._auto_3),
      Std.IsLinearPreorder α
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.instIsRegularPairingOfIsRegular : ∀ {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) [h.IsRegular], h.pairing.IsRegular
-- Mathlib.Topology.Order.NhdsSet
hasBasis_nhdsSet_Iic_Iic : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α] (a : α)
  [(nhdsWithin a (Set.Ioi a)).NeBot], (nhdsSet (Set.Iic a)).HasBasis (fun x => a < x) Set.Iic
-- Mathlib.Algebra.Module.PUnit
PUnit.smul : {R : Type u_1} → SMul R PUnit.{u_3 + 1}
-- Mathlib.RepresentationTheory.Coinvariants
Rep.coinvariantsAdjunction_unit_app : ∀ (k : Type u) (G : Type v) [inst : CommRing k] [inst_1 : Monoid G] (X : Rep.{w, u, v} k G),
  (Rep.coinvariantsAdjunction k G).unit.app X =
    Rep.ofHom { toLinearMap := ModuleCat.Hom.hom ((Rep.coinvariantsMk k G).app X), isIntertwining' := ⋯ }
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Λ'.Supports.eq_4 : ∀ (S : Finset Turing.PartrecToTM2.Λ') (p : Turing.PartrecToTM2.Γ' → Bool) (k : Turing.PartrecToTM2.K')
  (q : Turing.PartrecToTM2.Λ'),
  Turing.PartrecToTM2.Λ'.Supports S (Turing.PartrecToTM2.Λ'.clear p k q) = Turing.PartrecToTM2.Λ'.Supports S q
-- Std.Data.Internal.List.Associative
Std.Internal.List.length_insertList : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert →
      (∀ (a : α), Std.Internal.List.containsKey a l = true → (List.map Sigma.fst toInsert).contains a = false) →
        (Std.Internal.List.insertList l toInsert).length = l.length + toInsert.length
-- Lean.Elab.AssertExists
/-- The fully qualified name of a declaration that is expected to exist.  -/
Lean.Elab.Command.AssertExists.givenName : Lean.Elab.Command.AssertExists → Lean.Name
-- Init.Data.ByteArray.Bootstrap
ByteArray.ext : ∀ {x y : ByteArray}, x.data = y.data → x = y
-- Lean.Meta.Tactic.Grind.Theorems
Lean.Meta.Grind.instInhabitedTheorems : {a : Type} → Inhabited (Lean.Meta.Grind.Theorems a)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mul_lt_of_le_of_lt_one : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulLeftStrictMono α] {a b c : α},
  b ≤ c → a < 1 → b * a < c
-- Plausible.Testable
Plausible.instInhabitedConfiguration.default : Plausible.Configuration
-- Mathlib.Order.SetNotation
/-- Notation for `Set.sUnion`. Union of a set of sets.  -/
Set.«term⋃₀_» : Lean.ParserDescr
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
/-- Lifts `x : m α` into `HetT m α` with the trivial postcondition.

Caution: This is not a lawful monad lifting function
 -/
Std.Iterators.HetT.lift : {α : Type w} → {m : Type w → Type w'} → [Monad m] → m α → Std.Iterators.HetT m α
-- Mathlib.LinearAlgebra.AffineSpace.Independent
AffineIndependent.eq_zero_of_sum_eq_zero_subtype : ∀ {k : Type u_1} {V : Type u_2} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] {s : Finset V},
  AffineIndependent k Subtype.val → ∀ {w : V → k}, ∑ x ∈ s, w x = 0 → ∑ x ∈ s, w x • x = 0 → ∀ x ∈ s, w x = 0
-- Mathlib.CategoryTheory.ObjectProperty.ContainsZero
CategoryTheory.ObjectProperty.instContainsZeroMinOfIsClosedUnderIsomorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P Q : CategoryTheory.ObjectProperty C) [P.ContainsZero]
  [P.IsClosedUnderIsomorphisms] [Q.ContainsZero], (P ⊓ Q).ContainsZero
-- Mathlib.Algebra.CharP.Defs
ringExpChar.expChar : ∀ (R : Type u_1) [inst : Ring R] [IsDomain R], ExpChar R (ringExpChar R)
-- Mathlib.Combinatorics.Colex
/-- If `s ⊆ t`, then `s ≤ t` in the colex order. Note the converse does not hold, as inclusion does
not form a linear order.  -/
Finset.Colex.toColex_mono : ∀ {α : Type u_1} [inst : PartialOrder α], Monotone ⇑toColex
-- Batteries.Tactic.PrintDependents
Batteries.Tactic.CollectDependents.State.mk.sizeOf_spec : ∀ (otherAxiom : Bool) (result : Lean.NameMap Bool),
  sizeOf { otherAxiom := otherAxiom, result := result } = 1 + sizeOf otherAxiom + sizeOf result
-- Std.Time.Format.Modifier
Std.Time.Modifier.Q.injEq : ∀ (presentation presentation_1 : Std.Time.Number ⊕ Std.Time.Text),
  (Std.Time.Modifier.Q presentation = Std.Time.Modifier.Q presentation_1) = (presentation = presentation_1)
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.TaggedPrepartition.unionComplToSubordinate.congr_simp : ∀ {ι : Type u_1} [inst : Fintype ι] {I : BoxIntegral.Box ι} (π₁ π₁_1 : BoxIntegral.TaggedPrepartition I)
  (e_π₁ : π₁ = π₁_1) (π₂ π₂_1 : BoxIntegral.Prepartition I) (e_π₂ : π₂ = π₂_1) (hU : π₂.iUnion = ↑I \ π₁.iUnion)
  (r r_1 : (ι → ℝ) → ↑(Set.Ioi 0)),
  r = r_1 → π₁.unionComplToSubordinate π₂ hU r = π₁_1.unionComplToSubordinate π₂_1 ⋯ r_1
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int8.toBitVec_minValueSealed_eq_intMinSealed : Int8.minValueSealed✝.toBitVec = BitVec.Signed.intMinSealed✝ 8
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.insert : {α : Type u_1} →
  {β : Type u_2} → {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashMap α β → α → β → Lean.PersistentHashMap α β
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
/-- Post-composition with the preimage of an inducing function whose range is closed preserves
upper hemicontinuity.  -/
UpperHemicontinuousOn.isInducing_comp : ∀ {α : Type u_3} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {s : Set α}
  {γ : Type u_5} [inst_2 : TopologicalSpace γ] {i : γ → β},
  UpperHemicontinuousOn f s →
    Topology.IsInducing i → IsClosed (Set.range i) → UpperHemicontinuousOn (fun x => i ⁻¹' f x) s
-- Init.Data.ByteArray.Lemmas
ByteArray.append_right_inj : ∀ {ys₁ ys₂ : ByteArray} (xs : ByteArray), xs ++ ys₁ = xs ++ ys₂ ↔ ys₁ = ys₂
-- Mathlib.Algebra.Order.Field.Basic
le_mul_of_forall_lt₀ : ∀ {α : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a b c : α},
  (∀ a' > a, ∀ b' > b, c ≤ a' * b') → c ≤ a * b
-- Batteries.Data.List.Lemmas
_private.Batteries.Data.List.Lemmas.0.List.isPrefixOf.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (x : List α) (h_1 : (x : List α) → motive [] x)
  (h_2 : (x : List α) → motive x [])
  (h_3 : (a : α) → (as : List α) → (b : α) → (bs : List α) → motive (a :: as) (b :: bs)),
  (match [], x with
    | [], x => h_1 x
    | x, [] => h_2 x
    | a :: as, b :: bs => h_3 a as b bs) =
    h_1 x
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.DSimpArgs : Type
-- Mathlib.GroupTheory.CosetCover
AddSubgroup.exists_leftTransversal_of_FiniteIndex : ∀ {G : Type u_1} [inst : AddGroup G] {D H : AddSubgroup G} [D.FiniteIndex],
  D ≤ H → ∃ t, AddSubgroup.IsComplement ↑t ↑(D.addSubgroupOf H) ∧ ⋃ g ∈ t, ↑g +ᵥ ↑D = ↑H
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.comp_one : ∀ {α : Type u_2} {β : Type u_3} {M : Type u_7} [inst : One M] (f : M → β), f ∘ 1 = Function.const α (f 1)
-- Mathlib.RingTheory.RingHom.FiniteType
RingHom.finiteType_ofLocalizationSpanTarget : RingHom.OfLocalizationSpanTarget @RingHom.FiniteType
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.add_subset_add : ∀ {α : Type u_2} [inst : Add α] {s₁ s₂ t₁ t₂ : Set α}, s₁ ⊆ t₁ → s₂ ⊆ t₂ → s₁ + s₂ ⊆ t₁ + t₂
-- Std.Sync.Semaphore
_private.Std.Sync.Semaphore.0.Std.instNonemptySemaphoreState : Nonempty Std.SemaphoreState✝
-- Mathlib.Combinatorics.Enumerative.DoubleCounting
/-- Elements of `s` which are "below" `b` according to relation `r`.  -/
Finset.bipartiteBelow : {α : Type u_2} → {β : Type u_3} → (r : α → β → Prop) → Finset α → (b : β) → [(a : α) → Decidable (r a b)] → Finset α
-- Lean.Meta.Tactic.Grind.Arith.Simproc
Lean.Meta.Grind.Arith.normIntPowInst : Lean.Meta.Simp.DSimproc
-- Lean.Meta.Tactic.FVarSubst
Lean.Meta.FVarSubst.domain : Lean.Meta.FVarSubst → List Lean.FVarId
-- Lean.Attributes
Lean.instInhabitedAttributeExtensionState : Inhabited Lean.AttributeExtensionState
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile.0.Std.IterM.step_takeWhile.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : false = true → motive true) (h_2 : false = false → motive false),
  (match hP : false with
    | true => h_1 hP
    | false => h_2 hP) =
    h_2 ⋯
-- Mathlib.Algebra.Order.Group.Cone
AddGroupCone.mk.sizeOf_spec : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : SizeOf G] (toAddSubmonoid : AddSubmonoid G)
  (eq_zero_of_mem_of_neg_mem' : ∀ {a : G}, a ∈ toAddSubmonoid.carrier → -a ∈ toAddSubmonoid.carrier → a = 0),
  sizeOf { toAddSubmonoid := toAddSubmonoid, eq_zero_of_mem_of_neg_mem' := eq_zero_of_mem_of_neg_mem' } =
    1 + sizeOf toAddSubmonoid
-- Mathlib.Tactic.Positivity.Basic
/-- The `positivity` extension which identifies expressions of the form `a * b`,
such that `positivity` successfully recognises both `a` and `b`.  -/
Mathlib.Meta.Positivity.evalMul : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.Integrable.integrableOn : ∀ {α : Type u_1} {ε : Type u_3} {mα : MeasurableSpace α} {f : α → ε} {s : Set α} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε],
  MeasureTheory.Integrable f μ → MeasureTheory.IntegrableOn f s μ
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.ofList_eq_insertMany_empty : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List (α × β)}, Std.ExtHashMap.ofList l = ∅.insertMany l
-- Mathlib.Order.Partition.Basic
Partition.partscopyEquiv_symm_apply_coe : ∀ {α : Type u_1} {s t : α} [inst : CompleteLattice α] (P : Partition s) (hst : s = t)
  (b : { b // (fun x => x ∈ ↑P) b }), ↑((P.partscopyEquiv hst).symm b) = ↑b
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite
_private.Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite.0.CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.projectiveSeparator : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] → [CategoryTheory.IsGrothendieckAbelian.{v, v, u} C] → Cᵒᵖ
-- Mathlib.Combinatorics.Graph.Basic
Graph.Inc.isLoopAt_or_isNonloopAt : ∀ {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β}, G.Inc e x → G.IsLoopAt e x ∨ G.IsNonloopAt e x
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- **Alias** of `CategoryTheory.SubobjectRepresentableBy.isoΩ₀`.

---

`h.isoΩ₀` is the unique isomorphism from `h.Ω₀` to the canonical terminal object `⊤_ C`.  -/
CategoryTheory.Classifier.SubobjectRepresentableBy.isoΩ₀ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
      {Ω : C} →
        (h : CategoryTheory.SubobjectRepresentableBy Ω) →
          [inst_2 : CategoryTheory.Limits.HasTerminal C] → CategoryTheory.Subobject.underlying.obj h.Ω₀ ≅ ⊤_ C
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get?_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 : α},
  m.WF → (Std.DHashMap.Raw.filterMap f m).get? k = (m.get? k).bind (f k)
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.appIso_inv_naturality : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] {U V : X.Opens}
  (i : Opposite.op U ⟶ Opposite.op V),
  CategoryTheory.CategoryStruct.comp (X.presheaf.map i) (AlgebraicGeometry.Scheme.Hom.appIso f V).inv =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appIso f U).inv
      (Y.presheaf.map ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).op.map i))
-- Mathlib.Algebra.Group.Subgroup.Lattice
/-- The subgroup generated by a set includes the set.  -/
Subgroup.subset_closure : ∀ {G : Type u_1} [inst : Group G] {k : Set G}, k ⊆ ↑(Subgroup.closure k)
-- Mathlib.Algebra.Category.AlgCat.Limits
/-- The forgetful functor from R-algebras to R-modules preserves all limits.
 -/
AlgCat.forget₂Module_preservesLimitsOfSize : ∀ {R : Type u} [inst : CommRing R] [UnivLE.{v, w}],
  CategoryTheory.Limits.PreservesLimitsOfSize.{t, v, w, w, max u (w + 1), max u (w + 1)}
    (CategoryTheory.forget₂ (AlgCat R) (ModuleCat R))
-- Std.Http.Server.Handler
Std.Http.Server.Handler.mk : {σ : Type} →
  (ResponseBody : Type) →
    [responseBodyInstance : Std.Http.Body ResponseBody] →
      (σ → Std.Http.Request Std.Http.Body.Stream → Std.Async.ContextAsync (Std.Http.Response ResponseBody)) →
        (σ → IO.Error → Std.Async.Async Unit) →
          (σ → Std.Http.Request.Head → Std.Async.Async Bool) → Std.Http.Server.Handler σ
-- Mathlib.Data.Part
/-- The `some a` value in `Part` has a `True` domain and the
function returns `a`.  -/
Part.some : {α : Type u_1} → α → Part α
-- Mathlib.NumberTheory.ModularForms.Basic
ModularFormClass.toSlashInvariantFormClass : ∀ {F : Type u_2} {Γ : outParam (Subgroup (GL (Fin 2) ℝ))} {k : outParam ℤ} {inst : FunLike F UpperHalfPlane ℂ}
  [self : ModularFormClass F Γ k], SlashInvariantFormClass F Γ k
-- Init.Data.List.Basic
/-- Inserts an element into a list at the specified index. If the index is greater than the length of
the list, then the list is returned unmodified.

In other words, the new element is inserted into the list `l` after the first `i` elements of `l`.

Examples:
 * `["tues", "thur", "sat"].insertIdx 1 "wed" = ["tues", "wed", "thur", "sat"]`
 * `["tues", "thur", "sat"].insertIdx 2 "wed" = ["tues", "thur", "wed", "sat"]`
 * `["tues", "thur", "sat"].insertIdx 3 "wed" = ["tues", "thur", "sat", "wed"]`
 * `["tues", "thur", "sat"].insertIdx 4 "wed" = ["tues", "thur", "sat"]`
 -/
List.insertIdx : {α : Type u} → List α → ℕ → α → List α
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKeyD_erase_eq_of_not_compare_maxKeyD_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k fallback : α},
  (t.erase k).isEmpty = false →
    ¬cmp k (t.maxKeyD fallback) = Ordering.eq → (t.erase k).maxKeyD fallback = t.maxKeyD fallback
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.symm_apply_apply_mk : ∀ {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_3 : ∀ (x : B), Nonempty (E x)]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) {b : B}, b ∈ e.baseSet → ∀ (y : E b), e.symm b (↑e ⟨b, y⟩).2 = y
-- Mathlib.NumberTheory.ModularForms.LevelOne.Basic
ModularForm.levelOne_neg_weight_rank_zero : ∀ {k : ℤ}, k < 0 → Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) = 0
-- Init.Data.Option.Lemmas
Option.filter_eq_some_iff : ∀ {α : Type u_1} {a : α} {o : Option α} {p : α → Bool}, Option.filter p o = some a ↔ o = some a ∧ p a = true
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.DateBuilder.k : Std.Time.GenericFormat.DateBuilder✝ → Option (Std.Time.Internal.Bounded.LE 1 24)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
iteratedDerivWithin_cot_sub_inv_eq_add_mul_tsum : ∀ {z : ℂ} {k : ℕ},
  1 ≤ k →
    z ∈ UpperHalfPlane.upperHalfPlaneSet →
      iteratedDerivWithin k (fun x => ↑Real.pi * (↑Real.pi * x).cot - 1 / x) UpperHalfPlane.upperHalfPlaneSet z =
        -(-1) ^ k * ↑k.factorial * z ^ (-1 - ↑k) + (-1) ^ k * ↑k.factorial * ∑' (n : ℤ), (z + ↑n) ^ (-1 - ↑k)
-- Mathlib.Topology.Instances.Complex
/-- Let `K` a subfield of `ℂ` and let `ψ : K →+* ℂ` a ring homomorphism. Assume that `ψ` is uniform
continuous, then `ψ` is either the inclusion map or the composition of the inclusion map with the
complex conjugation.  -/
Complex.uniformContinuous_ringHom_eq_id_or_conj : ∀ (K : Subfield ℂ) {ψ : ↥K →+* ℂ},
  UniformContinuous ⇑ψ → (↑↑ψ).toFun = ⇑K.subtype ∨ (↑↑ψ).toFun = ⇑(starRingEnd ℂ) ∘ ⇑K.subtype
-- Lean.Widget.InteractiveDiagnostic
/-- Recursively moves child nodes after the first `blockSize` into a new "more" node.  -/
_private.Lean.Widget.InteractiveDiagnostic.0.Lean.Widget.msgToInteractiveAux.chopUpChildren : Lean.Name → ℕ → Subarray Lean.MessageData → Array Lean.MessageData
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.restrict.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Zero β] (f : MeasureTheory.SimpleFunc α β)
  (s : Set α), f.restrict s = if hs : MeasurableSet s then MeasureTheory.SimpleFunc.piecewise s hs f 0 else 0
-- Lean.Elab.InfoTree.Types
Lean.Elab.InfoTree.node.inj : ∀ {i : Lean.Elab.Info} {children : Lean.PersistentArray Lean.Elab.InfoTree} {i_1 : Lean.Elab.Info}
  {children_1 : Lean.PersistentArray Lean.Elab.InfoTree},
  Lean.Elab.InfoTree.node i children = Lean.Elab.InfoTree.node i_1 children_1 → i = i_1 ∧ children = children_1
-- Mathlib.LinearAlgebra.Dimension.RankNullity
/-- Given a nonzero vector in a space of dimension `> 1`, one may find another vector linearly
independent of the first one.  -/
exists_linearIndependent_pair_of_one_lt_rank : ∀ {R : Type u_1} {M : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [HasRankNullity.{u, u_1} R] [IsDomain R] [StrongRankCondition R] [Module.IsTorsionFree R M],
  1 < Module.rank R M → ∀ {x : M}, x ≠ 0 → ∃ y, LinearIndependent R ![x, y]
-- Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
Equiv.Perm.alternatingGroup_le_of_isPreprimitive : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α],
  4 < Nat.card α →
    ∀ (G : Subgroup (Equiv.Perm α)) [hG' : MulAction.IsPreprimitive (↥G) α] {s : Set α},
      MulAction.stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G → alternatingGroup α ≤ G
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.FiniteResidueField.ofArchimedean.congr_simp : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] {R : Type u_2}
  [inst_3 : LinearOrder R] [inst_4 : CommRing R] [inst_5 : IsStrictOrderedRing R] [inst_6 : Archimedean R]
  (f f_1 : R →+*o K),
  f = f_1 → ArchimedeanClass.FiniteResidueField.ofArchimedean f = ArchimedeanClass.FiniteResidueField.ofArchimedean f_1
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Internal.Small : Type v → Prop
-- Mathlib.Topology.MetricSpace.Similarity
Similar.symm : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoEMetricSpace P₁]
  [inst_1 : PseudoEMetricSpace P₂], Similar v₁ v₂ → Similar v₂ v₁
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
HasLineDerivAt.smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {f : E → F} {x v : E}
  {f' : F}, HasLineDerivAt 𝕜 f f' x v → ∀ (c : 𝕜), HasLineDerivAt 𝕜 f (c • f') x (c • v)
-- Lean.Environment
Lean.Kernel.Exception.letTypeMismatch.sizeOf_spec : ∀ (env : Lean.Kernel.Environment) (lctx : Lean.LocalContext) (name : Lean.Name) (givenType expectedType : Lean.Expr),
  sizeOf (Lean.Kernel.Exception.letTypeMismatch env lctx name givenType expectedType) =
    1 + sizeOf env + sizeOf lctx + sizeOf name + sizeOf givenType + sizeOf expectedType
-- Mathlib.Algebra.Group.Torsion
Subsingleton.to_isMulTorsionFree : ∀ {M : Type u_1} [inst : Monoid M] [Subsingleton M], IsMulTorsionFree M
-- Mathlib.Topology.Constructions.SumProd
Homeomorph.sumAssoc_toEquiv : ∀ (X : Type u) (Y : Type v) (Z : Type u_2) [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z], (Homeomorph.sumAssoc X Y Z).toEquiv = Equiv.sumAssoc X Y Z
-- Mathlib.Data.Matrix.Basic
AlgEquiv.mopMatrix_symm_apply : ∀ {m : Type u_2} {R : Type u_7} {α : Type u_11} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : CommSemiring R]
  [inst_3 : Semiring α] [inst_4 : Algebra R α] (M : (Matrix m m α)ᵐᵒᵖ),
  AlgEquiv.mopMatrix.symm M = (MulOpposite.unop M).transpose.map MulOpposite.op
-- Init.Data.Iterators.Lemmas.Consumers.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Loop.0.List.forIn'_eq_foldlM.match_1.splitter : {β : Type u_1} →
  (motive : ForInStep β → Sort u_2) →
    (b : ForInStep β) → ((b : β) → motive (ForInStep.yield b)) → ((b : β) → motive (ForInStep.done b)) → motive b
-- Mathlib.RepresentationTheory.Intertwining
/-- The `Equiv` between representations induced from `TensorProduct.assoc`.  -/
Representation.TensorProduct.assoc : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        {U : Type u_5} →
          [inst : CommSemiring A] →
            [inst_1 : Monoid G] →
              [inst_2 : AddCommMonoid V] →
                [inst_3 : AddCommMonoid W] →
                  [inst_4 : AddCommMonoid U] →
                    [inst_5 : Module A V] →
                      [inst_6 : Module A W] →
                        [inst_7 : Module A U] →
                          (ρ : Representation A G V) →
                            (σ : Representation A G W) →
                              (τ : Representation A G U) → ((ρ.tprod σ).tprod τ).Equiv (ρ.tprod (σ.tprod τ))
-- Mathlib.Data.Finset.Sort
Fin.sort_univ : ∀ (n : ℕ), (Finset.univ.sort fun x y => x ≤ y) = List.finRange n
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.comp_continuous_iff' : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] {β : Type u_5} [inst_7 : TopologicalSpace β] (e : A ≃A[R] B) {g : B → β},
  Continuous (g ∘ ⇑e) ↔ Continuous g