mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Matrix.Basis
Matrix.induction_on : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_7} [inst : DecidableEq m] [inst_1 : DecidableEq n]
  [inst_2 : AddCommMonoid α] [Finite m] [Finite n] [Nonempty m] [Nonempty n] {P : Matrix m n α → Prop}
  (M : Matrix m n α),
  (∀ (p q : Matrix m n α), P p → P q → P (p + q)) → (∀ (i : m) (j : n) (x : α), P (Matrix.single i j x)) → P M
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKeyD_inter_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {k fallback : α}, k ∉ t₂ → (t₁ ∩ t₂).getKeyD k fallback = fallback
-- Init.Data.String.Modify
String.Pos.appendRight : {s : String} → s.Pos → (t : String) → (s ++ t).Pos
-- Init.Data.Ord.SInt
Int32.instTransOrd : Std.TransOrd Int32
-- Init.MetaTypes
Lean.Meta.DSimp.instInhabitedConfig.default : Lean.Meta.DSimp.Config
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.instTensorUnit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      CategoryTheory.MonObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Formula.realize_iInf : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {β : Type v'} [inst_1 : Finite β]
  {f : β → L.Formula α} {v : α → M}, (FirstOrder.Language.Formula.iInf f).Realize v ↔ ∀ (b : β), (f b).Realize v
-- Aesop.Builder.Forward
Aesop.RuleBuilder.forwardCore : Aesop.ElabRuleTerm →
  Option (Array Lean.Name) → Option Aesop.RulePattern → Aesop.PhaseSpec → Bool → Lean.MetaM Aesop.LocalRuleSetMember
-- Init.Data.Array.Nat
Array.sum_replicate_nat : ∀ {n a : ℕ}, (Array.replicate n a).sum = n * a
-- Lean.Elab.PreDefinition.WF.GuessLex
/-- The elaborator is prone to duplicate terms, including recursive calls, even if the user
only wrote a single one. This duplication is wasteful if we run the tactics on duplicated
calls, and confusing in the output of GuessLex. So prune the list of recursive calls,
and remove those where another call exists that has the same goal and context that is no more
specific.
 -/
Lean.Elab.WF.GuessLex.filterSubsumed : Array Lean.Elab.WF.GuessLex.RecCallWithContext → Array Lean.Elab.WF.GuessLex.RecCallWithContext
-- Mathlib.Algebra.Homology.HomotopyCategory
/-- An arbitrarily chosen representation of the image of a chain map in the homotopy category
is homotopic to the original chain map.
 -/
HomotopyCategory.homotopyOutMap : {ι : Type u_2} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {c : ComplexShape ι} →
          {C D : HomologicalComplex V c} → (f : C ⟶ D) → Homotopy (Quot.out ((HomotopyCategory.quotient V c).map f)) f
-- Mathlib.Order.Interval.Set.Basic
Set.decidableMemIoi.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] {b x : α} [inst_1 : Decidable (b < x)], Set.decidableMemIoi = inst_1
-- Mathlib.Algebra.MonoidAlgebra.Module
MonoidAlgebra.distribMulAction.eq_1 : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Monoid S] [inst_1 : Semiring R] [inst_2 : DistribMulAction S R],
  MonoidAlgebra.distribMulAction =
    { toSMul := MonoidAlgebra.smulZeroClass.toSMul, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }
