mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.DoldKan.Compatibility
AlgebraicTopology.DoldKan.Compatibility.equivalenceUnitIso_hom_app : ∀ {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] [inst_2 : CategoryTheory.Category.{v_3, u_3} B]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} {eB : B ≌ B'} {e' : A' ≌ B'}
  {F : CategoryTheory.Functor A B'} {G : CategoryTheory.Functor B A}
  (hG : eB.functor.comp e'.inverse ≅ G.comp eA.functor) (ε : eA.functor ≅ F.comp e'.inverse) (X : A),
  (AlgebraicTopology.DoldKan.Compatibility.equivalenceUnitIso hG ε).hom.app X =
    CategoryTheory.CategoryStruct.comp (eA.unitIso.hom.app X)
      (CategoryTheory.CategoryStruct.comp (eA.inverse.map (ε.hom.app X))
        (CategoryTheory.CategoryStruct.comp (eA.inverse.map (e'.inverse.map (eB.counitIso.inv.app (F.obj X))))
          (CategoryTheory.CategoryStruct.comp (eA.inverse.map (hG.hom.app (eB.inverse.obj (F.obj X))))
            (eA.unitIso.inv.app (G.obj (eB.inverse.obj (F.obj X)))))))
-- Mathlib.Analysis.Normed.Ring.Basic
Prod.normOneClass : ∀ {α : Type u_2} {β : Type u_3} [inst : SeminormedAddCommGroup α] [inst_1 : One α] [NormOneClass α]
  [inst_3 : SeminormedAddCommGroup β] [inst_4 : One β] [NormOneClass β], NormOneClass (α × β)
-- Mathlib.NumberTheory.ModularForms.DedekindEta
ModularForm.eta_q_eq_cexp : ∀ (n : ℕ) (z : ℂ), ModularForm.eta_q n z = Complex.exp (2 * ↑Real.pi * Complex.I * (↑n + 1) * z)
-- Mathlib.Topology.Constructions
IsOpen.isOpenMap_subtype_val : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsOpen s → IsOpenMap Subtype.val
-- Std.Http.Data.URI.Encoding
_private.Std.Http.Data.URI.Encoding.0.List.toByteArray.match_1.eq_2 : ∀ (motive : List UInt8 → ByteArray → Sort u_1) (b : UInt8) (bs : List UInt8) (r : ByteArray)
  (h_1 : (r : ByteArray) → motive [] r) (h_2 : (b : UInt8) → (bs : List UInt8) → (r : ByteArray) → motive (b :: bs) r),
  (match b :: bs, r with
    | [], r => h_1 r
    | b :: bs, r => h_2 b bs r) =
    h_2 b bs r
-- Mathlib.LinearAlgebra.TensorProduct.Pi
/-- (Implementation): Bilinear map for defining `TensorProduct.piRightHom`.  -/
TensorProduct.piRightHomBil : (R : Type u_1) →
  [inst : CommSemiring R] →
    (S : Type u_2) →
      [inst_1 : CommSemiring S] →
        [inst_2 : Algebra R S] →
          (N : Type u_3) →
            [inst_3 : AddCommMonoid N] →
              [inst_4 : Module R N] →
                [inst_5 : Module S N] →
                  [inst_6 : IsScalarTower R S N] →
                    {ι : Type u_4} →
                      (M : ι → Type u_5) →
                        [inst_7 : (i : ι) → AddCommMonoid (M i)] →
                          [inst_8 : (i : ι) → Module R (M i)] →
                            N →ₗ[S] ((i : ι) → M i) →ₗ[R] (i : ι) → TensorProduct R N (M i)
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.factor_comp : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {p p' p'' : Submodule R M} (H1 : p ≤ p') (H2 : p' ≤ p''),
  Submodule.factor H2 ∘ₗ Submodule.factor H1 = Submodule.factor ⋯
-- Mathlib.Order.Interval.Finset.Fin
Fin.card_Ioc : ∀ {n : ℕ} (a b : Fin n), (Finset.Ioc a b).card = ↑b - ↑a
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.of_add_mul_right_left : ∀ {R : Type u} [inst : CommSemiring R] {x y z : R}, IsCoprime (x + z * y) y → IsCoprime x y
-- Lean.Elab.InfoTree.Main
/-- Run `x` as a new child infotree node with header given by `mkInfo`.  -/
Lean.Elab.withInfoContext : {m : Type → Type} →
  [Monad m] → [Lean.Elab.MonadInfoTree m] → {α : Type} → [MonadFinally m] → m α → m Lean.Elab.Info → m α
-- Mathlib.GroupTheory.Finiteness
AddMonoid.instFGNat : AddMonoid.FG ℕ
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
/-- A cofork is a colimit cocone in `Cᵒᵖ` if and only if the corresponding fork in `C` is
a limit cone.  -/
CategoryTheory.Limits.Cofork.isColimitEquivIsLimitUnop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : Cᵒᵖ} →
      {f g : X ⟶ Y} →
        (c : CategoryTheory.Limits.Cofork f g) →
          CategoryTheory.Limits.IsColimit c ≃ CategoryTheory.Limits.IsLimit c.unop
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- If `𝓕` is a filter on `β × β`, then the set of all `UniformFun.gen α β V` for
`V ∈ 𝓕` is a filter basis on `(α →ᵤ β) × (α →ᵤ β)`. This will only be applied to `𝓕 = 𝓤 β` when
`β` is equipped with a `UniformSpace` structure, but it is useful to define it for any filter in
order to be able to state that it has a lower adjoint (see `UniformFun.gc`).  -/
UniformFun.isBasis_gen : ∀ (α : Type u_1) (β : Type u_2) (𝓑 : Filter (β × β)), Filter.IsBasis (fun V => V ∈ 𝓑) (UniformFun.gen α β)
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.aemeasurable : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace β]
  [TopologicalSpace.PseudoMetrizableSpace β] [inst_3 : MeasurableSpace β] [BorelSpace β] (f : α →ₘ[μ] β),
  AEMeasurable (↑f) μ
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.Poly.isUnsatEq.match_1.splitter : (motive : Int.Internal.Linear.Poly → Sort u_1) →
  (p : Int.Internal.Linear.Poly) →
    ((k : ℤ) → motive (Int.Internal.Linear.Poly.num k)) →
      ((x : Int.Internal.Linear.Poly) → (∀ (k : ℤ), x = Int.Internal.Linear.Poly.num k → False) → motive x) → motive p
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.skipPrefix?_prop_eq_some_iff : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String.Slice} {pos : s.Pos},
  s.skipPrefix? P = some pos ↔ ∃ (h : s.startPos ≠ s.endPos), pos = s.startPos.next h ∧ P (s.startPos.get h)
-- LeanSearchClient.LoogleSyntax
LeanSearchClient.unicode_turnstile.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Tactic.TermCongr
/-- (Internal for `congr(...)`)
Elaborates to an expression satisfying `cHole?` that equals the LHS or RHS of `h`,
if the LHS or RHS is available after elaborating `h`. Uses the expected type as a hint.  -/
Mathlib.Tactic.TermCongr.elabCHoleExpand : Lean.Elab.Term.TermElab
-- Qq.Typ
Qq.instToMessageDataQuoted : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
-- Mathlib.NumberTheory.NumberField.Units.Basic
NumberField.Units.coe_ne_zero : ∀ {K : Type u_1} [inst : Field K] (x : (NumberField.RingOfIntegers K)ˣ),
  (algebraMap (NumberField.RingOfIntegers K) K) ↑x ≠ 0
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineSubspace.coe_subtypeₐᵢ : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P] (s : AffineSubspace 𝕜 P)
  [inst_5 : Nonempty ↥s], ⇑s.subtypeₐᵢ = ⇑s.subtype
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
/-- The Law of Quadratic Reciprocity: if `p` and `q` are odd primes, then
`(q / p) = (-1)^((p-1)(q-1)/4) * (p / q)`.  -/
legendreSym.quadratic_reciprocity' : ∀ {p q : ℕ} [inst : Fact (Nat.Prime p)] [inst_1 : Fact (Nat.Prime q)],
  p ≠ 2 → q ≠ 2 → legendreSym q ↑p = (-1) ^ (p / 2 * (q / 2)) * legendreSym p ↑q
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- Composition with a linear isometry equiv on the left preserves the norm of the iterated
derivative within a set.  -/
LinearIsometryEquiv.norm_iteratedFDerivWithin_comp_left : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} {x : E} (g : F ≃ₗᵢ[𝕜] G) (f : E → F),
  UniqueDiffOn 𝕜 s → x ∈ s → ∀ (i : ℕ), ‖iteratedFDerivWithin 𝕜 i (⇑g ∘ f) s x‖ = ‖iteratedFDerivWithin 𝕜 i f s x‖
