mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Multilinear.Curry
/-- Interpret a multilinear map in `n + 1` variables
as a linear map in `p`th variable with values in the multilinear maps in the other variables.  -/
MultilinearMap.curryMid : {R : Type uR} →
  {n : ℕ} →
    {M : Fin n.succ → Type v} →
      {M₂ : Type v₂} →
        [inst : CommSemiring R] →
          [inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : (i : Fin n.succ) → Module R (M i)] →
                [inst_4 : Module R M₂] →
                  (p : Fin (n + 1)) → MultilinearMap R M M₂ → M p →ₗ[R] MultilinearMap R (fun i => M (p.succAbove i)) M₂
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem?_diff_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∈ t₂ → (t₁ \ t₂)[k]? = none
-- Mathlib.Topology.Separation.Regular
Subtype.t3Space : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T3Space X] {p : X → Prop}, T3Space (Subtype p)
-- Mathlib.Combinatorics.Digraph.Basic
Digraph.completeAtomicBooleanAlgebra : {V : Type u_2} → CompleteAtomicBooleanAlgebra (Digraph V)
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.one_tmul_ground : ∀ {R : Type u} [inst : CommSemiring R] {M : Type u_3} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_4}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (f : M →ₚₗ[R] N) (S : Type u_5) [inst_5 : CommSemiring S]
  [inst_6 : Algebra R S] (x : M), 1 ⊗ₜ[R] f.ground x = PolynomialLaw.toFun S f (1 ⊗ₜ[R] x)
-- Mathlib.Algebra.Group.Prod
/-- Given monoids `M`, `N`, the natural projection homomorphism from `M × N` to `N`.  -/
MonoidHom.snd : (M : Type u_3) → (N : Type u_4) → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → M × N →* N
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
Real.iUnion_Iic_rat : ⋃ r, Set.Iic ↑r = Set.univ
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- Creates an E-match theorem using the given proof and kind.
If `groundPatterns` is `true`, it accepts patterns without pattern variables. This is useful for
theorems such as `theorem evenZ : Even 0`. For local theorems, we use `groundPatterns := false`
since the theorem is already in the `grind` state and there is nothing to be instantiated.
 -/
Lean.Meta.Grind.mkEMatchTheoremWithKind? : Lean.Meta.Grind.Origin →
  Array Lean.Name →
    Lean.Expr →
      Lean.Meta.Grind.EMatchTheoremKind →
        Lean.Meta.Grind.SymbolPriorities →
          optParam Bool true →
            optParam Bool false → optParam Bool false → Lean.MetaM (Option Lean.Meta.Grind.EMatchTheorem)
-- Mathlib.CategoryTheory.Comma.Over.Pullback
/-- The functor from `C` to `Over X` which sends `Y : C` to `π₁ : X ⨯ Y ⟶ X`, sometimes denoted `X*`.
 -/
CategoryTheory.Over.star : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X : C) → [CategoryTheory.Limits.HasBinaryProducts C] → CategoryTheory.Functor C (CategoryTheory.Over X)
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
RatFunc.algEquivOfTranscendental_algebraMap : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (f : L)
  (h : Transcendental K f) (g : Polynomial K),
  (RatFunc.algEquivOfTranscendental f h) ((algebraMap (Polynomial K) (RatFunc K)) g) =
    (Polynomial.aeval (IntermediateField.AdjoinSimple.gen K f)) g
-- Init.Data.BitVec.Lemmas
BitVec.toNat_mod_cancel_of_lt : ∀ {n m : ℕ} {x : BitVec n}, n < m → x.toNat % 2 ^ m = x.toNat
-- Mathlib.Combinatorics.Matroid.Minor.Contract
/-- `M ／ C` refers to the contraction of a set `C` from the matroid `M`.  -/
Matroid.«term_／_» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.Valuation.Basic
Valuation.map_sub : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀)
  (x y : R), v (x - y) ≤ max (v x) (v y)