-- Lean.MonadEnv
Lean.isRec? : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Lean.Name → m (Option Lean.RecursorVal)
-- Mathlib.Algebra.Homology.CommSq
CategoryTheory.IsPullback.mono_shortComplex'_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {X₁ X₂ X₃ X₄ : C}
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X₂ X₃] {fst : X₁ ⟶ X₂} {snd : X₁ ⟶ X₃} {f : X₂ ⟶ X₄} {g : X₃ ⟶ X₄}
  (h : CategoryTheory.IsPullback fst snd f g), CategoryTheory.Mono ⋯.shortComplex'.f
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.algHom_ext' : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommSemiring S] [inst_2 : Semiring T]
  [inst_3 : Algebra S R] [inst_4 : Algebra S T] {p : Polynomial R} {f g : AdjoinRoot p →ₐ[S] T},
  f.comp (AdjoinRoot.ofAlgHom S p) = g.comp (AdjoinRoot.ofAlgHom S p) →
    f (AdjoinRoot.root p) = g (AdjoinRoot.root p) → f = g
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
/-- Make a term of `(J.plusObj P).obj (op X)` from `x : Meq P S`.  -/
CategoryTheory.GrothendieckTopology.Plus.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {D : Type w} →
        [inst_1 : CategoryTheory.Category.{w', w} D] →
          {FD : D → D → Type u_1} →
            {CD : D → Type t} →
              [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] →
                [instCC : CategoryTheory.ConcreteCategory D FD] →
                  [∀ {X : C} (S : J.Cover X),
                        CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape)
                          (CategoryTheory.forget D)] →
                    [inst_4 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] →
                      [inst_5 :
                          ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X),
                            CategoryTheory.Limits.HasMultiequalizer (S.index P)] →
                        {X : C} →
                          {P : CategoryTheory.Functor Cᵒᵖ D} →
                            {S : J.Cover X} →
                              CategoryTheory.Meq P S → CategoryTheory.ToType ((J.plusObj P).obj (Opposite.op X))
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
CategoryTheory.OplaxFunctor.mapComp_assoc_left : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.OplaxFunctor B C) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
  CategoryTheory.CategoryStruct.comp (F.mapComp (CategoryTheory.CategoryStruct.comp f g) h)
      (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (F.map h)) =
    CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.associator f g h).hom)
      (CategoryTheory.CategoryStruct.comp (F.mapComp f (CategoryTheory.CategoryStruct.comp g h))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapComp g h))
          (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (F.map h)).inv))
-- Mathlib.Algebra.Polynomial.Div
Polynomial.modByMonic_eq_self_iff : ∀ {R : Type u} [inst : Ring R] {p q : Polynomial R} [Nontrivial R], q.Monic → (p %ₘ q = p ↔ p.degree < q.degree)
-- Mathlib.Algebra.Homology.AlternatingConst
HomologicalComplex.alternatingConst.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (A : C) {φ ψ : A ⟶ A} (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0)
  (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) {c : ComplexShape ℕ} [inst_2 : DecidableRel c.Rel]
  (hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)),
  HomologicalComplex.alternatingConst A hOdd hEven hc =
    { X := fun n => A, d := fun i j => if hij : c.Rel i j then if hi : Even i then φ else ψ else 0, shape := ⋯,
      d_comp_d' := ⋯ }
-- Mathlib.Data.Set.Finite.Basic
Set.univ_finite_iff_nonempty_fintype : ∀ {α : Type u}, Set.univ.Finite ↔ Nonempty (Fintype α)
-- Mathlib.Topology.Separation.Hausdorff
T2Quotient.unique_lift : ∀ {X : Type u_3} {Y : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : T2Space Y]
  {f : X → Y} (hf : Continuous f) {g : T2Quotient X → Y}, g ∘ T2Quotient.mk = f → g = T2Quotient.lift hf
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.locallyConstant_eq_of_fiber_zero_eq : ∀ {X : Type u_5} [inst : TopologicalSpace X] (f g : LocallyConstant X (Fin 2)), ⇑f ⁻¹' {0} = ⇑g ⁻¹' {0} → f = g
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.EnrichedFunctor.forgetId_hom_app : ∀ (W : Type v') [inst : CategoryTheory.Category.{w', v'} W] [inst_1 : CategoryTheory.MonoidalCategory W] (C : Type u₁)
  [inst_2 : CategoryTheory.EnrichedCategory W C] (X : CategoryTheory.ForgetEnrichment W C),
  (CategoryTheory.EnrichedFunctor.forgetId W C).hom.app X = CategoryTheory.CategoryStruct.id X
-- Mathlib.LinearAlgebra.Matrix.Block
Matrix.BlockTriangular.sub_iff_left : ∀ {α : Type u_1} {m : Type u_3} {R : Type v} {M N : Matrix m m R} {b : m → α} [inst : LT α] [inst_1 : AddGroup R],
  N.BlockTriangular b → ((M - N).BlockTriangular b ↔ M.BlockTriangular b)
-- Mathlib.Analysis.Normed.Group.Real
Real.norm_of_nonpos : ∀ {r : ℝ}, r ≤ 0 → ‖r‖ = -r
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.separatingRight_toMatrix_iff : ∀ {R₂ : Type u_3} {M₂ : Type u_4} [inst : CommRing R₂] [inst_1 : AddCommGroup M₂] [inst_2 : Module R₂ M₂] {ι : Type u_6}
  [inst_3 : DecidableEq ι] [inst_4 : Fintype ι] {B : LinearMap.BilinForm R₂ M₂} (b : Module.Basis ι R₂ M₂),
  ((LinearMap.BilinForm.toMatrix b) B).SeparatingRight ↔ LinearMap.SeparatingRight B
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.image_sub : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : SubtractionMonoid β]
  [inst_2 : FunLike F α β] [AddMonoidHomClass F α β] (m : F) {s t : Set α}, ⇑m '' (s - t) = ⇑m '' s - ⇑m '' t
-- Mathlib.Analysis.Fourier.AddCircle
fourier_coe_apply : ∀ {T : ℝ} {n : ℤ} {x : ℝ}, (fourier n) ↑x = Complex.exp (2 * ↑Real.pi * Complex.I * ↑n * ↑x / ↑T)
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_comp_assoc : ∀ {C : Type u_1} {D : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} {inst_2 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] {c c' c'' : C} {d d' d'' : D} (f₁ : d ⟶ d')
  (f₂ : d' ⟶ d'') (g₁ : c ⟶ c') (g₂ : c' ⟶ c'') {Z : D}
  (h : CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d'' c'' ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom (CategoryTheory.CategoryStruct.comp f₁ f₂)
        (CategoryTheory.CategoryStruct.comp g₁ g₂))
      h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom f₁ g₁)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom f₂ g₂) h)
