mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Http.Internal.IndexMultiMap
Std.Internal.IndexMultiMap.mk.inj : ∀ {α : Type u} {β : Type v} {inst : BEq α} {inst_1 : Hashable α} {entries : Array (α × β)}
  {indexes : Std.HashMap α (Array ℕ)}
  {validity :
    ∀ (k : α) (p : k ∈ indexes),
      let idx := indexes.get k p;
      idx.size > 0 ∧ ∀ i ∈ idx, i < entries.size}
  {entries_1 : Array (α × β)} {indexes_1 : Std.HashMap α (Array ℕ)}
  {validity_1 :
    ∀ (k : α) (p : k ∈ indexes_1),
      let idx := indexes_1.get k p;
      idx.size > 0 ∧ ∀ i ∈ idx, i < entries_1.size},
  { entries := entries, indexes := indexes, validity := validity } =
      { entries := entries_1, indexes := indexes_1, validity := validity_1 } →
    entries = entries_1 ∧ indexes = indexes_1
-- Batteries.Util.ProofWanted
_private.Batteries.Util.ProofWanted.0.WantedRefKind.defWanted : WantedRefKind✝
-- Mathlib.Algebra.Group.Even
IsSquare.div : ∀ {α : Type u_2} [inst : DivisionCommMonoid α] {a b : α}, IsSquare a → IsSquare b → IsSquare (a / b)
-- Mathlib.Algebra.Category.Grp.Biproducts
AddCommGrpCat.binaryProductLimitCone_isLimit_lift : ∀ (G H : AddCommGrpCat) (t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair G H)),
  (G.binaryProductLimitCone H).isLimit.lift t =
    AddCommGrpCat.ofHom
      ((AddCommGrpCat.Hom.hom (CategoryTheory.Limits.BinaryFan.fst t)).prod
        (AddCommGrpCat.Hom.hom (CategoryTheory.Limits.BinaryFan.snd t)))
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.below.neg : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  {motive : (a a_1 : RingCat.Colimits.Prequotient F) → RingCat.Colimits.Relation F a a_1 → Prop} (j : J)
  (x : ↑(F.obj j)), RingCat.Colimits.Relation.below ⋯
-- Mathlib.Algebra.GroupWithZero.WithZero
/-- The `MonoidWithZero` homomorphism `WithZero α →* WithZero β` induced by a monoid homomorphism
`f : α →* β`.  -/
WithZero.map' : {α : Type u_1} →
  {β : Type u_2} → [inst : MulOneClass α] → [inst_1 : MulOneClass β] → (α →* β) → WithZero α →*₀ WithZero β
-- Init.BinderPredicates
/-- Declare `∀ x ∈ y, ...` as syntax for `∀ x, x ∈ y → ...` and `∃ x ∈ y, ...` as syntax for
`∃ x, x ∈ y ∧ ...`  -/
Lean.«binderPred∈_» : Lean.ParserDescr
-- Mathlib.LinearAlgebra.Complex.Module
Complex.algHom_ext_iff : ∀ {A : Type u_3} [inst : Semiring A] [inst_1 : Algebra ℝ A] {f g : ℂ →ₐ[ℝ] A}, f = g ↔ f Complex.I = g Complex.I
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapGrp_obj_grp_mul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (A : CategoryTheory.Grp C),
  CategoryTheory.MonObj.mul =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F A.X A.X)
      (F.map CategoryTheory.MonObj.mul)
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
coe_basisOfPiSpaceOfLinearIndependent : ∀ {K : Type u} [inst : DivisionRing K] {ι : Type u_1} [inst_1 : Fintype ι] {b : ι → ι → K} (hb : LinearIndependent K b),
  ⇑(basisOfPiSpaceOfLinearIndependent hb) = b
