mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
circleMap_mem_closedBall : ∀ (c : ℂ) {R : ℝ}, 0 ≤ R → ∀ (θ : ℝ), circleMap c R θ ∈ Metric.closedBall c R
-- Mathlib.NumberTheory.ModularForms.SlashActions
/-- Variant of `is_invariant_one` with the left-hand side in simp normal form.  -/
ModularForm.is_invariant_one' : ∀ (A : Matrix.SpecialLinearGroup (Fin 2) ℤ),
  SlashAction.map 0 (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) A)) 1 = 1
-- Mathlib.Order.Filter.Basic
/-- Eta-expanded form of `Filter.EventuallyEq.inv` -/
Filter.EventuallyEq.fun_inv : ∀ {α : Type u} {β : Type v} [inst : Inv β] {f g : α → β} {l : Filter α},
  f =ᶠ[l] g → (fun i => (f i)⁻¹) =ᶠ[l] fun i => (g i)⁻¹
-- Mathlib.Order.Heyting.Basic
GeneralizedHeytingAlgebra.toDistribLattice : {α : Type u_2} → [GeneralizedHeytingAlgebra α] → DistribLattice α
-- Mathlib.CategoryTheory.Groupoid
CategoryTheory.Groupoid.invEquivalence_inverse_map : ∀ (C : Type u) [inst : CategoryTheory.Groupoid C] {x y : Cᵒᵖ} (f : x ⟶ y),
  (CategoryTheory.Groupoid.invEquivalence C).inverse.map f = CategoryTheory.Groupoid.inv f.unop
-- Init.System.Promise
_private.Init.System.Promise.0.IO.Promise.prom : {α : Type} → IO.Promise α → IO.PromisePointed✝.type
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.forIn_eq_forIn_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} {δ : Type w} {m : Type w → Type w'} [inst : Monad m]
  [LawfulMonad m] {f : α → δ → m (ForInStep δ)} {init : δ}, forIn t init f = forIn t.toList init f
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem!_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    ∀ {v : β} [inst_1 : Inhabited β],
      List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l → (k, v) ∈ l → (t.insertMany l)[k']! = v
-- Mathlib.Data.Matrix.Mul
Matrix.neg_mulVec : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalNonAssocRing α] [inst_1 : Fintype n] (v : n → α)
  (A : Matrix m n α), (-A).mulVec v = -A.mulVec v
-- Init.Data.List.Lemmas
List.foldl_filter : ∀ {α : Type u_1} {β : Type u_2} {p : α → Bool} {f : β → α → β} {l : List α} {init : β},
  List.foldl f init (List.filter p l) = List.foldl (fun x y => if p y = true then f x y else x) init l
-- Mathlib.Data.Part
Part.map_none : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), Part.map f Part.none = Part.none
-- Mathlib.CategoryTheory.Subfunctor.Basic
CategoryTheory.Subfunctor.min_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)}
  (S T : CategoryTheory.Subfunctor F) (i : C), (S ⊓ T).obj i = S.obj i ∩ T.obj i
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.preimage_basicOpen : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] {𝒜 : ℕ → σ}
  [inst_3 : GradedRing 𝒜] (f : A) (z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)),
  AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.toFun f ⁻¹'
      ↑(PrimeSpectrum.basicOpen (HomogeneousLocalization.mk z)) =
    Subtype.val ⁻¹' ↑(ProjectiveSpectrum.basicOpen 𝒜 ↑z.num)
-- Init.SizeOf
Unit.sizeOf : ∀ (u : Unit), sizeOf u = 1
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- The underlying set of configurations.  -/
SymbolicDynamics.FullShift.MulSubshift.carrier : {A : Type u_1} →
  [inst : TopologicalSpace A] →
    {G : Type u_2} → [inst_1 : Monoid G] → SymbolicDynamics.FullShift.MulSubshift A G → Set (G → A)
-- Mathlib.SetTheory.Ordinal.Veblen
/-- `veblen o₁ a ≤ veblen o₂ b` iff one of the following holds:
* `o₁ = o₂` and `a = b`
* `o₁ < o₂` and `a = veblen o₂ b`
* `o₁ > o₂` and `veblen o₁ a = b`  -/
Ordinal.veblen_eq_veblen_iff : ∀ {o₁ o₂ a b : Ordinal.{u}},
  Ordinal.veblen o₁ a = Ordinal.veblen o₂ b ↔
    o₁ = o₂ ∧ a = b ∨ o₁ < o₂ ∧ a = Ordinal.veblen o₂ b ∨ o₂ < o₁ ∧ Ordinal.veblen o₁ a = b
