mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.PontryaginDual
PontryaginDual.map_apply : ∀ {A : Type u_1} {B : Type u_2} [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] (f : A →ₜ* B) (x : PontryaginDual B) (y : A), ((PontryaginDual.map f) x) y = x (f y)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.filtration_monotone : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] (f : P.RankFunction ι),
  Monotone f.filtration
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.instNSMul.eq_1 : ∀ {α : Type u} {R : Type u_2} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace R] [inst_2 : AddMonoid R]
  [inst_3 : BoundedAdd R] [inst_4 : ContinuousAdd R],
  BoundedContinuousFunction.instNSMul =
    { smul := fun n f => { toFun := fun x => n • f x, continuous_toFun := ⋯, map_bounded' := ⋯ } }
-- Init.Data.SInt.Lemmas
Int16.ofIntTruncate_int8ToInt : ∀ (x : Int8), Int16.ofIntClamp x.toInt = x.toInt16
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullbackCone.reindex_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_2} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X}
  (s : CategoryTheory.Limits.WidePullbackCone f) {ι' : Type u_3} (e : ι' ≃ ι), (s.reindex e).pt = s.pt
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.Extension.Entry.name : Lean.Meta.Match.Extension.Entry → Lean.Name
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.instMonoNegHom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {P Q : C} {f : P ⟶ Q}
  [CategoryTheory.Mono f], CategoryTheory.Mono (-f)
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.AddConstAsyncResult.allRealizationsPromise : Lean.Environment.AddConstAsyncResult → IO.Promise (Lean.NameMap Lean.AsyncConst✝)
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.superpose_head_idempotent.injEq : ∀ (x : Lean.Grind.AC.Var) (c₁ : Lean.Meta.Grind.AC.EqCnstr) (x_1 : Lean.Grind.AC.Var)
  (c₁_1 : Lean.Meta.Grind.AC.EqCnstr),
  (Lean.Meta.Grind.AC.EqCnstrProof.superpose_head_idempotent x c₁ =
      Lean.Meta.Grind.AC.EqCnstrProof.superpose_head_idempotent x_1 c₁_1) =
    (x = x_1 ∧ c₁ = c₁_1)
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
GradedTensorProduct.algebraMap_def : ∀ {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring ι] [inst_1 : DecidableEq ι]
  [inst_2 : CommRing R] [inst_3 : Ring A] [inst_4 : Ring B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ]
  [inst_9 : Module ι (Additive ℤˣ)] (r : R), (algebraMap R (GradedTensorProduct R 𝒜 ℬ)) r = (algebraMap R A) r ᵍ⊗ₜ[R] 1
-- Init.Data.Fin.Lemmas
Fin.fin_two_eq_of_eq_zero_iff : ∀ {a b : Fin 2}, (a = 0 ↔ b = 0) → a = b
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- `L` with the spectral norm is a `NontriviallyNormedField`.  -/
spectralNorm.nontriviallyNormedField : (K : Type u) →
  [inst : NontriviallyNormedField K] →
    (L : Type v) →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] →
          [Algebra.IsAlgebraic K L] → [hu : IsUltrametricDist K] → [CompleteSpace K] → NontriviallyNormedField L
-- Mathlib.Geometry.Manifold.IsManifold.Basic
/-- Coercion of a model with corners to a function. We don't use `e.toFun` because it is actually
`e.toPartialEquiv.toFun`, so `simp` will apply lemmas about `toPartialEquiv`. While we may want to
switch to this behavior later, doing it mid-port will break a lot of proofs.  -/
ModelWithCorners.toFun' : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] → {H : Type u_3} → [inst_3 : TopologicalSpace H] → ModelWithCorners 𝕜 E H → H → E
-- Mathlib.CategoryTheory.Sites.LocallyBijective
CategoryTheory.GrothendieckTopology.instWEqualsLocallyBijectiveTypeFun : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C),
  J.WEqualsLocallyBijective (Type (max u v))
-- Mathlib.Dynamics.FixedPoints.Topology
/-- If the iterates `f^[n] x` converge to `y` and `f` is continuous at `y`,
then `y` is a fixed point for `f`.  -/
isFixedPt_of_tendsto_iterate : ∀ {α : Type u_1} [inst : TopologicalSpace α] [T2Space α] {f : α → α} {x y : α},
  Filter.Tendsto (fun n => f^[n] x) Filter.atTop (nhds y) → ContinuousAt f y → Function.IsFixedPt f y
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.replaceTR.go.eq_def : ∀ {α : Type u_1} [inst : BEq α] (l : List α) (b c : α) (a : List α) (a_1 : Array α),
  List.replaceTR.go✝ l b c a a_1 =
    match a, a_1 with
    | [], x => l
    | a :: as, acc => bif b == a then acc.toListAppend (c :: as) else List.replaceTR.go✝ l b c as (acc.push a)
