mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.AffineSpace.Basis
/-- In an affine space that is also a vector space, an `AffineBasis` can be scaled.

TODO: generalize to include `SMul (P ≃ᵃ[k] P) (AffineBasis ι k P)`, which acts on `P` with a `VAdd`
version of a `DistribMulAction`.  -/
AffineBasis.instSMul : {ι : Type u_1} →
  {G : Type u_3} →
    {k : Type u_5} →
      {V : Type u_6} →
        [inst : AddCommGroup V] →
          [inst_1 : Ring k] →
            [inst_2 : Module k V] →
              [inst_3 : Group G] → [inst_4 : DistribMulAction G V] → [SMulCommClass G k V] → SMul G (AffineBasis ι k V)
-- Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
isIntegral_iff_isIntegral_closure_finite : ∀ {R : Type u_1} {B : Type u_3} [inst : CommRing R] [inst_1 : Ring B] [inst_2 : Algebra R B] {r : B},
  IsIntegral R r ↔ ∃ s, s.Finite ∧ IsIntegral (↥(Subring.closure s)) r
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup_singleton : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {f : β → α} {b : β}, {b}.sup f = f b
-- Mathlib.Computability.DFA
DFA.evalFrom_of_pow : ∀ {α : Type u} {σ : Type v} (M : DFA α σ) {x y : List α} {s : σ},
  M.evalFrom s x = s → y ∈ KStar.kstar {x} → M.evalFrom s y = s
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.toList_eq_fold : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α m m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β},
  it.toList = Std.IterM.fold (fun l out => l ++ [out]) [] it
-- Mathlib.Algebra.GroupWithZero.Commute
Ring.mul_inverse_rev' : ∀ {M₀ : Type u_1} [inst : MonoidWithZero M₀] {a b : M₀},
  Commute a b → Ring.inverse (a * b) = Ring.inverse b * Ring.inverse a
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Presieve.CoverByImageStructure.fac : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {G : CategoryTheory.Functor C D} {V U : D} {f : V ⟶ U}
  (self : CategoryTheory.Presieve.CoverByImageStructure G f), CategoryTheory.CategoryStruct.comp self.lift self.map = f
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey!_union_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [inst : Inhabited α]
  [Std.TransCmp cmp], t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₂ → (t₁ ∪ t₂).getKey! k = t₁.getKey! k
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
norm_circleMap_zero : ∀ (R θ : ℝ), ‖circleMap 0 R θ‖ = |R|
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.instInhabited : Inhabited MonCat
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.arrow_congr : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : C} (X Y : CategoryTheory.Subobject A) (h : X = Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) Y.arrow = X.arrow
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.instAddCommGroupWithOne : {R : Type uR} →
  {A : Type uA} →
    {B : Type uB} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommGroupWithOne A] →
          [inst_2 : Module R A] →
            [inst_3 : AddCommMonoidWithOne B] → [inst_4 : Module R B] → AddCommGroupWithOne (TensorProduct R A B)
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.comp_id : ∀ {E : Type u_3} [inst : Group E] (p : GroupSeminorm E), p.comp (MonoidHom.id E) = p
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
Std.IterM.toListRev_eq : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α m β]
  [Std.Iterators.Finite α m] {it : Std.IterM m β}, it.toListRev = List.reverse <$> it.toList
