mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
CoassocSimps.lid_symm_comp : ∀ {R : Type u_1} {M : Type u_3} {M' : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (f : M →ₗ[R] M'),
  ↑(TensorProduct.lid R M').symm ∘ₗ f = TensorProduct.map LinearMap.id f ∘ₗ ↑(TensorProduct.lid R M).symm
-- Mathlib.Algebra.Algebra.Epi
/-- If an `R`-algebra `A` is epi, then the scalar multiplication `A ⊗[R] M → M` is injective, for
any `A`-module `M`.  -/
Algebra.injective_lift_lsmul : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  [Algebra.IsEpi R A] (M : Type u_3) [inst_4 : AddCommMonoid M] [inst_5 : Module R M] [inst_6 : Module A M]
  [inst_7 : IsScalarTower R A M],
  Function.Injective ⇑(TensorProduct.lift (LinearMap.restrictScalars₁₂ R R (LinearMap.lsmul A M)))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey?_eq_getLast?_keys : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → t.maxKey? = t.keys.getLast?
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.find?_toList_eq_none_iff_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α}, List.find? (fun x => cmp x.1 k == Ordering.eq) (Std.ExtDTreeMap.Const.toList t) = none ↔ t.contains k = false
-- Mathlib.Algebra.Order.Ring.Archimedean
ArchimedeanClass.mk_ofNat : ∀ {S : Type u_3} [inst : LinearOrder S] [inst_1 : CommRing S] [inst_2 : IsStrictOrderedRing S] {n : ℕ}
  [inst_3 : n.AtLeastTwo], ArchimedeanClass.mk (OfNat.ofNat n) = 0
-- Mathlib.Combinatorics.SimpleGraph.Density
SimpleGraph.card_interedges_le_mul : ∀ {α : Type u_4} (G : SimpleGraph α) [inst : DecidableRel G.Adj] (s t : Finset α),
  (G.interedges s t).card ≤ s.card * t.card
-- Lean.Elab.ConfigEval.Commands
Lean.Elab.ConfigEval.configEntries : Lean.ParserDescr
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.restrictScalars_apply : ∀ (R : Type u_1) {S : Type u_4} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R M₂]
  [inst_6 : Module S M] [inst_7 : Module S M₂] [inst_8 : LinearMap.CompatibleSMul M M₂ R S] (f : M ≃ₗ[S] M₂) (a : M),
  (LinearEquiv.restrictScalars R f) a = f a
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.updateBaseAfterKernelAdd : Lean.Environment → Lean.Kernel.Environment → Lean.Declaration → Lean.Environment
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_erase! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {k a : α} {fallback : β a},
      (Std.DTreeMap.Internal.Impl.erase! k t).getD a fallback =
        if compare k a = Ordering.eq then fallback else t.getD a fallback
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.prodComm_toLinearEquiv : ∀ (R₁ : Type u_1) [inst : Semiring R₁] (M₁ : Type u_4) [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  (M₂ : Type u_5) [inst_3 : TopologicalSpace M₂] [inst_4 : AddCommMonoid M₂] [inst_5 : Module R₁ M₁]
  [inst_6 : Module R₁ M₂], ↑(ContinuousLinearEquiv.prodComm R₁ M₁ M₂) = LinearEquiv.prodComm R₁ M₁ M₂
-- Mathlib.MeasureTheory.Function.Floor
Measurable.ceil : ∀ {α : Type u_1} {R : Type u_2} [inst : MeasurableSpace α] [inst_1 : Ring R] [inst_2 : LinearOrder R]
  [inst_3 : FloorRing R] [inst_4 : TopologicalSpace R] [OrderTopology R] [inst_6 : MeasurableSpace R]
  [OpensMeasurableSpace R] {f : α → R}, Measurable f → Measurable fun x => ⌈f x⌉
-- Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM
PointwiseConvergenceCLM.isUniformEmbedding_coeFn : ∀ {𝕜₁ : Type u_4} {𝕜₂ : Type u_5} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) (E : Type u_7)
  (Fᵤ : Type u_9) [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup Fᵤ]
  [inst_5 : UniformSpace Fᵤ] [inst_6 : IsUniformAddGroup Fᵤ] [inst_7 : Module 𝕜₁ E] [inst_8 : Module 𝕜₂ Fᵤ],
  IsUniformEmbedding DFunLike.coe
