mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.BigOperators.Ring.Finset
/-- If `g, h ≤ f` and `g i + h i ≤ f i`, then the product of `f` over `s` is at least the
sum of the products of `g` and `h`. This is the version for `OrderedCommSemiring`.  -/
Finset.prod_add_prod_le : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommSemiring R] [inst_1 : PartialOrder R] [IsOrderedRing R] {s : Finset ι}
  {i : ι} {f g h : ι → R},
  i ∈ s →
    g i + h i ≤ f i →
      (∀ j ∈ s, j ≠ i → g j ≤ f j) →
        (∀ j ∈ s, j ≠ i → h j ≤ f j) →
          (∀ i ∈ s, 0 ≤ g i) → (∀ i ∈ s, 0 ≤ h i) → ∏ i ∈ s, g i + ∏ i ∈ s, h i ≤ ∏ i ∈ s, f i
-- Std.Data.ExtDHashMap.Basic
/-- The number of mappings present in the hash map  -/
Std.ExtDHashMap.size : {α : Type u} →
  {β : α → Type v} → {x : BEq α} → {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → Std.ExtDHashMap α β → ℕ
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Var
Std.Tactic.BVDecide.BVExpr.bitblast.blastVar.go.eq_def : ∀ (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (w a curr : ℕ) (s : aig.RefVec curr) (hcurr : curr ≤ w),
  Std.Tactic.BVDecide.BVExpr.bitblast.blastVar.go aig w a curr s hcurr =
    if hcurr : curr < w then
      let res := aig.mkAtomCached { var := a, w := w, idx := ⟨curr, hcurr⟩ };
      let aig_1 := res.aig;
      have bitRef := res.ref;
      have s := s.cast ⋯;
      have s := s.push bitRef;
      Std.Tactic.BVDecide.BVExpr.bitblast.blastVar.go aig_1 w a (curr + 1) s ⋯
    else
      have hcurr := ⋯;
      { aig := aig, vec := hcurr ▸ s }
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanShape.prod_R : ∀ (ι : Type w), (CategoryTheory.Limits.MulticospanShape.prod ι).R = (ι × ι)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.cyclesFunctor_map : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasKernels C] [inst_3 : CategoryTheory.Limits.HasCokernels C]
  {X Y : CategoryTheory.ShortComplex C} (φ : X ⟶ Y),
  (CategoryTheory.ShortComplex.cyclesFunctor C).map φ = CategoryTheory.ShortComplex.cyclesMap φ
-- Lean.Meta.Sym.InstantiateMVarsS
/-- Instantiates metavariables occurring in `e`, and returns a maximally shared term.
 -/
Lean.Meta.Sym.instantiateMVarsS : Lean.Expr → Lean.Meta.Sym.SymM Lean.Expr
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.coeff_zero_reverse : ∀ {R : Type u_1} [inst : Semiring R] (f : Polynomial R), f.reverse.coeff 0 = f.leadingCoeff
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.measurable_gaussianReal : Measurable (Function.uncurry ProbabilityTheory.gaussianReal)
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.subset_compl_singleton : ∀ {α : Type u_1} {s : Finset α} [inst : Fintype α] [inst_1 : DecidableEq α] {a : α}, s ⊆ {a}ᶜ ↔ a ∉ s
-- Mathlib.Algebra.AddConstMap.Equiv
AddConstEquiv.trans_toEquiv : ∀ {G : Type u_1} {H : Type u_2} {K : Type u_3} [inst : Add G] [inst_1 : Add H] [inst_2 : Add K] {a : G} {b : H} {c : K}
  (e₁ : AddConstEquiv G H a b) (e₂ : AddConstEquiv H K b c), (e₁.trans e₂).toEquiv = e₁.trans e₂.toEquiv
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
/-- The opposite of a precylinder object is a pre-path object.  -/
HomotopicalAlgebra.Precylinder.op : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : C} → HomotopicalAlgebra.Precylinder A → HomotopicalAlgebra.PrepathObject (Opposite.op A)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.size_alter!_eq_self_of_not_mem : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} {f : Option β → Option β},
      k ∉ t →
        (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isNone = true →
          (Std.DTreeMap.Internal.Impl.Const.alter! k f t).size = t.size
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.Measure.ae_rnDeriv_ne_zero_imp_of_ae : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (ν : MeasureTheory.Measure α)
  [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] {p : α → Prop},
  (∀ᵐ (a : α) ∂μ, p a) → ∀ᵐ (a : α) ∂ν, μ.rnDeriv ν a ≠ 0 → p a
-- Mathlib.Data.Rel
SetRel.iUnion_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_5} (R : ι → SetRel α β) (S : SetRel β γ),
  SetRel.comp (⋃ i, R i) S = ⋃ i, (R i).comp S
