mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_fiberwise' : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : DecidableEq κ] [inst_2 : Fintype κ]
  (s : Finset ι) (g : ι → κ) (f : κ → M), ∑ j, ∑ i ∈ s with g i = j, f j = ∑ i ∈ s, f (g i)
-- Mathlib.MeasureTheory.Measure.MutuallySingular
/-- Two measures `μ`, `ν` are said to be mutually singular if there exists a measurable set `s`
such that `μ s = 0` and `ν sᶜ = 0`.  -/
MeasureTheory.«term_⟂ₘ_» : Lean.TrailingParserDescr
-- Init.Data.Vector.Algebra
Vector.mul_comm : ∀ {α : Type u_1} {n : ℕ} [inst : Mul α], (∀ (x y : α), x * y = y * x) → ∀ (xs ys : Vector α n), xs * ys = ys * xs
-- Mathlib.Computability.TuringMachine.Tape
Turing.BlankRel.symm : ∀ {Γ : Type u_1} [inst : Inhabited Γ] {l₁ l₂ : List Γ}, Turing.BlankRel l₁ l₂ → Turing.BlankRel l₂ l₁
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.Stmt.goto.injEq : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (a a_1 : σ → Λ),
  (Turing.TM2.Stmt.goto a = Turing.TM2.Stmt.goto a_1) = (a = a_1)
-- Mathlib.CategoryTheory.LiftingProperties.Adjunction
/-- A (right) adjoint square has a lifting if and only if the original square has a lifting.  -/
CategoryTheory.CommSq.right_adjoint_hasLift_iff : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {G : CategoryTheory.Functor C D} {F : CategoryTheory.Functor D C}
  {A B : C} {X Y : D} {i : A ⟶ B} {p : X ⟶ Y} {u : G.obj A ⟶ X} {v : G.obj B ⟶ Y}
  (sq : CategoryTheory.CommSq u (G.map i) p v) (adj : G ⊣ F), ⋯.HasLift ↔ sq.HasLift
-- Batteries.Data.Char.Basic
Char.toNat_ofNatAux : ∀ {n : ℕ} (h : n.isValidChar), (Char.ofNatAux n h).toNat = n
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
/-- A continuous linear map satisfies `IsBoundedLinearMap`  -/
ContinuousLinearMap.isBoundedLinearMap : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (f : E →L[𝕜] F), IsBoundedLinearMap 𝕜 ⇑f
-- Std.Http.Protocol.H1.Reader
Std.Http.Protocol.H1.Reader.instInhabitedState.default : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Reader.State dir
-- Mathlib.LinearAlgebra.Dimension.Basic
Submodule.rank_mono : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s t : Submodule R M},
  s ≤ t → Module.rank R ↥s ≤ Module.rank R ↥t
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.ext_iff : ∀ {α : Type u_1} {m₁ m₂ : MeasurableSpace α}, m₁ = m₂ ↔ ∀ (s : Set α), MeasurableSet s ↔ MeasurableSet s
-- Init.Data.String.Substring
Substring.Raw.Internal.dropImpl : Substring.Raw → ℕ → Substring.Raw
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.get_eq_getElem : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] {a : α} {h : a ∈ m},
  m.get a h = m[a]
