mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Ring.WithTop
WithTop.pow_lt_top : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MonoidWithZero α] [inst_2 : NoZeroDivisors α] [inst_3 : Nontrivial α]
  {x : WithTop α} {n : ℕ} [inst_4 : Preorder α], x < ⊤ → x ^ n < ⊤
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.IsEffectiveEquivalenceRelation.nonempty_effectiveEquivalenceRelation : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {R A : C} {p₁ p₂ : R ⟶ A}
  [self : CategoryTheory.IsEffectiveEquivalenceRelation p₁ p₂],
  Nonempty (CategoryTheory.EffectiveEquivalenceRelation p₁ p₂)
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.reverse.eq_1 : ∀ {α : Type u_1}, FreeMonoid.reverse = List.reverse
-- Mathlib.GroupTheory.Exponent
Monoid.exponent_ne_zero_iff_range_orderOf_finite : ∀ {G : Type u} [inst : Monoid G], (∀ (g : G), 0 < orderOf g) → (Monoid.exponent G ≠ 0 ↔ (Set.range orderOf).Finite)
-- Mathlib.Topology.Algebra.Group.CompactOpen
ContinuousAddMonoidHom.locallyCompactSpace_of_equicontinuousAt : ∀ {X : Type u_7} {Y : Type u_8} [inst : TopologicalSpace X] [inst_1 : AddGroup X] [IsTopologicalAddGroup X]
  [inst_3 : UniformSpace Y] [inst_4 : AddCommGroup Y] [IsUniformAddGroup Y] [T0Space Y] [CompactSpace Y] (U : Set X)
  (V : Set Y), IsCompact U → V ∈ nhds 0 → EquicontinuousAt (fun f => ⇑↑f) 0 → LocallyCompactSpace (X →ₜ+ Y)
-- Lean.Parser.Command
Lean.Parser.Command.docs_to_verso.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.Vector.Lemmas
Vector.set!_mk : ∀ {α : Type u_1} {n : ℕ} {xs : Array α} (h : xs.size = n) {i : ℕ} {x : α},
  (Vector.mk xs h).set! i x = Vector.mk (xs.set! i x) ⋯
-- Init.Data.SInt.Lemmas
Int64.toUInt64_ofNat : ∀ {n : ℕ}, Int64.toUInt64 (OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.RingTheory.Extension.Cotangent.Basis
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.instNontrivialT : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type u_4}
  {P : Algebra.Generators R S ι} {σ : Type u_5} {b : Module.Basis σ S P.toExtension.Cotangent}
  (D : Algebra.Generators.PresentationOfFreeCotangent.Aux✝ P b) [Nontrivial S],
  Nontrivial (Algebra.Generators.PresentationOfFreeCotangent.Aux.T✝ D)
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.smulRight.congr_simp : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : CommSemiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : TopologicalSpace R] [inst_6 : (i : ι) → TopologicalSpace (M₁ i)]
  [inst_7 : TopologicalSpace M₂] [inst_8 : ContinuousSMul R M₂] (f f_1 : ContinuousMultilinearMap R M₁ R),
  f = f_1 → ∀ (z z_1 : M₂), z = z_1 → f.smulRight z = f_1.smulRight z_1
-- Mathlib.Analysis.Normed.Module.Ray
/-- If `x` and `y` are on the same ray, then the triangle inequality becomes the equality: the norm
of `x + y` is the sum of the norms of `x` and `y`. The converse is true for a strictly convex
space.  -/
SameRay.norm_add : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {x y : E},
  SameRay ℝ x y → ‖x + y‖ = ‖x‖ + ‖y‖
-- Mathlib.Tactic.ModCases
/-- The end point is that once we have reduced to `∃ m, n ≤ m < n ∧ a ≡ m (mod n)`
there are no more cases to consider.
 -/
