mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- If the oriented angle between two vectors is `π / 2`, the inner product of those vectors
(reversed) is zero.  -/
Orientation.inner_rev_eq_zero_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑(Real.pi / 2) → inner ℝ y x = 0
-- Mathlib.Topology.Homotopy.HSpaces
Path.delayReflLeft_one : ∀ {X : Type u} [inst : TopologicalSpace X] {x y : X} (γ : Path x y), Path.delayReflLeft 1 γ = γ
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.UnsatProof.lt.injEq : ∀ (c c_1 : Lean.Meta.Grind.Arith.Linear.IneqCnstr),
  (Lean.Meta.Grind.Arith.Linear.UnsatProof.lt c = Lean.Meta.Grind.Arith.Linear.UnsatProof.lt c_1) = (c = c_1)
-- Mathlib.Order.CompleteLattice.Basic
/-- Introduction rule to prove that `b` is the infimum of `f`: it suffices to check that `b`
is smaller than `f i` for all `i`, and that this is not the case of any `w>b`.
See `ciInf_eq_of_forall_ge_of_forall_gt_exists_lt` for a version in conditionally complete
lattices.  -/
iInf_eq_of_forall_ge_of_forall_gt_exists_lt : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] {b : α} {f : ι → α},
  (∀ (i : ι), b ≤ f i) → (∀ (w : α), b < w → ∃ i, f i < w) → ⨅ i, f i = b
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.nnnorm_coeFn_eq : ∀ {α : Type u} [inst : TopologicalSpace α] (f : BoundedContinuousFunction α ℝ), ⇑f.nnnorm = nnnorm ∘ ⇑f
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.isNone_getElem?_toArray_ric_eq : ∀ {n i : ℕ}, ((*...=n).toArray[i]?.isNone = true) = (n < i)
-- Mathlib.LinearAlgebra.FreeModule.PID
Module.Basis.SmithNormalForm.mk.inj : ∀ {R : Type u_2} {inst : CommRing R} {M : Type u_3} {inst_1 : AddCommGroup M} {inst_2 : Module R M} {N : Submodule R M}
  {ι : Type u_4} {n : ℕ} {bM : Module.Basis ι R M} {bN : Module.Basis (Fin n) R ↥N} {f : Fin n ↪ ι} {a : Fin n → R}
  {snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)} {bM_1 : Module.Basis ι R M} {bN_1 : Module.Basis (Fin n) R ↥N}
  {f_1 : Fin n ↪ ι} {a_1 : Fin n → R} {snf_1 : ∀ (i : Fin n), ↑(bN_1 i) = a_1 i • bM_1 (f_1 i)},
  { bM := bM, bN := bN, f := f, a := a, snf := snf } = { bM := bM_1, bN := bN_1, f := f_1, a := a_1, snf := snf_1 } →
    bM = bM_1 ∧ bN = bN_1 ∧ f = f_1 ∧ a = a_1
-- Mathlib.Topology.MetricSpace.Pseudo.Pi
nndist_pi_const_le : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : Fintype β] (a b : α),
  (nndist (fun x => a) fun x => b) ≤ nndist a b
-- Mathlib.Analysis.Calculus.MeanValue
/-- The mean value theorem: if the derivative of a function is bounded by `C`, then the function is
`C`-Lipschitz. Version with `fderiv` and `LipschitzWith`.  -/
lipschitzWith_of_nnnorm_fderiv_le : ∀ {𝕜 : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜]
  [inst_2 : NormedAddCommGroup G] [inst_3 : NormedSpace 𝕜 G] {E : Type u_5} [inst_4 : NormedAddCommGroup E]
  [inst_5 : NormedSpace 𝕜 E] {f : E → G} {C : NNReal},
  Differentiable 𝕜 f → (∀ (x : E), ‖fderiv 𝕜 f x‖₊ ≤ C) → LipschitzWith C f
-- Std.Data.HashMap.Lemmas
Std.HashMap.get!_union : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} [inst : Inhabited β], (m₁ ∪ m₂).get! k = m₂.getD k (m₁.get! k)
-- Mathlib.CategoryTheory.Idempotents.Basic
CategoryTheory.Idempotents.Equivalence.isIdempotentComplete : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (ε : C ≌ D),
  CategoryTheory.IsIdempotentComplete C → CategoryTheory.IsIdempotentComplete D
