mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Valued.WithVal
NumberField.RingOfIntegers.withValEquiv_symm_apply : ∀ {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] {K : Type u_3} [inst_1 : Field K] (v : Valuation K Γ₀)
  (R : Type u_4) [inst_2 : CommRing R] [inst_3 : Algebra R K] [inst_4 : IsIntegralClosure R ℤ K] (a : R),
  (NumberField.RingOfIntegers.withValEquiv v R).symm a =
    (IsIntegralClosure.equiv ℤ R (WithVal v) (NumberField.RingOfIntegers (WithVal v))) a
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.contains_inter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (t₁ ∩ t₂).contains k = (t₁.contains k && t₂.contains k)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_add_size_eq_size_union_add_size_inter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → m₁.size + m₂.size = (m₁ ∪ m₂).size + (m₁ ∩ m₂).size
-- Mathlib.Analysis.SpecialFunctions.Arcosh
Real.contDiffOn_arcosh : ∀ {n : WithTop ℕ∞}, ContDiffOn ℝ n Real.arcosh (Set.Ioi 1)
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
CategoryTheory.SimplicialObject.Splitting.toNondegComplex_f_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  [inst_1 : CategoryTheory.Preadditive C] (n : ℕ) {Z : C} (h : s.nondegComplex.X n ⟶ Z),
  CategoryTheory.CategoryStruct.comp (s.toNondegComplex.f n) h =
    CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f n)
      (CategoryTheory.CategoryStruct.comp (s.toKaroubiNondegComplexIsoN₁.inv.f.f n) h)
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.exists_bifibrant_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {X₁ X₂ : HomotopicalAlgebra.CofibrantObject C} (f : X₁ ⟶ X₂),
  ∃ g,
    CategoryTheory.CategoryStruct.comp X₁.iBifibrantResolutionObj
        (HomotopicalAlgebra.BifibrantObject.ιCofibrantObject.map g) =
      CategoryTheory.CategoryStruct.comp f X₂.iBifibrantResolutionObj
-- Mathlib.CategoryTheory.Sites.SheafOfTypes
/-- The base of a sieve `S` is a colimit of `S` iff all Yoneda-presheaves satisfy
the sheaf condition for `S`.
 -/
CategoryTheory.Sieve.forallYonedaIsSheaf_iff_colimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (S : CategoryTheory.Sieve X),
  (∀ (W : C), CategoryTheory.Presieve.IsSheafFor (CategoryTheory.yoneda.obj W) S.arrows) ↔
    Nonempty (CategoryTheory.Limits.IsColimit S.arrows.cocone)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_eq_append : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] (k : α → Ordering) [Std.Internal.IsStrictCut compare k]
  {l : Std.DTreeMap.Internal.Impl α β},
  l.Ordered →
    l.toListModel =
      List.filter (fun x => k x.fst == Ordering.gt) l.toListModel ++
          (List.find? (fun x => k x.fst == Ordering.eq) l.toListModel).toList ++
        List.filter (fun x => k x.fst == Ordering.lt) l.toListModel
-- Mathlib.Data.Set.Finite.Basic
List.finite_toSet : ∀ {α : Type u} (l : List α), {x | x ∈ l}.Finite
-- Mathlib.Algebra.GCDMonoid.Basic
gcd_isUnit_iff_isRelPrime : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] {a b : α}, IsUnit (gcd a b) ↔ IsRelPrime a b
-- Init.Data.Array.Lemmas
Array.all_append : ∀ {α : Type u_1} {f : α → Bool} {xs ys : Array α}, (xs ++ ys).all f = (xs.all f && ys.all f)
-- Mathlib.CategoryTheory.Retract
CategoryTheory.Retract.refl_r : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C),
  (CategoryTheory.Retract.refl X).r = CategoryTheory.CategoryStruct.id X