Mathlib.Tactic.ModCases.NatMod.onModCases_stop : (p : Sort u_1) → (n a : ℕ) → Mathlib.Tactic.ModCases.NatMod.OnModCases n a n p
-- Mathlib.Analysis.Normed.Group.Defs
/-- A normed group is an additive group endowed with a norm for which `dist x y = ‖-x + y‖` defines
a metric space structure.  -/
NormedAddGroup : Type u_8 → Type u_8
-- Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
/-- The class of monomorphisms modulo a Serre class: given a
Serre class `P : ObjectProperty C`, this is the class of morphisms `f`
such that `kernel f` satisfies `P`.  -/
CategoryTheory.ObjectProperty.monoModSerre : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      (P : CategoryTheory.ObjectProperty C) → [P.IsSerreClass] → CategoryTheory.MorphismProperty C
-- Mathlib.LinearAlgebra.Eigenspace.Basic
/-- If an invariant subspace `p` of an endomorphism `f` is disjoint from the `μ`-eigenspace of `f`,
then the restriction of `f` to `p` has trivial `μ`-eigenspace.  -/
Module.End.eigenspace_restrict_eq_bot : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {p : Submodule R M} (hfp : ∀ x ∈ p, f x ∈ p) {μ : R},
  Disjoint (f.eigenspace μ) p → Module.End.eigenspace (LinearMap.restrict f hfp) μ = ⊥
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.coeff_coe_powerSeries : ∀ {R : Type u_1} [inst : Semiring R] (x : PowerSeries R) (n : ℕ),
  ((HahnSeries.ofPowerSeries ℤ R) x).coeff ↑n = (PowerSeries.coeff n) x
-- Init.Data.Dyadic.Basic
Dyadic.blt_iff_toRat : ∀ {x y : Dyadic}, x.blt y = true ↔ x.toRat < y.toRat
-- Mathlib.Data.Complex.Basic
Complex.div_ratCast : ∀ (z : ℂ) (x : ℚ), z / ↑x = { re := z.re / ↑x, im := z.im / ↑x }
-- Mathlib.Data.Multiset.ZeroCons
Multiset.attach_zero : ∀ {α : Type u_1}, Multiset.attach 0 = 0
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.size_modify : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} {k : α}
  {f : β → β}, (Std.DTreeMap.Const.modify t k f).size = t.size
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.case.injEq : ∀ (tid : Lean.Name) (x : Lean.IR.VarId) (xType : Lean.IR.IRType) (cs : Array Lean.IR.Alt) (tid_1 : Lean.Name)
  (x_1 : Lean.IR.VarId) (xType_1 : Lean.IR.IRType) (cs_1 : Array Lean.IR.Alt),
  (Lean.IR.FnBody.case tid x xType cs = Lean.IR.FnBody.case tid_1 x_1 xType_1 cs_1) =
    (tid = tid_1 ∧ x = x_1 ∧ xType = xType_1 ∧ cs = cs_1)
-- Mathlib.AlgebraicTopology.SimplexCategory.Rev
SimplexCategory.revEquivalence_counitIso : SimplexCategory.revEquivalence.counitIso = SimplexCategory.revCompRevIso
-- Mathlib.Data.List.Basic
/-- A version of `getElem_map` that can be used for rewriting.  -/
List.getElem_map_rev : ∀ {α : Type u} {β : Type v} (f : α → β) {l : List α} {n : ℕ} {h : n < l.length}, f l[n] = (List.map f l)[n]
-- Mathlib.Order.Interval.Finset.Basic
/-- `Finset.cons` version of `Finset.Ioc_insert_left`.  -/
Finset.Icc_eq_cons_Ioc : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] {a b : α},
  a ≤ b → Finset.Icc a b = Finset.cons a (Finset.Ioc a b) ⋯
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey!_empty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α],
  ∅.minKey! = default
