mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Data.PairingHeap
Batteries.PairingHeapImp.Heap.node.injEq : ∀ {α : Type u} (a : α) (child sibling : Batteries.PairingHeapImp.Heap α) (a_1 : α)
  (child_1 sibling_1 : Batteries.PairingHeapImp.Heap α),
  (Batteries.PairingHeapImp.Heap.node a child sibling = Batteries.PairingHeapImp.Heap.node a_1 child_1 sibling_1) =
    (a = a_1 ∧ child = child_1 ∧ sibling = sibling_1)
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
/-- A functor `F` preserves finite products if it preserves all from `Discrete J` for `Finite J`.
We require this for `J = Fin n` in the definition,
then generalize to `J : Type u` in the instance.  -/
CategoryTheory.Limits.PreservesFiniteProducts : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → Prop
-- Init.Data.Option.Lemmas
Option.bind_comm : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → Option γ} (a : Option α) (b : Option β),
  (a.bind fun x => b.bind (f x)) = b.bind fun y => a.bind fun x => f x y
-- Mathlib.Data.Int.CharZero
Int.cast_div_ofNat_charZero : ∀ {k : Type u_3} [inst : DivisionRing k] [CharZero k] {m n : ℕ}, n ∣ m → ↑(↑m / ↑n) = ↑m / ↑n
-- Mathlib.Algebra.Field.Subfield.Defs
SubfieldClass.toInvMemClass : ∀ {S : Type u_1} {K : Type u_2} {inst : DivisionRing K} {inst_1 : SetLike S K} [self : SubfieldClass S K],
  InvMemClass S K
-- Mathlib.Algebra.Group.Hom.Instances
AddMonoidHom.compr₂_apply : ∀ {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddCommMonoid P] [inst_3 : AddCommMonoid Q] (f : M →+ N →+ P) (g : P →+ Q) (m : M) (n : N),
  ((f.compr₂ g) m) n = g ((f m) n)
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.instCoeSortType : CoeSort AddGrpCat (Type u)
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.ofContinuousAddEquiv.eq_1 : ∀ {G : ProfiniteAddGrp.{u}} {H : Type v} [inst : TopologicalSpace H] [inst_1 : AddGroup H]
  [inst_2 : IsTopologicalAddGroup H] (e : ↑G.toProfinite.toTop ≃ₜ+ H),
  ProfiniteAddGrp.ofContinuousAddEquiv e = ProfiniteAddGrp.of H
-- Mathlib.Data.Set.Image
Set.preimage_injective : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Injective (Set.preimage f) ↔ Function.Surjective f
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.pointwiseLeftKanExtensionCompIsoOfPreserves_fac_app_assoc : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) [inst_4 : G.PreservesPointwiseLeftKanExtension F L]
  [inst_5 : L.HasPointwiseLeftKanExtension F] (a : A) {Z : D}
  (h : G.obj ((L.pointwiseLeftKanExtension F).obj (L.obj a)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((L.pointwiseLeftKanExtensionUnit (F.comp G)).app a)
      (CategoryTheory.CategoryStruct.comp ((G.pointwiseLeftKanExtensionCompIsoOfPreserves F L).inv.app (L.obj a)) h) =
    CategoryTheory.CategoryStruct.comp (G.map ((L.pointwiseLeftKanExtensionUnit F).app a)) h
-- Mathlib.CategoryTheory.Filtered.Final
/-- The inclusion of a terminal object is final.  -/
CategoryTheory.Functor.final_const_of_isTerminal : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.IsFiltered C] {X : D} (hX : CategoryTheory.Limits.IsTerminal X),
  ((CategoryTheory.Functor.const C).obj X).Final
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minView_kv_eq_minView! : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β} {hl : l.Balanced}
  {hr : r.Balanced} {hlr : Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size r.size},
  ⟨(Std.DTreeMap.Internal.Impl.minView k v l r hl hr hlr).k, (Std.DTreeMap.Internal.Impl.minView k v l r hl hr hlr).v⟩ =
    ⟨(Std.DTreeMap.Internal.Impl.minView! k v l r).k, (Std.DTreeMap.Internal.Impl.minView! k v l r).v⟩
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_fiberwise_eq_sum_filter' : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : DecidableEq κ] (s : Finset ι)
  (t : Finset κ) (g : ι → κ) (f : κ → M), ∑ j ∈ t, ∑ i ∈ s with g i = j, f j = ∑ i ∈ s with g i ∈ t, f (g i)
