mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.WhereFinally
Lean.Elab.WhereFinallyView.none : Lean.Elab.WhereFinallyView
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
/-- The inclusion of `E [⋀^ι]→L[𝕜] F` into `ContinuousMultilinearMap 𝕜 (fun _ : ι ↦ E) F`
as a linear isometry.  -/
ContinuousAlternatingMap.toContinuousMultilinearMapLI : {𝕜 : Type u} →
  {E : Type wE} →
    {F : Type wF} →
      {ι : Type v} →
        [inst : NontriviallyNormedField 𝕜] →
          [inst_1 : SeminormedAddCommGroup E] →
            [inst_2 : NormedSpace 𝕜 E] →
              [inst_3 : SeminormedAddCommGroup F] →
                [inst_4 : NormedSpace 𝕜 F] →
                  [inst_5 : Fintype ι] → E [⋀^ι]→L[𝕜] F →ₗᵢ[𝕜] ContinuousMultilinearMap 𝕜 (fun x => E) F
-- Mathlib.Tactic.IntervalCases
Mathlib.Tactic.IntervalCases.IntervalCasesSubgoal.mk : Lean.Expr → ℤ → Lean.MVarId → Mathlib.Tactic.IntervalCases.IntervalCasesSubgoal
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_add_int_mul_pi : ∀ (x : ℝ) (n : ℤ), Real.sin (x + ↑n * Real.pi) = (-1) ^ n * Real.sin x
-- Mathlib.MeasureTheory.Function.Piecewise
IndexedPartition.simpleFunc_piecewise.eq_1 : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] {s : ι → Set α} [inst_1 : Finite ι]
  (hs : IndexedPartition s) (hm : ∀ (i : ι), MeasurableSet (s i)) (f : ι → MeasureTheory.SimpleFunc α β),
  hs.simpleFunc_piecewise hm f =
    { toFun := hs.piecewise fun i => ⇑(f i), measurableSet_fiber' := ⋯, finite_range' := ⋯ }
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.instIsIsoSchemeMapOfCommRingCat : ∀ {R S : CommRingCat} (f : R ⟶ S) [CategoryTheory.IsIso f], CategoryTheory.IsIso (AlgebraicGeometry.Spec.map f)
-- Lean.Elab.Do.Basic
/-- The `v` in `m : Type u → Type v`.  -/
Lean.Elab.Do.MonadInfo.v : Lean.Elab.Do.MonadInfo → Lean.Level
-- Mathlib.CategoryTheory.Monoidal.CommMon_
/-- Implementation of `CommMon.equivLaxBraidedFunctorPUnit`.  -/
CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.counitIso : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        (CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided C).comp
            (CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon C) ≅
          CategoryTheory.Functor.id (CategoryTheory.CommMon C)
-- Mathlib.LinearAlgebra.Matrix.RowCol
/-- `Matrix.replicateCol ι u` is the matrix with all columns equal to the vector `u`.

To get a column matrix with exactly one column,
`Matrix.replicateCol (Fin 1) u` is the canonical choice.
 -/
Matrix.replicateCol : {m : Type u_2} → {α : Type v} → (ι : Type u_6) → (m → α) → Matrix m ι α
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
/-- The canonical isomorphism relating `Cospan f.op g.op` and `(Span f g).op`  -/
CategoryTheory.Limits.cospanOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y Z : C} →
      (f : X ⟶ Y) →
        (g : X ⟶ Z) →
          CategoryTheory.Limits.cospan f.op g.op ≅
            CategoryTheory.Limits.walkingSpanOpEquiv.inverse.comp (CategoryTheory.Limits.span f g).op
