mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.ModelTheory.Encoding
FirstOrder.Language.BoundedFormula.listEncode.eq_4 : ∀ {L : FirstOrder.Language} {α : Type u'} (x : ℕ) (φ₁ φ₂ : L.BoundedFormula α x),
  (φ₁.imp φ₂).listEncode = Sum.inr (Sum.inr 0) :: φ₁.listEncode ++ φ₂.listEncode
-- Mathlib.Data.Nat.Factorization.PrimePow
Nat.exponent_dvd_of_prime_pow_eq_pow : ∀ {p a m n : ℕ}, Nat.Prime p → p ^ m = a ^ n → n ∣ m
-- Mathlib.Algebra.Group.Submonoid.Saturation
AddSubmonoid.saturation.eq_1 : ∀ {M : Type u_1} [inst : AddZeroClass M] (s : AddSubmonoid M), s.saturation = sInf {t | s ≤ t.toAddSubmonoid}
-- Std.Data.ExtDTreeMap.Basic
Std.ExtDTreeMap.instInsertSigmaOfTransCmp : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Insert ((a : α) × β a) (Std.ExtDTreeMap α β cmp)
-- Mathlib.Topology.MetricSpace.ThickenedIndicator
one_le_thickenedIndicator_apply' : ∀ {X : Type u_2} [inst : PseudoEMetricSpace X] {δ : ℝ} (δ_pos : 0 < δ) {F : Set X} {x : X},
  x ∈ closure F → 1 ≤ (thickenedIndicator δ_pos F) x
-- Std.Time.Zoned.Database.TZdb
Std.Time.Database.TZdb.instBEqTZSpec.beq : Std.Time.Database.TZdb.TZSpec → Std.Time.Database.TZdb.TZSpec → Bool
-- Mathlib.Topology.Defs.Basic
IsOpen.inter : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsOpen s → IsOpen t → IsOpen (s ∩ t)
-- Mathlib.Topology.DenseEmbedding
IsDenseEmbedding.toIsDenseInducing : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {e : α → β},
  IsDenseEmbedding e → IsDenseInducing e
-- Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
AlgebraicClosure.instAlgebra : (k : Type u) →
  [inst : Field k] → {R : Type u_1} → [inst_1 : CommSemiring R] → [Algebra R k] → Algebra R (AlgebraicClosure k)
-- Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion
/-- Construct an abstract simplicial complex from a simple graph, where vertices of the graph
are 0-simplices and edges are 1-simplices.
 -/
Geometry.AbstractSimplicialComplex.ofSimpleGraph : {ι : Type u_1} → [DecidableEq ι] → SimpleGraph ι → AbstractSimplicialComplex ι
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
IsLocalDiffeomorphAt.contmdiffOn_localInverse : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H₁ : Type u_5}
  [inst_5 : TopologicalSpace H₁] {H₂ : Type u_6} [inst_6 : TopologicalSpace H₂] {I : ModelWithCorners 𝕜 E H₁}
  {J : ModelWithCorners 𝕜 F H₂} {M : Type u_8} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H₁ M] {N : Type u_9}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H₂ N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  (hf : IsLocalDiffeomorphAt I J n f x), ContMDiffOn J I n (↑hf.localInverse.toPartialEquiv) hf.localInverse.source
-- Mathlib.Computability.Primrec.Basic
Primrec₂.const : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable σ]
  (x : σ), Primrec₂ fun x_1 x_2 => x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.of_forall_get?_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], (∀ (k : α), t₁.get? k = t₂.get? k) → t₁.Equiv t₂
-- Mathlib.NumberTheory.Padics.PadicNumbers
PadicSeq.valuation.eq_1 : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (f : PadicSeq p),
  f.valuation = if hf : f ≈ 0 then 0 else padicValRat p (↑f (PadicSeq.stationaryPoint hf))
