mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SetFamily.LYM
/-- A bound on any top part of the sum in LYM in terms of the size of `falling k 𝒜`.  -/
Finset.le_card_falling_div_choose : ∀ {𝕜 : Type u_1} {α : Type u_2} [inst : Semifield 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : DecidableEq α] {k : ℕ} {𝒜 : Finset (Finset α)} [inst_4 : Fintype α],
  k ≤ Fintype.card α →
    IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜 →
      ∑ r ∈ Finset.range (k + 1),
          ↑(𝒜.slice (Fintype.card α - r)).card / ↑((Fintype.card α).choose (Fintype.card α - r)) ≤
        ↑(Finset.falling (Fintype.card α - k) 𝒜).card / ↑((Fintype.card α).choose (Fintype.card α - k))
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.AnchorRef.numDigits : Lean.Meta.Grind.AnchorRef → ℕ
-- Mathlib.Data.NNReal.Defs
Real.toNNReal_of_nonpos : ∀ {r : ℝ}, r ≤ 0 → r.toNNReal = 0
-- Mathlib.GroupTheory.FreeAbelianGroup
RingHom.mk.congr_simp : ∀ {α : Type u_5} {β : Type u_6} [inst : NonAssocSemiring α] [inst_1 : NonAssocSemiring β]
  (toMonoidHom toMonoidHom_1 : α →* β) (e_toMonoidHom : toMonoidHom = toMonoidHom_1)
  (map_zero' : (↑toMonoidHom).toFun 0 = 0)
  (map_add' : ∀ (x y : α), (↑toMonoidHom).toFun (x + y) = (↑toMonoidHom).toFun x + (↑toMonoidHom).toFun y),
  { toMonoidHom := toMonoidHom, map_zero' := map_zero', map_add' := map_add' } =
    { toMonoidHom := toMonoidHom_1, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
unitsNonZeroDivisorsEquiv_apply : ∀ {M₀ : Type u_1} [inst : MonoidWithZero M₀] (a : (↥(nonZeroDivisors M₀))ˣ),
  unitsNonZeroDivisorsEquiv a = (↑(Units.map (nonZeroDivisors M₀).subtype)).toFun a
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.setToL1_nonneg : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {G' : Type u_7} {G'' : Type u_8}
  [inst : NormedAddCommGroup G''] [inst_1 : PartialOrder G''] [IsOrderedAddMonoid G''] [inst_3 : NormedSpace ℝ G'']
  [inst_4 : CompleteSpace G''] [inst_5 : NormedAddCommGroup G'] [inst_6 : PartialOrder G'] [inst_7 : NormedSpace ℝ G']
  [ClosedIciTopology G''] {T : Set α → G' →L[ℝ] G''} {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C),
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x) →
    ∀ {f : ↥(MeasureTheory.Lp G' 1 μ)}, 0 ≤ f → 0 ≤ (MeasureTheory.L1.setToL1 hT) f
-- Mathlib.Analysis.Analytic.Composition
/-- An auxiliary function used in the definition of `sigmaEquivSigmaPi` below, associating to
two compositions `a` of `n` and `b` of `a.length`, and an index `i` bounded by the length of
`a.gather b`, the subcomposition of `a` made of those blocks belonging to the `i`-th block of
`a.gather b`.  -/
Composition.sigmaCompositionAux : {n : ℕ} →
  (a : Composition n) →
    (b : Composition a.length) → (i : Fin (a.gather b).length) → Composition ((a.gather b).blocksFun i)
-- Init.Data.SInt.Basic
/-- Multiplies two 8-bit signed integers, wrapping around on over- or underflow.  Usually accessed via
the `*` operator.

This function is overridden at runtime with an efficient implementation.
 -/
Int8.mul : Int8 → Int8 → Int8
-- Mathlib.Data.Nat.Totient
Nat.totient_le : ∀ (n : ℕ), n.totient ≤ n
-- Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
/-- A strict Segal simplicial set is 2-coskeletal.  -/
SSet.StrictSegal.isPointwiseRightKanExtensionAt : {X : SSet} →
  X.StrictSegal →
    (n : ℕ) → (SSet.Truncated.rightExtensionInclusion X 2).IsPointwiseRightKanExtensionAt (Opposite.op { len := n })
-- Batteries.Recycling.RBTree.Lemmas
/-- The list of elements to the right of the hole.
(This function is intended for specification purposes only.)  -/
RBTree.RBNode.Path.listR : {α : Type u_1} → RBTree.RBNode.Path α → List α
-- Mathlib.Analysis.Normed.Group.Continuity
ContinuousAt.norm : ∀ {α : Type u_1} {E : Type u_4} [inst : SeminormedAddGroup E] [inst_1 : TopologicalSpace α] {f : α → E} {a : α},
  ContinuousAt f a → ContinuousAt (fun x => ‖f x‖) a
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
/-- The canonical embedding of a number field `K` of degree `n` into `ℂ^n`.  -/
NumberField.canonicalEmbedding : (K : Type u_1) → [inst : Field K] → K →+* (K →+* ℂ) → ℂ
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem!_toArray_rcc : ∀ {m n : ℤ} {i : ℕ}, (m...=n).toArray[i]! = if i < (n + 1 - m).toNat then m + ↑i else 0
-- Mathlib.Algebra.Order.Monoid.Lex
OrderMonoidHom.fst.eq_1 : ∀ (α : Type u_1) (β : Type u_2) [inst : Monoid α] [inst_1 : PartialOrder α] [inst_2 : Monoid β] [inst_3 : Preorder β],
  OrderMonoidHom.fst α β = { toMonoidHom := MonoidHom.fst α β, monotone' := ⋯ }
-- Lean.Elab.InfoTree.Main
Lean.Elab.DelabTermInfo.docString? : Lean.PPContext → Lean.Elab.DelabTermInfo → IO (Option String)
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.eval_single : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (r : R) (i : ℕ)
  (m : M), (PolynomialModule.eval r) (PolynomialModule.single R i m) = r ^ i • m
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.comp_sub : ∀ {R : Type u_1} [inst : Ring R] {R₂ : Type u_2} [inst_1 : Ring R₂] {R₃ : Type u_3} [inst_2 : Ring R₃] {M : Type u_4}
  [inst_3 : TopologicalSpace M] [inst_4 : AddCommGroup M] {M₂ : Type u_5} [inst_5 : TopologicalSpace M₂]
  [inst_6 : AddCommGroup M₂] {M₃ : Type u_6} [inst_7 : TopologicalSpace M₃] [inst_8 : AddCommGroup M₃]
  [inst_9 : Module R M] [inst_10 : Module R₂ M₂] [inst_11 : Module R₃ M₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃}
  {σ₁₃ : R →+* R₃} [inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_13 : IsTopologicalAddGroup M₂]
  [inst_14 : IsTopologicalAddGroup M₃] (g : M₂ →SL[σ₂₃] M₃) (f₁ f₂ : M →SL[σ₁₂] M₂),
  g ∘SL (f₁ - f₂) = g ∘SL f₁ - g ∘SL f₂
-- Mathlib.Data.Stream.Init
Stream'.eq_of_bisim : ∀ {α : Type u} (R : Stream' α → Stream' α → Prop), Stream'.IsBisimulation R → ∀ {s₁ s₂ : Stream' α}, R s₁ s₂ → s₁ = s₂
-- Mathlib.RingTheory.Extension.Presentation.Submersive
/-- If `algebraMap R S` is bijective, the empty generators are a submersive
presentation with no relations.  -/
Algebra.SubmersivePresentation.ofBijectiveAlgebraMap : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          Function.Bijective ⇑(algebraMap R S) → Algebra.SubmersivePresentation R S PEmpty.{w + 1} PEmpty.{t + 1}
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.ofInt_eq_intCast : ∀ {d : ℤ} (n : ℤ), Zsqrtd.ofInt n = ↑n
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.linMulLin_apply : ∀ {R : Type u_3} {M : Type u_4} {A : Type u_7} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : Module R A] [inst_5 : SMulCommClass R A A]
  [inst_6 : IsScalarTower R A A] (f g : M →ₗ[R] A) (x : M), (QuadraticMap.linMulLin f g) x = f x * g x
-- Mathlib.Data.Finsupp.Single
Finsupp.support_single_subset : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {a : α} {b : M}, (fun₀ | a => b).support ⊆ {a}
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.conductor_mem_conductorSet : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n), χ.conductor ∈ χ.conductorSet
-- Mathlib.Data.Finset.SMulAntidiagonal
Set.IsWF.vadd : ∀ {G : Type u_1} {P : Type u_2} [inst : LinearOrder G] [inst_1 : LinearOrder P] [inst_2 : VAdd G P] [IsOrderedVAdd G P]
  {s : Set G} {t : Set P}, s.IsWF → t.IsWF → (s +ᵥ t).IsWF
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.DiseqCnstrProof.erase_dup.inj : ∀ {c c_1 : Lean.Meta.Grind.AC.DiseqCnstr},
  Lean.Meta.Grind.AC.DiseqCnstrProof.erase_dup c = Lean.Meta.Grind.AC.DiseqCnstrProof.erase_dup c_1 → c = c_1
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.C_injective : ∀ {R : Type u} [inst : Semiring R], Function.Injective ⇑Polynomial.C
-- Mathlib.Algebra.Group.Int.Units
Int.mul_eq_neg_one_iff_eq_one_or_neg_one : ∀ {u v : ℤ}, u * v = -1 ↔ u = 1 ∧ v = -1 ∨ u = -1 ∧ v = 1
-- Mathlib.Algebra.Group.Pi.Lemmas
AddHom.piMap.eq_1 : ∀ {ι : Type u_1} {M : ι → Type u_3} {N : ι → Type u_4} [inst : (i : ι) → Add (M i)] [inst_1 : (i : ι) → Add (N i)]
  (g : (i : ι) → M i →ₙ+ N i), AddHom.piMap g = AddHom.pi fun i => (g i).comp (Pi.evalAddHom M i)
-- Std.Sync.Broadcast
Std.Broadcast.Error.notSubscribed.sizeOf_spec : sizeOf Std.Broadcast.Error.notSubscribed = 1
-- Mathlib.Order.Disjointed
disjointed_apply : ∀ {α : Type u_1} {ι : Type u_2} [inst : GeneralizedBooleanAlgebra α] [inst_1 : Preorder ι]
  [inst_2 : LocallyFiniteOrderBot ι] (f : ι → α) (i : ι), disjointed f i = f i \ (Finset.Iio i).sup f
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey?_insertIfNew : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  (↑m).WF →
    ∀ {k a : α} {v : β k},
      (m.insertIfNew k v).getKey? a = if (k == a) = true ∧ m.contains k = false then some k else m.getKey? a
-- Mathlib.Probability.Martingale.Centering
MeasureTheory.predictablePart_smul : ∀ {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {f : ℕ → Ω → E} {ℱ : MeasureTheory.Filtration ℕ m0} [CompleteSpace E] (c : ℝ) (n : ℕ),
  MeasureTheory.predictablePart (c • f) ℱ μ n =ᵐ[μ] c • MeasureTheory.predictablePart f ℱ μ n
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.Iio_one_default_eq : default = ⟨0, ⋯⟩
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
tsub_tsub_tsub_cancel_right : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α}, c ≤ b → a - c - (b - c) = a - b
-- Mathlib.Data.Multiset.MapFold
Multiset.mem_map_of_injective : ∀ {α : Type u_1} {β : Type v} {f : α → β},
  Function.Injective f → ∀ {a : α} {s : Multiset α}, f a ∈ Multiset.map f s ↔ a ∈ s
-- Mathlib.NumberTheory.LegendreSymbol.ZModChar
/-- If `n % 4 = 1`, then `χ₄ n = 1`.  -/
ZMod.χ₄_nat_one_mod_four : ∀ {n : ℕ}, n % 4 = 1 → ZMod.χ₄ ↑n = 1
-- Mathlib.Analysis.Normed.Group.Basic
enorm_mul₄_le' : ∀ {E : Type u_8} [inst : TopologicalSpace E] [inst_1 : ESeminormedMonoid E] {a b c d : E},
  ‖a * b * c * d‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ + ‖c‖ₑ + ‖d‖ₑ
-- Mathlib.Algebra.Order.GroupWithZero.Synonym
OrderDual.instIsRightCancelMulZero : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [IsRightCancelMulZero α], IsRightCancelMulZero αᵒᵈ
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- Two `R`-linear maps from `SkewMonoidAlgebra M α` which agree on each `single x y`
agree everywhere.  -/
SkewMonoidAlgebra.lhom_ext : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N]
  {α : Type u_6} [inst_3 : Module R M] [inst_4 : Module R N] ⦃φ ψ : SkewMonoidAlgebra M α →ₗ[R] N⦄,
  (∀ (a : α) (b : M), φ (SkewMonoidAlgebra.single a b) = ψ (SkewMonoidAlgebra.single a b)) → φ = ψ
-- Mathlib.Topology.NhdsWithin
eventually_eventually_nhdsWithin : ∀ {α : Type u_1} [inst : TopologicalSpace α] {a : α} {s : Set α} {p : α → Prop},
  (∀ᶠ (y : α) in nhdsWithin a s, ∀ᶠ (x : α) in nhdsWithin y s, p x) ↔ ∀ᶠ (x : α) in nhdsWithin a s, p x
-- Mathlib.Data.Complex.Basic
/-- This shortcut instance ensures we do not find `Ring` via the noncomputable `Complex.field`
instance.  -/
Complex.instRing : Ring ℂ
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isEmpty_iff_forall_not_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = true ↔ ∀ (a : α), a ∉ t
-- Mathlib.NumberTheory.LSeries.HurwitzZeta
HurwitzZeta.expZeta.eq_1 : ∀ (a : UnitAddCircle) (s : ℂ), HurwitzZeta.expZeta a s = HurwitzZeta.cosZeta a s + Complex.I * HurwitzZeta.sinZeta a s
-- Init.Data.Float.Float
/-- Converts a `Float` into a `Float.Model`.  -/
Float.toModel : Float → Float.Model
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
Submodule.map_orthogonal_equiv : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] (K : Submodule 𝕜 E)
  (f : E ≃ₗᵢ[𝕜] F), Submodule.map (↑f.toLinearEquiv) Kᗮ = (Submodule.map (↑f.toLinearEquiv) K)ᗮ
-- Mathlib.Control.Bitraversable.Instances
/-- The bitraverse function for `α ⊕ β`.  -/
Sum.bitraverse : {F : Type u → Type u} →
  [Applicative F] →
    {α : Type u_1} → {α' : Type u} → {β : Type u_2} → {β' : Type u} → (α → F α') → (β → F β') → α ⊕ β → F (α' ⊕ β')
-- Mathlib.LinearAlgebra.Projectivization.Independence
/-- Dependence is the negation of independence.  -/
Projectivization.dependent_iff_not_independent : ∀ {ι : Type u_1} {K : Type u_2} {V : Type u_3} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {f : ι → Projectivization K V}, Projectivization.Dependent f ↔ ¬Projectivization.Independent f
-- Mathlib.RingTheory.OrderOfVanishing.Noetherian
/-- For `x y : R` where `R` is a discrete valuation ring, we have that
`min (ord R x) (ord R y) ≤ ord R (x + y)`. It should be noted that the order
we're using here is the order on `ℕ∞`, where `⊤` is greater than everything else.
This is relevant since when we're working with `ordFrac` we work with `ℤᵐ⁰`, where the
order instance has the `0` element less than everything else.
 -/
Ring.ord_add : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [IsDiscreteValuationRing R] (x y : R),
  min (Ring.ord R x) (Ring.ord R y) ≤ Ring.ord R (x + y)
-- Mathlib.Order.Interval.Basic
NonemptyInterval.instSubsingleton : ∀ {α : Type u_1} [inst : LE α] [Subsingleton α], Subsingleton (NonemptyInterval α)
-- Init.Data.Vector.Attach
Vector.pmap_pmap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} {p : α → Prop} {q : β → Prop} {g : (a : α) → p a → β}
  {f : (b : β) → q b → γ} {xs : Vector α n} (H₁ : ∀ a ∈ xs, p a) (H₂ : ∀ a ∈ Vector.pmap g xs H₁, q a),
  Vector.pmap f (Vector.pmap g xs H₁) H₂ = Vector.pmap (fun a h => f (g (↑a) h) ⋯) xs.attach ⋯
-- Batteries.Data.Fin.Basic
/-- `findSomeRev? f` returns `f i` for the last `i` for which `f i` is `some _`, or `none` if no such
element is found. The function `f` is not evaluated on further inputs after the first `i` is found.
 -/
Fin.findSomeRev? : {n : ℕ} → {α : Type u_1} → (Fin n → Option α) → Option α
-- Lean.Widget.InteractiveGoal
Lean.Widget.InteractiveTermGoal.toInteractiveGoalCore : Lean.Widget.InteractiveTermGoal → Lean.Widget.InteractiveGoalCore
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_le_ediv_iff_of_dvd_of_neg_of_neg : ∀ {a b c d : ℤ}, b < 0 → d < 0 → b ∣ a → d ∣ c → (a / b ≤ c / d ↔ d * a ≤ c * b)
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
ApproximatesLinearOn.approximatesLinearOn_iff_lipschitzOnWith : ∀ {𝕜 : 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 ↔ LipschitzOnWith c (f - ⇑f') s
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.IterM.forIn_filterMapM : ∀ {α : Type u₁} {n : Type u₁ → Type u_1} {o : Type u₁ → Type u_2} {β₂ γ : Type u₁} {m : Type u₁ → Type u_3}
  {β : Type u₁} {ps : Std.Do.PostShape} [inst : Monad m] [LawfulMonad m] [inst_2 : Monad n] [LawfulMonad n]
  [inst_4 : Monad o] [LawfulMonad o] [inst_6 : Std.Do.WPMonad o ps] [inst_7 : MonadAttach n] [WeaklyLawfulMonadAttach n]
  [inst_9 : MonadLiftT m n] [LawfulMonadLiftT m n] [inst_11 : MonadLiftT n o] [LawfulMonadLiftT n o]
  [inst_13 : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_15 : Std.IteratorLoop α m o]
  [Std.LawfulIteratorLoop α m o] {it : Std.IterM m β} {f : β → n (Option β₂)} {init : γ} {g : β₂ → γ → o (ForInStep γ)}
  {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond γ ps},
  ⦃P⦄
      forIn it init fun out acc => do
        let __do_lift ← liftM (f out)
        match __do_lift with
          | some c => g c acc
          | none => pure (ForInStep.yield acc) ⦃Q⦄ →
    ⦃P⦄ forIn (Std.IterM.filterMapM f it) init g ⦃Q⦄
-- Mathlib.Data.Nat.GCD.BigOperators
Nat.coprime_fintype_prod_right_iff : ∀ {ι : Type u_1} [inst : Fintype ι] {x : ℕ} {s : ι → ℕ}, x.Coprime (∏ i, s i) ↔ ∀ (i : ι), x.Coprime (s i)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.maxEntry!_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited (α × β)], t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.maxEntry! = t₂.maxEntry!
-- Mathlib.Data.Fin.SuccPred
/-- `castSucc` commutes with `predAbove`.  -/
Fin.castSucc_predAbove_castSucc : ∀ {n : ℕ} (a : Fin n) (b : Fin (n + 1)), a.castSucc.predAbove b.castSucc = (a.predAbove b).castSucc
-- Mathlib.Algebra.Group.Prod
Prod.instAddCancelCommMonoid.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : AddCancelCommMonoid M] [inst_1 : AddCancelCommMonoid N],
  Prod.instAddCancelCommMonoid = { toAddCommMonoid := Prod.instAddCommMonoid, toIsLeftCancelAdd := ⋯ }
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Zipper.iter.eq_1 : ∀ {α : Type u} {β : α → Type v} (t : Std.DTreeMap.Internal.Zipper α β), t.iter = { internalState := t }
-- Mathlib.Topology.Filter
Filter.specializes_iff_le : ∀ {α : Type u_2} {l₁ l₂ : Filter α}, l₁ ⤳ l₂ ↔ l₁ ≤ l₂
-- Mathlib.Algebra.Group.Subgroup.Even
/-- In an abelian additive group `G`, `AddSubgroup.even G` is
the subgroup of even elements in `G`.  -/
AddSubgroup.even : (G : Type u_1) → [inst : AddCommGroup G] → AddSubgroup G
-- Mathlib.CategoryTheory.Limits.Filtered
CategoryTheory.Limits.hasCofilteredLimitsOfSize_of_univLE : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [UnivLE.{w, w₂}] [UnivLE.{w', w₂'}]
  [CategoryTheory.Limits.HasCofilteredLimitsOfSize.{w₂', w₂, v, u} C],
  CategoryTheory.Limits.HasCofilteredLimitsOfSize.{w', w, v, u} C
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- A countable union of analytic sets is analytic.  -/
MeasureTheory.AnalyticSet.iUnion : ∀ {α : Type u_1} {ι : Type u_2} [inst : TopologicalSpace α] [Countable ι] {s : ι → Set α},
  (∀ (n : ι), MeasureTheory.AnalyticSet (s n)) → MeasureTheory.AnalyticSet (⋃ n, s n)
-- Mathlib.Topology.UniformSpace.Basic
UniformSpace.toTopologicalSpace_sInf : ∀ {α : Type ua} {s : Set (UniformSpace α)}, (sInf s).toTopologicalSpace = ⨅ i ∈ s, i.toTopologicalSpace
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonCompletionItemKind : Lean.FromJson Lean.Lsp.CompletionItemKind
-- Mathlib.Probability.Martingale.Centering
MeasureTheory.martingalePart_bdd_difference : ∀ {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {R : ℝ} {f : ℕ → Ω → E} (ℱ : MeasureTheory.Filtration ℕ m0),
  (∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ‖f (i + 1) ω - f i ω‖ ≤ R) →
    ∀ᵐ (ω : Ω) ∂μ,
      ∀ (i : ℕ), ‖MeasureTheory.martingalePart f ℱ μ (i + 1) ω - MeasureTheory.martingalePart f ℱ μ i ω‖ ≤ 2 * R
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.isScalarTower : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L)
  {R : Type u_4} [inst_3 : Semiring R] [inst_4 : SMul R K] [inst_5 : Module R L] [inst_6 : IsScalarTower R K L],
  IsScalarTower R K ↥S
-- Std.Data.DTreeMap.Internal.Cell
Std.DTreeMap.Internal.Cell.mk.congr_simp : ∀ {α : Type u} [inst : Ord α] {β : α → Type v} {k : α → Ordering} (inner inner_1 : Option ((a : α) × β a))
  (e_inner : inner = inner_1)
  (property : ∀ [Std.OrientedOrd α] (p : (a : α) × β a), inner = some p → k p.fst = Ordering.eq),
  { inner := inner, property := property } = { inner := inner_1, property := ⋯ }
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.SMulInvariantMeasure.smul_nnreal : ∀ {M : Type v} {α : Type w} [inst : SMul M α] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [MeasureTheory.SMulInvariantMeasure M α μ] (c : NNReal), MeasureTheory.SMulInvariantMeasure M α (c • μ)
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
CategoryTheory.NonPreadditiveAbelian.lift_sub_lift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.NonPreadditiveAbelian C] {X Y : C}
  (a b c d : X ⟶ Y),
  CategoryTheory.Limits.prod.lift a b - CategoryTheory.Limits.prod.lift c d =
    CategoryTheory.Limits.prod.lift (a - c) (b - d)
-- Init.Data.List.Sublist
List.subset_append_right : ∀ {α : Type u_1} (l₁ l₂ : List α), l₂ ⊆ l₁ ++ l₂
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddSubsemigroup.subsingleton_of_subsingleton : ∀ {M : Type u_1} [inst : Add M] [Subsingleton (AddSubsemigroup M)], Subsingleton M
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.mk_ofAlgEquiv_symm_eq_evalOneₐ : ∀ {S : Type u_5} [inst : CommRing S] (I : Ideal S) [inst_1 : IsAdicComplete I S] (x : AdicCompletion I S),
  (Ideal.Quotient.mk I) ((AdicCompletion.ofAlgEquiv I).symm x) = (AdicCompletion.evalOneₐ I) x
-- Mathlib.Order.RelSeries
RelSeries.head_toList : ∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r), p.toList.head ⋯ = p.head
-- Mathlib.Algebra.Order.Group.Unbundled.Int
Int.abs_eq_natAbs : ∀ (a : ℤ), |a| = ↑a.natAbs
-- Std.Time.Duration
Std.Time.Duration.instHSubOffset_4 : HSub Std.Time.Duration Std.Time.Second.Offset Std.Time.Duration
-- Mathlib.Data.Int.GCD
/-- If `gcd a (m * n) = 1`, then `gcd a m = 1`.  -/
Int.gcd_eq_one_of_gcd_mul_right_eq_one_left : ∀ {a : ℤ} {m n : ℕ}, a.gcd (↑m * ↑n) = 1 → a.gcd ↑m = 1
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Take
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.Take.0.Std.Iterators.Types.Take.instIterator.match_1.eq_1 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] (it : Std.IterM m β)
  (motive : it.internalState.inner.Step → Sort u_3) (it' : Std.IterM m β) (out : β)
  (h' : it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) →
        (h' : it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out)) →
          motive ⟨Std.IterStep.yield it' out, h'⟩)
  (h_2 :
    (it' : Std.IterM m β) →
      (h' : it.internalState.inner.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h'⟩)
  (h_3 : (h' : it.internalState.inner.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h'⟩),
  (match ⟨Std.IterStep.yield it' out, h'⟩ with
    | ⟨Std.IterStep.yield it' out, h'⟩ => h_1 it' out h'
    | ⟨Std.IterStep.skip it', h'⟩ => h_2 it' h'
    | ⟨Std.IterStep.done, h'⟩ => h_3 h') =
    h_1 it' out h'
-- Mathlib.Data.Setoid.Partition
Setoid.IsPartition.sUnion_eq_univ : ∀ {α : Type u_1} {c : Set (Set α)}, Setoid.IsPartition c → ⋃₀ c = Set.univ
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- The order-preserving multiplicative equivalence between the `ValueGroup₀` of the completion's
valuation, pulled back along `equiv`, and that of the completion.  -/
IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupOrderIso : {R : Type u_1} →
  [inst : CommRing R] →
    [inst_1 : IsDedekindDomain R] →
      (K : Type u_2) →
        [inst_2 : Field K] →
          [inst_3 : Algebra R K] →
            [inst_4 : IsFractionRing R K] →
              (v : IsDedekindDomain.HeightOneSpectrum R) →
                (MonoidWithZeroHom.ofClass
                      (IsDedekindDomain.HeightOneSpectrum.adicCompletion.valuation K v)).ValueGroup₀ ≃*o
                  (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀
-- Mathlib.Combinatorics.SimpleGraph.StronglyRegular
SimpleGraph.IsSRGWith.mk : ∀ {V : Type u} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] {n k ℓ μ : ℕ},
  Fintype.card V = n →
    G.IsRegularOfDegree k →
      (∀ (v w : V), G.Adj v w → Fintype.card ↑(G.commonNeighbors v w) = ℓ) →
        (Pairwise fun v w => ¬G.Adj v w → Fintype.card ↑(G.commonNeighbors v w) = μ) → G.IsSRGWith n k ℓ μ
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.d_normEq0_cert.eq_1 : ∀ (c : ℕ) (p₁ p₂ p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.d_normEq0_cert c p₁ p₂ p =
    (p₂.beq' (Lean.Grind.CommRing.Poly.num ↑c)).and' (p.beq' (p₁.normEq0 c))