mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Polynomial.Homogenize
Polynomial.homogenize.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] (p : Polynomial R) (n : ℕ),
  p.homogenize n =
    ∑ kl ∈ Finset.HasAntidiagonal.antidiagonal n, (MvPolynomial.monomial fun₀ | 0 => kl.1 | 1 => kl.2) (p.coeff kl.1)
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.rotate'.match_1.splitter : {α : Type u_1} →
  (motive : List α → ℕ → Sort u_2) →
    (x : List α) →
      (x_1 : ℕ) →
        ((x : ℕ) → motive [] x) →
          ((l : List α) → (l = [] → False) → motive l 0) →
            ((a : α) → (l : List α) → (n : ℕ) → motive (a :: l) n.succ) → motive x x_1
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Pos.revSkipWhile_le : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat]
  [inst_1 : String.Slice.Pattern.Model.PatternModel pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s : String} {pos : s.Pos}, pos.revSkipWhile pat ≤ pos
-- Mathlib.Algebra.DirectSum.Internal
/-- The ring `A 0` inherited from `R` in the presence of `SetLike.GradedMonoid A`.  -/
SetLike.GradeZero.instRing : {ι : Type u_1} →
  {σ : Type u_2} →
    {R : Type u_4} →
      [inst : Ring R] →
        [inst_1 : AddMonoid ι] →
          [inst_2 : SetLike σ R] → [AddSubgroupClass σ R] → (A : ι → σ) → [SetLike.GradedMonoid A] → Ring ↥(A 0)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.instPreservesColimitsOfSize_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} {C' : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} C']
  {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat}
  (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S))
  [CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max u u₁, max u u₂, max (max (u + 1) u₁) v₁,
        max (max (u + 1) u₂) v₂}
      F],
  CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, max u u₁, max u u₂, max (max (u + 1) u₁) v₁,
      max (max (u + 1) u₂) v₂}
    F
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.congr_mk : ∀ {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') (x : G),
  (QuotientGroup.congr G' H' e he) ↑x = ↑(e x)
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.aestronglyMeasurable : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace β]
  (f : α →ₘ[μ] β), MeasureTheory.AEStronglyMeasurable (↑f) μ
-- Aesop.Nanos
Aesop.Nanos.printAsMillis : Aesop.Nanos → String
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.find?_toList_eq_some_iff_getKey?_eq_some_and_get?_eq_some : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k k' : α} {v : β},
  List.find? (fun a => a.1 == k) (Std.DHashMap.Const.toList m) = some (k', v) ↔
    m.getKey? k = some k' ∧ Std.DHashMap.Const.get? m k = some v
-- Mathlib.Data.Vector.Basic
List.Vector.getElem_pmap : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {p : α → Prop} (f : (a : α) → p a → β) (v : List.Vector α n)
  (hp : ∀ x ∈ v.toList, p x) {i : ℕ} (hi : i < n), (List.Vector.pmap f v hp)[i] = f v[i] ⋯
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.pi_trans : ∀ {ι : Type u_5} {αi : ι → Type u_6} {βi : ι → Type u_7} {γi : ι → Type u_8} (ei : (i : ι) → PartialEquiv (αi i) (βi i))
  (ei' : (i : ι) → PartialEquiv (βi i) (γi i)),
  (PartialEquiv.pi ei).trans (PartialEquiv.pi ei') = PartialEquiv.pi fun i => (ei i).trans (ei' i)
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.nodalWeight.eq_1 : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] (s : Finset ι) (v : ι → F) (i : ι),
  Lagrange.nodalWeight s v i = ∏ j ∈ s.erase i, (v i - v j)⁻¹
-- Mathlib.Algebra.Group.Pointwise.Set.BigOperators
/-- An n-ary version of `Set.add_subset_add`.  -/
Set.finsetSum_subset_finsetSum : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] (t : Finset ι) (f₁ f₂ : ι → Set α),
  (∀ i ∈ t, f₁ i ⊆ f₂ i) → ∑ i ∈ t, f₁ i ⊆ ∑ i ∈ t, f₂ i
