mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.List.Destutter
/-- `List.destutter'` on a relation like `≠`, whose negation is an equivalence, gives the same
length if the first elements are not related.  -/
List.length_destutter'_congr : ∀ {α : Type u_1} (l : List α) {R : α → α → Prop} [inst : DecidableRel R] {a b : α} [IsEquiv α Rᶜ],
  ¬R a b → (List.destutter' R a l).length = (List.destutter' R b l).length
-- Mathlib.Algebra.Group.Units.Defs
Units.val_inv_copy : ∀ {α : Type u} [inst : Monoid α] (u : αˣ) (val : α) (hv : val = ↑u) (inv : α) (hi : inv = ↑u⁻¹),
  ↑(u.copy val hv inv hi)⁻¹ = inv
-- Mathlib.LinearAlgebra.InvariantBasisNumber
card_eq_of_linearEquiv : ∀ (R : Type u) [inst : Semiring R] [InvariantBasisNumber R] {α : Type u_1} {β : Type u_2} [inst_2 : Fintype α]
  [inst_3 : Fintype β] (f : (α → R) ≃ₗ[R] β → R), Fintype.card α = Fintype.card β
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.comp_continuousOn_iff : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) {α : Type u_14}
  [inst_9 : TopologicalSpace α] {f : α → P} {s : Set α}, ContinuousOn (⇑e ∘ f) s ↔ ContinuousOn f s
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
/-- `H.support` is the set of vertices that form edges in the subgraph `H`.  -/
SimpleGraph.Subgraph.support : {V : Type u} → {G : SimpleGraph V} → G.Subgraph → Set V
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint.match_1.congr_eq_2 : ∀ {n : ℕ}
  (motive : Std.Tactic.BVDecide.LRAT.Internal.ReduceResult (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → Sort u_1)
  (x : Std.Tactic.BVDecide.LRAT.Internal.ReduceResult (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))
  (h_1 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth)
  (h_2 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty)
  (h_3 :
    (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin n) →
      (b : Bool) → motive (Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit (l, b)))
  (h_4 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit),
  x = Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty →
    (match x with
      | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth => h_1 ()
      | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty => h_2 ()
      | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit (l, b) => h_3 l b
      | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit => h_4 ()) ≍
      h_2 ()
-- Lean.Data.JsonRpc
Lean.JsonRpc.Notification.method : {α : Type u} → Lean.JsonRpc.Notification α → String
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue_insertList_of_contains_eq_false_right : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l toInsert : List ((_ : α) × β)} {k : α},
  Std.Internal.List.containsKey k toInsert = false →
    ∀ {p1 : Std.Internal.List.containsKey k (Std.Internal.List.insertList l toInsert) = true}
      {p2 : Std.Internal.List.containsKey k l = true},
      Std.Internal.List.getValue k (Std.Internal.List.insertList l toInsert) p1 = Std.Internal.List.getValue k l p2
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.IsPartition.inf : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.Prepartition I},
  π₁.IsPartition → π₂.IsPartition → (π₁ ⊓ π₂).IsPartition
-- Init.Data.Iterators.Lemmas.Combinators.Take
_private.Init.Data.Iterators.Lemmas.Combinators.Take.0.Std.Iter.toArray_eq_match_step.match_1.eq_1 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2) (it' : Std.Iter β) (out : β)
  (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.yield it' out with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_1 it' out
-- Batteries.Recycling.RBTree.Depth
RBTree.RBNode.depth.eq_def : ∀ {α : Type u_1} (x : RBTree.RBNode α),
  x.depth =
    match x with
    | RBTree.RBNode.nil => 0
    | RBTree.RBNode.node c a v b => max a.depth b.depth + 1
-- Mathlib.Algebra.DirectSum.Module
DirectSum.IsInternal.ofBijective_coeLinearMap_of_mem : ∀ {R : Type u} [inst : Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] {A : ι → Submodule R M} (h : DirectSum.IsInternal A) {i : ι} {x : M} (hx : x ∈ A i),
  ((LinearEquiv.ofBijective (DirectSum.coeLinearMap A) h).symm x) i = ⟨x, hx⟩
-- Mathlib.Topology.DenseEmbedding
/-- If `i : α → β` is a dense inducing, then any function `f : α → γ` "extends" to a function `g =
IsDenseInducing.extend di f : β → γ`. If `γ` is Hausdorff and `f` has a continuous extension, then
`g` is the unique such extension. In general, `g` might not be continuous or even extend `f`.  -/
IsDenseInducing.extend : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      [inst : TopologicalSpace α] →
        [inst_1 : TopologicalSpace β] → {i : α → β} → [TopologicalSpace γ] → IsDenseInducing i → (α → γ) → β → γ
-- Mathlib.CategoryTheory.Sums.Basic
CategoryTheory.Functor.sum_obj_inr : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C D)
  (c : C), (F.sum G).obj (Sum.inr c) = Sum.inr (G.obj c)
-- Mathlib.MeasureTheory.Measure.Haar.Unique
MeasureTheory.Measure.addHaarScalarFactor_self : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] (μ : MeasureTheory.Measure G) [inst_5 : μ.IsAddHaarMeasure],
  μ.addHaarScalarFactor μ = 1
