mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Simp.Main
Lean.Meta.dsimp : Lean.Expr →
  Lean.Meta.Simp.Context →
    optParam Lean.Meta.Simp.SimprocsArray #[] →
      optParam Lean.Meta.Simp.Stats { } → Lean.MetaM (Lean.Expr × Lean.Meta.Simp.Stats)
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.nodal_erase_eq_nodal_div : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {v : ι → F} {i : ι},
  i ∈ s → Lagrange.nodal (s.erase i) v = Lagrange.nodal s v / (Polynomial.X - Polynomial.C (v i))
-- Mathlib.RingTheory.Ideal.IsAugmentation
Ideal.isAugmentation_iff : ∀ (R : Type u_1) [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : Algebra R A] (I : Ideal A),
  Ideal.IsAugmentation R I ↔ IsCompl 1 (Submodule.restrictScalars R I)
-- Mathlib.Analysis.InnerProductSpace.Reproducing
RKHS.coe_sub : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {X : Type u_2} {V : Type u_3} [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] {H : Type u_4} [inst_3 : NormedAddCommGroup H] [inst_4 : InnerProductSpace 𝕜 H]
  [inst_5 : RKHS 𝕜 H X V] (f g : H), ⇑(f - g) = ⇑f - ⇑g
-- Mathlib.Analysis.MeanInequalitiesPow
Real.pow_arith_mean_le_arith_mean_pow : ∀ {ι : Type u} (s : Finset ι) (w z : ι → ℝ),
  (∀ i ∈ s, 0 ≤ w i) →
    ∑ i ∈ s, w i = 1 → (∀ i ∈ s, 0 ≤ z i) → ∀ (n : ℕ), (∑ i ∈ s, w i * z i) ^ n ≤ ∑ i ∈ s, w i * z i ^ n
-- Mathlib.Data.Matrix.Basis
Matrix.single_mul_single_of_ne : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type u_7} [inst : DecidableEq l] [inst_1 : DecidableEq m]
  [inst_2 : DecidableEq n] [inst_3 : Fintype m] [inst_4 : NonUnitalNonAssocSemiring α] (c : α) (i : l) (j k : m)
  {l_1 : n}, j ≠ k → ∀ (d : α), Matrix.single i j c * Matrix.single k l_1 d = 0