-- Mathlib.Algebra.GCDMonoid.Basic
gcd_zero_right' : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] (a : α), Associated (gcd a 0) a
-- Mathlib.Data.Part
Part.div_def : ∀ {α : Type u_1} [inst : Div α] (a b : Part α),
  a / b = do
    let y ← a
    Part.map (fun x => y / x) b
-- Mathlib.Algebra.Lie.Basic
LieModuleHom.instModule : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      {N : Type w₁} →
        [inst : CommRing R] →
          [inst_1 : LieRing L] →
            [inst_2 : AddCommGroup M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : LieRingModule L M] →
                      [inst_7 : LieRingModule L N] →
                        [inst_8 : LieAlgebra R L] → [LieModule R L N] → Module R (M →ₗ⁅R,L⁆ N)
-- Mathlib.Combinatorics.SimpleGraph.Sum
/-- Disjoint sum of `G` and `H`.  -/
SimpleGraph.sum : {V : Type u_3} → {W : Type u_5} → SimpleGraph V → SimpleGraph W → SimpleGraph (V ⊕ W)
-- Mathlib.LinearAlgebra.TensorProduct.Basic
TensorProduct.CompatibleSMul.unit : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} {N : Type u_3} [inst_1 : AddCommGroup M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] {S : Type u_7} [inst_5 : Monoid S]
  [inst_6 : DistribMulAction S M] [inst_7 : DistribMulAction S N] [TensorProduct.CompatibleSMul R S M N],
  TensorProduct.CompatibleSMul R Sˣ M N
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.entryAtIdx!_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited (α × β)] {i : ℕ}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.entryAtIdx! i = t₂.entryAtIdx! i
-- Mathlib.Topology.Algebra.Group.SubmonoidClosure
topologicalClosure_subgroupClosure_toSubmonoid : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [CompactSpace G] [inst_3 : IsTopologicalGroup G]
  (s : Set G), (Subgroup.closure s).topologicalClosure = (Submonoid.closure s).topologicalClosure
-- Mathlib.Analysis.Normed.Group.Pointwise
singleton_sub_closedBall : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (δ : ℝ) (x y : E),
  {x} - Metric.closedBall y δ = Metric.closedBall (x - y) δ
-- Init.Data.BitVec.Lemmas
BitVec.not_allOnes : ∀ {w : ℕ}, ~~~BitVec.allOnes w = 0#w
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblenWith_lt_veblenWith_iff_right : ∀ {f : Ordinal.{u} → Ordinal.{u}} {o a b : Ordinal.{u}},
  Order.IsNormal f → (Ordinal.veblenWith f o a < Ordinal.veblenWith f o b ↔ a < b)
-- Mathlib.Data.Fintype.BigOperators
Fintype.sum_sumElim : ∀ {α₁ : Type u_4} {α₂ : Type u_5} {M : Type u_6} [inst : Fintype α₁] [inst_1 : Fintype α₂] [inst_2 : AddCommMonoid M]
  (f : α₁ → M) (g : α₂ → M), ∑ x, Sum.elim f g x = ∑ a₁, f a₁ + ∑ a₂, g a₂
-- Batteries.Lean.MonadBacktrack
/-- Execute the action `x`, then restore the initial state. Returns the state after
`x` finished.
 -/
Lean.withoutModifyingState' : {m : Type → Type} → {s α : Type} → [Monad m] → [Lean.MonadBacktrack s m] → [MonadFinally m] → m α → m (α × s)
-- Mathlib.Algebra.Colimit.Module
Module.DirectLimit.linearEquiv_symm_mk : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_2} [inst_1 : Preorder ι] (G : ι → Type u_3)
  [inst_2 : (i : ι) → AddCommMonoid (G i)] [inst_3 : (i : ι) → Module R (G i)] (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j)
  [inst_4 : DecidableEq ι] [inst_5 : Nonempty ι] [inst_6 : IsDirectedOrder ι]
  [inst_7 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] {g : (i : ι) × G i},
  (Module.DirectLimit.linearEquiv G f).symm ⟦g⟧ = (Module.DirectLimit.of R ι G f g.fst) g.snd
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.comp_assoc : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [inst : Max α] [inst_1 : Bot α] [inst_2 : Max β]
  [inst_3 : Bot β] [inst_4 : Max γ] [inst_5 : Bot γ] [inst_6 : Max δ] [inst_7 : Bot δ] (f : SupBotHom γ δ)
  (g : SupBotHom β γ) (h : SupBotHom α β), (f.comp g).comp h = f.comp (g.comp h)
-- Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
_private.Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections.0.TopCat.Presheaf.SheafCondition.pairwiseToOpensLeCoverObj.match_1.splitter : {ι : Type u_1} →
  (motive : CategoryTheory.Pairwise ι → Sort u_2) →
    (x : CategoryTheory.Pairwise ι) →
      ((i : ι) → motive (CategoryTheory.Pairwise.single i)) →
        ((i j : ι) → motive (CategoryTheory.Pairwise.pair i j)) → motive x
-- Mathlib.Analysis.Calculus.DifferentialForm.Basic
extDerivWithin.eq_1 : ∀ {𝕜 : 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] {n : ℕ}
  (ω : E → E [⋀^Fin n]→L[𝕜] F) (s : Set E) (x : E),
  extDerivWithin ω s x = ContinuousAlternatingMap.alternatizeUncurryFin (fderivWithin 𝕜 ω s x)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyGT?_eq_getEntryGT? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α β} {k : α},
  Std.DTreeMap.Internal.Impl.getKeyGT? k t = Option.map (fun x => x.fst) (Std.DTreeMap.Internal.Impl.getEntryGT? k t)
-- Mathlib.Tactic.DefEqTransformations
/-- `whnf at loc` puts the given location into weak-head normal form.
This also exists as a `conv`-mode tactic.

Weak-head normal form is when the outer-most expression has been fully reduced, the expression
may contain subexpressions which have not been reduced.
 -/
Mathlib.Tactic.tacticWhnf__ : Lean.ParserDescr
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.descFunLift.eq_2 : ∀ {J : Type v} [inst : CategoryTheory.Category.{u, v} J] (F : CategoryTheory.Functor J MonCat)
  (s : CategoryTheory.Limits.Cocone F), MonCat.Colimits.descFunLift F s MonCat.Colimits.Prequotient.one = 1
-- Mathlib.Algebra.Lie.TensorProduct
LieModule.toModuleHom_apply : ∀ (R : Type u) [inst : CommRing R] (L : Type v) (M : Type w) [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M] (x : L)
  (m : M), (LieModule.toModuleHom R L M) (x ⊗ₜ[R] m) = ⁅x, m⁆
-- Mathlib.SetTheory.ZFC.Cardinal
ZFSet.card_singleton : ∀ {x : ZFSet.{u}}, {x}.card = 1
-- Mathlib.Data.Finsupp.NeLocus
/-- Given two finitely supported functions `f g : α →₀ N`, `Finsupp.neLocus f g` is the `Finset`
where `f` and `g` differ. This generalizes `(f - g).support` to situations without subtraction.  -/
Finsupp.neLocus : {α : Type u_1} → {N : Type u_3} → [DecidableEq α] → [DecidableEq N] → [inst : Zero N] → (α →₀ N) → (α →₀ N) → Finset α
-- Init.Data.Array.Lemmas
Array.back_pop : ∀ {α : Type u_1} {xs : Array α} (h : 0 < xs.pop.size), xs.pop.back h = xs[xs.size - 2]
-- Mathlib.Data.List.Cycle
Cycle.prev_mem : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Cycle α) (hs : s.Nodup) (x : α) (hx : x ∈ s), s.prev hs x hx ∈ s
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.instRankPosOfNonemptyOfLoopless : ∀ {α : Type u_1} {M : Matroid α} [M.Nonempty] [M.Loopless], M.RankPos
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.mkOfHomEquiv_counit_app : ∀ {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 : CategoryTheory.Adjunction.CoreHomEquiv F G)
  (Y : D),
  (CategoryTheory.Adjunction.mkOfHomEquiv adj).counit.app Y =
    (adj.homEquiv (G.obj Y) Y).symm (CategoryTheory.CategoryStruct.id (G.obj Y))
-- Mathlib.Data.Nat.Factorization.Basic
Nat.factorization_div : ∀ {d n : ℕ}, d ∣ n → (n / d).factorization = n.factorization - d.factorization
-- Init.Data.Array.Lemmas
Array.extract_loop_succ : ∀ {α : Type u_1} {xs ys : Array α} {size start : ℕ} (h : start < xs.size),
  Array.extract.loop xs (size + 1) start ys = Array.extract.loop xs size (start + 1) (ys.push xs[start])
