mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKeyD_eq_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {k fallback : α}, k ∈ m → m.getKeyD k fallback = k
-- Mathlib.Analysis.Analytic.IteratedFDeriv
/-- The `n`-th iterated derivative of an analytic function on a set is symmetric.  -/
ContDiffWithinAt.iteratedFDerivWithin_comp_perm : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {s : Set E} {x : E},
  ContDiffWithinAt 𝕜 ⊤ f s x →
    UniqueDiffOn 𝕜 s →
      x ∈ s →
        ∀ {n : ℕ} (v : Fin n → E) (σ : Equiv.Perm (Fin n)),
          (iteratedFDerivWithin 𝕜 n f s x) (v ∘ ⇑σ) = (iteratedFDerivWithin 𝕜 n f s x) v
-- Init.Data.Array.Lemmas
Array.size_filter_lt_size_iff_exists : ∀ {α : Type u_1} {xs : Array α} {p : α → Bool}, (Array.filter p xs).size < xs.size ↔ ∃ x ∈ xs, ¬p x = true
-- Mathlib.Order.Filter.EventuallyConst
Filter.EventuallyConst.neg : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {f : α → β} [inst : Neg β],
  Filter.EventuallyConst f l → Filter.EventuallyConst (-f) l
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivativeFinsupp_X : ∀ {R : Type u} [inst : Semiring R],
  Polynomial.derivativeFinsupp Polynomial.X = (fun₀ | 0 => Polynomial.X) + fun₀ | 1 => 1
-- Mathlib.Topology.Sheaves.Over
TopologicalSpace.Opens.sheafEquivOver_inverse_obj_obj_obj : ∀ {X : Type u} [inst : TopologicalSpace X] (U : TopologicalSpace.Opens X) {A : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} A] (X_1 : CategoryTheory.Sheaf (Opens.grothendieckTopology ↥U) A)
  (X_2 : (CategoryTheory.Over U)ᵒᵖ),
  (U.sheafEquivOver.inverse.obj X_1).obj.obj X_2 =
    X_1.obj.obj (Opposite.op (U.overEquivalence.functor.obj (Opposite.unop X_2)))
-- Mathlib.RingTheory.Flat.Tensor
/-- The `lTensor`-variant of `iff_rTensor_injective`.  -/
Module.Flat.iff_lTensor_injective : ∀ {R : Type u} {M : Type v} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Module.Flat R M ↔ ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(LinearMap.lTensor M (Submodule.subtype I))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.maxKey?_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.maxKey? = t₂.maxKey?
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mfderivWithin_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {E'' : Type u_8}
  [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace 𝕜 E''] {H'' : Type u_9} [inst_13 : TopologicalSpace H'']
  {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M'']
  {f : M → M'} (x : M) {s : Set M} {g : M' → M''} {u : Set M'},
  MDiffAt[u] g (f x) →
    MDiffAt[s] f x → s ⊆ f ⁻¹' u → UniqueMDiffAt[s] x → mfderiv[s] (g ∘ f) x = mfderiv[u] g (f x) ∘SL mfderiv[s] f x
-- Mathlib.CategoryTheory.ObjectProperty.Shift
CategoryTheory.ObjectProperty.instIsStableUnderShiftShiftClosure : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) {A : Type u_2}
  [inst_1 : AddMonoid A] [inst_2 : CategoryTheory.HasShift C A], (P.shiftClosure A).IsStableUnderShift A
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintLinkLocation.mk.sizeOf_spec : ∀ (module : Lean.Name) (range : Lean.Syntax.Range),
  sizeOf { module := module, range := range } = 1 + sizeOf module + sizeOf range
-- Mathlib.Data.Fintype.EquivFin
Fintype.one_lt_card : ∀ {α : Type u_1} [inst : Fintype α] [h : Nontrivial α], 1 < Fintype.card α
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback_obj_obj_iso_inv : ∀ {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) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X)
  (x : X),
  (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback F G X).obj S).obj
          x).iso.inv =
    S.iso.inv.app x
-- Std.Time.Date.Unit.Weekday
/-- Gets the next `Weekday`.
 -/
Std.Time.Weekday.next : Std.Time.Weekday → Std.Time.Weekday
-- Mathlib.MeasureTheory.MeasurableSpace.Instances
Empty.instMeasurableSpace : MeasurableSpace Empty
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapGrp_map_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] {X Y : CategoryTheory.Grp C} (f : X ⟶ Y),
  (F.mapGrp.map f).hom.hom = F.map f.hom.hom
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.degree_induce_support : ∀ {V : Type u_1} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] (v : ↑G.support),
  (SimpleGraph.induce G.support G).degree v = G.degree ↑v
