mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.InnerProductSpace.l2Space
/-- The canonical linear isometry from the `lp 2` of a mutually orthogonal family of subspaces of
`E` into E, has range the closure of the span of the subspaces.  -/
OrthogonalFamily.range_linearIsometry : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] {G : ι → Type u_4} [inst_3 : (i : ι) → NormedAddCommGroup (G i)]
  [inst_4 : (i : ι) → InnerProductSpace 𝕜 (G i)] [inst_5 : CompleteSpace E] {V : (i : ι) → G i →ₗᵢ[𝕜] E}
  (hV : OrthogonalFamily 𝕜 G V) [∀ (i : ι), CompleteSpace (G i)],
  hV.linearIsometry.range = (⨆ i, (V i).range).topologicalClosure
-- Mathlib.AlgebraicTopology.SimplicialSet.Nerve
PartOrd.nerveFunctor_obj : ∀ (X : PartOrd), PartOrd.nerveFunctor.obj X = CategoryTheory.nerve ↑X
-- Mathlib.Data.Nat.Log
Nat.log_pos_iff : ∀ {b n : ℕ}, 0 < Nat.log b n ↔ b ≤ n ∧ 1 < b
-- Lean.Elab.InfoTree.Types
Lean.Elab.OptionInfo.stx : Lean.Elab.OptionInfo → Lean.Syntax
-- Mathlib.Order.Filter.Defs
Filter.NeBot.mk : ∀ {α : Type u_1} {f : Filter α}, f ≠ ⊥ → f.NeBot
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get_getKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp] {a : α}
  {h : (t.getKey? a).isSome = true}, (t.getKey? a).get h = t.getKey a ⋯
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
VectorField.mlieBracket_swap_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {x : M} {V W : (x : M) → TangentSpace I x},
  VectorField.mlieBracket I V W x = -VectorField.mlieBracket I W V x
