mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.Congruence.Defs
VAddCon.mk.injEq : ∀ {S : Type u_2} {M : Type u_3} [inst : VAdd S M] (toSetoid : Setoid M)
  (vadd : ∀ (s : S) {x y : M}, toSetoid x y → toSetoid (s +ᵥ x) (s +ᵥ y)) (toSetoid_1 : Setoid M)
  (vadd_1 : ∀ (s : S) {x y : M}, toSetoid_1 x y → toSetoid_1 (s +ᵥ x) (s +ᵥ y)),
  ({ toSetoid := toSetoid, vadd := vadd } = { toSetoid := toSetoid_1, vadd := vadd_1 }) = (toSetoid = toSetoid_1)
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
pow_succ_padicValNat_not_dvd : ∀ {p n : ℕ} [hp : Fact (Nat.Prime p)], n ≠ 0 → ¬p ^ (padicValNat p n + 1) ∣ n
-- Batteries.Data.Array.Scan
Subarray.scanr.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (f : α → β → β) (init : β) (as : Subarray α),
  Subarray.scanr f init as = Array.scanr f init as.array as.start as.stop
-- Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
_private.Lean.Meta.Tactic.Grind.Arith.CommRing.RingId.0.Lean.Meta.Grind.Arith.CommRing.getNonCommRingId?.go? : Lean.Expr → Lean.Meta.Grind.GoalM (Option ℕ)
-- Aesop.RuleTac.Basic
Aesop.CasesTarget.patterns.sizeOf_spec : ∀ (patterns : Array Aesop.CasesPattern), sizeOf (Aesop.CasesTarget.patterns patterns) = 1 + sizeOf patterns
-- Mathlib.LinearAlgebra.Ray
/-- If a vector `v₂` is on the same ray as a nonzero vector `v₁`, then it is equal to `c • v₁` for
some nonnegative `c`.  -/
SameRay.exists_nonneg_left : ∀ {R : Type u_1} [inst : Field R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {x y : M}, SameRay R x y → x ≠ 0 → ∃ r, 0 ≤ r ∧ r • x = y
-- Mathlib.LinearAlgebra.TensorProduct.DirectLimit
TensorProduct.directLimitLeft_tmul_of : ∀ {R : Type u_1} [inst : CommSemiring R] {ι : Type u_2} [inst_1 : DecidableEq ι] [inst_2 : Preorder ι]
  {G : ι → Type u_3} [inst_3 : (i : ι) → AddCommMonoid (G i)] [inst_4 : (i : ι) → Module R (G i)]
  (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) (M : Type u_4) [inst_5 : AddCommMonoid M] [inst_6 : Module R M] {i : ι}
  (g : G i) (m : M),
  (TensorProduct.directLimitLeft f M) ((Module.DirectLimit.of R ι G f i) g ⊗ₜ[R] m) =
    (Module.DirectLimit.of R ι (fun i => TensorProduct R (G i) M) (fun i j h => LinearMap.rTensor M (f i j h)) i)
      (g ⊗ₜ[R] m)
-- Mathlib.Algebra.Star.Basic
commute_star_star : ∀ {R : Type u} [inst : Mul R] [inst_1 : StarMul R] {x y : R}, Commute (star x) (star y) ↔ Commute x y
-- Mathlib.Data.Set.Finite.Lattice
Set.infinite_iUnion : ∀ {α : Type u} {ι : Type u_1} [Infinite ι] {s : ι → Set α}, Function.Injective s → (⋃ i, s i).Infinite
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.filterMap_equiv_filter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {f : α → β → Bool},
  (Std.TreeMap.filterMap (fun k => Option.guard fun v => f k v) t).Equiv (Std.TreeMap.filter f t)
-- Mathlib.Topology.Order.Basic
pi_Ioo_mem_nhds : ∀ {ι : Type u_1} {X : ι → Type u_2} [Finite ι] [inst : (i : ι) → LinearOrder (X i)]
  [inst_1 : (i : ι) → TopologicalSpace (X i)] [∀ (i : ι), OrderTopology (X i)] {a b x : (i : ι) → X i} [Nonempty ι],
  (∀ (i : ι), a i < x i) → (∀ (i : ι), x i < b i) → Set.Ioo a b ∈ nhds x
-- Mathlib.Order.RelIso.Basic
RelIso.symm_apply_rel : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) {x : β} {y : α},
  r (e.symm x) y ↔ s x (e y)
