mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.Iterators.Lemmas.Producers.Vector
Std.Iterators.Vector.isPlausibleStep_iter_of_pos : ∀ {β : Type w} {n : ℕ} {xs : Vector β n} (h : 0 < n),
  xs.iter.IsPlausibleStep (Std.IterStep.yield (xs.iterFromIdx 1) xs[0])
-- Mathlib.Computability.RegularExpressions
/-- `matchEpsilon P` is true if and only if `P` matches the empty string  -/
RegularExpression.matchEpsilon : {α : Type u_1} → RegularExpression α → Bool
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.instZero : {R : Type r} → [inst : CommRing R] → {W' : WeierstrassCurve.Affine R} → Zero W'.Point
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
dist_dist_dist_le_right : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x y z : α), dist (dist x y) (dist x z) ≤ dist y z
-- Mathlib.Analysis.Normed.Ring.Units
NormedRing.inverse_one_sub_nth_order : ∀ {R : Type u_1} [inst : NormedRing R] [HasSummableGeomSeries R] (n : ℕ),
  ∀ᶠ (t : R) in nhds 0, Ring.inverse (1 - t) = ∑ i ∈ Finset.range n, t ^ i + t ^ n * Ring.inverse (1 - t)
-- Lean.Parser.Types
/-- Returns the character at position `p` of the input string. If `p` is not a valid position, returns
the fallback value `(default : Char)`, which is `'A'`, but does not panic.
 -/
Lean.Parser.InputContext.get : Lean.Parser.InputContext → String.Pos.Raw → Char
-- Mathlib.Tactic.ComputeDegree
/-- The following two lemmas should be viewed as a hand-made "congr"-lemmas.
They achieve the following goals.
* They introduce *two* fresh metavariables replacing the given one `deg`,
  one for the `natDegree ≤` computation and one for the `coeff =` computation.
  This helps `compute_degree`, since it does not "pre-estimate" the degree,
  but it "picks it up along the way".
* They split checking the inequality `coeff p n ≠ 0` into the task of
  finding a value `c` for the `coeff` and then
  proving that this value is non-zero by `coeff_ne_zero`.
 -/
Mathlib.Tactic.ComputeDegree.natDegree_eq_of_le_of_coeff_ne_zero' : ∀ {R : Type u_1} [inst : Semiring R] {deg m o : ℕ} {c : R} {p : Polynomial R},
  p.natDegree ≤ m → p.coeff o = c → c ≠ 0 → m = deg → o = deg → p.natDegree = deg
-- Mathlib.RepresentationTheory.Homological.FiniteCyclic
Rep.FiniteCyclicGroup.resolution_π : ∀ (k : Type u) {G : Type u} [inst : CommRing k] [inst_1 : CommGroup G] [inst_2 : Fintype G] (g : G)
  (hg : ∀ (x : G), x ∈ Subgroup.zpowers g),
  (Rep.FiniteCyclicGroup.resolution k g hg).π = Rep.FiniteCyclicGroup.resolution.π k g
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.toArray_map : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Raw α (fun x => β) cmp}
  {f : α → β → γ},
  Std.DTreeMap.Raw.Const.toArray (Std.DTreeMap.Raw.map f t) =
    Array.map (fun p => (p.1, f p.1 p.2)) (Std.DTreeMap.Raw.Const.toArray t)
-- Mathlib.Topology.MetricSpace.Defs
dist_toAdd : ∀ {X : Type u_1} [inst : Dist X] (a b : Multiplicative X),
  dist (Multiplicative.toAdd a) (Multiplicative.toAdd b) = dist a b
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.div_def : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : Nonempty ι]
  [inst_5 : (i : ι) → Group (G i)] [inst_6 : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)] (i : ι)
  (x y : G i), ⟦⟨i, x⟩⟧ / ⟦⟨i, y⟩⟧ = ⟦⟨i, x / y⟩⟧