-- Mathlib.Data.Ordmap.Ordnode
/-- **Internal use only**

O(1). Rebalance a tree which was previously balanced but has had its left
side grow by 1, or its right side shrink by 1.  -/
Ordnode.balanceL : {α : Type u_1} → Ordnode α → α → Ordnode α → Ordnode α
-- Mathlib.Algebra.Group.Pi.Basic
Pi.commMagma.eq_1 : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → CommMagma (f i)],
  Pi.commMagma = { toMul := Pi.instMul, mul_comm := ⋯ }
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_lift_ExceptT_apply_eq : ∀ {Pred : Type u_1} {EPred : Type u_2} {m : Type u → Type v} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {α ε : Type u}
  {post : α → Pred} {epost : EPost.Cons✝ (ε → Pred) EPred} (x : m α),
  Std.Internal.Do.wp (ExceptT.lift x) post epost = Std.Internal.Do.wp (MonadLift.monadLift x) post epost
-- Mathlib.Order.Bounds.Basic
isLUB_lowerBounds : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {a : α}, IsLUB (lowerBounds s) a ↔ IsGLB s a
-- Mathlib.Algebra.Module.LinearMap.Prod
IsLinearMap.isLinearMap_sub : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  IsLinearMap R fun x => x.1 - x.2
-- Mathlib.Data.Finsupp.BigOperators
List.support_sum_subset : ∀ {ι : Type u_1} {M : Type u_2} [inst : DecidableEq ι] [inst_1 : AddZeroClass M] (l : List (ι →₀ M)),
  l.sum.support ⊆ List.foldr (fun x1 x2 => x1.support ⊔ x2) ∅ l
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.aeval_zero' : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] [inst_2 : Algebra R S₁]
  (p : MvPolynomial σ R), (MvPolynomial.aeval fun x => 0) p = (algebraMap R S₁) (MvPolynomial.constantCoeff p)
-- Init.Data.String.Defs
String.utf8EncodeChar.fun_cases_unfolding : ∀ (c : Char) (motive : List UInt8 → Prop),
  (have v := c.val.toNat;
    v ≤ 127 → motive [UInt8.ofNat v]) →
    (have v := c.val.toNat;
      ¬v ≤ 127 → v ≤ 2047 → motive [UInt8.ofNat (v / 64 % 32 + 192), UInt8.ofNat (v % 64 + 128)]) →
      (have v := c.val.toNat;
        ¬v ≤ 127 →
          ¬v ≤ 2047 →
            v ≤ 65535 →
              motive [UInt8.ofNat (v / 4096 % 16 + 224), UInt8.ofNat (v / 64 % 64 + 128), UInt8.ofNat (v % 64 + 128)]) →
        (have v := c.val.toNat;
          ¬v ≤ 127 →
            ¬v ≤ 2047 →
              ¬v ≤ 65535 →
                motive
                  [UInt8.ofNat (v / 262144 % 8 + 240), UInt8.ofNat (v / 4096 % 64 + 128),
                    UInt8.ofNat (v / 64 % 64 + 128), UInt8.ofNat (v % 64 + 128)]) →
          motive (String.utf8EncodeChar c)
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.IntegrableAtFilter.eventually : ∀ {α : Type u_1} {ε : Type u_3} {mα : MeasurableSpace α} {f : α → ε} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] {l : Filter α},
  MeasureTheory.IntegrableAtFilter f l μ → ∀ᶠ (s : Set α) in l.smallSets, MeasureTheory.IntegrableOn f s μ
