mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_union!_of_contains_eq_false_right : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited β],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        Std.DTreeMap.Internal.Impl.contains k m₂ = false →
          Std.DTreeMap.Internal.Impl.Const.get! (m₁.union! m₂) k = Std.DTreeMap.Internal.Impl.Const.get! m₁ k
-- Mathlib.Data.List.Basic
List.lookup_graph : ∀ {α : Type u} {β : Type v} [inst : BEq α] [LawfulBEq α] (f : α → β) {a : α} {as : List α},
  a ∈ as → List.lookup a (List.map (fun x => (x, f x)) as) = some (f a)
-- Mathlib.RepresentationTheory.Maschke
LinearMap.equivariantProjection_apply : ∀ {k : Type u_1} [inst : CommRing k] (G : Type u_2) [inst_1 : Group G] {V : Type u_3} [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [inst_4 : Module (MonoidAlgebra k G) V] [inst_5 : IsScalarTower k (MonoidAlgebra k G) V]
  {W : Type u_4} [inst_6 : AddCommGroup W] [inst_7 : Module k W] [inst_8 : Module (MonoidAlgebra k G) W]
  [inst_9 : IsScalarTower k (MonoidAlgebra k G) W] (π : W →ₗ[k] V) [inst_10 : Fintype G] (v : W),
  (LinearMap.equivariantProjection G π) v = Ring.inverse ↑(Nat.card G) • ∑ g, (π.conjugate g) v
-- Lean.Parser.Term
Lean.Parser.Term.macroArg.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Data.Multiset.Powerset
Multiset.powerset_aux'_perm : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Perm l₂ → (Multiset.powersetAux' l₁).Perm (Multiset.powersetAux' l₂)
-- Lean.Compiler.LCNF.Types
/-- `float` is a 64-bit floating point number.
 -/
Lean.Compiler.LCNF.ImpureType.float : Lean.Expr
-- Mathlib.FieldTheory.SplittingField.IsSplittingField
/-- Splitting field of `f` embeds into any field that splits `f`.  -/
Polynomial.IsSplittingField.lift : {F : Type u} →
  {K : Type v} →
    (L : Type w) →
      [inst : Field K] →
        [inst_1 : Field L] →
          [inst_2 : Field F] →
            [inst_3 : Algebra K L] →
              [inst_4 : Algebra K F] →
                (f : Polynomial K) →
                  [Polynomial.IsSplittingField K L f] → (Polynomial.map (algebraMap K F) f).Splits → L →ₐ[K] F
-- Mathlib.Combinatorics.SimpleGraph.Clique
/-- A graph's complement is `n`-independent set free iff it is `n`-clique free.  -/
SimpleGraph.indepSetFree_compl : ∀ {α : Type u_1} (G : SimpleGraph α) {n : ℕ}, Gᶜ.IndepSetFree n ↔ G.CliqueFree n
-- Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived
CategoryTheory.Functor.hasPointwiseRightDerivedFunctorAt_iff : ∀ {C : Type u₁} {D : Type u₂} {H : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] [inst_2 : CategoryTheory.Category.{v₃, u₃} H]
  (F : CategoryTheory.Functor C H) (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C)
  [L.IsLocalization W] (X : C), F.HasPointwiseRightDerivedFunctorAt W X ↔ L.HasPointwiseLeftKanExtensionAt F (L.obj X)
-- Init.Data.Rat.Lemmas
Rat.ceil_lt : ∀ {x : ℚ}, ↑x.ceil < x + 1
-- Lean.Elab.PatternVar
Lean.Elab.Term.CollectPatternVars.Context.explicit : Lean.Elab.Term.CollectPatternVars.Context → Bool
-- Lean.Elab.Tactic.Conv.Basic
/-- Given `lhs`, returns a pair of metavariables `(?rhs, ?newGoal)`
where `?newGoal : lhs = ?rhs`. `tag` is the name of `newGoal`.  -/
Lean.Elab.Tactic.Conv.mkConvGoalFor : Lean.Expr → optParam Lean.Name Lean.Name.anonymous → Lean.MetaM (Lean.Expr × Lean.Expr)
-- Init.Data.UInt.Lemmas
UInt64.ofNatClamp_bitVecToNat : ∀ (n : BitVec 64), UInt64.ofNatClamp n.toNat = { toBitVec := n }
-- Mathlib.CategoryTheory.Preadditive.OfBiproducts
CategoryTheory.SemiadditiveOfBinaryBiproducts.comp_add : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {X Y Z : C} (f : X ⟶ Y) (g h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp f (g + h) =
    CategoryTheory.CategoryStruct.comp f g + CategoryTheory.CategoryStruct.comp f h
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (left : S.LeftHomologyData) (right : S.RightHomologyData) (iso : left.H ≅ right.H)
  (comm :
    autoParam
      (CategoryTheory.CategoryStruct.comp left.π (CategoryTheory.CategoryStruct.comp iso.hom right.ι) =
        CategoryTheory.CategoryStruct.comp left.i right.p)
      CategoryTheory.ShortComplex.HomologyData.comm._autoParam)
  (left_1 : S.LeftHomologyData) (right_1 : S.RightHomologyData) (iso_1 : left_1.H ≅ right_1.H)
  (comm_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp left_1.π (CategoryTheory.CategoryStruct.comp iso_1.hom right_1.ι) =
        CategoryTheory.CategoryStruct.comp left_1.i right_1.p)
      CategoryTheory.ShortComplex.HomologyData.comm._autoParam),
  ({ left := left, right := right, iso := iso, comm := comm } =
      { left := left_1, right := right_1, iso := iso_1, comm := comm_1 }) =
    (left = left_1 ∧ right = right_1 ∧ iso ≍ iso_1)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVUnOp.eval_rotateRight : ∀ {n w : ℕ}, (Std.Tactic.BVDecide.BVUnOp.rotateRight n).eval = fun x => x.rotateRight n
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.equivLike_inv_eq_symm : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Mul α] [inst_3 : Mul β]
  (f : α ≃*o β), EquivLike.inv f = ⇑f.symm
