mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.Embedding.TruncLE
/-- The isomorphism `(K.truncLE e).X i' ≅ K.cycles i'` when `e.f i = i'`
and `e.BoundaryLE i` holds.  -/
HomologicalComplex.truncLEXIsoCycles : {ι : 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.HasZeroMorphisms C] →
              (K : HomologicalComplex C c') →
                (e : c.Embedding c') →
                  [inst_2 : e.IsTruncLE] →
                    [inst_3 : ∀ (i' : ι'), K.HasHomology i'] →
                      [inst_4 : CategoryTheory.Limits.HasZeroObject C] →
                        {i : ι} → {i' : ι'} → e.f i = i' → e.BoundaryLE i → ((K.truncLE e).X i' ≅ K.cycles i')
-- Mathlib.AlgebraicGeometry.Group.Affine
/-- The essential image of `R`-bialgebras under `Spec` is precisely affine monoid schemes over
`Spec R`.  -/
AlgebraicGeometry.essImage_bialgSpec : ∀ {R : CommRingCat} {G : CategoryTheory.Mon (CategoryTheory.Over (AlgebraicGeometry.Spec R))},
  (AlgebraicGeometry.bialgSpec R).essImage G ↔ AlgebraicGeometry.IsAffine G.X.left
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.val_top : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {L : BooleanSubalgebra α}, ↑⊤ = ⊤
-- Mathlib.Combinatorics.SimpleGraph.Diam
/-- A finite and nontrivial graph is connected if and only if its diameter is not zero.
See also `connected_iff_ediam_ne_top` for the extended diameter version.  -/
SimpleGraph.connected_iff_diam_ne_zero : ∀ {α : Type u_1} {G : SimpleGraph α} [Finite α] [Nontrivial α], G.Connected ↔ G.diam ≠ 0
-- Mathlib.Data.Finsupp.NeLocus
Finsupp.zipWith_neLocus_eq_right : ∀ {α : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : DecidableEq α] [inst_1 : DecidableEq M]
  [inst_2 : Zero M] [inst_3 : DecidableEq P] [inst_4 : Zero P] [inst_5 : Zero N] {F : M → N → P} (F0 : F 0 0 = 0)
  (f₁ f₂ : α →₀ M) (g : α →₀ N),
  (∀ (g : N), Function.Injective fun f => F f g) →
    (Finsupp.zipWith F F0 f₁ g).neLocus (Finsupp.zipWith F F0 f₂ g) = f₁.neLocus f₂
-- Mathlib.LinearAlgebra.CliffordAlgebra.Grading
CliffordAlgebra.evenOdd_mul_le : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (i j : ZMod 2),
  CliffordAlgebra.evenOdd Q i * CliffordAlgebra.evenOdd Q j ≤ CliffordAlgebra.evenOdd Q (i + j)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
CategoryTheory.IsPullback.inr_fst' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {b : CategoryTheory.Limits.BinaryBicone X Y}
  (h : b.IsBilimit), CategoryTheory.IsPullback b.inr 0 b.fst 0
-- Mathlib.Util.SynthesizeUsing
/-- `synthesizeUsing type tac` synthesizes an element of type `type` using tactic `tac`.

The tactic `tac` is allowed to leave goals open, and these remain as metavariables in the
returned expression.
 -/
synthesizeUsing : {u : Lean.Level} → (type : Q(Sort u)) → Lean.Elab.Tactic.TacticM Unit → Lean.MetaM (List Lean.MVarId × Q(«$type»))
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
/-- See Note [custom simps projection]  -/
OpenPartialHomeomorph.Simps.symm_apply : {X : Type u_1} →
  {Y : Type u_3} → [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → OpenPartialHomeomorph X Y → Y → X
-- Mathlib.Algebra.Group.Submonoid.Support
Submonoid.IsMulPointed.eq_one_of_mem_of_inv_mem : ∀ {G : Type u_1} [inst : Group G] {M : Submonoid G}, M.IsMulPointed → ∀ {x : G}, x ∈ M → x⁻¹ ∈ M → x = 1
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.TheoremGuard.check : Lean.Meta.Grind.TheoremGuard → Bool
-- Init.Data.SInt.Bitwise
Int32.toInt16_xor : ∀ (a b : Int32), (a ^^^ b).toInt16 = a.toInt16 ^^^ b.toInt16
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.of_keysArray_unit_perm : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α (fun x => Unit) cmp},
  t₁.keysArray.Perm t₂.keysArray → t₁.Equiv t₂
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.trans_transEquiv : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : PartialEquiv α β) (e' : PartialEquiv β γ)
  (f'' : γ ≃ δ), (e.trans e').transEquiv f'' = e.trans (e'.transEquiv f'')
-- Mathlib.FieldTheory.Galois.GaloisClosure
FiniteGaloisIntermediateField.instIsSeparableSubtypeMemIntermediateFieldMin : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K]
  (L₁ L₂ : IntermediateField k K) [Algebra.IsSeparable k ↥L₁], Algebra.IsSeparable k ↥(L₁ ⊓ L₂)
-- Mathlib.AlgebraicGeometry.FunctionField
AlgebraicGeometry.germ_injective_of_isIntegral : ∀ (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] {U : X.Opens} (x : ↥X) (hx : x ∈ U),
  Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U x hx))
