mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Grind.AC
Lean.Grind.AC.diseq_simp_lhs_suffix : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {x : Std.Associative ctx.op}
  (lhs₁ rhs₁ head lhs₂ rhs₂ lhs₂' : Lean.Grind.AC.Seq),
  Lean.Grind.AC.simp_suffix_cert lhs₁ rhs₁ head lhs₂ lhs₂' = true →
    Lean.Grind.AC.Seq.denote ctx lhs₁ = Lean.Grind.AC.Seq.denote ctx rhs₁ →
      Lean.Grind.AC.Seq.denote ctx lhs₂ ≠ Lean.Grind.AC.Seq.denote ctx rhs₂ →
        Lean.Grind.AC.Seq.denote ctx lhs₂' ≠ Lean.Grind.AC.Seq.denote ctx rhs₂
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get!_diff_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β],
  m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → Std.DTreeMap.Raw.Const.get! (m₁ \ m₂) k = Std.DTreeMap.Raw.Const.get! m₁ k
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
CategoryTheory.Limits.hasFiniteLimits_of_hasLimitsOfSize : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfSize.{v', u', v, u} C],
  CategoryTheory.Limits.HasFiniteLimits C
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- Any isomorphism is the projection from a single object product.  -/
CategoryTheory.Limits.Fan.isLimitMkOfUnique : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      (e : X ≅ Y) →
        (J : Type u_1) → [Unique J] → CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk X fun x => e.hom)
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.CompactOpens.ext : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s t : TopologicalSpace.CompactOpens α}, ↑s = ↑t → s = t
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
hasMFDerivWithinAt_univ : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M}
  {f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)}, HasMFDerivAt[Set.univ] f x f' ↔ HasMFDerivAt% f x f'
-- Mathlib.Topology.Bases
TopologicalSpace.isTopologicalBasis_empty : ∀ {α : Type u} [t : TopologicalSpace α], TopologicalSpace.IsTopologicalBasis ∅ ↔ IsEmpty α
-- Mathlib.Logic.Relation
Relation.SymmGen.refl : ∀ {α : Type u_1} (r : α → α → Prop) [Std.Refl r] (a : α), Relation.SymmGen r a a
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.RightFraction.ofInv_s : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (s : Y ⟶ X) (hs : W s), (CategoryTheory.MorphismProperty.RightFraction.ofInv s hs).s = s
-- Mathlib.Analysis.Analytic.Basic
analyticWithinAt_univ : ∀ {𝕜 : 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] {f : E → F} {x : E},
  AnalyticWithinAt 𝕜 f Set.univ x ↔ AnalyticAt 𝕜 f x
-- Mathlib.Topology.Order.SuccPred
AccPt.isPredLimit : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α] [PredOrder α] [NoMinOrder α]
  {a : α} {s : Set α}, AccPt a (Filter.principal s) → Order.IsPredLimit a
