mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SetFamily.Compression.UV
UV.compression_self : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] [inst_1 : DecidableRel Disjoint] [inst_2 : DecidableLE α]
  [inst_3 : DecidableEq α] (u : α) (s : Finset α), UV.compression u u s = s
-- Mathlib.Analysis.Convex.Join
convexJoin_mono_left : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {t s₁ s₂ : Set E}, s₁ ⊆ s₂ → convexJoin 𝕜 s₁ t ⊆ convexJoin 𝕜 s₂ t
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.coeff_single_mul_apply : ∀ {R : Type u_1} {G : Type u_3} [inst : Semiring R] [inst_1 : AddGroup G] (x : AddMonoidAlgebra R G) (r : R) (g h : G),
  (AddMonoidAlgebra.single g r * x).coeff h = r * x.coeff (-g + h)
-- Mathlib.Algebra.Homology.BifunctorFlip
HomologicalComplex.mapBifunctorFlipIso_hom_naturality_assoc : ∀ {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] {I₁ : Type u_4}
  {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Preadditive D] {K₁ L₁ : HomologicalComplex C₁ c₁} (φ₁ : K₁ ⟶ L₁)
  {K₂ L₂ : HomologicalComplex C₂ c₂} (φ₂ : K₂ ⟶ L₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
  [inst_6 : F.PreservesZeroMorphisms] [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J)
  [inst_8 : TotalComplexShape c₁ c₂ c] [inst_9 : TotalComplexShape c₂ c₁ c]
  [inst_10 : TotalComplexShapeSymmetry c₁ c₂ c] [inst_11 : DecidableEq J] [inst_12 : K₁.HasMapBifunctor K₂ F c]
  [inst_13 : L₁.HasMapBifunctor L₂ F c] {Z : HomologicalComplex D c} (h : L₁.mapBifunctor L₂ F c ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctorMap φ₂ φ₁ F.flip c)
      (CategoryTheory.CategoryStruct.comp (L₁.mapBifunctorFlipIso L₂ F c).hom h) =
    CategoryTheory.CategoryStruct.comp (K₁.mapBifunctorFlipIso K₂ F c).hom
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctorMap φ₁ φ₂ F c) h)
-- Init.BinderPredicates
/-- Declare `∃ x ≠ y, ...` as syntax for `∃ x, x ≠ y ∧ ...`  -/
Lean.«binderPred≠_» : Lean.ParserDescr
-- Mathlib.Algebra.Group.Defs
NSMul.toSMul : {M : Type u_2} → [NSMul M] → SMul ℕ M
-- Lean.Parser.Types
Lean.Parser.ParserModuleContext.env : Lean.Parser.ParserModuleContext → Lean.Environment
-- Mathlib.NumberTheory.RamificationInertia.Inertia
/-- The absolute norm of an ideal `P` above a rational (positive) prime `p` is
`p ^ ((span {p}).inertiaDeg' P)`.
See `absNorm_eq_pow_inertiaDeg` for a version with `p` of type `ℤ`.  -/
Ideal.absNorm_eq_pow_inertiaDeg' : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDedekindDomain R] [inst_2 : Module.Free ℤ R] [Module.Finite ℤ R] {p : ℕ}
  (P : Ideal R) [P.LiesOver (Ideal.span {↑p})], Nat.Prime p → Ideal.absNorm P = p ^ (Ideal.span {↑p}).inertiaDeg' P
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- In a preadditive category, we can construct a binary biproduct for `X Y : C` from
any binary bicone `b` satisfying `total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.X`.

(That is, such a bicone is a limit cone and a colimit cocone.)
 -/
CategoryTheory.Limits.hasBinaryBiproduct_of_total : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  (b : CategoryTheory.Limits.BinaryBicone X Y),
  CategoryTheory.CategoryStruct.comp b.fst b.inl + CategoryTheory.CategoryStruct.comp b.snd b.inr =
      CategoryTheory.CategoryStruct.id b.pt →
    CategoryTheory.Limits.HasBinaryBiproduct X Y
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
SlashInvariantForm.mk : {Γ : outParam (Subgroup (GL (Fin 2) ℝ))} →
  {k : outParam ℤ} →
    (toFun : UpperHalfPlane → ℂ) → (∀ γ ∈ Γ, SlashAction.map k γ toFun = toFun) → SlashInvariantForm Γ k
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.Int16.beq_eq_decide_eq : ∀ {a b : Int16}, (a == b) = decide (a = b)
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.reverse_X_mul : ∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R), (Polynomial.X * p).reverse = p.reverse
-- Mathlib.Geometry.RingedSpace.Basic
AlgebraicGeometry.RingedSpace.basicOpen_le : ∀ (X : AlgebraicGeometry.RingedSpace) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace}
  (f : ↑(X.presheaf.obj (Opposite.op U))), X.basicOpen f ≤ U