-- Mathlib.Algebra.Lie.Basic
LieHom.toLinearMap : {R : Type u_1} →
  {L : Type u_2} →
    {L' : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] → [inst_3 : LieRing L'] → [inst_4 : LieAlgebra R L'] → (L →ₗ⁅R⁆ L') → L →ₗ[R] L'
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
ENNReal.log_eq_iff : ∀ {x y : ENNReal}, x.log = y.log ↔ x = y
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instLeftCancelMonoid.eq_1 : ∀ {α : Type u_1} [inst : RightCancelMonoid α],
  MulOpposite.instLeftCancelMonoid = { toMonoid := MulOpposite.instMonoid, toIsLeftCancelMul := ⋯ }
-- Mathlib.Geometry.Diffeology.Basic
/-- The plots `EuclideanSpace ℝ (Fin n) → X` representing the smooth ways to map
`EuclideanSpace ℝ (Fin n)` into `X`. This is the main
piece of data underlying the diffeology.  -/
DiffeologicalSpace.plots : {X : Type u_1} → [self : DiffeologicalSpace X] → (n : ℕ) → Set (EuclideanSpace ℝ (Fin n) → X)
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- Given two sieves `R` and `S`, to show that `P` is a sheaf for `S`, we can show:
* `P` is a sheaf for `R`
* `P` is a sheaf for the pullback of `S` along any arrow in `R`
* `P` is separated for the pullback of `R` along any arrow in `S`.

This is mostly an auxiliary lemma to construct `Sheaf.finestTopology`.
Adapted from [Elephant], Lemma C2.1.7(ii) with suggestions as mentioned in
https://math.stackexchange.com/a/358709
 -/
CategoryTheory.Presieve.isSheafFor_trans : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (P : CategoryTheory.Functor Cᵒᵖ (Type u_1))
  (R S : CategoryTheory.Sieve X),
  CategoryTheory.Presieve.IsSheafFor P R.arrows →
    (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
        S.arrows f → CategoryTheory.Presieve.IsSeparatedFor P (CategoryTheory.Sieve.pullback f R).arrows) →
      (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
          R.arrows f → CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Sieve.pullback f S).arrows) →
        CategoryTheory.Presieve.IsSheafFor P S.arrows
-- Init.Data.List.Sort.Lemmas
_private.Init.Data.List.Sort.Lemmas.0.List.merge.match_1.splitter : {α : Type u_1} →
  (motive : List α → List α → Sort u_2) →
    (xs ys : List α) →
      ((ys : List α) → motive [] ys) →
        ((xs : List α) → (xs = [] → False) → motive xs []) →
          ((x : α) → (xs : List α) → (y : α) → (ys : List α) → motive (x :: xs) (y :: ys)) → motive xs ys
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubmonoid.ofAddUnits_addUnits_le : ∀ {M : Type u_1} [inst : AddMonoid M] (S : AddSubmonoid M), S.addUnits.ofAddUnits ≤ S
-- Mathlib.Combinatorics.Graph.Basic
Graph.IsLink.right_eq_or_eq : ∀ {α : Type u_1} {β : Type u_2} {x y z w : α} {e : β} {G : Graph α β}, G.IsLink e x y → G.IsLink e z w → y = z ∨ y = w
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.instPartialOrder : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring A] → [inst_2 : Module R A] → PartialOrder (NonUnitalSubalgebra R A)
-- Mathlib.MeasureTheory.Function.Egorov
/-- **Egorov's theorem**: If `f : ι → α → β` is a sequence of strongly measurable functions that
converges to `g : α → β` almost everywhere on a measurable set `s` of finite measure,
then for all `ε > 0`, there exists a subset `t ⊆ s` such that `μ t ≤ ε` and `f` converges to `g`
uniformly on `s \ t`. We require the index type `ι` to be countable, and usually `ι = ℕ`.