-- Lean.Data.Lsp.Basic
Lean.Lsp.SnippetString.mk.inj : ∀ {value value_1 : String}, { value := value } = { value := value_1 } → value = value_1
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_roo_eq_singleton_append : ∀ {m n : ℕ}, m + 1 < n → (m<...n).toArray = #[m + 1] ++ ((m + 1)<...n).toArray
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Ioo_ae_eq_Icc' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : PartialOrder α] {a b : α},
  μ {a} = 0 → μ {b} = 0 → Set.Ioo a b =ᵐ[μ] Set.Icc a b
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.toMonoidHom_eq_coe : ∀ {M : Type u_4} {N : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] (f : M ≃* N), f.toMonoidHom = ↑f
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.mk.inj : ∀ {K : Type u} {inst : Field K} {toSubring : Subring K}
  {mem_or_inv_mem' : ∀ (x : K), x ∈ toSubring.carrier ∨ x⁻¹ ∈ toSubring.carrier} {toSubring_1 : Subring K}
  {mem_or_inv_mem'_1 : ∀ (x : K), x ∈ toSubring_1.carrier ∨ x⁻¹ ∈ toSubring_1.carrier},
  { toSubring := toSubring, mem_or_inv_mem' := mem_or_inv_mem' } =
      { toSubring := toSubring_1, mem_or_inv_mem' := mem_or_inv_mem'_1 } →
    toSubring = toSubring_1
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.Relation.below.symm : ∀ {J : Type v} [inst : CategoryTheory.Category.{u, v} J] {F : CategoryTheory.Functor J MonCat}
  {motive : (a a_1 : MonCat.Colimits.Prequotient F) → MonCat.Colimits.Relation F a a_1 → Prop}
  (x y : MonCat.Colimits.Prequotient F) (x_1 : MonCat.Colimits.Relation F x y),
  MonCat.Colimits.Relation.below x_1 → motive x y x_1 → MonCat.Colimits.Relation.below ⋯
-- Mathlib.CategoryTheory.Category.Pairwise
CategoryTheory.Pairwise.single.sizeOf_spec : ∀ {ι : Type v} [inst : SizeOf ι] (a : ι), sizeOf (CategoryTheory.Pairwise.single a) = 1 + sizeOf a
-- Batteries.Data.Fin.Coding
Fin.encodeEmpty_decodeEmpty : ∀ (x : Fin 0), Fin.encodeEmpty x.decodeEmpty = x
-- Mathlib.Data.Multiset.AddSub
/-- This is a special case of `tsub_zero`, which should be used instead of this.
This is needed to prove `OrderedSub (Multiset α)`.  -/
Multiset.sub_zero : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Multiset α), s - 0 = s
-- Mathlib.Data.TypeVec
TypeVec.eq_of_drop_last_eq : ∀ {n : ℕ} {α : TypeVec.{u_1} (n + 1)} {β : TypeVec.{u_2} (n + 1)} {f g : α.Arrow β},
  TypeVec.dropFun f = TypeVec.dropFun g → TypeVec.lastFun f = TypeVec.lastFun g → f = g
-- Mathlib.Data.Finset.Lattice.Basic
Finset.subset_union_left : ∀ {α : Type u_1} [inst : DecidableEq α] {s₁ s₂ : Finset α}, s₁ ⊆ s₁ ∪ s₂
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.coe_toContinuousAffineEquiv : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂), ⇑e.toContinuousAffineEquiv = ⇑e
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
/-- Universal property of the Cartesian product: Maps to `X ⊗ Y` correspond to pairs of maps to `X`
and to `Y`.  -/
CategoryTheory.CartesianMonoidalCategory.homEquivToProd : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {X Y Z : C} → (Z ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) ≃ (Z ⟶ X) × (Z ⟶ Y)
-- Init.Data.Format.Basic
_private.Init.Data.Format.Basic.0.Std.Format.be : {m : Type → Type} → ℕ → [Monad m] → [Std.Format.MonadPrettyFormat m] → List Std.Format.WorkGroup✝ → m Unit
-- Mathlib.Order.Heyting.Basic
/-- **Alias** of the reverse direction of `le_compl_iff_disjoint_left`. -/
Disjoint.le_compl_left : ∀ {α : Type u_2} [inst : HeytingAlgebra α] {a b : α}, Disjoint b a → a ≤ bᶜ
-- Mathlib.Data.NNReal.Defs
NNReal.mk.congr_simp : ∀ (x x_1 : ℝ) (e_x : x = x_1) (hx : 0 ≤ x), NNReal.mk x hx = NNReal.mk x_1 ⋯
-- Mathlib.Order.Defs.Unbundled
/-- **Alias** of `Equivalence.isTrans`. -/
Equivalence.transitive : ∀ {α : Sort u_1} (r : α → α → Prop), Equivalence r → IsTrans α r
-- Mathlib.Data.Nat.Log
Nat.log_lt_log_succ_iff : ∀ {b n : ℕ}, 1 < b → n ≠ 0 → (Nat.log b n < Nat.log b (n + 1) ↔ b ^ Nat.log b (n + 1) = n + 1)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.center_eq_top : ∀ (R : Type u_1) [inst : CommSemiring R], Subsemiring.center R = ⊤
-- Mathlib.LinearAlgebra.Dual.Lemmas
Subspace.comap_dualAnnihilator_dualAnnihilator : ∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] (W : Subspace K V),
  Submodule.comap (Module.Dual.eval K V) (Submodule.dualAnnihilator W).dualAnnihilator = W
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
ContinuousLinearMap.hasMFDerivWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_5} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E']
  (f : E →L[𝕜] E') {s : Set E} {x : E}, HasMFDerivAt[s] (⇑f) x f
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.CommGrp.forget_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X Y : CategoryTheory.CommGrp C} (f : X ⟶ Y),
  (CategoryTheory.CommGrp.forget C).map f = f.hom.hom.hom
-- Mathlib.Data.Set.Restrict
/-- **Alias** of `Set.domRestrict_id`. -/
Set.restrict_id : ∀ {α : Type u_1} (s : Set α), s.domRestrict id = Subtype.val
-- Init.Data.Int.Order
Int.sub_right_le_of_le_add : ∀ {a b c : ℤ}, a ≤ b + c → a - c ≤ b
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_inv : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} (α : F ⟶ G) {a b : B} {f g : a ⟶ b} (η : f ≅ g),
  (α.naturality g).inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (α.app a) (G.map₂ η.inv))
      (CategoryTheory.CategoryStruct.comp (α.naturality f).inv
        (CategoryTheory.Bicategory.whiskerRight (F.map₂ η.hom) (α.app b)))