-- Mathlib.Data.Set.Lattice.Image
Set.prod_eq_biUnion_left : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β}, s ×ˢ t = ⋃ a ∈ s, (fun b => (a, b)) '' t
-- Mathlib.LinearAlgebra.PiTensorProduct.Dual
PiTensorProduct.dualDistribEquiv.eq_1 : ∀ {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} [inst : CommRing R] [inst_1 : (i : ι) → AddCommGroup (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [inst_3 : ∀ (i : ι), Module.Finite R (M i)]
  [inst_4 : ∀ (i : ι), Module.Free R (M i)] [inst_5 : Finite ι],
  PiTensorProduct.dualDistribEquiv = PiTensorProduct.dualDistribEquivOfBasis fun i => Module.Free.chooseBasis R (M i)
-- Mathlib.Algebra.Group.End
Equiv.permCongrHom_coe : ∀ {α : Type u_4} {β : Type u_5} (e : α ≃ β), ⇑e.permCongrHom = ⇑e.permCongr
-- Mathlib.Data.Nat.Factors
Nat.primeFactorsList_one : Nat.primeFactorsList 1 = []
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.instAdd : {R : Type u_2} →
  {M : Type u_4} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] → [inst_2 : AddCommMonoid M] → [inst_3 : Module R M] → Add (ConvexCone R M)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.nat_card_stabilizer_eq_one_or_two : ∀ (k : Type u_1) [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K]
  (w : NumberField.InfinitePlace K),
  Nat.card ↥(MulAction.stabilizer Gal(K/k) w) = 1 ∨ Nat.card ↥(MulAction.stabilizer Gal(K/k) w) = 2
-- Mathlib.Topology.MetricSpace.Pseudo.Basic
/-- **Alias** of `finite_cover_balls_of_compact`.

---

Any compact set in a pseudometric space can be covered by finitely many balls of a given
positive radius  -/
IsCompact.finite_cover_balls : ∀ {X : Type u_2} [inst : PseudoMetricSpace X] {s : Set X},
  IsCompact s → ∀ {e : ℝ}, 0 < e → ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ x ∈ t, Metric.ball x e
-- Mathlib.Combinatorics.SimpleGraph.DeleteEdges
SimpleGraph.deleteEdges_sup : ∀ {V : Type u_1} (G H : SimpleGraph V) (s : Set (Sym2 V)), (G ⊔ H).deleteEdges s = G.deleteEdges s ⊔ H.deleteEdges s
-- Mathlib.LinearAlgebra.BilinearForm.Orthogonal
/-- Given a bilinear form `B` and some `x` such that `B x x ≠ 0`, the span of the singleton of `x`
is complement to its orthogonal complement.  -/
LinearMap.BilinForm.isCompl_span_singleton_orthogonal : ∀ {V : Type u_5} {K : Type u_6} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {B : LinearMap.BilinForm K V} {x : V}, (B x) x ≠ 0 → IsCompl (K ∙ x) (B.orthogonal (K ∙ x))
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Expr.toNormPoly.eq_1 : ∀ (e : Nat.Internal.Linear.Expr), e.toNormPoly = e.toPoly.norm
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
MonCat.FilteredColimits.colimitCocone.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCat)
  [inst_1 : CategoryTheory.IsFiltered J],
  MonCat.FilteredColimits.colimitCocone F =
    { pt := MonCat.FilteredColimits.colimit F,
      ι := { app := MonCat.FilteredColimits.coconeMorphism F, naturality := ⋯ } }
