mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Fourier.Notation
FourierSMul.fourier_smul : ∀ {R : Type u_5} {E : Type u_6} {F : outParam (Type u_7)} {inst : SMul R E} {inst_1 : SMul R F}
  {inst_2 : FourierTransform E F} [self : FourierSMul R E F] (r : R) (f : E),
  FourierTransform.fourier (r • f) = r • FourierTransform.fourier f
-- Init.Data.Rat.Lemmas
Rat.le_of_mul_le_mul_right : ∀ {a b c : ℚ}, a * c ≤ b * c → 0 < c → a ≤ b
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
CategoryTheory.instReflectiveSSetCatNerveFunctor : CategoryTheory.Reflective CategoryTheory.nerveFunctor
-- Init.Data.SInt.Lemmas
Int64.ofBitVec_iSizeToBitVec : ∀ (x : ISize), Int64.ofBitVec (BitVec.signExtend 64 x.toBitVec) = x.toInt64
-- Mathlib.Analysis.Calculus.FDeriv.Linear
ContinuousLinearMap.differentiableWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] (f : E →L[𝕜] F) {x : E} {s : Set E}, DifferentiableWithinAt 𝕜 (⇑f) s x
-- Mathlib.Condensed.Light.InternallyProjective
/-- Given a `P : LightCondSet`, the light free light condensed module `R[P]` is internally projective if
and only if, for all `A B : LightCondMod R`, for all epimorphisms `e : A ⟶ B`, for all
`S : LightProfinite` and all morphisms `g : R[P × S] ⟶ B`, there exists a `S' : LightProfinite`
with a surjection `π : S' ⟶ S` and a morphism `g' : R[P × S'] ⟶ A`, making the diagram
```
R[P × S'] --> A
  |           |
  v           v
R[P × S]  --> B
```
commute.
 -/
LightCondensed.free_internallyProjective_iff_tensor_condition : ∀ (R : Type u) [inst : CommRing R] (P : LightCondSet),
  CategoryTheory.InternallyProjective ((LightCondensed.free R).obj P) ↔
    ∀ {A B : LightCondMod R} (e : A ⟶ B) [CategoryTheory.Epi e] (S : LightProfinite)
      (g : (LightCondensed.free R).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj P S.toCondensed) ⟶ B),
      ∃ S' π,
        ∃ (_ : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom π)),
          ∃ g',
            CategoryTheory.CategoryStruct.comp
                ((LightCondensed.free R).map
                  (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P (lightProfiniteToLightCondSet.map π)))
                g =
              CategoryTheory.CategoryStruct.comp g' e
-- Mathlib.Order.Filter.AtTopBot.Tendsto
Filter.Tendsto.eventually_lt_atBot : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder β] [NoBotOrder β] {f : α → β} {l : Filter α},
  Filter.Tendsto f l Filter.atBot → ∀ (c : β), ∀ᶠ (x : α) in l, f x < c
-- Mathlib.Algebra.Category.MonCat.Basic
/-- Universe lift functor for additive monoids.  -/
AddMonCat.uliftFunctor : CategoryTheory.Functor AddMonCat AddMonCat
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Bicone.toCocone_inj : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) (j : J),
  CategoryTheory.Limits.Cofan.inj B.toCocone j = B.ι j
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
WeakFEPair.g_modif.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (P : WeakFEPair E),
  P.g_modif =
    ((Set.Ioi 1).indicator fun x => P.g x - P.g₀) +
      (Set.Ioo 0 1).indicator fun x => P.g x - (P.ε⁻¹ * ↑(x ^ (-P.k))) • P.f₀
-- Lean.Elab.DocString
/-- Retrieves a flag from the arguments to a documentation extension. Returns `default` if the flag is
not explicit set.
 -/