-- Mathlib.Control.Monad.Writer
/-- Buffer the output produced by `f` as `w`, then emit `(← f).2 w` in its place.  -/
MonadWriter.pass : {ω : outParam (Type u)} → {M : Type u → Type v} → [self : MonadWriter ω M] → {α : Type u} → M (α × (ω → ω)) → M α
-- Batteries.Data.UnionFind.Basic
/-- Check whether two union-find nodes are equivalent with path compression,
returns `x == y` if either index is out of bounds  -/
Batteries.UnionFind.checkEquivD : Batteries.UnionFind → ℕ → ℕ → Batteries.UnionFind × Bool
-- Std.Internal.Do.Order.Heyting
Lean.Order.instPreservesSupMeet : ∀ (a : Prop), Lean.Order.PreservesSup (Lean.Order.meet a)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.contains_toList : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {k : α},
  m.WF → m.toList.contains k = m.contains k
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Finite
/-- **Alias** of the forward direction of `Set.finite_smul_set`. -/
Set.Finite.of_smul_set : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {a : G} {s : Set α}, (a • s).Finite → s.Finite
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.changeInverse_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) {G : CategoryTheory.Functor D C} (iso : e.inverse ≅ G), (e.changeInverse iso).inverse = G
-- Mathlib.Topology.Separation.Basic
instT1SpaceOfT0SpaceOfR0Space : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T0Space X] [R0Space X], T1Space X
-- Mathlib.Algebra.Order.Interval.Set.Group
Set.sub_mem_Ioo_iff_right : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {a b c d : α},
  a - b ∈ Set.Ioo c d ↔ b ∈ Set.Ioo (a - d) (a - c)
-- Mathlib.Order.Circular
/-- Closed-closed circular interval  -/
Set.cIcc : {α : Type u_1} → [CircularPreorder α] → α → α → Set α
-- Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
mul_lt_mul_iff_of_le_of_le : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : Mul α] [MulLeftMono α] [MulRightMono α] [MulLeftStrictMono α]
  [MulRightStrictMono α] {a₁ a₂ b₁ b₂ : α}, a₁ ≤ a₂ → b₁ ≤ b₂ → (a₁ * b₁ < a₂ * b₂ ↔ a₁ < a₂ ∨ b₁ < b₂)
-- Mathlib.CategoryTheory.SmallObject.Basic
CategoryTheory.MorphismProperty.instOrderBotToTypeOrdSmallObjectκ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (I : CategoryTheory.MorphismProperty C) → [inst_1 : I.HasSmallObjectArgument] → OrderBot I.smallObjectκ.ord.ToType
-- Mathlib.Order.UpperLower.Basic
not_bddBelow_Iic : ∀ {α : Type u_1} [inst : Preorder α] (a : α) [NoMinOrder α], ¬BddBelow (Set.Iic a)
-- Mathlib.Analysis.MellinTransform
/-- Auxiliary lemma to reduce convergence statements from vector-valued functions to real
scalar-valued functions.  -/
mellin_convergent_iff_norm : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℝ → E} {T : Set ℝ},
  T ⊆ Set.Ioi 0 →
    MeasurableSet T →
      MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (Set.Ioi 0)) →
        ∀ {s : ℂ},
          MeasureTheory.IntegrableOn (fun t => ↑t ^ (s - 1) • f t) T MeasureTheory.volume ↔
            MeasureTheory.IntegrableOn (fun t => t ^ (s.re - 1) * ‖f t‖) T MeasureTheory.volume
-- Lean.Environment
_private.Lean.Environment.0.Lean.AsyncConsts.size : Lean.AsyncConsts✝ → ℕ
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMon.hom_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M : CategoryTheory.AddMon C)
  [inst_3 : CategoryTheory.IsCommAddMonObj M.X], CategoryTheory.AddMonObj.zero.hom = CategoryTheory.AddMonObj.zero