-- Mathlib.NumberTheory.LSeries.Nonvanishing
_private.Mathlib.NumberTheory.LSeries.Nonvanishing.0.DirichletCharacter.re_log_comb_nonneg' : ∀ {a : ℝ},
  0 ≤ a →
    a < 1 →
      ∀ {z : ℂ},
        ‖z‖ = 1 →
          0 ≤ 3 * (-Complex.log (1 - ↑a)).re + 4 * (-Complex.log (1 - ↑a * z)).re + (-Complex.log (1 - ↑a * z ^ 2)).re
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
RootPairing.polarizationEquiv_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : Field R] [inst_4 : Module R M] [inst_5 : Module R N] (P : RootPairing ι R M N)
  [inst_6 : P.IsAnisotropic] [inst_7 : P.IsRootSystem] (m : M), P.PolarizationEquiv m = P.Polarization m
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.Gate.xor : Std.Tactic.BVDecide.Gate
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField
AlgebraicGeometry.LocallyRingedSpace.evaluation_ne_zero_iff_mem_basicOpen : ∀ (X : AlgebraicGeometry.LocallyRingedSpace) {U : TopologicalSpace.Opens ↑X.toTopCat} (x : ↥U)
  (f : ↑(X.presheaf.obj (Opposite.op U))),
  (CategoryTheory.ConcreteCategory.hom (X.evaluation x)) f ≠ 0 ↔ ↑x ∈ X.toRingedSpace.basicOpen f
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_indicator : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {s t : Set X} {μ : MeasureTheory.Measure X},
  MeasurableSet t → ∫ (x : X) in s, t.indicator f x ∂μ = ∫ (x : X) in s ∩ t, f x ∂μ
-- Mathlib.Algebra.Lie.Nilpotent
LieHom.isNilpotent_range : ∀ {R : Type u} {L : Type v} {L' : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing L'] [inst_4 : LieAlgebra R L'] [LieRing.IsNilpotent L] (f : L →ₗ⁅R⁆ L'),
  LieRing.IsNilpotent ↥f.range
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.det_ne_zero : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] [Nontrivial R]
  (g : Matrix.SpecialLinearGroup n R), (↑g).det ≠ 0
-- Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
/-- If `i` is an `F`-algebra homomorphism from `E` to `K`, then `i x` is contained in
`perfectClosure F K` if and only if `x` is contained in `perfectClosure F E`.  -/
map_mem_perfectClosure_iff : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type w} [inst_3 : Field K]
  [inst_4 : Algebra F K] (i : E →ₐ[F] K) {x : E}, i x ∈ perfectClosure F K ↔ x ∈ perfectClosure F E
-- Mathlib.Order.Interval.Finset.Defs
Set.finite_iff_bddBelow : ∀ {α : Type u_3} {s : Set α} [inst : SemilatticeInf α] [LocallyFiniteOrder α] [OrderTop α], s.Finite ↔ BddBelow s
-- Mathlib.LinearAlgebra.QuadraticForm.Basis
/-- Given an ordered basis, produce a bilinear form associated with the quadratic form.

Unlike `QuadraticMap.associated`, this is not symmetric; however, as a result it can be used even
in characteristic two. When considered as a matrix, the form is triangular.  -/
QuadraticMap.toBilin : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [LinearOrder ι] →
          [inst : CommRing R] →
            [inst_1 : AddCommGroup M] →
              [inst_2 : AddCommGroup N] →
                [inst_3 : Module R M] →
                  [inst_4 : Module R N] → QuadraticMap R M N → Module.Basis ι R M → LinearMap.BilinMap R M N
-- Mathlib.Topology.Algebra.Monoid
IsCompact.add : ∀ {N : Type u_4} [inst : TopologicalSpace N] [inst_1 : Add N] [ContinuousAdd N] {s t : Set N},
  IsCompact s → IsCompact t → IsCompact (s + t)
