mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.symm_toCoalgHom : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B] (e : A ≃ₗc[R] B), ↑↑e.symm = ↑e.toLinearEquiv.symm
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupNorm.instSemilatticeSup : {E : Type u_3} → [inst : AddGroup E] → SemilatticeSup (AddGroupNorm E)
-- Mathlib.Algebra.Module.Projective
Module.instProjectiveProd : ∀ {R : Type u_1} [inst : Semiring R] {P : Type u_2} [inst_1 : AddCommMonoid P] [inst_2 : Module R P] {Q : Type u_5}
  [inst_3 : AddCommMonoid Q] [inst_4 : Module R Q] [Module.Projective R P] [Module.Projective R Q],
  Module.Projective R (P × Q)
-- Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
MeasureTheory.meas_ge_le_mul_pow_eLpNorm_enorm : ∀ {α : Type u_1} {ε' : Type u_3} {m0 : MeasurableSpace α} [inst : TopologicalSpace ε'] [inst_1 : ContinuousENorm ε']
  {p : ENNReal} (μ : MeasureTheory.Measure α),
  p ≠ 0 →
    p ≠ ⊤ →
      ∀ {f : α → ε'},
        MeasureTheory.AEStronglyMeasurable f μ →
          ∀ {ε : ENNReal},
            ε ≠ 0 →
              (ε = ⊤ → μ {x | ‖f x‖ₑ = ⊤} = 0) →
                μ {x | ε ≤ ‖f x‖ₑ} ≤ ε⁻¹ ^ p.toReal * MeasureTheory.eLpNorm f p μ ^ p.toReal
-- Lean.Elab.Match
_private.Lean.Elab.Match.0.Lean.Elab.Term.ToDepElimPattern.main.pack : Array Lean.Expr → Array Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.adjoin_le_iff : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A] {S : NonUnitalStarSubalgebra R A} {s : Set A}, NonUnitalStarAlgebra.adjoin R s ≤ S ↔ s ⊆ ↑S
-- Init.Prelude
ShiftLeft.mk : {α : Type u} → (α → α → α) → ShiftLeft α
-- Mathlib.CategoryTheory.Sites.Coherent.Equivalence
/-- Equivalent preregular categories give equivalent regular toposes.
 -/
CategoryTheory.Equivalence.sheafCongrPreregular : {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] →
        [inst_2 : CategoryTheory.Preregular C] →
          (A : Type u_3) →
            [inst_3 : CategoryTheory.Category.{v_3, u_3} A] →
              (e : C ≌ D) →
                CategoryTheory.Sheaf (CategoryTheory.regularTopology C) A ≌
                  CategoryTheory.Sheaf (CategoryTheory.regularTopology D) A
-- Init.Data.String.Iterate
String.Slice.PosIterator.instFiniteSubtypePosNeEndPos : ∀ {m : Type → Type u_1} {s : String.Slice} [inst : Pure m], Std.Iterators.Finite s.PosIterator m
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
WithBot.sInf_empty : ∀ (α : Type u_5) [inst : CompleteLattice α], sInf ∅ = ⊤
-- Std.Async.System
Std.Async.System.OSInfo.mk : String → String → String → String → Std.Async.System.OSInfo
-- Lean.Meta.Sym.Arith.Types
/-- Classification state for a type with a `CommRing` instance.  -/
Lean.Meta.Sym.Arith.CommRing : Type
-- Lean.Meta.Eqns
/-- Throw an error if names for equation theorems for `declName` are not available.
 -/
Lean.Meta.ensureEqnReservedNamesAvailable : Lean.Name → Lean.CoreM Unit
-- Mathlib.Algebra.GroupWithZero.Basic
/-- Multiplying `a` by itself and then by its inverse results in `a`
(whether or not `a` is zero).  -/
mul_self_mul_inv : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] (a : G₀), a * a * a⁻¹ = a
-- Mathlib.Analysis.Normed.Lp.lpHolder
lp.holderₗ.congr_simp : ∀ {ι : Type u_1} {𝕜 : Type u_2} {E : ι → Type u_3} {F : ι → Type u_4} {G : ι → Type u_5} [inst : RCLike 𝕜]
  [inst_1 : (i : ι) → NormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : (i : ι) → NormedAddCommGroup (F i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (F i)]
  [inst_5 : (i : ι) → NormedAddCommGroup (G i)] [inst_6 : (i : ι) → NormedSpace 𝕜 (G i)] {p q : ENNReal} (r : ENNReal)
  [hpqr : p.HolderTriple q r] (B B_1 : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i) (e_B : B = B_1) {K K_1 : ℝ} (e_K : K = K_1)
  (hBK : ∀ (i : ι), ‖B i‖ ≤ K), lp.holderₗ r B hBK = lp.holderₗ r B_1 ⋯
-- Std.Data.HashMap.Lemmas
Std.HashMap.get_diff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {h_mem : k ∈ m₁ \ m₂}, (m₁ \ m₂).get k h_mem = m₁.get k ⋯
-- Init.Data.UInt.Lemmas
UInt16.toNat.eq_1 : ∀ (n : UInt16), n.toNat = n.toBitVec.toNat
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
NumberField.mixedEmbedding.convexBodyLT'Factor.congr_simp : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.mixedEmbedding.convexBodyLT'Factor K = NumberField.mixedEmbedding.convexBodyLT'Factor K
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- If `f : M →+ N` is a Localization map for a Submonoid `S` and `k : N ≃+ P` is an isomorphism
of `AddCommMonoid`s, `k ∘ f` is a Localization map for `M` at `S`.  -/
AddSubmonoid.LocalizationMap.ofAddEquivOfLocalizations : {M : Type u_1} →
  [inst : AddCommMonoid M] →
    {S : AddSubmonoid M} →
      {N : Type u_2} →
        [inst_1 : AddCommMonoid N] →
          {P : Type u_3} → [inst_2 : AddCommMonoid P] → S.LocalizationMap N → N ≃+ P → S.LocalizationMap P
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.condIndepSet_empty_left : ∀ {Ω : Type u_1} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω}
  [inst_1 : MeasureTheory.IsFiniteMeasure μ] (s : Set Ω), ProbabilityTheory.CondIndepSet m' hm' ∅ s μ
