mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
Matrix.toBilin.eq_1 : ∀ {R₁ : Type u_1} {M₁ : Type u_2} [inst : CommSemiring R₁] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R₁ M₁]
  {n : Type u_5} [inst_3 : Fintype n] [inst_4 : DecidableEq n] (b : Module.Basis n R₁ M₁),
  Matrix.toBilin b = (LinearMap.BilinForm.toMatrix b).symm
-- Std.Data.String.ToInt
String.toInt?_minus_append : ∀ {s : String}, ("-" ++ s).toInt? = Option.map (fun n => -↑n) s.toNat?
-- Mathlib.Probability.Kernel.Composition.Comp
ProbabilityTheory.Kernel.IsSFiniteKernel.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (η : ProbabilityTheory.Kernel β γ) [ProbabilityTheory.IsSFiniteKernel η]
  (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ], ProbabilityTheory.IsSFiniteKernel (η.comp κ)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Real.sin_sq_lt_sq : ∀ {x : ℝ}, x ≠ 0 → Real.sin x ^ 2 < x ^ 2
-- Mathlib.GroupTheory.Complement
AddSubgroup.isComplement_iff_existsUnique_add_neg_mem : ∀ {G : Type u_1} [inst : AddGroup G] {S T : Set G}, AddSubgroup.IsComplement S T ↔ ∀ (g : G), ∃! t, g + -↑t ∈ S
-- Mathlib.Algebra.Polynomial.Splits
/-- See `splits_iff_exists_multiset` for the version with subtraction.  -/
Polynomial.splits_iff_exists_multiset' : ∀ {R : Type u_1} [inst : CommSemiring R] {f : Polynomial R},
  f.Splits ↔ ∃ m, f = Polynomial.C f.leadingCoeff * (Multiset.map (fun x => Polynomial.X + Polynomial.C x) m).prod
-- Init.Data.Nat.Bitwise.Lemmas
Nat.testBit_mul_two_pow_add_eq : ∀ (a b i : ℕ), (2 ^ i * a + b).testBit i = (decide (a % 2 = 1) ^^ b.testBit i)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.center_le_centralizer : ∀ {R : Type u_1} [inst : Semiring R] (s : Set R), Subsemiring.center R ≤ Subsemiring.centralizer s
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsDedekindDomain.primesOver_ncard_ne_zero : ∀ {A : Type u_4} [inst : CommRing A] (p : Ideal A) [hpm : p.IsMaximal] (B : Type u_5) [inst_1 : CommRing B]
  [IsDedekindDomain B] [inst_3 : Algebra A B] [IsDomain A] [Module.IsTorsionFree A B] [Algebra.IsIntegral A B],
  (p.primesOver B).ncard ≠ 0
-- Mathlib.Algebra.Group.InjSurj
Function.Surjective.subNegMonoid.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₂] [inst_1 : Zero M₂] [inst_2 : SMul ℕ M₂] [inst_3 : Neg M₂]
  [inst_4 : Sub M₂] [inst_5 : SMul ℤ M₂] [inst_6 : SubNegMonoid M₁] (f : M₁ → M₂) (hf : Function.Surjective f)
  (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (inv : ∀ (x : M₁), f (-x) = -f x)
  (div : ∀ (x y : M₁), f (x - y) = f x - f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x)
  (zpow : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x),
  Function.Surjective.subNegMonoid f hf one mul inv div npow zpow =
    { toAddMonoid := Function.Surjective.addMonoid f hf one mul npow, toNeg := inst_3, toSub := inst_4,
      zsmul := fun n x => n • x, sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯ }
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.not_mem_of_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {a : α},
  t.isEmpty = true → a ∉ t
-- Init.Data.Int.Order
Int.nonneg_def : ∀ {a : ℤ}, a.NonNeg ↔ ∃ n, a = ↑n
-- Mathlib.LinearAlgebra.Dual.Defs
Submodule.dualAnnihilator_dualCoannihilator_dualAnnihilator : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (U : Submodule R M), U.dualAnnihilator.dualCoannihilator.dualAnnihilator = U.dualAnnihilator
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.ih_n.eq_1 : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F : Polynomial R} {a : ℤ_[p]}
  (hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2) {n : ℕ} {z : ℤ_[p]}
  (hz : ih_gen✝ n z),
  ih_n✝ hnorm hz = ⟨z - ⟨↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F)), ⋯⟩, ⋯⟩
