mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Logic.Function.Basic
/-- Shorthand for using projection notation with `Function.bijective_iff_existsUnique`.  -/
Function.Bijective.existsUnique : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β}, Function.Bijective f → ∀ (b : β), ∃! a, f a = b
-- Init.Data.Nat.Div.Basic
/-- Division of two divisible natural numbers. Division by `0` returns `0`.

This operation uses an optimized implementation, specialized for two divisible natural numbers.

This function is overridden at runtime with an efficient implementation. This definition is
the logical model.

Examples:
 * `Nat.divExact 21 3 (by decide) = 7`
 * `Nat.divExact 0 22 (by decide) = 0`
 * `Nat.divExact 0 0 (by decide) = 0`
 -/
Nat.divExact : (x y : ℕ) → y ∣ x → ℕ
-- Init.Grind.Ring.Field
Lean.Grind.Field.zpow_one : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] (a : α), a ^ 1 = a
-- Mathlib.Data.Num.Lemmas
_private.Mathlib.Data.Num.Lemmas.0.PosNum.cmp.match_1.eq_7 : ∀ (motive : PosNum → PosNum → Sort u_1) (a b : PosNum) (h_1 : Unit → motive PosNum.one PosNum.one)
  (h_2 : (x : PosNum) → motive x PosNum.one) (h_3 : (x : PosNum) → motive PosNum.one x)
  (h_4 : (a b : PosNum) → motive a.bit0 b.bit0) (h_5 : (a b : PosNum) → motive a.bit0 b.bit1)
  (h_6 : (a b : PosNum) → motive a.bit1 b.bit0) (h_7 : (a b : PosNum) → motive a.bit1 b.bit1),
  (match a.bit1, b.bit1 with
    | PosNum.one, PosNum.one => h_1 ()
    | x, PosNum.one => h_2 x
    | PosNum.one, x => h_3 x
    | a.bit0, b.bit0 => h_4 a b
    | a.bit0, b.bit1 => h_5 a b
    | a.bit1, b.bit0 => h_6 a b
    | a.bit1, b.bit1 => h_7 a b) =
    h_7 a b
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.ε_hom : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G],
  Rep.Hom.hom (CategoryTheory.Functor.LaxMonoidal.ε (Rep.linearization k G)) = Representation.LinearizeMonoidal.ε k G
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
HomologicalComplex.shortComplexFunctor'.eq_1 : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} (c : ComplexShape ι) (i j k : ι),
  HomologicalComplex.shortComplexFunctor' C c i j k =
    { obj := fun K => { X₁ := K.X i, X₂ := K.X j, X₃ := K.X k, f := K.d i j, g := K.d j k, zero := ⋯ },
      map := fun {X Y} f => { τ₁ := f.f i, τ₂ := f.f j, τ₃ := f.f k, comm₁₂ := ⋯, comm₂₃ := ⋯ }, map_id := ⋯,
      map_comp := ⋯ }
-- Mathlib.FieldTheory.NormalizedTrace
/-- The normalized trace commutes with (injective) maps.  -/
Algebra.normalizedTrace_comp_algHom : ∀ (F : Type u_1) (K : Type u_2) [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K] [inst_3 : CharZero F]
  [inst_4 : Algebra.IsIntegral F K] {E : Type u_3} [inst_5 : Field E] [inst_6 : Algebra F E]
  [inst_7 : Algebra.IsIntegral F E] (f : E →ₐ[F] K), Algebra.normalizedTrace F K ∘ₗ ↑f = Algebra.normalizedTrace F E
