mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.instIsFiniteMeasureOnCompactsRestrict : ∀ {α : Type u_1} {m0 : MeasurableSpace α} [inst : TopologicalSpace α] {μ : MeasureTheory.Measure α}
  [MeasureTheory.IsFiniteMeasureOnCompacts μ] {s : Set α}, MeasureTheory.IsFiniteMeasureOnCompacts (μ.restrict s)
-- Mathlib.NumberTheory.Bernoulli
/-- Odd Bernoulli numbers (greater than 1) are zero.  -/
bernoulli'_eq_zero_of_odd : ∀ {n : ℕ}, Odd n → 1 < n → bernoulli' n = 0
-- Mathlib.Order.Defs.Unbundled
MaximalFor.prop : ∀ {ι : Sort u_1} {α : Type u_2} [inst : LE α] {P : ι → Prop} {f : ι → α} {i : ι}, MaximalFor P f i → P i
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence
/-- Stated for readability of `δ₁_apply`.  -/
groupHomology.mem_cycles₁_of_comp_eq_d₂₁ : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)},
  X.ShortExact →
    ∀ {y : G × G →₀ ↑X.X₂} {x : G →₀ ↑X.X₁},
      (Finsupp.mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap) x =
          (CategoryTheory.ConcreteCategory.hom (groupHomology.d₂₁ X.X₂)) y →
        x ∈ groupHomology.cycles₁ X.X₁
-- Mathlib.Order.Hom.WithTopBot
OrderIso.withBotCongr_symm : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : PartialOrder β] (e : α ≃o β),
  e.symm.withBotCongr = e.withBotCongr.symm
-- Mathlib.RepresentationTheory.Rep.Basic
/-- The representation on `α →₀ A` defined pointwise by a representation on `A`.  -/
Rep.finsupp : {k : Type u} →
  {G : Type v} → [inst : CommRing k] → [inst_1 : Monoid G] → Type u' → Rep.{u_1, u, v} k G → Rep.{max u' u_1, u, v} k G
-- Mathlib.LinearAlgebra.PiTensorProduct.DFinsupp
PiTensorProduct.ofDFinsuppEquiv.eq_1 : ∀ {R : Type u_1} {ι : Type u_2} {κ : ι → Type u_3} {M : (i : ι) → κ i → Type u_4} [inst : CommSemiring R]
  [inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)] [inst_2 : (i : ι) → (j : κ i) → Module R (M i j)]
  [inst_3 : Fintype ι] [inst_4 : DecidableEq ι] [inst_5 : (i : ι) → DecidableEq (κ i)],
  PiTensorProduct.ofDFinsuppEquiv =
    LinearEquiv.ofLinearMap
      (PiTensorProduct.lift
        ((MultilinearMap.fromDFinsuppEquiv κ R) fun p =>
          (DFinsupp.lsingle p).compMultilinearMap (PiTensorProduct.tprod R)))
      ((DFinsupp.lsum R) fun p =>
        PiTensorProduct.lift
          ((PiTensorProduct.map fun i => DFinsupp.lsingle (p i)).compMultilinearMap (PiTensorProduct.tprod R)))
      ⋯ ⋯
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.aevalTower_comp_C : ∀ {R : Type u} {S : Type v} {A' : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring A'] [inst_2 : CommSemiring S]
  [inst_3 : Algebra S R] [inst_4 : Algebra S A'] (g : R →ₐ[S] A') (y : A'),
  (↑(Polynomial.aevalTower g y)).comp Polynomial.C = ↑g
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyMapData.ofIsColimitCokernelCofork_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (hg₁ : S₁.g = 0)
  (c₁ : CategoryTheory.Limits.CokernelCofork S₁.f) (hc₁ : CategoryTheory.Limits.IsColimit c₁) (hg₂ : S₂.g = 0)
  (c₂ : CategoryTheory.Limits.CokernelCofork S₂.f) (hc₂ : CategoryTheory.Limits.IsColimit c₂) (f : c₁.pt ⟶ c₂.pt)
  (comm :
    CategoryTheory.CategoryStruct.comp φ.τ₂ (CategoryTheory.Limits.Cofork.π c₂) =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π c₁) f),
  (CategoryTheory.ShortComplex.HomologyMapData.ofIsColimitCokernelCofork φ hg₁ c₁ hc₁ hg₂ c₂ hc₂ f comm).left =
    CategoryTheory.ShortComplex.LeftHomologyMapData.ofIsColimitCokernelCofork φ hg₁ c₁ hc₁ hg₂ c₂ hc₂ f comm
