mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Abelian.FreydMitchell
_private.Mathlib.CategoryTheory.Abelian.FreydMitchell.0.CategoryTheory.Abelian.FreydMitchell.F.eq_1 : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.Abelian.FreydMitchell.F✝ C = CategoryTheory.AsSmall.equiv.functor
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get!_alter_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k : α} [inst_3 : Inhabited (β k)] {f : Option (β k) → Option (β k)},
  m.WF → (m.alter k f).get! k = (f (m.get? k)).get!
-- Mathlib.RingTheory.RingHom.Locally
/-- Equivalence variant of `locally_of_exists`. This is sometimes easier to use, if the
`IsLocalization.Away` instance can't be automatically inferred.  -/
RingHom.locally_iff_exists : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} {R S : Type u}
  [inst : CommRing R] [inst_1 : CommRing S],
  (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P) →
    ∀ (f : R →+* S),
      RingHom.Locally (fun {R S} [CommRing R] [CommRing S] => P) f ↔
        ∃ ι s,
          ∃ (_ : Ideal.span (Set.range s) = ⊤),
            ∃ Sₜ x x_1, ∃ (_ : ∀ (i : ι), IsLocalization.Away (s i) (Sₜ i)), ∀ (i : ι), P ((algebraMap S (Sₜ i)).comp f)
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
HomotopicalAlgebra.PrepathObject.RightHomotopy.h₁_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {Y : C} {P : HomotopicalAlgebra.PrepathObject Y} {X : C}
  {f g : X ⟶ Y} (self : P.RightHomotopy f g) {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.h (CategoryTheory.CategoryStruct.comp P.p₁ h) =
    CategoryTheory.CategoryStruct.comp g h
-- Init.Data.Array.Extract
Array.extract_eq_empty_of_eq_empty : ∀ {α : Type u_1} {as : Array α} {i j : ℕ}, as = #[] → as.extract i j = #[]
-- Mathlib.Topology.Category.TopCat.OpenNhds
TopologicalSpace.OpenNhds.partialOrder : {X : TopCat} → (x : ↑X) → PartialOrder (TopologicalSpace.OpenNhds x)
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.mergeSort.eq_2 : ∀ {α : Type u_1} (x : α → α → Bool) (a : α), [a].mergeSort x = [a]
-- Mathlib.Algebra.Regular.SMul
/-- Any element in `Rˣ` is `M`-regular.  -/
Units.isSMulRegular : ∀ {R : Type u_1} (M : Type u_3) [inst : Monoid R] [inst_1 : MulAction R M] (a : Rˣ), IsSMulRegular M ↑a
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.posDef_natCast_iff : ∀ {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  [inst_4 : DecidableEq n] [NoZeroDivisors R] [Nonempty n] [Nontrivial R] {d : ℕ}, (↑d).PosDef ↔ 0 < d
-- Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
/-- A stochastic process `X : T → Ω → E` has independent increments if for any `n ≥ 1` and
`t₁ ≤ ... ≤ tₙ`, the random variables `X t₂ - X t₁, ..., X tₙ - X tₙ₋₁` are independent.

Although this corresponds to the standard definition, dealing with `Fin` might make things
complicated in some cases. Therefore we provide `HasIndepIncrements.of_nat` which instead requires
to prove that for any monotone sequence `(tₙ)` that is eventually constant,
the random variables `X tₙ₊₁ - X tₙ` are independent.  -/
ProbabilityTheory.HasIndepIncrements : {T : Type u_1} →
  {Ω : Type u_2} →
    {E : Type u_3} →
      {mΩ : MeasurableSpace Ω} →
        [Preorder T] →
          [MeasurableSpace E] →
            [Sub E] →
              (T → Ω → E) → autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.HasIndepIncrements._auto_1 → Prop
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKeyD_insertEntry_of_isEmpty : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α} {v : β k}
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    l.isEmpty = true → ∀ {fallback : α}, Std.Internal.List.minKeyD (Std.Internal.List.insertEntry k v l) fallback = k
-- Lean.Elab.Tactic.Omega.Core
/-- Whether the elimination would be exact, because all of the lower bound coefficients are `±1`.
 -/
Lean.Elab.Tactic.Omega.Problem.FourierMotzkinData.lowerExact : Lean.Elab.Tactic.Omega.Problem.FourierMotzkinData → Bool
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.instNatCastAdicCauchySequence : {R : Type u_1} → [inst : CommRing R] → (I : Ideal R) → NatCast (AdicCompletion.AdicCauchySequence I R)
-- Aesop.Forward.SlotIndex
Aesop.instBEqSlotIndex : BEq Aesop.SlotIndex
-- Mathlib.Topology.UniformSpace.Cauchy
/-- A uniform space is complete provided that (a) its uniformity filter has a countable basis;
(b) any sequence satisfying a "controlled" version of the Cauchy condition converges.  -/
UniformSpace.complete_of_convergent_controlled_sequences : ∀ {α : Type u} [uniformSpace : UniformSpace α] [(uniformity α).IsCountablyGenerated] (U : ℕ → SetRel α α),
  (∀ (n : ℕ), U n ∈ uniformity α) →
    (∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ a, Filter.Tendsto u Filter.atTop (nhds a)) →
      CompleteSpace α
-- Mathlib.Data.W.Constructions
WType.ofNat.eq_2 : ∀ (n : ℕ), WType.ofNat n.succ = WType.mk WType.Natα.succ fun x => WType.ofNat n
-- Mathlib.Order.Interval.Finset.Basic
Finset.Iio_eq_empty : ∀ {α : Type u_2} {a : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α], Finset.Iio a = ∅ ↔ IsMin a
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.eccent_pos_iff : ∀ {α : Type u_1} {G : SimpleGraph α} (u : α), 0 < G.eccent u ↔ Nontrivial α
-- Mathlib.Algebra.QuaternionBasis
/-- Intermediate result used to define `QuaternionAlgebra.Basis.liftHom`.  -/
QuaternionAlgebra.Basis.lift : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : Ring A] →
        [inst_2 : Algebra R A] → {c₁ c₂ c₃ : R} → QuaternionAlgebra.Basis A c₁ c₂ c₃ → QuaternionAlgebra R c₁ c₂ c₃ → A