-- Mathlib.Algebra.Group.Equiv.TypeTags
/-- `Additive (ι → G)` is equivalent to `ι → Additive G`.  -/
AddEquiv.funAdditive : (ι : Type u_1) → (G : Type u_2) → [inst : Mul G] → Additive (ι → G) ≃+ (ι → Additive G)
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
LinearIndependent.units_smul_iff : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (v : ι → M) (w : ι → Rˣ), LinearIndependent R (w • v) ↔ LinearIndependent R v
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- The sum of the composition of functions `f` and `g`, is the sum over
`b ∈ s.image g` of `f b` times of the cardinality of the fibre of `b`. See also
`Finset.sum_image`.  -/
Finset.sum_comp : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} {s : Finset ι} [inst : AddCommMonoid M] [inst_1 : DecidableEq κ]
  (f : κ → M) (g : ι → κ), ∑ a ∈ s, f (g a) = ∑ b ∈ Finset.image g s, {a ∈ s | g a = b}.card • f b
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.support_cycleOf_nonempty : ∀ {α : Type u_2} {f : Equiv.Perm α} {x : α} [inst : DecidableEq α] [inst_1 : Fintype α],
  (f.cycleOf x).support.Nonempty ↔ f x ≠ x
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.app_eq : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U V : Y.Opens} (e : U = V),
  AlgebraicGeometry.Scheme.Hom.app f U =
    CategoryTheory.CategoryStruct.comp (Y.presheaf.map (CategoryTheory.eqToHom ⋯).op)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app f V)
        (X.presheaf.map (CategoryTheory.eqToHom ⋯).op))
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.Indep.cardinalMk_le_isBasis : ∀ {α : Type u} {M : Matroid α} {I J X : Set α} [M.InvariantCardinalRank],
  M.Indep I → M.IsBasis J X → I ⊆ X → Cardinal.mk ↑I ≤ Cardinal.mk ↑J
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_insertMany_list : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] [inst : BEq α]
  [Std.LawfulBEqOrd α] (h : t.WF) {l : List ((a : α) × β a)} {k : α},
  Std.DTreeMap.Internal.Impl.contains k ↑(t.insertMany l ⋯) =
    (Std.DTreeMap.Internal.Impl.contains k t || (List.map Sigma.fst l).contains k)
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.beth_limit : ∀ {o : Ordinal.{u_1}}, Order.IsSuccLimit o → Cardinal.beth o = ⨆ a, Cardinal.beth ↑a
-- Mathlib.Algebra.Group.Action.Basic
isCancelVAdd_iff_eq_zero_of_vadd_eq : ∀ {α : Type u_5} {β : Type u_6} [inst : AddGroup α] [inst_1 : AddAction α β],
  IsCancelVAdd α β ↔ ∀ (g : α) (x : β), g +ᵥ x = x → g = 0
-- Mathlib.Order.Interval.Set.WithBotTop
WithTop.image_coe_Ioo : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, WithTop.some '' Set.Ioo a b = Set.Ioo ↑a ↑b
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
MeasureTheory.Measure.ae_compProd_iff : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {κ : ProbabilityTheory.Kernel α β} [MeasureTheory.SFinite μ] [ProbabilityTheory.IsSFiniteKernel κ] {p : α × β → Prop},
  MeasurableSet {x | p x} → ((∀ᵐ (x : α × β) ∂μ.compProd κ, p x) ↔ ∀ᵐ (a : α) ∂μ, ∀ᵐ (b : β) ∂κ a, p (a, b))
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
SimpleGraph.Walk.mapLe_append : ∀ {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u v w : V} (p : G.Walk u v) (q : G.Walk v w),
  SimpleGraph.Walk.mapLe h (p.append q) = (SimpleGraph.Walk.mapLe h p).append (SimpleGraph.Walk.mapLe h q)
-- Mathlib.Topology.Irreducible
IsIrreducible.isPreirreducible : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsIrreducible s → IsPreirreducible s
-- Mathlib.RingTheory.Extension.Generators
/-- Construct `Generators` from an assignment `I → S` such that `R[X] → S` is surjective.  -/
Algebra.Generators.ofSurjective : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : Algebra R S] →
            (val : ι → S) → Function.Surjective ⇑(MvPolynomial.aeval val) → Algebra.Generators R S ι
-- Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise
ContDiffPointwiseHolderAt.continuousAt : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {f : E → F} {a : E},
  ContDiffPointwiseHolderAt k α f a → ContinuousAt f a
-- Mathlib.Topology.Algebra.Group.Basic
Filter.map_subRight_nhdsLT : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : AddCommGroup H] [IsTopologicalAddGroup H] [inst_3 : PartialOrder H]
  [IsOrderedAddMonoid H] {c a : H},
  Filter.map (fun x => x - c) (nhdsWithin a (Set.Iio a)) = nhdsWithin (a - c) (Set.Iio (a - c))
-- Mathlib.Combinatorics.SimpleGraph.Prod
SimpleGraph.connected_boxProd : ∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β}, (G □ H).Connected ↔ G.Connected ∧ H.Connected
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.smul_toProd : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A] {S : Type u_3}
  [inst_5 : Monoid S] [inst_6 : DistribMulAction S A] [inst_7 : SMulCommClass 𝕜 S A] [inst_8 : ContinuousConstSMul S A]
  [inst_9 : IsScalarTower S A A] [inst_10 : SMulCommClass S A A] (s : S) (a : DoubleCentralizer 𝕜 A),
  (s • a).toProd = s • a.toProd
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.Congruence.toIsStableUnderPrecomp : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {r : HomRel C} [self : CategoryTheory.Congruence r],
  CategoryTheory.HomRel.IsStableUnderPrecomp r
