mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pullback.diagonal_fst_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPullback f f] {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.diagonal f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f f) h) =
    h
-- Mathlib.Algebra.Category.BoolRing
/-- The type of morphisms in `BoolRing`.  -/
BoolRing.Hom : BoolRing → BoolRing → Type (max u_1 u_2)
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.LambdaTheoremArgs.apply.sizeOf_spec : sizeOf Mathlib.Meta.FunProp.LambdaTheoremArgs.apply = 1
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.iSup_lt_of_isRegular : ∀ {ι : Type u_1} {f : ι → Cardinal.{u_1}} {c : Cardinal.{u_1}},
  c.IsRegular → Cardinal.mk ι < c → (∀ (i : ι), f i < c) → iSup f < c
-- Mathlib.Topology.FiberBundle.Basic
FiberBundleCore.mem_localTrivAt_target : ∀ {ι : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  (Z : FiberBundleCore ι B F) (p : B × F) (b : B), p ∈ (Z.localTrivAt b).target ↔ p.1 ∈ (Z.localTrivAt b).baseSet
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
/-- Given `f₁ : X₁ ⟶ S`, `f₂ : X₂ ⟶ S`, `h : ChosenPullback f₁ f₂` and morphisms
`g₁ : Y ⟶ X₁`, `g₂ : Y ⟶ X₂` and `b : Y ⟶ S`, this structure contains a morphism
`Y ⟶ h.pullback` such that `f ≫ h.p₁ = g₁`, `f ≫ h.p₂ = g₂` and `f ≫ h.p = b`.
(This is nonempty only when `g₁ ≫ f₁ = g₂ ≫ f₂ = b`.)  -/
CategoryTheory.Limits.ChosenPullback.LiftStruct : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₁ X₂ S : C} →
      {f₁ : X₁ ⟶ S} →
        {f₂ : X₂ ⟶ S} → CategoryTheory.Limits.ChosenPullback f₁ f₂ → {Y : C} → (Y ⟶ X₁) → (Y ⟶ X₂) → (Y ⟶ S) → Type v
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get!_union_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : α → Type v} {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α], m₁.WF → m₂.WF → ∀ {k : α} [inst_3 : Inhabited (β k)], k ∉ m₁ → (m₁ ∪ m₂).get! k = m₂.get! k
-- Mathlib.AlgebraicGeometry.Morphisms.IsIso
AlgebraicGeometry.instIsZariskiLocalAtTargetMonomorphismsScheme : AlgebraicGeometry.IsZariskiLocalAtTarget (CategoryTheory.MorphismProperty.monomorphisms AlgebraicGeometry.Scheme)
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Result.mkEqTrans : Lean.Meta.Simp.Result → Lean.Meta.Simp.Result → Lean.MetaM Lean.Meta.Simp.Result
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.pure_injective : ∀ {α : Type u}, Function.Injective pure
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.GrothendieckTopology.ofArrows_mem_iff_isLocallySurjective_cofanIsColimitDesc_uliftYoneda_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {S : C}
  {ι : Type u_2} [Small.{max w v, u_2} ι] {X : ι → C} (f : (i : ι) → X i ⟶ S)
  {c : CategoryTheory.Limits.Cofan fun i => CategoryTheory.uliftYoneda.{w, v, u}.obj (X i)}
  (hc : CategoryTheory.Limits.IsColimit c),
  CategoryTheory.Sieve.ofArrows X f ∈ J S ↔
    CategoryTheory.Presheaf.IsLocallySurjective J
      (CategoryTheory.Limits.Cofan.IsColimit.desc hc fun i => CategoryTheory.uliftYoneda.{w, v, u}.map (f i))
-- Std.Data.Iterators.Lemmas.Producers.Slice
Std.Slice.fold_iter : ∀ {γ : Type u} {α β : Type v} {α_1 : Type u_1} {f : α_1 → β → α_1} {init : α_1}
  [inst : Std.ToIterator (Std.Slice γ) Id α β] [inst_1 : Std.Iterator α Id β] [inst_2 : Std.IteratorLoop α Id Id]
  [Std.Iterators.Finite α Id] {s : Std.Slice γ}, Std.Iter.fold f init s.iter = Std.Slice.foldl f init s
