mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Integral.TorusIntegral
torusIntegral_smul : ∀ {n : ℕ} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {𝕜 : Type u_2} [inst_2 : RCLike 𝕜]
  [inst_3 : NormedSpace 𝕜 E] [SMulCommClass 𝕜 ℂ E] (a : 𝕜) (f : (Fin n → ℂ) → E) (c : Fin n → ℂ) (R : Fin n → ℝ),
  (∯ (x : Fin n → ℂ) in T(c, R), a • f x) = a • ∯ (x : Fin n → ℂ) in T(c, R), f x
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instInhabitedLetValue.default : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.LetValue pu
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Pi.functor_obj : ∀ (α : Type w₂) {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasProductsOfShape α C] (f : α → C), (CategoryTheory.Limits.Pi.functor α).obj f = ∏ᶜ f
-- Mathlib.Algebra.Polynomial.Expand
Polynomial.expand_contract : ∀ {R : Type u} [inst : CommSemiring R] (p : ℕ) [CharP R p] [NoZeroDivisors R] {f : Polynomial R},
  Polynomial.derivative f = 0 → p ≠ 0 → (Polynomial.expand R p) (Polynomial.contract p f) = f
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.IsZariskiLocalAtSource.sigmaDesc : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsZariskiLocalAtSource P]
  {X : AlgebraicGeometry.Scheme} {ι : Type v} [inst : Small.{u, v} ι] {Y : ι → AlgebraicGeometry.Scheme}
  {f : (i : ι) → Y i ⟶ X}, (∀ (i : ι), P (f i)) → P (CategoryTheory.Limits.Sigma.desc f)
-- Batteries.Data.Array.Scan
Array.scanl_extract : ∀ {β : Type u_1} {α : Type u_2} {start stop : ℕ} {init : β} {f : β → α → β} {as : Array α},
  Array.scanl f init (as.extract start stop) = Array.scanl f init as start stop
-- Mathlib.Analysis.Analytic.IteratedFDeriv
_private.Mathlib.Analysis.Analytic.IteratedFDeriv.0.FormalMultilinearSeries.iteratedFDerivSeries.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (k : ℕ) (h_1 : Unit → motive 0) (h_2 : (k : ℕ) → motive k.succ),
  (match k.succ with
    | 0 => h_1 ()
    | k.succ => h_2 k) =
    h_2 k
-- Mathlib.Condensed.Discrete.Module
CompHausLike.LocallyConstantModule.functorToPresheaves_map_app : ∀ {P : TopCat → Prop} (R : Type (max u w)) [inst : Ring R] {X Y : ModuleCat R} (f : X ⟶ Y) (S : (CompHausLike P)ᵒᵖ),
  ((CompHausLike.LocallyConstantModule.functorToPresheaves R).map f).app S =
    ModuleCat.ofHom (LocallyConstant.mapₗ R (ModuleCat.Hom.hom f))
-- Mathlib.GroupTheory.Solvable
Group.isSolvable_of_ker_le_range : ∀ {G : Type u_1} [inst : Group G] {G' : Type u_3} {G'' : Type u_4} [inst_1 : Group G'] [inst_2 : Group G'']
  (f : G' →* G) (g : G →* G''),
  g.ker ≤ f.range → ∀ [hG' : Group.IsSolvable G'] [hG'' : Group.IsSolvable G''], Group.IsSolvable G
-- Mathlib.FieldTheory.Normal.Closure
normalClosure.instIsScalarTowerSubtypeMemIntermediateFieldNormalClosure_1 : ∀ (F : Type u_1) (K : Type u_2) (L : Type u_3) [inst : Field F] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra F K] [inst_4 : Algebra F L] [inst_5 : Algebra K L] [inst_6 : IsScalarTower F K L],
  IsScalarTower K (↥(IntermediateField.normalClosure F K L)) L
-- Mathlib.Analysis.Normed.Group.Hom
/-- The operator norm satisfies the triangle inequality.  -/
NormedAddGroupHom.opNorm_add_le : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
  (f g : NormedAddGroupHom V₁ V₂), ‖f + g‖ ≤ ‖f‖ + ‖g‖
-- Mathlib.Topology.Order.Lattice
ContinuousOn.inf : ∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] [inst_2 : Min L]
  [ContinuousInf L] {f g : X → L} {s : Set X}, ContinuousOn f s → ContinuousOn g s → ContinuousOn (fun a => f a ⊓ g a) s