-- Init.Data.List.Sublist
List.sublist_reverse_iff : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂.reverse ↔ l₁.reverse.Sublist l₂
-- Lean.Elab.ParseImportsFast
Lean.ParseImports.instInhabitedParser : Inhabited Lean.ParseImports.Parser
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.constGetEntryGT!_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited (α × β)] {k : α},
  t₁.Equiv t₂ → Std.DTreeMap.Const.getEntryGT! t₁ k = Std.DTreeMap.Const.getEntryGT! t₂ k
-- Mathlib.FieldTheory.Differential.Liouville
IsLiouville.isLiouville : ∀ {F : Type u_1} {K : Type u_2} {inst : Field F} {inst_1 : Field K} {inst_2 : Differential F} {inst_3 : Differential K}
  {inst_4 : Algebra F K} [self : IsLiouville F K] (a : F) (ι : Type) [inst_5 : Fintype ι] (c : ι → F),
  (∀ (x : ι), (c x)′ = 0) →
    ∀ (u : ι → K) (v : K),
      ↑a = ∑ x, ↑(c x) * Differential.logDeriv (u x) + v′ →
        ∃ ι₀ x c₀, ∃ (_ : ∀ (x : ι₀), (c₀ x)′ = 0), ∃ u₀ v₀, a = ∑ x, c₀ x * Differential.logDeriv (u₀ x) + v₀′
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.injective_embSigma : ∀ (n : ℕ), Function.Injective (OrderedFinpartition.embSigma n)
-- Mathlib.Algebra.Order.Quantale
/-- Left- and right-residuation operators on a quantale are similar to the Heyting
operator on complete lattices, but for a non-commutative logic.
I.e. `x ≤ y ⇨ₗ z ↔ x * y ≤ z` or alternatively `x ⇨ₗ y = sSup { z | z * x ≤ y }`.
 -/
Quantale.«term_⇨ₗ_» : Lean.TrailingParserDescr
-- Init.Data.Order.LemmasExtra
Std.instAntisymmLeOfLawfulOrderOrdOfLawfulEqOrd : ∀ {α : Type u} [inst : Ord α] [inst_1 : LE α] [Std.LawfulOrderOrd α] [Std.LawfulEqOrd α],
  Std.Antisymm fun x1 x2 => x1 ≤ x2
-- Mathlib.Topology.UniformSpace.Separation
SeparationQuotient.lift'.eq_1 : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] [inst_2 : T0Space β] (f : α → β),
  SeparationQuotient.lift' f = if hc : UniformContinuous f then SeparationQuotient.lift f ⋯ else fun x => f ⋯.some
-- Mathlib.Topology.Algebra.Valued.ValuedField
/-- The extension of the valuation of a valued field to the completion of the field.  -/
Valued.extension : {K : Type u_1} →
  [inst : Field K] →
    {Γ₀ : Type u_2} →
      [inst_1 : LinearOrderedCommGroupWithZero Γ₀] →
        [hv : Valued K Γ₀] → UniformSpace.Completion K → (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀
-- Mathlib.Analysis.Complex.Norm
Complex.nndist_of_re_eq : ∀ {z w : ℂ}, z.re = w.re → nndist z w = nndist z.im w.im
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RicSliceData.mk.injEq : ∀ {α : Type u} {β : Type v} [inst : Ord α] (treeMap : Std.DTreeMap.Internal.Impl α fun x => β) (range : Std.Ric α)
  (treeMap_1 : Std.DTreeMap.Internal.Impl α fun x => β) (range_1 : Std.Ric α),
  ({ treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 }) =
    (treeMap = treeMap_1 ∧ range = range_1)
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearMap.IsInvertible.inverse : ∀ {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace M₂]
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂] {f : M →L[R] M₂}, f.IsInvertible → f.inverse.IsInvertible
-- Mathlib.Topology.Category.TopCat.Limits.Pullbacks
TopCat.pullback_snd_range : ∀ {X Y S : TopCat} (f : X ⟶ S) (g : Y ⟶ S),
  Set.range ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.snd f g)) =
    {y | ∃ x, (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) y}
