mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
NonUnitalSubsemiring.coe_copy : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] (S : NonUnitalSubsemiring R) (s : Set R) (hs : s = ↑S),
  ↑(S.copy s hs) = s
-- Mathlib.Data.ENNReal.Inv
/-- See `ENNReal.inv_mul_cancel_left'` for a stronger version.  -/
ENNReal.inv_mul_cancel_left : ∀ {a b : ENNReal}, a ≠ 0 → a ≠ ⊤ → a⁻¹ * (a * b) = b
-- Std.Data.ExtDTreeMap.Basic
/-- Given a proof that such a mapping exists, retrieves the key-value pair with the largest key that is
less than or equal to the given key.
 -/
Std.ExtDTreeMap.Const.getEntryLE : {α : Type u} →
  {cmp : α → α → Ordering} →
    {β : Type v} →
      [inst : Std.TransCmp cmp] →
        (t : Std.ExtDTreeMap α (fun x => β) cmp) → (k : α) → (∃ a ∈ t, (cmp a k).isLE = true) → α × β
-- Mathlib.Analysis.Matrix.Spectrum
Matrix.IsHermitian.mulVec_eigenvectorBasis : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : Fintype n] {A : Matrix n n 𝕜} [inst_2 : DecidableEq n]
  (hA : A.IsHermitian) (j : n), A.mulVec (hA.eigenvectorBasis j).ofLp = hA.eigenvalues j • (hA.eigenvectorBasis j).ofLp
-- Mathlib.NumberTheory.Zsqrtd.GaussianInt
GaussianInt.intCast_complex_norm : ∀ (x : GaussianInt), ↑(Zsqrtd.norm x) = ↑(Complex.normSq (GaussianInt.toComplex x))
-- Mathlib.Topology.Order.IntermediateValue
/-- Version of `exists_mem_Icc_isFixedPt_of_surjOn` using `Set.uIcc`  -/
exists_mem_uIcc_isFixedPt_of_surjOn : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {a b : α} {f : α → α},
  ContinuousOn f (Set.uIcc a b) →
    Set.SurjOn f (Set.uIcc a b) (Set.uIcc a b) → ∃ c ∈ Set.uIcc a b, Function.IsFixedPt f c
-- Batteries.Data.List.Scan
List.length_flatten_mem_partialSums_map_length : ∀ {α : Type u_1} (L : List (List α)), L.flatten.length ∈ (List.map List.length L).partialSums
-- Mathlib.Topology.WithTopology
WithTopology.instDecidableEq : {X : Type u_2} → {t : TopologicalSpace X} → [DecidableEq X] → DecidableEq (WithTopology X t)
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.laverage_union_mem_segment : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α} {f : α → ENNReal},
  MeasureTheory.AEDisjoint μ s t →
    MeasureTheory.NullMeasurableSet t μ →
      μ s ≠ ⊤ →
        μ t ≠ ⊤ → ⨍⁻ (x : α) in s ∪ t, f x ∂μ ∈ segment ENNReal (⨍⁻ (x : α) in s, f x ∂μ) (⨍⁻ (x : α) in t, f x ∂μ)
-- Mathlib.Order.Hom.Lex
OrderIso.sumLexIicIoi_symm_apply_of_lt : ∀ {α : Type u_1} [inst : LinearOrder α] {x y : α} (h : x < y), (OrderIso.sumLexIicIoi x).symm y = toLex (Sum.inr ⟨y, h⟩)
-- Init.Data.String.Substring
/-- Removes the longest suffix of a substring in which a Boolean predicate returns `true` for all
characters by moving the substring's end position. The end position is moved just after the position
of the last character for which the predicate returns `false`, or to the substring's start position
if the predicate always returns `true`.
 -/