-- Mathlib.Data.PFunctor.Univariate.M
/-- `sCorec f i n` creates an approximation of height `n`
of the final coalgebra of `f`  -/
PFunctor.Approx.sCorec : {F : PFunctor.{uA, uB}} → {X : Type w} → (X → ↑F X) → X → (n : ℕ) → PFunctor.Approx.CofixA F n
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
/-- The identity for the `J ⥤ V`-enrichment of the category `J ⥤ C`.  -/
CategoryTheory.Enriched.FunctorCategory.functorEnrichedId : (V : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} C] →
          {J : Type u₃} →
            [inst_3 : CategoryTheory.Category.{v₃, u₃} J] →
              [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] →
                (F₁ : CategoryTheory.Functor J C) →
                  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₁ F₁] →
                    CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Functor J V) ⟶
                      CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom V F₁ F₁
-- Mathlib.RepresentationTheory.Homological.TateCohomology.Basic
tateComplex.map_zero : ∀ {R G : Type u} [inst : CommRing R] [inst_1 : Group G] [inst_2 : Fintype G] {X Y : Rep.{u, u, u} R G},
  tateComplex.map 0 = 0
-- Mathlib.Geometry.Euclidean.NinePointCircle
Affine.Simplex.ninePointCircle_reindex : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {m n : ℕ} (s : Affine.Simplex ℝ P n) (e : Fin (n + 1) ≃ Fin (m + 1)),
  (s.reindex e).ninePointCircle = s.ninePointCircle
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
/-- See `lt_of_tsub_lt_tsub_left` for a stronger statement in a linear order.  -/
lt_of_tsub_lt_tsub_left_of_le : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] [AddLeftReflectLT α], c ≤ a → a - b < a - c → c < b
-- Mathlib.CategoryTheory.Action.Concrete
Action.FintypeCat.ofMulAction_apply : ∀ {G : Type u_1} {H : FintypeCat} [inst : Monoid G] [inst_1 : MulAction G H.obj] (g : G) (x : H.obj),
  (CategoryTheory.ConcreteCategory.hom ((Action.FintypeCat.ofMulAction G H).ρ g)) x = g • x
-- Lean.Data.Json.Basic
Lean.Json.brecOn_1.eq : ∀ {motive_1 : Lean.Json → Sort u} {motive_2 : Array Lean.Json → Sort u}
  {motive_3 : Std.TreeMap.Raw String Lean.Json compare → Sort u} {motive_4 : List Lean.Json → Sort u}
  {motive_5 : Std.DTreeMap.Raw String (fun x => Lean.Json) compare → Sort u}
  {motive_6 : (Std.DTreeMap.Internal.Impl String fun x => Lean.Json) → Sort u} (t : Array Lean.Json)
  (F_1 : (t : Lean.Json) → t.below → motive_1 t) (F_2 : (t : Array Lean.Json) → Lean.Json.below_1 t → motive_2 t)
  (F_3 : (t : Std.TreeMap.Raw String Lean.Json compare) → Lean.Json.below_2 t → motive_3 t)
  (F_4 : (t : List Lean.Json) → Lean.Json.below_3 t → motive_4 t)
  (F_5 : (t : Std.DTreeMap.Raw String (fun x => Lean.Json) compare) → Lean.Json.below_4 t → motive_5 t)
  (F_6 : (t : Std.DTreeMap.Internal.Impl String fun x => Lean.Json) → Lean.Json.below_5 t → motive_6 t),
  Lean.Json.brecOn_1 t F_1 F_2 F_3 F_4 F_5 F_6 = F_2 t (Lean.Json.brecOn_1.go t F_1 F_2 F_3 F_4 F_5 F_6).2
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
ContinuousAlternatingMap.uniformContinuous_coe_fun : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : UniformSpace F] [inst_7 : IsUniformAddGroup F] [ContinuousSMul 𝕜 E], UniformContinuous DFunLike.coe
-- Init.Data.Int.Order
_private.Init.Data.Int.Order.0.Int.toNat.match_1.splitter : (motive : ℤ → Sort u_1) → (x : ℤ) → ((n : ℕ) → motive (Int.ofNat n)) → ((a : ℕ) → motive (Int.negSucc a)) → motive x
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
SSet.Truncated.HomotopyCategory.BinaryProduct.square : ∀ {X Y : SSet.Truncated 2}
  {x₀ x₁ : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })}
  (ex : SSet.Truncated.Edge x₀ x₁)
  {y₀ y₁ : Y.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })}
  (ey : SSet.Truncated.Edge y₀ y₁),
  CategoryTheory.CategoryStruct.comp (SSet.Truncated.HomotopyCategory.homMk (ex.tensor (SSet.Truncated.Edge.id y₀)))
      (SSet.Truncated.HomotopyCategory.homMk ((SSet.Truncated.Edge.id x₁).tensor ey)) =
    CategoryTheory.CategoryStruct.comp (SSet.Truncated.HomotopyCategory.homMk ((SSet.Truncated.Edge.id x₀).tensor ey))
      (SSet.Truncated.HomotopyCategory.homMk (ex.tensor (SSet.Truncated.Edge.id y₁)))