-- Mathlib.AlgebraicGeometry.Morphisms.Proper
AlgebraicGeometry.IsProper.instFstScheme : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [AlgebraicGeometry.IsProper g],
  AlgebraicGeometry.IsProper (CategoryTheory.Limits.pullback.fst f g)
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.sum_sfiniteSeq : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [h : MeasureTheory.SFinite μ],
  MeasureTheory.Measure.sum (MeasureTheory.sfiniteSeq μ) = μ
-- Mathlib.RingTheory.WittVector.Basic
WittVector.mapFun.mul : ∀ {p : ℕ} {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Fact (Nat.Prime p)]
  (f : R →+* S) (x y : WittVector p R),
  WittVector.mapFun (⇑f) (x * y) = WittVector.mapFun (⇑f) x * WittVector.mapFun (⇑f) y
-- Mathlib.Data.ENat.Basic
ENat.lt_lift_iff : ∀ {x : ℕ} {n : ℕ∞} {h : n < ⊤}, x < n.lift h ↔ ↑x < n
-- Init.Grind.Ring.Basic
Lean.Grind.CommRing.toRing : {α : Type u} → [self : Lean.Grind.CommRing α] → Lean.Grind.Ring α
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.setRoot.match_1.eq_2 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (c : RBTree.RBColor) (a : RBTree.RBNode α) (v : α)
  (b : RBTree.RBNode α) (h_1 : Unit → motive RBTree.RBNode.nil)
  (h_2 :
    (c : RBTree.RBColor) →
      (a : RBTree.RBNode α) → (v : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node c a v b)),
  (match RBTree.RBNode.node c a v b with
    | RBTree.RBNode.nil => h_1 ()
    | RBTree.RBNode.node c a v b => h_2 c a v b) =
    h_2 c a v b
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.exists_eq_of_iSup_eq_of_not_isSuccPrelimit : ∀ {ι : Type u} (f : ι → Cardinal.{v}) (ω : Cardinal.{v}), ¬Order.IsSuccPrelimit ω → ⨆ i, f i = ω → ∃ i, f i = ω
-- Mathlib.Algebra.Star.Subalgebra
StarAlgebra.adjoin_nonUnitalStarSubalgebra_eq_span : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] (s : NonUnitalStarSubalgebra R A),
  Subalgebra.toSubmodule (StarAlgebra.adjoin R ↑s).toSubalgebra = R ∙ 1 ⊔ s.toSubmodule
-- Init.Data.Nat.Div.Basic
Nat.div_eq_of_lt_le : ∀ {k n m : ℕ}, k * n ≤ m → m < (k + 1) * n → m / n = k
-- Mathlib.MeasureTheory.Measure.Prod
/-- Two finite measures on a product `(α × β) × γ` that are equal on products of sets are equal.
See `ext_prod₃` for the same statement for `α × β × γ`.  -/
MeasureTheory.Measure.ext_prod₃' : ∀ {α : Type u_4} {β : Type u_5} {γ : Type u_6} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {μ ν : MeasureTheory.Measure ((α × β) × γ)} [MeasureTheory.IsFiniteMeasure μ],
  (∀ {s : Set α} {t : Set β} {u : Set γ},
      MeasurableSet s → MeasurableSet t → MeasurableSet u → μ ((s ×ˢ t) ×ˢ u) = ν ((s ×ˢ t) ×ˢ u)) →
    μ = ν
-- Mathlib.GroupTheory.IsSubnormal
/-- A normal additive subgroup is subnormal.  -/
AddSubgroup.Normal.isSubnormal : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, H.Normal → H.IsSubnormal
-- Mathlib.Data.Finset.Sups
Finset.sups_inter_subset_right : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] {s t₁ t₂ : Finset α},
  s ⊻ (t₁ ∩ t₂) ⊆ s ⊻ t₁ ∩ s ⊻ t₂
