mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Analytic.Composition
/-- Version of `AnalyticWithinAt.comp` where point equality is a separate hypothesis.  -/
AnalyticWithinAt.comp_of_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {g : F → G} {f : E → F} {y : F} {x : E} {t : Set F}
  {s : Set E},
  AnalyticWithinAt 𝕜 g t y → AnalyticWithinAt 𝕜 f s x → Set.MapsTo f s t → f x = y → AnalyticWithinAt 𝕜 (g ∘ f) s x
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.Reachable.pos_dist_of_ne : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V}, G.Reachable u v → u ≠ v → 0 < G.dist u v
-- Mathlib.LinearAlgebra.TensorProduct.Matrix
/-- The matrix built from `Matrix.kronecker` corresponds to the linear map built from
`TensorProduct.map`.  -/
Matrix.toLin_kronecker : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {M' : Type u_5} {N' : Type u_6} {ι : Type u_7} {κ : Type u_8}
  {ι' : Type u_10} {κ' : Type u_11} [inst : DecidableEq ι] [inst_1 : DecidableEq κ] [inst_2 : Fintype ι]
  [inst_3 : Fintype κ] [inst_4 : Finite ι'] [inst_5 : Finite κ'] [inst_6 : CommRing R] [inst_7 : AddCommGroup M]
  [inst_8 : AddCommGroup N] [inst_9 : AddCommGroup M'] [inst_10 : AddCommGroup N'] [inst_11 : Module R M]
  [inst_12 : Module R N] [inst_13 : Module R M'] [inst_14 : Module R N'] (bM : Module.Basis ι R M)
  (bN : Module.Basis κ R N) (bM' : Module.Basis ι' R M') (bN' : Module.Basis κ' R N') (A : Matrix ι' ι R)
  (B : Matrix κ' κ R),
  (Matrix.toLin (bM.tensorProduct bN) (bM'.tensorProduct bN')) (Matrix.kroneckerMap (fun x1 x2 => x1 * x2) A B) =
    TensorProduct.map ((Matrix.toLin bM bM') A) ((Matrix.toLin bN bN') B)
-- Mathlib.MeasureTheory.Function.AEEqFun
/-- The ae-limit is ae-unique.  -/
MeasureTheory.AEEqFun.tendsto_ae_unique : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace β]
  {ι : Type u_5} [T2Space β] {g h : α → β} {f : ι → α → β} {l : Filter ι} [l.NeBot],
  (∀ᵐ (ω : α) ∂μ, Filter.Tendsto (fun i => f i ω) l (nhds (g ω))) →
    (∀ᵐ (ω : α) ∂μ, Filter.Tendsto (fun i => f i ω) l (nhds (h ω))) → g =ᵐ[μ] h
-- Mathlib.Analysis.Normed.Group.Basic
nndist_one_right : ∀ {E : Type u_5} [inst : SeminormedGroup E] (a : E), nndist a 1 = ‖a‖₊
-- Mathlib.RepresentationTheory.Coinvariants
Representation.Coinvariants.instFinite : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommRing k] [inst_1 : Monoid G] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] (ρ : Representation k G V) [Module.Finite k V], Module.Finite k ρ.Coinvariants
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.apply_symm_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y) (y : Y),
  h (h.symm y) = y
-- Mathlib.CategoryTheory.MorphismProperty.Limits
/-- `P` has pullbacks if for every `f` satisfying `P`, pullbacks of arbitrary morphisms along `f`
exist.  -/
CategoryTheory.MorphismProperty.HasPullbacks : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → Prop
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.lift_of : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {N : Type u_4} [inst_1 : Monoid N]
  (fi : (i : ι) → M i →* N) {i : ι} (m : M i), (Monoid.CoprodI.lift fi) (Monoid.CoprodI.of m) = (fi i) m