-- Mathlib.NumberTheory.Padics.PadicNumbers
PadicSeq.stationaryPoint_spec : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {f : PadicSeq p} (hf : ¬f ≈ 0) {m n : ℕ},
  PadicSeq.stationaryPoint hf ≤ m → PadicSeq.stationaryPoint hf ≤ n → padicNorm p (↑f n) = padicNorm p (↑f m)
-- Mathlib.Algebra.Ring.Associator
/-- The associator `(x * y) * z - x * (y * z)`  -/
associator : {R : Type u_1} → [NonUnitalNonAssocRing R] → R → R → R → R
-- Init.Sym.Lemmas
Lean.Sym.Int16.eq_eq_true : ∀ (a b : Int16), decide (a = b) = true → (a = b) = True
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
hasLineDerivAt_iff_tendsto_slope_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {f : E → F} {f' : F}
  {x v : E},
  HasLineDerivAt 𝕜 f f' x v ↔ Filter.Tendsto (fun t => t⁻¹ • (f (x + t • v) - f x)) (nhdsWithin 0 {0}ᶜ) (nhds f')
-- Mathlib.Analysis.Real.Cardinality
/-- The cardinality of the interval $(a, b)$.  -/
Cardinal.mk_Ioo_real : ∀ {a b : ℝ}, a < b → Cardinal.mk ↑(Set.Ioo a b) = Cardinal.continuum
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.trans_h₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ φ₃ : S₁ ⟶ S₂} (h₁₂ : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂)
  (h₂₃ : CategoryTheory.ShortComplex.Homotopy φ₂ φ₃), (h₁₂.trans h₂₃).h₃ = h₁₂.h₃ + h₂₃.h₃
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ReducePostconditionInductionMotive : {n : ℕ} →
  Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) →
    Array Std.Tactic.BVDecide.LRAT.Internal.Assignment →
      ℕ → Std.Tactic.BVDecide.LRAT.Internal.ReduceResult (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → Prop
-- Mathlib.Testing.Plausible.Testable
Plausible.Fact.printableProp : {p : Prop} → [Plausible.PrintableProp p] → Plausible.PrintableProp (Fact p)
-- Mathlib.SetTheory.Ordinal.Notation
instDecidableEqNONote : DecidableEq NONote
-- Mathlib.Geometry.Convex.Cone.Basic
/-- A convex cone `C` is generating if its linear span is the entire `R`-module `M`.

`IsGenerating` is equivalent to `IsReproducing` modulo some conditions.
See `IsReproducing.isGenerating` and `IsGenerating.isReproducing` for details.  -/
ConvexCone.IsGenerating : {R : Type u_2} →
  {M : Type u_4} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] → [inst_2 : AddCommMonoid M] → [inst_3 : Module R M] → ConvexCone R M → Prop