-- Lean.Server.CodeActions.Attr
_private.Lean.Server.CodeActions.Attr.0.Lean.CodeAction.addBuiltin : Lean.Name → Array Lean.Name → Lean.AttrM Unit
-- Mathlib.Order.Antisymmetrization
AntisymmRel.setoid_r : ∀ (α : Type u_1) (r : α → α → Prop) [inst : IsPreorder α r] (a b : α), (AntisymmRel.setoid α r) a b = AntisymmRel r a b
-- Mathlib.RingTheory.Congruence.Hom
/-- The definition of the ring congruence relation defined by a ring homomorphism's kernel.  -/
RingCon.ker_apply : ∀ {M : Type u_1} {N : Type u_2} [inst : NonAssocSemiring M] [inst_1 : NonAssocSemiring N] (f : M →+* N) {x y : M},
  (RingCon.ker f) x y ↔ f x = f y
-- Mathlib.Geometry.Euclidean.Volume.Measure
IsometryEquiv.measurePreserving_euclideanHausdorffMeasure : ∀ {X : Type u_1} {Y : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X]
  [inst_3 : EMetricSpace Y] [inst_4 : MeasurableSpace Y] [inst_5 : BorelSpace Y] (e : X ≃ᵢ Y) (d : ℕ),
  MeasureTheory.MeasurePreserving (⇑e) (MeasureTheory.Measure.euclideanHausdorffMeasure d)
    (MeasureTheory.Measure.euclideanHausdorffMeasure d)
-- Init.Data.UInt.Bitwise
UInt64.xor_assoc : ∀ (a b c : UInt64), a ^^^ b ^^^ c = a ^^^ (b ^^^ c)
-- Mathlib.Data.Finset.Insert
Finset.nontrivial_def : ∀ {α : Type u_1} {s : Finset α}, s.Nontrivial ↔ ∃ a ∈ s, ∃ b ∈ s, a ≠ b
-- Mathlib.Algebra.Polynomial.Bivariate
/-- The notation `Y` for `X` in the `Polynomial` scope.  -/
Polynomial.Bivariate.termY : Lean.ParserDescr
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.aemeasurable : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β)
  {μ : MeasureTheory.Measure α}, AEMeasurable (⇑κ) μ
-- Std.Data.HashMap.Lemmas
Std.HashMap.mem_of_mem_filter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {f : α → β → Bool} {k : α}, k ∈ Std.HashMap.filter f m → k ∈ m
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.atMostAux : ℕ → Lean.Parser.ParserFn → String → Lean.Parser.ParserFn
-- Mathlib.LinearAlgebra.Eigenspace.Matrix
Matrix.spectrum_toLin : ∀ {R : Type u_1} {n : Type u_2} {M : Type u_3} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (A : Matrix n n R) (b : Module.Basis n R M),
  spectrum R ((Matrix.toLin b b) A) = spectrum R A
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
MulOpposite.instPseudoMetricSpace : {α : Type u_1} → [PseudoMetricSpace α] → PseudoMetricSpace αᵐᵒᵖ
-- Mathlib.Data.W.Basic
_private.Mathlib.Data.W.Basic.0.WType.f : {α : Type u_1} →
  {β : α → Type u_2} →
    [inst : (a : α) → Fintype (β a)] → (n : ℕ) → WType.WType'✝ β (n + 1) → (a : α) × (β a → WType.WType'✝ β n)
-- Init.Data.Int.Lemmas
Int.ofNat_mul_subNatNat : ∀ (m n k : ℕ), ↑m * Int.subNatNat n k = Int.subNatNat (m * n) (m * k)
-- Mathlib.Data.Set.Finite.Basic
Set.Infinite.preimage : ∀ {α : Type u} {β : Type v} {f : α → β} {s : Set β}, s.Infinite → s ⊆ Set.range f → (f ⁻¹' s).Infinite
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.liftCycles_comp_cyclesIso_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData) {A : C} (k : A ⟶ S.X₂)
  (hk : CategoryTheory.CategoryStruct.comp k S.g = 0) [inst_2 : S.HasLeftHomology],
  CategoryTheory.CategoryStruct.comp (S.liftCycles k hk) h.cyclesIso.hom = h.liftK k hk
