mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Range.Polymorphic.Basic
/-- If the smallest value in the range satisfies the upper bound and has no successor, the size is
  one.
   -/
Std.Rxi.LawfulHasSize.size_eq_one_of_succ?_eq_none : ∀ {α : Type u} {inst : Std.PRange.UpwardEnumerable α} {inst_1 : Std.Rxi.HasSize α} [self : Std.Rxi.LawfulHasSize α]
  (lo : α), Std.PRange.succ? lo = none → Std.Rxi.HasSize.size lo = 1
-- Mathlib.Data.List.Rotate
List.head?_cyclicPermutations : ∀ {α : Type u} (l : List α), l.cyclicPermutations.head? = some l
-- Aesop.Tree.Data
Aesop.GoalData.preNormGoal : {Rapp MVarCluster : Type} → Aesop.GoalData Rapp MVarCluster → Lean.MVarId
-- Mathlib.Data.Finset.Sum
Finset.toRight.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (u : Finset (α ⊕ β)), u.toRight = Finset.filterMap (Sum.elim (fun x => none) some) u ⋯
-- Init.Core
/-- Type class for the `singleton` operation.
Used to implement the `{ a, b, c }` syntax.
 -/
Singleton : outParam (Type u) → Type v → Type (max u v)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.HoverParams.mk : Lean.Lsp.TextDocumentPositionParams → Lean.Lsp.HoverParams
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.arg.mkNamed : ℕ → Lean.Parser.ParserContext → Lean.Parser.ParserState → Lean.Parser.ParserState
-- Mathlib.Analysis.Normed.Module.Ball.RadialEquiv
homeomorphUnitSphereProd_apply_fst_coe : ∀ (E : Type u_1) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (x : ↑{0}ᶜ),
  ↑((homeomorphUnitSphereProd E) x).1 = ‖↑x‖⁻¹ • ↑x
-- Mathlib.CategoryTheory.FintypeCat
FintypeCat.Skeleton.instSmallCategory : CategoryTheory.SmallCategory FintypeCat.Skeleton
-- Mathlib.Order.Filter.IsBounded
isCoboundedUnder_ge_finset_inf' : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : LinearOrder β] {f : Filter α} {F : ι → α → β} {s : Finset ι}
  (hs : s.Nonempty),
  (∃ i ∈ s, Filter.IsCoboundedUnder (fun x1 x2 => x2 ≤ x1) f (F i)) →
    Filter.IsCoboundedUnder (fun x1 x2 => x2 ≤ x1) f fun a => s.inf' hs fun i => F i a
-- Mathlib.CategoryTheory.Limits.Creates
CategoryTheory.CreatesLimitsOfShape.CreatesLimit : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {D : Type u₂} →
      {inst_1 : CategoryTheory.Category.{v₂, u₂} D} →
        {J : Type w} →
          {inst_2 : CategoryTheory.Category.{w', w} J} →
            {F : CategoryTheory.Functor C D} →
              [self : CategoryTheory.CreatesLimitsOfShape J F] →
                {K : CategoryTheory.Functor J C} → CategoryTheory.CreatesLimit K F
-- Mathlib.Data.Rel
Equiv.graph_inv : ∀ {α : Type u_1} {β : Type u_2} (f : α ≃ β), Function.graph ⇑f.symm = (Function.graph ⇑f).inv
-- Init.Data.Nat.Lemmas
Nat.div_dvd_of_dvd : ∀ {n m : ℕ}, n ∣ m → m / n ∣ m
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.isCoatom_comap_or_eq_top : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) {p : Submodule R₂ M₂},
  IsCoatom p → IsCoatom (Submodule.comap f p) ∨ Submodule.comap f p = ⊤
-- Std.Data.Internal.List.Associative
Std.Internal.List.isEmpty_filter_containsKey_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)},
  l₂.isEmpty = true → (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁).isEmpty = true
