mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.map_reindex_symm : ∀ {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7}
  [inst_1 : (i : ι) → AddCommMonoid (s i)] [inst_2 : (i : ι) → Module R (s i)] {t : ι → Type u_11}
  [inst_3 : (i : ι) → AddCommMonoid (t i)] [inst_4 : (i : ι) → Module R (t i)] (f : (i : ι) → s i →ₗ[R] t i)
  (e : ι ≃ ι₂) (x : PiTensorProduct R fun i => s (e.symm i)),
  (PiTensorProduct.map f) ((PiTensorProduct.reindex R s e).symm x) =
    (PiTensorProduct.reindex R t e).symm ((PiTensorProduct.map fun i => f (e.symm i)) x)
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth : {α : Type u} → Std.Tactic.BVDecide.LRAT.Internal.ReduceResult α
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.RealizeConstantResult.error? : Lean.Meta.RealizeConstantResult✝ → Option Lean.Exception
-- Init.Data.BitVec.Lemmas
BitVec.zero_width_append : ∀ {v : ℕ} (x : BitVec 0) (y : BitVec v), x ++ y = BitVec.cast ⋯ y
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMon.hom_add : ∀ {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.add.hom = CategoryTheory.AddMonObj.add
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.integral_Ioc_eq_integral_Ioo' : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {μ : MeasureTheory.Measure X} [inst_2 : PartialOrder X] {x y : X},
  μ {y} = 0 → ∫ (t : X) in Set.Ioc x y, f t ∂μ = ∫ (t : X) in Set.Ioo x y, f t ∂μ
-- Mathlib.Algebra.CharP.Lemmas
neg_one_pow_expChar : ∀ (R : Type u_1) [inst : Ring R] (p : ℕ) [hR : ExpChar R p], (-1) ^ p = -1
-- Mathlib.Algebra.Homology.HomologicalBicomplex
/-- Flipping a complex of complexes over the diagonal, as an equivalence of categories.  -/
HomologicalComplex₂.flipEquivalence : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {I₁ : Type u_2} →
        {I₂ : Type u_3} →
          (c₁ : ComplexShape I₁) → (c₂ : ComplexShape I₂) → HomologicalComplex₂ C c₁ c₂ ≌ HomologicalComplex₂ C c₂ c₁
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
/-- The pointwise distance is controlled by the distance between functions, by definition.  -/
BoundedContinuousFunction.dist_coe_le_dist : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
  {f g : BoundedContinuousFunction α β} (x : α), dist (f x) (g x) ≤ dist f g
-- Init.Data.Option.Attach
Option.attach_filter : ∀ {α : Type u_1} {o : Option α} {p : α → Bool},
  (Option.filter p o).attach =
    o.attach.bind fun x =>
      match x with
      | ⟨x, h⟩ => if h' : p x = true then some ⟨x, ⋯⟩ else none
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.instInhabited.eq_1 : MonCat.instInhabited = { default := MonCat.of PUnit.{u_1 + 1} }
-- Mathlib.Tactic.Linter.GlobalAttributeIn
/-- The `globalAttributeInLinter` linter flags any global attributes generated by an
`attribute [...] in` declaration. (This includes the `instance`, `simp` and `ext` attributes.)

Despite the `in`, these define *global* instances, which can be rather misleading.
Instead, remove the `in` or mark them with `local`.
 -/
_private.Mathlib.Tactic.Linter.GlobalAttributeIn.0.Mathlib.Linter.globalAttributeInLinter.globalAttributeIn : Lean.Linter
-- Mathlib.Tactic.FunProp.Types
/-- Pretty print `FunProp.Origin`. Returns string unlike `ppOrigin`.  -/
Mathlib.Meta.FunProp.ppOrigin' : Mathlib.Meta.FunProp.Origin → Lean.MetaM String
-- Lean.Server.FileWorker.SignatureHelp
Lean.Server.FileWorker.SignatureHelp.CandidateKind : Type
-- Mathlib.RingTheory.PolynomialAlgebra
/-- (Implementation detail)

The equivalence, ignoring the algebra structure, `(A ⊗[R] R[X]) ≃ A[X]`.
 -/
PolyEquivTensor.equiv : (R : Type u_1) →
  (A : Type u_3) →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] → [inst_2 : Algebra R A] → TensorProduct R A (Polynomial R) ≃ Polynomial A
