mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.SpectralObject.Differentials
CategoryTheory.Abelian.SpectralObject.d_ιE_fromOpcycles_assoc : ∀ {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₀ i₁ i₂ i₃ i₄ i₅ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (f₃₄ : i₂ ⟶ i₄),
  CategoryTheory.CategoryStruct.comp f₃ f₄ = f₃₄ →
    ∀ (f₄₅ : i₃ ⟶ i₅) (h₄₅ : CategoryTheory.CategoryStruct.comp f₄ f₅ = f₄₅) (n₀ n₁ n₂ n₃ : ℤ)
      (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.d_ιE_fromOpcycles._auto_1)
      (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.d_ιE_fromOpcycles._auto_3)
      (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.d_ιE_fromOpcycles._auto_5) {Z : C}
      (h : (X.H n₂).obj (CategoryTheory.ComposableArrows.mk₁ f₂₃) ⟶ Z),
      CategoryTheory.CategoryStruct.comp (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃)
          (CategoryTheory.CategoryStruct.comp (X.ιE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃)
            (CategoryTheory.CategoryStruct.comp (X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₂) h)) =
        CategoryTheory.CategoryStruct.comp (X.ιE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂)
          (CategoryTheory.CategoryStruct.comp (X.fromOpcycles f₄ f₅ f₄₅ h₄₅ n₁)
            (CategoryTheory.CategoryStruct.comp (X.δ f₂₃ f₄₅ n₁ n₂ hn₂) h))
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.symm_comp_cancel_left : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_8} {M₂ : Type u_9} {M₃ : Type u_10} [inst : Semiring R₁]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃}
  {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₃₁ : R₃ →+* R₁} {σ₃₂ : R₃ →+* R₂} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
  {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} [inst_6 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] [inst_7 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂]
  (e : M₁ ≃ₛₗ[σ₁₂] M₂) (f : M₃ →ₛₗ[σ₃₁] M₁), ↑e.symm ∘ₛₗ ↑e ∘ₛₗ f = f
-- Mathlib.Data.Multiset.AddSub
/-- This is a special case of `tsub_le_iff_left`, which should be used instead of this.  -/
Multiset.sub_le_iff_le_add' : ∀ {α : Type u_1} [inst : DecidableEq α] {s t u : Multiset α}, s - t ≤ u ↔ s ≤ t + u
-- Aesop.Util.UnorderedArraySet
/-- O(n)  -/
Aesop.UnorderedArraySet.all : {α : Type u_1} → [inst : BEq α] → (α → Bool) → (s : Aesop.UnorderedArraySet α) → optParam ℕ 0 → optParam ℕ s.size → Bool
-- Mathlib.Analysis.Convex.Side
AffineSubspace.WSameSide.map : ∀ {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [inst : CommRing R]
  [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V]
  [inst_5 : AddTorsor V P] [inst_6 : AddCommGroup V'] [inst_7 : Module R V'] [inst_8 : AddTorsor V' P']
  {s : AffineSubspace R P} {x y : P},
  s.WSameSide x y → ∀ (f : P →ᵃ[R] P'), (AffineSubspace.map f s).WSameSide (f x) (f y)
-- Mathlib.RingTheory.PowerSeries.WellKnown
PowerSeries.cos.eq_1 : ∀ (A : Type u_1) [inst : Ring A] [inst_1 : Algebra ℚ A],
  PowerSeries.cos A = PowerSeries.mk fun n => if Even n then (algebraMap ℚ A) ((-1) ^ (n / 2) / ↑n.factorial) else 0
-- Init.Data.BitVec.Lemmas
BitVec.msb_zero : ∀ {w : ℕ}, (0#w).msb = false
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonRpcConnected.toJson : Lean.Lsp.RpcConnected → Lean.Json
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.gcd_eq_zero_iff : ∀ {R : Type u} [inst : EuclideanDomain R] [inst_1 : DecidableEq R] {a b : R},
  EuclideanDomain.gcd a b = 0 ↔ a = 0 ∧ b = 0
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.isOrthoᵢ_def : ∀ {R : Type u_1} {R₁ : Type u_2} {M : Type u_5} {M₁ : Type u_6} {n : Type u_19} [inst : CommSemiring R]
  [inst_1 : CommSemiring R₁] [inst_2 : AddCommMonoid M₁] [inst_3 : Module R₁ M₁] [inst_4 : AddCommMonoid M]
  [inst_5 : Module R M] {I₁ I₁' : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] M} {v : n → M₁},
  B.IsOrthoᵢ v ↔ ∀ (i j : n), i ≠ j → (B (v i)) (v j) = 0
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.contains_maxKey : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {he : t ≠ ∅}, t.contains (t.maxKey he) = true
-- Mathlib.CategoryTheory.Galois.Decomposition
CategoryTheory.Limits.Concrete.productEquiv.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type (max w v)}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {J : Type w}
  (F : J → C) [inst_3 : CategoryTheory.Limits.HasProduct F]
  [inst_4 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor F) (CategoryTheory.forget C)],
  CategoryTheory.Limits.Concrete.productEquiv F = CategoryTheory.Limits.Concrete.productEquiv F
-- Init.Data.Range.Polymorphic.Internal.SignedBitVec
_private.Init.Data.Range.Polymorphic.Internal.SignedBitVec.0.BitVec.Signed.rotate_intMaxSealed : ∀ {n : ℕ}, BitVec.Signed.rotate✝ (BitVec.Signed.intMaxSealed✝ n) = ↑(2 ^ n - 1)
-- Init.Data.Array.Lemmas
Array.foldr_reverse : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → β → β} {b : β},
  Array.foldr f b xs.reverse = Array.foldl (fun x y => f y x) b xs
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.map_smul_of_iInf_genEigenspace_ne_bot : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsDomain R]
  [Module.IsTorsionFree R M] {L : Type u_1} {F : Type u_2} [inst_5 : SMul R L] [inst_6 : FunLike F L (Module.End R M)]
  [MulActionHomClass F R L (Module.End R M)] (f : F) (μ : L → R) (k : ℕ∞),
  ⨅ x, ((f x).genEigenspace (μ x)) k ≠ ⊥ → ∀ (t : R) (x : L), μ (t • x) = t • μ x
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.contained_proj : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] (o : Ordinal.{u}),
  Profinite.NobelingProof.contained (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o) o
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Returns the first output of the iterator, or `none` if no such output is found.