-- Mathlib.Order.Partition.Basic
Partition.disjoint : ∀ {α : Type u_1} {s x y : α} [inst : CompleteLattice α] {P : Partition s}, x ∈ P → y ∈ P → x ≠ y → Disjoint x y
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
IsCyclotomicExtension.Rat.associated_sub_one_of_isPrimitiveRoot : ∀ (p : ℕ) {K : Type u_1} [inst : Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ p) [inst_1 : NeZero p] {η : K}
  (hη : IsPrimitiveRoot η p), Associated (hζ.toInteger - 1) (hη.toInteger - 1)
-- Mathlib.LinearAlgebra.TensorProduct.Map
/-- Given semilinear maps `f : M → P`, `g : N → Q`, if we identify `M ⊗ N` with `N ⊗ M` and `P ⊗ Q`
with `Q ⊗ P`, then this lemma states that `f ⊗ g = g ⊗ f`.  -/
TensorProduct.map_comp_comm_eq : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7}
  {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N]
  [inst_4 : AddCommMonoid M₂] [inst_5 : AddCommMonoid N₂] [inst_6 : Module R M] [inst_7 : Module R N]
  [inst_8 : Module R₂ M₂] [inst_9 : Module R₂ N₂] (f : M →ₛₗ[σ₁₂] M₂) (g : N →ₛₗ[σ₁₂] N₂),
  TensorProduct.map f g ∘ₛₗ ↑(TensorProduct.comm R N M) = ↑(TensorProduct.comm R₂ N₂ M₂) ∘ₛₗ TensorProduct.map g f
-- Mathlib.CategoryTheory.Opposites
/-- If F is faithful then the `leftOp` of F is also faithful.  -/
CategoryTheory.Functor.leftOp_faithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C Dᵒᵖ} [F.Faithful], F.leftOp.Faithful
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.EqCnstr.brecOn.go : {motive_1 : Lean.Meta.Grind.Arith.Linear.EqCnstr → Sort u} →
  {motive_2 : Lean.Meta.Grind.Arith.Linear.EqCnstrProof → Sort u} →
    {motive_3 : Lean.Meta.Grind.Arith.Linear.IneqCnstr → Sort u} →
      {motive_4 : Lean.Meta.Grind.Arith.Linear.IneqCnstrProof → Sort u} →
        {motive_5 : Lean.Meta.Grind.Arith.Linear.DiseqCnstr → Sort u} →
          {motive_6 : Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof → Sort u} →
            {motive_7 : Lean.Meta.Grind.Arith.Linear.UnsatProof → Sort u} →
              (t : Lean.Meta.Grind.Arith.Linear.EqCnstr) →
                ((t : Lean.Meta.Grind.Arith.Linear.EqCnstr) → t.below → motive_1 t) →
                  ((t : Lean.Meta.Grind.Arith.Linear.EqCnstrProof) → t.below → motive_2 t) →
                    ((t : Lean.Meta.Grind.Arith.Linear.IneqCnstr) → t.below → motive_3 t) →
                      ((t : Lean.Meta.Grind.Arith.Linear.IneqCnstrProof) → t.below → motive_4 t) →
                        ((t : Lean.Meta.Grind.Arith.Linear.DiseqCnstr) → t.below → motive_5 t) →
                          ((t : Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof) → t.below → motive_6 t) →
                            ((t : Lean.Meta.Grind.Arith.Linear.UnsatProof) → t.below → motive_7 t) →
                              motive_1 t ×' t.below
-- Mathlib.Order.Irreducible
/-- **Alias** of the reverse direction of `supPrime_iff_supIrred`. -/
SupIrred.supPrime : ∀ {α : Type u_2} [inst : DistribLattice α] {a : α}, SupIrred a → SupPrime a
-- Mathlib.Data.Set.Basic
Set.not_nonempty_empty : ∀ {α : Type u}, ¬∅.Nonempty
-- Std.Http.Data.URI.Basic
/-- Attempts to create a `Scheme` from a string, normalizing to lowercase.
Returns `none` if the scheme is invalid per RFC 3986 Section 3.1.
 -/
