mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.Reindex
Matrix.reindexLinearEquiv_refl_refl : ∀ {m : Type u_2} {n : Type u_3} (R : Type u_11) (A : Type u_12) [inst : Semiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : Module R A], Matrix.reindexLinearEquiv R A (Equiv.refl m) (Equiv.refl n) = LinearEquiv.refl R (Matrix m n A)
-- Lean.PrivateName
Lean.privateToUserName : Lean.Name → Lean.Name
-- Mathlib.Data.Nat.Init
Nat.leRec.eq_def : ∀ {n : ℕ} {motive : (m : ℕ) → n ≤ m → Sort u_1} (refl : motive n ⋯)
  (le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯) (x : ℕ) (x_1 : n ≤ x),
  Nat.leRec refl le_succ_of_le x_1 =
    match x, x_1 with
    | 0, H =>
      (fun h =>
          Eq.ndrec (motive := fun {n} =>
            {motive : (m : ℕ) → n ≤ m → Sort u_1} →
              motive n ⋯ → (⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯) → (H : n ≤ 0) → motive 0 H)
            (fun {motive} refl le_succ_of_le H => refl) ⋯ refl le_succ_of_le H)
        ⋯
    | m.succ, H =>
      ⋯.by_cases (fun h => le_succ_of_le h (Nat.leRec refl le_succ_of_le h)) fun h =>
        Eq.ndrec (motive := fun {n} =>
          {motive : (m : ℕ) → n ≤ m → Sort u_1} →
            motive n ⋯ → (⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯) → (H : n ≤ m + 1) → motive (m + 1) H)
          (fun {motive} refl le_succ_of_le H => refl) ⋯ refl le_succ_of_le H
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.Clause.instEntailsLiteral : {α : Type u_1} → Std.Tactic.BVDecide.LRAT.Internal.Entails α (Std.Sat.Literal α)
-- Lean.Widget.TaggedText
_private.Lean.Widget.TaggedText.0.Lean.Widget.TaggedText.TaggedState.tagStack : Lean.Widget.TaggedText.TaggedState✝ → List (ℕ × ℕ × Lean.Widget.TaggedText (ℕ × ℕ))
-- Mathlib.Data.Nat.Prime.Defs
Nat.Prime.one_lt' : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], Fact (1 < p)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.addY_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} [inst_1 : DecidableEq F] {P Q : Fin 3 → F},
  W.Equation P →
    W.Equation Q →
      P 2 ≠ 0 →
        Q 2 ≠ 0 →
          P 0 * Q 2 ≠ Q 0 * P 2 →
            W.addY P Q / W.addZ P Q =
              W.toAffine.addY (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2)
                (W.toAffine.slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2))
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instFromJsonChangeAnnotationSupport : Lean.FromJson Lean.Lsp.ChangeAnnotationSupport
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.submatrix_zero : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [inst : Zero α], Matrix.submatrix 0 = 0
-- Init.Prelude
/-- An exception of type `ε` and a new state `σ`.  -/
EStateM.Result.error : {ε σ α : Type u} → ε → σ → EStateM.Result ε σ α
-- Init.Data.Range.Polymorphic.PRange
/-- The lower bound of the range. `lower` is included in the range.
   -/
Std.Rcc.lower : {α : Type u} → Std.Rcc α → α
-- Init.Data.String.Termination
String.Pos.Down.inner : {s : String} → String.Pos.Down s → s.Pos
-- Init.Data.SInt.Lemmas
Int32.ofIntClamp_int8ToInt : ∀ (x : Int8), Int32.ofIntClamp x.toInt = x.toInt32
-- Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
Algebra.Generators.snd_cotangentCompLocalizationAwayEquiv : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} {ι : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T] (g : S) [inst_7 : IsLocalization.Away g T] (P : Algebra.Generators R S ι)
  {x : ((Algebra.Generators.localizationAway T g).comp P).toExtension.Cotangent}
  (hx :
    (Algebra.Extension.Cotangent.map ((Algebra.Generators.localizationAway T g).ofComp P).toExtensionHom) x =
      Algebra.Generators.cMulXSubOneCotangent T g)
  (a : ((Algebra.Generators.localizationAway T g).comp P).toExtension.Cotangent),
  ((Algebra.Generators.cotangentCompLocalizationAwayEquiv g P hx) a).2 =
    (Algebra.Extension.Cotangent.map ((Algebra.Generators.localizationAway T g).ofComp P).toExtensionHom) a
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.nonUnitalNormedRing : {I : Type u_5} → {B : I → Type u_6} → [inst : (i : I) → NonUnitalNormedRing (B i)] → NonUnitalNormedRing ↥(lp B ⊤)
-- Init.Data.List.Basic
/-- Returns `true` if `true` is an element of the list `bs`.