-- Mathlib.RepresentationTheory.Continuous.Basic
/-- Given a monoid homomorphism `φ : H →* G`, a `G`-representation `π` and an
`H`-representation `π'`, a continuous intertwining map `f : π.restrict φ →ⁱL π'` induces a
continuous linear map `π.invariants →L[R] π'.invariants` between the invariant submodules.  -/
ContIntertwiningMap.mapInvariantsOfRes : {R : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Monoid G] →
          [inst_1 : Ring R] →
            [inst_2 : AddCommGroup V] →
              [inst_3 : TopologicalSpace V] →
                [inst_4 : IsTopologicalAddGroup V] →
                  [inst_5 : Module R V] →
                    [inst_6 : AddCommGroup W] →
                      [inst_7 : TopologicalSpace W] →
                        [inst_8 : IsTopologicalAddGroup W] →
                          [inst_9 : Module R W] →
                            {H : Type u_6} →
                              [inst_10 : Monoid H] →
                                {π : ContRepresentation R G V} →
                                  {π' : ContRepresentation R H W} →
                                    (φ : H →* G) →
                                      ContIntertwiningMap (π.restrict φ) π' → ↥π.invariants →L[R] ↥π'.invariants
-- Mathlib.RingTheory.FreeCommRing
FreeRing.coe_eq : ∀ (α : Type u), FreeRing.castFreeCommRing = Functor.map fun l => ↑l
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.LeftHomologyData.op_p : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData), h.op.p = h.i.op
-- Mathlib.Order.UpperLower.Closure
instDecidablePredMemLowerClosure.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} [inst_1 : DecidablePred fun x => ∃ a ∈ s, x ≤ a],
  instDecidablePredMemLowerClosure = inst_1
-- Mathlib.Algebra.BigOperators.Group.List.Defs
/-- The alternating product of a list.  -/
List.alternatingProd : {G : Type u_4} → [One G] → [Mul G] → [Inv G] → List G → G
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Flavors.zero.inj : ∀ {α : Type} {ch ch_1 : Std.CloseableChannel.Zero✝ α},
  Std.CloseableChannel.Flavors.zero✝ ch = Std.CloseableChannel.Flavors.zero✝ ch_1 → ch = ch_1
-- Mathlib.Probability.Distributions.Binomial
ProbabilityTheory.map_cast_binomial_zero : ∀ {R : Type u_1} [inst : MeasurableSpace R] [inst_1 : AddMonoidWithOne R] {p : ↑unitInterval},
  MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.binomial 0 p) = MeasureTheory.Measure.dirac 0
-- Mathlib.Data.ZMod.IntUnitsPower
uzpow_one : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : Module R (Additive ℤˣ)] (s : ℤˣ), s ^ 1 = s
-- Mathlib.Algebra.Notation.Indicator
Set.mulSupport_mulIndicator_subset : ∀ {α : Type u_1} {M : Type u_3} [inst : One M] {s : Set α} {f : α → M}, Function.mulSupport (s.mulIndicator f) ⊆ s
-- Mathlib.GroupTheory.PGroup
/-- The cardinality of the `center` of a `p`-group is `p ^ k` where `k` is positive.  -/
IsPGroup.card_center_eq_prime_pow : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] [Fact (Nat.Prime p)] {n : ℕ},
  Nat.card G = p ^ n → 0 < n → ∃ k > 0, Nat.card ↥(Subgroup.center G) = p ^ k
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.isEmpty_eq_false_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α],
  m.isEmpty = false ↔ ¬m = ∅
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
/-- The number of unramified places over an infinite place is equal to the number of unmixed
embeddings over the place.  -/
NumberField.InfinitePlace.unramifiedPlacesOver_ncard : ∀ {K : Type u_4} (L : Type u_5) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (v : NumberField.InfinitePlace K),
  (NumberField.InfinitePlace.unramifiedPlacesOver L v).ncard =
    (NumberField.ComplexEmbedding.unmixedEmbeddingsOver L v.embedding).ncard
-- Mathlib.RingTheory.MvPowerSeries.Equiv
MvPowerSeries.coeff_toAdicCompletion_val_apply_out : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : Finite σ] {x : σ →₀ ℕ} {p : MvPowerSeries σ R} {n : ℕ},
  Finsupp.degree x < n →
    MvPolynomial.coeff x (Quotient.out (↑((MvPowerSeries.toAdicCompletion σ R) p) n)) = (MvPowerSeries.coeff x) p