-- Init.Data.List.ToArray
List.findM?_toArray : ∀ {m : Type → Type u_1} {α : Type} [inst : Monad m] [LawfulMonad m] (f : α → m Bool) (l : List α),
  Array.findM? f l.toArray = List.findM? f l
-- Mathlib.Data.Nat.Bits
Nat.div2_bits_eq_tail : ∀ (n : ℕ), n.div2.bits = n.bits.tail
-- Mathlib.Order.RelClasses
isTrans_ge : ∀ {α : Type u} [inst : Preorder α], IsTrans α fun a a_1 => a_1 ≤ a
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X₁ X₂ X₃ : C} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃)
  (zero : autoParam (CategoryTheory.CategoryStruct.comp f g = 0) CategoryTheory.ShortComplex.zero._autoParam)
  (X₁_1 X₂_1 X₃_1 : C) (f_1 : X₁_1 ⟶ X₂_1) (g_1 : X₂_1 ⟶ X₃_1)
  (zero_1 : autoParam (CategoryTheory.CategoryStruct.comp f_1 g_1 = 0) CategoryTheory.ShortComplex.zero._autoParam),
  ({ X₁ := X₁, X₂ := X₂, X₃ := X₃, f := f, g := g, zero := zero } =
      { X₁ := X₁_1, X₂ := X₂_1, X₃ := X₃_1, f := f_1, g := g_1, zero := zero_1 }) =
    (X₁ = X₁_1 ∧ X₂ = X₂_1 ∧ X₃ = X₃_1 ∧ f ≍ f_1 ∧ g ≍ g_1)
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.ne_zero_or_ne_zero : ∀ {R : Type u} [inst : CommSemiring R] {x y : R} [Nontrivial R], IsCoprime x y → x ≠ 0 ∨ y ≠ 0
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.contains_empty : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {a : α},
  ∅.contains a = false
-- Init.Data.List.Lemmas
List.getElem_of_getElem? : ∀ {α : Type u_1} {i : ℕ} {a : α} {l : List α}, l[i]? = some a → ∃ (h : i < l.length), l[i] = a
-- Std.Data.Iterators.Combinators.Monadic.DropWhile
Std.Iterators.Types.DropWhile.mk.inj : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} {P : β → Std.Iterators.PostconditionT m (ULift.{w, 0} Bool)}
  {dropping : Bool} {inner : Std.IterM m β} {dropping_1 : Bool} {inner_1 : Std.IterM m β},
  { dropping := dropping, inner := inner } = { dropping := dropping_1, inner := inner_1 } →
    dropping = dropping_1 ∧ inner = inner_1
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.parent_lt : ∀ (self : Batteries.UnionFind) (i : ℕ), self.parent i < self.size ↔ i < self.size
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Real.sinc_eq_dslope : Real.sinc = dslope Real.sin 0
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem_eq_get_getElem? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp] (h : t.WF)
  {a : α} {h' : a ∈ t}, t[a] = t[a]?.get ⋯
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.denoteAsIntModule.go.eq_2 : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] (ctx : Lean.Grind.CommRing.Context α) (acc : α)
  (p : Lean.Grind.CommRing.Power) (m_1 : Lean.Grind.CommRing.Mon),
  Lean.Grind.CommRing.Mon.denoteAsIntModule.go ctx (Lean.Grind.CommRing.Mon.mult p m_1) acc =
    Lean.Grind.CommRing.Mon.denoteAsIntModule.go ctx m_1 (acc * Lean.Grind.CommRing.Power.denote ctx p)
-- Mathlib.Algebra.Group.Prod
Prod.instIsLeftCancelAdd : ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] [IsLeftCancelAdd G] [IsLeftCancelAdd H],
  IsLeftCancelAdd (G × H)
-- Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
RootPairing.pairingIn_eq_zero_of_add_notMem_of_sub_notMem : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) [Finite ι]
  [CharZero R] [inst_7 : P.IsCrystallographic] {i j : ι} [IsDomain R],
  i ≠ j →
    P.root i ≠ -P.root j →
      P.root i + P.root j ∉ Set.range ⇑P.root → P.root i - P.root j ∉ Set.range ⇑P.root → P.pairingIn ℤ i j = 0
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- The lax monoidal functor structure induced by a `Functor.CoreMonoidal` structure.  -/
CategoryTheory.Functor.CoreMonoidal.toLaxMonoidal : {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] →
            {F : CategoryTheory.Functor C D} → F.CoreMonoidal → F.LaxMonoidal
-- Init.Data.List.Attach
List.getElem?_pmap : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {l : List α} (h : ∀ a ∈ l, p a) (i : ℕ),
  (List.pmap f l h)[i]? = Option.pmap f l[i]? ⋯
-- Mathlib.AlgebraicTopology.DoldKan.Compatibility
AlgebraicTopology.DoldKan.Compatibility.equivalence₁UnitIso_hom_app : ∀ {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] [inst_2 : CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'}
  {e' : A' ≌ B'} {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F) (X : A),
  (AlgebraicTopology.DoldKan.Compatibility.equivalence₁UnitIso hF).hom.app X =
    CategoryTheory.CategoryStruct.comp (eA.unitIso.hom.app X)
      (CategoryTheory.CategoryStruct.comp (eA.inverse.map (e'.unitIso.hom.app (eA.functor.obj X)))
        (eA.inverse.map (e'.inverse.map (hF.hom.app X))))
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Char
String.Slice.endsWith_char_iff_get : ∀ {c : Char} {s : String.Slice}, s.endsWith c = true ↔ ∃ (h : s.endPos ≠ s.startPos), (s.endPos.prev h).get ⋯ = c
-- Mathlib.Algebra.Order.Ring.Archimedean
ArchimedeanClass.add_left_cancel_of_ne_top : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : CommRing R] [inst_2 : IsStrictOrderedRing R]
  {x y z : ArchimedeanClass R}, x ≠ ⊤ → x + y = x + z → y = z
-- Std.Http.Data.Body.Stream
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Channel.Consumer.select.inj : ∀ {finished finished_1 : Std.Async.Waiter (Option Std.Http.Chunk)},
  Std.Http.Body.Channel.Consumer.select✝ finished = Std.Http.Body.Channel.Consumer.select✝ finished_1 →
    finished = finished_1
-- Std.Data.DHashMap.Raw
_private.Std.Data.DHashMap.Raw.0.Std.DHashMap.Raw.insert.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Raw α β) (a : α) (b : β a),
  m.insert a b = if h : 0 < m.buckets.size then ↑(Std.DHashMap.Internal.Raw₀.insert ⟨m, h⟩ a b) else m
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₁.isIso_π_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (K L : CochainComplex C ℤ) [inst_2 : CategoryTheory.EnoughInjectives C] (n₁ i : ℤ),
  autoParam (i ≠ n₁) CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₁.isIso_π_f._auto_1✝ →
    CategoryTheory.IsIso ((CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₁.π✝ K L n₁).f i)
-- Mathlib.Combinatorics.SetFamily.LYM
/-- `falling k 𝒜` is all the finsets of cardinality `k` which are a subset of something in `𝒜`.  -/
Finset.falling : {α : Type u_2} → [DecidableEq α] → ℕ → Finset (Finset α) → Finset (Finset α)
-- Mathlib.Algebra.Group.Center
/-- The centralizer of a subset of a magma.  -/
Set.centralizer : {M : Type u_1} → Set M → [Mul M] → Set M
-- Lean.Data.KVMap
Lean.DataValue.ofName.injEq : ∀ (v v_1 : Lean.Name), (Lean.DataValue.ofName v = Lean.DataValue.ofName v_1) = (v = v_1)
-- Std.Time.Time.HourMarker
Std.Time.instOrientedOrdHourMarker : Std.OrientedOrd Std.Time.HourMarker
-- Mathlib.GroupTheory.Coset.Card
Subgroup.card_comap_dvd_of_injective : ∀ {α : Type u_1} [inst : Group α] {H : Type u_2} [inst_1 : Group H] (K : Subgroup H) (f : α →* H),
  Function.Injective ⇑f → Nat.card ↥(Subgroup.comap f K) ∣ Nat.card ↥K
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.below.map : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  {motive : (a a_1 : CommRingCat.Colimits.Prequotient F) → CommRingCat.Colimits.Relation F a a_1 → Prop} (j j' : J)
  (f : j ⟶ j') (x : ↑(F.obj j)), CommRingCat.Colimits.Relation.below ⋯
-- Lean.Elab.Term.TermElabM
/-- Creates a new metavariable of type `type` that will be synthesized using the tactic code.
The `tacticCode` syntax is the full `by ..` syntax.
 -/
Lean.Elab.Term.mkTacticMVar : Lean.Expr → Lean.Syntax → Lean.Elab.Term.TacticMVarKind → optParam Bool false → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.NumberTheory.Pell
/-- If a solution has `x > 1`, then `d` is not a square.  -/
Pell.Solution₁.d_nonsquare_of_one_lt_x : ∀ {d : ℤ} {a : Pell.Solution₁ d}, 1 < a.x → ¬IsSquare d
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Continuous.arccos : ∀ {X : Type u_1} [inst : TopologicalSpace X] {f : X → ℝ}, Continuous f → Continuous fun x => Real.arccos (f x)
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.smulOfNeZero_symm_apply : ∀ (K : Type u_3) (M : Type u_5) [inst : Field K] [inst_1 : AddCommGroup M] [inst_2 : Module K M] (a : K) (ha : a ≠ 0)
  (a_1 : M), (LinearEquiv.smulOfNeZero K M a ha).symm a_1 = (Units.mk0 a ha)⁻¹ • a_1
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
HomotopyCategory.hasShift : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] → CategoryTheory.HasShift (HomotopyCategory C (ComplexShape.up ℤ)) ℤ
-- Mathlib.Algebra.GCDMonoid.Basic
coe_normalizeHom : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : StrongNormalizationMonoid α], ⇑normalizeHom = normalize
-- Mathlib.Order.CompleteSublattice
CompleteSublattice.coe_sSup : ∀ {α : Type u_1} [inst : CompleteLattice α] {L : CompleteSublattice α} (S : Set ↥L),
  ↑(sSup S) = sSup {x | ∃ s ∈ S, ↑s = x}
-- Mathlib.CategoryTheory.PathCategory.Basic
/-- To prove a property on morphisms of a path category with given target `b`, it suffices to prove
it for the identity and prove that the property is preserved under composition on the left
with length 1 paths.  -/
CategoryTheory.Paths.induction_fixed_target : ∀ {V : Type u₁} [inst : Quiver V] {b : CategoryTheory.Paths V} (P : {a : CategoryTheory.Paths V} → (a ⟶ b) → Prop),
  P (CategoryTheory.CategoryStruct.id b) →
    (∀ {u v : V} (p : (CategoryTheory.Paths.of V).obj v ⟶ b) (q : u ⟶ v),
        P p → P (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Paths.of V).map q) p)) →
      ∀ {a : CategoryTheory.Paths V} (f : a ⟶ b), P f
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.toMatrix'.eq_1 : ∀ {R₁ : Type u_1} [inst : CommSemiring R₁] {n : Type u_5} [inst_1 : Fintype n] [inst_2 : DecidableEq n],
  LinearMap.BilinForm.toMatrix' = LinearMap.toMatrix₂' R₁
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
padicValInt.of_ne_one_ne_zero : ∀ {p : ℕ} {z : ℤ}, p ≠ 1 → z ≠ 0 → padicValInt p z = multiplicity (↑p) z
-- Mathlib.Tactic.DefEqTransformations
/-- Eta reduce everything  -/
Mathlib.Tactic.etaReduceAll : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.AlgebraicTopology.DoldKan.NCompGamma
/-- The natural isomorphism `toKaroubi (SimplicialObject C) ≅ N₁ ⋙ Γ₂`.  -/
AlgebraicTopology.DoldKan.Γ₂N₁ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] →
        CategoryTheory.Idempotents.toKaroubi (CategoryTheory.SimplicialObject C) ≅
          AlgebraicTopology.DoldKan.N₁.comp AlgebraicTopology.DoldKan.Γ₂
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.DoIfView.mk.injEq : ∀ (ref optIdent cond thenBranch elseBranch ref_1 optIdent_1 cond_1 thenBranch_1 elseBranch_1 : Lean.Syntax),
  ({ ref := ref, optIdent := optIdent, cond := cond, thenBranch := thenBranch, elseBranch := elseBranch } =
      { ref := ref_1, optIdent := optIdent_1, cond := cond_1, thenBranch := thenBranch_1,
        elseBranch := elseBranch_1 }) =
    (ref = ref_1 ∧ optIdent = optIdent_1 ∧ cond = cond_1 ∧ thenBranch = thenBranch_1 ∧ elseBranch = elseBranch_1)
-- Init.Data.SInt.Lemmas
ISize.toInt_ofNat_of_lt_two_pow_numBits : ∀ {n : ℕ}, n < 2 ^ (System.Platform.numBits - 1) → (ISize.ofNat n).toInt = ↑n
-- Mathlib.Data.Sigma.Lex
Sigma.Lex.right : ∀ {ι : Type u_1} {α : ι → Type u_2} {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop} {i : ι} (a b : α i),
  s i a b → Sigma.Lex r s ⟨i, a⟩ ⟨i, b⟩
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
/-- Shrink the indexing type of `QuasicoherentData` into the universe of the site.  -/
SheafOfModules.QuasicoherentData.shrink : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] →
          [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] →
            {M : SheafOfModules R} → M.QuasicoherentData → M.QuasicoherentData
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Complex.tan_add' : ∀ {x y : ℂ},
  ((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * ↑Real.pi / 2) ∧ ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * ↑Real.pi / 2) →
    Complex.tan (x + y) = (Complex.tan x + Complex.tan y) / (1 - Complex.tan x * Complex.tan y)
-- Std.Http.Data.Status
Std.Http.Status.useProxy.sizeOf_spec : sizeOf Std.Http.Status.useProxy = 1
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
/-- Permuting the columns changes the sign of the determinant.  -/
Matrix.det_permute : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (σ : Equiv.Perm n)
  (M : Matrix n n R), (M.submatrix (⇑σ) id).det = ↑↑(Equiv.Perm.sign σ) * M.det
-- Mathlib.Analysis.Complex.Periodic
/-- If `f` is periodic, and holomorphic and bounded near `I∞`, then it tends to a limit at `I∞`,
and this limit is the value of its cusp function at 0.
 -/
Function.Periodic.tendsto_at_I_inf : ∀ {h : ℝ} {f : ℂ → ℂ},
  0 < h →
    Function.Periodic f ↑h →
      (∀ᶠ (z : ℂ) in Filter.comap Complex.im Filter.atTop, DifferentiableAt ℂ f z) →
        (Filter.comap Complex.im Filter.atTop).BoundedAtFilter f →
          Filter.Tendsto f (Filter.comap Complex.im Filter.atTop) (nhds (Function.Periodic.cuspFunction h f 0))
-- Mathlib.Analysis.InnerProductSpace.PiL2
EuclideanSpace.norm_eq : ∀ {𝕜 : Type u_7} [inst : RCLike 𝕜] {n : Type u_8} [inst_1 : Fintype n] (x : EuclideanSpace 𝕜 n),
  ‖x‖ = √(∑ i, ‖x.ofLp i‖ ^ 2)
-- Mathlib.GroupTheory.Coxeter.Length
/-- The length of `w`; i.e., the minimum number of simple reflections that
must be multiplied to form `w`.  -/
CoxeterSystem.length : {B : Type u_1} → {W : Type u_2} → [inst : Group W] → {M : CoxeterMatrix B} → CoxeterSystem M W → W → ℕ
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.mem_iInf : ∀ {R : Type u} {M : Type v} [inst : VAdd R M] {ι : Sort u_1} {p : ι → SubAddAction R M} {x : M},
  x ∈ ⨅ i, p i ↔ ∀ (i : ι), x ∈ p i
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.leftUnitor_inv_left_fst : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X : C}
  (Y : CategoryTheory.Over X),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).inv)
      (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.id X) Y.hom) =
    Y.hom