-- Mathlib.GroupTheory.PGroup
IsPGroup.zero : ∀ (G : Type u_1) [inst : Group G], IsPGroup 0 G
-- Batteries.Data.String.Lemmas
String.map_isEmpty_eq_isEmpty : ∀ (s : String) (f : Char → Char), (String.Legacy.map f s).isEmpty = s.isEmpty
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryₘ.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (l : Std.DTreeMap.Internal.Impl α β) (k : α)
  (h : (l.getEntry?ₘ k).isSome = true), l.getEntryₘ k h = (l.getEntry?ₘ k).get h
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.inl.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N],
  Monoid.Coprod.inl = { toFun := fun x => Monoid.Coprod.mk (FreeMonoid.of (Sum.inl x)), map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
/-- The tensor product of two quadratic forms injects into quadratic forms on tensor products.

Note this is heterobasic; the quadratic form on the left can take values in a larger ring than
the one on the right.  -/
QuadraticForm.tensorDistrib : (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₁] →
                        [IsScalarTower R A M₁] →
                          [inst_9 : Module R M₂] →
                            [Invertible 2] →
                              TensorProduct R (QuadraticForm A M₁) (QuadraticForm R M₂) →ₗ[A]
                                QuadraticForm A (TensorProduct R M₁ M₂)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.commMap_apply_of_isComplex : ∀ (K : Type u_1) [inst : Field K] (x : (K →+* ℂ) → ℂ) {w : NumberField.InfinitePlace K} (hw : w.IsComplex),
  ((NumberField.mixedEmbedding.commMap K) x).2 ⟨w, hw⟩ = x w.embedding
-- Mathlib.Tactic.NormNum.Result
/-- A "raw nat cast" is an expression of the form `(Nat.rawCast lit : α)` where `lit` is a raw
natural number literal. These expressions are used by tactics like `ring` to decrease the number
of typeclass arguments required in each use of a number literal at type `α`.
 -/
Nat.rawCast : {α : Type u} → [AddMonoidWithOne α] → ℕ → α
-- Mathlib.NumberTheory.RamificationInertia.Ramification
/-- **Alias** of `Ideal.le_comap_of_ramificationIdx'_ne_zero`. -/
Ideal.le_comap_of_ramificationIdx_ne_zero : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal R}
  {P : Ideal S}, p.ramificationIdx' P ≠ 0 → p ≤ Ideal.comap (algebraMap R S) P
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.Descr.exportEntry? : {α β σ : Type} → Lean.ScopedEnvExtension.Descr α β σ → Lean.Environment → α → Lean.OLeanEntries (Option α)
-- Init.GrindInstances.Ring.UInt
UInt16.intCast : IntCast UInt16
-- Mathlib.Topology.UniformSpace.UniformEmbedding
isUniformInducing_iff' : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
  IsUniformInducing f ↔ UniformContinuous f ∧ Filter.comap (Prod.map f f) (uniformity β) ≤ uniformity α
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pushout.mapLift_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y S T S' : C} (f : T ⟶ X) (g : T ⟶ Y) (i : S ⟶ T)
  (i' : S' ⟶ S) [inst_1 : CategoryTheory.Limits.HasPushout f g]
  [inst_2 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp i f) (CategoryTheory.CategoryStruct.comp i g)]
  [inst_3 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp i' (CategoryTheory.CategoryStruct.comp i f))
      (CategoryTheory.CategoryStruct.comp i' (CategoryTheory.CategoryStruct.comp i g))]
  [inst_4 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp i' i) f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp i' i) g)],
  CategoryTheory.Limits.pushout.mapLift f g (CategoryTheory.CategoryStruct.comp i' i) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.congrHom ⋯ ⋯).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pushout.mapLift (CategoryTheory.CategoryStruct.comp i f)
          (CategoryTheory.CategoryStruct.comp i g) i')
        (CategoryTheory.Limits.pushout.mapLift f g i))