-- Init.Grind.AC
Lean.Grind.AC.Expr.op : Lean.Grind.AC.Expr → Lean.Grind.AC.Expr → Lean.Grind.AC.Expr
-- Mathlib.Analysis.InnerProductSpace.Laplacian
/-- If two functions agree in a neighborhood of a point, then so do their Laplacians.
 -/
InnerProductSpace.laplacianWithin_congr_nhdsWithin : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f₁ f₂ : E → F} {x : E} {s : Set E},
  f₁ =ᶠ[nhdsWithin x s] f₂ →
    UniqueDiffOn ℝ s → InnerProductSpace.laplacianWithin f₁ s =ᶠ[nhdsWithin x s] InnerProductSpace.laplacianWithin f₂ s
-- Mathlib.LinearAlgebra.QuadraticForm.Isometry
QuadraticMap.Isometry.mk : {R : Type u_1} →
  {M₁ : Type u_3} →
    {M₂ : Type u_4} →
      {N : Type u_7} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M₁] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : AddCommMonoid N] →
                [inst_4 : Module R M₁] →
                  [inst_5 : Module R M₂] →
                    [inst_6 : Module R N] →
                      {Q₁ : QuadraticMap R M₁ N} →
                        {Q₂ : QuadraticMap R M₂ N} →
                          (toLinearMap : M₁ →ₗ[R] M₂) → (∀ (m : M₁), Q₂ (toLinearMap.toFun m) = Q₁ m) → Q₁ →qᵢ Q₂
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.superpose.sizeOf_spec : ∀ (p s c : Lean.Grind.AC.Seq) (c₁ c₂ : Lean.Meta.Grind.AC.EqCnstr),
  sizeOf (Lean.Meta.Grind.AC.EqCnstrProof.superpose p s c c₁ c₂) =
    1 + sizeOf p + sizeOf s + sizeOf c + sizeOf c₁ + sizeOf c₂
-- Mathlib.Analysis.BoxIntegral.Partition.Split
/-- Let `s` be a finite set of boxes in `ℝⁿ = ι → ℝ`. Then there exists a finite set `t₀` of
hyperplanes (namely, the set of all hyperfaces of boxes in `s`) such that for any `t ⊇ t₀`
and any box `I` in `ℝⁿ` the following holds. The hyperplanes from `t` split `I` into subboxes.
Let `J'` be one of them, and let `J` be one of the boxes in `s`. If these boxes have a nonempty
intersection, then `J' ≤ J`.  -/
BoxIntegral.Prepartition.eventually_not_disjoint_imp_le_of_mem_splitMany : ∀ {ι : Type u_1} [Finite ι] (s : Finset (BoxIntegral.Box ι)),
  ∀ᶠ (t : Finset (ι × ℝ)) in Filter.atTop,
    ∀ (I J : BoxIntegral.Box ι), J ∈ s → ∀ J' ∈ BoxIntegral.Prepartition.splitMany I t, ¬Disjoint ↑J ↑J' → J' ≤ J
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.add : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Add ι] [inst_1 : LinearOrder ι]
  [CanonicallyOrderedAdd ι] [Countable ι] [inst_4 : TopologicalSpace ι] [OrderTopology ι]
  {f : MeasureTheory.Filtration ι m} {τ π : Ω → WithTop ι},
  MeasureTheory.IsStoppingTime f τ → MeasureTheory.IsStoppingTime f π → MeasureTheory.IsStoppingTime f (τ + π)