-- Mathlib.CategoryTheory.Category.Pairwise
_private.Mathlib.CategoryTheory.Category.Pairwise.0.CategoryTheory.Pairwise.diagramMap.match_1.eq_3 : ∀ {ι : Type u_1} (motive : (x x_1 : CategoryTheory.Pairwise ι) → (x ⟶ x_1) → Sort u_2) (i j : ι)
  (h_1 :
    (i : ι) →
      motive (CategoryTheory.Pairwise.single i) (CategoryTheory.Pairwise.single i)
        (CategoryTheory.Pairwise.Hom.id_single i))
  (h_2 :
    (i j : ι) →
      motive (CategoryTheory.Pairwise.pair i j) (CategoryTheory.Pairwise.pair i j)
        (CategoryTheory.Pairwise.Hom.id_pair i j))
  (h_3 :
    (i j : ι) →
      motive (CategoryTheory.Pairwise.pair i j) (CategoryTheory.Pairwise.single i)
        (CategoryTheory.Pairwise.Hom.left i j))
  (h_4 :
    (i j : ι) →
      motive (CategoryTheory.Pairwise.pair i j) (CategoryTheory.Pairwise.single j)
        (CategoryTheory.Pairwise.Hom.right i j)),
  (match CategoryTheory.Pairwise.pair i j, CategoryTheory.Pairwise.single i, CategoryTheory.Pairwise.Hom.left i j with
    | .(CategoryTheory.Pairwise.single i), .(CategoryTheory.Pairwise.single i),
      CategoryTheory.Pairwise.Hom.id_single i => h_1 i
    | .(CategoryTheory.Pairwise.pair i j), .(CategoryTheory.Pairwise.pair i j),
      CategoryTheory.Pairwise.Hom.id_pair i j => h_2 i j
    | .(CategoryTheory.Pairwise.pair i j), .(CategoryTheory.Pairwise.single i), CategoryTheory.Pairwise.Hom.left i j =>
      h_3 i j
    | .(CategoryTheory.Pairwise.pair i j), .(CategoryTheory.Pairwise.single j), CategoryTheory.Pairwise.Hom.right i j =>
      h_4 i j) =
    h_3 i j
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.map.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  [inst : MeasurableSpace γ] (κ : ProbabilityTheory.Kernel α β) (f : β → γ),
  κ.map f = if hf : Measurable f then κ.mapOfMeasurable f hf else 0
-- Mathlib.Topology.Compactness.Compact
compactSpace_generateFrom_of_compl_mem : ∀ {X : Type u} [T : TopologicalSpace X] (𝔅 : Set (Set X)),
  T = TopologicalSpace.generateFrom 𝔅 →
    (∀ s ∈ 𝔅, sᶜ ∈ 𝔅) → (∀ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) → (⋂₀ P).Nonempty) → CompactSpace X
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.smul_weierstrassMod : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A] (a : A) (f g : PowerSeries A)
  [inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A], a • f %ʷ g = a • (f %ʷ g)
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.instIsCentralScalar : ∀ {α : Type u_1} {R : Type u_6} [inst : SMul R ENNReal] [inst_1 : IsScalarTower R ENNReal ENNReal]
  [inst_2 : SMul Rᵐᵒᵖ ENNReal] [inst_3 : IsCentralScalar R ENNReal] {x : MeasurableSpace α},
  IsCentralScalar R (MeasureTheory.Measure α)
-- Mathlib.Order.InitialSeg
PrincipalSeg.mk.inj : ∀ {α : Type u_4} {β : Type u_5} {r : α → α → Prop} {s : β → β → Prop} {toRelEmbedding : r ↪r s} {top : β}
  {mem_range_iff_rel' : ∀ (b : β), b ∈ Set.range ⇑toRelEmbedding ↔ s b top} {toRelEmbedding_1 : r ↪r s} {top_1 : β}
  {mem_range_iff_rel'_1 : ∀ (b : β), b ∈ Set.range ⇑toRelEmbedding_1 ↔ s b top_1},
  { toRelEmbedding := toRelEmbedding, top := top, mem_range_iff_rel' := mem_range_iff_rel' } =
      { toRelEmbedding := toRelEmbedding_1, top := top_1, mem_range_iff_rel' := mem_range_iff_rel'_1 } →
    toRelEmbedding = toRelEmbedding_1 ∧ top = top_1
-- Mathlib.CategoryTheory.IsConnected
/-- A Zag in a discrete category entails an equality of its extremities  -/
CategoryTheory.eq_of_zag : ∀ (X : Type u_1) {a b : CategoryTheory.Discrete X}, CategoryTheory.Zag a b → a.as = b.as
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem?_map_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → γ} {k k' : α},
  m.getKey? k = some k' → (Std.HashMap.map f m)[k]? = Option.map (f k') m[k]?
-- Mathlib.MeasureTheory.Group.Measure
/-- If a left-invariant measure gives finite mass to a nonempty open set, then it gives finite mass
to any compact set.  -/
MeasureTheory.measure_lt_top_of_isCompact_of_isMulLeftInvariant : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G}
  [inst_3 : Group G] [IsTopologicalGroup G] [μ.IsMulLeftInvariant] (U : Set G),
  IsOpen U → U.Nonempty → μ U ≠ ⊤ → ∀ {K : Set G}, IsCompact K → μ K < ⊤