-- Mathlib.MeasureTheory.Measure.Restrict
/-- If `t` is a measurable set, then the measure of `t` with respect to the restriction of
the measure to `s` equals the outer measure of `t ∩ s`. An alternate version requiring that `s`
be measurable instead of `t` exists as `Measure.restrict_apply'`.  -/
MeasureTheory.Measure.restrict_apply : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasurableSet t → (μ.restrict s) t = μ (t ∩ s)
-- Init.Data.Char.Ordinal
Char.ordinal_comp_ofOrdinal : Char.ordinal ∘ Char.ofOrdinal = id
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp},
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ → ∀ (f : (a : α) → β a → Bool), (Std.DTreeMap.Raw.filter f t₁).Equiv (Std.DTreeMap.Raw.filter f t₂)
-- Mathlib.Data.PNat.Prime
PNat.dvd_prime : ∀ {p m : ℕ+}, p.Prime → (m ∣ p ↔ m = 1 ∨ m = p)
-- Mathlib.RingTheory.Frobenius
IsArithFrobAt.exists_primesOver_isConj : ∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (G : Type u_3)
  [inst_3 : Group G] [inst_4 : MulSemiringAction G S] [inst_5 : SMulCommClass G R S] [Finite G]
  [Algebra.IsInvariant R S G] (P : Ideal R),
  (∃ Q, Finite (S ⧸ ↑Q)) →
    ∃ σ, (∀ (Q : ↑(P.primesOver S)), IsArithFrobAt R (σ Q) ↑Q) ∧ ∀ (Q₁ Q₂ : ↑(P.primesOver S)), IsConj (σ Q₁) (σ Q₂)
-- Mathlib.Order.Interval.Set.SuccPred
Set.Iio_succ_eq_Iic_of_not_isMax : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] {b : α}, ¬IsMax b → Set.Iio (Order.succ b) = Set.Iic b
-- Mathlib.MeasureTheory.Group.Measure
/-- A measure is invariant under negation if `- μ = μ`. Equivalently, this means that for all
measurable `A` we have `μ (- A) = μ A`, where `- A` is the pointwise negation of `A`.  -/
MeasureTheory.Measure.IsNegInvariant : {G : Type u_1} → [inst : MeasurableSpace G] → [Neg G] → MeasureTheory.Measure G → Prop
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
SSet.Subcomplex.N.cases : ∀ {X : SSet} (A : X.Subcomplex) {motive : X.N → Prop},
  (∀ (s : X.N), s.subcomplex ≤ A → motive s) → (∀ (s : A.N), motive s.toN) → ∀ (s : X.N), motive s
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.toPoly'.go.eq_7 : ∀ (coeff : ℤ) (a : Int.Internal.Linear.Expr),
  Int.Internal.Linear.Expr.toPoly'.go coeff a.neg = Int.Internal.Linear.Expr.toPoly'.go (-coeff) a
-- Mathlib.Geometry.Manifold.Bordism
SingularManifold.compactSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] {k : WithTop ℕ∞} {E : Type u_2} {H : Type u_3}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] [inst_3 : FiniteDimensional ℝ E]
  [inst_4 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} (self : SingularManifold X k I), CompactSpace self.M
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.center_prod : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : StarRing A]
  [inst_3 : Module R A] [inst_4 : NonUnitalSemiring B] [inst_5 : StarRing B] [inst_6 : Module R B]
  [inst_7 : IsScalarTower R A A] [inst_8 : SMulCommClass R A A] [inst_9 : IsScalarTower R B B]
  [inst_10 : SMulCommClass R B B],
  NonUnitalStarSubalgebra.center R (A × B) =
    (NonUnitalStarSubalgebra.center R A).prod (NonUnitalStarSubalgebra.center R B)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.map_fst_toList_eq_keys : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp],
  List.map Prod.fst (Std.ExtDTreeMap.Const.toList t) = t.keys
-- Mathlib.Topology.Algebra.Module.Simple
/-- The kernel of a linear map taking values in a simple module over the base ring is closed or
dense. Applies, e.g., to the case when `R = N` is a division ring.  -/
LinearMap.isClosed_or_dense_ker : ∀ {R : Type u} {M : Type v} {N : Type w} [inst : Ring R] [inst_1 : TopologicalSpace R] [inst_2 : TopologicalSpace M]
  [inst_3 : AddCommGroup M] [inst_4 : AddCommGroup N] [inst_5 : Module R M] [ContinuousSMul R M] [inst_7 : Module R N]
  [ContinuousAdd M] [IsSimpleModule R N] (l : M →ₗ[R] N), IsClosed ↑l.ker ∨ Dense ↑l.ker