Lean.Doc.getFlag : Lean.Name → Bool → StateT (Array (Lean.TSyntax `doc_arg)) Lean.Doc.DocM Bool
-- Mathlib.Combinatorics.Additive.FreimanHom
IsAddFreimanIso.prodMap : ∀ {α₁ : Type u_5} {α₂ : Type u_6} {β₁ : Type u_7} {β₂ : Type u_8} [inst : AddCommMonoid α₁] [inst_1 : AddCommMonoid α₂]
  [inst_2 : AddCommMonoid β₁] [inst_3 : AddCommMonoid β₂] {A₁ : Set α₁} {A₂ : Set α₂} {B₁ : Set β₁} {B₂ : Set β₂}
  {f₁ : α₁ → β₁} {f₂ : α₂ → β₂} {n : ℕ},
  IsAddFreimanIso n A₁ B₁ f₁ → IsAddFreimanIso n A₂ B₂ f₂ → IsAddFreimanIso n (A₁ ×ˢ A₂) (B₁ ×ˢ B₂) (Prod.map f₁ f₂)
-- Mathlib.RingTheory.Algebraic.Integral
IsAlgebraic.zsmul : ∀ {R : Type u_1} {A : Type u_3} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {a : A},
  IsAlgebraic R a → ∀ (n : ℤ), IsAlgebraic R (n • a)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
inv_anti₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] [MulPosReflectLT G₀]
  {a b : G₀}, 0 < b → b ≤ a → a⁻¹ ≤ b⁻¹
-- Init.Data.Int.DivMod.Lemmas
Int.add_fmod : ∀ (a b n : ℤ), (a + b).fmod n = (a.fmod n + b.fmod n).fmod n
-- Init.Grind.ToIntLemmas
Lean.Grind.IntInterval.lo?.eq_3 : ∀ (hi : ℤ), (Lean.Grind.IntInterval.io hi).lo? = none
-- Lean.Expr
Lean.Expr.appArg!' : Lean.Expr → Lean.Expr
-- Mathlib.Logic.Equiv.Set
Equiv.image_subset : ∀ {α : Type u_3} {β : Type u_4} (e : α ≃ β) (s t : Set α), ⇑e '' s ⊆ ⇑e '' t ↔ s ⊆ t
-- Init.Data.Nat.Div.Basic
Nat.mul_add_mod_self_right : ∀ (a b c : ℕ), (a * b + c) % b = c % b
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.topEquiv_toMulHom : ∀ {M : Type u_1} [inst : Mul M], ↑Subsemigroup.topEquiv = MulMemClass.subtype ⊤
-- Mathlib.Algebra.Polynomial.Expand
Polynomial.coeff_contract : ∀ {R : Type u} [inst : CommSemiring R] {p : ℕ},
  p ≠ 0 → ∀ (f : Polynomial R) (n : ℕ), (Polynomial.contract p f).coeff n = f.coeff (n * p)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.operator : Lean.Lsp.CompletionItemKind
-- Mathlib.GroupTheory.PresentedGroup
PresentedGroup.to_group_eq_one_of_mem_closure : ∀ {α : Type u_1} {G : Type u_3} [inst : Group G] {f : α → G} {rels : Set (FreeGroup α)},
  (∀ r ∈ rels, (FreeGroup.lift f) r = 1) → ∀ x ∈ Subgroup.normalClosure rels, (FreeGroup.lift f) x = 1
-- Mathlib.Algebra.Exact.Basic
LinearMap.exact_map_mkQ_range : ∀ {R : Type u_8} {M : Type u_9} {N : Type u_10} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (f : M →ₗ[R] N), Function.Exact ⇑f ⇑f.range.mkQ
-- Mathlib.RingTheory.Derivation.MapCoeffs
Derivation.apply_aeval_eq : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {B : Type u_4}
  {M' : Type u_5} [inst_3 : CommRing B] [inst_4 : Algebra R B] [inst_5 : Algebra A B] [inst_6 : AddCommGroup M']
  [inst_7 : Module B M'] [inst_8 : Module R M'] [inst_9 : Module A M'] [inst_10 : IsScalarTower R A B]
  [inst_11 : IsScalarTower A B M'] (d : Derivation R B M') (x : B) (p : Polynomial A),
  d ((Polynomial.aeval x) p) =
    (PolynomialModule.eval x) ((PolynomialModule.map B LinearMap.id) ((Derivation.compAlgebraMap A d).mapCoeffs p)) +
      (Polynomial.aeval x) (Polynomial.derivative p) • d x
-- Init.Data.Fin.Basic
/-- Uses a proof that two bounds are equal to allow a value bounded by one to be used with the other.

In other words, when `eq : n = m`, `Fin.cast eq i` converts `i : Fin n` into a `Fin m`.
 -/
Fin.cast : {n m : ℕ} → n = m → Fin n → Fin m
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.const.inj : ∀ {w : ℕ} {val val_1 : BitVec w},
  Std.Tactic.BVDecide.BVExpr.const val = Std.Tactic.BVDecide.BVExpr.const val_1 → val = val_1
-- Mathlib.Probability.Kernel.Composition.ParallelComp
ProbabilityTheory.Kernel.parallelComp_def : ∀ {α : Type u_5} {β : Type u_6} {γ : Type u_7} {δ : Type u_8} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} (κ : ProbabilityTheory.Kernel α β)
  (η : ProbabilityTheory.Kernel γ δ),
  κ.parallelComp η =
    if h : ProbabilityTheory.IsSFiniteKernel κ ∧ ProbabilityTheory.IsSFiniteKernel η then
      { toFun := fun x => (κ x.1).prod (η x.2), measurable' := ⋯ }
    else 0
-- Lean.Meta.ArgsPacker
/-- Given expression `e` of type `(x : A ⊗' B ⊗' … ⊗' D) → R[x]`
return expression of type `(x : A) → (y : B) → … → (z : D) → R[(x,y,z)]`
 -/
_private.Lean.Meta.ArgsPacker.0.Lean.Meta.ArgsPacker.Unary.curry : Array Lean.Name → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.Bicategory.Coherence
CategoryTheory.FreeBicategory.normalizeAux.eq_1 : ∀ {B : Type u} [inst : Quiver B] {a : B} (x x_1 : B) (x_2 : Quiver.Path a x) (f : x ⟶ x_1),
  CategoryTheory.FreeBicategory.normalizeAux x_2 (CategoryTheory.FreeBicategory.Hom.of f) = x_2.cons f
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.nsmul_apply : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂] (r : ℕ)
  (f : NormedAddGroupHom V₁ V₂) (v : V₁), (r • f) v = r • f v
-- Init.Data.SInt.Bitwise
Int32.ne_not_self : ∀ {a : Int32}, a ≠ ~~~a
-- Init.Data.String.Lemmas.Order
String.Pos.ne_next : ∀ {s : String} {p : s.Pos} {h : p ≠ s.endPos}, p ≠ p.next h
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverseObj_comon_counit_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C (CategoryTheory.Comon D)) (X : C),
  CategoryTheory.ComonObj.counit.app X = CategoryTheory.ComonObj.counit
-- Init.Data.BitVec.Lemmas
BitVec.cpopNatRec_le_of_pos_le : ∀ {w : ℕ} {x : BitVec w} {pos pos' acc : ℕ}, pos ≤ pos' → x.cpopNatRec pos acc ≤ x.cpopNatRec pos' acc
-- Init.Data.Array.Find
Array.idxOf_lt_length_of_mem : ∀ {α : Type u_1} {a : α} [inst : BEq α] [LawfulBEq α] {xs : Array α}, a ∈ xs → Array.idxOf a xs < xs.size
-- Mathlib.Computability.Primrec.List
Primrec.fin_curry : ∀ {α : Type u_1} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable σ] {n : ℕ} {f : α → Fin n → σ},
  Primrec f ↔ Primrec₂ f
-- Mathlib.Data.Int.ModEq
AddCommGroup.intCast_modEq_intCast' : ∀ {G : Type u_1} [inst : AddCommGroupWithOne G] [CharZero G] {a b : ℤ} {n : ℕ}, ↑a ≡ ↑b [PMOD ↑n] ↔ a ≡ b [PMOD ↑n]
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem?_eq_some_iff : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β}, m[k]? = some v ↔ ∃ (h : k ∈ m), m[k] = v
-- Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
HasStrictFDerivAt.continuousAlternatingMap_apply : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F [⋀^ι]→L[𝕜] G} {f' : E →L[𝕜] F [⋀^ι]→L[𝕜] G}
  {g : ι → E → F} {g' : ι → E →L[𝕜] F} {x : E} [inst_7 : Fintype ι] [inst_8 : DecidableEq ι],
  HasStrictFDerivAt f f' x →
    (∀ (i : ι), HasStrictFDerivAt (g i) (g' i) x) →
      HasStrictFDerivAt (fun x => (f x) fun x_1 => g x_1 x)
        ((ContinuousAlternatingMap.apply 𝕜 F G fun x_1 => g x_1 x) ∘SL f' +
          ∑ i, (f x).toContinuousLinearMap (fun x_1 => g x_1 x) i ∘SL g' i)
        x
-- Mathlib.MeasureTheory.Function.AbsolutelyContinuous
/-- If `f` is interval integrable on `a..b` and `c ∈ uIcc a b`, then `fun x ↦ ∫ v in c..x, f v` is
absolutely continuous on `uIcc a b`.  -/
IntervalIntegrable.absolutelyContinuousOnInterval_intervalIntegral : ∀ {f : ℝ → ℝ} {a b c : ℝ},
  IntervalIntegrable f MeasureTheory.volume a b →
    c ∈ Set.uIcc a b → AbsolutelyContinuousOnInterval (fun x => ∫ (v : ℝ) in c..x, f v) a b
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.one_lt_rootMultiplicity_iff_isRoot_gcd : ∀ {R : Type u} [inst : CommRing R] [inst_1 : GCDMonoid (Polynomial R)] {p : Polynomial R} {t : R},
  p ≠ 0 → (1 < Polynomial.rootMultiplicity t p ↔ (gcd p (Polynomial.derivative p)).IsRoot t)
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Hom.comp.inj : ∀ {B : Type u} {inst : Quiver B} {a b c : B} {f : CategoryTheory.FreeBicategory.Hom a b}
  {g : CategoryTheory.FreeBicategory.Hom b c} {b_1 : B} {f_1 : CategoryTheory.FreeBicategory.Hom a b_1}
  {g_1 : CategoryTheory.FreeBicategory.Hom b_1 c}, f.comp g = f_1.comp g_1 → b = b_1 ∧ f ≍ f_1 ∧ g ≍ g_1
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.NormalExpr.nil.inj : ∀ {e : Mathlib.Tactic.BicategoryLike.Mor₂} {α : Mathlib.Tactic.BicategoryLike.Structural}
  {e_1 : Mathlib.Tactic.BicategoryLike.Mor₂} {α_1 : Mathlib.Tactic.BicategoryLike.Structural},
  Mathlib.Tactic.BicategoryLike.NormalExpr.nil e α = Mathlib.Tactic.BicategoryLike.NormalExpr.nil e_1 α_1 →
    e = e_1 ∧ α = α_1
-- Mathlib.Algebra.DirectSum.Internal
SetLike.GradeZero.instAlgebraSubtypeMemOfNat : {ι : Type u_1} →
  {σ : Type u_2} →
    {R : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : AddMonoid ι] →
          [inst_2 : SetLike σ R] →
            [inst_3 : AddSubmonoidClass σ R] → (A : ι → σ) → [inst_4 : SetLike.GradedMonoid A] → Algebra (↥(A 0)) R
-- Plausible.Shrinkable
/-- Shrink a list of a shrinkable type, either by discarding an element or shrinking an element.  -/
Plausible.List.shrinkable : {α : Type u_1} → [Plausible.Shrinkable α] → Plausible.Shrinkable (List α)
-- Init.Data.Nat.Bitwise.Lemmas
Nat.instIdempotentOpHOr : Std.IdempotentOp fun x1 x2 => x1 ||| x2
-- Init.Data.Array.Lemmas
Array.mem_reverse : ∀ {α : Type u_1} {x : α} {xs : Array α}, x ∈ xs.reverse ↔ x ∈ xs
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi
cfc_map_prod : ∀ {A : Type u_1} {B : Type u_2} {R : Type u_3} {S : Type u_4} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : MetricSpace R] [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : CommRing S]
  [inst_6 : Algebra R S] [inst_7 : Ring A] [inst_8 : Ring B] [inst_9 : Algebra S A] [inst_10 : Algebra S B]
  [inst_11 : Algebra R A] [inst_12 : Algebra R B] [IsScalarTower R S A] [IsScalarTower R S B] [inst_15 : StarRing A]
  [inst_16 : StarRing B] [inst_17 : TopologicalSpace A] [inst_18 : TopologicalSpace B] {pab : A × B → Prop}
  {pa : A → Prop} {pb : B → Prop} [inst_19 : ContinuousFunctionalCalculus R (A × B) pab]
  [inst_20 : ContinuousFunctionalCalculus R A pa] [inst_21 : ContinuousFunctionalCalculus R B pb]
  [ContinuousMap.UniqueHom R A] [ContinuousMap.UniqueHom R B] (f : R → R) (a : A) (b : B),
  autoParam (ContinuousOn f (spectrum R a ∪ spectrum R b)) cfc_map_prod._auto_1 →
    autoParam (pab (a, b)) cfc_map_prod._auto_3 →
      autoParam (pa a) cfc_map_prod._auto_5 → autoParam (pb b) cfc_map_prod._auto_7 → cfc f (a, b) = (cfc f a, cfc f b)
-- Mathlib.Algebra.Order.SuccPred
Order.IsSuccLimit.add_one_lt : ∀ {α : Type u_1} {x y : α} [inst : PartialOrder α] [inst_1 : Add α] [inst_2 : One α] [SuccAddOrder α],
  Order.IsSuccLimit x → y < x → y + 1 < x
-- Mathlib.RingTheory.AlgebraicIndependent.Transcendental
AlgebraicIndependent.iff_adjoin_image : ∀ {ι : Type u_1} {R : Type u_3} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A] (s : Set ι),
  AlgebraicIndependent R x ↔
    (AlgebraicIndependent R fun i => x ↑i) ∧ AlgebraicIndepOn (↥(Algebra.adjoin R (x '' s))) x sᶜ
-- Aesop.Forward.State
Aesop.instToMessageDataRuleState : Lean.ToMessageData Aesop.RuleState
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKeyD_diff_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k fallback : α}, k ∈ t₂ → (t₁ \ t₂).getKeyD k fallback = fallback
-- Mathlib.CategoryTheory.EssentiallySmall
CategoryTheory.ShrinkHoms.to_from : ∀ {C' : Type u_1} (X : C'), (CategoryTheory.ShrinkHoms.toShrinkHoms X).fromShrinkHoms = X
-- Batteries.Data.List.Perm
List.cons_uncurry_swapAt_perm_cons : ∀ {α : Type u_1} (xs : List α) (i : ℕ) (v : α), (Function.uncurry List.cons (xs.swapAt i v)).Perm (v :: xs)
-- Mathlib.Analysis.Complex.Circle
Circle.norm_coe : ∀ (z : Circle), ‖↑z‖ = 1
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.toLinearMap : {R : Type u_1} →
  {R₂ : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : Semiring R₂] →
        {σ₁₂ : R →+* R₂} →
          {E : Type u_11} →
            {E₂ : Type u_12} →
              [inst_2 : SeminormedAddCommGroup E] →
                [inst_3 : SeminormedAddCommGroup E₂] →
                  [inst_4 : Module R E] → [inst_5 : Module R₂ E₂] → (E →ₛₗᵢ[σ₁₂] E₂) → E →ₛₗ[σ₁₂] E₂
-- Mathlib.RingTheory.AdicCompletion.Basic
IsHausdorff.haus : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  IsHausdorff I M → ∀ (x : M), (∀ (n : ℕ), x ≡ 0 [SMOD I ^ n • ⊤]) → x = 0
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_filter! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] {f : (a : α) → β a → Bool} {k : α},
  t.WF → Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.filter! f t) = Option.any (f k) (t.get? k)