-- Mathlib.CategoryTheory.Monoidal.Ring
/-- The category of ring objects in a cartesian monoidal category.  -/
CategoryTheory.RingObjCat : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] → [CategoryTheory.BraidedCategory C] → Type (max u v)
-- Std.Data.HashMap.Lemmas
Std.HashMap.forIn_eq_forIn : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {δ : Type w} {m' : Type w → Type w'}
  [inst : Monad m'] [LawfulMonad m'] {f : α → β → δ → m' (ForInStep δ)} {init : δ},
  Std.HashMap.forIn f init m = forIn m init fun a d => f a.1 a.2 d
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.instOrderTop : {X : Type u_2} → [inst : TopologicalSpace X] → OrderTop (DiscreteQuotient X)
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.Entry.entry : {α : Type u} → {β : Type v} → {σ : Type w} → α → β → Lean.PersistentHashMap.Entry α β σ
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Ioo_ae_eq_Ico' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : PartialOrder α] {a b : α},
  μ {a} = 0 → Set.Ioo a b =ᵐ[μ] Set.Ico a b
-- Mathlib.GroupTheory.HNNExtension
/-- A constructor to append an element `g` of `G` and `u : ℤˣ` to a word `w` with sufficient
hypotheses that no normalization or cancellation need take place for the result to be in normal form
 -/
HNNExtension.NormalWord.cons : {G : Type u_1} →
  [inst : Group G] →
    {A B : Subgroup G} →
      {d : HNNExtension.NormalWord.TransversalPair G A B} →
        G →
          (u : ℤˣ) →
            (w : HNNExtension.NormalWord d) →
              w.head ∈ d.set u →
                (∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ HNNExtension.toSubgroup A B u → u = u') →
                  HNNExtension.NormalWord d
-- Mathlib.Analysis.Analytic.Basic
AnalyticOnNhd.continuousOn : ∀ {𝕜 : 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] {f : E → F} {s : Set E},
  AnalyticOnNhd 𝕜 f s → ContinuousOn f s
-- Mathlib.Data.DFinsupp.BigOperators
/-- The product over two dfinsupps agree if the functions agree and are well-behaved within the
shared support.  -/
DFinsupp.prod_congr_of_eq_on_union : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_3 : CommMonoid γ] {f1 f2 : Π₀ (i : ι), β i}
  {g1 g2 : (i : ι) → β i → γ},
  (∀ x ∈ f1.support ∪ f2.support, g1 x (f1 x) = g2 x (f2 x)) →
    (∀ x ∈ f1.support ∪ f2.support, g1 x 0 = 1) → (∀ x ∈ f1.support ∪ f2.support, g2 x 0 = 1) → f1.prod g1 = f2.prod g2
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.preAleph_lt_preAleph : ∀ {o₁ o₂ : Ordinal.{u_1}}, Cardinal.preAleph o₁ < Cardinal.preAleph o₂ ↔ o₁ < o₂
-- Mathlib.Tactic.GCongr.Core
/-- The number of arguments in the application of `head` that are different.
This is used for sorting the lemmas.
For example, `a + b ≤ a + c` has `numVarying := 1`.  -/
Mathlib.Tactic.GCongr.GCongrLemma.numVarying : Mathlib.Tactic.GCongr.GCongrLemma → ℕ
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.mem_comap : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {K : Subgroup N} {f : G →* N} {x : G},
  x ∈ Subgroup.comap f K ↔ f x ∈ K
-- Mathlib.Algebra.Group.Defs
AddCommGroup.toAddCancelCommMonoid : {G : Type u_1} → [AddCommGroup G] → AddCancelCommMonoid G
-- Mathlib.Data.Num.ZNum
ZNum.decidableDvd : DecidableRel fun x1 x2 => x1 ∣ x2
-- Mathlib.Topology.UrysohnsLemma
Urysohns.CU.approx.eq_2 : ∀ {X : Type u_1} [inst : TopologicalSpace X] {P : Set X → Set X → Prop} (x : Urysohns.CU P) (x_1 : X) (n : ℕ),
  Urysohns.CU.approx n.succ x x_1 = midpoint ℝ (Urysohns.CU.approx n x.left x_1) (Urysohns.CU.approx n x.right x_1)
-- Mathlib.Algebra.Order.ToIntervalMod
QuotientAddGroup.btw_coe_iff : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} [hp' : Fact (0 < p)] {x₁ x₂ x₃ : α}, btw ↑x₁ ↑x₂ ↑x₃ ↔ toIcoMod ⋯ x₁ x₂ ≤ toIocMod ⋯ x₁ x₃
-- Mathlib.Data.LawfulXor.Basic
xor_xor_cancel_comm : ∀ {α : Type u_1} [inst : XorOp α] [inst_1 : Zero α] [LawfulXor α] (a b : α), a ^^^ b ^^^ a = b
-- Mathlib.LinearAlgebra.Multilinear.Pi
/-- Two multilinear maps from finite families are equal if they agree on the generators.

This is a multilinear version of `LinearMap.pi_ext`.  -/
MultilinearMap.pi_ext : ∀ {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : Type uN} [inst : Semiring R]
  [inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)] [inst_2 : AddCommMonoid N]
  [inst_3 : (i : ι) → (k : κ i) → Module R (M i k)] [inst_4 : Module R N] [Finite ι] [∀ (i : ι), Finite (κ i)]
  [inst_7 : (i : ι) → DecidableEq (κ i)] ⦃f g : MultilinearMap R (fun i => (j : κ i) → M i j) N⦄,
  (∀ (p : (i : ι) → κ i),
      (f.compLinearMap fun i => LinearMap.single R (M i) (p i)) =
        g.compLinearMap fun i => LinearMap.single R (M i) (p i)) →
    f = g
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cochain.toSingleMk_postcomp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : K.X p ⟶ X) {n : ℤ}
  (h : p + n = q) {X' : C} (g : X ⟶ X'),
  CochainComplex.HomComplex.Cochain.toSingleMk (CategoryTheory.CategoryStruct.comp f g) h =
    (CochainComplex.HomComplex.Cochain.toSingleMk f h).comp
      (CochainComplex.HomComplex.Cochain.ofHom ((CochainComplex.singleFunctor C q).map g)) ⋯