-- Mathlib.Geometry.Euclidean.Inversion.Calculus
Differentiable.inversion : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : InnerProductSpace ℝ F] {c x : E → F} {R : E → ℝ},
  Differentiable ℝ c →
    Differentiable ℝ R →
      Differentiable ℝ x →
        (∀ (a : E), x a ≠ c a) → Differentiable ℝ fun a => EuclideanGeometry.inversion (c a) (R a) (x a)
-- Init.Data.Nat.Lemmas
_private.Init.Data.Nat.Lemmas.0.Nat.anyLTTR_loop_eq_true : ∀ {n : ℕ} {f : (i : ℕ) → i < n → Bool} (j : ℕ) (hj : j ≤ n),
  Nat.anyLTTR.loop✝ n f j hj = true ↔ ∃ i, ∃ (h : i < n), n - j ≤ i ∧ f i h = true
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
/-- The derivative of Weierstrass `℘` function with the `l₀`-term missing.
This is mainly a tool for calculations where one would want to omit a diverging term.
This has the notation `℘'[L - l₀]` in the namespace `PeriodPairs`.  -/
PeriodPair.«term℘'[_-_]» : Lean.ParserDescr
-- Std.Do.PredTrans
/-- The identity predicate transformer that transforms the postcondition's assertion about the return
value into an assertion about `a`.
 -/
Std.Do.PredTrans.pure : {ps : Std.Do.PostShape} → {α : Type u} → α → Std.Do.PredTrans ps α
-- Mathlib.CategoryTheory.Countable
CategoryTheory.CountableCategory.instCountableHomAsType : ∀ (α : Type u) [inst : CategoryTheory.Category.{v, u} α] [inst_1 : CategoryTheory.CountableCategory α],
  Countable (CategoryTheory.CountableCategory.HomAsType α)
-- Mathlib.Order.LiminfLimsup
Filter.Tendsto.limsup_comp_le_limsup : ∀ {ι : Type u_6} {α : Type u_7} {β : Type u_8} [inst : ConditionallyCompleteLattice β] {v : ι → α} {u : α → β}
  {f : Filter ι} {g : Filter α},
  Filter.Tendsto v f g →
    autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) (Filter.map v f) u)
        Filter.Tendsto.limsup_comp_le_limsup._auto_1 →
      autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) g u) Filter.Tendsto.limsup_comp_le_limsup._auto_3 →
        Filter.limsup (u ∘ v) f ≤ Filter.limsup u g
-- Mathlib.LinearAlgebra.BilinearForm.TensorProduct
/-- A tensor product of symmetric bilinear forms is symmetric.  -/
LinearMap.IsSymm.tmul : ∀ {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M₁] [inst_3 : AddCommMonoid M₂] [inst_4 : Algebra R A] [inst_5 : Module R M₁]
  [inst_6 : Module A M₁] [inst_7 : SMulCommClass R A M₁] [inst_8 : IsScalarTower R A M₁] [inst_9 : Module R M₂]
  {B₁ : LinearMap.BilinForm A M₁} {B₂ : LinearMap.BilinForm R M₂},
  LinearMap.IsSymm B₁ → LinearMap.IsSymm B₂ → LinearMap.IsSymm (B₁.tmul B₂)
