mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
_private.Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol.0.ZMod.χ₈.match_1.eq_6 : ∀ (motive : ZMod 8 → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 2) (h_3 : Unit → motive 4)
  (h_4 : Unit → motive 6) (h_5 : Unit → motive 1) (h_6 : Unit → motive 7) (h_7 : Unit → motive 3)
  (h_8 : Unit → motive 5),
  (match 7 with
    | 0 => h_1 ()
    | 2 => h_2 ()
    | 4 => h_3 ()
    | 6 => h_4 ()
    | 1 => h_5 ()
    | 7 => h_6 ()
    | 3 => h_7 ()
    | 5 => h_8 ()) =
    h_6 ()
-- Mathlib.Algebra.Star.MonoidHom
StarMulEquiv.instEquivLike : {A : Type u_2} →
  {B : Type u_3} → [inst : Mul A] → [inst_1 : Mul B] → [inst_2 : Star A] → [inst_3 : Star B] → EquivLike (A ≃⋆* B) A B
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
/-- Given a locally-full and cover-dense functor `G` and a natural transformation of sheaves
`α : ℱ ⟶ ℱ'`, if the pullback of `α` along `G` is iso, then `α` is also iso.
 -/
CategoryTheory.Functor.IsCoverDense.iso_of_restrict_iso : ∀ {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] {K : CategoryTheory.GrothendieckTopology D} {A : Type u_4}
  [inst_2 : CategoryTheory.Category.{v_4, u_4} A] {G : CategoryTheory.Functor C D} [G.IsCoverDense K]
  [G.IsLocallyFull K] {ℱ ℱ' : CategoryTheory.Sheaf K A} (α : ℱ ⟶ ℱ'),
  CategoryTheory.IsIso (G.op.whiskerLeft α.hom) → CategoryTheory.IsIso α
-- LeanSearchClient.Syntax
LeanSearchClient.SearchServer.mk : String →
  String →
    String →
      (String → ℕ → Lean.MetaM (Array LeanSearchClient.SearchResult)) → Lean.CoreM ℕ → LeanSearchClient.SearchServer
-- Mathlib.CategoryTheory.ConnectedComponents
CategoryTheory.instInhabitedConnectedComponents : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] → [Inhabited J] → Inhabited (CategoryTheory.ConnectedComponents J)
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.zero_add : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  (x : CommRingCat.Colimits.Prequotient F),
  CommRingCat.Colimits.Relation F (CommRingCat.Colimits.Prequotient.zero.add x) x