-- Mathlib.CategoryTheory.MorphismProperty.Basic
/-- The inverse image of a `MorphismProperty D` by a functor `C ⥤ D`  -/
CategoryTheory.MorphismProperty.inverseImage : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        CategoryTheory.MorphismProperty D → CategoryTheory.Functor C D → CategoryTheory.MorphismProperty C
-- Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly
/-- A family of functors jointly reflects isomorphisms if for every morphism `f : X ⟶ Y`
such that the image of `f` under all `F i` is an isomorphism, then `f` is an isomorphism.  -/
CategoryTheory.JointlyReflectIsomorphisms : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_4, u_1} C] →
    {I : Type u_2} →
      {D : I → Type u_3} →
        [inst_1 : (i : I) → CategoryTheory.Category.{u_5, u_3} (D i)] →
          ((i : I) → CategoryTheory.Functor C (D i)) → Prop
-- Mathlib.Data.List.Forall2
List.rel_foldr : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {R : α → β → Prop} {P : γ → δ → Prop},
  Relator.LiftFun (Relator.LiftFun R (Relator.LiftFun P P)) (Relator.LiftFun P (Relator.LiftFun (List.Forall₂ R) P))
    List.foldr List.foldr
-- Mathlib.RingTheory.Frobenius
AlgHom.IsArithFrobAt.comap_eq : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {φ : S →ₐ[R] S}
  {Q : Ideal S}, φ.IsArithFrobAt Q → ∀ [Q.IsPrime], Ideal.comap φ Q = Q
-- ProofWidgets.Component.Basic
ProofWidgets.InteractiveMessageProps : Type
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.ofNatTrans_succ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  (ε : CategoryTheory.Functor.id C ⟶ F) (G : CategoryTheory.Functor C C),
  (CategoryTheory.SmallObject.SuccStruct.ofNatTrans ε).succ G = G.comp F
-- Mathlib.Data.List.Chain
List.isChain_iff_forall₂ : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α}, List.IsChain R l ↔ List.Forall₂ R l.dropLast l.tail
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.ofMultiset_injective : ∀ (R : Type u) [inst : CommRing R] [IsDomain R], Function.Injective ⇑Polynomial.ofMultiset
-- Std.Http.Protocol.H1.Reader
Std.Http.Protocol.H1.Reader.instBEqBodyState.beq : Std.Http.Protocol.H1.Reader.BodyState → Std.Http.Protocol.H1.Reader.BodyState → Bool
-- Mathlib.Analysis.InnerProductSpace.Defs
PreInnerProductSpace.Core.mk.sizeOf_spec : ∀ {𝕜 : Type u_4} {F : Type u_5} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F] [inst_3 : SizeOf 𝕜]
  [inst_4 : SizeOf F] (toInner : Inner 𝕜 F) (conj_inner_symm : ∀ (x y : F), (starRingEnd 𝕜) (inner 𝕜 y x) = inner 𝕜 x y)
  (re_inner_nonneg : ∀ (x : F), 0 ≤ RCLike.re (inner 𝕜 x x))
  (add_left : ∀ (x y z : F), inner 𝕜 (x + y) z = inner 𝕜 x z + inner 𝕜 y z)
  (smul_left : ∀ (x y : F) (r : 𝕜), inner 𝕜 (r • x) y = (starRingEnd 𝕜) r * inner 𝕜 x y),
  sizeOf
      { toInner := toInner, conj_inner_symm := conj_inner_symm, re_inner_nonneg := re_inner_nonneg,
        add_left := add_left, smul_left := smul_left } =
    1 + sizeOf toInner
-- Lean.Parser.Term
Lean.Parser.Term.optConfig.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Field.Opposite
MulOpposite.instNNRatCast : {α : Type u_1} → [NNRatCast α] → NNRatCast αᵐᵒᵖ
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.Hom.range_subset_ker_support : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y), Set.range ⇑f ⊆ ↑(AlgebraicGeometry.Scheme.Hom.ker f).support
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- The isomorphism between
morphisms from `W` to the cone point of the limit cone for `F`
and cones over `F` with cone point `W`
is natural in `F`.
 -/
CategoryTheory.Limits.limYoneda : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.Limits.HasLimitsOfShape J C] →
          CategoryTheory.Limits.lim.comp
              (CategoryTheory.yoneda.comp
                ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ (Type v) (Type (max v u₁))).obj
                  CategoryTheory.uliftFunctor.{u₁, v})) ≅
            CategoryTheory.cones J C