In other words, a sequence of almost everywhere convergent functions converges uniformly except on
an arbitrarily small set.  -/
MeasureTheory.tendstoUniformlyOn_of_ae_tendsto : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} [inst : PseudoEMetricSpace β]
  {μ : MeasureTheory.Measure α} [inst_1 : SemilatticeSup ι] [Nonempty ι] [Countable ι] {f : ι → α → β} {g : α → β}
  {s : Set α},
  (∀ (n : ι), MeasureTheory.StronglyMeasurable (f n)) →
    MeasureTheory.StronglyMeasurable g →
      MeasurableSet s →
        μ s ≠ ⊤ →
          (∀ᵐ (x : α) ∂μ, x ∈ s → Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) →
            ∀ {ε : ℝ},
              0 < ε → ∃ t ⊆ s, MeasurableSet t ∧ μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g Filter.atTop (s \ t)
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.zipWith.congr_simp : ∀ {ι : Type u} {β : ι → Type v} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [inst : (i : ι) → Zero (β i)]
  [inst_1 : (i : ι) → Zero (β₁ i)] [inst_2 : (i : ι) → Zero (β₂ i)] (f f_1 : (i : ι) → β₁ i → β₂ i → β i)
  (e_f : f = f_1) (hf : ∀ (i : ι), f i 0 0 = 0) (x x_1 : Π₀ (i : ι), β₁ i),
  x = x_1 → ∀ (y y_1 : Π₀ (i : ι), β₂ i), y = y_1 → DFinsupp.zipWith f hf x y = DFinsupp.zipWith f_1 ⋯ x_1 y_1
-- Mathlib.CategoryTheory.Monoidal.Skeleton
/-- If `C` is monoidal and skeletal, it is a monoid.
See note [reducible non-instances].  -/
CategoryTheory.monoidOfSkeletalMonoidal : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.MonoidalCategory C] → CategoryTheory.Skeletal C → Monoid C
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- **Alias** of `NumberField.FinitePlace.hasFiniteMulSupport_int`. -/
NumberField.FinitePlace.mulSupport_finite_int : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {x : NumberField.RingOfIntegers K},
  x ≠ 0 → Function.HasFiniteMulSupport fun w => w ↑x
-- Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
CategoryTheory.SmallObject.SuccStruct.extendToSuccRestrictionLEIso_inv_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {J : Type u} [inst_1 : LinearOrder J]
  [inst_2 : SuccOrder J] {j : J} (hj : ¬IsMax j) (F : CategoryTheory.Functor (↑(Set.Iic j)) C) {X : C}
  (τ : F.obj ⟨j, ⋯⟩ ⟶ X) (X_1 : ↑(Set.Iic j)),
  (CategoryTheory.SmallObject.SuccStruct.extendToSuccRestrictionLEIso hj F τ).inv.app X_1 =
    (CategoryTheory.SmallObject.SuccStruct.extendToSuccObjIso hj F τ ↑X_1 ⋯).inv
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.forIn_eq_forIn_toList : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : (a : α) × β a → δ → m (ForInStep δ)} {init : δ},
  forIn t init f = forIn t.toList init f
-- Mathlib.GroupTheory.Complement
AddSubgroup.isComplement_range_left : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {f : G ⧸ H → G},
  (∀ (q : G ⧸ H), ↑(f q) = q) → AddSubgroup.IsComplement (Set.range f) ↑H
-- Mathlib.Algebra.Module.LinearMap.Basic
LinearMap.instIsTorsionFree : ∀ {R : Type u_1} {R' : Type u_2} {S : Type u_3} {M : Type u_4} {M' : Type u_5} [inst : Semiring R]
  [inst_1 : Semiring R'] [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M'] [inst_4 : Module R M]
  [inst_5 : Module R' M'] {σ₁₂ : R →+* R'} [inst_6 : Semiring S] [inst_7 : Module S M'] [inst_8 : SMulCommClass R' S M']
  [Module.IsTorsionFree S M'], Module.IsTorsionFree S (M →ₛₗ[σ₁₂] M')
-- Mathlib.CategoryTheory.EssentiallySmall
CategoryTheory.LocallySmall.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  autoParam (∀ (X Y : C), Small.{w, v} (X ⟶ Y)) CategoryTheory.LocallySmall.hom_small._autoParam →
    CategoryTheory.LocallySmall.{w, v, u} C
