mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- An inner product with a sum on the right.  -/
inner_sum : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} (s : Finset ι) (f : ι → E) (x : E), inner 𝕜 x (∑ i ∈ s, f i) = ∑ i ∈ s, inner 𝕜 x (f i)
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.Entry.ematch : Lean.Meta.Grind.EMatchTheorem → Lean.Meta.Grind.Entry
-- Mathlib.Util.Superscript
/-- A mapping from subscripts to and from regular text.  -/
Mathlib.Tactic.Superscript.Mapping.subscript : Mathlib.Tactic.Superscript.Mapping
-- Batteries.Tactic.Lint.Frontend
/-- Get the list of declarations in the current module.  -/
Batteries.Tactic.Lint.getDeclsInCurrModule : Lean.CoreM (Array Lean.Name)
-- Mathlib.Topology.Semicontinuity.Defs
SemicontinuousOn.inf : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {r : α → β → Prop} {s : Set α} {r' : α → β → Prop},
  SemicontinuousOn r s → SemicontinuousOn r' s → SemicontinuousOn (r ⊓ r') s
-- Mathlib.Order.Preorder.Finsupp
/-- `equivFunOnFinite` as an order isomorphism.  -/
Finsupp.orderIsoFunOnFinite : {ι : Type u_1} → {M : Type u_2} → [inst : Zero M] → [inst_1 : LE M] → [Finite ι] → (ι →₀ M) ≃o (ι → M)
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
/-- Ultrametric property of a p-adic valuation.  -/
padicValRat.add_eq_min : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {q r : ℚ},
  q + r ≠ 0 →
    q ≠ 0 → r ≠ 0 → padicValRat p q ≠ padicValRat p r → padicValRat p (q + r) = min (padicValRat p q) (padicValRat p r)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.defnCommRing.inj : ∀ {e : Lean.Expr} {p : Int.Internal.Linear.Poly} {re : Lean.Meta.Grind.Arith.CommRing.RingExpr}
  {rp : Lean.Grind.CommRing.Poly} {p' : Int.Internal.Linear.Poly} {e_1 : Lean.Expr} {p_1 : Int.Internal.Linear.Poly}
  {re_1 : Lean.Meta.Grind.Arith.CommRing.RingExpr} {rp_1 : Lean.Grind.CommRing.Poly} {p'_1 : Int.Internal.Linear.Poly},
  Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.defnCommRing e p re rp p' =
      Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.defnCommRing e_1 p_1 re_1 rp_1 p'_1 →
    e = e_1 ∧ p = p_1 ∧ re = re_1 ∧ rp = rp_1 ∧ p' = p'_1
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.prehaar_empty : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] (K₀ : TopologicalSpace.PositiveCompacts G) {U : Set G},
  MeasureTheory.Measure.haar.prehaar (↑K₀) U ⊥ = 0
-- Mathlib.Data.Set.Opposite
Set.singleton_unop_op : ∀ {α : Type u_1} (x : αᵒᵖ), {Opposite.unop x}.op = {x}
-- Mathlib.Algebra.Category.Ring.FilteredColimits
/-- The colimit of `F ⋙ forget₂ SemiRingCat MonCat` in the category `MonCat`.
In the following, we will show that this has the structure of a semiring.
 -/
SemiRingCat.FilteredColimits.R : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    CategoryTheory.Functor J SemiRingCat → [CategoryTheory.IsFiltered J] → MonCat
-- Mathlib.Geometry.Manifold.Instances.Sphere
_private.Mathlib.Geometry.Manifold.Instances.Sphere.0.stereographic'_neg : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {n : ℕ}
  [inst_2 : Fact (Module.finrank ℝ E = n + 1)] (v : ↑(Metric.sphere 0 1)), ↑(stereographic' n (-v)) v = 0
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- Suppose `a : X → Set A` is a continuous family of nonnegative elements.
Suppose further that `s : X → Set ℝ≥0` is a family of compact sets such that `s x₀` contains the
spectrum of `a x` for all sufficiently close `x`. If `f : ℝ≥0 → ℝ≥0` is continuous on each `s x`
and `f 0 = 0`, then `fun x ↦ cfc f (a x)` is continuous.  -/
Continuous.cfcₙ_nnreal : ∀ {X : Type u_1} {A : Type u_2} [inst : NonUnitalNormedRing A] [inst_1 : StarRing A] [inst_2 : NormedSpace ℝ A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : SMulCommClass ℝ A A] [ContinuousStar A]
  [inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A]
  [inst_8 : StarOrderedRing A] [inst_9 : NonnegSpectrumClass ℝ A] [T2Space A] [IsSemitopologicalRing A]
  [inst_12 : TopologicalSpace X] {s : X → Set NNReal} (f : NNReal → NNReal) {a : X → A},
  Continuous a →
    (∀ (x : X), IsCompact (s x)) →
      (∀ (x₀ : X), ∀ᶠ (x : X) in nhds x₀, quasispectrum NNReal (a x) ⊆ s x₀) →
        autoParam (∀ (x : X), ContinuousOn f (s x)) Continuous.cfcₙ_nnreal._auto_1 →
          autoParam (f 0 = 0) Continuous.cfcₙ_nnreal._auto_3 →
            autoParam (∀ (x : X), 0 ≤ a x) Continuous.cfcₙ_nnreal._auto_5 → Continuous fun x => cfcₙ f (a x)
-- Mathlib.CategoryTheory.Sites.Hypercover.Saturate
CategoryTheory.PreZeroHypercover.saturate_p₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  (x x_1 : E.I₀) (r : E.Relation x x_1), E.saturate.p₂ r = r.snd
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.equivComma_counitIso_hom_app_right_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (X : CategoryTheory.Comma (CategoryTheory.Functor.const C) (CategoryTheory.Functor.id (CategoryTheory.Functor C D)))
  (X_1 : C),
  (CategoryTheory.WithInitial.equivComma.counitIso.hom.app X).right.app X_1 =
    CategoryTheory.CategoryStruct.id
      (match CategoryTheory.WithInitial.incl.obj X_1 with
      | CategoryTheory.WithInitial.of x => X.right.obj x
      | CategoryTheory.WithInitial.star => X.left)
-- Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
CategoryTheory.MonoidalCategory.IsPushout.inr_isoPushout_inv_whiskerRight : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {Z X Y P : C}
  {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : CategoryTheory.IsPushout f g inl inr)
  [inst_2 : CategoryTheory.Limits.HasPushout f g] {Q : C},
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.pushout.inr f g) Q)
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight hP.isoPushout.inv Q) =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight inr Q
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toList_mapM_filterMapM : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [inst : Monad m]
  [LawfulMonad m] [inst_2 : Monad n] [inst_3 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
  [inst_6 : Monad o] [inst_7 : MonadAttach o] [LawfulMonad o] [WeaklyLawfulMonadAttach o] [inst_10 : MonadLiftT m n]
  [inst_11 : MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] {f : β → n (Option γ)} {g : γ → o δ} {it : Std.IterM m β},
  (Std.IterM.mapM g (Std.IterM.filterMapM f it)).toList =
    (Std.IterM.filterMapM
        (fun b => do
          let __do_lift ← liftM (f b)
          match __do_lift with
            | none => pure none
            | some fb => some <$> g fb)
        it).toList
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.of_forall_mem_unit_iff : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {t₁ t₂ : Std.TreeMap α Unit cmp},
  (∀ (k : α), k ∈ t₁ ↔ k ∈ t₂) → t₁.Equiv t₂
-- Mathlib.Topology.Sheaves.CommRingCat
TopCat.Presheaf.epi_toLocalizationPresheaf : ∀ {X : TopCat} {F : TopCat.Presheaf CommRingCat X} (G : F.SubmonoidPresheaf),
  CategoryTheory.Epi G.toLocalizationPresheaf
-- Aesop.Tree.State
Aesop.MVarCluster.isIrrelevantNoCache : Aesop.MVarCluster → BaseIO Bool
-- Mathlib.LinearAlgebra.Multilinear.Basic
LinearMap.compMultilinearMap_domDomCongr : ∀ {R : Type uR} {M₂ : Type v₂} {M₃ : Type v₃} {M' : Type v'} [inst : Semiring R] [inst_1 : AddCommMonoid M₂]
  [inst_2 : AddCommMonoid M₃] [inst_3 : AddCommMonoid M'] [inst_4 : Module R M₂] [inst_5 : Module R M₃]
  [inst_6 : Module R M'] {ι₁ : Type u_1} {ι₂ : Type u_2} (σ : ι₁ ≃ ι₂) (g : M₂ →ₗ[R] M₃)
  (f : MultilinearMap R (fun x => M') M₂),
  MultilinearMap.domDomCongr σ (g.compMultilinearMap f) = g.compMultilinearMap (MultilinearMap.domDomCongr σ f)
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.sheafIsoOfIso_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : AlgebraicGeometry.PresheafedSpace C} (H : X ≅ Y),
  (AlgebraicGeometry.PresheafedSpace.sheafIsoOfIso H).hom = H.hom.c
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.zsmul_empty : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SubtractionMonoid α] {n : ℤ}, n ≠ 0 → n • ∅ = ∅
-- Mathlib.Data.Analysis.Topology
Ctop.Realizer.tendsto_nhds_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {m : β → α} {f : Filter β} (F : f.Realizer)
  (R : Ctop.Realizer α) {a : α},
  Filter.Tendsto m f (nhds a) ↔ ∀ (t : R.σ), a ∈ R.F.f t → ∃ s, ∀ x ∈ F.F.f s, m x ∈ R.F.f t
-- Mathlib.Computability.TuringMachine.Tape
Turing.BlankRel.trans : ∀ {Γ : Type u_1} [inst : Inhabited Γ] {l₁ l₂ l₃ : List Γ},
  Turing.BlankRel l₁ l₂ → Turing.BlankRel l₂ l₃ → Turing.BlankRel l₁ l₃
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.instAddMonoid : {R : Type u_1} → {a b : R} → [AddMonoid R] → AddMonoid (QuadraticAlgebra R a b)
-- Mathlib.Probability.CDF
/-- The measure associated to the cdf of a probability measure is the same probability measure.  -/
ProbabilityTheory.measure_cdf : ∀ (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ], (ProbabilityTheory.cdf μ).measure = μ
-- Mathlib.NumberTheory.ModularForms.QExpansion
UpperHalfPlane.qExpansion_coeff_zero : ∀ {h : ℝ} {f : UpperHalfPlane → ℂ},
  0 < h →
    AnalyticAt ℂ (UpperHalfPlane.cuspFunction h f) 0 →
      Function.Periodic (f ∘ ↑UpperHalfPlane.ofComplex) ↑h →
        (PowerSeries.coeff 0) (UpperHalfPlane.qExpansion h f) = UpperHalfPlane.valueAtInfty f
-- Init.Grind.Ring.Basic
Lean.Grind.Ring.intCast_eq_ofNat_of_nonneg : ∀ {α : Type u} [inst : Lean.Grind.Ring α] (x : ℤ), Int.ble' 0 x = true → IntCast.intCast x = OfNat.ofNat x.toNat
-- Mathlib.Logic.Equiv.PartialEquiv
/-- Two equivalent partial equivs have coinciding inverses on the target.  -/
PartialEquiv.EqOnSource.symm_eqOn : ∀ {α : Type u_1} {β : Type u_2} {e e' : PartialEquiv α β}, e ≈ e' → Set.EqOn (↑e.symm) (↑e'.symm) e.target
-- Mathlib.Topology.Homotopy.HomotopyGroup
GenLoop.copy.eq_1 : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X} (f : ↑(GenLoop N X x)) (g : (N → ↑unitInterval) → X)
  (h : g = ⇑f), GenLoop.copy f g h = ⟨{ toFun := g, continuous_toFun := ⋯ }, ⋯⟩
-- Mathlib.Algebra.Field.Subfield.Defs
/-- A subfield contains the field's 1.  -/
Subfield.one_mem : ∀ {K : Type u} [inst : DivisionRing K] (s : Subfield K), 1 ∈ s
-- Init.Data.SInt.Lemmas
Int64.sub_right_inj : ∀ {a b : Int64} (c : Int64), c - a = c - b ↔ a = b
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instCommGroup.eq_1 : ∀ {α : Type u_1} {l : Filter α} {G : Type u_6} [inst : CommGroup G],
  Filter.Germ.instCommGroup = { toGroup := Filter.Germ.instGroup, mul_comm := ⋯ }
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_dvd_ediv : ∀ {a b c : ℤ}, a ∣ b → b ∣ c → b / a ∣ c / a
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.rightHomologyDataShortComplex_g' : ∀ {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 l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.rightHomologyDataShortComplex_g'._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.rightHomologyDataShortComplex_g'._auto_3),
  (X.rightHomologyDataShortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g' = X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ hn₂
-- Mathlib.Algebra.BigOperators.Fin
/-- A product of a function `f : Fin (n + 1) → M` over all `Fin (n + 1)`
is the product of `f 0` times the remaining product  -/
Fin.prod_univ_succ : ∀ {M : Type u_2} [inst : CommMonoid M] {n : ℕ} (f : Fin (n + 1) → M), ∏ i, f i = f 0 * ∏ i, f i.succ
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithInitial.coconeEquiv_counitIso_hom_app_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Under X)}
  (X_1 : CategoryTheory.Limits.Cocone (CategoryTheory.WithInitial.liftFromUnder.obj K)),
  (CategoryTheory.WithInitial.coconeEquiv.counitIso.hom.app X_1).hom = CategoryTheory.CategoryStruct.id X_1.pt
-- Mathlib.Algebra.Module.Rat
/-- There can be at most one `Module ℚ≥0 E` structure on an additive commutative monoid.  -/
subsingleton_nnrat_module : ∀ (E : Type u_3) [inst : AddCommMonoid E], Subsingleton (Module ℚ≥0 E)
-- Mathlib.Analysis.Real.Sqrt
/-- **Cauchy-Schwarz inequality** for finsets using square roots in `ℝ≥0`.  -/
NNReal.sum_sqrt_mul_sqrt_le : ∀ {ι : Type u_2} (s : Finset ι) (f g : ι → NNReal),
  ∑ i ∈ s, NNReal.sqrt (f i) * NNReal.sqrt (g i) ≤ NNReal.sqrt (∑ i ∈ s, f i) * NNReal.sqrt (∑ i ∈ s, g i)
-- Mathlib.Data.Setoid.Partition
IndexedPartition.proj_eq_iff : ∀ {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) {x y : α},
  hs.proj x = hs.proj y ↔ hs.index x = hs.index y
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.le_restrict_apply : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s t : Set α), μ (t ∩ s) ≤ (μ.restrict s) t
-- Mathlib.CategoryTheory.Enriched.Basic
/-- The identity enriched functor.  -/
CategoryTheory.EnrichedFunctor.id : (V : Type v) →
  [inst : CategoryTheory.Category.{w, v} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      (C : Type u₁) → [inst_2 : CategoryTheory.EnrichedCategory V C] → CategoryTheory.EnrichedFunctor V C C
-- Mathlib.Combinatorics.SimpleGraph.Paths
_private.Mathlib.Combinatorics.SimpleGraph.Paths.0.SimpleGraph.Walk.bypass.match_1.eq_2 : ∀ {V : Type u_1} {G : SimpleGraph V} {u : V} (motive : (v : V) → G.Walk u v → Sort u_2) (v v_1 : V) (ha : G.Adj u v_1)
  (p : G.Walk v_1 v) (h_1 : Unit → motive u SimpleGraph.Walk.nil)
  (h_2 : (v v_2 : V) → (ha : G.Adj u v_2) → (p : G.Walk v_2 v) → motive v (SimpleGraph.Walk.cons ha p)),
  (match v, SimpleGraph.Walk.cons ha p with
    | .(u), SimpleGraph.Walk.nil => h_1 ()
    | v, SimpleGraph.Walk.cons ha p => h_2 v v_2 ha p) =
    h_2 v v_1 ha p
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
SimpleGraph.adjMatrix_hadamard_self : ∀ (α : Type u_1) {V : Type u_2} (G : SimpleGraph V) [inst : DecidableRel G.Adj] [inst_1 : MulZeroOneClass α],
  (SimpleGraph.adjMatrix α G).hadamard (SimpleGraph.adjMatrix α G) = SimpleGraph.adjMatrix α G
-- Mathlib.Order.Interval.Set.SuccPred
Set.Ioc_pred_left_eq_Icc : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] [NoMinOrder α] (a b : α),
  Set.Ioc (Order.pred a) b = Set.Icc a b
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- A category with strong epi images has image maps.  -/
CategoryTheory.Limits.hasImageMapsOfHasStrongEpiImages : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasImages C]
  [CategoryTheory.Limits.HasStrongEpiImages C], CategoryTheory.Limits.HasImageMaps C
-- Batteries.Data.Nat.Bitwise.Lemmas
Nat.and_or_left_injective : ∀ {m x y : ℕ}, m &&& x = m &&& y → m ||| x = m ||| y → x = y
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.consRecOn_cons : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {motive : Monoid.CoprodI.Word M → Sort u_4} (i : ι)
  (m : M i) (w : Monoid.CoprodI.Word M) (h1 : w.fstIdx ≠ some i) (h2 : m ≠ 1)
  (h_empty : motive Monoid.CoprodI.Word.empty)
  (h_cons :
    (i : ι) →
      (m : M i) →
        (w : Monoid.CoprodI.Word M) →
          (h1 : w.fstIdx ≠ some i) → (h2 : m ≠ 1) → motive w → motive (Monoid.CoprodI.Word.cons m w h1 h2)),
  Monoid.CoprodI.Word.consRecOn (Monoid.CoprodI.Word.cons m w h1 h2) h_empty h_cons =
    h_cons i m w h1 h2 (Monoid.CoprodI.Word.consRecOn w h_empty h_cons)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigO_sup : ∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {f : α → E}
  {g' : α → F'} {l l' : Filter α}, f =O[l ⊔ l'] g' ↔ f =O[l] g' ∧ f =O[l'] g'
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRank_ne_top_iff : ∀ {α : Type u_1} (M : Matroid α), M.eRank ≠ ⊤ ↔ M.RankFinite
-- Init.Data.Int.Order
_private.Init.Data.Int.Order.0.Int.add.match_1.eq_4 : ∀ (motive : ℤ → ℤ → Sort u_1) (m n : ℕ) (h_1 : (m n : ℕ) → motive (Int.ofNat m) (Int.ofNat n))
  (h_2 : (m n : ℕ) → motive (Int.ofNat m) (Int.negSucc n)) (h_3 : (m n : ℕ) → motive (Int.negSucc m) (Int.ofNat n))
  (h_4 : (m n : ℕ) → motive (Int.negSucc m) (Int.negSucc n)),
  (match Int.negSucc m, Int.negSucc n with
    | Int.ofNat m, Int.ofNat n => h_1 m n
    | Int.ofNat m, Int.negSucc n => h_2 m n
    | Int.negSucc m, Int.ofNat n => h_3 m n
    | Int.negSucc m, Int.negSucc n => h_4 m n) =
    h_4 m n
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_inverse_obj_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (A : CategoryTheory.Mon C) {X Y : CategoryTheory.Discrete PUnit.{w + 1}} (x : X ⟶ Y),
  (CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit.inverse.obj A).map x = CategoryTheory.CategoryStruct.id A.X
-- Mathlib.Data.Set.Insert
Set.eq_or_mem_of_mem_insert : ∀ {α : Type u_1} {x a : α} {s : Set α}, x ∈ insert a s → x = a ∨ x ∈ s
-- Mathlib.Order.KrullDimension
LTSeries.height_last_longestOf : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : FiniteDimensionalOrder α],
  ↑(Order.height (RelSeries.last (LTSeries.longestOf α))) = Order.krullDim α
-- Init.Data.Array.MapIdx
Array.mapIdx_eq_iff : ∀ {α : Type u_1} {α_1 : Type u_2} {f : ℕ → α → α_1} {ys : Array α_1} {xs : Array α},
  Array.mapIdx f xs = ys ↔ ∀ (i : ℕ), ys[i]? = Option.map (f i) xs[i]?
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
CategoryTheory.Meq.equiv_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t}
  [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [inst_3 : CategoryTheory.ConcreteCategory D FD]
  [inst_4 :
    ∀ {X : C} (S : J.Cover X),
      CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape)
        (CategoryTheory.forget D)]
  {X : C} {P : CategoryTheory.Functor Cᵒᵖ D} {S : J.Cover X}
  [inst_5 : CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  (x : CategoryTheory.ToType (CategoryTheory.Limits.multiequalizer (S.index P))) (I : S.Arrow),
  ↑((CategoryTheory.Meq.equiv P S) x) I =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Multiequalizer.ι (S.index P) I)) x
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.center_nonempty : ∀ {α : Type u_1} {G : SimpleGraph α} [Nonempty α], G.center.Nonempty
-- Init.Data.UInt.Lemmas
UInt8.toUInt16_mod : ∀ (a b : UInt8), (a % b).toUInt16 = a.toUInt16 % b.toUInt16
-- Init.GrindInstances.Ring.Fin
Lean.Grind.Fin.instCommRingFinOfNeZeroNat : (n : ℕ) → [NeZero n] → Lean.Grind.CommRing (Fin n)
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.instIsCancelAdd : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [IsCancelAdd R], IsCancelAdd (AddMonoidAlgebra R M)
-- Init.Data.Slice.List.Basic
instSliceableListSliceNat_4 : {α : Type u} → Std.Roo.Sliceable (ListSlice α) ℕ (ListSlice α)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.mapConePostcomposeEquivalenceFunctor.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D)
  {F G : CategoryTheory.Functor J C} {α : F ≅ G} {c : CategoryTheory.Limits.Cone F},
  H.mapConePostcomposeEquivalenceFunctor =
    CategoryTheory.Limits.Cone.ext
      (CategoryTheory.Iso.refl (H.mapCone ((CategoryTheory.Limits.Cone.postcomposeEquivalence α).functor.obj c)).pt) ⋯
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.throw_Option_lift : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {ε α : Type u}
  [inst_4 : MonadExceptOf ε m] (err : ε) (post : α → Pred) (epost : EPost.Cons✝ Pred EPred),
  ⦃ Std.Internal.Do.wp (MonadExceptOf.throw err) (Std.Internal.Do.EPost.Cons.pushOption post epost) epost.tail ⦄
    MonadExceptOf.throw err ⦃ post; epost ⦄
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.normSq_ne_zero : ∀ (z : UpperHalfPlane), Complex.normSq ↑z ≠ 0
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.instNormedSpace : {α : Type u} →
  {β : Type v} →
    {𝕜 : Type u_1} →
      [inst : TopologicalSpace α] →
        [inst_1 : SeminormedAddCommGroup β] →
          [inst_2 : NormedField 𝕜] → [NormedSpace 𝕜 β] → NormedSpace 𝕜 (BoundedContinuousFunction α β)