-- Mathlib.Algebra.MvPolynomial.CommRing
/-- A ring homomorphism `f : Z[X_1, X_2, ...] → R`
is determined by the evaluations `f(X_1)`, `f(X_2)`, ...  -/
MvPolynomial.eval₂Hom_X : ∀ {S : Type v} [inst : CommRing S] {R : Type u} (c : ℤ →+* S) (f : MvPolynomial R ℤ →+* S) (x : MvPolynomial R ℤ),
  MvPolynomial.eval₂ c (⇑f ∘ MvPolynomial.X) x = f x
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
ENNReal.log.eq_1 : ∀ (x : ENNReal), x.log = if x = 0 then ⊥ else if x = ⊤ then ⊤ else ↑(Real.log x.toReal)
-- Mathlib.Geometry.Manifold.HasGroupoid
OpenPartialHomeomorph.singletonChartedSpace_chartAt_eq : ∀ {H : Type u} [inst : TopologicalSpace H] {α : Type u_5} [inst_1 : TopologicalSpace α] (e : OpenPartialHomeomorph α H)
  (h : e.source = Set.univ) {x : α}, chartAt H x = e
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
LieRinehartSubalgebra.coe_toLieSubalgebra : ∀ {A : Type u_1} {L : Type u_2} [inst : CommRing A] [inst_1 : LieRing L] [inst_2 : Module A L]
  (L' : LieRinehartSubalgebra A L) [inst_3 : LieRingModule L A] [inst_4 : LieRinehartRing A L] (R : Type u_3)
  [inst_5 : CommRing R] [inst_6 : Algebra R A] [inst_7 : LieAlgebra R L] [inst_8 : LieRinehartAlgebra R A L],
  ↑(L'.toLieSubalgebra R) = ↑L'
-- Mathlib.Algebra.Group.Commute.Defs
AddCommute.addSemiconjBy : ∀ {S : Type u_3} [inst : Add S] {a b : S}, AddCommute a b → AddSemiconjBy a b b
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.inv_apply : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : (i : ι) → Inv (G i)] (f : (i : ι) → G i) (i : ι), f⁻¹ i = (f i)⁻¹
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.hom_add : ∀ {R : Type u} [inst : Ring R] {M N : ModuleCat R} (f g : M ⟶ N),
  ModuleCat.Hom.hom (f + g) = ModuleCat.Hom.hom f + ModuleCat.Hom.hom g
-- Mathlib.Topology.Compactness.Compact
/-- The set difference of a compact set and an open set is a compact set.  -/
IsCompact.diff : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsCompact s → IsOpen t → IsCompact (s \ t)
-- Mathlib.Data.Set.Image
Set.image_insert_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {a : α} {s : Set α}, f '' insert a s = insert (f a) (f '' s)
-- Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Complex.not_continuousAt_Gamma_neg_nat : ∀ (n : ℕ), ¬ContinuousAt Complex.Gamma (-↑n)
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.mkMonoidHom_apply : ∀ {M : Type u_1} [inst : CommMonoid M] (a : M), Associates.mkMonoidHom a = Associates.mk a
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_roc_eq_nil_iff : ∀ {m n : ℕ}, (m<...=n).toArray = #[] ↔ n ≤ m
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.natTransTruncLEOfLE.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b),
  t.natTransTruncLEOfLE a b h = t.natTransTruncLEOfLE a b h
-- Mathlib.Topology.AlexandrovDiscrete
alexandrovDiscrete_coinduced : ∀ {α : Type u_3} [inst : TopologicalSpace α] [AlexandrovDiscrete α] {β : Type u_5} {f : α → β}, AlexandrovDiscrete β
-- Mathlib.GroupTheory.DivisibleHull
DivisibleHull.instIsOrderedCancelAddMonoid : ∀ {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedCancelAddMonoid M],
  IsOrderedCancelAddMonoid (DivisibleHull M)