-- Mathlib.Algebra.Ring.Subsemiring.Basic
RingHom.mem_rangeS : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] {f : R →+* S} {y : S},
  y ∈ f.rangeS ↔ ∃ x, f x = y
-- Mathlib.Analysis.Normed.Module.DoubleDual
/-- The inclusion of a normed space in its double (topological) strong dual, considered
as a bounded linear map.  -/
NormedSpace.inclusionInDoubleDual : (𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    (E : Type u_2) →
      [inst_1 : SeminormedAddCommGroup E] → [inst_2 : NormedSpace 𝕜 E] → E →L[𝕜] StrongDual 𝕜 (StrongDual 𝕜 E)
-- Std.Http.Data.Method
Std.Http.Method.search.sizeOf_spec : sizeOf Std.Http.Method.search = 1
-- Mathlib.Algebra.Order.UpperLower
IsLowerSet.sub_left : ∀ {α : Type u_2} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {s t : Set α},
  IsLowerSet t → IsUpperSet (s - t)
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
PresheafOfModules.Derivation.Universal.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} {F : CategoryTheory.Functor C D}
  {R : CategoryTheory.Functor Dᵒᵖ CommRingCat}
  {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} {φ : S ⟶ F.op.comp R}
  {d : M.Derivation φ} [inst_2 : SizeOf C] [inst_3 : SizeOf D]
  (desc : {M' : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} → M'.Derivation φ → (M ⟶ M'))
  (fac :
    autoParam
      (∀ {M' : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} (d' : M'.Derivation φ),
        d.postcomp (desc d') = d')
      PresheafOfModules.Derivation.Universal.fac._autoParam)
  (postcomp_injective :
    autoParam
      (∀ {M' : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} (φ_1 φ' : M ⟶ M'),
        d.postcomp φ_1 = d.postcomp φ' → φ_1 = φ')
      PresheafOfModules.Derivation.Universal.postcomp_injective._autoParam),
  sizeOf { desc := desc, fac := fac, postcomp_injective := postcomp_injective } = 1
-- Mathlib.Data.Fintype.Order
/-- A finite Boolean algebra is complete.  -/
Fintype.toCompleteBooleanAlgebra : (α : Type u_2) → [Fintype α] → [BooleanAlgebra α] → CompleteBooleanAlgebra α
-- Init.Data.List.Control
_private.Init.Data.List.Control.0.List.filter.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match false with
    | true => h_1 ()
    | false => h_2 ()) =
    h_2 ()
-- Mathlib.Tactic.DeriveCountable
_private.Mathlib.Tactic.DeriveCountable.0.Mathlib.Deriving.Countable.mkCountableCmds : Lean.InductiveVal → Array Lean.Name → Lean.Elab.TermElabM (Array Lean.Syntax)
-- Mathlib.Algebra.Algebra.Spectrum.Basic
spectrum.resolventSet_of_subsingleton : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] [Subsingleton A] (a : A),
  resolventSet R a = Set.univ
-- Mathlib.Combinatorics.SimpleGraph.Prod
SimpleGraph.Preconnected.boxProd : ∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β},
  G.Preconnected → H.Preconnected → (G □ H).Preconnected
-- Init.Data.Bool
Bool.forall_bool : ∀ {p : Bool → Prop}, (∀ (b : Bool), p b) ↔ p false ∧ p true
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
/-- A version of **Markov's inequality** with elements of Lp.  -/
MeasureTheory.Lp.mul_meas_ge_le_pow_enorm : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] (f : ↥(MeasureTheory.Lp E p μ)),
  p ≠ 0 → p ≠ ⊤ → ∀ (ε : ENNReal), ε * μ {x | ε ≤ ‖↑↑f x‖ₑ ^ p.toReal} ≤ ENNReal.ofReal ‖f‖ ^ p.toReal
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.Splitting.coe_mk : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : AddGroup N] [inst_1 : AddGroup E] [inst_2 : AddGroup G]
  {S : AddGroupExtension N E G} (s : G →+ E) (hs : Function.RightInverse ⇑s ⇑S.rightHom),
  ⇑{ toAddMonoidHom := s, rightInverse_rightHom := hs } = ⇑s
-- Mathlib.RingTheory.RootsOfUnity.Basic
map_rootsOfUnity_eq_pow_self : ∀ {R : Type u_4} {F : Type u_6} {k : ℕ} [NeZero k] [inst : CommRing R] [IsDomain R] [inst_2 : FunLike F R R]
  [MonoidHomClass F R R] (σ : F) (ζ : ↥(rootsOfUnity k R)), ∃ m, σ ↑↑ζ = ↑↑ζ ^ m
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.quotientQuotientEquivQuotientAux_mk_mk : ∀ {G : Type u} [inst : AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (M : AddSubgroup G) [nM : M.Normal] (h : N ≤ M)
  (x : G), (QuotientAddGroup.quotientQuotientEquivQuotientAux N M h) ↑↑x = ↑x
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.shrinkCoyoneda_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] {X Y : Cᵒᵖ}
  {f : X ⟶ Y},
  CategoryTheory.shrinkCoyoneda.{w, v, u}.map f =
    CategoryTheory.FunctorToTypes.shrinkMap (CategoryTheory.coyoneda.map f)
-- Aesop.Forward.State
Aesop.RawHyp.fvarId.injEq : ∀ (fvarId fvarId_1 : Lean.FVarId), (Aesop.RawHyp.fvarId fvarId = Aesop.RawHyp.fvarId fvarId_1) = (fvarId = fvarId_1)
-- Mathlib.Data.List.Chain
List.isChain_of_isChain_pmap : ∀ {α : Type u_1} {β : Type u_2} {R : α → α → Prop} {S : β → β → Prop} {p : α → Prop} (f : (a : α) → p a → β)
  {l : List α} (hl₁ : ∀ a ∈ l, p a),
  List.IsChain S (List.pmap f l hl₁) →
    (∀ (a b : α) (ha : p a) (hb : p b), S (f a ha) (f b hb) → R a b) → List.IsChain R l
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.mem_fixedPoints' : ∀ {M : Type u_1} {α : Type u_3} [inst : AddMonoid M] [inst_1 : AddAction M α] {a : α},
  a ∈ AddAction.fixedPoints M α ↔ ∀ a' ∈ AddAction.orbit M a, a' = a
-- Mathlib.Analysis.Meromorphic.Basic
/-- Eta-expanded form of `Meromorphic.sub` -/
Meromorphic.fun_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f g : 𝕜 → E}, Meromorphic f → Meromorphic g → Meromorphic fun i => f i - g i
-- Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Submodule.isCompl_orthogonal_of_hasOrthogonalProjection : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} [K.HasOrthogonalProjection], IsCompl K Kᗮ
-- Std.Internal.Do.Order.Basic
Lean.Order.le_prop_eq_imp : ∀ (p q : Prop), Lean.Order.PartialOrder.rel p q = (p → q)
-- Lean.Server.Completion.EligibleHeaderDecls
Lean.Server.Completion.EligibleDecl.mk : Lean.ConstantInfo →
  Lean.MetaM Lean.Lsp.CompletionItemKind →
    Lean.MetaM (Array Lean.Lsp.CompletionItemTag) → Lean.Server.Completion.EligibleDecl