-- Init.Data.List.Basic
List.zip_nil_left : ∀ {α : Type u} {β : Type v} {l : List β}, [].zip l = []
-- Lean.Environment
/-- Look up the entry for a given level.  -/
Lean.OLeanEntries.get : {α : Type} → Lean.OLeanEntries α → Lean.OLeanLevel → α
-- Init.Data.Slice.Array.Iterator
SubarrayIterator.step : {α : Type u} → {m : Type u → Type u_1} → Std.IterM Id α → Std.IterStep (Std.IterM m α) α
-- Mathlib.Order.Filter.Extr
IsMaxOn.neg : ∀ {α : Type u} {β : Type v} [inst : AddCommGroup β] [inst_1 : PartialOrder β] [IsOrderedAddMonoid β] {f : α → β} {a : α}
  {s : Set α}, IsMaxOn f s a → IsMinOn (fun x => -f x) s a
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.rnDeriv_singularPart : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α), (μ.singularPart ν).rnDeriv ν =ᵐ[ν] 0
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.rel_mk : ∀ {M : Type u_1} [inst : Add M] {s : Setoid M} {h : ∀ {w x y z : M}, s w x → s y z → s (w + y) (x + z)} {a b : M},
  { toSetoid := s, add' := h } a b ↔ s a b
-- Mathlib.GroupTheory.OrderOfElement
zsmul_eq_zsmul_iff_modEq : ∀ {G : Type u_1} [inst : AddGroup G] {x : G} {m n : ℤ}, m • x = n • x ↔ m ≡ n [ZMOD ↑(addOrderOf x)]
-- Mathlib.FieldTheory.Minpoly.ConjRootClass
ConjRootClass.instInvolutiveNeg : {K : Type u_1} →
  {L : Type u_2} → [inst : Field K] → [inst_1 : Field L] → [inst_2 : Algebra K L] → InvolutiveNeg (ConjRootClass K L)
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
/-- Given functors `F₁` and `F₂` in `J ⥤ C`, where `C` is a `V`-enriched ordinary category,
this is the bijection `(F₁ ⟶ F₂) ≃ (𝟙_ V ⟶ enrichedHom V F₁ F₂)`.  -/
CategoryTheory.Enriched.FunctorCategory.homEquiv : (V : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} C] →
          {J : Type u₃} →
            [inst_3 : CategoryTheory.Category.{v₃, u₃} J] →
              [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] →
                {F₁ F₂ : CategoryTheory.Functor J C} →
                  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂] →
                    (F₁ ⟶ F₂) ≃
                      (CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶
                        CategoryTheory.Enriched.FunctorCategory.enrichedHom V F₁ F₂)
-- Mathlib.Algebra.GCDMonoid.Finset
Finset.gcd_empty : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {f : β → α}, ∅.gcd f = 0
-- Aesop.Frontend.Attribute
Aesop.Frontend.AttrConfig.mk.injEq : ∀ (rules rules_1 : Array Aesop.Frontend.RuleExpr), ({ rules := rules } = { rules := rules_1 }) = (rules = rules_1)
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.isTheta_comm : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F} {l : Filter α},
  f =Θ[l] g ↔ g =Θ[l] f
-- Mathlib.CategoryTheory.Sites.PreservesLocallyBijective
CategoryTheory.Presheaf.isLocallySurjective_of_whisker : ∀ {C : Type u_1} {D : Type u_2} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} A]
  (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D)
  (H : CategoryTheory.Functor C D) {F G : CategoryTheory.Functor Dᵒᵖ A} (f : F ⟶ G) {FA : A → A → Type u_4}
  {CA : A → Type u_5} [inst_3 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)]
  [inst_4 : CategoryTheory.ConcreteCategory A FA],
  CategoryTheory.CoverPreserving J K H →
    ∀ [H.IsCoverDense K] [CategoryTheory.Presheaf.IsLocallySurjective J (H.op.whiskerLeft f)],
      CategoryTheory.Presheaf.IsLocallySurjective K f
-- Mathlib.CategoryTheory.Widesubcategory
CategoryTheory.InducedWideCategory.Hom.ext_iff : ∀ {C : Type u₁} {D : Type u₂} {inst : CategoryTheory.Category.{v₁, u₂} D} {F : C → D}
  {P : CategoryTheory.MorphismProperty D} {inst_1 : P.IsMultiplicative} {X Y : CategoryTheory.InducedWideCategory D F P}
  {x y : X.Hom Y}, x = y ↔ x.hom = y.hom
