mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.of_union : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  {v : MeasureTheory.VectorMeasure α M} [T2Space M] {A B : Set α},
  Disjoint A B → MeasurableSet A → MeasurableSet B → v (A ∪ B) = v A + v B
-- Mathlib.GroupTheory.OrderOfElement
/-- See `AddSubgroup.closure_toAddSubmonoid_of_isOfFinOrder` for a version with weaker
assumptions.  -/
AddSubgroup.closure_toAddSubmonoid_of_finite : ∀ {G : Type u_1} [inst : AddGroup G] [Finite G] {s : Set G},
  (AddSubgroup.closure s).toAddSubmonoid = AddSubmonoid.closure s
-- Init.Data.UInt.Lemmas
UInt16.toUInt8_sub : ∀ (a b : UInt16), (a - b).toUInt8 = a.toUInt8 - b.toUInt8
-- Mathlib.LinearAlgebra.Basis.Basic
Module.Basis.singleton.eq_1 : ∀ (ι : Type u_7) (R : Type u_8) [inst : Unique ι] [inst_1 : Semiring R],
  Module.Basis.singleton ι R =
    {
      repr :=
        { toFun := fun x => fun₀ | default => x, map_add' := ⋯, map_smul' := ⋯, invFun := fun f => f default,
          left_inv := ⋯, right_inv := ⋯ } }
-- Mathlib.GroupTheory.PGroup
IsPGroup.of_card : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] {n : ℕ}, Nat.card G = p ^ n → IsPGroup p G
-- Mathlib.Order.Interval.Basic
NonemptyInterval.toDualProd_apply : ∀ {α : Type u_1} [inst : LE α] (s : NonemptyInterval α), s.toDualProd = (OrderDual.toDual s.toProd.1, s.toProd.2)
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
instTopologicalSpaceWeakDual : (𝕜 : Type u_1) →
  (E : Type u_2) →
    [inst : CommSemiring 𝕜] →
      [inst_1 : TopologicalSpace 𝕜] →
        [inst_2 : ContinuousAdd 𝕜] →
          [inst_3 : ContinuousConstSMul 𝕜 𝕜] →
            [inst_4 : AddCommMonoid E] →
              [inst_5 : Module 𝕜 E] → [inst_6 : TopologicalSpace E] → TopologicalSpace (WeakDual 𝕜 E)
-- Mathlib.CategoryTheory.ObjectProperty.ContainsZero
CategoryTheory.ObjectProperty.instNonemptyOfContainsZero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.ContainsZero],
  P.Nonempty
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.checkWsBefore.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.toAbs_neg : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Ring R] (v : AbsoluteValue R S)
  (x : R), WithAbs.toAbs v (-x) = -WithAbs.toAbs v x
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.mk.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X A : C} (f f_1 : A ⟶ X) (e_f : f = f_1)
  [inst_1 : CategoryTheory.Mono f], CategoryTheory.Subobject.mk f = CategoryTheory.Subobject.mk f_1
-- Mathlib.Topology.EMetricSpace.Pi
edist_le_pi_edist : ∀ {β : Type v} {X : β → Type u_2} [inst : Fintype β] [inst_1 : (b : β) → EDist (X b)] (f g : (b : β) → X b) (b : β),
  edist (f b) (g b) ≤ edist f g
-- Init.Data.SInt.IntToBitVec
ISize.ne_iff_toBitVec32_ne : ∀ {a b : ISize} (h : System.Platform.numBits = 32), a ≠ b ↔ a.toBitVec32 h ≠ b.toBitVec32 h
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.toVal_pow : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀)
  (x : R) (n : ℕ), WithVal.toVal v (x ^ n) = WithVal.toVal v x ^ n