-- Mathlib.AlgebraicGeometry.StructureSheaf
_private.Mathlib.AlgebraicGeometry.StructureSheaf.0.AlgebraicGeometry.StructureSheaf.isIso_toBasicOpenₗ : ∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : R),
  CategoryTheory.IsIso (ModuleCat.ofHom (AlgebraicGeometry.StructureSheaf.toBasicOpenₗ✝ R M f))
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.GrothendieckTopology.Point.sheafFiberCompIso_hom_app : ∀ {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] {B : Type u''}
  [inst_2 : CategoryTheory.Category.{v'', u''} B] [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A]
  [inst_4 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} B] (F : CategoryTheory.Functor A B)
  [inst_5 : CategoryTheory.LocallySmall.{w, v, u} C]
  [inst_6 : CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v'', u', u''} F]
  [inst_7 : J.HasSheafCompose F] (X : CategoryTheory.Sheaf J A),
  (Φ.sheafFiberCompIso F).hom.app X =
    CategoryTheory.CategoryStruct.comp ((Φ.presheafFiberCompIso F).hom.app X.obj)
      (CategoryTheory.CategoryStruct.id (F.obj (Φ.presheafFiber.obj X.obj)))
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.foldl_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} {δ : Type w} [Std.TransCmp cmp] {f : δ → α → δ}
  {init : δ}, t₁.Equiv t₂ → Std.TreeSet.foldl f init t₁ = Std.TreeSet.foldl f init t₂