-- Mathlib.Order.Heyting.Basic
/-- Pullback a `BiheytingAlgebra` along an injection.  -/
Function.Injective.biheytingAlgebra : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Max α] →
      [inst_1 : Min α] →
        [inst_2 : LE α] →
          [inst_3 : LT α] →
            [inst_4 : Top α] →
              [inst_5 : Bot α] →
                [inst_6 : Compl α] →
                  [inst_7 : HNot α] →
                    [inst_8 : HImp α] →
                      [inst_9 : SDiff α] →
                        [inst_10 : BiheytingAlgebra β] →
                          (f : α → β) →
                            Function.Injective f →
                              (∀ {x y : α}, f x ≤ f y ↔ x ≤ y) →
                                (∀ {x y : α}, f x < f y ↔ x < y) →
                                  (∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) →
                                    (∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) →
                                      f ⊤ = ⊤ →
                                        f ⊥ = ⊥ →
                                          (∀ (a : α), f aᶜ = (f a)ᶜ) →
                                            (∀ (a : α), f (￢a) = ￢f a) →
                                              (∀ (a b : α), f (a ⇨ b) = f a ⇨ f b) →
                                                (∀ (a b : α), f (a \ b) = f a \ f b) → BiheytingAlgebra α
-- Mathlib.Algebra.Algebra.Rat
DivisionRing.toRatAlgebra : {R : Type u_2} → [inst : DivisionRing R] → [CharZero R] → Algebra ℚ R
-- Mathlib.SetTheory.ZFC.Class
Class.fval_ex : ∀ (F A : Class.{u}), F ′ A ∈ Class.univ
-- Mathlib.NumberTheory.NumberField.Discriminant.Basic
/-- The Minkowski lower bound `n^{2n}/((4/pi)^{2r_2}*n!^2)` for the absolute value of the discriminant
of a number field of degree n.
 -/
NumberField.abs_discr_ge' : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  ↑(Module.finrank ℚ K) ^ (2 * Module.finrank ℚ K) /
      ((4 / Real.pi) ^ (2 * NumberField.InfinitePlace.nrComplexPlaces K) * ↑(Module.finrank ℚ K).factorial ^ 2) ≤
    ↑|NumberField.discr K|
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
/-- If a subalgebra is contained in a finite-dimensional
subalgebra with the same or smaller dimension, they are equal.  -/
Subalgebra.eq_of_le_of_finrank_le : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Ring L] [inst_2 : Algebra K L] {F E : Subalgebra K L}
  [hfin : FiniteDimensional K ↥E], F ≤ E → Module.finrank K ↥E ≤ Module.finrank K ↥F → F = E
-- Lean.DocString.Parser
/-- Parses a paragraph (that is, a sequence of otherwise-undecorated inlines).  -/
Lean.Doc.Parser.para : Lean.Doc.Parser.BlockCtxt → Lean.Parser.ParserFn
-- Mathlib.NumberTheory.NumberField.Discriminant.Different
NumberField.discr_dvd_discr : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (L : Type u_3) [inst_2 : Field L] [inst_3 : NumberField L]
  [Algebra K L], NumberField.discr K ∣ NumberField.discr L
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get_insert : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α] (h : (↑m).WF) {k a : α} {v : β k} {h₁ : (m.insert k v).contains a = true},
  (m.insert k v).get a h₁ = if h₂ : (k == a) = true then cast ⋯ v else m.get a ⋯
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite
CategoryTheory.Limits.CreatesFiniteCoproducts.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          autoParam ((J : Type) → [Fintype J] → CategoryTheory.CreatesColimitsOfShape (CategoryTheory.Discrete J) F)
              CategoryTheory.Limits.CreatesFiniteCoproducts.creates._autoParam →
            CategoryTheory.Limits.CreatesFiniteCoproducts F
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup_const : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β},
  s.Nonempty → ∀ (c : α), (s.sup fun x => c) = c
-- Mathlib.CategoryTheory.Subobject.Limits
/-- The isomorphism between the kernel of `f ≫ g` and the kernel of `g`,
when `f` is an isomorphism.
 -/