-- Mathlib.Algebra.Ring.Defs
Ring.zsmul_zero' : ∀ {R : Type u} [self : Ring R] (a : R), 0 • a = 0
-- Mathlib.Data.Int.ModEq
AddCommGroup.intCast_modEq_intCast : ∀ {G : Type u_1} [inst : AddCommGroupWithOne G] [CharZero G] {a b z : ℤ}, ↑a ≡ ↑b [PMOD ↑z] ↔ a ≡ b [PMOD z]
-- Mathlib.Algebra.Group.Units.Defs
IsUnit.mul_left_iff : ∀ {M : Type u_1} [inst : Monoid M] {a b : M}, IsUnit a → (IsUnit (a * b) ↔ IsUnit b)
-- Init.Control.Lawful.MonadAttach.Instances
_private.Init.Control.Lawful.MonadAttach.Instances.0.EStateM.instMonadAttach.match_1.eq_2 : ∀ {ε σ α : Type u_1} (motive : EStateM.Result ε σ α → Sort u_2) (e : ε) (s' : σ)
  (h_1 :
    (a : α) → (s'_1 : σ) → EStateM.Result.error e s' = EStateM.Result.ok a s'_1 → motive (EStateM.Result.ok a s'_1))
  (h_2 :
    (e_1 : ε) →
      (s'_1 : σ) → EStateM.Result.error e s' = EStateM.Result.error e_1 s'_1 → motive (EStateM.Result.error e_1 s'_1)),
  (match h : EStateM.Result.error e s' with
    | EStateM.Result.ok a s'_1 => h_1 a s'_1 h
    | EStateM.Result.error e_1 s'_1 => h_2 e_1 s'_1 h) =
    h_2 e s' ⋯
-- Mathlib.Analysis.Seminorm
Seminorm.closedBall_smul_ball : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  (p : Seminorm 𝕜 E) {r₁ : ℝ}, r₁ ≠ 0 → ∀ (r₂ : ℝ), Metric.closedBall 0 r₁ • p.ball 0 r₂ ⊆ p.ball 0 (r₁ * r₂)
-- Mathlib.Combinatorics.KatonaCircle
Numbering.instDecidableIsPrefix : {X : Type u_1} → [inst : Fintype X] → {f : Numbering X} → {s : Finset X} → [DecidableEq X] → Decidable (f.IsPrefix s)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.lit.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (value : Lean.Compiler.LCNF.LitValue),
  sizeOf (Lean.Compiler.LCNF.LetValue.lit value) = 1 + sizeOf value
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ωScottContinuous.isLUB : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β] {f : α → β}
  {c : OmegaCompletePartialOrder.Chain α} (hf : OmegaCompletePartialOrder.ωScottContinuous f),
  IsLUB (Set.range ⇑(c.map { toFun := f, monotone' := ⋯ })) (f (OmegaCompletePartialOrder.ωSup c))
-- Mathlib.Algebra.Group.Defs
nsmulRec'_add_comm : ∀ {M : Type u_2} [inst : AddSemigroup M] [inst_1 : Zero M] {k : ℕ},
  k ≠ 0 → ∀ (m : M), m + nsmulRec' k m = nsmulRec' k m + m
-- Mathlib.Algebra.Category.Grp.LeftExactFunctor
/-- Implementation, see `leftExactFunctorForgetEquivalence`.  -/
AddCommGrpCat.leftExactFunctorForgetEquivalence.inverseAux : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [CategoryTheory.Limits.HasFiniteBiproducts C] →
        CategoryTheory.Functor (C ⥤ₗ Type v) (CategoryTheory.Functor C AddCommGrpCat)
-- Mathlib.Analysis.CStarAlgebra.Module.Constructions
_private.Mathlib.Analysis.CStarAlgebra.Module.Constructions.0.WithCStarModule.uniformity_prod_eq_aux : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] {E : Type u_2} {F : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : Module ℂ E] [inst_4 : SMul A E] [inst_5 : NormedAddCommGroup F]
  [inst_6 : Module ℂ F] [inst_7 : SMul A F] [inst_8 : CStarModule A E] [inst_9 : CStarModule A F]
  [inst_10 : StarOrderedRing A], uniformity (WithCStarModule A (E × F)) = uniformity (WithCStarModule A (E × F))
-- Lean.Elab.Quotation
/-- Check whether `stx` has unused alternatives, and remove the auxiliary `alt_idx` markers from it (see `markRhss`).
The parameter `alts` provides position information for alternatives.
`altIdxMap` and `ignoreIfUnused` are the map and set built using `markRhss`.
 -/
_private.Lean.Elab.Quotation.0.Lean.Elab.Term.Quotation.checkUnusedAlts : Lean.Syntax → Array Lean.Syntax → Lean.NameMap ℕ → Lean.Elab.Term.Quotation.IdxSet → Lean.Elab.TermElabM Lean.Syntax
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.coe_prod : ∀ {α : Type u} {R : Type u_2} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace R] {ι : Type u_3} (s : Finset ι)
  [inst_2 : CommMonoid R] [inst_3 : BoundedMul R] [inst_4 : ContinuousMul R] (f : ι → BoundedContinuousFunction α R),
  ⇑(∏ i ∈ s, f i) = ∏ i ∈ s, ⇑(f i)
-- Init.Data.UInt.Lemmas
UInt32.toNat_div : ∀ (a b : UInt32), (a / b).toNat = a.toNat / b.toNat
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.contains_unitOfList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k : α},
  (Std.HashMap.Raw.unitOfList l).contains k = l.contains k