-- Init.Grind.Order
Lean.Grind.Order.le_lt_trans_k : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [inst_3 : Std.IsPreorder α]
  [inst_4 : Lean.Grind.Ring α] [Lean.Grind.OrderedRing α] {a b c : α} {k₁ k₂ : ℤ} (k : ℤ),
  a ≤ b + ↑k₁ → b < c + ↑k₂ → (k == k₂ + k₁) = true → a < c + ↑k
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.instSubsingleton : ∀ (K : Type u) [inst : CommRing K] [Subsingleton K], Subsingleton (RatFunc K)
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.takeWhile₂.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : List α × List β → Sort u_3) →
      (x : List α × List β) → ((as' : List α) → (bs' : List β) → motive (as', bs')) → motive x
-- Init.Data.SInt.Lemmas
Int8.toNatClampNeg_le : ∀ {a b : Int8}, a ≤ b → a.toNatClampNeg ≤ b.toNatClampNeg
-- Lean.Elab.PreDefinition.WF.GuessLex
/-- Explain what we found out about the recursive calls (mutual case)  -/
Lean.Elab.WF.GuessLex.explainMutualFailure : Array Lean.Name →
  Array (Array Lean.Elab.WF.GuessLex.BasicMeasure) → Array Lean.Elab.WF.GuessLex.RecCallCache → Lean.MetaM Std.Format
-- Mathlib.Topology.ContinuousMap.Units
ContinuousMap.addUnitsLift.eq_1 : ∀ {X : Type u_1} {M : Type u_2} [inst : TopologicalSpace X] [inst_1 : AddMonoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : ContinuousAdd M],
  ContinuousMap.addUnitsLift =
    {
      toFun := fun f =>
        { val := { toFun := fun x => ↑(f x), continuous_toFun := ⋯ },
          neg := { toFun := fun x => ↑(-f x), continuous_toFun := ⋯ }, val_neg := ⋯, neg_val := ⋯ },
      invFun := fun f =>
        { toFun := fun x => { val := ↑f x, neg := ↑(-f) x, val_neg := ⋯, neg_val := ⋯ }, continuous_toFun := ⋯ },
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Algebra.Homology.Localization
HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh_hom_app_quotient_obj_assoc : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] {ι : Type u_2} (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Preadditive C] [inst_2 : CategoryTheory.CategoryWithHomology C]
  [inst_3 : (HomologicalComplex.quasiIso C c).HasLocalization] [inst_4 : c.QFactorsThroughHomotopy C]
  (K : HomologicalComplex C c) (i : ι) {Z : C}
  (h : (HomotopyCategory.homologyFunctor C c i).obj ((HomotopyCategory.quotient C c).obj K) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      ((HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh C c i).hom.app ((HomotopyCategory.quotient C c).obj K))
      h =
    CategoryTheory.CategoryStruct.comp
      ((HomologicalComplexUpToQuasiIso.homologyFunctor C c i).map
        ((HomologicalComplexUpToQuasiIso.quotientCompQhIso C c).hom.app K))
      (CategoryTheory.CategoryStruct.comp ((HomologicalComplexUpToQuasiIso.homologyFunctorFactors C c i).hom.app K)
        (CategoryTheory.CategoryStruct.comp ((HomotopyCategory.homologyFunctorFactors C c i).inv.app K) h))
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey?_diff_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, k ∈ m₂ → (m₁ \ m₂).getKey? k = none
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.measurable_rnDerivAux_right : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ η : ProbabilityTheory.Kernel α γ) (a : α),
  Measurable fun x => κ.rnDerivAux η a x
-- Mathlib.Order.Hom.Bounded
TopHom.copy_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : Top α] [inst_1 : Top β] (f : TopHom α β) (f' : α → β) (h : f' = ⇑f),
  f.copy f' h = f
-- Mathlib.RingTheory.Congruence.Hom
/-- An isomorphism of algebras `e : M ≃ₐ[R] N` generates an isomorphism between quotient spaces,
if it is compatible with the relations.  -/
RingCon.congrₐ : {M : Type u_1} →
  {N : Type u_2} →
    (R : Type u_4) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring M] →
          [inst_2 : Algebra R M] →
            [inst_3 : Semiring N] →
              [inst_4 : Algebra R N] →
                {c : RingCon M} → {d : RingCon N} → (e : M ≃ₐ[R] N) → c = d.comap e → c.Quotient ≃ₐ[R] d.Quotient
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.coe_prod : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S] (s : NonUnitalSubring R)
  (t : NonUnitalSubring S), ↑(s.prod t) = ↑s ×ˢ ↑t
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.eq_append_of_dropPrefix?_bool_eq_some : ∀ {p : Char → Bool} {s : String} {res : String.Slice},
  s.dropPrefix? p = some res → ∃ c, s = String.singleton c ++ res.copy ∧ p c = true
