mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Async.Basic
/-- Raises an error of type `ε` within the `EAsync` monad.
 -/
Std.Async.EAsync.throw : {ε α : Type} → ε → Std.Async.EAsync ε α
-- Mathlib.Algebra.Algebra.Hom
/-- Reinterpret an `AlgHom` as a `RingHom`  -/
AlgHom.toRingHom : {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] → (A →ₐ[R] B) → A →+* B
-- Mathlib.Computability.Primrec.List
Nat.Primrec'.prim_iff : ∀ {n : ℕ} {f : List.Vector ℕ n → ℕ}, Nat.Primrec' f ↔ Primrec f
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.isLeast_opNNNorm : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : Fintype ι]
  (f : ContinuousMultilinearMap 𝕜 E G), IsLeast {C | ∀ (m : (i : ι) → E i), ‖f m‖₊ ≤ C * ∏ i, ‖m i‖₊} ‖f‖₊
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.withBotDegree_mul_of_left_mem_nonZeroDivisors : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f g : MvPolynomial σ R},
  m.leadingCoeff f ∈ nonZeroDivisors R → m.withBotDegree (f * g) = m.withBotDegree f + m.withBotDegree g
-- Mathlib.RingTheory.Polynomial.Dickson
Polynomial.dickson.eq_def : ∀ {R : Type u_1} [inst : CommRing R] (k : ℕ) (a : R) (x : ℕ),
  Polynomial.dickson k a x =
    match x with
    | 0 => 3 - ↑k
    | 1 => Polynomial.X
    | n.succ.succ => Polynomial.X * Polynomial.dickson k a (n + 1) - Polynomial.C a * Polynomial.dickson k a n
-- Mathlib.Algebra.Category.Grp.Preadditive
AddCommGrpCat.instAddCommGroupHom : (P Q : AddCommGrpCat) → AddCommGroup (P ⟶ Q)
-- Mathlib.LinearAlgebra.Eigenspace.Semisimple
/-- A finitely-semisimple endomorphism is triangularizable if and only if it is diagonalizable.  -/
Module.End.IsFinitelySemisimple.iSup_maxGenEigenspace_eq_top_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {f : Module.End R M}, f.IsFinitelySemisimple → (⨆ μ, f.maxGenEigenspace μ = ⊤ ↔ ⨆ μ, f.eigenspace μ = ⊤)
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsDedekindDomain.quotientEquivPiFactors_mk : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {I : Ideal R} (hI : I ≠ ⊥) (x : R),
  (IsDedekindDomain.quotientEquivPiFactors hI) ((Ideal.Quotient.mk I) x) = fun _P =>
    (Ideal.Quotient.mk (↑_P ^ Multiset.count (↑_P) (UniqueFactorizationMonoid.factors I))) x
-- Lean.Meta.PPGoal
Lean.Meta.pp.showLetValues.tactic.threshold : Lean.Option ℕ
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.dvd_iff_roots_le_roots : ∀ {R : Type u_1} [inst : Field R] {f g : Polynomial R}, f.Splits → f ≠ 0 → g ≠ 0 → (f ∣ g ↔ f.roots ≤ g.roots)
-- Mathlib.Algebra.QuaternionBasis
QuaternionAlgebra.Basis.liftHom_apply : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {c₁ c₂ c₃ : R}
  (q : QuaternionAlgebra.Basis A c₁ c₂ c₃) (a : QuaternionAlgebra R c₁ c₂ c₃), q.liftHom a = q.lift a
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.map_one : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  {P' : Type u_3} [inst_3 : CommRing P'] [inst_4 : Algebra R P'] (g : P →ₐ[R] P'), FractionalIdeal.map g 1 = 1
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
/-- The `totalDegree` of a polynomial `p` is a special case of the `weightedTotalDegree` of `p`
where all of the weights are `1`.  -/
MvPolynomial.weightedTotalDegree_one : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] (φ : MvPolynomial σ R),
  MvPolynomial.weightedTotalDegree 1 φ = φ.totalDegree
