mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.MetricSpace.Completion
Isometry.extensionHom_coe : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : Ring α] [inst_2 : IsTopologicalRing α]
  [inst_3 : IsUniformAddGroup α] [inst_4 : Ring β] [inst_5 : PseudoMetricSpace β] [inst_6 : IsUniformAddGroup β]
  [inst_7 : IsTopologicalRing β] [inst_8 : CompleteSpace β] [inst_9 : T0Space β] {f : α →+* β} (h : Isometry ⇑f)
  (x : α), h.extensionHom ↑x = f x
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
DiscreteConvolution.addFiber_zero_mem : ∀ {M : Type u_1} [inst : AddMonoid M], (0, 0) ∈ DiscreteConvolution.addFiber 0
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.instFintypeSubtypeListProdBoolRed : {α : Type u_1} → [DecidableEq α] → (L₁ : List (α × Bool)) → Fintype { L₂ // FreeGroup.Red L₁ L₂ }
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.link!.eq_def : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.link! k v l r =
    match l with
    | Std.DTreeMap.Internal.Impl.leaf => Std.DTreeMap.Internal.Impl.insertMin! k v r
    | l@h:(Std.DTreeMap.Internal.Impl.inner szl k' v' l' r') =>
      match r with
      | Std.DTreeMap.Internal.Impl.leaf => Std.DTreeMap.Internal.Impl.insertMax! k v l
      | r@h:(Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'') =>
        if Std.DTreeMap.Internal.delta * szl < szr then
          Std.DTreeMap.Internal.Impl.balanceL! k'' v'' (Std.DTreeMap.Internal.Impl.link! k v l l'') r''
        else
          if Std.DTreeMap.Internal.delta * szr < szl then
            Std.DTreeMap.Internal.Impl.balanceR! k' v' l' (Std.DTreeMap.Internal.Impl.link! k v r' r)
          else Std.DTreeMap.Internal.Impl.inner (l.size + 1 + r.size) k v l r
-- Lean.Declaration
Lean.ConstructorVal.mk.injEq : ∀ (toConstantVal : Lean.ConstantVal) (induct : Lean.Name) (cidx numParams numFields : ℕ) (isUnsafe : Bool)
  (toConstantVal_1 : Lean.ConstantVal) (induct_1 : Lean.Name) (cidx_1 numParams_1 numFields_1 : ℕ) (isUnsafe_1 : Bool),
  ({ toConstantVal := toConstantVal, induct := induct, cidx := cidx, numParams := numParams, numFields := numFields,
        isUnsafe := isUnsafe } =
      { toConstantVal := toConstantVal_1, induct := induct_1, cidx := cidx_1, numParams := numParams_1,
        numFields := numFields_1, isUnsafe := isUnsafe_1 }) =
    (toConstantVal = toConstantVal_1 ∧
      induct = induct_1 ∧ cidx = cidx_1 ∧ numParams = numParams_1 ∧ numFields = numFields_1 ∧ isUnsafe = isUnsafe_1)
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
Ordinal.CNF.coeff_eq_zero_of_lt : ∀ {b o e : Ordinal.{u_1}}, o < b ^ e → (Ordinal.CNF.coeff b o) e = 0
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.subsingleton_of_unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (A B : Cᵒᵖ)
  [Subsingleton (Opposite.unop B ⟶ Opposite.unop A)], Subsingleton (A ⟶ B)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- `caseSplits` is `true` if linarith is searching for model and already performed case splits.
This information is used to decide whether a conflict should immediately close the
current `grind` goal or not.
 -/
Lean.Meta.Grind.Arith.Linear.Struct.caseSplits : Lean.Meta.Grind.Arith.Linear.Struct → Bool
-- Mathlib.Order.Hom.Lattice
InfHom.ext : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : Min β] {f g : InfHom α β}, (∀ (a : α), f a = g a) → f = g
-- Mathlib.Tactic.FunProp.Theorems
/-- return proof of function theorem  -/
Mathlib.Meta.FunProp.FunctionTheorem.getProof : Mathlib.Meta.FunProp.FunctionTheorem → Lean.MetaM Lean.Expr
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.ofSnowflaking_toSnowflaking : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} (x : X),
  Metric.Snowflaking.ofSnowflaking (Metric.Snowflaking.toSnowflaking x) = x
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.Functor.instIsEquivalenceQuotientHomRelLift : ∀ {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] (L : CategoryTheory.Functor C D) [L.Full] [L.EssSurj],
  (CategoryTheory.Quotient.lift L.homRel L ⋯).IsEquivalence
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- A version of `UniformOnFun.hasBasis_nhds_of_basis`
with weaker conclusion and weaker assumptions.