-- Lean.Elab.Do.Basic
Lean.Elab.Do.instNonemptyDoOpsRef : Nonempty Lean.Elab.Do.DoOpsRef
-- Mathlib.Analysis.Normed.Operator.Bilinear
ContinuousLinearMap.opNorm_ext : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_6} {G : Type u_8}
  [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F] [inst_2 : SeminormedAddCommGroup G]
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NontriviallyNormedField 𝕜₂] [inst_5 : NontriviallyNormedField 𝕜₃]
  [inst_6 : NormedSpace 𝕜 E] [inst_7 : NormedSpace 𝕜₂ F] [inst_8 : NormedSpace 𝕜₃ G] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₁₃ : 𝕜 →+* 𝕜₃}
  [RingHomIsometric σ₁₃] (f : E →SL[σ₁₂] F) (g : E →SL[σ₁₃] G), (∀ (x : E), ‖f x‖ = ‖g x‖) → ‖f‖ = ‖g‖
-- Mathlib.Topology.Order.MonotoneConvergence
iSup_eq_iSup_subseq_of_monotone : ∀ {ι₁ : Type u_3} {ι₂ : Type u_4} {α : Type u_5} [inst : Preorder ι₂] [inst_1 : CompleteLattice α] {l : Filter ι₁}
  [l.NeBot] {f : ι₂ → α} {φ : ι₁ → ι₂}, Monotone f → Filter.Tendsto φ l Filter.atTop → ⨆ i, f i = ⨆ i, f (φ i)
-- Mathlib.RingTheory.DedekindDomain.GaussLemma
/-- Given a polynomial `p` in `R[X]`, the `v`-adic Gauss norm of `p` is smaller than 1 if and only
if the content ideal of `p` is contained in the prime ideal corresponding to `v`.  -/
Polynomial.gaussNorm_lt_one_iff_contentIdeal_le : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
  {b : NNReal} (hb : 1 < b) (p : Polynomial R),
  Polynomial.gaussNorm (v.intAdicAbv hb) 1 p < 1 ↔ p.contentIdeal ≤ v.asIdeal
-- Std.Http.Internal.ChunkedBuffer
/-- Writes a `ChunkedBuffer` to the `ChunkedBuffer`.
 -/
Std.Http.Internal.ChunkedBuffer.append : Std.Http.Internal.ChunkedBuffer → Std.Http.Internal.ChunkedBuffer → Std.Http.Internal.ChunkedBuffer
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.IsInaccessible.isStrongLimit : ∀ {c : Cardinal.{u_1}}, c.IsInaccessible → c.IsStrongLimit
-- Mathlib.Order.Filter.Lift
Filter.prod_same_eq : ∀ {α : Type u_1} {f : Filter α}, f ×ˢ f = f.lift' fun t => t ×ˢ t
-- Init.Data.Nat.Lemmas
Nat.log2_two_mul : ∀ {n : ℕ}, n ≠ 0 → (2 * n).log2 = n.log2 + 1
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
/-- An invariant linear map from weight space to coweight space.  -/
RootPairing.Polarization : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → RootPairing ι R M N → [Fintype ι] → M →ₗ[R] N
-- Lean.Data.JsonRpc
Lean.JsonRpc.instBEqRequestID : BEq Lean.JsonRpc.RequestID
-- Mathlib.Analysis.Normed.Group.Uniform
cauchySeq_sum_of_eventually_eq : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] {u v : ℕ → E} {N : ℕ},
  (∀ n ≥ N, u n = v n) →
    (CauchySeq fun n => ∑ k ∈ Finset.range (n + 1), v k) → CauchySeq fun n => ∑ k ∈ Finset.range (n + 1), u k