-- Mathlib.Topology.Order.OrderClosed
Ico_mem_nhdsLT : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIicTopology α] {a b : α},
  a < b → Set.Ico a b ∈ nhdsWithin b (Set.Iio b)
-- Mathlib.MeasureTheory.Function.Intersectivity
/-- **Bergelson Intersectivity Lemma**: In a finite measure space, a sequence of events that have
measure at least `r` has an infinite subset whose finite intersections all have positive volume.  -/
bergelson : ∀ {ι : Type u_1} {α : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [MeasureTheory.IsFiniteMeasure μ] {r : ENNReal} [Infinite ι] {s : ι → Set α},
  (∀ (i : ι), MeasurableSet (s i)) →
    r ≠ 0 → (∀ (i : ι), r ≤ μ (s i)) → ∃ t, t.Infinite ∧ ∀ ⦃u : Set ι⦄, u ⊆ t → u.Finite → 0 < μ (⋂ i ∈ u, s i)
-- Mathlib.Data.Stream.Init
Stream'.unfolds_eq : ∀ {α : Type u} {β : Type v} (g : α → β) (f : α → α) (a : α),
  Stream'.unfolds g f a = Stream'.cons (g a) (Stream'.unfolds g f (f a))
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.kernelIsoOfEq.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f g : X ⟶ Y} [inst_2 : CategoryTheory.Limits.HasKernel f] [inst_3 : CategoryTheory.Limits.HasKernel g] (h : f = g),
  CategoryTheory.Limits.kernelIsoOfEq h = CategoryTheory.Limits.kernelIsoOfEq h
-- Mathlib.Data.List.Cycle
List.mem_of_nextOr_ne : ∀ {α : Type u_1} [inst : DecidableEq α] {xs : List α} {x d : α}, xs.nextOr x d ≠ d → x ∈ xs
-- Init.Data.Int.Pow
Int.mul_pow : ∀ {a b : ℤ} {n : ℕ}, (a * b) ^ n = a ^ n * b ^ n
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_add_right : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIcoMod hp a (b + p) = toIcoMod hp a b
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
MulOpposite.dist_unop : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] (x y : αᵐᵒᵖ), dist (MulOpposite.unop x) (MulOpposite.unop y) = dist x y
-- Mathlib.CategoryTheory.Subobject.FactorThru
CategoryTheory.Subobject.mk_factors_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : Y ⟶ X) [inst_1 : CategoryTheory.Mono f]
  (g : Z ⟶ X), (CategoryTheory.Subobject.mk f).Factors g ↔ (CategoryTheory.MonoOver.mk f).Factors g
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.entryAtIdx?_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] {i : ℕ},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.entryAtIdx? i = t₂.entryAtIdx? i
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.forM_eq_forM_keysArray : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) {m' : Type w → Type w'} [inst : Monad m']
  [LawfulMonad m'] {f : α → m' PUnit.{w + 1}}, Std.DHashMap.Raw.forM (fun a x => f a) ↑m = Array.forM f (↑m).keysArray
-- Mathlib.Analysis.MellinTransform
mellin_cpow_smul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : ℝ → E) (s a : ℂ),
  mellin (fun t => ↑t ^ a • f t) s = mellin f (s + a)
-- Init.Data.UInt.Lemmas
UInt8.size_le_usizeSize : UInt8.size ≤ USize.size
-- Mathlib.Order.Ideal
Order.Ideal.lower : ∀ {P : Type u_1} [inst : LE P] (s : Order.Ideal P), IsLowerSet ↑s
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.whiskeringRight₂_obj_obj_obj_map : ∀ (B : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} B] (C : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  (D : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} D] (E : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E] (X : CategoryTheory.Functor C (CategoryTheory.Functor D E))
  (X_1 : CategoryTheory.Functor B C) (Y : CategoryTheory.Functor B D) {X_2 Y_1 : B} (f : X_2 ⟶ Y_1),
  ((((CategoryTheory.Functor.whiskeringRight₂ B C D E).obj X).obj X_1).obj Y).map f =
    CategoryTheory.CategoryStruct.comp ((X.map (X_1.map f)).app (Y.obj X_2)) ((X.obj (X_1.obj Y_1)).map (Y.map f))