-- Mathlib.Algebra.Module.Equiv.Basic
Units.mulLeftLinearEquiv_mul_apply : ∀ {R : Type u_9} {A : Type u_10} [inst : Semiring R] [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A] (u v : Aˣ) (x : A),
  ((Units.mulLeftLinearEquiv R A) (u * v)) x = ((Units.mulLeftLinearEquiv R A) u) (((Units.mulLeftLinearEquiv R A) v) x)
-- Mathlib.Tactic.CrossRefAttribute
Mathlib.CrossRef.Database.lmfdb : Mathlib.CrossRef.Database
-- Mathlib.Logic.Equiv.Set
Equiv.apply_ofInjective_symm : ∀ {α : Sort u_3} {β : Type u_4} {f : α → β} (hf : Function.Injective f) (b : ↑(Set.range f)),
  f ((Equiv.ofInjective f hf).symm b) = ↑b
-- Mathlib.LinearAlgebra.AffineSpace.Midpoint
midpoint_vsub_midpoint_same_left : ∀ (R : Type u_1) {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] (p₁ p₂ p₃ : P), midpoint R p₁ p₂ -ᵥ midpoint R p₁ p₃ = ⅟2 • (p₂ -ᵥ p₃)
-- Init.Data.List.Pairwise
List.getD_inj : ∀ {α : Type u_1} {i j : ℕ} {fallback : α} {xs : List α},
  i < xs.length → j < xs.length → xs.Nodup → (xs.getD i fallback = xs.getD j fallback ↔ i = j)
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.HasCoseparator.of_equivalence : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.HasCoseparator C] (α : C ≌ D), CategoryTheory.HasCoseparator D
-- Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Homotopy.ofExtend_extend : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Preadditive C] {K L : HomologicalComplex C c} {f g : K ⟶ L} (h : Homotopy f g)
  (e : c.Embedding c') [inst_3 : e.IsRelIff], (h.extend e).ofExtend = h
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKeyD_eq_fallback : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = true → ∀ {fallback : α}, t.minKeyD fallback = fallback
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.distortion_disjUnion : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.TaggedPrepartition I} [inst : Fintype ι]
  (h : Disjoint π₁.iUnion π₂.iUnion), (π₁.disjUnion π₂ h).distortion = max π₁.distortion π₂.distortion