-- Mathlib.Algebra.Ring.Divisibility.Basic
min_pow_dvd_add : ∀ {α : Type u_1} [inst : Semiring α] {a b c : α} {m n : ℕ}, c ^ m ∣ a → c ^ n ∣ b → c ^ min m n ∣ a + b
-- Mathlib.Algebra.Homology.Double
HomologicalComplex.from_double_hom_ext : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X₀ X₁ : C} {f : X₀ ⟶ X₁} {ι : Type u_2} {c : ComplexShape ι}
  {i₀ i₁ : ι} {hi₀₁ : c.Rel i₀ i₁} {K : HomologicalComplex C c} {φ φ' : HomologicalComplex.double f hi₀₁ ⟶ K},
  φ.f i₀ = φ'.f i₀ → φ.f i₁ = φ'.f i₁ → φ = φ'
-- Mathlib.Algebra.Lie.Free
FreeLieAlgebra.instAddCommGroup : (R : Type u) → (X : Type v) → [inst : CommRing R] → AddCommGroup (FreeLieAlgebra R X)
-- Mathlib.ModelTheory.Encoding
FirstOrder.Language.Term.encoding_encode : ∀ {L : FirstOrder.Language} {α : Type u'} (a : L.Term α), FirstOrder.Language.Term.encoding.encode a = a.listEncode
-- Mathlib.Computability.EpsilonNFA
εNFA.mem_εClosure_iff_exists : ∀ {α : Type u} {σ : Type v} (M : εNFA α σ) {S : Set σ} {s : σ}, s ∈ M.εClosure S ↔ ∃ t ∈ S, s ∈ M.εClosure {t}
-- Init.Core
PSum.inl.sizeOf_spec : ∀ {α : Sort u} {β : Sort v} [inst : SizeOf α] [inst_1 : SizeOf β] (val : α), sizeOf (PSum.inl val) = 1 + sizeOf val
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.Localization.map_eq_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C}
  [inst_1 : W.HasLeftCalculusOfFractions] {X Y : C} (f g : W.LeftFraction X Y),
  f.map (CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W) ⋯ =
      g.map (CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W) ⋯ ↔
    CategoryTheory.MorphismProperty.LeftFractionRel f g
-- Mathlib.Combinatorics.SimpleGraph.Walk.Counting
SimpleGraph.finsetWalkLength.eq_1 : ∀ {V : Type u} (G : SimpleGraph V) [inst : DecidableEq V] [inst_1 : G.LocallyFinite] (u v : V),
  G.finsetWalkLength 0 u v = if h : u = v then ⋯ ▸ {SimpleGraph.Walk.nil} else ∅
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
/-- For an adjunction `F ⊣ G` with counit `ε`, the pair `(FGε_B, ε_FGB)` is reflexive.  -/
CategoryTheory.instIsReflexivePairMapAppCounitObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (B : D),
  CategoryTheory.IsReflexivePair (F.map (G.map (adj.counit.app B))) (adj.counit.app (F.obj (G.obj B)))
-- Mathlib.Geometry.Manifold.StructureGroupoid
StructureGroupoid.mk.sizeOf_spec : ∀ {H : Type u_2} [inst : TopologicalSpace H] [inst_1 : SizeOf H] (members : Set (OpenPartialHomeomorph H H))
  (trans' : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members → e' ∈ members → e.trans e' ∈ members)
  (symm' : ∀ e ∈ members, e.symm ∈ members) (id_mem' : OpenPartialHomeomorph.refl H ∈ members)
  (locality' :
    ∀ (e : OpenPartialHomeomorph H H), (∀ x ∈ e.source, ∃ s, IsOpen s ∧ x ∈ s ∧ e.restr s ∈ members) → e ∈ members)
  (mem_of_eqOnSource' : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members → e' ≈ e → e' ∈ members),
  sizeOf
      { members := members, trans' := trans', symm' := symm', id_mem' := id_mem', locality' := locality',
        mem_of_eqOnSource' := mem_of_eqOnSource' } =
    1 + sizeOf id_mem'
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
/-- The **universal property** of the topology on `𝓓^{n}_{K}(E, F)`: a map to `𝓓^{n}_{K}(E, F)`
is continuous if and only if its composition with each structure map
`structureMapCLM ℝ n i : 𝓓^{n}_{K}(E, F) → (E →ᵇ (E [×i]→L[ℝ] F))` is continuous.

Since `structureMapCLM ℝ n i` is zero whenever `i > n`, it suffices to check it for `i ≤ n`,
as proven by `continuous_iff_comp_order_le`.  -/
ContDiffMapSupportedIn.continuous_iff_comp : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} {X : Type u_5} [inst_4 : TopologicalSpace X]
  (φ : X → ContDiffMapSupportedIn E F n K),
  Continuous φ ↔ ∀ (i : ℕ), Continuous (⇑(ContDiffMapSupportedIn.structureMapCLM ℝ n i) ∘ φ)
-- Mathlib.MeasureTheory.Function.Egorov
MeasureTheory.Egorov.exists_notConvergentSeq_lt : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} [inst : PseudoEMetricSpace β]
  {μ : MeasureTheory.Measure α} {s : Set α} {ε : ℝ} {f : ι → α → β} {g : α → β} [inst_1 : SemilatticeSup ι] [Nonempty ι]
  [Countable ι],
  0 < ε →
    (∀ (n : ι), Measurable fun a => edist (f n a) (g a)) →
      MeasurableSet s →
        μ s ≠ ⊤ →
          (∀ᵐ (x : α) ∂μ, x ∈ s → Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) →
            ∀ (n : ℕ), ∃ j, μ (s ∩ MeasureTheory.Egorov.notConvergentSeq f g n j) ≤ ENNReal.ofReal (ε * 2⁻¹ ^ n)
-- Init.Data.Float.Model.Float
/-- Compute the product of two `Float.Model`.
 -/
Float.Model.mul : Float.Model → Float.Model → Float.Model
-- Mathlib.LinearAlgebra.Matrix.Nondegenerate
Matrix.SeparatingRight.congr_simp : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : NonUnitalNonAssocSemiring R] [inst_1 : Finite m]
  [inst_2 : Finite n] (M M_1 : Matrix m n R), M = M_1 → M.SeparatingRight = M_1.SeparatingRight
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- **Alias** of `FunLike.coeAddMonoidHom_apply`. -/
MultilinearMap.coeAddMonoidHom_apply : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : AddZero F] [inst_2 : AddZeroClass β]
  [inst_3 : IsZeroApply F α β] [inst_4 : IsAddApply F α β] (f : F), (FunLike.coeAddMonoidHom F α β) f = ⇑f