-- Std.Do.SPred.Laws
Std.Do.SPred.instTransBientails : {σs : List (Type u)} → Trans Std.Do.SPred.bientails Std.Do.SPred.bientails Std.Do.SPred.bientails
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.IsLittleO.smul : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {R : Type u_13} {𝕜' : Type u_16} [inst : SeminormedAddCommGroup E']
  [inst_1 : SeminormedAddCommGroup F'] [inst_2 : SeminormedRing R] [inst_3 : NormedDivisionRing 𝕜'] {f' : α → E'}
  {g' : α → F'} {l : Filter α} [inst_4 : Module R E'] [IsBoundedSMul R E'] [inst_6 : Module 𝕜' F'] [NormSMulClass 𝕜' F']
  {k₁ : α → R} {k₂ : α → 𝕜'}, k₁ =o[l] k₂ → f' =o[l] g' → (fun x => k₁ x • f' x) =o[l] fun x => k₂ x • g' x
-- Mathlib.Data.Set.Prod
Set.prod_subset_preimage_fst : ∀ {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β), s ×ˢ t ⊆ Prod.fst ⁻¹' s
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.minimalPeriod_iterate_eq_div_gcd' : ∀ {α : Type u_1} {f : α → α} {x : α} {n : ℕ},
  x ∈ Function.periodicPts f →
    Function.minimalPeriod f^[n] x = Function.minimalPeriod f x / (Function.minimalPeriod f x).gcd n
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.Mod.instInhabited : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (A : C) → [inst_2 : CategoryTheory.MonObj A] → Inhabited (CategoryTheory.Mod C A)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.FoldingRangeKind.comment.sizeOf_spec : sizeOf Lean.Lsp.FoldingRangeKind.comment = 1
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Stream.toList_nil : ∀ {α : Type u_1}, RBTree.RBNode.Stream.nil.toList = []
-- Mathlib.Algebra.Torsor.Defs
/-- Multiplying a group element with the point `p` is an injective function.  -/
smul_right_injective' : ∀ {G : Type u_1} {P : Type u_2} [inst : Group G] [T : Torsor G P] (p : P), Function.Injective fun x => x • p
-- Mathlib.Order.Lattice
SemilatticeInf.toMin : {α : Type u} → [SemilatticeInf α] → Min α
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.MapEq.w : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : Type w} [inst_1 : LinearOrder K] {x : K}
  (F G : CategoryTheory.Functor (↑(Set.Iic x)) C) {k₁ k₂ : K} {h₁₂ : k₁ ≤ k₂} {h₂ : k₂ ≤ x}
  (h : CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.MapEq F G k₁ k₂ h₁₂ h₂),
  F.map (CategoryTheory.homOfLE h₁₂) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.homOfLE h₁₂)) (CategoryTheory.eqToHom ⋯))