-- Mathlib.Data.Set.NAry
Set.image_image2_antidistrib : ∀ {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} {f : α → β → γ}
  {s : Set α} {t : Set β} {g : γ → δ} {f' : β' → α' → δ} {g₁ : β → β'} {g₂ : α → α'},
  (∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)) → g '' Set.image2 f s t = Set.image2 f' (g₁ '' t) (g₂ '' s)
-- Mathlib.Algebra.Group.Basic
sub_add_cancel_left : ∀ {G : Type u_3} [inst : AddCommGroup G] (a b : G), a - (a + b) = -b
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.vsub_eq_empty : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] [inst_1 : DecidableEq α] {s t : Finset β}, s -ᵥ t = ∅ ↔ s = ∅ ∨ t = ∅
-- Mathlib.Combinatorics.Matroid.Minor.Order
Matroid.IsMinor.le : ∀ {α : Type u_1} {M N : Matroid α}, N ≤m M → N ≤ M
-- Batteries.Lean.NameMapAttribute
Lean.instInhabitedNameMapExtension : {α : Type} → Inhabited (Lean.NameMapExtension α)
-- Mathlib.CategoryTheory.Functor.Category
CategoryTheory.Iso.map_hom_inv_id_app_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {X Y : C} (e : X ≅ Y)
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (Z : D) {Z_1 : E} (h : (F.obj X).obj Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp ((F.map e.hom).app Z)
      (CategoryTheory.CategoryStruct.comp ((F.map e.inv).app Z) h) =
    h
-- Lean.Environment
Lean.ConstantKind.recursor : Lean.ConstantKind
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.setToL1_zero_left' : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_4 : CompleteSpace F] {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C),
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = 0) →
    ∀ (f : ↥(MeasureTheory.Lp E 1 μ)), (MeasureTheory.L1.setToL1 hT) f = 0
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- Given a pair of maps into the summands of a binary biproduct,
we obtain a map into the binary biproduct.  -/
CategoryTheory.Limits.biprod.lift : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {W X Y : C} → [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] → (W ⟶ X) → (W ⟶ Y) → (W ⟶ X ⊞ Y)
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.stalkMap_congr_hom : ∀ {X Y : AlgebraicGeometry.Scheme} (f g : X ⟶ Y) (hfg : f = g) (x : ↥X),
  AlgebraicGeometry.Scheme.Hom.stalkMap f x =
    CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkCongr ⋯).hom (AlgebraicGeometry.Scheme.Hom.stalkMap g x)
-- Lean.Meta.Tactic.Grind.Extension
/-- Types that `grind` will case-split on.  -/
Lean.Meta.Grind.CasesTypes : Type
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.compare_get_self : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α} (h' : k ∈ t),
  cmp (t.get k h') k = Ordering.eq
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.swapRight_zero : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ}, ProbabilityTheory.Kernel.swapRight 0 = 0
-- Init.Data.Order.MinMaxOn
apply_minOn_le_left : ∀ {β : Type u_1} {α : Sort u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {x y : α},
  f (minOn f x y) ≤ f x
-- Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
/-- A `CompStruct f g h` is a witness for the fact that the morphisms represented by
`f` and `g` compose to the morphism represented by `h`.
 -/
SSet.Truncated.Edge.CompStruct.homotopyCategory₂_fac : ∀ {A : SSet.Truncated 2} [inst : A.Quasicategory₂]
  {x y z : A.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Quasicategory₂._proof_1 })}
  {f : SSet.Truncated.Edge x y} {g : SSet.Truncated.Edge y z} {h : SSet.Truncated.Edge x z} (s : f.CompStruct g h),
  CategoryTheory.CategoryStruct.comp (SSet.Truncated.HomotopyCategory₂.homMk f)
      (SSet.Truncated.HomotopyCategory₂.homMk g) =
    SSet.Truncated.HomotopyCategory₂.homMk h
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.liftCycles_homologyπ_eq_zero_of_boundary : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι} [inst_2 : K.HasHomology i] {A : C}
  (k : A ⟶ K.X i) (j : ι) (hj : c.next i = j) {i' : ι} (x : A ⟶ K.X i')
  (hx : k = CategoryTheory.CategoryStruct.comp x (K.d i' i)),
  CategoryTheory.CategoryStruct.comp (K.liftCycles k j hj ⋯) (K.homologyπ i) = 0
-- Mathlib.Data.Int.ModEq
Int.ModEq.mul_left_cancel_iff' : ∀ {m a b c : ℤ}, c ≠ 0 → (c * a ≡ c * b [ZMOD c * m] ↔ a ≡ b [ZMOD m])
-- Mathlib.Analysis.Convex.Side
AffineSubspace.SOppSide.trans_wOppSide : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y z : P}, s.SOppSide x y → s.WOppSide y z → s.WSameSide x z
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.domRestrict_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] {f : E →ₛₗ.[σ] F}
  {S_1 : Submodule R E} ⦃x : ↥(S_1 ⊓ f.domain)⦄ ⦃y : ↥f.domain⦄, ↑x = ↑y → ↑(f.domRestrict S_1) x = ↑f y
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.State : Type
-- Mathlib.Geometry.RingedSpace.OpenImmersion
/-- The universal property of open immersions:
For an open immersion `f : X ⟶ Z`, given any morphism of schemes `g : Y ⟶ Z` whose topological
image is contained in the image of `f`, we can lift this morphism to a unique `Y ⟶ X` that
commutes with these maps.
 -/
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift : {X Y Z : AlgebraicGeometry.LocallyRingedSpace} →
  (f : X ⟶ Z) →
    (g : Y ⟶ Z) →
      [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f] →
        Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base) ⊆
            Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base) →
          (Y ⟶ X)