-- Init.WF
WellFounded.Nat.eager_eq : ∀ (n : ℕ), WellFounded.Nat.eager n = n
-- Aesop.RulePattern.Cache
Aesop.instInhabitedRulePatternCache : Inhabited Aesop.RulePatternCache
-- Mathlib.CategoryTheory.Filtered.Small
_private.Mathlib.CategoryTheory.Filtered.Small.0.CategoryTheory.IsFiltered.FilteredClosureSmall.bundledAbstractFilteredClosure.eq_2 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFilteredOrEmpty C] {α : Type w}
  (f : α → C) (n : ℕ),
  CategoryTheory.IsFiltered.FilteredClosureSmall.bundledAbstractFilteredClosure✝ f n.succ =
    ⟨CategoryTheory.IsFiltered.FilteredClosureSmall.InductiveStep✝ (n + 1) fun m x =>
        CategoryTheory.IsFiltered.FilteredClosureSmall.bundledAbstractFilteredClosure✝ f m,
      CategoryTheory.IsFiltered.FilteredClosureSmall.inductiveStepRealization✝ (n + 1) fun m x =>
        CategoryTheory.IsFiltered.FilteredClosureSmall.bundledAbstractFilteredClosure✝ f m⟩
-- Std.Data.HashSet.Lemmas
Std.HashSet.Equiv.of_forall_get?_eq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α],
  (∀ (k : α), m₁.get? k = m₂.get? k) → m₁.Equiv m₂
-- Mathlib.Analysis.Calculus.FDeriv.Symmetric
IsSymmSndFDerivAt.isSymmSndFDerivWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E} {f : E → F} {x : E},
  IsSymmSndFDerivAt 𝕜 f x → ContDiffAt 𝕜 2 f x → UniqueDiffOn 𝕜 s → x ∈ s → IsSymmSndFDerivWithinAt 𝕜 f s x