-- Mathlib.Data.Num.Lemmas
SNum.le : LE SNum
-- Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
AlgebraicGeometry.HasAffineProperty.affineAnd_le_affineAnd : ∀ {Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
  {P P' : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme},
  AlgebraicGeometry.HasAffineProperty P (AlgebraicGeometry.affineAnd fun {R S} [CommRing R] [CommRing S] => Q) →
    AlgebraicGeometry.HasAffineProperty P' (AlgebraicGeometry.affineAnd fun {R S} [CommRing R] [CommRing S] => Q') →
      (∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, Q f → Q' f) → P ≤ P'
-- Mathlib.Order.BooleanAlgebra.Basic
disjoint_compl_left_iff : ∀ {α : Type u} {x y : α} [inst : BooleanAlgebra α], Disjoint xᶜ y ↔ y ≤ x
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.mergeWith : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ t₃ t₄ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp],
  t₁.WF →
    t₂.WF →
      t₃.WF →
        t₄.WF →
          ∀ (f : α → β → β → β),
            t₁.Equiv t₂ → t₃.Equiv t₄ → (Std.TreeMap.Raw.mergeWith f t₁ t₃).Equiv (Std.TreeMap.Raw.mergeWith f t₂ t₄)
-- Mathlib.Tactic.TFAE
Mathlib.Tactic.TFAE.Parser.tfaeHaveDecl.formatter : Lean.PrettyPrinter.Formatter
-- Lean.Meta.Tactic.Grind.Anchor
Lean.Meta.Grind.ExprWithAnchor.anchor : Lean.Meta.Grind.ExprWithAnchor → UInt64
-- Mathlib.CategoryTheory.Preadditive.Opposite
/-- `G ⟶ G` and `(End G)ᵐᵒᵖ` are isomorphic as `(End G)ᵐᵒᵖ`-modules.  -/
CategoryTheory.Preadditive.homSelfLinearEquivEndMulOpposite : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] → (G : C) → (G ⟶ G) ≃ₗ[(CategoryTheory.End G)ᵐᵒᵖ] (CategoryTheory.End G)ᵐᵒᵖ
-- Mathlib.Topology.ContinuousMap.Compact
BoundedContinuousFunction.dist_toContinuousMap : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : CompactSpace α] [inst_2 : PseudoMetricSpace β]
  (f g : BoundedContinuousFunction α β), dist f.toContinuousMap g.toContinuousMap = dist f g