-- Mathlib.SetTheory.Ordinal.Principal
/-- For `a ≠ 0`, the largest power of `ω` which is less or equal to it is also the smallest ordinal
`b` with `a - b < a`.  -/
Ordinal.isLeast_sub_lt_omega0_opow_log : ∀ {a : Ordinal.{u}}, a ≠ 0 → IsLeast {b | a - b < a} (Ordinal.omega0 ^ Ordinal.log Ordinal.omega0 a)
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.singularPart_eq_zero_of_ac : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α},
  μ.AbsolutelyContinuous ν → μ.singularPart ν = 0
-- Init.Data.Array.Lex.Lemmas
Array.lex_empty : ∀ {α : Type u_1} [inst : BEq α] {lt : α → α → Bool} {xs : Array α}, xs.lex #[] lt = false
-- Mathlib.MeasureTheory.Integral.MeanInequalities
/-- A different formulation of Hölder's inequality for two functions, with two exponents that sum to
1, instead of reciprocals of  -/
ENNReal.lintegral_mul_norm_pow_le : ∀ {α : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → ENNReal},
  AEMeasurable f μ →
    AEMeasurable g μ →
      ∀ {p q : ℝ},
        0 ≤ p →
          0 ≤ q → p + q = 1 → ∫⁻ (a : α), f a ^ p * g a ^ q ∂μ ≤ (∫⁻ (a : α), f a ∂μ) ^ p * (∫⁻ (a : α), g a ∂μ) ^ q