Substring.Raw.dropRightWhile : Substring.Raw → (Char → Bool) → Substring.Raw
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.pow : {α : Type u_1} → [One α] → [Pow α ℕ] → Pow (WithZero α) ℕ
-- Mathlib.Algebra.Ring.Int.Parity
Int.odd_sub' : ∀ {m n : ℤ}, Odd (m - n) ↔ (Odd n ↔ Even m)
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.Indep.cRk_eq_cardinalMk : ∀ {α : Type u} {M : Matroid α} {I : Set α}, M.Indep I → Cardinal.mk ↑I = M.cRk I
-- Mathlib.Topology.Order.LeftRight
IsAntichain.interior_eq_empty' : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : Preorder α] [∀ (x : α), (nhdsWithin x (Set.Ioi x)).NeBot]
  {s : Set α}, IsAntichain (fun x1 x2 => x1 ≤ x2) s → interior s = ∅
-- Lean.Meta.Sym.AlphaShareBuilder
Lean.Meta.Sym.Internal.Sym.assertShared : Lean.Expr → Lean.Meta.Sym.SymM Unit
-- Mathlib.Algebra.Group.Action.Basic
/-- `AddAction.toPerm` is injective on faithful actions.  -/
AddAction.toPerm_injective : ∀ {α : Type u_5} {β : Type u_6} [inst : AddGroup α] [inst_1 : AddAction α β] [FaithfulVAdd α β],
  Function.Injective AddAction.toPerm
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get!_diff_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} [inst_2 : Inhabited (β k)], k ∉ t₂ → (t₁ \ t₂).get! k = t₁.get! k
-- Aesop.Tree.Data
Aesop.instNonemptyRappData : ∀ {Goal : Type} [Nonempty Goal] {MVarCluster : Type}, Nonempty (Aesop.RappData Goal MVarCluster)
-- Mathlib.Logic.Equiv.Defs
/-- Inverse of an equivalence `e : α ≃ β`.  -/
Equiv.symm : {α : Sort u} → {β : Sort v} → α ≃ β → β ≃ α
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isBigOWith_principal : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {c : ℝ} {f : α → E} {g : α → F}
  {s : Set α}, Asymptotics.IsBigOWith c (Filter.principal s) f g ↔ ∀ x ∈ s, ‖f x‖ ≤ c * ‖g x‖
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubmonoid.val_addUnitsEquivAddUnitsType_symm_apply_coe : ∀ {M : Type u_1} [inst : AddMonoid M] (S : AddSubmonoid M) (x : AddUnits ↥S),
  ↑↑(S.addUnitsEquivAddUnitsType.symm x) = ↑↑x
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.CongrInfo.interlaced.injEq : ∀ (rewritable rewritable_1 : Array Bool),
  (Lean.Meta.Sym.CongrInfo.interlaced rewritable = Lean.Meta.Sym.CongrInfo.interlaced rewritable_1) =
    (rewritable = rewritable_1)
-- Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
DerivedCategory.homologyFunctorFactorsh_inv_app_quotient_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (K : CochainComplex C ℤ) (n : ℤ),
  (DerivedCategory.homologyFunctorFactorsh C n).inv.app ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K) =
    CategoryTheory.CategoryStruct.comp ((HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) n).hom.app K)
      (CategoryTheory.CategoryStruct.comp ((DerivedCategory.homologyFunctorFactors C n).inv.app K)
        ((DerivedCategory.homologyFunctor C n).map ((DerivedCategory.quotientCompQhIso C).inv.app K)))
-- Mathlib.AlgebraicTopology.ModelCategory.Homotopy
/-- Left homotopy classes of maps `X ⟶ Y` identify to right homotopy classes
when `X` is cofibrant and `Y` is fibrant.  -/
HomotopicalAlgebra.leftHomotopyClassEquivRightHomotopyClass : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      {X Y : C} →
        [HomotopicalAlgebra.IsCofibrant X] →
          [HomotopicalAlgebra.IsFibrant Y] →
            HomotopicalAlgebra.LeftHomotopyClass X Y ≃ HomotopicalAlgebra.RightHomotopyClass X Y