-- Mathlib.Combinatorics.Matroid.Map
Matroid.mapSetEquiv.ground : ∀ {α : Type u_1} {β : Type u_2} (M : Matroid α) {E : Set β} (e : ↑M.E ≃ ↑E), (M.mapSetEquiv e).E = E
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
DihedralGroup.r_one_pow_n : ∀ {n : ℕ}, DihedralGroup.r 1 ^ n = 1
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.applyPartition.go : {α : Type u} →
  {β : α → Type v} →
    {δ : Type w} →
      [inst : Ord α] →
        (k : α → Ordering) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (List ((a : α) × β a) →
                (c : Std.DTreeMap.Internal.Cell α β k) →
                  (Std.DTreeMap.Internal.Impl.contains' k l = true → c.contains = true) → List ((a : α) × β a) → δ) →
              List ((a : α) × β a) →
                (m : Std.DTreeMap.Internal.Impl α β) →
                  (Std.DTreeMap.Internal.Impl.contains' k l = true → Std.DTreeMap.Internal.Impl.contains' k m = true) →
                    List ((a : α) × β a) → δ
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.tactic.simp.user.exampleBool : Lean.Option Bool
-- Mathlib.LinearAlgebra.Basis.Basic
Module.Basis.uniqueBasis : {ι : Type u_1} →
  {R : Type u_3} →
    {M : Type u_5} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → [Subsingleton R] → Unique (Module.Basis ι R M)
-- Mathlib.Tactic.ClickSuggestions.SectionState
Mathlib.Tactic.ClickSuggestions.SectionKind.noConfusionType : Sort v✝ → Mathlib.Tactic.ClickSuggestions.SectionKind → Mathlib.Tactic.ClickSuggestions.SectionKind → Sort v✝
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_left_split_dvd : ∀ (ctx : Int.Internal.Linear.Context) (p₁ p₂ : Int.Internal.Linear.Poly) (k : ℕ) (a : ℤ)
  (p' : Int.Internal.Linear.Poly),
  Int.Internal.Linear.cooper_left_split ctx p₁ p₂ k →
    Int.Internal.Linear.cooper_left_split_dvd_cert p₁ p' a ↑k = true → a ∣ Int.Internal.Linear.Poly.denote' ctx p'
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.tryCatch_Except : ∀ {α ε : Type u_1} {x : Except ε α} {h : ε → Except ε α}
  (Q : Std.Do.PostCond α (Std.Do.PostShape.except ε Std.Do.PostShape.pure)),
  ⦃(Std.Do.wp x).apply (Q.1, fun e => (Std.Do.wp (h e)).apply Q, Q.2.2)⦄ MonadExceptOf.tryCatch x h ⦃Q⦄
-- Mathlib.RingTheory.Bialgebra.TensorProduct
/-- Representations of `a` and `b` yield a representation of `a * b`.  -/
Coalgebra.Repr.mul : {R : Type u_1} →
  {A : Type u_2} →
    {ι : Type u_4} →
      {κ : Type u_5} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Bialgebra R A] →
              {a b : A} → Coalgebra.Repr R a ι → Coalgebra.Repr R b κ → Coalgebra.Repr R (a * b) (ι × κ)
-- Mathlib.Order.BooleanAlgebra.Set
Set.subset_sdiff_union : ∀ {α : Type u_1} (s t : Set α), s ⊆ s \ t ∪ t
-- Mathlib.Analysis.Normed.Module.Dual
NormedSpace.eq_iff_forall_dual_eq : ∀ (𝕜 : Type u_1) [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {x y : E},
  x = y ↔ ∀ (g : StrongDual 𝕜 E), g x = g y
-- Mathlib.RingTheory.KrullDimension.Basic
Ideal.isMaximal_of_isPrime_of_ne_bot : ∀ {R : Type u_1} [inst : CommSemiring R] [NoZeroDivisors R] [Ring.KrullDimLE 1 R] (I : Ideal R) [I.IsPrime],
  I ≠ ⊥ → I.IsMaximal
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Matrix.charmatrix_one : ∀ {R : Type u_1} [inst : CommRing R] {n : Type u_4} [inst_1 : DecidableEq n] [inst_2 : Fintype n],
  Matrix.charmatrix 1 = Matrix.diagonal fun x => Polynomial.X - 1
-- Std.Http.Protocol.H1.Reader
Std.Http.Protocol.H1.Reader.State.pending.sizeOf_spec : ∀ {dir : Std.Http.Protocol.H1.Direction}, sizeOf Std.Http.Protocol.H1.Reader.State.pending = 1
-- Mathlib.Algebra.Group.Equiv.Opposite
AddOpposite.opMulEquiv_symm_apply : ∀ {α : Type u_2} [inst : Mul α], ⇑AddOpposite.opMulEquiv.symm = AddOpposite.unop
-- Mathlib.Data.DFinsupp.FiniteInfinite
DFinsupp.fintype : {ι : Type u_1} →
  {π : ι → Type u_2} →
    [DecidableEq ι] →
      [inst : (i : ι) → Zero (π i)] → [Fintype ι] → [(i : ι) → Fintype (π i)] → Fintype (Π₀ (i : ι), π i)
-- Mathlib.NumberTheory.Height.Basic
Height.mulHeight_zero : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2}, Height.mulHeight 0 = 1
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.RespectsIso.of_forall_exists_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} [J.RespectsIso] {S : C}
  {R T : CategoryTheory.Presieve S},
  (∀ ⦃Z : C⦄ (g : Z ⟶ S), R g → ∃ Y e, T (CategoryTheory.CategoryStruct.comp e.hom g)) →
    (∀ ⦃Z : C⦄ (g : Z ⟶ S), T g → ∃ Y e, R (CategoryTheory.CategoryStruct.comp e.hom g)) →
      R ∈ J.coverings S → T ∈ J.coverings S
-- Mathlib.Topology.Algebra.UniformConvergence
instSubUniformOnFun.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [inst : Sub β],
  instSubUniformOnFun = { sub := instSubUniformOnFun._aux_1 }
-- Mathlib.Algebra.Free
FreeAddSemigroup.lift_mk_eq_foldl : ∀ {α : Type u} {β : Type v} [inst : AddSemigroup β] {f : α → β} {x : α} {xs : List α},
  (FreeAddSemigroup.lift f) { head := x, tail := xs } = List.foldl (fun x1 x2 => x1 + f x2) (f x) xs
-- Mathlib.Analysis.Convex.Gauge
setOfPred_gauge_lt_one_subset_self : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E},
  Convex ℝ s → 0 ∈ s → Absorbent ℝ s → {x | gauge s x < 1} ⊆ s
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
/-- `deriv ℘ = ℘'`. This is true globally because of junk values.  -/
PeriodPair.deriv_weierstrassP : ∀ (L : PeriodPair), deriv L.weierstrassP = L.derivWeierstrassP
-- Mathlib.FieldTheory.Perfect
iterateFrobeniusEquiv_def : ∀ (R : Type u_1) (p n : ℕ) [inst : CommSemiring R] [inst_1 : ExpChar R p] [inst_2 : PerfectRing R p] (x : R),
  (iterateFrobeniusEquiv R p n) x = x ^ p ^ n
