mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Ring.IsFormallyReal
/-- **Alias** of the reverse direction of `isSumNonzeroSq_iff_isSumSq`. -/
IsSumSq.isSumNonzeroSq_of_ne_zero : ∀ {R : Type u_1} [inst : NonUnitalNonAssocSemiring R] {s : R}, s ≠ 0 → IsSumSq s → IsSumNonzeroSq s
-- Mathlib.Topology.IsLocalHomeomorph
/-- Proves that `f` satisfies `IsLocalHomeomorphOn f s`. The condition `h` is weaker than the
definition of `IsLocalHomeomorphOn f s`, since it only requires `e : OpenPartialHomeomorph X Y` to
agree with `f` on its source `e.source`, as opposed to on the whole space `X`.  -/
IsLocalHomeomorphOn.mk : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y) (s : Set X),
  (∀ x ∈ s, ∃ e, x ∈ e.source ∧ Set.EqOn f (↑e) e.source) → IsLocalHomeomorphOn f s
-- Init.Data.Slice.Notation
/-- Slices `carrier` with no bounds.
   -/
Std.Rii.Sliceable.mkSlice : {α : Type u} → {β : outParam (Type v)} → {γ : outParam (Type w)} → [self : Std.Rii.Sliceable α β γ] → α → Std.Rii β → γ
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKey!_modify_self : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited α] {k : α} {f : β → β},
  m.WF → (Std.DHashMap.Raw.Const.modify m k f).getKey! k = if k ∈ m then k else default
-- Batteries.Logic
/-- If all points are equal to a given point `x`, then `α` is a subsingleton.  -/
subsingleton_of_forall_eq : ∀ {α : Sort u_1} (x : α), (∀ (y : α), y = x) → Subsingleton α
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Functor.IsLocalization.mk' : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) (h₁ : CategoryTheory.Localization.StrictUniversalPropertyFixedTarget L W D)
  (h₂ : CategoryTheory.Localization.StrictUniversalPropertyFixedTarget L W W.Localization), L.IsLocalization W
-- Std.Data.DHashMap.Basic
/-- Checks if a mapping for the given key exists and returns the key-value pair if it does, otherwise `fallback`.
The key in the returned pair will be `BEq` to the input `a`.
 -/
Std.DHashMap.getEntryD : {α : Type u} →
  {β : α → Type v} → {x : BEq α} → {x_1 : Hashable α} → Std.DHashMap α β → α → (a : α) × β a → (a : α) × β a
-- Mathlib.Algebra.Order.UpperLower
IsUpperSet.add_right : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Preorder α] [IsOrderedAddMonoid α] {s t : Set α},
  IsUpperSet s → IsUpperSet (s + t)
-- Mathlib.Analysis.Complex.Basic
RCLike.hasSum_iff : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {L : SummationFilter α} (f : α → 𝕜) (c : 𝕜),
  HasSum f c L ↔ HasSum (fun x => RCLike.re (f x)) (RCLike.re c) L ∧ HasSum (fun x => RCLike.im (f x)) (RCLike.im c) L
-- Std.Time.Date.PlainDate
/-- Subtracts `Year.Offset` from a `PlainDate`, rolling over excess days to the next month.
 -/
Std.Time.PlainDate.subYearsRollOver : Std.Time.PlainDate → Std.Time.Year.Offset → Std.Time.PlainDate
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.compl_sup : ∀ {α : Type u_1} [inst : LE α] (s t : LowerSet α), (s ⊔ t).compl = s.compl ⊔ t.compl
-- Mathlib.CategoryTheory.ComposableArrows.Three
CategoryTheory.ComposableArrows.threeδ₁Toδ₀_app_two : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {i j k l : C} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l)
  (f₁₂ : i ⟶ k) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂),
  (CategoryTheory.ComposableArrows.threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂).app 2 =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.ComposableArrows.mk₂ f₁₂ f₃).obj 2)
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.relabel.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} {n : ℕ} (g : α → β ⊕ Fin n) {k : ℕ} (φ : L.BoundedFormula α k),
  FirstOrder.Language.BoundedFormula.relabel g φ =
    FirstOrder.Language.BoundedFormula.mapTermRel
      (fun x t => FirstOrder.Language.Term.relabel (FirstOrder.Language.BoundedFormula.relabelAux g x) t) (fun x => id)
      (fun x => FirstOrder.Language.BoundedFormula.castLE ⋯) φ
-- Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
minpoly.coe_equivAdjoin : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsDomain R] [inst_3 : Algebra R S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsDomain S] [inst_6 : Module.IsTorsionFree R S] {x : S}
  (hx : IsIntegral R x), ⇑(minpoly.equivAdjoin hx) = ⇑(AdjoinRoot.Minpoly.toAdjoin R x)
-- Mathlib.NumberTheory.RamificationInertia.Ramification
Ideal.ramificationIdx'_lt : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal R} {P : Ideal S}
  {n : ℕ}, ¬Ideal.map (algebraMap R S) p ≤ P ^ n → p.ramificationIdx' P < n
-- Mathlib.Algebra.Module.Presentation.Cokernel
/-- Constructor for `Presentation.CokernelData` in case we have a chosen set-theoretic
section of the projection `(pres₂.G →₀ A) → M₂`.  -/
Module.Presentation.CokernelData.ofSection : {A : Type u} →
  [inst : Ring A] →
    {M₁ : Type v₁} →
      {M₂ : Type v₂} →
        [inst_1 : AddCommGroup M₁] →
          [inst_2 : Module A M₁] →
            [inst_3 : AddCommGroup M₂] →
              [inst_4 : Module A M₂] →
                (pres₂ : Module.Presentation A M₂) →
                  (f : M₁ →ₗ[A] M₂) →
                    {ι : Type w₁} →
                      (g₁ : ι → M₁) →
                        (s : M₂ → pres₂.G →₀ A) → (∀ (m₂ : M₂), pres₂.π (s m₂) = m₂) → pres₂.CokernelData f g₁
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
/-- **Alias** of the reverse direction of `linearIndepOn_univ_iff`. -/
LinearIndependent.linearIndepOn_univ : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M], LinearIndependent R v → LinearIndepOn R v Set.univ
-- Mathlib.Analysis.Complex.Periodic
Function.Periodic.cuspFunction_sub : ∀ {h : ℝ} {f g : ℂ → ℂ},
  ContinuousAt (Function.Periodic.cuspFunction h f) 0 →
    ContinuousAt (Function.Periodic.cuspFunction h g) 0 →
      Function.Periodic.cuspFunction h (f - g) = Function.Periodic.cuspFunction h f - Function.Periodic.cuspFunction h g
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearMap.IsInvertible.of_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₂} {g : M₂ →L[R] M},
  f ∘SL g = ContinuousLinearMap.id R M₂ → g ∘SL f = ContinuousLinearMap.id R M → f.IsInvertible
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
_private.Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk.0.SzemerediRegularity.sum_card_subset_chunk_parts_le : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {P : Finpartition Finset.univ} {hP : P.IsEquipartition}
  {G : SimpleGraph α} [inst_2 : DecidableRel G.Adj] {ε : ℝ} {U : Finset α} {hU : U ∈ P.parts} {𝒜 : Finset (Finset α)}
  {s : Finset α},
  0 < ↑(Fintype.card α / SzemerediRegularity.stepBound P.parts.card) →
    𝒜 ⊆ (SzemerediRegularity.chunk hP G ε hU).parts →
      s ∈ 𝒜 →
        ↑(𝒜.sup id).card ≤
          ↑𝒜.card * ↑s.card *
            ((↑(Fintype.card α / SzemerediRegularity.stepBound P.parts.card) + 1) /
              ↑(Fintype.card α / SzemerediRegularity.stepBound P.parts.card))
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get!_filterMap : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] [inst_1 : Inhabited γ] {f : α → β → Option γ} {k : α},
  Std.DTreeMap.Const.get! (Std.DTreeMap.filterMap f t) k =
    ((Std.DTreeMap.Const.get? t k).pbind fun x h' => f (t.getKey k ⋯) x).get!
-- Mathlib.Data.Multiset.Sum
Multiset.disjSum_lt_disjSum_of_le_of_lt : ∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Multiset α} {t₁ t₂ : Multiset β},
  s₁ ≤ s₂ → t₁ < t₂ → s₁.disjSum t₁ < s₂.disjSum t₂
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
ApproximatesLinearOn.injOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E ≃L[𝕜] F} {s : Set E} {c : NNReal},
  ApproximatesLinearOn f (↑f') s c → Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹ → Set.InjOn f s
-- Init.Grind.Module.Envelope
Lean.Grind.IntModule.OfNatModule.neg_add_cancel : ∀ {α : Type u} [inst : Lean.Grind.NatModule α] (a : Lean.Grind.IntModule.OfNatModule.Q α),
  Lean.Grind.IntModule.OfNatModule.add (Lean.Grind.IntModule.OfNatModule.neg a) a =
    Lean.Grind.IntModule.OfNatModule.zero
-- Init.Data.UInt.Lemmas
UInt8.toUInt32_ofNatTruncate_of_le : ∀ {n : ℕ},
  UInt8.size ≤ n →
    (UInt8.ofNatClamp n).toUInt32 = UInt32.ofNatLT (UInt8.size - 1) UInt8.toUInt32_ofNatClamp_of_le._proof_1
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- The functor `costructuredArrowSndProj` is left adjoint to `costructuredArrowSndInclusion`.  -/
CategoryTheory.Comma.costructuredArrowSndAdjunction : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            (L : CategoryTheory.Functor A T) →
              (R : CategoryTheory.Functor B T) →
                (b : B) →
                  CategoryTheory.Comma.costructuredArrowSndProj L R b ⊣
                    CategoryTheory.Comma.costructuredArrowSndInclusion L R b
-- Init.Data.SInt.Basic
/-- The number of distinct values representable by `Int64`, that is, `2^64 = 18446744073709551616`.  -/
Int64.size : ℕ
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
/-- Composing a continuous alternating map with a continuous linear map gives again a
continuous alternating map.  -/
ContinuousLinearMap.compContinuousAlternatingMap : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_4} →
      {N' : Type u_5} →
        {ι : Type u_6} →
          [inst : Semiring R] →
            [inst_1 : AddCommMonoid M] →
              [inst_2 : Module R M] →
                [inst_3 : TopologicalSpace M] →
                  [inst_4 : AddCommMonoid N] →
                    [inst_5 : Module R N] →
                      [inst_6 : TopologicalSpace N] →
                        [inst_7 : AddCommMonoid N'] →
                          [inst_8 : Module R N'] →
                            [inst_9 : TopologicalSpace N'] → (N →L[R] N') → M [⋀^ι]→L[R] N → M [⋀^ι]→L[R] N'
-- Lean.Elab.MutualInductive
/-- Elaborates all the headers in the inductive views.
 -/
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.elabHeaders : Array Lean.Elab.Command.InductiveView → Lean.Elab.TermElabM (Array Lean.Elab.Command.PreElabHeaderResult)
-- Mathlib.FieldTheory.Perfect
frobeniusEquiv_symm_comp_frobenius : ∀ (R : Type u_1) (p : ℕ) [inst : CommSemiring R] [inst_1 : ExpChar R p] [inst_2 : PerfectRing R p],
  (↑(frobeniusEquiv R p).symm).comp (frobenius R p) = RingHom.id R
-- Mathlib.RingTheory.HopfAlgebra.GroupLike
IsGroupLikeElem.mul_antipode_cancel : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : HopfAlgebra R A] {a : A},
  IsGroupLikeElem R a → a * (HopfAlgebraStruct.antipode R) a = 1
-- Mathlib.Order.RelClasses
WellFounded.psigma_revLex : ∀ {α : Sort u_1} {β : Sort u_2} {r : α → α → Prop} {s : β → β → Prop},
  WellFounded r → WellFounded s → WellFounded (PSigma.RevLex r s)
-- Lean.Level
Lean.Level.zero.sizeOf_spec : sizeOf Lean.Level.zero = 1
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.uIoc_union_uIoc : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, b ∈ Set.uIcc a c → Set.uIoc a b ∪ Set.uIoc b c = Set.uIoc a c
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
LinearMap.BilinForm.baseChange.eq_1 : ∀ {R : Type uR} (A : Type uA) {M₂ : Type uM₂} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Algebra R A] [inst_4 : Module R M₂] (B : LinearMap.BilinForm R M₂),
  LinearMap.BilinForm.baseChange A B = LinearMap.BilinForm.tmul (LinearMap.mul A A) B
-- Mathlib.Algebra.Polynomial.Taylor
Polynomial.taylor_coeff_zero : ∀ {R : Type u_1} [inst : Semiring R] (r : R) (f : Polynomial R), ((Polynomial.taylor r) f).coeff 0 = Polynomial.eval r f
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKeyD_erase_eq_iff_not_compare_minKeyD_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k fallback : α},
  (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.isEmpty = false →
    ((Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.minKeyD fallback = t.minKeyD fallback ↔
      ¬compare k (t.minKeyD fallback) = Ordering.eq)
-- Lean.Parser.Basic
Lean.Parser.leadingNode : Lean.SyntaxNodeKind → ℕ → Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.Logic.Relation
Relation.Join.symm : ∀ {α : Type u_1} {r : α → α → Prop}, Std.Symm (Relation.Join r)
-- Mathlib.Data.Seq.Basic
Stream'.Seq.zipWith_map_left : ∀ {α : Type u} {β : Type v} {γ : Type w} {α' : Type u'} (s₁ : Stream'.Seq α) (s₂ : Stream'.Seq β) (f : α → α')
  (g : α' → β → γ), Stream'.Seq.zipWith g (Stream'.Seq.map f s₁) s₂ = Stream'.Seq.zipWith (fun a b => g (f a) b) s₁ s₂
-- Mathlib.Topology.Separation.Hausdorff
/-- In a `T2Space X`, for a compact set `t` and a point `x` outside `t`, `𝓝ˢ t` and `𝓝 x` are
disjoint.  -/
IsCompact.disjoint_nhdsSet_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X] {x : X} {t : Set X},
  IsCompact t → x ∉ t → Disjoint (nhdsSet t) (nhds x)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_pi_div_eight : Real.cos (Real.pi / 8) = √(2 + √2) / 2
-- Qq.Delab
Qq.Impl.delabQ : Lean.PrettyPrinter.Delaborator.Delab
-- Lean.Meta.CtorRecognizer
/-- Similar to `constructorApp?`, but on failure it puts `e` in WHNF and tries again.
It also uses `isOffset?` for `Nat`.

See also `Lean.Meta.isConstructorApp'?`.
 -/
Lean.Meta.constructorApp'? : Lean.Expr → Lean.MetaM (Option (Lean.ConstructorVal × Array Lean.Expr))
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem?_diff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (t₁ \ t₂)[k]? = if k ∈ t₂ then none else t₁[k]?
-- Mathlib.Analysis.Normed.Module.FiniteDimension
AffineEquiv.coe_toContinuousAffineEquiv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type w} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : CompleteSpace 𝕜] {PE : Type u_1} {PF : Type u_2} [inst_6 : MetricSpace PE] [inst_7 : NormedAddTorsor E PE]
  [inst_8 : MetricSpace PF] [inst_9 : NormedAddTorsor F PF] [inst_10 : FiniteDimensional 𝕜 E] (f : PE ≃ᵃ[𝕜] PF),
  ⇑(AffineEquiv.toContinuousAffineEquiv f) = ⇑f