-- Mathlib.Order.Hom.Lattice
LatticeHom.comp_apply : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : Lattice γ]
  (f : LatticeHom β γ) (g : LatticeHom α β) (a : α), (f.comp g) a = f (g a)
-- Mathlib.Data.Seq.Computation
/-- Bisimilarity over a sum of `Computation`s  -/
Computation.BisimO : {α : Type u} → (Computation α → Computation α → Prop) → α ⊕ Computation α → α ⊕ Computation α → Prop
-- Mathlib.Analysis.Calculus.Deriv.Pow
HasStrictDerivAt.fun_pow' : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕜 𝔸]
  {f : 𝕜 → 𝔸} {f' : 𝔸} {x : 𝕜},
  HasStrictDerivAt f f' x →
    ∀ (n : ℕ), HasStrictDerivAt (fun x => f x ^ n) (∑ i ∈ Finset.range n, f x ^ (n.pred - i) * f' * f x ^ i) x
-- Lean.Parser.Basic
_private.Lean.Parser.Basic.0.Lean.Parser.longestMatchFnAux.parse : Option Lean.Syntax → ℕ → ℕ → String.Pos.Raw → ℕ → List (Lean.Parser.Parser × ℕ) → Lean.Parser.ParserFn
-- Lean.Elab.PatternVar
Lean.Elab.Term.CollectPatternVars.Context.mk.inj : ∀ {funId : Lean.Ident} {ctorVal? : Option Lean.ConstructorVal} {explicit ellipsis : Bool}
  {paramDecls : Array (Lean.Name × Lean.BinderInfo)} {paramDeclIdx : ℕ} {namedArgs : Array Lean.Elab.Term.NamedArg}
  {usedNames : Std.HashSet Lean.Name} {args : List Lean.Elab.Term.Arg} {newArgs : Array Lean.Term}
  {funId_1 : Lean.Ident} {ctorVal?_1 : Option Lean.ConstructorVal} {explicit_1 ellipsis_1 : Bool}
  {paramDecls_1 : Array (Lean.Name × Lean.BinderInfo)} {paramDeclIdx_1 : ℕ}
  {namedArgs_1 : Array Lean.Elab.Term.NamedArg} {usedNames_1 : Std.HashSet Lean.Name} {args_1 : List Lean.Elab.Term.Arg}
  {newArgs_1 : Array Lean.Term},
  { funId := funId, ctorVal? := ctorVal?, explicit := explicit, ellipsis := ellipsis, paramDecls := paramDecls,
        paramDeclIdx := paramDeclIdx, namedArgs := namedArgs, usedNames := usedNames, args := args,
        newArgs := newArgs } =
      { funId := funId_1, ctorVal? := ctorVal?_1, explicit := explicit_1, ellipsis := ellipsis_1,
        paramDecls := paramDecls_1, paramDeclIdx := paramDeclIdx_1, namedArgs := namedArgs_1, usedNames := usedNames_1,
        args := args_1, newArgs := newArgs_1 } →
    funId = funId_1 ∧
      ctorVal? = ctorVal?_1 ∧
        explicit = explicit_1 ∧
          ellipsis = ellipsis_1 ∧
            paramDecls = paramDecls_1 ∧
              paramDeclIdx = paramDeclIdx_1 ∧
                namedArgs = namedArgs_1 ∧ usedNames = usedNames_1 ∧ args = args_1 ∧ newArgs = newArgs_1
-- Mathlib.CategoryTheory.Extensive
CategoryTheory.finitaryExtensive_of_reflective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u''} [inst_1 : CategoryTheory.Category.{v'', u''} D]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts D] [CategoryTheory.HasPullbacksOfInclusions D]
  [inst_4 : CategoryTheory.FinitaryExtensive C] {Gl : CategoryTheory.Functor C D} {Gr : CategoryTheory.Functor D C}
  (adj : Gl ⊣ Gr) [Gr.Full] [Gr.Faithful]
  [∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), CategoryTheory.Limits.HasPullback (Gr.map f) (adj.unit.app Y)]
  [∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y),
      CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (Gr.map f) (adj.unit.app Y)) Gl]
  [CategoryTheory.PreservesPullbacksOfInclusions Gl], CategoryTheory.FinitaryExtensive D
-- Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} {X Y : C} {p : X ⟶ Y} {f : F.obj ⊥ ⟶ X}
  {g : c.pt ⟶ Y} {j : J} (self : CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct c p f g j),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.homOfLE ⋯)) self.f' = f
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instSubsingleton : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_5} [Subsingleton A], Subsingleton (CStarMatrix m n A)
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpEntry.toUnfold : Lean.Name → Lean.Meta.SimpEntry
-- Mathlib.RingTheory.IntegralClosure.Algebra.Ideal
Polynomial.coeff_mem_pow_of_mem_adjoin_C_mul_X : ∀ {R : Type u_3} [inst : CommRing R] {I : Ideal R} {P : Polynomial R},
  P ∈ Algebra.adjoin R {x | ∃ r ∈ I, Polynomial.C r * Polynomial.X = x} → ∀ (i : ℕ), P.coeff i ∈ I ^ i
-- Mathlib.Analysis.Normed.Module.WeakDual
/-- A map into `WeakBilin (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜)` over `𝕜` (with `RCLike 𝕜`) is
continuous if the real parts of all the evaluation maps `a ↦ B (g a) y` are
continuous for each `y : F`.  -/
WeakBilin.continuous_of_continuous_eval_re : ∀ {α : Type u_4} {𝕜 : Type u_5} {E : Type u_6} {F : Type u_7} [inst : TopologicalSpace α] [inst_1 : RCLike 𝕜]
  [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) {g : α → WeakBilin B}, (∀ (y : F), Continuous fun a => RCLike.re ((B (g a)) y)) → Continuous g
-- Mathlib.Logic.Equiv.Option
Equiv.optionSubtypeNe_some : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (b : { b // b ≠ a }), (Equiv.optionSubtypeNe a) (some b) = ↑b
-- Mathlib.Data.PNat.Prime
PNat.Coprime.gcd_mul_left_cancel : ∀ (m : ℕ+) {n k : ℕ+}, k.Coprime n → (k * m).gcd n = m.gcd n
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
CategoryTheory.Limits.Types.binaryCoproductIso_inr_comp_inv : ∀ (X Y : Type u),
  CategoryTheory.CategoryStruct.comp (TypeCat.ofHom Sum.inr) (CategoryTheory.Limits.Types.binaryCoproductIso X Y).inv =
    CategoryTheory.Limits.coprod.inr
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_snd : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] (i : 𝒰.I₀),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso 𝒰 f g i).hom
      (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) (𝒰.f i))
      (AlgebraicGeometry.Scheme.Pullback.p2 𝒰 f g)
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.swap_inr : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (x : N),
  (Monoid.Coprod.swap M N) (Monoid.Coprod.inr x) = Monoid.Coprod.inl x
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.preΨ_three : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R), W.preΨ 3 = W.Ψ₃
-- Init.GrindInstances.ToInt
Lean.Grind.instLEUInt16UintOfNatNat : Lean.Grind.ToInt.LE UInt16 (Lean.Grind.IntInterval.uint 16)
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.mk.sizeOf_spec : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommMonoidWithZero R'] [inst_2 : SizeOf R]
  [inst_3 : SizeOf R'] (toMonoidHom : R →* R') (map_nonunit' : ∀ (a : R), ¬IsUnit a → (↑toMonoidHom).toFun a = 0),
  sizeOf { toMonoidHom := toMonoidHom, map_nonunit' := map_nonunit' } = 1 + sizeOf toMonoidHom
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- If the second of three points is weakly between the other two, and not equal to the first,
the angle at the first point is zero.  -/
Wbtw.angle₂₁₃_eq_zero_of_ne : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P}, Wbtw ℝ p₁ p₂ p₃ → p₂ ≠ p₁ → EuclideanGeometry.angle p₂ p₁ p₃ = 0
-- Mathlib.Analysis.Normed.Module.ContinuousInverse
ContinuousLinearMap.HasLeftInverse.leftInverse_leftInverse : ∀ {R : Type u_1} [inst : Semiring R] {E : Type u_2} {F : Type u_4} [inst_1 : TopologicalSpace E]
  [inst_2 : AddCommMonoid E] [inst_3 : Module R E] [inst_4 : TopologicalSpace F] [inst_5 : AddCommMonoid F]
  [inst_6 : Module R F] {f : E →L[R] F} (h : f.HasLeftInverse), Function.LeftInverse ⇑h.leftInverse ⇑f
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.symm_bijective : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E]
  [inst_7 : Module R₂ E₂], Function.Bijective LinearIsometryEquiv.symm