`O(|bs|)`. Short-circuits at the first `true` value.

* `[true, true, true].or = true`
* `[true, false, true].or = true`
* `[false, false, false].or = false`
* `[false, false, true].or = true`
* `[].or = false`
 -/
List.or : List Bool → Bool
-- Mathlib.CategoryTheory.Comma.Over.Pullback
/-- If `G` is a right adjoint and its source category has pushouts, then so is
`post G : Under Y ⥤ Under (G Y)`.

If the left adjoint of `G` is `F`, then the left adjoint of `post G` is given by
`(G Y ⟶ X) ↦ (Y ⟶ Y ⨿_{F G Y} F X ⟶ F X)`.  -/
CategoryTheory.Under.postAdjunctionRight : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.Limits.HasPushouts D] →
          {Y : D} →
            {F : CategoryTheory.Functor C D} →
              {G : CategoryTheory.Functor D C} →
                (a : F ⊣ G) →
                  (CategoryTheory.Under.post F).comp (CategoryTheory.Under.pushout (a.counit.app Y)) ⊣
                    CategoryTheory.Under.post G
-- Mathlib.Algebra.Order.Hom.Monoid
/-- An `OrderMonoidIso` respects `≤`.  -/
OrderMonoidIso.map_le_map_iff' : ∀ {α : Type u_6} {β : Type u_7} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Mul α] [inst_3 : Mul β]
  (self : α ≃*o β) {a b : α}, self.toFun a ≤ self.toFun b ↔ a ≤ b
-- Init.Data.BitVec.Lemmas
BitVec.getMsb?_eq_getLsb? : ∀ {w : ℕ} (x : BitVec w) (i : ℕ), x.getMsb? i = if i < w then x.getLsb? (w - 1 - i) else none
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.coe_center : ∀ (R : Type u) [inst : NonUnitalNonAssocRing R], ↑(NonUnitalSubring.center R) = Set.center R
-- Mathlib.Topology.Order.Monotone
/-- A monotone function continuous at the indexed infimum over a nonempty `Sort` sends this indexed
infimum to the indexed infimum of the composition.  -/
Monotone.map_ciInf_of_continuousAt : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
  [OrderTopology α] [inst_3 : ConditionallyCompleteLinearOrder β] [inst_4 : TopologicalSpace β] [OrderClosedTopology β]
  {ι : Sort u_3} [Nonempty ι] {f : α → β} {g : ι → α},
  ContinuousAt f (iInf g) →
    Monotone f →
      autoParam (BddBelow (Set.range g)) Monotone.map_ciInf_of_continuousAt._auto_1 → f (⨅ i, g i) = ⨅ i, f (g i)
-- Mathlib.Order.Heyting.Regular
Heyting.Regular.coe_le_coe : ∀ {α : Type u_1} [inst : HeytingAlgebra α] {a b : Heyting.Regular α}, ↑a ≤ ↑b ↔ a ≤ b
-- Init.Data.String.Pattern.String
String.Slice.Pattern.ForwardSliceSearcher : String.Slice → Type
-- Init.Data.Array.Lemmas
Array.sum_eq_foldl : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : Add α] [Std.Associative fun x1 x2 => x1 + x2]
  [Std.LawfulIdentity (fun x1 x2 => x1 + x2) 0] {xs : Array α}, xs.sum = Array.foldl (fun x1 x2 => x1 + x2) 0 xs
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.contains_inter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, (m₁.inter m₂).contains k = (m₁.contains k && m₂.contains k)
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
IsSymmetricAlgebra.algHom_ext : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_3}
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] {f : M →ₗ[R] A} {A' : Type u_4} [inst_5 : CommSemiring A']
  [inst_6 : Algebra R A'], IsSymmetricAlgebra f → ∀ {F G : A →ₐ[R] A'}, ↑F ∘ₗ f = ↑G ∘ₗ f → F = G