-- Init.Data.String.Iterator
String.Legacy.Iterator.sizeOf_next_lt_of_hasNext : ∀ (i : String.Legacy.Iterator), i.hasNext = true → sizeOf i.next < sizeOf i
-- Mathlib.Analysis.InnerProductSpace.Adjoint
ContinuousLinearMap.star_eq_adjoint : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] (A : E →L[𝕜] E), star A = ContinuousLinearMap.adjoint A
-- Lean.Language.Basic
/-- Returns task result if already finished or else `none`.  -/
Lean.Language.SnapshotTask.get? : {α : Type} → Lean.Language.SnapshotTask α → BaseIO (Option α)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (f' : W ⟶ X)
  [inst_1 : CategoryTheory.Limits.HasPullback f g]
  [inst_2 : CategoryTheory.Limits.HasPullback f' (CategoryTheory.Limits.pullback.fst f g)] {Z_1 : C} (h : X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackRightPullbackFstIso f g f').inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd f' (CategoryTheory.Limits.pullback.fst f g))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp f' f) g)
      (CategoryTheory.CategoryStruct.comp f' h)
-- Mathlib.Order.Interval.Set.Basic
Set.Icc_eq_Icc_iff : ∀ {α : Type u_1} [inst : PartialOrder α] {a b c d : α}, a ≤ b → (Set.Icc a b = Set.Icc c d ↔ a = c ∧ b = d)
-- Mathlib.Topology.Algebra.Order.Group
tendsto_mabs_nhdsNE_one : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : CommGroup G] [inst_2 : LinearOrder G] [IsOrderedMonoid G]
  [OrderTopology G], Filter.Tendsto mabs (nhdsWithin 1 {1}ᶜ) (nhdsWithin 1 (Set.Ioi 1))
-- Mathlib.Algebra.Order.SuccPred
Order.one_le_iff_pos : ∀ {α : Type u_1} {x : α} [inst : PartialOrder α] [inst_1 : AddMonoidWithOne α] [ZeroLEOneClass α] [NeZero 1]
  [SuccAddOrder α], 1 ≤ x ↔ 0 < x
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.Splitting.toMonoidHom : {N : Type u_1} →
  {E : Type u_2} →
    {G : Type u_3} →
      [inst : Group N] → [inst_1 : Group E] → [inst_2 : Group G] → {S : GroupExtension N E G} → S.Splitting → G →* E
