mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintInfo.mk.sizeOf_spec : ∀ (position : String.Pos.Raw) (label : Lean.Elab.InlayHintLabel) (kind? : Option Lean.Elab.InlayHintKind)
  (textEdits : Array Lean.Elab.InlayHintTextEdit) (tooltip? : Option String) (paddingLeft paddingRight : Bool),
  sizeOf
      { position := position, label := label, kind? := kind?, textEdits := textEdits, tooltip? := tooltip?,
        paddingLeft := paddingLeft, paddingRight := paddingRight } =
    1 + sizeOf position + sizeOf label + sizeOf kind? + sizeOf textEdits + sizeOf tooltip? + sizeOf paddingLeft +
      sizeOf paddingRight
-- Mathlib.Combinatorics.SimpleGraph.LapMatrix
SimpleGraph.degree_eq_sum_if_adj : ∀ {V : Type u_1} [inst : Fintype V] (G : SimpleGraph V) [inst_1 : DecidableRel G.Adj] {R : Type u_3}
  [inst_2 : AddCommMonoidWithOne R] (i : V), ↑(G.degree i) = ∑ j, if G.Adj i j then 1 else 0
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instHashableLitValue.hash : Lean.Compiler.LCNF.LitValue → UInt64
-- Lean.Linter.UnusedVariables
/-- The list of all `FVarId`s that are considered as being defined at this position.
This can have more than one element if multiple variables are declared by the same
syntax, such as the `h` in `if h : c then ... else ...`. We only report an unused variable
at this span if all variables in `aliases` are unused.  -/
Lean.Linter.UnusedVariables.FVarDefinition.aliases : Lean.Linter.UnusedVariables.FVarDefinition → Array Lean.FVarId
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.ι_map_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} {d : CategoryTheory.Limits.Cocone G} (hd : CategoryTheory.Limits.IsColimit d)
  (c : CategoryTheory.Limits.Cocone F) (α : G ⟶ F) (j : J) {Z : C} (h : c.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp (d.ι.app j) (CategoryTheory.CategoryStruct.comp (hd.map c α) h) =
    CategoryTheory.CategoryStruct.comp (α.app j) (CategoryTheory.CategoryStruct.comp (c.ι.app j) h)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.min?_erase_eq_iff_not_compare_eq_min? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, (t.erase k).min? = t.min? ↔ ∀ {km : α}, t.min? = some km → ¬cmp k km = Ordering.eq
-- Mathlib.Order.Interval.Set.Monotone
MonotoneOn.Ioc : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f g : α → β} {s : Set α},
  MonotoneOn f s → AntitoneOn g s → AntitoneOn (fun x => Set.Ioc (f x) (g x)) s
