mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.LSeries.DirichletContinuation
/-- **Functional equation** for primitive Dirichlet L-functions.  -/
DirichletCharacter.IsPrimitive.completedLFunction_one_sub : ∀ {N : ℕ} [inst : NeZero N] {χ : DirichletCharacter ℂ N},
  χ.IsPrimitive →
    ∀ (s : ℂ),
      DirichletCharacter.completedLFunction χ (1 - s) =
        ↑N ^ (s - 1 / 2) * χ.rootNumber * DirichletCharacter.completedLFunction χ⁻¹ s
-- Mathlib.MeasureTheory.Measure.AddContent
/-- In a ring of sets, continuity of an additive content at `∅` implies σ-additivity.
This is not true in general in semirings, or without the hypothesis that `m` is finite. See the
examples 7 and 8 in Halmos' book Measure Theory (1974), page 40.  -/
MeasureTheory.addContent_iUnion_eq_sum_of_tendsto_zero : ∀ {α : Type u_1} {C : Set (Set α)},
  MeasureTheory.IsSetRing C →
    ∀ (m : MeasureTheory.AddContent ENNReal C),
      (∀ s ∈ C, m s ≠ ⊤) →
        (∀ ⦃s : ℕ → Set α⦄,
            (∀ (n : ℕ), s n ∈ C) →
              Antitone s → ⋂ n, s n = ∅ → Filter.Tendsto (fun n => m (s n)) Filter.atTop (nhds 0)) →
          ∀ ⦃f : ℕ → Set α⦄,
            (∀ (i : ℕ), f i ∈ C) →
              ⋃ i, f i ∈ C → Pairwise (Function.onFun Disjoint f) → m (⋃ i, f i) = ∑' (i : ℕ), m (f i)
-- Lean.Server.ServerTask
Lean.Server.ServerTask.IO.asTask : {α : Type} → IO α → BaseIO (Lean.Server.ServerTask (Except IO.Error α))
-- Mathlib.CategoryTheory.Preadditive.Injective.Preserves
CategoryTheory.Functor.preservesInjectiveObjects_of_adjunction_of_preservesMonomorphisms : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [F.PreservesMonomorphisms],
  G.PreservesInjectiveObjects
