mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.toProd_comp_inl : ∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : AddMonoid N],
  AddMonoid.Coprod.toProd.comp AddMonoid.Coprod.inl = AddMonoidHom.inl M N
-- Mathlib.Lean.Thunk
Thunk.get_pure : ∀ {α : Type u_1} (x : α), (Thunk.pure x).get = x
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
/-- The (unique) isomorphism between any initial object and the zero object.  -/
CategoryTheory.Limits.IsZero.isoIsInitial : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → CategoryTheory.Limits.IsZero X → CategoryTheory.Limits.IsInitial Y → (X ≅ Y)
-- Init.Data.Fin.Lemmas
Fin.val_pred : ∀ {n : ℕ} (j : Fin (n + 1)) (h : j ≠ 0), ↑(j.pred h) = ↑j - 1
-- Mathlib.Topology.Connected.TotallyDisconnected
Subtype.totallyDisconnectedSpace : ∀ {α : Type u_3} {p : α → Prop} [inst : TopologicalSpace α] [TotallyDisconnectedSpace α],
  TotallyDisconnectedSpace (Subtype p)
-- Init.GrindInstances.ToInt
Lean.Grind.instAddFinCoOfNatIntCast : ∀ {n : ℕ}, Lean.Grind.ToInt.Add (Fin n) (Lean.Grind.IntInterval.co 0 ↑n)
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.le_weightedOrder_prod : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] {ι : Type u_4} (w : σ → ℕ) (f : ι → MvPowerSeries σ R)
  (s : Finset ι), ∑ i ∈ s, MvPowerSeries.weightedOrder w (f i) ≤ MvPowerSeries.weightedOrder w (∏ i ∈ s, f i)
-- Mathlib.LinearAlgebra.FreeModule.Finite.Quotient
/-- Decompose `M⧸N` as a direct sum of cyclic `R`-modules
(quotients by the ideals generated by Smith coefficients of `N`).  -/
Submodule.quotientEquivDirectSum : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            [inst_3 : IsDomain R] →
              [inst_4 : IsPrincipalIdealRing R] →
                [inst_5 : Finite ι] →
                  (F : Type u_4) →
                    [inst_6 : CommRing F] →
                      [inst_7 : Algebra F R] →
                        [inst_8 : Module F M] →
                          [inst_9 : IsScalarTower F R M] →
                            (b : Module.Basis ι R M) →
                              {N : Submodule R M} →
                                (h : Module.finrank R ↥N = Module.finrank R M) →
                                  (M ⧸ N) ≃ₗ[F]
                                    DirectSum ι fun i => R ⧸ Ideal.span {Submodule.smithNormalFormCoeffs b h i}
-- Mathlib.Analysis.Calculus.ContDiff.Comp
ContDiff.comp₂_contDiffWithinAt : ∀ {𝕜 : Type u_1} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] {n : WithTop ℕ∞} {E₁ : Type u_6}
  {E₂ : Type u_7} [inst_5 : NormedAddCommGroup E₁] [inst_6 : NormedAddCommGroup E₂] [inst_7 : NormedSpace 𝕜 E₁]
  [inst_8 : NormedSpace 𝕜 E₂] {g : E₁ × E₂ → G} {f₁ : F → E₁} {f₂ : F → E₂} {s : Set F} {x : F},
  ContDiff 𝕜 n g →
    ContDiffWithinAt 𝕜 n f₁ s x → ContDiffWithinAt 𝕜 n f₂ s x → ContDiffWithinAt 𝕜 n (fun x => g (f₁ x, f₂ x)) s x
-- Init.Data.UInt.Lemmas
UInt32.ofNat_sub : ∀ {a b : ℕ}, b ≤ a → UInt32.ofNat (a - b) = UInt32.ofNat a - UInt32.ofNat b
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.Quotient.factorₐ_comp_mk : ∀ (R₁ : Type u_1) {A : Type u_3} [inst : CommSemiring R₁] [inst_1 : Ring A] [inst_2 : Algebra R₁ A] {I J : Ideal A}
  [inst_3 : I.IsTwoSided] [inst_4 : J.IsTwoSided] (hIJ : I ≤ J),
  (Ideal.Quotient.factorₐ R₁ hIJ).comp (Ideal.Quotient.mkₐ R₁ I) = Ideal.Quotient.mkₐ R₁ J