We make no assumptions about the set `𝔖`
but conclude only that the neighbourhoods filter is equal to some indexed infimum.  -/
UniformOnFun.nhds_eq_of_basis : ∀ {α : Type u_1} (β : Type u_2) [inst : UniformSpace β] (𝔖 : Set (Set α)) {ι : Sort u_5} {p : ι → Prop}
  {V : ι → Set (β × β)},
  (uniformity β).HasBasis p V →
    ∀ (f : UniformOnFun α β 𝔖),
      nhds f =
        ⨅ s ∈ 𝔖,
          ⨅ i,
            ⨅ (_ : p i), Filter.principal {g | ∀ x ∈ s, ((UniformOnFun.toFun 𝔖) f x, (UniformOnFun.toFun 𝔖) g x) ∈ V i}
-- Mathlib.Algebra.Order.Monoid.Defs
IsOrderedCancelMonoid.toMulRightReflectLT : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : PartialOrder α] [IsOrderedCancelMonoid α], MulRightReflectLT α
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.SimpleFunc.setToL1S_nonneg : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {G'' : Type u_7} {G' : Type u_8}
  [inst : NormedAddCommGroup G'] [inst_1 : PartialOrder G'] [IsOrderedAddMonoid G'] [inst_3 : NormedSpace ℝ G']
  [inst_4 : NormedAddCommGroup G''] [inst_5 : PartialOrder G''] [inst_6 : NormedSpace ℝ G''] {T : Set α → G'' →L[ℝ] G'},
  (∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0) →
    MeasureTheory.FinMeasAdditive μ T →
      (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G''), 0 ≤ x → 0 ≤ (T s) x) →
        ∀ {f : ↥(α →₁ₛ[μ] G'')}, 0 ≤ f → 0 ≤ MeasureTheory.L1.SimpleFunc.setToL1S T f
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
DifferentiableWithinAt.sin : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {s : Set E},
  DifferentiableWithinAt ℝ f s x → DifferentiableWithinAt ℝ (fun x => Real.sin (f x)) s x
-- Mathlib.Analysis.SpecialFunctions.Exponential
/-- The exponential map in a commutative Banach algebra `𝔸` over a normed field `𝕂` of
characteristic zero has Fréchet derivative `NormedSpace.exp x • 1 : 𝔸 →L[𝕂] 𝔸`
at any point `x` in the disk of convergence.  -/
hasFDerivAt_exp_of_mem_ball : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕂] [inst_1 : NormedCommRing 𝔸]
  [inst_2 : NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] [CharZero 𝕂] {x : 𝔸},
  x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius → HasFDerivAt NormedSpace.exp (NormedSpace.exp x • 1) x
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey_modifyKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [inst_3 : Std.LawfulBEqOrd α]
  [inst_4 : Std.LawfulEqOrd α] {k : α} {f : β k → β k} {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {he : (Std.Internal.List.modifyKey k f l).isEmpty = false},
      Std.Internal.List.minKey (Std.Internal.List.modifyKey k f l) he = Std.Internal.List.minKey l ⋯
-- Batteries.Control.OptionT
OptionT.run_monadLift : ∀ {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {α : Type u_1} [inst : Monad m] [LawfulMonad m]
  [inst_2 : MonadLiftT n m] (x : n α), (monadLift x).run = some <$> monadLift x
-- Mathlib.LinearAlgebra.TensorProduct.RightExactness
/-- The inverse map in `rTensor.equiv`  -/
rTensor.inverse : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      {P : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : AddCommGroup N] →
              [inst_3 : AddCommGroup P] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : Module R P] →
                      {f : M →ₗ[R] N} →
                        {g : N →ₗ[R] P} →
                          (Q : Type u_5) →
                            [inst_7 : AddCommGroup Q] →
                              [inst_8 : Module R Q] →
                                Function.Exact ⇑f ⇑g →
                                  Function.Surjective ⇑g →
                                    TensorProduct R P Q →ₗ[R] TensorProduct R N Q ⧸ (LinearMap.rTensor Q f).range
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.aleph0_mul_mk_eq : ∀ {α : Type u_1} [Infinite α], Cardinal.aleph0 * Cardinal.mk α = Cardinal.mk α
-- Mathlib.CategoryTheory.Limits.Types.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.sectionsEquiv_symm_apply_val : ∀ {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J (Type u))
  (s : ↑I.multicospan.sections) (i : J.L),
  (I.sectionsEquiv.symm s).val i = ↑s (CategoryTheory.Limits.WalkingMulticospan.left i)
-- Mathlib.Order.Category.DistLat
DistLat.Iso.mk_inv : ∀ {α β : DistLat} (e : ↑α ≃o ↑β),
  (DistLat.Iso.mk e).inv = DistLat.ofHom { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X Y : CategoryTheory.Comon C} {f g : X ⟶ Y}, f.hom = g.hom → f = g
-- Mathlib.Topology.Algebra.Group.Torsor
/-- The underlying group of a topological additive torsor is a topological additive
group. This is not an instance, as `P` cannot be inferred.  -/
IsTopologicalAddTorsor.to_isTopologicalAddGroup : ∀ (V : Type u_1) (P : Type u_2) [inst : AddGroup V] [inst_1 : TopologicalSpace V] [inst_2 : AddTorsor V P]
  [inst_3 : TopologicalSpace P] [IsTopologicalAddTorsor P], IsTopologicalAddGroup V
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
Ordinal.CNF.opow_mul_add : ∀ {b e x y : Ordinal.{u_1}},
  1 < b → x ≠ 0 → x < b → y < b ^ e → Ordinal.CNF b (b ^ e * x + y) = (e, x) :: Ordinal.CNF b y
-- Mathlib.Topology.Order.DenselyOrdered
closure_interior_Icc : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a b : α},
  a ≠ b → closure (interior (Set.Icc a b)) = Set.Icc a b
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
/-- The permutation group `Equiv.Perm α` acts `n`-pretransitively on `α` for all `n`.  -/
Equiv.Perm.isMultiplyPretransitive : ∀ (α : Type u_1) (n : ℕ), MulAction.IsMultiplyPretransitive (Equiv.Perm α) α n
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.BoolExpr.eval_literal : ∀ {α : Type} {a : α → Bool} {l : α}, Std.Tactic.BVDecide.BoolExpr.eval a (Std.Tactic.BVDecide.BoolExpr.literal l) = a l
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.poly_eq_zero_eq_false : ∀ (ctx : Int.Internal.Linear.Context) {p : Int.Internal.Linear.Poly} {k : ℤ},
  Int.Internal.Linear.Poly.divCoeffs k p = true →
    k > 0 → Int.Internal.Linear.cmod p.getConst k < 0 → (Int.Internal.Linear.Poly.denote ctx p = 0) = False