-- Init.Data.Float.Model.Unpacked.Pack.Lemmas
Float.Model.UnpackedFloat.pack.match_1.congr_eq_1 : ∀ (motive : Float.Model.UnpackedFloat → Sort u_1) (x : Float.Model.UnpackedFloat)
  (h_1 : Unit → motive Float.Model.UnpackedFloat.notANumber)
  (h_2 : (s : Float.Model.UnpackedFloat.Sign) → motive (Float.Model.UnpackedFloat.infinity s))
  (h_3 : (s : Float.Model.UnpackedFloat.Sign) → motive (Float.Model.UnpackedFloat.zero s))
  (h_4 :
    (s : Float.Model.UnpackedFloat.Sign) →
      (m : ℕ) → (e : ℤ) → (mantissa_pos : 0 < m) → motive (Float.Model.UnpackedFloat.finite s m e mantissa_pos)),
  x = Float.Model.UnpackedFloat.notANumber →
    (match x with
      | Float.Model.UnpackedFloat.notANumber => h_1 ()
      | Float.Model.UnpackedFloat.infinity s => h_2 s
      | Float.Model.UnpackedFloat.zero s => h_3 s
      | Float.Model.UnpackedFloat.finite s m e mantissa_pos => h_4 s m e mantissa_pos) ≍
      h_1 ()