-- Mathlib.Order.Filter.CountablyGenerated
Filter.antitone_seq_of_seq : ∀ {α : Type u_1} (s : ℕ → Set α), ∃ t, Antitone t ∧ ⨅ i, Filter.principal (s i) = ⨅ i, Filter.principal (t i)
-- Mathlib.Tactic.DepRewrite
Mathlib.Tactic.DepRewrite.heqR : ∀ {α β : Sort u} {a : α} {b : β} (h : a ≍ b), cast ⋯ a = b
-- Mathlib.GroupTheory.Submonoid.Center
Subsemigroup.centerToMulOpposite_symm_apply_coe : ∀ {M : Type u_2} [inst : Mul M] (r : ↥(Subsemigroup.center Mᵐᵒᵖ)),
  ↑(Subsemigroup.centerToMulOpposite.symm r) = MulOpposite.unop ↑r
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
/-- The group of `AffineEquiv`s are equivalent to the group of units of `AffineMap`.

This is the affine version of `LinearMap.GeneralLinearGroup.generalLinearEquiv`.  -/
AffineEquiv.equivUnitsAffineMap : {k : Type u_1} →
  {P₁ : Type u_2} →
    {V₁ : Type u_6} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V₁] →
          [inst_2 : Module k V₁] → [inst_3 : AddTorsor V₁ P₁] → (P₁ ≃ᵃ[k] P₁) ≃* (P₁ →ᵃ[k] P₁)ˣ
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
/-- If `1 ≤ a` and `a ≤ n`, partitions of `n` containing `a` as a part are equivalent to
partitions of `n - a`. The forward map removes one occurrence of `a`, and the inverse adds `a` as
a part.  -/
Nat.Partition.partitionWithPartEquiv : {n a : ℕ} → 1 ≤ a → a ≤ n → { p // a ∈ p.parts } ≃ (n - a).Partition
-- Mathlib.Order.Filter.Finite
Filter.iInf_principal_finset : ∀ {α : Type u} {ι : Type w} (s : Finset ι) (f : ι → Set α),
  ⨅ i ∈ s, Filter.principal (f i) = Filter.principal (⋂ i ∈ s, f i)
-- Mathlib.Topology.Sets.VietorisTopology
/-- **Alias** of `TopologicalSpace.Compacts.isOpen_setOfPred_disjoint`. -/
TopologicalSpace.Compacts.isOpen_setOf_disjoint : ∀ {α : Type u_1} [inst : TopologicalSpace α] [T2Space α], IsOpen {p | Disjoint p.1 p.2}
-- Mathlib.Analysis.Normed.Group.Basic
NormedAddCommGroup.induced.eq_1 : ∀ {𝓕 : Type u_1} (E : Type u_5) (F : Type u_6) [inst : FunLike 𝓕 E F] [inst_1 : AddCommGroup E]
  [inst_2 : NormedAddGroup F] [inst_3 : AddMonoidHomClass 𝓕 E F] (f : 𝓕) (h : Function.Injective ⇑f),
  NormedAddCommGroup.induced E F f h =
    { norm := fun a => ‖f a‖, toAddCommGroup := inst_1, dist := fun a a_1 => dist (f a) (f a_1), dist_self := ⋯,
      dist_comm := ⋯, dist_triangle := ⋯, edist := fun a a_1 => PseudoMetricSpace.edist (f a) (f a_1), edist_dist := ⋯,
      toUniformSpace :=
        { toTopologicalSpace := TopologicalSpace.induced (⇑f) PseudoMetricSpace.toUniformSpace.toTopologicalSpace,
          uniformity := Filter.comap (fun p => (f p.1, f p.2)) (uniformity F), symm := ⋯, comp := ⋯,
          nhds_eq_comap_uniformity := ⋯ },
      uniformity_dist := ⋯, toBornology := { cobounded := Filter.comap (⇑f) (Bornology.cobounded F), le_cofinite := ⋯ },
      cobounded_sets := ⋯, eq_of_dist_eq_zero := ⋯, dist_eq := ⋯ }
-- Init.Data.List.FinRange
/-- Lists all elements of `Fin n` in order, starting at `0`.

Examples:
* `List.finRange 0 = ([] : List (Fin 0))`
* `List.finRange 2 = ([0, 1] : List (Fin 2))`
 -/
List.finRange : (n : ℕ) → List (Fin n)
-- Mathlib.Data.Opposite
Opposite.op_eq_iff_eq_unop : ∀ {α : Sort u} {x : α} {y : αᵒᵖ}, Opposite.op x = y ↔ x = Opposite.unop y
-- Mathlib.Probability.Process.Adapted
MeasureTheory.IsProgressive.finsetProd : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} {mi : MeasurableSpace ι} {mβ : MeasurableSpace β} {γ : Type u_4} [inst_1 : CommMonoid β]
  [MeasurableMul₂ β] {U : γ → ι → Ω → β} {s : Finset γ},
  (∀ c ∈ s, MeasureTheory.IsProgressive f (U c)) → MeasureTheory.IsProgressive f fun i ω => ∏ c ∈ s, U c i ω