-- Mathlib.Data.Fin.Tuple.Curry
Function.FromTypes.curryEquiv_apply : ∀ {n : ℕ} {τ : Type u} (p : Fin n → Type u) (a : ((i : Fin n) → p i) → τ),
  (Function.FromTypes.curryEquiv p) a = Function.FromTypes.curry a
-- Init.Grind.Interactive
Lean.Parser.Tactic.anchor : Lean.ParserDescr
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.mem_sup_right : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] {S T : NonUnitalSubalgebra R A} {x : A},
  x ∈ T → x ∈ S ⊔ T
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.addMonoid.eq_1 : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddMonoid α],
  Finset.addMonoid = Function.Injective.addMonoid SetLike.coe ⋯ ⋯ ⋯ ⋯
-- Mathlib.Analysis.Distribution.TemperedDistribution
TemperedDistribution.instFourierPairInv : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E]
  [inst_2 : FiniteDimensional ℝ E] [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] [inst_5 : AddCommGroup F]
  [inst_6 : Module ℂ F] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F]
  [inst_9 : ContinuousConstSMul ℂ F], FourierInvPair (TemperedDistribution E F) (TemperedDistribution E F)
-- Mathlib.Analysis.Distribution.Sobolev
/-- The Fourier multiplier with a bounded function maps `H ^ s` to `H ^ s`.  -/
TemperedDistribution.MemSobolev.fourierMultiplierCLM_of_bounded : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : FiniteDimensional ℝ E] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E]
  [inst_6 : InnerProductSpace ℂ F] [inst_7 : CompleteSpace F] {s : ℝ} {f : TemperedDistribution E F},
  TemperedDistribution.MemSobolev s 2 f →
    ∀ {g : E → ℂ},
      Function.HasTemperateGrowth g →
        (∃ C, ∀ (x : E), ‖g x‖ ≤ C) →
          TemperedDistribution.MemSobolev s 2 ((TemperedDistribution.fourierMultiplierCLM F g) f)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.diagramIsoSpan_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingSpan C) (X : CategoryTheory.Limits.WalkingSpan),
  (CategoryTheory.Limits.diagramIsoSpan F).inv.app X = ((fun j => CategoryTheory.eqToIso ⋯) X).inv
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.default_def : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂], default = 0
-- Std.Tactic.BVDecide.LRAT.Internal.Entails
Std.Tactic.BVDecide.LRAT.Internal.Limplies.refl : ∀ {α : Type u} {σ : Type v} [inst : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ] (f : σ),
  Std.Tactic.BVDecide.LRAT.Internal.Limplies α f f
-- Mathlib.LinearAlgebra.Complex.Module
Complex.coe_selfAdjointEquiv : ∀ (z : ↥(selfAdjoint ℂ)), ↑(Complex.selfAdjointEquiv z) = ↑z
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.Grothendieck.mk.inj : ∀ {𝒮 : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} 𝒮}
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} {base : 𝒮}
  {fiber : ↑(F.obj { as := base })} {base_1 : 𝒮} {fiber_1 : ↑(F.obj { as := base_1 })},
  { base := base, fiber := fiber } = { base := base_1, fiber := fiber_1 } → base = base_1 ∧ fiber ≍ fiber_1
-- Mathlib.Order.Category.BddDistLat
BddDistLat.Hom.ext_iff : ∀ {X Y : BddDistLat} {x y : X.Hom Y}, x = y ↔ x.hom' = y.hom'
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.RespectsIso.precomp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) [P.RespectsIso]
  {X Y Z : C} (e : X ⟶ Y) [CategoryTheory.IsIso e] (f : Y ⟶ Z), P f → P (CategoryTheory.CategoryStruct.comp e f)