-- Init.Data.List.MapIdx
List.mapIdx_eq_replicate_iff : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : ℕ → α → β} {b : β},
  List.mapIdx f l = List.replicate l.length b ↔ ∀ (i : ℕ) (h : i < l.length), f i l[i] = b
-- Lean.Meta.Sym.Arith.Poly
/-- Returns the leading coefficient of the given polynomial  -/
Lean.Grind.CommRing.Poly.lc : Lean.Grind.CommRing.Poly → ℤ
-- Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsFunctorPreservesLimit : ∀ {J : Type u_1} {C : Type u_3} (K : Type u_5) [inst : CategoryTheory.Category.{v_1, u_5} K]
  [inst_1 : CategoryTheory.Category.{v_3, u_1} J] [inst_2 : CategoryTheory.Category.{v_5, u_3} C]
  (F : CategoryTheory.Functor K J), (CategoryTheory.ObjectProperty.preservesLimit F).IsClosedUnderIsomorphisms
-- Mathlib.GroupTheory.OrderOfElement
orderOf_le_card_univ : ∀ {G : Type u_1} [inst : Monoid G] {x : G} [inst_1 : Fintype G], orderOf x ≤ Fintype.card G
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.getD.eq_2 : ∀ {α : Type u} {β : Type v} [inst : BEq α] (a : α) (fallback : β) (k : α) (v : β)
  (es : Std.DHashMap.Internal.AssocList α fun x => β),
  Std.DHashMap.Internal.AssocList.getD a fallback (Std.DHashMap.Internal.AssocList.cons k v es) =
    bif k == a then v else Std.DHashMap.Internal.AssocList.getD a fallback es
-- Mathlib.Algebra.MonoidAlgebra.Support
/-- **Alias** of `MonoidAlgebra.support_coeff_mul_single_eq_image`. -/
MonoidAlgebra.support_mul_single_eq_image : ∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] [inst_1 : Mul G] [inst_2 : DecidableEq G] (f : MonoidAlgebra k G)
  {r : k},
  (∀ (y : k), y * r = 0 ↔ y = 0) →
    ∀ {x : G},
      IsRightRegular x →
        (f * MonoidAlgebra.single x r).coeff.support = Finset.image (fun x_1 => x_1 * x) f.coeff.support
-- Mathlib.Topology.Connected.Clopen
ConnectedComponents.equivOfIsClopen_symm_mk : ∀ {α : Type u} [inst : TopologicalSpace α] {ι : Type u_3} {U : ι → Set α} (hclopen : ∀ (i : ι), IsClopen (U i))
  (hdisj : Pairwise (Function.onFun Disjoint U)) (hunion : ⋃ i, U i = Set.univ) {i : ι} (x : ↑(U i)),
  (ConnectedComponents.equivOfIsClopen hclopen hdisj hunion).symm ⟨i, ConnectedComponents.mk x⟩ =
    ConnectedComponents.mk ↑x
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
AEMeasurable.clog : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℂ},
  AEMeasurable f μ → AEMeasurable (fun x => Complex.log (f x)) μ
-- Mathlib.Algebra.MvPolynomial.Eval
/-- If `f` is a left-inverse of `g` then `map f` is a left-inverse of `map g`.  -/
MvPolynomial.map_leftInverse : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] {f : R →+* S₁}
  {g : S₁ →+* R}, Function.LeftInverse ⇑f ⇑g → Function.LeftInverse ⇑(MvPolynomial.map f) ⇑(MvPolynomial.map g)
-- Mathlib.Algebra.MvPolynomial.Equiv
/-- The function from multivariable polynomials in a sum of two types,
to multivariable polynomials in one of the types,
with coefficients in multivariable polynomials in the other type.

See `sumRingEquiv` for the ring isomorphism.
 -/
MvPolynomial.sumToIter : (R : Type u) →
  (S₁ : Type v) →
    (S₂ : Type w) → [inst : CommSemiring R] → MvPolynomial (S₁ ⊕ S₂) R →+* MvPolynomial S₁ (MvPolynomial S₂ R)