-- Mathlib.Order.WithBot
WithBot.decidableLE.eq_1 : ∀ {α : Type u_1} [inst : LE α] [inst_1 : DecidableLE α] (x : WithBot α), WithBot.decidableLE none x = isTrue ⋯
-- Init.Conv
/-- `with_annotate_state stx t` annotates the lexical range of `stx : Syntax` with
the initial and final state of running tactic `t`.
 -/
Lean.Parser.Tactic.Conv.withAnnotateState : Lean.ParserDescr
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.shortComplexFunctor_map_τ₂ : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} (c : ComplexShape ι) (i : ι) {X Y : HomologicalComplex C c} (f : X ⟶ Y),
  ((HomologicalComplex.shortComplexFunctor C c i).map f).τ₂ = f.f i
-- Lean.ReducibilityAttrs
/-- Return `true` if the given declaration has been marked as `[implicit_reducible]`.  -/
Lean.isImplicitReducible : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Lean.Name → m Bool
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.Hom.algebraMap_toAlgHom : ∀ {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'] [IsScalarTower R R' S'] [IsScalarTower R S S'] (f : P.Hom P')
  (x : P.Ring), (MvPolynomial.aeval P'.val) (f.toAlgHom x) = (algebraMap S S') ((MvPolynomial.aeval P.val) x)
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.setRange_algebraMap : ∀ {R : Type u_3} {A : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  (S : Subalgebra R A), Set.range ⇑(algebraMap (↥S) A) = ↑S
-- Mathlib.Topology.Algebra.Algebra.Equiv
/-- The inverse of a continuous algebra equivalence.  -/
ContinuousAlgEquiv.symm : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : TopologicalSpace A] →
            [inst_3 : Semiring B] →
              [inst_4 : TopologicalSpace B] → [inst_5 : Algebra R A] → [inst_6 : Algebra R B] → (A ≃A[R] B) → B ≃A[R] A
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.mem_insert_of_mem_toList : ∀ {α : Type u_1} {cmp : α → α → Ordering} {v' : α} [Std.OrientedCmp cmp] (v : α) {t : RBTree.RBSet α cmp},
  v' ∈ t.toList → v' ∈ t.insert v
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.NormalizePattern.State.symbolSet : Lean.Meta.Grind.NormalizePattern.State → Std.HashSet Lean.HeadIndex
-- Mathlib.Topology.Category.TopCat.Limits.Products
TopCat.isInducing_prodMap : ∀ {W X Y Z : TopCat} {f : W ⟶ X} {g : Y ⟶ Z},
  Topology.IsInducing ⇑(CategoryTheory.ConcreteCategory.hom f) →
    Topology.IsInducing ⇑(CategoryTheory.ConcreteCategory.hom g) →
      Topology.IsInducing ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.prod.map f g))
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.hasRightResolutions_arrow_iff_of_equivalences : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {W₁' : CategoryTheory.MorphismProperty D₁}
  {W₂' : CategoryTheory.MorphismProperty D₂} {T : CategoryTheory.LocalizerMorphism W₁ W₂}
  {L : CategoryTheory.LocalizerMorphism W₁ W₁'} {R : CategoryTheory.LocalizerMorphism W₂ W₂'}
  {B : CategoryTheory.LocalizerMorphism W₁' W₂'} [R.functor.IsEquivalence] [R.IsInduced] [L.functor.IsEquivalence]
  [W₂'.RespectsIso] (iso : T.functor.comp R.functor ≅ L.functor.comp B.functor),
  T.arrow.HasRightResolutions ↔ B.arrow.HasRightResolutions
-- Mathlib.LinearAlgebra.TensorProduct.DirectLimit
TensorProduct.directLimitLeft_rTensor_of : ∀ {R : Type u_1} [inst : CommSemiring R] {ι : Type u_2} [inst_1 : DecidableEq ι] [inst_2 : Preorder ι]
  {G : ι → Type u_3} [inst_3 : (i : ι) → AddCommMonoid (G i)] [inst_4 : (i : ι) → Module R (G i)]
  (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) (M : Type u_4) [inst_5 : AddCommMonoid M] [inst_6 : Module R M] {i : ι}
  (x : TensorProduct R (G i) M),
  (TensorProduct.directLimitLeft f M) ((LinearMap.rTensor M (Module.DirectLimit.of R ι G f i)) x) =
    (Module.DirectLimit.of R ι (fun i => TensorProduct R (G i) M) (fun i j h => LinearMap.rTensor M (f i j h)) i) x
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.filter_true : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I), (π.filter fun x => True) = π
-- Std.Data.TreeMap.Basic
Std.TreeMap.instInsertProd : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Insert (α × β) (Std.TreeMap α β cmp)
-- Mathlib.Topology.Order.Basic
PredOrder.hasBasis_nhds_Ico_of_exists_gt : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [PredOrder α] {a : α},
  (∃ l, a < l) → (nhds a).HasBasis (fun x => a < x) fun x => Set.Ico a x
-- Mathlib.Algebra.Module.Equiv.Defs
/-- The identity map is a linear equivalence.  -/
LinearEquiv.refl : (R : Type u_1) → (M : Type u_7) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → M ≃ₗ[R] M
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHom.id_comp : ∀ {M : Type u_4} {N : Type u_5} [inst : MulOne M] [inst_1 : MulOne N] (f : M →* N), (MonoidHom.id N).comp f = f
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₁₂.hom_ext : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_3} C₁₂] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₁₂] [inst_9 : CategoryTheory.Preadditive C₄]
  {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)}
  {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} [inst_10 : F₁₂.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [inst_12 : G.Additive]
  [inst_13 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9}
  {ι₁₂ : Type u_10} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} {K₁ : HomologicalComplex C₁ c₁} {K₂ : HomologicalComplex C₂ c₂} {K₃ : HomologicalComplex C₃ c₃}
  {c₁₂ : ComplexShape ι₁₂} {c₄ : ComplexShape ι₄} [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [inst_18 : DecidableEq ι₁₂]
  [inst_19 : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄]
  [HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄] {j : ι₄} {A : C₄}
  {f g : ((K₁.mapBifunctor K₂ F₁₂ c₁₂).mapBifunctor K₃ G c₄).X j ⟶ A},
  (∀ (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j),
      CategoryTheory.CategoryStruct.comp ⋯ f = CategoryTheory.CategoryStruct.comp ⋯ g) →
    f = g
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
_private.Init.Data.String.Lemmas.Pattern.TakeDrop.Basic.0.String.Slice.skipPrefix?.eq_1 : ∀ {ρ : Type} (s : String.Slice) (pat : ρ) [inst : String.Slice.Pattern.ForwardPattern pat],
  s.skipPrefix? pat = String.Slice.Pattern.ForwardPattern.skipPrefix? pat s
-- Mathlib.Topology.Algebra.Module.Basic
Submodule.topologicalClosure_minimal : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : ContinuousConstSMul R M] [inst_5 : ContinuousAdd M] (s : Submodule R M)
  {t : Submodule R M}, s ≤ t → IsClosed ↑t → s.topologicalClosure ≤ t