-- Mathlib.Algebra.Notation
LeOnePart.mk : {α : Type u_1} → (α → α) → LeOnePart α
-- Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli
/-- First version, with pointwise equicontinuity and range in a compact space.  -/
BoundedContinuousFunction.arzela_ascoli₁ : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [CompactSpace α] [inst_2 : PseudoMetricSpace β] [CompactSpace β]
  (A : Set (BoundedContinuousFunction α β)), IsClosed A → (Equicontinuous fun x => ⇑↑x) → IsCompact A
-- Mathlib.RingTheory.Ideal.Quotient.PowTransition
Submodule.powSMulQuotInclusion_injective : ∀ {R : Type u_3} [inst : CommRing R] (I : Ideal R) {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {a b c : ℕ} (h : c = b + a) (N : Submodule R M), Function.Injective ⇑(Submodule.powSMulQuotInclusion I M h N)
-- Mathlib.Analysis.Calculus.Deriv.Add
HasDerivAt.neg : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜}, HasDerivAt f f' x → HasDerivAt (-f) (-f') x
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Complex.differentiable_iteratedDeriv_cosh : ∀ (n : ℕ), Differentiable ℂ (iteratedDeriv n Complex.cosh)
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Measurable.aemeasurable : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β}
  {μ : MeasureTheory.Measure α}, Measurable f → AEMeasurable f μ
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasurableEmbedding.rnDeriv_map : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β},
  MeasurableEmbedding f →
    ∀ (μ ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν],
      (fun x => (MeasureTheory.Measure.map f μ).rnDeriv (MeasureTheory.Measure.map f ν) (f x)) =ᵐ[ν] μ.rnDeriv ν
-- Mathlib.NumberTheory.LSeries.Basic
LSeriesHasSum.LSeriesSummable : ∀ {f : ℕ → ℂ} {s a : ℂ}, LSeriesHasSum f s a → LSeriesSummable f s
-- Init.Data.Int.Order
Int.eq_iff_le_and_ge : ∀ {x y : ℤ}, x = y ↔ x ≤ y ∧ y ≤ x
-- Mathlib.Algebra.GroupWithZero.Defs
noZeroDivisors_iff_eq_zero_of_mul : ∀ {M₀ : Type u_1} [inst : MulZeroClass M₀],
  NoZeroDivisors M₀ ↔ ∀ (x : M₀), x ≠ 0 → (∀ (y : M₀), x * y = 0 → y = 0) ∧ ∀ (y : M₀), y * x = 0 → y = 0
-- Mathlib.Data.Set.Sigma
Set.biInter_sigma' : ∀ {ι : Type u_1} {α : ι → Type u_3} {β : Type u_5} (s : Set ι) (t : (i : ι) → Set (α i)) (f : (i : ι) → α i → Set β),
  ⋂ i ∈ s, ⋂ j ∈ t i, f i j = ⋂ ij ∈ s.sigma t, f ij.fst ij.snd
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
inv_mul_le_iff_le_mul : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [MulLeftMono α] {a b c : α}, b⁻¹ * a ≤ c ↔ a ≤ b * c
-- Init.Data.List.MinMaxIdx
_private.Init.Data.List.MinMaxIdx.0.List.minIdxOn.go_eq : ∀ {β : Type u_1} {α : Type u_2} {i j : ℕ} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {x : α}
  {xs : List α} {f : α → β},
  List.minIdxOn.go✝ f x i j xs =
    if h : xs = [] then i else if f x ≤ f (List.minOn f xs h) then i else List.minIdxOn f xs h + j
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.descOpcycles_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) {A : C} (k : S.X₂ ⟶ A) (hk : CategoryTheory.CategoryStruct.comp S.f k = 0)
  [inst_2 : S.HasRightHomology] {A' : C} (α : A ⟶ A'),
  CategoryTheory.CategoryStruct.comp (S.descOpcycles k hk) α = S.descOpcycles (CategoryTheory.CategoryStruct.comp k α) ⋯
-- Mathlib.Topology.Homotopy.Contractible
ContractibleSpace.instOfNonemptyOfSubsingleton : ∀ {Y : Type u_2} [inst : TopologicalSpace Y] [Nonempty Y] [Subsingleton Y], ContractibleSpace Y
-- Mathlib.Topology.Category.TopCat.Basic
TopCat.isOpenEmbedding_iff_comp_isIso' : ∀ {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.IsIso g],
  Topology.IsOpenEmbedding (⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)) ↔
    Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Geometry.Manifold.ContMDiffMap
