mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
CategoryTheory.Limits.kernel_map_comp_preserves_kernel_iso_inv_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (G : CategoryTheory.Functor C D) [inst_4 : G.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y)
  [inst_5 : CategoryTheory.Limits.HasKernel f] [inst_6 : CategoryTheory.Limits.HasKernel (G.map f)]
  [inst_7 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) G] {X' Y' : C} (g : X' ⟶ Y')
  [inst_8 : CategoryTheory.Limits.HasKernel g] [inst_9 : CategoryTheory.Limits.HasKernel (G.map g)]
  [inst_10 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair g 0) G] (p : X ⟶ X') (q : Y ⟶ Y')
  (hpq : CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p g) {Z : D}
  (h : G.obj (CategoryTheory.Limits.kernel g) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesKernel.iso G g).inv h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesKernel.iso G f).inv
      (CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.kernel.map f g p q hpq)) h)
-- Mathlib.Data.Nat.Count
Nat.count_mono_left : ∀ {p : ℕ → Prop} [inst : DecidablePred p] {q : ℕ → Prop} [inst_1 : DecidablePred q] {n : ℕ},
  (∀ k < n, p k → q k) → Nat.count p n ≤ Nat.count q n
-- Lean.ReducibilityAttrs
_private.Lean.ReducibilityAttrs.0.Lean.addAttr : Lean.ReducibilityStatus → Lean.Name → Lean.Syntax → Lean.AttributeKind → Lean.AttrM Unit
-- Lean.Elab.PreDefinition.FixedParams
Lean.Elab.FixedParamPerm.numFixed : Lean.Elab.FixedParamPerm → ℕ
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Affine.Simplex.centroid.eq_1 : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} (t : Affine.Simplex k P n), t.centroid = Finset.centroid k Finset.univ t.points
-- Mathlib.GroupTheory.GroupAction.ConjAct
ConjAct.toConjAct_one : ∀ {G : Type u_3} [inst : DivInvMonoid G], ConjAct.toConjAct 1 = 1
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_list_count : ∀ {M : Type u_4} [inst : CommMonoid M] [inst_1 : DecidableEq M] (s : List M),
  s.prod = ∏ m ∈ s.toFinset, m ^ List.count m s
-- Lean.Elab.Tactic.Conv.Basic
Lean.Elab.Tactic.Conv.evalConv : Lean.Elab.Tactic.Tactic
-- Lean.Meta.Tactic.Grind.PropagateInj
_private.Lean.Meta.Tactic.Grind.PropagateInj.0.Lean.Meta.Grind.propagateInj : Lean.Meta.Grind.Propagator
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.instSupSet : {α : Type u_1} → [inst : LE α] → SupSet (LowerSet α)
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.IsNNRat.mk : ∀ {α : Type u} [inst : Semiring α] {a : α} {num denom : ℕ} (inv : Invertible ↑denom),
  a = ↑num * ⅟↑denom → Mathlib.Meta.NormNum.IsNNRat a num denom
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- If `C` has strong epi mono factorisations, then the image is unique up to isomorphism, in that if
`f` factors as a strong epi followed by a mono, this factorisation is essentially the image
factorisation.
 -/