-- Lean.Environment
Lean.Environment.Visibility.private.sizeOf_spec : sizeOf Lean.Environment.Visibility.private = 1
-- Mathlib.Data.Set.Image
Set.leftInverse_rangeSplitting : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), Function.LeftInverse (Set.rangeFactorization f) (Set.rangeSplitting f)
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
/-- Given a weak FE-pair `(f, g)`, modify it into a strong FE-pair by subtracting suitable
correction terms from `f` and `g`.

(See `WeakFEPair.isStrongFEPair_toStrongFEPair` for the proof that this is actually a strong
FE-pair.)  -/
WeakFEPair.toStrongFEPair : {E : Type u_1} → [inst : NormedAddCommGroup E] → [inst_1 : NormedSpace ℂ E] → WeakFEPair E → WeakFEPair E
-- Init.Data.Nat.Bitwise.Lemmas
Nat.lt_pow_two_of_testBit : ∀ {n : ℕ} (x : ℕ), (∀ i ≥ n, x.testBit i = false) → x < 2 ^ n
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKeyD_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List (α × β)} {k fallback : α},
  (List.map Prod.fst l).contains k = false →
    (Std.ExtDHashMap.Const.insertMany m l).getKeyD k fallback = m.getKeyD k fallback
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- A *cycle* at `u : V` is a circuit at `u` whose only repeating vertex
is `u` (which appears exactly twice).  -/
SimpleGraph.Walk.IsCycle : {V : Type u} → {G : SimpleGraph V} → {u : V} → G.Walk u u → Prop
-- Lean.Elab.InfoTree.Types
Lean.Elab.InfoTree.context.inj : ∀ {i : Lean.Elab.PartialContextInfo} {t : Lean.Elab.InfoTree} {i_1 : Lean.Elab.PartialContextInfo}
  {t_1 : Lean.Elab.InfoTree}, Lean.Elab.InfoTree.context i t = Lean.Elab.InfoTree.context i_1 t_1 → i = i_1 ∧ t = t_1