-- Mathlib.Algebra.Order.Monoid.Defs
/-- An ordered cancellative additive monoid is an ordered additive
monoid in which addition is cancellative and monotone.  -/
IsOrderedCancelAddMonoid : (α : Type u_2) → [AddCommMonoid α] → [Preorder α] → Prop
-- Mathlib.CategoryTheory.Bicategory.Free
_private.Mathlib.CategoryTheory.Bicategory.Free.0.CategoryTheory.FreeBicategory.liftHom.match_1.splitter : {B : Type u_1} →
  [inst : Quiver B] →
    (motive : (x x_1 : CategoryTheory.FreeBicategory B) → (x ⟶ x_1) → Sort u_3) →
      (x x_1 : CategoryTheory.FreeBicategory B) →
        (x_2 : x ⟶ x_1) →
          ((x x_3 : B) → (f : x ⟶ x_3) → motive x x_3 (CategoryTheory.FreeBicategory.Hom.of f)) →
            ((a : B) → motive a a (CategoryTheory.FreeBicategory.Hom.id a)) →
              ((x x_3 b : B) →
                  (f : CategoryTheory.FreeBicategory.Hom x b) →
                    (g : CategoryTheory.FreeBicategory.Hom b x_3) → motive x x_3 (f.comp g)) →
                motive x x_1 x_2
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem!_toList_rco_eq_add : ∀ {m n : ℤ} {i : ℕ}, i < (n - m).toNat → (m...n).toList[i]! = m + ↑i
-- Mathlib.Order.Hom.Bounded
TopHom.mk.inj : ∀ {α : Type u_6} {β : Type u_7} {inst : Top α} {inst_1 : Top β} {toFun : α → β} {map_top' : toFun ⊤ = ⊤}
  {toFun_1 : α → β} {map_top'_1 : toFun_1 ⊤ = ⊤},
  { toFun := toFun, map_top' := map_top' } = { toFun := toFun_1, map_top' := map_top'_1 } → toFun = toFun_1
-- Mathlib.Combinatorics.Enumerative.DyckWord
/-- A property stating that `p` is nonempty and strictly positive in its interior,
i.e. is of the form `(x)` with `x` a Dyck word.  -/
DyckWord.IsNested : DyckWord → Prop
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeRule.Rewrites.below.head : ∀ {T : Type u_1} {N : Type u_2} {r : ContextFreeRule T N}
  {motive : (a a_1 : List (Symbol T N)) → r.Rewrites a a_1 → Prop} (s : List (Symbol T N)),
  ContextFreeRule.Rewrites.below ⋯
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
MeasureTheory.charFun_map_mul_comp : ∀ {X : Type u_3} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {f : X → ℝ},
  AEMeasurable f μ →
    ∀ (r t : ℝ),
      MeasureTheory.charFun (MeasureTheory.Measure.map (fun x => r * f x) μ) t =
        MeasureTheory.charFun (MeasureTheory.Measure.map f μ) (r * t)
-- Std.Data.DTreeMap.Internal.Operations
_private.Std.Data.DTreeMap.Internal.Operations.0.Std.DTreeMap.Internal.Impl.link.match_3.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (r' : Std.DTreeMap.Internal.Impl α β) →
      (szr : ℕ) →
        (k'' : α) →
          (v'' : β k'') →
            (l'' r'' : Std.DTreeMap.Internal.Impl α β) →
              (motive :
                  Std.DTreeMap.Internal.Impl.Tree α β
                      (r'.size + 1 + (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'').size) →
                    Sort u_3) →
                (x :
                    Std.DTreeMap.Internal.Impl.Tree α β
                      (r'.size + 1 + (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'').size)) →
                  ((ℓ : Std.DTreeMap.Internal.Impl α β) →
                      (hℓ₁ : ℓ.Balanced) →
                        (hℓ₂ : ℓ.size = r'.size + 1 + (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'').size) →
                          motive { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ }) →
                    motive x
-- Mathlib.Algebra.Group.Hom.Instances
/-- The expression `fun m q ↦ f m (g q)` as a `MonoidHom`.

Note that the expression `fun q n ↦ f (g q) n` is simply `MonoidHom.comp`.  -/
MonoidHom.compl₂ : {M : Type uM} →
  {N : Type uN} →
    {P : Type uP} →
      {Q : Type uQ} →
        [inst : MulOneClass M] →
          [inst_1 : MulOneClass N] →
            [inst_2 : CommMonoid P] → [inst_3 : MulOneClass Q] → (M →* N →* P) → (Q →* N) → M →* Q →* P
-- Init.Data.UInt.Lemmas
USize.toUInt8_ofNat' : ∀ (n : ℕ), (USize.ofNat n).toUInt8 = UInt8.ofNat n
-- Mathlib.Combinatorics.Additive.Corner.Defs
/-- **Alias** of the forward direction of `isCorner_image`. -/
IsCorner.of_image : ∀ {G : Type u_1} {H : Type u_2} [inst : AddCommMonoid G] [inst_1 : AddCommMonoid H] {A : Set (G × G)} {s : Set G}
  {t : Set H} {f : G → H} {x₁ y₁ x₂ y₂ : G},
  IsAddFreimanIso 2 s t f →
    A ⊆ s ×ˢ s →
      x₁ ∈ s →
        y₁ ∈ s → x₂ ∈ s → y₂ ∈ s → IsCorner (Prod.map f f '' A) (f x₁) (f y₁) (f x₂) (f y₂) → IsCorner A x₁ y₁ x₂ y₂
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.eLpNorm_densityProcess_le : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] {κ : ProbabilityTheory.Kernel α (γ × β)}
  {ν : ProbabilityTheory.Kernel α γ},
  κ.fst ≤ ν →
    ∀ (n : ℕ) (a : α) (s : Set β), MeasureTheory.eLpNorm (fun x => κ.densityProcess ν n a x s) 1 (ν a) ≤ (ν a) Set.univ
-- Mathlib.RingTheory.Derivation.Basic
/-- For a tower `R → A → B → M`, the precomposition defined in `compAlgebraMap`
is a `B`-linear map.  -/
Derivation.compAlgebraMapL : (R : Type u_1) →
  (A : Type u_2) →
    (B : Type u_3) →
      (M : Type u_4) →
        [inst : CommSemiring R] →
          [inst_1 : CommSemiring A] →
            [inst_2 : CommSemiring B] →
              [inst_3 : AddCommMonoid M] →
                [inst_4 : Algebra R A] →
                  [inst_5 : Algebra R B] →
                    [inst_6 : Module A M] →
                      [inst_7 : Module B M] →
                        [inst_8 : Module R M] →
                          [inst_9 : Algebra A B] →
                            [IsScalarTower R A B] →
                              [inst_11 : IsScalarTower A B M] →
                                [inst_12 : IsScalarTower R B M] → Derivation R B M →ₗ[B] Derivation R A M
-- Init.Data.Vector.Basic
/-- Get an element of a vector using a `Fin` index.  -/
Vector.get : {α : Type u_1} → {n : ℕ} → Vector α n → Fin n → α
-- Mathlib.Data.Finset.NAry
/-- Symmetric statement to `Finset.image_image₂_right_comm`.  -/
Finset.image_image₂_distrib_right : ∀ {α : Type u_1} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} [inst : DecidableEq β']
  [inst_1 : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β} [inst_2 : DecidableEq δ] {g : γ → δ}
  {f' : α → β' → δ} {g' : β → β'},
  (∀ (a : α) (b : β), g (f a b) = f' a (g' b)) →
    Finset.image g (Finset.image₂ f s t) = Finset.image₂ f' s (Finset.image g' t)
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.ConstPromiseVal.nestedConsts : Lean.Environment.ConstPromiseVal✝ → Lean.VisibilityMap✝ Lean.AsyncConsts✝
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.tan_arcsin : ∀ (x : ℝ), Real.tan (Real.arcsin x) = x / √(1 - x ^ 2)
-- Mathlib.Topology.Order.Lattice
ContinuousOn.finset_sup'_apply : ∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] {ι : Type u_3}
  [inst_2 : SemilatticeSup L] [ContinuousSup L] {s : Finset ι} {f : ι → X → L} {t : Set X} (hne : s.Nonempty),
  (∀ i ∈ s, ContinuousOn (f i) t) → ContinuousOn (fun a => s.sup' hne fun x => f x a) t
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.Hom.comp_hom : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {A : Type u_5} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift D A] {F G H : CategoryTheory.SingleFunctors C D A} (α : F.Hom G) (β : G.Hom H)
  (a : A), (α.comp β).hom a = CategoryTheory.CategoryStruct.comp (α.hom a) (β.hom a)
-- Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
/-- `F : C ⥤ D ⥤ E` preserves finite limits if it does for each `d : D`.  -/
CategoryTheory.preservesFiniteColimits_of_evaluation : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} E]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)),
  (∀ (d : D), CategoryTheory.Limits.PreservesFiniteColimits (F.comp ((CategoryTheory.evaluation D E).obj d))) →
    CategoryTheory.Limits.PreservesFiniteColimits F