-- Mathlib.Data.Finset.MulAntidiagonal
Finset.antidiagonal_mono_right : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelAddMonoid α] {s t : Set α}
  {hs : s.IsPWO} {ht : t.IsPWO} {a : α} {u : Set α} {hu : u.IsPWO},
  u ⊆ t → Finset.antidiagonal hs hu a ⊆ Finset.antidiagonal hs ht a
-- Mathlib.Topology.Algebra.OpenSubgroup
IsTopologicalGroup.mulInvClosureNhd.mul : ∀ {G : Type u_1} [inst : TopologicalSpace G] {T W : Set G} [inst_1 : Group G],
  IsTopologicalGroup.mulInvClosureNhd T W → W * T ⊆ W
-- Mathlib.Analysis.Normed.Group.Uniform
edist_mul_mul_le : ∀ {E : Type u_2} [inst : SeminormedCommGroup E] (a₁ a₂ b₁ b₂ : E), edist (a₁ * a₂) (b₁ * b₂) ≤ edist a₁ b₁ + edist a₂ b₂
-- Init.Data.Range.Polymorphic.PRange
/-- `*...<b` is the range of elements less than `b`. See also `Std.Rio`.  -/
Std.«term*...<_» : Lean.ParserDescr
-- Init.Data.Nat.Lemmas
_private.Init.Data.Nat.Lemmas.0.Nat.anyLTTR.loop.congr_simp : ∀ (n : ℕ) (f f_1 : (i : ℕ) → i < n → Bool),
  f = f_1 → ∀ (i i_1 : ℕ) (e_i : i = i_1) (a : i ≤ n), Nat.anyLTTR.loop✝ n f i a = Nat.anyLTTR.loop✝ n f_1 i_1 ⋯
