mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- **Alias** of `MulHom.pi_apply`. -/
Pi.mulHom_apply : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → Mul (f i)] {γ : Type w} [inst_1 : Mul γ] (g : (i : I) → γ →ₙ* f i)
  (x : γ) (i : I), (MulHom.pi g) x i = (g i) x
-- Mathlib.Topology.ContinuousMap.Basic
Set.liftCover.congr_simp : ∀ {α : Type u_1} {ι : Sort u_2} {β : Sort u_3} (S : ι → Set α) (f f_1 : (i : ι) → ↑(S i) → β) (e_f : f = f_1)
  (hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩) (hS : Set.iUnion S = Set.univ)
  (a a_1 : α), a = a_1 → Set.liftCover S f hf hS a = Set.liftCover S f_1 ⋯ hS a_1
-- Lean.Parser.Types
Lean.Parser.ParserCacheEntry.stx : Lean.Parser.ParserCacheEntry → Lean.Syntax
-- Mathlib.Algebra.Order.Chebyshev
sum_div_card_sq_le_sum_sq_div_card : ∀ {ι : Type u_1} {α : Type u_2} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α]
  {s : Finset ι} {f : ι → α}, ((∑ i ∈ s, f i) / ↑s.card) ^ 2 ≤ (∑ i ∈ s, f i ^ 2) / ↑s.card
-- Mathlib.LinearAlgebra.RootSystem.Basic
/-- The bijection on the indexing set induced by reflection.  -/
RootPairing.equiv_of_mapsTo : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  (p : M →ₗ[R] N →ₗ[R] R) →
                    (root : ι ↪ M) →
                      (coroot : ι ↪ N) →
                        ι →
                          (∀ (i : ι),
                              Set.MapsTo (⇑(Module.preReflection (root i) (p.flip (coroot i)))) (Set.range ⇑root)
                                (Set.range ⇑root)) →
                            (∀ (i : ι), (p (root i)) (coroot i) = 2) → ι ≃ ι
-- Mathlib.Dynamics.FixedPoints.Basic
/-- If self-maps `f` and `g` commute, then `f` is bijective on the set of fixed points of `f ∘ g`.
This is a particular case of `Function.bijOn_fixedPoints_comp`.  -/
Function.Commute.left_bijOn_fixedPoints_comp : ∀ {α : Type u_1} {f g : α → α},
  Function.Commute f g → Set.BijOn f (Function.fixedPoints (f ∘ g)) (Function.fixedPoints (f ∘ g))
-- Mathlib.RingTheory.Noetherian.Basic
isNoetherian_iSup : ∀ {R : Type u_1} {N : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup N] [inst_2 : Module R N] {ι : Type u_6}
  [Finite ι] {M : ι → Submodule R N} [∀ (i : ι), IsNoetherian R ↥(M i)], IsNoetherian R ↥(⨆ i, M i)
-- Mathlib.RingTheory.TensorProduct.MonoidAlgebra
MonoidAlgebra.tensorEquiv_symm_single_eq_single_one_tmul : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommSemiring R] (mn : M × N) (r : R),
  (MonoidAlgebra.tensorEquiv R).symm (MonoidAlgebra.single mn r) =
    MonoidAlgebra.single mn.1 1 ⊗ₜ[R] MonoidAlgebra.single mn.2 r
-- Init.Data.List.Pairwise
List.Pairwise.imp₂ : ∀ {α : Type u_1} {R S T : α → α → Prop} {l : List α},
  (∀ (a b : α), R a b → S a b → T a b) → List.Pairwise R l → List.Pairwise S l → List.Pairwise T l
-- Aesop.Rule.Forward
/-- Is this rule a `destruct` rule (i.e., should we clear matched hyps)?  -/
Aesop.ForwardRule.destruct : Aesop.ForwardRule → Bool
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.toFun_eq_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : AddZeroClass α]
  [inst_3 : AddZeroClass β] (f : α →+o β), (↑f.toAddMonoidHom).toFun = ⇑f
