mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Multiset.Sum
Multiset.inr_mem_disjSum : ∀ {α : Type u_1} {β : Type u_2} {s : Multiset α} {t : Multiset β} {b : β}, Sum.inr b ∈ s.disjSum t ↔ b ∈ t
-- Mathlib.CategoryTheory.Distributive.Monoidal
CategoryTheory.IsMonoidalLeftDistrib.of_isIso_coprodComparisonTensorLeft : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C]
  [i :
    ∀ {X Y Z : C},
      CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison (CategoryTheory.MonoidalCategory.tensorLeft X) Y Z)],
  CategoryTheory.IsMonoidalLeftDistrib C
-- Mathlib.Analysis.Calculus.FDeriv.Add
DifferentiableWithinAt.const_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} {s : Set E}, DifferentiableWithinAt 𝕜 f s x → ∀ (c : F), DifferentiableWithinAt 𝕜 (fun y => c - f y) s x
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.Full.map_surjective : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {F : CategoryTheory.Functor C D} [self : F.Full] {X Y : C}, Function.Surjective F.map
-- Mathlib.RingTheory.MvPowerSeries.Derivative
/-- If `f` and `g` have the same constant term and all partial derivatives, then they are equal.

The `CommRing` assumption is needed because the proof uses `smul_right_inj`, which requires
cancellation of addition in `R`; `IsAddTorsionFree` alone does not suffice.  -/
MvPowerSeries.pderiv.ext : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R] [IsAddTorsionFree R] {f g : MvPowerSeries σ R},
  (∀ (i : σ), (MvPowerSeries.pderiv R i) f = (MvPowerSeries.pderiv R i) g) →
    MvPowerSeries.constantCoeff f = MvPowerSeries.constantCoeff g → f = g
-- Mathlib.Algebra.Order.Module.Defs
smul_pos_iff_of_pos_right : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulWithZero α β]
  [inst_3 : Preorder α] [inst_4 : Preorder β] [SMulPosStrictMono α β] [SMulPosReflectLT α β],
  0 < b → (0 < a • b ↔ 0 < a)
-- Init.Core
/-- Left identity `o` is an identity.  -/
Std.LawfulLeftIdentity.left_id : ∀ {α : Sort u} {β : Sort u_1} {op : α → β → β} {o : outParam α} [self : Std.LawfulLeftIdentity op o] (a : β), op o a = a
-- Mathlib.CategoryTheory.ConcreteCategory.EpiMono
CategoryTheory.ConcreteCategory.mono_iff_injective_of_preservesPullback : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {X Y : C}
  (f : X ⟶ Y)
  [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan (CategoryTheory.forget C)],
  CategoryTheory.Mono f ↔ Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- **Alias** of `MonoidAlgebra.coeff_mapRingEquiv`. -/
MonoidAlgebra.mapRangeRingEquiv_apply : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Monoid M]
  (e : R ≃+* S) (x : MonoidAlgebra R M) (m : M), ((MonoidAlgebra.mapRingEquiv M e) x).coeff m = e (x.coeff m)