-- Batteries.Data.List.Lemmas
List.idxOfNth_lt_length_of_lt_count : ∀ {α : Type u_1} {n : ℕ} {x : α} {xs : List α} [inst : BEq α], n < List.count x xs → List.idxOfNth x xs n < xs.length
-- Mathlib.Order.Filter.Defs
/-- Coproduct of filters.  -/
Filter.coprod : {α : Type u_1} → {β : Type u_2} → Filter α → Filter β → Filter (α × β)
-- Mathlib.Topology.Algebra.ContinuousAffineMap
/-- A continuous map of affine spaces  -/
«term_→ᴬ[_]_» : Lean.TrailingParserDescr
-- Mathlib.GroupTheory.GroupAction.Embedding
Function.Embedding.instMulAction : {G : Type u_1} → {α : Type u_3} → {β : Type u_4} → [inst : Group G] → [MulAction G β] → MulAction G (α ↪ β)
-- Mathlib.GroupTheory.OrderOfElement
addOrderOf_le_card : ∀ {G : Type u_1} [inst : AddMonoid G] {x : G} [Finite G], addOrderOf x ≤ Nat.card G
-- Mathlib.RingTheory.Multiplicity
dvd_of_emultiplicity_pos : ∀ {α : Type u_1} [inst : Monoid α] {a b : α}, 0 < emultiplicity a b → a ∣ b
-- Init.Data.UInt.Bitwise
UInt64.shiftLeft_add_of_toNat_lt : ∀ {a b c : UInt64}, b.toNat + c.toNat < 64 → a <<< (b + c) = a <<< b <<< c
-- Mathlib.Order.Interval.Finset.Gaps
Finset.intervalGapsWithin_surjOn : ∀ {α : Type u_1} [inst : LinearOrder α] (F : Finset (α × α)) {k : ℕ} (h : F.card = k) (a b : α),
  Set.SurjOn (fun j => ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) (Set.Iio k) ↑F
-- Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
NumberField.instIsTotallyRealSubtypeMemIntermediateFieldRatOfIsAlgebraic : ∀ {K : Type u_2} [inst : Field K] [NumberField.IsTotallyReal K] [inst_2 : CharZero K] (F : IntermediateField ℚ K)
  [Algebra.IsAlgebraic (↥F) K], NumberField.IsTotallyReal ↥F
-- Qq.Macro
Qq.Impl.MVarSynth.level : Lean.LMVarId → Qq.Impl.MVarSynth
-- Mathlib.Analysis.Complex.RealDeriv
DifferentiableOn.real_of_complex : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {s : Set ℂ},
  DifferentiableOn ℂ f s → DifferentiableOn ℝ f s
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.ofHom_lift : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ}
  (α : M ⟶ K) (β : CochainComplex.HomComplex.Cochain M L (-1))
  (hαβ :
    CochainComplex.HomComplex.δ (-1) 0 β +
        CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp α φ) =
      0),
  CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCocone.lift φ α β hαβ) =
    CochainComplex.mappingCocone.liftCochain φ (CochainComplex.HomComplex.Cochain.ofHom α) β
      CochainComplex.mappingCocone.lift._proof_1
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
/-- The free-forgetful adjunction between `Grpd` and `Cat`.  -/
CategoryTheory.Grpd.freeForgetAdjunction : CategoryTheory.Grpd.free ⊣ CategoryTheory.Grpd.forgetToCat
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.CongrInfo.fixedPrefix.sizeOf_spec : ∀ (prefixSize suffixSize : ℕ),
  sizeOf (Lean.Meta.Sym.CongrInfo.fixedPrefix prefixSize suffixSize) = 1 + sizeOf prefixSize + sizeOf suffixSize