-- Lean.Data.KVMap
Lean.DataValue.ofBool : Bool → Lean.DataValue
-- Mathlib.Tactic.Linter.FlexibleLinter
/-- The stained location  -/
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.StainData.stained : Mathlib.Linter.Flexible.StainData✝ → Mathlib.Linter.Flexible.Stained✝
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
/-- If `(a :: l)` is `m`-admissible then a is less than all elements of `l`  -/
SimplexCategoryGenRel.IsAdmissible.head_lt : ∀ {m a : ℕ} {L : List ℕ}, SimplexCategoryGenRel.IsAdmissible m (a :: L) → ∀ a' ∈ L, a < a'
-- Mathlib.Analysis.Distribution.TemperateGrowth
/-- The product of two functions of temperate growth is again of temperate growth.

Version for scalar multiplication.  -/
Function.HasTemperateGrowth.smul : ∀ {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NontriviallyNormedField 𝕜]
  [inst_5 : NormedAlgebra ℝ 𝕜] [inst_6 : NormedSpace 𝕜 F] {f : E → 𝕜} {g : E → F},
  Function.HasTemperateGrowth f → Function.HasTemperateGrowth g → Function.HasTemperateGrowth (f • g)
-- Mathlib.Combinatorics.Enumerative.Composition
CompositionAsSet.mk.inj : ∀ {n : ℕ} {boundaries : Finset (Fin n.succ)} {zero_mem : 0 ∈ boundaries} {getLast_mem : Fin.last n ∈ boundaries}
  {boundaries_1 : Finset (Fin n.succ)} {zero_mem_1 : 0 ∈ boundaries_1} {getLast_mem_1 : Fin.last n ∈ boundaries_1},
  { boundaries := boundaries, zero_mem := zero_mem, getLast_mem := getLast_mem } =
      { boundaries := boundaries_1, zero_mem := zero_mem_1, getLast_mem := getLast_mem_1 } →
    boundaries = boundaries_1
-- Mathlib.Data.Rat.Cast.Defs
NNRat.cast_natCast : ∀ {α : Type u_3} [inst : DivisionSemiring α] (n : ℕ), ↑↑n = ↑n
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_inter : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (S S' : Submodule R M), Submodule.span R (↑S ∩ ↑S') = S ⊓ S'
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
MeasurableSet.of_mem_nhdsGT_aux : ∀ {α : Type u_1} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α] [inst_2 : LinearOrder α]
  [OrderTopology α] [SecondCountableTopology α] {s : Set α},
  (∀ x ∈ s, s ∈ nhdsWithin x (Set.Ioi x)) → (∀ x ∈ s, ∃ y, x < y) → MeasurableSet s
-- Mathlib.CategoryTheory.Abelian.CommSq
CategoryTheory.IsPushout.exact_shortComplex : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X₁ X₂ X₃ X₄ : C}
  {t : X₁ ⟶ X₂} {l : X₁ ⟶ X₃} {r : X₂ ⟶ X₄} {b : X₃ ⟶ X₄} (h : CategoryTheory.IsPushout t l r b), ⋯.shortComplex.Exact
-- Mathlib.RingTheory.GradedAlgebra.TensorProduct
GradedAlgebra.baseChange : {ι : Type u_1} →
  {R : Type u_2} →
    {A : Type u_3} →
      {S : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : CommSemiring S] →
            [inst_2 : Algebra R S] →
              [inst_3 : DecidableEq ι] →
                [inst_4 : AddMonoid ι] →
                  [inst_5 : Semiring A] →
                    [inst_6 : Algebra R A] →
                      (𝒜 : ι → Submodule R A) → [GradedAlgebra 𝒜] → GradedAlgebra fun i => Submodule.baseChange S (𝒜 i)
