mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.toComon_obj_comon_comul : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : CategoryTheory.Comon (CategoryTheory.Mon C)),
  CategoryTheory.ComonObj.comul = CategoryTheory.ComonObj.comul.hom
-- Mathlib.CategoryTheory.Limits.Constructions.Filtered
CategoryTheory.Limits.CoproductsFromFiniteFiltered.finiteSubcoproductsCocone_ι_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type w}
  [inst_1 : CategoryTheory.Limits.HasFiniteCoproducts C] (f : α → C) [inst_2 : CategoryTheory.Limits.HasCoproduct f]
  (S : Finset (CategoryTheory.Discrete α)),
  (CategoryTheory.Limits.CoproductsFromFiniteFiltered.finiteSubcoproductsCocone f).ι.app S =
    CategoryTheory.Limits.Sigma.desc fun s => CategoryTheory.Limits.Sigma.ι f (↑s).as
-- Lean.Parser.Types
_private.Lean.Parser.Types.0.Lean.Parser.SyntaxStack.mk : Array Lean.Syntax → ℕ → Lean.Parser.SyntaxStack
-- Init.Data.SInt.Lemmas
Int32.toInt_ofNat' : ∀ {n : ℕ}, (Int32.ofNat n).toInt = (↑n).bmod Int32.size
-- Batteries.Data.List.Basic
List.swapTR.go.eq_4 : ∀ {α : Type u_1} (l : List α) (a : Array α) (a_1 : α) (xs : List α) (i : ℕ),
  List.swapTR.go l (a_1 :: xs) i.succ 0 a = a.toListAppend (Function.uncurry List.cons (xs.swapAt i a_1))
-- Mathlib.GroupTheory.Coprod.Basic
/-- `Coprod.lift` as an equivalence.  -/
Monoid.Coprod.liftEquiv : {M : Type u_1} →
  {N : Type u_2} →
    {P : Type u_3} →
      [inst : MulOneClass M] →
        [inst_1 : MulOneClass N] → [inst_2 : Monoid P] → (M →* P) × (N →* P) ≃ (Monoid.Coprod M N →* P)
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
AlgebraicGeometry.instIsClosedImmersionOfSubsingletonCarrierCarrierCommRingCatOfIsOver : ∀ {X Y : AlgebraicGeometry.Scheme} [Subsingleton ↥Y] [inst : X.Over Y] (f : Y ⟶ X)
  [AlgebraicGeometry.Scheme.Hom.IsOver f Y], AlgebraicGeometry.IsClosedImmersion f
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.of_near : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [IsAbsoluteValue abv] (f : ℕ → β) (g : CauSeq β abv),
  (∀ ε > 0, ∃ i, ∀ j ≥ i, abv (f j - ↑g j) < ε) → IsCauSeq abv f
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.rename_X : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] (f : σ → τ) (i : σ),
  (MvPolynomial.rename f) (MvPolynomial.X i) = MvPolynomial.X (f i)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Submodule