CategoryTheory.Limits.kernelSubobjectIsoComp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {X' : C} →
          (f : X' ⟶ X) →
            [inst_2 : CategoryTheory.IsIso f] →
              (g : X ⟶ Y) →
                [inst_3 : CategoryTheory.Limits.HasKernel g] →
                  CategoryTheory.Subobject.underlying.obj
                      (CategoryTheory.Limits.kernelSubobject (CategoryTheory.CategoryStruct.comp f g)) ≅
                    CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject g)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.coe_toIcoMod : ∀ (θ ψ : ℝ), ↑(toIcoMod Real.two_pi_pos ψ θ) = ↑θ
-- Lean.Linter.Init
/-- The `envLinterSnapshotExt` extension saves the state of all (Boolean-valued) `Lean.Option`s
associated with environment linters.
 -/
Lean.Linter.envLinterSnapshotExt : Lean.MapDeclarationExtension Lean.Linter.EnvLinterSnapshot
-- Mathlib.Tactic.LinearCombinationPrime
Mathlib.Tactic.LinearCombinationPrime.inv_pf : ∀ {α : Type u_1} {a b : α} [inst : Inv α], a = b → a⁻¹ = b⁻¹
-- Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
/-- Given an open set `s` in a finite-dimensional real normed vector space, there exists a smooth
function with values in `[0, 1]` whose support is exactly `s`.  -/
IsOpen.exists_contDiff_support_eq : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ∞} {s : Set E},
  IsOpen s → ∃ f, Function.support f = s ∧ ContDiff ℝ (↑n) f ∧ Set.range f ⊆ Set.Icc 0 1
