mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂.coherenceComp.injEq : ∀ (e : Lean.Expr) (isoLift? : Option Mathlib.Tactic.BicategoryLike.IsoLift)
  (f g h i : Mathlib.Tactic.BicategoryLike.Mor₁) (α : Mathlib.Tactic.BicategoryLike.CoherenceHom)
  (η θ : Mathlib.Tactic.BicategoryLike.Mor₂) (e_1 : Lean.Expr)
  (isoLift?_1 : Option Mathlib.Tactic.BicategoryLike.IsoLift) (f_1 g_1 h_1 i_1 : Mathlib.Tactic.BicategoryLike.Mor₁)
  (α_1 : Mathlib.Tactic.BicategoryLike.CoherenceHom) (η_1 θ_1 : Mathlib.Tactic.BicategoryLike.Mor₂),
  (Mathlib.Tactic.BicategoryLike.Mor₂.coherenceComp e isoLift? f g h i α η θ =
      Mathlib.Tactic.BicategoryLike.Mor₂.coherenceComp e_1 isoLift?_1 f_1 g_1 h_1 i_1 α_1 η_1 θ_1) =
    (e = e_1 ∧ isoLift? = isoLift?_1 ∧ f = f_1 ∧ g = g_1 ∧ h = h_1 ∧ i = i_1 ∧ α = α_1 ∧ η = η_1 ∧ θ = θ_1)