-- Mathlib.Order.SupIndep
Finset.supIndep_attach : ∀ {α : Type u_1} {ι : Type u_3} [inst : Lattice α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α},
  (s.attach.SupIndep fun a => f ↑a) ↔ s.SupIndep f
-- Mathlib.Analysis.CStarAlgebra.Module.Defs
CStarModule.inner_smul_right_complex : ∀ {A : Type u_1} {E : Type u_2} {inst : NonUnitalSemiring A} {inst_1 : StarRing A} {inst_2 : Module ℂ A}
  {inst_3 : AddCommGroup E} {inst_4 : Module ℂ E} {inst_5 : PartialOrder A} {inst_6 : SMul A E} {inst_7 : Norm A}
  {inst_8 : Norm E} [self : CStarModule A E] {z : ℂ} {x y : E}, inner A x (z • y) = z • inner A x y
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.mapIso_inverse_obj_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T T' : D} {S : CategoryTheory.Functor C D} (i : T ≅ T')
  (X : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T')),
  ((CategoryTheory.CostructuredArrow.mapIso i).inverse.obj X).hom = CategoryTheory.CategoryStruct.comp X.hom i.inv
-- Mathlib.Probability.ProductMeasure
/-- Infinite product measure indexed by `ℕ`. This is an auxiliary construction, you should use
the generic product measure `Measure.infinitePi`.  -/
MeasureTheory.Measure.infinitePiNat : {X : ℕ → Type u_1} →
  {mX : (n : ℕ) → MeasurableSpace (X n)} →
    (μ : (n : ℕ) → MeasureTheory.Measure (X n)) →
      [hμ : ∀ (n : ℕ), MeasureTheory.IsProbabilityMeasure (μ n)] → MeasureTheory.Measure ((n : ℕ) → X n)
-- Aesop.Index.Basic
/-- Goal locations where the rule matched. The rule's `indexingMode`
determines which locations can be contained in this set. The array contains
no duplicates.  -/
Aesop.IndexMatchResult.locations : {α : Type} → Aesop.IndexMatchResult α → Array Aesop.IndexMatchLocation
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
MeasureTheory.abs_condExp_ae_le_condExp_abs : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] [inst_3 : Lattice E] [HasSolidNorm E] [IsOrderedAddMonoid E]
  [IsOrderedModule ℝ E] (f : α → E), |μ[f | m]| ≤ᵐ[μ] μ[|f| | m]
-- Mathlib.Algebra.Order.Interval.Finset.SuccPred
Finset.Ioo_sub_one_left_eq_Ioc : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : LocallyFiniteOrder α] [inst_3 : Sub α]
  [PredSubOrder α] [NoMinOrder α] (a b : α), Finset.Ioo (a - 1) b = Finset.Ico a b
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
ContinuousAt.arcsin : ∀ {X : Type u_1} [inst : TopologicalSpace X] {f : X → ℝ} {x : X},
  ContinuousAt f x → ContinuousAt (fun x => Real.arcsin (f x)) x
-- Mathlib.RingTheory.Localization.Finiteness
Module.Finite.instLocalizationLocalizedModule : ∀ {R : Type u} [inst : CommSemiring R] (S : Submonoid R) {M : Type w} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Finite R M], Module.Finite (Localization S) (LocalizedModule S M)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_eq_some_iff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α], t.WF → ∀ {k : α} {v : β k}, t.get? k = some v ↔ ∃ (h : k ∈ t), t.get k h = v
-- Mathlib.Topology.FiberBundle.Basic
FiberPrebundle.instMemTrivializationAtlasTrivializationOfMemPretrivializationAtlas : ∀ {B : Type u_2} {F : Type u_3} {E : B → Type u_5} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : (x : B) → TopologicalSpace (E x)] (a : FiberPrebundle F E)
  {e₀ : Bundle.Pretrivialization F Bundle.TotalSpace.proj} (he₀ : e₀ ∈ a.pretrivializationAtlas),
  MemTrivializationAtlas (a.trivializationOfMemPretrivializationAtlas he₀)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Real.borel_eq_generateFrom_Ioo_rat : borel ℝ = MeasurableSpace.generateFrom (⋃ a, ⋃ b, ⋃ (_ : a < b), {Set.Ioo ↑a ↑b})
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.instIntCastCauchy : {α : Type u_1} →
  [inst : Field α] →
    [inst_1 : LinearOrder α] →
      [inst_2 : IsStrictOrderedRing α] →
        {β : Type u_2} →
          [inst_3 : Ring β] → {abv : β → α} → [inst_4 : IsAbsoluteValue abv] → IntCast (CauSeq.Completion.Cauchy abv)