-- Mathlib.Analysis.Calculus.Deriv.Comp
/-- The chain rule.

Note that the function `h₂` is a function on an algebra. If you are looking for the chain rule
with `h₂` taking values in a vector space, use `HasDerivAt.scomp`.  -/
HasDerivAt.comp : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (x : 𝕜) {𝕜' : Type u_1} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {h : 𝕜 → 𝕜'} {h₂ : 𝕜' → 𝕜'} {h' h₂' : 𝕜'},
  HasDerivAt h₂ h₂' (h x) → HasDerivAt h h' x → HasDerivAt (h₂ ∘ h) (h₂' * h') x
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
_private.Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup.0.Matrix.SpecialLinearGroup.diag_decompose : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (i₀ : ι) (D : ι → F),
  (Matrix.diagonal D).det = 1 → (∏ i with i ≠ i₀, fun k => if k = i then D i else if k = i₀ then (D i)⁻¹ else 1) = D
-- Mathlib.Data.PNat.Defs
NeZero.pnat : ∀ {a : ℕ+}, NeZero ↑a
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.replicateCol_add : ∀ {m : Type u_2} {α : Type v} {ι : Type u_6} [inst : Add α] (v w : m → α),
  Matrix.replicateCol ι (v + w) = Matrix.replicateCol ι v + Matrix.replicateCol ι w
-- Mathlib.Algebra.Homology.DerivedCategory.Plus
DerivedCategory.Plus.isGE_ι_obj_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (X : DerivedCategory.Plus C) (n : ℤ), (DerivedCategory.Plus.ι.obj X).IsGE n ↔ X.IsGE n
-- Mathlib.Algebra.Free
FreeAddSemigroup.lift_comp_of' : ∀ {α : Type u} {β : Type v} [inst : AddSemigroup β] (f : FreeAddSemigroup α →ₙ+ β),
  FreeAddSemigroup.lift (⇑f ∘ FreeAddSemigroup.of) = f
-- Mathlib.Control.Functor.Multivariate
MvFunctor.of_mem_supp : ∀ {n : ℕ} {F : TypeVec.{u} n → Type v} [inst : MvFunctor F] {α : TypeVec.{u} n} {x : F α}
  {P : ⦃i : Fin2 n⦄ → α i → Prop}, MvFunctor.LiftP P x → ∀ (i : Fin2 n), ∀ y ∈ MvFunctor.supp x i, P y
-- Mathlib.Analysis.InnerProductSpace.Spectrum
/-- Unsorted eigenvalues and eigenvectors.  These private definitions should not be used directly.
Instead use the functions eigenvalues and eigenvectorBasis defined below.  -/
_private.Mathlib.Analysis.InnerProductSpace.Spectrum.0.LinearMap.IsSymmetric.unsortedEigenvalues : {𝕜 : Type u_1} →
  [inst : RCLike 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : InnerProductSpace 𝕜 E] →
          {T : E →ₗ[𝕜] E} → [FiniteDimensional 𝕜 E] → {n : ℕ} → T.IsSymmetric → Module.finrank 𝕜 E = n → Fin n → ℝ
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.contains_max : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {he : t.isEmpty = false},
  t.contains (t.max he) = true
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
IsTranscendenceBasis.mvPolynomial : ∀ (ι : Type u) (R : Type u_1) [inst : CommRing R] [Nontrivial R], IsTranscendenceBasis R MvPolynomial.X
-- Mathlib.Topology.QuasiSeparated
Topology.IsOpenEmbedding.quasiSeparatedSpace : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β}
  [QuasiSeparatedSpace β], Topology.IsOpenEmbedding f → QuasiSeparatedSpace α
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.ofMonoidHom.injEq : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} [inst : Monoid G] [inst_1 : Ring R] [inst_2 : AddCommGroup V]
  [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  (toMonoidHom toMonoidHom_1 : G →* V →L[R] V),
  ({ toMonoidHom := toMonoidHom } = { toMonoidHom := toMonoidHom_1 }) = (toMonoidHom = toMonoidHom_1)
-- Mathlib.Topology.Algebra.UniformMulAction
AddOpposite.uniformContinuousConstVAdd : ∀ {M : Type v} {X : Type x} [inst : UniformSpace X] [inst_1 : VAdd M X] [UniformContinuousConstVAdd M X],
  UniformContinuousConstVAdd M Xᵃᵒᵖ
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.prod_symm : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : PartialEquiv α β) (e' : PartialEquiv γ δ),
  (e.prod e').symm = e.symm.prod e'.symm
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
SSet.δ_comp_σ_self_apply : ∀ {S : SSet} {n : ℕ} (i : Fin (n + 1)) (x : S.obj (Opposite.op { len := n })),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ S i.castSucc))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ S i)) x) =
    x