CategoryTheory.Limits.image.isoStrongEpiMono : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasStrongEpiMonoFactorisations C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          {I' : C} →
            (e : X ⟶ I') →
              (m : I' ⟶ Y) →
                CategoryTheory.CategoryStruct.comp e m = f →
                  [CategoryTheory.StrongEpi e] → [CategoryTheory.Mono m] → I' ≅ CategoryTheory.Limits.image f
-- Mathlib.Algebra.Group.Action.Defs
IsLeftCancelSMul.mk : ∀ {G : Type u_9} {P : Type u_10} [inst : SMul G P], (∀ (a : G) (b c : P), a • b = a • c → b = c) → IsLeftCancelSMul G P
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
CochainComplex.HomComplex.CohomologyClass.descAddMonoidHom_cohomologyClass : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ} {G : Type u_2} [inst_2 : AddCommGroup G]
  (f : CochainComplex.HomComplex.Cocycle K L n →+ G) (hf : CochainComplex.HomComplex.coboundaries K L n ≤ f.ker)
  (x : CochainComplex.HomComplex.Cocycle K L n),
  (CochainComplex.HomComplex.CohomologyClass.descAddMonoidHom f hf) (CochainComplex.HomComplex.CohomologyClass.mk x) =
    f x
-- Mathlib.Algebra.Homology.Embedding.TruncGE
HomologicalComplex.restrictionToTruncGE'_naturality : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K L : HomologicalComplex C c'} (φ : K ⟶ L) (e : c.Embedding c') [inst_2 : e.IsTruncGE]
  [inst_3 : ∀ (i' : ι'), K.HasHomology i'] [inst_4 : ∀ (i' : ι'), L.HasHomology i'],
  CategoryTheory.CategoryStruct.comp (K.restrictionToTruncGE' e) (HomologicalComplex.truncGE'Map φ e) =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.restrictionMap φ e) (L.restrictionToTruncGE' e)
-- Mathlib.Analysis.Normed.Field.UnitBall
Subsemigroup.unitBall.eq_1 : ∀ (𝕜 : Type u_2) [inst : NonUnitalSeminormedRing 𝕜],
  Subsemigroup.unitBall 𝕜 = { carrier := Metric.ball 0 1, mul_mem' := ⋯ }
-- Lean.Elab.App
/-- Record a valid named argument for the function.  -/
_private.Lean.Elab.App.0.Lean.Elab.Term.ElabAppArgs.pushFoundNamedArg : Lean.Name → Lean.Elab.Term.ElabAppArgs.M Unit
-- Mathlib.Algebra.Homology.ShortComplex.Linear
CategoryTheory.ShortComplex.LeftHomologyMapData.smul_φH : ∀ {R : Type u_1} {C : Type u_2} [inst : Semiring R] [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C] {S₁ S₂ : CategoryTheory.ShortComplex C}
  {φ : S₁ ⟶ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData}
  (γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂) (a : R), (γ.smul a).φH = a • γ.φH
-- Mathlib.Analysis.Analytic.Constructions
AnalyticOnNhd.add : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F} {s : Set E},
  AnalyticOnNhd 𝕜 f s → AnalyticOnNhd 𝕜 g s → AnalyticOnNhd 𝕜 (f + g) s
-- Lean.ImportingFlag
/-- Execute `x` with "importing" flag turned on.
When the "importing" flag is set to true, we allow user-extensions defined with
the `initialize` command to update global references.
IMPORTANT: There is no semaphore controlling the access to these global references.
We assume these global references are updated by a single execution thread.
This is true in the Lean frontend where we process the `import` commands at the beginning
of the execution only. Users must make sure that when `importModules` is used, there is only
one execution thread accessing the global references.
 -/
Lean.withImporting : {α : Type} → IO α → IO α
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.sUnion_edgeSet_eq_vertexSet_iff_all_vertex_not_isolated : ∀ {α : Type u_1} {H : Hypergraph α}, ⋃₀ H.edgeSet = H.vertexSet ↔ ∀ x ∈ H.vertexSet, ¬H.IsIsolated x
-- Mathlib.Topology.Semicontinuity.Basic
ContinuousAt.comp_upperSemicontinuousWithinAt_antitone : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {x : α} {γ : Type u_4} [inst_1 : LinearOrder γ]
  [inst_2 : TopologicalSpace γ] [OrderTopology γ] {δ : Type u_5} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ]
  [OrderTopology δ] {g : γ → δ} {f : α → γ},
  ContinuousAt g (f x) → UpperSemicontinuousWithinAt f s x → Antitone g → LowerSemicontinuousWithinAt (g ∘ f) s x
-- Mathlib.Order.Filter.Defs
Filter.instTop : {α : Type u_1} → Top (Filter α)
-- Mathlib.CategoryTheory.Adhesive.Basic
CategoryTheory.Adhesive.mono_of_isPushout_of_mono_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z}
  [CategoryTheory.Adhesive C], CategoryTheory.IsPushout f g h i → ∀ [CategoryTheory.Mono g], CategoryTheory.Mono h