-- Std.Data.ExtHashMap.Basic
Std.ExtHashMap.instLawfulBEq : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : LawfulBEq α] [inst_1 : BEq β] [LawfulBEq β],
  LawfulBEq (Std.ExtHashMap α β)
-- Mathlib.Analysis.Normed.Affine.Simplex
Affine.Simplex.Regular.equilateral : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring R] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : PseudoMetricSpace P] [inst_3 : Module R V] [inst_4 : NormedAddTorsor V P] {n : ℕ}
  {s : Affine.Simplex R P n}, s.Regular → s.Equilateral
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.commSemiring : CommSemiring Cardinal.{u}
-- Lean.Elab.BuiltinTerm
Lean.Elab.Term.elabStrLit : Lean.Elab.Term.TermElab
-- Lean.Elab.Tactic.Omega.Frontend
/-- Given a collection of facts, try prove `False` using the omega algorithm,
and close the goal using that.
 -/
Lean.Elab.Tactic.Omega.omega : List Lean.Expr → Lean.MVarId → optParam Lean.Meta.Omega.OmegaConfig { } → Lean.MetaM Unit
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
QuadraticForm.tmul.congr_simp : ∀ {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : AddCommGroup M₁] [inst_3 : AddCommGroup M₂] [inst_4 : Algebra R A] [inst_5 : Module R M₁]
  [inst_6 : Module A M₁] [inst_7 : SMulCommClass R A M₁] [inst_8 : IsScalarTower R A M₁] [inst_9 : Module R M₂]
  [inst_10 : Invertible 2] (Q₁ Q₁_1 : QuadraticForm A M₁),
  Q₁ = Q₁_1 → ∀ (Q₂ Q₂_1 : QuadraticForm R M₂), Q₂ = Q₂_1 → Q₁.tmul Q₂ = Q₁_1.tmul Q₂_1
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.ground_nonempty_iff : ∀ {α : Type u_1} (M : Matroid α), M.E.Nonempty ↔ M.Nonempty
-- Lean.Meta.Tactic.Grind.Action
_private.Lean.Meta.Tactic.Grind.Action.0.Lean.Meta.Grind.Action.loopRef.eq_1 : ∀ (x : Lean.Meta.Grind.Action) (goal : Lean.Meta.Grind.Goal) (x_1 kp : Lean.Meta.Grind.ActionCont),
  Lean.Meta.Grind.Action.loopRef 0 x goal x_1 kp = kp goal
-- Init.Data.BitVec.Lemmas
/-- Unsigned multiplication overflow reassociation.
If `(x * y)` and `(y * z)` do not overflow, then `(x * y) * z` overflows iff `x * (y * z)` overflows.
 -/
BitVec.umulOverflow_assoc : ∀ {w : ℕ} {x y z : BitVec w},
  ¬x.umulOverflow y = true → ¬y.umulOverflow z = true → (x * y).umulOverflow z = x.umulOverflow (y * z)
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.X_order_mul_powerSeriesPart : ∀ {R : Type u_1} [inst : Semiring R] {n : ℕ} {f : LaurentSeries R},
  ↑n = HahnSeries.order f → (HahnSeries.ofPowerSeries ℤ R) (PowerSeries.X ^ n * f.powerSeriesPart) = f
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast?_replaceEntry : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)} {a k : α} {v : β k},
  Std.Internal.List.getValueCast? a (Std.Internal.List.replaceEntry k v l) =
    if h : Std.Internal.List.containsKey k l = true ∧ (k == a) = true then some (cast ⋯ v)
    else Std.Internal.List.getValueCast? a l
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Functor.splitEpiBiprodComparison.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) (X Y : C) [inst_4 : CategoryTheory.Limits.HasBinaryBiproduct X Y]
  [inst_5 : CategoryTheory.Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] [inst_6 : F.PreservesZeroMorphisms],
  F.splitEpiBiprodComparison X Y = F.splitEpiBiprodComparison X Y