-- Mathlib.Order.InitialSeg
PrincipalSeg.exists_eq_iff_rel : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsTrans β s] (f : PrincipalSeg r s) {a : α}
  {b : β}, s b (f.toRelEmbedding a) ↔ ∃ a', f.toRelEmbedding a' = b ∧ r a' a
-- Mathlib.Combinatorics.Additive.FreimanHom
IsMulFreimanHom.mapsTo : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] {n : ℕ} {A : Set α} {B : Set β}
  {f : α → β}, IsMulFreimanHom n A B f → Set.MapsTo f A B
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
/-- The Law of Quadratic Reciprocity: if `p` and `q` are primes that are both congruent
to `3` mod `4`, then `(q / p) = -(p / q)`.  -/
legendreSym.quadratic_reciprocity_three_mod_four : ∀ {p q : ℕ} [inst : Fact (Nat.Prime p)] [inst_1 : Fact (Nat.Prime q)],
  p % 4 = 3 → q % 4 = 3 → legendreSym q ↑p = -legendreSym p ↑q
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- **Alias** of `Submodule.starProjection_apply_mem`. -/
Submodule.orthogonalProjectionFn_mem : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (U : Submodule 𝕜 E) [inst_3 : U.HasOrthogonalProjection] (x : E), U.starProjection x ∈ U
-- Mathlib.RepresentationTheory.Coinvariants
/-- The submodule of a representation generated by elements of the form `ρ g x - x`.  -/
Representation.Coinvariants.ker : {k : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : CommRing k] →
        [inst_1 : Monoid G] → [inst_2 : AddCommGroup V] → [inst_3 : Module k V] → Representation k G V → Submodule k V