-- Mathlib.Order.LiminfLimsup
Filter.Tendsto.liminf_le_liminf_comp : ∀ {ι : Type u_6} {α : Type u_7} {β : Type u_8} [inst : ConditionallyCompleteLattice β] {v : ι → α} {u : α → β}
  {f : Filter ι} {g : Filter α},
  Filter.Tendsto v f g →
    autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) (Filter.map v f) u)
        Filter.Tendsto.liminf_le_liminf_comp._auto_1 →
      autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) g u) Filter.Tendsto.liminf_le_liminf_comp._auto_3 →
        Filter.liminf u g ≤ Filter.liminf (u ∘ v) f
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- An arrow in bind has the form `A ⟶ B ⟶ X` where `A ⟶ B` is an arrow in `T I` for some `I`.
and `B ⟶ X` is an arrow of `S`. This is the hom `A ⟶ B`, as an arrow.  -/
CategoryTheory.GrothendieckTopology.Cover.Arrow.toMiddle : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {X : C} → {S : J.Cover X} → {T : (I : S.Arrow) → J.Cover I.Y} → (I : (S.bind T).Arrow) → (T I.fromMiddle).Arrow
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.isOpen_compl_image_coe : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsOpen (OnePoint.some '' s)ᶜ ↔ IsClosed s ∧ IsCompact s
-- Aesop.Script.Step
Aesop.Script.LazyStep.preGoal : Aesop.Script.LazyStep → Lean.MVarId
-- Mathlib.Order.WithBot
WithTop.untop_lt_iff : ∀ {α : Type u_1} {a : α} [inst : LT α] {x : WithTop α} (hx : x ≠ ⊤), x.untop hx < a ↔ x < ↑a
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKey!_modify_self : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp}
  [inst : Inhabited α] {k : α} {f : β → β}, (Std.DTreeMap.Const.modify t k f).getKey! k = if k ∈ t then k else default
-- Mathlib.RingTheory.Valuation.Integers
Valuation.Integers.valuation_irreducible_pos : ∀ {F : Type u} {Γ₀ : Type v} [inst : Field F] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {v : Valuation F Γ₀}
  {O : Type w} [inst_2 : CommRing O] [inst_3 : Algebra O F],
  v.Integers O → ∀ {ϖ : O}, Irreducible ϖ → 0 < v ((algebraMap O F) ϖ)
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.mul_def : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : Add M] (x y : AddMonoidAlgebra R M),
  x * y = x.coeff.sum fun m₁ r₁ => y.coeff.sum fun m₂ r₂ => AddMonoidAlgebra.single (m₁ + m₂) (r₁ * r₂)
-- Mathlib.LinearAlgebra.Contraction
rTensorHomEquivHomRTensor.eq_1 : ∀ (R : Type u_2) (M : Type u_3) (P : Type u_5) (Q : Type u_6) [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid P] [inst_3 : AddCommMonoid Q] [inst_4 : Module R M] [inst_5 : Module R P]
  [inst_6 : Module R Q] [inst_7 : Module.Projective R M] [inst_8 : Module.Finite R M],
  rTensorHomEquivHomRTensor R M P Q =
    ((TensorProduct.congr (dualTensorHomEquiv R M P).symm (LinearEquiv.refl R Q)).trans
          (TensorProduct.assoc R (Module.Dual R M) P Q)).trans
      (dualTensorHomEquiv R M (TensorProduct R P Q))
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.AccLevelState.mk : Lean.LevelMap ℤ → Lean.Elab.Command.AccLevelState✝
-- Mathlib.CategoryTheory.Triangulated.Opposite.Triangle
CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso_inv_app_hom₂ : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  (X : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ),
  ((CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso C).inv.app X).hom₂ =
    CategoryTheory.CategoryStruct.id X.obj₂
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.Prototile.mk.injEq : ∀ {G : Type u_1} {X : Type u_2} [inst : Group G] [inst_1 : MulAction G X] (carrier : Set X)
  (symmetries : Subgroup ↥(MulAction.stabilizer G carrier)) (carrier_1 : Set X)
  (symmetries_1 : Subgroup ↥(MulAction.stabilizer G carrier_1)),
  ({ carrier := carrier, symmetries := symmetries } = { carrier := carrier_1, symmetries := symmetries_1 }) =
    (carrier = carrier_1 ∧ symmetries ≍ symmetries_1)
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.MutualClosure.FixPoint.modifyUsedFVars : (Lean.Elab.Term.MutualClosure.UsedFVarsMap → Lean.Elab.Term.MutualClosure.UsedFVarsMap) →
  Lean.Elab.Term.MutualClosure.FixPoint.M Unit