-- Lean.Message
/-- The list of messages not already reported, in insertion order.  -/
Lean.MessageLog.unreported : Lean.MessageLog → Lean.PersistentArray Lean.Message
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.CondIndepSets.union : ∀ {Ω : Type u_1} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω}
  [inst_1 : MeasureTheory.IsFiniteMeasure μ] {s₁ s₂ s' : Set (Set Ω)},
  ProbabilityTheory.CondIndepSets m' hm' s₁ s' μ →
    ProbabilityTheory.CondIndepSets m' hm' s₂ s' μ → ProbabilityTheory.CondIndepSets m' hm' (s₁ ∪ s₂) s' μ
-- Mathlib.CategoryTheory.Category.Bipointed
/-- The equivalence between `Bipointed` and itself induced by `Prod.swap` both ways.  -/
Bipointed.swapEquiv : Bipointed ≌ Bipointed
-- Mathlib.Order.Interval.Finset.Defs
OrderDual.instLocallyFiniteOrderBot.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α],
  OrderDual.instLocallyFiniteOrderBot =
    { finsetIio := fun a => Finset.Ioi (OrderDual.ofDual a), finsetIic := fun a => Finset.Ici (OrderDual.ofDual a),
      finset_mem_Iic := ⋯, finset_mem_Iio := ⋯ }
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.Point.mk.injEq : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {point : WeierstrassCurve.Jacobian.PointClass R}
  (nonsingular : W'.NonsingularLift point) (point_1 : WeierstrassCurve.Jacobian.PointClass R)
  (nonsingular_1 : W'.NonsingularLift point_1),
  ({ point := point, nonsingular := nonsingular } = { point := point_1, nonsingular := nonsingular_1 }) =
    (point = point_1)
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
QuadraticForm.polarBilin_tmul : ∀ {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : AddCommGroup M₁] [inst_3 : AddCommGroup M₂] [inst_4 : Algebra R A] [inst_5 : Module R M₁]
  [inst_6 : Module A M₁] [inst_7 : SMulCommClass R A M₁] [inst_8 : IsScalarTower R A M₁] [inst_9 : Module R M₂]
  [inst_10 : Invertible 2] [inst_11 : Invertible 2] (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂),
  QuadraticMap.polarBilin (Q₁.tmul Q₂) =
    ⅟2 • LinearMap.BilinForm.tmul (QuadraticMap.polarBilin Q₁) (QuadraticMap.polarBilin Q₂)
-- Mathlib.Combinatorics.SimpleGraph.Cayley
SimpleGraph.addCayley_adj : ∀ {M : Type u_1} (s : Set M) [inst : AddGroup M] (u v : M),
  (SimpleGraph.addCayley s).Adj u v ↔ u ≠ v ∧ (-u + v ∈ s ∨ -v + u ∈ s)
-- Mathlib.Combinatorics.Quiver.Path.Weight
/-- The additive weight of a path is the sum of the weights of its edges.  -/
Quiver.Path.addWeight : {V : Type u_1} →
  [inst : Quiver V] → {R : Type u_3} → [AddMonoid R] → ({i j : V} → (i ⟶ j) → R) → {i j : V} → Quiver.Path i j → R
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.foldr_eq_foldr_toList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} {δ : Type w} {f : α → β → δ → δ}
  {init : δ}, Std.TreeMap.Raw.foldr f init t = List.foldr (fun a b => f a.1 a.2 b) init t.toList
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.gaussianReal_zero_var : ∀ (μ : ℝ), ProbabilityTheory.gaussianReal μ 0 = MeasureTheory.Measure.dirac μ
-- Mathlib.Tactic.NormNum.Pow
/-- Proves `Nat.pow a b = c` where `a` and `b` are raw nat literals. This could be done by just
`rfl` but the kernel does not have a special case implementation for `Nat.pow` so this would
proceed by unary recursion on `b`, which is too slow and also leads to deep recursion.

We instead do the proof by binary recursion, but this can still lead to deep recursion,
so we use an additional trick to do binary subdivision on `log2 b`. As a result this produces
a proof of depth `log (log b)` which will essentially never overflow before the numbers involved
themselves exceed memory limits.
 -/
Mathlib.Meta.NormNum.evalNatPow : (a b : Q(ℕ)) → OptionT Lean.CoreM ((c : Q(ℕ)) × Q(«$a».pow «$b» = «$c»))
-- Mathlib.Computability.StateTransition
_private.Mathlib.Computability.StateTransition.0.StateTransition.Respects.match_1.splitter : {σ₁ : Type u_1} →
  (motive : Option σ₁ → Sort u_2) → (x : Option σ₁) → ((b₁ : σ₁) → motive (some b₁)) → (Unit → motive none) → motive x
-- Init.Data.Nat.Bitwise.Basic
Nat.shiftRight_eq_div_pow : ∀ (m n : ℕ), m >>> n = m / 2 ^ n
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.ker_ideal_of_isPullback_of_isOpenImmersion : ∀ {X Y U V : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (f' : U ⟶ V) (iU : U ⟶ X) (iV : V ⟶ Y)
  [inst : AlgebraicGeometry.IsOpenImmersion iV] [AlgebraicGeometry.QuasiCompact f],
  CategoryTheory.IsPullback f' iU iV f →
    ∀ (W : ↑V.affineOpens),
      (AlgebraicGeometry.Scheme.Hom.ker f').ideal W =
        Ideal.comap (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appIso iV ↑W).inv)
          ((AlgebraicGeometry.Scheme.Hom.ker f).ideal ⟨(AlgebraicGeometry.Scheme.Hom.opensFunctor iV).obj ↑W, ⋯⟩)
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
analyticOn_sigmoid : AnalyticOn ℝ Real.sigmoid Set.univ
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs
/-- One entry of one scalar Bird recurrence step.

Bird's paper defines a matrix recursion for an `n × n` matrix `A`:

```
F_0 = A
F_{t+1} = μ(F_t) * A
```

where `μ(F_t)` is obtained from `F_t` by replacing each diagonal entry
`F_t k k` with the negative sum of the diagonal entries below it, setting the
entries in the lower triangular part to 0, and leaving all other entries
unchanged:

```
μ(F_t) =
  0                                   if i >= j
  - ∑ k from i+1 to n-1, F_t k k      if i = j
  F_t i j                             if i < j
```

If we write out the entry-wise matrix multiplication `F_{t+1} i j = (μ(F_t) * A) i j`
we obtain:

```
F_{t+1} i j =
  - (∑ k from i+1 to n-1, F_t k k) * (A i j)
  + ∑ k from i+1 to n-1, (F_t i k) * (A k j)
```
 -/
BirdDet.stepEntry : {R : Type u_1} → [CommRing R] → ℕ → Array R → (ℕ → ℕ → R) → ℕ → ℕ → R
-- Mathlib.Geometry.Convex.Cone.Dual
PointedCone.dual_flip_dual_dual_flip : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {N : Type u_3} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  {p : M →ₗ[R] N →ₗ[R] R} (s : Set N),
  PointedCone.dual p.flip ↑(PointedCone.dual p ↑(PointedCone.dual p.flip s)) = PointedCone.dual p.flip s
-- Lean.Meta.Tactic.Simp.Arith.Int.Basic
_private.Lean.Meta.Tactic.Simp.Arith.Int.Basic.0.Int.Internal.Linear.Expr.applyPerm.go : Lean.Perm → Int.Internal.Linear.Expr → Int.Internal.Linear.Expr
-- Mathlib.Data.WSeq.Basic
_private.Mathlib.Data.WSeq.Basic.0.Stream'.Seq.omap.match_1.splitter : {α : Type u_2} →
  {β : Type u_1} →
    (motive : Option (α × β) → Sort u_3) →
      (x : Option (α × β)) → (Unit → motive none) → ((a : α) → (b : β) → motive (some (a, b))) → motive x
-- Mathlib.Analysis.Calculus.IteratedDeriv.WithinZpow
iteratedDerivWithin_zpow : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {s : Set 𝕜} (m : ℤ) (k : ℕ),
  IsOpen s →
    Set.EqOn (iteratedDerivWithin k (fun y => y ^ m) s) (fun y => (∏ i ∈ Finset.range k, (↑m - ↑i)) * y ^ (m - ↑k)) s
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
/-- The embedding `v.Completion →+* ℝ` at a real infinite place is an isometry.  -/
NumberField.InfinitePlace.Completion.isometry_extensionEmbeddingOfIsReal : ∀ {K : Type u_1} [inst : Field K] {v : NumberField.InfinitePlace K} (hv : v.IsReal),
  Isometry ⇑(NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal hv)
-- Std.Data.DTreeMap.Internal.Model
/-- Model implementation of the `get?` function.
Internal implementation detail of the tree map
 -/
Std.DTreeMap.Internal.Impl.get?ₘ : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] → [Std.OrientedOrd α] → [Std.LawfulEqOrd α] → Std.DTreeMap.Internal.Impl α β → (k : α) → Option (β k)
-- Mathlib.Algebra.Divisibility.Basic
dvd_mul_left : ∀ {α : Type u_1} [inst : CommSemigroup α] (a b : α), a ∣ b * a
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
NumberField.mixedEmbedding.convexBodySumFun_apply : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : NumberField.mixedEmbedding.mixedSpace K),
  NumberField.mixedEmbedding.convexBodySumFun x = ∑ w, ↑w.mult * (NumberField.mixedEmbedding.normAtPlace w) x
-- Mathlib.RepresentationTheory.Action
Representation.LinearizeMonoidal.δ_apply_single : ∀ {G : Type v} [inst : Monoid G] {X Y : Action (Type w) G} {k : Type u} [inst_1 : CommSemiring k]
  (xy : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).V),
  (Representation.LinearizeMonoidal.δ X Y) (MonoidAlgebra.single xy 1) =
    MonoidAlgebra.single xy.1 1 ⊗ₜ[k] MonoidAlgebra.single xy.2 1