-- Mathlib.Data.Finset.Piecewise
Finset.le_piecewise_of_le_of_le : ∀ {ι : Type u_1} (s : Finset ι) [inst : (j : ι) → Decidable (j ∈ s)] {π : ι → Type u_3} {f g h : (i : ι) → π i}
  [inst_1 : (i : ι) → Preorder (π i)], h ≤ f → h ≤ g → h ≤ s.piecewise f g
-- Init.Data.Int.Linear
Int.Internal.Linear.dvd_of_eq_cert.eq_1 : ∀ (x : Int.Internal.Linear.Var) (p₁ : Int.Internal.Linear.Poly) (d₂ : ℤ) (p₂ : Int.Internal.Linear.Poly),
  Int.Internal.Linear.dvd_of_eq_cert x p₁ d₂ p₂ =
    (d₂.beq' (Int.Internal.Linear.abs (p₁.coeff_k x))).and'
      (p₂.beq' (Int.Internal.Linear.Poly.insert (-p₁.coeff_k x) x p₁))
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.inv_last : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : (i : ι) → Group (G i)] {i j : ι} (w : Monoid.CoprodI.NeWord G i j),
  w.inv.last = w.head⁻¹
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- `n ↦ ∏ₙ X` is left adjoint to `Hom(-, X)`.  -/
CategoryTheory.Limits.piConstAdj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasProducts C] →
      (X : C) → (CategoryTheory.Limits.piConst.obj X).rightOp ⊣ CategoryTheory.yoneda.obj X
-- Lean.Elab.AssertExists
/-- The type of the assertion: `true` means declaration, `false` means import.  -/
Lean.Elab.Command.AssertExists.isDecl : Lean.Elab.Command.AssertExists → Bool
-- Batteries.Data.Vector.Lemmas
Vector.get_ofFn : ∀ {n : ℕ} {α : Type u_1} (f : Fin n → α) (i : Fin n), (Vector.ofFn f).get i = f i
-- Std.Do.Triple.SpecLemmas
List.gt_of_range'_eq_append_cons : ∀ {s n step : ℕ} {xs : List ℕ} {i : ℕ} {ys : List ℕ} {j : ℕ},
  List.range' s n step = xs ++ i :: ys → 0 < step → j ∈ xs → j < i
-- Mathlib.GroupTheory.SchurZassenhaus
/-- The quotient of the transversals of an abelian normal `N` by the `diff` relation.  -/
Subgroup.QuotientDiff : {G : Type u_1} → [inst : Group G] → (H : Subgroup G) → [IsMulCommutative ↥H] → [H.FiniteIndex] → Type u_1
-- Mathlib.Algebra.MonoidAlgebra.Support
MonoidAlgebra.support_coeff_single_mul : ∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] [inst_1 : Mul G] [inst_2 : IsLeftCancelMul G] (f : MonoidAlgebra k G)
  (r : k),
  (∀ (y : k), r * y = 0 ↔ y = 0) →
    ∀ (x : G), (MonoidAlgebra.single x r * f).coeff.support = Finset.map (mulLeftEmbedding x) f.coeff.support
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.instInhabitedBtℕ : (e : Lean.Expr) → Inhabited (Mathlib.Tactic.Ring.Common.btℕ e)
-- Mathlib.Topology.Homotopy.Path
/-- If paths `p` and `q` are homotopic as paths `x ⟶ y`,
then they are homotopic as paths `x' ⟶ y'`, where `x' = x` and `y' = y`.  -/
Path.Homotopy.pathCast : {X : Type u} →
  [inst : TopologicalSpace X] →
    {x x' y y' : X} →
      {p q : Path x y} → p.Homotopy q → (hx : x' = x) → (hy : y' = y) → (p.cast hx hy).Homotopy (q.cast hx hy)
-- Init.System.IO
EIO.tryCatch : {ε α : Type} → EIO ε α → (ε → EIO ε α) → EIO ε α
-- Lean.Data.KVMap
Lean.instBEqDataValue : BEq Lean.DataValue
-- Mathlib.Analysis.Normed.Group.Ultra
IsUltrametricDist.isUltrametricDist_iff_isNonarchimedean_nnnorm : ∀ {R : Type u_4} [inst : SeminormedAddCommGroup R], IsUltrametricDist R ↔ IsNonarchimedean fun x => ↑‖x‖₊
-- Mathlib.Order.Interval.Basic
Interval.mem_pure : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, b ∈ Interval.pure a ↔ b = a
-- Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
PositiveLinearMap.instInnerProductSpaceComplexPreGNS : {A : Type u_1} →
  [inst : NonUnitalCStarAlgebra A] →
    [inst_1 : PartialOrder A] → (f : A →ₚ[ℂ] ℂ) → [inst_2 : StarOrderedRing A] → InnerProductSpace ℂ f.PreGNS