-- Init.Data.SInt.Bitwise
Int16.xor_left_inj : ∀ {a b : Int16} (c : Int16), a ^^^ c = b ^^^ c ↔ a = b
-- Init.Data.SInt.Lemmas
Int32.toInt_ofInt : ∀ {n : ℤ}, (Int32.ofInt n).toInt = n.bmod Int32.size
-- Lean.Parser.Term
Lean.Parser.Term.structInstFieldDef.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Computability.Primrec.Basic
Primrec.comp : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable σ]
  {f : β → σ} {g : α → β}, Primrec f → Primrec g → Primrec fun a => f (g a)
-- Mathlib.CategoryTheory.Bicategory.Span.Basic
CategoryTheory.Span.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {Wₗ Wᵣ : CategoryTheory.MorphismProperty C} {c c' : C}
  [inst_1 : SizeOf C] [inst_2 : ⦃X Y : C⦄ → (x : X ⟶ Y) → SizeOf (Wₗ x)]
  [inst_3 : ⦃X Y : C⦄ → (x : X ⟶ Y) → SizeOf (Wᵣ x)] (apex : C) (l : apex ⟶ c) (r : apex ⟶ c') (wl : Wₗ l) (wr : Wᵣ r),
  sizeOf { apex := apex, l := l, r := r, wl := wl, wr := wr } =
    1 + sizeOf apex + sizeOf l + sizeOf r + sizeOf wl + sizeOf wr
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv.0.Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastShiftConcat.match_1.splitter : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {w : ℕ} →
        (aig : Std.Sat.AIG α) →
          (motive : Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.ShiftConcatInput aig w → Sort u_1) →
            (input : Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.ShiftConcatInput aig w) →
              ((lhs : aig.RefVec w) → (bit : aig.Ref) → motive { lhs := lhs, bit := bit }) → motive input
-- Mathlib.Analysis.Calculus.FDeriv.Mul
fderivWithin_smul_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E}
  {s : Set E} {𝕜' : Type u_5} [inst_5 : NormedRing 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜'] [inst_7 : Module 𝕜' F]
  [inst_8 : IsBoundedSMul 𝕜' F] [inst_9 : IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'},
  UniqueDiffWithinAt 𝕜 s x →
    DifferentiableWithinAt 𝕜 c s x →
      ∀ (f : F), fderivWithin 𝕜 (fun y => c y • f) s x = (fderivWithin 𝕜 c s x).smulRight f
-- Mathlib.Data.Fintype.Card
Fintype.card_congr : ∀ {α : Type u_4} {β : Type u_5} [inst : Fintype α] [inst_1 : Fintype β] (f : α ≃ β), Fintype.card α = Fintype.card β
-- Lean.Meta.Closure
Lean.Meta.Closure.visitLevel : (Lean.Level → Lean.Meta.Closure.ClosureM Lean.Level) → Lean.Level → Lean.Meta.Closure.ClosureM Lean.Level
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.cancel_iso_hom_right_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X X' Y Z : C} (f : W ⟶ X) (g : X ⟶ Y) (f' : W ⟶ X')
  (g' : X' ⟶ Y) (h : Y ≅ Z),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h.hom) =
      CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g' h.hom) ↔
    CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f' g'
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Precoverage.pullbackArrows_mem : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} [J.IsStableUnderBaseChange]
  {X Y : C} (f : X ⟶ Y) {R : CategoryTheory.Presieve Y},
  R ∈ J.coverings Y → ∀ [inst_2 : R.HasPullbacks f], CategoryTheory.Presieve.pullbackArrows f R ∈ J.coverings X