-- Lean.Compiler.LCNF.Types
_private.Lean.Compiler.LCNF.Types.0.Lean.Compiler.LCNF.toLCNFType.visitForall.match_9.splitter : (motive : Lean.Expr → Sort u_1) →
  (e : Lean.Expr) →
    ((n : Lean.Name) → (d b : Lean.Expr) → (bi : Lean.BinderInfo) → motive (Lean.Expr.forallE n d b bi)) →
      ((x : Lean.Expr) →
          (∀ (n : Lean.Name) (d b : Lean.Expr) (bi : Lean.BinderInfo), x = Lean.Expr.forallE n d b bi → False) →
            motive x) →
        motive e
-- Init.Data.String.Lemmas.Search
_private.Init.Data.String.Lemmas.Search.0.String.Slice.Pos.find.eq_1 : ∀ {ρ : Type} {σ : String.Slice → Type}
  [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)]
  [inst_1 : (s : String.Slice) → Std.IteratorLoop (σ s) Id Id] {s : String.Slice} (pos : s.Pos) (pattern : ρ)
  [inst_2 : String.Slice.Pattern.ToForwardSearcher pattern σ],
  pos.find pattern = String.Slice.Pos.ofSliceFrom ((s.sliceFrom pos).find pattern)
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Roi.Internal.toArray_eq_toArray_iter : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.Rxi.IsAlwaysFinite α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Roi α}, r.toArray = (Std.Roi.Internal.iter r).toArray
-- Mathlib.Combinatorics.Matroid.Map
Matroid.instRankPosMapEmbedding : ∀ {α : Type u_1} {β : Type u_2} {M : Matroid α} [M.RankPos] {f : α ↪ β}, (M.mapEmbedding f).RankPos
-- Mathlib.Geometry.Manifold.StructureGroupoid
Pregroupoid.mk.sizeOf_spec : ∀ {H : Type u_2} [inst : TopologicalSpace H] [inst_1 : SizeOf H] (property : (H → H) → Set H → Prop)
  (comp :
    ∀ {f g : H → H} {u v : Set H},
      property f u → property g v → IsOpen u → IsOpen v → IsOpen (u ∩ f ⁻¹' v) → property (g ∘ f) (u ∩ f ⁻¹' v))
  (id_mem : property id Set.univ)
  (locality :
    ∀ {f : H → H} {u : Set H}, IsOpen u → (∀ x ∈ u, ∃ v, IsOpen v ∧ x ∈ v ∧ property f (u ∩ v)) → property f u)
  (congr : ∀ {f g : H → H} {u : Set H}, IsOpen u → (∀ x ∈ u, g x = f x) → property f u → property g u),
  sizeOf { property := property, comp := comp, id_mem := id_mem, locality := locality, congr := congr } =
    1 + sizeOf id_mem
-- Lean.Structure
Lean.StructureResolutionState.resolutions : Lean.StructureResolutionState → Lean.PHashMap Lean.Name (Array Lean.Name)
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.linear_prodAssoc : ∀ (k : Type u_1) (P₁ : Type u_2) (P₂ : Type u_3) (P₃ : Type u_4) {V₁ : Type u_6} {V₂ : Type u_7} {V₃ : Type u_8}
  [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : AddCommGroup V₃]
  [inst_4 : Module k V₁] [inst_5 : Module k V₂] [inst_6 : Module k V₃] [inst_7 : AddTorsor V₁ P₁]
  [inst_8 : AddTorsor V₂ P₂] [inst_9 : AddTorsor V₃ P₃],
  (AffineEquiv.prodAssoc k P₁ P₂ P₃).linear = LinearEquiv.prodAssoc k V₁ V₂ V₃
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
/-- Notation for `actionAssocIso`, the structural isomorphism
`- ⊗ - ⊙ₗ - ≅ - ⊙ₗ - ⊙ₗ -`.  -/
CategoryTheory.MonoidalCategory.MonoidalLeftAction.termαₗ : Lean.ParserDescr
-- Mathlib.GroupTheory.GroupAction.Blocks
MulAction.IsTrivialBlock.smul : ∀ {M : Type u_3} {α : Type u_4} [inst : Group M] [inst_1 : MulAction M α] {B : Set α},
  MulAction.IsTrivialBlock B → ∀ (g : M), MulAction.IsTrivialBlock (g • B)
