mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.OpenPartialHomeomorph.Composition
Homeomorph.trans_toOpenPartialHomeomorph : ∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (e : X ≃ₜ Y) (e' : Y ≃ₜ Z),
  (e.trans e').toOpenPartialHomeomorph = e.toOpenPartialHomeomorph.trans e'.toOpenPartialHomeomorph
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.NullMeasurableSet.compl_iff : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasureTheory.NullMeasurableSet sᶜ μ ↔ MeasureTheory.NullMeasurableSet s μ
-- Mathlib.LinearAlgebra.Pi
/-- The `LinearMap` version of `AddMonoidHom.single` and `Pi.single`.  -/
LinearMap.single : (R : Type u) →
  {ι : Type x} →
    [inst : Semiring R] →
      (φ : ι → Type i) →
        [inst_1 : (i : ι) → AddCommMonoid (φ i)] →
          [inst_2 : (i : ι) → Module R (φ i)] → [DecidableEq ι] → (i : ι) → φ i →ₗ[R] (i : ι) → φ i
-- Lean.Parser.Term
/-- `dbg_trace e; body` evaluates to `body` and prints `e` (which can be an
interpolated string literal) to stderr. It should only be used for debugging.
 -/
Lean.Parser.Term.dbgTrace : Lean.Parser.Parser
-- Mathlib.Control.Traversable.Basic
ApplicativeTransformation.mk.injEq : ∀ {F : Type u → Type v} [inst : Applicative F] {G : Type u → Type w} [inst_1 : Applicative G]
  (app : (α : Type u) → F α → G α) (preserves_pure' : ∀ {α : Type u} (x : α), app α (pure x) = pure x)
  (preserves_seq' : ∀ {α β : Type u} (x : F (α → β)) (y : F α), app β (x <*> y) = app (α → β) x <*> app α y)
  (app_1 : (α : Type u) → F α → G α) (preserves_pure'_1 : ∀ {α : Type u} (x : α), app_1 α (pure x) = pure x)
  (preserves_seq'_1 : ∀ {α β : Type u} (x : F (α → β)) (y : F α), app_1 β (x <*> y) = app_1 (α → β) x <*> app_1 α y),
  ({ app := app, preserves_pure' := preserves_pure', preserves_seq' := preserves_seq' } =
      { app := app_1, preserves_pure' := preserves_pure'_1, preserves_seq' := preserves_seq'_1 }) =
    (app = app_1)
-- Mathlib.NumberTheory.ModularForms.Basic
CuspForm.instNeg : {Γ : Subgroup (GL (Fin 2) ℝ)} → {k : ℤ} → Neg (CuspForm Γ k)
-- Mathlib.AlgebraicGeometry.ColimitsOver
AlgebraicGeometry.Scheme.Cover.ColimitGluingData.functor_map : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.IsStableUnderBaseChange]
  [inst_1 : P.IsMultiplicative] {S : AlgebraicGeometry.Scheme} {J : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover}
  [inst_3 : CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [inst_4 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰]
  (d : AlgebraicGeometry.Scheme.Cover.ColimitGluingData D 𝒰) {i j : 𝒰.I₀} (hij : i ⟶ j),
  d.functor.map hij = (d.transitionMap hij).left
-- Init.Data.Vector.Count
Vector.countP_map : ∀ {α : Type u_2} {β : Type u_1} {n : ℕ} {p : β → Bool} {f : α → β} {xs : Vector α n},
  Vector.countP p (Vector.map f xs) = Vector.countP (p ∘ f) xs
-- Init.Grind.Ordered.Linarith
_private.Init.Grind.Ordered.Linarith.0.Lean.Grind.Linarith.Expr.denote.match_1.eq_2 : ∀ (motive : Lean.Grind.Linarith.Expr → Sort u_1) (v : Lean.Grind.Linarith.Var)
  (h_1 : Unit → motive Lean.Grind.Linarith.Expr.zero)
  (h_2 : (v : Lean.Grind.Linarith.Var) → motive (Lean.Grind.Linarith.Expr.var v))
  (h_3 : (a b : Lean.Grind.Linarith.Expr) → motive (a.add b))
  (h_4 : (a b : Lean.Grind.Linarith.Expr) → motive (a.sub b))
  (h_5 : (k : ℕ) → (a : Lean.Grind.Linarith.Expr) → motive (Lean.Grind.Linarith.Expr.natMul k a))
  (h_6 : (k : ℤ) → (a : Lean.Grind.Linarith.Expr) → motive (Lean.Grind.Linarith.Expr.intMul k a))
  (h_7 : (a : Lean.Grind.Linarith.Expr) → motive a.neg),
  (match Lean.Grind.Linarith.Expr.var v with
    | Lean.Grind.Linarith.Expr.zero => h_1 ()
    | Lean.Grind.Linarith.Expr.var v => h_2 v
    | a.add b => h_3 a b
    | a.sub b => h_4 a b
    | Lean.Grind.Linarith.Expr.natMul k a => h_5 k a
    | Lean.Grind.Linarith.Expr.intMul k a => h_6 k a
    | a.neg => h_7 a) =
    h_2 v
-- Init.Data.Range.Polymorphic.Internal.SignedBitVec
_private.Init.Data.Range.Polymorphic.Internal.SignedBitVec.0.BitVec.Signed.intMinSealed_add_intMinSealed : ∀ {n : ℕ}, BitVec.Signed.intMinSealed✝ n + BitVec.Signed.intMinSealed✝ n = 0
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.id_comp : ∀ {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [inst : VAdd M X] {Y : Type u_6} [inst_1 : VAdd N Y]
  (f : X →ₑ[φ] Y), (AddActionHom.id N).comp f = f
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rxi.Iterator.pairwise_toList_upwardEnumerableLt : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α] [Std.Rxi.IsAlwaysFinite α]
  (it : Std.Iter α), List.Pairwise (fun a b => Std.PRange.UpwardEnumerable.LT a b) it.toList
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.fundamentalInterior_smul : ∀ (G : Type u_1) {H : Type u_2} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] (s : Set α) [inst_2 : Group H]
  [inst_3 : MulAction H α] [SMulCommClass H G α] (g : H),
  MeasureTheory.fundamentalInterior G (g • s) = g • MeasureTheory.fundamentalInterior G s
-- Std.Data.DTreeMap.Internal.Balanced
Std.DTreeMap.Internal.Impl.balancedAtRoot_one_two : Std.DTreeMap.Internal.Impl.BalancedAtRoot 1 2
-- Mathlib.Algebra.Group.Hom.Defs
OneHom.coe_copy : ∀ {M : Type u_4} {N : Type u_5} {x : One M} {x_1 : One N} (f : OneHom M N) (f' : M → N) (h : f' = ⇑f),
  ⇑(f.copy f' h) = f'
-- Mathlib.Algebra.Field.Opposite
AddOpposite.instSemifield : {α : Type u_1} → [Semifield α] → Semifield αᵃᵒᵖ
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getD_filterMap_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  {f : α → β → Option γ} {k k' : α} {fallback : γ},
  t.getKey? k = some k' → (Std.TreeMap.filterMap f t).getD k fallback = (t[k]?.bind (f k')).getD fallback
-- Std.Data.DHashMap.Lemmas
/-- Simpler variant of `getD_filter` when `LawfulBEq` is available.  -/
Std.DHashMap.Const.getD_filter' : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [LawfulBEq α]
  {f : α → β → Bool} {k : α} {fallback : β},
  Std.DHashMap.Const.getD (Std.DHashMap.filter f m) k fallback =
    (Option.filter (f k) (Std.DHashMap.Const.get? m k)).getD fallback
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.L₀X₂ToP.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), S.L₀X₂ToP = CategoryTheory.Limits.pullback.lift S.v₀₁.τ₂ S.L₀.g ⋯
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Substructure.fg_iff_finite : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] [L.IsRelational] {S : L.Substructure M},
  S.FG ↔ Finite ↥S
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.coe_inf : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] (p p' : NonUnitalSubring R), ↑(p ⊓ p') = ↑p ∩ ↑p'
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
SSet.Edge.InvStruct.ofEq_invHomId : ∀ {X : SSet} {x₀ x₁ y₀ y₁ : X.obj (Opposite.op { len := 0 })} {hom : SSet.Edge x₀ x₁} {hom' : SSet.Edge y₀ y₁}
  (I : hom.InvStruct) (hhom : hom.edge = hom'.edge), (I.ofEq hhom).invHomId = I.invHomId.ofEq ⋯ hhom ⋯
-- Mathlib.Algebra.Group.Pi.Lemmas
MulHom.coeFn.eq_1 : ∀ (α : Type u_5) (β : Type u_6) [inst : Mul α] [inst_1 : CommSemigroup β],
  MulHom.coeFn α β = { toFun := fun g => ⇑g, map_mul' := ⋯ }
-- Init.Data.Fin.Fold
Fin.foldr_succ : ∀ {n : ℕ} {α : Sort u_1} (f : Fin (n + 1) → α → α) (x : α),
  Fin.foldr (n + 1) f x = f 0 (Fin.foldr n (fun i => f i.succ) x)
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
uniformContinuous_sub_const : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] (a : α),
  UniformContinuous fun b => b - a
-- Mathlib.CategoryTheory.Galois.GaloisObjects
CategoryTheory.PreGaloisCategory.isGalois_iff_aux : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C] (X : C)
  [inst_2 : CategoryTheory.PreGaloisCategory.IsConnected X],
  CategoryTheory.PreGaloisCategory.IsGalois X ↔
    Nonempty
      (CategoryTheory.Limits.IsTerminal
        (CategoryTheory.Limits.colimit (CategoryTheory.SingleObj.functor (CategoryTheory.Aut.toEnd X))))
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Cover.locallyDirectedPullbackCover.eq_1 : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme}
  [inst : P.IsStableUnderBaseChange] (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X)
  [inst_1 : CategoryTheory.Category.{v_2, u_1} 𝒰.I₀] [inst_2 : 𝒰.LocallyDirected] {Y : AlgebraicGeometry.Scheme}
  (f : Y ⟶ X),
  𝒰.locallyDirectedPullbackCover f =
    {
      trans := fun {i j} hij =>
        CategoryTheory.Limits.pullback.map f (𝒰.f i) f (𝒰.f j) (CategoryTheory.CategoryStruct.id Y) (𝒰.trans hij)
          (CategoryTheory.CategoryStruct.id X) ⋯ ⋯,
      trans_id := ⋯, trans_comp := ⋯, w := ⋯, directed := ⋯, property_trans := ⋯ }
-- Mathlib.Tactic.Module
Mathlib.Tactic.Module.NF.algebraMap.eq_1 : ∀ {S : Type u_1} (R : Type u_2) {M : Type u_3} [inst : CommSemiring S] [inst_1 : Semiring R] [inst_2 : Algebra S R]
  (l : Mathlib.Tactic.Module.NF S M),
  Mathlib.Tactic.Module.NF.algebraMap R l =
    List.map
      (fun x =>
        match x with
        | (s, x) => ((algebraMap S R) s, x))
      l
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBasis.subset_ground : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α}, M.IsBasis I X → X ⊆ M.E
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.emb_invEmbedding : ∀ {n : ℕ} (c : OrderedFinpartition n) (j : Fin n), c.emb (c.index j) (c.invEmbedding j) = j
-- Mathlib.Data.Finset.NAry
/-- If `a` is a left identity for `f : α → β → β`, then `{a}` is a left identity for
`Finset.image₂ f`.  -/
Finset.image₂_left_identity : ∀ {α : Type u_1} {γ : Type u_5} [inst : DecidableEq γ] {f : α → γ → γ} {a : α},
  (∀ (b : γ), f a b = b) → ∀ (t : Finset γ), Finset.image₂ f {a} t = t
-- Mathlib.Topology.PartitionOfUnity
BumpCovering.mk : {ι : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace X] →
      {s : optParam (Set X) Set.univ} →
        (toFun : ι → C(X, ℝ)) →
          (LocallyFinite fun i => Function.support ⇑(toFun i)) →
            0 ≤ toFun → toFun ≤ 1 → (∀ x ∈ s, ∃ i, ⇑(toFun i) =ᶠ[nhds x] 1) → BumpCovering ι X s
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.blastCpop_le_size : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (input : aig.RefVec w),
  aig.decls.size ≤ (Std.Tactic.BVDecide.BVExpr.bitblast.blastCpop aig input).aig.decls.size
-- Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated
CategoryTheory.Pretriangulated.Opposite.complete_distinguished_triangle_morphism : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (T₁ T₂ : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ),
  T₁ ∈ CategoryTheory.Pretriangulated.Opposite.distinguishedTriangles C →
    T₂ ∈ CategoryTheory.Pretriangulated.Opposite.distinguishedTriangles C →
      ∀ (a : T₁.obj₁ ⟶ T₂.obj₁) (b : T₁.obj₂ ⟶ T₂.obj₂),
        CategoryTheory.CategoryStruct.comp T₁.mor₁ b = CategoryTheory.CategoryStruct.comp a T₂.mor₁ →
          ∃ c,
            CategoryTheory.CategoryStruct.comp T₁.mor₂ c = CategoryTheory.CategoryStruct.comp b T₂.mor₂ ∧
              CategoryTheory.CategoryStruct.comp T₁.mor₃ ((CategoryTheory.shiftFunctor Cᵒᵖ 1).map a) =
                CategoryTheory.CategoryStruct.comp c T₂.mor₃
-- Init.Data.BitVec.Lemmas
/-- Unsigned division is zero if and only if either the denominator is zero,
or the numerator is unsigned less than the denominator  -/
BitVec.udiv_eq_zero_iff_eq_zero_or_lt : ∀ {w : ℕ} {x y : BitVec w}, x / y = 0#w ↔ y = 0#w ∨ x < y
-- Init.Data.Iterators.Basic
/-- Termination measure to be used in recursive functions built with `WellFounded.extrinsicFix`
recursing over a productive iterator without requiring a proof of productiveness
(see also `Productive`).
 -/
Std.Iter.finitelyManySkips! : {α β : Type w} → [inst : Std.Iterator α Id β] → Std.Iter β → Std.IterM.TerminationMeasures.Productive α Id
-- Mathlib.Lean.Expr.Basic
Lean.Name.isBlackListed : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Lean.Name → m Bool
-- Init.Data.SInt.Lemmas
Int16.toNatClampNeg_toISize : ∀ (x : Int16), x.toISize.toNatClampNeg = x.toNatClampNeg
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
/-- Verify that the constructed cocone is indeed a colimit.  -/
CategoryTheory.Limits.pushoutCoconeOfRightIsoIsLimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      (f : X ⟶ Y) →
        (g : X ⟶ Z) →
          [inst_1 : CategoryTheory.IsIso g] →
            CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.pushoutCoconeOfRightIso f g)