-- Mathlib.Data.Finset.Finsupp
/-- Given a finitely supported function `f : ι →₀ Finset α`, one can define the finset
`f.pi` of all finitely supported functions whose value at `i` is in `f i` for all `i`.  -/
Finsupp.pi : {ι : Type u_1} → {α : Type u_2} → [inst : Zero α] → (ι →₀ Finset α) → Finset (ι →₀ α)
-- Lean.Hygiene
Lean.NameSanitizerState.mk.inj : ∀ {options : Lean.Options} {nameStem2Idx : Lean.NameMap ℕ} {userName2Sanitized : Lean.NameMap Lean.Name}
  {options_1 : Lean.Options} {nameStem2Idx_1 : Lean.NameMap ℕ} {userName2Sanitized_1 : Lean.NameMap Lean.Name},
  { options := options, nameStem2Idx := nameStem2Idx, userName2Sanitized := userName2Sanitized } =
      { options := options_1, nameStem2Idx := nameStem2Idx_1, userName2Sanitized := userName2Sanitized_1 } →
    options = options_1 ∧ nameStem2Idx = nameStem2Idx_1 ∧ userName2Sanitized = userName2Sanitized_1
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.support_map : ∀ {V : Type u_1} {W : Type u_2} (f : V ↪ W) (G : SimpleGraph V), (SimpleGraph.map (⇑f) G).support = ⇑f '' G.support
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd
/-- The quotient functor from `Arrow V` to `RightFreyd V`.  -/
CategoryTheory.Preadditive.RightFreyd.quotient : (V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    [inst_1 : CategoryTheory.Preadditive V] →
      CategoryTheory.Functor (CategoryTheory.Arrow V) (CategoryTheory.Preadditive.RightFreyd V)
-- Mathlib.Data.List.Cycle
Cycle.map_eq_nil : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Cycle α), Cycle.map f s = Cycle.nil ↔ s = Cycle.nil
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- An angle in a right-angled triangle expressed using `arcsin`.  -/
InnerProductGeometry.angle_add_eq_arcsin_of_inner_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  inner ℝ x y = 0 → x ≠ 0 ∨ y ≠ 0 → InnerProductGeometry.angle x (x + y) = Real.arcsin (‖y‖ / ‖x + y‖)
-- Mathlib.Topology.UniformSpace.Pi
Pi.complete : ∀ {ι : Type u_1} (α : ι → Type u) [U : (i : ι) → UniformSpace (α i)] [∀ (i : ι), CompleteSpace (α i)],
  CompleteSpace ((i : ι) → α i)
-- Lean.Meta.ReduceEval
Lean.Meta.ReduceEval : Type → Type
-- Mathlib.Analysis.Real.OfDigits
/-- `ofDigits` takes a sequence of digits `(d₀, d₁, ...)` in base `b` and returns the
real number `0.d₀d₁d₂... = ∑ᵢ(dᵢ/bⁱ)`. This auxiliary definition `ofDigitsTerm` sends the
sequence to the function sending `i` to `dᵢ/bⁱ`.  -/
Real.ofDigitsTerm : {b : ℕ} → (ℕ → Fin b) → ℕ → ℝ
-- Mathlib.Algebra.Order.AddTorsor
/-- An ordered cancellative vector addition is an ordered vector addition that is cancellative.  -/
IsOrderedCancelVAdd : (G : Type u_3) → (P : Type u_4) → [LE G] → [LE P] → [VAdd G P] → Prop
-- Mathlib.Analysis.InnerProductSpace.Basic
Inner.rclikeToReal.eq_1 : ∀ (𝕜 : Type u_1) (E : Type u_2) [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E],
  Inner.rclikeToReal 𝕜 E = { inner := fun x y => RCLike.re (inner 𝕜 x y) }
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.StAct.peek.sizeOf_spec : ∀ {K : Type u_1} {Γ : K → Type u_2} {σ : Type u_4} {k : K} [inst : SizeOf K] [inst_1 : (a : K) → SizeOf (Γ a)]
  [inst_2 : SizeOf σ] (a : σ → Option (Γ k) → σ), sizeOf (Turing.TM2to1.StAct.peek a) = 1