-- Mathlib.Order.Fin.Tuple
strictAnti_vecCons : ∀ {α : Type u_1} [inst : Preorder α] {n : ℕ} {f : Fin (n + 1) → α} {a : α},
  StrictAnti (Matrix.vecCons a f) ↔ f 0 < a ∧ StrictAnti f
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.instToFormatSimprocEntry : Std.ToFormat Lean.Meta.Simp.SimprocEntry
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.flipping_inverse_obj_map_app : ∀ {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]
  (F : CategoryTheory.Functor D (CategoryTheory.Functor C E)) {X Y : C} (f : X ⟶ Y) (j : D),
  ((CategoryTheory.Functor.flipping.inverse.obj F).map f).app j = (F.obj j).map f
-- Mathlib.Algebra.Order.Module.Defs
pos_iff_pos_of_smul_pos : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulWithZero α β]
  [inst_3 : Preorder α] [inst_4 : Preorder β] [PosSMulReflectLT α β] [SMulPosReflectLT α β], 0 < a • b → (0 < a ↔ 0 < b)
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
ContDiffBump.eventuallyEq_one_of_mem_ball : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E] {c : E}
  (f : ContDiffBump c) {x : E}, x ∈ Metric.ball c f.rIn → ↑f =ᶠ[nhds x] 1
-- Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
ContinuousAffineMap.norm_comp_le : ∀ {𝕜 : Type u_1} {V : Type u_3} {W : Type u_4} {W₂ : Type u_5} [inst : SeminormedAddCommGroup V]
  [inst_1 : SeminormedAddCommGroup W] [inst_2 : SeminormedAddCommGroup W₂] [inst_3 : NontriviallyNormedField 𝕜]
  [inst_4 : NormedSpace 𝕜 V] [inst_5 : NormedSpace 𝕜 W] [inst_6 : NormedSpace 𝕜 W₂] (f : V →ᴬ[𝕜] W) (g : W₂ →ᴬ[𝕜] V),
  ‖f.comp g‖ ≤ ‖f‖ * ‖g‖ + ‖f 0‖
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.Entry.inj.injEq : ∀ (thm thm_1 : Lean.Meta.Grind.InjectiveTheorem),
  (Lean.Meta.Grind.Entry.inj thm = Lean.Meta.Grind.Entry.inj thm_1) = (thm = thm_1)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.diff_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t₁.diff t₂ = t₁ \ t₂
-- Mathlib.Algebra.Order.Group.PosPart
/-- The *negative part* of an element `a` in a lattice ordered group is `(-a) ⊔ 0`, denoted `a⁻`.
 -/
instNegPart : {α : Type u_1} → [Lattice α] → [SubNegMonoid α] → NegPart α
-- Mathlib.CategoryTheory.FiberedCategory.Cocartesian
CategoryTheory.Functor.IsCocartesian.universal_property : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} {inst : CategoryTheory.Category.{v₁, u₁} 𝒮} {inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳}
  {p : CategoryTheory.Functor 𝒳 𝒮} {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) {φ : a ⟶ b} [self : p.IsCocartesian f φ] {b' : 𝒳}
  (φ' : a ⟶ b') [p.IsHomLift f φ'],
  ∃! χ, p.IsHomLift (CategoryTheory.CategoryStruct.id S) χ ∧ CategoryTheory.CategoryStruct.comp φ χ = φ'
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DefinitionParams.toTextDocumentPositionParams : Lean.Lsp.DefinitionParams → Lean.Lsp.TextDocumentPositionParams
-- Mathlib.Data.Nat.Log
Nat.log_mul_base : ∀ {b n : ℕ}, 1 < b → n ≠ 0 → Nat.log b (n * b) = Nat.log b n + 1
-- Mathlib.AlgebraicTopology.SimplicialCategory.SimplicialObject
CategoryTheory.SimplicialObject.instSimplicialCategorySSet : CategoryTheory.SimplicialCategory SSet
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α (fun x => Unit) cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp],
  t.WF →
    ∀ {l : List α} {k : α},
      k ∉ t → l.contains k = false → (Std.DTreeMap.Raw.Const.insertManyIfNewUnit t l).getKey? k = none
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.inter_Y : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S)
  (F : CategoryTheory.PreOneHypercover S)
  [inst_1 : ∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)]
  [inst_2 :
    ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b),
      CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (E.p₁ k) (E.f i))
        (CategoryTheory.CategoryStruct.comp (F.p₁ l) (F.f a))]
  (i j : (E.inter F.toPreZeroHypercover).I₀) (k : E.I₁ i.1 j.1 × F.I₁ i.2 j.2),
  (E.inter F).Y k =
    CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp (E.p₁ k.1) (E.f i.1))
      (CategoryTheory.CategoryStruct.comp (F.p₁ k.2) (F.f i.2))