-- Mathlib.Data.Analysis.Filter
Filter.Realizer.ofEquiv_σ : ∀ {α : Type u_1} {τ : Type u_4} {f : Filter α} (F : f.Realizer) (E : F.σ ≃ τ), (F.ofEquiv E).σ = τ
-- Mathlib.RingTheory.ClassGroup.Basic
ClassGroup.mk0.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDedekindDomain R],
  ClassGroup.mk0 = ClassGroup.mk0
-- Mathlib.AlgebraicGeometry.Fiber
AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatFiberOfQuasiCompact : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.QuasiCompact f] (y : ↥Y),
  CompactSpace ↥(AlgebraicGeometry.Scheme.Hom.fiber f y)
-- Mathlib.LinearAlgebra.AffineSpace.Pointwise
AffineSubspace.coe_smul : ∀ {M : Type u_1} {k : Type u_2} {V : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : DistribSMul M V] [inst_4 : SMulCommClass M k V] (a : M) (s : AffineSubspace k V), ↑(a • s) = a • ↑s
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.compLinearMapₗ_apply : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₁' : ι → Type v₁'} {M₂ : Type v₂} [inst : CommSemiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : (i : ι) → AddCommMonoid (M₁' i)] [inst_6 : (i : ι) → Module R (M₁' i)]
  (f : (i : ι) → M₁ i →ₗ[R] M₁' i) (g : MultilinearMap R M₁' M₂),
  (MultilinearMap.compLinearMapₗ f) g = g.compLinearMap f
-- Mathlib.Data.Nat.Fib.Basic
/-- **Alias** of `Nat.fastFibAux_bit_false`. -/
Nat.fast_fib_aux_bit_ff : ∀ (n : ℕ),
  (Nat.bit false n).fastFibAux =
    have p := n.fastFibAux;
    (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2)
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- The isomorphism between `(G.mapComposableArrows 1).obj (.mk₁ f)` and
`.mk₁ (G.map f)`.  -/
CategoryTheory.Functor.mapComposableArrowsObjMk₁Iso : {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] →
        (G : CategoryTheory.Functor C D) →
          {X Y : C} →
            (f : X ⟶ Y) →
              (G.mapComposableArrows 1).obj (CategoryTheory.ComposableArrows.mk₁ f) ≅
                CategoryTheory.ComposableArrows.mk₁ (G.map f)
-- Mathlib.RingTheory.MvPolynomial.Basic
MvPolynomial.restrictSupport_zero : ∀ {σ : Type u} (R : Type v) [inst : CommSemiring R], MvPolynomial.restrictSupport R 0 = 1
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
/-- subsumed by `IdealSheafData.map_ideal` below.  -/
_private.Mathlib.AlgebraicGeometry.IdealSheaf.Basic.0.AlgebraicGeometry.Scheme.IdealSheafData.map_ideal_basicOpen_of_eq : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) {U V : ↑X.affineOpens} (f : ↑(X.presheaf.obj (Opposite.op ↑U)))
  (hV : V = X.affineBasicOpen f),
  Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (CategoryTheory.homOfLE ⋯).op)) (I.ideal U) = I.ideal V
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
MeasurableSet.Subtype.instEmptyCollection : {α : Type u_1} → [inst : MeasurableSpace α] → EmptyCollection (Subtype MeasurableSet)
-- Mathlib.Data.Finsupp.ToDFinsupp
finsuppAddEquivDFinsupp_apply : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : AddZeroClass M] [inst_2 : (m : M) → Decidable (m ≠ 0)],
  ⇑finsuppAddEquivDFinsupp = Finsupp.toDFinsupp
-- Batteries.Data.Array.Lemmas
Array.size_eraseIdxIfInBounds : ∀ {α : Type u_1} (a : Array α) (i : ℕ), (a.eraseIdxIfInBounds i).size = if i < a.size then a.size - 1 else a.size
-- Lean.DocString.Types
/-- A code block.
 -/