-- Std.Tactic.BVDecide.Normalize.Canonicalize
Std.Tactic.BVDecide.Normalize.Bool.and_to_and : ∀ (a b : Bool), (a = true ∧ b = true) = ((a && b) = true)
-- Mathlib.Data.Multiset.Count
Multiset.count_cons_of_ne : ∀ {α : Type u_1} [inst : DecidableEq α] {a b : α},
  a ≠ b → ∀ (s : Multiset α), Multiset.count a (b ::ₘ s) = Multiset.count a s
-- Lean.Meta.TryThis
/-- A packet of information about a "Try this" suggestion
that we store in the infotree for the associated code action to retrieve.
 -/
Lean.Meta.Tactic.TryThis.TryThisInfo : Type
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
/-- The `0`-simplices of `Δ[n]` identify to the elements in `Fin (n + 1)`.  -/
SSet.stdSimplex.obj₀Equiv : {n : ℕ} → (SSet.stdSimplex.obj { len := n }).obj (Opposite.op { len := 0 }) ≃ Fin (n + 1)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey?_eq_none : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α}, a ∉ m → m.getKey? a = none
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.op_f₂₄ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C), sq.op.f₂₄ = sq.f₁₂.op
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.liftInitialSeg_coe : ⇑Ordinal.liftInitialSeg = Ordinal.lift.{v, u}
-- Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes
/-- The level for objects.  -/
Mathlib.Tactic.Monoidal.Context.level₁ : Mathlib.Tactic.Monoidal.Context → Lean.Level
-- Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
_private.Mathlib.LinearAlgebra.Matrix.FixedDetMatrices.0.FixedDetMatrices.reduce_aux : ∀ {m : ℤ} {A : FixedDetMatrix (Fin 2) ℤ m}, ↑A 1 0 ≠ 0 → |↑(FixedDetMatrices.reduceStep A) 1 0| < |↑A 1 0|
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.addCommMonoidWithOne : {α : Type u} → [AddCommMonoidWithOne α] → AddCommMonoidWithOne (WithTop α)
-- Std.Data.DTreeMap.Raw.Iterator
/-- Returns a finite iterator over the entries of a dependent tree map.
The iterator yields the elements of the map in order and then terminates.

**Termination properties:**

* `Finite` instance: always
* `Productive` instance: always
 -/
Std.DTreeMap.Raw.iter : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → Std.Iter ((a : α) × β a)
-- Mathlib.Algebra.Module.GradedModule
/-- The smul multiplication of `A` on `⨁ i, 𝓜 i` from `(⨁ i, 𝓐 i) →+ (⨁ i, 𝓜 i) →+ ⨁ i, 𝓜 i`
turns `⨁ i, 𝓜 i` into an `A`-module
 -/
