mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.UniformSpace.UniformEmbedding
UniformContinuous.rangeFactorization : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
  UniformContinuous f → UniformContinuous (Set.rangeFactorization f)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.erase_empty : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {k : α}, ∅.erase k = ∅
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.smooth' : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] (self : SchwartzMap E F), ContDiff ℝ (↑⊤) self.toFun
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.sum_map_eq_nsmul_single : ∀ {α : Type u_2} {M : Type u_4} [inst : AddMonoid M] [inst_1 : DecidableEq α] {l : List α} (a : α) (f : α → M),
  (∀ (a' : α), a' ≠ a → a' ∈ l → f a' = 0) → (List.map f l).sum = List.count a l • f a
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
/-- An alternative formulation of `contMDiffWithinAt_iff_of_mem_maximalAtlas`
if the set `s` lies in `e.source`.  -/
contMDiffWithinAt_iff_image : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {e : OpenPartialHomeomorph M H}
  {e' : OpenPartialHomeomorph M' H'} {f : M → M'} {s : Set M} {x : M} {n : WithTop ℕ∞},
  e ∈ IsManifold.maximalAtlas I n M →
    e' ∈ IsManifold.maximalAtlas I' n M' →
      s ⊆ e.source →
        x ∈ e.source →
          f x ∈ e'.source →
            (ContMDiffWithinAt I I' n f s x ↔
              ContinuousWithinAt f s x ∧
                ContDiffWithinAt 𝕜 n (↑(e'.extend I') ∘ f ∘ ↑(e.extend I).symm) (↑(e.extend I) '' s) (↑(e.extend I) x))
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftLeft
Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeftConst.go.congr_simp : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (input input_1 : aig.RefVec w),
  input = input_1 →
    ∀ (distance distance_1 : ℕ),
      distance = distance_1 →
        ∀ (curr : ℕ) (hcurr : curr ≤ w) (s s_1 : aig.RefVec curr),
          s = s_1 →
            Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeftConst.go aig input distance curr hcurr s =
              Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeftConst.go aig input_1 distance_1 curr hcurr s_1
-- Init.Data.Order.Ord
List.instOrientedOrd : ∀ {α : Type u_1} [inst : Ord α] [Std.OrientedOrd α], Std.OrientedOrd (List α)
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.reindexRange.eq_1 : ∀ {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M),
  b.reindexRange =
    if h : Nontrivial R then b.reindex (Equiv.ofInjective ⇑b ⋯)
    else { repr := Module.subsingletonEquiv R M ↑(Set.range ⇑b) }
-- Mathlib.Analysis.Polynomial.Norm
/-- The sup norm of a polynomial on a semi-normed ring, defined as the maximum of its coefficients.
Often called the _(naive) height_ of the polynomial.

This is defined in terms of `Polynomial.gaussNorm`.  -/
Polynomial.supNorm : {A : Type u_1} → [inst : SeminormedRing A] → Polynomial A → ℝ
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
AffineSubspace.bot_ne_top : ∀ (k : Type u_1) (V : Type u_2) (P : Type u_3) [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P], ⊥ ≠ ⊤
-- Init.Data.Range.Polymorphic.SInt
Int64.instRxoIsAlwaysFinite : Std.Rxo.IsAlwaysFinite Int64
-- Mathlib.Order.SuccPred.Basic
instPredOrderOrderDualOfSuccOrder.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α],
  instPredOrderOrderDualOfSuccOrder =
    { pred := ⇑OrderDual.toDual ∘ SuccOrder.succ ∘ ⇑OrderDual.ofDual, pred_le := ⋯, min_of_le_pred := ⋯,
      le_pred_of_lt := ⋯ }
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.Hom.comp_id : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {P : Algebra.Generators R S ι} {R' : Type u_1} {S' : Type u_2} {ι' : Type u_3} [inst_3 : CommRing R']
  [inst_4 : CommRing S'] [inst_5 : Algebra R' S'] {P' : Algebra.Generators R' S' ι'} [inst_6 : Algebra R R']
  [inst_7 : Algebra S S'] [inst_8 : Algebra R S'] [inst_9 : IsScalarTower R R' S'] [inst_10 : IsScalarTower R S S']
  (f : P.Hom P'), f.comp (Algebra.Generators.Hom.id P) = f
-- Mathlib.Order.CompactlyGenerated.Basic
/-- In an atomic lattice, every element `b` has a complement of the form `sSup s`, where each
element of `s` is an atom. See also `complementedLattice_of_sSup_atoms_eq_top`.  -/
exists_sSupIndep_isCompl_sSup_atoms : ∀ {α : Type u_2} [inst : CompleteLattice α] [IsModularLattice α] [IsCompactlyGenerated α],
  sSup {a | IsAtom a} = ⊤ → ∀ (b : α), ∃ s, sSupIndep s ∧ IsCompl b (sSup s) ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a
-- Mathlib.AlgebraicGeometry.LimitsOver
AlgebraicGeometry.instIsOpenImmersionLeftSchemeDiscretePUnitMapWalkingSpanOverTopMorphismPropertySpan : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) {S : AlgebraicGeometry.Scheme} {U X Y : P.Over ⊤ S}
  (f : U ⟶ X) (g : U ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f.left] [AlgebraicGeometry.IsOpenImmersion g.left]
  {i j : CategoryTheory.Limits.WalkingSpan} (t : i ⟶ j),
  AlgebraicGeometry.IsOpenImmersion ((CategoryTheory.Limits.span f g).map t).left
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.forInStep.match_1.eq_1 : ∀ {δ : Type u_1} (motive : ForInStep δ → Sort u_2) (d : δ) (h_1 : (d : δ) → motive (ForInStep.done d))
  (h_2 : (d : δ) → motive (ForInStep.yield d)),
  (match ForInStep.done d with
    | ForInStep.done d => h_1 d
    | ForInStep.yield d => h_2 d) =
    h_1 d
-- Mathlib.Analysis.Normed.Group.Quotient
/-- An alternative definition of the norm on the quotient group: the norm of `((x : M) : M ⧸ S)` is
equal to the distance from `x` to `S`.  -/
QuotientGroup.norm_mk : ∀ {M : Type u_1} [inst : SeminormedCommGroup M] {S : Subgroup M} (x : M), ‖↑x‖ = Metric.infDist x ↑S
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- Given three points in weak order on the same line, with the second not equal to the third,
and a fourth point, the angles at the fourth point between the second and third or first and
third points have the same sign.  -/
Wbtw.oangle_sign_eq_of_ne_right : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P} (p₄ : P),
  Wbtw ℝ p₁ p₂ p₃ → p₂ ≠ p₃ → (EuclideanGeometry.oangle p₂ p₄ p₃).sign = (EuclideanGeometry.oangle p₁ p₄ p₃).sign