-- Init.Control.Except
instMonadExceptOfExcept : (ε : Type u_1) → MonadExceptOf ε (Except ε)
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.map_comp_smul : ∀ {X : AlgebraicGeometry.Scheme} {M : X.Modules} {U V : X.Opens} (i : U ⟶ V) (r : ↑(X.presheaf.obj (Opposite.op V))),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Modules.smul r) (M.presheaf.map i.op) =
    CategoryTheory.CategoryStruct.comp (M.presheaf.map i.op)
      (AlgebraicGeometry.Scheme.Modules.smul ((CategoryTheory.ConcreteCategory.hom (X.presheaf.map i.op)) r))
-- Mathlib.Analysis.Normed.Lp.lpSpace
Memℓp.infty_pow : ∀ {I : Type u_5} {B : I → Type u_6} [inst : (i : I) → NormedRing (B i)] [∀ (i : I), NormOneClass (B i)]
  {f : (i : I) → B i}, Memℓp f ⊤ → ∀ (n : ℕ), Memℓp (f ^ n) ⊤
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
MeasureTheory.Measure.fst_compProd : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μ : MeasureTheory.Measure α)
  [MeasureTheory.SFinite μ] (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel κ],
  (μ.compProd κ).fst = μ
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
MulAlgebraNorm.mulAlgebraNormClass : ∀ {R : outParam (Type u_1)} {S : outParam (Type u_2)} [inst : SeminormedCommRing R] [inst_1 : Ring S]
  [inst_2 : Algebra R S], MulAlgebraNormClass (MulAlgebraNorm R S) R S
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.termg.eq_1 : ∀ {α : Type u_1} [inst : AddCommGroup α] (n : ℤ) (x a : α), Mathlib.Tactic.Abel.termg n x a = n • x + a
-- Mathlib.Analysis.ODE.PicardLindelof
ODE.FunSpace.dist_iterate_iterate_next_le_of_lipschitzWith : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E → E} {tmin tmax : ℝ}
  {t₀ : ↑(Set.Icc tmin tmax)} {x₀ x : E} {a r L K : NNReal} (hf : IsPicardLindelof f t₀ x₀ a r L K)
  (hx : x ∈ Metric.closedBall x₀ ↑r) (α : ODE.FunSpace t₀ x₀ r L) {m : ℕ} {C : NNReal},
  LipschitzWith C (ODE.FunSpace.next hf hx)^[m] →
    ∀ (n : ℕ),
      dist α ((ODE.FunSpace.next hf hx)^[m] ^[n] α) ≤
        ((∑ i ∈ Finset.range m, (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i.factorial) *
            ∑ i ∈ Finset.range n, ↑C ^ i) *
          dist α (ODE.FunSpace.next hf hx α)
-- Std.Do.WP.Basic
Std.Do.Id.instWP : Std.Do.WP Id Std.Do.PostShape.pure
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.Hom.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
      {M₁ M₂ : PresheafOfModules R} →
        (app : (X : Cᵒᵖ) → M₁.obj X ⟶ M₂.obj X) →
          autoParam
              (∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
                CategoryTheory.CategoryStruct.comp (M₁.map f)
                    ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (app Y)) =
                  CategoryTheory.CategoryStruct.comp (app X) (M₂.map f))
              PresheafOfModules.Hom.naturality._autoParam →
            M₁.Hom M₂
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.μ_pullback_left_fst_snd : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X R : C}
  {f : R ⟶ X} (R_1 S : CategoryTheory.Over X),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Over.pullback f) R_1 S))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst (CategoryTheory.MonoidalCategoryStruct.tensorObj R_1 S).hom f)
        (CategoryTheory.Limits.pullback.snd R_1.hom S.hom)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd ((CategoryTheory.Over.pullback f).obj R_1).hom
        ((CategoryTheory.Over.pullback f).obj S).hom)
      (CategoryTheory.Limits.pullback.fst S.hom f)
-- Mathlib.Algebra.Group.End
Equiv.Perm.extendDomain_mul : ∀ {α : Type u_4} {β : Type u_5} {p : β → Prop} [inst : DecidablePred p] (f : α ≃ Subtype p) (e e' : Equiv.Perm α),
  e.extendDomain f * e'.extendDomain f = (e * e').extendDomain f