-- Mathlib.Order.Category.DistLat
DistLat.hom_comp : ∀ {X Y Z : DistLat} (f : X ⟶ Y) (g : Y ⟶ Z),
  DistLat.Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (DistLat.Hom.hom g).comp (DistLat.Hom.hom f)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.Ioc_add_Ico_subset : ∀ {α : Type u_1} [inst : Add α] [inst_1 : PartialOrder α] [AddLeftStrictMono α] [AddRightStrictMono α] (a b c d : α),
  Set.Ioc a b + Set.Ico c d ⊆ Set.Ioo (a + c) (b + d)
-- Mathlib.Data.Ordmap.Invariants
_private.Mathlib.Data.Ordmap.Invariants.0.Ordnode.splitMax'.match_3.splitter : {α : Type u_1} →
  (motive : Ordnode α → α → Ordnode α → Sort u_2) →
    (x : Ordnode α) →
      (x_1 : α) →
        (x_2 : Ordnode α) →
          ((l : Ordnode α) → (x : α) → motive l x Ordnode.nil) →
            ((l : Ordnode α) →
                (x : α) →
                  (size : ℕ) →
                    (rl : Ordnode α) → (rx : α) → (rr : Ordnode α) → motive l x (Ordnode.node size rl rx rr)) →
              motive x x_1 x_2
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
Matrix.ProjGenLinGroup.mk_scalar : ∀ {n : Type u_1} {R : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R] (u : Rˣ),
  Matrix.ProjGenLinGroup.mk ((Matrix.GeneralLinearGroup.scalar n) u) = 1
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.ext_iff : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  {e e' : A ≃ₐc[R] B}, e = e' ↔ ∀ (x : A), e x = e' x
-- Init.Data.List.Nat.Erase
List.eraseIdx_eq_dropLast : ∀ {α : Type u_1} {l : List α} {i : ℕ}, i + 1 = l.length → l.eraseIdx i = l.dropLast
-- Mathlib.Analysis.Normed.Group.Basic
/-- An analogue of `nnnorm_le_mul_nnnorm_add` for the multiplication from the left.  -/
nnnorm_le_mul_nnnorm_add' : ∀ {E : Type u_5} [inst : SeminormedGroup E] (a b : E), ‖b‖₊ ≤ ‖a * b‖₊ + ‖a‖₊
-- Mathlib.RingTheory.Spectrum.Prime.Basic
/-- `zeroLocus` and `vanishingIdeal` form a Galois connection.  -/
PrimeSpectrum.gc_set : ∀ (R : Type u) [inst : CommSemiring R],
  GaloisConnection (fun s => PrimeSpectrum.zeroLocus s) fun t => ↑(PrimeSpectrum.vanishingIdeal t)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey?_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {km : α}, t.maxKey? = some km → km ∈ t
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.locallyIntegrableOn_zero : ∀ {X : Type u_1} {ε'' : Type u_5} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace ε''] [inst_3 : ESeminormedAddMonoid ε''] {μ : MeasureTheory.Measure X} {s : Set X},
  MeasureTheory.LocallyIntegrableOn (fun x => 0) s μ