-- Mathlib.Analysis.Normed.Group.Constructions
norm_ofAdd : ∀ {E : Type u_2} [inst : Norm E] (x : E), ‖Multiplicative.ofAdd x‖ = ‖x‖
-- Init.Data.String.Substring
Substring.Raw.Internal.prevImpl : Substring.Raw → String.Pos.Raw → String.Pos.Raw
-- Lean.Meta.Basic
/-- If `s` is nonempty, then `withZetaDeltaSet s x` executes `x` with `zetaDeltaSet := s`.
The cache is temporarily reset while executing `x`.

If `s` is empty, then runs `x` without changing `zetaDeltaSet` or resetting the cache.

See also `withTrackingZetaDeltaSet` for tracking zeta-delta reductions.
 -/
Lean.Meta.withZetaDeltaSet : {n : Type → Type u_1} → [MonadControlT Lean.MetaM n] → [Monad n] → {α : Type} → Lean.FVarIdSet → n α → n α
-- Init.Data.Nat.Simproc
Nat.Simproc.add_le_gt : ∀ (a : ℕ) {b c : ℕ}, b > c → (a + b ≤ c) = False
-- Mathlib.CategoryTheory.Limits.MorphismProperty
CategoryTheory.CostructuredArrow.isClosedUnderColimitsOfShape : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {A : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A] {L : CategoryTheory.Functor A T} {J : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} J] {P : CategoryTheory.MorphismProperty T} [P.RespectsIso]
  [CategoryTheory.Limits.PreservesColimitsOfShape J L] [CategoryTheory.Limits.HasColimitsOfShape J A]
  (c : (D : CategoryTheory.Functor J T) → [CategoryTheory.Limits.HasColimit D] → CategoryTheory.Limits.Cocone D)
  (hc :
    (D : CategoryTheory.Functor J T) →
      [inst_6 : CategoryTheory.Limits.HasColimit D] → CategoryTheory.Limits.IsColimit (c D)),
  (∀ (D : CategoryTheory.Functor J T) [inst_6 : CategoryTheory.Limits.HasColimit D] {X : T}
      (s : D ⟶ (CategoryTheory.Functor.const J).obj X),
      (∀ (j : J), P (s.app j)) → P ((hc D).desc { pt := X, ι := s })) →
    ∀ (X : T), (CategoryTheory.MorphismProperty.costructuredArrowObj L P).IsClosedUnderColimitsOfShape J
-- Mathlib.LinearAlgebra.Matrix.Invertible
/-- A copy oy of `invOf_mul_eq_iff_eq_mul_left` for rectangular matrices.  -/
Matrix.invOf_mul_eq_iff_eq_mul_left : ∀ {m : Type u_1} {n : Type u_2} {α : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring α]
  {A B : Matrix n m α} {C : Matrix n n α} [inst_3 : Invertible C], ⅟C * A = B ↔ A = C * B