-- Lean.Elab.BuiltinCommand
Lean.Elab.Command.elabWithExporting : Lean.Elab.Command.CommandElab
-- Init.Data.UInt.Lemmas
UInt8.toFin_toUInt32 : ∀ (n : UInt8), n.toUInt32.toFin = Fin.castLE UInt8.toFin_toUInt32._proof_1 n.toFin
-- Mathlib.Geometry.Manifold.StructureGroupoid
/-- The trivial restriction-closed groupoid, containing only open partial homeomorphisms equivalent
to the restriction of the identity to the various open subsets.  -/
idRestrGroupoid : {H : Type u_1} → [inst : TopologicalSpace H] → StructureGroupoid H
-- Mathlib.LinearAlgebra.Matrix.Hadamard
Matrix.diagonal_hadamard_diagonal : ∀ {α : Type u_1} {n : Type u_3} [inst : DecidableEq n] [inst_1 : MulZeroClass α] (v w : n → α),
  (Matrix.diagonal v).hadamard (Matrix.diagonal w) = Matrix.diagonal (v * w)
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.calc_eval_z' : {p : ℕ} →
  [inst : Fact (Nat.Prime p)] →
    {R : Type u_1} →
      [inst_1 : CommSemiring R] →
        [inst_2 : Algebra R ℤ_[p]] →
          {F : Polynomial R} →
            {a : ℤ_[p]} →
              ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 →
                {z z' z1 : ℤ_[p]} →
                  z' = z - z1 →
                    {n : ℕ} →
                      ih_gen✝ n z →
                        (h1 : ‖↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F))‖ ≤ 1) →
                          z1 = ⟨↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F)), h1⟩ →
                            { q // (Polynomial.aeval z') F = q * z1 ^ 2 }
-- Mathlib.Lean.Thunk
Thunk.add_get : ∀ {α : Type u} [inst : Add α] {a b : Thunk α}, (a + b).get = a.get + b.get
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.LeftLift.w_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  {s t : CategoryTheory.Bicategory.LeftLift f g} (h : s ⟶ t) {Z : c ⟶ a}
  (h_1 : CategoryTheory.CategoryStruct.comp (CategoryTheory.StructuredArrow.right t) f ⟶ Z),
  CategoryTheory.CategoryStruct.comp s.unit
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.StructuredArrow.Hom.right h) f) h_1) =
    CategoryTheory.CategoryStruct.comp t.unit h_1
-- Mathlib.Analysis.Convex.Intrinsic
intrinsicClosure_nonempty : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring 𝕜] [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
  [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] {s : Set P}, (intrinsicClosure 𝕜 s).Nonempty ↔ s.Nonempty
-- Mathlib.NumberTheory.ModularForms.QExpansion
ModularForm.qExpansion_mul : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} [inst : Γ.HasDetPlusMinusOne],
  0 < h →
    h ∈ Γ.strictPeriods →
      ∀ {a b : ℤ} (f : ModularForm Γ a) (g : ModularForm Γ b),
        UpperHalfPlane.qExpansion h ⇑(f.mul g) = UpperHalfPlane.qExpansion h ⇑f * UpperHalfPlane.qExpansion h ⇑g
-- Lean.Meta.Tactic.Ext
/-- The tree of `ext` extensions.  -/
Lean.Meta.Ext.ExtTheorems.tree : Lean.Meta.Ext.ExtTheorems → Lean.Meta.DiscrTree Lean.Meta.Ext.ExtTheorem
-- Std.Time.DateTime
/-- The timezone rules applied to this datetime.
 -/