-- Mathlib.Probability.Kernel.Condexp
/-- Auxiliary lemma for `condExp_ae_eq_trim_integral_condExpKernel`.  -/
ProbabilityTheory.condExp_ae_eq_trim_integral_condExpKernel_of_stronglyMeasurable : ∀ {Ω : Type u_1} {F : Type u_2} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [inst : StandardBorelSpace Ω]
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] [inst_2 : NormedAddCommGroup F] {f : Ω → F}
  [inst_3 : NormedSpace ℝ F] [CompleteSpace F] (hm : m ≤ mΩ),
  MeasureTheory.StronglyMeasurable f →
    MeasureTheory.Integrable f μ →
      μ[f | m] =ᵐ[μ.trim hm] fun ω => ∫ (y : Ω), f y ∂(ProbabilityTheory.condExpKernel μ m) ω
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.leadingCoeff_zero : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : LinearOrder B] [inst_2 : OrderBot B]
  {D : A → B} [inst_3 : Nonempty A], AddMonoidAlgebra.leadingCoeff D 0 = 0
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.ext : ∀ {ι : Type u_1} {M : ι → Type u_2} {inst : (i : ι) → Monoid (M i)} {x y : Monoid.CoprodI.Word M},
  x.toList = y.toList → x = y
-- Mathlib.Analysis.Convex.Continuous
ConvexOn.continuousOn_Ici : ∀ {f : ℝ → ℝ} {y : ℝ}, ConvexOn ℝ (Set.Ici y) f → ContinuousWithinAt f (Set.Ici y) y → ContinuousOn f (Set.Ici y)
-- Mathlib.Algebra.Category.Ring.Under.Limits
CommRingCat.Under.equalizer_comp : ∀ {R : CommRingCat} {A B : CategoryTheory.Under R} (f g : A ⟶ B),
  CategoryTheory.CategoryStruct.comp ((CommRingCat.toAlgHom f).equalizer (CommRingCat.toAlgHom g)).val.toUnder f =
    CategoryTheory.CategoryStruct.comp ((CommRingCat.toAlgHom f).equalizer (CommRingCat.toAlgHom g)).val.toUnder g