-- Mathlib.Algebra.Algebra.Equiv
MulSemiringAction.toRingEquiv_algEquiv : ∀ {R : Type uR} {A₁ : Type uA₁} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Algebra R A₁]
  (σ : A₁ ≃ₐ[R] A₁), (MulSemiringAction.toRingEquiv (A₁ ≃ₐ[R] A₁) A₁) σ = σ.toRingEquiv
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem!_toArray_rcc_eq_add : ∀ {m n : ℤ} {i : ℕ}, i < (n + 1 - m).toNat → (m...=n).toArray[i]! = m + ↑i
-- Lean.Elab.PatternVar
_private.Lean.Elab.PatternVar.0.Lean.Elab.Term.CollectPatternVars.collect.processCtorAppContext : Lean.Elab.Term.CollectPatternVars.Context → Lean.Elab.Term.CollectPatternVars.M Lean.Syntax
-- Mathlib.Analysis.MellinTransform
mellin_div_const : ∀ (f : ℝ → ℂ) (s a : ℂ), mellin (fun t => f t / a) s = mellin f s / a
-- Lean.Parser.Types
Lean.Parser.ParserState.setCache : Lean.Parser.ParserState → Lean.Parser.ParserCache → Lean.Parser.ParserState
-- Mathlib.NumberTheory.Bernoulli
/-- **Faulhaber's theorem** relating the **sum of p-th powers** to the Bernoulli numbers:
$$\sum_{k=0}^{n-1} k^p = \sum_{i=0}^p B_i\binom{p+1}{i}\frac{n^{p+1-i}}{p+1}.$$
See https://proofwiki.org/wiki/Faulhaber%27s_Formula and [orosi2018faulhaber] for
the proof provided here.  -/
sum_range_pow : ∀ (n p : ℕ),
  ∑ k ∈ Finset.range n, ↑k ^ p =
    ∑ i ∈ Finset.range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / (↑p + 1)
-- Init.Data.UInt.Lemmas
UInt32.toUInt16_ofNatClamp_of_le : ∀ {n : ℕ},
  UInt32.size ≤ n →
    (UInt32.ofNatClamp n).toUInt16 = UInt16.ofNatLT (UInt16.size - 1) UInt32.toUInt16_ofNatClamp_of_le._proof_1
-- Mathlib.Geometry.Euclidean.Triangle
/-- **Converse of pons asinorum**, oriented vector angle form (given equality of angles mod `π`).  -/
Orientation.norm_eq_of_two_zsmul_oangle_sub_eq : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V},
  2 • o.oangle x (x - y) = 2 • o.oangle (y - x) y → o.oangle x y ≠ 0 → o.oangle x y ≠ ↑Real.pi → ‖x‖ = ‖y‖
-- Mathlib.RingTheory.TotallySplit
Algebra.IsFiniteSplit.of_subsingleton_top : ∀ {R : Type u_2} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Subsingleton S],
  Algebra.IsFiniteSplit R S
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
CoassocSimps.symm_comp_lid_symm : ∀ {R : Type u_1} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  ↑(TensorProduct.comm R R M) ∘ₗ ↑(TensorProduct.lid R M).symm = ↑(TensorProduct.rid R M).symm
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.CoeExpansionTrace : Type
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.map_mk : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] {𝒜 : ι → σ}
  [inst_5 : GradedRing 𝒜] {B : Type u_4} {τ : Type u_5} [inst_6 : CommRing B] [inst_7 : SetLike τ B]
  [inst_8 : AddSubgroupClass τ B] {ℬ : ι → τ} [inst_9 : GradedRing ℬ] {P : Submonoid A} {Q : Submonoid B} (g : 𝒜 →+*ᵍ ℬ)
  (comap_le : P ≤ Submonoid.comap g Q) (x : HomogeneousLocalization.NumDenSameDeg 𝒜 P),
  (HomogeneousLocalization.map g comap_le) (HomogeneousLocalization.mk x) =
    HomogeneousLocalization.mk { deg := x.deg, num := ⟨g ↑x.num, ⋯⟩, den := ⟨g ↑x.den, ⋯⟩, den_mem := ⋯ }
-- Init.Data.Array.MapIdx
/-- Variant of `mk_mem_zipIdx_iff_le_and_getElem?_sub` specialized at `k = 0`,
to avoid the inequality and the subtraction.  -/
Array.mk_mem_zipIdx_iff_getElem? : ∀ {α : Type u_1} {x : α} {i : ℕ} {xs : Array α}, (x, i) ∈ xs.zipIdx ↔ xs[i]? = some x
-- Mathlib.CategoryTheory.Limits.Presentation
CategoryTheory.Limits.ColimitPresentation.map_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.Category.{t, w} J]
  {X : C} (P : CategoryTheory.Limits.ColimitPresentation J X) {D : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} D] (F : CategoryTheory.Functor C D)
  [inst_3 : CategoryTheory.Limits.PreservesColimitsOfShape J F],
  (P.map F).ι =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight P.ι F)
      (CategoryTheory.Functor.constComp J X F).hom