-- Mathlib.LinearAlgebra.Projectivization.Collinear
/-- If there exists a submodule of dimension at most `2` containing all points in
`S`, then `S` is collinear. The finite-dimensionality is required so that this notion is
meaningful even when `V` is infinite-dimensional.  -/
Projectivization.IsCollinear : {K : Type u_1} →
  {V : Type u_2} →
    [inst : DivisionRing K] → [inst_1 : AddCommGroup V] → [inst_2 : Module K V] → Set (Projectivization K V) → Prop
-- Mathlib.AlgebraicGeometry.Cover.Over
AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_X : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme)
  [inst : P.IsStableUnderBaseChange] [inst_1 : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P]
  {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X)
  (f : W ⟶ X) [inst_2 : W.Over S] [inst_3 : X.Over S] [inst_4 : AlgebraicGeometry.Scheme.Cover.Over S 𝒰]
  [inst_5 : AlgebraicGeometry.Scheme.Hom.IsOver f S] {Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  [inst_6 : Q.HasOfPostcompProperty Q] [inst_7 : Q.IsStableUnderBaseChange] [inst_8 : Q.IsStableUnderComposition]
  (hX : Q (X ↘ S)) (hW : Q (W ↘ S)) (hQ : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)) (x : 𝒰.I₀),
  (AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp' S 𝒰 f hX hW hQ).X x =
    (CategoryTheory.Limits.pullback (AlgebraicGeometry.Scheme.Hom.asOverProp (𝒰.f x) S)
        (AlgebraicGeometry.Scheme.Hom.asOverProp f S)).left
-- Mathlib.LinearAlgebra.Matrix.Trace
/-- `Matrix.trace` as a `LinearMap`  -/
Matrix.traceLinearMap : (n : Type u_3) →
  (α : Type u_5) →
    (R : Type u_6) →
      [Fintype n] → [inst : AddCommMonoid R] → [inst_1 : Semiring α] → [inst_2 : Module α R] → Matrix n n R →ₗ[α] R
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- A family of AddHom's `f a : γ → β a` defines an AddHom `AddHom.pi f : γ → Π a, β a` given by
`AddHom.pi f x b = f b x`.  -/
AddHom.pi : {I : Type u} →
  {f : I → Type v} →
    [inst : (i : I) → Add (f i)] → {γ : Type w} → [inst_1 : Add γ] → ((i : I) → γ →ₙ+ f i) → γ →ₙ+ (i : I) → f i
-- Init.Internal.Order.Lemmas
Array.forIn'.loop.induct : ∀ {α : Type u} {β : Type v} (as : Array α) (motive : (i : ℕ) → i ≤ as.size → β → Prop),
  (∀ (b : β) (x : 0 ≤ as.size), motive 0 x b) →
    (∀ (b : β) (i : ℕ) (h : i + 1 ≤ as.size) (h' : i < as.size),
        as.size - 1 < as.size → as.size - 1 - i < as.size → (∀ (b : β), motive i ⋯ b) → motive i.succ h b) →
      ∀ (i : ℕ) (h : i ≤ as.size) (b : β), motive i h b
-- Mathlib.Analysis.Normed.Group.Continuity
continuous_enorm : ∀ {E : Type u_7} [inst : TopologicalSpace E] [inst_1 : ContinuousENorm E], Continuous fun a => ‖a‖ₑ
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.hom_ext_succ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} {F G : CategoryTheory.ComposableArrows C (n + 1)}
  {f g : F ⟶ G},
  CategoryTheory.ComposableArrows.app' f 0 ⋯ = CategoryTheory.ComposableArrows.app' g 0 ⋯ →
    CategoryTheory.ComposableArrows.δ₀Functor.map f = CategoryTheory.ComposableArrows.δ₀Functor.map g → f = g
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap.0.Std.IterM.step_flattenAfter.match_5.eq_1 : ∀ {α₂ β : Type u_1} {m : Type u_1 → Type u_2} (motive : Option (Std.IterM m β) → Sort u_3) (h_1 : Unit → motive none)
  (h_2 : (it₂ : Std.IterM m β) → motive (some it₂)),
  (match none with
    | none => h_1 ()
    | some it₂ => h_2 it₂) =
    h_1 ()
-- Mathlib.Algebra.Homology.Monoidal
HomologicalComplex.monoidalCategoryStruct : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.Preadditive C] →
        [CategoryTheory.Limits.HasZeroObject C] →
          [(CategoryTheory.MonoidalCategory.curriedTensor C).Additive] →
            [∀ (X₁ : C), ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁).Additive] →
              {I : Type u_2} →
                [inst_6 : AddMonoid I] →
                  (c : ComplexShape I) →
                    [c.TensorSigns] →
                      [∀ (X₁ X₂ : CategoryTheory.GradedObject I C), X₁.HasTensor X₂] →
                        [∀ (X₁ : C),
                              CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C)
                                ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁)] →
                          [∀ (X₂ : C),
                                CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C)
                                  ((CategoryTheory.MonoidalCategory.curriedTensor C).flip.obj X₂)] →
                            [∀ (X₁ X₂ X₃ : CategoryTheory.GradedObject I C), X₁.HasGoodTensor₁₂Tensor X₂ X₃] →
                              [∀ (X₁ X₂ X₃ : CategoryTheory.GradedObject I C), X₁.HasGoodTensorTensor₂₃ X₂ X₃] →
                                [DecidableEq I] → CategoryTheory.MonoidalCategoryStruct (HomologicalComplex C c)
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.mul.congr_simp : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} {β : Type u_6} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ]
  [inst_2 : IsOrderedCancelAddMonoid Γ] [inst_3 : Semiring R] (s s_1 : HahnSeries.SummableFamily Γ R α),
  s = s_1 → ∀ (t t_1 : HahnSeries.SummableFamily Γ R β), t = t_1 → s.mul t = s_1.mul t_1