-- Init.Control.Lawful.Instances
ExceptT.seqRight_eq : ∀ {m : Type u_1 → Type u_2} {ε α β : Type u_1} [inst : Monad m] [LawfulMonad m] (x : ExceptT ε m α) (y : ExceptT ε m β),
  x *> y = Function.const α id <$> x <*> y
-- Mathlib.RingTheory.Coalgebra.Basic
DFinsupp.counit_comp_lsingle : ∀ (R : Type u) (ι : Type v) (A : ι → Type w) [inst : DecidableEq ι] [inst_1 : CommSemiring R]
  [inst_2 : (i : ι) → AddCommMonoid (A i)] [inst_3 : (i : ι) → Module R (A i)]
  [inst_4 : (i : ι) → CoalgebraStruct R (A i)] (i : ι),
  CoalgebraStruct.counit ∘ₗ DFinsupp.lsingle i = CoalgebraStruct.counit
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Connected.mk : ∀ {V : Type u} {G : SimpleGraph V}, G.Preconnected → ∀ [nonempty : Nonempty V], G.Connected
-- Mathlib.NumberTheory.Padics.Complex
/-- `PadicAlgCl p` is a normed field, where the norm is the `p`-adic norm, that is, the
spectral norm induced by the `p`-adic norm on `ℚ_[p]`.  -/
PadicAlgCl.normedField : (p : ℕ) → [hp : Fact (Nat.Prime p)] → NormedField (PadicAlgCl p)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- If the directions of two nonempty affine subspaces are complements of each other, they intersect
in exactly one point.  -/
AffineSubspace.inter_eq_singleton_of_nonempty_of_isCompl : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {s₁ s₂ : AffineSubspace k P},
  (↑s₁).Nonempty → (↑s₂).Nonempty → IsCompl s₁.direction s₂.direction → ∃ p, ↑s₁ ∩ ↑s₂ = {p}
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- Being initial is independent of the empty diagram, its universe, and the cocone over it,
as long as the cocone points are isomorphic.  -/
CategoryTheory.Limits.isColimitChangeEmptyCocone : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {F₁ : CategoryTheory.Functor (CategoryTheory.Discrete PEmpty.{w + 1}) C} →
      {F₂ : CategoryTheory.Functor (CategoryTheory.Discrete PEmpty.{w' + 1}) C} →
        {c₁ : CategoryTheory.Limits.Cocone F₁} →
          CategoryTheory.Limits.IsColimit c₁ →
            (c₂ : CategoryTheory.Limits.Cocone F₂) → (c₁.pt ≅ c₂.pt) → CategoryTheory.Limits.IsColimit c₂
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
/-- The `degreeOf` a variable `i` for a polynomial `p` is a special case of the
`weightedTotalDegree` of `p` where `i` has the only nonzero weight and that weight is `1`.  -/
MvPolynomial.weightedTotalDegree_piSingle : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] [inst_1 : DecidableEq σ] (i : σ) (p : MvPolynomial σ R),
  MvPolynomial.weightedTotalDegree (Pi.single i 1) p = MvPolynomial.degreeOf i p
-- Std.Time.DateTime.Timestamp
/-- Adds a `Day.Offset` to the given `Timestamp`.
 -/
Std.Time.Timestamp.addDays : Std.Time.Timestamp → Std.Time.Day.Offset → Std.Time.Timestamp
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.levelMVarToParamHeaders.process : Array Lean.Elab.DefView →
  Array Lean.Elab.DefViewElabHeader → StateRefT' IO.RealWorld ℕ Lean.Elab.TermElabM (Array Lean.Elab.DefViewElabHeader)
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks
/-- The pullback cone reconstructed using `PullbackCone.mk` from a pullback cone that is a
weak limit, is also a weak limit.  -/
CategoryTheory.Limits.PullbackCone.mkSelfIsWeakLimit : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y Z : C} →
      {f : X ⟶ Z} →
        {g : Y ⟶ Z} →
          {t : CategoryTheory.Limits.PullbackCone f g} →
            CategoryTheory.Limits.IsWeakLimit t →
              CategoryTheory.Limits.IsWeakLimit (CategoryTheory.Limits.PullbackCone.mk t.fst t.snd ⋯)
-- Mathlib.Analysis.Calculus.Deriv.Basic
/-- This theorem holds for any T2 TVS, see `isClosedEmbedding_smul_left`,
but this would require more imports.

The proof for a TVS is more complicated, and we wouldn't benefit from that form here,
so we prove a weaker version as a private lemma instead.  -/
_private.Mathlib.Analysis.Calculus.Deriv.Basic.0.isInducing_toSpanSingleton : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f' : F}, f' ≠ 0 → Topology.IsInducing ⇑(ContinuousLinearMap.toSpanSingleton 𝕜 f')
-- Mathlib.CategoryTheory.ObjectProperty.Kernels
CategoryTheory.ObjectProperty.IsClosedUnderKernels.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P : CategoryTheory.ObjectProperty C},
  (CategoryTheory.MorphismProperty.ofObjectProperty P P).kernels ≤ P → P.IsClosedUnderKernels
-- Std.Time.Time.Unit.Second
Std.Time.Second.instLEOffset : LE Std.Time.Second.Offset
-- Init.Data.SInt.Bitwise
ISize.shiftRight_xor : ∀ {a b c : ISize}, (a ^^^ b) >>> c = a >>> c ^^^ b >>> c
-- Mathlib.Algebra.Order.GroupWithZero.Defs
PosMulStrictMono.toMulPosStrictMono : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [IsMulCommutative α] [PosMulStrictMono α],
  MulPosStrictMono α
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.ofInjective.eq_1 : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {f : G →* N} (hf : Function.Injective ⇑f),
  MonoidHom.ofInjective hf = MulEquiv.ofBijective (f.codRestrict f.range ⋯) ⋯
-- Mathlib.Order.GaloisConnection.Basic
GaloisInsertion.liftSemilatticeInf.eq_1 : ∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : PartialOrder β] [inst_1 : SemilatticeInf α]
  (gi : GaloisInsertion l u),
  gi.liftSemilatticeInf =
    { toPartialOrder := inst, inf := fun a b => gi.choice (u a ⊓ u b) ⋯, inf_le_left := ⋯, inf_le_right := ⋯,
      le_inf := ⋯ }
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.entryAtIdx.match_1.eq_3 : ∀ (motive : Ordering → Sort u_1) (h_1 : Ordering.gt = Ordering.lt → motive Ordering.lt)
  (h_2 : Ordering.gt = Ordering.eq → motive Ordering.eq) (h_3 : Ordering.gt = Ordering.gt → motive Ordering.gt),
  (match h : Ordering.gt with
    | Ordering.lt => h_1 h
    | Ordering.eq => h_2 h
    | Ordering.gt => h_3 h) =
    h_3 ⋯
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get?_emptyc : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] {a : α}, Std.DTreeMap.Const.get? ∅ a = none
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
/-- A low-dimensional special case of the previous  -/
_private.Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono.0.SimplexCategoryGenRel.switch_δ_σ₀ : ∀ (i : Fin 1) (i' : Fin 2),
  CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.δ i') (SimplexCategoryGenRel.σ i) =
    CategoryTheory.CategoryStruct.id (SimplexCategoryGenRel.mk 0)
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.flatMapTR.go.eq_def : ∀ {α : Type u_1} {β : Type u_2} (f : α → List β) (a : List α) (a_1 : Array β),
  List.flatMapTR.go✝ f a a_1 =
    match a, a_1 with
    | [], acc => acc.toList
    | x :: xs, acc => List.flatMapTR.go✝ f xs (acc ++ f x)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get_insertMany_list_of_mem : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {l : List α} {k : α} (mem : k ∈ m) {h₃ : k ∈ m.insertMany l}, (m.insertMany l).get k h₃ = m.get k mem
-- Init.Data.Slice.Array.Lemmas
Array.mkSlice_rio_eq_mkSlice_rco : ∀ {α : Type u_1} {xs : Array α} {hi : ℕ}, (Std.Rio.Sliceable.mkSlice xs *...hi) = Std.Rco.Sliceable.mkSlice xs 0...hi
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_tryCatch_lift_ExceptT_apply_eq : ∀ {Pred : Type u_1} {EPred : Type u_2} {ε : Type u} {m : Type u → Type v} [inst : Monad m]
  [inst_1 : Std.Internal.Do.Assertion Pred] [inst_2 : Std.Internal.Do.Assertion EPred]
  [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] [inst_4 : MonadExceptOf ε m] {ε' α : Type u} {post : α → Pred}
  {epost : EPost.Cons✝ (ε' → Pred) EPred} (x : ExceptT ε' m α) (h : ε → ExceptT ε' m α),
  Std.Internal.Do.wp (MonadExceptOf.tryCatch x h) post epost =
    Std.Internal.Do.wp (MonadExceptOf.tryCatch x h) (Std.Internal.Do.EPost.Cons.pushExcept post epost) epost.tail
-- Mathlib.Algebra.Group.Nat.Hom
powersHom_symm_apply : ∀ {M : Type u_1} [inst : Monoid M] (f : Multiplicative ℕ →* M), (powersHom M).symm f = f (Multiplicative.ofAdd 1)
-- Mathlib.GroupTheory.GroupAction.FixedPoints
MulAction.mem_fixedBy_zpow : ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {g : G} {a : α},
  a ∈ MulAction.fixedBy α g → ∀ (j : ℤ), a ∈ MulAction.fixedBy α (g ^ j)
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- Adding a point in the affine span of a set does not change whether that set is collinear.  -/
collinear_insert_iff_of_mem_affineSpan : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : Set P} {p : P}, p ∈ affineSpan k s → (Collinear k (insert p s) ↔ Collinear k s)
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
/-- The set of affine maps to a vector space is an additive commutative group.  -/
AffineMap.instAddCommGroup : {k : Type u_1} →
  {V1 : Type u_2} →
    {P1 : Type u_3} →
      {V2 : Type u_4} →
        [inst : Ring k] →
          [inst_1 : AddCommGroup V1] →
            [inst_2 : Module k V1] →
              [inst_3 : AddTorsor V1 P1] →
                [inst_4 : AddCommGroup V2] → [inst_5 : Module k V2] → AddCommGroup (P1 →ᵃ[k] V2)
-- Lean.Meta.Tactic.FVarSubst
Lean.Meta.FVarSubst.contains : Lean.Meta.FVarSubst → Lean.FVarId → Bool
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.Nontrivial.pow : ∀ {α : Type u_2} [inst : CancelMonoid α] {s : Set α}, s.Nontrivial → ∀ {n : ℕ}, n ≠ 0 → (s ^ n).Nontrivial
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.derivWeierstrassPExcept_neg : ∀ (L : PeriodPair) (l₀ z : ℂ), L.derivWeierstrassPExcept l₀ (-z) = -L.derivWeierstrassPExcept (-l₀) z
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift
Std.IterM.count_uLift : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {n : Type (max u_1 u_3) → Type u_4} {β : Type u_1}
  [inst : Std.Iterator α m β] [inst_1 : Monad m] [inst_2 : Monad n] {it : Std.IterM m β}
  [inst_3 : MonadLiftT m (Std.Iterators.ULiftT n)] [Std.Iterators.Finite α m] [inst_5 : Std.IteratorLoop α m m]
  [LawfulMonad m] [LawfulMonad n] [Std.LawfulIteratorLoop α m m] [LawfulMonadLiftT m (Std.Iterators.ULiftT n)],
  (it.uLift n).length = (fun x => { down := x.down.down }) <$> (monadLift it.length).run
-- Init.Data.UInt.Lemmas
UInt8.zero_def : 0 = { toBitVec := 0 }
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.transpose_submatrix : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} (A : Matrix m n α) (r : l → m) (c : o → n),
  (A.submatrix r c).transpose = A.transpose.submatrix c r
-- Mathlib.Order.Monotone.Basic
antitone_add_nat_of_succ_le : ∀ {α : Type u} [inst : Preorder α] {f : ℕ → α} {k : ℕ}, (∀ n ≥ k, f (n + 1) ≤ f n) → Antitone fun n => f (n + k)
-- Lean.Meta.Tactic.Simp.Arith.Nat.Basic
Lean.Meta.Simp.Arith.Nat.ToLinear.State : Type
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.dominatedFinMeasAdditive_condExpInd : ∀ {α : Type u_1} (G : Type u_4) [inst : NormedAddCommGroup G] {m m0 : MeasurableSpace α} [inst_1 : NormedSpace ℝ G]
  (hm : m ≤ m0) (μ : MeasureTheory.Measure α) [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)],
  MeasureTheory.DominatedFinMeasAdditive μ (MeasureTheory.condExpInd G hm μ) 1
-- Mathlib.Algebra.Ring.Defs
right_distrib : ∀ {R : Type v} [inst : Mul R] [inst_1 : Add R] [RightDistribClass R] (a b c : R), (a + b) * c = a * c + b * c
-- Mathlib.Data.ENat.Basic
instZeroLEOneClassENat : ZeroLEOneClass ℕ∞
-- Lean.Meta.Tactic.Grind.Arith.Linear.StructId
_private.Lean.Meta.Tactic.Grind.Arith.Linear.StructId.0.Lean.Meta.Grind.Arith.Linear.getStructId?.goCore? : Lean.Expr → Lean.Meta.Grind.GoalM (Option ℕ)
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.hasCoeToMatrix : {n : Type u} →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] → {R : Type v} → [inst_2 : CommRing R] → Coe (Matrix.SpecialLinearGroup n R) (Matrix n n R)
-- Mathlib.Order.CompleteBooleanAlgebra
CompletelyDistribLattice.toHNot : {α : Type u} → [self : CompletelyDistribLattice α] → HNot α
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
MeasurableSpace.comap_iSup : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort uι} {g : β → α} {m : ι → MeasurableSpace α},
  MeasurableSpace.comap g (⨆ i, m i) = ⨆ i, MeasurableSpace.comap g (m i)