-- Mathlib.Algebra.Symmetrized
SymAlg.instInv : {α : Type u_1} → [Inv α] → Inv αˢʸᵐ
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
/-- Binary entropy is strictly increasing in interval [0, 1/2].  -/
Real.binEntropy_strictMonoOn : StrictMonoOn Real.binEntropy (Set.Icc 0 2⁻¹)
-- Init.Data.String.Basic
String.toList_singleton : ∀ (c : Char), (String.singleton c).toList = [c]
-- Mathlib.Analysis.Calculus.Deriv.Pow
HasDerivAt.pow : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedCommRing 𝔸]
  [inst_2 : NormedAlgebra 𝕜 𝔸] {f : 𝕜 → 𝔸} {f' : 𝔸} {x : 𝕜},
  HasDerivAt f f' x → ∀ (n : ℕ), HasDerivAt (f ^ n) (↑n * f x ^ (n - 1) * f') x
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.comp_liftCycles : ∀ {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' A : C}
  (k : A ⟶ K.X i) (j : ι) (hj : c.next i = j) (hk : CategoryTheory.CategoryStruct.comp k (K.d i j) = 0) (α : A' ⟶ A),
  CategoryTheory.CategoryStruct.comp α (K.liftCycles k j hj hk) =
    K.liftCycles (CategoryTheory.CategoryStruct.comp α k) j hj ⋯
-- Lean.Declaration
Lean.Declaration.definitionVal! : Lean.Declaration → Lean.DefinitionVal
-- LeanSearchClient.LoogleSyntax
LeanSearchClient.instReprLoogleMatch : Repr LeanSearchClient.LoogleMatch
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousLinearMap.flipMultilinear_apply_apply : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} {G' : Type wG'} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : SeminormedAddCommGroup G']
  [inst_6 : NormedSpace 𝕜 G'] [inst_7 : Fintype ι] (f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G') (m : (i : ι) → E i)
  (x : G), (f.flipMultilinear m) x = (f x) m
-- Mathlib.GroupTheory.Commutator.Basic
instNonemptyElemAddCommutatorSet : ∀ (G : Type u_1) [inst : AddGroup G], Nonempty ↑(addCommutatorSet G)
-- Mathlib.LinearAlgebra.AffineSpace.Pointwise
AffineSubspace.pointwise_vadd_top : ∀ {k : Type u_2} {V : Type u_3} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (v : V), v +ᵥ ⊤ = ⊤
-- Mathlib.Tactic.Linter.TextBased
/-- Verify that no module name is forbidden according to Windows' filename rules.  -/
Mathlib.Linter.TextBased.linter.modulesForbiddenWindows : Lean.Option Bool
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙHom_of_cfcHom.congr_simp : ∀ (R : Type u_1) {A : Type u_2} {p p_1 : A → Prop} (e_p : p = p_1) [inst : Semifield R] [inst_1 : StarRing R]
  [inst_2 : MetricSpace R] [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Ring A]
  [inst_6 : StarRing A] [inst_7 : TopologicalSpace A] [inst_8 : Algebra R A]
  [inst_9 : ContinuousFunctionalCalculus R A p] {a : A} (ha : p a), cfcₙHom_of_cfcHom R ha = cfcₙHom_of_cfcHom R ⋯
-- Mathlib.Analysis.Complex.Poisson
_private.Mathlib.Analysis.Complex.Poisson.0.re_herglotzRieszKernel_le_aux : ∀ (φ θ r R : ℝ),
  0 < r →
    r < R →
      ((↑R * Complex.exp (↑θ * Complex.I) + ↑r * Complex.exp (↑φ * Complex.I)) /
            (↑R * Complex.exp (↑θ * Complex.I) - ↑r * Complex.exp (↑φ * Complex.I))).re ≤
        (R + r) / (R - r)
-- Mathlib.CategoryTheory.Galois.Full
/-- Let `X` be an object of a Galois category with fiber functor `F` and `Y` a sub-`Aut F`-set
of `F.obj X`. Then there exists a sub-object `Z` of `X` and an isomorphism
`Y ≅ F.obj X` as `Aut F`-sets such that the obvious triangle commutes.
 -/
CategoryTheory.PreGaloisCategory.exists_lift_of_mono : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C)
  (Y : Action FintypeCat (CategoryTheory.Aut F)) (i : Y ⟶ (CategoryTheory.PreGaloisCategory.functorToAction F).obj X)
  [CategoryTheory.Mono i],
  ∃ Z f u,
    CategoryTheory.Mono f ∧
      CategoryTheory.CategoryStruct.comp u.hom ((CategoryTheory.PreGaloisCategory.functorToAction F).map f) = i
-- Mathlib.Logic.Denumerable
_private.Mathlib.Logic.Denumerable.0.Encodable.decodeSum.match_1.eq_1 : ∀ (motive : Bool → ℕ → Sort u_1) (m : ℕ) (h_1 : (m : ℕ) → motive false m) (h_2 : (x : Bool) → (m : ℕ) → motive x m),
  (match false, m with
    | false, m => h_1 m
    | x, m => h_2 x m) =
    h_1 m
-- Mathlib.CategoryTheory.Sites.Point.Presheaf
CategoryTheory.GrothendieckTopology.pointBotPresheafFiberIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] (X : C)
  (A : Type u_1) [inst_2 : CategoryTheory.Category.{u_2, u_1} A]
  [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, u_2, u_1} A],
  (CategoryTheory.GrothendieckTopology.pointBotPresheafFiberIso X A).inv =
    (CategoryTheory.GrothendieckTopology.pointBot X).toPresheafFiberNatTrans X
      (CategoryTheory.shrinkYonedaObjObjEquiv.symm (CategoryTheory.CategoryStruct.id X))