-- Mathlib.Data.DFinsupp.Notation
/-- Unexpander for the `fun₀ | i => x` notation.  -/
DFinsupp.updateUnexpander : Lean.PrettyPrinter.Unexpander
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.subsingleton_iff : ∀ {M : Type u_1} [inst : AddZeroClass M], Subsingleton (AddSubmonoid M) ↔ Subsingleton M
-- Mathlib.Data.Sigma.Order
/-- The lexicographical linear order on a sigma type.  -/
Sigma.Lex.linearOrder : {ι : Type u_1} → {α : ι → Type u_2} → [LinearOrder ι] → [(i : ι) → LinearOrder (α i)] → LinearOrder (Σₗ (i : ι), α i)
-- Mathlib.Topology.UniformSpace.CompactConvergence
/-- When `α` is compact, `f : X → C(α, β)` is continuous if any only if it is continuous when
reinterpreted as a map `f : X → α →ᵤ β`.  -/
ContinuousMap.continuous_iff_continuous_uniformFun : ∀ {α : Type u₁} {β : Type u₂} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] [CompactSpace α] {X : Type u_1}
  [inst_3 : TopologicalSpace X] (f : X → C(α, β)), Continuous f ↔ Continuous fun x => UniformFun.ofFun ⇑(f x)
-- Mathlib.Order.Category.Semilat
SemilatInfCat.instCoeSortType : CoeSort SemilatInfCat (Type u_1)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.asIsoHomologyι_inv_comp_homologyι_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) [inst_2 : S.HasHomology] {Z : C} (h : S.opcycles ⟶ Z),
  CategoryTheory.CategoryStruct.comp (S.asIsoHomologyι hg).inv (CategoryTheory.CategoryStruct.comp S.homologyι h) = h
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.T_eq_half_mul_C_comp_two_mul_X : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : Invertible 2] (n : ℤ),
  Polynomial.Chebyshev.T R n = Polynomial.C ⅟2 * (Polynomial.Chebyshev.C R n).comp (2 * Polynomial.X)
-- Mathlib.Data.Finsupp.NeLocus
Finsupp.mapRange_neLocus_eq : ∀ {α : Type u_1} {M : Type u_2} {N : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq N] [inst_2 : DecidableEq M]
  [inst_3 : Zero M] [inst_4 : Zero N] (f g : α →₀ N) {F : N → M} (F0 : F 0 = 0),
  Function.Injective F → (Finsupp.mapRange F F0 f).neLocus (Finsupp.mapRange F F0 g) = f.neLocus g
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.false_of_to_star' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C}
  (f : (CategoryTheory.WithInitial.of X).Hom CategoryTheory.WithInitial.star), False
-- Init.Data.String.Lemmas.IsEmpty
String.Slice.isEmpty_sliceFrom_eq_false_iff : ∀ {s : String.Slice} {p : s.Pos}, (s.sliceFrom p).isEmpty = false ↔ p ≠ s.endPos
-- Mathlib.Data.Int.Bitwise
Int.shiftRight_neg : ∀ (m n : ℤ), m >>> (-n) = m <<< n
-- Aesop.Stats.Basic
Aesop.RuleStatsTotals.mk.sizeOf_spec : ∀ (numSuccessful numFailed : ℕ) (elapsedSuccessful elapsedFailed : Aesop.Nanos),
  sizeOf
      { numSuccessful := numSuccessful, numFailed := numFailed, elapsedSuccessful := elapsedSuccessful,
        elapsedFailed := elapsedFailed } =
    1 + sizeOf numSuccessful + sizeOf numFailed + sizeOf elapsedSuccessful + sizeOf elapsedFailed