-- Std.Time.Duration
/-- Converts a `Duration` to a `Millisecond.Offset`
 -/
Std.Time.Duration.toMilliseconds : Std.Time.Duration → Std.Time.Millisecond.Offset
-- Mathlib.Tactic.GCongr.Core
Mathlib.Tactic.GCongr.GCongrKey.mk : Lean.Name → Lean.Name → ℕ → Mathlib.Tactic.GCongr.GCongrKey
-- Batteries.Data.List.Lemmas
List.swap_eq_of_ge_left : ∀ {α : Type u_1} {i j : ℕ} {xs : List α}, xs.length ≤ i → xs.swap i j = xs
-- Lean.Server.FileWorker.InlayHints
Lean.Server.FileWorker.instInhabitedInlayHintState : Inhabited Lean.Server.FileWorker.InlayHintState
-- Mathlib.Data.List.Sym
_private.Mathlib.Data.List.Sym.0.List.sym2.match_1.splitter : {α : Type u_1} →
  (motive : List α → Sort u_2) →
    (x : List α) → (Unit → motive []) → ((x : α) → (xs : List α) → motive (x :: xs)) → motive x
-- Init.Data.Vector.Lex
Vector.le_toList : ∀ {α : Type u_1} {n : ℕ} [inst : LT α] {xs ys : Vector α n}, xs.toList ≤ ys.toList ↔ xs ≤ ys
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.integral_Ici_eq_integral_Ioi : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {μ : MeasureTheory.Measure X} [inst_2 : PartialOrder X] {x : X} [MeasureTheory.NullSingletonClass μ],
  ∫ (t : X) in Set.Ici x, f t ∂μ = ∫ (t : X) in Set.Ioi x, f t ∂μ
-- Mathlib.Order.Sublocale
Sublocale.carrier.instHeytingAlgebra : {X : Type u_1} → [inst : Order.Frame X] → {S : Sublocale X} → HeytingAlgebra ↥S
-- Mathlib.Analysis.InnerProductSpace.Completion
_private.Mathlib.Analysis.InnerProductSpace.Completion.0.«term⟪_,_⟫» : Lean.ParserDescr
-- Mathlib.RingTheory.WittVector.FrobeniusFractionField
WittVector.RecursionBase.solution_pow : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : Field k] [IsAlgClosed k] (a₁ a₂ : WittVector p k),
  ∃ x, x ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0
-- Mathlib.Data.Nat.Nth
Nat.nth_of_forall : ∀ {p : ℕ → Prop} {n : ℕ}, (∀ n' ≤ n, p n') → Nat.nth p n = n
-- Mathlib.Data.Complex.Basic
Complex.normSq_ratCast : ∀ (q : ℚ), Complex.normSq ↑q = ↑q * ↑q
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.trans_toBialgHom : ∀ {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Semiring C] [inst_4 : Algebra R A] [inst_5 : Algebra R B] [inst_6 : Algebra R C]
  [inst_7 : CoalgebraStruct R A] [inst_8 : CoalgebraStruct R B] [inst_9 : CoalgebraStruct R C] {e₁₂ : A ≃ₐc[R] B}
  {e₂₃ : B ≃ₐc[R] C}, ↑(e₁₂.trans e₂₃) = (↑e₂₃).comp ↑e₁₂
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.ofFintype_apply : ∀ {α : Type u_1} [inst : Fintype α] {f : α → ENNReal} (h : ∑ a, f a = 1) (a : α), (PMF.ofFintype f h) a = f a
-- Mathlib.RingTheory.AdicCompletion.Basic
IsPrecomplete.prec' : ∀ {R : Type u_1} {inst : CommRing R} {I : Ideal R} {M : Type u_4} {inst_1 : AddCommGroup M} {inst_2 : Module R M}
  [self : IsPrecomplete I M] (f : ℕ → M),
  (∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]) → ∃ L, ∀ (n : ℕ), f n ≡ L [SMOD I ^ n • ⊤]