-- Mathlib.RingTheory.ZariskisMainTheorem
/-- [Stacks Tag 00PY](https://stacks.math.columbia.edu/tag/00PY) -/
isStronglyTranscendental_mk_radical_conductor : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  integralClosure R S = ⊥ →
    ∀ (x : S), (Polynomial.aeval x).Finite → IsStronglyTranscendental R ((Ideal.Quotient.mk (conductor R x).radical) x)
-- Mathlib.Algebra.Group.TypeTags.Basic
Multiplicative.mulOneClass : {α : Type u} → [AddZeroClass α] → MulOneClass (Multiplicative α)
-- Mathlib.Algebra.Category.FGModuleCat.Basic
/-- The dual module is the dual in the rigid monoidal category `FGModuleCat K`.  -/
FGModuleCat.FGModuleCatDual : (K : Type u) → [inst : Field K] → FGModuleCat K → FGModuleCat K
-- Mathlib.Combinatorics.Quiver.Cast
Quiver.eq_nil_of_length_zero : ∀ {U : Type u_1} [inst : Quiver U] {u v : U} (p : Quiver.Path u v) (hzero : p.length = 0),
  Quiver.Path.cast ⋯ ⋯ p = Quiver.Path.nil
-- Batteries.Data.Vector.Lemmas
_private.Batteries.Data.Vector.Lemmas.0.Vector.scanrM.loop_toArray : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : ℕ} {cur : β} [inst : Monad m] [LawfulMonad m]
  {f : α → β → m β} {as : Vector α n} {i : ℕ} {hi : i ≤ n} {acc_v : Vector β (n - i)} {acc_a : Array β}
  {h_acc : acc_v.toArray = acc_a},
  Vector.toArray <$> Vector.scanrM.loop f as cur i hi acc_v = Array.scanrM.loop f cur as.toArray i 0 ⋯ acc_a
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.star_add_self' : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) [inst : CommRing R],
  star a + a = ↑(2 * a.re + c₂ * a.imI)
-- Mathlib.Data.Set.Card
Set.encard_mono : ∀ {α : Type u_3}, Monotone Set.encard
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.coeff_preΨ_ne_zero : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) {n : ℤ},
  ↑n ≠ 0 → (W.preΨ n).coeff ((n.natAbs ^ 2 - if Even n then 4 else 1) / 2) ≠ 0
-- Mathlib.Topology.UniformSpace.Ultra.Basic
ball_subset_of_mem : ∀ {X : Type u_1} {V : SetRel X X} [V.IsTrans] {x y : X},
  y ∈ UniformSpace.ball x V → UniformSpace.ball y V ⊆ UniformSpace.ball x V