-- Mathlib.Order.SuccPred.Basic
Order.pred_strictMono : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] [NoMinOrder α], StrictMono Order.pred
-- Mathlib.AlgebraicTopology.SimplicialSet.Nonempty
SSet.instNonemptyObjOppositeSimplexCategoryOfNonempty : ∀ (X : SSet) (n : SimplexCategoryᵒᵖ) [X.Nonempty], Nonempty (X.obj n)
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.comp_zero : ∀ {α : Type u_2} {β : Type u_3} {M : Type u_7} [inst : Zero M] (f : M → β), f ∘ 0 = Function.const α (f 0)
-- Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology
/-- The defining property of the weak operator topology: a function `f` tends to
`A : E →WOT[𝕜] F` along filter `l` iff `⟪y, (f a) x⟫` tends to `⟪y, A x⟫` along the same filter.  -/
ContinuousLinearMapWOT.tendsto_iff_forall_inner_apply_tendsto : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E]
  [inst_3 : Module 𝕜 E] [inst_4 : NormedAddCommGroup F] [inst_5 : InnerProductSpace 𝕜 F] [CompleteSpace F]
  {α : Type u_4} {l : Filter α} {f : α → E →WOT[𝕜] F} {A : E →WOT[𝕜] F},
  Filter.Tendsto f l (nhds A) ↔
    ∀ (x : E) (y : F), Filter.Tendsto (fun a => inner 𝕜 y ((f a) x)) l (nhds (inner 𝕜 y (A x)))
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
HasFiniteFPowerSeriesOnBall.hasStrictFDerivAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {n : ℕ} {f : E → F} {x : E},
  HasFiniteFPowerSeriesOnBall f p x n r →
    ∀ {y : E}, ↑‖y‖₊ < r → HasStrictFDerivAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin y 1)) (x + y)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.Red.cons_cons_iff : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)} (p : α × Bool), FreeAddGroup.Red (p :: L₁) (p :: L₂) ↔ FreeAddGroup.Red L₁ L₂