-- Mathlib.Order.Defs.Unbundled
of_eq : ∀ {α : Sort u_1} {r : α → α → Prop} [Std.Refl r] {a b : α}, a = b → r a b
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.filter.eq_1 : ∀ {α : Type u_1} (p : PMF α) (s : Set α) (h : ∃ a ∈ s, a ∈ p.support), p.filter s h = PMF.normalize (s.indicator ⇑p) ⋯ ⋯
-- Mathlib.Order.Disjoint
/-- An element is *complemented* if it has a complement.  -/
IsComplemented : {α : Type u_1} → [inst : Lattice α] → [BoundedOrder α] → α → Prop
-- Mathlib.Data.Seq.Parallel
_private.Mathlib.Data.Seq.Parallel.0.Computation.parallel.aux1.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option (Stream'.Seq1 (Option (Computation α))) → Sort u_2)
  (S' : Stream'.Seq (Option (Computation α))) (h_1 : Unit → motive none)
  (h_2 : (S' : Stream'.Seq (Option (Computation α))) → motive (some (none, S')))
  (h_3 : (c : Computation α) → (S' : Stream'.Seq (Option (Computation α))) → motive (some (some c, S'))),
  (match some (none, S') with
    | none => h_1 ()
    | some (none, S') => h_2 S'
    | some (some c, S') => h_3 c S') =
    h_2 S'
-- Mathlib.Algebra.ContinuedFractions.Translations
GenContFract.zeroth_conv'_eq_h : ∀ {K : Type u_1} {g : GenContFract K} [inst : DivisionRing K], g.convs' 0 = g.h
-- Lean.Meta.Tactic.FunIndInfo
Lean.Meta.instReprFunIndInfo.repr : Lean.Meta.FunIndInfo → ℕ → Std.Format
-- Mathlib.Analysis.Meromorphic.Basic
/-- Eta-expanded form of `meromorphicAt_comp_sub_const_iff_meromorphicAt`

---

`MeromorphicAt` is invariant under translation.  -/
meromorphicAt_fun_comp_sub_const_iff_meromorphicAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x c : 𝕜} {f : 𝕜 → E}, MeromorphicAt (fun x => f (x - c)) x ↔ MeromorphicAt f (x - c)
-- Init.Data.Option.Basic
/-- Gets the value in an option, monadically computing a default value on `none`.

This is the monadic analogue of `Option.getD`.
 -/
Option.getDM : {m : Type u_1 → Type u_2} → {α : Type u_1} → [Pure m] → Option α → m α → m α
-- Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Equiv.Perm.card_le_of_centralizer_le_alternating : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {g : Equiv.Perm α},
  Subgroup.centralizer {g} ≤ alternatingGroup α → Fintype.card α ≤ g.cycleType.sum + 1
-- Mathlib.Topology.Separation.Basic
exists_mem_nhds_isCompact_mapsTo_of_isCompact_mem_nhds : ∀ {X : Type u_3} {Y : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [R1Space Y] {f : X → Y}
  {x : X} {K : Set X} {s : Set Y},
  Continuous f → s ∈ nhds (f x) → IsCompact K → K ∈ nhds x → ∃ L ∈ nhds x, IsCompact L ∧ Set.MapsTo f L s
-- Mathlib.Order.Hom.CompleteLattice
sInfHom.symm_dual_id : ∀ {α : Type u_2} [inst : InfSet α], sInfHom.dual.symm (sSupHom.id αᵒᵈ) = sInfHom.id α
-- Lean.Meta.Tactic.Simp.Arith.Int.Simp
Int.Internal.Linear.Poly.gcdCoeffs' : Int.Internal.Linear.Poly → ℕ
-- Lean.Meta.Sym.Eta
/-- Checks if `body` is eta-expanded with `n` applications: `f (.bvar (n-1)) ... (.bvar 0)`.
Returns `f` if so and `f` has no loose bvars with indices in the range `[0, n)`; otherwise returns `default`.
- `n`: number of remaining applications to check
- `i`: expected bvar index (starts at 0, increments with each application)
- `default`: returned when not eta-reducible (enables pointer equality check)
 -/
_private.Lean.Meta.Sym.Eta.0.Lean.Meta.Sym.etaReduceAux : Lean.Expr → ℕ → ℕ → Lean.Expr → Lean.Expr
-- Mathlib.Algebra.Module.ULift
ULift.moduleEquiv_symm_apply : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (down : M),
  ULift.moduleEquiv.symm down = { down := down }
-- Mathlib.Topology.Algebra.Nonarchimedean.Bases
/-- A family of submodules in an `R`-module `M` is a submodules basis if it satisfies
some axioms ensuring there is a topology on `M` which is compatible with the module structure and
admits this family as a basis of neighborhoods of zero.  -/
SubmodulesBasis : {ι : Type u_1} →
  {R : Type u_2} →
    [inst : CommRing R] →
      {M : Type u_4} →
        [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → [TopologicalSpace R] → (ι → Submodule R M) → Prop
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.Agree'.below : {F : PFunctor.{uA, uB}} →
  {motive : (a : ℕ) → (a_1 a_2 : F.M) → PFunctor.M.Agree' a a_1 a_2 → Prop} →
    {a : ℕ} → {a_1 a_2 : F.M} → PFunctor.M.Agree' a a_1 a_2 → Prop
-- Lean.Data.Lsp.BasicAux
Lean.Lsp.instOrdRange.ord : Lean.Lsp.Range → Lean.Lsp.Range → Ordering
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.OneLine.State.column : Lean.PrettyPrinter.OneLine.State → ℕ
-- Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange
CliffordAlgebra.toBaseChange_comp_involute : ∀ {R : Type u_1} (A : Type u_2) {V : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : AddCommGroup V]
  [inst_3 : Algebra R A] [inst_4 : Module R V] [inst_5 : Invertible 2] (Q : QuadraticForm R V),
  (CliffordAlgebra.toBaseChange A Q).comp CliffordAlgebra.involute =
    (Algebra.TensorProduct.map (AlgHom.id A A) CliffordAlgebra.involute).comp (CliffordAlgebra.toBaseChange A Q)
-- Mathlib.Algebra.Order.Ring.Archimedean
_private.Mathlib.Algebra.Order.Ring.Archimedean.0.ArchimedeanClass.zsmul_succ' : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : Field R] [inst_2 : IsOrderedRing R] (n : ℕ) (x : ArchimedeanClass R),
  ↑n.succ • x = ↑n • x + x
-- Mathlib.Data.Fin.SuccPred
Fin.range_castSucc : ∀ {n : ℕ}, Set.range Fin.castSucc = {i | ↑i < n}
-- Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
SimpleGraph.Walk.IsSubwalk.dropLast : ∀ {V : Type u_1} {G : SimpleGraph V} {u v u' v' : V} {p : G.Walk u v} {q : G.Walk u' v'},
  p.IsSubwalk q → p.dropLast.IsSubwalk q
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast?_filter_not_contains_map_fst : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.getValueCast? k (List.filter (fun p => !(List.map Sigma.fst l₂).contains p.fst) l₁) =
      if Std.Internal.List.containsKey k l₂ = true then none else Std.Internal.List.getValueCast? k l₁
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.ultrafilter_le_nhds_infty : ∀ {X : Type u_1} [inst : TopologicalSpace X] {f : Ultrafilter (OnePoint X)},
  ↑f ≤ nhds OnePoint.infty ↔ ∀ (s : Set X), IsClosed s → IsCompact s → OnePoint.some '' s ∉ f
-- Mathlib.LinearAlgebra.Complex.Module
/-- The matrix representation of `conjAe`.  -/
Complex.toMatrix_conjAe : (LinearMap.toMatrix Complex.basisOneI Complex.basisOneI) ↑↑Complex.conjAe = !![1, 0; 0, -1]
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get?_diff_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α}, k ∉ m₂ → (m₁ \ m₂).get? k = m₁.get? k
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- `HasImageMap sq` means that there is an `ImageMap` for the square `sq`.  -/
CategoryTheory.Limits.HasImageMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {f g : CategoryTheory.Arrow C} →
      [CategoryTheory.Limits.HasImage f.hom] → [CategoryTheory.Limits.HasImage g.hom] → (f ⟶ g) → Prop
-- Mathlib.Data.Set.Finite.Basic
Finite.Set.finite_inter_of_left : ∀ {α : Type u} (s t : Set α) [Finite ↑s], Finite ↑(s ∩ t)
-- Lean.Elab.ParseImportsFast
Lean.PrintImportsResult.mk.injEq : ∀ (imports imports_1 : Array Lean.PrintImportResult),
  ({ imports := imports } = { imports := imports_1 }) = (imports = imports_1)
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.limNthHom_spec : ∀ {R : Type u_1} [inst : NonAssocSemiring R] {p : ℕ} {f : (k : ℕ) → R →+* ZMod (p ^ k)} [hp_prime : Fact (Nat.Prime p)]
  (f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1) (r : R) (ε : ℝ),
  0 < ε → ∃ N, ∀ n ≥ N, ‖PadicInt.limNthHom f_compat r - ↑(PadicInt.nthHom f r n)‖ < ε
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.del.congr_simp : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId fvarId_1 : Lean.FVarId),
  fvarId = fvarId_1 →
    ∀ (k k_1 : Lean.Compiler.LCNF.Code pu),
      k = k_1 →
        ∀ (h : pu = Lean.Compiler.LCNF.Purity.impure),
          Lean.Compiler.LCNF.Code.del fvarId k h = Lean.Compiler.LCNF.Code.del fvarId_1 k_1 h
-- Qq.Macro
Qq.Impl.ExprBackSubstResult.unquoted.sizeOf_spec : ∀ (e : Lean.Expr), sizeOf (Qq.Impl.ExprBackSubstResult.unquoted e) = 1 + sizeOf e
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskeringLeft₃ObjObjObj_obj_obj_obj_map : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6}
  [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} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃] (E : Type u_7)
  [inst_6 : CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁)
  (F₂ : CategoryTheory.Functor C₂ D₂) (F₃ : CategoryTheory.Functor C₃ D₃)
  (X : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E))) (X_1 : C₁) (X_2 : C₂)
  {X_3 Y : C₃} (f : X_3 ⟶ Y),
  ((((CategoryTheory.Functor.whiskeringLeft₃ObjObjObj E F₁ F₂ F₃).obj X).obj X_1).obj X_2).map f =
    ((X.obj (F₁.obj X_1)).obj (F₂.obj X_2)).map (F₃.map f)
-- Batteries.Data.Vector.Lemmas
Vector.getElem?_scanl_zero : ∀ {β : Type u_1} {α : Type u_2} {n : ℕ} {init : β} {f : β → α → β} {as : Vector α n},
  (Vector.scanl f init as)[0]? = some init
-- Mathlib.NumberTheory.Zsqrtd.GaussianInt
GaussianInt.normSq_div_sub_div_lt_one : ∀ (x y : GaussianInt),
  Complex.normSq (GaussianInt.toComplex x / GaussianInt.toComplex y - GaussianInt.toComplex (x / y)) < 1
-- Mathlib.Algebra.Order.BigOperators.Group.List
List.le_prod_of_submultiplicative : ∀ {α : Type u_5} {β : Type u_6} [inst : Monoid α] [inst_1 : CommMonoid β] [inst_2 : Preorder β] [IsOrderedMonoid β]
  (f : α → β), f 1 ≤ 1 → (∀ (a b : α), f (a * b) ≤ f a * f b) → ∀ (l : List α), f l.prod ≤ (List.map f l).prod
-- Lean.Compiler.IR.Basic
Lean.IR.Alt.brecOn.eq : ∀ {motive_1 : Lean.IR.Alt → Sort u} {motive_2 : Lean.IR.FnBody → Sort u} {motive_3 : Array Lean.IR.Alt → Sort u}
  {motive_4 : List Lean.IR.Alt → Sort u} (t : Lean.IR.Alt) (F_1 : (t : Lean.IR.Alt) → t.below → motive_1 t)
  (F_2 : (t : Lean.IR.FnBody) → t.below → motive_2 t)
  (F_3 : (t : Array Lean.IR.Alt) → Lean.IR.Alt.below_1 t → motive_3 t)
  (F_4 : (t : List Lean.IR.Alt) → Lean.IR.Alt.below_2 t → motive_4 t),
  t.brecOn F_1 F_2 F_3 F_4 = F_1 t (Lean.IR.Alt.brecOn.go t F_1 F_2 F_3 F_4).2
-- Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Module.rankAtStalk_eq_of_le_of_finite_of_flat' : ∀ {R : Type uR} (M : Type uM) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Flat R M]
  [Module.Finite R M] {p q : Ideal R} [hp : p.IsPrime] [hq : q.IsPrime],
  p ≤ q → Module.rankAtStalk M { asIdeal := p, isPrime := hp } = Module.rankAtStalk M { asIdeal := q, isPrime := hq }
-- Init.Data.Vector.Attach
Vector.pmap_append : ∀ {ι : Type u_1} {α : Type u_2} {n m : ℕ} {p : ι → Prop} {f : (a : ι) → p a → α} {xs : Vector ι n} {ys : Vector ι m}
  (h : ∀ a ∈ xs ++ ys, p a), Vector.pmap f (xs ++ ys) h = Vector.pmap f xs ⋯ ++ Vector.pmap f ys ⋯
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_filter!_key_iff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] {f : α → Bool}
  {k : α},
  t.WF →
    (Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.filter! (fun a x => f a) t) = true ↔
      ∃ (h : Std.DTreeMap.Internal.Impl.contains k t = true), f (t.getKey k h) = true)
-- Init.Data.String.Lemmas.FindPos
String.posLT_eq_posLT_toSlice : ∀ {s : String} {p : String.Pos.Raw} (h : 0 < p), s.posLT p h = String.Pos.ofToSlice (s.toSlice.posLT p h)
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instLeftCancelMonoid : {α : Type u_1} → [LeftCancelMonoid α] → LeftCancelMonoid (Lex α)
-- Mathlib.Algebra.Homology.ExactSequenceFour
CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_inv_hom_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Balanced C] {n : ℕ} {S : CategoryTheory.ComposableArrows C (n + 3)} (hS : S.Exact) (k : ℕ)
  (hk : k ≤ n) (cc : CategoryTheory.Limits.CokernelCofork (S.map' k (k + 1) ⋯ ⋯))
  (kf : CategoryTheory.Limits.KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)) (hcc : CategoryTheory.Limits.IsColimit cc)
  (hkf : CategoryTheory.Limits.IsLimit kf),
  CategoryTheory.CategoryStruct.comp (hS.cokerIsoKer' k hk cc kf hcc hkf).inv (hS.cokerToKer' k hk cc kf hcc hkf) =
    CategoryTheory.CategoryStruct.id kf.pt