-- Lean.ToExpr
Lean.instToExprNat : Lean.ToExpr ℕ
-- Lean.Elab.Tactic.Split
Lean.Elab.Tactic.evalSplit : Lean.Elab.Tactic.Tactic
-- Init.Data.List.Attach
List.filterMap_wfParam : ∀ {α : Type u_1} {β : Type u_2} {xs : List α} {f : α → Option β},
  List.filterMap f (wfParam xs) = List.filterMap f xs.attach.unattach
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Descent
Module.FaithfullyFlat.surjective_of_tensorProduct : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {T : Type u_3}
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [Module.FaithfullyFlat R S],
  Function.Surjective ⇑(algebraMap S (TensorProduct R S T)) → Function.Surjective ⇑(algebraMap R T)
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.subring_closure_le : ∀ {K : Type u} [inst : DivisionRing K] (s : Set K), Subring.closure s ≤ (Subfield.closure s).toSubring
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.leftUnitor_inv_left_snd : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X : C}
  (Y : CategoryTheory.Over X),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).inv)
      (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.id X) Y.hom) =
    CategoryTheory.CategoryStruct.id Y.left
-- Mathlib.Geometry.Manifold.Riemannian.PathELength
Manifold.riemannianEDist_triangle : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : (x : M) → ENorm (TangentSpace I x)] [∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)] {x y z : M},
  Manifold.riemannianEDist I x z ≤ Manifold.riemannianEDist I x y + Manifold.riemannianEDist I y z
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.nodup_keys : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → m.keys.Nodup
-- Init.Data.Rat.Lemmas
Rat.ne_of_lt : ∀ {a b : ℚ}, a < b → a ≠ b
-- Mathlib.Topology.Inseparable
SeparationQuotient.preimage_image_mk_open : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X},
  IsOpen s → SeparationQuotient.mk ⁻¹' SeparationQuotient.mk '' s = s
-- Mathlib.Algebra.GroupWithZero.Defs
mul_right_inj' : ∀ {M₀ : Type u_1} [inst : Mul M₀] [inst_1 : Zero M₀] [IsLeftCancelMulZero M₀] {a b c : M₀},
  a ≠ 0 → (a * b = a * c ↔ b = c)
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.toFinset_eq_toFinset : ∀ {α : Type u} {s : Set α} [inst : Fintype ↑s] (h : s.Finite), h.toFinset = s.toFinset
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.jp.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (decl : Lean.Compiler.LCNF.FunDecl pu) (k : Lean.Compiler.LCNF.Code pu)
  (decl_1 : Lean.Compiler.LCNF.FunDecl pu) (k_1 : Lean.Compiler.LCNF.Code pu),
  (Lean.Compiler.LCNF.Code.jp decl k = Lean.Compiler.LCNF.Code.jp decl_1 k_1) = (decl = decl_1 ∧ k = k_1)
-- Mathlib.RingTheory.Ideal.Quotient.Defs
Ideal.Quotient.factor_eq : ∀ {R : Type u} [inst : Ring R] {S : Ideal R} [inst_1 : S.IsTwoSided], Ideal.Quotient.factor ⋯ = RingHom.id (R ⧸ S)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
/-- The embedding from the scheme-theoretic image to the codomain.  -/
AlgebraicGeometry.Scheme.Hom.imageι : {X Y : AlgebraicGeometry.Scheme} → (f : X ⟶ Y) → AlgebraicGeometry.Scheme.Hom.image f ⟶ Y
-- Std.Sat.AIG.Lemmas
Std.Sat.AIG.instLawfulOperatorBoolMkConst : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulOperator α (fun x => Bool) Std.Sat.AIG.mkConst
-- Mathlib.Algebra.Pointwise.Stabilizer
_private.Mathlib.Algebra.Pointwise.Stabilizer.0.MulAction.termQ_1 : Lean.ParserDescr
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.equation_of_Z_eq_zero : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {P : Fin 3 → R},
  P 2 = 0 → (W'.Equation P ↔ P 1 ^ 2 = P 0 ^ 3)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
SheafOfModules.pushforwardNatTrans_app_val_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D}
  {F G : CategoryTheory.Functor C D} {T : CategoryTheory.Sheaf J RingCat} {S : CategoryTheory.Sheaf K RingCat}
  [inst_2 : F.IsContinuous J K] [inst_3 : G.IsContinuous J K] (φ : T ⟶ (G.sheafPushforwardContinuous RingCat J K).obj S)
  (α : F ⟶ G) (M : SheafOfModules S) (U : Cᵒᵖ) (x : ↑(((SheafOfModules.pushforward φ).obj M).val.obj U)),
  (CategoryTheory.ConcreteCategory.hom (((SheafOfModules.pushforwardNatTrans φ α).app M).val.app U)) x =
    (CategoryTheory.ConcreteCategory.hom (M.val.map (α.app (Opposite.unop U)).op)) x