-- Mathlib.Algebra.Group.Hom.Basic
/-- If `f` is an additive monoid homomorphism to an additive commutative group,
then `-f` is the homomorphism sending `x` to `-(f x)`.  -/
AddMonoidHom.instNeg : {M : Type u_2} → {G : Type u_5} → [inst : AddZeroClass M] → [inst_1 : AddCommGroup G] → Neg (M →+ G)
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.isClosed_iff_of_mem : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set (OnePoint X)},
  OnePoint.infty ∈ s → (IsClosed s ↔ IsClosed (OnePoint.some ⁻¹' s))
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
AddLECancellable.inj : ∀ {α : Type u_1} [inst : Add α] [inst_1 : PartialOrder α] {a b c : α}, AddLECancellable a → (a + b = a + c ↔ b = c)
-- Mathlib.LinearAlgebra.Projection
Submodule.projectionOnto_apply_eq_zero_iff : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (h : IsCompl p q) {x : E}, (p.projectionOnto q h) x = 0 ↔ x ∈ q
-- Std.Http.Protocol.H1.Parser
/-- Parses a reason phrase (text after status code).

Allows only `HTAB / SP / VCHAR` bytes (strict ASCII-only).
 -/
_private.Std.Http.Protocol.H1.Parser.0.Std.Http.Protocol.H1.parseReasonPhrase : Std.Http.Protocol.H1.Config → Std.Internal.Parsec.ByteArray.Parser String
-- Init.Data.Array.Lemmas
Array.eq_push_append_of_mem : ∀ {α : Type u_1} {xs : Array α} {x : α}, x ∈ xs → ∃ as bs, xs = as.push x ++ bs ∧ x ∉ as
-- Mathlib.Algebra.CharP.Defs
ringChar.charP : ∀ (R : Type u_1) [inst : NonAssocSemiring R], CharP R (ringChar R)
-- Mathlib.RingTheory.Invariant.Galois
Ideal.IsFractionRing.finite_of_isInvariant : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (G : Type u_3)
  [Finite G] [inst_4 : Group G] [inst_5 : MulSemiringAction G B] [Algebra.IsInvariant A B G] (P : Ideal A) (Q : Ideal B)
  [inst_7 : Q.LiesOver P] [P.IsPrime] [Q.IsPrime] (K : Type u_4) (L : Type u_5) [inst_10 : Field K] [inst_11 : Field L]
  [inst_12 : Algebra K L] [inst_13 : Algebra (A ⧸ P) K] [IsFractionRing (A ⧸ P) K] [inst_15 : Algebra (B ⧸ Q) L]
  [IsFractionRing (B ⧸ Q) L] [inst_17 : Algebra (A ⧸ P) L] [IsScalarTower (A ⧸ P) (B ⧸ Q) L] [IsScalarTower (A ⧸ P) K L]
  [SMulCommClass G A B] [Algebra.IsSeparable K L], Module.Finite K L
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Coverage.Saturate.of : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {K : CategoryTheory.Coverage C} (X : C),
  ∀ S ∈ K.coverings X, K.Saturate X (CategoryTheory.Sieve.generate S)
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- Suppose that the topology on `α` is defined by its restrictions to the sets of `𝔖`.

Then the set of continuous functions is closed
in the topology of uniform convergence on the sets of `𝔖`.  -/
UniformOnFun.isClosed_setOfPred_continuous : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace β] {𝔖 : Set (Set α)} [inst_1 : TopologicalSpace α],
  Topology.IsCoherentWith 𝔖 → IsClosed {f | Continuous ((UniformOnFun.toFun 𝔖) f)}
-- Lean.Meta.Sym.Arith.Poly
/-- `coprime m₁ m₂` returns `true` if the given monomials
do not have any variable in common.
 -/
Lean.Grind.CommRing.Mon.coprime : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Bool
-- Std.Data.Internal.List.Associative
Std.Internal.List.minEntry?_insertEntry : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α} {v : β k}
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.minEntry? (Std.Internal.List.insertEntry k v l) =
      some
        (match Std.Internal.List.minEntry? l with
        | none => ⟨k, v⟩
        | some w => if (compare k w.fst).isLE = true then ⟨k, v⟩ else w)
-- Mathlib.CategoryTheory.Action.Concrete
/-- Bundles a finite type `H` with a multiplicative action of `G` as an `Action`.  -/
Action.FintypeCat.ofMulAction : (G : Type u_1) → (H : FintypeCat) → [inst : Monoid G] → [MulAction G H.obj] → Action FintypeCat G
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
CochainComplex.mappingCone.triangleMapOfHomotopy_comm₃_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {K₁ L₁ K₂ L₂ : CochainComplex C ℤ} {φ₁ : K₁ ⟶ L₁}
  {φ₂ : K₂ ⟶ L₂} {a : K₁ ⟶ K₂} {b : L₁ ⟶ L₂}
  (H : Homotopy (CategoryTheory.CategoryStruct.comp φ₁ b) (CategoryTheory.CategoryStruct.comp a φ₂))
  {Z : CochainComplex C ℤ}
  (h : (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).obj (CochainComplex.mappingCone.triangle φ₂).obj₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.mapOfHomotopy H)
      (CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.triangle φ₂).mor₃ h) =
    CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.triangle φ₁).mor₃
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map a) h)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKeyD_filterMap : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {f : α → β → Option γ} {k fallback : α},
  (Std.ExtDTreeMap.filterMap f t).getKeyD k fallback =
    ((t.getKey? k).pfilter fun x h' => (f x (Std.ExtDTreeMap.Const.get t x ⋯)).isSome).getD fallback
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
/-- The right fraction from `X` to `Y` given by a morphism `s : Y ⟶ X` such that `W s`.  -/
CategoryTheory.MorphismProperty.RightFraction.ofInv : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} → {X Y : C} → (s : Y ⟶ X) → W s → W.RightFraction X Y
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.getThenInsertIfNew?_eq_get?ₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) (b : β a), (m.getThenInsertIfNew? a b).1 = m.get?ₘ a
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
SimpleGraph.edgeSet_completeBipartiteGraph : ∀ {W₁ : Type u_2} {W₂ : Type u_3},
  (completeBipartiteGraph W₁ W₂).edgeSet = Set.range fun x => s(Sum.inl x.1, Sum.inr x.2)