-- Init.Data.UInt.BasicAux
UInt8.instOfNat : {n : ℕ} → OfNat UInt8 n
-- Lean.Data.Lsp.BasicAux
Lean.Lsp.instReprPosition.repr : Lean.Lsp.Position → ℕ → Std.Format
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
IsDiscreteValuationRing.addVal_eq_zero_of_unit : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] (u : Rˣ),
  (IsDiscreteValuationRing.addVal R) ↑u = 0
-- Mathlib.CategoryTheory.Core
CategoryTheory.CoreHom.ext_iff : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {X Y : CategoryTheory.Core C}
  {x y : CategoryTheory.CoreHom X Y}, x = y ↔ x.iso = y.iso
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
mdifferentiable_smul_const_section : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : TopologicalSpace B]
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : (x : B) → TopologicalSpace (E x)]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : FiberBundle F E] [inst_7 : (x : B) → AddCommGroup (E x)] [inst_8 : (x : B) → Module 𝕜 (E x)]
  [VectorBundle 𝕜 F E] {HB : Type u_7} [inst_10 : TopologicalSpace HB] [inst_11 : ChartedSpace HB B] {EB : Type u_8}
  [inst_12 : NormedAddCommGroup EB] [inst_13 : NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {a : 𝕜}
  {s : (x : B) → E x}, MDiff (T% s) → MDiff fun x => ⟨x, (a • s) x⟩
-- Mathlib.Data.Finsupp.Basic
/-- Given an `AddCommMonoid M` and `s : Set α`, `restrictSupportEquiv s M` is the `Equiv`
between the subtype of finitely supported functions with support contained in `s` and
the type of finitely supported functions from `s`.  -/
Finsupp.restrictSupportEquiv : {α : Type u_1} → (s : Set α) → (M : Type u_12) → [inst : AddCommMonoid M] → { f // ↑f.support ⊆ s } ≃ (↑s →₀ M)
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonLeanImport.fromJson : Lean.Json → Except String Lean.Lsp.LeanImport
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctorAssociatorX.congr_simp : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_3} C₁₂] [inst_5 : CategoryTheory.Category.{v_6, u_4} C₂₃]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_8 : CategoryTheory.Limits.HasZeroMorphisms C₃] [inst_9 : CategoryTheory.Preadditive C₁₂]
  [inst_10 : CategoryTheory.Preadditive C₂₃] [inst_11 : CategoryTheory.Preadditive C₄]
  {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)}
  {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)}
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)}
  {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} [inst_12 : F₁₂.PreservesZeroMorphisms]
  [inst_13 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [inst_14 : G.Additive]
  [inst_15 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] [inst_16 : G₂₃.PreservesZeroMorphisms]
  [inst_17 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [inst_18 : F.PreservesZeroMorphisms]
  [inst_19 : ∀ (X₁ : C₁), (F.obj X₁).Additive]
  (associator associator_1 : CategoryTheory.bifunctorComp₁₂ F₁₂ G ≅ CategoryTheory.bifunctorComp₂₃ F G₂₃),
  associator = associator_1 →
    ∀ {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12}
      [inst_20 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃}
      (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃)
      (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [inst_21 : TotalComplexShape c₁ c₂ c₁₂]
      [inst_22 : TotalComplexShape c₁₂ c₃ c₄] [inst_23 : TotalComplexShape c₂ c₃ c₂₃], ⋯
-- Init.Data.Fin.Lemmas
Fin.addNat_last : ∀ {m : ℕ} (n : ℕ), (Fin.last n).addNat m = Fin.cast ⋯ (Fin.last (n + m))
-- Mathlib.RingTheory.Derivation.ToSquareZero
derivationToSquareZeroEquivLift_symm_apply_apply_coe : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (I : Ideal B) [inst_5 : Algebra A B] (hI : I ^ 2 = ⊥)
  [inst_6 : IsScalarTower R A B] (f : { f // (Ideal.Quotient.mkₐ R I).comp f = IsScalarTower.toAlgHom R A (B ⧸ I) })
  (c : A), ↑(((derivationToSquareZeroEquivLift I hI).symm f) c) = ↑f c - (algebraMap A B) c
-- Mathlib.Logic.Equiv.Prod
/-- Type product is associative up to an equivalence.  -/
Equiv.prodAssoc : (α : Type u_9) → (β : Type u_10) → (γ : Type u_11) → (α × β) × γ ≃ α × β × γ
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.equivSMul_symm_apply_coe : ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : Group α] [inst_2 : MulDistribMulAction α G] (a : α)
  (H : Subgroup G) (y : ↑(⇑↑(MulDistribMulAction.toMulEquiv G a) '' ↑H.toSubmonoid)),
  ↑((Subgroup.equivSMul a H).symm y) = a⁻¹ • ↑y
-- Mathlib.GroupTheory.GroupAction.Basic
MulAction.stabilizerEquivStabilizer_one : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {a : α},
  MulAction.stabilizerEquivStabilizer ⋯ = MulEquiv.refl ↥(MulAction.stabilizer G a)
-- Mathlib.Data.Multiset.Replicate
Multiset.eq_of_mem_replicate : ∀ {α : Type u_1} {a b : α} {n : ℕ}, b ∈ Multiset.replicate n a → b = a
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Pi.equivalenceOfEquiv_counitIso : ∀ {I : Type w₀} {J : Type w₁} (C : I → Type u₁) [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] (e : J ≃ I),
  (CategoryTheory.Pi.equivalenceOfEquiv C e).counitIso =
    CategoryTheory.NatIso.pi' fun i =>
      ((CategoryTheory.Functor.pi' fun i' => CategoryTheory.Pi.eval C (e i')).associator
            (CategoryTheory.Pi.eval (fun j => C (e j)) (e.symm i))
            (CategoryTheory.Pi.eqToEquivalence C ⋯).functor).symm ≪≫
        CategoryTheory.Functor.isoWhiskerRight
            (CategoryTheory.Functor.pi'CompEval (fun i' => CategoryTheory.Pi.eval C (e i')) (e.symm i))
            (CategoryTheory.Pi.eqToEquivalence C ⋯).functor ≪≫
          CategoryTheory.Pi.evalCompEqToEquivalenceFunctor C ⋯ ≪≫ (CategoryTheory.Pi.eval C i).leftUnitor.symm
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Finsupp.singleAddHom.eq_1 : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddZeroClass M] (a : ι),
  Finsupp.singleAddHom a = { toFun := Finsupp.single a, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.isBigOWith : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F} {l : Filter α},
  f =O[l] g → ∃ c, Asymptotics.IsBigOWith c l f g
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
/-- The forgetful functor from the under category preserves any connected limit.  -/
CategoryTheory.Under.preservesColimitsOfShape_forget_of_isConnected : ∀ {J : Type u'} [inst : CategoryTheory.Category.{v', u'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [CategoryTheory.IsConnected J] {B : C},
  CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.Under.forget B)
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.IsBasis.eq_exchange_of_sdiff_eq_singleton : ∀ {α : Type u_1} {M : Matroid α} {I X J : Set α} {e : α},
  M.IsBasis I X → M.IsBasis J X → I \ J = {e} → ∃ f ∈ J \ I, J = insert f I \ {e}
-- Mathlib.Data.ENat.Basic
ENat.eq_top_iff_forall_ne : ∀ {n : ℕ∞}, n = ⊤ ↔ ∀ (m : ℕ), ↑m ≠ n
-- Lean.Parser.Basic
Lean.Parser.unicodeSymbolFnAux : String → String → List String → Lean.Parser.ParserFn
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.tr_respects_aux₃ : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [inst : DecidableEq K] (M : Λ → Turing.TM2.Stmt Γ Λ σ)
  {q : Turing.TM2.Stmt Γ Λ σ} {v : σ} {L : Turing.ListBlank ((k : K) → Option (Γ k))} (n : ℕ),
  StateTransition.Reaches₀ (Turing.TM1.step (Turing.TM2to1.tr M))
    { l := some (Turing.TM2to1.Λ'.ret q), var := v,
      Tape := (Turing.Tape.move Turing.Dir.right)^[n] (Turing.Tape.mk' ∅ (Turing.TM2to1.addBottom L)) }
    { l := some (Turing.TM2to1.Λ'.ret q), var := v, Tape := Turing.Tape.mk' ∅ (Turing.TM2to1.addBottom L) }
-- Mathlib.RingTheory.Ideal.Operations
Ideal.subset_iUnion_iff_mem_of_isMaximal_of_finite : ∀ {R : Type u_2} [inst : CommRing R] {M : Ideal R} [M.IsMaximal] {S : Set (Ideal R)},
  S.Finite → ∀ (a b : Ideal R), (∀ I ∈ S, I ≠ a → I ≠ b → I.IsPrime) → a ≠ ⊤ → b ≠ ⊤ → (↑M ⊆ ⋃ I ∈ S, ↑I ↔ M ∈ S)
-- Mathlib.Order.Filter.Bases.Finite
Filter.generate_neBot_iff : ∀ {α : Type u_1} {s : Set (Set α)}, (Filter.generate s).NeBot ↔ ∀ t ⊆ s, t.Finite → (⋂₀ t).Nonempty
-- Mathlib.Order.Filter.Finite
Filter.biInter_mem : ∀ {α : Type u} {f : Filter α} {β : Type v} {s : β → Set α} {is : Set β},
  is.Finite → (⋂ i ∈ is, s i ∈ f ↔ ∀ i ∈ is, s i ∈ f)
-- Mathlib.Algebra.Module.LocalizedModule.Int
/-- We can clear the denominators of a finite set of fractions.  -/
IsLocalizedModule.exist_integer_multiples_of_finset : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] {M' : Type u_3} [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  [IsLocalizedModule S f] (s : Finset M'), ∃ b, ∀ a ∈ s, IsLocalizedModule.IsInteger f (↑b • a)
-- Mathlib.Algebra.Colimit.Ring
/-- Consider direct limits `lim G` and `lim G'` with direct system `f` and `f'` respectively, any
family of equivalences `eᵢ : Gᵢ ≅ G'ᵢ` such that `e ∘ f = f' ∘ e` induces an equivalence
`lim G ⟶ lim G'`.
 -/
Ring.DirectLimit.congr : {ι : Type u_1} →
  [inst : Preorder ι] →
    {G : ι → Type u_2} →
      [inst_1 : (i : ι) → CommRing (G i)] →
        {f : (i j : ι) → i ≤ j → G i →+* G j} →
          {G' : ι → Type u_4} →
            [inst_2 : (i : ι) → CommRing (G' i)] →
              {f' : (i j : ι) → i ≤ j → G' i →+* G' j} →
                (e : (i : ι) → G i ≃+* G' i) →
                  (∀ (i j : ι) (h : i ≤ j), (e j).toRingHom.comp (f i j h) = (f' i j h).comp ↑(e i)) →
                    (Ring.DirectLimit G fun x x_1 h => ⇑(f x x_1 h)) ≃+*
                      Ring.DirectLimit G' fun x x_1 h => ⇑(f' x x_1 h)
-- Mathlib.Topology.Homotopy.TopCat.Path
TopCat.Path.mk : {X : TopCat} →
  {x y : ↑X} →
    (hom : TopCat.I ⟶ X) →
      autoParam ((CategoryTheory.ConcreteCategory.hom hom) 0 = x) TopCat.Path.hom₀._autoParam →
        autoParam ((CategoryTheory.ConcreteCategory.hom hom) 1 = y) TopCat.Path.hom₁._autoParam → X.Path x y
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.norm.eq_1 : ∀ (p : Nat.Internal.Linear.Poly), p.norm = Nat.Internal.Linear.Poly.norm.go p []
-- Std.Time.Format
/-- Parses a time string in the 12-hour format (`hh:mm:ss aa`) and returns a `PlainTime`.
 -/
Std.Time.PlainTime.fromTime12Hour : String → Except String Std.Time.PlainTime
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
_private.Init.Data.String.Lemmas.Pattern.String.ForwardPattern.0.String.Slice.takeEndWhile.eq_1 : ∀ {ρ : Type} (s : String.Slice) (pat : ρ) [inst : String.Slice.Pattern.BackwardPattern pat],
  s.takeEndWhile pat = s.sliceFrom (s.skipSuffixWhile pat)
-- Lean.Elab.Term.TermElabM
/-- Execute `x` without storing `Syntax` for recursive applications. See `saveRecAppSyntax` field at `Context`.
 -/
Lean.Elab.Term.withoutSavingRecAppSyntax : {α : Type} → Lean.Elab.TermElabM α → Lean.Elab.TermElabM α
-- Mathlib.Tactic.Translate.Reorder
Mathlib.Tactic.Translate.Reorder.mk.sizeOf_spec : ∀ (univReorder : Mathlib.Tactic.Translate.Permutation) (reorder : Mathlib.Tactic.Translate.ArgReorder),
  sizeOf { univReorder := univReorder, reorder := reorder } = 1 + sizeOf univReorder + sizeOf reorder
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tprod_range : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {g : γ → β}
  (f : β → α), Function.Injective g → ∏' (x : ↑(Set.range g)), f ↑x = ∏' (x : γ), f (g x)
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.Content.outerRegular : ∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) [inst_1 : R1Space G] [S : MeasurableSpace G]
  [inst_2 : BorelSpace G], μ.measure.OuterRegular
-- Mathlib.Order.Filter.Pi
Filter.PiInfPrincipalPi.neBot : ∀ {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} {s : (i : ι) → Set (α i)}
  [h : ∀ (i : ι), (f i ⊓ Filter.principal (s i)).NeBot] {I : Set ι}, (Filter.pi f ⊓ Filter.principal (I.pi s)).NeBot
-- Mathlib.Topology.Compactness.SigmaCompact
/-- The sets in the compact exhaustion are in fact compact.  -/
CompactExhaustion.isCompact' : ∀ {X : Type u_4} [inst : TopologicalSpace X] (self : CompactExhaustion X) (n : ℕ), IsCompact (self.toFun n)
-- Mathlib.GroupTheory.Exponent
Monoid.ExponentExists.orderOf_pos : ∀ {G : Type u} [inst : Monoid G], Monoid.ExponentExists G → ∀ (g : G), 0 < orderOf g
-- Init.Data.List.Lemmas
List.append_eq_flatten_iff : ∀ {α : Type u_1} {xs : List (List α)} {ys zs : List α},
  ys ++ zs = xs.flatten ↔
    (∃ as bs, xs = as ++ bs ∧ ys = as.flatten ∧ zs = bs.flatten) ∨
      ∃ as bs c cs ds, xs = as ++ (bs ++ c :: cs) :: ds ∧ ys = as.flatten ++ bs ∧ zs = c :: cs ++ ds.flatten
-- Init.Data.Order.Ord
Std.OrientedCmp.not_lt_of_isLE : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.OrientedCmp cmp] {a b : α}, (cmp a b).isLE = true → cmp b a ≠ Ordering.lt
-- Batteries.Recycling.RBTree.Basic
RBTree.RBMap.instForMKeysOfMonad : {α : Type u} →
  {β : Type v} → {cmp : α → α → Ordering} → {m : Type u_1 → Type u_2} → [Monad m] → ForM m (RBTree.RBMap.Keys α β cmp) α
-- Mathlib.Analysis.Matrix.Spectrum
/-- The spectrum of a Hermitian matrix is the range of its eigenvalues under `RCLike.ofReal`.  -/
Matrix.IsHermitian.spectrum_eq_image_range : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : Fintype n] {A : Matrix n n 𝕜} [inst_2 : DecidableEq n]
  (hA : A.IsHermitian), spectrum 𝕜 A = RCLike.ofReal '' Set.range hA.eigenvalues
-- Mathlib.Order.CountableSupClosed
CountableSupClosed.iSup_mem : ∀ {ι : Sort u_1} {α : Type u_2} {s : Set α} [inst : CompleteLattice α] [Countable ι] [Nonempty ι],
  CountableSupClosed s → ∀ {A : ι → α}, (∀ (n : ι), A n ∈ s) → ⨆ n, A n ∈ s
-- Mathlib.Topology.Homotopy.Path
Path.Homotopy.source : ∀ {X : Type u} [inst : TopologicalSpace X] {x₀ x₁ : X} {p₀ p₁ : Path x₀ x₁} (F : p₀.Homotopy p₁) (t : ↑unitInterval),
  F (t, 0) = x₀
-- Mathlib.Analysis.Complex.Trigonometric
Complex.two_sin : ∀ (x : ℂ), 2 * Complex.sin x = (Complex.exp (-x * Complex.I) - Complex.exp (x * Complex.I)) * Complex.I
-- Mathlib.Data.Fin.Embedding
/-- `Fin.castAdd` as an `Embedding`, `castAddEmb m i` embeds `i : Fin n` in `Fin (n+m)`.
See also `Fin.natAddEmb` and `Fin.addNatEmb`.  -/
Fin.castAddEmb : {n : ℕ} → (m : ℕ) → Fin n ↪ Fin (n + m)
-- Mathlib.Topology.Separation.Hausdorff
/-- In a `T2Space`, every compact set is closed.  -/
IsCompact.isClosed : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X] {s : Set X}, IsCompact s → IsClosed s
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.FlatMap.0.Std.Iter.step_flatMapAfterM.match_3.splitter : {α₂ γ : Type u_1} →
  {m : Type u_1 → Type u_2} →
    [inst : Std.Iterator α₂ m γ] →
      (it₂ : Std.IterM m γ) →
        (motive : it₂.Step → Sort u_3) →
          (x : it₂.Step) →
            ((it₂' : Std.IterM m γ) →
                (out : γ) →
                  (h : it₂.IsPlausibleStep (Std.IterStep.yield it₂' out)) → motive ⟨Std.IterStep.yield it₂' out, h⟩) →
              ((it₂' : Std.IterM m γ) →
                  (h : it₂.IsPlausibleStep (Std.IterStep.skip it₂')) → motive ⟨Std.IterStep.skip it₂', h⟩) →
                ((h : it₂.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩) → motive x
-- Mathlib.Algebra.MonoidAlgebra.Module
/-- This is not an instance as it conflicts with `MonoidAlgebra.distribMulAction` when `M = kˣ`.

TODO: Change the type to `DistribMulAction Gᵈᵐᵃ S[M]` and then it can be an instance.
TODO: Generalise to a group acting on another, instead of just the left multiplication action.
 -/
MonoidAlgebra.comapDistribMulActionSelf : {S : Type u_2} → {G : Type u_6} → [inst : Group G] → [inst_1 : Semiring S] → DistribMulAction G (MonoidAlgebra S G)
-- Mathlib.CategoryTheory.Sites.Canonical
CategoryTheory.GrothendieckTopology.instFaithfulSheafTypeUliftYoneda : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical], (CategoryTheory.GrothendieckTopology.uliftYoneda.{w, v, u} J).Faithful
-- Mathlib.SetTheory.ZFC.Rank
ZFSet.rank_iUnion : ∀ {α : Type u_1} [inst : Small.{u, u_1} α] (f : α → ZFSet.{u}), (ZFSet.iUnion fun i => f i).rank = ⨆ i, (f i).rank
-- Mathlib.Algebra.BigOperators.Group.List.Basic
/-- A list with sum not zero must have positive length.  -/
List.length_pos_of_sum_ne_zero : ∀ {M : Type u_4} [inst : AddMonoid M] (L : List M), L.sum ≠ 0 → 0 < L.length
-- Lean.Elab.Parallel
/-- Runs a list of CoreM computations in parallel and returns the first successful result
(by completion order, not list order).

If `cancel := true` (the default), cancels all remaining tasks after the first success.
 -/
Lean.Core.CoreM.parFirst : {α : Type} → List (Lean.CoreM α) → optParam Bool true → Lean.CoreM α
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.inl_v_desc_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ}
  (α : CochainComplex.HomComplex.Cochain K M 0) (β : CochainComplex.HomComplex.Cocycle L M 1)
  (hαβ : CochainComplex.HomComplex.δ 0 1 α + (CochainComplex.HomComplex.Cochain.ofHom φ).comp ↑β ⋯ = 0) (p : ℤ),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.inl φ).v p p ⋯)
      ((CochainComplex.mappingCocone.desc φ α β hαβ).f p) =
    α.v p p ⋯
-- Init.Data.Array.Lemmas
Array.toList_zip : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {ys : Array β}, (xs.zip ys).toList = xs.toList.zip ys.toList
-- Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
AddChar.expect_apply_ne_zero_iff_eq_zero : ∀ {α : Type u_1} [inst : AddCommGroup α] {a : α} [inst_1 : Finite α], (Finset.univ.expect fun ψ => ψ a) ≠ 0 ↔ a = 0
-- Std.Time.Date.PlainDate
/-- Sets the date to the specified `desiredWeekday`. If the `desiredWeekday` is the same as the current weekday,
the original `date` is returned without modification. If the `desiredWeekday` is in the future, the
function adjusts the date forward to the next occurrence of that weekday.
 -/
Std.Time.PlainDate.withWeekday : Std.Time.PlainDate → Std.Time.Weekday → Std.Time.PlainDate
-- Mathlib.Analysis.Seminorm
Seminorm.mem_closedBall_zero : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E]
  (p : Seminorm 𝕜 E) {y : E} {r : ℝ}, y ∈ p.closedBall 0 r ↔ p y ≤ r
-- Mathlib.Topology.Homotopy.HomotopyGroup
GenLoop.instContinuousEval : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X},
  ContinuousEval (↑(GenLoop N X x)) (N → ↑unitInterval) X
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
MeasureTheory.SignedMeasure.rnDeriv_def : ∀ {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α),
  s.rnDeriv μ = fun x =>
    (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal - (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal
-- Mathlib.MeasureTheory.Function.AEEqFun
ContinuousMap.toAEEqFunMulHom.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) [inst_1 : TopologicalSpace α]
  [inst_2 : BorelSpace α] [inst_3 : TopologicalSpace β] [inst_4 : SecondCountableTopologyEither α β]
  [inst_5 : TopologicalSpace.PseudoMetrizableSpace β] [inst_6 : Group β] [inst_7 : IsTopologicalGroup β],
  ContinuousMap.toAEEqFunMulHom μ = { toFun := ContinuousMap.toAEEqFun μ, map_one' := ⋯, map_mul' := ⋯ }
-- Aesop.RuleTac.Forward
Aesop.RuleTac.ForwardM.Context.forwardHypData : Aesop.RuleTac.ForwardM.Context → Aesop.ForwardHypData
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
/-- A `PrelaxFunctorStruct` between bicategories consists of functions between objects,
1-morphisms, and 2-morphisms. This structure will be extended to define `PrelaxFunctor`.
 -/
CategoryTheory.PrelaxFunctorStruct : (B : Type u₁) →
  [inst : Quiver B] →
    [(a b : B) → Quiver (a ⟶ b)] →
      (C : Type u₂) →
        [inst : Quiver C] → [(a b : C) → Quiver (a ⟶ b)] → Type (max (max (max (max (max u₁ u₂) v₁) v₂) w₁) w₂)