-- Mathlib.Order.Partition.Basic
Partition.bot_lt_of_mem : ∀ {α : Type u_1} {s x : α} [inst : CompleteLattice α] {P : Partition s}, x ∈ P → ⊥ < x
-- Mathlib.Tactic.Translate.Reorder
/-- Two reorders are considered equal if all permutations are the same.  -/
Mathlib.Tactic.Translate.ArgReorder.beq : Mathlib.Tactic.Translate.ArgReorder → Mathlib.Tactic.Translate.ArgReorder → Bool
-- Mathlib.Analysis.Polynomial.MahlerMeasure
Polynomial.logMahlerMeasure_X : Polynomial.X.logMahlerMeasure = 0
-- Mathlib.Algebra.NonAssoc.LieAdmissible.Defs
/-- A `LieAdmissibleAlgebra` is a `LieAdmissibleRing` equipped with a compatible action by scalars
from a commutative ring.  -/
LieAdmissibleAlgebra : (R : Type u_1) → (L : Type u_2) → [CommRing R] → [LieAdmissibleRing L] → Type (max u_1 u_2)
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
CategoryTheory.instPreservesLimitsOfShapeCostructuredArrowOverToOverOfIsConnectedOfHasLimitsOfShape : ∀ {J : Type u'} [inst : CategoryTheory.Category.{v', u'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {D : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} D] {K : CategoryTheory.Functor C D} {B : D}
  [CategoryTheory.IsConnected J] [CategoryTheory.Limits.HasLimitsOfShape J C]
  [CategoryTheory.Limits.PreservesLimitsOfShape J K],
  CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.CostructuredArrow.toOver K B)
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.coe_ofNat : ∀ {α : Type u} [inst : AddMonoidWithOne α] (n : ℕ) [inst_1 : n.AtLeastTwo], ↑(OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.IsMultiplicative.unop : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty Cᵒᵖ) [W.IsMultiplicative],
  W.unop.IsMultiplicative
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey_alterKey_eq_self : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [inst_3 : Std.LawfulBEqOrd α]
  [inst_4 : Std.LawfulEqOrd α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {f : Option (β k) → Option (β k)} {he : (Std.Internal.List.alterKey k f l).isEmpty = false},
      Std.Internal.List.maxKey (Std.Internal.List.alterKey k f l) he = k ↔
        (f (Std.Internal.List.getValueCast? k l)).isSome = true ∧
          ∀ (k' : α), Std.Internal.List.containsKey k' l = true → (compare k' k).isLE = true
-- Mathlib.Logic.Unique
Unique.default_eq : ∀ {α : Sort u_1} [inst : Unique α] (a : α), default = a
-- Init.Data.Nat.Internal.SOM
Nat.Internal.SOM.Expr.brecOn.go : {motive : Nat.Internal.SOM.Expr → Sort u} →
  (t : Nat.Internal.SOM.Expr) →
    ((t : Nat.Internal.SOM.Expr) → Nat.Internal.SOM.Expr.below t → motive t) → motive t ×' Nat.Internal.SOM.Expr.below t
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
/-- The logarithmic counting function `logCounting f ⊤` is the logarithmic counting function associated
with the pole-divisor of `f`.
 -/
ValueDistribution.logCounting_top : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : ProperSpace 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {f : 𝕜 → E},
  ValueDistribution.logCounting f ⊤ = Function.locallyFinsuppWithin.logCounting (MeromorphicOn.divisor f Set.univ)⁻
-- Mathlib.Analysis.Calculus.Deriv.Abs
HasFDerivWithinAt.abs_of_pos : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {s : Set E}
  {x : E}, HasFDerivWithinAt f f' s x → 0 < f x → HasFDerivWithinAt (fun x => |f x|) f' s x
-- Init.Data.Array.Find
Array.findIdx_le_findIdx : ∀ {α : Type u_1} {xs : Array α} {p q : α → Bool},
  (∀ x ∈ xs, p x = true → q x = true) → Array.findIdx q xs ≤ Array.findIdx p xs
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.IsTangentAt.inner_left_eq_zero_of_mem : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p : P} {as : AffineSubspace ℝ P},
  s.IsTangentAt p as → ∀ {x : P}, x ∈ as → inner ℝ (x -ᵥ p) (p -ᵥ s.center) = 0
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get?_eq_some_of_contains : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α],
  m.WF → ∀ {k : α}, m.contains k = true → m.get? k = some k
-- Init.Prelude
/-- The `save` implementation for `Backtrackable PUnit σ`.  -/
EStateM.dummySave : {σ : Type u} → σ → PUnit.{u_1}
-- Mathlib.Topology.Algebra.Group.Basic
isClosedMap_mul_left : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [SeparatelyContinuousMul G] (a : G),
  IsClosedMap fun x => a * x
-- Mathlib.Order.Bounded
Set.unbounded_lt_inter_lt : ∀ {α : Type u_1} {s : Set α} [inst : LinearOrder α] [NoMaxOrder α] (a : α),
  Set.Unbounded (fun x1 x2 => x1 < x2) (s ∩ {b | a < b}) ↔ Set.Unbounded (fun x1 x2 => x1 < x2) s
-- Mathlib.Computability.TuringDegree
TuringEquivalent.refl : ∀ (f : ℕ →. ℕ), TuringEquivalent f f
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
/-- If the left cosets of `t` by elements of `s` are disjoint (but not necessarily distinct!), then
the size of `t` divides the size of `s • t`.  -/
Finset.card_dvd_card_smul_right : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : Group α] [inst_2 : MulAction α β] {t : Finset β}
  {s : Finset α}, ((fun x => x • t) '' ↑s).PairwiseDisjoint id → t.card ∣ (s • t).card
-- ProofWidgets.Cancellable
ProofWidgets.CheckRequestResponse.running.sizeOf_spec : sizeOf ProofWidgets.CheckRequestResponse.running = 1
-- Mathlib.Analysis.Complex.Periodic
Function.Periodic.cuspFunction_zero_eq_limUnder_nhds_ne : ∀ (h : ℝ) (f : ℂ → ℂ),
  Function.Periodic.cuspFunction h f 0 = (nhdsWithin 0 {0}ᶜ).limUnder (Function.Periodic.cuspFunction h f)