-- Mathlib.Data.Quot
Quotient.map₂'_mk'' : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {s₁ : Setoid α} {s₂ : Setoid β} {s₃ : Setoid γ} (f : α → β → γ)
  (h : ∀ ⦃a₁ a₂ : α⦄, s₁ a₁ a₂ → ∀ ⦃b₁ b₂ : β⦄, s₂ b₁ b₂ → s₃ (f a₁ b₁) (f a₂ b₂)) (x : α),
  Quotient.map₂' f h (Quotient.mk'' x) = Quotient.map' (f x) ⋯
-- Init.Data.String.Pattern.String
String.Slice.Pattern.ForwardSliceSearcher.emptyAt.inj : ∀ {s : String.Slice} {pos : s.Pos} {h : pos ≠ s.endPos} {pos_1 : s.Pos} {h_1 : pos_1 ≠ s.endPos},
  String.Slice.Pattern.ForwardSliceSearcher.emptyAt pos h =
      String.Slice.Pattern.ForwardSliceSearcher.emptyAt pos_1 h_1 →
    pos = pos_1
-- Mathlib.Data.WSeq.Productive
Stream'.WSeq.Productive.mk : ∀ {α : Type u} {s : Stream'.WSeq α}, (∀ (n : ℕ), (s.get? n).Terminates) → s.Productive
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Given three nonzero vectors, the angle between the first and the third minus the angle
between the second and the third equals the angle between the first and the second.  -/
Orientation.oangle_sub_right : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y z : V}, x ≠ 0 → y ≠ 0 → z ≠ 0 → o.oangle x z - o.oangle y z = o.oangle x y
-- Init.Data.List.Sort.Lemmas
List.mergeSort_nil : ∀ {α : Type u_1} {r : α → α → Bool}, [].mergeSort r = []
-- Mathlib.Data.PEquiv
PEquiv.mk.injEq : ∀ {α : Type u} {β : Type v} (toFun : α → Option β) (invFun : β → Option α)
  (inv : ∀ (a : α) (b : β), invFun b = some a ↔ toFun a = some b) (toFun_1 : α → Option β) (invFun_1 : β → Option α)
  (inv_1 : ∀ (a : α) (b : β), invFun_1 b = some a ↔ toFun_1 a = some b),
  ({ toFun := toFun, invFun := invFun, inv := inv } = { toFun := toFun_1, invFun := invFun_1, inv := inv_1 }) =
    (toFun = toFun_1 ∧ invFun = invFun_1)