-- Mathlib.Analysis.Normed.Ring.Basic
NonUnitalSeminormedRing.toPseudoMetricSpace : {α : Type u_5} → [self : NonUnitalSeminormedRing α] → PseudoMetricSpace α
-- Mathlib.Algebra.Homology.DerivedCategory.Plus
DerivedCategory.Plus.Qh_map_bijective_of_isKInjective : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (K L : HomotopyCategory.Plus C),
  CochainComplex.IsKInjective L.obj.as → Function.Bijective DerivedCategory.Plus.Qh.map
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnModule.SMulCommClass : ∀ {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_5} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ]
  [IsOrderedCancelAddMonoid Γ] [inst_3 : PartialOrder Γ'] [inst_4 : AddAction Γ Γ'] [inst_5 : IsOrderedCancelVAdd Γ Γ']
  [inst_6 : AddCommMonoid V] [inst_7 : CommSemiring R] [inst_8 : Module R V],
  SMulCommClass R (HahnSeries Γ R) (HahnModule Γ' R V)
-- Mathlib.Order.Basic
Pi.compl_def : ∀ {ι : Type u_1} {π : ι → Type u_4} [inst : (i : ι) → Compl (π i)] (x : (i : ι) → π i), xᶜ = fun i => (x i)ᶜ
-- Init.Data.Range.Polymorphic.Basic
/-- If the smallest value in the range is beyond the upper bound, the size is zero.  -/
Std.Rxc.LawfulHasSize.size_eq_zero_of_not_le : ∀ {α : Type u} {inst : LE α} {inst_1 : Std.PRange.UpwardEnumerable α} {inst_2 : Std.Rxc.HasSize α}
  [self : Std.Rxc.LawfulHasSize α] (lo hi : α), ¬lo ≤ hi → Std.Rxc.HasSize.size lo hi = 0
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.CoextendScalars.ext : ∀ {R : Type u₁} {S : Type u₂} [inst : Ring R] [inst_1 : Ring S] {f : R →+* S} {M : ModuleCat R}
  {g g' : ↑((ModuleCat.coextendScalars f).obj M)},
  (ModuleCat.CoextendScalars.equiv f M) g = (ModuleCat.CoextendScalars.equiv f M) g' → g = g'
-- Mathlib.Order.CompleteLattice.PiLex
_private.Mathlib.Order.CompleteLattice.PiLex.0.Pi.Lex.inf.eq_1 : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : LinearOrder ι] [inst_1 : (i : ι) → CompleteLinearOrder (α i)]
  [inst_2 : WellFoundedLT ι] (s : Set (Lex ((i : ι) → (fun i => α i) i))) (i : ι), Pi.Lex.inf✝ s i = ⨅ e, ↑e i
-- Mathlib.Topology.MetricSpace.Gluing
Metric.toGlue_commute : ∀ {X : Type u} {Y : Type v} {Z : Type w} [inst : Nonempty Z] [inst_1 : MetricSpace Z] [inst_2 : MetricSpace X]
  [inst_3 : MetricSpace Y] {Φ : Z → X} {Ψ : Z → Y} (hΦ : Isometry Φ) (hΨ : Isometry Ψ),
  Metric.toGlueL hΦ hΨ ∘ Φ = Metric.toGlueR hΦ hΨ ∘ Ψ
-- Mathlib.Algebra.MonoidAlgebra.Module
AddMonoidAlgebra.coeff_supportedEquivFinsupp_symm_apply_coe_support_val : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Module R S]
  (s : Set M) (a : ↑s →₀ S),
  (↑((AddMonoidAlgebra.supportedEquivFinsupp s).symm a)).coeff.support.val = Multiset.map Subtype.val a.support.val
-- Mathlib.Geometry.Manifold.IsManifold.Basic
/-- A vector space is a model with corners, denoted as `𝓘(𝕜, E)` within the `Manifold` namespace.  -/
modelWithCornersSelf : (𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    (E : Type u_2) → [inst_1 : NormedAddCommGroup E] → [inst_2 : NormedSpace 𝕜 E] → ModelWithCorners 𝕜 E E
-- Mathlib.Algebra.Homology.ShortComplex.Basic
/-- The opposite `ShortComplex` in `Cᵒᵖ` associated to a short complex in `C`.  -/
CategoryTheory.ShortComplex.op : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      CategoryTheory.ShortComplex C → CategoryTheory.ShortComplex Cᵒᵖ
-- Init.Data.Int.Basic
Int.cast_eq : ∀ (x : ℤ), ↑x = x
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.ToIntInfo.range : Lean.Meta.Grind.Arith.Cutsat.ToIntInfo → Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.coeff_zero : ∀ {R : Type u} [inst : Semiring R] (n : ℕ), Polynomial.coeff 0 n = 0
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- **Alias** of `Submodule.norm_orthogonalProjectionOnto`.

---

The operator norm of the orthogonal projection onto a nontrivial subspace is `1`.  -/
Submodule.norm_orthogonalProjection : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection], K ≠ ⊥ → ‖K.orthogonalProjectionOnto‖ = 1
-- Mathlib.Data.Part
Part.none.eq_1 : ∀ {α : Type u_1}, Part.none = { Dom := False, get := fun t => False.rec (fun x => α) t }
-- Mathlib.GroupTheory.Congruence.Hom
/-- The definition of the congruence relation defined by a monoid homomorphism's kernel.  -/
Con.ker_rel : ∀ {M : Type u_1} {N : Type u_2} {F : Type u_4} [inst : Mul M] [inst_1 : Mul N] [inst_2 : FunLike F M N]
  [inst_3 : MulHomClass F M N] (f : F) {x y : M}, (Con.ker f) x y ↔ f x = f y
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.vsub_iInter₂_subset : ∀ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [inst : VSub α β] (s : Set β)
  (t : (i : ι) → κ i → Set β), s -ᵥ ⋂ i, ⋂ j, t i j ⊆ ⋂ i, ⋂ j, s -ᵥ t i j
-- Mathlib.CategoryTheory.Filtered.Small
_private.Mathlib.CategoryTheory.Filtered.Small.0.CategoryTheory.IsCofiltered.CofilteredClosureSmall.InductiveStep.min.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {n : ℕ} {X : (k : ℕ) → k < n → (t : Type (max v w)) × (t → C)}
  {k k' : ℕ} (hk : k < n) (hk' : k' < n) (a : (X k hk).fst) (a_1 : (X k' hk').fst) (k_1 k'_1 : ℕ) (hk_1 : k_1 < n)
  (hk'_1 : k'_1 < n) (a_2 : (X k_1 hk_1).fst) (a_3 : (X k'_1 hk'_1).fst),
  (CategoryTheory.IsCofiltered.CofilteredClosureSmall.InductiveStep.min✝ hk hk' a a_1 =
      CategoryTheory.IsCofiltered.CofilteredClosureSmall.InductiveStep.min✝ hk_1 hk'_1 a_2 a_3) =
    (k = k_1 ∧ k' = k'_1 ∧ a ≍ a_2 ∧ a_1 ≍ a_3)
-- Mathlib.ModelTheory.Algebra.Ring.Basic
FirstOrder.instDecidableEqRingFunc.decEq : {a : ℕ} → (x x_1 : FirstOrder.ringFunc a) → Decidable (x = x_1)
-- Lean.Meta.Tactic.Grind.Types
/-- Congruence theorems generated so far. Recall that for constant symbols
we rely on the reserved name feature (i.e., `mkHCongrWithArityForConst?`).
Remark: we currently do not reuse congruence theorems
 -/
Lean.Meta.Grind.State.congrThms : Lean.Meta.Grind.State → Lean.PHashMap Lean.Meta.Grind.CongrTheoremCacheKey Lean.Meta.CongrTheorem
-- Mathlib.Algebra.BigOperators.Associated
/-- Let x, y ∈ M₀. If x * y can be written as a product of units and prime elements, then x can be
written as a product of units and prime elements.  -/
divisor_closure_eq_closure : ∀ {M₀ : Type u_3} [inst : CommMonoidWithZero M₀] [IsCancelMulZero M₀] (x y : M₀),
  x * y ∈ Submonoid.closure {r | IsUnit r ∨ Prime r} → x ∈ Submonoid.closure {r | IsUnit r ∨ Prime r}
-- Mathlib.Geometry.Diffeology.Basic
DiffeologicalSpace.toPlots_inf : ∀ {X : Type u_1} (d₁ d₂ : DiffeologicalSpace X), (d₁ ⊓ d₂).toPlots = d₁.toPlots ∩ d₂.toPlots
-- Mathlib.Order.OrdContinuous
/-- A function `f` between preorders is right order continuous if it preserves all infima of
nonempty sets.  We define it using `IsGLB` instead of `sInf` so that the proof works both for
complete lattices and conditionally complete lattices.  -/
RightOrdContinuous : {α : Type u} → {β : Type v} → [Preorder α] → [Preorder β] → (α → β) → Prop
-- Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Asymptotics.isLittleO_pow_pow_cobounded_of_lt : ∀ {R : Type u_1} [inst : NormedRing R] [NormMulClass R] {p q : ℕ},
  p < q → (fun x => x ^ p) =o[Bornology.cobounded R] fun x => x ^ q
-- Init.Data.UInt.Lemmas
UInt16.toUSize_ofNatClamp_of_lt : ∀ {n : ℕ} (hn : n < UInt16.size), (UInt16.ofNatClamp n).toUSize = USize.ofNatLT n ⋯
-- Batteries.Tactic.Trans
/-- Constant name for transitive relation.  -/
Batteries.Tactic.TransRelation.implies : Lean.Name → Lean.BinderInfo → Batteries.Tactic.TransRelation
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ofEq.sizeOf_spec : ∀ (a b : Lean.Expr) (la lb : Lean.Meta.Grind.Arith.Linear.LinExpr),
  sizeOf (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ofEq a b la lb) = 1 + sizeOf a + sizeOf b + sizeOf la + sizeOf lb
-- Lean.Declaration
Lean.instInhabitedDefinitionSafety.default : Lean.DefinitionSafety
-- Mathlib.RepresentationTheory.Tannaka
TannakaDuality.FiniteGroup.equivApp_inv : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (g : G) (X : FDRep k G),
  (TannakaDuality.FiniteGroup.equivApp g X).inv = CategoryTheory.InducedCategory.homMk (ModuleCat.ofHom (X.ρ g⁻¹))
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
LieRinehartSubalgebra.mem_mk_iff : ∀ {A : Type u_1} {L : Type u_2} [inst : CommRing A] [inst_1 : LieRing L] [inst_2 : Module A L] (S : Set L)
  (h₁ : ∀ {a b : L}, a ∈ S → b ∈ S → a + b ∈ S) (h₂ : S 0)
  (h₃ :
    ∀ (c : A) {x : L},
      x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrier →
        c • x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrier)
  (h₄ :
    ∀ {a b : L},
      a ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier →
        b ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier →
          ⁅a, b⁆ ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier)
  {x : L}, x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃, lie_mem' := h₄ } ↔ x ∈ S
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.sdiv_udiv : ∀ {w : ℕ} (x y : BitVec w),
  x.sdiv y =
    bif x.getLsbD (w - 1) then bif y.getLsbD (w - 1) then -x / -y else -(-x / y)
    else bif y.getLsbD (w - 1) then -(x / -y) else x / y
-- Mathlib.RingTheory.QuotSMulTop
QuotSMulTop.equivQuotTensor_naturality : ∀ {R : Type u_2} [inst : CommRing R] (r : R) {M : Type u_1} {M' : Type u_3} [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup M'] [inst_4 : Module R M'] (f : M →ₗ[R] M'),
  ↑(QuotSMulTop.equivQuotTensor r M') ∘ₗ (QuotSMulTop.map r) f =
    LinearMap.lTensor (R ⧸ Ideal.span {r}) f ∘ₗ ↑(QuotSMulTop.equivQuotTensor r M)
-- Mathlib.Topology.Algebra.Monoid.Defs
ContinuousOn.add : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Add M] [ContinuousAdd M] {X : Type u_2}
  [inst_3 : TopologicalSpace X] {f g : X → M} {s : Set X}, ContinuousOn f s → ContinuousOn g s → ContinuousOn (f + g) s
-- Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
CategoryTheory.Triangulated.TStructure.triangleω₁δ_obj_mor₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : CategoryTheory.IsTriangulated C] (a b c : EInt) (hab : a ≤ b)
  (hbc : b ≤ c) (j : C),
  ((t.triangleω₁δ a b c hab hbc).obj j).mor₂ =
    (t.eTruncGE.map (CategoryTheory.homOfLE hab)).app ((t.eTruncLT.obj c).obj j)
-- Mathlib.Order.Atoms
isAtomistic_dual_iff_isCoatomistic : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderTop α], IsAtomistic αᵒᵈ ↔ IsCoatomistic α
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.Quotient.lift_map_functor_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (r : HomRel C) {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D)
  (H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂) {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.Quotient.lift r F H).map ((CategoryTheory.Quotient.functor r).map f) = F.map f
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.extendId_inv_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (s : CategoryTheory.Limits.Cone F),
  s.extendId.inv.hom = CategoryTheory.CategoryStruct.id s.pt