`O(|it|)` since the iterator may skip an unknown number of times before returning a result.
Short-circuits upon encountering the first result. The elements in `it` are examined in order of
iteration.

This variant terminates after finitely many steps and requires a proof that the iterator is
productive. If such a proof is not available, consider using `IterM.first?`.

Examples:
* `([7, 6].iterM Id).first? = pure (some 7)`
* `([].iterM Id).first? = pure none`
 -/
Std.IterM.Total.first? : {α β : Type w} →
  {m : Type w → Type w'} →
    [Monad m] →
      [inst : Std.Iterator α m β] →
        [Std.IteratorLoop α m m] → [Std.Iterators.Productive α m] → Std.IterM.Total m β → m (Option β)
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.toLp.sizeOf_spec : ∀ (p : ENNReal) {V : Type u_1} [inst : SizeOf V] (ofLp : V), sizeOf (WithLp.toLp p ofLp) = 1 + sizeOf ofLp
-- Mathlib.Topology.Connected.PathConnected
pathComponentIn.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] (F : Set X) (x : X), pathComponentIn F x = {y | JoinedIn F x y}
-- Mathlib.AlgebraicGeometry.Stalk
AlgebraicGeometry.Scheme.SpecMap_stalkSpecializes_fromSpecStalk : ∀ {X : AlgebraicGeometry.Scheme} {x y : ↥X} (h : x ⤳ y),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (X.presheaf.stalkSpecializes h)) (X.fromSpecStalk y) =
    X.fromSpecStalk x
