mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.OrderOfElement
/-- If `x^n = 1`, but `x^(n/p) ≠ 1` for all prime factors `p` of `n`,
then `x` has order `n` in `G`.  -/
orderOf_eq_of_pow_and_pow_div_prime : ∀ {G : Type u_1} [inst : Monoid G] {x : G} {n : ℕ},
  0 < n → x ^ n = 1 → (∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1) → orderOf x = n
-- Std.Data.DTreeMap.Basic
Std.DTreeMap.instSDiff : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → SDiff (Std.DTreeMap α β cmp)
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- This is an auxiliary data structure useful for constructing adjunctions.
See `Adjunction.mkOfHomEquiv`.
This structure won't typically be used anywhere else.
 -/
CategoryTheory.Adjunction.CoreHomEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.Functor C D → CategoryTheory.Functor D C → Type (max (max (max u₁ u₂) v₁) v₂)
-- Batteries.Recycling.MonadSatisfying.Array
Array.size_mapM : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] (f : α → m β) (as : Array α),
  SatisfiesM (fun arr => arr.size = as.size) (Array.mapM f as)
-- Init.Data.Array.Lemmas
Array.append_inj : ∀ {α : Type u_1} {xs₁ xs₂ ys₁ ys₂ : Array α}, xs₁ ++ ys₁ = xs₂ ++ ys₂ → xs₁.size = xs₂.size → xs₁ = xs₂ ∧ ys₁ = ys₂
-- Mathlib.Data.Complex.Basic
/-- A vertical segment `[b₁, b₂]` translated by `a` is the complex line segment.  -/
Complex.verticalSegment_eq : ∀ (a b₁ b₂ : ℝ), (fun y => ↑a + ↑y * Complex.I) '' Set.uIcc b₁ b₂ = {a} ×ℂ Set.uIcc b₁ b₂
-- Init.Grind.Config
Lean.Grind.OrderConfig.mk.sizeOf_spec : ∀ (toNoopConfig : Lean.Grind.NoopConfig), sizeOf { toNoopConfig := toNoopConfig } = 1 + sizeOf toNoopConfig
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Over.mk_hom : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P : CategoryTheory.MorphismProperty T}
  (Q : CategoryTheory.MorphismProperty T) {X A : T} (f : A ⟶ X) (hf : P f),
  (CategoryTheory.MorphismProperty.Over.mk Q f hf).hom = f
-- Mathlib.Topology.MetricSpace.Lipschitz
LipschitzWith.mk_one : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β},
  (∀ (x y : α), dist (f x) (f y) ≤ dist x y) → LipschitzWith 1 f