-- Mathlib.AlgebraicTopology.DoldKan.Normalized
/-- When the category `A` is abelian,
the functor `N₁ : SimplicialObject A ⥤ Karoubi (ChainComplex A ℕ)` defined
using `PInfty` identifies to the composition of the normalized Moore complex functor
and the inclusion in the Karoubi envelope.  -/
AlgebraicTopology.DoldKan.N₁_iso_normalizedMooreComplex_comp_toKaroubi : (A : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    [inst_1 : CategoryTheory.Abelian A] →
      AlgebraicTopology.DoldKan.N₁ ≅
        (AlgebraicTopology.normalizedMooreComplex A).comp (CategoryTheory.Idempotents.toKaroubi (ChainComplex A ℕ))
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass
CategoryTheory.ShortComplex.ShortExact.instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoX₃CochainComplexMapSingleFunctorOfNatX₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] [CategoryTheory.HasExt C]
  {S : CategoryTheory.ShortComplex C},
  CategoryTheory.Localization.HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ
    (S.map (CochainComplex.singleFunctor C 0)).X₃ (S.map (CochainComplex.singleFunctor C 0)).X₁
-- Mathlib.Algebra.Module.Submodule.IterateMapComap
/-- If `f` is surjective, `i` is injective, and there exists some `m` such that
`LinearMap.iterateMapComap f i m K = LinearMap.iterateMapComap f i (m + 1) K`,
then for any `n`,
`LinearMap.iterateMapComap f i n K = LinearMap.iterateMapComap f i (n + 1) K`.
In particular, by taking `n = 0`, the kernel of `f` is contained in `K`
(`LinearMap.ker_le_of_iterateMapComap_eq_succ`),
which is a consequence of `LinearMap.ker_le_comap`.  -/
LinearMap.iterateMapComap_eq_succ : ∀ {R : Type u_1} {N : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid N] [inst_2 : Module R N]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (f i : N →ₗ[R] M) (K : Submodule R N) (m : ℕ),
  f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K →
    Function.Surjective ⇑f → Function.Injective ⇑i → ∀ (n : ℕ), f.iterateMapComap i n K = f.iterateMapComap i (n + 1) K
-- Batteries.Data.List.Basic
List.all₂.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (r : α → β → Bool), List.all₂ r [] [] = true
-- Mathlib.Topology.Metrizable.Real
ENNReal.instMetrizableSpace : TopologicalSpace.MetrizableSpace ENNReal
-- Mathlib.Topology.MetricSpace.Infsep
Set.einfsep_top : ∀ {α : Type u_1} [inst : EDist α] {s : Set α}, s.einfsep = ⊤ ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → edist x y = ⊤
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape
CategoryTheory.Limits.hasIterationOfShape_of_initialSeg : ∀ {J : Type w} [inst : LinearOrder J] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasIterationOfShape J C] [SuccOrder J] [WellFoundedLT J] {α : Type u_1}
  [inst_5 : LinearOrder α] (h : α ≤i J) [Nonempty α], CategoryTheory.Limits.HasIterationOfShape α C
-- Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal
CategoryTheory.SimplicialObject.Truncated.rightExtensionInclusion_right_as : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) (n : ℕ),
  (CategoryTheory.SimplicialObject.Truncated.rightExtensionInclusion X n).right.as = PUnit.unit
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw.union_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} (h₁ : m₁.WF)
  (h₂ : m₂.WF), m₁.union m₂ = ↑(Std.DHashMap.Internal.Raw₀.union ⟨m₁, ⋯⟩ ⟨m₂, ⋯⟩)
-- Mathlib.Topology.ContinuousMap.Basic
Topology.IsQuotientMap.homeomorph_symm_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : C(X, Y)}
  (hf : Topology.IsQuotientMap ⇑f) (b : Y), hf.homeomorph.symm b = Quotient.mk'' (Function.surjInv ⋯ b)