-- Init.Data.Int.Order
Int.add_nonneg : ∀ {a b : ℤ}, 0 ≤ a → 0 ≤ b → 0 ≤ a + b
-- Lean.Meta.Basic
/-- Restore backtrackable parts of the state.  -/
Lean.Meta.SavedState.restore : Lean.Meta.SavedState → Lean.MetaM Unit
-- Mathlib.Algebra.Category.MonCat.Limits
AddMonCat.HasLimits.limitConeIsLimit.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddMonCat)
  [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddMonCat)).sections],
  AddMonCat.HasLimits.limitConeIsLimit F =
    CategoryTheory.Limits.IsLimit.ofFaithful (CategoryTheory.forget AddMonCat)
      (CategoryTheory.Limits.Types.Small.limitConeIsLimit (F.comp (CategoryTheory.forget AddMonCat)))
      (fun s =>
        AddMonCat.ofHom
          {
            toFun := fun v =>
              EquivLike.coe (equivShrink ↑(F.comp (CategoryTheory.forget AddMonCat)).sections)
                ⟨fun j =>
                  (CategoryTheory.ConcreteCategory.hom (((CategoryTheory.forget AddMonCat).mapCone s).π.app j)) v, ⋯⟩,
            map_zero' := ⋯, map_add' := ⋯ })
      ⋯
-- Mathlib.Algebra.GroupWithZero.Defs
GroupWithZero.toZPow : {G₀ : Type u} → [self : GroupWithZero G₀] → ZPow G₀
-- Mathlib.AlgebraicTopology.DoldKan.Normalized
_private.Mathlib.AlgebraicTopology.DoldKan.Normalized.0.AlgebraicTopology.NormalizedMooreComplex.objX.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.CategoryTheory.Simple
CategoryTheory.Simple.iff_of_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (i : X ≅ Y), CategoryTheory.Simple X ↔ CategoryTheory.Simple Y
-- Mathlib.Analysis.Complex.Trigonometric
Complex.cos_zero : Complex.cos 0 = 1
-- Mathlib.Analysis.Calculus.Deriv.Abs
deriv_abs_zero : deriv (fun x => |x|) 0 = 0
-- Init.Data.Int.Linear
Int.Internal.Linear.not_le_of_le_cert.eq_def : ∀ (p₁ p₂ : Int.Internal.Linear.Poly),
  Int.Internal.Linear.not_le_of_le_cert p₁ p₂ =
    match p₁, p₂ with
    | Int.Internal.Linear.Poly.add k v p, Int.Internal.Linear.Poly.num k_1 => false
    | Int.Internal.Linear.Poly.num k, Int.Internal.Linear.Poly.add k_1 v p => false
    | Int.Internal.Linear.Poly.num c₁, Int.Internal.Linear.Poly.num c₂ => decide (c₁ ≥ 1 - c₂)
    | Int.Internal.Linear.Poly.add a₁ x₁ p₁, Int.Internal.Linear.Poly.add a₂ x₂ p₂ =>
      a₁ == -a₂ && x₁ == x₂ && Int.Internal.Linear.not_le_of_le_cert p₁ p₂
