mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
/-- **Alias** of `IsSemilinearSet.sdiff`.

---

Semilinear sets are closed under set difference.  -/
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsSemilinearSet.diff : ∀ {M : Type u_1} [inst : AddCommMonoid M] {s₁ s₂ : Set M},
  IsSemilinearSet s₁ → IsSemilinearSet s₂ → IsSemilinearSet (s₁ \ s₂)
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw.WF.out : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [i₁ : EquivBEq α] [i₂ : LawfulHashable α]
  {m : Std.DHashMap.Raw α β}, m.WF → Std.DHashMap.Internal.Raw.WFImp m
-- Mathlib.Probability.Independence.InfinitePi
/-- If random variables are independent then their joint distribution is the product measure. This
is an `AEMeasurable` version of `iIndepFun.map_fun_eq_infinitePi_map`, which is why it requires
`ι` to be countable.  -/
ProbabilityTheory.iIndepFun.map_fun_eq_infinitePi_map₀' : ∀ {ι : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {𝓧 : ι → Type u_3}
  {m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)} {X : (i : ι) → Ω → 𝓧 i} [Countable ι],
  (∀ (i : ι), AEMeasurable (X i) P) →
    ProbabilityTheory.iIndepFun X P →
      MeasureTheory.Measure.map (fun ω i => X i ω) P =
        MeasureTheory.Measure.infinitePi fun i => MeasureTheory.Measure.map (X i) P
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : CategoryTheory.CommMon C)
  (x : CategoryTheory.Discrete PUnit.{u + 1}),
  (CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj A).obj x = A.X
-- Mathlib.Tactic.Translate.Core
Mathlib.Tactic.Translate.Config.mk.injEq : ∀ (trace : Bool) (target : Lean.Name) (doc : Option (Lean.TSyntax `Lean.Parser.Command.docComment))
  (allowAutoName : Bool) (reorder? : Option Mathlib.Tactic.Translate.ArgReorder)
  (relevantArg? : Option Mathlib.Tactic.Translate.RelevantArg) (attrs : Array Lean.Syntax) (dontTranslate : List ℕ)
  (ref : Lean.Syntax) (existing self none : Bool) (rename : Lean.NameMap Lean.Name) (trace_1 : Bool)
  (target_1 : Lean.Name) (doc_1 : Option (Lean.TSyntax `Lean.Parser.Command.docComment)) (allowAutoName_1 : Bool)
  (reorder?_1 : Option Mathlib.Tactic.Translate.ArgReorder)
  (relevantArg?_1 : Option Mathlib.Tactic.Translate.RelevantArg) (attrs_1 : Array Lean.Syntax)
  (dontTranslate_1 : List ℕ) (ref_1 : Lean.Syntax) (existing_1 self_1 none_1 : Bool)
  (rename_1 : Lean.NameMap Lean.Name),
  ({ trace := trace, target := target, doc := doc, allowAutoName := allowAutoName, reorder? := reorder?,
        relevantArg? := relevantArg?, attrs := attrs, dontTranslate := dontTranslate, ref := ref, existing := existing,
        self := self, none := none, rename := rename } =
      { trace := trace_1, target := target_1, doc := doc_1, allowAutoName := allowAutoName_1, reorder? := reorder?_1,
        relevantArg? := relevantArg?_1, attrs := attrs_1, dontTranslate := dontTranslate_1, ref := ref_1,
        existing := existing_1, self := self_1, none := none_1, rename := rename_1 }) =
    (trace = trace_1 ∧
      target = target_1 ∧
        doc = doc_1 ∧
          allowAutoName = allowAutoName_1 ∧
            reorder? = reorder?_1 ∧
              relevantArg? = relevantArg?_1 ∧
                attrs = attrs_1 ∧
                  dontTranslate = dontTranslate_1 ∧
                    ref = ref_1 ∧ existing = existing_1 ∧ self = self_1 ∧ none = none_1 ∧ rename = rename_1)
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesWithinAt.continuousWithinAt_insert : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E},
  HasFPowerSeriesWithinAt f p s x → ContinuousWithinAt f (insert x s) x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_insertIfNew : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {k a : α} {v : β k},
  (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl.get? a =
    if h : compare k a = Ordering.eq ∧ k ∉ t then some (cast ⋯ v) else t.get? a
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.interSmallerFn.match_1.eq_1 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : Option ((a : α) × β a) → Sort u_3) (kv' : (a : α) × β a)
  (h_1 : (kv' : (a : α) × β a) → motive (some kv')) (h_2 : Unit → motive none),
  (match some kv' with
    | some kv' => h_1 kv'
    | none => h_2 ()) =
    h_1 kv'
-- Mathlib.Topology.EMetricSpace.Lipschitz
LocallyLipschitz.iterate : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {f : α → α}, LocallyLipschitz f → ∀ (n : ℕ), LocallyLipschitz f^[n]
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.IsAtom.congr_simp : ∀ {G : Type u_1} [inst : Group G] {inst_1 : DecidableEq G} [inst_2 : DecidableEq G] (K K_1 : ℝ),
  K = K_1 →
    ∀ (S S_1 : Finset G), S = S_1 → ∀ (A A_1 : Finset G), A = A_1 → Finset.IsAtom✝ K S A = Finset.IsAtom✝ K_1 S_1 A_1
-- Mathlib.CategoryTheory.Sites.CoverPreserving
/-- If `F` is flat, it is continuous if and only if it preserves covers.  -/
CategoryTheory.Functor.isContinuous_iff_coverPreserving : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {J : CategoryTheory.GrothendieckTopology C}
  {K : CategoryTheory.GrothendieckTopology D} [CategoryTheory.RepresentablyFlat F],
  F.IsContinuous J K ↔ CategoryTheory.CoverPreserving J K F
-- Std.Time.Format.DateFormat
/-- Short AM marker (used by `a`/`aa`/`aaa`).
 -/
Std.Time.DateFormatSymbols.amShort : Std.Time.DateFormatSymbols → String
-- Lean.Data.Lsp.Basic
Lean.Lsp.DocumentChange.rename : Lean.Lsp.RenameFile → Lean.Lsp.DocumentChange
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_Iic_sub_Iic : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E}
  {μ : MeasureTheory.Measure ℝ},
  MeasureTheory.IntegrableOn f (Set.Iic a) μ →
    MeasureTheory.IntegrableOn f (Set.Iic b) μ →
      ∫ (x : ℝ) in Set.Iic b, f x ∂μ - ∫ (x : ℝ) in Set.Iic a, f x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ
-- Mathlib.Algebra.Tropical.BigOperators
List.trop_sum : ∀ {R : Type u_1} [inst : AddMonoid R] (l : List R), Tropical.trop l.sum = (List.map Tropical.trop l).prod
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
/-- The finpartition derived from `h.setoid`.  -/
SimpleGraph.IsTuranMaximal.finpartition : {V : Type u_1} →
  [inst : Fintype V] →
    {G : SimpleGraph V} →
      [inst_1 : DecidableRel G.Adj] → {r : ℕ} → G.IsTuranMaximal r → [inst_2 : DecidableEq V] → Finpartition Finset.univ
-- Aesop.Util.Basic
/-- Note: the returned local context contains invalid `LocalDecl`s.
 -/
Aesop.getUnusedNames : Lean.LocalContext → Array Lean.Name → Array Lean.Name × Lean.LocalContext
-- Mathlib.NumberTheory.ModularForms.LFunction
ModularForm.Λ.eq_1 : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.IsArithmetic] {k : ℤ} (hk : 0 < k) {F : Type u_1}
  [inst_1 : FunLike F UpperHalfPlane ℂ] (f : F) [inst_2 : ModularFormClass F Γ k],
  ModularForm.Λ hk f = (ModularForm.weakFEPair hk f).Λ
-- Mathlib.Topology.MetricSpace.Pseudo.Pi
dist_pi_const : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : Fintype β] [Nonempty β] (a b : α),
  (dist (fun x => a) fun x => b) = dist a b
-- Mathlib.Data.Sum.Interval
Sum.Ioc_inl_inr : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] (a₁ : α) (b₂ : β), Finset.Ioc (Sum.inl a₁) (Sum.inr b₂) = ∅
-- Mathlib.Topology.Bornology.Constructions
Bornology.forall_isBounded_image_eval_iff : ∀ {ι : Type u_3} {X : ι → Type u_4} [inst : (i : ι) → Bornology (X i)] {s : Set ((i : ι) → X i)},
  (∀ (i : ι), Bornology.IsBounded (Function.eval i '' s)) ↔ Bornology.IsBounded s
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
/-- The natural map from `n`-cycles to `n`th group homology for a `k`-linear
`G`-representation `A`.  -/
groupHomology.π : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] → (A : Rep.{u, u, u} k G) → (n : ℕ) → groupHomology.cycles A n ⟶ groupHomology A n
-- Mathlib.Logic.Relation
Relation.SymmGen.rfl : ∀ {α : Type u_1} {r : α → α → Prop} {a : α} [Std.Refl r], Relation.SymmGen r a a
-- Mathlib.Tactic.Core
/-- Introduce variables, giving them names from a specified list.  -/
Lean.MVarId.introsWithBinderIdents : Lean.MVarId →
  List (Lean.TSyntax `Lean.binderIdent) →
    optParam (Option ℕ) none → Lean.MetaM (List (Lean.TSyntax `Lean.binderIdent) × Array Lean.FVarId × Lean.MVarId)
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.mapsTo_maxGenEigenspace_of_comm : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f g : Module.End R M},
  Commute f g → ∀ (μ : R), Set.MapsTo ⇑g ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