-- Lean.Server.CodeActions.Basic
/-- This is the initial code action that is sent to the server, to implement  -/
Lean.Server.LazyCodeAction.eager : Lean.Server.LazyCodeAction → Lean.Lsp.CodeAction
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instAddGroup : {α : Type u_1} → {l : Filter α} → {G : Type u_6} → [AddGroup G] → AddGroup (l.Germ G)
-- Mathlib.Analysis.Convex.SimplicialComplex.Basic
Geometry.SimplicialComplex.mk.injEq : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] (toPreAbstractSimplicialComplex : PreAbstractSimplicialComplex E)
  (indep : ∀ {s : Finset E}, s ∈ toPreAbstractSimplicialComplex.faces → AffineIndependent 𝕜 Subtype.val)
  (inter_subset_convexHull :
    ∀ {s t : Finset E},
      s ∈ toPreAbstractSimplicialComplex.faces →
        t ∈ toPreAbstractSimplicialComplex.faces → (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t ⊆ (convexHull 𝕜) (↑s ∩ ↑t))
  (toPreAbstractSimplicialComplex_1 : PreAbstractSimplicialComplex E)
  (indep_1 : ∀ {s : Finset E}, s ∈ toPreAbstractSimplicialComplex_1.faces → AffineIndependent 𝕜 Subtype.val)
  (inter_subset_convexHull_1 :
    ∀ {s t : Finset E},
      s ∈ toPreAbstractSimplicialComplex_1.faces →
        t ∈ toPreAbstractSimplicialComplex_1.faces → (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t ⊆ (convexHull 𝕜) (↑s ∩ ↑t)),
  ({ toPreAbstractSimplicialComplex := toPreAbstractSimplicialComplex, indep := indep,
        inter_subset_convexHull := inter_subset_convexHull } =
      { toPreAbstractSimplicialComplex := toPreAbstractSimplicialComplex_1, indep := indep_1,
        inter_subset_convexHull := inter_subset_convexHull_1 }) =
    (toPreAbstractSimplicialComplex = toPreAbstractSimplicialComplex_1)
-- Mathlib.Topology.Compactness.Lindelof
isLindelof_iff_lindelofSpace : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsLindelof s ↔ LindelofSpace ↑s
-- Init.Data.Ord.Basic
Ordering.swap_lt : Ordering.lt.swap = Ordering.gt
-- Mathlib.Data.Num.Bitwise
/-- Bitwise `not` for `SNum`.  -/
SNum.not : SNum → SNum
-- Mathlib.Data.Num.ZNum
PosNum.sub'.eq_1 : ∀ (x : PosNum), x.sub' PosNum.one = x.pred'.toZNum
-- Lean.Compiler.NameMangling
_private.Lean.Compiler.NameMangling.0.Lean.Name.demangleAux.match_6.eq_2 : ∀ (s : String) (motive : Char → Option (s.Pos × ℕ) → Sort u_1) (x : Char) (x_1 : Option (s.Pos × ℕ))
  (h_1 : (q : s.Pos) → (v : ℕ) → x_1 = some (q, v) → motive 'x' (some (q, v)))
  (h_2 : (x : Char) → (x_2 : Option (s.Pos × ℕ)) → x_1 = x_2 → motive x x_2),
  (∀ (q : s.Pos) (v : ℕ), x = 'x' → x_1 = some (q, v) → False) →
    (match x, h₁ : x_1 with
      | 'x', some (q, v) => h_1 q v h₁
      | x, x_3 => h_2 x x_3 h₁) =
      h_2 x x_1 ⋯
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.toWord : {ι : Type u_1} →
  {G : ι → Type u_2} →
    {H : Type u_3} →
      [inst : (i : ι) → Group (G i)] →
        [inst_1 : Group H] →
          {φ : (i : ι) → H →* G i} →
            {d : Monoid.PushoutI.NormalWord.Transversal φ} → Monoid.PushoutI.NormalWord d → Monoid.CoprodI.Word G
-- Mathlib.Data.List.Basic
List.idxOf_eq_zero_iff_head_eq : ∀ {α : Type u} [inst : BEq α] [LawfulBEq α] {l : List α} (hl : l ≠ []) {a : α}, List.idxOf a l = 0 ↔ l.head hl = a
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
IsCyclotomicExtension.Rat.subgroupGalEquivSubgroupChar.eq_1 : ∀ (n : ℕ) [inst : NeZero n] (K : Type u_1) [inst_1 : Field K] [inst_2 : NumberField K]
  [hK : IsCyclotomicExtension {n} ℚ K] (R : Type u_2) [inst_3 : CommRing R]
  [inst_4 : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)],
  IsCyclotomicExtension.Rat.subgroupGalEquivSubgroupChar n K R =
    (IsCyclotomicExtension.Rat.galEquivZMod n K).mapSubgroup.trans (MulChar.subgroupOrderIsoSubgroupMulChar (ZMod n) R)
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Set.smul_univ₀' : ∀ {α : Type u_1} {β : Type u_2} [inst : GroupWithZero α] [inst_1 : MulAction α β] {s : Set α},
  s.Nontrivial → s • Set.univ = Set.univ
-- Mathlib.Algebra.CharP.Two
CharTwo.natCast_eq_ite : ∀ {R : Type u_1} [inst : AddMonoidWithOne R] [CharP R 2] (n : ℕ), ↑n = if Even n then 0 else 1
-- Init.Data.Fin.Lemmas
Fin.rev_le_rev : ∀ {n : ℕ} {i j : Fin n}, i.rev ≤ j.rev ↔ j ≤ i
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupSeminorm.instIsScalarTowerOfReal : ∀ {R : Type u_1} {R' : Type u_2} {E : Type u_3} [inst : AddGroup E] [inst_1 : SMul R ℝ] [inst_2 : SMul R NNReal]
  [inst_3 : IsScalarTower R NNReal ℝ] [inst_4 : SMul R' ℝ] [inst_5 : SMul R' NNReal]
  [inst_6 : IsScalarTower R' NNReal ℝ] [inst_7 : SMul R R'] [IsScalarTower R R' ℝ],
  IsScalarTower R R' (NonarchAddGroupSeminorm E)
-- Mathlib.RingTheory.Regular.RegularSequence
RingTheory.Sequence.isRegular_cons_iff' : ∀ {R : Type u_1} (M : Type u_3) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (r : R)
  (rs : List R),
  RingTheory.Sequence.IsRegular M (r :: rs) ↔
    IsSMulRegular M r ∧
      RingTheory.Sequence.IsRegular (QuotSMulTop r M) (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs)
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.UnfoldLift.monadLift_trans : ∀ {m : Type u → Type v} {n : Type u → Type u_1} {o : Type u → Type u_2} {α : Type u} [inst : MonadLift n o]
  [inst_1 : MonadLiftT m n] (x : m α), monadLift x = MonadLift.monadLift (monadLift x)
-- Std.Internal.UV.Loop
/-- Accumulate the amount of idle time the event loop spends in the event provider.
 -/
Std.Internal.UV.Loop.Options.accumulateIdleTime : Std.Internal.UV.Loop.Options → Bool
-- Mathlib.MeasureTheory.Group.Arithmetic
DiscreteMeasurableSpace.toMeasurableInv : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : Inv α] [DiscreteMeasurableSpace α], MeasurableInv α
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.mul_eq_right_iff_opow_omega0_dvd : ∀ {a b : Ordinal.{u_1}}, a * b = b ↔ a ^ Ordinal.omega0 ∣ b
-- Lean.Data.Json.Basic
Lean.JsonNumber.shiftl : Lean.JsonNumber → ℕ → Lean.JsonNumber
-- Mathlib.CategoryTheory.Filtered.Final
/-- In this situation, `F` is also final, see
`Functor.final_of_exists_of_isFiltered_of_fullyFaithful`.  -/
CategoryTheory.IsFiltered.of_exists_of_isFiltered_of_fullyFaithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.IsFiltered D] [F.Full] [F.Faithful],
  (∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)) → CategoryTheory.IsFiltered C