-- Mathlib.MeasureTheory.Covering.VitaliFamily
VitaliFamily.FineSubfamilyOn.exists_disjoint_covering_ae : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m0 : MeasurableSpace X} {μ : MeasureTheory.Measure X}
  {v : VitaliFamily μ} {f : X → Set (Set X)} {s : Set X},
  v.FineSubfamilyOn f s →
    ∃ t,
      (∀ p ∈ t, p.1 ∈ s) ∧
        (t.PairwiseDisjoint fun p => p.2) ∧ (∀ p ∈ t, p.2 ∈ v.setsAt p.1 ∩ f p.1) ∧ μ (s \ ⋃ p ∈ t, p.2) = 0
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKeyD_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β}
  {fallback : α}, (t.insert k v).maxKeyD fallback = t.maxKey?.elim k fun k' => if (cmp k' k).isLE = true then k else k'
-- Mathlib.Order.Comparable
CompRel.of_le : ∀ {α : Type u_1} {a b : α} [inst : LE α], a ≤ b → CompRel (fun x1 x2 => x1 ≤ x2) a b
-- Mathlib.Order.RelSeries
RelSeries.head_drop : ∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (i : Fin (p.length + 1)), (p.drop i).head = p.toFun i
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.of : {C : Type u} → C → CategoryTheory.FreeMonoidalCategory C
-- Init.Data.List.Sublist
List.IsPrefix.length_le : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <+: l₂ → l₁.length ≤ l₂.length
-- Mathlib.Topology.SeparatedMap
isSeparatedMap_iff_isClosedMap : ∀ {X : Type u_1} {Y : Sort u_2} [inst : TopologicalSpace X] {f : X → Y},
  IsSeparatedMap f ↔ IsClosedMap (toPullbackDiag f)
-- Mathlib.Algebra.Group.Submonoid.BigOperators
AddSubmonoidClass.coe_list_sum : ∀ {M : Type u_1} {B : Type u_3} [inst : AddMonoid M] [inst_1 : SetLike B M] [inst_2 : AddSubmonoidClass B M] {S : B}
  (l : List ↥S), ↑l.sum = (List.map Subtype.val l).sum