-- Std.Http.Internal.String
_private.Std.Http.Internal.String.0.Std.Http.Internal.UnquoteState.valid : Bool → String → Std.Http.Internal.UnquoteState✝
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.epi_of_target_iso_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) (i : Y ≅ 0), CategoryTheory.Epi f
-- Mathlib.RingTheory.Flat.Localization
Module.flat_of_localized_maximal : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_3) [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  (∀ (P : Ideal R) [inst_3 : P.IsMaximal], Module.Flat R (LocalizedModule P.primeCompl M)) → Module.Flat R M
-- Std.Data.TreeSet.Raw.Iterator
/-- Returns a finite iterator over the entries of a tree set.
The iterator yields the elements of the set in order and then terminates.

**Termination properties:**

* `Finite` instance: always
* `Productive` instance: always
 -/
Std.TreeSet.Raw.iter : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet.Raw α cmp → Std.Iter α
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.loopyOn.eq_1 : ∀ {α : Type u_1} (E : Set α), Matroid.loopyOn E = (Matroid.emptyOn α).restrict E
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.updateCol_comm : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : DecidableEq n] (A : Matrix m n α) {j j' : n},
  j ≠ j' → ∀ (x y : m → α), (A.updateCol j x).updateCol j' y = (A.updateCol j' y).updateCol j x
-- Mathlib.Data.Ordmap.Ordnode
/-- O(log n). Split the tree into those smaller than `x` and those greater than it,
plus an element equivalent to `x`, if it exists.

```
split3 2 {1, 2, 4} = ({1}, some 2, {4})
split3 3 {1, 2, 4} = ({1, 2}, none, {4})
split3 4 {1, 2, 4} = ({1, 2}, some 4, ∅)
```

Using a preorder on `ℕ × ℕ` that only compares the first coordinate:

```
split3 (1, 1) {(0, 1), (1, 2)} = ({(0, 1)}, some (1, 2), ∅)
split3 (3, 1) {(0, 1), (1, 2)} = ({(0, 1), (1, 2)}, none, ∅)
```  -/
Ordnode.split3 : {α : Type u_1} → [inst : LE α] → [DecidableLE α] → α → Ordnode α → Ordnode α × Option α × Ordnode α
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.yonedaEquiv_comp : ∀ {X Y : SSet} {n : SimplexCategory} (f : SSet.stdSimplex.obj n ⟶ X) (g : X ⟶ Y),
  SSet.yonedaEquiv (CategoryTheory.CategoryStruct.comp f g) =
    (CategoryTheory.ConcreteCategory.hom (g.app (Opposite.op n))) (SSet.yonedaEquiv f)
-- Init.Data.String.Lemmas.Iterate
/-- A list of all positions starting at `p`.

This function is not meant to be used in actual programs. Actual programs should use
`Slice.positionsFrom` or `Slice.positions`.
 -/
String.Model.positionsFrom : {s : String} → s.Pos → List { p // p ≠ s.endPos }
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroupRel'.trans.sizeOf_spec : ∀ {R : Type u} [inst : Rack R] [inst_1 : SizeOf R] {a b c : Rack.PreEnvelGroup R} (hab : Rack.PreEnvelGroupRel' R a b)
  (hbc : Rack.PreEnvelGroupRel' R b c),
  sizeOf (hab.trans hbc) = 1 + sizeOf a + sizeOf b + sizeOf c + sizeOf hab + sizeOf hbc
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.ofList_cons : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {hd : α} {tl : List α},
  Std.ExtHashSet.ofList (hd :: tl) = (∅.insert hd).insertMany tl
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
CategoryTheory.Limits.IsZero.to_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (h : CategoryTheory.Limits.IsZero X) (f : X ⟶ Y),
  h.to_ Y = f
-- Mathlib.Topology.Instances.NNReal.Lemmas
NNReal.iInf_real_pos_eq_iInf_nnreal_pos : ∀ {α : Type u_2} [inst : CompleteLattice α] {f : ℝ → α}, ⨅ n, ⨅ (_ : 0 < n), f n = ⨅ n, ⨅ (_ : 0 < n), f ↑n
-- Mathlib.RingTheory.FinitePresentation
RingHom.FinitePresentation.comp : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : CommRing C]
  {g : B →+* C} {f : A →+* B}, g.FinitePresentation → f.FinitePresentation → (g.comp f).FinitePresentation
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.dblZ.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Jacobian R) (P : Fin 3 → R),
  W'.dblZ P = P 2 * (P 1 - W'.negY P)
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
UniqueFactorizationMonoid.zero_notMem_normalizedFactors : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizationMonoid α] [inst_2 : UniqueFactorizationMonoid α]
  (x : α), 0 ∉ UniqueFactorizationMonoid.normalizedFactors x
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.ofCoeff.sizeOf_spec : ∀ {k : Type u_1} {G : Type u_2} [inst : Zero k] [inst_1 : SizeOf k] [inst_2 : SizeOf G] (coeff : G →₀ k),
  sizeOf { coeff := coeff } = 1 + sizeOf coeff
-- Mathlib.RingTheory.Localization.Away.Basic
IsLocalization.away_snd : ∀ {R : Type u_4} {S : Type u_5} [inst : CommSemiring R] [inst_1 : CommSemiring S], IsLocalization.Away (0, 1) S
-- Mathlib.Topology.VectorBundle.Basic
VectorPrebundle.mk : {R : Type u_1} →
  {B : Type u_2} →
    {F : Type u_3} →
      {E : B → Type u_4} →
        [inst : NontriviallyNormedField R] →
          [inst_1 : (x : B) → AddCommMonoid (E x)] →
            [inst_2 : (x : B) → Module R (E x)] →
              [inst_3 : NormedAddCommGroup F] →
                [inst_4 : NormedSpace R F] →
                  [inst_5 : TopologicalSpace B] →
                    [inst_6 : (x : B) → TopologicalSpace (E x)] →
                      (pretrivializationAtlas : Set (Bundle.Pretrivialization F Bundle.TotalSpace.proj)) →
                        (∀ e ∈ pretrivializationAtlas, Bundle.Pretrivialization.IsLinear R e) →
                          (pretrivializationAt : B → Bundle.Pretrivialization F Bundle.TotalSpace.proj) →
                            (∀ (x : B), x ∈ (pretrivializationAt x).baseSet) →
                              (∀ (x : B), pretrivializationAt x ∈ pretrivializationAtlas) →
                                (∀ e ∈ pretrivializationAtlas,
                                    ∀ e' ∈ pretrivializationAtlas,
                                      ∃ f,
                                        ContinuousOn f (e.baseSet ∩ e'.baseSet) ∧
                                          ∀ b ∈ e.baseSet ∩ e'.baseSet, ∀ (v : F), (f b) v = (↑e' ⟨b, e.symm b v⟩).2) →
                                  (∀ (b : B), Topology.IsInducing (↑(pretrivializationAt b) ∘ Bundle.TotalSpace.mk b)) →
                                    VectorPrebundle R F E