-- Std.Data.Internal.List.Associative
Std.Internal.List.DistinctKeys.insertListIfNew : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l₁ l₂ : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l₁ → Std.Internal.List.DistinctKeys (Std.Internal.List.insertListIfNew l₁ l₂)
-- Lean.Widget.UserWidget
Lean.Widget.GetWidgetSourceParams.mk : UInt64 → Lean.Lsp.Position → Lean.Widget.GetWidgetSourceParams
-- Mathlib.Topology.Bases
TopologicalSpace.instFirstCountableTopologyProd : ∀ {α : Type u} [t : TopologicalSpace α] {β : Type u_1} [inst : TopologicalSpace β] [FirstCountableTopology α]
  [FirstCountableTopology β], FirstCountableTopology (α × β)
-- Mathlib.Order.UpperLower.Hom
UpperSet.iciSupHom_apply : ∀ {α : Type u_1} [inst : SemilatticeSup α] (a : α), UpperSet.iciSupHom a = UpperSet.Ici a
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.SimpleFunc.setToL1SCLM_smul_left' : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T T' : Set α → E →L[ℝ] F} {C C' : ℝ} (c : ℝ) (hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
  (hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C'),
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T' s = c • T s) →
    ∀ (f : ↥(α →₁ₛ[μ] E)),
      (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT') f = c • (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT) f
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.addLECancellable_iff_ne_bot : ∀ {α : Type u} [inst : Add α] {x : WithBot α} [Nonempty α] [inst_2 : Preorder α] [AddLeftReflectLE α],
  AddLECancellable x ↔ x ≠ ⊥
-- Mathlib.Topology.Algebra.InfiniteSum.Module
/-- Automorphization of a function into an `R`-`Module` distributes, that is, commutes with the
`R`-scalar multiplication.  -/
QuotientGroup.automorphize_smul_left : ∀ {M : Type u_11} [inst : TopologicalSpace M] [inst_1 : AddCommMonoid M] [T2Space M] {R : Type u_12}
  [inst_3 : DivisionRing R] [inst_4 : Module R M] [ContinuousConstSMul R M] {G : Type u_13} [inst_6 : Group G]
  {Γ : Subgroup G} (f : G → M) (g : G ⧸ Γ → R),
  QuotientGroup.automorphize (g ∘ Quotient.mk' • f) = g • QuotientGroup.automorphize f
-- Mathlib.Data.Nat.Size
Nat.size_pos : ∀ {n : ℕ}, 0 < n.size ↔ 0 < n
-- Mathlib.Algebra.Order.BigOperators.Expect
/-- **Cauchy-Schwarz inequality** in terms of `Finset.expect`.  -/
Finset.expect_mul_sq_le_sq_mul_sq : ∀ {ι : Type u_1} {R : Type u_3} [inst : CommSemiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [ExistsAddOfLE R] [inst_4 : Module ℚ≥0 R] [PosSMulMono ℚ≥0 R] (s : Finset ι) (f g : ι → R),
  (s.expect fun i => f i * g i) ^ 2 ≤ (s.expect fun i => f i ^ 2) * s.expect fun i => g i ^ 2
-- Mathlib.Data.Finset.Sort
/-- Any increasing map `f` from `Fin k` to a finset of cardinality `k` has to coincide with
the increasing bijection `orderEmbOfFin s h`.  -/
Finset.orderEmbOfFin_unique : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Finset α} {k : ℕ} (h : s.card = k) {f : Fin k → α},
  (∀ (x : Fin k), f x ∈ s) → StrictMono f → f = ⇑(s.orderEmbOfFin h)
-- Mathlib.Topology.Order.LiminfLimsup
Monotone.liminf_nhdsLT_eq_iSup₂ : ∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [DenselyOrdered α] [inst_4 : CompleteLattice β] {f : α → β} [NoMinOrder α],
  Monotone f → ∀ (a : α), Filter.liminf f (nhdsWithin a (Set.Iio a)) = ⨆ r, ⨆ (_ : r < a), f r
-- ProofWidgets.Component.FilterDetails
ProofWidgets.FilterDetailsProps.mk : ProofWidgets.Html → ProofWidgets.Html → ProofWidgets.Html → Bool → ProofWidgets.FilterDetailsProps
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.coe_copy : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (Q : QuadraticMap R M N) (Q' : M → N) (h : Q' = ⇑Q),
  ⇑(Q.copy Q' h) = Q'
-- Std.Data.Iterators.Lemmas.Combinators.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.TakeWhile.0.Std.Iter.atIdxSlow?_eq_match.match_3.eq_1 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2) (it' : Std.Iter β) (out : β)
  (h_1 : (it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.Iter β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.yield it' out with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_1 it' out
-- Lean.Elab.InfoTree.Types
Lean.Elab.instInhabitedTermInfo : Inhabited Lean.Elab.TermInfo
-- Mathlib.LinearAlgebra.Projectivization.Subspace
Projectivization.Subspace.instPartialOrder : {K : Type u_1} →
  {V : Type u_2} →
    [inst : DivisionRing K] →
      [inst_1 : AddCommGroup V] → [inst_2 : Module K V] → PartialOrder (Projectivization.Subspace K V)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point.0.WeierstrassCurve.Affine.Point.add.match_1.eq_2 : ∀ {F : Type u_1} [inst : Field F] {W : WeierstrassCurve.Affine F} (motive : W.Point → W.Point → Sort u_2) (P : W.Point)
  (h_1 : (P : W.Point) → motive WeierstrassCurve.Affine.Point.zero P)
  (h_2 : (P : W.Point) → motive P WeierstrassCurve.Affine.Point.zero)
  (h_3 :
    (x₁ y₁ : F) →
      (h₁ : W.Nonsingular x₁ y₁) →
        (x₂ y₂ : F) →
          (h₂ : W.Nonsingular x₂ y₂) →
            motive (WeierstrassCurve.Affine.Point.some x₁ y₁ h₁) (WeierstrassCurve.Affine.Point.some x₂ y₂ h₂)),
  (P = WeierstrassCurve.Affine.Point.zero → False) →
    (match P, WeierstrassCurve.Affine.Point.zero with
      | WeierstrassCurve.Affine.Point.zero, P => h_1 P
      | P, WeierstrassCurve.Affine.Point.zero => h_2 P
      | WeierstrassCurve.Affine.Point.some x₁ y₁ h₁, WeierstrassCurve.Affine.Point.some x₂ y₂ h₂ =>
        h_3 x₁ y₁ h₁ x₂ y₂ h₂) =
      h_2 P
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- Composition by continuous linear maps on the right preserves `C^n` functions.  -/
ContDiff.comp_continuousLinearMap : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : WithTop ℕ∞} {f : E → F} {g : G →L[𝕜] E},
  ContDiff 𝕜 n f → ContDiff 𝕜 n (f ∘ ⇑g)
-- Mathlib.RingTheory.Coalgebra.Convolution
/-- Convolution algebra structure on linear maps from a coalgebra to an algebra.  -/
LinearMap.convAlgebra : {R : Type u_1} →
  {S : Type u_2} →
    {A : Type u_3} →
      {C : Type u_5} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Algebra R A] →
              [inst_3 : AddCommMonoid C] →
                [inst_4 : Module R C] →
                  [inst_5 : Coalgebra R C] →
                    [inst_6 : CommSemiring S] →
                      [inst_7 : Algebra S A] → [SMulCommClass R S A] → Algebra S (WithConv (C →ₗ[R] A))
-- Mathlib.Data.Matrix.Mul
zero_dotProduct' : ∀ {m : Type u_2} {α : Type v} [inst : Fintype m] [inst_1 : NonUnitalNonAssocSemiring α] (v : m → α),
  (fun x => 0) ⬝ᵥ v = 0
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instGroup : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [Group Y] → Group (LocallyConstant X Y)
-- Mathlib.NumberTheory.LucasLehmer
/-- A closed form for the recurrence relation.  -/
LucasLehmer.X.closed_form : ∀ {q : ℕ} (i : ℕ), ↑(LucasLehmer.s i) = LucasLehmer.X.ω ^ 2 ^ i + LucasLehmer.X.ωb ^ 2 ^ i
-- Mathlib.MeasureTheory.Function.UniformIntegrable
MeasureTheory.unifIntegrable_of_tendsto_Lp_zero : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {p : ENNReal} {f : ℕ → α → β},
  1 ≤ p →
    p ≠ ⊤ →
      (∀ (n : ℕ), MeasureTheory.MemLp (f n) p μ) →
        Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n) p μ) Filter.atTop (nhds 0) →
          MeasureTheory.UnifIntegrable f p μ
-- Mathlib.Algebra.Star.StarRingHom
NonUnitalStarRingHomClass.toStarHomClass : ∀ {F : Type u_1} {A : outParam (Type u_2)} {B : outParam (Type u_3)} {inst : NonUnitalNonAssocSemiring A}
  {inst_1 : Star A} {inst_2 : NonUnitalNonAssocSemiring B} {inst_3 : Star B} {inst_4 : FunLike F A B}
  {inst_5 : NonUnitalRingHomClass F A B} [self : NonUnitalStarRingHomClass F A B], StarHomClass F A B
-- Mathlib.GroupTheory.Commensurable
AddSubgroup.Commensurable.trans : ∀ {G : Type u_1} [inst : AddGroup G] {H K L : AddSubgroup G}, H.Commensurable K → K.Commensurable L → H.Commensurable L
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
/-- Auxiliary definition for `FreeMonoidalCategory.project`.  -/
CategoryTheory.FreeMonoidalCategory.projectMapAux : {C : Type u} →
  {D : Type u'} →
    [inst : CategoryTheory.Category.{v', u'} D] →
      [inst_1 : CategoryTheory.MonoidalCategory D] →
        (f : C → D) →
          {X Y : CategoryTheory.FreeMonoidalCategory C} →
            X.Hom Y →
              (CategoryTheory.FreeMonoidalCategory.projectObj f X ⟶ CategoryTheory.FreeMonoidalCategory.projectObj f Y)
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
/-- On square matrices, `mul_left_comm` applies under `det`.  -/
Matrix.det_mul_left_comm : ∀ {m : Type u_1} [inst : DecidableEq m] [inst_1 : Fintype m] {R : Type v} [inst_2 : CommRing R] (M N P : Matrix m m R),
  (M * (N * P)).det = (N * (M * P)).det
-- Mathlib.Combinatorics.Matroid.IndepAxioms
IndepMatroid.mk.sizeOf_spec : ∀ {α : Type u_2} [inst : SizeOf α] (E : Set α) (Indep : Set α → Prop) (indep_empty : Indep ∅)
  (indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I)
  (indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I))
  (indep_maximal : ∀ X ⊆ E, Matroid.ExistsMaximalSubsetProperty Indep X)
  (subset_ground : ∀ (I : Set α), Indep I → I ⊆ E),
  sizeOf
      { E := E, Indep := Indep, indep_empty := indep_empty, indep_subset := indep_subset, indep_aug := indep_aug,
        indep_maximal := indep_maximal, subset_ground := subset_ground } =
    1 + sizeOf indep_empty
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.fromSpec_image_basicOpen : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U)
  (f : ↑(X.presheaf.obj (Opposite.op U))),
  (AlgebraicGeometry.Scheme.Hom.opensFunctor hU.fromSpec).obj (PrimeSpectrum.basicOpen f) = X.basicOpen f
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem?_inter_of_not_mem_left : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∉ m₁ → (m₁ ∩ m₂)[k]? = none
-- Mathlib.RingTheory.Congruence.Basic
RingCon.instNontrivial : ∀ {R : Type u_3} [inst : Add R] [inst_1 : Mul R] [Nontrivial R], Nontrivial (RingCon R)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.instZeroHom.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (G H : CategoryTheory.AddGrp C),
  G.instZeroHom H =
    {
      zero :=
        CategoryTheory.AddGrp.homMk
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit G.X)
            CategoryTheory.AddMonObj.zero) }