-- Mathlib.Order.Max
IsBot.fst : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {x : α × β}, IsBot x → IsBot x.1
-- Mathlib.MeasureTheory.Function.LpSpace.Indicator
MeasureTheory.Lp.constL_apply : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α)
  [inst : NormedAddCommGroup E] [inst_1 : MeasureTheory.IsFiniteMeasure μ] (𝕜 : Type u_3) [inst_2 : NormedRing 𝕜]
  [inst_3 : Module 𝕜 E] [inst_4 : IsBoundedSMul 𝕜 E] [inst_5 : Fact (1 ≤ p)] (a : E),
  (MeasureTheory.Lp.constL p μ 𝕜) a = (MeasureTheory.Lp.const p μ) a
-- Mathlib.LinearAlgebra.QuadraticForm.Signature
QuadraticForm.sigNeg_weightedSumSquares : ∀ {𝕜 : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] {ι : Type u_5} [inst_2 : Fintype ι] {w : ι → 𝕜}
  [IsStrictOrderedRing 𝕜], sigNeg (QuadraticMap.weightedSumSquares 𝕜 w) = {i | w i < 0}.ncard
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
SeminormFamily.basisSets.eq_1 : ∀ {R : Type u_1} {E : Type u_6} {ι : Type u_9} [inst : SeminormedRing R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  (p : SeminormFamily R E ι), p.basisSets = ⋃ s, ⋃ r, ⋃ (_ : 0 < r), {(s.sup p).ball 0 r}
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.contains_congr : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k k' : α}, cmp k k' = Ordering.eq → t.contains k = t.contains k'
-- Mathlib.CategoryTheory.EssentiallySmall
/-- We define a type alias `ShrinkHoms C` for `C`. When we have `LocallySmall.{w} C`,
we'll put a `Category.{w}` instance on `ShrinkHoms C`.
 -/
CategoryTheory.ShrinkHoms : Type u → Type u
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.Subcomplex.coe_eq_carrier : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D]
  {E : Topology.RelCWComplex.Subcomplex C}, ↑E = E.carrier