-- Mathlib.Algebra.Algebra.Spectrum.Basic
_private.Mathlib.Algebra.Algebra.Spectrum.Basic.0.AlgHom.«term↑ₐ» : Lean.ParserDescr
-- Mathlib.Logic.Basic
/-- Construct a function from a default value `H0`, and a function to use if there exists a value
satisfying the predicate.  -/
Classical.existsCases : {α : Sort u_2} → {C : Sort u_3} → {p : α → Prop} → C → ((a : α) → p a → C) → C
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRk_eq_zero_iff : ∀ {α : Type u_1} {M : Matroid α} {X : Set α},
  autoParam (X ⊆ M.E) Matroid.eRk_eq_zero_iff._auto_1 → (M.eRk X = 0 ↔ X ⊆ M.loops)
-- Mathlib.Algebra.Ring.Action.Group
/-- **Alias** of `MulSemiringAction.toRingEquiv_apply_apply`. -/
MulSemiringAction.toRingEquiv_apply : ∀ (G : Type u_1) [inst : Group G] (R : Type u_2) [inst_1 : Semiring R] [inst_2 : MulSemiringAction G R] (x : G) (a : R),
  ((MulSemiringAction.toRingEquiv G R) x) a = x • a
-- Mathlib.RingTheory.Extension.Cotangent.Basis
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.ker_presLeft_le : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type u_4}
  {P : Algebra.Generators R S ι} {σ : Type u_5} {b : Module.Basis σ S P.toExtension.Cotangent}
  (D : Algebra.Generators.PresentationOfFreeCotangent.Aux✝ P b),
  (Algebra.Generators.PresentationOfFreeCotangent.Aux.presLeft✝ D).ker ≤ P.ker
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getD_ofList_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp]
  {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β k} {fallback : β k'},
  List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l →
    ⟨k, v⟩ ∈ l → (Std.ExtDTreeMap.ofList l cmp).getD k' fallback = cast ⋯ v
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- `map f` and `comap f` form a `GaloisInsertion` when `f` is surjective.  -/
Submonoid.giMapComap : {M : Type u_1} →
  {N : Type u_2} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] →
        {F : Type u_4} →
          [inst_2 : FunLike F M N] →
            [mc : MonoidHomClass F M N] →
              {f : F} → Function.Surjective ⇑f → GaloisInsertion (Submonoid.map f) (Submonoid.comap f)