-- Mathlib.Topology.Algebra.InfiniteSum.Order
hasSum_of_isGLB_of_nonpos : ∀ {ι : Type u_1} {α : Type u_3} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α]
  [inst_3 : TopologicalSpace α] [OrderTopology α] {f : ι → α} (i : α),
  (∀ (i : ι), f i ≤ 0) → IsGLB (Set.range fun s => ∑ i ∈ s, f i) i → HasSum f i
-- Std.Do.PostCond
Std.Do.ExceptConds.imp.eq_def : ∀ {ps : Std.Do.PostShape} (x y : Std.Do.ExceptConds ps),
  (x →ₑ y) =
    match ps, x, y with
    | Std.Do.PostShape.pure, x, y => PUnit.unit
    | Std.Do.PostShape.arg σ ps, x, y => x →ₑ y
    | Std.Do.PostShape.except ε a, x, y => (fun e => spred(x.1 e → y.1 e), x.2 →ₑ y.2)
-- Mathlib.Algebra.BigOperators.Pi
Pi.list_sum_apply : ∀ {α : Type u_7} {M : α → Type u_8} [inst : (a : α) → AddMonoid (M a)] (a : α) (l : List ((a : α) → M a)),
  l.sum a = (List.map (fun f => f a) l).sum
-- Mathlib.Algebra.Category.Grp.Basic
/-- An alias for `GrpCat.{max u v}`, to deal around unification issues.  -/
GrpMax : Type ((max u1 u2) + 1)
-- Mathlib.Algebra.Category.Grp.Limits
GrpCat.forget_createsLimit.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J GrpCat),
  GrpCat.forget_createsLimit F =
    CategoryTheory.createsLimitOfNatIso
      (CategoryTheory.Iso.refl ((CategoryTheory.forget₂ GrpCat MonCat).comp (CategoryTheory.forget MonCat)))
-- Mathlib.NumberTheory.RamificationInertia.Basic
Ideal.powQuotSuccInclusion_injective : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R) (P : Ideal S)
  (i : ℕ), Function.Injective ⇑(p.powQuotSuccInclusion P i)
-- Mathlib.Topology.Order.ScottTopology
Topology.IsScott.scottContinuousOn_iff_continuous : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : TopologicalSpace α] [inst_2 : Preorder β]
  [inst_3 : TopologicalSpace β] [Topology.IsScott β Set.univ] {f : α → β} {D : Set (Set α)} [Topology.IsScott α D],
  (∀ (a b : α), a ≤ b → {a, b} ∈ D) → (ScottContinuousOn D f ↔ Continuous f)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.reverse_reverse : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.reverse.reverse = p
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
/-- `binEntropy` is symmetric about 1/2.  -/
Real.binEntropy_one_sub : ∀ (p : ℝ), Real.binEntropy (1 - p) = Real.binEntropy p
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.mapAlgEquiv_apply : ∀ (R : Type u_1) {A : Type u_4} {B : Type u_5} (M : Type u_7) [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : Monoid M] (e : A ≃ₐ[R] B)
  (a : MonoidAlgebra A M), (MonoidAlgebra.mapAlgEquiv R M e) a = (↑↑(MonoidAlgebra.mapAlgHom M ↑e).toRingHom).toFun a
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryGT?.go.eq_2 : ∀ {α : Type u} {β : Type v} [inst : Ord α] (k : α) (best : Option (α × β)) (size : ℕ) (k' : α) (v' : β)
  (l r : Std.DTreeMap.Internal.Impl α fun x => β),
  Std.DTreeMap.Internal.Impl.Const.getEntryGT?.go k best (Std.DTreeMap.Internal.Impl.inner size k' v' l r) =
    match compare k k' with
    | Ordering.lt => Std.DTreeMap.Internal.Impl.Const.getEntryGT?.go k (some (k', v')) l
    | x => Std.DTreeMap.Internal.Impl.Const.getEntryGT?.go k best r
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
lift_trdeg_le_of_surjective : ∀ {R : Type u_2} {A : Type v} {A' : Type v'} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing A']
  [inst_3 : Algebra R A] [inst_4 : Algebra R A'] (f : A →ₐ[R] A'),
  Function.Surjective ⇑f → Cardinal.lift.{v, v'} (Algebra.trdeg R A') ≤ Cardinal.lift.{v', v} (Algebra.trdeg R A)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey_diff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {h_mem : k ∈ m₁ \ m₂}, (m₁ \ m₂).getKey k h_mem = m₁.getKey k ⋯
-- Mathlib.Order.Interval.Set.Pi
Set.image_single_uIcc_left : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Lattice (α i)] [inst_1 : DecidableEq ι]
  [inst_2 : (i : ι) → Zero (α i)] (i : ι) (a : α i), Pi.single i '' Set.uIcc a 0 = Set.uIcc (Pi.single i a) 0
