mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
/-- The forgetful functor from commutative group objects to group objects is fully faithful.  -/
CategoryTheory.CommGrp.fullyFaithfulForget₂Grp : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → (CategoryTheory.CommGrp.forget₂Grp C).FullyFaithful
-- Mathlib.Algebra.Order.Monoid.NatCast
one_lt_two : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [ZeroLEOneClass α] [NeZero 1]
  [AddLeftStrictMono α], 1 < 2
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.card_cliqueFinset_le : ∀ {α : Type u_1} {G : SimpleGraph α} [inst : Fintype α] [inst_1 : DecidableEq α] [inst_2 : DecidableRel G.Adj] {n : ℕ},
  (G.cliqueFinset n).card ≤ (Fintype.card α).choose n
-- Init.Grind.Norm
Lean.Grind.true_imp_eq : ∀ (p : Prop), (True → p) = p
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_trim_ae : ∀ {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {β : Type u_6} {m m0 : MeasurableSpace β}
  {μ : MeasureTheory.Measure β} (hm : m ≤ m0) {f : β → G},
  MeasureTheory.AEStronglyMeasurable f (μ.trim hm) → ∫ (x : β), f x ∂μ = ∫ (x : β), f x ∂μ.trim hm
-- Mathlib.Data.Fintype.BigOperators
/-- It is equivalent to compute the product of a function over `Fin n` or `Finset.range n`.  -/
Fin.prod_univ_eq_prod_range : ∀ {α : Type u_1} [inst : CommMonoid α] (f : ℕ → α) (n : ℕ), ∏ i, f ↑i = ∏ i ∈ Finset.range n, f i
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.mk : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor A B} →
              {G : CategoryTheory.Functor C B} →
                (fst : A) → (snd : C) → (F.obj fst ≅ G.obj snd) → CategoryTheory.Limits.CategoricalPullback F G
-- Mathlib.Algebra.Ring.Parity
Nat.not_odd_zero : ¬Odd 0
-- Init.Data.Order.Ord
List.instReflOrd : ∀ {α : Type u_1} [inst : Ord α] [Std.ReflOrd α], Std.ReflOrd (List α)
-- Mathlib.RingTheory.Radical.Basic
UniqueFactorizationMonoid.primeFactors_mul_eq_disjUnion : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  {a b : M} (hc : IsRelPrime a b),
  UniqueFactorizationMonoid.primeFactors (a * b) =
    (UniqueFactorizationMonoid.primeFactors a).disjUnion (UniqueFactorizationMonoid.primeFactors b) ⋯
-- Init.Data.UInt.Lemmas
UInt8.toUInt32_mul : ∀ (a b : UInt8), (a * b).toUInt32 = a.toUInt32 * b.toUInt32 % 256
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.evaluation_naturality_apply : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {V : Y.Opens} (x : ↥X) (hx : f x ∈ V)
  (s : ↑(Y.presheaf.obj (Opposite.op V))),
  (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.residueFieldMap f x))
      ((CategoryTheory.ConcreteCategory.hom (Y.evaluation V (f x) hx)) s) =
    (CategoryTheory.ConcreteCategory.hom (X.evaluation ((TopologicalSpace.Opens.map f.base).obj V) x hx))
      ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.app f V)) s)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roo.forIn'_toList_eq_forIn' : ∀ {α : Type u} {r : Std.Roo α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerableLT α] [inst_4 : Std.Rxo.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [inst_6 : Monad m]
  [LawfulMonad m] {f : (a : α) → a ∈ r.toList → γ → m (ForInStep γ)},
  forIn' r.toList init f = forIn' r init fun a ha acc => f a ⋯ acc
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.postComp_hom_app_right : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X : T} {E : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} E] (F : CategoryTheory.Functor T D)
  (G : CategoryTheory.Functor D E) (X_1 : CategoryTheory.Under X),
  ((CategoryTheory.Under.postComp F G).hom.app X_1).right = CategoryTheory.CategoryStruct.id (G.obj (F.obj X_1.right))
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.zipIdxTR.eq_1 : ∀ {α : Type u_1} (l : List α) (n : ℕ),
  l.zipIdxTR n =
    (Array.foldr
        (fun a x =>
          match x with
          | (n, acc) => (n - 1, (a, n - 1) :: acc))
        (n + l.toArray.size, []) l.toArray).2