-- Mathlib.CategoryTheory.Shift.InducedShiftSequence
CategoryTheory.Functor.ShiftSequence.induced.isoZero_hom_app_obj : ∀ {C : Type u_1} {D : Type u_2} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} A]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor D A} {G : CategoryTheory.Functor C A} (e : L.comp F ≅ G)
  (M : Type u_4) [inst_3 : AddMonoid M] [inst_4 : CategoryTheory.HasShift C M] [inst_5 : G.ShiftSequence M]
  (F' : M → CategoryTheory.Functor D A) (e' : (m : M) → L.comp (F' m) ≅ G.shift m)
  [inst_6 : ((CategoryTheory.Functor.whiskeringLeft C D A).obj L).Full]
  [inst_7 : ((CategoryTheory.Functor.whiskeringLeft C D A).obj L).Faithful] (X : C),
  (CategoryTheory.Functor.ShiftSequence.induced.isoZero e M F' e').hom.app (L.obj X) =
    CategoryTheory.CategoryStruct.comp ((e' 0).hom.app X)
      (CategoryTheory.CategoryStruct.comp ((G.isoShiftZero M).hom.app X) (e.inv.app X))
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
/-- Eta-expanded form of `CurveIntegrable.zero` -/
CurveIntegrable.fun_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b : E} {γ : Path a b},
  CurveIntegrable (fun x => 0) γ
-- Mathlib.Data.ENNReal.Inv
ENNReal.mul_comm_div : ∀ {a b c : ENNReal}, a / b * c = a * (c / b)
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.process : Lean.Expr → Lean.Expr → Lean.Meta.Sym.UnifyM✝ Bool
-- Batteries.Data.List.Lemmas
_private.Batteries.Data.List.Lemmas.0.List.filterMap.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match some b with
    | none => h_1 ()
    | some b => h_2 b) =
    h_2 b
-- Mathlib.Order.Hom.Lattice
InfHom.dual_id : ∀ {α : Type u_2} [inst : Min α], InfHom.dual (InfHom.id α) = SupHom.id αᵒᵈ
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_minKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = false → ∀ {fallback : α}, t.getKey? (t.minKeyD fallback) = some (t.minKeyD fallback)
-- Mathlib.Data.Nat.Prime.Int
Nat.prime_iff_prime_int : ∀ {p : ℕ}, Nat.Prime p ↔ Prime ↑p
-- Mathlib.Order.Hom.Bounded
instCoeTCTopHomOfTopHomClass : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] → [inst_1 : Top α] → [inst_2 : Top β] → [TopHomClass F α β] → CoeTC F (TopHom α β)
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
HurwitzZeta.completedHurwitzZetaEven.eq_1 : ∀ (a : UnitAddCircle) (s : ℂ),
  HurwitzZeta.completedHurwitzZetaEven a s = (HurwitzZeta.hurwitzEvenFEPair a).Λ (s / 2) / 2
-- Mathlib.Order.RelIso.Basic
wellFounded_liftOn₂'_iff : ∀ {α : Type u_1} {s : Setoid α} {r : α → α → Prop} {H : ∀ (a₁ a₂ b₁ b₂ : α), s a₁ b₁ → s a₂ b₂ → r a₁ a₂ = r b₁ b₂},
  (WellFounded fun x y => x.liftOn₂' y r H) ↔ WellFounded r
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.prod_attach_univ : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] [inst_1 : Fintype ι] (f : ↥Finset.univ → M),
  ∏ i ∈ Finset.univ.attach, f i = ∏ i, f ⟨i, ⋯⟩
-- Mathlib.LinearAlgebra.Basis.Defs
/-- Given a basis `v` indexed by `ι`, the canonical linear equivalence between `ι → R` and `M` maps
a function `x : ι → R` to the linear combination `∑_i x i • v i`.  -/
Module.Basis.equivFun_symm_apply : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Fintype ι] (b : Module.Basis ι R M) (x : ι → R), b.equivFun.symm x = ∑ i, x i • b i
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_neg_of_pi_div_two_lt_of_lt : ∀ {x : ℝ}, Real.pi / 2 < x → x < Real.pi + Real.pi / 2 → Real.cos x < 0
-- Init.Data.Nat.Bitwise.Lemmas
Nat.exists_testBit_of_ne_zero : ∀ {x : ℕ}, x ≠ 0 → ∃ i, x.testBit i = true
-- Mathlib.Topology.Instances.TrivSqZeroExt
TrivSqZeroExt.nhds_inl : ∀ {R : Type u_3} {M : Type u_4} [inst : TopologicalSpace R] [inst_1 : TopologicalSpace M] [inst_2 : Zero M] (x : R),
  nhds (TrivSqZeroExt.inl x) = nhds x ×ˢ nhds 0
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.lintegral_gaussianPDF_eq_one : ∀ (μ : ℝ) {v : NNReal}, v ≠ 0 → ∫⁻ (x : ℝ), ProbabilityTheory.gaussianPDF μ v x = 1
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.rankPos_iff_exists_isCocircuit : ∀ {α : Type u_1} {M : Matroid α}, M.RankPos ↔ ∃ K, M.IsCocircuit K
-- Init.Data.SInt.Lemmas
Int16.toISize_ofInt : ∀ {n : ℤ}, Int16.minValue.toInt ≤ n → n ≤ Int16.maxValue.toInt → (Int16.ofInt n).toISize = ISize.ofInt n
-- Mathlib.RingTheory.FractionalIdeal.Extended
FractionalIdeal.extendedHom_le_one_iff : ∀ {A : Type u_1} {K : Type u_2} (L : Type u_3) (B : Type u_4) [inst : CommRing A] [inst_1 : IsDomain A]
  [inst_2 : CommRing B] [inst_3 : IsDomain B] [inst_4 : Algebra A B] [inst_5 : Module.IsTorsionFree A B]
  [inst_6 : Field K] [inst_7 : Field L] [inst_8 : Algebra A K] [inst_9 : Algebra B L] [inst_10 : IsFractionRing A K]
  [inst_11 : IsFractionRing B L] {I : FractionalIdeal (nonZeroDivisors A) K} [inst_12 : Algebra K L]
  [inst_13 : Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsIntegral A B] [IsIntegrallyClosed A]
  [IsIntegrallyClosed B], (FractionalIdeal.extendedHom L B) I ≤ 1 ↔ I ≤ 1