-- Mathlib.Data.EReal.Operations
EReal.recENNReal_coe_ennreal : ∀ {motive : EReal → Sort u_1} (coe : (x : ENNReal) → motive ↑x) (neg_coe : (x : ENNReal) → 0 < x → motive (-↑x))
  (x : ENNReal), EReal.recENNReal coe neg_coe ↑x = coe x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {l : List ((a : α) × β a)} {k k' : α} (k_beq : compare k k' = Ordering.eq)
  {v : β k} {fallback : β k'},
  List.Pairwise (fun a b => ¬compare a.fst b.fst = Ordering.eq) l →
    ⟨k, v⟩ ∈ l → (↑(t.insertMany l ⋯)).getD k' fallback = cast ⋯ v
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.symm.eq_1 : ∀ {M : Type u_9} {N : Type u_10} [inst : Add M] [inst_1 : Add N] (h : M ≃+ N),
  h.symm = { toEquiv := h.symm, map_add' := ⋯ }
-- Mathlib.Algebra.Notation.Lemmas
ite_neg : ∀ {α : Type u_1} [inst : Zero α] {p : Prop} [inst_1 : Decidable p] {a b : α} [inst_2 : LT α],
  a < 0 → b < 0 → (if p then a else b) < 0
-- Mathlib.Order.Partition.Basic
Partition.rel_rfl_iff : ∀ {α : Type u_1} {x : α} {u : Set α} {P : Partition u}, P.Rel x x ↔ x ∈ u
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- The map between indexing types of the coverings of the fibre products over `S`.  -/
CategoryTheory.PreOneHypercover.Hom.s₁ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      {E : CategoryTheory.PreOneHypercover S} →
        {F : CategoryTheory.PreOneHypercover S} →
          (self : E.Hom F) → {i j : E.I₀} → E.I₁ i j → F.I₁ (self.s₀ i) (self.s₀ j)
-- Mathlib.Data.Finset.Powerset
Finset.powersetCard_mono : ∀ {α : Type u_1} {n : ℕ} {s t : Finset α}, s ⊆ t → Finset.powersetCard n s ⊆ Finset.powersetCard n t
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- Let `C(G, A)` denote the complex of inhomogeneous chains of `A : Rep k G`. This lemma
says `d₂₁` gives a simpler expression for the 1st differential: that is, the following
square commutes:
```
  C₂(G, A) --d 2 1--> C₁(G, A)
    |                    |
    |                    |
    |                    |
    v                    v
  (G² →₀ A) --d₂₁--> (G →₀ A)
```
where the vertical arrows are `chainsIso₂` and `chainsIso₁` respectively.
 -/
groupHomology.comp_d₂₁_eq : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.CategoryStruct.comp (groupHomology.chainsIso₂ A).hom (groupHomology.d₂₁ A) =
    CategoryTheory.CategoryStruct.comp ((groupHomology.inhomogeneousChains A).d 2 1) (groupHomology.chainsIso₁ A).hom
-- Mathlib.FieldTheory.Relrank
Subfield.inf_relfinrank_left : ∀ {E : Type v} [inst : Field E] (A B : Subfield E), (A ⊓ B).relfinrank A = B.relfinrank A
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- The `w'`-index type of a `w'`-small `0`-hypercover.  -/
CategoryTheory.Precoverage.ZeroHypercover.Small.Index : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Precoverage C} → {S : C} → (E : J.ZeroHypercover S) → [E.Small] → Type w'
-- Init.Data.Int.Order
Int.mul.eq_2 : ∀ (m_2 n_2 : ℕ), (Int.ofNat m_2).mul (Int.negSucc n_2) = Int.negOfNat (m_2 * n_2.succ)
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.map_const : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (l : Filter α) (a : β) (f : β → γ), Filter.Germ.map f ↑a = ↑(f a)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
CategoryTheory.Limits.pullbackConeOfLeftIso_π_app_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.IsIso f],
  (CategoryTheory.Limits.pullbackConeOfLeftIso f g).π.app CategoryTheory.Limits.WalkingCospan.left =
    CategoryTheory.CategoryStruct.comp g (CategoryTheory.inv f)