-- Lean.Elab.PreDefinition.FixedParams
Lean.Elab.FixedParams.Info.format : Lean.Elab.FixedParams.Info → Std.Format
-- Init.Data.String.Length
String.length_push : ∀ {s : String} (c : Char), (s.push c).length = s.length + 1
-- Mathlib.NumberTheory.Padics.MahlerBasis
mahler_apply : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (k : ℕ) (x : ℤ_[p]), (mahler k) x = Ring.choose x k
-- Mathlib.Combinatorics.Matroid.Closure
/-- **Alias** of `Matroid.Indep.closure_sdiff_singleton_ssubset`. -/
Matroid.Indep.closure_diff_singleton_ssubset : ∀ {α : Type u_2} {M : Matroid α} {e : α} {I : Set α}, M.Indep I → e ∈ I → M.closure (I \ {e}) ⊂ M.closure I
-- Std.Http.Internal.IndexMultiMap
/-- Converts the multimap to an array of key-value pairs (flattened).
 -/
Std.Internal.IndexMultiMap.toArray : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Std.Internal.IndexMultiMap α β → Array (α × β)
-- Mathlib.Data.Sym.Basic
Sym.map_id : ∀ {α : Type u_3} {n : ℕ} (s : Sym α n), Sym.map id s = s
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instNonUnitalSemiringOfMulOpposite.eq_1 : ∀ {M : Type u_1} [inst : NonUnitalSemiring Mᵐᵒᵖ], DomMulAct.instNonUnitalSemiringOfMulOpposite = inst
-- Mathlib.RingTheory.RingHom.Etale
RingHom.Etale.containsIdentities : RingHom.ContainsIdentities fun {R S} [CommRing R] [CommRing S] => RingHom.Etale
-- Mathlib.Topology.Spectral.Prespectral
LowerSet.mk.congr_simp : ∀ {α : Type u_1} [inst : LE α] (carrier carrier_1 : Set α) (e_carrier : carrier = carrier_1)
  (lower' : IsLowerSet carrier), { carrier := carrier, lower' := lower' } = { carrier := carrier_1, lower' := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PushoutObjObj.ofIsInitialRight_inr : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₂ Y₂ : C₂} (f₂ : X₂ ⟶ Y₂)
  [inst_3 : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (F.obj X₁)]
  [inst_4 : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (F.obj Y₁)]
  (h : CategoryTheory.Limits.IsInitial X₂),
  (CategoryTheory.Functor.PushoutObjObj.ofIsInitialRight F f₁ f₂ h).inr =
    CategoryTheory.CategoryStruct.id ((F.obj X₁).obj Y₂)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey!_erase_le_maxKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α}, t.erase k ≠ ∅ → (cmp (t.erase k).maxKey! t.maxKey!).isLE = true
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHom.mk'_apply : ∀ {M : Type u_4} {G : Type u_7} [inst : Group G] [inst_1 : MulOneClass M] (f : M → G)
  (map_mul : ∀ (a b : M), f (a * b) = f a * f b), ⇑(MonoidHom.mk' f map_mul) = f
-- Mathlib.FieldTheory.IsRealClosed.Basic
IsRealClosed.toIsSemireal : ∀ {R : Type u_1} {inst : Field R} [self : IsRealClosed R], IsSemireal R
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.instUniqueOfIsEmpty : {α : Type u_2} → [inst : TopologicalSpace α] → [IsEmpty α] → Unique (TopologicalSpace.Opens α)
-- Lean.Meta.Tactic.Grind.Intro
_private.Lean.Meta.Tactic.Grind.Intro.0.Lean.Meta.Grind.IntroResult.newDepHyp.injEq : ∀ (goal goal_1 : Lean.Meta.Grind.Goal),
  (Lean.Meta.Grind.IntroResult.newDepHyp✝ goal = Lean.Meta.Grind.IntroResult.newDepHyp✝ goal_1) = (goal = goal_1)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.whiskerLeft_left_fst_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X : C}
  {R S T : CategoryTheory.Over X} (f : S ⟶ T) {Z : C} (h : R.left ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R f))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst R.hom T.hom) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst R.hom S.hom) h
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryGT?.go.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Ord α] (k : α) (best : Option (α × β)),
  Std.DTreeMap.Internal.Impl.Const.getEntryGT?.go k best Std.DTreeMap.Internal.Impl.leaf = best
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.map_comap_le : ∀ {V : Type u_1} {W : Type u_2} (f : V ↪ W) (G : SimpleGraph W), SimpleGraph.map (⇑f) (SimpleGraph.comap (⇑f) G) ≤ G
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- The map `f ↦ (x ↦ B (f x) (g x))` as a continuous `𝕜`-linear map on Schwartz space,
where `B` is a continuous `𝕜`-linear map and `g` is a function of temperate growth.  -/
SchwartzMap.bilinLeftCLM : {𝕜 : Type u_2} →
  {D : Type u_4} →
    {E : Type u_5} →
      {F : Type u_6} →
        {G : Type u_7} →
          [inst : NormedAddCommGroup E] →
            [inst_1 : NormedSpace ℝ E] →
              [inst_2 : NormedAddCommGroup F] →
                [inst_3 : NormedSpace ℝ F] →
                  [inst_4 : NontriviallyNormedField 𝕜] →
                    [inst_5 : NormedAlgebra ℝ 𝕜] →
                      [inst_6 : NormedAddCommGroup D] →
                        [inst_7 : NormedSpace ℝ D] →
                          [inst_8 : NormedAddCommGroup G] →
                            [inst_9 : NormedSpace ℝ G] →
                              [inst_10 : NormedSpace 𝕜 F] →
                                [inst_11 : NormedSpace 𝕜 E] →
                                  [inst_12 : NormedSpace 𝕜 G] →
                                    (E →L[𝕜] F →L[𝕜] G) →
                                      {g : D → F} →
                                        Function.HasTemperateGrowth g → SchwartzMap D E →L[𝕜] SchwartzMap D G