-- Mathlib.RingTheory.Coalgebra.Equiv
/-- An equivalence of coalgebras is an invertible coalgebra homomorphism.  -/
«term_≃ₗc[_]_» : Lean.TrailingParserDescr
-- Init.Data.String.Defs
String.Pos.le_iff : ∀ {s : String} {l r : s.Pos}, l ≤ r ↔ l.offset ≤ r.offset
-- Mathlib.RingTheory.RingHom.EssFiniteType
RingHom.EssFiniteType.comp_iff : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  {f : R →+* S} {g : S →+* T}, f.EssFiniteType → ((g.comp f).EssFiniteType ↔ g.EssFiniteType)
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.mk : {R : Type u_1} →
  [inst : Semiring R] →
    {M : Type u_2} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {N : Type u_3} →
            [inst_3 : AddCommMonoid N] →
              [inst_4 : Module R N] →
                {ι : Type u_7} →
                  (toMultilinearMap : MultilinearMap R (fun x => M) N) →
                    (∀ (v : ι → M) (i j : ι), v i = v j → i ≠ j → toMultilinearMap.toFun v = 0) → M [⋀^ι]→ₗ[R] N
-- Mathlib.Data.Set.Pairwise.Basic
/-- A set is `PairwiseDisjoint` under `f`, if the images of any distinct two elements under `f`
are disjoint.

`s.Pairwise Disjoint` is (definitionally) the same as `s.PairwiseDisjoint id`. We prefer the latter
in order to allow dot notation on `Set.PairwiseDisjoint`, even though the former unfolds more
nicely.  -/
Set.PairwiseDisjoint : {α : Type u_1} → {ι : Type u_4} → [inst : PartialOrder α] → [OrderBot α] → Set ι → (ι → α) → Prop
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.single_ne_zero : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {r : R} {m : M}, MonoidAlgebra.single m r ≠ 0 ↔ r ≠ 0
-- Mathlib.Topology.LocallyFinsupp.Pushforward
/-- The pushforward of a function `c` of locally finite support by a spectral map with respect to a
weight function `w`.
 -/
Function.locallyFinsupp.map : {X : Type u_1} →
  {Y : Type u_2} →
    {R : Type u_3} →
      [inst : TopologicalSpace X] →
        [inst_1 : TopologicalSpace Y] →
          (f : X → Y) →
            (X → R) →
              [inst_2 : Semiring R] →
                [PrespectralSpace Y] → IsSpectralMap f → Function.locallyFinsupp X R → Function.locallyFinsupp Y R
-- Lean.Elab.Do.Legacy
_private.Lean.Elab.Do.Legacy.0.Lean.Elab.Term.getDoSeq : Lean.Syntax → Lean.Syntax
-- Mathlib.Algebra.Group.TransferInstance
Equiv.add.eq_1 : ∀ {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : Add β],
  e.add = { add := fun x y => e.invFun (e.toFun x + e.toFun y) }