-- Mathlib.Analysis.Complex.Angle
Complex.angle_exp_exp : ∀ (x y : ℝ),
  InnerProductGeometry.angle (Complex.exp (↑x * Complex.I)) (Complex.exp (↑y * Complex.I)) =
    |toIocMod Real.two_pi_pos (-Real.pi) (x - y)|
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.getKey?_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] {k : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getKey? k = t₂.getKey? k
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instSub : {m : Type u_1} → {n : Type u_2} → {A : Type u_5} → [Sub A] → Sub (CStarMatrix m n A)
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
abs_abs_sub_abs_le : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddCommGroup α] [AddLeftMono α] (a b : α), ||a| - |b|| ≤ |a - b|
-- Mathlib.Algebra.Group.Nat.Hom
multiplesAddHom_apply : ∀ {M : Type u_1} [inst : AddCommMonoid M] (x : M) (n : ℕ), ((multiplesAddHom M) x) n = n • x
-- Std.Sync.RecursiveMutex
/-- Creates a new recursive mutex.  -/
Std.RecursiveMutex.new : {α : Type} → α → BaseIO (Std.RecursiveMutex α)
-- Mathlib.Data.Fin.SuccPred
/-- Embedding `i : Fin n` into `Fin (n + 1)` with a hole around `p : Fin (n + 1)`
embeds `i` by `succ` when the resulting `p < i.succ`.  -/
Fin.succAbove_of_le_castSucc : ∀ {n : ℕ} (p : Fin (n + 1)) (i : Fin n), p ≤ i.castSucc → p.succAbove i = i.succ
-- Mathlib.RingTheory.PowerSeries.Substitution
/-- A more general version of `HasSubst.smul`.  -/
PowerSeries.HasSubst.smul' : ∀ {A : Type u_1} [inst : CommRing A] {R : Type u_2} [inst_1 : CommRing R] [inst_2 : Algebra A R] {τ : Type u_3}
  {f : MvPowerSeries τ R} (a : A), PowerSeries.HasSubst f → PowerSeries.HasSubst (a • f)
-- Mathlib.RepresentationTheory.Coinvariants
Representation.Coinvariants.map_mk : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : CommRing k] [inst_1 : Monoid G]
  [inst_2 : AddCommGroup V] [inst_3 : Module k V] [inst_4 : AddCommGroup W] [inst_5 : Module k W]
  {ρ : Representation k G V} {τ : Representation k G W} (f : ρ.IntertwiningMap τ) (x : V),
  (Representation.Coinvariants.map ρ τ f) ((Representation.Coinvariants.mk ρ) x) =
    (Representation.Coinvariants.mk τ) (f x)
-- Mathlib.Data.Finsupp.Defs
Finsupp.equivFunOnFinite_symm_apply_apply : ∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] [inst_1 : Finite α] (f : α → M) (a : α),
  (Finsupp.equivFunOnFinite.symm f) a = f a
-- Mathlib.RingTheory.WittVector.Defs
WittVector.eval.eq_1 : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] {k : ℕ} (φ : ℕ → MvPolynomial (Fin k × ℕ) ℤ) (x : Fin k → WittVector p R),
  WittVector.eval φ x = WittVector.mk p fun n => WittVector.peval (φ n) fun i => (x i).coeff
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
ProfiniteGrp.ProfiniteCompletion.finiteGrpDiagram.eq_1 : ∀ (G : GrpCat),
  ProfiniteGrp.ProfiniteCompletion.finiteGrpDiagram G =
    { obj := fun H => FiniteGrp.of (↑G ⧸ H.toSubgroup),
      map := fun {X Y} f => FiniteGrp.ofHom (QuotientGroup.map X.toSubgroup Y.toSubgroup (MonoidHom.id ↑G) ⋯),
      map_id := ⋯, map_comp := ⋯ }
-- Mathlib.Algebra.Group.Subgroup.Ker
/-- The kernel of a homomorphism composed with an isomorphism is equal to the kernel of
the homomorphism mapped by the inverse isomorphism.  -/
MonoidHom.ker_comp_mulEquiv : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {P : Type u_8} [inst_2 : MulOneClass P] (g : N →* P)
  (iso : G ≃* N), (g.comp ↑iso).ker = Subgroup.map (↑iso.symm) g.ker
-- Lean.Parser.Types
Lean.Parser.Error.mk : Lean.Syntax → String → List String → Lean.Parser.Error
-- Mathlib.Data.Set.Card
Set.ncard_eq_two : ∀ {α : Type u_1} {s : Set α}, s.ncard = 2 ↔ ∃ x y, x ≠ y ∧ s = {x, y}
-- Mathlib.NumberTheory.NumberField.Discriminant.Basic
NumberField.mixedEmbedding.covolume_idealLattice : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ),
  ZLattice.covolume (NumberField.mixedEmbedding.idealLattice K I) MeasureTheory.volume =
    ↑(FractionalIdeal.absNorm ↑I) * 2⁻¹ ^ NumberField.InfinitePlace.nrComplexPlaces K * √|↑(NumberField.discr K)|