-- Lean.Elab.Match
Lean.Elab.Term.match.ignoreUnusedAlts : Lean.Option Bool
-- Mathlib.NumberTheory.NumberField.CMField
NumberField.IsCMField.regOfFamily_realFunSystem : ∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [inst_2 : NumberField.IsCMField K] [inst_3 : NumberField K],
  NumberField.Units.regOfFamily (NumberField.IsCMField.realFundSystem K) =
    2 ^ NumberField.Units.rank K * NumberField.Units.regulator ↥(NumberField.maximalRealSubfield K)
-- Mathlib.Algebra.Order.Antidiag.Prod
Finset.HasMulAntidiagonal.mulAntidiagonalOfLocallyFinite.eq_1 : ∀ {A : Type u_2} [inst : CommMonoid A] [inst_1 : PartialOrder A] [inst_2 : CanonicallyOrderedMul A]
  [inst_3 : LocallyFiniteOrderBot A] [inst_4 : DecidableEq A],
  Finset.HasMulAntidiagonal.mulAntidiagonalOfLocallyFinite =
    { mulAntidiagonal := fun n => {uv ∈ Finset.Iic n ×ˢ Finset.Iic n | uv.1 * uv.2 = n}, mem_mulAntidiagonal := ⋯ }
-- Mathlib.Analysis.Complex.UpperHalfPlane.Measure
/-- Express the volume of a measurable set as a Lebesgue integral
over the corresponding subset of `ℂ`.  -/
UpperHalfPlane.volume_eq_lintegral : ∀ (s : Set UpperHalfPlane), MeasureTheory.volume s = ∫⁻ (z : ℂ) in UpperHalfPlane.coe '' s, ↑((1 / ‖z.im‖₊) ^ 2)
-- Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric
/-- The regularized Gaussian hypergeometric function.  -/
Complex.regularizedGaussHGFunSeries : ℂ → ℂ → ℂ → FormalMultilinearSeries ℂ ℂ ℂ
-- Mathlib.CategoryTheory.Functor.CurryingThree
CategoryTheory.Functor.bifunctorComp₁₂Iso_inv_app_app_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {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_4, u_3} C₁₂]
  [inst_4 : CategoryTheory.Category.{v_9, u_9} E] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
  (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ E)) (X : C₁) (X_1 : C₂) (X_2 : C₃),
  (((F₁₂.bifunctorComp₁₂Iso G).inv.app X).app X_1).app X_2 =
    CategoryTheory.CategoryStruct.id ((G.obj ((F₁₂.obj X).obj X_1)).obj X_2)