-- Mathlib.RingTheory.Congruence.Defs
/-- Two elements are related by a congruence relation `c` iff they are represented by the same
element of the quotient by `c`.  -/
RingCon.eq : ∀ {R : Type u_1} [inst : Add R] [inst_1 : Mul R] (c : RingCon R) {a b : R}, ↑a = ↑b ↔ c a b
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Bounded.State.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (producers : Std.Queue (IO.Promise Bool))
  (waiters : Std.Queue (Std.Broadcast.Consumer✝ α)) (capacity : { x // 0 < x }) (size : ℕ)
  (buffer : Vector (IO.Ref (Std.Slot✝ α)) ↑capacity) (write read : Fin ↑capacity) (receivers : Std.TreeMap ℕ ℕ compare)
  (nextId : ℕ) (closed : Bool) (pos : ℕ),
  sizeOf
      { producers := producers, waiters := waiters, capacity := capacity, size := size, buffer := buffer,
        write := write, read := read, receivers := receivers, nextId := nextId, closed := closed, pos := pos } =
    1 + sizeOf producers + sizeOf waiters + sizeOf capacity + sizeOf size + sizeOf buffer + sizeOf write + sizeOf read +
            sizeOf receivers +
          sizeOf nextId +
        sizeOf closed +
      sizeOf pos
-- Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
CategoryTheory.SimplicialObject.Homotopy.h_comp_σ_castSucc_of_le_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.SimplicialObject C} {f g : X ⟶ Y}
  (self : CategoryTheory.SimplicialObject.Homotopy f g) {n : ℕ} (i j : Fin (n + 1)),
  i ≤ j →
    ∀ {Z : C} (h : Y.obj (Opposite.op { len := n + 1 + 1 }) ⟶ Z),
      CategoryTheory.CategoryStruct.comp (self.h j) (CategoryTheory.CategoryStruct.comp (Y.σ i.castSucc) h) =
        CategoryTheory.CategoryStruct.comp (X.σ i) (CategoryTheory.CategoryStruct.comp (self.h j.succ) h)
-- Init.Data.SInt.Lemmas
Int64.ofInt_add : ∀ (a b : ℤ), Int64.ofInt (a + b) = Int64.ofInt a + Int64.ofInt b
-- Mathlib.AlgebraicGeometry.Sites.Pretopology
/-- The Grothendieck topology defined by `P`-covers agrees with the Grothendieck
topology induced by the intersection of the pretopology of surjective families with
the pretopology defined by `P`.
 -/
AlgebraicGeometry.Scheme.grothendieckTopology_eq_inf : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) [inst : P.IsStableUnderBaseChange]
  [inst_1 : P.IsMultiplicative],
  AlgebraicGeometry.Scheme.grothendieckTopology P =
    (AlgebraicGeometry.Scheme.jointlySurjectivePretopology ⊓ P.pretopology).toGrothendieck
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
PresheafOfModules.Sheafify.SMulCandidate.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {J : CategoryTheory.GrothendieckTopology C}
  {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} {α : R₀ ⟶ R.obj}
  {M₀ : PresheafOfModules R₀} {A : CategoryTheory.Sheaf J AddCommGrpCat} {φ : M₀.presheaf ⟶ A.obj} {X : Cᵒᵖ}
  {r : ↑(R.obj.obj X)} {m x : ↑(A.obj.obj X)}
  {h :
    ∀ ⦃Y : Cᵒᵖ⦄ (f : X ⟶ Y) (r₀ : ↑(R₀.obj Y)),
      (CategoryTheory.ConcreteCategory.hom (α.app Y)) r₀ = (CategoryTheory.ConcreteCategory.hom (R.obj.map f)) r →
        ∀ (m₀ : ↑(M₀.obj Y)),
          (CategoryTheory.ConcreteCategory.hom (φ.app Y)) m₀ = (CategoryTheory.ConcreteCategory.hom (A.obj.map f)) m →
            (CategoryTheory.ConcreteCategory.hom (A.obj.map f)) x =
              (CategoryTheory.ConcreteCategory.hom (φ.app Y)) (r₀ • m₀)}
  {x_1 : ↑(A.obj.obj X)}
  {h_1 :
    ∀ ⦃Y : Cᵒᵖ⦄ (f : X ⟶ Y) (r₀ : ↑(R₀.obj Y)),
      (CategoryTheory.ConcreteCategory.hom (α.app Y)) r₀ = (CategoryTheory.ConcreteCategory.hom (R.obj.map f)) r →
        ∀ (m₀ : ↑(M₀.obj Y)),
          (CategoryTheory.ConcreteCategory.hom (φ.app Y)) m₀ = (CategoryTheory.ConcreteCategory.hom (A.obj.map f)) m →
            (CategoryTheory.ConcreteCategory.hom (A.obj.map f)) x_1 =
              (CategoryTheory.ConcreteCategory.hom (φ.app Y)) (r₀ • m₀)},
  { x := x, h := h } = { x := x_1, h := h_1 } → x = x_1
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.toLp_eq_zero : ∀ (p : ENNReal) {V : Type u_4} [inst : AddCommGroup V] {x : V}, WithLp.toLp p x = 0 ↔ x = 0
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
_private.Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification.0.NumberField.InfinitePlace.bijOn_extensionIte : ∀ {K : Type u_4} (L : Type u_5) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (v : NumberField.InfinitePlace K),
  Set.BijOn (NumberField.InfinitePlace.embeddingConjugateIte✝ v) (NumberField.InfinitePlace.unramifiedPlacesOver L v)
    (NumberField.ComplexEmbedding.unmixedEmbeddingsOver L v.embedding)