-- Mathlib.Algebra.BigOperators.Finprod
finsum_zero : ∀ {M : Type u_2} {α : Sort u_4} [inst : AddCommMonoid M], ∑ᶠ (x : α), 0 = 0
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.getEMatchTheoremNumInstances : Lean.Meta.Grind.EMatchTheorem → Lean.Meta.Grind.GrindM ℕ
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.a₂_of_isShortNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsShortNF], W.a₂ = 0
-- Init.Data.Vector.Attach
Vector.back?_attach : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n}, xs.attach.back? = xs.back?.pbind fun a h => some ⟨a, ⋯⟩
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.isSome_minKey?_modify_eq_isSome : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : β → β}, (t.modify k f).minKey?.isSome = t.minKey?.isSome
-- Mathlib.Algebra.ContinuedFractions.Basic
GenContFract.Pair.mk.sizeOf_spec : ∀ {α : Type u_1} [inst : SizeOf α] (a b : α), sizeOf { a := a, b := b } = 1 + sizeOf a + sizeOf b
-- Lean.Meta.Sym.Arith.Poly
_private.Lean.Meta.Sym.Arith.Poly.0.Lean.Grind.CommRing.Mon.sharesVar.match_3.eq_1 : ∀ (motive : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Sort u_1) (x : Lean.Grind.CommRing.Mon)
  (h_1 : (x : Lean.Grind.CommRing.Mon) → motive Lean.Grind.CommRing.Mon.unit x)
  (h_2 : (x : Lean.Grind.CommRing.Mon) → motive x Lean.Grind.CommRing.Mon.unit)
  (h_3 :
    (pw₁ : Lean.Grind.CommRing.Power) →
      (m₁ : Lean.Grind.CommRing.Mon) →
        (pw₂ : Lean.Grind.CommRing.Power) →
          (m₂ : Lean.Grind.CommRing.Mon) →
            motive (Lean.Grind.CommRing.Mon.mult pw₁ m₁) (Lean.Grind.CommRing.Mon.mult pw₂ m₂)),
  (match Lean.Grind.CommRing.Mon.unit, x with
    | Lean.Grind.CommRing.Mon.unit, x => h_1 x
    | x, Lean.Grind.CommRing.Mon.unit => h_2 x
    | Lean.Grind.CommRing.Mon.mult pw₁ m₁, Lean.Grind.CommRing.Mon.mult pw₂ m₂ => h_3 pw₁ m₁ pw₂ m₂) =
    h_1 x