-- Mathlib.Algebra.Module.Submodule.Pointwise
Submodule.neg_restrictScalars : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {S : Type u_4}
  [inst_3 : Semiring S] [inst_4 : SMul S R] [inst_5 : Module S M] [inst_6 : IsScalarTower S R M] (p : Submodule R M),
  -Submodule.restrictScalars S p = Submodule.restrictScalars S (-p)
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- **Alias** of `MonoidAlgebra.coe_mapRingHom`. -/
MonoidAlgebra.coe_mapRangeRingHom : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Monoid M]
  (f : R →+* S), ⇑(MonoidAlgebra.mapRingHom M f) = MonoidAlgebra.map ↑f
-- Std.Time.Zoned.ZoneRules
/-- Find the current `TimeZone` out of a `Transition` in a `Array Transition`
 -/
Std.Time.TimeZone.Transition.timezoneAt : Array Std.Time.TimeZone.Transition → Std.Time.Timestamp → Except String Std.Time.TimeZone
-- Mathlib.Algebra.Group.Equiv.Opposite
/-- A monoid homomorphism `f : M →* N` such that `f x` commutes with `f y` for all `x, y` defines
a monoid homomorphism to `Nᵐᵒᵖ`.  -/
MonoidHom.toOpposite : {M : Type u_3} →
  {N : Type u_4} →
    [inst : MulOneClass M] → [inst_1 : MulOneClass N] → (f : M →* N) → (∀ (x y : M), Commute (f x) (f y)) → M →* Nᵐᵒᵖ