-- Init.Data.SInt.Lemmas
Int8.toBitVec_ofIntClamp : ∀ {n : ℤ}, Int8.minValue.toInt ≤ n → n ≤ Int8.maxValue.toInt → (Int8.ofIntClamp n).toBitVec = BitVec.ofInt 8 n
-- Mathlib.Topology.UniformSpace.Equiv
/-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
because it is a composition of multiple projections.  -/
UniformEquiv.Simps.apply : {α : Type u} → {β : Type u_1} → [inst : UniformSpace α] → [inst_1 : UniformSpace β] → α ≃ᵤ β → α → β
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.IsIndex.unique : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} {x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N} {d : ℕ}
  {hd : x.dim = d} {l : Fin d},
  SSet.prodStdSimplex.pairingCore.IsIndex x hd l.succ →
    ∀ {l' : Fin d}, SSet.prodStdSimplex.pairingCore.IsIndex x hd l'.succ → l = l'
-- Std.Data.TreeMap.Raw.Lemmas
/-- Simpler variant of `getD_filter` when `LawfulEqCmp` is available.  -/
Std.TreeMap.Raw.getD_filter' : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {f : α → β → Bool} {k : α} {fallback : β},
  t.WF → (Std.TreeMap.Raw.filter f t).getD k fallback = (Option.filter (f k) t[k]?).getD fallback
-- Mathlib.Order.Interval.Finset.Defs
WithBot.Ioo_bot_coe : ∀ (α : Type u_1) [inst : PartialOrder α] [inst_1 : OrderBot α] [inst_2 : LocallyFiniteOrder α] (a : α),
  Finset.Ioo ⊥ ↑a = Finset.map Function.Embedding.some (Finset.Iio a)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.append_nil : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.append SimpleGraph.Walk.nil = p
-- Lean.Meta.Tactic.Grind.Intro
_private.Lean.Meta.Tactic.Grind.Intro.0.Lean.Meta.Grind.applyInjection? : Lean.Meta.Grind.Goal → Lean.FVarId → Lean.MetaM (Option Lean.Meta.Grind.Goal)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.cokernelIsoOfEq.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f g : X ⟶ Y} [inst_2 : CategoryTheory.Limits.HasCokernel f] [inst_3 : CategoryTheory.Limits.HasCokernel g]
  (h : f = g), CategoryTheory.Limits.cokernelIsoOfEq h = CategoryTheory.Limits.cokernelIsoOfEq h
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.Augmented.whiskering_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (D : Type u') [inst_1 : CategoryTheory.Category.{v', u'} D]
  (F : CategoryTheory.Functor C D),
  (CategoryTheory.CosimplicialObject.Augmented.whiskering C D).obj F =
    CategoryTheory.CosimplicialObject.Augmented.whiskeringObj C D F
-- Mathlib.NumberTheory.Divisors
_private.Mathlib.NumberTheory.Divisors.0.Int.divisorsAntidiag.match_1.eq_2 : ∀ (motive : ℤ → Sort u_1) (n : ℕ) (h_1 : (n : ℕ) → motive (Int.ofNat n)) (h_2 : (n : ℕ) → motive (Int.negSucc n)),
  (match Int.negSucc n with
    | Int.ofNat n => h_1 n
    | Int.negSucc n => h_2 n) =
    h_2 n
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
/-- The natural isomorphism (in `Karoubi (ChainComplex C ℕ)`) between the chain complex
of nondegenerate simplices of a split simplicial object and the normalized Moore complex
defined as a formal direct factor of the alternating face map complex.  -/
CategoryTheory.SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      CategoryTheory.SimplicialObject.Split.nondegComplexFunctor.comp
          (CategoryTheory.Idempotents.toKaroubi (ChainComplex C ℕ)) ≅
        (CategoryTheory.SimplicialObject.Split.forget C).comp AlgebraicTopology.DoldKan.N₁
-- Mathlib.Order.Filter.Pointwise
/-- `a +ᵥ f` is the map of `f` under `a +ᵥ` in scope `Pointwise`.  -/
Filter.instVAddFilter : {α : Type u_2} → {β : Type u_3} → [VAdd α β] → VAdd α (Filter β)
-- Mathlib.ModelTheory.Types
FirstOrder.Language.Theory.CompleteType.not_mem_iff : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} (p : T.CompleteType α) (φ : (L.withConstants α).Sentence),
  FirstOrder.Language.Formula.not φ ∈ p ↔ φ ∉ p