-- Mathlib.Order.Circular
/-- **Alias** of `not_sbtw_of_btw`. -/
Btw.btw.not_sbtw : ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, btw a b c → ¬sbtw c b a
-- Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
/-- For `1 ≤ r`, the characteristic function for the poles of `f * g` is less than or equal to the sum
of the characteristic functions for the poles of `f` and `g`, respectively.
 -/
ValueDistribution.characteristic_mul_top_le : ∀ {f₁ f₂ : ℂ → ℂ} {r : ℝ},
  1 ≤ r →
    Meromorphic f₁ →
      (∀ (z : ℂ), meromorphicOrderAt f₁ z ≠ ⊤) →
        Meromorphic f₂ →
          (∀ (z : ℂ), meromorphicOrderAt f₂ z ≠ ⊤) →
            ValueDistribution.characteristic (f₁ * f₂) ⊤ r ≤
              (ValueDistribution.characteristic f₁ ⊤ + ValueDistribution.characteristic f₂ ⊤) r
-- Mathlib.LinearAlgebra.SymplecticGroup
SymplecticGroup.symplectic_det : ∀ {l : Type u_1} {R : Type u_2} [inst : DecidableEq l] [inst_1 : Fintype l] [inst_2 : CommRing R]
  {A : Matrix (l ⊕ l) (l ⊕ l) R}, A ∈ Matrix.symplecticGroup l R → IsUnit A.det