-- Aesop.Check
Aesop.Check.name : Aesop.Check → Lean.Name
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.isBigOTVS_fun_comm : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {l : Filter α} {g : α → F} [ContinuousNeg E] {f₁ f₂ : α → E},
  (fun a => f₁ a - f₂ a) =O[𝕜; l] g ↔ (fun a => f₂ a - f₁ a) =O[𝕜; l] g
-- Mathlib.CategoryTheory.Limits.Bicones
CategoryTheory.Bicone.diagram.sizeOf_spec : ∀ {J : Type u₁} [inst : SizeOf J] (val : J), sizeOf (CategoryTheory.Bicone.diagram val) = 1 + sizeOf val
-- Mathlib.Topology.Category.Sequential
Sequential.homeoOfIso_apply : ∀ {X Y : Sequential} (f : X ≅ Y) (a : ↑X.toTop),
  (Sequential.homeoOfIso f) a = (CategoryTheory.ConcreteCategory.hom f.hom) a
-- Mathlib.Tactic.FunProp.Types
/-- Count the number of steps and stop when maxSteps is reached.  -/
Mathlib.Meta.FunProp.State.numSteps : Mathlib.Meta.FunProp.State → ℕ
-- Lean.Meta.Tactic.Simp.Main
/-- See `simpTarget`. This method assumes `mvarId` is not assigned, and we are already using `mvarId`s local context.  -/
Lean.Meta.simpTargetCore : Lean.MVarId →
  Lean.Meta.Simp.Context →
    optParam Lean.Meta.Simp.SimprocsArray #[] →
      optParam (Option Lean.Meta.Simp.Discharge) none →
        optParam Bool true → optParam Lean.Meta.Simp.Stats { } → Lean.MetaM (Option Lean.MVarId × Lean.Meta.Simp.Stats)