-- Mathlib.Data.Set.Lattice
Set.biUnion_ge : ∀ {α : Type u_1} {ι : Type u_12} [inst : PartialOrder ι] (s : ι → Set α) (i : ι),
  ⋃ j, ⋃ (_ : j ≥ i), s j = s i ∪ ⋃ j, ⋃ (_ : j > i), s j
-- Mathlib.Data.Set.Defs
/-- The image of `s : Set α` by `f : α → β`, written `f '' s`, is the set of `b : β` such that
`f a = b` for some `a ∈ s`.  -/
Set.image : {α : Type u} → {β : Type v} → (α → β) → Set α → Set β
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Set.powersetCard.disjUnion.congr_simp : ∀ {α : Type u_1} {n m : ℕ} {s s_1 : ↑(Set.powersetCard α m)} (e_s : s = s_1) {t t_1 : ↑(Set.powersetCard α n)}
  (e_t : t = t_1) (hst : Disjoint ↑s ↑t), Set.powersetCard.disjUnion hst = Set.powersetCard.disjUnion ⋯
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.mulL.sizeOf_spec : ∀ (k : ℤ) (a : Int.Internal.Linear.Expr), sizeOf (Int.Internal.Linear.Expr.mulL k a) = 1 + sizeOf k + sizeOf a
-- Mathlib.Analysis.Normed.Group.Defs
ENormedMonoid.enorm_eq_zero : ∀ {E : Type u_8} {inst : TopologicalSpace E} [self : ENormedMonoid E] (x : E), ‖x‖ₑ = 0 ↔ x = 1
-- Mathlib.MeasureTheory.Measure.Haar.Unique
MeasureTheory.Measure.mul_haarScalarFactor_smul : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [LocallyCompactSpace G] (μ' μ : MeasureTheory.Measure G)
  [inst_6 : μ.IsHaarMeasure] [inst_7 : MeasureTheory.IsFiniteMeasureOnCompacts μ'] [inst_8 : μ'.IsMulLeftInvariant]
  {c : NNReal} (hc : c ≠ 0), c * μ'.haarScalarFactor (c • μ) = μ'.haarScalarFactor μ
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
/-- The Hurwitz zeta function is differentiable everywhere except at `s = 1`. This is true
even in the delicate case `a = 0` and `s = 0` (where the completed zeta has a pole, but this is
cancelled out by the Gamma factor).  -/
HurwitzZeta.differentiableAt_hurwitzZetaEven : ∀ (a : UnitAddCircle) {s : ℂ}, s ≠ 1 → DifferentiableAt ℂ (HurwitzZeta.hurwitzZetaEven a) s
-- Mathlib.CategoryTheory.PathCategory.Basic
CategoryTheory.composePath.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C},
  CategoryTheory.composePath Quiver.Path.nil = CategoryTheory.CategoryStruct.id X
-- Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
ContinuousAlternatingMap.norm_alternatizeUncurryFin_le : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ}
  (f : E →L[𝕜] E [⋀^Fin n]→L[𝕜] F), ‖ContinuousAlternatingMap.alternatizeUncurryFin f‖ ≤ (↑n + 1) * ‖f‖
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.range_snd_comp : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S),
  Set.range ⇑(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f g) g) =
    Set.range ⇑f ∩ Set.range ⇑g
-- Std.Tactic.BVDecide.LRAT.Internal.LRATChecker
Std.Tactic.BVDecide.LRAT.Internal.lratChecker : {α : Type u_1} →
  {β : Type u_2} →
    {σ : Type u_3} →
      [DecidableEq α] →
        [inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β] →
          [inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ] →
            [Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ] →
              σ → List (Std.Tactic.BVDecide.LRAT.Action β α) → Std.Tactic.BVDecide.LRAT.Internal.Result
