mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
CategoryTheory.Functor.mapPresheaf_obj_X : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D)
  (X : AlgebraicGeometry.PresheafedSpace C), ↑(F.mapPresheaf.obj X) = ↑X
-- Lean.Attributes
Lean.ensureAttrDeclIsPublic : Lean.Name → Lean.Name → Lean.AttributeKind → Lean.AttrM Unit
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
NumberField.FinitePlace.equivHeightOneSpectrum_symm_apply : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (x : K),
  (NumberField.FinitePlace.equivHeightOneSpectrum.symm v) x = ‖(NumberField.FinitePlace.embedding v) x‖
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.matchAt?_eq_some_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice}
  {startPos endPos : s.Pos},
  String.Slice.Pattern.Model.matchAt? pat startPos = some endPos ↔
    String.Slice.Pattern.Model.IsLongestMatchAt pat startPos endPos
-- Init.Data.List.Zip
List.zip_eq_nil_iff : ∀ {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List β}, l₁.zip l₂ = [] ↔ l₁ = [] ∨ l₂ = []
-- Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
IntermediateField.isTotallyReal_bot : ∀ (K : Type u_2) [inst : Field K] [inst_1 : CharZero K], NumberField.IsTotallyReal ↥⊥
-- Mathlib.Order.Filter.Pointwise
Filter.coe_pureMulHom : ∀ {α : Type u_2} [inst : Mul α], ⇑Filter.pureMulHom = pure
-- Mathlib.Algebra.Category.CommBialgCat
CommBialgCat.hom_ext_iff : ∀ {R : Type u} [inst : CommRing R] {A B : CommBialgCat R} {f g : A ⟶ B},
  f = g ↔ CommBialgCat.Hom.hom f = CommBialgCat.Hom.hom g
-- Mathlib.Topology.Convenient.Category
/-- The unit isomorphism of the equivalence `ContinuousGeneratedByCat.equivalence`.  -/
ContinuousGeneratedByCat.equivalenceUnitIso : {ι : Type t} →
  {X : ι → Type u} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      CategoryTheory.Functor.id (GeneratedByTopCat X) ≅
        ContinuousGeneratedByCat.fromGeneratedByTopCat.comp ContinuousGeneratedByCat.toGeneratedByTopCat
-- Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
SchwartzMap.integral_norm_sq_fourier : ∀ {V : Type u_3} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : FiniteDimensional ℝ V]
  [inst_3 : MeasurableSpace V] [inst_4 : BorelSpace V] {H : Type u_4} [inst_5 : NormedAddCommGroup H]
  [inst_6 : InnerProductSpace ℂ H] [CompleteSpace H] (f : SchwartzMap V H),
  ∫ (ξ : V), ‖(FourierTransform.fourier f) ξ‖ ^ 2 = ∫ (x : V), ‖f x‖ ^ 2
-- Mathlib.CategoryTheory.Functor.CurryingThree
/-- Flip the first and third arguments in a trifunctor.
 -/
CategoryTheory.Functor.flip₁₃ : {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 C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E)) →
                  CategoryTheory.Functor C₃ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₁ E))
-- Mathlib.CategoryTheory.Limits.FinallySmall
CategoryTheory.finallySmall_of_final_of_finallySmall : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {K : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} K]
  [CategoryTheory.FinallySmall K] (F : CategoryTheory.Functor K J) [F.Final], CategoryTheory.FinallySmall J
-- Mathlib.Combinatorics.Additive.Energy
Finset.mulEnergy_self_pos : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Mul α] {s : Finset α}, s.Nonempty → 0 < s.mulEnergy s
-- Std.Sat.AIG.CNF
/-- There are always as many marks as AIG nodes.
 -/
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.Cache.hmarks : ∀ {aig : Std.Sat.AIG ℕ} {cnf : Std.Sat.CNF ℕ} (self : Std.Sat.AIG.toCNF.Cache✝ aig cnf),
  (Std.Sat.AIG.toCNF.Cache.marks✝ self).size = aig.decls.size
-- Init.ByCases
/-- A function applied to a `ite` is a `ite` of that function applied to each of the branches.  -/
apply_ite : ∀ {α : Sort u_1} {β : Sort u_2} (f : α → β) (P : Prop) [inst : Decidable P] (x y : α),
  f (if P then x else y) = if P then f x else f y