Std.Http.URI.Scheme.ofString? : String → Option Std.Http.URI.Scheme
-- Init.Data.String.Lemmas.Pattern.TakeDrop.String
String.Slice.skipSuffix?_slice_eq_some_iff : ∀ {pat s : String.Slice} {pos : s.Pos}, s.skipSuffix? pat = some pos ↔ ∃ t, pos.Splits t pat.copy
-- Mathlib.Algebra.Category.CommAlgCat.Monoidal
CommAlgCat.instMonoidalCategory : {R : Type u} → [inst : CommRing R] → CategoryTheory.MonoidalCategory (CommAlgCat R)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.mem_support_nil_iff : ∀ {V : Type u} {G : SimpleGraph V} {u v : V}, u ∈ SimpleGraph.Walk.nil.support ↔ u = v
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
Ordinal.CNF.coeff_zero_right : ∀ (b : Ordinal.{u_1}), Ordinal.CNF.coeff b 0 = 0
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.comp_add_left_iff : ∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] {f : ℝ → ε} {a b : ℝ}
  [TopologicalSpace.PseudoMetrizableSpace ε] {c : ℝ},
  autoParam (‖f (min a b)‖ₑ ≠ ⊤) IntervalIntegrable.comp_add_left_iff._auto_1 →
    (IntervalIntegrable (fun x => f (c + x)) MeasureTheory.volume (a - c) (b - c) ↔
      IntervalIntegrable f MeasureTheory.volume a b)
-- Mathlib.Algebra.Group.Units.Equiv
Units.mulRight_symm : ∀ {M : Type u_3} [inst : Monoid M] (u : Mˣ), Equiv.symm u.mulRight = u⁻¹.mulRight
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst_assoc : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g]
  (s : CategoryTheory.Limits.PullbackCone f g) (i j : 𝒰.I₀) {Z_1 : AlgebraicGeometry.Scheme}
  (h : CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap 𝒰 f g s i j)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) (𝒰.f i))
          (𝒰.f j))
        h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry s.fst (𝒰.f i)).hom
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pullback.map (𝒰.f i) s.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g
            (CategoryTheory.CategoryStruct.id (𝒰.X i)) s.snd f ⋯ ⋯)
          h))
-- Init.Data.Range.Polymorphic.Map
Std.PRange.UpwardEnumerable.Map.mk : {α : Type u} →
  {β : Type v} →
    [inst : Std.PRange.UpwardEnumerable α] →
      [inst_1 : Std.PRange.UpwardEnumerable β] →
        (toFun : α → β) →
          Function.Injective toFun →
            (∀ (a : α), Std.PRange.succ? (toFun a) = Option.map toFun (Std.PRange.succ? a)) →
              (∀ (n : ℕ) (a : α), Std.PRange.succMany? n (toFun a) = Option.map toFun (Std.PRange.succMany? n a)) →
                Std.PRange.UpwardEnumerable.Map α β
-- Lean.Elab.Do.Basic
Lean.Elab.Do.instInhabitedContInfo : Inhabited Lean.Elab.Do.ContInfo
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.ofNat_eq_toENat : ∀ {c : Cardinal.{u}} {n : ℕ} [inst : n.AtLeastTwo], OfNat.ofNat n = Cardinal.toENat c ↔ OfNat.ofNat n = c
-- Mathlib.Data.NNReal.Defs
Real.toNNReal_coe : ∀ {r : NNReal}, (↑r).toNNReal = r
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- Assumes left covariance.
The lemma assuming right covariance is `Right.one_lt_mul_of_le_of_lt`.  -/
Left.one_lt_mul_of_le_of_lt : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulLeftStrictMono α] {a b : α}, 1 ≤ a → 1 < b → 1 < a * b
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.average_neg : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  (μ : MeasureTheory.Measure α) (f : α → E), ⨍ (x : α), -f x ∂μ = -⨍ (x : α), f x ∂μ
-- Mathlib.Analysis.Convex.Deriv
StrictConvexOn.rightDeriv_lt_slope : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y : ℝ},
  StrictConvexOn ℝ S f →
    x ∈ S → y ∈ S → x < y → DifferentiableWithinAt ℝ f (Set.Ioi x) x → derivWithin f (Set.Ioi x) x < slope f x y
-- Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
BoundedContinuousFunction.charAlgHom_apply : ∀ {V : Type u_1} {W : Type u_2} [inst : AddCommGroup V] [inst_1 : Module ℝ V] [inst_2 : TopologicalSpace V]
  [inst_3 : AddCommGroup W] [inst_4 : Module ℝ W] [inst_5 : TopologicalSpace W] {e : AddChar ℝ Circle}
  {L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ} {he : Continuous ⇑e} {hL : Continuous fun p => (L p.1) p.2} (w : AddMonoidAlgebra ℂ W)
  (v : V), ((BoundedContinuousFunction.charAlgHom he hL) w) v = w.coeff.sum fun a z => z • ↑(e ((L v) a))
-- Mathlib.Data.EReal.Basic
EReal.bot_ne_zero : ⊥ ≠ 0
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
LinearIndependent.notMem_span : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [Nontrivial R], LinearIndependent R v → ∀ (i : ι), v i ∉ Submodule.span R (v '' {i}ᶜ)
-- Mathlib.Order.Atoms
IsCoatom.Ici : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : OrderTop α] {a x : α}, IsCoatom a → ∀ (hax : x ≤ a), IsCoatom ⟨a, hax⟩
-- Std.Data.Internal.Cut
Std.Internal.instIsStrictCutCompare : ∀ {α : Type u} [inst : Ord α] [Std.TransOrd α] {k : α}, Std.Internal.IsStrictCut compare (compare k)
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.ext_iff : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] {I J : TwoSidedIdeal R}, I = J ↔ ∀ (x : R), x ∈ I ↔ x ∈ J
-- Init.Data.Int.Gcd
Int.lcm_eq_natAbs_right : ∀ {a b : ℤ}, a ∣ b → a.lcm b = b.natAbs
-- Mathlib.AlgebraicGeometry.ResidueField
/-- If `U` is an open of `X` containing `x`, we have a canonical ring map from the sections
over `U` to the residue field of `x`.

If we interpret sections over `U` as functions of `X` defined on `U`, then this ring map
corresponds to evaluation at `x`.
 -/
AlgebraicGeometry.Scheme.evaluation : (X : AlgebraicGeometry.Scheme) → (U : X.Opens) → (x : ↥X) → x ∈ U → (X.presheaf.obj (Opposite.op U) ⟶ X.residueField x)
-- Mathlib.Topology.ContinuousMap.Defs
/-- `C(X, Y)` is the type of continuous maps from `X` to `Y`.  -/
«termC(_,_)» : Lean.ParserDescr
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.LocallyIntegrable.mono_measure : ∀ {X : Type u_1} {ε : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace ε]
  [inst_3 : ContinuousENorm ε] {f : X → ε} {μ ν : MeasureTheory.Measure X},
  MeasureTheory.LocallyIntegrable f μ → ν ≤ μ → MeasureTheory.LocallyIntegrable f ν
-- Init.Data.UInt.Basic
USize.le_size : 2 ^ 32 ≤ USize.size
-- Mathlib.Data.QPF.Multivariate.Constructions.Cofix
/-- Equivalence relation on M-types representing a value of type `Cofix F`  -/
MvQPF.Mcongr : {n : ℕ} →
  {F : TypeVec.{u} (n + 1) → Type u} → [q : MvQPF F] → {α : TypeVec.{u} n} → (MvQPF.P F).M α → (MvQPF.P F).M α → Prop