GradedModule.isModule : {ιA : Type u_1} →
  {ιM : Type u_2} →
    {A : Type u_4} →
      {M : Type u_5} →
        {σ : Type u_6} →
          {σ' : Type u_7} →
            [inst : AddMonoid ιA] →
              [inst_1 : AddAction ιA ιM] →
                [inst_2 : Semiring A] →
                  (𝓐 : ιA → σ') →
                    [inst_3 : SetLike σ' A] →
                      (𝓜 : ιM → σ) →
                        [inst_4 : AddCommMonoid M] →
                          [inst_5 : Module A M] →
                            [inst_6 : SetLike σ M] →
                              [inst_7 : AddSubmonoidClass σ' A] →
                                [inst_8 : AddSubmonoidClass σ M] →
                                  [SetLike.GradedSMul 𝓐 𝓜] →
                                    [inst_10 : DecidableEq ιA] →
                                      [DecidableEq ιM] → [GradedRing 𝓐] → Module A (DirectSum ιM fun i => ↥(𝓜 i))
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.map_X : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] (F : CategoryTheory.Functor C D)
  (E : CategoryTheory.PreZeroHypercover S) (i : E.I₀), (CategoryTheory.PreZeroHypercover.map F E).X i = F.obj (E.X i)
-- Aesop.Util.OrderedHashSet
Aesop.OrderedHashSet.foldlM : {α : Type u_1} →
  [inst : BEq α] →
    [inst_1 : Hashable α] →
      {m : Type u_2 → Type u_3} → {β : Type u_2} → [Monad m] → (β → α → m β) → β → Aesop.OrderedHashSet α → m β
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Three
/-- If `λ` divides `x - 1`, then `λ ^ 4` divides `x ^ 3 - 1`.  -/
IsCyclotomicExtension.Rat.Three.lambda_pow_four_dvd_cube_sub_one_of_dvd_sub_one : ∀ {K : Type u_1} [inst : Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ 3) [inst_1 : NumberField K]
  [IsCyclotomicExtension {3} ℚ K] {x : NumberField.RingOfIntegers K},
  hζ.toInteger - 1 ∣ x - 1 → (hζ.toInteger - 1) ^ 4 ∣ x ^ 3 - 1
-- Mathlib.Order.Category.PartOrd
PartOrd.instCategory : CategoryTheory.Category.{u, u + 1} PartOrd
-- Init.Data.String.Basic
String.Slice.Pos.get_eq_get_str : ∀ {s : String.Slice} {p : s.Pos} {h : p ≠ s.endPos}, p.get h = p.str.get ⋯
-- Init.Notation
/-- The membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. -/
«term_∈_» : Lean.TrailingParserDescr
-- Mathlib.Data.LawfulXor.Basic
/-- A typeclass indicating that the xor operation, `^^^`, is lawful.  -/
LawfulXor : (α : Type u_1) → [XorOp α] → [Zero α] → Prop
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
MulDistribMulAction.toMonoidHomZModOfIsCyclic_apply : ∀ {G : Type u_2} [inst : Group G] {M : Type u_4} [inst_1 : Monoid M] [inst_2 : IsCyclic G]
  [inst_3 : MulDistribMulAction M G] {n : ℕ} (hn : Nat.card G = n) (m : M) (g : G) (k : ℤ),
  (MulDistribMulAction.toMonoidHomZModOfIsCyclic G M hn) m = ↑k → m • g = g ^ k
-- Mathlib.Algebra.Group.Units.Basic
AddUnits.neg_add_eq_neg_add_iff : ∀ {α : Type u} [inst : AddCommMonoid α] (a c : α) (b d : AddUnits α), ↑(-b) + a = ↑(-d) + c ↔ a + ↑d = c + ↑b
-- Mathlib.Tactic.NormNum.Pow
Mathlib.Meta.NormNum.isNat_pow : ∀ {α : Type u_1} [inst : Semiring α] {f : α → ℕ → α} {a : α} {b a' b' c : ℕ},
  f = HPow.hPow →
    Mathlib.Meta.NormNum.IsNat a a' →
      Mathlib.Meta.NormNum.IsNat b b' → a'.pow b' = c → Mathlib.Meta.NormNum.IsNat (f a b) c
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits.0.CategoryTheory.WithTerminal.map.match_1.eq_2 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C]
  (motive : (X Y : CategoryTheory.WithTerminal C) → (X ⟶ Y) → Sort u_3) (a : C)
  (x : CategoryTheory.WithTerminal.of a ⟶ CategoryTheory.WithTerminal.star)
  (h_1 :
    (a a_1 : C) →
      (f : CategoryTheory.WithTerminal.of a ⟶ CategoryTheory.WithTerminal.of a_1) →
        motive (CategoryTheory.WithTerminal.of a) (CategoryTheory.WithTerminal.of a_1) f)
  (h_2 :
    (a : C) →
      (x : CategoryTheory.WithTerminal.of a ⟶ CategoryTheory.WithTerminal.star) →
        motive (CategoryTheory.WithTerminal.of a) CategoryTheory.WithTerminal.star x)
  (h_3 :
    (x : CategoryTheory.WithTerminal.star ⟶ CategoryTheory.WithTerminal.star) →
      motive CategoryTheory.WithTerminal.star CategoryTheory.WithTerminal.star x),
  (match CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.star, x with
    | CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.of a_1, f => h_1 a a_1 f
    | CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.star, x => h_2 a x
    | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x => h_3 x) =
    h_2 a x
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.emptyWithCapacity_equiv_iff_isEmpty : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {c : ℕ}, (Std.DHashMap.emptyWithCapacity c).Equiv m ↔ m.isEmpty = true
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- Lift a functor `F : C ⥤ Comma L R` to the subcategory `P.Comma L R Q W` under
suitable assumptions on `F`.  -/
CategoryTheory.MorphismProperty.Comma.lift : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    {B : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
        {T : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} T] →
            {L : CategoryTheory.Functor A T} →
              {R : CategoryTheory.Functor B T} →
                {P : CategoryTheory.MorphismProperty T} →
                  {Q : CategoryTheory.MorphismProperty A} →
                    {W : CategoryTheory.MorphismProperty B} →
                      [inst_3 : Q.IsMultiplicative] →
                        [inst_4 : W.IsMultiplicative] →
                          {C : Type u_4} →
                            [inst_5 : CategoryTheory.Category.{v_4, u_4} C] →
                              (F : CategoryTheory.Functor C (CategoryTheory.Comma L R)) →
                                (∀ (X : C), P (F.obj X).hom) →
                                  (∀ {X Y : C} (f : X ⟶ Y), Q (F.map f).left) →
                                    (∀ {X Y : C} (f : X ⟶ Y), W (F.map f).right) →
                                      CategoryTheory.Functor C (CategoryTheory.MorphismProperty.Comma L R P Q W)
-- Mathlib.Order.Hom.Basic
RelHom.toOrderHom_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : Preorder β]
  (f : (fun x1 x2 => x1 < x2) →r fun x1 x2 => x1 < x2), ⇑f.toOrderHom = ⇑f
-- Mathlib.NumberTheory.Bernoulli
bernoulli'_three : bernoulli' 3 = 0
-- Std.Time.Time.PlainTime
Std.Time.PlainTime.instHAddOffset_3 : HAdd Std.Time.PlainTime Std.Time.Minute.Offset Std.Time.PlainTime
-- Mathlib.RingTheory.MvPowerSeries.Derivative
_private.Mathlib.RingTheory.MvPowerSeries.Derivative.0.MvPowerSeries.trunc_pderivFun : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] [inst_1 : DecidableEq σ] {i : σ} (f : MvPowerSeries σ R)
  (n : σ →₀ ℕ),
  (MvPowerSeries.trunc R n) (MvPowerSeries.pderivFun i f) =
    (MvPolynomial.pderiv i) ((MvPowerSeries.trunc R (n + fun₀ | i => 1)) f)
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
/-- Pull back a `HasExactLimitsOfShape J` along a functor which preserves and reflects finite colimits
and preserves limits of shape `J`
 -/