-- Mathlib.LinearAlgebra.Multilinear.TensorProduct
MultilinearMap.domCoprod'_apply : ∀ {R : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} [inst : CommSemiring R] {N₁ : Type u_6} [inst_1 : AddCommMonoid N₁]
  [inst_2 : Module R N₁] {N₂ : Type u_7} [inst_3 : AddCommMonoid N₂] [inst_4 : Module R N₂] {N : Type u_8}
  [inst_5 : AddCommMonoid N] [inst_6 : Module R N] (a : MultilinearMap R (fun x => N) N₁)
  (b : MultilinearMap R (fun x => N) N₂), MultilinearMap.domCoprod' (a ⊗ₜ[R] b) = a.domCoprod b
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquivClass.instMulHomClass : ∀ {M : Type u_4} {N : Type u_5} (F : Type u_9) [inst : Mul M] [inst_1 : Mul N] [inst_2 : EquivLike F M N]
  [h : MulEquivClass F M N], MulHomClass F M N
-- Mathlib.Computability.Ackermann
lt_ack_right : ∀ (m n : ℕ), n < ack m n
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.closure_eq_range : ∀ {β : Type v} [inst : AddGroup β] (s : Set β), AddSubgroup.closure s = (FreeAddGroup.lift Subtype.val).range
-- Mathlib.RingTheory.WittVector.IsPoly
/-- Multiplication of Witt vectors is a polynomial function.  -/
WittVector.mulIsPoly₂ : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)], WittVector.IsPoly₂ p fun x x_1 x1 x2 => x1 * x2
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.delabHOrElse : Lean.PrettyPrinter.Delaborator.Delab
-- Std.Http.Data.Headers
Std.Http.Headers.instUnion : Union Std.Http.Headers
-- Lean.Compiler.CSimpAttr
Lean.Compiler.CSimp.State.mk.sizeOf_spec : ∀ (map : Lean.SMap Lean.Name Lean.Compiler.CSimp.Entry) (thmNames : Lean.SSet Lean.Name),
  sizeOf { map := map, thmNames := thmNames } = 1 + sizeOf map + sizeOf thmNames
-- Mathlib.Tactic.NormNum.Basic
Mathlib.Meta.NormNum.ne_of_false_of_true : ∀ {a b : Prop}, ¬a → b → a ≠ b
-- Lean.PrettyPrinter.Delaborator.Builtins
_private.Lean.PrettyPrinter.Delaborator.Builtins.0.Lean.PrettyPrinter.Delaborator.delabDIte.delabBranch : Option Lean.Name → Lean.PrettyPrinter.Delaborator.DelabM (Lean.Syntax × Lean.Name)
-- Mathlib.RingTheory.LaurentSeries
/-- The extension of the `X`-adic valuation from `K⟮X⟯` up to its abstract completion coincides,
modulo the isomorphism with `K⸨X⸩`, with the `X`-adic valuation on `K⸨X⸩`.  -/
LaurentSeries.valuation_compare : ∀ (K : Type u_2) [inst : Field K] (f : LaurentSeries K),
  Valued.v ((LaurentSeries.LaurentSeriesRingEquiv K) f) = Valued.v f
-- Mathlib.RingTheory.Unramified.Basic
/-- A version without stray universes that is more easy to rewrite with.  -/
Algebra.FormallyUnramified.iff_comp_injective : ∀ {R : Type v} [inst : CommRing R] {A : Type u} [inst_1 : CommRing A] [inst_2 : Algebra R A],
  Algebra.FormallyUnramified R A ↔
    ∀ ⦃B : Type u⦄ [inst_3 : CommRing B] [inst_4 : Algebra R B] (I : Ideal B),
      I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get!_eq_of_mem : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α] [inst_3 : Inhabited α],
  m.WF → ∀ {k : α}, k ∈ m → m.get! k = k
