mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multiequalizer.isoEqualizer.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) [inst_1 : CategoryTheory.Limits.HasMultiequalizer I]
  [inst_2 : CategoryTheory.Limits.HasProduct I.left] [inst_3 : CategoryTheory.Limits.HasProduct I.right],
  CategoryTheory.Limits.Multiequalizer.isoEqualizer I =
    CategoryTheory.Limits.limit.isoLimitCone
      {
        cone :=
          I.multiforkEquivPiFork.inverse.obj
            (CategoryTheory.Limits.limit.cone (CategoryTheory.Limits.parallelPair I.fstPiMap I.sndPiMap)),
        isLimit :=
          CategoryTheory.Limits.IsLimit.ofPreservesConeTerminal I.multiforkEquivPiFork.inverse
            (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Limits.parallelPair I.fstPiMap I.sndPiMap)) }
-- Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered
CategoryTheory.Functor.ιColimitType_eq_iff_of_isFiltered : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] [CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J (Type w₀)) {j j' : J} (x : F.obj j) (y : F.obj j'),
  F.ιColimitType j x = F.ιColimitType j' y ↔
    ∃ k f f', (CategoryTheory.ConcreteCategory.hom (F.map f)) x = (CategoryTheory.ConcreteCategory.hom (F.map f')) y
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.natTrailingDegree_zero : ∀ {R : Type u} [inst : Semiring R], Polynomial.natTrailingDegree 0 = 0
-- Mathlib.Data.ENNReal.Operations
ENNReal.sub_le_sub_iff_left : ∀ {a b c : ENNReal}, c ≤ a → a ≠ ⊤ → (a - b ≤ a - c ↔ c ≤ b)
-- Mathlib.Analysis.LocallyConvex.AbsConvex
absConvexHull_add_subset : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] {s t : Set E}, (absConvexHull 𝕜) (s + t) ⊆ (absConvexHull 𝕜) s + (absConvexHull 𝕜) t
-- Mathlib.Algebra.Group.Units.Defs
Units.instOne.eq_1 : ∀ {α : Type u} [inst : Monoid α], Units.instOne = { one := { val := 1, inv := 1, val_inv := ⋯, inv_val := ⋯ } }
-- Mathlib.Data.Matrix.Composition
Matrix.comp_apply : ∀ (I : Type u_1) (J : Type u_2) (K : Type u_3) (L : Type u_4) (R : Type u_5) (m : Matrix I J (Matrix K L R))
  (ik : I × K) (jl : J × L), (Matrix.comp I J K L R) m ik jl = m ik.1 jl.1 ik.2 jl.2
-- Init.Conv
/-- `conv => ...` allows the user to perform targeted rewriting on a goal or hypothesis,
by focusing on particular subexpressions.

See <https://lean-lang.org/theorem_proving_in_lean4/conv.html> for more details.

Basic forms:
* `conv => cs` will rewrite the goal with conv tactics `cs`.
* `conv at h => cs` will rewrite hypothesis `h`.
* `conv in pat => cs` will rewrite the first subexpression matching `pat` (see `pattern`).
 -/