-- Init.Data.SInt.Lemmas
Int32.mul_comm : ∀ (a b : Int32), a * b = b * a
-- Mathlib.Analysis.Analytic.Constructions
/-- Eta-expanded form of `AnalyticOnNhd.zpow_nonneg`

---

ZPowers of analytic functions (into a normed division algebra over `𝕜`) are analytic if the
exponent is nonnegative.  -/
AnalyticOnNhd.fun_zpow_nonneg : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝕝 : Type u_8} [inst_3 : NormedDivisionRing 𝕝] [inst_4 : NormedAlgebra 𝕜 𝕝] {f : E → 𝕝}
  {s : Set E} {n : ℤ}, AnalyticOnNhd 𝕜 f s → 0 ≤ n → AnalyticOnNhd 𝕜 (fun i => f i ^ n) s
-- LeanSearchClient.LoogleSyntax
LeanSearchClient.LoogleResult.failure.inj : ∀ {error : String} {suggestions : Option (List String)} {error_1 : String} {suggestions_1 : Option (List String)},
  LeanSearchClient.LoogleResult.failure error suggestions =
      LeanSearchClient.LoogleResult.failure error_1 suggestions_1 →
    error = error_1 ∧ suggestions = suggestions_1
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.floor_congr : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] {a : R} {S : Type u_3}
  [inst_3 : Semiring S] [inst_4 : LinearOrder S] [inst_5 : FloorSemiring S] {b : S} [IsStrictOrderedRing R]
  [IsStrictOrderedRing S], (∀ (n : ℕ), ↑n ≤ a ↔ ↑n ≤ b) → ⌊a⌋₊ = ⌊b⌋₊
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
quasispectrum.nonempty : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalRing A] [inst_2 : Module R A] [Nontrivial R]
  (a : A), (quasispectrum R a).Nonempty
-- Mathlib.Data.Finset.Prod
Finset.product_sdiff_offDiag : ∀ {α : Type u_1} (s : Finset α) [inst : DecidableEq α], s ×ˢ s \ s.offDiag = s.diag
-- Init.Data.String.Lemmas.Search
String.front?_eq_get? : ∀ {s : String}, s.front? = s.startPos.get?
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.DiagramOfCones.conePoints_obj : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} (D : CategoryTheory.Limits.DiagramOfCones F) (j : J),
  D.conePoints.obj j = (D.obj j).pt
-- Mathlib.Data.Finset.Image
Finset.mem_filterMap : ∀ {α : Type u_1} {β : Type u_2} (f : α → Option β) {s : Finset α} {f_inj : ∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a'}
  {b : β}, b ∈ Finset.filterMap f s f_inj ↔ ∃ a ∈ s, f a = some b
-- Lean.Widget.UserWidget
/-- The syntactic span in the Lean file at which the panel widget is displayed.  -/
Lean.Widget.PanelWidgetInstance.range? : Lean.Widget.PanelWidgetInstance → Option Lean.Lsp.Range
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.ofIsClopen.eq_1 : ∀ {X : Type u_5} [inst : TopologicalSpace X] {U : Set X} [inst_1 : (x : X) → Decidable (x ∈ U)] (hU : IsClopen U),
  LocallyConstant.ofIsClopen hU = { toFun := fun x => if x ∈ U then 0 else 1, isLocallyConstant := ⋯ }
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.instIsCancelMulZeroOfIsCancelAdd : ∀ {R : Type u} [inst : Semiring R] [IsCancelAdd R] [IsCancelMulZero R], IsCancelMulZero (Polynomial R)
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.toEquiv_injective : ∀ {α : Type u_9} {β : Type u_10} [inst : Add α] [inst_1 : Add β], Function.Injective AddEquiv.toEquiv
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
/-- To show that a right lift `t` is a Kan lift, we need to show that for every right lift `s`
there is a unique morphism `s ⟶ t`.  -/
CategoryTheory.Bicategory.RightLift.IsKan.mk : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : b ⟶ a} →
        {g : c ⟶ a} →
          {t : CategoryTheory.Bicategory.RightLift f g} →
            (desc : (s : CategoryTheory.Bicategory.RightLift f g) → s ⟶ t) →
              (∀ (s : CategoryTheory.Bicategory.RightLift f g) (τ : s ⟶ t), τ = desc s) → t.IsKan