-- Mathlib.Topology.MetricSpace.Algebra
LipschitzMul.continuousMul : ∀ {β : Type u_2} [inst : PseudoMetricSpace β] [inst_1 : Monoid β] [LipschitzMul β], ContinuousMul β
-- Mathlib.Topology.Algebra.Monoid
Filter.Tendsto.val_addUnits : ∀ {ι : Type u_1} {N : Type u_4} [inst : TopologicalSpace N] [inst_1 : AddMonoid N] [inst_2 : ContinuousAdd N]
  [inst_3 : T2Space N] {f : ι → AddUnits N} {r₁ r₂ : N} {l : Filter ι} [inst_4 : l.NeBot]
  (h₁ : Filter.Tendsto (fun x => ↑(f x)) l (nhds r₁)) (h₂ : Filter.Tendsto (fun x => ↑(-f x)) l (nhds r₂)),
  ↑(h₁.addUnits h₂) = r₁
-- Mathlib.Analysis.Complex.Conformal
ContinuousLinearMap.complexOfReal.congr_simp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (ℓ ℓ_1 : ℂ →L[ℝ] E) (e_ℓ : ℓ = ℓ_1)
  (h : ℓ Complex.I = Complex.I • ℓ 1), ℓ.complexOfReal h = ℓ_1.complexOfReal ⋯
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion
SemiNormedGrp.completion_obj_carrier : ∀ (V : SemiNormedGrp), (SemiNormedGrp.completion.obj V).carrier = UniformSpace.Completion V.carrier
-- Mathlib.ModelTheory.Arithmetic.Presburger.Definability
FirstOrder.Language.presburger.isSemilinearSet_boundedFormula_realize : ∀ {α : Type u_1} {A : Set ℕ} [Finite α] {n : ℕ}
  (φ : (FirstOrder.Language.presburger.withConstants ↑A).BoundedFormula α n),
  IsSemilinearSet {v | φ.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)}