Lean.Parser.Tactic.Conv.conv : Lean.ParserDescr
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.AppImplicitArg.skip.sizeOf_spec : sizeOf Lean.PrettyPrinter.Delaborator.AppImplicitArg.skip = 1
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
Tactic.ComputeAsymptotics.MultiseriesExpansion.one_toFun : ∀ {basis : Tactic.ComputeAsymptotics.Basis}, Tactic.ComputeAsymptotics.MultiseriesExpansion.one.toFun = 1
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.instIsSMulApplyForall : ∀ {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : (i : ι) → AddCommMonoid (M₁ i)] [inst_1 : AddCommMonoid M₂]
  [inst_2 : (i : ι) → TopologicalSpace (M₁ i)] [inst_3 : TopologicalSpace M₂] {R' : Type u_1} {A : Type u_3}
  [inst_4 : Semiring A] [inst_5 : (i : ι) → Module A (M₁ i)] [inst_6 : Module A M₂] [inst_7 : DistribSMul R' M₂]
  [inst_8 : ContinuousConstSMul R' M₂] [inst_9 : SMulCommClass A R' M₂],
  IsSMulApply R' (ContinuousMultilinearMap A M₁ M₂) ((i : ι) → M₁ i) M₂
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
_private.Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms.0.SimplexCategoryGenRel.simplicialInsert.match_1.splitter : (motive : List ℕ → Sort u_1) → (x : List ℕ) → (Unit → motive []) → ((b : ℕ) → (l : List ℕ) → motive (b :: l)) → motive x
-- Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
BoundedVariationOn.vectorMeasure_Ici : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : DenselyOrdered α] [inst_2 : TopologicalSpace α]
  [inst_3 : OrderTopology α] [inst_4 : SecondCountableTopology α] [inst_5 : CompactIccSpace α] [hα : MeasurableSpace α]
  [inst_6 : BorelSpace α] {E : Type u_2} [inst_7 : NormedAddCommGroup E] [inst_8 : CompleteSpace E] {f : α → E}
  (hf : BoundedVariationOn f Set.univ) (a : α),
  hf.vectorMeasure (Set.Ici a) = Filter.atTop.limUnder f - Function.leftLim f a
-- Mathlib.MeasureTheory.OuterMeasure.Basic
/-- If `s : ι → Set α` is a sequence of sets, `S = ⋃ n, s n`, and `m (S \ s n)` tends to zero along
some nontrivial filter (usually `atTop` on `ι = ℕ`), then `m S = ⨆ n, m (s n)`.  -/
MeasureTheory.OuterMeasure.iUnion_of_tendsto_zero : ∀ {α : Type u_1} {ι : Type u_3} (m : MeasureTheory.OuterMeasure α) {s : ι → Set α} (l : Filter ι) [l.NeBot],
  Filter.Tendsto (fun k => m ((⋃ n, s n) \ s k)) l (nhds 0) → m (⋃ n, s n) = ⨆ n, m (s n)
-- Mathlib.Data.Set.Countable
Set.countable_range : ∀ {β : Type v} {ι : Sort x} [Countable ι] (f : ι → β), (Set.range f).Countable
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.assignmentsInvariant_of_strongAssignmentsInvariant : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n),
  f.StrongAssignmentsInvariant → f.AssignmentsInvariant
-- Mathlib.Data.Real.ConjExponents
ENNReal.HolderConjugate.mul_eq_add : ∀ {p q : ENNReal} [h : p.HolderConjugate q], p * q = p + q
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.ofList_comp_toList : ∀ {α : Type u_1}, ⇑FreeMonoid.ofList ∘ ⇑FreeMonoid.toList = id
-- Mathlib.Tactic.CategoryTheory.Coherence
/-- `pure_coherence` uses the coherence theorem for monoidal categories to prove the goal.
It can prove any equality made up only of associators, unitors, and identities.
```lean
example {C : Type} [Category* C] [MonoidalCategory C] :
  (λ_ (𝟙_ C)).hom = (ρ_ (𝟙_ C)).hom := by
  pure_coherence
```

Users will typically just use the `coherence` tactic,
which can also cope with identities of the form
`a ≫ f ≫ b ≫ g ≫ c = a' ≫ f ≫ b' ≫ g ≫ c'`
where `a = a'`, `b = b'`, and `c = c'` can be proved using `pure_coherence`
 -/
Mathlib.Tactic.Coherence.pure_coherence : Lean.ParserDescr
-- Lean.Meta.Basic
Lean.Meta.instInhabitedParamInfo.default : Lean.Meta.ParamInfo
-- Std.Data.HashSet.Basic
Std.HashSet.instEmptyCollection : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → EmptyCollection (Std.HashSet α)
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.Pi.ι_π_of_ne_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {β : Type w} [inst_2 : DecidableEq β] (f : β → C) [inst_3 : CategoryTheory.Limits.HasProduct f] {b c : β},
  b ≠ c →
    ∀ {Z : C} (h : f c ⟶ Z),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.ι f b)
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f c) h) =
        CategoryTheory.CategoryStruct.comp 0 h