-- Mathlib.Geometry.Convex.Set
Convexity.IsConvexSet.inter : ∀ {R : Type u_3} {X : Type u_5} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X] {s t : Set X},
  Convexity.IsConvexSet R s → Convexity.IsConvexSet R t → Convexity.IsConvexSet R (s ∩ t)
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mfderivWithin_comp_of_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [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'] {E'' : Type u_8}
  [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace 𝕜 E''] {H'' : Type u_9} [inst_13 : TopologicalSpace H'']
  {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M'']
  {f : M → M'} {s : Set M} {g : M' → M''} {u : Set M'} {x : M} {y : M'},
  MDiffAt[u] g y →
    MDiffAt[s] f x →
      s ⊆ f ⁻¹' u → UniqueMDiffAt[s] x → f x = y → mfderiv[s] (g ∘ f) x = mfderiv[u] g y ∘SL mfderiv[s] f x
-- Mathlib.Order.WellFounded
WellFounded.not_rel_apply_succ : ∀ {α : Type u_1} {r : α → α → Prop} [h : IsWellFounded α r] (f : ℕ → α), ∃ n, ¬r (f (n + 1)) (f n)
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsClosedSubgraph.trans : ∀ {α : Type u_1} {β : Type u_2} {G G₁ G₂ : Graph α β},
  G.IsClosedSubgraph G₁ → G₁.IsClosedSubgraph G₂ → G.IsClosedSubgraph G₂
-- Init.Data.List.Notation
/-- Auxiliary syntax for implementing `[$elem,*]` list literal syntax.
The syntax `%[a,b,c|tail]` constructs a value equivalent to `a::b::c::tail`.
It uses binary partitioning to construct a tree of intermediate let bindings as in
`let left := [d, e, f]; a :: b :: c :: left` to avoid creating very deep expressions.
 -/
«term%[_|_]» : Lean.ParserDescr
-- Mathlib.Order.Hom.CompleteLattice
FrameHom.toFun_eq_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : FrameHom α β), f.toFun = ⇑f
-- Mathlib.Topology.UniformSpace.AbstractCompletion
AbstractCompletion.mk : {α : Type u} →
  [inst : UniformSpace α] →
    (space : Type v) →
      (coe : α → space) →
        (uniformStruct : UniformSpace space) →
          CompleteSpace space → T0Space space → IsUniformInducing coe → DenseRange coe → AbstractCompletion.{v, u} α
-- Mathlib.Analysis.CStarAlgebra.Classes
CommCStarAlgebra.toCStarRing : ∀ {A : Type u_1} [self : CommCStarAlgebra A], CStarRing A
-- Mathlib.NumberTheory.Divisors
Nat.pos_of_mem_properDivisors : ∀ {n m : ℕ}, m ∈ n.properDivisors → 0 < m
-- Mathlib.LinearAlgebra.Contraction
/-- If `M` is free, the natural linear map $M^* ⊗ N → Hom(M, N)$ is an equivalence. This function
provides this equivalence in return for a basis of `M`.  -/
dualTensorHomEquivOfBasis : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : AddCommMonoid N] →
              [inst_3 : Module R M] →
                [inst_4 : Module R N] →
                  Module.Basis ι R M →
                    [DecidableEq ι] → [Fintype ι] → TensorProduct R (Module.Dual R M) N ≃ₗ[R] M →ₗ[R] N
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
/-- The residue of `Λ` at `s = k` is equal to `ε • g₀`.  -/
WeakFEPair.Λ_residue_k : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (P : WeakFEPair E),
  Filter.Tendsto (fun s => (s - ↑P.k) • P.Λ s) (nhdsWithin ↑P.k {↑P.k}ᶜ) (nhds (P.ε • P.g₀))
-- Mathlib.Algebra.Group.Action.Defs
/-- An action of `M` on `α` and a function `N → M` induces an action of `N` on `α`.  -/
SMul.comp : {M : Type u_1} → {N : Type u_2} → (α : Type u_5) → [SMul M α] → (N → M) → SMul N α
-- Mathlib.Algebra.Algebra.Basic
/-- If `E` is an `F`-algebra, and there exists an injective `F`-linear map from `F` to `E`,
then the algebra map from `F` to `E` is also injective.  -/
injective_algebraMap_of_linearMap : ∀ {F : Type u_1} {E : Type u_2} [inst : CommSemiring F] [inst_1 : Semiring E] [inst_2 : Algebra F E] (b : F →ₗ[F] E),
  Function.Injective ⇑b → Function.Injective ⇑(algebraMap F E)