-- Std.Do.WP.SimpLemmas
_private.Std.Do.WP.SimpLemmas.0.EStateM.tryCatch.match_1.splitter : {ε σ α : Type u_1} →
  (motive : EStateM.Result ε σ α → Sort u_2) →
    (x : EStateM.Result ε σ α) →
      ((e : ε) → (s : σ) → motive (EStateM.Result.error e s)) →
        ((ok : EStateM.Result ε σ α) → (∀ (e : ε) (s : σ), ok = EStateM.Result.error e s → False) → motive ok) →
          motive x
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isEmpty_iff_forall_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = true ↔ ∀ (a : α), t.contains a = false
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.size_inter_le_size_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α], (↑m₁).WF → (↑m₂).WF → (↑(m₁.inter m₂)).size ≤ (↑m₁).size
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get!_union : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β] {k : α},
  Std.DTreeMap.Const.get! (t₁ ∪ t₂) k = Std.DTreeMap.Const.getD t₂ k (Std.DTreeMap.Const.get! t₁ k)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α Unit} [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {l : List α} {k : α}, k ∈ m → (m.insertManyIfNewUnit l).getKey? k = m.getKey? k
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Line.mk.sizeOf_spec : ∀ {α : Type u_5} {ι : Type u_6} [inst : SizeOf α] [inst_1 : SizeOf ι] (idxFun : ι → Option α)
  (proper : ∃ i, idxFun i = none), sizeOf { idxFun := idxFun, proper := proper } = 1 + sizeOf proper
-- Mathlib.Geometry.Manifold.BumpFunction
SmoothBumpFunction.ball_subset : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {c : M}
  (f : SmoothBumpFunction I c), Metric.ball (↑(extChartAt I c) c) f.rOut ∩ Set.range ↑I ⊆ (extChartAt I c).target
-- Mathlib.Algebra.MvPolynomial.Division
MvPolynomial.divMonomial_add_modMonomial : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (x : MvPolynomial σ R) (s : σ →₀ ℕ),
  (MvPolynomial.monomial s) 1 * x.divMonomial s + x.modMonomial s = x
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.hasColimit_of_hasLimit_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasLimit F.op], CategoryTheory.Limits.HasColimit F
-- Lean.Meta.Tactic.Grind.Types
/-- The `grind` state for a goal, excluding the metavariable.