-- Mathlib.Data.Finsupp.Interval
Finsupp.mem_rangeSingleton_apply_iff : ∀ {ι : Type u_1} {α : Type u_2} [inst : Zero α] {f : ι →₀ α} {i : ι} {a : α}, a ∈ f.rangeSingleton i ↔ a = f i
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PushoutProduct
SSet.anodyneExtensions.whiskerLeft : ∀ {X Y : SSet} {f : X ⟶ Y},
  SSet.anodyneExtensions f →
    ∀ (Z : SSet), SSet.anodyneExtensions (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z f)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.eval_polynomial_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F},
  P 2 ≠ 0 →
    (MvPolynomial.eval P) W.polynomial / P 2 ^ 3 = Polynomial.evalEval (P 0 / P 2) (P 1 / P 2) W.toAffine.polynomial
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.contract_eq_contract_iff : ∀ {α : Type u_1} {M : Matroid α} {C₁ C₂ : Set α}, M.contract C₁ = M.contract C₂ ↔ C₁ ∩ M.E = C₂ ∩ M.E
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.starProjection_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (U : Submodule 𝕜 E) [inst_3 : U.HasOrthogonalProjection] (v : E), U.starProjection v = ↑(U.orthogonalProjectionOnto v)
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X : CategoryTheory.SimplicialObject.Augmented C} →
      (s' : X.right ⟶ X.left.obj (Opposite.op { len := 0 })) →
        (s : (n : ℕ) → X.left.obj (Opposite.op { len := n }) ⟶ X.left.obj (Opposite.op { len := n + 1 })) →
          autoParam
              (CategoryTheory.CategoryStruct.comp s' (X.hom.app (Opposite.op { len := 0 })) =
                CategoryTheory.CategoryStruct.id X.right)
              CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s'_comp_ε._autoParam →
            autoParam
                (CategoryTheory.CategoryStruct.comp (s 0) (X.left.δ 1) =
                  CategoryTheory.CategoryStruct.comp (X.hom.app (Opposite.op { len := 0 })) s')
                CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s₀_comp_δ₁._autoParam →
              autoParam
                  (∀ (n : ℕ),
                    CategoryTheory.CategoryStruct.comp (s n) (X.left.δ 0) =
                      CategoryTheory.CategoryStruct.id (X.left.obj (Opposite.op { len := n })))
                  CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_δ₀._autoParam →
                autoParam
                    (∀ (n : ℕ) (i : Fin (n + 2)),
                      CategoryTheory.CategoryStruct.comp (s (n + 1)) (X.left.δ i.succ) =
                        CategoryTheory.CategoryStruct.comp (X.left.δ i) (s n))
                    CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_δ._autoParam →
                  autoParam
                      (∀ (n : ℕ) (i : Fin (n + 1)),
                        CategoryTheory.CategoryStruct.comp (s n) (X.left.σ i.succ) =
                          CategoryTheory.CategoryStruct.comp (X.left.σ i) (s (n + 1)))
                      CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_σ._autoParam →
                    X.ExtraDegeneracy
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.composableArrowsFunctor_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {X Y : CategoryTheory.ShortComplex.SnakeInput C} (f : X ⟶ Y),
  CategoryTheory.ShortComplex.SnakeInput.composableArrowsFunctor.map f =
    CategoryTheory.ComposableArrows.homMk₅ f.f₀.τ₁ f.f₀.τ₂ f.f₀.τ₃ f.f₃.τ₁ f.f₃.τ₂ f.f₃.τ₃ ⋯ ⋯ ⋯ ⋯ ⋯
-- Mathlib.Data.WSeq.Basic
/-- Map a function over a weak sequence  -/
Stream'.WSeq.map : {α : Type u} → {β : Type v} → (α → β) → Stream'.WSeq α → Stream'.WSeq β
-- Lean.Meta.LetToHave
/-- Increments the count of the number of `let`s transformed into `have`s.  -/
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.incCount : Lean.Meta.LetToHave.M✝ Unit
-- Mathlib.Algebra.Group.Finsupp
Finsupp.induction : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddZeroClass M] {motive : (ι →₀ M) → Prop} (f : ι →₀ M),
  motive 0 →
    (∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive ((fun₀ | a => b) + f)) → motive f