-- Lean.Meta.IndPredBelow
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.NewDecl.getDecl : Lean.Meta.IndPredBelow.NewDecl✝ → Lean.LocalDecl
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToCodeBlock.checkReassignable : Array Lean.Elab.Term.Do.Var → Lean.Elab.Term.Do.ToCodeBlock.M Unit
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsFundamentalDomain.image_of_equiv : ∀ {G : Type u_1} {H : Type u_2} {α : Type u_3} {β : Type u_4} [inst : Group G] [inst_1 : Group H]
  [inst_2 : MulAction G α] [inst_3 : MeasurableSpace α] [inst_4 : MulAction H β] [inst_5 : MeasurableSpace β]
  {s : Set α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β},
  MeasureTheory.IsFundamentalDomain G s μ →
    ∀ (f : α ≃ β),
      MeasureTheory.Measure.QuasiMeasurePreserving (⇑f.symm) ν μ →
        ∀ (e : H ≃ G),
          (∀ (g : H), Function.Semiconj (⇑f) (fun x => e g • x) fun x => g • x) →
            MeasureTheory.IsFundamentalDomain H (⇑f '' s) ν
-- Lean.Server.Rpc.Basic
Lean.Server.RpcObjectStore : Type
-- Mathlib.LinearAlgebra.RootSystem.Chain
RootPairing.root_add_zsmul_mem_range_iff : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : CharZero R] [inst_3 : IsDomain R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsCrystallographic] {i j : ι},
  LinearIndependent R ![P.root i, P.root j] →
    ∀ {z : ℤ},
      P.root j + z • P.root i ∈ Set.range ⇑P.root ↔
        z ∈ Set.Icc (-↑(RootPairing.chainBotCoeff i j)) ↑(RootPairing.chainTopCoeff i j)
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
OpenPartialHomeomorph.lift_openEmbedding_trans : ∀ {X : Type u_7} {X' : Type u_8} {Z : Type u_9} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace X']
  [inst_2 : TopologicalSpace Z] [inst_3 : Nonempty Z] {f : X → X'} (e e' : OpenPartialHomeomorph X Z)
  (hf : Topology.IsOpenEmbedding f), (e.lift_openEmbedding hf).symm.trans (e'.lift_openEmbedding hf) = e.symm.trans e'
-- Mathlib.MeasureTheory.Measure.Map
MeasureTheory.Measure.map_smul : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {R : Type u_4} [inst : SMul R ENNReal]
  [inst_1 : IsScalarTower R ENNReal ENNReal] (c : R) (μ : MeasureTheory.Measure α) (f : α → β),
  MeasureTheory.Measure.map f (c • μ) = c • MeasureTheory.Measure.map f μ
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval₂_finsetProd : ∀ {R : Type u} {S : Type v} {ι : Type y} [inst : CommSemiring R] [inst_1 : CommSemiring S] (f : R →+* S) (s : Finset ι)
  (g : ι → Polynomial R) (x : S), Polynomial.eval₂ f x (∏ i ∈ s, g i) = ∏ i ∈ s, Polynomial.eval₂ f x (g i)
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.DiseqCnstrProof.simp_ac.injEq : ∀ (lhs : Bool) (s : Lean.Grind.AC.Seq) (c₁ : Lean.Meta.Grind.AC.EqCnstr) (c₂ : Lean.Meta.Grind.AC.DiseqCnstr)
  (lhs_1 : Bool) (s_1 : Lean.Grind.AC.Seq) (c₁_1 : Lean.Meta.Grind.AC.EqCnstr) (c₂_1 : Lean.Meta.Grind.AC.DiseqCnstr),
  (Lean.Meta.Grind.AC.DiseqCnstrProof.simp_ac lhs s c₁ c₂ =
      Lean.Meta.Grind.AC.DiseqCnstrProof.simp_ac lhs_1 s_1 c₁_1 c₂_1) =
    (lhs = lhs_1 ∧ s = s_1 ∧ c₁ = c₁_1 ∧ c₂ = c₂_1)
-- Lean.MetavarContext
Lean.LevelMetavarDecl.mk.injEq : ∀ (depth index depth_1 index_1 : ℕ),
  ({ depth := depth, index := index } = { depth := depth_1, index := index_1 }) = (depth = depth_1 ∧ index = index_1)
-- Aesop.Tree.Tracing
Aesop.Goal.traceMetadata : Aesop.Goal → Aesop.TraceOption → Lean.MetaM Unit
-- Mathlib.CategoryTheory.Adjunction.FullyFaithful
CategoryTheory.Adjunction.instIsIsoMapAppCounitOfFaithfulOfFull : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) [L.Faithful] [L.Full] {Y : D},
  CategoryTheory.IsIso (R.map (h.counit.app Y))
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.BiconeMorphism.mk : {J : Type w} →
  {C : Type uC} →
    [inst : CategoryTheory.Category.{uC', uC} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {F : J → C} →
          {A B : CategoryTheory.Limits.Bicone F} →
            (hom : A.pt ⟶ B.pt) →
              autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp hom (B.π j) = A.π j)
                  CategoryTheory.Limits.BiconeMorphism.wπ._autoParam →
                autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp (A.ι j) hom = B.ι j)
                    CategoryTheory.Limits.BiconeMorphism.wι._autoParam →
                  CategoryTheory.Limits.BiconeMorphism A B