-- Mathlib.MeasureTheory.Measure.AddContent
MeasureTheory.AddContent.extend_eq_top : ∀ {α : Type u_1} {C : Set (Set α)} {s : Set α} (hC : MeasureTheory.IsSetSemiring C)
  (m : MeasureTheory.AddContent ENNReal C), s ∉ C → (MeasureTheory.AddContent.extend hC m) s = ⊤
-- Std.Sync.Mutex
_private.Std.Sync.Mutex.0.Std.Mutex.mk : {α : Type} → IO.Ref α → Std.BaseMutex → Std.Mutex α
-- Mathlib.Analysis.Calculus.FDeriv.Add
hasFDerivAtFilter_const_add_iff : ∀ {𝕜 : 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} {L : Filter (E × E)} (c : F), HasFDerivAtFilter (fun x => c + f x) f' L ↔ HasFDerivAtFilter f f' L
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the reverse direction of `antivary_inv₀`. -/
Antivary.inv₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : Semifield β] [inst_4 : LinearOrder β] [IsStrictOrderedRing β] {f : ι → α} {g : ι → β},
  StrongLT 0 f → StrongLT 0 g → Antivary f g → Antivary f⁻¹ g⁻¹
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- A natural isomorphism `L₁ ≅ L₂` induces an equivalence of categories
`P.Comma L₁ R Q W ≌ P.Comma L₂ R Q W`.  -/
CategoryTheory.MorphismProperty.Comma.mapLeftIso : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    {B : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
        {T : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} T] →
            (R : CategoryTheory.Functor B T) →
              {P : CategoryTheory.MorphismProperty T} →
                {Q : CategoryTheory.MorphismProperty A} →
                  {W : CategoryTheory.MorphismProperty B} →
                    [inst_3 : Q.IsMultiplicative] →
                      [inst_4 : W.IsMultiplicative] →
                        {L₁ L₂ : CategoryTheory.Functor A T} →
                          [P.RespectsIso] →
                            [Q.RespectsIso] →
                              [W.RespectsIso] →
                                (L₁ ≅ L₂) →
                                  (CategoryTheory.MorphismProperty.Comma L₁ R P Q W ≌
                                    CategoryTheory.MorphismProperty.Comma L₂ R P Q W)