-- Mathlib.Data.Nat.Cast.Order.Ring
Nat.cast_max : ∀ {α : Type u_3} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (m n : ℕ), ↑(max m n) = max ↑m ↑n
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.L1.SimpleFunc.integrable : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {μ : MeasureTheory.Measure α}
  (f : ↥(α →₁ₛ[μ] E)), MeasureTheory.Integrable (⇑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f)) μ
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.map.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N) (S : Subsemigroup M),
  Subsemigroup.map f S = { carrier := ⇑f '' ↑S, mul_mem' := ⋯ }
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.sin_eq_iff_eq_or_add_eq_pi : ∀ {θ ψ : Real.Angle}, θ.sin = ψ.sin ↔ θ = ψ ∨ θ + ψ = ↑Real.pi
-- Mathlib.Topology.Separation.Basic
/-- **Alias** of `Ne.nhdsWithin_sdiff_singleton`. -/
Ne.nhdsWithin_diff_singleton : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {x y : X},
  x ≠ y → ∀ (s : Set X), nhdsWithin x (s \ {y}) = nhdsWithin x s
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.Red.Step.diamond_aux : ∀ {α : Type u} {L₁ L₂ L₃ L₄ : List (α × Bool)} {x1 : α} {b1 : Bool} {x2 : α} {b2 : Bool},
  L₁ ++ (x1, b1) :: (x1, !b1) :: L₂ = L₃ ++ (x2, b2) :: (x2, !b2) :: L₄ →
    L₁ ++ L₂ = L₃ ++ L₄ ∨ ∃ L₅, FreeGroup.Red.Step (L₁ ++ L₂) L₅ ∧ FreeGroup.Red.Step (L₃ ++ L₄) L₅
-- Mathlib.RingTheory.OreLocalization.NonZeroDivisors
OreLocalization.nontrivial_of_nonZeroDivisorsLeft : ∀ {R : Type u_1} [inst : MonoidWithZero R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] [Nontrivial R],
  S ≤ nonZeroDivisorsLeft R → Nontrivial (OreLocalization S R)
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- The language of a set of configurations `X` on a finite shape `U`.

This is the set of all finite patterns obtained by restricting some configuration
`x ∈ X` to `U`.  -/
SymbolicDynamics.FullShift.LanguageOn : {A : Type u_1} →
  [inst : Inhabited A] → {G : Type u_2} → Set (G → A) → Finset G → Set (SymbolicDynamics.FullShift.Pattern A G)
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.LocallyIntegrableOn.integrableOn_compact_subset : ∀ {X : Type u_1} {ε : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace ε]
  [inst_3 : ContinuousENorm ε] {f : X → ε} {μ : MeasureTheory.Measure X} {s : Set X}
  [TopologicalSpace.PseudoMetrizableSpace ε],
  MeasureTheory.LocallyIntegrableOn f s μ → ∀ {t : Set X}, t ⊆ s → IsCompact t → MeasureTheory.IntegrableOn f t μ
-- Mathlib.Data.Seq.Parallel
_private.Mathlib.Data.Seq.Parallel.0.Computation.Corec.f.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : α ⊕ β → Sort u_3) (val : β) (h_1 : (a : α) → motive (Sum.inl a))
  (h_2 : (val : β) → motive (Sum.inr val)),
  (match Sum.inr val with
    | Sum.inl a => h_1 a
    | Sum.inr val => h_2 val) =
    h_2 val