-- Mathlib.Topology.Maps.Strict.Group
/-- The product (in the sense of `AddMonoidHom.prodMap`) of strict
additive group homomorphisms is strict.  -/
AddMonoidHom.isStrictMap_prodMap : ∀ {G : Type u_1} {H : Type u_2} {G' : Type u_3} {H' : Type u_4} [inst : AddGroup G'] [inst_1 : AddGroup H']
  [inst_2 : AddGroup G] [inst_3 : AddGroup H] {f : G →+ H} {g : G' →+ H'} [inst_4 : TopologicalSpace G]
  [inst_5 : TopologicalSpace H] [IsTopologicalAddGroup G] [inst_7 : TopologicalSpace G'] [IsTopologicalAddGroup G']
  [inst_9 : TopologicalSpace H'],
  Topology.IsStrictMap ⇑f → Topology.IsStrictMap ⇑g → Topology.IsStrictMap ⇑(f.prodMap g)
-- Mathlib.Order.Cover
/-- **Alias** of the forward direction of `wcovBy_iff_covBy_or_le_and_le`. -/
WCovBy.covBy_or_le_and_le : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ⩿ b → a ⋖ b ∨ a ≤ b ∧ b ≤ a
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- Composition of two linear maps is a linear map  -/
LinearMap.«term_∘ₛₗ_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.sum_map : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [inst : AddCommMonoid M] (s : Finset ι) (e : ι ↪ κ) (f : κ → M),
  ∑ x ∈ Finset.map e s, f x = ∑ x ∈ s, f (e x)
-- Mathlib.Analysis.Complex.CauchyIntegral
/-- **Cauchy-Goursat theorem** for a rectangle: the integral of a complex differentiable function
over the boundary of a rectangle equals zero. More precisely, if `f` is complex differentiable on a
closed rectangle, then its integral over the boundary of the rectangle equals zero.  -/
Complex.integral_boundary_rect_eq_zero_of_differentiableOn : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : ℂ → E) (z w : ℂ),
  DifferentiableOn ℂ f (Set.uIcc z.re w.re ×ℂ Set.uIcc z.im w.im) →
    (((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * Complex.I)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * Complex.I)) +
          Complex.I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * Complex.I)) -
        Complex.I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * Complex.I) =
      0