Lean.Doc.Block.code : {i : Type u} → {b : Type v} → String → Lean.Doc.Block i b
-- Init.Data.Nat.Lcm
Nat.lcm_dvd_lcm_mul_right_left : ∀ (m n k : ℕ), m.lcm n ∣ (m * k).lcm n
-- Mathlib.Algebra.AffineMonoid.Basic
IsAffineMonoid.toFG : ∀ {M : Type u_1} {inst : CommMonoid M} [self : IsAffineMonoid M], Monoid.FG M
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.isLittleOTVS_fun_neg_left : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {l : Filter α} {f : α → E} {g : α → F} [ContinuousNeg E],
  (fun x => -f x) =o[𝕜; l] g ↔ f =o[𝕜; l] g
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.ceil_eq_zero : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] {a : R}, ⌈a⌉₊ = 0 ↔ a ≤ 0
-- Std.Do.Triple.SpecLemmas
/-- Helper definition for specifying loop invariants for loops with early return.

`for ... in ...` loops with early return of type `γ` elaborate to a call like this:
```lean
forIn (β := MProd (Option γ) ...) (b := ⟨none, ...⟩) collection loopBody
```
Note that the first component of the `MProd` state tuple is the optional early return value.
It is `none` as long as there was no early return and `some r` if the loop returned early with `r`.

This function allows to specify different invariants for the loop body depending on whether the loop
terminated early or not. When there was an early return, the loop has effectively finished, which is
encoded by the additional `⌜pos = s.endPos⌝` assertion in the invariant. This assertion is vital for
successfully proving the induction step, as it contradicts with the assumption that
`pos ≠ s.endPos` of the inductive hypothesis at the start of the loop body, meaning that users
won't need to prove anything about the bogus case where the loop has returned early yet takes
another iteration of the loop body.
 -/
Std.Do.StringInvariant.withEarlyReturn : {β : Type (max u₁ u₂)} →
  {ps : Std.Do.PostShape} →
    {γ : Type (max u₁ u₂)} →
      {s : String} →
        (s.Pos → β → Std.Do.Assertion ps) →
          (γ → β → Std.Do.Assertion ps) →
            optParam (Std.Do.ExceptConds ps) Std.Do.ExceptConds.false → Std.Do.StringInvariant s (MProd (Option γ) β) ps
-- Std.Data.TreeSet.Raw.Basic
/-- Tries to retrieve the smallest element that is greater than the given element,
returning `fallback` if no such element exists.
 -/
Std.TreeSet.Raw.getGTD : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet.Raw α cmp → α → α → α
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.map_lsingle : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (R' : Type u_6)
  {M' : Type u_7} [inst_3 : CommRing R'] [inst_4 : AddCommGroup M'] [inst_5 : Module R' M'] [inst_6 : Module R M']
  (f : M →ₗ[R] M') (i : ℕ) (m : M),
  (PolynomialModule.map R' f) ((PolynomialModule.lsingle R i) m) = (PolynomialModule.lsingle R' i) (f m)
-- Mathlib.SetTheory.Cardinal.Cofinality.Basic
Order.cof_eq_aleph0 : ∀ {α : Type u} [inst : LinearOrder α] [NoMaxOrder α] [Nonempty α] [Countable α], Order.cof α = Cardinal.aleph0
-- Mathlib.Algebra.Notation.Prod
Prod.mul_def : ∀ {M : Type u_8} {N : Type u_9} [inst : Mul M] [inst_1 : Mul N] (p q : M × N), p * q = (p.1 * q.1, p.2 * q.2)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Carry
Std.Tactic.BVDecide.BVExpr.bitblast.OverflowInput.mk : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} →
        (w : ℕ) → aig.BinaryRefVec w → aig.Ref → Std.Tactic.BVDecide.BVExpr.bitblast.OverflowInput aig
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
CategoryTheory.Limits.hasInitialChangeUniverse : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C]
  [h : CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete PEmpty.{w + 1}) C],
  CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete PEmpty.{w' + 1}) C
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.IsCycle₁.eq_1 : ∀ {G : Type u_1} {A : Type u_2} [inst : Inv G] [inst_1 : AddCommGroup A] [inst_2 : SMul G A] (x : G →₀ A),
  groupHomology.IsCycle₁ x = ((x.sum fun g a => g⁻¹ • a) = x.sum fun x a => a)
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.subConst_neg_right : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] (A B : Finset G), A.subConst (-B) = A.addConst B
-- Mathlib.Algebra.Homology.Bifunctor
HomologicalComplex.mapBifunctor.d₁_eq_zero : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D] {I₁ : Type u_4}
  {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂)
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [inst_8 : TotalComplexShape c₁ c₂ c]
  [inst_9 : K₁.HasMapBifunctor K₂ F c] [inst_10 : DecidableEq J] (i₁ : I₁) (i₂ : I₂) (j : J),
  ¬c₁.Rel i₁ (c₁.next i₁) → HomologicalComplex.mapBifunctor.d₁ K₁ K₂ F c i₁ i₂ j = 0