-- Mathlib.Logic.Equiv.Defs
Quot.map.eq_1 : ∀ {α : Sort u_1} {β : Sort u_2} {ra : α → α → Prop} {rb : β → β → Prop} (f : α → β)
  (h : ∀ ⦃a b : α⦄, ra a b → rb (f a) (f b)), Quot.map f h = Quot.lift (fun x => Quot.mk rb (f x)) ⋯
-- Mathlib.Algebra.Category.Ring.Constructions
CommRingCat.pullback_isLocalRing : ∀ {A B C : CommRingCat} (f : A ⟶ C) (g : B ⟶ C) [IsLocalHom (CommRingCat.Hom.hom g)] [IsLocalRing ↑A],
  IsLocalRing ↑(CategoryTheory.Limits.pullback f g)
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.eq_empty_or_nonempty : ∀ (u : ZFSet.{u_1}), u = ∅ ∨ u.Nonempty
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.sInf_toAddSubmonoid : ∀ {R : Type u} [inst : NonAssocSemiring R] (s : Set (Subsemiring R)),
  (sInf s).toAddSubmonoid = ⨅ t ∈ s, t.toAddSubmonoid
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- Given a morphism property `P` on a category `T`, this is the
subcategory of `Arrow T` defined by `P` where morphisms satisfy `Q` and `W` on the left and right,
respectively.  -/
CategoryTheory.MorphismProperty.Arrow : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    CategoryTheory.MorphismProperty T →
      CategoryTheory.MorphismProperty T → CategoryTheory.MorphismProperty T → Type (max v_1 u_1)
-- Mathlib.CategoryTheory.Monad.Kleisli
CategoryTheory.Kleisli.Adjunction.toKleisli_obj_of : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (T : CategoryTheory.Monad C) (X : C),
  ((CategoryTheory.Kleisli.Adjunction.toKleisli T).obj X).of = X
-- Mathlib.Topology.Bornology.Basic
OrderDual.instBornology : {α : Type u_2} → [Bornology α] → Bornology αᵒᵈ
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentColorOptions.mk : Lean.Lsp.WorkDoneProgressOptions → Lean.Lsp.DocumentColorOptions
-- Lean.Elab.Level
Lean.Elab.Level.State.ngen : Lean.Elab.Level.State → Lean.NameGenerator
-- Mathlib.Data.Sign.Defs
instFintypeSignType : Fintype SignType
-- Mathlib.RingTheory.Algebraic.Basic
Polynomial.algEquivOfTranscendental_apply : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] (s : S)
  (h : Transcendental R s) (f : Polynomial R),
  (Polynomial.algEquivOfTranscendental R s h) f = (Polynomial.aeval ⟨s, ⋯⟩) f
-- Init.Data.List.Attach
/-- If we fold over `l.attach` with a function that ignores the membership predicate,
we get the same results as folding over `l` directly.

This is useful when we need to use `attach` to show termination.

Unfortunately this can't be applied by `simp` because of the higher order unification problem,
and even when rewriting we need to specify the function explicitly.
See however `foldr_subtype` below.
 -/
List.foldr_attach : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : α → β → β} {b : β},
  List.foldr (fun t acc => f (↑t) acc) b l.attach = List.foldr f b l
-- Mathlib.Logic.Equiv.Basic
Equiv.Perm.extendDomain_trans : ∀ {α' : Type u_9} {β' : Type u_10} {p : β' → Prop} [inst : DecidablePred p] (f : α' ≃ Subtype p) (e e' : Equiv.Perm α'),
  Equiv.trans (e.extendDomain f) (e'.extendDomain f) = Equiv.Perm.extendDomain (Equiv.trans e e') f