-- Init.Data.List.ToArray
List.zipWithM_toArray : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u} {m : Type u → Type v} [inst : Monad m] [LawfulMonad m] (f : α → β → m γ)
  (as : List α) (bs : List β),
  Array.zipWithM f as.toArray bs.toArray = do
    let __do_lift ← List.zipWithM f as bs
    pure __do_lift.toArray
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.startsWith_bool_eq_head? : ∀ {p : Char → Bool} {s : String.Slice}, s.startsWith p = Option.any p s.copy.toList.head?
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.HomClass.realize_term : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] {α : Type u'}
  {F : Type u_4} [inst_2 : FunLike F M N] [L.HomClass F M N] (g : F) {t : L.Term α} {v : α → M},
  FirstOrder.Language.Term.realize (⇑g ∘ v) t = g (FirstOrder.Language.Term.realize v t)
-- Mathlib.Order.Interval.Multiset
Multiset.Ico_subset_Ico_iff : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] {a₁ b₁ a₂ b₂ : α},
  a₁ < b₁ → (Multiset.Ico a₁ b₁ ⊆ Multiset.Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.map_a₁ : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) {A : Type v} [inst_1 : CommRing A] (f : R →+* A),
  (W.map f).a₁ = f W.a₁
-- Mathlib.Probability.Independence.Process.Basic
/-- A stochastic process $(X_s)_{s \in S}$ is independent from a random variable $Y$ if
for all $s_1, ..., s_p \in S$ the family $(X_{s_1}, ..., X_{s_p})$ is independent from $Y$.

This version only requires a.e.-measurability.  -/
ProbabilityTheory.IndepFun.process_indepFun₀ : ∀ {S : Type u_1} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {𝓧 : S → Type u_4} {𝓨 : Type u_5}
  [inst : (i : S) → MeasurableSpace (𝓧 i)] [inst_1 : MeasurableSpace 𝓨] {X : (i : S) → Ω → 𝓧 i} {Y : Ω → 𝓨},
  (∀ (i : S), AEMeasurable (X i) P) →
    AEMeasurable Y P →
      (∀ (I : Finset S), ProbabilityTheory.IndepFun (fun ω i => X (↑i) ω) Y P) →
        ∀ [MeasureTheory.IsZeroOrProbabilityMeasure P], ProbabilityTheory.IndepFun (fun ω i => X i ω) Y P
-- Init.Data.List.SplitOn.Lemmas
/-- When a list of the form `[...xs, sep, ...as]` is split at the `sep` element satisfying `p`,
the result is the concatenation of `splitOnP` called on `xs` and `as`  -/
List.splitOnP_append_cons : ∀ {α : Type u_1} {p : α → Bool} (xs as : List α) {sep : α},
  p sep = true → List.splitOnP p (xs ++ sep :: as) = List.splitOnP p xs ++ List.splitOnP p as
-- Init.Grind.Attr
Lean.Parser.Attr.grindGen : Lean.ParserDescr
-- Mathlib.Algebra.Order.Ring.Abs
_private.Mathlib.Algebra.Order.Ring.Abs.0.geomSum.eq_def : ∀ {α : Type u_1} [inst : CommRing α] (a b : α) (x : ℕ),
  geomSum✝ a b x =
    match x with
    | 0 => 1
    | n.succ => a * geomSum✝ a b n + b ^ (n + 1)
-- Mathlib.Order.Interval.Finset.Basic
Finset.right_notMem_Ioo : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α], b ∉ Finset.Ioo a b
-- Mathlib.Topology.UniformSpace.Basic
uniformContinuous_toMul : ∀ {α : Type ua} [inst : UniformSpace α], UniformContinuous ⇑Additive.toMul
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf'_le_iff : ∀ {α : Type u_2} {ι : Type u_5} [inst : LinearOrder α] {s : Finset ι} (H : s.Nonempty) {f : ι → α} {a : α},
  s.inf' H f ≤ a ↔ ∃ b ∈ s, f b ≤ a
-- Mathlib.FieldTheory.Minpoly.IsConjRoot
/-- A variant of `IsConjRoot.eq_of_isConjRoot_algebraMap`, only assuming `IsDomain R`,
`IsTorsionFree R A` and `Function.Injective (algebraMap R A)` instead of `Field R`. If `x` is a
conjugate root of some element `algebraMap R S r` in the image of the base ring, then
`x = algebraMap R S r`.
 -/
IsConjRoot.eq_algebraMap_of_injective : ∀ {R : Type u_1} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsDomain S]
  [IsDomain R] [Module.IsTorsionFree R S] {r : R} {x : S},
  IsConjRoot R ((algebraMap R S) r) x → Function.Injective ⇑(algebraMap R S) → x = (algebraMap R S) r
-- Mathlib.Topology.AlexandrovDiscrete
nhds_basis_nhdsKer_singleton : ∀ {α : Type u_3} [inst : TopologicalSpace α] [AlexandrovDiscrete α] (a : α),
  (nhds a).HasBasis (fun x => True) fun x => nhdsKer {a}