Std.Time.DateTime.rules : Std.Time.DateTime → Std.Time.TimeZone.ZoneRules
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Connected.map : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {H : SimpleGraph V'} (f : G →g H),
  Function.Surjective ⇑f → G.Connected → H.Connected
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.instInhabitedMVarErrorKind : Inhabited Lean.Elab.Term.MVarErrorKind
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.orImpR.injEq : ∀ (p p_1 : Mathlib.Tactic.ITauto.Proof), (p.orImpR = p_1.orImpR) = (p = p_1)
-- Mathlib.Data.Set.MemPartition
memPartitionSet_of_mem : ∀ {α : Type u_1} {f : ℕ → Set α} {n : ℕ} {a : α} {s : Set α}, s ∈ memPartition f n → a ∈ s → memPartitionSet f n a = s
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.instElemOrbit.eq_1 : ∀ {M : Type u_1} {α : Type u_3} [inst : AddMonoid M] [inst_1 : AddAction M α] {a : α},
  AddAction.instElemOrbit =
    { vadd := fun m => Set.MapsTo.restrict (fun x => m +ᵥ x) (AddAction.orbit M a) (AddAction.orbit M a) ⋯,
      add_vadd := ⋯, zero_vadd := ⋯ }
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.ParenthesizerM : Type → Type
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.logMap_apply : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : NumberField.mixedEmbedding.mixedSpace K)
  (w : { w // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ }),
  NumberField.mixedEmbedding.logMap x w =
    ↑(↑w).mult *
      (Real.log ((NumberField.mixedEmbedding.normAtPlace ↑w) x) -
        Real.log (NumberField.mixedEmbedding.norm x) * (↑(Module.finrank ℚ K))⁻¹)
-- Mathlib.RingTheory.PowerBasis
PowerBasis.map_gen : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {S' : Type u_7}
  [inst_3 : CommRing S'] [inst_4 : Algebra R S'] (pb : PowerBasis R S) (e : S ≃ₐ[R] S'), (pb.map e).gen = e pb.gen
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Sphere.isDiameter_iff_right_mem_and_pointReflection_center_right : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p₁ p₂ : P},
  s.IsDiameter p₁ p₂ ↔ p₂ ∈ s ∧ (Equiv.pointReflection s.center) p₂ = p₁
-- Mathlib.GroupTheory.Perm.Centralizer
Equiv.Perm.Basis.ofPermHomFun_apply_of_mem_fixedPoints : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {g : Equiv.Perm α} (a : g.Basis)
  (τ : ↥(Equiv.Perm.OnCycleFactors.range_toPermHom' g)) {x : α}, x ∈ Function.fixedPoints ⇑g → a.ofPermHomFun τ x = x
-- Init.Data.SInt.Bitwise
Int8.ne_not_self : ∀ {a : Int8}, a ≠ ~~~a
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.fundCircuit_restrict_univ : ∀ {α : Type u_1} {I : Set α} {e : α} (M : Matroid α), (M.restrict Set.univ).fundCircuit e I = M.fundCircuit e I
-- Mathlib.Algebra.Polynomial.RingDivision
/-- A degree 1 polynomial `C a * X + C b` is irreducible
if `a, b` are relatively prime.  -/
Polynomial.irreducible_of_degree_eq_one_of_isRelPrime_coeff : ∀ {R : Type u} [inst : CommRing R] [IsDomain R] {p : Polynomial R},
  p.degree = 1 → IsRelPrime (p.coeff 0) (p.coeff 1) → Irreducible p
-- Mathlib.Data.Finmap
Multiset.keys_singleton : ∀ {α : Type u} {β : α → Type v} {a : α} {b : β a}, {⟨a, b⟩}.keys = {a}
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.mul'.eq_1 : ∀ (k k_1 : ℤ), (Int.Internal.Linear.Poly.num k_1).mul' k = Int.Internal.Linear.Poly.num (k * k_1)
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Array
Array.toList_iterM : ∀ {m : Type w → Type w'} [inst : Monad m] {β : Type w} [LawfulMonad m] {array : Array β},
  (array.iterM m).toList = pure array.toList
-- Init.Data.Vector.Lemmas
Vector.map_replicate : ∀ {n : ℕ} {α : Type u_1} {a : α} {α_1 : Type u_2} {f : α → α_1},
  Vector.map f (Vector.replicate n a) = Vector.replicate n (f a)
-- Mathlib.Tactic.Algebra.Lemmas
Mathlib.Tactic.Algebra.add_eq_of_zero_add : ∀ {A : Type u_2} [sA : CommSemiring A] {a₁ a₂ b₁ b₂ : A}, a₁ = 0 → a₂ = b₁ + b₂ → a₁ + a₂ = b₁ + b₂
-- Mathlib.CategoryTheory.Presentable.ColimitPresentation
CategoryTheory.Limits.ColimitPresentation.comp_base : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u_1} {I : J → Type u_2}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] [inst_2 : (j : J) → CategoryTheory.Category.{u_3, u_2} (I j)]
  {D : CategoryTheory.Functor J C} {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)}
  {X Y Z : CategoryTheory.Limits.ColimitPresentation.Total P} (f : X.Hom Y) (g : Y.Hom Z),
  (CategoryTheory.CategoryStruct.comp f g).base = CategoryTheory.CategoryStruct.comp f.base g.base
-- Mathlib.Data.Finset.Image
Finset.map_inter : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst_1 : DecidableEq β] {f : α ↪ β} (s₁ s₂ : Finset α),
  Finset.map f (s₁ ∩ s₂) = Finset.map f s₁ ∩ Finset.map f s₂
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.AddGrpObj.sub_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G H X : C} [inst_2 : CategoryTheory.AddGrpObj G] [inst_3 : CategoryTheory.AddGrpObj H] (f g : X ⟶ G) (h : G ⟶ H)
  [CategoryTheory.IsAddMonHom h],
  CategoryTheory.CategoryStruct.comp (f - g) h =
    CategoryTheory.CategoryStruct.comp f h - CategoryTheory.CategoryStruct.comp g h
-- Mathlib.Topology.Algebra.UniformRing
/-- Given a topological ring `α` equipped with a uniform structure that makes subtraction uniformly
continuous, get a homeomorphism between the separated quotient of `α` and the quotient ring
corresponding to the closure of zero.  -/
UniformSpace.sepQuotHomeomorphRingQuot : (α : Type u_2) →
  [inst : Ring α] →
    [inst_1 : TopologicalSpace α] → [inst_2 : IsTopologicalRing α] → SeparationQuotient α ≃ₜ α ⧸ ⊥.closure
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.isRed.match_1.eq_2 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (x : RBTree.RBNode α)
  (h_1 :
    (c : RBTree.RBColor) →
      (l : RBTree.RBNode α) → (v : α) → (r : RBTree.RBNode α) → motive (RBTree.RBNode.node c l v r))
  (h_2 : (x : RBTree.RBNode α) → motive x),
  (∀ (c : RBTree.RBColor) (l : RBTree.RBNode α) (v : α) (r : RBTree.RBNode α), x = RBTree.RBNode.node c l v r → False) →
    (match x with
      | RBTree.RBNode.node c l v r => h_1 c l v r
      | x => h_2 x) =
      h_2 x
-- Aesop.Stats.Basic
/-- Number of failed applications of a rule.
 -/
Aesop.RuleStatsTotals.numFailed : Aesop.RuleStatsTotals → ℕ
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.inverseImage_trW_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {D : Type u_2} [inst_6 : CategoryTheory.Category.{v_2, u_2} D] [inst_7 : CategoryTheory.Preadditive D]
  [inst_8 : CategoryTheory.Limits.HasZeroObject D] [inst_9 : CategoryTheory.HasShift D ℤ]
  [inst_10 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [inst_11 : CategoryTheory.Pretriangulated D]
  (P : CategoryTheory.ObjectProperty C) (F : CategoryTheory.Functor D C) [inst_12 : F.CommShift ℤ] [F.IsTriangulated]
  [P.IsClosedUnderIsomorphisms] {X Y : D} (s : X ⟶ Y), (P.inverseImage F).trW s ↔ P.trW (F.map s)
-- Batteries.Data.Fin.Coding
Fin.decodeChar_encodeChar : ∀ (x : Char), Fin.decodeChar (Fin.encodeChar x) = x
-- Lean.Server.Rpc.RequestHandling
Lean.Server.instInhabitedRpcProcedure : Inhabited Lean.Server.RpcProcedure
-- Mathlib.Topology.Algebra.Ring.Basic
IsSemitopologicalRing.toIsTopologicalAddGroup : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] [inst_1 : TopologicalSpace R] [IsSemitopologicalRing R],
  IsTopologicalAddGroup R
-- Mathlib.Topology.PartialHomeomorph.Defs
Homeomorph.toPartialHomeomorphOfImageEq_apply : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : X ≃ₜ Y) (s : Set X)
  (t : Set Y) (h : ⇑e '' s = t), ↑(e.toPartialHomeomorphOfImageEq s t h) = ⇑e