-- Mathlib.Combinatorics.Schnirelmann
_private.Mathlib.Combinatorics.Schnirelmann.0.add_eq_univ_of_one_le_schirelmannDensity_add_schnirelmannDensity.match_1_1.congr_eq_2 : ∀ (motive : ℕ ⊕ ℕ → Sort u_1) (x : ℕ ⊕ ℕ) (h_1 : (x : ℕ) → motive (Sum.inl x)) (h_2 : (y : ℕ) → motive (Sum.inr y))
  (y : ℕ),
  x = Sum.inr y →
    (match x with
      | Sum.inl x => h_1 x
      | Sum.inr y => h_2 y) ≍
      h_2 y
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.density_nonneg : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] {κ : ProbabilityTheory.Kernel α (γ × β)}
  {ν : ProbabilityTheory.Kernel α γ}, κ.fst ≤ ν → ∀ (a : α) (x : γ) (s : Set β), 0 ≤ κ.density ν a x s
-- Mathlib.Algebra.Ring.Defs
NonUnitalCommRing.toNonUnitalNonAssocCommRing : {α : Type u} → [self : NonUnitalCommRing α] → NonUnitalNonAssocCommRing α
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getD_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k a : α}
  {fallback : β}, (t.erase k).getD a fallback = if cmp k a = Ordering.eq then fallback else t.getD a fallback
-- Mathlib.Order.LiminfLimsup
Filter.blimsup_true : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] (f : Filter β) (u : β → α),
  (Filter.blimsup u f fun x => True) = Filter.limsup u f
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Folds a function over an iterator from the left, accumulating a value starting with `init`.
The accumulated value is combined with the each element of the list in order, using `f`.

It is equivalent to `it.toList.foldl`.

This variant terminates after finitely many steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using `IterM.fold`.
 -/