-- Lean.Data.AssocList
Lean.AssocList.insert : {α : Type u} → {β : Type v} → [BEq α] → Lean.AssocList α β → α → β → Lean.AssocList α β
-- Mathlib.RingTheory.Kaehler.Basic
/-- The module of Kähler differentials (Kahler differentials, Kaehler differentials).
This is implemented as `I / I ^ 2` with `I` the kernel of the multiplication map `S ⊗[R] S →ₐ[R] S`.
To view elements as a linear combination of the form `s • D s'`, use
`KaehlerDifferential.tensorProductTo_surjective` and `Derivation.tensorProductTo_tmul`.

We also provide the notation `Ω[S⁄R]` for `KaehlerDifferential R S`.
Note that the slash is `\textfractionsolidus`.
 -/
KaehlerDifferential : (R : Type u) → (S : Type v) → [inst : CommRing R] → [inst_1 : CommRing S] → [Algebra R S] → Type v
-- Init.Data.UInt.Lemmas
UInt8.eq_sub_iff_add_eq : ∀ {a b c : UInt8}, a = c - b ↔ a + b = c
-- Std.Sync.CancellationToken
Std.instToStringCancellationReason : ToString Std.CancellationReason
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.sub_apply : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M] (a : L)
  {D1 D2 : LieDerivation R L M}, (D1 - D2) a = D1 a - D2 a