-- Mathlib.LinearAlgebra.SymplecticGroup
SymplecticGroup.fromBlocks_mem_iff : ∀ {l : Type u_1} {R : Type u_2} [inst : DecidableEq l] [inst_1 : Fintype l] [inst_2 : CommRing R]
  {A B C D : Matrix l l R},
  Matrix.fromBlocks A B C D ∈ Matrix.symplecticGroup l R ↔
    A.transpose * C = C.transpose * A ∧ B.transpose * D = D.transpose * B ∧ A.transpose * D - C.transpose * B = 1
-- Mathlib.Analysis.BoxIntegral.Box.Basic
/-- coordinates of the lower and upper corners of the box  -/
BoxIntegral.Box.lower : {ι : Type u_2} → BoxIntegral.Box ι → ι → ℝ
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.homEquiv_symm_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (X : C) (Y : D) (g : X ⟶ G.obj Y),
  (adj.homEquiv X Y).symm g = CategoryTheory.CategoryStruct.comp (F.map g) (adj.counit.app Y)
-- Mathlib.Topology.Algebra.Monoid
ContinuousMul.induced : ∀ {α : Type u_6} {β : Type u_7} {F : Type u_8} [inst : FunLike F α β] [inst_1 : Mul α] [inst_2 : Mul β]
  [MulHomClass F α β] [tβ : TopologicalSpace β] [ContinuousMul β] (f : F), ContinuousMul α
