mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Simple
/-- A nonzero morphism `f` to a simple object is an epimorphism
(assuming `f` has an image, and `C` has equalizers).
 -/
CategoryTheory.epi_of_nonzero_to_simple : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasEqualizers C] {X Y : C} [CategoryTheory.Simple Y] {f : X ⟶ Y}
  [CategoryTheory.Limits.HasImage f], f ≠ 0 → CategoryTheory.Epi f
-- Mathlib.Tactic.FieldSimp
/-- Try to drop an expression `zpow' x r` from the beginning of a product. If `r ≠ 0` this of course
can't be done. If `r = 0`, then `zpow' x r` is equal to `x / x`, so it can be simplified to 1 (hence
dropped from the beginning of the product) if we can find a proof that `x ≠ 0`.  -/
Mathlib.Tactic.FieldSimp.qNF.tryClearZero : {v : Lean.Level} →
  {M : Q(Type v)} →
    ({u : Lean.Level} → (type : Q(Sort u)) → Lean.MetaM Q(«$type»)) →
      (iM : Q(CommGroupWithZero «$M»)) →
        (r : ℤ) →
          (x : Q(«$M»)) →
            (i : ℕ) →
              (l : Mathlib.Tactic.FieldSimp.qNF M) →
                Lean.MetaM
                  ((l' : Mathlib.Tactic.FieldSimp.qNF M) ×
                    have a := l'.toNF;
                    have a_1 := Mathlib.Tactic.FieldSimp.qNF.toNF (((r, x), i) :: l);
                    Q(«$a_1».eval = «$a».eval))
-- Mathlib.Topology.NhdsWithin
nhdsSetWithin_eq_principal_of_subset : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s t : Set α}, t ⊆ s → nhdsSetWithin s t = Filter.principal t
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.has_smallest_products_of_hasProducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C],
  CategoryTheory.Limits.HasProducts C
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast_filter_not_contains : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    ∀ {h₁ : Std.Internal.List.containsKey k (List.filter (fun p => !l₂.contains p.fst) l₁) = true}
      {h₂ : Std.Internal.List.containsKey k l₁ = true},
      Std.Internal.List.getValueCast k (List.filter (fun p => !l₂.contains p.fst) l₁) h₁ =
        Std.Internal.List.getValueCast k l₁ h₂
-- Mathlib.Tactic.Ring.Common
/-- The fallback case for exponentiating polynomials is to use `ExBase.toProd` to just build an
exponent expression.

* `x ^ e = x ^ e * 1 + 0`
 -/
Mathlib.Tactic.Ring.Common.evalPowAtom : {u : Lean.Level} →
  {α : Q(Type u)} →
    {bt : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} →
        Mathlib.Tactic.Ring.Common.RingCompute bt sα →
          {a : Q(«$α»)} →
            {b : Q(ℕ)} →
              Mathlib.Tactic.Ring.Common.ExBase bt sα a →
                Mathlib.Tactic.Ring.Common.ExProdNat b →
                  Mathlib.Tactic.Ring.Common.Result (Mathlib.Tactic.Ring.Common.ExSum bt sα) q(«$a» ^ «$b»)
-- Mathlib.CategoryTheory.Preadditive.Injective.InjectiveObject
CategoryTheory.InjectiveObject.instHasFiniteProducts : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C],
  CategoryTheory.Limits.HasFiniteProducts (CategoryTheory.InjectiveObject C)
-- Mathlib.Topology.Constructions.SumProd
isEmbedding_prodMkRight : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (x : X),
  Topology.IsEmbedding (Prod.mk x)
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.StructuredArrow.createsFiniteLimits : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {T : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} T] →
        {X : T} →
          {G : CategoryTheory.Functor A T} →
            [CategoryTheory.Limits.PreservesFiniteLimits G] →
              CategoryTheory.Limits.CreatesFiniteLimits (CategoryTheory.StructuredArrow.proj X G)
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.isIso_δ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C),
  CategoryTheory.Limits.IsZero S.L₀.X₂ → CategoryTheory.Limits.IsZero S.L₃.X₂ → CategoryTheory.IsIso S.δ
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapLeftComp_inv_app_left : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (R : CategoryTheory.Functor B T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {L₁ L₂ L₃ : CategoryTheory.Functor A T} [inst_5 : Q.RespectsIso] [inst_6 : W.RespectsIso] (l : L₁ ⟶ L₂) (l' : L₂ ⟶ L₃)
  (hl :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L₂ R P Q W),
      P (CategoryTheory.CategoryStruct.comp (l.app X.left) X.hom))
  (hl' :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L₃ R P Q W),
      P (CategoryTheory.CategoryStruct.comp (l'.app X.left) X.hom))
  (hll' :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L₃ R P Q W),
      P (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryStruct.comp l l').app X.left) X.hom))
  (X : CategoryTheory.MorphismProperty.Comma L₃ R P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapLeftComp R l l' hl hl' hll').inv.app X).left =
    CategoryTheory.CategoryStruct.id X.left
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char
Char.reduceLE : Lean.Meta.Simp.Simproc
-- Mathlib.Data.WSeq.Basic
_private.Mathlib.Data.WSeq.Basic.0.Stream'.WSeq.drop.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Batteries.Data.UnionFind.Basic
/-- Link two union-find nodes  -/
Batteries.UnionFind.linkAux : (self : Array Batteries.UFNode) → Fin self.size → Fin self.size → Array Batteries.UFNode
-- Mathlib.Analysis.Convolution
MeasureTheory.Integrable.convolution_integrand : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'}
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F]
  (L : E →L[𝕜] E' →L[𝕜] F) [inst_7 : MeasurableSpace G] {μ ν : MeasureTheory.Measure G} [inst_8 : AddGroup G]
  [MeasurableAdd₂ G] [MeasurableNeg G] [MeasureTheory.SFinite μ] [μ.IsAddRightInvariant] [MeasureTheory.SFinite ν],
  MeasureTheory.Integrable f ν →
    MeasureTheory.Integrable g μ → MeasureTheory.Integrable (fun p => (L (f p.2)) (g (p.1 - p.2))) (μ.prod ν)
-- Mathlib.Data.Finset.Lattice.Fold
/-- **Alias** of `Finset.le_inf_const`. -/
Finset.le_inf_const_le : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {s : Finset β} {a : α},
  a ≤ s.inf fun x => a
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.SeparatesPoints.separates : ∀ {α : Type u_3} {m : MeasurableSpace α} [self : MeasurableSpace.SeparatesPoints α] (x y : α),
  (∀ (s : Set α), MeasurableSet s → x ∈ s → y ∈ s) → x = y
-- Batteries.Data.List.Lemmas
List.findIdxNth_le_length : ∀ {α : Type u_1} {p : α → Bool} {n : ℕ} {xs : List α}, List.findIdxNth p xs n ≤ xs.length
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.map_fst_toArray_eq_keysArray : ∀ {α : Type u} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β},
  Array.map Prod.fst (Std.DTreeMap.Internal.Impl.Const.toArray t) = t.keysArray
-- Mathlib.Analysis.CStarAlgebra.Spectrum
StarSubalgebra.mem_spectrum_iff : ∀ {A : Type u_1} [inst : CStarAlgebra A] (S : StarSubalgebra ℂ A) [hS : IsClosed ↑S] {a : ↥S} {z : ℂ},
  z ∈ spectrum ℂ a ↔ z ∈ spectrum ℂ ↑a
-- Mathlib.Algebra.MvPolynomial.PDeriv
MvPolynomial.pderiv_monomial : ∀ {R : Type u} {σ : Type v} {a : R} {s : σ →₀ ℕ} [inst : CommSemiring R] {i : σ},
  (MvPolynomial.pderiv i) ((MvPolynomial.monomial s) a) = (MvPolynomial.monomial (s - fun₀ | i => 1)) (a * ↑(s i))
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.Decidable.isLongestMatchAtChain_iff_isLongestMatchAtChain_decide : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice} {pos pos' : s.Pos},
  String.Slice.Pattern.Model.IsLongestMatchAtChain p pos pos' ↔
    String.Slice.Pattern.Model.IsLongestMatchAtChain (fun x => decide (p x)) pos pos'
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.Grp.instMonObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {H : CategoryTheory.Grp C} → [CategoryTheory.IsCommMonObj H.X] → CategoryTheory.MonObj H
-- Mathlib.Topology.Sheaves.LocalPredicate
TopCat.LocalPredicate.toPrelocalPredicate : {X : TopCat} → {T : ↑X → Type u_1} → TopCat.LocalPredicate T → TopCat.PrelocalPredicate T
-- Mathlib.Topology.MetricSpace.CantorScheme
CantorScheme.Disjoint.eq_1 : ∀ {β : Type u_1} {α : Type u_2} (A : List β → Set α),
  CantorScheme.Disjoint A = ∀ (l : List β), Pairwise fun a b => Disjoint (A (a :: l)) (A (b :: l))
-- Init.System.IOError
IO.Error.unsupportedOperation.injEq : ∀ (osCode : UInt32) (details : String) (osCode_1 : UInt32) (details_1 : String),
  (IO.Error.unsupportedOperation osCode details = IO.Error.unsupportedOperation osCode_1 details_1) =
    (osCode = osCode_1 ∧ details = details_1)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_eq_default_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {a : α}, t.contains a = false → t.getKey! a = default
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.constMinEntry!_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited (α × β)],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → Std.DTreeMap.Raw.Const.minEntry! t₁ = Std.DTreeMap.Raw.Const.minEntry! t₂
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.trans : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Std.TreeMap α β cmp},
  t₁.Equiv t₂ → t₂.Equiv t₃ → t₁.Equiv t₃
-- Mathlib.Order.DirectedInverseSystem
/-- Restrict a partial family of bijections to a smaller set.  -/
InverseSystem.PEquivOn.restrict : {ι : Type u_6} →
  {F : ι → Type u_7} →
    {X : ι → Type u_8} →
      [inst : LinearOrder ι] →
        {f : ⦃i j : ι⦄ → i ≤ j → F j → F i} →
          [inst_1 : SuccOrder ι] →
            {equivSucc : ⦃i : ι⦄ → ¬IsMax i → F (Order.succ i) ≃ F i × X i} →
              {s t : Set ι} → InverseSystem.PEquivOn f equivSucc t → s ⊆ t → InverseSystem.PEquivOn f equivSucc s
-- Mathlib.Analysis.Calculus.FDeriv.Comp
DifferentiableAt.comp : ∀ {𝕜 : 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] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} (x : E) {g : F → G},
  DifferentiableAt 𝕜 g (f x) → DifferentiableAt 𝕜 f x → DifferentiableAt 𝕜 (g ∘ f) x
-- Mathlib.MeasureTheory.Integral.TorusIntegral
torusIntegral_dim0 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] (f : (Fin 0 → ℂ) → E)
  (c : Fin 0 → ℂ) (R : Fin 0 → ℝ), (∯ (x : Fin 0 → ℂ) in T(c, R), f x) = f c
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Precoverage.instPullbacksPreservedByOfPreservesLimitsOfShapeWalkingCospan : ∀ {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] (J : CategoryTheory.Precoverage C) (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F], J.PullbacksPreservedBy F
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt
CFC.conjSqrt_of_not_nonneg : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] [inst_8 : SeparatelyContinuousMul A] {c a : A}, ¬0 ≤ c → (CFC.conjSqrt c) a = 0
-- Lean.Parser.Command
Lean.Parser.Command.namedPrio : Lean.Parser.Parser
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.Hom.id.eq_1 : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Extension R S),
  Algebra.Extension.Hom.id P = { toRingHom := RingHom.id P.Ring, toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ }
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.MemLp.toLp_sub : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {f g : α → E} (hf : MeasureTheory.MemLp f p μ) (hg : MeasureTheory.MemLp g p μ),
  MeasureTheory.MemLp.toLp (f - g) ⋯ = MeasureTheory.MemLp.toLp f hf - MeasureTheory.MemLp.toLp g hg
-- Lean.Parser.Command
Lean.Parser.Command.derivingClass.formatter : Lean.PrettyPrinter.Formatter
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.forIn_eq : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] {m : Type x → Type x'} [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α Id m] [hl : Std.LawfulIteratorLoop α Id m] {γ : Type x} {it : Std.Iter β}
  {init : γ} {f : β → γ → m (ForInStep γ)},
  forIn it init f =
    Std.IterM.DefaultConsumers.forIn' (fun x x_1 f c => f c.run) γ (fun x x_1 x_2 => True) it.toIterM init
      it.toIterM.IsPlausibleIndirectOutput ⋯ fun out x acc => do
      let __do_lift ← f out acc
      pure ⟨__do_lift, trivial⟩
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback.hp₁_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S}
  (self : CategoryTheory.Limits.ChosenPullback f₁ f₂) {Z : C} (h : S ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.p₁ (CategoryTheory.CategoryStruct.comp f₁ h) =
    CategoryTheory.CategoryStruct.comp self.p h
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.of.inj : ∀ {C : Type u} {a a_1 : C}, CategoryTheory.WithTerminal.of a = CategoryTheory.WithTerminal.of a_1 → a = a_1
-- Init.Data.Array.Basic
/-- Creates an array by applying `f` to each potential index in order, starting at `0`.

Examples:
* `Array.ofFn (n := 3) toString = #["0", "1", "2"]`
* `Array.ofFn (fun i => #["red", "green", "blue"].get i.val i.isLt) = #["red", "green", "blue"]`
 -/