-- Mathlib.ModelTheory.Substructures
/-- The substructure of elements `x : M` such that `f x = g x`  -/
FirstOrder.Language.Hom.eqLocus : {L : FirstOrder.Language} →
  {M : Type w} →
    {N : Type u_1} → [inst : L.Structure M] → [inst_1 : L.Structure N] → L.Hom M N → L.Hom M N → L.Substructure M
-- Lean.Meta.Tactic.Grind.SimpUtil
Lean.Meta.Grind.simpEq : Lean.Meta.Simp.Simproc
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
AlgebraicIndependent.isAlgebraic_adjoin_iff_of_matroid_isBasis : ∀ {R : Type u_1} {A : Type w} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : FaithfulSMul R A] [inst_4 : NoZeroDivisors A] {s t : Set A} {a : A},
  (AlgebraicIndependent.matroid R A).IsBasis s t →
    (IsAlgebraic (↥(Algebra.adjoin R s)) a ↔ IsAlgebraic (↥(Algebra.adjoin R t)) a)
-- Mathlib.FieldTheory.CardinalEmb
Field.Emb.Cardinal.instInverseSystemWithTopToTypeOrdRankAlgHomSubtypeMemIntermediateFieldCoeOrderEmbeddingFiltrationAlgebraicClosureEmbFunctor : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  [rank_inf : Fact (Cardinal.aleph0 ≤ Module.rank F E)] [inst_3 : Algebra.IsAlgebraic F E],
  InverseSystem (Field.Emb.Cardinal.embFunctor F E)
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.isoMk_hom_τ₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (e₁ : S₁.X₁ ≅ S₂.X₁) (e₂ : S₁.X₂ ≅ S₂.X₂) (e₃ : S₁.X₃ ≅ S₂.X₃)
  (comm₁₂ :
    autoParam (CategoryTheory.CategoryStruct.comp e₁.hom S₂.f = CategoryTheory.CategoryStruct.comp S₁.f e₂.hom)
      CategoryTheory.ShortComplex.isoMk._auto_1)
  (comm₂₃ :
    autoParam (CategoryTheory.CategoryStruct.comp e₂.hom S₂.g = CategoryTheory.CategoryStruct.comp S₁.g e₃.hom)
      CategoryTheory.ShortComplex.isoMk._auto_3),
  (CategoryTheory.ShortComplex.isoMk e₁ e₂ e₃ comm₁₂ comm₂₃).hom.τ₂ = e₂.hom
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.T_eval_one : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ), Polynomial.eval 1 (Polynomial.Chebyshev.T R n) = 1