-- Mathlib.Combinatorics.Matroid.Minor.Delete
Matroid.delete_subset_ground : ∀ {α : Type u_1} (M : Matroid α) (D : Set α), (M.delete D).E ⊆ M.E
-- Lean.Expr
_private.Lean.Expr.0.Lean.Expr.betaRev.go : Array Lean.Expr → Bool → Bool → ℕ → Lean.Expr → ℕ → Lean.Expr
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
MeasurableSpace.comap_generateFrom : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set (Set β)},
  MeasurableSpace.comap f (MeasurableSpace.generateFrom s) = MeasurableSpace.generateFrom (Set.preimage f '' s)
-- Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
SchwartzMap.instFourierInvSMul : ∀ (𝕜 : Type u_1) [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℂ E]
  [inst_3 : NormedSpace 𝕜 E] [inst_4 : SMulCommClass ℂ 𝕜 E] {V : Type u_3} [inst_5 : NormedAddCommGroup V]
  [inst_6 : InnerProductSpace ℝ V] [inst_7 : FiniteDimensional ℝ V] [inst_8 : MeasurableSpace V]
  [inst_9 : BorelSpace V], FourierInvSMul 𝕜 (SchwartzMap V E) (SchwartzMap V E)
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.Option.isSome_dmap : ∀ {α : Type u} {β : Type v} {o : Option α} {f : (a : α) → o = some a → β},
  (Std.Internal.List.Option.dmap✝ o f).isSome = o.isSome
-- Mathlib.Algebra.Group.EvenFunction
Function.Even.const_smul : ∀ {α : Type u_1} {β : Type u_2} [inst : Neg α] {γ : Type u_3} {g : α → γ} [inst_1 : SMul β γ],
  Function.Even g → ∀ (r : β), Function.Even (r • g)
-- Mathlib.Topology.Algebra.NonUnitalAlgebra
NonUnitalAlgebra.elemental.isClosed : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] [inst_5 : TopologicalSpace A]
  [inst_6 : IsSemitopologicalSemiring A] [inst_7 : ContinuousConstSMul R A] (x : A),
  IsClosed ↑(NonUnitalAlgebra.elemental R x)