-- Mathlib.Topology.Neighborhoods
/-- The open neighborhoods of `x` are a basis for the neighborhood filter. See `nhds_basis_opens`
for a variant using open sets around `x` instead.  -/
nhds_basis_opens' : ∀ {X : Type u} [inst : TopologicalSpace X] (x : X), (nhds x).HasBasis (fun s => s ∈ nhds x ∧ IsOpen s) fun x => x
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffOn.continuousOn_fderivWithin : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {n : WithTop ℕ∞}, ContDiffOn 𝕜 n f s → UniqueDiffOn 𝕜 s → 1 ≤ n → ContinuousOn (fderivWithin 𝕜 f s) s
-- Mathlib.MeasureTheory.Integral.Lebesgue.Add
/-- A double integral of a product where each factor contains only one variable
is a product of integrals  -/
MeasureTheory.lintegral_lintegral_mul : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_3} [inst : MeasurableSpace β]
  {ν : MeasureTheory.Measure β} {f : α → ENNReal} {g : β → ENNReal},
  AEMeasurable f μ →
    AEMeasurable g ν → ∫⁻ (x : α), ∫⁻ (y : β), f x * g y ∂ν ∂μ = (∫⁻ (x : α), f x ∂μ) * ∫⁻ (y : β), g y ∂ν
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
ComplexShape.Embedding.AreComplementary.disjoint : ∀ {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c}, e₁.AreComplementary e₂ → ∀ (i₁ : ι₁) (i₂ : ι₂), e₁.f i₁ ≠ e₂.f i₂
-- Mathlib.Algebra.Homology.ShortComplex.Limits
CategoryTheory.ShortComplex.instPreservesLimitsOfShapeπ₁ : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasLimitsOfShape J C],
  CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.ShortComplex.π₁
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.measure_eq_measure_of_null_sdiff : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α}, s ⊆ t → μ (t \ s) = 0 → μ s = μ t
-- Mathlib.Computability.PartrecCode
/-- A decoder for `Nat.Partrec.Code.encodeCode`, taking any ℕ to the `Nat.Partrec.Code` it represents.
 -/
Nat.Partrec.Code.ofNatCode : ℕ → Nat.Partrec.Code
-- Mathlib.Order.Basic
Pi.sdiff_apply : ∀ {ι : Type u_1} {π : ι → Type u_4} [inst : (i : ι) → SDiff (π i)] (x y : (i : ι) → π i) (i : ι), (x \ y) i = x i \ y i
-- Mathlib.Analysis.Normed.Operator.Banach
ContinuousLinearMap.equivRange_symm_toLinearEquiv : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'}
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {F : Type u_4}
  [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜' F] {σ' : 𝕜' →+* 𝕜} [inst_6 : RingHomInvPair σ σ']
  [inst_7 : RingHomIsometric σ] [inst_8 : RingHomIsometric σ'] [inst_9 : CompleteSpace F] [inst_10 : CompleteSpace E]
  [inst_11 : RingHomInvPair σ' σ] {f : E →SL[σ] F} (hinj : Function.Injective ⇑f) (hclo : IsClosed (Set.range ⇑f)),
  (↑(ContinuousLinearMap.equivRange hinj hclo)).symm = (LinearEquiv.ofInjective (↑f) hinj).symm
-- Mathlib.Algebra.Group.Basic
div_right_inj : ∀ {G : Type u_3} [inst : Group G] {a b c : G}, a / b = a / c ↔ b = c
-- Mathlib.RingTheory.ClassGroup.Basic
/-- Induction principle for the class group: to show something holds for all `x : ClassGroup R`,
we can choose a fraction field `K` and show it holds for the equivalence class of each
`I : FractionalIdeal R⁰ K`.  -/
ClassGroup.induction : ∀ {R : Type u_1} (K : Type u_2) [inst : CommRing R] [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDomain R] {P : ClassGroup R → Prop},
  (∀ (I : (FractionalIdeal (nonZeroDivisors R) K)ˣ), P ((ClassGroup.mk K) I)) → ∀ (x : ClassGroup R), P x
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.contains_insertManyIfNewUnit_of_contains : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) {ρ : Type w}
  [inst_2 : ForIn Id ρ α] [EquivBEq α] [LawfulHashable α],
  (↑m).WF →
    ∀ {l : ρ} {k : α},
      m.contains k = true → (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l)).contains k = true