-- Mathlib.MeasureTheory.Function.L1Space.AEEqFun
/-- Computing the norm of a difference between two L¹-functions. Note that this is not a
special case of `norm_def` since `(f - g) x` and `f x - g x` are not equal
(but only a.e.-equal).  -/
MeasureTheory.L1.norm_sub_eq_lintegral : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  (f g : ↥(MeasureTheory.Lp β 1 μ)), ‖f - g‖ = (∫⁻ (x : α), ‖↑↑f x - ↑↑g x‖ₑ ∂μ).toReal
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.genWeightSpace_le_genWeightSpaceOf : ∀ {R : Type u_2} {L : Type u_3} (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] (x : L) (χ : L → R),
  LieModule.genWeightSpace M χ ≤ LieModule.genWeightSpaceOf M (χ x) x
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Structure.FG.instCountable_hom : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] (N : Type u_2) [inst_1 : L.Structure N] [Countable N]
  [h : FirstOrder.Language.Structure.FG L M], Countable (L.Hom M N)
-- Mathlib.Analysis.Convex.Segment
openSegment_same : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [AddRightMono 𝕜] [inst_3 : AddCommGroup E]
  [inst_4 : Module 𝕜 E] [ZeroLEOneClass 𝕜] [Nontrivial 𝕜] [DenselyOrdered 𝕜] (x : E), openSegment 𝕜 x x = {x}
-- Std.Http.Internal.LowerCase
Char.toLower.eq_1 : ∀ (c : Char),
  c.toLower = if h : c.val ≥ 'A'.val ∧ c.val ≤ 'Z'.val then { val := c.val + ('a'.val - 'A'.val), valid := ⋯ } else c
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintLabelPart.mk.injEq : ∀ (value : String) (tooltip? : Option String) (location? : Option Lean.Elab.InlayHintLinkLocation) (value_1 : String)
  (tooltip?_1 : Option String) (location?_1 : Option Lean.Elab.InlayHintLinkLocation),
  ({ value := value, tooltip? := tooltip?, location? := location? } =
      { value := value_1, tooltip? := tooltip?_1, location? := location?_1 }) =
    (value = value_1 ∧ tooltip? = tooltip?_1 ∧ location? = location?_1)
-- Mathlib.MeasureTheory.Measure.Dirac
/-- Two measures on a countable space are equal if and only if they agree on singletons.  -/
MeasureTheory.Measure.ext_iff_singleton : ∀ {α : Type u_1} [inst : MeasurableSpace α] [Countable α] {μ ν : MeasureTheory.Measure α},
  μ = ν ↔ ∀ (a : α), μ {a} = ν {a}
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.piCongrLeft'.eq_1 : ∀ {ι : Type u_7} {ι' : Type u_8} (R : ι → Type u_9) (e : ι ≃ ι') [inst : (i : ι) → NonUnitalNonAssocSemiring (R i)],
  RingEquiv.piCongrLeft' R e = { toEquiv := Equiv.piCongrLeft' R e, map_mul' := ⋯, map_add' := ⋯ }
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.symm_symm : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Mul M]
  [inst_3 : Mul N] (f : M ≃ₜ* N), f.symm.symm = f
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.IsStableUnderBaseChange.isomorphisms : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  (CategoryTheory.MorphismProperty.isomorphisms C).IsStableUnderBaseChange
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.getLetPatDeclVars : Lean.Syntax → Lean.Elab.TermElabM (Array Lean.Elab.Term.Do.Var)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
/-- The pushforward of an ideal sheaf.  -/
AlgebraicGeometry.Scheme.IdealSheafData.map : {X Y : AlgebraicGeometry.Scheme} → X.IdealSheafData → (X ⟶ Y) → Y.IdealSheafData
-- Mathlib.Data.Finset.Max
/-- To rewrite from right to left, use `Monotone.map_finset_min'`.  -/
Finset.min'_image : ∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β},
  Monotone f → ∀ (s : Finset α) (h : (Finset.image f s).Nonempty), (Finset.image f s).min' h = f (s.min' ⋯)