-- Mathlib.Analysis.BoxIntegral.Basic
/-- This is an auxiliary lemma used to prove two statements at once. Use one of the next two
lemmas instead.  -/
BoxIntegral.HasIntegral.of_bRiemann_eq_false_of_forall_isLittleO : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
  {l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤},
  l.bRiemann = false →
    ∀ (B : BoxIntegral.BoxAdditiveMap ι ℝ ↑I),
      (∀ (J : BoxIntegral.Box ι), 0 ≤ B J) →
        ∀ (g : BoxIntegral.BoxAdditiveMap ι F ↑I) (s : Set (ι → ℝ)),
          s.Countable →
            (s.Nonempty → l.bHenstock = true) →
              (∀ (c : NNReal),
                  ∀ x ∈ BoxIntegral.Box.Icc I ∩ s,
                    ∀ ε > 0,
                      ∃ δ > 0,
                        ∀ J ≤ I,
                          BoxIntegral.Box.Icc J ⊆ Metric.closedBall x δ →
                            x ∈ BoxIntegral.Box.Icc J →
                              (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε) →
                (∀ (c : NNReal),
                    ∀ x ∈ BoxIntegral.Box.Icc I \ s,
                      ∀ ε > 0,
                        ∃ δ > 0,
                          ∀ J ≤ I,
                            BoxIntegral.Box.Icc J ⊆ Metric.closedBall x δ →
                              (l.bHenstock = true → x ∈ BoxIntegral.Box.Icc J) →
                                (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε * B J) →
                  BoxIntegral.HasIntegral I l f vol (g I)
-- Mathlib.RingTheory.Ideal.Maps
RingHom.liftOfSurjective_comp_apply : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : Ring A] [inst_1 : Ring B] [inst_2 : Ring C] (f : A →+* B)
  (hf : Function.Surjective ⇑f) (g : { g // RingHom.ker f ≤ RingHom.ker g }) (x : A),
  ((f.liftOfSurjective hf) g) (f x) = ↑g x
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.inl_v_desc_f_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ}
  (α : CochainComplex.HomComplex.Cochain F K (-1)) (β : G ⟶ K)
  (eq :
    CochainComplex.HomComplex.δ (-1) 0 α =
      CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp φ β))
  (p q : ℤ) (h : p + -1 = q) {Z : C} (h_1 : K.X q ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inl φ).v p q h)
      (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.desc φ α β eq).f q) h_1) =
    CategoryTheory.CategoryStruct.comp (α.v p q h) h_1
-- Mathlib.Analysis.Calculus.MeanValue
/-- The mean value theorem on a convex set: if the derivative of a function is bounded by `C` on
`s`, then the function is `C`-Lipschitz on `s`. Version with `HasFDerivWithinAt` and
`LipschitzOnWith`.  -/
Convex.lipschitzOnWith_of_nnnorm_hasFDerivWithin_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4}
  [inst_2 : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → G} {s : Set E} {f' : E → E →L[𝕜] G} {C : NNReal},
  (∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) → (∀ x ∈ s, ‖f' x‖₊ ≤ C) → Convex ℝ s → LipschitzOnWith C f s
-- Mathlib.Analysis.Convex.Side
Wbtw.wOppSide₁₃ : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y z : P}, Wbtw R x y z → y ∈ s → s.WOppSide x z
-- Mathlib.Order.SuccPred.Basic
/-- **Alias** of `Order.succ_eq_of_covBy`.

---

See also `Order.le_succ_of_wcovBy`.  -/
CovBy.succ_eq : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] {a b : α}, a ⋖ b → Order.succ a = b
-- Mathlib.Analysis.InnerProductSpace.l2Space
lp.inner_eq_tsum : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {G : ι → Type u_4} [inst_1 : (i : ι) → NormedAddCommGroup (G i)]
  [inst_2 : (i : ι) → InnerProductSpace 𝕜 (G i)] (f g : ↥(lp G 2)), inner 𝕜 f g = ∑' (i : ι), inner 𝕜 (↑f i) (↑g i)
-- Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
AlternatingMap.alternatizeUncurryFin_apply : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] {n : ℕ} (f : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) (v : Fin (n + 1) → M),
  (AlternatingMap.alternatizeUncurryFin f) v = ∑ i, (-1) ^ ↑i • (f (v i)) (i.removeNth v)
-- Mathlib.Analysis.Calculus.FDeriv.Comp
Differentiable.iterate : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : E → E}, Differentiable 𝕜 f → ∀ (n : ℕ), Differentiable 𝕜 f^[n]
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.hasForgetToAddGroup : CategoryTheory.HasForget₂ AddCommGrpCat AddGrpCat
-- Mathlib.MeasureTheory.Order.Lattice
Measurable.sup : ∀ {M : Type u_1} [inst : MeasurableSpace M] {α : Type u_2} {m : MeasurableSpace α} {f g : α → M} [inst_1 : Max M]
  [MeasurableSup₂ M], Measurable f → Measurable g → Measurable (f ⊔ g)
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval_zero : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R], MvPolynomial.eval 0 = MvPolynomial.constantCoeff
-- Mathlib.Algebra.Group.Submonoid.Basic
MonoidHom.ofClosureMEqTopRight.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : Monoid M] [inst_1 : Monoid N] {s : Set M} (f : M → N)
  (hs : Submonoid.closure s = ⊤) (h1 : f 1 = 1) (hmul : ∀ (x y : M), y ∈ s → f (x * y) = f x * f y),
  MonoidHom.ofClosureMEqTopRight f hs h1 hmul = { toFun := f, map_one' := h1, map_mul' := ⋯ }
-- Std.Internal.Do.WP.Lemmas
_private.Std.Internal.Do.WP.Lemmas.0.ExceptT.run_bind.match_1.eq_1 : ∀ {ε α : Type u_1} (motive : Except ε α → Sort u_2) (x : α) (h_1 : (x : α) → motive (Except.ok x))
  (h_2 : (e : ε) → motive (Except.error e)),
  (match Except.ok x with
    | Except.ok x => h_1 x
    | Except.error e => h_2 e) =
    h_1 x
-- Mathlib.Topology.UniformSpace.Cauchy
UniformSpace.secondCountable_of_almost_dense_set : ∀ {α : Type u} [uniformSpace : UniformSpace α] [(uniformity α).IsCountablyGenerated],
  (∀ U ∈ uniformity α, ∃ t, t.Countable ∧ ⋃ x ∈ t, UniformSpace.ball x U = Set.univ) → SecondCountableTopology α
-- Init.Data.Array.Lemmas
Array.isPrefixOf_toList : ∀ {α : Type u_1} [inst : BEq α] {xs ys : Array α}, xs.toList.isPrefixOf ys.toList = xs.isPrefixOf ys
-- Mathlib.Tactic.Ring.RingNF
Mathlib.Tactic.RingNF.RingMode.raw.sizeOf_spec : sizeOf Mathlib.Tactic.RingNF.RingMode.raw = 1
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.wellFoundedGT_of_noetherian : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] [IsNoetherian R M], WellFoundedGT (LieSubmodule R L M)
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.w₀₂_τ₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), CategoryTheory.CategoryStruct.comp S.v₀₁.τ₃ S.v₁₂.τ₃ = 0
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.equation_of_equiv : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {P Q : Fin 3 → R},
  P ≈ Q → (W'.Equation P ↔ W'.Equation Q)
-- Lean.Meta.ACLt
Lean.Expr.ctorWeight : Lean.Expr → UInt8
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
/-- Define a non-unital star algebra homomorphism on a directed supremum of non-unital star
subalgebras by defining it on each non-unital star subalgebra, and proving that it agrees on the
intersection of non-unital star subalgebras.  -/
NonUnitalStarSubalgebra.iSupLift : {R : Type u} →
  {A : Type v} →
    {B : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : NonUnitalSemiring A] →
          [inst_2 : StarRing A] →
            [inst_3 : Module R A] →
              [inst_4 : NonUnitalSemiring B] →
                [inst_5 : StarRing B] →
                  [inst_6 : Module R B] →
                    {ι : Type u_1} →
                      [inst_7 : StarRing R] →
                        [inst_8 : IsScalarTower R A A] →
                          [inst_9 : SMulCommClass R A A] →
                            [inst_10 : StarModule R A] →
                              [Nonempty ι] →
                                (K : ι → NonUnitalStarSubalgebra R A) →
                                  Directed (fun x1 x2 => x1 ≤ x2) K →
                                    (f : (i : ι) → ↥(K i) →⋆ₙₐ[R] B) →
                                      (∀ (i j : ι) (h : K i ≤ K j),
                                          f i = (f j).comp (NonUnitalStarSubalgebra.inclusion h)) →
                                        (T : NonUnitalStarSubalgebra R A) → T = iSup K → ↥T →⋆ₙₐ[R] B