-- Mathlib.NumberTheory.SelbergSieve
BoundingSieve.prod_primeFactors_nu : ∀ {s : BoundingSieve} {d : ℕ}, d ∣ s.prodPrimes → ∏ p ∈ d.primeFactors, s.nu p = s.nu d
-- Mathlib.Algebra.Ring.Action.Subobjects
/-- A stronger version of `Subgroup.distribMulAction`.  -/
Subgroup.mulSemiringAction : {G : Type u_2} →
  {R : Type u_3} →
    [inst : Group G] → [inst_1 : Semiring R] → [MulSemiringAction G R] → (H : Subgroup G) → MulSemiringAction (↥H) R
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Char
String.Slice.Pos.skip?_char_eq_some_iff : ∀ {c : Char} {s : String.Slice} {pos res : s.Pos},
  pos.skip? c = some res ↔ ∃ (h : pos ≠ s.endPos), res = pos.next h ∧ pos.get h = c
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.opEquivOpOver_counitIso : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] (X : T),
  (CategoryTheory.Under.opEquivOpOver X).counitIso =
    CategoryTheory.Iso.refl
      ({ obj := fun Y => CategoryTheory.Under.mk (Opposite.unop Y).hom.op,
            map := fun {Z Y} f => CategoryTheory.Under.homMk (CategoryTheory.Over.Hom.left f.unop).op ⋯, map_id := ⋯,
            map_comp := ⋯ }.comp
        { obj := fun Y => Opposite.op (CategoryTheory.Over.mk Y.hom.unop),
          map := fun {Z Y} f => Opposite.op (CategoryTheory.Over.homMk (CategoryTheory.Under.Hom.right f).unop ⋯),
          map_id := ⋯, map_comp := ⋯ })
-- Mathlib.Data.ZMod.ValMinAbs
ZMod.valMinAbs_natCast_of_half_lt : ∀ {n a : ℕ}, n / 2 < a → a < n → (↑a).valMinAbs = ↑a - ↑n
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.leftComm_symm_tmul : ∀ {R : Type uR} {A : Type uA} {B : Type uB} {C : Type uC} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : Semiring C] [inst_6 : Algebra R C]
  (m : A) (n : B) (p : C), (Algebra.TensorProduct.leftComm R A B C).symm (n ⊗ₜ[R] (m ⊗ₜ[R] p)) = m ⊗ₜ[R] (n ⊗ₜ[R] p)
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.OplaxTrans.Hom.of.injEq : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} (as as_1 : CategoryTheory.Oplax.OplaxTrans.Modification η θ),
  ({ as := as } = { as := as_1 }) = (as = as_1)
-- Mathlib.RingTheory.DedekindDomain.Dvr
IsLocalization.AtPrime.not_isField : ∀ (A : Type u_1) [inst : CommRing A] [IsDomain A] {P : Ideal A},
  P ≠ ⊥ →
    ∀ [pP : P.IsPrime] (Aₘ : Type u_2) [inst_2 : CommRing Aₘ] [inst_3 : Algebra A Aₘ] [IsLocalization.AtPrime Aₘ P],
      ¬IsField Aₘ
-- Mathlib.Data.Finset.Filter
/-- If all elements of a `Finset` satisfy the predicate `p`, `s.filter p` is `s`.  -/
Finset.filter_true_of_mem : ∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {s : Finset α}, (∀ x ∈ s, p x) → Finset.filter p s = s
-- Mathlib.Algebra.Group.End
/-- **Alias** of `AddAut.addConj_neg_apply`. -/
AddAut.conj_inv_apply : ∀ {G : Type u_3} [inst : AddGroup G] (g h : G), (-AddAut.addConj g) h = -g + h + g
-- Mathlib.Order.DirSupClosed
DirSupClosed.mem_imp_of_antisymmRel : ∀ {α : Type u_1} {s : Set α} [inst : Preorder α],
  DirSupClosed s → ∀ {a b : α}, AntisymmRel (fun x1 x2 => x1 ≤ x2) a b → a ∈ s → b ∈ s
-- Init.Notation
/-- The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. -/
«term_×_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Homology.ComplexShapeSigns
ComplexShape.next_add : ∀ {I : Type u_7} [inst : AddMonoid I] (c : ComplexShape I) [c.TensorSigns] (p q : I),
  c.Rel p (c.next p) → c.next (p + q) = c.next p + q