-- Mathlib.LinearAlgebra.Contraction
/-- As a matrix, `dualTensorHom` evaluated on a basis element of `M* ⊗ N` is a matrix with a
single one and zeros elsewhere  -/
toMatrix_dualTensorHom : ∀ {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] {m : Type u_7} {n : Type u_8}
  [inst_5 : Fintype m] [inst_6 : Finite n] [inst_7 : DecidableEq m] [inst_8 : DecidableEq n] (bM : Module.Basis m R M)
  (bN : Module.Basis n R N) (j : m) (i : n),
  (LinearMap.toMatrix bM bN) ((dualTensorHom R M N) (bM.coord j ⊗ₜ[R] bN i)) = Matrix.single i j 1
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
ComplexShape.Embedding.AreComplementary.symm : ∀ {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c}, e₁.AreComplementary e₂ → e₂.AreComplementary e₁
-- Mathlib.Data.Finsupp.MonomialOrder
MonomialOrder.mk.inj : ∀ {σ : Type u_1} {syn : Type u_2}
  {addCommMonoidSyn : autoParam (AddCommMonoid syn) MonomialOrder.addCommMonoidSyn._autoParam}
  {linearOrderSyn : autoParam (LinearOrder syn) MonomialOrder.linearOrderSyn._autoParam}
  {isOrderedAddMonoid_syn : autoParam (IsOrderedAddMonoid syn) MonomialOrder.isOrderedAddMonoid_syn._autoParam}
  {toSyn : (σ →₀ ℕ) ≃+ syn} {toSyn_monotone : Monotone ⇑toSyn}
  {wellFoundedLT_syn : autoParam (WellFoundedLT syn) MonomialOrder.wellFoundedLT_syn._autoParam} {syn_1 : Type u_2}
  {addCommMonoidSyn_1 : autoParam (AddCommMonoid syn_1) MonomialOrder.addCommMonoidSyn._autoParam}
  {linearOrderSyn_1 : autoParam (LinearOrder syn_1) MonomialOrder.linearOrderSyn._autoParam}
  {isOrderedAddMonoid_syn_1 : autoParam (IsOrderedAddMonoid syn_1) MonomialOrder.isOrderedAddMonoid_syn._autoParam}
  {toSyn_1 : (σ →₀ ℕ) ≃+ syn_1} {toSyn_monotone_1 : Monotone ⇑toSyn_1}
  {wellFoundedLT_syn_1 : autoParam (WellFoundedLT syn_1) MonomialOrder.wellFoundedLT_syn._autoParam},
  { syn := syn, addCommMonoidSyn := addCommMonoidSyn, linearOrderSyn := linearOrderSyn,
        isOrderedAddMonoid_syn := isOrderedAddMonoid_syn, toSyn := toSyn, toSyn_monotone := toSyn_monotone,
        wellFoundedLT_syn := wellFoundedLT_syn } =
      { syn := syn_1, addCommMonoidSyn := addCommMonoidSyn_1, linearOrderSyn := linearOrderSyn_1,
        isOrderedAddMonoid_syn := isOrderedAddMonoid_syn_1, toSyn := toSyn_1, toSyn_monotone := toSyn_monotone_1,
        wellFoundedLT_syn := wellFoundedLT_syn_1 } →
    syn = syn_1 ∧ addCommMonoidSyn ≍ addCommMonoidSyn_1 ∧ linearOrderSyn ≍ linearOrderSyn_1 ∧ toSyn ≍ toSyn_1