-- Mathlib.MeasureTheory.Group.Measure
/-- Continuity of the measure of translates of a compact set: Given a compact set `k`
in an additive topological group, for `g` close enough to the origin, `μ (g +ᵥ k \ k)` is
arbitrarily small.  -/
MeasureTheory.eventually_nhds_zero_measure_vadd_sdiff_lt : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G}
  [inst_3 : AddGroup G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] [MeasureTheory.IsFiniteMeasureOnCompacts μ]
  [μ.InnerRegularCompactLTTop] {k : Set G},
  IsCompact k → IsClosed k → ∀ {ε : ENNReal}, ε ≠ 0 → ∀ᶠ (g : G) in nhds 0, μ ((g +ᵥ k) \ k) < ε
-- Mathlib.Data.Finset.Fold
Finset.fold.congr_simp : ∀ {α : Type u_1} {β : Type u_2} (op op_1 : β → β → β) (e_op : op = op_1) [hc : Std.Commutative op]
  [ha : Std.Associative op] (b b_1 : β),
  b = b_1 →
    ∀ (f f_1 : α → β), f = f_1 → ∀ (s s_1 : Finset α), s = s_1 → Finset.fold op b f s = Finset.fold op_1 b_1 f_1 s_1
-- Mathlib.RingTheory.Extension.Presentation.Basic
/-- The canonical `R`-presentation of `R` with no generators and no relations.  -/
Algebra.Presentation.id : (R : Type u) → [inst : CommRing R] → Algebra.Presentation R R PEmpty.{w + 1} PEmpty.{t + 1}
-- Init.Data.Nat.Lemmas
Nat.ne_zero_of_mul_ne_zero_right : ∀ {n m : ℕ}, n * m ≠ 0 → m ≠ 0
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.nndist_eq_sum : ∀ {ι : Type u_2} [inst : Fintype ι] {p : ENNReal} [inst_1 : Fact (1 ≤ p)] {β : ι → Type u_5}
  [inst_2 : (i : ι) → PseudoMetricSpace (β i)],
  p ≠ ⊤ → ∀ (x y : PiLp p β), nndist x y = (∑ i, nndist (x.ofLp i) (y.ofLp i) ^ p.toReal) ^ (1 / p.toReal)
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly
LinearMap.minpoly_toMatrix : ∀ {R : Type u} [inst : CommRing R] {n : Type v} [inst_1 : DecidableEq n] [inst_2 : Fintype n] {N : Type w}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (b : Module.Basis n R N) (f : N →ₗ[R] N),
  minpoly R ((LinearMap.toMatrix b b) f) = minpoly R f
-- Lean.Server.Requests
Lean.Server.RequestM.sendServerRequest : (paramType : Type u_1) →
  [Lean.ToJson paramType] →
    (responseType : Type) →
      [Lean.FromJson responseType] →
        [Inhabited responseType] →
          String →
            paramType → Lean.Server.RequestM (Lean.Server.ServerTask (Lean.Server.ServerRequestResponse responseType))
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift_decl_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (n d : aig.RefVec w) (wn wr : ℕ)
  (q r : aig.RefVec w) (idx : ℕ) (h1 : idx < aig.decls.size)
  (h2 : idx < (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig n d wn wr q r).aig.decls.size),
  (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig n d wn wr q r).aig.decls[idx] =
    aig.decls[idx]