-- Init.Data.SInt.Lemmas
ISize.add_right_inj : ∀ {a b : ISize} (c : ISize), c + a = c + b ↔ a = b
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddLocalization.ndrec_mk : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {p : AddLocalization S → Sort u}
  (f : (a : M) → (b : ↥S) → p (AddLocalization.mk a b))
  (H : ∀ {a c : M} {b d : ↥S} (h : (AddLocalization.r S) (a, b) (c, d)), ⋯ ▸ f a b = f c d) (a : M) (b : ↥S),
  AddLocalization.rec f H (AddLocalization.mk a b) = f a b
-- Mathlib.Algebra.Group.WithOne.Basic
WithZero.mapAddHom_coe : ∀ {α : Type u} {β : Type v} [inst : Add α] [inst_1 : Add β] (f : α →ₙ+ β) (a : α), (WithZero.mapAddHom f) ↑a = ↑(f a)
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.monomial_eq_monomial_iff : ∀ {R : Type u} [inst : Semiring R] {m n : ℕ} {a b : R},
  (Polynomial.monomial m) a = (Polynomial.monomial n) b ↔ m = n ∧ a = b ∨ a = 0 ∧ b = 0
-- Mathlib.Algebra.BigOperators.Fin
Fin.partialSum.eq_1 : ∀ {M : Type u_2} [inst : AddMonoid M] {n : ℕ} (f : Fin n → M) (i : Fin (n + 1)),
  Fin.partialSum f i = (List.take (↑i) (List.ofFn f)).sum
-- Mathlib.Algebra.Notation.Support
Function.mulSupport_nonempty_iff : ∀ {ι : Type u_1} {M : Type u_3} [inst : One M] {f : ι → M}, (Function.mulSupport f).Nonempty ↔ f ≠ 1
-- Mathlib.CategoryTheory.Center.NegOnePow
CategoryTheory.CatCenter.app_neg_one_zpow : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (n : ℤ) (X : C),
  (↑((-1) ^ n)).app X = n.negOnePow • CategoryTheory.CategoryStruct.id X
-- Mathlib.Order.ConditionallyCompletePartialOrder.Defs
ConditionallyCompletePartialOrderInf.toInfSet : {α : Type u_3} → [self : ConditionallyCompletePartialOrderInf α] → InfSet α
-- Mathlib.CategoryTheory.Shift.Opposite
/-- Construction of the naive shift on the opposite category of a category `C`:
the shiftfunctor by `n` is `(shiftFunctor C n).op`.  -/
CategoryTheory.HasShift.mkShiftCoreOp : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (A : Type u_2) → [inst_1 : AddMonoid A] → [CategoryTheory.HasShift C A] → CategoryTheory.ShiftMkCore Cᵒᵖ A
-- Std.Http.Data.Chunk
Std.Http.Trailer.instEncodeV11 : Std.Http.Internal.Encode Std.Http.Version.v11 Std.Http.Trailer
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.div_iUnion : ∀ {α : Type u_2} {ι : Sort u_5} [inst : Div α] (s : Set α) (t : ι → Set α), s / ⋃ i, t i = ⋃ i, s / t i
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.prodComparison_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) (A B : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.prodComparison F A B)
      (CategoryTheory.SemiCartesianMonoidalCategory.fst (F.obj A) (F.obj B)) =
    F.map (CategoryTheory.SemiCartesianMonoidalCategory.fst A B)
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_def_assoc : ∀ {C : Type u_1} {D : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} {inst_2 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {c c' : C} {d d' : D} (f : c ⟶ c') (g : d ⟶ d')
  {Z : D} (h : CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c' d' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom f g) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f d)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c' g)
        h)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.isLocalizationMap_top_nat_int : ⊤.IsLocalizationMap Nat.cast
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.iCycles.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) [inst_2 : K.HasHomology i],
  K.iCycles i = (K.sc i).iCycles