-- Mathlib.RingTheory.Valuation.Basic
AddValuation.IsEquiv.symm : ∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : LinearOrderedAddCommMonoidWithTop Γ₀]
  [inst_1 : LinearOrderedAddCommMonoidWithTop Γ'₀] [inst_2 : Ring R] {v₁ : AddValuation R Γ₀} {v₂ : AddValuation R Γ'₀},
  v₁.IsEquiv v₂ → v₂.IsEquiv v₁
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- In a preadditive category, any binary bicone which is a limit cone is in fact a bilimit
bicone.  -/
CategoryTheory.Limits.isBinaryBilimitOfIsLimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X Y : C} → (t : CategoryTheory.Limits.BinaryBicone X Y) → CategoryTheory.Limits.IsLimit t.toCone → t.IsBilimit
-- Std.Data.HashSet.Lemmas
Std.HashSet.containsThenInsert_fst : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} {k : α}, (m.containsThenInsert k).1 = m.contains k
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.Limits.preservesColimitsOfShape_walkingCospan_of_forall_isPushout : ∀ {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 Y Z : C⦄ (f : Z ⟶ X) (g : Z ⟶ Y) [CategoryTheory.Limits.HasPushout f g],
      ∃ P inl inr,
        CategoryTheory.IsPushout f g inl inr ∧ CategoryTheory.IsPushout (F.map f) (F.map g) (F.map inl) (F.map inr)) →
    CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingSpan F
-- Mathlib.Algebra.Order.Antidiag.Pi
/-- Auxiliary construction for `finAntidiagonal` that bundles a proof of lawfulness
(`mem_finAntidiagonal`), as this is needed to invoke `disjiUnion`. Using `Finset.disjiUnion` makes
this computationally much more efficient than using `Finset.biUnion`.  -/
Finset.finAntidiagonal.aux : {μ : Type u_2} →
  [inst : AddCommMonoid μ] →
    [Finset.HasAntidiagonal μ] → [DecidableEq μ] → (d : ℕ) → (n : μ) → { s // ∀ (f : Fin d → μ), f ∈ s ↔ ∑ i, f i = n }
-- Init.Data.Vector.Perm
Vector.Perm.rfl : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n}, xs.Perm xs
-- Mathlib.CategoryTheory.Shift.Twist
/-- Given a category `C` equipped with a shift by a monoid `A`  -/
CategoryTheory.TwistShiftData : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    (A : Type w) → [inst_1 : AddMonoid A] → [CategoryTheory.HasShift C A] → Type (max (max u v) w)
-- Mathlib.Analysis.Distribution.DerivNotation
LineDeriv.iteratedLineDerivOp_neg : ∀ {V : Type u_5} {E : Type u_6} [inst : LineDeriv V E E] {n : ℕ} (m : Fin n → V) [inst_1 : AddCommGroup V]
  [inst_2 : AddCommGroup E] [LineDerivAdd V E E] (x : E),
  LineDeriv.iteratedLineDerivOp m (-x) = -LineDeriv.iteratedLineDerivOp m x
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size_alter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {f : Option β → Option β},
  (m.alter k f).size =
    if k ∈ m ∧ (f m[k]?).isNone = true then m.size - 1
    else if k ∉ m ∧ (f m[k]?).isSome = true then m.size + 1 else m.size
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.IsImage.iff_preimage_eq' : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y},
  e.IsImage s t ↔ e.source ∩ ↑e ⁻¹' (e.target ∩ t) = e.source ∩ s
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.HasBinaryBiproduct.hasColimit_pair : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} [CategoryTheory.Limits.HasBinaryBiproduct P Q],
  CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.pair P Q)
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveCodiscrete
CategoryTheory.Codiscrete.equivFun_symm_apply_map : ∀ {X : Type u} {n : ℕ} (f : Fin (n + 1) → X) {X_1 Y : Fin ((Opposite.unop (Opposite.op { len := n })).len + 1)}
  (x : X_1 ⟶ Y), (CategoryTheory.Codiscrete.equivFun.symm f).map x = ({ as := f X_1 }.iso { as := f Y }).hom
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso_inv_naturality_assoc : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A]
  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X)
  [inst_4 : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : CategoryTheory.Sheaf J₀ A) {X₀ Y₀ : C₀}
  (f : X₀ ⟶ Y₀) {Z : A}
  (h : (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheaf data G₀).obj (Opposite.op (F.obj X₀)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (G₀.obj.map f.op)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso data G₀ X₀).inv h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso data G₀ Y₀).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap data G₀ (F.map f)) h)