-- Mathlib.Computability.PartrecBasis
Nat.Partrec'.comp : ∀ {m n : ℕ} {f : List.Vector ℕ n →. ℕ} (g : Fin n → List.Vector ℕ m →. ℕ),
  Nat.Partrec' f → (∀ (i : Fin n), Nat.Partrec' (g i)) → Nat.Partrec' fun v => (List.Vector.mOfFn fun i => g i v) >>= f
-- Mathlib.Data.Set.Card.Arithmetic
Set.encard_iUnion_le_of_fintype : ∀ {α : Type u_1} {ι : Type u_2} [inst : Fintype ι] (s : ι → Set α), (⋃ i, s i).encard ≤ ∑ i, (s i).encard
-- Std.Data.Iterators.Producers.Range
/-- Returns an iterator over the given range. This iterator will emit the elements of the range
in increasing order.
 -/
Std.Roc.iter : {α : Type u_1} → [Std.PRange.UpwardEnumerable α] → Std.Roc α → Std.Iter α
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Take
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.Take.0.Std.IterM.step_take.match_3.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (k : ℕ) → motive k.succ),
  (match 0 with
    | 0 => h_1 ()
    | k.succ => h_2 k) =
    h_1 ()
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
_private.Mathlib.Analysis.Distribution.SchwartzSpace.Basic.0.SchwartzMap.bounds_bddBelow : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] (k n : ℕ) (f : SchwartzMap E F),
  BddBelow {c | 0 ≤ c ∧ ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ c}
-- Lean.Environment
Lean.OLeanEntries.mk : {α : Type} → α → α → α → Lean.OLeanEntries α
-- Mathlib.CategoryTheory.Triangulated.Basic
/-- The second morphism of a triangle, as a natural transformation `π₂ ⟶ π₃`.  -/
CategoryTheory.Pretriangulated.Triangle.π₂Toπ₃ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      CategoryTheory.Pretriangulated.Triangle.π₂ ⟶ CategoryTheory.Pretriangulated.Triangle.π₃
-- Mathlib.Logic.Equiv.Defs
Equiv.functionSwap_symm_apply : ∀ (α : Sort u_1) (β : Sort u_2) (γ : α → β → Sort u_3), ⇑(Equiv.functionSwap α β γ).symm = Function.swap
-- Mathlib.Analysis.Calculus.FDeriv.Const
hasFDerivAt_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] (x : E), HasFDerivAt 0 0 x
-- Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
/-- The base change homomorphism underlying `IsBaseChange.linearMapRight`  -/
IsBaseChange.linearMapRightBaseChangeHom : {R : Type u_1} →
  [inst : CommSemiring R] →
    (S : Type u_2) →
      [inst_1 : CommSemiring S] →
        [inst_2 : Algebra R S] →
          (M : Type u_3) →
            [inst_3 : AddCommMonoid M] →
              [inst_4 : Module R M] →
                {N : Type u_4} →
                  [inst_5 : AddCommMonoid N] →
                    [inst_6 : Module R N] →
                      {P : Type u_5} →
                        [inst_7 : AddCommMonoid P] →
                          [inst_8 : Module R P] →
                            [inst_9 : Module S P] →
                              [inst_10 : IsScalarTower R S P] →
                                (N →ₗ[R] P) → TensorProduct R S (M →ₗ[R] N) →ₗ[S] M →ₗ[R] P
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.evaluation₄_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Square C} (φ : X ⟶ Y),
  CategoryTheory.Square.evaluation₄.map φ = φ.τ₄
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Rco.isEmpty.eq_1 : ∀ {α : Type u} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α] (r : Std.Rco α),
  r.isEmpty = decide ¬r.lower < r.upper
-- Std.Time.Zoned.ZoneRules
Std.Time.TimeZone.instReprZoneRules : Repr Std.Time.TimeZone.ZoneRules
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKeyD.congr_simp : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m m_1 : Std.ExtDHashMap α β),
  m = m_1 →
    ∀ (a a_1 : α),
      a = a_1 → ∀ (fallback fallback_1 : α), fallback = fallback_1 → m.getKeyD a fallback = m_1.getKeyD a_1 fallback_1