-- Mathlib.Topology.MetricSpace.Basic
Prod.metricSpaceMax : {β : Type v} → {γ : Type w} → [MetricSpace γ] → [MetricSpace β] → MetricSpace (γ × β)
-- Mathlib.Algebra.Algebra.Equiv
AlgEquivClass.toAlgHomClass : ∀ (F : Type u_1) (R : Type u_2) (A : Type u_3) (B : Type u_4) [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : EquivLike F A B]
  [h : AlgEquivClass F R A B], AlgHomClass F R A B
-- Mathlib.Analysis.Calculus.FDeriv.Add
fderivWithin_fun_neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} {s : Set E}, UniqueDiffWithinAt 𝕜 s x → fderivWithin 𝕜 (fun y => -f y) s x = -fderivWithin 𝕜 f s x
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.isInvalidContinuationByte_getElem_utf8EncodeChar_one_of_utf8Size_eq_three : ∀ {c : Char} (hc : c.utf8Size = 3),
  ByteArray.utf8DecodeChar?.isInvalidContinuationByte (String.utf8EncodeChar c)[1] = false
-- Init.Data.Order.Classes
Std.LawfulOrderLT.lt_iff : ∀ {α : Type u} {inst : LT α} {inst_1 : LE α} [self : Std.LawfulOrderLT α] (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
-- Mathlib.Data.Bool.Basic
Bool.not_eq_iff : ∀ {a b : Bool}, (!a) = b ↔ a ≠ b
-- Mathlib.Data.Seq.Computation
_private.Mathlib.Data.Seq.Computation.0.Computation.run.match_1.splitter : {α : Type u_1} →
  (motive : α ⊕ Computation α → Sort u_2) →
    (x : α ⊕ Computation α) → ((a : α) → motive (Sum.inl a)) → ((ca : Computation α) → motive (Sum.inr ca)) → motive x
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_rcc_eq_singleton_append_iff : ∀ {xs : Array ℤ} {m n a : ℤ}, (m...=n).toArray = #[a] ++ xs ↔ m = a ∧ m ≤ n ∧ ((m + 1)...=n).toArray = xs
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.instNonemptyFixedTermElabRef : Nonempty Lean.Elab.Term.FixedTermElabRef
-- Mathlib.Order.Filter.Basic
Filter.iInf_sets_eq : ∀ {α : Type u} {ι : Sort x} {f : ι → Filter α},
  Directed (fun x1 x2 => x1 ≥ x2) f → ∀ [ne : Nonempty ι], (iInf f).sets = ⋃ i, (f i).sets
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.Subobject.eq_of_isDetecting : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasPullbacks C]
  {𝒢 : CategoryTheory.ObjectProperty C},
  𝒢.IsDetecting →
    ∀ {X : C} (P Q : CategoryTheory.Subobject X), (∀ (G : C), 𝒢 G → ∀ {f : G ⟶ X}, P.Factors f ↔ Q.Factors f) → P = Q
-- Mathlib.Analysis.Calculus.FDeriv.Basic
DifferentiableOn.mono : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {s t : Set E}, DifferentiableOn 𝕜 f t → s ⊆ t → DifferentiableOn 𝕜 f s
-- Init.Data.Option.Lemmas
Option.get_pbind : ∀ {α : Type u_1} {β : Type u_2} {o : Option α} {f : (a : α) → o = some a → Option β} {h : (o.pbind f).isSome = true},
  (o.pbind f).get h = (f (o.get ⋯) ⋯).get ⋯
-- Mathlib.CategoryTheory.FiberedCategory.HasFibers
HasFibers.Fib.hom_ext_iff : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  {p : CategoryTheory.Functor 𝒳 𝒮} [inst_2 : HasFibers p] {S : 𝒮} {a b : HasFibers.Fib p S} {f g : a ⟶ b},
  f = g ↔ (HasFibers.ι S).map f = (HasFibers.ι S).map g
-- Std.Net.Addr
/-- Representation of an IPv4 address.
 -/