-- Mathlib.LinearAlgebra.DirectSum.TensorProduct
TensorProduct.directSumLeft_tmul : ∀ (R : Type u) [inst : CommSemiring R] (S : Type u_1) [inst_1 : Semiring S] [inst_2 : Algebra R S] {ι₁ : Type v₁}
  [inst_3 : DecidableEq ι₁] {M₁ : ι₁ → Type w₁} {M₂' : Type w₂'} [inst_4 : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)]
  [inst_5 : AddCommMonoid M₂'] [inst_6 : (i₁ : ι₁) → Module R (M₁ i₁)] [inst_7 : Module R M₂']
  [inst_8 : (i₁ : ι₁) → Module S (M₁ i₁)] [inst_9 : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)]
  (m : DirectSum ι₁ fun i => M₁ i) (n : M₂') (i : ι₁),
  ((TensorProduct.directSumLeft R S M₁ M₂') (m ⊗ₜ[R] n)) i = m i ⊗ₜ[R] n
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
/-- **Alias** of `BddAbove.mul`. -/
Set.BddAbove.mul : ∀ {M : Type u_3} [inst : Mul M] [inst_1 : Preorder M] [MulLeftMono M] [MulRightMono M] {s t : Set M},
  BddAbove s → BddAbove t → BddAbove (s * t)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- The semantics for `BVPred`.
 -/
Std.Tactic.BVDecide.BVPred.eval : Std.Tactic.BVDecide.BVExpr.Assignment → Std.Tactic.BVDecide.BVPred → Bool
-- Init.Omega.Constraint
Lean.Omega.Constraint.translate_sat : ∀ {t : ℤ} {c : Lean.Omega.Constraint} {v : ℤ}, c.sat v = true → (c.translate t).sat (v + t) = true
-- Mathlib.Analysis.Normed.Group.Bounded
tendsto_norm_comp_cofinite_atTop_of_isClosedEmbedding' : ∀ {E : Type u_2} [inst : SeminormedGroup E] {X : Type u_5} [inst_1 : TopologicalSpace X] [DiscreteTopology X]
  [ProperSpace E] {e : X → E}, Topology.IsClosedEmbedding e → Filter.Tendsto (norm ∘ e) Filter.cofinite Filter.atTop
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsAddFundamentalDomain.image_of_equiv : ∀ {G : Type u_1} {H : Type u_2} {α : Type u_3} {β : Type u_4} [inst : AddGroup G] [inst_1 : AddGroup H]
  [inst_2 : AddAction G α] [inst_3 : MeasurableSpace α] [inst_4 : AddAction H β] [inst_5 : MeasurableSpace β]
  {s : Set α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β},
  MeasureTheory.IsAddFundamentalDomain G s μ →
    ∀ (f : α ≃ β),
      MeasureTheory.Measure.QuasiMeasurePreserving (⇑f.symm) ν μ →
        ∀ (e : H ≃ G),
          (∀ (g : H), Function.Semiconj (⇑f) (fun x => e g +ᵥ x) fun x => g +ᵥ x) →
            MeasureTheory.IsAddFundamentalDomain H (⇑f '' s) ν
-- Init.Data.UInt.Lemmas
USize.lt_asymm : ∀ {a b : USize}, a < b → ¬b < a
-- Init.Core
instSubsingletonDecidable : ∀ (p : Prop), Subsingleton (Decidable p)
-- Mathlib.Topology.DiscreteSubset
IsCompact.finite_sdiff_of_mem_codiscreteWithin : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s K : Set X}, IsCompact K → s ∈ Filter.codiscreteWithin K → (K \ s).Finite
-- Init.Prelude
instPowNat : {α : Type u_1} → [NatPow α] → Pow α ℕ
-- Mathlib.FieldTheory.SplittingField.IsSplittingField
Polynomial.IsSplittingField.splits : ∀ {K : Type v} (L : Type w) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (f : Polynomial K)
  [Polynomial.IsSplittingField K L f], (Polynomial.map (algebraMap K L) f).Splits
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.sdiv.match_1.eq_4 : ∀ (motive : Bool → Bool → Sort u_1) (h_1 : Unit → motive false false) (h_2 : Unit → motive false true)
  (h_3 : Unit → motive true false) (h_4 : Unit → motive true true),
  (match true, true with
    | false, false => h_1 ()
    | false, true => h_2 ()
    | true, false => h_3 ()
    | true, true => h_4 ()) =
    h_4 ()
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get!_union_of_contains_eq_false_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β}
  [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited β],
  (↑m₁).WF →
    (↑m₂).WF →
      ∀ {k : α},
        m₁.contains k = false →
          Std.DHashMap.Internal.Raw₀.Const.get! (m₁.union m₂) k = Std.DHashMap.Internal.Raw₀.Const.get! m₂ k
-- Mathlib.Data.Nat.Choose.Lucas
/-- For primes `p`, `choose n k` is congruent to `choose (n % p) (k % p) * choose (n / p) (k / p)`
modulo `p`. Also see `choose_modEq_choose_mod_mul_choose_div_nat` for the version with `MOD`.  -/
Choose.choose_modEq_choose_mod_mul_choose_div : ∀ {n k p : ℕ} [Fact (Nat.Prime p)], ↑(n.choose k) ≡ ↑((n % p).choose (k % p)) * ↑((n / p).choose (k / p)) [ZMOD ↑p]
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
/-- The pure tensors (i.e. the elements of the image of `PiTensorProduct.tprod`) span
the tensor product.  -/
PiTensorProduct.span_tprod_eq_top : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)], Submodule.span R (Set.range ⇑(PiTensorProduct.tprod R)) = ⊤
-- Mathlib.GroupTheory.Submonoid.Center
Submonoid.center_pi : ∀ {ι : Type u_2} {M : ι → Type u_3} [inst : (i : ι) → MulOneClass (M i)],
  Submonoid.center ((i : ι) → M i) = Submonoid.pi Set.univ fun i => Submonoid.center (M i)