Array.ofFn : {α : Type u} → {n : ℕ} → (Fin n → α) → Array α
-- Mathlib.Tactic.TFAE
Mathlib.Tactic.TFAE.Parser.impArrow.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Topology.Order.OrderClosed
instClosedIciTopologyOrderDual : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Preorder α] [ClosedIicTopology α], ClosedIciTopology αᵒᵈ
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
WithSeminorms.continuous_normedSpace_rng : ∀ {𝕝 : Type u_4} {𝕝₂ : Type u_5} {E : Type u_6} {ι : Type u_9} [inst : AddCommGroup E] [inst_1 : NormedField 𝕝]
  [inst_2 : Module 𝕝 E] [inst_3 : NormedField 𝕝₂] {τ₁₂ : 𝕝 →+* 𝕝₂} [inst_4 : RingHomIsometric τ₁₂] (F : Type u_11)
  [inst_5 : SeminormedAddCommGroup F] [inst_6 : NormedSpace 𝕝₂ F] [inst_7 : TopologicalSpace E] {p : ι → Seminorm 𝕝 E},
  WithSeminorms p → ∀ (f : E →ₛₗ[τ₁₂] F), (∃ s C, (normSeminorm 𝕝₂ F).comp f ≤ C • s.sup p) → Continuous ⇑f