-- Mathlib.Order.Filter.AtTopBot.CompleteLattice
/-- If `s` is a monotone family of sets and `f` tends to `atBot` along a nontrivial filter,
then the indexed intersection of `s ∘ f` is equal to the indexed intersection of `s`.  -/
Monotone.iInter_comp_tendsto_atBot : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : Preorder β] {l : Filter α} [l.NeBot] {s : β → Set γ},
  Monotone s → ∀ {f : α → β}, Filter.Tendsto f l Filter.atBot → ⋂ a, s (f a) = ⋂ b, s b
-- Init.Data.Array.Set
/-- Replaces the element at the provided index in an array. The array is returned unmodified if the
index is out of bounds.

The array is modified in-place if there are no other references to it.

Examples:
* `#[0, 1, 2].setIfInBounds 1 5 = #[0, 5, 2]`
* `#["orange", "apple"].setIfInBounds 1 "grape" = #["orange", "grape"]`
* `#["orange", "apple"].setIfInBounds 5 "grape" = #["orange", "apple"]`
 -/
Array.setIfInBounds : {α : Type u_1} → Array α → ℕ → α → Array α
-- Mathlib.Logic.IsEmpty.Basic
isEmpty_pi : ∀ {α : Sort u_1} {π : α → Sort u_4}, IsEmpty ((a : α) → π a) ↔ ∃ a, IsEmpty (π a)
-- Aesop.Rule
/-- A global rule for the norm simplifier. Each `SimpEntry` represents a member
of the simp set, e.g. a declaration whose type is an equality or a smart
unfolding theorem for a declaration.
 -/
Aesop.NormSimpRule : Type
-- Mathlib.RingTheory.NoetherNormalization
/-- `up` is defined as `2 + f.totalDegree`. Any big enough number would work.  -/
_private.Mathlib.RingTheory.NoetherNormalization.0.NoetherNormalization.termUp : Lean.ParserDescr
-- Mathlib.Algebra.Category.ModuleCat.Semi
/-- Build a `LinearEquiv` from an isomorphism in the category `SemimoduleCat R`.  -/
CategoryTheory.Iso.toLinearEquivₛ : {R : Type u} → [inst : Semiring R] → {X Y : SemimoduleCat R} → (X ≅ Y) → ↑X ≃ₗ[R] ↑Y
-- Mathlib.RingTheory.Regular.Flat
RingTheory.Sequence.IsWeaklyRegular.isRegular_of_isLocalizedModule_of_mem : ∀ {R : Type u_1} (S : Type u_2) {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : AddCommGroup N] [inst_6 : Module R N]
  [inst_7 : Module S N] [IsScalarTower R S N] (p : Ideal R) [inst_9 : p.IsPrime] [IsLocalization.AtPrime S p]
  [Nontrivial N] [Module.Finite S N] (f : M →ₗ[R] N) [IsLocalizedModule.AtPrime p f] {rs : List R},
  RingTheory.Sequence.IsWeaklyRegular M rs →
    (∀ r ∈ rs, r ∈ p) → RingTheory.Sequence.IsRegular N (List.map (⇑(algebraMap R S)) rs)
-- Lean.Data.Lsp.Window
Lean.Lsp.instToJsonShowMessageResponse : Lean.ToJson Lean.Lsp.ShowMessageResponse
-- Mathlib.RingTheory.Bialgebra.GroupLike
/-- Group-like elements in a bialgebra are stable under inverses, when they exist.  -/
IsGroupLikeElem.of_mul_eq_one : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A] {a b : A},
  a * b = 1 → b * a = 1 → IsGroupLikeElem R a → IsGroupLikeElem R b
-- Mathlib.Order.LiminfLimsup
Filter.liminf_le_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLinearOrder β] {f : Filter α} {u : α → β} {x : β},
  autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f u) Filter.liminf_le_iff._auto_1 →
    autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) Filter.liminf_le_iff._auto_3 →
      (Filter.liminf u f ≤ x ↔ ∀ y > x, ∃ᶠ (a : α) in f, u a < y)