-- Lean.Elab.App
Lean.Elab.Term.ElabAppArgs.State.mk : Lean.Expr →
  Lean.Expr →
    Array Lean.Expr →
      List Lean.Elab.Term.Arg →
        List Lean.Elab.Term.NamedArg →
          Option Lean.Expr →
            Array (Lean.Name × Lean.Expr) →
              Array Lean.MVarId →
                Array Lean.MVarId → Bool → Option Lean.MVarId → Array Lean.Name → Lean.Elab.Term.ElabAppArgs.State
-- Mathlib.Order.RelClasses
OrderDual.total_ge : ∀ {α : Type u} [inst : LE α] [h : Std.Total fun x1 x2 => x2 ≤ x1], Std.Total fun x1 x2 => x2 ≤ x1
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.IsRatCondKernelCDF.measurable : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α × β → ℚ → ℝ}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β},
  ProbabilityTheory.IsRatCondKernelCDF f κ ν → Measurable f
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.spanUnop_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} (f : X ⟶ Z) (g : Y ⟶ Z)
  (X_1 : CategoryTheory.Limits.WalkingSpan),
  (CategoryTheory.Limits.spanUnop f g).hom.app X_1 =
    (match X_1 with
      | none => CategoryTheory.Iso.refl (Opposite.unop Z)
      | some CategoryTheory.Limits.WalkingPair.left => CategoryTheory.Iso.refl (Opposite.unop X)
      | some CategoryTheory.Limits.WalkingPair.right => CategoryTheory.Iso.refl (Opposite.unop Y)).hom
-- Mathlib.Data.Set.Sups
/-- `s ⊼ t` is the set of elements of the form `a ⊓ b` where `a ∈ s`, `b ∈ t`.  -/
Set.hasInfs : {α : Type u_2} → [SemilatticeInf α] → HasInfs (Set α)
-- Std.Data.HashMap.Lemmas
Std.HashMap.inter_eq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β}, m₁.inter m₂ = m₁ ∩ m₂
-- Init.Data.UInt.Lemmas
UInt16.zero_lt_one : 0 < 1
-- Mathlib.SetTheory.Cardinal.HasCardinalLT
hasCardinalLT_sum_iff : ∀ (X : Type u) (Y : Type u') (κ : Cardinal.{w}),
  Cardinal.aleph0 ≤ κ → (HasCardinalLT (X ⊕ Y) κ ↔ HasCardinalLT X κ ∧ HasCardinalLT Y κ)
-- Mathlib.Dynamics.Ergodic.Function
/-- Let `f : α → α` be an ergodic map.
Let `g : α → X` be an a.e. strongly measurable function
from `α` to a nonempty metrizable topological space.
If `g` is a.e.-invariant under `f`, then `g` is a.e. constant.  -/
Ergodic.ae_eq_const_of_ae_eq_comp_ae : ∀ {α : Type u_1} {X : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace X]
  [TopologicalSpace.MetrizableSpace X] [Nonempty X] {f : α → α} {g : α → X},
  Ergodic f μ → MeasureTheory.AEStronglyMeasurable g μ → g ∘ f =ᵐ[μ] g → ∃ c, g =ᵐ[μ] Function.const α c
-- Mathlib.LinearAlgebra.RootSystem.Chain
RootPairing.Iic_chainTopCoeff_eq : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : CharZero R] [inst_3 : IsDomain R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsCrystallographic] {i j : ι},
  LinearIndependent R ![P.root i, P.root j] →
    Set.Iic (RootPairing.chainTopCoeff i j) = {k | P.root j + k • P.root i ∈ Set.range ⇑P.root}