-- Mathlib.Topology.MetricSpace.PiNat
/-- In the case where `E` has constant value `α`,
the cylinder `cylinder x n` can be identified with the element of `List α`
consisting of the first `n` entries of `x`. See `cylinder_eq_res`.
We call this list `res x n`, the restriction of `x` to `n`.  -/
PiNat.res : {α : Type u_2} → (ℕ → α) → ℕ → List α
-- Mathlib.Data.Set.Card
Set.Finite.encard_eq_coe : ∀ {α : Type u_1} {s : Set α}, s.Finite → s.encard = ↑s.encard.toNat
-- Mathlib.Algebra.Group.Subsemigroup.Membership
Subsemigroup.mem_iSup_of_directed : ∀ {M : Type u_2} [inst : Mul M] {ι : Sort u_3} {S : ι → Subsemigroup M},
  Directed (fun x1 x2 => x1 ≤ x2) S → ∀ {x : M}, x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.mem_add : ∀ {α : Type u_1} {m : α} {a b : FreeAddMonoid α}, m ∈ a + b ↔ m ∈ a ∨ m ∈ b
-- Lean.DocString.Extension
Lean.ElabInline.deferred.inj : ∀ {index index_1 : ℕ}, Lean.ElabInline.deferred index = Lean.ElabInline.deferred index_1 → index = index_1
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_obj_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D)
  (R : CategoryTheory.Functor E D)
  (P : CategoryTheory.Grothendieck (R.comp (CategoryTheory.CostructuredArrow.functor L))),
  ((CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma L R).obj P).left =
    CategoryTheory.CostructuredArrow.left P.fiber
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- Expressions for atomic non-structural 2-isomorphisms.  -/
Mathlib.Tactic.BicategoryLike.AtomIso : Type
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
/-- `exp ∘ f` is analytic  -/
AnalyticAt.cexp' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {x : E},
  AnalyticAt ℂ f x → AnalyticAt ℂ (fun z => Complex.exp (f z)) x
-- Mathlib.Algebra.Algebra.Hom
AlgHom.coe_fn_injective : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B], Function.Injective DFunLike.coe
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryLT.congr_simp : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k k_1 : α) (e_k : k = k_1)
  (t t_1 : Std.DTreeMap.Internal.Impl α fun x => β) (e_t : t = t_1) (ho : t.Ordered)
  (he : ∃ a ∈ t, compare a k = Ordering.lt),
  Std.DTreeMap.Internal.Impl.Const.getEntryLT k t ho he = Std.DTreeMap.Internal.Impl.Const.getEntryLT k_1 t_1 ⋯ ⋯
-- Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
TensorialAt.mkHom_apply : ∀ {𝕜 : 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] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] {A : Type u_9} [inst_13 : AddCommGroup A]
  [inst_14 : Module 𝕜 A] [inst_15 : VectorBundle 𝕜 F V] [inst_16 : CompleteSpace 𝕜] [inst_17 : FiniteDimensional 𝕜 F]
  [inst_18 : ContMDiffVectorBundle 1 F V I] [inst_19 : TopologicalSpace A] [inst_20 : IsTopologicalAddGroup A]
  [inst_21 : ContinuousSMul 𝕜 A] {Φ : ((x : M) → V x) → A} {x : M} (hΦ : TensorialAt I F (fun x => Φ x) x)
  {σ : (x : M) → V x}, MDiffAt (T% σ) x → (TensorialAt.mkHom Φ x hΦ) (σ x) = Φ σ
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
/-- A pseudofunctor `F` between bicategories `B` and `C` consists of a function between objects
`F.obj`, a function between 1-morphisms `F.map`, and a function between 2-morphisms `F.map₂`.

Unlike functors between categories, `F.map` does not need to strictly commute with composition,
and does not need to strictly preserve the identity. Instead, there are specified 2-isomorphisms
`F.map (𝟙 a) ≅ 𝟙 (F.obj a)` and `F.map (f ≫ g) ≅ F.map f ≫ F.map g`.

`F.map₂` strictly commutes with compositions and preserves the identity. It also preserves the
associator, the left unitor, and the right unitor modulo some adjustments of domains and codomains
of 2-morphisms.
 -/