-- Mathlib.Data.Finset.MulAntidiagonal
/-- **Alias** of `Finset.support_antidiagonal_subset_add`. -/
Finset.support_addAntidiagonal_subset_add : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelAddMonoid α] {s t : Set α}
  {hs : s.IsPWO} {ht : t.IsPWO}, {a | (Finset.antidiagonal hs ht a).Nonempty} ⊆ s + t
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
CategoryTheory.Functor.LaxMonoidal.ofBifunctor.leftMapᵣ_app : ∀ {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] [inst_2 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) (X : C),
  (CategoryTheory.Functor.LaxMonoidal.ofBifunctor.leftMapᵣ F).app X =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj X)).hom
-- Init.Data.Vector.Algebra
Vector.right_distrib : ∀ {α : Type u_1} {n : ℕ} [inst : Add α] [inst_1 : Mul α],
  (∀ (x y z : α), (x + y) * z = x * z + y * z) → ∀ (xs ys zs : Vector α n), (xs + ys) * zs = xs * zs + ys * zs
-- Mathlib.Algebra.Group.End
/-- **Alias** of `AddAut.symm_neg`. -/
AddAut.symm_inv : ∀ (M : Type u_2) [inst : Add M] (e : AddAut M), -AddEquiv.symm e = e
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.ExplorationStep.gt.sizeOf_spec : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {k : α → Ordering} [inst_1 : SizeOf α] [inst_2 : (a : α) → SizeOf (β a)]
  (a : List ((a : α) × β a)) (a_1 : α) (a_2 : k a_1 = Ordering.gt) (a_3 : β a_1),
  sizeOf (Std.DTreeMap.Internal.Impl.ExplorationStep.gt a a_1 a_2 a_3) =
    1 + sizeOf a + sizeOf a_1 + sizeOf a_2 + sizeOf a_3
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
/-- The submodule generated by products `Pm * Pn` of weighted homogeneous polynomials of degrees `m`
and `n` is contained in the submodule of weighted homogeneous polynomials of degree `m + n`.  -/
MvPolynomial.weightedHomogeneousSubmodule_mul : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] (w : σ → M) (m n : M),
  MvPolynomial.weightedHomogeneousSubmodule R w m * MvPolynomial.weightedHomogeneousSubmodule R w n ≤
    MvPolynomial.weightedHomogeneousSubmodule R w (m + n)
-- Mathlib.LinearAlgebra.FreeModule.Basic
Module.Free.instFaithfulSMulOfNontrivial : ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M]
  [Nontrivial M], FaithfulSMul R M