-- Mathlib.RingTheory.RingHom.FinitePresentation
/-- Finite-presentation can be checked on a standard covering of the target.  -/
RingHom.finitePresentation_ofLocalizationSpanTarget : RingHom.OfLocalizationSpanTarget @RingHom.FinitePresentation
-- Mathlib.Geometry.Manifold.MFDeriv.FDeriv
/-- For maps between vector spaces, `MDifferentiableOn` and `DifferentiableOn` coincide  -/
mdifferentiableOn_iff_differentiableOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {f : E → E'}
  {s : Set E}, MDiff[s] f ↔ DifferentiableOn 𝕜 f s
-- Std.Do.SPred.Laws
Std.Do.SPred.entails.eq_1 : ∀ (P_2 Q_2 : Std.Do.SPred []), (P_2 ⊢ₛ Q_2) = (P_2.down → Q_2.down)
-- Std.Http.Data.Response
Std.Http.Response.Builder.mk.sizeOf_spec : ∀ (line : Std.Http.Response.Head) (extensions : Std.Http.Extensions),
  sizeOf { line := line, extensions := extensions } = 1 + sizeOf line + sizeOf extensions
-- Mathlib.Algebra.NonAssoc.PreLie.Basic
LeftPreLieRing.ext : ∀ {L : Type u_1} {x y : LeftPreLieRing L},
  Add.add = Add.add →
    Zero.zero = Zero.zero →
      NSMul.nsmul = NSMul.nsmul →
        Neg.neg = Neg.neg → Sub.sub = Sub.sub → ZSMul.zsmul = ZSMul.zsmul → Mul.mul = Mul.mul → x = y
-- Mathlib.Data.Nat.Factorization.LCM
Nat.factorizationLCMRight_zero_right : ∀ (a : ℕ), a.factorizationLCMRight 0 = 1
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roo.isSome_succMany?_of_lt_size_toArray : ∀ {α : Type u} {r : Std.Roo α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.Rxo.IsAlwaysFinite α] {i : ℕ}, i < r.toArray.size → (Std.PRange.succMany? (i + 1) r.lower).isSome = true
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- Reorder a sum.

The difference with `Finset.sum_bij'` is that the bijection is specified as a surjective injection,
rather than by an inverse function.

The difference with `Finset.sum_nbij` is that the bijection is allowed to use membership of the
domain of the sum, rather than being a non-dependent function.  -/
Finset.sum_bij : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [inst : AddCommMonoid M] {s : Finset ι} {t : Finset κ} {f : ι → M}
  {g : κ → M} (i : (a : ι) → a ∈ s → κ),
  (∀ (a : ι) (ha : a ∈ s), i a ha ∈ t) →
    (∀ (a₁ : ι) (ha₁ : a₁ ∈ s) (a₂ : ι) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂) →
      (∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b) →
        (∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)) → ∑ x ∈ s, f x = ∑ x ∈ t, g x
-- Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
_private.Mathlib.AlgebraicTopology.SimplicialSet.Degenerate.0.SSet.unique_nonDegenerate.map_g_op_y₂ : ∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := n })} {m₁ m₂ : ℕ} {f₁ : { len := n } ⟶ { len := m₁ }}
  (hf₁ : CategoryTheory.SplitEpi f₁) {y₁ : ↑(X.nonDegenerate m₁)},
  x = (CategoryTheory.ConcreteCategory.hom (X.map f₁.op)) ↑y₁ →
    ∀ {f₂ : { len := n } ⟶ { len := m₂ }} {y₂ : X.obj (Opposite.op { len := m₂ })},
      x = (CategoryTheory.ConcreteCategory.hom (X.map f₂.op)) y₂ →
        (CategoryTheory.ConcreteCategory.hom (X.map (SSet.unique_nonDegenerate.g✝ hf₁ f₂).op)) y₂ = ↑y₁
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
SSet.Subcomplex.Pairing.ofIso.congr_simp : ∀ {X : SSet} {A : X.Subcomplex} (P P_1 : A.Pairing),
  P = P_1 →
    ∀ {Y : SSet} {B : Y.Subcomplex} (e e_1 : Y ≅ X) (e_e : e = e_1) (hA : A.preimage e.hom = B),
      P.ofIso e hA = P_1.ofIso e_1 ⋯