-- Init.Data.Vector.Lemmas
Vector.mem_dite_empty_left : ∀ {α : Type u_1} {p : Prop} {x : α} [inst : Decidable p] {xs : ¬p → Vector α 0},
  (x ∈ if h : p then #v[] else xs h) ↔ ∃ (h : ¬p), x ∈ xs h
-- Mathlib.Analysis.Normed.Operator.Compact.Basic
isCompactOperator_of_tendsto : ∀ {ι : Type u_1} {𝕜₁ : Type u_2} {𝕜₂ : Type u_3} [inst : NontriviallyNormedField 𝕜₁] [inst_1 : NormedField 𝕜₂]
  {σ₁₂ : 𝕜₁ →+* 𝕜₂} {M₁ : Type u_4} {M₂ : Type u_5} [inst_2 : SeminormedAddCommGroup M₁] [inst_3 : AddCommGroup M₂]
  [inst_4 : NormedSpace 𝕜₁ M₁] [inst_5 : Module 𝕜₂ M₂] [inst_6 : UniformSpace M₂] [inst_7 : IsUniformAddGroup M₂]
  [ContinuousConstSMul 𝕜₂ M₂] [T2Space M₂] [CompleteSpace M₂] {l : Filter ι} [l.NeBot] {F : ι → M₁ →SL[σ₁₂] M₂}
  {f : M₁ →SL[σ₁₂] M₂}, Filter.Tendsto F l (nhds f) → (∀ᶠ (i : ι) in l, IsCompactOperator ⇑(F i)) → IsCompactOperator ⇑f
-- Mathlib.Order.Filter.AtTopBot.CountablyGenerated
/-- An abstract version of continuity of sequentially continuous functions on metric spaces:
if a filter `k` is countably generated then `Tendsto f k l` iff for every sequence `u`
converging to `k`, `f ∘ u` tends to `l`.  -/
Filter.tendsto_iff_seq_tendsto : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {k : Filter α} {l : Filter β} [k.IsCountablyGenerated],
  Filter.Tendsto f k l ↔ ∀ (x : ℕ → α), Filter.Tendsto x Filter.atTop k → Filter.Tendsto (f ∘ x) Filter.atTop l
-- Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
/-- **Alias** of `AlgebraicGeometry.IsPreimmersion.isEmbedding`. -/
AlgebraicGeometry.Scheme.Hom.isEmbedding : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [self : AlgebraicGeometry.IsPreimmersion f], Topology.IsEmbedding ⇑f
-- Mathlib.Algebra.Homology.QuasiIso
HomologicalComplex.quasiIso_map_iff_of_preservesHomology : ∀ {ι : Type u_1} {c : ComplexShape ι} {C₁ : Type u_2} {C₂ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_2} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} C₂] [inst_2 : CategoryTheory.Preadditive C₁]
  [inst_3 : CategoryTheory.Preadditive C₂] {K L : HomologicalComplex C₁ c} (φ : K ⟶ L)
  (F : CategoryTheory.Functor C₁ C₂) [inst_4 : F.Additive] [F.PreservesHomology] [inst_6 : ∀ (i : ι), K.HasHomology i]
  [inst_7 : ∀ (i : ι), L.HasHomology i] [inst_8 : ∀ (i : ι), ((F.mapHomologicalComplex c).obj K).HasHomology i]
  [inst_9 : ∀ (i : ι), ((F.mapHomologicalComplex c).obj L).HasHomology i] [F.ReflectsIsomorphisms],
  QuasiIso ((F.mapHomologicalComplex c).map φ) ↔ QuasiIso φ
-- Mathlib.Data.Multiset.Powerset
Multiset.card_powersetCard : ∀ {α : Type u_1} (n : ℕ) (s : Multiset α), (Multiset.powersetCard n s).card = s.card.choose n
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.Monic.add_of_lt : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f g : MvPolynomial σ R},
  m.Monic f → m.toSyn (m.degree g) < m.toSyn (m.degree f) → m.Monic (f + g)
-- Mathlib.CategoryTheory.Bicategory.EqToHom
/-- In a bicategory, `eqToHom`s do not compose strictly,
but they do up to isomorphism.  -/
CategoryTheory.Bicategory.eqToHomTransIso : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {x y z : B} →
      (e₁ : x = y) →
        (e₂ : y = z) →
          CategoryTheory.eqToHom ⋯ ≅
            CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom e₁) (CategoryTheory.eqToHom e₂)
-- Lean.Meta.MatchUtil
Lean.Meta.matchConstructorApp? : Lean.Expr → Lean.MetaM (Option Lean.ConstructorVal)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKey?_erase_le_maxKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  (h : t.WF) {k km kme : α} (hkme : (t.erase k).maxKey? = some kme), t.maxKey?.get ⋯ = km → (cmp kme km).isLE = true
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- In a preadditive category, if all binary coproducts exist, then all binary biproducts exist.  -/
CategoryTheory.Limits.HasBinaryBiproducts.of_hasBinaryCoproducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [CategoryTheory.Limits.HasBinaryCoproducts C], CategoryTheory.Limits.HasBinaryBiproducts C
-- Mathlib.Topology.Order.ScottTopology
Topology.IsScott.mk : ∀ {α : Type u_1} {D : Set (Set α)} [inst : Preorder α] [inst_1 : TopologicalSpace α],
  inst_1 = Topology.scott α D → Topology.IsScott α D