/-- The identity as a `C^n` map.  -/
ContMDiffMap.id : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_4} →
            [inst_3 : TopologicalSpace H] →
              {I : ModelWithCorners 𝕜 E H} →
                {M : Type u_6} →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] → {n : WithTop ℕ∞} → ContMDiffMap I I M M n
-- Mathlib.Topology.LocalAtTarget
TopologicalSpace.IsOpenCover.isOpenMap_iff_restrictPreimage : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {ι : Type u_3}
  {U : ι → TopologicalSpace.Opens β},
  TopologicalSpace.IsOpenCover U → (IsOpenMap f ↔ ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f))
-- Mathlib.Algebra.Group.Units.Defs
/-- The additive inverse of an additive unit in an `AddMonoid`.  -/
AddUnits.instNeg : {α : Type u} → [inst : AddMonoid α] → Neg (AddUnits α)
-- Mathlib.NumberTheory.RatFunc.Ostrowski
RatFunc.valuation_isEquiv_valuationIdeal_adic_of_valuation_X_le_one : ∀ {K : Type u_1} {Γ : Type u_2} [inst : Field K] [inst_1 : LinearOrderedCommGroupWithZero Γ]
  {v : Valuation (RatFunc K) Γ} [inst_2 : v.IsNontrivial] [inst_3 : Valuation.IsTrivialOn K v] (hle : v RatFunc.X ≤ 1)
  [v.IsRankOneDiscrete],
  v.IsEquiv (IsDedekindDomain.HeightOneSpectrum.valuation (RatFunc K) (RatFunc.valuationIdeal hle))
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.inv_right : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  {ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (f : ψ' ⟶ ψ') [inst_6 : CategoryTheory.IsIso f],
  CategoryTheory.inv f.right = (CategoryTheory.inv f).right
-- Mathlib.Data.Multiset.Sym
Multiset.card_sym2 : ∀ {α : Type u_1} {m : Multiset α}, m.sym2.card = (m.card + 1).choose 2
-- Mathlib.Topology.Algebra.Ring.Basic
IsTopologicalSemiring.toIsSemitopologicalSemiring : ∀ (R : Type u_2) [inst : TopologicalSpace R] [inst_1 : NonUnitalNonAssocSemiring R] [IsTopologicalSemiring R],
  IsSemitopologicalSemiring R
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LitValue.uint64.injEq : ∀ (val val_1 : UInt64),
  (Lean.Compiler.LCNF.LitValue.uint64 val = Lean.Compiler.LCNF.LitValue.uint64 val_1) = (val = val_1)
-- Mathlib.RingTheory.Smooth.Flat
/-- If `A` is `R`-smooth and `R` is Noetherian, then `A` is `R`-flat.  -/
Algebra.Smooth.flat_of_isNoetherianRing : ∀ (R : Type u_1) (A : Type u_2) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] [IsNoetherianRing R]
  [Algebra.Smooth R A], Module.Flat R A
-- Mathlib.NumberTheory.LSeries.ZetaZeros
/-- Any compact subset of `ℂ` contains only finitely many zeros of the Riemann zeta function.  -/
IsCompact.inter_riemannZetaZeros_finite : ∀ {S : Set ℂ}, IsCompact S → (S ∩ riemannZetaZeros).Finite
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
AddCircle.injective_toCircle : ∀ {T : ℝ}, T ≠ 0 → Function.Injective AddCircle.toCircle
-- Init.Data.SInt.Lemmas
Int16.add_neg_eq_sub : ∀ {a b : Int16}, a + -b = a - b
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.State.addGate.congr_simp : ∀ {aig : Std.Sat.AIG ℕ} {lhs lhs_1 : Std.Sat.AIG.Fanin} (e_lhs : lhs = lhs_1) {rhs rhs_1 : Std.Sat.AIG.Fanin}
  (e_rhs : rhs = rhs_1) (state : Std.Sat.AIG.toCNF.State✝ aig)
  {hlb : lhs.gate < (Std.Sat.AIG.toCNF.Cache.marks✝ (Std.Sat.AIG.toCNF.State.cache✝ state)).size}
  {hrb : rhs.gate < (Std.Sat.AIG.toCNF.Cache.marks✝ (Std.Sat.AIG.toCNF.State.cache✝ state)).size} (idx : ℕ)
  (h : idx < aig.decls.size) (htip : aig.decls[idx] = Std.Sat.AIG.Decl.gate lhs rhs)
  (hl : (Std.Sat.AIG.toCNF.Cache.marks✝ (Std.Sat.AIG.toCNF.State.cache✝ state))[lhs.gate] = true)
  (hr : (Std.Sat.AIG.toCNF.Cache.marks✝ (Std.Sat.AIG.toCNF.State.cache✝ state))[rhs.gate] = true),
  Std.Sat.AIG.toCNF.State.addGate✝ state idx h htip hl hr = Std.Sat.AIG.toCNF.State.addGate✝ state idx h ⋯ ⋯ ⋯