CategoryTheory.Pseudofunctor : (B : Type u₁) →
  [CategoryTheory.Bicategory B] →
    (C : Type u₂) → [CategoryTheory.Bicategory C] → Type (max (max (max (max (max u₁ u₂) v₁) v₂) w₁) w₂)
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
/-- The map `a` of Equations (3,4) [MM92].  -/
CategoryTheory.Equalizer.Sieve.secondMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) →
      {X : C} →
        (S : CategoryTheory.Sieve X) →
          CategoryTheory.Equalizer.FirstObj P S.arrows ⟶ CategoryTheory.Equalizer.Sieve.SecondObj P S
-- Mathlib.Tactic.MkIffOfInductiveProp
/-- Calls `cases` on `h` (assumed to be a binary product) `n` times, and returns
the resulting subgoal and the new hypotheses.
 -/
Mathlib.Tactic.MkIff.nCasesProd : ℕ → Lean.MVarId → Lean.FVarId → Lean.MetaM (Lean.MVarId × List Lean.FVarId)
-- Init.Data.Array.Attach
Array.foldr_unattach : ∀ {α : Type u_1} {β : Type u_2} {P : α → Prop} {xs : Array (Subtype P)} {f : α → β → β} {x : β},
  Array.foldr f x xs.unattach =
    Array.foldr
      (fun x s =>
        match x with
        | ⟨x, h⟩ => binderNameHint x f (binderNameHint s (f x) (binderNameHint h () (f (wfParam x) s))))
      x xs
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- The fork obtained by postcomposing an equalizer fork with a monomorphism is an equalizer.  -/
CategoryTheory.Limits.isEqualizerCompMono : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f g : X ⟶ Y} →
        {c : CategoryTheory.Limits.Fork f g} →
          CategoryTheory.Limits.IsLimit c →
            {Z : C} →
              (h : Y ⟶ Z) →
                [hm : CategoryTheory.Mono h] →
                  have this := ⋯;
                  CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι c.ι ⋯)
-- Init.Data.UInt.Bitwise
UInt8.ofBitVec_xor : ∀ (a b : BitVec 8), { toBitVec := a ^^^ b } = { toBitVec := a } ^^^ { toBitVec := b }
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Hom.resLE_map_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U U' : Y.Opens} {V : X.Opens}
  (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (i : U ≤ U') {Z : AlgebraicGeometry.Scheme} (h : ↑U' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.resLE f U V e)
      (CategoryTheory.CategoryStruct.comp (Y.homOfLE i) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.resLE f U' V ⋯) h
-- Mathlib.Algebra.Homology.ExactSequenceFour
CategoryTheory.ComposableArrows.Exact.cokerIsoKer'.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Balanced C] {n : ℕ} {S : CategoryTheory.ComposableArrows C (n + 3)} (hS : S.Exact) (k : ℕ)
  (hk : k ≤ n) (cc : CategoryTheory.Limits.CokernelCofork (S.map' k (k + 1) ⋯ ⋯))
  (kf : CategoryTheory.Limits.KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)) (hcc hcc_1 : CategoryTheory.Limits.IsColimit cc),
  hcc = hcc_1 →
    ∀ (hkf hkf_1 : CategoryTheory.Limits.IsLimit kf),
      hkf = hkf_1 → hS.cokerIsoKer' k hk cc kf hcc hkf = hS.cokerIsoKer' k hk cc kf hcc_1 hkf_1
-- Mathlib.Order.Filter.Pointwise
Filter.prod_one : ∀ {α : Type u_2} {β : Type u_3} [inst : One α] {l : Filter β}, l ×ˢ 1 = Filter.map (fun x => (x, 1)) l
-- Aesop.Rule.Basic
Aesop.Rule.instBEq : {α : Type} → BEq (Aesop.Rule α)
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
/-- A congruence lemma for `mfderiv`, (ab)using the fact that `TangentSpace I' (f x)` is
definitionally equal to `E'`.  -/
mfderiv_congr_point : ∀ {𝕜 : 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] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x x' : M},
  x = x' → mfderiv% f x = mfderiv% f x'
-- Mathlib.Algebra.WithConv
/-- Converts an element of `WithConv A` back to `A`.  -/
WithConv.ofConv : {A : Sort u_1} → WithConv A → A
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Finpartition.mk_mem_nonUniforms : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : DecidableEq α] {A : Finset α}
  (P : Finpartition A) (G : SimpleGraph α) [inst_3 : DecidableRel G.Adj] {ε : 𝕜} {u v : Finset α},
  (u, v) ∈ P.nonUniforms G ε ↔ u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ¬G.IsUniform ε u v
-- Mathlib.Analysis.Convex.Hull
convexHull_eq_self : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {s : Set E}, (convexHull 𝕜) s = s ↔ Convex 𝕜 s
-- Mathlib.Algebra.Ring.BooleanRing
instSubBool_mathlib : Sub Bool
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.toPresheaf_map : ∀ {X : AlgebraicGeometry.Scheme} {M N : X.Modules} {φ : M ⟶ N},
  (AlgebraicGeometry.Scheme.Modules.toPresheaf X).map φ = AlgebraicGeometry.Scheme.Modules.Hom.mapPresheaf φ
-- Mathlib.Topology.Defs.Sequences
SequentialSpace.isClosed_of_seq : ∀ {X : Type u_1} {inst : TopologicalSpace X} [self : SequentialSpace X] (s : Set X), IsSeqClosed s → IsClosed s
-- Mathlib.Order.WithBot
WithTop.lt_toDual_iff : ∀ {α : Type u_1} [inst : LT α] {x : WithTop α} {y : WithBot αᵒᵈ}, y < WithTop.toDual x ↔ x < WithBot.ofDual y
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsQF.isExistential : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α n}, φ.IsQF → φ.IsExistential
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Pi.isoLimit_hom_π_assoc : ∀ {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C)
  [inst_1 : CategoryTheory.Limits.HasProduct fun j => X.obj { as := j }] [inst_2 : CategoryTheory.Limits.HasLimit X]
  (j : α) {Z : C} (h : X.obj { as := j } ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.isoLimit X).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π X { as := j }) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun j => X.obj { as := j }) j) h