-- Mathlib.RingTheory.Ideal.Quotient.PowTransition
Submodule.mapQ_eq_factor : ∀ {R : Type u_1} [inst : Ring R] {I J : Ideal R} (h : I ≤ J) (x : R ⧸ I),
  (Submodule.mapQ I J LinearMap.id h) x = (Submodule.factor h) x
-- Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence
/-- The unit isomorphism of the equivalence
`ShortComplex.functorEquivalence : ShortComplex (J ⥤ C) ≌ J ⥤ ShortComplex C`.  -/
CategoryTheory.ShortComplex.FunctorEquivalence.unitIso : (J : Type u_1) →
  (C : Type u_2) →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          CategoryTheory.Functor.id (CategoryTheory.ShortComplex (CategoryTheory.Functor J C)) ≅
            (CategoryTheory.ShortComplex.FunctorEquivalence.functor J C).comp
              (CategoryTheory.ShortComplex.FunctorEquivalence.inverse J C)
-- Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Asymptotics.superpolynomialDecay_mul_param_iff : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {k : α → β} (f : α → β) [inst : TopologicalSpace β] [inst_1 : Field β]
  [inst_2 : LinearOrder β] [IsStrictOrderedRing β] [OrderTopology β],
  Filter.Tendsto k l Filter.atTop →
    (Asymptotics.SuperpolynomialDecay l k (f * k) ↔ Asymptotics.SuperpolynomialDecay l k f)
-- Lean.Meta.Closure
_private.Lean.Meta.Closure.0.Lean.Meta.Closure.TopoSort.doneMark : Lean.Meta.Closure.TopoSort✝ → Lean.FVarIdHashSet
-- Mathlib.Combinatorics.Colex
/-- **Alias** of `Finset.sum_toFinset_bitIndices_two_pow`. -/
Finset.twoPowSum_toFinset_bitIndices : ∀ (n : ℕ), ∑ i ∈ n.bitIndices.toFinset, 2 ^ i = n
-- Init.Data.Ord.String
/-- Lexicographic comparison of strings
 -/