-- Mathlib.CategoryTheory.Category.Pointed
Pointed.mk : (X : Type u) → X → Pointed
-- Mathlib.Combinatorics.Matroid.Circuit
/-- **Alias** of `Matroid.fundCircuit_sdiff_eq_inter`. -/
Matroid.fundCircuit_diff_eq_inter : ∀ {α : Type u_1} {I : Set α} {e : α} (M : Matroid α), e ∉ I → M.fundCircuit e I \ {e} = M.fundCircuit e I ∩ I
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
AlgebraicTopology.DoldKan.Isδ₀.eq_δ₀ : ∀ {n : ℕ} {i : { len := n } ⟶ { len := n + 1 }} [inst : CategoryTheory.Mono i],
  AlgebraicTopology.DoldKan.Isδ₀ i → i = SimplexCategory.δ 0
-- Mathlib.Data.NNReal.Defs
NNReal.mul_lt_of_lt_div : ∀ {a b r : NNReal}, a < b / r → a * r < b
-- Lean.Elab.Match
/-- We (try to) elaborate a `match` only when the expected type is available.
If the `matchType` has not been provided by the user, we also try to postpone elaboration if the type
of a discriminant is not available. That is, it is of the form `(?m ...)`.
We use `expandNonAtomicDiscrs?` to make sure all discriminants are metavariables,
so that they are not elaborated twice.
This is a standard trick we use in the elaborator, and it is also used to elaborate structure instances.
Suppose, we are trying to elaborate
```
match g x with
  | ... => ...
```
`expandNonAtomicDiscrs?` converts it intro
```
let_mvar% ?discr := g x
match ?discr with
  | ... => ...
```