-- Mathlib.MeasureTheory.Measure.Restrict
MeasurableEmbedding.comap_preimage : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} {m1 : MeasurableSpace β} {f : α → β},
  MeasurableEmbedding f →
    ∀ (μ : MeasureTheory.Measure β) (s : Set β), (MeasureTheory.Measure.comap f μ) (f ⁻¹' s) = μ (s ∩ Set.range f)
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
/-- Allocate constants to tasks according to `constantsPerTask`.  -/
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Initialize.0.Lean.Meta.RefinedDiscrTree.createImportedDiscrTree.go : {α : Type} →
  Lean.Environment →
    (Lean.Name →
        Lean.ConstantInfo →
          Lean.MetaM (List (α × List (Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry)))) →
      ℕ →
        ℕ →
          Lean.Core.Context →
            Lean.NameGenerator →
              Array (Task (Lean.Meta.RefinedDiscrTree.InitResults✝ α)) →
                ℕ → ℕ → ℕ → Lean.CoreM (Array (Task (Lean.Meta.RefinedDiscrTree.InitResults✝ α)))
-- Aesop.Tree.Data
Aesop.GoalId.instToString : ToString Aesop.GoalId
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKey?_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {km : α}, t.minKey? = some km → km ∈ t
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
addEquivOfAddOrderOfEq_symm : ∀ {G : Type u_2} {G' : Type u_3} [inst : AddGroup G] [inst_1 : AddGroup G'] {g : G}
  (hg : ∀ (x : G), x ∈ AddSubgroup.zmultiples g) {g' : G'} (hg' : ∀ (x : G'), x ∈ AddSubgroup.zmultiples g')
  (h : addOrderOf g = addOrderOf g'), (addEquivOfAddOrderOfEq hg hg' h).symm = addEquivOfAddOrderOfEq hg' hg ⋯
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.add_of_Y_ne : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F},
  W.Equation P →
    W.Equation Q →
      P 2 ≠ 0 →
        Q 2 ≠ 0 →
          P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2 →
            P 1 * Q 2 ^ 3 ≠ Q 1 * P 2 ^ 3 → W.add P Q = WeierstrassCurve.Jacobian.addU P Q • ![1, 1, 0]
-- Lean.Elab.PreDefinition.Main
_private.Lean.Elab.PreDefinition.Main.0.Lean.Elab.getMVarsAtPreDef : Lean.Elab.PreDefinition → Lean.MetaM (Array Lean.MVarId)
-- Init.Classical
/-- All propositions are `Decidable`.  -/
Classical.propDecidable : (a : Prop) → Decidable a
-- Mathlib.LinearAlgebra.Finsupp.Defs
/-- **Alias** of `Finsupp.curryLinearEquiv_symm_apply_apply`. -/
Finsupp.finsuppProdLEquiv_symm_apply_apply : ∀ {α : Type u_9} {β : Type u_10} {R : Type u_11} {M : Type u_12} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (f : α →₀ β →₀ M) (xy : α × β), ((Finsupp.curryLinearEquiv R).symm f) xy = (f xy.1) xy.2
-- Mathlib.Topology.Connected.Clopen
/-- A set `s` is preconnected if and only if
for every cover by two closed sets that are disjoint on `s`,
it is contained in one of the two covering sets.  -/
isPreconnected_iff_subset_of_disjoint_closed : ∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α},
  IsPreconnected s ↔ ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