PresheafOfModules.Submodule.instMonoι : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M : PresheafOfModules R} (N : M.Submodule), CategoryTheory.Mono N.ι
-- Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup
Subgroup.subgroupOfContinuousMulEquivOfLe_apply : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] {H K : Subgroup G} (hHK : H ≤ K)
  (a : ↥(H.subgroupOf K)), (Subgroup.subgroupOfContinuousMulEquivOfLe hHK) a = (Subgroup.subgroupOfEquivOfLe hHK) a
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.brecOn_2.eq : ∀ {motive_1 : Lean.Elab.Term.Do.Code → Sort u}
  {motive_2 : Array (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) → Sort u}
  {motive_3 : Array (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) → Sort u}
  {motive_4 : List (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) → Sort u}
  {motive_5 : List (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) → Sort u}
  {motive_6 : Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code → Sort u}
  {motive_7 : Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code → Sort u}
  (t : Array (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code))
  (F_1 : (t : Lean.Elab.Term.Do.Code) → t.below → motive_1 t)
  (F_2 : (t : Array (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code)) → Lean.Elab.Term.Do.Code.below_1 t → motive_2 t)
  (F_3 : (t : Array (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code)) → Lean.Elab.Term.Do.Code.below_2 t → motive_3 t)
  (F_4 : (t : List (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code)) → Lean.Elab.Term.Do.Code.below_3 t → motive_4 t)
  (F_5 : (t : List (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code)) → Lean.Elab.Term.Do.Code.below_4 t → motive_5 t)
  (F_6 : (t : Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) → Lean.Elab.Term.Do.Code.below_5 t → motive_6 t)
  (F_7 : (t : Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) → Lean.Elab.Term.Do.Code.below_6 t → motive_7 t),
  Lean.Elab.Term.Do.Code.brecOn_2 t F_1 F_2 F_3 F_4 F_5 F_6 F_7 =
    F_3 t (Lean.Elab.Term.Do.Code.brecOn_2.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7).2
-- Mathlib.Algebra.Lie.SemiDirect
LieAlgebra.SemiDirectSum.mk.inj : ∀ {R : Type u_1} {inst : CommRing R} {K : Type u_2} {inst_1 : LieRing K} {inst_2 : LieAlgebra R K} {L : Type u_3}
  {inst_3 : LieRing L} {inst_4 : LieAlgebra R L} {x : L →ₗ⁅R⁆ LieDerivation R K K} {left : K} {right : L} {left_1 : K}
  {right_1 : L},
  { left := left, right := right } = { left := left_1, right := right_1 } → left = left_1 ∧ right = right_1
-- Lean.Parser.Command
Lean.Parser.Command.declModifiersT.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffOn.congr_mono : ∀ {𝕜 : 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 s₁ : Set E}
  {f f₁ : E → F} {n : WithTop ℕ∞}, ContDiffOn 𝕜 n f s → (∀ x ∈ s₁, f₁ x = f x) → s₁ ⊆ s → ContDiffOn 𝕜 n f₁ s₁
-- Mathlib.Algebra.Group.Pi.Basic
Pi.addGroup : {I : Type u} → {f : I → Type v₁} → [(i : I) → AddGroup (f i)] → AddGroup ((i : I) → f i)
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.toStream.match_1.eq_2 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → RBTree.RBNode.Stream α → Sort u_2) (c : RBTree.RBColor)
  (l : RBTree.RBNode α) (v : α) (r : RBTree.RBNode α) (acc : RBTree.RBNode.Stream α)
  (h_1 : (acc : RBTree.RBNode.Stream α) → motive RBTree.RBNode.nil acc)
  (h_2 :
    (c : RBTree.RBColor) →
      (l : RBTree.RBNode α) →
        (v : α) → (r : RBTree.RBNode α) → (acc : RBTree.RBNode.Stream α) → motive (RBTree.RBNode.node c l v r) acc),
  (match RBTree.RBNode.node c l v r, acc with
    | RBTree.RBNode.nil, acc => h_1 acc
    | RBTree.RBNode.node c l v r, acc => h_2 c l v r acc) =
    h_2 c l v r acc