-- Init.Data.List.Attach
List.attachWith_map_subtype_val : ∀ {α : Type u_1} {p : α → Prop} {l : List α} (H : ∀ a ∈ l, p a), List.map Subtype.val (l.attachWith p H) = l
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
Submodule.localized'_eq_span : ∀ {R : Type u_1} (S : Type u_2) {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Algebra R S] [inst_7 : Module S N] [inst_8 : IsScalarTower R S N] (p : Submonoid R)
  [inst_9 : IsLocalization p S] (f : M →ₗ[R] N) [inst_10 : IsLocalizedModule p f] (M' : Submodule R M),
  Submodule.localized' S p f M' = Submodule.span S (⇑f '' ↑M')
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.coeff_C : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : DecidableEq σ] (n : σ →₀ ℕ) (a : R),
  (MvPowerSeries.coeff n) (MvPowerSeries.C a) = if n = 0 then a else 0
-- Mathlib.AlgebraicGeometry.OrderOfVanishing
AlgebraicGeometry.Scheme.ord.congr_simp : ∀ {X : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsIntegral X]
  [inst_1 : AlgebraicGeometry.IsLocallyNoetherian X] (f f_1 : ↑X.functionField),
  f = f_1 → ∀ (z z_1 : ↥X), z = z_1 → AlgebraicGeometry.Scheme.ord f z = AlgebraicGeometry.Scheme.ord f_1 z_1
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.contains_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k a : α} {v : β k}, (t.insertIfNew k v).contains a = (cmp k a == Ordering.eq || t.contains a)
-- Mathlib.Analysis.Calculus.FDeriv.Congr
hasFDerivWithinAt_congr_set : ∀ {𝕜 : 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 → F} {f' : E →L[𝕜] F} {x : E} {s t : Set E},
  s =ᶠ[nhds x] t → (HasFDerivWithinAt f f' s x ↔ HasFDerivWithinAt f f' t x)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂Iso.of : Mathlib.Tactic.BicategoryLike.AtomIso → Mathlib.Tactic.BicategoryLike.Mor₂Iso
-- Mathlib.Order.SupClosed
infClosure_isClosed : ∀ {α : Type u_3} [inst : SemilatticeInf α] (s : Set α), infClosure.IsClosed s = InfClosed s
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.cons_vecMul : ∀ {α : Type u} {n : ℕ} {o' : Type uₒ} [inst : NonUnitalNonAssocSemiring α] (x : α) (v : Fin n → α)
  (B : Fin n.succ → o' → α),
  Matrix.vecMul (Matrix.vecCons x v) (Matrix.of B) =
    x • Matrix.vecHead B + Matrix.vecMul v (Matrix.of (Matrix.vecTail B))
-- Mathlib.Algebra.Colimit.Ring
/-- The universal property of the direct limit: maps from the components to another ring
that respect the directed system structure (i.e. make some diagram commute) give rise
to a unique map out of the direct limit.
 -/
Ring.DirectLimit.lift : {ι : Type u_1} →
  [inst : Preorder ι] →
    (G : ι → Type u_2) →
      [inst_1 : (i : ι) → CommRing (G i)] →
        (f : (i j : ι) → i ≤ j → G i → G j) →
          (P : Type u_3) →
            [inst_2 : CommRing P] →
              (g : (i : ι) → G i →+* P) →
                (∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x) → Ring.DirectLimit G f →+* P
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.equiv_iff_toList_perm : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp},
  t₁.Equiv t₂ ↔ t₁.toList.Perm t₂.toList
-- Init.Data.Vector.Erase
Vector.set_eraseIdx_le : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} {w : i < n} {j : ℕ} {a : α},
  i ≤ j → ∀ (hj : j < n - 1), (xs.eraseIdx i w).set j a hj = (xs.set (j + 1) a ⋯).eraseIdx i w
-- Mathlib.Analysis.SumIntegralComparisons
/-- The sum of a nonnegative, antitone function is bounded below by its integral.  -/
AntitoneOn.integral_le_tsum_comp_add : ∀ {f : ℝ → ℝ} (N : ℕ),
  AntitoneOn f (Set.Ici ↑N) →
    (Summable fun n => f ↑n) → (∀ t ∈ Set.Ioi ↑N, 0 ≤ f t) → ∫ (x : ℝ) in Set.Ioi ↑N, f x ≤ ∑' (n : ℕ), f ↑(n + N)
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.val_neg : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (f : AdicCompletion I M), ↑(-f) = -↑f
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.isoProd.eq_1 : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (X Y : C) [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  CategoryTheory.Limits.biprod.isoProd X Y =
    (CategoryTheory.Limits.BinaryBiproduct.isLimit X Y).conePointUniqueUpToIso
      (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Limits.pair X Y))
-- Mathlib.MeasureTheory.Function.EssSup
ENNReal.essSup_mul_le : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f g : α → ENNReal),
  essSup (f * g) μ ≤ essSup f μ * essSup g μ
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the smallest key that is greater than or equal to the
given key, returning `fallback` if no such key exists.
 -/