-- Mathlib.Order.SuccPred.Basic
/-- See also `Order.succ_eq_of_covBy`.  -/
Order.le_succ_of_wcovBy : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] {a b : α}, a ⩿ b → b ≤ Order.succ a
-- Mathlib.Order.Max
not_isMin_of_lt : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, b < a → ¬IsMin a
-- Mathlib.Topology.Algebra.Monoid
continuousOn_finsetProd : ∀ {ι : Type u_1} {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M]
  [inst_2 : CommMonoid M] [ContinuousMul M] {f : ι → X → M} (s : Finset ι) {t : Set X},
  (∀ i ∈ s, ContinuousOn (f i) t) → ContinuousOn (fun a => ∏ i ∈ s, f i a) t
-- Mathlib.Data.EReal.Basic
EReal.zero_lt_top : 0 < ⊤
-- Std.Data.DTreeMap.Internal.WF.Defs
/-- This is the actual well-formedness invariant: the tree must be a balanced BST.  -/
Std.DTreeMap.Internal.Impl.WF.wf : ∀ {α : Type u} [inst : Ord α] {x : α → Type v} {t : Std.DTreeMap.Internal.Impl α x},
  t.Balanced → (∀ [Std.TransOrd α], t.Ordered) → t.WF
-- Mathlib.Algebra.MvPolynomial.PDeriv
MvPolynomial.pderiv_def : ∀ {R : Type u} {σ : Type v} [inst : CommSemiring R] [inst_1 : DecidableEq σ] (i : σ),
  MvPolynomial.pderiv i = MvPolynomial.mkDerivation R (Pi.single i 1)
-- Lean.Parser.Term
Lean.Parser.Term.char.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.Option.Attach
Option.instLawfulMonadAttach : LawfulMonadAttach Option
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.RealizeValueResult.mk : Except Lean.Exception Dynamic → Option Lean.Language.SnapshotTree → Lean.Meta.RealizeValueResult✝
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.mul_bind : ∀ {α β : Type u} (f : α → FreeGroup β) (x y : FreeGroup α), x * y >>= f = (x >>= f) * (y >>= f)
-- Mathlib.LinearAlgebra.TensorProduct.Pi
_private.Mathlib.LinearAlgebra.TensorProduct.Pi.0.TensorProduct.piRightInv_apply : ∀ (R : Type u_1) [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (N : Type u_3)
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : Module S N] [inst_6 : IsScalarTower R S N] {ι : Type u_4}
  (M : ι → Type u_5) [inst_7 : (i : ι) → AddCommMonoid (M i)] [inst_8 : (i : ι) → Module R (M i)] [inst_9 : Fintype ι]
  [inst_10 : DecidableEq ι] (x : N) (m : (i : ι) → M i),
  ((TensorProduct.piRightInv R S N M) fun i => x ⊗ₜ[R] m i) = x ⊗ₜ[R] m
-- Init.Data.UInt.Bitwise
UInt32.toFin_shiftRight : ∀ (a b : UInt32), b < 32 → (a >>> b).toFin = a.toFin >>> b.toFin
-- Mathlib.Tactic.Tauto
Mathlib.Tactic.Tauto.DistribNotState.mk : List Lean.Expr → Lean.MVarId → Mathlib.Tactic.Tauto.DistribNotState
-- Lean.Data.RArray
_private.Lean.Data.RArray.0.Lean.RArray.getImpl.match_1.eq_2 : ∀ {α : Type u_1} (motive : Lean.RArray α → Sort u_2) (p : ℕ) (l r : Lean.RArray α)
  (h_1 : (x : α) → motive (Lean.RArray.leaf x))
  (h_2 : (p : ℕ) → (l r : Lean.RArray α) → motive (Lean.RArray.branch p l r)),
  (match Lean.RArray.branch p l r with
    | Lean.RArray.leaf x => h_1 x
    | Lean.RArray.branch p l r => h_2 p l r) =
    h_2 p l r