-- Mathlib.Algebra.Group.Units.Defs
/-- See Note [custom simps projection]  -/
Units.Simps.val_inv : {α : Type u} → [inst : Monoid α] → αˣ → α
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.withPosition.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Data.Finset.Grade
CovBy.exists_finset_cons : ∀ {α : Type u_1} {s t : Finset α}, s ⋖ t → ∃ a, ∃ (ha : a ∉ s), Finset.cons a s ha = t
-- Mathlib.Order.Hom.CompleteLattice
/-- Copy of a `FrameHom` with a new `toFun` equal to the old one. Useful to fix definitional
equalities.  -/
FrameHom.copy : {α : Type u_2} →
  {β : Type u_3} →
    [inst : CompleteLattice α] →
      [inst_1 : CompleteLattice β] → (f : FrameHom α β) → (f' : α → β) → f' = ⇑f → FrameHom α β
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F.leftOp : Cᵒᵖ ⥤ D` creates limits of `K.op : Jᵒᵖ ⥤ Cᵒᵖ`, then `F : C ⥤ Dᵒᵖ` creates
colimits of `K : J ⥤ C`.  -/
CategoryTheory.Limits.createsColimitOfLeftOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            (K : CategoryTheory.Functor J C) →
              (F : CategoryTheory.Functor C Dᵒᵖ) →
                [CategoryTheory.CreatesLimit K.op F.leftOp] → CategoryTheory.CreatesColimit K F
-- Mathlib.CategoryTheory.Products.Associator
CategoryTheory.prod.associator_map : ∀ (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 x_1 : (C × D) × E) (f : x ⟶ x_1),
  (CategoryTheory.prod.associator C D E).map f = CategoryTheory.Prod.mkHom f.1.1 (CategoryTheory.Prod.mkHom f.1.2 f.2)
-- Mathlib.FieldTheory.PurelyInseparable.Tower
/-- If `E / F` is a purely inseparable field extension, `f` is a separable irreducible polynomial
over `F`, then it is also irreducible over `E`.  -/
Polynomial.Separable.map_irreducible_of_isPurelyInseparable : ∀ {F : Type u} (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {f : Polynomial F},
  f.Separable → Irreducible f → ∀ [IsPurelyInseparable F E], Irreducible (Polynomial.map (algebraMap F E) f)
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
mulRothNumber_empty : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Monoid α], mulRothNumber ∅ = 0
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.toProd_comp_inr : ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N],
  Monoid.Coprod.toProd.comp Monoid.Coprod.inr = MonoidHom.inr M N
-- Lean.Elab.Tactic.Config
Lean.Elab.Tactic.ConfigItemView.mk : Lean.Syntax → Lean.Ident → Lean.Term → Bool → Lean.Elab.Tactic.ConfigItemView
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.prod_comp : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : AddCommMonoid U] [inst_5 : Module A V]
  [inst_6 : Module A W] [inst_7 : Module A U] {ρ : Representation A G V} {σ : Representation A G W}
  {τ : Representation A G U} (X : Type u_6) [inst_8 : AddCommMonoid X] [inst_9 : Module A X] {π : Representation A G X}
  (f : ρ.IntertwiningMap σ) (g₁ : σ.IntertwiningMap τ) (g₂ : σ.IntertwiningMap π),
  (g₁.prod g₂).comp f = (g₁.comp f).prod (g₂.comp f)
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.mem_pair : ∀ {x y z : ZFSet.{u}}, x ∈ {y, z} ↔ x = y ∨ x = z
-- Mathlib.Order.Filter.AtTopBot.Field
/-- If a function tends to negative infinity along a filter,
then `f` multiplied by a negative constant (on the right) tends to positive infinity.  -/
Filter.Tendsto.atBot_mul_const_of_neg : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {l : Filter β}
  {f : β → α} {r : α}, r < 0 → Filter.Tendsto f l Filter.atBot → Filter.Tendsto (fun x => f x * r) l Filter.atTop
-- Mathlib.Topology.Algebra.Nonarchimedean.Bases
/-- The topology associated to a basis of submodules in a module.  -/
SubmodulesBasis.topology : {ι : Type u_1} →
  {R : Type u_2} →
    [inst : CommRing R] →
      {M : Type u_4} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            [inst_3 : TopologicalSpace R] →
              [Nonempty ι] → {B : ι → Submodule R M} → SubmodulesBasis B → TopologicalSpace M
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure
CategoryTheory.ObjectProperty.le_colimitsClosure : ∀ {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 ≤ P.colimitsClosure J
-- Mathlib.CategoryTheory.Filtered.Small
_private.Mathlib.CategoryTheory.Filtered.Small.0.CategoryTheory.IsFiltered.FilteredClosureSmall.bundledAbstractFilteredClosure.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.AndKind.noConfusionType : Sort v✝ → Mathlib.Tactic.ITauto.AndKind → Mathlib.Tactic.ITauto.AndKind → Sort v✝
-- Init.Data.String.Lemmas.Iterate
String.toList_revPositions : ∀ {s : String}, s.revPositions.toList = String.Model.revPositionsFrom s.endPos
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
LinearIndependent.eq_of_pair : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {x y : M},
  LinearIndependent R ![x, y] → ∀ {s t s' t' : R}, s • x + t • y = s' • x + t' • y → s = s' ∧ t = t'
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.mk.sizeOf_spec : ∀ {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} [inst_3 : SizeOf A] [inst_4 : SizeOf B]
  [inst_5 : SizeOf C] (fst : A) (snd : C) (iso : F.obj fst ≅ G.obj snd),
  sizeOf { fst := fst, snd := snd, iso := iso } = 1 + sizeOf fst + sizeOf snd + sizeOf iso
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
/-- All functors `F : J ⥤ C` from `J` have weak limits  -/
CategoryTheory.Limits.HasWeakLimitsOfShape.hasWeakLimit : ∀ {J : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} J} {C : Type u_3}
  {inst_1 : CategoryTheory.Category.{v_3, u_3} C} [self : CategoryTheory.Limits.HasWeakLimitsOfShape J C]
  (F : CategoryTheory.Functor J C), CategoryTheory.Limits.HasWeakLimit F
-- Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs
SimpleGraph.instIsProbabilityMeasureBinomialRandom : ∀ {V : Type u_1} {p : ↑unitInterval} [Countable V], MeasureTheory.IsProbabilityMeasure (SimpleGraph.binomialRandom V p)
-- Mathlib.Algebra.Group.Basic
neg_eq_iff_add_eq_zero : ∀ {G : Type u_3} [inst : AddGroup G] {a b : G}, -a = b ↔ a + b = 0
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.mk.sizeOf_spec : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [inst_3 : SizeOf R]
  [inst_4 : SizeOf S] (Ring : Type w) [commRing : CommRing Ring] [algebra₁ : Algebra R Ring] [algebra₂ : Algebra Ring S]
  [isScalarTower : IsScalarTower R Ring S] (σ : S → Ring) (algebraMap_σ : ∀ (x : S), (algebraMap Ring S) (σ x) = x),
  sizeOf
      { Ring := Ring, commRing := commRing, algebra₁ := algebra₁, algebra₂ := algebra₂, isScalarTower := isScalarTower,
        σ := σ, algebraMap_σ := algebraMap_σ } =
    1 + sizeOf Ring + sizeOf commRing + sizeOf algebra₁ + sizeOf algebra₂ + sizeOf isScalarTower
-- Mathlib.Algebra.Group.Hom.Defs
AddHom.funLike.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N],
  AddHom.funLike = { coe := AddHom.toFun, coe_injective := ⋯ }
-- Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Module.rankAtStalk.eq_1 : ∀ {R : Type uR} (M : Type uM) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : PrimeSpectrum R),
  Module.rankAtStalk M p = Module.finrank (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl M)
-- Mathlib.CategoryTheory.Shift.ShiftSequence
CategoryTheory.Functor.instPreservesZeroMorphismsShift : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A) {M : Type u_4} [inst_2 : AddMonoid M]
  [inst_3 : CategoryTheory.HasShift C M] [inst_4 : F.ShiftSequence M]
  [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_6 : CategoryTheory.Limits.HasZeroMorphisms A]
  [F.PreservesZeroMorphisms] [∀ (n : M), (CategoryTheory.shiftFunctor C n).PreservesZeroMorphisms] (n : M),
  (F.shift n).PreservesZeroMorphisms
-- Mathlib.NumberTheory.Multiplicity
emultiplicity_pow_prime_sub_pow_prime : ∀ {R : Type u_1} [inst : CommRing R] {x y : R} {p : ℕ} [IsDomain R],
  Prime ↑p → Odd p → ↑p ∣ x - y → ¬↑p ∣ x → emultiplicity (↑p) (x ^ p - y ^ p) = emultiplicity (↑p) (x - y) + 1
-- Mathlib.Topology.Separation.Basic
nhds_le_nhds_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {a b : X}, nhds a ≤ nhds b ↔ a = b
-- Init.Core
/-- If two terms are heterogeneously equal then their types are propositionally equal.  -/
type_eq_of_heq : ∀ {α β : Sort u} {a : α} {b : β}, a ≍ b → α = β
-- Mathlib.Order.Disjointed
partialSups_disjointed : ∀ {α : Type u_1} {ι : Type u_2} [inst : GeneralizedBooleanAlgebra α] [inst_1 : PartialOrder ι]
  [inst_2 : LocallyFiniteOrderBot ι] (f : ι → α), partialSups (disjointed f) = partialSups f
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.integral_comp_rpow_Ioi_of_pos : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {g : ℝ → E} {p : ℝ},
  0 < p → ∫ (x : ℝ) in Set.Ioi 0, (p * x ^ (p - 1)) • g (x ^ p) = ∫ (y : ℝ) in Set.Ioi 0, g y
-- Mathlib.Algebra.Star.Basic
starRingAut_apply : ∀ {R : Type u} [inst : CommSemiring R] [inst_1 : StarRing R] (a : R), starRingAut a = star a
-- Mathlib.Data.Ordmap.Ordnode
Ordnode.instEmptyCollection : {α : Type u_1} → EmptyCollection (Ordnode α)
-- Mathlib.Computability.Primrec.Basic
Nat.Primrec.casesOn1 : ∀ {f : ℕ → ℕ} (m : ℕ), Nat.Primrec f → Nat.Primrec fun x => Nat.casesOn x m f
-- Mathlib.Probability.Kernel.Disintegration.StandardBorel
/-- `condKernel κ` is a Markov kernel.  -/
ProbabilityTheory.Kernel.instIsMarkovKernelCondKernel : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] [inst_1 : Nonempty Ω]
  [h : MeasurableSpace.CountableOrCountablyGenerated α β] (κ : ProbabilityTheory.Kernel α (β × Ω))
  [inst_2 : ProbabilityTheory.IsFiniteKernel κ], ProbabilityTheory.IsMarkovKernel κ.condKernel
-- Mathlib.Analysis.Calculus.BumpFunction.Normed
ContDiffBump.contDiff_normed : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E]
  [inst_3 : MeasurableSpace E] {c : E} (f : ContDiffBump c) {μ : MeasureTheory.Measure E} {n : ℕ∞},
  ContDiff ℝ (↑n) (f.normed μ)
-- Mathlib.Data.Finset.Sum
Finset.sumEquiv_apply_fst : ∀ {α : Type u_4} {β : Type u_5} (s : Finset (α ⊕ β)), (Finset.sumEquiv s).1 = s.toLeft
-- Lean.Expr
_private.Lean.Expr.0.Lean.natMulFn : Lean.Expr
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.log_of_ne_zero : ∀ {x : ℝ} (hx : x ≠ 0), Real.log x = Real.expOrderIso.symm ⟨|x|, ⋯⟩
-- Mathlib.Logic.Lemmas
ite_dite_distrib_left : ∀ {α : Sort u_1} {p q : Prop} [inst : Decidable p] [inst_1 : Decidable q] {a : α} {b : q → α} {c : ¬q → α},
  (if p then a else dite q b c) = if hq : q then if p then a else b hq else if p then a else c hq
-- Mathlib.LinearAlgebra.CliffordAlgebra.Inversion
/-- Over a ring where `2` is invertible, `Q m` is invertible whenever `ι Q m`.  -/
CliffordAlgebra.invertibleOfInvertibleι : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          (Q : QuadraticForm R M) → [Invertible 2] → (m : M) → [Invertible ((CliffordAlgebra.ι Q) m)] → Invertible (Q m)
-- Mathlib.Tactic.Widget.StringDiagram
/-- The horizontal position of a node in a string diagram, counting strings in codomains.  -/
Mathlib.Tactic.Widget.StringDiagram.Node.hPosTar : Mathlib.Tactic.Widget.StringDiagram.Node → ℕ
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.hasCoproductsOfShape_of_hasBiproductsOfShape : ∀ {J : Type w} (C : Type uC) [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBiproductsOfShape J C],
  CategoryTheory.Limits.HasCoproductsOfShape J C
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.integrable_iff_cauchy : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
  {l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤}
  [CompleteSpace F],
  BoxIntegral.Integrable I l f vol ↔
    Cauchy (Filter.map (BoxIntegral.integralSum f vol) (BoxIntegral.IntegrationParams.toFilteriUnion I ⊤))
-- Mathlib.Algebra.Group.Units.Hom
AddMonoidHom.coe_toHomAddUnits : ∀ {G : Type u_1} {M : Type u_2} [inst : AddGroup G] [inst_1 : AddMonoid M] (f : G →+ M) (g : G),
  ↑(f.toHomAddUnits g) = f g
-- Mathlib.Topology.Algebra.Group.CompactOpen
/-- `ContinuousAddMonoidHom f _` is a functor.  -/
ContinuousAddMonoidHom.compRight : (A : Type u_2) →
  {E : Type u_6} →
    [inst : AddMonoid A] →
      [inst_1 : AddCommGroup E] →
        [inst_2 : TopologicalSpace A] →
          [inst_3 : TopologicalSpace E] →
            [inst_4 : IsTopologicalAddGroup E] →
              {B : Type u_7} →
                [inst_5 : AddCommGroup B] →
                  [inst_6 : TopologicalSpace B] → [inst_7 : IsTopologicalAddGroup B] → (B →ₜ+ E) → (A →ₜ+ B) →ₜ+ A →ₜ+ E
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.Presieve.functorPullback.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X : C} (R : CategoryTheory.Presieve (F.obj X)) (x : C) (f : x ⟶ X),
  CategoryTheory.Presieve.functorPullback F R f = R (F.map f)
-- Mathlib.Order.BoundedOrder.Monotone
Antitone.forall : ∀ {α : Type u} {β : Type v} [inst : Preorder α] {P : β → α → Prop},
  (∀ (x : β), Antitone (P x)) → Antitone fun y => ∀ (x : β), P x y
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
quasispectrum_eq_spectrum_union : ∀ (R : Type u_3) {A : Type u_4} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] (a : A),
  quasispectrum R a = spectrum R a ∪ {r | ¬IsUnit r}
-- Mathlib.FieldTheory.IsSepClosed
IsSepClosed.exists_aeval_eq_zero : ∀ (K : Type v) [inst : Field K] {k : Type u_1} [inst_1 : CommSemiring k] [IsSepClosed K] [inst_3 : Algebra k K]
  [FaithfulSMul k K] (p : Polynomial k), p.degree ≠ 0 → p.Separable → ∃ x, (Polynomial.aeval x) p = 0
-- Mathlib.Topology.Order.LowerUpperTopology
/-- The complements of the lower closures of finite sets are a collection of upper sets
which form a basis for the upper topology.  -/
Topology.IsUpper.upperBasis : (α : Type u_3) → [Preorder α] → Set (Set α)
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iUnion_smul_left_image : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {s : Set α} {t : Set β}, ⋃ a ∈ s, a • t = s • t
-- Lean.Meta.TryThis
Lean.Meta.Tactic.TryThis.TryThisInfo.mk : Lean.Lsp.TextEdit → String → Lean.Meta.Tactic.TryThis.Suggestion → Lean.Meta.Tactic.TryThis.TryThisInfo
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_diff_of_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₂ → Std.DHashMap.Raw.Const.get? (m₁.diff m₂) k = none
-- Std.Time.Time.Unit.Millisecond
Std.Time.Millisecond.instDecidableLtOrdinal : {x y : Std.Time.Millisecond.Ordinal} → Decidable (x < y)
-- Mathlib.Algebra.Group.ForwardDiff
fwdDiff_iter_add : ∀ {M : Type u_1} {G : Type u_2} [inst : AddCommMonoid M] [inst_1 : AddCommGroup G] (h : M) (f g : M → G) (n : ℕ),
  (fwdDiff h)^[n] (f + g) = (fwdDiff h)^[n] f + (fwdDiff h)^[n] g
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToCodeBlock.Catch.mk.injEq : ∀ (x optType : Lean.Syntax) (codeBlock : Lean.Elab.Term.Do.CodeBlock) (x_1 optType_1 : Lean.Syntax)
  (codeBlock_1 : Lean.Elab.Term.Do.CodeBlock),
  ({ x := x, optType := optType, codeBlock := codeBlock } =
      { x := x_1, optType := optType_1, codeBlock := codeBlock_1 }) =
    (x = x_1 ∧ optType = optType_1 ∧ codeBlock = codeBlock_1)
-- Mathlib.Analysis.Fourier.Notation
FourierInvPair.fourier_fourierInv_eq : ∀ {E : Type u_5} {F : Type u_6} {inst : FourierTransform F E} {inst_1 : FourierTransformInv E F}
  [self : FourierInvPair E F] (f : E), FourierTransform.fourier (FourierTransformInv.fourierInv f) = f
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
measurableSet_Iic : ∀ {α : Type u_1} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [inst_2 : Preorder α]
  {a : α} [ClosedIicTopology α], MeasurableSet (Set.Iic a)
-- Std.Data.DTreeMap.Raw.Basic
Std.DTreeMap.Raw.instLawfulSingletonSigma : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}, LawfulSingleton ((a : α) × β a) (Std.DTreeMap.Raw α β cmp)
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.Karoubi.zsmul_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {P Q : CategoryTheory.Idempotents.Karoubi C} (n : ℤ) (f : P ⟶ Q), (n • f).f = n • f.f
-- Lean.ReducibilityAttrs
Lean.ReducibilityStatus.instanceReducible : Lean.ReducibilityStatus
-- Init.Data.String.Lemmas.FindPos
String.Slice.offset_posGE_eq_self_iff : ∀ {s : String.Slice} {p : String.Pos.Raw} {h : p ≤ s.rawEndPos},
  (s.posGE p h).offset = p ↔ String.Pos.Raw.IsValidForSlice s p
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.pi_Ioo_ae_eq_pi_Icc : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  {μ : (i : ι) → MeasureTheory.Measure (α i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)]
  [inst_3 : (i : ι) → PartialOrder (α i)] [∀ (i : ι), MeasureTheory.NullSingletonClass (μ i)] {s : Set ι}
  {f g : (i : ι) → α i},
  (s.pi fun i => Set.Ioo (f i) (g i)) =ᵐ[MeasureTheory.Measure.pi μ] s.pi fun i => Set.Icc (f i) (g i)
-- Mathlib.Geometry.Euclidean.MongePoint
/-- The Monge point of an (n+2)-simplex, in terms of
`pointsWithCircumcenter`.  -/
Affine.Simplex.mongePoint_eq_affineCombination_of_pointsWithCircumcenter : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P (n + 2)),
  s.mongePoint =
    (Finset.affineCombination ℝ Finset.univ s.pointsWithCircumcenter)
      (Affine.Simplex.mongePointWeightsWithCircumcenter n)
-- Mathlib.Data.List.Nodup
List.Nodup.of_map : ∀ {α : Type u} {β : Type v} (f : α → β) {l : List α}, (List.map f l).Nodup → l.Nodup
-- Lean.Server.Completion.SyntheticCompletion
_private.Lean.Server.Completion.SyntheticCompletion.0.Lean.Server.Completion.findSyntheticIdentifierCompletion? : String.Pos.Raw → Lean.Elab.InfoTree → Option Lean.Server.Completion.ContextualizedCompletionInfo
-- Mathlib.GroupTheory.HNNExtension
/-- The equivalence between elements of the HNN extension and words in normal form.  -/
HNNExtension.NormalWord.equiv : {G : Type u_1} →
  [inst : Group G] →
    {A B : Subgroup G} →
      (φ : ↥A ≃* ↥B) →
        (d : HNNExtension.NormalWord.TransversalPair G A B) → HNNExtension G A B φ ≃ HNNExtension.NormalWord d
-- Mathlib.Data.Set.Image
Set.disjoint_image_right : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} {t : Set β}, Disjoint t (f '' s) ↔ Disjoint (f ⁻¹' t) s
-- Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
NNReal.dist_agmSequences_fst_snd : ∀ {x y : NNReal} (n : ℕ), dist (x.agmSequences y n).1 (x.agmSequences y n).2 ≤ dist x y / 2 ^ (n + 1)
-- Mathlib.Topology.VectorBundle.Basic
/-- The base space of a vector bundle core, as a convenience function for dot notation  -/
VectorBundleCore.Base : {B : Type u_2} → Type u_2
-- Mathlib.Data.Nat.Choose.Factorization
Nat.factorization_choose_of_lt_three_mul : ∀ {p n k : ℕ}, p ≠ 2 → p ≤ k → p ≤ n - k → n < 3 * p → (n.choose k).factorization p = 0
-- Mathlib.Algebra.GCDMonoid.Basic
nonempty_strongNormalizedGCDMonoid_iff : ∀ {α : Type u_2} [inst : CommMonoidWithZero α],
  Nonempty (StrongNormalizedGCDMonoid α) ↔ IsGCDMonoid α ∧ Nonempty (StrongNormalizationMonoid α)
-- Mathlib.Algebra.Ring.Commute
sq_sub_sq : ∀ {R : Type u} [inst : CommRing R] (a b : R), a ^ 2 - b ^ 2 = (a + b) * (a - b)
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.vecMul_surjective_iff_exists_left_inverse : ∀ {m : Type u} {n : Type u'} {R : Type u_2} [inst : Semiring R] [inst_1 : DecidableEq n] [inst_2 : Fintype m] [Finite n]
  {A : Matrix m n R}, (Function.Surjective fun v => Matrix.vecMul v A) ↔ ∃ B, B * A = 1
-- Init.Data.Option.Lemmas
Option.join_pfilter : ∀ {α : Type u_1} {o : Option (Option α)} {p : (o' : Option α) → o = some o' → Bool},
  (o.pfilter p).join = o.pbind fun o' ho' => if p o' ho' = true then o' else none
-- Mathlib.Order.Bounds.Image
isGLB_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {s : Set (α × β)} {p : α × β},
  IsGLB s p ↔ IsGLB (Prod.fst '' s) p.1 ∧ IsGLB (Prod.snd '' s) p.2
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.ofIsEmpty_onFunction : ∀ (L : FirstOrder.Language) (L' : FirstOrder.Language) [inst : L.IsAlgebraic] [inst_1 : L.IsRelational] {n : ℕ}
  (a : L.Functions n), (FirstOrder.Language.LHom.ofIsEmpty L L').onFunction a = isEmptyElim a
-- Lean.Parser.Extension
/-- Parser aliases for making `ParserDescr` extensible  -/
Lean.Parser.AliasValue : Type → Type
-- Mathlib.Topology.Basic
/-- **Alias** of the reverse direction of `isClosed_compl_iff`. -/
IsOpen.isClosed_compl : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsOpen s → IsClosed sᶜ
-- Mathlib.RingTheory.WittVector.Complete
/-- If `k` is a perfect ring of characteristic `p`, then the ring of Witt vectors `𝕎 k`
is `p`-adically complete.
 -/
WittVector.isAdicCompleteIdealSpanP : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : CommRing k] [CharP k p] [PerfectRing k p],
  IsAdicComplete (Ideal.span {↑p}) (WittVector p k)
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
/-- The trivial zeroes of the cosine zeta function.  -/
HurwitzZeta.cosZeta_neg_two_mul_nat_add_one : ∀ (a : UnitAddCircle) (n : ℕ), HurwitzZeta.cosZeta a (-2 * (↑n + 1)) = 0
-- Mathlib.Analysis.Convex.Exposed
IsExposed.inter_right : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : TopologicalSpace 𝕜] [inst_1 : Ring 𝕜] [inst_2 : PartialOrder 𝕜]
  [inst_3 : AddCommMonoid E] [inst_4 : TopologicalSpace E] [inst_5 : Module 𝕜 E] {A B C : Set E},
  IsExposed 𝕜 B C → C ⊆ A → IsExposed 𝕜 (A ∩ B) C
-- Mathlib.Data.Finmap
/-- The underlying `Multiset` of a `Finmap`  -/
Finmap.entries : {α : Type u} → {β : α → Type v} → Finmap β → Multiset (Sigma β)