This elaboration technique is needed to elaborate terms such as:
```lean
xs.filter fun (a, b) => a > b
```
which are syntax sugar for
```lean
List.filter (fun p => match p with | (a, b) => a > b) xs
```
When we visit `match p with | (a, b) => a > b`, we don't know the type of `p` yet.
 -/
_private.Lean.Elab.Match.0.Lean.Elab.Term.waitExpectedTypeAndDiscrs : Lean.Syntax → Option Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.mkInductiveAux₂_add_one : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {P Q : ChainComplex V ℕ} (e : P ⟶ Q) (zero : P.X 0 ⟶ Q.X 1)
  (comm_zero : e.f 0 = CategoryTheory.CategoryStruct.comp zero (Q.d 1 0)) (one : P.X 1 ⟶ Q.X 2)
  (comm_one :
    e.f 1 = CategoryTheory.CategoryStruct.comp (P.d 1 0) zero + CategoryTheory.CategoryStruct.comp one (Q.d 2 1))
  (succ :
    (n : ℕ) →
      (p :
          (f : P.X n ⟶ Q.X (n + 1)) ×'
            (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×'
              e.f (n + 1) =
                CategoryTheory.CategoryStruct.comp (P.d (n + 1) n) f +
                  CategoryTheory.CategoryStruct.comp f' (Q.d (n + 2) (n + 1))) →
        (f'' : P.X (n + 2) ⟶ Q.X (n + 3)) ×'
          e.f (n + 2) =
            CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 1)) p.snd.fst +
              CategoryTheory.CategoryStruct.comp f'' (Q.d (n + 3) (n + 2)))
  (n : ℕ),
  Homotopy.mkInductiveAux₂ e zero comm_zero one comm_one succ (n + 1) =
    ⟨CategoryTheory.CategoryStruct.comp (HomologicalComplex.xNextIso P ⋯).hom
        (Homotopy.mkInductiveAux₁ e zero one comm_one succ n).fst,
      ⟨CategoryTheory.CategoryStruct.comp (Homotopy.mkInductiveAux₁ e zero one comm_one succ n).snd.fst
          (HomologicalComplex.xPrevIso Q ⋯).inv,
        ⋯⟩⟩
-- Mathlib.Data.Nat.SuccPred
Nat.instIsPredArchimedean : IsPredArchimedean ℕ