Std.IterM.Total.fold : {m : Type w → Type w'} →
  {α β γ : Type w} →
    [Monad m] →
      [inst : Std.Iterator α m β] →
        [Std.IteratorLoop α m m] → [Std.Iterators.Finite α m] → (γ → β → γ) → γ → Std.IterM.Total m β → m γ
-- Mathlib.Algebra.Star.SelfAdjoint
selfAdjoint.instNNRatCast : {R : Type u_1} → [inst : Field R] → [inst_1 : StarRing R] → NNRatCast ↥(selfAdjoint R)
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
/-- `elimAllVarsM` eliminates all variables from the linarith state, leaving it with a set of
ground comparisons. If this succeeds without exception, the original `linarith` state is consistent.
 -/
Mathlib.Tactic.Linarith.elimAllVarsM : Mathlib.Tactic.Linarith.LinarithM Unit
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.instInvOneClass : {α : Type u} → [Inv α] → InvOneClass (WithOne α)
-- Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
MeasureTheory.eLpNorm'_smul_le_mul_eLpNorm' : ∀ {𝕜 : Type u_1} {α : Type u_2} {E : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedRing 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : MulActionWithZero 𝕜 E] [IsBoundedSMul 𝕜 E] {p q r : ℝ}
  {f : α → E},
  MeasureTheory.AEStronglyMeasurable f μ →
    ∀ {φ : α → 𝕜},
      MeasureTheory.AEStronglyMeasurable φ μ →
        0 < p →
          p < q →
            1 / p = 1 / q + 1 / r →
              MeasureTheory.eLpNorm' (φ • f) p μ ≤ MeasureTheory.eLpNorm' φ q μ * MeasureTheory.eLpNorm' f r μ
-- Lean.Meta.Constructions.SparseCasesOn
_private.Lean.Meta.Constructions.SparseCasesOn.0.Lean.Meta.instHashableSparseCasesOnKey.hash : Lean.Meta.SparseCasesOnKey✝ → UInt64
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.instAddRightMono : AddRightMono Ordinal.{u}
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- Removing an edge from `H` for each subgraph isomorphic to `G` means that the number of edges
we've removed is at most the number of copies of `G` in `H`.  -/
SimpleGraph.le_card_edgeFinset_killCopies : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [inst : Fintype ↑G.edgeSet]
  [inst_1 : Fintype V], G.edgeFinset.card - G.copyCount H ≤ (G.killCopies H).edgeFinset.card
-- Mathlib.Data.Rat.Cast.Defs
Rat.cast_zero : ∀ {α : Type u_3} [inst : DivisionRing α], ↑0 = 0
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Class
Std.Tactic.BVDecide.LRAT.Internal.Formula.formulaEntails_def : ∀ {α : outParam (Type u)} {β : outParam (Type v)} {inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β} {σ : Type w}
  {inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ} [self : Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ]
  (p : α → Bool) (f : σ),
  Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p f =
    (((Std.Tactic.BVDecide.LRAT.Internal.Formula.toList f).all fun c =>
        decide (Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p c)) =
      true)
-- Lean.Meta.Transform
/-- Similar to `Core.transform`, but terms provided to `pre` and `post` do not contain loose bound variables.
So, it is safe to use any `MetaM` method at `pre` and `post`.

Warning: `pre` and `post` should not depend on variables in the local context introduced by `transform`.
This is in order to allow aggressive caching.

If `skipConstInApp := true`, then for an expression `mkAppN (.const f) args`, the subexpression
`.const f` is not visited again. Put differently: every `.const f` is visited once, with its
arguments if present, on its own otherwise.
 -/
Lean.Meta.transform : {m : Type → Type} →
  [inst : Monad m] →
    [MonadLiftT Lean.MetaM m] →
      [MonadControlT Lean.MetaM m] →
        Lean.Expr →
          (optParam (Lean.Expr → m Lean.TransformStep) fun x => pure Lean.TransformStep.continue) →
            (optParam (Lean.Expr → m Lean.TransformStep) fun e => pure (Lean.TransformStep.done e)) →
              optParam Bool false → optParam Bool false → m Lean.Expr
-- Batteries.Recycling.MonadSatisfying.Array
Array.SatisfiesM_mapM : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {as : Array α} {f : α → m β}
  {motive : ℕ → Prop} {p : Fin as.size → β → Prop},
  motive 0 →
    (∀ (i : Fin as.size), motive ↑i → SatisfiesM (fun x => p i x ∧ motive (↑i + 1)) (f as[i])) →
      SatisfiesM (fun arr => motive as.size ∧ ∃ (eq : arr.size = as.size), ∀ (i : ℕ) (h : i < as.size), p ⟨i, h⟩ arr[i])
        (Array.mapM f as)
-- Mathlib.NumberTheory.RamificationInertia.Inertia
Ideal.inertiaDeg'_pos : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R) (P : Ideal S)
  [p.IsMaximal] [Module.Finite R S] [P.LiesOver p], 0 < p.inertiaDeg' P
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.tensorHom_comp_tensorHom : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : CategoryTheory.GradedObject I C} (f₁ : X₁ ⟶ X₂)
  (f₂ : X₂ ⟶ X₃) (g₁ : Y₁ ⟶ Y₂) (g₂ : Y₂ ⟶ Y₃) [inst_3 : X₁.HasTensor Y₁] [inst_4 : X₂.HasTensor Y₂]
  [inst_5 : X₃.HasTensor Y₃],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.tensorHom f₁ g₁)
      (CategoryTheory.GradedObject.Monoidal.tensorHom f₂ g₂) =
    CategoryTheory.GradedObject.Monoidal.tensorHom (CategoryTheory.CategoryStruct.comp f₁ f₂)
      (CategoryTheory.CategoryStruct.comp g₁ g₂)