-- Mathlib.MeasureTheory.Measure.Haar.Extension
TopologicalGroup.IsSES.pushforward_mono : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : Group A] [inst_1 : Group B] [inst_2 : Group C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] {φ : A →* B} {ψ : B →* C}
  (H : TopologicalGroup.IsSES φ ψ) [inst_6 : IsTopologicalGroup A] [inst_7 : IsTopologicalGroup B]
  [inst_8 : MeasurableSpace A] [inst_9 : BorelSpace A] (μA : MeasureTheory.Measure A) [hμA : μA.IsHaarMeasure]
  [inst_10 : IsTopologicalGroup C] [inst_11 : LocallyCompactSpace B] {f g : CompactlySupportedContinuousMap B ℝ},
  f ≤ g → (H.pushforward μA) f ≤ (H.pushforward μA) g
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.inclHomEquiv_symm_apply_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) (Y : CategoryTheory.Limits.FormalCoproduct C)
  (f : (i : Y.I) × (X ⟶ Y.obj i)) (x : ((CategoryTheory.Limits.FormalCoproduct.incl C).obj X).I),
  ((CategoryTheory.Limits.FormalCoproduct.inclHomEquiv X Y).symm f).f x = f.fst
-- Lean.Server.References
/-- Direct imports of the module.  -/
Lean.Server.Ilean.directImports : Lean.Server.Ilean → Array Lean.Lsp.ImportInfo
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.range_path_ssubset_univ : ∀ (x y : Circle), Set.range ⇑(x.path y) ⊂ Set.univ
-- Mathlib.Topology.Baire.BaireMeasurable
BaireMeasurableSet.inter : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s t : Set α},
  BaireMeasurableSet s → BaireMeasurableSet t → BaireMeasurableSet (s ∩ t)
-- Lean.Widget.InteractiveCode
Lean.Widget.DiffTag.willChange : Lean.Widget.DiffTag
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getD_union_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α} {fallback : β},
  k ∉ m₁ → Std.DHashMap.Const.getD (m₁.union m₂) k fallback = Std.DHashMap.Const.getD m₂ k fallback
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
/-- The parts in a complete equipartite subgraph.  -/
SimpleGraph.CompleteEquipartiteSubgraph.parts : {V : Type u_1} → {G : SimpleGraph V} → {r t : ℕ} → G.CompleteEquipartiteSubgraph r t → Finset (Finset V)
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.one_eq_coe : ∀ {α : Type u} [inst : One α] {a : α}, 1 = ↑a ↔ a = 1
-- Mathlib.Algebra.Algebra.Opposite
AlgHom.toRingHom_op : ∀ {R : Type u_1} {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] (f : A →ₐ[R] B), (AlgHom.op f).toRingHom = RingHom.op f.toRingHom
-- Mathlib.NumberTheory.RamificationInertia.Inertia
/-- **Alias** of `Ideal.inertiaDeg'_pos'`.

---

Variant with a weaker constraint, but on the prime upstairs instead.  -/
Ideal.inertiaDeg_pos' : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R) (P : Ideal S)
  [P.IsPrime] [Module.Finite R S] [P.LiesOver p], 0 < p.inertiaDeg' P
-- Mathlib.GroupTheory.Sylow
/-- A Sylow p-subgroup has index indivisible by `p`, assuming [N(P) : P] < ∞.  -/
Sylow.not_dvd_index' : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] [hp : Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G),
  (↑P).relIndex (Subgroup.normalizer ↑P) ≠ 0 → ¬p ∣ (↑P).index