-- Mathlib.Topology.Category.CompHausLike.EffectiveEpi
CompHausLike.preregular : ∀ {P : TopCat → Prop} [CompHausLike.HasExplicitPullbacks P],
  (∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
      CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) →
    CategoryTheory.Preregular (CompHausLike P)
-- Init.Data.SInt.Lemmas
Int16.ofBitVec_ofNatLT : ∀ (n : ℕ) (hn : n < 2 ^ 16), Int16.ofBitVec n#'hn = Int16.ofNat n
-- Lean.Meta.Sym.AlphaShareCommon
_private.Lean.Meta.Sym.AlphaShareCommon.0.Lean.Meta.Sym.saveInc : Lean.Expr → Lean.Meta.Sym.AlphaShareCommonM Lean.Expr
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instLeftCancelSemigroup.eq_1 : ∀ {α : Type u_1} [inst : LeftCancelSemigroup α],
  Lex.instLeftCancelSemigroup = { toSemigroup := Lex.instSemigroup, toIsLeftCancelMul := ⋯ }
-- Mathlib.Order.Preorder.Chain
Antitone.isChain_image : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α} {f : α → β},
  Antitone f → IsChain (fun x1 x2 => x1 ≤ x2) s → IsChain (fun x1 x2 => x1 ≤ x2) (f '' s)