-- Mathlib.CategoryTheory.Sites.Subcanonical
CategoryTheory.GrothendieckTopology.yonedaOpCompCoyoneda_hom_app_app_hom_apply_down : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] (X : Cᵒᵖ) (X_1 : CategoryTheory.Sheaf J (Type v))
  (a : ((J.yoneda.op.comp CategoryTheory.coyoneda).obj X).obj X_1),
  ((CategoryTheory.ConcreteCategory.hom ((J.yonedaOpCompCoyoneda.hom.app X).app X_1)) a).down =
    CategoryTheory.yonedaEquiv
      ((CategoryTheory.CategoryStruct.comp
            ((CategoryTheory.sheafToPresheafCompCoyonedaCompWhiskeringLeftSheafToPresheaf.inv.app
                  (Opposite.op (J.yoneda.obj (Opposite.unop X)))).app
              X_1)
            (TypeCat.ofHom fun g =>
              CategoryTheory.CategoryStruct.comp (J.yonedaCompSheafToPresheaf.inv.app (Opposite.unop X)) g)).hom'
        a)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_div_Iic : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b : α),
  (fun x => a / x) ⁻¹' Set.Iic b = Set.Ici (a / b)
-- Mathlib.CategoryTheory.Galois.Topology
/-- We put the discrete topology on `F.obj X`.  -/
CategoryTheory.PreGaloisCategory.instTopologicalSpaceObjFiniteObjFintypeCat : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    (F : CategoryTheory.Functor C FintypeCat) → (X : C) → TopologicalSpace (F.obj X).obj
-- Mathlib.MeasureTheory.Constructions.Pi
/-- **Alias** of `MeasureTheory.Measure.pi_nullSingletonClass'`. -/
MeasureTheory.Measure.pi_noAtoms' : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  {μ : (i : ι) → MeasureTheory.Measure (α i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] [h : Nonempty ι]
  [∀ (i : ι), MeasureTheory.NullSingletonClass (μ i)], MeasureTheory.NullSingletonClass (MeasureTheory.Measure.pi μ)