-- Init.Data.Ord.Basic
List.compare_eq_compareLex : ∀ {α : Type u_1} [inst : Ord α], compare = List.compareLex compare
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
/-- If `C` has all limits of diagrams `cospan f g`, then it has all pullbacks  -/
CategoryTheory.Limits.hasPullbacks_of_hasLimit_cospan : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C]
  [∀ {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}, CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.cospan f g)],
  CategoryTheory.Limits.HasPullbacks C
-- Mathlib.Algebra.Homology.Functor
HomologicalComplex.quasiIsoAt_iff_evaluation : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {V : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} V] [inst_2 : CategoryTheory.Abelian V] {ι : Type u_3}
  {c : ComplexShape ι} {K₁ K₂ : HomologicalComplex (CategoryTheory.Functor T V) c} (f : K₁ ⟶ K₂) (i : ι),
  QuasiIsoAt f i ↔ ∀ (t : T), QuasiIsoAt ((((CategoryTheory.evaluation T V).obj t).mapHomologicalComplex c).map f) i
-- Mathlib.Order.Monotone.MonovaryOrder
monovaryOn_iff_exists_antitoneOn : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : ι → α} {g : ι → β}
  {s : Set ι}, MonovaryOn f g s ↔ ∃ x, AntitoneOn f s ∧ AntitoneOn g s
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.iCondIndepFun.condIndepFun_finsetSum_of_notMem : ∀ {Ω : Type u_1} {ι : Type u_2} {β : Type u_3} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {m : MeasurableSpace β}
  [inst_2 : AddCommMonoid β] [MeasurableAdd₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iCondIndepFun m' hm' f μ →
    (∀ (i : ι), Measurable (f i)) →
      ∀ {s : Finset ι} {i : ι}, i ∉ s → ProbabilityTheory.CondIndepFun m' hm' (∑ j ∈ s, f j) (f i) μ
-- Lean.Meta.Tactic.Util
Lean.Meta.throwTacticEx : {α : Type} → Lean.Name → Lean.MVarId → optParam (Option Lean.MessageData) none → Lean.MetaM α
-- Mathlib.Data.Fin.Rev
Fin.lt_rev_iff : ∀ {n : ℕ} {i j : Fin n}, i < j.rev ↔ j < i.rev
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.forM.eq_1 : ∀ {α : Type u} {β : α → Type v} {m : Type u_1 → Type u_2} [inst : Monad m] (f : (a : α) → β a → m PUnit.{u_1 + 1})
  (t : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.forM f t = Std.DTreeMap.Internal.Impl.foldlM (fun x k v => f k v) PUnit.unit t
-- Init.Prelude
/-- Bijection between `α` and `PULift.{v} α`  -/
PULift.up_down : ∀ {α : Sort u} (b : PULift α), { down := b.down } = b
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.sum_add_sum : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {ι : Type u_8} (μ ν : ι → MeasureTheory.Measure α),
  MeasureTheory.Measure.sum μ + MeasureTheory.Measure.sum ν = MeasureTheory.Measure.sum fun n => μ n + ν n
-- Mathlib.NumberTheory.ArithmeticFunction.Zeta
ArithmeticFunction.ppow_succ : ∀ {R : Type u_1} [inst : Semiring R] {f : ArithmeticFunction R} {k : ℕ} {kpos : 0 < k},
  f.ppow (k + 1) = (f.ppow k).pmul f
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.Turing.TM2.SupportsStmt.match_1.eq_3 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (motive : Turing.TM2.Stmt Γ Λ σ → Sort u_5) (k : K)
  (a : σ → Option (Γ k) → σ) (q : Turing.TM2.Stmt Γ Λ σ)
  (h_1 : (k : K) → (a : σ → Γ k) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.push k a q))
  (h_2 : (k : K) → (a : σ → Option (Γ k) → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.peek k a q))
  (h_3 : (k : K) → (a : σ → Option (Γ k) → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.pop k a q))
  (h_4 : (a : σ → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.load a q))
  (h_5 : (a : σ → Bool) → (q₁ q₂ : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.branch a q₁ q₂))
  (h_6 : (l : σ → Λ) → motive (Turing.TM2.Stmt.goto l)) (h_7 : Unit → motive Turing.TM2.Stmt.halt),
  (match Turing.TM2.Stmt.pop k a q with
    | Turing.TM2.Stmt.push k a q => h_1 k a q
    | Turing.TM2.Stmt.peek k a q => h_2 k a q
    | Turing.TM2.Stmt.pop k a q => h_3 k a q
    | Turing.TM2.Stmt.load a q => h_4 a q
    | Turing.TM2.Stmt.branch a q₁ q₂ => h_5 a q₁ q₂
    | Turing.TM2.Stmt.goto l => h_6 l
    | Turing.TM2.Stmt.halt => h_7 ()) =
    h_3 k a q
-- Mathlib.Order.Category.NonemptyFinLinOrd
NonemptyFinLinOrd.fintype : (self : NonemptyFinLinOrd) → Fintype ↑self.toLinOrd
-- Mathlib.Algebra.Module.Basic
invOf_two_smul_add_invOf_two_smul : ∀ {M : Type u_3} (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Invertible 2] (x : M), ⅟2 • x + ⅟2 • x = x
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.orderBot : OrderBot Cardinal.{u}
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.instHashableExpr_lean : Hashable Lean.Grind.Linarith.Expr
-- Mathlib.Algebra.Polynomial.Module.AEval
/-- The canonical linear equivalence between `M` and `Module.AEval R M a` as an `R`-module.
 -/
Module.AEval.of : (R : Type u_1) →
  {A : Type u_2} →
    (M : Type u_3) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          (a : A) →
            [inst_2 : Algebra R A] →
              [inst_3 : AddCommMonoid M] →
                [inst_4 : Module A M] →
                  [inst_5 : Module R M] → [inst_6 : IsScalarTower R A M] → M ≃ₗ[R] Module.AEval R M a
-- Init.Data.Range.Polymorphic.PRange
Std.Roc.mk.inj : ∀ {α : Type u} {lower upper lower_1 upper_1 : α},
  ((lower<...=upper) = lower_1<...=upper_1) → lower = lower_1 ∧ upper = upper_1
-- Init.Data.Option.Attach
Option.get_attach : ∀ {α : Type u_1} {o : Option α} (h : o.attach.isSome = true), o.attach.get h = ⟨o.get ⋯, ⋯⟩
-- Mathlib.Algebra.BigOperators.Ring.List
/-- If zero is an element of a list `l`, then `List.prod l = 0`. If the domain is a nontrivial
monoid with zero with no zero divisors, then this implication becomes an `iff`, see
`List.prod_eq_zero_iff`.  -/
List.prod_eq_zero : ∀ {M₀ : Type u_4} [inst : MonoidWithZero M₀] {l : List M₀}, 0 ∈ l → l.prod = 0
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
AlgebraicGeometry.Proj.germ_map_sectionInBasicOpen : ∀ {A B σ τ : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] [inst_3 : CommRing B]
  [inst_4 : SetLike τ B] [inst_5 : AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [inst_6 : GradedRing 𝒜]
  [inst_7 : GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ)
  (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜))
  {p : ProjectiveSpectrum ℬ}
  (c :
    HomogeneousLocalization.NumDenSameDeg 𝒜
      ((AlgebraicGeometry.ProjectiveSpectrum.comap f hf) p).asHomogeneousIdeal.toIdeal.primeCompl),
  (CategoryTheory.ConcreteCategory.hom
        ((AlgebraicGeometry.Proj.toSheafedSpace ℬ).presheaf.germ
          ((TopologicalSpace.Opens.map (AlgebraicGeometry.Proj.sheafedSpaceMap f hf).hom.base).obj
            (Opposite.unop (Opposite.op (ProjectiveSpectrum.basicOpen 𝒜 ↑c.den))))
          p ⋯))
      ((CategoryTheory.ConcreteCategory.hom
          ((AlgebraicGeometry.Proj.sheafedSpaceMap f hf).hom.c.app
            (Opposite.op (ProjectiveSpectrum.basicOpen 𝒜 ↑c.den))))
        (AlgebraicGeometry.sectionInBasicOpen 𝒜 ((AlgebraicGeometry.ProjectiveSpectrum.comap f hf) p) c)) =
    (CategoryTheory.ConcreteCategory.hom
        ((AlgebraicGeometry.Proj.toSheafedSpace ℬ).presheaf.germ (ProjectiveSpectrum.basicOpen ℬ (f ↑c.den)) p ⋯))
      (AlgebraicGeometry.sectionInBasicOpen ℬ p (HomogeneousLocalization.NumDenSameDeg.map f ⋯ c))
-- Init.Data.Ord.Basic
/-- Constructs an `LE` instance from an `Ord` instance.
 -/
Ord.toLE : {α : Type u_1} → Ord α → LE α
-- Mathlib.RingTheory.TensorProduct.Finite
Algebra.TensorProduct.cancelBaseChange.congr_simp : ∀ (R : Type uR) (S : Type uS) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (T : Type u_3)
  (A : Type u_4) (B : Type u_5) [inst_3 : CommSemiring T] [inst_4 : CommSemiring A] [inst_5 : CommSemiring B]
  [inst_6 : Algebra R T] [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : Algebra T A]
  [inst_10 : IsScalarTower R T A] [inst_11 : Algebra S A] [inst_12 : IsScalarTower R S A] [inst_13 : Algebra S T]
  [inst_14 : IsScalarTower S T A],
  Algebra.TensorProduct.cancelBaseChange R S T A B = Algebra.TensorProduct.cancelBaseChange R S T A B
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.State.addAtom.congr_simp : ∀ {aig : Std.Sat.AIG ℕ} {a a_1 : ℕ} (e_a : a = a_1) (state : Std.Sat.AIG.toCNF.State✝ aig) (idx : ℕ)
  (h : idx < aig.decls.size) (htip : aig.decls[idx] = Std.Sat.AIG.Decl.atom a),
  Std.Sat.AIG.toCNF.State.addAtom✝ state idx h htip = Std.Sat.AIG.toCNF.State.addAtom✝ state idx h ⋯
-- Std.Http.Data.Method
/-- Reorder members of a collection.
Source: https://www.rfc-editor.org/rfc/rfc3648#section-7
 -/
Std.Http.Method.orderpatch : Std.Http.Method
-- Mathlib.GroupTheory.FiniteAbelian.Duality
CommGroup.apply_monoidHomMonoidHomEquiv : ∀ {G : Type u_1} (M : Type u_2) [inst : CommGroup G] [inst_1 : Finite G] [inst_2 : CommMonoid M]
  [hM : HasEnoughRootsOfUnity M (Monoid.exponent G)] (φ : G →* Mˣ) (η : (G →* Mˣ) →* Mˣ),
  φ ((CommGroup.monoidHomMonoidHomEquiv G M) η) = η φ
-- Mathlib.CategoryTheory.Sites.Whiskering
/-- For every sheaf `P`, `P ⋙ F` is a sheaf.  -/
CategoryTheory.GrothendieckTopology.HasSheafCompose.isSheaf : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {A : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} A}
  {B : Type u₃} {inst_2 : CategoryTheory.Category.{v₃, u₃} B} {J : CategoryTheory.GrothendieckTopology C}
  {F : CategoryTheory.Functor A B} [self : J.HasSheafCompose F] (P : CategoryTheory.Functor Cᵒᵖ A),
  CategoryTheory.Presheaf.IsSheaf J P → CategoryTheory.Presheaf.IsSheaf J (P.comp F)