-- Mathlib.Algebra.Algebra.Operations
Submodule.pow_eq_npowRec : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] (M : Submodule R A) {n : ℕ}, M ^ n = npowRec n M
-- Mathlib.Algebra.Homology.SpectralObject.Differentials
CategoryTheory.Abelian.SpectralObject.Ψ_opcyclesMap_exact : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₁₂ : i ⟶ k)
  (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) (f₂₃ : j ⟶ l)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.Ψ_opcyclesMap_exact._auto_1),
  { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
      g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (CategoryTheory.ComposableArrows.threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁,
      zero := ⋯ }.Exact
-- Mathlib.Data.Fintype.Sets
/-- Given a fintype `α`, `finsetOrderIsoSet` is the order isomorphism between `Finset α` and `Set α`
(all sets on a finite type are finite).  -/
Fintype.finsetOrderIsoSet : {α : Type u_1} → [Fintype α] → Finset α ≃o Set α
-- Init.Data.UInt.Lemmas
UInt32.toUInt8_ofNatTruncate_of_le : ∀ {n : ℕ},
  UInt32.size ≤ n →
    (UInt32.ofNatClamp n).toUInt8 = UInt8.ofNatLT (UInt8.size - 1) UInt16.toUInt8_ofNatClamp_of_le._proof_1
-- Mathlib.Order.Interval.Set.Monotone
AntitoneOn.Iio : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  AntitoneOn f s → AntitoneOn (fun x => Set.Iio (f x)) s
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
/-- The top right map in the oplax associativity hexagon.
 -/
CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.secondMap₁ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          (F : CategoryTheory.Functor C D) →
            CategoryTheory.MonoidalCategory.curriedTensorPostPost F ⟶
              CategoryTheory.MonoidalCategory.curriedTensorPostPost' F
-- Init.Data.Int.Linear
/-- Returns the ceiling of the division `a / b`. That is, the result is equivalent to `⌈a / b⌉`.
Examples:
- `cdiv 7 3` returns `3`
- `cdiv (-7) 3` returns `-2`.
 -/
Int.Internal.Linear.cdiv : ℤ → ℤ → ℤ
-- Init.Data.Order.Lemmas
Std.instAntisymmLtOfLawfulOrderLTOfLe : ∀ {α : Type u} {x : LT α} [inst : LE α] [Std.LawfulOrderLT α] [Std.Antisymm fun x1 x2 => x1 ≤ x2],
  Std.Antisymm fun x1 x2 => x1 < x2
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtend.go.eq_def : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {outWidth : ℕ} {aig : Std.Sat.AIG α} {w : ℕ} (idx : ℕ)
  (x : aig.RefVec w) (acc : aig.RefVec (w * idx)) (h : idx ≤ w) (h' : outWidth = w * w),
  Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtend.go idx x acc h h' =
    if hidx : idx < w then
      let res := Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtendBit aig { start := idx, x := x };
      have this := ⋯;
      have aig_1 := res.aig;
      have bv := res.vec;
      have acc := acc.cast this;
      have x_1 := x.cast this;
      have acc := acc.append bv;
      have hcast := ⋯;
      have acc := ⋯ ▸ acc;
      Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtend.go (idx + 1) x_1 acc ⋯ h'
    else
      have hcast := ⋯;
      { aig := aig, vec := hcast ▸ acc }
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKeyD_map : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → γ} {k fallback : α},
  m.WF → (Std.HashMap.Raw.map f m).getKeyD k fallback = m.getKeyD k fallback
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.mul : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] (ctx : Lean.Grind.CommRing.Context α) (p₁ : Lean.Grind.CommRing.Poly)
  (k : ℤ) (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Stepwise.mul_cert p₁ k p = true →
    Lean.Grind.CommRing.Poly.denote ctx p₁ = 0 → Lean.Grind.CommRing.Poly.denote ctx p = 0
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsAtomic.rel : ∀ {L : FirstOrder.Language} {α : Type u'} {n l : ℕ} (R : L.Relations l) (ts : Fin l → L.Term (α ⊕ Fin n)),
  (R.boundedFormula ts).IsAtomic
-- Mathlib.Algebra.Order.Ring.Ordering.Basic
RingPreordering.isOrdering_iff : ∀ {R : Type u_1} [inst : CommRing R] {P : RingPreordering R}, P.IsOrdering ↔ ∀ (a b : R), -(a * b) ∈ P → a ∈ P ∨ b ∈ P
-- Mathlib.Algebra.Category.Ring.FinitePresentation
/-- If `S` is a finitely presented `R`-algebra, then `Hom_R(S, -)` preserves filtered colimits.  -/
CommRingCat.preservesColimit_coyoneda_of_finitePresentation : ∀ {J : Type uJ} [inst : CategoryTheory.Category.{vJ, uJ} J] [CategoryTheory.IsFiltered J] (R : CommRingCat)
  (S : CategoryTheory.Under R),
  (CommRingCat.Hom.hom S.hom).FinitePresentation →
    ∀ (F : CategoryTheory.Functor J (CategoryTheory.Under R))
      [CategoryTheory.Limits.PreservesColimit (F.comp (CategoryTheory.Under.forget R))
          (CategoryTheory.forget CommRingCat)],
      CategoryTheory.Limits.PreservesColimit F (CategoryTheory.coyoneda.obj (Opposite.op S))
-- Mathlib.Data.Finset.NoncommProd
Multiset.map_noncommProd_aux : ∀ {F : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Monoid α] [inst_1 : Monoid β] [inst_2 : FunLike F α β]
  [MulHomClass F α β] (s : Multiset α),
  {x | x ∈ s}.Pairwise Commute → ∀ (f : F), {x | x ∈ Multiset.map (⇑f) s}.Pairwise Commute
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.mul : ∀ {α : Type u_1} {β : Type u_2} {f g : α → β} {c : α} [inst : Add α] [inst_1 : Mul β],
  Function.Periodic f c → Function.Periodic g c → Function.Periodic (f * g) c
-- Lean.Data.Lsp.Internal
/-- Module that `decl` is defined in.  -/
Lean.Lsp.LeanIdentifier.module : Lean.Lsp.LeanIdentifier → Lean.Name
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.sign_ne_zero_iff : ∀ {θ : Real.Angle}, θ.sign ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ ↑Real.pi
-- Mathlib.Algebra.Order.Ring.Defs
IsStrictOrderedRing.isDomain : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [ExistsAddOfLE R], IsDomain R
-- Mathlib.Order.PiLex
Pi.Colex.noMaxOrder' : ∀ {ι : Type u_1} {β : ι → Type u_2} [inst : Preorder ι] [inst_1 : (i : ι) → LT (β i)] (i : ι) [NoMaxOrder (β i)],
  NoMaxOrder (Colex ((i : ι) → β i))
-- Mathlib.GroupTheory.Finiteness
/-- An additive group is finitely generated iff there exists a surjective homomorphism
from a `FreeAddGroup` on an arbitrary finite type `α` to the group.  -/
AddGroup.fg_iff_exists_freeAddGroup_hom_surjective_finite : ∀ {G : Type u_3} [inst : AddGroup G], AddGroup.FG G ↔ ∃ α, ∃ (_ : Finite α), ∃ φ, Function.Surjective ⇑φ
-- Mathlib.AlgebraicGeometry.Morphisms.Constructors
AlgebraicGeometry.stalkwise_SpecMap_iff : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P) →
    ∀ {R S : CommRingCat} (φ : R ⟶ S),
      AlgebraicGeometry.stalkwise (fun {R S} [CommRing R] [CommRing S] => P) (AlgebraicGeometry.Spec.map φ) ↔
        ∀ (p : Ideal ↑S) (x : p.IsPrime),
          P (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) p) p (CommRingCat.Hom.hom φ) ⋯)