-- Mathlib.RingTheory.SimpleModule.Isotypic
bot_lt_isotypicComponents : ∀ {R : Type u_2} {M : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {m : Submodule R M},
  m ∈ isotypicComponents R M → ⊥ < m
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Pi.optionEquivalence_counitIso : ∀ {J : Type w₁} (C' : Option J → Type u₁) [inst : (i : Option J) → CategoryTheory.Category.{v₁, u₁} (C' i)],
  (CategoryTheory.Pi.optionEquivalence C').counitIso =
    CategoryTheory.Iso.refl
      ((CategoryTheory.Functor.pi' fun i =>
            match i with
            | none => CategoryTheory.Prod.fst (C' none) ((j : J) → C' (some j))
            | some i =>
              (CategoryTheory.Prod.snd (C' none) ((j : J) → C' (some j))).comp
                (CategoryTheory.Pi.eval (fun j => C' (some j)) i)).comp
        ((CategoryTheory.Pi.eval C' none).prod'
          (CategoryTheory.Functor.pi' fun i => CategoryTheory.Pi.eval C' (some i))))
-- Mathlib.Order.CompleteLattice.Basic
iSup_iInf_le_iInf_iSup : ∀ {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [inst : CompleteLattice α] (f : ι → ι' → α),
  ⨆ i, ⨅ j, f i j ≤ ⨅ j, ⨆ i, f i j
-- Mathlib.NumberTheory.SelbergSieve
/-- `X * mainSum μ⁺` is the main term in the upper bound on `sifted_sum`.  -/
BoundingSieve.mainSum : {s : BoundingSieve} → (ℕ → ℝ) → ℝ
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.ofHom_id : ∀ {M : Type u} [inst : AddMonoid M],
  AddMonCat.ofHom (AddMonoidHom.id M) = CategoryTheory.CategoryStruct.id (AddMonCat.of M)
-- Mathlib.Data.Nat.Totient
Nat.card_units_zmod_lt_sub_one : ∀ {p : ℕ}, 1 < p → ∀ [inst : Fintype (ZMod p)ˣ], Fintype.card (ZMod p)ˣ ≤ p - 1
-- Init.Data.SInt.Lemmas
Int64.toInt_inj : ∀ {x y : Int64}, x.toInt = y.toInt ↔ x = y
-- Mathlib.RingTheory.AdicCompletion.AsTensorProduct
/-- `ofTensorProduct` as an equiv in the case of `M = R^ι` where `ι` is finite.  -/
AdicCompletion.ofTensorProductEquivOfPiFintype : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      (ι : Type u_4) →
        [Fintype ι] →
          [DecidableEq ι] → TensorProduct R (AdicCompletion I R) (ι → R) ≃ₗ[AdicCompletion I R] AdicCompletion I (ι → R)
-- Mathlib.CategoryTheory.CodiscreteCategory
/-- A function induces a functor between codiscrete categories.  -/
CategoryTheory.Codiscrete.functorOfFun : {A : Type u_1} →
  {B : Type u_2} → (A → B) → CategoryTheory.Functor (CategoryTheory.Codiscrete A) (CategoryTheory.Codiscrete B)
-- Mathlib.Analysis.Analytic.Composition
/-- The norm of `q.compAlongComposition p c` is controlled by the product of
the norms of the relevant bits of `q` and `p`.  -/
FormalMultilinearSeries.compAlongComposition_norm : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : ℕ} (q : FormalMultilinearSeries 𝕜 F G)
  (p : FormalMultilinearSeries 𝕜 E F) (c : Composition n),
  ‖q.compAlongComposition p c‖ ≤ ‖q c.length‖ * ∏ i, ‖p (c.blocksFun i)‖
-- Lean.Meta.DiscrTree.Types
Lean.Meta.DiscrTree.instInhabitedKey.default : Lean.Meta.DiscrTree.Key
-- Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
QuadraticMap.IsometryEquiv.mk : {R : Type u_2} →
  {M₁ : Type u_5} →
    {M₂ : Type u_6} →
      {N : Type u_9} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M₁] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : AddCommMonoid N] →
                [inst_4 : Module R M₁] →
                  [inst_5 : Module R M₂] →
                    [inst_6 : Module R N] →
                      {Q₁ : QuadraticMap R M₁ N} →
                        {Q₂ : QuadraticMap R M₂ N} →
                          (toLinearEquiv : M₁ ≃ₗ[R] M₂) →
                            (∀ (m : M₁), Q₂ ((↑toLinearEquiv).toFun m) = Q₁ m) → Q₁.IsometryEquiv Q₂
-- Mathlib.RingTheory.PrincipalIdealDomain
/-- `factors a` is a multiset of irreducible elements whose product is `a`, up to units  -/
PrincipalIdealRing.factors : {R : Type u} → [inst : CommRing R] → [IsDomain R] → [IsPrincipalIdealRing R] → R → Multiset R
-- Mathlib.Order.Disjoint
Codisjoint.eq_iff : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderTop α] {a b : α}, Codisjoint a b → (a = b ↔ a = ⊤ ∧ b = ⊤)
-- Lean.Meta.Tactic.Simp.Types
/-- A proof that `$e = $expr`, where the simplified expression is on the RHS.
If `none`, the proof is assumed to be `refl`.  -/
Lean.Meta.Simp.Result.proof? : Lean.Meta.Simp.Result → Option Lean.Expr
-- Mathlib.Algebra.MonoidAlgebra.Division
AddMonoidAlgebra.zero_divOf : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : AddCommMonoid G] [inst_2 : IsCancelAdd G] (g : G),
  AddMonoidAlgebra.divOf 0 g = 0
-- Mathlib.MeasureTheory.Measure.Haar.NormedSpace
MeasureTheory.Measure.integral_comp_inv_mul_left : ∀ {F : Type u_2} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] (g : ℝ → F) (a : ℝ),
  ∫ (x : ℝ), g (a⁻¹ * x) = |a| • ∫ (y : ℝ), g y
-- Mathlib.LinearAlgebra.Multilinear.Basis
/-- A basis for multilinear maps given a finite basis on each domain and a basis on the codomain.  -/
Basis.multilinearMap : {ι : Type u_1} →
  {R : Type u_2} →
    [inst : CommSemiring R] →
      {M : ι → Type u_3} →
        [inst_1 : (i : ι) → AddCommMonoid (M i)] →
          [inst_2 : (i : ι) → Module R (M i)] →
            {κ : ι → Type u_5} →
              ((i : ι) → Module.Basis (κ i) R (M i)) →
                {ι' : Type u_6} →
                  {N : Type u_7} →
                    [inst_3 : AddCommMonoid N] →
                      [inst_4 : Module R N] →
                        Module.Basis ι' R N →
                          [Finite ι] →
                            [∀ (i : ι), Finite (κ i)] → Module.Basis (((i : ι) → κ i) × ι') R (MultilinearMap R M N)
-- Init.Data.BitVec.Lemmas
BitVec.cpop_allOnes : ∀ {w : ℕ}, (BitVec.allOnes w).cpop = BitVec.ofNat w w
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.kernelSequenceCycles_exact : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.kernelSequenceCycles_exact._auto_1),
  (X.kernelSequenceCycles f g n₀ n₁ hn₁).Exact
-- Init.Meta.Defs
Lean.Syntax.decodeNatLitVal? : String → Option ℕ
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
_private.Mathlib.Algebra.Homology.Embedding.AreComplementary.0.ComplexShape.Embedding.AreComplementary.fromSum.match_1.splitter : {ι₁ : Type u_1} →
  {ι₂ : Type u_2} →
    (motive : ι₁ ⊕ ι₂ → Sort u_3) →
      (x : ι₁ ⊕ ι₂) → ((i₁ : ι₁) → motive (Sum.inl i₁)) → ((i₂ : ι₂) → motive (Sum.inr i₂)) → motive x
-- Mathlib.Topology.Algebra.FilterBasis
AddGroupFilterBasis.topology.eq_1 : ∀ {G : Type u} [inst : AddGroup G] (B : AddGroupFilterBasis G), B.topology = TopologicalSpace.mkOfNhds B.N
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.subtype_apply : ∀ {G : Type u_1} [inst : AddGroup G] {s : AddSubgroup G} (x : ↥s), s.subtype x = ↑x
-- Mathlib.Combinatorics.Digraph.Basic
Digraph.ext : ∀ {V : Type u_1} {x y : Digraph V}, x.Adj = y.Adj → x = y
-- Mathlib.Data.Real.Basic
Real.instInhabited : Inhabited ℝ
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- Eta-expanded form of `CircleIntegrable.continuousOn_mul`

---

If `g` is continuous on the circle `sphere c |R|` and `f` is circle integrable, then `g * f` is
circle integrable.
 -/
CircleIntegrable.fun_continuousOn_mul : ∀ {c : ℂ} {R : ℝ} {𝕜 : Type u_3} [inst : NormedRing 𝕜] {f g : ℂ → 𝕜},
  CircleIntegrable f c R → ContinuousOn g (Metric.sphere c |R|) → CircleIntegrable (fun i => g i * f i) c R
-- Mathlib.RingTheory.Bialgebra.TensorProduct
Coalgebra.Repr.mul_right : ∀ {R : Type u_1} {A : Type u_2} {ι : Type u_4} {κ : Type u_5} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Bialgebra R A] {a b : A} (ℛ₁ : Coalgebra.Repr R a ι) (ℛ₂ : Coalgebra.Repr R b κ) (a_1 : ι × κ),
  (ℛ₁.mul ℛ₂).right a_1 = ℛ₁.right a_1.1 * ℛ₂.right a_1.2
-- Mathlib.GroupTheory.PGroup
/-- If a p-group acts on `α` and the cardinality of `α` is a multiple
of `p`, and the action has one fixed point, then it has another fixed point.  -/
IsPGroup.exists_fixed_point_of_prime_dvd_card_of_fixed_point : ∀ {p : ℕ} {G : Type u_1} [inst : Group G],
  IsPGroup p G →
    ∀ [hp : Fact (Nat.Prime p)] (α : Type u_2) [inst_1 : MulAction G α] [Finite α],
      p ∣ Nat.card α → ∀ {a : α}, a ∈ MulAction.fixedPoints G α → ∃ b ∈ MulAction.fixedPoints G α, a ≠ b
-- Lean.DocString.Links
/-- Validates all links to the Lean reference manual in `docstring`, printing an error message if any
are invalid. Returns `true` if all links are valid.

This is intended to be used before saving a docstring that is later subject to rewriting with
`rewriteManualLinks`, in contexts where the imports needed to produce better error messages in
`validateDocComment` are not yet available.
 -/
Lean.validateBuiltinDocString : String → IO Unit
-- Mathlib.Order.GaloisConnection.Basic
GaloisInsertion.l_inf_u : ∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β]
  (gi : GaloisInsertion l u) (a b : β), l (u a ⊓ u b) = a ⊓ b
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.add_one_sub_one_of_two_dvd : ∀ {R : Type u} [inst : CommRing R] {x : R}, 2 ∣ x → IsCoprime (x + 1) (x - 1)
-- Mathlib.Data.Finset.SMulAntidiagonal
Set.IsPWO.vadd : ∀ {G : Type u_1} {P : Type u_2} [inst : Preorder G] [inst_1 : Preorder P] [inst_2 : VAdd G P] [IsOrderedVAdd G P]
  {s : Set G} {t : Set P}, s.IsPWO → t.IsPWO → (s +ᵥ t).IsPWO
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.IsMultiplicative.of_unop : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty Cᵒᵖ)
  [W.unop.IsMultiplicative], W.IsMultiplicative
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.A_diag : ∀ (n : ℕ), (CartanMatrix.A n).diag = 2
-- Init.Data.List.Zip
List.of_mem_zip : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} {l₁ : List α} {l₂ : List β}, (a, b) ∈ l₁.zip l₂ → a ∈ l₁ ∧ b ∈ l₂
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
CategoryTheory.Limits.PreservesLimitPair.iso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) (X Y : C) [inst_2 : CategoryTheory.Limits.HasBinaryProduct X Y]
  [inst_3 : CategoryTheory.Limits.HasBinaryProduct (G.obj X) (G.obj Y)]
  [inst_4 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair X Y) G],
  (CategoryTheory.Limits.PreservesLimitPair.iso G X Y).hom = CategoryTheory.Limits.prodComparison G X Y