String.compare : String → String → Ordering
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.instIsTopologicalRingCoePrincipal : ∀ {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i}
  {T : Set ι} [inst_1 : (i : ι) → TopologicalSpace (R i)] [inst_2 : (i : ι) → Ring (R i)]
  [inst_3 : ∀ (i : ι), SubringClass (S i) (R i)] [∀ (i : ι), IsTopologicalRing (R i)],
  IsTopologicalRing (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) (Filter.principal T))
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.fundamentalSequence.match_1.eq_4 : ∀ (motive : Option ONote ⊕ (ℕ → ONote) → ℕ → Sort u_1) (a' : ONote) (m : ℕ) (h_1 : Unit → motive (Sum.inl none) 0)
  (h_2 : (m : ℕ) → motive (Sum.inl none) m.succ) (h_3 : (a' : ONote) → motive (Sum.inl (some a')) 0)
  (h_4 : (a' : ONote) → (m : ℕ) → motive (Sum.inl (some a')) m.succ) (h_5 : (f : ℕ → ONote) → motive (Sum.inr f) 0)
  (h_6 : (f : ℕ → ONote) → (m : ℕ) → motive (Sum.inr f) m.succ),
  (match Sum.inl (some a'), m.succ with
    | Sum.inl none, 0 => h_1 ()
    | Sum.inl none, m.succ => h_2 m
    | Sum.inl (some a'), 0 => h_3 a'
    | Sum.inl (some a'), m.succ => h_4 a' m
    | Sum.inr f, 0 => h_5 f
    | Sum.inr f, m.succ => h_6 f m) =
    h_4 a' m
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.map_surjective_of_surjective : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] (N : AddSubgroup G) [nN : N.Normal]
  (M : AddSubgroup H) [inst_2 : M.Normal] (f : G →+ H),
  Function.Surjective (QuotientAddGroup.mk ∘ ⇑f) →
    ∀ (h : N ≤ AddSubgroup.comap f M), Function.Surjective ⇑(QuotientAddGroup.map N M f h)
-- Mathlib.LinearAlgebra.QuadraticForm.Radical
/-- If `2` is invertible in the coefficient ring,
the radical of a quadratic map is the kernel of its polar bilinear map.  -/
QuadraticMap.radical_eq_ker_polarBilin : ∀ {R : Type u_1} {M : Type u_2} {P : Type u_4} [inst : AddCommGroup M] [inst_1 : AddCommGroup P] [inst_2 : CommRing R]
  [inst_3 : Module R M] [inst_4 : Module R P] {Q : QuadraticMap R M P} [Invertible 2],
  Q.radical = LinearMap.ker Q.polarBilin
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.curryAddEquiv.eq_1 : ∀ {R : Type u_1} {M : Type u_4} {N : Type u_5} [inst : Semiring R] [inst_1 : Monoid M] [inst_2 : Monoid N],
  MonoidAlgebra.curryAddEquiv =
    MonoidAlgebra.coeffAddEquiv.trans
      (Finsupp.curryAddEquiv.trans
        ((Finsupp.mapRange.addEquiv MonoidAlgebra.coeffAddEquiv.symm).trans MonoidAlgebra.coeffAddEquiv.symm))
-- Mathlib.Data.Rat.Lemmas
Rat.intCast_div_self : ∀ (n : ℤ), ↑(n / n) = ↑n / ↑n
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.instHasPullbackMapF : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] {C' : Type u₂} [inst_1 : CategoryTheory.Category.{v, u₂} C']
  (D : CategoryTheory.GlueData C) (F : CategoryTheory.Functor C C')
  [∀ (i j k : D.J), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F]
  (i j k : D.J), CategoryTheory.Limits.HasPullback (F.map (D.f i j)) (F.map (D.f i k))
-- Lean.Meta.Sym.SymM
_private.Lean.Meta.Sym.SymM.0.Lean.Meta.Sym.SymExtension.modifyStateImpl : {σ : Type} → Lean.Meta.Sym.SymExtension σ → (σ → σ) → Lean.Meta.Sym.SymM Unit
-- Mathlib.Analysis.Convex.Function
OrderIso.convexOn_symm : ∀ {𝕜 : Type u_1} {α : Type u_4} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid α]
  [inst_3 : PartialOrder α] [inst_4 : SMul 𝕜 α] [inst_5 : AddCommMonoid β] [inst_6 : PartialOrder β] [inst_7 : SMul 𝕜 β]
  (f : α ≃o β), ConcaveOn 𝕜 Set.univ ⇑f → ConvexOn 𝕜 Set.univ ⇑f.symm
-- Mathlib.Data.Matrix.ColumnRowPartitioned
Matrix.fromCols_zero : ∀ {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} [inst : Semiring R], Matrix.fromCols 0 0 = 0
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
IsPrimitiveRoot.adjoinEquivRingOfIntegersOfPrimePow_symm_apply : ∀ {p k : ℕ} {K : Type u} [inst : Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [inst_1 : CharZero K]
  [inst_2 : IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ k)) (a : NumberField.RingOfIntegers K),
  hζ.adjoinEquivRingOfIntegersOfPrimePow.symm a = (IsIntegralClosure.lift ℤ (↥ℤ[ζ]) K) a
-- Mathlib.CategoryTheory.Presentable.SharplyLT.Basic
/-- The subset of `X` given by the union over all `C : Y B hB` of
`C` and `{m B hB C _}`.  -/
_private.Mathlib.CategoryTheory.Presentable.SharplyLT.Basic.0.Cardinal.SharplyLT.existsIsCardinalFilteredSetOfExistsCofinal.φ₀ : {κ₁ κ₂ : Cardinal.{w}} →
  {X : Type w} →
    (Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (CategoryTheory.CardinalDirectedPoset.SetCardinalLT κ₁ ↑B)) →
      ((B : Set X) →
          (hB : HasCardinalLT (↑B) κ₂) →
            (C : CategoryTheory.CardinalDirectedPoset.SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X) →
        (B : Set X) → HasCardinalLT (↑B) κ₂ → Set X
-- Init.Data.Vector.Lemmas
Vector.foldlM_toArray : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {n : ℕ} [inst : Monad m] {f : β → α → m β} {init : β}
  {xs : Vector α n}, Array.foldlM f init xs.toArray = Vector.foldlM f init xs
-- Mathlib.Algebra.Ring.Defs
CommSemiring.mk : {R : Type u} → [toSemiring : Semiring R] → (∀ (a b : R), a * b = b * a) → CommSemiring R
-- Mathlib.RingTheory.KrullDimension.Basic
Ring.KrullDimLE.mk₁ : ∀ {R : Type u_1} [inst : CommSemiring R],
  (∀ (I : Ideal R), I.IsPrime → I ∈ minimalPrimes R ∨ I.IsMaximal) → Ring.KrullDimLE 1 R
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
CategoryTheory.EffectiveEpiStruct.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} {f : Y ⟶ X}
  (desc :
    {W : C} →
      (e : Y ⟶ W) →
        (∀ {Z : C} (g₁ g₂ : Z ⟶ Y),
            CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f →
              CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e) →
          (X ⟶ W))
  (fac :
    ∀ {W : C} (e : Y ⟶ W)
      (h :
        ∀ {Z : C} (g₁ g₂ : Z ⟶ Y),
          CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f →
            CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e),
      CategoryTheory.CategoryStruct.comp f (desc e ⋯) = e)
  (uniq :
    ∀ {W : C} (e : Y ⟶ W)
      (h :
        ∀ {Z : C} (g₁ g₂ : Z ⟶ Y),
          CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f →
            CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e)
      (m : X ⟶ W), CategoryTheory.CategoryStruct.comp f m = e → m = desc e ⋯)
  (desc_1 :
    {W : C} →
      (e : Y ⟶ W) →
        (∀ {Z : C} (g₁ g₂ : Z ⟶ Y),
            CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f →
              CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e) →
          (X ⟶ W))
  (fac_1 :
    ∀ {W : C} (e : Y ⟶ W)
      (h :
        ∀ {Z : C} (g₁ g₂ : Z ⟶ Y),
          CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f →
            CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e),
      CategoryTheory.CategoryStruct.comp f (desc_1 e ⋯) = e)
  (uniq_1 :
    ∀ {W : C} (e : Y ⟶ W)
      (h :
        ∀ {Z : C} (g₁ g₂ : Z ⟶ Y),
          CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f →
            CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e)
      (m : X ⟶ W), CategoryTheory.CategoryStruct.comp f m = e → m = desc_1 e ⋯),
  ({ desc := desc, fac := fac, uniq := uniq } = { desc := desc_1, fac := fac_1, uniq := uniq_1 }) = (desc = desc_1)
-- Mathlib.Topology.Algebra.MulAction
Prod.continuousSMul : ∀ {M : Type u_1} {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace Y] [inst_3 : SMul M X] [inst_4 : SMul M Y] [ContinuousSMul M X] [ContinuousSMul M Y],
  ContinuousSMul M (X × Y)
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.norm_integral_le_integral_norm : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {f : X → E} {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G},
  ‖∫ᵛ (a : X), f a ∂[B; μ]‖ ≤ ‖B‖ * ∫ (a : X), ‖f a‖ ∂μ.variation
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Contravariant.flip : ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop}, Contravariant M N μ r → Contravariant M N μ (flip r)