-- Mathlib.LinearAlgebra.Basis.Exact
/-- **Alias** of `Submodule.projectionOnto_comp_surjective_of_exact`. -/
Submodule.linearProjOfIsCompl_comp_surjective_of_exact : ∀ {R : Type u_1} {M : Type u_2} {K : Type u_3} {P : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup K] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R K] [inst_6 : Module R P]
  {f : K →ₗ[R] M} {g : M →ₗ[R] P},
  Function.Exact ⇑f ⇑g →
    ∀ {p q : Submodule R M} (hpq : IsCompl p q),
      Submodule.map g q = ⊤ → Function.Surjective ⇑(p.projectionOnto q hpq ∘ₗ f)
-- Mathlib.GroupTheory.Perm.Finite
Equiv.Set.union.congr_simp : ∀ {α : Type u_3} {s t : Set α} [inst : DecidablePred fun x => x ∈ s] (H : Disjoint s t),
  Equiv.Set.union H = Equiv.Set.union H
-- Mathlib.CategoryTheory.Presentable.Basic
/-- An object of a category is presentable relative to a universe `w`
if it is `κ`-presentable for some regular `κ : Cardinal.{w}`.  -/
CategoryTheory.IsPresentable : {C : Type u₁} → [CategoryTheory.Category.{v₁, u₁} C] → C → Prop
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.VectorsProdEqOne.card : ∀ (G : Type u_2) [inst : Group G] (n : ℕ) [inst_1 : Fintype G],
  Fintype.card ↑(Equiv.Perm.vectorsProdEqOne G n) = Fintype.card G ^ (n - 1)
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.sum_mapRange_index : ∀ {α : Type u_1} {M : Type u_8} {M' : Type u_9} {N : Type u_10} [inst : Zero M] [inst_1 : Zero M']
  [inst_2 : AddCommMonoid N] {f : M → M'} {hf : f 0 = 0} {g : α →₀ M} {h : α → M' → N},
  (∀ (a : α), h a 0 = 0) → (Finsupp.mapRange f hf g).sum h = g.sum fun a b => h a (f b)
-- Mathlib.CategoryTheory.Abelian.SerreClass.Localization
CategoryTheory.ObjectProperty.SerreClassLocalization.mono_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C)
  [inst_3 : P.IsSerreClass] [L.IsLocalization P.isoModSerre] [inst_5 : CategoryTheory.Preadditive D] [L.Additive]
  {X Y : D} (f : X ⟶ Y),
  CategoryTheory.Mono f ↔
    ∃ X' Y' f',
      ∃ (_ : CategoryTheory.Mono f'), Nonempty (CategoryTheory.Arrow.mk (L.map f') ≅ CategoryTheory.Arrow.mk f)
-- Mathlib.Tactic.Abel
/-- Apply the function `n : ∀ {α} [inst α], _` to the implicit parameters in the
context, and the given list of arguments.

Compared to `context.app`, this takes the name of the typeclass, rather than an
inferred typeclass instance.
 -/
Mathlib.Tactic.Abel.Context.mkApp : Mathlib.Tactic.Abel.Context → Lean.Name → Lean.Name → Array Lean.Expr → Lean.MetaM Lean.Expr
-- Init.Data.SInt.Basic
/-- Converts 8-bit signed integers to word-sized signed integers that denote the same number. This
conversion is lossless, because `ISize` is either `Int32` or `Int64`.

This function is overridden at runtime with an efficient implementation.
 -/