-- Mathlib.Data.List.Basic
List.foldl_ext : ∀ {α : Type u} {β : Type v} (f g : α → β → α) (a : α) {l : List β},
  (∀ (a : α), ∀ b ∈ l, f a b = g a b) → List.foldl f a l = List.foldl g a l
-- Mathlib.Tactic.FieldSimp
_private.Mathlib.Tactic.FieldSimp.0.Mathlib.Tactic.FieldSimp.qNF.mkMulProof.match_1.eq_2 : ∀ {v : Lean.Level} {M : Q(Type v)} (motive : Mathlib.Tactic.FieldSimp.qNF M → Mathlib.Tactic.FieldSimp.qNF M → Sort u_1)
  (l : Mathlib.Tactic.FieldSimp.qNF M) (h_1 : (l : Mathlib.Tactic.FieldSimp.qNF M) → motive [] l)
  (h_2 : (l : Mathlib.Tactic.FieldSimp.qNF M) → motive l [])
  (h_3 :
    (a₁ : ℤ) →
      (x₁ : Q(«$M»)) →
        (k₁ : ℕ) →
          (t₁ : List ((ℤ × Q(«$M»)) × ℕ)) →
            (a₂ : ℤ) →
              (x₂ : Q(«$M»)) →
                (k₂ : ℕ) → (t₂ : List ((ℤ × Q(«$M»)) × ℕ)) → motive (((a₁, x₁), k₁) :: t₁) (((a₂, x₂), k₂) :: t₂)),
  (l = [] → False) →
    (match l, [] with
      | [], l => h_1 l
      | l, [] => h_2 l
      | ((a₁, x₁), k₁) :: t₁, ((a₂, x₂), k₂) :: t₂ => h_3 a₁ x₁ k₁ t₁ a₂ x₂ k₂ t₂) =
      h_2 l