-- Mathlib.CategoryTheory.Functor.CurryingThree
CategoryTheory.Functor.instFaithfulProdUncurry₃ : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_4} C₃]
  [inst_3 : CategoryTheory.Category.{v_9, u_9} E], CategoryTheory.Functor.uncurry₃.Faithful
-- Mathlib.CategoryTheory.Localization.SmallHom
CategoryTheory.LocalizerMorphism.smallHomMap'.eq_1 : ∀ {C₁ : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C₁] {W₁ : CategoryTheory.MorphismProperty C₁} {C₂ : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₂ : CategoryTheory.MorphismProperty C₂}
  (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) {X Y : C₁}
  [inst_2 : CategoryTheory.Localization.HasSmallLocalizedHom W₁ X Y] {X' Y' : C₂}
  [inst_3 : CategoryTheory.Localization.HasSmallLocalizedHom W₂ X' X']
  [inst_4 : CategoryTheory.Localization.HasSmallLocalizedHom W₂ X' Y']
  [inst_5 : CategoryTheory.Localization.HasSmallLocalizedHom W₂ Y' Y'] (eX : Φ.functor.obj X ≅ X')
  (eY : Φ.functor.obj Y ≅ Y') (f : CategoryTheory.Localization.SmallHom W₁ X Y),
  Φ.smallHomMap' eX eY f =
    (CategoryTheory.Localization.SmallHom.mk W₂ eX.inv).comp
      ((Φ.smallHomMap f).comp (CategoryTheory.Localization.SmallHom.mk W₂ eY.hom))
-- Mathlib.Analysis.SpecialFunctions.PolarCoord
Complex.integral_comp_pi_polarCoord_symm : ∀ {ι : Type u_1} [inst : Fintype ι] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  (f : (ι → ℂ) → E),
  (∫ (p : ι → ℝ × ℝ) in Set.univ.pi fun x => Complex.polarCoord.target,
      (∏ i, (p i).1) • f fun i => ↑Complex.polarCoord.symm (p i)) =
    ∫ (p : ι → ℂ), f p
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.intercalateTR.eq_1 : ∀ {α : Type u_1} (sep : List α), sep.intercalateTR [] = []
-- Lean.Data.Iterators.Producers.PersistentHashMap
_private.Lean.Data.Iterators.Producers.PersistentHashMap.0.Lean.PersistentHashMap.Node.measure.match_1.eq_3 : ∀ {α : Type u_1} {β : Type u_2} (motive : Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β) → Sort u_3)
  (node : Lean.PersistentHashMap.Node α β)
  (h_1 :
    Lean.PersistentHashMap.Entry.ref node = Lean.PersistentHashMap.Entry.null →
      motive Lean.PersistentHashMap.Entry.null)
  (h_2 :
    (key : α) →
      (val : β) →
        Lean.PersistentHashMap.Entry.ref node = Lean.PersistentHashMap.Entry.entry key val →
          motive (Lean.PersistentHashMap.Entry.entry key val))
  (h_3 :
    (node_1 : Lean.PersistentHashMap.Node α β) →
      Lean.PersistentHashMap.Entry.ref node = Lean.PersistentHashMap.Entry.ref node_1 →
        motive (Lean.PersistentHashMap.Entry.ref node_1)),
  (match h_eq : Lean.PersistentHashMap.Entry.ref node with
    | Lean.PersistentHashMap.Entry.null => h_1 h_eq
    | Lean.PersistentHashMap.Entry.entry key val => h_2 key val h_eq
    | Lean.PersistentHashMap.Entry.ref node_1 => h_3 node_1 h_eq) =
    h_3 node ⋯
-- Mathlib.Geometry.Euclidean.Sphere.Basic
/-- center of this sphere  -/
EuclideanGeometry.Sphere.center : {P : Type u_2} → [inst : MetricSpace P] → EuclideanGeometry.Sphere P → P
-- Mathlib.Analysis.Normed.Group.InfiniteSum
Summable.of_norm : ∀ {ι : Type u_1} {E : Type u_3} [inst : SeminormedAddCommGroup E] [CompleteSpace E] {f : ι → E},
  (Summable fun a => ‖f a‖) → Summable f
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.eval_un : ∀ {assign : Std.Tactic.BVDecide.BVExpr.Assignment} {op : Std.Tactic.BVDecide.BVUnOp} {a : ℕ}
  {operand : Std.Tactic.BVDecide.BVExpr a},
  Std.Tactic.BVDecide.BVExpr.eval assign (Std.Tactic.BVDecide.BVExpr.un op operand) =
    op.eval (Std.Tactic.BVDecide.BVExpr.eval assign operand)
-- Mathlib.Order.Monotone.Monovary
Antivary.dual_right : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β},
  Antivary f g → Monovary f (⇑OrderDual.toDual ∘ g)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey?_diff_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₁ → (t₁ \ t₂).getKey? k = none
-- Mathlib.Data.Fintype.Sets
Set.subset_toFinset : ∀ {α : Type u_1} {t : Set α} {s : Finset α} [inst : Fintype ↑t], s ⊆ t.toFinset ↔ ↑s ⊆ t
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.IsDynCoverOf.coverMincard_le_card : ∀ {X : Type u_1} {T : X → X} {U : SetRel X X} {F : Set X} {n : ℕ} {s : Finset X},
  Dynamics.IsDynCoverOf T F U n ↑s → Dynamics.coverMincard T F U n ≤ ↑s.card