-- Mathlib.Combinatorics.Enumerative.Bell
Nat.bell.eq_1 : Nat.bell 0 = 1
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse_obj_hom : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T)
  (G : CategoryTheory.Functor D T) (c : C) (Y : CategoryTheory.Comma ((CategoryTheory.Under.forget c).comp F) G),
  ((CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse F G c).obj Y).hom = Y.left.hom
-- Mathlib.RingTheory.Algebraic.Integral
/-- An integral element of an algebra is algebraic.  -/
IsIntegral.isAlgebraic : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] [Nontrivial R] {x : A},
  IsIntegral R x → IsAlgebraic R x
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instBEqDiagnosticCode : BEq Lean.Lsp.DiagnosticCode
-- Lean.Parser.Command
/-- Debugging command: Prints the result of `Environment.dumpAsyncEnvState`.  -/
Lean.Parser.Command.dumpAsyncEnvState : Lean.Parser.Parser
-- Mathlib.Tactic.Order.ToInt
Mathlib.Tactic.Order.ToInt.toInt_lt_toInt : ∀ {α : Type u_1} [inst : LinearOrder α] {n : ℕ} (val : Fin n → α) (i j : Fin n),
  Mathlib.Tactic.Order.ToInt.toInt val i < Mathlib.Tactic.Order.ToInt.toInt val j ↔ val i < val j
-- Mathlib.MeasureTheory.Covering.Differentiation
VitaliFamily.aemeasurable_limRatio : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (v : VitaliFamily μ) [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ]
  {ρ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure ρ],
  ρ.AbsolutelyContinuous μ → AEMeasurable (v.limRatio ρ) μ
-- Mathlib.Analysis.Calculus.FDeriv.Mul
/-- Eta-expanded form of `DifferentiableAt.inv` -/
DifferentiableAt.fun_inv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {R : Type u_5} [inst_3 : NormedDivisionRing R] [inst_4 : NormedAlgebra 𝕜 R] {h : E → R}
  {z : E}, DifferentiableAt 𝕜 h z → h z ≠ 0 → DifferentiableAt 𝕜 (fun i => (h i)⁻¹) z
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Subgroup.hasDetPlusMinusOne_iff_abs_det : ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {R : Type u_2} [inst_2 : CommRing R]
  (Γ : Subgroup (GL n R)) [inst_3 : LinearOrder R] [IsOrderedRing R],
  Γ.HasDetPlusMinusOne ↔ ∀ {g : GL n R}, g ∈ Γ → |↑(Matrix.GeneralLinearGroup.det g)| = 1
-- Mathlib.CategoryTheory.ObjectProperty.Equivalence
CategoryTheory.Equivalence.congrFullSubcategory_functor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {P : CategoryTheory.ObjectProperty C} {Q : CategoryTheory.ObjectProperty D} (e : C ≌ D)
  [inst_2 : Q.IsClosedUnderIsomorphisms] (h : Q.inverseImage e.functor = P),
  (e.congrFullSubcategory h).functor = Q.lift (P.ι.comp e.functor) ⋯
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.PartialEquiv.ext_iff : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  {f g : L.PartialEquiv M N},
  f = g ↔
    ∃ (h_dom : f.dom = g.dom),
      ∀ (x : M) (h : x ∈ f.dom), f.cod.subtype (f.toEquiv ⟨x, h⟩) = g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.min?_eq_getElem?_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp], t.WF → t.min? = t.toArray[0]?
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_map_equiv : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {Ω' : Type u_2} {mΩ' : MeasurableSpace Ω'} {μ : MeasureTheory.Measure Ω'}
  (X Y : Ω → ℝ) (Z : Ω' ≃ᵐ Ω),
  ProbabilityTheory.covariance X Y (MeasureTheory.Measure.map (⇑Z) μ) = ProbabilityTheory.covariance (X ∘ ⇑Z) (Y ∘ ⇑Z) μ
-- Mathlib.Combinatorics.Additive.PluenneckeRuzsa
/-- **Ruzsa's triangle inequality**. Sub-add-add version.  -/
Finset.ruzsa_triangle_inequality_sub_add_add : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : AddGroup G] (A B C : Finset G),
  (A - C).card * B.card ≤ (A + B).card * (C + B).card