-- Mathlib.Analysis.Calculus.FDeriv.Mul
HasStrictFDerivAt.multiset_prod : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {ι : Type u_5} {𝔸' : Type u_7} [inst_3 : NormedCommRing 𝔸'] [inst_4 : NormedAlgebra 𝕜 𝔸']
  {g : ι → E → 𝔸'} {g' : ι → E →L[𝕜] 𝔸'} [inst_5 : DecidableEq ι] {u : Multiset ι} {x : E},
  (∀ i ∈ u, HasStrictFDerivAt (fun x => g i x) (g' i) x) →
    HasStrictFDerivAt (fun x => (Multiset.map (fun x_1 => g x_1 x) u).prod)
      (Multiset.map (fun i => (Multiset.map (fun x_1 => g x_1 x) (u.erase i)).prod • g' i) u).sum x
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- The action by a subsemiring is the action by the underlying semiring.  -/
Subsemiring.smul : {R' : Type u_1} → {α : Type u_2} → [inst : NonAssocSemiring R'] → [SMul R' α] → (S : Subsemiring R') → SMul (↥S) α
-- Mathlib.LinearAlgebra.AffineSpace.Basis
AffineBasis.coe_reindex : ∀ {ι : Type u_1} {ι' : Type u_2} {k : Type u_5} {V : Type u_6} {P : Type u_7} [inst : AddCommGroup V]
  [inst_1 : AddTorsor V P] [inst_2 : Ring k] [inst_3 : Module k V] (b : AffineBasis ι k P) (e : ι ≃ ι'),
  ⇑(b.reindex e) = ⇑b ∘ ⇑e.symm
-- Mathlib.RingTheory.Derivation.Lie
Derivation.instLieRing : {R : Type u_1} →
  [inst : CommRing R] → {A : Type u_2} → [inst_1 : CommRing A] → [inst_2 : Algebra R A] → LieRing (Derivation R A A)
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
_private.Mathlib.CategoryTheory.Monoidal.Free.Coherence.0.CategoryTheory.FreeMonoidalCategory.termF : Lean.ParserDescr
-- Mathlib.Order.Filter.Defs
Filter.mem_sets : ∀ {α : Type u_1} {f : Filter α} {s : Set α}, s ∈ f.sets ↔ s ∈ f
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
linearIndependent_finCons : ∀ {K : Type u_3} {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {x : V} {n : ℕ}
  {v : Fin n → V}, LinearIndependent K (Fin.cons x v) ↔ LinearIndependent K v ∧ x ∉ Submodule.span K (Set.range v)
-- Mathlib.GroupTheory.FiniteAbelian.Basic
_private.Mathlib.GroupTheory.FiniteAbelian.Basic.0.directSumNeZeroMulEquiv : (ι : Type) →
  [DecidableEq ι] →
    (p n : ι → ℕ) → (DirectSum { i // n i ≠ 0 } fun i => ZMod (p ↑i ^ n ↑i)) ≃+ DirectSum ι fun i => ZMod (p i ^ n i)
-- Mathlib.Order.Category.HeytAlg
_private.Mathlib.Order.Category.HeytAlg.0.HeytAlg.Hom.mk.sizeOf_spec : ∀ {X Y : HeytAlg} (hom' : HeytingHom ↑X ↑Y), sizeOf { hom' := hom' } = 1 + sizeOf hom'
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Real.hasStrictDerivAt_arcsin : ∀ {x : ℝ}, x ≠ -1 → x ≠ 1 → HasStrictDerivAt Real.arcsin (1 / √(1 - x ^ 2)) x
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
_private.Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality.0.Polynomial.Chebyshev.measureT.eq_1 : Polynomial.Chebyshev.measureT =
  (MeasureTheory.volume.withDensity fun x => ↑(NNReal.mk √(1 - x ^ 2)⁻¹ ⋯)).restrict (Set.Ioc (-1) 1)
-- Mathlib.Data.Set.Sigma
Set.sigma_preimage_left : ∀ {ι : Type u_1} {ι' : Type u_2} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {f : ι' → ι},
  ((f ⁻¹' s).sigma fun i => t (f i)) = (fun p => ⟨f p.fst, p.snd⟩) ⁻¹' s.sigma t
-- Mathlib.CategoryTheory.Monad.Equalizer
CategoryTheory.Comonad.CofreeEqualizer.ι_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Comonad C} (X : T.Coalgebra),
  (CategoryTheory.Comonad.CofreeEqualizer.ι X).f = X.a
-- Mathlib.AlgebraicTopology.SimplicialSet.Op
SSet.opEquivalence_inverse : SSet.opEquivalence.inverse = SSet.opFunctor
-- Mathlib.Data.List.Nodup
List.nodup_concat : ∀ {α : Type u} (l : List α) (u : α), (l.concat u).Nodup ↔ u ∉ l ∧ l.Nodup
-- Mathlib.ModelTheory.Definability
FirstOrder.Language.DefinableSet.instTop : {L : FirstOrder.Language} →
  {M : Type w} → [inst : L.Structure M] → {A : Set M} → {α : Type u₁} → Top (L.DefinableSet A α)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey!_le : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.isEmpty = false → ∀ {k : α}, (cmp t.maxKey! k).isLE = true ↔ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Lean.Meta.MonadSimp
Lean.Meta.MonadSimp.Result.step.injEq : ∀ (e h e_1 h_1 : Lean.Expr),
  (Lean.Meta.MonadSimp.Result.step e h = Lean.Meta.MonadSimp.Result.step e_1 h_1) = (e = e_1 ∧ h = h_1)
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintLabel.name.injEq : ∀ (n n_1 : String), (Lean.Elab.InlayHintLabel.name n = Lean.Elab.InlayHintLabel.name n_1) = (n = n_1)
-- Mathlib.Algebra.Homology.DerivedCategory.Plus
/-- The canonical t-structure on `DerivedCategory.Plus C`.  -/
DerivedCategory.Plus.TStructure.t : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : HasDerivedCategory C] → CategoryTheory.Triangulated.TStructure (DerivedCategory.Plus C)
-- Mathlib.Algebra.Polynomial.Div
Polynomial.rootMultiplicity_zero : ∀ {R : Type u} [inst : Ring R] {x : R}, Polynomial.rootMultiplicity x 0 = 0
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
/-- Any module is a quotient of a free module. This is stated as surjectivity of
`Finsupp.linearCombination R id : (M →₀ R) →ₗ[R] M`.  -/
Finsupp.linearCombination_id_surjective : ∀ (R : Type u_5) [inst : Semiring R] (M : Type u_9) [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Function.Surjective ⇑(Finsupp.linearCombination R id)
-- Mathlib.Tactic.ClickSuggestions.SectionState
/-- Insert the new result `res` into the array `arr` of already existing results.

We maintain the invariants that `results` is sorted, and for each set of duplicate results,
only the first one can have the `filtered` field set to `some`.  -/
Mathlib.Tactic.ClickSuggestions.Result.insertInArray : {α : Type} →
  [Ord α] →
    [Inhabited α] →
      Mathlib.Tactic.ClickSuggestions.Result α →
        Array (Mathlib.Tactic.ClickSuggestions.Result α) →
          (α → α → Lean.MetaM Bool) → Lean.MetaM (Array (Mathlib.Tactic.ClickSuggestions.Result α))
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
AlgebraicGeometry.UniversallyInjective.respectsIso : CategoryTheory.MorphismProperty.RespectsIso @AlgebraicGeometry.UniversallyInjective
-- Mathlib.Algebra.Ring.Shrink
Shrink.instAddGroupWithOne : {α : Type u_1} → [inst : Small.{v, u_1} α] → [AddGroupWithOne α] → AddGroupWithOne (Shrink.{v, u_1} α)
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.coevaluation_comp_rightAdjointMate_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  [inst_2 : CategoryTheory.HasRightDual X] [inst_3 : CategoryTheory.HasRightDual Y] (f : X ⟶ Y) {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Y Xᘁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (η_ Y Yᘁ)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (fᘁ)) h) =
    CategoryTheory.CategoryStruct.comp (η_ X Xᘁ)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Xᘁ) h)
-- Batteries.Data.ByteSlice
ByteSlice.instForInUInt8OfMonad_batteries : {m : Type u_1 → Type u_2} → [Monad m] → ForIn m ByteSlice UInt8
-- Mathlib.ModelTheory.Syntax
/-- Relabels a term's variables along a bijection.  -/
FirstOrder.Language.Term.relabelEquiv : {L : FirstOrder.Language} → {α : Type u'} → {β : Type v'} → α ≃ β → L.Term α ≃ L.Term β
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.contains_minKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {km : α}, t.minKey? = some km → t.contains km = true
-- Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
ContinuousAlternatingMap.toContinuousLinearMap.congr_simp : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N] (f f_1 : M [⋀^ι]→L[R] N),
  f = f_1 →
    ∀ {inst_7 : DecidableEq ι} [inst_8 : DecidableEq ι] (m m_1 : ι → M),
      m = m_1 → ∀ (i i_1 : ι), i = i_1 → f.toContinuousLinearMap m i = f_1.toContinuousLinearMap m_1 i_1
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.instInhabited : {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} → Inhabited (M [⋀^ι]→ₗ[R] N)
-- Mathlib.Topology.Constructions.SumProd
isOpen_range_inr : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y], IsOpen (Set.range Sum.inr)
-- Mathlib.Data.Nat.Prime.Basic
Nat.Prime.mul_eq_prime_sq_iff : ∀ {x y p : ℕ}, Nat.Prime p → x ≠ 1 → y ≠ 1 → (x * y = p ^ 2 ↔ x = p ∧ y = p)
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.pi_Iio_ae_eq_pi_Iic : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  {μ : (i : ι) → MeasureTheory.Measure (α i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)]
  [inst_3 : (i : ι) → PartialOrder (α i)] [∀ (i : ι), MeasureTheory.NullSingletonClass (μ i)] {s : Set ι}
  {f : (i : ι) → α i}, (s.pi fun i => Set.Iio (f i)) =ᵐ[MeasureTheory.Measure.pi μ] s.pi fun i => Set.Iic (f i)
-- Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
/-- The GL-image of `Γ(1)` equals `𝒮ℒ` (the image of `SL(2, ℤ)` in `GL(2, ℝ)`).  -/
CongruenceSubgroup.Gamma_one_coe_eq_SL : Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1) =
  (Matrix.SpecialLinearGroup.mapGL ℝ).range
-- Mathlib.AlgebraicGeometry.Restrict
/-- `X ∣_ U ∣_ V` is isomorphic to `X ∣_ V ∣_ U`  -/
AlgebraicGeometry.Scheme.restrictRestrictComm : (X : AlgebraicGeometry.Scheme) →
  (U V : X.Opens) → ↑((TopologicalSpace.Opens.map U.ι.base).obj V) ≅ ↑((TopologicalSpace.Opens.map V.ι.base).obj U)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.denote_blastShiftRight : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w0 : ℕ} (aig : Std.Sat.AIG α)
  (target : aig.ArbitraryShiftTarget w0) (lhs : BitVec w0) (rhs : BitVec target.n) (assign : α → Bool),
  (∀ (idx : ℕ) (hidx : idx < w0), ⟦assign, { aig := aig, ref := target.target.get idx hidx }⟧ = lhs.getLsbD idx) →
    (∀ (idx : ℕ) (hidx : idx < target.n),
        ⟦assign, { aig := aig, ref := target.distance.get idx hidx }⟧ = rhs.getLsbD idx) →
      ∀ (idx : ℕ) (hidx : idx < w0),
        ⟦assign,
            { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRight aig target).aig,
              ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRight aig target).vec.get idx hidx }⟧ =
          (lhs >>> rhs).getLsbD idx
-- Init.Data.UInt.Lemmas
UInt64.toNat_lt : ∀ (n : UInt64), n.toNat < 2 ^ 64
-- Mathlib.Order.SymmDiff
inf_sup_symmDiff : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ⊓ b ⊔ symmDiff a b = a ⊔ b
-- Mathlib.Order.WithBot
WithBot.unbotA_eq_unbot : ∀ {α : Type u_1} [inst : Nonempty α] {a : WithBot α} (ha : a ≠ ⊥), a.unbotA = a.unbot ha
-- Mathlib.Algebra.Lie.Extension
_private.Mathlib.Algebra.Lie.Extension.0.LieAlgebra.Extension.twoCocycleAux.congr_simp : ∀ {R : Type u_1} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing M] [inst_4 : LieAlgebra R M] (E : LieAlgebra.Extension R M L) {s s_1 : L →ₗ[R] E.L} (e_s : s = s_1)
  (hs : Function.LeftInverse ⇑E.proj ⇑s),
  LieAlgebra.Extension.twoCocycleAux✝ E hs = LieAlgebra.Extension.twoCocycleAux✝ E ⋯
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryFst_mapPullbackAdj_unit_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X Y : C) (T : CategoryTheory.Over (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)),
  (CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y)).unit.app
      T =
    CategoryTheory.Over.homMk
      (CategoryTheory.CartesianMonoidalCategory.lift
        (CategoryTheory.CategoryStruct.id
          ((CategoryTheory.Functor.id (CategoryTheory.Over (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))).obj
              T).left)
        (CategoryTheory.CategoryStruct.comp T.hom (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y)))
      ⋯
-- Lean.Environment
/-- Free compacted regions of imports. No live references to imported objects may exist at the time of invocation; in
particular, `env` should be the last reference to any `Environment` derived from these imports.  -/
Lean.Environment.freeRegions : Lean.Environment → IO Unit
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.biUnion_boxes : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I)
  (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J),
  (π.biUnion πi).boxes = π.boxes.biUnion fun J => (πi J).boxes