-- Mathlib.Topology.Algebra.Group.SubmonoidClosure
denseRange_zpow_iff_pow : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [CompactSpace G] [IsTopologicalGroup G] {x : G},
  (DenseRange fun x_1 => x ^ x_1) ↔ DenseRange fun x_1 => x ^ x_1
-- Mathlib.Analysis.Convex.Intrinsic
intrinsicInterior_singleton : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring 𝕜] [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
  [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] (x : P), intrinsicInterior 𝕜 {x} = {x}
-- Mathlib.Topology.Order.AtTopBotIxx
tendsto_comp_coe_Ioi_atBot : ∀ {X : Type u_1} [inst : LinearOrder X] [inst_1 : TopologicalSpace X] [OrderTopology X] {a : X} {α : Type u_2}
  {l : Filter α} {f : X → α},
  autoParam (Order.IsPredPrelimit a) tendsto_comp_coe_Ioi_atBot._auto_1 →
    (Filter.Tendsto (fun x => f ↑x) Filter.atBot l ↔ Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) l)
-- Mathlib.Data.Finset.Basic
Multiset.toFinset_inter : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Multiset α), (s ∩ t).toFinset = s.toFinset ∩ t.toFinset
-- Init.Data.String.Slice
/-- Appends the slices in a list of slices, placing the separator `s` between each pair.

Examples:

* `", ".toSlice.intercalate ["red".toSlice, "green".toSlice, "blue".toSlice] = "red, green, blue"`

* `" and ".toSlice.intercalate ["tea".toSlice, "coffee".toSlice] = "tea and coffee"`

* `" | ".toSlice.intercalate ["M".toSlice, "".toSlice, "N".toSlice] = "M |  | N"`
 -/
String.Slice.intercalate : String.Slice → List String.Slice → String
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.mk.injEq : ∀ (toProfinite : Profinite) [group : Group ↑toProfinite.toTop]
  [topologicalGroup : IsTopologicalGroup ↑toProfinite.toTop] (toProfinite_1 : Profinite)
  (group_1 : Group ↑toProfinite_1.toTop) (topologicalGroup_1 : IsTopologicalGroup ↑toProfinite_1.toTop),
  ({ toProfinite := toProfinite, group := group, topologicalGroup := topologicalGroup } =
      { toProfinite := toProfinite_1, group := group_1, topologicalGroup := topologicalGroup_1 }) =
    (toProfinite = toProfinite_1 ∧ group ≍ group_1)