-- Mathlib.CategoryTheory.Sites.Point.Skyscraper
CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv_naturality_right_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.Limits.HasProducts A]
  {P : CategoryTheory.Functor Cᵒᵖ A} {M N : A} [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A]
  (f : Φ.presheafFiber.obj P ⟶ M) (g : M ⟶ N) {Z : CategoryTheory.Functor Cᵒᵖ A} (h : Φ.skyscraperPresheaf N ⟶ Z),
  CategoryTheory.CategoryStruct.comp (Φ.skyscraperPresheafHomEquiv (CategoryTheory.CategoryStruct.comp f g)) h =
    CategoryTheory.CategoryStruct.comp (Φ.skyscraperPresheafHomEquiv f)
      (CategoryTheory.CategoryStruct.comp (Φ.skyscraperPresheafFunctor.map g) h)
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.instIsLeftAdjointModuleCatWithModuleTopology : ∀ (R : Type u) [inst : Ring R] [inst_1 : TopologicalSpace R], (TopModuleCat.withModuleTopology R).IsLeftAdjoint
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.restrictScalars_self : ∀ (R : Type u_1) {M : Type u_8} {M₂ : Type u_10} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M] [inst_4 : Module R M₂] (f : M →ₗ[R] M₂), ↑R f = f
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.add_def : ∀ {M : Type u_4} [inst : AddZeroClass M] (S : AddSubmonoid M) (x y : ↥S), x + y = ⟨↑x + ↑y, ⋯⟩
-- Mathlib.Algebra.Lie.Normalizer
/-- A Lie subalgebra is an ideal of its normalizer.  -/
LieSubalgebra.ideal_in_normalizer : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  {H : LieSubalgebra R L} {x y : L}, x ∈ H.normalizer → y ∈ H → ⁅x, y⁆ ∈ H
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Zipper.toList.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Zipper α β → Sort u_3)
  (h_1 : Unit → motive Std.DTreeMap.Internal.Zipper.done)
  (h_2 :
    (k : α) →
      (v : β k) →
        (tree : Std.DTreeMap.Internal.Impl α β) →
          (next : Std.DTreeMap.Internal.Zipper α β) → motive (Std.DTreeMap.Internal.Zipper.cons k v tree next)),
  (match Std.DTreeMap.Internal.Zipper.done with
    | Std.DTreeMap.Internal.Zipper.done => h_1 ()
    | Std.DTreeMap.Internal.Zipper.cons k v tree next => h_2 k v tree next) =
    h_1 ()
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.lengthTRAux.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → ℕ → Sort u_2) (n : ℕ) (h_1 : (n : ℕ) → motive [] n)
  (h_2 : (head : α) → (as : List α) → (n : ℕ) → motive (head :: as) n),
  (match [], n with
    | [], n => h_1 n
    | head :: as, n => h_2 head as n) =
    h_1 n
-- Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
/-- The formula which characterises the output of `modularCyclotomicCharacter g n`.  -/
modularCyclotomicCharacter.toFun_spec : ∀ {L : Type u} [inst : CommRing L] [inst_1 : IsDomain L] (g : L ≃+* L) {n : ℕ} [inst_2 : NeZero n]
  (t : ↥(rootsOfUnity n L)), g ↑↑t = ↑(↑t ^ (modularCyclotomicCharacter.toFun n g).val)
-- Mathlib.Order.Interval.Multiset
Multiset.Ico_add_Ico_eq_Ico : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] {a b c : α},
  a ≤ b → b ≤ c → Multiset.Ico a b + Multiset.Ico b c = Multiset.Ico a c
-- Mathlib.CategoryTheory.Endomorphism
CategoryTheory.Aut.Aut_inv_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) (f : CategoryTheory.Aut X),
  f⁻¹ = CategoryTheory.Iso.symm f
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
CategoryTheory.Localization.Preadditive.add_eq_add : ∀ {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] [inst_2 : CategoryTheory.Preadditive C]
  {L : CategoryTheory.Functor C D} (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  [inst_4 : W.HasLeftCalculusOfFractions] {X Y : C} {X' Y' : D} (eX : L.obj X ≅ X') (eY : L.obj Y ≅ Y') {X'' Y'' : C}
  (eX' : L.obj X'' ≅ X') (eY' : L.obj Y'' ≅ Y') (f₁ f₂ : X' ⟶ Y'),
  CategoryTheory.Localization.Preadditive.add W eX eY f₁ f₂ =
    CategoryTheory.Localization.Preadditive.add W eX' eY' f₁ f₂
-- Mathlib.LinearAlgebra.AffineSpace.Basis
AffineBasis.surjective_coord : ∀ {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : Ring k] [inst_3 : Module k V] (b : AffineBasis ι k P) [Nontrivial ι] (i : ι),
  Function.Surjective ⇑(b.coord i)
-- Mathlib.Logic.Function.Defs
Function.Injective.beq_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : BEq α] [LawfulBEq α] [inst_2 : BEq β] [LawfulBEq β] {f : α → β},
  Function.Injective f → ∀ {a b : α}, (f a == f b) = (a == b)