-- Mathlib.Order.DirectedInverseSystem
InverseSystem.pEquivOn_apply_eq : ∀ {ι : Type u_6} {F : ι → Type u_7} {X : ι → Type u_8} [inst : LinearOrder ι] {f : ⦃i j : ι⦄ → i ≤ j → F j → F i}
  [inst_1 : SuccOrder ι] {equivSucc : ⦃i : ι⦄ → ¬IsMax i → F (Order.succ i) ≃ F i × X i} {s t : Set ι}
  [WellFoundedLT ι],
  IsLowerSet (s ∩ t) →
    ∀ {e₁ : InverseSystem.PEquivOn f equivSucc s} {e₂ : InverseSystem.PEquivOn f equivSucc t} {i : ι} {his : i ∈ s}
      {hit : i ∈ t}, e₁.equiv ⟨i, his⟩ = e₂.equiv ⟨i, hit⟩
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.Matroidᵣ.coe_inj : ∀ {α : Type u_1} {M₁ M₂ : Matroid.Matroidᵣ α}, M₁.toMatroid = M₂.toMatroid ↔ M₁ = M₂
-- Mathlib.Algebra.BigOperators.Finprod
finsum_emb_domain' : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] {f : α → β},
  Function.Injective f →
    ∀ [inst_1 : DecidablePred fun x => x ∈ Set.range f] (g : α → M),
      (∑ᶠ (b : β), if h : b ∈ Set.range f then g (Classical.choose h) else 0) = ∑ᶠ (a : α), g a
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.nthRootsFinset_toSet : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] {n : ℕ},
  0 < n → ∀ (a : R), ↑(Polynomial.nthRootsFinset n a) = {r | r ^ n = a}
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.normAtAllPlaces_image_preimage_of_nonneg : ∀ {K : Type u_1} [inst : Field K] {s : Set (NumberField.mixedEmbedding.realSpace K)},
  (∀ x ∈ s, ∀ (w : NumberField.InfinitePlace K), 0 ≤ x w) →
    NumberField.mixedEmbedding.normAtAllPlaces '' NumberField.mixedEmbedding.normAtAllPlaces ⁻¹' s = s
-- Mathlib.Algebra.Exact.Basic
Function.Exact.linearEquivOfSurjective_symm_apply : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {P : Type u_6} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R P]
  {f : M →ₗ[R] N} {g : N →ₗ[R] P} (h : Function.Exact ⇑f ⇑g) (hg : Function.Surjective ⇑g) (x : N),
  (h.linearEquivOfSurjective hg).symm (g x) = Submodule.Quotient.mk x
-- Mathlib.RepresentationTheory.Subrepresentation
/-- An order-preserving equivalence between subrepresentations of `ρ` and submodules of
`ρ.asModule`.  -/
Subrepresentation.subrepresentationSubmoduleOrderIso : {A : Type u_1} →
  {G : Type u_2} →
    {W : Type u_3} →
      [inst : CommSemiring A] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommMonoid W] →
            [inst_3 : Module A W] →
              {ρ : Representation A G W} → Subrepresentation ρ ≃o Submodule (MonoidAlgebra A G) ρ.asModule
-- Init.Data.UInt.Lemmas
UInt32.mul_one : ∀ (a : UInt32), a * 1 = a
-- Mathlib.NumberTheory.PowModTotient
Nat.pow_add_totient_mod_eq : ∀ {x k n : ℕ}, 1 < n → x.Coprime n → x ^ (k + n.totient) % n = x ^ k % n
-- Aesop.Search.Expansion
Aesop.SafeRulesResult.proved.inj : ∀ {newRapps newRapps_1 : Array Aesop.RappRef},
  Aesop.SafeRulesResult.proved newRapps = Aesop.SafeRulesResult.proved newRapps_1 → newRapps = newRapps_1
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.quasiSober : ∀ {R : Type u} [inst : CommSemiring R], QuasiSober (PrimeSpectrum R)
-- Mathlib.LinearAlgebra.PiTensorProduct.DirectSum
/-- The n-ary tensor product distributes over m-ary direct sums.  -/
PiTensorProduct.ofDirectSumEquiv : {R : Type u_1} →
  {ι : Type u_2} →
    {κ : ι → Type u_3} →
      {M : (i : ι) → κ i → Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)] →
            [inst_2 : (i : ι) → (j : κ i) → Module R (M i j)] →
              [Finite ι] →
                (PiTensorProduct R fun i => DirectSum (κ i) fun j => M i j) ≃ₗ[R]
                  DirectSum ((i : ι) → κ i) fun p => PiTensorProduct R fun i => M i (p i)
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.divides_sq_eq_zero : ∀ {d : ℕ} [dnsq : Zsqrtd.Nonsquare d] {x y : ℕ}, x * x = d * y * y → x = 0 ∧ y = 0
-- Std.Data.DTreeMap.AdditionalOperations
/-- Given a proof that such a mapping exists, retrieves the largest key that is
less than the given key.
 -/