-- Mathlib.Combinatorics.SimpleGraph.LineGraph
/-- Lift a copy between graphs to an embedding between their line graphs  -/
SimpleGraph.Copy.toLineGraphEmbedding : {V : Type u_1} → {V' : Type u_2} → {G : SimpleGraph V} → {G' : SimpleGraph V'} → G.Copy G' → G.lineGraph ↪g G'.lineGraph
-- Mathlib.Algebra.Order.Monovary
Antivary.pow_left₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : PartialOrder α] [IsOrderedRing α]
  [inst_3 : PartialOrder β] {f : ι → α} {g : ι → β}, 0 ≤ f → Antivary f g → ∀ (n : ℕ), Antivary (f ^ n) g
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.EffectiveEquivalenceRelation.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {R A : C} {p₁ p₂ : R ⟶ A}
  {toEquivalenceRelation : CategoryTheory.EquivalenceRelation p₁ p₂} {B : C} {π : A ⟶ B}
  {isKernelPair : CategoryTheory.IsKernelPair π p₁ p₂} {isPushout : CategoryTheory.IsPushout p₁ p₂ π π}
  {toEquivalenceRelation_1 : CategoryTheory.EquivalenceRelation p₁ p₂} {B_1 : C} {π_1 : A ⟶ B_1}
  {isKernelPair_1 : CategoryTheory.IsKernelPair π_1 p₁ p₂} {isPushout_1 : CategoryTheory.IsPushout p₁ p₂ π_1 π_1},
  { toEquivalenceRelation := toEquivalenceRelation, B := B, π := π, isKernelPair := isKernelPair,
        isPushout := isPushout } =
      { toEquivalenceRelation := toEquivalenceRelation_1, B := B_1, π := π_1, isKernelPair := isKernelPair_1,
        isPushout := isPushout_1 } →
    toEquivalenceRelation = toEquivalenceRelation_1 ∧ B = B_1 ∧ π ≍ π_1
-- Mathlib.Algebra.Order.GroupWithZero.Basic
pow_le_one_iff_of_nonneg : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : LinearOrder M₀] [PosMulStrictMono M₀] {a : M₀} {n : ℕ}
  [ZeroLEOneClass M₀], 0 ≤ a → n ≠ 0 → (a ^ n ≤ 1 ↔ a ≤ 1)
-- Mathlib.Logic.Pairwise
Set.Pairwise.eq : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} {a b : α}, s.Pairwise r → a ∈ s → b ∈ s → ¬r a b → a = b
-- Mathlib.Analysis.Calculus.FDeriv.Linear
ContinuousLinearMap.hasFDerivAtFilter : ∀ {𝕜 : 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) {L : Filter (E × E)}, HasFDerivAtFilter (⇑f) f L
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
/-- If `G` is a group with measurable multiplication, then left multiplication by `g : G` is a
measurable automorphism of `G`.  -/
MeasurableEquiv.mulLeft : {G : Type u_1} → [inst : Group G] → [inst_1 : MeasurableSpace G] → [MeasurableMul G] → G → G ≃ᵐ G
-- Mathlib.Order.GaloisConnection.Basic
GaloisCoinsertion.u_iSup_l : ∀ {α : Type u} {β : Type v} {u : α → β} {l : β → α} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  (gi : GaloisCoinsertion l u) {ι : Sort x} (f : ι → β), u (⨆ i, l (f i)) = ⨆ i, f i
-- Mathlib.Data.FunLike.IsApply
/-- **Alias** of `IsPowApply.pow_apply`. -/
pow_apply : ∀ {M : Type u_1} {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} {inst : FunLike F α β}
  {inst_1 : Pow β M} {inst_2 : Pow F M} [self : IsPowApply M F α β] (f : F) (n : M) (x : α), (f ^ n) x = f x ^ n