-- Mathlib.Algebra.Lie.UniversalEnveloping
UniversalEnvelopingAlgebra.mkAlgHom.eq_1 : ∀ (R : Type u₁) (L : Type u₂) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  UniversalEnvelopingAlgebra.mkAlgHom R L = RingCon.mkₐ R (UniversalEnvelopingAlgebra.ringCon R L)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
CliffordAlgebraQuaternion.ofQuaternion_mk : ∀ {R : Type u_1} [inst : CommRing R] {c₁ c₂ : R} (a₁ a₂ a₃ a₄ : R),
  CliffordAlgebraQuaternion.ofQuaternion { re := a₁, imI := a₂, imJ := a₃, imK := a₄ } =
    (algebraMap R (CliffordAlgebra (CliffordAlgebraQuaternion.Q c₁ c₂))) a₁ +
          a₂ • (CliffordAlgebra.ι (CliffordAlgebraQuaternion.Q c₁ c₂)) (1, 0) +
        a₃ • (CliffordAlgebra.ι (CliffordAlgebraQuaternion.Q c₁ c₂)) (0, 1) +
      a₄ •
        ((CliffordAlgebra.ι (CliffordAlgebraQuaternion.Q c₁ c₂)) (1, 0) *
          (CliffordAlgebra.ι (CliffordAlgebraQuaternion.Q c₁ c₂)) (0, 1))
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Context.config : Lean.Meta.Grind.Context → Lean.Grind.Config
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.map_add_toList_roc : ∀ {m n k : ℕ}, List.map (fun x => x + k) (m<...=n).toList = ((m + k)<...=n + k).toList
-- Mathlib.Order.Heyting.Basic
compl_top : ∀ {α : Type u_2} [inst : HeytingAlgebra α], ⊤ᶜ = ⊥
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.minimalPeriod_id : ∀ {α : Type u_1} {x : α}, Function.minimalPeriod id x = 1
-- Init.Data.List.Lemmas
List.head?_flatMap : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : α → List β},
  (List.flatMap f l).head? = List.findSome? (fun a => (f a).head?) l
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_erase_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, (t.erase k).getKey? k = none
-- Mathlib.GroupTheory.GroupAction.Blocks
AddAction.isBlock_subtypeVal : ∀ {G : Type u_1} [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] {C : SubAddAction G X} {B : Set ↥C},
  AddAction.IsBlock G (Subtype.val '' B) ↔ AddAction.IsBlock G B
-- Mathlib.Analysis.Normed.Ring.Basic
/-- Normed commutative ring structure on the product of two normed commutative rings, using the sup
norm.  -/
Prod.normedCommRing : {α : Type u_2} → {β : Type u_3} → [NormedCommRing α] → [NormedCommRing β] → NormedCommRing (α × β)
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Cover.LocallyDirected.mk.congr_simp : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme}
  {𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X}
  [inst : CategoryTheory.Category.{v_1, u_1} 𝒰.I₀] (trans trans_1 : {i j : 𝒰.I₀} → (i ⟶ j) → (𝒰.X i ⟶ 𝒰.X j))
  (e_trans : trans = trans_1)
  (trans_id : ∀ (i : 𝒰.I₀), trans (CategoryTheory.CategoryStruct.id i) = CategoryTheory.CategoryStruct.id (𝒰.X i))
  (trans_comp :
    ∀ {i j k : 𝒰.I₀} (hij : i ⟶ j) (hjk : j ⟶ k),
      trans (CategoryTheory.CategoryStruct.comp hij hjk) = CategoryTheory.CategoryStruct.comp (trans hij) (trans hjk))
  (w : ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), CategoryTheory.CategoryStruct.comp (trans hij) (𝒰.f j) = 𝒰.f i)
  (directed :
    ∀ {i j : 𝒰.I₀} (x : ↥(CategoryTheory.Limits.pullback (𝒰.f i) (𝒰.f j))),
      ∃ k hki hkj y, (CategoryTheory.Limits.pullback.lift (trans hki) (trans hkj) ⋯) y = x)
  (property_trans : ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), P (trans hij)),
  { trans := trans, trans_id := trans_id, trans_comp := trans_comp, w := w, directed := directed,
      property_trans := property_trans } =
    { trans := trans_1, trans_id := ⋯, trans_comp := ⋯, w := ⋯, directed := ⋯, property_trans := ⋯ }