-- Mathlib.Data.List.Forall2
List.rel_flatMap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {R : α → β → Prop} {P : γ → δ → Prop},
  Relator.LiftFun (List.Forall₂ R) (Relator.LiftFun (Relator.LiftFun R (List.Forall₂ P)) (List.Forall₂ P))
    (Function.swap List.flatMap) (Function.swap List.flatMap)
-- Mathlib.Data.Vector.Zip
List.Vector.zipWith_toList : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} (f : α → β → γ) (x : List.Vector α n) (y : List.Vector β n),
  (List.Vector.zipWith f x y).toList = List.zipWith f x.toList y.toList
-- Lean.Meta.Tactic.Grind.AC.Seq
Lean.Grind.AC.SubseqResult.exact.sizeOf_spec : sizeOf Lean.Grind.AC.SubseqResult.exact = 1
-- Lean.Compiler.IR.Basic
Lean.IR.LocalContextEntry.localVar.sizeOf_spec : ∀ (a : Lean.IR.IRType) (a_1 : Lean.IR.Expr),
  sizeOf (Lean.IR.LocalContextEntry.localVar a a_1) = 1 + sizeOf a + sizeOf a_1
-- Mathlib.Control.Basic
fish_pure : ∀ {m : Type u → Type v} [inst : Monad m] [LawfulMonad m] {α : Type u_1} {β : Type u} (f : α → m β), f >=> pure = f
-- Mathlib.Tactic.NormNum.Result
/-- Assert that an element of a ring is equal to `num / denom`
(and `denom` is invertible so that this makes sense).
We will usually also have `num` and `denom` coprime,
although this is not part of the definition.
 -/
Mathlib.Meta.NormNum.IsRat : {α : Type u} → [Ring α] → α → ℤ → ℕ → Prop
-- Mathlib.GroupTheory.Index
Subgroup.inf_relIndex_left : ∀ {G : Type u_1} [inst : Group G] (H K : Subgroup G), (H ⊓ K).relIndex H = K.relIndex H
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapRightIso_functor_obj_left : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  {R₁ R₂ : CategoryTheory.Functor B T} (i : R₁ ≅ R₂) (X : CategoryTheory.Comma L R₁),
  ((CategoryTheory.Comma.mapRightIso L i).functor.obj X).left = X.left
-- Init.Data.SInt.Lemmas
Int16.le_refl : ∀ (a : Int16), a ≤ a
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
DihedralGroup.sr.sizeOf_spec : ∀ {n : ℕ} (a : ZMod n), sizeOf (DihedralGroup.sr a) = 1 + sizeOf a
-- Mathlib.Data.Int.Init
_private.Mathlib.Data.Int.Init.0.Int.inductionOn'.pos.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Line.coe_apply : ∀ {α : Type u_2} {ι : Type u_3} (l : Combinatorics.Line α ι) (x : α) (i : ι), ↑l x i = (l.idxFun i).getD x