-- Mathlib.Topology.UniformSpace.Cauchy
cauchy_iInf_uniformSpace : ∀ {β : Type v} {ι : Sort u_1} [Nonempty ι] {u : ι → UniformSpace β} {l : Filter β}, Cauchy l ↔ ∀ (i : ι), Cauchy l
-- Mathlib.CategoryTheory.Category.Preorder
CategoryTheory.homOfLE_isIso_of_eq : ∀ {X : Type u} [inst : Preorder X] {x y : X} (h : x ≤ y), x = y → CategoryTheory.IsIso (CategoryTheory.homOfLE h)
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.tr.eq_11 : ∀ (f : Turing.ToPartrec.Code) (k : Turing.PartrecToTM2.Cont'),
  Turing.PartrecToTM2.tr (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.fix f k)) =
    Turing.PartrecToTM2.pop' Turing.PartrecToTM2.K'.main
      (Turing.TM2.Stmt.goto fun s =>
        bif Turing.PartrecToTM2.natEnd (s.getD default) then Turing.PartrecToTM2.Λ'.ret k
        else
          Turing.PartrecToTM2.Λ'.clear Turing.PartrecToTM2.natEnd Turing.PartrecToTM2.K'.main
            (Turing.PartrecToTM2.trNormal f (Turing.PartrecToTM2.Cont'.fix f k)))
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.Recv.response.injEq : ∀ {β : Type} (x x_1 : Except IO.Error (Std.Http.Response β)),
  (Std.Http.Server.Connection.Recv.response✝ x = Std.Http.Server.Connection.Recv.response✝ x_1) = (x = x_1)
-- Mathlib.Analysis.Normed.Module.Ball.Homeomorph
OpenPartialHomeomorph.unitBallBall_apply : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {P : Type u_2}
  [inst_2 : PseudoMetricSpace P] [inst_3 : NormedAddTorsor E P] (c : P) (r : ℝ) (hr : 0 < r) (a : E),
  ↑(OpenPartialHomeomorph.unitBallBall c r hr) a = r • a +ᵥ c
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get?_insert_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {v : β k}, (t.insert k v).get? k = some v
-- Mathlib.CategoryTheory.EffectiveEpi.Preserves
CategoryTheory.Functor.PreservesEffectiveEpis.mk : ∀ {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] {F : CategoryTheory.Functor C D},
  (∀ {X Y : C} (f : X ⟶ Y) [CategoryTheory.EffectiveEpi f], CategoryTheory.EffectiveEpi (F.map f)) →
    F.PreservesEffectiveEpis
-- Mathlib.Computability.Primrec.List
Nat.Primrec'.prim_iff₁ : ∀ {f : ℕ → ℕ}, (Nat.Primrec' fun v => f v.head) ↔ Primrec f
-- Mathlib.Analysis.CStarAlgebra.Spectrum
Unitary.spectrum_subset_circle : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] {E : Type u_2} [inst_1 : NormedRing E] [inst_2 : StarRing E] [CStarRing E]
  [inst_4 : NormedAlgebra 𝕜 E] [CompleteSpace E] (u : ↥(unitary E)), spectrum 𝕜 ↑u ⊆ Metric.sphere 0 1
-- Mathlib.Tactic.FunProp.Decl
/-- Returns function `f` from `e = P f` and `P` is function property.  -/
Mathlib.Meta.FunProp.getFunPropFun? : Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofCompletionInfo.injEq : ∀ (i i_1 : Lean.Elab.CompletionInfo),
  (Lean.Elab.Info.ofCompletionInfo i = Lean.Elab.Info.ofCompletionInfo i_1) = (i = i_1)
-- Mathlib.Order.ModularLattice
infIooOrderIsoIooSup'_apply_coe : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : IsModularLattice α] (a b : α) (a_1 : ↑(Set.Ioo (a ⊓ b) b)),
  ↑((infIooOrderIsoIooSup' a b) a_1) = ↑a_1 ⊔ a
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.tensorLeftHomEquiv_naturality : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X Y Y' Z Z' : C} [inst_2 : CategoryTheory.ExactPairing Y Y']
  (f : CategoryTheory.MonoidalCategoryStruct.tensorObj Y' X ⟶ Z) (g : Z ⟶ Z'),
  (CategoryTheory.tensorLeftHomEquiv X Y Y' Z') (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.tensorLeftHomEquiv X Y Y' Z) f)
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y g)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- If `s` is a limit fork over `f` and `g`, then a morphism `k : W ⟶ X` satisfying
`k ≫ f = k ≫ g` induces a morphism `l : W ⟶ s.pt` such that `l ≫ fork.ι s = k`.  -/
CategoryTheory.Limits.Fork.IsLimit.lift : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f g : X ⟶ Y} →
        {s : CategoryTheory.Limits.Fork f g} →
          CategoryTheory.Limits.IsLimit s →
            {W : C} →
              (k : W ⟶ X) → CategoryTheory.CategoryStruct.comp k f = CategoryTheory.CategoryStruct.comp k g → (W ⟶ s.pt)
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.instTransIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → Trans (fun x1 x2 => x1 ≅ x2) (fun x1 x2 => x1 ≅ x2) fun x1 x2 => x1 ≅ x2
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.continuous_inducingFn : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] [inst_8 : IsTopologicalAddGroup F]
  [inst_9 : ContinuousConstSMul 𝕜₂ F], Continuous ⇑(ContinuousLinearMapWOT.inducingFn σ E F)
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.Karoubi.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {X : C} {p : X ⟶ X}
  {idem : autoParam (CategoryTheory.CategoryStruct.comp p p = p) CategoryTheory.Idempotents.Karoubi.idem._autoParam}
  {X_1 : C} {p_1 : X_1 ⟶ X_1}
  {idem_1 :
    autoParam (CategoryTheory.CategoryStruct.comp p_1 p_1 = p_1) CategoryTheory.Idempotents.Karoubi.idem._autoParam},
  { X := X, p := p, idem := idem } = { X := X_1, p := p_1, idem := idem_1 } → X = X_1 ∧ p ≍ p_1
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.lcm_neg_left : ∀ (a b : ℤ), (-a).lcm b = a.lcm b
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.coe_sub : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → AddGroup (β i)] (g₁ g₂ : Π₀ (i : ι), β i), ⇑(g₁ - g₂) = ⇑g₁ - ⇑g₂
-- Mathlib.Tactic.FunProp.ToBatteries
_private.Mathlib.Tactic.FunProp.ToBatteries.0.Mathlib.Meta.FunProp.betaThroughLetAux.eq_def : ∀ (f : Lean.Expr) (args : List Lean.Expr),
  Mathlib.Meta.FunProp.betaThroughLetAux✝ f args =
    match f, args with
    | f, [] => f
    | Lean.Expr.lam binderName binderType b binderInfo, a :: as =>
      Mathlib.Meta.FunProp.betaThroughLetAux✝ (b.instantiate1 a) as
    | Lean.Expr.letE n t v b nondep, args =>
      Lean.Expr.letE n t v (Mathlib.Meta.FunProp.betaThroughLetAux✝ b args) nondep
    | Lean.Expr.mdata data b, args => Mathlib.Meta.FunProp.betaThroughLetAux✝ b args
    | f, args => Lean.mkAppN f args.toArray
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Right.pow_lt_one_iff : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : LinearOrder M] [MulRightStrictMono M] {n : ℕ} {x : M},
  0 < n → (x ^ n < 1 ↔ x < 1)