-- Mathlib.Algebra.Module.Injective
/-- If `x ∈ M ⊔ ⟨y⟩`, then `x = m + r • y`, `snd` pick an arbitrary such `r`.  -/
Module.Baer.ExtensionOfMaxAdjoin.snd : {R : Type u} →
  [inst : Ring R] →
    {Q : Type v} →
      [inst_1 : AddCommGroup Q] →
        [inst_2 : Module R Q] →
          {M : Type u_1} →
            {N : Type u_2} →
              [inst_3 : AddCommGroup M] →
                [inst_4 : AddCommGroup N] →
                  [inst_5 : Module R M] →
                    [inst_6 : Module R N] →
                      (i : M →ₗ[R] N) →
                        {f : M →ₗ[R] Q} →
                          [inst_7 : Fact (Function.Injective ⇑i)] →
                            {y : N} → ↥(Module.Baer.supExtensionOfMaxSingleton i f y) → R
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Zipper.prependMapGT.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (t : Std.DTreeMap.Internal.Impl α β) (lowerBound : α)
  (it : Std.DTreeMap.Internal.Zipper α β),
  Std.DTreeMap.Internal.Zipper.prependMapGT t lowerBound it =
    match t with
    | Std.DTreeMap.Internal.Impl.leaf => it
    | Std.DTreeMap.Internal.Impl.inner size k v l r =>
      match compare lowerBound k with
      | Ordering.lt =>
        Std.DTreeMap.Internal.Zipper.prependMapGT l lowerBound (Std.DTreeMap.Internal.Zipper.cons k v r it)
      | Ordering.eq => Std.DTreeMap.Internal.Zipper.prependMapGT r lowerBound it
      | Ordering.gt => Std.DTreeMap.Internal.Zipper.prependMapGT r lowerBound it
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.mul_apply : ∀ {A : Type u_2} {E : Type u_6} [inst : Monoid A] [inst_1 : TopologicalSpace A] [inst_2 : CommMonoid E]
  [inst_3 : TopologicalSpace E] [inst_4 : ContinuousMul E] (f g : A →ₜ* E) (a : A), (f * g) a = f a * g a
-- Mathlib.Topology.MetricSpace.Pseudo.Pi
Fin.dist_insertNth_insertNth : ∀ {n : ℕ} {α : Fin (n + 1) → Type u_4} [inst : (i : Fin (n + 1)) → PseudoMetricSpace (α i)] (i : Fin (n + 1))
  (x y : α i) (f g : (j : Fin n) → α (i.succAbove j)),
  dist (i.insertNth x f) (i.insertNth y g) = max (dist x y) (dist f g)
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.trans_counitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (e : C ≌ D) (f : D ≌ E),
  (e.trans f).counitIso =
    ((f.inverse.comp e.inverse).associator e.functor f.functor).symm ≪≫
      CategoryTheory.Functor.isoWhiskerRight
          (f.inverse.associator e.inverse e.functor ≪≫ f.inverse.isoWhiskerLeft e.counitIso ≪≫ f.inverse.rightUnitor)
          f.functor ≪≫
        f.counitIso
-- Mathlib.GroupTheory.Perm.Cycle.Factors
/-- If `c` and `d` are cycles of `g`, then `d` stabilizes the support of `c`  -/
Equiv.Perm.mem_support_cycle_of_cycle : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {g d c : Equiv.Perm α},
  c ∈ g.cycleFactorsFinset → d ∈ g.cycleFactorsFinset → ∀ (x : α), d x ∈ c.support ↔ x ∈ c.support
-- Mathlib.Topology.Category.TopCat.Monoidal
TopCat.ι₀_fst : ∀ (X : TopCat),
  CategoryTheory.CategoryStruct.comp TopCat.ι₀ (CategoryTheory.SemiCartesianMonoidalCategory.fst X TopCat.I) =
    CategoryTheory.CategoryStruct.id X
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.eq_pow_of_pow_eq_one : ∀ {R : Type u_4} [inst : CommRing R] [IsDomain R] {k : ℕ} [NeZero k] {ζ ξ : R},
  IsPrimitiveRoot ζ k → ξ ^ k = 1 → ∃ i < k, ζ ^ i = ξ