-- Lean.Data.Lsp.Workspace
Lean.Lsp.FileSystemWatcher.create : ℕ
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.induction_on : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {motive : AddMonoid.Coprod M N → Prop}
  (m : AddMonoid.Coprod M N),
  (∀ (m : M), motive (AddMonoid.Coprod.inl m)) →
    (∀ (n : N), motive (AddMonoid.Coprod.inr n)) →
      (∀ (x y : AddMonoid.Coprod M N), motive x → motive y → motive (x + y)) → motive m
-- Mathlib.Data.ENNReal.Operations
ENNReal.toReal_sub_of_le : ∀ {a b : ENNReal}, b ≤ a → a ≠ ⊤ → (a - b).toReal = a.toReal - b.toReal
-- Mathlib.Algebra.BigOperators.Fin
/-- **Alias** of `List.alternatingProd_eq_finsetProd`. -/
List.alternatingProd_eq_finset_prod : ∀ {G : Type u_3} [inst : DivisionCommMonoid G] (L : List G), L.alternatingProd = ∏ i, L[i] ^ (-1) ^ ↑i
-- Mathlib.CategoryTheory.MorphismProperty.LocalClosure
CategoryTheory.MorphismProperty.sourceLocalClosure.sourceLocalClosure_iff_of_respectsLeft : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C}
  {P : CategoryTheory.MorphismProperty C} [P.RespectsIso] [P.RespectsLeft K.morphismProperty] [K.HasIsos]
  [K.IsStableUnderBaseChange] [K.IsStableUnderComposition] [K.HasPullbacks] {X Y : C} {f : X ⟶ Y},
  CategoryTheory.MorphismProperty.sourceLocalClosure K P f ↔
    ∃ R ∈ K.coverings X, ∀ (U : C) (g : U ⟶ X), R g → P (CategoryTheory.CategoryStruct.comp g f)
-- Mathlib.Data.List.Defs
/-- Right-biased version of `List.map₂`. `map₂Right' f as bs` applies `f` to each
pair of elements `aᵢ ∈ as` and `bᵢ ∈ bs`. If `as` is shorter than `bs`, `f` is
applied to `none` for the remaining `bᵢ`. Returns the results of the `f`
applications and the remaining `as`.

```
map₂Right' prod.mk [1] ['a', 'b'] = ([(some 1, 'a'), (none, 'b')], [])

map₂Right' prod.mk [1, 2] ['a'] = ([(some 1, 'a')], [2])
```
 -/
List.map₂Right' : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → (Option α → β → γ) → List α → List β → List γ × List α
-- Mathlib.LinearAlgebra.Matrix.Circulant
Matrix.Fin.transpose_circulant : ∀ {α : Type u_1} {n : ℕ} (v : Fin n → α), (Matrix.circulant v).transpose = Matrix.circulant fun i => v (-i)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get?_insertMany_emptyWithCapacity_list_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k : α},
  (List.map Prod.fst l).contains k = false →
    Std.DHashMap.Internal.Raw₀.Const.get?
        (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)) k =
      none
-- Mathlib.Algebra.Group.WithOne.Basic
WithZero.mapAddHom.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Add α] [inst_1 : Add β] (f : α →ₙ+ β),
  WithZero.mapAddHom f = WithZero.lift (WithZero.coeAddHom.comp f)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.iSup_approx_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace β] [inst_2 : CompleteLattice β]
  [OrderClosedTopology β] [inst_4 : Zero β] [inst_5 : MeasurableSpace β] [OpensMeasurableSpace β] (i : ℕ → β)
  (f : α → β) (a : α),
  Measurable f → 0 = ⊥ → ⨆ n, (MeasureTheory.SimpleFunc.approx i f n) a = ⨆ k, ⨆ (_ : i k ≤ f a), i k
-- Mathlib.Order.SuccPred.Archimedean
/-- A `PredOrder` is pred-archimedean if one can go from any two comparable elements by iterating
`pred`  -/
IsPredArchimedean : (α : Type u_3) → [inst : Preorder α] → [PredOrder α] → Prop
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.HomotopicWith.symm : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {P : C(X, Y) → Prop}
  ⦃f g : C(X, Y)⦄, f.HomotopicWith g P → g.HomotopicWith f P