-- Init.Data.List.Basic
List.dropLast.eq_2 : ∀ {α : Type u_1} (head : α), [head].dropLast = []
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.lawfulMonad : ∀ {R : Type u_3} [inst : CommSemiring R], LawfulMonad fun σ => MvPolynomial σ R
-- Mathlib.Data.ENat.Basic
ENat.monotone_map_iff : ∀ {α : Type u_1} {f : ℕ → α} [inst : Preorder α], Monotone (ENat.map f) ↔ Monotone f
-- Mathlib.Algebra.Module.Equiv.Basic
/-- An `R`-linear isomorphism between two `R`-modules `M₂` and `M₃` induces an `S`-linear
isomorphism between `M₂ →ₗ[R] M` and `M₃ →ₗ[R] M`, if `M` is both an `R`-module and an
`S`-module and their actions commute.  -/
LinearEquiv.congrLeft : (M : Type u_5) →
  {M₂ : Type u_7} →
    {M₃ : Type u_8} →
      [inst : AddCommMonoid M] →
        [inst_1 : AddCommMonoid M₂] →
          [inst_2 : AddCommMonoid M₃] →
            {R : Type u_9} →
              (S : Type u_10) →
                [inst_3 : Semiring R] →
                  [inst_4 : Semiring S] →
                    [inst_5 : Module R M₂] →
                      [inst_6 : Module R M₃] →
                        [inst_7 : Module R M] →
                          [inst_8 : Module S M] →
                            [inst_9 : SMulCommClass R S M] → (M₂ ≃ₗ[R] M₃) → (M₂ →ₗ[R] M) ≃ₗ[S] M₃ →ₗ[R] M
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Order.cof_Iio : ∀ {α : Type u} [inst : LinearOrder α] [inst_1 : WellFoundedLT α] (x : α),
  Order.cof ↑(Set.Iio x) = ((Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding x).cof
-- Mathlib.Tactic.ProdAssoc
Lean.Expr.ProdTree.type.sizeOf_spec : ∀ (tp : Lean.Expr) (l : Lean.Level), sizeOf (Lean.Expr.ProdTree.type tp l) = 1 + sizeOf tp + sizeOf l
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.add_lt_add_of_le_of_lt : ∀ {α : Type u} [inst : Add α] {w x y z : WithTop α} [inst_1 : Preorder α] [AddLeftStrictMono α] [AddRightMono α],
  w ≠ ⊤ → w ≤ y → x < z → w + x < y + z
-- Init.Data.BitVec.Lemmas
BitVec.msb_signExtend : ∀ {w v : ℕ} {x : BitVec w}, (BitVec.signExtend v x).msb = (decide (0 < v) && if w ≥ v then x.getMsbD (w - v) else x.msb)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey!.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  (t t_1 : Std.ExtDTreeMap α β cmp), t = t_1 → t.maxKey! = t_1.maxKey!
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.incidenceSetEquivNeighborSet_apply_coe : ∀ {V : Type u} (G : SimpleGraph V) [inst : DecidableEq V] (v : V) (e : ↑(G.incidenceSet v)),
  ↑((G.incidenceSetEquivNeighborSet v) e) = G.otherVertexOfIncident ⋯
-- Init.System.IOError
IO.Error.hardwareFault.sizeOf_spec : ∀ (osCode : UInt32) (details : String),
  sizeOf (IO.Error.hardwareFault osCode details) = 1 + sizeOf osCode + sizeOf details
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.compContinuousLinearMap_apply : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₁' : ι → Type w₁'} {M₄ : Type w₄} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : (i : ι) → AddCommMonoid (M₁' i)] [inst_3 : AddCommMonoid M₄]
  [inst_4 : (i : ι) → Module R (M₁ i)] [inst_5 : (i : ι) → Module R (M₁' i)] [inst_6 : Module R M₄]
  [inst_7 : (i : ι) → TopologicalSpace (M₁ i)] [inst_8 : (i : ι) → TopologicalSpace (M₁' i)]
  [inst_9 : TopologicalSpace M₄] (g : ContinuousMultilinearMap R M₁' M₄) (f : (i : ι) → M₁ i →L[R] M₁' i)
  (m : (i : ι) → M₁ i), (g.compContinuousLinearMap f) m = g fun i => (f i) (m i)
-- Mathlib.Analysis.CStarAlgebra.Basic
toLinearEquiv_starₗᵢ : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : CommSemiring 𝕜] [inst_1 : StarRing 𝕜] [inst_2 : SeminormedAddCommGroup E]
  [inst_3 : StarAddMonoid E] [inst_4 : NormedStarGroup E] [inst_5 : Module 𝕜 E] [inst_6 : StarModule 𝕜 E],
  (starₗᵢ 𝕜).toLinearEquiv = starLinearEquiv 𝕜
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.ofArrows_eq_ofArrows_uncurry : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {ι : Type u_1} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S),
  CategoryTheory.Presieve.ofArrows X f =
    CategoryTheory.Presieve.ofArrows (fun i => X (CategoryTheory.Presieve.ofArrows.idx ⋯)) fun i =>
      f (CategoryTheory.Presieve.ofArrows.idx ⋯)
-- Mathlib.Algebra.Group.Hom.Defs
Monoid.End.eq_1 : ∀ (M : Type u_4) [inst : MulOne M], Monoid.End M = (M →* M)
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.iInf_normalizer_le_normalizer_iSup : ∀ {G : Type u_2} [inst : Group G] {ι : Sort u_5} (H : ι → Subgroup G),
  ⨅ i, Subgroup.normalizer ↑(H i) ≤ Subgroup.normalizer ↑(⨆ i, H i)
-- Mathlib.LinearAlgebra.Determinant
LinearMap.det_toMatrix : ∀ {M : Type u_2} [inst : AddCommGroup M] {ι : Type u_4} [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] {A : Type u_5}
  [inst_3 : CommRing A] [inst_4 : Module A M] (b : Module.Basis ι A M) (f : M →ₗ[A] M),
  ((LinearMap.toMatrix b b) f).det = LinearMap.det f
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RioSliceData : (α : Type u) → [Ord α] → Type u
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.isEmpty_dropWhile_iff_takeWhile_eq_self : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat] {s : String.Slice},
  (s.dropWhile pat).isEmpty = true ↔ s.takeWhile pat = s
-- Mathlib.Order.Bounds.Basic
lowerBounds_mono : ∀ {α : Type u_1} [inst : Preorder α] ⦃s t : Set α⦄, s ⊆ t → ∀ ⦃a b : α⦄, b ≤ a → a ∈ lowerBounds t → b ∈ lowerBounds s
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.isSuccLimit_iff : ∀ {c : Cardinal.{u_1}}, Order.IsSuccLimit c ↔ c ≠ 0 ∧ Order.IsSuccPrelimit c
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Bicategory.LeftAdjoint.mk.injEq : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {a b : B} {right : b ⟶ a} (left : a ⟶ b)
  (adj : CategoryTheory.Bicategory.Adjunction left right) (left_1 : a ⟶ b)
  (adj_1 : CategoryTheory.Bicategory.Adjunction left_1 right),
  ({ left := left, adj := adj } = { left := left_1, adj := adj_1 }) = (left = left_1 ∧ adj ≍ adj_1)
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.instUniqueSubtypeMemBot.eq_1 : ∀ {G : Type u_1} [inst : Group G], Subgroup.instUniqueSubtypeMemBot = { default := 1, uniq := ⋯ }
-- Init.Data.Slice.Array.Iterator
instIteratorSubarrayIteratorId.eq_1 : ∀ {α : Type u},
  instIteratorSubarrayIteratorId =
    { IsPlausibleStep := fun it step => step = SubarrayIterator.step it,
      step := fun it => pure (Std.Shrink.deflate ⟨SubarrayIterator.step it, ⋯⟩) }
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey_insertMany_list_of_mem : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {l : List (α × β)} {k k' : α},
  compare k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬compare a.1 b.1 = Ordering.eq) l →
      k ∈ List.map Prod.fst l →
        ∀ {h' : Std.DTreeMap.Internal.Impl.contains k' ↑(Std.DTreeMap.Internal.Impl.Const.insertMany t l ⋯) = true},
          (↑(Std.DTreeMap.Internal.Impl.Const.insertMany t l ⋯)).getKey k' h' = k
-- Mathlib.AlgebraicGeometry.Morphisms.Constructors
/-- If `P` respects isos, then `stalkwise P` respects isos.  -/
AlgebraicGeometry.stalkwise_respectsIso : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P) →
    (AlgebraicGeometry.stalkwise fun {R S} [CommRing R] [CommRing S] => P).RespectsIso
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getD_alter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' : α} {fallback : β} {f : Option β → Option β},
  Std.ExtDHashMap.Const.getD (Std.ExtDHashMap.Const.alter m k f) k' fallback =
    if (k == k') = true then (f (Std.ExtDHashMap.Const.get? m k)).getD fallback
    else Std.ExtDHashMap.Const.getD m k' fallback
-- Mathlib.AlgebraicGeometry.Cover.Sigma
/-- A refinement of coverings induces a refinement on the single object coverings.  -/
AlgebraicGeometry.Scheme.Cover.Hom.sigma : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  {S : AlgebraicGeometry.Scheme} →
    [inst : AlgebraicGeometry.IsZariskiLocalAtSource P] →
      [inst_1 : UnivLE.{v, u}] →
        {𝒰 𝒱 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) S} →
          (𝒰 ⟶ 𝒱) → (𝒰.sigma ⟶ 𝒱.sigma)
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.norm_le_of_ae_bound : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [MeasureTheory.IsFiniteMeasure μ] {f : ↥(MeasureTheory.Lp E p μ)} {C : ℝ},
  0 ≤ C → (∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ C) → ‖f‖ ≤ ↑(MeasureTheory.measureUnivNNReal μ) ^ p.toReal⁻¹ * C
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
TopPair.HomologyPretheory.iso_homₚ_inv_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {HP HP' : TopPair.HomologyPretheory C c} (f : HP ⟶ HP') (i : ι),
  CategoryTheory.CategoryStruct.comp (HP.iso i).hom
      (CategoryTheory.CategoryStruct.comp (TopPair.incl.whiskerLeft (f.homₚ i)) (HP'.iso i).inv) =
    f.hom i
-- Batteries.Data.List.Lemmas
_private.Batteries.Data.List.Lemmas.0.List.insertP.loop.match_1.splitter : {α : Type u_1} →
  (motive : List α → List α → Sort u_2) →
    (x x_1 : List α) → ((r : List α) → motive [] r) → ((b : α) → (l r : List α) → motive (b :: l) r) → motive x x_1
-- Mathlib.Data.Fintype.Card
Fintype.card_plift : ∀ (α : Type u_4) [inst : Fintype α], Fintype.card (PLift α) = Fintype.card α
-- Init.Data.BitVec.Lemmas
BitVec.setWidth_shiftLeft_of_le : ∀ {w i : ℕ} {x : BitVec w} {y : ℕ}, i ≤ w → BitVec.setWidth i (x <<< y) = BitVec.setWidth i x <<< y
-- Mathlib.Data.Finsupp.Defs
Finsupp.onFinset_support : ∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] (f : α →₀ M), Finsupp.onFinset f.support ⇑f ⋯ = f
-- Std.Http.Internal.IndexMultiMap
Std.Internal.IndexMultiMap.instSingletonProdOfEquivBEqOfLawfulHashable : {α : Type u} →
  {β : Type v} →
    [inst : BEq α] →
      [inst_1 : Hashable α] → [EquivBEq α] → [LawfulHashable α] → Singleton (α × β) (Std.Internal.IndexMultiMap α β)
-- Mathlib.Algebra.CharP.Lemmas
add_pow_eq_mul_pow_add_pow_div_expChar : ∀ {R : Type u_1} [inst : CommSemiring R] (x y : R) (p n : ℕ) [hR : ExpChar R p],
  (x + y) ^ n = (x + y) ^ (n % p) * (x ^ p + y ^ p) ^ (n / p)
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.ι_mapBifunctorComp₁₂MapObjIso_hom : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C₁₂] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
  (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9}
  {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r)
  (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂)
  (X₃ : CategoryTheory.GradedObject I₃ C₃)
  [inst_5 : (((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
  [inst_6 :
    (((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj
              (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj
          X₃).HasMap
      ρ₁₂.q]
  [H : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃]
  [inst_7 :
    ((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj
          X₃).HasMap
      r]
  (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.ιMapTrifunctorMapObj (CategoryTheory.bifunctorComp₁₂ F₁₂ G) r X₁ X₂ X₃ i₁ i₂ i₃ j h)
      ((CategoryTheory.GradedObject.mapBifunctorComp₁₂MapObjIso F₁₂ G ρ₁₂ X₁ X₂ X₃).hom j) =
    CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.eq_iff : ∀ {G : Type u_1} [inst : Group G] {M : Type u_7} [inst_1 : MulOneClass M] (f : G →* M) {x y : G},
  f x = f y ↔ y⁻¹ * x ∈ f.ker
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_le_size_alter : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {k : α} {f : Option (β k) → Option (β k)},
  t.size - 1 ≤ (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl.size
-- Init.Data.Nat.Bitwise.Basic
Nat.instAndOp : AndOp ℕ
-- Std.Time.Zoned.Database.TzIf
_private.Std.Time.Zoned.Database.TzIf.0.Std.Time.TimeZone.TZif.parseIndicators : UInt32 → Std.Internal.Parsec.ByteArray.Parser (Array Bool)
-- Mathlib.Algebra.Algebra.Basic
IsScalarTower.to_smulCommClass' : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : Algebra R A] {M : Type u_3}
  [inst_3 : AddCommMonoid M] [inst_4 : Module A M] [inst_5 : Module R M] [IsScalarTower R A M], SMulCommClass A R M
-- Mathlib.Data.Sign.Defs
SignType.cast.eq_3 : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : One α] [inst_2 : Neg α], ↑SignType.neg = -1
-- Mathlib.Control.Basic
/-- The monadic `bind` operation for `Sum`.  -/
Sum.bind : {e : Type v} → {α : Type u_1} → {β : Type u_2} → e ⊕ α → (α → e ⊕ β) → e ⊕ β
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Line.instInhabitedAlmostMonoDefaultOfNonempty : {α : Type u_5} →
  {ι : Type u_6} →
    {κ : Type u_7} → [Nonempty ι] → [inst : Inhabited κ] → Inhabited (Combinatorics.Line.AlmostMono fun x => default)
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
/-- The `Equiv` that witnesses that `pullbackCone f g pb` is actually a pullback. This is the
universal property of pullbacks.  -/
CategoryTheory.Limits.FormalCoproduct.homPullbackEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : CategoryTheory.Limits.FormalCoproduct C} →
      (f : X ⟶ Z) →
        (g : Y ⟶ Z) →
          (pb :
              (i : Function.Pullback f.f g.f) →
                CategoryTheory.Limits.PullbackCone
                  (CategoryTheory.CategoryStruct.comp (f.φ (↑i).1) (CategoryTheory.eqToHom ⋯)) (g.φ (↑i).2)) →
            ((i : Function.Pullback f.f g.f) → CategoryTheory.Limits.IsLimit (pb i)) →
              (T : CategoryTheory.Limits.FormalCoproduct C) →
                (T ⟶ (CategoryTheory.Limits.FormalCoproduct.pullbackCone f g pb).pt) ≃
                  { p // CategoryTheory.CategoryStruct.comp p.1 f = CategoryTheory.CategoryStruct.comp p.2 g }