-- Mathlib.ModelTheory.Definability
Set.definable_iff_exists_formula_sum : ∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u₁} {s : Set (α → M)},
  A.Definable L s ↔ ∃ φ, s = {v | φ.Realize (Sum.elim Subtype.val v)}
-- Mathlib.Analysis.InnerProductSpace.Rayleigh
IsSelfAdjoint.eq_smul_self_of_isLocalExtrOn_real : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] [inst_2 : CompleteSpace F]
  {T : F →L[ℝ] F},
  IsSelfAdjoint T →
    ∀ {x₀ : F}, IsLocalExtrOn T.reApplyInnerSelf (Metric.sphere 0 ‖x₀‖) x₀ → T x₀ = T.rayleighQuotient x₀ • x₀
-- Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
/-- Functions are harmonic iff their compositions with continuous linear equivalences are harmonic.
 -/
InnerProductSpace.harmonicOnNhd_comp_CLE_iff : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {G : Type u_3}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace ℝ G] {f : E → F} {s : Set E} (l : F ≃L[ℝ] G),
  InnerProductSpace.HarmonicOnNhd (⇑l ∘ f) s ↔ InnerProductSpace.HarmonicOnNhd f s
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.single_neg : ∀ {ι : Type u} [inst : DecidableEq ι] {β : ι → Type v} [inst_1 : (i : ι) → AddGroup (β i)] (i : ι) (x : β i),
  (fun₀ | i => -x) = -fun₀ | i => x
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.StdSimplex.map_comp : ∀ {R : Type u} [inst : PartialOrder R] [inst_1 : Semiring R] {M : Type u_9} {N : Type u_10} {P : Type u_11}
  [inst_2 : IsStrictOrderedRing R] (f : Convexity.StdSimplex R M) (g₁ : M → N) (g₂ : N → P),
  Convexity.StdSimplex.map (g₂ ∘ g₁) f = Convexity.StdSimplex.map g₂ (Convexity.StdSimplex.map g₁ f)
-- Mathlib.Combinatorics.Matroid.Map
Matroid.comapOn_isBase_iff_of_surjOn : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {N : Matroid β} {E B : Set α},
  Set.SurjOn f E N.E → ((N.comapOn E f).IsBase B ↔ N.IsBase (f '' B) ∧ Set.InjOn f B ∧ B ⊆ E)