Int8.toISize : Int8 → ISize
-- Mathlib.Topology.Path
Path.refl_extend : ∀ {X : Type u_1} [inst : TopologicalSpace X] {a : X}, (Path.refl a).extend = ContinuousMap.const ℝ a
-- Mathlib.Topology.Category.UniformSpace
UniformSpaceCat.extensionHom_val : ∀ {X : UniformSpaceCat} {Y : CpltSepUniformSpace}
  (f : X ⟶ (CategoryTheory.forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y)
  (x : (UniformSpaceCat.completionFunctor.obj X).α),
  (CategoryTheory.ConcreteCategory.hom (UniformSpaceCat.extensionHom f)) x =
    UniformSpace.Completion.extension (⇑(CategoryTheory.ConcreteCategory.hom f)) x
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.getKey!_eq : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α] {k : α}, m₁.WF → m₂.WF → m₁.Equiv m₂ → m₁.getKey! k = m₂.getKey! k
-- Mathlib.Algebra.Homology.DerivedCategory.TStructure
/-- The canonical t-structure on `DerivedCategory C`.  -/
DerivedCategory.TStructure.t : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : HasDerivedCategory C] → CategoryTheory.Triangulated.TStructure (DerivedCategory C)
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.toSubgroupEquiv_neg_one : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B), HNNExtension.toSubgroupEquiv φ (-1) = φ.symm
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
/-- `fderivCompContinuousLinearMap` as a continuous linear map  -/
ContinuousAlternatingMap.fderivCompContinuousLinearMapCLM : {𝕜 : Type u} →
  {E : Type wE} →
    {F : Type wF} →
      (G : Type wG) →
        {ι : Type v} →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : SeminormedAddCommGroup E] →
              [inst_2 : NormedSpace 𝕜 E] →
                [inst_3 : SeminormedAddCommGroup F] →
                  [inst_4 : NormedSpace 𝕜 F] →
                    [inst_5 : SeminormedAddCommGroup G] →
                      [inst_6 : NormedSpace 𝕜 G] →
                        [Fintype ι] →
                          [DecidableEq ι] → (E →L[𝕜] F) → F [⋀^ι]→L[𝕜] G →L[𝕜] (E →L[𝕜] F) →L[𝕜] E [⋀^ι]→L[𝕜] G
-- Mathlib.Data.Set.Prod
Set.prod_subset_compl_diagonal_iff_disjoint : ∀ {α : Type u_1} {s t : Set α}, s ×ˢ t ⊆ (Set.diagonal α)ᶜ ↔ Disjoint s t
-- Mathlib.CategoryTheory.Linear.Basic
CategoryTheory.Linear.fullSubcategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {R : Type w} →
        [inst_2 : Semiring R] →
          [CategoryTheory.Linear R C] →
            (Z : CategoryTheory.ObjectProperty C) → CategoryTheory.Linear R Z.FullSubcategory
-- Mathlib.Analysis.Fourier.FourierTransform
Real.fourierInv_eq' : ∀ {V : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : MeasurableSpace V] [inst_5 : BorelSpace V] [inst_6 : FiniteDimensional ℝ V]
  (f : V → E) (w : V),
  FourierTransformInv.fourierInv f w = ∫ (v : V), Complex.exp (↑(2 * Real.pi * inner ℝ v w) * Complex.I) • f v
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
/-- Two isomorphic sheaves of modules have equivalent families of generating sections.  -/
SheafOfModules.GeneratingSections.equivOfIso : {C : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat] →
          [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] →
            {M N : SheafOfModules R} → (M ≅ N) → M.GeneratingSections ≃ N.GeneratingSections
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.image_symm : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] (f : P₁ ≃ᵃ[k] P₂) (s : Set P₂), ⇑f.symm '' s = ⇑f ⁻¹' s
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.divCoeffs.sizeOf_spec : ∀ (c : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.divCoeffs c) = 1 + sizeOf c
-- Mathlib.Logic.Function.FromTypes
/-- The definitional equality between `p`-ary heterogeneous functions into `τ`
and function from `vecHead p` to `(vecTail p)`-ary heterogeneous functions into `τ`.  -/
Function.fromTypes_succ_equiv : {n : ℕ} →
  (p : Fin (n + 1) → Type u) →
    (τ : Type u) → Function.FromTypes p τ ≃ (Matrix.vecHead p → Function.FromTypes (Matrix.vecTail p) τ)
-- Mathlib.Algebra.Group.Hom.Instances
instIsRightCancelAddZeroHom : ∀ {M : Type uM} {N : Type uN} [inst : Zero M] [inst_1 : AddZeroClass N] [IsRightCancelAdd N],
  IsRightCancelAdd (ZeroHom M N)
-- Lean.Server.Rpc.RequestHandling
_private.Lean.Server.Rpc.RequestHandling.0.Lean.Server.RpcProcedure.mk.inj : ∀ {wrapper wrapper_1 : UInt64 → Lean.Json → Lean.Server.RequestM (Lean.Server.RequestTask Lean.Json)},
  { wrapper := wrapper } = { wrapper := wrapper_1 } → wrapper = wrapper_1
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.ModEq.add_left_cancel' : ∀ {M : Type u_1} [inst : AddCancelCommMonoid M] {a b p : M} (c : M), c + a ≡ c + b [PMOD p] → a ≡ b [PMOD p]