-- Lean.Util.Trace
Lean.trace : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadTrace m] →
      [Lean.MonadRef m] →
        [Lean.AddMessageContext m] → [Lean.MonadOptions m] → Lean.Name → (Unit → Lean.MessageData) → m Unit
-- Mathlib.Data.Num.Bitwise
/-- Bitwise "xor" for `PosNum`.  -/
PosNum.lxor : PosNum → PosNum → Num
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.mem_prod : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : StarRing A]
  [inst_3 : Module R A] [inst_4 : NonUnitalSemiring B] [inst_5 : StarRing B] [inst_6 : Module R B]
  {S : NonUnitalStarSubalgebra R A} {S₁ : NonUnitalStarSubalgebra R B} {x : A × B}, x ∈ S.prod S₁ ↔ x.1 ∈ S ∧ x.2 ∈ S₁
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
NumberField.FinitePlace.instNonarchimedeanHomClassReal : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K], NonarchimedeanHomClass (NumberField.FinitePlace K) K ℝ
-- Mathlib.GroupTheory.Perm.ConjAct
Equiv.Perm.cycleFactorsFinset_conj_eq : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (k : ConjAct (Equiv.Perm α)) (g : Equiv.Perm α),
  (k • g).cycleFactorsFinset = k • g.cycleFactorsFinset
-- Lean.Meta.Tactic.Grind.PP
Lean.Meta.Grind.goalDiagToMessageData : Lean.Meta.Grind.Goal →
  Lean.Grind.Config → optParam String "Goal diagnostics" → optParam Bool true → Lean.MetaM Lean.MessageData
-- Mathlib.Algebra.Group.Graph
/-- **Vertical line test** for additive monoid homomorphisms.

Let `G ≤ H × I` be a submonoid of a product of monoids. Assume that `G` surjects onto the first
factor and `G` intersects every "vertical line" `{(h, i) | i : I}` at most once. Then `G` is the
graph of some monoid homomorphism `f : H → I`.  -/
AddSubgroup.exists_eq_graph : ∀ {H : Type u_2} {I : Type u_3} [inst : AddGroup H] [inst_1 : AddGroup I] {G : AddSubgroup (H × I)},
  Function.Bijective (Prod.fst ∘ ⇑G.subtype) → ∃ f, G = f.graph
-- Mathlib.Tactic.ClickSuggestions.Util
Mathlib.Tactic.ClickSuggestions.State.mk.injEq : ∀ (status : Std.HashMap String ℕ) (progress : Bool) (solvedSuggestions : Array ProofWidgets.Html)
  (status_1 : Std.HashMap String ℕ) (progress_1 : Bool) (solvedSuggestions_1 : Array ProofWidgets.Html),
  ({ status := status, progress := progress, solvedSuggestions := solvedSuggestions } =
      { status := status_1, progress := progress_1, solvedSuggestions := solvedSuggestions_1 }) =
    (status = status_1 ∧ progress = progress_1 ∧ solvedSuggestions = solvedSuggestions_1)
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.mapTriangleInvRotateIso_hom_app_hom₁ : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ]
  [inst_5 : CategoryTheory.Preadditive C] [inst_6 : CategoryTheory.Preadditive D] [inst_7 : F.Additive]
  (X : CategoryTheory.Pretriangulated.Triangle C),
  (F.mapTriangleInvRotateIso.hom.app X).hom₁ = (CategoryTheory.Functor.commShiftIso F (-1)).inv.app X.obj₃
-- Lean.Declaration
/-- Number of indices. An index is an argument that varies over constructors.

An example of this is the `n : Nat` argument in the vector constructor `cons : α → Vector α n → Vector α (n+1)`.
 -/