Std.ExtDTreeMap.getKeyGED : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtDTreeMap α β cmp → α → α → α
-- Mathlib.Algebra.Homology.Homotopy
HomologicalComplex.instHasTwoOutOfThreePropertyHomotopyEquivalences : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι}, (HomologicalComplex.homotopyEquivalences V c).HasTwoOutOfThreeProperty
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
IsPrimitiveRoot.subOneIntegralPowerBasisOfPrimePow_gen_prime : ∀ {p k : ℕ} {K : Type u} [inst : Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [inst_1 : CharZero K]
  [inst_2 : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))),
  Prime hζ.subOneIntegralPowerBasisOfPrimePow.gen
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.sub_int_mul_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [inst : NonAssocRing α],
  Function.Periodic f c → ∀ (n : ℤ), f (x - ↑n * c) = f x
-- Mathlib.Algebra.Lie.Free
_private.Mathlib.Algebra.Lie.Free.0.termLib : Lean.ParserDescr
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- Three points are collinear if and only if the first or third point equals the second or the
angle between them is 0 or π.  -/
EuclideanGeometry.collinear_iff_eq_or_eq_or_angle_eq_zero_or_angle_eq_pi : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P},
  Collinear ℝ {p₁, p₂, p₃} ↔
    p₁ = p₂ ∨ p₃ = p₂ ∨ EuclideanGeometry.angle p₁ p₂ p₃ = 0 ∨ EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi
-- Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Ideal.height_le_height_add_one_of_mem : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] {r : R} {p : Ideal R} [p.IsPrime],
  r ∈ p → p.height ≤ (Ideal.map (Ideal.Quotient.mk (Ideal.span {r})) p).height + 1
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.mk' : {ι : Type u} →
  {β : ι → Type v} →
    [inst : (i : ι) → Zero (β i)] → (toFun : (i : ι) → β i) → Trunc { s // ∀ (i : ι), i ∈ s ∨ toFun i = 0 } → DFinsupp β
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
MvPolynomial.weightedHomogeneousComponent_C_mul : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] {w : σ → M}
  (φ : MvPolynomial σ R) (n : M) (r : R),
  (MvPolynomial.weightedHomogeneousComponent w n) (MvPolynomial.C r * φ) =
    MvPolynomial.C r * (MvPolynomial.weightedHomogeneousComponent w n) φ
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- The algebra homomorphism of monoid algebras induced by a homomorphism of the base algebras.  -/
MonoidAlgebra.mapAlgHom : {R : Type u_1} →
  {A : Type u_4} →
    {B : Type u_5} →
      (M : Type u_7) →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Semiring B] →
              [inst_3 : Algebra R A] →
                [inst_4 : Algebra R B] → [inst_5 : Monoid M] → (A →ₐ[R] B) → MonoidAlgebra A M →ₐ[R] MonoidAlgebra B M
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.eq_symm_apply : ∀ {𝕜 : 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₂) {x : P₂} {y : P},
  y = e.symm x ↔ e y = x