-- Mathlib.Topology.Algebra.ConstMulAction
nhds_smul : ∀ {α : Type u_2} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : Group G] [inst_2 : MulAction G α]
  [ContinuousConstSMul G α] (c : G) (x : α), nhds (c • x) = c • nhds x
-- Mathlib.RingTheory.Kaehler.JacobiZariski
Algebra.Generators.CotangentSpace.compEquiv_symm_inr : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {T : Type u₃}
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] {ι : Type w₁}
  {σ : Type w₂} (Q : Algebra.Generators S T ι) (P : Algebra.Generators R S σ),
  ↑(Algebra.Generators.CotangentSpace.compEquiv Q P).symm ∘ₗ
      LinearMap.inr T Q.toExtension.CotangentSpace (TensorProduct S T P.toExtension.CotangentSpace) =
    LinearMap.liftBaseChange T (Algebra.Extension.CotangentSpace.map (Q.toComp P).toExtensionHom)
-- Init.Grind.Ring.Basic
Lean.Grind.Ring.neg_mul : ∀ {α : Type u} [inst : Lean.Grind.Ring α] (a b : α), -a * b = -(a * b)
-- Mathlib.Analysis.SpecialFunctions.Exp
ContinuousOn.cexp : ∀ {α : Type u_1} [inst : TopologicalSpace α] {f : α → ℂ} {s : Set α},
  ContinuousOn f s → ContinuousOn (fun y => Complex.exp (f y)) s
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_eraseKey_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k fallback : α},
  Std.Internal.List.DistinctKeys l → Std.Internal.List.getKeyD k (Std.Internal.List.eraseKey k l) fallback = fallback
-- Mathlib.Topology.UniformSpace.UniformApproximation
/-- If `Fₙ` converges locally uniformly on a neighborhood of `x` to a function `f` which is
continuous at `x`, and `gₙ` tends to `x`, then `Fₙ (gₙ)` tends to `f x`.  -/
tendsto_comp_of_locally_uniform_limit : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {F : ι → α → β}
  {f : α → β} {x : α} {p : Filter ι} {g : ι → α},
  ContinuousAt f x →
    Filter.Tendsto g p (nhds x) →
      (∀ u ∈ uniformity β, ∃ t ∈ nhds x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u) →
        Filter.Tendsto (fun n => F n (g n)) p (nhds (f x))