-- Mathlib.Tactic.Linarith.Preprocessing
/-- `normalizeDenominatorsLHS h lhs` assumes that `h` is a proof of `lhs R 0`.
It creates a proof of `lhs' R 0`, where all numeric division in `lhs` has been cancelled.
 -/
Mathlib.Tactic.Linarith.normalizeDenominatorsLHS : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.tr.eq_8 : ∀ (fs : Turing.ToPartrec.Code) (k : Turing.PartrecToTM2.Cont'),
  Turing.PartrecToTM2.tr (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.cons₁ fs k)) =
    Turing.TM2.Stmt.goto fun x =>
      Turing.PartrecToTM2.move₂ (fun x => false) Turing.PartrecToTM2.K'.main Turing.PartrecToTM2.K'.aux
        (Turing.PartrecToTM2.move₂ (fun s => decide (s = Turing.PartrecToTM2.Γ'.consₗ)) Turing.PartrecToTM2.K'.stack
          Turing.PartrecToTM2.K'.main
          (Turing.PartrecToTM2.move₂ (fun x => false) Turing.PartrecToTM2.K'.aux Turing.PartrecToTM2.K'.stack
            (Turing.PartrecToTM2.trNormal fs k.cons₂)))
-- Mathlib.LinearAlgebra.RootSystem.Chain
RootPairing.chainBotCoeff_sub_chainTopCoeff : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : CharZero R] [inst_3 : IsDomain R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsCrystallographic] {i j : ι},
  LinearIndependent R ![P.root i, P.root j] →
    ↑(RootPairing.chainBotCoeff i j) - ↑(RootPairing.chainTopCoeff i j) = P.pairingIn ℤ j i
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.ofFinsupp_sub : ∀ {R : Type u} [inst : Ring R] {a b : AddMonoidAlgebra R ℕ},
  { toFinsupp := a - b } = { toFinsupp := a } - { toFinsupp := b }
-- Mathlib.Algebra.Colimit.Ring
Ring.DirectLimit.hom_ext_iff : ∀ {ι : Type u_1} [inst : Preorder ι] {G : ι → Type u_2} [inst_1 : (i : ι) → CommRing (G i)]
  {f : (i j : ι) → i ≤ j → G i → G j} {P : Type u_3} [inst_2 : CommRing P] {g₁ g₂ : Ring.DirectLimit G f →+* P},
  g₁ = g₂ ↔ ∀ (i : ι), g₁.comp (Ring.DirectLimit.of G f i) = g₂.comp (Ring.DirectLimit.of G f i)
-- Mathlib.Analysis.Normed.Order.Lattice
norm_abs_eq_norm : ∀ {α : Type u_1} [inst : NormedAddCommGroup α] [inst_1 : Lattice α] [HasSolidNorm α] [IsOrderedAddMonoid α] (a : α),
  ‖|a|‖ = ‖a‖
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- Eta-expanded form of `meromorphicNFOn_ball_comp_sub_const_iff_meromorphicNFOn_ball`

---

`MeromorphicNFOn` is invariant under translation, special case where the set is a ball.  -/
meromorphicNFOn_ball_fun_comp_sub_const_iff_meromorphicNFOn_ball : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {c : 𝕜} {R : ℝ},
  MeromorphicNFOn (fun x => f (x - c)) (Metric.ball c R) ↔ MeromorphicNFOn f (Metric.ball 0 R)
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.commute_iff : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → Mul (f i)] {x y : (i : I) → f i},
  Commute x y ↔ ∀ (i : I), Commute (x i) (y i)
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.hasCountableSeparatingOn_of_countablySeparated : ∀ {α : Type u_1} [inst : MeasurableSpace α] [h : MeasurableSpace.CountablySeparated α],
  HasCountableSeparatingOn α MeasurableSet Set.univ