-- Mathlib.RingTheory.WittVector.Compare
/-- The ring of Witt vectors over `ZMod p` is isomorphic to the ring of `p`-adic integers. This
equivalence is witnessed by `WittVector.toPadicInt` with inverse `WittVector.fromPadicInt`.
 -/
WittVector.equiv : (p : ℕ) → [hp : Fact (Nat.Prime p)] → WittVector p (ZMod p) ≃+* ℤ_[p]
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.instFunLike : {α : Type u_2} →
  {β : Type u_3} → [inst : Min α] → [inst_1 : Top α] → [inst_2 : Min β] → [inst_3 : Top β] → FunLike (InfTopHom α β) α β
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrix'_symm : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_4} {n : Type u_5} [inst_1 : DecidableEq n] [inst_2 : Fintype n],
  LinearMap.toMatrix'.symm = Matrix.toLin'
-- Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
/-- The projection map from `functorObj M N n` to `N m`, when `m ≥ n`  -/
CategoryTheory.Limits.SequentialProduct.functorObjProj_neg : {C : Type u_1} →
  {M N : ℕ → C} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Limits.HasCountableProducts C] →
        (n m : ℕ) → ¬m < n → (CategoryTheory.Limits.SequentialProduct.functorObj M N n ⟶ N m)
-- Mathlib.Data.Matrix.Basis
Matrix.liftLinear_apply : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_5} (S : Type u_6) {α : Type u_7} {β : Type u_8} [inst : DecidableEq m]
  [inst_1 : DecidableEq n] [inst_2 : Fintype m] [inst_3 : Fintype n] [inst_4 : Semiring R] [inst_5 : Semiring S]
  [inst_6 : AddCommMonoid α] [inst_7 : AddCommMonoid β] [inst_8 : Module R α] [inst_9 : Module R β]
  [inst_10 : Module S β] [inst_11 : SMulCommClass R S β] (f : m → n → α →ₗ[R] β) (M : Matrix m n α),
  ((Matrix.liftLinear S) f) M = ∑ i, ∑ j, (f i j) (M i j)