Lean.InductiveVal.numIndices : Lean.InductiveVal → ℕ
-- Init.Data.Rat.Lemmas
Rat.ofScientific_def_eq_if : ∀ {m : ℕ} {s : Bool} {e : ℕ}, OfScientific.ofScientific m s e = if s = true then ↑m / 10 ^ e else ↑m * 10 ^ e
-- Mathlib.Geometry.Diffeology.Basic
DiffeologicalSpace.mk : {X : Type u_1} →
  (plots : (n : ℕ) → Set (EuclideanSpace ℝ (Fin n) → X)) →
    (∀ {n : ℕ} (x : X), (fun x_1 => x) ∈ plots n) →
      (∀ {n m : ℕ} {p : EuclideanSpace ℝ (Fin m) → X} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)},
          p ∈ plots m → ContDiff ℝ (↑⊤) f → p ∘ f ∈ plots n) →
        (∀ {n : ℕ} {p : EuclideanSpace ℝ (Fin n) → X},
            (∀ (x : EuclideanSpace ℝ (Fin n)),
                ∃ u,
                  IsOpen u ∧
                    x ∈ u ∧
                      ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
                        (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) → ContDiff ℝ (↑⊤) f → p ∘ f ∈ plots m) →
              p ∈ plots n) →
          (dTopology : TopologicalSpace X) →
            autoParam (∀ {u : Set X}, TopologicalSpace.IsOpen u ↔ ∀ {n : ℕ}, ∀ p ∈ plots n, IsOpen (p ⁻¹' u))
                DiffeologicalSpace.isOpen_iff_preimages_plots._autoParam →
              DiffeologicalSpace X
-- Mathlib.Topology.Algebra.Order.Field
/-- The function `r ↦ r⁻¹` tends to `0` on the right as `r → +∞`.  -/
tendsto_inv_atTop_nhdsGT_zero : ∀ {𝕜 : Type u_1} [inst : Semifield 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [OrderTopology 𝕜], Filter.Tendsto (fun r => r⁻¹) Filter.atTop (nhdsWithin 0 (Set.Ioi 0))
-- Mathlib.InformationTheory.Hamming
/-- Corresponds to `norm_pos_iff`.  -/
hammingNorm_pos_iff : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)]
  [inst_2 : (i : ι) → Zero (β i)] {x : (i : ι) → β i}, 0 < hammingNorm x ↔ x ≠ 0
-- Mathlib.NumberTheory.Divisors
Nat.divisors_zero : Nat.divisors 0 = ∅
-- Mathlib.Data.ZMod.Basic
ZMod.coe_mul_inv_eq_one : ∀ {n : ℕ} (x : ℕ), x.Coprime n → ↑x * (↑x)⁻¹ = 1
-- Init.Data.Array.Lemmas
Array.appendList_nil : ∀ {α : Type u_1} {xs : Array α}, xs ++ [] = xs
-- Mathlib.Order.Hom.Lattice
/-- Evaluation as a lattice homomorphism.  -/
Pi.evalLatticeHom : {ι : Type u_6} → {α : ι → Type u_7} → [inst : (i : ι) → Lattice (α i)] → (i : ι) → LatticeHom ((i : ι) → α i) (α i)
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- Two submodules `M` and `N` in an algebra `S` over `R` are linearly disjoint if the natural map
`M ⊗[R] N →ₗ[R] S` induced by multiplication in `S` is injective.  -/
Submodule.LinearDisjoint : {R : Type u} →
  {S : Type v} →
    [inst : CommSemiring R] → [inst_1 : Semiring S] → [inst_2 : Algebra R S] → Submodule R S → Submodule R S → Prop
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.values_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.values = t₂.values
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.hasHomology_of_epi_of_isIso_of_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [S₁.HasHomology] [CategoryTheory.Epi φ.τ₁]
  [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃], S₂.HasHomology
-- Mathlib.NumberTheory.LSeries.SumCoeff
/-- If the partial sums `∑ k ∈ Icc 1 n, f k` are `O(n ^ r)` for some real `0 ≤ r` and the
L-series `LSeries f` converges at `s : ℂ` with `r < s.re`, then
`LSeries f s = s * ∫ t in Set.Ioi 1, (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * t ^ (-(s + 1))`.  -/
LSeries_eq_mul_integral : ∀ (f : ℕ → ℂ) {r : ℝ},
  0 ≤ r →
    ∀ {s : ℂ},
      r < s.re →
        LSeriesSummable f s →
          ((fun n => ∑ k ∈ Finset.Icc 1 n, f k) =O[Filter.atTop] fun n => ↑n ^ r) →
            LSeries f s = s * ∫ (t : ℝ) in Set.Ioi 1, (∑ k ∈ Finset.Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-(s + 1))
-- Init.Data.List.Erase
_private.Init.Data.List.Erase.0.List.filterMap.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match some b with
    | none => h_1 ()
    | some b => h_2 b) =
    h_2 b