This separation from `Goal` allows multiple goals with different metavariables to share
the same `GoalState`. This is useful for automation such as symbolic simulation, where applying
theorems create multiple goals that inherit the same E-graph, congruence closure state, and other
accumulated facts.
 -/
Lean.Meta.Grind.GoalState : Type
-- Mathlib.CategoryTheory.Join.Basic
/-- A natural transformation `Fᵣ ⟶ Gᵣ` induces a natural transformation
`mapPair H Fᵣ ⟶ mapPair H Gᵣ` for every `H : C ⥤ E`.  -/
CategoryTheory.Join.mapWhiskerLeft : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            {E' : Type u₄} →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} E'] →
                (H : CategoryTheory.Functor C E) →
                  {Fᵣ Gᵣ : CategoryTheory.Functor D E'} →
                    (Fᵣ ⟶ Gᵣ) → (CategoryTheory.Join.mapPair H Fᵣ ⟶ CategoryTheory.Join.mapPair H Gᵣ)
-- Batteries.Recycling.RBTree.Basic
/-- `O(n₂ * log (n₁ + n₂))`. Merges the maps `t₁` and `t₂`, if a key `a : α` exists in both,
then use `mergeFn a b₁ b₂` to produce the new merged value.
 -/
RBTree.RBMap.mergeWith : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} → (α → β → β → β) → RBTree.RBMap α β cmp → RBTree.RBMap α β cmp → RBTree.RBMap α β cmp
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.biUnion_le : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I)
  (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J), π.biUnion πi ≤ π
-- Mathlib.Order.ConditionallyCompletePartialOrder.Basic
/-- The supremum of a singleton is the element of the singleton  -/
csSup_singleton : ∀ {α : Type u_1} [inst : ConditionallyCompletePartialOrderSup α] (a : α), sSup {a} = a
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.contains_of_contains_map : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} {γ : α → Type w}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] {f : (a : α) → β a → γ a} {k : α},
  (Std.ExtDHashMap.map f m).contains k = true → m.contains k = true
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.dropLast.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h_1 : Unit → motive []) (h_2 : (head : α) → motive [head])
  (h_3 : (a : α) → (as : List α) → motive (a :: as)),
  (match [] with
    | [] => h_1 ()
    | [head] => h_2 head
    | a :: as => h_3 a as) =
    h_1 ()