-- Mathlib.AlgebraicGeometry.AffineScheme
/-- The set of affine opens as a subset of `opens X`.  -/
AlgebraicGeometry.Scheme.affineOpens : (X : AlgebraicGeometry.Scheme) → Set X.Opens
-- Mathlib.Order.Antisymmetrization
antisymmRel_swap_apply : ∀ {α : Type u_1} {a b : α} (r : α → α → Prop), AntisymmRel (Function.swap r) a b ↔ AntisymmRel r a b
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.ValueGroupWithZero.lift_mul : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {α : Type u_2} [inst_2 : Mul α]
  (f : R → ↥(ValuativeRel.posSubmonoid R) → α)
  (hf : ∀ (x y : R) (t s : ↥(ValuativeRel.posSubmonoid R)), x * ↑t ≤ᵥ y * ↑s → y * ↑s ≤ᵥ x * ↑t → f x s = f y t),
  (∀ (a b : R) (r s : ↥(ValuativeRel.posSubmonoid R)), f (a * b) (r * s) = f a r * f b s) →
    ∀ (a b : ValuativeRel.ValueGroupWithZero R),
      ValuativeRel.ValueGroupWithZero.lift f hf (a * b) =
        ValuativeRel.ValueGroupWithZero.lift f hf a * ValuativeRel.ValueGroupWithZero.lift f hf b
-- Std.Data.HashMap.Lemmas
Std.HashMap.not_mem_diff_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, k ∈ m₂ → k ∉ m₁ \ m₂
-- Mathlib.LinearAlgebra.Matrix.Basis
Module.Basis.restrictScalars_toMatrix : ∀ {ι : Type u_1} (R₂ : Type u_7) {M₂ : Type u_8} [inst : CommRing R₂] [inst_1 : AddCommGroup M₂] [inst_2 : Module R₂ M₂]
  [inst_3 : Fintype ι] [inst_4 : DecidableEq ι] {S : Type u_9} [inst_5 : CommRing S] [inst_6 : Nontrivial S]
  [inst_7 : Algebra R₂ S] [inst_8 : Module S M₂] [inst_9 : IsScalarTower R₂ S M₂] [inst_10 : IsDomain R₂]
  [inst_11 : Module.IsTorsionFree R₂ S] (b : Module.Basis ι S M₂) (v : ι → ↥(Submodule.span R₂ (Set.range ⇑b))),
  (algebraMap R₂ S).mapMatrix ((Module.Basis.restrictScalars R₂ b).toMatrix v) = b.toMatrix fun i => ↑(v i)
-- Mathlib.GroupTheory.Torsion
/-- The torsion additive submonoid of an abelian group equals the torsion
additive subgroup as an additive submonoid.  -/
AddCommGroup.torsion_eq_torsion_addSubmonoid : ∀ (G : Type u_1) [inst : AddCommGroup G], AddCommMonoid.addTorsion G = (AddCommGroup.torsion G).toAddSubmonoid
-- Mathlib.Algebra.Lie.NonUnitalNonAssocAlgebra
LieAlgebra.instCommutatorRing : (R : Type u) →
  (L : Type v) → [inst : CommRing R] → [inst_1 : LieRing L] → [LieAlgebra R L] → LieAlgebra R (CommutatorRing L)
-- Mathlib.Data.List.Rotate
List.get_rotate : ∀ {α : Type u} (l : List α) (n : ℕ) (k : Fin (l.rotate n).length), (l.rotate n).get k = l.get ⟨(↑k + n) % l.length, ⋯⟩
-- Aesop.Rule
Aesop.RegularRule.unsafe.inj : ∀ {r r_1 : Aesop.UnsafeRule}, Aesop.RegularRule.unsafe r = Aesop.RegularRule.unsafe r_1 → r = r_1
-- Mathlib.RingTheory.PowerSeries.GaussNorm
PowerSeries.HasGaussNorm.hasMvGaussNorm : ∀ {R : Type u_1} [inst : Semiring R] (v : R → ℝ) (c : ℝ) (f : PowerSeries R),
  PowerSeries.HasGaussNorm v c f → MvPowerSeries.HasGaussNorm v (fun x => c) f