-- Mathlib.Algebra.GroupWithZero.Action.Pi
Pi.smulWithZero' : {I : Type u} →
  {f : I → Type v} →
    {g : I → Type u_1} →
      [inst : (i : I) → Zero (g i)] →
        [inst_1 : (i : I) → Zero (f i)] →
          [(i : I) → SMulWithZero (g i) (f i)] → SMulWithZero ((i : I) → g i) ((i : I) → f i)
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.ConstPromiseVal.mk.injEq : ∀ (privateConstInfo exportedConstInfo : Lean.ConstantInfo) (exts : Array Lean.EnvExtensionState)
  (nestedConsts : Lean.VisibilityMap✝ Lean.AsyncConsts✝) (privateConstInfo_1 exportedConstInfo_1 : Lean.ConstantInfo)
  (exts_1 : Array Lean.EnvExtensionState) (nestedConsts_1 : Lean.VisibilityMap✝ Lean.AsyncConsts✝),
  ({ privateConstInfo := privateConstInfo, exportedConstInfo := exportedConstInfo, exts := exts,
        nestedConsts := nestedConsts } =
      { privateConstInfo := privateConstInfo_1, exportedConstInfo := exportedConstInfo_1, exts := exts_1,
        nestedConsts := nestedConsts_1 }) =
    (privateConstInfo = privateConstInfo_1 ∧
      exportedConstInfo = exportedConstInfo_1 ∧ exts = exts_1 ∧ nestedConsts = nestedConsts_1)
-- Mathlib.Data.DFinsupp.Module
DFinsupp.coeFnLinearMap_apply : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : Semiring γ] [inst_1 : (i : ι) → AddCommMonoid (β i)]
  [inst_2 : (i : ι) → Module γ (β i)] (v : Π₀ (i : ι), β i), (DFinsupp.coeFnLinearMap γ) v = ⇑v
-- Mathlib.RingTheory.Ideal.Cotangent
IsLocalRing.instModuleResidueFieldCotangentSpace : (R : Type u_1) →
  [inst : CommRing R] → [inst_1 : IsLocalRing R] → Module (IsLocalRing.ResidueField R) (IsLocalRing.CotangentSpace R)