-- Mathlib.CategoryTheory.MorphismProperty.LocalClosure
CategoryTheory.MorphismProperty.sourceLocalClosure.instIsStableUnderBaseChangeOfIsStableUnderBaseChangeOfHasPullbacks : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C}
  {P : CategoryTheory.MorphismProperty C} [P.IsStableUnderBaseChange] [K.IsStableUnderBaseChange]
  [CategoryTheory.Limits.HasPullbacks C],
  (CategoryTheory.MorphismProperty.sourceLocalClosure K P).IsStableUnderBaseChange
-- Mathlib.Data.Finset.Max
Finset.map_ofDual_max : ∀ {α : Type u_2} [inst : LinearOrder α] (s : Finset αᵒᵈ),
  WithBot.map (⇑OrderDual.ofDual) s.max = (Finset.image (⇑OrderDual.ofDual) s).min
-- Init.Data.List.MinMax
List.max_eq_get_max? : ∀ {α : Type u_1} [inst : Max α] (l : List α) (hl : l ≠ []), l.max hl = l.max?.get ⋯
-- Mathlib.Logic.Equiv.Fin.Basic
/-- The equivalence between `Fin (m + n)` and `Fin (n + m)` which rotates by `n`.  -/
finAddFlip : {m n : ℕ} → Fin (m + n) ≃ Fin (n + m)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.self_le_maxKeyD_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k} {fallback : α}, (cmp k ((t.insert k v).maxKeyD fallback)).isLE = true
-- Init.Data.Ord.UInt
UInt8.instLawfulOrderOrd : Std.LawfulOrderOrd UInt8
-- Init.Data.UInt.Bitwise
UInt16.or_neg_one : ∀ {a : UInt16}, a ||| -1 = -1
-- Mathlib.Data.Quot
/-- A version of `Quotient.recOnSubsingleton₂` taking `{s₁ : Setoid α} {s₂ : Setoid α}`
as implicit arguments instead of instance arguments.  -/
Quotient.recOnSubsingleton₂' : {α : Sort u_1} →
  {β : Sort u_2} →
    {s₁ : Setoid α} →
      {s₂ : Setoid β} →
        {φ : Quotient s₁ → Quotient s₂ → Sort u_5} →
          [∀ (a : α) (b : β), Subsingleton (φ ⟦a⟧ ⟦b⟧)] →
            (q₁ : Quotient s₁) →
              (q₂ : Quotient s₂) → ((a₁ : α) → (a₂ : β) → φ (Quotient.mk'' a₁) (Quotient.mk'' a₂)) → φ q₁ q₂
-- Init.Data.Int.Linear
Int.Internal.Linear.eq_def_cert : Int.Internal.Linear.Var → Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Bool
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.HalfBraiding.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X : C}
  [inst_2 : SizeOf C]
  (β :
    (U : C) → CategoryTheory.MonoidalCategoryStruct.tensorObj X U ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj U X)
  (monoidal :
    autoParam
      (∀ (U U' : C),
        (β (CategoryTheory.MonoidalCategoryStruct.tensorObj U U')).hom =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X U U').inv
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β U).hom U')
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator U X U').hom
                (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft U (β U').hom)
                  (CategoryTheory.MonoidalCategoryStruct.associator U U' X).inv))))
      CategoryTheory.HalfBraiding.monoidal._autoParam)
  (naturality :
    autoParam
      (∀ {U U' : C} (f : U ⟶ U'),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f) (β U').hom =
          CategoryTheory.CategoryStruct.comp (β U).hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X))
      CategoryTheory.HalfBraiding.naturality._autoParam),
  sizeOf { β := β, monoidal := monoidal, naturality := naturality } = 1
-- Init.Data.Float.Float
/-- Converts a floating-point number to a 32-bit unsigned integer.

If the given `Float` is non-negative, truncates the value to a positive integer, rounding down and
clamping to the range of `UInt32`. Returns `0` if the `Float` is negative or `NaN`, and returns the
largest `UInt32` value (i.e. `UInt32.size - 1`) if the float is larger than it.

This function has a logical model in terms of `Float.Model`.
 -/
Float.toUInt32 : Float → UInt32
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.congr_symm : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] (G' : Subgroup G) (H' : Subgroup H)
  [inst_2 : G'.Normal] [inst_3 : H'.Normal] (e : G ≃* H) (he : Subgroup.map (↑e) G' = H'),
  (QuotientGroup.congr G' H' e he).symm = QuotientGroup.congr H' G' e.symm ⋯