-- Mathlib.Combinatorics.SetFamily.Compression.UV
UV.IsCompressed.congr_simp : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] {inst_1 : DecidableRel Disjoint} [inst_2 : DecidableRel Disjoint]
  {inst_3 : DecidableLE α} [inst_4 : DecidableLE α] {inst_5 : DecidableEq α} [inst_6 : DecidableEq α] (u u_1 : α),
  u = u_1 → ∀ (v v_1 : α), v = v_1 → ∀ (s s_1 : Finset α), s = s_1 → UV.IsCompressed u v s = UV.IsCompressed u_1 v_1 s_1
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
IsDiscreteValuationRing.addVal_one : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R],
  (IsDiscreteValuationRing.addVal R) 1 = 0
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.oreSub_vadd_oreSub : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] {X : Type u_2}
  [inst_2 : AddAction R X] {r₁ : R} {r₂ : X} {s₁ s₂ : ↥S},
  (r₁ -ₒ s₁) +ᵥ r₂ -ₒ s₂ = (AddOreLocalization.oreMin r₁ s₂ +ᵥ r₂) -ₒ (AddOreLocalization.oreSubtra r₁ s₂ + s₁)
-- Mathlib.RingTheory.PowerSeries.Order
PowerSeries.order_pow : ∀ {R : Type u_1} [inst : Semiring R] [NoZeroDivisors R] [Nontrivial R] (φ : PowerSeries R) (n : ℕ),
  (φ ^ n).order = n • φ.order
-- Mathlib.Algebra.Group.Basic
inv_inj : ∀ {G : Type u_3} [inst : InvolutiveInv G] {a b : G}, a⁻¹ = b⁻¹ ↔ a = b
-- Mathlib.Topology.Category.FinTopCat
FinTopCat.instTopologicalSpaceObjFiniteObjFintypeCatForget₂ContinuousMapCarrierToTopFun : (X : FinTopCat) → TopologicalSpace ((CategoryTheory.forget₂ FinTopCat FintypeCat).obj X).obj
-- Lean.Data.NameTrie
Lean.NameTrie.forMatchingM : {m : Type → Type u_1} → {β : Type u_2} → [Monad m] → Lean.NameTrie β → Lean.Name → (β → m Unit) → m Unit
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.SimpleFunc.measure_lt_top_of_memLp_indicator : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {μ : MeasureTheory.Measure α}
  {p : ENNReal},
  p ≠ 0 →
    p ≠ ⊤ →
      ∀ {c : E},
        c ≠ 0 →
          ∀ {s : Set α} (hs : MeasurableSet s),
            MeasureTheory.MemLp
                (⇑(MeasureTheory.SimpleFunc.piecewise s hs (MeasureTheory.SimpleFunc.const α c)
                    (MeasureTheory.SimpleFunc.const α 0)))
                p μ →
              μ s < ⊤
-- Lean.Meta.Tactic.Grind.ForallProp
Lean.Meta.Grind.addForallSimproc : Lean.Meta.Simprocs → Lean.CoreM Lean.Meta.Simprocs
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.any_eq_false : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α] {p : (a : α) → β a → Bool},
  (↑m).WF → ((↑m).any p = false ↔ ∀ (a : α) (h : m.contains a = true), p a (m.get a h) = false)
-- Mathlib.Topology.Bases
Set.Countable.isSeparable : ∀ {α : Type u} [t : TopologicalSpace α] {s : Set α}, s.Countable → TopologicalSpace.IsSeparable s
-- Lean.Parser.Syntax
Lean.Parser.precedence.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Tactic.Module
Mathlib.Tactic.Module.NF.eq_cons_const : ∀ {R : Type u_2} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : Semiring R] [inst_2 : Module R M] {r : R} (m : M)
  {n : M} {l : Mathlib.Tactic.Module.NF R M}, r = 0 → l.eval = n → ((r, m) ::ᵣ l).eval = n
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
/-- Rotating twice is equivalent to rotating by the sum of the angles.  -/
Orientation.rotation_trans : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (θ₁ θ₂ : Real.Angle), (o.rotation θ₁).trans (o.rotation θ₂) = o.rotation (θ₂ + θ₁)
-- Mathlib.CategoryTheory.Join.Sum
CategoryTheory.Join.inlCompFromSum_hom_app : ∀ (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] (X : C),
  (CategoryTheory.Join.inlCompFromSum C D).hom.app X = CategoryTheory.CategoryStruct.id (CategoryTheory.Join.left X)