-- Mathlib.Algebra.Group.TypeTags.Basic
Multiplicative.divInvMonoid : {α : Type u} → [h : SubNegMonoid α] → DivInvMonoid (Multiplicative α)
-- Mathlib.Topology.Semicontinuity.Basic
IsOpen.lowerSemicontinuousWithinAt_indicator : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {s t : Set α} {x : α} {y : β} [inst_1 : Zero β]
  [inst_2 : Preorder β], IsOpen s → 0 ≤ y → LowerSemicontinuousWithinAt (s.indicator fun _x => y) t x
-- Mathlib.Analysis.Normed.Module.FiniteDimension
/-- A weaker version of `Basis.opNorm_le` that abstracts away the value of `C`.  -/
Module.Basis.exists_opNorm_le : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type w} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace 𝕜]
  {ι : Type u_1} [Finite ι] (v : Module.Basis ι 𝕜 E),
  ∃ C > 0, ∀ {u : E →L[𝕜] F} {M : ℝ}, 0 ≤ M → (∀ (i : ι), ‖u (v i)‖ ≤ M) → ‖u‖ ≤ C * M
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Equivalence.rightOp_unitIso_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : Cᵒᵖ ≌ D) (X : C), e.rightOp.unitIso.hom.app X = (e.unitIso.inv.app (Opposite.op X)).unop
-- Init.Data.Vector.Lex
Vector.append_left_le : ∀ {α : Type u_1} {n m : ℕ} [inst : LT α] [Std.Asymm fun x1 x2 => x1 < x2] [Std.Trichotomous fun x1 x2 => x1 < x2]
  {xs : Vector α n} {ys ys' : Vector α m}, ys ≤ ys' → xs ++ ys ≤ xs ++ ys'
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.map_eq_zero_iff : ∀ {M : Type u_4} {N : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (h : M ≃+ N) {x : M}, h x = 0 ↔ x = 0
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry?_insertList : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert →
      ∀ (k : α),
        Std.Internal.List.getEntry? k (Std.Internal.List.insertList l toInsert) =
          (Std.Internal.List.getEntry? k toInsert).or (Std.Internal.List.getEntry? k l)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- The family of morphisms into a universal arrow.  -/
CategoryTheory.CostructuredArrow.IsUniversal.lift : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {T : D} →
          {S : CategoryTheory.Functor C D} →
            {f : CategoryTheory.CostructuredArrow S T} →
              f.IsUniversal → (g : CategoryTheory.CostructuredArrow S T) → g.left ⟶ f.left
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.Prototile.ext_iff : ∀ {G : Type u_1} {X : Type u_2} {inst : Group G} {inst_1 : MulAction G X} {x y : DiscreteTiling.Prototile G X},
  x = y ↔ ↑x = ↑y ∧ x.symmetries ≍ y.symmetries
-- Mathlib.Order.SuccPred.WithBot
/-- Not to be confused with `WithTop.orderPred_coe`, which is about `Order.pred`.  -/
WithTop.pred_coe : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderTop α] [inst_2 : PredOrder α] (a : α), (↑a).pred = Order.pred a
-- Mathlib.Data.TypeVec
/-- arrow composition in the category of `TypeVec`  -/
MvFunctor.«term_⊚_» : Lean.TrailingParserDescr
-- Mathlib.Data.Num.Basic
ZNum.neg : PosNum → ZNum
-- Mathlib.Order.Filter.Prod
/-- `p ∧ q` occurs frequently along the product of two filters
iff both `p` and `q` occur frequently along the corresponding filters.  -/
Filter.frequently_prod_and : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} {p : α → Prop} {q : β → Prop},
  (∃ᶠ (x : α × β) in f ×ˢ g, p x.1 ∧ q x.2) ↔ (∃ᶠ (a : α) in f, p a) ∧ ∃ᶠ (b : β) in g, q b