-- Mathlib.Analysis.Complex.Trigonometric
Real.tanh_neg : ∀ (x : ℝ), Real.tanh (-x) = -Real.tanh x
-- Mathlib.Order.Defs.LinearOrder
min_def : ∀ {α : Type u_1} [inst : LinearOrder α] (a b : α), min a b = if a ≤ b then a else b
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.contains_alter_of_not_compare_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k k' : α} {f : Option β → Option β}, ¬cmp k k' = Ordering.eq → (t.alter k f).contains k' = t.contains k'
-- Mathlib.Order.RelClasses
/-- Set notation form of `lt_of_eq_of_lt` -/
ssubset_of_eq_of_ssubset : ∀ {α : Type u_1} [UsesSetNotationForOrder α] {a b c : α} [inst : LT α], a = b → b ⊂ c → a ⊂ c
-- Mathlib.Combinatorics.SimpleGraph.Sum
/-- Disjoint sum of `G` and `H`.  -/
SimpleGraph.«term_⊕g_» : Lean.TrailingParserDescr
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.transEquiv_transEquiv : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : PartialEquiv α β) (f' : β ≃ γ) (f'' : γ ≃ δ),
  (e.transEquiv f').transEquiv f'' = e.transEquiv (f'.trans f'')
-- Std.Http.Test.Helpers
/-- Default config for server tests. Short lingering timeout, no Date header.
 -/
Std.Http.Internal.Test.defaultConfig : Std.Http.Config
-- Std.Data.DTreeMap.Internal.Lemmas
_private.Std.Data.DTreeMap.Internal.Lemmas.0.Std.DTreeMap.Internal.Impl.Const.get_insertMany_list.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (v : β) (h_1 : (v_1 : β) → some v = some v_1 → motive (some v_1))
  (h_2 : some v = none → motive none),
  (match w : some v with
    | some v_1 => h_1 v_1 w
    | none => h_2 w) =
    h_1 v ⋯
-- Mathlib.Data.ENNReal.BigOperators
ENNReal.prod_inv_distrib : ∀ {ι : Type u_1} {f : ι → ENNReal} {s : Finset ι},
  ((↑s).Pairwise fun i j => f i ≠ 0 ∨ f j ≠ ⊤) → (∏ i ∈ s, f i)⁻¹ = ∏ i ∈ s, (f i)⁻¹
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey?_erase_le_maxKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k km kme : α}
  (hkme : (t.erase k).maxKey? = some kme), t.maxKey?.get ⋯ = km → (cmp kme km).isLE = true
-- Batteries.Lean.Meta.Basic
/-- Solve a goal by synthesizing an instance.  -/
Lean.MVarId.synthInstance : Lean.MVarId → Lean.MetaM Unit
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
/-- If the scalar multiplication `(· • ·) : α → β → β` is distributive,
then so is `(· • ·) : α → Set β → Set β`.  -/
Set.distribSMulSet : {α : Type u_1} → {β : Type u_2} → [inst : AddZeroClass β] → [DistribSMul α β] → DistribSMul α (Set β)
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.precomp_obj : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} (c : B) (f : a ⟶ b) (x : b ⟶ c),
  (CategoryTheory.Bicategory.precomp c f).obj x = CategoryTheory.CategoryStruct.comp f x
-- Mathlib.Analysis.Calculus.FDeriv.Basic
fderivWithin_mem_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {t : Set E} {s : Set (E →L[𝕜] F)} {x : E},
  fderivWithin 𝕜 f t x ∈ s ↔
    DifferentiableWithinAt 𝕜 f t x ∧ fderivWithin 𝕜 f t x ∈ s ∨ ¬DifferentiableWithinAt 𝕜 f t x ∧ 0 ∈ s
-- Mathlib.Topology.Order.MonotoneConvergence
/-- proof that a monotone function tends to `𝓝 a` as `x → ∞`  -/
SupConvergenceClass.tendsto_coe_atTop_isLUB : ∀ {α : Type u_3} {inst : Preorder α} {inst_1 : TopologicalSpace α} [self : SupConvergenceClass α] (a : α) (s : Set α),
  IsLUB s a → Filter.Tendsto Subtype.val Filter.atTop (nhds a)
-- Mathlib.Data.Finset.Image
Finset.image_erase : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst_1 : DecidableEq α] {f : α → β},
  Function.Injective f → ∀ (s : Finset α) (a : α), Finset.image f (s.erase a) = (Finset.image f s).erase (f a)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get!_map : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Raw α (fun x => β) cmp}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [inst : Inhabited γ] {f : α → β → γ} {k : α},
  t.WF →
    Std.DTreeMap.Raw.Const.get! (Std.DTreeMap.Raw.map f t) k = (Option.map (f k) (Std.DTreeMap.Raw.Const.get? t k)).get!
-- Mathlib.Data.Set.Function
/-- If we have a commutative square

```
α --f--> β
|        |
p₁       p₂
|        |
\/       \/
γ --g--> δ
```

and `f` induces a bijection from `s : Set α` to `t : Set β`, then `g`
induces a bijection from the image of `s` to the image of `t`, as long as `g` is
is injective on the image of `s`.
 -/