-- Mathlib.Order.Interval.Set.Image
Set.image_subtype_val_Iic_subset : ∀ {α : Type u_1} [inst : Preorder α] {p : α → Prop} (a : { x // p x }), Subtype.val '' Set.Iic a ⊆ Set.Iic ↑a
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.mapTermRelEquiv_symm_apply : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} {β : Type v'}
  (ft : (n : ℕ) → L.Term (α ⊕ Fin n) ≃ L'.Term (β ⊕ Fin n)) (fr : (n : ℕ) → L.Relations n ≃ L'.Relations n) {n : ℕ}
  (a : L'.BoundedFormula β n),
  (FirstOrder.Language.BoundedFormula.mapTermRelEquiv ft fr).symm a =
    FirstOrder.Language.BoundedFormula.mapTermRel (fun n => ⇑(ft n).symm) (fun n => ⇑(fr n).symm) (fun x => id) a
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.congr_right : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {l : Filter α}
  {g₁ g₂ : α → F}, f =o[l] g₁ → (∀ (x : α), g₁ x = g₂ x) → f =o[l] g₂
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.HeapNode.brecOn.go : {α : Type u} →
  {motive : Batteries.BinomialHeap.Imp.HeapNode α → Sort u_1} →
    (t : Batteries.BinomialHeap.Imp.HeapNode α) →
      ((t : Batteries.BinomialHeap.Imp.HeapNode α) → Batteries.BinomialHeap.Imp.HeapNode.below t → motive t) →
        motive t ×' Batteries.BinomialHeap.Imp.HeapNode.below t
-- Mathlib.Algebra.Group.Defs
/-- `a ^ -(n + 1) = (a ^ (n + 1))⁻¹`  -/
DivInvMonoid.zpow_neg' : ∀ {G : Type u} [self : DivInvMonoid G] (n : ℕ) (a : G), a ^ Int.negSucc n = (a ^ ↑n.succ)⁻¹
-- Init.Core
/-- Heterogeneous equality postcomposes with propositional equality.  -/
heq_of_eq_of_heq : ∀ {α β : Sort u} {a a' : α} {b : β}, a = a' → a' ≍ b → a ≍ b
-- Mathlib.GroupTheory.Perm.Finite
Equiv.Perm.disjoint_ofSubtype_of_memFixedPoints_self : ∀ {α : Type u} [inst : DecidableEq α] {g : Equiv.Perm α} (u : Equiv.Perm ↑(Function.fixedPoints ⇑g)),
  (Equiv.Perm.ofSubtype u).Disjoint g
-- Mathlib.Algebra.Homology.Bifunctor
CategoryTheory.Functor.mapBifunctorHomologicalComplexObj_map_f_f : ∀ {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]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
  {I₁ : Type u_4} {I₂ : Type u_5} {c₁ : ComplexShape I₁} (c₂ : ComplexShape I₂) [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (K₁ : HomologicalComplex C₁ c₁)
  {K₂ K₂' : HomologicalComplex C₂ c₂} {φ : K₂ ⟶ K₂'} (i₁ : I₁) (i₂ : I₂),
  (((F.mapBifunctorHomologicalComplexObj c₂ K₁).map φ).f i₁).f i₂ = (F.obj (K₁.X i₁)).map (φ.f i₂)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.isSome_apply_of_mem_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Option γ} {k : α} (h : k ∈ Std.ExtHashMap.filterMap f m),
  (f (m.getKey k ⋯) m[k]).isSome = true
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.presieve₀_add : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) {T : C}
  (f : T ⟶ S), (E.add f).presieve₀ = E.presieve₀ ⊔ CategoryTheory.Presieve.singleton f
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.dist_le_two_norm' : ∀ {β : Type v} {γ : Type w} [inst : SeminormedAddCommGroup β] {f : γ → β} {C : ℝ},
  (∀ (x : γ), ‖f x‖ ≤ C) → ∀ (x y : γ), dist (f x) (f y) ≤ 2 * C
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.mk.congr_simp : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} (points points_1 : Fin (n + 1) → P) (e_points : points = points_1)
  (independent : AffineIndependent k points),
  { points := points, independent := independent } = { points := points_1, independent := ⋯ }
-- Mathlib.Analysis.Convex.Cone.Basic
ConvexCone.canLift : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : AddCommMonoid E] [inst_1 : TopologicalSpace E] [inst_2 : Semifield 𝕜]
  [inst_3 : LinearOrder 𝕜] [inst_4 : Module 𝕜 E] [inst_5 : TopologicalSpace 𝕜] [OrderTopology 𝕜] [DenselyOrdered 𝕜]
  [NoMaxOrder 𝕜] [ContinuousSMul 𝕜 E] [inst_10 : IsOrderedRing 𝕜],
  CanLift (ConvexCone 𝕜 E) (ProperCone 𝕜 E) (fun x => ↑↑x) fun C => (↑C).Nonempty ∧ IsClosed ↑C
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.IsDetpBalanced.smul : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R] {A : Matrix n n R}
  {a b : R}, A.IsDetpBalanced a b → ∀ (c : R), (c • A).IsDetpBalanced a b
-- Mathlib.Data.Set.Prod
Set.pi_if : ∀ {ι : Type u_1} {α : ι → Type u_2} {p : ι → Prop} [h : DecidablePred p] (s : Set ι) (t₁ t₂ : (i : ι) → Set (α i)),
  (s.pi fun i => if p i then t₁ i else t₂ i) = {i | i ∈ s ∧ p i}.pi t₁ ∩ {i | i ∈ s ∧ ¬p i}.pi t₂