-- Mathlib.Algebra.Torsor.Defs
sdiv_ne_one : ∀ {G : Type u_1} {P : Type u_2} [inst : Group G] [T : Torsor G P] {p q : P}, p /ₛ q ≠ 1 ↔ p ≠ q
-- Mathlib.Algebra.CharP.Lemmas
multiset_sum_pow_char_pow : ∀ {R : Type u_3} [inst : CommSemiring R] (p n : ℕ) [ExpChar R p] (s : Multiset R),
  s.sum ^ p ^ n = (Multiset.map (fun x => x ^ p ^ n) s).sum
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.map_iso_commute : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M₀ : Type u_6} {M₀' : Type u_9} [inst_1 : AddCommMonoid M₀]
  [inst_2 : AddCommMonoid M₀'] [inst_3 : Module R M₀] [inst_4 : Module R M₀'] (f₀ : M₀ →ₗ[R] M₀')
  [inst_5 : IsLocalizedModule S f₀] {M₁ : Type u_7} {M₁' : Type u_8} [inst_6 : AddCommMonoid M₁]
  [inst_7 : AddCommMonoid M₁'] [inst_8 : Module R M₁] [inst_9 : Module R M₁'] (f₁ : M₁ →ₗ[R] M₁')
  [inst_10 : IsLocalizedModule S f₁] (g : M₀ →ₗ[R] M₁),
  (IsLocalizedModule.map S f₀ f₁) g ∘ₗ ↑(IsLocalizedModule.iso S f₀) =
    ↑(IsLocalizedModule.iso S f₁) ∘ₗ
      (IsLocalizedModule.map S (LocalizedModule.mkLinearMap S M₀) (LocalizedModule.mkLinearMap S M₁)) g
-- Std.Data.HashMap.Lemmas
Std.HashMap.mem_keysArray : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [LawfulBEq α] {k : α},
  k ∈ m.keysArray ↔ k ∈ m
-- Mathlib.Tactic.Ring.Common
/-- A coefficient `value`, which must not be `0`. `e` is a raw rat cast.
If `value` is not an integer, then `hyp` should be a proof of `(value.den : α) ≠ 0`.  -/
Mathlib.Tactic.Ring.Common.ExProd.const : {u : Lean.Level} →
  {α : Q(Type u)} →
    {BaseType : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} → {e : Q(«$α»)} → BaseType e → Mathlib.Tactic.Ring.Common.ExProd BaseType sα e
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.submatrix.eq_1 : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} (A : Matrix m n α) (r : l → m) (c : o → n),
  A.submatrix r c = Matrix.of fun i j => A (r i) (c j)
-- Lean.Meta.Tactic.FVarSubst
Lean.Meta.FVarSubst.empty : Lean.Meta.FVarSubst
-- Init.Data.Array.Lemmas
/-- See also `eq_push_append_of_mem`, which proves a stronger version
in which the initial array must not contain the element.
 -/
Array.append_of_mem : ∀ {α : Type u_1} {a : α} {xs : Array α}, a ∈ xs → ∃ as bs, xs = as.push a ++ bs
-- Mathlib.CategoryTheory.Category.Pointed
/-- Constructs an isomorphism between pointed types from an equivalence that preserves the point
between them.  -/
Pointed.Iso.mk : {α β : Pointed} → (e : α.X ≃ β.X) → e α.point = β.point → (α ≅ β)
-- Std.Data.TreeSet.Raw.Basic
/-- Tries to retrieve the smallest element that is greater than or equal to the
given element, returning `none` if no such element exists.
 -/
Std.TreeSet.Raw.getGE? : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet.Raw α cmp → α → Option α
-- Mathlib.Algebra.Order.BigOperators.Expect
_private.Mathlib.Algebra.Order.BigOperators.Expect.0.«term_/ℚ_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.GuitartExact.KanExtension
CategoryTheory.TwoSquare.instIsIsoFunctorLanBaseChangeOfGuitartExact : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} {D : Type u₅} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] [inst_4 : CategoryTheory.Category.{v₅, u₅} D]
  {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃} {R : CategoryTheory.Functor C₂ C₄}
  {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B)
  [inst_5 : ∀ (F : CategoryTheory.Functor C₁ D), L.HasLeftKanExtension F]
  [inst_6 : ∀ (F : CategoryTheory.Functor C₂ D), R.HasPointwiseLeftKanExtension F] [w.GuitartExact],
  CategoryTheory.IsIso w.lanBaseChange
-- Mathlib.Analysis.Seminorm
Seminorm.finset_sup_smul : ∀ {𝕜 : Type u_3} {E : Type u_7} {ι : Type u_11} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] (p : ι → Seminorm 𝕜 E) (s : Finset ι) (C : NNReal), s.sup (C • p) = C • s.sup p
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.nonsingular_iff : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (P : Fin 3 → R),
  W'.Nonsingular P ↔
    W'.Equation P ∧
      (W'.a₁ * P 1 * P 2 - (3 * P 0 ^ 2 + 2 * W'.a₂ * P 0 * P 2 + W'.a₄ * P 2 ^ 2) ≠ 0 ∨
        2 * P 1 * P 2 + W'.a₁ * P 0 * P 2 + W'.a₃ * P 2 ^ 2 ≠ 0 ∨
          P 1 ^ 2 + W'.a₁ * P 0 * P 1 + 2 * W'.a₃ * P 1 * P 2 -
              (W'.a₂ * P 0 ^ 2 + 2 * W'.a₄ * P 0 * P 2 + 3 * W'.a₆ * P 2 ^ 2) ≠
            0)