-- Lean.PrettyPrinter
Lean.PrettyPrinter.ppConstNameWithInfos : Lean.Name → Lean.MetaM Lean.FormatWithInfos
-- Mathlib.Order.Category.HeytAlg
/-- The category of Heyting algebras.  -/
HeytAlg : Type (u_1 + 1)
-- Init.Data.Vector.Lemmas
Vector.getElem?_append : ∀ {α : Type u_1} {n m : ℕ} {xs : Vector α n} {ys : Vector α m} {i : ℕ},
  (xs ++ ys)[i]? = if i < n then xs[i]? else ys[i - n]?
-- Init.Data.UInt.Lemmas
UInt16.eq_of_toFin_eq : ∀ {a b : UInt16}, a.toFin = b.toFin → a = b
-- Mathlib.FieldTheory.IsAlgClosed.Basic
IntermediateField.algHomEquivAlgHomOfSplits_apply : ∀ {F : Type u_1} {K : Type u_2} (A : Type u_3) [inst : Field F] [inst_1 : Field K] [inst_2 : Field A]
  [inst_3 : Algebra F K] [inst_4 : Algebra F A] [inst_5 : Algebra.IsAlgebraic F K] (L : IntermediateField F A)
  (hL : ∀ (x : K), (Polynomial.map (algebraMap F ↥L) (minpoly F x)).Splits) (φ₂ : K →ₐ[F] ↥L),
  (IntermediateField.algHomEquivAlgHomOfSplits A L hL) φ₂ = L.val.comp φ₂
-- Init.Control.Lawful.Instances
StateT.run_pure : ∀ {m : Type u_1 → Type u_2} {α σ : Type u_1} [inst : Monad m] (a : α) (s : σ), (pure a).run s = pure (a, s)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKey?_filter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : α → β → Bool} {k : α} (h : (↑m).WF),
  (Std.DHashMap.Internal.Raw₀.filter f m).getKey? k =
    (m.getKey? k).pfilter fun x h' => f x (Std.DHashMap.Internal.Raw₀.Const.get m x ⋯)
-- Mathlib.Analysis.Convex.DoublyStochasticMatrix
/-- A matrix is doubly stochastic iff its transpose is doubly stochastic  -/
transpose_mem_doublyStochastic_iff : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R] {M : Matrix n n R},
  M.transpose ∈ doublyStochastic R n ↔ M ∈ doublyStochastic R n
-- Mathlib.CategoryTheory.ComposableArrows.Basic
_private.Mathlib.CategoryTheory.ComposableArrows.Basic.0.CategoryTheory.ComposableArrows.homMk₀.match_1.splitter : (motive : Fin (0 + 1) → Sort u_1) → (i : Fin (0 + 1)) → ((isLt : 0 < 0 + 1) → motive ⟨0, isLt⟩) → motive i
-- Mathlib.NumberTheory.Real.Irrational
Irrational.of_natCast_add : ∀ {x : ℝ} (m : ℕ), Irrational (↑m + x) → Irrational x
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey!_union : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α}, (t₁ ∪ t₂).getKey! k = t₂.getKeyD k (t₁.getKey! k)
-- Mathlib.SetTheory.Cardinal.Finite
Nat.card_pos : ∀ {α : Type u_1} [Nonempty α] [Finite α], 0 < Nat.card α
-- Mathlib.Data.Finset.Sigma
Finset.mem_sigmaLift : ∀ {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {γ : ι → Type u_4} [inst : DecidableEq ι]
  (f : ⦃i : ι⦄ → α i → β i → Finset (γ i)) (a : Sigma α) (b : Sigma β) (x : Sigma γ),
  x ∈ Finset.sigmaLift f a b ↔ ∃ (ha : a.fst = x.fst) (hb : b.fst = x.fst), x.snd ∈ f (ha ▸ a.snd) (hb ▸ b.snd)
-- Std.Http.Data.URI.Encoding
/-- Creates an encoded userinfo component from raw bytes, panicking on invalid encoding.
 -/
Std.Http.URI.EncodedUserInfo.ofByteArray! : ByteArray → Std.Http.URI.EncodedUserInfo
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
/-- If `X` represents a presheaf of groups `F`, then `Hom(-, X)` is isomorphic to `F` as
a presheaf of groups.  -/
CategoryTheory.yonedaGrpObjIsoOfRepresentableBy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      (X : C) →
        (F : CategoryTheory.Functor Cᵒᵖ GrpCat) →
          (α : (F.comp (CategoryTheory.forget GrpCat)).RepresentableBy X) → CategoryTheory.yonedaGrpObj X ≅ F
-- Mathlib.Algebra.Homology.SpectralObject.Homology
CategoryTheory.Abelian.SpectralObject.dKernelSequence_X₃ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {i₀ i₁ i₂ i₃ i₄ i₅ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₂₃ : i₁ ⟶ i₃)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ n₃ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.dKernelSequence._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.dKernelSequence._auto_3)
  (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.dKernelSequence._auto_5),
  (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃).X₃ = X.E f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.toListModel_unionₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m₁ →
    Std.DHashMap.Internal.Raw.WFImp ↑m₂ →
      (Std.DHashMap.Internal.toListModel (↑(m₁.unionₘ m₂)).buckets).Perm
        (Std.Internal.List.insertList (Std.DHashMap.Internal.toListModel (↑m₁).buckets)
          (Std.DHashMap.Internal.toListModel (↑m₂).buckets))