-- Mathlib.CategoryTheory.Comma.Over.OverClass
CategoryTheory.OverClass.asOver_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X S : C) [inst_1 : CategoryTheory.OverClass X S],
  (CategoryTheory.OverClass.asOver X S).hom = X ↘ S
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.coeff_smul : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {S₁ : Type u_2} [inst_1 : SMulZeroClass S₁ R] (m : σ →₀ ℕ)
  (C : S₁) (p : MvPolynomial σ R), MvPolynomial.coeff m (C • p) = C • MvPolynomial.coeff m p
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.rightUnshift_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (K L : CochainComplex C ℤ) (n a n' : ℤ) (hn' : n' + a = n), CochainComplex.HomComplex.Cochain.rightUnshift 0 n hn' = 0
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.mul_eq_one_iff : ∀ {α : Type u_2} [inst : CommGroup α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedMonoid α] {s t : NonemptyInterval α},
  s * t = 1 ↔ ∃ a b, s = NonemptyInterval.pure a ∧ t = NonemptyInterval.pure b ∧ a * b = 1
-- Mathlib.Algebra.Group.Units.Basic
IsUnit.div_eq_div_iff : ∀ {α : Type u} [inst : DivisionCommMonoid α] {a b c d : α}, IsUnit b → IsUnit d → (a / b = c / d ↔ a * d = c * b)
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofOptionInfo.injEq : ∀ (i i_1 : Lean.Elab.OptionInfo), (Lean.Elab.Info.ofOptionInfo i = Lean.Elab.Info.ofOptionInfo i_1) = (i = i_1)
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Coverage.toGrothendieck_toPrecoverage : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.Coverage C),
  J.toGrothendieck = J.toGrothendieck
-- Mathlib.Combinatorics.Quiver.Path.Weight
Quiver.Path.addWeight.eq_1 : ∀ {V : Type u_1} [inst : Quiver V] {R : Type u_3} [inst_1 : AddMonoid R] (w : {i j : V} → (i ⟶ j) → R) (x : V),
  Quiver.Path.addWeight w Quiver.Path.nil = 0
-- Mathlib.Data.List.Basic
List.map_foldl_erase : ∀ {α : Type u} {β : Type v} [inst : BEq α] [LawfulBEq α] [inst_2 : BEq β] [LawfulBEq β] {f : α → β},
  Function.Injective f →
    ∀ {l₁ l₂ : List α},
      List.map f (List.foldl List.erase l₁ l₂) = List.foldl (fun l a => l.erase (f a)) (List.map f l₁) l₂
-- Mathlib.AlgebraicGeometry.Limits
/-- **Alias** of `AlgebraicGeometry.specPUnitIsInitial`.

---

`Spec 0` is the initial object in the category of schemes.  -/
AlgebraicGeometry.specPunitIsInitial : CategoryTheory.Limits.IsInitial (AlgebraicGeometry.Spec (CommRingCat.of PUnit.{u + 1}))
-- Mathlib.Topology.Category.UniformSpace
UniformSpaceCat.coe_comp : ∀ {X Y Z : UniformSpaceCat} (f : X ⟶ Y) (g : Y ⟶ Z),
  ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) =
    ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Init.Internal.Order.Basic
Lean.Order.monotone_ite : ∀ {α : Sort u} {β : Sort v} [inst : Lean.Order.PartialOrder α] [inst_1 : Lean.Order.PartialOrder β] (c : Prop)
  [inst_2 : Decidable c] (k₁ k₂ : α → β),
  Lean.Order.monotone k₁ → Lean.Order.monotone k₂ → Lean.Order.monotone fun x => if c then k₁ x else k₂ x
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.instInhabitedWidePullbackShape : (J : Type w) → Inhabited (CategoryTheory.Limits.WidePullbackShape J)
-- Mathlib.Data.Finite.Prod
Set.Finite.toFinset_offDiag : ∀ {α : Type u_1} {s : Set α} (hs : s.Finite), ⋯.toFinset = hs.toFinset.offDiag
-- Mathlib.RingTheory.AdicCompletion.Basic
/-- The composition of lift linear map `lift I f h : M →ₗ[R] N` with the canonical
projection `N → N ⧸ (I ^ n • ⊤)` is `f n` .
 -/