-- Mathlib.Algebra.Order.Group.OrderIso
OrderIso.addRight.eq_1 : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [inst_2 : AddRightMono α] (a : α),
  OrderIso.addRight a = { toEquiv := Equiv.addRight a, map_rel_iff' := ⋯ }
-- Mathlib.AlgebraicGeometry.Cover.Directed
AlgebraicGeometry.Scheme.OpenCover.glueMorphismsOverOfLocallyDirected.eq_1 : ∀ {S : AlgebraicGeometry.Scheme} {X : CategoryTheory.Over S} (𝒰 : X.left.OpenCover)
  [inst : CategoryTheory.Category.{v_2, u_1} 𝒰.I₀] [inst_1 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰]
  {Y : CategoryTheory.Over S} (g : (i : 𝒰.I₀) → 𝒰.X i ⟶ Y.left)
  (h :
    ∀ {i j : 𝒰.I₀} (hij : i ⟶ j),
      CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij) (g j) = g i)
  (w : ∀ (i : 𝒰.I₀), CategoryTheory.CategoryStruct.comp (g i) Y.hom = CategoryTheory.CategoryStruct.comp (𝒰.f i) X.hom),
  𝒰.glueMorphismsOverOfLocallyDirected g h w = CategoryTheory.Over.homMk (𝒰.glueMorphismsOfLocallyDirected g ⋯) ⋯
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.mem_insertUnit_fold_units : ∀ {n : ℕ} (units : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)))
  (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (foundContradiction : Bool)
  (l : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
  have insertUnit_fold_res :=
    List.foldl Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertUnit (units, assignments, foundContradiction) l;
  ∀ l' ∈ insertUnit_fold_res.1.toList, l' ∈ l ∨ l' ∈ units.toList
-- Mathlib.Algebra.Notation.Support
Pi.support_single_zero : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Zero M] {i : ι}, Function.support (Pi.single i 0) = ∅
-- Mathlib.CategoryTheory.CopyDiscardCategory.Deterministic
/-- Deterministic morphisms commute with copying.  -/
CategoryTheory.Deterministic.copy_natural : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.CopyDiscardCategory C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Deterministic f],
  CategoryTheory.CategoryStruct.comp f CategoryTheory.ComonObj.comul =
    CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
      (CategoryTheory.MonoidalCategoryStruct.tensorHom f f)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey_eq_getEntry_fst : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {a : α}
  {h : Std.Internal.List.containsKey a l = true},
  Std.Internal.List.getKey a l h = (Std.Internal.List.getEntry a l h).fst
-- Mathlib.ModelTheory.Basic
/-- Interpretation of a constant symbol  -/
FirstOrder.Language.constantMap : {L : FirstOrder.Language} → {M : Type w} → [L.Structure M] → L.Constants → M
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Path.singleton_coe : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (h : G.Adj u v),
  ↑(SimpleGraph.Path.singleton h) = SimpleGraph.Walk.cons h SimpleGraph.Walk.nil
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.GrindCnstr.isGround : Lean.Parser.Parser
-- Mathlib.Computability.RegularExpressions
_private.Mathlib.Computability.RegularExpressions.0.RegularExpression.deriv.match_1.eq_1 : ∀ {α : Type u_1} (motive : RegularExpression α → α → Sort u_2) (x : α) (h_1 : (x : α) → motive RegularExpression.zero x)
  (h_2 : (x : α) → motive RegularExpression.epsilon x) (h_3 : (a₁ a₂ : α) → motive (RegularExpression.char a₁) a₂)
  (h_4 : (P Q : RegularExpression α) → (a : α) → motive (P.plus Q) a)
  (h_5 : (P Q : RegularExpression α) → (a : α) → motive (P.comp Q) a)
  (h_6 : (P : RegularExpression α) → (a : α) → motive P.star a),
  (match RegularExpression.zero, x with
    | RegularExpression.zero, x => h_1 x
    | RegularExpression.epsilon, x => h_2 x
    | RegularExpression.char a₁, a₂ => h_3 a₁ a₂
    | P.plus Q, a => h_4 P Q a
    | P.comp Q, a => h_5 P Q a
    | P.star, a => h_6 P a) =
    h_1 x
-- Mathlib.NumberTheory.Zsqrtd.GaussianInt
GaussianInt.mod_def : ∀ (x y : GaussianInt), x % y = x - y * (x / y)
-- Mathlib.Topology.DiscreteQuotient
/-- The setoid whose quotient yields the discrete quotient.  -/
DiscreteQuotient.toSetoid : {X : Type u_5} → [inst : TopologicalSpace X] → DiscreteQuotient X → Setoid X
-- Mathlib.Geometry.Diffeology.Basic
Diffeology.dSmooth_const : ∀ {X : Type u_1} {Y : Type u_2} [inst : DiffeologicalSpace X] [inst_1 : DiffeologicalSpace Y] {y : Y},
  Diffeology.DSmooth fun x => y