-- Mathlib.Algebra.Star.Basic
Units.coe_star_inv : ∀ {R : Type u} [inst : Monoid R] [inst_1 : StarMul R] (u : Rˣ), ↑(star u)⁻¹ = star ↑u⁻¹
-- Mathlib.Order.SuccPred.Limit
Order.IsSuccLimit.bot_lt : ∀ {α : Type u_1} {a : α} [inst : Preorder α] [inst_1 : OrderBot α], Order.IsSuccLimit a → ⊥ < a
-- Std.Net.Addr
/-- Turn `addr` into a `String` in the IPv6 format described in
[RFC 2373](https://datatracker.ietf.org/doc/html/rfc2373).
 -/
Std.Net.IPv6Addr.toString : Std.Net.IPv6Addr → String
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
AlgebraicGeometry.mono_pushoutSection_of_iSup_eq : ∀ {X Y S T : AlgebraicGeometry.Scheme} {f : T ⟶ S} {g : Y ⟶ X} {iX : X ⟶ S} {iY : Y ⟶ T}
  (H : CategoryTheory.IsPullback g iY iX f) {US : S.Opens} {UT : T.Opens} {UX : X.Opens}
  (hUST : UT ≤ (TopologicalSpace.Opens.map f.base).obj US) (hUSX : UX ≤ (TopologicalSpace.Opens.map iX.base).obj US)
  {UY : Y.Opens} (hUY : UY = (TopologicalSpace.Opens.map g.base).obj UX ⊓ (TopologicalSpace.Opens.map iY.base).obj UT)
  {ι : Type u_1} [Finite ι] (VX : ι → X.Opens) (hVU : iSup VX = UX),
  (∀ (i : ι), CategoryTheory.Mono (AlgebraicGeometry.pushoutSection H hUST ⋯ ⋯)) →
    (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f US UT hUST)).Flat →
      CategoryTheory.Mono (AlgebraicGeometry.pushoutSection H hUST hUSX hUY)
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.foldTR.loop : {α : Type u} → (n : ℕ) → ((i : ℕ) → i < n → α → α) → (j : ℕ) → j ≤ n → α → α
-- Mathlib.Algebra.Group.Basic
addConj_eq_zero_iff : ∀ {G : Type u_3} [inst : AddGroup G] {a b : G}, a + b + -a = 0 ↔ b = 0
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintKind : Type
-- Mathlib.CategoryTheory.ConcreteCategory.Forget
CategoryTheory.forget_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)}
  {CC : outParam (C → Type w)} [inst_1 : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))]
  [inst_2 : CategoryTheory.ConcreteCategory C FC] (X : C), (CategoryTheory.forget C).obj X = CategoryTheory.ToType X
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
/-- The number of all darts in a simple finite graph is equal to the dot product of
`G.adjMatrix α *ᵥ 1` and `1`.  -/
SimpleGraph.natCast_card_dart_eq_dotProduct : ∀ {α : Type u_1} {V : Type u_2} (G : SimpleGraph V) [inst : DecidableRel G.Adj] [inst_1 : Fintype V]
  [inst_2 : NonAssocSemiring α], ↑(Fintype.card G.Dart) = (SimpleGraph.adjMatrix α G).mulVec 1 ⬝ᵥ 1
-- Mathlib.Topology.Algebra.UniformConvergence
instIsScalarTowerUniformFun : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_6} [inst : SMul M N] [inst_1 : SMul M β] [inst_2 : SMul N β]
  [IsScalarTower M N β], IsScalarTower M N (UniformFun α β)