-- Mathlib.Algebra.LinearRecurrence
/-- The geometric sequence `q^n` is a solution of `E` iff
`q` is a root of `E`'s characteristic polynomial.  -/
LinearRecurrence.geom_sol_iff_root_charPoly : ∀ {R : Type u_1} [inst : CommRing R] (E : LinearRecurrence R) (q : R),
  (E.IsSolution fun n => q ^ n) ↔ E.charPoly.IsRoot q
-- Mathlib.CategoryTheory.CommSq
CategoryTheory.CommSq.fac_right : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A B X Y : C} {f : X ⟶ A} {i : B ⟶ A} {p : Y ⟶ X}
  {g : Y ⟶ B} (sq : CategoryTheory.CommSq g p i f) [hsq : sq.HasLift], CategoryTheory.CategoryStruct.comp sq.lift i = f
-- Lean.Elab.PreDefinition.Structural.IndGroupInfo
/-- Instantiates the right `.brecOn` for the given type former index,
including universe parameters and fixed prefix.   -/
Lean.Elab.Structural.IndGroupInst.brecOn : Lean.Elab.Structural.IndGroupInst → Lean.Level → ℕ → Lean.Expr
-- Mathlib.Algebra.Homology.SingleHomology
HomologicalComplex.singleObjCyclesSelfIso_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  (A : C) {Z : C} (h : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjCyclesSelfIso c j A).hom h =
    CategoryTheory.CategoryStruct.comp (((HomologicalComplex.single C c j).obj A).iCycles j)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf c j A).hom h)
-- Init.Tactics
/-- `mreplace` is like `replace`, but operating on a stateful `Std.Do.SPred` goal.
```lean
example (P Q : SPred σs) : P ⊢ₛ (P → Q) → Q := by
  mintro HP HPQ
  mreplace HPQ : Q := by mspecialize HPQ HP; mexact HPQ
  mexact HPQ
```
 -/
Lean.Parser.Tactic.mreplaceMacro : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
CategoryTheory.IsNormalMonoCategory.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C],
  (∀ {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f], Nonempty (CategoryTheory.NormalMono f)) →
    CategoryTheory.IsNormalMonoCategory C
-- Mathlib.Data.Finsupp.Multiset
Multiset.toFinsupp_sum_eq : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Multiset α), ((Multiset.toFinsupp s).sum fun x => id) = s.card
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.decodeSigma.match_3.eq_1 : ∀ (motive : (n : ℕ) → (f : Fin n → ℕ) → Fin (Fin.sum f) → Sort u_1) (x : Fin 0 → ℕ) (val : ℕ) (h : val < Fin.sum x)
  (h_1 : (x : Fin 0 → ℕ) → (val : ℕ) → (h : val < Fin.sum x) → motive 0 x ⟨val, h⟩)
  (h_2 : (n : ℕ) → (f : Fin (n + 1) → ℕ) → (x : ℕ) → (hx : x < Fin.sum f) → motive n.succ f ⟨x, hx⟩),
  (match 0, x, ⟨val, h⟩ with
    | 0, x, ⟨val, h⟩ => h_1 x val h
    | n.succ, f, ⟨x, hx⟩ => h_2 n f x hx) =
    h_1 x val h
