mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.Iteration.obj_succ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C}
  [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J]
  [inst_4 : CategoryTheory.Limits.HasIterationOfShape J C] [inst_5 : WellFoundedLT J] {j : J} (iter : Φ.Iteration j)
  (i : J) (hi : i < j), iter.F.obj ⟨Order.succ i, ⋯⟩ = Φ.succ (iter.F.obj ⟨i, ⋯⟩)
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.loopyOn_rankFinite : ∀ {α : Type u_1} {E : Set α}, (Matroid.loopyOn E).RankFinite
-- Init.Data.Slice.InternalLemmas
Std.Slice.Internal.toList_eq_toList_iter : ∀ {γ : Type u} {α β : Type v} {s : Std.Slice γ} [inst : Std.ToIterator (Std.Slice γ) Id α β]
  [inst_1 : Std.Iterator α Id β] [Std.Iterators.Finite α Id], s.toList = (Std.Slice.Internal.iter s).toList
-- Mathlib.Order.Interval.Finset.Basic
/-- **Alias** of the reverse direction of `Finset.nonempty_Ico`. -/
Finset.Aesop.nonempty_Ico_of_lt : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α], a < b → (Finset.Ico a b).Nonempty
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
HurwitzKernelBounds.F_nat_zero_le : ∀ {a : ℝ},
  0 ≤ a →
    ∀ {t : ℝ},
      0 < t → ‖HurwitzKernelBounds.F_nat 0 a t‖ ≤ Real.exp (-Real.pi * a ^ 2 * t) / (1 - Real.exp (-Real.pi * t))
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.instSMulCommClass : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] {M : Type u_7} {N : Type u_8}
  [inst_6 : Monoid M] [inst_7 : DistribMulAction M F] [inst_8 : SMulCommClass S M F] [inst_9 : Monoid N]
  [inst_10 : DistribMulAction N F] [inst_11 : SMulCommClass S N F] [SMulCommClass M N F],
  SMulCommClass M N (E →ₛₗ.[σ] F)
-- Mathlib.CategoryTheory.Category.Pointed
Pointed.Hom.mk.sizeOf_spec : ∀ {X Y : Pointed} (toFun : X.X → Y.X) (map_point : toFun X.point = Y.point),
  sizeOf { toFun := toFun, map_point := map_point } = 1 + sizeOf map_point
-- Mathlib.Data.Set.Prod
Set.prod_preimage_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {f : γ → α},
  (f ⁻¹' s) ×ˢ t = (fun p => (f p.1, p.2)) ⁻¹' s ×ˢ t
-- Mathlib.Topology.MetricSpace.Pseudo.Basic
/-- **Alias** of the forward direction of `Metric.inseparable_iff_nndist`. -/
Inseparable.nndist_eq_zero : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α}, Inseparable x y → nndist x y = 0
-- Init.Data.Fin.Lemmas
Fin.cast_cast : ∀ {n m k : ℕ} (h : n = m) (h' : m = k) {i : Fin n}, Fin.cast h' (Fin.cast h i) = Fin.cast ⋯ i
-- Mathlib.LinearAlgebra.Matrix.Bilinear
/-- On square matrices, `Matrix.mulLeftLinearMap` and `LinearMap.mulLeft` coincide.  -/
mulLeftLinearMap_eq_mulLeft : ∀ {m : Type u_2} (R : Type u_5) {A : Type u_6} [inst : Fintype m] [inst_1 : Semiring R]
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : Module R A] [inst_4 : SMulCommClass R A A],
  mulLeftLinearMap m R = LinearMap.mulLeft R