-- Mathlib.RingTheory.WittVector.TeichmullerSeries
WittVector.teichmuller_mul_pow_coeff_of_ne : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {R : Type u_1} [inst : CommRing R] [CharP R p] (x : R) {m n : ℕ},
  m ≠ n → ((WittVector.teichmuller p) x * ↑p ^ n).coeff m = 0
-- Mathlib.Algebra.Ring.Hom.Defs
RingHom.id_apply : ∀ {α : Type u_2} {x : NonAssocSemiring α} (x_1 : α), (RingHom.id α) x_1 = x_1
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- The subshift defined by a family of forbidden patterns `F`.

This is a standard way to construct subshifts:
`Subshift.ofForbidden F` consists of all configurations `x : G → A` in which no pattern
`p ∈ F` occurs at any position.

Formally:
* the carrier is `forbidden F` (configurations avoiding `F`),
* it is closed because each occurrence set is open, and
* it is shift-invariant since avoidance is preserved by shifts.  -/
SymbolicDynamics.FullShift.Subshift.ofForbidden : {A : Type u_1} →
  [inst : TopologicalSpace A] →
    [inst_1 : Inhabited A] →
      {G : Type u_2} →
        [inst_2 : AddMonoid G] →
          [IsLeftCancelAdd G] →
            [DiscreteTopology A] →
              Set (SymbolicDynamics.FullShift.Pattern A G) → SymbolicDynamics.FullShift.Subshift A G
-- Qq.MetaM
Qq.synthInstanceQ? : {u : Lean.Level} → (α : Q(Sort u)) → Lean.MetaM (Option Q(«$α»))
-- Mathlib.GroupTheory.PGroup
IsPGroup.card_orbit : ∀ {p : ℕ} {G : Type u_1} [inst : Group G],
  IsPGroup p G →
    ∀ [hp : Fact (Nat.Prime p)] {α : Type u_2} [inst_1 : MulAction G α] (a : α) [Finite ↑(MulAction.orbit G a)],
      ∃ n, Nat.card ↑(MulAction.orbit G a) = p ^ n
-- Mathlib.Analysis.Normed.Lp.Finsupp
/-- The L^1 extended metric on `ι`-many copies of a metric space `X`  -/
Finsupp.instEMetricSpaceWithLpOfNNReal : {ι : Type u_1} →
  {X : Type u_2} →
    [inst : Zero X] → {p : NNReal} → [Fact (1 ≤ p)] → [EMetricSpace X] → EMetricSpace (WithLp (↑p) (ι →₀ X))
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Zipper.size_prependMap : ∀ {α : Type u} {β : α → Type v} (t : Std.DTreeMap.Internal.Impl α β) (it : Std.DTreeMap.Internal.Zipper α β),
  Std.DTreeMap.Internal.Zipper.size✝ (Std.DTreeMap.Internal.Zipper.prependMap t it) =
    t.treeSize + Std.DTreeMap.Internal.Zipper.size✝ it
-- Mathlib.Analysis.Complex.UpperHalfPlane.Topology
/-- Each element of `GL(2, ℝ)` defines a continuous map `ℍ → ℍ`.  -/
UpperHalfPlane.instContinuousGLSMul : ContinuousConstSMul (GL (Fin 2) ℝ) UpperHalfPlane
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Expr.toPoly.match_4.eq_6 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (a b : Lean.Grind.CommRing.Expr)
  (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k))
  (h_2 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k))
  (h_3 : (k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k))
  (h_4 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_5 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_6 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b)) (h_7 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_8 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b))
  (h_9 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k)),
  (match a.mul b with
    | Lean.Grind.CommRing.Expr.num k => h_1 k
    | Lean.Grind.CommRing.Expr.intCast k => h_2 k
    | Lean.Grind.CommRing.Expr.natCast k => h_3 k
    | Lean.Grind.CommRing.Expr.var x => h_4 x
    | a.add b => h_5 a b
    | a.mul b => h_6 a b
    | a.neg => h_7 a
    | a.sub b => h_8 a b
    | a.pow k => h_9 a k) =
    h_6 a b
-- Std.Data.ExtDTreeMap.Basic
Std.ExtDTreeMap.instBEqOfLawfulEqCmpOfTransCmp : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [Std.LawfulEqCmp cmp] → [Std.TransCmp cmp] → [(k : α) → BEq (β k)] → BEq (Std.ExtDTreeMap α β cmp)