-- Mathlib.Data.Finset.Sups
Finset.subset_diffs : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : GeneralizedBooleanAlgebra α] {u : Finset α} {s t : Set α},
  ↑u ⊆ Set.image2 (fun x1 x2 => x1 \ x2) s t → ∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s'.diffs t'
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.instAdd : {ι : Type u_1} → {M : ι → Type u_5} → [(i : ι) → Add (M i)] → Add ((i : ι) → M i)
-- Mathlib.FieldTheory.IsAlgClosed.Basic
IsAlgClosure.equivOfEquiv_comp_algebraMap : ∀ {R : Type u} {S : Type u_3} (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Field L]
  [inst_3 : Field M] [inst_4 : Algebra R M] [inst_5 : Module.IsTorsionFree R M] [inst_6 : IsAlgClosure R M]
  [inst_7 : Algebra S L] [inst_8 : Module.IsTorsionFree S L] [inst_9 : IsAlgClosure S L] [inst_10 : IsDomain R]
  [inst_11 : IsDomain S] (hSR : S ≃+* R),
  (↑(IsAlgClosure.equivOfEquiv L M hSR)).comp (algebraMap S L) = (algebraMap R M).comp ↑hSR
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Fintype.sum_empty : ∀ {ι : Type u_1} {M : Type u_3} [inst : Fintype ι] [inst_1 : AddCommMonoid M] [IsEmpty ι] (f : ι → M), ∑ x, f x = 0
-- Mathlib.Logic.Embedding.Basic
Function.instFunLikeEmbedding : {α : Sort u} → {β : Sort v} → FunLike (α ↪ β) α β
-- Mathlib.Tactic.FastInstance
/-- `fast_instance% inst` takes an expression for a typeclass instance `inst`, and unfolds it into
constructor applications that leverage existing instances. It uses the expected type to fill in
the constructor applications and lambda binders of data fields.

For instance, when used as
```lean
instance instSemiring : Semiring X := sorry
instance instRing : Ring X := fast_instance% Function.Injective.ring ..
```
this will define `instRing` as a nested constructor application that refers to `instSemiring`
rather than applications of `Function.Injective.ring` or other non-canonical constructors.
The advantage is then that `instRing.toSemiring` unifies almost immediately with `instSemiring`,
rather than having to break it down into smaller pieces.
 -/
Mathlib.Elab.FastInstance.elabFastInstance : Lean.Elab.Term.TermElab
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.le_degree_of_mem_support : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {p : MvPolynomial σ R} {a : σ →₀ ℕ},
  a ∈ p.support → m.toSyn a ≤ m.toSyn (m.degree p)