-- Mathlib.AlgebraicGeometry.AffineScheme
/-- Given `f : X ⟶ Spec A` and some ideal `I ≤ ker(A ⟶ Γ(X, ⊤))`,
this is the lift to `X ⟶ Spec (A ⧸ I)`.  -/
AlgebraicGeometry.Scheme.Hom.liftQuotient : {X : AlgebraicGeometry.Scheme} →
  {A : CommRingCat} →
    (f : X.Hom (AlgebraicGeometry.Spec A)) →
      (I : Ideal ↑A) →
        I ≤
            RingHom.ker
              (CommRingCat.Hom.hom
                (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso A).inv f.appTop)) →
          (X ⟶ AlgebraicGeometry.Spec (CommRingCat.of (↑A ⧸ I)))
-- Mathlib.Algebra.Order.Nonneg.Field
Nonneg.coe_inv : ∀ {α : Type u_1} [inst : Semifield α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] (a : { x // 0 ≤ x }),
  ↑a⁻¹ = (↑a)⁻¹
-- Mathlib.CategoryTheory.Category.RelCat
CategoryTheory.RelCat.Hom.rel_comp : ∀ {X Y Z : CategoryTheory.RelCat} (f : X ⟶ Y) (g : Y ⟶ Z),
  (CategoryTheory.CategoryStruct.comp f g).rel = f.rel.comp g.rel
-- Std.Do.WP.SimpLemmas
Std.Do.WP.lift_StateT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α σ : Type u} {Q : Std.Do.PostCond α (Std.Do.PostShape.arg σ ps)}
  [inst : Std.Do.WP m ps] [inst_1 : Monad m] (x : m α),
  (Std.Do.wp (StateT.lift x)).apply Q = (Std.Do.wp (MonadLift.monadLift x)).apply Q
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
/-- Pull-out property of the conditional expectation.  -/
MeasureTheory.condExp_bilin_of_aestronglyMeasurable_right : ∀ {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {E : Type u_2} {F : Type u_3} {G : Type u_4}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F]
  [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G] [CompleteSpace G] (B : F →L[ℝ] E →L[ℝ] G) [CompleteSpace F]
  {f : Ω → F} {g : Ω → E},
  MeasureTheory.AEStronglyMeasurable g μ →
    MeasureTheory.Integrable (fun ω => (B (f ω)) (g ω)) μ →
      MeasureTheory.Integrable f μ → μ[fun ω => (B (f ω)) (g ω) | m] =ᵐ[μ] fun ω => (B (μ[f | m] ω)) (g ω)
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.PartialIso.mk.sizeOf_spec : ∀ {X Y : AlgebraicGeometry.Scheme} (source : X.Opens) (dense_source : Dense ↑source) (target : Y.Opens)
  (dense_target : Dense ↑target) (iso : ↑source ≅ ↑target),
  sizeOf
      { source := source, dense_source := dense_source, target := target, dense_target := dense_target, iso := iso } =
    1 + sizeOf source + sizeOf target + sizeOf iso
-- Mathlib.Algebra.Module.Submodule.Equiv
/-- Given `p` a submodule of the module `M` and `q` a submodule of `p`, `p.equivSubtypeMap q`
is the natural `LinearEquiv` between `q` and `q.map p.subtype`.  -/
Submodule.equivSubtypeMap : {R : Type u_1} →
  {M : Type u_5} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] → (p : Submodule R M) → (q : Submodule R ↥p) → ↥q ≃ₗ[R] ↥(Submodule.map p.subtype q)
-- Mathlib.LinearAlgebra.RootSystem.Chain
RootPairing.root_chainBotIdx : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : CharZero R] [inst_3 : IsDomain R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsCrystallographic] {i j : ι},
  P.root (RootPairing.chainBotIdx i j) = P.root j - RootPairing.chainBotCoeff i j • P.root i