IsAdicComplete.mk_lift : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u_5} [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : IsAdicComplete I N]
  {f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤} (h : ∀ {m n : ℕ} (hle : m ≤ n), Submodule.factorPow I N hle ∘ₗ f n = f m)
  (n : ℕ) (x : M), Submodule.Quotient.mk ((IsAdicComplete.lift I f ⋯) x) = (f n) x
-- Mathlib.RingTheory.Polynomial.Opposites
Polynomial.opRingEquiv_op_C : ∀ {R : Type u_1} [inst : Semiring R] (a : R),
  (Polynomial.opRingEquiv R) (MulOpposite.op (Polynomial.C a)) = Polynomial.C (MulOpposite.op a)
-- Mathlib.Order.Category.FinBddDistLat
FinBddDistLat.id_apply : ∀ (X : FinBddDistLat) (x : ↑X.toDistLat),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
/-- The type (II) simplex obtained as a face of a type (I) simplex.  -/
SSet.prodStdSimplex.pairingCore.Type₁.δ : {m : ℕ} →
  {k : Fin (m + 1)} →
    {n : ℕ} → SSet.prodStdSimplex.pairingCore.Type₁ k n → ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N
-- Mathlib.Combinatorics.Colex
Finset.geomSum_ofColex_strictMono : ∀ {n : ℕ}, 2 ≤ n → StrictMono fun s => ∑ k ∈ ofColex s, n ^ k
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_trunc : ∀ {M : Type u_2} [inst : CommMonoid M] {a b : ℕ} (f : Fin (a + b) → M),
  (∀ (j : Fin b), f (Fin.natAdd a j) = 1) → ∏ i, f i = ∏ i, f (Fin.castAdd b i)
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
/-- `repr` is the isomorphism between the additive group `G` and the additive free group
generated by `ι`.  -/
FreeAddGroupBasis.repr : {ι : Type u_1} → {G : Type u_2} → [inst : AddGroup G] → FreeAddGroupBasis ι G → G ≃+ FreeAddGroup ι
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.instNontrivialLocalizationOfIsCancelAdd : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} [IsCancelAdd M] [Nontrivial M],
  Nontrivial (AddLocalization S)
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.norm_integral_le_of_norm_le : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {f : α → G} {g : α → ℝ},
  MeasureTheory.Integrable g μ → (∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ g x) → ‖∫ (x : α), f x ∂μ‖ ≤ ∫ (x : α), g x ∂μ
-- Mathlib.Algebra.Category.Grp.EpiMono
MonoidHom.range_eq_top_of_cancel : ∀ {A : Type u} {B : Type v} [inst : CommGroup A] [inst_1 : CommGroup B] {f : A →* B},
  (∀ (u v : B →* B ⧸ f.range), u.comp f = v.comp f → u = v) → f.range = ⊤
-- Mathlib.Logic.Relator
/-- A relation is "right total" if every element appears on the right.  -/
Relator.RightTotal : {α : Sort u₁} → {β : Sort u₂} → (α → β → Prop) → Prop
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.mkElimApp.loop : Lean.Meta.ElimInfo → Lean.Name → Lean.Elab.Tactic.ElimApp.M✝ Unit
-- Init.Data.Array.Lemmas
Array.flatten_replicate_replicate : ∀ {n m : ℕ} {α : Type u_1} {a : α}, (Array.replicate n (Array.replicate m a)).flatten = Array.replicate (n * m) a
-- Std.Data.DHashMap.Raw
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Raw.WF.size_buckets_pos : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Raw α β),
  m.WF → 0 < m.buckets.size
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRightConst.go_le_size : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (distance : ℕ)
  (input : aig.RefVec w) (curr : ℕ) (hcurr : curr ≤ w) (s : aig.RefVec curr),
  aig.decls.size ≤
    (Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRightConst.go aig input distance curr hcurr s).aig.decls.size
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.ext_iff : ∀ {J : Type w} {inst : CategoryTheory.SmallCategory J} {κ : Cardinal.{w}}
  {x y : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ}, x = y ↔ x.W = y.W ∧ x.P = y.P