-- Mathlib.NumberTheory.Height.Basic
/-- Extension for the `positivity` tactic: `Height.logHeight` is always nonnegative.  -/
Mathlib.Meta.Positivity.evalLogHeight : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Analysis.Convex.Between
/-- **Alias** of the reverse direction of `sbtw_add_const_iff`. -/
Sbtw.add_const : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] {x y z : V} (v : V), Sbtw R x y z → Sbtw R (x + v) (y + v) (z + v)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.le_maxKey?_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k km : α}
  (hc : k ∈ t), t.maxKey?.get ⋯ = km → (cmp k km).isLE = true
-- Mathlib.RingTheory.Regular.RegularSequence
/-- A simplified version of `IsRegular.recIterModByRegular` where the motive is
not allowed to depend on the proof of `IsRegular`.  -/
RingTheory.Sequence.IsRegular.ndrecIterModByRegular : {R : Type u_1} →
  [inst : CommRing R] →
    {motive : (M : Type v) → [inst_1 : AddCommGroup M] → [Module R M] → List R → Sort u_7} →
      ((M : Type v) → [inst_1 : AddCommGroup M] → [inst : Module R M] → [Nontrivial M] → motive M []) →
        ({M : Type v} →
            [inst_1 : AddCommGroup M] →
              [inst_2 : Module R M] →
                (r : R) →
                  (rs : List R) →
                    IsSMulRegular M r →
                      RingTheory.Sequence.IsRegular (QuotSMulTop r M) rs →
                        motive (QuotSMulTop r M) rs → motive M (r :: rs)) →
          {M : Type v} →
            [inst_1 : AddCommGroup M] →
              [inst_2 : Module R M] → {rs : List R} → RingTheory.Sequence.IsRegular M rs → motive M rs
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.RationalMap.mem_domain : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X.RationalMap Y} {x : ↥X},
  x ∈ f.domain ↔ ∃ g, x ∈ g.domain ∧ g.toRationalMap = f