-- Init.Control.Lawful.MonadLift.Instances
StateCpsT.instLawfulMonadLiftOfLawfulMonad : ∀ {m : Type u → Type v} {σ : Type u} [inst : Monad m] [LawfulMonad m], LawfulMonadLift m (StateCpsT σ m)
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.quasiMeasurePreserving_eval : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] (i : ι),
  MeasureTheory.Measure.QuasiMeasurePreserving (Function.eval i) (MeasureTheory.Measure.pi μ) (μ i)
-- Init.Data.Iterators.Lemmas.Basic
_private.Init.Data.Iterators.Lemmas.Basic.0.Std.Iter.inductSteps.eq_def : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [inst_1 : Std.Iterators.Finite α Id] (motive : Std.Iter β → Sort x)
  (step :
    (it : Std.Iter β) →
      ({it' : Std.Iter β} → {out : β} → it.IsPlausibleStep (Std.IterStep.yield it' out) → motive it') →
        ({it' : Std.Iter β} → it.IsPlausibleStep (Std.IterStep.skip it') → motive it') → motive it)
  (it : Std.Iter β),
  Std.Iter.inductSteps motive step it =
    step it (fun {it'} {x} x_1 => Std.Iter.inductSteps motive step it') fun {it'} x =>
      Std.Iter.inductSteps motive step it'
-- Mathlib.Analysis.Normed.Group.AddTorsor
LipschitzWith.vsub : ∀ {α : Type u_1} {V : Type u_2} {P : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] [inst_3 : PseudoEMetricSpace α] {f g : α → P} {Kf Kg : NNReal},
  LipschitzWith Kf f → LipschitzWith Kg g → LipschitzWith (Kf + Kg) (f -ᵥ g)
-- Mathlib.Algebra.Algebra.Unitization
NonUnitalAlgHom.toAlgHom_zero : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A], ⇑(NonUnitalAlgHom.toAlgHom 0) = fun x => x.toProd.1
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_roc_succ_right_eq_append : ∀ {m n : ℤ}, m ≤ n → (m<...=n + 1).toList = (m<...=n).toList ++ [n + 1]
-- Init.Data.Array.Lemmas
Array.back?_flatten : ∀ {α : Type u_1} {xss : Array (Array α)}, xss.flatten.back? = Array.findSome? (fun xs => xs.back?) xss.reverse
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.tensorCongr_SpecTensorTo_assoc : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} {T T' : AlgebraicGeometry.Scheme.Pullback.Triplet f g}
  (h : T = T') {Z : AlgebraicGeometry.Scheme} (h_1 : CategoryTheory.Limits.pullback f g ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr h).hom)
      (CategoryTheory.CategoryStruct.comp T.SpecTensorTo h_1) =
    CategoryTheory.CategoryStruct.comp T'.SpecTensorTo h_1
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.nndist_eq_of_L1 : ∀ {ι : Type u_2} {β : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedAddCommGroup (β i)]
  (x y : PiLp 1 β), nndist x y = ∑ i, nndist (x.ofLp i) (y.ofLp i)
-- Mathlib.Order.SuccPred.Basic
/-- **Alias** of `Order.le_succ_of_wcovBy`.

---

See also `Order.succ_eq_of_covBy`.  -/
WCovBy.le_succ : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] {a b : α}, a ⩿ b → b ≤ Order.succ a
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Zipper.prependMapGT.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (lowerBound : α) (it : Std.DTreeMap.Internal.Zipper α β) (sz : ℕ) (k : α)
  (v : β k) (l r : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Zipper.prependMapGT (Std.DTreeMap.Internal.Impl.inner sz k v l r) lowerBound it =
    match compare lowerBound k with
    | Ordering.lt => Std.DTreeMap.Internal.Zipper.prependMapGT l lowerBound (Std.DTreeMap.Internal.Zipper.cons k v r it)
    | Ordering.eq => Std.DTreeMap.Internal.Zipper.prependMapGT r lowerBound it
    | Ordering.gt => Std.DTreeMap.Internal.Zipper.prependMapGT r lowerBound it
-- Mathlib.RingTheory.IsTensorProduct
/-- If `N` is the base change of `M` to `A`, then `N ⊗[R] P` is the base change
of `M ⊗[R] P` to `A`. This is simply the isomorphism
`A ⊗[S] (M ⊗[R] P) ≃ₗ[A] (A ⊗[S] M) ⊗[R] P`.  -/
isBaseChange_tensorProduct_map : ∀ {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N]
  [inst_2 : CommSemiring R] [inst_3 : CommSemiring S] [inst_4 : Algebra R S] [inst_5 : Module R M] [inst_6 : Module R N]
  [inst_7 : Module S N] [inst_8 : IsScalarTower R S N] {P : Type u_2} [inst_9 : AddCommMonoid P] [inst_10 : Module R P]
  (A : Type u_4) [inst_11 : CommSemiring A] [inst_12 : Algebra R A] [inst_13 : Algebra S A] [IsScalarTower R S A]
  [inst_15 : Module S M] [inst_16 : IsScalarTower R S M] [inst_17 : Module A N] [inst_18 : IsScalarTower S A N]
  [inst_19 : IsScalarTower R A N] {f : M →ₗ[S] N},
  IsBaseChange A f → IsBaseChange A (TensorProduct.AlgebraTensorModule.map f LinearMap.id)
-- Mathlib.GroupTheory.Torsion
/-- If a group exponent exists, the additive group is torsion.  -/
ExponentExists.isAddTorsion : ∀ {G : Type u_1} [inst : AddGroup G], AddMonoid.ExponentExists G → IsAddTorsion G
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.coe_map : ∀ {R : Type u_2} {M : Type u_4} {N : Type u_5} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R M] [inst_5 : Module R N] (C : ConvexCone R M) (f : M →ₗ[R] N),
  ↑(ConvexCone.map f C) = ⇑f '' ↑C
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.lineMap_lineMap_left : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
  [inst_3 : AddTorsor V1 P1] (p₀ p₁ : P1) (c d : k),
  (AffineMap.lineMap ((AffineMap.lineMap p₀ p₁) c) p₁) d = (AffineMap.lineMap p₀ p₁) (1 - (1 - d) * (1 - c))
-- Mathlib.RingTheory.Ideal.Colon
Submodule.inf_colon : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {N₁ N₂ : Submodule R M} {S : Set M}, (N₁ ⊓ N₂).colon S = N₁.colon S ⊓ N₂.colon S
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Run `simp_all? +suggestions` at every step in proofs, reporting where it succeeds.  -/
tryAtEachStepSimpAllSuggestions : Mathlib.TacticAnalysis.Config
-- Std.Data.Iterators.Lemmas.Consumers.Collect
Std.Iter.Equiv.toArray_eq : ∀ {α₁ β α₂ : Type u_1} [inst : Std.Iterator α₁ Id β] [inst_1 : Std.Iterator α₂ Id β] [Std.Iterators.Finite α₁ Id]
  [Std.Iterators.Finite α₂ Id] {ita : Std.Iter β} {itb : Std.Iter β}, ita.Equiv itb → ita.toArray = itb.toArray
-- Mathlib.Algebra.Free
FreeAddSemigroup.hom_ext_iff : ∀ {α : Type u} {β : Type v} [inst : Add β] {f g : FreeAddSemigroup α →ₙ+ β},
  f = g ↔ ⇑f ∘ FreeAddSemigroup.of = ⇑g ∘ FreeAddSemigroup.of
-- Mathlib.RingTheory.RingHom.EssFiniteType
RingHom.EssFiniteType.of_comp : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  (f : R →+* S) {g : S →+* T}, (g.comp f).EssFiniteType → g.EssFiniteType
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.dual_contract : ∀ {α : Type u_1} (M : Matroid α) (X : Set α), (M.contract X)✶ = M✶.delete X
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddMod.addMod : {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.MonoidalLeftAction C D] →
            {A : C} →
              [inst_4 : CategoryTheory.AddMonObj A] →
                (self : CategoryTheory.AddMod D A) → CategoryTheory.AddModObj A self.X