-- Mathlib.Topology.ContinuousMap.StoneWeierstrass
ContinuousMap.sup_mem_subalgebra_closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : CompactSpace X] (A : Subalgebra ℝ C(X, ℝ)) (f g : ↥A),
  ↑f ⊔ ↑g ∈ A.topologicalClosure
-- Lean.Compiler.ExternAttr
Lean.externAttr : Lean.ParametricAttribute Lean.ExternAttrData
-- Mathlib.Algebra.Group.Conj
ConjClasses.mkEquiv.eq_1 : ∀ {α : Type u} [inst : CommMonoid α],
  ConjClasses.mkEquiv = { toFun := ConjClasses.mk, invFun := Quotient.lift id ⋯, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.str : (self : SemiNormedGrp) → SeminormedAddCommGroup self.carrier
-- Mathlib.Order.Interval.Set.Image
Set.preimage_subtype_val_Iio : ∀ {α : Type u_1} [inst : Preorder α] {p : α → Prop} (a : { x // p x }), Subtype.val ⁻¹' Set.Iio ↑a = Set.Iio a
-- Mathlib.Algebra.Module.Submodule.Ker
LinearMap.ker_eq_bot' : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  {f : M →ₛₗ[τ₁₂] M₂}, f.ker = ⊥ ↔ ∀ (m : M), f m = 0 → m = 0
-- Mathlib.Tactic.NormNum.Basic
Mathlib.Meta.NormNum.isNNRat_div : ∀ {α : Type u} [inst : DivisionSemiring α] {a b : α} {cn cd : ℕ},
  Mathlib.Meta.NormNum.IsNNRat (a * b⁻¹) cn cd → Mathlib.Meta.NormNum.IsNNRat (a / b) cn cd
-- Mathlib.Topology.Continuous
Equiv.isOpenMap_symm_iff : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : X ≃ Y),
  IsOpenMap ⇑e.symm ↔ Continuous ⇑e
-- Mathlib.Algebra.Notation.Prod
Prod.snd_zero : ∀ {M : Type u_3} {N : Type u_4} [inst : Zero M] [inst_1 : Zero N], 0.2 = 0
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.Hom.ext_iff : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C}
  {S₁ S₂ : CategoryTheory.ShortComplex C} {x y : S₁.Hom S₂}, x = y ↔ x.τ₁ = y.τ₁ ∧ x.τ₂ = y.τ₂ ∧ x.τ₃ = y.τ₃
-- Mathlib.Algebra.SkewMonoidAlgebra.Lift
SkewMonoidAlgebra.lift_apply' : ∀ {k : Type u_1} {G : Type u_2} [inst : CommSemiring k] [inst_1 : Monoid G] {A : Type u_4} [inst_2 : Semiring A]
  [inst_3 : Algebra k A] [inst_4 : MulSemiringAction G k] [inst_5 : SMulCommClass G k k] (F : G →* A)
  (f : SkewMonoidAlgebra k G), ((SkewMonoidAlgebra.lift k G A) F) f = f.sum fun a b => (algebraMap k A) b * F a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_of_contains_insertMany!_list : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] [inst : BEq α]
  [Std.LawfulBEqOrd α],
  t.WF →
    ∀ {l : List ((a : α) × β a)} {k : α},
      Std.DTreeMap.Internal.Impl.contains k ↑(t.insertMany! l) = true →
        (List.map Sigma.fst l).contains k = false → Std.DTreeMap.Internal.Impl.contains k t = true