-- Lean.Meta.Tactic.Backtrack
_private.Lean.Meta.Tactic.Backtrack.0.Lean.Meta.Tactic.Backtrack.Backtrack.run.match_3.eq_1 : ∀ (motive : List Lean.MVarId → Sort u_1) (h_1 : Unit → motive [])
  (h_2 : (g : Lean.MVarId) → (gs : List Lean.MVarId) → motive (g :: gs)),
  (match [] with
    | [] => h_1 ()
    | g :: gs => h_2 g gs) =
    h_1 ()
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.forM_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} {m : Type w → Type w'}
  [Std.TransCmp cmp] [inst : Monad m] [LawfulMonad m] {f : (a : α) × β a → m PUnit.{w + 1}},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → forM t₁ f = forM t₂ f
-- Mathlib.MeasureTheory.Measure.Comap
/-- Pullback of a `Measure` as a linear map. If `f` sends each measurable set to a measurable
set, then for each measurable set `s` we have `comapₗ f μ s = μ (f '' s)`.

Note that if `f` is not injective, this definition assigns `Set.univ` measure zero.

If the linearity is not needed, please use `comap` instead, which works for a larger class of
functions. `comapₗ` is an auxiliary definition and most lemmas deal with comap.  -/
MeasureTheory.Measure.comapₗ : {α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] →
      [inst_1 : MeasurableSpace β] → (α → β) → MeasureTheory.Measure β →ₗ[ENNReal] MeasureTheory.Measure α
-- Mathlib.AlgebraicGeometry.Cover.Open
AlgebraicGeometry.Scheme.instIsOpenImmersionF : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (i : 𝒰.I₀), AlgebraicGeometry.IsOpenImmersion (𝒰.f i)
-- Mathlib.NumberTheory.Height.MvPolynomial
AbsoluteValue.eval_mvPolynomial_le : ∀ {K : Type u_4} [inst : Field K] {ι : Type u_5} [Finite ι] (v : AbsoluteValue K ℝ) {p : MvPolynomial ι K} {N : ℕ},
  p.IsHomogeneous N → ∀ (x : ι → K), v ((MvPolynomial.eval x) p) ≤ (p.coeff.sum fun x c => v c) * (⨆ i, v (x i)) ^ N
-- Mathlib.NumberTheory.LSeries.Linearity
LSeriesSummable.smul_iff : ∀ {f : ℕ → ℂ} {c s : ℂ}, c ≠ 0 → (LSeriesSummable (c • f) s ↔ LSeriesSummable f s)
-- Aesop.Tree.Data
Aesop.Iteration.succ : Aesop.Iteration → Aesop.Iteration
-- Mathlib.CategoryTheory.ObjectProperty.Opposite
CategoryTheory.ObjectProperty.op_singleton : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] (X : C),
  (CategoryTheory.ObjectProperty.singleton X).op = CategoryTheory.ObjectProperty.singleton (Opposite.op X)
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.restrictScalarsCongr_hom_app : ∀ {R : Type u₁} {S : Type u₂} [inst : Ring R] [inst_1 : Ring S] {f g : R →+* S} (e : f = g) (M : ModuleCat S) (x : ↑M),
  (CategoryTheory.ConcreteCategory.hom ((ModuleCat.restrictScalarsCongr e).hom.app M)) x = x
-- Mathlib.Algebra.Polynomial.Laurent
Polynomial.toLaurent_comp_C : ∀ {R : Type u_1} [inst : Semiring R], ⇑Polynomial.toLaurent ∘ ⇑Polynomial.C = ⇑LaurentPolynomial.C
-- Mathlib.CategoryTheory.Bicategory.Opposites
Bicategory.Opposite.bicategory_whiskerLeft_unop2 : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : Bᵒᵖ} (f : a ⟶ b) (g h : b ⟶ c) (η : g ⟶ h),
  (CategoryTheory.Bicategory.whiskerLeft f η).unop2 = CategoryTheory.Bicategory.whiskerRight η.unop2 f.unop
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.divCoeffs : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr → Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof
-- Mathlib.RingTheory.Valuation.Discrete.Basic
/-- The generator of a discrete valuation in `ℤᵐ⁰` that contains `exp (-1)` in its range
is equal to `exp (-1)`.  -/
Valuation.IsRankOneDiscrete.generator_eq_exp_neg_one_of_mem_range : ∀ {A : Type u_2} [inst : Ring A] {v : Valuation A (WithZero (Multiplicative ℤ))} [hv : v.IsRankOneDiscrete],
  WithZero.exp (-1) ∈ Set.range ⇑v →
    Valuation.IsRankOneDiscrete.generator v =
      Units.mk0 (WithZero.exp (-1)) Valuation.IsRankOneDiscrete.generator_eq_exp_neg_one_of_mem_range._proof_1