Std.DTreeMap.getKeyLT : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] → (t : Std.DTreeMap α β cmp) → (k : α) → (∃ a ∈ t, cmp a k = Ordering.lt) → α
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
log_riemannZeta_add_log_sub_isBigO_ofReal : (fun s => Real.log (riemannZeta ↑s).re + Real.log (s - 1)) =O[nhdsWithin 1 (Set.Ioi 1)] fun x => x - 1
-- Mathlib.LinearAlgebra.FixedSubmodule
/-- The linear equivalence deduced from `e : V ≃ₗ[R] V`
by passing to the quotient by `e.fixedSubmodule`.  -/
LinearEquiv.fixedReduce : {R : Type u_4} →
  {V : Type u_5} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module R V] → (e : V ≃ₗ[R] V) → (V ⧸ (↑e).fixedSubmodule) ≃ₗ[R] V ⧸ (↑e).fixedSubmodule
-- Batteries.Data.List.Lemmas
List.isChain_range' : ∀ (s n step : ℕ), List.IsChain (fun a b => b = a + step) (List.range' s n step)
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.inclLiftToInitial_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsInitial Z) (x : C),
  (CategoryTheory.WithInitial.inclLiftToInitial F hZ).hom.app x =
    CategoryTheory.CategoryStruct.id
      (match CategoryTheory.WithInitial.incl.obj x with
      | CategoryTheory.WithInitial.of x => F.obj x
      | CategoryTheory.WithInitial.star => Z)
-- Mathlib.Algebra.Field.IsField
/-- For a semiring to be a field, it must have two distinct elements.  -/
IsField.exists_pair_ne : ∀ {R : Type u} [inst : Semiring R], IsField R → ∃ x y, x ≠ y
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.mem_add : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α] {s t : Finset α} {x : α},
  x ∈ s + t ↔ ∃ y ∈ s, ∃ z ∈ t, y + z = x
-- Mathlib.CategoryTheory.Shift.CommShift
/-- **Alias** of `CategoryTheory.Functor.CommShift.id_commShiftIso_inv_app`. -/
CategoryTheory.Functor.commShiftIso_id_inv_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u_4} [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (x : A) (X : C),
  (CategoryTheory.Functor.commShiftIso (CategoryTheory.Functor.id C) x).inv.app X =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.shiftFunctor C x).obj X)
-- Init.Data.Fin.Lemmas
Fin.le_coe_natAdd : ∀ {n : ℕ} (m : ℕ) (i : Fin n), m ≤ ↑(Fin.natAdd m i)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- The function `f ↦ cfcₙ f a` is Lipschitz with constant 1 with respect to
supremum metric (on `R →ᵤ[{s}] R`) on those functions which are continuous on a set `s` containing
the quasispectrum and map zero to itself.  -/
lipschitzOnWith_cfcₙ_fun_of_subset : ∀ {R : Type u_2} {A : Type u_3} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : Nontrivial R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : MetricSpace A] [inst_9 : Module R A] [inst_10 : SMulCommClass R A A]
  [inst_11 : IsScalarTower R A A] [inst_12 : NonUnitalIsometricContinuousFunctionalCalculus R A p] (a : A) {s : Set R},
  quasispectrum R a ⊆ s →
    LipschitzOnWith 1 (fun f => cfcₙ ((UniformOnFun.toFun {s}) f) a)
      {f | ContinuousOn ((UniformOnFun.toFun {s}) f) s ∧ f 0 = 0}
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.mk.sizeOf_spec : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : Group N] [inst_1 : Group E] [inst_2 : Group G]
  [inst_3 : SizeOf N] [inst_4 : SizeOf E] [inst_5 : SizeOf G] (inl : N →* E) (rightHom : E →* G)
  (inl_injective : Function.Injective ⇑inl) (range_inl_eq_ker_rightHom : inl.range = rightHom.ker)
  (rightHom_surjective : Function.Surjective ⇑rightHom),
  sizeOf
      { inl := inl, rightHom := rightHom, inl_injective := inl_injective,
        range_inl_eq_ker_rightHom := range_inl_eq_ker_rightHom, rightHom_surjective := rightHom_surjective } =
    1 + sizeOf inl + sizeOf rightHom + sizeOf range_inl_eq_ker_rightHom