-- Mathlib.MeasureTheory.Integral.IntegrableOn
/-- Eta-expanded form of `MeasureTheory.IntegrableOn.neg` -/
MeasureTheory.IntegrableOn.fun_neg : ∀ {α : Type u_1} {E : Type u_5} {mα : MeasurableSpace α} [inst : NormedAddCommGroup E] {s : Set α}
  {μ : MeasureTheory.Measure α} {f : α → E},
  MeasureTheory.IntegrableOn f s μ → MeasureTheory.IntegrableOn (fun i => -f i) s μ
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_mono : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [inst_2 : PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E]
  [ClosedIciTopology E] {f g : α → E},
  MeasureTheory.Integrable f μ → MeasureTheory.Integrable g μ → f ≤ g → ∫ (x : α), f x ∂μ ≤ ∫ (x : α), g x ∂μ
-- Mathlib.Data.Set.Pairwise.Lattice
/-- Bind operation for `Set.PairwiseDisjoint`. If you want to only consider finsets of indices, you
can use `Set.PairwiseDisjoint.biUnion_finset`.  -/
Set.PairwiseDisjoint.biUnion : ∀ {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} [inst : CompleteLattice α] {s : Set ι'} {g : ι' → Set ι} {f : ι → α},
  (s.PairwiseDisjoint fun i' => ⨆ i ∈ g i', f i) →
    (∀ i ∈ s, (g i).PairwiseDisjoint f) → (⋃ i ∈ s, g i).PairwiseDisjoint f
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.b.congr_simp : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] (f : P.RankFunction ι)
  [inst_1 : P.IsProper] [inst_2 : SuccOrder ι] [inst_3 : NoMaxOrder ι] (j : ι), f.b j = f.b j
-- Mathlib.Analysis.Normed.Lp.Matrix
/-- Note that applying this theorem needs an explicit choice of `q`.  -/
Matrix.toLpLin_symm_comp : ∀ {m : Type u_1} {n : Type u_2} {o : Type u_3} {R : Type u_4} [inst : Fintype n] [inst_1 : DecidableEq n]
  [inst_2 : CommRing R] (p q r : ENNReal) [inst_3 : Fintype o] [inst_4 : DecidableEq o]
  (A : WithLp q (n → R) →ₗ[R] WithLp r (m → R)) (B : WithLp p (o → R) →ₗ[R] WithLp q (n → R)),
  (Matrix.toLpLin p r).symm (A ∘ₗ B) = (Matrix.toLpLin q r).symm A * (Matrix.toLpLin p q).symm B
-- Std.Data.DTreeMap.Basic
/-- Given a proof that a mapping for the given key is present, retrieves the mapping for the given key.

Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 -/
Std.DTreeMap.Const.get : {α : Type u} → {cmp : α → α → Ordering} → {β : Type v} → (t : Std.DTreeMap α (fun x => β) cmp) → (a : α) → a ∈ t → β
-- Mathlib.LinearAlgebra.Span.TensorProduct
Submodule.finrank_span_eq_finrank : ∀ {R : Type u_1} (A : Type u_2) {M : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [Nontrivial A]
  [inst_3 : Algebra R A] [Algebra.IsEpi R A] [Module.Flat R A] [inst_6 : AddCommGroup M] [inst_7 : Module R M]
  [inst_8 : Module A M] [IsScalarTower R A M] (p : Submodule R M) [Module.Free R ↥p] [Module.Finite R ↥p],
  Module.finrank A ↥(Submodule.span A ↑p) = Module.finrank R ↥p
-- Init.Omega.Constraint
/-- `positivize` and `normalize`  -/
Lean.Omega.tidy : Lean.Omega.Constraint × Lean.Omega.Coeffs → Lean.Omega.Constraint × Lean.Omega.Coeffs
-- Mathlib.Algebra.Group.AddChar
/-- Define coercion to a function.  -/
AddChar.instFunLike : {A : Type u_1} → {M : Type u_3} → [inst : AddMonoid A] → [inst_1 : Monoid M] → FunLike (AddChar A M) A M
-- Mathlib.Topology.Algebra.InfiniteSum.Ring
/-- The infinite version of `Finset.prod_one_sub_ordered`.  -/
tprod_one_sub_ordered : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : LocallyFiniteOrderBot ι] {α : Type u_4} {f : ι → α}
  [inst_2 : CommRing α] [inst_3 : TopologicalSpace α] [T2Space α] [IsTopologicalAddGroup α],
  (Summable fun i => f i * ∏ j < i, (1 - f j)) →
    (Multipliable fun x => 1 - f x) → ∏' (i : ι), (1 - f i) = 1 - ∑' (i : ι), f i * ∏ j < i, (1 - f j)