-- Mathlib.Algebra.Category.Grp.CartesianMonoidal
CommGrpCat.binaryProductLimitCone_isLimit_lift : ∀ (G H : CommGrpCat) (t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair G H)),
  (G.binaryProductLimitCone H).isLimit.lift t =
    CommGrpCat.ofHom
      ((CommGrpCat.Hom.hom (CategoryTheory.Limits.BinaryFan.fst t)).prod
        (CommGrpCat.Hom.hom (CategoryTheory.Limits.BinaryFan.snd t)))
-- Mathlib.Topology.Order.Monotone
MonotoneOn.insert_of_continuousWithinAt : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : LinearOrder β] {s : Set α} {x : α} {f : α → β} [inst_4 : TopologicalSpace β] [OrderClosedTopology β],
  MonotoneOn f s → ClusterPt x (Filter.principal s) → ContinuousWithinAt f s x → MonotoneOn f (insert x s)
-- Mathlib.Tactic.TacticAnalysis
/-- Test the `config` against a sequence of tactics, using the context info and tactic info
from the start of the sequence.  -/
Mathlib.TacticAnalysis.testTacticSeq : (config : Mathlib.TacticAnalysis.ComplexConfig) →
  Array (Lean.TSyntax `tactic) → Mathlib.TacticAnalysis.TacticNode → config.ctx → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.Order.Interval.Finset.Defs
Finset.Iic_eq_Icc : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : OrderBot α] (a : α),
  Finset.Iic a = Finset.Icc ⊥ a
-- Mathlib.Data.Real.ConjExponents
ENNReal.HolderTriple.of_toReal : ∀ {p q r : ENNReal}, p.toReal.HolderTriple q.toReal r.toReal → p.HolderTriple q r
-- Mathlib.Tactic.CategoryTheory.IsoReassoc
Mathlib.Tactic.Reassoc.Iso.eq_whisker : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} {f g : X ≅ Y},
  f = g → ∀ {Z : C} (h : Y ≅ Z), f ≪≫ h = g ≪≫ h
-- Mathlib.Data.List.OfFn
List.ofFnRec_ofFn : ∀ {α : Type u} {C : List α → Sort u_1} (h : (n : ℕ) → (f : Fin n → α) → C (List.ofFn f)) {n : ℕ} (f : Fin n → α),
  List.ofFnRec h (List.ofFn f) = h n f
-- Mathlib.Order.Bounds.Image
IsLeast.image2 : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {f : α → β → γ}
  {s : Set α} {t : Set β} {a : α} {b : β},
  (∀ (b : β), Monotone (Function.swap f b)) →
    (∀ (a : α), Monotone (f a)) → IsLeast s a → IsLeast t b → IsLeast (Set.image2 f s t) (f a b)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
mulPosMono_iff_covariant_pos : ∀ {α : Type u_1} [inst : MulZeroClass α] [inst_1 : PartialOrder α],
  MulPosMono α ↔ CovariantClass { x // 0 < x } α (fun x y => y * ↑x) fun x1 x2 => x1 ≤ x2
-- Mathlib.Logic.Equiv.Option
Equiv.removeNone_symm : ∀ {α : Type u_1} {β : Type u_2} (e : Option α ≃ Option β), e.removeNone.symm = e.symm.removeNone
-- Mathlib.GroupTheory.Exponent
Monoid.orderOf_le_exponent : ∀ {G : Type u} [inst : Monoid G], Monoid.ExponentExists G → ∀ (g : G), orderOf g ≤ Monoid.exponent G
-- Lean.Data.Json.FromToJson.Basic
Lean.instToJsonArray : {α : Type u_1} → [Lean.ToJson α] → Lean.ToJson (Array α)
-- Mathlib.Data.Complex.Basic
Complex.div_ratCast_re : ∀ (z : ℂ) (x : ℚ), (z / ↑x).re = z.re / ↑x
-- Mathlib.GroupTheory.Congruence.Hom
/-- The diagram describing the universal property for quotients of
`AddMonoid`s commutes.  -/
AddCon.lift_coe : ∀ {M : Type u_1} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass P] {c : AddCon M} {f : M →+ P}
  (H : c ≤ AddCon.ker f) (x : M), (c.lift f H) ↑x = f x
-- Mathlib.Data.Finset.Sum
Finset.card_toLeft_le : ∀ {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)}, u.toLeft.card ≤ u.card
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingHom.mk.injEq : ∀ {α : Type u_6} {β : Type u_7} [inst : NonAssocSemiring α] [inst_1 : Preorder α] [inst_2 : NonAssocSemiring β]
  [inst_3 : Preorder β] (toRingHom : α →+* β) (monotone' : Monotone (↑↑toRingHom).toFun) (toRingHom_1 : α →+* β)
  (monotone'_1 : Monotone (↑↑toRingHom_1).toFun),
  ({ toRingHom := toRingHom, monotone' := monotone' } = { toRingHom := toRingHom_1, monotone' := monotone'_1 }) =
    (toRingHom = toRingHom_1)
-- Mathlib.GroupTheory.GroupAction.Quotient
MulAction.ofQuotientStabilizer.eq_1 : ∀ (G : Type u) {X : Type v} [inst : Group G] [inst_1 : MulAction G X] (x : X) (g : G ⧸ MulAction.stabilizer G x),
  MulAction.ofQuotientStabilizer G x g = Quotient.liftOn' g (fun x_1 => x_1 • x) ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- Image maps for composable commutative squares induce an image map in the composite square.  -/
CategoryTheory.Limits.imageMapComp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {f g : CategoryTheory.Arrow C} →
      [inst_1 : CategoryTheory.Limits.HasImage f.hom] →
        [inst_2 : CategoryTheory.Limits.HasImage g.hom] →
          (sq : f ⟶ g) →
            [CategoryTheory.Limits.HasImageMap sq] →
              {h : CategoryTheory.Arrow C} →
                [inst_4 : CategoryTheory.Limits.HasImage h.hom] →
                  (sq' : g ⟶ h) →
                    [CategoryTheory.Limits.HasImageMap sq'] →
                      CategoryTheory.Limits.ImageMap (CategoryTheory.CategoryStruct.comp sq sq')
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_add_uIcc : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] (a b c : α),
  (fun x => a + x) ⁻¹' Set.uIcc b c = Set.uIcc (b - a) (c - a)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.map_add_toArray_ric : ∀ {n k : ℕ}, Array.map (fun x => x + k) (*...=n).toArray = (k...=n + k).toArray
-- Std.Time.Zoned.TimeZone
Std.Time.TimeZone.Offset.ext : ∀ {x y : Std.Time.TimeZone.Offset}, x.second = y.second → x = y
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey_minKeyD_eq_minKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {fallback : α} {he : Std.Internal.List.containsKey (Std.Internal.List.minKeyD l fallback) l = true},
      Std.Internal.List.getKey (Std.Internal.List.minKeyD l fallback) l he = Std.Internal.List.minKey l ⋯
-- Mathlib.Algebra.GradedMonoid
/-- The commutative monoid `A 0` inherited from `R` in the presence of `SetLike.GradedMonoid A`.  -/
SetLike.GradeZero.instCommMonoid : {ι : Type u_1} →
  [inst : AddMonoid ι] →
    {R : Type u_4} →
      {S : Type u_5} →
        [inst_1 : SetLike S R] → [inst_2 : CommMonoid R] → {A : ι → S} → [SetLike.GradedMonoid A] → CommMonoid ↥(A 0)
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
Delone.DeloneSet.mem_carrier : ∀ {X : Type u_1} [inst : MetricSpace X] {D : Delone.DeloneSet X} {x : X}, x ∈ D.carrier ↔ x ∈ D
-- Mathlib.Algebra.Notation.Indicator
Set.comp_mulIndicator : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_3} [inst : One M] (h : M → β) (f : α → M) {s : Set α} {x : α}
  [inst_1 : DecidablePred fun x => x ∈ s], h (s.mulIndicator f x) = s.piecewise (h ∘ f) (Function.const α (h 1)) x
-- Mathlib.Analysis.SpecialFunctions.Stirling
/-- We have a bound for successive elements in the sequence `log (stirlingSeq k)`.  -/
Stirling.log_stirlingSeq_sdiff_le_geo_sum : ∀ (n : ℕ),
  Real.log (Stirling.stirlingSeq (n + 1)) - Real.log (Stirling.stirlingSeq (n + 2)) ≤
    (1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2)
-- Init.Data.UInt.Bitwise
UInt16.toUInt32_not : ∀ (a : UInt16), (~~~a).toUInt32 = ~~~a.toUInt32 % 65536