-- Mathlib.Topology.UnitInterval
unitInterval.symm_inj : ∀ {i j : ↑unitInterval}, unitInterval.symm i = unitInterval.symm j ↔ i = j
-- Mathlib.Data.Rat.Defs
Rat.divInt_one_one : Rat.divInt 1 1 = 1
-- Mathlib.Combinatorics.SimpleGraph.Ends.Defs
SimpleGraph.ComponentCompl.exists_eq_mk : ∀ {V : Type u} {G : SimpleGraph V} {K : Set V} (C : G.ComponentCompl K), ∃ v, ∃ (h : v ∉ K), G.componentComplMk h = C
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.comp_sumAddHom : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] {δ : Type u_1}
  [inst_1 : (i : ι) → AddZeroClass (β i)] [inst_2 : AddCommMonoid γ] [inst_3 : AddCommMonoid δ] (g : γ →+ δ)
  (f : (i : ι) → β i →+ γ), g.comp (DFinsupp.sumAddHom f) = DFinsupp.sumAddHom fun a => g.comp (f a)
-- Mathlib.Tactic.NormNum.BigOperators
Mathlib.Meta.Finset.ProveEmptyOrConsResult.empty.sizeOf_spec : ∀ {u : Lean.Level} {α : Q(Type u)} {s : Q(Finset «$α»)} (pf : Q(«$s» = ∅)),
  sizeOf (Mathlib.Meta.Finset.ProveEmptyOrConsResult.empty pf) = 1 + sizeOf pf
-- Init.Data.UInt.Lemmas
instCommutativeUInt32HAdd : Std.Commutative fun x1 x2 => x1 + x2
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.unitOfList_cons : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {hd : α} {tl : List α},
  Std.DHashMap.Const.unitOfList (hd :: tl) = Std.DHashMap.Const.insertManyIfNewUnit (∅.insertIfNew hd ()) tl
-- Std.Sat.AIG.Basic
_private.Std.Sat.AIG.Basic.0.Std.Sat.AIG.toGraphviz.go.match_1.eq_2 : ∀ {α : Type} (motive : Std.Sat.AIG.Decl α → Sort u_1) (idx : α)
  (h_1 : Std.Sat.AIG.Decl.atom idx = Std.Sat.AIG.Decl.false → motive Std.Sat.AIG.Decl.false)
  (h_2 : (idx_1 : α) → Std.Sat.AIG.Decl.atom idx = Std.Sat.AIG.Decl.atom idx_1 → motive (Std.Sat.AIG.Decl.atom idx_1))
  (h_3 :
    (lhs rhs : Std.Sat.AIG.Fanin) →
      Std.Sat.AIG.Decl.atom idx = Std.Sat.AIG.Decl.gate lhs rhs → motive (Std.Sat.AIG.Decl.gate lhs rhs)),
  (match elem : Std.Sat.AIG.Decl.atom idx with
    | Std.Sat.AIG.Decl.false => h_1 elem
    | Std.Sat.AIG.Decl.atom idx_1 => h_2 idx_1 elem
    | Std.Sat.AIG.Decl.gate lhs rhs => h_3 lhs rhs elem) =
    h_2 idx ⋯
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
/-- The set containing all color classes.  -/
SimpleGraph.Coloring.colorClasses : {V : Type u} → {G : SimpleGraph V} → {α : Type u_2} → G.Coloring α → Set (Set V)
-- Std.Data.Internal.Cut
Std.Internal.IsStrictCut.lt_of_isLE_of_lt : ∀ {α : Type u} {cmp : α → α → Ordering} {cut : α → Ordering} [Std.Internal.IsStrictCut cmp cut] {k k' : α},
  (cut k').isLE = true → cmp k' k = Ordering.lt → cut k = Ordering.lt
-- Mathlib.Order.UpperLower.Fibration
Relation.fibration_iff_isUpperSet_image_Ici : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : LE β],
  Relation.Fibration (fun x1 x2 => x1 ≥ x2) (fun x1 x2 => x1 ≥ x2) f ↔ ∀ (x : α), IsUpperSet (f '' Set.Ici x)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getD_diff_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α} {fallback : β}, k ∉ m₂ → (m₁ \ m₂).getD k fallback = m₁.getD k fallback
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
HomogeneousIdeal.instTop : {ι : Type u_1} →
  {σ : Type u_2} →
    {A : Type u_3} →
      [inst : Semiring A] →
        [inst_1 : DecidableEq ι] →
          [inst_2 : AddMonoid ι] →
            [inst_3 : SetLike σ A] →
              [inst_4 : AddSubmonoidClass σ A] → {𝒜 : ι → σ} → [inst_5 : GradedRing 𝒜] → Top (HomogeneousIdeal 𝒜)