CategoryTheory.HasExactLimitsOfShape.domain_of_functor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} (J : Type u_2)
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] [inst_2 : CategoryTheory.Category.{v_2, u_2} J]
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C] [inst_4 : CategoryTheory.Limits.HasLimitsOfShape J D]
  [CategoryTheory.HasExactLimitsOfShape J D] (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.PreservesFiniteColimits F] [CategoryTheory.Limits.ReflectsFiniteColimits F]
  [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.Limits.PreservesLimitsOfShape J F],
  CategoryTheory.HasExactLimitsOfShape J C
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get?.congr_simp : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtTreeSet α cmp),
  t = t_1 → ∀ (a a_1 : α), a = a_1 → t.get? a = t_1.get? a_1
-- Mathlib.Topology.Category.TopPair
TopPair.Hom.w_apply : ∀ {X Y : TopPair} (f : X ⟶ Y) (x : ↑TopPair.snd),
  (CategoryTheory.ConcreteCategory.hom TopPair.map) ((CategoryTheory.ConcreteCategory.hom (TopPair.Hom.snd f)) x) =
    (CategoryTheory.ConcreteCategory.hom (TopPair.Hom.fst f)) ((CategoryTheory.ConcreteCategory.hom TopPair.map) x)
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.append.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (a : α) (as bs : List α) (h_1 : (bs : List α) → motive [] bs)
  (h_2 : (a : α) → (as bs : List α) → motive (a :: as) bs),
  (match a :: as, bs with
    | [], bs => h_1 bs
    | a :: as, bs => h_2 a as bs) =
    h_2 a as bs
-- Mathlib.Data.Part
Part.getOrElse_none : ∀ {α : Type u_1} (d : α) [inst : Decidable Part.none.Dom], Part.none.getOrElse d = d