-- Mathlib.Data.Set.Lattice
Set.iInter_ite : ∀ {α : Type u_1} {ι : Sort u_5} (p : ι → Prop) [inst : DecidablePred p] (f g : ι → Set α),
  (⋂ i, if p i then f i else g i) = (⋂ i, ⋂ (_ : p i), f i) ∩ ⋂ i, ⋂ (_ : ¬p i), g i
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.smul_fst : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A] {S : Type u_3}
  [inst_5 : Monoid S] [inst_6 : DistribMulAction S A] [inst_7 : SMulCommClass 𝕜 S A] [inst_8 : ContinuousConstSMul S A]
  [inst_9 : IsScalarTower S A A] [inst_10 : SMulCommClass S A A] (s : S) (a : DoubleCentralizer 𝕜 A),
  (s • a).toProd.1 = s • a.toProd.1
-- Mathlib.RingTheory.Congruence.Hom
RingCon.congrₐ_mk : ∀ {M : Type u_1} {N : Type u_2} {R : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring M] [inst_2 : Algebra R M]
  [inst_3 : Semiring N] [inst_4 : Algebra R N] {c : RingCon M} {d : RingCon N} (e : M ≃ₐ[R] N) (h : c = d.comap e)
  (a : M), (RingCon.congrₐ R e h) ↑a = ↑(e a)
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop.0.Std.IterM.forIn'_eq_match_step.match_1.eq_1 : ∀ {γ : Type u_1} (motive : ForInStep γ → Sort u_2) (c : γ) (h_1 : (c : γ) → motive (ForInStep.yield c))
  (h_2 : (c : γ) → motive (ForInStep.done c)),
  (match ForInStep.yield c with
    | ForInStep.yield c => h_1 c
    | ForInStep.done c => h_2 c) =
    h_1 c
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
/-- **Alias** of `LinearMap.BilinForm.toMatrix_comp`. -/
BilinForm.toMatrix_comp : ∀ {R₁ : Type u_1} {M₁ : Type u_2} [inst : CommSemiring R₁] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R₁ M₁]
  {n : Type u_5} {o : Type u_6} [inst_3 : Fintype n] [inst_4 : Fintype o] [inst_5 : DecidableEq n]
  (b : Module.Basis n R₁ M₁) {M₂' : Type u_7} [inst_6 : AddCommMonoid M₂'] [inst_7 : Module R₁ M₂']
  (c : Module.Basis o R₁ M₂') [inst_8 : DecidableEq o] (B : LinearMap.BilinForm R₁ M₁) (l r : M₂' →ₗ[R₁] M₁),
  (LinearMap.BilinForm.toMatrix c) (B.comp l r) =
    ((LinearMap.toMatrix c b) l).transpose * (LinearMap.BilinForm.toMatrix b) B * (LinearMap.toMatrix c b) r
-- Mathlib.Control.Functor
Functor.Comp.run_map : ∀ {F : Type u → Type w} {G : Type v → Type u} [inst : Functor F] [inst_1 : Functor G] {α β : Type v} (h : α → β)
  (x : Functor.Comp F G α), (h <$> x).run = (fun x => h <$> x) <$> x.run
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.card_neighborSet_toSubgraph : ∀ {V : Type u} (G H : SimpleGraph V) (h : H ≤ G) (v : V) [inst : Fintype ↑((SimpleGraph.toSubgraph H h).neighborSet v)]
  [inst_1 : Fintype ↑(H.neighborSet v)], Fintype.card ↑((SimpleGraph.toSubgraph H h).neighborSet v) = H.degree v
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.sup_le : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {a b c : CauSeq α abs},
  a ≤ c → b ≤ c → a ⊔ b ≤ c
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.add_of_Y_ne : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} [inst_1 : DecidableEq F] {x₁ x₂ y₁ y₂ : F}
  {h₁ : W.Nonsingular x₁ y₁} {h₂ : W.Nonsingular x₂ y₂} (hy : y₁ ≠ W.negY x₂ y₂),
  WeierstrassCurve.Affine.Point.some x₁ y₁ h₁ + WeierstrassCurve.Affine.Point.some x₂ y₂ h₂ =
    WeierstrassCurve.Affine.Point.some (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂)) ⋯
-- Mathlib.CategoryTheory.Monad.Comonadicity
CategoryTheory.Comonad.ComonadicityInternal.instHasLimitWalkingParallelPairParallelPairMapAppUnitObjOfHasEqualizerAA : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G)
  [∀ (A : adj.toComonad.Coalgebra), CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] (B : C),
  CategoryTheory.Limits.HasLimit
    (CategoryTheory.Limits.parallelPair (G.map (F.map (adj.unit.app B))) (adj.unit.app (G.obj (F.obj B))))