-- Mathlib.Data.Finsupp.MonomialOrder
MonomialOrder.lex_lt_iff_of_unique : ∀ {σ : Type u_1} [inst : LinearOrder σ] [inst_1 : Unique σ] {c d : σ →₀ ℕ},
  MonomialOrder.lex.toSyn c < MonomialOrder.lex.toSyn d ↔ c default < d default
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.exists_iterate_apply_eq_of_mem_periodicPts : ∀ {α : Type u_1} {f : α → α} {x : α}, x ∈ Function.periodicPts f → ∃ n, f^[n] x = x
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.coe_equivMapOfInjective_apply : ∀ {N : Type u_2} [inst : AddZeroClass N] {M : Type u_5} [inst_1 : AddZeroClass M] (S : AddSubmonoid M) (f : M →+ N)
  (hf : Function.Injective ⇑f) (x : ↥S), ↑((S.equivMapOfInjective f hf) x) = f ↑x
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.mk_mor₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z) (h : Z ⟶ (CategoryTheory.shiftFunctor C 1).obj X),
  (CategoryTheory.Pretriangulated.Triangle.mk f g h).mor₁ = f
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionUnitIso : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction Cᴹᵒᵖ D] (x : D),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso x =
    CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso x
-- Mathlib.Data.Matrix.Block
Matrix.blockDiagonal_apply_ne : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [inst : DecidableEq o] [inst_1 : Zero α]
  (M : o → Matrix m n α) (i : m) (j : n) {k k' : o}, k ≠ k' → Matrix.blockDiagonal M (i, k) (j, k') = 0
-- Mathlib.Data.Set.Finite.Basic
/-- A finite set coerced to a type is a `Fintype`.
This is the `Fintype` projection for a `Set.Finite`.

Note that because `Finite` isn't a typeclass, this definition will not fire if it
is made into an instance  -/
Set.Finite.fintype : {α : Type u} → {s : Set α} → s.Finite → Fintype ↑s
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.isCocircuit_def : ∀ {α : Type u_1} {M : Matroid α} {K : Set α}, M.IsCocircuit K ↔ M✶.IsCircuit K
-- Mathlib.Algebra.Group.Pi.Lemmas
MulHom.coeFn_apply : ∀ (α : Type u_5) (β : Type u_6) [inst : Mul α] [inst_1 : CommSemigroup β] (g : α →ₙ* β) (a : α),
  (MulHom.coeFn α β) g a = g a
-- Mathlib.Analysis.SpecialFunctions.Log.Deriv
Real.contDiffAt_log : ∀ {n : WithTop ℕ∞} {x : ℝ}, ContDiffAt ℝ n Real.log x ↔ x ≠ 0