-- Init.Data.Float.Float
instSubFloat : Sub Float
-- Mathlib.Topology.Semicontinuity.Defs
/-- **Alias** of the forward direction of `upperSemicontinuousWithinAt_iff_frequently`. -/
UpperSemicontinuousWithinAt.frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f : α → β} {x : α} {s : Set α},
  UpperSemicontinuousWithinAt f s x → ∀ (y : β), (∃ᶠ (x' : α) in nhdsWithin x s, f x' ≥ y) → f x ≥ y
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHom.mul_apply : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : CoalgebraStruct R A] (φ ψ : A →ₗc[R] A) (x : A), (φ * ψ) x = φ (ψ x)
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddResult
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddResult.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insert.match_1.eq_1 : ∀ {n : ℕ} (motive : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n → Sort u_1)
  (clauses : Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)))
  (rupUnits ratUnits : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)))
  (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment)
  (h_1 :
    (clauses : Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n))) →
      (rupUnits ratUnits : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))) →
        (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) →
          motive { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments }),
  (match { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments } with
    | { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments } =>
      h_1 clauses rupUnits ratUnits assignments) =
    h_1 clauses rupUnits ratUnits assignments
-- Init.Data.SInt.Basic
/-- Bitwise left shift for word-sized signed integers. Usually accessed via the `<<<` operator.

Signed integers are interpreted as bitvectors according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.
 -/
ISize.shiftLeft : ISize → ISize → ISize
-- Mathlib.Order.Monotone.Monovary
antivaryOn_comm : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : ι → α} {g : ι → β}
  {s : Set ι}, AntivaryOn f g s ↔ AntivaryOn g f s
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.maxKey_modify_eq_maxKey : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {k : α} {f : β → β} {he : Std.ExtDTreeMap.Const.modify t k f ≠ ∅},
  (Std.ExtDTreeMap.Const.modify t k f).maxKey he = t.maxKey ⋯
-- Lean.DocString.Extension
Lean.VersoDocString.mk : Array (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock) →
  Array (Lean.Doc.Part Lean.ElabInline Lean.ElabBlock Empty) → Lean.VersoDocString
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.prodMulEquiv_apply : ∀ {G : Type u} [inst : Group G] {H : Type v} [inst_1 : Group H] (A : Subgroup G) (B : Subgroup H) [inst_2 : A.Normal]
  [inst_3 : B.Normal] (q : (G × H) ⧸ A.prod B),
  (QuotientGroup.prodMulEquiv A B) q = Quotient.liftOn' q (fun x => (↑x.1, ↑x.2)) ⋯
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.support_induce_subset_coe_preimage_support : ∀ {V : Type u_1} (G : SimpleGraph V) (s : Set V), (SimpleGraph.induce s G).support ⊆ Subtype.val ⁻¹' G.support
-- Mathlib.CategoryTheory.Extensive
CategoryTheory.types.finitaryExtensive : CategoryTheory.FinitaryExtensive (Type u)
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.coe_sInf : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : Module R M] (S : Set (ClosedSubmodule R M)), ↑(sInf S) = ⨅ s ∈ S, ↑s
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.UnitMonomial.toFun_nil_basis : ∀ (m : Tactic.ComputeAsymptotics.UnitMonomial), m.toFun [] = 1
-- Mathlib.Algebra.Notation.Indicator
Set.mulIndicator.eq_1 : ∀ {α : Type u_1} {M : Type u_3} [inst : One M] (s : Set α) (f : α → M) (x : α),
  s.mulIndicator f x = if x ∈ s then f x else 1
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.ObjectProperty.IsSeparating.mk_of_exists_colimitsOfShape : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.ObjectProperty C},
  (∀ (X : C), ∃ J x, P.colimitsOfShape J X) → P.IsSeparating
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile
Std.IterM.step_takeWhileM : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [inst_3 : Std.Iterator α m β] {it : Std.IterM m β} {P : β → m (ULift.{u_1, 0} Bool)},
  (Std.IterM.takeWhileM P it).step = do
    let __do_lift ← it.step
    match __do_lift.inflate with
      | ⟨Std.IterStep.yield it' out, h⟩ => do
        let __do_lift ← MonadAttach.attach (P out)
        match __do_lift with
          | ⟨{ down := true }, hP⟩ =>
            pure (Std.Shrink.deflate (Std.PlausibleIterStep.yield (Std.IterM.takeWhileM P it') out ⋯))
          | ⟨{ down := false }, hP⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.done ⋯))
      | ⟨Std.IterStep.skip it', h⟩ =>
        pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.takeWhileM P it') ⋯))
      | ⟨Std.IterStep.done, h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.done ⋯))