-- Mathlib.SetTheory.Lists
_private.Mathlib.SetTheory.Lists.0.Lists'.toList.match_1.eq_1 : ∀ {α : Type u_1} (motive : (x : Bool) → Lists' α x → Sort u_2) (a : α) (h_1 : (a : α) → motive false (Lists'.atom a))
  (h_2 : Unit → motive true Lists'.nil)
  (h_3 : (b : Bool) → (a : Lists' α b) → (l : Lists' α true) → motive true (a.cons' l)),
  (match false, Lists'.atom a with
    | .(false), Lists'.atom a => h_1 a
    | .(true), Lists'.nil => h_2 ()
    | .(true), a.cons' l => h_3 b a l) =
    h_1 a
-- Std.Data.HashSet.Lemmas
Std.HashSet.get?_eq_some_get!_of_contains : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] [inst : Inhabited α]
  {a : α}, m.contains a = true → m.get? a = some (m.get! a)
-- Mathlib.CategoryTheory.Sites.LocallyInjective
CategoryTheory.Presheaf.isLocallyInjective_of_isLocallyInjective_fac : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {FD : D → D → Type u_1} {CD : D → Type w} [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
  [inst_3 : CategoryTheory.ConcreteCategory D FD] (J : CategoryTheory.GrothendieckTopology C)
  {F₁ F₂ F₃ : CategoryTheory.Functor Cᵒᵖ D} {φ : F₁ ⟶ F₂} {ψ : F₂ ⟶ F₃} {φψ : F₁ ⟶ F₃},
  CategoryTheory.CategoryStruct.comp φ ψ = φψ →
    ∀ [CategoryTheory.Presheaf.IsLocallyInjective J φψ], CategoryTheory.Presheaf.IsLocallyInjective J φ
-- Aesop.Saturate
Aesop.SaturateM : Type → Type
-- Mathlib.Topology.Sets.Compacts
/-- The product of two `TopologicalSpace.NonemptyCompacts`, as a `TopologicalSpace.NonemptyCompacts`
in the product space.  -/
TopologicalSpace.NonemptyCompacts.instSProdProd : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        SProd (TopologicalSpace.NonemptyCompacts α) (TopologicalSpace.NonemptyCompacts β)
          (TopologicalSpace.NonemptyCompacts (α × β))
-- Std.Data.Internal.List.Associative
Std.Internal.List.length_insertEntryIfNew : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k},
  (Std.Internal.List.insertEntryIfNew k v l).length =
    if Std.Internal.List.containsKey k l = true then l.length else l.length + 1
-- Mathlib.Data.TypeVec
/-- cases distinction for 0-length type vector  -/
TypeVec.casesNil : {β : TypeVec.{u_2} 0 → Sort u_1} → β Fin2.elim0 → (v : TypeVec.{u_2} 0) → β v
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.indep_iSup_of_antitone : ∀ {Ω : Type u_1} {ι : Type u_2} {m : ι → MeasurableSpace Ω} {m1 _mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  [inst : SemilatticeInf ι] [MeasureTheory.IsZeroOrProbabilityMeasure μ],
  (∀ (i : ι), ProbabilityTheory.Indep (m i) m1 μ) →
    (∀ (i : ι), m i ≤ _mΩ) → m1 ≤ _mΩ → Antitone m → ProbabilityTheory.Indep (⨆ i, m i) m1 μ
-- Mathlib.Data.ZMod.Basic
ZMod.intCast_cast_sub : ∀ {n : ℕ} (x y : ZMod n), (x - y).cast = (x.cast - y.cast) % ↑n
-- Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
CategoryTheory.Pretriangulated.Opposite.instCommShiftOppositeOpOpInt : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] → (CategoryTheory.opOp C).CommShift ℤ
-- Mathlib.Analysis.Convex.PathConnected
/-- The path from `a` to `b` going along a straight line segment  -/
Path.segment : {E : Type u_1} →
  [inst : AddCommGroup E] →
    [inst_1 : Module ℝ E] →
      [inst_2 : TopologicalSpace E] → [ContinuousAdd E] → [ContinuousSMul ℝ E] → (a b : E) → Path a b
-- Aesop.Stats.Basic
Aesop.GoalKind.postNorm : Aesop.GoalKind
-- Init.Data.AC
_private.Init.Data.AC.0.Lean.Data.AC.removeNeutrals.loop.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match false with
    | true => h_1 ()
    | false => h_2 ()) =
    h_2 ()
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Tactic.ComputeAsymptotics.WellFormedBasis.compare_left_aux : ∀ {basis : Tactic.ComputeAsymptotics.Basis} {f : ℝ → ℝ},
  Tactic.ComputeAsymptotics.WellFormedBasis basis →
    (∀ (g : ℝ → ℝ), List.getLast? basis = some g → (Real.log ∘ f) =o[Filter.atTop] (Real.log ∘ g)) →
      ∀ g ∈ basis, (Real.log ∘ f) =o[Filter.atTop] (Real.log ∘ g)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_insertList_of_mem : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k k' : α},
      (k == k') = true →
        List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert →
          k ∈ List.map Sigma.fst toInsert →
            Std.Internal.List.getKey? k' (Std.Internal.List.insertList l toInsert) = some k
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `0` and `+` is an additive monoid, if it admits a
surjective map that preserves `0` and `+` to an additive monoid. This version takes a custom `nsmul`
as a `[SMul ℕ M₂]` argument.  -/
Function.Surjective.addMonoid : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Add M₂] →
      [inst_1 : Zero M₂] →
        [inst_2 : SMul ℕ M₂] →
          [inst_3 : AddMonoid M₁] →
            (f : M₁ → M₂) →
              Function.Surjective f →
                f 0 = 0 →
                  (∀ (x y : M₁), f (x + y) = f x + f y) → (∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) → AddMonoid M₂
-- Mathlib.NumberTheory.Primorial
lt_primorial_self : ∀ {n : ℕ}, 2 < n → n < primorial n
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.instEpiPOpcycles : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n : ℤ),
  CategoryTheory.Epi (X.pOpcycles f g n)
-- Init.Data.UInt.IntToBitVec
USize.toBitVec32_toUInt8 : ∀ (n : USize) (h : System.Platform.numBits = 32), n.toUInt8.toBitVec = BitVec.setWidth 8 (n.toBitVec32 h)
-- Mathlib.Algebra.Group.Submonoid.Defs
OneMemClass.mk : ∀ {S : Type u_3} {M : outParam (Type u_4)} [inst : One M] [inst_1 : SetLike S M], (∀ (s : S), 1 ∈ s) → OneMemClass S M
-- Mathlib.Data.Finsupp.Defs
Finsupp.instZero : {α : Type u_1} → {M : Type u_4} → [inst : Zero M] → Zero (α →₀ M)
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.integralAgainstBilinCLM_eq_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {m : MeasurableSpace E}
  [inst_3 : OpensMeasurableSpace E] {F₁ : Type u_6} {F₂ : Type u_7} {F₃ : Type u_8} [inst_4 : NormedAddCommGroup F₁]
  [inst_5 : NormedSpace 𝕜 F₁] [inst_6 : NormedSpace ℝ F₁] [inst_7 : NormedAddCommGroup F₂] [inst_8 : NormedSpace 𝕜 F₂]
  [inst_9 : NormedAddCommGroup F₃] [inst_10 : NormedSpace 𝕜 F₃] [inst_11 : Algebra ℝ 𝕜] [inst_12 : IsScalarTower ℝ 𝕜 F₁]
  [inst_13 : NormedSpace ℝ F₃] [inst_14 : IsScalarTower ℝ 𝕜 F₃] {B : F₁ →L[𝕜] F₂ →L[𝕜] F₃} {μ : MeasureTheory.Measure E}
  {φ : E → F₂}, ¬MeasureTheory.LocallyIntegrableOn φ (↑Ω) μ → TestFunction.integralAgainstBilinCLM B μ φ = 0
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKeyD_union_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 = t₁.getKeyD k fallback
-- Mathlib.Algebra.Lie.Cochain
LieModule.Cohomology.mem_twoCocycle_iff : ∀ (R : Type u_1) [inst : CommRing R] (L : Type u_2) [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (M : Type u_3)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  (a : ↥(LieModule.Cohomology.twoCochain R L M)),
  a ∈ LieModule.Cohomology.twoCocycle R L M ↔ (LieModule.Cohomology.d₂₃ R L M) a = 0
-- Mathlib.Data.List.MinMax
List.le_minimum_of_forall_le : ∀ {α : Type u_1} [inst : LinearOrder α] {l : List α} {b : WithTop α}, (∀ a ∈ l, b ≤ ↑a) → b ≤ l.minimum
-- Mathlib.Data.NNReal.Defs
NNReal.instIsScalarTowerOfReal : ∀ {M : Type u_1} {N : Type u_2} [inst : MulAction ℝ M] [inst_1 : MulAction ℝ N] [inst_2 : SMul M N]
  [IsScalarTower ℝ M N], IsScalarTower NNReal M N
-- Mathlib.Combinatorics.Configuration
/-- Line through two points  -/
Configuration.ProjectivePlane.mkLine : {P : Type u_1} →
  {L : Type u_2} → {inst : Membership P L} → [self : Configuration.ProjectivePlane P L] → {p₁ p₂ : P} → p₁ ≠ p₂ → L
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Real.aemeasurable_of_aemeasurable_exp : ∀ {α : Type u_1} {x : MeasurableSpace α} {f : α → ℝ} {μ : MeasureTheory.Measure α},
  AEMeasurable (fun x => Real.exp (f x)) μ → AEMeasurable f μ
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.ideal_ext_iff : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens},
  AlgebraicGeometry.IsAffineOpen U →
    ∀ {I J : Ideal ↑(X.presheaf.obj (Opposite.op U))},
      I = J ↔
        ∀ (x : ↥X) (h : x ∈ U),
          Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I =
            Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) J
-- Mathlib.Analysis.Normed.Group.Basic
norm_sub_eq_norm_left : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (x : E) {y : E}, ‖y‖ = 0 → ‖x - y‖ = ‖x‖
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?_diff_of_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, k ∈ t₂ → (t₁ \ t₂).getKey? k = none
-- Lean.Data.Lsp.Basic
Lean.Lsp.VersionedTextDocumentIdentifier.version? : Lean.Lsp.VersionedTextDocumentIdentifier → Option ℕ
-- Lean.Meta.GeneralizeVars
/-- Collect variables to be generalized.
It uses the following heuristic
- Collect forward dependencies that are not in the forbidden set, and depend on some variable in `targets`.

- We use `mkForbiddenSet` to compute `forbidden`.

Remark: we *not* collect instance implicit arguments nor auxiliary declarations for compiling
recursive declarations.
 -/
Lean.Meta.getFVarSetToGeneralize : Array Lean.Expr → Lean.FVarIdSet → optParam Bool false → Lean.MetaM Lean.FVarIdSet
-- Mathlib.Data.Nat.Factorization.Basic
Nat.ordCompl_dvd_ordCompl_of_dvd : ∀ {a b : ℕ}, a ∣ b → ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get!_filter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {f : α → β → Bool} {k : α},
  Std.DHashMap.Const.get! (Std.DHashMap.filter f m) k =
    ((Std.DHashMap.Const.get? m k).pfilter fun x_2 h' => f (m.getKey k ⋯) x_2).get!
-- Mathlib.Probability.CDF
/-- Cumulative distribution function of a real measure. The definition currently makes sense only
for probability measures. In that case, it satisfies `cdf μ x = μ.real (Iic x)` (see
`ProbabilityTheory.cdf_eq_real`).  -/
ProbabilityTheory.cdf : MeasureTheory.Measure ℝ → StieltjesFunction ℝ
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.GLPos.coe_neg_apply : ∀ {n : Type u} {R : Type v} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing R] [inst_3 : LinearOrder R]
  [inst_4 : IsStrictOrderedRing R] [inst_5 : Fact (Even (Fintype.card n))] (g : ↥(Matrix.GLPos n R)) (i j : n),
  ↑↑(-g) i j = -↑↑g i j
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
/-- Let `F` be a semi-`NormedSpace` over a `NontriviallyNormedField`, and let `q` be a
seminorm on `F`. If `q` is continuous, then it is uniformly controlled by the norm, that is there
is some `C > 0` such that `∀ x, q x ≤ C * ‖x‖`.
The continuity ensures boundedness on a ball of some radius `ε`. The nontriviality of the
norm is then used to rescale any element into an element of norm in `[ε/C, ε[`, thus with a
controlled image by `q`. The control of `q` at the original element follows by rescaling.  -/
Seminorm.bound_of_continuous_normedSpace : ∀ {𝕜 : Type u_2} {F : Type u_7} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (q : Seminorm 𝕜 F), Continuous ⇑q → ∃ C, 0 < C ∧ ∀ (x : F), q x ≤ C * ‖x‖
-- Mathlib.LinearAlgebra.Dimension.Constructions
finrank_ulift : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Module.finrank R (ULift.{u_2, v} M) = Module.finrank R M
-- Mathlib.LinearAlgebra.Prod
/-- `LinearMap.prodMap` as a `RingHom`  -/
LinearMap.prodMapRingHom : (R : Type u) →
  (M : Type v) →
    (M₂ : Type w) →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid M₂] →
            [inst_3 : Module R M] → [inst_4 : Module R M₂] → (M →ₗ[R] M) × (M₂ →ₗ[R] M₂) →+* M × M₂ →ₗ[R] M × M₂
-- Init.GrindInstances.ToInt
Lean.Grind.instToIntUInt8UintOfNatNat : Lean.Grind.ToInt UInt8 (Lean.Grind.IntInterval.uint 8)
-- Mathlib.Order.Filter.CountablyGenerated
Filter.prod.isCountablyGenerated : ∀ {α : Type u_1} {β : Type u_2} (la : Filter α) (lb : Filter β) [la.IsCountablyGenerated] [lb.IsCountablyGenerated],
  (la ×ˢ lb).IsCountablyGenerated
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.Arrow.precompRelation_g₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C}
  {S : J.Cover X} (I : S.Arrow) {Z : C} (g : Z ⟶ I.Y), (I.precompRelation g).g₂ = g