-- Mathlib.Logic.Equiv.PartialEquiv
Equiv.transPartialEquiv_target : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : α ≃ β) (f' : PartialEquiv β γ),
  (e.transPartialEquiv f').target = f'.target
-- Init.Data.List.Nat.TakeDrop
List.drop_eq_getElem?_toList_append : ∀ {α : Type u_1} {l : List α} {i : ℕ}, List.drop i l = l[i]?.toList ++ List.drop (i + 1) l
-- Mathlib.Algebra.Category.Grp.Basic
/-- multiplicative equivalences between `Group`s are the same as (isomorphic to) isomorphisms
in `GrpCat`  -/
mulEquivIsoGroupIso : {X Y : GrpCat} → ↑X ≃* ↑Y ≅ X ≅ Y
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.instIsSMulApplySetENNReal : ∀ {α : Type u_1} {R : Type u_3} [inst : SMul R ENNReal] [inst_1 : IsScalarTower R ENNReal ENNReal],
  IsSMulApply R (MeasureTheory.OuterMeasure α) (Set α) ENNReal
-- Mathlib.Data.Set.Pairwise.Basic
Set.pairwise_empty : ∀ {α : Type u_1} (r : α → α → Prop), ∅.Pairwise r
-- Mathlib.Control.Fix
/-- A series of successive, finite approximation of the fixed point of `f`, defined by
`approx f n = f^[n] ⊥`. The limit of this chain is the fixed point of `f`.  -/
Part.Fix.approx : {α : Type u_1} → {β : α → Type u_2} → (((a : α) → Part (β a)) → (a : α) → Part (β a)) → Stream' ((a : α) → Part (β a))
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.sqLe_of_le : ∀ {c d x y z w : ℕ}, z ≤ x → y ≤ w → Zsqrtd.SqLe x c y d → Zsqrtd.SqLe z c w d
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
/-- The pullback cone in the opposite category associated to the cocone of
a commutative square identifies to the cone of the flipped commutative square in
the opposite category  -/
CategoryTheory.CommSq.coconeOp : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W X Y Z : C} →
      {f : W ⟶ X} → {g : W ⟶ Y} → {h : X ⟶ Z} → {i : Y ⟶ Z} → (p : CategoryTheory.CommSq f g h i) → p.cocone.op ≅ ⋯.cone
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.nrRealPlaces_pos_of_odd_finrank : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K],
  Odd (Module.finrank ℚ K) → 0 < NumberField.InfinitePlace.nrRealPlaces K
-- Mathlib.Data.PNat.Defs
/-- Convert a natural number to a positive natural number. The
positivity assumption is inferred by `dec_trivial`.  -/
Nat.toPNat : (n : ℕ) → autoParam (0 < n) Nat.toPNat._auto_1 → ℕ+
-- Mathlib.AlgebraicGeometry.Scheme
/-- **Alias** of `AlgebraicGeometry.Scheme.preimage_basicOpen`. -/
AlgebraicGeometry.Scheme.Hom.preimage_basicOpen : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U : Y.Opens} (r : ↑(Y.presheaf.obj (Opposite.op U))),
  (TopologicalSpace.Opens.map f.base).obj (Y.basicOpen r) =
    X.basicOpen ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.app f U)) r)
-- Mathlib.Order.Interval.Finset.Defs
Finset.card_uIcc_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] [inst_4 : DecidableLE (α × β)] (x y : α × β),
  (Finset.uIcc x y).card = (Finset.uIcc x.1 y.1).card * (Finset.uIcc x.2 y.2).card
-- Mathlib.Algebra.GroupWithZero.Defs
MulZeroOneClass.toMulZeroClass : {M₀ : Type u} → [self : MulZeroOneClass M₀] → MulZeroClass M₀
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.grind.debug.proofs : Lean.Option Bool
-- Lean.Message
Lean.instToJsonMessageSeverity : Lean.ToJson Lean.MessageSeverity
-- Mathlib.Analysis.Calculus.Deriv.Mul
HasDerivWithinAt.smul : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s : Set 𝕜} {𝕜' : Type u_2} [inst_3 : NormedRing 𝕜']
  [inst_4 : NormedAlgebra 𝕜 𝕜'] [inst_5 : Module 𝕜' F] [IsBoundedSMul 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : 𝕜 → 𝕜'}
  {c' : 𝕜'}, HasDerivWithinAt c c' s x → HasDerivWithinAt f f' s x → HasDerivWithinAt (c • f) (c x • f' + c' • f x) s x