-- Mathlib.GroupTheory.OrderOfElement
/-- In a nontrivial monoid with zero, the order of the zero element is zero.  -/
orderOf_zero : ∀ (M₀ : Type u_6) [inst : MonoidWithZero M₀] [Nontrivial M₀], orderOf 0 = 0
-- Mathlib.Topology.LocalAtTarget
Set.restrictPreimage_isEmbedding : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} (s : Set β),
  Topology.IsEmbedding f → Topology.IsEmbedding (s.restrictPreimage f)
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Function.Surjective.multipliable_iff_of_hasProd_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {α' : Type u_4}
  [inst_2 : CommMonoid α'] [inst_3 : TopologicalSpace α'] {e : α' → α},
  Function.Surjective e →
    ∀ {f : β → α} {g : γ → α'}, (∀ {a : α'}, HasProd f (e a) ↔ HasProd g a) → (Multipliable f ↔ Multipliable g)
-- Mathlib.Logic.Nonempty
subsingleton_of_not_nonempty : ∀ {α : Sort u_3}, ¬Nonempty α → Subsingleton α
-- Init.NotationExtra
Lean.expandBracketedBindersAux : Lean.Syntax → Array Lean.Syntax → Lean.Syntax → Lean.MacroM Lean.Syntax
-- Mathlib.LinearAlgebra.Matrix.Hermitian
Matrix.IsHermitian.conjTranspose : ∀ {α : Type u_1} {n : Type u_4} [inst : Star α] {A : Matrix n n α}, A.IsHermitian → A.conjTranspose.IsHermitian
-- Mathlib.Topology.SmallInductiveDimension
HasSmallInductiveDimensionLE.mono : ∀ {X : Type u_1} [inst : TopologicalSpace X] {m n : ℕ},
  m ≤ n → HasSmallInductiveDimensionLE X m → HasSmallInductiveDimensionLE X n
-- Mathlib.Order.LiminfLimsup
Filter.HasBasis.limsup_eq_sInf_iUnion_iInter : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {ι : Type u_6} {ι' : Type u_7} {f : ι → α} {v : Filter ι}
  {p : ι' → Prop} {s : ι' → Set ι}, v.HasBasis p s → Filter.limsup f v = sInf (⋃ j, ⋂ i, Set.Ici (f ↑i))
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.selfEquivSigmaOrbits'.eq_1 : ∀ (G : Type u_1) (α : Type u_2) [inst : Group G] [inst_1 : MulAction G α],
  MulAction.selfEquivSigmaOrbits' G α =
    Trans.trans (Equiv.sigmaFiberEquiv Quotient.mk').symm (Equiv.sigmaCongrRight fun x => Equiv.subtypeEquivRight ⋯)
-- Mathlib.CategoryTheory.Galois.Prorepresentability
CategoryTheory.PreGaloisCategory.PointedGaloisObject.instHasColimitOppositeFunctorTypeCompOpInclCoyoneda : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F],
  CategoryTheory.Limits.HasColimit
    ((CategoryTheory.PreGaloisCategory.PointedGaloisObject.incl F).op.comp CategoryTheory.coyoneda)
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_cons : ∀ (b : Bool) {n : ℕ} (x : BitVec n) (i : ℕ), (BitVec.cons b x).getLsbD i = if i = n then b else x.getLsbD i
-- Lean.Widget.InteractiveDiagnostic
_private.Lean.Widget.InteractiveDiagnostic.0.Lean.Widget.EmbedFmt.widget.injEq : ∀ (wi : Lean.Widget.WidgetInstance) (alt : Std.Format) (wi_1 : Lean.Widget.WidgetInstance) (alt_1 : Std.Format),
  (Lean.Widget.EmbedFmt.widget✝ wi alt = Lean.Widget.EmbedFmt.widget✝ wi_1 alt_1) = (wi = wi_1 ∧ alt = alt_1)
-- Mathlib.LinearAlgebra.Dual.Lemmas
Module.exists_dual_forall_apply_eq_one : ∀ {ι : Type u_1} {K : Type u_2} {V : Type u_3} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {s : Set ι} {v : ι → V}, LinearIndepOn K v s → ∃ f, ∀ i ∈ s, f (v i) = 1