-- Mathlib.Analysis.Analytic.WithLp
WithLp.analyticOn_toLp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 F] (p : ENNReal)
  [inst_5 : Fact (1 ≤ p)] (s : Set (E × F)), AnalyticOn 𝕜 (WithLp.toLp p) s
-- Mathlib.Data.Finsupp.Lex
/-- The linear order on `Finsupp`s obtained by the colexicographic ordering.  -/
Finsupp.Colex.linearOrder : {α : Type u_1} → {N : Type u_2} → [inst : Zero N] → [LinearOrder α] → [LinearOrder N] → LinearOrder (Colex (α →₀ N))
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.isoOfHom_id_inv : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : L.IsLocalization W] (X : C)
  (hX : W (CategoryTheory.CategoryStruct.id X)),
  (CategoryTheory.Localization.isoOfHom L W (CategoryTheory.CategoryStruct.id X) hX).inv =
    CategoryTheory.CategoryStruct.id (L.obj X)
-- Mathlib.Data.Sum.Lattice
Sum.Lex.inr_sup : ∀ {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β] (b₁ b₂ : β),
  Sum.inrₗ (b₁ ⊔ b₂) = Sum.inrₗ b₁ ⊔ Sum.inrₗ b₂
-- Mathlib.Computability.TuringMachine.StackTuringMachine
/-- The initial state of the TM2 model. The input is provided on a designated stack.  -/
Turing.TM2.init : {K : Type u_1} →
  {Γ : K → Type u_2} →
    {Λ : Type u_3} →
      {σ : Type u_4} → [Inhabited Λ] → [DecidableEq K] → [Inhabited σ] → (k : K) → List (Γ k) → Turing.TM2.Cfg Γ Λ σ
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Ideal.prime_of_mem_primesOver : ∀ {A : Type u_2} [inst : CommRing A] [IsDedekindDomain A] {R : Type u_4} [inst_2 : CommRing R] [inst_3 : Algebra R A]
  {p : Ideal R} [IsDomain R] [Module.IsTorsionFree R A], p ≠ ⊥ → ∀ {P : Ideal A}, P ∈ p.primesOver A → Prime P
-- Mathlib.RingTheory.MvPowerSeries.Expand
MvPowerSeries.map_expand : ∀ {σ : Type u_1} {R : Type u_3} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] (p : ℕ) (hp : p ≠ 0)
  (f : R →+* S) (φ : MvPowerSeries σ R),
  (MvPowerSeries.map f) ((MvPowerSeries.expand p hp) φ) = (MvPowerSeries.expand p hp) ((MvPowerSeries.map f) φ)