-- Mathlib.LinearAlgebra.AffineSpace.Centroid
/-- The weights in the centroid sum to 1, if the number of points,
converted to `k`, is not zero.  -/
Finset.sum_centroidWeights_eq_one_of_cast_card_ne_zero : ∀ {k : Type u_1} [inst : DivisionRing k] {ι : Type u_4} (s : Finset ι),
  ↑s.card ≠ 0 → ∑ i ∈ s, Finset.centroidWeights k s i = 1
-- Lean.Meta.Sym.SymM
/-- `true` if this argument is a proof (its type is a `Prop`).  -/
Lean.Meta.Sym.ProofInstArgInfo.isProof : Lean.Meta.Sym.ProofInstArgInfo → Bool
-- Mathlib.Analysis.Calculus.Conformal.NormedSpace
Conformal.differentiable : ∀ {X : Type u_1} {Y : Type u_2} [inst : NormedAddCommGroup X] [inst_1 : NormedAddCommGroup Y] [inst_2 : NormedSpace ℝ X]
  [inst_3 : NormedSpace ℝ Y] {f : X → Y}, Conformal f → Differentiable ℝ f
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.rightOp : C ⥤ Dᵒᵖ` preserves colimits of shape `Jᵒᵖ`, then `F : Cᵒᵖ ⥤ D` preserves limits
of shape `J`.  -/
CategoryTheory.Limits.preservesLimitsOfShape_of_rightOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (J : Type w) [inst_2 : CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor Cᵒᵖ D)
  [CategoryTheory.Limits.PreservesColimitsOfShape Jᵒᵖ F.rightOp], CategoryTheory.Limits.PreservesLimitsOfShape J F