-- Lean.Elab.DeclModifiers
Lean.Elab.Modifiers.visibility : Lean.Elab.Modifiers → Lean.Elab.Visibility
-- Mathlib.CategoryTheory.FiberedCategory.Cartesian
CategoryTheory.Functor.IsStronglyCartesian.fac_assoc : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [inst_2 : p.IsStronglyCartesian f φ]
  {R' : 𝒮} {a' : 𝒳} {g : R' ⟶ R} {f' : R' ⟶ S} (hf' : f' = CategoryTheory.CategoryStruct.comp g f) (φ' : a' ⟶ b)
  [inst_3 : p.IsHomLift f' φ'] {Z : 𝒳} (h : b ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsStronglyCartesian.map p f φ hf' φ')
      (CategoryTheory.CategoryStruct.comp φ h) =
    CategoryTheory.CategoryStruct.comp φ' h
-- Mathlib.Order.DirectedInverseSystem
InverseSystem.unique_pEquivOn : ∀ {ι : Type u_6} {F : ι → Type u_7} {X : ι → Type u_8} [inst : LinearOrder ι] {f : ⦃i j : ι⦄ → i ≤ j → F j → F i}
  [inst_1 : SuccOrder ι] {equivSucc : ⦃i : ι⦄ → ¬IsMax i → F (Order.succ i) ≃ F i × X i} {s : Set ι} [WellFoundedLT ι],
  IsLowerSet s → ∀ {e₁ e₂ : InverseSystem.PEquivOn f equivSucc s}, e₁ = e₂
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
OrderIso.map_csInf' : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] [inst_1 : ConditionallyCompleteLattice β]
  (e : α ≃o β) {s : Set α}, s.Nonempty → BddBelow s → e (sInf s) = sInf (⇑e '' s)
-- Mathlib.GroupTheory.GroupAction.Quotient
AddAction.QuotientAction.mk : ∀ {G : Type u} {X : Type v} [inst : AddGroup G] [inst_1 : AddMonoid X] [inst_2 : AddAction X G] {H : AddSubgroup G},
  (∀ (x : X) {g g' : G}, -g + g' ∈ H → -(x +ᵥ g) + (x +ᵥ g') ∈ H) → AddAction.QuotientAction X H
-- Mathlib.CategoryTheory.Galois.Basic
CategoryTheory.PreGaloisCategory.instHasColimitsOfShapeSingleObjOfFinite : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.PreGaloisCategory C] {G : Type u_1}
  [inst_2 : Group G] [Finite G], CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.SingleObj G) C
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestRevMatch.isLongestRevMatchAt_ofSliceTo : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {p₀ : s.Pos}
  {pos : (s.sliceTo p₀).Pos},
  String.Slice.Pattern.Model.IsLongestRevMatch pat pos →
    String.Slice.Pattern.Model.IsLongestRevMatchAt pat (String.Slice.Pos.ofSliceTo pos) p₀
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.all_eq_true_iff_forall_mem : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α] {p : α → Bool},
  m.WF → (m.all p = true ↔ ∀ a ∈ m, p a = true)
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.limit_ext_iff : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J ProfiniteGrp.{max v u}}
  {x y : ↑(ProfiniteGrp.limit F).toProfinite.toTop}, x = y ↔ ∀ (j : J), ↑x j = ↑y j
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.instMonoFromOpcycles : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ), CategoryTheory.Mono (X.fromOpcycles f g fg h n)
-- Mathlib.Analysis.Complex.Convex
convex_halfSpace_re_gt : ∀ (r : ℝ), Convex ℝ {c | r < c.re}
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.size_filter_le_size : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {f : (a : α) → β a → Bool}, m.WF → (Std.DHashMap.Raw.filter f m).size ≤ m.size
-- Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
InnerProductSpace.HarmonicAt.congr_simp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] (f f_1 : E → F),
  f = f_1 → ∀ (x x_1 : E), x = x_1 → InnerProductSpace.HarmonicAt f x = InnerProductSpace.HarmonicAt f_1 x_1
-- Lean.Compiler.NameMangling
_private.Lean.Compiler.NameMangling.0.Lean.Name.demangleAux.match_6.splitter : (s : String) →
  (motive : Char → Option (s.Pos × ℕ) → Sort u_1) →
    (ch : Char) →
      (x : Option (s.Pos × ℕ)) →
        ((q : s.Pos) → (v : ℕ) → x = some (q, v) → motive 'x' (some (q, v))) →
          ((x_1 : Char) →
              (x_2 : Option (s.Pos × ℕ)) →
                (∀ (q : s.Pos) (v : ℕ), x_1 = 'x' → x_2 = some (q, v) → False) → x = x_2 → motive x_1 x_2) →
            motive ch x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback₃.p₁₂_p₁_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S}
  {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃}
  {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} (h : CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃) {Z : C}
  (h_1 : X₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp h.p₁₂ (CategoryTheory.CategoryStruct.comp h₁₂.p₁ h_1) =
    CategoryTheory.CategoryStruct.comp h.p₁ h_1