-- Std.Data.Internal.List.Associative
Std.Internal.List.insertListIfNewUnit_perm_of_perm_first : ∀ {α : Type u} [inst : BEq α] [EquivBEq α] {l1 l2 : List ((_ : α) × Unit)} {toInsert : List α},
  l1.Perm l2 →
    Std.Internal.List.DistinctKeys l1 →
      (Std.Internal.List.insertListIfNewUnit l1 toInsert).Perm (Std.Internal.List.insertListIfNewUnit l2 toInsert)
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.mk.congr_simp : ∀ {R : Type u_7} {S : Type u_8} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S]
  (toEquiv toEquiv_1 : R ≃ S) (e_toEquiv : toEquiv = toEquiv_1)
  (map_mul' : ∀ (x y : R), toEquiv.toFun (x * y) = toEquiv.toFun x * toEquiv.toFun y)
  (map_add' : ∀ (x y : R), toEquiv.toFun (x + y) = toEquiv.toFun x + toEquiv.toFun y),
  { toEquiv := toEquiv, map_mul' := map_mul', map_add' := map_add' } =
    { toEquiv := toEquiv_1, map_mul' := ⋯, map_add' := ⋯ }
-- Init.Data.Int.Pow
Int.instNeZeroHPowOfNat : ∀ {n : ℤ}, NeZero (n ^ 0)
-- Aesop.Script.Check
Aesop.Script.UScript.checkIfEnabled : Aesop.Script.UScript → Lean.MetaM Unit
-- Mathlib.CategoryTheory.Filtered.Small
CategoryTheory.IsFiltered.filteredClosure.below.max : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFilteredOrEmpty C] {α : Type w}
  {f : α → C} {motive : (a : C) → CategoryTheory.IsFiltered.filteredClosure f a → Prop} {j j' : C}
  (a : CategoryTheory.IsFiltered.filteredClosure f j) (a_1 : CategoryTheory.IsFiltered.filteredClosure f j'),
  CategoryTheory.IsFiltered.filteredClosure.below a →
    motive j a →
      CategoryTheory.IsFiltered.filteredClosure.below a_1 →
        motive j' a_1 → CategoryTheory.IsFiltered.filteredClosure.below ⋯
-- Mathlib.SetTheory.Ordinal.Basic
RelEmbedding.ordinal_type_le : ∀ {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [inst : IsWellOrder α r] [inst_1 : IsWellOrder β s]
  (h : r ↪r s), Ordinal.type r ≤ Ordinal.type s
-- Mathlib.Algebra.GroupWithZero.Action.Defs
boole_smul : ∀ {M₀ : Type u_2} {A : Type u_7} [inst : MonoidWithZero M₀] [inst_1 : Zero A] [inst_2 : MulActionWithZero M₀ A]
  (p : Prop) [inst_3 : Decidable p] (a : A), (if p then 1 else 0) • a = if p then a else 0
-- Lean.Parser.Term.Basic
Lean.Parser.Term.hole.formatter : Lean.PrettyPrinter.Formatter
-- Lean.Compiler.IR.Basic
Lean.IR.CtorInfo.size : Lean.IR.CtorInfo → ℕ
-- Mathlib.Topology.Algebra.FilterBasis
GroupFilterBasis.inv : ∀ {G : Type u} [inst : Group G] {B : GroupFilterBasis G} {U : Set G}, U ∈ B → ∃ V ∈ B, V ⊆ (fun x => x⁻¹) ⁻¹' U
-- Mathlib.Data.Set.Image
/-- The powerset of `{a} ∪ s` is `𝒫 s` together with `{a} ∪ t` for each `t ∈ 𝒫 s`.  -/
Set.powerset_insert : ∀ {α : Type u_1} (s : Set α) (a : α), 𝒫 insert a s = 𝒫 s ∪ insert a '' 𝒫 s
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.trStAct.eq_2 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [inst : DecidableEq K] {k : K}
  (q : Turing.TM1.Stmt (Turing.TM2to1.Γ' K Γ) (Turing.TM2to1.Λ' K Γ Λ σ) σ) (f : σ → Option (Γ k) → σ),
  Turing.TM2to1.trStAct q (Turing.TM2to1.StAct.peek f) =
    Turing.TM1.Stmt.move Turing.Dir.left
      (Turing.TM1.Stmt.load (fun a s => f s (a.2 k)) (Turing.TM1.Stmt.move Turing.Dir.right q))
-- Init.Data.Nat.Lemmas
Nat.eq_mul_of_div_eq_left : ∀ {a b c : ℕ}, b ∣ a → a / b = c → a = c * b
-- Mathlib.Analysis.Convolution
HasCompactSupport.convolution_integrand_bound_right_of_subset : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'}
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F]
  (L : E →L[𝕜] E' →L[𝕜] F) [inst_7 : AddGroup G] [inst_8 : TopologicalSpace G],
  HasCompactSupport g →
    Continuous g →
      ∀ {x t : G} {s u : Set G},
        x ∈ s → -tsupport g + s ⊆ u → ‖(L (f t)) (g (x - t))‖ ≤ u.indicator (fun t => ‖L‖ * ‖f t‖ * ⨆ i, ‖g i‖) t
-- Mathlib.Data.Fintype.Order
le_iSup_iff_of_directed : ∀ {ι : Sort u_1} {α : Type u_2} [inst : CompleteLattice α] {a : α} {f : ι → α} [Nonempty ι] [Finite ι],
  Directed (fun x1 x2 => x1 ≤ x2) f → (a ≤ ⨆ i, f i ↔ ∃ i, a ≤ f i)
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
ChainComplex.mk'.eq_1 : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] (X₀ X₁ : V)
  (d : X₁ ⟶ X₀)
  (succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' CategoryTheory.CategoryStruct.comp d f = 0),
  ChainComplex.mk' X₀ X₁ d succ' = ChainComplex.mk X₀ X₁ (succ' d).fst d (succ' d).snd.fst ⋯ fun S => succ' S.f
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Presheaf.restrictedULiftYoneda_obj_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {ℰ : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} ℰ]
  (A : CategoryTheory.Functor C ℰ) (X : ℰ) {X_1 Y : Cᵒᵖ} (f : X_1 ⟶ Y),
  ((CategoryTheory.Presheaf.restrictedULiftYoneda A).obj X).map f =
    TypeCat.ofHom fun x => { down := CategoryTheory.CategoryStruct.comp (A.map f.unop) x.down }
-- Mathlib.Order.UpperLower.Closure
lowerClosure_singleton : ∀ {α : Type u_1} [inst : Preorder α] (a : α), lowerClosure {a} = LowerSet.Iic a
-- Mathlib.Combinatorics.KatonaCircle
Numbering.disjoint_prefixed_prefixed : ∀ {X : Type u_1} [inst : Fintype X] {s t : Finset X} [inst_1 : DecidableEq X],
  ¬s ⊆ t → ¬t ⊆ s → Disjoint (Numbering.prefixed s) (Numbering.prefixed t)
-- Mathlib.Analysis.Matrix.Order
Matrix.isStrictlyPositive_iff_posDef : ∀ {𝕜 : Type u_1} {n : Type u_2} [inst : RCLike 𝕜] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {x : Matrix n n 𝕜},
  IsStrictlyPositive x ↔ x.PosDef
-- Lean.Meta.Tactic.FunIndInfo
Lean.Meta.FunIndInfo.params : Lean.Meta.FunIndInfo → Array Lean.Meta.FunIndParamKind
-- Init.Grind.Ring.Envelope
_private.Init.Grind.Ring.Envelope.0.Lean.Grind.Ring.OfSemiring.helper : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (h : Equivalence (Lean.Grind.Ring.OfSemiring.r α))
  (q₁ q₂ : Lean.Grind.Ring.OfSemiring.Q α), q₁ = q₂ → Lean.Grind.Ring.OfSemiring.rel✝ h q₁ q₂
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_alter_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] [Inhabited α] (h : t.WF) {k : α} {f : Option (β k) → Option (β k)}
  {hc : k ∈ (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl},
  (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl.getKey k hc = k
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Zero : Type → Type
-- Mathlib.Data.Set.Lattice
Set.iInter_inter : ∀ {β : Type u_2} {ι : Sort u_5} [Nonempty ι] (s : Set β) (t : ι → Set β), (⋂ i, t i) ∩ s = ⋂ i, t i ∩ s
-- Mathlib.Util.Notation3
/-- Keywording indicating whether to use a left- or right-fold.  -/
Mathlib.Notation3.foldKind : Lean.ParserDescr
-- Init.Data.List.Lemmas
List.singleton_eq_flatten_iff : ∀ {α : Type u_1} {xs : List (List α)} {y : α},
  [y] = xs.flatten ↔ ∃ as bs, xs = as ++ [y] :: bs ∧ (∀ l ∈ as, l = []) ∧ ∀ l ∈ bs, l = []
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
SubMulAction.ofStabilizer.conjMap_bijective : ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] {g : G} {a b : α} (hg : b = g • a),
  Function.Bijective ⇑(SubMulAction.ofStabilizer.conjMap hg)
-- Mathlib.CategoryTheory.Functor.Trifunctor
CategoryTheory.bifunctorComp₂₃Obj_obj_map : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_6} C₂₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
  (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) (X₁ : C₁) (X₂ : C₂) {X Y : C₃} (φ : X ⟶ Y),
  ((CategoryTheory.bifunctorComp₂₃Obj F G₂₃ X₁).obj X₂).map φ = (F.obj X₁).map ((G₂₃.obj X₂).map φ)
-- Init.GrindInstances.Ring.SInt
Lean.Grind.instCommRingInt8 : Lean.Grind.CommRing Int8
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
/-- `negAt s A` is also equal to the preimage of `A` by `negAt s`. This fact is used to simplify
some proofs.  -/
NumberField.mixedEmbedding.negAt_preimage : ∀ {K : Type u_1} [inst : Field K] (s : Set { w // w.IsReal }) (A : Set (NumberField.mixedEmbedding.mixedSpace K)),
  ⇑(NumberField.mixedEmbedding.negAt s) ⁻¹' A = ⇑(NumberField.mixedEmbedding.negAt s) '' A
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.instBEqExpr.beq : Lean.Grind.Linarith.Expr → Lean.Grind.Linarith.Expr → Bool
-- Mathlib.RingTheory.LocalProperties.Submodule
Submodule.eq_bot_of_isLocalized'_span : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s : Set R),
  Ideal.span s = ⊤ →
    ∀ (Rₚ : ↑s → Type u_4) [inst_3 : (r : ↑s) → CommSemiring (Rₚ r)] [inst_4 : (r : ↑s) → Algebra R (Rₚ r)]
      [inst_5 : ∀ (r : ↑s), IsLocalization.Away (↑r) (Rₚ r)] (Mₚ : ↑s → Type u_5)
      [inst_6 : (r : ↑s) → AddCommMonoid (Mₚ r)] [inst_7 : (r : ↑s) → Module R (Mₚ r)]
      [inst_8 : (r : ↑s) → Module (Rₚ r) (Mₚ r)] [inst_9 : ∀ (r : ↑s), IsScalarTower R (Rₚ r) (Mₚ r)]
      (f : (r : ↑s) → M →ₗ[R] Mₚ r) [inst_10 : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)] {N : Submodule R M},
      (∀ (r : ↑s), Submodule.localized' (Rₚ r) (Submonoid.powers ↑r) (f r) N = ⊥) → N = ⊥
-- Mathlib.LinearAlgebra.TensorProduct.Submodule
Submodule.lTensorOne_tmul : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {N : Submodule R S}
  (y : R) (n : ↥N), N.lTensorOne ((algebraMap R ↥⊥) y ⊗ₜ[R] n) = y • n
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
/-- By making an arbitrary choice of roots pairing to `-3`, we can obtain an embedded `𝔤₂` root
system just from the knowledge that such a pairs exists.  -/
RootPairing.IsG2.toEmbeddedG2 : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → (P : RootPairing ι R M N) → [P.IsG2] → P.EmbeddedG2
-- Mathlib.Algebra.Group.Defs
AddGroup.neg_add_cancel : ∀ {A : Type u} [self : AddGroup A] (a : A), -a + a = 0
-- Mathlib.Algebra.Category.Semigrp.Basic
_private.Mathlib.Algebra.Category.Semigrp.Basic.0.Semigrp.Hom.mk.injEq : ∀ {A B : Semigrp} (hom' hom'_1 : ↑A →ₙ* ↑B), ({ hom' := hom' } = { hom' := hom'_1 }) = (hom' = hom'_1)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey?_eq_none_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t.maxKey? = none ↔ t = ∅
-- Mathlib.NumberTheory.Primorial
primorial_monotone : Monotone primorial
-- Mathlib.Data.Sign.Defs
SignType.not_one_lt : ∀ (a : SignType), ¬1 < a
-- Mathlib.Data.Finsupp.Basic
Finsupp.mem_graph_iff : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {c : α × M} {f : α →₀ M}, c ∈ f.graph ↔ f c.1 = c.2 ∧ c.2 ≠ 0
-- Mathlib.Analysis.Calculus.FDeriv.Add
fderivWithin_const_smul_field' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_3} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {R : Type u_4} [inst_3 : DivisionSemiring R] [inst_4 : Module R F]
  [inst_5 : SMulCommClass 𝕜 R F] [inst_6 : ContinuousConstSMul R F] {s : Set 𝕜} {f : 𝕜 → F} {x : 𝕜} (c : R),
  fderivWithin 𝕜 (c • f) s x = c • fderivWithin 𝕜 f s x
-- Mathlib.Topology.Constructions
map_nhds_subtype_coe_eq_nhds : ∀ {X : Type u} [inst : TopologicalSpace X] {p : X → Prop} {x : X} (hx : p x),
  (∀ᶠ (x : X) in nhds x, p x) → Filter.map Subtype.val (nhds ⟨x, hx⟩) = nhds x
-- Mathlib.Order.Hom.CompleteLattice
CompleteLatticeHom.coe_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  [inst_2 : CompleteLattice γ] (f : CompleteLatticeHom β γ) (g : CompleteLatticeHom α β), ⇑(f.comp g) = ⇑f ∘ ⇑g
-- Mathlib.MeasureTheory.Function.L1Space.AEEqFun
/-- Computing the norm of a difference between two L¹-functions. Note that this is not a
special case of `ofReal_norm_eq_lintegral` since `(f - g) x` and `f x - g x` are not equal
(but only a.e.-equal).  -/
MeasureTheory.L1.ofReal_norm_sub_eq_lintegral : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  (f g : ↥(MeasureTheory.Lp β 1 μ)), ENNReal.ofReal ‖f - g‖ = ∫⁻ (x : α), ‖↑↑f x - ↑↑g x‖ₑ ∂μ
-- Mathlib.Topology.Category.TopCat.Monoidal
/-- The unit interval, as an object of `TopCat`.  -/
TopCat.I : TopCat
-- Mathlib.Data.QPF.Multivariate.Basic
MvQPF.liftP_iff : ∀ {n : ℕ} {F : TypeVec.{u} n → Type u_1} [q : MvQPF F] {α : TypeVec.{u} n} (p : ⦃i : Fin2 n⦄ → α i → Prop) (x : F α),
  MvFunctor.LiftP p x ↔ ∃ a f, x = MvQPF.abs ⟨a, f⟩ ∧ ∀ (i : Fin2 n) (j : (MvQPF.P F).B a i), p (f i j)
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.ClosedComplemented.exists_isClosed_isCompl : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p : Submodule R M} [T1Space ↥p], p.ClosedComplemented → ∃ q, IsClosed ↑q ∧ IsCompl p q
-- Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
MeasureTheory.MemLp.of_le_mul : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] {f : α → E} {g : α → F} {c : ℝ},
  MeasureTheory.MemLp g p μ →
    MeasureTheory.AEStronglyMeasurable f μ → (∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c * ‖g x‖) → MeasureTheory.MemLp f p μ
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.cospanExt_hom_app_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z X' Y' Z' : C} (iX : X ≅ X') (iY : Y ≅ Y') (iZ : Z ≅ Z')
  {f : X ⟶ Z} {g : Y ⟶ Z} {f' : X' ⟶ Z'} {g' : Y' ⟶ Z'}
  (wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iZ.hom)
  (wg : CategoryTheory.CategoryStruct.comp iY.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom),
  (CategoryTheory.Limits.cospanExt iX iY iZ wf wg).hom.app CategoryTheory.Limits.WalkingCospan.right = iY.hom
-- Lean.Meta.HaveTelescope
/-- The universe level for the `have` expression, cached.  -/
Lean.Meta.HaveTelescopeInfo.level : Lean.Meta.HaveTelescopeInfo → Lean.Level
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.lt_nfp_iff : ∀ {f : Ordinal.{u} → Ordinal.{u}} {a b : Ordinal.{u}}, a < Ordinal.nfp f b ↔ ∃ n, a < f^[n] b
-- Mathlib.Algebra.Group.Equiv.Basic
/-- There is a unique monoid homomorphism between two monoids with a unique element.  -/
MulEquiv.instUnique : {M : Type u_16} → {N : Type u_17} → [Unique M] → [Unique N] → [inst : Mul M] → [inst_1 : Mul N] → Unique (M ≃* N)
-- Mathlib.CategoryTheory.Sites.Monoidal
CategoryTheory.GrothendieckTopology.W.whiskerLeft : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₃}
  [inst_1 : CategoryTheory.Category.{v₃, u₃} A] [inst_2 : CategoryTheory.MonoidalCategory A]
  [inst_3 : CategoryTheory.MonoidalClosed A]
  [∀ (F₁ F₂ : CategoryTheory.Functor Cᵒᵖ A), CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom A F₁ F₂]
  [∀ (F₁ F₂ : CategoryTheory.Functor Cᵒᵖ A), CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom A F₁ F₂]
  {G₁ G₂ : CategoryTheory.Functor Cᵒᵖ A} {g : G₁ ⟶ G₂},
  J.W g → ∀ (F : CategoryTheory.Functor Cᵒᵖ A), J.W (CategoryTheory.MonoidalCategoryStruct.whiskerLeft F g)
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure
CategoryTheory.ObjectProperty.colimitsClosure_eq_unop_limitsClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {α : Type t}
  (J : α → Type u') [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)],
  P.colimitsClosure J = (P.op.limitsClosure fun a => (J a)ᵒᵖ).unop
-- Mathlib.Analysis.Calculus.FDeriv.Pi
hasFDerivAt_update : ∀ {𝕜 : Type u_1} {ι : Type u_2} [inst : DecidableEq ι] [inst_1 : NontriviallyNormedField 𝕜] {E : ι → Type u_3}
  [inst_2 : (i : ι) → NormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] (x : (i : ι) → E i) {i : ι}
  (y : E i), HasFDerivAt (Function.update x i) (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 (E i)))) y
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.coe_lineMap : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
  [inst_3 : AddTorsor V1 P1] (p₀ p₁ : P1), ⇑(AffineMap.lineMap p₀ p₁) = fun c => c • (p₁ -ᵥ p₀) +ᵥ p₀
-- Mathlib.Algebra.BigOperators.Group.Finset.Lemmas
/-- See also `Finset.sum_apply`, with the same conclusion but with the weaker hypothesis
`f : α → M → N`  -/
AddMonoidHom.finsetSum_apply : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : AddZeroClass M] [inst_1 : AddCommMonoid N] (f : ι → M →+ N)
  (s : Finset ι) (b : M), (∑ x ∈ s, f x) b = ∑ x ∈ s, (f x) b
-- Mathlib.Topology.Inseparable
SeparationQuotient.isOpenMap_mk : ∀ {X : Type u_1} [inst : TopologicalSpace X], IsOpenMap SeparationQuotient.mk