-- Mathlib.Algebra.Lie.Rank
/-- Let `x` be an element of a Lie algebra `L` over `R`, and write `n` for `rank R L`.
Then `x` is *regular*
if the `n`-th coefficient of the characteristic polynomial of `ad R L x` is non-zero.  -/
LieModule.IsRegular : (R : Type u_1) →
  {L : Type u_3} →
    (M : Type u_4) →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [Module.Finite R L] →
              [Module.Free R L] →
                [inst_5 : AddCommGroup M] →
                  [inst_6 : Module R M] →
                    [inst_7 : LieRingModule L M] →
                      [LieModule R L M] → [Module.Finite R M] → [Module.Free R M] → L → Prop
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_9.eq_5 : ∀ (motive : Std.Tactic.BVDecide.BVBinOp → Sort u_1) (h_1 : Unit → motive Std.Tactic.BVDecide.BVBinOp.and)
  (h_2 : Unit → motive Std.Tactic.BVDecide.BVBinOp.or) (h_3 : Unit → motive Std.Tactic.BVDecide.BVBinOp.xor)
  (h_4 : Unit → motive Std.Tactic.BVDecide.BVBinOp.add) (h_5 : Unit → motive Std.Tactic.BVDecide.BVBinOp.mul)
  (h_6 : Unit → motive Std.Tactic.BVDecide.BVBinOp.udiv) (h_7 : Unit → motive Std.Tactic.BVDecide.BVBinOp.umod),
  (match Std.Tactic.BVDecide.BVBinOp.mul with
    | Std.Tactic.BVDecide.BVBinOp.and => h_1 ()
    | Std.Tactic.BVDecide.BVBinOp.or => h_2 ()
    | Std.Tactic.BVDecide.BVBinOp.xor => h_3 ()
    | Std.Tactic.BVDecide.BVBinOp.add => h_4 ()
    | Std.Tactic.BVDecide.BVBinOp.mul => h_5 ()
    | Std.Tactic.BVDecide.BVBinOp.udiv => h_6 ()
    | Std.Tactic.BVDecide.BVBinOp.umod => h_7 ()) =
    h_5 ()
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.triangle_assoc_comp_right_inv_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c) {Z : a ⟶ c}
  (h :
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id b) g) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.rightUnitor f).inv g)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.id b) g).hom h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.leftUnitor g).inv) h
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.map_le_map_iff : ∀ {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : LieRingModule L M] [inst_5 : AddCommGroup M']
  [inst_6 : Module R M'] [inst_7 : LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'} {N N₂ : LieSubmodule R L M},
  Function.Injective ⇑f → (LieSubmodule.map f N ≤ LieSubmodule.map f N₂ ↔ N ≤ N₂)
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.leftRegularHom_hom_single : ∀ {k : Type u} {G : Type v} [inst : Ring k] [inst_1 : Monoid G] {A : Rep.{max u v, u, v} k G} (g : G) (x : ↑A) (r : k),
  (Rep.Hom.hom (A.leftRegularHom x)) (MonoidAlgebra.single g r) = r • (A.ρ g) x
-- Mathlib.GroupTheory.GroupAction.Defs
/-- The stabilizer of a point `a` as an additive submonoid of `M`.  -/
AddAction.stabilizerAddSubmonoid : (M : Type u_1) → {α : Type u_3} → [inst : AddMonoid M] → [AddAction M α] → α → AddSubmonoid M
-- Mathlib.Data.Fintype.Defs
List.instDecidableBijOnCoeFinsetOfDecidableEq : {α : Type u_1} →
  {β : Type u_2} → {f : α → β} → {s : Finset α} → {t' : Finset β} → [DecidableEq β] → Decidable (Set.BijOn f ↑s ↑t')