-- Init.Data.Range.Polymorphic.Internal.SignedBitVec
_private.Init.Data.Range.Polymorphic.Internal.SignedBitVec.0.BitVec.Signed.instUpwardEnumerable : {n : ℕ} → Std.PRange.UpwardEnumerable (BitVec n)
-- Lean.Parser.Command
Lean.Parser.Command.nonrec.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Data.Set.Function
Set.SurjOn.mapsTo_compl : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β},
  Set.SurjOn f s t → Function.Injective f → Set.MapsTo f sᶜ tᶜ
-- Mathlib.Algebra.Group.Subgroup.Ker
AddSubgroup.comap_le_comap_of_surjective : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {f : G →+ N} {K L : AddSubgroup N},
  Function.Surjective ⇑f → (AddSubgroup.comap f K ≤ AddSubgroup.comap f L ↔ K ≤ L)
-- Lean.Elab.Binders
Lean.Elab.Term.elabHaveIDecl : Lean.Elab.Term.TermElab
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.inv.eq_def : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : (i : ι) → Group (G i)] (x x_1 : ι) (x_2 : Monoid.CoprodI.NeWord G x x_1),
  x_2.inv =
    match x, x_1, x_2 with
    | x, .(x), Monoid.CoprodI.NeWord.singleton x_3 h => Monoid.CoprodI.NeWord.singleton x_3⁻¹ ⋯
    | x, x_3, w₁.append h w₂ => w₂.inv.append ⋯ w₁.inv