-- Mathlib.Topology.Homotopy.Path
/-- The canonical map from `Path x₀ x₁` to `Path.Homotopic.Quotient x₀ x₁`.  -/
Path.Homotopic.Quotient.mk : {X : Type u} → [inst : TopologicalSpace X] → {x₀ x₁ : X} → Path x₀ x₁ → Path.Homotopic.Quotient x₀ x₁
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- Given a `k`-module `A` with a compatible `DistribMulAction` of `G`, and a function
`f : G × G → A` satisfying the 2-coboundary condition, produces a 2-coboundary for the
representation on `A` induced by the `DistribMulAction`.  -/
groupCohomology.coboundariesOfIsCoboundary₂ : {k G A : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      [inst_2 : AddCommGroup A] →
        [inst_3 : Module k A] →
          [inst_4 : DistribMulAction G A] →
            [inst_5 : SMulCommClass G k A] →
              {f : G × G → A} →
                groupCohomology.IsCoboundary₂ f → ↥(groupCohomology.coboundaries₂ (Rep.ofDistribMulAction k G A))
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.coe_natCast : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : NatCast β] (n : ℕ),
  ⇑↑n = ↑n
-- Init.Prelude
/-- Equality is symmetric: if `a = b` then `b = a`.

Because this is in the `Eq` namespace, if you have a variable `h : a = b`,
`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.

For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)
 -/
Eq.symm : ∀ {α : Sort u} {a b : α}, a = b → b = a
-- Mathlib.Algebra.Module.Torsion.Basic
/-- The annihilator of a module is the intersection of the torsion ideals of its elements.  -/
Module.annihilator_eq_iInf_torsionOf : ∀ (R : Type u_1) {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Module.annihilator R M = ⨅ x, Ideal.torsionOf R M x
-- Aesop.Forward.State
/-- Add a pattern substitution to the forward state.  -/
Aesop.ForwardState.enqueuePatSubst : Aesop.ForwardRule → Aesop.Substitution → Aesop.PatSubstSource → Aesop.ForwardState → Aesop.ForwardState
-- Mathlib.RingTheory.Spectrum.Prime.Jacobson
PrimeSpectrum.exists_isClosed_singleton_of_isJacobsonRing : ∀ {R : Type u_1} [inst : CommRing R] [IsJacobsonRing R] (s : Set (PrimeSpectrum R)),
  IsOpen s → s.Nonempty → ∃ x ∈ s, IsClosed {x}
-- Mathlib.Order.SymmDiff
bihimp_eq_sup_himp_inf : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] (a b : α), bihimp a b = a ⊔ b ⇨ a ⊓ b
-- Mathlib.LinearAlgebra.Matrix.ToLin
/-- A `Matrix m n R` is linearly equivalent over `Rᵐᵒᵖ` to a linear map `(m → R) →ₗ[R] (n → R)`,
by having matrices act by right multiplication.  -/
Matrix.toLinearMapRight' : {R : Type u_1} →
  [inst : Semiring R] →
    {m : Type u_3} → {n : Type u_4} → [Fintype m] → [DecidableEq m] → Matrix m n R ≃ₗ[Rᵐᵒᵖ] (m → R) →ₗ[R] n → R
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.mapGlueData_t : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] {C' : Type u₂} [inst_1 : CategoryTheory.Category.{v, u₂} C']
  (D : CategoryTheory.GlueData C) (F : CategoryTheory.Functor C C')
  [inst_2 : ∀ (i j k : D.J), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F]
  (i j : D.J), (D.mapGlueData F).t i j = F.map (D.t i j)
-- Mathlib.Order.Basic
Prod.mk_lt_swap : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {a : α} {b : β} {x : α × β},
  (b, a) < x.swap ↔ (a, b) < x
-- Mathlib.RingTheory.Artinian.Module
IsArtinianRing.primeSpectrumEquivMaximalSpectrum_apply_asIdeal : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsArtinianRing R] (I : PrimeSpectrum R),
  (IsArtinianRing.primeSpectrumEquivMaximalSpectrum I).asIdeal = I.asIdeal
-- Mathlib.Topology.Algebra.Order.Field
/-- If `g` tends to zero and there exist constants `b B : 𝕜` such that eventually `b ≤ f x| ≤ B`,
then the product `f * g` tends to zero.  -/
bdd_le_mul_tendsto_zero : ∀ {𝕜 : Type u_1} {α : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {f g : α → 𝕜} {b B : 𝕜},
  (∀ᶠ (x : α) in l, b ≤ f x) →
    (∀ᶠ (x : α) in l, f x ≤ B) → Filter.Tendsto g l (nhds 0) → Filter.Tendsto (fun x => f x * g x) l (nhds 0)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.kernelCompMono_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y Z : C}
  (f : X ⟶ Y) (g : Y ⟶ Z) [inst_2 : CategoryTheory.Limits.HasKernel f] [inst_3 : CategoryTheory.Mono g],
  (CategoryTheory.Limits.kernelCompMono f g).inv =
    CategoryTheory.Limits.kernel.lift (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.Limits.kernel.ι f) ⋯
-- Mathlib.Order.RelSeries
LTSeries.range_apply : ∀ (n : ℕ) (i : Fin (n + 1)), (LTSeries.range n).toFun i = ↑i
-- Mathlib.RingTheory.Valuation.Basic
Valuation.IsEquiv.isTrivialOn : ∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀]
  [inst_2 : LinearOrderedCommMonoidWithZero Γ'₀] {v₁ : Valuation R Γ₀} {v₂ : Valuation R Γ'₀} {A : Type u_7}
  [inst_3 : CommSemiring A] [inst_4 : Algebra A R],
  v₁.IsEquiv v₂ → Valuation.IsTrivialOn A v₁ → Valuation.IsTrivialOn A v₂
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.integrableOn_congr_set_ae : ∀ {α : Type u_1} {ε : Type u_3} {mα : MeasurableSpace α} {f : α → ε} {s t : Set α} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε],
  s =ᵐ[μ] t → (MeasureTheory.IntegrableOn f s μ ↔ MeasureTheory.IntegrableOn f t μ)
-- Mathlib.Order.Filter.Pointwise
Filter.smul_filter_eq_bot_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {f : Filter β} {a : α}, a • f = ⊥ ↔ f = ⊥
-- Mathlib.Topology.Order.Compact
/-- The **extreme value theorem**: if a continuous function `f` tends to infinity away from compact
sets, then it has a global minimum.  -/
Continuous.exists_forall_le : ∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : TopologicalSpace β]
  [ClosedIicTopology α] [Nonempty β] {f : β → α},
  Continuous f → Filter.Tendsto f (Filter.cocompact β) Filter.atTop → ∃ x, ∀ (y : β), f x ≤ f y
-- Mathlib.Analysis.Complex.Exponential
Real.exp_zero : Real.exp 0 = 1
-- Init.Data.SInt.Basic
/-- Constructs an `Int8` from an `Int` that is known to be in bounds.  -/
Int8.ofIntLE : (i : ℤ) → Int8.minValue.toInt ≤ i → i ≤ Int8.maxValue.toInt → Int8
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonRpcOptions : Lean.FromJson Lean.Lsp.RpcOptions
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.get?_inter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (t₁ ∩ t₂).get? k = if k ∈ t₂ then t₁.get? k else none
-- Mathlib.MeasureTheory.SetAlgebra
MeasureTheory.generateSetAlgebra.below.base : ∀ {α : Type u_2} {𝒜 : Set (Set α)} {motive : (a : Set α) → MeasureTheory.generateSetAlgebra 𝒜 a → Prop} (s : Set α)
  (s_mem : s ∈ 𝒜), MeasureTheory.generateSetAlgebra.below ⋯
-- Mathlib.Data.Set.Function
Set.injOn_univ : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Set.InjOn f Set.univ ↔ Function.Injective f
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRk_ground : ∀ {α : Type u_1} (M : Matroid α), M.eRk M.E = M.eRank
-- Mathlib.Util.AtomM.Recurse
/-- if true, implication hypotheses are added to the local context of the discharger  -/
Mathlib.Tactic.AtomM.Recurse.Config.contextual : Mathlib.Tactic.AtomM.Recurse.Config → Bool
-- Std.Sat.AIG.CachedLemmas
Std.Sat.AIG.mkConstCached.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig : Std.Sat.AIG α) (val : Bool),
  aig.mkConstCached val = { gate := 0, invert := val, hgate := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- If a category has biproducts of a shape `J`, its `colim` and `lim` functor on diagrams over `J`
are isomorphic.  -/
CategoryTheory.Limits.HasBiproductsOfShape.colimIsoLim : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        [inst_2 : CategoryTheory.Limits.HasBiproductsOfShape J C] →
          CategoryTheory.Limits.colim ≅ CategoryTheory.Limits.lim
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Subsemiring.op_unop : ∀ {R : Type u_2} [inst : NonAssocSemiring R] (S : Subsemiring Rᵐᵒᵖ), S.unop.op = S
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.b₄_of_char_three : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [CharP R 3], W.b₄ = -W.a₄ + W.a₁ * W.a₃
-- Std.Data.String.ToInt
String.Slice.toInt?_eq_none : ∀ {s : String.Slice}, s.isInt = false → s.toInt? = none
-- Mathlib.Order.Filter.Basic
Filter.sInf_neBot_of_directed' : ∀ {α : Type u} {s : Set (Filter α)}, s.Nonempty → DirectedOn (fun x1 x2 => x1 ≥ x2) s → ⊥ ∉ s → (sInf s).NeBot
-- Batteries.Tactic.GeneralizeProofs
Batteries.Tactic.GeneralizeProofs.GState.mk : Lean.ExprMap Lean.Expr → Batteries.Tactic.GeneralizeProofs.GState
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.liftPrecomp.eq_1 : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {Z : C} (h : Z ⟶ X)
  {s : CategoryTheory.Limits.Fork f g} (hs : CategoryTheory.Limits.IsLimit s)
  {c : CategoryTheory.Limits.PullbackCone s.ι h} (hc : CategoryTheory.Limits.IsLimit c)
  (s' : CategoryTheory.Limits.Fork (CategoryTheory.CategoryStruct.comp h f) (CategoryTheory.CategoryStruct.comp h g)),
  CategoryTheory.Limits.liftPrecomp h hs hc s' =
    hc.lift
      (CategoryTheory.Limits.PullbackCone.mk
        (hs.lift (CategoryTheory.Limits.Fork.ofι (CategoryTheory.CategoryStruct.comp s'.ι h) ⋯)) s'.ι ⋯)
-- Init.Data.Array.Lex.Lemmas
Array.le_empty : ∀ {α : Type u_1} [inst : LT α] {xs : Array α}, xs ≤ #[] ↔ xs = #[]
-- Mathlib.CategoryTheory.Limits.Indization.ParallelPair
/-- Given an `IndParallelPairPresentation f g`, we can understand the parallel pair `(f, g)`
as the colimit of `(P.φ, P.ψ)` in `Cᵒᵖ ⥤ Type v`.  -/
CategoryTheory.IndParallelPairPresentation.parallelPairIsoParallelPairCompYoneda : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} →
      {f g : A ⟶ B} →
        (P : CategoryTheory.IndParallelPairPresentation f g) →
          CategoryTheory.Limits.parallelPair f g ≅
            (CategoryTheory.Limits.parallelPair P.φ P.ψ).comp
              (((CategoryTheory.Functor.whiskeringRight P.I C (CategoryTheory.Functor Cᵒᵖ (Type v₁))).obj
                    CategoryTheory.yoneda).comp
                CategoryTheory.Limits.colim)
-- Mathlib.Logic.Embedding.Basic
/-- An embedding `e : α ↪ β` defines an embedding `(α → γ) ↪ (β → γ)` for any inhabited type `γ`.
This embedding sends each `f : α → γ` to a function `g : β → γ` such that `g ∘ e = f` and
`g y = default` whenever `y ∉ range e`.  -/
Function.Embedding.arrowCongrLeft : {α : Sort u} → {β : Sort v} → {γ : Sort w} → [Inhabited γ] → (α ↪ β) → (α → γ) ↪ β → γ
-- Batteries.Data.Nat.Bitwise.Lemmas
Nat.and_or_right_injective : ∀ {m x y : ℕ}, x &&& m = y &&& m → x ||| m = y ||| m → x = y
-- Mathlib.Data.Fin.SuccPred
Fin.castSucc_ne_last : ∀ {n : ℕ} (i : Fin n), i.castSucc ≠ Fin.last n
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.Ico_union_Ico_angleDiff_add_arg : ∀ {x y : Circle},
  x ≠ y →
    Set.Ico (↑x).arg (x.angleDiff y + (↑x).arg) ∪ Set.Ico (↑y).arg (y.angleDiff x + (↑y).arg) =
      Set.Ico (min (↑x).arg (↑y).arg) (min (↑x).arg (↑y).arg + 2 * Real.pi)
-- Mathlib.Topology.MetricSpace.Gluing
/-- The injection of a space in a disjoint union is an isometry  -/
Metric.Sigma.isometry_mk : ∀ {ι : Type u_1} {E : ι → Type u_2} [inst : (i : ι) → MetricSpace (E i)] (i : ι), Isometry (Sigma.mk i)
-- Mathlib.Analysis.Analytic.Constructions
HasFPowerSeriesAt.sub : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {pf pg : FormalMultilinearSeries 𝕜 E F} {x : E},
  HasFPowerSeriesAt f pf x → HasFPowerSeriesAt g pg x → HasFPowerSeriesAt (f - g) (pf - pg) x
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.coequifibered_normalizationDiagramMap : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.QuasiCompact f] [AlgebraicGeometry.QuasiSeparated f],
  CategoryTheory.NatTrans.Coequifibered
    ((AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor Y).op.whiskerLeft
      (AlgebraicGeometry.Scheme.Hom.normalizationDiagramMap f))
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.zero_testAgainstNN_apply : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] (f : BoundedContinuousFunction Ω NNReal),
  MeasureTheory.FiniteMeasure.testAgainstNN 0 f = 0
-- Std.Time.Time.PlainTime
/-- Creates a new `PlainTime` by adjusting the `hour` component to the given value.
 -/
Std.Time.PlainTime.withHours : Std.Time.PlainTime → Std.Time.Hour.Ordinal → Std.Time.PlainTime
-- Init.Data.Option.Basic
Option.orElse_some : ∀ {α : Type u_1} {a : α} {b : Unit → Option α}, (some a).orElse b = some a
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.coeff_subst_X_zero_subst_mul_X_one : ∀ {R : Type u_2} [inst : CommRing R] (f : PowerSeries R) (e : Fin 2 →₀ ℕ),
  (MvPowerSeries.coeff e) (PowerSeries.subst (MvPowerSeries.X 0) f * PowerSeries.subst (MvPowerSeries.X 1) f) =
    (PowerSeries.coeff (e 0)) f * (PowerSeries.coeff (e 1)) f
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
/-- `OrderMonoidWithZeroHom α β` is the type of functions `α → β` that preserve
the `MonoidWithZero` structure.

`OrderMonoidWithZeroHom` is also used for group homomorphisms.

When possible, instead of parametrizing results over `(f : α →+ β)`,
you should parameterize over
`(F : Type*) [FunLike F M N] [MonoidWithZeroHomClass F M N] [OrderHomClass F M N] (f : F)`.  -/
OrderMonoidWithZeroHom : (α : Type u_6) →
  (β : Type u_7) → [Preorder α] → [Preorder β] → [MulZeroOneClass α] → [MulZeroOneClass β] → Type (max u_6 u_7)
-- Mathlib.CategoryTheory.WithTerminal.Cone
_private.Mathlib.CategoryTheory.WithTerminal.Cone.0.CategoryTheory.WithTerminal.liftFromOverComp.match_1.eq_1 : ∀ {J : Type u_1} (motive : CategoryTheory.WithTerminal J → Sort u_2)
  (h_1 : Unit → motive CategoryTheory.WithTerminal.star) (h_2 : (a : J) → motive (CategoryTheory.WithTerminal.of a)),
  (match CategoryTheory.WithTerminal.star with
    | CategoryTheory.WithTerminal.star => h_1 ()
    | CategoryTheory.WithTerminal.of a => h_2 a) =
    h_1 ()