-- Mathlib.Computability.Primrec.List
_private.Mathlib.Computability.Primrec.List.0.list_reverse' : ∀ {β : Type u_2} [inst : Primcodable β] (H : Nat.Primrec fun n => Encodable.encode (Encodable.decode n)),
  Primrec List.reverse
-- Lean.Declaration
Lean.mkRecName : Lean.Name → Lean.Name
-- Mathlib.Combinatorics.Colex
Finset.Colex.le_iff_max'_mem : ∀ {α : Type u_1} [inst : LinearOrder α] {s t : Colex (Finset α)},
  s ≤ t ↔ ∀ (h : s ≠ t), (symmDiff (ofColex s) (ofColex t)).max' ⋯ ∈ ofColex t
-- Std.Data.Iterators.Lemmas.Consumers.Monadic.Collect
Std.IterM.Equiv.toListRev_eq : ∀ {m : Type u_1 → Type u_2} {α₁ β α₂ : Type u_1} [inst : Monad m] [inst_1 : LawfulMonad m]
  [inst_2 : Std.Iterator α₁ m β] [inst_3 : Std.Iterator α₂ m β] [Std.Iterators.Finite α₁ m] [Std.Iterators.Finite α₂ m]
  {ita : Std.IterM m β} {itb : Std.IterM m β}, ita.Equiv itb → ita.toListRev = itb.toListRev
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor_map_right_right : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor D T) (Y : T) (X : D)
  {X_1 Y_1 : CategoryTheory.StructuredArrow X (CategoryTheory.StructuredArrow.proj Y F)} (g : X_1 ⟶ Y_1),
  ((CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor F Y X).map g).right.right = g.right.right
-- Lean.Elab.App
_private.Lean.Elab.App.0.Lean.Elab.Term.elabAppLValsAux.loop : Array Lean.Elab.Term.NamedArg →
  Array Lean.Elab.Term.Arg →
    Option Lean.Expr → Bool → Bool → Lean.Expr → List Lean.Elab.Term.LVal → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
FixedDetMatrices.reduce_rec.eq_def : ∀ {m : ℤ} {C : FixedDetMatrix (Fin 2) ℤ m → Sort u_3} (base : (A : FixedDetMatrix (Fin 2) ℤ m) → ↑A 1 0 = 0 → C A)
  (step : (A : FixedDetMatrix (Fin 2) ℤ m) → ↑A 1 0 ≠ 0 → C (FixedDetMatrices.reduceStep A) → C A)
  (A : FixedDetMatrix (Fin 2) ℤ m),
  FixedDetMatrices.reduce_rec base step A =
    if h : ↑A 1 0 = 0 then base A h
    else step A h (FixedDetMatrices.reduce_rec base step (FixedDetMatrices.reduceStep A))
-- Mathlib.Algebra.Ring.Subring.IntPolynomial
Polynomial.int_coeff_eq : ∀ {K : Type u_1} [inst : Field K] (R : Subring K) (P : Polynomial K) (hP : ∀ (n : ℕ), P.coeff n ∈ R) (n : ℕ),
  ↑((Polynomial.int R P hP).coeff n) = P.coeff n
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
HasSum.sigma : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] [ContinuousAdd α]
  [RegularSpace α] {γ : β → Type u_4} {f : (b : β) × γ b → α} {g : β → α} {a : α},
  HasSum f a → (∀ (b : β), HasSum (fun c => f ⟨b, c⟩) (g b)) → HasSum g a
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get?_of_isEmpty : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α}, t.isEmpty = true → t.get? a = none
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
ModelWithCorners.interiorPoint_inl : ∀ {𝕜 : 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] {M' : Type u_5} [inst_6 : TopologicalSpace M']
  [inst_7 : ChartedSpace H M'] (x : M), I.IsInteriorPoint x → I.IsInteriorPoint (Sum.inl x)
-- Mathlib.CategoryTheory.Simple
CategoryTheory.epi_from_simple_zero_of_not_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C}
  [CategoryTheory.Simple X] {f : X ⟶ Y} [CategoryTheory.Epi f], (CategoryTheory.IsIso f → False) → f = 0
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.equivMonComonUnitIsoAppX_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M : CategoryTheory.Bimon C),
  M.equivMonComonUnitIsoAppX.hom.hom = CategoryTheory.CategoryStruct.id M.X.X