-- Lean.Message
Lean.Message.toString : Lean.Message → optParam Bool false → BaseIO String
-- Mathlib.Order.RelIso.Set
/-- The relation embedding from the inherited relation on a subset.  -/
Subrel.relEmbedding : {α : Type u_1} → (r : α → α → Prop) → (p : α → Prop) → Subrel r p ↪r r
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.size_filter_eq_size_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  {f : α → β → Bool},
  t.WF →
    ((Std.DTreeMap.Raw.filter f t).size = t.size ↔
      ∀ (a : α) (h : a ∈ t), f (t.getKey a h) (Std.DTreeMap.Raw.Const.get t a h) = true)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.cyclesMk₀_eq : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (x : ↑A),
  groupHomology.cyclesMk 0 0 groupHomology.cyclesMk₀_eq._proof_1
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.chainsIso₀ A).inv) x) ⋯ =
    (CategoryTheory.ConcreteCategory.hom (groupHomology.cyclesIso₀ A).inv) x
-- Mathlib.Algebra.Pointwise.Stabilizer
AddAction.add_stabilizer_self : ∀ {G : Type u_1} [inst : AddCommGroup G] (s : Set G), s + ↑(AddAction.stabilizer G s) = s
-- Mathlib.NumberTheory.NumberField.Basic
Rat.ringOfIntegersEquiv_symm_apply_coe : ∀ (x : ℤ), ↑(Rat.ringOfIntegersEquiv.symm x) = ↑x
-- Init.Data.Vector.Lemmas
Vector.replace_singleton : ∀ {α : Type u_1} [inst : BEq α] {a b c : α}, #v[a].replace b c = #v[if (a == b) = true then c else a]
-- Mathlib.CategoryTheory.Sites.CoverLifting
CategoryTheory.Functor.sheafAdjunctionCocontinuous_unit_app_hom : ∀ {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] (G : CategoryTheory.Functor C D) (A : Type w)
  [inst_2 : CategoryTheory.Category.{w', w} A] (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) [inst_3 : G.IsCocontinuous J K]
  [inst_4 : ∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] [inst_5 : G.IsContinuous J K]
  (F : CategoryTheory.Sheaf K A),
  ((G.sheafAdjunctionCocontinuous A J K).unit.app F).hom = (G.op.ranAdjunction A).unit.app F.obj
-- Mathlib.Data.ENNReal.Basic
ENNReal.max_zero_right : ∀ {a : ENNReal}, max a 0 = a
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.contains_unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List α}
  {k : α}, (Std.ExtDTreeMap.Const.unitOfList l cmp).contains k = l.contains k
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.path_injective_of_ne : ∀ {x y : Circle}, x ≠ y → Function.Injective ⇑(x.path y)
-- Init.Data.UInt.Basic
instSubUInt16 : Sub UInt16
-- Init.Data.String.Slice
String.Slice.RevSplitIterator.operating : {σ : String.Slice → Type} →
  {ρ : Type} →
    {pat : ρ} →
      {s : String.Slice} →
        [inst : String.Slice.Pattern.ToBackwardSearcher pat σ] →
          s.Pos → Std.Iter (String.Slice.Pattern.SearchStep s) → String.Slice.RevSplitIterator pat s
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.Quotient.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {r : HomRel C} [inst_1 : SizeOf C]
  [inst_2 : ⦃X Y : C⦄ → (a a_1 : X ⟶ Y) → SizeOf (r a a_1)] (as : C), sizeOf { as := as } = 1 + sizeOf as
-- Mathlib.Algebra.Group.Prod
AddMonoidHom.inl_apply : ∀ {M : Type u_3} {N : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (x : M),
  (AddMonoidHom.inl M N) x = (x, 0)
-- Mathlib.Algebra.Category.Semigrp.Basic
AddSemigrp.hom_id : ∀ {X : AddSemigrp}, AddSemigrp.Hom.hom (CategoryTheory.CategoryStruct.id X) = AddHom.id ↑X
-- Mathlib.MeasureTheory.Integral.DominatedConvergence
/-- Interval integrals commute with countable sums, when the supremum norms are summable (a
special case of the dominated convergence theorem).  -/
intervalIntegral.hasSum_intervalIntegral_of_summable_norm : ∀ {ι : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} [Countable ι]
  {f : ι → C(ℝ, E)},
  (Summable fun i => ‖ContinuousMap.restrict (↑{ carrier := Set.uIcc a b, isCompact' := ⋯ }) (f i)‖) →
    HasSum (fun i => ∫ (x : ℝ) in a..b, (f i) x) (∫ (x : ℝ) in a..b, ∑' (i : ι), (f i) x)
-- Mathlib.Algebra.MvPolynomial.Supported
MvPolynomial.supported_univ : ∀ {σ : Type u_1} {R : Type u} [inst : CommSemiring R], MvPolynomial.supported R Set.univ = ⊤
-- Lean.Parser.Module.Syntax
Lean.Parser.Module.module.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.List.Find
List.findIdx?_eq_map_findFinIdx?_val : ∀ {α : Type u_1} {xs : List α} {p : α → Bool}, List.findIdx? p xs = Option.map (fun x => ↑x) (List.findFinIdx? p xs)
-- Mathlib.Logic.Equiv.Defs
/-- If `α` has a unique term, then the type of function `α → β` is equivalent to `β`.  -/
Equiv.funUnique : (α : Sort u) → (β : Sort u_1) → [Unique α] → (α → β) ≃ β
-- Mathlib.Algebra.Order.Group.Lattice
inf_mul : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] [MulRightMono α] (a b c : α), (a ⊓ b) * c = a * c ⊓ b * c
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.isEmpty_takeEndWhile_dropEndWhile : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s : String}, ((s.dropEndWhile pat).takeEndWhile pat).isEmpty = true
-- Mathlib.CategoryTheory.Elements
/-- The equivalence `F.elementsᵒᵖ ≌ (yoneda, F)` is compatible with the forgetful functors.  -/
CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalenceInverseπ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor Cᵒᵖ (Type v)) →
      (CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence F).inverse.comp
          (CategoryTheory.CategoryOfElements.π F).leftOp ≅
        CategoryTheory.CostructuredArrow.proj CategoryTheory.yoneda F
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- If `x` is a letter and `w` is a word such that `xw` reduces to the empty word, then `w` reduces
to `x⁻¹`  -/
FreeGroup.Red.cons_nil_iff_singleton : ∀ {α : Type u} {L : List (α × Bool)} {x : α} {b : Bool}, FreeGroup.Red ((x, b) :: L) [] ↔ FreeGroup.Red L [(x, !b)]
-- Init.Data.Order.Ord
/-- A typeclass for ordered types for which `compare a a = .eq` for all `a`.  -/
Std.ReflOrd : (α : Type u) → [Ord α] → Prop
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.unop_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) (X : C), F.unop.obj X = Opposite.unop (F.obj (Opposite.op X))
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.CheckCoverageResult.ok.sizeOf_spec : sizeOf Lean.Meta.Grind.CheckCoverageResult.ok = 1
-- Mathlib.Data.Multiset.ZeroCons
Multiset.cons_zero : ∀ {α : Type u_1} (a : α), a ::ₘ 0 = {a}
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.copy_p : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData) {Q' H' : C} (eQ : Q' ≅ h.Q) (eH : H' ≅ h.H),
  (h.copy eQ eH).p = CategoryTheory.CategoryStruct.comp h.p eQ.inv
-- Mathlib.Topology.Sheaves.Alexandrov
Alexandrov.projSup_obj : ∀ {X : Type v} [inst : TopologicalSpace X] [inst_1 : Preorder X] [inst_2 : Topology.IsUpperSet X] {ι : Type v}
  (Us : ι → TopologicalSpace.Opens X)
  (f : CategoryTheory.StructuredArrow (Opposite.op (iSup Us)) (Alexandrov.principals X)),
  (Alexandrov.projSup Us).obj f = Opposite.op { obj := Alexandrov.principalOpen f.right, property := ⋯ }
-- Mathlib.CategoryTheory.Abelian.Basic
/-- the image is a kernel  -/
CategoryTheory.Abelian.AbelianStruct.imageIsKernel : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          (self : CategoryTheory.Abelian.AbelianStruct f) →
            CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι self.imageι ⋯)
-- Mathlib.Order.BoundedOrder.Monotone
StrictMono.maximal_preimage_top : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] [inst_2 : OrderTop β] {f : α → β},
  StrictMono f → ∀ {a : α}, f a = ⊤ → ∀ (x : α), x ≤ a