-- Mathlib.AlgebraicTopology.SimplicialSet.Simplices
/-- the simplex  -/
SSet.S.simplex : {X : SSet} → (self : X.S) → X.obj (Opposite.op { len := self.dim })
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.xRep_some : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} {x y : R} (h : W'.Nonsingular x y),
  (WeierstrassCurve.Affine.Point.some x y h).xRep = ![x, 1]
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
/-- The coordinates of a representative of `P + Q` for two distinct Jacobian point
representatives `P` and `Q` on a Weierstrass curve.

If the representatives of `P` and `Q` are equal, then this returns the value `![0, 0, 0]`.  -/
WeierstrassCurve.Jacobian.addXYZ : {R : Type r} → [CommRing R] → WeierstrassCurve.Jacobian R → (Fin 3 → R) → (Fin 3 → R) → Fin 3 → R
-- Lean.Elab.Tactic.Grind.Basic
/-- Cache key for `Sym.dsimp` variant invocations.  -/
Lean.Elab.Tactic.Grind.DSimpCacheKey : Type
-- Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
/-- We say that `μ` is absolutely continuous with respect to `ν`, or that `μ` is dominated by `ν`,
if `ν(A) = 0` implies that `μ(A) = 0`.  -/
MeasureTheory.«term_≪_» : Lean.TrailingParserDescr
-- Mathlib.Topology.Algebra.Module.IsWeak
LinearMap.IsWeak.instFlip : ∀ {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜]
  [inst_2 : AddCommMonoid E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommMonoid F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace E] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [hB : B.IsWeak], B.flip.flip.IsWeak
-- Mathlib.Topology.Algebra.InfiniteSum.Order
Multipliable.tprod_ne_one_iff : ∀ {ι : Type u_1} {α : Type u_3} [inst : CommMonoid α] [inst_1 : PartialOrder α] [IsOrderedMonoid α]
  [CanonicallyOrderedMul α] [inst_4 : TopologicalSpace α] [OrderClosedTopology α] {f : ι → α},
  Multipliable f → (∏' (i : ι), f i ≠ 1 ↔ ∃ x, f x ≠ 1)
-- Mathlib.Analysis.Seminorm
Seminorm.bot_eq_zero : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E], ⊥ = 0
-- Mathlib.Order.Category.DistLat
/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas.  -/
DistLat.Hom.Simps.hom : (X Y : DistLat) → X.Hom Y → LatticeHom ↑X ↑Y
-- Std.Time.Duration
/-- Adds a `Day.Offset` to a `Duration`
 -/
Std.Time.Duration.addDays : Std.Time.Duration → Std.Time.Day.Offset → Std.Time.Duration
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.mk.injEq : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2]
  [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2] (toFun : P1 → P2) (linear : V1 →ₗ[k] V2)
  (map_vadd' : ∀ (p : P1) (v : V1), toFun (v +ᵥ p) = linear v +ᵥ toFun p) (toFun_1 : P1 → P2) (linear_1 : V1 →ₗ[k] V2)
  (map_vadd'_1 : ∀ (p : P1) (v : V1), toFun_1 (v +ᵥ p) = linear_1 v +ᵥ toFun_1 p),
  ({ toFun := toFun, linear := linear, map_vadd' := map_vadd' } =
      { toFun := toFun_1, linear := linear_1, map_vadd' := map_vadd'_1 }) =
    (toFun = toFun_1 ∧ linear = linear_1)
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.tendsto_integral_Iio_zero : ∀ {ι : Type u_1} {E : Type u_2} {μ : MeasureTheory.Measure ℝ} {l : Filter ι} [l.IsCountablyGenerated]
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a : ι → ℝ} {f : ℝ → E},
  Filter.Tendsto a l Filter.atBot → Filter.Tendsto (fun i => ∫ (x : ℝ) in Set.Iio (a i), f x ∂μ) l (nhds 0)
-- Mathlib.Logic.Function.Iterate
Function.Commute.comp_iterate : ∀ {α : Type u} {f g : α → α}, Function.Commute f g → ∀ (n : ℕ), (f ∘ g)^[n] = f^[n] ∘ g^[n]
-- Mathlib.Algebra.Star.CHSH
IsCHSHTuple.A₁B₁_commutes : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] {A₀ A₁ B₀ B₁ : R}, IsCHSHTuple A₀ A₁ B₀ B₁ → A₁ * B₁ = B₁ * A₁
-- Mathlib.Topology.Bases
/-- In a first-countable space, a cluster point `x` of a countably generated filter is the limit of
some sequence.  -/
ClusterPt.exists_seq_tendsto : ∀ {α : Type u} [t : TopologicalSpace α] [FirstCountableTopology α] {x : α} {f : Filter α} [f.IsCountablyGenerated],
  ClusterPt x f → ∃ ψ, Filter.Tendsto ψ Filter.atTop (nhds x) ∧ Filter.Tendsto ψ Filter.atTop f