-- Init.Data.UInt.Lemmas
UInt32.neg_zero : -0 = 0
-- Init.Data.List.Find
List.find?_replicate_eq_some_iff : ∀ {α : Type u_1} {n : ℕ} {a b : α} {p : α → Bool},
  List.find? p (List.replicate n a) = some b ↔ n ≠ 0 ∧ p a = true ∧ a = b
-- Lean.Parser.Extension
Lean.Parser.mkCategoryAntiquotParser : Lean.Name → Lean.Parser.Parser
-- Mathlib.Probability.Process.Filtration
/-- Given a process `f` and a filtration `ℱ`, if `f` converges to some `g` almost everywhere and
`g` is `⨆ n, ℱ n`-measurable, then `limitProcess f ℱ μ` chooses said `g`, else it returns 0.

This definition is used to phrase the a.e. martingale convergence theorem
`Submartingale.ae_tendsto_limitProcess` where an L¹-bounded submartingale `f` adapted to `ℱ`
converges to `limitProcess f ℱ μ` `μ`-almost everywhere.  -/
MeasureTheory.Filtration.limitProcess : {Ω : Type u_1} →
  {ι : Type u_2} →
    {m : MeasurableSpace Ω} →
      [inst : Preorder ι] →
        {E : Type u_4} →
          [Zero E] → [TopologicalSpace E] → (ι → Ω → E) → MeasureTheory.Filtration ι m → MeasureTheory.Measure Ω → Ω → E
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeAddGroup.reduce_singleton : ∀ {α : Type u_1} [inst : DecidableEq α] (s : α × Bool), FreeAddGroup.reduce [s] = [s]
-- Mathlib.CategoryTheory.Limits.Comma
/-- If `R` preserves the appropriate limit, then given a cone for `F ⋙ fst L R : J ⥤ L` and a
limit cone for `F ⋙ snd L R : J ⥤ R` we can build a cone for `F` which will turn out to be a limit
cone.
 -/
CategoryTheory.Comma.coneOfPreserves : {J : Type w} →
  [inst : CategoryTheory.Category.{w', w} J] →
    {A : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} A] →
        {B : Type u₂} →
          [inst_2 : CategoryTheory.Category.{v₂, u₂} B] →
            {T : Type u₃} →
              [inst_3 : CategoryTheory.Category.{v₃, u₃} T] →
                {L : CategoryTheory.Functor A T} →
                  {R : CategoryTheory.Functor B T} →
                    (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) →
                      [CategoryTheory.Limits.PreservesLimit (F.comp (CategoryTheory.Comma.snd L R)) R] →
                        CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.fst L R)) →
                          {c₂ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.snd L R))} →
                            CategoryTheory.Limits.IsLimit c₂ → CategoryTheory.Limits.Cone F