Set.bijOn_image_image : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {s : Set α} {t : Set β} {f : α → β} {p₁ : α → γ}
  {p₂ : β → δ} {g : γ → δ},
  (∀ (a : α), p₂ (f a) = g (p₁ a)) → Set.BijOn f s t → Set.InjOn g (p₁ '' s) → Set.BijOn g (p₁ '' s) (p₂ '' t)
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.NonemptyCompacts.continuous_toCloseds : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : T2Space α], Continuous TopologicalSpace.NonemptyCompacts.toCloseds
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRight.go_denote_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {n w : ℕ} (aig : Std.Sat.AIG α) (distance : aig.RefVec n),
  ∀ curr ≤ n - 1,
    ∀ (acc : aig.RefVec w) (lhs : BitVec w) (rhs : BitVec n) (assign : α → Bool),
      (∀ (idx : ℕ) (hidx : idx < w),
          ⟦assign, { aig := aig, ref := acc.get idx hidx }⟧ = (lhs.ushiftRightRec rhs curr).getLsbD idx) →
        (∀ (idx : ℕ) (hidx : idx < n), ⟦assign, { aig := aig, ref := distance.get idx hidx }⟧ = rhs.getLsbD idx) →
          ∀ (idx : ℕ) (hidx : idx < w),
            ⟦assign,
                { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRight.go aig distance curr acc).aig,
                  ref :=
                    (Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRight.go aig distance curr acc).vec.get idx hidx }⟧ =
              (lhs.ushiftRightRec rhs (n - 1)).getLsbD idx
-- Init.Data.SInt.Basic
instAndOpInt32 : AndOp Int32
-- Init.Data.Array.Lemmas
Array.getElem?_ofFn : ∀ {n : ℕ} {α : Type u_1} {f : Fin n → α} {i : ℕ}, (Array.ofFn f)[i]? = if h : i < n then some (f ⟨i, h⟩) else none
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.left_inv : ∀ {𝕜 : 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) (x : H),
  ↑I.symm (↑I x) = x
-- Mathlib.MeasureTheory.Covering.Differentiation
/-- For almost every point `x`, sufficiently small sets in a Vitali family around `x` have positive
measure. (This is a nontrivial result, following from the covering property of Vitali families).  -/
VitaliFamily.ae_eventually_measure_pos : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (v : VitaliFamily μ) [SecondCountableTopology α], ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Polynomial.Chebyshev.eval_T_real_eq_neg_one_iff : ∀ {n : ℕ},
  n ≠ 0 →
    ∀ (x : ℝ), Polynomial.eval x (Polynomial.Chebyshev.T ℝ ↑n) = -1 ↔ ∃ k ≤ n, Odd k ∧ x = Real.cos (↑k * Real.pi / ↑n)
-- Init.Internal.Order.Basic
Lean.Order.instMonoBindStateT : ∀ {m : Type u_1 → Type u_2} {ρ : Type u_1} [inst : Monad m] [inst_1 : (α : Type u_1) → Lean.Order.PartialOrder (m α)]
  [Lean.Order.MonoBind m], Lean.Order.MonoBind (StateT ρ m)
-- Mathlib.Tactic.Ring.Compare
/-- `CommSemiring` implies `AddMonoidWithOne`.  -/
Mathlib.Tactic.Ring.addMonoidWithOneOfCommSemiring : (α : Type u_1) → [CommSemiring α] → AddMonoidWithOne α
-- Mathlib.RingTheory.HahnSeries.Lex
HahnSeries.finiteArchimedeanClassOrderIso.congr_simp : ∀ (Γ : Type u_1) (R : Type u_2) [inst : LinearOrder Γ] [inst_1 : LinearOrder R] [inst_2 : AddCommGroup R]
  [inst_3 : IsOrderedAddMonoid R] [inst_4 : Archimedean R] [inst_5 : Nontrivial R],
  HahnSeries.finiteArchimedeanClassOrderIso Γ R = HahnSeries.finiteArchimedeanClassOrderIso Γ R