-- Mathlib.Algebra.Ring.GeomSum
Nat.sub_dvd_pow_sub_pow : ∀ (x y n : ℕ), x - y ∣ x ^ n - y ^ n
-- Mathlib.Order.Hom.Basic
OrderIso.symm_mk : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] (e : α ≃ β)
  (map_rel_iff' : ∀ {a b : α}, e a ≤ e b ↔ a ≤ b),
  OrderIso.symm { toEquiv := e, map_rel_iff' := map_rel_iff' } = { toEquiv := e.symm, map_rel_iff' := ⋯ }
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.diff_eq : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], m₁.diff m₂ = m₁ \ m₂
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Initialize.0.Lean.Meta.RefinedDiscrTree.createImportInitResults.go.eq_def : ∀ {α : Type} (cctx : Lean.Core.Context) (env : Lean.Environment)
  (act :
    Lean.Name →
      Lean.ConstantInfo →
        Lean.MetaM (List (α × List (Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry))))
  (start stop : ℕ) (tree : Lean.Meta.RefinedDiscrTree.PreDiscrTree α)
  (data : Lean.Meta.RefinedDiscrTree.ImportErrorData✝) (mstate : IO.Ref Lean.Meta.State)
  (cstate : IO.Ref Lean.Core.State),
  Lean.Meta.RefinedDiscrTree.createImportInitResults.go✝ cctx env act start stop tree data mstate cstate =
    if start < stop then
      have mname := env.header.moduleNames[start]!;
      have mdata := env.header.moduleData[start]!;
      do
      let tree ← Lean.Meta.RefinedDiscrTree.loadImportedModule✝ cctx env data mstate cstate act mname mdata tree
      Lean.Meta.RefinedDiscrTree.createImportInitResults.go✝ cctx env act (start + 1) stop tree data mstate cstate
    else Lean.Meta.RefinedDiscrTree.toInitResults✝ data tree
-- Std.Do.Triple.SpecLemmas
Std.Do.Iter.foldM_mapWithPostcondition : ∀ {ps : Std.Do.PostShape} {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
  [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Monad m] [inst_3 : Monad n] [inst_4 : Monad o]
  [LawfulMonad m] [LawfulMonad n] [LawfulMonad o] [inst_8 : Std.Do.WPMonad o ps] [inst_9 : Std.IteratorLoop α Id n]
  [inst_10 : Std.IteratorLoop α Id o] [Std.LawfulIteratorLoop α Id n] [Std.LawfulIteratorLoop α Id o]
  [inst_13 : MonadLiftT n o] [LawfulMonadLiftT n o] {f : β → Std.Iterators.PostconditionT n γ} {g : δ → γ → o δ}
  {init : δ} {it : Std.Iter β} {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond δ ps},
  ⦃P⦄
      Std.Iter.foldM
        (fun d b => do
          let c ← liftM (f b).run
          g d c)
        init it ⦃Q⦄ →
    ⦃P⦄ Std.IterM.foldM g init (Std.Iter.mapWithPostcondition f it) ⦃Q⦄
-- Mathlib.Algebra.Ring.Invertible
/-- `-⅟a` is the inverse of `-a`  -/
invertibleNeg : {R : Type u_1} →
  [inst : Mul R] → [inst_1 : One R] → [inst_2 : HasDistribNeg R] → (a : R) → [Invertible a] → Invertible (-a)
-- Mathlib.Order.WithBot
WithTop.exists : ∀ {α : Type u_1} {p : WithTop α → Prop}, (∃ x, p x) ↔ p ⊤ ∨ ∃ x, p ↑x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get!_ofList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    ∀ {v : β} [inst : Inhabited β],
      List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
        (k, v) ∈ l → Std.DTreeMap.Const.get! (Std.DTreeMap.Const.ofList l cmp) k' = v
-- Init.Internal.Order.Basic
Lean.Order.prod_csup_eq : ∀ {α : Sort u} {β : Sort v} [inst : Lean.Order.CCPO α] [inst_1 : Lean.Order.CCPO β] (c : α ×' β → Prop)
  (hchain : Lean.Order.chain c), Lean.Order.prod_csup c hchain = Lean.Order.CCPO.csup hchain
-- Mathlib.MeasureTheory.MeasurableSpace.Invariants
/-- A set `s` is `(invariants f)`-measurable
iff it is measurable w.r.t. the canonical σ-algebra on `α` and `f ⁻¹' s = s`.  -/
MeasurableSpace.measurableSet_invariants : ∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → α} {s : Set α}, MeasurableSet s ↔ MeasurableSet s ∧ f ⁻¹' s = s
-- Mathlib.Tactic.Linter.DirectoryDependency
/-- Look up all names `m` which are values of some prefix of `n` under this relation.  -/
_private.Mathlib.Tactic.Linter.DirectoryDependency.0.Mathlib.Linter.DirectoryDependency.NamePrefixRel.getAllLeft : Mathlib.Linter.DirectoryDependency.NamePrefixRel✝ → Lean.Name → Lean.NameSet
-- Mathlib.Tactic.ByCases
/-- `by_cases! h : p` runs the `by_cases h : p` tactic, followed by
`push Not at h` in the second subgoal. For example,
- `by_cases! h : a < b` creates one goal with hypothesis `h : a < b` and
  another with `h : b ≤ a`.
- `by_cases! h : a ≠ b` creates one goal with hypothesis `h : a ≠ b` and
  another with `h : a = b`.
 -/
Mathlib.Tactic.ByCases.byCases! : Lean.ParserDescr
-- Mathlib.RingTheory.Bialgebra.Equiv
AlgEquiv.ofBijective.congr_simp : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (f f_1 : A₁ →ₐ[R] A₂) (e_f : f = f_1) (hf : Function.Bijective ⇑f),
  AlgEquiv.ofBijective f hf = AlgEquiv.ofBijective f_1 ⋯
-- Mathlib.Data.Nat.Factorization.Defs
Nat.Prime.factorization_pos_of_dvd : ∀ {n p : ℕ}, Nat.Prime p → n ≠ 0 → p ∣ n → 0 < n.factorization p
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
CategoryTheory.ObjectProperty.instFullFullSubcategoryLift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (P : CategoryTheory.ObjectProperty D) (F : CategoryTheory.Functor C D) (hF : ∀ (X : C), P (F.obj X)) [F.Full],
  (P.lift F hF).Full
-- Mathlib.MeasureTheory.Measure.Haar.Quotient
/-- Given a subgroup `Γ` of a topological additive group `G` with measure `ν`, and a
measure 'μ' on the quotient `G ⧸ Γ` satisfying `AddQuotientMeasureEqMeasurePreimage`, the
restriction of `ν` to a fundamental domain is measure-preserving with respect to `μ`.  -/
measurePreserving_quotientAddGroup_mk_of_AddQuotientMeasureEqMeasurePreimage : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : MeasurableSpace G] (ν : MeasureTheory.Measure G) {Γ : AddSubgroup G}
  {𝓕 : Set G},
  MeasureTheory.IsAddFundamentalDomain (↥Γ.op) 𝓕 ν →
    ∀ (μ : MeasureTheory.Measure (G ⧸ Γ)) [MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ],
      MeasureTheory.MeasurePreserving QuotientAddGroup.mk (ν.restrict 𝓕) μ
-- Mathlib.Tactic.CrossRefAttribute
/-- The `lmfdb` attribute.
Use it as `@[lmfdb foo.bar "Optional comment"]` to associate a Mathlib declaration with
the corresponding [LMFDB](https://www.lmfdb.org) item.
 -/
Mathlib.CrossRef.lmfdbTag : Lean.ParserDescr
-- Mathlib.LinearAlgebra.QuadraticForm.Dual
QuadraticForm.dualProdProdIsometry_toFun : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (x : Module.Dual R (M × N) × M × N),
  QuadraticForm.dualProdProdIsometry x = ((x.1 ∘ₗ LinearMap.inl R M N, x.2.1), x.1 ∘ₗ LinearMap.inr R M N, x.2.2)
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
one_lt_mabs_pos_of_one_lt : ∀ {α : Type u_1} [inst : Group α] [inst_1 : LinearOrder α] [MulLeftMono α] {a : α}, 1 < a → 1 < |a|ₘ
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeAddGroup.reduce_cons_reduce : ∀ {α : Type u_1} {L : List (α × Bool)} [inst : DecidableEq α] (a : α × Bool),
  FreeAddGroup.reduce (a :: FreeAddGroup.reduce L) = FreeAddGroup.reduce (a :: L)
-- Batteries.Tactic.OpenPrivate
/-- The command `open private a b c in foo bar` will look for private definitions named `a`, `b`, `c`
in declarations `foo` and `bar` and open them in the current scope. This does not make the
definitions public, but rather makes them accessible in the current section by the short name `a`
instead of the (unnameable) internal name for the private declaration, something like
`_private.Other.Module.0.Other.Namespace.foo.a`, which cannot be typed directly because of the `0`
name component.

It is also possible to specify the module instead with
`open private a b c from Other.Module`.
 -/
Lean.Elab.Command.openPrivate : Lean.ParserDescr
-- Mathlib.Data.Fintype.Perm
_private.Mathlib.Data.Fintype.Perm.0.permsOfList.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h_1 : Unit → motive []) (h_2 : (a : α) → (l : List α) → motive (a :: l)),
  (match [] with
    | [] => h_1 ()
    | a :: l => h_2 a l) =
    h_1 ()
-- Std.Tactic.BVDecide.LRAT.Parser
Std.Tactic.BVDecide.LRAT.Parser.Binary.parseZero : Std.Internal.Parsec.ByteArray.Parser Unit
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.minEntryD.match_1.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → (a : α) × β a → Sort u_3) (size : ℕ)
  (k : α) (v : β k) (r : Std.DTreeMap.Internal.Impl α β) (x : (a : α) × β a)
  (h_1 : (fallback : (a : α) × β a) → motive Std.DTreeMap.Internal.Impl.leaf fallback)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (r : Std.DTreeMap.Internal.Impl α β) →
            (x : (a : α) × β a) →
              motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x)
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β k_1) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r →
                      (r_1 : Std.DTreeMap.Internal.Impl α β) →
                        (fallback : (a : α) × β a) →
                          motive
                            (Std.DTreeMap.Internal.Impl.inner size k v
                              (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) r_1)
                            fallback),
  (match Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x with
    | Std.DTreeMap.Internal.Impl.leaf, fallback => h_1 fallback
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x => h_2 size k v r x
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) r_1,
      fallback => h_3 size k v l size_1 k_1 v_1 l_1 r h r_1 fallback) =
    h_2 size k v r x
-- Lean.Meta.Tactic.Grind.Core
/-- Adds a new `fact` justified by the given proof and using the given generation.  -/
Lean.Meta.Grind.add : Lean.Expr → Lean.Expr → optParam ℕ 0 → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Algebra.Group.Action.Defs
smul_zpow : ∀ {G : Type u_3} {H : Type u_4} [inst : Group G] [inst_1 : Group H] [inst_2 : MulAction G H] [SMulCommClass G H H]
  [IsScalarTower G H H] (g : G) (a : H) (n : ℤ), (g • a) ^ n = g ^ n • a ^ n
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.twoTorsionPolynomial_of_char_two : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [CharP R 2],
  W.twoTorsionPolynomial = { a := 0, b := W.b₂, c := 0, d := W.b₆ }