-- Mathlib.Topology.Irreducible
Topology.IsOpenEmbedding.preirreducibleSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : Y → X},
  Topology.IsOpenEmbedding f → ∀ [PreirreducibleSpace X], PreirreducibleSpace Y
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
/-- **Alias** of `AffineEquiv.coe_pointReflection`. -/
AffineEquiv.pointReflection_apply_eq_equivPointReflection_apply : ∀ (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] (x y : P₁), (AffineEquiv.pointReflection k x) y = (Equiv.pointReflection x) y
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.CanonArgKey.mk.inj : ∀ {f : Lean.Expr} {i : ℕ} {arg f_1 : Lean.Expr} {i_1 : ℕ} {arg_1 : Lean.Expr},
  { f := f, i := i, arg := arg } = { f := f_1, i := i_1, arg := arg_1 } → f = f_1 ∧ i = i_1 ∧ arg = arg_1
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
Multipliable.tprod_prod_uncurry : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] [ContinuousMul α]
  [T3Space α] {f : β → γ → α},
  Multipliable (Function.uncurry f) →
    (∀ (b : β), Multipliable fun c => f b c) → ∏' (p : β × γ), Function.uncurry f p = ∏' (b : β) (c : γ), f b c
-- Mathlib.CategoryTheory.Comma.Arrow
/-- A morphism in the arrow category is a commutative square connecting two objects of the arrow
category.  -/
CategoryTheory.Arrow.homMk : {T : Type u} →
  [inst : CategoryTheory.Category.{v, u} T] →
    {f g : CategoryTheory.Arrow T} →
      (u : f.left ⟶ g.left) →
        (v : f.right ⟶ g.right) →
          autoParam (CategoryTheory.CategoryStruct.comp u g.hom = CategoryTheory.CategoryStruct.comp f.hom v)
              CategoryTheory.Arrow.homMk._auto_1 →
            (f ⟶ g)
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.ins.match_3.eq_1 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (h_1 : Unit → motive RBTree.RBNode.nil)
  (h_2 : (a : RBTree.RBNode α) → (y : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.red a y b))
  (h_3 :
    (a : RBTree.RBNode α) → (y : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.black a y b)),
  (match RBTree.RBNode.nil with
    | RBTree.RBNode.nil => h_1 ()
    | RBTree.RBNode.node RBTree.RBColor.red a y b => h_2 a y b
    | RBTree.RBNode.node RBTree.RBColor.black a y b => h_3 a y b) =
    h_1 ()
-- Mathlib.Topology.MetricSpace.PiNat
/-- Any nonempty complete second countable metric space is the continuous image of the
fundamental space `ℕ → ℕ`. For a version of this theorem in the context of Polish spaces, see
`exists_nat_nat_continuous_surjective_of_polishSpace`.  -/
exists_nat_nat_continuous_surjective_of_completeSpace : ∀ (α : Type u_2) [inst : MetricSpace α] [CompleteSpace α] [SecondCountableTopology α] [Nonempty α],
  ∃ f, Continuous f ∧ Function.Surjective f
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.contains_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : BEq α]
  [Std.LawfulBEqCmp cmp] [Std.TransCmp cmp] {k : α}, t.keys.contains k = t.contains k