-- Init.Data.Option.Lemmas
Option.isNone_choice_iff_not_nonempty : ∀ {α : Type u_1}, (Option.choice α).isNone = true ↔ ¬Nonempty α
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instAddCancelCommMonoid.eq_1 : ∀ {α : Type u_1} [inst : AddCancelCommMonoid α],
  Colex.instAddCancelCommMonoid = { toAddCommMonoid := Colex.instAddCommMonoid, toIsLeftCancelAdd := ⋯ }
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.isTrail_copy : ∀ {V : Type u} {G : SimpleGraph V} {u v u' v' : V} (p : G.Walk u v) (hu : u = u') (hv : v = v'),
  (p.copy hu hv).IsTrail ↔ p.IsTrail
-- Mathlib.LinearAlgebra.Determinant
/-- When the function is over the base ring, the determinant is the evaluation at `1`.  -/
LinearMap.det_ring : ∀ {R : Type u_1} [inst : CommRing R] (f : R →ₗ[R] R), LinearMap.det f = f 1
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurableSet_le' : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
  {τ : Ω → WithTop ι} (hτ : MeasureTheory.IsStoppingTime f τ) (i : ι), MeasurableSet {ω | τ ω ≤ ↑i}
-- Lean.Environment
/-- Returns `true` if `cinfo₁` and `cinfo₂` represent the same theorem/axiom, with `cinfo₁` potentially
being a richer representation; under the module system, a theorem may be weakened to an axiom when
exported. We allow different modules to prove the same theorem.

Motivation: We want to generate equational theorems on demand and potentially
in different files, and we want them to have non-private names.
We may add support for other kinds of definitions in the future. For now, theorems are
sufficient for our purposes.

We may have to revise this design decision and eagerly generate equational theorems when
we implement the module system.

Remark: we do not check whether the theorem `value` field match. This feature is useful and
ensures the proofs for equational theorems do not need to be identical. This decision
relies on the fact that theorem types are propositions, we have proof irrelevance,
and theorems are (mostly) opaque in Lean. For `Acc.rec`, we may unfold theorems
during type-checking, but we are assuming this is not an issue in practice,
and we are planning to address this issue in the future.
 -/
_private.Lean.Environment.0.Lean.subsumesInfo : Std.HashMap Lean.Name Lean.ConstantInfo → Lean.ConstantInfo → Lean.ConstantInfo → Bool
-- Mathlib.Algebra.Homology.HomotopyCofiber
/-- The left inclusion `K ⟶ K.cylinder`.  -/
HomologicalComplex.cylinder.ι₀ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          (K : HomologicalComplex C c) →
            [inst_2 : DecidableRel c.Rel] →
              [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] →
                [inst_4 : K.HasCylinder] → K ⟶ K.cylinder
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.Cover.isOpenEmbedding_fromGlued : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover),
  Topology.IsOpenEmbedding ⇑(AlgebraicGeometry.Scheme.Cover.fromGlued 𝒰)
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.vietoris.closure_finite_subsets : ∀ {α : Type u_1} [inst : TopologicalSpace α] (s : Set α), closure {t | t.Finite ∧ t ⊆ s} = 𝒫 closure s
-- Mathlib.Analysis.SpecificLimits.Basic
ENNReal.exists_pos_tsum_mul_lt_of_countable : ∀ {ε : ENNReal},
  ε ≠ 0 →
    ∀ {ι : Type u_4} [Countable ι] (w : ι → ENNReal),
      (∀ (i : ι), w i ≠ ⊤) → ∃ δ, (∀ (i : ι), 0 < δ i) ∧ ∑' (i : ι), w i * ↑(δ i) < ε
-- Init.Data.Array.Lemmas
Array.map_congr_left : ∀ {α : Type u_1} {xs : Array α} {α_1 : Type u_2} {f g : α → α_1},
  (∀ a ∈ xs, f a = g a) → Array.map f xs = Array.map g xs