-- Mathlib.NumberTheory.Zsqrtd.GaussianInt
GaussianInt.natAbs_norm_eq : ∀ (x : GaussianInt), (Zsqrtd.norm x).natAbs = x.re.natAbs * x.re.natAbs + x.im.natAbs * x.im.natAbs
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
MulAlgebraNorm.coe_AlgebraNorm : ∀ {R : outParam (Type u_1)} {S : outParam (Type u_2)} [inst : SeminormedCommRing R] [inst_1 : Ring S]
  [inst_2 : Algebra R S] (f : MulAlgebraNorm R S), ⇑f.toAlgebraNorm = ⇑f
-- Mathlib.AlgebraicGeometry.StructureSheaf
/-- We will define the structure sheaf as
the subsheaf of all dependent functions in `Π x : U, Localizations R x`
consisting of those functions which can locally be expressed as a ratio of
(the images in the localization of) elements of `R`.

Quoting Hartshorne:

For an open set $U ⊆ Spec A$, we define $𝒪(U)$ to be the set of functions
$s : U → ⨆_{𝔭 ∈ U} A_𝔭$, such that $s(𝔭) ∈ A_𝔭$ for each $𝔭$,
and such that $s$ is locally a quotient of elements of $A$:
to be precise, we require that for each $𝔭 ∈ U$, there is a neighborhood $V$ of $𝔭$,
contained in $U$, and elements $a, f ∈ A$, such that for each $𝔮 ∈ V, f ∉ 𝔮$,
and $s(𝔮) = a/f$ in $A_𝔮$.

Now Hartshorne had the disadvantage of not knowing about dependent functions,
so we replace his circumlocution about functions into a disjoint union with
`Π x : U, Localizations x`.
 -/
AlgebraicGeometry.StructureSheaf.isLocallyFraction : (R M : Type u) →
  [inst : CommRing R] →
    [inst_1 : AddCommGroup M] →
      [inst_2 : Module R M] → TopCat.LocalPredicate (AlgebraicGeometry.StructureSheaf.Localizations M)
-- Mathlib.Algebra.Module.Submodule.Basic
Submodule.toSubMulAction_mono : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Monotone Submodule.toSubMulAction
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
HurwitzZeta.completedCosZeta₀.eq_1 : ∀ (a : UnitAddCircle) (s : ℂ), HurwitzZeta.completedCosZeta₀ a s = (HurwitzZeta.hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2
-- Mathlib.MeasureTheory.Measure.Support
MeasureTheory.Measure.nonempty_support_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] {μ : MeasureTheory.Measure X}
  [HereditarilyLindelofSpace X], μ.support.Nonempty ↔ μ ≠ 0
-- Mathlib.Analysis.Convex.Exposed
exposedPoints_subset_extremePoints : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : TopologicalSpace 𝕜] [inst_1 : Ring 𝕜] [inst_2 : LinearOrder 𝕜]
  [IsStrictOrderedRing 𝕜] [inst_4 : AddCommMonoid E] [inst_5 : TopologicalSpace E] [inst_6 : Module 𝕜 E] {A : Set E},
  Set.exposedPoints 𝕜 A ⊆ Set.extremePoints 𝕜 A
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey?_union_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : α → Type v} {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → (m₁ ∪ m₂).getKey? k = m₁.getKey? k
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isEmpty_toArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp}, t.toArray.isEmpty = t.isEmpty
-- Mathlib.Analysis.Normed.Group.Basic
eq_one_or_norm_pos : ∀ {E : Type u_5} [inst : NormedGroup E] (a : E), a = 1 ∨ 0 < ‖a‖