-- Mathlib.Data.Finset.Density
Finset.dens_eq_zero : ∀ {α : Type u_2} [inst : Fintype α] {s : Finset α}, s.dens = 0 ↔ s = ∅
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
MeasureTheory.Measure.addHaar_real_closedBall_center : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E)
  [μ.IsAddHaarMeasure] (x : E) (r : ℝ), μ.real (Metric.closedBall x r) = μ.real (Metric.closedBall 0 r)
-- Mathlib.Topology.Order.LocalExtr
IsMinOn.localize : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β} {s : Set α} {a : α},
  IsMinOn f s a → IsLocalMinOn f s a
-- Mathlib.Data.Nat.PSub
_private.Mathlib.Data.Nat.PSub.0.Nat.ppred.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.Topology.UniformSpace.Separation
SeparationQuotient.uniformity_eq : ∀ {α : Type u} [inst : UniformSpace α],
  uniformity (SeparationQuotient α) = Filter.map (Prod.map SeparationQuotient.mk SeparationQuotient.mk) (uniformity α)
-- Std.Async.Basic
/-- Create an `ETask` that resolves to the value of the promise `x`. If the promise gets dropped then it
panics.
 -/
Std.Async.ETask.ofPromise! : {ε α : Type} → IO.Promise (Except ε α) → Std.Async.ETask ε α
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.insert_eq_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {p : (a : α) × β a}, insert p t = t.insert p.fst p.snd
-- Aesop.Util.Basic
Aesop.PersistentHashSet.toHashSet : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → Lean.PHashSet α → Std.HashSet α
-- Mathlib.Analysis.Calculus.Implicit
HasStrictFDerivAt.implicitFunction_apply_image : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : CompleteSpace 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : CompleteSpace E] {F : Type u_3}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] [inst_7 : FiniteDimensional 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {a : E} (hf : HasStrictFDerivAt f f' a) (hf' : (↑f').range = ⊤),
  HasStrictFDerivAt.implicitFunction f f' hf hf' (f a) 0 = a
-- Mathlib.Data.Set.Subsingleton
Set.nontrivial_of_exists_lt : ∀ {α : Type u} {s : Set α} [inst : Preorder α], (∃ x ∈ s, ∃ y ∈ s, x < y) → s.Nontrivial
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.contains_ofList : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp] {l : List α} {k : α},
  (Std.TreeSet.ofList l cmp).contains k = l.contains k
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.instAlternativeDelabM : Alternative Lean.PrettyPrinter.Delaborator.DelabM
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.zeroLocus_subset_zeroLocus_singleton_iff : ∀ {R : Type u} [inst : CommSemiring R] (f g : R),
  PrimeSpectrum.zeroLocus {f} ⊆ PrimeSpectrum.zeroLocus {g} ↔ g ∈ (Ideal.span {f}).radical
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.constMaxEntry?_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → Std.DTreeMap.Const.maxEntry? t₁ = Std.DTreeMap.Const.maxEntry? t₂
-- Init.Data.BitVec.Lemmas
BitVec.sdivOverflow_eq_negOverflow_of_eq_allOnes : ∀ {w : ℕ} {x y : BitVec w}, y = BitVec.allOnes w → x.sdivOverflow y = x.negOverflow
-- Mathlib.RingTheory.Nakayama
/-- **Alias** of `Submodule.le_of_map_mkQ_le_map_mkQ_of_le_jacobson_bot`. -/
Submodule.le_span_of_map_mkQ_le_map_mkQ_span_of_le_jacobson_bot : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I : Ideal R}
  {N N' : Submodule R M}, N.FG → I ≤ ⊥.jacobson → Submodule.map (I • N).mkQ N ≤ Submodule.map (I • N).mkQ N' → N ≤ N'
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Localization.r.eq_1 : ∀ {M : Type u_1} [inst : CommMonoid M] (S : Submonoid M), Localization.r S = sInf {c | ∀ (y : ↥S), c 1 (↑y, y)}
-- Mathlib.Algebra.Group.End
Equiv.Perm.sumCongr_inv : ∀ {α : Type u_7} {β : Type u_8} (e : Equiv.Perm α) (f : Equiv.Perm β), (e.sumCongr f)⁻¹ = e⁻¹.sumCongr f⁻¹
-- Mathlib.Combinatorics.Matroid.IndepAxioms
/-- An independence predicate satisfying the finite matroid axioms determines a matroid,
provided independence is determined by its behaviour on finite sets.  -/
IndepMatroid.ofFinitaryCardAugment : {α : Type u_1} →
  (E : Set α) →
    (Indep : Set α → Prop) →
      Indep ∅ →
        (∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I) →
          (∀ ⦃I J : Set α⦄,
              Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)) →
            (∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I) → (∀ (I : Set α), Indep I → I ⊆ E) → IndepMatroid α
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
/-- Given
```
X₁ - f₁ -> X₂ - f₂ -> X₃
|          |          |
i₁         i₂         i₃
↓          ↓          ↓
Y₁ - g₁ -> Y₂ - g₂ -> Y₃
```
Then the left square is a pullback if the right square and the big square are.
 -/
CategoryTheory.Limits.leftSquareIsPullback : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₃ Y₁ Y₂ Y₃ : C} →
      {g₁ : Y₁ ⟶ Y₂} →
        {g₂ : Y₂ ⟶ Y₃} →
          {i₃ : X₃ ⟶ Y₃} →
            {t₂ : CategoryTheory.Limits.PullbackCone g₂ i₃} →
              {i₂ : t₂.pt ⟶ Y₂} →
                (t₁ : CategoryTheory.Limits.PullbackCone g₁ i₂) →
                  (hi₂ : i₂ = t₂.fst) →
                    CategoryTheory.Limits.IsLimit t₂ →
                      CategoryTheory.Limits.IsLimit (t₂.pasteHoriz t₁ hi₂) → CategoryTheory.Limits.IsLimit t₁
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
_private.Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion.0.Tactic.ComputeAsymptotics.Seq.FriendlyOperation.exists_fixed_point.match_1.eq_1 : ∀ {α : Type u_3} {β : Type u_1} {γ : Type u_2} (motive : Option (α × γ × β) → Sort u_4) (h_1 : Unit → motive none)
  (h_2 : (a : α) → (c : γ) → (b' : β) → motive (some (a, c, b'))),
  (match none with
    | none => h_1 ()
    | some (a, c, b') => h_2 a c b') =
    h_1 ()
-- Mathlib.Order.Bounded
Set.unbounded_ge_iff_unbounded_inter_ge : ∀ {α : Type u_1} {s : Set α} [inst : LinearOrder α] (a : α),
  Set.Unbounded (fun x1 x2 => x1 ≥ x2) (s ∩ {b | b ≤ a}) ↔ Set.Unbounded (fun x1 x2 => x1 ≥ x2) s
-- Std.Data.HashSet.Lemmas
Std.HashSet.get!_union : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {k : α}, (m₁ ∪ m₂).get! k = m₂.getD k (m₁.get! k)
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_set_one : ∀ {α : Type u_4} (s : Set α), ∑' (x : ↑s), 1 = ↑s.encard
-- Mathlib.Algebra.Group.Equiv.Opposite
AddEquiv.opOp.eq_1 : ∀ (M : Type u_3) [inst : Add M],
  AddEquiv.opOp M = { toEquiv := AddOpposite.opEquiv.trans AddOpposite.opEquiv, map_add' := ⋯ }
-- Mathlib.Data.Vector3
vectorEx_iff_exists : ∀ {α : Type u_1} {n : ℕ} (f : Vector3 α n → Prop), VectorEx n f ↔ Exists f
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
SummationFilter.support_eq_univ : ∀ {β : Type u_2} (L : SummationFilter β) [L.LeAtTop], L.support = Set.univ
-- Init.Data.Char.Basic
/-- Converts an 8-bit unsigned integer into a character.

The integer's value is interpreted as a Unicode code point.
 -/
Char.ofUInt8 : UInt8 → Char
-- Mathlib.Algebra.Category.Ring.LinearAlgebra
CommRingCat.nontrivial_of_isPushout_of_isField : ∀ {A B C D : CommRingCat},
  IsField ↑A →
    ∀ {f : A ⟶ B} {g : A ⟶ C} {inl : B ⟶ D} {inr : C ⟶ D} [Nontrivial ↑B] [Nontrivial ↑C],
      CategoryTheory.IsPushout f g inl inr → Nontrivial ↑D
-- Mathlib.Analysis.Convex.Topology
closedConvexHull_eq_closure_convexHull : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E},
  (closedConvexHull 𝕜) s = closure ((convexHull 𝕜) s)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.minD_eq_iff_get?_eq_self_and_forall : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF →
    t.isEmpty = false →
      ∀ {km fallback : α}, t.minD fallback = km ↔ t.get? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsColimitsOfShape : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J], (P.colimitsOfShape J).IsClosedUnderIsomorphisms