-- Std.Http.Data.URI.Basic
Std.Http.URI.Port.omitted.sizeOf_spec : sizeOf Std.Http.URI.Port.omitted = 1
-- Lean.DocString.Markdown
Lean.Doc.MdRendererState.mk.inj : ∀ {imported current imported_1 current_1 : Lean.NameMap Lean.Name},
  { imported := imported, current := current } = { imported := imported_1, current := current_1 } →
    imported = imported_1 ∧ current = current_1
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMap.mk.injEq : ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H} (toFun : G → H)
  (map_add_const' : ∀ (x : G), toFun (x + a) = toFun x + b) (toFun_1 : G → H)
  (map_add_const'_1 : ∀ (x : G), toFun_1 (x + a) = toFun_1 x + b),
  ({ toFun := toFun, map_add_const' := map_add_const' } = { toFun := toFun_1, map_add_const' := map_add_const'_1 }) =
    (toFun = toFun_1)
-- Mathlib.GroupTheory.Solvable
/-- **Alias** of `Group.isSolvable_of_isSolvable_injective`. -/
solvable_of_solvable_injective : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] {f : G →* G'},
  Function.Injective ⇑f → ∀ [Group.IsSolvable G'], Group.IsSolvable G
-- Mathlib.Logic.Equiv.Defs
Equiv.lt_def : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) [inst : LT β] (a b : α), e a < e b ↔ a < b
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.cokernelOrderHom_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasCokernels C] (X : C) (a : CategoryTheory.Subobject X),
  (CategoryTheory.Limits.cokernelOrderHom X) a =
    CategoryTheory.Subobject.lift (fun x f x_1 => CategoryTheory.Subobject.mk (CategoryTheory.Limits.cokernel.π f).op) ⋯
      a
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- The uniqueness of `lift`.  -/
CategoryTheory.WithInitial.liftUnique : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        {Z : D} →
          (F : CategoryTheory.Functor C D) →
            (M : (x : C) → Z ⟶ F.obj x) →
              (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (M x) (F.map f) = M y) →
                (G : CategoryTheory.Functor (CategoryTheory.WithInitial C) D) →
                  (h : CategoryTheory.WithInitial.incl.comp G ≅ F) →
                    (hG : G.obj CategoryTheory.WithInitial.star ≅ Z) →
                      (∀ (x : C),
                          CategoryTheory.CategoryStruct.comp hG.symm.hom
                              (G.map
                                (CategoryTheory.WithInitial.starInitial.to (CategoryTheory.WithInitial.incl.obj x))) =
                            CategoryTheory.CategoryStruct.comp (M x) (h.symm.hom.app x)) →
                        (G ≅ CategoryTheory.WithInitial.lift F M hM)
-- Init.Data.Range.Polymorphic.IntLemmas
/-- Induction principle for proving properties of `Int`-based ranges of the form `a<...b` by
varying the lower bound.

In the `base` case, one proves that for any `a : Int` and `b : Int` with
`b ≤ a + 1`, the statement holds for the empty range `a<...b`.

In the `step` case, one proves that for any `a : Int` and `b : Int`, the
statement holds for nonempty ranges `a<...b` if it holds for the smaller range
`(a + 1)<...b`.

The following is an example reproving `length_toList_roo`.

```
example (a b : Int) : (a<...b).toList.length = (b - a - 1).toNat := by
  induction a, b using Int.induct_roo_left
  case base =>
    simp only [Int.toList_roo_eq_nil, List.length_nil, Int.zero_eq_toNat_sub_iff, *]; omega
  case step =>
    simp only [Int.toList_roo_eq_cons, List.length_cons, *]; omega
``` -/
Int.induct_roo_left : ∀ (motive : ℤ → ℤ → Prop),
  (∀ (a b : ℤ), b ≤ a + 1 → motive a b) →
    (∀ (a b : ℤ), a + 1 < b → motive (a + 1) b → motive a b) → ∀ (a b : ℤ), motive a b
-- Lean.Meta.Tactic.Grind.Internalize
_private.Lean.Meta.Tactic.Grind.Internalize.0.Lean.Meta.Grind.mkEMatchTheoremWithKind'? : Lean.Meta.Grind.Origin →
  Array Lean.Name →
    Lean.Expr →
      Lean.Meta.Grind.EMatchTheoremKind →
        Lean.Meta.Grind.SymbolPriorities → Lean.MetaM (Option Lean.Meta.Grind.EMatchTheorem)
-- Init.Data.Int.DivMod.Lemmas
Int.negSucc_dvd : ∀ {a : ℕ} {b : ℤ}, Int.negSucc a ∣ b ↔ ↑(a + 1) ∣ b
-- Mathlib.Data.Sign.Defs
SignType.instHasDistribNeg : HasDistribNeg SignType
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.LiftRelO.eq_2 : ∀ {α : Type u} {β : Type v} (R : α → β → Prop) (C : Stream'.WSeq α → Stream'.WSeq β → Prop) (a : α) (s : Stream'.WSeq α)
  (b : β) (t : Stream'.WSeq β), Stream'.WSeq.LiftRelO R C (some (a, s)) (some (b, t)) = (R a b ∧ C s t)
-- Mathlib.GroupTheory.GroupAction.ConjAct
ConjAct.unitsSMulCommClass' : ∀ (α : Type u_1) {M : Type u_2} [inst : Monoid M] [inst_1 : SMul α M] [SMulCommClass M α M] [IsScalarTower α M M],
  SMulCommClass (ConjAct Mˣ) α M