-- Mathlib.Algebra.Order.Group.Abs
mabs_pow : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] (n : ℕ) (a : G), |a ^ n|ₘ = |a|ₘ ^ n
-- Mathlib.CategoryTheory.Shift.Adjunction
CategoryTheory.Equivalence.CommShift.instCommShiftHomFunctorUnitIso : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (E : C ≌ D) (A : Type u_3) [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A] [inst_5 : E.functor.CommShift A]
  [inst_6 : E.inverse.CommShift A] [E.CommShift A], CategoryTheory.NatTrans.CommShift E.unitIso.hom A
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.getEntryLT?_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ → ∀ {k : α}, Std.DTreeMap.Internal.Impl.getEntryLT? k t₁ = Std.DTreeMap.Internal.Impl.getEntryLT? k t₂
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommGroupWithTop.add_neg_cancel_iff_ne_top : ∀ {α : Type u_2} [inst : LinearOrderedAddCommGroupWithTop α] {a : α}, a + -a = 0 ↔ a ≠ ⊤
-- Mathlib.Data.Nat.Multiplicity
Nat.Prime.emultiplicity_one : ∀ {p : ℕ}, Nat.Prime p → emultiplicity p 1 = 0
-- Mathlib.Algebra.Polynomial.SumIteratedDerivative
Polynomial.aeval_sumIDeriv_of_pos : ∀ {R : Type u_1} [inst : CommSemiring R] (A : Type u_3) [inst_1 : CommRing A] [inst_2 : Algebra R A] [Nontrivial A]
  [NoZeroDivisors A] (p : Polynomial R) {q : ℕ},
  0 < q →
    Function.Injective ⇑(algebraMap R A) →
      ∃ gp,
        gp.natDegree ≤ p.natDegree - q ∧
          ∀ (r : A) {p' : Polynomial A},
            Polynomial.map (algebraMap R A) p = (Polynomial.X - Polynomial.C r) ^ (q - 1) * p' →
              (Polynomial.aeval r) (Polynomial.sumIDeriv p) =
                (q - 1).factorial • Polynomial.eval r p' + q.factorial • (Polynomial.aeval r) gp
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.mul_div_eq_iff_isRoot : ∀ {R : Type u} {a : R} [inst : Field R] {p : Polynomial R},
  (Polynomial.X - Polynomial.C a) * (p / (Polynomial.X - Polynomial.C a)) = p ↔ p.IsRoot a
-- Lean.Data.KVMap
Lean.KVMap.Value.mk : {α : Type} → (α → Lean.DataValue) → (Lean.DataValue → Option α) → Lean.KVMap.Value α
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.lipschitz : ∀ {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₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂), LipschitzWith 1 ⇑e
-- Mathlib.Algebra.Homology.SpectralObject.FirstPage
CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.instHasFirstPageComputationEIntProdNatCoreE₂CohomologicalNat : CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalNat.HasFirstPageComputation
-- Mathlib.Analysis.LocallyConvex.Polar
LinearMap.mem_polar_singleton : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedCommRing 𝕜] [inst_1 : AddCommMonoid E]
  [inst_2 : AddCommMonoid F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) {x : E} (y : F),
  y ∈ B.polar {x} ↔ ‖(B x) y‖ ≤ 1