-- Mathlib.Algebra.DirectSum.Module
/-- Scalar multiplication commutes with the inclusion of each component into the direct sum.  -/
DirectSum.of_smul : ∀ (R : Type u) [inst : Semiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [inst_3 : DecidableEq ι] (i : ι) (c : R) (x : M i),
  (DirectSum.of M i) (c • x) = c • (DirectSum.of M i) x
-- Mathlib.RingTheory.MvPolynomial.Ideal
MvPolynomial.mem_pow_idealOfVars_iff' : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (n : ℕ) (p : MvPolynomial σ R),
  p ∈ MvPolynomial.idealOfVars σ R ^ n ↔ ∀ (x : σ →₀ ℕ), Finsupp.degree x < n → MvPolynomial.coeff x p = 0
-- Mathlib.Topology.Instances.Rat
NNRat.instContinuousSMulRatReal : ContinuousSMul ℚ ℝ
-- Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated
/-- If a discrete group acts on a T2 space `X` such that `X × X` is compactly
generated, and if the action is continuous in the second variable, then the action is properly
discontinuous if and only if it is proper. This is in particular true if `X` is first-countable or
weakly locally compact.  -/
properlyDiscontinuousSMul_iff_properSMul : ∀ {G : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] [inst_1 : Group G] [inst_2 : TopologicalSpace G]
  [inst_3 : MulAction G X] [CompactlyGeneratedSpace (X × X)] [T2Space X] [DiscreteTopology G] [ContinuousConstSMul G X],
  ProperlyDiscontinuousSMul G X ↔ ProperSMul G X
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Real.differentiable_iteratedDeriv_cosh : ∀ (n : ℕ), Differentiable ℝ (iteratedDeriv n Real.cosh)
-- Mathlib.Analysis.Real.OfDigits
/-- A generalization of the identity `0.(9) = 1` to arbitrary positional numeral systems.  -/
Real.ofDigits_const_last_eq_one : ∀ (b : ℕ) [NeZero b], (Real.ofDigits fun x => Fin.last b) = 1
-- Mathlib.CategoryTheory.FiberedCategory.Cocartesian
CategoryTheory.Functor.IsCocartesian.map_isHomLift : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [inst_2 : p.IsCocartesian f φ] {b' : 𝒳}
  (φ' : a ⟶ b') [inst_3 : p.IsHomLift f φ'],
  p.IsHomLift (CategoryTheory.CategoryStruct.id S) (CategoryTheory.Functor.IsCocartesian.map p f φ φ')
-- Mathlib.Order.Heyting.Boundary
Coheyting.boundary_bot : ∀ {α : Type u_1} [inst : CoheytingAlgebra α], Coheyting.boundary ⊥ = ⊥
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
AddCommMonCat.FilteredColimits.colimitAddCommMonoid : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [inst_1 : CategoryTheory.IsFiltered J] →
      (F : CategoryTheory.Functor J AddCommMonCat) → AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M F)
-- Mathlib.Control.Basic
map_seq : ∀ {α β γ : Type u} {F : Type u → Type v} [inst : Applicative F] [LawfulApplicative F] (f : β → γ) (x : F (α → β))
  (y : F α), f <$> (x <*> y) = (fun x => f ∘ x) <$> x <*> y
-- Mathlib.Data.Nat.Factorial.DoubleFactorial
_private.Mathlib.Data.Nat.Factorial.DoubleFactorial.0.Nat.factorial.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.Data.Stream.Init
Stream'.map_map : ∀ {α : Type u} {β : Type v} {δ : Type w} (g : β → δ) (f : α → β) (s : Stream' α),
  Stream'.map g (Stream'.map f s) = Stream'.map (g ∘ f) s
-- Init.Data.UInt.Lemmas
USize.not_lt : ∀ {a b : USize}, ¬a < b ↔ b ≤ a