-- Mathlib.Algebra.Order.Ring.Basic
Odd.pow_neg_iff : ∀ {R : Type u_3} [inst : Semiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {a : R} {n : ℕ} [ExistsAddOfLE R],
  Odd n → (a ^ n < 0 ↔ a < 0)
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.vadd_set_pi_of_surjective : ∀ {M : Type u_5} {ι : Type u_6} {π : ι → Type u_7} [inst : (i : ι) → VAdd M (π i)] (c : M) (I : Set ι)
  (s : (i : ι) → Set (π i)), (∀ i ∉ I, Function.Surjective fun x => c +ᵥ x) → c +ᵥ I.pi s = I.pi (c +ᵥ s)
-- Mathlib.Algebra.Ring.Opposite
/-- A ring hom `R →+* S` can equivalently be viewed as a ring hom `Rᵐᵒᵖ →+* Sᵐᵒᵖ`. This is the
action of the (fully faithful) `ᵐᵒᵖ`-functor on morphisms.  -/
RingHom.op : {R : Type u_2} →
  {S : Type u_3} → [inst : NonAssocSemiring R] → [inst_1 : NonAssocSemiring S] → (R →+* S) ≃ (Rᵐᵒᵖ →+* Sᵐᵒᵖ)
-- Mathlib.LinearAlgebra.Dimension.Basic
LinearIndependent.cardinal_le_rank : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Nontrivial R]
  {ι : Type v} {v : ι → M}, LinearIndependent R v → Cardinal.mk ι ≤ Module.rank R M
-- Mathlib.Topology.EMetricSpace.PairReduction
PairReduction.logSizeBallStruct.ball.eq_1 : ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] (struct : PairReduction.logSizeBallStruct T) (c : ENNReal),
  struct.ball c = {x ∈ struct.finset | edist struct.point x ≤ ↑struct.radius * c}
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.isCentralScalar : ∀ {S : Type u'} {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : MulAction R M] [inst_2 : SMul S R]
  [inst_3 : SMul S M] [inst_4 : IsScalarTower S R M] (p : SubMulAction R M) [inst_5 : SMul Sᵐᵒᵖ R]
  [inst_6 : SMul Sᵐᵒᵖ M] [inst_7 : IsScalarTower Sᵐᵒᵖ R M] [IsCentralScalar S M], IsCentralScalar S ↥p
-- Mathlib.Topology.EMetricSpace.Lipschitz
LocallyLipschitzOn.continuousOn : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β} {s : Set α},
  LocallyLipschitzOn s f → ContinuousOn f s