-- Mathlib.Data.List.MinMax
List.argmin_mem : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] [inst_1 : DecidableLT β] {f : α → β} {l : List α} {m : α},
  m ∈ List.argmin f l → m ∈ l
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.foldrM_eq_foldrM_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} {δ : Type w} {m : Type w → Type w'} [inst : Monad m]
  [LawfulMonad m] {f : α → δ → m δ} {init : δ}, Std.TreeSet.foldrM f init t = Array.foldrM f init t.toArray
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
/-- The identity oplax transformation.  -/
CategoryTheory.Oplax.OplaxTrans.id : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        (F : CategoryTheory.OplaxFunctor B C) → CategoryTheory.Oplax.OplaxTrans F F
-- Std.Time.Date.PlainDate
Std.Time.PlainDate.compare_def : compare = compareLex (compareOn fun x => x.year) (compareLex (compareOn fun x => x.month) (compareOn fun x => x.day))
-- Mathlib.Tactic.Linter.FlexibleLinter
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.Stained.wildcard : Mathlib.Linter.Flexible.Stained✝
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
/-- A graph is locally linear if each edge belongs to exactly one triangle.  -/
SimpleGraph.LocallyLinear : {α : Type u_1} → SimpleGraph α → Prop
-- Mathlib.Order.SuccPred.IntervalSucc
/-- If `α` is a linear archimedean succ order and `β` is a linear order, then for any monotone
function `f` and `m n : α`, the union of intervals `Set.Ioc (f i) (f (Order.succ i))`, `m ≤ i < n`,
is equal to `Set.Ioc (f m) (f n)`  -/
Monotone.biUnion_Ico_Ioc_map_succ : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : SuccOrder α] [IsSuccArchimedean α]
  [inst_3 : LinearOrder β] {f : α → β},
  Monotone f → ∀ (m n : α), ⋃ i ∈ Set.Ico m n, Set.Ioc (f i) (f (Order.succ i)) = Set.Ioc (f m) (f n)
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.norm_ofSubsingleton_id_le : ∀ {𝕜 : Type u} {E : Type wE} {ι : Type v} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : Fintype ι] [inst_4 : Subsingleton ι] (i : ι),
  ‖(ContinuousAlternatingMap.ofSubsingleton 𝕜 E E i) (ContinuousLinearMap.id 𝕜 E)‖ ≤ 1