-- Mathlib.MeasureTheory.Covering.Besicovitch
Besicovitch.TauPackage.mk : {β : Type u_1} → {α : Type u_2} → Besicovitch.BallPackage β α → (τ : ℝ) → 1 < τ → Besicovitch.TauPackage β α
-- Mathlib.Algebra.Homology.Embedding.TruncLEHomology
/-- The cokernel sequence of the monomorphism `K.ιTruncLE e`.  -/
HomologicalComplex.shortComplexTruncLE : {ι : 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.Abelian C] →
              HomologicalComplex C c' →
                (e : c.Embedding c') → [e.IsTruncLE] → CategoryTheory.ShortComplex (HomologicalComplex C c')
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.smul_stabilizer_of_no_doubling_aux : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {A : Finset G} {a : G},
  (A * A).card ≤ A.card →
    a ∈ A → a • ↑(MulAction.stabilizer G A) = ↑A ∧ MulOpposite.op a • ↑(MulAction.stabilizer G A) = ↑A
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
/-- See note [comp_of_eq lemmas]  -/
ContMDiffWithinAt.comp_of_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_7 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7}
  [inst_8 : TopologicalSpace M'] {E'' : Type u_8} [inst_9 : NormedAddCommGroup E''] [inst_10 : NormedSpace 𝕜 E'']
  {H'' : Type u_9} [inst_11 : TopologicalSpace H''] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10}
  [inst_12 : TopologicalSpace M''] [inst_13 : ChartedSpace H M] [inst_14 : ChartedSpace H' M']
  [inst_15 : ChartedSpace H'' M''] {f : M → M'} {s : Set M} {n : WithTop ℕ∞} {t : Set M'} {g : M' → M''} {x : M}
  {y : M'},
  ContMDiffWithinAt I' I'' n g t y →
    ContMDiffWithinAt I I' n f s x → Set.MapsTo f s t → f x = y → ContMDiffWithinAt I I'' n (g ∘ f) s x
-- Mathlib.Algebra.Homology.ExactSequence
CategoryTheory.ComposableArrows.exact_iff_δlast : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {n : ℕ} (S : CategoryTheory.ComposableArrows C (n + 2)),
  S.Exact ↔
    S.δlast.Exact ∧ (CategoryTheory.ComposableArrows.mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact
-- Mathlib.RingTheory.WittVector.IsPoly
/-- The composition of polynomial functions is polynomial.  -/
WittVector.IsPoly.comp : ∀ {p : ℕ} {g f : ⦃R : Type u_2⦄ → [CommRing R] → WittVector p R → WittVector p R} [hg : WittVector.IsPoly p g]
  [hf : WittVector.IsPoly p f], WittVector.IsPoly p fun R _Rcr => g ∘ f
-- Mathlib.MeasureTheory.Integral.MeanInequalities
/-- Variant of Minkowski's inequality for functions `α → ℝ≥0∞` in `ℒp` with `p ≤ 1`: the `ℒp`
seminorm of the sum of two functions is bounded by a constant multiple of the sum
of their `ℒp` seminorms.  -/
ENNReal.lintegral_Lp_add_le_of_le_one : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : ℝ} {f g : α → ENNReal},
  AEMeasurable f μ →
    0 ≤ p →
      p ≤ 1 →
        (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤
          2 ^ (1 / p - 1) * ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))
-- Mathlib.Algebra.Order.Star.Basic
/-- A star projection `p` is less than or equal to a star projection `q` when `p * q = p`.  -/
IsStarProjection.le_of_mul_eq_left : ∀ {R : Type u_1} [inst : NonUnitalRing R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R] {p q : R},
  IsStarProjection p → IsStarProjection q → p * q = p → p ≤ q
-- Mathlib.Order.Antichain
IsStrongAntichain.isAntichain : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} [Std.Refl r], IsStrongAntichain r s → IsAntichain r s
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
contMDiffAt_subtype_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_7 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7}
  [inst_8 : TopologicalSpace M'] [inst_9 : ChartedSpace H M] [inst_10 : ChartedSpace H' M'] {n : WithTop ℕ∞}
  {U : TopologicalSpace.Opens M} {f : M → M'} {x : ↥U}, ContMDiffAt I I' n (fun x => f ↑x) x ↔ ContMDiffAt I I' n f ↑x
-- LeanSearchClient.Syntax
LeanSearchClient.SearchServer.searchTermSuggestions : LeanSearchClient.SearchServer → Lean.Syntax → Lean.TSyntax `str → Lean.Elab.TermElabM Unit
-- Std.Data.DTreeMap.Internal.Balanced
Std.DTreeMap.Internal.Impl.Balanced.below.leaf : ∀ {α : Type u} {β : α → Type v} {motive : (a : Std.DTreeMap.Internal.Impl α β) → a.Balanced → Prop},
  Std.DTreeMap.Internal.Impl.Balanced.below ⋯
-- Init.Data.BitVec.Lemmas
/-- Negating `x` and then extracting [lo:hi] is the same as extracting and then negating.
For the extraction to be well-behaved,
we need the range [lo:hi] to be a valid closed interval inside the bitvector:
1. `lo ≤ hi` for the interval to be a well-formed closed interval.
2. `hi < w`, for the interval to be contained inside the bitvector.
 -/
BitVec.extractLsb_not_of_lt : ∀ {w : ℕ} {x : BitVec w} {hi lo : ℕ}, lo ≤ hi → hi < w → BitVec.extractLsb hi lo (~~~x) = ~~~BitVec.extractLsb hi lo x
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.mkInductiveDeclCore : {α : Type} →
  (Lean.Elab.Command.AddAndFinalizeContext✝ → Lean.Elab.TermElabM α) →
    Array Lean.Expr →
      Array Lean.Elab.Command.InductiveElabStep1 →
        Array Lean.Elab.Command.PreElabHeaderResult → List Lean.Name → Lean.Elab.TermElabM α
-- Mathlib.Topology.Order.LowerUpperTopology
/-- `toUpper` is the identity function to the `WithUpper` of a type.  -/
Topology.WithUpper.toUpper : {α : Type u_1} → α ≃ Topology.WithUpper α
-- Mathlib.NumberTheory.Padics.Measure.Basic
AbstractMeasure.congr_simp : ∀ (X : Type u_1) (R : Type u_3) (E : Type u_4) [inst : TopologicalSpace X] [inst_1 : AddCommGroup E]
  [inst_2 : TopologicalSpace E] [inst_3 : CommRing R] [inst_4 : TopologicalSpace R] [inst_5 : IsTopologicalRing R]
  [inst_6 : Module R E], AbstractMeasure X R E = AbstractMeasure X R E
-- Mathlib.Algebra.Category.Grp.Basic
/-- The (bundled) group of automorphisms of a type is isomorphic to the (bundled) group
of permutations.  -/
CategoryTheory.Aut.isoPerm : {α : Type u} → GrpCat.of (CategoryTheory.Aut α) ≅ GrpCat.of (Equiv.Perm α)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
tendsto_euler_sin_prod' : ∀ {x : ℂ},
  x ≠ 0 →
    Filter.Tendsto (fun n => ∏ i ∈ Finset.range n, (1 + sineTerm x i)) Filter.atTop
      (nhds (Complex.sin (↑Real.pi * x) / (↑Real.pi * x)))
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryPseudofunctor.mk.inj : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {toPseudofunctor : CategoryTheory.Pseudofunctor B C}
  {map_id :
    autoParam
      (∀ (X : B),
        toPseudofunctor.map (CategoryTheory.CategoryStruct.id X) =
          CategoryTheory.CategoryStruct.id (toPseudofunctor.obj X))
      CategoryTheory.StrictlyUnitaryPseudofunctor.map_id._autoParam}
  {mapId_eq_eqToIso :
    autoParam (∀ (X : B), toPseudofunctor.mapId X = CategoryTheory.eqToIso ⋯)
      CategoryTheory.StrictlyUnitaryPseudofunctor.mapId_eq_eqToIso._autoParam}
  {toPseudofunctor_1 : CategoryTheory.Pseudofunctor B C}
  {map_id_1 :
    autoParam
      (∀ (X : B),
        toPseudofunctor_1.map (CategoryTheory.CategoryStruct.id X) =
          CategoryTheory.CategoryStruct.id (toPseudofunctor_1.obj X))
      CategoryTheory.StrictlyUnitaryPseudofunctor.map_id._autoParam}
  {mapId_eq_eqToIso_1 :
    autoParam (∀ (X : B), toPseudofunctor_1.mapId X = CategoryTheory.eqToIso ⋯)
      CategoryTheory.StrictlyUnitaryPseudofunctor.mapId_eq_eqToIso._autoParam},
  { toPseudofunctor := toPseudofunctor, map_id := map_id, mapId_eq_eqToIso := mapId_eq_eqToIso } =
      { toPseudofunctor := toPseudofunctor_1, map_id := map_id_1, mapId_eq_eqToIso := mapId_eq_eqToIso_1 } →
    toPseudofunctor = toPseudofunctor_1
-- Lean.Elab.Tactic.Ext
/-- Apply a single extensionality theorem to `goal`.  -/
Lean.Elab.Tactic.Ext.applyExtTheoremAt : Lean.MVarId → Lean.MetaM (List Lean.MVarId)
-- Mathlib.FieldTheory.FinTrdeg
/-- A field extension L/K is said to have finite transcendence degree if there is some
intermediate extension L/E/K with E/K finitely generated and L/E algebraic.  -/
FinTrdeg : (K : Type u_1) → (L : Type u_2) → [inst : Field K] → [inst_1 : Field L] → [Algebra K L] → Prop
-- Aesop.Util.EqualUpToIds
/-- A map from metavariables which are unassigned in the left goal
to their corresponding expression in the right goal. Only used when
`allowAssignmentDiff = true`.  -/
Aesop.EqualUpToIdsM.State.leftUnassignedMVarValues : Aesop.EqualUpToIdsM.State → Std.HashMap Lean.MVarId Lean.Expr
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.transvection_mem_center_iff : ∀ {ι : Type u_1} {F : Type u_2} [inst : DecidableEq ι] [inst_1 : Fintype ι] [inst_2 : CommRing F] {i j : ι}
  (hij : i ≠ j) (b : F),
  Matrix.SpecialLinearGroup.transvection hij b ∈ Subgroup.center (Matrix.SpecialLinearGroup ι F) ↔ b = 0
-- Mathlib.CategoryTheory.Yoneda
/-- Transport `RepresentableBy` along an isomorphism of the object.  -/
CategoryTheory.Functor.RepresentableBy.ofIsoObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {F : CategoryTheory.Functor Cᵒᵖ (Type w)} → {X Y : C} → F.RepresentableBy X → (Y ≅ X) → F.RepresentableBy Y
-- Lean.Meta.Tactic.Grind.Types
/-- Mapping from pairs `(f, i)` to a list of arguments.
Each argument occurs as the `i`-th of an `f`-application.
We use this information to add splits/lookaheads for
triggering extensionality theorems and model-based theory combination.
See `addSplitCandidatesForExt`.
 -/
Lean.Meta.Grind.Split.State.argsAt : Lean.Meta.Grind.Split.State → Lean.PHashMap (Lean.Expr × ℕ) (List Lean.Meta.Grind.SplitArg)
-- Mathlib.Probability.Distributions.Gamma
ProbabilityTheory.gammaMeasure.eq_1 : ∀ (a r : ℝ), ProbabilityTheory.gammaMeasure a r = MeasureTheory.volume.withDensity (ProbabilityTheory.gammaPDF a r)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.Stmt.halt.sizeOf_spec : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [inst : SizeOf Γ] [inst_1 : SizeOf Λ] [inst_2 : SizeOf σ],
  sizeOf Turing.TM1.Stmt.halt = 1
-- Mathlib.Probability.Process.Adapted
/-- **Alias** of `MeasureTheory.IsStronglyProgressive.finsetSum`. -/
MeasureTheory.ProgMeasurable.finset_sum : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} [inst_1 : TopologicalSpace β] [inst_2 : MeasurableSpace ι] {γ : Type u_4} [inst_3 : AddCommMonoid β]
  [ContinuousAdd β] {U : γ → ι → Ω → β} {s : Finset γ},
  (∀ c ∈ s, MeasureTheory.IsStronglyProgressive f (U c)) →
    MeasureTheory.IsStronglyProgressive f fun i a => ∑ c ∈ s, U c i a
-- Batteries.Data.UInt
UInt8.le_iff_toNat_le_toNat : ∀ {x y : UInt8}, x ≤ y ↔ x.toNat ≤ y.toNat
-- Lean.Data.KVMap
Lean.KVMap.setSyntax : Lean.KVMap → Lean.Name → Lean.Syntax → Lean.KVMap