-- Mathlib.Topology.EMetricSpace.Defs
/-- **Alias** of `Metric.eball_mem_nhds`. -/
EMetric.ball_mem_nhds : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (x : α) {ε : ENNReal}, 0 < ε → Metric.eball x ε ∈ nhds x
-- Mathlib.CategoryTheory.Adhesive.Basic
CategoryTheory.adhesive_of_preserves_and_reflects : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u''} [inst_1 : CategoryTheory.Category.{v'', u''} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Adhesive D]
  [H₁ : ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [CategoryTheory.Mono f], CategoryTheory.Limits.HasPullback f g]
  [H₂ : ∀ {X Y S : C} (f : S ⟶ X) (g : S ⟶ Y) [CategoryTheory.Mono f], CategoryTheory.Limits.HasPushout f g]
  [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F]
  [CategoryTheory.Limits.ReflectsLimitsOfShape CategoryTheory.Limits.WalkingCospan F]
  [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingSpan F]
  [CategoryTheory.Limits.ReflectsColimitsOfShape CategoryTheory.Limits.WalkingSpan F], CategoryTheory.Adhesive C
-- Mathlib.Probability.Distributions.Fernique
ProbabilityTheory.Fernique.lintegral_exp_mul_sq_norm_le_mul : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [SecondCountableTopology E]
  [inst_3 : MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} {a : ℝ}
  [MeasureTheory.IsProbabilityMeasure μ],
  MeasureTheory.Measure.map (⇑(ContinuousLinearMap.rotation (-(Real.pi / 4)))) (μ.prod μ) = μ.prod μ →
    0 < a →
      ∀ {c' : ENNReal},
        c' ≤ μ {x | ‖x‖ ≤ a} →
          2⁻¹ < c' →
            ∫⁻ (x : E), ENNReal.ofReal (Real.exp (ProbabilityTheory.Fernique.logRatio c' * a⁻¹ ^ 2 * ‖x‖ ^ 2)) ∂μ ≤
              μ {x | ‖x‖ ≤ a} *
                (ENNReal.ofReal (Real.exp (ProbabilityTheory.Fernique.logRatio c')) +
                  ∑' (n : ℕ), ENNReal.ofReal (Real.exp (-2⁻¹ * Real.log (c' / (1 - c')).toReal * 2 ^ n)))
-- Mathlib.Analysis.Calculus.Deriv.Mul
HasDerivWithinAt.const_mul : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {𝔸 : Type u_3} [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedAlgebra 𝕜 𝔸] {d : 𝕜 → 𝔸} {d' : 𝔸} (c : 𝔸),
  HasDerivWithinAt d d' s x → HasDerivWithinAt (fun y => c * d y) (c * d') s x
-- Batteries.Tactic.Lemma
/-- Enables the use of `lemma` as a synonym for `theorem`  -/
Batteries.Tactic.Lemma.lang.lemmaCmd : Lean.Option Bool
-- Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
CategoryTheory.ObjectProperty.instIsVerdierRightLocalizingUnopOfIsVerdierLeftLocalizingOpposite : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (A B : CategoryTheory.ObjectProperty Cᵒᵖ)
  [A.IsVerdierLeftLocalizing B], A.unop.IsVerdierRightLocalizing B.unop
-- Mathlib.Topology.Instances.Matrix
HasSum.matrix_conjTranspose : ∀ {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [inst : AddCommMonoid R] [inst_1 : TopologicalSpace R]
  {L : SummationFilter X} [inst_2 : StarAddMonoid R] [ContinuousStar R] {f : X → Matrix m n R} {a : Matrix m n R},
  HasSum f a L → HasSum (fun x => (f x).conjTranspose) a.conjTranspose L
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.rightAngleRotation.congr_simp : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o o_1 : Orientation ℝ E (Fin 2)), o = o_1 → o.rightAngleRotation = o_1.rightAngleRotation
-- Mathlib.AlgebraicGeometry.Cover.Open
AlgebraicGeometry.Scheme.affineOpenCoverOfSpanRangeEqTop_X_carrier : ∀ {R : CommRingCat} {ι : Type u_1} (s : ι → ↑R) (hs : Ideal.span (Set.range s) = ⊤) (i : ι),
  ↑((AlgebraicGeometry.Scheme.affineOpenCoverOfSpanRangeEqTop s hs).X i) = Localization.Away (s i)