-- Lean.Elab.Tactic.RCases
/-- The implementation of the `rintro` tactic. It takes a list of patterns `pats` and
an optional type ascription `ty?` and introduces the patterns, resulting in zero or more goals.
 -/
Lean.Elab.Tactic.RCases.rintro : Lean.TSyntaxArray `rintroPat → Option Lean.Term → Lean.MVarId → Lean.Elab.TermElabM (List Lean.MVarId)
-- Mathlib.Data.Prod.TProd
/-- A product of sets in `TProd α l`.  -/
Set.tprod : {ι : Type u} → {α : ι → Type v} → (l : List ι) → ((i : ι) → Set (α i)) → Set (List.TProd α l)
-- Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
IsPrimitiveRoot.subOnePowerBasis_dim : ∀ {n : ℕ} [inst : NeZero n] (K : Type u) {L : Type v} [inst_1 : Field K] [inst_2 : CommRing L] [inst_3 : IsDomain L]
  [inst_4 : Algebra K L] [inst_5 : IsCyclotomicExtension {n} K L] {ζ : L} (hζ : IsPrimitiveRoot ζ n),
  (IsPrimitiveRoot.subOnePowerBasis K hζ).dim = (minpoly K (ζ - 1)).natDegree
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- The spectral norm is submultiplicative.  -/
spectralNorm_mul : ∀ {K : Type u_2} [inst : NormedField K] {L : Type u_3} [inst_1 : Field L] [inst_2 : Algebra K L] [IsUltrametricDist K]
  {x y : L}, IsAlgebraic K x → IsAlgebraic K y → spectralNorm K L (x * y) ≤ spectralNorm K L x * spectralNorm K L y
-- Mathlib.Probability.Process.Adapted
MeasureTheory.isProgressive_const : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {β : Type u_3} {mi : MeasurableSpace ι}
  {mβ : MeasurableSpace β} (f : MeasureTheory.Filtration ι m) (b : β), MeasureTheory.IsProgressive f fun x x_1 => b
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Finsupp.range_linearCombination : ∀ {α : Type u_1} {M : Type u_2} (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {v : α → M}, (Finsupp.linearCombination R v).range = Submodule.span R (Set.range v)
-- Mathlib.CategoryTheory.Endomorphism
/-- `mulEquivEnd` as an isomorphism between endomorphism monoids.  -/
CategoryTheory.Functor.FullyFaithful.mulEquivEnd : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        {f : CategoryTheory.Functor C D} →
          f.FullyFaithful → (X : C) → CategoryTheory.End X ≃* CategoryTheory.End (f.obj X)
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- Given a functor `F` and an equivalence of categories `e` such that `e.functor` and `F ⋙ e.inverse`
are monoidal functors, `F` is monoidal as well.
 -/
CategoryTheory.Equivalence.monoidalOfPostcompInverse : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {E : Type u₃} →
              [inst_4 : CategoryTheory.Category.{v₃, u₃} E] →
                [inst_5 : CategoryTheory.MonoidalCategory E] →
                  (e : C ≌ D) →
                    (F : CategoryTheory.Functor E D) →
                      {F' : CategoryTheory.Functor E C} →
                        (F.comp e.inverse ≅ F') → [e.functor.Monoidal] → [F'.Monoidal] → F.Monoidal
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosDef.of_dotProduct_mulVec_pos : ∀ {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [inst_3 : Fintype n]
  {M : Matrix n n R}, M.IsHermitian → (∀ ⦃x : n → R⦄, x ≠ 0 → 0 < star x ⬝ᵥ M.mulVec x) → M.PosDef
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- Exactness of `L₀.X₂ ⟶ L₀.X₃ ⟶ L₃.X₁`.  -/
CategoryTheory.ShortComplex.SnakeInput.L₁'_exact : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), S.L₁'.Exact