-- Init.Data.List.Sublist
List.isPrefixOf_length_pos_nil : ∀ {α : Type u_1} [inst : BEq α] {l : List α}, 0 < l.length → l.isPrefixOf [] = false
-- Std.Do.SPred.SPred
/-- Negation in `SPred`: states that do not satisfy `P` satisfy `spred(¬ P)`.  -/
Std.Do.SPred.not : {σs : List (Type u)} → Std.Do.SPred σs → Std.Do.SPred σs
-- Mathlib.Tactic.Determinant.Bird.Meta
Mathlib.Tactic.Determinant.ReifiedBirdDet.mk.inj : ∀ {u : Lean.Level} {α : Q(Type u)} {rα : Q(CommRing «$α»)} {ctx : Mathlib.Tactic.Determinant.Ctx rα} {u_1 : Lean.Level}
  {α_1 : Q(Type u_1)} {rα_1 : Q(CommRing «$α_1»)} {ctx_1 : Mathlib.Tactic.Determinant.Ctx rα_1},
  { u := u, α := α, rα := rα, ctx := ctx } = { u := u_1, α := α_1, rα := rα_1, ctx := ctx_1 } →
    u = u_1 ∧ α = α_1 ∧ rα = rα_1 ∧ ctx ≍ ctx_1
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.lmul'_comp_map : ∀ {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : CommSemiring S] [inst_4 : Algebra R A] [inst_5 : Algebra R B] [inst_6 : Algebra R S]
  (f : A →ₐ[R] S) (g : B →ₐ[R] S),
  (Algebra.TensorProduct.lmul' R).comp (Algebra.TensorProduct.map f g) = Algebra.TensorProduct.lift f g ⋯
-- Init.Data.BitVec.Lemmas
BitVec.ule_eq_decide : ∀ {w : ℕ} {x y : BitVec w}, x.ule y = decide (x.toNat ≤ y.toNat)
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
UniqueMDiffWithinAt.inter : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {x : M} {s t : Set M},
  UniqueMDiffAt[s] x → t ∈ nhds x → UniqueMDiffAt[s ∩ t] x
-- Mathlib.Logic.Equiv.Basic
Equiv.piComm_symm : ∀ {α : Sort u_1} {β : Sort u_4} {φ : α → β → Sort u_9}, (Equiv.piComm φ).symm = Equiv.piComm (Function.swap φ)