-- Mathlib.Probability.Kernel.Category.SFinKer
SFinKer.Hom.mk.injEq : ∀ {X Y : SFinKer} (hom : ProbabilityTheory.Kernel X.carrier Y.carrier)
  (property : ProbabilityTheory.IsSFiniteKernel hom) (hom_1 : ProbabilityTheory.Kernel X.carrier Y.carrier)
  (property_1 : ProbabilityTheory.IsSFiniteKernel hom_1),
  ({ hom := hom, property := property } = { hom := hom_1, property := property_1 }) = (hom = hom_1)
-- Lean.Parser.Do
/-- Internal syntax used in the `if` and `unless` elaborators. Behaves like `pure PUnit.unit` but
uses `()` if possible and gives better error messages.
 -/
Lean.Parser.Term.InternalSyntax.doSkip : Lean.ParserDescr
-- Mathlib.Geometry.Manifold.ChartedSpace
/-- If a topological space admits an atlas with locally compact charts, then the space itself
is locally compact.  -/
ChartedSpace.locallyCompactSpace : ∀ (H : Type u) (M : Type u_2) [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [ChartedSpace H M]
  [LocallyCompactSpace H], LocallyCompactSpace M
-- Mathlib.Analysis.Normed.Group.Basic
/-- **Alias** of the reverse direction of `indiscreteTopology_iff_forall_norm_eq_zero'`. -/
IndiscreteTopology.of_forall_norm_eq_zero' : ∀ {E : Type u_5} [inst : SeminormedGroup E], (∀ (x : E), ‖x‖ = 0) → IndiscreteTopology E
-- Std.Data.HashSet.Lemmas
Std.HashSet.insertMany_ind : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {ρ : Type v} [inst : ForIn Id ρ α] {motive : Std.HashSet α → Prop}
  (m : Std.HashSet α) {l : ρ},
  motive m → (∀ (m : Std.HashSet α) (a : α), motive m → motive (m.insert a)) → motive (m.insertMany l)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- The left inclusion into the disjoint union.  -/
CategoryTheory.PreZeroHypercover.sumInl : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} → (E : CategoryTheory.PreZeroHypercover S) → (F : CategoryTheory.PreZeroHypercover S) → E.Hom (E.sum F)
-- Mathlib.RingTheory.Extension.Presentation.Submersive
/-- The dimension of the composition of two finite submersive presentations is
the sum of the dimensions.  -/
Algebra.PreSubmersivePresentation.dimension_comp_eq_dimension_add_dimension : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_1} {σ' : Type u_2} {T : Type u_3} [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T] (Q : Algebra.PreSubmersivePresentation S T ι' σ')
  (P : Algebra.PreSubmersivePresentation R S ι σ) [Finite ι] [Finite ι'] [Finite σ] [Finite σ'],
  (Q.comp P).dimension = Q.dimension + P.dimension
-- Mathlib.CategoryTheory.Simple
/-- In an abelian category, an object satisfying the dual of the definition of a simple object is
simple.  -/
CategoryTheory.simple_of_cosimple : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] (X : C),
  (∀ {Z : C} (f : X ⟶ Z) [CategoryTheory.Epi f], CategoryTheory.IsIso f ↔ f ≠ 0) → CategoryTheory.Simple X
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Bicone.ι_of_isLimit : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {t : CategoryTheory.Limits.Bicone f}
  (ht : CategoryTheory.Limits.IsLimit t.toCone) (j : J),
  t.ι j = ht.lift (CategoryTheory.Limits.Fan.mk (f j) fun j' => if h : j = j' then CategoryTheory.eqToHom ⋯ else 0)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey!_alter_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  [inst_1 : Inhabited α] {k : α} {f : Option (β k) → Option (β k)},
  (m.alter k f).getKey! k = if (f (m.get? k)).isSome = true then k else default
-- Std.Http.Data.Body.Full
Std.Http.Body.instFull : Std.Http.Body Std.Http.Body.Full
-- Lean.Util.CollectLooseBVars
/-- Collects the loose bound variables in `e` with indices at least `offset`.
Returns a set of indices relative to `offset`.