-- Mathlib.Algebra.Group.Torsion
inv_eq_self : ∀ {G : Type u_2} [inst : Group G] [IsMulTorsionFree G] {a : G}, a⁻¹ = a ↔ a = 1
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get?_diff_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → (m₁ \ m₂).get? k = m₁.get? k
-- Mathlib.Topology.Defs.Filter
/-- There are various definitions of "locally compact space" in the literature,
which agree for Hausdorff spaces but not in general.
This one is the precise condition on X needed
for the evaluation map `C(X, Y) × X → Y` to be continuous for all `Y`
when `C(X, Y)` is given the compact-open topology.

See also `WeaklyLocallyCompactSpace`, a typeclass that only assumes
that each point has a compact neighborhood.  -/
LocallyCompactSpace : (X : Type u_3) → [TopologicalSpace X] → Prop
-- Mathlib.Order.Filter.CountablyGenerated
Filter.pi.isCountablyGenerated : ∀ {ι : Type u_6} {α : ι → Type u_7} [Countable ι] (f : (i : ι) → Filter (α i)) [∀ (i : ι), (f i).IsCountablyGenerated],
  (Filter.pi f).IsCountablyGenerated
-- Mathlib.Algebra.Group.Subgroup.Finite
Subgroup.card_le_one_iff_eq_bot : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) [Finite ↥H], Nat.card ↥H ≤ 1 ↔ H = ⊥
-- Mathlib.Data.Nat.Factorial.SuperFactorial
Nat.superFactorial.eq_1 : Nat.superFactorial 0 = 1
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBMap.mem_toList_unique : ∀ {α : Type u_1} {cmp : α → α → Ordering} {β : Type u_2} {x y : α × β} [Std.TransCmp cmp] {t : RBTree.RBMap α β cmp},
  x ∈ t.toList → y ∈ t.toList → cmp x.1 y.1 = Ordering.eq → x = y
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.degree_le : ∀ {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (v : V) [inst : Fintype ↑(G'.neighborSet v)]
  [inst_1 : Fintype ↑(G.neighborSet v)], G'.degree v ≤ G.degree v
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.shortComplexOfDistTriangle_X₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C]
  (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles),
  (CategoryTheory.Pretriangulated.shortComplexOfDistTriangle T hT).X₁ = T.obj₁
-- Mathlib.CategoryTheory.Bicategory.Coherence
_private.Mathlib.CategoryTheory.Bicategory.Coherence.0.CategoryTheory.FreeBicategory.normalizeAux.match_1.splitter : {B : Type u_2} →
  [inst : Quiver B] →
    {a : B} →
      (motive : (x x_1 : B) → Quiver.Path a x → CategoryTheory.FreeBicategory.Hom x x_1 → Sort u_3) →
        (x x_1 : B) →
          (x_2 : Quiver.Path a x) →
            (x_3 : CategoryTheory.FreeBicategory.Hom x x_1) →
              ((x x_4 : B) →
                  (p : Quiver.Path a x) → (f : x ⟶ x_4) → motive x x_4 p (CategoryTheory.FreeBicategory.Hom.of f)) →
                ((x : B) → (p : Quiver.Path a x) → motive x x p (CategoryTheory.FreeBicategory.Hom.id x)) →
                  ((x x_4 : B) →
                      (p : Quiver.Path a x) →
                        (b : B) →
                          (f : CategoryTheory.FreeBicategory.Hom x b) →
                            (g : CategoryTheory.FreeBicategory.Hom b x_4) → motive x x_4 p (f.comp g)) →
                    motive x x_1 x_2 x_3
-- Init.Data.Dyadic.Basic
/-- A dyadic rational is either zero or of the form `n * 2^(-k)` for some (unique) `n k : Int`
where `n` is odd.
 -/
Dyadic : Type
-- Lean.Data.Lsp.Basic
Lean.Lsp.TextDocumentPositionParams.mk.injEq : ∀ (textDocument : Lean.Lsp.TextDocumentIdentifier) (position : Lean.Lsp.Position)
  (textDocument_1 : Lean.Lsp.TextDocumentIdentifier) (position_1 : Lean.Lsp.Position),
  ({ textDocument := textDocument, position := position } =
      { textDocument := textDocument_1, position := position_1 }) =
    (textDocument = textDocument_1 ∧ position = position_1)
-- Init.Data.String.Lemmas.Iter
_private.Init.Data.String.Lemmas.Iter.0.String.join.eq_1 : ∀ (l : List String), String.join l = List.foldl (fun r s => r ++ s) "" l
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getD_inter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t₁.WF →
    t₂.WF →
      ∀ {k : α} {fallback : β k},
        (t₁ ∩ t₂).getD k fallback = if t₂.contains k = true then t₁.getD k fallback else fallback
-- Init.Data.UInt.Lemmas
UInt16.toUSize_toUInt64 : ∀ (n : UInt16), n.toUInt64.toUSize = n.toUSize
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
/-- `u` is a **right quasi-inverse** to `v` if `v ∘ₗ u ≈ id` modulo
linear maps with noetherian ranges. Recall that if the scalar ring is noetherian
(e.g a field), then "noetherian range" can be replaced by "finitely generated range".  -/
LinearMap.IsRightQuasiInverse : {K : Type u_1} →
  {V₂ : Type u_4} →
    {V₃ : Type u_6} →
      [inst : CommRing K] →
        [inst_1 : AddCommGroup V₂] →
          [inst_2 : Module K V₂] →
            [inst_3 : AddCommGroup V₃] → [inst_4 : Module K V₃] → (V₃ →ₗ[K] V₂) → (V₂ →ₗ[K] V₃) → Prop
-- Mathlib.MeasureTheory.Function.LpOrder
MeasureTheory.Lp.instIsOrderedAddMonoid : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : ENNReal}
  [inst : NormedAddCommGroup E] [inst_1 : PartialOrder E] [IsOrderedAddMonoid E],
  IsOrderedAddMonoid ↥(MeasureTheory.Lp E p μ)
-- Lean.Expr
Lean.Expr.forallE.inj : ∀ {binderName : Lean.Name} {binderType body : Lean.Expr} {binderInfo : Lean.BinderInfo} {binderName_1 : Lean.Name}
  {binderType_1 body_1 : Lean.Expr} {binderInfo_1 : Lean.BinderInfo},
  Lean.Expr.forallE binderName binderType body binderInfo =
      Lean.Expr.forallE binderName_1 binderType_1 body_1 binderInfo_1 →
    binderName = binderName_1 ∧ binderType = binderType_1 ∧ body = body_1 ∧ binderInfo = binderInfo_1