-- Mathlib.GroupTheory.Commutator.Basic
commutator_eq_normalClosure : ∀ (G : Type u_1) [inst : Group G], commutator G = Subgroup.normalClosure (commutatorSet G)
-- Mathlib.Data.Real.Embedding
Archimedean.ratLt'_bddAbove : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [IsOrderedAddMonoid M] [inst_3 : One M]
  [ZeroLEOneClass M] [NeZero 1] [Archimedean M] (x : M), BddAbove (Archimedean.ratLt' x)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.alter.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.LawfulEqOrd α] (k : α) (f : Option (β k) → Option (β k))
  (hr_1 : Std.DTreeMap.Internal.Impl.leaf.Balanced),
  Std.DTreeMap.Internal.Impl.alter k f Std.DTreeMap.Internal.Impl.leaf hr_1 =
    match f none with
    | none =>
      { impl := Std.DTreeMap.Internal.Impl.leaf, balanced_impl := ⋯, lb_le_size_impl := ⋯, size_impl_le_ub := ⋯ }
    | some v =>
      { impl := Std.DTreeMap.Internal.Impl.inner 1 k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf,
        balanced_impl := ⋯, lb_le_size_impl := ⋯, size_impl_le_ub := ⋯ }
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.extensionProductIter_add' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) [CategoryTheory.IsTriangulated C] {n m m' : ℕ},
  m = m' + 1 → P.extensionProductIter (n + m) = (P.extensionProductIter n).extensionProduct (P.extensionProductIter m')
-- Mathlib.Data.Finset.Preimage
Finset.preimage_univ : ∀ {α : Type u} {β : Type v} {f : α → β} [inst : Fintype α] [inst_1 : Fintype β] (hf : Set.InjOn f (f ⁻¹' ↑Finset.univ)),
  Finset.univ.preimage f hf = Finset.univ
-- Mathlib.NumberTheory.MulChar.Basic
/-- Bundled version of `MulChar.ringHomComp` as a `MonoidHom`.  -/
MulChar.ringHomCompHom : {R : Type u_1} →
  [inst : CommMonoid R] →
    {R' : Type u_2} →
      [inst_1 : CommRing R'] → {R'' : Type u_3} → [inst_2 : CommRing R''] → (R' →+* R'') → MulChar R R' →* MulChar R R''
-- Mathlib.Combinatorics.Additive.Energy
Finset.mulEnergy_mono : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Mul α] {s₁ s₂ t₁ t₂ : Finset α},
  s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁.mulEnergy t₁ ≤ s₂.mulEnergy t₂
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.getEntryLE?_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp] {k : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getEntryLE? k = t₂.getEntryLE? k
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get?_eq_some_iff : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  {v : β k}, m.get? k = some v ↔ ∃ (h : k ∈ m), m.get k h = v
-- Mathlib.Order.Bounds.Image
StrictAnti.mem_upperBounds_image : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {a : α} {s : Set α},
  StrictAnti f → (f a ∈ upperBounds (f '' s) ↔ a ∈ lowerBounds s)
-- Init.Data.Vector.Lemmas
Vector.find?_toArray : ∀ {α : Type} {n : ℕ} {p : α → Bool} {xs : Vector α n}, Array.find? p xs.toArray = Vector.find? p xs
-- Mathlib.RingTheory.Valuation.Basic
/-- The subgroup of elements whose valuation is less than or equal to a certain value.  -/
Valuation.leAddSubgroup : {R : Type u_3} →
  {Γ₀ : Type u_4} → [inst : Ring R] → [inst_1 : LinearOrderedCommGroupWithZero Γ₀] → Valuation R Γ₀ → Γ₀ → AddSubgroup R
-- Batteries.Data.Fin.Basic
/-- Compute `i % n`, where `n` is a `Nat` and inferred the type of `i`.  -/
Fin.modNat : {m n : ℕ} → Fin (m * n) → Fin n
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.integral_add : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
  {l : BoxIntegral.IntegrationParams} {f g : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤},
  BoxIntegral.Integrable I l f vol →
    BoxIntegral.Integrable I l g vol →
      BoxIntegral.integral I l (f + g) vol = BoxIntegral.integral I l f vol + BoxIntegral.integral I l g vol