-- Init.Data.BitVec.Lemmas
BitVec.msb_and : ∀ {w : ℕ} {x y : BitVec w}, (x &&& y).msb = (x.msb && y.msb)
-- Mathlib.Order.Bounds.Image
Antitone.mem_upperBounds_image : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Antitone f → ∀ {a : α} {s : Set α}, a ∈ lowerBounds s → f a ∈ upperBounds (f '' s)
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.NumDenSameDeg.num_zero : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubmonoidClass σ A] {𝒜 : ι → σ} (x : Submonoid A) [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι]
  [inst_5 : GradedRing 𝒜], HomogeneousLocalization.NumDenSameDeg.num 0 = 0
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.instInhabited.eq_1 : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S],
  AddOreLocalization.instInhabited = { default := 0 }
-- Std.Http.Data.URI.Encoding
_private.Std.Http.Data.URI.Encoding.0.Std.Http.URI.List.toByteArray_loop_eq : ∀ (xs : List UInt8) (acc : ByteArray), (List.toByteArray.loop xs acc).data = acc.data ++ xs.toArray
-- Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
RootPairing.forall_pairingIn_eq_swap_or : ∀ {ι : 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 : RootPairing ι R M N) [Finite ι]
  [CharZero R] [inst_7 : P.IsCrystallographic] [IsDomain R] [P.IsReduced] [P.IsIrreducible],
  (∀ (i j : ι),
      P.pairingIn ℤ i j = P.pairingIn ℤ j i ∨
        P.pairingIn ℤ i j = 2 * P.pairingIn ℤ j i ∨ P.pairingIn ℤ j i = 2 * P.pairingIn ℤ i j) ∨
    ∀ (i j : ι),
      P.pairingIn ℤ i j = P.pairingIn ℤ j i ∨
        P.pairingIn ℤ i j = 3 * P.pairingIn ℤ j i ∨ P.pairingIn ℤ j i = 3 * P.pairingIn ℤ i j
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
MeasurableSet.Subtype.instInsert : {α : Type u_1} → [inst : MeasurableSpace α] → [MeasurableSingletonClass α] → Insert α (Subtype MeasurableSet)
-- Mathlib.Algebra.Group.Equiv.TypeTags
MulEquiv.toMultiplicative_toAdditive_apply : ∀ {G : Type u_2} [inst : MulOneClass G] (a : Multiplicative (Additive G)),
  MulEquiv.toMultiplicative_toAdditive a = Additive.toMul (Multiplicative.toAdd a)
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
/-- An antilinear isometric embedding of a normed `R`-module into another one.  -/
«term_→ₗᵢ⋆[_]_» : Lean.TrailingParserDescr
-- Mathlib.Data.Prod.Lex
Prod.Lex.noMaxOrder_of_left : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [NoMaxOrder α], NoMaxOrder (Lex (α × β))
-- Mathlib.CategoryTheory.Monoidal.Subcategory
CategoryTheory.ObjectProperty.ι_ε : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsMonoidal],
  CategoryTheory.Functor.LaxMonoidal.ε P.ι =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Complex.differentiableAt_cos : ∀ {x : ℂ}, DifferentiableAt ℂ Complex.cos x
-- Mathlib.Algebra.Module.End
AddMonoid.End.natCast_def : ∀ {M : Type u_3} [inst : AddCommMonoid M] (n : ℕ), ↑n = (DistribMulAction.toAddMonoidEnd ℕ M) n
-- Mathlib.RingTheory.Valuation.Discrete.Basic
/-- Given a linearly ordered commutative group with zero `Γ` such that `Γˣ` is
nontrivial cyclic, a valuation `v : A → Γ` on a ring `A` is *discrete*, if
`genLTOne Γˣ` belongs to the image. Note that the latter is equivalent to
asking that `1 : ℤ` belongs to the image of the corresponding additive valuation.  -/
Valuation.IsRankOneDiscrete : {Γ : Type u_1} → [inst : LinearOrderedCommGroupWithZero Γ] → {A : Type u_2} → [inst_1 : Ring A] → Valuation A Γ → Prop
-- Mathlib.Algebra.Homology.Factorizations.CM5b
CochainComplex.cm5b.i_f_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.EnoughInjectives C] {K L : CochainComplex C ℤ} (f : K ⟶ L) (n : ℤ),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.cm5b.i f).f n)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.fst.f n)
        ((CochainComplex.mappingCone.snd (CategoryTheory.CategoryStruct.id (CochainComplex.cm5b.I K))).v n n ⋯)) =
    CategoryTheory.Injective.ι (K.X n)