-- Init.Data.Fin.Lemmas
Fin.not_lt : ∀ {n : ℕ} {a b : Fin n}, ¬a < b ↔ b ≤ a
-- Std.Data.HashSet.Lemmas
Std.HashSet.size_inter_le_size_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α],
  (m₁ ∩ m₂).size ≤ m₂.size
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.leftOp : Cᵒᵖ ⥤ D` reflects colimits of `K.op : Jᵒᵖ ⥤ Cᵒᵖ`, then `F : C ⥤ Dᵒᵖ` reflects
limits of `K : J ⥤ C`.  -/
CategoryTheory.Limits.reflectsLimit_of_leftOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C)
  (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.ReflectsColimit K.op F.leftOp],
  CategoryTheory.Limits.ReflectsLimit K F
-- Mathlib.Algebra.Group.InjSurj
Function.Injective.monoid.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₁] [inst_1 : One M₁] [inst_2 : Pow M₁ ℕ] [inst_3 : Monoid M₂]
  (f : M₁ → M₂) (hf : Function.Injective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y)
  (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n),
  Function.Injective.monoid f hf one mul npow =
    { toSemigroup := Function.Injective.semigroup f hf mul,
      toOne := (Function.Injective.mulOneClass f hf one mul).toOne, one_mul := ⋯, mul_one := ⋯,
      npow := fun n x => x ^ n, npow_zero := ⋯, npow_succ := ⋯ }
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
ContMDiffAt.of_le : ∀ {𝕜 : 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'] {f : M → M'} {x : M} {m n : WithTop ℕ∞},
  ContMDiffAt I I' n f x → m ≤ n → ContMDiffAt I I' m f x
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.AssocList.forInStep.go.match_1.splitter : {δ : Type u_1} →
  (motive : ForInStep δ → Sort u_2) →
    (__do_lift : ForInStep δ) →
      ((d : δ) → motive (ForInStep.done d)) → ((d : δ) → motive (ForInStep.yield d)) → motive __do_lift
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
RootPairing.GeckConstruction.trace_h_eq_zero : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [CharZero R] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : AddCommGroup N] [inst_5 : Module R N] {P : RootPairing ι R M N}
  [inst_6 : P.IsCrystallographic] {b : P.Base} [inst_7 : Fintype ι] (i : ↥b.support),
  (RootPairing.GeckConstruction.h i).trace = 0
-- Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
ordinaryHypergeometric_radius_top_of_neg_nat₁ : ∀ {𝕂 : Type u_1} (𝔸 : Type u_2) [inst : RCLike 𝕂] [inst_1 : NormedDivisionRing 𝔸] [inst_2 : NormedAlgebra 𝕂 𝔸] (b c : 𝕂)
  {k : ℕ}, (ordinaryHypergeometricSeries 𝔸 (-↑k) b c).radius = ⊤
-- Mathlib.Order.Circular
/-- **Alias** of `btw_cyclic_right`. -/
Btw.btw.cyclic_right : ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, btw a b c → btw c a b
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Rxi.Iterator.step.eq_1 : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] (it : Std.Iter α),
  Std.Rxi.Iterator.step it =
    match it.internalState.next with
    | none => Std.IterStep.done
    | some next => Std.IterStep.yield { internalState := { next := Std.PRange.succ? next } } next
-- Mathlib.Combinatorics.Additive.Convolution
Finset.addConvolution_le_card_right : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] {A B : Finset G} {x : G}, A.addConvolution B x ≤ B.card
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
/-- `padicValInt p 1` is `0` for any `p`.  -/
padicValInt.one : ∀ {p : ℕ}, padicValInt p 1 = 0
-- Mathlib.RingTheory.LaurentSeries
/-- The uniform space equivalence between two abstract completions of `ratfunc K` as a ring
equivalence: it goes from `K⸨X⸩` to `RatFuncAdicCompl K`  -/
LaurentSeries.LaurentSeriesRingEquiv : (K : Type u_2) → [inst : Field K] → LaurentSeries K ≃+* LaurentSeries.RatFuncAdicCompl K
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_rev_uIcc : ∀ {n : ℕ} (i j : Fin n), Fin.rev ⁻¹' Set.uIcc i j = Set.uIcc i.rev j.rev
-- Std.Time.DateTime.Timestamp
/-- Duration since the unix epoch.
 -/
Std.Time.Timestamp.val : Std.Time.Timestamp → Std.Time.Duration
-- Mathlib.RingTheory.Localization.AtPrime.Basic
Localization.localRingHom_bijective_of_saturated_inf_eq_top : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {P : Ideal S}
  [inst_3 : P.IsPrime] {s : Subalgebra R S},
  s.saturation (P.primeCompl ⊓ s.toSubmonoid) ⋯ = ⊤ →
    ∀ (p : Ideal ↥s) [inst_4 : p.IsPrime] [inst_5 : P.LiesOver p],
      Function.Bijective ⇑(Localization.localRingHom p P (algebraMap (↥s) S) ⋯)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
CategoryTheory.Limits.instIsIsoKernelComparison : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (G : CategoryTheory.Functor C D) [inst_4 : G.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y)
  [inst_5 : CategoryTheory.Limits.HasKernel f] [inst_6 : CategoryTheory.Limits.HasKernel (G.map f)]
  [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) G],
  CategoryTheory.IsIso (CategoryTheory.Limits.kernelComparison f G)
-- Mathlib.Data.Multiset.MapFold
Multiset.map_comp_cons : ∀ {α : Type u_1} {β : Type v} (f : α → β) (t : α),
  Multiset.map f ∘ Multiset.cons t = Multiset.cons (f t) ∘ Multiset.map f
-- Init.Data.String.Lemmas.Iterate
String.Slice.Model.map_get_positionsFrom_of_splits : ∀ {s : String.Slice} {p : s.Pos} {t₁ t₂ : String},
  p.Splits t₁ t₂ → List.map (fun p => (↑p).get ⋯) (String.Slice.Model.positionsFrom p) = t₂.toList
-- Init.Data.List.Basic
List.flatMap_cons : ∀ {α : Type u} {β : Type v} {x : α} {xs : List α} {f : α → List β}, List.flatMap f (x :: xs) = f x ++ List.flatMap f xs
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.one_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] (i : ℕ), ↑1 i = 1
-- Lean.Meta.Tactic.Grind.AC.Util
Lean.Meta.Grind.AC.getOpId? : Lean.Expr → Lean.Meta.Grind.GoalM (Option ℕ)
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.GrothendieckTopology.Point.instPreservesFiniteLimitsFunctorOppositePresheafFiberOfLocallySmallOfHasFiniteLimitsOfAB5OfSize : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] [CategoryTheory.LocallySmall.{w, v, u} C]
  [CategoryTheory.Limits.HasFiniteLimits A] [CategoryTheory.AB5OfSize.{w, w, v', u'} A],
  CategoryTheory.Limits.PreservesFiniteLimits Φ.presheafFiber
-- Lean.Parser.Basic
Lean.Parser.error : String → Lean.Parser.Parser
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_eq_default : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited β], t.WF → ∀ {a : α}, a ∉ t → Std.DTreeMap.Internal.Impl.Const.get! t a = default
-- Mathlib.NumberTheory.MahlerMeasure
Polynomial.ncard_boxPoly : ∀ (n : ℕ) (B₁ B₂ : Fin (n + 1) → ℝ), (Polynomial.boxPoly n B₁ B₂).ncard = ∏ i, (⌊B₂ i⌋ - ⌈B₁ i⌉ + 1).toNat
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey!_diff_of_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [inst : Inhabited α]
  [Std.TransCmp cmp] {k : α}, k ∈ t₂ → (t₁ \ t₂).getKey! k = default
-- Init.Data.Vector.MapIdx
Vector.mem_mapIdx : ∀ {β : Type u_1} {α : Type u_2} {n : ℕ} {f : ℕ → α → β} {b : β} {xs : Vector α n},
  b ∈ Vector.mapIdx f xs ↔ ∃ i, ∃ (h : i < n), f i xs[i] = b
-- Mathlib.Analysis.Normed.Order.UpperLower
IsUpperSet.cthickening : ∀ {α : Type u_1} [inst : NormedAddCommGroup α] [inst_1 : Preorder α] [IsOrderedAddMonoid α] {s : Set α},
  IsUpperSet s → ∀ (ε : ℝ), IsUpperSet (Metric.cthickening ε s)
-- Init.System.IO
IO.FS.instBEqSystemTime : BEq IO.FS.SystemTime
-- Mathlib.Topology.Category.TopCommRingCat
TopCommRingCat.hasForgetToCommRingCat : CategoryTheory.HasForget₂ TopCommRingCat CommRingCat
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
SimpleGraph.bipartiteDoubleCover.eq_1 : ∀ {V : Type u_1} (G : SimpleGraph V),
  G.bipartiteDoubleCover =
    {
      Adj := fun x x_1 =>
        match x, x_1 with
        | Sum.inl v', Sum.inr w' => G.Adj v' w'
        | Sum.inr v', Sum.inl w' => G.Adj v' w'
        | x, x_2 => False,
      symm := ⋯, loopless := ⋯ }
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.addCommMagma.eq_1 : ∀ {M : Type u_4} [inst : AddCommMagma M] (c : AddCon M), c.addCommMagma = { toAdd := c.hasAdd, add_comm := ⋯ }
-- Mathlib.NumberTheory.Padics.Hensel
limit_zero_of_norm_tendsto_zero : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {ncs : CauSeq ℤ_[p] norm} {F : Polynomial R},
  Filter.Tendsto (fun i => ‖(Polynomial.aeval (↑ncs i)) F‖) Filter.atTop (nhds 0) → (Polynomial.aeval ncs.lim) F = 0
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM1.stmts₁.match_1.eq_4 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (motive : Turing.TM1.Stmt Γ Λ σ → Sort u_4) (a : Γ → σ → Bool)
  (q₁ q₂ : Turing.TM1.Stmt Γ Λ σ)
  (h_1 :
    (Q : Turing.TM1.Stmt Γ Λ σ) →
      (a : Turing.Dir) → (q : Turing.TM1.Stmt Γ Λ σ) → Q = Turing.TM1.Stmt.move a q → motive (Turing.TM1.Stmt.move a q))
  (h_2 :
    (Q : Turing.TM1.Stmt Γ Λ σ) →
      (a : Γ → σ → Γ) →
        (q : Turing.TM1.Stmt Γ Λ σ) → Q = Turing.TM1.Stmt.write a q → motive (Turing.TM1.Stmt.write a q))
  (h_3 :
    (Q : Turing.TM1.Stmt Γ Λ σ) →
      (a : Γ → σ → σ) → (q : Turing.TM1.Stmt Γ Λ σ) → Q = Turing.TM1.Stmt.load a q → motive (Turing.TM1.Stmt.load a q))
  (h_4 :
    (Q : Turing.TM1.Stmt Γ Λ σ) →
      (a : Γ → σ → Bool) →
        (q₁ q₂ : Turing.TM1.Stmt Γ Λ σ) → Q = Turing.TM1.Stmt.branch a q₁ q₂ → motive (Turing.TM1.Stmt.branch a q₁ q₂))
  (h_5 : (Q : Turing.TM1.Stmt Γ Λ σ) → motive Q),
  (match Turing.TM1.Stmt.branch a q₁ q₂ with
    | Q@h:(Turing.TM1.Stmt.move a q) => h_1 Q a q h
    | Q@h:(Turing.TM1.Stmt.write a q) => h_2 Q a q h
    | Q@h:(Turing.TM1.Stmt.load a q) => h_3 Q a q h
    | Q@h:(Turing.TM1.Stmt.branch a q₁ q₂) => h_4 Q a q₁ q₂ h
    | Q => h_5 Q) =
    h_4 (Turing.TM1.Stmt.branch a q₁ q₂) a q₁ q₂ ⋯
-- Mathlib.Tactic.ModCases
/-- `OnModCases n a lb p` represents a partial proof by cases that
there exists `0 ≤ m < n` such that `a ≡ m (mod n)`.
It asserts that if `∃ m, lb ≤ m < n ∧ a ≡ m (mod n)` holds, then `p`
(where `p` is the current goal).
 -/
Mathlib.Tactic.ModCases.NatMod.OnModCases : ℕ → ℕ → ℕ → Sort u_1 → Sort u_1
-- Mathlib.RingTheory.PowerSeries.PiTopology
/-- Assuming the base ring has a discrete topology, the powers of a `PowerSeries` converge to 0
iff its constant coefficient is nilpotent.
[N. Bourbaki, *Algebra II*, Chapter 4, §4, n°2, corollary of prop. 3][bourbaki1981]  -/
PowerSeries.WithPiTopology.isTopologicallyNilpotent_iff_constantCoeff_isNilpotent : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : CommRing R] [DiscreteTopology R] (f : PowerSeries R),
  Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0) ↔ IsNilpotent (PowerSeries.constantCoeff f)
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.sum_apply : ∀ {ι : Type u_1} {β : ι → Type v} {ι₁ : Type u₁} [inst : DecidableEq ι₁] {β₁ : ι₁ → Type v₁}
  [inst_1 : (i₁ : ι₁) → Zero (β₁ i₁)] [inst_2 : (i : ι₁) → (x : β₁ i) → Decidable (x ≠ 0)]
  [inst_3 : (i : ι) → AddCommMonoid (β i)] {f : Π₀ (i₁ : ι₁), β₁ i₁} {g : (i₁ : ι₁) → β₁ i₁ → Π₀ (i : ι), β i} {i₂ : ι},
  (f.sum g) i₂ = f.sum fun i₁ b => (g i₁ b) i₂
-- Mathlib.Algebra.CharP.Defs
/-- The characteristic is prime if it is non-zero.  -/
CharP.char_prime_of_ne_zero : ∀ (R : Type u_1) [inst : NonAssocSemiring R] [NoZeroDivisors R] [Nontrivial R] {p : ℕ} [CharP R p], p ≠ 0 → Nat.Prime p
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.sub_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G K : CochainComplex C ℤ} {n₁ n₂ n₁₂ : ℤ} (z₁ z₁' : CochainComplex.HomComplex.Cochain F G n₁)
  (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (h : n₁ + n₂ = n₁₂),
  (z₁ - z₁').comp z₂ h = z₁.comp z₂ h - z₁'.comp z₂ h
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
/-- The image of an element `p` of `FreeAddMonoid (R × Π i, s i)` in the `PiTensorProduct` is
equal to the sum of `a • ⨂ₜ[R] i, m i` over all the entries `(a, m)` of `p`.
 -/
FreeAddMonoid.toPiTensorProduct : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] (p : FreeAddMonoid (R × ((i : ι) → s i))),
  ↑p = (List.map (fun x => x.1 • ⨂ₜ[R] (i : ι), x.2 i) (FreeAddMonoid.toList p)).sum
-- Mathlib.Topology.MetricSpace.IsometricSMul
/-- Addition `y ↦ x + y` as an `IsometryEquiv`.  -/
IsometryEquiv.addLeft : {G : Type v} → [inst : AddGroup G] → [inst_1 : PseudoEMetricSpace G] → [IsIsometricVAdd G G] → G → G ≃ᵢ G
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.singleton_vsub_singleton : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] [inst_1 : DecidableEq α] (a b : β), {a} -ᵥ {b} = {a -ᵥ b}
-- Mathlib.Topology.Homotopy.Product
/-- The product of homotopies `F` and `G`,
where `F` takes `f₀` to `f₁` and `G` takes `g₀` to `g₁`  -/
ContinuousMap.Homotopy.prod : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        {A : Type u_3} →
          [inst_2 : TopologicalSpace A] →
            {f₀ f₁ : C(A, α)} →
              {g₀ g₁ : C(A, β)} → f₀.Homotopy f₁ → g₀.Homotopy g₁ → (f₀.prodMk g₀).Homotopy (f₁.prodMk g₁)
-- Mathlib.Topology.ClusterPt
mem_closure_iff_comap_neBot : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {s : Set X},
  x ∈ closure s ↔ (Filter.comap Subtype.val (nhds x)).NeBot
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap_presheafObjObjIso_hom_assoc : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A]
  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X)
  [inst_4 : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : CategoryTheory.Sheaf J₀ A) (X : C)
  (i : (data X).I₀) {Z : A} (h : G₀.obj.obj (Opposite.op ((data X).X i)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap data G₀ ((data X).f i))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso data G₀ ((data X).X i)).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjπ data G₀ X i)
      h
-- Mathlib.NumberTheory.LSeries.Injectivity
/-- The abscissa of absolute convergence of `f - g` is at most the maximum of those
of `f` and `g`.  -/
LSeries.abscissaOfAbsConv_sub_le : ∀ (f g : ℕ → ℂ), LSeries.abscissaOfAbsConv (f - g) ≤ max (LSeries.abscissaOfAbsConv f) (LSeries.abscissaOfAbsConv g)
-- Batteries.Data.List.Lemmas
List.disjoint_of_disjoint_cons_right : ∀ {α : Type u_1} {a : α} {l₁ l₂ : List α}, l₁.Disjoint (a :: l₂) → l₁.Disjoint l₂
-- Mathlib.Topology.Algebra.MulAction
/-- Suppose that `N` acts on `X` and `M` continuously acts on `Y`.
Suppose that `g : Y → X` is an action homomorphism in the following sense:
there exists a continuous function `f : N → M` such that `g (c • x) = f c • g x`.
Then the action of `N` on `X` is continuous as well.

In many cases, `f = id` so that `g` is an action homomorphism in the sense of `MulActionHom`.
However, this version also works for semilinear maps and `f = Units.val`.  -/
Topology.IsInducing.continuousSMul : ∀ {M : Type u_1} {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace Y] [inst_3 : SMul M X] [ContinuousSMul M X] {g : Y → X} {N : Type u_5} [inst_5 : SMul N Y]
  [inst_6 : TopologicalSpace N] {f : N → M},
  Topology.IsInducing g → Continuous f → (∀ {c : N} {x : Y}, g (c • x) = f c • g x) → ContinuousSMul N Y
-- Mathlib.Order.CompleteSublattice
CompleteSublattice.map_carrier : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : CompleteLatticeHom α β)
  (L : CompleteSublattice α), (CompleteSublattice.map f L).carrier = ⇑f '' ↑L
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.Hom.sieve₀_le_sieve₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreZeroHypercover S}
  {F : CategoryTheory.PreZeroHypercover S} (f : E.Hom F), E.sieve₀ ≤ F.sieve₀
-- Mathlib.RingTheory.SimpleModule.Basic
Module.toModuleEnd.congr_simp : ∀ (R : Type u_1) {S : Type u_3} (M : Type u_4) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Semiring S] [inst_4 : Module S M] [inst_5 : SMulCommClass S R M],
  Module.toModuleEnd R M = Module.toModuleEnd R M
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.constGetEntryLTD_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {k : α} {fallback : α × β},
  t₁.Equiv t₂ → Std.DTreeMap.Const.getEntryLTD t₁ k fallback = Std.DTreeMap.Const.getEntryLTD t₂ k fallback
-- Batteries.Data.AssocList
Batteries.AssocList.modify.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : BEq α] (a : α) (f : α → β → β),
  Batteries.AssocList.modify a f Batteries.AssocList.nil = Batteries.AssocList.nil
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanShape.mk : (L : Type w) → (R : Type w') → (L → R) → (L → R) → CategoryTheory.Limits.MultispanShape
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.SimprocDeclExtState : Type
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.toZeroAtInfty_toBCF : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] [inst_4 : ProperSpace E] (f : SchwartzMap E F),
  f.toZeroAtInfty.toBCF = f.toBoundedContinuousFunction
-- Mathlib.Order.Disjoint
IsCompl.sup_inf : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : BoundedOrder α] {x y x' y' : α},
  IsCompl x y → IsCompl x' y' → IsCompl (x ⊔ x') (y ⊓ y')
-- Std.Sat.AIG.RelabelNat
Std.Sat.AIG.RelabelNat.State.Inv2.below.false : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] {decls : Array (Std.Sat.AIG.Decl α)}
  {motive : (a : ℕ) → (a_1 : Std.HashMap α ℕ) → Std.Sat.AIG.RelabelNat.State.Inv2 decls a a_1 → Prop} {idx : ℕ}
  {map : Std.HashMap α ℕ} (hinv : Std.Sat.AIG.RelabelNat.State.Inv2 decls idx map) (hlt : idx < decls.size)
  (hatom : decls[idx] = Std.Sat.AIG.Decl.false),
  Std.Sat.AIG.RelabelNat.State.Inv2.below hinv → motive idx map hinv → Std.Sat.AIG.RelabelNat.State.Inv2.below ⋯
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.CooperSplitPred.mk.inj : ∀ {left : Bool} {c₁ c₂ : Lean.Meta.Grind.Arith.Cutsat.LeCnstr} {c₃? : Option Lean.Meta.Grind.Arith.Cutsat.DvdCnstr}
  {left_1 : Bool} {c₁_1 c₂_1 : Lean.Meta.Grind.Arith.Cutsat.LeCnstr}
  {c₃?_1 : Option Lean.Meta.Grind.Arith.Cutsat.DvdCnstr},
  { left := left, c₁ := c₁, c₂ := c₂, c₃? := c₃? } = { left := left_1, c₁ := c₁_1, c₂ := c₂_1, c₃? := c₃?_1 } →
    left = left_1 ∧ c₁ = c₁_1 ∧ c₂ = c₂_1 ∧ c₃? = c₃?_1
-- Std.Data.ExtTreeSet.Lemmas
/-- This is a restatement of `mem_of_mem_insert` that is written to exactly match the
proof obligation in the statement of `get_insert`.  -/
Std.ExtTreeSet.mem_of_mem_insert' : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k a : α},
  a ∈ t.insert k → ¬(cmp k a = Ordering.eq ∧ k ∉ t) → a ∈ t
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.importRealizationCtx? : Lean.Environment → Option Lean.RealizationContext✝
-- Mathlib.Order.DirSupClosed
IsUpperSet.dirSupClosedOn : ∀ {α : Type u_1} {s : Set α} {D : Set (Set α)} [inst : Preorder α], IsUpperSet s → DirSupClosedOn D s
-- Lean.Meta.Basic
Lean.Meta.elimMVarDeps : Array Lean.Expr → Lean.Expr → optParam Bool false → Lean.MetaM Lean.Expr