-- Batteries.Data.Char.Basic
/-- Number of valid character code points.
(See [unicode scalar value](https://www.unicode.org/glossary/#unicode_scalar_value).)
 -/
Char.count : ℕ
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentColorParams.toWorkDoneProgressParams : Lean.Lsp.DocumentColorParams → Lean.Lsp.WorkDoneProgressParams
-- Mathlib.Algebra.Group.Defs
MulOne.ext : ∀ {M : Type u_2} {x y : MulOne M}, One.one = One.one → Mul.mul = Mul.mul → x = y
-- Mathlib.Algebra.BigOperators.Associated
Multiset.prod_ne_zero_of_prime : ∀ {M₀ : Type u_3} [inst : CommMonoidWithZero M₀] [NoZeroDivisors M₀] [Nontrivial M₀] (s : Multiset M₀),
  (∀ x ∈ s, Prime x) → s.prod ≠ 0
-- Mathlib.Probability.Kernel.Posterior
ProbabilityTheory.posterior_eq_withDensity_of_countable : ∀ {𝓧 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {Ω : Type u_5} [Countable Ω] [inst : MeasurableSpace Ω] [inst_1 : Nonempty Ω]
  [inst_2 : StandardBorelSpace Ω] (κ : ProbabilityTheory.Kernel Ω 𝓧) [inst_3 : ProbabilityTheory.IsFiniteKernel κ]
  (μ : MeasureTheory.Measure Ω) [inst_4 : MeasureTheory.IsFiniteMeasure μ],
  ∀ᵐ (x : 𝓧) ∂μ.bind ⇑κ, (ProbabilityTheory.posterior κ μ) x = μ.withDensity fun ω => (κ ω).rnDeriv (μ.bind ⇑κ) x
-- Lean.Data.Lsp.Basic
Lean.Lsp.RenameFile.mk.sizeOf_spec : ∀ (oldUri newUri : Lean.Lsp.DocumentUri) (options? : Option Lean.Lsp.CreateFile.Options)
  (annotationId? : Option String),
  sizeOf { oldUri := oldUri, newUri := newUri, options? := options?, annotationId? := annotationId? } =
    1 + sizeOf oldUri + sizeOf newUri + sizeOf options? + sizeOf annotationId?
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ofArray_fold_fn.match_3.eq_1 : ∀ {n : ℕ} (motive : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → Sort u_1) (h_1 : Unit → motive none)
  (h_2 : (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → motive (some c)),
  (match none with
    | none => h_1 ()
    | some c => h_2 c) =
    h_1 ()
-- Mathlib.Tactic.Order.CollectFacts
/-- Monad for the fact collection procedure.  -/
Mathlib.Tactic.Order.CollectFactsM : Type → Type
-- Lean.Elab.InfoTree.Types
Lean.Elab.instInhabitedFieldInfo.default : Lean.Elab.FieldInfo
-- Mathlib.Data.List.Sort
/-- `l.SortedGT` means that the list is strictly antitonic.  -/
List.SortedGT : {α : Type u_1} → [Preorder α] → List α → Prop
-- Mathlib.Analysis.Complex.Trigonometric
Real.cos_zero : Real.cos 0 = 1
-- Lean.Data.Json.FromToJson.Basic
Lean.instFromJsonString : Lean.FromJson String
-- Mathlib.CategoryTheory.Generator.Sheaf
/-- Given `J : GrothendieckTopology C`, `X : C` and `M : A`, this is the associated
sheaf to the presheaf `Presheaf.freeYoneda X M`.  -/
CategoryTheory.Sheaf.freeYoneda : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {A : Type u'} →
        [inst_1 : CategoryTheory.Category.{v', u'} A] →
          [CategoryTheory.Limits.HasCoproducts A] →
            [CategoryTheory.HasWeakSheafify J A] → C → A → CategoryTheory.Sheaf J A
-- Mathlib.Algebra.Order.Group.Multiset
Multiset.coe_countPAddMonoidHom : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p], ⇑(Multiset.countPAddMonoidHom p) = Multiset.countP p
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- The characteristic map of the `n`-cell given by the index `i`.
This map is a bijection when restricting to `ball 0 1`, where we consider `(Fin n → ℝ)`
endowed with the maximum metric.  -/
Topology.RelCWComplex.map : {X : Type u} →
  {inst : TopologicalSpace X} →
    {C : Set X} →
      {D : outParam (Set X)} →
        [self : Topology.RelCWComplex C D] → (n : ℕ) → Topology.RelCWComplex.cell C n → PartialEquiv (Fin n → ℝ) X
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_Ioc_cast : ∀ {M : Type u_2} [inst : CommMonoid M] {n m : ℕ} (h : n = m) (f : Fin m → M) (a b : Fin n),
  ∏ i ∈ Finset.Ioc (Fin.cast h a) (Fin.cast h b), f i = ∏ i ∈ Finset.Ioc a b, f (Fin.cast h i)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.inter_eq : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β}, m₁.inter m₂ = m₁ ∩ m₂
-- Mathlib.Algebra.Group.Submonoid.Saturation
/-- If `M` is commutative, we only need to check the right condition `y ∈ s`.  -/
AddSubmonoid.AddSaturated.of_right : ∀ {M : Type u_2} [inst : AddCommMonoid M] {s : AddSubmonoid M}, (∀ ⦃x y : M⦄, x + y ∈ s → y ∈ s) → s.AddSaturated
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
CategoryTheory.Functor.preservesZeroMorphisms_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_4 : CategoryTheory.Limits.HasZeroMorphisms D] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [F.PreservesZeroMorphisms]
  [G.PreservesZeroMorphisms], (F.comp G).PreservesZeroMorphisms
-- Mathlib.Algebra.Star.Pointwise
Set.nonempty_star : ∀ {α : Type u_1} [inst : InvolutiveStar α] {s : Set α}, (star s).Nonempty ↔ s.Nonempty
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintKind.parameter.sizeOf_spec : sizeOf Lean.Elab.InlayHintKind.parameter = 1
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Var.revlex : Lean.Grind.CommRing.Var → Lean.Grind.CommRing.Var → Ordering
-- Mathlib.Algebra.Order.ToIntervalMod
toIocDiv_eq_neg_floor : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] [inst_3 : FloorRing α]
  {p : α} (hp : 0 < p) (a b : α), toIocDiv hp a b = -⌊(a + p - b) / p⌋
-- Mathlib.RingTheory.SimpleModule.Isotypic
/-- An `R`-module `M` is isotypic if all its simple submodules are isomorphic.  -/
IsIsotypic : (R : Type u_2) → (M : Type u) → [inst : Ring R] → [inst_1 : AddCommGroup M] → [Module R M] → Prop
-- Mathlib.Algebra.Order.GroupWithZero.Basic
mul_le_iff_le_one_left : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Zero α] {a b : α} [inst_2 : Preorder α] [MulPosMono α]
  [MulPosReflectLE α], 0 < b → (a * b ≤ b ↔ a ≤ 1)