-- Std.Data.HashMap.Lemmas
Std.HashMap.mem_alter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k k' : α} {f : Option β → Option β}, k' ∈ m.alter k f ↔ if (k == k') = true then (f m[k]?).isSome = true else k' ∈ m
-- Lean.Elab.InfoTree.Types
/-- The elaborator creates holes (aka metavariables) for tactics and postponed terms  -/
Lean.Elab.InfoTree.hole : Lean.MVarId → Lean.Elab.InfoTree
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- Given an injective graph homomorphism, map paths to paths.  -/
SimpleGraph.Path.map : {V : Type u} →
  {V' : Type v} →
    {G : SimpleGraph V} →
      {G' : SimpleGraph V'} → (f : G →g G') → Function.Injective ⇑f → {u v : V} → G.Path u v → G'.Path (f u) (f v)
-- Mathlib.Analysis.Calculus.Deriv.Mul
DifferentiableWithinAt.div_const : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {𝕜' : Type u_2} [inst_1 : NormedDivisionRing 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {c : 𝕜 → 𝕜'},
  DifferentiableWithinAt 𝕜 c s x → ∀ (d : 𝕜'), DifferentiableWithinAt 𝕜 (fun x => c x / d) s x
-- Mathlib.CategoryTheory.Shift.Basic
/-- Shifting by `i` and shifting by `j` forms an equivalence when `i + j = 0`.  -/
CategoryTheory.shiftEquiv' : (C : Type u) →
  {A : Type u_1} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : AddGroup A] → [CategoryTheory.HasShift C A] → (i j : A) → i + j = 0 → (C ≌ C)
-- Mathlib.Algebra.Colimit.Finiteness
Module.fgSystem.instDirectedSystemSubtypeSubmoduleFGMemValCoeLinearMapId : ∀ (R : Type u_1) (M : Type u_2) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  DirectedSystem (fun x2 => ↥↑x2) fun x1 x2 x3 x4 => (Module.fgSystem R M x1 x2 x3) x4
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get!_erase_self : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → ∀ {k : α}, (t.erase k).get! k = default
-- Mathlib.LinearAlgebra.Matrix.Bilinear
/-- A version of `LinearMap.mulLeft_zero_eq_zero` for matrix multiplication.  -/
mulRightLinearMap_zero_eq_zero : ∀ (l : Type u_1) {m : Type u_2} {n : Type u_3} (R : Type u_5) {A : Type u_6} [inst : Fintype m] [inst_1 : Semiring R]
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : Module R A] [inst_4 : IsScalarTower R A A],
  mulRightLinearMap l R 0 = 0
-- Mathlib.Order.Hom.Basic
OrderIso.dualDual_symm_apply : ∀ {α : Type u_2} [inst : LE α] (a : αᵒᵈᵒᵈ), (OrderIso.dualDual α).symm a = OrderDual.ofDual (OrderDual.ofDual a)
-- Mathlib.Topology.Order.LeftRightNhds
/-- If `a` is positive, then the intervals `(a - ε, a + ε)`, `0 < ε ≤ a`,
form a basis of neighborhoods of `a`.

This upper bound for `ε` guarantees that all elements of these intervals are positive.  -/
nhds_basis_Ioo_pos_of_pos : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : AddCommGroup α] [inst_2 : LinearOrder α] [IsOrderedAddMonoid α]
  [OrderTopology α] [NoMaxOrder α] {a : α},
  0 < a → (nhds a).HasBasis (fun ε => 0 < ε ∧ ε ≤ a) fun ε => Set.Ioo (a - ε) (a + ε)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.mem_alter_of_not_compare_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF → ∀ {k k' : α} {f : Option (β k) → Option (β k)}, ¬cmp k k' = Ordering.eq → (k' ∈ t.alter k f ↔ k' ∈ t)
-- Mathlib.Order.CompleteLattice.Finset
Finset.iInf_finset_image : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : CompleteLattice β] [inst_1 : DecidableEq α] {f : γ → α}
  {g : α → β} {s : Finset γ}, ⨅ x ∈ Finset.image f s, g x = ⨅ y ∈ s, g (f y)
-- Mathlib.Algebra.BigOperators.Finprod
/-- **Alias** of `map_finsetSum`. -/
map_finset_sum : ∀ {M : Type u_5} {N : Type u_6} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] {α : Type u_7} {F : Type u_8}
  [inst_2 : Fintype α] [inst_3 : EquivLike F M N] [AddEquivClass F M N] (f : F) (g : α → M), f (∑ i, g i) = ∑ i, f (g i)
-- Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Module.isLocallyConstant_rankAtStalk : ∀ {R : Type uR} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [Module.FinitePresentation R M] [Module.Flat R M], IsLocallyConstant (Module.rankAtStalk M)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Map
/-- If `g : α → β` is a measurable embedding and `f : β → ℝ≥0∞` is any function (not necessarily
measurable), then `∫⁻ a, f a ∂(map g μ) = ∫⁻ a, f (g a) ∂μ`. Compare with `lintegral_map` which
applies to any measurable `g : α → β` but requires that `f` is measurable as well.  -/
MeasurableEmbedding.lintegral_map : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {g : α → β},
  MeasurableEmbedding g → ∀ (f : β → ENNReal), ∫⁻ (a : β), f a ∂MeasureTheory.Measure.map g μ = ∫⁻ (a : α), f (g a) ∂μ
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- If a family is affinely independent, so is any subfamily given by
composition of an embedding into index type with the original
family.  -/
AffineIndependent.comp_embedding : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} {ι2 : Type u_5} (f : ι2 ↪ ι) {p : ι → P},
  AffineIndependent k p → AffineIndependent k (p ∘ ⇑f)