-- Mathlib.Data.Set.Lattice.Image
Set.biUnion_inter_of_pairwise_disjoint : ∀ {α : Type u_1} {ι : Type u_9} {f : ι → Set α},
  Pairwise (Function.onFun Disjoint f) → ∀ (s t : Set ι), ⋃ i ∈ s ∩ t, f i = (⋃ i ∈ s, f i) ∩ ⋃ i ∈ t, f i
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
IsDiscreteValuationRing.addVal.congr_simp : ∀ (R : Type u) [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R],
  IsDiscreteValuationRing.addVal R = IsDiscreteValuationRing.addVal R
-- Init.WF
InvImage.wf : ∀ {α : Sort u} {β : Sort v} {r : β → β → Prop} (f : α → β), WellFounded r → WellFounded (InvImage r f)
-- Mathlib.Order.Defs.Unbundled
UpperSet.mk.injEq : ∀ {α : Type u_1} [inst : LE α] (carrier : Set α) (upper' : IsUpperSet carrier) (carrier_1 : Set α)
  (upper'_1 : IsUpperSet carrier_1),
  ({ carrier := carrier, upper' := upper' } = { carrier := carrier_1, upper' := upper'_1 }) = (carrier = carrier_1)
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.instAddCommMonoid : {R : Type u} →
  [inst : CommSemiring R] →
    {M : Type u_1} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {N : Type u_2} → [inst_3 : AddCommMonoid N] → [inst_4 : Module R N] → AddCommMonoid (M →ₚₗ[R] N)
-- Init.System.IO
/-- Returns the current thread's standard output stream.

Use `IO.setStdout` to replace the current thread's standard output stream.
 -/
IO.getStdout : BaseIO IO.FS.Stream
-- Mathlib.Algebra.Homology.Homotopy
prevD_comp_left : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D E : HomologicalComplex V c} (f : C ⟶ D) (g : (i j : ι) → D.X i ⟶ E.X j) (j : ι),
  ((prevD j) fun i j => CategoryTheory.CategoryStruct.comp (f.f i) (g i j)) =
    CategoryTheory.CategoryStruct.comp (f.f j) ((prevD j) g)
-- Mathlib.Analysis.Distribution.TemperedDistribution
TemperedDistribution.instFourierSMul : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E]
  [inst_2 : FiniteDimensional ℝ E] [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] [inst_5 : AddCommGroup F]
  [inst_6 : Module ℂ F] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F]
  [inst_9 : ContinuousConstSMul ℂ F], FourierSMul ℂ (TemperedDistribution E F) (TemperedDistribution E F)
-- Mathlib.LinearAlgebra.Projection
Submodule.projection_add_projection_eq_self : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (hpq : IsCompl p q) (x : E), (p.projection q hpq) x + (q.projection p ⋯) x = x
-- Mathlib.Data.Set.Image
Set.range_subset_iff : ∀ {α : Type u_1} {ι : Sort u_4} {f : ι → α} {s : Set α}, Set.range f ⊆ s ↔ ∀ (y : ι), f y ∈ s
-- Mathlib.RingTheory.Extension.Cotangent.Basis
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.presRight.eq_1 : ∀ {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),
  Algebra.Generators.PresentationOfFreeCotangent.Aux.presRight✝ D =
    Algebra.Presentation.localizationAway S (Algebra.Generators.PresentationOfFreeCotangent.Aux.gbar✝ D)
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.FiniteResidueField.mk_lt_mk : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K]
  {x y : ArchimedeanClass.FiniteElement K},
  ArchimedeanClass.FiniteResidueField.mk x < ArchimedeanClass.FiniteResidueField.mk y ↔
    x < y ∧ ArchimedeanClass.FiniteResidueField.mk x ≠ ArchimedeanClass.FiniteResidueField.mk y
-- Mathlib.Order.UpperLower.Basic
isLowerSet_iff_Iic_subset : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, IsLowerSet s ↔ ∀ ⦃a : α⦄, a ∈ s → Set.Iic a ⊆ s
-- Mathlib.Algebra.Order.BigOperators.Ring.Finset
IsAbsoluteValue.map_prod : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : CommSemiring R] [Nontrivial R] [inst_2 : CommRing S]
  [inst_3 : LinearOrder S] [IsStrictOrderedRing S] (abv : R → S) [IsAbsoluteValue abv] (f : ι → R) (s : Finset ι),
  abv (∏ i ∈ s, f i) = ∏ i ∈ s, abv (f i)