-- Mathlib.Topology.Semicontinuity.Defs
/-- **Alias** of the reverse direction of `upperHemicontinuousWithinAt_iff_frequently`. -/
UpperHemicontinuousWithinAt.of_frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {x : α}
  {s : Set α},
  (∀ (t : Set β), IsClosed t → (∃ᶠ (x' : α) in nhdsWithin x s, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty) →
    UpperHemicontinuousWithinAt f s x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] [inst_1 : BEq α] [Std.LawfulBEqOrd α] (h : t.WF) {l : List ((a : α) × β a)} {k : α},
  (List.map Sigma.fst l).contains k = false → (↑(t.insertMany l ⋯)).get? k = t.get? k
-- Mathlib.Order.Hom.CompleteLattice
FrameHom.toInfTopHom : {α : Type u_8} →
  {β : Type u_9} → [inst : CompleteLattice α] → [inst_1 : CompleteLattice β] → FrameHom α β → InfTopHom α β
-- Mathlib.Data.Num.Lemmas
/-- This tactic tries to turn an (in)equality about `Num`s to one about `Nat`s by rewriting.
```lean
example (n : Num) (m : Num) : n ≤ n + m := by
  transfer_rw
  exact Nat.le_add_right _ _
```
 -/
Num.transfer_rw : Lean.ParserDescr
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
/-- A choice of isomorphism `T₁ ≅ T₂` between two distinguished triangles
when we are given two isomorphisms `e₁ : T₁.obj₁ ≅ T₂.obj₁` and `e₃ : T₁.obj₃ ≅ T₂.obj₃`.  -/
CategoryTheory.Pretriangulated.isoTriangleOfIso₁₃ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.HasShift C ℤ] →
        [inst_3 : CategoryTheory.Preadditive C] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [hC : CategoryTheory.Pretriangulated C] →
              (T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C) →
                T₁ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
                  T₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
                    (e₁ : T₁.obj₁ ≅ T₂.obj₁) →
                      (e₃ : T₁.obj₃ ≅ T₂.obj₃) →
                        CategoryTheory.CategoryStruct.comp T₁.mor₃ ((CategoryTheory.shiftFunctor C 1).map e₁.hom) =
                            CategoryTheory.CategoryStruct.comp e₃.hom T₂.mor₃ →
                          (T₁ ≅ T₂)
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpTheorem.post : Lean.Meta.SimpTheorem → Bool
-- Mathlib.Analysis.Complex.Arg
Complex.norm_add_eq : ∀ {x y : ℂ}, x.arg = y.arg → ‖x + y‖ = ‖x‖ + ‖y‖
-- Mathlib.ModelTheory.Arithmetic.Presburger.Basic
FirstOrder.Language.presburger.natCast_succ : ∀ {α : Type u_1} (n : ℕ), ↑(n + 1) = ↑n + 1
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C] {J : CategoryTheory.Precoverage C} [J.HasPullbacks]
  [J.IsStableUnderBaseChange] (P : CategoryTheory.Functor Cᵒᵖ (Type u_1)),
  CategoryTheory.Presieve.IsSheaf J.toGrothendieck P ↔
    ∀ ⦃X : C⦄, ∀ R ∈ J.coverings X, CategoryTheory.Presieve.IsSheafFor P R
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.Measure.ext_iff' : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ₁ μ₂ : MeasureTheory.Measure α}, μ₁ = μ₂ ↔ ∀ (s : Set α), μ₁ s = μ₂ s
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.corec_cons : ∀ {β : Type u_1} {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis} {exp : ℝ}
  {coef : Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl} {next : β}
  {f : β → Option (ℝ × Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl × β)} {b : β},
  f b = some (exp, coef, next) →
    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.corec f b =
      Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons exp coef
        (Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.corec f next)
-- Lean.Level
Lean.LMVarIdSet : Type
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_eq_some_get! : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited β] {a : α},
  a ∈ m → Std.DHashMap.Const.get? m a = some (Std.DHashMap.Const.get! m a)
-- Mathlib.Algebra.Category.CommHopfAlgCat
instIsCommMonObjOppositeCommAlgCatXUnopGrpObjCommHopfAlgCatFunctorCommHopfAlgCatEquivCogrpCommAlgCatOfIsCocommX : ∀ {R : Type u} [inst : CommRing R] {A : CommHopfAlgCat R} [Coalgebra.IsCocomm R ↑A],
  CategoryTheory.IsCommMonObj (Opposite.unop ((commHopfAlgCatEquivCogrpCommAlgCat R).functor.obj A)).X
-- Mathlib.Data.QPF.Multivariate.Constructions.Fix
MvQPF.Fix.mk.eq_1 : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (x : F (α ::: MvQPF.Fix F α)),
  MvQPF.Fix.mk x =
    Quot.mk (⇑(MvQPF.wSetoid α)) ((MvQPF.P F).wMk' (MvFunctor.map (TypeVec.id ::: MvQPF.fixToW) (MvQPF.repr x)))
-- Mathlib.ModelTheory.Equivalence
FirstOrder.Language.BoundedFormula.inf_not_iff_bot : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} (φ : L.BoundedFormula α n), T.Iff (φ ⊓ φ.not) ⊥