-- Init.Data.String.Iterate
_private.Init.Data.String.Iterate.0.String.Slice.RevPosIterator.finitenessRelation : {m : Type → Type u_1} → {s : String.Slice} → [inst : Pure m] → Std.Iterators.FinitenessRelation s.RevPosIterator m
-- Mathlib.Analysis.PSeries
/-- A sequence `u` has the property that its ratio of successive differences is bounded
when there is a positive real number `C` such that, for all n ∈ ℕ,
(u (n + 2) - u (n + 1)) ≤ C * (u (n + 1) - u n)
 -/
SuccDiffBounded : ℕ → (ℕ → ℕ) → Prop
-- Mathlib.Topology.Maps.Proper.Basic
/-- A closed embedding is proper.  -/
Topology.IsClosedEmbedding.isProperMap : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Topology.IsClosedEmbedding f → IsProperMap f
-- Mathlib.Probability.Kernel.Composition.MeasureComp
ProbabilityTheory.boolKernel_comp_measure : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) (π : MeasureTheory.Measure Bool),
  π.bind ⇑(ProbabilityTheory.Kernel.boolKernel μ ν) = π {true} • ν + π {false} • μ
-- Mathlib.Data.Multiset.AddSub
Multiset.eq_sub_of_add_eq : ∀ {α : Type u_1} [inst : DecidableEq α] {s t u : Multiset α}, s + t = u → s = u - t
-- Mathlib.Computability.DFA
DFA.eval_comap : ∀ {α : Type u} {σ : Type v} (M : DFA α σ) {α' : Type u_1} (f : α' → α) (x : List α'),
  (DFA.comap f M).eval x = M.eval (List.map f x)
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Extension.H1Cotangent.map_apply_coe : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {R' : Type u'} {S' : Type v'} [inst_3 : CommRing R'] [inst_4 : CommRing S'] [inst_5 : Algebra R' S']
  {P' : Algebra.Extension R' S'} [inst_6 : Algebra R R'] [inst_7 : Algebra S S'] [inst_8 : Algebra R S']
  [inst_9 : IsScalarTower R R' S'] (f : P.Hom P') (c : ↥P.cotangentComplex.ker),
  ↑((Algebra.Extension.H1Cotangent.map f) c) = (Algebra.Extension.Cotangent.map f) ↑c
-- Mathlib.Algebra.Star.Subalgebra
Subalgebra.mem_starClosure : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] (S : Subalgebra R A) {x : A},
  x ∈ S.starClosure ↔ x ∈ S ⊔ star S
-- Mathlib.Algebra.DirectSum.Module
DirectSum.IsInternal.collectedBasis_repr_of_mem : ∀ {R : Type u} [inst : Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] {A : ι → Submodule R M} (h : DirectSum.IsInternal A) {α : ι → Type u_2}
  (v : (i : ι) → Module.Basis (α i) R ↥(A i)) {x : M} {i : ι} {a : α i} (hx : x ∈ A i),
  ((h.collectedBasis v).repr x) ⟨i, a⟩ = ((v i).repr ⟨x, hx⟩) a
-- Mathlib.Data.ENNReal.Basic
ENNReal.toNNReal_top : ⊤.toNNReal = 0