-- Init.Data.BitVec.Lemmas
BitVec.ofInt_ofNat : ∀ (w n : ℕ), BitVec.ofInt w (OfNat.ofNat n) = BitVec.ofNat w (OfNat.ofNat n)
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.withDensity_indicator_one : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasurableSet s → μ.withDensity (s.indicator 1) = μ.restrict s
-- Mathlib.Algebra.Homology.SpectralObject.Homology
/-- The homology data of the short complex
`E^{n-1}(f₅, f₆, f₇) ⟶ E^{n}(f₃, f₄, f₅) ⟶ E^{n+1}(f₁, f₂, f₃)` for which
* the cycles are `E^n(f₂ ≫ f₃, f₄, f₅)`;
* the opcycles are `E^n(f₃, f₄, f₅ ≫ f₆)`;
* the homology is `E^n(f₂ ≫ f₃, f₄, f₅ ≫ f₆)`.  -/
CategoryTheory.Abelian.SpectralObject.dHomologyData : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Abelian C] →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] →
          (X : CategoryTheory.Abelian.SpectralObject C ι) →
            {i₀ i₁ i₂ i₃ i₄ i₅ i₆ i₇ : ι} →
              (f₁ : i₀ ⟶ i₁) →
                (f₂ : i₁ ⟶ i₂) →
                  (f₃ : i₂ ⟶ i₃) →
                    (f₄ : i₃ ⟶ i₄) →
                      (f₅ : i₄ ⟶ i₅) →
                        (f₆ : i₅ ⟶ i₆) →
                          (f₇ : i₆ ⟶ i₇) →
                            (f₂₃ : i₁ ⟶ i₃) →
                              CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃ →
                                (f₅₆ : i₄ ⟶ i₆) →
                                  CategoryTheory.CategoryStruct.comp f₅ f₆ = f₅₆ →
                                    (n₀ n₁ n₂ n₃ n₄ : ℤ) →
                                      (hn₁ :
                                          autoParam (n₀ + 1 = n₁)
                                            CategoryTheory.Abelian.SpectralObject.dHomologyData._auto_1) →
                                        (hn₂ :
                                            autoParam (n₁ + 1 = n₂)
                                              CategoryTheory.Abelian.SpectralObject.dHomologyData._auto_3) →
                                          (hn₃ :
                                              autoParam (n₂ + 1 = n₃)
                                                CategoryTheory.Abelian.SpectralObject.dHomologyData._auto_5) →
                                            (hn₄ :
                                                autoParam (n₃ + 1 = n₄)
                                                  CategoryTheory.Abelian.SpectralObject.dHomologyData._auto_7) →
                                              (X.dShortComplex f₁ f₂ f₃ f₄ f₅ f₆ f₇ n₀ n₁ n₂ n₃ n₄ ⋯ ⋯ ⋯ ⋯).HomologyData
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- The rightmost object of `F : ComposableArrows C n`.  -/
CategoryTheory.ComposableArrows.right : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → {n : ℕ} → CategoryTheory.ComposableArrows C n → C
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.mkFullAdder.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig : Std.Sat.AIG α)
  (input : Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput aig),
  Std.Tactic.BVDecide.BVExpr.bitblast.mkFullAdder aig input =
    {
      aig :=
        (Std.Tactic.BVDecide.BVExpr.bitblast.mkFullAdderCarry
            (Std.Tactic.BVDecide.BVExpr.bitblast.mkFullAdderOut aig input).aig (input.cast ⋯)).aig,
      out := (Std.Tactic.BVDecide.BVExpr.bitblast.mkFullAdderOut aig input).ref.cast ⋯,
      cout :=
        (Std.Tactic.BVDecide.BVExpr.bitblast.mkFullAdderCarry
            (Std.Tactic.BVDecide.BVExpr.bitblast.mkFullAdderOut aig input).aig (input.cast ⋯)).ref,
      hle := ⋯ }
-- Mathlib.Analysis.Convex.Between
sbtw_iff_right_ne_and_left_mem_image_Ioi : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] {x y z : P},
  Sbtw R x y z ↔ z ≠ y ∧ x ∈ ⇑(AffineMap.lineMap z y) '' Set.Ioi 1
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.map_bot : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S] (f : R →ₙ+* S),
  NonUnitalSubring.map f ⊥ = ⊥