-- Mathlib.Algebra.Polynomial.Eval.Coeff
Polynomial.eval_zero_map : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (p : Polynomial R),
  Polynomial.eval 0 (Polynomial.map f p) = f (Polynomial.eval 0 p)
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.colimitsOfShape_colimMap : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {J : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] {X Y : CategoryTheory.Functor J C} (f : X ⟶ Y)
  [inst_2 : CategoryTheory.Limits.HasColimit X] [inst_3 : CategoryTheory.Limits.HasColimit Y],
  W.functorCategory J f → W.colimitsOfShape J (CategoryTheory.Limits.colimMap f)
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.domDomCongr.eq_1 : ∀ {R : Type uR} {M₂ : Type v₂} {M₃ : Type v₃} [inst : Semiring R] [inst_1 : AddCommMonoid M₂]
  [inst_2 : AddCommMonoid M₃] [inst_3 : Module R M₂] [inst_4 : Module R M₃] {ι₁ : Type u_1} {ι₂ : Type u_2}
  (σ : ι₁ ≃ ι₂) (m : MultilinearMap R (fun x => M₂) M₃),
  MultilinearMap.domDomCongr σ m = { toFun := fun v => m fun i => v (σ i), map_update_add' := ⋯, map_update_smul' := ⋯ }
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.relabelAux_sumInl : ∀ {α : Type u'} {n : ℕ} (k : ℕ), FirstOrder.Language.BoundedFormula.relabelAux Sum.inl k = Sum.map id (Fin.natAdd n)
-- Mathlib.Algebra.Module.Submodule.Lattice
/-- An additive subgroup is equivalent to a ℤ-submodule.  -/
AddSubgroup.toIntSubmodule : {M : Type u_3} → [inst : AddCommGroup M] → AddSubgroup M ≃o Submodule ℤ M
-- Mathlib.GroupTheory.OrderOfElement
RightCancelMonoid.groupOfFinite.eq_1 : ∀ {H : Type u_6} [inst : RightCancelMonoid H] [inst_1 : Finite H],
  RightCancelMonoid.groupOfFinite = (MulEquiv.opOp H).group
-- Mathlib.Order.Interval.Set.WithBotTop
WithBot.Ioo_coe : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ioo ↑b ↑a = WithBot.some '' Set.Ioo b a
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- The product of a strictly antitone function and an antitone function is strictly antitone.  -/
StrictAntiOn.mul_antitone' : ∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α} {s : Set β}
  [MulLeftMono α] [MulRightStrictMono α], StrictAntiOn f s → AntitoneOn g s → StrictAntiOn (fun x => f x * g x) s
-- Mathlib.GroupTheory.Congruence.Defs
/-- Defining the quotient by a congruence relation of a type with a multiplication.  -/
Con.Quotient : {M : Type u_1} → [inst : Mul M] → Con M → Type u_1
-- Mathlib.Algebra.GroupWithZero.WithZero
MonoidWithZeroHom.one_apply_val_unit : ∀ {M₀ : Type u_1} {N₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : MulZeroOneClass N₀]
  [inst_2 : DecidablePred fun x => x = 0] [inst_3 : Nontrivial M₀] [inst_4 : NoZeroDivisors M₀] (x : M₀ˣ), 1 ↑x = 1
-- Mathlib.Tactic.TacticAnalysis
/-- Determines which (sequences of) tactics to analyze.

`context` is `some ctx` whenever the previous trigger returned `continue ctx`,
`none` at the start of a tactic sequence or after a `skip`/`accept`.

If the last returned value is `continue` at the end of the sequence, the framework inserts an
extra `done` to run the `trigger` on.
 -/
Mathlib.TacticAnalysis.ComplexConfig.trigger : (self : Mathlib.TacticAnalysis.ComplexConfig) →
  Option self.ctx → Lean.Syntax → Mathlib.TacticAnalysis.TriggerCondition self.ctx