Specification: `i ∈ e.collectLooseBVars offset ↔ e.hasLooseBVar (i + offset)`.
 -/
Lean.Expr.collectLooseBVars : Lean.Expr → optParam ℕ 0 → Std.HashSet ℕ
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.isoOfComponents_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : AlgebraicGeometry.PresheafedSpace C} (H : ↑X ≅ ↑Y)
  (α : (TopCat.Presheaf.pushforward C H.hom).obj X.presheaf ≅ Y.presheaf),
  (AlgebraicGeometry.PresheafedSpace.isoOfComponents H α).hom = { base := H.hom, c := α.inv }
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.isLongestMatchAt_cast_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s t : String.Slice} (hst : s.copy = t.copy)
  {startPos endPos : s.Pos},
  String.Slice.Pattern.Model.IsLongestMatchAt pat (startPos.cast hst) (endPos.cast hst) ↔
    String.Slice.Pattern.Model.IsLongestMatchAt pat startPos endPos
-- Lean.Server.Requests
Lean.Server.RequestContext.cancelTk : Lean.Server.RequestContext → Lean.Server.RequestCancellationToken
-- Mathlib.CategoryTheory.Action.Basic
/-- An `Action V G` represents a bundled action of
the monoid `G` on an object of some category `V`.

As an example, when `V = ModuleCat R`, this is an `R`-linear representation of `G`,
while when `V = Type` this is a `G`-action.
 -/
Action : (V : Type u_1) → [CategoryTheory.Category.{v_1, u_1} V] → (G : Type u_2) → [Monoid G] → Type (max (max u_1 u_2) v_1)
-- Mathlib.Analysis.InnerProductSpace.Spectrum
/-- The eigenspaces of a self-adjoint operator on a finite-dimensional inner product space `E` gives
an internal direct sum decomposition of `E`.

Note this takes `hT` as a `Fact` to allow it to be an instance.  -/
LinearMap.IsSymmetric.directSumDecomposition : {𝕜 : Type u_1} →
  [inst : RCLike 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : InnerProductSpace 𝕜 E] →
          {T : E →ₗ[𝕜] E} →
            [FiniteDimensional 𝕜 E] →
              [hT : Fact T.IsSymmetric] → DirectSum.Decomposition fun μ => Module.End.eigenspace T (↑T 1 μ)
-- Init.Data.BitVec.Lemmas
BitVec.replicate.eq_2 : ∀ {w : ℕ} (x : BitVec w) (n : ℕ), BitVec.replicate n.succ x = BitVec.cast ⋯ (x ++ BitVec.replicate n x)
-- Mathlib.LinearAlgebra.Matrix.ToLin
Algebra.leftMulMatrix_mulVec_repr : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {m : Type u_3}
  [inst_3 : Fintype m] [inst_4 : DecidableEq m] (b : Module.Basis m R S) (x y : S),
  ((Algebra.leftMulMatrix b) x).mulVec ⇑(b.repr y) = ⇑(b.repr (x * y))
-- Lean.Meta.Tactic.Cases
_private.Lean.Meta.Tactic.Cases.0.Lean.Meta.Cases.mkCasesContext? : Lean.FVarId → Lean.MetaM (Option Lean.Meta.Cases.Context)
-- Mathlib.CategoryTheory.Functor.Derived.RightDerived
/-- The natural transformation `RF ⟶ RF'` on right derived functors that is
induced by a natural transformation `F ⟶ F'`.  -/
CategoryTheory.Functor.rightDerivedNatTrans : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_5, u_3} H] →
            (RF RF' : CategoryTheory.Functor D H) →
              {F F' : CategoryTheory.Functor C H} →
                {L : CategoryTheory.Functor C D} →
                  (α : F ⟶ L.comp RF) →
                    (F' ⟶ L.comp RF') →
                      (W : CategoryTheory.MorphismProperty C) →
                        [inst_3 : L.IsLocalization W] → [RF.IsRightDerivedFunctor α W] → (F ⟶ F') → (RF ⟶ RF')
-- Mathlib.Topology.Baire.BaireMeasurable
/-- Any `BaireMeasurableSet` differs from some open set by a meager set.  -/
BaireMeasurableSet.residualEq_isOpen : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α}, BaireMeasurableSet s → ∃ u, IsOpen u ∧ s =ᶠ[residual α] u