-- Mathlib.GroupTheory.Congruence.Defs
/-- The infimum of two congruence relations equals the infimum of the underlying binary
operations.  -/
Con.coe_inf : ∀ {M : Type u_1} [inst : Mul M] {c d : Con M}, ⇑(c ⊓ d) = ⇑c ⊓ ⇑d
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.Triplet.hx : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (self : AlgebraicGeometry.Scheme.Pullback.Triplet f g),
  f self.x = self.s
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- If two additive homomorphisms from `R[M]` are equal on each `single r m`,
then they are equal.

We formulate this using equality of `AddMonoidHom`s so that `ext` tactic can apply a type-specific
extensionality lemma after this one.  E.g., if the fiber `M` is `ℕ` or `ℤ`, then it suffices to
verify `f (single a 1) = g (single a 1)`.

TODO: Rename to `addMonoidHom_ext'`.  -/
MonoidAlgebra.addHom_ext' : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {N : Type u_8} [inst_1 : AddZeroClass N]
  ⦃f g : MonoidAlgebra R M →+ N⦄,
  (∀ (m : M), f.comp (MonoidAlgebra.singleAddHom m) = g.comp (MonoidAlgebra.singleAddHom m)) → f = g
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupSeminorm.ext : ∀ {E : Type u_3} [inst : AddGroup E] {p q : NonarchAddGroupSeminorm E}, (∀ (x : E), p x = q x) → p = q
-- Mathlib.Analysis.Analytic.Constructions
alternatingGeometricSeries_apply_norm : ∀ (𝕜 : Type u_2) [inst : NontriviallyNormedField 𝕜] (A : Type u_7) [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  [NormOneClass A] (n : ℕ), ‖alternatingGeometricSeries 𝕜 A n‖ = 1
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Adjunction.mapMon_counit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (a : F ⊣ G) [inst_4 : F.Monoidal]
  [inst_5 : G.LaxMonoidal] [inst_6 : a.IsMonoidal],
  a.mapMon.counit =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.mapMonCompIso.inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.mapMonNatTrans a.counit)
        CategoryTheory.Functor.mapMonIdIso.hom)
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Path.Homotopy.transReflReparamAux_one : Path.Homotopy.transReflReparamAux 1 = 1