-- Lean.Elab.BindersUtil
Lean.Elab.Term.clearInMatchAlt : Lean.TSyntax `Lean.Parser.Term.matchAlt → Array Lean.Ident → Lean.TSyntax `Lean.Parser.Term.matchAlt
-- Init.Data.Fin.Lemmas
Fin.rev_rev : ∀ {n : ℕ} (i : Fin n), i.rev.rev = i
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
AbsoluteValue.nonpos_iff : ∀ {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  (abv : AbsoluteValue R S) {x : R}, abv x ≤ 0 ↔ x = 0
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.zero_lt_getElem!_toArray_roo_iff : ∀ {m n i : ℕ}, 0 < (m<...n).toArray[i]! ↔ i < n - (m + 1)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get?_union_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₂ → (t₁ ∪ t₂).get? k = t₁.get? k
-- Mathlib.Data.EReal.Basic
/-- Extension for the `positivity` tactic: projection from `EReal` to `ℝ≥0∞`.

We show that `EReal.toENNReal x` is positive whenever `x` is positive,
and it is nonnegative otherwise.
We cannot deduce any corollaries from `x ≠ 0`, since `EReal.toENNReal x = 0` for `x < 0`.
 -/
Mathlib.Meta.Positivity.evalERealToENNReal : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Topology.Metrizable.Urysohn
/-- *Urysohn's metrization theorem* (Tychonoff's version):
a regular topological space with second countable topology `X` is metrizable,
i.e., there exists a pseudometric space structure that generates the same topology.  -/
TopologicalSpace.PseudoMetrizableSpace.of_regularSpace_secondCountableTopology : ∀ (X : Type u_1) [inst : TopologicalSpace X] [RegularSpace X] [SecondCountableTopology X],
  TopologicalSpace.PseudoMetrizableSpace X
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- An equalizer morphism is a monomorphism  -/
CategoryTheory.Limits.equalizer.ι_mono : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y}
  [inst_1 : CategoryTheory.Limits.HasEqualizer f g], CategoryTheory.Mono (CategoryTheory.Limits.equalizer.ι f g)
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
LinearIsometryEquiv.hasStrictFDerivAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E}
  (iso : E ≃ₗᵢ[𝕜] F), HasStrictFDerivAt (⇑iso) (↑↑iso) x