-- Lean.Elab.Task
/-- Given a monadic value in `TacticM`, creates a task that runs it in the current state,
returning
* a cancellation hook and
* a monadic value with the cached result (and subsequent state as it was after running).
 -/
Lean.Elab.Tactic.TacticM.asTask : {α : Type} → Lean.Elab.Tactic.TacticM α → Lean.Elab.Tactic.TacticM (BaseIO Unit × Task (Lean.Elab.Tactic.TacticM α))
-- Std.Async.UDP
/-- Creates a `Selector` that resolves once `s` has data available, up to at most `size` bytes,
and provides that data. If the socket has not been previously bound with `bind`, it is
automatically bound to `0.0.0.0` (all interfaces) with a random port.
Calling this function does starts the data wait, only when it's used with `Selectable.one` or `combine`.
It must not be called in parallel with `recv`.
 -/
Std.Async.UDP.Socket.recvSelector : Std.Async.UDP.Socket → UInt64 → Std.Async.Selector (ByteArray × Option Std.Net.SocketAddress)
-- Mathlib.Topology.Hom.Open
ContinuousOpenMap.toContinuousMap : {α : Type u_6} → {β : Type u_7} → [inst : TopologicalSpace α] → [inst_1 : TopologicalSpace β] → (α →CO β) → C(α, β)
-- Mathlib.NumberTheory.LSeries.MellinEqDirichlet
/-- Tailored version for odd Jacobi theta functions.  -/
hasSum_mellin_pi_mul_sq' : ∀ {ι : Type u_1} [Countable ι] {a : ι → ℂ} {r : ι → ℝ} {F : ℝ → ℂ} {s : ℂ},
  0 < s.re →
    (∀ t ∈ Set.Ioi 0, HasSum (fun i => a i * ↑(r i) * ↑(Real.exp (-Real.pi * r i ^ 2 * t))) (F t)) →
      (Summable fun i => ‖a i‖ / |r i| ^ s.re) →
        HasSum (fun i => (s + 1).Gammaℝ * a i * ↑(SignType.sign (r i)) / ↑|r i| ^ s) (mellin F ((s + 1) / 2))
-- Mathlib.Combinatorics.Matroid.Rank.Finite
/-- **Alias** of the reverse direction of `Matroid.IsBasis'.finite_iff_isRkFinite`. -/
Matroid.IsBasis'.finite_of_isRkFinite : ∀ {α : Type u_1} {M : Matroid α} {X I : Set α}, M.IsBasis' I X → M.IsRkFinite X → I.Finite
-- Mathlib.RingTheory.HopfAlgebra.GroupLike
IsGroupLikeElem.antipode_mul_cancel : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : HopfAlgebra R A] {a : A},
  IsGroupLikeElem R a → (HopfAlgebraStruct.antipode R) a * a = 1
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKey!_ofList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] [inst : Inhabited α] {l : List (α × β)}
  {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
      k ∈ List.map Prod.fst l → (Std.DTreeMap.Raw.Const.ofList l cmp).getKey! k' = k
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_le_one_iff_set_subsingleton : ∀ {α : Type u} {s : Set α}, Cardinal.mk ↑s ≤ 1 ↔ s.Subsingleton