-- Init.Data.UInt.Lemmas
UInt32.toUSize_ofNatTruncate_of_lt : ∀ {n : ℕ} (hn : n < UInt32.size), (UInt32.ofNatClamp n).toUSize = USize.ofNatLT n ⋯
-- Mathlib.Topology.Algebra.Star
continuousWithinAt_star : ∀ {R : Type u_2} [inst : TopologicalSpace R] [inst_1 : Star R] [ContinuousStar R] {s : Set R} {x : R},
  ContinuousWithinAt star s x
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.uniqueUpToIso_inv : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {s t : CategoryTheory.Limits.Cone F} (P : CategoryTheory.Limits.IsLimit s)
  (Q : CategoryTheory.Limits.IsLimit t), (P.uniqueUpToIso Q).inv = P.liftConeMorphism t
-- Mathlib.Data.Matrix.Mul
Matrix.add_mulVec : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype n]
  (A B : Matrix m n α) (x : n → α), (A + B).mulVec x = A.mulVec x + B.mulVec x
-- Init.Data.Array.Basic
Array.toArray_toList : ∀ {α : Type u} {xs : Array α}, xs.toList.toArray = xs
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.skip?_startPos : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s : String.Slice}, s.startPos.skip? pat = s.skipPrefix? pat
-- Mathlib.RingTheory.Extension.Cotangent.BaseChange
Ideal.Cotangent.equivOfEq.congr_simp : ∀ {R : Type u} [inst : CommRing R] (I J : Ideal R) (hIJ : I = J),
  Ideal.Cotangent.equivOfEq I J hIJ = Ideal.Cotangent.equivOfEq I J hIJ
-- Mathlib.Data.DFinsupp.BigOperators
/-- Evaluation at a point is an `AddMonoidHom`. This is the finitely-supported version of
`Pi.evalAddMonoidHom`.  -/
DFinsupp.evalAddMonoidHom : {ι : Type u} → {β : ι → Type v} → [inst : (i : ι) → AddZeroClass (β i)] → (i : ι) → (Π₀ (i : ι), β i) →+ β i