-- Init.Data.SInt.Basic
Int8.toBitVec.inj : ∀ {x y : Int8}, x.toBitVec = y.toBitVec → x = y
-- Mathlib.Data.Nat.Log
Nat.log.go.match_3.congr_eq_2 : ∀ (motive : ℕ → ℕ → Sort u_1) (x x_1 : ℕ) (h_1 : (x : ℕ) → motive x 0) (h_2 : (b fuel : ℕ) → motive b fuel.succ)
  (b fuel : ℕ),
  x = b →
    x_1 = fuel.succ →
      (match x, x_1 with
        | x, 0 => h_1 x
        | b, fuel.succ => h_2 b fuel) ≍
        h_2 b fuel
-- Lean.EnvExtension
Lean.SimplePersistentEnvExtensionDescr.replay? : {α σ : Type} → Lean.SimplePersistentEnvExtensionDescr α σ → Option (List α → σ → σ → List α × σ)
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.BasedNatTrans.isHomLift : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] {𝒳 : CategoryTheory.BasedCategory 𝒮}
  {𝒴 : CategoryTheory.BasedCategory 𝒮} {F G : CategoryTheory.BasedFunctor 𝒳 𝒴} (α : CategoryTheory.BasedNatTrans F G)
  {a : 𝒳.obj} {S : 𝒮}, 𝒳.p.obj a = S → 𝒴.p.IsHomLift (CategoryTheory.CategoryStruct.id S) (α.app a)
-- Mathlib.RingTheory.MvPowerSeries.GaussNorm
MvPowerSeries.gaussNorm_eq_zero_iff : ∀ {R : Type u_1} {σ : Type u_2} (v : R → ℝ) (c : σ → ℝ) (f : MvPowerSeries σ R) [inst : Semiring R],
  v 0 = 0 →
    (∀ (a : R), v a ≥ 0) →
      (∀ (x : R), v x = 0 → x = 0) →
        (∀ (i : σ), 0 < c i) → MvPowerSeries.HasGaussNorm v c f → (MvPowerSeries.gaussNorm v c f = 0 ↔ f = 0)
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
EisensteinSeries.eisensteinSeriesSIF_apply : ∀ {N : ℕ} (a : Fin 2 → ZMod N) (k : ℤ) (z : UpperHalfPlane),
  (EisensteinSeries.eisensteinSeriesSIF a k) z = eisensteinSeries a k z
-- Mathlib.RingTheory.NonUnitalSubring.Basic
/-- `NonUnitalSubring`s of a ring form a complete lattice.  -/
NonUnitalSubring.instCompleteLattice : {R : Type u} → [inst : NonUnitalNonAssocRing R] → CompleteLattice (NonUnitalSubring R)
-- Mathlib.CategoryTheory.Subfunctor.Image
CategoryTheory.Subfunctor.toRange.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F F' : CategoryTheory.Functor C (Type w)} (p : F' ⟶ F),
  CategoryTheory.Subfunctor.toRange p = CategoryTheory.Subfunctor.lift p ⋯
-- Std.Async.Timer
/-- Setup up an `Interval` that waits for `duration` milliseconds.
This function only initializes but does not yet start the timer.
 -/
Std.Async.Interval.mk : (duration : Std.Time.Millisecond.Offset) →
  autoParam (0 < duration) Std.Async.Interval.mk._auto_1 → IO Std.Async.Interval
-- Std.Data.ExtTreeSet.Basic
/-- Returns a set that contains all mappings of `t₁` and `t₂.

This function ensures that `t₁` is used linearly.
Hence, as long as `t₁` is unshared, the performance characteristics follow the following imperative
description: Iterate over all mappings in `t₂`, inserting them into `t₁`.

Hence, the runtime of this method scales logarithmically in the size of `t₁` and linearly in the
size of `t₂` as long as `t₁` is unshared.
 -/
Std.ExtTreeSet.merge : {α : Type u} →
  {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeSet α cmp → Std.ExtTreeSet α cmp → Std.ExtTreeSet α cmp
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.map_appLE' : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U U' : Y.Opens} {V : X.Opens}
  (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (i : U' = U),
  CategoryTheory.CategoryStruct.comp (Y.presheaf.map (CategoryTheory.eqToHom i).op)
      (AlgebraicGeometry.Scheme.Hom.appLE f U' V ⋯) =
    AlgebraicGeometry.Scheme.Hom.appLE f U V e