-- Mathlib.LinearAlgebra.PerfectPairing.Basic
/-- Given a perfect pairing `p` between `M` and `N`, we say a pair of submodules `U` in `M` and
`V` in `N` are perfectly complementary w.r.t. `p` if their dual annihilators are complementary,
using `p` to identify `M` and `N` with dual spaces.  -/
LinearMap.IsPerfectCompl : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            [inst_3 : AddCommGroup N] →
              [inst_4 : Module R N] → (p : M →ₗ[R] N →ₗ[R] R) → [p.IsPerfPair] → Submodule R M → Submodule R N → Prop
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.smulWithZeroRight : {𝕜 : Type u_2} →
  {𝕝 : Type u_3} →
    {α : Type u_5} →
      [inst : Zero 𝕜] → [inst_1 : Zero 𝕝] → [SMulWithZero 𝕜 𝕝] → [inst_3 : LE α] → SMulWithZero 𝕜 (IncidenceAlgebra 𝕝 α)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
_private.Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr.0.Lean.Grind.CommRing.Poly.denoteExpr.denoteTerm : {M : Type → Type} →
  [Monad M] →
    [Lean.MonadError M] →
      [MonadLiftT Lean.MetaM M] →
        [Lean.Meta.Sym.Arith.MonadCanon M] →
          [Lean.Meta.Grind.Arith.CommRing.MonadRing M] → ℤ → Lean.Grind.CommRing.Mon → M Lean.Expr
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
/-- Tries to evaluate the polynomial `p` using the partial model/assignment built so far.
The result is `none` if the polynomial contains variables that have not been assigned.
 -/
Int.Internal.Linear.Poly.eval? : Int.Internal.Linear.Poly → Lean.Meta.Grind.GoalM (Option ℚ)
-- Mathlib.GroupTheory.Subgroup.Center
/-- The center of isomorphic groups are isomorphic.  -/
Subgroup.centerCongr : {G : Type u_1} →
  [inst : Group G] → {H : Type u_2} → [inst_1 : Group H] → G ≃* H → ↥(Subgroup.center G) ≃* ↥(Subgroup.center H)
-- Lean.Elab.MutualInductive
Lean.Elab.Command.PreElabHeaderResult.numParams : Lean.Elab.Command.PreElabHeaderResult → ℕ
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.rightExtensionEquivalenceOfIso₂.eq_1 : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (L : CategoryTheory.Functor C D) {F F' : CategoryTheory.Functor C H} (iso₂ : F ≅ F'),
  L.rightExtensionEquivalenceOfIso₂ iso₂ = CategoryTheory.CostructuredArrow.mapIso iso₂
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
SubMulAction.ofStabilizer.isMultiplyPretransitive_iff_of_conj : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {n : ℕ} {a b : α} {g : G},
  b = g • a →
    (MulAction.IsMultiplyPretransitive (↥(MulAction.stabilizer G a)) (↥(SubMulAction.ofStabilizer G a)) n ↔
      MulAction.IsMultiplyPretransitive (↥(MulAction.stabilizer G b)) (↥(SubMulAction.ofStabilizer G b)) n)
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_dvd_left_split_dvd1_cert.eq_1 : ∀ (p₁ p' : Int.Internal.Linear.Poly) (a k : ℤ),
  Int.Internal.Linear.cooper_dvd_left_split_dvd1_cert p₁ p' a k =
    (a.beq' p₁.leadCoeff).and' (p'.beq' (p₁.tail.addConst_k k))