-- Mathlib.Analysis.Seminorm
Seminorm.instModule : {R : Type u_1} →
  {𝕜 : Type u_3} →
    {E : Type u_7} →
      [inst : SeminormedRing 𝕜] →
        [inst_1 : AddGroup E] →
          [inst_2 : SMul 𝕜 E] →
            [inst_3 : Semiring R] →
              [inst_4 : Module R ℝ] → [inst_5 : SMul R NNReal] → [IsScalarTower R NNReal ℝ] → Module R (Seminorm 𝕜 E)
-- Mathlib.Analysis.SpecificLimits.Normed
tendsto_smul_congr_of_tendsto_left_cobounded_of_isBoundedUnder : ∀ {α : Type u_1} {R : Type u_4} {K : Type u_5} [inst : NormedRing K] [IsDomain K] [inst_2 : NormedAddCommGroup R]
  [inst_3 : Module K R] [Module.IsTorsionFree K R] [NormSMulClass K R] {f₁ f₂ : α → K} {g : α → R} {t : R}
  {l : Filter α},
  Filter.Tendsto (fun x => f₁ x • g x) l (nhds t) →
    Filter.Tendsto f₁ l (Bornology.cobounded K) →
      (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => ‖f₁ x - f₂ x‖) →
        Filter.Tendsto (fun x => f₂ x • g x) l (nhds t)
-- Lean.DocString.Types
Lean.Doc.Block.ul.sizeOf_spec : ∀ {i : Type u} {b : Type v} [inst : SizeOf i] [inst_1 : SizeOf b]
  (items : Array (Lean.Doc.ListItem (Lean.Doc.Block i b))), sizeOf (Lean.Doc.Block.ul items) = 1 + sizeOf items
-- Mathlib.Analysis.Calculus.FDeriv.Basic
HasFDerivAt.unique : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul 𝕜 E] {F : Type u_3} [inst_6 : AddCommGroup F]
  [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [ContinuousAdd F] [ContinuousSMul 𝕜 F] {f : E → F}
  {f' f₁' : E →L[𝕜] F} {x : E} [T2Space F], HasFDerivAt f f' x → HasFDerivAt f f₁' x → f' = f₁'
-- Mathlib.Combinatorics.SimpleGraph.Density
Rel.abs_edgeDensity_sub_edgeDensity_le_two_mul_sub_sq : ∀ {𝕜 : Type u_1} {α : Type u_4} {β : Type u_5} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  (r : α → β → Prop) [inst_3 : (a : α) → DecidablePred (r a)] {s₁ s₂ : Finset α} {t₁ t₂ : Finset β} {δ : 𝕜},
  s₂ ⊆ s₁ →
    t₂ ⊆ t₁ →
      0 ≤ δ →
        δ < 1 →
          (1 - δ) * ↑s₁.card ≤ ↑s₂.card →
            (1 - δ) * ↑t₁.card ≤ ↑t₂.card → |↑(Rel.edgeDensity r s₂ t₂) - ↑(Rel.edgeDensity r s₁ t₁)| ≤ 2 * δ - δ ^ 2
-- Mathlib.Order.Filter.Lift
Filter.mem_lift_sets : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Set α → Filter β},
  Monotone g → ∀ {s : Set β}, s ∈ f.lift g ↔ ∃ t ∈ f, s ∈ g t
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.liftRel_think_left : ∀ {α : Type u} {β : Type v} (R : α → β → Prop) (s : Stream'.WSeq α) (t : Stream'.WSeq β),
  Stream'.WSeq.LiftRel R s.think t ↔ Stream'.WSeq.LiftRel R s t
-- Mathlib.Algebra.Lie.Abelian
LieModule.maxTrivEquiv_of_refl_eq_refl : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M],
  LieModule.maxTrivEquiv LieModuleEquiv.refl = LieModuleEquiv.refl
-- Lean.Elab.PreDefinition.Basic
_private.Lean.Elab.PreDefinition.Basic.0.Lean.Elab.shouldGenCodeFor : Lean.Elab.PreDefinition → Bool