Std.Net.IPv4Addr : Type
-- Std.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.Equiv.fold_eq : ∀ {α₁ α₂ β γ : Type w} {m : Type w → Type w'} [Std.Iterator α₁ Id β] [Std.Iterator α₂ Id β]
  [inst : Std.Iterator α₁ Id β] [inst_1 : Std.Iterator α₂ Id β] [Std.Iterators.Finite α₁ Id]
  [Std.Iterators.Finite α₂ Id] [inst_4 : Monad m] [LawfulMonad m] [inst_6 : Std.IteratorLoop α₁ Id Id]
  [Std.LawfulIteratorLoop α₁ Id Id] [inst_8 : Std.IteratorLoop α₂ Id Id] [Std.LawfulIteratorLoop α₂ Id Id] {init : γ}
  {f : γ → β → γ} {ita : Std.Iter β} {itb : Std.Iter β},
  ita.Equiv itb → Std.Iter.fold f init ita = Std.Iter.fold f init itb
-- Init.Data.UInt.Lemmas
USize.toUSize_toUInt8 : ∀ (n : USize), n.toUInt8.toUSize = n % 256
-- Lean.PrettyPrinter.Delaborator.SubExpr
/-- Runs `xf` in the context of `Lean.Expr.getBoundedAppFn maxArgs`.
This is equivalent to `withBoundedAppFnArgs maxArgs xf pure`.
 -/
Lean.PrettyPrinter.Delaborator.SubExpr.withBoundedAppFn : {α : Type} →
  {m : Type → Type} → [Monad m] → [MonadReaderOf Lean.SubExpr m] → [MonadWithReaderOf Lean.SubExpr m] → ℕ → m α → m α
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey!_diff_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {k : α}, k ∉ m₂ → (m₁ \ m₂).getKey! k = m₁.getKey! k
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PrepathObject.toFullSubcategory_p₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X : P.FullSubcategory}
  (Q : HomotopicalAlgebra.PrepathObject X.obj) (hQ : P Q.P),
  (Q.toFullSubcategory hQ).p₁ = CategoryTheory.ObjectProperty.homMk Q.p₁
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.max?_bind_get? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp],
  t.max?.bind t.get? = t.max?
-- Init.Data.List.Basic
List.head?_nil : ∀ {α : Type u}, [].head? = none
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.biSup_comap_eq_top_of_surjective : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [RingHomSurjective τ₁₂] {ι : Type u_8} (s : Set ι),
  s.Nonempty →
    ∀ (p : ι → Submodule R₂ M₂),
      ⨆ i ∈ s, p i = ⊤ → ∀ (f : M →ₛₗ[τ₁₂] M₂), Function.Surjective ⇑f → ⨆ i ∈ s, Submodule.comap f (p i) = ⊤
-- Init.Data.Order.Classes
Std.IsLinearPreorder.toIsPreorder : ∀ {α : Type u} {inst : LE α} [self : Std.IsLinearPreorder α], Std.IsPreorder α
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
_private.Mathlib.Analysis.Distribution.SchwartzSpace.Basic.0.SchwartzMap.le_seminormAux : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] (k n : ℕ) (f : SchwartzMap E F) (x : E),
  ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ SchwartzMap.seminormAux✝ k n f
-- Aesop.Tree.ExtractProof
_private.Aesop.Tree.ExtractProof.0.Aesop.termThrowPRError_ : Lean.ParserDescr
-- Mathlib.Analysis.Asymptotics.Theta
/-- **Alias** of the reverse direction of `Asymptotics.isTheta_const_smul_left`. -/
Asymptotics.IsTheta.const_smul_left : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} {𝕜 : Type u_14} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E']
  [inst_2 : NormedField 𝕜] {g : α → F} {f' : α → E'} {l : Filter α} [inst_3 : NormedSpace 𝕜 E'] {c : 𝕜},
  c ≠ 0 → f' =Θ[l] g → (fun x => c • f' x) =Θ[l] g
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
/-- The left fraction in the opposite category corresponding to a right fraction.  -/
CategoryTheory.MorphismProperty.RightFraction.op : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} →
      {X Y : C} → W.RightFraction X Y → W.op.LeftFraction (Opposite.op Y) (Opposite.op X)
-- Mathlib.Data.Finsupp.Single
Finsupp.support_subset_singleton : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {f : α →₀ M} {a : α}, f.support ⊆ {a} ↔ f = fun₀ | a => f a
-- Mathlib.Data.Tree.Basic
BinaryTree.numLeaves_eq_numNodes_succ : ∀ {α : Type u} (x : BinaryTree α), x.numLeaves = x.numNodes + 1